Time bar (total: 37.5s)
| 327.0ms | 161× | body | 1280 | valid |
| 116.0ms | 69× | body | 640 | valid |
| 11.0ms | 16× | body | 320 | valid |
| 4.0ms | 8× | body | 160 | valid |
| 1.0ms | 2× | body | 80 | valid |
| Iter | Nodes |
|---|---|
| done | 34 |
| 3 | 34 |
| 2 | 33 |
| 1 | 26 |
| 0 | 17 |
1 alts after pruning (1 fresh and 0 done)
Merged error: 18.4b
Found 4 expressions with local error:
| 0.2b | (* (* (cos phi1) (cos phi2)) (cos (- lambda1 lambda2))) |
| 0.2b | (* (acos (+ (* (sin phi1) (sin phi2)) (* (* (cos phi1) (cos phi2)) (cos (- lambda1 lambda2))))) R) |
| 1.1b | (acos (+ (* (sin phi1) (sin phi2)) (* (* (cos phi1) (cos phi2)) (cos (- lambda1 lambda2))))) |
| 2.7b | (cos (- lambda1 lambda2)) |
| 11× | pow1 add-cbrt-cube add-exp-log |
| 9× | add-sqr-sqrt |
| 7× | *-un-lft-identity add-cube-cbrt |
| 6× | associate-*r* |
| 4× | associate-*l* pow-prod-down prod-exp cbrt-unprod insert-posit16 add-log-exp |
| 3× | cos-diff |
| 2× | cos-sum *-commutative |
| 1× | distribute-rgt-in acos-asin sub-neg distribute-lft-in associate-*l/ cos-mult unswap-sqr |
| 54.0ms | (* (* (cos phi1) (cos phi2)) (cos (- lambda1 lambda2))) |
| 12.0ms | (* (acos (+ (* (sin phi1) (sin phi2)) (* (* (cos phi1) (cos phi2)) (cos (- lambda1 lambda2))))) R) |
| 4.0ms | (acos (+ (* (sin phi1) (sin phi2)) (* (* (cos phi1) (cos phi2)) (cos (- lambda1 lambda2))))) |
| 10.0ms | (cos (- lambda1 lambda2)) |
| 161.0ms | (* (* (cos phi1) (cos phi2)) (cos (- lambda1 lambda2))) |
| 77.0ms | (* (acos (+ (* (sin phi1) (sin phi2)) (* (* (cos phi1) (cos phi2)) (cos (- lambda1 lambda2))))) R) |
| 20.0ms | (acos (+ (* (sin phi1) (sin phi2)) (* (* (cos phi1) (cos phi2)) (cos (- lambda1 lambda2))))) |
| 57.0ms | (cos (- lambda1 lambda2)) |
| Iter | Nodes |
|---|---|
| done | 5000 |
| 3 | 2771 |
| 2 | 737 |
| 1 | 278 |
| 0 | 125 |
13 alts after pruning (13 fresh and 0 done)
Merged error: 3.7b
Found 4 expressions with local error:
| 0.2b | (* (* (cos phi1) (cos phi2)) (+ (* (cos lambda1) (cos lambda2)) (* (sin lambda1) (sin lambda2)))) |
| 0.2b | (* (acos (+ (* (sin phi1) (sin phi2)) (* (* (cos phi1) (cos phi2)) (+ (* (cos lambda1) (cos lambda2)) (* (sin lambda1) (sin lambda2)))))) R) |
| 0.2b | (* (sin lambda1) (sin lambda2)) |
| 1.0b | (acos (+ (* (sin phi1) (sin phi2)) (* (* (cos phi1) (cos phi2)) (+ (* (cos lambda1) (cos lambda2)) (* (sin lambda1) (sin lambda2)))))) |
| 13× | add-sqr-sqrt pow1 add-cbrt-cube add-exp-log |
| 9× | *-un-lft-identity associate-*r* add-cube-cbrt |
| 7× | associate-*l* |
| 6× | cos-mult |
| 5× | pow-prod-down prod-exp cbrt-unprod |
| 4× | insert-posit16 add-log-exp |
| 3× | frac-times associate-*r/ *-commutative sin-mult |
| 2× | flip3-+ frac-add flip-+ unswap-sqr |
| 1× | distribute-rgt-in acos-asin distribute-lft-in associate-*l/ |
| 107.0ms | (* (* (cos phi1) (cos phi2)) (+ (* (cos lambda1) (cos lambda2)) (* (sin lambda1) (sin lambda2)))) |
| 11.0ms | (* (acos (+ (* (sin phi1) (sin phi2)) (* (* (cos phi1) (cos phi2)) (+ (* (cos lambda1) (cos lambda2)) (* (sin lambda1) (sin lambda2)))))) R) |
| 31.0ms | (* (sin lambda1) (sin lambda2)) |
| 2.0ms | (acos (+ (* (sin phi1) (sin phi2)) (* (* (cos phi1) (cos phi2)) (+ (* (cos lambda1) (cos lambda2)) (* (sin lambda1) (sin lambda2)))))) |
| 387.0ms | (* (* (cos phi1) (cos phi2)) (+ (* (cos lambda1) (cos lambda2)) (* (sin lambda1) (sin lambda2)))) |
| 119.0ms | (* (acos (+ (* (sin phi1) (sin phi2)) (* (* (cos phi1) (cos phi2)) (+ (* (cos lambda1) (cos lambda2)) (* (sin lambda1) (sin lambda2)))))) R) |
| 64.0ms | (* (sin lambda1) (sin lambda2)) |
| 29.0ms | (acos (+ (* (sin phi1) (sin phi2)) (* (* (cos phi1) (cos phi2)) (+ (* (cos lambda1) (cos lambda2)) (* (sin lambda1) (sin lambda2)))))) |
| Iter | Nodes |
|---|---|
| done | 5005 |
| 2 | 1879 |
| 1 | 506 |
| 0 | 185 |
16 alts after pruning (16 fresh and 0 done)
Merged error: 3.6b
Found 4 expressions with local error:
| 0.2b | (* (sin lambda1) (sin lambda2)) |
| 0.4b | (exp (acos (+ (* (sin phi1) (sin phi2)) (* (* (cos phi1) (cos phi2)) (+ (* (cos lambda1) (cos lambda2)) (* (sin lambda1) (sin lambda2))))))) |
| 0.9b | (log (exp (acos (+ (* (sin phi1) (sin phi2)) (* (* (cos phi1) (cos phi2)) (+ (* (cos lambda1) (cos lambda2)) (* (sin lambda1) (sin lambda2)))))))) |
| 1.0b | (acos (+ (* (sin phi1) (sin phi2)) (* (* (cos phi1) (cos phi2)) (+ (* (cos lambda1) (cos lambda2)) (* (sin lambda1) (sin lambda2)))))) |
| 11× | add-sqr-sqrt |
| 9× | *-un-lft-identity add-cube-cbrt |
| 7× | pow1 |
| 6× | exp-prod add-cbrt-cube add-exp-log |
| 5× | add-log-exp |
| 4× | log-pow insert-posit16 |
| 3× | acos-asin log-prod associate-*r* associate-*l* |
| 2× | exp-diff |
| 1× | log-div rem-log-exp pow-prod-down prod-exp *-commutative cbrt-unprod sin-mult unswap-sqr rem-exp-log |
| 12.0ms | (* (sin lambda1) (sin lambda2)) |
| 3.0ms | (exp (acos (+ (* (sin phi1) (sin phi2)) (* (* (cos phi1) (cos phi2)) (+ (* (cos lambda1) (cos lambda2)) (* (sin lambda1) (sin lambda2))))))) |
| 8.0ms | (log (exp (acos (+ (* (sin phi1) (sin phi2)) (* (* (cos phi1) (cos phi2)) (+ (* (cos lambda1) (cos lambda2)) (* (sin lambda1) (sin lambda2)))))))) |
| 4.0ms | (acos (+ (* (sin phi1) (sin phi2)) (* (* (cos phi1) (cos phi2)) (+ (* (cos lambda1) (cos lambda2)) (* (sin lambda1) (sin lambda2)))))) |
| 56.0ms | (* (sin lambda1) (sin lambda2)) |
| 56.0ms | (exp (acos (+ (* (sin phi1) (sin phi2)) (* (* (cos phi1) (cos phi2)) (+ (* (cos lambda1) (cos lambda2)) (* (sin lambda1) (sin lambda2))))))) |
| 29.0ms | (log (exp (acos (+ (* (sin phi1) (sin phi2)) (* (* (cos phi1) (cos phi2)) (+ (* (cos lambda1) (cos lambda2)) (* (sin lambda1) (sin lambda2)))))))) |
| 21.0ms | (acos (+ (* (sin phi1) (sin phi2)) (* (* (cos phi1) (cos phi2)) (+ (* (cos lambda1) (cos lambda2)) (* (sin lambda1) (sin lambda2)))))) |
| Iter | Nodes |
|---|---|
| done | 5002 |
| 6 | 4482 |
| 5 | 2671 |
| 4 | 1591 |
| 3 | 869 |
| 2 | 393 |
| 1 | 203 |
| 0 | 111 |
20 alts after pruning (20 fresh and 0 done)
Merged error: 3.5b
Found 4 expressions with local error:
| 0.3b | (* (* (cos lambda1) (cos lambda2)) (* (sin lambda1) (sin lambda2))) |
| 0.3b | (* (* (cos lambda1) (cos lambda2)) (* (cos lambda1) (cos lambda2))) |
| 0.3b | (* (* (cos lambda1) (cos lambda2)) (* (cos lambda1) (cos lambda2))) |
| 1.0b | (acos (+ (* (sin phi1) (sin phi2)) (/ (* (* (cos phi1) (cos phi2)) (+ (* (* (* (cos lambda1) (cos lambda2)) (* (cos lambda1) (cos lambda2))) (* (cos lambda1) (cos lambda2))) (* (* (sin lambda1) (sin lambda2)) (* (* (sin lambda1) (sin lambda2)) (* (sin lambda1) (sin lambda2)))))) (+ (* (* (cos lambda1) (cos lambda2)) (* (cos lambda1) (cos lambda2))) (- (* (* (sin lambda1) (sin lambda2)) (* (sin lambda1) (sin lambda2))) (* (* (cos lambda1) (cos lambda2)) (* (sin lambda1) (sin lambda2)))))))) |
| 94× | pow1 |
| 42× | pow-prod-down |
| 40× | add-cbrt-cube add-exp-log |
| 24× | prod-exp cbrt-unprod |
| 10× | cos-mult |
| 8× | pow-sqr pow-prod-up |
| 4× | add-sqr-sqrt *-un-lft-identity pow-plus add-cube-cbrt insert-posit16 add-log-exp |
| 3× | frac-times associate-*r* associate-*l* associate-*l/ associate-*r/ *-commutative |
| 2× | pow2 swap-sqr sin-mult |
| 1× | acos-asin |
| 71.0ms | (* (* (cos lambda1) (cos lambda2)) (* (sin lambda1) (sin lambda2))) |
| 58.0ms | (* (* (cos lambda1) (cos lambda2)) (* (cos lambda1) (cos lambda2))) |
| 76.0ms | (* (* (cos lambda1) (cos lambda2)) (* (cos lambda1) (cos lambda2))) |
| 2.0ms | (acos (+ (* (sin phi1) (sin phi2)) (/ (* (* (cos phi1) (cos phi2)) (+ (* (* (* (cos lambda1) (cos lambda2)) (* (cos lambda1) (cos lambda2))) (* (cos lambda1) (cos lambda2))) (* (* (sin lambda1) (sin lambda2)) (* (* (sin lambda1) (sin lambda2)) (* (sin lambda1) (sin lambda2)))))) (+ (* (* (cos lambda1) (cos lambda2)) (* (cos lambda1) (cos lambda2))) (- (* (* (sin lambda1) (sin lambda2)) (* (sin lambda1) (sin lambda2))) (* (* (cos lambda1) (cos lambda2)) (* (sin lambda1) (sin lambda2)))))))) |
| 141.0ms | (* (* (cos lambda1) (cos lambda2)) (* (sin lambda1) (sin lambda2))) |
| 79.0ms | (* (* (cos lambda1) (cos lambda2)) (* (cos lambda1) (cos lambda2))) |
| 77.0ms | (* (* (cos lambda1) (cos lambda2)) (* (cos lambda1) (cos lambda2))) |
| 71.0ms | (acos (+ (* (sin phi1) (sin phi2)) (/ (* (* (cos phi1) (cos phi2)) (+ (* (* (* (cos lambda1) (cos lambda2)) (* (cos lambda1) (cos lambda2))) (* (cos lambda1) (cos lambda2))) (* (* (sin lambda1) (sin lambda2)) (* (* (sin lambda1) (sin lambda2)) (* (sin lambda1) (sin lambda2)))))) (+ (* (* (cos lambda1) (cos lambda2)) (* (cos lambda1) (cos lambda2))) (- (* (* (sin lambda1) (sin lambda2)) (* (sin lambda1) (sin lambda2))) (* (* (cos lambda1) (cos lambda2)) (* (sin lambda1) (sin lambda2)))))))) |
| Iter | Nodes |
|---|---|
| done | 5014 |
| 2 | 1855 |
| 1 | 431 |
| 0 | 158 |
20 alts after pruning (20 fresh and 0 done)
Merged error: 3.5b
0% (0.4b remaining)
Error of 3.7b against oracle of 3.3b and baseline of 3.7b
| Iter | Nodes |
|---|---|
| done | 44 |
| 1 | 44 |
| 0 | 32 |
| 11.9s | 4788× | body | 1280 | valid |
| 3.7s | 2070× | body | 640 | valid |
| 1.0s | 730× | body | 320 | valid |
| 549.0ms | 272× | body | 160 | valid |
| 75.0ms | 16× | body | 2560 | valid |
| 32.0ms | 126× | body | 80 | valid |