0.001 * [progress]: [Phase 1 of 3] Setting up. 0.001 * * * [progress]: [1/2] Preparing points 0.002 * * * * [points]: Sampling 256 additional inputs, on iter 0 have 0 / 256 0.003 * * * * [points]: Computing exacts on every 16 of 256 points to ramp up precision 0.006 * * * * [points]: Setting MPFR precision to 64 0.007 * * * * [points]: Setting MPFR precision to 320 0.008 * * * * [points]: Computing exacts on every 8 of 256 points to ramp up precision 0.012 * * * * [points]: Setting MPFR precision to 64 0.014 * * * * [points]: Setting MPFR precision to 320 0.016 * * * * [points]: Computing exacts on every 4 of 256 points to ramp up precision 0.019 * * * * [points]: Setting MPFR precision to 64 0.022 * * * * [points]: Setting MPFR precision to 320 0.026 * * * * [points]: Computing exacts on every 2 of 256 points to ramp up precision 0.030 * * * * [points]: Setting MPFR precision to 64 0.037 * * * * [points]: Setting MPFR precision to 320 0.048 * * * * [points]: Computing exacts for 256 points 0.054 * * * * [points]: Setting MPFR precision to 64 0.084 * * * * [points]: Setting MPFR precision to 320 0.139 * * * * [points]: Filtering points with unrepresentable outputs 0.139 * * * * [points]: Sampling 225 additional inputs, on iter 1 have 31 / 256 0.141 * * * * [points]: Computing exacts on every 14 of 225 points to ramp up precision 0.147 * * * * [points]: Setting MPFR precision to 64 0.149 * * * * [points]: Setting MPFR precision to 320 0.151 * * * * [points]: Computing exacts on every 7 of 225 points to ramp up precision 0.157 * * * * [points]: Setting MPFR precision to 64 0.161 * * * * [points]: Setting MPFR precision to 320 0.165 * * * * [points]: Computing exacts on every 3 of 225 points to ramp up precision 0.171 * * * * [points]: Setting MPFR precision to 64 0.178 * * * * [points]: Setting MPFR precision to 320 0.184 * * * * [points]: Computing exacts for 225 points 0.191 * * * * [points]: Setting MPFR precision to 64 0.218 * * * * [points]: Setting MPFR precision to 320 0.239 * * * * [points]: Filtering points with unrepresentable outputs 0.239 * * * * [points]: Sampling 192 additional inputs, on iter 2 have 64 / 256 0.240 * * * * [points]: Computing exacts on every 12 of 192 points to ramp up precision 0.243 * * * * [points]: Setting MPFR precision to 64 0.244 * * * * [points]: Setting MPFR precision to 320 0.245 * * * * [points]: Computing exacts on every 6 of 192 points to ramp up precision 0.249 * * * * [points]: Setting MPFR precision to 64 0.252 * * * * [points]: Setting MPFR precision to 320 0.255 * * * * [points]: Computing exacts on every 3 of 192 points to ramp up precision 0.261 * * * * [points]: Setting MPFR precision to 64 0.267 * * * * [points]: Setting MPFR precision to 320 0.271 * * * * [points]: Computing exacts for 192 points 0.295 * * * * [points]: Setting MPFR precision to 64 0.308 * * * * [points]: Setting MPFR precision to 320 0.321 * * * * [points]: Filtering points with unrepresentable outputs 0.321 * * * * [points]: Sampling 166 additional inputs, on iter 3 have 90 / 256 0.322 * * * * [points]: Computing exacts on every 10 of 166 points to ramp up precision 0.326 * * * * [points]: Setting MPFR precision to 64 0.327 * * * * [points]: Setting MPFR precision to 320 0.328 * * * * [points]: Computing exacts on every 5 of 166 points to ramp up precision 0.332 * * * * [points]: Setting MPFR precision to 64 0.334 * * * * [points]: Setting MPFR precision to 320 0.336 * * * * [points]: Computing exacts on every 2 of 166 points to ramp up precision 0.339 * * * * [points]: Setting MPFR precision to 64 0.343 * * * * [points]: Setting MPFR precision to 320 0.347 * * * * [points]: Computing exacts for 166 points 0.350 * * * * [points]: Setting MPFR precision to 64 0.361 * * * * [points]: Setting MPFR precision to 320 0.372 * * * * [points]: Filtering points with unrepresentable outputs 0.372 * * * * [points]: Sampling 148 additional inputs, on iter 4 have 108 / 256 0.373 * * * * [points]: Computing exacts on every 9 of 148 points to ramp up precision 0.377 * * * * [points]: Setting MPFR precision to 64 0.378 * * * * [points]: Setting MPFR precision to 320 0.379 * * * * [points]: Computing exacts on every 4 of 148 points to ramp up precision 0.384 * * * * [points]: Setting MPFR precision to 64 0.388 * * * * [points]: Setting MPFR precision to 320 0.420 * * * * [points]: Computing exacts on every 2 of 148 points to ramp up precision 0.424 * * * * [points]: Setting MPFR precision to 64 0.427 * * * * [points]: Setting MPFR precision to 320 0.431 * * * * [points]: Computing exacts for 148 points 0.435 * * * * [points]: Setting MPFR precision to 64 0.444 * * * * [points]: Setting MPFR precision to 320 0.454 * * * * [points]: Filtering points with unrepresentable outputs 0.454 * * * * [points]: Sampling 134 additional inputs, on iter 5 have 122 / 256 0.455 * * * * [points]: Computing exacts on every 8 of 134 points to ramp up precision 0.458 * * * * [points]: Setting MPFR precision to 64 0.460 * * * * [points]: Setting MPFR precision to 320 0.461 * * * * [points]: Computing exacts on every 4 of 134 points to ramp up precision 0.464 * * * * [points]: Setting MPFR precision to 64 0.466 * * * * [points]: Setting MPFR precision to 320 0.468 * * * * [points]: Computing exacts on every 2 of 134 points to ramp up precision 0.471 * * * * [points]: Setting MPFR precision to 64 0.474 * * * * [points]: Setting MPFR precision to 320 0.477 * * * * [points]: Computing exacts for 134 points 0.481 * * * * [points]: Setting MPFR precision to 64 0.490 * * * * [points]: Setting MPFR precision to 320 0.499 * * * * [points]: Filtering points with unrepresentable outputs 0.499 * * * * [points]: Sampling 120 additional inputs, on iter 6 have 136 / 256 0.499 * * * * [points]: Computing exacts on every 7 of 120 points to ramp up precision 0.503 * * * * [points]: Setting MPFR precision to 64 0.504 * * * * [points]: Setting MPFR precision to 320 0.505 * * * * [points]: Computing exacts on every 3 of 120 points to ramp up precision 0.527 * * * * [points]: Setting MPFR precision to 64 0.529 * * * * [points]: Setting MPFR precision to 320 0.531 * * * * [points]: Computing exacts for 120 points 0.535 * * * * [points]: Setting MPFR precision to 64 0.543 * * * * [points]: Setting MPFR precision to 320 0.551 * * * * [points]: Filtering points with unrepresentable outputs 0.551 * * * * [points]: Sampling 107 additional inputs, on iter 7 have 149 / 256 0.552 * * * * [points]: Computing exacts on every 6 of 107 points to ramp up precision 0.555 * * * * [points]: Setting MPFR precision to 64 0.556 * * * * [points]: Setting MPFR precision to 320 0.557 * * * * [points]: Computing exacts on every 3 of 107 points to ramp up precision 0.561 * * * * [points]: Setting MPFR precision to 64 0.562 * * * * [points]: Setting MPFR precision to 320 0.564 * * * * [points]: Computing exacts for 107 points 0.568 * * * * [points]: Setting MPFR precision to 64 0.576 * * * * [points]: Setting MPFR precision to 320 0.588 * * * * [points]: Filtering points with unrepresentable outputs 0.588 * * * * [points]: Sampling 92 additional inputs, on iter 8 have 164 / 256 0.589 * * * * [points]: Computing exacts on every 5 of 92 points to ramp up precision 0.595 * * * * [points]: Setting MPFR precision to 64 0.597 * * * * [points]: Setting MPFR precision to 320 0.598 * * * * [points]: Computing exacts on every 2 of 92 points to ramp up precision 0.604 * * * * [points]: Setting MPFR precision to 64 0.608 * * * * [points]: Setting MPFR precision to 320 0.611 * * * * [points]: Computing exacts for 92 points 0.617 * * * * [points]: Setting MPFR precision to 64 0.627 * * * * [points]: Setting MPFR precision to 320 0.638 * * * * [points]: Filtering points with unrepresentable outputs 0.638 * * * * [points]: Sampling 81 additional inputs, on iter 9 have 175 / 256 0.639 * * * * [points]: Computing exacts on every 5 of 81 points to ramp up precision 0.671 * * * * [points]: Setting MPFR precision to 64 0.673 * * * * [points]: Setting MPFR precision to 320 0.675 * * * * [points]: Computing exacts on every 2 of 81 points to ramp up precision 0.680 * * * * [points]: Setting MPFR precision to 64 0.683 * * * * [points]: Setting MPFR precision to 320 0.686 * * * * [points]: Computing exacts for 81 points 0.692 * * * * [points]: Setting MPFR precision to 64 0.698 * * * * [points]: Setting MPFR precision to 320 0.704 * * * * [points]: Filtering points with unrepresentable outputs 0.704 * * * * [points]: Sampling 71 additional inputs, on iter 10 have 185 / 256 0.704 * * * * [points]: Computing exacts on every 4 of 71 points to ramp up precision 0.708 * * * * [points]: Setting MPFR precision to 64 0.709 * * * * [points]: Setting MPFR precision to 320 0.710 * * * * [points]: Computing exacts on every 2 of 71 points to ramp up precision 0.713 * * * * [points]: Setting MPFR precision to 64 0.715 * * * * [points]: Setting MPFR precision to 320 0.717 * * * * [points]: Computing exacts for 71 points 0.720 * * * * [points]: Setting MPFR precision to 64 0.725 * * * * [points]: Setting MPFR precision to 320 0.730 * * * * [points]: Filtering points with unrepresentable outputs 0.730 * * * * [points]: Sampling 64 additional inputs, on iter 11 have 192 / 256 0.730 * * * * [points]: Computing exacts on every 4 of 64 points to ramp up precision 0.734 * * * * [points]: Setting MPFR precision to 64 0.735 * * * * [points]: Setting MPFR precision to 320 0.735 * * * * [points]: Computing exacts on every 2 of 64 points to ramp up precision 0.739 * * * * [points]: Setting MPFR precision to 64 0.740 * * * * [points]: Setting MPFR precision to 320 0.742 * * * * [points]: Computing exacts for 64 points 0.745 * * * * [points]: Setting MPFR precision to 64 0.750 * * * * [points]: Setting MPFR precision to 320 0.754 * * * * [points]: Filtering points with unrepresentable outputs 0.754 * * * * [points]: Sampling 52 additional inputs, on iter 12 have 204 / 256 0.754 * * * * [points]: Computing exacts on every 3 of 52 points to ramp up precision 0.758 * * * * [points]: Setting MPFR precision to 64 0.759 * * * * [points]: Setting MPFR precision to 320 0.760 * * * * [points]: Computing exacts for 52 points 0.780 * * * * [points]: Setting MPFR precision to 64 0.783 * * * * [points]: Setting MPFR precision to 320 0.787 * * * * [points]: Filtering points with unrepresentable outputs 0.787 * * * * [points]: Sampling 46 additional inputs, on iter 13 have 210 / 256 0.787 * * * * [points]: Computing exacts on every 2 of 46 points to ramp up precision 0.792 * * * * [points]: Setting MPFR precision to 64 0.793 * * * * [points]: Setting MPFR precision to 320 0.794 * * * * [points]: Computing exacts for 46 points 0.798 * * * * [points]: Setting MPFR precision to 64 0.801 * * * * [points]: Setting MPFR precision to 320 0.804 * * * * [points]: Filtering points with unrepresentable outputs 0.804 * * * * [points]: Sampling 39 additional inputs, on iter 14 have 217 / 256 0.804 * * * * [points]: Computing exacts on every 2 of 39 points to ramp up precision 0.808 * * * * [points]: Setting MPFR precision to 64 0.809 * * * * [points]: Setting MPFR precision to 320 0.810 * * * * [points]: Computing exacts for 39 points 0.813 * * * * [points]: Setting MPFR precision to 64 0.816 * * * * [points]: Setting MPFR precision to 320 0.819 * * * * [points]: Filtering points with unrepresentable outputs 0.819 * * * * [points]: Sampling 31 additional inputs, on iter 15 have 225 / 256 0.819 * * * * [points]: Computing exacts for 31 points 0.823 * * * * [points]: Setting MPFR precision to 64 0.825 * * * * [points]: Setting MPFR precision to 320 0.827 * * * * [points]: Filtering points with unrepresentable outputs 0.828 * * * * [points]: Sampling 29 additional inputs, on iter 16 have 227 / 256 0.828 * * * * [points]: Computing exacts for 29 points 0.831 * * * * [points]: Setting MPFR precision to 64 0.833 * * * * [points]: Setting MPFR precision to 320 0.835 * * * * [points]: Filtering points with unrepresentable outputs 0.835 * * * * [points]: Sampling 23 additional inputs, on iter 17 have 233 / 256 0.836 * * * * [points]: Computing exacts for 23 points 0.839 * * * * [points]: Setting MPFR precision to 64 0.841 * * * * [points]: Setting MPFR precision to 320 0.842 * * * * [points]: Filtering points with unrepresentable outputs 0.842 * * * * [points]: Sampling 21 additional inputs, on iter 18 have 235 / 256 0.843 * * * * [points]: Computing exacts for 21 points 0.846 * * * * [points]: Setting MPFR precision to 64 0.848 * * * * [points]: Setting MPFR precision to 320 0.849 * * * * [points]: Filtering points with unrepresentable outputs 0.849 * * * * [points]: Sampling 19 additional inputs, on iter 19 have 237 / 256 0.849 * * * * [points]: Computing exacts for 19 points 0.853 * * * * [points]: Setting MPFR precision to 64 0.854 * * * * [points]: Setting MPFR precision to 320 0.855 * * * * [points]: Filtering points with unrepresentable outputs 0.855 * * * * [points]: Sampling 16 additional inputs, on iter 20 have 240 / 256 0.855 * * * * [points]: Computing exacts for 16 points 0.862 * * * * [points]: Setting MPFR precision to 64 0.888 * * * * [points]: Setting MPFR precision to 320 0.891 * * * * [points]: Filtering points with unrepresentable outputs 0.891 * * * * [points]: Sampling 15 additional inputs, on iter 21 have 241 / 256 0.891 * * * * [points]: Computing exacts for 15 points 0.898 * * * * [points]: Setting MPFR precision to 64 0.900 * * * * [points]: Setting MPFR precision to 320 0.902 * * * * [points]: Filtering points with unrepresentable outputs 0.902 * * * * [points]: Sampling 13 additional inputs, on iter 22 have 243 / 256 0.902 * * * * [points]: Computing exacts for 13 points 0.908 * * * * [points]: Setting MPFR precision to 64 0.909 * * * * [points]: Setting MPFR precision to 320 0.911 * * * * [points]: Filtering points with unrepresentable outputs 0.911 * * * * [points]: Sampling 10 additional inputs, on iter 23 have 246 / 256 0.911 * * * * [points]: Computing exacts for 10 points 0.917 * * * * [points]: Setting MPFR precision to 64 0.918 * * * * [points]: Setting MPFR precision to 320 0.919 * * * * [points]: Filtering points with unrepresentable outputs 0.919 * * * * [points]: Sampling 8 additional inputs, on iter 24 have 248 / 256 0.920 * * * * [points]: Computing exacts for 8 points 0.925 * * * * [points]: Setting MPFR precision to 64 0.926 * * * * [points]: Setting MPFR precision to 320 0.927 * * * * [points]: Filtering points with unrepresentable outputs 0.927 * * * * [points]: Sampling 8 additional inputs, on iter 25 have 248 / 256 0.928 * * * * [points]: Computing exacts for 8 points 0.933 * * * * [points]: Setting MPFR precision to 64 0.934 * * * * [points]: Setting MPFR precision to 320 0.935 * * * * [points]: Filtering points with unrepresentable outputs 0.935 * * * * [points]: Sampling 7 additional inputs, on iter 26 have 249 / 256 0.935 * * * * [points]: Computing exacts for 7 points 0.941 * * * * [points]: Setting MPFR precision to 64 0.942 * * * * [points]: Setting MPFR precision to 320 0.943 * * * * [points]: Filtering points with unrepresentable outputs 0.943 * * * * [points]: Sampling 5 additional inputs, on iter 27 have 251 / 256 0.943 * * * * [points]: Computing exacts for 5 points 0.949 * * * * [points]: Setting MPFR precision to 64 0.950 * * * * [points]: Setting MPFR precision to 320 0.951 * * * * [points]: Filtering points with unrepresentable outputs 0.951 * * * * [points]: Sampling 5 additional inputs, on iter 28 have 251 / 256 0.951 * * * * [points]: Computing exacts for 5 points 0.956 * * * * [points]: Setting MPFR precision to 64 0.957 * * * * [points]: Setting MPFR precision to 320 0.958 * * * * [points]: Filtering points with unrepresentable outputs 0.958 * * * * [points]: Sampling 4 additional inputs, on iter 29 have 252 / 256 0.958 * * * * [points]: Computing exacts for 4 points 0.964 * * * * [points]: Setting MPFR precision to 64 0.964 * * * * [points]: Setting MPFR precision to 320 0.965 * * * * [points]: Filtering points with unrepresentable outputs 0.965 * * * * [points]: Sampling 4 additional inputs, on iter 30 have 252 / 256 0.965 * * * * [points]: Computing exacts for 4 points 0.971 * * * * [points]: Setting MPFR precision to 64 0.972 * * * * [points]: Setting MPFR precision to 320 0.972 * * * * [points]: Filtering points with unrepresentable outputs 0.972 * * * * [points]: Sampling 4 additional inputs, on iter 31 have 252 / 256 0.972 * * * * [points]: Computing exacts for 4 points 0.978 * * * * [points]: Setting MPFR precision to 64 0.979 * * * * [points]: Setting MPFR precision to 320 0.979 * * * * [points]: Filtering points with unrepresentable outputs 0.979 * * * * [points]: Sampling 4 additional inputs, on iter 32 have 252 / 256 0.979 * * * * [points]: Computing exacts for 4 points 0.985 * * * * [points]: Setting MPFR precision to 64 0.986 * * * * [points]: Setting MPFR precision to 320 0.986 * * * * [points]: Filtering points with unrepresentable outputs 0.986 * * * * [points]: Sampling 4 additional inputs, on iter 33 have 253 / 256 0.986 * * * * [points]: Computing exacts for 4 points 0.993 * * * * [points]: Setting MPFR precision to 64 0.994 * * * * [points]: Setting MPFR precision to 320 0.994 * * * * [points]: Filtering points with unrepresentable outputs 0.995 * * * * [points]: Sampling 4 additional inputs, on iter 34 have 253 / 256 0.995 * * * * [points]: Computing exacts for 4 points 1.002 * * * * [points]: Setting MPFR precision to 64 1.003 * * * * [points]: Setting MPFR precision to 320 1.003 * * * * [points]: Filtering points with unrepresentable outputs 1.003 * * * * [points]: Sampling 4 additional inputs, on iter 35 have 253 / 256 1.004 * * * * [points]: Computing exacts for 4 points 1.024 * * * * [points]: Setting MPFR precision to 64 1.025 * * * * [points]: Setting MPFR precision to 320 1.025 * * * * [points]: Filtering points with unrepresentable outputs 1.026 * * * * [points]: Sampling 4 additional inputs, on iter 36 have 254 / 256 1.026 * * * * [points]: Computing exacts for 4 points 1.031 * * * * [points]: Setting MPFR precision to 64 1.032 * * * * [points]: Setting MPFR precision to 320 1.033 * * * * [points]: Filtering points with unrepresentable outputs 1.033 * * * * [points]: Sampling 4 additional inputs, on iter 37 have 254 / 256 1.033 * * * * [points]: Computing exacts for 4 points 1.039 * * * * [points]: Setting MPFR precision to 64 1.039 * * * * [points]: Setting MPFR precision to 320 1.040 * * * * [points]: Filtering points with unrepresentable outputs 1.040 * * * * [points]: Sampling 4 additional inputs, on iter 38 have 255 / 256 1.040 * * * * [points]: Computing exacts for 4 points 1.046 * * * * [points]: Setting MPFR precision to 64 1.046 * * * * [points]: Setting MPFR precision to 320 1.047 * * * * [points]: Filtering points with unrepresentable outputs 1.047 * * * * [points]: Sampling 4 additional inputs, on iter 39 have 255 / 256 1.047 * * * * [points]: Computing exacts for 4 points 1.053 * * * * [points]: Setting MPFR precision to 64 1.054 * * * * [points]: Setting MPFR precision to 320 1.054 * * * * [points]: Filtering points with unrepresentable outputs 1.054 * * * * [points]: Sampling 4 additional inputs, on iter 40 have 255 / 256 1.054 * * * * [points]: Computing exacts for 4 points 1.060 * * * * [points]: Setting MPFR precision to 64 1.061 * * * * [points]: Setting MPFR precision to 320 1.061 * * * * [points]: Filtering points with unrepresentable outputs 1.061 * * * * [points]: Sampling 4 additional inputs, on iter 41 have 255 / 256 1.062 * * * * [points]: Computing exacts for 4 points 1.067 * * * * [points]: Setting MPFR precision to 64 1.068 * * * * [points]: Setting MPFR precision to 320 1.069 * * * * [points]: Filtering points with unrepresentable outputs 1.069 * * * * [points]: Sampling 4 additional inputs, on iter 42 have 255 / 256 1.069 * * * * [points]: Computing exacts for 4 points 1.075 * * * * [points]: Setting MPFR precision to 64 1.075 * * * * [points]: Setting MPFR precision to 320 1.076 * * * * [points]: Filtering points with unrepresentable outputs 1.076 * * * * [points]: Sampling 4 additional inputs, on iter 43 have 255 / 256 1.076 * * * * [points]: Computing exacts for 4 points 1.082 * * * * [points]: Setting MPFR precision to 64 1.082 * * * * [points]: Setting MPFR precision to 320 1.083 * * * * [points]: Filtering points with unrepresentable outputs 1.083 * * * * [points]: Sampled 256 points with exact outputs 1.083 * * * [progress]: [2/2] Setting up program. 1.100 * [progress]: [Phase 2 of 3] Improving. 1.101 * * * * [progress]: [ 1 / 1 ] simplifiying candidate #posit16 2)) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) a)) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) b)) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) c))))> 1.101 * [simplify]: Simplifying (sqrt.p16 (*.p16 (*.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) a)) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) b)) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) c))) 1.101 * * [simplify]: iters left: 6 (15 enodes) 1.107 * * [simplify]: iters left: 5 (54 enodes) 1.124 * * [simplify]: iters left: 4 (174 enodes) 1.247 * * [simplify]: Extracting #0: cost 1 inf + 0 1.247 * * [simplify]: Extracting #1: cost 2 inf + 0 1.248 * * [simplify]: Extracting #2: cost 52 inf + 0 1.252 * * [simplify]: Extracting #3: cost 218 inf + 0 1.254 * * [simplify]: Extracting #4: cost 350 inf + 488 1.258 * * [simplify]: Extracting #5: cost 271 inf + 83278 1.272 * * [simplify]: Extracting #6: cost 99 inf + 301152 1.315 * * [simplify]: Extracting #7: cost 13 inf + 445414 1.367 * * [simplify]: Extracting #8: cost 0 inf + 471346 1.420 * [simplify]: Simplified to (sqrt.p16 (*.p16 (*.p16 (-.p16 (/.p16 (+.p16 (+.p16 b a) c) (real->posit16 2)) b) (*.p16 (-.p16 (/.p16 (+.p16 (+.p16 b a) c) (real->posit16 2)) a) (/.p16 (+.p16 (+.p16 b a) c) (real->posit16 2)))) (-.p16 (/.p16 (+.p16 (+.p16 b a) c) (real->posit16 2)) c))) 1.420 * [simplify]: Simplified (2) to (λ (a b c) (sqrt.p16 (*.p16 (*.p16 (-.p16 (/.p16 (+.p16 (+.p16 b a) c) (real->posit16 2)) b) (*.p16 (-.p16 (/.p16 (+.p16 (+.p16 b a) c) (real->posit16 2)) a) (/.p16 (+.p16 (+.p16 b a) c) (real->posit16 2)))) (-.p16 (/.p16 (+.p16 (+.p16 b a) c) (real->posit16 2)) c)))) 1.438 * * [progress]: iteration 1 / 4 1.438 * * * [progress]: picking best candidate 1.448 * * * * [pick]: Picked #posit16 2)) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) a)) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) b)) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) c))))> 1.449 * * * [progress]: localizing error 1.786 * * * [progress]: generating rewritten candidates 1.786 * * * * [progress]: [ 1 / 4 ] rewriting at (2 1 2) 1.840 * * * * [progress]: [ 2 / 4 ] rewriting at (2 1 1 1 2) 1.885 * * * * [progress]: [ 3 / 4 ] rewriting at (2 1 1 2) 1.931 * * * * [progress]: [ 4 / 4 ] rewriting at (2 1 2 1) 1.954 * * * [progress]: generating series expansions 1.954 * * * * [progress]: [ 1 / 4 ] generating series at (2 1 2) 1.954 * * * * [progress]: [ 2 / 4 ] generating series at (2 1 1 1 2) 1.954 * * * * [progress]: [ 3 / 4 ] generating series at (2 1 1 2) 1.954 * * * * [progress]: [ 4 / 4 ] generating series at (2 1 2 1) 1.954 * * * [progress]: simplifying candidates 1.954 * * * * [progress]: [ 1 / 10 ] simplifiying candidate #posit16 2)) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) a)) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) b)) (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (neg.p16 c)))))> 1.954 * * * * [progress]: [ 2 / 10 ] simplifiying candidate #posit16 2)) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) a)) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) b)) (/.p16 (-.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2))) (*.p16 c c)) (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) c)))))> 1.954 * * * * [progress]: [ 3 / 10 ] simplifiying candidate #posit16 2)) (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (neg.p16 a))) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) b)) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) c))))> 1.954 * * * * [progress]: [ 4 / 10 ] simplifiying candidate #posit16 2)) (/.p16 (-.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2))) (*.p16 a a)) (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) a))) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) b)) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) c))))> 1.954 * * * * [progress]: [ 5 / 10 ] simplifiying candidate #posit16 2)) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) a)) (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (neg.p16 b))) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) c))))> 1.954 * * * * [progress]: [ 6 / 10 ] simplifiying candidate #posit16 2)) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) a)) (/.p16 (-.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2))) (*.p16 b b)) (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) b))) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) c))))> 1.954 * * * * [progress]: [ 7 / 10 ] simplifiying candidate #posit16 2)) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) a)) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) b)) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) c))))> 1.955 * [simplify]: Simplifying (sqrt.p16 (*.p16 (*.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) a)) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) b)) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) c))) 1.955 * * [simplify]: iters left: 6 (15 enodes) 1.961 * * [simplify]: iters left: 5 (54 enodes) 1.971 * * [simplify]: iters left: 4 (174 enodes) 2.089 * * [simplify]: Extracting #0: cost 1 inf + 0 2.089 * * [simplify]: Extracting #1: cost 2 inf + 0 2.089 * * [simplify]: Extracting #2: cost 52 inf + 0 2.090 * * [simplify]: Extracting #3: cost 218 inf + 0 2.092 * * [simplify]: Extracting #4: cost 350 inf + 488 2.099 * * [simplify]: Extracting #5: cost 271 inf + 83278 2.123 * * [simplify]: Extracting #6: cost 99 inf + 301152 2.165 * * [simplify]: Extracting #7: cost 13 inf + 445414 2.212 * * [simplify]: Extracting #8: cost 0 inf + 471346 2.239 * [simplify]: Simplified to (sqrt.p16 (*.p16 (*.p16 (-.p16 (/.p16 (+.p16 (+.p16 b a) c) (real->posit16 2)) b) (*.p16 (-.p16 (/.p16 (+.p16 (+.p16 b a) c) (real->posit16 2)) a) (/.p16 (+.p16 (+.p16 b a) c) (real->posit16 2)))) (-.p16 (/.p16 (+.p16 (+.p16 b a) c) (real->posit16 2)) c))) 2.239 * [simplify]: Simplified (2) to (λ (a b c) (sqrt.p16 (*.p16 (*.p16 (-.p16 (/.p16 (+.p16 (+.p16 b a) c) (real->posit16 2)) b) (*.p16 (-.p16 (/.p16 (+.p16 (+.p16 b a) c) (real->posit16 2)) a) (/.p16 (+.p16 (+.p16 b a) c) (real->posit16 2)))) (-.p16 (/.p16 (+.p16 (+.p16 b a) c) (real->posit16 2)) c)))) 2.239 * * * * [progress]: [ 8 / 10 ] simplifiying candidate #posit16 2)) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) a)) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) b)) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) c))))> 2.239 * [simplify]: Simplifying (sqrt.p16 (*.p16 (*.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) a)) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) b)) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) c))) 2.239 * * [simplify]: iters left: 6 (15 enodes) 2.243 * * [simplify]: iters left: 5 (54 enodes) 2.253 * * [simplify]: iters left: 4 (174 enodes) 2.323 * * [simplify]: Extracting #0: cost 1 inf + 0 2.323 * * [simplify]: Extracting #1: cost 2 inf + 0 2.323 * * [simplify]: Extracting #2: cost 52 inf + 0 2.324 * * [simplify]: Extracting #3: cost 218 inf + 0 2.325 * * [simplify]: Extracting #4: cost 350 inf + 488 2.329 * * [simplify]: Extracting #5: cost 271 inf + 83278 2.344 * * [simplify]: Extracting #6: cost 99 inf + 301152 2.375 * * [simplify]: Extracting #7: cost 13 inf + 445414 2.402 * * [simplify]: Extracting #8: cost 0 inf + 471346 2.431 * [simplify]: Simplified to (sqrt.p16 (*.p16 (*.p16 (-.p16 (/.p16 (+.p16 (+.p16 b a) c) (real->posit16 2)) b) (*.p16 (-.p16 (/.p16 (+.p16 (+.p16 b a) c) (real->posit16 2)) a) (/.p16 (+.p16 (+.p16 b a) c) (real->posit16 2)))) (-.p16 (/.p16 (+.p16 (+.p16 b a) c) (real->posit16 2)) c))) 2.431 * [simplify]: Simplified (2) to (λ (a b c) (sqrt.p16 (*.p16 (*.p16 (-.p16 (/.p16 (+.p16 (+.p16 b a) c) (real->posit16 2)) b) (*.p16 (-.p16 (/.p16 (+.p16 (+.p16 b a) c) (real->posit16 2)) a) (/.p16 (+.p16 (+.p16 b a) c) (real->posit16 2)))) (-.p16 (/.p16 (+.p16 (+.p16 b a) c) (real->posit16 2)) c)))) 2.431 * * * * [progress]: [ 9 / 10 ] simplifiying candidate #posit16 2)) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) a)) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) b)) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) c))))> 2.432 * [simplify]: Simplifying (sqrt.p16 (*.p16 (*.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) a)) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) b)) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) c))) 2.432 * * [simplify]: iters left: 6 (15 enodes) 2.435 * * [simplify]: iters left: 5 (54 enodes) 2.445 * * [simplify]: iters left: 4 (174 enodes) 2.515 * * [simplify]: Extracting #0: cost 1 inf + 0 2.515 * * [simplify]: Extracting #1: cost 2 inf + 0 2.515 * * [simplify]: Extracting #2: cost 52 inf + 0 2.515 * * [simplify]: Extracting #3: cost 218 inf + 0 2.516 * * [simplify]: Extracting #4: cost 350 inf + 488 2.520 * * [simplify]: Extracting #5: cost 271 inf + 83278 2.534 * * [simplify]: Extracting #6: cost 99 inf + 301152 2.559 * * [simplify]: Extracting #7: cost 13 inf + 445414 2.588 * * [simplify]: Extracting #8: cost 0 inf + 471346 2.616 * [simplify]: Simplified to (sqrt.p16 (*.p16 (*.p16 (-.p16 (/.p16 (+.p16 (+.p16 b a) c) (real->posit16 2)) b) (*.p16 (-.p16 (/.p16 (+.p16 (+.p16 b a) c) (real->posit16 2)) a) (/.p16 (+.p16 (+.p16 b a) c) (real->posit16 2)))) (-.p16 (/.p16 (+.p16 (+.p16 b a) c) (real->posit16 2)) c))) 2.616 * [simplify]: Simplified (2) to (λ (a b c) (sqrt.p16 (*.p16 (*.p16 (-.p16 (/.p16 (+.p16 (+.p16 b a) c) (real->posit16 2)) b) (*.p16 (-.p16 (/.p16 (+.p16 (+.p16 b a) c) (real->posit16 2)) a) (/.p16 (+.p16 (+.p16 b a) c) (real->posit16 2)))) (-.p16 (/.p16 (+.p16 (+.p16 b a) c) (real->posit16 2)) c)))) 2.616 * * * * [progress]: [ 10 / 10 ] simplifiying candidate #posit16 2)) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) a)) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) b)) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) c))))> 2.616 * [simplify]: Simplifying (sqrt.p16 (*.p16 (*.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) a)) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) b)) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) c))) 2.617 * * [simplify]: iters left: 6 (15 enodes) 2.621 * * [simplify]: iters left: 5 (54 enodes) 2.631 * * [simplify]: iters left: 4 (174 enodes) 2.699 * * [simplify]: Extracting #0: cost 1 inf + 0 2.699 * * [simplify]: Extracting #1: cost 2 inf + 0 2.700 * * [simplify]: Extracting #2: cost 52 inf + 0 2.700 * * [simplify]: Extracting #3: cost 218 inf + 0 2.701 * * [simplify]: Extracting #4: cost 350 inf + 488 2.705 * * [simplify]: Extracting #5: cost 271 inf + 83278 2.724 * * [simplify]: Extracting #6: cost 99 inf + 301152 2.749 * * [simplify]: Extracting #7: cost 13 inf + 445414 2.788 * * [simplify]: Extracting #8: cost 0 inf + 471346 2.826 * [simplify]: Simplified to (sqrt.p16 (*.p16 (*.p16 (-.p16 (/.p16 (+.p16 (+.p16 b a) c) (real->posit16 2)) b) (*.p16 (-.p16 (/.p16 (+.p16 (+.p16 b a) c) (real->posit16 2)) a) (/.p16 (+.p16 (+.p16 b a) c) (real->posit16 2)))) (-.p16 (/.p16 (+.p16 (+.p16 b a) c) (real->posit16 2)) c))) 2.827 * [simplify]: Simplified (2) to (λ (a b c) (sqrt.p16 (*.p16 (*.p16 (-.p16 (/.p16 (+.p16 (+.p16 b a) c) (real->posit16 2)) b) (*.p16 (-.p16 (/.p16 (+.p16 (+.p16 b a) c) (real->posit16 2)) a) (/.p16 (+.p16 (+.p16 b a) c) (real->posit16 2)))) (-.p16 (/.p16 (+.p16 (+.p16 b a) c) (real->posit16 2)) c)))) 2.827 * * * [progress]: adding candidates to table 3.092 * * [progress]: iteration 2 / 4 3.092 * * * [progress]: picking best candidate 3.120 * * * * [pick]: Picked #posit16 2)) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) a)) (/.p16 (-.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2))) (*.p16 b b)) (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) b))) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) c))))> 3.120 * * * [progress]: localizing error 3.468 * * * [progress]: generating rewritten candidates 3.468 * * * * [progress]: [ 1 / 4 ] rewriting at (2 1 1 2) 3.529 * * * * [progress]: [ 2 / 4 ] rewriting at (2 1 2) 3.551 * * * * [progress]: [ 3 / 4 ] rewriting at (2 1 1 1 2) 3.573 * * * * [progress]: [ 4 / 4 ] rewriting at (2 1 1 2 1) 3.577 * * * [progress]: generating series expansions 3.577 * * * * [progress]: [ 1 / 4 ] generating series at (2 1 1 2) 3.577 * * * * [progress]: [ 2 / 4 ] generating series at (2 1 2) 3.577 * * * * [progress]: [ 3 / 4 ] generating series at (2 1 1 1 2) 3.577 * * * * [progress]: [ 4 / 4 ] generating series at (2 1 1 2 1) 3.577 * * * [progress]: simplifying candidates 3.577 * * * * [progress]: [ 1 / 13 ] simplifiying candidate #posit16 2)) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) a)) (/.p16 (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) b) (/.p16 (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) b) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) b)))) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) c))))> 3.577 * [simplify]: Simplifying (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) b) 3.577 * * [simplify]: iters left: 4 (9 enodes) 3.579 * * [simplify]: iters left: 3 (21 enodes) 3.583 * * [simplify]: iters left: 2 (27 enodes) 3.587 * * [simplify]: iters left: 1 (28 enodes) 3.591 * * [simplify]: Extracting #0: cost 1 inf + 0 3.591 * * [simplify]: Extracting #1: cost 3 inf + 0 3.591 * * [simplify]: Extracting #2: cost 4 inf + 1 3.591 * * [simplify]: Extracting #3: cost 10 inf + 1 3.591 * * [simplify]: Extracting #4: cost 5 inf + 47 3.591 * * [simplify]: Extracting #5: cost 1 inf + 738 3.591 * * [simplify]: Extracting #6: cost 0 inf + 1302 3.591 * [simplify]: Simplified to (+.p16 (/.p16 (+.p16 a (+.p16 c b)) (real->posit16 2)) b) 3.591 * [simplify]: Simplified (2 1 1 2 1) to (λ (a b c) (sqrt.p16 (*.p16 (*.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) a)) (/.p16 (+.p16 (/.p16 (+.p16 a (+.p16 c b)) (real->posit16 2)) b) (/.p16 (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) b) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) b)))) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) c)))) 3.592 * * * * [progress]: [ 2 / 13 ] simplifiying candidate #posit16 2)) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) a)) (/.p16 (-.p16 (*.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2))) (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)))) (*.p16 (*.p16 b b) (*.p16 b b))) (*.p16 (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) b) (+.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2))) (*.p16 b b))))) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) c))))> 3.592 * [simplify]: Simplifying (-.p16 (*.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2))) (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)))) (*.p16 (*.p16 b b) (*.p16 b b))) 3.592 * * [simplify]: iters left: 6 (13 enodes) 3.595 * * [simplify]: iters left: 5 (46 enodes) 3.604 * * [simplify]: iters left: 4 (130 enodes) 3.640 * * [simplify]: Extracting #0: cost 1 inf + 0 3.640 * * [simplify]: Extracting #1: cost 25 inf + 0 3.640 * * [simplify]: Extracting #2: cost 62 inf + 0 3.640 * * [simplify]: Extracting #3: cost 156 inf + 1 3.641 * * [simplify]: Extracting #4: cost 157 inf + 19646 3.647 * * [simplify]: Extracting #5: cost 52 inf + 148242 3.659 * * [simplify]: Extracting #6: cost 1 inf + 239837 3.671 * * [simplify]: Extracting #7: cost 0 inf + 242361 3.684 * [simplify]: Simplified to (*.p16 (-.p16 (*.p16 (/.p16 (+.p16 (+.p16 b a) c) (real->posit16 2)) (/.p16 (+.p16 (+.p16 b a) c) (real->posit16 2))) (*.p16 b b)) (+.p16 (*.p16 b b) (*.p16 (/.p16 (+.p16 (+.p16 b a) c) (real->posit16 2)) (/.p16 (+.p16 (+.p16 b a) c) (real->posit16 2))))) 3.684 * [simplify]: Simplified (2 1 1 2 1) to (λ (a b c) (sqrt.p16 (*.p16 (*.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) a)) (/.p16 (*.p16 (-.p16 (*.p16 (/.p16 (+.p16 (+.p16 b a) c) (real->posit16 2)) (/.p16 (+.p16 (+.p16 b a) c) (real->posit16 2))) (*.p16 b b)) (+.p16 (*.p16 b b) (*.p16 (/.p16 (+.p16 (+.p16 b a) c) (real->posit16 2)) (/.p16 (+.p16 (+.p16 b a) c) (real->posit16 2))))) (*.p16 (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) b) (+.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2))) (*.p16 b b))))) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) c)))) 3.685 * * * * [progress]: [ 3 / 13 ] simplifiying candidate #posit16 2)) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) a)) (/.p16 (-.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2))) (*.p16 b b)) (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) b))) (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (neg.p16 c)))))> 3.685 * * * * [progress]: [ 4 / 13 ] simplifiying candidate #posit16 2)) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) a)) (/.p16 (-.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2))) (*.p16 b b)) (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) b))) (/.p16 (-.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2))) (*.p16 c c)) (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) c)))))> 3.685 * * * * [progress]: [ 5 / 13 ] simplifiying candidate #posit16 2)) (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (neg.p16 a))) (/.p16 (-.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2))) (*.p16 b b)) (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) b))) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) c))))> 3.685 * * * * [progress]: [ 6 / 13 ] simplifiying candidate #posit16 2)) (/.p16 (-.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2))) (*.p16 a a)) (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) a))) (/.p16 (-.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2))) (*.p16 b b)) (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) b))) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) c))))> 3.685 * * * * [progress]: [ 7 / 13 ] simplifiying candidate #posit16 2)) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) a)) (/.p16 (*.p16 (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) b) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) b)) (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) b))) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) c))))> 3.685 * [simplify]: Simplifying (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) b) 3.685 * * [simplify]: iters left: 4 (9 enodes) 3.687 * * [simplify]: iters left: 3 (21 enodes) 3.690 * * [simplify]: iters left: 2 (27 enodes) 3.694 * * [simplify]: iters left: 1 (28 enodes) 3.697 * * [simplify]: Extracting #0: cost 1 inf + 0 3.697 * * [simplify]: Extracting #1: cost 3 inf + 0 3.697 * * [simplify]: Extracting #2: cost 4 inf + 1 3.697 * * [simplify]: Extracting #3: cost 10 inf + 1 3.698 * * [simplify]: Extracting #4: cost 5 inf + 47 3.698 * * [simplify]: Extracting #5: cost 1 inf + 738 3.698 * * [simplify]: Extracting #6: cost 0 inf + 1302 3.698 * [simplify]: Simplified to (+.p16 (/.p16 (+.p16 a (+.p16 c b)) (real->posit16 2)) b) 3.698 * [simplify]: Simplified (2 1 1 2 1 1) to (λ (a b c) (sqrt.p16 (*.p16 (*.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) a)) (/.p16 (*.p16 (+.p16 (/.p16 (+.p16 a (+.p16 c b)) (real->posit16 2)) b) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) b)) (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) b))) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) c)))) 3.698 * [simplify]: Simplifying (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) b) 3.698 * * [simplify]: iters left: 4 (9 enodes) 3.700 * * [simplify]: iters left: 3 (27 enodes) 3.704 * * [simplify]: iters left: 2 (47 enodes) 3.714 * * [simplify]: iters left: 1 (123 enodes) 3.743 * * [simplify]: Extracting #0: cost 1 inf + 0 3.743 * * [simplify]: Extracting #1: cost 15 inf + 0 3.744 * * [simplify]: Extracting #2: cost 52 inf + 82 3.744 * * [simplify]: Extracting #3: cost 87 inf + 1044 3.744 * * [simplify]: Extracting #4: cost 140 inf + 5615 3.745 * * [simplify]: Extracting #5: cost 118 inf + 19352 3.748 * * [simplify]: Extracting #6: cost 58 inf + 77580 3.756 * * [simplify]: Extracting #7: cost 8 inf + 157140 3.765 * * [simplify]: Extracting #8: cost 0 inf + 176132 3.774 * [simplify]: Simplified to (-.p16 (/.p16 (+.p16 b (+.p16 a c)) (real->posit16 2)) b) 3.774 * [simplify]: Simplified (2 1 1 2 1 2) to (λ (a b c) (sqrt.p16 (*.p16 (*.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) a)) (/.p16 (*.p16 (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) b) (-.p16 (/.p16 (+.p16 b (+.p16 a c)) (real->posit16 2)) b)) (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) b))) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) c)))) 3.775 * * * * [progress]: [ 8 / 13 ] simplifiying candidate #posit16 2)) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) a)) (/.p16 (+.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2))) (neg.p16 (*.p16 b b))) (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) b))) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) c))))> 3.775 * * * * [progress]: [ 9 / 13 ] simplifiying candidate #posit16 2)) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) a)) (/.p16 (/.p16 (-.p16 (*.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2))) (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)))) (*.p16 (*.p16 b b) (*.p16 b b))) (+.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2))) (*.p16 b b))) (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) b))) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) c))))> 3.775 * * * * [progress]: [ 10 / 13 ] simplifiying candidate #posit16 2)) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) a)) (/.p16 (-.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2))) (*.p16 b b)) (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) b))) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) c))))> 3.775 * * * * [progress]: [ 11 / 13 ] simplifiying candidate #posit16 2)) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) a)) (/.p16 (-.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2))) (*.p16 b b)) (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) b))) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) c))))> 3.775 * * * * [progress]: [ 12 / 13 ] simplifiying candidate #posit16 2)) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) a)) (/.p16 (-.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2))) (*.p16 b b)) (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) b))) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) c))))> 3.775 * * * * [progress]: [ 13 / 13 ] simplifiying candidate #posit16 2)) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) a)) (/.p16 (-.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2))) (*.p16 b b)) (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) b))) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) c))))> 3.775 * * * [progress]: adding candidates to table 4.158 * * [progress]: iteration 3 / 4 4.158 * * * [progress]: picking best candidate 4.209 * * * * [pick]: Picked #posit16 2)) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) a)) (/.p16 (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) b) (/.p16 (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) b) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) b)))) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) c))))> 4.209 * * * [progress]: localizing error 4.577 * * * [progress]: generating rewritten candidates 4.577 * * * * [progress]: [ 1 / 4 ] rewriting at (2 1 1 2 2) 4.656 * * * * [progress]: [ 2 / 4 ] rewriting at (2 1 2) 4.678 * * * * [progress]: [ 3 / 4 ] rewriting at (2 1 1 1 2) 4.714 * * * * [progress]: [ 4 / 4 ] rewriting at (2 1 1 2 2 2) 4.759 * * * [progress]: generating series expansions 4.759 * * * * [progress]: [ 1 / 4 ] generating series at (2 1 1 2 2) 4.759 * * * * [progress]: [ 2 / 4 ] generating series at (2 1 2) 4.759 * * * * [progress]: [ 3 / 4 ] generating series at (2 1 1 1 2) 4.759 * * * * [progress]: [ 4 / 4 ] generating series at (2 1 1 2 2 2) 4.759 * * * [progress]: simplifying candidates 4.759 * * * * [progress]: [ 1 / 11 ] simplifiying candidate #posit16 2)) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) a)) (/.p16 (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) b) (*.p16 (/.p16 (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) b) (-.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2))) (*.p16 b b))) (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) b)))) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) c))))> 4.759 * [simplify]: Simplifying (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) b) 4.759 * * [simplify]: iters left: 4 (9 enodes) 4.763 * * [simplify]: iters left: 3 (21 enodes) 4.769 * * [simplify]: iters left: 2 (27 enodes) 4.777 * * [simplify]: iters left: 1 (28 enodes) 4.784 * * [simplify]: Extracting #0: cost 1 inf + 0 4.784 * * [simplify]: Extracting #1: cost 3 inf + 0 4.784 * * [simplify]: Extracting #2: cost 4 inf + 1 4.784 * * [simplify]: Extracting #3: cost 10 inf + 1 4.784 * * [simplify]: Extracting #4: cost 5 inf + 47 4.784 * * [simplify]: Extracting #5: cost 1 inf + 738 4.785 * * [simplify]: Extracting #6: cost 0 inf + 1302 4.785 * [simplify]: Simplified to (+.p16 (/.p16 (+.p16 a (+.p16 c b)) (real->posit16 2)) b) 4.785 * [simplify]: Simplified (2 1 1 2 2 2) to (λ (a b c) (sqrt.p16 (*.p16 (*.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) a)) (/.p16 (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) b) (*.p16 (/.p16 (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) b) (-.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2))) (*.p16 b b))) (+.p16 (/.p16 (+.p16 a (+.p16 c b)) (real->posit16 2)) b)))) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) c)))) 4.785 * * * * [progress]: [ 2 / 11 ] simplifiying candidate #posit16 2)) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) a)) (/.p16 (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) b) (/.p16 (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) b) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) b)))) (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (neg.p16 c)))))> 4.785 * * * * [progress]: [ 3 / 11 ] simplifiying candidate #posit16 2)) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) a)) (/.p16 (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) b) (/.p16 (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) b) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) b)))) (/.p16 (-.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2))) (*.p16 c c)) (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) c)))))> 4.786 * * * * [progress]: [ 4 / 11 ] simplifiying candidate #posit16 2)) (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (neg.p16 a))) (/.p16 (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) b) (/.p16 (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) b) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) b)))) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) c))))> 4.786 * * * * [progress]: [ 5 / 11 ] simplifiying candidate #posit16 2)) (/.p16 (-.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2))) (*.p16 a a)) (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) a))) (/.p16 (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) b) (/.p16 (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) b) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) b)))) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) c))))> 4.786 * * * * [progress]: [ 6 / 11 ] simplifiying candidate #posit16 2)) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) a)) (/.p16 (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) b) (/.p16 (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) b) (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (neg.p16 b))))) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) c))))> 4.786 * * * * [progress]: [ 7 / 11 ] simplifiying candidate #posit16 2)) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) a)) (/.p16 (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) b) (/.p16 (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) b) (/.p16 (-.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2))) (*.p16 b b)) (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) b))))) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) c))))> 4.786 * * * * [progress]: [ 8 / 11 ] simplifiying candidate #posit16 2)) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) a)) (/.p16 (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) b) (/.p16 (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) b) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) b)))) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) c))))> 4.786 * [simplify]: Simplifying (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) b) 4.786 * * [simplify]: iters left: 4 (9 enodes) 4.790 * * [simplify]: iters left: 3 (21 enodes) 4.796 * * [simplify]: iters left: 2 (27 enodes) 4.804 * * [simplify]: iters left: 1 (28 enodes) 4.811 * * [simplify]: Extracting #0: cost 1 inf + 0 4.811 * * [simplify]: Extracting #1: cost 3 inf + 0 4.811 * * [simplify]: Extracting #2: cost 4 inf + 1 4.811 * * [simplify]: Extracting #3: cost 10 inf + 1 4.811 * * [simplify]: Extracting #4: cost 5 inf + 47 4.811 * * [simplify]: Extracting #5: cost 1 inf + 738 4.812 * * [simplify]: Extracting #6: cost 0 inf + 1302 4.812 * [simplify]: Simplified to (+.p16 (/.p16 (+.p16 a (+.p16 c b)) (real->posit16 2)) b) 4.812 * [simplify]: Simplified (2 1 1 2 1) to (λ (a b c) (sqrt.p16 (*.p16 (*.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) a)) (/.p16 (+.p16 (/.p16 (+.p16 a (+.p16 c b)) (real->posit16 2)) b) (/.p16 (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) b) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) b)))) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) c)))) 4.812 * * * * [progress]: [ 9 / 11 ] simplifiying candidate #posit16 2)) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) a)) (/.p16 (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) b) (/.p16 (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) b) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) b)))) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) c))))> 4.813 * [simplify]: Simplifying (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) b) 4.813 * * [simplify]: iters left: 4 (9 enodes) 4.817 * * [simplify]: iters left: 3 (21 enodes) 4.824 * * [simplify]: iters left: 2 (27 enodes) 4.831 * * [simplify]: iters left: 1 (28 enodes) 4.838 * * [simplify]: Extracting #0: cost 1 inf + 0 4.838 * * [simplify]: Extracting #1: cost 3 inf + 0 4.838 * * [simplify]: Extracting #2: cost 4 inf + 1 4.838 * * [simplify]: Extracting #3: cost 10 inf + 1 4.838 * * [simplify]: Extracting #4: cost 5 inf + 47 4.839 * * [simplify]: Extracting #5: cost 1 inf + 738 4.839 * * [simplify]: Extracting #6: cost 0 inf + 1302 4.839 * [simplify]: Simplified to (+.p16 (/.p16 (+.p16 a (+.p16 c b)) (real->posit16 2)) b) 4.839 * [simplify]: Simplified (2 1 1 2 1) to (λ (a b c) (sqrt.p16 (*.p16 (*.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) a)) (/.p16 (+.p16 (/.p16 (+.p16 a (+.p16 c b)) (real->posit16 2)) b) (/.p16 (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) b) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) b)))) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) c)))) 4.840 * * * * [progress]: [ 10 / 11 ] simplifiying candidate #posit16 2)) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) a)) (/.p16 (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) b) (/.p16 (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) b) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) b)))) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) c))))> 4.840 * [simplify]: Simplifying (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) b) 4.840 * * [simplify]: iters left: 4 (9 enodes) 4.844 * * [simplify]: iters left: 3 (21 enodes) 4.850 * * [simplify]: iters left: 2 (27 enodes) 4.858 * * [simplify]: iters left: 1 (28 enodes) 4.865 * * [simplify]: Extracting #0: cost 1 inf + 0 4.865 * * [simplify]: Extracting #1: cost 3 inf + 0 4.865 * * [simplify]: Extracting #2: cost 4 inf + 1 4.865 * * [simplify]: Extracting #3: cost 10 inf + 1 4.865 * * [simplify]: Extracting #4: cost 5 inf + 47 4.865 * * [simplify]: Extracting #5: cost 1 inf + 738 4.865 * * [simplify]: Extracting #6: cost 0 inf + 1302 4.866 * [simplify]: Simplified to (+.p16 (/.p16 (+.p16 a (+.p16 c b)) (real->posit16 2)) b) 4.866 * [simplify]: Simplified (2 1 1 2 1) to (λ (a b c) (sqrt.p16 (*.p16 (*.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) a)) (/.p16 (+.p16 (/.p16 (+.p16 a (+.p16 c b)) (real->posit16 2)) b) (/.p16 (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) b) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) b)))) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) c)))) 4.866 * * * * [progress]: [ 11 / 11 ] simplifiying candidate #posit16 2)) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) a)) (/.p16 (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) b) (/.p16 (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) b) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) b)))) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) c))))> 4.866 * [simplify]: Simplifying (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) b) 4.866 * * [simplify]: iters left: 4 (9 enodes) 4.870 * * [simplify]: iters left: 3 (21 enodes) 4.877 * * [simplify]: iters left: 2 (27 enodes) 4.885 * * [simplify]: iters left: 1 (28 enodes) 4.891 * * [simplify]: Extracting #0: cost 1 inf + 0 4.891 * * [simplify]: Extracting #1: cost 3 inf + 0 4.892 * * [simplify]: Extracting #2: cost 4 inf + 1 4.892 * * [simplify]: Extracting #3: cost 10 inf + 1 4.892 * * [simplify]: Extracting #4: cost 5 inf + 47 4.892 * * [simplify]: Extracting #5: cost 1 inf + 738 4.892 * * [simplify]: Extracting #6: cost 0 inf + 1302 4.892 * [simplify]: Simplified to (+.p16 (/.p16 (+.p16 a (+.p16 c b)) (real->posit16 2)) b) 4.893 * [simplify]: Simplified (2 1 1 2 1) to (λ (a b c) (sqrt.p16 (*.p16 (*.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) a)) (/.p16 (+.p16 (/.p16 (+.p16 a (+.p16 c b)) (real->posit16 2)) b) (/.p16 (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) b) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) b)))) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) c)))) 4.893 * * * [progress]: adding candidates to table 5.215 * * [progress]: iteration 4 / 4 5.215 * * * [progress]: picking best candidate 5.286 * * * * [pick]: Picked #posit16 2)) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) a)) (/.p16 (-.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2))) (*.p16 b b)) (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) b))) (/.p16 (-.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2))) (*.p16 c c)) (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) c)))))> 5.286 * * * [progress]: localizing error 5.980 * * * [progress]: generating rewritten candidates 5.980 * * * * [progress]: [ 1 / 4 ] rewriting at (2 1 2) 6.039 * * * * [progress]: [ 2 / 4 ] rewriting at (2 1 1 2) 6.126 * * * * [progress]: [ 3 / 4 ] rewriting at (2 1 1 1 2) 6.170 * * * * [progress]: [ 4 / 4 ] rewriting at (2 1 1 2 1) 6.176 * * * [progress]: generating series expansions 6.176 * * * * [progress]: [ 1 / 4 ] generating series at (2 1 2) 6.176 * * * * [progress]: [ 2 / 4 ] generating series at (2 1 1 2) 6.176 * * * * [progress]: [ 3 / 4 ] generating series at (2 1 1 1 2) 6.177 * * * * [progress]: [ 4 / 4 ] generating series at (2 1 1 2 1) 6.177 * * * [progress]: simplifying candidates 6.177 * * * * [progress]: [ 1 / 13 ] simplifiying candidate #posit16 2)) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) a)) (/.p16 (-.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2))) (*.p16 b b)) (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) b))) (/.p16 (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) c) (/.p16 (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) c) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) c))))))> 6.177 * [simplify]: Simplifying (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) c) 6.177 * * [simplify]: iters left: 4 (9 enodes) 6.182 * * [simplify]: iters left: 3 (21 enodes) 6.188 * * [simplify]: iters left: 2 (27 enodes) 6.196 * * [simplify]: iters left: 1 (28 enodes) 6.203 * * [simplify]: Extracting #0: cost 1 inf + 0 6.203 * * [simplify]: Extracting #1: cost 3 inf + 0 6.203 * * [simplify]: Extracting #2: cost 4 inf + 1 6.203 * * [simplify]: Extracting #3: cost 10 inf + 1 6.203 * * [simplify]: Extracting #4: cost 5 inf + 47 6.203 * * [simplify]: Extracting #5: cost 1 inf + 738 6.203 * * [simplify]: Extracting #6: cost 0 inf + 1302 6.204 * [simplify]: Simplified to (+.p16 c (/.p16 (+.p16 a (+.p16 c b)) (real->posit16 2))) 6.204 * [simplify]: Simplified (2 1 2 1) to (λ (a b c) (sqrt.p16 (*.p16 (*.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) a)) (/.p16 (-.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2))) (*.p16 b b)) (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) b))) (/.p16 (+.p16 c (/.p16 (+.p16 a (+.p16 c b)) (real->posit16 2))) (/.p16 (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) c) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) c)))))) 6.204 * * * * [progress]: [ 2 / 13 ] simplifiying candidate #posit16 2)) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) a)) (/.p16 (-.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2))) (*.p16 b b)) (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) b))) (/.p16 (-.p16 (*.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2))) (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)))) (*.p16 (*.p16 c c) (*.p16 c c))) (*.p16 (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) c) (+.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2))) (*.p16 c c)))))))> 6.204 * [simplify]: Simplifying (-.p16 (*.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2))) (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)))) (*.p16 (*.p16 c c) (*.p16 c c))) 6.205 * * [simplify]: iters left: 6 (13 enodes) 6.211 * * [simplify]: iters left: 5 (46 enodes) 6.224 * * [simplify]: iters left: 4 (130 enodes) 6.261 * * [simplify]: Extracting #0: cost 1 inf + 0 6.261 * * [simplify]: Extracting #1: cost 25 inf + 0 6.261 * * [simplify]: Extracting #2: cost 62 inf + 0 6.261 * * [simplify]: Extracting #3: cost 154 inf + 82 6.262 * * [simplify]: Extracting #4: cost 155 inf + 19371 6.268 * * [simplify]: Extracting #5: cost 43 inf + 161234 6.279 * * [simplify]: Extracting #6: cost 2 inf + 235712 6.291 * * [simplify]: Extracting #7: cost 0 inf + 242680 6.303 * [simplify]: Simplified to (-.p16 (*.p16 (*.p16 (/.p16 (+.p16 b (+.p16 a c)) (real->posit16 2)) (/.p16 (+.p16 b (+.p16 a c)) (real->posit16 2))) (*.p16 (/.p16 (+.p16 b (+.p16 a c)) (real->posit16 2)) (/.p16 (+.p16 b (+.p16 a c)) (real->posit16 2)))) (*.p16 (*.p16 c c) (*.p16 c c))) 6.304 * [simplify]: Simplified (2 1 2 1) to (λ (a b c) (sqrt.p16 (*.p16 (*.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) a)) (/.p16 (-.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2))) (*.p16 b b)) (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) b))) (/.p16 (-.p16 (*.p16 (*.p16 (/.p16 (+.p16 b (+.p16 a c)) (real->posit16 2)) (/.p16 (+.p16 b (+.p16 a c)) (real->posit16 2))) (*.p16 (/.p16 (+.p16 b (+.p16 a c)) (real->posit16 2)) (/.p16 (+.p16 b (+.p16 a c)) (real->posit16 2)))) (*.p16 (*.p16 c c) (*.p16 c c))) (*.p16 (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) c) (+.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2))) (*.p16 c c))))))) 6.304 * * * * [progress]: [ 3 / 13 ] simplifiying candidate #posit16 2)) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) a)) (/.p16 (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) b) (/.p16 (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) b) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) b)))) (/.p16 (-.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2))) (*.p16 c c)) (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) c)))))> 6.304 * [simplify]: Simplifying (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) b) 6.304 * * [simplify]: iters left: 4 (9 enodes) 6.306 * * [simplify]: iters left: 3 (21 enodes) 6.309 * * [simplify]: iters left: 2 (27 enodes) 6.313 * * [simplify]: iters left: 1 (28 enodes) 6.321 * * [simplify]: Extracting #0: cost 1 inf + 0 6.321 * * [simplify]: Extracting #1: cost 3 inf + 0 6.321 * * [simplify]: Extracting #2: cost 4 inf + 1 6.321 * * [simplify]: Extracting #3: cost 10 inf + 1 6.321 * * [simplify]: Extracting #4: cost 5 inf + 47 6.321 * * [simplify]: Extracting #5: cost 1 inf + 738 6.321 * * [simplify]: Extracting #6: cost 0 inf + 1302 6.322 * [simplify]: Simplified to (+.p16 (/.p16 (+.p16 a (+.p16 c b)) (real->posit16 2)) b) 6.322 * [simplify]: Simplified (2 1 1 2 1) to (λ (a b c) (sqrt.p16 (*.p16 (*.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) a)) (/.p16 (+.p16 (/.p16 (+.p16 a (+.p16 c b)) (real->posit16 2)) b) (/.p16 (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) b) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) b)))) (/.p16 (-.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2))) (*.p16 c c)) (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) c))))) 6.322 * * * * [progress]: [ 4 / 13 ] simplifiying candidate #posit16 2)) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) a)) (/.p16 (-.p16 (*.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2))) (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)))) (*.p16 (*.p16 b b) (*.p16 b b))) (*.p16 (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) b) (+.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2))) (*.p16 b b))))) (/.p16 (-.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2))) (*.p16 c c)) (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) c)))))> 6.322 * [simplify]: Simplifying (-.p16 (*.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2))) (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)))) (*.p16 (*.p16 b b) (*.p16 b b))) 6.323 * * [simplify]: iters left: 6 (13 enodes) 6.326 * * [simplify]: iters left: 5 (46 enodes) 6.335 * * [simplify]: iters left: 4 (130 enodes) 6.380 * * [simplify]: Extracting #0: cost 1 inf + 0 6.380 * * [simplify]: Extracting #1: cost 25 inf + 0 6.380 * * [simplify]: Extracting #2: cost 62 inf + 0 6.380 * * [simplify]: Extracting #3: cost 156 inf + 1 6.382 * * [simplify]: Extracting #4: cost 157 inf + 19646 6.387 * * [simplify]: Extracting #5: cost 52 inf + 148242 6.399 * * [simplify]: Extracting #6: cost 1 inf + 239837 6.414 * * [simplify]: Extracting #7: cost 0 inf + 242361 6.438 * [simplify]: Simplified to (*.p16 (-.p16 (*.p16 (/.p16 (+.p16 (+.p16 b a) c) (real->posit16 2)) (/.p16 (+.p16 (+.p16 b a) c) (real->posit16 2))) (*.p16 b b)) (+.p16 (*.p16 b b) (*.p16 (/.p16 (+.p16 (+.p16 b a) c) (real->posit16 2)) (/.p16 (+.p16 (+.p16 b a) c) (real->posit16 2))))) 6.438 * [simplify]: Simplified (2 1 1 2 1) to (λ (a b c) (sqrt.p16 (*.p16 (*.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) a)) (/.p16 (*.p16 (-.p16 (*.p16 (/.p16 (+.p16 (+.p16 b a) c) (real->posit16 2)) (/.p16 (+.p16 (+.p16 b a) c) (real->posit16 2))) (*.p16 b b)) (+.p16 (*.p16 b b) (*.p16 (/.p16 (+.p16 (+.p16 b a) c) (real->posit16 2)) (/.p16 (+.p16 (+.p16 b a) c) (real->posit16 2))))) (*.p16 (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) b) (+.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2))) (*.p16 b b))))) (/.p16 (-.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2))) (*.p16 c c)) (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) c))))) 6.439 * * * * [progress]: [ 5 / 13 ] simplifiying candidate #posit16 2)) (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (neg.p16 a))) (/.p16 (-.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2))) (*.p16 b b)) (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) b))) (/.p16 (-.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2))) (*.p16 c c)) (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) c)))))> 6.439 * * * * [progress]: [ 6 / 13 ] simplifiying candidate #posit16 2)) (/.p16 (-.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2))) (*.p16 a a)) (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) a))) (/.p16 (-.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2))) (*.p16 b b)) (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) b))) (/.p16 (-.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2))) (*.p16 c c)) (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) c)))))> 6.439 * * * * [progress]: [ 7 / 13 ] simplifiying candidate #posit16 2)) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) a)) (/.p16 (*.p16 (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) b) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) b)) (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) b))) (/.p16 (-.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2))) (*.p16 c c)) (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) c)))))> 6.439 * [simplify]: Simplifying (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) b) 6.439 * * [simplify]: iters left: 4 (9 enodes) 6.443 * * [simplify]: iters left: 3 (21 enodes) 6.449 * * [simplify]: iters left: 2 (27 enodes) 6.457 * * [simplify]: iters left: 1 (28 enodes) 6.464 * * [simplify]: Extracting #0: cost 1 inf + 0 6.464 * * [simplify]: Extracting #1: cost 3 inf + 0 6.464 * * [simplify]: Extracting #2: cost 4 inf + 1 6.465 * * [simplify]: Extracting #3: cost 10 inf + 1 6.465 * * [simplify]: Extracting #4: cost 5 inf + 47 6.465 * * [simplify]: Extracting #5: cost 1 inf + 738 6.465 * * [simplify]: Extracting #6: cost 0 inf + 1302 6.465 * [simplify]: Simplified to (+.p16 (/.p16 (+.p16 a (+.p16 c b)) (real->posit16 2)) b) 6.465 * [simplify]: Simplified (2 1 1 2 1 1) to (λ (a b c) (sqrt.p16 (*.p16 (*.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) a)) (/.p16 (*.p16 (+.p16 (/.p16 (+.p16 a (+.p16 c b)) (real->posit16 2)) b) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) b)) (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) b))) (/.p16 (-.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2))) (*.p16 c c)) (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) c))))) 6.466 * [simplify]: Simplifying (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) b) 6.466 * * [simplify]: iters left: 4 (9 enodes) 6.470 * * [simplify]: iters left: 3 (27 enodes) 6.479 * * [simplify]: iters left: 2 (47 enodes) 6.487 * * [simplify]: iters left: 1 (123 enodes) 6.524 * * [simplify]: Extracting #0: cost 1 inf + 0 6.524 * * [simplify]: Extracting #1: cost 15 inf + 0 6.525 * * [simplify]: Extracting #2: cost 52 inf + 82 6.525 * * [simplify]: Extracting #3: cost 87 inf + 1044 6.526 * * [simplify]: Extracting #4: cost 140 inf + 5615 6.528 * * [simplify]: Extracting #5: cost 118 inf + 19352 6.535 * * [simplify]: Extracting #6: cost 58 inf + 77580 6.546 * * [simplify]: Extracting #7: cost 8 inf + 157140 6.555 * * [simplify]: Extracting #8: cost 0 inf + 176132 6.564 * [simplify]: Simplified to (-.p16 (/.p16 (+.p16 b (+.p16 a c)) (real->posit16 2)) b) 6.564 * [simplify]: Simplified (2 1 1 2 1 2) to (λ (a b c) (sqrt.p16 (*.p16 (*.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) a)) (/.p16 (*.p16 (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) b) (-.p16 (/.p16 (+.p16 b (+.p16 a c)) (real->posit16 2)) b)) (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) b))) (/.p16 (-.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2))) (*.p16 c c)) (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) c))))) 6.564 * * * * [progress]: [ 8 / 13 ] simplifiying candidate #posit16 2)) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) a)) (/.p16 (+.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2))) (neg.p16 (*.p16 b b))) (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) b))) (/.p16 (-.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2))) (*.p16 c c)) (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) c)))))> 6.564 * * * * [progress]: [ 9 / 13 ] simplifiying candidate #posit16 2)) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) a)) (/.p16 (/.p16 (-.p16 (*.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2))) (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)))) (*.p16 (*.p16 b b) (*.p16 b b))) (+.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2))) (*.p16 b b))) (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) b))) (/.p16 (-.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2))) (*.p16 c c)) (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) c)))))> 6.564 * * * * [progress]: [ 10 / 13 ] simplifiying candidate #posit16 2)) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) a)) (/.p16 (-.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2))) (*.p16 b b)) (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) b))) (/.p16 (-.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2))) (*.p16 c c)) (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) c)))))> 6.565 * * * * [progress]: [ 11 / 13 ] simplifiying candidate #posit16 2)) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) a)) (/.p16 (-.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2))) (*.p16 b b)) (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) b))) (/.p16 (-.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2))) (*.p16 c c)) (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) c)))))> 6.565 * * * * [progress]: [ 12 / 13 ] simplifiying candidate #posit16 2)) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) a)) (/.p16 (-.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2))) (*.p16 b b)) (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) b))) (/.p16 (-.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2))) (*.p16 c c)) (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) c)))))> 6.565 * * * * [progress]: [ 13 / 13 ] simplifiying candidate #posit16 2)) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) a)) (/.p16 (-.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2))) (*.p16 b b)) (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) b))) (/.p16 (-.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2))) (*.p16 c c)) (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) c)))))> 6.565 * * * [progress]: adding candidates to table 6.912 * [progress]: [Phase 3 of 3] Extracting. 6.912 * * [regime]: Finding splitpoints for: (#posit16 2)) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) a)) (/.p16 (-.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2))) (*.p16 b b)) (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) b))) (/.p16 (-.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2))) (*.p16 c c)) (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) c)))))> #posit16 2)) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) a)) (/.p16 (-.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2))) (*.p16 b b)) (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) b))) (/.p16 (-.p16 (*.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2))) (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)))) (*.p16 (*.p16 c c) (*.p16 c c))) (*.p16 (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) c) (+.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2))) (*.p16 c c)))))))> #posit16 2)) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) a)) (/.p16 (/.p16 (-.p16 (*.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2))) (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)))) (*.p16 (*.p16 b b) (*.p16 b b))) (+.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2))) (*.p16 b b))) (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) b))) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) c))))> #posit16 2)) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) a)) (/.p16 (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) b) (/.p16 (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) b) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) b)))) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) c))))> #posit16 2)) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) a)) (/.p16 (-.p16 (*.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2))) (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)))) (*.p16 (*.p16 b b) (*.p16 b b))) (*.p16 (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) b) (+.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2))) (*.p16 b b))))) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) c))))>) 6.917 * * * [regime-changes]: Trying 3 branch expressions: (c b a) 6.917 * * * * [regimes]: Trying to branch on c from (#posit16 2)) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) a)) (/.p16 (-.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2))) (*.p16 b b)) (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) b))) (/.p16 (-.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2))) (*.p16 c c)) (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) c)))))> #posit16 2)) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) a)) (/.p16 (-.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2))) (*.p16 b b)) (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) b))) (/.p16 (-.p16 (*.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2))) (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)))) (*.p16 (*.p16 c c) (*.p16 c c))) (*.p16 (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) c) (+.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2))) (*.p16 c c)))))))> #posit16 2)) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) a)) (/.p16 (/.p16 (-.p16 (*.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2))) (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)))) (*.p16 (*.p16 b b) (*.p16 b b))) (+.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2))) (*.p16 b b))) (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) b))) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) c))))> #posit16 2)) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) a)) (/.p16 (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) b) (/.p16 (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) b) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) b)))) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) c))))> #posit16 2)) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) a)) (/.p16 (-.p16 (*.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2))) (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)))) (*.p16 (*.p16 b b) (*.p16 b b))) (*.p16 (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) b) (+.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2))) (*.p16 b b))))) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) c))))>) 7.036 * * * * [regimes]: Trying to branch on b from (#posit16 2)) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) a)) (/.p16 (-.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2))) (*.p16 b b)) (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) b))) (/.p16 (-.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2))) (*.p16 c c)) (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) c)))))> #posit16 2)) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) a)) (/.p16 (-.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2))) (*.p16 b b)) (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) b))) (/.p16 (-.p16 (*.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2))) (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)))) (*.p16 (*.p16 c c) (*.p16 c c))) (*.p16 (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) c) (+.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2))) (*.p16 c c)))))))> #posit16 2)) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) a)) (/.p16 (/.p16 (-.p16 (*.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2))) (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)))) (*.p16 (*.p16 b b) (*.p16 b b))) (+.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2))) (*.p16 b b))) (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) b))) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) c))))> #posit16 2)) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) a)) (/.p16 (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) b) (/.p16 (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) b) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) b)))) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) c))))> #posit16 2)) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) a)) (/.p16 (-.p16 (*.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2))) (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)))) (*.p16 (*.p16 b b) (*.p16 b b))) (*.p16 (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) b) (+.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2))) (*.p16 b b))))) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) c))))>) 7.158 * * * * [regimes]: Trying to branch on a from (#posit16 2)) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) a)) (/.p16 (-.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2))) (*.p16 b b)) (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) b))) (/.p16 (-.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2))) (*.p16 c c)) (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) c)))))> #posit16 2)) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) a)) (/.p16 (-.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2))) (*.p16 b b)) (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) b))) (/.p16 (-.p16 (*.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2))) (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)))) (*.p16 (*.p16 c c) (*.p16 c c))) (*.p16 (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) c) (+.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2))) (*.p16 c c)))))))> #posit16 2)) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) a)) (/.p16 (/.p16 (-.p16 (*.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2))) (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)))) (*.p16 (*.p16 b b) (*.p16 b b))) (+.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2))) (*.p16 b b))) (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) b))) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) c))))> #posit16 2)) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) a)) (/.p16 (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) b) (/.p16 (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) b) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) b)))) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) c))))> #posit16 2)) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) a)) (/.p16 (-.p16 (*.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2))) (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)))) (*.p16 (*.p16 b b) (*.p16 b b))) (*.p16 (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) b) (+.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2))) (*.p16 b b))))) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) c))))>) 7.283 * * * [regime]: Found split indices: #