Time bar (total: 26.3s)
2 alts after pruning (2 fresh and 0 done)
Merged error: 3.4b
Found 4 expressions with local error:
| 3.2b | (/.p16 (+.p16 (+.p16 (*.p16 (*.p16 (*.p16 (*.p16 x x) (*.p16 x x)) (*.p16 (*.p16 x x) (*.p16 x x))) (+.p16 (real->posit16 0.0005064034) (*.p16 (*.p16 x x) (real->posit16 0.0001789971)))) (+.p16 (real->posit16 1) (*.p16 (*.p16 x x) (real->posit16 0.1049934947)))) (*.p16 (*.p16 (*.p16 x x) (*.p16 x x)) (+.p16 (*.p16 (real->posit16 0.0072644182) (*.p16 x x)) (real->posit16 0.0424060604)))) (+.p16 (*.p16 (*.p16 x x) (+.p16 (*.p16 (*.p16 (*.p16 x x) (*.p16 x x)) (+.p16 (real->posit16 0.0694555761) (*.p16 (real->posit16 0.0140005442) (*.p16 x x)))) (*.p16 (*.p16 (*.p16 (*.p16 x x) (*.p16 x x)) (*.p16 (*.p16 x x) (*.p16 x x))) (+.p16 (real->posit16 0.0008327945) (*.p16 (real->posit16 2) (*.p16 (*.p16 x x) (real->posit16 0.0001789971))))))) (+.p16 (*.p16 (*.p16 (*.p16 x x) (*.p16 x x)) (real->posit16 0.2909738639)) (+.p16 (real->posit16 1) (*.p16 (*.p16 x x) (real->posit16 0.7715471019)))))) |
| 0.8b | (*.p16 (*.p16 (*.p16 (*.p16 x x) (*.p16 x x)) (*.p16 (*.p16 x x) (*.p16 x x))) (+.p16 (real->posit16 0.0005064034) (*.p16 (*.p16 x x) (real->posit16 0.0001789971)))) |
| 0.7b | (*.p16 (real->posit16 0.0140005442) (*.p16 x x)) |
| 0.7b | (*.p16 (*.p16 x x) (real->posit16 0.0001789971)) |
| 3× | *-commutative |
| 2× | associate-*l* |
| 1× | distribute-rgt-in distribute-lft-in associate-*r* |
| 95.0ms | (/.p16 (+.p16 (+.p16 (*.p16 (*.p16 (*.p16 (*.p16 x x) (*.p16 x x)) (*.p16 (*.p16 x x) (*.p16 x x))) (+.p16 (real->posit16 0.0005064034) (*.p16 (*.p16 x x) (real->posit16 0.0001789971)))) (+.p16 (real->posit16 1) (*.p16 (*.p16 x x) (real->posit16 0.1049934947)))) (*.p16 (*.p16 (*.p16 x x) (*.p16 x x)) (+.p16 (*.p16 (real->posit16 0.0072644182) (*.p16 x x)) (real->posit16 0.0424060604)))) (+.p16 (*.p16 (*.p16 x x) (+.p16 (*.p16 (*.p16 (*.p16 x x) (*.p16 x x)) (+.p16 (real->posit16 0.0694555761) (*.p16 (real->posit16 0.0140005442) (*.p16 x x)))) (*.p16 (*.p16 (*.p16 (*.p16 x x) (*.p16 x x)) (*.p16 (*.p16 x x) (*.p16 x x))) (+.p16 (real->posit16 0.0008327945) (*.p16 (real->posit16 2) (*.p16 (*.p16 x x) (real->posit16 0.0001789971))))))) (+.p16 (*.p16 (*.p16 (*.p16 x x) (*.p16 x x)) (real->posit16 0.2909738639)) (+.p16 (real->posit16 1) (*.p16 (*.p16 x x) (real->posit16 0.7715471019)))))) |
| 40.0ms | (*.p16 (*.p16 (*.p16 (*.p16 x x) (*.p16 x x)) (*.p16 (*.p16 x x) (*.p16 x x))) (+.p16 (real->posit16 0.0005064034) (*.p16 (*.p16 x x) (real->posit16 0.0001789971)))) |
| 8.0ms | (*.p16 (real->posit16 0.0140005442) (*.p16 x x)) |
| 7.0ms | (*.p16 (*.p16 x x) (real->posit16 0.0001789971)) |
| 0.0ms | (/.p16 (+.p16 (+.p16 (*.p16 (*.p16 (*.p16 (*.p16 x x) (*.p16 x x)) (*.p16 (*.p16 x x) (*.p16 x x))) (+.p16 (real->posit16 0.0005064034) (*.p16 (*.p16 x x) (real->posit16 0.0001789971)))) (+.p16 (real->posit16 1) (*.p16 (*.p16 x x) (real->posit16 0.1049934947)))) (*.p16 (*.p16 (*.p16 x x) (*.p16 x x)) (+.p16 (*.p16 (real->posit16 0.0072644182) (*.p16 x x)) (real->posit16 0.0424060604)))) (+.p16 (*.p16 (*.p16 x x) (+.p16 (*.p16 (*.p16 (*.p16 x x) (*.p16 x x)) (+.p16 (real->posit16 0.0694555761) (*.p16 (real->posit16 0.0140005442) (*.p16 x x)))) (*.p16 (*.p16 (*.p16 (*.p16 x x) (*.p16 x x)) (*.p16 (*.p16 x x) (*.p16 x x))) (+.p16 (real->posit16 0.0008327945) (*.p16 (real->posit16 2) (*.p16 (*.p16 x x) (real->posit16 0.0001789971))))))) (+.p16 (*.p16 (*.p16 (*.p16 x x) (*.p16 x x)) (real->posit16 0.2909738639)) (+.p16 (real->posit16 1) (*.p16 (*.p16 x x) (real->posit16 0.7715471019)))))) |
| 0.0ms | (*.p16 (*.p16 (*.p16 (*.p16 x x) (*.p16 x x)) (*.p16 (*.p16 x x) (*.p16 x x))) (+.p16 (real->posit16 0.0005064034) (*.p16 (*.p16 x x) (real->posit16 0.0001789971)))) |
| 0.0ms | (*.p16 (*.p16 x x) (real->posit16 0.0001789971)) |
| 0.0ms | (*.p16 (real->posit16 0.0140005442) (*.p16 x x)) |
5 alts after pruning (4 fresh and 1 done)
Merged error: 3.0b
Found 4 expressions with local error:
| 3.2b | (/.p16 (+.p16 (+.p16 (+.p16 (*.p16 (*.p16 (*.p16 (*.p16 x x) (*.p16 x x)) (*.p16 (*.p16 x x) (*.p16 x x))) (real->posit16 0.0005064034)) (*.p16 (*.p16 (*.p16 (*.p16 x x) (*.p16 x x)) (*.p16 (*.p16 x x) (*.p16 x x))) (*.p16 (*.p16 x x) (real->posit16 0.0001789971)))) (+.p16 (real->posit16 1) (*.p16 (*.p16 x x) (real->posit16 0.1049934947)))) (*.p16 (*.p16 (*.p16 x x) (*.p16 x x)) (+.p16 (*.p16 (real->posit16 0.0072644182) (*.p16 x x)) (real->posit16 0.0424060604)))) (+.p16 (*.p16 (*.p16 x x) (+.p16 (*.p16 (*.p16 (*.p16 x x) (*.p16 x x)) (+.p16 (real->posit16 0.0694555761) (*.p16 (real->posit16 0.0140005442) (*.p16 x x)))) (*.p16 (*.p16 (*.p16 (*.p16 x x) (*.p16 x x)) (*.p16 (*.p16 x x) (*.p16 x x))) (+.p16 (real->posit16 0.0008327945) (*.p16 (real->posit16 2) (*.p16 (*.p16 x x) (real->posit16 0.0001789971))))))) (+.p16 (*.p16 (*.p16 (*.p16 x x) (*.p16 x x)) (real->posit16 0.2909738639)) (+.p16 (real->posit16 1) (*.p16 (*.p16 x x) (real->posit16 0.7715471019)))))) |
| 1.9b | (*.p16 (*.p16 (*.p16 (*.p16 x x) (*.p16 x x)) (*.p16 (*.p16 x x) (*.p16 x x))) (real->posit16 0.0005064034)) |
| 0.9b | (*.p16 (*.p16 (*.p16 (*.p16 x x) (*.p16 x x)) (*.p16 (*.p16 x x) (*.p16 x x))) (*.p16 (*.p16 x x) (real->posit16 0.0001789971))) |
| 0.7b | (*.p16 (real->posit16 0.0140005442) (*.p16 x x)) |
| 3× | *-commutative |
| 2× | associate-*r* associate-*l* |
| 64.0ms | (/.p16 (+.p16 (+.p16 (+.p16 (*.p16 (*.p16 (*.p16 (*.p16 x x) (*.p16 x x)) (*.p16 (*.p16 x x) (*.p16 x x))) (real->posit16 0.0005064034)) (*.p16 (*.p16 (*.p16 (*.p16 x x) (*.p16 x x)) (*.p16 (*.p16 x x) (*.p16 x x))) (*.p16 (*.p16 x x) (real->posit16 0.0001789971)))) (+.p16 (real->posit16 1) (*.p16 (*.p16 x x) (real->posit16 0.1049934947)))) (*.p16 (*.p16 (*.p16 x x) (*.p16 x x)) (+.p16 (*.p16 (real->posit16 0.0072644182) (*.p16 x x)) (real->posit16 0.0424060604)))) (+.p16 (*.p16 (*.p16 x x) (+.p16 (*.p16 (*.p16 (*.p16 x x) (*.p16 x x)) (+.p16 (real->posit16 0.0694555761) (*.p16 (real->posit16 0.0140005442) (*.p16 x x)))) (*.p16 (*.p16 (*.p16 (*.p16 x x) (*.p16 x x)) (*.p16 (*.p16 x x) (*.p16 x x))) (+.p16 (real->posit16 0.0008327945) (*.p16 (real->posit16 2) (*.p16 (*.p16 x x) (real->posit16 0.0001789971))))))) (+.p16 (*.p16 (*.p16 (*.p16 x x) (*.p16 x x)) (real->posit16 0.2909738639)) (+.p16 (real->posit16 1) (*.p16 (*.p16 x x) (real->posit16 0.7715471019)))))) |
| 25.0ms | (*.p16 (*.p16 (*.p16 (*.p16 x x) (*.p16 x x)) (*.p16 (*.p16 x x) (*.p16 x x))) (*.p16 (*.p16 x x) (real->posit16 0.0001789971))) |
| 18.0ms | (*.p16 (*.p16 (*.p16 (*.p16 x x) (*.p16 x x)) (*.p16 (*.p16 x x) (*.p16 x x))) (real->posit16 0.0005064034)) |
| 8.0ms | (*.p16 (real->posit16 0.0140005442) (*.p16 x x)) |
| 0.0ms | (/.p16 (+.p16 (+.p16 (+.p16 (*.p16 (*.p16 (*.p16 (*.p16 x x) (*.p16 x x)) (*.p16 (*.p16 x x) (*.p16 x x))) (real->posit16 0.0005064034)) (*.p16 (*.p16 (*.p16 (*.p16 x x) (*.p16 x x)) (*.p16 (*.p16 x x) (*.p16 x x))) (*.p16 (*.p16 x x) (real->posit16 0.0001789971)))) (+.p16 (real->posit16 1) (*.p16 (*.p16 x x) (real->posit16 0.1049934947)))) (*.p16 (*.p16 (*.p16 x x) (*.p16 x x)) (+.p16 (*.p16 (real->posit16 0.0072644182) (*.p16 x x)) (real->posit16 0.0424060604)))) (+.p16 (*.p16 (*.p16 x x) (+.p16 (*.p16 (*.p16 (*.p16 x x) (*.p16 x x)) (+.p16 (real->posit16 0.0694555761) (*.p16 (real->posit16 0.0140005442) (*.p16 x x)))) (*.p16 (*.p16 (*.p16 (*.p16 x x) (*.p16 x x)) (*.p16 (*.p16 x x) (*.p16 x x))) (+.p16 (real->posit16 0.0008327945) (*.p16 (real->posit16 2) (*.p16 (*.p16 x x) (real->posit16 0.0001789971))))))) (+.p16 (*.p16 (*.p16 (*.p16 x x) (*.p16 x x)) (real->posit16 0.2909738639)) (+.p16 (real->posit16 1) (*.p16 (*.p16 x x) (real->posit16 0.7715471019)))))) |
| 0.0ms | (*.p16 (real->posit16 0.0140005442) (*.p16 x x)) |
| 0.0ms | (*.p16 (*.p16 (*.p16 (*.p16 x x) (*.p16 x x)) (*.p16 (*.p16 x x) (*.p16 x x))) (*.p16 (*.p16 x x) (real->posit16 0.0001789971))) |
| 0.0ms | (*.p16 (*.p16 (*.p16 (*.p16 x x) (*.p16 x x)) (*.p16 (*.p16 x x) (*.p16 x x))) (real->posit16 0.0005064034)) |
8 alts after pruning (6 fresh and 2 done)
Merged error: 2.8b
Found 4 expressions with local error:
| 3.3b | (/.p16 (*.p16 (+.p16 (+.p16 (*.p16 (*.p16 (*.p16 x x) (*.p16 x x)) (+.p16 (+.p16 (real->posit16 0.0424060604) (*.p16 (*.p16 x (real->posit16 0.0072644182)) x)) (*.p16 (+.p16 (*.p16 (real->posit16 0.0001789971) (*.p16 x x)) (real->posit16 0.0005064034)) (*.p16 (*.p16 x x) (*.p16 x x))))) (*.p16 (*.p16 x x) (real->posit16 0.1049934947))) (real->posit16 1)) x) (+.p16 (+.p16 (*.p16 (*.p16 (*.p16 x x) (*.p16 x x)) (real->posit16 0.2909738639)) (real->posit16 1)) (*.p16 (*.p16 x x) (+.p16 (real->posit16 0.7715471019) (*.p16 (+.p16 (+.p16 (*.p16 (*.p16 (*.p16 x x) (*.p16 x x)) (+.p16 (*.p16 (*.p16 (real->posit16 0.0001789971) (*.p16 x x)) (real->posit16 2)) (real->posit16 0.0008327945))) (real->posit16 0.0694555761)) (*.p16 (*.p16 x x) (real->posit16 0.0140005442))) (*.p16 (*.p16 x x) (*.p16 x x))))))) |
| 0.7b | (*.p16 (*.p16 x x) (real->posit16 0.0140005442)) |
| 0.7b | (*.p16 (real->posit16 0.0001789971) (*.p16 x x)) |
| 0.7b | (*.p16 (real->posit16 0.0001789971) (*.p16 x x)) |
| 3× | *-commutative |
| 2× | associate-*r* |
| 1× | associate-*l* associate-/l* |
| 20.0ms | (/.p16 (*.p16 (+.p16 (+.p16 (*.p16 (*.p16 (*.p16 x x) (*.p16 x x)) (+.p16 (+.p16 (real->posit16 0.0424060604) (*.p16 (*.p16 x (real->posit16 0.0072644182)) x)) (*.p16 (+.p16 (*.p16 (real->posit16 0.0001789971) (*.p16 x x)) (real->posit16 0.0005064034)) (*.p16 (*.p16 x x) (*.p16 x x))))) (*.p16 (*.p16 x x) (real->posit16 0.1049934947))) (real->posit16 1)) x) (+.p16 (+.p16 (*.p16 (*.p16 (*.p16 x x) (*.p16 x x)) (real->posit16 0.2909738639)) (real->posit16 1)) (*.p16 (*.p16 x x) (+.p16 (real->posit16 0.7715471019) (*.p16 (+.p16 (+.p16 (*.p16 (*.p16 (*.p16 x x) (*.p16 x x)) (+.p16 (*.p16 (*.p16 (real->posit16 0.0001789971) (*.p16 x x)) (real->posit16 2)) (real->posit16 0.0008327945))) (real->posit16 0.0694555761)) (*.p16 (*.p16 x x) (real->posit16 0.0140005442))) (*.p16 (*.p16 x x) (*.p16 x x))))))) |
| 7.0ms | (*.p16 (real->posit16 0.0001789971) (*.p16 x x)) |
| 7.0ms | (*.p16 (real->posit16 0.0001789971) (*.p16 x x)) |
| 6.0ms | (*.p16 (*.p16 x x) (real->posit16 0.0140005442)) |
| 0.0ms | (/.p16 (*.p16 (+.p16 (+.p16 (*.p16 (*.p16 (*.p16 x x) (*.p16 x x)) (+.p16 (+.p16 (real->posit16 0.0424060604) (*.p16 (*.p16 x (real->posit16 0.0072644182)) x)) (*.p16 (+.p16 (*.p16 (real->posit16 0.0001789971) (*.p16 x x)) (real->posit16 0.0005064034)) (*.p16 (*.p16 x x) (*.p16 x x))))) (*.p16 (*.p16 x x) (real->posit16 0.1049934947))) (real->posit16 1)) x) (+.p16 (+.p16 (*.p16 (*.p16 (*.p16 x x) (*.p16 x x)) (real->posit16 0.2909738639)) (real->posit16 1)) (*.p16 (*.p16 x x) (+.p16 (real->posit16 0.7715471019) (*.p16 (+.p16 (+.p16 (*.p16 (*.p16 (*.p16 x x) (*.p16 x x)) (+.p16 (*.p16 (*.p16 (real->posit16 0.0001789971) (*.p16 x x)) (real->posit16 2)) (real->posit16 0.0008327945))) (real->posit16 0.0694555761)) (*.p16 (*.p16 x x) (real->posit16 0.0140005442))) (*.p16 (*.p16 x x) (*.p16 x x))))))) |
| 0.0ms | (*.p16 (*.p16 x x) (real->posit16 0.0140005442)) |
| 0.0ms | (*.p16 (real->posit16 0.0001789971) (*.p16 x x)) |
| 0.0ms | (*.p16 (real->posit16 0.0001789971) (*.p16 x x)) |
9 alts after pruning (6 fresh and 3 done)
Merged error: 2.8b
Found 4 expressions with local error:
| 3.2b | (/.p16 (+.p16 (+.p16 (+.p16 (*.p16 (*.p16 (*.p16 x x) (*.p16 x x)) (*.p16 (*.p16 (*.p16 x x) (*.p16 x x)) (real->posit16 0.0005064034))) (*.p16 (*.p16 (*.p16 (*.p16 x x) (*.p16 x x)) (*.p16 (*.p16 x x) (*.p16 x x))) (*.p16 (*.p16 x x) (real->posit16 0.0001789971)))) (+.p16 (real->posit16 1) (*.p16 (*.p16 x x) (real->posit16 0.1049934947)))) (*.p16 (*.p16 (*.p16 x x) (*.p16 x x)) (+.p16 (*.p16 (real->posit16 0.0072644182) (*.p16 x x)) (real->posit16 0.0424060604)))) (+.p16 (*.p16 (*.p16 x x) (+.p16 (*.p16 (*.p16 (*.p16 x x) (*.p16 x x)) (+.p16 (real->posit16 0.0694555761) (*.p16 (real->posit16 0.0140005442) (*.p16 x x)))) (*.p16 (*.p16 (*.p16 (*.p16 x x) (*.p16 x x)) (*.p16 (*.p16 x x) (*.p16 x x))) (+.p16 (real->posit16 0.0008327945) (*.p16 (real->posit16 2) (*.p16 (*.p16 x x) (real->posit16 0.0001789971))))))) (+.p16 (*.p16 (*.p16 (*.p16 x x) (*.p16 x x)) (real->posit16 0.2909738639)) (+.p16 (real->posit16 1) (*.p16 (*.p16 x x) (real->posit16 0.7715471019)))))) |
| 1.4b | (*.p16 (*.p16 (*.p16 x x) (*.p16 x x)) (real->posit16 0.0005064034)) |
| 0.9b | (*.p16 (*.p16 (*.p16 (*.p16 x x) (*.p16 x x)) (*.p16 (*.p16 x x) (*.p16 x x))) (*.p16 (*.p16 x x) (real->posit16 0.0001789971))) |
| 0.7b | (*.p16 (real->posit16 0.0140005442) (*.p16 x x)) |
| 3× | *-commutative |
| 2× | associate-*r* associate-*l* |
| 64.0ms | (/.p16 (+.p16 (+.p16 (+.p16 (*.p16 (*.p16 (*.p16 x x) (*.p16 x x)) (*.p16 (*.p16 (*.p16 x x) (*.p16 x x)) (real->posit16 0.0005064034))) (*.p16 (*.p16 (*.p16 (*.p16 x x) (*.p16 x x)) (*.p16 (*.p16 x x) (*.p16 x x))) (*.p16 (*.p16 x x) (real->posit16 0.0001789971)))) (+.p16 (real->posit16 1) (*.p16 (*.p16 x x) (real->posit16 0.1049934947)))) (*.p16 (*.p16 (*.p16 x x) (*.p16 x x)) (+.p16 (*.p16 (real->posit16 0.0072644182) (*.p16 x x)) (real->posit16 0.0424060604)))) (+.p16 (*.p16 (*.p16 x x) (+.p16 (*.p16 (*.p16 (*.p16 x x) (*.p16 x x)) (+.p16 (real->posit16 0.0694555761) (*.p16 (real->posit16 0.0140005442) (*.p16 x x)))) (*.p16 (*.p16 (*.p16 (*.p16 x x) (*.p16 x x)) (*.p16 (*.p16 x x) (*.p16 x x))) (+.p16 (real->posit16 0.0008327945) (*.p16 (real->posit16 2) (*.p16 (*.p16 x x) (real->posit16 0.0001789971))))))) (+.p16 (*.p16 (*.p16 (*.p16 x x) (*.p16 x x)) (real->posit16 0.2909738639)) (+.p16 (real->posit16 1) (*.p16 (*.p16 x x) (real->posit16 0.7715471019)))))) |
| 28.0ms | (*.p16 (*.p16 (*.p16 (*.p16 x x) (*.p16 x x)) (*.p16 (*.p16 x x) (*.p16 x x))) (*.p16 (*.p16 x x) (real->posit16 0.0001789971))) |
| 14.0ms | (*.p16 (*.p16 (*.p16 x x) (*.p16 x x)) (real->posit16 0.0005064034)) |
| 4.0ms | (*.p16 (real->posit16 0.0140005442) (*.p16 x x)) |
| 0.0ms | (/.p16 (+.p16 (+.p16 (+.p16 (*.p16 (*.p16 (*.p16 x x) (*.p16 x x)) (*.p16 (*.p16 (*.p16 x x) (*.p16 x x)) (real->posit16 0.0005064034))) (*.p16 (*.p16 (*.p16 (*.p16 x x) (*.p16 x x)) (*.p16 (*.p16 x x) (*.p16 x x))) (*.p16 (*.p16 x x) (real->posit16 0.0001789971)))) (+.p16 (real->posit16 1) (*.p16 (*.p16 x x) (real->posit16 0.1049934947)))) (*.p16 (*.p16 (*.p16 x x) (*.p16 x x)) (+.p16 (*.p16 (real->posit16 0.0072644182) (*.p16 x x)) (real->posit16 0.0424060604)))) (+.p16 (*.p16 (*.p16 x x) (+.p16 (*.p16 (*.p16 (*.p16 x x) (*.p16 x x)) (+.p16 (real->posit16 0.0694555761) (*.p16 (real->posit16 0.0140005442) (*.p16 x x)))) (*.p16 (*.p16 (*.p16 (*.p16 x x) (*.p16 x x)) (*.p16 (*.p16 x x) (*.p16 x x))) (+.p16 (real->posit16 0.0008327945) (*.p16 (real->posit16 2) (*.p16 (*.p16 x x) (real->posit16 0.0001789971))))))) (+.p16 (*.p16 (*.p16 (*.p16 x x) (*.p16 x x)) (real->posit16 0.2909738639)) (+.p16 (real->posit16 1) (*.p16 (*.p16 x x) (real->posit16 0.7715471019)))))) |
| 0.0ms | (*.p16 (*.p16 (*.p16 (*.p16 x x) (*.p16 x x)) (*.p16 (*.p16 x x) (*.p16 x x))) (*.p16 (*.p16 x x) (real->posit16 0.0001789971))) |
| 0.0ms | (*.p16 (real->posit16 0.0140005442) (*.p16 x x)) |
| 0.0ms | (*.p16 (*.p16 (*.p16 x x) (*.p16 x x)) (real->posit16 0.0005064034)) |
10 alts after pruning (6 fresh and 4 done)
Merged error: 2.7b
-∞% (-60.6b remaining)
Error of 3.4b against oracle of 64.0b and baseline of 64.0b