Time bar (total: 37.8s)
| 74.0ms | 256× | body | 80 | valid |
| 16.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 | (* u2 (* 2 PI)) |
| 0.1b | (pow (* -2 (log u1)) 0.5) |
| 0.0b | (+ 0.5 (* (* 1/6 (pow (* -2 (log u1)) 0.5)) (cos (* u2 (* 2 PI))))) |
| 20× | add-exp-log |
| 12× | pow1 |
| 11× | add-sqr-sqrt add-cbrt-cube |
| 9× | prod-exp |
| 8× | *-un-lft-identity add-cube-cbrt |
| 6× | associate-*r* associate-*l* add-log-exp |
| 4× | pow-prod-down pow-exp cbrt-unprod insert-posit16 |
| 3× | pow-unpow sqr-pow |
| 2× | pow-to-exp unpow-prod-down pow-pow *-commutative unswap-sqr |
| 1× | +-commutative sum-log flip3-+ flip-+ |
| 29.0ms | (* 1/6 (pow (* -2 (log u1)) 0.5)) |
| 23.0ms | (* u2 (* 2 PI)) |
| 20.0ms | (+ 0.5 (* (* 1/6 (pow (* -2 (log u1)) 0.5)) (cos (* u2 (* 2 PI))))) |
| 9.0ms | (pow (* -2 (log u1)) 0.5) |
| 907.0ms | (* 1/6 (pow (* -2 (log u1)) 0.5)) |
| 594.0ms | (+ 0.5 (* (* 1/6 (pow (* -2 (log u1)) 0.5)) (cos (* u2 (* 2 PI))))) |
| 356.0ms | (pow (* -2 (log u1)) 0.5) |
| 63.0ms | (* u2 (* 2 PI)) |
8 alts after pruning (8 fresh and 0 done)
Merged error: 0b
Found 4 expressions with local error:
| 0.3b | (* (sqrt 1/6) (* (sqrt 1/6) (pow (* -2 (log u1)) 0.5))) |
| 0.3b | (* (sqrt 1/6) (pow (* -2 (log u1)) 0.5)) |
| 0.2b | (* u2 (* 2 PI)) |
| 0.1b | (pow (* -2 (log u1)) 0.5) |
| 34× | add-exp-log |
| 19× | prod-exp |
| 17× | add-sqr-sqrt |
| 16× | add-cbrt-cube |
| 15× | associate-*l* |
| 14× | pow1 |
| 11× | *-un-lft-identity add-cube-cbrt |
| 8× | sqrt-prod |
| 7× | associate-*r* cbrt-unprod |
| 6× | pow-exp |
| 5× | pow-prod-down |
| 4× | insert-posit16 add-log-exp unswap-sqr sqr-pow |
| 3× | pow-to-exp pow-unpow *-commutative |
| 2× | unpow-prod-down pow-pow |
| 59.0ms | (* (sqrt 1/6) (* (sqrt 1/6) (pow (* -2 (log u1)) 0.5))) |
| 25.0ms | (* u2 (* 2 PI)) |
| 23.0ms | (* (sqrt 1/6) (pow (* -2 (log u1)) 0.5)) |
| 9.0ms | (pow (* -2 (log u1)) 0.5) |
| 1.0s | (* (sqrt 1/6) (pow (* -2 (log u1)) 0.5)) |
| 970.0ms | (* (sqrt 1/6) (* (sqrt 1/6) (pow (* -2 (log u1)) 0.5))) |
| 344.0ms | (pow (* -2 (log u1)) 0.5) |
| 38.0ms | (* u2 (* 2 PI)) |
8 alts after pruning (7 fresh and 1 done)
Merged error: 0b
Found 4 expressions with local error:
| 0.5b | (cbrt (* (* (pow (* -2 (log u1)) 0.5) (pow (* -2 (log u1)) 0.5)) (pow (* -2 (log u1)) 0.5))) |
| 0.5b | (* (pow (* -2 (log u1)) 0.5) (pow (* -2 (log u1)) 0.5)) |
| 0.4b | (* 1/6 (cbrt (* (* (pow (* -2 (log u1)) 0.5) (pow (* -2 (log u1)) 0.5)) (pow (* -2 (log u1)) 0.5)))) |
| 0.3b | (* (* (pow (* -2 (log u1)) 0.5) (pow (* -2 (log u1)) 0.5)) (pow (* -2 (log u1)) 0.5)) |
| 238× | add-exp-log |
| 206× | prod-exp |
| 114× | pow-exp |
| 57× | pow-to-exp |
| 18× | add-sqr-sqrt |
| 14× | associate-*r* |
| 12× | add-cbrt-cube |
| 11× | *-un-lft-identity add-cube-cbrt |
| 10× | sqr-pow |
| 9× | associate-*l* |
| 7× | unswap-sqr |
| 6× | pow1 |
| 5× | unpow-prod-down swap-sqr cbrt-unprod |
| 4× | pow-prod-down pow-prod-up insert-posit16 add-log-exp |
| 3× | *-commutative |
| 2× | cbrt-prod pow2 pow3 pow-sqr |
| 1× | pow-plus pow1/3 rem-cbrt-cube |
| 85.0ms | (* 1/6 (cbrt (* (* (pow (* -2 (log u1)) 0.5) (pow (* -2 (log u1)) 0.5)) (pow (* -2 (log u1)) 0.5)))) |
| 43.0ms | (* (* (pow (* -2 (log u1)) 0.5) (pow (* -2 (log u1)) 0.5)) (pow (* -2 (log u1)) 0.5)) |
| 30.0ms | (cbrt (* (* (pow (* -2 (log u1)) 0.5) (pow (* -2 (log u1)) 0.5)) (pow (* -2 (log u1)) 0.5))) |
| 15.0ms | (* (pow (* -2 (log u1)) 0.5) (pow (* -2 (log u1)) 0.5)) |
| 1.1s | (* 1/6 (cbrt (* (* (pow (* -2 (log u1)) 0.5) (pow (* -2 (log u1)) 0.5)) (pow (* -2 (log u1)) 0.5)))) |
| 1.0s | (cbrt (* (* (pow (* -2 (log u1)) 0.5) (pow (* -2 (log u1)) 0.5)) (pow (* -2 (log u1)) 0.5))) |
| 1.0s | (* (pow (* -2 (log u1)) 0.5) (pow (* -2 (log u1)) 0.5)) |
| 980.0ms | (* (* (pow (* -2 (log u1)) 0.5) (pow (* -2 (log u1)) 0.5)) (pow (* -2 (log u1)) 0.5)) |
7 alts after pruning (6 fresh and 1 done)
Merged error: 0b
Found 4 expressions with local error:
| 0.5b | (* (* -2 (log u1)) (* -2 (log u1))) |
| 0.5b | (cbrt (* (pow (* (* -2 (log u1)) (* -2 (log u1))) 0.5) (pow (* -2 (log u1)) 0.5))) |
| 0.4b | (* 1/6 (cbrt (* (pow (* (* -2 (log u1)) (* -2 (log u1))) 0.5) (pow (* -2 (log u1)) 0.5)))) |
| 0.3b | (* (pow (* (* -2 (log u1)) (* -2 (log u1))) 0.5) (pow (* -2 (log u1)) 0.5)) |
| 102× | add-exp-log |
| 76× | prod-exp |
| 45× | pow1 |
| 34× | pow-exp |
| 19× | add-sqr-sqrt add-cbrt-cube pow-prod-down |
| 12× | distribute-rgt-in log-prod *-un-lft-identity distribute-lft-in add-cube-cbrt |
| 11× | pow-to-exp |
| 10× | associate-*r* cbrt-unprod |
| 9× | associate-*l* |
| 7× | unswap-sqr sqr-pow |
| 6× | unpow-prod-down |
| 4× | pow-sqr pow-prod-up insert-posit16 add-log-exp |
| 3× | *-commutative |
| 2× | cbrt-prod pow-plus pow3 |
| 1× | pow2 pow1/3 swap-sqr rem-cbrt-cube |
| 60.0ms | (* 1/6 (cbrt (* (pow (* (* -2 (log u1)) (* -2 (log u1))) 0.5) (pow (* -2 (log u1)) 0.5)))) |
| 56.0ms | (* (pow (* (* -2 (log u1)) (* -2 (log u1))) 0.5) (pow (* -2 (log u1)) 0.5)) |
| 23.0ms | (* (* -2 (log u1)) (* -2 (log u1))) |
| 22.0ms | (cbrt (* (pow (* (* -2 (log u1)) (* -2 (log u1))) 0.5) (pow (* -2 (log u1)) 0.5))) |
| 1.9s | (* 1/6 (cbrt (* (pow (* (* -2 (log u1)) (* -2 (log u1))) 0.5) (pow (* -2 (log u1)) 0.5)))) |
| 1.8s | (cbrt (* (pow (* (* -2 (log u1)) (* -2 (log u1))) 0.5) (pow (* -2 (log u1)) 0.5))) |
| 1.5s | (* (pow (* (* -2 (log u1)) (* -2 (log u1))) 0.5) (pow (* -2 (log u1)) 0.5)) |
| 258.0ms | (* (* -2 (log u1)) (* -2 (log u1))) |
6 alts after pruning (5 fresh and 1 done)
Merged error: 0b
0% (0.3b remaining)
Error of 0.4b against oracle of 0.0b and baseline of 0.4b
| 2.5s | 8000× | body | 80 | valid |
| 375.0ms | 8000× | pre | 80 | true |