Time bar (total: 37.5s)
| 184.0ms | 100× | body | 1280 | valid |
| 173.0ms | 88× | body | 2560 | valid |
| 111.0ms | 55× | body | 10240 | exit |
| 29.0ms | 34× | body | 640 | valid |
| 15.0ms | 312× | pre | 80 | true |
| 9.0ms | 15× | body | 320 | valid |
| 2.0ms | 14× | body | 80 | valid |
| 2.0ms | 6× | body | 160 | valid |
1 alts after pruning (1 fresh and 0 done)
Merged error: 25.9b
Found 4 expressions with local error:
| 16.4b | (/ (* (expm1 (* (+ a b) eps)) (/ eps (expm1 (* eps b)))) (expm1 (* eps a))) |
| 15.8b | (/ eps (expm1 (* eps b))) |
| 7.0b | (* (expm1 (* (+ a b) eps)) (/ eps (expm1 (* eps b)))) |
| 0.1b | (expm1 (* (+ a b) eps)) |
| 27× | add-sqr-sqrt |
| 22× | *-un-lft-identity times-frac add-cube-cbrt |
| 20× | add-cbrt-cube add-exp-log |
| 13× | associate-*r* |
| 6× | pow1 cbrt-undiv associate-/r* div-exp |
| 5× | log1p-expm1-u |
| 4× | expm1-log1p-u prod-exp cbrt-unprod insert-posit16 associate-/l* add-log-exp |
| 3× | associate-*l* div-inv |
| 2× | clear-num frac-2neg associate-*r/ unswap-sqr |
| 1× | expm1-log1p pow-prod-down *-commutative expm1-udef associate-/l/ |
| 12.0ms | (/ (* (expm1 (* (+ a b) eps)) (/ eps (expm1 (* eps b)))) (expm1 (* eps a))) |
| 9.0ms | (* (expm1 (* (+ a b) eps)) (/ eps (expm1 (* eps b)))) |
| 8.0ms | (/ eps (expm1 (* eps b))) |
| 0.0ms | (expm1 (* (+ a b) eps)) |
| 596.0ms | (/ (* (expm1 (* (+ a b) eps)) (/ eps (expm1 (* eps b)))) (expm1 (* eps a))) |
| 179.0ms | (* (expm1 (* (+ a b) eps)) (/ eps (expm1 (* eps b)))) |
| 75.0ms | (expm1 (* (+ a b) eps)) |
| 45.0ms | (/ eps (expm1 (* eps b))) |
3 alts after pruning (3 fresh and 0 done)
Merged error: 0.0b
Found 1 expressions with local error:
| 0.0b | (+ (/ 1 a) (/ 1 b)) |
| 20× | *-un-lft-identity |
| 15× | times-frac |
| 13× | fma-def |
| 10× | add-sqr-sqrt add-cube-cbrt |
| 7× | distribute-lft-out |
| 5× | div-inv |
| 3× | add-log-exp |
| 1× | expm1-log1p-u pow1 +-commutative sum-log flip3-+ add-cbrt-cube frac-add add-exp-log flip-+ insert-posit16 log1p-expm1-u |
| 22.0ms | (+ (/ 1 a) (/ 1 b)) |
| 16.0ms | (+ (/ 1 a) (/ 1 b)) |
5 alts after pruning (4 fresh and 1 done)
Merged error: 0b
Found 4 expressions with local error:
| 0.6b | (cbrt (/ 1 a)) |
| 0.6b | (cbrt (/ 1 a)) |
| 0.6b | (cbrt (/ 1 a)) |
| 0.5b | (* (cbrt (/ 1 a)) (cbrt (/ 1 a))) |
| 119× | cbrt-prod |
| 97× | add-sqr-sqrt |
| 79× | times-frac |
| 67× | *-un-lft-identity |
| 57× | add-cube-cbrt |
| 18× | swap-sqr |
| 16× | associate-*r* associate-*l* unswap-sqr |
| 11× | pow1 |
| 9× | pow1/3 div-inv |
| 7× | cbrt-div |
| 6× | add-exp-log |
| 4× | expm1-log1p-u add-cbrt-cube insert-posit16 log1p-expm1-u add-log-exp |
| 2× | pow-prod-down pow-sqr pow-prod-up |
| 1× | pow2 frac-times pow-plus associate-*l/ prod-exp associate-*r/ *-commutative cbrt-unprod |
| 14.0ms | (* (cbrt (/ 1 a)) (cbrt (/ 1 a))) |
| 2.0ms | (cbrt (/ 1 a)) |
| 2.0ms | (cbrt (/ 1 a)) |
| 1.0ms | (cbrt (/ 1 a)) |
| 298.0ms | (cbrt (/ 1 a)) |
| 273.0ms | (cbrt (/ 1 a)) |
| 269.0ms | (* (cbrt (/ 1 a)) (cbrt (/ 1 a))) |
| 253.0ms | (cbrt (/ 1 a)) |
4 alts after pruning (3 fresh and 1 done)
Merged error: 0b
Found 4 expressions with local error:
| 0.6b | (cbrt (/ 1 a)) |
| 0.6b | (cbrt (/ 1 a)) |
| 0.6b | (cbrt a) |
| 0.5b | (* (/ 1 (cbrt a)) (cbrt (/ 1 a))) |
| 93× | add-sqr-sqrt |
| 74× | cbrt-prod |
| 71× | times-frac |
| 53× | *-un-lft-identity |
| 40× | add-cube-cbrt |
| 22× | associate-*l* |
| 20× | unswap-sqr |
| 16× | associate-*r* |
| 13× | add-exp-log |
| 6× | pow1 add-cbrt-cube |
| 4× | expm1-log1p-u cbrt-div prod-exp insert-posit16 log1p-expm1-u div-inv add-log-exp |
| 3× | pow1/3 |
| 2× | div-exp cbrt-unprod |
| 1× | frac-times cbrt-undiv rec-exp 1-exp pow-prod-down associate-*l/ associate-*r/ *-commutative |
| 29.0ms | (* (/ 1 (cbrt a)) (cbrt (/ 1 a))) |
| 3.0ms | (cbrt (/ 1 a)) |
| 3.0ms | (cbrt (/ 1 a)) |
| 1.0ms | (cbrt a) |
| 335.0ms | (cbrt (/ 1 a)) |
| 285.0ms | (cbrt (/ 1 a)) |
| 254.0ms | (cbrt a) |
| 244.0ms | (* (/ 1 (cbrt a)) (cbrt (/ 1 a))) |
4 alts after pruning (2 fresh and 2 done)
Merged error: 0b
0% (3.1b remaining)
Error of 3.1b against oracle of 0.0b and baseline of 3.1b
| 6.1s | 2633× | body | 2560 | valid |
| 5.2s | 3412× | body | 1280 | valid |
| 4.9s | 2023× | body | 10240 | exit |
| 998.0ms | 1084× | body | 640 | valid |
| 628.0ms | 323× | body | 320 | valid |
| 543.0ms | 10027× | pre | 80 | true |
| 421.0ms | 136× | body | 160 | valid |
| 99.0ms | 416× | body | 80 | valid |