Time bar (total: 44.2s)
2 alts after pruning (2 fresh and 0 done)
Merged error: 3.1b
Found 4 expressions with local error:
| 3.3b | (/.p16 (*.p16 (*.p16 i (+.p16 (+.p16 alpha beta) i)) (+.p16 (*.p16 beta alpha) (*.p16 i (+.p16 (+.p16 alpha beta) i)))) (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)))) |
| 1.4b | (/.p16 (/.p16 (*.p16 (*.p16 i (+.p16 (+.p16 alpha beta) i)) (+.p16 (*.p16 beta alpha) (*.p16 i (+.p16 (+.p16 alpha beta) i)))) (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)))) (-.p16 (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i))) (real->posit16 1.0))) |
| 0.2b | (+.p16 (*.p16 beta alpha) (*.p16 i (+.p16 (+.p16 alpha beta) i))) |
| 0.2b | (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) |
| 4× | p16-times-frac |
| 2× | +-commutative associate-+r+ associate-/r* difference-of-sqr-1 associate-/l* |
| 1× | distribute-rgt-in associate-+l+ distribute-lft-in p16-flip-- associate-/r/ associate-/l/ |
| 11.0ms | (/.p16 (*.p16 (*.p16 i (+.p16 (+.p16 alpha beta) i)) (+.p16 (*.p16 beta alpha) (*.p16 i (+.p16 (+.p16 alpha beta) i)))) (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)))) |
| 10.0ms | (/.p16 (/.p16 (*.p16 (*.p16 i (+.p16 (+.p16 alpha beta) i)) (+.p16 (*.p16 beta alpha) (*.p16 i (+.p16 (+.p16 alpha beta) i)))) (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)))) (-.p16 (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i))) (real->posit16 1.0))) |
| 9.0ms | (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) |
| 3.0ms | (+.p16 (*.p16 beta alpha) (*.p16 i (+.p16 (+.p16 alpha beta) i))) |
| 0.0ms | (/.p16 (*.p16 (*.p16 i (+.p16 (+.p16 alpha beta) i)) (+.p16 (*.p16 beta alpha) (*.p16 i (+.p16 (+.p16 alpha beta) i)))) (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)))) |
| 0.0ms | (/.p16 (/.p16 (*.p16 (*.p16 i (+.p16 (+.p16 alpha beta) i)) (+.p16 (*.p16 beta alpha) (*.p16 i (+.p16 (+.p16 alpha beta) i)))) (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)))) (-.p16 (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i))) (real->posit16 1.0))) |
| 0.0ms | (+.p16 (*.p16 beta alpha) (*.p16 i (+.p16 (+.p16 alpha beta) i))) |
| 0.0ms | (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) |
8 alts after pruning (8 fresh and 0 done)
Merged error: 0.8b
Found 4 expressions with local error:
| 1.3b | (/.p16 (+.p16 (*.p16 beta alpha) (*.p16 i (+.p16 (+.p16 alpha beta) i))) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i))) |
| 1.3b | (/.p16 (*.p16 i (+.p16 (+.p16 alpha beta) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i))) |
| 0.8b | (/.p16 (/.p16 (+.p16 (*.p16 beta alpha) (*.p16 i (+.p16 (+.p16 alpha beta) i))) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i))) (-.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (real->posit16 1.0))) |
| 0.7b | (/.p16 (/.p16 (*.p16 i (+.p16 (+.p16 alpha beta) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i))) (+.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (real->posit16 1.0))) |
| 2× | associate-/l/ |
| 1× | p16-flip-- associate-/r/ associate-/l* |
| 38.0ms | (/.p16 (/.p16 (*.p16 i (+.p16 (+.p16 alpha beta) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i))) (+.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (real->posit16 1.0))) |
| 25.0ms | (/.p16 (*.p16 i (+.p16 (+.p16 alpha beta) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i))) |
| 21.0ms | (/.p16 (/.p16 (+.p16 (*.p16 beta alpha) (*.p16 i (+.p16 (+.p16 alpha beta) i))) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i))) (-.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (real->posit16 1.0))) |
| 7.0ms | (/.p16 (+.p16 (*.p16 beta alpha) (*.p16 i (+.p16 (+.p16 alpha beta) i))) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i))) |
| 0.0ms | (/.p16 (+.p16 (*.p16 beta alpha) (*.p16 i (+.p16 (+.p16 alpha beta) i))) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i))) |
| 0.0ms | (/.p16 (/.p16 (+.p16 (*.p16 beta alpha) (*.p16 i (+.p16 (+.p16 alpha beta) i))) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i))) (-.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (real->posit16 1.0))) |
| 0.0ms | (/.p16 (/.p16 (*.p16 i (+.p16 (+.p16 alpha beta) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i))) (+.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (real->posit16 1.0))) |
| 0.0ms | (/.p16 (*.p16 i (+.p16 (+.p16 alpha beta) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i))) |
12 alts after pruning (11 fresh and 1 done)
Merged error: 0.5b
Found 4 expressions with local error:
| 1.3b | (/.p16 (+.p16 (*.p16 beta alpha) (*.p16 i (+.p16 (+.p16 alpha beta) i))) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i))) |
| 1.2b | (/.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (+.p16 (+.p16 alpha beta) i)) |
| 0.8b | (/.p16 (/.p16 (+.p16 (*.p16 beta alpha) (*.p16 i (+.p16 (+.p16 alpha beta) i))) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i))) (-.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (real->posit16 1.0))) |
| 0.7b | (/.p16 (/.p16 i (/.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (+.p16 (+.p16 alpha beta) i))) (+.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (real->posit16 1.0))) |
| 2× | associate-/r/ associate-/l/ |
| 1× | p16-flip-- associate-/l* |
| 51.0ms | (/.p16 (/.p16 i (/.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (+.p16 (+.p16 alpha beta) i))) (+.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (real->posit16 1.0))) |
| 24.0ms | (/.p16 (/.p16 (+.p16 (*.p16 beta alpha) (*.p16 i (+.p16 (+.p16 alpha beta) i))) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i))) (-.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (real->posit16 1.0))) |
| 16.0ms | (/.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (+.p16 (+.p16 alpha beta) i)) |
| 6.0ms | (/.p16 (+.p16 (*.p16 beta alpha) (*.p16 i (+.p16 (+.p16 alpha beta) i))) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i))) |
| 0.0ms | (/.p16 (+.p16 (*.p16 beta alpha) (*.p16 i (+.p16 (+.p16 alpha beta) i))) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i))) |
| 0.0ms | (/.p16 (/.p16 (+.p16 (*.p16 beta alpha) (*.p16 i (+.p16 (+.p16 alpha beta) i))) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i))) (-.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (real->posit16 1.0))) |
| 0.0ms | (/.p16 (/.p16 i (/.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (+.p16 (+.p16 alpha beta) i))) (+.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (real->posit16 1.0))) |
| 0.0ms | (/.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (+.p16 (+.p16 alpha beta) i)) |
16 alts after pruning (14 fresh and 2 done)
Merged error: 0.5b
Found 4 expressions with local error:
| 1.3b | (/.p16 (+.p16 (*.p16 beta alpha) (*.p16 i (+.p16 (+.p16 alpha beta) i))) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i))) |
| 1.2b | (/.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (+.p16 (+.p16 alpha beta) i)) |
| 0.8b | (/.p16 i (*.p16 (+.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (real->posit16 1.0)) (/.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (+.p16 (+.p16 alpha beta) i)))) |
| 0.8b | (/.p16 (/.p16 (+.p16 (*.p16 beta alpha) (*.p16 i (+.p16 (+.p16 alpha beta) i))) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i))) (-.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (real->posit16 1.0))) |
| 2× | associate-/r/ |
| 1× | associate-/r* associate-*r/ p16-flip-- associate-/l/ |
| 43.0ms | (/.p16 (/.p16 (+.p16 (*.p16 beta alpha) (*.p16 i (+.p16 (+.p16 alpha beta) i))) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i))) (-.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (real->posit16 1.0))) |
| 33.0ms | (/.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (+.p16 (+.p16 alpha beta) i)) |
| 22.0ms | (/.p16 (+.p16 (*.p16 beta alpha) (*.p16 i (+.p16 (+.p16 alpha beta) i))) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i))) |
| 5.0ms | (/.p16 i (*.p16 (+.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (real->posit16 1.0)) (/.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (+.p16 (+.p16 alpha beta) i)))) |
| 0.0ms | (/.p16 (+.p16 (*.p16 beta alpha) (*.p16 i (+.p16 (+.p16 alpha beta) i))) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i))) |
| 0.0ms | (/.p16 (/.p16 (+.p16 (*.p16 beta alpha) (*.p16 i (+.p16 (+.p16 alpha beta) i))) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i))) (-.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (real->posit16 1.0))) |
| 0.0ms | (/.p16 i (*.p16 (+.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (real->posit16 1.0)) (/.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (+.p16 (+.p16 alpha beta) i)))) |
| 0.0ms | (/.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (+.p16 (+.p16 alpha beta) i)) |
18 alts after pruning (15 fresh and 3 done)
Merged error: 0.5b
-∞% (-62.5b remaining)
Error of 1.5b against oracle of 64.0b and baseline of 64.0b