0.002 * [progress]: [Phase 1 of 3] Setting up. 0.002 * * * [progress]: [1/2] Preparing points 0.002 * * * * [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.007 * * * * [points]: Setting MPFR precision to 64 0.008 * * * * [points]: Setting MPFR precision to 320 0.010 * * * * [points]: Computing exacts on every 8 of 256 points to ramp up precision 0.014 * * * * [points]: Setting MPFR precision to 64 0.017 * * * * [points]: Setting MPFR precision to 320 0.019 * * * * [points]: Computing exacts on every 4 of 256 points to ramp up precision 0.024 * * * * [points]: Setting MPFR precision to 64 0.029 * * * * [points]: Setting MPFR precision to 320 0.033 * * * * [points]: Computing exacts on every 2 of 256 points to ramp up precision 0.038 * * * * [points]: Setting MPFR precision to 64 0.046 * * * * [points]: Setting MPFR precision to 320 0.053 * * * * [points]: Computing exacts for 256 points 0.058 * * * * [points]: Setting MPFR precision to 64 0.094 * * * * [points]: Setting MPFR precision to 320 0.117 * * * * [points]: Filtering points with unrepresentable outputs 0.117 * * * * [points]: Sampled 256 points with exact outputs 0.118 * * * [progress]: [2/2] Setting up program. 0.142 * [progress]: [Phase 2 of 3] Improving. 0.142 * * * * [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.142 * [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.142 * * [simplify]: iteration 1: (12 enodes) 0.148 * * [simplify]: iteration 2: (35 enodes) 0.162 * * [simplify]: iteration 3: (83 enodes) 0.196 * * [simplify]: iteration 4: (233 enodes) 0.338 * * [simplify]: iteration 5: (1047 enodes) 1.644 * * [simplify]: Extracting #0: cost 1 inf + 0 1.644 * * [simplify]: Extracting #1: cost 63 inf + 0 1.646 * * [simplify]: Extracting #2: cost 424 inf + 0 1.654 * * [simplify]: Extracting #3: cost 1384 inf + 1 1.671 * * [simplify]: Extracting #4: cost 2011 inf + 6310 1.705 * * [simplify]: Extracting #5: cost 1965 inf + 268223 1.859 * * [simplify]: Extracting #6: cost 1004 inf + 1944471 2.120 * * [simplify]: Extracting #7: cost 229 inf + 3572048 2.472 * * [simplify]: Extracting #8: cost 7 inf + 4121456 2.706 * * [simplify]: Extracting #9: cost 0 inf + 4134475 3.016 * [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)) 3.030 * * [progress]: iteration 1 / 4 3.030 * * * [progress]: picking best candidate 3.044 * * * * [pick]: Picked #posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (real->posit16 2) x)) (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1)))))> 3.044 * * * [progress]: localizing error 3.222 * * * [progress]: generating rewritten candidates 3.222 * * * * [progress]: [ 1 / 4 ] rewriting at (2) 3.236 * * * * [progress]: [ 2 / 4 ] rewriting at (2 1) 3.239 * * * * [progress]: [ 3 / 4 ] rewriting at (2 1 1) 3.241 * * * * [progress]: [ 4 / 4 ] rewriting at (2 2) 3.243 * * * [progress]: generating series expansions 3.243 * * * * [progress]: [ 1 / 4 ] generating series at (2) 3.243 * * * * [progress]: [ 2 / 4 ] generating series at (2 1) 3.243 * * * * [progress]: [ 3 / 4 ] generating series at (2 1 1) 3.243 * * * * [progress]: [ 4 / 4 ] generating series at (2 2) 3.243 * * * [progress]: simplifying candidates 3.243 * * * * [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.243 * * * * [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.243 * * * * [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.244 * * * * [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.244 * * * * [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.244 * * * * [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.244 * * * * [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.244 * * * * [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.244 * * * * [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.244 * * * * [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.244 * [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.244 * * [simplify]: iteration 1: (23 enodes) 3.251 * * [simplify]: iteration 2: (69 enodes) 3.271 * * [simplify]: iteration 3: (191 enodes) 3.320 * * [simplify]: iteration 4: (708 enodes) 3.837 * * [simplify]: Extracting #0: cost 7 inf + 0 3.838 * * [simplify]: Extracting #1: cost 159 inf + 0 3.842 * * [simplify]: Extracting #2: cost 719 inf + 0 3.852 * * [simplify]: Extracting #3: cost 1116 inf + 59063 3.902 * * [simplify]: Extracting #4: cost 977 inf + 589227 4.033 * * [simplify]: Extracting #5: cost 431 inf + 1552307 4.201 * * [simplify]: Extracting #6: cost 98 inf + 2274244 4.445 * * [simplify]: Extracting #7: cost 0 inf + 2521505 4.645 * * [simplify]: Extracting #8: cost 0 inf + 2496545 4.869 * [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.870 * * * [progress]: adding candidates to table 5.231 * * [progress]: iteration 2 / 4 5.231 * * * [progress]: picking best candidate 5.299 * * * * [pick]: Picked #posit16 1) (+.p16 x (real->posit16 1))) (-.p16 (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1))) (/.p16 (real->posit16 2) x))))> 5.299 * * * [progress]: localizing error 5.533 * * * [progress]: generating rewritten candidates 5.533 * * * * [progress]: [ 1 / 4 ] rewriting at (2) 5.541 * * * * [progress]: [ 2 / 4 ] rewriting at (2 2) 5.545 * * * * [progress]: [ 3 / 4 ] rewriting at (2 1) 5.547 * * * * [progress]: [ 4 / 4 ] rewriting at (2 2 1) 5.549 * * * [progress]: generating series expansions 5.549 * * * * [progress]: [ 1 / 4 ] generating series at (2) 5.549 * * * * [progress]: [ 2 / 4 ] generating series at (2 2) 5.549 * * * * [progress]: [ 3 / 4 ] generating series at (2 1) 5.549 * * * * [progress]: [ 4 / 4 ] generating series at (2 2 1) 5.549 * * * [progress]: simplifying candidates 5.549 * * * * [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))))> 5.549 * * * * [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)))> 5.549 * * * * [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)))))> 5.549 * * * * [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)))))> 5.550 * * * * [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)))))> 5.550 * * * * [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))))> 5.550 * * * * [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))))> 5.550 * * * * [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))))> 5.550 * * * * [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))))> 5.550 * * * * [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))))> 5.550 * [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))) 5.550 * * [simplify]: iteration 1: (22 enodes) 5.560 * * [simplify]: iteration 2: (62 enodes) 5.579 * * [simplify]: iteration 3: (168 enodes) 5.636 * * [simplify]: iteration 4: (708 enodes) 6.790 * * [simplify]: Extracting #0: cost 6 inf + 0 6.791 * * [simplify]: Extracting #1: cost 154 inf + 0 6.796 * * [simplify]: Extracting #2: cost 815 inf + 0 6.808 * * [simplify]: Extracting #3: cost 1510 inf + 7988 6.847 * * [simplify]: Extracting #4: cost 1564 inf + 391339 7.053 * * [simplify]: Extracting #5: cost 389 inf + 2721949 7.211 * * [simplify]: Extracting #6: cost 44 inf + 3392628 7.428 * * [simplify]: Extracting #7: cost 1 inf + 3495039 7.723 * * [simplify]: Extracting #8: cost 0 inf + 3496722 8.016 * [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)))) 8.016 * * * [progress]: adding candidates to table 8.383 * * [progress]: iteration 3 / 4 8.383 * * * [progress]: picking best candidate 8.438 * * * * [pick]: Picked #posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1)))) (/.p16 (real->posit16 2) x)))> 8.438 * * * [progress]: localizing error 8.708 * * * [progress]: generating rewritten candidates 8.708 * * * * [progress]: [ 1 / 4 ] rewriting at (2) 8.735 * * * * [progress]: [ 2 / 4 ] rewriting at (2 1) 8.745 * * * * [progress]: [ 3 / 4 ] rewriting at (2 1 1) 8.750 * * * * [progress]: [ 4 / 4 ] rewriting at (2 1 2) 8.753 * * * [progress]: generating series expansions 8.753 * * * * [progress]: [ 1 / 4 ] generating series at (2) 8.753 * * * * [progress]: [ 2 / 4 ] generating series at (2 1) 8.753 * * * * [progress]: [ 3 / 4 ] generating series at (2 1 1) 8.754 * * * * [progress]: [ 4 / 4 ] generating series at (2 1 2) 8.754 * * * [progress]: simplifying candidates 8.754 * * * * [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))))> 8.754 * * * * [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))))> 8.754 * * * * [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))))> 8.754 * * * * [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)))> 8.754 * * * * [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)))> 8.754 * * * * [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)))> 8.754 * * * * [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)))> 8.754 * * * * [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)))> 8.754 * * * * [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)))> 8.755 * [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)))) 8.755 * * [simplify]: iteration 1: (21 enodes) 8.766 * * [simplify]: iteration 2: (66 enodes) 8.794 * * [simplify]: iteration 3: (202 enodes) 8.856 * * [simplify]: iteration 4: (864 enodes) 9.887 * * [simplify]: Extracting #0: cost 6 inf + 0 9.888 * * [simplify]: Extracting #1: cost 150 inf + 0 9.893 * * [simplify]: Extracting #2: cost 959 inf + 0 9.905 * * [simplify]: Extracting #3: cost 1589 inf + 3015 9.922 * * [simplify]: Extracting #4: cost 1751 inf + 65385 10.005 * * [simplify]: Extracting #5: cost 1025 inf + 1314833 10.260 * * [simplify]: Extracting #6: cost 146 inf + 3380005 10.655 * * [simplify]: Extracting #7: cost 0 inf + 3799193 10.916 * * [simplify]: Extracting #8: cost 0 inf + 3789873 11.182 * [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))) 11.183 * * * [progress]: adding candidates to table 11.415 * * [progress]: iteration 4 / 4 11.415 * * * [progress]: picking best candidate 11.490 * * * * [pick]: Picked #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)))))> 11.490 * * * [progress]: localizing error 11.701 * * * [progress]: generating rewritten candidates 11.702 * * * * [progress]: [ 1 / 4 ] rewriting at (2) 11.724 * * * * [progress]: [ 2 / 4 ] rewriting at (2 2) 11.741 * * * * [progress]: [ 3 / 4 ] rewriting at (2 1) 11.748 * * * * [progress]: [ 4 / 4 ] rewriting at (2 2 1 2) 11.758 * * * [progress]: generating series expansions 11.758 * * * * [progress]: [ 1 / 4 ] generating series at (2) 11.758 * * * * [progress]: [ 2 / 4 ] generating series at (2 2) 11.758 * * * * [progress]: [ 3 / 4 ] generating series at (2 1) 11.758 * * * * [progress]: [ 4 / 4 ] generating series at (2 2 1 2) 11.758 * * * [progress]: simplifying candidates 11.758 * * * * [progress]: [ 1 / 20 ] simplifiying candidate #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)))) x)) (*.p16 (/.p16 (real->posit16 1) (*.p16 (+.p16 x (real->posit16 1)) (-.p16 x (real->posit16 1)))) (real->posit16 1))))> 11.759 * * * * [progress]: [ 2 / 20 ] simplifiying candidate #posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (real->posit16 2) x)) (*.p16 x (/.p16 (real->posit16 1) (*.p16 (+.p16 x (real->posit16 1)) (-.p16 x (real->posit16 1)))))) (*.p16 (real->posit16 1) (/.p16 (real->posit16 1) (*.p16 (+.p16 x (real->posit16 1)) (-.p16 x (real->posit16 1)))))))> 11.759 * * * * [progress]: [ 3 / 20 ] simplifiying candidate #posit16 1) (+.p16 x (real->posit16 1))) (+.p16 (neg.p16 (/.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))))))> 11.759 * * * * [progress]: [ 4 / 20 ] simplifiying candidate #posit16 1) (+.p16 x (real->posit16 1))) (-.p16 (/.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))))))> 11.759 * * * * [progress]: [ 5 / 20 ] simplifiying candidate #posit16 1) (*.p16 (+.p16 x (real->posit16 1)) (-.p16 x (real->posit16 1)))) (+.p16 x (real->posit16 1))) (-.p16 (/.p16 (real->posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (real->posit16 2) x))))> 11.759 * * * * [progress]: [ 6 / 20 ] simplifiying candidate #posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (real->posit16 2) x)) (+.p16 (*.p16 (/.p16 (real->posit16 1) (*.p16 (+.p16 x (real->posit16 1)) (-.p16 x (real->posit16 1)))) x) (*.p16 (/.p16 (real->posit16 1) (*.p16 (+.p16 x (real->posit16 1)) (-.p16 x (real->posit16 1)))) (real->posit16 1)))))> 11.759 * * * * [progress]: [ 7 / 20 ] simplifiying candidate #posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (real->posit16 2) x)) (+.p16 (*.p16 x (/.p16 (real->posit16 1) (*.p16 (+.p16 x (real->posit16 1)) (-.p16 x (real->posit16 1))))) (*.p16 (real->posit16 1) (/.p16 (real->posit16 1) (*.p16 (+.p16 x (real->posit16 1)) (-.p16 x (real->posit16 1))))))))> 11.759 * * * * [progress]: [ 8 / 20 ] simplifiying candidate #posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (real->posit16 2) x)) (*.p16 (/.p16 (real->posit16 1) (*.p16 (+.p16 x (real->posit16 1)) (-.p16 (*.p16 x x) (*.p16 (real->posit16 1) (real->posit16 1))))) (*.p16 (+.p16 x (real->posit16 1)) (+.p16 x (real->posit16 1))))))> 11.759 * * * * [progress]: [ 9 / 20 ] simplifiying candidate #posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (real->posit16 2) x)) (/.p16 (*.p16 (real->posit16 1) (+.p16 x (real->posit16 1))) (*.p16 (+.p16 x (real->posit16 1)) (-.p16 x (real->posit16 1))))))> 11.759 * * * * [progress]: [ 10 / 20 ] simplifiying candidate #posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (real->posit16 2) x)) (*.p16 (+.p16 x (real->posit16 1)) (/.p16 (real->posit16 1) (*.p16 (+.p16 x (real->posit16 1)) (-.p16 x (real->posit16 1)))))))> 11.759 * * * * [progress]: [ 11 / 20 ] simplifiying candidate #posit16 1) (+.p16 x (real->posit16 1))) (neg.p16 (/.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)))))> 11.759 * * * * [progress]: [ 12 / 20 ] 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 (/.p16 (real->posit16 1) (*.p16 (+.p16 x (real->posit16 1)) (-.p16 x (real->posit16 1)))) (+.p16 x (real->posit16 1)))))> 11.759 * * * * [progress]: [ 13 / 20 ] simplifiying candidate #posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (real->posit16 2) x)) (*.p16 (/.p16 (real->posit16 1) (+.p16 (*.p16 (+.p16 x (real->posit16 1)) x) (*.p16 (+.p16 x (real->posit16 1)) (neg.p16 (real->posit16 1))))) (+.p16 x (real->posit16 1)))))> 11.759 * * * * [progress]: [ 14 / 20 ] simplifiying candidate #posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (real->posit16 2) x)) (*.p16 (/.p16 (real->posit16 1) (+.p16 (*.p16 x (+.p16 x (real->posit16 1))) (*.p16 (neg.p16 (real->posit16 1)) (+.p16 x (real->posit16 1))))) (+.p16 x (real->posit16 1)))))> 11.760 * * * * [progress]: [ 15 / 20 ] simplifiying candidate #posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (real->posit16 2) x)) (*.p16 (/.p16 (real->posit16 1) (/.p16 (*.p16 (+.p16 x (real->posit16 1)) (-.p16 (*.p16 x x) (*.p16 (real->posit16 1) (real->posit16 1)))) (+.p16 x (real->posit16 1)))) (+.p16 x (real->posit16 1)))))> 11.760 * * * * [progress]: [ 16 / 20 ] simplifiying candidate #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)))))> 11.760 * * * * [progress]: [ 17 / 20 ] simplifiying candidate #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)))))> 11.760 * * * * [progress]: [ 18 / 20 ] simplifiying candidate #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)))))> 11.760 * * * * [progress]: [ 19 / 20 ] simplifiying candidate #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)))))> 11.760 * * * * [progress]: [ 20 / 20 ] simplifiying candidate #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)))))> 11.760 * [simplify]: Simplifying (+.p16 (-.p16 (/.p16 (real->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)))) x)), (+.p16 (-.p16 (/.p16 (real->posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (real->posit16 2) x)) (*.p16 x (/.p16 (real->posit16 1) (*.p16 (+.p16 x (real->posit16 1)) (-.p16 x (real->posit16 1)))))), (+.p16 (neg.p16 (/.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)))), (-.p16 (/.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)))), (*.p16 (/.p16 (real->posit16 1) (*.p16 (+.p16 x (real->posit16 1)) (-.p16 x (real->posit16 1)))) x), (*.p16 (/.p16 (real->posit16 1) (*.p16 (+.p16 x (real->posit16 1)) (-.p16 x (real->posit16 1)))) (real->posit16 1)), (*.p16 x (/.p16 (real->posit16 1) (*.p16 (+.p16 x (real->posit16 1)) (-.p16 x (real->posit16 1))))), (*.p16 (real->posit16 1) (/.p16 (real->posit16 1) (*.p16 (+.p16 x (real->posit16 1)) (-.p16 x (real->posit16 1))))), (*.p16 (+.p16 x (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 (+.p16 x (real->posit16 1)) x), (*.p16 (+.p16 x (real->posit16 1)) (neg.p16 (real->posit16 1))), (*.p16 x (+.p16 x (real->posit16 1))), (*.p16 (neg.p16 (real->posit16 1)) (+.p16 x (real->posit16 1))), (*.p16 (+.p16 x (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 (/.p16 (real->posit16 1) (*.p16 (+.p16 x (real->posit16 1)) (-.p16 x (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 (/.p16 (real->posit16 1) (*.p16 (+.p16 x (real->posit16 1)) (-.p16 x (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 (/.p16 (real->posit16 1) (*.p16 (+.p16 x (real->posit16 1)) (-.p16 x (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 (/.p16 (real->posit16 1) (*.p16 (+.p16 x (real->posit16 1)) (-.p16 x (real->posit16 1)))) (+.p16 x (real->posit16 1)))) 11.761 * * [simplify]: iteration 1: (38 enodes) 11.781 * * [simplify]: iteration 2: (114 enodes) 11.832 * * [simplify]: iteration 3: (372 enodes) 11.992 * * [simplify]: iteration 4: (1812 enodes) 36.826 * * [simplify]: Extracting #0: cost 14 inf + 0 36.829 * * [simplify]: Extracting #1: cost 658 inf + 0 36.849 * * [simplify]: Extracting #2: cost 2592 inf + 322 36.882 * * [simplify]: Extracting #3: cost 3868 inf + 1647 36.939 * * [simplify]: Extracting #4: cost 4725 inf + 100014 37.247 * * [simplify]: Extracting #5: cost 2905 inf + 3769024 37.807 * * [simplify]: Extracting #6: cost 413 inf + 9314868 38.635 * * [simplify]: Extracting #7: cost 24 inf + 10120561 39.427 * * [simplify]: Extracting #8: cost 0 inf + 10174338 40.205 * * [simplify]: Extracting #9: cost 0 inf + 10174218 40.907 * [simplify]: Simplified to (-.p16 (*.p16 (+.p16 (/.p16 x (-.p16 x (real->posit16 1))) (real->posit16 1.0)) (/.p16 (real->posit16 1) (+.p16 x (real->posit16 1)))) (/.p16 (real->posit16 2) x)), (-.p16 (*.p16 (+.p16 (/.p16 x (-.p16 x (real->posit16 1))) (real->posit16 1.0)) (/.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 2) x) (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1)))), (/.p16 (*.p16 x (real->posit16 1)) (*.p16 (-.p16 x (real->posit16 1)) (+.p16 x (real->posit16 1)))), (/.p16 (*.p16 (real->posit16 1) (real->posit16 1)) (*.p16 (-.p16 x (real->posit16 1)) (+.p16 x (real->posit16 1)))), (/.p16 (*.p16 x (real->posit16 1)) (*.p16 (-.p16 x (real->posit16 1)) (+.p16 x (real->posit16 1)))), (/.p16 (*.p16 (real->posit16 1) (real->posit16 1)) (*.p16 (-.p16 x (real->posit16 1)) (+.p16 x (real->posit16 1)))), (*.p16 (+.p16 x (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 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 (+.p16 x (real->posit16 1)) x), (*.p16 (+.p16 x (real->posit16 1)) (neg.p16 (real->posit16 1))), (*.p16 (+.p16 x (real->posit16 1)) x), (*.p16 (+.p16 x (real->posit16 1)) (neg.p16 (real->posit16 1))), (*.p16 (*.p16 (-.p16 x (real->posit16 1)) (+.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))) 40.909 * * * [progress]: adding candidates to table 41.847 * [progress]: [Phase 3 of 3] Extracting. 41.847 * * [regime]: Finding splitpoints for: (#posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (real->posit16 2) x)) (*.p16 (/.p16 (real->posit16 1) (/.p16 (*.p16 (*.p16 (-.p16 x (real->posit16 1)) (+.p16 x (real->posit16 1))) (+.p16 x (real->posit16 1))) (+.p16 x (real->posit16 1)))) (+.p16 x (real->posit16 1)))))> #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 (*.p16 x x) (*.p16 (real->posit16 1) (real->posit16 1))))) (*.p16 (+.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 (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1))) (/.p16 (real->posit16 2) x))))> #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 2) x)) (*.p16 (/.p16 (real->posit16 1) (*.p16 (+.p16 x (real->posit16 1)) (-.p16 x (real->posit16 1)))) x)) (*.p16 (/.p16 (real->posit16 1) (*.p16 (+.p16 x (real->posit16 1)) (-.p16 x (real->posit16 1)))) (real->posit16 1))))> #posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (real->posit16 2) x)) (*.p16 (/.p16 (real->posit16 1) (+.p16 (*.p16 x (+.p16 x (real->posit16 1))) (*.p16 (neg.p16 (real->posit16 1)) (+.p16 x (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 (+.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 (real->posit16 2) x)))>) 41.849 * * * [regime-changes]: Trying 1 branch expressions: (x) 41.849 * * * * [regimes]: Trying to branch on x from (#posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (real->posit16 2) x)) (*.p16 (/.p16 (real->posit16 1) (/.p16 (*.p16 (*.p16 (-.p16 x (real->posit16 1)) (+.p16 x (real->posit16 1))) (+.p16 x (real->posit16 1))) (+.p16 x (real->posit16 1)))) (+.p16 x (real->posit16 1)))))> #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 (*.p16 x x) (*.p16 (real->posit16 1) (real->posit16 1))))) (*.p16 (+.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 (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1))) (/.p16 (real->posit16 2) x))))> #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 2) x)) (*.p16 (/.p16 (real->posit16 1) (*.p16 (+.p16 x (real->posit16 1)) (-.p16 x (real->posit16 1)))) x)) (*.p16 (/.p16 (real->posit16 1) (*.p16 (+.p16 x (real->posit16 1)) (-.p16 x (real->posit16 1)))) (real->posit16 1))))> #posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (real->posit16 2) x)) (*.p16 (/.p16 (real->posit16 1) (+.p16 (*.p16 x (+.p16 x (real->posit16 1))) (*.p16 (neg.p16 (real->posit16 1)) (+.p16 x (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 (+.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 (real->posit16 2) x)))>) 42.080 * * * [regime]: Found split indices: #