Time bar (total: 51.1s)
| 421.0ms | 93× | body | 1280 | valid |
| 263.0ms | 69× | body | 640 | valid |
| 47.0ms | 63× | body | 80 | valid |
| 38.0ms | 20× | body | 320 | valid |
| 13.0ms | 11× | body | 160 | valid |
| Iter | Nodes |
|---|---|
| done | 55 |
| 3 | 55 |
| 2 | 54 |
| 1 | 35 |
| 0 | 22 |
1 alts after pruning (1 fresh and 0 done)
Merged error: 0.2b
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.4b | (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 |
| 4× | insert-posit16 |
| 2× | pow-prod-down prod-exp *-commutative cbrt-unprod sin-mult unswap-sqr |
| 1× | asin-acos sub-neg flip3-- diff-log flip-- |
| 28.0ms | (* (sin theta) (sin delta)) |
| 22.0ms | (* (sin phi1) (sin (asin (+ (* (sin phi1) (cos delta)) (* (* (cos phi1) (sin delta)) (cos theta)))))) |
| 2.0ms | (asin (+ (* (sin phi1) (cos delta)) (* (* (cos phi1) (sin delta)) (cos theta)))) |
| 6.0ms | (- (cos delta) (* (sin phi1) (sin (asin (+ (* (sin phi1) (cos delta)) (* (* (cos phi1) (sin delta)) (cos theta))))))) |
| 65.0ms | (* (sin theta) (sin delta)) |
| 219.0ms | (* (sin phi1) (sin (asin (+ (* (sin phi1) (cos delta)) (* (* (cos phi1) (sin delta)) (cos theta)))))) |
| 8.0ms | (asin (+ (* (sin phi1) (cos delta)) (* (* (cos phi1) (sin delta)) (cos theta)))) |
| 621.0ms | (- (cos delta) (* (sin phi1) (sin (asin (+ (* (sin phi1) (cos delta)) (* (* (cos phi1) (sin delta)) (cos theta))))))) |
| Iter | Nodes |
|---|---|
| done | 5000 |
| 3 | 2232 |
| 2 | 734 |
| 1 | 317 |
| 0 | 148 |
11 alts after pruning (11 fresh and 0 done)
Merged error: 0.1b
Found 4 expressions with local error:
| 0.4b | (asin (+ (* (sin phi1) (cos delta)) (* (* (cos phi1) (sin delta)) (cos theta)))) |
| 0.4b | (asin (+ (* (sin phi1) (cos delta)) (* (* (cos phi1) (sin delta)) (cos theta)))) |
| 0.6b | (- (cos delta) (cbrt (* (* (* (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))))))) (* (sin phi1) (sin (asin (+ (* (sin phi1) (cos delta)) (* (* (cos phi1) (sin delta)) (cos theta))))))))) |
| 19.1b | (cbrt (* (* (* (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))))))) (* (sin phi1) (sin (asin (+ (* (sin phi1) (cos delta)) (* (* (cos phi1) (sin delta)) (cos theta)))))))) |
| 12× | sin-mult |
| 7× | cbrt-div |
| 6× | add-sqr-sqrt *-un-lft-identity add-log-exp |
| 5× | frac-times associate-*l/ |
| 4× | pow1 add-cbrt-cube add-exp-log add-cube-cbrt insert-posit16 |
| 3× | associate-*r/ |
| 2× | asin-acos |
| 1× | cbrt-prod sub-neg flip3-- pow1/3 diff-log pow3 rem-cbrt-cube flip-- distribute-lft-out-- difference-of-squares |
| 4.0ms | (asin (+ (* (sin phi1) (cos delta)) (* (* (cos phi1) (sin delta)) (cos theta)))) |
| 4.0ms | (asin (+ (* (sin phi1) (cos delta)) (* (* (cos phi1) (sin delta)) (cos theta)))) |
| 13.0ms | (- (cos delta) (cbrt (* (* (* (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))))))) (* (sin phi1) (sin (asin (+ (* (sin phi1) (cos delta)) (* (* (cos phi1) (sin delta)) (cos theta))))))))) |
| 153.0ms | (cbrt (* (* (* (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))))))) (* (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)))) |
| 7.0ms | (asin (+ (* (sin phi1) (cos delta)) (* (* (cos phi1) (sin delta)) (cos theta)))) |
| 267.0ms | (- (cos delta) (cbrt (* (* (* (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))))))) (* (sin phi1) (sin (asin (+ (* (sin phi1) (cos delta)) (* (* (cos phi1) (sin delta)) (cos theta))))))))) |
| 238.0ms | (cbrt (* (* (* (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))))))) (* (sin phi1) (sin (asin (+ (* (sin phi1) (cos delta)) (* (* (cos phi1) (sin delta)) (cos theta)))))))) |
| Iter | Nodes |
|---|---|
| done | 5001 |
| 4 | 4459 |
| 3 | 1657 |
| 2 | 540 |
| 1 | 245 |
| 0 | 124 |
12 alts after pruning (12 fresh and 0 done)
Merged error: 0.0b
Found 4 expressions with local error:
| 0.4b | (asin (+ (* (sin phi1) (cos delta)) (* (* (cos phi1) (sin delta)) (cos theta)))) |
| 0.6b | (- (cos delta) (log (exp (cbrt (* (* (* (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))))))) (* (sin phi1) (sin (asin (+ (* (sin phi1) (cos delta)) (* (* (cos phi1) (sin delta)) (cos theta))))))))))) |
| 2.6b | (log (exp (cbrt (* (* (* (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))))))) (* (sin phi1) (sin (asin (+ (* (sin phi1) (cos delta)) (* (* (cos phi1) (sin delta)) (cos theta)))))))))) |
| 19.1b | (cbrt (* (* (* (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))))))) (* (sin phi1) (sin (asin (+ (* (sin phi1) (cos delta)) (* (* (cos phi1) (sin delta)) (cos theta)))))))) |
| 12× | sin-mult |
| 10× | *-un-lft-identity |
| 9× | add-sqr-sqrt |
| 7× | cbrt-div add-cube-cbrt |
| 6× | pow1 log-prod log-pow |
| 5× | frac-times associate-*l/ add-log-exp |
| 4× | exp-prod add-cbrt-cube add-exp-log insert-posit16 |
| 3× | associate-*r/ associate--r+ |
| 2× | cbrt-prod distribute-lft-out-- |
| 1× | asin-acos sub-neg flip3-- pow1/3 diff-log rem-log-exp pow3 rem-cbrt-cube flip-- difference-of-squares |
| 2.0ms | (asin (+ (* (sin phi1) (cos delta)) (* (* (cos phi1) (sin delta)) (cos theta)))) |
| 9.0ms | (- (cos delta) (log (exp (cbrt (* (* (* (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))))))) (* (sin phi1) (sin (asin (+ (* (sin phi1) (cos delta)) (* (* (cos phi1) (sin delta)) (cos theta))))))))))) |
| 2.0ms | (log (exp (cbrt (* (* (* (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))))))) (* (sin phi1) (sin (asin (+ (* (sin phi1) (cos delta)) (* (* (cos phi1) (sin delta)) (cos theta)))))))))) |
| 150.0ms | (cbrt (* (* (* (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))))))) (* (sin phi1) (sin (asin (+ (* (sin phi1) (cos delta)) (* (* (cos phi1) (sin delta)) (cos theta)))))))) |
| 7.0ms | (asin (+ (* (sin phi1) (cos delta)) (* (* (cos phi1) (sin delta)) (cos theta)))) |
| 260.0ms | (- (cos delta) (log (exp (cbrt (* (* (* (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))))))) (* (sin phi1) (sin (asin (+ (* (sin phi1) (cos delta)) (* (* (cos phi1) (sin delta)) (cos theta))))))))))) |
| 254.0ms | (log (exp (cbrt (* (* (* (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))))))) (* (sin phi1) (sin (asin (+ (* (sin phi1) (cos delta)) (* (* (cos phi1) (sin delta)) (cos theta)))))))))) |
| 220.0ms | (cbrt (* (* (* (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))))))) (* (sin phi1) (sin (asin (+ (* (sin phi1) (cos delta)) (* (* (cos phi1) (sin delta)) (cos theta)))))))) |
| Iter | Nodes |
|---|---|
| done | 5000 |
| 3 | 1912 |
| 2 | 634 |
| 1 | 287 |
| 0 | 151 |
12 alts after pruning (11 fresh and 1 done)
Merged error: 0.0b
Found 4 expressions with local error:
| 0.4b | (- (* (cos delta) (cos delta)) (* (cbrt (* (* (* (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))))))) (* (sin phi1) (sin (asin (+ (* (sin phi1) (cos delta)) (* (* (cos phi1) (sin delta)) (cos theta)))))))) (cbrt (* (* (* (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))))))) (* (sin phi1) (sin (asin (+ (* (sin phi1) (cos delta)) (* (* (cos phi1) (sin delta)) (cos theta)))))))))) |
| 19.1b | (cbrt (* (* (* (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))))))) (* (sin phi1) (sin (asin (+ (* (sin phi1) (cos delta)) (* (* (cos phi1) (sin delta)) (cos theta)))))))) |
| 19.1b | (cbrt (* (* (* (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))))))) (* (sin phi1) (sin (asin (+ (* (sin phi1) (cos delta)) (* (* (cos phi1) (sin delta)) (cos theta)))))))) |
| 19.1b | (cbrt (* (* (* (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))))))) (* (sin phi1) (sin (asin (+ (* (sin phi1) (cos delta)) (* (* (cos phi1) (sin delta)) (cos theta)))))))) |
| 228× | sin-mult |
| 144× | frac-times |
| 133× | cbrt-div |
| 102× | associate-*l/ |
| 64× | associate-*r/ |
| 63× | cos-mult frac-sub |
| 6× | add-log-exp |
| 4× | add-sqr-sqrt pow1 *-un-lft-identity add-cbrt-cube add-exp-log add-cube-cbrt insert-posit16 |
| 3× | cbrt-prod pow1/3 pow3 rem-cbrt-cube |
| 1× | sqr-cos sub-neg flip3-- diff-log associate--l+ flip-- difference-of-squares |
| 764.0ms | (- (* (cos delta) (cos delta)) (* (cbrt (* (* (* (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))))))) (* (sin phi1) (sin (asin (+ (* (sin phi1) (cos delta)) (* (* (cos phi1) (sin delta)) (cos theta)))))))) (cbrt (* (* (* (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))))))) (* (sin phi1) (sin (asin (+ (* (sin phi1) (cos delta)) (* (* (cos phi1) (sin delta)) (cos theta)))))))))) |
| 165.0ms | (cbrt (* (* (* (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))))))) (* (sin phi1) (sin (asin (+ (* (sin phi1) (cos delta)) (* (* (cos phi1) (sin delta)) (cos theta)))))))) |
| 173.0ms | (cbrt (* (* (* (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))))))) (* (sin phi1) (sin (asin (+ (* (sin phi1) (cos delta)) (* (* (cos phi1) (sin delta)) (cos theta)))))))) |
| 170.0ms | (cbrt (* (* (* (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))))))) (* (sin phi1) (sin (asin (+ (* (sin phi1) (cos delta)) (* (* (cos phi1) (sin delta)) (cos theta)))))))) |
| 916.0ms | (- (* (cos delta) (cos delta)) (* (cbrt (* (* (* (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))))))) (* (sin phi1) (sin (asin (+ (* (sin phi1) (cos delta)) (* (* (cos phi1) (sin delta)) (cos theta)))))))) (cbrt (* (* (* (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))))))) (* (sin phi1) (sin (asin (+ (* (sin phi1) (cos delta)) (* (* (cos phi1) (sin delta)) (cos theta)))))))))) |
| 251.0ms | (cbrt (* (* (* (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))))))) (* (sin phi1) (sin (asin (+ (* (sin phi1) (cos delta)) (* (* (cos phi1) (sin delta)) (cos theta)))))))) |
| 257.0ms | (cbrt (* (* (* (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))))))) (* (sin phi1) (sin (asin (+ (* (sin phi1) (cos delta)) (* (* (cos phi1) (sin delta)) (cos theta)))))))) |
| 284.0ms | (cbrt (* (* (* (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))))))) (* (sin phi1) (sin (asin (+ (* (sin phi1) (cos delta)) (* (* (cos phi1) (sin delta)) (cos theta)))))))) |
| Iter | Nodes |
|---|---|
| done | 5006 |
| 2 | 2302 |
| 1 | 862 |
| 0 | 367 |
11 alts after pruning (11 fresh and 0 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 | 40 |
| 1 | 40 |
| 0 | 29 |
| 14.6s | 3105× | body | 1280 | valid |
| 5.9s | 1828× | body | 640 | valid |
| 1.4s | 2024× | body | 80 | valid |
| 1.3s | 709× | body | 320 | valid |
| 699.0ms | 334× | body | 160 | valid |