Time bar (total: 10.0m)
| 49.8s | 3254× | body | 10240 | exit |
| 532.0ms | 3510× | pre | 80 | true |
| 54.0ms | 246× | body | 80 | valid |
| 6.0ms | 1× | body | 5120 | valid |
| 6.0ms | 2× | body | 1280 | valid |
| 3.0ms | 1× | body | 2560 | valid |
| 2.0ms | 3× | body | 160 | valid |
| 2.0ms | 2× | body | 320 | valid |
| 1.0ms | 1× | body | 640 | valid |
| Iter | Nodes |
|---|---|
| done | 5005 |
| 3 | 743 |
| 2 | 143 |
| 1 | 54 |
| 0 | 22 |
1 alts after pruning (1 fresh and 0 done)
Merged error: 6.9b
Found 4 expressions with local error:
| 0.0b | (pow (- 1 (/ 1 (+ 1 (exp (- s))))) c_n) |
| 0.7b | (pow (/ 1 (+ 1 (exp (- s)))) c_p) |
| 2.2b | (pow (/ 1 (+ 1 (exp (- t)))) c_p) |
| 3.7b | (/ (* (pow (/ 1 (+ 1 (exp (- s)))) c_p) (pow (- 1 (/ 1 (+ 1 (exp (- s))))) c_n)) (* (pow (/ 1 (+ 1 (exp (- t)))) c_p) (pow (- 1 (/ 1 (+ 1 (exp (- t))))) c_n))) |
| 5829× | times-frac |
| 5603× | add-sqr-sqrt |
| 5035× | unpow-prod-down |
| 3408× | *-un-lft-identity |
| 2552× | associate-*l* |
| 1740× | associate-*r* unswap-sqr |
| 1416× | add-cube-cbrt |
| 1193× | add-exp-log |
| 1163× | sqr-pow |
| 702× | difference-of-squares |
| 693× | pow-exp |
| 684× | prod-exp |
| 593× | div-exp |
| 354× | distribute-lft-out |
| 345× | pow-to-exp |
| 236× | associate-/r/ div-inv |
| 234× | distribute-lft-out-- |
| 118× | flip3-+ flip-+ |
| 116× | rec-exp 1-exp *-commutative |
| 57× | associate-/r* associate-/l* |
| 16× | add-cbrt-cube |
| 9× | pow1 pow-unpow |
| 7× | pow-pow |
| 4× | expm1-log1p-u cbrt-undiv cbrt-unprod insert-posit16 log1p-expm1-u add-log-exp |
| 2× | pow-flip inv-pow |
| 1× | clear-num frac-2neg |
| 83.0ms | (pow (- 1 (/ 1 (+ 1 (exp (- s))))) c_n) |
| 26.0ms | (pow (/ 1 (+ 1 (exp (- s)))) c_p) |
| 27.0ms | (pow (/ 1 (+ 1 (exp (- t)))) c_p) |
| 1.8s | (/ (* (pow (/ 1 (+ 1 (exp (- s)))) c_p) (pow (- 1 (/ 1 (+ 1 (exp (- s))))) c_n)) (* (pow (/ 1 (+ 1 (exp (- t)))) c_p) (pow (- 1 (/ 1 (+ 1 (exp (- t))))) c_n))) |
| 68.0ms | (pow (- 1 (/ 1 (+ 1 (exp (- s))))) c_n) |
| 57.0ms | (pow (/ 1 (+ 1 (exp (- s)))) c_p) |
| 59.0ms | (pow (/ 1 (+ 1 (exp (- t)))) c_p) |
| 540.0ms | (/ (* (pow (/ 1 (+ 1 (exp (- s)))) c_p) (pow (- 1 (/ 1 (+ 1 (exp (- s))))) c_n)) (* (pow (/ 1 (+ 1 (exp (- t)))) c_p) (pow (- 1 (/ 1 (+ 1 (exp (- t))))) c_n))) |
| Iter | Nodes |
|---|---|
| done | 5000 |
| 0 | 4958 |
5 alts after pruning (5 fresh and 0 done)
Merged error: 0.3b
Found 4 expressions with local error:
| 0.3b | (log (- 1 (/ 1 (+ 1 (exp (- t)))))) |
| 0.7b | (log (/ 1 (+ 1 (exp (- s))))) |
| 2.2b | (log (/ 1 (+ 1 (exp (- t))))) |
| 10.1b | (- (+ (* (log (/ 1 (+ 1 (exp (- s))))) c_p) (* (log (- 1 (/ 1 (+ 1 (exp (- s)))))) c_n)) (+ (* (log (/ 1 (+ 1 (exp (- t))))) c_p) (* (log (- 1 (/ 1 (+ 1 (exp (- t)))))) c_n))) |
| 636× | *-un-lft-identity |
| 540× | associate-*l* |
| 413× | distribute-lft-out |
| 279× | pow1 |
| 277× | log-pow |
| 144× | prod-diff |
| 102× | distribute-lft-out-- |
| 63× | add-sqr-sqrt |
| 50× | add-cube-cbrt |
| 47× | log-prod |
| 28× | times-frac |
| 22× | log-div |
| 16× | add-log-exp |
| 15× | add-exp-log |
| 12× | fma-neg |
| 9× | rem-log-exp |
| 8× | associate-/r* associate-/l* |
| 7× | difference-of-squares |
| 6× | flip3-+ log-rec flip-+ |
| 4× | expm1-log1p-u clear-num sum-log add-cbrt-cube diff-log div-exp associate-/r/ frac-sub insert-posit16 log1p-expm1-u |
| 3× | div-inv |
| 2× | +-commutative rec-exp sub-neg frac-2neg log1p-def flip3-- 1-exp associate--l+ pow-flip flip-- associate--r+ inv-pow |
| 52.0ms | (log (- 1 (/ 1 (+ 1 (exp (- t)))))) |
| 24.0ms | (log (/ 1 (+ 1 (exp (- s))))) |
| 24.0ms | (log (/ 1 (+ 1 (exp (- t))))) |
| 1.1s | (- (+ (* (log (/ 1 (+ 1 (exp (- s))))) c_p) (* (log (- 1 (/ 1 (+ 1 (exp (- s)))))) c_n)) (+ (* (log (/ 1 (+ 1 (exp (- t))))) c_p) (* (log (- 1 (/ 1 (+ 1 (exp (- t)))))) c_n))) |
| 71.0ms | (log (- 1 (/ 1 (+ 1 (exp (- t)))))) |
| 61.0ms | (log (/ 1 (+ 1 (exp (- s))))) |
| 57.0ms | (log (/ 1 (+ 1 (exp (- t))))) |
| 323.0ms | (- (+ (* (log (/ 1 (+ 1 (exp (- s))))) c_p) (* (log (- 1 (/ 1 (+ 1 (exp (- s)))))) c_n)) (+ (* (log (/ 1 (+ 1 (exp (- t))))) c_p) (* (log (- 1 (/ 1 (+ 1 (exp (- t)))))) c_n))) |
| Iter | Nodes |
|---|---|
| done | 5001 |
| 2 | 2784 |
| 1 | 948 |
| 0 | 388 |
5 alts after pruning (5 fresh and 0 done)
Merged error: 0.0b
Found 4 expressions with local error:
| 0.3b | (log (- 1 (/ 1 (+ 1 (exp (- s)))))) |
| 0.3b | (log (- 1 (/ 1 (+ 1 (exp (- t)))))) |
| 0.7b | (log (/ 1 (+ 1 (exp (- s))))) |
| 10.1b | (- (+ (* (log (/ 1 (+ 1 (exp (- s))))) c_p) (* (log (- 1 (/ 1 (+ 1 (exp (- s)))))) c_n)) (+ (* (fma (* t t) -1/8 (fma 1/2 t (log 1/2))) c_p) (* (log (- 1 (/ 1 (+ 1 (exp (- t)))))) c_n))) |
| 504× | *-un-lft-identity |
| 358× | associate-*l* |
| 289× | distribute-lft-out |
| 154× | pow1 |
| 151× | log-pow |
| 108× | prod-diff |
| 74× | distribute-lft-out-- |
| 62× | add-sqr-sqrt |
| 40× | log-prod |
| 38× | add-cube-cbrt |
| 20× | times-frac |
| 16× | add-log-exp |
| 14× | log-div |
| 13× | difference-of-squares |
| 12× | fma-neg |
| 11× | add-exp-log |
| 6× | rem-log-exp |
| 5× | flip3-+ flip-+ |
| 4× | expm1-log1p-u associate-/r* sum-log log1p-def add-cbrt-cube diff-log frac-sub insert-posit16 log1p-expm1-u associate-/l* |
| 3× | sub-neg flip3-- log-rec div-inv flip-- |
| 2× | +-commutative clear-num div-exp associate--l+ associate-/r/ associate--r+ |
| 1× | rec-exp frac-2neg 1-exp pow-flip inv-pow |
| 52.0ms | (log (- 1 (/ 1 (+ 1 (exp (- s)))))) |
| 52.0ms | (log (- 1 (/ 1 (+ 1 (exp (- t)))))) |
| 24.0ms | (log (/ 1 (+ 1 (exp (- s))))) |
| 934.0ms | (- (+ (* (log (/ 1 (+ 1 (exp (- s))))) c_p) (* (log (- 1 (/ 1 (+ 1 (exp (- s)))))) c_n)) (+ (* (fma (* t t) -1/8 (fma 1/2 t (log 1/2))) c_p) (* (log (- 1 (/ 1 (+ 1 (exp (- t)))))) c_n))) |
| 71.0ms | (log (- 1 (/ 1 (+ 1 (exp (- s)))))) |
| 71.0ms | (log (- 1 (/ 1 (+ 1 (exp (- t)))))) |
| 62.0ms | (log (/ 1 (+ 1 (exp (- s))))) |
| 395.0ms | (- (+ (* (log (/ 1 (+ 1 (exp (- s))))) c_p) (* (log (- 1 (/ 1 (+ 1 (exp (- s)))))) c_n)) (+ (* (fma (* t t) -1/8 (fma 1/2 t (log 1/2))) c_p) (* (log (- 1 (/ 1 (+ 1 (exp (- t)))))) c_n))) |
| Iter | Nodes |
|---|---|
| done | 5001 |
| 2 | 2923 |
| 1 | 918 |
| 0 | 377 |
4 alts after pruning (4 fresh and 0 done)
Merged error: 0.0b
Found 4 expressions with local error:
| 0.5b | (* c_n (log1p (/ -1 (+ (exp (- t)) 1)))) |
| 0.7b | (log1p (exp (- s))) |
| 7.8b | (- (fma c_n (log1p (/ -1 (+ (exp (- s)) 1))) (- (* (- c_p) (log1p (exp (- s)))) (* c_n (log1p (/ -1 (+ (exp (- t)) 1)))))) (* (fma (* t t) -1/8 (fma 1/2 t (log 1/2))) c_p)) |
| 23.6b | (fma c_n (log1p (/ -1 (+ (exp (- s)) 1))) (- (* (- c_p) (log1p (exp (- s)))) (* c_n (log1p (/ -1 (+ (exp (- t)) 1)))))) |
| 41× | add-sqr-sqrt |
| 36× | prod-diff |
| 32× | *-un-lft-identity |
| 28× | add-cube-cbrt |
| 13× | associate-*l* |
| 12× | associate-*r* |
| 6× | pow1 add-cbrt-cube add-exp-log add-log-exp |
| 5× | expm1-log1p-u unswap-sqr |
| 4× | *-commutative insert-posit16 log1p-expm1-u |
| 3× | fma-neg |
| 2× | fma-udef distribute-lft-out-- difference-of-squares |
| 1× | log1p-udef sub-neg flip3-- diff-log pow-prod-down prod-exp associate--l+ log1p-expm1 cbrt-unprod flip-- |
| 7.0ms | (* c_n (log1p (/ -1 (+ (exp (- t)) 1)))) |
| 0.0ms | (log1p (exp (- s))) |
| 16.0ms | (- (fma c_n (log1p (/ -1 (+ (exp (- s)) 1))) (- (* (- c_p) (log1p (exp (- s)))) (* c_n (log1p (/ -1 (+ (exp (- t)) 1)))))) (* (fma (* t t) -1/8 (fma 1/2 t (log 1/2))) c_p)) |
| 0.0ms | (fma c_n (log1p (/ -1 (+ (exp (- s)) 1))) (- (* (- c_p) (log1p (exp (- s)))) (* c_n (log1p (/ -1 (+ (exp (- t)) 1)))))) |
| 71.0ms | (* c_n (log1p (/ -1 (+ (exp (- t)) 1)))) |
| 51.0ms | (log1p (exp (- s))) |
| 402.0ms | (- (fma c_n (log1p (/ -1 (+ (exp (- s)) 1))) (- (* (- c_p) (log1p (exp (- s)))) (* c_n (log1p (/ -1 (+ (exp (- t)) 1)))))) (* (fma (* t t) -1/8 (fma 1/2 t (log 1/2))) c_p)) |
| 243.0ms | (fma c_n (log1p (/ -1 (+ (exp (- s)) 1))) (- (* (- c_p) (log1p (exp (- s)))) (* c_n (log1p (/ -1 (+ (exp (- t)) 1)))))) |
| Iter | Nodes |
|---|---|
| done | 5000 |
| 2 | 1571 |
| 1 | 599 |
| 0 | 263 |
4 alts after pruning (3 fresh and 1 done)
Merged error: 0.0b
| Iters | Range | Point | |
|---|---|---|---|
| 5 | 2.138597944988289e-25 | 8.405593532113127e-25 | 2.202640187188369e-25 |
| Iter | Nodes |
|---|---|
| done | 63 |
| 1 | 63 |
| 0 | 50 |
| 8.3m | 36825× | body | 10240 | exit |
| 2.0s | 39719× | pre | 80 | true |
| 633.0ms | 2801× | body | 80 | valid |
| 112.0ms | 6× | body | 5120 | valid |
| 40.0ms | 19× | body | 1280 | valid |
| 26.0ms | 7× | body | 2560 | valid |
| 21.0ms | 18× | body | 640 | valid |
| 15.0ms | 34× | body | 160 | valid |
| 5.0ms | 8× | body | 320 | valid |