Time bar (total: 3.9m)
| 1.1m | 3344× | body | 10240 | exit |
| 304.0ms | 3600× | pre | 80 | true |
| 90.0ms | 250× | body | 80 | valid |
| 9.0ms | 1× | body | 2560 | valid |
| 3.0ms | 4× | body | 160 | valid |
| 1.0ms | 1× | body | 320 | valid |
| 286.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))) |
1 alts after pruning (1 fresh and 0 done)
Merged error: 4.2b
Found 4 expressions with local error:
| 2.2b | (/ (* (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))) |
| 1.0b | (pow (/ 1 (+ 1 (exp (- t)))) c_p) |
| 0.5b | (pow (/ 1 (+ 1 (exp (- s)))) c_p) |
| 0.3b | (- 1 (/ 1 (+ 1 (exp (- s))))) |
| 1192× | add-exp-log |
| 692× | pow-exp |
| 684× | prod-exp |
| 593× | div-exp |
| 344× | pow-to-exp |
| 116× | rec-exp 1-exp |
| 103× | *-un-lft-identity |
| 76× | add-sqr-sqrt |
| 65× | times-frac add-cube-cbrt |
| 54× | prod-diff |
| 36× | unpow-prod-down |
| 16× | add-cbrt-cube |
| 15× | distribute-lft-out |
| 10× | associate-/r/ |
| 8× | pow1 |
| 7× | div-inv |
| 6× | pow-unpow pow-pow add-log-exp difference-of-squares |
| 5× | flip3-+ flip-+ |
| 4× | expm1-log1p-u cbrt-undiv cbrt-unprod insert-posit16 log1p-expm1-u |
| 3× | fma-neg |
| 2× | pow-flip distribute-lft-out-- inv-pow sqr-pow |
| 1× | clear-num associate-/r* sub-neg frac-2neg flip3-- diff-log flip-- associate-/l* |
| 178.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))) |
| 41.0ms | (- 1 (/ 1 (+ 1 (exp (- s))))) |
| 21.0ms | (pow (/ 1 (+ 1 (exp (- t)))) c_p) |
| 18.0ms | (pow (/ 1 (+ 1 (exp (- s)))) c_p) |
| 579.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))) |
| 62.0ms | (pow (/ 1 (+ 1 (exp (- s)))) c_p) |
| 61.0ms | (pow (/ 1 (+ 1 (exp (- t)))) c_p) |
| 29.0ms | (- 1 (/ 1 (+ 1 (exp (- s))))) |
| 3.2s | (/ (* (* (* (pow (/ 1 (+ 1 (exp (- s)))) c_p) (pow (- 1 (/ 1 (+ 1 (exp (- s))))) c_n)) (* (pow (/ 1 (+ 1 (exp (- s)))) c_p) (pow (- 1 (/ 1 (+ 1 (exp (- s))))) c_n))) (* (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)) (* (pow (/ 1 (+ 1 (exp (- t)))) c_p) (pow (- 1 (/ 1 (+ 1 (exp (- t))))) c_n))) (* (pow (/ 1 (+ 1 (exp (- t)))) c_p) (pow (- 1 (/ 1 (+ 1 (exp (- t))))) c_n)))) |
| 2.8s | (/ (* (* (* (pow (/ 1 (+ 1 (exp (- s)))) c_p) (pow (/ 1 (+ 1 (exp (- s)))) c_p)) (pow (/ 1 (+ 1 (exp (- s)))) c_p)) (* (* (pow (- 1 (/ 1 (+ 1 (exp (- s))))) c_n) (pow (- 1 (/ 1 (+ 1 (exp (- s))))) c_n)) (pow (- 1 (/ 1 (+ 1 (exp (- s))))) c_n))) (* (* (* (pow (/ 1 (+ 1 (exp (- t)))) c_p) (pow (- 1 (/ 1 (+ 1 (exp (- t))))) c_n)) (* (pow (/ 1 (+ 1 (exp (- t)))) c_p) (pow (- 1 (/ 1 (+ 1 (exp (- t))))) c_n))) (* (pow (/ 1 (+ 1 (exp (- t)))) c_p) (pow (- 1 (/ 1 (+ 1 (exp (- t))))) c_n)))) |
| 2.6s | (/ (* (* (* (pow (/ 1 (+ 1 (exp (- s)))) c_p) (pow (/ 1 (+ 1 (exp (- s)))) c_p)) (pow (/ 1 (+ 1 (exp (- s)))) c_p)) (* (* (pow (- 1 (/ 1 (+ 1 (exp (- s))))) c_n) (pow (- 1 (/ 1 (+ 1 (exp (- s))))) c_n)) (pow (- 1 (/ 1 (+ 1 (exp (- s))))) c_n))) (* (* (* (pow (/ 1 (+ 1 (exp (- t)))) c_p) (pow (/ 1 (+ 1 (exp (- t)))) c_p)) (pow (/ 1 (+ 1 (exp (- t)))) c_p)) (* (* (pow (- 1 (/ 1 (+ 1 (exp (- t))))) c_n) (pow (- 1 (/ 1 (+ 1 (exp (- t))))) c_n)) (pow (- 1 (/ 1 (+ 1 (exp (- t))))) c_n)))) |
| 2.3s | (/ (* (* (* (pow (/ 1 (+ 1 (exp (- s)))) c_p) (pow (- 1 (/ 1 (+ 1 (exp (- s))))) c_n)) (* (pow (/ 1 (+ 1 (exp (- s)))) c_p) (pow (- 1 (/ 1 (+ 1 (exp (- s))))) c_n))) (* (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 (exp (- t)))) c_p)) (pow (/ 1 (+ 1 (exp (- t)))) c_p)) (* (* (pow (- 1 (/ 1 (+ 1 (exp (- t))))) c_n) (pow (- 1 (/ 1 (+ 1 (exp (- t))))) c_n)) (pow (- 1 (/ 1 (+ 1 (exp (- t))))) c_n)))) |
| 850.0ms | (/ (pow (- 1 (/ 1 (+ 1 (exp (- s))))) c_n) (pow (- 1 (/ 1 (+ 1 (exp (- t))))) c_n)) |
3 alts after pruning (3 fresh and 0 done)
Merged error: 0.3b
Found 4 expressions with local error:
| 46.6b | (fma (log1p (/ -1 (+ 1 (exp (- s))))) c_n (- (* (+ (- (log1p (exp (- s)))) (log1p (/ 1 (exp t)))) c_p) (* (log1p (/ -1 (+ 1 (/ 1 (exp t))))) c_n))) |
| 10.2b | (+ (- (log1p (exp (- s)))) (log1p (/ 1 (exp t)))) |
| 1.0b | (log1p (/ 1 (exp t))) |
| 0.5b | (log1p (exp (- s))) |
| 11× | *-un-lft-identity add-log-exp |
| 10× | fma-def |
| 7× | add-sqr-sqrt log1p-udef add-cube-cbrt |
| 6× | expm1-log1p-u sum-log |
| 4× | pow1 distribute-rgt-neg-in add-cbrt-cube neg-log add-exp-log insert-posit16 log1p-expm1-u |
| 3× | distribute-lft-neg-in |
| 2× | log1p-expm1 distribute-lft-out |
| 1× | neg-sub0 +-commutative neg-mul-1 flip3-+ associate-+l- flip-+ fma-udef |
| 15.0ms | (+ (- (log1p (exp (- s)))) (log1p (/ 1 (exp t)))) |
| 0.0ms | (log1p (/ 1 (exp t))) |
| 0.0ms | (log1p (exp (- s))) |
| 0.0ms | (fma (log1p (/ -1 (+ 1 (exp (- s))))) c_n (- (* (+ (- (log1p (exp (- s)))) (log1p (/ 1 (exp t)))) c_p) (* (log1p (/ -1 (+ 1 (/ 1 (exp t))))) c_n))) |
| 348.0ms | (fma (log1p (/ -1 (+ 1 (exp (- s))))) c_n (- (* (+ (- (log1p (exp (- s)))) (log1p (/ 1 (exp t)))) c_p) (* (log1p (/ -1 (+ 1 (/ 1 (exp t))))) c_n))) |
| 76.0ms | (+ (- (log1p (exp (- s)))) (log1p (/ 1 (exp t)))) |
| 56.0ms | (log1p (/ 1 (exp t))) |
| 54.0ms | (log1p (exp (- s))) |
| 303.0ms | (- (+ (* c_p (log (+ (/ 1 (exp t)) 1))) (* c_n (log (- 1 (/ 1 (+ (exp (* -1 s)) 1)))))) (+ (* c_p (log (+ (exp (* -1 s)) 1))) (* c_n (log (- 1 (/ 1 (+ (/ 1 (exp t)) 1))))))) |
| 261.0ms | (- (+ (* c_n (log (- 1 (/ 1 (+ (exp (- s)) 1))))) (* c_p (log (+ (/ 1 (exp t)) 1)))) (+ (* c_p (log (+ (exp (- s)) 1))) (* c_n (log (- 1 (/ 1 (+ (/ 1 (exp t)) 1))))))) |
| 176.0ms | (- (* 1/2 s) (+ (* 1/2 t) (* 1/8 (pow s 2)))) |
| 114.0ms | (- (log (+ (/ 1 (exp t)) 1)) (log (+ (exp (* -1 s)) 1))) |
| 100.0ms | (- (+ (log 2) (* 1/8 (pow t 2))) (* 1/2 t)) |
3 alts after pruning (2 fresh and 1 done)
Merged error: 0.3b
Found 4 expressions with local error:
| 41.0b | (fma (log1p (/ -1 (+ 1 (exp (- s))))) c_n (- (* (fma t -1/2 (* s (fma s -1/8 1/2))) c_p) (* (log1p (/ -1 (+ 1 (/ 1 (exp t))))) c_n))) |
| 0.2b | (log1p (/ -1 (+ 1 (exp (- s))))) |
| 0.2b | (* (log1p (/ -1 (+ 1 (/ 1 (exp t))))) c_n) |
| 0.1b | (log1p (/ -1 (+ 1 (/ 1 (exp t))))) |
| 8× | add-sqr-sqrt |
| 6× | expm1-log1p-u pow1 *-un-lft-identity add-cbrt-cube add-exp-log add-cube-cbrt |
| 4× | insert-posit16 log1p-expm1-u add-log-exp |
| 3× | associate-*r* associate-*l* |
| 2× | log1p-udef log1p-expm1 |
| 1× | pow-prod-down prod-exp *-commutative cbrt-unprod fma-udef unswap-sqr |
| 7.0ms | (* (log1p (/ -1 (+ 1 (/ 1 (exp t))))) c_n) |
| 0.0ms | (log1p (/ -1 (+ 1 (exp (- s))))) |
| 0.0ms | (log1p (/ -1 (+ 1 (/ 1 (exp t))))) |
| 0.0ms | (fma (log1p (/ -1 (+ 1 (exp (- s))))) c_n (- (* (fma t -1/2 (* s (fma s -1/8 1/2))) c_p) (* (log1p (/ -1 (+ 1 (/ 1 (exp t))))) c_n))) |
| 168.0ms | (fma (log1p (/ -1 (+ 1 (exp (- s))))) c_n (- (* (fma t -1/2 (* s (fma s -1/8 1/2))) c_p) (* (log1p (/ -1 (+ 1 (/ 1 (exp t))))) c_n))) |
| 86.0ms | (* (log1p (/ -1 (+ 1 (/ 1 (exp t))))) c_n) |
| 71.0ms | (log1p (/ -1 (+ 1 (/ 1 (exp t))))) |
| 70.0ms | (log1p (/ -1 (+ 1 (exp (- s))))) |
| 299.0ms | (* (* (* (log1p (/ -1 (+ 1 (/ 1 (exp t))))) (log1p (/ -1 (+ 1 (/ 1 (exp t)))))) (log1p (/ -1 (+ 1 (/ 1 (exp t)))))) (* (* c_n c_n) c_n)) |
| 183.0ms | (- (log 1/2) (+ (* 1/2 t) (* 1/8 (pow t 2)))) |
| 166.0ms | (- (log 1/2) (+ (* 1/8 (pow s 2)) (* 1/2 s))) |
| 142.0ms | (- (* 1/2 (* c_p s)) (+ (* 1/2 (* t c_p)) (* 1/8 (* c_p (pow s 2))))) |
| 139.0ms | (- (* 1/2 (* c_p s)) (+ (* 1/2 (* t c_p)) (* 1/8 (* c_p (pow s 2))))) |
3 alts after pruning (2 fresh and 1 done)
Merged error: 0.0b
Found 2 expressions with local error:
| 0.0b | (* c_p (- (* 1/2 (- s t)) (* 1/8 (* s s)))) |
| 0.0b | (- (* 1/2 (- s t)) (* 1/8 (* s s))) |
| 66× | associate--l+ |
| 58× | distribute-rgt-in distribute-lft-in |
| 57× | prod-diff |
| 42× | add-sqr-sqrt |
| 40× | *-un-lft-identity add-cube-cbrt |
| 9× | sub-neg |
| 4× | pow1 add-cbrt-cube add-exp-log add-log-exp |
| 3× | associate-*r* associate-*l* |
| 2× | expm1-log1p-u flip3-- associate-*r/ insert-posit16 log1p-expm1-u flip-- |
| 1× | fma-neg diff-log pow-prod-down prod-exp *-commutative cbrt-unprod unswap-sqr |
| 69.0ms | (* c_p (- (* 1/2 (- s t)) (* 1/8 (* s s)))) |
| 23.0ms | (- (* 1/2 (- s t)) (* 1/8 (* s s))) |
| 73.0ms | (* c_p (- (* 1/2 (- s t)) (* 1/8 (* s s)))) |
| 34.0ms | (- (* 1/2 (- s t)) (* 1/8 (* s s))) |
| 409.0ms | (- (* 1/2 (* c_p s)) (+ (* 1/2 (* t c_p)) (* 1/8 (* c_p (pow s 2))))) |
| 249.0ms | (/ (exp (* 1/2 (- s t))) (exp (* 1/8 (* s s)))) |
| 246.0ms | (* c_p (- (* (fma (- (sqrt t)) (sqrt t) (* (sqrt t) (sqrt t))) 1/2) (* 1/8 (* s s)))) |
| 245.0ms | (* c_p (- (* (fma (- (sqrt t)) (sqrt t) (* (sqrt t) (sqrt t))) 1/2) (* 1/8 (* s s)))) |
| 244.0ms | (* c_p (- (* (fma (- (sqrt t)) (sqrt t) (* (sqrt t) (sqrt t))) 1/2) (* 1/8 (* s s)))) |
3 alts after pruning (1 fresh and 2 done)
Merged error: 0.0b