Time bar (total: 3.0m)
| 88.0ms | 75× | body | 1280 | valid |
| 53.0ms | 72× | body | 640 | valid |
| 44.0ms | 259× | body | 80 | valid |
| 20.0ms | 34× | body | 320 | valid |
| 5.0ms | 14× | body | 160 | valid |
| 141.0ms | (+ (* (/ (cos th) (sqrt 2)) (* a1 a1)) (* (/ (cos th) (sqrt 2)) (* a2 a2))) |
2 alts after pruning (2 fresh and 0 done)
Merged error: 0.4b
Found 4 expressions with local error:
| 0.7b | (/ (cos th) (sqrt 2)) |
| 0.7b | (/ (cos th) (sqrt 2)) |
| 0.2b | (* (/ (cos th) (sqrt 2)) (* a2 a2)) |
| 0.2b | (* (/ (cos th) (sqrt 2)) (* a1 a1)) |
| 76× | times-frac |
| 70× | add-sqr-sqrt |
| 60× | *-un-lft-identity add-cube-cbrt |
| 44× | associate-*l* sqrt-prod |
| 32× | add-cbrt-cube add-exp-log |
| 14× | pow1 |
| 12× | associate-/r* prod-exp cbrt-unprod |
| 6× | cbrt-undiv div-exp pow-prod-down associate-/l* unswap-sqr |
| 4× | insert-posit16 div-inv add-log-exp |
| 2× | clear-num frac-2neg associate-*r* associate-*l/ *-commutative |
| 32.0ms | (* (/ (cos th) (sqrt 2)) (* a2 a2)) |
| 25.0ms | (* (/ (cos th) (sqrt 2)) (* a1 a1)) |
| 17.0ms | (/ (cos th) (sqrt 2)) |
| 17.0ms | (/ (cos th) (sqrt 2)) |
| 173.0ms | (* (/ (cos th) (sqrt 2)) (* a1 a1)) |
| 131.0ms | (* (/ (cos th) (sqrt 2)) (* a2 a2)) |
| 99.0ms | (/ (cos th) (sqrt 2)) |
| 83.0ms | (/ (cos th) (sqrt 2)) |
| 666.0ms | (* (* (* (/ (cos th) (sqrt 2)) (/ (cos th) (sqrt 2))) (/ (cos th) (sqrt 2))) (* (* (* a2 a2) (* a2 a2)) (* a2 a2))) |
| 614.0ms | (* (* (* (/ (cos th) (sqrt 2)) (/ (cos th) (sqrt 2))) (/ (cos th) (sqrt 2))) (* (* (* a1 a1) a1) (* (* a1 a1) a1))) |
| 614.0ms | (* (* (* (/ (cos th) (sqrt 2)) (/ (cos th) (sqrt 2))) (/ (cos th) (sqrt 2))) (* (* (* a2 a2) a2) (* (* a2 a2) a2))) |
| 591.0ms | (* (* (* (/ (cos th) (sqrt 2)) (/ (cos th) (sqrt 2))) (/ (cos th) (sqrt 2))) (* (* (* a1 a1) (* a1 a1)) (* a1 a1))) |
| 355.0ms | (- (+ (/ 1 (sqrt 2)) (* 1/24 (/ (pow th 4) (sqrt 2)))) (* 1/2 (/ (pow th 2) (sqrt 2)))) |
9 alts after pruning (9 fresh and 0 done)
Merged error: 0b
Found 4 expressions with local error:
| 0.7b | (/ (cos th) (sqrt 2)) |
| 0.7b | (/ (cos th) (sqrt (sqrt 2))) |
| 0.6b | (/ (/ (cos th) (sqrt (sqrt 2))) (sqrt (sqrt 2))) |
| 0.2b | (* (/ (cos th) (sqrt 2)) (* a2 a2)) |
| 616× | sqrt-prod |
| 614× | times-frac |
| 345× | add-sqr-sqrt |
| 340× | *-un-lft-identity add-cube-cbrt |
| 37× | associate-/l* |
| 25× | add-cbrt-cube add-exp-log |
| 24× | associate-/r* |
| 22× | associate-*l* |
| 14× | div-inv |
| 9× | pow1 |
| 7× | cbrt-undiv div-exp |
| 6× | prod-exp cbrt-unprod |
| 4× | insert-posit16 add-log-exp |
| 3× | clear-num frac-2neg pow-prod-down unswap-sqr |
| 1× | associate-*r* associate-*l/ *-commutative associate-/l/ |
| 43.0ms | (* (/ (cos th) (sqrt 2)) (* a2 a2)) |
| 34.0ms | (/ (/ (cos th) (sqrt (sqrt 2))) (sqrt (sqrt 2))) |
| 18.0ms | (/ (cos th) (sqrt (sqrt 2))) |
| 9.0ms | (/ (cos th) (sqrt 2)) |
| 167.0ms | (* (/ (cos th) (sqrt 2)) (* a2 a2)) |
| 139.0ms | (/ (cos th) (sqrt (sqrt 2))) |
| 89.0ms | (/ (/ (cos th) (sqrt (sqrt 2))) (sqrt (sqrt 2))) |
| 76.0ms | (/ (cos th) (sqrt 2)) |
| 650.0ms | (* (* (* (/ (cos th) (sqrt 2)) (/ (cos th) (sqrt 2))) (/ (cos th) (sqrt 2))) (* (* (* a2 a2) (* a2 a2)) (* a2 a2))) |
| 588.0ms | (* (* (* (/ (cos th) (sqrt 2)) (/ (cos th) (sqrt 2))) (/ (cos th) (sqrt 2))) (* (* (* a2 a2) a2) (* (* a2 a2) a2))) |
| 512.0ms | (/ (* (* (cos th) (cos th)) (cos th)) (* (* (sqrt (sqrt 2)) (sqrt (sqrt 2))) (sqrt (sqrt 2)))) |
| 449.0ms | (/ (/ (* (cbrt (cos th)) (cbrt (cos th))) (sqrt (sqrt (sqrt 2)))) (sqrt (* (cbrt (sqrt 2)) (cbrt (sqrt 2))))) |
| 365.0ms | (- (+ (/ 1 (sqrt 2)) (* 1/24 (/ (pow th 4) (sqrt 2)))) (* 1/2 (/ (pow th 2) (sqrt 2)))) |
8 alts after pruning (8 fresh and 0 done)
Merged error: 0b
Found 4 expressions with local error:
| 1.0b | (/ (/ 1 (sqrt (sqrt 2))) (sqrt (cbrt (sqrt 2)))) |
| 1.0b | (/ 1 (sqrt (sqrt 2))) |
| 0.7b | (/ (cos th) (sqrt 2)) |
| 0.2b | (* (/ (cos th) (sqrt 2)) (* a2 a2)) |
| 793× | sqrt-prod |
| 788× | times-frac |
| 434× | add-sqr-sqrt |
| 429× | *-un-lft-identity add-cube-cbrt |
| 192× | cbrt-prod |
| 37× | associate-/l* |
| 31× | add-exp-log |
| 27× | associate-/r* |
| 25× | add-cbrt-cube |
| 22× | associate-*l* |
| 17× | div-inv |
| 13× | pow1 |
| 11× | div-exp |
| 7× | cbrt-undiv sqrt-pow1 pow-flip |
| 6× | prod-exp cbrt-unprod |
| 4× | insert-posit16 add-log-exp |
| 3× | clear-num frac-2neg pow1/2 pow-prod-down unswap-sqr |
| 2× | rec-exp pow1/3 1-exp pow-div |
| 1× | associate-*r* associate-*l/ *-commutative inv-pow associate-/l/ |
| 32.0ms | (* (/ (cos th) (sqrt 2)) (* a2 a2)) |
| 18.0ms | (/ (cos th) (sqrt 2)) |
| 12.0ms | (/ (/ 1 (sqrt (sqrt 2))) (sqrt (cbrt (sqrt 2)))) |
| 6.0ms | (/ 1 (sqrt (sqrt 2))) |
| 142.0ms | (* (/ (cos th) (sqrt 2)) (* a2 a2)) |
| 81.0ms | (/ (cos th) (sqrt 2)) |
| 0.0ms | (/ (/ 1 (sqrt (sqrt 2))) (sqrt (cbrt (sqrt 2)))) |
| 0.0ms | (/ 1 (sqrt (sqrt 2))) |
| 685.0ms | (* (* (* (/ (cos th) (sqrt 2)) (/ (cos th) (sqrt 2))) (/ (cos th) (sqrt 2))) (* (* (* a2 a2) (* a2 a2)) (* a2 a2))) |
| 681.0ms | (* (* (* (/ (cos th) (sqrt 2)) (/ (cos th) (sqrt 2))) (/ (cos th) (sqrt 2))) (* (* (* a2 a2) a2) (* (* a2 a2) a2))) |
| 521.0ms | (+ (- (log (cos th)) (log (sqrt 2))) (+ (log a2) (log a2))) |
| 392.0ms | (- (+ (/ 1 (sqrt 2)) (* 1/24 (/ (pow th 4) (sqrt 2)))) (* 1/2 (/ (pow th 2) (sqrt 2)))) |
| 364.0ms | (/ (* (* (/ 1 (sqrt (sqrt 2))) (/ 1 (sqrt (sqrt 2)))) (/ 1 (sqrt (sqrt 2)))) (* (* (sqrt (cbrt (sqrt 2))) (sqrt (cbrt (sqrt 2)))) (sqrt (cbrt (sqrt 2))))) |
7 alts after pruning (7 fresh and 0 done)
Merged error: 0b
Found 4 expressions with local error:
| 1.0b | (/ (/ 1 (sqrt (sqrt 2))) (sqrt (cbrt (sqrt 2)))) |
| 1.0b | (/ 1 (sqrt (sqrt 2))) |
| 0.7b | (/ (cos th) (sqrt (sqrt 2))) |
| 0.6b | (/ (/ (cos th) (sqrt (sqrt 2))) (sqrt (sqrt 2))) |
| 1365× | sqrt-prod |
| 1326× | times-frac |
| 709× | add-sqr-sqrt *-un-lft-identity add-cube-cbrt |
| 192× | cbrt-prod |
| 68× | associate-/l* |
| 39× | associate-/r* |
| 27× | div-inv |
| 24× | add-exp-log |
| 18× | add-cbrt-cube |
| 12× | div-exp |
| 8× | pow1 cbrt-undiv |
| 7× | sqrt-pow1 pow-flip |
| 4× | clear-num frac-2neg insert-posit16 add-log-exp |
| 3× | pow1/2 |
| 2× | rec-exp pow1/3 1-exp pow-div associate-/l/ |
| 1× | inv-pow |
| 29.0ms | (/ (/ (cos th) (sqrt (sqrt 2))) (sqrt (sqrt 2))) |
| 24.0ms | (/ (/ 1 (sqrt (sqrt 2))) (sqrt (cbrt (sqrt 2)))) |
| 18.0ms | (/ (cos th) (sqrt (sqrt 2))) |
| 12.0ms | (/ 1 (sqrt (sqrt 2))) |
| 176.0ms | (/ (cos th) (sqrt (sqrt 2))) |
| 67.0ms | (/ (/ (cos th) (sqrt (sqrt 2))) (sqrt (sqrt 2))) |
| 0.0ms | (/ (/ 1 (sqrt (sqrt 2))) (sqrt (cbrt (sqrt 2)))) |
| 0.0ms | (/ 1 (sqrt (sqrt 2))) |
| 557.0ms | (/ (/ (* (cbrt (cos th)) (cbrt (cos th))) (* (cbrt (sqrt (sqrt 2))) (cbrt (sqrt (sqrt 2))))) (* (cbrt (sqrt (sqrt 2))) (cbrt (sqrt (sqrt 2))))) |
| 433.0ms | (/ (* (* (cos th) (cos th)) (cos th)) (* (* (sqrt (sqrt 2)) (sqrt (sqrt 2))) (sqrt (sqrt 2)))) |
| 418.0ms | (/ (/ (* (cbrt 1) (cbrt 1)) (* (cbrt (sqrt (sqrt 2))) (cbrt (sqrt (sqrt 2))))) (* (cbrt (sqrt (cbrt (sqrt 2)))) (cbrt (sqrt (cbrt (sqrt 2)))))) |
| 391.0ms | (/ (/ (* (* (cos th) (cos th)) (cos th)) (* (* (sqrt (sqrt 2)) (sqrt (sqrt 2))) (sqrt (sqrt 2)))) (* (* (sqrt (sqrt 2)) (sqrt (sqrt 2))) (sqrt (sqrt 2)))) |
| 308.0ms | (- (+ (/ 1 (sqrt 2)) (* 1/24 (/ (pow th 4) (sqrt 2)))) (* 1/2 (/ (pow th 2) (sqrt 2)))) |
7 alts after pruning (6 fresh and 1 done)
Merged error: 0b
0% (0.4b remaining)
Error of 0.5b against oracle of 0.0b and baseline of 0.5b
| 3.2s | 2508× | body | 1280 | valid |
| 2.6s | 2055× | body | 640 | valid |
| 1.7s | 8001× | body | 80 | valid |
| 620.0ms | 1084× | body | 320 | valid |
| 184.0ms | 532× | body | 160 | valid |