Time bar (total: 1.1m)
| 244.0ms | 93× | body | 1280 | valid |
| 154.0ms | 63× | body | 640 | valid |
| 67.0ms | 68× | body | 80 | valid |
| 34.0ms | 19× | body | 320 | valid |
| 10.0ms | 13× | body | 160 | valid |
| Iter | Nodes |
|---|---|
| done | 62 |
| 3 | 62 |
| 2 | 56 |
| 1 | 35 |
| 0 | 22 |
1 alts after pruning (1 fresh and 0 done)
Merged error: 0.1b
Found 4 expressions with local error:
| 0.2b | (* (sin theta) (sin delta)) |
| 0.3b | (* (sin phi1) (sin (asin (+ (* (sin phi1) (cos delta)) (* (* (cos phi1) (sin delta)) (cos theta)))))) |
| 0.3b | (asin (+ (* (sin phi1) (cos delta)) (* (* (cos phi1) (sin delta)) (cos theta)))) |
| 0.6b | (- (cos delta) (* (sin phi1) (sin (asin (+ (* (sin phi1) (cos delta)) (* (* (cos phi1) (sin delta)) (cos theta))))))) |
| 12× | add-sqr-sqrt |
| 8× | pow1 *-un-lft-identity add-cbrt-cube add-exp-log add-cube-cbrt |
| 6× | associate-*r* associate-*l* add-log-exp |
| 2× | pow-prod-down prod-exp *-commutative cbrt-unprod sin-mult unswap-sqr |
| 1× | asin-acos sub-neg flip3-- diff-log flip-- |
| 26.0ms | (* (sin theta) (sin delta)) |
| 21.0ms | (* (sin phi1) (sin (asin (+ (* (sin phi1) (cos delta)) (* (* (cos phi1) (sin delta)) (cos theta)))))) |
| 3.0ms | (asin (+ (* (sin phi1) (cos delta)) (* (* (cos phi1) (sin delta)) (cos theta)))) |
| 7.0ms | (- (cos delta) (* (sin phi1) (sin (asin (+ (* (sin phi1) (cos delta)) (* (* (cos phi1) (sin delta)) (cos theta))))))) |
| 60.0ms | (* (sin theta) (sin delta)) |
| 222.0ms | (* (sin phi1) (sin (asin (+ (* (sin phi1) (cos delta)) (* (* (cos phi1) (sin delta)) (cos theta)))))) |
| 10.0ms | (asin (+ (* (sin phi1) (cos delta)) (* (* (cos phi1) (sin delta)) (cos theta)))) |
| 261.0ms | (- (cos delta) (* (sin phi1) (sin (asin (+ (* (sin phi1) (cos delta)) (* (* (cos phi1) (sin delta)) (cos theta))))))) |
| Iter | Nodes |
|---|---|
| done | 5001 |
| 2 | 1120 |
| 1 | 312 |
| 0 | 144 |
9 alts after pruning (9 fresh and 0 done)
Merged error: 0.1b
Found 4 expressions with local error:
| 0.5b | (cbrt (* (* (- (cos delta) (* (sin phi1) (sin (asin (+ (* (sin phi1) (cos delta)) (* (* (cos phi1) (sin delta)) (cos theta))))))) (- (cos delta) (* (sin phi1) (sin (asin (+ (* (sin phi1) (cos delta)) (* (* (cos phi1) (sin delta)) (cos theta)))))))) (- (cos delta) (* (sin phi1) (sin (asin (+ (* (sin phi1) (cos delta)) (* (* (cos phi1) (sin delta)) (cos theta))))))))) |
| 0.6b | (- (cos delta) (* (sin phi1) (sin (asin (+ (* (sin phi1) (cos delta)) (* (* (cos phi1) (sin delta)) (cos theta))))))) |
| 0.6b | (- (cos delta) (* (sin phi1) (sin (asin (+ (* (sin phi1) (cos delta)) (* (* (cos phi1) (sin delta)) (cos theta))))))) |
| 0.6b | (- (cos delta) (* (sin phi1) (sin (asin (+ (* (sin phi1) (cos delta)) (* (* (cos phi1) (sin delta)) (cos theta))))))) |
| 30× | flip3-- flip-- |
| 28× | frac-times |
| 26× | cbrt-div |
| 14× | associate-*l/ |
| 10× | add-log-exp |
| 8× | associate-*r/ |
| 4× | add-sqr-sqrt pow1 *-un-lft-identity add-cbrt-cube add-exp-log add-cube-cbrt |
| 3× | sub-neg diff-log |
| 1× | cbrt-prod pow1/3 pow3 rem-cbrt-cube |
| 78.0ms | (cbrt (* (* (- (cos delta) (* (sin phi1) (sin (asin (+ (* (sin phi1) (cos delta)) (* (* (cos phi1) (sin delta)) (cos theta))))))) (- (cos delta) (* (sin phi1) (sin (asin (+ (* (sin phi1) (cos delta)) (* (* (cos phi1) (sin delta)) (cos theta)))))))) (- (cos delta) (* (sin phi1) (sin (asin (+ (* (sin phi1) (cos delta)) (* (* (cos phi1) (sin delta)) (cos theta))))))))) |
| 7.0ms | (- (cos delta) (* (sin phi1) (sin (asin (+ (* (sin phi1) (cos delta)) (* (* (cos phi1) (sin delta)) (cos theta))))))) |
| 5.0ms | (- (cos delta) (* (sin phi1) (sin (asin (+ (* (sin phi1) (cos delta)) (* (* (cos phi1) (sin delta)) (cos theta))))))) |
| 5.0ms | (- (cos delta) (* (sin phi1) (sin (asin (+ (* (sin phi1) (cos delta)) (* (* (cos phi1) (sin delta)) (cos theta))))))) |
| 261.0ms | (cbrt (* (* (- (cos delta) (* (sin phi1) (sin (asin (+ (* (sin phi1) (cos delta)) (* (* (cos phi1) (sin delta)) (cos theta))))))) (- (cos delta) (* (sin phi1) (sin (asin (+ (* (sin phi1) (cos delta)) (* (* (cos phi1) (sin delta)) (cos theta)))))))) (- (cos delta) (* (sin phi1) (sin (asin (+ (* (sin phi1) (cos delta)) (* (* (cos phi1) (sin delta)) (cos theta))))))))) |
| 285.0ms | (- (cos delta) (* (sin phi1) (sin (asin (+ (* (sin phi1) (cos delta)) (* (* (cos phi1) (sin delta)) (cos theta))))))) |
| 309.0ms | (- (cos delta) (* (sin phi1) (sin (asin (+ (* (sin phi1) (cos delta)) (* (* (cos phi1) (sin delta)) (cos theta))))))) |
| 274.0ms | (- (cos delta) (* (sin phi1) (sin (asin (+ (* (sin phi1) (cos delta)) (* (* (cos phi1) (sin delta)) (cos theta))))))) |
| Iter | Nodes |
|---|---|
| done | 5001 |
| 2 | 1356 |
| 1 | 351 |
| 0 | 153 |
10 alts after pruning (10 fresh and 0 done)
Merged error: 0.1b
Found 4 expressions with local error:
| 0.4b | (pow (* (sin phi1) (sin (asin (+ (* (sin phi1) (cos delta)) (* (* (cos phi1) (sin delta)) (cos theta)))))) 3) |
| 0.4b | (cbrt (* (+ (* (cos delta) (cos delta)) (+ (* (* (sin phi1) (sin (asin (+ (* (sin phi1) (cos delta)) (* (* (cos phi1) (sin delta)) (cos theta)))))) (* (sin phi1) (sin (asin (+ (* (sin phi1) (cos delta)) (* (* (cos phi1) (sin delta)) (cos theta))))))) (* (cos delta) (* (sin phi1) (sin (asin (+ (* (sin phi1) (cos delta)) (* (* (cos phi1) (sin delta)) (cos theta))))))))) (+ (* (cos delta) (cos delta)) (+ (* (* (sin phi1) (sin (asin (+ (* (sin phi1) (cos delta)) (* (* (cos phi1) (sin delta)) (cos theta)))))) (* (sin phi1) (sin (asin (+ (* (sin phi1) (cos delta)) (* (* (cos phi1) (sin delta)) (cos theta))))))) (* (cos delta) (* (sin phi1) (sin (asin (+ (* (sin phi1) (cos delta)) (* (* (cos phi1) (sin delta)) (cos theta))))))))))) |
| 0.5b | (cbrt (* (* (- (cos delta) (* (sin phi1) (sin (asin (+ (* (sin phi1) (cos delta)) (* (* (cos phi1) (sin delta)) (cos theta))))))) (- (pow (cos delta) 3) (pow (* (sin phi1) (sin (asin (+ (* (sin phi1) (cos delta)) (* (* (cos phi1) (sin delta)) (cos theta)))))) 3))) (- (pow (cos delta) 3) (pow (* (sin phi1) (sin (asin (+ (* (sin phi1) (cos delta)) (* (* (cos phi1) (sin delta)) (cos theta)))))) 3)))) |
| 0.6b | (- (cos delta) (* (sin phi1) (sin (asin (+ (* (sin phi1) (cos delta)) (* (* (cos phi1) (sin delta)) (cos theta))))))) |
| 128× | frac-add |
| 113× | sin-mult |
| 93× | frac-times |
| 89× | cbrt-div |
| 80× | cos-mult |
| 79× | associate-*r/ |
| 37× | associate-*l/ |
| 32× | flip3-+ flip-+ |
| 28× | flip3-- flip-- |
| 7× | pow1 add-cbrt-cube add-exp-log |
| 6× | add-log-exp |
| 5× | add-sqr-sqrt *-un-lft-identity add-cube-cbrt |
| 3× | pow-unpow |
| 2× | cbrt-prod pow-pow pow1/3 pow-exp rem-cube-cbrt |
| 1× | cube-div cube-mult pow-to-exp sub-neg unpow-prod-down diff-log unpow3 cube-prod pow-prod-down prod-exp cbrt-unprod sqr-pow |
| 16.0ms | (pow (* (sin phi1) (sin (asin (+ (* (sin phi1) (cos delta)) (* (* (cos phi1) (sin delta)) (cos theta)))))) 3) |
| 296.0ms | (cbrt (* (+ (* (cos delta) (cos delta)) (+ (* (* (sin phi1) (sin (asin (+ (* (sin phi1) (cos delta)) (* (* (cos phi1) (sin delta)) (cos theta)))))) (* (sin phi1) (sin (asin (+ (* (sin phi1) (cos delta)) (* (* (cos phi1) (sin delta)) (cos theta))))))) (* (cos delta) (* (sin phi1) (sin (asin (+ (* (sin phi1) (cos delta)) (* (* (cos phi1) (sin delta)) (cos theta))))))))) (+ (* (cos delta) (cos delta)) (+ (* (* (sin phi1) (sin (asin (+ (* (sin phi1) (cos delta)) (* (* (cos phi1) (sin delta)) (cos theta)))))) (* (sin phi1) (sin (asin (+ (* (sin phi1) (cos delta)) (* (* (cos phi1) (sin delta)) (cos theta))))))) (* (cos delta) (* (sin phi1) (sin (asin (+ (* (sin phi1) (cos delta)) (* (* (cos phi1) (sin delta)) (cos theta))))))))))) |
| 104.0ms | (cbrt (* (* (- (cos delta) (* (sin phi1) (sin (asin (+ (* (sin phi1) (cos delta)) (* (* (cos phi1) (sin delta)) (cos theta))))))) (- (pow (cos delta) 3) (pow (* (sin phi1) (sin (asin (+ (* (sin phi1) (cos delta)) (* (* (cos phi1) (sin delta)) (cos theta)))))) 3))) (- (pow (cos delta) 3) (pow (* (sin phi1) (sin (asin (+ (* (sin phi1) (cos delta)) (* (* (cos phi1) (sin delta)) (cos theta)))))) 3)))) |
| 5.0ms | (- (cos delta) (* (sin phi1) (sin (asin (+ (* (sin phi1) (cos delta)) (* (* (cos phi1) (sin delta)) (cos theta))))))) |
| 439.0ms | (pow (* (sin phi1) (sin (asin (+ (* (sin phi1) (cos delta)) (* (* (cos phi1) (sin delta)) (cos theta)))))) 3) |
| 2.1s | (cbrt (* (+ (* (cos delta) (cos delta)) (+ (* (* (sin phi1) (sin (asin (+ (* (sin phi1) (cos delta)) (* (* (cos phi1) (sin delta)) (cos theta)))))) (* (sin phi1) (sin (asin (+ (* (sin phi1) (cos delta)) (* (* (cos phi1) (sin delta)) (cos theta))))))) (* (cos delta) (* (sin phi1) (sin (asin (+ (* (sin phi1) (cos delta)) (* (* (cos phi1) (sin delta)) (cos theta))))))))) (+ (* (cos delta) (cos delta)) (+ (* (* (sin phi1) (sin (asin (+ (* (sin phi1) (cos delta)) (* (* (cos phi1) (sin delta)) (cos theta)))))) (* (sin phi1) (sin (asin (+ (* (sin phi1) (cos delta)) (* (* (cos phi1) (sin delta)) (cos theta))))))) (* (cos delta) (* (sin phi1) (sin (asin (+ (* (sin phi1) (cos delta)) (* (* (cos phi1) (sin delta)) (cos theta))))))))))) |
| 3.8s | (cbrt (* (* (- (cos delta) (* (sin phi1) (sin (asin (+ (* (sin phi1) (cos delta)) (* (* (cos phi1) (sin delta)) (cos theta))))))) (- (pow (cos delta) 3) (pow (* (sin phi1) (sin (asin (+ (* (sin phi1) (cos delta)) (* (* (cos phi1) (sin delta)) (cos theta)))))) 3))) (- (pow (cos delta) 3) (pow (* (sin phi1) (sin (asin (+ (* (sin phi1) (cos delta)) (* (* (cos phi1) (sin delta)) (cos theta)))))) 3)))) |
| 245.0ms | (- (cos delta) (* (sin phi1) (sin (asin (+ (* (sin phi1) (cos delta)) (* (* (cos phi1) (sin delta)) (cos theta))))))) |
| Iter | Nodes |
|---|---|
| done | 5000 |
| 1 | 1951 |
| 0 | 617 |
10 alts after pruning (9 fresh and 1 done)
Merged error: 0.0b
Found 4 expressions with local error:
| 0.4b | (cbrt (* (+ (* (cos delta) (cos delta)) (+ (* (* (sin phi1) (sin (asin (+ (* (sin phi1) (cos delta)) (* (* (cos phi1) (sin delta)) (cos theta)))))) (* (sin phi1) (sin (asin (+ (* (sin phi1) (cos delta)) (* (* (cos phi1) (sin delta)) (cos theta))))))) (* (cos delta) (* (sin phi1) (sin (asin (+ (* (sin phi1) (cos delta)) (* (* (cos phi1) (sin delta)) (cos theta))))))))) (+ (* (cos delta) (cos delta)) (+ (* (* (sin phi1) (sin (asin (+ (* (sin phi1) (cos delta)) (* (* (cos phi1) (sin delta)) (cos theta)))))) (* (sin phi1) (sin (asin (+ (* (sin phi1) (cos delta)) (* (* (cos phi1) (sin delta)) (cos theta))))))) (* (cos delta) (* (sin phi1) (sin (asin (+ (* (sin phi1) (cos delta)) (* (* (cos phi1) (sin delta)) (cos theta))))))))))) |
| 0.5b | (cbrt (* (* (log (exp (- (cos delta) (* (sin phi1) (sin (asin (+ (* (sin phi1) (cos delta)) (* (* (cos phi1) (sin delta)) (cos theta))))))))) (- (pow (cos delta) 3) (pow (* (sin phi1) (sin (asin (+ (* (sin phi1) (cos delta)) (* (* (cos phi1) (sin delta)) (cos theta)))))) 3))) (- (pow (cos delta) 3) (pow (* (sin phi1) (sin (asin (+ (* (sin phi1) (cos delta)) (* (* (cos phi1) (sin delta)) (cos theta)))))) 3)))) |
| 0.6b | (- (cos delta) (* (sin phi1) (sin (asin (+ (* (sin phi1) (cos delta)) (* (* (cos phi1) (sin delta)) (cos theta))))))) |
| 0.9b | (log (exp (- (cos delta) (* (sin phi1) (sin (asin (+ (* (sin phi1) (cos delta)) (* (* (cos phi1) (sin delta)) (cos theta))))))))) |
| 128× | frac-add |
| 112× | sin-mult |
| 80× | cos-mult |
| 79× | associate-*r/ |
| 71× | cbrt-div |
| 69× | frac-times |
| 32× | flip3-+ flip-+ |
| 25× | associate-*l/ |
| 7× | flip3-- flip-- |
| 6× | add-sqr-sqrt *-un-lft-identity add-cube-cbrt add-log-exp |
| 5× | pow1 log-prod |
| 4× | add-cbrt-cube add-exp-log log-pow |
| 3× | exp-prod |
| 2× | cbrt-prod sub-neg pow1/3 exp-sum |
| 1× | log-div exp-diff diff-log rem-log-exp |
| 254.0ms | (cbrt (* (+ (* (cos delta) (cos delta)) (+ (* (* (sin phi1) (sin (asin (+ (* (sin phi1) (cos delta)) (* (* (cos phi1) (sin delta)) (cos theta)))))) (* (sin phi1) (sin (asin (+ (* (sin phi1) (cos delta)) (* (* (cos phi1) (sin delta)) (cos theta))))))) (* (cos delta) (* (sin phi1) (sin (asin (+ (* (sin phi1) (cos delta)) (* (* (cos phi1) (sin delta)) (cos theta))))))))) (+ (* (cos delta) (cos delta)) (+ (* (* (sin phi1) (sin (asin (+ (* (sin phi1) (cos delta)) (* (* (cos phi1) (sin delta)) (cos theta)))))) (* (sin phi1) (sin (asin (+ (* (sin phi1) (cos delta)) (* (* (cos phi1) (sin delta)) (cos theta))))))) (* (cos delta) (* (sin phi1) (sin (asin (+ (* (sin phi1) (cos delta)) (* (* (cos phi1) (sin delta)) (cos theta))))))))))) |
| 132.0ms | (cbrt (* (* (log (exp (- (cos delta) (* (sin phi1) (sin (asin (+ (* (sin phi1) (cos delta)) (* (* (cos phi1) (sin delta)) (cos theta))))))))) (- (pow (cos delta) 3) (pow (* (sin phi1) (sin (asin (+ (* (sin phi1) (cos delta)) (* (* (cos phi1) (sin delta)) (cos theta)))))) 3))) (- (pow (cos delta) 3) (pow (* (sin phi1) (sin (asin (+ (* (sin phi1) (cos delta)) (* (* (cos phi1) (sin delta)) (cos theta)))))) 3)))) |
| 10.0ms | (- (cos delta) (* (sin phi1) (sin (asin (+ (* (sin phi1) (cos delta)) (* (* (cos phi1) (sin delta)) (cos theta))))))) |
| 15.0ms | (log (exp (- (cos delta) (* (sin phi1) (sin (asin (+ (* (sin phi1) (cos delta)) (* (* (cos phi1) (sin delta)) (cos theta))))))))) |
| 2.1s | (cbrt (* (+ (* (cos delta) (cos delta)) (+ (* (* (sin phi1) (sin (asin (+ (* (sin phi1) (cos delta)) (* (* (cos phi1) (sin delta)) (cos theta)))))) (* (sin phi1) (sin (asin (+ (* (sin phi1) (cos delta)) (* (* (cos phi1) (sin delta)) (cos theta))))))) (* (cos delta) (* (sin phi1) (sin (asin (+ (* (sin phi1) (cos delta)) (* (* (cos phi1) (sin delta)) (cos theta))))))))) (+ (* (cos delta) (cos delta)) (+ (* (* (sin phi1) (sin (asin (+ (* (sin phi1) (cos delta)) (* (* (cos phi1) (sin delta)) (cos theta)))))) (* (sin phi1) (sin (asin (+ (* (sin phi1) (cos delta)) (* (* (cos phi1) (sin delta)) (cos theta))))))) (* (cos delta) (* (sin phi1) (sin (asin (+ (* (sin phi1) (cos delta)) (* (* (cos phi1) (sin delta)) (cos theta))))))))))) |
| 4.1s | (cbrt (* (* (log (exp (- (cos delta) (* (sin phi1) (sin (asin (+ (* (sin phi1) (cos delta)) (* (* (cos phi1) (sin delta)) (cos theta))))))))) (- (pow (cos delta) 3) (pow (* (sin phi1) (sin (asin (+ (* (sin phi1) (cos delta)) (* (* (cos phi1) (sin delta)) (cos theta)))))) 3))) (- (pow (cos delta) 3) (pow (* (sin phi1) (sin (asin (+ (* (sin phi1) (cos delta)) (* (* (cos phi1) (sin delta)) (cos theta)))))) 3)))) |
| 278.0ms | (- (cos delta) (* (sin phi1) (sin (asin (+ (* (sin phi1) (cos delta)) (* (* (cos phi1) (sin delta)) (cos theta))))))) |
| 275.0ms | (log (exp (- (cos delta) (* (sin phi1) (sin (asin (+ (* (sin phi1) (cos delta)) (* (* (cos phi1) (sin delta)) (cos theta))))))))) |
| Iter | Nodes |
|---|---|
| done | 5000 |
| 1 | 1642 |
| 0 | 534 |
10 alts after pruning (9 fresh and 1 done)
Merged error: 0.0b
0% (0.1b remaining)
Error of 0.2b against oracle of 0.1b and baseline of 0.2b
| Iter | Nodes |
|---|---|
| done | 52 |
| 1 | 52 |
| 0 | 39 |
| 10.4s | 3026× | body | 1280 | valid |
| 4.5s | 1898× | body | 640 | valid |
| 899.0ms | 752× | body | 320 | valid |
| 635.0ms | 2001× | body | 80 | valid |
| 197.0ms | 323× | body | 160 | valid |