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.008 * * * * [points]: Setting MPFR precision to 64 0.010 * * * * [points]: Setting MPFR precision to 320 0.011 * * * * [points]: Computing exacts on every 8 of 256 points to ramp up precision 0.015 * * * * [points]: Setting MPFR precision to 64 0.019 * * * * [points]: Setting MPFR precision to 320 0.022 * * * * [points]: Computing exacts on every 4 of 256 points to ramp up precision 0.029 * * * * [points]: Setting MPFR precision to 64 0.036 * * * * [points]: Setting MPFR precision to 320 0.042 * * * * [points]: Computing exacts on every 2 of 256 points to ramp up precision 0.049 * * * * [points]: Setting MPFR precision to 64 0.060 * * * * [points]: Setting MPFR precision to 320 0.071 * * * * [points]: Computing exacts for 256 points 0.079 * * * * [points]: Setting MPFR precision to 64 0.102 * * * * [points]: Setting MPFR precision to 320 0.120 * * * * [points]: Filtering points with unrepresentable outputs 0.121 * * * * [points]: Sampling 219 additional inputs, on iter 1 have 37 / 256 0.122 * * * * [points]: Computing exacts on every 13 of 219 points to ramp up precision 0.125 * * * * [points]: Setting MPFR precision to 64 0.126 * * * * [points]: Setting MPFR precision to 320 0.128 * * * * [points]: Computing exacts on every 6 of 219 points to ramp up precision 0.131 * * * * [points]: Setting MPFR precision to 64 0.133 * * * * [points]: Setting MPFR precision to 320 0.136 * * * * [points]: Computing exacts on every 3 of 219 points to ramp up precision 0.163 * * * * [points]: Setting MPFR precision to 64 0.167 * * * * [points]: Setting MPFR precision to 320 0.171 * * * * [points]: Computing exacts for 219 points 0.177 * * * * [points]: Setting MPFR precision to 64 0.206 * * * * [points]: Setting MPFR precision to 320 0.235 * * * * [points]: Filtering points with unrepresentable outputs 0.235 * * * * [points]: Sampling 184 additional inputs, on iter 2 have 72 / 256 0.237 * * * * [points]: Computing exacts on every 11 of 184 points to ramp up precision 0.244 * * * * [points]: Setting MPFR precision to 64 0.246 * * * * [points]: Setting MPFR precision to 320 0.249 * * * * [points]: Computing exacts on every 5 of 184 points to ramp up precision 0.256 * * * * [points]: Setting MPFR precision to 64 0.260 * * * * [points]: Setting MPFR precision to 320 0.264 * * * * [points]: Computing exacts on every 2 of 184 points to ramp up precision 0.271 * * * * [points]: Setting MPFR precision to 64 0.280 * * * * [points]: Setting MPFR precision to 320 0.288 * * * * [points]: Computing exacts for 184 points 0.296 * * * * [points]: Setting MPFR precision to 64 0.321 * * * * [points]: Setting MPFR precision to 320 0.380 * * * * [points]: Filtering points with unrepresentable outputs 0.381 * * * * [points]: Sampling 152 additional inputs, on iter 3 have 104 / 256 0.382 * * * * [points]: Computing exacts on every 9 of 152 points to ramp up precision 0.393 * * * * [points]: Setting MPFR precision to 64 0.395 * * * * [points]: Setting MPFR precision to 320 0.398 * * * * [points]: Computing exacts on every 4 of 152 points to ramp up precision 0.405 * * * * [points]: Setting MPFR precision to 64 0.409 * * * * [points]: Setting MPFR precision to 320 0.413 * * * * [points]: Computing exacts on every 2 of 152 points to ramp up precision 0.420 * * * * [points]: Setting MPFR precision to 64 0.426 * * * * [points]: Setting MPFR precision to 320 0.433 * * * * [points]: Computing exacts for 152 points 0.439 * * * * [points]: Setting MPFR precision to 64 0.456 * * * * [points]: Setting MPFR precision to 320 0.468 * * * * [points]: Filtering points with unrepresentable outputs 0.468 * * * * [points]: Sampling 142 additional inputs, on iter 4 have 114 / 256 0.468 * * * * [points]: Computing exacts on every 8 of 142 points to ramp up precision 0.472 * * * * [points]: Setting MPFR precision to 64 0.473 * * * * [points]: Setting MPFR precision to 320 0.474 * * * * [points]: Computing exacts on every 4 of 142 points to ramp up precision 0.478 * * * * [points]: Setting MPFR precision to 64 0.480 * * * * [points]: Setting MPFR precision to 320 0.482 * * * * [points]: Computing exacts on every 2 of 142 points to ramp up precision 0.488 * * * * [points]: Setting MPFR precision to 64 0.495 * * * * [points]: Setting MPFR precision to 320 0.500 * * * * [points]: Computing exacts for 142 points 0.507 * * * * [points]: Setting MPFR precision to 64 0.525 * * * * [points]: Setting MPFR precision to 320 0.578 * * * * [points]: Filtering points with unrepresentable outputs 0.578 * * * * [points]: Sampling 123 additional inputs, on iter 5 have 133 / 256 0.579 * * * * [points]: Computing exacts on every 7 of 123 points to ramp up precision 0.586 * * * * [points]: Setting MPFR precision to 64 0.587 * * * * [points]: Setting MPFR precision to 320 0.589 * * * * [points]: Computing exacts on every 3 of 123 points to ramp up precision 0.594 * * * * [points]: Setting MPFR precision to 64 0.596 * * * * [points]: Setting MPFR precision to 320 0.598 * * * * [points]: Computing exacts for 123 points 0.602 * * * * [points]: Setting MPFR precision to 64 0.611 * * * * [points]: Setting MPFR precision to 320 0.619 * * * * [points]: Filtering points with unrepresentable outputs 0.619 * * * * [points]: Sampling 114 additional inputs, on iter 6 have 142 / 256 0.620 * * * * [points]: Computing exacts on every 7 of 114 points to ramp up precision 0.628 * * * * [points]: Setting MPFR precision to 64 0.630 * * * * [points]: Setting MPFR precision to 320 0.632 * * * * [points]: Computing exacts on every 3 of 114 points to ramp up precision 0.638 * * * * [points]: Setting MPFR precision to 64 0.642 * * * * [points]: Setting MPFR precision to 320 0.644 * * * * [points]: Computing exacts for 114 points 0.648 * * * * [points]: Setting MPFR precision to 64 0.656 * * * * [points]: Setting MPFR precision to 320 0.664 * * * * [points]: Filtering points with unrepresentable outputs 0.664 * * * * [points]: Sampling 106 additional inputs, on iter 7 have 150 / 256 0.665 * * * * [points]: Computing exacts on every 6 of 106 points to ramp up precision 0.668 * * * * [points]: Setting MPFR precision to 64 0.669 * * * * [points]: Setting MPFR precision to 320 0.670 * * * * [points]: Computing exacts on every 3 of 106 points to ramp up precision 0.674 * * * * [points]: Setting MPFR precision to 64 0.694 * * * * [points]: Setting MPFR precision to 320 0.696 * * * * [points]: Computing exacts for 106 points 0.699 * * * * [points]: Setting MPFR precision to 64 0.708 * * * * [points]: Setting MPFR precision to 320 0.716 * * * * [points]: Filtering points with unrepresentable outputs 0.716 * * * * [points]: Sampling 97 additional inputs, on iter 8 have 159 / 256 0.716 * * * * [points]: Computing exacts on every 6 of 97 points to ramp up precision 0.720 * * * * [points]: Setting MPFR precision to 64 0.721 * * * * [points]: Setting MPFR precision to 320 0.722 * * * * [points]: Computing exacts on every 3 of 97 points to ramp up precision 0.726 * * * * [points]: Setting MPFR precision to 64 0.728 * * * * [points]: Setting MPFR precision to 320 0.729 * * * * [points]: Computing exacts for 97 points 0.733 * * * * [points]: Setting MPFR precision to 64 0.740 * * * * [points]: Setting MPFR precision to 320 0.751 * * * * [points]: Filtering points with unrepresentable outputs 0.751 * * * * [points]: Sampling 87 additional inputs, on iter 9 have 169 / 256 0.752 * * * * [points]: Computing exacts on every 5 of 87 points to ramp up precision 0.758 * * * * [points]: Setting MPFR precision to 64 0.760 * * * * [points]: Setting MPFR precision to 320 0.762 * * * * [points]: Computing exacts on every 2 of 87 points to ramp up precision 0.769 * * * * [points]: Setting MPFR precision to 64 0.772 * * * * [points]: Setting MPFR precision to 320 0.774 * * * * [points]: Computing exacts for 87 points 0.778 * * * * [points]: Setting MPFR precision to 64 0.784 * * * * [points]: Setting MPFR precision to 320 0.790 * * * * [points]: Filtering points with unrepresentable outputs 0.790 * * * * [points]: Sampling 78 additional inputs, on iter 10 have 178 / 256 0.790 * * * * [points]: Computing exacts on every 4 of 78 points to ramp up precision 0.794 * * * * [points]: Setting MPFR precision to 64 0.795 * * * * [points]: Setting MPFR precision to 320 0.796 * * * * [points]: Computing exacts on every 2 of 78 points to ramp up precision 0.827 * * * * [points]: Setting MPFR precision to 64 0.831 * * * * [points]: Setting MPFR precision to 320 0.837 * * * * [points]: Computing exacts for 78 points 0.844 * * * * [points]: Setting MPFR precision to 64 0.853 * * * * [points]: Setting MPFR precision to 320 0.863 * * * * [points]: Filtering points with unrepresentable outputs 0.863 * * * * [points]: Sampling 65 additional inputs, on iter 11 have 191 / 256 0.864 * * * * [points]: Computing exacts on every 4 of 65 points to ramp up precision 0.871 * * * * [points]: Setting MPFR precision to 64 0.873 * * * * [points]: Setting MPFR precision to 320 0.875 * * * * [points]: Computing exacts on every 2 of 65 points to ramp up precision 0.881 * * * * [points]: Setting MPFR precision to 64 0.884 * * * * [points]: Setting MPFR precision to 320 0.887 * * * * [points]: Computing exacts for 65 points 0.894 * * * * [points]: Setting MPFR precision to 64 0.902 * * * * [points]: Setting MPFR precision to 320 0.910 * * * * [points]: Filtering points with unrepresentable outputs 0.910 * * * * [points]: Sampling 57 additional inputs, on iter 12 have 199 / 256 0.911 * * * * [points]: Computing exacts on every 3 of 57 points to ramp up precision 0.917 * * * * [points]: Setting MPFR precision to 64 0.919 * * * * [points]: Setting MPFR precision to 320 0.921 * * * * [points]: Computing exacts for 57 points 0.929 * * * * [points]: Setting MPFR precision to 64 0.936 * * * * [points]: Setting MPFR precision to 320 0.943 * * * * [points]: Filtering points with unrepresentable outputs 0.943 * * * * [points]: Sampling 49 additional inputs, on iter 13 have 207 / 256 0.943 * * * * [points]: Computing exacts on every 3 of 49 points to ramp up precision 0.949 * * * * [points]: Setting MPFR precision to 64 0.950 * * * * [points]: Setting MPFR precision to 320 0.951 * * * * [points]: Computing exacts for 49 points 0.954 * * * * [points]: Setting MPFR precision to 64 0.958 * * * * [points]: Setting MPFR precision to 320 0.961 * * * * [points]: Filtering points with unrepresentable outputs 0.961 * * * * [points]: Sampling 43 additional inputs, on iter 14 have 213 / 256 0.961 * * * * [points]: Computing exacts on every 2 of 43 points to ramp up precision 0.965 * * * * [points]: Setting MPFR precision to 64 0.984 * * * * [points]: Setting MPFR precision to 320 0.985 * * * * [points]: Computing exacts for 43 points 0.991 * * * * [points]: Setting MPFR precision to 64 0.997 * * * * [points]: Setting MPFR precision to 320 1.003 * * * * [points]: Filtering points with unrepresentable outputs 1.003 * * * * [points]: Sampling 39 additional inputs, on iter 15 have 217 / 256 1.003 * * * * [points]: Computing exacts on every 2 of 39 points to ramp up precision 1.011 * * * * [points]: Setting MPFR precision to 64 1.013 * * * * [points]: Setting MPFR precision to 320 1.015 * * * * [points]: Computing exacts for 39 points 1.022 * * * * [points]: Setting MPFR precision to 64 1.027 * * * * [points]: Setting MPFR precision to 320 1.032 * * * * [points]: Filtering points with unrepresentable outputs 1.032 * * * * [points]: Sampling 35 additional inputs, on iter 16 have 221 / 256 1.032 * * * * [points]: Computing exacts on every 2 of 35 points to ramp up precision 1.039 * * * * [points]: Setting MPFR precision to 64 1.041 * * * * [points]: Setting MPFR precision to 320 1.042 * * * * [points]: Computing exacts for 35 points 1.049 * * * * [points]: Setting MPFR precision to 64 1.054 * * * * [points]: Setting MPFR precision to 320 1.058 * * * * [points]: Filtering points with unrepresentable outputs 1.058 * * * * [points]: Sampling 30 additional inputs, on iter 17 have 226 / 256 1.059 * * * * [points]: Computing exacts for 30 points 1.066 * * * * [points]: Setting MPFR precision to 64 1.070 * * * * [points]: Setting MPFR precision to 320 1.074 * * * * [points]: Filtering points with unrepresentable outputs 1.074 * * * * [points]: Sampling 26 additional inputs, on iter 18 have 230 / 256 1.074 * * * * [points]: Computing exacts for 26 points 1.080 * * * * [points]: Setting MPFR precision to 64 1.082 * * * * [points]: Setting MPFR precision to 320 1.084 * * * * [points]: Filtering points with unrepresentable outputs 1.084 * * * * [points]: Sampling 23 additional inputs, on iter 19 have 233 / 256 1.084 * * * * [points]: Computing exacts for 23 points 1.088 * * * * [points]: Setting MPFR precision to 64 1.089 * * * * [points]: Setting MPFR precision to 320 1.091 * * * * [points]: Filtering points with unrepresentable outputs 1.092 * * * * [points]: Sampling 19 additional inputs, on iter 20 have 237 / 256 1.092 * * * * [points]: Computing exacts for 19 points 1.096 * * * * [points]: Setting MPFR precision to 64 1.097 * * * * [points]: Setting MPFR precision to 320 1.099 * * * * [points]: Filtering points with unrepresentable outputs 1.099 * * * * [points]: Sampling 17 additional inputs, on iter 21 have 239 / 256 1.099 * * * * [points]: Computing exacts for 17 points 1.103 * * * * [points]: Setting MPFR precision to 64 1.104 * * * * [points]: Setting MPFR precision to 320 1.105 * * * * [points]: Filtering points with unrepresentable outputs 1.105 * * * * [points]: Sampling 14 additional inputs, on iter 22 have 242 / 256 1.105 * * * * [points]: Computing exacts for 14 points 1.109 * * * * [points]: Setting MPFR precision to 64 1.110 * * * * [points]: Setting MPFR precision to 320 1.126 * * * * [points]: Filtering points with unrepresentable outputs 1.127 * * * * [points]: Sampling 13 additional inputs, on iter 23 have 243 / 256 1.127 * * * * [points]: Computing exacts for 13 points 1.130 * * * * [points]: Setting MPFR precision to 64 1.131 * * * * [points]: Setting MPFR precision to 320 1.132 * * * * [points]: Filtering points with unrepresentable outputs 1.132 * * * * [points]: Sampling 13 additional inputs, on iter 24 have 243 / 256 1.133 * * * * [points]: Computing exacts for 13 points 1.138 * * * * [points]: Setting MPFR precision to 64 1.139 * * * * [points]: Setting MPFR precision to 320 1.140 * * * * [points]: Filtering points with unrepresentable outputs 1.140 * * * * [points]: Sampling 9 additional inputs, on iter 25 have 247 / 256 1.140 * * * * [points]: Computing exacts for 9 points 1.144 * * * * [points]: Setting MPFR precision to 64 1.144 * * * * [points]: Setting MPFR precision to 320 1.145 * * * * [points]: Filtering points with unrepresentable outputs 1.145 * * * * [points]: Sampling 8 additional inputs, on iter 26 have 248 / 256 1.145 * * * * [points]: Computing exacts for 8 points 1.149 * * * * [points]: Setting MPFR precision to 64 1.150 * * * * [points]: Setting MPFR precision to 320 1.150 * * * * [points]: Filtering points with unrepresentable outputs 1.150 * * * * [points]: Sampling 8 additional inputs, on iter 27 have 248 / 256 1.150 * * * * [points]: Computing exacts for 8 points 1.154 * * * * [points]: Setting MPFR precision to 64 1.155 * * * * [points]: Setting MPFR precision to 320 1.155 * * * * [points]: Filtering points with unrepresentable outputs 1.155 * * * * [points]: Sampling 7 additional inputs, on iter 28 have 249 / 256 1.155 * * * * [points]: Computing exacts for 7 points 1.159 * * * * [points]: Setting MPFR precision to 64 1.159 * * * * [points]: Setting MPFR precision to 320 1.160 * * * * [points]: Filtering points with unrepresentable outputs 1.160 * * * * [points]: Sampling 7 additional inputs, on iter 29 have 249 / 256 1.160 * * * * [points]: Computing exacts for 7 points 1.164 * * * * [points]: Setting MPFR precision to 64 1.164 * * * * [points]: Setting MPFR precision to 320 1.165 * * * * [points]: Filtering points with unrepresentable outputs 1.165 * * * * [points]: Sampling 7 additional inputs, on iter 30 have 249 / 256 1.165 * * * * [points]: Computing exacts for 7 points 1.169 * * * * [points]: Setting MPFR precision to 64 1.169 * * * * [points]: Setting MPFR precision to 320 1.170 * * * * [points]: Filtering points with unrepresentable outputs 1.170 * * * * [points]: Sampling 5 additional inputs, on iter 31 have 251 / 256 1.170 * * * * [points]: Computing exacts for 5 points 1.173 * * * * [points]: Setting MPFR precision to 64 1.174 * * * * [points]: Setting MPFR precision to 320 1.174 * * * * [points]: Filtering points with unrepresentable outputs 1.174 * * * * [points]: Sampling 5 additional inputs, on iter 32 have 251 / 256 1.174 * * * * [points]: Computing exacts for 5 points 1.179 * * * * [points]: Setting MPFR precision to 64 1.179 * * * * [points]: Setting MPFR precision to 320 1.180 * * * * [points]: Filtering points with unrepresentable outputs 1.180 * * * * [points]: Sampling 5 additional inputs, on iter 33 have 251 / 256 1.180 * * * * [points]: Computing exacts for 5 points 1.183 * * * * [points]: Setting MPFR precision to 64 1.184 * * * * [points]: Setting MPFR precision to 320 1.184 * * * * [points]: Filtering points with unrepresentable outputs 1.184 * * * * [points]: Sampling 4 additional inputs, on iter 34 have 253 / 256 1.184 * * * * [points]: Computing exacts for 4 points 1.188 * * * * [points]: Setting MPFR precision to 64 1.188 * * * * [points]: Setting MPFR precision to 320 1.189 * * * * [points]: Filtering points with unrepresentable outputs 1.189 * * * * [points]: Sampling 4 additional inputs, on iter 35 have 255 / 256 1.189 * * * * [points]: Computing exacts for 4 points 1.192 * * * * [points]: Setting MPFR precision to 64 1.193 * * * * [points]: Setting MPFR precision to 320 1.193 * * * * [points]: Filtering points with unrepresentable outputs 1.193 * * * * [points]: Sampled 256 points with exact outputs 1.193 * * * [progress]: [2/2] Setting up program. 1.213 * [progress]: [Phase 2 of 3] Improving. 1.213 * * * * [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.213 * [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.213 * * [simplify]: iteration 1: (15 enodes) 1.220 * * [simplify]: iteration 2: (54 enodes) 1.233 * * [simplify]: iteration 3: (174 enodes) 1.319 * * [simplify]: iteration 4: (1021 enodes) 3.041 * * [simplify]: Extracting #0: cost 1 inf + 0 3.041 * * [simplify]: Extracting #1: cost 2 inf + 0 3.041 * * [simplify]: Extracting #2: cost 174 inf + 0 3.044 * * [simplify]: Extracting #3: cost 1342 inf + 0 3.053 * * [simplify]: Extracting #4: cost 2271 inf + 691 3.065 * * [simplify]: Extracting #5: cost 2231 inf + 82476 3.141 * * [simplify]: Extracting #6: cost 1375 inf + 1509565 3.429 * * [simplify]: Extracting #7: cost 86 inf + 4121745 3.796 * * [simplify]: Extracting #8: cost 0 inf + 3944289 4.074 * * [simplify]: Extracting #9: cost 0 inf + 3923289 4.428 * [simplify]: Simplified to: (sqrt.p16 (*.p16 (*.p16 (/.p16 (+.p16 (+.p16 c b) a) (real->posit16 2)) (*.p16 (-.p16 (/.p16 (+.p16 (+.p16 c b) a) (real->posit16 2)) c) (-.p16 (/.p16 (+.p16 (+.p16 c b) a) (real->posit16 2)) b))) (-.p16 (/.p16 (+.p16 (+.p16 c b) a) (real->posit16 2)) a))) 4.444 * * [progress]: iteration 1 / 4 4.444 * * * [progress]: picking best candidate 4.464 * * * * [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))))> 4.464 * * * [progress]: localizing error 4.786 * * * [progress]: generating rewritten candidates 4.786 * * * * [progress]: [ 1 / 4 ] rewriting at (2 1 2) 4.844 * * * * [progress]: [ 2 / 4 ] rewriting at (2 1 1 1 2) 4.892 * * * * [progress]: [ 3 / 4 ] rewriting at (2 1 1 2) 4.941 * * * * [progress]: [ 4 / 4 ] rewriting at (2 1 2 1) 4.967 * * * [progress]: generating series expansions 4.968 * * * * [progress]: [ 1 / 4 ] generating series at (2 1 2) 4.968 * * * * [progress]: [ 2 / 4 ] generating series at (2 1 1 1 2) 4.968 * * * * [progress]: [ 3 / 4 ] generating series at (2 1 1 2) 4.968 * * * * [progress]: [ 4 / 4 ] generating series at (2 1 2 1) 4.968 * * * [progress]: simplifying candidates 4.968 * * * * [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)))))> 4.968 * * * * [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)))))> 4.968 * * * * [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))))> 4.968 * * * * [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))))> 4.968 * * * * [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))))> 4.968 * * * * [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))))> 4.968 * * * * [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))))> 4.968 * * * * [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))))> 4.968 * * * * [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))))> 4.969 * * * * [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))))> 4.969 * [simplify]: Simplifying: (neg.p16 c) (-.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) (neg.p16 a) (-.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) (neg.p16 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) (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))) (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))) (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))) (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))) 4.970 * * [simplify]: iteration 1: (28 enodes) 4.981 * * [simplify]: iteration 2: (83 enodes) 5.013 * * [simplify]: iteration 3: (285 enodes) 5.219 * * [simplify]: iteration 4: (1785 enodes) 11.649 * * [simplify]: Extracting #0: cost 10 inf + 0 11.650 * * [simplify]: Extracting #1: cost 190 inf + 0 11.655 * * [simplify]: Extracting #2: cost 1095 inf + 2813 11.676 * * [simplify]: Extracting #3: cost 3592 inf + 10264 11.722 * * [simplify]: Extracting #4: cost 5603 inf + 59377 11.849 * * [simplify]: Extracting #5: cost 4896 inf + 1192482 12.557 * * [simplify]: Extracting #6: cost 1089 inf + 8532425 13.674 * * [simplify]: Extracting #7: cost 3 inf + 10939844 14.802 * * [simplify]: Extracting #8: cost 0 inf + 10935016 15.712 * [simplify]: Simplified to: (neg.p16 c) (*.p16 (+.p16 c (/.p16 (+.p16 c (+.p16 a b)) (real->posit16 2))) (-.p16 (/.p16 (+.p16 c (+.p16 a b)) (real->posit16 2)) c)) (+.p16 c (/.p16 (+.p16 c (+.p16 a b)) (real->posit16 2))) (neg.p16 a) (*.p16 (-.p16 (/.p16 (+.p16 c (+.p16 a b)) (real->posit16 2)) a) (+.p16 (/.p16 (+.p16 c (+.p16 a b)) (real->posit16 2)) a)) (+.p16 (/.p16 (+.p16 c (+.p16 a b)) (real->posit16 2)) a) (neg.p16 b) (*.p16 (-.p16 (/.p16 (+.p16 c (+.p16 a b)) (real->posit16 2)) b) (+.p16 b (/.p16 (+.p16 c (+.p16 a b)) (real->posit16 2)))) (+.p16 b (/.p16 (+.p16 c (+.p16 a b)) (real->posit16 2))) (sqrt.p16 (*.p16 (-.p16 (/.p16 (+.p16 c (+.p16 a b)) (real->posit16 2)) b) (*.p16 (*.p16 (/.p16 (+.p16 c (+.p16 a b)) (real->posit16 2)) (-.p16 (/.p16 (+.p16 c (+.p16 a b)) (real->posit16 2)) a)) (-.p16 (/.p16 (+.p16 c (+.p16 a b)) (real->posit16 2)) c)))) (sqrt.p16 (*.p16 (-.p16 (/.p16 (+.p16 c (+.p16 a b)) (real->posit16 2)) b) (*.p16 (*.p16 (/.p16 (+.p16 c (+.p16 a b)) (real->posit16 2)) (-.p16 (/.p16 (+.p16 c (+.p16 a b)) (real->posit16 2)) a)) (-.p16 (/.p16 (+.p16 c (+.p16 a b)) (real->posit16 2)) c)))) (sqrt.p16 (*.p16 (-.p16 (/.p16 (+.p16 c (+.p16 a b)) (real->posit16 2)) b) (*.p16 (*.p16 (/.p16 (+.p16 c (+.p16 a b)) (real->posit16 2)) (-.p16 (/.p16 (+.p16 c (+.p16 a b)) (real->posit16 2)) a)) (-.p16 (/.p16 (+.p16 c (+.p16 a b)) (real->posit16 2)) c)))) (sqrt.p16 (*.p16 (-.p16 (/.p16 (+.p16 c (+.p16 a b)) (real->posit16 2)) b) (*.p16 (*.p16 (/.p16 (+.p16 c (+.p16 a b)) (real->posit16 2)) (-.p16 (/.p16 (+.p16 c (+.p16 a b)) (real->posit16 2)) a)) (-.p16 (/.p16 (+.p16 c (+.p16 a b)) (real->posit16 2)) c)))) 15.714 * * * [progress]: adding candidates to table 16.002 * * [progress]: iteration 2 / 4 16.002 * * * [progress]: picking best candidate 16.072 * * * * [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 (+.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)))))> 16.072 * * * [progress]: localizing error 16.492 * * * [progress]: generating rewritten candidates 16.492 * * * * [progress]: [ 1 / 4 ] rewriting at (2 1 2) 16.621 * * * * [progress]: [ 2 / 4 ] rewriting at (2 1 1 1 2) 16.646 * * * * [progress]: [ 3 / 4 ] rewriting at (2 1 2 1) 16.652 * * * * [progress]: [ 4 / 4 ] rewriting at (2 1 1 2) 16.701 * * * [progress]: generating series expansions 16.701 * * * * [progress]: [ 1 / 4 ] generating series at (2 1 2) 16.701 * * * * [progress]: [ 2 / 4 ] generating series at (2 1 1 1 2) 16.701 * * * * [progress]: [ 3 / 4 ] generating series at (2 1 2 1) 16.701 * * * * [progress]: [ 4 / 4 ] generating series at (2 1 1 2) 16.701 * * * [progress]: simplifying candidates 16.701 * * * * [progress]: [ 1 / 13 ] 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 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))))))> 16.702 * * * * [progress]: [ 2 / 13 ] 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 (+.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)))))))> 16.702 * * * * [progress]: [ 3 / 13 ] 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 (+.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)))))> 16.702 * * * * [progress]: [ 4 / 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 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)))))> 16.702 * * * * [progress]: [ 5 / 13 ] 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)) c) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) c)) (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) c)))))> 16.702 * * * * [progress]: [ 6 / 13 ] 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))) (neg.p16 (*.p16 c c))) (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) c)))))> 16.702 * * * * [progress]: [ 7 / 13 ] 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 (+.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)) (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2))) (*.p16 c c))) (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) c)))))> 16.702 * * * * [progress]: [ 8 / 13 ] 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 (+.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)))))> 16.702 * * * * [progress]: [ 9 / 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)))))> 16.702 * * * * [progress]: [ 10 / 13 ] 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)))))> 16.702 * * * * [progress]: [ 11 / 13 ] 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)))))> 16.703 * * * * [progress]: [ 12 / 13 ] 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)))))> 16.703 * * * * [progress]: [ 13 / 13 ] 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)))))> 16.703 * [simplify]: Simplifying: (/.p16 (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) c) (-.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 (+.p16 a b) c) (real->posit16 2)) (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2))) (*.p16 c c))) (neg.p16 a) (-.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)) c) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) c) (neg.p16 (*.p16 c c)) (-.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)) (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2))) (*.p16 c c)) (neg.p16 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 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) (-.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) (-.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) (-.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) 16.704 * * [simplify]: iteration 1: (28 enodes) 16.717 * * [simplify]: iteration 2: (92 enodes) 16.737 * * [simplify]: iteration 3: (269 enodes) 16.820 * * [simplify]: iteration 4: (1093 enodes) 18.136 * * [simplify]: Extracting #0: cost 14 inf + 0 18.137 * * [simplify]: Extracting #1: cost 328 inf + 0 18.141 * * [simplify]: Extracting #2: cost 1346 inf + 2891 18.148 * * [simplify]: Extracting #3: cost 1842 inf + 18997 18.160 * * [simplify]: Extracting #4: cost 1998 inf + 90109 18.194 * * [simplify]: Extracting #5: cost 1816 inf + 298720 18.297 * * [simplify]: Extracting #6: cost 982 inf + 1851714 18.590 * * [simplify]: Extracting #7: cost 64 inf + 3878875 18.917 * * [simplify]: Extracting #8: cost 0 inf + 4027702 19.230 * [simplify]: Simplified to: (/.p16 (+.p16 c (/.p16 (+.p16 b (+.p16 a c)) (real->posit16 2))) (-.p16 (/.p16 (+.p16 b (+.p16 a c)) (real->posit16 2)) c)) (*.p16 (+.p16 c (/.p16 (+.p16 b (+.p16 a c)) (real->posit16 2))) (+.p16 (*.p16 (/.p16 (+.p16 b (+.p16 a c)) (real->posit16 2)) (/.p16 (+.p16 b (+.p16 a c)) (real->posit16 2))) (*.p16 c c))) (neg.p16 a) (*.p16 (+.p16 a (/.p16 (+.p16 b (+.p16 a c)) (real->posit16 2))) (-.p16 (/.p16 (+.p16 b (+.p16 a c)) (real->posit16 2)) a)) (+.p16 a (/.p16 (+.p16 b (+.p16 a c)) (real->posit16 2))) (+.p16 c (/.p16 (+.p16 b (+.p16 a c)) (real->posit16 2))) (-.p16 (/.p16 (+.p16 b (+.p16 a c)) (real->posit16 2)) c) (neg.p16 (*.p16 c c)) (*.p16 (-.p16 (*.p16 (/.p16 (+.p16 b (+.p16 a c)) (real->posit16 2)) (/.p16 (+.p16 b (+.p16 a c)) (real->posit16 2))) (*.p16 c c)) (+.p16 (*.p16 (/.p16 (+.p16 b (+.p16 a c)) (real->posit16 2)) (/.p16 (+.p16 b (+.p16 a c)) (real->posit16 2))) (*.p16 c c))) (+.p16 (*.p16 (/.p16 (+.p16 b (+.p16 a c)) (real->posit16 2)) (/.p16 (+.p16 b (+.p16 a c)) (real->posit16 2))) (*.p16 c c)) (neg.p16 b) (*.p16 (+.p16 (/.p16 (+.p16 b (+.p16 a c)) (real->posit16 2)) b) (-.p16 (/.p16 (+.p16 b (+.p16 a c)) (real->posit16 2)) b)) (+.p16 (/.p16 (+.p16 b (+.p16 a c)) (real->posit16 2)) b) (*.p16 (+.p16 c (/.p16 (+.p16 b (+.p16 a c)) (real->posit16 2))) (-.p16 (/.p16 (+.p16 b (+.p16 a c)) (real->posit16 2)) c)) (+.p16 c (/.p16 (+.p16 b (+.p16 a c)) (real->posit16 2))) (*.p16 (+.p16 c (/.p16 (+.p16 b (+.p16 a c)) (real->posit16 2))) (-.p16 (/.p16 (+.p16 b (+.p16 a c)) (real->posit16 2)) c)) (+.p16 c (/.p16 (+.p16 b (+.p16 a c)) (real->posit16 2))) (*.p16 (+.p16 c (/.p16 (+.p16 b (+.p16 a c)) (real->posit16 2))) (-.p16 (/.p16 (+.p16 b (+.p16 a c)) (real->posit16 2)) c)) (+.p16 c (/.p16 (+.p16 b (+.p16 a c)) (real->posit16 2))) (*.p16 (+.p16 c (/.p16 (+.p16 b (+.p16 a c)) (real->posit16 2))) (-.p16 (/.p16 (+.p16 b (+.p16 a c)) (real->posit16 2)) c)) (+.p16 c (/.p16 (+.p16 b (+.p16 a c)) (real->posit16 2))) 19.233 * * * [progress]: adding candidates to table 19.601 * * [progress]: iteration 3 / 4 19.601 * * * [progress]: picking best candidate 19.691 * * * * [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 (+.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))))))> 19.691 * * * [progress]: localizing error 20.197 * * * [progress]: generating rewritten candidates 20.197 * * * * [progress]: [ 1 / 4 ] rewriting at (2 1 2 2) 20.372 * * * * [progress]: [ 2 / 4 ] rewriting at (2 1 2 2 2) 20.420 * * * * [progress]: [ 3 / 4 ] rewriting at (2 1 1 1 2) 20.469 * * * * [progress]: [ 4 / 4 ] rewriting at (2 1 1 2) 20.518 * * * [progress]: generating series expansions 20.518 * * * * [progress]: [ 1 / 4 ] generating series at (2 1 2 2) 20.518 * * * * [progress]: [ 2 / 4 ] generating series at (2 1 2 2 2) 20.518 * * * * [progress]: [ 3 / 4 ] generating series at (2 1 1 1 2) 20.518 * * * * [progress]: [ 4 / 4 ] generating series at (2 1 1 2) 20.518 * * * [progress]: simplifying candidates 20.518 * * * * [progress]: [ 1 / 11 ] 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 a b) c) (real->posit16 2)) c) (*.p16 (/.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))) (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) c))))))> 20.518 * * * * [progress]: [ 2 / 11 ] 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 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)) (neg.p16 c)))))))> 20.519 * * * * [progress]: [ 3 / 11 ] 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 a b) c) (real->posit16 2)) c) (/.p16 (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) c) (/.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)))))))> 20.519 * * * * [progress]: [ 4 / 11 ] 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 (+.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))))))> 20.519 * * * * [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 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))))))> 20.519 * * * * [progress]: [ 6 / 11 ] 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 (+.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))))))> 20.519 * * * * [progress]: [ 7 / 11 ] 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))))))> 20.519 * * * * [progress]: [ 8 / 11 ] 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 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))))))> 20.519 * * * * [progress]: [ 9 / 11 ] 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 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))))))> 20.519 * * * * [progress]: [ 10 / 11 ] 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 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))))))> 20.519 * * * * [progress]: [ 11 / 11 ] 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 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))))))> 20.520 * [simplify]: Simplifying: (/.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))) (neg.p16 c) (-.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) (neg.p16 a) (-.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) (neg.p16 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 a b) c) (real->posit16 2)) c) (-.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)) (/.p16 (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) c) (-.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)) 20.520 * * [simplify]: iteration 1: (24 enodes) 20.530 * * [simplify]: iteration 2: (68 enodes) 20.554 * * [simplify]: iteration 3: (168 enodes) 20.632 * * [simplify]: iteration 4: (605 enodes) 21.289 * * [simplify]: Extracting #0: cost 11 inf + 0 21.289 * * [simplify]: Extracting #1: cost 178 inf + 0 21.294 * * [simplify]: Extracting #2: cost 676 inf + 405 21.301 * * [simplify]: Extracting #3: cost 903 inf + 5940 21.311 * * [simplify]: Extracting #4: cost 1070 inf + 38463 21.344 * * [simplify]: Extracting #5: cost 906 inf + 258791 21.462 * * [simplify]: Extracting #6: cost 304 inf + 1295525 21.670 * * [simplify]: Extracting #7: cost 20 inf + 1870832 21.882 * * [simplify]: Extracting #8: cost 0 inf + 1922731 22.096 * * [simplify]: Extracting #9: cost 0 inf + 1922575 22.323 * [simplify]: Simplified to: (/.p16 (real->posit16 1.0) (-.p16 (/.p16 (+.p16 (+.p16 b a) c) (real->posit16 2)) c)) (neg.p16 c) (*.p16 (+.p16 c (/.p16 (+.p16 (+.p16 b a) c) (real->posit16 2))) (-.p16 (/.p16 (+.p16 (+.p16 b a) c) (real->posit16 2)) c)) (+.p16 c (/.p16 (+.p16 (+.p16 b a) c) (real->posit16 2))) (neg.p16 a) (*.p16 (+.p16 a (/.p16 (+.p16 (+.p16 b a) c) (real->posit16 2))) (-.p16 (/.p16 (+.p16 (+.p16 b a) c) (real->posit16 2)) a)) (+.p16 a (/.p16 (+.p16 (+.p16 b a) c) (real->posit16 2))) (neg.p16 b) (*.p16 (-.p16 (/.p16 (+.p16 (+.p16 b a) c) (real->posit16 2)) b) (+.p16 (/.p16 (+.p16 (+.p16 b a) c) (real->posit16 2)) b)) (+.p16 (/.p16 (+.p16 (+.p16 b a) c) (real->posit16 2)) b) (/.p16 (+.p16 c (/.p16 (+.p16 (+.p16 b a) c) (real->posit16 2))) (-.p16 (/.p16 (+.p16 (+.p16 b a) c) (real->posit16 2)) c)) (/.p16 (+.p16 c (/.p16 (+.p16 (+.p16 b a) c) (real->posit16 2))) (-.p16 (/.p16 (+.p16 (+.p16 b a) c) (real->posit16 2)) c)) (/.p16 (+.p16 c (/.p16 (+.p16 (+.p16 b a) c) (real->posit16 2))) (-.p16 (/.p16 (+.p16 (+.p16 b a) c) (real->posit16 2)) c)) (/.p16 (+.p16 c (/.p16 (+.p16 (+.p16 b a) c) (real->posit16 2))) (-.p16 (/.p16 (+.p16 (+.p16 b a) c) (real->posit16 2)) c)) 22.325 * * * [progress]: adding candidates to table 22.606 * * [progress]: iteration 4 / 4 22.606 * * * [progress]: picking best candidate 22.644 * * * * [pick]: Picked #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 (+.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)))))> 22.645 * * * [progress]: localizing error 23.424 * * * [progress]: generating rewritten candidates 23.424 * * * * [progress]: [ 1 / 4 ] rewriting at (2 1 1 1 2) 23.515 * * * * [progress]: [ 2 / 4 ] rewriting at (2 1 2) 23.594 * * * * [progress]: [ 3 / 4 ] rewriting at (2 1 1 1 2 1) 23.600 * * * * [progress]: [ 4 / 4 ] rewriting at (2 1 2 1) 23.607 * * * [progress]: generating series expansions 23.607 * * * * [progress]: [ 1 / 4 ] generating series at (2 1 1 1 2) 23.607 * * * * [progress]: [ 2 / 4 ] generating series at (2 1 2) 23.607 * * * * [progress]: [ 3 / 4 ] generating series at (2 1 1 1 2 1) 23.607 * * * * [progress]: [ 4 / 4 ] generating series at (2 1 2 1) 23.607 * * * [progress]: simplifying candidates 23.607 * * * * [progress]: [ 1 / 14 ] simplifiying candidate #posit16 2)) (/.p16 (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) a) (/.p16 (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) 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 (+.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)))))> 23.607 * * * * [progress]: [ 2 / 14 ] simplifiying candidate #posit16 2)) (/.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 a a) (*.p16 a a))) (*.p16 (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) a) (+.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)) 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)))))> 23.607 * * * * [progress]: [ 3 / 14 ] 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 (+.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))))))> 23.607 * * * * [progress]: [ 4 / 14 ] 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 (/.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)))))))> 23.607 * * * * [progress]: [ 5 / 14 ] simplifiying candidate #posit16 2)) (/.p16 (*.p16 (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) a) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) 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 (+.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)))))> 23.608 * * * * [progress]: [ 6 / 14 ] 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))) (neg.p16 (*.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 (+.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)))))> 23.608 * * * * [progress]: [ 7 / 14 ] simplifiying candidate #posit16 2)) (/.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 a a) (*.p16 a a))) (+.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 (+.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)))))> 23.608 * * * * [progress]: [ 8 / 14 ] 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 (+.p16 (+.p16 a b) c) (real->posit16 2)) c) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) c)) (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) c)))))> 23.608 * * * * [progress]: [ 9 / 14 ] 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 (+.p16 (+.p16 a b) c) (real->posit16 2)) (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2))) (neg.p16 (*.p16 c c))) (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) c)))))> 23.608 * * * * [progress]: [ 10 / 14 ] 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 (*.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)) (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2))) (*.p16 c c))) (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) c)))))> 23.608 * * * * [progress]: [ 11 / 14 ] 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 (+.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)))))> 23.608 * * * * [progress]: [ 12 / 14 ] 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 (+.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)))))> 23.608 * * * * [progress]: [ 13 / 14 ] 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 (+.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)))))> 23.608 * * * * [progress]: [ 14 / 14 ] 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 (+.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)))))> 23.609 * [simplify]: Simplifying: (/.p16 (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) a) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) a)) (*.p16 (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) a) (+.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 (+.p16 a b) c) (real->posit16 2)) c) (-.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 (+.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)) a) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) a) (neg.p16 (*.p16 a a)) (-.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 a a) (*.p16 a a))) (+.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)) c) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) c) (neg.p16 (*.p16 c c)) (-.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)) (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2))) (*.p16 c c)) (-.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)) (/.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)) (/.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)) (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2))) (*.p16 a a)) (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) a) 23.609 * * [simplify]: iteration 1: (29 enodes) 23.621 * * [simplify]: iteration 2: (99 enodes) 23.658 * * [simplify]: iteration 3: (304 enodes) 23.781 * * [simplify]: iteration 4: (1236 enodes) 25.118 * * [simplify]: Extracting #0: cost 15 inf + 0 25.119 * * [simplify]: Extracting #1: cost 356 inf + 0 25.127 * * [simplify]: Extracting #2: cost 1378 inf + 3291 25.140 * * [simplify]: Extracting #3: cost 1980 inf + 14585 25.164 * * [simplify]: Extracting #4: cost 2124 inf + 109596 25.206 * * [simplify]: Extracting #5: cost 1915 inf + 347678 25.341 * * [simplify]: Extracting #6: cost 1068 inf + 1813521 25.750 * * [simplify]: Extracting #7: cost 238 inf + 3718394 26.237 * * [simplify]: Extracting #8: cost 4 inf + 4344981 26.725 * * [simplify]: Extracting #9: cost 0 inf + 4329032 27.278 * [simplify]: Simplified to: (/.p16 (+.p16 a (/.p16 (+.p16 b (+.p16 a c)) (real->posit16 2))) (-.p16 (/.p16 (+.p16 b (+.p16 a c)) (real->posit16 2)) a)) (*.p16 (+.p16 a (/.p16 (+.p16 b (+.p16 a c)) (real->posit16 2))) (+.p16 (*.p16 (/.p16 (+.p16 b (+.p16 a c)) (real->posit16 2)) (/.p16 (+.p16 b (+.p16 a c)) (real->posit16 2))) (*.p16 a a))) (/.p16 (+.p16 c (/.p16 (+.p16 b (+.p16 a c)) (real->posit16 2))) (-.p16 (/.p16 (+.p16 b (+.p16 a c)) (real->posit16 2)) c)) (*.p16 (+.p16 c (/.p16 (+.p16 b (+.p16 a c)) (real->posit16 2))) (+.p16 (*.p16 c c) (*.p16 (/.p16 (+.p16 b (+.p16 a c)) (real->posit16 2)) (/.p16 (+.p16 b (+.p16 a c)) (real->posit16 2))))) (+.p16 a (/.p16 (+.p16 b (+.p16 a c)) (real->posit16 2))) (-.p16 (/.p16 (+.p16 b (+.p16 a c)) (real->posit16 2)) a) (neg.p16 (*.p16 a a)) (*.p16 (+.p16 (*.p16 (/.p16 (+.p16 b (+.p16 a c)) (real->posit16 2)) (/.p16 (+.p16 b (+.p16 a c)) (real->posit16 2))) (*.p16 a a)) (-.p16 (*.p16 (/.p16 (+.p16 b (+.p16 a c)) (real->posit16 2)) (/.p16 (+.p16 b (+.p16 a c)) (real->posit16 2))) (*.p16 a a))) (+.p16 (*.p16 (/.p16 (+.p16 b (+.p16 a c)) (real->posit16 2)) (/.p16 (+.p16 b (+.p16 a c)) (real->posit16 2))) (*.p16 a a)) (+.p16 c (/.p16 (+.p16 b (+.p16 a c)) (real->posit16 2))) (-.p16 (/.p16 (+.p16 b (+.p16 a c)) (real->posit16 2)) c) (neg.p16 (*.p16 c c)) (-.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 c c) (*.p16 (/.p16 (+.p16 b (+.p16 a c)) (real->posit16 2)) (/.p16 (+.p16 b (+.p16 a c)) (real->posit16 2)))) (*.p16 (+.p16 a (/.p16 (+.p16 b (+.p16 a c)) (real->posit16 2))) (-.p16 (/.p16 (+.p16 b (+.p16 a c)) (real->posit16 2)) a)) (+.p16 a (/.p16 (+.p16 b (+.p16 a c)) (real->posit16 2))) (*.p16 (+.p16 a (/.p16 (+.p16 b (+.p16 a c)) (real->posit16 2))) (-.p16 (/.p16 (+.p16 b (+.p16 a c)) (real->posit16 2)) a)) (+.p16 a (/.p16 (+.p16 b (+.p16 a c)) (real->posit16 2))) (*.p16 (+.p16 a (/.p16 (+.p16 b (+.p16 a c)) (real->posit16 2))) (-.p16 (/.p16 (+.p16 b (+.p16 a c)) (real->posit16 2)) a)) (+.p16 a (/.p16 (+.p16 b (+.p16 a c)) (real->posit16 2))) (*.p16 (+.p16 a (/.p16 (+.p16 b (+.p16 a c)) (real->posit16 2))) (-.p16 (/.p16 (+.p16 b (+.p16 a c)) (real->posit16 2)) a)) (+.p16 a (/.p16 (+.p16 b (+.p16 a c)) (real->posit16 2))) 27.285 * * * [progress]: adding candidates to table 28.045 * [progress]: [Phase 3 of 3] Extracting. 28.045 * * [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 a b) c) (real->posit16 2)) c))))> #posit16 2)) (/.p16 (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) a) (/.p16 (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) 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 (+.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 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))))))> #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 (+.p16 (+.p16 a b) c) (real->posit16 2)) c) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) c)) (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) c)))))> #posit16 2)) (/.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 a a) (*.p16 a a))) (*.p16 (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) a) (+.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)) 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 (+.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 (/.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)))))))>) 28.057 * * * [regime-changes]: Trying 3 branch expressions: (c b a) 28.057 * * * * [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 a b) c) (real->posit16 2)) c))))> #posit16 2)) (/.p16 (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) a) (/.p16 (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) 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 (+.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 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))))))> #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 (+.p16 (+.p16 a b) c) (real->posit16 2)) c) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) c)) (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) c)))))> #posit16 2)) (/.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 a a) (*.p16 a a))) (*.p16 (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) a) (+.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)) 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 (+.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 (/.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)))))))>) 28.298 * * * * [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 a b) c) (real->posit16 2)) c))))> #posit16 2)) (/.p16 (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) a) (/.p16 (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) 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 (+.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 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))))))> #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 (+.p16 (+.p16 a b) c) (real->posit16 2)) c) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) c)) (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) c)))))> #posit16 2)) (/.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 a a) (*.p16 a a))) (*.p16 (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) a) (+.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)) 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 (+.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 (/.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)))))))>) 28.535 * * * * [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 a b) c) (real->posit16 2)) c))))> #posit16 2)) (/.p16 (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) a) (/.p16 (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) 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 (+.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 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))))))> #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 (+.p16 (+.p16 a b) c) (real->posit16 2)) c) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) c)) (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) c)))))> #posit16 2)) (/.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 a a) (*.p16 a a))) (*.p16 (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) a) (+.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)) 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 (+.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 (/.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)))))))>) 28.732 * * * [regime]: Found split indices: #