Time bar (total: 43.6s)
| 176.0ms | 67× | body | 1280 | valid |
| 103.0ms | 58× | body | 640 | valid |
| 70.0ms | 178× | body | 80 | valid |
| 52.0ms | 22× | body | 160 | valid |
| 52.0ms | 41× | body | 320 | valid |
2 alts after pruning (2 fresh and 0 done)
Merged error: 17.6b
Found 4 expressions with local error:
| 15.1b | (/ (/ 2 (+ (* (/ k t) (/ k t)) 2)) (* (* (* (/ t l) t) (sin k)) (* (tan k) (/ t l)))) |
| 4.2b | (* (* (/ t l) t) (sin k)) |
| 3.1b | (* (tan k) (/ t l)) |
| 0.3b | (/ 2 (+ (* (/ k t) (/ k t)) 2)) |
| 169× | add-cbrt-cube add-exp-log |
| 77× | prod-exp cbrt-unprod |
| 56× | cbrt-undiv div-exp |
| 52× | times-frac |
| 40× | add-sqr-sqrt |
| 35× | *-un-lft-identity add-cube-cbrt |
| 18× | associate-/l* |
| 16× | associate-*r* |
| 14× | associate-*l/ |
| 13× | associate-/r/ |
| 11× | pow1 |
| 6× | frac-times tan-quot associate-*r/ |
| 5× | div-inv |
| 4× | associate-/r* associate-*l* pow-prod-down insert-posit16 add-log-exp |
| 3× | flip3-+ flip-+ |
| 2× | clear-num frac-2neg *-commutative unswap-sqr |
| 1× | associate-/l/ |
| 130.0ms | (/ (/ 2 (+ (* (/ k t) (/ k t)) 2)) (* (* (* (/ t l) t) (sin k)) (* (tan k) (/ t l)))) |
| 29.0ms | (* (* (/ t l) t) (sin k)) |
| 25.0ms | (/ 2 (+ (* (/ k t) (/ k t)) 2)) |
| 14.0ms | (* (tan k) (/ t l)) |
| 818.0ms | (/ (/ 2 (+ (* (/ k t) (/ k t)) 2)) (* (* (* (/ t l) t) (sin k)) (* (tan k) (/ t l)))) |
| 135.0ms | (* (tan k) (/ t l)) |
| 81.0ms | (* (* (/ t l) t) (sin k)) |
| 78.0ms | (/ 2 (+ (* (/ k t) (/ k t)) 2)) |
14 alts after pruning (14 fresh and 0 done)
Merged error: 10.6b
Found 4 expressions with local error:
| 14.0b | (/ (/ 1 (sqrt (+ (* (/ k t) (/ k t)) 2))) (* (* (/ t l) t) (sin k))) |
| 8.2b | (/ (/ 2 (sqrt (+ (* (/ k t) (/ k t)) 2))) (* (tan k) (/ t l))) |
| 8.2b | (sqrt (+ (* (/ k t) (/ k t)) 2)) |
| 8.2b | (sqrt (+ (* (/ k t) (/ k t)) 2)) |
| 120× | times-frac |
| 85× | add-exp-log |
| 60× | add-sqr-sqrt |
| 58× | *-un-lft-identity add-cube-cbrt |
| 57× | add-cbrt-cube |
| 48× | associate-/l* |
| 42× | sqrt-prod |
| 39× | div-exp |
| 25× | cbrt-undiv |
| 24× | prod-exp |
| 14× | cbrt-unprod |
| 12× | sqrt-div associate-/r/ |
| 6× | pow1 flip3-+ flip-+ div-inv |
| 4× | rec-exp 1-exp insert-posit16 add-log-exp |
| 3× | associate-*l/ |
| 2× | rem-sqrt-square clear-num associate-/r* frac-2neg sqrt-pow1 pow1/2 tan-quot associate-/l/ |
| 1× | frac-times associate-*r/ |
| 81.0ms | (/ (/ 1 (sqrt (+ (* (/ k t) (/ k t)) 2))) (* (* (/ t l) t) (sin k))) |
| 64.0ms | (/ (/ 2 (sqrt (+ (* (/ k t) (/ k t)) 2))) (* (tan k) (/ t l))) |
| 17.0ms | (sqrt (+ (* (/ k t) (/ k t)) 2)) |
| 14.0ms | (sqrt (+ (* (/ k t) (/ k t)) 2)) |
| 343.0ms | (/ (/ 2 (sqrt (+ (* (/ k t) (/ k t)) 2))) (* (tan k) (/ t l))) |
| 243.0ms | (/ (/ 1 (sqrt (+ (* (/ k t) (/ k t)) 2))) (* (* (/ t l) t) (sin k))) |
| 56.0ms | (sqrt (+ (* (/ k t) (/ k t)) 2)) |
| 50.0ms | (sqrt (+ (* (/ k t) (/ k t)) 2)) |
12 alts after pruning (12 fresh and 0 done)
Merged error: 10.5b
Found 4 expressions with local error:
| 14.0b | (* (sqrt (+ (* (/ k t) (/ k t)) 2)) (* (/ t l) (* t (sin k)))) |
| 8.2b | (/ (/ 2 (sqrt (+ (* (/ k t) (/ k t)) 2))) (* (tan k) (/ t l))) |
| 8.2b | (sqrt (+ (* (/ k t) (/ k t)) 2)) |
| 8.2b | (sqrt (+ (* (/ k t) (/ k t)) 2)) |
| 60× | times-frac |
| 43× | add-cbrt-cube add-exp-log |
| 36× | add-sqr-sqrt |
| 34× | *-un-lft-identity add-cube-cbrt |
| 27× | sqrt-prod |
| 24× | associate-/l* |
| 15× | pow1 prod-exp cbrt-unprod |
| 13× | cbrt-undiv div-exp |
| 12× | sqrt-div |
| 7× | associate-/r/ |
| 6× | flip3-+ associate-*l* pow-prod-down associate-*l/ flip-+ |
| 4× | insert-posit16 add-log-exp |
| 3× | frac-times div-inv |
| 2× | rem-sqrt-square sqrt-pow1 pow1/2 tan-quot associate-*r/ |
| 1× | clear-num associate-/r* frac-2neg associate-*r* *-commutative associate-/l/ |
| 127.0ms | (* (sqrt (+ (* (/ k t) (/ k t)) 2)) (* (/ t l) (* t (sin k)))) |
| 51.0ms | (/ (/ 2 (sqrt (+ (* (/ k t) (/ k t)) 2))) (* (tan k) (/ t l))) |
| 26.0ms | (sqrt (+ (* (/ k t) (/ k t)) 2)) |
| 15.0ms | (sqrt (+ (* (/ k t) (/ k t)) 2)) |
| 372.0ms | (/ (/ 2 (sqrt (+ (* (/ k t) (/ k t)) 2))) (* (tan k) (/ t l))) |
| 255.0ms | (* (sqrt (+ (* (/ k t) (/ k t)) 2)) (* (/ t l) (* t (sin k)))) |
| 72.0ms | (sqrt (+ (* (/ k t) (/ k t)) 2)) |
| 60.0ms | (sqrt (+ (* (/ k t) (/ k t)) 2)) |
12 alts after pruning (11 fresh and 1 done)
Merged error: 10.5b
Found 4 expressions with local error:
| 14.0b | (* (* (sqrt (sqrt (+ (* (/ k t) (/ k t)) 2))) (sqrt (sqrt (+ (* (/ k t) (/ k t)) 2)))) (* (/ t l) (* t (sin k)))) |
| 12.3b | (sqrt (sqrt (+ (* (/ k t) (/ k t)) 2))) |
| 12.3b | (sqrt (sqrt (+ (* (/ k t) (/ k t)) 2))) |
| 8.2b | (/ (/ 2 (sqrt (+ (* (/ k t) (/ k t)) 2))) (* (tan k) (/ t l))) |
| 66× | add-cbrt-cube add-exp-log |
| 60× | times-frac sqrt-div |
| 38× | add-sqr-sqrt sqrt-prod |
| 34× | *-un-lft-identity add-cube-cbrt |
| 31× | prod-exp cbrt-unprod |
| 29× | pow1 |
| 24× | associate-/l* |
| 22× | associate-*l/ |
| 17× | frac-times |
| 16× | flip3-+ flip-+ |
| 15× | cbrt-undiv div-exp pow-prod-down |
| 8× | sqrt-pow1 |
| 7× | associate-/r/ |
| 6× | associate-*r/ |
| 4× | rem-sqrt-square pow1/2 insert-posit16 add-log-exp |
| 3× | div-inv |
| 2× | tan-quot |
| 1× | clear-num associate-/r* frac-2neg associate-*r* associate-*l* *-commutative associate-/l/ |
| 198.0ms | (* (* (sqrt (sqrt (+ (* (/ k t) (/ k t)) 2))) (sqrt (sqrt (+ (* (/ k t) (/ k t)) 2)))) (* (/ t l) (* t (sin k)))) |
| 35.0ms | (/ (/ 2 (sqrt (+ (* (/ k t) (/ k t)) 2))) (* (tan k) (/ t l))) |
| 28.0ms | (sqrt (sqrt (+ (* (/ k t) (/ k t)) 2))) |
| 25.0ms | (sqrt (sqrt (+ (* (/ k t) (/ k t)) 2))) |
| 297.0ms | (/ (/ 2 (sqrt (+ (* (/ k t) (/ k t)) 2))) (* (tan k) (/ t l))) |
| 258.0ms | (* (* (sqrt (sqrt (+ (* (/ k t) (/ k t)) 2))) (sqrt (sqrt (+ (* (/ k t) (/ k t)) 2)))) (* (/ t l) (* t (sin k)))) |
| 226.0ms | (sqrt (sqrt (+ (* (/ k t) (/ k t)) 2))) |
| 176.0ms | (sqrt (sqrt (+ (* (/ k t) (/ k t)) 2))) |
11 alts after pruning (10 fresh and 1 done)
Merged error: 10.5b
0% (0.8b remaining)
Error of 11.4b against oracle of 10.6b and baseline of 11.4b
| 7.1s | 2049× | body | 1280 | valid |
| 3.8s | 1677× | body | 640 | valid |
| 2.5s | 5982× | body | 80 | valid |
| 1.8s | 884× | body | 320 | valid |
| 394.0ms | 447× | body | 160 | valid |