0.002 * [progress]: [Phase 1 of 3] Setting up. 0.002 * * * [progress]: [1/2] Preparing points 0.004 * * * * [points]: Sampling 256 additional inputs, on iter 0 have 0 / 256 0.006 * * * * [points]: Computing exacts on every 16 of 256 points to ramp up precision 0.012 * * * * [points]: Setting MPFR precision to 64 0.015 * * * * [points]: Setting MPFR precision to 320 0.016 * * * * [points]: Computing exacts on every 8 of 256 points to ramp up precision 0.023 * * * * [points]: Setting MPFR precision to 64 0.026 * * * * [points]: Setting MPFR precision to 320 0.028 * * * * [points]: Computing exacts on every 4 of 256 points to ramp up precision 0.032 * * * * [points]: Setting MPFR precision to 64 0.036 * * * * [points]: Setting MPFR precision to 320 0.040 * * * * [points]: Computing exacts on every 2 of 256 points to ramp up precision 0.046 * * * * [points]: Setting MPFR precision to 64 0.056 * * * * [points]: Setting MPFR precision to 320 0.065 * * * * [points]: Computing exacts for 256 points 0.072 * * * * [points]: Setting MPFR precision to 64 0.114 * * * * [points]: Setting MPFR precision to 320 0.138 * * * * [points]: Filtering points with unrepresentable outputs 0.138 * * * * [points]: Sampling 218 additional inputs, on iter 1 have 38 / 256 0.139 * * * * [points]: Computing exacts on every 13 of 218 points to ramp up precision 0.144 * * * * [points]: Setting MPFR precision to 64 0.146 * * * * [points]: Setting MPFR precision to 320 0.147 * * * * [points]: Computing exacts on every 6 of 218 points to ramp up precision 0.154 * * * * [points]: Setting MPFR precision to 64 0.157 * * * * [points]: Setting MPFR precision to 320 0.161 * * * * [points]: Computing exacts on every 3 of 218 points to ramp up precision 0.168 * * * * [points]: Setting MPFR precision to 64 0.173 * * * * [points]: Setting MPFR precision to 320 0.179 * * * * [points]: Computing exacts for 218 points 0.186 * * * * [points]: Setting MPFR precision to 64 0.208 * * * * [points]: Setting MPFR precision to 320 0.224 * * * * [points]: Filtering points with unrepresentable outputs 0.224 * * * * [points]: Sampling 187 additional inputs, on iter 2 have 69 / 256 0.225 * * * * [points]: Computing exacts on every 11 of 187 points to ramp up precision 0.252 * * * * [points]: Setting MPFR precision to 64 0.253 * * * * [points]: Setting MPFR precision to 320 0.254 * * * * [points]: Computing exacts on every 5 of 187 points to ramp up precision 0.262 * * * * [points]: Setting MPFR precision to 64 0.265 * * * * [points]: Setting MPFR precision to 320 0.269 * * * * [points]: Computing exacts on every 2 of 187 points to ramp up precision 0.275 * * * * [points]: Setting MPFR precision to 64 0.282 * * * * [points]: Setting MPFR precision to 320 0.288 * * * * [points]: Computing exacts for 187 points 0.295 * * * * [points]: Setting MPFR precision to 64 0.311 * * * * [points]: Setting MPFR precision to 320 0.324 * * * * [points]: Filtering points with unrepresentable outputs 0.324 * * * * [points]: Sampling 165 additional inputs, on iter 3 have 91 / 256 0.325 * * * * [points]: Computing exacts on every 10 of 165 points to ramp up precision 0.332 * * * * [points]: Setting MPFR precision to 64 0.334 * * * * [points]: Setting MPFR precision to 320 0.335 * * * * [points]: Computing exacts on every 5 of 165 points to ramp up precision 0.340 * * * * [points]: Setting MPFR precision to 64 0.342 * * * * [points]: Setting MPFR precision to 320 0.344 * * * * [points]: Computing exacts on every 2 of 165 points to ramp up precision 0.350 * * * * [points]: Setting MPFR precision to 64 0.377 * * * * [points]: Setting MPFR precision to 320 0.384 * * * * [points]: Computing exacts for 165 points 0.389 * * * * [points]: Setting MPFR precision to 64 0.402 * * * * [points]: Setting MPFR precision to 320 0.419 * * * * [points]: Filtering points with unrepresentable outputs 0.419 * * * * [points]: Sampling 145 additional inputs, on iter 4 have 111 / 256 0.420 * * * * [points]: Computing exacts on every 9 of 145 points to ramp up precision 0.426 * * * * [points]: Setting MPFR precision to 64 0.428 * * * * [points]: Setting MPFR precision to 320 0.429 * * * * [points]: Computing exacts on every 4 of 145 points to ramp up precision 0.436 * * * * [points]: Setting MPFR precision to 64 0.439 * * * * [points]: Setting MPFR precision to 320 0.442 * * * * [points]: Computing exacts on every 2 of 145 points to ramp up precision 0.449 * * * * [points]: Setting MPFR precision to 64 0.454 * * * * [points]: Setting MPFR precision to 320 0.460 * * * * [points]: Computing exacts for 145 points 0.466 * * * * [points]: Setting MPFR precision to 64 0.480 * * * * [points]: Setting MPFR precision to 320 0.509 * * * * [points]: Filtering points with unrepresentable outputs 0.510 * * * * [points]: Sampling 119 additional inputs, on iter 5 have 137 / 256 0.510 * * * * [points]: Computing exacts on every 7 of 119 points to ramp up precision 0.515 * * * * [points]: Setting MPFR precision to 64 0.516 * * * * [points]: Setting MPFR precision to 320 0.517 * * * * [points]: Computing exacts on every 3 of 119 points to ramp up precision 0.523 * * * * [points]: Setting MPFR precision to 64 0.525 * * * * [points]: Setting MPFR precision to 320 0.527 * * * * [points]: Computing exacts for 119 points 0.532 * * * * [points]: Setting MPFR precision to 64 0.543 * * * * [points]: Setting MPFR precision to 320 0.555 * * * * [points]: Filtering points with unrepresentable outputs 0.555 * * * * [points]: Sampling 110 additional inputs, on iter 6 have 146 / 256 0.556 * * * * [points]: Computing exacts on every 6 of 110 points to ramp up precision 0.562 * * * * [points]: Setting MPFR precision to 64 0.563 * * * * [points]: Setting MPFR precision to 320 0.565 * * * * [points]: Computing exacts on every 3 of 110 points to ramp up precision 0.572 * * * * [points]: Setting MPFR precision to 64 0.574 * * * * [points]: Setting MPFR precision to 320 0.577 * * * * [points]: Computing exacts for 110 points 0.584 * * * * [points]: Setting MPFR precision to 64 0.596 * * * * [points]: Setting MPFR precision to 320 0.608 * * * * [points]: Filtering points with unrepresentable outputs 0.608 * * * * [points]: Sampling 86 additional inputs, on iter 7 have 170 / 256 0.609 * * * * [points]: Computing exacts on every 5 of 86 points to ramp up precision 0.615 * * * * [points]: Setting MPFR precision to 64 0.637 * * * * [points]: Setting MPFR precision to 320 0.639 * * * * [points]: Computing exacts on every 2 of 86 points to ramp up precision 0.648 * * * * [points]: Setting MPFR precision to 64 0.651 * * * * [points]: Setting MPFR precision to 320 0.654 * * * * [points]: Computing exacts for 86 points 0.661 * * * * [points]: Setting MPFR precision to 64 0.670 * * * * [points]: Setting MPFR precision to 320 0.679 * * * * [points]: Filtering points with unrepresentable outputs 0.679 * * * * [points]: Sampling 71 additional inputs, on iter 8 have 185 / 256 0.680 * * * * [points]: Computing exacts on every 4 of 71 points to ramp up precision 0.686 * * * * [points]: Setting MPFR precision to 64 0.688 * * * * [points]: Setting MPFR precision to 320 0.690 * * * * [points]: Computing exacts on every 2 of 71 points to ramp up precision 0.696 * * * * [points]: Setting MPFR precision to 64 0.699 * * * * [points]: Setting MPFR precision to 320 0.701 * * * * [points]: Computing exacts for 71 points 0.708 * * * * [points]: Setting MPFR precision to 64 0.715 * * * * [points]: Setting MPFR precision to 320 0.723 * * * * [points]: Filtering points with unrepresentable outputs 0.723 * * * * [points]: Sampling 60 additional inputs, on iter 9 have 196 / 256 0.723 * * * * [points]: Computing exacts on every 3 of 60 points to ramp up precision 0.730 * * * * [points]: Setting MPFR precision to 64 0.732 * * * * [points]: Setting MPFR precision to 320 0.733 * * * * [points]: Computing exacts for 60 points 0.740 * * * * [points]: Setting MPFR precision to 64 0.746 * * * * [points]: Setting MPFR precision to 320 0.753 * * * * [points]: Filtering points with unrepresentable outputs 0.753 * * * * [points]: Sampling 52 additional inputs, on iter 10 have 204 / 256 0.753 * * * * [points]: Computing exacts on every 3 of 52 points to ramp up precision 0.774 * * * * [points]: Setting MPFR precision to 64 0.775 * * * * [points]: Setting MPFR precision to 320 0.776 * * * * [points]: Computing exacts for 52 points 0.782 * * * * [points]: Setting MPFR precision to 64 0.786 * * * * [points]: Setting MPFR precision to 320 0.790 * * * * [points]: Filtering points with unrepresentable outputs 0.790 * * * * [points]: Sampling 45 additional inputs, on iter 11 have 211 / 256 0.790 * * * * [points]: Computing exacts on every 2 of 45 points to ramp up precision 0.794 * * * * [points]: Setting MPFR precision to 64 0.795 * * * * [points]: Setting MPFR precision to 320 0.797 * * * * [points]: Computing exacts for 45 points 0.801 * * * * [points]: Setting MPFR precision to 64 0.804 * * * * [points]: Setting MPFR precision to 320 0.807 * * * * [points]: Filtering points with unrepresentable outputs 0.807 * * * * [points]: Sampling 41 additional inputs, on iter 12 have 215 / 256 0.808 * * * * [points]: Computing exacts on every 2 of 41 points to ramp up precision 0.812 * * * * [points]: Setting MPFR precision to 64 0.813 * * * * [points]: Setting MPFR precision to 320 0.814 * * * * [points]: Computing exacts for 41 points 0.818 * * * * [points]: Setting MPFR precision to 64 0.822 * * * * [points]: Setting MPFR precision to 320 0.824 * * * * [points]: Filtering points with unrepresentable outputs 0.824 * * * * [points]: Sampling 36 additional inputs, on iter 13 have 220 / 256 0.825 * * * * [points]: Computing exacts on every 2 of 36 points to ramp up precision 0.829 * * * * [points]: Setting MPFR precision to 64 0.830 * * * * [points]: Setting MPFR precision to 320 0.831 * * * * [points]: Computing exacts for 36 points 0.835 * * * * [points]: Setting MPFR precision to 64 0.838 * * * * [points]: Setting MPFR precision to 320 0.840 * * * * [points]: Filtering points with unrepresentable outputs 0.840 * * * * [points]: Sampling 31 additional inputs, on iter 14 have 225 / 256 0.840 * * * * [points]: Computing exacts for 31 points 0.859 * * * * [points]: Setting MPFR precision to 64 0.863 * * * * [points]: Setting MPFR precision to 320 0.865 * * * * [points]: Filtering points with unrepresentable outputs 0.865 * * * * [points]: Sampling 27 additional inputs, on iter 15 have 229 / 256 0.865 * * * * [points]: Computing exacts for 27 points 0.870 * * * * [points]: Setting MPFR precision to 64 0.872 * * * * [points]: Setting MPFR precision to 320 0.874 * * * * [points]: Filtering points with unrepresentable outputs 0.874 * * * * [points]: Sampling 23 additional inputs, on iter 16 have 233 / 256 0.874 * * * * [points]: Computing exacts for 23 points 0.878 * * * * [points]: Setting MPFR precision to 64 0.880 * * * * [points]: Setting MPFR precision to 320 0.882 * * * * [points]: Filtering points with unrepresentable outputs 0.882 * * * * [points]: Sampling 16 additional inputs, on iter 17 have 240 / 256 0.882 * * * * [points]: Computing exacts for 16 points 0.886 * * * * [points]: Setting MPFR precision to 64 0.887 * * * * [points]: Setting MPFR precision to 320 0.889 * * * * [points]: Filtering points with unrepresentable outputs 0.889 * * * * [points]: Sampling 14 additional inputs, on iter 18 have 242 / 256 0.889 * * * * [points]: Computing exacts for 14 points 0.894 * * * * [points]: Setting MPFR precision to 64 0.896 * * * * [points]: Setting MPFR precision to 320 0.897 * * * * [points]: Filtering points with unrepresentable outputs 0.897 * * * * [points]: Sampling 12 additional inputs, on iter 19 have 244 / 256 0.897 * * * * [points]: Computing exacts for 12 points 0.902 * * * * [points]: Setting MPFR precision to 64 0.903 * * * * [points]: Setting MPFR precision to 320 0.904 * * * * [points]: Filtering points with unrepresentable outputs 0.904 * * * * [points]: Sampling 11 additional inputs, on iter 20 have 245 / 256 0.904 * * * * [points]: Computing exacts for 11 points 0.908 * * * * [points]: Setting MPFR precision to 64 0.909 * * * * [points]: Setting MPFR precision to 320 0.910 * * * * [points]: Filtering points with unrepresentable outputs 0.910 * * * * [points]: Sampling 9 additional inputs, on iter 21 have 247 / 256 0.910 * * * * [points]: Computing exacts for 9 points 0.915 * * * * [points]: Setting MPFR precision to 64 0.915 * * * * [points]: Setting MPFR precision to 320 0.916 * * * * [points]: Filtering points with unrepresentable outputs 0.916 * * * * [points]: Sampling 7 additional inputs, on iter 22 have 249 / 256 0.916 * * * * [points]: Computing exacts for 7 points 0.921 * * * * [points]: Setting MPFR precision to 64 0.921 * * * * [points]: Setting MPFR precision to 320 0.922 * * * * [points]: Filtering points with unrepresentable outputs 0.922 * * * * [points]: Sampling 6 additional inputs, on iter 23 have 250 / 256 0.922 * * * * [points]: Computing exacts for 6 points 0.926 * * * * [points]: Setting MPFR precision to 64 0.927 * * * * [points]: Setting MPFR precision to 320 0.927 * * * * [points]: Filtering points with unrepresentable outputs 0.927 * * * * [points]: Sampling 5 additional inputs, on iter 24 have 251 / 256 0.927 * * * * [points]: Computing exacts for 5 points 0.945 * * * * [points]: Setting MPFR precision to 64 0.946 * * * * [points]: Setting MPFR precision to 320 0.946 * * * * [points]: Filtering points with unrepresentable outputs 0.946 * * * * [points]: Sampling 4 additional inputs, on iter 25 have 252 / 256 0.946 * * * * [points]: Computing exacts for 4 points 0.953 * * * * [points]: Setting MPFR precision to 64 0.954 * * * * [points]: Setting MPFR precision to 320 0.954 * * * * [points]: Filtering points with unrepresentable outputs 0.954 * * * * [points]: Sampling 4 additional inputs, on iter 26 have 252 / 256 0.954 * * * * [points]: Computing exacts for 4 points 0.960 * * * * [points]: Setting MPFR precision to 64 0.961 * * * * [points]: Setting MPFR precision to 320 0.962 * * * * [points]: Filtering points with unrepresentable outputs 0.962 * * * * [points]: Sampling 4 additional inputs, on iter 27 have 254 / 256 0.962 * * * * [points]: Computing exacts for 4 points 0.968 * * * * [points]: Setting MPFR precision to 64 0.969 * * * * [points]: Setting MPFR precision to 320 0.969 * * * * [points]: Filtering points with unrepresentable outputs 0.969 * * * * [points]: Sampling 4 additional inputs, on iter 28 have 254 / 256 0.969 * * * * [points]: Computing exacts for 4 points 0.976 * * * * [points]: Setting MPFR precision to 64 0.976 * * * * [points]: Setting MPFR precision to 320 0.977 * * * * [points]: Filtering points with unrepresentable outputs 0.977 * * * * [points]: Sampling 4 additional inputs, on iter 29 have 255 / 256 0.977 * * * * [points]: Computing exacts for 4 points 0.983 * * * * [points]: Setting MPFR precision to 64 0.984 * * * * [points]: Setting MPFR precision to 320 0.984 * * * * [points]: Filtering points with unrepresentable outputs 0.984 * * * * [points]: Sampling 4 additional inputs, on iter 30 have 255 / 256 0.984 * * * * [points]: Computing exacts for 4 points 0.991 * * * * [points]: Setting MPFR precision to 64 0.991 * * * * [points]: Setting MPFR precision to 320 0.992 * * * * [points]: Filtering points with unrepresentable outputs 0.992 * * * * [points]: Sampling 4 additional inputs, on iter 31 have 255 / 256 0.992 * * * * [points]: Computing exacts for 4 points 0.998 * * * * [points]: Setting MPFR precision to 64 0.999 * * * * [points]: Setting MPFR precision to 320 0.999 * * * * [points]: Filtering points with unrepresentable outputs 0.999 * * * * [points]: Sampling 4 additional inputs, on iter 32 have 255 / 256 0.999 * * * * [points]: Computing exacts for 4 points 1.006 * * * * [points]: Setting MPFR precision to 64 1.006 * * * * [points]: Setting MPFR precision to 320 1.007 * * * * [points]: Filtering points with unrepresentable outputs 1.007 * * * * [points]: Sampled 257 points with exact outputs 1.007 * * * [progress]: [2/2] Setting up program. 1.028 * [progress]: [Phase 2 of 3] Improving. 1.028 * * * * [progress]: [ 1 / 1 ] simplifiying candidate #posit16 2) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)))) (-.p16 (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i))) (real->posit16 1.0))))> 1.028 * [simplify]: Simplifying (/.p16 (/.p16 (*.p16 (*.p16 i (+.p16 (+.p16 alpha beta) i)) (+.p16 (*.p16 beta alpha) (*.p16 i (+.p16 (+.p16 alpha beta) i)))) (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)))) (-.p16 (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i))) (real->posit16 1.0))) 1.029 * * [simplify]: iters left: 6 (19 enodes) 1.035 * * [simplify]: iters left: 5 (76 enodes) 1.075 * * [simplify]: iters left: 4 (344 enodes) 1.296 * * [simplify]: Extracting #0: cost 1 inf + 0 1.297 * * [simplify]: Extracting #1: cost 75 inf + 0 1.298 * * [simplify]: Extracting #2: cost 474 inf + 1 1.303 * * [simplify]: Extracting #3: cost 741 inf + 26817 1.314 * * [simplify]: Extracting #4: cost 682 inf + 140740 1.325 * * [simplify]: Extracting #5: cost 610 inf + 190036 1.342 * * [simplify]: Extracting #6: cost 582 inf + 205163 1.369 * * [simplify]: Extracting #7: cost 359 inf + 459086 1.419 * * [simplify]: Extracting #8: cost 52 inf + 926046 1.479 * * [simplify]: Extracting #9: cost 0 inf + 1027849 1.541 * * [simplify]: Extracting #10: cost 0 inf + 1026329 1.617 * [simplify]: Simplified to (/.p16 (*.p16 (*.p16 i (+.p16 i (+.p16 alpha beta))) (+.p16 (*.p16 beta alpha) (*.p16 i (+.p16 i (+.p16 alpha beta))))) (*.p16 (*.p16 (+.p16 beta (+.p16 (*.p16 (real->posit16 2) i) alpha)) (+.p16 beta (+.p16 (*.p16 (real->posit16 2) i) alpha))) (-.p16 (*.p16 (+.p16 beta (+.p16 (*.p16 (real->posit16 2) i) alpha)) (+.p16 beta (+.p16 (*.p16 (real->posit16 2) i) alpha))) (real->posit16 1.0)))) 1.617 * [simplify]: Simplified (2) to (λ (alpha beta i) (/.p16 (*.p16 (*.p16 i (+.p16 i (+.p16 alpha beta))) (+.p16 (*.p16 beta alpha) (*.p16 i (+.p16 i (+.p16 alpha beta))))) (*.p16 (*.p16 (+.p16 beta (+.p16 (*.p16 (real->posit16 2) i) alpha)) (+.p16 beta (+.p16 (*.p16 (real->posit16 2) i) alpha))) (-.p16 (*.p16 (+.p16 beta (+.p16 (*.p16 (real->posit16 2) i) alpha)) (+.p16 beta (+.p16 (*.p16 (real->posit16 2) i) alpha))) (real->posit16 1.0))))) 1.648 * * [progress]: iteration 1 / 4 1.649 * * * [progress]: picking best candidate 1.678 * * * * [pick]: Picked #posit16 2) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)))) (-.p16 (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i))) (real->posit16 1.0))))> 1.678 * * * [progress]: localizing error 2.029 * * * [progress]: generating rewritten candidates 2.029 * * * * [progress]: [ 1 / 4 ] rewriting at (2 1) 2.038 * * * * [progress]: [ 2 / 4 ] rewriting at (2) 2.056 * * * * [progress]: [ 3 / 4 ] rewriting at (2 1 1 2) 2.062 * * * * [progress]: [ 4 / 4 ] rewriting at (2 2 1 2) 2.076 * * * [progress]: generating series expansions 2.076 * * * * [progress]: [ 1 / 4 ] generating series at (2 1) 2.076 * * * * [progress]: [ 2 / 4 ] generating series at (2) 2.076 * * * * [progress]: [ 3 / 4 ] generating series at (2 1 1 2) 2.076 * * * * [progress]: [ 4 / 4 ] generating series at (2 2 1 2) 2.076 * * * [progress]: simplifying candidates 2.076 * * * * [progress]: [ 1 / 17 ] simplifiying candidate #posit16 2) i))) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i))) (-.p16 (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i))) (real->posit16 1.0))))> 2.076 * [simplify]: Simplifying (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) 2.076 * * [simplify]: iters left: 3 (8 enodes) 2.078 * * [simplify]: iters left: 2 (20 enodes) 2.081 * * [simplify]: iters left: 1 (26 enodes) 2.085 * * [simplify]: Extracting #0: cost 1 inf + 0 2.085 * * [simplify]: Extracting #1: cost 7 inf + 0 2.085 * * [simplify]: Extracting #2: cost 7 inf + 2 2.085 * * [simplify]: Extracting #3: cost 6 inf + 45 2.085 * * [simplify]: Extracting #4: cost 4 inf + 47 2.085 * * [simplify]: Extracting #5: cost 1 inf + 1136 2.086 * * [simplify]: Extracting #6: cost 0 inf + 1499 2.086 * [simplify]: Simplified to (+.p16 (+.p16 beta alpha) (*.p16 (real->posit16 2) i)) 2.086 * [simplify]: Simplified (2 1 2) to (λ (alpha beta i) (/.p16 (/.p16 (/.p16 (*.p16 (*.p16 i (+.p16 (+.p16 alpha beta) i)) (+.p16 (*.p16 beta alpha) (*.p16 i (+.p16 (+.p16 alpha beta) i)))) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i))) (+.p16 (+.p16 beta alpha) (*.p16 (real->posit16 2) i))) (-.p16 (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i))) (real->posit16 1.0)))) 2.086 * * * * [progress]: [ 2 / 17 ] simplifiying candidate #posit16 2) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i))) (+.p16 (*.p16 beta alpha) (*.p16 i (+.p16 (+.p16 alpha beta) i))))) (-.p16 (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i))) (real->posit16 1.0))))> 2.086 * [simplify]: Simplifying (*.p16 i (+.p16 (+.p16 alpha beta) i)) 2.086 * * [simplify]: iters left: 3 (6 enodes) 2.087 * * [simplify]: iters left: 2 (22 enodes) 2.091 * * [simplify]: iters left: 1 (42 enodes) 2.099 * * [simplify]: Extracting #0: cost 1 inf + 0 2.099 * * [simplify]: Extracting #1: cost 12 inf + 0 2.099 * * [simplify]: Extracting #2: cost 16 inf + 1 2.099 * * [simplify]: Extracting #3: cost 9 inf + 1412 2.100 * * [simplify]: Extracting #4: cost 0 inf + 4393 2.100 * [simplify]: Simplified to (*.p16 i (+.p16 i (+.p16 alpha beta))) 2.100 * [simplify]: Simplified (2 1 1) to (λ (alpha beta i) (/.p16 (/.p16 (*.p16 i (+.p16 i (+.p16 alpha beta))) (/.p16 (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i))) (+.p16 (*.p16 beta alpha) (*.p16 i (+.p16 (+.p16 alpha beta) i))))) (-.p16 (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i))) (real->posit16 1.0)))) 2.100 * * * * [progress]: [ 3 / 17 ] simplifiying candidate #posit16 2) i))) (/.p16 (+.p16 (*.p16 beta alpha) (*.p16 i (+.p16 (+.p16 alpha beta) i))) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)))) (-.p16 (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i))) (real->posit16 1.0))))> 2.100 * [simplify]: Simplifying (/.p16 (*.p16 i (+.p16 (+.p16 alpha beta) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i))) 2.100 * * [simplify]: iters left: 4 (11 enodes) 2.104 * * [simplify]: iters left: 3 (34 enodes) 2.113 * * [simplify]: iters left: 2 (62 enodes) 2.130 * * [simplify]: iters left: 1 (116 enodes) 2.165 * * [simplify]: Extracting #0: cost 1 inf + 0 2.165 * * [simplify]: Extracting #1: cost 18 inf + 0 2.165 * * [simplify]: Extracting #2: cost 32 inf + 1 2.166 * * [simplify]: Extracting #3: cost 28 inf + 688 2.166 * * [simplify]: Extracting #4: cost 20 inf + 2471 2.167 * * [simplify]: Extracting #5: cost 11 inf + 5213 2.169 * * [simplify]: Extracting #6: cost 0 inf + 16616 2.171 * [simplify]: Simplified to (*.p16 (/.p16 i (+.p16 beta (+.p16 (*.p16 (real->posit16 2) i) alpha))) (+.p16 (+.p16 alpha i) beta)) 2.171 * [simplify]: Simplified (2 1 1) to (λ (alpha beta i) (/.p16 (*.p16 (*.p16 (/.p16 i (+.p16 beta (+.p16 (*.p16 (real->posit16 2) i) alpha))) (+.p16 (+.p16 alpha i) beta)) (/.p16 (+.p16 (*.p16 beta alpha) (*.p16 i (+.p16 (+.p16 alpha beta) i))) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)))) (-.p16 (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i))) (real->posit16 1.0)))) 2.172 * [simplify]: Simplifying (/.p16 (+.p16 (*.p16 beta alpha) (*.p16 i (+.p16 (+.p16 alpha beta) i))) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i))) 2.172 * * [simplify]: iters left: 5 (13 enodes) 2.177 * * [simplify]: iters left: 4 (36 enodes) 2.188 * * [simplify]: iters left: 3 (69 enodes) 2.207 * * [simplify]: iters left: 2 (108 enodes) 2.229 * * [simplify]: iters left: 1 (142 enodes) 2.255 * * [simplify]: Extracting #0: cost 1 inf + 0 2.255 * * [simplify]: Extracting #1: cost 3 inf + 0 2.255 * * [simplify]: Extracting #2: cost 25 inf + 0 2.255 * * [simplify]: Extracting #3: cost 26 inf + 2 2.255 * * [simplify]: Extracting #4: cost 20 inf + 1217 2.256 * * [simplify]: Extracting #5: cost 5 inf + 6972 2.257 * * [simplify]: Extracting #6: cost 0 inf + 9668 2.259 * [simplify]: Simplified to (/.p16 (*.p16 (+.p16 beta i) (+.p16 i alpha)) (+.p16 (*.p16 (real->posit16 2) i) (+.p16 alpha beta))) 2.259 * [simplify]: Simplified (2 1 2) to (λ (alpha beta i) (/.p16 (*.p16 (/.p16 (*.p16 i (+.p16 (+.p16 alpha beta) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i))) (/.p16 (*.p16 (+.p16 beta i) (+.p16 i alpha)) (+.p16 (*.p16 (real->posit16 2) i) (+.p16 alpha beta)))) (-.p16 (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i))) (real->posit16 1.0)))) 2.259 * * * * [progress]: [ 4 / 17 ] simplifiying candidate #posit16 2) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)))) (+.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (real->posit16 1.0))) (-.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (real->posit16 1.0))))> 2.259 * [simplify]: Simplifying (-.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (real->posit16 1.0)) 2.259 * * [simplify]: iters left: 4 (11 enodes) 2.263 * * [simplify]: iters left: 3 (33 enodes) 2.273 * * [simplify]: iters left: 2 (87 enodes) 2.303 * * [simplify]: iters left: 1 (455 enodes) 2.856 * * [simplify]: Extracting #0: cost 1 inf + 0 2.856 * * [simplify]: Extracting #1: cost 41 inf + 0 2.857 * * [simplify]: Extracting #2: cost 340 inf + 2 2.862 * * [simplify]: Extracting #3: cost 944 inf + 2428 2.871 * * [simplify]: Extracting #4: cost 917 inf + 30276 2.894 * * [simplify]: Extracting #5: cost 642 inf + 234865 2.982 * * [simplify]: Extracting #6: cost 130 inf + 773963 3.074 * * [simplify]: Extracting #7: cost 0 inf + 938356 3.167 * [simplify]: Simplified to (+.p16 (-.p16 (+.p16 beta alpha) (real->posit16 1.0)) (*.p16 (real->posit16 2) i)) 3.167 * [simplify]: Simplified (2 2) to (λ (alpha beta i) (/.p16 (/.p16 (/.p16 (*.p16 (*.p16 i (+.p16 (+.p16 alpha beta) i)) (+.p16 (*.p16 beta alpha) (*.p16 i (+.p16 (+.p16 alpha beta) i)))) (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)))) (+.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (real->posit16 1.0))) (+.p16 (-.p16 (+.p16 beta alpha) (real->posit16 1.0)) (*.p16 (real->posit16 2) i)))) 3.168 * * * * [progress]: [ 5 / 17 ] simplifiying candidate #posit16 2) i))) (/.p16 (-.p16 (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i))) (real->posit16 1.0)) (/.p16 (+.p16 (*.p16 beta alpha) (*.p16 i (+.p16 (+.p16 alpha beta) i))) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i))))))> 3.168 * [simplify]: Simplifying (/.p16 (*.p16 i (+.p16 (+.p16 alpha beta) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i))) 3.168 * * [simplify]: iters left: 4 (11 enodes) 3.171 * * [simplify]: iters left: 3 (34 enodes) 3.176 * * [simplify]: iters left: 2 (62 enodes) 3.187 * * [simplify]: iters left: 1 (116 enodes) 3.206 * * [simplify]: Extracting #0: cost 1 inf + 0 3.206 * * [simplify]: Extracting #1: cost 18 inf + 0 3.207 * * [simplify]: Extracting #2: cost 32 inf + 1 3.207 * * [simplify]: Extracting #3: cost 28 inf + 688 3.207 * * [simplify]: Extracting #4: cost 20 inf + 2471 3.207 * * [simplify]: Extracting #5: cost 11 inf + 5213 3.208 * * [simplify]: Extracting #6: cost 0 inf + 16616 3.210 * [simplify]: Simplified to (*.p16 (/.p16 i (+.p16 beta (+.p16 (*.p16 (real->posit16 2) i) alpha))) (+.p16 (+.p16 alpha i) beta)) 3.210 * [simplify]: Simplified (2 1) to (λ (alpha beta i) (/.p16 (*.p16 (/.p16 i (+.p16 beta (+.p16 (*.p16 (real->posit16 2) i) alpha))) (+.p16 (+.p16 alpha i) beta)) (/.p16 (-.p16 (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i))) (real->posit16 1.0)) (/.p16 (+.p16 (*.p16 beta alpha) (*.p16 i (+.p16 (+.p16 alpha beta) i))) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)))))) 3.210 * * * * [progress]: [ 6 / 17 ] simplifiying candidate #posit16 2) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)))) (-.p16 (*.p16 (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i))) (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)))) (*.p16 (real->posit16 1.0) (real->posit16 1.0)))) (+.p16 (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i))) (real->posit16 1.0))))> 3.210 * [simplify]: Simplifying (+.p16 (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i))) (real->posit16 1.0)) 3.210 * * [simplify]: iters left: 5 (12 enodes) 3.213 * * [simplify]: iters left: 4 (32 enodes) 3.219 * * [simplify]: iters left: 3 (90 enodes) 3.248 * * [simplify]: iters left: 2 (378 enodes) 3.491 * * [simplify]: Extracting #0: cost 1 inf + 0 3.491 * * [simplify]: Extracting #1: cost 90 inf + 0 3.493 * * [simplify]: Extracting #2: cost 387 inf + 0 3.496 * * [simplify]: Extracting #3: cost 379 inf + 3950 3.503 * * [simplify]: Extracting #4: cost 271 inf + 84531 3.538 * * [simplify]: Extracting #5: cost 20 inf + 357584 3.576 * * [simplify]: Extracting #6: cost 0 inf + 383761 3.614 * [simplify]: Simplified to (+.p16 (real->posit16 1.0) (*.p16 (+.p16 (+.p16 beta alpha) (*.p16 (real->posit16 2) i)) (+.p16 (+.p16 beta alpha) (*.p16 (real->posit16 2) i)))) 3.614 * [simplify]: Simplified (2 2) to (λ (alpha beta i) (*.p16 (/.p16 (/.p16 (*.p16 (*.p16 i (+.p16 (+.p16 alpha beta) i)) (+.p16 (*.p16 beta alpha) (*.p16 i (+.p16 (+.p16 alpha beta) i)))) (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)))) (-.p16 (*.p16 (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i))) (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)))) (*.p16 (real->posit16 1.0) (real->posit16 1.0)))) (+.p16 (real->posit16 1.0) (*.p16 (+.p16 (+.p16 beta alpha) (*.p16 (real->posit16 2) i)) (+.p16 (+.p16 beta alpha) (*.p16 (real->posit16 2) i)))))) 3.615 * * * * [progress]: [ 7 / 17 ] simplifiying candidate #posit16 2) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i))) (real->posit16 1.0)) (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i))))))> 3.615 * [simplify]: Simplifying (*.p16 (*.p16 i (+.p16 (+.p16 alpha beta) i)) (+.p16 (*.p16 beta alpha) (*.p16 i (+.p16 (+.p16 alpha beta) i)))) 3.615 * * [simplify]: iters left: 5 (9 enodes) 3.618 * * [simplify]: iters left: 4 (35 enodes) 3.630 * * [simplify]: iters left: 3 (128 enodes) 3.702 * * [simplify]: Extracting #0: cost 1 inf + 0 3.702 * * [simplify]: Extracting #1: cost 39 inf + 0 3.703 * * [simplify]: Extracting #2: cost 167 inf + 1 3.704 * * [simplify]: Extracting #3: cost 185 inf + 9642 3.711 * * [simplify]: Extracting #4: cost 54 inf + 131260 3.722 * * [simplify]: Extracting #5: cost 0 inf + 183768 3.737 * [simplify]: Simplified to (*.p16 (*.p16 i (+.p16 i (+.p16 alpha beta))) (+.p16 (*.p16 beta alpha) (*.p16 i (+.p16 i (+.p16 alpha beta))))) 3.737 * [simplify]: Simplified (2 1) to (λ (alpha beta i) (/.p16 (*.p16 (*.p16 i (+.p16 i (+.p16 alpha beta))) (+.p16 (*.p16 beta alpha) (*.p16 i (+.p16 i (+.p16 alpha beta))))) (*.p16 (-.p16 (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i))) (real->posit16 1.0)) (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)))))) 3.738 * * * * [progress]: [ 8 / 17 ] simplifiying candidate #posit16 2) i))) (+.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (real->posit16 1.0))) (/.p16 (/.p16 (+.p16 (*.p16 beta alpha) (*.p16 i (+.p16 (+.p16 alpha beta) i))) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i))) (-.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (real->posit16 1.0)))))> 3.738 * [simplify]: Simplifying (/.p16 (/.p16 (*.p16 i (+.p16 (+.p16 alpha beta) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i))) (+.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (real->posit16 1.0))) 3.738 * * [simplify]: iters left: 5 (15 enodes) 3.744 * * [simplify]: iters left: 4 (44 enodes) 3.756 * * [simplify]: iters left: 3 (112 enodes) 3.791 * * [simplify]: iters left: 2 (473 enodes) 4.151 * * [simplify]: Extracting #0: cost 1 inf + 0 4.151 * * [simplify]: Extracting #1: cost 35 inf + 0 4.152 * * [simplify]: Extracting #2: cost 286 inf + 1 4.156 * * [simplify]: Extracting #3: cost 528 inf + 4158 4.162 * * [simplify]: Extracting #4: cost 530 inf + 7620 4.169 * * [simplify]: Extracting #5: cost 473 inf + 34154 4.196 * * [simplify]: Extracting #6: cost 203 inf + 247385 4.239 * * [simplify]: Extracting #7: cost 17 inf + 433812 4.285 * * [simplify]: Extracting #8: cost 0 inf + 455263 4.326 * [simplify]: Simplified to (/.p16 (*.p16 i (+.p16 (+.p16 alpha i) beta)) (+.p16 (*.p16 (+.p16 alpha (+.p16 (*.p16 (real->posit16 2) i) beta)) (+.p16 alpha (+.p16 (*.p16 (real->posit16 2) i) beta))) (+.p16 alpha (+.p16 (*.p16 (real->posit16 2) i) beta)))) 4.326 * [simplify]: Simplified (2 1) to (λ (alpha beta i) (*.p16 (/.p16 (*.p16 i (+.p16 (+.p16 alpha i) beta)) (+.p16 (*.p16 (+.p16 alpha (+.p16 (*.p16 (real->posit16 2) i) beta)) (+.p16 alpha (+.p16 (*.p16 (real->posit16 2) i) beta))) (+.p16 alpha (+.p16 (*.p16 (real->posit16 2) i) beta)))) (/.p16 (/.p16 (+.p16 (*.p16 beta alpha) (*.p16 i (+.p16 (+.p16 alpha beta) i))) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i))) (-.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (real->posit16 1.0))))) 4.326 * [simplify]: Simplifying (/.p16 (/.p16 (+.p16 (*.p16 beta alpha) (*.p16 i (+.p16 (+.p16 alpha beta) i))) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i))) (-.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (real->posit16 1.0))) 4.326 * * [simplify]: iters left: 6 (17 enodes) 4.330 * * [simplify]: iters left: 5 (52 enodes) 4.341 * * [simplify]: iters left: 4 (154 enodes) 4.390 * * [simplify]: Extracting #0: cost 1 inf + 0 4.390 * * [simplify]: Extracting #1: cost 27 inf + 0 4.390 * * [simplify]: Extracting #2: cost 137 inf + 0 4.391 * * [simplify]: Extracting #3: cost 277 inf + 366 4.392 * * [simplify]: Extracting #4: cost 284 inf + 5479 4.394 * * [simplify]: Extracting #5: cost 252 inf + 13708 4.397 * * [simplify]: Extracting #6: cost 206 inf + 39018 4.408 * * [simplify]: Extracting #7: cost 38 inf + 214592 4.427 * * [simplify]: Extracting #8: cost 0 inf + 247968 4.443 * * [simplify]: Extracting #9: cost 0 inf + 243888 4.459 * * [simplify]: Extracting #10: cost 0 inf + 243528 4.475 * [simplify]: Simplified to (/.p16 (+.p16 (*.p16 alpha beta) (*.p16 (+.p16 (+.p16 alpha beta) i) i)) (*.p16 (+.p16 (*.p16 (real->posit16 2) i) (+.p16 alpha beta)) (+.p16 (*.p16 (real->posit16 2) i) (-.p16 (+.p16 alpha beta) (real->posit16 1.0))))) 4.475 * [simplify]: Simplified (2 2) to (λ (alpha beta i) (*.p16 (/.p16 (/.p16 (*.p16 i (+.p16 (+.p16 alpha beta) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i))) (+.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (real->posit16 1.0))) (/.p16 (+.p16 (*.p16 alpha beta) (*.p16 (+.p16 (+.p16 alpha beta) i) i)) (*.p16 (+.p16 (*.p16 (real->posit16 2) i) (+.p16 alpha beta)) (+.p16 (*.p16 (real->posit16 2) i) (-.p16 (+.p16 alpha beta) (real->posit16 1.0))))))) 4.476 * * * * [progress]: [ 9 / 17 ] simplifiying candidate #posit16 2) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)))) (-.p16 (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i))) (real->posit16 1.0))))> 4.476 * [simplify]: Simplifying (*.p16 i i) 4.476 * * [simplify]: iters left: 1 (2 enodes) 4.476 * * [simplify]: Extracting #0: cost 1 inf + 0 4.476 * * [simplify]: Extracting #1: cost 2 inf + 0 4.476 * * [simplify]: Extracting #2: cost 1 inf + 1 4.476 * * [simplify]: Extracting #3: cost 0 inf + 322 4.477 * [simplify]: Simplified to (*.p16 i i) 4.477 * [simplify]: Simplified (2 1 1 2 2) to (λ (alpha beta i) (/.p16 (/.p16 (*.p16 (*.p16 i (+.p16 (+.p16 alpha beta) i)) (+.p16 (+.p16 (*.p16 beta alpha) (*.p16 i (+.p16 alpha beta))) (*.p16 i i))) (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)))) (-.p16 (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i))) (real->posit16 1.0)))) 4.477 * * * * [progress]: [ 10 / 17 ] simplifiying candidate #posit16 2) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)))) (-.p16 (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i))) (real->posit16 1.0))))> 4.477 * [simplify]: Simplifying (*.p16 i i) 4.477 * * [simplify]: iters left: 1 (2 enodes) 4.477 * * [simplify]: Extracting #0: cost 1 inf + 0 4.477 * * [simplify]: Extracting #1: cost 2 inf + 0 4.477 * * [simplify]: Extracting #2: cost 1 inf + 1 4.477 * * [simplify]: Extracting #3: cost 0 inf + 322 4.477 * [simplify]: Simplified to (*.p16 i i) 4.477 * [simplify]: Simplified (2 1 1 2 2) to (λ (alpha beta i) (/.p16 (/.p16 (*.p16 (*.p16 i (+.p16 (+.p16 alpha beta) i)) (+.p16 (+.p16 (*.p16 beta alpha) (*.p16 (+.p16 alpha beta) i)) (*.p16 i i))) (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)))) (-.p16 (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i))) (real->posit16 1.0)))) 4.478 * * * * [progress]: [ 11 / 17 ] simplifiying candidate #posit16 2) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)))) (-.p16 (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i))) (real->posit16 1.0))))> 4.478 * * * * [progress]: [ 12 / 17 ] simplifiying candidate #posit16 2) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)))) (-.p16 (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (+.p16 alpha (+.p16 beta (*.p16 (real->posit16 2) i)))) (real->posit16 1.0))))> 4.478 * * * * [progress]: [ 13 / 17 ] simplifiying candidate #posit16 2) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)))) (-.p16 (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (+.p16 (*.p16 (real->posit16 2) i) (+.p16 alpha beta))) (real->posit16 1.0))))> 4.478 * * * * [progress]: [ 14 / 17 ] simplifiying candidate #posit16 2) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)))) (-.p16 (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i))) (real->posit16 1.0))))> 4.478 * [simplify]: Simplifying (/.p16 (/.p16 (*.p16 (*.p16 i (+.p16 (+.p16 alpha beta) i)) (+.p16 (*.p16 beta alpha) (*.p16 i (+.p16 (+.p16 alpha beta) i)))) (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)))) (-.p16 (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i))) (real->posit16 1.0))) 4.478 * * [simplify]: iters left: 6 (19 enodes) 4.483 * * [simplify]: iters left: 5 (76 enodes) 4.504 * * [simplify]: iters left: 4 (344 enodes) 4.676 * * [simplify]: Extracting #0: cost 1 inf + 0 4.676 * * [simplify]: Extracting #1: cost 75 inf + 0 4.677 * * [simplify]: Extracting #2: cost 474 inf + 1 4.680 * * [simplify]: Extracting #3: cost 741 inf + 26817 4.687 * * [simplify]: Extracting #4: cost 682 inf + 140740 4.701 * * [simplify]: Extracting #5: cost 610 inf + 190036 4.713 * * [simplify]: Extracting #6: cost 582 inf + 205163 4.745 * * [simplify]: Extracting #7: cost 359 inf + 459086 4.807 * * [simplify]: Extracting #8: cost 52 inf + 926046 4.889 * * [simplify]: Extracting #9: cost 0 inf + 1027849 4.968 * * [simplify]: Extracting #10: cost 0 inf + 1026329 5.037 * [simplify]: Simplified to (/.p16 (*.p16 (*.p16 i (+.p16 i (+.p16 alpha beta))) (+.p16 (*.p16 beta alpha) (*.p16 i (+.p16 i (+.p16 alpha beta))))) (*.p16 (*.p16 (+.p16 beta (+.p16 (*.p16 (real->posit16 2) i) alpha)) (+.p16 beta (+.p16 (*.p16 (real->posit16 2) i) alpha))) (-.p16 (*.p16 (+.p16 beta (+.p16 (*.p16 (real->posit16 2) i) alpha)) (+.p16 beta (+.p16 (*.p16 (real->posit16 2) i) alpha))) (real->posit16 1.0)))) 5.037 * [simplify]: Simplified (2) to (λ (alpha beta i) (/.p16 (*.p16 (*.p16 i (+.p16 i (+.p16 alpha beta))) (+.p16 (*.p16 beta alpha) (*.p16 i (+.p16 i (+.p16 alpha beta))))) (*.p16 (*.p16 (+.p16 beta (+.p16 (*.p16 (real->posit16 2) i) alpha)) (+.p16 beta (+.p16 (*.p16 (real->posit16 2) i) alpha))) (-.p16 (*.p16 (+.p16 beta (+.p16 (*.p16 (real->posit16 2) i) alpha)) (+.p16 beta (+.p16 (*.p16 (real->posit16 2) i) alpha))) (real->posit16 1.0))))) 5.038 * * * * [progress]: [ 15 / 17 ] simplifiying candidate #posit16 2) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)))) (-.p16 (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i))) (real->posit16 1.0))))> 5.038 * [simplify]: Simplifying (/.p16 (/.p16 (*.p16 (*.p16 i (+.p16 (+.p16 alpha beta) i)) (+.p16 (*.p16 beta alpha) (*.p16 i (+.p16 (+.p16 alpha beta) i)))) (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)))) (-.p16 (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i))) (real->posit16 1.0))) 5.038 * * [simplify]: iters left: 6 (19 enodes) 5.044 * * [simplify]: iters left: 5 (76 enodes) 5.063 * * [simplify]: iters left: 4 (344 enodes) 5.284 * * [simplify]: Extracting #0: cost 1 inf + 0 5.284 * * [simplify]: Extracting #1: cost 75 inf + 0 5.285 * * [simplify]: Extracting #2: cost 474 inf + 1 5.293 * * [simplify]: Extracting #3: cost 741 inf + 26817 5.306 * * [simplify]: Extracting #4: cost 682 inf + 140740 5.323 * * [simplify]: Extracting #5: cost 610 inf + 190036 5.342 * * [simplify]: Extracting #6: cost 582 inf + 205163 5.381 * * [simplify]: Extracting #7: cost 359 inf + 459086 5.459 * * [simplify]: Extracting #8: cost 52 inf + 926046 5.559 * * [simplify]: Extracting #9: cost 0 inf + 1027849 5.652 * * [simplify]: Extracting #10: cost 0 inf + 1026329 5.745 * [simplify]: Simplified to (/.p16 (*.p16 (*.p16 i (+.p16 i (+.p16 alpha beta))) (+.p16 (*.p16 beta alpha) (*.p16 i (+.p16 i (+.p16 alpha beta))))) (*.p16 (*.p16 (+.p16 beta (+.p16 (*.p16 (real->posit16 2) i) alpha)) (+.p16 beta (+.p16 (*.p16 (real->posit16 2) i) alpha))) (-.p16 (*.p16 (+.p16 beta (+.p16 (*.p16 (real->posit16 2) i) alpha)) (+.p16 beta (+.p16 (*.p16 (real->posit16 2) i) alpha))) (real->posit16 1.0)))) 5.745 * [simplify]: Simplified (2) to (λ (alpha beta i) (/.p16 (*.p16 (*.p16 i (+.p16 i (+.p16 alpha beta))) (+.p16 (*.p16 beta alpha) (*.p16 i (+.p16 i (+.p16 alpha beta))))) (*.p16 (*.p16 (+.p16 beta (+.p16 (*.p16 (real->posit16 2) i) alpha)) (+.p16 beta (+.p16 (*.p16 (real->posit16 2) i) alpha))) (-.p16 (*.p16 (+.p16 beta (+.p16 (*.p16 (real->posit16 2) i) alpha)) (+.p16 beta (+.p16 (*.p16 (real->posit16 2) i) alpha))) (real->posit16 1.0))))) 5.745 * * * * [progress]: [ 16 / 17 ] simplifiying candidate #posit16 2) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)))) (-.p16 (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i))) (real->posit16 1.0))))> 5.746 * [simplify]: Simplifying (/.p16 (/.p16 (*.p16 (*.p16 i (+.p16 (+.p16 alpha beta) i)) (+.p16 (*.p16 beta alpha) (*.p16 i (+.p16 (+.p16 alpha beta) i)))) (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)))) (-.p16 (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i))) (real->posit16 1.0))) 5.746 * * [simplify]: iters left: 6 (19 enodes) 5.754 * * [simplify]: iters left: 5 (76 enodes) 5.786 * * [simplify]: iters left: 4 (344 enodes) 5.995 * * [simplify]: Extracting #0: cost 1 inf + 0 5.995 * * [simplify]: Extracting #1: cost 75 inf + 0 5.996 * * [simplify]: Extracting #2: cost 474 inf + 1 5.999 * * [simplify]: Extracting #3: cost 741 inf + 26817 6.006 * * [simplify]: Extracting #4: cost 682 inf + 140740 6.022 * * [simplify]: Extracting #5: cost 610 inf + 190036 6.041 * * [simplify]: Extracting #6: cost 582 inf + 205163 6.081 * * [simplify]: Extracting #7: cost 359 inf + 459086 6.156 * * [simplify]: Extracting #8: cost 52 inf + 926046 6.231 * * [simplify]: Extracting #9: cost 0 inf + 1027849 6.336 * * [simplify]: Extracting #10: cost 0 inf + 1026329 6.409 * [simplify]: Simplified to (/.p16 (*.p16 (*.p16 i (+.p16 i (+.p16 alpha beta))) (+.p16 (*.p16 beta alpha) (*.p16 i (+.p16 i (+.p16 alpha beta))))) (*.p16 (*.p16 (+.p16 beta (+.p16 (*.p16 (real->posit16 2) i) alpha)) (+.p16 beta (+.p16 (*.p16 (real->posit16 2) i) alpha))) (-.p16 (*.p16 (+.p16 beta (+.p16 (*.p16 (real->posit16 2) i) alpha)) (+.p16 beta (+.p16 (*.p16 (real->posit16 2) i) alpha))) (real->posit16 1.0)))) 6.409 * [simplify]: Simplified (2) to (λ (alpha beta i) (/.p16 (*.p16 (*.p16 i (+.p16 i (+.p16 alpha beta))) (+.p16 (*.p16 beta alpha) (*.p16 i (+.p16 i (+.p16 alpha beta))))) (*.p16 (*.p16 (+.p16 beta (+.p16 (*.p16 (real->posit16 2) i) alpha)) (+.p16 beta (+.p16 (*.p16 (real->posit16 2) i) alpha))) (-.p16 (*.p16 (+.p16 beta (+.p16 (*.p16 (real->posit16 2) i) alpha)) (+.p16 beta (+.p16 (*.p16 (real->posit16 2) i) alpha))) (real->posit16 1.0))))) 6.409 * * * * [progress]: [ 17 / 17 ] simplifiying candidate #posit16 2) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)))) (-.p16 (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i))) (real->posit16 1.0))))> 6.410 * [simplify]: Simplifying (/.p16 (/.p16 (*.p16 (*.p16 i (+.p16 (+.p16 alpha beta) i)) (+.p16 (*.p16 beta alpha) (*.p16 i (+.p16 (+.p16 alpha beta) i)))) (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)))) (-.p16 (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i))) (real->posit16 1.0))) 6.410 * * [simplify]: iters left: 6 (19 enodes) 6.419 * * [simplify]: iters left: 5 (76 enodes) 6.453 * * [simplify]: iters left: 4 (344 enodes) 6.727 * * [simplify]: Extracting #0: cost 1 inf + 0 6.728 * * [simplify]: Extracting #1: cost 75 inf + 0 6.730 * * [simplify]: Extracting #2: cost 474 inf + 1 6.737 * * [simplify]: Extracting #3: cost 741 inf + 26817 6.750 * * [simplify]: Extracting #4: cost 682 inf + 140740 6.767 * * [simplify]: Extracting #5: cost 610 inf + 190036 6.791 * * [simplify]: Extracting #6: cost 582 inf + 205163 6.815 * * [simplify]: Extracting #7: cost 359 inf + 459086 6.861 * * [simplify]: Extracting #8: cost 52 inf + 926046 6.930 * * [simplify]: Extracting #9: cost 0 inf + 1027849 7.010 * * [simplify]: Extracting #10: cost 0 inf + 1026329 7.103 * [simplify]: Simplified to (/.p16 (*.p16 (*.p16 i (+.p16 i (+.p16 alpha beta))) (+.p16 (*.p16 beta alpha) (*.p16 i (+.p16 i (+.p16 alpha beta))))) (*.p16 (*.p16 (+.p16 beta (+.p16 (*.p16 (real->posit16 2) i) alpha)) (+.p16 beta (+.p16 (*.p16 (real->posit16 2) i) alpha))) (-.p16 (*.p16 (+.p16 beta (+.p16 (*.p16 (real->posit16 2) i) alpha)) (+.p16 beta (+.p16 (*.p16 (real->posit16 2) i) alpha))) (real->posit16 1.0)))) 7.103 * [simplify]: Simplified (2) to (λ (alpha beta i) (/.p16 (*.p16 (*.p16 i (+.p16 i (+.p16 alpha beta))) (+.p16 (*.p16 beta alpha) (*.p16 i (+.p16 i (+.p16 alpha beta))))) (*.p16 (*.p16 (+.p16 beta (+.p16 (*.p16 (real->posit16 2) i) alpha)) (+.p16 beta (+.p16 (*.p16 (real->posit16 2) i) alpha))) (-.p16 (*.p16 (+.p16 beta (+.p16 (*.p16 (real->posit16 2) i) alpha)) (+.p16 beta (+.p16 (*.p16 (real->posit16 2) i) alpha))) (real->posit16 1.0))))) 7.103 * * * [progress]: adding candidates to table 7.969 * * [progress]: iteration 2 / 4 7.969 * * * [progress]: picking best candidate 8.230 * * * * [pick]: Picked #posit16 2) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i))) (+.p16 (*.p16 beta alpha) (*.p16 i (+.p16 (+.p16 alpha beta) i))))) (-.p16 (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i))) (real->posit16 1.0))))> 8.230 * * * [progress]: localizing error 8.572 * * * [progress]: generating rewritten candidates 8.572 * * * * [progress]: [ 1 / 4 ] rewriting at (2 1 2) 8.576 * * * * [progress]: [ 2 / 4 ] rewriting at (2) 8.581 * * * * [progress]: [ 3 / 4 ] rewriting at (2 1) 8.585 * * * * [progress]: [ 4 / 4 ] rewriting at (2 1 2 2) 8.588 * * * [progress]: generating series expansions 8.588 * * * * [progress]: [ 1 / 4 ] generating series at (2 1 2) 8.588 * * * * [progress]: [ 2 / 4 ] generating series at (2) 8.588 * * * * [progress]: [ 3 / 4 ] generating series at (2 1) 8.589 * * * * [progress]: [ 4 / 4 ] generating series at (2 1 2 2) 8.589 * * * [progress]: simplifying candidates 8.589 * * * * [progress]: [ 1 / 15 ] simplifiying candidate #posit16 2) i)) (/.p16 (+.p16 (*.p16 beta alpha) (*.p16 i (+.p16 (+.p16 alpha beta) i))) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i))))) (-.p16 (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i))) (real->posit16 1.0))))> 8.589 * [simplify]: Simplifying (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) 8.589 * * [simplify]: iters left: 3 (8 enodes) 8.591 * * [simplify]: iters left: 2 (20 enodes) 8.594 * * [simplify]: iters left: 1 (26 enodes) 8.598 * * [simplify]: Extracting #0: cost 1 inf + 0 8.598 * * [simplify]: Extracting #1: cost 7 inf + 0 8.598 * * [simplify]: Extracting #2: cost 7 inf + 2 8.598 * * [simplify]: Extracting #3: cost 6 inf + 45 8.598 * * [simplify]: Extracting #4: cost 4 inf + 47 8.598 * * [simplify]: Extracting #5: cost 1 inf + 1136 8.598 * * [simplify]: Extracting #6: cost 0 inf + 1499 8.599 * [simplify]: Simplified to (+.p16 (+.p16 beta alpha) (*.p16 (real->posit16 2) i)) 8.599 * [simplify]: Simplified (2 1 2 1) to (λ (alpha beta i) (/.p16 (/.p16 (*.p16 i (+.p16 (+.p16 alpha beta) i)) (/.p16 (+.p16 (+.p16 beta alpha) (*.p16 (real->posit16 2) i)) (/.p16 (+.p16 (*.p16 beta alpha) (*.p16 i (+.p16 (+.p16 alpha beta) i))) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i))))) (-.p16 (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i))) (real->posit16 1.0)))) 8.599 * * * * [progress]: [ 2 / 15 ] simplifiying candidate #posit16 2) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i))) (+.p16 (*.p16 beta alpha) (*.p16 i (+.p16 (+.p16 alpha beta) i))))) (+.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (real->posit16 1.0))) (-.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (real->posit16 1.0))))> 8.599 * [simplify]: Simplifying (-.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (real->posit16 1.0)) 8.599 * * [simplify]: iters left: 4 (11 enodes) 8.602 * * [simplify]: iters left: 3 (33 enodes) 8.608 * * [simplify]: iters left: 2 (87 enodes) 8.636 * * [simplify]: iters left: 1 (455 enodes) 9.114 * * [simplify]: Extracting #0: cost 1 inf + 0 9.114 * * [simplify]: Extracting #1: cost 41 inf + 0 9.115 * * [simplify]: Extracting #2: cost 340 inf + 2 9.123 * * [simplify]: Extracting #3: cost 944 inf + 2428 9.129 * * [simplify]: Extracting #4: cost 917 inf + 30276 9.151 * * [simplify]: Extracting #5: cost 642 inf + 234865 9.233 * * [simplify]: Extracting #6: cost 130 inf + 773963 9.337 * * [simplify]: Extracting #7: cost 0 inf + 938356 9.429 * [simplify]: Simplified to (+.p16 (-.p16 (+.p16 beta alpha) (real->posit16 1.0)) (*.p16 (real->posit16 2) i)) 9.429 * [simplify]: Simplified (2 2) to (λ (alpha beta i) (/.p16 (/.p16 (/.p16 (*.p16 i (+.p16 (+.p16 alpha beta) i)) (/.p16 (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i))) (+.p16 (*.p16 beta alpha) (*.p16 i (+.p16 (+.p16 alpha beta) i))))) (+.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (real->posit16 1.0))) (+.p16 (-.p16 (+.p16 beta alpha) (real->posit16 1.0)) (*.p16 (real->posit16 2) i)))) 9.429 * * * * [progress]: [ 3 / 15 ] simplifiying candidate #posit16 2) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)))) (/.p16 (-.p16 (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i))) (real->posit16 1.0)) (+.p16 (*.p16 beta alpha) (*.p16 i (+.p16 (+.p16 alpha beta) i))))))> 9.429 * [simplify]: Simplifying (/.p16 (*.p16 i (+.p16 (+.p16 alpha beta) i)) (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)))) 9.429 * * [simplify]: iters left: 5 (12 enodes) 9.432 * * [simplify]: iters left: 4 (46 enodes) 9.442 * * [simplify]: iters left: 3 (130 enodes) 9.490 * * [simplify]: iters left: 2 (450 enodes) 9.753 * * [simplify]: Extracting #0: cost 1 inf + 0 9.753 * * [simplify]: Extracting #1: cost 25 inf + 0 9.753 * * [simplify]: Extracting #2: cost 122 inf + 1 9.754 * * [simplify]: Extracting #3: cost 292 inf + 2997 9.756 * * [simplify]: Extracting #4: cost 281 inf + 9272 9.760 * * [simplify]: Extracting #5: cost 221 inf + 62332 9.778 * * [simplify]: Extracting #6: cost 33 inf + 254938 9.816 * * [simplify]: Extracting #7: cost 0 inf + 291590 9.856 * [simplify]: Simplified to (/.p16 (*.p16 i (+.p16 beta (+.p16 alpha i))) (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)))) 9.856 * [simplify]: Simplified (2 1) to (λ (alpha beta i) (/.p16 (/.p16 (*.p16 i (+.p16 beta (+.p16 alpha i))) (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)))) (/.p16 (-.p16 (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i))) (real->posit16 1.0)) (+.p16 (*.p16 beta alpha) (*.p16 i (+.p16 (+.p16 alpha beta) i)))))) 9.857 * * * * [progress]: [ 4 / 15 ] simplifiying candidate #posit16 2) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i))) (+.p16 (*.p16 beta alpha) (*.p16 i (+.p16 (+.p16 alpha beta) i))))) (-.p16 (*.p16 (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i))) (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)))) (*.p16 (real->posit16 1.0) (real->posit16 1.0)))) (+.p16 (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i))) (real->posit16 1.0))))> 9.857 * [simplify]: Simplifying (+.p16 (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i))) (real->posit16 1.0)) 9.857 * * [simplify]: iters left: 5 (12 enodes) 9.863 * * [simplify]: iters left: 4 (32 enodes) 9.875 * * [simplify]: iters left: 3 (90 enodes) 9.926 * * [simplify]: iters left: 2 (378 enodes) 10.248 * * [simplify]: Extracting #0: cost 1 inf + 0 10.248 * * [simplify]: Extracting #1: cost 90 inf + 0 10.249 * * [simplify]: Extracting #2: cost 387 inf + 0 10.251 * * [simplify]: Extracting #3: cost 379 inf + 3950 10.256 * * [simplify]: Extracting #4: cost 271 inf + 84531 10.278 * * [simplify]: Extracting #5: cost 20 inf + 357584 10.307 * * [simplify]: Extracting #6: cost 0 inf + 383761 10.353 * [simplify]: Simplified to (+.p16 (real->posit16 1.0) (*.p16 (+.p16 (+.p16 beta alpha) (*.p16 (real->posit16 2) i)) (+.p16 (+.p16 beta alpha) (*.p16 (real->posit16 2) i)))) 10.353 * [simplify]: Simplified (2 2) to (λ (alpha beta i) (*.p16 (/.p16 (/.p16 (*.p16 i (+.p16 (+.p16 alpha beta) i)) (/.p16 (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i))) (+.p16 (*.p16 beta alpha) (*.p16 i (+.p16 (+.p16 alpha beta) i))))) (-.p16 (*.p16 (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i))) (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)))) (*.p16 (real->posit16 1.0) (real->posit16 1.0)))) (+.p16 (real->posit16 1.0) (*.p16 (+.p16 (+.p16 beta alpha) (*.p16 (real->posit16 2) i)) (+.p16 (+.p16 beta alpha) (*.p16 (real->posit16 2) i)))))) 10.354 * * * * [progress]: [ 5 / 15 ] simplifiying candidate #posit16 2) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i))) (real->posit16 1.0)) (/.p16 (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i))) (+.p16 (*.p16 beta alpha) (*.p16 i (+.p16 (+.p16 alpha beta) i)))))))> 10.354 * [simplify]: Simplifying (*.p16 i (+.p16 (+.p16 alpha beta) i)) 10.354 * * [simplify]: iters left: 3 (6 enodes) 10.356 * * [simplify]: iters left: 2 (22 enodes) 10.359 * * [simplify]: iters left: 1 (42 enodes) 10.366 * * [simplify]: Extracting #0: cost 1 inf + 0 10.366 * * [simplify]: Extracting #1: cost 12 inf + 0 10.366 * * [simplify]: Extracting #2: cost 16 inf + 1 10.366 * * [simplify]: Extracting #3: cost 9 inf + 1412 10.366 * * [simplify]: Extracting #4: cost 0 inf + 4393 10.366 * [simplify]: Simplified to (*.p16 i (+.p16 i (+.p16 alpha beta))) 10.366 * [simplify]: Simplified (2 1) to (λ (alpha beta i) (/.p16 (*.p16 i (+.p16 i (+.p16 alpha beta))) (*.p16 (-.p16 (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i))) (real->posit16 1.0)) (/.p16 (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i))) (+.p16 (*.p16 beta alpha) (*.p16 i (+.p16 (+.p16 alpha beta) i))))))) 10.367 * * * * [progress]: [ 6 / 15 ] simplifiying candidate #posit16 2) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)))) (+.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (real->posit16 1.0))) (/.p16 (+.p16 (*.p16 beta alpha) (*.p16 i (+.p16 (+.p16 alpha beta) i))) (-.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (real->posit16 1.0)))))> 10.367 * [simplify]: Simplifying (/.p16 (/.p16 (*.p16 i (+.p16 (+.p16 alpha beta) i)) (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)))) (+.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (real->posit16 1.0))) 10.367 * * [simplify]: iters left: 6 (16 enodes) 10.371 * * [simplify]: iters left: 5 (56 enodes) 10.383 * * [simplify]: iters left: 4 (182 enodes) 10.454 * * [simplify]: Extracting #0: cost 1 inf + 0 10.454 * * [simplify]: Extracting #1: cost 35 inf + 0 10.455 * * [simplify]: Extracting #2: cost 183 inf + 1 10.456 * * [simplify]: Extracting #3: cost 320 inf + 1981 10.457 * * [simplify]: Extracting #4: cost 312 inf + 7171 10.463 * * [simplify]: Extracting #5: cost 262 inf + 51009 10.482 * * [simplify]: Extracting #6: cost 37 inf + 284804 10.505 * * [simplify]: Extracting #7: cost 0 inf + 324730 10.535 * [simplify]: Simplified to (/.p16 (*.p16 i (+.p16 i (+.p16 alpha beta))) (*.p16 (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i))) (+.p16 (+.p16 (+.p16 (real->posit16 1.0) alpha) (*.p16 (real->posit16 2) i)) beta))) 10.535 * [simplify]: Simplified (2 1) to (λ (alpha beta i) (*.p16 (/.p16 (*.p16 i (+.p16 i (+.p16 alpha beta))) (*.p16 (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i))) (+.p16 (+.p16 (+.p16 (real->posit16 1.0) alpha) (*.p16 (real->posit16 2) i)) beta))) (/.p16 (+.p16 (*.p16 beta alpha) (*.p16 i (+.p16 (+.p16 alpha beta) i))) (-.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (real->posit16 1.0))))) 10.536 * [simplify]: Simplifying (/.p16 (+.p16 (*.p16 beta alpha) (*.p16 i (+.p16 (+.p16 alpha beta) i))) (-.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (real->posit16 1.0))) 10.536 * * [simplify]: iters left: 5 (16 enodes) 10.540 * * [simplify]: iters left: 4 (49 enodes) 10.550 * * [simplify]: iters left: 3 (132 enodes) 10.606 * * [simplify]: Extracting #0: cost 1 inf + 0 10.606 * * [simplify]: Extracting #1: cost 23 inf + 0 10.606 * * [simplify]: Extracting #2: cost 112 inf + 0 10.607 * * [simplify]: Extracting #3: cost 184 inf + 366 10.608 * * [simplify]: Extracting #4: cost 189 inf + 7206 10.611 * * [simplify]: Extracting #5: cost 139 inf + 26225 10.619 * * [simplify]: Extracting #6: cost 32 inf + 109682 10.629 * * [simplify]: Extracting #7: cost 0 inf + 157117 10.639 * [simplify]: Simplified to (/.p16 (+.p16 (*.p16 alpha beta) (*.p16 (+.p16 (+.p16 alpha beta) i) i)) (-.p16 (+.p16 (*.p16 (real->posit16 2) i) (+.p16 alpha beta)) (real->posit16 1.0))) 10.639 * [simplify]: Simplified (2 2) to (λ (alpha beta i) (*.p16 (/.p16 (/.p16 (*.p16 i (+.p16 (+.p16 alpha beta) i)) (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)))) (+.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (real->posit16 1.0))) (/.p16 (+.p16 (*.p16 alpha beta) (*.p16 (+.p16 (+.p16 alpha beta) i) i)) (-.p16 (+.p16 (*.p16 (real->posit16 2) i) (+.p16 alpha beta)) (real->posit16 1.0))))) 10.639 * * * * [progress]: [ 7 / 15 ] simplifiying candidate #posit16 2) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i))) (+.p16 (*.p16 beta alpha) (*.p16 i (+.p16 (+.p16 alpha beta) i)))) (+.p16 (+.p16 alpha beta) i))) (-.p16 (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i))) (real->posit16 1.0))))> 10.639 * * * * [progress]: [ 8 / 15 ] simplifiying candidate #posit16 2) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)))) (+.p16 (*.p16 beta alpha) (*.p16 i (+.p16 (+.p16 alpha beta) i)))) (-.p16 (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i))) (real->posit16 1.0))))> 10.639 * [simplify]: Simplifying (+.p16 (*.p16 beta alpha) (*.p16 i (+.p16 (+.p16 alpha beta) i))) 10.639 * * [simplify]: iters left: 4 (8 enodes) 10.641 * * [simplify]: iters left: 3 (26 enodes) 10.646 * * [simplify]: iters left: 2 (53 enodes) 10.661 * * [simplify]: iters left: 1 (91 enodes) 10.678 * * [simplify]: Extracting #0: cost 1 inf + 0 10.678 * * [simplify]: Extracting #1: cost 24 inf + 0 10.678 * * [simplify]: Extracting #2: cost 31 inf + 0 10.678 * * [simplify]: Extracting #3: cost 26 inf + 366 10.679 * * [simplify]: Extracting #4: cost 9 inf + 8250 10.680 * * [simplify]: Extracting #5: cost 0 inf + 15077 10.680 * [simplify]: Simplified to (+.p16 (*.p16 alpha (+.p16 beta i)) (*.p16 (+.p16 beta i) i)) 10.681 * [simplify]: Simplified (2 1 2) to (λ (alpha beta i) (/.p16 (*.p16 (/.p16 (*.p16 i (+.p16 (+.p16 alpha beta) i)) (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)))) (+.p16 (*.p16 alpha (+.p16 beta i)) (*.p16 (+.p16 beta i) i))) (-.p16 (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i))) (real->posit16 1.0)))) 10.681 * * * * [progress]: [ 9 / 15 ] simplifiying candidate #posit16 2) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i))) (+.p16 (+.p16 (*.p16 beta alpha) (*.p16 i (+.p16 alpha beta))) (*.p16 i i)))) (-.p16 (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i))) (real->posit16 1.0))))> 10.681 * [simplify]: Simplifying (*.p16 i i) 10.681 * * [simplify]: iters left: 1 (2 enodes) 10.681 * * [simplify]: Extracting #0: cost 1 inf + 0 10.681 * * [simplify]: Extracting #1: cost 2 inf + 0 10.681 * * [simplify]: Extracting #2: cost 1 inf + 1 10.681 * * [simplify]: Extracting #3: cost 0 inf + 322 10.681 * [simplify]: Simplified to (*.p16 i i) 10.682 * [simplify]: Simplified (2 1 2 2 2) to (λ (alpha beta i) (/.p16 (/.p16 (*.p16 i (+.p16 (+.p16 alpha beta) i)) (/.p16 (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i))) (+.p16 (+.p16 (*.p16 beta alpha) (*.p16 i (+.p16 alpha beta))) (*.p16 i i)))) (-.p16 (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i))) (real->posit16 1.0)))) 10.682 * * * * [progress]: [ 10 / 15 ] simplifiying candidate #posit16 2) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i))) (+.p16 (+.p16 (*.p16 beta alpha) (*.p16 (+.p16 alpha beta) i)) (*.p16 i i)))) (-.p16 (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i))) (real->posit16 1.0))))> 10.682 * [simplify]: Simplifying (*.p16 i i) 10.682 * * [simplify]: iters left: 1 (2 enodes) 10.682 * * [simplify]: Extracting #0: cost 1 inf + 0 10.682 * * [simplify]: Extracting #1: cost 2 inf + 0 10.682 * * [simplify]: Extracting #2: cost 1 inf + 1 10.682 * * [simplify]: Extracting #3: cost 0 inf + 322 10.682 * [simplify]: Simplified to (*.p16 i i) 10.682 * [simplify]: Simplified (2 1 2 2 2) to (λ (alpha beta i) (/.p16 (/.p16 (*.p16 i (+.p16 (+.p16 alpha beta) i)) (/.p16 (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i))) (+.p16 (+.p16 (*.p16 beta alpha) (*.p16 (+.p16 alpha beta) i)) (*.p16 i i)))) (-.p16 (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i))) (real->posit16 1.0)))) 10.683 * * * * [progress]: [ 11 / 15 ] simplifiying candidate #posit16 2) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i))) (+.p16 (*.p16 i (+.p16 (+.p16 alpha beta) i)) (*.p16 beta alpha)))) (-.p16 (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i))) (real->posit16 1.0))))> 10.683 * * * * [progress]: [ 12 / 15 ] simplifiying candidate #posit16 2) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i))) (+.p16 (*.p16 beta alpha) (*.p16 i (+.p16 (+.p16 alpha beta) i))))) (-.p16 (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i))) (real->posit16 1.0))))> 10.683 * [simplify]: Simplifying (*.p16 i (+.p16 (+.p16 alpha beta) i)) 10.683 * * [simplify]: iters left: 3 (6 enodes) 10.684 * * [simplify]: iters left: 2 (22 enodes) 10.692 * * [simplify]: iters left: 1 (42 enodes) 10.705 * * [simplify]: Extracting #0: cost 1 inf + 0 10.705 * * [simplify]: Extracting #1: cost 12 inf + 0 10.705 * * [simplify]: Extracting #2: cost 16 inf + 1 10.706 * * [simplify]: Extracting #3: cost 9 inf + 1412 10.706 * * [simplify]: Extracting #4: cost 0 inf + 4393 10.707 * [simplify]: Simplified to (*.p16 i (+.p16 i (+.p16 alpha beta))) 10.707 * [simplify]: Simplified (2 1 1) to (λ (alpha beta i) (/.p16 (/.p16 (*.p16 i (+.p16 i (+.p16 alpha beta))) (/.p16 (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i))) (+.p16 (*.p16 beta alpha) (*.p16 i (+.p16 (+.p16 alpha beta) i))))) (-.p16 (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i))) (real->posit16 1.0)))) 10.707 * * * * [progress]: [ 13 / 15 ] simplifiying candidate #posit16 2) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i))) (+.p16 (*.p16 beta alpha) (*.p16 i (+.p16 (+.p16 alpha beta) i))))) (-.p16 (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i))) (real->posit16 1.0))))> 10.707 * [simplify]: Simplifying (*.p16 i (+.p16 (+.p16 alpha beta) i)) 10.707 * * [simplify]: iters left: 3 (6 enodes) 10.710 * * [simplify]: iters left: 2 (22 enodes) 10.716 * * [simplify]: iters left: 1 (42 enodes) 10.728 * * [simplify]: Extracting #0: cost 1 inf + 0 10.728 * * [simplify]: Extracting #1: cost 12 inf + 0 10.728 * * [simplify]: Extracting #2: cost 16 inf + 1 10.728 * * [simplify]: Extracting #3: cost 9 inf + 1412 10.729 * * [simplify]: Extracting #4: cost 0 inf + 4393 10.730 * [simplify]: Simplified to (*.p16 i (+.p16 i (+.p16 alpha beta))) 10.730 * [simplify]: Simplified (2 1 1) to (λ (alpha beta i) (/.p16 (/.p16 (*.p16 i (+.p16 i (+.p16 alpha beta))) (/.p16 (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i))) (+.p16 (*.p16 beta alpha) (*.p16 i (+.p16 (+.p16 alpha beta) i))))) (-.p16 (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i))) (real->posit16 1.0)))) 10.730 * * * * [progress]: [ 14 / 15 ] simplifiying candidate #posit16 2) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i))) (+.p16 (*.p16 beta alpha) (*.p16 i (+.p16 (+.p16 alpha beta) i))))) (-.p16 (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i))) (real->posit16 1.0))))> 10.730 * [simplify]: Simplifying (*.p16 i (+.p16 (+.p16 alpha beta) i)) 10.730 * * [simplify]: iters left: 3 (6 enodes) 10.733 * * [simplify]: iters left: 2 (22 enodes) 10.739 * * [simplify]: iters left: 1 (42 enodes) 10.750 * * [simplify]: Extracting #0: cost 1 inf + 0 10.750 * * [simplify]: Extracting #1: cost 12 inf + 0 10.750 * * [simplify]: Extracting #2: cost 16 inf + 1 10.750 * * [simplify]: Extracting #3: cost 9 inf + 1412 10.750 * * [simplify]: Extracting #4: cost 0 inf + 4393 10.751 * [simplify]: Simplified to (*.p16 i (+.p16 i (+.p16 alpha beta))) 10.751 * [simplify]: Simplified (2 1 1) to (λ (alpha beta i) (/.p16 (/.p16 (*.p16 i (+.p16 i (+.p16 alpha beta))) (/.p16 (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i))) (+.p16 (*.p16 beta alpha) (*.p16 i (+.p16 (+.p16 alpha beta) i))))) (-.p16 (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i))) (real->posit16 1.0)))) 10.751 * * * * [progress]: [ 15 / 15 ] simplifiying candidate #posit16 2) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i))) (+.p16 (*.p16 beta alpha) (*.p16 i (+.p16 (+.p16 alpha beta) i))))) (-.p16 (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i))) (real->posit16 1.0))))> 10.751 * [simplify]: Simplifying (*.p16 i (+.p16 (+.p16 alpha beta) i)) 10.751 * * [simplify]: iters left: 3 (6 enodes) 10.753 * * [simplify]: iters left: 2 (22 enodes) 10.756 * * [simplify]: iters left: 1 (42 enodes) 10.767 * * [simplify]: Extracting #0: cost 1 inf + 0 10.767 * * [simplify]: Extracting #1: cost 12 inf + 0 10.767 * * [simplify]: Extracting #2: cost 16 inf + 1 10.768 * * [simplify]: Extracting #3: cost 9 inf + 1412 10.768 * * [simplify]: Extracting #4: cost 0 inf + 4393 10.769 * [simplify]: Simplified to (*.p16 i (+.p16 i (+.p16 alpha beta))) 10.769 * [simplify]: Simplified (2 1 1) to (λ (alpha beta i) (/.p16 (/.p16 (*.p16 i (+.p16 i (+.p16 alpha beta))) (/.p16 (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i))) (+.p16 (*.p16 beta alpha) (*.p16 i (+.p16 (+.p16 alpha beta) i))))) (-.p16 (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i))) (real->posit16 1.0)))) 10.769 * * * [progress]: adding candidates to table 11.543 * * [progress]: iteration 3 / 4 11.543 * * * [progress]: picking best candidate 11.912 * * * * [pick]: Picked #posit16 2) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)))) (+.p16 (*.p16 beta alpha) (*.p16 i (+.p16 (+.p16 alpha beta) i)))) (-.p16 (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i))) (real->posit16 1.0))))> 11.912 * * * [progress]: localizing error 12.323 * * * [progress]: generating rewritten candidates 12.323 * * * * [progress]: [ 1 / 4 ] rewriting at (2 1 1) 12.330 * * * * [progress]: [ 2 / 4 ] rewriting at (2) 12.343 * * * * [progress]: [ 3 / 4 ] rewriting at (2 1) 12.351 * * * * [progress]: [ 4 / 4 ] rewriting at (2 1 2) 12.354 * * * [progress]: generating series expansions 12.354 * * * * [progress]: [ 1 / 4 ] generating series at (2 1 1) 12.354 * * * * [progress]: [ 2 / 4 ] generating series at (2) 12.354 * * * * [progress]: [ 3 / 4 ] generating series at (2 1) 12.354 * * * * [progress]: [ 4 / 4 ] generating series at (2 1 2) 12.354 * * * [progress]: simplifying candidates 12.354 * * * * [progress]: [ 1 / 20 ] simplifiying candidate #posit16 2) i))) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i))) (+.p16 (*.p16 beta alpha) (*.p16 i (+.p16 (+.p16 alpha beta) i)))) (-.p16 (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i))) (real->posit16 1.0))))> 12.355 * [simplify]: Simplifying (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) 12.355 * * [simplify]: iters left: 3 (8 enodes) 12.357 * * [simplify]: iters left: 2 (20 enodes) 12.360 * * [simplify]: iters left: 1 (26 enodes) 12.364 * * [simplify]: Extracting #0: cost 1 inf + 0 12.364 * * [simplify]: Extracting #1: cost 7 inf + 0 12.364 * * [simplify]: Extracting #2: cost 7 inf + 2 12.364 * * [simplify]: Extracting #3: cost 6 inf + 45 12.364 * * [simplify]: Extracting #4: cost 4 inf + 47 12.364 * * [simplify]: Extracting #5: cost 1 inf + 1136 12.364 * * [simplify]: Extracting #6: cost 0 inf + 1499 12.364 * [simplify]: Simplified to (+.p16 (+.p16 beta alpha) (*.p16 (real->posit16 2) i)) 12.365 * [simplify]: Simplified (2 1 1 2) to (λ (alpha beta i) (/.p16 (*.p16 (/.p16 (/.p16 (*.p16 i (+.p16 (+.p16 alpha beta) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i))) (+.p16 (+.p16 beta alpha) (*.p16 (real->posit16 2) i))) (+.p16 (*.p16 beta alpha) (*.p16 i (+.p16 (+.p16 alpha beta) i)))) (-.p16 (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i))) (real->posit16 1.0)))) 12.365 * * * * [progress]: [ 2 / 20 ] simplifiying candidate #posit16 2) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i))) (+.p16 (+.p16 alpha beta) i))) (+.p16 (*.p16 beta alpha) (*.p16 i (+.p16 (+.p16 alpha beta) i)))) (-.p16 (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i))) (real->posit16 1.0))))> 12.365 * * * * [progress]: [ 3 / 20 ] simplifiying candidate #posit16 2) i))) (/.p16 (+.p16 (+.p16 alpha beta) i) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)))) (+.p16 (*.p16 beta alpha) (*.p16 i (+.p16 (+.p16 alpha beta) i)))) (-.p16 (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i))) (real->posit16 1.0))))> 12.365 * [simplify]: Simplifying (/.p16 i (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i))) 12.365 * * [simplify]: iters left: 4 (9 enodes) 12.367 * * [simplify]: iters left: 3 (21 enodes) 12.371 * * [simplify]: iters left: 2 (27 enodes) 12.379 * * [simplify]: iters left: 1 (28 enodes) 12.387 * * [simplify]: Extracting #0: cost 1 inf + 0 12.388 * * [simplify]: Extracting #1: cost 3 inf + 0 12.388 * * [simplify]: Extracting #2: cost 8 inf + 1 12.388 * * [simplify]: Extracting #3: cost 6 inf + 45 12.388 * * [simplify]: Extracting #4: cost 7 inf + 45 12.388 * * [simplify]: Extracting #5: cost 1 inf + 1499 12.388 * * [simplify]: Extracting #6: cost 0 inf + 2343 12.389 * [simplify]: Simplified to (/.p16 i (+.p16 beta (+.p16 alpha (*.p16 i (real->posit16 2))))) 12.389 * [simplify]: Simplified (2 1 1 1) to (λ (alpha beta i) (/.p16 (*.p16 (*.p16 (/.p16 i (+.p16 beta (+.p16 alpha (*.p16 i (real->posit16 2))))) (/.p16 (+.p16 (+.p16 alpha beta) i) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)))) (+.p16 (*.p16 beta alpha) (*.p16 i (+.p16 (+.p16 alpha beta) i)))) (-.p16 (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i))) (real->posit16 1.0)))) 12.389 * [simplify]: Simplifying (/.p16 (+.p16 (+.p16 alpha beta) i) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i))) 12.390 * * [simplify]: iters left: 4 (10 enodes) 12.400 * * [simplify]: iters left: 3 (25 enodes) 12.409 * * [simplify]: iters left: 2 (37 enodes) 12.419 * * [simplify]: iters left: 1 (40 enodes) 12.429 * * [simplify]: Extracting #0: cost 1 inf + 0 12.429 * * [simplify]: Extracting #1: cost 3 inf + 0 12.429 * * [simplify]: Extracting #2: cost 12 inf + 0 12.429 * * [simplify]: Extracting #3: cost 9 inf + 45 12.429 * * [simplify]: Extracting #4: cost 7 inf + 212 12.429 * * [simplify]: Extracting #5: cost 6 inf + 213 12.430 * * [simplify]: Extracting #6: cost 4 inf + 536 12.430 * * [simplify]: Extracting #7: cost 0 inf + 2590 12.430 * [simplify]: Simplified to (/.p16 (+.p16 alpha (+.p16 i beta)) (+.p16 (+.p16 beta alpha) (*.p16 (real->posit16 2) i))) 12.431 * [simplify]: Simplified (2 1 1 2) to (λ (alpha beta i) (/.p16 (*.p16 (*.p16 (/.p16 i (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i))) (/.p16 (+.p16 alpha (+.p16 i beta)) (+.p16 (+.p16 beta alpha) (*.p16 (real->posit16 2) i)))) (+.p16 (*.p16 beta alpha) (*.p16 i (+.p16 (+.p16 alpha beta) i)))) (-.p16 (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i))) (real->posit16 1.0)))) 12.431 * * * * [progress]: [ 4 / 20 ] simplifiying candidate #posit16 2) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)))) (+.p16 (*.p16 beta alpha) (*.p16 i (+.p16 (+.p16 alpha beta) i)))) (+.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (real->posit16 1.0))) (-.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (real->posit16 1.0))))> 12.431 * [simplify]: Simplifying (-.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (real->posit16 1.0)) 12.431 * * [simplify]: iters left: 4 (11 enodes) 12.436 * * [simplify]: iters left: 3 (33 enodes) 12.448 * * [simplify]: iters left: 2 (87 enodes) 12.496 * * [simplify]: iters left: 1 (455 enodes) 13.619 * * [simplify]: Extracting #0: cost 1 inf + 0 13.619 * * [simplify]: Extracting #1: cost 41 inf + 0 13.620 * * [simplify]: Extracting #2: cost 340 inf + 2 13.624 * * [simplify]: Extracting #3: cost 944 inf + 2428 13.630 * * [simplify]: Extracting #4: cost 917 inf + 30276 13.646 * * [simplify]: Extracting #5: cost 642 inf + 234865 13.703 * * [simplify]: Extracting #6: cost 130 inf + 773963 13.813 * * [simplify]: Extracting #7: cost 0 inf + 938356 13.935 * [simplify]: Simplified to (+.p16 (-.p16 (+.p16 beta alpha) (real->posit16 1.0)) (*.p16 (real->posit16 2) i)) 13.935 * [simplify]: Simplified (2 2) to (λ (alpha beta i) (/.p16 (/.p16 (*.p16 (/.p16 (*.p16 i (+.p16 (+.p16 alpha beta) i)) (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)))) (+.p16 (*.p16 beta alpha) (*.p16 i (+.p16 (+.p16 alpha beta) i)))) (+.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (real->posit16 1.0))) (+.p16 (-.p16 (+.p16 beta alpha) (real->posit16 1.0)) (*.p16 (real->posit16 2) i)))) 13.935 * * * * [progress]: [ 5 / 20 ] simplifiying candidate #posit16 2) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)))) (/.p16 (-.p16 (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i))) (real->posit16 1.0)) (+.p16 (*.p16 beta alpha) (*.p16 i (+.p16 (+.p16 alpha beta) i))))))> 13.936 * [simplify]: Simplifying (/.p16 (*.p16 i (+.p16 (+.p16 alpha beta) i)) (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)))) 13.936 * * [simplify]: iters left: 5 (12 enodes) 13.942 * * [simplify]: iters left: 4 (46 enodes) 13.962 * * [simplify]: iters left: 3 (130 enodes) 14.007 * * [simplify]: iters left: 2 (450 enodes) 14.428 * * [simplify]: Extracting #0: cost 1 inf + 0 14.428 * * [simplify]: Extracting #1: cost 25 inf + 0 14.429 * * [simplify]: Extracting #2: cost 122 inf + 1 14.431 * * [simplify]: Extracting #3: cost 292 inf + 2997 14.434 * * [simplify]: Extracting #4: cost 281 inf + 9272 14.440 * * [simplify]: Extracting #5: cost 221 inf + 62332 14.475 * * [simplify]: Extracting #6: cost 33 inf + 254938 14.514 * * [simplify]: Extracting #7: cost 0 inf + 291590 14.555 * [simplify]: Simplified to (/.p16 (*.p16 i (+.p16 beta (+.p16 alpha i))) (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)))) 14.555 * [simplify]: Simplified (2 1) to (λ (alpha beta i) (/.p16 (/.p16 (*.p16 i (+.p16 beta (+.p16 alpha i))) (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)))) (/.p16 (-.p16 (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i))) (real->posit16 1.0)) (+.p16 (*.p16 beta alpha) (*.p16 i (+.p16 (+.p16 alpha beta) i)))))) 14.555 * * * * [progress]: [ 6 / 20 ] simplifiying candidate #posit16 2) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)))) (+.p16 (*.p16 beta alpha) (*.p16 i (+.p16 (+.p16 alpha beta) i)))) (-.p16 (*.p16 (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i))) (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)))) (*.p16 (real->posit16 1.0) (real->posit16 1.0)))) (+.p16 (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i))) (real->posit16 1.0))))> 14.556 * [simplify]: Simplifying (+.p16 (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i))) (real->posit16 1.0)) 14.556 * * [simplify]: iters left: 5 (12 enodes) 14.562 * * [simplify]: iters left: 4 (32 enodes) 14.575 * * [simplify]: iters left: 3 (90 enodes) 14.633 * * [simplify]: iters left: 2 (378 enodes) 15.011 * * [simplify]: Extracting #0: cost 1 inf + 0 15.011 * * [simplify]: Extracting #1: cost 90 inf + 0 15.013 * * [simplify]: Extracting #2: cost 387 inf + 0 15.015 * * [simplify]: Extracting #3: cost 379 inf + 3950 15.022 * * [simplify]: Extracting #4: cost 271 inf + 84531 15.044 * * [simplify]: Extracting #5: cost 20 inf + 357584 15.085 * * [simplify]: Extracting #6: cost 0 inf + 383761 15.111 * [simplify]: Simplified to (+.p16 (real->posit16 1.0) (*.p16 (+.p16 (+.p16 beta alpha) (*.p16 (real->posit16 2) i)) (+.p16 (+.p16 beta alpha) (*.p16 (real->posit16 2) i)))) 15.111 * [simplify]: Simplified (2 2) to (λ (alpha beta i) (*.p16 (/.p16 (*.p16 (/.p16 (*.p16 i (+.p16 (+.p16 alpha beta) i)) (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)))) (+.p16 (*.p16 beta alpha) (*.p16 i (+.p16 (+.p16 alpha beta) i)))) (-.p16 (*.p16 (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i))) (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)))) (*.p16 (real->posit16 1.0) (real->posit16 1.0)))) (+.p16 (real->posit16 1.0) (*.p16 (+.p16 (+.p16 beta alpha) (*.p16 (real->posit16 2) i)) (+.p16 (+.p16 beta alpha) (*.p16 (real->posit16 2) i)))))) 15.111 * * * * [progress]: [ 7 / 20 ] simplifiying candidate #posit16 2) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i))) (real->posit16 1.0)) (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i))))))> 15.111 * [simplify]: Simplifying (*.p16 (*.p16 i (+.p16 (+.p16 alpha beta) i)) (+.p16 (*.p16 beta alpha) (*.p16 i (+.p16 (+.p16 alpha beta) i)))) 15.111 * * [simplify]: iters left: 5 (9 enodes) 15.113 * * [simplify]: iters left: 4 (35 enodes) 15.121 * * [simplify]: iters left: 3 (128 enodes) 15.169 * * [simplify]: Extracting #0: cost 1 inf + 0 15.169 * * [simplify]: Extracting #1: cost 39 inf + 0 15.170 * * [simplify]: Extracting #2: cost 167 inf + 1 15.171 * * [simplify]: Extracting #3: cost 185 inf + 9642 15.176 * * [simplify]: Extracting #4: cost 54 inf + 131260 15.183 * * [simplify]: Extracting #5: cost 0 inf + 183768 15.191 * [simplify]: Simplified to (*.p16 (*.p16 i (+.p16 i (+.p16 alpha beta))) (+.p16 (*.p16 beta alpha) (*.p16 i (+.p16 i (+.p16 alpha beta))))) 15.191 * [simplify]: Simplified (2 1) to (λ (alpha beta i) (/.p16 (*.p16 (*.p16 i (+.p16 i (+.p16 alpha beta))) (+.p16 (*.p16 beta alpha) (*.p16 i (+.p16 i (+.p16 alpha beta))))) (*.p16 (-.p16 (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i))) (real->posit16 1.0)) (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)))))) 15.192 * * * * [progress]: [ 8 / 20 ] simplifiying candidate #posit16 2) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)))) (+.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (real->posit16 1.0))) (/.p16 (+.p16 (*.p16 beta alpha) (*.p16 i (+.p16 (+.p16 alpha beta) i))) (-.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (real->posit16 1.0)))))> 15.192 * [simplify]: Simplifying (/.p16 (/.p16 (*.p16 i (+.p16 (+.p16 alpha beta) i)) (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)))) (+.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (real->posit16 1.0))) 15.192 * * [simplify]: iters left: 6 (16 enodes) 15.198 * * [simplify]: iters left: 5 (56 enodes) 15.219 * * [simplify]: iters left: 4 (182 enodes) 15.344 * * [simplify]: Extracting #0: cost 1 inf + 0 15.344 * * [simplify]: Extracting #1: cost 35 inf + 0 15.345 * * [simplify]: Extracting #2: cost 183 inf + 1 15.347 * * [simplify]: Extracting #3: cost 320 inf + 1981 15.350 * * [simplify]: Extracting #4: cost 312 inf + 7171 15.356 * * [simplify]: Extracting #5: cost 262 inf + 51009 15.383 * * [simplify]: Extracting #6: cost 37 inf + 284804 15.423 * * [simplify]: Extracting #7: cost 0 inf + 324730 15.461 * [simplify]: Simplified to (/.p16 (*.p16 i (+.p16 i (+.p16 alpha beta))) (*.p16 (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i))) (+.p16 (+.p16 (+.p16 (real->posit16 1.0) alpha) (*.p16 (real->posit16 2) i)) beta))) 15.461 * [simplify]: Simplified (2 1) to (λ (alpha beta i) (*.p16 (/.p16 (*.p16 i (+.p16 i (+.p16 alpha beta))) (*.p16 (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i))) (+.p16 (+.p16 (+.p16 (real->posit16 1.0) alpha) (*.p16 (real->posit16 2) i)) beta))) (/.p16 (+.p16 (*.p16 beta alpha) (*.p16 i (+.p16 (+.p16 alpha beta) i))) (-.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (real->posit16 1.0))))) 15.463 * [simplify]: Simplifying (/.p16 (+.p16 (*.p16 beta alpha) (*.p16 i (+.p16 (+.p16 alpha beta) i))) (-.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (real->posit16 1.0))) 15.463 * * [simplify]: iters left: 5 (16 enodes) 15.474 * * [simplify]: iters left: 4 (49 enodes) 15.494 * * [simplify]: iters left: 3 (132 enodes) 15.556 * * [simplify]: Extracting #0: cost 1 inf + 0 15.556 * * [simplify]: Extracting #1: cost 23 inf + 0 15.556 * * [simplify]: Extracting #2: cost 112 inf + 0 15.557 * * [simplify]: Extracting #3: cost 184 inf + 366 15.559 * * [simplify]: Extracting #4: cost 189 inf + 7206 15.562 * * [simplify]: Extracting #5: cost 139 inf + 26225 15.574 * * [simplify]: Extracting #6: cost 32 inf + 109682 15.593 * * [simplify]: Extracting #7: cost 0 inf + 157117 15.615 * [simplify]: Simplified to (/.p16 (+.p16 (*.p16 alpha beta) (*.p16 (+.p16 (+.p16 alpha beta) i) i)) (-.p16 (+.p16 (*.p16 (real->posit16 2) i) (+.p16 alpha beta)) (real->posit16 1.0))) 15.615 * [simplify]: Simplified (2 2) to (λ (alpha beta i) (*.p16 (/.p16 (/.p16 (*.p16 i (+.p16 (+.p16 alpha beta) i)) (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)))) (+.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (real->posit16 1.0))) (/.p16 (+.p16 (*.p16 alpha beta) (*.p16 (+.p16 (+.p16 alpha beta) i) i)) (-.p16 (+.p16 (*.p16 (real->posit16 2) i) (+.p16 alpha beta)) (real->posit16 1.0))))) 15.615 * * * * [progress]: [ 9 / 20 ] simplifiying candidate #posit16 2) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)))) (*.p16 beta alpha)) (*.p16 (/.p16 (*.p16 i (+.p16 (+.p16 alpha beta) i)) (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)))) (*.p16 i (+.p16 (+.p16 alpha beta) i)))) (-.p16 (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i))) (real->posit16 1.0))))> 15.615 * [simplify]: Simplifying (*.p16 (/.p16 (*.p16 i (+.p16 (+.p16 alpha beta) i)) (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)))) (*.p16 i (+.p16 (+.p16 alpha beta) i))) 15.616 * * [simplify]: iters left: 6 (13 enodes) 15.622 * * [simplify]: iters left: 5 (52 enodes) 15.647 * * [simplify]: iters left: 4 (205 enodes) 15.758 * * [simplify]: Extracting #0: cost 1 inf + 0 15.759 * * [simplify]: Extracting #1: cost 48 inf + 0 15.759 * * [simplify]: Extracting #2: cost 226 inf + 1 15.761 * * [simplify]: Extracting #3: cost 257 inf + 13987 15.764 * * [simplify]: Extracting #4: cost 195 inf + 69011 15.771 * * [simplify]: Extracting #5: cost 154 inf + 114114 15.788 * * [simplify]: Extracting #6: cost 18 inf + 287386 15.807 * * [simplify]: Extracting #7: cost 0 inf + 314297 15.826 * [simplify]: Simplified to (*.p16 (*.p16 i (/.p16 (+.p16 i (+.p16 alpha beta)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)))) (*.p16 i (/.p16 (+.p16 i (+.p16 alpha beta)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i))))) 15.826 * [simplify]: Simplified (2 1 2) to (λ (alpha beta i) (/.p16 (+.p16 (*.p16 (/.p16 (*.p16 i (+.p16 (+.p16 alpha beta) i)) (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)))) (*.p16 beta alpha)) (*.p16 (*.p16 i (/.p16 (+.p16 i (+.p16 alpha beta)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)))) (*.p16 i (/.p16 (+.p16 i (+.p16 alpha beta)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)))))) (-.p16 (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i))) (real->posit16 1.0)))) 15.826 * * * * [progress]: [ 10 / 20 ] simplifiying candidate #posit16 2) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i))))) (*.p16 (*.p16 i (+.p16 (+.p16 alpha beta) i)) (/.p16 (*.p16 i (+.p16 (+.p16 alpha beta) i)) (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)))))) (-.p16 (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i))) (real->posit16 1.0))))> 15.826 * [simplify]: Simplifying (*.p16 (*.p16 i (+.p16 (+.p16 alpha beta) i)) (/.p16 (*.p16 i (+.p16 (+.p16 alpha beta) i)) (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i))))) 15.826 * * [simplify]: iters left: 6 (13 enodes) 15.829 * * [simplify]: iters left: 5 (52 enodes) 15.841 * * [simplify]: iters left: 4 (191 enodes) 15.961 * * [simplify]: Extracting #0: cost 1 inf + 0 15.962 * * [simplify]: Extracting #1: cost 49 inf + 0 15.963 * * [simplify]: Extracting #2: cost 214 inf + 1 15.965 * * [simplify]: Extracting #3: cost 243 inf + 17482 15.972 * * [simplify]: Extracting #4: cost 194 inf + 65079 15.982 * * [simplify]: Extracting #5: cost 162 inf + 90223 16.005 * * [simplify]: Extracting #6: cost 42 inf + 243588 16.036 * * [simplify]: Extracting #7: cost 0 inf + 306234 16.054 * * [simplify]: Extracting #8: cost 0 inf + 305994 16.077 * [simplify]: Simplified to (*.p16 (/.p16 (*.p16 i (+.p16 i (+.p16 alpha beta))) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i))) (/.p16 (*.p16 i (+.p16 i (+.p16 alpha beta))) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)))) 16.078 * [simplify]: Simplified (2 1 2) to (λ (alpha beta i) (/.p16 (+.p16 (*.p16 (*.p16 beta alpha) (/.p16 (*.p16 i (+.p16 (+.p16 alpha beta) i)) (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i))))) (*.p16 (/.p16 (*.p16 i (+.p16 i (+.p16 alpha beta))) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i))) (/.p16 (*.p16 i (+.p16 i (+.p16 alpha beta))) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i))))) (-.p16 (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i))) (real->posit16 1.0)))) 16.078 * * * * [progress]: [ 11 / 20 ] simplifiying candidate #posit16 2) i))) (*.p16 (/.p16 (+.p16 (+.p16 alpha beta) i) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i))) (+.p16 (*.p16 beta alpha) (*.p16 i (+.p16 (+.p16 alpha beta) i))))) (-.p16 (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i))) (real->posit16 1.0))))> 16.078 * [simplify]: Simplifying (/.p16 i (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i))) 16.078 * * [simplify]: iters left: 4 (9 enodes) 16.082 * * [simplify]: iters left: 3 (21 enodes) 16.090 * * [simplify]: iters left: 2 (27 enodes) 16.098 * * [simplify]: iters left: 1 (28 enodes) 16.102 * * [simplify]: Extracting #0: cost 1 inf + 0 16.102 * * [simplify]: Extracting #1: cost 3 inf + 0 16.102 * * [simplify]: Extracting #2: cost 8 inf + 1 16.102 * * [simplify]: Extracting #3: cost 6 inf + 45 16.102 * * [simplify]: Extracting #4: cost 7 inf + 45 16.102 * * [simplify]: Extracting #5: cost 1 inf + 1499 16.102 * * [simplify]: Extracting #6: cost 0 inf + 2343 16.102 * [simplify]: Simplified to (/.p16 i (+.p16 beta (+.p16 alpha (*.p16 i (real->posit16 2))))) 16.102 * [simplify]: Simplified (2 1 1) to (λ (alpha beta i) (/.p16 (*.p16 (/.p16 i (+.p16 beta (+.p16 alpha (*.p16 i (real->posit16 2))))) (*.p16 (/.p16 (+.p16 (+.p16 alpha beta) i) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i))) (+.p16 (*.p16 beta alpha) (*.p16 i (+.p16 (+.p16 alpha beta) i))))) (-.p16 (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i))) (real->posit16 1.0)))) 16.103 * * * * [progress]: [ 12 / 20 ] simplifiying candidate #posit16 2) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)))) (-.p16 (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i))) (real->posit16 1.0))))> 16.103 * [simplify]: Simplifying (*.p16 (*.p16 i (+.p16 (+.p16 alpha beta) i)) (+.p16 (*.p16 beta alpha) (*.p16 i (+.p16 (+.p16 alpha beta) i)))) 16.103 * * [simplify]: iters left: 5 (9 enodes) 16.105 * * [simplify]: iters left: 4 (35 enodes) 16.112 * * [simplify]: iters left: 3 (128 enodes) 16.164 * * [simplify]: Extracting #0: cost 1 inf + 0 16.165 * * [simplify]: Extracting #1: cost 39 inf + 0 16.165 * * [simplify]: Extracting #2: cost 167 inf + 1 16.166 * * [simplify]: Extracting #3: cost 185 inf + 9642 16.170 * * [simplify]: Extracting #4: cost 54 inf + 131260 16.178 * * [simplify]: Extracting #5: cost 0 inf + 183768 16.186 * [simplify]: Simplified to (*.p16 (*.p16 i (+.p16 i (+.p16 alpha beta))) (+.p16 (*.p16 beta alpha) (*.p16 i (+.p16 i (+.p16 alpha beta))))) 16.186 * [simplify]: Simplified (2 1 1) to (λ (alpha beta i) (/.p16 (/.p16 (*.p16 (*.p16 i (+.p16 i (+.p16 alpha beta))) (+.p16 (*.p16 beta alpha) (*.p16 i (+.p16 i (+.p16 alpha beta))))) (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)))) (-.p16 (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i))) (real->posit16 1.0)))) 16.186 * * * * [progress]: [ 13 / 20 ] simplifiying candidate #posit16 2) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i))))) (-.p16 (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i))) (real->posit16 1.0))))> 16.186 * * * * [progress]: [ 14 / 20 ] simplifiying candidate #posit16 2) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)))) (+.p16 (+.p16 (*.p16 beta alpha) (*.p16 i (+.p16 alpha beta))) (*.p16 i i))) (-.p16 (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i))) (real->posit16 1.0))))> 16.187 * [simplify]: Simplifying (*.p16 i i) 16.187 * * [simplify]: iters left: 1 (2 enodes) 16.187 * * [simplify]: Extracting #0: cost 1 inf + 0 16.187 * * [simplify]: Extracting #1: cost 2 inf + 0 16.187 * * [simplify]: Extracting #2: cost 1 inf + 1 16.187 * * [simplify]: Extracting #3: cost 0 inf + 322 16.187 * [simplify]: Simplified to (*.p16 i i) 16.187 * [simplify]: Simplified (2 1 2 2) to (λ (alpha beta i) (/.p16 (*.p16 (/.p16 (*.p16 i (+.p16 (+.p16 alpha beta) i)) (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)))) (+.p16 (+.p16 (*.p16 beta alpha) (*.p16 i (+.p16 alpha beta))) (*.p16 i i))) (-.p16 (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i))) (real->posit16 1.0)))) 16.187 * * * * [progress]: [ 15 / 20 ] simplifiying candidate #posit16 2) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)))) (+.p16 (+.p16 (*.p16 beta alpha) (*.p16 (+.p16 alpha beta) i)) (*.p16 i i))) (-.p16 (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i))) (real->posit16 1.0))))> 16.188 * [simplify]: Simplifying (*.p16 i i) 16.188 * * [simplify]: iters left: 1 (2 enodes) 16.188 * * [simplify]: Extracting #0: cost 1 inf + 0 16.188 * * [simplify]: Extracting #1: cost 2 inf + 0 16.188 * * [simplify]: Extracting #2: cost 1 inf + 1 16.188 * * [simplify]: Extracting #3: cost 0 inf + 322 16.188 * [simplify]: Simplified to (*.p16 i i) 16.188 * [simplify]: Simplified (2 1 2 2) to (λ (alpha beta i) (/.p16 (*.p16 (/.p16 (*.p16 i (+.p16 (+.p16 alpha beta) i)) (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)))) (+.p16 (+.p16 (*.p16 beta alpha) (*.p16 (+.p16 alpha beta) i)) (*.p16 i i))) (-.p16 (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i))) (real->posit16 1.0)))) 16.188 * * * * [progress]: [ 16 / 20 ] simplifiying candidate #posit16 2) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)))) (+.p16 (*.p16 i (+.p16 (+.p16 alpha beta) i)) (*.p16 beta alpha))) (-.p16 (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i))) (real->posit16 1.0))))> 16.188 * * * * [progress]: [ 17 / 20 ] simplifiying candidate #posit16 2) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)))) (+.p16 (*.p16 beta alpha) (*.p16 i (+.p16 (+.p16 alpha beta) i)))) (-.p16 (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i))) (real->posit16 1.0))))> 16.189 * [simplify]: Simplifying (+.p16 (*.p16 beta alpha) (*.p16 i (+.p16 (+.p16 alpha beta) i))) 16.189 * * [simplify]: iters left: 4 (8 enodes) 16.190 * * [simplify]: iters left: 3 (26 enodes) 16.195 * * [simplify]: iters left: 2 (53 enodes) 16.204 * * [simplify]: iters left: 1 (91 enodes) 16.217 * * [simplify]: Extracting #0: cost 1 inf + 0 16.218 * * [simplify]: Extracting #1: cost 24 inf + 0 16.218 * * [simplify]: Extracting #2: cost 31 inf + 0 16.218 * * [simplify]: Extracting #3: cost 26 inf + 366 16.218 * * [simplify]: Extracting #4: cost 9 inf + 8250 16.219 * * [simplify]: Extracting #5: cost 0 inf + 15077 16.220 * [simplify]: Simplified to (+.p16 (*.p16 alpha (+.p16 beta i)) (*.p16 (+.p16 beta i) i)) 16.220 * [simplify]: Simplified (2 1 2) to (λ (alpha beta i) (/.p16 (*.p16 (/.p16 (*.p16 i (+.p16 (+.p16 alpha beta) i)) (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)))) (+.p16 (*.p16 alpha (+.p16 beta i)) (*.p16 (+.p16 beta i) i))) (-.p16 (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i))) (real->posit16 1.0)))) 16.220 * * * * [progress]: [ 18 / 20 ] simplifiying candidate #posit16 2) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)))) (+.p16 (*.p16 beta alpha) (*.p16 i (+.p16 (+.p16 alpha beta) i)))) (-.p16 (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i))) (real->posit16 1.0))))> 16.220 * [simplify]: Simplifying (+.p16 (*.p16 beta alpha) (*.p16 i (+.p16 (+.p16 alpha beta) i))) 16.221 * * [simplify]: iters left: 4 (8 enodes) 16.222 * * [simplify]: iters left: 3 (26 enodes) 16.231 * * [simplify]: iters left: 2 (53 enodes) 16.249 * * [simplify]: iters left: 1 (91 enodes) 16.277 * * [simplify]: Extracting #0: cost 1 inf + 0 16.277 * * [simplify]: Extracting #1: cost 24 inf + 0 16.277 * * [simplify]: Extracting #2: cost 31 inf + 0 16.277 * * [simplify]: Extracting #3: cost 26 inf + 366 16.278 * * [simplify]: Extracting #4: cost 9 inf + 8250 16.280 * * [simplify]: Extracting #5: cost 0 inf + 15077 16.281 * [simplify]: Simplified to (+.p16 (*.p16 alpha (+.p16 beta i)) (*.p16 (+.p16 beta i) i)) 16.281 * [simplify]: Simplified (2 1 2) to (λ (alpha beta i) (/.p16 (*.p16 (/.p16 (*.p16 i (+.p16 (+.p16 alpha beta) i)) (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)))) (+.p16 (*.p16 alpha (+.p16 beta i)) (*.p16 (+.p16 beta i) i))) (-.p16 (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i))) (real->posit16 1.0)))) 16.282 * * * * [progress]: [ 19 / 20 ] simplifiying candidate #posit16 2) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)))) (+.p16 (*.p16 beta alpha) (*.p16 i (+.p16 (+.p16 alpha beta) i)))) (-.p16 (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i))) (real->posit16 1.0))))> 16.282 * [simplify]: Simplifying (+.p16 (*.p16 beta alpha) (*.p16 i (+.p16 (+.p16 alpha beta) i))) 16.282 * * [simplify]: iters left: 4 (8 enodes) 16.286 * * [simplify]: iters left: 3 (26 enodes) 16.295 * * [simplify]: iters left: 2 (53 enodes) 16.312 * * [simplify]: iters left: 1 (91 enodes) 16.336 * * [simplify]: Extracting #0: cost 1 inf + 0 16.337 * * [simplify]: Extracting #1: cost 24 inf + 0 16.337 * * [simplify]: Extracting #2: cost 31 inf + 0 16.337 * * [simplify]: Extracting #3: cost 26 inf + 366 16.338 * * [simplify]: Extracting #4: cost 9 inf + 8250 16.339 * * [simplify]: Extracting #5: cost 0 inf + 15077 16.340 * [simplify]: Simplified to (+.p16 (*.p16 alpha (+.p16 beta i)) (*.p16 (+.p16 beta i) i)) 16.340 * [simplify]: Simplified (2 1 2) to (λ (alpha beta i) (/.p16 (*.p16 (/.p16 (*.p16 i (+.p16 (+.p16 alpha beta) i)) (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)))) (+.p16 (*.p16 alpha (+.p16 beta i)) (*.p16 (+.p16 beta i) i))) (-.p16 (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i))) (real->posit16 1.0)))) 16.341 * * * * [progress]: [ 20 / 20 ] simplifiying candidate #posit16 2) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)))) (+.p16 (*.p16 beta alpha) (*.p16 i (+.p16 (+.p16 alpha beta) i)))) (-.p16 (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i))) (real->posit16 1.0))))> 16.341 * [simplify]: Simplifying (+.p16 (*.p16 beta alpha) (*.p16 i (+.p16 (+.p16 alpha beta) i))) 16.341 * * [simplify]: iters left: 4 (8 enodes) 16.344 * * [simplify]: iters left: 3 (26 enodes) 16.356 * * [simplify]: iters left: 2 (53 enodes) 16.373 * * [simplify]: iters left: 1 (91 enodes) 16.401 * * [simplify]: Extracting #0: cost 1 inf + 0 16.402 * * [simplify]: Extracting #1: cost 24 inf + 0 16.402 * * [simplify]: Extracting #2: cost 31 inf + 0 16.402 * * [simplify]: Extracting #3: cost 26 inf + 366 16.403 * * [simplify]: Extracting #4: cost 9 inf + 8250 16.404 * * [simplify]: Extracting #5: cost 0 inf + 15077 16.406 * [simplify]: Simplified to (+.p16 (*.p16 alpha (+.p16 beta i)) (*.p16 (+.p16 beta i) i)) 16.406 * [simplify]: Simplified (2 1 2) to (λ (alpha beta i) (/.p16 (*.p16 (/.p16 (*.p16 i (+.p16 (+.p16 alpha beta) i)) (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)))) (+.p16 (*.p16 alpha (+.p16 beta i)) (*.p16 (+.p16 beta i) i))) (-.p16 (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i))) (real->posit16 1.0)))) 16.407 * * * [progress]: adding candidates to table 17.229 * * [progress]: iteration 4 / 4 17.229 * * * [progress]: picking best candidate 17.575 * * * * [pick]: Picked #posit16 2) i))) (/.p16 (+.p16 (+.p16 alpha beta) i) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)))) (+.p16 (*.p16 beta alpha) (*.p16 i (+.p16 (+.p16 alpha beta) i)))) (-.p16 (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i))) (real->posit16 1.0))))> 17.575 * * * [progress]: localizing error 18.127 * * * [progress]: generating rewritten candidates 18.127 * * * * [progress]: [ 1 / 4 ] rewriting at (2) 18.141 * * * * [progress]: [ 2 / 4 ] rewriting at (2 1 1 2) 18.174 * * * * [progress]: [ 3 / 4 ] rewriting at (2 1 1 1) 18.192 * * * * [progress]: [ 4 / 4 ] rewriting at (2 1) 18.202 * * * [progress]: generating series expansions 18.202 * * * * [progress]: [ 1 / 4 ] generating series at (2) 18.202 * * * * [progress]: [ 2 / 4 ] generating series at (2 1 1 2) 18.202 * * * * [progress]: [ 3 / 4 ] generating series at (2 1 1 1) 18.202 * * * * [progress]: [ 4 / 4 ] generating series at (2 1) 18.202 * * * [progress]: simplifying candidates 18.202 * * * * [progress]: [ 1 / 16 ] simplifiying candidate #posit16 2) i))) (/.p16 (+.p16 (+.p16 alpha beta) i) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)))) (+.p16 (*.p16 beta alpha) (*.p16 i (+.p16 (+.p16 alpha beta) i)))) (+.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (real->posit16 1.0))) (-.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (real->posit16 1.0))))> 18.202 * [simplify]: Simplifying (-.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (real->posit16 1.0)) 18.202 * * [simplify]: iters left: 4 (11 enodes) 18.209 * * [simplify]: iters left: 3 (33 enodes) 18.221 * * [simplify]: iters left: 2 (87 enodes) 18.268 * * [simplify]: iters left: 1 (455 enodes) 19.013 * * [simplify]: Extracting #0: cost 1 inf + 0 19.014 * * [simplify]: Extracting #1: cost 41 inf + 0 19.015 * * [simplify]: Extracting #2: cost 340 inf + 2 19.021 * * [simplify]: Extracting #3: cost 944 inf + 2428 19.033 * * [simplify]: Extracting #4: cost 917 inf + 30276 19.067 * * [simplify]: Extracting #5: cost 642 inf + 234865 19.170 * * [simplify]: Extracting #6: cost 130 inf + 773963 19.252 * * [simplify]: Extracting #7: cost 0 inf + 938356 19.335 * [simplify]: Simplified to (+.p16 (-.p16 (+.p16 beta alpha) (real->posit16 1.0)) (*.p16 (real->posit16 2) i)) 19.335 * [simplify]: Simplified (2 2) to (λ (alpha beta i) (/.p16 (/.p16 (*.p16 (*.p16 (/.p16 i (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i))) (/.p16 (+.p16 (+.p16 alpha beta) i) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)))) (+.p16 (*.p16 beta alpha) (*.p16 i (+.p16 (+.p16 alpha beta) i)))) (+.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (real->posit16 1.0))) (+.p16 (-.p16 (+.p16 beta alpha) (real->posit16 1.0)) (*.p16 (real->posit16 2) i)))) 19.335 * * * * [progress]: [ 2 / 16 ] simplifiying candidate #posit16 2) i))) (/.p16 (+.p16 (+.p16 alpha beta) i) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)))) (/.p16 (-.p16 (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i))) (real->posit16 1.0)) (+.p16 (*.p16 beta alpha) (*.p16 i (+.p16 (+.p16 alpha beta) i))))))> 19.335 * [simplify]: Simplifying (*.p16 (/.p16 i (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i))) (/.p16 (+.p16 (+.p16 alpha beta) i) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)))) 19.336 * * [simplify]: iters left: 5 (12 enodes) 19.340 * * [simplify]: iters left: 4 (32 enodes) 19.351 * * [simplify]: iters left: 3 (68 enodes) 19.378 * * [simplify]: iters left: 2 (136 enodes) 19.431 * * [simplify]: iters left: 1 (270 enodes) 19.498 * * [simplify]: Extracting #0: cost 1 inf + 0 19.498 * * [simplify]: Extracting #1: cost 21 inf + 0 19.498 * * [simplify]: Extracting #2: cost 52 inf + 1 19.499 * * [simplify]: Extracting #3: cost 98 inf + 1453 19.501 * * [simplify]: Extracting #4: cost 87 inf + 4997 19.502 * * [simplify]: Extracting #5: cost 74 inf + 12235 19.509 * * [simplify]: Extracting #6: cost 14 inf + 67140 19.521 * * [simplify]: Extracting #7: cost 0 inf + 80273 19.534 * [simplify]: Simplified to (*.p16 (/.p16 i (*.p16 (+.p16 (*.p16 i (real->posit16 2)) (+.p16 alpha beta)) (+.p16 (*.p16 i (real->posit16 2)) (+.p16 alpha beta)))) (+.p16 (+.p16 beta i) alpha)) 19.534 * [simplify]: Simplified (2 1) to (λ (alpha beta i) (/.p16 (*.p16 (/.p16 i (*.p16 (+.p16 (*.p16 i (real->posit16 2)) (+.p16 alpha beta)) (+.p16 (*.p16 i (real->posit16 2)) (+.p16 alpha beta)))) (+.p16 (+.p16 beta i) alpha)) (/.p16 (-.p16 (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i))) (real->posit16 1.0)) (+.p16 (*.p16 beta alpha) (*.p16 i (+.p16 (+.p16 alpha beta) i)))))) 19.535 * * * * [progress]: [ 3 / 16 ] simplifiying candidate #posit16 2) i))) (/.p16 (+.p16 (+.p16 alpha beta) i) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)))) (+.p16 (*.p16 beta alpha) (*.p16 i (+.p16 (+.p16 alpha beta) i)))) (-.p16 (*.p16 (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i))) (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)))) (*.p16 (real->posit16 1.0) (real->posit16 1.0)))) (+.p16 (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i))) (real->posit16 1.0))))> 19.535 * [simplify]: Simplifying (+.p16 (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i))) (real->posit16 1.0)) 19.535 * * [simplify]: iters left: 5 (12 enodes) 19.542 * * [simplify]: iters left: 4 (32 enodes) 19.553 * * [simplify]: iters left: 3 (90 enodes) 19.609 * * [simplify]: iters left: 2 (378 enodes) 19.997 * * [simplify]: Extracting #0: cost 1 inf + 0 19.998 * * [simplify]: Extracting #1: cost 90 inf + 0 19.999 * * [simplify]: Extracting #2: cost 387 inf + 0 20.001 * * [simplify]: Extracting #3: cost 379 inf + 3950 20.007 * * [simplify]: Extracting #4: cost 271 inf + 84531 20.055 * * [simplify]: Extracting #5: cost 20 inf + 357584 20.103 * * [simplify]: Extracting #6: cost 0 inf + 383761 20.130 * [simplify]: Simplified to (+.p16 (real->posit16 1.0) (*.p16 (+.p16 (+.p16 beta alpha) (*.p16 (real->posit16 2) i)) (+.p16 (+.p16 beta alpha) (*.p16 (real->posit16 2) i)))) 20.130 * [simplify]: Simplified (2 2) to (λ (alpha beta i) (*.p16 (/.p16 (*.p16 (*.p16 (/.p16 i (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i))) (/.p16 (+.p16 (+.p16 alpha beta) i) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)))) (+.p16 (*.p16 beta alpha) (*.p16 i (+.p16 (+.p16 alpha beta) i)))) (-.p16 (*.p16 (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i))) (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)))) (*.p16 (real->posit16 1.0) (real->posit16 1.0)))) (+.p16 (real->posit16 1.0) (*.p16 (+.p16 (+.p16 beta alpha) (*.p16 (real->posit16 2) i)) (+.p16 (+.p16 beta alpha) (*.p16 (real->posit16 2) i)))))) 20.130 * * * * [progress]: [ 4 / 16 ] simplifiying candidate #posit16 2) i))) (+.p16 (+.p16 alpha beta) i)) (+.p16 (*.p16 beta alpha) (*.p16 i (+.p16 (+.p16 alpha beta) i)))) (*.p16 (-.p16 (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i))) (real->posit16 1.0)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)))))> 20.130 * [simplify]: Simplifying (*.p16 (*.p16 (/.p16 i (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i))) (+.p16 (+.p16 alpha beta) i)) (+.p16 (*.p16 beta alpha) (*.p16 i (+.p16 (+.p16 alpha beta) i)))) 20.130 * * [simplify]: iters left: 6 (15 enodes) 20.135 * * [simplify]: iters left: 5 (55 enodes) 20.150 * * [simplify]: iters left: 4 (211 enodes) 20.319 * * [simplify]: Extracting #0: cost 1 inf + 0 20.319 * * [simplify]: Extracting #1: cost 51 inf + 0 20.320 * * [simplify]: Extracting #2: cost 294 inf + 1 20.322 * * [simplify]: Extracting #3: cost 338 inf + 15340 20.327 * * [simplify]: Extracting #4: cost 249 inf + 93433 20.338 * * [simplify]: Extracting #5: cost 187 inf + 182628 20.360 * * [simplify]: Extracting #6: cost 2 inf + 513246 20.385 * * [simplify]: Extracting #7: cost 0 inf + 516894 20.409 * [simplify]: Simplified to (/.p16 (*.p16 (*.p16 i (+.p16 i (+.p16 alpha beta))) (+.p16 (*.p16 beta alpha) (*.p16 i (+.p16 i (+.p16 alpha beta))))) (+.p16 (*.p16 i (real->posit16 2)) (+.p16 alpha beta))) 20.409 * [simplify]: Simplified (2 1) to (λ (alpha beta i) (/.p16 (/.p16 (*.p16 (*.p16 i (+.p16 i (+.p16 alpha beta))) (+.p16 (*.p16 beta alpha) (*.p16 i (+.p16 i (+.p16 alpha beta))))) (+.p16 (*.p16 i (real->posit16 2)) (+.p16 alpha beta))) (*.p16 (-.p16 (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i))) (real->posit16 1.0)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i))))) 20.409 * * * * [progress]: [ 5 / 16 ] simplifiying candidate #posit16 2) i)))) (+.p16 (*.p16 beta alpha) (*.p16 i (+.p16 (+.p16 alpha beta) i)))) (*.p16 (-.p16 (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i))) (real->posit16 1.0)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)))))> 20.409 * [simplify]: Simplifying (*.p16 (*.p16 i (/.p16 (+.p16 (+.p16 alpha beta) i) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)))) (+.p16 (*.p16 beta alpha) (*.p16 i (+.p16 (+.p16 alpha beta) i)))) 20.409 * * [simplify]: iters left: 6 (15 enodes) 20.414 * * [simplify]: iters left: 5 (49 enodes) 20.424 * * [simplify]: iters left: 4 (152 enodes) 20.488 * * [simplify]: Extracting #0: cost 1 inf + 0 20.488 * * [simplify]: Extracting #1: cost 25 inf + 0 20.490 * * [simplify]: Extracting #2: cost 119 inf + 1 20.491 * * [simplify]: Extracting #3: cost 156 inf + 1090 20.495 * * [simplify]: Extracting #4: cost 99 inf + 45852 20.503 * * [simplify]: Extracting #5: cost 71 inf + 71849 20.510 * * [simplify]: Extracting #6: cost 64 inf + 77272 20.526 * * [simplify]: Extracting #7: cost 5 inf + 172266 20.546 * * [simplify]: Extracting #8: cost 0 inf + 182526 20.567 * [simplify]: Simplified to (/.p16 (*.p16 (*.p16 i (+.p16 i (+.p16 alpha beta))) (+.p16 (*.p16 beta alpha) (*.p16 i (+.p16 i (+.p16 alpha beta))))) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i))) 20.567 * [simplify]: Simplified (2 1) to (λ (alpha beta i) (/.p16 (/.p16 (*.p16 (*.p16 i (+.p16 i (+.p16 alpha beta))) (+.p16 (*.p16 beta alpha) (*.p16 i (+.p16 i (+.p16 alpha beta))))) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i))) (*.p16 (-.p16 (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i))) (real->posit16 1.0)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i))))) 20.568 * * * * [progress]: [ 6 / 16 ] simplifiying candidate #posit16 2) i))) (/.p16 (+.p16 (+.p16 alpha beta) i) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)))) (+.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (real->posit16 1.0))) (/.p16 (+.p16 (*.p16 beta alpha) (*.p16 i (+.p16 (+.p16 alpha beta) i))) (-.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (real->posit16 1.0)))))> 20.568 * [simplify]: Simplifying (/.p16 (*.p16 (/.p16 i (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i))) (/.p16 (+.p16 (+.p16 alpha beta) i) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)))) (+.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (real->posit16 1.0))) 20.568 * * [simplify]: iters left: 6 (16 enodes) 20.576 * * [simplify]: iters left: 5 (42 enodes) 20.591 * * [simplify]: iters left: 4 (100 enodes) 20.624 * * [simplify]: iters left: 3 (308 enodes) 20.789 * * [simplify]: Extracting #0: cost 1 inf + 0 20.789 * * [simplify]: Extracting #1: cost 36 inf + 0 20.789 * * [simplify]: Extracting #2: cost 174 inf + 1 20.791 * * [simplify]: Extracting #3: cost 421 inf + 1301 20.793 * * [simplify]: Extracting #4: cost 398 inf + 7591 20.806 * * [simplify]: Extracting #5: cost 173 inf + 220846 20.834 * * [simplify]: Extracting #6: cost 1 inf + 434687 20.877 * * [simplify]: Extracting #7: cost 0 inf + 435131 20.908 * [simplify]: Simplified to (/.p16 (*.p16 i (+.p16 i (+.p16 alpha beta))) (*.p16 (*.p16 (+.p16 (+.p16 (*.p16 i (real->posit16 2)) (+.p16 (real->posit16 1.0) beta)) alpha) (+.p16 (*.p16 i (real->posit16 2)) (+.p16 alpha beta))) (+.p16 (*.p16 i (real->posit16 2)) (+.p16 alpha beta)))) 20.908 * [simplify]: Simplified (2 1) to (λ (alpha beta i) (*.p16 (/.p16 (*.p16 i (+.p16 i (+.p16 alpha beta))) (*.p16 (*.p16 (+.p16 (+.p16 (*.p16 i (real->posit16 2)) (+.p16 (real->posit16 1.0) beta)) alpha) (+.p16 (*.p16 i (real->posit16 2)) (+.p16 alpha beta))) (+.p16 (*.p16 i (real->posit16 2)) (+.p16 alpha beta)))) (/.p16 (+.p16 (*.p16 beta alpha) (*.p16 i (+.p16 (+.p16 alpha beta) i))) (-.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (real->posit16 1.0))))) 20.908 * [simplify]: Simplifying (/.p16 (+.p16 (*.p16 beta alpha) (*.p16 i (+.p16 (+.p16 alpha beta) i))) (-.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (real->posit16 1.0))) 20.908 * * [simplify]: iters left: 5 (16 enodes) 20.912 * * [simplify]: iters left: 4 (49 enodes) 20.923 * * [simplify]: iters left: 3 (132 enodes) 20.965 * * [simplify]: Extracting #0: cost 1 inf + 0 20.965 * * [simplify]: Extracting #1: cost 23 inf + 0 20.965 * * [simplify]: Extracting #2: cost 112 inf + 0 20.965 * * [simplify]: Extracting #3: cost 184 inf + 366 20.966 * * [simplify]: Extracting #4: cost 189 inf + 7206 20.968 * * [simplify]: Extracting #5: cost 139 inf + 26225 20.976 * * [simplify]: Extracting #6: cost 32 inf + 109682 20.986 * * [simplify]: Extracting #7: cost 0 inf + 157117 21.002 * [simplify]: Simplified to (/.p16 (+.p16 (*.p16 alpha beta) (*.p16 (+.p16 (+.p16 alpha beta) i) i)) (-.p16 (+.p16 (*.p16 (real->posit16 2) i) (+.p16 alpha beta)) (real->posit16 1.0))) 21.003 * [simplify]: Simplified (2 2) to (λ (alpha beta i) (*.p16 (/.p16 (*.p16 (/.p16 i (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i))) (/.p16 (+.p16 (+.p16 alpha beta) i) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)))) (+.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (real->posit16 1.0))) (/.p16 (+.p16 (*.p16 alpha beta) (*.p16 (+.p16 (+.p16 alpha beta) i) i)) (-.p16 (+.p16 (*.p16 (real->posit16 2) i) (+.p16 alpha beta)) (real->posit16 1.0))))) 21.003 * * * * [progress]: [ 7 / 16 ] simplifiying candidate #posit16 2) i))) (/.p16 (+.p16 (+.p16 alpha beta) i) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)))) (*.p16 beta alpha)) (*.p16 (*.p16 (/.p16 i (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i))) (/.p16 (+.p16 (+.p16 alpha beta) i) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)))) (*.p16 i (+.p16 (+.p16 alpha beta) i)))) (-.p16 (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i))) (real->posit16 1.0))))> 21.003 * [simplify]: Simplifying (*.p16 (*.p16 (/.p16 i (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i))) (/.p16 (+.p16 (+.p16 alpha beta) i) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)))) (*.p16 i (+.p16 (+.p16 alpha beta) i))) 21.004 * * [simplify]: iters left: 6 (14 enodes) 21.010 * * [simplify]: iters left: 5 (45 enodes) 21.031 * * [simplify]: iters left: 4 (159 enodes) 21.154 * * [simplify]: Extracting #0: cost 1 inf + 0 21.154 * * [simplify]: Extracting #1: cost 37 inf + 0 21.155 * * [simplify]: Extracting #2: cost 165 inf + 1 21.156 * * [simplify]: Extracting #3: cost 164 inf + 2862 21.159 * * [simplify]: Extracting #4: cost 138 inf + 20618 21.162 * * [simplify]: Extracting #5: cost 126 inf + 30256 21.180 * * [simplify]: Extracting #6: cost 15 inf + 206778 21.207 * * [simplify]: Extracting #7: cost 0 inf + 233518 21.226 * [simplify]: Simplified to (*.p16 (*.p16 (/.p16 i (+.p16 (*.p16 i (real->posit16 2)) (+.p16 alpha beta))) (+.p16 alpha (+.p16 beta i))) (*.p16 (/.p16 i (+.p16 (*.p16 i (real->posit16 2)) (+.p16 alpha beta))) (+.p16 alpha (+.p16 beta i)))) 21.226 * [simplify]: Simplified (2 1 2) to (λ (alpha beta i) (/.p16 (+.p16 (*.p16 (*.p16 (/.p16 i (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i))) (/.p16 (+.p16 (+.p16 alpha beta) i) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)))) (*.p16 beta alpha)) (*.p16 (*.p16 (/.p16 i (+.p16 (*.p16 i (real->posit16 2)) (+.p16 alpha beta))) (+.p16 alpha (+.p16 beta i))) (*.p16 (/.p16 i (+.p16 (*.p16 i (real->posit16 2)) (+.p16 alpha beta))) (+.p16 alpha (+.p16 beta i))))) (-.p16 (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i))) (real->posit16 1.0)))) 21.227 * * * * [progress]: [ 8 / 16 ] simplifiying candidate #posit16 2) i))) (/.p16 (+.p16 (+.p16 alpha beta) i) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i))))) (*.p16 (*.p16 i (+.p16 (+.p16 alpha beta) i)) (*.p16 (/.p16 i (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i))) (/.p16 (+.p16 (+.p16 alpha beta) i) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)))))) (-.p16 (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i))) (real->posit16 1.0))))> 21.227 * [simplify]: Simplifying (*.p16 (*.p16 i (+.p16 (+.p16 alpha beta) i)) (*.p16 (/.p16 i (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i))) (/.p16 (+.p16 (+.p16 alpha beta) i) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i))))) 21.227 * * [simplify]: iters left: 6 (14 enodes) 21.233 * * [simplify]: iters left: 5 (45 enodes) 21.242 * * [simplify]: iters left: 4 (135 enodes) 21.287 * * [simplify]: Extracting #0: cost 1 inf + 0 21.287 * * [simplify]: Extracting #1: cost 40 inf + 0 21.288 * * [simplify]: Extracting #2: cost 153 inf + 1 21.288 * * [simplify]: Extracting #3: cost 141 inf + 4068 21.289 * * [simplify]: Extracting #4: cost 129 inf + 11420 21.291 * * [simplify]: Extracting #5: cost 125 inf + 12827 21.292 * * [simplify]: Extracting #6: cost 121 inf + 15480 21.306 * * [simplify]: Extracting #7: cost 33 inf + 157711 21.319 * * [simplify]: Extracting #8: cost 0 inf + 218563 21.331 * [simplify]: Simplified to (*.p16 (/.p16 (*.p16 i (+.p16 alpha (+.p16 beta i))) (+.p16 alpha (+.p16 (*.p16 (real->posit16 2) i) beta))) (/.p16 (*.p16 i (+.p16 alpha (+.p16 beta i))) (+.p16 alpha (+.p16 (*.p16 (real->posit16 2) i) beta)))) 21.331 * [simplify]: Simplified (2 1 2) to (λ (alpha beta i) (/.p16 (+.p16 (*.p16 (*.p16 beta alpha) (*.p16 (/.p16 i (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i))) (/.p16 (+.p16 (+.p16 alpha beta) i) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i))))) (*.p16 (/.p16 (*.p16 i (+.p16 alpha (+.p16 beta i))) (+.p16 alpha (+.p16 (*.p16 (real->posit16 2) i) beta))) (/.p16 (*.p16 i (+.p16 alpha (+.p16 beta i))) (+.p16 alpha (+.p16 (*.p16 (real->posit16 2) i) beta))))) (-.p16 (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i))) (real->posit16 1.0)))) 21.332 * * * * [progress]: [ 9 / 16 ] simplifiying candidate #posit16 2) i))) (*.p16 (/.p16 (+.p16 (+.p16 alpha beta) i) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i))) (+.p16 (*.p16 beta alpha) (*.p16 i (+.p16 (+.p16 alpha beta) i))))) (-.p16 (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i))) (real->posit16 1.0))))> 21.332 * [simplify]: Simplifying (/.p16 i (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i))) 21.332 * * [simplify]: iters left: 4 (9 enodes) 21.334 * * [simplify]: iters left: 3 (21 enodes) 21.338 * * [simplify]: iters left: 2 (27 enodes) 21.342 * * [simplify]: iters left: 1 (28 enodes) 21.346 * * [simplify]: Extracting #0: cost 1 inf + 0 21.346 * * [simplify]: Extracting #1: cost 3 inf + 0 21.346 * * [simplify]: Extracting #2: cost 8 inf + 1 21.346 * * [simplify]: Extracting #3: cost 6 inf + 45 21.346 * * [simplify]: Extracting #4: cost 7 inf + 45 21.346 * * [simplify]: Extracting #5: cost 1 inf + 1499 21.347 * * [simplify]: Extracting #6: cost 0 inf + 2343 21.347 * [simplify]: Simplified to (/.p16 i (+.p16 beta (+.p16 alpha (*.p16 i (real->posit16 2))))) 21.347 * [simplify]: Simplified (2 1 1) to (λ (alpha beta i) (/.p16 (*.p16 (/.p16 i (+.p16 beta (+.p16 alpha (*.p16 i (real->posit16 2))))) (*.p16 (/.p16 (+.p16 (+.p16 alpha beta) i) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i))) (+.p16 (*.p16 beta alpha) (*.p16 i (+.p16 (+.p16 alpha beta) i))))) (-.p16 (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i))) (real->posit16 1.0)))) 21.347 * * * * [progress]: [ 10 / 16 ] simplifiying candidate #posit16 2) i))) (+.p16 (+.p16 alpha beta) i)) (+.p16 (*.p16 beta alpha) (*.p16 i (+.p16 (+.p16 alpha beta) i)))) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i))) (-.p16 (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i))) (real->posit16 1.0))))> 21.347 * [simplify]: Simplifying (*.p16 (*.p16 (/.p16 i (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i))) (+.p16 (+.p16 alpha beta) i)) (+.p16 (*.p16 beta alpha) (*.p16 i (+.p16 (+.p16 alpha beta) i)))) 21.347 * * [simplify]: iters left: 6 (15 enodes) 21.351 * * [simplify]: iters left: 5 (55 enodes) 21.366 * * [simplify]: iters left: 4 (211 enodes) 21.469 * * [simplify]: Extracting #0: cost 1 inf + 0 21.469 * * [simplify]: Extracting #1: cost 51 inf + 0 21.469 * * [simplify]: Extracting #2: cost 294 inf + 1 21.471 * * [simplify]: Extracting #3: cost 338 inf + 15340 21.479 * * [simplify]: Extracting #4: cost 249 inf + 93433 21.495 * * [simplify]: Extracting #5: cost 187 inf + 182628 21.545 * * [simplify]: Extracting #6: cost 2 inf + 513246 21.595 * * [simplify]: Extracting #7: cost 0 inf + 516894 21.642 * [simplify]: Simplified to (/.p16 (*.p16 (*.p16 i (+.p16 i (+.p16 alpha beta))) (+.p16 (*.p16 beta alpha) (*.p16 i (+.p16 i (+.p16 alpha beta))))) (+.p16 (*.p16 i (real->posit16 2)) (+.p16 alpha beta))) 21.642 * [simplify]: Simplified (2 1 1) to (λ (alpha beta i) (/.p16 (/.p16 (/.p16 (*.p16 (*.p16 i (+.p16 i (+.p16 alpha beta))) (+.p16 (*.p16 beta alpha) (*.p16 i (+.p16 i (+.p16 alpha beta))))) (+.p16 (*.p16 i (real->posit16 2)) (+.p16 alpha beta))) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i))) (-.p16 (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i))) (real->posit16 1.0)))) 21.643 * * * * [progress]: [ 11 / 16 ] simplifiying candidate #posit16 2) i)))) (+.p16 (*.p16 beta alpha) (*.p16 i (+.p16 (+.p16 alpha beta) i)))) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i))) (-.p16 (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i))) (real->posit16 1.0))))> 21.643 * [simplify]: Simplifying (*.p16 (*.p16 i (/.p16 (+.p16 (+.p16 alpha beta) i) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)))) (+.p16 (*.p16 beta alpha) (*.p16 i (+.p16 (+.p16 alpha beta) i)))) 21.643 * * [simplify]: iters left: 6 (15 enodes) 21.650 * * [simplify]: iters left: 5 (49 enodes) 21.672 * * [simplify]: iters left: 4 (152 enodes) 21.765 * * [simplify]: Extracting #0: cost 1 inf + 0 21.765 * * [simplify]: Extracting #1: cost 25 inf + 0 21.766 * * [simplify]: Extracting #2: cost 119 inf + 1 21.767 * * [simplify]: Extracting #3: cost 156 inf + 1090 21.770 * * [simplify]: Extracting #4: cost 99 inf + 45852 21.776 * * [simplify]: Extracting #5: cost 71 inf + 71849 21.783 * * [simplify]: Extracting #6: cost 64 inf + 77272 21.798 * * [simplify]: Extracting #7: cost 5 inf + 172266 21.820 * * [simplify]: Extracting #8: cost 0 inf + 182526 21.840 * [simplify]: Simplified to (/.p16 (*.p16 (*.p16 i (+.p16 i (+.p16 alpha beta))) (+.p16 (*.p16 beta alpha) (*.p16 i (+.p16 i (+.p16 alpha beta))))) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i))) 21.840 * [simplify]: Simplified (2 1 1) to (λ (alpha beta i) (/.p16 (/.p16 (/.p16 (*.p16 (*.p16 i (+.p16 i (+.p16 alpha beta))) (+.p16 (*.p16 beta alpha) (*.p16 i (+.p16 i (+.p16 alpha beta))))) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i))) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i))) (-.p16 (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i))) (real->posit16 1.0)))) 21.840 * * * * [progress]: [ 12 / 16 ] simplifiying candidate #posit16 2) i))) (/.p16 (+.p16 (+.p16 alpha beta) i) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i))))) (-.p16 (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i))) (real->posit16 1.0))))> 21.840 * * * * [progress]: [ 13 / 16 ] simplifiying candidate #posit16 2) i))) (/.p16 (+.p16 (+.p16 alpha beta) i) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)))) (+.p16 (*.p16 beta alpha) (*.p16 i (+.p16 (+.p16 alpha beta) i)))) (-.p16 (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i))) (real->posit16 1.0))))> 21.841 * [simplify]: Simplifying (/.p16 i (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i))) 21.841 * * [simplify]: iters left: 4 (9 enodes) 21.845 * * [simplify]: iters left: 3 (21 enodes) 21.852 * * [simplify]: iters left: 2 (27 enodes) 21.860 * * [simplify]: iters left: 1 (28 enodes) 21.867 * * [simplify]: Extracting #0: cost 1 inf + 0 21.868 * * [simplify]: Extracting #1: cost 3 inf + 0 21.868 * * [simplify]: Extracting #2: cost 8 inf + 1 21.868 * * [simplify]: Extracting #3: cost 6 inf + 45 21.868 * * [simplify]: Extracting #4: cost 7 inf + 45 21.868 * * [simplify]: Extracting #5: cost 1 inf + 1499 21.868 * * [simplify]: Extracting #6: cost 0 inf + 2343 21.869 * [simplify]: Simplified to (/.p16 i (+.p16 beta (+.p16 alpha (*.p16 i (real->posit16 2))))) 21.869 * [simplify]: Simplified (2 1 1 1) to (λ (alpha beta i) (/.p16 (*.p16 (*.p16 (/.p16 i (+.p16 beta (+.p16 alpha (*.p16 i (real->posit16 2))))) (/.p16 (+.p16 (+.p16 alpha beta) i) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)))) (+.p16 (*.p16 beta alpha) (*.p16 i (+.p16 (+.p16 alpha beta) i)))) (-.p16 (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i))) (real->posit16 1.0)))) 21.869 * [simplify]: Simplifying (/.p16 (+.p16 (+.p16 alpha beta) i) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i))) 21.869 * * [simplify]: iters left: 4 (10 enodes) 21.874 * * [simplify]: iters left: 3 (25 enodes) 21.877 * * [simplify]: iters left: 2 (37 enodes) 21.883 * * [simplify]: iters left: 1 (40 enodes) 21.889 * * [simplify]: Extracting #0: cost 1 inf + 0 21.889 * * [simplify]: Extracting #1: cost 3 inf + 0 21.889 * * [simplify]: Extracting #2: cost 12 inf + 0 21.889 * * [simplify]: Extracting #3: cost 9 inf + 45 21.889 * * [simplify]: Extracting #4: cost 7 inf + 212 21.889 * * [simplify]: Extracting #5: cost 6 inf + 213 21.889 * * [simplify]: Extracting #6: cost 4 inf + 536 21.889 * * [simplify]: Extracting #7: cost 0 inf + 2590 21.889 * [simplify]: Simplified to (/.p16 (+.p16 alpha (+.p16 i beta)) (+.p16 (+.p16 beta alpha) (*.p16 (real->posit16 2) i))) 21.890 * [simplify]: Simplified (2 1 1 2) to (λ (alpha beta i) (/.p16 (*.p16 (*.p16 (/.p16 i (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i))) (/.p16 (+.p16 alpha (+.p16 i beta)) (+.p16 (+.p16 beta alpha) (*.p16 (real->posit16 2) i)))) (+.p16 (*.p16 beta alpha) (*.p16 i (+.p16 (+.p16 alpha beta) i)))) (-.p16 (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i))) (real->posit16 1.0)))) 21.890 * * * * [progress]: [ 14 / 16 ] simplifiying candidate #posit16 2) i))) (/.p16 (+.p16 (+.p16 alpha beta) i) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)))) (+.p16 (*.p16 beta alpha) (*.p16 i (+.p16 (+.p16 alpha beta) i)))) (-.p16 (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i))) (real->posit16 1.0))))> 21.890 * [simplify]: Simplifying (/.p16 i (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i))) 21.890 * * [simplify]: iters left: 4 (9 enodes) 21.892 * * [simplify]: iters left: 3 (21 enodes) 21.898 * * [simplify]: iters left: 2 (27 enodes) 21.907 * * [simplify]: iters left: 1 (28 enodes) 21.916 * * [simplify]: Extracting #0: cost 1 inf + 0 21.916 * * [simplify]: Extracting #1: cost 3 inf + 0 21.916 * * [simplify]: Extracting #2: cost 8 inf + 1 21.917 * * [simplify]: Extracting #3: cost 6 inf + 45 21.917 * * [simplify]: Extracting #4: cost 7 inf + 45 21.917 * * [simplify]: Extracting #5: cost 1 inf + 1499 21.917 * * [simplify]: Extracting #6: cost 0 inf + 2343 21.918 * [simplify]: Simplified to (/.p16 i (+.p16 beta (+.p16 alpha (*.p16 i (real->posit16 2))))) 21.918 * [simplify]: Simplified (2 1 1 1) to (λ (alpha beta i) (/.p16 (*.p16 (*.p16 (/.p16 i (+.p16 beta (+.p16 alpha (*.p16 i (real->posit16 2))))) (/.p16 (+.p16 (+.p16 alpha beta) i) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)))) (+.p16 (*.p16 beta alpha) (*.p16 i (+.p16 (+.p16 alpha beta) i)))) (-.p16 (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i))) (real->posit16 1.0)))) 21.918 * [simplify]: Simplifying (/.p16 (+.p16 (+.p16 alpha beta) i) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i))) 21.918 * * [simplify]: iters left: 4 (10 enodes) 21.924 * * [simplify]: iters left: 3 (25 enodes) 21.933 * * [simplify]: iters left: 2 (37 enodes) 21.944 * * [simplify]: iters left: 1 (40 enodes) 21.957 * * [simplify]: Extracting #0: cost 1 inf + 0 21.957 * * [simplify]: Extracting #1: cost 3 inf + 0 21.957 * * [simplify]: Extracting #2: cost 12 inf + 0 21.957 * * [simplify]: Extracting #3: cost 9 inf + 45 21.957 * * [simplify]: Extracting #4: cost 7 inf + 212 21.958 * * [simplify]: Extracting #5: cost 6 inf + 213 21.958 * * [simplify]: Extracting #6: cost 4 inf + 536 21.958 * * [simplify]: Extracting #7: cost 0 inf + 2590 21.959 * [simplify]: Simplified to (/.p16 (+.p16 alpha (+.p16 i beta)) (+.p16 (+.p16 beta alpha) (*.p16 (real->posit16 2) i))) 21.959 * [simplify]: Simplified (2 1 1 2) to (λ (alpha beta i) (/.p16 (*.p16 (*.p16 (/.p16 i (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i))) (/.p16 (+.p16 alpha (+.p16 i beta)) (+.p16 (+.p16 beta alpha) (*.p16 (real->posit16 2) i)))) (+.p16 (*.p16 beta alpha) (*.p16 i (+.p16 (+.p16 alpha beta) i)))) (-.p16 (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i))) (real->posit16 1.0)))) 21.959 * * * * [progress]: [ 15 / 16 ] simplifiying candidate #posit16 2) i))) (/.p16 (+.p16 (+.p16 alpha beta) i) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)))) (+.p16 (*.p16 beta alpha) (*.p16 i (+.p16 (+.p16 alpha beta) i)))) (-.p16 (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i))) (real->posit16 1.0))))> 21.959 * [simplify]: Simplifying (/.p16 i (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i))) 21.959 * * [simplify]: iters left: 4 (9 enodes) 21.963 * * [simplify]: iters left: 3 (21 enodes) 21.970 * * [simplify]: iters left: 2 (27 enodes) 21.974 * * [simplify]: iters left: 1 (28 enodes) 21.977 * * [simplify]: Extracting #0: cost 1 inf + 0 21.977 * * [simplify]: Extracting #1: cost 3 inf + 0 21.978 * * [simplify]: Extracting #2: cost 8 inf + 1 21.978 * * [simplify]: Extracting #3: cost 6 inf + 45 21.978 * * [simplify]: Extracting #4: cost 7 inf + 45 21.978 * * [simplify]: Extracting #5: cost 1 inf + 1499 21.978 * * [simplify]: Extracting #6: cost 0 inf + 2343 21.978 * [simplify]: Simplified to (/.p16 i (+.p16 beta (+.p16 alpha (*.p16 i (real->posit16 2))))) 21.978 * [simplify]: Simplified (2 1 1 1) to (λ (alpha beta i) (/.p16 (*.p16 (*.p16 (/.p16 i (+.p16 beta (+.p16 alpha (*.p16 i (real->posit16 2))))) (/.p16 (+.p16 (+.p16 alpha beta) i) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)))) (+.p16 (*.p16 beta alpha) (*.p16 i (+.p16 (+.p16 alpha beta) i)))) (-.p16 (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i))) (real->posit16 1.0)))) 21.978 * [simplify]: Simplifying (/.p16 (+.p16 (+.p16 alpha beta) i) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i))) 21.979 * * [simplify]: iters left: 4 (10 enodes) 21.981 * * [simplify]: iters left: 3 (25 enodes) 21.985 * * [simplify]: iters left: 2 (37 enodes) 21.990 * * [simplify]: iters left: 1 (40 enodes) 21.995 * * [simplify]: Extracting #0: cost 1 inf + 0 21.995 * * [simplify]: Extracting #1: cost 3 inf + 0 21.996 * * [simplify]: Extracting #2: cost 12 inf + 0 21.996 * * [simplify]: Extracting #3: cost 9 inf + 45 21.996 * * [simplify]: Extracting #4: cost 7 inf + 212 21.996 * * [simplify]: Extracting #5: cost 6 inf + 213 21.996 * * [simplify]: Extracting #6: cost 4 inf + 536 21.996 * * [simplify]: Extracting #7: cost 0 inf + 2590 21.996 * [simplify]: Simplified to (/.p16 (+.p16 alpha (+.p16 i beta)) (+.p16 (+.p16 beta alpha) (*.p16 (real->posit16 2) i))) 21.996 * [simplify]: Simplified (2 1 1 2) to (λ (alpha beta i) (/.p16 (*.p16 (*.p16 (/.p16 i (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i))) (/.p16 (+.p16 alpha (+.p16 i beta)) (+.p16 (+.p16 beta alpha) (*.p16 (real->posit16 2) i)))) (+.p16 (*.p16 beta alpha) (*.p16 i (+.p16 (+.p16 alpha beta) i)))) (-.p16 (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i))) (real->posit16 1.0)))) 21.997 * * * * [progress]: [ 16 / 16 ] simplifiying candidate #posit16 2) i))) (/.p16 (+.p16 (+.p16 alpha beta) i) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)))) (+.p16 (*.p16 beta alpha) (*.p16 i (+.p16 (+.p16 alpha beta) i)))) (-.p16 (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i))) (real->posit16 1.0))))> 21.997 * [simplify]: Simplifying (/.p16 i (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i))) 21.997 * * [simplify]: iters left: 4 (9 enodes) 22.000 * * [simplify]: iters left: 3 (21 enodes) 22.007 * * [simplify]: iters left: 2 (27 enodes) 22.015 * * [simplify]: iters left: 1 (28 enodes) 22.023 * * [simplify]: Extracting #0: cost 1 inf + 0 22.023 * * [simplify]: Extracting #1: cost 3 inf + 0 22.023 * * [simplify]: Extracting #2: cost 8 inf + 1 22.023 * * [simplify]: Extracting #3: cost 6 inf + 45 22.024 * * [simplify]: Extracting #4: cost 7 inf + 45 22.024 * * [simplify]: Extracting #5: cost 1 inf + 1499 22.024 * * [simplify]: Extracting #6: cost 0 inf + 2343 22.025 * [simplify]: Simplified to (/.p16 i (+.p16 beta (+.p16 alpha (*.p16 i (real->posit16 2))))) 22.025 * [simplify]: Simplified (2 1 1 1) to (λ (alpha beta i) (/.p16 (*.p16 (*.p16 (/.p16 i (+.p16 beta (+.p16 alpha (*.p16 i (real->posit16 2))))) (/.p16 (+.p16 (+.p16 alpha beta) i) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)))) (+.p16 (*.p16 beta alpha) (*.p16 i (+.p16 (+.p16 alpha beta) i)))) (-.p16 (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i))) (real->posit16 1.0)))) 22.025 * [simplify]: Simplifying (/.p16 (+.p16 (+.p16 alpha beta) i) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i))) 22.025 * * [simplify]: iters left: 4 (10 enodes) 22.030 * * [simplify]: iters left: 3 (25 enodes) 22.038 * * [simplify]: iters left: 2 (37 enodes) 22.049 * * [simplify]: iters left: 1 (40 enodes) 22.060 * * [simplify]: Extracting #0: cost 1 inf + 0 22.060 * * [simplify]: Extracting #1: cost 3 inf + 0 22.060 * * [simplify]: Extracting #2: cost 12 inf + 0 22.060 * * [simplify]: Extracting #3: cost 9 inf + 45 22.060 * * [simplify]: Extracting #4: cost 7 inf + 212 22.061 * * [simplify]: Extracting #5: cost 6 inf + 213 22.061 * * [simplify]: Extracting #6: cost 4 inf + 536 22.061 * * [simplify]: Extracting #7: cost 0 inf + 2590 22.062 * [simplify]: Simplified to (/.p16 (+.p16 alpha (+.p16 i beta)) (+.p16 (+.p16 beta alpha) (*.p16 (real->posit16 2) i))) 22.062 * [simplify]: Simplified (2 1 1 2) to (λ (alpha beta i) (/.p16 (*.p16 (*.p16 (/.p16 i (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i))) (/.p16 (+.p16 alpha (+.p16 i beta)) (+.p16 (+.p16 beta alpha) (*.p16 (real->posit16 2) i)))) (+.p16 (*.p16 beta alpha) (*.p16 i (+.p16 (+.p16 alpha beta) i)))) (-.p16 (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i))) (real->posit16 1.0)))) 22.062 * * * [progress]: adding candidates to table 22.905 * [progress]: [Phase 3 of 3] Extracting. 22.906 * * [regime]: Finding splitpoints for: (#posit16 2) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i))) (+.p16 (*.p16 beta alpha) (*.p16 i (+.p16 (+.p16 alpha beta) i))))) (-.p16 (*.p16 (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i))) (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)))) (*.p16 (real->posit16 1.0) (real->posit16 1.0)))) (+.p16 (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i))) (real->posit16 1.0))))> #posit16 2) i))) (/.p16 (+.p16 (+.p16 alpha beta) i) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)))) (/.p16 (-.p16 (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i))) (real->posit16 1.0)) (+.p16 (*.p16 beta alpha) (*.p16 i (+.p16 (+.p16 alpha beta) i))))))> #posit16 2) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i))))) (*.p16 (*.p16 i (+.p16 (+.p16 alpha beta) i)) (/.p16 (*.p16 i (+.p16 (+.p16 alpha beta) i)) (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)))))) (-.p16 (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i))) (real->posit16 1.0))))> #posit16 2) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i))) (real->posit16 1.0)) (/.p16 (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i))) (+.p16 (*.p16 beta alpha) (*.p16 i (+.p16 (+.p16 alpha beta) i)))))))> #posit16 2) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)))) (+.p16 (+.p16 (*.p16 beta alpha) (*.p16 i (+.p16 alpha beta))) (*.p16 i i))) (-.p16 (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i))) (real->posit16 1.0))))> #posit16 2) i))) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i))) (-.p16 (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i))) (real->posit16 1.0))))> #posit16 2) i))) (/.p16 (-.p16 (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i))) (real->posit16 1.0)) (/.p16 (+.p16 (*.p16 beta alpha) (*.p16 i (+.p16 (+.p16 alpha beta) i))) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i))))))> #posit16 2) i))) (+.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (real->posit16 1.0))) (/.p16 (/.p16 (+.p16 (*.p16 beta alpha) (*.p16 i (+.p16 (+.p16 alpha beta) i))) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i))) (-.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (real->posit16 1.0)))))> #posit16 2) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)))) (-.p16 (*.p16 (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i))) (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)))) (*.p16 (real->posit16 1.0) (real->posit16 1.0)))) (+.p16 (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i))) (real->posit16 1.0))))> #posit16 2) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)))) (+.p16 (*.p16 beta alpha) (*.p16 i (+.p16 (+.p16 alpha beta) i)))) (-.p16 (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i))) (real->posit16 1.0))))> #posit16 2) i))) (/.p16 (+.p16 (+.p16 alpha beta) i) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)))) (+.p16 (*.p16 beta alpha) (*.p16 i (+.p16 (+.p16 alpha beta) i)))) (+.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (real->posit16 1.0))) (-.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (real->posit16 1.0))))> #posit16 2) i))) (*.p16 (/.p16 (+.p16 (+.p16 alpha beta) i) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i))) (+.p16 (*.p16 beta alpha) (*.p16 i (+.p16 (+.p16 alpha beta) i))))) (-.p16 (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i))) (real->posit16 1.0))))> #posit16 2) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i))) (real->posit16 1.0)) (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i))))))> #posit16 2) i))) (/.p16 (+.p16 (+.p16 alpha beta) i) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)))) (+.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (real->posit16 1.0))) (/.p16 (+.p16 (*.p16 beta alpha) (*.p16 i (+.p16 (+.p16 alpha beta) i))) (-.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (real->posit16 1.0)))))> #posit16 2) i))) (+.p16 (+.p16 alpha beta) i)) (+.p16 (*.p16 beta alpha) (*.p16 i (+.p16 (+.p16 alpha beta) i)))) (*.p16 (-.p16 (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i))) (real->posit16 1.0)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)))))> #posit16 2) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)))) (+.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (real->posit16 1.0))) (-.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (real->posit16 1.0))))> #posit16 2) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)))) (-.p16 (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (+.p16 alpha (+.p16 beta (*.p16 (real->posit16 2) i)))) (real->posit16 1.0))))>) 22.925 * * * [regime-changes]: Trying 3 branch expressions: (beta alpha i) 22.925 * * * * [regimes]: Trying to branch on beta from (#posit16 2) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i))) (+.p16 (*.p16 beta alpha) (*.p16 i (+.p16 (+.p16 alpha beta) i))))) (-.p16 (*.p16 (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i))) (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)))) (*.p16 (real->posit16 1.0) (real->posit16 1.0)))) (+.p16 (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i))) (real->posit16 1.0))))> #posit16 2) i))) (/.p16 (+.p16 (+.p16 alpha beta) i) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)))) (/.p16 (-.p16 (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i))) (real->posit16 1.0)) (+.p16 (*.p16 beta alpha) (*.p16 i (+.p16 (+.p16 alpha beta) i))))))> #posit16 2) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i))))) (*.p16 (*.p16 i (+.p16 (+.p16 alpha beta) i)) (/.p16 (*.p16 i (+.p16 (+.p16 alpha beta) i)) (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)))))) (-.p16 (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i))) (real->posit16 1.0))))> #posit16 2) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i))) (real->posit16 1.0)) (/.p16 (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i))) (+.p16 (*.p16 beta alpha) (*.p16 i (+.p16 (+.p16 alpha beta) i)))))))> #posit16 2) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)))) (+.p16 (+.p16 (*.p16 beta alpha) (*.p16 i (+.p16 alpha beta))) (*.p16 i i))) (-.p16 (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i))) (real->posit16 1.0))))> #posit16 2) i))) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i))) (-.p16 (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i))) (real->posit16 1.0))))> #posit16 2) i))) (/.p16 (-.p16 (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i))) (real->posit16 1.0)) (/.p16 (+.p16 (*.p16 beta alpha) (*.p16 i (+.p16 (+.p16 alpha beta) i))) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i))))))> #posit16 2) i))) (+.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (real->posit16 1.0))) (/.p16 (/.p16 (+.p16 (*.p16 beta alpha) (*.p16 i (+.p16 (+.p16 alpha beta) i))) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i))) (-.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (real->posit16 1.0)))))> #posit16 2) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)))) (-.p16 (*.p16 (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i))) (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)))) (*.p16 (real->posit16 1.0) (real->posit16 1.0)))) (+.p16 (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i))) (real->posit16 1.0))))> #posit16 2) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)))) (+.p16 (*.p16 beta alpha) (*.p16 i (+.p16 (+.p16 alpha beta) i)))) (-.p16 (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i))) (real->posit16 1.0))))> #posit16 2) i))) (/.p16 (+.p16 (+.p16 alpha beta) i) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)))) (+.p16 (*.p16 beta alpha) (*.p16 i (+.p16 (+.p16 alpha beta) i)))) (+.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (real->posit16 1.0))) (-.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (real->posit16 1.0))))> #posit16 2) i))) (*.p16 (/.p16 (+.p16 (+.p16 alpha beta) i) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i))) (+.p16 (*.p16 beta alpha) (*.p16 i (+.p16 (+.p16 alpha beta) i))))) (-.p16 (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i))) (real->posit16 1.0))))> #posit16 2) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i))) (real->posit16 1.0)) (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i))))))> #posit16 2) i))) (/.p16 (+.p16 (+.p16 alpha beta) i) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)))) (+.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (real->posit16 1.0))) (/.p16 (+.p16 (*.p16 beta alpha) (*.p16 i (+.p16 (+.p16 alpha beta) i))) (-.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (real->posit16 1.0)))))> #posit16 2) i))) (+.p16 (+.p16 alpha beta) i)) (+.p16 (*.p16 beta alpha) (*.p16 i (+.p16 (+.p16 alpha beta) i)))) (*.p16 (-.p16 (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i))) (real->posit16 1.0)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)))))> #posit16 2) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)))) (+.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (real->posit16 1.0))) (-.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (real->posit16 1.0))))> #posit16 2) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)))) (-.p16 (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (+.p16 alpha (+.p16 beta (*.p16 (real->posit16 2) i)))) (real->posit16 1.0))))>) 23.493 * * * * [regimes]: Trying to branch on alpha from (#posit16 2) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i))) (+.p16 (*.p16 beta alpha) (*.p16 i (+.p16 (+.p16 alpha beta) i))))) (-.p16 (*.p16 (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i))) (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)))) (*.p16 (real->posit16 1.0) (real->posit16 1.0)))) (+.p16 (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i))) (real->posit16 1.0))))> #posit16 2) i))) (/.p16 (+.p16 (+.p16 alpha beta) i) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)))) (/.p16 (-.p16 (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i))) (real->posit16 1.0)) (+.p16 (*.p16 beta alpha) (*.p16 i (+.p16 (+.p16 alpha beta) i))))))> #posit16 2) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i))))) (*.p16 (*.p16 i (+.p16 (+.p16 alpha beta) i)) (/.p16 (*.p16 i (+.p16 (+.p16 alpha beta) i)) (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)))))) (-.p16 (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i))) (real->posit16 1.0))))> #posit16 2) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i))) (real->posit16 1.0)) (/.p16 (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i))) (+.p16 (*.p16 beta alpha) (*.p16 i (+.p16 (+.p16 alpha beta) i)))))))> #posit16 2) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)))) (+.p16 (+.p16 (*.p16 beta alpha) (*.p16 i (+.p16 alpha beta))) (*.p16 i i))) (-.p16 (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i))) (real->posit16 1.0))))> #posit16 2) i))) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i))) (-.p16 (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i))) (real->posit16 1.0))))> #posit16 2) i))) (/.p16 (-.p16 (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i))) (real->posit16 1.0)) (/.p16 (+.p16 (*.p16 beta alpha) (*.p16 i (+.p16 (+.p16 alpha beta) i))) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i))))))> #posit16 2) i))) (+.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (real->posit16 1.0))) (/.p16 (/.p16 (+.p16 (*.p16 beta alpha) (*.p16 i (+.p16 (+.p16 alpha beta) i))) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i))) (-.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (real->posit16 1.0)))))> #posit16 2) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)))) (-.p16 (*.p16 (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i))) (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)))) (*.p16 (real->posit16 1.0) (real->posit16 1.0)))) (+.p16 (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i))) (real->posit16 1.0))))> #posit16 2) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)))) (+.p16 (*.p16 beta alpha) (*.p16 i (+.p16 (+.p16 alpha beta) i)))) (-.p16 (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i))) (real->posit16 1.0))))> #posit16 2) i))) (/.p16 (+.p16 (+.p16 alpha beta) i) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)))) (+.p16 (*.p16 beta alpha) (*.p16 i (+.p16 (+.p16 alpha beta) i)))) (+.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (real->posit16 1.0))) (-.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (real->posit16 1.0))))> #posit16 2) i))) (*.p16 (/.p16 (+.p16 (+.p16 alpha beta) i) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i))) (+.p16 (*.p16 beta alpha) (*.p16 i (+.p16 (+.p16 alpha beta) i))))) (-.p16 (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i))) (real->posit16 1.0))))> #posit16 2) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i))) (real->posit16 1.0)) (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i))))))> #posit16 2) i))) (/.p16 (+.p16 (+.p16 alpha beta) i) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)))) (+.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (real->posit16 1.0))) (/.p16 (+.p16 (*.p16 beta alpha) (*.p16 i (+.p16 (+.p16 alpha beta) i))) (-.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (real->posit16 1.0)))))> #posit16 2) i))) (+.p16 (+.p16 alpha beta) i)) (+.p16 (*.p16 beta alpha) (*.p16 i (+.p16 (+.p16 alpha beta) i)))) (*.p16 (-.p16 (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i))) (real->posit16 1.0)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)))))> #posit16 2) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)))) (+.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (real->posit16 1.0))) (-.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (real->posit16 1.0))))> #posit16 2) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)))) (-.p16 (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (+.p16 alpha (+.p16 beta (*.p16 (real->posit16 2) i)))) (real->posit16 1.0))))>) 24.143 * * * * [regimes]: Trying to branch on i from (#posit16 2) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i))) (+.p16 (*.p16 beta alpha) (*.p16 i (+.p16 (+.p16 alpha beta) i))))) (-.p16 (*.p16 (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i))) (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)))) (*.p16 (real->posit16 1.0) (real->posit16 1.0)))) (+.p16 (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i))) (real->posit16 1.0))))> #posit16 2) i))) (/.p16 (+.p16 (+.p16 alpha beta) i) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)))) (/.p16 (-.p16 (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i))) (real->posit16 1.0)) (+.p16 (*.p16 beta alpha) (*.p16 i (+.p16 (+.p16 alpha beta) i))))))> #posit16 2) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i))))) (*.p16 (*.p16 i (+.p16 (+.p16 alpha beta) i)) (/.p16 (*.p16 i (+.p16 (+.p16 alpha beta) i)) (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)))))) (-.p16 (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i))) (real->posit16 1.0))))> #posit16 2) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i))) (real->posit16 1.0)) (/.p16 (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i))) (+.p16 (*.p16 beta alpha) (*.p16 i (+.p16 (+.p16 alpha beta) i)))))))> #posit16 2) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)))) (+.p16 (+.p16 (*.p16 beta alpha) (*.p16 i (+.p16 alpha beta))) (*.p16 i i))) (-.p16 (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i))) (real->posit16 1.0))))> #posit16 2) i))) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i))) (-.p16 (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i))) (real->posit16 1.0))))> #posit16 2) i))) (/.p16 (-.p16 (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i))) (real->posit16 1.0)) (/.p16 (+.p16 (*.p16 beta alpha) (*.p16 i (+.p16 (+.p16 alpha beta) i))) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i))))))> #posit16 2) i))) (+.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (real->posit16 1.0))) (/.p16 (/.p16 (+.p16 (*.p16 beta alpha) (*.p16 i (+.p16 (+.p16 alpha beta) i))) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i))) (-.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (real->posit16 1.0)))))> #posit16 2) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)))) (-.p16 (*.p16 (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i))) (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)))) (*.p16 (real->posit16 1.0) (real->posit16 1.0)))) (+.p16 (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i))) (real->posit16 1.0))))> #posit16 2) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)))) (+.p16 (*.p16 beta alpha) (*.p16 i (+.p16 (+.p16 alpha beta) i)))) (-.p16 (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i))) (real->posit16 1.0))))> #posit16 2) i))) (/.p16 (+.p16 (+.p16 alpha beta) i) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)))) (+.p16 (*.p16 beta alpha) (*.p16 i (+.p16 (+.p16 alpha beta) i)))) (+.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (real->posit16 1.0))) (-.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (real->posit16 1.0))))> #posit16 2) i))) (*.p16 (/.p16 (+.p16 (+.p16 alpha beta) i) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i))) (+.p16 (*.p16 beta alpha) (*.p16 i (+.p16 (+.p16 alpha beta) i))))) (-.p16 (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i))) (real->posit16 1.0))))> #posit16 2) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i))) (real->posit16 1.0)) (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i))))))> #posit16 2) i))) (/.p16 (+.p16 (+.p16 alpha beta) i) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)))) (+.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (real->posit16 1.0))) (/.p16 (+.p16 (*.p16 beta alpha) (*.p16 i (+.p16 (+.p16 alpha beta) i))) (-.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (real->posit16 1.0)))))> #posit16 2) i))) (+.p16 (+.p16 alpha beta) i)) (+.p16 (*.p16 beta alpha) (*.p16 i (+.p16 (+.p16 alpha beta) i)))) (*.p16 (-.p16 (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i))) (real->posit16 1.0)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)))))> #posit16 2) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)))) (+.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (real->posit16 1.0))) (-.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (real->posit16 1.0))))> #posit16 2) i)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)))) (-.p16 (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (+.p16 alpha (+.p16 beta (*.p16 (real->posit16 2) i)))) (real->posit16 1.0))))>) 24.728 * * * [regime]: Found split indices: #