Time bar (total: 5.8m)
| 69.0ms | 48× | body | 1280 | valid |
| 34.0ms | 43× | body | 640 | valid |
| 26.0ms | 133× | body | 80 | valid |
| 12.0ms | 22× | body | 320 | valid |
| 4.0ms | 12× | body | 160 | valid |
| 206.0ms | (* (* (* -2 J) (cos (/ K 2))) (sqrt (+ 1 (pow (/ U (* (* 2 J) (cos (/ K 2)))) 2)))) |
1 alts after pruning (1 fresh and 0 done)
Merged error: 12.7b
Found 4 expressions with local error:
| 8.0b | (sqrt (+ (* (/ U (* 2 (* (cos (/ K 2)) J))) (/ U (* 2 (* (cos (/ K 2)) J)))) 1)) |
| 4.6b | (* (sqrt (+ (* (/ U (* 2 (* (cos (/ K 2)) J))) (/ U (* 2 (* (cos (/ K 2)) J)))) 1)) (* -2 (* (cos (/ K 2)) J))) |
| 0.2b | (* (/ U (* 2 (* (cos (/ K 2)) J))) (/ U (* 2 (* (cos (/ K 2)) J)))) |
| 0.2b | (/ U (* 2 (* (cos (/ K 2)) J))) |
| 11× | pow1 |
| 10× | add-sqr-sqrt associate-*l* |
| 9× | *-un-lft-identity add-cube-cbrt |
| 8× | add-cbrt-cube add-exp-log |
| 6× | sqrt-prod |
| 5× | associate-*r* |
| 4× | sqrt-div insert-posit16 add-log-exp |
| 3× | associate-*l/ div-inv |
| 2× | flip3-+ pow-prod-down prod-exp *-commutative cbrt-unprod flip-+ |
| 1× | pow2 frac-times rem-sqrt-square clear-num associate-/r* frac-2neg pow-plus pow1/2 associate-*r/ pow-prod-up |
| 53.0ms | (* (sqrt (+ (* (/ U (* 2 (* (cos (/ K 2)) J))) (/ U (* 2 (* (cos (/ K 2)) J)))) 1)) (* -2 (* (cos (/ K 2)) J))) |
| 24.0ms | (sqrt (+ (* (/ U (* 2 (* (cos (/ K 2)) J))) (/ U (* 2 (* (cos (/ K 2)) J)))) 1)) |
| 24.0ms | (* (/ U (* 2 (* (cos (/ K 2)) J))) (/ U (* 2 (* (cos (/ K 2)) J)))) |
| 7.0ms | (/ U (* 2 (* (cos (/ K 2)) J))) |
| 154.0ms | (* (sqrt (+ (* (/ U (* 2 (* (cos (/ K 2)) J))) (/ U (* 2 (* (cos (/ K 2)) J)))) 1)) (* -2 (* (cos (/ K 2)) J))) |
| 114.0ms | (sqrt (+ (* (/ U (* 2 (* (cos (/ K 2)) J))) (/ U (* 2 (* (cos (/ K 2)) J)))) 1)) |
| 96.0ms | (* (/ U (* 2 (* (cos (/ K 2)) J))) (/ U (* 2 (* (cos (/ K 2)) J)))) |
| 88.0ms | (/ U (* 2 (* (cos (/ K 2)) J))) |
| 809.0ms | (+ (log (/ U (* 2 (* (cos (/ K 2)) J)))) (log (/ U (* 2 (* (cos (/ K 2)) J))))) |
| 516.0ms | (+ (log (sqrt (+ (* (/ U (* 2 (* (cos (/ K 2)) J))) (/ U (* 2 (* (cos (/ K 2)) J)))) 1))) (log (* -2 (* (cos (/ K 2)) J)))) |
| 501.0ms | (* (cbrt (sqrt (+ (* (/ U (* 2 (* (cos (/ K 2)) J))) (/ U (* 2 (* (cos (/ K 2)) J)))) 1))) (cbrt (sqrt (+ (* (/ U (* 2 (* (cos (/ K 2)) J))) (/ U (* 2 (* (cos (/ K 2)) J)))) 1)))) |
| 469.0ms | (* (* (* (/ U (* 2 (* (cos (/ K 2)) J))) (/ U (* 2 (* (cos (/ K 2)) J)))) (/ U (* 2 (* (cos (/ K 2)) J)))) (* (* (/ U (* 2 (* (cos (/ K 2)) J))) (/ U (* 2 (* (cos (/ K 2)) J)))) (/ U (* 2 (* (cos (/ K 2)) J))))) |
| 458.0ms | (* (sqrt (+ (* (/ U (* 2 (* (cos (/ K 2)) J))) (/ U (* 2 (* (cos (/ K 2)) J)))) 1)) (* -2 (* (cos (/ K 2)) J))) |
6 alts after pruning (5 fresh and 1 done)
Merged error: 4.5b
Found 4 expressions with local error:
| 8.0b | (sqrt (+ (* (/ U (* 2 (* (cos (/ K 2)) J))) (/ U (* 2 (* (cos (/ K 2)) J)))) 1)) |
| 8.0b | (sqrt (+ (* (/ U (* 2 (* (cos (/ K 2)) J))) (/ U (* 2 (* (cos (/ K 2)) J)))) 1)) |
| 8.0b | (sqrt (+ (* (/ U (* 2 (* (cos (/ K 2)) J))) (/ U (* 2 (* (cos (/ K 2)) J)))) 1)) |
| 4.6b | (* (sqrt (+ (* (/ U (* 2 (* (cos (/ K 2)) J))) (/ U (* 2 (* (cos (/ K 2)) J)))) 1)) (* -2 (* (cos (/ K 2)) J))) |
| 12× | add-sqr-sqrt sqrt-prod |
| 9× | *-un-lft-identity add-cube-cbrt |
| 8× | sqrt-div |
| 6× | pow1 add-cbrt-cube associate-*l* add-exp-log |
| 4× | flip3-+ flip-+ insert-posit16 add-log-exp |
| 3× | rem-sqrt-square pow1/2 |
| 2× | associate-*l/ |
| 1× | associate-*r* pow-prod-down prod-exp *-commutative cbrt-unprod |
| 41.0ms | (* (sqrt (+ (* (/ U (* 2 (* (cos (/ K 2)) J))) (/ U (* 2 (* (cos (/ K 2)) J)))) 1)) (* -2 (* (cos (/ K 2)) J))) |
| 27.0ms | (sqrt (+ (* (/ U (* 2 (* (cos (/ K 2)) J))) (/ U (* 2 (* (cos (/ K 2)) J)))) 1)) |
| 17.0ms | (sqrt (+ (* (/ U (* 2 (* (cos (/ K 2)) J))) (/ U (* 2 (* (cos (/ K 2)) J)))) 1)) |
| 13.0ms | (sqrt (+ (* (/ U (* 2 (* (cos (/ K 2)) J))) (/ U (* 2 (* (cos (/ K 2)) J)))) 1)) |
| 187.0ms | (* (sqrt (+ (* (/ U (* 2 (* (cos (/ K 2)) J))) (/ U (* 2 (* (cos (/ K 2)) J)))) 1)) (* -2 (* (cos (/ K 2)) J))) |
| 95.0ms | (sqrt (+ (* (/ U (* 2 (* (cos (/ K 2)) J))) (/ U (* 2 (* (cos (/ K 2)) J)))) 1)) |
| 93.0ms | (sqrt (+ (* (/ U (* 2 (* (cos (/ K 2)) J))) (/ U (* 2 (* (cos (/ K 2)) J)))) 1)) |
| 82.0ms | (sqrt (+ (* (/ U (* 2 (* (cos (/ K 2)) J))) (/ U (* 2 (* (cos (/ K 2)) J)))) 1)) |
| 452.0ms | (* (sqrt (+ (* (/ U (* 2 (* (cos (/ K 2)) J))) (/ U (* 2 (* (cos (/ K 2)) J)))) 1)) (* -2 (* (cos (/ K 2)) J))) |
| 445.0ms | (sqrt (* (cbrt (+ (* (/ U (* 2 (* (cos (/ K 2)) J))) (/ U (* 2 (* (cos (/ K 2)) J)))) 1)) (cbrt (+ (* (/ U (* 2 (* (cos (/ K 2)) J))) (/ U (* 2 (* (cos (/ K 2)) J)))) 1)))) |
| 418.0ms | (sqrt (* (cbrt (+ (* (/ U (* 2 (* (cos (/ K 2)) J))) (/ U (* 2 (* (cos (/ K 2)) J)))) 1)) (cbrt (+ (* (/ U (* 2 (* (cos (/ K 2)) J))) (/ U (* 2 (* (cos (/ K 2)) J)))) 1)))) |
| 415.0ms | (sqrt (sqrt (+ (* (/ U (* 2 (* (cos (/ K 2)) J))) (/ U (* 2 (* (cos (/ K 2)) J)))) 1))) |
| 409.0ms | (sqrt (sqrt (+ (* (/ U (* 2 (* (cos (/ K 2)) J))) (/ U (* 2 (* (cos (/ K 2)) J)))) 1))) |
6 alts after pruning (4 fresh and 2 done)
Merged error: 4.5b
Found 4 expressions with local error:
| 16.5b | (/ (* (sqrt (+ 1 (* (* (* (/ (/ U (* 2 (cos (/ K 2)))) J) (/ (/ U (* 2 (cos (/ K 2)))) J)) (* (/ (/ U (* 2 (cos (/ K 2)))) J) (/ (/ U (* 2 (cos (/ K 2)))) J))) (* (/ (/ U (* 2 (cos (/ K 2)))) J) (/ (/ U (* 2 (cos (/ K 2)))) J))))) (* (* -2 J) (cos (/ K 2)))) (sqrt (+ (* (* (/ U (* 2 (* (cos (/ K 2)) J))) (/ U (* 2 (* (cos (/ K 2)) J)))) (* (/ U (* 2 (* (cos (/ K 2)) J))) (/ U (* 2 (* (cos (/ K 2)) J))))) (- (* 1 1) (* (* (/ U (* 2 (* (cos (/ K 2)) J))) (/ U (* 2 (* (cos (/ K 2)) J)))) 1))))) |
| 10.6b | (+ (* (* (/ U (* 2 (* (cos (/ K 2)) J))) (/ U (* 2 (* (cos (/ K 2)) J)))) (* (/ U (* 2 (* (cos (/ K 2)) J))) (/ U (* 2 (* (cos (/ K 2)) J))))) (- (* 1 1) (* (* (/ U (* 2 (* (cos (/ K 2)) J))) (/ U (* 2 (* (cos (/ K 2)) J)))) 1))) |
| 6.8b | (sqrt (+ (* (* (/ U (* 2 (* (cos (/ K 2)) J))) (/ U (* 2 (* (cos (/ K 2)) J)))) (* (/ U (* 2 (* (cos (/ K 2)) J))) (/ U (* 2 (* (cos (/ K 2)) J))))) (- (* 1 1) (* (* (/ U (* 2 (* (cos (/ K 2)) J))) (/ U (* 2 (* (cos (/ K 2)) J)))) 1)))) |
| 4.2b | (sqrt (+ 1 (* (* (* (/ (/ U (* 2 (cos (/ K 2)))) J) (/ (/ U (* 2 (cos (/ K 2)))) J)) (* (/ (/ U (* 2 (cos (/ K 2)))) J) (/ (/ U (* 2 (cos (/ K 2)))) J))) (* (/ (/ U (* 2 (cos (/ K 2)))) J) (/ (/ U (* 2 (cos (/ K 2)))) J))))) |
| 102× | frac-times |
| 90× | frac-add |
| 68× | sqrt-div associate-*l/ |
| 66× | associate-*r/ |
| 45× | flip3-- flip-- |
| 32× | associate-/r/ |
| 13× | add-cbrt-cube add-exp-log |
| 12× | add-sqr-sqrt sqrt-prod |
| 10× | *-un-lft-identity add-cube-cbrt |
| 9× | add-log-exp |
| 6× | associate-/r* times-frac |
| 5× | flip3-+ flip-+ |
| 4× | pow1 insert-posit16 |
| 3× | cbrt-undiv div-exp prod-exp cbrt-unprod |
| 2× | rem-sqrt-square associate-+r+ sum-log pow1/2 associate-/l/ |
| 1× | +-commutative clear-num associate-+r- sub-neg frac-2neg diff-log div-inv associate-/l* |
| 109.0ms | (/ (* (sqrt (+ 1 (* (* (* (/ (/ U (* 2 (cos (/ K 2)))) J) (/ (/ U (* 2 (cos (/ K 2)))) J)) (* (/ (/ U (* 2 (cos (/ K 2)))) J) (/ (/ U (* 2 (cos (/ K 2)))) J))) (* (/ (/ U (* 2 (cos (/ K 2)))) J) (/ (/ U (* 2 (cos (/ K 2)))) J))))) (* (* -2 J) (cos (/ K 2)))) (sqrt (+ (* (* (/ U (* 2 (* (cos (/ K 2)) J))) (/ U (* 2 (* (cos (/ K 2)) J)))) (* (/ U (* 2 (* (cos (/ K 2)) J))) (/ U (* 2 (* (cos (/ K 2)) J))))) (- (* 1 1) (* (* (/ U (* 2 (* (cos (/ K 2)) J))) (/ U (* 2 (* (cos (/ K 2)) J)))) 1))))) |
| 98.0ms | (sqrt (+ (* (* (/ U (* 2 (* (cos (/ K 2)) J))) (/ U (* 2 (* (cos (/ K 2)) J)))) (* (/ U (* 2 (* (cos (/ K 2)) J))) (/ U (* 2 (* (cos (/ K 2)) J))))) (- (* 1 1) (* (* (/ U (* 2 (* (cos (/ K 2)) J))) (/ U (* 2 (* (cos (/ K 2)) J)))) 1)))) |
| 63.0ms | (+ (* (* (/ U (* 2 (* (cos (/ K 2)) J))) (/ U (* 2 (* (cos (/ K 2)) J)))) (* (/ U (* 2 (* (cos (/ K 2)) J))) (/ U (* 2 (* (cos (/ K 2)) J))))) (- (* 1 1) (* (* (/ U (* 2 (* (cos (/ K 2)) J))) (/ U (* 2 (* (cos (/ K 2)) J)))) 1))) |
| 1.0ms | (sqrt (+ 1 (* (* (* (/ (/ U (* 2 (cos (/ K 2)))) J) (/ (/ U (* 2 (cos (/ K 2)))) J)) (* (/ (/ U (* 2 (cos (/ K 2)))) J) (/ (/ U (* 2 (cos (/ K 2)))) J))) (* (/ (/ U (* 2 (cos (/ K 2)))) J) (/ (/ U (* 2 (cos (/ K 2)))) J))))) |
| 340.0ms | (/ (* (sqrt (+ 1 (* (* (* (/ (/ U (* 2 (cos (/ K 2)))) J) (/ (/ U (* 2 (cos (/ K 2)))) J)) (* (/ (/ U (* 2 (cos (/ K 2)))) J) (/ (/ U (* 2 (cos (/ K 2)))) J))) (* (/ (/ U (* 2 (cos (/ K 2)))) J) (/ (/ U (* 2 (cos (/ K 2)))) J))))) (* (* -2 J) (cos (/ K 2)))) (sqrt (+ (* (* (/ U (* 2 (* (cos (/ K 2)) J))) (/ U (* 2 (* (cos (/ K 2)) J)))) (* (/ U (* 2 (* (cos (/ K 2)) J))) (/ U (* 2 (* (cos (/ K 2)) J))))) (- (* 1 1) (* (* (/ U (* 2 (* (cos (/ K 2)) J))) (/ U (* 2 (* (cos (/ K 2)) J)))) 1))))) |
| 212.0ms | (sqrt (+ (* (* (/ U (* 2 (* (cos (/ K 2)) J))) (/ U (* 2 (* (cos (/ K 2)) J)))) (* (/ U (* 2 (* (cos (/ K 2)) J))) (/ U (* 2 (* (cos (/ K 2)) J))))) (- (* 1 1) (* (* (/ U (* 2 (* (cos (/ K 2)) J))) (/ U (* 2 (* (cos (/ K 2)) J)))) 1)))) |
| 127.0ms | (+ (* (* (/ U (* 2 (* (cos (/ K 2)) J))) (/ U (* 2 (* (cos (/ K 2)) J)))) (* (/ U (* 2 (* (cos (/ K 2)) J))) (/ U (* 2 (* (cos (/ K 2)) J))))) (- (* 1 1) (* (* (/ U (* 2 (* (cos (/ K 2)) J))) (/ U (* 2 (* (cos (/ K 2)) J)))) 1))) |
| 105.0ms | (sqrt (+ 1 (* (* (* (/ (/ U (* 2 (cos (/ K 2)))) J) (/ (/ U (* 2 (cos (/ K 2)))) J)) (* (/ (/ U (* 2 (cos (/ K 2)))) J) (/ (/ U (* 2 (cos (/ K 2)))) J))) (* (/ (/ U (* 2 (cos (/ K 2)))) J) (/ (/ U (* 2 (cos (/ K 2)))) J))))) |
| 1.8s | (/ (* (* (* (sqrt (+ 1 (* (* (* (/ (/ U (* 2 (cos (/ K 2)))) J) (/ (/ U (* 2 (cos (/ K 2)))) J)) (* (/ (/ U (* 2 (cos (/ K 2)))) J) (/ (/ U (* 2 (cos (/ K 2)))) J))) (* (/ (/ U (* 2 (cos (/ K 2)))) J) (/ (/ U (* 2 (cos (/ K 2)))) J))))) (* (* -2 J) (cos (/ K 2)))) (* (sqrt (+ 1 (* (* (* (/ (/ U (* 2 (cos (/ K 2)))) J) (/ (/ U (* 2 (cos (/ K 2)))) J)) (* (/ (/ U (* 2 (cos (/ K 2)))) J) (/ (/ U (* 2 (cos (/ K 2)))) J))) (* (/ (/ U (* 2 (cos (/ K 2)))) J) (/ (/ U (* 2 (cos (/ K 2)))) J))))) (* (* -2 J) (cos (/ K 2))))) (* (sqrt (+ 1 (* (* (* (/ (/ U (* 2 (cos (/ K 2)))) J) (/ (/ U (* 2 (cos (/ K 2)))) J)) (* (/ (/ U (* 2 (cos (/ K 2)))) J) (/ (/ U (* 2 (cos (/ K 2)))) J))) (* (/ (/ U (* 2 (cos (/ K 2)))) J) (/ (/ U (* 2 (cos (/ K 2)))) J))))) (* (* -2 J) (cos (/ K 2))))) (* (* (sqrt (+ (* (* (/ U (* 2 (* (cos (/ K 2)) J))) (/ U (* 2 (* (cos (/ K 2)) J)))) (* (/ U (* 2 (* (cos (/ K 2)) J))) (/ U (* 2 (* (cos (/ K 2)) J))))) (- (* 1 1) (* (* (/ U (* 2 (* (cos (/ K 2)) J))) (/ U (* 2 (* (cos (/ K 2)) J)))) 1)))) (sqrt (+ (* (* (/ U (* 2 (* (cos (/ K 2)) J))) (/ U (* 2 (* (cos (/ K 2)) J)))) (* (/ U (* 2 (* (cos (/ K 2)) J))) (/ U (* 2 (* (cos (/ K 2)) J))))) (- (* 1 1) (* (* (/ U (* 2 (* (cos (/ K 2)) J))) (/ U (* 2 (* (cos (/ K 2)) J)))) 1))))) (sqrt (+ (* (* (/ U (* 2 (* (cos (/ K 2)) J))) (/ U (* 2 (* (cos (/ K 2)) J)))) (* (/ U (* 2 (* (cos (/ K 2)) J))) (/ U (* 2 (* (cos (/ K 2)) J))))) (- (* 1 1) (* (* (/ U (* 2 (* (cos (/ K 2)) J))) (/ U (* 2 (* (cos (/ K 2)) J)))) 1)))))) |
| 1.4s | (sqrt (+ (* (* (* U (/ U (* 2 (* (cos (/ K 2)) J)))) (* (/ U (* 2 (* (cos (/ K 2)) J))) U)) (+ (* (* 1 1) (* 1 1)) (+ (* (* (* (/ U (* 2 (* (cos (/ K 2)) J))) (/ U (* 2 (* (cos (/ K 2)) J)))) 1) (* (* (/ U (* 2 (* (cos (/ K 2)) J))) (/ U (* 2 (* (cos (/ K 2)) J)))) 1)) (* (* 1 1) (* (* (/ U (* 2 (* (cos (/ K 2)) J))) (/ U (* 2 (* (cos (/ K 2)) J)))) 1))))) (* (* (* 2 (* (cos (/ K 2)) J)) (* 2 (* (cos (/ K 2)) J))) (- (pow (* 1 1) 3) (pow (* (* (/ U (* 2 (* (cos (/ K 2)) J))) (/ U (* 2 (* (cos (/ K 2)) J)))) 1) 3))))) |
| 1.4s | (sqrt (+ (* (* (* (/ U (* 2 (* (cos (/ K 2)) J))) U) (* (/ U (* 2 (* (cos (/ K 2)) J))) U)) (+ (* (* 1 1) (* 1 1)) (+ (* (* (* (/ U (* 2 (* (cos (/ K 2)) J))) (/ U (* 2 (* (cos (/ K 2)) J)))) 1) (* (* (/ U (* 2 (* (cos (/ K 2)) J))) (/ U (* 2 (* (cos (/ K 2)) J)))) 1)) (* (* 1 1) (* (* (/ U (* 2 (* (cos (/ K 2)) J))) (/ U (* 2 (* (cos (/ K 2)) J)))) 1))))) (* (* (* 2 (* (cos (/ K 2)) J)) (* 2 (* (cos (/ K 2)) J))) (- (pow (* 1 1) 3) (pow (* (* (/ U (* 2 (* (cos (/ K 2)) J))) (/ U (* 2 (* (cos (/ K 2)) J)))) 1) 3))))) |
| 1.3s | (+ (* (* (* U U) (* U U)) (+ (* (* 1 1) (* 1 1)) (+ (* (* (* (/ U (* 2 (* (cos (/ K 2)) J))) (/ U (* 2 (* (cos (/ K 2)) J)))) 1) (* (* (/ U (* 2 (* (cos (/ K 2)) J))) (/ U (* 2 (* (cos (/ K 2)) J)))) 1)) (* (* 1 1) (* (* (/ U (* 2 (* (cos (/ K 2)) J))) (/ U (* 2 (* (cos (/ K 2)) J)))) 1))))) (* (* (* (* 2 (* (cos (/ K 2)) J)) (* 2 (* (cos (/ K 2)) J))) (* (* 2 (* (cos (/ K 2)) J)) (* 2 (* (cos (/ K 2)) J)))) (- (pow (* 1 1) 3) (pow (* (* (/ U (* 2 (* (cos (/ K 2)) J))) (/ U (* 2 (* (cos (/ K 2)) J)))) 1) 3)))) |
| 1.3s | (+ (* (* (* (/ U (* 2 (* (cos (/ K 2)) J))) U) (* (/ U (* 2 (* (cos (/ K 2)) J))) U)) (+ (* (* 1 1) (* 1 1)) (+ (* (* (* (/ U (* 2 (* (cos (/ K 2)) J))) (/ U (* 2 (* (cos (/ K 2)) J)))) 1) (* (* (/ U (* 2 (* (cos (/ K 2)) J))) (/ U (* 2 (* (cos (/ K 2)) J)))) 1)) (* (* 1 1) (* (* (/ U (* 2 (* (cos (/ K 2)) J))) (/ U (* 2 (* (cos (/ K 2)) J)))) 1))))) (* (* (* 2 (* (cos (/ K 2)) J)) (* 2 (* (cos (/ K 2)) J))) (- (pow (* 1 1) 3) (pow (* (* (/ U (* 2 (* (cos (/ K 2)) J))) (/ U (* 2 (* (cos (/ K 2)) J)))) 1) 3)))) |
8 alts after pruning (5 fresh and 3 done)
Merged error: 4.5b
Found 4 expressions with local error:
| 14.7b | (* (/ (sqrt (+ 1 (* (* (* (/ (/ U (* 2 (cos (/ K 2)))) J) (/ (/ U (* 2 (cos (/ K 2)))) J)) (* (/ (/ U (* 2 (cos (/ K 2)))) J) (/ (/ U (* 2 (cos (/ K 2)))) J))) (* (/ (/ U (* 2 (cos (/ K 2)))) J) (/ (/ U (* 2 (cos (/ K 2)))) J))))) (sqrt (sqrt (+ (* (* (/ U (* 2 (* (cos (/ K 2)) J))) (/ U (* 2 (* (cos (/ K 2)) J)))) (* (/ U (* 2 (* (cos (/ K 2)) J))) (/ U (* 2 (* (cos (/ K 2)) J))))) (- (* 1 1) (* (* (/ U (* 2 (* (cos (/ K 2)) J))) (/ U (* 2 (* (cos (/ K 2)) J)))) 1)))))) (/ (* (* -2 J) (cos (/ K 2))) (sqrt (sqrt (+ (* (* (/ U (* 2 (* (cos (/ K 2)) J))) (/ U (* 2 (* (cos (/ K 2)) J)))) (* (/ U (* 2 (* (cos (/ K 2)) J))) (/ U (* 2 (* (cos (/ K 2)) J))))) (- (* 1 1) (* (* (/ U (* 2 (* (cos (/ K 2)) J))) (/ U (* 2 (* (cos (/ K 2)) J)))) 1))))))) |
| 10.6b | (+ (* (* (/ U (* 2 (* (cos (/ K 2)) J))) (/ U (* 2 (* (cos (/ K 2)) J)))) (* (/ U (* 2 (* (cos (/ K 2)) J))) (/ U (* 2 (* (cos (/ K 2)) J))))) (- (* 1 1) (* (* (/ U (* 2 (* (cos (/ K 2)) J))) (/ U (* 2 (* (cos (/ K 2)) J)))) 1))) |
| 10.6b | (+ (* (* (/ U (* 2 (* (cos (/ K 2)) J))) (/ U (* 2 (* (cos (/ K 2)) J)))) (* (/ U (* 2 (* (cos (/ K 2)) J))) (/ U (* 2 (* (cos (/ K 2)) J))))) (- (* 1 1) (* (* (/ U (* 2 (* (cos (/ K 2)) J))) (/ U (* 2 (* (cos (/ K 2)) J)))) 1))) |
| 8.5b | (/ (sqrt (+ 1 (* (* (* (/ (/ U (* 2 (cos (/ K 2)))) J) (/ (/ U (* 2 (cos (/ K 2)))) J)) (* (/ (/ U (* 2 (cos (/ K 2)))) J) (/ (/ U (* 2 (cos (/ K 2)))) J))) (* (/ (/ U (* 2 (cos (/ K 2)))) J) (/ (/ U (* 2 (cos (/ K 2)))) J))))) (sqrt (sqrt (+ (* (* (/ U (* 2 (* (cos (/ K 2)) J))) (/ U (* 2 (* (cos (/ K 2)) J)))) (* (/ U (* 2 (* (cos (/ K 2)) J))) (/ U (* 2 (* (cos (/ K 2)) J))))) (- (* 1 1) (* (* (/ U (* 2 (* (cos (/ K 2)) J))) (/ U (* 2 (* (cos (/ K 2)) J)))) 1)))))) |
| 194× | sqrt-div |
| 183× | sqrt-prod |
| 171× | frac-times |
| 150× | frac-add |
| 117× | times-frac |
| 111× | associate-*l/ associate-*r/ |
| 96× | associate-/r/ |
| 90× | associate-*l* |
| 86× | add-sqr-sqrt *-un-lft-identity add-cube-cbrt |
| 75× | flip3-- flip-- |
| 45× | associate-*r* |
| 27× | add-cbrt-cube add-exp-log |
| 14× | add-log-exp |
| 9× | associate-/r* |
| 8× | cbrt-undiv div-exp prod-exp cbrt-unprod |
| 6× | pow1 flip3-+ flip-+ associate-/l* |
| 4× | associate-+r+ sum-log insert-posit16 |
| 3× | div-inv |
| 2× | +-commutative associate-+r- sub-neg diff-log associate-/l/ |
| 1× | sqrt-undiv clear-num frac-2neg pow-prod-down *-commutative |
| 306.0ms | (* (/ (sqrt (+ 1 (* (* (* (/ (/ U (* 2 (cos (/ K 2)))) J) (/ (/ U (* 2 (cos (/ K 2)))) J)) (* (/ (/ U (* 2 (cos (/ K 2)))) J) (/ (/ U (* 2 (cos (/ K 2)))) J))) (* (/ (/ U (* 2 (cos (/ K 2)))) J) (/ (/ U (* 2 (cos (/ K 2)))) J))))) (sqrt (sqrt (+ (* (* (/ U (* 2 (* (cos (/ K 2)) J))) (/ U (* 2 (* (cos (/ K 2)) J)))) (* (/ U (* 2 (* (cos (/ K 2)) J))) (/ U (* 2 (* (cos (/ K 2)) J))))) (- (* 1 1) (* (* (/ U (* 2 (* (cos (/ K 2)) J))) (/ U (* 2 (* (cos (/ K 2)) J)))) 1)))))) (/ (* (* -2 J) (cos (/ K 2))) (sqrt (sqrt (+ (* (* (/ U (* 2 (* (cos (/ K 2)) J))) (/ U (* 2 (* (cos (/ K 2)) J)))) (* (/ U (* 2 (* (cos (/ K 2)) J))) (/ U (* 2 (* (cos (/ K 2)) J))))) (- (* 1 1) (* (* (/ U (* 2 (* (cos (/ K 2)) J))) (/ U (* 2 (* (cos (/ K 2)) J)))) 1))))))) |
| 128.0ms | (/ (sqrt (+ 1 (* (* (* (/ (/ U (* 2 (cos (/ K 2)))) J) (/ (/ U (* 2 (cos (/ K 2)))) J)) (* (/ (/ U (* 2 (cos (/ K 2)))) J) (/ (/ U (* 2 (cos (/ K 2)))) J))) (* (/ (/ U (* 2 (cos (/ K 2)))) J) (/ (/ U (* 2 (cos (/ K 2)))) J))))) (sqrt (sqrt (+ (* (* (/ U (* 2 (* (cos (/ K 2)) J))) (/ U (* 2 (* (cos (/ K 2)) J)))) (* (/ U (* 2 (* (cos (/ K 2)) J))) (/ U (* 2 (* (cos (/ K 2)) J))))) (- (* 1 1) (* (* (/ U (* 2 (* (cos (/ K 2)) J))) (/ U (* 2 (* (cos (/ K 2)) J)))) 1)))))) |
| 52.0ms | (+ (* (* (/ U (* 2 (* (cos (/ K 2)) J))) (/ U (* 2 (* (cos (/ K 2)) J)))) (* (/ U (* 2 (* (cos (/ K 2)) J))) (/ U (* 2 (* (cos (/ K 2)) J))))) (- (* 1 1) (* (* (/ U (* 2 (* (cos (/ K 2)) J))) (/ U (* 2 (* (cos (/ K 2)) J)))) 1))) |
| 47.0ms | (+ (* (* (/ U (* 2 (* (cos (/ K 2)) J))) (/ U (* 2 (* (cos (/ K 2)) J)))) (* (/ U (* 2 (* (cos (/ K 2)) J))) (/ U (* 2 (* (cos (/ K 2)) J))))) (- (* 1 1) (* (* (/ U (* 2 (* (cos (/ K 2)) J))) (/ U (* 2 (* (cos (/ K 2)) J)))) 1))) |
| 407.0ms | (/ (sqrt (+ 1 (* (* (* (/ (/ U (* 2 (cos (/ K 2)))) J) (/ (/ U (* 2 (cos (/ K 2)))) J)) (* (/ (/ U (* 2 (cos (/ K 2)))) J) (/ (/ U (* 2 (cos (/ K 2)))) J))) (* (/ (/ U (* 2 (cos (/ K 2)))) J) (/ (/ U (* 2 (cos (/ K 2)))) J))))) (sqrt (sqrt (+ (* (* (/ U (* 2 (* (cos (/ K 2)) J))) (/ U (* 2 (* (cos (/ K 2)) J)))) (* (/ U (* 2 (* (cos (/ K 2)) J))) (/ U (* 2 (* (cos (/ K 2)) J))))) (- (* 1 1) (* (* (/ U (* 2 (* (cos (/ K 2)) J))) (/ U (* 2 (* (cos (/ K 2)) J)))) 1)))))) |
| 361.0ms | (* (/ (sqrt (+ 1 (* (* (* (/ (/ U (* 2 (cos (/ K 2)))) J) (/ (/ U (* 2 (cos (/ K 2)))) J)) (* (/ (/ U (* 2 (cos (/ K 2)))) J) (/ (/ U (* 2 (cos (/ K 2)))) J))) (* (/ (/ U (* 2 (cos (/ K 2)))) J) (/ (/ U (* 2 (cos (/ K 2)))) J))))) (sqrt (sqrt (+ (* (* (/ U (* 2 (* (cos (/ K 2)) J))) (/ U (* 2 (* (cos (/ K 2)) J)))) (* (/ U (* 2 (* (cos (/ K 2)) J))) (/ U (* 2 (* (cos (/ K 2)) J))))) (- (* 1 1) (* (* (/ U (* 2 (* (cos (/ K 2)) J))) (/ U (* 2 (* (cos (/ K 2)) J)))) 1)))))) (/ (* (* -2 J) (cos (/ K 2))) (sqrt (sqrt (+ (* (* (/ U (* 2 (* (cos (/ K 2)) J))) (/ U (* 2 (* (cos (/ K 2)) J)))) (* (/ U (* 2 (* (cos (/ K 2)) J))) (/ U (* 2 (* (cos (/ K 2)) J))))) (- (* 1 1) (* (* (/ U (* 2 (* (cos (/ K 2)) J))) (/ U (* 2 (* (cos (/ K 2)) J)))) 1))))))) |
| 120.0ms | (+ (* (* (/ U (* 2 (* (cos (/ K 2)) J))) (/ U (* 2 (* (cos (/ K 2)) J)))) (* (/ U (* 2 (* (cos (/ K 2)) J))) (/ U (* 2 (* (cos (/ K 2)) J))))) (- (* 1 1) (* (* (/ U (* 2 (* (cos (/ K 2)) J))) (/ U (* 2 (* (cos (/ K 2)) J)))) 1))) |
| 106.0ms | (+ (* (* (/ U (* 2 (* (cos (/ K 2)) J))) (/ U (* 2 (* (cos (/ K 2)) J)))) (* (/ U (* 2 (* (cos (/ K 2)) J))) (/ U (* 2 (* (cos (/ K 2)) J))))) (- (* 1 1) (* (* (/ U (* 2 (* (cos (/ K 2)) J))) (/ U (* 2 (* (cos (/ K 2)) J)))) 1))) |
| 1.6s | (/ (sqrt (+ 1 (* (* (* (/ (/ U (* 2 (cos (/ K 2)))) J) (/ (/ U (* 2 (cos (/ K 2)))) J)) (* (/ (/ U (* 2 (cos (/ K 2)))) J) (/ (/ U (* 2 (cos (/ K 2)))) J))) (* (/ (/ U (* 2 (cos (/ K 2)))) J) (/ (/ U (* 2 (cos (/ K 2)))) J))))) (sqrt (sqrt (+ (* (* (* (/ U (* 2 (* (cos (/ K 2)) J))) (/ U (* 2 (* (cos (/ K 2)) J)))) (* (/ U (* 2 (* (cos (/ K 2)) J))) U)) (+ (* (* 1 1) (* 1 1)) (+ (* (* (* (/ U (* 2 (* (cos (/ K 2)) J))) (/ U (* 2 (* (cos (/ K 2)) J)))) 1) (* (* (/ U (* 2 (* (cos (/ K 2)) J))) (/ U (* 2 (* (cos (/ K 2)) J)))) 1)) (* (* 1 1) (* (* (/ U (* 2 (* (cos (/ K 2)) J))) (/ U (* 2 (* (cos (/ K 2)) J)))) 1))))) (* (* 2 (* (cos (/ K 2)) J)) (- (pow (* 1 1) 3) (pow (* (* (/ U (* 2 (* (cos (/ K 2)) J))) (/ U (* 2 (* (cos (/ K 2)) J)))) 1) 3))))))) |
| 1.5s | (/ (sqrt (+ 1 (* (* (* (/ (/ U (* 2 (cos (/ K 2)))) J) (/ (/ U (* 2 (cos (/ K 2)))) J)) (* (/ (/ U (* 2 (cos (/ K 2)))) J) (/ (/ U (* 2 (cos (/ K 2)))) J))) (* (/ (/ U (* 2 (cos (/ K 2)))) J) (/ (/ U (* 2 (cos (/ K 2)))) J))))) (sqrt (sqrt (+ (* (* (* (/ U (* 2 (* (cos (/ K 2)) J))) U) (* (/ U (* 2 (* (cos (/ K 2)) J))) (/ U (* 2 (* (cos (/ K 2)) J))))) (+ (* (* 1 1) (* 1 1)) (+ (* (* (* (/ U (* 2 (* (cos (/ K 2)) J))) (/ U (* 2 (* (cos (/ K 2)) J)))) 1) (* (* (/ U (* 2 (* (cos (/ K 2)) J))) (/ U (* 2 (* (cos (/ K 2)) J)))) 1)) (* (* 1 1) (* (* (/ U (* 2 (* (cos (/ K 2)) J))) (/ U (* 2 (* (cos (/ K 2)) J)))) 1))))) (* (* 2 (* (cos (/ K 2)) J)) (- (pow (* 1 1) 3) (pow (* (* (/ U (* 2 (* (cos (/ K 2)) J))) (/ U (* 2 (* (cos (/ K 2)) J)))) 1) 3))))))) |
| 1.4s | (* (* (* (/ (sqrt (+ 1 (* (* (* (/ (/ U (* 2 (cos (/ K 2)))) J) (/ (/ U (* 2 (cos (/ K 2)))) J)) (* (/ (/ U (* 2 (cos (/ K 2)))) J) (/ (/ U (* 2 (cos (/ K 2)))) J))) (* (/ (/ U (* 2 (cos (/ K 2)))) J) (/ (/ U (* 2 (cos (/ K 2)))) J))))) (sqrt (sqrt (+ (* (* (/ U (* 2 (* (cos (/ K 2)) J))) (/ U (* 2 (* (cos (/ K 2)) J)))) (* (/ U (* 2 (* (cos (/ K 2)) J))) (/ U (* 2 (* (cos (/ K 2)) J))))) (- (* 1 1) (* (* (/ U (* 2 (* (cos (/ K 2)) J))) (/ U (* 2 (* (cos (/ K 2)) J)))) 1)))))) (/ (sqrt (+ 1 (* (* (* (/ (/ U (* 2 (cos (/ K 2)))) J) (/ (/ U (* 2 (cos (/ K 2)))) J)) (* (/ (/ U (* 2 (cos (/ K 2)))) J) (/ (/ U (* 2 (cos (/ K 2)))) J))) (* (/ (/ U (* 2 (cos (/ K 2)))) J) (/ (/ U (* 2 (cos (/ K 2)))) J))))) (sqrt (sqrt (+ (* (* (/ U (* 2 (* (cos (/ K 2)) J))) (/ U (* 2 (* (cos (/ K 2)) J)))) (* (/ U (* 2 (* (cos (/ K 2)) J))) (/ U (* 2 (* (cos (/ K 2)) J))))) (- (* 1 1) (* (* (/ U (* 2 (* (cos (/ K 2)) J))) (/ U (* 2 (* (cos (/ K 2)) J)))) 1))))))) (/ (sqrt (+ 1 (* (* (* (/ (/ U (* 2 (cos (/ K 2)))) J) (/ (/ U (* 2 (cos (/ K 2)))) J)) (* (/ (/ U (* 2 (cos (/ K 2)))) J) (/ (/ U (* 2 (cos (/ K 2)))) J))) (* (/ (/ U (* 2 (cos (/ K 2)))) J) (/ (/ U (* 2 (cos (/ K 2)))) J))))) (sqrt (sqrt (+ (* (* (/ U (* 2 (* (cos (/ K 2)) J))) (/ U (* 2 (* (cos (/ K 2)) J)))) (* (/ U (* 2 (* (cos (/ K 2)) J))) (/ U (* 2 (* (cos (/ K 2)) J))))) (- (* 1 1) (* (* (/ U (* 2 (* (cos (/ K 2)) J))) (/ U (* 2 (* (cos (/ K 2)) J)))) 1))))))) (* (* (/ (* (* -2 J) (cos (/ K 2))) (sqrt (sqrt (+ (* (* (/ U (* 2 (* (cos (/ K 2)) J))) (/ U (* 2 (* (cos (/ K 2)) J)))) (* (/ U (* 2 (* (cos (/ K 2)) J))) (/ U (* 2 (* (cos (/ K 2)) J))))) (- (* 1 1) (* (* (/ U (* 2 (* (cos (/ K 2)) J))) (/ U (* 2 (* (cos (/ K 2)) J)))) 1)))))) (/ (* (* -2 J) (cos (/ K 2))) (sqrt (sqrt (+ (* (* (/ U (* 2 (* (cos (/ K 2)) J))) (/ U (* 2 (* (cos (/ K 2)) J)))) (* (/ U (* 2 (* (cos (/ K 2)) J))) (/ U (* 2 (* (cos (/ K 2)) J))))) (- (* 1 1) (* (* (/ U (* 2 (* (cos (/ K 2)) J))) (/ U (* 2 (* (cos (/ K 2)) J)))) 1))))))) (/ (* (* -2 J) (cos (/ K 2))) (sqrt (sqrt (+ (* (* (/ U (* 2 (* (cos (/ K 2)) J))) (/ U (* 2 (* (cos (/ K 2)) J)))) (* (/ U (* 2 (* (cos (/ K 2)) J))) (/ U (* 2 (* (cos (/ K 2)) J))))) (- (* 1 1) (* (* (/ U (* 2 (* (cos (/ K 2)) J))) (/ U (* 2 (* (cos (/ K 2)) J)))) 1)))))))) |
| 1.3s | (sqrt (sqrt (* (* (* 2 (* (cos (/ K 2)) J)) (* (* 2 (* (cos (/ K 2)) J)) (* 2 (* (cos (/ K 2)) J)))) (+ (* (* 1 1) (* 1 1)) (+ (* (* (* (/ U (* 2 (* (cos (/ K 2)) J))) (/ U (* 2 (* (cos (/ K 2)) J)))) 1) (* (* (/ U (* 2 (* (cos (/ K 2)) J))) (/ U (* 2 (* (cos (/ K 2)) J)))) 1)) (* (* 1 1) (* (* (/ U (* 2 (* (cos (/ K 2)) J))) (/ U (* 2 (* (cos (/ K 2)) J)))) 1))))))) |
| 1.2s | (/ (sqrt (+ 1 (* (* (* (/ (/ U (* 2 (cos (/ K 2)))) J) (/ (/ U (* 2 (cos (/ K 2)))) J)) (* (/ (/ U (* 2 (cos (/ K 2)))) J) (/ (/ U (* 2 (cos (/ K 2)))) J))) (* (/ (/ U (* 2 (cos (/ K 2)))) J) (/ (/ U (* 2 (cos (/ K 2)))) J))))) (sqrt (sqrt (+ (* (* (* (/ U (* 2 (* (cos (/ K 2)) J))) (/ U (* 2 (* (cos (/ K 2)) J)))) (* U (/ U (* 2 (* (cos (/ K 2)) J))))) (+ (* (* 1 1) (* 1 1)) (+ (* (* (* (/ U (* 2 (* (cos (/ K 2)) J))) (/ U (* 2 (* (cos (/ K 2)) J)))) 1) (* (* (/ U (* 2 (* (cos (/ K 2)) J))) (/ U (* 2 (* (cos (/ K 2)) J)))) 1)) (* (* 1 1) (* (* (/ U (* 2 (* (cos (/ K 2)) J))) (/ U (* 2 (* (cos (/ K 2)) J)))) 1))))) (* (* 2 (* (cos (/ K 2)) J)) (- (pow (* 1 1) 3) (pow (* (* (/ U (* 2 (* (cos (/ K 2)) J))) (/ U (* 2 (* (cos (/ K 2)) J)))) 1) 3))))))) |
9 alts after pruning (6 fresh and 3 done)
Merged error: 4.5b
12.2% (7.5b remaining)
Error of 15.6b against oracle of 8.1b and baseline of 16.6b
| 1.7s | 1514× | body | 1280 | valid |
| 1.2s | 1296× | body | 640 | valid |
| 783.0ms | 4296× | body | 80 | valid |
| 362.0ms | 588× | body | 320 | valid |
| 96.0ms | 309× | body | 160 | valid |