0.002 * [progress]: [Phase 1 of 3] Setting up. 0.002 * * * [progress]: [1/2] Preparing points 0.003 * * * * [points]: Sampling 256 additional inputs, on iter 0 have 0 / 256 0.003 * * * * [points]: Computing exacts on every 16 of 256 points to ramp up precision 0.030 * * * * [points]: Setting MPFR precision to 64 0.033 * * * * [points]: Setting MPFR precision to 320 0.036 * * * * [points]: Computing exacts on every 8 of 256 points to ramp up precision 0.074 * * * * [points]: Setting MPFR precision to 64 0.080 * * * * [points]: Setting MPFR precision to 320 0.085 * * * * [points]: Computing exacts on every 4 of 256 points to ramp up precision 0.114 * * * * [points]: Setting MPFR precision to 64 0.129 * * * * [points]: Setting MPFR precision to 320 0.135 * * * * [points]: Computing exacts on every 2 of 256 points to ramp up precision 0.166 * * * * [points]: Setting MPFR precision to 64 0.182 * * * * [points]: Setting MPFR precision to 320 0.196 * * * * [points]: Computing exacts for 256 points 0.234 * * * * [points]: Setting MPFR precision to 64 0.309 * * * * [points]: Setting MPFR precision to 320 0.354 * * * * [points]: Filtering points with unrepresentable outputs 0.355 * * * * [points]: Sampled 256 points with exact outputs 0.355 * * * [progress]: [2/2] Setting up program. 0.423 * [progress]: [Phase 2 of 3] Improving. 0.423 * * * * [progress]: [ 1 / 1 ] simplifiying candidate #posit16 1) (*.p16 (real->posit16 0.1049934947) (*.p16 x x))) (*.p16 (real->posit16 0.0424060604) (*.p16 (*.p16 x x) (*.p16 x x)))) (*.p16 (real->posit16 0.0072644182) (*.p16 (*.p16 (*.p16 x x) (*.p16 x x)) (*.p16 x x)))) (*.p16 (real->posit16 0.0005064034) (*.p16 (*.p16 (*.p16 (*.p16 x x) (*.p16 x x)) (*.p16 x x)) (*.p16 x x)))) (*.p16 (real->posit16 0.0001789971) (*.p16 (*.p16 (*.p16 (*.p16 (*.p16 x x) (*.p16 x x)) (*.p16 x x)) (*.p16 x x)) (*.p16 x x)))) (+.p16 (+.p16 (+.p16 (+.p16 (+.p16 (+.p16 (real->posit16 1) (*.p16 (real->posit16 0.7715471019) (*.p16 x x))) (*.p16 (real->posit16 0.2909738639) (*.p16 (*.p16 x x) (*.p16 x x)))) (*.p16 (real->posit16 0.0694555761) (*.p16 (*.p16 (*.p16 x x) (*.p16 x x)) (*.p16 x x)))) (*.p16 (real->posit16 0.0140005442) (*.p16 (*.p16 (*.p16 (*.p16 x x) (*.p16 x x)) (*.p16 x x)) (*.p16 x x)))) (*.p16 (real->posit16 0.0008327945) (*.p16 (*.p16 (*.p16 (*.p16 (*.p16 x x) (*.p16 x x)) (*.p16 x x)) (*.p16 x x)) (*.p16 x x)))) (*.p16 (*.p16 (real->posit16 2) (real->posit16 0.0001789971)) (*.p16 (*.p16 (*.p16 (*.p16 (*.p16 (*.p16 x x) (*.p16 x x)) (*.p16 x x)) (*.p16 x x)) (*.p16 x x)) (*.p16 x x))))) x))> 0.424 * [simplify]: Simplifying: (*.p16 (/.p16 (+.p16 (+.p16 (+.p16 (+.p16 (+.p16 (real->posit16 1) (*.p16 (real->posit16 0.1049934947) (*.p16 x x))) (*.p16 (real->posit16 0.0424060604) (*.p16 (*.p16 x x) (*.p16 x x)))) (*.p16 (real->posit16 0.0072644182) (*.p16 (*.p16 (*.p16 x x) (*.p16 x x)) (*.p16 x x)))) (*.p16 (real->posit16 0.0005064034) (*.p16 (*.p16 (*.p16 (*.p16 x x) (*.p16 x x)) (*.p16 x x)) (*.p16 x x)))) (*.p16 (real->posit16 0.0001789971) (*.p16 (*.p16 (*.p16 (*.p16 (*.p16 x x) (*.p16 x x)) (*.p16 x x)) (*.p16 x x)) (*.p16 x x)))) (+.p16 (+.p16 (+.p16 (+.p16 (+.p16 (+.p16 (real->posit16 1) (*.p16 (real->posit16 0.7715471019) (*.p16 x x))) (*.p16 (real->posit16 0.2909738639) (*.p16 (*.p16 x x) (*.p16 x x)))) (*.p16 (real->posit16 0.0694555761) (*.p16 (*.p16 (*.p16 x x) (*.p16 x x)) (*.p16 x x)))) (*.p16 (real->posit16 0.0140005442) (*.p16 (*.p16 (*.p16 (*.p16 x x) (*.p16 x x)) (*.p16 x x)) (*.p16 x x)))) (*.p16 (real->posit16 0.0008327945) (*.p16 (*.p16 (*.p16 (*.p16 (*.p16 x x) (*.p16 x x)) (*.p16 x x)) (*.p16 x x)) (*.p16 x x)))) (*.p16 (*.p16 (real->posit16 2) (real->posit16 0.0001789971)) (*.p16 (*.p16 (*.p16 (*.p16 (*.p16 (*.p16 x x) (*.p16 x x)) (*.p16 x x)) (*.p16 x x)) (*.p16 x x)) (*.p16 x x))))) x) 0.424 * * [simplify]: iteration 1: (56 enodes) 0.460 * * [simplify]: iteration 2: (159 enodes) 0.496 * * [simplify]: iteration 3: (526 enodes) 0.818 * * [simplify]: iteration 4: (1907 enodes) 4.402 * * [simplify]: Extracting #0: cost 1 inf + 0 4.402 * * [simplify]: Extracting #1: cost 7 inf + 0 4.403 * * [simplify]: Extracting #2: cost 337 inf + 1 4.412 * * [simplify]: Extracting #3: cost 1447 inf + 1 4.428 * * [simplify]: Extracting #4: cost 1690 inf + 1609 4.455 * * [simplify]: Extracting #5: cost 1612 inf + 64467 4.522 * * [simplify]: Extracting #6: cost 1026 inf + 1022588 4.763 * * [simplify]: Extracting #7: cost 123 inf + 3103670 5.052 * * [simplify]: Extracting #8: cost 0 inf + 3328963 5.420 * * [simplify]: Extracting #9: cost 0 inf + 3307083 5.870 * * [simplify]: Extracting #10: cost 0 inf + 3304843 6.317 * * [simplify]: Extracting #11: cost 0 inf + 3302603 6.660 * [simplify]: Simplified to: (*.p16 (/.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))))) x) 6.890 * * [progress]: iteration 1 / 4 6.890 * * * [progress]: picking best candidate 7.071 * * * * [pick]: Picked #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))))) x))> 7.072 * * * [progress]: localizing error 7.854 * * * [progress]: generating rewritten candidates 7.854 * * * * [progress]: [ 1 / 4 ] rewriting at (2 1) 7.866 * * * * [progress]: [ 2 / 4 ] rewriting at (2 1 2 1 1 2 1 2 1) 7.878 * * * * [progress]: [ 3 / 4 ] rewriting at (2 1 1 1 1 2 1 2 1) 7.881 * * * * [progress]: [ 4 / 4 ] rewriting at (2) 7.889 * * * [progress]: generating series expansions 7.889 * * * * [progress]: [ 1 / 4 ] generating series at (2 1) 7.889 * * * * [progress]: [ 2 / 4 ] generating series at (2 1 2 1 1 2 1 2 1) 7.889 * * * * [progress]: [ 3 / 4 ] generating series at (2 1 1 1 1 2 1 2 1) 7.889 * * * * [progress]: [ 4 / 4 ] generating series at (2) 7.889 * * * [progress]: simplifying candidates 7.889 * * * * [progress]: [ 1 / 10 ] simplifiying candidate #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 (*.p16 (real->posit16 0.0001789971) (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))))) x))> 7.889 * * * * [progress]: [ 2 / 10 ] simplifiying candidate #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 (*.p16 (real->posit16 2) (*.p16 x x)) (real->posit16 0.0001789971)) (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))))) x))> 7.889 * * * * [progress]: [ 3 / 10 ] simplifiying candidate #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))))) x))> 7.889 * * * * [progress]: [ 4 / 10 ] simplifiying candidate #posit16 0.0001789971) (*.p16 x x)) (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))))) x))> 7.889 * * * * [progress]: [ 5 / 10 ] simplifiying candidate #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))) x) (+.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))))))> 7.890 * * * * [progress]: [ 6 / 10 ] simplifiying candidate #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)))))))> 7.890 * * * * [progress]: [ 7 / 10 ] simplifiying candidate #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))))) x))> 7.890 * * * * [progress]: [ 8 / 10 ] simplifiying candidate #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))))) x))> 7.890 * * * * [progress]: [ 9 / 10 ] simplifiying candidate #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))))) x))> 7.890 * * * * [progress]: [ 10 / 10 ] simplifiying candidate #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))))) x))> 7.890 * [simplify]: Simplifying: (*.p16 (real->posit16 0.0001789971) (real->posit16 2)) (*.p16 x (real->posit16 0.0001789971)) (*.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))) x) (*.p16 (/.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))))) x) (*.p16 (/.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))))) x) (*.p16 (/.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))))) x) (*.p16 (/.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))))) x) 7.891 * * [simplify]: iteration 1: (56 enodes) 7.905 * * [simplify]: iteration 2: (168 enodes) 7.948 * * [simplify]: iteration 3: (570 enodes) 8.245 * * [simplify]: Extracting #0: cost 4 inf + 0 8.246 * * [simplify]: Extracting #1: cost 21 inf + 0 8.246 * * [simplify]: Extracting #2: cost 90 inf + 1 8.247 * * [simplify]: Extracting #3: cost 351 inf + 326 8.249 * * [simplify]: Extracting #4: cost 496 inf + 17629 8.253 * * [simplify]: Extracting #5: cost 458 inf + 67960 8.260 * * [simplify]: Extracting #6: cost 382 inf + 153055 8.290 * * [simplify]: Extracting #7: cost 179 inf + 505248 8.340 * * [simplify]: Extracting #8: cost 30 inf + 835119 8.433 * * [simplify]: Extracting #9: cost 0 inf + 884034 8.538 * * [simplify]: Extracting #10: cost 0 inf + 883074 8.644 * [simplify]: Simplified to: (*.p16 (real->posit16 0.0001789971) (real->posit16 2)) (*.p16 x (real->posit16 0.0001789971)) (*.p16 (+.p16 (*.p16 (*.p16 x x) (+.p16 (*.p16 (+.p16 (*.p16 (*.p16 x x) (+.p16 (+.p16 (*.p16 (real->posit16 0.0005064034) (*.p16 x x)) (*.p16 (*.p16 (*.p16 x x) (*.p16 x x)) (real->posit16 0.0001789971))) (real->posit16 0.0072644182))) (real->posit16 0.0424060604)) (*.p16 x x)) (real->posit16 0.1049934947))) (real->posit16 1)) x) (*.p16 (/.p16 x (+.p16 (+.p16 (*.p16 (*.p16 x x) (real->posit16 0.7715471019)) (real->posit16 1)) (*.p16 (*.p16 (*.p16 x x) (*.p16 x x)) (+.p16 (+.p16 (*.p16 (*.p16 x x) (real->posit16 0.0694555761)) (real->posit16 0.2909738639)) (*.p16 (+.p16 (*.p16 (*.p16 x x) (+.p16 (real->posit16 0.0008327945) (*.p16 (*.p16 x x) (*.p16 (real->posit16 0.0001789971) (real->posit16 2))))) (real->posit16 0.0140005442)) (*.p16 (*.p16 x x) (*.p16 x x))))))) (+.p16 (*.p16 (*.p16 x x) (+.p16 (*.p16 (+.p16 (*.p16 (*.p16 x x) (+.p16 (+.p16 (*.p16 (real->posit16 0.0005064034) (*.p16 x x)) (*.p16 (*.p16 (*.p16 x x) (*.p16 x x)) (real->posit16 0.0001789971))) (real->posit16 0.0072644182))) (real->posit16 0.0424060604)) (*.p16 x x)) (real->posit16 0.1049934947))) (real->posit16 1))) (*.p16 (/.p16 x (+.p16 (+.p16 (*.p16 (*.p16 x x) (real->posit16 0.7715471019)) (real->posit16 1)) (*.p16 (*.p16 (*.p16 x x) (*.p16 x x)) (+.p16 (+.p16 (*.p16 (*.p16 x x) (real->posit16 0.0694555761)) (real->posit16 0.2909738639)) (*.p16 (+.p16 (*.p16 (*.p16 x x) (+.p16 (real->posit16 0.0008327945) (*.p16 (*.p16 x x) (*.p16 (real->posit16 0.0001789971) (real->posit16 2))))) (real->posit16 0.0140005442)) (*.p16 (*.p16 x x) (*.p16 x x))))))) (+.p16 (*.p16 (*.p16 x x) (+.p16 (*.p16 (+.p16 (*.p16 (*.p16 x x) (+.p16 (+.p16 (*.p16 (real->posit16 0.0005064034) (*.p16 x x)) (*.p16 (*.p16 (*.p16 x x) (*.p16 x x)) (real->posit16 0.0001789971))) (real->posit16 0.0072644182))) (real->posit16 0.0424060604)) (*.p16 x x)) (real->posit16 0.1049934947))) (real->posit16 1))) (*.p16 (/.p16 x (+.p16 (+.p16 (*.p16 (*.p16 x x) (real->posit16 0.7715471019)) (real->posit16 1)) (*.p16 (*.p16 (*.p16 x x) (*.p16 x x)) (+.p16 (+.p16 (*.p16 (*.p16 x x) (real->posit16 0.0694555761)) (real->posit16 0.2909738639)) (*.p16 (+.p16 (*.p16 (*.p16 x x) (+.p16 (real->posit16 0.0008327945) (*.p16 (*.p16 x x) (*.p16 (real->posit16 0.0001789971) (real->posit16 2))))) (real->posit16 0.0140005442)) (*.p16 (*.p16 x x) (*.p16 x x))))))) (+.p16 (*.p16 (*.p16 x x) (+.p16 (*.p16 (+.p16 (*.p16 (*.p16 x x) (+.p16 (+.p16 (*.p16 (real->posit16 0.0005064034) (*.p16 x x)) (*.p16 (*.p16 (*.p16 x x) (*.p16 x x)) (real->posit16 0.0001789971))) (real->posit16 0.0072644182))) (real->posit16 0.0424060604)) (*.p16 x x)) (real->posit16 0.1049934947))) (real->posit16 1))) (*.p16 (/.p16 x (+.p16 (+.p16 (*.p16 (*.p16 x x) (real->posit16 0.7715471019)) (real->posit16 1)) (*.p16 (*.p16 (*.p16 x x) (*.p16 x x)) (+.p16 (+.p16 (*.p16 (*.p16 x x) (real->posit16 0.0694555761)) (real->posit16 0.2909738639)) (*.p16 (+.p16 (*.p16 (*.p16 x x) (+.p16 (real->posit16 0.0008327945) (*.p16 (*.p16 x x) (*.p16 (real->posit16 0.0001789971) (real->posit16 2))))) (real->posit16 0.0140005442)) (*.p16 (*.p16 x x) (*.p16 x x))))))) (+.p16 (*.p16 (*.p16 x x) (+.p16 (*.p16 (+.p16 (*.p16 (*.p16 x x) (+.p16 (+.p16 (*.p16 (real->posit16 0.0005064034) (*.p16 x x)) (*.p16 (*.p16 (*.p16 x x) (*.p16 x x)) (real->posit16 0.0001789971))) (real->posit16 0.0072644182))) (real->posit16 0.0424060604)) (*.p16 x x)) (real->posit16 0.1049934947))) (real->posit16 1))) 8.648 * * * [progress]: adding candidates to table 10.249 * * [progress]: iteration 2 / 4 10.249 * * * [progress]: picking best candidate 10.442 * * * * [pick]: Picked #posit16 0.7715471019)) (real->posit16 1)) (*.p16 (*.p16 (*.p16 x x) (*.p16 x x)) (+.p16 (+.p16 (*.p16 (*.p16 x x) (real->posit16 0.0694555761)) (real->posit16 0.2909738639)) (*.p16 (+.p16 (*.p16 (*.p16 x x) (+.p16 (real->posit16 0.0008327945) (*.p16 (*.p16 x x) (*.p16 (real->posit16 0.0001789971) (real->posit16 2))))) (real->posit16 0.0140005442)) (*.p16 (*.p16 x x) (*.p16 x x))))))) (+.p16 (*.p16 (*.p16 x x) (+.p16 (*.p16 (+.p16 (*.p16 (*.p16 x x) (+.p16 (+.p16 (*.p16 (real->posit16 0.0005064034) (*.p16 x x)) (*.p16 (*.p16 (*.p16 x x) (*.p16 x x)) (real->posit16 0.0001789971))) (real->posit16 0.0072644182))) (real->posit16 0.0424060604)) (*.p16 x x)) (real->posit16 0.1049934947))) (real->posit16 1))))> 10.442 * * * [progress]: localizing error 11.371 * * * [progress]: generating rewritten candidates 11.371 * * * * [progress]: [ 1 / 4 ] rewriting at (2) 11.377 * * * * [progress]: [ 2 / 4 ] rewriting at (2 2 1 2 1 1 1 2 1 2) 11.392 * * * * [progress]: [ 3 / 4 ] rewriting at (2 2 1 2 1 1 1 2 1 1) 11.401 * * * * [progress]: [ 4 / 4 ] rewriting at (2 1 2 2 2 2 1 1 2 2) 11.412 * * * [progress]: generating series expansions 11.412 * * * * [progress]: [ 1 / 4 ] generating series at (2) 11.412 * * * * [progress]: [ 2 / 4 ] generating series at (2 2 1 2 1 1 1 2 1 2) 11.412 * * * * [progress]: [ 3 / 4 ] generating series at (2 2 1 2 1 1 1 2 1 1) 11.412 * * * * [progress]: [ 4 / 4 ] generating series at (2 1 2 2 2 2 1 1 2 2) 11.412 * * * [progress]: simplifying candidates 11.412 * * * * [progress]: [ 1 / 15 ] simplifiying candidate #posit16 0.7715471019)) (real->posit16 1)) (*.p16 (*.p16 (*.p16 x x) (*.p16 x x)) (+.p16 (+.p16 (*.p16 (*.p16 x x) (real->posit16 0.0694555761)) (real->posit16 0.2909738639)) (*.p16 (+.p16 (*.p16 (*.p16 x x) (+.p16 (real->posit16 0.0008327945) (*.p16 (*.p16 x x) (*.p16 (real->posit16 0.0001789971) (real->posit16 2))))) (real->posit16 0.0140005442)) (*.p16 (*.p16 x x) (*.p16 x x))))))) (*.p16 (*.p16 x x) (+.p16 (*.p16 (+.p16 (*.p16 (*.p16 x x) (+.p16 (+.p16 (*.p16 (real->posit16 0.0005064034) (*.p16 x x)) (*.p16 (*.p16 (*.p16 x x) (*.p16 x x)) (real->posit16 0.0001789971))) (real->posit16 0.0072644182))) (real->posit16 0.0424060604)) (*.p16 x x)) (real->posit16 0.1049934947)))) (*.p16 (/.p16 x (+.p16 (+.p16 (*.p16 (*.p16 x x) (real->posit16 0.7715471019)) (real->posit16 1)) (*.p16 (*.p16 (*.p16 x x) (*.p16 x x)) (+.p16 (+.p16 (*.p16 (*.p16 x x) (real->posit16 0.0694555761)) (real->posit16 0.2909738639)) (*.p16 (+.p16 (*.p16 (*.p16 x x) (+.p16 (real->posit16 0.0008327945) (*.p16 (*.p16 x x) (*.p16 (real->posit16 0.0001789971) (real->posit16 2))))) (real->posit16 0.0140005442)) (*.p16 (*.p16 x x) (*.p16 x x))))))) (real->posit16 1))))> 11.412 * * * * [progress]: [ 2 / 15 ] simplifiying candidate #posit16 0.0005064034) (*.p16 x x)) (*.p16 (*.p16 (*.p16 x x) (*.p16 x x)) (real->posit16 0.0001789971))) (real->posit16 0.0072644182))) (real->posit16 0.0424060604)) (*.p16 x x)) (real->posit16 0.1049934947))) (/.p16 x (+.p16 (+.p16 (*.p16 (*.p16 x x) (real->posit16 0.7715471019)) (real->posit16 1)) (*.p16 (*.p16 (*.p16 x x) (*.p16 x x)) (+.p16 (+.p16 (*.p16 (*.p16 x x) (real->posit16 0.0694555761)) (real->posit16 0.2909738639)) (*.p16 (+.p16 (*.p16 (*.p16 x x) (+.p16 (real->posit16 0.0008327945) (*.p16 (*.p16 x x) (*.p16 (real->posit16 0.0001789971) (real->posit16 2))))) (real->posit16 0.0140005442)) (*.p16 (*.p16 x x) (*.p16 x x)))))))) (*.p16 (real->posit16 1) (/.p16 x (+.p16 (+.p16 (*.p16 (*.p16 x x) (real->posit16 0.7715471019)) (real->posit16 1)) (*.p16 (*.p16 (*.p16 x x) (*.p16 x x)) (+.p16 (+.p16 (*.p16 (*.p16 x x) (real->posit16 0.0694555761)) (real->posit16 0.2909738639)) (*.p16 (+.p16 (*.p16 (*.p16 x x) (+.p16 (real->posit16 0.0008327945) (*.p16 (*.p16 x x) (*.p16 (real->posit16 0.0001789971) (real->posit16 2))))) (real->posit16 0.0140005442)) (*.p16 (*.p16 x x) (*.p16 x x))))))))))> 11.413 * * * * [progress]: [ 3 / 15 ] simplifiying candidate #posit16 0.0005064034) (*.p16 x x)) (*.p16 (*.p16 (*.p16 x x) (*.p16 x x)) (real->posit16 0.0001789971))) (real->posit16 0.0072644182))) (real->posit16 0.0424060604)) (*.p16 x x)) (real->posit16 0.1049934947))) (real->posit16 1))) (+.p16 (+.p16 (*.p16 (*.p16 x x) (real->posit16 0.7715471019)) (real->posit16 1)) (*.p16 (*.p16 (*.p16 x x) (*.p16 x x)) (+.p16 (+.p16 (*.p16 (*.p16 x x) (real->posit16 0.0694555761)) (real->posit16 0.2909738639)) (*.p16 (+.p16 (*.p16 (*.p16 x x) (+.p16 (real->posit16 0.0008327945) (*.p16 (*.p16 x x) (*.p16 (real->posit16 0.0001789971) (real->posit16 2))))) (real->posit16 0.0140005442)) (*.p16 (*.p16 x x) (*.p16 x x))))))))> 11.413 * * * * [progress]: [ 4 / 15 ] simplifiying candidate #posit16 0.0005064034) (*.p16 x x)) (*.p16 (*.p16 (*.p16 x x) (*.p16 x x)) (real->posit16 0.0001789971))) (real->posit16 0.0072644182))) (real->posit16 0.0424060604)) (*.p16 x x)) (real->posit16 0.1049934947))) (real->posit16 1)) (/.p16 x (+.p16 (+.p16 (*.p16 (*.p16 x x) (real->posit16 0.7715471019)) (real->posit16 1)) (*.p16 (*.p16 (*.p16 x x) (*.p16 x x)) (+.p16 (+.p16 (*.p16 (*.p16 x x) (real->posit16 0.0694555761)) (real->posit16 0.2909738639)) (*.p16 (+.p16 (*.p16 (*.p16 x x) (+.p16 (real->posit16 0.0008327945) (*.p16 (*.p16 x x) (*.p16 (real->posit16 0.0001789971) (real->posit16 2))))) (real->posit16 0.0140005442)) (*.p16 (*.p16 x x) (*.p16 x x)))))))))> 11.413 * * * * [progress]: [ 5 / 15 ] simplifiying candidate #posit16 0.7715471019)) (real->posit16 1)) (*.p16 (*.p16 (*.p16 x x) (*.p16 x x)) (+.p16 (+.p16 (*.p16 (*.p16 x x) (real->posit16 0.0694555761)) (real->posit16 0.2909738639)) (*.p16 (+.p16 (*.p16 (*.p16 x x) (+.p16 (real->posit16 0.0008327945) (*.p16 (*.p16 x x) (*.p16 (real->posit16 0.0001789971) (real->posit16 2))))) (real->posit16 0.0140005442)) (*.p16 (*.p16 x x) (*.p16 x x))))))) (+.p16 (*.p16 (*.p16 x x) (+.p16 (*.p16 (+.p16 (*.p16 (*.p16 x x) (+.p16 (+.p16 (*.p16 (real->posit16 0.0005064034) (*.p16 x x)) (*.p16 (*.p16 x x) (*.p16 (*.p16 x x) (real->posit16 0.0001789971)))) (real->posit16 0.0072644182))) (real->posit16 0.0424060604)) (*.p16 x x)) (real->posit16 0.1049934947))) (real->posit16 1))))> 11.413 * * * * [progress]: [ 6 / 15 ] simplifiying candidate #posit16 0.7715471019)) (real->posit16 1)) (*.p16 (*.p16 (*.p16 x x) (*.p16 x x)) (+.p16 (+.p16 (*.p16 (*.p16 x x) (real->posit16 0.0694555761)) (real->posit16 0.2909738639)) (*.p16 (+.p16 (*.p16 (*.p16 x x) (+.p16 (real->posit16 0.0008327945) (*.p16 (*.p16 x x) (*.p16 (real->posit16 0.0001789971) (real->posit16 2))))) (real->posit16 0.0140005442)) (*.p16 (*.p16 x x) (*.p16 x x))))))) (+.p16 (*.p16 (*.p16 x x) (+.p16 (*.p16 (+.p16 (*.p16 (*.p16 x x) (+.p16 (+.p16 (*.p16 (real->posit16 0.0005064034) (*.p16 x x)) (*.p16 (real->posit16 0.0001789971) (*.p16 (*.p16 x x) (*.p16 x x)))) (real->posit16 0.0072644182))) (real->posit16 0.0424060604)) (*.p16 x x)) (real->posit16 0.1049934947))) (real->posit16 1))))> 11.413 * * * * [progress]: [ 7 / 15 ] simplifiying candidate #posit16 0.7715471019)) (real->posit16 1)) (*.p16 (*.p16 (*.p16 x x) (*.p16 x x)) (+.p16 (+.p16 (*.p16 (*.p16 x x) (real->posit16 0.0694555761)) (real->posit16 0.2909738639)) (*.p16 (+.p16 (*.p16 (*.p16 x x) (+.p16 (real->posit16 0.0008327945) (*.p16 (*.p16 x x) (*.p16 (real->posit16 0.0001789971) (real->posit16 2))))) (real->posit16 0.0140005442)) (*.p16 (*.p16 x x) (*.p16 x x))))))) (+.p16 (*.p16 (*.p16 x x) (+.p16 (*.p16 (+.p16 (*.p16 (*.p16 x x) (+.p16 (+.p16 (*.p16 (*.p16 (real->posit16 0.0005064034) x) x) (*.p16 (*.p16 (*.p16 x x) (*.p16 x x)) (real->posit16 0.0001789971))) (real->posit16 0.0072644182))) (real->posit16 0.0424060604)) (*.p16 x x)) (real->posit16 0.1049934947))) (real->posit16 1))))> 11.413 * * * * [progress]: [ 8 / 15 ] simplifiying candidate #posit16 0.7715471019)) (real->posit16 1)) (*.p16 (*.p16 (*.p16 x x) (*.p16 x x)) (+.p16 (+.p16 (*.p16 (*.p16 x x) (real->posit16 0.0694555761)) (real->posit16 0.2909738639)) (*.p16 (+.p16 (*.p16 (*.p16 x x) (+.p16 (real->posit16 0.0008327945) (*.p16 (*.p16 x x) (*.p16 (real->posit16 0.0001789971) (real->posit16 2))))) (real->posit16 0.0140005442)) (*.p16 (*.p16 x x) (*.p16 x x))))))) (+.p16 (*.p16 (*.p16 x x) (+.p16 (*.p16 (+.p16 (*.p16 (*.p16 x x) (+.p16 (+.p16 (*.p16 (*.p16 x x) (real->posit16 0.0005064034)) (*.p16 (*.p16 (*.p16 x x) (*.p16 x x)) (real->posit16 0.0001789971))) (real->posit16 0.0072644182))) (real->posit16 0.0424060604)) (*.p16 x x)) (real->posit16 0.1049934947))) (real->posit16 1))))> 11.413 * * * * [progress]: [ 9 / 15 ] simplifiying candidate #posit16 0.7715471019)) (real->posit16 1)) (*.p16 (*.p16 (*.p16 x x) (*.p16 x x)) (+.p16 (+.p16 (*.p16 (*.p16 x x) (real->posit16 0.0694555761)) (real->posit16 0.2909738639)) (*.p16 (+.p16 (*.p16 (*.p16 x x) (+.p16 (real->posit16 0.0008327945) (*.p16 (*.p16 (*.p16 x x) (real->posit16 0.0001789971)) (real->posit16 2)))) (real->posit16 0.0140005442)) (*.p16 (*.p16 x x) (*.p16 x x))))))) (+.p16 (*.p16 (*.p16 x x) (+.p16 (*.p16 (+.p16 (*.p16 (*.p16 x x) (+.p16 (+.p16 (*.p16 (real->posit16 0.0005064034) (*.p16 x x)) (*.p16 (*.p16 (*.p16 x x) (*.p16 x x)) (real->posit16 0.0001789971))) (real->posit16 0.0072644182))) (real->posit16 0.0424060604)) (*.p16 x x)) (real->posit16 0.1049934947))) (real->posit16 1))))> 11.413 * * * * [progress]: [ 10 / 15 ] simplifiying candidate #posit16 0.7715471019)) (real->posit16 1)) (*.p16 (*.p16 (*.p16 x x) (*.p16 x x)) (+.p16 (+.p16 (*.p16 (*.p16 x x) (real->posit16 0.0694555761)) (real->posit16 0.2909738639)) (*.p16 (+.p16 (*.p16 (*.p16 x x) (+.p16 (real->posit16 0.0008327945) (*.p16 x (*.p16 x (*.p16 (real->posit16 0.0001789971) (real->posit16 2)))))) (real->posit16 0.0140005442)) (*.p16 (*.p16 x x) (*.p16 x x))))))) (+.p16 (*.p16 (*.p16 x x) (+.p16 (*.p16 (+.p16 (*.p16 (*.p16 x x) (+.p16 (+.p16 (*.p16 (real->posit16 0.0005064034) (*.p16 x x)) (*.p16 (*.p16 (*.p16 x x) (*.p16 x x)) (real->posit16 0.0001789971))) (real->posit16 0.0072644182))) (real->posit16 0.0424060604)) (*.p16 x x)) (real->posit16 0.1049934947))) (real->posit16 1))))> 11.413 * * * * [progress]: [ 11 / 15 ] simplifiying candidate #posit16 0.7715471019)) (real->posit16 1)) (*.p16 (*.p16 (*.p16 x x) (*.p16 x x)) (+.p16 (+.p16 (*.p16 (*.p16 x x) (real->posit16 0.0694555761)) (real->posit16 0.2909738639)) (*.p16 (+.p16 (*.p16 (*.p16 x x) (+.p16 (real->posit16 0.0008327945) (*.p16 (*.p16 (real->posit16 0.0001789971) (real->posit16 2)) (*.p16 x x)))) (real->posit16 0.0140005442)) (*.p16 (*.p16 x x) (*.p16 x x))))))) (+.p16 (*.p16 (*.p16 x x) (+.p16 (*.p16 (+.p16 (*.p16 (*.p16 x x) (+.p16 (+.p16 (*.p16 (real->posit16 0.0005064034) (*.p16 x x)) (*.p16 (*.p16 (*.p16 x x) (*.p16 x x)) (real->posit16 0.0001789971))) (real->posit16 0.0072644182))) (real->posit16 0.0424060604)) (*.p16 x x)) (real->posit16 0.1049934947))) (real->posit16 1))))> 11.413 * * * * [progress]: [ 12 / 15 ] simplifiying candidate #posit16 0.7715471019)) (real->posit16 1)) (*.p16 (*.p16 (*.p16 x x) (*.p16 x x)) (+.p16 (+.p16 (*.p16 (*.p16 x x) (real->posit16 0.0694555761)) (real->posit16 0.2909738639)) (*.p16 (+.p16 (*.p16 (*.p16 x x) (+.p16 (real->posit16 0.0008327945) (*.p16 (*.p16 x x) (*.p16 (real->posit16 0.0001789971) (real->posit16 2))))) (real->posit16 0.0140005442)) (*.p16 (*.p16 x x) (*.p16 x x))))))) (+.p16 (*.p16 (*.p16 x x) (+.p16 (*.p16 (+.p16 (*.p16 (*.p16 x x) (+.p16 (+.p16 (*.p16 (real->posit16 0.0005064034) (*.p16 x x)) (*.p16 (*.p16 (*.p16 x x) (*.p16 x x)) (real->posit16 0.0001789971))) (real->posit16 0.0072644182))) (real->posit16 0.0424060604)) (*.p16 x x)) (real->posit16 0.1049934947))) (real->posit16 1))))> 11.414 * * * * [progress]: [ 13 / 15 ] simplifiying candidate #posit16 0.7715471019)) (real->posit16 1)) (*.p16 (*.p16 (*.p16 x x) (*.p16 x x)) (+.p16 (+.p16 (*.p16 (*.p16 x x) (real->posit16 0.0694555761)) (real->posit16 0.2909738639)) (*.p16 (+.p16 (*.p16 (*.p16 x x) (+.p16 (real->posit16 0.0008327945) (*.p16 (*.p16 x x) (*.p16 (real->posit16 0.0001789971) (real->posit16 2))))) (real->posit16 0.0140005442)) (*.p16 (*.p16 x x) (*.p16 x x))))))) (+.p16 (*.p16 (*.p16 x x) (+.p16 (*.p16 (+.p16 (*.p16 (*.p16 x x) (+.p16 (+.p16 (*.p16 (real->posit16 0.0005064034) (*.p16 x x)) (*.p16 (*.p16 (*.p16 x x) (*.p16 x x)) (real->posit16 0.0001789971))) (real->posit16 0.0072644182))) (real->posit16 0.0424060604)) (*.p16 x x)) (real->posit16 0.1049934947))) (real->posit16 1))))> 11.414 * * * * [progress]: [ 14 / 15 ] simplifiying candidate #posit16 0.7715471019)) (real->posit16 1)) (*.p16 (*.p16 (*.p16 x x) (*.p16 x x)) (+.p16 (+.p16 (*.p16 (*.p16 x x) (real->posit16 0.0694555761)) (real->posit16 0.2909738639)) (*.p16 (+.p16 (*.p16 (*.p16 x x) (+.p16 (real->posit16 0.0008327945) (*.p16 (*.p16 x x) (*.p16 (real->posit16 0.0001789971) (real->posit16 2))))) (real->posit16 0.0140005442)) (*.p16 (*.p16 x x) (*.p16 x x))))))) (+.p16 (*.p16 (*.p16 x x) (+.p16 (*.p16 (+.p16 (*.p16 (*.p16 x x) (+.p16 (+.p16 (*.p16 (real->posit16 0.0005064034) (*.p16 x x)) (*.p16 (*.p16 (*.p16 x x) (*.p16 x x)) (real->posit16 0.0001789971))) (real->posit16 0.0072644182))) (real->posit16 0.0424060604)) (*.p16 x x)) (real->posit16 0.1049934947))) (real->posit16 1))))> 11.414 * * * * [progress]: [ 15 / 15 ] simplifiying candidate #posit16 0.7715471019)) (real->posit16 1)) (*.p16 (*.p16 (*.p16 x x) (*.p16 x x)) (+.p16 (+.p16 (*.p16 (*.p16 x x) (real->posit16 0.0694555761)) (real->posit16 0.2909738639)) (*.p16 (+.p16 (*.p16 (*.p16 x x) (+.p16 (real->posit16 0.0008327945) (*.p16 (*.p16 x x) (*.p16 (real->posit16 0.0001789971) (real->posit16 2))))) (real->posit16 0.0140005442)) (*.p16 (*.p16 x x) (*.p16 x x))))))) (+.p16 (*.p16 (*.p16 x x) (+.p16 (*.p16 (+.p16 (*.p16 (*.p16 x x) (+.p16 (+.p16 (*.p16 (real->posit16 0.0005064034) (*.p16 x x)) (*.p16 (*.p16 (*.p16 x x) (*.p16 x x)) (real->posit16 0.0001789971))) (real->posit16 0.0072644182))) (real->posit16 0.0424060604)) (*.p16 x x)) (real->posit16 0.1049934947))) (real->posit16 1))))> 11.414 * [simplify]: Simplifying: (*.p16 (/.p16 x (+.p16 (+.p16 (*.p16 (*.p16 x x) (real->posit16 0.7715471019)) (real->posit16 1)) (*.p16 (*.p16 (*.p16 x x) (*.p16 x x)) (+.p16 (+.p16 (*.p16 (*.p16 x x) (real->posit16 0.0694555761)) (real->posit16 0.2909738639)) (*.p16 (+.p16 (*.p16 (*.p16 x x) (+.p16 (real->posit16 0.0008327945) (*.p16 (*.p16 x x) (*.p16 (real->posit16 0.0001789971) (real->posit16 2))))) (real->posit16 0.0140005442)) (*.p16 (*.p16 x x) (*.p16 x x))))))) (*.p16 (*.p16 x x) (+.p16 (*.p16 (+.p16 (*.p16 (*.p16 x x) (+.p16 (+.p16 (*.p16 (real->posit16 0.0005064034) (*.p16 x x)) (*.p16 (*.p16 (*.p16 x x) (*.p16 x x)) (real->posit16 0.0001789971))) (real->posit16 0.0072644182))) (real->posit16 0.0424060604)) (*.p16 x x)) (real->posit16 0.1049934947)))) (*.p16 (/.p16 x (+.p16 (+.p16 (*.p16 (*.p16 x x) (real->posit16 0.7715471019)) (real->posit16 1)) (*.p16 (*.p16 (*.p16 x x) (*.p16 x x)) (+.p16 (+.p16 (*.p16 (*.p16 x x) (real->posit16 0.0694555761)) (real->posit16 0.2909738639)) (*.p16 (+.p16 (*.p16 (*.p16 x x) (+.p16 (real->posit16 0.0008327945) (*.p16 (*.p16 x x) (*.p16 (real->posit16 0.0001789971) (real->posit16 2))))) (real->posit16 0.0140005442)) (*.p16 (*.p16 x x) (*.p16 x x))))))) (real->posit16 1)) (*.p16 (*.p16 (*.p16 x x) (+.p16 (*.p16 (+.p16 (*.p16 (*.p16 x x) (+.p16 (+.p16 (*.p16 (real->posit16 0.0005064034) (*.p16 x x)) (*.p16 (*.p16 (*.p16 x x) (*.p16 x x)) (real->posit16 0.0001789971))) (real->posit16 0.0072644182))) (real->posit16 0.0424060604)) (*.p16 x x)) (real->posit16 0.1049934947))) (/.p16 x (+.p16 (+.p16 (*.p16 (*.p16 x x) (real->posit16 0.7715471019)) (real->posit16 1)) (*.p16 (*.p16 (*.p16 x x) (*.p16 x x)) (+.p16 (+.p16 (*.p16 (*.p16 x x) (real->posit16 0.0694555761)) (real->posit16 0.2909738639)) (*.p16 (+.p16 (*.p16 (*.p16 x x) (+.p16 (real->posit16 0.0008327945) (*.p16 (*.p16 x x) (*.p16 (real->posit16 0.0001789971) (real->posit16 2))))) (real->posit16 0.0140005442)) (*.p16 (*.p16 x x) (*.p16 x x)))))))) (*.p16 (real->posit16 1) (/.p16 x (+.p16 (+.p16 (*.p16 (*.p16 x x) (real->posit16 0.7715471019)) (real->posit16 1)) (*.p16 (*.p16 (*.p16 x x) (*.p16 x x)) (+.p16 (+.p16 (*.p16 (*.p16 x x) (real->posit16 0.0694555761)) (real->posit16 0.2909738639)) (*.p16 (+.p16 (*.p16 (*.p16 x x) (+.p16 (real->posit16 0.0008327945) (*.p16 (*.p16 x x) (*.p16 (real->posit16 0.0001789971) (real->posit16 2))))) (real->posit16 0.0140005442)) (*.p16 (*.p16 x x) (*.p16 x x)))))))) (*.p16 x (+.p16 (*.p16 (*.p16 x x) (+.p16 (*.p16 (+.p16 (*.p16 (*.p16 x x) (+.p16 (+.p16 (*.p16 (real->posit16 0.0005064034) (*.p16 x x)) (*.p16 (*.p16 (*.p16 x x) (*.p16 x x)) (real->posit16 0.0001789971))) (real->posit16 0.0072644182))) (real->posit16 0.0424060604)) (*.p16 x x)) (real->posit16 0.1049934947))) (real->posit16 1))) (*.p16 (*.p16 x x) (real->posit16 0.0001789971)) (*.p16 (real->posit16 0.0005064034) x) (*.p16 (*.p16 x x) (real->posit16 0.0001789971)) (*.p16 x (*.p16 (real->posit16 0.0001789971) (real->posit16 2))) (*.p16 (/.p16 x (+.p16 (+.p16 (*.p16 (*.p16 x x) (real->posit16 0.7715471019)) (real->posit16 1)) (*.p16 (*.p16 (*.p16 x x) (*.p16 x x)) (+.p16 (+.p16 (*.p16 (*.p16 x x) (real->posit16 0.0694555761)) (real->posit16 0.2909738639)) (*.p16 (+.p16 (*.p16 (*.p16 x x) (+.p16 (real->posit16 0.0008327945) (*.p16 (*.p16 x x) (*.p16 (real->posit16 0.0001789971) (real->posit16 2))))) (real->posit16 0.0140005442)) (*.p16 (*.p16 x x) (*.p16 x x))))))) (+.p16 (*.p16 (*.p16 x x) (+.p16 (*.p16 (+.p16 (*.p16 (*.p16 x x) (+.p16 (+.p16 (*.p16 (real->posit16 0.0005064034) (*.p16 x x)) (*.p16 (*.p16 (*.p16 x x) (*.p16 x x)) (real->posit16 0.0001789971))) (real->posit16 0.0072644182))) (real->posit16 0.0424060604)) (*.p16 x x)) (real->posit16 0.1049934947))) (real->posit16 1))) (*.p16 (/.p16 x (+.p16 (+.p16 (*.p16 (*.p16 x x) (real->posit16 0.7715471019)) (real->posit16 1)) (*.p16 (*.p16 (*.p16 x x) (*.p16 x x)) (+.p16 (+.p16 (*.p16 (*.p16 x x) (real->posit16 0.0694555761)) (real->posit16 0.2909738639)) (*.p16 (+.p16 (*.p16 (*.p16 x x) (+.p16 (real->posit16 0.0008327945) (*.p16 (*.p16 x x) (*.p16 (real->posit16 0.0001789971) (real->posit16 2))))) (real->posit16 0.0140005442)) (*.p16 (*.p16 x x) (*.p16 x x))))))) (+.p16 (*.p16 (*.p16 x x) (+.p16 (*.p16 (+.p16 (*.p16 (*.p16 x x) (+.p16 (+.p16 (*.p16 (real->posit16 0.0005064034) (*.p16 x x)) (*.p16 (*.p16 (*.p16 x x) (*.p16 x x)) (real->posit16 0.0001789971))) (real->posit16 0.0072644182))) (real->posit16 0.0424060604)) (*.p16 x x)) (real->posit16 0.1049934947))) (real->posit16 1))) (*.p16 (/.p16 x (+.p16 (+.p16 (*.p16 (*.p16 x x) (real->posit16 0.7715471019)) (real->posit16 1)) (*.p16 (*.p16 (*.p16 x x) (*.p16 x x)) (+.p16 (+.p16 (*.p16 (*.p16 x x) (real->posit16 0.0694555761)) (real->posit16 0.2909738639)) (*.p16 (+.p16 (*.p16 (*.p16 x x) (+.p16 (real->posit16 0.0008327945) (*.p16 (*.p16 x x) (*.p16 (real->posit16 0.0001789971) (real->posit16 2))))) (real->posit16 0.0140005442)) (*.p16 (*.p16 x x) (*.p16 x x))))))) (+.p16 (*.p16 (*.p16 x x) (+.p16 (*.p16 (+.p16 (*.p16 (*.p16 x x) (+.p16 (+.p16 (*.p16 (real->posit16 0.0005064034) (*.p16 x x)) (*.p16 (*.p16 (*.p16 x x) (*.p16 x x)) (real->posit16 0.0001789971))) (real->posit16 0.0072644182))) (real->posit16 0.0424060604)) (*.p16 x x)) (real->posit16 0.1049934947))) (real->posit16 1))) (*.p16 (/.p16 x (+.p16 (+.p16 (*.p16 (*.p16 x x) (real->posit16 0.7715471019)) (real->posit16 1)) (*.p16 (*.p16 (*.p16 x x) (*.p16 x x)) (+.p16 (+.p16 (*.p16 (*.p16 x x) (real->posit16 0.0694555761)) (real->posit16 0.2909738639)) (*.p16 (+.p16 (*.p16 (*.p16 x x) (+.p16 (real->posit16 0.0008327945) (*.p16 (*.p16 x x) (*.p16 (real->posit16 0.0001789971) (real->posit16 2))))) (real->posit16 0.0140005442)) (*.p16 (*.p16 x x) (*.p16 x x))))))) (+.p16 (*.p16 (*.p16 x x) (+.p16 (*.p16 (+.p16 (*.p16 (*.p16 x x) (+.p16 (+.p16 (*.p16 (real->posit16 0.0005064034) (*.p16 x x)) (*.p16 (*.p16 (*.p16 x x) (*.p16 x x)) (real->posit16 0.0001789971))) (real->posit16 0.0072644182))) (real->posit16 0.0424060604)) (*.p16 x x)) (real->posit16 0.1049934947))) (real->posit16 1))) 11.416 * * [simplify]: iteration 1: (60 enodes) 11.445 * * [simplify]: iteration 2: (178 enodes) 11.527 * * [simplify]: iteration 3: (509 enodes) 11.845 * * [simplify]: iteration 4: (1753 enodes) 14.664 * * [simplify]: Extracting #0: cost 7 inf + 0 14.664 * * [simplify]: Extracting #1: cost 69 inf + 0 14.665 * * [simplify]: Extracting #2: cost 420 inf + 322 14.669 * * [simplify]: Extracting #3: cost 1005 inf + 4181 14.677 * * [simplify]: Extracting #4: cost 1331 inf + 89630 14.710 * * [simplify]: Extracting #5: cost 1192 inf + 371504 14.781 * * [simplify]: Extracting #6: cost 881 inf + 911884 14.931 * * [simplify]: Extracting #7: cost 300 inf + 2298124 15.163 * * [simplify]: Extracting #8: cost 54 inf + 3258890 15.508 * * [simplify]: Extracting #9: cost 0 inf + 3493420 15.873 * * [simplify]: Extracting #10: cost 0 inf + 3473260 16.282 * * [simplify]: Extracting #11: cost 0 inf + 3467500 16.760 * * [simplify]: Extracting #12: cost 0 inf + 3419500 17.125 * * [simplify]: Extracting #13: cost 0 inf + 3403180 17.414 * [simplify]: Simplified to: (*.p16 (/.p16 (*.p16 x x) (+.p16 (*.p16 (+.p16 (real->posit16 0.7715471019) (*.p16 (*.p16 x x) (+.p16 (*.p16 (+.p16 (*.p16 (*.p16 x x) (+.p16 (*.p16 (*.p16 (*.p16 x x) (real->posit16 2)) (*.p16 (real->posit16 0.0001789971) (*.p16 x x))) (+.p16 (real->posit16 0.0140005442) (*.p16 (*.p16 x x) (real->posit16 0.0008327945))))) (real->posit16 0.0694555761)) (*.p16 x x)) (real->posit16 0.2909738639)))) (*.p16 x x)) (real->posit16 1))) (*.p16 x (+.p16 (*.p16 (*.p16 x x) (+.p16 (*.p16 (*.p16 x x) (+.p16 (*.p16 (+.p16 (real->posit16 0.0005064034) (*.p16 (real->posit16 0.0001789971) (*.p16 x x))) (*.p16 x x)) (real->posit16 0.0072644182))) (real->posit16 0.0424060604))) (real->posit16 0.1049934947)))) (/.p16 (*.p16 (real->posit16 1) x) (+.p16 (*.p16 (+.p16 (real->posit16 0.7715471019) (*.p16 (*.p16 x x) (+.p16 (*.p16 (+.p16 (*.p16 (*.p16 x x) (+.p16 (*.p16 (*.p16 (*.p16 x x) (real->posit16 2)) (*.p16 (real->posit16 0.0001789971) (*.p16 x x))) (+.p16 (real->posit16 0.0140005442) (*.p16 (*.p16 x x) (real->posit16 0.0008327945))))) (real->posit16 0.0694555761)) (*.p16 x x)) (real->posit16 0.2909738639)))) (*.p16 x x)) (real->posit16 1))) (*.p16 (/.p16 (*.p16 x x) (+.p16 (*.p16 (+.p16 (real->posit16 0.7715471019) (*.p16 (*.p16 x x) (+.p16 (*.p16 (+.p16 (*.p16 (*.p16 x x) (+.p16 (*.p16 (*.p16 (*.p16 x x) (real->posit16 2)) (*.p16 (real->posit16 0.0001789971) (*.p16 x x))) (+.p16 (real->posit16 0.0140005442) (*.p16 (*.p16 x x) (real->posit16 0.0008327945))))) (real->posit16 0.0694555761)) (*.p16 x x)) (real->posit16 0.2909738639)))) (*.p16 x x)) (real->posit16 1))) (*.p16 x (+.p16 (*.p16 (*.p16 x x) (+.p16 (*.p16 (*.p16 x x) (+.p16 (*.p16 (+.p16 (real->posit16 0.0005064034) (*.p16 (real->posit16 0.0001789971) (*.p16 x x))) (*.p16 x x)) (real->posit16 0.0072644182))) (real->posit16 0.0424060604))) (real->posit16 0.1049934947)))) (/.p16 (*.p16 (real->posit16 1) x) (+.p16 (*.p16 (+.p16 (real->posit16 0.7715471019) (*.p16 (*.p16 x x) (+.p16 (*.p16 (+.p16 (*.p16 (*.p16 x x) (+.p16 (*.p16 (*.p16 (*.p16 x x) (real->posit16 2)) (*.p16 (real->posit16 0.0001789971) (*.p16 x x))) (+.p16 (real->posit16 0.0140005442) (*.p16 (*.p16 x x) (real->posit16 0.0008327945))))) (real->posit16 0.0694555761)) (*.p16 x x)) (real->posit16 0.2909738639)))) (*.p16 x x)) (real->posit16 1))) (*.p16 x (+.p16 (real->posit16 1) (*.p16 (*.p16 x x) (+.p16 (*.p16 (*.p16 x x) (+.p16 (*.p16 (*.p16 x x) (+.p16 (*.p16 (+.p16 (real->posit16 0.0005064034) (*.p16 (real->posit16 0.0001789971) (*.p16 x x))) (*.p16 x x)) (real->posit16 0.0072644182))) (real->posit16 0.0424060604))) (real->posit16 0.1049934947))))) (*.p16 (real->posit16 0.0001789971) (*.p16 x x)) (*.p16 (real->posit16 0.0005064034) x) (*.p16 (real->posit16 0.0001789971) (*.p16 x x)) (*.p16 (*.p16 (real->posit16 2) (real->posit16 0.0001789971)) x) (/.p16 (*.p16 x (+.p16 (real->posit16 1) (*.p16 (*.p16 x x) (+.p16 (*.p16 (*.p16 x x) (+.p16 (*.p16 (*.p16 x x) (+.p16 (*.p16 (+.p16 (real->posit16 0.0005064034) (*.p16 (real->posit16 0.0001789971) (*.p16 x x))) (*.p16 x x)) (real->posit16 0.0072644182))) (real->posit16 0.0424060604))) (real->posit16 0.1049934947))))) (+.p16 (*.p16 (+.p16 (real->posit16 0.7715471019) (*.p16 (*.p16 x x) (+.p16 (*.p16 (+.p16 (*.p16 (*.p16 x x) (+.p16 (*.p16 (*.p16 (*.p16 x x) (real->posit16 2)) (*.p16 (real->posit16 0.0001789971) (*.p16 x x))) (+.p16 (real->posit16 0.0140005442) (*.p16 (*.p16 x x) (real->posit16 0.0008327945))))) (real->posit16 0.0694555761)) (*.p16 x x)) (real->posit16 0.2909738639)))) (*.p16 x x)) (real->posit16 1))) (/.p16 (*.p16 x (+.p16 (real->posit16 1) (*.p16 (*.p16 x x) (+.p16 (*.p16 (*.p16 x x) (+.p16 (*.p16 (*.p16 x x) (+.p16 (*.p16 (+.p16 (real->posit16 0.0005064034) (*.p16 (real->posit16 0.0001789971) (*.p16 x x))) (*.p16 x x)) (real->posit16 0.0072644182))) (real->posit16 0.0424060604))) (real->posit16 0.1049934947))))) (+.p16 (*.p16 (+.p16 (real->posit16 0.7715471019) (*.p16 (*.p16 x x) (+.p16 (*.p16 (+.p16 (*.p16 (*.p16 x x) (+.p16 (*.p16 (*.p16 (*.p16 x x) (real->posit16 2)) (*.p16 (real->posit16 0.0001789971) (*.p16 x x))) (+.p16 (real->posit16 0.0140005442) (*.p16 (*.p16 x x) (real->posit16 0.0008327945))))) (real->posit16 0.0694555761)) (*.p16 x x)) (real->posit16 0.2909738639)))) (*.p16 x x)) (real->posit16 1))) (/.p16 (*.p16 x (+.p16 (real->posit16 1) (*.p16 (*.p16 x x) (+.p16 (*.p16 (*.p16 x x) (+.p16 (*.p16 (*.p16 x x) (+.p16 (*.p16 (+.p16 (real->posit16 0.0005064034) (*.p16 (real->posit16 0.0001789971) (*.p16 x x))) (*.p16 x x)) (real->posit16 0.0072644182))) (real->posit16 0.0424060604))) (real->posit16 0.1049934947))))) (+.p16 (*.p16 (+.p16 (real->posit16 0.7715471019) (*.p16 (*.p16 x x) (+.p16 (*.p16 (+.p16 (*.p16 (*.p16 x x) (+.p16 (*.p16 (*.p16 (*.p16 x x) (real->posit16 2)) (*.p16 (real->posit16 0.0001789971) (*.p16 x x))) (+.p16 (real->posit16 0.0140005442) (*.p16 (*.p16 x x) (real->posit16 0.0008327945))))) (real->posit16 0.0694555761)) (*.p16 x x)) (real->posit16 0.2909738639)))) (*.p16 x x)) (real->posit16 1))) (/.p16 (*.p16 x (+.p16 (real->posit16 1) (*.p16 (*.p16 x x) (+.p16 (*.p16 (*.p16 x x) (+.p16 (*.p16 (*.p16 x x) (+.p16 (*.p16 (+.p16 (real->posit16 0.0005064034) (*.p16 (real->posit16 0.0001789971) (*.p16 x x))) (*.p16 x x)) (real->posit16 0.0072644182))) (real->posit16 0.0424060604))) (real->posit16 0.1049934947))))) (+.p16 (*.p16 (+.p16 (real->posit16 0.7715471019) (*.p16 (*.p16 x x) (+.p16 (*.p16 (+.p16 (*.p16 (*.p16 x x) (+.p16 (*.p16 (*.p16 (*.p16 x x) (real->posit16 2)) (*.p16 (real->posit16 0.0001789971) (*.p16 x x))) (+.p16 (real->posit16 0.0140005442) (*.p16 (*.p16 x x) (real->posit16 0.0008327945))))) (real->posit16 0.0694555761)) (*.p16 x x)) (real->posit16 0.2909738639)))) (*.p16 x x)) (real->posit16 1))) 17.420 * * * [progress]: adding candidates to table 20.847 * * [progress]: iteration 3 / 4 20.847 * * * [progress]: picking best candidate 21.268 * * * * [pick]: Picked #posit16 1) (*.p16 (*.p16 x x) (+.p16 (*.p16 (*.p16 x x) (+.p16 (*.p16 (*.p16 x x) (+.p16 (*.p16 (+.p16 (real->posit16 0.0005064034) (*.p16 (real->posit16 0.0001789971) (*.p16 x x))) (*.p16 x x)) (real->posit16 0.0072644182))) (real->posit16 0.0424060604))) (real->posit16 0.1049934947))))) (+.p16 (*.p16 (+.p16 (real->posit16 0.7715471019) (*.p16 (*.p16 x x) (+.p16 (*.p16 (+.p16 (*.p16 (*.p16 x x) (+.p16 (*.p16 (*.p16 (*.p16 x x) (real->posit16 2)) (*.p16 (real->posit16 0.0001789971) (*.p16 x x))) (+.p16 (real->posit16 0.0140005442) (*.p16 (*.p16 x x) (real->posit16 0.0008327945))))) (real->posit16 0.0694555761)) (*.p16 x x)) (real->posit16 0.2909738639)))) (*.p16 x x)) (real->posit16 1))))> 21.268 * * * [progress]: localizing error 22.307 * * * [progress]: generating rewritten candidates 22.307 * * * * [progress]: [ 1 / 4 ] rewriting at (2) 22.312 * * * * [progress]: [ 2 / 4 ] rewriting at (2 2 1 1 2 2 1 1 1 2 2 2) 22.315 * * * * [progress]: [ 3 / 4 ] rewriting at (2 2 1 1 2 2 1 1 1 2 1 2) 22.325 * * * * [progress]: [ 4 / 4 ] rewriting at (2 1 2 2 2 1 2 1 2 1 1 2) 22.329 * * * [progress]: generating series expansions 22.329 * * * * [progress]: [ 1 / 4 ] generating series at (2) 22.329 * * * * [progress]: [ 2 / 4 ] generating series at (2 2 1 1 2 2 1 1 1 2 2 2) 22.329 * * * * [progress]: [ 3 / 4 ] generating series at (2 2 1 1 2 2 1 1 1 2 1 2) 22.329 * * * * [progress]: [ 4 / 4 ] generating series at (2 1 2 2 2 1 2 1 2 1 1 2) 22.329 * * * [progress]: simplifying candidates 22.329 * * * * [progress]: [ 1 / 11 ] simplifiying candidate #posit16 0.7715471019) (*.p16 (*.p16 x x) (+.p16 (*.p16 (+.p16 (*.p16 (*.p16 x x) (+.p16 (*.p16 (*.p16 (*.p16 x x) (real->posit16 2)) (*.p16 (real->posit16 0.0001789971) (*.p16 x x))) (+.p16 (real->posit16 0.0140005442) (*.p16 (*.p16 x x) (real->posit16 0.0008327945))))) (real->posit16 0.0694555761)) (*.p16 x x)) (real->posit16 0.2909738639)))) (*.p16 x x)) (real->posit16 1)) (+.p16 (real->posit16 1) (*.p16 (*.p16 x x) (+.p16 (*.p16 (*.p16 x x) (+.p16 (*.p16 (*.p16 x x) (+.p16 (*.p16 (+.p16 (real->posit16 0.0005064034) (*.p16 (real->posit16 0.0001789971) (*.p16 x x))) (*.p16 x x)) (real->posit16 0.0072644182))) (real->posit16 0.0424060604))) (real->posit16 0.1049934947)))))))> 22.329 * * * * [progress]: [ 2 / 11 ] simplifiying candidate #posit16 1) (*.p16 (*.p16 x x) (+.p16 (*.p16 (*.p16 x x) (+.p16 (*.p16 (*.p16 x x) (+.p16 (*.p16 (+.p16 (real->posit16 0.0005064034) (*.p16 (real->posit16 0.0001789971) (*.p16 x x))) (*.p16 x x)) (real->posit16 0.0072644182))) (real->posit16 0.0424060604))) (real->posit16 0.1049934947))))) (+.p16 (*.p16 (+.p16 (real->posit16 0.7715471019) (*.p16 (*.p16 x x) (+.p16 (*.p16 (+.p16 (*.p16 (*.p16 x x) (+.p16 (*.p16 (*.p16 (*.p16 x x) (real->posit16 2)) (*.p16 (real->posit16 0.0001789971) (*.p16 x x))) (+.p16 (real->posit16 0.0140005442) (*.p16 x (*.p16 x (real->posit16 0.0008327945)))))) (real->posit16 0.0694555761)) (*.p16 x x)) (real->posit16 0.2909738639)))) (*.p16 x x)) (real->posit16 1))))> 22.329 * * * * [progress]: [ 3 / 11 ] simplifiying candidate #posit16 1) (*.p16 (*.p16 x x) (+.p16 (*.p16 (*.p16 x x) (+.p16 (*.p16 (*.p16 x x) (+.p16 (*.p16 (+.p16 (real->posit16 0.0005064034) (*.p16 (real->posit16 0.0001789971) (*.p16 x x))) (*.p16 x x)) (real->posit16 0.0072644182))) (real->posit16 0.0424060604))) (real->posit16 0.1049934947))))) (+.p16 (*.p16 (+.p16 (real->posit16 0.7715471019) (*.p16 (*.p16 x x) (+.p16 (*.p16 (+.p16 (*.p16 (*.p16 x x) (+.p16 (*.p16 (*.p16 (*.p16 x x) (real->posit16 2)) (*.p16 (real->posit16 0.0001789971) (*.p16 x x))) (+.p16 (real->posit16 0.0140005442) (*.p16 (real->posit16 0.0008327945) (*.p16 x x))))) (real->posit16 0.0694555761)) (*.p16 x x)) (real->posit16 0.2909738639)))) (*.p16 x x)) (real->posit16 1))))> 22.329 * * * * [progress]: [ 4 / 11 ] simplifiying candidate #posit16 1) (*.p16 (*.p16 x x) (+.p16 (*.p16 (*.p16 x x) (+.p16 (*.p16 (*.p16 x x) (+.p16 (*.p16 (+.p16 (real->posit16 0.0005064034) (*.p16 (real->posit16 0.0001789971) (*.p16 x x))) (*.p16 x x)) (real->posit16 0.0072644182))) (real->posit16 0.0424060604))) (real->posit16 0.1049934947))))) (+.p16 (*.p16 (+.p16 (real->posit16 0.7715471019) (*.p16 (*.p16 x x) (+.p16 (*.p16 (+.p16 (*.p16 (*.p16 x x) (+.p16 (*.p16 (*.p16 (*.p16 x x) (real->posit16 2)) (*.p16 (*.p16 (real->posit16 0.0001789971) x) x)) (+.p16 (real->posit16 0.0140005442) (*.p16 (*.p16 x x) (real->posit16 0.0008327945))))) (real->posit16 0.0694555761)) (*.p16 x x)) (real->posit16 0.2909738639)))) (*.p16 x x)) (real->posit16 1))))> 22.330 * * * * [progress]: [ 5 / 11 ] simplifiying candidate #posit16 1) (*.p16 (*.p16 x x) (+.p16 (*.p16 (*.p16 x x) (+.p16 (*.p16 (*.p16 x x) (+.p16 (*.p16 (+.p16 (real->posit16 0.0005064034) (*.p16 (real->posit16 0.0001789971) (*.p16 x x))) (*.p16 x x)) (real->posit16 0.0072644182))) (real->posit16 0.0424060604))) (real->posit16 0.1049934947))))) (+.p16 (*.p16 (+.p16 (real->posit16 0.7715471019) (*.p16 (*.p16 x x) (+.p16 (*.p16 (+.p16 (*.p16 (*.p16 x x) (+.p16 (*.p16 (*.p16 (*.p16 x x) (real->posit16 2)) (*.p16 (*.p16 x x) (real->posit16 0.0001789971))) (+.p16 (real->posit16 0.0140005442) (*.p16 (*.p16 x x) (real->posit16 0.0008327945))))) (real->posit16 0.0694555761)) (*.p16 x x)) (real->posit16 0.2909738639)))) (*.p16 x x)) (real->posit16 1))))> 22.330 * * * * [progress]: [ 6 / 11 ] simplifiying candidate #posit16 1) (*.p16 (*.p16 x x) (+.p16 (*.p16 (*.p16 x x) (+.p16 (*.p16 (*.p16 x x) (+.p16 (*.p16 (+.p16 (real->posit16 0.0005064034) (*.p16 (*.p16 (real->posit16 0.0001789971) x) x)) (*.p16 x x)) (real->posit16 0.0072644182))) (real->posit16 0.0424060604))) (real->posit16 0.1049934947))))) (+.p16 (*.p16 (+.p16 (real->posit16 0.7715471019) (*.p16 (*.p16 x x) (+.p16 (*.p16 (+.p16 (*.p16 (*.p16 x x) (+.p16 (*.p16 (*.p16 (*.p16 x x) (real->posit16 2)) (*.p16 (real->posit16 0.0001789971) (*.p16 x x))) (+.p16 (real->posit16 0.0140005442) (*.p16 (*.p16 x x) (real->posit16 0.0008327945))))) (real->posit16 0.0694555761)) (*.p16 x x)) (real->posit16 0.2909738639)))) (*.p16 x x)) (real->posit16 1))))> 22.330 * * * * [progress]: [ 7 / 11 ] simplifiying candidate #posit16 1) (*.p16 (*.p16 x x) (+.p16 (*.p16 (*.p16 x x) (+.p16 (*.p16 (*.p16 x x) (+.p16 (*.p16 (+.p16 (real->posit16 0.0005064034) (*.p16 (*.p16 x x) (real->posit16 0.0001789971))) (*.p16 x x)) (real->posit16 0.0072644182))) (real->posit16 0.0424060604))) (real->posit16 0.1049934947))))) (+.p16 (*.p16 (+.p16 (real->posit16 0.7715471019) (*.p16 (*.p16 x x) (+.p16 (*.p16 (+.p16 (*.p16 (*.p16 x x) (+.p16 (*.p16 (*.p16 (*.p16 x x) (real->posit16 2)) (*.p16 (real->posit16 0.0001789971) (*.p16 x x))) (+.p16 (real->posit16 0.0140005442) (*.p16 (*.p16 x x) (real->posit16 0.0008327945))))) (real->posit16 0.0694555761)) (*.p16 x x)) (real->posit16 0.2909738639)))) (*.p16 x x)) (real->posit16 1))))> 22.330 * * * * [progress]: [ 8 / 11 ] simplifiying candidate #posit16 1) (*.p16 (*.p16 x x) (+.p16 (*.p16 (*.p16 x x) (+.p16 (*.p16 (*.p16 x x) (+.p16 (*.p16 (+.p16 (real->posit16 0.0005064034) (*.p16 (real->posit16 0.0001789971) (*.p16 x x))) (*.p16 x x)) (real->posit16 0.0072644182))) (real->posit16 0.0424060604))) (real->posit16 0.1049934947))))) (+.p16 (*.p16 (+.p16 (real->posit16 0.7715471019) (*.p16 (*.p16 x x) (+.p16 (*.p16 (+.p16 (*.p16 (*.p16 x x) (+.p16 (*.p16 (*.p16 (*.p16 x x) (real->posit16 2)) (*.p16 (real->posit16 0.0001789971) (*.p16 x x))) (+.p16 (real->posit16 0.0140005442) (*.p16 (*.p16 x x) (real->posit16 0.0008327945))))) (real->posit16 0.0694555761)) (*.p16 x x)) (real->posit16 0.2909738639)))) (*.p16 x x)) (real->posit16 1))))> 22.330 * * * * [progress]: [ 9 / 11 ] simplifiying candidate #posit16 1) (*.p16 (*.p16 x x) (+.p16 (*.p16 (*.p16 x x) (+.p16 (*.p16 (*.p16 x x) (+.p16 (*.p16 (+.p16 (real->posit16 0.0005064034) (*.p16 (real->posit16 0.0001789971) (*.p16 x x))) (*.p16 x x)) (real->posit16 0.0072644182))) (real->posit16 0.0424060604))) (real->posit16 0.1049934947))))) (+.p16 (*.p16 (+.p16 (real->posit16 0.7715471019) (*.p16 (*.p16 x x) (+.p16 (*.p16 (+.p16 (*.p16 (*.p16 x x) (+.p16 (*.p16 (*.p16 (*.p16 x x) (real->posit16 2)) (*.p16 (real->posit16 0.0001789971) (*.p16 x x))) (+.p16 (real->posit16 0.0140005442) (*.p16 (*.p16 x x) (real->posit16 0.0008327945))))) (real->posit16 0.0694555761)) (*.p16 x x)) (real->posit16 0.2909738639)))) (*.p16 x x)) (real->posit16 1))))> 22.330 * * * * [progress]: [ 10 / 11 ] simplifiying candidate #posit16 1) (*.p16 (*.p16 x x) (+.p16 (*.p16 (*.p16 x x) (+.p16 (*.p16 (*.p16 x x) (+.p16 (*.p16 (+.p16 (real->posit16 0.0005064034) (*.p16 (real->posit16 0.0001789971) (*.p16 x x))) (*.p16 x x)) (real->posit16 0.0072644182))) (real->posit16 0.0424060604))) (real->posit16 0.1049934947))))) (+.p16 (*.p16 (+.p16 (real->posit16 0.7715471019) (*.p16 (*.p16 x x) (+.p16 (*.p16 (+.p16 (*.p16 (*.p16 x x) (+.p16 (*.p16 (*.p16 (*.p16 x x) (real->posit16 2)) (*.p16 (real->posit16 0.0001789971) (*.p16 x x))) (+.p16 (real->posit16 0.0140005442) (*.p16 (*.p16 x x) (real->posit16 0.0008327945))))) (real->posit16 0.0694555761)) (*.p16 x x)) (real->posit16 0.2909738639)))) (*.p16 x x)) (real->posit16 1))))> 22.330 * * * * [progress]: [ 11 / 11 ] simplifiying candidate #posit16 1) (*.p16 (*.p16 x x) (+.p16 (*.p16 (*.p16 x x) (+.p16 (*.p16 (*.p16 x x) (+.p16 (*.p16 (+.p16 (real->posit16 0.0005064034) (*.p16 (real->posit16 0.0001789971) (*.p16 x x))) (*.p16 x x)) (real->posit16 0.0072644182))) (real->posit16 0.0424060604))) (real->posit16 0.1049934947))))) (+.p16 (*.p16 (+.p16 (real->posit16 0.7715471019) (*.p16 (*.p16 x x) (+.p16 (*.p16 (+.p16 (*.p16 (*.p16 x x) (+.p16 (*.p16 (*.p16 (*.p16 x x) (real->posit16 2)) (*.p16 (real->posit16 0.0001789971) (*.p16 x x))) (+.p16 (real->posit16 0.0140005442) (*.p16 (*.p16 x x) (real->posit16 0.0008327945))))) (real->posit16 0.0694555761)) (*.p16 x x)) (real->posit16 0.2909738639)))) (*.p16 x x)) (real->posit16 1))))> 22.330 * [simplify]: Simplifying: (/.p16 (+.p16 (*.p16 (+.p16 (real->posit16 0.7715471019) (*.p16 (*.p16 x x) (+.p16 (*.p16 (+.p16 (*.p16 (*.p16 x x) (+.p16 (*.p16 (*.p16 (*.p16 x x) (real->posit16 2)) (*.p16 (real->posit16 0.0001789971) (*.p16 x x))) (+.p16 (real->posit16 0.0140005442) (*.p16 (*.p16 x x) (real->posit16 0.0008327945))))) (real->posit16 0.0694555761)) (*.p16 x x)) (real->posit16 0.2909738639)))) (*.p16 x x)) (real->posit16 1)) (+.p16 (real->posit16 1) (*.p16 (*.p16 x x) (+.p16 (*.p16 (*.p16 x x) (+.p16 (*.p16 (*.p16 x x) (+.p16 (*.p16 (+.p16 (real->posit16 0.0005064034) (*.p16 (real->posit16 0.0001789971) (*.p16 x x))) (*.p16 x x)) (real->posit16 0.0072644182))) (real->posit16 0.0424060604))) (real->posit16 0.1049934947))))) (*.p16 x (real->posit16 0.0008327945)) (*.p16 (real->posit16 0.0001789971) x) (*.p16 (real->posit16 0.0001789971) x) (/.p16 (*.p16 x (+.p16 (real->posit16 1) (*.p16 (*.p16 x x) (+.p16 (*.p16 (*.p16 x x) (+.p16 (*.p16 (*.p16 x x) (+.p16 (*.p16 (+.p16 (real->posit16 0.0005064034) (*.p16 (real->posit16 0.0001789971) (*.p16 x x))) (*.p16 x x)) (real->posit16 0.0072644182))) (real->posit16 0.0424060604))) (real->posit16 0.1049934947))))) (+.p16 (*.p16 (+.p16 (real->posit16 0.7715471019) (*.p16 (*.p16 x x) (+.p16 (*.p16 (+.p16 (*.p16 (*.p16 x x) (+.p16 (*.p16 (*.p16 (*.p16 x x) (real->posit16 2)) (*.p16 (real->posit16 0.0001789971) (*.p16 x x))) (+.p16 (real->posit16 0.0140005442) (*.p16 (*.p16 x x) (real->posit16 0.0008327945))))) (real->posit16 0.0694555761)) (*.p16 x x)) (real->posit16 0.2909738639)))) (*.p16 x x)) (real->posit16 1))) (/.p16 (*.p16 x (+.p16 (real->posit16 1) (*.p16 (*.p16 x x) (+.p16 (*.p16 (*.p16 x x) (+.p16 (*.p16 (*.p16 x x) (+.p16 (*.p16 (+.p16 (real->posit16 0.0005064034) (*.p16 (real->posit16 0.0001789971) (*.p16 x x))) (*.p16 x x)) (real->posit16 0.0072644182))) (real->posit16 0.0424060604))) (real->posit16 0.1049934947))))) (+.p16 (*.p16 (+.p16 (real->posit16 0.7715471019) (*.p16 (*.p16 x x) (+.p16 (*.p16 (+.p16 (*.p16 (*.p16 x x) (+.p16 (*.p16 (*.p16 (*.p16 x x) (real->posit16 2)) (*.p16 (real->posit16 0.0001789971) (*.p16 x x))) (+.p16 (real->posit16 0.0140005442) (*.p16 (*.p16 x x) (real->posit16 0.0008327945))))) (real->posit16 0.0694555761)) (*.p16 x x)) (real->posit16 0.2909738639)))) (*.p16 x x)) (real->posit16 1))) (/.p16 (*.p16 x (+.p16 (real->posit16 1) (*.p16 (*.p16 x x) (+.p16 (*.p16 (*.p16 x x) (+.p16 (*.p16 (*.p16 x x) (+.p16 (*.p16 (+.p16 (real->posit16 0.0005064034) (*.p16 (real->posit16 0.0001789971) (*.p16 x x))) (*.p16 x x)) (real->posit16 0.0072644182))) (real->posit16 0.0424060604))) (real->posit16 0.1049934947))))) (+.p16 (*.p16 (+.p16 (real->posit16 0.7715471019) (*.p16 (*.p16 x x) (+.p16 (*.p16 (+.p16 (*.p16 (*.p16 x x) (+.p16 (*.p16 (*.p16 (*.p16 x x) (real->posit16 2)) (*.p16 (real->posit16 0.0001789971) (*.p16 x x))) (+.p16 (real->posit16 0.0140005442) (*.p16 (*.p16 x x) (real->posit16 0.0008327945))))) (real->posit16 0.0694555761)) (*.p16 x x)) (real->posit16 0.2909738639)))) (*.p16 x x)) (real->posit16 1))) (/.p16 (*.p16 x (+.p16 (real->posit16 1) (*.p16 (*.p16 x x) (+.p16 (*.p16 (*.p16 x x) (+.p16 (*.p16 (*.p16 x x) (+.p16 (*.p16 (+.p16 (real->posit16 0.0005064034) (*.p16 (real->posit16 0.0001789971) (*.p16 x x))) (*.p16 x x)) (real->posit16 0.0072644182))) (real->posit16 0.0424060604))) (real->posit16 0.1049934947))))) (+.p16 (*.p16 (+.p16 (real->posit16 0.7715471019) (*.p16 (*.p16 x x) (+.p16 (*.p16 (+.p16 (*.p16 (*.p16 x x) (+.p16 (*.p16 (*.p16 (*.p16 x x) (real->posit16 2)) (*.p16 (real->posit16 0.0001789971) (*.p16 x x))) (+.p16 (real->posit16 0.0140005442) (*.p16 (*.p16 x x) (real->posit16 0.0008327945))))) (real->posit16 0.0694555761)) (*.p16 x x)) (real->posit16 0.2909738639)))) (*.p16 x x)) (real->posit16 1))) 22.331 * * [simplify]: iteration 1: (54 enodes) 22.344 * * [simplify]: iteration 2: (159 enodes) 22.380 * * [simplify]: iteration 3: (445 enodes) 22.528 * * [simplify]: iteration 4: (1375 enodes) 23.606 * * [simplify]: Extracting #0: cost 4 inf + 0 23.607 * * [simplify]: Extracting #1: cost 19 inf + 0 23.607 * * [simplify]: Extracting #2: cost 119 inf + 1 23.608 * * [simplify]: Extracting #3: cost 351 inf + 1289 23.610 * * [simplify]: Extracting #4: cost 642 inf + 10310 23.615 * * [simplify]: Extracting #5: cost 740 inf + 39203 23.629 * * [simplify]: Extracting #6: cost 714 inf + 85602 23.643 * * [simplify]: Extracting #7: cost 567 inf + 299143 23.692 * * [simplify]: Extracting #8: cost 243 inf + 910402 23.775 * * [simplify]: Extracting #9: cost 63 inf + 1280246 23.880 * * [simplify]: Extracting #10: cost 1 inf + 1512306 23.991 * * [simplify]: Extracting #11: cost 0 inf + 1514596 24.103 * * [simplify]: Extracting #12: cost 0 inf + 1514276 24.303 * [simplify]: Simplified to: (/.p16 (+.p16 (*.p16 (*.p16 (*.p16 x x) (*.p16 x x)) (+.p16 (+.p16 (*.p16 (*.p16 x x) (real->posit16 0.0694555761)) (real->posit16 0.2909738639)) (*.p16 (+.p16 (*.p16 (real->posit16 2) (*.p16 (real->posit16 0.0001789971) (*.p16 (*.p16 x x) (*.p16 x x)))) (+.p16 (real->posit16 0.0140005442) (*.p16 (*.p16 x x) (real->posit16 0.0008327945)))) (*.p16 (*.p16 x x) (*.p16 x x))))) (+.p16 (*.p16 (real->posit16 0.7715471019) (*.p16 x x)) (real->posit16 1))) (+.p16 (+.p16 (real->posit16 1) (*.p16 (*.p16 x x) (real->posit16 0.1049934947))) (*.p16 (+.p16 (+.p16 (*.p16 (real->posit16 0.0005064034) (*.p16 (*.p16 x x) (*.p16 x x))) (*.p16 (*.p16 x x) (+.p16 (*.p16 (real->posit16 0.0001789971) (*.p16 (*.p16 x x) (*.p16 x x))) (real->posit16 0.0072644182)))) (real->posit16 0.0424060604)) (*.p16 (*.p16 x x) (*.p16 x x))))) (*.p16 x (real->posit16 0.0008327945)) (*.p16 x (real->posit16 0.0001789971)) (*.p16 x (real->posit16 0.0001789971)) (/.p16 (*.p16 (+.p16 (+.p16 (real->posit16 1) (*.p16 (*.p16 x x) (real->posit16 0.1049934947))) (*.p16 (+.p16 (+.p16 (*.p16 (real->posit16 0.0005064034) (*.p16 (*.p16 x x) (*.p16 x x))) (*.p16 (*.p16 x x) (+.p16 (*.p16 (real->posit16 0.0001789971) (*.p16 (*.p16 x x) (*.p16 x x))) (real->posit16 0.0072644182)))) (real->posit16 0.0424060604)) (*.p16 (*.p16 x x) (*.p16 x x)))) x) (+.p16 (*.p16 (*.p16 (*.p16 x x) (*.p16 x x)) (+.p16 (+.p16 (*.p16 (*.p16 x x) (real->posit16 0.0694555761)) (real->posit16 0.2909738639)) (*.p16 (+.p16 (*.p16 (real->posit16 2) (*.p16 (real->posit16 0.0001789971) (*.p16 (*.p16 x x) (*.p16 x x)))) (+.p16 (real->posit16 0.0140005442) (*.p16 (*.p16 x x) (real->posit16 0.0008327945)))) (*.p16 (*.p16 x x) (*.p16 x x))))) (+.p16 (*.p16 (real->posit16 0.7715471019) (*.p16 x x)) (real->posit16 1)))) (/.p16 (*.p16 (+.p16 (+.p16 (real->posit16 1) (*.p16 (*.p16 x x) (real->posit16 0.1049934947))) (*.p16 (+.p16 (+.p16 (*.p16 (real->posit16 0.0005064034) (*.p16 (*.p16 x x) (*.p16 x x))) (*.p16 (*.p16 x x) (+.p16 (*.p16 (real->posit16 0.0001789971) (*.p16 (*.p16 x x) (*.p16 x x))) (real->posit16 0.0072644182)))) (real->posit16 0.0424060604)) (*.p16 (*.p16 x x) (*.p16 x x)))) x) (+.p16 (*.p16 (*.p16 (*.p16 x x) (*.p16 x x)) (+.p16 (+.p16 (*.p16 (*.p16 x x) (real->posit16 0.0694555761)) (real->posit16 0.2909738639)) (*.p16 (+.p16 (*.p16 (real->posit16 2) (*.p16 (real->posit16 0.0001789971) (*.p16 (*.p16 x x) (*.p16 x x)))) (+.p16 (real->posit16 0.0140005442) (*.p16 (*.p16 x x) (real->posit16 0.0008327945)))) (*.p16 (*.p16 x x) (*.p16 x x))))) (+.p16 (*.p16 (real->posit16 0.7715471019) (*.p16 x x)) (real->posit16 1)))) (/.p16 (*.p16 (+.p16 (+.p16 (real->posit16 1) (*.p16 (*.p16 x x) (real->posit16 0.1049934947))) (*.p16 (+.p16 (+.p16 (*.p16 (real->posit16 0.0005064034) (*.p16 (*.p16 x x) (*.p16 x x))) (*.p16 (*.p16 x x) (+.p16 (*.p16 (real->posit16 0.0001789971) (*.p16 (*.p16 x x) (*.p16 x x))) (real->posit16 0.0072644182)))) (real->posit16 0.0424060604)) (*.p16 (*.p16 x x) (*.p16 x x)))) x) (+.p16 (*.p16 (*.p16 (*.p16 x x) (*.p16 x x)) (+.p16 (+.p16 (*.p16 (*.p16 x x) (real->posit16 0.0694555761)) (real->posit16 0.2909738639)) (*.p16 (+.p16 (*.p16 (real->posit16 2) (*.p16 (real->posit16 0.0001789971) (*.p16 (*.p16 x x) (*.p16 x x)))) (+.p16 (real->posit16 0.0140005442) (*.p16 (*.p16 x x) (real->posit16 0.0008327945)))) (*.p16 (*.p16 x x) (*.p16 x x))))) (+.p16 (*.p16 (real->posit16 0.7715471019) (*.p16 x x)) (real->posit16 1)))) (/.p16 (*.p16 (+.p16 (+.p16 (real->posit16 1) (*.p16 (*.p16 x x) (real->posit16 0.1049934947))) (*.p16 (+.p16 (+.p16 (*.p16 (real->posit16 0.0005064034) (*.p16 (*.p16 x x) (*.p16 x x))) (*.p16 (*.p16 x x) (+.p16 (*.p16 (real->posit16 0.0001789971) (*.p16 (*.p16 x x) (*.p16 x x))) (real->posit16 0.0072644182)))) (real->posit16 0.0424060604)) (*.p16 (*.p16 x x) (*.p16 x x)))) x) (+.p16 (*.p16 (*.p16 (*.p16 x x) (*.p16 x x)) (+.p16 (+.p16 (*.p16 (*.p16 x x) (real->posit16 0.0694555761)) (real->posit16 0.2909738639)) (*.p16 (+.p16 (*.p16 (real->posit16 2) (*.p16 (real->posit16 0.0001789971) (*.p16 (*.p16 x x) (*.p16 x x)))) (+.p16 (real->posit16 0.0140005442) (*.p16 (*.p16 x x) (real->posit16 0.0008327945)))) (*.p16 (*.p16 x x) (*.p16 x x))))) (+.p16 (*.p16 (real->posit16 0.7715471019) (*.p16 x x)) (real->posit16 1)))) 24.306 * * * [progress]: adding candidates to table 26.293 * * [progress]: iteration 4 / 4 26.293 * * * [progress]: picking best candidate 26.680 * * * * [pick]: Picked #posit16 1) (*.p16 (*.p16 x x) (+.p16 (*.p16 (*.p16 x x) (+.p16 (*.p16 (*.p16 x x) (+.p16 (*.p16 (+.p16 (real->posit16 0.0005064034) (*.p16 (*.p16 (real->posit16 0.0001789971) x) x)) (*.p16 x x)) (real->posit16 0.0072644182))) (real->posit16 0.0424060604))) (real->posit16 0.1049934947))))) (+.p16 (*.p16 (+.p16 (real->posit16 0.7715471019) (*.p16 (*.p16 x x) (+.p16 (*.p16 (+.p16 (*.p16 (*.p16 x x) (+.p16 (*.p16 (*.p16 (*.p16 x x) (real->posit16 2)) (*.p16 (real->posit16 0.0001789971) (*.p16 x x))) (+.p16 (real->posit16 0.0140005442) (*.p16 (*.p16 x x) (real->posit16 0.0008327945))))) (real->posit16 0.0694555761)) (*.p16 x x)) (real->posit16 0.2909738639)))) (*.p16 x x)) (real->posit16 1))))> 26.680 * * * [progress]: localizing error 27.399 * * * [progress]: generating rewritten candidates 27.399 * * * * [progress]: [ 1 / 4 ] rewriting at (2) 27.404 * * * * [progress]: [ 2 / 4 ] rewriting at (2 2 1 1 2 2 1 1 1 2 2 2) 27.407 * * * * [progress]: [ 3 / 4 ] rewriting at (2 2 1 1 2 2 1 1 1 2 1 2) 27.411 * * * * [progress]: [ 4 / 4 ] rewriting at (2 2 1 1 2 2 1 1 1 2 1) 27.423 * * * [progress]: generating series expansions 27.423 * * * * [progress]: [ 1 / 4 ] generating series at (2) 27.423 * * * * [progress]: [ 2 / 4 ] generating series at (2 2 1 1 2 2 1 1 1 2 2 2) 27.423 * * * * [progress]: [ 3 / 4 ] generating series at (2 2 1 1 2 2 1 1 1 2 1 2) 27.423 * * * * [progress]: [ 4 / 4 ] generating series at (2 2 1 1 2 2 1 1 1 2 1) 27.423 * * * [progress]: simplifying candidates 27.423 * * * * [progress]: [ 1 / 12 ] simplifiying candidate #posit16 0.7715471019) (*.p16 (*.p16 x x) (+.p16 (*.p16 (+.p16 (*.p16 (*.p16 x x) (+.p16 (*.p16 (*.p16 (*.p16 x x) (real->posit16 2)) (*.p16 (real->posit16 0.0001789971) (*.p16 x x))) (+.p16 (real->posit16 0.0140005442) (*.p16 (*.p16 x x) (real->posit16 0.0008327945))))) (real->posit16 0.0694555761)) (*.p16 x x)) (real->posit16 0.2909738639)))) (*.p16 x x)) (real->posit16 1)) (+.p16 (real->posit16 1) (*.p16 (*.p16 x x) (+.p16 (*.p16 (*.p16 x x) (+.p16 (*.p16 (*.p16 x x) (+.p16 (*.p16 (+.p16 (real->posit16 0.0005064034) (*.p16 (*.p16 (real->posit16 0.0001789971) x) x)) (*.p16 x x)) (real->posit16 0.0072644182))) (real->posit16 0.0424060604))) (real->posit16 0.1049934947)))))))> 27.423 * * * * [progress]: [ 2 / 12 ] simplifiying candidate #posit16 1) (*.p16 (*.p16 x x) (+.p16 (*.p16 (*.p16 x x) (+.p16 (*.p16 (*.p16 x x) (+.p16 (*.p16 (+.p16 (real->posit16 0.0005064034) (*.p16 (*.p16 (real->posit16 0.0001789971) x) x)) (*.p16 x x)) (real->posit16 0.0072644182))) (real->posit16 0.0424060604))) (real->posit16 0.1049934947))))) (+.p16 (*.p16 (+.p16 (real->posit16 0.7715471019) (*.p16 (*.p16 x x) (+.p16 (*.p16 (+.p16 (*.p16 (*.p16 x x) (+.p16 (*.p16 (*.p16 (*.p16 x x) (real->posit16 2)) (*.p16 (real->posit16 0.0001789971) (*.p16 x x))) (+.p16 (real->posit16 0.0140005442) (*.p16 x (*.p16 x (real->posit16 0.0008327945)))))) (real->posit16 0.0694555761)) (*.p16 x x)) (real->posit16 0.2909738639)))) (*.p16 x x)) (real->posit16 1))))> 27.423 * * * * [progress]: [ 3 / 12 ] simplifiying candidate #posit16 1) (*.p16 (*.p16 x x) (+.p16 (*.p16 (*.p16 x x) (+.p16 (*.p16 (*.p16 x x) (+.p16 (*.p16 (+.p16 (real->posit16 0.0005064034) (*.p16 (*.p16 (real->posit16 0.0001789971) x) x)) (*.p16 x x)) (real->posit16 0.0072644182))) (real->posit16 0.0424060604))) (real->posit16 0.1049934947))))) (+.p16 (*.p16 (+.p16 (real->posit16 0.7715471019) (*.p16 (*.p16 x x) (+.p16 (*.p16 (+.p16 (*.p16 (*.p16 x x) (+.p16 (*.p16 (*.p16 (*.p16 x x) (real->posit16 2)) (*.p16 (real->posit16 0.0001789971) (*.p16 x x))) (+.p16 (real->posit16 0.0140005442) (*.p16 (real->posit16 0.0008327945) (*.p16 x x))))) (real->posit16 0.0694555761)) (*.p16 x x)) (real->posit16 0.2909738639)))) (*.p16 x x)) (real->posit16 1))))> 27.423 * * * * [progress]: [ 4 / 12 ] simplifiying candidate #posit16 1) (*.p16 (*.p16 x x) (+.p16 (*.p16 (*.p16 x x) (+.p16 (*.p16 (*.p16 x x) (+.p16 (*.p16 (+.p16 (real->posit16 0.0005064034) (*.p16 (*.p16 (real->posit16 0.0001789971) x) x)) (*.p16 x x)) (real->posit16 0.0072644182))) (real->posit16 0.0424060604))) (real->posit16 0.1049934947))))) (+.p16 (*.p16 (+.p16 (real->posit16 0.7715471019) (*.p16 (*.p16 x x) (+.p16 (*.p16 (+.p16 (*.p16 (*.p16 x x) (+.p16 (*.p16 (*.p16 (*.p16 x x) (real->posit16 2)) (*.p16 (*.p16 (real->posit16 0.0001789971) x) x)) (+.p16 (real->posit16 0.0140005442) (*.p16 (*.p16 x x) (real->posit16 0.0008327945))))) (real->posit16 0.0694555761)) (*.p16 x x)) (real->posit16 0.2909738639)))) (*.p16 x x)) (real->posit16 1))))> 27.423 * * * * [progress]: [ 5 / 12 ] simplifiying candidate #posit16 1) (*.p16 (*.p16 x x) (+.p16 (*.p16 (*.p16 x x) (+.p16 (*.p16 (*.p16 x x) (+.p16 (*.p16 (+.p16 (real->posit16 0.0005064034) (*.p16 (*.p16 (real->posit16 0.0001789971) x) x)) (*.p16 x x)) (real->posit16 0.0072644182))) (real->posit16 0.0424060604))) (real->posit16 0.1049934947))))) (+.p16 (*.p16 (+.p16 (real->posit16 0.7715471019) (*.p16 (*.p16 x x) (+.p16 (*.p16 (+.p16 (*.p16 (*.p16 x x) (+.p16 (*.p16 (*.p16 (*.p16 x x) (real->posit16 2)) (*.p16 (*.p16 x x) (real->posit16 0.0001789971))) (+.p16 (real->posit16 0.0140005442) (*.p16 (*.p16 x x) (real->posit16 0.0008327945))))) (real->posit16 0.0694555761)) (*.p16 x x)) (real->posit16 0.2909738639)))) (*.p16 x x)) (real->posit16 1))))> 27.423 * * * * [progress]: [ 6 / 12 ] simplifiying candidate #posit16 1) (*.p16 (*.p16 x x) (+.p16 (*.p16 (*.p16 x x) (+.p16 (*.p16 (*.p16 x x) (+.p16 (*.p16 (+.p16 (real->posit16 0.0005064034) (*.p16 (*.p16 (real->posit16 0.0001789971) x) x)) (*.p16 x x)) (real->posit16 0.0072644182))) (real->posit16 0.0424060604))) (real->posit16 0.1049934947))))) (+.p16 (*.p16 (+.p16 (real->posit16 0.7715471019) (*.p16 (*.p16 x x) (+.p16 (*.p16 (+.p16 (*.p16 (*.p16 x x) (+.p16 (*.p16 (*.p16 (*.p16 (*.p16 x x) (real->posit16 2)) (real->posit16 0.0001789971)) (*.p16 x x)) (+.p16 (real->posit16 0.0140005442) (*.p16 (*.p16 x x) (real->posit16 0.0008327945))))) (real->posit16 0.0694555761)) (*.p16 x x)) (real->posit16 0.2909738639)))) (*.p16 x x)) (real->posit16 1))))> 27.423 * * * * [progress]: [ 7 / 12 ] simplifiying candidate #posit16 1) (*.p16 (*.p16 x x) (+.p16 (*.p16 (*.p16 x x) (+.p16 (*.p16 (*.p16 x x) (+.p16 (*.p16 (+.p16 (real->posit16 0.0005064034) (*.p16 (*.p16 (real->posit16 0.0001789971) x) x)) (*.p16 x x)) (real->posit16 0.0072644182))) (real->posit16 0.0424060604))) (real->posit16 0.1049934947))))) (+.p16 (*.p16 (+.p16 (real->posit16 0.7715471019) (*.p16 (*.p16 x x) (+.p16 (*.p16 (+.p16 (*.p16 (*.p16 x x) (+.p16 (*.p16 (*.p16 x x) (*.p16 (real->posit16 2) (*.p16 (real->posit16 0.0001789971) (*.p16 x x)))) (+.p16 (real->posit16 0.0140005442) (*.p16 (*.p16 x x) (real->posit16 0.0008327945))))) (real->posit16 0.0694555761)) (*.p16 x x)) (real->posit16 0.2909738639)))) (*.p16 x x)) (real->posit16 1))))> 27.423 * * * * [progress]: [ 8 / 12 ] simplifiying candidate #posit16 1) (*.p16 (*.p16 x x) (+.p16 (*.p16 (*.p16 x x) (+.p16 (*.p16 (*.p16 x x) (+.p16 (*.p16 (+.p16 (real->posit16 0.0005064034) (*.p16 (*.p16 (real->posit16 0.0001789971) x) x)) (*.p16 x x)) (real->posit16 0.0072644182))) (real->posit16 0.0424060604))) (real->posit16 0.1049934947))))) (+.p16 (*.p16 (+.p16 (real->posit16 0.7715471019) (*.p16 (*.p16 x x) (+.p16 (*.p16 (+.p16 (*.p16 (*.p16 x x) (+.p16 (*.p16 (*.p16 (real->posit16 0.0001789971) (*.p16 x x)) (*.p16 (*.p16 x x) (real->posit16 2))) (+.p16 (real->posit16 0.0140005442) (*.p16 (*.p16 x x) (real->posit16 0.0008327945))))) (real->posit16 0.0694555761)) (*.p16 x x)) (real->posit16 0.2909738639)))) (*.p16 x x)) (real->posit16 1))))> 27.424 * * * * [progress]: [ 9 / 12 ] simplifiying candidate #posit16 1) (*.p16 (*.p16 x x) (+.p16 (*.p16 (*.p16 x x) (+.p16 (*.p16 (*.p16 x x) (+.p16 (*.p16 (+.p16 (real->posit16 0.0005064034) (*.p16 (*.p16 (real->posit16 0.0001789971) x) x)) (*.p16 x x)) (real->posit16 0.0072644182))) (real->posit16 0.0424060604))) (real->posit16 0.1049934947))))) (+.p16 (*.p16 (+.p16 (real->posit16 0.7715471019) (*.p16 (*.p16 x x) (+.p16 (*.p16 (+.p16 (*.p16 (*.p16 x x) (+.p16 (*.p16 (*.p16 (*.p16 x x) (real->posit16 2)) (*.p16 (real->posit16 0.0001789971) (*.p16 x x))) (+.p16 (real->posit16 0.0140005442) (*.p16 (*.p16 x x) (real->posit16 0.0008327945))))) (real->posit16 0.0694555761)) (*.p16 x x)) (real->posit16 0.2909738639)))) (*.p16 x x)) (real->posit16 1))))> 27.424 * * * * [progress]: [ 10 / 12 ] simplifiying candidate #posit16 1) (*.p16 (*.p16 x x) (+.p16 (*.p16 (*.p16 x x) (+.p16 (*.p16 (*.p16 x x) (+.p16 (*.p16 (+.p16 (real->posit16 0.0005064034) (*.p16 (*.p16 (real->posit16 0.0001789971) x) x)) (*.p16 x x)) (real->posit16 0.0072644182))) (real->posit16 0.0424060604))) (real->posit16 0.1049934947))))) (+.p16 (*.p16 (+.p16 (real->posit16 0.7715471019) (*.p16 (*.p16 x x) (+.p16 (*.p16 (+.p16 (*.p16 (*.p16 x x) (+.p16 (*.p16 (*.p16 (*.p16 x x) (real->posit16 2)) (*.p16 (real->posit16 0.0001789971) (*.p16 x x))) (+.p16 (real->posit16 0.0140005442) (*.p16 (*.p16 x x) (real->posit16 0.0008327945))))) (real->posit16 0.0694555761)) (*.p16 x x)) (real->posit16 0.2909738639)))) (*.p16 x x)) (real->posit16 1))))> 27.424 * * * * [progress]: [ 11 / 12 ] simplifiying candidate #posit16 1) (*.p16 (*.p16 x x) (+.p16 (*.p16 (*.p16 x x) (+.p16 (*.p16 (*.p16 x x) (+.p16 (*.p16 (+.p16 (real->posit16 0.0005064034) (*.p16 (*.p16 (real->posit16 0.0001789971) x) x)) (*.p16 x x)) (real->posit16 0.0072644182))) (real->posit16 0.0424060604))) (real->posit16 0.1049934947))))) (+.p16 (*.p16 (+.p16 (real->posit16 0.7715471019) (*.p16 (*.p16 x x) (+.p16 (*.p16 (+.p16 (*.p16 (*.p16 x x) (+.p16 (*.p16 (*.p16 (*.p16 x x) (real->posit16 2)) (*.p16 (real->posit16 0.0001789971) (*.p16 x x))) (+.p16 (real->posit16 0.0140005442) (*.p16 (*.p16 x x) (real->posit16 0.0008327945))))) (real->posit16 0.0694555761)) (*.p16 x x)) (real->posit16 0.2909738639)))) (*.p16 x x)) (real->posit16 1))))> 27.424 * * * * [progress]: [ 12 / 12 ] simplifiying candidate #posit16 1) (*.p16 (*.p16 x x) (+.p16 (*.p16 (*.p16 x x) (+.p16 (*.p16 (*.p16 x x) (+.p16 (*.p16 (+.p16 (real->posit16 0.0005064034) (*.p16 (*.p16 (real->posit16 0.0001789971) x) x)) (*.p16 x x)) (real->posit16 0.0072644182))) (real->posit16 0.0424060604))) (real->posit16 0.1049934947))))) (+.p16 (*.p16 (+.p16 (real->posit16 0.7715471019) (*.p16 (*.p16 x x) (+.p16 (*.p16 (+.p16 (*.p16 (*.p16 x x) (+.p16 (*.p16 (*.p16 (*.p16 x x) (real->posit16 2)) (*.p16 (real->posit16 0.0001789971) (*.p16 x x))) (+.p16 (real->posit16 0.0140005442) (*.p16 (*.p16 x x) (real->posit16 0.0008327945))))) (real->posit16 0.0694555761)) (*.p16 x x)) (real->posit16 0.2909738639)))) (*.p16 x x)) (real->posit16 1))))> 27.424 * [simplify]: Simplifying: (/.p16 (+.p16 (*.p16 (+.p16 (real->posit16 0.7715471019) (*.p16 (*.p16 x x) (+.p16 (*.p16 (+.p16 (*.p16 (*.p16 x x) (+.p16 (*.p16 (*.p16 (*.p16 x x) (real->posit16 2)) (*.p16 (real->posit16 0.0001789971) (*.p16 x x))) (+.p16 (real->posit16 0.0140005442) (*.p16 (*.p16 x x) (real->posit16 0.0008327945))))) (real->posit16 0.0694555761)) (*.p16 x x)) (real->posit16 0.2909738639)))) (*.p16 x x)) (real->posit16 1)) (+.p16 (real->posit16 1) (*.p16 (*.p16 x x) (+.p16 (*.p16 (*.p16 x x) (+.p16 (*.p16 (*.p16 x x) (+.p16 (*.p16 (+.p16 (real->posit16 0.0005064034) (*.p16 (*.p16 (real->posit16 0.0001789971) x) x)) (*.p16 x x)) (real->posit16 0.0072644182))) (real->posit16 0.0424060604))) (real->posit16 0.1049934947))))) (*.p16 x (real->posit16 0.0008327945)) (*.p16 (real->posit16 0.0001789971) x) (*.p16 (*.p16 (*.p16 x x) (real->posit16 2)) (real->posit16 0.0001789971)) (*.p16 (real->posit16 2) (*.p16 (real->posit16 0.0001789971) (*.p16 x x))) (*.p16 (real->posit16 0.0001789971) x) (*.p16 (real->posit16 0.0001789971) x) (*.p16 (real->posit16 0.0001789971) x) (*.p16 (real->posit16 0.0001789971) x) 27.424 * * [simplify]: iteration 1: (55 enodes) 27.447 * * [simplify]: iteration 2: (155 enodes) 27.499 * * [simplify]: iteration 3: (428 enodes) 27.685 * * [simplify]: iteration 4: (1265 enodes) 28.654 * * [simplify]: Extracting #0: cost 4 inf + 0 28.654 * * [simplify]: Extracting #1: cost 16 inf + 0 28.654 * * [simplify]: Extracting #2: cost 57 inf + 322 28.655 * * [simplify]: Extracting #3: cost 196 inf + 2256 28.657 * * [simplify]: Extracting #4: cost 500 inf + 8032 28.674 * * [simplify]: Extracting #5: cost 565 inf + 72941 28.701 * * [simplify]: Extracting #6: cost 435 inf + 271861 28.770 * * [simplify]: Extracting #7: cost 197 inf + 670982 28.899 * * [simplify]: Extracting #8: cost 23 inf + 1016049 29.038 * * [simplify]: Extracting #9: cost 0 inf + 1059123 29.180 * * [simplify]: Extracting #10: cost 0 inf + 1057843 29.323 * [simplify]: Simplified to: (/.p16 (+.p16 (+.p16 (*.p16 (real->posit16 0.7715471019) (*.p16 x x)) (real->posit16 1)) (*.p16 (*.p16 (*.p16 x x) (*.p16 x x)) (+.p16 (real->posit16 0.2909738639) (*.p16 (*.p16 x x) (+.p16 (real->posit16 0.0694555761) (*.p16 (+.p16 (*.p16 (*.p16 (real->posit16 2) (real->posit16 0.0001789971)) (*.p16 (*.p16 x x) (*.p16 x x))) (+.p16 (real->posit16 0.0140005442) (*.p16 (*.p16 x x) (real->posit16 0.0008327945)))) (*.p16 x x))))))) (+.p16 (real->posit16 1) (*.p16 (+.p16 (*.p16 (+.p16 (*.p16 (+.p16 (*.p16 (+.p16 (real->posit16 0.0005064034) (*.p16 (real->posit16 0.0001789971) (*.p16 x x))) (*.p16 x x)) (real->posit16 0.0072644182)) (*.p16 x x)) (real->posit16 0.0424060604)) (*.p16 x x)) (real->posit16 0.1049934947)) (*.p16 x x)))) (*.p16 x (real->posit16 0.0008327945)) (*.p16 x (real->posit16 0.0001789971)) (*.p16 (*.p16 x (real->posit16 0.0001789971)) (*.p16 x (real->posit16 2))) (*.p16 (*.p16 x (real->posit16 0.0001789971)) (*.p16 x (real->posit16 2))) (*.p16 x (real->posit16 0.0001789971)) (*.p16 x (real->posit16 0.0001789971)) (*.p16 x (real->posit16 0.0001789971)) (*.p16 x (real->posit16 0.0001789971)) 29.328 * * * [progress]: adding candidates to table 30.967 * [progress]: [Phase 3 of 3] Extracting. 30.967 * * [regime]: Finding splitpoints for: (#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))))) x))> #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))) x) (+.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))))))> #posit16 1) (*.p16 (real->posit16 0.1049934947) (*.p16 x x))) (*.p16 (real->posit16 0.0424060604) (*.p16 (*.p16 x x) (*.p16 x x)))) (*.p16 (real->posit16 0.0072644182) (*.p16 (*.p16 (*.p16 x x) (*.p16 x x)) (*.p16 x x)))) (*.p16 (real->posit16 0.0005064034) (*.p16 (*.p16 (*.p16 (*.p16 x x) (*.p16 x x)) (*.p16 x x)) (*.p16 x x)))) (*.p16 (real->posit16 0.0001789971) (*.p16 (*.p16 (*.p16 (*.p16 (*.p16 x x) (*.p16 x x)) (*.p16 x x)) (*.p16 x x)) (*.p16 x x)))) (+.p16 (+.p16 (+.p16 (+.p16 (+.p16 (+.p16 (real->posit16 1) (*.p16 (real->posit16 0.7715471019) (*.p16 x x))) (*.p16 (real->posit16 0.2909738639) (*.p16 (*.p16 x x) (*.p16 x x)))) (*.p16 (real->posit16 0.0694555761) (*.p16 (*.p16 (*.p16 x x) (*.p16 x x)) (*.p16 x x)))) (*.p16 (real->posit16 0.0140005442) (*.p16 (*.p16 (*.p16 (*.p16 x x) (*.p16 x x)) (*.p16 x x)) (*.p16 x x)))) (*.p16 (real->posit16 0.0008327945) (*.p16 (*.p16 (*.p16 (*.p16 (*.p16 x x) (*.p16 x x)) (*.p16 x x)) (*.p16 x x)) (*.p16 x x)))) (*.p16 (*.p16 (real->posit16 2) (real->posit16 0.0001789971)) (*.p16 (*.p16 (*.p16 (*.p16 (*.p16 (*.p16 x x) (*.p16 x x)) (*.p16 x x)) (*.p16 x x)) (*.p16 x x)) (*.p16 x x))))) x))> #posit16 0.7715471019) (*.p16 (*.p16 x x) (+.p16 (*.p16 (+.p16 (*.p16 (*.p16 x x) (+.p16 (*.p16 (*.p16 (*.p16 x x) (real->posit16 2)) (*.p16 (real->posit16 0.0001789971) (*.p16 x x))) (+.p16 (real->posit16 0.0140005442) (*.p16 (*.p16 x x) (real->posit16 0.0008327945))))) (real->posit16 0.0694555761)) (*.p16 x x)) (real->posit16 0.2909738639)))) (*.p16 x x)) (real->posit16 1)) (+.p16 (real->posit16 1) (*.p16 (*.p16 x x) (+.p16 (*.p16 (*.p16 x x) (+.p16 (*.p16 (*.p16 x x) (+.p16 (*.p16 (+.p16 (real->posit16 0.0005064034) (*.p16 (real->posit16 0.0001789971) (*.p16 x x))) (*.p16 x x)) (real->posit16 0.0072644182))) (real->posit16 0.0424060604))) (real->posit16 0.1049934947)))))))> #posit16 1) (*.p16 (*.p16 x x) (+.p16 (*.p16 (*.p16 x x) (+.p16 (*.p16 (*.p16 x x) (+.p16 (*.p16 (+.p16 (real->posit16 0.0005064034) (*.p16 (*.p16 (real->posit16 0.0001789971) x) x)) (*.p16 x x)) (real->posit16 0.0072644182))) (real->posit16 0.0424060604))) (real->posit16 0.1049934947))))) (+.p16 (*.p16 (+.p16 (real->posit16 0.7715471019) (*.p16 (*.p16 x x) (+.p16 (*.p16 (+.p16 (*.p16 (*.p16 x x) (+.p16 (*.p16 (*.p16 (*.p16 x x) (real->posit16 2)) (*.p16 (real->posit16 0.0001789971) (*.p16 x x))) (+.p16 (real->posit16 0.0140005442) (*.p16 (*.p16 x x) (real->posit16 0.0008327945))))) (real->posit16 0.0694555761)) (*.p16 x x)) (real->posit16 0.2909738639)))) (*.p16 x x)) (real->posit16 1))))> #posit16 0.7715471019)) (real->posit16 1)) (*.p16 (*.p16 (*.p16 x x) (*.p16 x x)) (+.p16 (+.p16 (*.p16 (*.p16 x x) (real->posit16 0.0694555761)) (real->posit16 0.2909738639)) (*.p16 (+.p16 (*.p16 (*.p16 x x) (+.p16 (real->posit16 0.0008327945) (*.p16 (*.p16 x x) (*.p16 (real->posit16 0.0001789971) (real->posit16 2))))) (real->posit16 0.0140005442)) (*.p16 (*.p16 x x) (*.p16 x x))))))) (+.p16 (*.p16 (*.p16 x x) (+.p16 (*.p16 (+.p16 (*.p16 (*.p16 x x) (+.p16 (+.p16 (*.p16 (real->posit16 0.0005064034) (*.p16 x x)) (*.p16 (*.p16 x x) (*.p16 (*.p16 x x) (real->posit16 0.0001789971)))) (real->posit16 0.0072644182))) (real->posit16 0.0424060604)) (*.p16 x x)) (real->posit16 0.1049934947))) (real->posit16 1))))> #posit16 0.7715471019)) (real->posit16 1)) (*.p16 (*.p16 (*.p16 x x) (*.p16 x x)) (+.p16 (+.p16 (*.p16 (*.p16 x x) (real->posit16 0.0694555761)) (real->posit16 0.2909738639)) (*.p16 (+.p16 (*.p16 (*.p16 x x) (+.p16 (real->posit16 0.0008327945) (*.p16 (*.p16 x x) (*.p16 (real->posit16 0.0001789971) (real->posit16 2))))) (real->posit16 0.0140005442)) (*.p16 (*.p16 x x) (*.p16 x x))))))) (*.p16 (*.p16 x x) (+.p16 (*.p16 (+.p16 (*.p16 (*.p16 x x) (+.p16 (+.p16 (*.p16 (real->posit16 0.0005064034) (*.p16 x x)) (*.p16 (*.p16 (*.p16 x x) (*.p16 x x)) (real->posit16 0.0001789971))) (real->posit16 0.0072644182))) (real->posit16 0.0424060604)) (*.p16 x x)) (real->posit16 0.1049934947)))) (*.p16 (/.p16 x (+.p16 (+.p16 (*.p16 (*.p16 x x) (real->posit16 0.7715471019)) (real->posit16 1)) (*.p16 (*.p16 (*.p16 x x) (*.p16 x x)) (+.p16 (+.p16 (*.p16 (*.p16 x x) (real->posit16 0.0694555761)) (real->posit16 0.2909738639)) (*.p16 (+.p16 (*.p16 (*.p16 x x) (+.p16 (real->posit16 0.0008327945) (*.p16 (*.p16 x x) (*.p16 (real->posit16 0.0001789971) (real->posit16 2))))) (real->posit16 0.0140005442)) (*.p16 (*.p16 x x) (*.p16 x x))))))) (real->posit16 1))))>) 30.984 * * * [regime-changes]: Trying 1 branch expressions: (x) 30.984 * * * * [regimes]: Trying to branch on x from (#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))))) x))> #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))) x) (+.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))))))> #posit16 1) (*.p16 (real->posit16 0.1049934947) (*.p16 x x))) (*.p16 (real->posit16 0.0424060604) (*.p16 (*.p16 x x) (*.p16 x x)))) (*.p16 (real->posit16 0.0072644182) (*.p16 (*.p16 (*.p16 x x) (*.p16 x x)) (*.p16 x x)))) (*.p16 (real->posit16 0.0005064034) (*.p16 (*.p16 (*.p16 (*.p16 x x) (*.p16 x x)) (*.p16 x x)) (*.p16 x x)))) (*.p16 (real->posit16 0.0001789971) (*.p16 (*.p16 (*.p16 (*.p16 (*.p16 x x) (*.p16 x x)) (*.p16 x x)) (*.p16 x x)) (*.p16 x x)))) (+.p16 (+.p16 (+.p16 (+.p16 (+.p16 (+.p16 (real->posit16 1) (*.p16 (real->posit16 0.7715471019) (*.p16 x x))) (*.p16 (real->posit16 0.2909738639) (*.p16 (*.p16 x x) (*.p16 x x)))) (*.p16 (real->posit16 0.0694555761) (*.p16 (*.p16 (*.p16 x x) (*.p16 x x)) (*.p16 x x)))) (*.p16 (real->posit16 0.0140005442) (*.p16 (*.p16 (*.p16 (*.p16 x x) (*.p16 x x)) (*.p16 x x)) (*.p16 x x)))) (*.p16 (real->posit16 0.0008327945) (*.p16 (*.p16 (*.p16 (*.p16 (*.p16 x x) (*.p16 x x)) (*.p16 x x)) (*.p16 x x)) (*.p16 x x)))) (*.p16 (*.p16 (real->posit16 2) (real->posit16 0.0001789971)) (*.p16 (*.p16 (*.p16 (*.p16 (*.p16 (*.p16 x x) (*.p16 x x)) (*.p16 x x)) (*.p16 x x)) (*.p16 x x)) (*.p16 x x))))) x))> #posit16 0.7715471019) (*.p16 (*.p16 x x) (+.p16 (*.p16 (+.p16 (*.p16 (*.p16 x x) (+.p16 (*.p16 (*.p16 (*.p16 x x) (real->posit16 2)) (*.p16 (real->posit16 0.0001789971) (*.p16 x x))) (+.p16 (real->posit16 0.0140005442) (*.p16 (*.p16 x x) (real->posit16 0.0008327945))))) (real->posit16 0.0694555761)) (*.p16 x x)) (real->posit16 0.2909738639)))) (*.p16 x x)) (real->posit16 1)) (+.p16 (real->posit16 1) (*.p16 (*.p16 x x) (+.p16 (*.p16 (*.p16 x x) (+.p16 (*.p16 (*.p16 x x) (+.p16 (*.p16 (+.p16 (real->posit16 0.0005064034) (*.p16 (real->posit16 0.0001789971) (*.p16 x x))) (*.p16 x x)) (real->posit16 0.0072644182))) (real->posit16 0.0424060604))) (real->posit16 0.1049934947)))))))> #posit16 1) (*.p16 (*.p16 x x) (+.p16 (*.p16 (*.p16 x x) (+.p16 (*.p16 (*.p16 x x) (+.p16 (*.p16 (+.p16 (real->posit16 0.0005064034) (*.p16 (*.p16 (real->posit16 0.0001789971) x) x)) (*.p16 x x)) (real->posit16 0.0072644182))) (real->posit16 0.0424060604))) (real->posit16 0.1049934947))))) (+.p16 (*.p16 (+.p16 (real->posit16 0.7715471019) (*.p16 (*.p16 x x) (+.p16 (*.p16 (+.p16 (*.p16 (*.p16 x x) (+.p16 (*.p16 (*.p16 (*.p16 x x) (real->posit16 2)) (*.p16 (real->posit16 0.0001789971) (*.p16 x x))) (+.p16 (real->posit16 0.0140005442) (*.p16 (*.p16 x x) (real->posit16 0.0008327945))))) (real->posit16 0.0694555761)) (*.p16 x x)) (real->posit16 0.2909738639)))) (*.p16 x x)) (real->posit16 1))))> #posit16 0.7715471019)) (real->posit16 1)) (*.p16 (*.p16 (*.p16 x x) (*.p16 x x)) (+.p16 (+.p16 (*.p16 (*.p16 x x) (real->posit16 0.0694555761)) (real->posit16 0.2909738639)) (*.p16 (+.p16 (*.p16 (*.p16 x x) (+.p16 (real->posit16 0.0008327945) (*.p16 (*.p16 x x) (*.p16 (real->posit16 0.0001789971) (real->posit16 2))))) (real->posit16 0.0140005442)) (*.p16 (*.p16 x x) (*.p16 x x))))))) (+.p16 (*.p16 (*.p16 x x) (+.p16 (*.p16 (+.p16 (*.p16 (*.p16 x x) (+.p16 (+.p16 (*.p16 (real->posit16 0.0005064034) (*.p16 x x)) (*.p16 (*.p16 x x) (*.p16 (*.p16 x x) (real->posit16 0.0001789971)))) (real->posit16 0.0072644182))) (real->posit16 0.0424060604)) (*.p16 x x)) (real->posit16 0.1049934947))) (real->posit16 1))))> #posit16 0.7715471019)) (real->posit16 1)) (*.p16 (*.p16 (*.p16 x x) (*.p16 x x)) (+.p16 (+.p16 (*.p16 (*.p16 x x) (real->posit16 0.0694555761)) (real->posit16 0.2909738639)) (*.p16 (+.p16 (*.p16 (*.p16 x x) (+.p16 (real->posit16 0.0008327945) (*.p16 (*.p16 x x) (*.p16 (real->posit16 0.0001789971) (real->posit16 2))))) (real->posit16 0.0140005442)) (*.p16 (*.p16 x x) (*.p16 x x))))))) (*.p16 (*.p16 x x) (+.p16 (*.p16 (+.p16 (*.p16 (*.p16 x x) (+.p16 (+.p16 (*.p16 (real->posit16 0.0005064034) (*.p16 x x)) (*.p16 (*.p16 (*.p16 x x) (*.p16 x x)) (real->posit16 0.0001789971))) (real->posit16 0.0072644182))) (real->posit16 0.0424060604)) (*.p16 x x)) (real->posit16 0.1049934947)))) (*.p16 (/.p16 x (+.p16 (+.p16 (*.p16 (*.p16 x x) (real->posit16 0.7715471019)) (real->posit16 1)) (*.p16 (*.p16 (*.p16 x x) (*.p16 x x)) (+.p16 (+.p16 (*.p16 (*.p16 x x) (real->posit16 0.0694555761)) (real->posit16 0.2909738639)) (*.p16 (+.p16 (*.p16 (*.p16 x x) (+.p16 (real->posit16 0.0008327945) (*.p16 (*.p16 x x) (*.p16 (real->posit16 0.0001789971) (real->posit16 2))))) (real->posit16 0.0140005442)) (*.p16 (*.p16 x x) (*.p16 x x))))))) (real->posit16 1))))>) 31.596 * * * [regime]: Found split indices: #