Time bar (total: 54.1s)
1 alts after pruning (1 fresh and 0 done)
Merged error: 0.6b
Found 4 expressions with local error:
| 0.6b | (/.p16 (-.p16 beta alpha) (+.p16 (+.p16 alpha beta) (real->posit16 2.0))) |
| 0.3b | (+.p16 (/.p16 (-.p16 beta alpha) (+.p16 (+.p16 alpha beta) (real->posit16 2.0))) (real->posit16 1.0)) |
| 0.1b | (+.p16 (+.p16 alpha beta) (real->posit16 2.0)) |
| 0.0b | (/.p16 (+.p16 (/.p16 (-.p16 beta alpha) (+.p16 (+.p16 alpha beta) (real->posit16 2.0))) (real->posit16 1.0)) (real->posit16 2.0)) |
| 2× | +-commutative |
| 1× | associate-+l+ p16-flip-- associate-/l/ |
| 27.0ms | (/.p16 (+.p16 (/.p16 (-.p16 beta alpha) (+.p16 (+.p16 alpha beta) (real->posit16 2.0))) (real->posit16 1.0)) (real->posit16 2.0)) |
| 26.0ms | (/.p16 (-.p16 beta alpha) (+.p16 (+.p16 alpha beta) (real->posit16 2.0))) |
| 18.0ms | (+.p16 (+.p16 alpha beta) (real->posit16 2.0)) |
| 14.0ms | (+.p16 (/.p16 (-.p16 beta alpha) (+.p16 (+.p16 alpha beta) (real->posit16 2.0))) (real->posit16 1.0)) |
| 0.0ms | (/.p16 (-.p16 beta alpha) (+.p16 (+.p16 alpha beta) (real->posit16 2.0))) |
| 0.0ms | (+.p16 (/.p16 (-.p16 beta alpha) (+.p16 (+.p16 alpha beta) (real->posit16 2.0))) (real->posit16 1.0)) |
| 0.0ms | (/.p16 (+.p16 (/.p16 (-.p16 beta alpha) (+.p16 (+.p16 alpha beta) (real->posit16 2.0))) (real->posit16 1.0)) (real->posit16 2.0)) |
| 0.0ms | (+.p16 (+.p16 alpha beta) (real->posit16 2.0)) |
3 alts after pruning (2 fresh and 1 done)
Merged error: 0.5b
Found 4 expressions with local error:
| 0.6b | (/.p16 (-.p16 beta alpha) (+.p16 alpha (+.p16 beta (real->posit16 2.0)))) |
| 0.3b | (+.p16 (/.p16 (-.p16 beta alpha) (+.p16 alpha (+.p16 beta (real->posit16 2.0)))) (real->posit16 1.0)) |
| 0.2b | (+.p16 alpha (+.p16 beta (real->posit16 2.0))) |
| 0.0b | (/.p16 (+.p16 (/.p16 (-.p16 beta alpha) (+.p16 alpha (+.p16 beta (real->posit16 2.0)))) (real->posit16 1.0)) (real->posit16 2.0)) |
| 2× | +-commutative |
| 1× | associate-+r+ p16-flip-- associate-/l/ |
| 25.0ms | (/.p16 (+.p16 (/.p16 (-.p16 beta alpha) (+.p16 alpha (+.p16 beta (real->posit16 2.0)))) (real->posit16 1.0)) (real->posit16 2.0)) |
| 24.0ms | (+.p16 (/.p16 (-.p16 beta alpha) (+.p16 alpha (+.p16 beta (real->posit16 2.0)))) (real->posit16 1.0)) |
| 10.0ms | (/.p16 (-.p16 beta alpha) (+.p16 alpha (+.p16 beta (real->posit16 2.0)))) |
| 9.0ms | (+.p16 alpha (+.p16 beta (real->posit16 2.0))) |
| 0.0ms | (/.p16 (-.p16 beta alpha) (+.p16 alpha (+.p16 beta (real->posit16 2.0)))) |
| 0.0ms | (+.p16 (/.p16 (-.p16 beta alpha) (+.p16 alpha (+.p16 beta (real->posit16 2.0)))) (real->posit16 1.0)) |
| 0.0ms | (/.p16 (+.p16 (/.p16 (-.p16 beta alpha) (+.p16 alpha (+.p16 beta (real->posit16 2.0)))) (real->posit16 1.0)) (real->posit16 2.0)) |
| 0.0ms | (+.p16 alpha (+.p16 beta (real->posit16 2.0))) |
4 alts after pruning (2 fresh and 2 done)
Merged error: 0.5b
Found 4 expressions with local error:
| 1.1b | (/.p16 (-.p16 (*.p16 beta beta) (*.p16 alpha alpha)) (*.p16 (+.p16 (+.p16 alpha beta) (real->posit16 2.0)) (+.p16 beta alpha))) |
| 0.3b | (-.p16 (*.p16 beta beta) (*.p16 alpha alpha)) |
| 0.3b | (+.p16 (/.p16 (-.p16 (*.p16 beta beta) (*.p16 alpha alpha)) (*.p16 (+.p16 (+.p16 alpha beta) (real->posit16 2.0)) (+.p16 beta alpha))) (real->posit16 1.0)) |
| 0.2b | (*.p16 (+.p16 (+.p16 alpha beta) (real->posit16 2.0)) (+.p16 beta alpha)) |
| 3× | difference-of-squares |
| 2× | p16-flip-- |
| 1× | distribute-rgt-in +-commutative associate-/r* sub-neg distribute-lft-in p16-times-frac *-commutative associate-/l* associate-/l/ |
| 19.0ms | (+.p16 (/.p16 (-.p16 (*.p16 beta beta) (*.p16 alpha alpha)) (*.p16 (+.p16 (+.p16 alpha beta) (real->posit16 2.0)) (+.p16 beta alpha))) (real->posit16 1.0)) |
| 17.0ms | (*.p16 (+.p16 (+.p16 alpha beta) (real->posit16 2.0)) (+.p16 beta alpha)) |
| 8.0ms | (/.p16 (-.p16 (*.p16 beta beta) (*.p16 alpha alpha)) (*.p16 (+.p16 (+.p16 alpha beta) (real->posit16 2.0)) (+.p16 beta alpha))) |
| 6.0ms | (-.p16 (*.p16 beta beta) (*.p16 alpha alpha)) |
| 0.0ms | (/.p16 (-.p16 (*.p16 beta beta) (*.p16 alpha alpha)) (*.p16 (+.p16 (+.p16 alpha beta) (real->posit16 2.0)) (+.p16 beta alpha))) |
| 0.0ms | (+.p16 (/.p16 (-.p16 (*.p16 beta beta) (*.p16 alpha alpha)) (*.p16 (+.p16 (+.p16 alpha beta) (real->posit16 2.0)) (+.p16 beta alpha))) (real->posit16 1.0)) |
| 0.0ms | (-.p16 (*.p16 beta beta) (*.p16 alpha alpha)) |
| 0.0ms | (*.p16 (+.p16 (+.p16 alpha beta) (real->posit16 2.0)) (+.p16 beta alpha)) |
9 alts after pruning (7 fresh and 2 done)
Merged error: 0.4b
Found 4 expressions with local error:
| 0.7b | (/.p16 (-.p16 beta alpha) (+.p16 beta alpha)) |
| 0.4b | (*.p16 (/.p16 (+.p16 beta alpha) (+.p16 (+.p16 alpha beta) (real->posit16 2.0))) (/.p16 (-.p16 beta alpha) (+.p16 beta alpha))) |
| 0.4b | (/.p16 (+.p16 beta alpha) (+.p16 (+.p16 alpha beta) (real->posit16 2.0))) |
| 0.3b | (+.p16 (*.p16 (/.p16 (+.p16 beta alpha) (+.p16 (+.p16 alpha beta) (real->posit16 2.0))) (/.p16 (-.p16 beta alpha) (+.p16 beta alpha))) (real->posit16 1.0)) |
| 1× | +-commutative associate-*l/ associate-*r/ p16-flip-- *-commutative associate-/l/ |
| 9.0ms | (/.p16 (+.p16 beta alpha) (+.p16 (+.p16 alpha beta) (real->posit16 2.0))) |
| 5.0ms | (*.p16 (/.p16 (+.p16 beta alpha) (+.p16 (+.p16 alpha beta) (real->posit16 2.0))) (/.p16 (-.p16 beta alpha) (+.p16 beta alpha))) |
| 4.0ms | (+.p16 (*.p16 (/.p16 (+.p16 beta alpha) (+.p16 (+.p16 alpha beta) (real->posit16 2.0))) (/.p16 (-.p16 beta alpha) (+.p16 beta alpha))) (real->posit16 1.0)) |
| 4.0ms | (/.p16 (-.p16 beta alpha) (+.p16 beta alpha)) |
| 0.0ms | (/.p16 (-.p16 beta alpha) (+.p16 beta alpha)) |
| 0.0ms | (+.p16 (*.p16 (/.p16 (+.p16 beta alpha) (+.p16 (+.p16 alpha beta) (real->posit16 2.0))) (/.p16 (-.p16 beta alpha) (+.p16 beta alpha))) (real->posit16 1.0)) |
| 0.0ms | (*.p16 (/.p16 (+.p16 beta alpha) (+.p16 (+.p16 alpha beta) (real->posit16 2.0))) (/.p16 (-.p16 beta alpha) (+.p16 beta alpha))) |
| 0.0ms | (/.p16 (+.p16 beta alpha) (+.p16 (+.p16 alpha beta) (real->posit16 2.0))) |
9 alts after pruning (7 fresh and 2 done)
Merged error: 0.4b
-∞% (-63.3b remaining)
Error of 0.7b against oracle of 64.0b and baseline of 64.0b