Time bar (total: 26.3s)
| 163.0ms | 83× | body | 1280 | valid |
| 59.0ms | 68× | body | 640 | valid |
| 15.0ms | 21× | body | 320 | valid |
| 14.0ms | 76× | body | 80 | valid |
| 3.0ms | 8× | body | 160 | valid |
| Iter | Nodes |
|---|---|
| done | 20 |
| 5 | 20 |
| 4 | 19 |
| 3 | 17 |
| 2 | 14 |
| 1 | 12 |
| 0 | 8 |
1 alts after pruning (1 fresh and 0 done)
Merged error: 12.7b
Found 3 expressions with local error:
| 0.1b | (* r (sin b)) |
| 0.2b | (/ (* r (sin b)) (cos (+ a b))) |
| 3.0b | (cos (+ a b)) |
| 40× | add-sqr-sqrt |
| 36× | times-frac |
| 30× | *-un-lft-identity add-cube-cbrt |
| 15× | associate-*r* associate-*l* |
| 12× | associate-/l* |
| 10× | add-cbrt-cube add-exp-log |
| 5× | pow1 *-commutative unswap-sqr |
| 3× | expm1-log1p-u associate-/r* insert-posit16 log1p-expm1-u add-log-exp |
| 2× | cbrt-undiv cos-sum div-exp prod-exp cbrt-unprod |
| 1× | +-commutative clear-num frac-2neg pow-prod-down div-inv |
| 10.0ms | (* r (sin b)) |
| 23.0ms | (/ (* r (sin b)) (cos (+ a b))) |
| 15.0ms | (cos (+ a b)) |
| 52.0ms | (* r (sin b)) |
| 112.0ms | (/ (* r (sin b)) (cos (+ a b))) |
| 32.0ms | (cos (+ a b)) |
| Iter | Nodes |
|---|---|
| done | 5001 |
| 3 | 4587 |
| 2 | 1154 |
| 1 | 367 |
| 0 | 163 |
9 alts after pruning (9 fresh and 0 done)
Merged error: 0.1b
Found 4 expressions with local error:
| 0.1b | (- (* (cos b) (cos a)) (* (sin b) (sin a))) |
| 0.1b | (* r (sin b)) |
| 0.2b | (* (sin b) (sin a)) |
| 0.2b | (/ (* r (sin b)) (- (* (cos b) (cos a)) (* (sin b) (sin a)))) |
| 378× | add-sqr-sqrt |
| 244× | *-un-lft-identity |
| 173× | associate-*l* |
| 144× | prod-diff |
| 132× | times-frac add-cube-cbrt |
| 117× | associate-*r* |
| 95× | unswap-sqr |
| 56× | distribute-lft-out-- difference-of-squares |
| 39× | *-commutative |
| 13× | add-cbrt-cube add-exp-log |
| 12× | fma-neg associate-/l* |
| 11× | associate-/r* |
| 8× | pow1 |
| 6× | add-log-exp |
| 5× | sin-mult |
| 4× | expm1-log1p-u associate-/r/ cos-mult insert-posit16 log1p-expm1-u |
| 3× | prod-exp cbrt-unprod |
| 2× | cbrt-undiv flip3-- div-exp pow-prod-down frac-sub flip-- sub-div |
| 1× | clear-num sub-neg frac-2neg diff-log div-inv |
| 157.0ms | (- (* (cos b) (cos a)) (* (sin b) (sin a))) |
| 11.0ms | (* r (sin b)) |
| 15.0ms | (* (sin b) (sin a)) |
| 144.0ms | (/ (* r (sin b)) (- (* (cos b) (cos a)) (* (sin b) (sin a)))) |
| 115.0ms | (- (* (cos b) (cos a)) (* (sin b) (sin a))) |
| 56.0ms | (* r (sin b)) |
| 64.0ms | (* (sin b) (sin a)) |
| 368.0ms | (/ (* r (sin b)) (- (* (cos b) (cos a)) (* (sin b) (sin a)))) |
| Iter | Nodes |
|---|---|
| done | 5003 |
| 2 | 2848 |
| 1 | 1103 |
| 0 | 486 |
15 alts after pruning (15 fresh and 0 done)
Merged error: 0.0b
Found 4 expressions with local error:
| 0.1b | (- (* (cos b) (cos a)) (log1p (expm1 (* (sin b) (sin a))))) |
| 0.1b | (* r (sin b)) |
| 0.2b | (* (sin b) (sin a)) |
| 0.2b | (/ (* r (sin b)) (- (* (cos b) (cos a)) (log1p (expm1 (* (sin b) (sin a)))))) |
| 167× | add-sqr-sqrt |
| 125× | *-un-lft-identity |
| 84× | times-frac |
| 69× | add-cube-cbrt |
| 56× | associate-*l* |
| 42× | associate-*r* |
| 36× | prod-diff |
| 28× | distribute-lft-out-- difference-of-squares unswap-sqr |
| 14× | *-commutative |
| 13× | add-cbrt-cube add-exp-log |
| 12× | fma-neg associate-/l* |
| 8× | pow1 |
| 7× | associate-/r* add-log-exp |
| 4× | expm1-log1p-u insert-posit16 log1p-expm1-u |
| 3× | prod-exp cbrt-unprod |
| 2× | cbrt-undiv flip3-- diff-log div-exp pow-prod-down associate-/r/ flip-- |
| 1× | log1p-udef clear-num sub-neg frac-2neg div-inv sin-mult |
| 55.0ms | (- (* (cos b) (cos a)) (log1p (expm1 (* (sin b) (sin a))))) |
| 12.0ms | (* r (sin b)) |
| 23.0ms | (* (sin b) (sin a)) |
| 114.0ms | (/ (* r (sin b)) (- (* (cos b) (cos a)) (log1p (expm1 (* (sin b) (sin a)))))) |
| 182.0ms | (- (* (cos b) (cos a)) (log1p (expm1 (* (sin b) (sin a))))) |
| 54.0ms | (* r (sin b)) |
| 69.0ms | (* (sin b) (sin a)) |
| 378.0ms | (/ (* r (sin b)) (- (* (cos b) (cos a)) (log1p (expm1 (* (sin b) (sin a)))))) |
| Iter | Nodes |
|---|---|
| done | 5137 |
| 2 | 2302 |
| 1 | 757 |
| 0 | 322 |
14 alts after pruning (14 fresh and 0 done)
Merged error: 0.0b
Found 4 expressions with local error:
| 0.2b | (/ (* r (sin b)) (+ (fma (cos a) (cos b) (- (* (log1p (expm1 (* (sin b) (sin a)))) 1))) (fma (- (log1p (expm1 (* (sin b) (sin a))))) 1 (* (log1p (expm1 (* (sin b) (sin a)))) 1)))) |
| 0.2b | (* (sin b) (sin a)) |
| 0.2b | (* (sin b) (sin a)) |
| 0.2b | (* (sin b) (sin a)) |
| 64× | *-un-lft-identity |
| 54× | add-sqr-sqrt |
| 48× | times-frac |
| 38× | add-cube-cbrt |
| 24× | associate-*r* associate-*l* |
| 15× | add-cbrt-cube add-exp-log |
| 13× | distribute-lft-out |
| 12× | associate-/l* |
| 10× | pow1 |
| 8× | *-commutative unswap-sqr |
| 4× | expm1-log1p-u associate-/r* prod-exp cbrt-unprod insert-posit16 log1p-expm1-u add-log-exp |
| 3× | pow-prod-down sin-mult |
| 2× | cbrt-undiv div-exp associate-/r/ |
| 1× | clear-num frac-2neg flip3-+ flip-+ div-inv |
| 53.0ms | (/ (* r (sin b)) (+ (fma (cos a) (cos b) (- (* (log1p (expm1 (* (sin b) (sin a)))) 1))) (fma (- (log1p (expm1 (* (sin b) (sin a))))) 1 (* (log1p (expm1 (* (sin b) (sin a)))) 1)))) |
| 22.0ms | (* (sin b) (sin a)) |
| 19.0ms | (* (sin b) (sin a)) |
| 14.0ms | (* (sin b) (sin a)) |
| 697.0ms | (/ (* r (sin b)) (+ (fma (cos a) (cos b) (- (* (log1p (expm1 (* (sin b) (sin a)))) 1))) (fma (- (log1p (expm1 (* (sin b) (sin a))))) 1 (* (log1p (expm1 (* (sin b) (sin a)))) 1)))) |
| 71.0ms | (* (sin b) (sin a)) |
| 72.0ms | (* (sin b) (sin a)) |
| 73.0ms | (* (sin b) (sin a)) |
| Iter | Nodes |
|---|---|
| done | 5002 |
| 2 | 1451 |
| 1 | 474 |
| 0 | 194 |
14 alts after pruning (13 fresh and 1 done)
Merged error: 0b
0% (0.3b remaining)
Error of 0.3b against oracle of 0.0b and baseline of 0.3b
| Iter | Nodes |
|---|---|
| done | 32 |
| 2 | 32 |
| 1 | 30 |
| 0 | 19 |
| 4.1s | 2839× | body | 1280 | valid |
| 2.1s | 1837× | body | 640 | valid |
| 411.0ms | 766× | body | 320 | valid |
| 360.0ms | 2216× | body | 80 | valid |
| 128.0ms | 344× | body | 160 | valid |