0.001 * [progress]: [Phase 1 of 3] Setting up. 0.001 * * * [progress]: [1/2] Preparing points 0.001 * * * * [points]: Sampling 256 additional inputs, on iter 0 have 0 / 256 0.002 * * * * [points]: Computing exacts on every 16 of 256 points to ramp up precision 0.004 * * * * [points]: Setting MPFR precision to 64 0.005 * * * * [points]: Setting MPFR precision to 320 0.006 * * * * [points]: Computing exacts on every 8 of 256 points to ramp up precision 0.009 * * * * [points]: Setting MPFR precision to 64 0.011 * * * * [points]: Setting MPFR precision to 320 0.014 * * * * [points]: Computing exacts on every 4 of 256 points to ramp up precision 0.019 * * * * [points]: Setting MPFR precision to 64 0.023 * * * * [points]: Setting MPFR precision to 320 0.028 * * * * [points]: Computing exacts on every 2 of 256 points to ramp up precision 0.032 * * * * [points]: Setting MPFR precision to 64 0.037 * * * * [points]: Setting MPFR precision to 320 0.041 * * * * [points]: Computing exacts for 256 points 0.043 * * * * [points]: Setting MPFR precision to 64 0.065 * * * * [points]: Setting MPFR precision to 320 0.080 * * * * [points]: Filtering points with unrepresentable outputs 0.081 * * * * [points]: Sampled 256 points with exact outputs 0.081 * * * [progress]: [2/2] Setting up program. 0.094 * [progress]: [Phase 2 of 3] Improving. 0.094 * * * * [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.094 * [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.094 * * [simplify]: iters left: 5 (12 enodes) 0.097 * * [simplify]: iters left: 4 (35 enodes) 0.108 * * [simplify]: iters left: 3 (83 enodes) 0.135 * * [simplify]: iters left: 2 (233 enodes) 0.256 * * [simplify]: Extracting #0: cost 1 inf + 0 0.256 * * [simplify]: Extracting #1: cost 29 inf + 0 0.256 * * [simplify]: Extracting #2: cost 123 inf + 0 0.257 * * [simplify]: Extracting #3: cost 244 inf + 1 0.259 * * [simplify]: Extracting #4: cost 308 inf + 32857 0.271 * * [simplify]: Extracting #5: cost 149 inf + 308686 0.311 * * [simplify]: Extracting #6: cost 4 inf + 549893 0.360 * * [simplify]: Extracting #7: cost 0 inf + 561504 0.409 * [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.409 * [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.433 * * [progress]: iteration 1 / 4 0.433 * * * [progress]: picking best candidate 0.454 * * * * [pick]: Picked #posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (real->posit16 2) x)) (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1)))))> 0.454 * * * [progress]: localizing error 0.681 * * * [progress]: generating rewritten candidates 0.681 * * * * [progress]: [ 1 / 4 ] rewriting at (2) 0.693 * * * * [progress]: [ 2 / 4 ] rewriting at (2 1) 0.696 * * * * [progress]: [ 3 / 4 ] rewriting at (2 1 1) 0.698 * * * * [progress]: [ 4 / 4 ] rewriting at (2 2) 0.700 * * * [progress]: generating series expansions 0.700 * * * * [progress]: [ 1 / 4 ] generating series at (2) 0.700 * * * * [progress]: [ 2 / 4 ] generating series at (2 1) 0.700 * * * * [progress]: [ 3 / 4 ] generating series at (2 1 1) 0.700 * * * * [progress]: [ 4 / 4 ] generating series at (2 2) 0.700 * * * [progress]: simplifying candidates 0.700 * * * * [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.701 * [simplify]: Simplifying (/.p16 (real->posit16 1) (+.p16 x (real->posit16 1))) 0.701 * * [simplify]: iters left: 3 (5 enodes) 0.702 * * [simplify]: iters left: 2 (11 enodes) 0.704 * * [simplify]: iters left: 1 (13 enodes) 0.706 * * [simplify]: Extracting #0: cost 1 inf + 0 0.706 * * [simplify]: Extracting #1: cost 3 inf + 0 0.706 * * [simplify]: Extracting #2: cost 5 inf + 0 0.706 * * [simplify]: Extracting #3: cost 3 inf + 2 0.706 * * [simplify]: Extracting #4: cost 0 inf + 527 0.706 * [simplify]: Simplified to (/.p16 (real->posit16 1) (+.p16 (real->posit16 1) x)) 0.707 * [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.707 * * * * [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.707 * [simplify]: Simplifying (/.p16 (real->posit16 1) (+.p16 x (real->posit16 1))) 0.707 * * [simplify]: iters left: 3 (5 enodes) 0.708 * * [simplify]: iters left: 2 (11 enodes) 0.710 * * [simplify]: iters left: 1 (13 enodes) 0.712 * * [simplify]: Extracting #0: cost 1 inf + 0 0.712 * * [simplify]: Extracting #1: cost 3 inf + 0 0.712 * * [simplify]: Extracting #2: cost 5 inf + 0 0.712 * * [simplify]: Extracting #3: cost 3 inf + 2 0.712 * * [simplify]: Extracting #4: cost 0 inf + 527 0.712 * [simplify]: Simplified to (/.p16 (real->posit16 1) (+.p16 (real->posit16 1) x)) 0.712 * [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.712 * * * * [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.712 * * * * [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.712 * * * * [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.712 * * * * [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.712 * [simplify]: Simplifying (+.p16 x (real->posit16 1)) 0.712 * * [simplify]: iters left: 2 (4 enodes) 0.713 * * [simplify]: iters left: 1 (10 enodes) 0.715 * * [simplify]: Extracting #0: cost 1 inf + 0 0.715 * * [simplify]: Extracting #1: cost 3 inf + 0 0.715 * * [simplify]: Extracting #2: cost 3 inf + 1 0.715 * * [simplify]: Extracting #3: cost 0 inf + 45 0.715 * [simplify]: Simplified to (+.p16 (real->posit16 1) x) 0.715 * [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.715 * * * * [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.715 * [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.716 * * [simplify]: iters left: 5 (12 enodes) 0.718 * * [simplify]: iters left: 4 (35 enodes) 0.725 * * [simplify]: iters left: 3 (83 enodes) 0.749 * * [simplify]: iters left: 2 (233 enodes) 0.862 * * [simplify]: Extracting #0: cost 1 inf + 0 0.863 * * [simplify]: Extracting #1: cost 29 inf + 0 0.863 * * [simplify]: Extracting #2: cost 123 inf + 0 0.865 * * [simplify]: Extracting #3: cost 244 inf + 1 0.869 * * [simplify]: Extracting #4: cost 308 inf + 32857 0.891 * * [simplify]: Extracting #5: cost 149 inf + 308686 0.933 * * [simplify]: Extracting #6: cost 4 inf + 549893 0.980 * * [simplify]: Extracting #7: cost 0 inf + 561504 1.026 * [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.026 * [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.026 * * * * [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)))))> 1.027 * [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.028 * * [simplify]: iters left: 5 (12 enodes) 1.034 * * [simplify]: iters left: 4 (35 enodes) 1.047 * * [simplify]: iters left: 3 (83 enodes) 1.078 * * [simplify]: iters left: 2 (233 enodes) 1.197 * * [simplify]: Extracting #0: cost 1 inf + 0 1.197 * * [simplify]: Extracting #1: cost 29 inf + 0 1.198 * * [simplify]: Extracting #2: cost 123 inf + 0 1.198 * * [simplify]: Extracting #3: cost 244 inf + 1 1.200 * * [simplify]: Extracting #4: cost 308 inf + 32857 1.216 * * [simplify]: Extracting #5: cost 149 inf + 308686 1.260 * * [simplify]: Extracting #6: cost 4 inf + 549893 1.314 * * [simplify]: Extracting #7: cost 0 inf + 561504 1.362 * [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.362 * [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.362 * * * * [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.363 * [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.363 * * [simplify]: iters left: 5 (12 enodes) 1.369 * * [simplify]: iters left: 4 (35 enodes) 1.382 * * [simplify]: iters left: 3 (83 enodes) 1.415 * * [simplify]: iters left: 2 (233 enodes) 1.536 * * [simplify]: Extracting #0: cost 1 inf + 0 1.536 * * [simplify]: Extracting #1: cost 29 inf + 0 1.536 * * [simplify]: Extracting #2: cost 123 inf + 0 1.537 * * [simplify]: Extracting #3: cost 244 inf + 1 1.539 * * [simplify]: Extracting #4: cost 308 inf + 32857 1.558 * * [simplify]: Extracting #5: cost 149 inf + 308686 1.606 * * [simplify]: Extracting #6: cost 4 inf + 549893 1.655 * * [simplify]: Extracting #7: cost 0 inf + 561504 1.703 * [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.703 * [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.703 * * * * [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.704 * [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.704 * * [simplify]: iters left: 5 (12 enodes) 1.710 * * [simplify]: iters left: 4 (35 enodes) 1.723 * * [simplify]: iters left: 3 (83 enodes) 1.758 * * [simplify]: iters left: 2 (233 enodes) 1.887 * * [simplify]: Extracting #0: cost 1 inf + 0 1.887 * * [simplify]: Extracting #1: cost 29 inf + 0 1.888 * * [simplify]: Extracting #2: cost 123 inf + 0 1.888 * * [simplify]: Extracting #3: cost 244 inf + 1 1.890 * * [simplify]: Extracting #4: cost 308 inf + 32857 1.902 * * [simplify]: Extracting #5: cost 149 inf + 308686 1.924 * * [simplify]: Extracting #6: cost 4 inf + 549893 1.954 * * [simplify]: Extracting #7: cost 0 inf + 561504 1.982 * [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.982 * [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.984 * * * [progress]: adding candidates to table 2.421 * * [progress]: iteration 2 / 4 2.421 * * * [progress]: picking best candidate 2.505 * * * * [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.505 * * * [progress]: localizing error 2.837 * * * [progress]: generating rewritten candidates 2.837 * * * * [progress]: [ 1 / 4 ] rewriting at (2) 2.849 * * * * [progress]: [ 2 / 4 ] rewriting at (2 2) 2.866 * * * * [progress]: [ 3 / 4 ] rewriting at (2 1) 2.869 * * * * [progress]: [ 4 / 4 ] rewriting at (2 2 2) 2.871 * * * [progress]: generating series expansions 2.871 * * * * [progress]: [ 1 / 4 ] generating series at (2) 2.871 * * * * [progress]: [ 2 / 4 ] generating series at (2 2) 2.871 * * * * [progress]: [ 3 / 4 ] generating series at (2 1) 2.871 * * * * [progress]: [ 4 / 4 ] generating series at (2 2 2) 2.871 * * * [progress]: simplifying candidates 2.871 * * * * [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.871 * [simplify]: Simplifying (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1))) 2.871 * * [simplify]: iters left: 3 (5 enodes) 2.873 * * [simplify]: iters left: 2 (17 enodes) 2.876 * * [simplify]: iters left: 1 (31 enodes) 2.882 * * [simplify]: Extracting #0: cost 1 inf + 0 2.882 * * [simplify]: Extracting #1: cost 11 inf + 0 2.882 * * [simplify]: Extracting #2: cost 28 inf + 0 2.882 * * [simplify]: Extracting #3: cost 29 inf + 324 2.882 * * [simplify]: Extracting #4: cost 22 inf + 6266 2.883 * * [simplify]: Extracting #5: cost 3 inf + 23256 2.884 * * [simplify]: Extracting #6: cost 0 inf + 26382 2.885 * * [simplify]: Extracting #7: cost 0 inf + 25822 2.886 * [simplify]: Simplified to (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1))) 2.886 * [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.886 * * * * [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.886 * * * * [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.886 * * * * [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.886 * [simplify]: Simplifying (+.p16 x (real->posit16 1)) 2.886 * * [simplify]: iters left: 2 (4 enodes) 2.888 * * [simplify]: iters left: 1 (10 enodes) 2.889 * * [simplify]: Extracting #0: cost 1 inf + 0 2.889 * * [simplify]: Extracting #1: cost 3 inf + 0 2.890 * * [simplify]: Extracting #2: cost 3 inf + 1 2.890 * * [simplify]: Extracting #3: cost 0 inf + 45 2.890 * [simplify]: Simplified to (+.p16 (real->posit16 1) x) 2.890 * [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.890 * * * * [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.890 * [simplify]: Simplifying (/.p16 (real->posit16 1) (+.p16 x (real->posit16 1))) 2.890 * * [simplify]: iters left: 3 (5 enodes) 2.891 * * [simplify]: iters left: 2 (11 enodes) 2.893 * * [simplify]: iters left: 1 (13 enodes) 2.895 * * [simplify]: Extracting #0: cost 1 inf + 0 2.895 * * [simplify]: Extracting #1: cost 3 inf + 0 2.895 * * [simplify]: Extracting #2: cost 5 inf + 0 2.895 * * [simplify]: Extracting #3: cost 3 inf + 2 2.895 * * [simplify]: Extracting #4: cost 0 inf + 527 2.895 * [simplify]: Simplified to (/.p16 (real->posit16 1) (+.p16 (real->posit16 1) x)) 2.895 * [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.895 * * * * [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.895 * [simplify]: Simplifying (/.p16 (real->posit16 1) (+.p16 x (real->posit16 1))) 2.896 * * [simplify]: iters left: 3 (5 enodes) 2.897 * * [simplify]: iters left: 2 (11 enodes) 2.899 * * [simplify]: iters left: 1 (13 enodes) 2.901 * * [simplify]: Extracting #0: cost 1 inf + 0 2.901 * * [simplify]: Extracting #1: cost 3 inf + 0 2.901 * * [simplify]: Extracting #2: cost 5 inf + 0 2.901 * * [simplify]: Extracting #3: cost 3 inf + 2 2.901 * * [simplify]: Extracting #4: cost 0 inf + 527 2.901 * [simplify]: Simplified to (/.p16 (real->posit16 1) (+.p16 (real->posit16 1) x)) 2.901 * [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.901 * * * * [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.901 * [simplify]: Simplifying (/.p16 (real->posit16 1) (+.p16 x (real->posit16 1))) 2.901 * * [simplify]: iters left: 3 (5 enodes) 2.903 * * [simplify]: iters left: 2 (11 enodes) 2.905 * * [simplify]: iters left: 1 (13 enodes) 2.909 * * [simplify]: Extracting #0: cost 1 inf + 0 2.909 * * [simplify]: Extracting #1: cost 3 inf + 0 2.909 * * [simplify]: Extracting #2: cost 5 inf + 0 2.909 * * [simplify]: Extracting #3: cost 3 inf + 2 2.910 * * [simplify]: Extracting #4: cost 0 inf + 527 2.910 * [simplify]: Simplified to (/.p16 (real->posit16 1) (+.p16 (real->posit16 1) x)) 2.910 * [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.910 * * * * [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.910 * [simplify]: Simplifying (/.p16 (real->posit16 1) (+.p16 x (real->posit16 1))) 2.910 * * [simplify]: iters left: 3 (5 enodes) 2.913 * * [simplify]: iters left: 2 (11 enodes) 2.916 * * [simplify]: iters left: 1 (13 enodes) 2.920 * * [simplify]: Extracting #0: cost 1 inf + 0 2.920 * * [simplify]: Extracting #1: cost 3 inf + 0 2.920 * * [simplify]: Extracting #2: cost 5 inf + 0 2.920 * * [simplify]: Extracting #3: cost 3 inf + 2 2.921 * * [simplify]: Extracting #4: cost 0 inf + 527 2.921 * [simplify]: Simplified to (/.p16 (real->posit16 1) (+.p16 (real->posit16 1) x)) 2.921 * [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.921 * * * [progress]: adding candidates to table 3.312 * * [progress]: iteration 3 / 4 3.312 * * * [progress]: picking best candidate 3.391 * * * * [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.391 * * * [progress]: localizing error 3.693 * * * [progress]: generating rewritten candidates 3.693 * * * * [progress]: [ 1 / 4 ] rewriting at (2) 3.717 * * * * [progress]: [ 2 / 4 ] rewriting at (2 2) 3.722 * * * * [progress]: [ 3 / 4 ] rewriting at (2 1) 3.728 * * * * [progress]: [ 4 / 4 ] rewriting at (2 2 1 2) 3.733 * * * [progress]: generating series expansions 3.733 * * * * [progress]: [ 1 / 4 ] generating series at (2) 3.733 * * * * [progress]: [ 2 / 4 ] generating series at (2 2) 3.733 * * * * [progress]: [ 3 / 4 ] generating series at (2 1) 3.733 * * * * [progress]: [ 4 / 4 ] generating series at (2 2 1 2) 3.733 * * * [progress]: simplifying candidates 3.733 * * * * [progress]: [ 1 / 19 ] 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.733 * [simplify]: Simplifying (*.p16 (/.p16 (real->posit16 1) (-.p16 (*.p16 x x) (*.p16 (real->posit16 1) (real->posit16 1)))) (real->posit16 1)) 3.734 * * [simplify]: iters left: 5 (8 enodes) 3.738 * * [simplify]: iters left: 4 (25 enodes) 3.748 * * [simplify]: iters left: 3 (62 enodes) 3.778 * * [simplify]: iters left: 2 (193 enodes) 3.855 * * [simplify]: Extracting #0: cost 1 inf + 0 3.855 * * [simplify]: Extracting #1: cost 65 inf + 0 3.856 * * [simplify]: Extracting #2: cost 241 inf + 0 3.858 * * [simplify]: Extracting #3: cost 260 inf + 43096 3.868 * * [simplify]: Extracting #4: cost 122 inf + 266467 3.887 * * [simplify]: Extracting #5: cost 18 inf + 464771 3.910 * * [simplify]: Extracting #6: cost 0 inf + 502437 3.931 * * [simplify]: Extracting #7: cost 0 inf + 501277 3.952 * [simplify]: Simplified to (/.p16 (*.p16 (real->posit16 1) (real->posit16 1)) (-.p16 (*.p16 x x) (*.p16 (real->posit16 1) (real->posit16 1)))) 3.952 * [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.952 * * * * [progress]: [ 2 / 19 ] 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.953 * [simplify]: Simplifying (*.p16 (real->posit16 1) (/.p16 (real->posit16 1) (-.p16 (*.p16 x x) (*.p16 (real->posit16 1) (real->posit16 1))))) 3.953 * * [simplify]: iters left: 5 (8 enodes) 3.955 * * [simplify]: iters left: 4 (25 enodes) 3.960 * * [simplify]: iters left: 3 (62 enodes) 3.973 * * [simplify]: iters left: 2 (193 enodes) 4.072 * * [simplify]: Extracting #0: cost 1 inf + 0 4.072 * * [simplify]: Extracting #1: cost 65 inf + 0 4.073 * * [simplify]: Extracting #2: cost 241 inf + 0 4.076 * * [simplify]: Extracting #3: cost 260 inf + 43096 4.092 * * [simplify]: Extracting #4: cost 122 inf + 266467 4.117 * * [simplify]: Extracting #5: cost 18 inf + 464771 4.139 * * [simplify]: Extracting #6: cost 0 inf + 502437 4.163 * * [simplify]: Extracting #7: cost 0 inf + 501277 4.205 * [simplify]: Simplified to (/.p16 (*.p16 (real->posit16 1) (real->posit16 1)) (-.p16 (*.p16 x x) (*.p16 (real->posit16 1) (real->posit16 1)))) 4.205 * [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)))))) 4.205 * * * * [progress]: [ 3 / 19 ] 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))))))> 4.205 * [simplify]: Simplifying (/.p16 (real->posit16 1) (+.p16 x (real->posit16 1))) 4.205 * * [simplify]: iters left: 3 (5 enodes) 4.207 * * [simplify]: iters left: 2 (11 enodes) 4.209 * * [simplify]: iters left: 1 (13 enodes) 4.211 * * [simplify]: Extracting #0: cost 1 inf + 0 4.211 * * [simplify]: Extracting #1: cost 3 inf + 0 4.211 * * [simplify]: Extracting #2: cost 5 inf + 0 4.211 * * [simplify]: Extracting #3: cost 3 inf + 2 4.211 * * [simplify]: Extracting #4: cost 0 inf + 527 4.211 * [simplify]: Simplified to (/.p16 (real->posit16 1) (+.p16 (real->posit16 1) x)) 4.211 * [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)))))) 4.211 * * * * [progress]: [ 4 / 19 ] 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))))))> 4.211 * [simplify]: Simplifying (/.p16 (real->posit16 1) (+.p16 x (real->posit16 1))) 4.211 * * [simplify]: iters left: 3 (5 enodes) 4.212 * * [simplify]: iters left: 2 (11 enodes) 4.214 * * [simplify]: iters left: 1 (13 enodes) 4.216 * * [simplify]: Extracting #0: cost 1 inf + 0 4.216 * * [simplify]: Extracting #1: cost 3 inf + 0 4.216 * * [simplify]: Extracting #2: cost 5 inf + 0 4.216 * * [simplify]: Extracting #3: cost 3 inf + 2 4.216 * * [simplify]: Extracting #4: cost 0 inf + 527 4.216 * [simplify]: Simplified to (/.p16 (real->posit16 1) (+.p16 (real->posit16 1) x)) 4.216 * [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)))))) 4.216 * * * * [progress]: [ 5 / 19 ] 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))))> 4.216 * * * * [progress]: [ 6 / 19 ] 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)))))> 4.217 * [simplify]: Simplifying (*.p16 (/.p16 (real->posit16 1) (-.p16 (*.p16 x x) (*.p16 (real->posit16 1) (real->posit16 1)))) (real->posit16 1)) 4.217 * * [simplify]: iters left: 5 (8 enodes) 4.219 * * [simplify]: iters left: 4 (25 enodes) 4.223 * * [simplify]: iters left: 3 (62 enodes) 4.235 * * [simplify]: iters left: 2 (193 enodes) 4.322 * * [simplify]: Extracting #0: cost 1 inf + 0 4.322 * * [simplify]: Extracting #1: cost 65 inf + 0 4.323 * * [simplify]: Extracting #2: cost 241 inf + 0 4.325 * * [simplify]: Extracting #3: cost 260 inf + 43096 4.338 * * [simplify]: Extracting #4: cost 122 inf + 266467 4.357 * * [simplify]: Extracting #5: cost 18 inf + 464771 4.378 * * [simplify]: Extracting #6: cost 0 inf + 502437 4.399 * * [simplify]: Extracting #7: cost 0 inf + 501277 4.435 * [simplify]: Simplified to (/.p16 (*.p16 (real->posit16 1) (real->posit16 1)) (-.p16 (*.p16 x x) (*.p16 (real->posit16 1) (real->posit16 1)))) 4.435 * [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.435 * * * * [progress]: [ 7 / 19 ] 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.435 * [simplify]: Simplifying (*.p16 (real->posit16 1) (/.p16 (real->posit16 1) (-.p16 (*.p16 x x) (*.p16 (real->posit16 1) (real->posit16 1))))) 4.435 * * [simplify]: iters left: 5 (8 enodes) 4.439 * * [simplify]: iters left: 4 (25 enodes) 4.444 * * [simplify]: iters left: 3 (62 enodes) 4.457 * * [simplify]: iters left: 2 (193 enodes) 4.610 * * [simplify]: Extracting #0: cost 1 inf + 0 4.611 * * [simplify]: Extracting #1: cost 65 inf + 0 4.612 * * [simplify]: Extracting #2: cost 241 inf + 0 4.617 * * [simplify]: Extracting #3: cost 260 inf + 43096 4.637 * * [simplify]: Extracting #4: cost 122 inf + 266467 4.672 * * [simplify]: Extracting #5: cost 18 inf + 464771 4.700 * * [simplify]: Extracting #6: cost 0 inf + 502437 4.736 * * [simplify]: Extracting #7: cost 0 inf + 501277 4.758 * [simplify]: Simplified to (/.p16 (*.p16 (real->posit16 1) (real->posit16 1)) (-.p16 (*.p16 x x) (*.p16 (real->posit16 1) (real->posit16 1)))) 4.758 * [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.758 * * * * [progress]: [ 8 / 19 ] 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.759 * [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.759 * * [simplify]: iters left: 5 (9 enodes) 4.763 * * [simplify]: iters left: 4 (32 enodes) 4.775 * * [simplify]: iters left: 3 (76 enodes) 4.810 * * [simplify]: iters left: 2 (239 enodes) 4.988 * * [simplify]: Extracting #0: cost 1 inf + 0 4.988 * * [simplify]: Extracting #1: cost 46 inf + 0 4.989 * * [simplify]: Extracting #2: cost 215 inf + 0 4.993 * * [simplify]: Extracting #3: cost 259 inf + 37842 5.018 * * [simplify]: Extracting #4: cost 141 inf + 336186 5.068 * * [simplify]: Extracting #5: cost 28 inf + 595296 5.135 * * [simplify]: Extracting #6: cost 1 inf + 655569 5.199 * * [simplify]: Extracting #7: cost 0 inf + 659011 5.260 * [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))))) 5.260 * [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)))))) 5.261 * * * * [progress]: [ 9 / 19 ] 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))))))> 5.261 * [simplify]: Simplifying (*.p16 (real->posit16 1) (+.p16 x (real->posit16 1))) 5.261 * * [simplify]: iters left: 3 (5 enodes) 5.264 * * [simplify]: iters left: 2 (17 enodes) 5.270 * * [simplify]: iters left: 1 (21 enodes) 5.275 * * [simplify]: Extracting #0: cost 1 inf + 0 5.276 * * [simplify]: Extracting #1: cost 5 inf + 0 5.276 * * [simplify]: Extracting #2: cost 7 inf + 0 5.276 * * [simplify]: Extracting #3: cost 5 inf + 2 5.276 * * [simplify]: Extracting #4: cost 0 inf + 1050 5.276 * [simplify]: Simplified to (*.p16 (real->posit16 1) (+.p16 (real->posit16 1) x)) 5.276 * [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)))))) 5.276 * * * * [progress]: [ 10 / 19 ] 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)))))))> 5.276 * * * * [progress]: [ 11 / 19 ] 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)))))> 5.276 * * * * [progress]: [ 12 / 19 ] 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)))))> 5.276 * * * * [progress]: [ 13 / 19 ] simplifiying candidate #posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (real->posit16 2) x)) (*.p16 (/.p16 (real->posit16 1) (*.p16 (+.p16 x (real->posit16 1)) (-.p16 x (real->posit16 1)))) (+.p16 x (real->posit16 1)))))> 5.277 * [simplify]: Simplifying (+.p16 x (real->posit16 1)) 5.277 * * [simplify]: iters left: 2 (4 enodes) 5.279 * * [simplify]: iters left: 1 (10 enodes) 5.283 * * [simplify]: Extracting #0: cost 1 inf + 0 5.283 * * [simplify]: Extracting #1: cost 3 inf + 0 5.283 * * [simplify]: Extracting #2: cost 3 inf + 1 5.283 * * [simplify]: Extracting #3: cost 0 inf + 45 5.283 * [simplify]: Simplified to (+.p16 (real->posit16 1) x) 5.283 * [simplify]: Simplified (2 2 1 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 (real->posit16 1) x) (-.p16 x (real->posit16 1)))) (+.p16 x (real->posit16 1))))) 5.283 * [simplify]: Simplifying (-.p16 x (real->posit16 1)) 5.284 * * [simplify]: iters left: 2 (4 enodes) 5.286 * * [simplify]: iters left: 1 (16 enodes) 5.293 * * [simplify]: Extracting #0: cost 1 inf + 0 5.293 * * [simplify]: Extracting #1: cost 6 inf + 0 5.294 * * [simplify]: Extracting #2: cost 11 inf + 1 5.294 * * [simplify]: Extracting #3: cost 11 inf + 323 5.294 * * [simplify]: Extracting #4: cost 5 inf + 1491 5.294 * * [simplify]: Extracting #5: cost 1 inf + 3657 5.295 * * [simplify]: Extracting #6: cost 0 inf + 5019 5.295 * [simplify]: Simplified to (-.p16 x (real->posit16 1)) 5.295 * [simplify]: Simplified (2 2 1 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 (real->posit16 1)) (-.p16 x (real->posit16 1)))) (+.p16 x (real->posit16 1))))) 5.295 * * * * [progress]: [ 14 / 19 ] simplifiying candidate #posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (real->posit16 2) x)) (*.p16 (/.p16 (real->posit16 1) (+.p16 (*.p16 x x) (neg.p16 (*.p16 (real->posit16 1) (real->posit16 1))))) (+.p16 x (real->posit16 1)))))> 5.295 * * * * [progress]: [ 15 / 19 ] simplifiying candidate #posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (real->posit16 2) x)) (*.p16 (/.p16 (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))))) (+.p16 x (real->posit16 1)))))> 5.295 * * * * [progress]: [ 16 / 19 ] 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)))))> 5.296 * [simplify]: Simplifying (+.p16 x (real->posit16 1)) 5.296 * * [simplify]: iters left: 2 (4 enodes) 5.298 * * [simplify]: iters left: 1 (10 enodes) 5.301 * * [simplify]: Extracting #0: cost 1 inf + 0 5.302 * * [simplify]: Extracting #1: cost 3 inf + 0 5.302 * * [simplify]: Extracting #2: cost 3 inf + 1 5.302 * * [simplify]: Extracting #3: cost 0 inf + 45 5.302 * [simplify]: Simplified to (+.p16 (real->posit16 1) x) 5.302 * [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)))) 5.302 * * * * [progress]: [ 17 / 19 ] 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)))))> 5.302 * [simplify]: Simplifying (+.p16 x (real->posit16 1)) 5.302 * * [simplify]: iters left: 2 (4 enodes) 5.305 * * [simplify]: iters left: 1 (10 enodes) 5.309 * * [simplify]: Extracting #0: cost 1 inf + 0 5.309 * * [simplify]: Extracting #1: cost 3 inf + 0 5.309 * * [simplify]: Extracting #2: cost 3 inf + 1 5.309 * * [simplify]: Extracting #3: cost 0 inf + 45 5.309 * [simplify]: Simplified to (+.p16 (real->posit16 1) x) 5.309 * [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)))) 5.309 * * * * [progress]: [ 18 / 19 ] 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)))))> 5.310 * [simplify]: Simplifying (+.p16 x (real->posit16 1)) 5.310 * * [simplify]: iters left: 2 (4 enodes) 5.312 * * [simplify]: iters left: 1 (10 enodes) 5.316 * * [simplify]: Extracting #0: cost 1 inf + 0 5.316 * * [simplify]: Extracting #1: cost 3 inf + 0 5.316 * * [simplify]: Extracting #2: cost 3 inf + 1 5.316 * * [simplify]: Extracting #3: cost 0 inf + 45 5.316 * [simplify]: Simplified to (+.p16 (real->posit16 1) x) 5.316 * [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)))) 5.316 * * * * [progress]: [ 19 / 19 ] 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)))))> 5.317 * [simplify]: Simplifying (+.p16 x (real->posit16 1)) 5.317 * * [simplify]: iters left: 2 (4 enodes) 5.319 * * [simplify]: iters left: 1 (10 enodes) 5.322 * * [simplify]: Extracting #0: cost 1 inf + 0 5.322 * * [simplify]: Extracting #1: cost 3 inf + 0 5.322 * * [simplify]: Extracting #2: cost 3 inf + 1 5.322 * * [simplify]: Extracting #3: cost 0 inf + 45 5.322 * [simplify]: Simplified to (+.p16 (real->posit16 1) x) 5.322 * [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)))) 5.322 * * * [progress]: adding candidates to table 6.244 * * [progress]: iteration 4 / 4 6.244 * * * [progress]: picking best candidate 6.394 * * * * [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))))))> 6.394 * * * [progress]: localizing error 6.767 * * * [progress]: generating rewritten candidates 6.767 * * * * [progress]: [ 1 / 4 ] rewriting at (2) 6.794 * * * * [progress]: [ 2 / 4 ] rewriting at (2 2) 6.812 * * * * [progress]: [ 3 / 4 ] rewriting at (2 1) 6.815 * * * * [progress]: [ 4 / 4 ] rewriting at (2 2 2) 6.818 * * * [progress]: generating series expansions 6.818 * * * * [progress]: [ 1 / 4 ] generating series at (2) 6.818 * * * * [progress]: [ 2 / 4 ] generating series at (2 2) 6.818 * * * * [progress]: [ 3 / 4 ] generating series at (2 1) 6.818 * * * * [progress]: [ 4 / 4 ] generating series at (2 2 2) 6.818 * * * [progress]: simplifying candidates 6.818 * * * * [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)))))))> 6.818 * [simplify]: Simplifying (/.p16 (real->posit16 1) (+.p16 x (real->posit16 1))) 6.818 * * [simplify]: iters left: 3 (5 enodes) 6.822 * * [simplify]: iters left: 2 (11 enodes) 6.824 * * [simplify]: iters left: 1 (13 enodes) 6.827 * * [simplify]: Extracting #0: cost 1 inf + 0 6.827 * * [simplify]: Extracting #1: cost 3 inf + 0 6.827 * * [simplify]: Extracting #2: cost 5 inf + 0 6.827 * * [simplify]: Extracting #3: cost 3 inf + 2 6.827 * * [simplify]: Extracting #4: cost 0 inf + 527 6.827 * [simplify]: Simplified to (/.p16 (real->posit16 1) (+.p16 (real->posit16 1) x)) 6.827 * [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))))))) 6.827 * * * * [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)))))))> 6.828 * [simplify]: Simplifying (/.p16 (real->posit16 1) (+.p16 x (real->posit16 1))) 6.828 * * [simplify]: iters left: 3 (5 enodes) 6.829 * * [simplify]: iters left: 2 (11 enodes) 6.831 * * [simplify]: iters left: 1 (13 enodes) 6.834 * * [simplify]: Extracting #0: cost 1 inf + 0 6.834 * * [simplify]: Extracting #1: cost 3 inf + 0 6.834 * * [simplify]: Extracting #2: cost 5 inf + 0 6.834 * * [simplify]: Extracting #3: cost 3 inf + 2 6.834 * * [simplify]: Extracting #4: cost 0 inf + 527 6.834 * [simplify]: Simplified to (/.p16 (real->posit16 1) (+.p16 (real->posit16 1) x)) 6.834 * [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))))))) 6.834 * * * * [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))))> 6.834 * * * * [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)))))> 6.834 * [simplify]: Simplifying (-.p16 x (real->posit16 1)) 6.834 * * [simplify]: iters left: 2 (4 enodes) 6.835 * * [simplify]: iters left: 1 (16 enodes) 6.838 * * [simplify]: Extracting #0: cost 1 inf + 0 6.838 * * [simplify]: Extracting #1: cost 6 inf + 0 6.838 * * [simplify]: Extracting #2: cost 11 inf + 1 6.838 * * [simplify]: Extracting #3: cost 11 inf + 323 6.838 * * [simplify]: Extracting #4: cost 5 inf + 1491 6.838 * * [simplify]: Extracting #5: cost 1 inf + 3657 6.839 * * [simplify]: Extracting #6: cost 0 inf + 5019 6.839 * [simplify]: Simplified to (-.p16 x (real->posit16 1)) 6.839 * [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.839 * * * * [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.839 * [simplify]: Simplifying (real->posit16 1) 6.839 * * [simplify]: iters left: 1 (2 enodes) 6.840 * * [simplify]: Extracting #0: cost 1 inf + 0 6.840 * * [simplify]: Extracting #1: cost 2 inf + 0 6.840 * * [simplify]: Extracting #2: cost 1 inf + 1 6.840 * * [simplify]: Extracting #3: cost 0 inf + 2 6.840 * [simplify]: Simplified to (real->posit16 1) 6.840 * [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.840 * * * * [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.840 * [simplify]: Simplifying (+.p16 (*.p16 x x) (*.p16 (real->posit16 1) (real->posit16 1))) 6.840 * * [simplify]: iters left: 3 (6 enodes) 6.842 * * [simplify]: iters left: 2 (12 enodes) 6.844 * * [simplify]: iters left: 1 (14 enodes) 6.846 * * [simplify]: Extracting #0: cost 1 inf + 0 6.846 * * [simplify]: Extracting #1: cost 3 inf + 0 6.846 * * [simplify]: Extracting #2: cost 5 inf + 0 6.846 * * [simplify]: Extracting #3: cost 5 inf + 1 6.846 * * [simplify]: Extracting #4: cost 0 inf + 1327 6.846 * [simplify]: Simplified to (+.p16 (*.p16 (real->posit16 1) (real->posit16 1)) (*.p16 x x)) 6.846 * [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.846 * * * * [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.847 * [simplify]: Simplifying (/.p16 (real->posit16 1) (+.p16 x (real->posit16 1))) 6.847 * * [simplify]: iters left: 3 (5 enodes) 6.848 * * [simplify]: iters left: 2 (11 enodes) 6.850 * * [simplify]: iters left: 1 (13 enodes) 6.852 * * [simplify]: Extracting #0: cost 1 inf + 0 6.852 * * [simplify]: Extracting #1: cost 3 inf + 0 6.852 * * [simplify]: Extracting #2: cost 5 inf + 0 6.852 * * [simplify]: Extracting #3: cost 3 inf + 2 6.852 * * [simplify]: Extracting #4: cost 0 inf + 527 6.852 * [simplify]: Simplified to (/.p16 (real->posit16 1) (+.p16 (real->posit16 1) x)) 6.852 * [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.852 * [simplify]: Simplifying (/.p16 (+.p16 x (real->posit16 1)) (-.p16 x (real->posit16 1))) 6.852 * * [simplify]: iters left: 3 (6 enodes) 6.853 * * [simplify]: iters left: 2 (18 enodes) 6.856 * * [simplify]: iters left: 1 (31 enodes) 6.862 * * [simplify]: Extracting #0: cost 1 inf + 0 6.862 * * [simplify]: Extracting #1: cost 10 inf + 0 6.862 * * [simplify]: Extracting #2: cost 26 inf + 0 6.862 * * [simplify]: Extracting #3: cost 31 inf + 1 6.862 * * [simplify]: Extracting #4: cost 35 inf + 323 6.863 * * [simplify]: Extracting #5: cost 17 inf + 8069 6.864 * * [simplify]: Extracting #6: cost 0 inf + 25900 6.865 * [simplify]: Simplified to (/.p16 (+.p16 (real->posit16 1) x) (-.p16 x (real->posit16 1))) 6.865 * [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.865 * * * * [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.865 * * * * [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.865 * * * * [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.865 * [simplify]: Simplifying (+.p16 x (real->posit16 1)) 6.865 * * [simplify]: iters left: 2 (4 enodes) 6.866 * * [simplify]: iters left: 1 (10 enodes) 6.868 * * [simplify]: Extracting #0: cost 1 inf + 0 6.868 * * [simplify]: Extracting #1: cost 3 inf + 0 6.868 * * [simplify]: Extracting #2: cost 3 inf + 1 6.868 * * [simplify]: Extracting #3: cost 0 inf + 45 6.868 * [simplify]: Simplified to (+.p16 (real->posit16 1) x) 6.868 * [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.868 * [simplify]: Simplifying (-.p16 x (real->posit16 1)) 6.868 * * [simplify]: iters left: 2 (4 enodes) 6.869 * * [simplify]: iters left: 1 (16 enodes) 6.872 * * [simplify]: Extracting #0: cost 1 inf + 0 6.872 * * [simplify]: Extracting #1: cost 6 inf + 0 6.872 * * [simplify]: Extracting #2: cost 11 inf + 1 6.872 * * [simplify]: Extracting #3: cost 11 inf + 323 6.872 * * [simplify]: Extracting #4: cost 5 inf + 1491 6.872 * * [simplify]: Extracting #5: cost 1 inf + 3657 6.872 * * [simplify]: Extracting #6: cost 0 inf + 5019 6.873 * [simplify]: Simplified to (-.p16 x (real->posit16 1)) 6.873 * [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.873 * * * * [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.873 * * * * [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.873 * * * * [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.873 * [simplify]: Simplifying (*.p16 (real->posit16 1) (+.p16 x (real->posit16 1))) 6.873 * * [simplify]: iters left: 3 (5 enodes) 6.874 * * [simplify]: iters left: 2 (17 enodes) 6.877 * * [simplify]: iters left: 1 (21 enodes) 6.880 * * [simplify]: Extracting #0: cost 1 inf + 0 6.880 * * [simplify]: Extracting #1: cost 5 inf + 0 6.880 * * [simplify]: Extracting #2: cost 7 inf + 0 6.880 * * [simplify]: Extracting #3: cost 5 inf + 2 6.880 * * [simplify]: Extracting #4: cost 0 inf + 1050 6.880 * [simplify]: Simplified to (*.p16 (real->posit16 1) (+.p16 (real->posit16 1) x)) 6.880 * [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.880 * * * * [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.880 * [simplify]: Simplifying (*.p16 (real->posit16 1) (+.p16 x (real->posit16 1))) 6.880 * * [simplify]: iters left: 3 (5 enodes) 6.882 * * [simplify]: iters left: 2 (17 enodes) 6.885 * * [simplify]: iters left: 1 (21 enodes) 6.887 * * [simplify]: Extracting #0: cost 1 inf + 0 6.887 * * [simplify]: Extracting #1: cost 5 inf + 0 6.887 * * [simplify]: Extracting #2: cost 7 inf + 0 6.888 * * [simplify]: Extracting #3: cost 5 inf + 2 6.888 * * [simplify]: Extracting #4: cost 0 inf + 1050 6.888 * [simplify]: Simplified to (*.p16 (real->posit16 1) (+.p16 (real->posit16 1) x)) 6.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 (*.p16 (real->posit16 1) (+.p16 (real->posit16 1) x)) (-.p16 (*.p16 x x) (*.p16 (real->posit16 1) (real->posit16 1)))))) 6.888 * * * * [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.888 * [simplify]: Simplifying (*.p16 (real->posit16 1) (+.p16 x (real->posit16 1))) 6.888 * * [simplify]: iters left: 3 (5 enodes) 6.891 * * [simplify]: iters left: 2 (17 enodes) 6.894 * * [simplify]: iters left: 1 (21 enodes) 6.896 * * [simplify]: Extracting #0: cost 1 inf + 0 6.896 * * [simplify]: Extracting #1: cost 5 inf + 0 6.897 * * [simplify]: Extracting #2: cost 7 inf + 0 6.897 * * [simplify]: Extracting #3: cost 5 inf + 2 6.897 * * [simplify]: Extracting #4: cost 0 inf + 1050 6.897 * [simplify]: Simplified to (*.p16 (real->posit16 1) (+.p16 (real->posit16 1) x)) 6.897 * [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.897 * * * * [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.897 * [simplify]: Simplifying (*.p16 (real->posit16 1) (+.p16 x (real->posit16 1))) 6.897 * * [simplify]: iters left: 3 (5 enodes) 6.898 * * [simplify]: iters left: 2 (17 enodes) 6.901 * * [simplify]: iters left: 1 (21 enodes) 6.904 * * [simplify]: Extracting #0: cost 1 inf + 0 6.904 * * [simplify]: Extracting #1: cost 5 inf + 0 6.904 * * [simplify]: Extracting #2: cost 7 inf + 0 6.904 * * [simplify]: Extracting #3: cost 5 inf + 2 6.904 * * [simplify]: Extracting #4: cost 0 inf + 1050 6.904 * [simplify]: Simplified to (*.p16 (real->posit16 1) (+.p16 (real->posit16 1) x)) 6.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 x) (*.p16 (real->posit16 1) (real->posit16 1)))))) 6.904 * * * [progress]: adding candidates to table 7.426 * [progress]: [Phase 3 of 3] Extracting. 7.426 * * [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 (*.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 (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 (real->posit16 1) (-.p16 x (real->posit16 1)))))> #posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (real->posit16 2) x)) (*.p16 (/.p16 (real->posit16 1) (*.p16 (+.p16 x (real->posit16 1)) (-.p16 x (real->posit16 1)))) (+.p16 x (real->posit16 1)))))> #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)))))))> #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))))))> #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 (*.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))))))> #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))))>) 7.428 * * * [regime-changes]: Trying 1 branch expressions: (x) 7.428 * * * * [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 (*.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 (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 (real->posit16 1) (-.p16 x (real->posit16 1)))))> #posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (real->posit16 2) x)) (*.p16 (/.p16 (real->posit16 1) (*.p16 (+.p16 x (real->posit16 1)) (-.p16 x (real->posit16 1)))) (+.p16 x (real->posit16 1)))))> #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)))))))> #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))))))> #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 (*.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))))))> #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))))>) 7.623 * * * [regime]: Found split indices: #