Time bar (total: 15.0s)
| 543.0ms | (/.p16 (+.p16 (/.p16 (-.p16 beta alpha) (+.p16 (+.p16 alpha beta) (real->posit16 2.0))) (real->posit16 1.0)) (real->posit16 2.0)) |
1 alts after pruning (1 fresh and 0 done)
Merged error: 0.8b
Found 4 expressions with local error:
| 0.7b | (/.p16 (-.p16 beta alpha) (+.p16 (+.p16 alpha beta) (real->posit16 2.0))) |
| 0.4b | (+.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/ |
| 24.0ms | (+.p16 (/.p16 (-.p16 beta alpha) (+.p16 (+.p16 alpha beta) (real->posit16 2.0))) (real->posit16 1.0)) |
| 21.0ms | (/.p16 (+.p16 (/.p16 (-.p16 beta alpha) (+.p16 (+.p16 alpha beta) (real->posit16 2.0))) (real->posit16 1.0)) (real->posit16 2.0)) |
| 18.0ms | (+.p16 (+.p16 alpha beta) (real->posit16 2.0)) |
| 16.0ms | (/.p16 (-.p16 beta alpha) (+.p16 (+.p16 alpha beta) (real->posit16 2.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)) |
| 598.0ms | (/.p16 (+.p16 (/.p16 (-.p16 beta alpha) (+.p16 (+.p16 alpha beta) (real->posit16 2.0))) (real->posit16 1.0)) (real->posit16 2.0)) |
| 585.0ms | (/.p16 (+.p16 (/.p16 (-.p16 beta alpha) (+.p16 (+.p16 alpha beta) (real->posit16 2.0))) (real->posit16 1.0)) (real->posit16 2.0)) |
| 467.0ms | (/.p16 (+.p16 (/.p16 (-.p16 beta alpha) (+.p16 (+.p16 alpha beta) (real->posit16 2.0))) (real->posit16 1.0)) (real->posit16 2.0)) |
| 450.0ms | (/.p16 (+.p16 (/.p16 (-.p16 beta alpha) (+.p16 (+.p16 alpha beta) (real->posit16 2.0))) (real->posit16 1.0)) (real->posit16 2.0)) |
| 60.0ms | (*.p16 (+.p16 (+.p16 alpha beta) (real->posit16 2.0)) (+.p16 beta alpha)) |
3 alts after pruning (2 fresh and 1 done)
Merged error: 0.7b
Found 4 expressions with local error:
| 0.7b | (/.p16 (-.p16 beta alpha) (+.p16 alpha (+.p16 beta (real->posit16 2.0)))) |
| 0.4b | (+.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/ |
| 24.0ms | (+.p16 (/.p16 (-.p16 beta alpha) (+.p16 alpha (+.p16 beta (real->posit16 2.0)))) (real->posit16 1.0)) |
| 21.0ms | (/.p16 (+.p16 (/.p16 (-.p16 beta alpha) (+.p16 alpha (+.p16 beta (real->posit16 2.0)))) (real->posit16 1.0)) (real->posit16 2.0)) |
| 10.0ms | (+.p16 alpha (+.p16 beta (real->posit16 2.0))) |
| 9.0ms | (/.p16 (-.p16 beta alpha) (+.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 (-.p16 beta alpha) (+.p16 alpha (+.p16 beta (real->posit16 2.0)))) (real->posit16 1.0)) (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 alpha (+.p16 beta (real->posit16 2.0))) |
| 140.0ms | (*.p16 (+.p16 alpha (+.p16 beta (real->posit16 2.0))) (+.p16 beta alpha)) |
| 6.0ms | (+.p16 beta (real->posit16 2.0)) |
| 5.0ms | (+.p16 beta (real->posit16 2.0)) |
| 5.0ms | (+.p16 beta (real->posit16 2.0)) |
| 3.0ms | (+.p16 beta (real->posit16 2.0)) |
3 alts after pruning (1 fresh and 2 done)
Merged error: 0.7b
Found 4 expressions with local error:
| 1.3b | (/.p16 (-.p16 (*.p16 beta beta) (*.p16 alpha alpha)) (*.p16 (+.p16 beta alpha) (+.p16 (+.p16 beta alpha) (real->posit16 2.0)))) |
| 0.4b | (+.p16 (/.p16 (-.p16 (*.p16 beta beta) (*.p16 alpha alpha)) (*.p16 (+.p16 beta alpha) (+.p16 (+.p16 beta alpha) (real->posit16 2.0)))) (real->posit16 1.0)) |
| 0.3b | (*.p16 (+.p16 beta alpha) (+.p16 (+.p16 beta alpha) (real->posit16 2.0))) |
| 0.2b | (-.p16 (*.p16 beta beta) (*.p16 alpha 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/ |
| 21.0ms | (+.p16 (/.p16 (-.p16 (*.p16 beta beta) (*.p16 alpha alpha)) (*.p16 (+.p16 beta alpha) (+.p16 (+.p16 beta alpha) (real->posit16 2.0)))) (real->posit16 1.0)) |
| 18.0ms | (/.p16 (-.p16 (*.p16 beta beta) (*.p16 alpha alpha)) (*.p16 (+.p16 beta alpha) (+.p16 (+.p16 beta alpha) (real->posit16 2.0)))) |
| 13.0ms | (*.p16 (+.p16 beta alpha) (+.p16 (+.p16 beta alpha) (real->posit16 2.0))) |
| 3.0ms | (-.p16 (*.p16 beta beta) (*.p16 alpha alpha)) |
| 0.0ms | (/.p16 (-.p16 (*.p16 beta beta) (*.p16 alpha alpha)) (*.p16 (+.p16 beta alpha) (+.p16 (+.p16 beta alpha) (real->posit16 2.0)))) |
| 0.0ms | (+.p16 (/.p16 (-.p16 (*.p16 beta beta) (*.p16 alpha alpha)) (*.p16 (+.p16 beta alpha) (+.p16 (+.p16 beta alpha) (real->posit16 2.0)))) (real->posit16 1.0)) |
| 0.0ms | (*.p16 (+.p16 beta alpha) (+.p16 (+.p16 beta alpha) (real->posit16 2.0))) |
| 0.0ms | (-.p16 (*.p16 beta beta) (*.p16 alpha alpha)) |
| 774.0ms | (/.p16 (+.p16 (/.p16 (-.p16 (*.p16 beta beta) (*.p16 alpha alpha)) (*.p16 (+.p16 beta alpha) (+.p16 (+.p16 beta alpha) (real->posit16 2.0)))) (real->posit16 1.0)) (real->posit16 2.0)) |
| 772.0ms | (/.p16 (+.p16 (/.p16 (-.p16 (*.p16 beta beta) (*.p16 alpha alpha)) (*.p16 (+.p16 beta alpha) (+.p16 (+.p16 beta alpha) (real->posit16 2.0)))) (real->posit16 1.0)) (real->posit16 2.0)) |
| 602.0ms | (/.p16 (+.p16 (/.p16 (-.p16 (*.p16 beta beta) (*.p16 alpha alpha)) (*.p16 (+.p16 beta alpha) (+.p16 (+.p16 beta alpha) (real->posit16 2.0)))) (real->posit16 1.0)) (real->posit16 2.0)) |
| 477.0ms | (/.p16 (+.p16 (/.p16 (-.p16 (*.p16 beta beta) (*.p16 alpha alpha)) (*.p16 (+.p16 beta alpha) (+.p16 (+.p16 beta alpha) (real->posit16 2.0)))) (real->posit16 1.0)) (real->posit16 2.0)) |
| 216.0ms | (*.p16 (*.p16 (+.p16 beta alpha) (+.p16 (+.p16 beta alpha) (real->posit16 2.0))) (+.p16 (*.p16 beta beta) (*.p16 alpha alpha))) |
7 alts after pruning (5 fresh and 2 done)
Merged error: 0.6b
Found 4 expressions with local error:
| 1.3b | (/.p16 (*.p16 (+.p16 beta alpha) (-.p16 beta alpha)) (*.p16 (+.p16 beta alpha) (+.p16 (+.p16 beta alpha) (real->posit16 2.0)))) |
| 0.4b | (+.p16 (/.p16 (*.p16 (+.p16 beta alpha) (-.p16 beta alpha)) (*.p16 (+.p16 beta alpha) (+.p16 (+.p16 beta alpha) (real->posit16 2.0)))) (real->posit16 1.0)) |
| 0.3b | (*.p16 (+.p16 beta alpha) (+.p16 (+.p16 beta alpha) (real->posit16 2.0))) |
| 0.1b | (*.p16 (+.p16 beta alpha) (-.p16 beta alpha)) |
| 2× | distribute-rgt-in sub-neg distribute-lft-in associate-*r/ p16-flip-- *-commutative |
| 1× | +-commutative associate-/r* p16-times-frac associate-/l* associate-/l/ |
| 8.0ms | (*.p16 (+.p16 beta alpha) (+.p16 (+.p16 beta alpha) (real->posit16 2.0))) |
| 6.0ms | (+.p16 (/.p16 (*.p16 (+.p16 beta alpha) (-.p16 beta alpha)) (*.p16 (+.p16 beta alpha) (+.p16 (+.p16 beta alpha) (real->posit16 2.0)))) (real->posit16 1.0)) |
| 6.0ms | (*.p16 (+.p16 beta alpha) (-.p16 beta alpha)) |
| 4.0ms | (/.p16 (*.p16 (+.p16 beta alpha) (-.p16 beta alpha)) (*.p16 (+.p16 beta alpha) (+.p16 (+.p16 beta alpha) (real->posit16 2.0)))) |
| 0.0ms | (/.p16 (*.p16 (+.p16 beta alpha) (-.p16 beta alpha)) (*.p16 (+.p16 beta alpha) (+.p16 (+.p16 beta alpha) (real->posit16 2.0)))) |
| 0.0ms | (+.p16 (/.p16 (*.p16 (+.p16 beta alpha) (-.p16 beta alpha)) (*.p16 (+.p16 beta alpha) (+.p16 (+.p16 beta alpha) (real->posit16 2.0)))) (real->posit16 1.0)) |
| 0.0ms | (*.p16 (+.p16 beta alpha) (+.p16 (+.p16 beta alpha) (real->posit16 2.0))) |
| 0.0ms | (*.p16 (+.p16 beta alpha) (-.p16 beta alpha)) |
| 225.0ms | (/.p16 (*.p16 (+.p16 beta alpha) (+.p16 (+.p16 beta alpha) (real->posit16 2.0))) (-.p16 beta alpha)) |
| 72.0ms | (*.p16 (*.p16 (+.p16 beta alpha) (+.p16 (+.p16 beta alpha) (real->posit16 2.0))) (+.p16 beta alpha)) |
| 49.0ms | (/.p16 (*.p16 (+.p16 beta alpha) (-.p16 beta alpha)) (+.p16 beta alpha)) |
| 38.0ms | (*.p16 (+.p16 beta alpha) (-.p16 (*.p16 beta beta) (*.p16 alpha alpha))) |
| 32.0ms | (/.p16 (-.p16 beta alpha) (+.p16 (+.p16 beta alpha) (real->posit16 2.0))) |
7 alts after pruning (5 fresh and 2 done)
Merged error: 0.6b
-∞% (-63.3b remaining)
Error of 0.7b against oracle of 64.0b and baseline of 64.0b