0.002 * [progress]: [Phase 1 of 3] Setting up. 0.002 * * * [progress]: [1/2] Preparing points 0.003 * * * * [points]: Sampling 256 additional inputs, on iter 0 have 0 / 256 0.005 * * * * [points]: Computing exacts on every 16 of 256 points to ramp up precision 0.010 * * * * [points]: Setting MPFR precision to 64 0.013 * * * * [points]: Setting MPFR precision to 320 0.015 * * * * [points]: Computing exacts on every 8 of 256 points to ramp up precision 0.022 * * * * [points]: Setting MPFR precision to 64 0.025 * * * * [points]: Setting MPFR precision to 320 0.034 * * * * [points]: Computing exacts on every 4 of 256 points to ramp up precision 0.042 * * * * [points]: Setting MPFR precision to 64 0.049 * * * * [points]: Setting MPFR precision to 320 0.056 * * * * [points]: Computing exacts on every 2 of 256 points to ramp up precision 0.063 * * * * [points]: Setting MPFR precision to 64 0.074 * * * * [points]: Setting MPFR precision to 320 0.086 * * * * [points]: Computing exacts for 256 points 0.094 * * * * [points]: Setting MPFR precision to 64 0.130 * * * * [points]: Setting MPFR precision to 320 0.164 * * * * [points]: Filtering points with unrepresentable outputs 0.164 * * * * [points]: Sampling 225 additional inputs, on iter 1 have 31 / 256 0.166 * * * * [points]: Computing exacts on every 14 of 225 points to ramp up precision 0.173 * * * * [points]: Setting MPFR precision to 64 0.176 * * * * [points]: Setting MPFR precision to 320 0.178 * * * * [points]: Computing exacts on every 7 of 225 points to ramp up precision 0.185 * * * * [points]: Setting MPFR precision to 64 0.190 * * * * [points]: Setting MPFR precision to 320 0.194 * * * * [points]: Computing exacts on every 3 of 225 points to ramp up precision 0.201 * * * * [points]: Setting MPFR precision to 64 0.208 * * * * [points]: Setting MPFR precision to 320 0.216 * * * * [points]: Computing exacts for 225 points 0.260 * * * * [points]: Setting MPFR precision to 64 0.293 * * * * [points]: Setting MPFR precision to 320 0.323 * * * * [points]: Filtering points with unrepresentable outputs 0.323 * * * * [points]: Sampling 202 additional inputs, on iter 2 have 54 / 256 0.325 * * * * [points]: Computing exacts on every 12 of 202 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 6 of 202 points to ramp up precision 0.344 * * * * [points]: Setting MPFR precision to 64 0.348 * * * * [points]: Setting MPFR precision to 320 0.351 * * * * [points]: Computing exacts on every 3 of 202 points to ramp up precision 0.357 * * * * [points]: Setting MPFR precision to 64 0.363 * * * * [points]: Setting MPFR precision to 320 0.369 * * * * [points]: Computing exacts for 202 points 0.376 * * * * [points]: Setting MPFR precision to 64 0.401 * * * * [points]: Setting MPFR precision to 320 0.428 * * * * [points]: Filtering points with unrepresentable outputs 0.428 * * * * [points]: Sampling 177 additional inputs, on iter 3 have 79 / 256 0.430 * * * * [points]: Computing exacts on every 11 of 177 points to ramp up precision 0.436 * * * * [points]: Setting MPFR precision to 64 0.438 * * * * [points]: Setting MPFR precision to 320 0.440 * * * * [points]: Computing exacts on every 5 of 177 points to ramp up precision 0.476 * * * * [points]: Setting MPFR precision to 64 0.479 * * * * [points]: Setting MPFR precision to 320 0.481 * * * * [points]: Computing exacts on every 2 of 177 points to ramp up precision 0.486 * * * * [points]: Setting MPFR precision to 64 0.490 * * * * [points]: Setting MPFR precision to 320 0.495 * * * * [points]: Computing exacts for 177 points 0.498 * * * * [points]: Setting MPFR precision to 64 0.511 * * * * [points]: Setting MPFR precision to 320 0.523 * * * * [points]: Filtering points with unrepresentable outputs 0.523 * * * * [points]: Sampling 162 additional inputs, on iter 4 have 94 / 256 0.524 * * * * [points]: Computing exacts on every 10 of 162 points to ramp up precision 0.527 * * * * [points]: Setting MPFR precision to 64 0.529 * * * * [points]: Setting MPFR precision to 320 0.530 * * * * [points]: Computing exacts on every 5 of 162 points to ramp up precision 0.534 * * * * [points]: Setting MPFR precision to 64 0.536 * * * * [points]: Setting MPFR precision to 320 0.538 * * * * [points]: Computing exacts on every 2 of 162 points to ramp up precision 0.542 * * * * [points]: Setting MPFR precision to 64 0.548 * * * * [points]: Setting MPFR precision to 320 0.554 * * * * [points]: Computing exacts for 162 points 0.561 * * * * [points]: Setting MPFR precision to 64 0.580 * * * * [points]: Setting MPFR precision to 320 0.631 * * * * [points]: Filtering points with unrepresentable outputs 0.632 * * * * [points]: Sampling 142 additional inputs, on iter 5 have 114 / 256 0.636 * * * * [points]: Computing exacts on every 8 of 142 points to ramp up precision 0.643 * * * * [points]: Setting MPFR precision to 64 0.646 * * * * [points]: Setting MPFR precision to 320 0.648 * * * * [points]: Computing exacts on every 4 of 142 points to ramp up precision 0.655 * * * * [points]: Setting MPFR precision to 64 0.659 * * * * [points]: Setting MPFR precision to 320 0.663 * * * * [points]: Computing exacts on every 2 of 142 points to ramp up precision 0.670 * * * * [points]: Setting MPFR precision to 64 0.677 * * * * [points]: Setting MPFR precision to 320 0.684 * * * * [points]: Computing exacts for 142 points 0.691 * * * * [points]: Setting MPFR precision to 64 0.711 * * * * [points]: Setting MPFR precision to 320 0.730 * * * * [points]: Filtering points with unrepresentable outputs 0.730 * * * * [points]: Sampling 120 additional inputs, on iter 6 have 136 / 256 0.731 * * * * [points]: Computing exacts on every 7 of 120 points to ramp up precision 0.738 * * * * [points]: Setting MPFR precision to 64 0.740 * * * * [points]: Setting MPFR precision to 320 0.742 * * * * [points]: Computing exacts on every 3 of 120 points to ramp up precision 0.749 * * * * [points]: Setting MPFR precision to 64 0.754 * * * * [points]: Setting MPFR precision to 320 0.758 * * * * [points]: Computing exacts for 120 points 0.765 * * * * [points]: Setting MPFR precision to 64 0.780 * * * * [points]: Setting MPFR precision to 320 0.796 * * * * [points]: Filtering points with unrepresentable outputs 0.796 * * * * [points]: Sampling 110 additional inputs, on iter 7 have 146 / 256 0.797 * * * * [points]: Computing exacts on every 6 of 110 points to ramp up precision 0.843 * * * * [points]: Setting MPFR precision to 64 0.846 * * * * [points]: Setting MPFR precision to 320 0.851 * * * * [points]: Computing exacts on every 3 of 110 points to ramp up precision 0.858 * * * * [points]: Setting MPFR precision to 64 0.862 * * * * [points]: Setting MPFR precision to 320 0.865 * * * * [points]: Computing exacts for 110 points 0.872 * * * * [points]: Setting MPFR precision to 64 0.887 * * * * [points]: Setting MPFR precision to 320 0.902 * * * * [points]: Filtering points with unrepresentable outputs 0.902 * * * * [points]: Sampling 92 additional inputs, on iter 8 have 164 / 256 0.903 * * * * [points]: Computing exacts on every 5 of 92 points to ramp up precision 0.910 * * * * [points]: Setting MPFR precision to 64 0.912 * * * * [points]: Setting MPFR precision to 320 0.915 * * * * [points]: Computing exacts on every 2 of 92 points to ramp up precision 0.921 * * * * [points]: Setting MPFR precision to 64 0.925 * * * * [points]: Setting MPFR precision to 320 0.930 * * * * [points]: Computing exacts for 92 points 0.937 * * * * [points]: Setting MPFR precision to 64 0.950 * * * * [points]: Setting MPFR precision to 320 0.963 * * * * [points]: Filtering points with unrepresentable outputs 0.963 * * * * [points]: Sampling 75 additional inputs, on iter 9 have 181 / 256 0.964 * * * * [points]: Computing exacts on every 4 of 75 points to ramp up precision 0.971 * * * * [points]: Setting MPFR precision to 64 0.973 * * * * [points]: Setting MPFR precision to 320 0.975 * * * * [points]: Computing exacts on every 2 of 75 points to ramp up precision 0.982 * * * * [points]: Setting MPFR precision to 64 0.986 * * * * [points]: Setting MPFR precision to 320 0.989 * * * * [points]: Computing exacts for 75 points 0.996 * * * * [points]: Setting MPFR precision to 64 1.005 * * * * [points]: Setting MPFR precision to 320 1.049 * * * * [points]: Filtering points with unrepresentable outputs 1.049 * * * * [points]: Sampling 67 additional inputs, on iter 10 have 189 / 256 1.050 * * * * [points]: Computing exacts on every 4 of 67 points to ramp up precision 1.060 * * * * [points]: Setting MPFR precision to 64 1.062 * * * * [points]: Setting MPFR precision to 320 1.064 * * * * [points]: Computing exacts on every 2 of 67 points to ramp up precision 1.072 * * * * [points]: Setting MPFR precision to 64 1.075 * * * * [points]: Setting MPFR precision to 320 1.078 * * * * [points]: Computing exacts for 67 points 1.085 * * * * [points]: Setting MPFR precision to 64 1.095 * * * * [points]: Setting MPFR precision to 320 1.104 * * * * [points]: Filtering points with unrepresentable outputs 1.104 * * * * [points]: Sampling 53 additional inputs, on iter 11 have 203 / 256 1.104 * * * * [points]: Computing exacts on every 3 of 53 points to ramp up precision 1.111 * * * * [points]: Setting MPFR precision to 64 1.113 * * * * [points]: Setting MPFR precision to 320 1.115 * * * * [points]: Computing exacts for 53 points 1.122 * * * * [points]: Setting MPFR precision to 64 1.129 * * * * [points]: Setting MPFR precision to 320 1.136 * * * * [points]: Filtering points with unrepresentable outputs 1.136 * * * * [points]: Sampling 47 additional inputs, on iter 12 have 209 / 256 1.137 * * * * [points]: Computing exacts on every 2 of 47 points to ramp up precision 1.143 * * * * [points]: Setting MPFR precision to 64 1.146 * * * * [points]: Setting MPFR precision to 320 1.148 * * * * [points]: Computing exacts for 47 points 1.155 * * * * [points]: Setting MPFR precision to 64 1.161 * * * * [points]: Setting MPFR precision to 320 1.167 * * * * [points]: Filtering points with unrepresentable outputs 1.167 * * * * [points]: Sampling 43 additional inputs, on iter 13 have 213 / 256 1.168 * * * * [points]: Computing exacts on every 2 of 43 points to ramp up precision 1.175 * * * * [points]: Setting MPFR precision to 64 1.177 * * * * [points]: Setting MPFR precision to 320 1.179 * * * * [points]: Computing exacts for 43 points 1.186 * * * * [points]: Setting MPFR precision to 64 1.191 * * * * [points]: Setting MPFR precision to 320 1.197 * * * * [points]: Filtering points with unrepresentable outputs 1.197 * * * * [points]: Sampling 36 additional inputs, on iter 14 have 220 / 256 1.198 * * * * [points]: Computing exacts on every 2 of 36 points to ramp up precision 1.205 * * * * [points]: Setting MPFR precision to 64 1.207 * * * * [points]: Setting MPFR precision to 320 1.208 * * * * [points]: Computing exacts for 36 points 1.245 * * * * [points]: Setting MPFR precision to 64 1.250 * * * * [points]: Setting MPFR precision to 320 1.258 * * * * [points]: Filtering points with unrepresentable outputs 1.258 * * * * [points]: Sampling 34 additional inputs, on iter 15 have 222 / 256 1.258 * * * * [points]: Computing exacts on every 2 of 34 points to ramp up precision 1.265 * * * * [points]: Setting MPFR precision to 64 1.267 * * * * [points]: Setting MPFR precision to 320 1.268 * * * * [points]: Computing exacts for 34 points 1.275 * * * * [points]: Setting MPFR precision to 64 1.280 * * * * [points]: Setting MPFR precision to 320 1.285 * * * * [points]: Filtering points with unrepresentable outputs 1.285 * * * * [points]: Sampling 28 additional inputs, on iter 16 have 228 / 256 1.285 * * * * [points]: Computing exacts for 28 points 1.292 * * * * [points]: Setting MPFR precision to 64 1.296 * * * * [points]: Setting MPFR precision to 320 1.300 * * * * [points]: Filtering points with unrepresentable outputs 1.300 * * * * [points]: Sampling 25 additional inputs, on iter 17 have 231 / 256 1.300 * * * * [points]: Computing exacts for 25 points 1.308 * * * * [points]: Setting MPFR precision to 64 1.311 * * * * [points]: Setting MPFR precision to 320 1.315 * * * * [points]: Filtering points with unrepresentable outputs 1.315 * * * * [points]: Sampling 23 additional inputs, on iter 18 have 233 / 256 1.315 * * * * [points]: Computing exacts for 23 points 1.318 * * * * [points]: Setting MPFR precision to 64 1.320 * * * * [points]: Setting MPFR precision to 320 1.322 * * * * [points]: Filtering points with unrepresentable outputs 1.322 * * * * [points]: Sampling 22 additional inputs, on iter 19 have 234 / 256 1.322 * * * * [points]: Computing exacts for 22 points 1.326 * * * * [points]: Setting MPFR precision to 64 1.328 * * * * [points]: Setting MPFR precision to 320 1.330 * * * * [points]: Filtering points with unrepresentable outputs 1.330 * * * * [points]: Sampling 19 additional inputs, on iter 20 have 237 / 256 1.330 * * * * [points]: Computing exacts for 19 points 1.333 * * * * [points]: Setting MPFR precision to 64 1.335 * * * * [points]: Setting MPFR precision to 320 1.336 * * * * [points]: Filtering points with unrepresentable outputs 1.336 * * * * [points]: Sampling 16 additional inputs, on iter 21 have 240 / 256 1.336 * * * * [points]: Computing exacts for 16 points 1.340 * * * * [points]: Setting MPFR precision to 64 1.341 * * * * [points]: Setting MPFR precision to 320 1.342 * * * * [points]: Filtering points with unrepresentable outputs 1.342 * * * * [points]: Sampling 16 additional inputs, on iter 22 have 240 / 256 1.342 * * * * [points]: Computing exacts for 16 points 1.346 * * * * [points]: Setting MPFR precision to 64 1.347 * * * * [points]: Setting MPFR precision to 320 1.348 * * * * [points]: Filtering points with unrepresentable outputs 1.348 * * * * [points]: Sampling 14 additional inputs, on iter 23 have 242 / 256 1.348 * * * * [points]: Computing exacts for 14 points 1.352 * * * * [points]: Setting MPFR precision to 64 1.353 * * * * [points]: Setting MPFR precision to 320 1.354 * * * * [points]: Filtering points with unrepresentable outputs 1.354 * * * * [points]: Sampling 13 additional inputs, on iter 24 have 243 / 256 1.354 * * * * [points]: Computing exacts for 13 points 1.358 * * * * [points]: Setting MPFR precision to 64 1.359 * * * * [points]: Setting MPFR precision to 320 1.360 * * * * [points]: Filtering points with unrepresentable outputs 1.360 * * * * [points]: Sampling 10 additional inputs, on iter 25 have 246 / 256 1.360 * * * * [points]: Computing exacts for 10 points 1.378 * * * * [points]: Setting MPFR precision to 64 1.379 * * * * [points]: Setting MPFR precision to 320 1.380 * * * * [points]: Filtering points with unrepresentable outputs 1.380 * * * * [points]: Sampling 10 additional inputs, on iter 26 have 246 / 256 1.380 * * * * [points]: Computing exacts for 10 points 1.384 * * * * [points]: Setting MPFR precision to 64 1.385 * * * * [points]: Setting MPFR precision to 320 1.388 * * * * [points]: Filtering points with unrepresentable outputs 1.388 * * * * [points]: Sampling 10 additional inputs, on iter 27 have 246 / 256 1.388 * * * * [points]: Computing exacts for 10 points 1.392 * * * * [points]: Setting MPFR precision to 64 1.392 * * * * [points]: Setting MPFR precision to 320 1.393 * * * * [points]: Filtering points with unrepresentable outputs 1.393 * * * * [points]: Sampling 9 additional inputs, on iter 28 have 247 / 256 1.393 * * * * [points]: Computing exacts for 9 points 1.398 * * * * [points]: Setting MPFR precision to 64 1.399 * * * * [points]: Setting MPFR precision to 320 1.399 * * * * [points]: Filtering points with unrepresentable outputs 1.399 * * * * [points]: Sampling 7 additional inputs, on iter 29 have 249 / 256 1.399 * * * * [points]: Computing exacts for 7 points 1.403 * * * * [points]: Setting MPFR precision to 64 1.404 * * * * [points]: Setting MPFR precision to 320 1.405 * * * * [points]: Filtering points with unrepresentable outputs 1.405 * * * * [points]: Sampling 7 additional inputs, on iter 30 have 249 / 256 1.405 * * * * [points]: Computing exacts for 7 points 1.412 * * * * [points]: Setting MPFR precision to 64 1.413 * * * * [points]: Setting MPFR precision to 320 1.414 * * * * [points]: Filtering points with unrepresentable outputs 1.414 * * * * [points]: Sampling 6 additional inputs, on iter 31 have 250 / 256 1.414 * * * * [points]: Computing exacts for 6 points 1.421 * * * * [points]: Setting MPFR precision to 64 1.422 * * * * [points]: Setting MPFR precision to 320 1.423 * * * * [points]: Filtering points with unrepresentable outputs 1.423 * * * * [points]: Sampling 4 additional inputs, on iter 32 have 252 / 256 1.423 * * * * [points]: Computing exacts for 4 points 1.426 * * * * [points]: Setting MPFR precision to 64 1.427 * * * * [points]: Setting MPFR precision to 320 1.427 * * * * [points]: Filtering points with unrepresentable outputs 1.427 * * * * [points]: Sampling 4 additional inputs, on iter 33 have 252 / 256 1.427 * * * * [points]: Computing exacts for 4 points 1.431 * * * * [points]: Setting MPFR precision to 64 1.431 * * * * [points]: Setting MPFR precision to 320 1.431 * * * * [points]: Filtering points with unrepresentable outputs 1.431 * * * * [points]: Sampling 4 additional inputs, on iter 34 have 252 / 256 1.431 * * * * [points]: Computing exacts for 4 points 1.435 * * * * [points]: Setting MPFR precision to 64 1.435 * * * * [points]: Setting MPFR precision to 320 1.436 * * * * [points]: Filtering points with unrepresentable outputs 1.436 * * * * [points]: Sampling 4 additional inputs, on iter 35 have 253 / 256 1.436 * * * * [points]: Computing exacts for 4 points 1.439 * * * * [points]: Setting MPFR precision to 64 1.440 * * * * [points]: Setting MPFR precision to 320 1.440 * * * * [points]: Filtering points with unrepresentable outputs 1.440 * * * * [points]: Sampling 4 additional inputs, on iter 36 have 253 / 256 1.440 * * * * [points]: Computing exacts for 4 points 1.444 * * * * [points]: Setting MPFR precision to 64 1.444 * * * * [points]: Setting MPFR precision to 320 1.444 * * * * [points]: Filtering points with unrepresentable outputs 1.444 * * * * [points]: Sampling 4 additional inputs, on iter 37 have 253 / 256 1.444 * * * * [points]: Computing exacts for 4 points 1.448 * * * * [points]: Setting MPFR precision to 64 1.448 * * * * [points]: Setting MPFR precision to 320 1.449 * * * * [points]: Filtering points with unrepresentable outputs 1.449 * * * * [points]: Sampling 4 additional inputs, on iter 38 have 253 / 256 1.449 * * * * [points]: Computing exacts for 4 points 1.452 * * * * [points]: Setting MPFR precision to 64 1.453 * * * * [points]: Setting MPFR precision to 320 1.453 * * * * [points]: Filtering points with unrepresentable outputs 1.453 * * * * [points]: Sampling 4 additional inputs, on iter 39 have 253 / 256 1.453 * * * * [points]: Computing exacts for 4 points 1.467 * * * * [points]: Setting MPFR precision to 64 1.468 * * * * [points]: Setting MPFR precision to 320 1.468 * * * * [points]: Filtering points with unrepresentable outputs 1.468 * * * * [points]: Sampling 4 additional inputs, on iter 40 have 253 / 256 1.468 * * * * [points]: Computing exacts for 4 points 1.472 * * * * [points]: Setting MPFR precision to 64 1.472 * * * * [points]: Setting MPFR precision to 320 1.473 * * * * [points]: Filtering points with unrepresentable outputs 1.473 * * * * [points]: Sampling 4 additional inputs, on iter 41 have 253 / 256 1.473 * * * * [points]: Computing exacts for 4 points 1.478 * * * * [points]: Setting MPFR precision to 64 1.479 * * * * [points]: Setting MPFR precision to 320 1.479 * * * * [points]: Filtering points with unrepresentable outputs 1.479 * * * * [points]: Sampling 4 additional inputs, on iter 42 have 254 / 256 1.480 * * * * [points]: Computing exacts for 4 points 1.486 * * * * [points]: Setting MPFR precision to 64 1.487 * * * * [points]: Setting MPFR precision to 320 1.487 * * * * [points]: Filtering points with unrepresentable outputs 1.487 * * * * [points]: Sampling 4 additional inputs, on iter 43 have 255 / 256 1.488 * * * * [points]: Computing exacts for 4 points 1.491 * * * * [points]: Setting MPFR precision to 64 1.491 * * * * [points]: Setting MPFR precision to 320 1.492 * * * * [points]: Filtering points with unrepresentable outputs 1.492 * * * * [points]: Sampling 4 additional inputs, on iter 44 have 255 / 256 1.492 * * * * [points]: Computing exacts for 4 points 1.499 * * * * [points]: Setting MPFR precision to 64 1.500 * * * * [points]: Setting MPFR precision to 320 1.500 * * * * [points]: Filtering points with unrepresentable outputs 1.501 * * * * [points]: Sampling 4 additional inputs, on iter 45 have 255 / 256 1.501 * * * * [points]: Computing exacts for 4 points 1.507 * * * * [points]: Setting MPFR precision to 64 1.508 * * * * [points]: Setting MPFR precision to 320 1.508 * * * * [points]: Filtering points with unrepresentable outputs 1.509 * * * * [points]: Sampled 256 points with exact outputs 1.509 * * * [progress]: [2/2] Setting up program. 1.526 * [progress]: [Phase 2 of 3] Improving. 1.526 * * * * [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.526 * [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.527 * * [simplify]: iters left: 6 (15 enodes) 1.534 * * [simplify]: iters left: 5 (54 enodes) 1.555 * * [simplify]: iters left: 4 (174 enodes) 1.651 * * [simplify]: Extracting #0: cost 1 inf + 0 1.651 * * [simplify]: Extracting #1: cost 2 inf + 0 1.651 * * [simplify]: Extracting #2: cost 52 inf + 0 1.652 * * [simplify]: Extracting #3: cost 218 inf + 0 1.653 * * [simplify]: Extracting #4: cost 350 inf + 488 1.658 * * [simplify]: Extracting #5: cost 271 inf + 83278 1.676 * * [simplify]: Extracting #6: cost 99 inf + 301152 1.701 * * [simplify]: Extracting #7: cost 13 inf + 445414 1.729 * * [simplify]: Extracting #8: cost 0 inf + 471346 1.780 * [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.780 * [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.805 * * [progress]: iteration 1 / 4 1.805 * * * [progress]: picking best candidate 1.826 * * * * [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.826 * * * [progress]: localizing error 2.242 * * * [progress]: generating rewritten candidates 2.242 * * * * [progress]: [ 1 / 4 ] rewriting at (2 1 1 2) 2.297 * * * * [progress]: [ 2 / 4 ] rewriting at (2 1 1 1 2) 2.344 * * * * [progress]: [ 3 / 4 ] rewriting at (2 1 2) 2.390 * * * * [progress]: [ 4 / 4 ] rewriting at (2 1 2 1) 2.414 * * * [progress]: generating series expansions 2.414 * * * * [progress]: [ 1 / 4 ] generating series at (2 1 1 2) 2.415 * * * * [progress]: [ 2 / 4 ] generating series at (2 1 1 1 2) 2.415 * * * * [progress]: [ 3 / 4 ] generating series at (2 1 2) 2.415 * * * * [progress]: [ 4 / 4 ] generating series at (2 1 2 1) 2.415 * * * [progress]: simplifying candidates 2.415 * * * * [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)) (neg.p16 b))) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) c))))> 2.415 * * * * [progress]: [ 2 / 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))))> 2.415 * * * * [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))))> 2.415 * * * * [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))))> 2.415 * * * * [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)) b)) (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (neg.p16 c)))))> 2.415 * * * * [progress]: [ 6 / 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)))))> 2.415 * * * * [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))))> 2.416 * [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.416 * * [simplify]: iters left: 6 (15 enodes) 2.423 * * [simplify]: iters left: 5 (54 enodes) 2.445 * * [simplify]: iters left: 4 (174 enodes) 2.586 * * [simplify]: Extracting #0: cost 1 inf + 0 2.586 * * [simplify]: Extracting #1: cost 2 inf + 0 2.586 * * [simplify]: Extracting #2: cost 52 inf + 0 2.586 * * [simplify]: Extracting #3: cost 218 inf + 0 2.587 * * [simplify]: Extracting #4: cost 350 inf + 488 2.592 * * [simplify]: Extracting #5: cost 271 inf + 83278 2.606 * * [simplify]: Extracting #6: cost 99 inf + 301152 2.634 * * [simplify]: Extracting #7: cost 13 inf + 445414 2.662 * * [simplify]: Extracting #8: cost 0 inf + 471346 2.690 * [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.690 * [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.690 * * * * [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.691 * [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.691 * * [simplify]: iters left: 6 (15 enodes) 2.694 * * [simplify]: iters left: 5 (54 enodes) 2.705 * * [simplify]: iters left: 4 (174 enodes) 2.776 * * [simplify]: Extracting #0: cost 1 inf + 0 2.776 * * [simplify]: Extracting #1: cost 2 inf + 0 2.776 * * [simplify]: Extracting #2: cost 52 inf + 0 2.777 * * [simplify]: Extracting #3: cost 218 inf + 0 2.778 * * [simplify]: Extracting #4: cost 350 inf + 488 2.786 * * [simplify]: Extracting #5: cost 271 inf + 83278 2.800 * * [simplify]: Extracting #6: cost 99 inf + 301152 2.825 * * [simplify]: Extracting #7: cost 13 inf + 445414 2.853 * * [simplify]: Extracting #8: cost 0 inf + 471346 2.882 * [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.882 * [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.882 * * * * [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.882 * [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.883 * * [simplify]: iters left: 6 (15 enodes) 2.887 * * [simplify]: iters left: 5 (54 enodes) 2.899 * * [simplify]: iters left: 4 (174 enodes) 2.972 * * [simplify]: Extracting #0: cost 1 inf + 0 2.972 * * [simplify]: Extracting #1: cost 2 inf + 0 2.972 * * [simplify]: Extracting #2: cost 52 inf + 0 2.972 * * [simplify]: Extracting #3: cost 218 inf + 0 2.973 * * [simplify]: Extracting #4: cost 350 inf + 488 2.978 * * [simplify]: Extracting #5: cost 271 inf + 83278 2.993 * * [simplify]: Extracting #6: cost 99 inf + 301152 3.018 * * [simplify]: Extracting #7: cost 13 inf + 445414 3.074 * * [simplify]: Extracting #8: cost 0 inf + 471346 3.129 * [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))) 3.130 * [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)))) 3.130 * * * * [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))))> 3.130 * [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))) 3.130 * * [simplify]: iters left: 6 (15 enodes) 3.136 * * [simplify]: iters left: 5 (54 enodes) 3.147 * * [simplify]: iters left: 4 (174 enodes) 3.264 * * [simplify]: Extracting #0: cost 1 inf + 0 3.265 * * [simplify]: Extracting #1: cost 2 inf + 0 3.265 * * [simplify]: Extracting #2: cost 52 inf + 0 3.266 * * [simplify]: Extracting #3: cost 218 inf + 0 3.268 * * [simplify]: Extracting #4: cost 350 inf + 488 3.276 * * [simplify]: Extracting #5: cost 271 inf + 83278 3.295 * * [simplify]: Extracting #6: cost 99 inf + 301152 3.321 * * [simplify]: Extracting #7: cost 13 inf + 445414 3.349 * * [simplify]: Extracting #8: cost 0 inf + 471346 3.379 * [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))) 3.379 * [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)))) 3.379 * * * [progress]: adding candidates to table 3.689 * * [progress]: iteration 2 / 4 3.689 * * * [progress]: picking best candidate 3.744 * * * * [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 a b) c) (real->posit16 2)) c))))> 3.744 * * * [progress]: localizing error 4.128 * * * [progress]: generating rewritten candidates 4.129 * * * * [progress]: [ 1 / 4 ] rewriting at (2 1 1 1 2) 4.222 * * * * [progress]: [ 2 / 4 ] rewriting at (2 1 1 2) 4.271 * * * * [progress]: [ 3 / 4 ] rewriting at (2 1 1 1 2 1) 4.277 * * * * [progress]: [ 4 / 4 ] rewriting at (2 1 2) 4.324 * * * [progress]: generating series expansions 4.324 * * * * [progress]: [ 1 / 4 ] generating series at (2 1 1 1 2) 4.324 * * * * [progress]: [ 2 / 4 ] generating series at (2 1 1 2) 4.324 * * * * [progress]: [ 3 / 4 ] generating series at (2 1 1 1 2 1) 4.324 * * * * [progress]: [ 4 / 4 ] generating series at (2 1 2) 4.324 * * * [progress]: simplifying candidates 4.324 * * * * [progress]: [ 1 / 13 ] 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 a b) c) (real->posit16 2)) c))))> 4.324 * [simplify]: Simplifying (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) a) 4.325 * * [simplify]: iters left: 4 (9 enodes) 4.329 * * [simplify]: iters left: 3 (21 enodes) 4.335 * * [simplify]: iters left: 2 (27 enodes) 4.343 * * [simplify]: iters left: 1 (28 enodes) 4.351 * * [simplify]: Extracting #0: cost 1 inf + 0 4.351 * * [simplify]: Extracting #1: cost 3 inf + 0 4.351 * * [simplify]: Extracting #2: cost 4 inf + 1 4.351 * * [simplify]: Extracting #3: cost 10 inf + 1 4.351 * * [simplify]: Extracting #4: cost 1 inf + 738 4.351 * * [simplify]: Extracting #5: cost 0 inf + 1302 4.352 * [simplify]: Simplified to (+.p16 a (/.p16 (+.p16 (+.p16 b a) c) (real->posit16 2))) 4.352 * [simplify]: Simplified (2 1 1 1 2 1) to (λ (a b c) (sqrt.p16 (*.p16 (*.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (/.p16 (+.p16 a (/.p16 (+.p16 (+.p16 b a) c) (real->posit16 2))) (/.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 a b) c) (real->posit16 2)) c)))) 4.352 * * * * [progress]: [ 2 / 13 ] 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 a b) c) (real->posit16 2)) c))))> 4.353 * [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 a a) (*.p16 a a))) 4.353 * * [simplify]: iters left: 6 (13 enodes) 4.359 * * [simplify]: iters left: 5 (46 enodes) 4.378 * * [simplify]: iters left: 4 (130 enodes) 4.441 * * [simplify]: Extracting #0: cost 1 inf + 0 4.441 * * [simplify]: Extracting #1: cost 25 inf + 0 4.441 * * [simplify]: Extracting #2: cost 62 inf + 0 4.441 * * [simplify]: Extracting #3: cost 154 inf + 82 4.442 * * [simplify]: Extracting #4: cost 156 inf + 19005 4.449 * * [simplify]: Extracting #5: cost 37 inf + 171376 4.465 * * [simplify]: Extracting #6: cost 3 inf + 231747 4.481 * * [simplify]: Extracting #7: cost 0 inf + 241279 4.494 * [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 (/.p16 (+.p16 (+.p16 b a) c) (real->posit16 2)) (/.p16 (+.p16 (+.p16 b a) c) (real->posit16 2)))) (*.p16 (*.p16 a a) (*.p16 a a))) 4.494 * [simplify]: Simplified (2 1 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 (/.p16 (+.p16 (+.p16 b a) c) (real->posit16 2)) (/.p16 (+.p16 (+.p16 b a) c) (real->posit16 2))) (*.p16 (/.p16 (+.p16 (+.p16 b a) c) (real->posit16 2)) (/.p16 (+.p16 (+.p16 b a) 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 a b) c) (real->posit16 2)) c)))) 4.494 * * * * [progress]: [ 3 / 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)) (neg.p16 b))) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) c))))> 4.494 * * * * [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 (+.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.494 * * * * [progress]: [ 5 / 13 ] 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 a b) c) (real->posit16 2)) c))))> 4.494 * [simplify]: Simplifying (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) a) 4.494 * * [simplify]: iters left: 4 (9 enodes) 4.496 * * [simplify]: iters left: 3 (21 enodes) 4.499 * * [simplify]: iters left: 2 (27 enodes) 4.503 * * [simplify]: iters left: 1 (28 enodes) 4.507 * * [simplify]: Extracting #0: cost 1 inf + 0 4.507 * * [simplify]: Extracting #1: cost 3 inf + 0 4.507 * * [simplify]: Extracting #2: cost 4 inf + 1 4.507 * * [simplify]: Extracting #3: cost 10 inf + 1 4.507 * * [simplify]: Extracting #4: cost 1 inf + 738 4.507 * * [simplify]: Extracting #5: cost 0 inf + 1302 4.507 * [simplify]: Simplified to (+.p16 a (/.p16 (+.p16 (+.p16 b a) c) (real->posit16 2))) 4.507 * [simplify]: Simplified (2 1 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 a (/.p16 (+.p16 (+.p16 b a) 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)) a))) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) b)) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) c)))) 4.508 * [simplify]: Simplifying (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) a) 4.508 * * [simplify]: iters left: 4 (9 enodes) 4.510 * * [simplify]: iters left: 3 (27 enodes) 4.514 * * [simplify]: iters left: 2 (47 enodes) 4.525 * * [simplify]: iters left: 1 (123 enodes) 4.555 * * [simplify]: Extracting #0: cost 1 inf + 0 4.555 * * [simplify]: Extracting #1: cost 15 inf + 0 4.555 * * [simplify]: Extracting #2: cost 53 inf + 1 4.556 * * [simplify]: Extracting #3: cost 87 inf + 1044 4.556 * * [simplify]: Extracting #4: cost 139 inf + 5657 4.557 * * [simplify]: Extracting #5: cost 115 inf + 19521 4.561 * * [simplify]: Extracting #6: cost 57 inf + 79064 4.569 * * [simplify]: Extracting #7: cost 8 inf + 157140 4.582 * * [simplify]: Extracting #8: cost 0 inf + 176132 4.601 * [simplify]: Simplified to (-.p16 (/.p16 (+.p16 b (+.p16 a c)) (real->posit16 2)) a) 4.601 * [simplify]: Simplified (2 1 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 (+.p16 (+.p16 a b) c) (real->posit16 2)) a) (-.p16 (/.p16 (+.p16 b (+.p16 a 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 a b) c) (real->posit16 2)) c)))) 4.601 * * * * [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))) (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 a b) c) (real->posit16 2)) c))))> 4.601 * * * * [progress]: [ 7 / 13 ] 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 a b) c) (real->posit16 2)) c))))> 4.601 * * * * [progress]: [ 8 / 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 a b) c) (real->posit16 2)) (neg.p16 c)))))> 4.601 * * * * [progress]: [ 9 / 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)))))> 4.602 * * * * [progress]: [ 10 / 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 a b) c) (real->posit16 2)) c))))> 4.602 * * * * [progress]: [ 11 / 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 a b) c) (real->posit16 2)) c))))> 4.602 * * * * [progress]: [ 12 / 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 a b) c) (real->posit16 2)) c))))> 4.602 * * * * [progress]: [ 13 / 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 a b) c) (real->posit16 2)) c))))> 4.602 * * * [progress]: adding candidates to table 5.022 * * [progress]: iteration 3 / 4 5.023 * * * [progress]: picking best candidate 5.066 * * * * [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 (+.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))))> 5.066 * * * [progress]: localizing error 5.649 * * * [progress]: generating rewritten candidates 5.649 * * * * [progress]: [ 1 / 4 ] rewriting at (2 1 1 1 2) 5.749 * * * * [progress]: [ 2 / 4 ] rewriting at (2 1 1 2) 5.869 * * * * [progress]: [ 3 / 4 ] rewriting at (2 1 1 2 1) 5.875 * * * * [progress]: [ 4 / 4 ] rewriting at (2 1 1 1 2 1) 5.881 * * * [progress]: generating series expansions 5.881 * * * * [progress]: [ 1 / 4 ] generating series at (2 1 1 1 2) 5.881 * * * * [progress]: [ 2 / 4 ] generating series at (2 1 1 2) 5.881 * * * * [progress]: [ 3 / 4 ] generating series at (2 1 1 2 1) 5.881 * * * * [progress]: [ 4 / 4 ] generating series at (2 1 1 1 2 1) 5.881 * * * [progress]: simplifying candidates 5.881 * * * * [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 (+.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))))> 5.882 * [simplify]: Simplifying (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) a) 5.882 * * [simplify]: iters left: 4 (9 enodes) 5.886 * * [simplify]: iters left: 3 (21 enodes) 5.893 * * [simplify]: iters left: 2 (27 enodes) 5.903 * * [simplify]: iters left: 1 (28 enodes) 5.911 * * [simplify]: Extracting #0: cost 1 inf + 0 5.911 * * [simplify]: Extracting #1: cost 3 inf + 0 5.911 * * [simplify]: Extracting #2: cost 4 inf + 1 5.911 * * [simplify]: Extracting #3: cost 10 inf + 1 5.911 * * [simplify]: Extracting #4: cost 1 inf + 738 5.912 * * [simplify]: Extracting #5: cost 0 inf + 1302 5.912 * [simplify]: Simplified to (+.p16 a (/.p16 (+.p16 (+.p16 b a) c) (real->posit16 2))) 5.912 * [simplify]: Simplified (2 1 1 1 2 1) to (λ (a b c) (sqrt.p16 (*.p16 (*.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (/.p16 (+.p16 a (/.p16 (+.p16 (+.p16 b a) c) (real->posit16 2))) (/.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 (+.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)))) 5.912 * * * * [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 (+.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))))> 5.913 * [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 a a) (*.p16 a a))) 5.913 * * [simplify]: iters left: 6 (13 enodes) 5.920 * * [simplify]: iters left: 5 (46 enodes) 5.940 * * [simplify]: iters left: 4 (130 enodes) 5.997 * * [simplify]: Extracting #0: cost 1 inf + 0 5.997 * * [simplify]: Extracting #1: cost 25 inf + 0 5.997 * * [simplify]: Extracting #2: cost 62 inf + 0 5.998 * * [simplify]: Extracting #3: cost 154 inf + 82 6.000 * * [simplify]: Extracting #4: cost 156 inf + 19005 6.012 * * [simplify]: Extracting #5: cost 37 inf + 171376 6.033 * * [simplify]: Extracting #6: cost 3 inf + 231747 6.055 * * [simplify]: Extracting #7: cost 0 inf + 241279 6.069 * [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 (/.p16 (+.p16 (+.p16 b a) c) (real->posit16 2)) (/.p16 (+.p16 (+.p16 b a) c) (real->posit16 2)))) (*.p16 (*.p16 a a) (*.p16 a a))) 6.069 * [simplify]: Simplified (2 1 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 (/.p16 (+.p16 (+.p16 b a) c) (real->posit16 2)) (/.p16 (+.p16 (+.p16 b a) c) (real->posit16 2))) (*.p16 (/.p16 (+.p16 (+.p16 b a) c) (real->posit16 2)) (/.p16 (+.p16 (+.p16 b a) 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 (+.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)))) 6.069 * * * * [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 (+.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))))> 6.070 * [simplify]: Simplifying (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) b) 6.070 * * [simplify]: iters left: 4 (9 enodes) 6.072 * * [simplify]: iters left: 3 (21 enodes) 6.075 * * [simplify]: iters left: 2 (27 enodes) 6.079 * * [simplify]: iters left: 1 (28 enodes) 6.083 * * [simplify]: Extracting #0: cost 1 inf + 0 6.083 * * [simplify]: Extracting #1: cost 3 inf + 0 6.083 * * [simplify]: Extracting #2: cost 4 inf + 1 6.083 * * [simplify]: Extracting #3: cost 10 inf + 1 6.083 * * [simplify]: Extracting #4: cost 5 inf + 47 6.083 * * [simplify]: Extracting #5: cost 1 inf + 738 6.083 * * [simplify]: Extracting #6: cost 0 inf + 1302 6.084 * [simplify]: Simplified to (+.p16 (/.p16 (+.p16 a (+.p16 c b)) (real->posit16 2)) b) 6.084 * [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 (+.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 (+.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)))) 6.084 * * * * [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 (/.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.084 * [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.084 * * [simplify]: iters left: 6 (13 enodes) 6.087 * * [simplify]: iters left: 5 (46 enodes) 6.096 * * [simplify]: iters left: 4 (130 enodes) 6.134 * * [simplify]: Extracting #0: cost 1 inf + 0 6.134 * * [simplify]: Extracting #1: cost 25 inf + 0 6.134 * * [simplify]: Extracting #2: cost 62 inf + 0 6.134 * * [simplify]: Extracting #3: cost 156 inf + 1 6.136 * * [simplify]: Extracting #4: cost 157 inf + 19646 6.141 * * [simplify]: Extracting #5: cost 52 inf + 148242 6.153 * * [simplify]: Extracting #6: cost 1 inf + 239837 6.170 * * [simplify]: Extracting #7: cost 0 inf + 242361 6.195 * [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.195 * [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 (+.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 (+.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)))) 6.195 * * * * [progress]: [ 5 / 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 (+.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))))> 6.196 * [simplify]: Simplifying (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) b) 6.196 * * [simplify]: iters left: 4 (9 enodes) 6.200 * * [simplify]: iters left: 3 (21 enodes) 6.207 * * [simplify]: iters left: 2 (27 enodes) 6.211 * * [simplify]: iters left: 1 (28 enodes) 6.214 * * [simplify]: Extracting #0: cost 1 inf + 0 6.214 * * [simplify]: Extracting #1: cost 3 inf + 0 6.214 * * [simplify]: Extracting #2: cost 4 inf + 1 6.215 * * [simplify]: Extracting #3: cost 10 inf + 1 6.215 * * [simplify]: Extracting #4: cost 5 inf + 47 6.215 * * [simplify]: Extracting #5: cost 1 inf + 738 6.215 * * [simplify]: Extracting #6: cost 0 inf + 1302 6.215 * [simplify]: Simplified to (+.p16 (/.p16 (+.p16 a (+.p16 c b)) (real->posit16 2)) b) 6.215 * [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 (+.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 (+.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)))) 6.215 * [simplify]: Simplifying (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) b) 6.215 * * [simplify]: iters left: 4 (9 enodes) 6.218 * * [simplify]: iters left: 3 (27 enodes) 6.222 * * [simplify]: iters left: 2 (47 enodes) 6.231 * * [simplify]: iters left: 1 (123 enodes) 6.264 * * [simplify]: Extracting #0: cost 1 inf + 0 6.264 * * [simplify]: Extracting #1: cost 15 inf + 0 6.264 * * [simplify]: Extracting #2: cost 52 inf + 82 6.264 * * [simplify]: Extracting #3: cost 87 inf + 1044 6.265 * * [simplify]: Extracting #4: cost 140 inf + 5615 6.266 * * [simplify]: Extracting #5: cost 118 inf + 19352 6.270 * * [simplify]: Extracting #6: cost 58 inf + 77580 6.278 * * [simplify]: Extracting #7: cost 8 inf + 157140 6.287 * * [simplify]: Extracting #8: cost 0 inf + 176132 6.297 * [simplify]: Simplified to (-.p16 (/.p16 (+.p16 b (+.p16 a c)) (real->posit16 2)) b) 6.297 * [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 (+.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)) 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)))) 6.298 * * * * [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))) (*.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))) (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))))> 6.298 * * * * [progress]: [ 7 / 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 (*.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))))> 6.298 * * * * [progress]: [ 8 / 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 (+.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))))> 6.298 * [simplify]: Simplifying (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) a) 6.298 * * [simplify]: iters left: 4 (9 enodes) 6.300 * * [simplify]: iters left: 3 (21 enodes) 6.303 * * [simplify]: iters left: 2 (27 enodes) 6.307 * * [simplify]: iters left: 1 (28 enodes) 6.312 * * [simplify]: Extracting #0: cost 1 inf + 0 6.312 * * [simplify]: Extracting #1: cost 3 inf + 0 6.312 * * [simplify]: Extracting #2: cost 4 inf + 1 6.312 * * [simplify]: Extracting #3: cost 10 inf + 1 6.313 * * [simplify]: Extracting #4: cost 1 inf + 738 6.313 * * [simplify]: Extracting #5: cost 0 inf + 1302 6.313 * [simplify]: Simplified to (+.p16 a (/.p16 (+.p16 (+.p16 b a) c) (real->posit16 2))) 6.313 * [simplify]: Simplified (2 1 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 a (/.p16 (+.p16 (+.p16 b a) 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)) 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)))) 6.313 * [simplify]: Simplifying (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) a) 6.313 * * [simplify]: iters left: 4 (9 enodes) 6.315 * * [simplify]: iters left: 3 (27 enodes) 6.320 * * [simplify]: iters left: 2 (47 enodes) 6.336 * * [simplify]: iters left: 1 (123 enodes) 6.371 * * [simplify]: Extracting #0: cost 1 inf + 0 6.371 * * [simplify]: Extracting #1: cost 15 inf + 0 6.372 * * [simplify]: Extracting #2: cost 53 inf + 1 6.372 * * [simplify]: Extracting #3: cost 87 inf + 1044 6.372 * * [simplify]: Extracting #4: cost 139 inf + 5657 6.373 * * [simplify]: Extracting #5: cost 115 inf + 19521 6.377 * * [simplify]: Extracting #6: cost 57 inf + 79064 6.385 * * [simplify]: Extracting #7: cost 8 inf + 157140 6.394 * * [simplify]: Extracting #8: cost 0 inf + 176132 6.406 * [simplify]: Simplified to (-.p16 (/.p16 (+.p16 b (+.p16 a c)) (real->posit16 2)) a) 6.406 * [simplify]: Simplified (2 1 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 (+.p16 (+.p16 a b) c) (real->posit16 2)) a) (-.p16 (/.p16 (+.p16 b (+.p16 a c)) (real->posit16 2)) 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)))) 6.406 * * * * [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))) (neg.p16 (*.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))))> 6.406 * * * * [progress]: [ 10 / 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 (+.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))))> 6.406 * * * * [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 (+.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))))> 6.407 * * * * [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 (+.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))))> 6.407 * * * * [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 (+.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))))> 6.407 * * * * [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 (+.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))))> 6.407 * * * [progress]: adding candidates to table 6.847 * * [progress]: iteration 4 / 4 6.847 * * * [progress]: picking best candidate 6.878 * * * * [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)))))> 6.878 * * * [progress]: localizing error 7.408 * * * [progress]: generating rewritten candidates 7.408 * * * * [progress]: [ 1 / 4 ] rewriting at (2 1 1 1 2) 7.534 * * * * [progress]: [ 2 / 4 ] rewriting at (2 1 2) 7.609 * * * * [progress]: [ 3 / 4 ] rewriting at (2 1 1 2) 7.633 * * * * [progress]: [ 4 / 4 ] rewriting at (2 1 1 1 2 1) 7.638 * * * [progress]: generating series expansions 7.638 * * * * [progress]: [ 1 / 4 ] generating series at (2 1 1 1 2) 7.638 * * * * [progress]: [ 2 / 4 ] generating series at (2 1 2) 7.638 * * * * [progress]: [ 3 / 4 ] generating series at (2 1 1 2) 7.638 * * * * [progress]: [ 4 / 4 ] generating series at (2 1 1 1 2 1) 7.638 * * * [progress]: simplifying candidates 7.638 * * * * [progress]: [ 1 / 13 ] 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)))))> 7.638 * [simplify]: Simplifying (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) a) 7.638 * * [simplify]: iters left: 4 (9 enodes) 7.642 * * [simplify]: iters left: 3 (21 enodes) 7.647 * * [simplify]: iters left: 2 (27 enodes) 7.653 * * [simplify]: iters left: 1 (28 enodes) 7.660 * * [simplify]: Extracting #0: cost 1 inf + 0 7.661 * * [simplify]: Extracting #1: cost 3 inf + 0 7.661 * * [simplify]: Extracting #2: cost 4 inf + 1 7.661 * * [simplify]: Extracting #3: cost 10 inf + 1 7.661 * * [simplify]: Extracting #4: cost 1 inf + 738 7.661 * * [simplify]: Extracting #5: cost 0 inf + 1302 7.661 * [simplify]: Simplified to (+.p16 a (/.p16 (+.p16 (+.p16 b a) c) (real->posit16 2))) 7.661 * [simplify]: Simplified (2 1 1 1 2 1) to (λ (a b c) (sqrt.p16 (*.p16 (*.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (/.p16 (+.p16 a (/.p16 (+.p16 (+.p16 b a) c) (real->posit16 2))) (/.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))))) 7.662 * * * * [progress]: [ 2 / 13 ] 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)))))> 7.662 * [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 a a) (*.p16 a a))) 7.662 * * [simplify]: iters left: 6 (13 enodes) 7.668 * * [simplify]: iters left: 5 (46 enodes) 7.684 * * [simplify]: iters left: 4 (130 enodes) 7.724 * * [simplify]: Extracting #0: cost 1 inf + 0 7.724 * * [simplify]: Extracting #1: cost 25 inf + 0 7.724 * * [simplify]: Extracting #2: cost 62 inf + 0 7.725 * * [simplify]: Extracting #3: cost 154 inf + 82 7.726 * * [simplify]: Extracting #4: cost 156 inf + 19005 7.732 * * [simplify]: Extracting #5: cost 37 inf + 171376 7.743 * * [simplify]: Extracting #6: cost 3 inf + 231747 7.756 * * [simplify]: Extracting #7: cost 0 inf + 241279 7.769 * [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 (/.p16 (+.p16 (+.p16 b a) c) (real->posit16 2)) (/.p16 (+.p16 (+.p16 b a) c) (real->posit16 2)))) (*.p16 (*.p16 a a) (*.p16 a a))) 7.769 * [simplify]: Simplified (2 1 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 (/.p16 (+.p16 (+.p16 b a) c) (real->posit16 2)) (/.p16 (+.p16 (+.p16 b a) c) (real->posit16 2))) (*.p16 (/.p16 (+.p16 (+.p16 b a) c) (real->posit16 2)) (/.p16 (+.p16 (+.p16 b a) 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))))) 7.769 * * * * [progress]: [ 3 / 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 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))))))> 7.770 * [simplify]: Simplifying (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) c) 7.770 * * [simplify]: iters left: 4 (9 enodes) 7.772 * * [simplify]: iters left: 3 (21 enodes) 7.775 * * [simplify]: iters left: 2 (27 enodes) 7.779 * * [simplify]: iters left: 1 (28 enodes) 7.783 * * [simplify]: Extracting #0: cost 1 inf + 0 7.783 * * [simplify]: Extracting #1: cost 3 inf + 0 7.783 * * [simplify]: Extracting #2: cost 4 inf + 1 7.783 * * [simplify]: Extracting #3: cost 10 inf + 1 7.783 * * [simplify]: Extracting #4: cost 5 inf + 47 7.783 * * [simplify]: Extracting #5: cost 1 inf + 738 7.783 * * [simplify]: Extracting #6: cost 0 inf + 1302 7.784 * [simplify]: Simplified to (+.p16 c (/.p16 (+.p16 a (+.p16 c b)) (real->posit16 2))) 7.784 * [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 (+.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 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)))))) 7.784 * * * * [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 (+.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)))))))> 7.784 * [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))) 7.784 * * [simplify]: iters left: 6 (13 enodes) 7.787 * * [simplify]: iters left: 5 (46 enodes) 7.796 * * [simplify]: iters left: 4 (130 enodes) 7.840 * * [simplify]: Extracting #0: cost 1 inf + 0 7.841 * * [simplify]: Extracting #1: cost 25 inf + 0 7.841 * * [simplify]: Extracting #2: cost 62 inf + 0 7.841 * * [simplify]: Extracting #3: cost 154 inf + 82 7.843 * * [simplify]: Extracting #4: cost 155 inf + 19371 7.853 * * [simplify]: Extracting #5: cost 43 inf + 161234 7.870 * * [simplify]: Extracting #6: cost 2 inf + 235712 7.890 * * [simplify]: Extracting #7: cost 0 inf + 242680 7.909 * [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))) 7.909 * [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 (+.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 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))))))) 7.910 * * * * [progress]: [ 5 / 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)) (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)))))> 7.910 * * * * [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)))))> 7.910 * * * * [progress]: [ 7 / 13 ] 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)))))> 7.910 * [simplify]: Simplifying (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) a) 7.911 * * [simplify]: iters left: 4 (9 enodes) 7.914 * * [simplify]: iters left: 3 (21 enodes) 7.919 * * [simplify]: iters left: 2 (27 enodes) 7.926 * * [simplify]: iters left: 1 (28 enodes) 7.933 * * [simplify]: Extracting #0: cost 1 inf + 0 7.933 * * [simplify]: Extracting #1: cost 3 inf + 0 7.933 * * [simplify]: Extracting #2: cost 4 inf + 1 7.933 * * [simplify]: Extracting #3: cost 10 inf + 1 7.934 * * [simplify]: Extracting #4: cost 1 inf + 738 7.934 * * [simplify]: Extracting #5: cost 0 inf + 1302 7.934 * [simplify]: Simplified to (+.p16 a (/.p16 (+.p16 (+.p16 b a) c) (real->posit16 2))) 7.934 * [simplify]: Simplified (2 1 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 a (/.p16 (+.p16 (+.p16 b a) 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)) 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))))) 7.935 * [simplify]: Simplifying (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) a) 7.935 * * [simplify]: iters left: 4 (9 enodes) 7.938 * * [simplify]: iters left: 3 (27 enodes) 7.946 * * [simplify]: iters left: 2 (47 enodes) 7.959 * * [simplify]: iters left: 1 (123 enodes) 8.002 * * [simplify]: Extracting #0: cost 1 inf + 0 8.002 * * [simplify]: Extracting #1: cost 15 inf + 0 8.002 * * [simplify]: Extracting #2: cost 53 inf + 1 8.003 * * [simplify]: Extracting #3: cost 87 inf + 1044 8.003 * * [simplify]: Extracting #4: cost 139 inf + 5657 8.004 * * [simplify]: Extracting #5: cost 115 inf + 19521 8.008 * * [simplify]: Extracting #6: cost 57 inf + 79064 8.018 * * [simplify]: Extracting #7: cost 8 inf + 157140 8.033 * * [simplify]: Extracting #8: cost 0 inf + 176132 8.051 * [simplify]: Simplified to (-.p16 (/.p16 (+.p16 b (+.p16 a c)) (real->posit16 2)) a) 8.051 * [simplify]: Simplified (2 1 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 (+.p16 (+.p16 a b) c) (real->posit16 2)) a) (-.p16 (/.p16 (+.p16 b (+.p16 a 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))))) 8.052 * * * * [progress]: [ 8 / 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))) (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)))))> 8.052 * * * * [progress]: [ 9 / 13 ] 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)))))> 8.052 * * * * [progress]: [ 10 / 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)))))> 8.052 * * * * [progress]: [ 11 / 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)))))> 8.052 * * * * [progress]: [ 12 / 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)))))> 8.052 * * * * [progress]: [ 13 / 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)))))> 8.052 * * * [progress]: adding candidates to table 8.490 * [progress]: [Phase 3 of 3] Extracting. 8.490 * * [regime]: Finding splitpoints for: (#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)))))))> #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))))> #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)))))> #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)))))>) 8.497 * * * [regime-changes]: Trying 3 branch expressions: (c b a) 8.497 * * * * [regimes]: Trying to branch on c from (#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)))))))> #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))))> #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)))))> #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)))))>) 8.609 * * * * [regimes]: Trying to branch on b from (#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)))))))> #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))))> #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)))))> #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)))))>) 8.723 * * * * [regimes]: Trying to branch on a from (#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)))))))> #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))))> #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)))))> #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)))))>) 8.845 * * * [regime]: Found split indices: #