Time bar (total: 4.0m)
| 165.0ms | 72× | body | 1280 | valid |
| 149.0ms | 206× | body | 80 | valid |
| 93.0ms | 50× | body | 640 | valid |
| 30.0ms | 25× | body | 320 | valid |
| 11.0ms | 14× | body | 160 | valid |
2 alts after pruning (2 fresh and 0 done)
Merged error: 21.1b
Found 4 expressions with local error:
| 15.0b | (/ (/ 2 (+ (* (/ k t) (/ k t)) 2)) (/ (tan k) (/ (* (/ l t) (/ l t)) (* (sin k) t)))) |
| 3.2b | (/ (tan k) (/ (* (/ l t) (/ l t)) (* (sin k) t))) |
| 3.2b | (/ (* (/ l t) (/ l t)) (* (sin k) t)) |
| 0.2b | (* (/ l t) (/ l t)) |
| 837× | times-frac |
| 345× | add-sqr-sqrt |
| 333× | *-un-lft-identity add-cube-cbrt |
| 254× | add-cbrt-cube add-exp-log |
| 145× | cbrt-undiv div-exp |
| 96× | div-inv |
| 60× | associate-/r/ |
| 56× | prod-exp cbrt-unprod |
| 26× | associate-/r* |
| 21× | flip3-+ flip-+ |
| 19× | associate-/l* |
| 13× | swap-sqr associate-*r* associate-*l* |
| 11× | pow1 |
| 5× | associate-/l/ |
| 4× | insert-posit16 add-log-exp unswap-sqr |
| 3× | clear-num frac-2neg |
| 2× | frac-times associate-*l/ associate-*r/ |
| 1× | pow2 pow-plus pow-prod-down tan-quot pow-sqr *-commutative pow-prod-up |
| 65.0ms | (/ (/ 2 (+ (* (/ k t) (/ k t)) 2)) (/ (tan k) (/ (* (/ l t) (/ l t)) (* (sin k) t)))) |
| 36.0ms | (/ (tan k) (/ (* (/ l t) (/ l t)) (* (sin k) t))) |
| 19.0ms | (/ (* (/ l t) (/ l t)) (* (sin k) t)) |
| 12.0ms | (* (/ l t) (/ l t)) |
| 894.0ms | (/ (/ 2 (+ (* (/ k t) (/ k t)) 2)) (/ (tan k) (/ (* (/ l t) (/ l t)) (* (sin k) t)))) |
| 328.0ms | (/ (tan k) (/ (* (/ l t) (/ l t)) (* (sin k) t))) |
| 128.0ms | (/ (* (/ l t) (/ l t)) (* (sin k) t)) |
| 32.0ms | (* (/ l t) (/ l t)) |
15 alts after pruning (15 fresh and 0 done)
Merged error: 11.5b
Found 4 expressions with local error:
| 10.7b | (/ (sqrt (/ 2 (+ (* (/ k t) (/ k t)) 2))) (/ (tan k) (/ (/ l t) t))) |
| 10.5b | (sqrt (/ 2 (+ (* (/ k t) (/ k t)) 2))) |
| 10.5b | (sqrt (/ 2 (+ (* (/ k t) (/ k t)) 2))) |
| 6.4b | (/ (sqrt (/ 2 (+ (* (/ k t) (/ k t)) 2))) (/ 1 (/ (/ l t) (sin k)))) |
| 19700× | times-frac |
| 7846× | add-sqr-sqrt |
| 7840× | *-un-lft-identity add-cube-cbrt |
| 4080× | sqrt-prod |
| 768× | div-inv |
| 584× | associate-/r/ |
| 272× | flip3-+ flip-+ |
| 268× | associate-/r* |
| 50× | add-exp-log |
| 36× | associate-/l* |
| 35× | div-exp |
| 32× | add-cbrt-cube |
| 20× | cbrt-undiv |
| 6× | pow1 |
| 4× | rem-sqrt-square sqrt-div insert-posit16 add-log-exp |
| 3× | rec-exp 1-exp |
| 2× | clear-num frac-2neg sqrt-pow1 pow1/2 associate-/l/ |
| 74.0ms | (/ (sqrt (/ 2 (+ (* (/ k t) (/ k t)) 2))) (/ (tan k) (/ (/ l t) t))) |
| 52.0ms | (/ (sqrt (/ 2 (+ (* (/ k t) (/ k t)) 2))) (/ 1 (/ (/ l t) (sin k)))) |
| 28.0ms | (sqrt (/ 2 (+ (* (/ k t) (/ k t)) 2))) |
| 14.0ms | (sqrt (/ 2 (+ (* (/ k t) (/ k t)) 2))) |
| 508.0ms | (/ (sqrt (/ 2 (+ (* (/ k t) (/ k t)) 2))) (/ (tan k) (/ (/ l t) t))) |
| 303.0ms | (/ (sqrt (/ 2 (+ (* (/ k t) (/ k t)) 2))) (/ 1 (/ (/ l t) (sin k)))) |
| 140.0ms | (sqrt (/ 2 (+ (* (/ k t) (/ k t)) 2))) |
| 136.0ms | (sqrt (/ 2 (+ (* (/ k t) (/ k t)) 2))) |
13 alts after pruning (13 fresh and 0 done)
Merged error: 10.3b
Found 4 expressions with local error:
| 10.5b | (sqrt (/ 2 (+ (* (/ k t) (/ k t)) 2))) |
| 10.5b | (sqrt (/ 2 (+ (* (/ k t) (/ k t)) 2))) |
| 10.5b | (sqrt (/ 2 (+ (* (/ k t) (/ k t)) 2))) |
| 8.9b | (sqrt (sqrt (/ 2 (+ (* (/ k t) (/ k t)) 2)))) |
| 80× | sqrt-prod |
| 46× | add-sqr-sqrt |
| 40× | times-frac |
| 33× | *-un-lft-identity add-cube-cbrt |
| 9× | pow1 rem-sqrt-square |
| 8× | associate-/r/ |
| 7× | sqrt-pow1 |
| 5× | pow1/2 sqrt-div |
| 4× | flip3-+ add-cbrt-cube add-exp-log flip-+ insert-posit16 div-inv add-log-exp |
| 20.0ms | (sqrt (/ 2 (+ (* (/ k t) (/ k t)) 2))) |
| 15.0ms | (sqrt (sqrt (/ 2 (+ (* (/ k t) (/ k t)) 2)))) |
| 15.0ms | (sqrt (/ 2 (+ (* (/ k t) (/ k t)) 2))) |
| 14.0ms | (sqrt (/ 2 (+ (* (/ k t) (/ k t)) 2))) |
| 319.0ms | (sqrt (sqrt (/ 2 (+ (* (/ k t) (/ k t)) 2)))) |
| 141.0ms | (sqrt (/ 2 (+ (* (/ k t) (/ k t)) 2))) |
| 129.0ms | (sqrt (/ 2 (+ (* (/ k t) (/ k t)) 2))) |
| 121.0ms | (sqrt (/ 2 (+ (* (/ k t) (/ k t)) 2))) |
13 alts after pruning (12 fresh and 1 done)
Merged error: 10.3b
Found 4 expressions with local error:
| 10.9b | (sqrt (/ (sqrt 2) (+ (* (/ k t) (/ k t)) 2))) |
| 10.5b | (sqrt (/ 2 (+ (* (/ k t) (/ k t)) 2))) |
| 9.0b | (/ (sqrt (/ (sqrt 2) (+ (* (/ k t) (/ k t)) 2))) t) |
| 6.4b | (/ (sqrt (/ 2 (+ (* (/ k t) (/ k t)) 2))) (/ 1 (/ (/ l t) (sin k)))) |
| 10023× | times-frac |
| 4027× | add-sqr-sqrt |
| 4019× | *-un-lft-identity add-cube-cbrt |
| 2206× | sqrt-prod |
| 390× | div-inv |
| 302× | associate-/r/ |
| 141× | flip3-+ flip-+ |
| 137× | associate-/r* |
| 45× | associate-/l* |
| 38× | add-exp-log |
| 26× | div-exp |
| 20× | add-cbrt-cube |
| 11× | cbrt-undiv |
| 6× | pow1 |
| 5× | rem-sqrt-square |
| 4× | sqrt-div insert-posit16 add-log-exp |
| 3× | rec-exp 1-exp |
| 2× | clear-num frac-2neg sqrt-pow1 pow1/2 associate-/l/ |
| 63.0ms | (/ (sqrt (/ 2 (+ (* (/ k t) (/ k t)) 2))) (/ 1 (/ (/ l t) (sin k)))) |
| 29.0ms | (/ (sqrt (/ (sqrt 2) (+ (* (/ k t) (/ k t)) 2))) t) |
| 26.0ms | (sqrt (/ 2 (+ (* (/ k t) (/ k t)) 2))) |
| 15.0ms | (sqrt (/ (sqrt 2) (+ (* (/ k t) (/ k t)) 2))) |
| 289.0ms | (/ (sqrt (/ 2 (+ (* (/ k t) (/ k t)) 2))) (/ 1 (/ (/ l t) (sin k)))) |
| 195.0ms | (/ (sqrt (/ (sqrt 2) (+ (* (/ k t) (/ k t)) 2))) t) |
| 176.0ms | (sqrt (/ (sqrt 2) (+ (* (/ k t) (/ k t)) 2))) |
| 109.0ms | (sqrt (/ 2 (+ (* (/ k t) (/ k t)) 2))) |
12 alts after pruning (10 fresh and 2 done)
Merged error: 10.3b
0% (0.3b remaining)
Error of 10.8b against oracle of 10.5b and baseline of 10.8b
| 4.7s | 2082× | body | 1280 | valid |
| 2.2s | 1724× | body | 640 | valid |
| 1.5s | 5851× | body | 80 | valid |
| 1.1s | 880× | body | 320 | valid |
| 229.0ms | 385× | body | 160 | valid |