Time bar (total: 1.1m)
| 167.0ms | 256× | body | 80 | valid |
| 44.0ms | 256× | pre | 80 | true |
1 alts after pruning (1 fresh and 0 done)
Merged error: 0.4b
Found 4 expressions with local error:
| 0.4b | (* (/ 1 6) (pow (* -2 (log u1)) 0.5)) |
| 0.2b | (* (* 2 PI) u2) |
| 0.1b | (pow (* -2 (log u1)) 0.5) |
| 0.0b | (+ (* (* (/ 1 6) (pow (* -2 (log u1)) 0.5)) (cos (* (* 2 PI) u2))) 0.5) |
| 48× | add-exp-log |
| 25× | add-sqr-sqrt |
| 24× | prod-exp |
| 16× | *-un-lft-identity |
| 14× | add-cbrt-cube associate-*l* add-cube-cbrt |
| 13× | times-frac |
| 12× | pow1 |
| 10× | pow-exp |
| 8× | div-exp associate-*r* |
| 6× | add-log-exp unswap-sqr |
| 5× | pow-to-exp cbrt-unprod sqr-pow |
| 4× | rec-exp 1-exp pow-prod-down insert-posit16 |
| 3× | pow-unpow |
| 2× | unpow-prod-down pow-pow *-commutative |
| 1× | cbrt-undiv +-commutative sum-log flip3-+ associate-*l/ flip-+ div-inv |
| 80.0ms | (+ (* (* (/ 1 6) (pow (* -2 (log u1)) 0.5)) (cos (* (* 2 PI) u2))) 0.5) |
| 34.0ms | (* (/ 1 6) (pow (* -2 (log u1)) 0.5)) |
| 27.0ms | (* (* 2 PI) u2) |
| 9.0ms | (pow (* -2 (log u1)) 0.5) |
| 1.6s | (* (/ 1 6) (pow (* -2 (log u1)) 0.5)) |
| 585.0ms | (+ (* (* (/ 1 6) (pow (* -2 (log u1)) 0.5)) (cos (* (* 2 PI) u2))) 0.5) |
| 350.0ms | (pow (* -2 (log u1)) 0.5) |
| 56.0ms | (* (* 2 PI) u2) |
10 alts after pruning (10 fresh and 0 done)
Merged error: 0.0b
Found 4 expressions with local error:
| 0.3b | (* (sqrt (/ 1 6)) (pow (* -2 (log u1)) 0.5)) |
| 0.3b | (* (sqrt (/ 1 6)) (* (sqrt (/ 1 6)) (pow (* -2 (log u1)) 0.5))) |
| 0.2b | (* (* 2 PI) u2) |
| 0.1b | (pow (* -2 (log u1)) 0.5) |
| 37× | add-sqr-sqrt |
| 34× | add-exp-log |
| 33× | associate-*l* |
| 32× | sqrt-prod |
| 25× | *-un-lft-identity |
| 23× | add-cube-cbrt |
| 22× | times-frac |
| 19× | prod-exp |
| 16× | add-cbrt-cube |
| 14× | pow1 |
| 9× | associate-*r* |
| 8× | unswap-sqr |
| 7× | cbrt-unprod |
| 6× | pow-exp sqr-pow |
| 5× | sqrt-div pow-prod-down |
| 4× | associate-*l/ insert-posit16 add-log-exp |
| 3× | pow-to-exp pow-unpow *-commutative |
| 2× | unpow-prod-down pow-pow div-inv |
| 1× | frac-times associate-*r/ |
| 81.0ms | (* (sqrt (/ 1 6)) (* (sqrt (/ 1 6)) (pow (* -2 (log u1)) 0.5))) |
| 30.0ms | (* (sqrt (/ 1 6)) (pow (* -2 (log u1)) 0.5)) |
| 22.0ms | (* (* 2 PI) u2) |
| 7.0ms | (pow (* -2 (log u1)) 0.5) |
| 1.1s | (* (sqrt (/ 1 6)) (* (sqrt (/ 1 6)) (pow (* -2 (log u1)) 0.5))) |
| 1.1s | (* (sqrt (/ 1 6)) (pow (* -2 (log u1)) 0.5)) |
| 428.0ms | (pow (* -2 (log u1)) 0.5) |
| 64.0ms | (* (* 2 PI) u2) |
7 alts after pruning (7 fresh and 0 done)
Merged error: 0.0b
Found 4 expressions with local error:
| 0.5b | (* (/ (* (cos (* (* PI u2) 2)) (pow (* -2 (log u1)) 0.5)) 6) (/ (* (cos (* (* PI u2) 2)) (pow (* -2 (log u1)) 0.5)) 6)) |
| 0.5b | (* (/ (* (cos (* (* PI u2) 2)) (pow (* -2 (log u1)) 0.5)) 6) (/ (* (cos (* (* PI u2) 2)) (pow (* -2 (log u1)) 0.5)) 6)) |
| 0.4b | (* (* (/ (* (cos (* (* PI u2) 2)) (pow (* -2 (log u1)) 0.5)) 6) (/ (* (cos (* (* PI u2) 2)) (pow (* -2 (log u1)) 0.5)) 6)) (/ (* (cos (* (* PI u2) 2)) (pow (* -2 (log u1)) 0.5)) 6)) |
| 0.3b | (/ (+ (* (* (/ (* (cos (* (* PI u2) 2)) (pow (* -2 (log u1)) 0.5)) 6) (/ (* (cos (* (* PI u2) 2)) (pow (* -2 (log u1)) 0.5)) 6)) (/ (* (cos (* (* PI u2) 2)) (pow (* -2 (log u1)) 0.5)) 6)) (* 0.5 (* 0.5 0.5))) (+ (* 0.5 (- 0.5 (/ (* (cos (* (* PI u2) 2)) (pow (* -2 (log u1)) 0.5)) 6))) (* (/ (* (cos (* (* PI u2) 2)) (pow (* -2 (log u1)) 0.5)) 6) (/ (* (cos (* (* PI u2) 2)) (pow (* -2 (log u1)) 0.5)) 6)))) |
| 2007× | add-exp-log |
| 1175× | prod-exp |
| 666× | div-exp |
| 266× | pow-exp |
| 249× | add-cbrt-cube |
| 133× | pow-to-exp |
| 115× | cbrt-unprod |
| 81× | cbrt-undiv |
| 39× | times-frac |
| 37× | pow1 |
| 36× | add-sqr-sqrt |
| 31× | *-un-lft-identity add-cube-cbrt |
| 21× | associate-*r* |
| 15× | associate-*l* |
| 14× | swap-sqr |
| 13× | associate-*r/ |
| 10× | div-inv |
| 9× | frac-times associate-*l/ |
| 8× | pow-plus associate-/r/ pow-prod-up |
| 6× | frac-add |
| 5× | pow3 pow-prod-down |
| 4× | pow2 cube-unmult pow-sqr sum-cubes insert-posit16 associate-/l* add-log-exp |
| 3× | associate-/r* flip3-- *-commutative flip-- unswap-sqr |
| 2× | flip3-+ flip-+ associate-/l/ |
| 1× | clear-num frac-2neg |
| 361.0ms | (/ (+ (* (* (/ (* (cos (* (* PI u2) 2)) (pow (* -2 (log u1)) 0.5)) 6) (/ (* (cos (* (* PI u2) 2)) (pow (* -2 (log u1)) 0.5)) 6)) (/ (* (cos (* (* PI u2) 2)) (pow (* -2 (log u1)) 0.5)) 6)) (* 0.5 (* 0.5 0.5))) (+ (* 0.5 (- 0.5 (/ (* (cos (* (* PI u2) 2)) (pow (* -2 (log u1)) 0.5)) 6))) (* (/ (* (cos (* (* PI u2) 2)) (pow (* -2 (log u1)) 0.5)) 6) (/ (* (cos (* (* PI u2) 2)) (pow (* -2 (log u1)) 0.5)) 6)))) |
| 112.0ms | (* (* (/ (* (cos (* (* PI u2) 2)) (pow (* -2 (log u1)) 0.5)) 6) (/ (* (cos (* (* PI u2) 2)) (pow (* -2 (log u1)) 0.5)) 6)) (/ (* (cos (* (* PI u2) 2)) (pow (* -2 (log u1)) 0.5)) 6)) |
| 28.0ms | (* (/ (* (cos (* (* PI u2) 2)) (pow (* -2 (log u1)) 0.5)) 6) (/ (* (cos (* (* PI u2) 2)) (pow (* -2 (log u1)) 0.5)) 6)) |
| 26.0ms | (* (/ (* (cos (* (* PI u2) 2)) (pow (* -2 (log u1)) 0.5)) 6) (/ (* (cos (* (* PI u2) 2)) (pow (* -2 (log u1)) 0.5)) 6)) |
| 1.8s | (/ (+ (* (* (/ (* (cos (* (* PI u2) 2)) (pow (* -2 (log u1)) 0.5)) 6) (/ (* (cos (* (* PI u2) 2)) (pow (* -2 (log u1)) 0.5)) 6)) (/ (* (cos (* (* PI u2) 2)) (pow (* -2 (log u1)) 0.5)) 6)) (* 0.5 (* 0.5 0.5))) (+ (* 0.5 (- 0.5 (/ (* (cos (* (* PI u2) 2)) (pow (* -2 (log u1)) 0.5)) 6))) (* (/ (* (cos (* (* PI u2) 2)) (pow (* -2 (log u1)) 0.5)) 6) (/ (* (cos (* (* PI u2) 2)) (pow (* -2 (log u1)) 0.5)) 6)))) |
| 561.0ms | (* (* (/ (* (cos (* (* PI u2) 2)) (pow (* -2 (log u1)) 0.5)) 6) (/ (* (cos (* (* PI u2) 2)) (pow (* -2 (log u1)) 0.5)) 6)) (/ (* (cos (* (* PI u2) 2)) (pow (* -2 (log u1)) 0.5)) 6)) |
| 505.0ms | (* (/ (* (cos (* (* PI u2) 2)) (pow (* -2 (log u1)) 0.5)) 6) (/ (* (cos (* (* PI u2) 2)) (pow (* -2 (log u1)) 0.5)) 6)) |
| 460.0ms | (* (/ (* (cos (* (* PI u2) 2)) (pow (* -2 (log u1)) 0.5)) 6) (/ (* (cos (* (* PI u2) 2)) (pow (* -2 (log u1)) 0.5)) 6)) |
6 alts after pruning (6 fresh and 0 done)
Merged error: 0.0b
Found 4 expressions with local error:
| 0.5b | (* (/ (* (cos (* (* PI u2) 2)) (pow (* -2 (log u1)) 0.5)) 6) (/ (* (cos (* (* PI u2) 2)) (pow (* -2 (log u1)) 0.5)) 6)) |
| 0.5b | (* (/ (pow (* -2 (log u1)) 0.5) 6) (/ (* (cos (* (* PI u2) 2)) (pow (* -2 (log u1)) 0.5)) 6)) |
| 0.4b | (* (* (/ (cos (* (* PI u2) 2)) 1) (* (/ (pow (* -2 (log u1)) 0.5) 6) (/ (* (cos (* (* PI u2) 2)) (pow (* -2 (log u1)) 0.5)) 6))) (/ (* (cos (* (* PI u2) 2)) (pow (* -2 (log u1)) 0.5)) 6)) |
| 0.3b | (/ (+ (* (* (/ (cos (* (* PI u2) 2)) 1) (* (/ (pow (* -2 (log u1)) 0.5) 6) (/ (* (cos (* (* PI u2) 2)) (pow (* -2 (log u1)) 0.5)) 6))) (/ (* (cos (* (* PI u2) 2)) (pow (* -2 (log u1)) 0.5)) 6)) (* 0.5 (* 0.5 0.5))) (+ (* 0.5 (- 0.5 (/ (* (cos (* (* PI u2) 2)) (pow (* -2 (log u1)) 0.5)) 6))) (* (/ (* (cos (* (* PI u2) 2)) (pow (* -2 (log u1)) 0.5)) 6) (/ (* (cos (* (* PI u2) 2)) (pow (* -2 (log u1)) 0.5)) 6)))) |
| 4815× | add-exp-log |
| 2847× | prod-exp |
| 1834× | div-exp |
| 630× | pow-exp |
| 351× | add-cbrt-cube |
| 315× | pow-to-exp |
| 186× | 1-exp |
| 173× | cbrt-unprod |
| 113× | cbrt-undiv |
| 44× | times-frac |
| 42× | add-sqr-sqrt |
| 33× | *-un-lft-identity add-cube-cbrt |
| 27× | associate-*l* |
| 22× | pow1 |
| 21× | frac-times associate-*r* associate-*r/ |
| 17× | associate-*l/ |
| 8× | pow-prod-down associate-/r/ div-inv |
| 7× | swap-sqr |
| 6× | frac-add |
| 4× | insert-posit16 add-log-exp unswap-sqr sqr-pow |
| 3× | associate-/r* unpow-prod-down flip3-- *-commutative flip-- associate-/l* |
| 2× | flip3-+ flip-+ associate-/l/ |
| 1× | pow2 clear-num frac-2neg pow-plus pow-sqr pow-prod-up |
| 505.0ms | (/ (+ (* (* (/ (cos (* (* PI u2) 2)) 1) (* (/ (pow (* -2 (log u1)) 0.5) 6) (/ (* (cos (* (* PI u2) 2)) (pow (* -2 (log u1)) 0.5)) 6))) (/ (* (cos (* (* PI u2) 2)) (pow (* -2 (log u1)) 0.5)) 6)) (* 0.5 (* 0.5 0.5))) (+ (* 0.5 (- 0.5 (/ (* (cos (* (* PI u2) 2)) (pow (* -2 (log u1)) 0.5)) 6))) (* (/ (* (cos (* (* PI u2) 2)) (pow (* -2 (log u1)) 0.5)) 6) (/ (* (cos (* (* PI u2) 2)) (pow (* -2 (log u1)) 0.5)) 6)))) |
| 212.0ms | (* (* (/ (cos (* (* PI u2) 2)) 1) (* (/ (pow (* -2 (log u1)) 0.5) 6) (/ (* (cos (* (* PI u2) 2)) (pow (* -2 (log u1)) 0.5)) 6))) (/ (* (cos (* (* PI u2) 2)) (pow (* -2 (log u1)) 0.5)) 6)) |
| 48.0ms | (* (/ (* (cos (* (* PI u2) 2)) (pow (* -2 (log u1)) 0.5)) 6) (/ (* (cos (* (* PI u2) 2)) (pow (* -2 (log u1)) 0.5)) 6)) |
| 34.0ms | (* (/ (pow (* -2 (log u1)) 0.5) 6) (/ (* (cos (* (* PI u2) 2)) (pow (* -2 (log u1)) 0.5)) 6)) |
| 1.7s | (/ (+ (* (* (/ (cos (* (* PI u2) 2)) 1) (* (/ (pow (* -2 (log u1)) 0.5) 6) (/ (* (cos (* (* PI u2) 2)) (pow (* -2 (log u1)) 0.5)) 6))) (/ (* (cos (* (* PI u2) 2)) (pow (* -2 (log u1)) 0.5)) 6)) (* 0.5 (* 0.5 0.5))) (+ (* 0.5 (- 0.5 (/ (* (cos (* (* PI u2) 2)) (pow (* -2 (log u1)) 0.5)) 6))) (* (/ (* (cos (* (* PI u2) 2)) (pow (* -2 (log u1)) 0.5)) 6) (/ (* (cos (* (* PI u2) 2)) (pow (* -2 (log u1)) 0.5)) 6)))) |
| 584.0ms | (* (/ (pow (* -2 (log u1)) 0.5) 6) (/ (* (cos (* (* PI u2) 2)) (pow (* -2 (log u1)) 0.5)) 6)) |
| 546.0ms | (* (/ (* (cos (* (* PI u2) 2)) (pow (* -2 (log u1)) 0.5)) 6) (/ (* (cos (* (* PI u2) 2)) (pow (* -2 (log u1)) 0.5)) 6)) |
| 541.0ms | (* (* (/ (cos (* (* PI u2) 2)) 1) (* (/ (pow (* -2 (log u1)) 0.5) 6) (/ (* (cos (* (* PI u2) 2)) (pow (* -2 (log u1)) 0.5)) 6))) (/ (* (cos (* (* PI u2) 2)) (pow (* -2 (log u1)) 0.5)) 6)) |
7 alts after pruning (6 fresh and 1 done)
Merged error: 0b
0% (0.4b remaining)
Error of 0.4b against oracle of 0.0b and baseline of 0.4b
| 2.5s | 8000× | body | 80 | valid |
| 422.0ms | 8000× | pre | 80 | true |