Time bar (total: 2.9m)
| 24.0ms | 298× | body | 80 | valid |
| 1.0ms | 5× | body | 320 | valid |
| 1.0ms | 4× | body | 640 | valid |
| 1.0ms | 2× | body | 1280 | valid |
| 1.0ms | 5× | body | 160 | valid |
| 103.0ms | (+ (+ (* d1 3) (* d1 d2)) (* d1 d3)) |
2 alts after pruning (2 fresh and 0 done)
Merged error: 0.0b
Found 1 expressions with local error:
| 0.0b | (* (+ (+ 3 d3) d2) d1) |
| 8× | *-un-lft-identity |
| 5× | add-sqr-sqrt associate-*l* |
| 3× | pow1 add-cbrt-cube associate-*r* add-exp-log add-cube-cbrt distribute-lft-out |
| 2× | associate-*l/ |
| 1× | expm1-log1p-u flip3-+ pow-prod-down prod-exp *-commutative cbrt-unprod flip-+ insert-posit16 log1p-expm1-u add-log-exp unswap-sqr |
| 70.0ms | (* (+ (+ 3 d3) d2) d1) |
| 32.0ms | (* (+ (+ 3 d3) d2) d1) |
| 286.0ms | (* (* (* (+ (+ 3 d3) d2) (+ (+ 3 d3) d2)) (+ (+ 3 d3) d2)) (* (* d1 d1) d1)) |
| 283.0ms | (* (- (* (+ 3 d3) (+ 3 d3)) (* d2 d2)) d1) |
| 252.0ms | (* (+ (pow (+ 3 d3) 3) (pow d2 3)) d1) |
| 130.0ms | (+ (* d3 d1) (+ (* d2 d1) (* 3 d1))) |
| 100.0ms | (+ (* d3 d1) (+ (* d2 d1) (* 3 d1))) |
3 alts after pruning (2 fresh and 1 done)
Merged error: 0.0b
Found 4 expressions with local error:
| 17.4b | (/ (* (- (* (+ 3 d3) (+ 3 d3)) (* d2 d2)) d1) (- (+ 3 d3) d2)) |
| 8.5b | (* (- (* (+ 3 d3) (+ 3 d3)) (* d2 d2)) d1) |
| 3.3b | (- (* (+ 3 d3) (+ 3 d3)) (* d2 d2)) |
| 0.0b | (* (+ 3 d3) (+ 3 d3)) |
| 36× | *-un-lft-identity |
| 20× | add-sqr-sqrt |
| 13× | pow1 add-cbrt-cube add-exp-log |
| 12× | add-cube-cbrt |
| 8× | associate-*l* distribute-lft-out |
| 7× | associate-*r* |
| 6× | associate-/r* flip3-+ times-frac swap-sqr associate-*l/ flip-+ add-log-exp |
| 4× | expm1-log1p-u frac-times flip3-- insert-posit16 log1p-expm1-u flip-- distribute-lft-out-- difference-of-squares |
| 3× | prod-exp cbrt-unprod |
| 2× | distribute-rgt-in cbrt-undiv distribute-lft-in div-exp pow-prod-down associate--l+ associate-*r/ associate-/r/ *-commutative unswap-sqr associate-/l/ |
| 1× | pow2 clear-num sub-neg frac-2neg pow-plus fma-neg diff-log prod-diff pow-sqr pow-prod-up div-inv associate-/l* |
| 95.0ms | (* (- (* (+ 3 d3) (+ 3 d3)) (* d2 d2)) d1) |
| 68.0ms | (/ (* (- (* (+ 3 d3) (+ 3 d3)) (* d2 d2)) d1) (- (+ 3 d3) d2)) |
| 41.0ms | (* (+ 3 d3) (+ 3 d3)) |
| 31.0ms | (- (* (+ 3 d3) (+ 3 d3)) (* d2 d2)) |
| 94.0ms | (/ (* (- (* (+ 3 d3) (+ 3 d3)) (* d2 d2)) d1) (- (+ 3 d3) d2)) |
| 71.0ms | (* (- (* (+ 3 d3) (+ 3 d3)) (* d2 d2)) d1) |
| 40.0ms | (- (* (+ 3 d3) (+ 3 d3)) (* d2 d2)) |
| 12.0ms | (* (+ 3 d3) (+ 3 d3)) |
| 841.0ms | (/ (* (* (* (- (* (+ 3 d3) (+ 3 d3)) (* d2 d2)) d1) (* (- (* (+ 3 d3) (+ 3 d3)) (* d2 d2)) d1)) (* (- (* (+ 3 d3) (+ 3 d3)) (* d2 d2)) d1)) (* (* (- (+ 3 d3) d2) (- (+ 3 d3) d2)) (- (+ 3 d3) d2))) |
| 575.0ms | (/ (* (* (* (- (* (+ 3 d3) (+ 3 d3)) (* d2 d2)) (- (* (+ 3 d3) (+ 3 d3)) (* d2 d2))) (- (* (+ 3 d3) (+ 3 d3)) (* d2 d2))) (* (* d1 d1) d1)) (* (* (- (+ 3 d3) d2) (- (+ 3 d3) d2)) (- (+ 3 d3) d2))) |
| 482.0ms | (* (- (* 3 3) (* d3 d3)) (+ (pow 3 3) (pow d3 3))) |
| 474.0ms | (* (- (* 3 3) (* d3 d3)) (+ 3 d3)) |
| 422.0ms | (/ (- (* (+ 3 d3) (+ 3 d3)) (* d2 d2)) (* (cbrt (- (+ 3 d3) d2)) (cbrt (- (+ 3 d3) d2)))) |
3 alts after pruning (1 fresh and 2 done)
Merged error: 0b
Found 4 expressions with local error:
| 39.7b | (/ (* d1 (- (* (* (+ d3 3) (+ d3 3)) (* (* (+ d3 3) (+ d3 3)) (* (+ d3 3) (+ d3 3)))) (* (* (* d2 d2) (* d2 d2)) (* d2 d2)))) (* (- (+ 3 d3) d2) (+ (* (* (+ 3 d3) (+ 3 d3)) (* (+ 3 d3) (+ 3 d3))) (+ (* (* d2 d2) (* d2 d2)) (* (* (+ 3 d3) (+ 3 d3)) (* d2 d2)))))) |
| 9.2b | (- (* (* (+ d3 3) (+ d3 3)) (* (* (+ d3 3) (+ d3 3)) (* (+ d3 3) (+ d3 3)))) (* (* (* d2 d2) (* d2 d2)) (* d2 d2))) |
| 6.8b | (* (* (+ 3 d3) (+ 3 d3)) (* d2 d2)) |
| 2.4b | (* d1 (- (* (* (+ d3 3) (+ d3 3)) (* (* (+ d3 3) (+ d3 3)) (* (+ d3 3) (+ d3 3)))) (* (* (* d2 d2) (* d2 d2)) (* d2 d2)))) |
| 1144× | frac-times |
| 897× | flip3-+ flip-+ |
| 488× | associate-/r/ |
| 480× | frac-add |
| 432× | associate-*r/ |
| 276× | associate-*l/ |
| 166× | flip3-- flip-- |
| 47× | distribute-rgt-in distribute-lft-in |
| 34× | pow1 |
| 30× | add-cbrt-cube add-exp-log |
| 24× | associate--l+ |
| 15× | pow-prod-down |
| 13× | prod-exp cbrt-unprod |
| 8× | add-sqr-sqrt |
| 6× | *-un-lft-identity add-cube-cbrt add-log-exp |
| 5× | associate-*r* |
| 4× | expm1-log1p-u cbrt-undiv pow-plus div-exp associate-*l* pow-prod-up insert-posit16 log1p-expm1-u |
| 3× | sub-neg prod-diff |
| 2× | pow2 difference-cubes cube-unmult pow3 pow-sqr *-commutative unswap-sqr associate-/l/ |
| 1× | clear-num associate-/r* frac-2neg times-frac fma-neg diff-log div-inv associate-/l* |
| 2.0s | (* d1 (- (* (* (+ d3 3) (+ d3 3)) (* (* (+ d3 3) (+ d3 3)) (* (+ d3 3) (+ d3 3)))) (* (* (* d2 d2) (* d2 d2)) (* d2 d2)))) |
| 877.0ms | (/ (* d1 (- (* (* (+ d3 3) (+ d3 3)) (* (* (+ d3 3) (+ d3 3)) (* (+ d3 3) (+ d3 3)))) (* (* (* d2 d2) (* d2 d2)) (* d2 d2)))) (* (- (+ 3 d3) d2) (+ (* (* (+ 3 d3) (+ 3 d3)) (* (+ 3 d3) (+ 3 d3))) (+ (* (* d2 d2) (* d2 d2)) (* (* (+ 3 d3) (+ 3 d3)) (* d2 d2)))))) |
| 414.0ms | (- (* (* (+ d3 3) (+ d3 3)) (* (* (+ d3 3) (+ d3 3)) (* (+ d3 3) (+ d3 3)))) (* (* (* d2 d2) (* d2 d2)) (* d2 d2))) |
| 70.0ms | (* (* (+ 3 d3) (+ 3 d3)) (* d2 d2)) |
| 833.0ms | (* d1 (- (* (* (+ d3 3) (+ d3 3)) (* (* (+ d3 3) (+ d3 3)) (* (+ d3 3) (+ d3 3)))) (* (* (* d2 d2) (* d2 d2)) (* d2 d2)))) |
| 715.0ms | (/ (* d1 (- (* (* (+ d3 3) (+ d3 3)) (* (* (+ d3 3) (+ d3 3)) (* (+ d3 3) (+ d3 3)))) (* (* (* d2 d2) (* d2 d2)) (* d2 d2)))) (* (- (+ 3 d3) d2) (+ (* (* (+ 3 d3) (+ 3 d3)) (* (+ 3 d3) (+ 3 d3))) (+ (* (* d2 d2) (* d2 d2)) (* (* (+ 3 d3) (+ 3 d3)) (* d2 d2)))))) |
| 272.0ms | (- (* (* (+ d3 3) (+ d3 3)) (* (* (+ d3 3) (+ d3 3)) (* (+ d3 3) (+ d3 3)))) (* (* (* d2 d2) (* d2 d2)) (* d2 d2))) |
| 47.0ms | (* (* (+ 3 d3) (+ 3 d3)) (* d2 d2)) |
| 1.3s | (* (+ (* (+ 3 d3) (+ 3 d3)) (+ (* d2 d2) (* (+ 3 d3) d2))) (* (* (* (- 3 d3) (+ (* 3 3) (- (* d3 d3) (* 3 d3)))) (* (- 3 d3) (+ (* 3 3) (- (* d3 d3) (* 3 d3))))) (- (* (* d2 d2) (* d2 d2)) (* (* (+ 3 d3) (+ 3 d3)) (* d2 d2))))) |
| 1.1s | (* (+ (* (+ 3 d3) (+ 3 d3)) (+ (* d2 d2) (* (+ 3 d3) d2))) (* (* (* (- 3 d3) (+ (* 3 3) (- (* d3 d3) (* 3 d3)))) (* (+ (* 3 3) (- (* d3 d3) (* 3 d3))) (+ (* 3 3) (- (* d3 d3) (* 3 d3))))) (- (* (* d2 d2) (* d2 d2)) (* (* (+ 3 d3) (+ 3 d3)) (* d2 d2))))) |
| 872.0ms | (* (+ (* (+ 3 d3) (+ 3 d3)) (+ (* d2 d2) (* (+ 3 d3) d2))) (* (* (* (- 3 d3) (+ (* 3 3) (- (* d3 d3) (* 3 d3)))) (* (+ (* 3 3) (- (* d3 d3) (* 3 d3))) (- 3 d3))) (- (* (* d2 d2) (* d2 d2)) (* (* (+ 3 d3) (+ 3 d3)) (* d2 d2))))) |
| 869.0ms | (* (* (* (- 3 d3) (- 3 d3)) (- 3 d3)) (+ (* (* (* d2 d2) (* d2 d2)) (* (* d2 d2) (* d2 d2))) (- (* (* (* (+ 3 d3) (+ 3 d3)) (* d2 d2)) (* (* (+ 3 d3) (+ 3 d3)) (* d2 d2))) (* (* (* d2 d2) (* d2 d2)) (* (* (+ 3 d3) (+ 3 d3)) (* d2 d2)))))) |
| 863.0ms | (* (+ (* (+ 3 d3) (+ 3 d3)) (+ (* d2 d2) (* (+ 3 d3) d2))) (* (* (* (+ (* 3 3) (- (* d3 d3) (* 3 d3))) (+ (* 3 3) (- (* d3 d3) (* 3 d3)))) (+ (* 3 3) (- (* d3 d3) (* 3 d3)))) (- (* (* d2 d2) (* d2 d2)) (* (* (+ 3 d3) (+ 3 d3)) (* d2 d2))))) |
3 alts after pruning (0 fresh and 3 done)
Merged error: 0b
0% (0.0b remaining)
Error of 0.1b against oracle of 0.0b and baseline of 0.1b
| 653.0ms | 9610× | body | 80 | valid |
| 45.0ms | 213× | body | 640 | valid |
| 39.0ms | 82× | body | 1280 | valid |
| 24.0ms | 148× | body | 320 | valid |
| 10.0ms | 90× | body | 160 | valid |