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.006 * * * * [points]: Setting MPFR precision to 64 0.007 * * * * [points]: Setting MPFR precision to 320 0.008 * * * * [points]: Computing exacts on every 8 of 256 points to ramp up precision 0.011 * * * * [points]: Setting MPFR precision to 64 0.012 * * * * [points]: Setting MPFR precision to 320 0.014 * * * * [points]: Computing exacts on every 4 of 256 points to ramp up precision 0.016 * * * * [points]: Setting MPFR precision to 64 0.019 * * * * [points]: Setting MPFR precision to 320 0.022 * * * * [points]: Computing exacts on every 2 of 256 points to ramp up precision 0.024 * * * * [points]: Setting MPFR precision to 64 0.029 * * * * [points]: Setting MPFR precision to 320 0.042 * * * * [points]: Computing exacts for 256 points 0.048 * * * * [points]: Setting MPFR precision to 64 0.073 * * * * [points]: Setting MPFR precision to 320 0.097 * * * * [points]: Filtering points with unrepresentable outputs 0.097 * * * * [points]: Sampled 256 points with exact outputs 0.098 * * * [progress]: [2/2] Setting up program. 0.122 * [progress]: [Phase 2 of 3] Improving. 0.122 * * * * [progress]: [ 1 / 1 ] simplifiying candidate #posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (real->posit16 2) x)) (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1)))))> 0.122 * [simplify]: Simplifying: (+.p16 (-.p16 (/.p16 (real->posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (real->posit16 2) x)) (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1)))) 0.122 * * [simplify]: iteration 1: (12 enodes) 0.127 * * [simplify]: iteration 2: (35 enodes) 0.134 * * [simplify]: iteration 3: (83 enodes) 0.156 * * [simplify]: iteration 4: (233 enodes) 0.261 * * [simplify]: iteration 5: (1047 enodes) 1.450 * * [simplify]: Extracting #0: cost 1 inf + 0 1.450 * * [simplify]: Extracting #1: cost 63 inf + 0 1.451 * * [simplify]: Extracting #2: cost 424 inf + 0 1.456 * * [simplify]: Extracting #3: cost 1384 inf + 1 1.482 * * [simplify]: Extracting #4: cost 2011 inf + 6310 1.517 * * [simplify]: Extracting #5: cost 1965 inf + 268223 1.668 * * [simplify]: Extracting #6: cost 1004 inf + 1944471 1.933 * * [simplify]: Extracting #7: cost 229 inf + 3572048 2.194 * * [simplify]: Extracting #8: cost 7 inf + 4121456 2.532 * * [simplify]: Extracting #9: cost 0 inf + 4134475 2.866 * [simplify]: Simplified to: (-.p16 (+.p16 (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1))) (/.p16 (real->posit16 1) (+.p16 (real->posit16 1) x))) (/.p16 (real->posit16 2) x)) 2.886 * * [progress]: iteration 1 / 4 2.886 * * * [progress]: picking best candidate 2.906 * * * * [pick]: Picked #posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (real->posit16 2) x)) (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1)))))> 2.906 * * * [progress]: localizing error 3.181 * * * [progress]: generating rewritten candidates 3.181 * * * * [progress]: [ 1 / 4 ] rewriting at (2) 3.201 * * * * [progress]: [ 2 / 4 ] rewriting at (2 1) 3.206 * * * * [progress]: [ 3 / 4 ] rewriting at (2 2) 3.209 * * * * [progress]: [ 4 / 4 ] rewriting at (2 1 1) 3.212 * * * [progress]: generating series expansions 3.213 * * * * [progress]: [ 1 / 4 ] generating series at (2) 3.213 * * * * [progress]: [ 2 / 4 ] generating series at (2 1) 3.213 * * * * [progress]: [ 3 / 4 ] generating series at (2 2) 3.213 * * * * [progress]: [ 4 / 4 ] generating series at (2 1 1) 3.213 * * * [progress]: simplifying candidates 3.213 * * * * [progress]: [ 1 / 10 ] simplifiying candidate #posit16 1) (+.p16 x (real->posit16 1))) (+.p16 (neg.p16 (/.p16 (real->posit16 2) x)) (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1))))))> 3.213 * * * * [progress]: [ 2 / 10 ] simplifiying candidate #posit16 1) (+.p16 x (real->posit16 1))) (-.p16 (/.p16 (real->posit16 2) x) (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1))))))> 3.213 * * * * [progress]: [ 3 / 10 ] simplifiying candidate #posit16 1) (-.p16 x (real->posit16 1))) (-.p16 (/.p16 (real->posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (real->posit16 2) x))))> 3.213 * * * * [progress]: [ 4 / 10 ] simplifiying candidate #posit16 1) (+.p16 x (real->posit16 1))) (neg.p16 (/.p16 (real->posit16 2) x))) (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1)))))> 3.213 * * * * [progress]: [ 5 / 10 ] simplifiying candidate #posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (real->posit16 1) (+.p16 x (real->posit16 1)))) (*.p16 (/.p16 (real->posit16 2) x) (/.p16 (real->posit16 2) x))) (+.p16 (/.p16 (real->posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (real->posit16 2) x))) (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1)))))> 3.213 * * * * [progress]: [ 6 / 10 ] simplifiying candidate #posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (real->posit16 2) x)) (*.p16 (/.p16 (real->posit16 1) (-.p16 (*.p16 x x) (*.p16 (real->posit16 1) (real->posit16 1)))) (+.p16 x (real->posit16 1)))))> 3.213 * * * * [progress]: [ 7 / 10 ] simplifiying candidate #posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (real->posit16 2) x)) (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1)))))> 3.213 * * * * [progress]: [ 8 / 10 ] simplifiying candidate #posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (real->posit16 2) x)) (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1)))))> 3.213 * * * * [progress]: [ 9 / 10 ] simplifiying candidate #posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (real->posit16 2) x)) (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1)))))> 3.213 * * * * [progress]: [ 10 / 10 ] simplifiying candidate #posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (real->posit16 2) x)) (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1)))))> 3.214 * [simplify]: Simplifying: (+.p16 (neg.p16 (/.p16 (real->posit16 2) x)) (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1)))) (-.p16 (/.p16 (real->posit16 2) x) (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1)))) (neg.p16 (/.p16 (real->posit16 2) x)) (-.p16 (*.p16 (/.p16 (real->posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (real->posit16 1) (+.p16 x (real->posit16 1)))) (*.p16 (/.p16 (real->posit16 2) x) (/.p16 (real->posit16 2) x))) (+.p16 (/.p16 (real->posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (real->posit16 2) x)) (/.p16 (real->posit16 1) (-.p16 (*.p16 x x) (*.p16 (real->posit16 1) (real->posit16 1)))) (+.p16 (-.p16 (/.p16 (real->posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (real->posit16 2) x)) (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1)))) (+.p16 (-.p16 (/.p16 (real->posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (real->posit16 2) x)) (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1)))) (+.p16 (-.p16 (/.p16 (real->posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (real->posit16 2) x)) (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1)))) (+.p16 (-.p16 (/.p16 (real->posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (real->posit16 2) x)) (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1)))) 3.214 * * [simplify]: iteration 1: (23 enodes) 3.222 * * [simplify]: iteration 2: (69 enodes) 3.235 * * [simplify]: iteration 3: (191 enodes) 3.288 * * [simplify]: iteration 4: (708 enodes) 3.771 * * [simplify]: Extracting #0: cost 7 inf + 0 3.771 * * [simplify]: Extracting #1: cost 159 inf + 0 3.773 * * [simplify]: Extracting #2: cost 719 inf + 0 3.779 * * [simplify]: Extracting #3: cost 1116 inf + 59063 3.804 * * [simplify]: Extracting #4: cost 977 inf + 589227 3.880 * * [simplify]: Extracting #5: cost 431 inf + 1552307 4.022 * * [simplify]: Extracting #6: cost 98 inf + 2274244 4.144 * * [simplify]: Extracting #7: cost 0 inf + 2521505 4.305 * * [simplify]: Extracting #8: cost 0 inf + 2496545 4.438 * [simplify]: Simplified to: (-.p16 (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1))) (/.p16 (real->posit16 2) x)) (-.p16 (/.p16 (real->posit16 2) x) (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1)))) (neg.p16 (/.p16 (real->posit16 2) x)) (*.p16 (-.p16 (/.p16 (real->posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (real->posit16 2) x)) (+.p16 (/.p16 (real->posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (real->posit16 2) x))) (+.p16 (/.p16 (real->posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (real->posit16 2) x)) (/.p16 (real->posit16 1) (*.p16 (+.p16 x (real->posit16 1)) (-.p16 x (real->posit16 1)))) (+.p16 (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1))) (-.p16 (/.p16 (real->posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (real->posit16 2) x))) (+.p16 (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1))) (-.p16 (/.p16 (real->posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (real->posit16 2) x))) (+.p16 (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1))) (-.p16 (/.p16 (real->posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (real->posit16 2) x))) (+.p16 (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1))) (-.p16 (/.p16 (real->posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (real->posit16 2) x))) 4.438 * * * [progress]: adding candidates to table 4.703 * * [progress]: iteration 2 / 4 4.703 * * * [progress]: picking best candidate 4.751 * * * * [pick]: Picked #posit16 1) (+.p16 x (real->posit16 1))) (-.p16 (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1))) (/.p16 (real->posit16 2) x))))> 4.751 * * * [progress]: localizing error 4.940 * * * [progress]: generating rewritten candidates 4.940 * * * * [progress]: [ 1 / 4 ] rewriting at (2) 4.947 * * * * [progress]: [ 2 / 4 ] rewriting at (2 2) 4.950 * * * * [progress]: [ 3 / 4 ] rewriting at (2 2 1) 4.952 * * * * [progress]: [ 4 / 4 ] rewriting at (2 1) 4.954 * * * [progress]: generating series expansions 4.954 * * * * [progress]: [ 1 / 4 ] generating series at (2) 4.954 * * * * [progress]: [ 2 / 4 ] generating series at (2 2) 4.954 * * * * [progress]: [ 3 / 4 ] generating series at (2 2 1) 4.954 * * * * [progress]: [ 4 / 4 ] generating series at (2 1) 4.954 * * * [progress]: simplifying candidates 4.954 * * * * [progress]: [ 1 / 10 ] simplifiying candidate #posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1)))) (neg.p16 (/.p16 (real->posit16 2) x))))> 4.954 * * * * [progress]: [ 2 / 10 ] simplifiying candidate #posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1)))) (/.p16 (real->posit16 2) x)))> 4.954 * * * * [progress]: [ 3 / 10 ] simplifiying candidate #posit16 1) (-.p16 x (real->posit16 1))) (/.p16 (real->posit16 2) x)) (/.p16 (real->posit16 1) (+.p16 x (real->posit16 1)))))> 4.954 * * * * [progress]: [ 4 / 10 ] simplifiying candidate #posit16 1) (+.p16 x (real->posit16 1))) (+.p16 (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1))) (neg.p16 (/.p16 (real->posit16 2) x)))))> 4.954 * * * * [progress]: [ 5 / 10 ] simplifiying candidate #posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (-.p16 (*.p16 (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1))) (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1)))) (*.p16 (/.p16 (real->posit16 2) x) (/.p16 (real->posit16 2) x))) (+.p16 (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1))) (/.p16 (real->posit16 2) x)))))> 4.954 * * * * [progress]: [ 6 / 10 ] simplifiying candidate #posit16 1) (+.p16 x (real->posit16 1))) (-.p16 (*.p16 (/.p16 (real->posit16 1) (-.p16 (*.p16 x x) (*.p16 (real->posit16 1) (real->posit16 1)))) (+.p16 x (real->posit16 1))) (/.p16 (real->posit16 2) x))))> 4.954 * * * * [progress]: [ 7 / 10 ] simplifiying candidate #posit16 1) (+.p16 x (real->posit16 1))) (-.p16 (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1))) (/.p16 (real->posit16 2) x))))> 4.954 * * * * [progress]: [ 8 / 10 ] simplifiying candidate #posit16 1) (+.p16 x (real->posit16 1))) (-.p16 (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1))) (/.p16 (real->posit16 2) x))))> 4.954 * * * * [progress]: [ 9 / 10 ] simplifiying candidate #posit16 1) (+.p16 x (real->posit16 1))) (-.p16 (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1))) (/.p16 (real->posit16 2) x))))> 4.954 * * * * [progress]: [ 10 / 10 ] simplifiying candidate #posit16 1) (+.p16 x (real->posit16 1))) (-.p16 (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1))) (/.p16 (real->posit16 2) x))))> 4.955 * [simplify]: Simplifying: (+.p16 (/.p16 (real->posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1)))) (+.p16 (/.p16 (real->posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1)))) (neg.p16 (/.p16 (real->posit16 2) x)) (-.p16 (*.p16 (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1))) (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1)))) (*.p16 (/.p16 (real->posit16 2) x) (/.p16 (real->posit16 2) x))) (+.p16 (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1))) (/.p16 (real->posit16 2) x)) (/.p16 (real->posit16 1) (-.p16 (*.p16 x x) (*.p16 (real->posit16 1) (real->posit16 1)))) (+.p16 (/.p16 (real->posit16 1) (+.p16 x (real->posit16 1))) (-.p16 (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1))) (/.p16 (real->posit16 2) x))) (+.p16 (/.p16 (real->posit16 1) (+.p16 x (real->posit16 1))) (-.p16 (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1))) (/.p16 (real->posit16 2) x))) (+.p16 (/.p16 (real->posit16 1) (+.p16 x (real->posit16 1))) (-.p16 (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1))) (/.p16 (real->posit16 2) x))) (+.p16 (/.p16 (real->posit16 1) (+.p16 x (real->posit16 1))) (-.p16 (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1))) (/.p16 (real->posit16 2) x))) 4.955 * * [simplify]: iteration 1: (22 enodes) 4.960 * * [simplify]: iteration 2: (62 enodes) 4.971 * * [simplify]: iteration 3: (168 enodes) 5.017 * * [simplify]: iteration 4: (708 enodes) 5.836 * * [simplify]: Extracting #0: cost 6 inf + 0 5.844 * * [simplify]: Extracting #1: cost 154 inf + 0 5.846 * * [simplify]: Extracting #2: cost 815 inf + 0 5.852 * * [simplify]: Extracting #3: cost 1510 inf + 7988 5.874 * * [simplify]: Extracting #4: cost 1564 inf + 391339 6.029 * * [simplify]: Extracting #5: cost 389 inf + 2721949 6.303 * * [simplify]: Extracting #6: cost 44 inf + 3392628 6.474 * * [simplify]: Extracting #7: cost 1 inf + 3495039 6.666 * * [simplify]: Extracting #8: cost 0 inf + 3496722 6.933 * [simplify]: Simplified to: (+.p16 (/.p16 (real->posit16 1) (+.p16 (real->posit16 1) x)) (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1)))) (+.p16 (/.p16 (real->posit16 1) (+.p16 (real->posit16 1) x)) (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1)))) (neg.p16 (/.p16 (real->posit16 2) x)) (*.p16 (+.p16 (/.p16 (real->posit16 2) x) (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1)))) (-.p16 (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1))) (/.p16 (real->posit16 2) x))) (+.p16 (/.p16 (real->posit16 2) x) (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1)))) (/.p16 (real->posit16 1) (*.p16 (-.p16 x (real->posit16 1)) (+.p16 (real->posit16 1) x))) (+.p16 (-.p16 (/.p16 (real->posit16 1) (+.p16 (real->posit16 1) x)) (/.p16 (real->posit16 2) x)) (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1)))) (+.p16 (-.p16 (/.p16 (real->posit16 1) (+.p16 (real->posit16 1) x)) (/.p16 (real->posit16 2) x)) (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1)))) (+.p16 (-.p16 (/.p16 (real->posit16 1) (+.p16 (real->posit16 1) x)) (/.p16 (real->posit16 2) x)) (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1)))) (+.p16 (-.p16 (/.p16 (real->posit16 1) (+.p16 (real->posit16 1) x)) (/.p16 (real->posit16 2) x)) (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1)))) 6.933 * * * [progress]: adding candidates to table 7.298 * * [progress]: iteration 3 / 4 7.298 * * * [progress]: picking best candidate 7.371 * * * * [pick]: Picked #posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1)))) (/.p16 (real->posit16 2) x)))> 7.371 * * * [progress]: localizing error 7.549 * * * [progress]: generating rewritten candidates 7.549 * * * * [progress]: [ 1 / 4 ] rewriting at (2) 7.567 * * * * [progress]: [ 2 / 4 ] rewriting at (2 1) 7.572 * * * * [progress]: [ 3 / 4 ] rewriting at (2 1 2) 7.573 * * * * [progress]: [ 4 / 4 ] rewriting at (2 1 1) 7.575 * * * [progress]: generating series expansions 7.575 * * * * [progress]: [ 1 / 4 ] generating series at (2) 7.575 * * * * [progress]: [ 2 / 4 ] generating series at (2 1) 7.575 * * * * [progress]: [ 3 / 4 ] generating series at (2 1 2) 7.575 * * * * [progress]: [ 4 / 4 ] generating series at (2 1 1) 7.575 * * * [progress]: simplifying candidates 7.575 * * * * [progress]: [ 1 / 9 ] simplifiying candidate #posit16 1) (+.p16 x (real->posit16 1))) (-.p16 (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1))) (/.p16 (real->posit16 2) x))))> 7.576 * * * * [progress]: [ 2 / 9 ] simplifiying candidate #posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1)))) (neg.p16 (/.p16 (real->posit16 2) x))))> 7.576 * * * * [progress]: [ 3 / 9 ] simplifiying candidate #posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1)))) (+.p16 (/.p16 (real->posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1))))) (*.p16 (/.p16 (real->posit16 2) x) (/.p16 (real->posit16 2) x))) (+.p16 (+.p16 (/.p16 (real->posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1)))) (/.p16 (real->posit16 2) x))))> 7.576 * * * * [progress]: [ 4 / 9 ] simplifiying candidate #posit16 1) (-.p16 x (real->posit16 1))) (/.p16 (real->posit16 1) (+.p16 x (real->posit16 1)))) (/.p16 (real->posit16 2) x)))> 7.576 * * * * [progress]: [ 5 / 9 ] simplifiying candidate #posit16 1) (+.p16 x (real->posit16 1))) (*.p16 (/.p16 (real->posit16 1) (-.p16 (*.p16 x x) (*.p16 (real->posit16 1) (real->posit16 1)))) (+.p16 x (real->posit16 1)))) (/.p16 (real->posit16 2) x)))> 7.576 * * * * [progress]: [ 6 / 9 ] simplifiying candidate #posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1)))) (/.p16 (real->posit16 2) x)))> 7.576 * * * * [progress]: [ 7 / 9 ] simplifiying candidate #posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1)))) (/.p16 (real->posit16 2) x)))> 7.576 * * * * [progress]: [ 8 / 9 ] simplifiying candidate #posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1)))) (/.p16 (real->posit16 2) x)))> 7.576 * * * * [progress]: [ 9 / 9 ] simplifiying candidate #posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1)))) (/.p16 (real->posit16 2) x)))> 7.576 * [simplify]: Simplifying: (-.p16 (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1))) (/.p16 (real->posit16 2) x)) (neg.p16 (/.p16 (real->posit16 2) x)) (-.p16 (*.p16 (+.p16 (/.p16 (real->posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1)))) (+.p16 (/.p16 (real->posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1))))) (*.p16 (/.p16 (real->posit16 2) x) (/.p16 (real->posit16 2) x))) (+.p16 (+.p16 (/.p16 (real->posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1)))) (/.p16 (real->posit16 2) x)) (/.p16 (real->posit16 1) (-.p16 (*.p16 x x) (*.p16 (real->posit16 1) (real->posit16 1)))) (+.p16 (/.p16 (real->posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1)))) (+.p16 (/.p16 (real->posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1)))) (+.p16 (/.p16 (real->posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1)))) (+.p16 (/.p16 (real->posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1)))) 7.576 * * [simplify]: iteration 1: (21 enodes) 7.582 * * [simplify]: iteration 2: (66 enodes) 7.595 * * [simplify]: iteration 3: (202 enodes) 7.663 * * [simplify]: iteration 4: (864 enodes) 9.057 * * [simplify]: Extracting #0: cost 6 inf + 0 9.058 * * [simplify]: Extracting #1: cost 150 inf + 0 9.063 * * [simplify]: Extracting #2: cost 959 inf + 0 9.074 * * [simplify]: Extracting #3: cost 1589 inf + 3015 9.105 * * [simplify]: Extracting #4: cost 1751 inf + 65385 9.204 * * [simplify]: Extracting #5: cost 1025 inf + 1314833 9.492 * * [simplify]: Extracting #6: cost 146 inf + 3380005 9.831 * * [simplify]: Extracting #7: cost 0 inf + 3799193 10.175 * * [simplify]: Extracting #8: cost 0 inf + 3789873 10.540 * [simplify]: Simplified to: (-.p16 (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1))) (/.p16 (real->posit16 2) x)) (neg.p16 (/.p16 (real->posit16 2) x)) (*.p16 (+.p16 (/.p16 (real->posit16 2) x) (+.p16 (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1))) (/.p16 (real->posit16 1) (+.p16 (real->posit16 1) x)))) (-.p16 (+.p16 (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1))) (/.p16 (real->posit16 1) (+.p16 (real->posit16 1) x))) (/.p16 (real->posit16 2) x))) (+.p16 (/.p16 (real->posit16 2) x) (+.p16 (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1))) (/.p16 (real->posit16 1) (+.p16 (real->posit16 1) x)))) (/.p16 (real->posit16 1) (*.p16 (-.p16 x (real->posit16 1)) (+.p16 (real->posit16 1) x))) (+.p16 (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1))) (/.p16 (real->posit16 1) (+.p16 (real->posit16 1) x))) (+.p16 (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1))) (/.p16 (real->posit16 1) (+.p16 (real->posit16 1) x))) (+.p16 (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1))) (/.p16 (real->posit16 1) (+.p16 (real->posit16 1) x))) (+.p16 (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1))) (/.p16 (real->posit16 1) (+.p16 (real->posit16 1) x))) 10.541 * * * [progress]: adding candidates to table 10.843 * * [progress]: iteration 4 / 4 10.843 * * * [progress]: picking best candidate 10.926 * * * * [pick]: Picked #posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1)))) (+.p16 (/.p16 (real->posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1))))) (*.p16 (/.p16 (real->posit16 2) x) (/.p16 (real->posit16 2) x))) (+.p16 (+.p16 (/.p16 (real->posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1)))) (/.p16 (real->posit16 2) x))))> 10.926 * * * [progress]: localizing error 11.246 * * * [progress]: generating rewritten candidates 11.246 * * * * [progress]: [ 1 / 4 ] rewriting at (2) 11.314 * * * * [progress]: [ 2 / 4 ] rewriting at (2 1) 11.318 * * * * [progress]: [ 3 / 4 ] rewriting at (2 2 1) 11.322 * * * * [progress]: [ 4 / 4 ] rewriting at (2 1 1 2) 11.326 * * * [progress]: generating series expansions 11.326 * * * * [progress]: [ 1 / 4 ] generating series at (2) 11.326 * * * * [progress]: [ 2 / 4 ] generating series at (2 1) 11.326 * * * * [progress]: [ 3 / 4 ] generating series at (2 2 1) 11.326 * * * * [progress]: [ 4 / 4 ] generating series at (2 1 1 2) 11.326 * * * [progress]: simplifying candidates 11.326 * * * * [progress]: [ 1 / 13 ] simplifiying candidate #posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1)))) (/.p16 (real->posit16 2) x)) (/.p16 (+.p16 (+.p16 (/.p16 (real->posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1)))) (/.p16 (real->posit16 2) x)) (-.p16 (+.p16 (/.p16 (real->posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1)))) (/.p16 (real->posit16 2) x)))))> 11.326 * * * * [progress]: [ 2 / 13 ] simplifiying candidate #posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1)))) (+.p16 (/.p16 (real->posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1))))) (*.p16 (+.p16 (/.p16 (real->posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1)))) (+.p16 (/.p16 (real->posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1)))))) (*.p16 (*.p16 (/.p16 (real->posit16 2) x) (/.p16 (real->posit16 2) x)) (*.p16 (/.p16 (real->posit16 2) x) (/.p16 (real->posit16 2) x)))) (*.p16 (+.p16 (+.p16 (/.p16 (real->posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1)))) (/.p16 (real->posit16 2) x)) (+.p16 (*.p16 (+.p16 (/.p16 (real->posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1)))) (+.p16 (/.p16 (real->posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1))))) (*.p16 (/.p16 (real->posit16 2) x) (/.p16 (real->posit16 2) x))))))> 11.326 * * * * [progress]: [ 3 / 13 ] simplifiying candidate #posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1)))) (/.p16 (real->posit16 2) x)) (-.p16 (+.p16 (/.p16 (real->posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1)))) (/.p16 (real->posit16 2) x))) (+.p16 (+.p16 (/.p16 (real->posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1)))) (/.p16 (real->posit16 2) x))))> 11.326 * * * * [progress]: [ 4 / 13 ] simplifiying candidate #posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1)))) (/.p16 (real->posit16 1) (+.p16 x (real->posit16 1)))) (-.p16 (*.p16 (+.p16 (/.p16 (real->posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1)))) (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1)))) (*.p16 (/.p16 (real->posit16 2) x) (/.p16 (real->posit16 2) x)))) (+.p16 (+.p16 (/.p16 (real->posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1)))) (/.p16 (real->posit16 2) x))))> 11.326 * * * * [progress]: [ 5 / 13 ] simplifiying candidate #posit16 1) (+.p16 x (real->posit16 1))) (+.p16 (/.p16 (real->posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1))))) (-.p16 (*.p16 (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1))) (+.p16 (/.p16 (real->posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1))))) (*.p16 (/.p16 (real->posit16 2) x) (/.p16 (real->posit16 2) x)))) (+.p16 (+.p16 (/.p16 (real->posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1)))) (/.p16 (real->posit16 2) x))))> 11.326 * * * * [progress]: [ 6 / 13 ] simplifiying candidate #posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1)))) (+.p16 (/.p16 (real->posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1))))) (neg.p16 (*.p16 (/.p16 (real->posit16 2) x) (/.p16 (real->posit16 2) x)))) (+.p16 (+.p16 (/.p16 (real->posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1)))) (/.p16 (real->posit16 2) x))))> 11.327 * * * * [progress]: [ 7 / 13 ] simplifiying candidate #posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1)))) (+.p16 (/.p16 (real->posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1))))) (*.p16 (+.p16 (/.p16 (real->posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1)))) (+.p16 (/.p16 (real->posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1)))))) (*.p16 (*.p16 (/.p16 (real->posit16 2) x) (/.p16 (real->posit16 2) x)) (*.p16 (/.p16 (real->posit16 2) x) (/.p16 (real->posit16 2) x)))) (+.p16 (*.p16 (+.p16 (/.p16 (real->posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1)))) (+.p16 (/.p16 (real->posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1))))) (*.p16 (/.p16 (real->posit16 2) x) (/.p16 (real->posit16 2) x)))) (+.p16 (+.p16 (/.p16 (real->posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1)))) (/.p16 (real->posit16 2) x))))> 11.327 * * * * [progress]: [ 8 / 13 ] simplifiying candidate #posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1)))) (+.p16 (/.p16 (real->posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1))))) (*.p16 (/.p16 (real->posit16 2) x) (/.p16 (real->posit16 2) x))) (+.p16 (+.p16 (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1))) (/.p16 (real->posit16 1) (+.p16 x (real->posit16 1)))) (/.p16 (real->posit16 2) x))))> 11.327 * * * * [progress]: [ 9 / 13 ] simplifiying candidate #posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1)))) (+.p16 (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1))) (/.p16 (real->posit16 1) (+.p16 x (real->posit16 1))))) (*.p16 (/.p16 (real->posit16 2) x) (/.p16 (real->posit16 2) x))) (+.p16 (+.p16 (/.p16 (real->posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1)))) (/.p16 (real->posit16 2) x))))> 11.327 * * * * [progress]: [ 10 / 13 ] simplifiying candidate #posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1)))) (+.p16 (/.p16 (real->posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1))))) (*.p16 (/.p16 (real->posit16 2) x) (/.p16 (real->posit16 2) x))) (+.p16 (+.p16 (/.p16 (real->posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1)))) (/.p16 (real->posit16 2) x))))> 11.327 * * * * [progress]: [ 11 / 13 ] simplifiying candidate #posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1)))) (+.p16 (/.p16 (real->posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1))))) (*.p16 (/.p16 (real->posit16 2) x) (/.p16 (real->posit16 2) x))) (+.p16 (+.p16 (/.p16 (real->posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1)))) (/.p16 (real->posit16 2) x))))> 11.327 * * * * [progress]: [ 12 / 13 ] simplifiying candidate #posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1)))) (+.p16 (/.p16 (real->posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1))))) (*.p16 (/.p16 (real->posit16 2) x) (/.p16 (real->posit16 2) x))) (+.p16 (+.p16 (/.p16 (real->posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1)))) (/.p16 (real->posit16 2) x))))> 11.327 * * * * [progress]: [ 13 / 13 ] simplifiying candidate #posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1)))) (+.p16 (/.p16 (real->posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1))))) (*.p16 (/.p16 (real->posit16 2) x) (/.p16 (real->posit16 2) x))) (+.p16 (+.p16 (/.p16 (real->posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1)))) (/.p16 (real->posit16 2) x))))> 11.327 * [simplify]: Simplifying: (/.p16 (+.p16 (+.p16 (/.p16 (real->posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1)))) (/.p16 (real->posit16 2) x)) (-.p16 (+.p16 (/.p16 (real->posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1)))) (/.p16 (real->posit16 2) x))) (*.p16 (+.p16 (+.p16 (/.p16 (real->posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1)))) (/.p16 (real->posit16 2) x)) (+.p16 (*.p16 (+.p16 (/.p16 (real->posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1)))) (+.p16 (/.p16 (real->posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1))))) (*.p16 (/.p16 (real->posit16 2) x) (/.p16 (real->posit16 2) x)))) (+.p16 (+.p16 (/.p16 (real->posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1)))) (/.p16 (real->posit16 2) x)) (-.p16 (+.p16 (/.p16 (real->posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1)))) (/.p16 (real->posit16 2) x)) (-.p16 (*.p16 (+.p16 (/.p16 (real->posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1)))) (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1)))) (*.p16 (/.p16 (real->posit16 2) x) (/.p16 (real->posit16 2) x))) (-.p16 (*.p16 (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1))) (+.p16 (/.p16 (real->posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1))))) (*.p16 (/.p16 (real->posit16 2) x) (/.p16 (real->posit16 2) x))) (neg.p16 (*.p16 (/.p16 (real->posit16 2) x) (/.p16 (real->posit16 2) x))) (-.p16 (*.p16 (*.p16 (+.p16 (/.p16 (real->posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1)))) (+.p16 (/.p16 (real->posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1))))) (*.p16 (+.p16 (/.p16 (real->posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1)))) (+.p16 (/.p16 (real->posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1)))))) (*.p16 (*.p16 (/.p16 (real->posit16 2) x) (/.p16 (real->posit16 2) x)) (*.p16 (/.p16 (real->posit16 2) x) (/.p16 (real->posit16 2) x)))) (+.p16 (*.p16 (+.p16 (/.p16 (real->posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1)))) (+.p16 (/.p16 (real->posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1))))) (*.p16 (/.p16 (real->posit16 2) x) (/.p16 (real->posit16 2) x))) (-.p16 (*.p16 (+.p16 (/.p16 (real->posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1)))) (+.p16 (/.p16 (real->posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1))))) (*.p16 (/.p16 (real->posit16 2) x) (/.p16 (real->posit16 2) x))) (+.p16 (+.p16 (/.p16 (real->posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1)))) (/.p16 (real->posit16 2) x)) (-.p16 (*.p16 (+.p16 (/.p16 (real->posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1)))) (+.p16 (/.p16 (real->posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1))))) (*.p16 (/.p16 (real->posit16 2) x) (/.p16 (real->posit16 2) x))) (+.p16 (+.p16 (/.p16 (real->posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1)))) (/.p16 (real->posit16 2) x)) (-.p16 (*.p16 (+.p16 (/.p16 (real->posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1)))) (+.p16 (/.p16 (real->posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1))))) (*.p16 (/.p16 (real->posit16 2) x) (/.p16 (real->posit16 2) x))) (+.p16 (+.p16 (/.p16 (real->posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1)))) (/.p16 (real->posit16 2) x)) (-.p16 (*.p16 (+.p16 (/.p16 (real->posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1)))) (+.p16 (/.p16 (real->posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1))))) (*.p16 (/.p16 (real->posit16 2) x) (/.p16 (real->posit16 2) x))) (+.p16 (+.p16 (/.p16 (real->posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1)))) (/.p16 (real->posit16 2) x)) 11.328 * * [simplify]: iteration 1: (27 enodes) 11.334 * * [simplify]: iteration 2: (103 enodes) 11.368 * * [simplify]: iteration 3: (400 enodes) 11.647 * * [simplify]: Extracting #0: cost 9 inf + 0 11.648 * * [simplify]: Extracting #1: cost 214 inf + 0 11.651 * * [simplify]: Extracting #2: cost 551 inf + 0 11.657 * * [simplify]: Extracting #3: cost 703 inf + 322 11.692 * * [simplify]: Extracting #4: cost 541 inf + 362319 11.772 * * [simplify]: Extracting #5: cost 110 inf + 1333691 11.922 * * [simplify]: Extracting #6: cost 3 inf + 1586635 12.038 * * [simplify]: Extracting #7: cost 0 inf + 1594122 12.132 * [simplify]: Simplified to: (/.p16 (+.p16 (+.p16 (/.p16 (real->posit16 1) (+.p16 (real->posit16 1) x)) (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1)))) (/.p16 (real->posit16 2) x)) (-.p16 (+.p16 (/.p16 (real->posit16 1) (+.p16 (real->posit16 1) x)) (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1)))) (/.p16 (real->posit16 2) x))) (*.p16 (+.p16 (+.p16 (/.p16 (real->posit16 1) (+.p16 (real->posit16 1) x)) (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1)))) (/.p16 (real->posit16 2) x)) (+.p16 (*.p16 (+.p16 (/.p16 (real->posit16 1) (+.p16 (real->posit16 1) x)) (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1)))) (+.p16 (/.p16 (real->posit16 1) (+.p16 (real->posit16 1) x)) (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1))))) (*.p16 (/.p16 (real->posit16 2) x) (/.p16 (real->posit16 2) x)))) (+.p16 (+.p16 (/.p16 (real->posit16 1) (+.p16 (real->posit16 1) x)) (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1)))) (/.p16 (real->posit16 2) x)) (-.p16 (+.p16 (/.p16 (real->posit16 1) (+.p16 (real->posit16 1) x)) (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1)))) (/.p16 (real->posit16 2) x)) (-.p16 (*.p16 (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1))) (+.p16 (/.p16 (real->posit16 1) (+.p16 (real->posit16 1) x)) (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1))))) (*.p16 (/.p16 (real->posit16 2) x) (/.p16 (real->posit16 2) x))) (-.p16 (*.p16 (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1))) (+.p16 (/.p16 (real->posit16 1) (+.p16 (real->posit16 1) x)) (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1))))) (*.p16 (/.p16 (real->posit16 2) x) (/.p16 (real->posit16 2) x))) (neg.p16 (*.p16 (/.p16 (real->posit16 2) x) (/.p16 (real->posit16 2) x))) (-.p16 (*.p16 (*.p16 (+.p16 (/.p16 (real->posit16 1) (+.p16 (real->posit16 1) x)) (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1)))) (+.p16 (/.p16 (real->posit16 1) (+.p16 (real->posit16 1) x)) (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1))))) (*.p16 (+.p16 (/.p16 (real->posit16 1) (+.p16 (real->posit16 1) x)) (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1)))) (+.p16 (/.p16 (real->posit16 1) (+.p16 (real->posit16 1) x)) (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1)))))) (*.p16 (*.p16 (/.p16 (real->posit16 2) x) (/.p16 (real->posit16 2) x)) (*.p16 (/.p16 (real->posit16 2) x) (/.p16 (real->posit16 2) x)))) (+.p16 (*.p16 (+.p16 (/.p16 (real->posit16 1) (+.p16 (real->posit16 1) x)) (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1)))) (+.p16 (/.p16 (real->posit16 1) (+.p16 (real->posit16 1) x)) (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1))))) (*.p16 (/.p16 (real->posit16 2) x) (/.p16 (real->posit16 2) x))) (*.p16 (+.p16 (+.p16 (/.p16 (real->posit16 1) (+.p16 (real->posit16 1) x)) (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1)))) (/.p16 (real->posit16 2) x)) (-.p16 (+.p16 (/.p16 (real->posit16 1) (+.p16 (real->posit16 1) x)) (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1)))) (/.p16 (real->posit16 2) x))) (+.p16 (+.p16 (/.p16 (real->posit16 1) (+.p16 (real->posit16 1) x)) (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1)))) (/.p16 (real->posit16 2) x)) (*.p16 (+.p16 (+.p16 (/.p16 (real->posit16 1) (+.p16 (real->posit16 1) x)) (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1)))) (/.p16 (real->posit16 2) x)) (-.p16 (+.p16 (/.p16 (real->posit16 1) (+.p16 (real->posit16 1) x)) (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1)))) (/.p16 (real->posit16 2) x))) (+.p16 (+.p16 (/.p16 (real->posit16 1) (+.p16 (real->posit16 1) x)) (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1)))) (/.p16 (real->posit16 2) x)) (*.p16 (+.p16 (+.p16 (/.p16 (real->posit16 1) (+.p16 (real->posit16 1) x)) (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1)))) (/.p16 (real->posit16 2) x)) (-.p16 (+.p16 (/.p16 (real->posit16 1) (+.p16 (real->posit16 1) x)) (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1)))) (/.p16 (real->posit16 2) x))) (+.p16 (+.p16 (/.p16 (real->posit16 1) (+.p16 (real->posit16 1) x)) (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1)))) (/.p16 (real->posit16 2) x)) (*.p16 (+.p16 (+.p16 (/.p16 (real->posit16 1) (+.p16 (real->posit16 1) x)) (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1)))) (/.p16 (real->posit16 2) x)) (-.p16 (+.p16 (/.p16 (real->posit16 1) (+.p16 (real->posit16 1) x)) (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1)))) (/.p16 (real->posit16 2) x))) (+.p16 (+.p16 (/.p16 (real->posit16 1) (+.p16 (real->posit16 1) x)) (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1)))) (/.p16 (real->posit16 2) x)) 12.134 * * * [progress]: adding candidates to table 12.730 * [progress]: [Phase 3 of 3] Extracting. 12.730 * * [regime]: Finding splitpoints for: (#posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (*.p16 (+.p16 (/.p16 (real->posit16 2) x) (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1)))) (-.p16 (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1))) (/.p16 (real->posit16 2) x))) (+.p16 (/.p16 (real->posit16 2) x) (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1)))))))> #posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1)))) (/.p16 (real->posit16 2) x)) (/.p16 (+.p16 (+.p16 (/.p16 (real->posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1)))) (/.p16 (real->posit16 2) x)) (-.p16 (+.p16 (/.p16 (real->posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1)))) (/.p16 (real->posit16 2) x)))))> #posit16 1) (+.p16 x (real->posit16 1))) (*.p16 (/.p16 (real->posit16 1) (*.p16 (-.p16 x (real->posit16 1)) (+.p16 (real->posit16 1) x))) (+.p16 x (real->posit16 1)))) (/.p16 (real->posit16 2) x)))> #posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (real->posit16 2) x)) (*.p16 (/.p16 (real->posit16 1) (*.p16 (+.p16 x (real->posit16 1)) (-.p16 x (real->posit16 1)))) (+.p16 x (real->posit16 1)))))> #posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1)))) (+.p16 (/.p16 (real->posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1))))) (*.p16 (/.p16 (real->posit16 2) x) (/.p16 (real->posit16 2) x))) (+.p16 (+.p16 (/.p16 (real->posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1)))) (/.p16 (real->posit16 2) x))))> #posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1)))) (+.p16 (/.p16 (real->posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1))))) (*.p16 (+.p16 (/.p16 (real->posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1)))) (+.p16 (/.p16 (real->posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1)))))) (*.p16 (*.p16 (/.p16 (real->posit16 2) x) (/.p16 (real->posit16 2) x)) (*.p16 (/.p16 (real->posit16 2) x) (/.p16 (real->posit16 2) x)))) (*.p16 (+.p16 (+.p16 (/.p16 (real->posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1)))) (/.p16 (real->posit16 2) x)) (+.p16 (*.p16 (+.p16 (/.p16 (real->posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1)))) (+.p16 (/.p16 (real->posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1))))) (*.p16 (/.p16 (real->posit16 2) x) (/.p16 (real->posit16 2) x))))))> #posit16 1) (+.p16 x (real->posit16 1))) (+.p16 (/.p16 (real->posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1))))) (-.p16 (*.p16 (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1))) (+.p16 (/.p16 (real->posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1))))) (*.p16 (/.p16 (real->posit16 2) x) (/.p16 (real->posit16 2) x)))) (+.p16 (+.p16 (/.p16 (real->posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1)))) (/.p16 (real->posit16 2) x))))> #posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (real->posit16 2) x)) (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1)))))> #posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (real->posit16 2) x)) (+.p16 (/.p16 (real->posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (real->posit16 2) x))) (+.p16 (/.p16 (real->posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (real->posit16 2) x))) (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1)))))> #posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1)))) (/.p16 (real->posit16 2) x)) (-.p16 (+.p16 (/.p16 (real->posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1)))) (/.p16 (real->posit16 2) x))) (+.p16 (+.p16 (/.p16 (real->posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1)))) (/.p16 (real->posit16 2) x))))> #posit16 1) (+.p16 x (real->posit16 1))) (-.p16 (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1))) (/.p16 (real->posit16 2) x))))>) 12.735 * * * [regime-changes]: Trying 1 branch expressions: (x) 12.735 * * * * [regimes]: Trying to branch on x from (#posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (*.p16 (+.p16 (/.p16 (real->posit16 2) x) (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1)))) (-.p16 (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1))) (/.p16 (real->posit16 2) x))) (+.p16 (/.p16 (real->posit16 2) x) (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1)))))))> #posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1)))) (/.p16 (real->posit16 2) x)) (/.p16 (+.p16 (+.p16 (/.p16 (real->posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1)))) (/.p16 (real->posit16 2) x)) (-.p16 (+.p16 (/.p16 (real->posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1)))) (/.p16 (real->posit16 2) x)))))> #posit16 1) (+.p16 x (real->posit16 1))) (*.p16 (/.p16 (real->posit16 1) (*.p16 (-.p16 x (real->posit16 1)) (+.p16 (real->posit16 1) x))) (+.p16 x (real->posit16 1)))) (/.p16 (real->posit16 2) x)))> #posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (real->posit16 2) x)) (*.p16 (/.p16 (real->posit16 1) (*.p16 (+.p16 x (real->posit16 1)) (-.p16 x (real->posit16 1)))) (+.p16 x (real->posit16 1)))))> #posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1)))) (+.p16 (/.p16 (real->posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1))))) (*.p16 (/.p16 (real->posit16 2) x) (/.p16 (real->posit16 2) x))) (+.p16 (+.p16 (/.p16 (real->posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1)))) (/.p16 (real->posit16 2) x))))> #posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1)))) (+.p16 (/.p16 (real->posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1))))) (*.p16 (+.p16 (/.p16 (real->posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1)))) (+.p16 (/.p16 (real->posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1)))))) (*.p16 (*.p16 (/.p16 (real->posit16 2) x) (/.p16 (real->posit16 2) x)) (*.p16 (/.p16 (real->posit16 2) x) (/.p16 (real->posit16 2) x)))) (*.p16 (+.p16 (+.p16 (/.p16 (real->posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1)))) (/.p16 (real->posit16 2) x)) (+.p16 (*.p16 (+.p16 (/.p16 (real->posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1)))) (+.p16 (/.p16 (real->posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1))))) (*.p16 (/.p16 (real->posit16 2) x) (/.p16 (real->posit16 2) x))))))> #posit16 1) (+.p16 x (real->posit16 1))) (+.p16 (/.p16 (real->posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1))))) (-.p16 (*.p16 (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1))) (+.p16 (/.p16 (real->posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1))))) (*.p16 (/.p16 (real->posit16 2) x) (/.p16 (real->posit16 2) x)))) (+.p16 (+.p16 (/.p16 (real->posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1)))) (/.p16 (real->posit16 2) x))))> #posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (real->posit16 2) x)) (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1)))))> #posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (real->posit16 2) x)) (+.p16 (/.p16 (real->posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (real->posit16 2) x))) (+.p16 (/.p16 (real->posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (real->posit16 2) x))) (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1)))))> #posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1)))) (/.p16 (real->posit16 2) x)) (-.p16 (+.p16 (/.p16 (real->posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1)))) (/.p16 (real->posit16 2) x))) (+.p16 (+.p16 (/.p16 (real->posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1)))) (/.p16 (real->posit16 2) x))))> #posit16 1) (+.p16 x (real->posit16 1))) (-.p16 (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1))) (/.p16 (real->posit16 2) x))))>) 12.990 * * * [regime]: Found split indices: #