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.006 * * * * [points]: Setting MPFR precision to 64 0.007 * * * * [points]: Setting MPFR precision to 320 0.009 * * * * [points]: Computing exacts on every 8 of 256 points to ramp up precision 0.012 * * * * [points]: Setting MPFR precision to 64 0.015 * * * * [points]: Setting MPFR precision to 320 0.017 * * * * [points]: Computing exacts on every 4 of 256 points to ramp up precision 0.021 * * * * [points]: Setting MPFR precision to 64 0.025 * * * * [points]: Setting MPFR precision to 320 0.027 * * * * [points]: Computing exacts on every 2 of 256 points to ramp up precision 0.030 * * * * [points]: Setting MPFR precision to 64 0.034 * * * * [points]: Setting MPFR precision to 320 0.038 * * * * [points]: Computing exacts for 256 points 0.041 * * * * [points]: Setting MPFR precision to 64 0.053 * * * * [points]: Setting MPFR precision to 320 0.069 * * * * [points]: Filtering points with unrepresentable outputs 0.069 * * * * [points]: Sampled 256 points with exact outputs 0.069 * * * [progress]: [2/2] Setting up program. 0.082 * [progress]: [Phase 2 of 3] Improving. 0.082 * * * * [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.082 * [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.082 * * [simplify]: iters left: 5 (12 enodes) 0.085 * * [simplify]: iters left: 4 (35 enodes) 0.093 * * [simplify]: iters left: 3 (83 enodes) 0.141 * * [simplify]: iters left: 2 (233 enodes) 0.216 * * [simplify]: Extracting #0: cost 1 inf + 0 0.216 * * [simplify]: Extracting #1: cost 29 inf + 0 0.216 * * [simplify]: Extracting #2: cost 123 inf + 0 0.217 * * [simplify]: Extracting #3: cost 244 inf + 1 0.219 * * [simplify]: Extracting #4: cost 308 inf + 32857 0.230 * * [simplify]: Extracting #5: cost 149 inf + 308686 0.252 * * [simplify]: Extracting #6: cost 4 inf + 549893 0.278 * * [simplify]: Extracting #7: cost 0 inf + 561504 0.306 * [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.306 * [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.320 * * [progress]: iteration 1 / 4 0.321 * * * [progress]: picking best candidate 0.336 * * * * [pick]: Picked #posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (real->posit16 2) x)) (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1)))))> 0.336 * * * [progress]: localizing error 0.501 * * * [progress]: generating rewritten candidates 0.501 * * * * [progress]: [ 1 / 4 ] rewriting at (2) 0.513 * * * * [progress]: [ 2 / 4 ] rewriting at (2 1) 0.516 * * * * [progress]: [ 3 / 4 ] rewriting at (2 2) 0.518 * * * * [progress]: [ 4 / 4 ] rewriting at (2 1 1) 0.520 * * * [progress]: generating series expansions 0.520 * * * * [progress]: [ 1 / 4 ] generating series at (2) 0.520 * * * * [progress]: [ 2 / 4 ] generating series at (2 1) 0.520 * * * * [progress]: [ 3 / 4 ] generating series at (2 2) 0.520 * * * * [progress]: [ 4 / 4 ] generating series at (2 1 1) 0.520 * * * [progress]: simplifying candidates 0.520 * * * * [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.520 * [simplify]: Simplifying (/.p16 (real->posit16 1) (+.p16 x (real->posit16 1))) 0.520 * * [simplify]: iters left: 3 (5 enodes) 0.522 * * [simplify]: iters left: 2 (11 enodes) 0.524 * * [simplify]: iters left: 1 (13 enodes) 0.526 * * [simplify]: Extracting #0: cost 1 inf + 0 0.526 * * [simplify]: Extracting #1: cost 3 inf + 0 0.526 * * [simplify]: Extracting #2: cost 5 inf + 0 0.527 * * [simplify]: Extracting #3: cost 3 inf + 2 0.527 * * [simplify]: Extracting #4: cost 0 inf + 527 0.527 * [simplify]: Simplified to (/.p16 (real->posit16 1) (+.p16 (real->posit16 1) x)) 0.527 * [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.527 * * * * [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.527 * [simplify]: Simplifying (/.p16 (real->posit16 1) (+.p16 x (real->posit16 1))) 0.527 * * [simplify]: iters left: 3 (5 enodes) 0.529 * * [simplify]: iters left: 2 (11 enodes) 0.531 * * [simplify]: iters left: 1 (13 enodes) 0.533 * * [simplify]: Extracting #0: cost 1 inf + 0 0.533 * * [simplify]: Extracting #1: cost 3 inf + 0 0.533 * * [simplify]: Extracting #2: cost 5 inf + 0 0.533 * * [simplify]: Extracting #3: cost 3 inf + 2 0.533 * * [simplify]: Extracting #4: cost 0 inf + 527 0.533 * [simplify]: Simplified to (/.p16 (real->posit16 1) (+.p16 (real->posit16 1) x)) 0.533 * [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.533 * * * * [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.533 * * * * [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.533 * * * * [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.533 * * * * [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.533 * [simplify]: Simplifying (+.p16 x (real->posit16 1)) 0.533 * * [simplify]: iters left: 2 (4 enodes) 0.535 * * [simplify]: iters left: 1 (10 enodes) 0.536 * * [simplify]: Extracting #0: cost 1 inf + 0 0.536 * * [simplify]: Extracting #1: cost 3 inf + 0 0.536 * * [simplify]: Extracting #2: cost 3 inf + 1 0.536 * * [simplify]: Extracting #3: cost 0 inf + 45 0.536 * [simplify]: Simplified to (+.p16 (real->posit16 1) x) 0.536 * [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.537 * * * * [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.540 * [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.541 * * [simplify]: iters left: 5 (12 enodes) 0.544 * * [simplify]: iters left: 4 (35 enodes) 0.551 * * [simplify]: iters left: 3 (83 enodes) 0.567 * * [simplify]: iters left: 2 (233 enodes) 0.645 * * [simplify]: Extracting #0: cost 1 inf + 0 0.645 * * [simplify]: Extracting #1: cost 29 inf + 0 0.645 * * [simplify]: Extracting #2: cost 123 inf + 0 0.646 * * [simplify]: Extracting #3: cost 244 inf + 1 0.648 * * [simplify]: Extracting #4: cost 308 inf + 32857 0.660 * * [simplify]: Extracting #5: cost 149 inf + 308686 0.681 * * [simplify]: Extracting #6: cost 4 inf + 549893 0.709 * * [simplify]: Extracting #7: cost 0 inf + 561504 0.733 * [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.733 * [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.733 * * * * [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.733 * [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.734 * * [simplify]: iters left: 5 (12 enodes) 0.737 * * [simplify]: iters left: 4 (35 enodes) 0.744 * * [simplify]: iters left: 3 (83 enodes) 0.761 * * [simplify]: iters left: 2 (233 enodes) 0.834 * * [simplify]: Extracting #0: cost 1 inf + 0 0.834 * * [simplify]: Extracting #1: cost 29 inf + 0 0.834 * * [simplify]: Extracting #2: cost 123 inf + 0 0.835 * * [simplify]: Extracting #3: cost 244 inf + 1 0.837 * * [simplify]: Extracting #4: cost 308 inf + 32857 0.850 * * [simplify]: Extracting #5: cost 149 inf + 308686 0.876 * * [simplify]: Extracting #6: cost 4 inf + 549893 0.900 * * [simplify]: Extracting #7: cost 0 inf + 561504 0.936 * [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.936 * [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.936 * * * * [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)))))> 0.936 * [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.937 * * [simplify]: iters left: 5 (12 enodes) 0.942 * * [simplify]: iters left: 4 (35 enodes) 0.953 * * [simplify]: iters left: 3 (83 enodes) 0.980 * * [simplify]: iters left: 2 (233 enodes) 1.054 * * [simplify]: Extracting #0: cost 1 inf + 0 1.054 * * [simplify]: Extracting #1: cost 29 inf + 0 1.054 * * [simplify]: Extracting #2: cost 123 inf + 0 1.055 * * [simplify]: Extracting #3: cost 244 inf + 1 1.057 * * [simplify]: Extracting #4: cost 308 inf + 32857 1.072 * * [simplify]: Extracting #5: cost 149 inf + 308686 1.103 * * [simplify]: Extracting #6: cost 4 inf + 549893 1.127 * * [simplify]: Extracting #7: cost 0 inf + 561504 1.154 * [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.154 * [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.154 * * * * [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.154 * [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.154 * * [simplify]: iters left: 5 (12 enodes) 1.158 * * [simplify]: iters left: 4 (35 enodes) 1.166 * * [simplify]: iters left: 3 (83 enodes) 1.182 * * [simplify]: iters left: 2 (233 enodes) 1.253 * * [simplify]: Extracting #0: cost 1 inf + 0 1.253 * * [simplify]: Extracting #1: cost 29 inf + 0 1.253 * * [simplify]: Extracting #2: cost 123 inf + 0 1.254 * * [simplify]: Extracting #3: cost 244 inf + 1 1.257 * * [simplify]: Extracting #4: cost 308 inf + 32857 1.269 * * [simplify]: Extracting #5: cost 149 inf + 308686 1.310 * * [simplify]: Extracting #6: cost 4 inf + 549893 1.337 * * [simplify]: Extracting #7: cost 0 inf + 561504 1.361 * [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.361 * [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.361 * * * [progress]: adding candidates to table 1.625 * * [progress]: iteration 2 / 4 1.625 * * * [progress]: picking best candidate 1.673 * * * * [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))))))> 1.673 * * * [progress]: localizing error 1.868 * * * [progress]: generating rewritten candidates 1.868 * * * * [progress]: [ 1 / 4 ] rewriting at (2) 1.874 * * * * [progress]: [ 2 / 4 ] rewriting at (2 2) 1.877 * * * * [progress]: [ 3 / 4 ] rewriting at (2 2 2) 1.879 * * * * [progress]: [ 4 / 4 ] rewriting at (2 1) 1.881 * * * [progress]: generating series expansions 1.881 * * * * [progress]: [ 1 / 4 ] generating series at (2) 1.881 * * * * [progress]: [ 2 / 4 ] generating series at (2 2) 1.881 * * * * [progress]: [ 3 / 4 ] generating series at (2 2 2) 1.881 * * * * [progress]: [ 4 / 4 ] generating series at (2 1) 1.881 * * * [progress]: simplifying candidates 1.881 * * * * [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)))))> 1.882 * [simplify]: Simplifying (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1))) 1.882 * * [simplify]: iters left: 3 (5 enodes) 1.883 * * [simplify]: iters left: 2 (17 enodes) 1.887 * * [simplify]: iters left: 1 (31 enodes) 1.894 * * [simplify]: Extracting #0: cost 1 inf + 0 1.894 * * [simplify]: Extracting #1: cost 11 inf + 0 1.894 * * [simplify]: Extracting #2: cost 28 inf + 0 1.894 * * [simplify]: Extracting #3: cost 29 inf + 324 1.894 * * [simplify]: Extracting #4: cost 22 inf + 6266 1.895 * * [simplify]: Extracting #5: cost 3 inf + 23256 1.896 * * [simplify]: Extracting #6: cost 0 inf + 26382 1.897 * * [simplify]: Extracting #7: cost 0 inf + 25822 1.898 * [simplify]: Simplified to (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1))) 1.898 * [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))))) 1.898 * * * * [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)))))> 1.898 * * * * [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)))))> 1.898 * * * * [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))))))> 1.898 * [simplify]: Simplifying (+.p16 x (real->posit16 1)) 1.898 * * [simplify]: iters left: 2 (4 enodes) 1.900 * * [simplify]: iters left: 1 (10 enodes) 1.901 * * [simplify]: Extracting #0: cost 1 inf + 0 1.901 * * [simplify]: Extracting #1: cost 3 inf + 0 1.901 * * [simplify]: Extracting #2: cost 3 inf + 1 1.901 * * [simplify]: Extracting #3: cost 0 inf + 45 1.901 * [simplify]: Simplified to (+.p16 (real->posit16 1) x) 1.901 * [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))))) 1.902 * * * * [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))))))> 1.902 * [simplify]: Simplifying (/.p16 (real->posit16 1) (+.p16 x (real->posit16 1))) 1.902 * * [simplify]: iters left: 3 (5 enodes) 1.903 * * [simplify]: iters left: 2 (11 enodes) 1.905 * * [simplify]: iters left: 1 (13 enodes) 1.907 * * [simplify]: Extracting #0: cost 1 inf + 0 1.907 * * [simplify]: Extracting #1: cost 3 inf + 0 1.907 * * [simplify]: Extracting #2: cost 5 inf + 0 1.907 * * [simplify]: Extracting #3: cost 3 inf + 2 1.908 * * [simplify]: Extracting #4: cost 0 inf + 527 1.908 * [simplify]: Simplified to (/.p16 (real->posit16 1) (+.p16 (real->posit16 1) x)) 1.908 * [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)))))) 1.908 * * * * [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))))))> 1.908 * [simplify]: Simplifying (/.p16 (real->posit16 1) (+.p16 x (real->posit16 1))) 1.908 * * [simplify]: iters left: 3 (5 enodes) 1.909 * * [simplify]: iters left: 2 (11 enodes) 1.911 * * [simplify]: iters left: 1 (13 enodes) 1.913 * * [simplify]: Extracting #0: cost 1 inf + 0 1.913 * * [simplify]: Extracting #1: cost 3 inf + 0 1.913 * * [simplify]: Extracting #2: cost 5 inf + 0 1.913 * * [simplify]: Extracting #3: cost 3 inf + 2 1.913 * * [simplify]: Extracting #4: cost 0 inf + 527 1.913 * [simplify]: Simplified to (/.p16 (real->posit16 1) (+.p16 (real->posit16 1) x)) 1.913 * [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)))))) 1.914 * * * * [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))))))> 1.914 * [simplify]: Simplifying (/.p16 (real->posit16 1) (+.p16 x (real->posit16 1))) 1.914 * * [simplify]: iters left: 3 (5 enodes) 1.915 * * [simplify]: iters left: 2 (11 enodes) 1.917 * * [simplify]: iters left: 1 (13 enodes) 1.919 * * [simplify]: Extracting #0: cost 1 inf + 0 1.919 * * [simplify]: Extracting #1: cost 3 inf + 0 1.919 * * [simplify]: Extracting #2: cost 5 inf + 0 1.919 * * [simplify]: Extracting #3: cost 3 inf + 2 1.919 * * [simplify]: Extracting #4: cost 0 inf + 527 1.919 * [simplify]: Simplified to (/.p16 (real->posit16 1) (+.p16 (real->posit16 1) x)) 1.919 * [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)))))) 1.919 * * * * [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))))))> 1.920 * [simplify]: Simplifying (/.p16 (real->posit16 1) (+.p16 x (real->posit16 1))) 1.920 * * [simplify]: iters left: 3 (5 enodes) 1.921 * * [simplify]: iters left: 2 (11 enodes) 1.923 * * [simplify]: iters left: 1 (13 enodes) 1.925 * * [simplify]: Extracting #0: cost 1 inf + 0 1.925 * * [simplify]: Extracting #1: cost 3 inf + 0 1.925 * * [simplify]: Extracting #2: cost 5 inf + 0 1.925 * * [simplify]: Extracting #3: cost 3 inf + 2 1.925 * * [simplify]: Extracting #4: cost 0 inf + 527 1.925 * [simplify]: Simplified to (/.p16 (real->posit16 1) (+.p16 (real->posit16 1) x)) 1.925 * [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)))))) 1.926 * * * [progress]: adding candidates to table 2.174 * * [progress]: iteration 3 / 4 2.174 * * * [progress]: picking best candidate 2.200 * * * * [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)))))> 2.200 * * * [progress]: localizing error 2.458 * * * [progress]: generating rewritten candidates 2.458 * * * * [progress]: [ 1 / 4 ] rewriting at (2) 2.480 * * * * [progress]: [ 2 / 4 ] rewriting at (2 2) 2.485 * * * * [progress]: [ 3 / 4 ] rewriting at (2 1) 2.490 * * * * [progress]: [ 4 / 4 ] rewriting at (2 2 1) 2.493 * * * [progress]: generating series expansions 2.493 * * * * [progress]: [ 1 / 4 ] generating series at (2) 2.493 * * * * [progress]: [ 2 / 4 ] generating series at (2 2) 2.493 * * * * [progress]: [ 3 / 4 ] generating series at (2 1) 2.494 * * * * [progress]: [ 4 / 4 ] generating series at (2 2 1) 2.494 * * * [progress]: simplifying candidates 2.494 * * * * [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))))> 2.494 * [simplify]: Simplifying (*.p16 (/.p16 (real->posit16 1) (-.p16 (*.p16 x x) (*.p16 (real->posit16 1) (real->posit16 1)))) (real->posit16 1)) 2.494 * * [simplify]: iters left: 5 (8 enodes) 2.498 * * [simplify]: iters left: 4 (25 enodes) 2.508 * * [simplify]: iters left: 3 (62 enodes) 2.542 * * [simplify]: iters left: 2 (193 enodes) 2.625 * * [simplify]: Extracting #0: cost 1 inf + 0 2.625 * * [simplify]: Extracting #1: cost 65 inf + 0 2.625 * * [simplify]: Extracting #2: cost 241 inf + 0 2.627 * * [simplify]: Extracting #3: cost 260 inf + 43096 2.637 * * [simplify]: Extracting #4: cost 122 inf + 266467 2.656 * * [simplify]: Extracting #5: cost 18 inf + 464771 2.679 * * [simplify]: Extracting #6: cost 0 inf + 502437 2.700 * * [simplify]: Extracting #7: cost 0 inf + 501277 2.722 * [simplify]: Simplified to (/.p16 (*.p16 (real->posit16 1) (real->posit16 1)) (-.p16 (*.p16 x x) (*.p16 (real->posit16 1) (real->posit16 1)))) 2.722 * [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)))))) 2.722 * * * * [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)))))))> 2.722 * [simplify]: Simplifying (*.p16 (real->posit16 1) (/.p16 (real->posit16 1) (-.p16 (*.p16 x x) (*.p16 (real->posit16 1) (real->posit16 1))))) 2.722 * * [simplify]: iters left: 5 (8 enodes) 2.725 * * [simplify]: iters left: 4 (25 enodes) 2.732 * * [simplify]: iters left: 3 (62 enodes) 2.761 * * [simplify]: iters left: 2 (193 enodes) 2.873 * * [simplify]: Extracting #0: cost 1 inf + 0 2.873 * * [simplify]: Extracting #1: cost 65 inf + 0 2.875 * * [simplify]: Extracting #2: cost 241 inf + 0 2.878 * * [simplify]: Extracting #3: cost 260 inf + 43096 2.897 * * [simplify]: Extracting #4: cost 122 inf + 266467 2.917 * * [simplify]: Extracting #5: cost 18 inf + 464771 2.939 * * [simplify]: Extracting #6: cost 0 inf + 502437 2.967 * * [simplify]: Extracting #7: cost 0 inf + 501277 2.990 * [simplify]: Simplified to (/.p16 (*.p16 (real->posit16 1) (real->posit16 1)) (-.p16 (*.p16 x x) (*.p16 (real->posit16 1) (real->posit16 1)))) 2.990 * [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)))))) 2.990 * * * * [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))))))> 2.991 * [simplify]: Simplifying (/.p16 (real->posit16 1) (+.p16 x (real->posit16 1))) 2.991 * * [simplify]: iters left: 3 (5 enodes) 2.992 * * [simplify]: iters left: 2 (11 enodes) 2.995 * * [simplify]: iters left: 1 (13 enodes) 2.997 * * [simplify]: Extracting #0: cost 1 inf + 0 2.997 * * [simplify]: Extracting #1: cost 3 inf + 0 2.997 * * [simplify]: Extracting #2: cost 5 inf + 0 2.997 * * [simplify]: Extracting #3: cost 3 inf + 2 2.997 * * [simplify]: Extracting #4: cost 0 inf + 527 2.997 * [simplify]: Simplified to (/.p16 (real->posit16 1) (+.p16 (real->posit16 1) x)) 2.997 * [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)))))) 2.997 * * * * [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))))))> 2.997 * [simplify]: Simplifying (/.p16 (real->posit16 1) (+.p16 x (real->posit16 1))) 2.997 * * [simplify]: iters left: 3 (5 enodes) 2.999 * * [simplify]: iters left: 2 (11 enodes) 3.001 * * [simplify]: iters left: 1 (13 enodes) 3.003 * * [simplify]: Extracting #0: cost 1 inf + 0 3.003 * * [simplify]: Extracting #1: cost 3 inf + 0 3.003 * * [simplify]: Extracting #2: cost 5 inf + 0 3.003 * * [simplify]: Extracting #3: cost 3 inf + 2 3.003 * * [simplify]: Extracting #4: cost 0 inf + 527 3.003 * [simplify]: Simplified to (/.p16 (real->posit16 1) (+.p16 (real->posit16 1) x)) 3.003 * [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.003 * * * * [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.003 * * * * [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.004 * [simplify]: Simplifying (*.p16 (/.p16 (real->posit16 1) (-.p16 (*.p16 x x) (*.p16 (real->posit16 1) (real->posit16 1)))) (real->posit16 1)) 3.004 * * [simplify]: iters left: 5 (8 enodes) 3.006 * * [simplify]: iters left: 4 (25 enodes) 3.011 * * [simplify]: iters left: 3 (62 enodes) 3.024 * * [simplify]: iters left: 2 (193 enodes) 3.136 * * [simplify]: Extracting #0: cost 1 inf + 0 3.136 * * [simplify]: Extracting #1: cost 65 inf + 0 3.138 * * [simplify]: Extracting #2: cost 241 inf + 0 3.142 * * [simplify]: Extracting #3: cost 260 inf + 43096 3.163 * * [simplify]: Extracting #4: cost 122 inf + 266467 3.183 * * [simplify]: Extracting #5: cost 18 inf + 464771 3.205 * * [simplify]: Extracting #6: cost 0 inf + 502437 3.227 * * [simplify]: Extracting #7: cost 0 inf + 501277 3.249 * [simplify]: Simplified to (/.p16 (*.p16 (real->posit16 1) (real->posit16 1)) (-.p16 (*.p16 x x) (*.p16 (real->posit16 1) (real->posit16 1)))) 3.249 * [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))))))) 3.249 * * * * [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))))))))> 3.250 * [simplify]: Simplifying (*.p16 (real->posit16 1) (/.p16 (real->posit16 1) (-.p16 (*.p16 x x) (*.p16 (real->posit16 1) (real->posit16 1))))) 3.250 * * [simplify]: iters left: 5 (8 enodes) 3.253 * * [simplify]: iters left: 4 (25 enodes) 3.263 * * [simplify]: iters left: 3 (62 enodes) 3.284 * * [simplify]: iters left: 2 (193 enodes) 3.369 * * [simplify]: Extracting #0: cost 1 inf + 0 3.370 * * [simplify]: Extracting #1: cost 65 inf + 0 3.370 * * [simplify]: Extracting #2: cost 241 inf + 0 3.372 * * [simplify]: Extracting #3: cost 260 inf + 43096 3.382 * * [simplify]: Extracting #4: cost 122 inf + 266467 3.401 * * [simplify]: Extracting #5: cost 18 inf + 464771 3.429 * * [simplify]: Extracting #6: cost 0 inf + 502437 3.464 * * [simplify]: Extracting #7: cost 0 inf + 501277 3.489 * [simplify]: Simplified to (/.p16 (*.p16 (real->posit16 1) (real->posit16 1)) (-.p16 (*.p16 x x) (*.p16 (real->posit16 1) (real->posit16 1)))) 3.489 * [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))))))) 3.489 * * * * [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))))))> 3.489 * [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))))) 3.490 * * [simplify]: iters left: 5 (9 enodes) 3.492 * * [simplify]: iters left: 4 (32 enodes) 3.500 * * [simplify]: iters left: 3 (76 enodes) 3.524 * * [simplify]: iters left: 2 (239 enodes) 3.618 * * [simplify]: Extracting #0: cost 1 inf + 0 3.619 * * [simplify]: Extracting #1: cost 46 inf + 0 3.620 * * [simplify]: Extracting #2: cost 215 inf + 0 3.623 * * [simplify]: Extracting #3: cost 259 inf + 37842 3.645 * * [simplify]: Extracting #4: cost 141 inf + 336186 3.693 * * [simplify]: Extracting #5: cost 28 inf + 595296 3.741 * * [simplify]: Extracting #6: cost 1 inf + 655569 3.773 * * [simplify]: Extracting #7: cost 0 inf + 659011 3.823 * [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))))) 3.823 * [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)))))) 3.823 * * * * [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))))))> 3.823 * [simplify]: Simplifying (*.p16 (real->posit16 1) (+.p16 x (real->posit16 1))) 3.823 * * [simplify]: iters left: 3 (5 enodes) 3.825 * * [simplify]: iters left: 2 (17 enodes) 3.828 * * [simplify]: iters left: 1 (21 enodes) 3.831 * * [simplify]: Extracting #0: cost 1 inf + 0 3.831 * * [simplify]: Extracting #1: cost 5 inf + 0 3.831 * * [simplify]: Extracting #2: cost 7 inf + 0 3.831 * * [simplify]: Extracting #3: cost 5 inf + 2 3.831 * * [simplify]: Extracting #4: cost 0 inf + 1050 3.831 * [simplify]: Simplified to (*.p16 (real->posit16 1) (+.p16 (real->posit16 1) x)) 3.831 * [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)))))) 3.831 * * * * [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)))))))> 3.832 * * * * [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)))))> 3.832 * * * * [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)))))> 3.832 * * * * [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)))))> 3.832 * [simplify]: Simplifying (-.p16 x (real->posit16 1)) 3.832 * * [simplify]: iters left: 2 (4 enodes) 3.833 * * [simplify]: iters left: 1 (16 enodes) 3.836 * * [simplify]: Extracting #0: cost 1 inf + 0 3.836 * * [simplify]: Extracting #1: cost 6 inf + 0 3.836 * * [simplify]: Extracting #2: cost 11 inf + 1 3.836 * * [simplify]: Extracting #3: cost 11 inf + 323 3.836 * * [simplify]: Extracting #4: cost 5 inf + 1491 3.836 * * [simplify]: Extracting #5: cost 1 inf + 3657 3.837 * * [simplify]: Extracting #6: cost 0 inf + 5019 3.837 * [simplify]: Simplified to (-.p16 x (real->posit16 1)) 3.837 * [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))))) 3.837 * * * * [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)))))> 3.837 * [simplify]: Simplifying (+.p16 (*.p16 x x) (*.p16 (real->posit16 1) (real->posit16 1))) 3.837 * * [simplify]: iters left: 3 (6 enodes) 3.839 * * [simplify]: iters left: 2 (12 enodes) 3.842 * * [simplify]: iters left: 1 (14 enodes) 3.845 * * [simplify]: Extracting #0: cost 1 inf + 0 3.845 * * [simplify]: Extracting #1: cost 3 inf + 0 3.845 * * [simplify]: Extracting #2: cost 5 inf + 0 3.845 * * [simplify]: Extracting #3: cost 5 inf + 1 3.845 * * [simplify]: Extracting #4: cost 0 inf + 1327 3.845 * [simplify]: Simplified to (+.p16 (*.p16 (real->posit16 1) (real->posit16 1)) (*.p16 x x)) 3.845 * [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))))) 3.845 * * * * [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)))))> 3.846 * [simplify]: Simplifying (+.p16 x (real->posit16 1)) 3.846 * * [simplify]: iters left: 2 (4 enodes) 3.847 * * [simplify]: iters left: 1 (10 enodes) 3.849 * * [simplify]: Extracting #0: cost 1 inf + 0 3.849 * * [simplify]: Extracting #1: cost 3 inf + 0 3.849 * * [simplify]: Extracting #2: cost 3 inf + 1 3.849 * * [simplify]: Extracting #3: cost 0 inf + 45 3.849 * [simplify]: Simplified to (+.p16 (real->posit16 1) x) 3.849 * [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)))) 3.850 * * * * [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)))))> 3.850 * [simplify]: Simplifying (+.p16 x (real->posit16 1)) 3.850 * * [simplify]: iters left: 2 (4 enodes) 3.851 * * [simplify]: iters left: 1 (10 enodes) 3.853 * * [simplify]: Extracting #0: cost 1 inf + 0 3.853 * * [simplify]: Extracting #1: cost 3 inf + 0 3.853 * * [simplify]: Extracting #2: cost 3 inf + 1 3.853 * * [simplify]: Extracting #3: cost 0 inf + 45 3.853 * [simplify]: Simplified to (+.p16 (real->posit16 1) x) 3.853 * [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)))) 3.853 * * * * [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)))))> 3.854 * [simplify]: Simplifying (+.p16 x (real->posit16 1)) 3.854 * * [simplify]: iters left: 2 (4 enodes) 3.855 * * [simplify]: iters left: 1 (10 enodes) 3.857 * * [simplify]: Extracting #0: cost 1 inf + 0 3.857 * * [simplify]: Extracting #1: cost 3 inf + 0 3.857 * * [simplify]: Extracting #2: cost 3 inf + 1 3.857 * * [simplify]: Extracting #3: cost 0 inf + 45 3.857 * [simplify]: Simplified to (+.p16 (real->posit16 1) x) 3.857 * [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)))) 3.857 * * * * [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)))))> 3.857 * [simplify]: Simplifying (+.p16 x (real->posit16 1)) 3.857 * * [simplify]: iters left: 2 (4 enodes) 3.858 * * [simplify]: iters left: 1 (10 enodes) 3.860 * * [simplify]: Extracting #0: cost 1 inf + 0 3.860 * * [simplify]: Extracting #1: cost 3 inf + 0 3.860 * * [simplify]: Extracting #2: cost 3 inf + 1 3.860 * * [simplify]: Extracting #3: cost 0 inf + 45 3.860 * [simplify]: Simplified to (+.p16 (real->posit16 1) x) 3.860 * [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)))) 3.861 * * * [progress]: adding candidates to table 4.507 * * [progress]: iteration 4 / 4 4.507 * * * [progress]: picking best candidate 4.594 * * * * [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))))))> 4.594 * * * [progress]: localizing error 4.845 * * * [progress]: generating rewritten candidates 4.845 * * * * [progress]: [ 1 / 4 ] rewriting at (2) 4.859 * * * * [progress]: [ 2 / 4 ] rewriting at (2 2) 4.863 * * * * [progress]: [ 3 / 4 ] rewriting at (2 1) 4.867 * * * * [progress]: [ 4 / 4 ] rewriting at (2 2 2) 4.869 * * * [progress]: generating series expansions 4.869 * * * * [progress]: [ 1 / 4 ] generating series at (2) 4.869 * * * * [progress]: [ 2 / 4 ] generating series at (2 2) 4.869 * * * * [progress]: [ 3 / 4 ] generating series at (2 1) 4.869 * * * * [progress]: [ 4 / 4 ] generating series at (2 2 2) 4.869 * * * [progress]: simplifying candidates 4.869 * * * * [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)))))))> 4.870 * [simplify]: Simplifying (/.p16 (real->posit16 1) (+.p16 x (real->posit16 1))) 4.870 * * [simplify]: iters left: 3 (5 enodes) 4.871 * * [simplify]: iters left: 2 (11 enodes) 4.873 * * [simplify]: iters left: 1 (13 enodes) 4.875 * * [simplify]: Extracting #0: cost 1 inf + 0 4.875 * * [simplify]: Extracting #1: cost 3 inf + 0 4.875 * * [simplify]: Extracting #2: cost 5 inf + 0 4.875 * * [simplify]: Extracting #3: cost 3 inf + 2 4.875 * * [simplify]: Extracting #4: cost 0 inf + 527 4.876 * [simplify]: Simplified to (/.p16 (real->posit16 1) (+.p16 (real->posit16 1) x)) 4.876 * [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))))))) 4.876 * * * * [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)))))))> 4.876 * [simplify]: Simplifying (/.p16 (real->posit16 1) (+.p16 x (real->posit16 1))) 4.876 * * [simplify]: iters left: 3 (5 enodes) 4.877 * * [simplify]: iters left: 2 (11 enodes) 4.879 * * [simplify]: iters left: 1 (13 enodes) 4.881 * * [simplify]: Extracting #0: cost 1 inf + 0 4.881 * * [simplify]: Extracting #1: cost 3 inf + 0 4.881 * * [simplify]: Extracting #2: cost 5 inf + 0 4.881 * * [simplify]: Extracting #3: cost 3 inf + 2 4.881 * * [simplify]: Extracting #4: cost 0 inf + 527 4.881 * [simplify]: Simplified to (/.p16 (real->posit16 1) (+.p16 (real->posit16 1) x)) 4.881 * [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))))))) 4.882 * * * * [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))))> 4.882 * * * * [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)))))> 4.882 * [simplify]: Simplifying (-.p16 x (real->posit16 1)) 4.882 * * [simplify]: iters left: 2 (4 enodes) 4.883 * * [simplify]: iters left: 1 (16 enodes) 4.886 * * [simplify]: Extracting #0: cost 1 inf + 0 4.886 * * [simplify]: Extracting #1: cost 6 inf + 0 4.886 * * [simplify]: Extracting #2: cost 11 inf + 1 4.886 * * [simplify]: Extracting #3: cost 11 inf + 323 4.886 * * [simplify]: Extracting #4: cost 5 inf + 1491 4.886 * * [simplify]: Extracting #5: cost 1 inf + 3657 4.887 * * [simplify]: Extracting #6: cost 0 inf + 5019 4.887 * [simplify]: Simplified to (-.p16 x (real->posit16 1)) 4.887 * [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))))) 4.887 * * * * [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))))))> 4.887 * [simplify]: Simplifying (real->posit16 1) 4.887 * * [simplify]: iters left: 1 (2 enodes) 4.888 * * [simplify]: Extracting #0: cost 1 inf + 0 4.888 * * [simplify]: Extracting #1: cost 2 inf + 0 4.888 * * [simplify]: Extracting #2: cost 1 inf + 1 4.888 * * [simplify]: Extracting #3: cost 0 inf + 2 4.888 * [simplify]: Simplified to (real->posit16 1) 4.888 * [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)))))) 4.888 * * * * [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))))))> 4.888 * [simplify]: Simplifying (+.p16 (*.p16 x x) (*.p16 (real->posit16 1) (real->posit16 1))) 4.888 * * [simplify]: iters left: 3 (6 enodes) 4.890 * * [simplify]: iters left: 2 (12 enodes) 4.892 * * [simplify]: iters left: 1 (14 enodes) 4.898 * * [simplify]: Extracting #0: cost 1 inf + 0 4.898 * * [simplify]: Extracting #1: cost 3 inf + 0 4.898 * * [simplify]: Extracting #2: cost 5 inf + 0 4.898 * * [simplify]: Extracting #3: cost 5 inf + 1 4.898 * * [simplify]: Extracting #4: cost 0 inf + 1327 4.898 * [simplify]: Simplified to (+.p16 (*.p16 (real->posit16 1) (real->posit16 1)) (*.p16 x x)) 4.898 * [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))))) 4.899 * * * * [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))))))> 4.899 * [simplify]: Simplifying (/.p16 (real->posit16 1) (+.p16 x (real->posit16 1))) 4.899 * * [simplify]: iters left: 3 (5 enodes) 4.900 * * [simplify]: iters left: 2 (11 enodes) 4.902 * * [simplify]: iters left: 1 (13 enodes) 4.904 * * [simplify]: Extracting #0: cost 1 inf + 0 4.904 * * [simplify]: Extracting #1: cost 3 inf + 0 4.904 * * [simplify]: Extracting #2: cost 5 inf + 0 4.904 * * [simplify]: Extracting #3: cost 3 inf + 2 4.904 * * [simplify]: Extracting #4: cost 0 inf + 527 4.904 * [simplify]: Simplified to (/.p16 (real->posit16 1) (+.p16 (real->posit16 1) x)) 4.904 * [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)))))) 4.905 * [simplify]: Simplifying (/.p16 (+.p16 x (real->posit16 1)) (-.p16 x (real->posit16 1))) 4.905 * * [simplify]: iters left: 3 (6 enodes) 4.906 * * [simplify]: iters left: 2 (18 enodes) 4.909 * * [simplify]: iters left: 1 (31 enodes) 4.915 * * [simplify]: Extracting #0: cost 1 inf + 0 4.915 * * [simplify]: Extracting #1: cost 10 inf + 0 4.915 * * [simplify]: Extracting #2: cost 26 inf + 0 4.915 * * [simplify]: Extracting #3: cost 31 inf + 1 4.916 * * [simplify]: Extracting #4: cost 35 inf + 323 4.916 * * [simplify]: Extracting #5: cost 17 inf + 8069 4.917 * * [simplify]: Extracting #6: cost 0 inf + 25900 4.918 * [simplify]: Simplified to (/.p16 (+.p16 (real->posit16 1) x) (-.p16 x (real->posit16 1))) 4.918 * [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)))))) 4.918 * * * * [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))))))> 4.918 * * * * [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))))))> 4.918 * * * * [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))))))> 4.918 * [simplify]: Simplifying (+.p16 x (real->posit16 1)) 4.918 * * [simplify]: iters left: 2 (4 enodes) 4.919 * * [simplify]: iters left: 1 (10 enodes) 4.921 * * [simplify]: Extracting #0: cost 1 inf + 0 4.921 * * [simplify]: Extracting #1: cost 3 inf + 0 4.921 * * [simplify]: Extracting #2: cost 3 inf + 1 4.921 * * [simplify]: Extracting #3: cost 0 inf + 45 4.921 * [simplify]: Simplified to (+.p16 (real->posit16 1) x) 4.921 * [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)))))) 4.922 * [simplify]: Simplifying (-.p16 x (real->posit16 1)) 4.922 * * [simplify]: iters left: 2 (4 enodes) 4.923 * * [simplify]: iters left: 1 (16 enodes) 4.926 * * [simplify]: Extracting #0: cost 1 inf + 0 4.926 * * [simplify]: Extracting #1: cost 6 inf + 0 4.926 * * [simplify]: Extracting #2: cost 11 inf + 1 4.926 * * [simplify]: Extracting #3: cost 11 inf + 323 4.926 * * [simplify]: Extracting #4: cost 5 inf + 1491 4.926 * * [simplify]: Extracting #5: cost 1 inf + 3657 4.926 * * [simplify]: Extracting #6: cost 0 inf + 5019 4.926 * [simplify]: Simplified to (-.p16 x (real->posit16 1)) 4.926 * [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)))))) 4.927 * * * * [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)))))))> 4.927 * * * * [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)))))))> 4.927 * * * * [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))))))> 4.927 * [simplify]: Simplifying (*.p16 (real->posit16 1) (+.p16 x (real->posit16 1))) 4.927 * * [simplify]: iters left: 3 (5 enodes) 4.928 * * [simplify]: iters left: 2 (17 enodes) 4.931 * * [simplify]: iters left: 1 (21 enodes) 4.934 * * [simplify]: Extracting #0: cost 1 inf + 0 4.934 * * [simplify]: Extracting #1: cost 5 inf + 0 4.934 * * [simplify]: Extracting #2: cost 7 inf + 0 4.934 * * [simplify]: Extracting #3: cost 5 inf + 2 4.934 * * [simplify]: Extracting #4: cost 0 inf + 1050 4.935 * [simplify]: Simplified to (*.p16 (real->posit16 1) (+.p16 (real->posit16 1) x)) 4.935 * [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.935 * * * * [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))))))> 4.935 * [simplify]: Simplifying (*.p16 (real->posit16 1) (+.p16 x (real->posit16 1))) 4.935 * * [simplify]: iters left: 3 (5 enodes) 4.937 * * [simplify]: iters left: 2 (17 enodes) 4.943 * * [simplify]: iters left: 1 (21 enodes) 4.948 * * [simplify]: Extracting #0: cost 1 inf + 0 4.949 * * [simplify]: Extracting #1: cost 5 inf + 0 4.949 * * [simplify]: Extracting #2: cost 7 inf + 0 4.949 * * [simplify]: Extracting #3: cost 5 inf + 2 4.949 * * [simplify]: Extracting #4: cost 0 inf + 1050 4.949 * [simplify]: Simplified to (*.p16 (real->posit16 1) (+.p16 (real->posit16 1) x)) 4.949 * [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.949 * * * * [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))))))> 4.950 * [simplify]: Simplifying (*.p16 (real->posit16 1) (+.p16 x (real->posit16 1))) 4.950 * * [simplify]: iters left: 3 (5 enodes) 4.952 * * [simplify]: iters left: 2 (17 enodes) 4.958 * * [simplify]: iters left: 1 (21 enodes) 4.964 * * [simplify]: Extracting #0: cost 1 inf + 0 4.964 * * [simplify]: Extracting #1: cost 5 inf + 0 4.964 * * [simplify]: Extracting #2: cost 7 inf + 0 4.964 * * [simplify]: Extracting #3: cost 5 inf + 2 4.964 * * [simplify]: Extracting #4: cost 0 inf + 1050 4.965 * [simplify]: Simplified to (*.p16 (real->posit16 1) (+.p16 (real->posit16 1) x)) 4.965 * [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.965 * * * * [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))))))> 4.965 * [simplify]: Simplifying (*.p16 (real->posit16 1) (+.p16 x (real->posit16 1))) 4.965 * * [simplify]: iters left: 3 (5 enodes) 4.968 * * [simplify]: iters left: 2 (17 enodes) 4.971 * * [simplify]: iters left: 1 (21 enodes) 4.974 * * [simplify]: Extracting #0: cost 1 inf + 0 4.974 * * [simplify]: Extracting #1: cost 5 inf + 0 4.974 * * [simplify]: Extracting #2: cost 7 inf + 0 4.974 * * [simplify]: Extracting #3: cost 5 inf + 2 4.974 * * [simplify]: Extracting #4: cost 0 inf + 1050 4.974 * [simplify]: Simplified to (*.p16 (real->posit16 1) (+.p16 (real->posit16 1) x)) 4.974 * [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.975 * * * [progress]: adding candidates to table 5.637 * [progress]: [Phase 3 of 3] Extracting. 5.637 * * [regime]: Finding splitpoints for: (#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 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 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 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 (*.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))))))))> #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 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)))))))>) 5.640 * * * [regime-changes]: Trying 1 branch expressions: (x) 5.640 * * * * [regimes]: Trying to branch on x from (#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 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 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 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 (*.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))))))))> #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 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)))))))>) 5.873 * * * [regime]: Found split indices: #