Time bar (total: 33.4s)
| 69.0ms | 46× | body | 1280 | valid |
| 40.0ms | 40× | body | 640 | valid |
| 36.0ms | 141× | body | 80 | valid |
| 14.0ms | 19× | body | 320 | valid |
| 5.0ms | 10× | body | 160 | valid |
1 alts after pruning (1 fresh and 0 done)
Merged error: 7.6b
Found 4 expressions with local error:
| 7.6b | (* (hypot 1 (/ U (* J (* (cos (/ K 2)) 2)))) (* (cos (/ K 2)) (* -2 J))) |
| 0.1b | (* J (* (cos (/ K 2)) 2)) |
| 0.1b | (* (cos (/ K 2)) (* -2 J)) |
| 0.1b | (/ U (* J (* (cos (/ K 2)) 2))) |
| 32× | add-cbrt-cube add-exp-log |
| 23× | pow1 |
| 15× | prod-exp cbrt-unprod |
| 12× | pow-prod-down |
| 9× | add-sqr-sqrt *-un-lft-identity associate-*l* add-cube-cbrt |
| 4× | expm1-log1p-u insert-posit16 log1p-expm1-u add-log-exp |
| 3× | cbrt-undiv times-frac div-exp associate-*r* *-commutative associate-/l* |
| 1× | clear-num associate-/r* frac-2neg div-inv |
| 40.0ms | (* (hypot 1 (/ U (* J (* (cos (/ K 2)) 2)))) (* (cos (/ K 2)) (* -2 J))) |
| 15.0ms | (* J (* (cos (/ K 2)) 2)) |
| 14.0ms | (* (cos (/ K 2)) (* -2 J)) |
| 14.0ms | (/ U (* J (* (cos (/ K 2)) 2))) |
| 366.0ms | (* (hypot 1 (/ U (* J (* (cos (/ K 2)) 2)))) (* (cos (/ K 2)) (* -2 J))) |
| 114.0ms | (/ U (* J (* (cos (/ K 2)) 2))) |
| 65.0ms | (* J (* (cos (/ K 2)) 2)) |
| 61.0ms | (* (cos (/ K 2)) (* -2 J)) |
9 alts after pruning (8 fresh and 1 done)
Merged error: 2.8b
Found 4 expressions with local error:
| 7.6b | (sqrt (hypot 1 (/ U (* J (* (cos (/ K 2)) 2))))) |
| 7.6b | (sqrt (hypot 1 (/ U (* J (* (cos (/ K 2)) 2))))) |
| 0.2b | (* (sqrt (hypot 1 (/ U (* J (* (cos (/ K 2)) 2))))) (* (cos (/ K 2)) (* -2 J))) |
| 0.1b | (* (sqrt (hypot 1 (/ U (* J (* (cos (/ K 2)) 2))))) (* (sqrt (hypot 1 (/ U (* J (* (cos (/ K 2)) 2))))) (* (cos (/ K 2)) (* -2 J)))) |
| 29× | pow1 |
| 27× | add-cbrt-cube add-exp-log |
| 16× | pow-prod-down prod-exp cbrt-unprod |
| 12× | add-sqr-sqrt associate-*l* sqrt-prod |
| 10× | *-un-lft-identity add-cube-cbrt |
| 4× | expm1-log1p-u insert-posit16 log1p-expm1-u add-log-exp |
| 2× | rem-sqrt-square sqrt-pow1 pow1/2 associate-*r* *-commutative |
| 160.0ms | (* (sqrt (hypot 1 (/ U (* J (* (cos (/ K 2)) 2))))) (* (sqrt (hypot 1 (/ U (* J (* (cos (/ K 2)) 2))))) (* (cos (/ K 2)) (* -2 J)))) |
| 42.0ms | (* (sqrt (hypot 1 (/ U (* J (* (cos (/ K 2)) 2))))) (* (cos (/ K 2)) (* -2 J))) |
| 1.0ms | (sqrt (hypot 1 (/ U (* J (* (cos (/ K 2)) 2))))) |
| 1.0ms | (sqrt (hypot 1 (/ U (* J (* (cos (/ K 2)) 2))))) |
| 321.0ms | (* (sqrt (hypot 1 (/ U (* J (* (cos (/ K 2)) 2))))) (* (sqrt (hypot 1 (/ U (* J (* (cos (/ K 2)) 2))))) (* (cos (/ K 2)) (* -2 J)))) |
| 314.0ms | (* (sqrt (hypot 1 (/ U (* J (* (cos (/ K 2)) 2))))) (* (cos (/ K 2)) (* -2 J))) |
| 286.0ms | (sqrt (hypot 1 (/ U (* J (* (cos (/ K 2)) 2))))) |
| 251.0ms | (sqrt (hypot 1 (/ U (* J (* (cos (/ K 2)) 2))))) |
8 alts after pruning (7 fresh and 1 done)
Merged error: 2.8b
Found 4 expressions with local error:
| 7.6b | (sqrt (hypot 1 (/ U (* J (* (cos (/ K 2)) 2))))) |
| 7.6b | (sqrt (hypot 1 (/ U (* J (* (cos (/ K 2)) 2))))) |
| 7.6b | (sqrt (hypot 1 (/ U (* J (* (cos (/ K 2)) 2))))) |
| 0.2b | (* (sqrt (sqrt (hypot 1 (/ U (* J (* (cos (/ K 2)) 2)))))) (sqrt (sqrt (hypot 1 (/ U (* J (* (cos (/ K 2)) 2))))))) |
| 75× | sqrt-prod |
| 52× | add-sqr-sqrt |
| 35× | sqrt-pow1 |
| 30× | pow1 |
| 19× | *-un-lft-identity pow1/2 add-cube-cbrt |
| 15× | swap-sqr |
| 9× | associate-*r* associate-*l* pow-prod-up unswap-sqr |
| 6× | add-cbrt-cube add-exp-log |
| 5× | pow-prod-down pow-sqr |
| 4× | expm1-log1p-u insert-posit16 log1p-expm1-u add-log-exp |
| 3× | rem-sqrt-square |
| 1× | pow2 rem-square-sqrt pow-plus sqrt-unprod prod-exp *-commutative cbrt-unprod |
| 13.0ms | (* (sqrt (sqrt (hypot 1 (/ U (* J (* (cos (/ K 2)) 2)))))) (sqrt (sqrt (hypot 1 (/ U (* J (* (cos (/ K 2)) 2))))))) |
| 7.0ms | (sqrt (hypot 1 (/ U (* J (* (cos (/ K 2)) 2))))) |
| 2.0ms | (sqrt (hypot 1 (/ U (* J (* (cos (/ K 2)) 2))))) |
| 2.0ms | (sqrt (hypot 1 (/ U (* J (* (cos (/ K 2)) 2))))) |
| 274.0ms | (sqrt (hypot 1 (/ U (* J (* (cos (/ K 2)) 2))))) |
| 241.0ms | (sqrt (hypot 1 (/ U (* J (* (cos (/ K 2)) 2))))) |
| 216.0ms | (* (sqrt (sqrt (hypot 1 (/ U (* J (* (cos (/ K 2)) 2)))))) (sqrt (sqrt (hypot 1 (/ U (* J (* (cos (/ K 2)) 2))))))) |
| 195.0ms | (sqrt (hypot 1 (/ U (* J (* (cos (/ K 2)) 2))))) |
8 alts after pruning (6 fresh and 2 done)
Merged error: 2.8b
Found 4 expressions with local error:
| 7.8b | (cbrt (hypot 1 (/ U (* J (* (cos (/ K 2)) 2))))) |
| 7.8b | (cbrt (hypot 1 (/ U (* J (* (cos (/ K 2)) 2))))) |
| 7.8b | (cbrt (hypot 1 (/ U (* J (* (cos (/ K 2)) 2))))) |
| 7.6b | (sqrt (hypot 1 (/ U (* J (* (cos (/ K 2)) 2))))) |
| 9× | cbrt-prod add-sqr-sqrt |
| 8× | *-un-lft-identity add-cube-cbrt |
| 5× | pow1 |
| 4× | expm1-log1p-u add-cbrt-cube add-exp-log insert-posit16 log1p-expm1-u add-log-exp |
| 3× | pow1/3 sqrt-prod |
| 1× | rem-sqrt-square sqrt-pow1 pow1/2 |
| 1.0ms | (sqrt (hypot 1 (/ U (* J (* (cos (/ K 2)) 2))))) |
| 1.0ms | (cbrt (hypot 1 (/ U (* J (* (cos (/ K 2)) 2))))) |
| 1.0ms | (cbrt (hypot 1 (/ U (* J (* (cos (/ K 2)) 2))))) |
| 1.0ms | (cbrt (hypot 1 (/ U (* J (* (cos (/ K 2)) 2))))) |
| 354.0ms | (cbrt (hypot 1 (/ U (* J (* (cos (/ K 2)) 2))))) |
| 342.0ms | (cbrt (hypot 1 (/ U (* J (* (cos (/ K 2)) 2))))) |
| 331.0ms | (cbrt (hypot 1 (/ U (* J (* (cos (/ K 2)) 2))))) |
| 227.0ms | (sqrt (hypot 1 (/ U (* J (* (cos (/ K 2)) 2))))) |
8 alts after pruning (5 fresh and 3 done)
Merged error: 2.8b
-18% (4.5b remaining)
Error of 8.4b against oracle of 3.8b and baseline of 7.7b
| 3.4s | 1526× | body | 1280 | valid |
| 1.4s | 1206× | body | 640 | valid |
| 1.2s | 4301× | body | 80 | valid |
| 573.0ms | 641× | body | 320 | valid |
| 163.0ms | 330× | body | 160 | valid |