Time bar (total: 7.8m)
| 54.8s | 3540× | body | 10240 | exit |
| 209.0ms | 3796× | pre | 80 | true |
| 33.0ms | 246× | body | 80 | valid |
| 7.0ms | 3× | body | 1280 | valid |
| 3.0ms | 1× | body | 2560 | valid |
| 2.0ms | 2× | body | 640 | valid |
| 2.0ms | 2× | body | 320 | valid |
| 1.0ms | 2× | body | 160 | valid |
| Iter | Nodes |
|---|---|
| done | 5002 |
| 3 | 744 |
| 2 | 143 |
| 1 | 53 |
| 0 | 22 |
1 alts after pruning (1 fresh and 0 done)
Merged error: 7.5b
Found 4 expressions with local error:
| 0.0b | (pow (- 1.0 (/ 1.0 (+ 1.0 (exp (- t))))) c_n) |
| 1.2b | (pow (/ 1.0 (+ 1.0 (exp (- s)))) c_p) |
| 1.7b | (pow (/ 1.0 (+ 1.0 (exp (- t)))) c_p) |
| 3.9b | (/ (* (pow (/ 1.0 (+ 1.0 (exp (- s)))) c_p) (pow (- 1.0 (/ 1.0 (+ 1.0 (exp (- s))))) c_n)) (* (pow (/ 1.0 (+ 1.0 (exp (- t)))) c_p) (pow (- 1.0 (/ 1.0 (+ 1.0 (exp (- t))))) c_n))) |
| 557× | add-exp-log |
| 312× | prod-exp |
| 265× | pow-exp |
| 249× | div-exp |
| 185× | pow-to-exp |
| 42× | unpow-prod-down |
| 38× | *-un-lft-identity |
| 29× | add-sqr-sqrt |
| 26× | times-frac |
| 24× | add-cube-cbrt |
| 16× | add-cbrt-cube |
| 9× | pow-unpow |
| 7× | pow1 |
| 6× | distribute-lft-out |
| 4× | cbrt-undiv associate-/r/ cbrt-unprod add-log-exp |
| 3× | pow-pow div-inv sqr-pow |
| 2× | flip3-+ flip-+ difference-of-squares |
| 1× | clear-num associate-/r* frac-2neg associate-/l* distribute-lft-out-- |
| 48.0ms | (pow (- 1.0 (/ 1.0 (+ 1.0 (exp (- t))))) c_n) |
| 16.0ms | (pow (/ 1.0 (+ 1.0 (exp (- s)))) c_p) |
| 16.0ms | (pow (/ 1.0 (+ 1.0 (exp (- t)))) c_p) |
| 141.0ms | (/ (* (pow (/ 1.0 (+ 1.0 (exp (- s)))) c_p) (pow (- 1.0 (/ 1.0 (+ 1.0 (exp (- s))))) c_n)) (* (pow (/ 1.0 (+ 1.0 (exp (- t)))) c_p) (pow (- 1.0 (/ 1.0 (+ 1.0 (exp (- t))))) c_n))) |
| 91.0ms | (pow (- 1.0 (/ 1.0 (+ 1.0 (exp (- t))))) c_n) |
| 73.0ms | (pow (/ 1.0 (+ 1.0 (exp (- s)))) c_p) |
| 74.0ms | (pow (/ 1.0 (+ 1.0 (exp (- t)))) c_p) |
| 626.0ms | (/ (* (pow (/ 1.0 (+ 1.0 (exp (- s)))) c_p) (pow (- 1.0 (/ 1.0 (+ 1.0 (exp (- s))))) c_n)) (* (pow (/ 1.0 (+ 1.0 (exp (- t)))) c_p) (pow (- 1.0 (/ 1.0 (+ 1.0 (exp (- t))))) c_n))) |
| Iter | Nodes |
|---|---|
| done | 5042 |
| 2 | 3097 |
| 1 | 1168 |
| 0 | 370 |
4 alts after pruning (4 fresh and 0 done)
Merged error: 0.0b
Found 4 expressions with local error:
| 0.0b | (pow (- 1.0 (/ 1.0 (+ 1.0 (exp (- t))))) c_n) |
| 0.2b | (* c_p (log 0.5)) |
| 1.2b | (pow (/ 1.0 (+ 1.0 (exp (- s)))) c_p) |
| 2.2b | (/ (* (pow (/ 1.0 (+ 1.0 (exp (- s)))) c_p) (pow (- 1.0 (/ 1.0 (+ 1.0 (exp (- s))))) c_n)) (* (+ (* 0.5 (* t c_p)) (+ (* c_p (log 0.5)) 1)) (pow (- 1.0 (/ 1.0 (+ 1.0 (exp (- t))))) c_n))) |
| 172× | add-exp-log |
| 88× | prod-exp |
| 65× | div-exp |
| 56× | pow-exp |
| 43× | pow-to-exp |
| 27× | *-un-lft-identity |
| 26× | add-sqr-sqrt |
| 24× | unpow-prod-down |
| 19× | add-cube-cbrt |
| 18× | add-cbrt-cube |
| 14× | times-frac |
| 9× | pow1 |
| 6× | pow-unpow log-prod |
| 5× | cbrt-unprod |
| 4× | cbrt-undiv associate-*r* associate-/r/ add-log-exp |
| 3× | distribute-rgt-in distribute-lft-in associate-*l* distribute-lft-out |
| 2× | pow-pow flip3-+ associate-*l/ flip-+ div-inv difference-of-squares sqr-pow |
| 1× | clear-num associate-/r* frac-2neg pow-prod-down log-pow *-commutative associate-/l* distribute-lft-out-- unswap-sqr |
| 47.0ms | (pow (- 1.0 (/ 1.0 (+ 1.0 (exp (- t))))) c_n) |
| 7.0ms | (* c_p (log 0.5)) |
| 16.0ms | (pow (/ 1.0 (+ 1.0 (exp (- s)))) c_p) |
| 143.0ms | (/ (* (pow (/ 1.0 (+ 1.0 (exp (- s)))) c_p) (pow (- 1.0 (/ 1.0 (+ 1.0 (exp (- s))))) c_n)) (* (+ (* 0.5 (* t c_p)) (+ (* c_p (log 0.5)) 1)) (pow (- 1.0 (/ 1.0 (+ 1.0 (exp (- t))))) c_n))) |
| 95.0ms | (pow (- 1.0 (/ 1.0 (+ 1.0 (exp (- t))))) c_n) |
| 166.0ms | (* c_p (log 0.5)) |
| 74.0ms | (pow (/ 1.0 (+ 1.0 (exp (- s)))) c_p) |
| 754.0ms | (/ (* (pow (/ 1.0 (+ 1.0 (exp (- s)))) c_p) (pow (- 1.0 (/ 1.0 (+ 1.0 (exp (- s))))) c_n)) (* (+ (* 0.5 (* t c_p)) (+ (* c_p (log 0.5)) 1)) (pow (- 1.0 (/ 1.0 (+ 1.0 (exp (- t))))) c_n))) |
| Iter | Nodes |
|---|---|
| done | 5003 |
| 2 | 3707 |
| 1 | 1022 |
| 0 | 342 |
3 alts after pruning (3 fresh and 0 done)
Merged error: 0.0b
Found 4 expressions with local error:
| 0.0b | (/ 1.0 (+ 1.0 (exp (- s)))) |
| 0.2b | (* c_p (log 0.5)) |
| 0.2b | (* c_n (log 0.5)) |
| 1.2b | (pow (/ 1.0 (+ 1.0 (exp (- s)))) c_p) |
| 44× | *-un-lft-identity |
| 34× | add-sqr-sqrt |
| 30× | add-cube-cbrt |
| 24× | times-frac |
| 18× | unpow-prod-down |
| 13× | add-exp-log |
| 12× | log-prod |
| 11× | pow1 |
| 10× | add-cbrt-cube |
| 8× | associate-*r* |
| 7× | distribute-lft-out |
| 6× | distribute-rgt-in distribute-lft-in associate-*l* |
| 4× | associate-/r* associate-/r/ add-log-exp |
| 3× | pow-unpow associate-/l* |
| 2× | flip3-+ div-exp pow-prod-down pow-exp prod-exp log-pow *-commutative cbrt-unprod flip-+ div-inv unswap-sqr |
| 1× | pow-to-exp cbrt-undiv clear-num pow-pow frac-2neg sqr-pow |
| 14.0ms | (/ 1.0 (+ 1.0 (exp (- s)))) |
| 11.0ms | (* c_p (log 0.5)) |
| 7.0ms | (* c_n (log 0.5)) |
| 16.0ms | (pow (/ 1.0 (+ 1.0 (exp (- s)))) c_p) |
| 29.0ms | (/ 1.0 (+ 1.0 (exp (- s)))) |
| 178.0ms | (* c_p (log 0.5)) |
| 180.0ms | (* c_n (log 0.5)) |
| 79.0ms | (pow (/ 1.0 (+ 1.0 (exp (- s)))) c_p) |
| Iter | Nodes |
|---|---|
| done | 5002 |
| 3 | 4424 |
| 2 | 1373 |
| 1 | 553 |
| 0 | 207 |
3 alts after pruning (2 fresh and 1 done)
Merged error: 0.0b
Found 4 expressions with local error:
| 0.0b | (pow (sqrt (- 1.0 (/ 1.0 (+ 1.0 (exp (- t)))))) c_n) |
| 0.2b | (* c_p (log 0.5)) |
| 1.2b | (pow (/ 1.0 (+ 1.0 (exp (- s)))) c_p) |
| 2.2b | (/ (* (pow (/ 1.0 (+ 1.0 (exp (- s)))) c_p) (pow (- 1.0 (/ 1.0 (+ 1.0 (exp (- s))))) c_n)) (* (+ (* 0.5 (* t c_p)) (+ (* c_p (log 0.5)) 1)) (* (pow (sqrt (- 1.0 (/ 1.0 (+ 1.0 (exp (- t)))))) c_n) (pow (sqrt (- 1.0 (/ 1.0 (+ 1.0 (exp (- t)))))) c_n)))) |
| 553× | add-exp-log |
| 380× | prod-exp |
| 191× | pow-exp |
| 177× | div-exp |
| 157× | pow-to-exp |
| 28× | *-un-lft-identity |
| 27× | add-sqr-sqrt unpow-prod-down add-cbrt-cube |
| 20× | add-cube-cbrt |
| 14× | times-frac |
| 10× | pow1 cbrt-unprod |
| 6× | cbrt-undiv pow-unpow log-prod sqrt-prod |
| 4× | pow-pow associate-*r* associate-/r/ add-log-exp |
| 3× | distribute-rgt-in distribute-lft-in associate-*l* distribute-lft-out |
| 2× | flip3-+ associate-*l/ flip-+ div-inv difference-of-squares sqr-pow |
| 1× | clear-num associate-/r* frac-2neg sqrt-pow1 pow1/2 pow-prod-down log-pow *-commutative sqrt-pow2 associate-/l* distribute-lft-out-- unswap-sqr |
| 48.0ms | (pow (sqrt (- 1.0 (/ 1.0 (+ 1.0 (exp (- t)))))) c_n) |
| 6.0ms | (* c_p (log 0.5)) |
| 16.0ms | (pow (/ 1.0 (+ 1.0 (exp (- s)))) c_p) |
| 392.0ms | (/ (* (pow (/ 1.0 (+ 1.0 (exp (- s)))) c_p) (pow (- 1.0 (/ 1.0 (+ 1.0 (exp (- s))))) c_n)) (* (+ (* 0.5 (* t c_p)) (+ (* c_p (log 0.5)) 1)) (* (pow (sqrt (- 1.0 (/ 1.0 (+ 1.0 (exp (- t)))))) c_n) (pow (sqrt (- 1.0 (/ 1.0 (+ 1.0 (exp (- t)))))) c_n)))) |
| 154.0ms | (pow (sqrt (- 1.0 (/ 1.0 (+ 1.0 (exp (- t)))))) c_n) |
| 171.0ms | (* c_p (log 0.5)) |
| 75.0ms | (pow (/ 1.0 (+ 1.0 (exp (- s)))) c_p) |
| 829.0ms | (/ (* (pow (/ 1.0 (+ 1.0 (exp (- s)))) c_p) (pow (- 1.0 (/ 1.0 (+ 1.0 (exp (- s))))) c_n)) (* (+ (* 0.5 (* t c_p)) (+ (* c_p (log 0.5)) 1)) (* (pow (sqrt (- 1.0 (/ 1.0 (+ 1.0 (exp (- t)))))) c_n) (pow (sqrt (- 1.0 (/ 1.0 (+ 1.0 (exp (- t)))))) c_n)))) |
| Iter | Nodes |
|---|---|
| done | 5227 |
| 2 | 4320 |
| 1 | 1191 |
| 0 | 396 |
4 alts after pruning (2 fresh and 2 done)
Merged error: 0.0b
| Iter | Nodes |
|---|---|
| done | 71 |
| 1 | 71 |
| 0 | 50 |
| 6.5m | 30071× | body | 10240 | exit |
| 2.0s | 32421× | pre | 80 | true |
| 288.0ms | 2274× | body | 80 | valid |
| 43.0ms | 7× | body | 2560 | valid |
| 25.0ms | 4× | body | 5120 | valid |
| 22.0ms | 12× | body | 1280 | valid |
| 19.0ms | 23× | body | 640 | valid |
| 7.0ms | 25× | body | 160 | valid |
| 2.0ms | 5× | body | 320 | valid |