Time bar (total: 39.3s)
| 412.0ms | 48× | body | 1280 | valid |
| 155.0ms | 19× | body | 2560 | valid |
| 58.0ms | 130× | body | 80 | valid |
| 45.0ms | 42× | body | 640 | valid |
| 11.0ms | 15× | body | 320 | valid |
| 4.0ms | 11× | body | 160 | valid |
| Iter | Nodes |
|---|---|
| done | 142 |
| 7 | 142 |
| 6 | 139 |
| 5 | 125 |
| 4 | 109 |
| 3 | 70 |
| 2 | 41 |
| 1 | 19 |
| 0 | 10 |
1 alts after pruning (1 fresh and 0 done)
Merged error: 15.5b
Found 4 expressions with local error:
| 0.3b | (* PI l) |
| 0.7b | (/ 1.0 (* F F)) |
| 4.1b | (* (/ 1.0 (* F F)) (tan (* PI l))) |
| 32.0b | (tan (* PI l)) |
| 20× | add-exp-log add-cbrt-cube |
| 17× | add-sqr-sqrt |
| 11× | add-cube-cbrt *-un-lft-identity |
| 10× | associate-*l* |
| 8× | pow1 |
| 7× | times-frac |
| 6× | associate-*r* prod-exp cbrt-unprod |
| 4× | cbrt-undiv expm1-log1p-u div-exp log1p-expm1-u add-log-exp |
| 3× | tan-quot associate-/l* unswap-sqr |
| 2× | pow-prod-down *-commutative div-inv |
| 1× | frac-times frac-2neg associate-*r/ associate-*l/ clear-num associate-/r* |
| 11.0ms | (* PI l) |
| 21.0ms | (/ 1.0 (* F F)) |
| 173.0ms | (* (/ 1.0 (* F F)) (tan (* PI l))) |
| 40.0ms | (tan (* PI l)) |
| 38.0ms | (* PI l) |
| 49.0ms | (/ 1.0 (* F F)) |
| 391.0ms | (* (/ 1.0 (* F F)) (tan (* PI l))) |
| 247.0ms | (tan (* PI l)) |
| Iter | Nodes |
|---|---|
| done | 5004 |
| 2 | 1205 |
| 1 | 341 |
| 0 | 143 |
13 alts after pruning (13 fresh and 0 done)
Merged error: 11.1b
Found 4 expressions with local error:
| 0.3b | (* l PI) |
| 0.3b | (* PI l) |
| 0.3b | (/ (tan (* l PI)) F) |
| 32.0b | (tan (* l PI)) |
| 20× | add-sqr-sqrt |
| 16× | add-cube-cbrt *-un-lft-identity |
| 10× | add-exp-log add-cbrt-cube |
| 9× | times-frac |
| 8× | pow1 |
| 6× | associate-*r* associate-*l* |
| 4× | expm1-log1p-u log1p-expm1-u add-log-exp |
| 3× | associate-/r* associate-/l* |
| 2× | tan-quot pow-prod-down prod-exp *-commutative cbrt-unprod unswap-sqr |
| 1× | cbrt-undiv frac-2neg div-exp clear-num div-inv associate-/l/ |
| 16.0ms | (* l PI) |
| 127.0ms | (* PI l) |
| 23.0ms | (/ (tan (* l PI)) F) |
| 14.0ms | (tan (* l PI)) |
| 42.0ms | (* l PI) |
| 57.0ms | (* PI l) |
| 209.0ms | (/ (tan (* l PI)) F) |
| 176.0ms | (tan (* l PI)) |
| Iter | Nodes |
|---|---|
| done | 5011 |
| 3 | 2204 |
| 2 | 718 |
| 1 | 272 |
| 0 | 133 |
22 alts after pruning (22 fresh and 0 done)
Merged error: 11.0b
Found 4 expressions with local error:
| 0.3b | (* l PI) |
| 0.3b | (* PI l) |
| 0.3b | (* (tan (* l PI)) (/ 1 F)) |
| 32.0b | (tan (* l PI)) |
| 27× | add-sqr-sqrt |
| 19× | associate-*r* |
| 17× | add-exp-log *-un-lft-identity |
| 16× | add-cube-cbrt |
| 13× | add-cbrt-cube |
| 11× | times-frac |
| 10× | pow1 |
| 9× | associate-*l* |
| 6× | prod-exp |
| 5× | unswap-sqr |
| 4× | expm1-log1p-u cbrt-unprod log1p-expm1-u add-log-exp |
| 3× | tan-quot pow-prod-down *-commutative |
| 2× | div-exp |
| 1× | cbrt-undiv frac-times rec-exp 1-exp associate-*r/ associate-*l/ un-div-inv div-inv |
| 14.0ms | (* l PI) |
| 15.0ms | (* PI l) |
| 70.0ms | (* (tan (* l PI)) (/ 1 F)) |
| 17.0ms | (tan (* l PI)) |
| 49.0ms | (* l PI) |
| 43.0ms | (* PI l) |
| 209.0ms | (* (tan (* l PI)) (/ 1 F)) |
| 131.0ms | (tan (* l PI)) |
| Iter | Nodes |
|---|---|
| done | 5083 |
| 3 | 2764 |
| 2 | 965 |
| 1 | 378 |
| 0 | 159 |
22 alts after pruning (21 fresh and 1 done)
Merged error: 11.0b
Found 4 expressions with local error:
| 1.0b | (cbrt PI) |
| 1.0b | (cbrt PI) |
| 1.0b | (* (cbrt PI) (cbrt PI)) |
| 32.7b | (tan (* (* l (* (cbrt PI) (cbrt PI))) (cbrt PI))) |
| 22× | cbrt-prod add-sqr-sqrt |
| 14× | add-cube-cbrt *-un-lft-identity |
| 11× | pow1 |
| 8× | pow1/3 |
| 6× | add-exp-log swap-sqr associate-*r* associate-*l* |
| 4× | expm1-log1p-u add-cbrt-cube log1p-expm1-u add-log-exp unswap-sqr |
| 2× | pow-prod-down pow-sqr pow-prod-up |
| 1× | tan-quot pow2 pow-plus prod-exp *-commutative cbrt-unprod |
| 1.0ms | (cbrt PI) |
| 1.0ms | (cbrt PI) |
| 22.0ms | (* (cbrt PI) (cbrt PI)) |
| 115.0ms | (tan (* (* l (* (cbrt PI) (cbrt PI))) (cbrt PI))) |
| 0.0ms | (cbrt PI) |
| 0.0ms | (cbrt PI) |
| 0.0ms | (* (cbrt PI) (cbrt PI)) |
| 142.0ms | (tan (* (* l (* (cbrt PI) (cbrt PI))) (cbrt PI))) |
| Iter | Nodes |
|---|---|
| done | 5003 |
| 4 | 3559 |
| 3 | 988 |
| 2 | 387 |
| 1 | 160 |
| 0 | 80 |
22 alts after pruning (22 fresh and 0 done)
Merged error: 11.0b
0% (0.3b remaining)
Error of 12.3b against oracle of 12.0b and baseline of 12.3b
| Iter | Nodes |
|---|---|
| done | 25 |
| 1 | 25 |
| 0 | 18 |
| 5.4s | 789× | body | 2560 | valid |
| 3.6s | 1613× | body | 1280 | valid |
| 1.1s | 1017× | body | 640 | valid |
| 952.0ms | 4623× | body | 80 | valid |
| 231.0ms | 394× | body | 320 | valid |
| 118.0ms | 3× | body | 10240 | exit |
| 70.0ms | 190× | body | 160 | valid |