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.007 * * * * [points]: Setting MPFR precision to 64 0.009 * * * * [points]: Setting MPFR precision to 320 0.010 * * * * [points]: Computing exacts on every 8 of 256 points to ramp up precision 0.015 * * * * [points]: Setting MPFR precision to 64 0.018 * * * * [points]: Setting MPFR precision to 320 0.021 * * * * [points]: Computing exacts on every 4 of 256 points to ramp up precision 0.026 * * * * [points]: Setting MPFR precision to 64 0.030 * * * * [points]: Setting MPFR precision to 320 0.035 * * * * [points]: Computing exacts on every 2 of 256 points to ramp up precision 0.040 * * * * [points]: Setting MPFR precision to 64 0.048 * * * * [points]: Setting MPFR precision to 320 0.056 * * * * [points]: Computing exacts for 256 points 0.062 * * * * [points]: Setting MPFR precision to 64 0.087 * * * * [points]: Setting MPFR precision to 320 0.109 * * * * [points]: Filtering points with unrepresentable outputs 0.110 * * * * [points]: Sampled 256 points with exact outputs 0.110 * * * [progress]: [2/2] Setting up program. 0.132 * [progress]: [Phase 2 of 3] Improving. 0.132 * * * * [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.132 * [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.132 * * [simplify]: iters left: 5 (12 enodes) 0.139 * * [simplify]: iters left: 4 (35 enodes) 0.168 * * [simplify]: iters left: 3 (83 enodes) 0.198 * * [simplify]: iters left: 2 (233 enodes) 0.300 * * [simplify]: Extracting #0: cost 1 inf + 0 0.300 * * [simplify]: Extracting #1: cost 29 inf + 0 0.300 * * [simplify]: Extracting #2: cost 123 inf + 0 0.301 * * [simplify]: Extracting #3: cost 244 inf + 1 0.303 * * [simplify]: Extracting #4: cost 308 inf + 32857 0.314 * * [simplify]: Extracting #5: cost 149 inf + 308686 0.336 * * [simplify]: Extracting #6: cost 4 inf + 549893 0.360 * * [simplify]: Extracting #7: cost 0 inf + 561504 0.386 * [simplify]: Simplified to (+.p16 (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1))) (-.p16 (/.p16 (real->posit16 1) (+.p16 (real->posit16 1) x)) (/.p16 (real->posit16 2) x))) 0.386 * [simplify]: Simplified (2) to (λ (x) (+.p16 (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1))) (-.p16 (/.p16 (real->posit16 1) (+.p16 (real->posit16 1) x)) (/.p16 (real->posit16 2) x)))) 0.399 * * [progress]: iteration 1 / 4 0.399 * * * [progress]: picking best candidate 0.419 * * * * [pick]: Picked #posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (real->posit16 2) x)) (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1)))))> 0.419 * * * [progress]: localizing error 0.683 * * * [progress]: generating rewritten candidates 0.683 * * * * [progress]: [ 1 / 4 ] rewriting at (2) 0.703 * * * * [progress]: [ 2 / 4 ] rewriting at (2 1) 0.708 * * * * [progress]: [ 3 / 4 ] rewriting at (2 1 1) 0.711 * * * * [progress]: [ 4 / 4 ] rewriting at (2 2) 0.724 * * * [progress]: generating series expansions 0.724 * * * * [progress]: [ 1 / 4 ] generating series at (2) 0.724 * * * * [progress]: [ 2 / 4 ] generating series at (2 1) 0.724 * * * * [progress]: [ 3 / 4 ] generating series at (2 1 1) 0.724 * * * * [progress]: [ 4 / 4 ] generating series at (2 2) 0.725 * * * [progress]: simplifying candidates 0.725 * * * * [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))))))> 0.725 * [simplify]: Simplifying (/.p16 (real->posit16 1) (+.p16 x (real->posit16 1))) 0.725 * * [simplify]: iters left: 3 (5 enodes) 0.727 * * [simplify]: iters left: 2 (11 enodes) 0.731 * * [simplify]: iters left: 1 (13 enodes) 0.734 * * [simplify]: Extracting #0: cost 1 inf + 0 0.734 * * [simplify]: Extracting #1: cost 3 inf + 0 0.734 * * [simplify]: Extracting #2: cost 5 inf + 0 0.734 * * [simplify]: Extracting #3: cost 3 inf + 2 0.734 * * [simplify]: Extracting #4: cost 0 inf + 527 0.734 * [simplify]: Simplified to (/.p16 (real->posit16 1) (+.p16 (real->posit16 1) x)) 0.734 * [simplify]: Simplified (2 1) to (λ (x) (+.p16 (/.p16 (real->posit16 1) (+.p16 (real->posit16 1) x)) (+.p16 (neg.p16 (/.p16 (real->posit16 2) x)) (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1)))))) 0.734 * * * * [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))))))> 0.735 * [simplify]: Simplifying (/.p16 (real->posit16 1) (+.p16 x (real->posit16 1))) 0.735 * * [simplify]: iters left: 3 (5 enodes) 0.737 * * [simplify]: iters left: 2 (11 enodes) 0.740 * * [simplify]: iters left: 1 (13 enodes) 0.743 * * [simplify]: Extracting #0: cost 1 inf + 0 0.743 * * [simplify]: Extracting #1: cost 3 inf + 0 0.743 * * [simplify]: Extracting #2: cost 5 inf + 0 0.743 * * [simplify]: Extracting #3: cost 3 inf + 2 0.744 * * [simplify]: Extracting #4: cost 0 inf + 527 0.744 * [simplify]: Simplified to (/.p16 (real->posit16 1) (+.p16 (real->posit16 1) x)) 0.744 * [simplify]: Simplified (2 1) to (λ (x) (-.p16 (/.p16 (real->posit16 1) (+.p16 (real->posit16 1) x)) (-.p16 (/.p16 (real->posit16 2) x) (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1)))))) 0.744 * * * * [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))))> 0.744 * * * * [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)))))> 0.744 * * * * [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)))))> 0.744 * * * * [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)))))> 0.744 * [simplify]: Simplifying (+.p16 x (real->posit16 1)) 0.744 * * [simplify]: iters left: 2 (4 enodes) 0.746 * * [simplify]: iters left: 1 (10 enodes) 0.747 * * [simplify]: Extracting #0: cost 1 inf + 0 0.747 * * [simplify]: Extracting #1: cost 3 inf + 0 0.747 * * [simplify]: Extracting #2: cost 3 inf + 1 0.747 * * [simplify]: Extracting #3: cost 0 inf + 45 0.748 * [simplify]: Simplified to (+.p16 (real->posit16 1) x) 0.748 * [simplify]: Simplified (2 2 2) to (λ (x) (+.p16 (-.p16 (/.p16 (real->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 (real->posit16 1) x)))) 0.748 * * * * [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)))))> 0.748 * [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.748 * * [simplify]: iters left: 5 (12 enodes) 0.751 * * [simplify]: iters left: 4 (35 enodes) 0.757 * * [simplify]: iters left: 3 (83 enodes) 0.784 * * [simplify]: iters left: 2 (233 enodes) 0.867 * * [simplify]: Extracting #0: cost 1 inf + 0 0.867 * * [simplify]: Extracting #1: cost 29 inf + 0 0.867 * * [simplify]: Extracting #2: cost 123 inf + 0 0.868 * * [simplify]: Extracting #3: cost 244 inf + 1 0.870 * * [simplify]: Extracting #4: cost 308 inf + 32857 0.881 * * [simplify]: Extracting #5: cost 149 inf + 308686 0.912 * * [simplify]: Extracting #6: cost 4 inf + 549893 0.945 * * [simplify]: Extracting #7: cost 0 inf + 561504 0.969 * [simplify]: Simplified to (+.p16 (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1))) (-.p16 (/.p16 (real->posit16 1) (+.p16 (real->posit16 1) x)) (/.p16 (real->posit16 2) x))) 0.969 * [simplify]: Simplified (2) to (λ (x) (+.p16 (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1))) (-.p16 (/.p16 (real->posit16 1) (+.p16 (real->posit16 1) x)) (/.p16 (real->posit16 2) x)))) 0.970 * * * * [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)))))> 0.970 * [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.970 * * [simplify]: iters left: 5 (12 enodes) 0.973 * * [simplify]: iters left: 4 (35 enodes) 0.984 * * [simplify]: iters left: 3 (83 enodes) 1.008 * * [simplify]: iters left: 2 (233 enodes) 1.087 * * [simplify]: Extracting #0: cost 1 inf + 0 1.087 * * [simplify]: Extracting #1: cost 29 inf + 0 1.087 * * [simplify]: Extracting #2: cost 123 inf + 0 1.088 * * [simplify]: Extracting #3: cost 244 inf + 1 1.090 * * [simplify]: Extracting #4: cost 308 inf + 32857 1.107 * * [simplify]: Extracting #5: cost 149 inf + 308686 1.132 * * [simplify]: Extracting #6: cost 4 inf + 549893 1.168 * * [simplify]: Extracting #7: cost 0 inf + 561504 1.208 * [simplify]: Simplified to (+.p16 (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1))) (-.p16 (/.p16 (real->posit16 1) (+.p16 (real->posit16 1) x)) (/.p16 (real->posit16 2) x))) 1.208 * [simplify]: Simplified (2) to (λ (x) (+.p16 (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1))) (-.p16 (/.p16 (real->posit16 1) (+.p16 (real->posit16 1) x)) (/.p16 (real->posit16 2) x)))) 1.208 * * * * [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)))))> 1.208 * [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)))) 1.208 * * [simplify]: iters left: 5 (12 enodes) 1.211 * * [simplify]: iters left: 4 (35 enodes) 1.219 * * [simplify]: iters left: 3 (83 enodes) 1.248 * * [simplify]: iters left: 2 (233 enodes) 1.332 * * [simplify]: Extracting #0: cost 1 inf + 0 1.332 * * [simplify]: Extracting #1: cost 29 inf + 0 1.332 * * [simplify]: Extracting #2: cost 123 inf + 0 1.333 * * [simplify]: Extracting #3: cost 244 inf + 1 1.335 * * [simplify]: Extracting #4: cost 308 inf + 32857 1.346 * * [simplify]: Extracting #5: cost 149 inf + 308686 1.368 * * [simplify]: Extracting #6: cost 4 inf + 549893 1.409 * * [simplify]: Extracting #7: cost 0 inf + 561504 1.437 * [simplify]: Simplified to (+.p16 (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1))) (-.p16 (/.p16 (real->posit16 1) (+.p16 (real->posit16 1) x)) (/.p16 (real->posit16 2) x))) 1.437 * [simplify]: Simplified (2) to (λ (x) (+.p16 (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1))) (-.p16 (/.p16 (real->posit16 1) (+.p16 (real->posit16 1) x)) (/.p16 (real->posit16 2) x)))) 1.437 * * * * [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)))))> 1.437 * [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)))) 1.437 * * [simplify]: iters left: 5 (12 enodes) 1.443 * * [simplify]: iters left: 4 (35 enodes) 1.456 * * [simplify]: iters left: 3 (83 enodes) 1.485 * * [simplify]: iters left: 2 (233 enodes) 1.592 * * [simplify]: Extracting #0: cost 1 inf + 0 1.592 * * [simplify]: Extracting #1: cost 29 inf + 0 1.592 * * [simplify]: Extracting #2: cost 123 inf + 0 1.593 * * [simplify]: Extracting #3: cost 244 inf + 1 1.596 * * [simplify]: Extracting #4: cost 308 inf + 32857 1.619 * * [simplify]: Extracting #5: cost 149 inf + 308686 1.666 * * [simplify]: Extracting #6: cost 4 inf + 549893 1.714 * * [simplify]: Extracting #7: cost 0 inf + 561504 1.759 * [simplify]: Simplified to (+.p16 (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1))) (-.p16 (/.p16 (real->posit16 1) (+.p16 (real->posit16 1) x)) (/.p16 (real->posit16 2) x))) 1.759 * [simplify]: Simplified (2) to (λ (x) (+.p16 (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1))) (-.p16 (/.p16 (real->posit16 1) (+.p16 (real->posit16 1) x)) (/.p16 (real->posit16 2) x)))) 1.759 * * * [progress]: adding candidates to table 2.137 * * [progress]: iteration 2 / 4 2.137 * * * [progress]: picking best candidate 2.201 * * * * [pick]: Picked #posit16 1) (+.p16 x (real->posit16 1))) (+.p16 (neg.p16 (/.p16 (real->posit16 2) x)) (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1))))))> 2.201 * * * [progress]: localizing error 2.760 * * * [progress]: generating rewritten candidates 2.760 * * * * [progress]: [ 1 / 4 ] rewriting at (2) 2.766 * * * * [progress]: [ 2 / 4 ] rewriting at (2 2) 2.769 * * * * [progress]: [ 3 / 4 ] rewriting at (2 1) 2.771 * * * * [progress]: [ 4 / 4 ] rewriting at (2 2 2) 2.772 * * * [progress]: generating series expansions 2.773 * * * * [progress]: [ 1 / 4 ] generating series at (2) 2.773 * * * * [progress]: [ 2 / 4 ] generating series at (2 2) 2.773 * * * * [progress]: [ 3 / 4 ] generating series at (2 1) 2.773 * * * * [progress]: [ 4 / 4 ] generating series at (2 2 2) 2.773 * * * [progress]: simplifying candidates 2.773 * * * * [progress]: [ 1 / 8 ] 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)))))> 2.773 * [simplify]: Simplifying (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1))) 2.773 * * [simplify]: iters left: 3 (5 enodes) 2.775 * * [simplify]: iters left: 2 (17 enodes) 2.777 * * [simplify]: iters left: 1 (31 enodes) 2.783 * * [simplify]: Extracting #0: cost 1 inf + 0 2.783 * * [simplify]: Extracting #1: cost 11 inf + 0 2.783 * * [simplify]: Extracting #2: cost 28 inf + 0 2.783 * * [simplify]: Extracting #3: cost 29 inf + 324 2.783 * * [simplify]: Extracting #4: cost 22 inf + 6266 2.784 * * [simplify]: Extracting #5: cost 3 inf + 23256 2.785 * * [simplify]: Extracting #6: cost 0 inf + 26382 2.786 * * [simplify]: Extracting #7: cost 0 inf + 25822 2.787 * [simplify]: Simplified to (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1))) 2.787 * [simplify]: Simplified (2 2) to (λ (x) (+.p16 (+.p16 (/.p16 (real->posit16 1) (+.p16 x (real->posit16 1))) (neg.p16 (/.p16 (real->posit16 2) x))) (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1))))) 2.787 * * * * [progress]: [ 2 / 8 ] simplifiying candidate #posit16 2) x)) (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1)))) (/.p16 (real->posit16 1) (+.p16 x (real->posit16 1)))))> 2.787 * * * * [progress]: [ 3 / 8 ] 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)))))> 2.787 * * * * [progress]: [ 4 / 8 ] 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 x) (*.p16 (real->posit16 1) (real->posit16 1)))) (+.p16 x (real->posit16 1))))))> 2.787 * [simplify]: Simplifying (+.p16 x (real->posit16 1)) 2.787 * * [simplify]: iters left: 2 (4 enodes) 2.789 * * [simplify]: iters left: 1 (10 enodes) 2.790 * * [simplify]: Extracting #0: cost 1 inf + 0 2.790 * * [simplify]: Extracting #1: cost 3 inf + 0 2.790 * * [simplify]: Extracting #2: cost 3 inf + 1 2.790 * * [simplify]: Extracting #3: cost 0 inf + 45 2.790 * [simplify]: Simplified to (+.p16 (real->posit16 1) x) 2.790 * [simplify]: Simplified (2 2 2 2) to (λ (x) (+.p16 (/.p16 (real->posit16 1) (+.p16 x (real->posit16 1))) (+.p16 (neg.p16 (/.p16 (real->posit16 2) x)) (*.p16 (/.p16 (real->posit16 1) (-.p16 (*.p16 x x) (*.p16 (real->posit16 1) (real->posit16 1)))) (+.p16 (real->posit16 1) x))))) 2.791 * * * * [progress]: [ 5 / 8 ] 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))))))> 2.791 * [simplify]: Simplifying (/.p16 (real->posit16 1) (+.p16 x (real->posit16 1))) 2.791 * * [simplify]: iters left: 3 (5 enodes) 2.792 * * [simplify]: iters left: 2 (11 enodes) 2.794 * * [simplify]: iters left: 1 (13 enodes) 2.796 * * [simplify]: Extracting #0: cost 1 inf + 0 2.796 * * [simplify]: Extracting #1: cost 3 inf + 0 2.796 * * [simplify]: Extracting #2: cost 5 inf + 0 2.796 * * [simplify]: Extracting #3: cost 3 inf + 2 2.796 * * [simplify]: Extracting #4: cost 0 inf + 527 2.796 * [simplify]: Simplified to (/.p16 (real->posit16 1) (+.p16 (real->posit16 1) x)) 2.796 * [simplify]: Simplified (2 1) to (λ (x) (+.p16 (/.p16 (real->posit16 1) (+.p16 (real->posit16 1) x)) (+.p16 (neg.p16 (/.p16 (real->posit16 2) x)) (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1)))))) 2.796 * * * * [progress]: [ 6 / 8 ] 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))))))> 2.796 * [simplify]: Simplifying (/.p16 (real->posit16 1) (+.p16 x (real->posit16 1))) 2.796 * * [simplify]: iters left: 3 (5 enodes) 2.798 * * [simplify]: iters left: 2 (11 enodes) 2.799 * * [simplify]: iters left: 1 (13 enodes) 2.801 * * [simplify]: Extracting #0: cost 1 inf + 0 2.801 * * [simplify]: Extracting #1: cost 3 inf + 0 2.801 * * [simplify]: Extracting #2: cost 5 inf + 0 2.801 * * [simplify]: Extracting #3: cost 3 inf + 2 2.801 * * [simplify]: Extracting #4: cost 0 inf + 527 2.801 * [simplify]: Simplified to (/.p16 (real->posit16 1) (+.p16 (real->posit16 1) x)) 2.801 * [simplify]: Simplified (2 1) to (λ (x) (+.p16 (/.p16 (real->posit16 1) (+.p16 (real->posit16 1) x)) (+.p16 (neg.p16 (/.p16 (real->posit16 2) x)) (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1)))))) 2.802 * * * * [progress]: [ 7 / 8 ] 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))))))> 2.802 * [simplify]: Simplifying (/.p16 (real->posit16 1) (+.p16 x (real->posit16 1))) 2.802 * * [simplify]: iters left: 3 (5 enodes) 2.803 * * [simplify]: iters left: 2 (11 enodes) 2.809 * * [simplify]: iters left: 1 (13 enodes) 2.811 * * [simplify]: Extracting #0: cost 1 inf + 0 2.811 * * [simplify]: Extracting #1: cost 3 inf + 0 2.811 * * [simplify]: Extracting #2: cost 5 inf + 0 2.811 * * [simplify]: Extracting #3: cost 3 inf + 2 2.811 * * [simplify]: Extracting #4: cost 0 inf + 527 2.811 * [simplify]: Simplified to (/.p16 (real->posit16 1) (+.p16 (real->posit16 1) x)) 2.811 * [simplify]: Simplified (2 1) to (λ (x) (+.p16 (/.p16 (real->posit16 1) (+.p16 (real->posit16 1) x)) (+.p16 (neg.p16 (/.p16 (real->posit16 2) x)) (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1)))))) 2.811 * * * * [progress]: [ 8 / 8 ] 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))))))> 2.811 * [simplify]: Simplifying (/.p16 (real->posit16 1) (+.p16 x (real->posit16 1))) 2.811 * * [simplify]: iters left: 3 (5 enodes) 2.812 * * [simplify]: iters left: 2 (11 enodes) 2.814 * * [simplify]: iters left: 1 (13 enodes) 2.816 * * [simplify]: Extracting #0: cost 1 inf + 0 2.816 * * [simplify]: Extracting #1: cost 3 inf + 0 2.816 * * [simplify]: Extracting #2: cost 5 inf + 0 2.816 * * [simplify]: Extracting #3: cost 3 inf + 2 2.816 * * [simplify]: Extracting #4: cost 0 inf + 527 2.816 * [simplify]: Simplified to (/.p16 (real->posit16 1) (+.p16 (real->posit16 1) x)) 2.816 * [simplify]: Simplified (2 1) to (λ (x) (+.p16 (/.p16 (real->posit16 1) (+.p16 (real->posit16 1) x)) (+.p16 (neg.p16 (/.p16 (real->posit16 2) x)) (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1)))))) 2.816 * * * [progress]: adding candidates to table 3.029 * * [progress]: iteration 3 / 4 3.029 * * * [progress]: picking best candidate 3.071 * * * * [pick]: Picked #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.071 * * * [progress]: localizing error 3.294 * * * [progress]: generating rewritten candidates 3.294 * * * * [progress]: [ 1 / 4 ] rewriting at (2) 3.314 * * * * [progress]: [ 2 / 4 ] rewriting at (2 2) 3.317 * * * * [progress]: [ 3 / 4 ] rewriting at (2 1) 3.320 * * * * [progress]: [ 4 / 4 ] rewriting at (2 2 1) 3.322 * * * [progress]: generating series expansions 3.322 * * * * [progress]: [ 1 / 4 ] generating series at (2) 3.323 * * * * [progress]: [ 2 / 4 ] generating series at (2 2) 3.323 * * * * [progress]: [ 3 / 4 ] generating series at (2 1) 3.323 * * * * [progress]: [ 4 / 4 ] generating series at (2 2 1) 3.323 * * * [progress]: simplifying candidates 3.323 * * * * [progress]: [ 1 / 18 ] 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)))) x)) (*.p16 (/.p16 (real->posit16 1) (-.p16 (*.p16 x x) (*.p16 (real->posit16 1) (real->posit16 1)))) (real->posit16 1))))> 3.323 * [simplify]: Simplifying (*.p16 (/.p16 (real->posit16 1) (-.p16 (*.p16 x x) (*.p16 (real->posit16 1) (real->posit16 1)))) (real->posit16 1)) 3.323 * * [simplify]: iters left: 5 (8 enodes) 3.327 * * [simplify]: iters left: 4 (25 enodes) 3.332 * * [simplify]: iters left: 3 (62 enodes) 3.349 * * [simplify]: iters left: 2 (193 enodes) 3.461 * * [simplify]: Extracting #0: cost 1 inf + 0 3.461 * * [simplify]: Extracting #1: cost 65 inf + 0 3.462 * * [simplify]: Extracting #2: cost 241 inf + 0 3.464 * * [simplify]: Extracting #3: cost 260 inf + 43096 3.474 * * [simplify]: Extracting #4: cost 122 inf + 266467 3.499 * * [simplify]: Extracting #5: cost 18 inf + 464771 3.521 * * [simplify]: Extracting #6: cost 0 inf + 502437 3.542 * * [simplify]: Extracting #7: cost 0 inf + 501277 3.564 * [simplify]: Simplified to (/.p16 (*.p16 (real->posit16 1) (real->posit16 1)) (-.p16 (*.p16 x x) (*.p16 (real->posit16 1) (real->posit16 1)))) 3.564 * [simplify]: Simplified (2 2) to (λ (x) (+.p16 (+.p16 (-.p16 (/.p16 (real->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)))) x)) (/.p16 (*.p16 (real->posit16 1) (real->posit16 1)) (-.p16 (*.p16 x x) (*.p16 (real->posit16 1) (real->posit16 1)))))) 3.564 * * * * [progress]: [ 2 / 18 ] simplifiying candidate #posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (real->posit16 2) x)) (*.p16 x (/.p16 (real->posit16 1) (-.p16 (*.p16 x x) (*.p16 (real->posit16 1) (real->posit16 1)))))) (*.p16 (real->posit16 1) (/.p16 (real->posit16 1) (-.p16 (*.p16 x x) (*.p16 (real->posit16 1) (real->posit16 1)))))))> 3.564 * [simplify]: Simplifying (*.p16 (real->posit16 1) (/.p16 (real->posit16 1) (-.p16 (*.p16 x x) (*.p16 (real->posit16 1) (real->posit16 1))))) 3.564 * * [simplify]: iters left: 5 (8 enodes) 3.567 * * [simplify]: iters left: 4 (25 enodes) 3.574 * * [simplify]: iters left: 3 (62 enodes) 3.596 * * [simplify]: iters left: 2 (193 enodes) 3.717 * * [simplify]: Extracting #0: cost 1 inf + 0 3.717 * * [simplify]: Extracting #1: cost 65 inf + 0 3.718 * * [simplify]: Extracting #2: cost 241 inf + 0 3.720 * * [simplify]: Extracting #3: cost 260 inf + 43096 3.730 * * [simplify]: Extracting #4: cost 122 inf + 266467 3.749 * * [simplify]: Extracting #5: cost 18 inf + 464771 3.771 * * [simplify]: Extracting #6: cost 0 inf + 502437 3.794 * * [simplify]: Extracting #7: cost 0 inf + 501277 3.815 * [simplify]: Simplified to (/.p16 (*.p16 (real->posit16 1) (real->posit16 1)) (-.p16 (*.p16 x x) (*.p16 (real->posit16 1) (real->posit16 1)))) 3.815 * [simplify]: Simplified (2 2) to (λ (x) (+.p16 (+.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 x) (*.p16 (real->posit16 1) (real->posit16 1)))))) (/.p16 (*.p16 (real->posit16 1) (real->posit16 1)) (-.p16 (*.p16 x x) (*.p16 (real->posit16 1) (real->posit16 1)))))) 3.815 * * * * [progress]: [ 3 / 18 ] 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 x) (*.p16 (real->posit16 1) (real->posit16 1)))) (+.p16 x (real->posit16 1))))))> 3.815 * [simplify]: Simplifying (/.p16 (real->posit16 1) (+.p16 x (real->posit16 1))) 3.816 * * [simplify]: iters left: 3 (5 enodes) 3.817 * * [simplify]: iters left: 2 (11 enodes) 3.819 * * [simplify]: iters left: 1 (13 enodes) 3.821 * * [simplify]: Extracting #0: cost 1 inf + 0 3.821 * * [simplify]: Extracting #1: cost 3 inf + 0 3.821 * * [simplify]: Extracting #2: cost 5 inf + 0 3.821 * * [simplify]: Extracting #3: cost 3 inf + 2 3.821 * * [simplify]: Extracting #4: cost 0 inf + 527 3.821 * [simplify]: Simplified to (/.p16 (real->posit16 1) (+.p16 (real->posit16 1) x)) 3.821 * [simplify]: Simplified (2 1) to (λ (x) (+.p16 (/.p16 (real->posit16 1) (+.p16 (real->posit16 1) x)) (+.p16 (neg.p16 (/.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.821 * * * * [progress]: [ 4 / 18 ] simplifiying candidate #posit16 1) (+.p16 x (real->posit16 1))) (-.p16 (/.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.822 * [simplify]: Simplifying (/.p16 (real->posit16 1) (+.p16 x (real->posit16 1))) 3.822 * * [simplify]: iters left: 3 (5 enodes) 3.823 * * [simplify]: iters left: 2 (11 enodes) 3.825 * * [simplify]: iters left: 1 (13 enodes) 3.827 * * [simplify]: Extracting #0: cost 1 inf + 0 3.827 * * [simplify]: Extracting #1: cost 3 inf + 0 3.827 * * [simplify]: Extracting #2: cost 5 inf + 0 3.827 * * [simplify]: Extracting #3: cost 3 inf + 2 3.827 * * [simplify]: Extracting #4: cost 0 inf + 527 3.827 * [simplify]: Simplified to (/.p16 (real->posit16 1) (+.p16 (real->posit16 1) x)) 3.827 * [simplify]: Simplified (2 1) to (λ (x) (-.p16 (/.p16 (real->posit16 1) (+.p16 (real->posit16 1) x)) (-.p16 (/.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.827 * * * * [progress]: [ 5 / 18 ] simplifiying candidate #posit16 1) (-.p16 (*.p16 x x) (*.p16 (real->posit16 1) (real->posit16 1)))) (+.p16 x (real->posit16 1))) (-.p16 (/.p16 (real->posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (real->posit16 2) x))))> 3.827 * * * * [progress]: [ 6 / 18 ] simplifiying candidate #posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (real->posit16 2) x)) (+.p16 (*.p16 (/.p16 (real->posit16 1) (-.p16 (*.p16 x x) (*.p16 (real->posit16 1) (real->posit16 1)))) x) (*.p16 (/.p16 (real->posit16 1) (-.p16 (*.p16 x x) (*.p16 (real->posit16 1) (real->posit16 1)))) (real->posit16 1)))))> 3.827 * [simplify]: Simplifying (*.p16 (/.p16 (real->posit16 1) (-.p16 (*.p16 x x) (*.p16 (real->posit16 1) (real->posit16 1)))) (real->posit16 1)) 3.827 * * [simplify]: iters left: 5 (8 enodes) 3.829 * * [simplify]: iters left: 4 (25 enodes) 3.834 * * [simplify]: iters left: 3 (62 enodes) 3.848 * * [simplify]: iters left: 2 (193 enodes) 4.005 * * [simplify]: Extracting #0: cost 1 inf + 0 4.006 * * [simplify]: Extracting #1: cost 65 inf + 0 4.007 * * [simplify]: Extracting #2: cost 241 inf + 0 4.011 * * [simplify]: Extracting #3: cost 260 inf + 43096 4.031 * * [simplify]: Extracting #4: cost 122 inf + 266467 4.069 * * [simplify]: Extracting #5: cost 18 inf + 464771 4.112 * * [simplify]: Extracting #6: cost 0 inf + 502437 4.158 * * [simplify]: Extracting #7: cost 0 inf + 501277 4.202 * [simplify]: Simplified to (/.p16 (*.p16 (real->posit16 1) (real->posit16 1)) (-.p16 (*.p16 x x) (*.p16 (real->posit16 1) (real->posit16 1)))) 4.203 * [simplify]: Simplified (2 2 2) to (λ (x) (+.p16 (-.p16 (/.p16 (real->posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (real->posit16 2) x)) (+.p16 (*.p16 (/.p16 (real->posit16 1) (-.p16 (*.p16 x x) (*.p16 (real->posit16 1) (real->posit16 1)))) x) (/.p16 (*.p16 (real->posit16 1) (real->posit16 1)) (-.p16 (*.p16 x x) (*.p16 (real->posit16 1) (real->posit16 1))))))) 4.203 * * * * [progress]: [ 7 / 18 ] simplifiying candidate #posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (real->posit16 2) x)) (+.p16 (*.p16 x (/.p16 (real->posit16 1) (-.p16 (*.p16 x x) (*.p16 (real->posit16 1) (real->posit16 1))))) (*.p16 (real->posit16 1) (/.p16 (real->posit16 1) (-.p16 (*.p16 x x) (*.p16 (real->posit16 1) (real->posit16 1))))))))> 4.203 * [simplify]: Simplifying (*.p16 (real->posit16 1) (/.p16 (real->posit16 1) (-.p16 (*.p16 x x) (*.p16 (real->posit16 1) (real->posit16 1))))) 4.203 * * [simplify]: iters left: 5 (8 enodes) 4.208 * * [simplify]: iters left: 4 (25 enodes) 4.217 * * [simplify]: iters left: 3 (62 enodes) 4.244 * * [simplify]: iters left: 2 (193 enodes) 4.319 * * [simplify]: Extracting #0: cost 1 inf + 0 4.319 * * [simplify]: Extracting #1: cost 65 inf + 0 4.320 * * [simplify]: Extracting #2: cost 241 inf + 0 4.322 * * [simplify]: Extracting #3: cost 260 inf + 43096 4.331 * * [simplify]: Extracting #4: cost 122 inf + 266467 4.354 * * [simplify]: Extracting #5: cost 18 inf + 464771 4.375 * * [simplify]: Extracting #6: cost 0 inf + 502437 4.401 * * [simplify]: Extracting #7: cost 0 inf + 501277 4.422 * [simplify]: Simplified to (/.p16 (*.p16 (real->posit16 1) (real->posit16 1)) (-.p16 (*.p16 x x) (*.p16 (real->posit16 1) (real->posit16 1)))) 4.422 * [simplify]: Simplified (2 2 2) to (λ (x) (+.p16 (-.p16 (/.p16 (real->posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (real->posit16 2) x)) (+.p16 (*.p16 x (/.p16 (real->posit16 1) (-.p16 (*.p16 x x) (*.p16 (real->posit16 1) (real->posit16 1))))) (/.p16 (*.p16 (real->posit16 1) (real->posit16 1)) (-.p16 (*.p16 x x) (*.p16 (real->posit16 1) (real->posit16 1))))))) 4.422 * * * * [progress]: [ 8 / 18 ] simplifiying candidate #posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (real->posit16 2) x)) (*.p16 (/.p16 (real->posit16 1) (-.p16 (*.p16 (*.p16 x x) (*.p16 x x)) (*.p16 (*.p16 (real->posit16 1) (real->posit16 1)) (*.p16 (real->posit16 1) (real->posit16 1))))) (*.p16 (+.p16 (*.p16 x x) (*.p16 (real->posit16 1) (real->posit16 1))) (+.p16 x (real->posit16 1))))))> 4.423 * [simplify]: Simplifying (/.p16 (real->posit16 1) (-.p16 (*.p16 (*.p16 x x) (*.p16 x x)) (*.p16 (*.p16 (real->posit16 1) (real->posit16 1)) (*.p16 (real->posit16 1) (real->posit16 1))))) 4.423 * * [simplify]: iters left: 5 (9 enodes) 4.426 * * [simplify]: iters left: 4 (32 enodes) 4.434 * * [simplify]: iters left: 3 (76 enodes) 4.459 * * [simplify]: iters left: 2 (239 enodes) 4.552 * * [simplify]: Extracting #0: cost 1 inf + 0 4.552 * * [simplify]: Extracting #1: cost 46 inf + 0 4.553 * * [simplify]: Extracting #2: cost 215 inf + 0 4.557 * * [simplify]: Extracting #3: cost 259 inf + 37842 4.580 * * [simplify]: Extracting #4: cost 141 inf + 336186 4.625 * * [simplify]: Extracting #5: cost 28 inf + 595296 4.671 * * [simplify]: Extracting #6: cost 1 inf + 655569 4.704 * * [simplify]: Extracting #7: cost 0 inf + 659011 4.754 * [simplify]: Simplified to (/.p16 (real->posit16 1) (-.p16 (*.p16 (*.p16 x x) (*.p16 x x)) (*.p16 (*.p16 (real->posit16 1) (real->posit16 1)) (*.p16 (real->posit16 1) (real->posit16 1))))) 4.754 * [simplify]: Simplified (2 2 1) to (λ (x) (+.p16 (-.p16 (/.p16 (real->posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (real->posit16 2) x)) (*.p16 (/.p16 (real->posit16 1) (-.p16 (*.p16 (*.p16 x x) (*.p16 x x)) (*.p16 (*.p16 (real->posit16 1) (real->posit16 1)) (*.p16 (real->posit16 1) (real->posit16 1))))) (*.p16 (+.p16 (*.p16 x x) (*.p16 (real->posit16 1) (real->posit16 1))) (+.p16 x (real->posit16 1)))))) 4.754 * * * * [progress]: [ 9 / 18 ] 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 x) (*.p16 (real->posit16 1) (real->posit16 1))))))> 4.755 * [simplify]: Simplifying (*.p16 (real->posit16 1) (+.p16 x (real->posit16 1))) 4.755 * * [simplify]: iters left: 3 (5 enodes) 4.757 * * [simplify]: iters left: 2 (17 enodes) 4.760 * * [simplify]: iters left: 1 (21 enodes) 4.763 * * [simplify]: Extracting #0: cost 1 inf + 0 4.763 * * [simplify]: Extracting #1: cost 5 inf + 0 4.763 * * [simplify]: Extracting #2: cost 7 inf + 0 4.763 * * [simplify]: Extracting #3: cost 5 inf + 2 4.763 * * [simplify]: Extracting #4: cost 0 inf + 1050 4.763 * [simplify]: Simplified to (*.p16 (real->posit16 1) (+.p16 (real->posit16 1) x)) 4.763 * [simplify]: Simplified (2 2 1) to (λ (x) (+.p16 (-.p16 (/.p16 (real->posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (real->posit16 2) x)) (/.p16 (*.p16 (real->posit16 1) (+.p16 (real->posit16 1) x)) (-.p16 (*.p16 x x) (*.p16 (real->posit16 1) (real->posit16 1)))))) 4.763 * * * * [progress]: [ 10 / 18 ] 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 x) (*.p16 (real->posit16 1) (real->posit16 1)))))))> 4.763 * * * * [progress]: [ 11 / 18 ] simplifiying candidate #posit16 1) (+.p16 x (real->posit16 1))) (neg.p16 (/.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)))))> 4.763 * * * * [progress]: [ 12 / 18 ] 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 x) (*.p16 (real->posit16 1) (real->posit16 1)))) (+.p16 x (real->posit16 1)))))> 4.763 * * * * [progress]: [ 13 / 18 ] simplifiying candidate #posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (real->posit16 2) x)) (*.p16 (/.p16 (/.p16 (real->posit16 1) (+.p16 x (real->posit16 1))) (-.p16 x (real->posit16 1))) (+.p16 x (real->posit16 1)))))> 4.763 * [simplify]: Simplifying (-.p16 x (real->posit16 1)) 4.763 * * [simplify]: iters left: 2 (4 enodes) 4.764 * * [simplify]: iters left: 1 (16 enodes) 4.767 * * [simplify]: Extracting #0: cost 1 inf + 0 4.767 * * [simplify]: Extracting #1: cost 6 inf + 0 4.767 * * [simplify]: Extracting #2: cost 11 inf + 1 4.768 * * [simplify]: Extracting #3: cost 11 inf + 323 4.768 * * [simplify]: Extracting #4: cost 5 inf + 1491 4.768 * * [simplify]: Extracting #5: cost 1 inf + 3657 4.768 * * [simplify]: Extracting #6: cost 0 inf + 5019 4.768 * [simplify]: Simplified to (-.p16 x (real->posit16 1)) 4.768 * [simplify]: Simplified (2 2 1 2) to (λ (x) (+.p16 (-.p16 (/.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 x (real->posit16 1))) (+.p16 x (real->posit16 1))))) 4.768 * * * * [progress]: [ 14 / 18 ] simplifiying candidate #posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (real->posit16 2) x)) (*.p16 (*.p16 (/.p16 (real->posit16 1) (-.p16 (*.p16 (*.p16 x x) (*.p16 x x)) (*.p16 (*.p16 (real->posit16 1) (real->posit16 1)) (*.p16 (real->posit16 1) (real->posit16 1))))) (+.p16 (*.p16 x x) (*.p16 (real->posit16 1) (real->posit16 1)))) (+.p16 x (real->posit16 1)))))> 4.768 * [simplify]: Simplifying (+.p16 (*.p16 x x) (*.p16 (real->posit16 1) (real->posit16 1))) 4.769 * * [simplify]: iters left: 3 (6 enodes) 4.770 * * [simplify]: iters left: 2 (12 enodes) 4.772 * * [simplify]: iters left: 1 (14 enodes) 4.774 * * [simplify]: Extracting #0: cost 1 inf + 0 4.774 * * [simplify]: Extracting #1: cost 3 inf + 0 4.775 * * [simplify]: Extracting #2: cost 5 inf + 0 4.775 * * [simplify]: Extracting #3: cost 5 inf + 1 4.775 * * [simplify]: Extracting #4: cost 0 inf + 1327 4.775 * [simplify]: Simplified to (+.p16 (*.p16 (real->posit16 1) (real->posit16 1)) (*.p16 x x)) 4.775 * [simplify]: Simplified (2 2 1 2) to (λ (x) (+.p16 (-.p16 (/.p16 (real->posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (real->posit16 2) x)) (*.p16 (*.p16 (/.p16 (real->posit16 1) (-.p16 (*.p16 (*.p16 x x) (*.p16 x x)) (*.p16 (*.p16 (real->posit16 1) (real->posit16 1)) (*.p16 (real->posit16 1) (real->posit16 1))))) (+.p16 (*.p16 (real->posit16 1) (real->posit16 1)) (*.p16 x x))) (+.p16 x (real->posit16 1))))) 4.775 * * * * [progress]: [ 15 / 18 ] 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)))))> 4.775 * [simplify]: Simplifying (+.p16 x (real->posit16 1)) 4.775 * * [simplify]: iters left: 2 (4 enodes) 4.776 * * [simplify]: iters left: 1 (10 enodes) 4.778 * * [simplify]: Extracting #0: cost 1 inf + 0 4.778 * * [simplify]: Extracting #1: cost 3 inf + 0 4.778 * * [simplify]: Extracting #2: cost 3 inf + 1 4.778 * * [simplify]: Extracting #3: cost 0 inf + 45 4.778 * [simplify]: Simplified to (+.p16 (real->posit16 1) x) 4.778 * [simplify]: Simplified (2 2 2) to (λ (x) (+.p16 (-.p16 (/.p16 (real->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 (real->posit16 1) x)))) 4.778 * * * * [progress]: [ 16 / 18 ] 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)))))> 4.778 * [simplify]: Simplifying (+.p16 x (real->posit16 1)) 4.778 * * [simplify]: iters left: 2 (4 enodes) 4.779 * * [simplify]: iters left: 1 (10 enodes) 4.781 * * [simplify]: Extracting #0: cost 1 inf + 0 4.781 * * [simplify]: Extracting #1: cost 3 inf + 0 4.781 * * [simplify]: Extracting #2: cost 3 inf + 1 4.781 * * [simplify]: Extracting #3: cost 0 inf + 45 4.781 * [simplify]: Simplified to (+.p16 (real->posit16 1) x) 4.781 * [simplify]: Simplified (2 2 2) to (λ (x) (+.p16 (-.p16 (/.p16 (real->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 (real->posit16 1) x)))) 4.781 * * * * [progress]: [ 17 / 18 ] 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)))))> 4.782 * [simplify]: Simplifying (+.p16 x (real->posit16 1)) 4.782 * * [simplify]: iters left: 2 (4 enodes) 4.783 * * [simplify]: iters left: 1 (10 enodes) 4.784 * * [simplify]: Extracting #0: cost 1 inf + 0 4.784 * * [simplify]: Extracting #1: cost 3 inf + 0 4.784 * * [simplify]: Extracting #2: cost 3 inf + 1 4.785 * * [simplify]: Extracting #3: cost 0 inf + 45 4.785 * [simplify]: Simplified to (+.p16 (real->posit16 1) x) 4.785 * [simplify]: Simplified (2 2 2) to (λ (x) (+.p16 (-.p16 (/.p16 (real->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 (real->posit16 1) x)))) 4.785 * * * * [progress]: [ 18 / 18 ] 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)))))> 4.785 * [simplify]: Simplifying (+.p16 x (real->posit16 1)) 4.785 * * [simplify]: iters left: 2 (4 enodes) 4.786 * * [simplify]: iters left: 1 (10 enodes) 4.788 * * [simplify]: Extracting #0: cost 1 inf + 0 4.788 * * [simplify]: Extracting #1: cost 3 inf + 0 4.788 * * [simplify]: Extracting #2: cost 3 inf + 1 4.788 * * [simplify]: Extracting #3: cost 0 inf + 45 4.788 * [simplify]: Simplified to (+.p16 (real->posit16 1) x) 4.788 * [simplify]: Simplified (2 2 2) to (λ (x) (+.p16 (-.p16 (/.p16 (real->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 (real->posit16 1) x)))) 4.788 * * * [progress]: adding candidates to table 5.471 * * [progress]: iteration 4 / 4 5.471 * * * [progress]: picking best candidate 5.554 * * * * [pick]: Picked #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 x) (*.p16 (real->posit16 1) (real->posit16 1))))))> 5.554 * * * [progress]: localizing error 5.956 * * * [progress]: generating rewritten candidates 5.956 * * * * [progress]: [ 1 / 4 ] rewriting at (2) 5.969 * * * * [progress]: [ 2 / 4 ] rewriting at (2 2) 5.972 * * * * [progress]: [ 3 / 4 ] rewriting at (2 1) 5.975 * * * * [progress]: [ 4 / 4 ] rewriting at (2 2 2) 5.977 * * * [progress]: generating series expansions 5.977 * * * * [progress]: [ 1 / 4 ] generating series at (2) 5.977 * * * * [progress]: [ 2 / 4 ] generating series at (2 2) 5.978 * * * * [progress]: [ 3 / 4 ] generating series at (2 1) 5.978 * * * * [progress]: [ 4 / 4 ] generating series at (2 2 2) 5.978 * * * [progress]: simplifying candidates 5.978 * * * * [progress]: [ 1 / 16 ] simplifiying candidate #posit16 1) (+.p16 x (real->posit16 1))) (+.p16 (neg.p16 (/.p16 (real->posit16 2) x)) (/.p16 (*.p16 (real->posit16 1) (+.p16 x (real->posit16 1))) (-.p16 (*.p16 x x) (*.p16 (real->posit16 1) (real->posit16 1)))))))> 5.978 * [simplify]: Simplifying (/.p16 (real->posit16 1) (+.p16 x (real->posit16 1))) 5.978 * * [simplify]: iters left: 3 (5 enodes) 5.979 * * [simplify]: iters left: 2 (11 enodes) 5.989 * * [simplify]: iters left: 1 (13 enodes) 5.992 * * [simplify]: Extracting #0: cost 1 inf + 0 5.992 * * [simplify]: Extracting #1: cost 3 inf + 0 5.992 * * [simplify]: Extracting #2: cost 5 inf + 0 5.992 * * [simplify]: Extracting #3: cost 3 inf + 2 5.992 * * [simplify]: Extracting #4: cost 0 inf + 527 5.992 * [simplify]: Simplified to (/.p16 (real->posit16 1) (+.p16 (real->posit16 1) x)) 5.992 * [simplify]: Simplified (2 1) to (λ (x) (+.p16 (/.p16 (real->posit16 1) (+.p16 (real->posit16 1) x)) (+.p16 (neg.p16 (/.p16 (real->posit16 2) x)) (/.p16 (*.p16 (real->posit16 1) (+.p16 x (real->posit16 1))) (-.p16 (*.p16 x x) (*.p16 (real->posit16 1) (real->posit16 1))))))) 5.992 * * * * [progress]: [ 2 / 16 ] simplifiying candidate #posit16 1) (+.p16 x (real->posit16 1))) (-.p16 (/.p16 (real->posit16 2) x) (/.p16 (*.p16 (real->posit16 1) (+.p16 x (real->posit16 1))) (-.p16 (*.p16 x x) (*.p16 (real->posit16 1) (real->posit16 1)))))))> 5.992 * [simplify]: Simplifying (/.p16 (real->posit16 1) (+.p16 x (real->posit16 1))) 5.992 * * [simplify]: iters left: 3 (5 enodes) 5.994 * * [simplify]: iters left: 2 (11 enodes) 5.996 * * [simplify]: iters left: 1 (13 enodes) 5.998 * * [simplify]: Extracting #0: cost 1 inf + 0 5.998 * * [simplify]: Extracting #1: cost 3 inf + 0 5.998 * * [simplify]: Extracting #2: cost 5 inf + 0 5.998 * * [simplify]: Extracting #3: cost 3 inf + 2 5.998 * * [simplify]: Extracting #4: cost 0 inf + 527 5.998 * [simplify]: Simplified to (/.p16 (real->posit16 1) (+.p16 (real->posit16 1) x)) 5.998 * [simplify]: Simplified (2 1) to (λ (x) (-.p16 (/.p16 (real->posit16 1) (+.p16 (real->posit16 1) x)) (-.p16 (/.p16 (real->posit16 2) x) (/.p16 (*.p16 (real->posit16 1) (+.p16 x (real->posit16 1))) (-.p16 (*.p16 x x) (*.p16 (real->posit16 1) (real->posit16 1))))))) 5.998 * * * * [progress]: [ 3 / 16 ] simplifiying candidate #posit16 1) (+.p16 x (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 2) x))))> 5.998 * * * * [progress]: [ 4 / 16 ] simplifiying candidate #posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (real->posit16 2) x)) (/.p16 (/.p16 (*.p16 (real->posit16 1) (+.p16 x (real->posit16 1))) (+.p16 x (real->posit16 1))) (-.p16 x (real->posit16 1)))))> 5.999 * [simplify]: Simplifying (-.p16 x (real->posit16 1)) 5.999 * * [simplify]: iters left: 2 (4 enodes) 6.000 * * [simplify]: iters left: 1 (16 enodes) 6.003 * * [simplify]: Extracting #0: cost 1 inf + 0 6.003 * * [simplify]: Extracting #1: cost 6 inf + 0 6.003 * * [simplify]: Extracting #2: cost 11 inf + 1 6.003 * * [simplify]: Extracting #3: cost 11 inf + 323 6.003 * * [simplify]: Extracting #4: cost 5 inf + 1491 6.003 * * [simplify]: Extracting #5: cost 1 inf + 3657 6.003 * * [simplify]: Extracting #6: cost 0 inf + 5019 6.003 * [simplify]: Simplified to (-.p16 x (real->posit16 1)) 6.003 * [simplify]: Simplified (2 2 2) to (λ (x) (+.p16 (-.p16 (/.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 x (real->posit16 1))) (-.p16 x (real->posit16 1))))) 6.003 * * * * [progress]: [ 5 / 16 ] simplifiying candidate #posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (real->posit16 2) x)) (/.p16 (real->posit16 1) (/.p16 (-.p16 (*.p16 x x) (*.p16 (real->posit16 1) (real->posit16 1))) (+.p16 x (real->posit16 1))))))> 6.004 * [simplify]: Simplifying (real->posit16 1) 6.004 * * [simplify]: iters left: 1 (2 enodes) 6.004 * * [simplify]: Extracting #0: cost 1 inf + 0 6.004 * * [simplify]: Extracting #1: cost 2 inf + 0 6.004 * * [simplify]: Extracting #2: cost 1 inf + 1 6.004 * * [simplify]: Extracting #3: cost 0 inf + 2 6.004 * [simplify]: Simplified to (real->posit16 1) 6.004 * [simplify]: Simplified (2 2 1) to (λ (x) (+.p16 (-.p16 (/.p16 (real->posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (real->posit16 2) x)) (/.p16 (real->posit16 1) (/.p16 (-.p16 (*.p16 x x) (*.p16 (real->posit16 1) (real->posit16 1))) (+.p16 x (real->posit16 1)))))) 6.005 * * * * [progress]: [ 6 / 16 ] simplifiying candidate #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 (*.p16 x x) (*.p16 x x)) (*.p16 (*.p16 (real->posit16 1) (real->posit16 1)) (*.p16 (real->posit16 1) (real->posit16 1))))) (+.p16 (*.p16 x x) (*.p16 (real->posit16 1) (real->posit16 1))))))> 6.005 * [simplify]: Simplifying (+.p16 (*.p16 x x) (*.p16 (real->posit16 1) (real->posit16 1))) 6.005 * * [simplify]: iters left: 3 (6 enodes) 6.006 * * [simplify]: iters left: 2 (12 enodes) 6.008 * * [simplify]: iters left: 1 (14 enodes) 6.010 * * [simplify]: Extracting #0: cost 1 inf + 0 6.010 * * [simplify]: Extracting #1: cost 3 inf + 0 6.010 * * [simplify]: Extracting #2: cost 5 inf + 0 6.011 * * [simplify]: Extracting #3: cost 5 inf + 1 6.011 * * [simplify]: Extracting #4: cost 0 inf + 1327 6.011 * [simplify]: Simplified to (+.p16 (*.p16 (real->posit16 1) (real->posit16 1)) (*.p16 x x)) 6.011 * [simplify]: Simplified (2 2 2) to (λ (x) (+.p16 (-.p16 (/.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 (*.p16 x x) (*.p16 x x)) (*.p16 (*.p16 (real->posit16 1) (real->posit16 1)) (*.p16 (real->posit16 1) (real->posit16 1))))) (+.p16 (*.p16 (real->posit16 1) (real->posit16 1)) (*.p16 x x))))) 6.011 * * * * [progress]: [ 7 / 16 ] 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))))))> 6.011 * [simplify]: Simplifying (/.p16 (real->posit16 1) (+.p16 x (real->posit16 1))) 6.011 * * [simplify]: iters left: 3 (5 enodes) 6.012 * * [simplify]: iters left: 2 (11 enodes) 6.014 * * [simplify]: iters left: 1 (13 enodes) 6.016 * * [simplify]: Extracting #0: cost 1 inf + 0 6.016 * * [simplify]: Extracting #1: cost 3 inf + 0 6.016 * * [simplify]: Extracting #2: cost 5 inf + 0 6.016 * * [simplify]: Extracting #3: cost 3 inf + 2 6.016 * * [simplify]: Extracting #4: cost 0 inf + 527 6.016 * [simplify]: Simplified to (/.p16 (real->posit16 1) (+.p16 (real->posit16 1) x)) 6.016 * [simplify]: Simplified (2 2 1) to (λ (x) (+.p16 (-.p16 (/.p16 (real->posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (real->posit16 2) x)) (*.p16 (/.p16 (real->posit16 1) (+.p16 (real->posit16 1) x)) (/.p16 (+.p16 x (real->posit16 1)) (-.p16 x (real->posit16 1)))))) 6.016 * [simplify]: Simplifying (/.p16 (+.p16 x (real->posit16 1)) (-.p16 x (real->posit16 1))) 6.016 * * [simplify]: iters left: 3 (6 enodes) 6.018 * * [simplify]: iters left: 2 (18 enodes) 6.021 * * [simplify]: iters left: 1 (31 enodes) 6.027 * * [simplify]: Extracting #0: cost 1 inf + 0 6.027 * * [simplify]: Extracting #1: cost 10 inf + 0 6.027 * * [simplify]: Extracting #2: cost 26 inf + 0 6.027 * * [simplify]: Extracting #3: cost 31 inf + 1 6.027 * * [simplify]: Extracting #4: cost 35 inf + 323 6.027 * * [simplify]: Extracting #5: cost 17 inf + 8069 6.028 * * [simplify]: Extracting #6: cost 0 inf + 25900 6.029 * [simplify]: Simplified to (/.p16 (+.p16 (real->posit16 1) x) (-.p16 x (real->posit16 1))) 6.029 * [simplify]: Simplified (2 2 2) to (λ (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 (+.p16 (real->posit16 1) x) (-.p16 x (real->posit16 1)))))) 6.029 * * * * [progress]: [ 8 / 16 ] simplifiying candidate #posit16 1) (+.p16 x (real->posit16 1))) (neg.p16 (/.p16 (real->posit16 2) x))) (/.p16 (*.p16 (real->posit16 1) (+.p16 x (real->posit16 1))) (-.p16 (*.p16 x x) (*.p16 (real->posit16 1) (real->posit16 1))))))> 6.029 * * * * [progress]: [ 9 / 16 ] 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 x (real->posit16 1))) (-.p16 (*.p16 x x) (*.p16 (real->posit16 1) (real->posit16 1))))))> 6.030 * * * * [progress]: [ 10 / 16 ] 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))))))> 6.030 * [simplify]: Simplifying (+.p16 x (real->posit16 1)) 6.030 * * [simplify]: iters left: 2 (4 enodes) 6.031 * * [simplify]: iters left: 1 (10 enodes) 6.033 * * [simplify]: Extracting #0: cost 1 inf + 0 6.033 * * [simplify]: Extracting #1: cost 3 inf + 0 6.033 * * [simplify]: Extracting #2: cost 3 inf + 1 6.033 * * [simplify]: Extracting #3: cost 0 inf + 45 6.033 * [simplify]: Simplified to (+.p16 (real->posit16 1) x) 6.033 * [simplify]: Simplified (2 2 2 1) to (λ (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 (+.p16 (real->posit16 1) x) (-.p16 x (real->posit16 1)))))) 6.033 * [simplify]: Simplifying (-.p16 x (real->posit16 1)) 6.033 * * [simplify]: iters left: 2 (4 enodes) 6.034 * * [simplify]: iters left: 1 (16 enodes) 6.037 * * [simplify]: Extracting #0: cost 1 inf + 0 6.037 * * [simplify]: Extracting #1: cost 6 inf + 0 6.037 * * [simplify]: Extracting #2: cost 11 inf + 1 6.037 * * [simplify]: Extracting #3: cost 11 inf + 323 6.037 * * [simplify]: Extracting #4: cost 5 inf + 1491 6.037 * * [simplify]: Extracting #5: cost 1 inf + 3657 6.037 * * [simplify]: Extracting #6: cost 0 inf + 5019 6.038 * [simplify]: Simplified to (-.p16 x (real->posit16 1)) 6.038 * [simplify]: Simplified (2 2 2 2) to (λ (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 (+.p16 x (real->posit16 1)) (-.p16 x (real->posit16 1)))))) 6.038 * * * * [progress]: [ 11 / 16 ] 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 x) (neg.p16 (*.p16 (real->posit16 1) (real->posit16 1)))))))> 6.038 * * * * [progress]: [ 12 / 16 ] 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 (*.p16 (*.p16 x x) (*.p16 x x)) (*.p16 (*.p16 (real->posit16 1) (real->posit16 1)) (*.p16 (real->posit16 1) (real->posit16 1)))) (+.p16 (*.p16 x x) (*.p16 (real->posit16 1) (real->posit16 1)))))))> 6.038 * * * * [progress]: [ 13 / 16 ] 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 x) (*.p16 (real->posit16 1) (real->posit16 1))))))> 6.038 * [simplify]: Simplifying (*.p16 (real->posit16 1) (+.p16 x (real->posit16 1))) 6.038 * * [simplify]: iters left: 3 (5 enodes) 6.040 * * [simplify]: iters left: 2 (17 enodes) 6.043 * * [simplify]: iters left: 1 (21 enodes) 6.047 * * [simplify]: Extracting #0: cost 1 inf + 0 6.047 * * [simplify]: Extracting #1: cost 5 inf + 0 6.047 * * [simplify]: Extracting #2: cost 7 inf + 0 6.047 * * [simplify]: Extracting #3: cost 5 inf + 2 6.047 * * [simplify]: Extracting #4: cost 0 inf + 1050 6.047 * [simplify]: Simplified to (*.p16 (real->posit16 1) (+.p16 (real->posit16 1) x)) 6.047 * [simplify]: Simplified (2 2 1) to (λ (x) (+.p16 (-.p16 (/.p16 (real->posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (real->posit16 2) x)) (/.p16 (*.p16 (real->posit16 1) (+.p16 (real->posit16 1) x)) (-.p16 (*.p16 x x) (*.p16 (real->posit16 1) (real->posit16 1)))))) 6.047 * * * * [progress]: [ 14 / 16 ] 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 x) (*.p16 (real->posit16 1) (real->posit16 1))))))> 6.048 * [simplify]: Simplifying (*.p16 (real->posit16 1) (+.p16 x (real->posit16 1))) 6.048 * * [simplify]: iters left: 3 (5 enodes) 6.049 * * [simplify]: iters left: 2 (17 enodes) 6.052 * * [simplify]: iters left: 1 (21 enodes) 6.055 * * [simplify]: Extracting #0: cost 1 inf + 0 6.055 * * [simplify]: Extracting #1: cost 5 inf + 0 6.055 * * [simplify]: Extracting #2: cost 7 inf + 0 6.055 * * [simplify]: Extracting #3: cost 5 inf + 2 6.055 * * [simplify]: Extracting #4: cost 0 inf + 1050 6.055 * [simplify]: Simplified to (*.p16 (real->posit16 1) (+.p16 (real->posit16 1) x)) 6.055 * [simplify]: Simplified (2 2 1) to (λ (x) (+.p16 (-.p16 (/.p16 (real->posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (real->posit16 2) x)) (/.p16 (*.p16 (real->posit16 1) (+.p16 (real->posit16 1) x)) (-.p16 (*.p16 x x) (*.p16 (real->posit16 1) (real->posit16 1)))))) 6.055 * * * * [progress]: [ 15 / 16 ] 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 x) (*.p16 (real->posit16 1) (real->posit16 1))))))> 6.055 * [simplify]: Simplifying (*.p16 (real->posit16 1) (+.p16 x (real->posit16 1))) 6.055 * * [simplify]: iters left: 3 (5 enodes) 6.057 * * [simplify]: iters left: 2 (17 enodes) 6.060 * * [simplify]: iters left: 1 (21 enodes) 6.063 * * [simplify]: Extracting #0: cost 1 inf + 0 6.063 * * [simplify]: Extracting #1: cost 5 inf + 0 6.063 * * [simplify]: Extracting #2: cost 7 inf + 0 6.063 * * [simplify]: Extracting #3: cost 5 inf + 2 6.063 * * [simplify]: Extracting #4: cost 0 inf + 1050 6.063 * [simplify]: Simplified to (*.p16 (real->posit16 1) (+.p16 (real->posit16 1) x)) 6.063 * [simplify]: Simplified (2 2 1) to (λ (x) (+.p16 (-.p16 (/.p16 (real->posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (real->posit16 2) x)) (/.p16 (*.p16 (real->posit16 1) (+.p16 (real->posit16 1) x)) (-.p16 (*.p16 x x) (*.p16 (real->posit16 1) (real->posit16 1)))))) 6.063 * * * * [progress]: [ 16 / 16 ] 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 x) (*.p16 (real->posit16 1) (real->posit16 1))))))> 6.063 * [simplify]: Simplifying (*.p16 (real->posit16 1) (+.p16 x (real->posit16 1))) 6.063 * * [simplify]: iters left: 3 (5 enodes) 6.065 * * [simplify]: iters left: 2 (17 enodes) 6.068 * * [simplify]: iters left: 1 (21 enodes) 6.070 * * [simplify]: Extracting #0: cost 1 inf + 0 6.070 * * [simplify]: Extracting #1: cost 5 inf + 0 6.070 * * [simplify]: Extracting #2: cost 7 inf + 0 6.071 * * [simplify]: Extracting #3: cost 5 inf + 2 6.071 * * [simplify]: Extracting #4: cost 0 inf + 1050 6.071 * [simplify]: Simplified to (*.p16 (real->posit16 1) (+.p16 (real->posit16 1) x)) 6.071 * [simplify]: Simplified (2 2 1) to (λ (x) (+.p16 (-.p16 (/.p16 (real->posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (real->posit16 2) x)) (/.p16 (*.p16 (real->posit16 1) (+.p16 (real->posit16 1) x)) (-.p16 (*.p16 x x) (*.p16 (real->posit16 1) (real->posit16 1)))))) 6.071 * * * [progress]: adding candidates to table 6.519 * [progress]: [Phase 3 of 3] Extracting. 6.519 * * [regime]: Finding splitpoints for: (#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 (/.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)))))> #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 (*.p16 x x) (*.p16 x x)) (*.p16 (*.p16 (real->posit16 1) (real->posit16 1)) (*.p16 (real->posit16 1) (real->posit16 1))))) (+.p16 (*.p16 x x) (*.p16 (real->posit16 1) (real->posit16 1))))))> #posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (real->posit16 2) x)) (*.p16 (/.p16 (/.p16 (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 (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 (/.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 x) (*.p16 (real->posit16 1) (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 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 x (real->posit16 1))) (-.p16 (*.p16 x x) (*.p16 (real->posit16 1) (real->posit16 1))))))> #posit16 1) (+.p16 x (real->posit16 1))) (+.p16 (neg.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 x) (*.p16 (real->posit16 1) (real->posit16 1)))) x)) (*.p16 (/.p16 (real->posit16 1) (-.p16 (*.p16 x x) (*.p16 (real->posit16 1) (real->posit16 1)))) (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 x) (*.p16 (real->posit16 1) (real->posit16 1))))))>) 6.521 * * * [regime-changes]: Trying 1 branch expressions: (x) 6.521 * * * * [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 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 (/.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)))))> #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 (*.p16 x x) (*.p16 x x)) (*.p16 (*.p16 (real->posit16 1) (real->posit16 1)) (*.p16 (real->posit16 1) (real->posit16 1))))) (+.p16 (*.p16 x x) (*.p16 (real->posit16 1) (real->posit16 1))))))> #posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (real->posit16 2) x)) (*.p16 (/.p16 (/.p16 (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 (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 (/.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 x) (*.p16 (real->posit16 1) (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 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 x (real->posit16 1))) (-.p16 (*.p16 x x) (*.p16 (real->posit16 1) (real->posit16 1))))))> #posit16 1) (+.p16 x (real->posit16 1))) (+.p16 (neg.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 x) (*.p16 (real->posit16 1) (real->posit16 1)))) x)) (*.p16 (/.p16 (real->posit16 1) (-.p16 (*.p16 x x) (*.p16 (real->posit16 1) (real->posit16 1)))) (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 x) (*.p16 (real->posit16 1) (real->posit16 1))))))>) 6.711 * * * [regime]: Found split indices: #