Time bar (total: 31.1s)
2 alts after pruning (2 fresh and 0 done)
Merged error: 3.2b
Found 4 expressions with local error:
| 2.9b | (/.p16 (+.p16 (+.p16 (*.p16 (*.p16 (*.p16 x x) (*.p16 x x)) (+.p16 (*.p16 (*.p16 (*.p16 x x) (*.p16 x x)) (+.p16 (*.p16 (*.p16 x x) (real->posit16 0.0001789971)) (real->posit16 0.0005064034))) (+.p16 (real->posit16 0.0424060604) (*.p16 (real->posit16 0.0072644182) (*.p16 x x))))) (real->posit16 1)) (*.p16 (*.p16 x x) (real->posit16 0.1049934947))) (+.p16 (+.p16 (*.p16 (*.p16 (*.p16 (*.p16 x x) (*.p16 x x)) (*.p16 (*.p16 x x) (*.p16 x x))) (+.p16 (*.p16 (*.p16 x x) (+.p16 (*.p16 (real->posit16 0.0001789971) (*.p16 (real->posit16 2) (*.p16 x x))) (real->posit16 0.0008327945))) (real->posit16 0.0140005442))) (*.p16 (*.p16 (*.p16 x x) (*.p16 x x)) (+.p16 (*.p16 (*.p16 x x) (real->posit16 0.0694555761)) (real->posit16 0.2909738639)))) (+.p16 (real->posit16 1) (*.p16 (*.p16 x x) (real->posit16 0.7715471019))))) |
| 0.8b | (*.p16 (real->posit16 0.0001789971) (*.p16 (real->posit16 2) (*.p16 x x))) |
| 0.7b | (*.p16 (*.p16 x x) (real->posit16 0.0001789971)) |
| 0.5b | (*.p16 (*.p16 (*.p16 x x) (*.p16 x x)) (+.p16 (*.p16 (*.p16 x x) (real->posit16 0.0001789971)) (real->posit16 0.0005064034))) |
| 3× | *-commutative |
| 2× | associate-*l* |
| 1× | distribute-rgt-in distribute-lft-in associate-*r* |
| 20.0ms | (*.p16 (*.p16 (*.p16 x x) (*.p16 x x)) (+.p16 (*.p16 (*.p16 x x) (real->posit16 0.0001789971)) (real->posit16 0.0005064034))) |
| 16.0ms | (/.p16 (+.p16 (+.p16 (*.p16 (*.p16 (*.p16 x x) (*.p16 x x)) (+.p16 (*.p16 (*.p16 (*.p16 x x) (*.p16 x x)) (+.p16 (*.p16 (*.p16 x x) (real->posit16 0.0001789971)) (real->posit16 0.0005064034))) (+.p16 (real->posit16 0.0424060604) (*.p16 (real->posit16 0.0072644182) (*.p16 x x))))) (real->posit16 1)) (*.p16 (*.p16 x x) (real->posit16 0.1049934947))) (+.p16 (+.p16 (*.p16 (*.p16 (*.p16 (*.p16 x x) (*.p16 x x)) (*.p16 (*.p16 x x) (*.p16 x x))) (+.p16 (*.p16 (*.p16 x x) (+.p16 (*.p16 (real->posit16 0.0001789971) (*.p16 (real->posit16 2) (*.p16 x x))) (real->posit16 0.0008327945))) (real->posit16 0.0140005442))) (*.p16 (*.p16 (*.p16 x x) (*.p16 x x)) (+.p16 (*.p16 (*.p16 x x) (real->posit16 0.0694555761)) (real->posit16 0.2909738639)))) (+.p16 (real->posit16 1) (*.p16 (*.p16 x x) (real->posit16 0.7715471019))))) |
| 13.0ms | (*.p16 (real->posit16 0.0001789971) (*.p16 (real->posit16 2) (*.p16 x x))) |
| 6.0ms | (*.p16 (*.p16 x x) (real->posit16 0.0001789971)) |
| 0.0ms | (/.p16 (+.p16 (+.p16 (*.p16 (*.p16 (*.p16 x x) (*.p16 x x)) (+.p16 (*.p16 (*.p16 (*.p16 x x) (*.p16 x x)) (+.p16 (*.p16 (*.p16 x x) (real->posit16 0.0001789971)) (real->posit16 0.0005064034))) (+.p16 (real->posit16 0.0424060604) (*.p16 (real->posit16 0.0072644182) (*.p16 x x))))) (real->posit16 1)) (*.p16 (*.p16 x x) (real->posit16 0.1049934947))) (+.p16 (+.p16 (*.p16 (*.p16 (*.p16 (*.p16 x x) (*.p16 x x)) (*.p16 (*.p16 x x) (*.p16 x x))) (+.p16 (*.p16 (*.p16 x x) (+.p16 (*.p16 (real->posit16 0.0001789971) (*.p16 (real->posit16 2) (*.p16 x x))) (real->posit16 0.0008327945))) (real->posit16 0.0140005442))) (*.p16 (*.p16 (*.p16 x x) (*.p16 x x)) (+.p16 (*.p16 (*.p16 x x) (real->posit16 0.0694555761)) (real->posit16 0.2909738639)))) (+.p16 (real->posit16 1) (*.p16 (*.p16 x x) (real->posit16 0.7715471019))))) |
| 0.0ms | (*.p16 (*.p16 (*.p16 x x) (*.p16 x x)) (+.p16 (*.p16 (*.p16 x x) (real->posit16 0.0001789971)) (real->posit16 0.0005064034))) |
| 0.0ms | (*.p16 (real->posit16 0.0001789971) (*.p16 (real->posit16 2) (*.p16 x x))) |
| 0.0ms | (*.p16 (*.p16 x x) (real->posit16 0.0001789971)) |
5 alts after pruning (5 fresh and 0 done)
Merged error: 2.9b
Found 4 expressions with local error:
| 3.0b | (/.p16 (*.p16 x (+.p16 (+.p16 (real->posit16 1) (*.p16 (real->posit16 0.1049934947) (*.p16 x x))) (*.p16 (*.p16 (*.p16 x x) (*.p16 x x)) (+.p16 (*.p16 (*.p16 x x) (+.p16 (real->posit16 0.0072644182) (+.p16 (*.p16 (*.p16 (*.p16 x x) (*.p16 x x)) (real->posit16 0.0001789971)) (*.p16 (*.p16 x x) (real->posit16 0.0005064034))))) (real->posit16 0.0424060604))))) (+.p16 (*.p16 (*.p16 (*.p16 x x) (*.p16 x x)) (+.p16 (+.p16 (*.p16 (real->posit16 0.0694555761) (*.p16 x x)) (real->posit16 0.2909738639)) (*.p16 (*.p16 (*.p16 x x) (*.p16 x x)) (+.p16 (*.p16 (*.p16 x x) (+.p16 (*.p16 (real->posit16 0.0001789971) (*.p16 (*.p16 x x) (real->posit16 2))) (real->posit16 0.0008327945))) (real->posit16 0.0140005442))))) (+.p16 (*.p16 (real->posit16 0.7715471019) (*.p16 x x)) (real->posit16 1)))) |
| 1.1b | (*.p16 (*.p16 (*.p16 x x) (*.p16 x x)) (real->posit16 0.0001789971)) |
| 0.9b | (*.p16 (*.p16 x x) (real->posit16 0.0005064034)) |
| 0.8b | (*.p16 (real->posit16 0.0001789971) (*.p16 (*.p16 x x) (real->posit16 2))) |
| 3× | *-commutative |
| 2× | associate-*l* |
| 1× | associate-*r* associate-/l* |
| 10.0ms | (/.p16 (*.p16 x (+.p16 (+.p16 (real->posit16 1) (*.p16 (real->posit16 0.1049934947) (*.p16 x x))) (*.p16 (*.p16 (*.p16 x x) (*.p16 x x)) (+.p16 (*.p16 (*.p16 x x) (+.p16 (real->posit16 0.0072644182) (+.p16 (*.p16 (*.p16 (*.p16 x x) (*.p16 x x)) (real->posit16 0.0001789971)) (*.p16 (*.p16 x x) (real->posit16 0.0005064034))))) (real->posit16 0.0424060604))))) (+.p16 (*.p16 (*.p16 (*.p16 x x) (*.p16 x x)) (+.p16 (+.p16 (*.p16 (real->posit16 0.0694555761) (*.p16 x x)) (real->posit16 0.2909738639)) (*.p16 (*.p16 (*.p16 x x) (*.p16 x x)) (+.p16 (*.p16 (*.p16 x x) (+.p16 (*.p16 (real->posit16 0.0001789971) (*.p16 (*.p16 x x) (real->posit16 2))) (real->posit16 0.0008327945))) (real->posit16 0.0140005442))))) (+.p16 (*.p16 (real->posit16 0.7715471019) (*.p16 x x)) (real->posit16 1)))) |
| 9.0ms | (*.p16 (*.p16 (*.p16 x x) (*.p16 x x)) (real->posit16 0.0001789971)) |
| 6.0ms | (*.p16 (real->posit16 0.0001789971) (*.p16 (*.p16 x x) (real->posit16 2))) |
| 4.0ms | (*.p16 (*.p16 x x) (real->posit16 0.0005064034)) |
| 0.0ms | (/.p16 (*.p16 x (+.p16 (+.p16 (real->posit16 1) (*.p16 (real->posit16 0.1049934947) (*.p16 x x))) (*.p16 (*.p16 (*.p16 x x) (*.p16 x x)) (+.p16 (*.p16 (*.p16 x x) (+.p16 (real->posit16 0.0072644182) (+.p16 (*.p16 (*.p16 (*.p16 x x) (*.p16 x x)) (real->posit16 0.0001789971)) (*.p16 (*.p16 x x) (real->posit16 0.0005064034))))) (real->posit16 0.0424060604))))) (+.p16 (*.p16 (*.p16 (*.p16 x x) (*.p16 x x)) (+.p16 (+.p16 (*.p16 (real->posit16 0.0694555761) (*.p16 x x)) (real->posit16 0.2909738639)) (*.p16 (*.p16 (*.p16 x x) (*.p16 x x)) (+.p16 (*.p16 (*.p16 x x) (+.p16 (*.p16 (real->posit16 0.0001789971) (*.p16 (*.p16 x x) (real->posit16 2))) (real->posit16 0.0008327945))) (real->posit16 0.0140005442))))) (+.p16 (*.p16 (real->posit16 0.7715471019) (*.p16 x x)) (real->posit16 1)))) |
| 0.0ms | (*.p16 (*.p16 (*.p16 x x) (*.p16 x x)) (real->posit16 0.0001789971)) |
| 0.0ms | (*.p16 (real->posit16 0.0001789971) (*.p16 (*.p16 x x) (real->posit16 2))) |
| 0.0ms | (*.p16 (*.p16 x x) (real->posit16 0.0005064034)) |
7 alts after pruning (7 fresh and 0 done)
Merged error: 2.7b
Found 4 expressions with local error:
| 3.0b | (/.p16 (*.p16 x (+.p16 (+.p16 (real->posit16 1) (*.p16 (real->posit16 0.1049934947) (*.p16 x x))) (*.p16 (*.p16 (*.p16 x x) (*.p16 x x)) (+.p16 (*.p16 (*.p16 x x) (+.p16 (real->posit16 0.0072644182) (+.p16 (*.p16 (*.p16 (*.p16 x x) (*.p16 x x)) (real->posit16 0.0001789971)) (*.p16 x (*.p16 x (real->posit16 0.0005064034)))))) (real->posit16 0.0424060604))))) (+.p16 (*.p16 (*.p16 (*.p16 x x) (*.p16 x x)) (+.p16 (+.p16 (*.p16 (real->posit16 0.0694555761) (*.p16 x x)) (real->posit16 0.2909738639)) (*.p16 (*.p16 (*.p16 x x) (*.p16 x x)) (+.p16 (*.p16 (*.p16 x x) (+.p16 (*.p16 (real->posit16 0.0001789971) (*.p16 (*.p16 x x) (real->posit16 2))) (real->posit16 0.0008327945))) (real->posit16 0.0140005442))))) (+.p16 (*.p16 (real->posit16 0.7715471019) (*.p16 x x)) (real->posit16 1)))) |
| 1.1b | (*.p16 (*.p16 (*.p16 x x) (*.p16 x x)) (real->posit16 0.0001789971)) |
| 0.8b | (*.p16 (real->posit16 0.0001789971) (*.p16 (*.p16 x x) (real->posit16 2))) |
| 0.6b | (*.p16 x (real->posit16 0.0005064034)) |
| 3× | *-commutative |
| 1× | associate-*r* associate-*l* associate-/l* |
| 15.0ms | (*.p16 (*.p16 (*.p16 x x) (*.p16 x x)) (real->posit16 0.0001789971)) |
| 10.0ms | (/.p16 (*.p16 x (+.p16 (+.p16 (real->posit16 1) (*.p16 (real->posit16 0.1049934947) (*.p16 x x))) (*.p16 (*.p16 (*.p16 x x) (*.p16 x x)) (+.p16 (*.p16 (*.p16 x x) (+.p16 (real->posit16 0.0072644182) (+.p16 (*.p16 (*.p16 (*.p16 x x) (*.p16 x x)) (real->posit16 0.0001789971)) (*.p16 x (*.p16 x (real->posit16 0.0005064034)))))) (real->posit16 0.0424060604))))) (+.p16 (*.p16 (*.p16 (*.p16 x x) (*.p16 x x)) (+.p16 (+.p16 (*.p16 (real->posit16 0.0694555761) (*.p16 x x)) (real->posit16 0.2909738639)) (*.p16 (*.p16 (*.p16 x x) (*.p16 x x)) (+.p16 (*.p16 (*.p16 x x) (+.p16 (*.p16 (real->posit16 0.0001789971) (*.p16 (*.p16 x x) (real->posit16 2))) (real->posit16 0.0008327945))) (real->posit16 0.0140005442))))) (+.p16 (*.p16 (real->posit16 0.7715471019) (*.p16 x x)) (real->posit16 1)))) |
| 6.0ms | (*.p16 (real->posit16 0.0001789971) (*.p16 (*.p16 x x) (real->posit16 2))) |
| 2.0ms | (*.p16 x (real->posit16 0.0005064034)) |
| 0.0ms | (/.p16 (*.p16 x (+.p16 (+.p16 (real->posit16 1) (*.p16 (real->posit16 0.1049934947) (*.p16 x x))) (*.p16 (*.p16 (*.p16 x x) (*.p16 x x)) (+.p16 (*.p16 (*.p16 x x) (+.p16 (real->posit16 0.0072644182) (+.p16 (*.p16 (*.p16 (*.p16 x x) (*.p16 x x)) (real->posit16 0.0001789971)) (*.p16 x (*.p16 x (real->posit16 0.0005064034)))))) (real->posit16 0.0424060604))))) (+.p16 (*.p16 (*.p16 (*.p16 x x) (*.p16 x x)) (+.p16 (+.p16 (*.p16 (real->posit16 0.0694555761) (*.p16 x x)) (real->posit16 0.2909738639)) (*.p16 (*.p16 (*.p16 x x) (*.p16 x x)) (+.p16 (*.p16 (*.p16 x x) (+.p16 (*.p16 (real->posit16 0.0001789971) (*.p16 (*.p16 x x) (real->posit16 2))) (real->posit16 0.0008327945))) (real->posit16 0.0140005442))))) (+.p16 (*.p16 (real->posit16 0.7715471019) (*.p16 x x)) (real->posit16 1)))) |
| 0.0ms | (*.p16 (real->posit16 0.0001789971) (*.p16 (*.p16 x x) (real->posit16 2))) |
| 0.0ms | (*.p16 x (real->posit16 0.0005064034)) |
| 0.0ms | (*.p16 (*.p16 (*.p16 x x) (*.p16 x x)) (real->posit16 0.0001789971)) |
7 alts after pruning (6 fresh and 1 done)
Merged error: 2.7b
Found 4 expressions with local error:
| 2.7b | (*.p16 (/.p16 x (+.p16 (real->posit16 1) (*.p16 (*.p16 x x) (+.p16 (real->posit16 0.7715471019) (*.p16 (*.p16 x x) (+.p16 (*.p16 (*.p16 x x) (+.p16 (*.p16 (+.p16 (real->posit16 0.0140005442) (*.p16 (+.p16 (*.p16 (*.p16 (*.p16 x x) (real->posit16 0.0001789971)) (real->posit16 2)) (real->posit16 0.0008327945)) (*.p16 x x))) (*.p16 x x)) (real->posit16 0.0694555761))) (real->posit16 0.2909738639))))))) (+.p16 (*.p16 (+.p16 (real->posit16 0.1049934947) (*.p16 (+.p16 (real->posit16 0.0424060604) (*.p16 (+.p16 (*.p16 (*.p16 x x) (+.p16 (*.p16 (*.p16 x x) (real->posit16 0.0001789971)) (real->posit16 0.0005064034))) (real->posit16 0.0072644182)) (*.p16 x x))) (*.p16 x x))) (*.p16 x x)) (real->posit16 1))) |
| 0.8b | (/.p16 x (+.p16 (real->posit16 1) (*.p16 (*.p16 x x) (+.p16 (real->posit16 0.7715471019) (*.p16 (*.p16 x x) (+.p16 (*.p16 (*.p16 x x) (+.p16 (*.p16 (+.p16 (real->posit16 0.0140005442) (*.p16 (+.p16 (*.p16 (*.p16 (*.p16 x x) (real->posit16 0.0001789971)) (real->posit16 2)) (real->posit16 0.0008327945)) (*.p16 x x))) (*.p16 x x)) (real->posit16 0.0694555761))) (real->posit16 0.2909738639))))))) |
| 0.7b | (*.p16 (*.p16 x x) (real->posit16 0.0001789971)) |
| 0.7b | (*.p16 (*.p16 x x) (real->posit16 0.0001789971)) |
| 3× | *-commutative |
| 2× | associate-*l* |
| 1× | distribute-rgt-in distribute-lft-in associate-*l/ |
| 4.0ms | (*.p16 (*.p16 x x) (real->posit16 0.0001789971)) |
| 3.0ms | (*.p16 (*.p16 x x) (real->posit16 0.0001789971)) |
| 3.0ms | (*.p16 (/.p16 x (+.p16 (real->posit16 1) (*.p16 (*.p16 x x) (+.p16 (real->posit16 0.7715471019) (*.p16 (*.p16 x x) (+.p16 (*.p16 (*.p16 x x) (+.p16 (*.p16 (+.p16 (real->posit16 0.0140005442) (*.p16 (+.p16 (*.p16 (*.p16 (*.p16 x x) (real->posit16 0.0001789971)) (real->posit16 2)) (real->posit16 0.0008327945)) (*.p16 x x))) (*.p16 x x)) (real->posit16 0.0694555761))) (real->posit16 0.2909738639))))))) (+.p16 (*.p16 (+.p16 (real->posit16 0.1049934947) (*.p16 (+.p16 (real->posit16 0.0424060604) (*.p16 (+.p16 (*.p16 (*.p16 x x) (+.p16 (*.p16 (*.p16 x x) (real->posit16 0.0001789971)) (real->posit16 0.0005064034))) (real->posit16 0.0072644182)) (*.p16 x x))) (*.p16 x x))) (*.p16 x x)) (real->posit16 1))) |
| 2.0ms | (/.p16 x (+.p16 (real->posit16 1) (*.p16 (*.p16 x x) (+.p16 (real->posit16 0.7715471019) (*.p16 (*.p16 x x) (+.p16 (*.p16 (*.p16 x x) (+.p16 (*.p16 (+.p16 (real->posit16 0.0140005442) (*.p16 (+.p16 (*.p16 (*.p16 (*.p16 x x) (real->posit16 0.0001789971)) (real->posit16 2)) (real->posit16 0.0008327945)) (*.p16 x x))) (*.p16 x x)) (real->posit16 0.0694555761))) (real->posit16 0.2909738639))))))) |
| 0.0ms | (*.p16 (/.p16 x (+.p16 (real->posit16 1) (*.p16 (*.p16 x x) (+.p16 (real->posit16 0.7715471019) (*.p16 (*.p16 x x) (+.p16 (*.p16 (*.p16 x x) (+.p16 (*.p16 (+.p16 (real->posit16 0.0140005442) (*.p16 (+.p16 (*.p16 (*.p16 (*.p16 x x) (real->posit16 0.0001789971)) (real->posit16 2)) (real->posit16 0.0008327945)) (*.p16 x x))) (*.p16 x x)) (real->posit16 0.0694555761))) (real->posit16 0.2909738639))))))) (+.p16 (*.p16 (+.p16 (real->posit16 0.1049934947) (*.p16 (+.p16 (real->posit16 0.0424060604) (*.p16 (+.p16 (*.p16 (*.p16 x x) (+.p16 (*.p16 (*.p16 x x) (real->posit16 0.0001789971)) (real->posit16 0.0005064034))) (real->posit16 0.0072644182)) (*.p16 x x))) (*.p16 x x))) (*.p16 x x)) (real->posit16 1))) |
| 0.0ms | (/.p16 x (+.p16 (real->posit16 1) (*.p16 (*.p16 x x) (+.p16 (real->posit16 0.7715471019) (*.p16 (*.p16 x x) (+.p16 (*.p16 (*.p16 x x) (+.p16 (*.p16 (+.p16 (real->posit16 0.0140005442) (*.p16 (+.p16 (*.p16 (*.p16 (*.p16 x x) (real->posit16 0.0001789971)) (real->posit16 2)) (real->posit16 0.0008327945)) (*.p16 x x))) (*.p16 x x)) (real->posit16 0.0694555761))) (real->posit16 0.2909738639))))))) |
| 0.0ms | (*.p16 (*.p16 x x) (real->posit16 0.0001789971)) |
| 0.0ms | (*.p16 (*.p16 x x) (real->posit16 0.0001789971)) |
9 alts after pruning (8 fresh and 1 done)
Merged error: 2.7b
-∞% (-60.6b remaining)
Error of 3.4b against oracle of 64.0b and baseline of 64.0b