0.003 * [progress]: [Phase 1 of 3] Setting up. 0.003 * * * [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.011 * * * * [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.023 * * * * [points]: Setting MPFR precision to 64 0.027 * * * * [points]: Setting MPFR precision to 320 0.031 * * * * [points]: Computing exacts on every 4 of 256 points to ramp up precision 0.038 * * * * [points]: Setting MPFR precision to 64 0.045 * * * * [points]: Setting MPFR precision to 320 0.052 * * * * [points]: Computing exacts on every 2 of 256 points to ramp up precision 0.059 * * * * [points]: Setting MPFR precision to 64 0.071 * * * * [points]: Setting MPFR precision to 320 0.093 * * * * [points]: Computing exacts for 256 points 0.097 * * * * [points]: Setting MPFR precision to 64 0.117 * * * * [points]: Setting MPFR precision to 320 0.137 * * * * [points]: Filtering points with unrepresentable outputs 0.137 * * * * [points]: Sampling 227 additional inputs, on iter 1 have 29 / 256 0.138 * * * * [points]: Computing exacts on every 14 of 227 points to ramp up precision 0.142 * * * * [points]: Setting MPFR precision to 64 0.143 * * * * [points]: Setting MPFR precision to 320 0.144 * * * * [points]: Computing exacts on every 7 of 227 points to ramp up precision 0.148 * * * * [points]: Setting MPFR precision to 64 0.150 * * * * [points]: Setting MPFR precision to 320 0.152 * * * * [points]: Computing exacts on every 3 of 227 points to ramp up precision 0.157 * * * * [points]: Setting MPFR precision to 64 0.165 * * * * [points]: Setting MPFR precision to 320 0.173 * * * * [points]: Computing exacts for 227 points 0.180 * * * * [points]: Setting MPFR precision to 64 0.198 * * * * [points]: Setting MPFR precision to 320 0.247 * * * * [points]: Filtering points with unrepresentable outputs 0.247 * * * * [points]: Sampling 199 additional inputs, on iter 2 have 57 / 256 0.249 * * * * [points]: Computing exacts on every 12 of 199 points to ramp up precision 0.260 * * * * [points]: Setting MPFR precision to 64 0.262 * * * * [points]: Setting MPFR precision to 320 0.264 * * * * [points]: Computing exacts on every 6 of 199 points to ramp up precision 0.271 * * * * [points]: Setting MPFR precision to 64 0.275 * * * * [points]: Setting MPFR precision to 320 0.279 * * * * [points]: Computing exacts on every 3 of 199 points to ramp up precision 0.286 * * * * [points]: Setting MPFR precision to 64 0.293 * * * * [points]: Setting MPFR precision to 320 0.300 * * * * [points]: Computing exacts for 199 points 0.308 * * * * [points]: Setting MPFR precision to 64 0.333 * * * * [points]: Setting MPFR precision to 320 0.359 * * * * [points]: Filtering points with unrepresentable outputs 0.359 * * * * [points]: Sampling 176 additional inputs, on iter 3 have 80 / 256 0.361 * * * * [points]: Computing exacts on every 11 of 176 points to ramp up precision 0.368 * * * * [points]: Setting MPFR precision to 64 0.370 * * * * [points]: Setting MPFR precision to 320 0.372 * * * * [points]: Computing exacts on every 5 of 176 points to ramp up precision 0.379 * * * * [points]: Setting MPFR precision to 64 0.381 * * * * [points]: Setting MPFR precision to 320 0.383 * * * * [points]: Computing exacts on every 2 of 176 points to ramp up precision 0.387 * * * * [points]: Setting MPFR precision to 64 0.390 * * * * [points]: Setting MPFR precision to 320 0.394 * * * * [points]: Computing exacts for 176 points 0.398 * * * * [points]: Setting MPFR precision to 64 0.431 * * * * [points]: Setting MPFR precision to 320 0.443 * * * * [points]: Filtering points with unrepresentable outputs 0.443 * * * * [points]: Sampling 158 additional inputs, on iter 4 have 98 / 256 0.444 * * * * [points]: Computing exacts on every 9 of 158 points to ramp up precision 0.448 * * * * [points]: Setting MPFR precision to 64 0.449 * * * * [points]: Setting MPFR precision to 320 0.450 * * * * [points]: Computing exacts on every 4 of 158 points to ramp up precision 0.453 * * * * [points]: Setting MPFR precision to 64 0.456 * * * * [points]: Setting MPFR precision to 320 0.458 * * * * [points]: Computing exacts on every 2 of 158 points to ramp up precision 0.461 * * * * [points]: Setting MPFR precision to 64 0.465 * * * * [points]: Setting MPFR precision to 320 0.469 * * * * [points]: Computing exacts for 158 points 0.473 * * * * [points]: Setting MPFR precision to 64 0.484 * * * * [points]: Setting MPFR precision to 320 0.495 * * * * [points]: Filtering points with unrepresentable outputs 0.495 * * * * [points]: Sampling 138 additional inputs, on iter 5 have 118 / 256 0.495 * * * * [points]: Computing exacts on every 8 of 138 points to ramp up precision 0.499 * * * * [points]: Setting MPFR precision to 64 0.500 * * * * [points]: Setting MPFR precision to 320 0.501 * * * * [points]: Computing exacts on every 4 of 138 points to ramp up precision 0.505 * * * * [points]: Setting MPFR precision to 64 0.507 * * * * [points]: Setting MPFR precision to 320 0.509 * * * * [points]: Computing exacts on every 2 of 138 points to ramp up precision 0.535 * * * * [points]: Setting MPFR precision to 64 0.539 * * * * [points]: Setting MPFR precision to 320 0.543 * * * * [points]: Computing exacts for 138 points 0.547 * * * * [points]: Setting MPFR precision to 64 0.557 * * * * [points]: Setting MPFR precision to 320 0.566 * * * * [points]: Filtering points with unrepresentable outputs 0.566 * * * * [points]: Sampling 120 additional inputs, on iter 6 have 136 / 256 0.567 * * * * [points]: Computing exacts on every 7 of 120 points to ramp up precision 0.571 * * * * [points]: Setting MPFR precision to 64 0.572 * * * * [points]: Setting MPFR precision to 320 0.573 * * * * [points]: Computing exacts on every 3 of 120 points to ramp up precision 0.577 * * * * [points]: Setting MPFR precision to 64 0.579 * * * * [points]: Setting MPFR precision to 320 0.581 * * * * [points]: Computing exacts for 120 points 0.585 * * * * [points]: Setting MPFR precision to 64 0.594 * * * * [points]: Setting MPFR precision to 320 0.602 * * * * [points]: Filtering points with unrepresentable outputs 0.603 * * * * [points]: Sampling 110 additional inputs, on iter 7 have 146 / 256 0.603 * * * * [points]: Computing exacts on every 6 of 110 points to ramp up precision 0.607 * * * * [points]: Setting MPFR precision to 64 0.608 * * * * [points]: Setting MPFR precision to 320 0.609 * * * * [points]: Computing exacts on every 3 of 110 points to ramp up precision 0.613 * * * * [points]: Setting MPFR precision to 64 0.615 * * * * [points]: Setting MPFR precision to 320 0.617 * * * * [points]: Computing exacts for 110 points 0.621 * * * * [points]: Setting MPFR precision to 64 0.648 * * * * [points]: Setting MPFR precision to 320 0.656 * * * * [points]: Filtering points with unrepresentable outputs 0.656 * * * * [points]: Sampling 96 additional inputs, on iter 8 have 160 / 256 0.658 * * * * [points]: Computing exacts on every 6 of 96 points to ramp up precision 0.662 * * * * [points]: Setting MPFR precision to 64 0.663 * * * * [points]: Setting MPFR precision to 320 0.664 * * * * [points]: Computing exacts on every 3 of 96 points to ramp up precision 0.668 * * * * [points]: Setting MPFR precision to 64 0.670 * * * * [points]: Setting MPFR precision to 320 0.672 * * * * [points]: Computing exacts for 96 points 0.675 * * * * [points]: Setting MPFR precision to 64 0.682 * * * * [points]: Setting MPFR precision to 320 0.688 * * * * [points]: Filtering points with unrepresentable outputs 0.689 * * * * [points]: Sampling 75 additional inputs, on iter 9 have 181 / 256 0.689 * * * * [points]: Computing exacts on every 4 of 75 points to ramp up precision 0.693 * * * * [points]: Setting MPFR precision to 64 0.694 * * * * [points]: Setting MPFR precision to 320 0.695 * * * * [points]: Computing exacts on every 2 of 75 points to ramp up precision 0.699 * * * * [points]: Setting MPFR precision to 64 0.701 * * * * [points]: Setting MPFR precision to 320 0.702 * * * * [points]: Computing exacts for 75 points 0.706 * * * * [points]: Setting MPFR precision to 64 0.712 * * * * [points]: Setting MPFR precision to 320 0.717 * * * * [points]: Filtering points with unrepresentable outputs 0.717 * * * * [points]: Sampling 64 additional inputs, on iter 10 have 192 / 256 0.717 * * * * [points]: Computing exacts on every 4 of 64 points to ramp up precision 0.721 * * * * [points]: Setting MPFR precision to 64 0.722 * * * * [points]: Setting MPFR precision to 320 0.723 * * * * [points]: Computing exacts on every 2 of 64 points to ramp up precision 0.727 * * * * [points]: Setting MPFR precision to 64 0.728 * * * * [points]: Setting MPFR precision to 320 0.730 * * * * [points]: Computing exacts for 64 points 0.733 * * * * [points]: Setting MPFR precision to 64 0.753 * * * * [points]: Setting MPFR precision to 320 0.758 * * * * [points]: Filtering points with unrepresentable outputs 0.758 * * * * [points]: Sampling 55 additional inputs, on iter 11 have 201 / 256 0.758 * * * * [points]: Computing exacts on every 3 of 55 points to ramp up precision 0.764 * * * * [points]: Setting MPFR precision to 64 0.765 * * * * [points]: Setting MPFR precision to 320 0.766 * * * * [points]: Computing exacts for 55 points 0.770 * * * * [points]: Setting MPFR precision to 64 0.774 * * * * [points]: Setting MPFR precision to 320 0.778 * * * * [points]: Filtering points with unrepresentable outputs 0.778 * * * * [points]: Sampling 49 additional inputs, on iter 12 have 207 / 256 0.778 * * * * [points]: Computing exacts on every 3 of 49 points to ramp up precision 0.782 * * * * [points]: Setting MPFR precision to 64 0.783 * * * * [points]: Setting MPFR precision to 320 0.784 * * * * [points]: Computing exacts for 49 points 0.787 * * * * [points]: Setting MPFR precision to 64 0.791 * * * * [points]: Setting MPFR precision to 320 0.794 * * * * [points]: Filtering points with unrepresentable outputs 0.794 * * * * [points]: Sampling 41 additional inputs, on iter 13 have 215 / 256 0.795 * * * * [points]: Computing exacts on every 2 of 41 points to ramp up precision 0.798 * * * * [points]: Setting MPFR precision to 64 0.799 * * * * [points]: Setting MPFR precision to 320 0.800 * * * * [points]: Computing exacts for 41 points 0.804 * * * * [points]: Setting MPFR precision to 64 0.807 * * * * [points]: Setting MPFR precision to 320 0.810 * * * * [points]: Filtering points with unrepresentable outputs 0.810 * * * * [points]: Sampling 37 additional inputs, on iter 14 have 219 / 256 0.810 * * * * [points]: Computing exacts on every 2 of 37 points to ramp up precision 0.814 * * * * [points]: Setting MPFR precision to 64 0.815 * * * * [points]: Setting MPFR precision to 320 0.816 * * * * [points]: Computing exacts for 37 points 0.819 * * * * [points]: Setting MPFR precision to 64 0.822 * * * * [points]: Setting MPFR precision to 320 0.825 * * * * [points]: Filtering points with unrepresentable outputs 0.825 * * * * [points]: Sampling 31 additional inputs, on iter 15 have 225 / 256 0.825 * * * * [points]: Computing exacts for 31 points 0.829 * * * * [points]: Setting MPFR precision to 64 0.831 * * * * [points]: Setting MPFR precision to 320 0.833 * * * * [points]: Filtering points with unrepresentable outputs 0.833 * * * * [points]: Sampling 25 additional inputs, on iter 16 have 231 / 256 0.833 * * * * [points]: Computing exacts for 25 points 0.837 * * * * [points]: Setting MPFR precision to 64 1.122 * * * * [points]: Setting MPFR precision to 320 1.125 * * * * [points]: Filtering points with unrepresentable outputs 1.125 * * * * [points]: Sampling 23 additional inputs, on iter 17 have 233 / 256 1.126 * * * * [points]: Computing exacts for 23 points 1.133 * * * * [points]: Setting MPFR precision to 64 1.136 * * * * [points]: Setting MPFR precision to 320 1.139 * * * * [points]: Filtering points with unrepresentable outputs 1.139 * * * * [points]: Sampling 20 additional inputs, on iter 18 have 236 / 256 1.140 * * * * [points]: Computing exacts for 20 points 1.151 * * * * [points]: Setting MPFR precision to 64 1.154 * * * * [points]: Setting MPFR precision to 320 1.157 * * * * [points]: Filtering points with unrepresentable outputs 1.157 * * * * [points]: Sampling 19 additional inputs, on iter 19 have 237 / 256 1.157 * * * * [points]: Computing exacts for 19 points 1.164 * * * * [points]: Setting MPFR precision to 64 1.166 * * * * [points]: Setting MPFR precision to 320 1.168 * * * * [points]: Filtering points with unrepresentable outputs 1.168 * * * * [points]: Sampling 14 additional inputs, on iter 20 have 242 / 256 1.168 * * * * [points]: Computing exacts for 14 points 1.172 * * * * [points]: Setting MPFR precision to 64 1.173 * * * * [points]: Setting MPFR precision to 320 1.174 * * * * [points]: Filtering points with unrepresentable outputs 1.174 * * * * [points]: Sampling 13 additional inputs, on iter 21 have 243 / 256 1.174 * * * * [points]: Computing exacts for 13 points 1.177 * * * * [points]: Setting MPFR precision to 64 1.178 * * * * [points]: Setting MPFR precision to 320 1.179 * * * * [points]: Filtering points with unrepresentable outputs 1.179 * * * * [points]: Sampling 12 additional inputs, on iter 22 have 244 / 256 1.180 * * * * [points]: Computing exacts for 12 points 1.184 * * * * [points]: Setting MPFR precision to 64 1.185 * * * * [points]: Setting MPFR precision to 320 1.186 * * * * [points]: Filtering points with unrepresentable outputs 1.186 * * * * [points]: Sampling 12 additional inputs, on iter 23 have 244 / 256 1.186 * * * * [points]: Computing exacts for 12 points 1.189 * * * * [points]: Setting MPFR precision to 64 1.190 * * * * [points]: Setting MPFR precision to 320 1.192 * * * * [points]: Filtering points with unrepresentable outputs 1.192 * * * * [points]: Sampling 9 additional inputs, on iter 24 have 247 / 256 1.192 * * * * [points]: Computing exacts for 9 points 1.195 * * * * [points]: Setting MPFR precision to 64 1.196 * * * * [points]: Setting MPFR precision to 320 1.197 * * * * [points]: Filtering points with unrepresentable outputs 1.197 * * * * [points]: Sampling 8 additional inputs, on iter 25 have 248 / 256 1.197 * * * * [points]: Computing exacts for 8 points 1.201 * * * * [points]: Setting MPFR precision to 64 1.201 * * * * [points]: Setting MPFR precision to 320 1.202 * * * * [points]: Filtering points with unrepresentable outputs 1.202 * * * * [points]: Sampling 8 additional inputs, on iter 26 have 248 / 256 1.202 * * * * [points]: Computing exacts for 8 points 1.208 * * * * [points]: Setting MPFR precision to 64 1.210 * * * * [points]: Setting MPFR precision to 320 1.211 * * * * [points]: Filtering points with unrepresentable outputs 1.211 * * * * [points]: Sampling 8 additional inputs, on iter 27 have 248 / 256 1.211 * * * * [points]: Computing exacts for 8 points 1.218 * * * * [points]: Setting MPFR precision to 64 1.219 * * * * [points]: Setting MPFR precision to 320 1.221 * * * * [points]: Filtering points with unrepresentable outputs 1.221 * * * * [points]: Sampling 7 additional inputs, on iter 28 have 249 / 256 1.221 * * * * [points]: Computing exacts for 7 points 1.228 * * * * [points]: Setting MPFR precision to 64 1.229 * * * * [points]: Setting MPFR precision to 320 1.230 * * * * [points]: Filtering points with unrepresentable outputs 1.230 * * * * [points]: Sampling 7 additional inputs, on iter 29 have 249 / 256 1.230 * * * * [points]: Computing exacts for 7 points 1.254 * * * * [points]: Setting MPFR precision to 64 1.255 * * * * [points]: Setting MPFR precision to 320 1.255 * * * * [points]: Filtering points with unrepresentable outputs 1.255 * * * * [points]: Sampling 5 additional inputs, on iter 30 have 251 / 256 1.256 * * * * [points]: Computing exacts for 5 points 1.259 * * * * [points]: Setting MPFR precision to 64 1.260 * * * * [points]: Setting MPFR precision to 320 1.260 * * * * [points]: Filtering points with unrepresentable outputs 1.260 * * * * [points]: Sampling 5 additional inputs, on iter 31 have 251 / 256 1.260 * * * * [points]: Computing exacts for 5 points 1.264 * * * * [points]: Setting MPFR precision to 64 1.264 * * * * [points]: Setting MPFR precision to 320 1.265 * * * * [points]: Filtering points with unrepresentable outputs 1.265 * * * * [points]: Sampling 4 additional inputs, on iter 32 have 252 / 256 1.265 * * * * [points]: Computing exacts for 4 points 1.268 * * * * [points]: Setting MPFR precision to 64 1.269 * * * * [points]: Setting MPFR precision to 320 1.269 * * * * [points]: Filtering points with unrepresentable outputs 1.269 * * * * [points]: Sampling 4 additional inputs, on iter 33 have 252 / 256 1.269 * * * * [points]: Computing exacts for 4 points 1.273 * * * * [points]: Setting MPFR precision to 64 1.274 * * * * [points]: Setting MPFR precision to 320 1.274 * * * * [points]: Filtering points with unrepresentable outputs 1.274 * * * * [points]: Sampling 4 additional inputs, on iter 34 have 252 / 256 1.274 * * * * [points]: Computing exacts for 4 points 1.278 * * * * [points]: Setting MPFR precision to 64 1.278 * * * * [points]: Setting MPFR precision to 320 1.278 * * * * [points]: Filtering points with unrepresentable outputs 1.278 * * * * [points]: Sampling 4 additional inputs, on iter 35 have 252 / 256 1.278 * * * * [points]: Computing exacts for 4 points 1.282 * * * * [points]: Setting MPFR precision to 64 1.283 * * * * [points]: Setting MPFR precision to 320 1.283 * * * * [points]: Filtering points with unrepresentable outputs 1.283 * * * * [points]: Sampling 4 additional inputs, on iter 36 have 252 / 256 1.283 * * * * [points]: Computing exacts for 4 points 1.287 * * * * [points]: Setting MPFR precision to 64 1.287 * * * * [points]: Setting MPFR precision to 320 1.287 * * * * [points]: Filtering points with unrepresentable outputs 1.287 * * * * [points]: Sampling 4 additional inputs, on iter 37 have 253 / 256 1.287 * * * * [points]: Computing exacts for 4 points 1.291 * * * * [points]: Setting MPFR precision to 64 1.291 * * * * [points]: Setting MPFR precision to 320 1.292 * * * * [points]: Filtering points with unrepresentable outputs 1.292 * * * * [points]: Sampling 4 additional inputs, on iter 38 have 254 / 256 1.292 * * * * [points]: Computing exacts for 4 points 1.296 * * * * [points]: Setting MPFR precision to 64 1.296 * * * * [points]: Setting MPFR precision to 320 1.297 * * * * [points]: Filtering points with unrepresentable outputs 1.297 * * * * [points]: Sampling 4 additional inputs, on iter 39 have 254 / 256 1.297 * * * * [points]: Computing exacts for 4 points 1.304 * * * * [points]: Setting MPFR precision to 64 1.305 * * * * [points]: Setting MPFR precision to 320 1.305 * * * * [points]: Filtering points with unrepresentable outputs 1.305 * * * * [points]: Sampled 257 points with exact outputs 1.306 * * * [progress]: [2/2] Setting up program. 1.318 * [progress]: [Phase 2 of 3] Improving. 1.319 * * * * [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.319 * [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.319 * * [simplify]: iters left: 6 (15 enodes) 1.323 * * [simplify]: iters left: 5 (54 enodes) 1.340 * * [simplify]: iters left: 4 (174 enodes) 1.450 * * [simplify]: Extracting #0: cost 1 inf + 0 1.450 * * [simplify]: Extracting #1: cost 2 inf + 0 1.450 * * [simplify]: Extracting #2: cost 52 inf + 0 1.451 * * [simplify]: Extracting #3: cost 218 inf + 0 1.454 * * [simplify]: Extracting #4: cost 350 inf + 488 1.462 * * [simplify]: Extracting #5: cost 271 inf + 83278 1.476 * * [simplify]: Extracting #6: cost 99 inf + 301152 1.511 * * [simplify]: Extracting #7: cost 13 inf + 445414 1.564 * * [simplify]: Extracting #8: cost 0 inf + 471346 1.620 * [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.620 * [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.641 * * [progress]: iteration 1 / 4 1.641 * * * [progress]: picking best candidate 1.660 * * * * [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.660 * * * [progress]: localizing error 2.064 * * * [progress]: generating rewritten candidates 2.064 * * * * [progress]: [ 1 / 4 ] rewriting at (2 1 2) 2.108 * * * * [progress]: [ 2 / 4 ] rewriting at (2 1 1 2) 2.130 * * * * [progress]: [ 3 / 4 ] rewriting at (2 1 1 1 2) 2.155 * * * * [progress]: [ 4 / 4 ] rewriting at (2 1 1) 2.207 * * * [progress]: generating series expansions 2.207 * * * * [progress]: [ 1 / 4 ] generating series at (2 1 2) 2.207 * * * * [progress]: [ 2 / 4 ] generating series at (2 1 1 2) 2.207 * * * * [progress]: [ 3 / 4 ] generating series at (2 1 1 1 2) 2.208 * * * * [progress]: [ 4 / 4 ] generating series at (2 1 1) 2.208 * * * [progress]: simplifying candidates 2.208 * * * * [progress]: [ 1 / 17 ] 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.208 * [simplify]: Simplifying (neg.p16 c) 2.208 * * [simplify]: iters left: 1 (2 enodes) 2.209 * * [simplify]: Extracting #0: cost 1 inf + 0 2.209 * * [simplify]: Extracting #1: cost 2 inf + 0 2.209 * * [simplify]: Extracting #2: cost 1 inf + 1 2.209 * * [simplify]: Extracting #3: cost 0 inf + 82 2.209 * [simplify]: Simplified to (neg.p16 c) 2.209 * [simplify]: Simplified (2 1 2 2) to (λ (a b c) (sqrt.p16 (*.p16 (*.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) a)) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) b)) (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (neg.p16 c))))) 2.209 * * * * [progress]: [ 2 / 17 ] 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.209 * [simplify]: Simplifying (-.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2))) (*.p16 c c)) 2.210 * * [simplify]: iters left: 5 (11 enodes) 2.215 * * [simplify]: iters left: 4 (36 enodes) 2.223 * * [simplify]: iters left: 3 (93 enodes) 2.245 * * [simplify]: iters left: 2 (310 enodes) 2.386 * * [simplify]: Extracting #0: cost 1 inf + 0 2.386 * * [simplify]: Extracting #1: cost 32 inf + 0 2.387 * * [simplify]: Extracting #2: cost 177 inf + 0 2.389 * * [simplify]: Extracting #3: cost 262 inf + 323 2.395 * * [simplify]: Extracting #4: cost 417 inf + 52622 2.417 * * [simplify]: Extracting #5: cost 157 inf + 465463 2.455 * * [simplify]: Extracting #6: cost 2 inf + 707329 2.498 * * [simplify]: Extracting #7: cost 0 inf + 711417 2.539 * [simplify]: Simplified to (*.p16 (+.p16 c (/.p16 (+.p16 (+.p16 b a) c) (real->posit16 2))) (-.p16 (/.p16 (+.p16 (+.p16 b a) c) (real->posit16 2)) c)) 2.539 * [simplify]: Simplified (2 1 2 1) to (λ (a b c) (sqrt.p16 (*.p16 (*.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) a)) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) b)) (/.p16 (*.p16 (+.p16 c (/.p16 (+.p16 (+.p16 b a) c) (real->posit16 2))) (-.p16 (/.p16 (+.p16 (+.p16 b a) c) (real->posit16 2)) c)) (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) c))))) 2.539 * [simplify]: Simplifying (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) c) 2.539 * * [simplify]: iters left: 4 (9 enodes) 2.541 * * [simplify]: iters left: 3 (21 enodes) 2.544 * * [simplify]: iters left: 2 (27 enodes) 2.548 * * [simplify]: iters left: 1 (28 enodes) 2.552 * * [simplify]: Extracting #0: cost 1 inf + 0 2.552 * * [simplify]: Extracting #1: cost 3 inf + 0 2.552 * * [simplify]: Extracting #2: cost 4 inf + 1 2.552 * * [simplify]: Extracting #3: cost 10 inf + 1 2.552 * * [simplify]: Extracting #4: cost 5 inf + 47 2.552 * * [simplify]: Extracting #5: cost 1 inf + 738 2.552 * * [simplify]: Extracting #6: cost 0 inf + 1302 2.552 * [simplify]: Simplified to (+.p16 c (/.p16 (+.p16 a (+.p16 c b)) (real->posit16 2))) 2.552 * [simplify]: Simplified (2 1 2 2) to (λ (a b c) (sqrt.p16 (*.p16 (*.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) a)) (-.p16 (/.p16 (+.p16 (+.p16 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 c (/.p16 (+.p16 a (+.p16 c b)) (real->posit16 2))))))) 2.552 * * * * [progress]: [ 3 / 17 ] 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.552 * [simplify]: Simplifying (neg.p16 b) 2.552 * * [simplify]: iters left: 1 (2 enodes) 2.553 * * [simplify]: Extracting #0: cost 1 inf + 0 2.553 * * [simplify]: Extracting #1: cost 2 inf + 0 2.553 * * [simplify]: Extracting #2: cost 1 inf + 1 2.553 * * [simplify]: Extracting #3: cost 0 inf + 82 2.553 * [simplify]: Simplified to (neg.p16 b) 2.553 * [simplify]: Simplified (2 1 1 2 2) to (λ (a b c) (sqrt.p16 (*.p16 (*.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) a)) (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (neg.p16 b))) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) c)))) 2.553 * * * * [progress]: [ 4 / 17 ] 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.553 * [simplify]: Simplifying (-.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2))) (*.p16 b b)) 2.553 * * [simplify]: iters left: 5 (11 enodes) 2.556 * * [simplify]: iters left: 4 (36 enodes) 2.563 * * [simplify]: iters left: 3 (93 enodes) 2.592 * * [simplify]: iters left: 2 (310 enodes) 2.835 * * [simplify]: Extracting #0: cost 1 inf + 0 2.836 * * [simplify]: Extracting #1: cost 32 inf + 0 2.836 * * [simplify]: Extracting #2: cost 177 inf + 0 2.838 * * [simplify]: Extracting #3: cost 260 inf + 323 2.841 * * [simplify]: Extracting #4: cost 456 inf + 5597 2.862 * * [simplify]: Extracting #5: cost 278 inf + 236939 2.931 * * [simplify]: Extracting #6: cost 27 inf + 652788 3.010 * * [simplify]: Extracting #7: cost 2 inf + 706688 3.087 * * [simplify]: Extracting #8: cost 0 inf + 713376 3.166 * [simplify]: Simplified to (*.p16 (+.p16 (/.p16 (+.p16 (+.p16 b a) c) (real->posit16 2)) b) (-.p16 (/.p16 (+.p16 (+.p16 b a) c) (real->posit16 2)) b)) 3.166 * [simplify]: Simplified (2 1 1 2 1) to (λ (a b c) (sqrt.p16 (*.p16 (*.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) a)) (/.p16 (*.p16 (+.p16 (/.p16 (+.p16 (+.p16 b a) c) (real->posit16 2)) b) (-.p16 (/.p16 (+.p16 (+.p16 b a) c) (real->posit16 2)) b)) (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) b))) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) c)))) 3.167 * [simplify]: Simplifying (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) b) 3.167 * * [simplify]: iters left: 4 (9 enodes) 3.171 * * [simplify]: iters left: 3 (21 enodes) 3.177 * * [simplify]: iters left: 2 (27 enodes) 3.185 * * [simplify]: iters left: 1 (28 enodes) 3.192 * * [simplify]: Extracting #0: cost 1 inf + 0 3.192 * * [simplify]: Extracting #1: cost 3 inf + 0 3.192 * * [simplify]: Extracting #2: cost 4 inf + 1 3.193 * * [simplify]: Extracting #3: cost 10 inf + 1 3.193 * * [simplify]: Extracting #4: cost 5 inf + 47 3.193 * * [simplify]: Extracting #5: cost 1 inf + 738 3.193 * * [simplify]: Extracting #6: cost 0 inf + 1302 3.193 * [simplify]: Simplified to (+.p16 (/.p16 (+.p16 a (+.p16 c b)) (real->posit16 2)) b) 3.194 * [simplify]: Simplified (2 1 1 2 2) to (λ (a b c) (sqrt.p16 (*.p16 (*.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) a)) (/.p16 (-.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2))) (*.p16 b b)) (+.p16 (/.p16 (+.p16 a (+.p16 c b)) (real->posit16 2)) b))) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) c)))) 3.194 * * * * [progress]: [ 5 / 17 ] 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))))> 3.194 * [simplify]: Simplifying (neg.p16 a) 3.194 * * [simplify]: iters left: 1 (2 enodes) 3.195 * * [simplify]: Extracting #0: cost 1 inf + 0 3.195 * * [simplify]: Extracting #1: cost 2 inf + 0 3.195 * * [simplify]: Extracting #2: cost 1 inf + 1 3.195 * * [simplify]: Extracting #3: cost 0 inf + 82 3.195 * [simplify]: Simplified to (neg.p16 a) 3.195 * [simplify]: Simplified (2 1 1 1 2 2) to (λ (a b c) (sqrt.p16 (*.p16 (*.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (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)))) 3.195 * * * * [progress]: [ 6 / 17 ] 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))))> 3.196 * [simplify]: Simplifying (-.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2))) (*.p16 a a)) 3.196 * * [simplify]: iters left: 5 (11 enodes) 3.201 * * [simplify]: iters left: 4 (36 enodes) 3.214 * * [simplify]: iters left: 3 (93 enodes) 3.253 * * [simplify]: iters left: 2 (310 enodes) 3.459 * * [simplify]: Extracting #0: cost 1 inf + 0 3.459 * * [simplify]: Extracting #1: cost 32 inf + 0 3.459 * * [simplify]: Extracting #2: cost 177 inf + 0 3.460 * * [simplify]: Extracting #3: cost 262 inf + 323 3.463 * * [simplify]: Extracting #4: cost 416 inf + 51663 3.485 * * [simplify]: Extracting #5: cost 116 inf + 501475 3.525 * * [simplify]: Extracting #6: cost 0 inf + 713857 3.567 * * [simplify]: Extracting #7: cost 0 inf + 713577 3.608 * [simplify]: Simplified to (*.p16 (+.p16 a (/.p16 (+.p16 (+.p16 b a) c) (real->posit16 2))) (-.p16 (/.p16 (+.p16 (+.p16 b a) c) (real->posit16 2)) a)) 3.608 * [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 a (/.p16 (+.p16 (+.p16 b a) c) (real->posit16 2))) (-.p16 (/.p16 (+.p16 (+.p16 b 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)))) 3.608 * [simplify]: Simplifying (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) a) 3.609 * * [simplify]: iters left: 4 (9 enodes) 3.611 * * [simplify]: iters left: 3 (21 enodes) 3.614 * * [simplify]: iters left: 2 (27 enodes) 3.618 * * [simplify]: iters left: 1 (28 enodes) 3.622 * * [simplify]: Extracting #0: cost 1 inf + 0 3.622 * * [simplify]: Extracting #1: cost 3 inf + 0 3.622 * * [simplify]: Extracting #2: cost 4 inf + 1 3.622 * * [simplify]: Extracting #3: cost 10 inf + 1 3.622 * * [simplify]: Extracting #4: cost 1 inf + 738 3.622 * * [simplify]: Extracting #5: cost 0 inf + 1302 3.622 * [simplify]: Simplified to (+.p16 a (/.p16 (+.p16 (+.p16 b a) c) (real->posit16 2))) 3.622 * [simplify]: Simplified (2 1 1 1 2 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 a (/.p16 (+.p16 (+.p16 b a) c) (real->posit16 2))))) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) b)) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) c)))) 3.623 * * * * [progress]: [ 7 / 17 ] simplifiying candidate #posit16 2)) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) a)) (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2))) (*.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) a)) (neg.p16 b))) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) c))))> 3.623 * [simplify]: Simplifying (*.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 a b) c) (real->posit16 2))) 3.623 * * [simplify]: iters left: 6 (11 enodes) 3.626 * * [simplify]: iters left: 5 (35 enodes) 3.632 * * [simplify]: iters left: 4 (99 enodes) 3.663 * * [simplify]: Extracting #0: cost 1 inf + 0 3.663 * * [simplify]: Extracting #1: cost 30 inf + 0 3.664 * * [simplify]: Extracting #2: cost 119 inf + 0 3.664 * * [simplify]: Extracting #3: cost 164 inf + 5280 3.669 * * [simplify]: Extracting #4: cost 60 inf + 113080 3.678 * * [simplify]: Extracting #5: cost 3 inf + 183806 3.689 * * [simplify]: Extracting #6: cost 0 inf + 189337 3.699 * [simplify]: Simplified to (*.p16 (*.p16 (-.p16 (/.p16 (+.p16 (+.p16 b a) c) (real->posit16 2)) a) (/.p16 (+.p16 (+.p16 b a) c) (real->posit16 2))) (/.p16 (+.p16 (+.p16 b a) c) (real->posit16 2))) 3.699 * [simplify]: Simplified (2 1 1 1) to (λ (a b c) (sqrt.p16 (*.p16 (+.p16 (*.p16 (*.p16 (-.p16 (/.p16 (+.p16 (+.p16 b a) c) (real->posit16 2)) a) (/.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)) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) a)) (neg.p16 b))) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) c)))) 3.699 * [simplify]: Simplifying (*.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) a)) (neg.p16 b)) 3.699 * * [simplify]: iters left: 6 (12 enodes) 3.702 * * [simplify]: iters left: 5 (36 enodes) 3.709 * * [simplify]: iters left: 4 (88 enodes) 3.732 * * [simplify]: iters left: 3 (326 enodes) 3.881 * * [simplify]: Extracting #0: cost 1 inf + 0 3.882 * * [simplify]: Extracting #1: cost 40 inf + 0 3.883 * * [simplify]: Extracting #2: cost 283 inf + 0 3.888 * * [simplify]: Extracting #3: cost 411 inf + 35676 3.903 * * [simplify]: Extracting #4: cost 171 inf + 301659 3.932 * * [simplify]: Extracting #5: cost 71 inf + 492019 3.967 * * [simplify]: Extracting #6: cost 2 inf + 616990 4.003 * * [simplify]: Extracting #7: cost 0 inf + 622758 4.038 * [simplify]: Simplified to (*.p16 (neg.p16 b) (*.p16 (-.p16 (/.p16 (+.p16 (+.p16 b a) c) (real->posit16 2)) a) (/.p16 (+.p16 (+.p16 b a) c) (real->posit16 2)))) 4.038 * [simplify]: Simplified (2 1 1 2) to (λ (a b c) (sqrt.p16 (*.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 a b) c) (real->posit16 2))) (*.p16 (neg.p16 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 a b) c) (real->posit16 2)) c)))) 4.039 * * * * [progress]: [ 8 / 17 ] simplifiying candidate #posit16 2)) (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) a))) (*.p16 (neg.p16 b) (*.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)) c))))> 4.039 * [simplify]: Simplifying (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) a))) 4.039 * * [simplify]: iters left: 6 (11 enodes) 4.042 * * [simplify]: iters left: 5 (36 enodes) 4.048 * * [simplify]: iters left: 4 (93 enodes) 4.075 * * [simplify]: iters left: 3 (390 enodes) 4.434 * * [simplify]: Extracting #0: cost 1 inf + 0 4.434 * * [simplify]: Extracting #1: cost 44 inf + 0 4.436 * * [simplify]: Extracting #2: cost 324 inf + 0 4.442 * * [simplify]: Extracting #3: cost 576 inf + 34479 4.484 * * [simplify]: Extracting #4: cost 260 inf + 444609 4.575 * * [simplify]: Extracting #5: cost 4 inf + 812472 4.666 * * [simplify]: Extracting #6: cost 0 inf + 821045 4.760 * [simplify]: Simplified to (*.p16 (*.p16 (-.p16 (/.p16 (+.p16 (+.p16 b a) c) (real->posit16 2)) a) (/.p16 (+.p16 (+.p16 b a) c) (real->posit16 2))) (/.p16 (+.p16 (+.p16 b a) c) (real->posit16 2))) 4.760 * [simplify]: Simplified (2 1 1 1) to (λ (a b c) (sqrt.p16 (*.p16 (+.p16 (*.p16 (*.p16 (-.p16 (/.p16 (+.p16 (+.p16 b a) c) (real->posit16 2)) a) (/.p16 (+.p16 (+.p16 b a) c) (real->posit16 2))) (/.p16 (+.p16 (+.p16 b a) c) (real->posit16 2))) (*.p16 (neg.p16 b) (*.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)) c)))) 4.760 * [simplify]: Simplifying (*.p16 (neg.p16 b) (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) a))) 4.761 * * [simplify]: iters left: 6 (12 enodes) 4.766 * * [simplify]: iters left: 5 (36 enodes) 4.780 * * [simplify]: iters left: 4 (94 enodes) 4.826 * * [simplify]: iters left: 3 (374 enodes) 5.146 * * [simplify]: Extracting #0: cost 1 inf + 0 5.146 * * [simplify]: Extracting #1: cost 43 inf + 0 5.148 * * [simplify]: Extracting #2: cost 304 inf + 0 5.153 * * [simplify]: Extracting #3: cost 438 inf + 30239 5.188 * * [simplify]: Extracting #4: cost 124 inf + 416568 5.228 * * [simplify]: Extracting #5: cost 24 inf + 620451 5.264 * * [simplify]: Extracting #6: cost 0 inf + 654867 5.327 * [simplify]: Simplified to (*.p16 (neg.p16 b) (*.p16 (/.p16 (+.p16 c (+.p16 a b)) (real->posit16 2)) (-.p16 (/.p16 (+.p16 c (+.p16 a b)) (real->posit16 2)) a))) 5.327 * [simplify]: Simplified (2 1 1 2) to (λ (a b c) (sqrt.p16 (*.p16 (+.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) a))) (*.p16 (neg.p16 b) (*.p16 (/.p16 (+.p16 c (+.p16 a b)) (real->posit16 2)) (-.p16 (/.p16 (+.p16 c (+.p16 a b)) (real->posit16 2)) a)))) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) c)))) 5.328 * * * * [progress]: [ 9 / 17 ] simplifiying candidate #posit16 2)) (*.p16 (-.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))))> 5.328 * [simplify]: Simplifying (*.p16 (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) a) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) b)) 5.328 * * [simplify]: iters left: 5 (11 enodes) 5.331 * * [simplify]: iters left: 4 (36 enodes) 5.337 * * [simplify]: iters left: 3 (85 enodes) 5.356 * * [simplify]: iters left: 2 (286 enodes) 5.483 * * [simplify]: Extracting #0: cost 1 inf + 0 5.483 * * [simplify]: Extracting #1: cost 64 inf + 0 5.485 * * [simplify]: Extracting #2: cost 296 inf + 0 5.488 * * [simplify]: Extracting #3: cost 414 inf + 1288 5.501 * * [simplify]: Extracting #4: cost 288 inf + 175558 5.553 * * [simplify]: Extracting #5: cost 49 inf + 536188 5.598 * * [simplify]: Extracting #6: cost 0 inf + 628584 5.637 * * [simplify]: Extracting #7: cost 0 inf + 627824 5.703 * [simplify]: Simplified to (*.p16 (-.p16 (/.p16 (+.p16 (+.p16 b a) c) (real->posit16 2)) a) (-.p16 (/.p16 (+.p16 (+.p16 b a) c) (real->posit16 2)) b)) 5.703 * [simplify]: Simplified (2 1 1 2) to (λ (a b c) (sqrt.p16 (*.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (*.p16 (-.p16 (/.p16 (+.p16 (+.p16 b a) c) (real->posit16 2)) a) (-.p16 (/.p16 (+.p16 (+.p16 b a) c) (real->posit16 2)) b))) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) c)))) 5.703 * * * * [progress]: [ 10 / 17 ] simplifiying candidate #posit16 2)) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) a)) (-.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (/.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.704 * [simplify]: Simplifying (*.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) a)) (-.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2))) (*.p16 b b))) 5.704 * * [simplify]: iters left: 6 (14 enodes) 5.707 * * [simplify]: iters left: 5 (51 enodes) 5.719 * * [simplify]: iters left: 4 (171 enodes) 5.794 * * [simplify]: Extracting #0: cost 1 inf + 0 5.794 * * [simplify]: Extracting #1: cost 46 inf + 0 5.795 * * [simplify]: Extracting #2: cost 203 inf + 0 5.797 * * [simplify]: Extracting #3: cost 243 inf + 32533 5.811 * * [simplify]: Extracting #4: cost 117 inf + 241265 5.844 * * [simplify]: Extracting #5: cost 6 inf + 400335 5.885 * * [simplify]: Extracting #6: cost 0 inf + 412799 5.928 * [simplify]: Simplified to (*.p16 (-.p16 (/.p16 (+.p16 (+.p16 b a) c) (real->posit16 2)) a) (*.p16 (-.p16 (/.p16 (+.p16 (+.p16 b a) c) (real->posit16 2)) b) (*.p16 (+.p16 (/.p16 (+.p16 (+.p16 b a) c) (real->posit16 2)) b) (/.p16 (+.p16 (+.p16 b a) c) (real->posit16 2))))) 5.929 * [simplify]: Simplified (2 1 1 1) to (λ (a b c) (sqrt.p16 (*.p16 (/.p16 (*.p16 (-.p16 (/.p16 (+.p16 (+.p16 b a) c) (real->posit16 2)) a) (*.p16 (-.p16 (/.p16 (+.p16 (+.p16 b a) c) (real->posit16 2)) b) (*.p16 (+.p16 (/.p16 (+.p16 (+.p16 b a) c) (real->posit16 2)) b) (/.p16 (+.p16 (+.p16 b a) c) (real->posit16 2))))) (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) b)) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) c)))) 5.929 * * * * [progress]: [ 11 / 17 ] simplifiying candidate #posit16 2)) (-.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)) a)) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) c))))> 5.929 * [simplify]: Simplifying (*.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (-.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)) 5.929 * * [simplify]: iters left: 6 (14 enodes) 5.933 * * [simplify]: iters left: 5 (51 enodes) 5.943 * * [simplify]: iters left: 4 (173 enodes) 6.013 * * [simplify]: Extracting #0: cost 1 inf + 0 6.013 * * [simplify]: Extracting #1: cost 48 inf + 0 6.014 * * [simplify]: Extracting #2: cost 196 inf + 0 6.016 * * [simplify]: Extracting #3: cost 239 inf + 46998 6.035 * * [simplify]: Extracting #4: cost 95 inf + 284642 6.076 * * [simplify]: Extracting #5: cost 4 inf + 421483 6.100 * * [simplify]: Extracting #6: cost 0 inf + 428092 6.124 * [simplify]: Simplified to (*.p16 (*.p16 (+.p16 a (/.p16 (+.p16 (+.p16 b a) c) (real->posit16 2))) (-.p16 (/.p16 (+.p16 (+.p16 b a) c) (real->posit16 2)) a)) (*.p16 (/.p16 (+.p16 (+.p16 b a) c) (real->posit16 2)) (-.p16 (/.p16 (+.p16 (+.p16 b a) c) (real->posit16 2)) b))) 6.124 * [simplify]: Simplified (2 1 1 1) to (λ (a b c) (sqrt.p16 (*.p16 (/.p16 (*.p16 (*.p16 (+.p16 a (/.p16 (+.p16 (+.p16 b a) c) (real->posit16 2))) (-.p16 (/.p16 (+.p16 (+.p16 b a) c) (real->posit16 2)) a)) (*.p16 (/.p16 (+.p16 (+.p16 b a) c) (real->posit16 2)) (-.p16 (/.p16 (+.p16 (+.p16 b a) c) (real->posit16 2)) b))) (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) a)) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) c)))) 6.124 * * * * [progress]: [ 12 / 17 ] simplifiying candidate #posit16 2)) a)) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) b)) (real->posit16 2)) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) c))))> 6.124 * [simplify]: Simplifying (*.p16 (*.p16 (+.p16 (+.p16 a b) c) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) a)) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) b)) 6.124 * * [simplify]: iters left: 6 (12 enodes) 6.127 * * [simplify]: iters left: 5 (40 enodes) 6.135 * * [simplify]: iters left: 4 (117 enodes) 6.200 * * [simplify]: Extracting #0: cost 1 inf + 0 6.200 * * [simplify]: Extracting #1: cost 47 inf + 0 6.201 * * [simplify]: Extracting #2: cost 171 inf + 0 6.201 * * [simplify]: Extracting #3: cost 247 inf + 1577 6.204 * * [simplify]: Extracting #4: cost 187 inf + 58448 6.216 * * [simplify]: Extracting #5: cost 28 inf + 257133 6.236 * * [simplify]: Extracting #6: cost 4 inf + 293508 6.262 * * [simplify]: Extracting #7: cost 0 inf + 302484 6.287 * [simplify]: Simplified to (*.p16 (-.p16 (/.p16 (+.p16 (+.p16 b a) c) (real->posit16 2)) b) (*.p16 (+.p16 (+.p16 b a) c) (-.p16 (/.p16 (+.p16 (+.p16 b a) c) (real->posit16 2)) a))) 6.287 * [simplify]: Simplified (2 1 1 1) to (λ (a b c) (sqrt.p16 (*.p16 (/.p16 (*.p16 (-.p16 (/.p16 (+.p16 (+.p16 b a) c) (real->posit16 2)) b) (*.p16 (+.p16 (+.p16 b a) c) (-.p16 (/.p16 (+.p16 (+.p16 b a) c) (real->posit16 2)) a))) (real->posit16 2)) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) c)))) 6.287 * * * * [progress]: [ 13 / 17 ] simplifiying candidate #posit16 2)) b) (*.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)) c))))> 6.287 * * * * [progress]: [ 14 / 17 ] 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))))> 6.288 * [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))) 6.288 * * [simplify]: iters left: 6 (15 enodes) 6.291 * * [simplify]: iters left: 5 (54 enodes) 6.302 * * [simplify]: iters left: 4 (174 enodes) 6.389 * * [simplify]: Extracting #0: cost 1 inf + 0 6.389 * * [simplify]: Extracting #1: cost 2 inf + 0 6.389 * * [simplify]: Extracting #2: cost 52 inf + 0 6.389 * * [simplify]: Extracting #3: cost 218 inf + 0 6.390 * * [simplify]: Extracting #4: cost 350 inf + 488 6.395 * * [simplify]: Extracting #5: cost 271 inf + 83278 6.408 * * [simplify]: Extracting #6: cost 99 inf + 301152 6.436 * * [simplify]: Extracting #7: cost 13 inf + 445414 6.474 * * [simplify]: Extracting #8: cost 0 inf + 471346 6.503 * [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))) 6.503 * [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)))) 6.503 * * * * [progress]: [ 15 / 17 ] 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))))> 6.503 * [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))) 6.503 * * [simplify]: iters left: 6 (15 enodes) 6.507 * * [simplify]: iters left: 5 (54 enodes) 6.517 * * [simplify]: iters left: 4 (174 enodes) 6.615 * * [simplify]: Extracting #0: cost 1 inf + 0 6.615 * * [simplify]: Extracting #1: cost 2 inf + 0 6.615 * * [simplify]: Extracting #2: cost 52 inf + 0 6.618 * * [simplify]: Extracting #3: cost 218 inf + 0 6.620 * * [simplify]: Extracting #4: cost 350 inf + 488 6.624 * * [simplify]: Extracting #5: cost 271 inf + 83278 6.641 * * [simplify]: Extracting #6: cost 99 inf + 301152 6.686 * * [simplify]: Extracting #7: cost 13 inf + 445414 6.713 * * [simplify]: Extracting #8: cost 0 inf + 471346 6.759 * [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))) 6.759 * [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)))) 6.759 * * * * [progress]: [ 16 / 17 ] 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))))> 6.759 * [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))) 6.759 * * [simplify]: iters left: 6 (15 enodes) 6.763 * * [simplify]: iters left: 5 (54 enodes) 6.773 * * [simplify]: iters left: 4 (174 enodes) 6.891 * * [simplify]: Extracting #0: cost 1 inf + 0 6.891 * * [simplify]: Extracting #1: cost 2 inf + 0 6.891 * * [simplify]: Extracting #2: cost 52 inf + 0 6.892 * * [simplify]: Extracting #3: cost 218 inf + 0 6.894 * * [simplify]: Extracting #4: cost 350 inf + 488 6.902 * * [simplify]: Extracting #5: cost 271 inf + 83278 6.929 * * [simplify]: Extracting #6: cost 99 inf + 301152 6.978 * * [simplify]: Extracting #7: cost 13 inf + 445414 7.021 * * [simplify]: Extracting #8: cost 0 inf + 471346 7.050 * [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))) 7.050 * [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)))) 7.050 * * * * [progress]: [ 17 / 17 ] 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))))> 7.050 * [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))) 7.050 * * [simplify]: iters left: 6 (15 enodes) 7.054 * * [simplify]: iters left: 5 (54 enodes) 7.065 * * [simplify]: iters left: 4 (174 enodes) 7.140 * * [simplify]: Extracting #0: cost 1 inf + 0 7.140 * * [simplify]: Extracting #1: cost 2 inf + 0 7.140 * * [simplify]: Extracting #2: cost 52 inf + 0 7.141 * * [simplify]: Extracting #3: cost 218 inf + 0 7.142 * * [simplify]: Extracting #4: cost 350 inf + 488 7.146 * * [simplify]: Extracting #5: cost 271 inf + 83278 7.163 * * [simplify]: Extracting #6: cost 99 inf + 301152 7.209 * * [simplify]: Extracting #7: cost 13 inf + 445414 7.260 * * [simplify]: Extracting #8: cost 0 inf + 471346 7.298 * [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))) 7.298 * [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)))) 7.298 * * * [progress]: adding candidates to table 7.919 * * [progress]: iteration 2 / 4 7.919 * * * [progress]: picking best candidate 7.975 * * * * [pick]: Picked #posit16 2)) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) a)) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) b)) (/.p16 (-.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2))) (*.p16 c c)) (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) c)))))> 7.975 * * * [progress]: localizing error 8.366 * * * [progress]: generating rewritten candidates 8.366 * * * * [progress]: [ 1 / 4 ] rewriting at (2 1 2) 8.436 * * * * [progress]: [ 2 / 4 ] rewriting at (2 1 1 2) 8.461 * * * * [progress]: [ 3 / 4 ] rewriting at (2 1 1 1 2) 8.487 * * * * [progress]: [ 4 / 4 ] rewriting at (2 1 2 1) 8.490 * * * [progress]: generating series expansions 8.490 * * * * [progress]: [ 1 / 4 ] generating series at (2 1 2) 8.490 * * * * [progress]: [ 2 / 4 ] generating series at (2 1 1 2) 8.490 * * * * [progress]: [ 3 / 4 ] generating series at (2 1 1 1 2) 8.490 * * * * [progress]: [ 4 / 4 ] generating series at (2 1 2 1) 8.490 * * * [progress]: simplifying candidates 8.490 * * * * [progress]: [ 1 / 13 ] simplifiying candidate #posit16 2)) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) a)) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) b)) (/.p16 (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) c) (/.p16 (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) c) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) c))))))> 8.491 * [simplify]: Simplifying (/.p16 (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) c) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) c)) 8.491 * * [simplify]: iters left: 5 (11 enodes) 8.494 * * [simplify]: iters left: 4 (29 enodes) 8.499 * * [simplify]: iters left: 3 (50 enodes) 8.514 * * [simplify]: iters left: 2 (136 enodes) 8.567 * * [simplify]: Extracting #0: cost 1 inf + 0 8.567 * * [simplify]: Extracting #1: cost 19 inf + 0 8.568 * * [simplify]: Extracting #2: cost 68 inf + 0 8.568 * * [simplify]: Extracting #3: cost 105 inf + 404 8.568 * * [simplify]: Extracting #4: cost 144 inf + 3212 8.569 * * [simplify]: Extracting #5: cost 141 inf + 17509 8.573 * * [simplify]: Extracting #6: cost 62 inf + 102535 8.586 * * [simplify]: Extracting #7: cost 9 inf + 195869 8.598 * * [simplify]: Extracting #8: cost 0 inf + 216465 8.609 * * [simplify]: Extracting #9: cost 0 inf + 216025 8.623 * [simplify]: Simplified to (/.p16 (+.p16 c (/.p16 (+.p16 b (+.p16 a c)) (real->posit16 2))) (-.p16 (/.p16 (+.p16 b (+.p16 a c)) (real->posit16 2)) c)) 8.623 * [simplify]: Simplified (2 1 2 2) to (λ (a b c) (sqrt.p16 (*.p16 (*.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) a)) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) b)) (/.p16 (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) c) (/.p16 (+.p16 c (/.p16 (+.p16 b (+.p16 a c)) (real->posit16 2))) (-.p16 (/.p16 (+.p16 b (+.p16 a c)) (real->posit16 2)) c)))))) 8.623 * * * * [progress]: [ 2 / 13 ] simplifiying candidate #posit16 2)) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) a)) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) b)) (/.p16 (-.p16 (*.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2))) (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)))) (*.p16 (*.p16 c c) (*.p16 c c))) (*.p16 (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) c) (+.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2))) (*.p16 c c)))))))> 8.623 * [simplify]: Simplifying (*.p16 (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) c) (+.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2))) (*.p16 c c))) 8.623 * * [simplify]: iters left: 6 (13 enodes) 8.626 * * [simplify]: iters left: 5 (37 enodes) 8.634 * * [simplify]: iters left: 4 (103 enodes) 8.657 * * [simplify]: iters left: 3 (299 enodes) 8.782 * * [simplify]: Extracting #0: cost 1 inf + 0 8.782 * * [simplify]: Extracting #1: cost 15 inf + 0 8.783 * * [simplify]: Extracting #2: cost 76 inf + 0 8.784 * * [simplify]: Extracting #3: cost 225 inf + 1 8.789 * * [simplify]: Extracting #4: cost 218 inf + 50046 8.800 * * [simplify]: Extracting #5: cost 20 inf + 255793 8.823 * * [simplify]: Extracting #6: cost 0 inf + 279953 8.846 * [simplify]: Simplified to (*.p16 (+.p16 c (/.p16 (+.p16 (+.p16 b a) c) (real->posit16 2))) (+.p16 (*.p16 c c) (*.p16 (/.p16 (+.p16 (+.p16 b a) c) (real->posit16 2)) (/.p16 (+.p16 (+.p16 b a) c) (real->posit16 2))))) 8.846 * [simplify]: Simplified (2 1 2 2) to (λ (a b c) (sqrt.p16 (*.p16 (*.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) a)) (-.p16 (/.p16 (+.p16 (+.p16 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 c (/.p16 (+.p16 (+.p16 b a) c) (real->posit16 2))) (+.p16 (*.p16 c c) (*.p16 (/.p16 (+.p16 (+.p16 b a) c) (real->posit16 2)) (/.p16 (+.p16 (+.p16 b a) c) (real->posit16 2))))))))) 8.846 * * * * [progress]: [ 3 / 13 ] simplifiying candidate #posit16 2)) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) a)) (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (neg.p16 b))) (/.p16 (-.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2))) (*.p16 c c)) (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) c)))))> 8.846 * [simplify]: Simplifying (neg.p16 b) 8.846 * * [simplify]: iters left: 1 (2 enodes) 8.847 * * [simplify]: Extracting #0: cost 1 inf + 0 8.847 * * [simplify]: Extracting #1: cost 2 inf + 0 8.847 * * [simplify]: Extracting #2: cost 1 inf + 1 8.847 * * [simplify]: Extracting #3: cost 0 inf + 82 8.847 * [simplify]: Simplified to (neg.p16 b) 8.847 * [simplify]: Simplified (2 1 1 2 2) to (λ (a b c) (sqrt.p16 (*.p16 (*.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) a)) (+.p16 (/.p16 (+.p16 (+.p16 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))))) 8.847 * * * * [progress]: [ 4 / 13 ] simplifiying candidate #posit16 2)) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) a)) (/.p16 (-.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2))) (*.p16 b b)) (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) b))) (/.p16 (-.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2))) (*.p16 c c)) (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) c)))))> 8.847 * [simplify]: Simplifying (-.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2))) (*.p16 b b)) 8.847 * * [simplify]: iters left: 5 (11 enodes) 8.850 * * [simplify]: iters left: 4 (36 enodes) 8.857 * * [simplify]: iters left: 3 (93 enodes) 8.883 * * [simplify]: iters left: 2 (310 enodes) 9.059 * * [simplify]: Extracting #0: cost 1 inf + 0 9.059 * * [simplify]: Extracting #1: cost 32 inf + 0 9.059 * * [simplify]: Extracting #2: cost 177 inf + 0 9.060 * * [simplify]: Extracting #3: cost 260 inf + 323 9.062 * * [simplify]: Extracting #4: cost 456 inf + 5597 9.072 * * [simplify]: Extracting #5: cost 278 inf + 236939 9.124 * * [simplify]: Extracting #6: cost 27 inf + 652788 9.210 * * [simplify]: Extracting #7: cost 2 inf + 706688 9.267 * * [simplify]: Extracting #8: cost 0 inf + 713376 9.339 * [simplify]: Simplified to (*.p16 (+.p16 (/.p16 (+.p16 (+.p16 b a) c) (real->posit16 2)) b) (-.p16 (/.p16 (+.p16 (+.p16 b a) c) (real->posit16 2)) b)) 9.339 * [simplify]: Simplified (2 1 1 2 1) to (λ (a b c) (sqrt.p16 (*.p16 (*.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) a)) (/.p16 (*.p16 (+.p16 (/.p16 (+.p16 (+.p16 b a) c) (real->posit16 2)) b) (-.p16 (/.p16 (+.p16 (+.p16 b a) c) (real->posit16 2)) b)) (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) b))) (/.p16 (-.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2))) (*.p16 c c)) (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) c))))) 9.339 * [simplify]: Simplifying (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) b) 9.340 * * [simplify]: iters left: 4 (9 enodes) 9.343 * * [simplify]: iters left: 3 (21 enodes) 9.349 * * [simplify]: iters left: 2 (27 enodes) 9.355 * * [simplify]: iters left: 1 (28 enodes) 9.362 * * [simplify]: Extracting #0: cost 1 inf + 0 9.362 * * [simplify]: Extracting #1: cost 3 inf + 0 9.362 * * [simplify]: Extracting #2: cost 4 inf + 1 9.362 * * [simplify]: Extracting #3: cost 10 inf + 1 9.362 * * [simplify]: Extracting #4: cost 5 inf + 47 9.362 * * [simplify]: Extracting #5: cost 1 inf + 738 9.362 * * [simplify]: Extracting #6: cost 0 inf + 1302 9.363 * [simplify]: Simplified to (+.p16 (/.p16 (+.p16 a (+.p16 c b)) (real->posit16 2)) b) 9.363 * [simplify]: Simplified (2 1 1 2 2) to (λ (a b c) (sqrt.p16 (*.p16 (*.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) a)) (/.p16 (-.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2))) (*.p16 b b)) (+.p16 (/.p16 (+.p16 a (+.p16 c b)) (real->posit16 2)) b))) (/.p16 (-.p16 (*.p16 (/.p16 (+.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))))) 9.363 * * * * [progress]: [ 5 / 13 ] simplifiying candidate #posit16 2)) (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (neg.p16 a))) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) b)) (/.p16 (-.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2))) (*.p16 c c)) (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) c)))))> 9.363 * [simplify]: Simplifying (neg.p16 a) 9.363 * * [simplify]: iters left: 1 (2 enodes) 9.364 * * [simplify]: Extracting #0: cost 1 inf + 0 9.364 * * [simplify]: Extracting #1: cost 2 inf + 0 9.364 * * [simplify]: Extracting #2: cost 1 inf + 1 9.364 * * [simplify]: Extracting #3: cost 0 inf + 82 9.364 * [simplify]: Simplified to (neg.p16 a) 9.364 * [simplify]: Simplified (2 1 1 1 2 2) to (λ (a b c) (sqrt.p16 (*.p16 (*.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (neg.p16 a))) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) b)) (/.p16 (-.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2))) (*.p16 c c)) (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) c))))) 9.364 * * * * [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 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)))))> 9.364 * [simplify]: Simplifying (-.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2))) (*.p16 a a)) 9.364 * * [simplify]: iters left: 5 (11 enodes) 9.367 * * [simplify]: iters left: 4 (36 enodes) 9.374 * * [simplify]: iters left: 3 (93 enodes) 9.394 * * [simplify]: iters left: 2 (310 enodes) 9.558 * * [simplify]: Extracting #0: cost 1 inf + 0 9.558 * * [simplify]: Extracting #1: cost 32 inf + 0 9.558 * * [simplify]: Extracting #2: cost 177 inf + 0 9.559 * * [simplify]: Extracting #3: cost 262 inf + 323 9.562 * * [simplify]: Extracting #4: cost 416 inf + 51663 9.587 * * [simplify]: Extracting #5: cost 116 inf + 501475 9.626 * * [simplify]: Extracting #6: cost 0 inf + 713857 9.667 * * [simplify]: Extracting #7: cost 0 inf + 713577 9.736 * [simplify]: Simplified to (*.p16 (+.p16 a (/.p16 (+.p16 (+.p16 b a) c) (real->posit16 2))) (-.p16 (/.p16 (+.p16 (+.p16 b a) c) (real->posit16 2)) a)) 9.736 * [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 a (/.p16 (+.p16 (+.p16 b a) c) (real->posit16 2))) (-.p16 (/.p16 (+.p16 (+.p16 b 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))))) 9.736 * [simplify]: Simplifying (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) a) 9.736 * * [simplify]: iters left: 4 (9 enodes) 9.740 * * [simplify]: iters left: 3 (21 enodes) 9.746 * * [simplify]: iters left: 2 (27 enodes) 9.753 * * [simplify]: iters left: 1 (28 enodes) 9.760 * * [simplify]: Extracting #0: cost 1 inf + 0 9.760 * * [simplify]: Extracting #1: cost 3 inf + 0 9.760 * * [simplify]: Extracting #2: cost 4 inf + 1 9.761 * * [simplify]: Extracting #3: cost 10 inf + 1 9.761 * * [simplify]: Extracting #4: cost 1 inf + 738 9.761 * * [simplify]: Extracting #5: cost 0 inf + 1302 9.761 * [simplify]: Simplified to (+.p16 a (/.p16 (+.p16 (+.p16 b a) c) (real->posit16 2))) 9.761 * [simplify]: Simplified (2 1 1 1 2 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 a (/.p16 (+.p16 (+.p16 b a) c) (real->posit16 2))))) (-.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))))) 9.762 * * * * [progress]: [ 7 / 13 ] simplifiying candidate #posit16 2)) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) a)) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) b)) (/.p16 (*.p16 (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) c) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) c)) (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) c)))))> 9.762 * [simplify]: Simplifying (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) c) 9.762 * * [simplify]: iters left: 4 (9 enodes) 9.766 * * [simplify]: iters left: 3 (21 enodes) 9.772 * * [simplify]: iters left: 2 (27 enodes) 9.779 * * [simplify]: iters left: 1 (28 enodes) 9.787 * * [simplify]: Extracting #0: cost 1 inf + 0 9.787 * * [simplify]: Extracting #1: cost 3 inf + 0 9.787 * * [simplify]: Extracting #2: cost 4 inf + 1 9.787 * * [simplify]: Extracting #3: cost 10 inf + 1 9.787 * * [simplify]: Extracting #4: cost 5 inf + 47 9.787 * * [simplify]: Extracting #5: cost 1 inf + 738 9.787 * * [simplify]: Extracting #6: cost 0 inf + 1302 9.788 * [simplify]: Simplified to (+.p16 c (/.p16 (+.p16 a (+.p16 c b)) (real->posit16 2))) 9.788 * [simplify]: Simplified (2 1 2 1 1) to (λ (a b c) (sqrt.p16 (*.p16 (*.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) a)) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) b)) (/.p16 (*.p16 (+.p16 c (/.p16 (+.p16 a (+.p16 c b)) (real->posit16 2))) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) c)) (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) c))))) 9.788 * [simplify]: Simplifying (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) c) 9.788 * * [simplify]: iters left: 4 (9 enodes) 9.792 * * [simplify]: iters left: 3 (27 enodes) 9.800 * * [simplify]: iters left: 2 (47 enodes) 9.817 * * [simplify]: iters left: 1 (123 enodes) 9.876 * * [simplify]: Extracting #0: cost 1 inf + 0 9.876 * * [simplify]: Extracting #1: cost 15 inf + 0 9.877 * * [simplify]: Extracting #2: cost 52 inf + 82 9.877 * * [simplify]: Extracting #3: cost 87 inf + 1044 9.878 * * [simplify]: Extracting #4: cost 138 inf + 5615 9.880 * * [simplify]: Extracting #5: cost 116 inf + 19272 9.886 * * [simplify]: Extracting #6: cost 57 inf + 78898 9.901 * * [simplify]: Extracting #7: cost 8 inf + 156974 9.918 * * [simplify]: Extracting #8: cost 0 inf + 175966 9.935 * [simplify]: Simplified to (-.p16 (/.p16 (+.p16 b (+.p16 a c)) (real->posit16 2)) c) 9.935 * [simplify]: Simplified (2 1 2 1 2) to (λ (a b c) (sqrt.p16 (*.p16 (*.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) a)) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) b)) (/.p16 (*.p16 (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) c) (-.p16 (/.p16 (+.p16 b (+.p16 a c)) (real->posit16 2)) c)) (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) c))))) 9.935 * * * * [progress]: [ 8 / 13 ] simplifiying candidate #posit16 2)) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) a)) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) b)) (/.p16 (+.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2))) (neg.p16 (*.p16 c c))) (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) c)))))> 9.935 * [simplify]: Simplifying (neg.p16 (*.p16 c c)) 9.936 * * [simplify]: iters left: 2 (3 enodes) 9.937 * * [simplify]: iters left: 1 (5 enodes) 9.938 * * [simplify]: Extracting #0: cost 1 inf + 0 9.938 * * [simplify]: Extracting #1: cost 2 inf + 0 9.938 * * [simplify]: Extracting #2: cost 3 inf + 0 9.938 * * [simplify]: Extracting #3: cost 2 inf + 1 9.938 * * [simplify]: Extracting #4: cost 0 inf + 723 9.939 * [simplify]: Simplified to (neg.p16 (*.p16 c c)) 9.939 * [simplify]: Simplified (2 1 2 1 2) to (λ (a b c) (sqrt.p16 (*.p16 (*.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) a)) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) b)) (/.p16 (+.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2))) (neg.p16 (*.p16 c c))) (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) c))))) 9.939 * * * * [progress]: [ 9 / 13 ] simplifiying candidate #posit16 2)) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) a)) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) b)) (/.p16 (/.p16 (-.p16 (*.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2))) (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)))) (*.p16 (*.p16 c c) (*.p16 c c))) (+.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2))) (*.p16 c c))) (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) c)))))> 9.939 * [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))) 9.939 * * [simplify]: iters left: 6 (13 enodes) 9.946 * * [simplify]: iters left: 5 (46 enodes) 9.963 * * [simplify]: iters left: 4 (130 enodes) 10.029 * * [simplify]: Extracting #0: cost 1 inf + 0 10.029 * * [simplify]: Extracting #1: cost 25 inf + 0 10.030 * * [simplify]: Extracting #2: cost 62 inf + 0 10.030 * * [simplify]: Extracting #3: cost 156 inf + 82 10.032 * * [simplify]: Extracting #4: cost 155 inf + 20973 10.042 * * [simplify]: Extracting #5: cost 51 inf + 151607 10.061 * * [simplify]: Extracting #6: cost 3 inf + 236996 10.073 * * [simplify]: Extracting #7: cost 0 inf + 246088 10.085 * [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))) 10.085 * [simplify]: Simplified (2 1 2 1 1) to (λ (a b c) (sqrt.p16 (*.p16 (*.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) a)) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) b)) (/.p16 (/.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)) (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2))) (*.p16 c c))) (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) c))))) 10.086 * [simplify]: Simplifying (+.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2))) (*.p16 c c)) 10.086 * * [simplify]: iters left: 5 (11 enodes) 10.090 * * [simplify]: iters left: 4 (27 enodes) 10.095 * * [simplify]: iters left: 3 (53 enodes) 10.111 * * [simplify]: iters left: 2 (121 enodes) 10.143 * * [simplify]: iters left: 1 (313 enodes) 10.316 * * [simplify]: Extracting #0: cost 1 inf + 0 10.316 * * [simplify]: Extracting #1: cost 21 inf + 0 10.316 * * [simplify]: Extracting #2: cost 48 inf + 0 10.317 * * [simplify]: Extracting #3: cost 201 inf + 324 10.321 * * [simplify]: Extracting #4: cost 143 inf + 47287 10.329 * * [simplify]: Extracting #5: cost 17 inf + 136312 10.338 * * [simplify]: Extracting #6: cost 0 inf + 151168 10.358 * [simplify]: Simplified to (+.p16 (*.p16 c c) (*.p16 (/.p16 (+.p16 (+.p16 b a) c) (real->posit16 2)) (/.p16 (+.p16 (+.p16 b a) c) (real->posit16 2)))) 10.358 * [simplify]: Simplified (2 1 2 1 2) to (λ (a b c) (sqrt.p16 (*.p16 (*.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) a)) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) b)) (/.p16 (/.p16 (-.p16 (*.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2))) (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)))) (*.p16 (*.p16 c c) (*.p16 c c))) (+.p16 (*.p16 c c) (*.p16 (/.p16 (+.p16 (+.p16 b a) c) (real->posit16 2)) (/.p16 (+.p16 (+.p16 b a) c) (real->posit16 2))))) (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) c))))) 10.358 * * * * [progress]: [ 10 / 13 ] simplifiying candidate #posit16 2)) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) a)) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) b)) (/.p16 (-.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2))) (*.p16 c c)) (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) c)))))> 10.359 * [simplify]: Simplifying (-.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2))) (*.p16 c c)) 10.359 * * [simplify]: iters left: 5 (11 enodes) 10.364 * * [simplify]: iters left: 4 (36 enodes) 10.376 * * [simplify]: iters left: 3 (93 enodes) 10.411 * * [simplify]: iters left: 2 (310 enodes) 10.580 * * [simplify]: Extracting #0: cost 1 inf + 0 10.580 * * [simplify]: Extracting #1: cost 32 inf + 0 10.580 * * [simplify]: Extracting #2: cost 177 inf + 0 10.581 * * [simplify]: Extracting #3: cost 262 inf + 323 10.584 * * [simplify]: Extracting #4: cost 417 inf + 52622 10.604 * * [simplify]: Extracting #5: cost 157 inf + 465463 10.652 * * [simplify]: Extracting #6: cost 2 inf + 707329 10.703 * * [simplify]: Extracting #7: cost 0 inf + 711417 10.771 * [simplify]: Simplified to (*.p16 (+.p16 c (/.p16 (+.p16 (+.p16 b a) c) (real->posit16 2))) (-.p16 (/.p16 (+.p16 (+.p16 b a) c) (real->posit16 2)) c)) 10.771 * [simplify]: Simplified (2 1 2 1) to (λ (a b c) (sqrt.p16 (*.p16 (*.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) a)) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) b)) (/.p16 (*.p16 (+.p16 c (/.p16 (+.p16 (+.p16 b a) c) (real->posit16 2))) (-.p16 (/.p16 (+.p16 (+.p16 b a) c) (real->posit16 2)) c)) (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) c))))) 10.771 * [simplify]: Simplifying (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) c) 10.771 * * [simplify]: iters left: 4 (9 enodes) 10.775 * * [simplify]: iters left: 3 (21 enodes) 10.781 * * [simplify]: iters left: 2 (27 enodes) 10.787 * * [simplify]: iters left: 1 (28 enodes) 10.794 * * [simplify]: Extracting #0: cost 1 inf + 0 10.794 * * [simplify]: Extracting #1: cost 3 inf + 0 10.794 * * [simplify]: Extracting #2: cost 4 inf + 1 10.794 * * [simplify]: Extracting #3: cost 10 inf + 1 10.794 * * [simplify]: Extracting #4: cost 5 inf + 47 10.794 * * [simplify]: Extracting #5: cost 1 inf + 738 10.795 * * [simplify]: Extracting #6: cost 0 inf + 1302 10.795 * [simplify]: Simplified to (+.p16 c (/.p16 (+.p16 a (+.p16 c b)) (real->posit16 2))) 10.795 * [simplify]: Simplified (2 1 2 2) to (λ (a b c) (sqrt.p16 (*.p16 (*.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) a)) (-.p16 (/.p16 (+.p16 (+.p16 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 c (/.p16 (+.p16 a (+.p16 c b)) (real->posit16 2))))))) 10.795 * * * * [progress]: [ 11 / 13 ] simplifiying candidate #posit16 2)) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) a)) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) b)) (/.p16 (-.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2))) (*.p16 c c)) (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) c)))))> 10.795 * [simplify]: Simplifying (-.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2))) (*.p16 c c)) 10.796 * * [simplify]: iters left: 5 (11 enodes) 10.800 * * [simplify]: iters left: 4 (36 enodes) 10.811 * * [simplify]: iters left: 3 (93 enodes) 10.846 * * [simplify]: iters left: 2 (310 enodes) 11.006 * * [simplify]: Extracting #0: cost 1 inf + 0 11.006 * * [simplify]: Extracting #1: cost 32 inf + 0 11.007 * * [simplify]: Extracting #2: cost 177 inf + 0 11.008 * * [simplify]: Extracting #3: cost 262 inf + 323 11.011 * * [simplify]: Extracting #4: cost 417 inf + 52622 11.040 * * [simplify]: Extracting #5: cost 157 inf + 465463 11.087 * * [simplify]: Extracting #6: cost 2 inf + 707329 11.131 * * [simplify]: Extracting #7: cost 0 inf + 711417 11.172 * [simplify]: Simplified to (*.p16 (+.p16 c (/.p16 (+.p16 (+.p16 b a) c) (real->posit16 2))) (-.p16 (/.p16 (+.p16 (+.p16 b a) c) (real->posit16 2)) c)) 11.172 * [simplify]: Simplified (2 1 2 1) to (λ (a b c) (sqrt.p16 (*.p16 (*.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) a)) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) b)) (/.p16 (*.p16 (+.p16 c (/.p16 (+.p16 (+.p16 b a) c) (real->posit16 2))) (-.p16 (/.p16 (+.p16 (+.p16 b a) c) (real->posit16 2)) c)) (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) c))))) 11.172 * [simplify]: Simplifying (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) c) 11.172 * * [simplify]: iters left: 4 (9 enodes) 11.175 * * [simplify]: iters left: 3 (21 enodes) 11.178 * * [simplify]: iters left: 2 (27 enodes) 11.182 * * [simplify]: iters left: 1 (28 enodes) 11.185 * * [simplify]: Extracting #0: cost 1 inf + 0 11.185 * * [simplify]: Extracting #1: cost 3 inf + 0 11.185 * * [simplify]: Extracting #2: cost 4 inf + 1 11.185 * * [simplify]: Extracting #3: cost 10 inf + 1 11.185 * * [simplify]: Extracting #4: cost 5 inf + 47 11.185 * * [simplify]: Extracting #5: cost 1 inf + 738 11.186 * * [simplify]: Extracting #6: cost 0 inf + 1302 11.186 * [simplify]: Simplified to (+.p16 c (/.p16 (+.p16 a (+.p16 c b)) (real->posit16 2))) 11.186 * [simplify]: Simplified (2 1 2 2) to (λ (a b c) (sqrt.p16 (*.p16 (*.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) a)) (-.p16 (/.p16 (+.p16 (+.p16 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 c (/.p16 (+.p16 a (+.p16 c b)) (real->posit16 2))))))) 11.186 * * * * [progress]: [ 12 / 13 ] simplifiying candidate #posit16 2)) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) a)) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) b)) (/.p16 (-.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2))) (*.p16 c c)) (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) c)))))> 11.186 * [simplify]: Simplifying (-.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2))) (*.p16 c c)) 11.186 * * [simplify]: iters left: 5 (11 enodes) 11.191 * * [simplify]: iters left: 4 (36 enodes) 11.204 * * [simplify]: iters left: 3 (93 enodes) 11.224 * * [simplify]: iters left: 2 (310 enodes) 11.377 * * [simplify]: Extracting #0: cost 1 inf + 0 11.377 * * [simplify]: Extracting #1: cost 32 inf + 0 11.378 * * [simplify]: Extracting #2: cost 177 inf + 0 11.378 * * [simplify]: Extracting #3: cost 262 inf + 323 11.381 * * [simplify]: Extracting #4: cost 417 inf + 52622 11.402 * * [simplify]: Extracting #5: cost 157 inf + 465463 11.444 * * [simplify]: Extracting #6: cost 2 inf + 707329 11.497 * * [simplify]: Extracting #7: cost 0 inf + 711417 11.539 * [simplify]: Simplified to (*.p16 (+.p16 c (/.p16 (+.p16 (+.p16 b a) c) (real->posit16 2))) (-.p16 (/.p16 (+.p16 (+.p16 b a) c) (real->posit16 2)) c)) 11.539 * [simplify]: Simplified (2 1 2 1) to (λ (a b c) (sqrt.p16 (*.p16 (*.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) a)) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) b)) (/.p16 (*.p16 (+.p16 c (/.p16 (+.p16 (+.p16 b a) c) (real->posit16 2))) (-.p16 (/.p16 (+.p16 (+.p16 b a) c) (real->posit16 2)) c)) (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) c))))) 11.539 * [simplify]: Simplifying (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) c) 11.539 * * [simplify]: iters left: 4 (9 enodes) 11.541 * * [simplify]: iters left: 3 (21 enodes) 11.544 * * [simplify]: iters left: 2 (27 enodes) 11.548 * * [simplify]: iters left: 1 (28 enodes) 11.552 * * [simplify]: Extracting #0: cost 1 inf + 0 11.552 * * [simplify]: Extracting #1: cost 3 inf + 0 11.552 * * [simplify]: Extracting #2: cost 4 inf + 1 11.552 * * [simplify]: Extracting #3: cost 10 inf + 1 11.552 * * [simplify]: Extracting #4: cost 5 inf + 47 11.552 * * [simplify]: Extracting #5: cost 1 inf + 738 11.553 * * [simplify]: Extracting #6: cost 0 inf + 1302 11.553 * [simplify]: Simplified to (+.p16 c (/.p16 (+.p16 a (+.p16 c b)) (real->posit16 2))) 11.553 * [simplify]: Simplified (2 1 2 2) to (λ (a b c) (sqrt.p16 (*.p16 (*.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) a)) (-.p16 (/.p16 (+.p16 (+.p16 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 c (/.p16 (+.p16 a (+.p16 c b)) (real->posit16 2))))))) 11.553 * * * * [progress]: [ 13 / 13 ] simplifiying candidate #posit16 2)) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) a)) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) b)) (/.p16 (-.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2))) (*.p16 c c)) (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) c)))))> 11.553 * [simplify]: Simplifying (-.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2))) (*.p16 c c)) 11.553 * * [simplify]: iters left: 5 (11 enodes) 11.556 * * [simplify]: iters left: 4 (36 enodes) 11.563 * * [simplify]: iters left: 3 (93 enodes) 11.595 * * [simplify]: iters left: 2 (310 enodes) 11.839 * * [simplify]: Extracting #0: cost 1 inf + 0 11.839 * * [simplify]: Extracting #1: cost 32 inf + 0 11.840 * * [simplify]: Extracting #2: cost 177 inf + 0 11.841 * * [simplify]: Extracting #3: cost 262 inf + 323 11.847 * * [simplify]: Extracting #4: cost 417 inf + 52622 11.890 * * [simplify]: Extracting #5: cost 157 inf + 465463 11.966 * * [simplify]: Extracting #6: cost 2 inf + 707329 12.040 * * [simplify]: Extracting #7: cost 0 inf + 711417 12.116 * [simplify]: Simplified to (*.p16 (+.p16 c (/.p16 (+.p16 (+.p16 b a) c) (real->posit16 2))) (-.p16 (/.p16 (+.p16 (+.p16 b a) c) (real->posit16 2)) c)) 12.116 * [simplify]: Simplified (2 1 2 1) to (λ (a b c) (sqrt.p16 (*.p16 (*.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) a)) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) b)) (/.p16 (*.p16 (+.p16 c (/.p16 (+.p16 (+.p16 b a) c) (real->posit16 2))) (-.p16 (/.p16 (+.p16 (+.p16 b a) c) (real->posit16 2)) c)) (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) c))))) 12.116 * [simplify]: Simplifying (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) c) 12.116 * * [simplify]: iters left: 4 (9 enodes) 12.120 * * [simplify]: iters left: 3 (21 enodes) 12.126 * * [simplify]: iters left: 2 (27 enodes) 12.134 * * [simplify]: iters left: 1 (28 enodes) 12.142 * * [simplify]: Extracting #0: cost 1 inf + 0 12.142 * * [simplify]: Extracting #1: cost 3 inf + 0 12.142 * * [simplify]: Extracting #2: cost 4 inf + 1 12.142 * * [simplify]: Extracting #3: cost 10 inf + 1 12.142 * * [simplify]: Extracting #4: cost 5 inf + 47 12.142 * * [simplify]: Extracting #5: cost 1 inf + 738 12.142 * * [simplify]: Extracting #6: cost 0 inf + 1302 12.143 * [simplify]: Simplified to (+.p16 c (/.p16 (+.p16 a (+.p16 c b)) (real->posit16 2))) 12.143 * [simplify]: Simplified (2 1 2 2) to (λ (a b c) (sqrt.p16 (*.p16 (*.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) a)) (-.p16 (/.p16 (+.p16 (+.p16 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 c (/.p16 (+.p16 a (+.p16 c b)) (real->posit16 2))))))) 12.143 * * * [progress]: adding candidates to table 12.615 * * [progress]: iteration 3 / 4 12.615 * * * [progress]: picking best candidate 12.705 * * * * [pick]: Picked #posit16 2)) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) a)) (/.p16 (-.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2))) (*.p16 b b)) (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) b))) (/.p16 (-.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2))) (*.p16 c c)) (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) c)))))> 12.705 * * * [progress]: localizing error 13.344 * * * [progress]: generating rewritten candidates 13.344 * * * * [progress]: [ 1 / 4 ] rewriting at (2 1 1 2) 13.457 * * * * [progress]: [ 2 / 4 ] rewriting at (2 1 2) 13.543 * * * * [progress]: [ 3 / 4 ] rewriting at (2 1 1 1 2) 13.570 * * * * [progress]: [ 4 / 4 ] rewriting at (2 1 2 1) 13.575 * * * [progress]: generating series expansions 13.575 * * * * [progress]: [ 1 / 4 ] generating series at (2 1 1 2) 13.575 * * * * [progress]: [ 2 / 4 ] generating series at (2 1 2) 13.575 * * * * [progress]: [ 3 / 4 ] generating series at (2 1 1 1 2) 13.575 * * * * [progress]: [ 4 / 4 ] generating series at (2 1 2 1) 13.575 * * * [progress]: simplifying candidates 13.575 * * * * [progress]: [ 1 / 13 ] simplifiying candidate #posit16 2)) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) a)) (/.p16 (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) b) (/.p16 (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) b) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) b)))) (/.p16 (-.p16 (*.p16 (/.p16 (+.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)))))> 13.576 * [simplify]: Simplifying (/.p16 (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) b) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) b)) 13.576 * * [simplify]: iters left: 5 (11 enodes) 13.581 * * [simplify]: iters left: 4 (29 enodes) 13.589 * * [simplify]: iters left: 3 (50 enodes) 13.606 * * [simplify]: iters left: 2 (136 enodes) 13.672 * * [simplify]: Extracting #0: cost 1 inf + 0 13.672 * * [simplify]: Extracting #1: cost 19 inf + 0 13.672 * * [simplify]: Extracting #2: cost 68 inf + 0 13.673 * * [simplify]: Extracting #3: cost 107 inf + 2 13.673 * * [simplify]: Extracting #4: cost 146 inf + 1531 13.675 * * [simplify]: Extracting #5: cost 151 inf + 11530 13.682 * * [simplify]: Extracting #6: cost 63 inf + 103615 13.700 * * [simplify]: Extracting #7: cost 9 inf + 195949 13.721 * * [simplify]: Extracting #8: cost 0 inf + 216545 13.742 * * [simplify]: Extracting #9: cost 0 inf + 216105 13.763 * [simplify]: Simplified to (/.p16 (+.p16 (/.p16 (+.p16 (+.p16 b a) c) (real->posit16 2)) b) (-.p16 (/.p16 (+.p16 (+.p16 b a) c) (real->posit16 2)) b)) 13.763 * [simplify]: Simplified (2 1 1 2 2) to (λ (a b c) (sqrt.p16 (*.p16 (*.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) a)) (/.p16 (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) b) (/.p16 (+.p16 (/.p16 (+.p16 (+.p16 b a) c) (real->posit16 2)) b) (-.p16 (/.p16 (+.p16 (+.p16 b a) 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))))) 13.763 * * * * [progress]: [ 2 / 13 ] simplifiying candidate #posit16 2)) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) a)) (/.p16 (-.p16 (*.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2))) (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)))) (*.p16 (*.p16 b b) (*.p16 b b))) (*.p16 (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) b) (+.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2))) (*.p16 b b))))) (/.p16 (-.p16 (*.p16 (/.p16 (+.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)))))> 13.764 * [simplify]: Simplifying (*.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))) 13.764 * * [simplify]: iters left: 6 (13 enodes) 13.769 * * [simplify]: iters left: 5 (37 enodes) 13.782 * * [simplify]: iters left: 4 (103 enodes) 13.826 * * [simplify]: iters left: 3 (299 enodes) 13.949 * * [simplify]: Extracting #0: cost 1 inf + 0 13.949 * * [simplify]: Extracting #1: cost 15 inf + 0 13.949 * * [simplify]: Extracting #2: cost 76 inf + 0 13.950 * * [simplify]: Extracting #3: cost 226 inf + 1 13.953 * * [simplify]: Extracting #4: cost 226 inf + 48319 13.965 * * [simplify]: Extracting #5: cost 17 inf + 267948 13.984 * * [simplify]: Extracting #6: cost 0 inf + 289975 14.013 * [simplify]: Simplified to (*.p16 (+.p16 (/.p16 (+.p16 (+.p16 b a) c) (real->posit16 2)) b) (+.p16 (*.p16 b b) (*.p16 (/.p16 (+.p16 (+.p16 b a) c) (real->posit16 2)) (/.p16 (+.p16 (+.p16 b a) c) (real->posit16 2))))) 14.013 * [simplify]: Simplified (2 1 1 2 2) to (λ (a b c) (sqrt.p16 (*.p16 (*.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) a)) (/.p16 (-.p16 (*.p16 (*.p16 (/.p16 (+.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 b a) c) (real->posit16 2)) 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 (+.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))))) 14.014 * * * * [progress]: [ 3 / 13 ] simplifiying candidate #posit16 2)) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) a)) (/.p16 (-.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2))) (*.p16 b b)) (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) b))) (/.p16 (+.p16 (/.p16 (+.p16 (+.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))))))> 14.014 * [simplify]: Simplifying (/.p16 (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) c) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) c)) 14.014 * * [simplify]: iters left: 5 (11 enodes) 14.019 * * [simplify]: iters left: 4 (29 enodes) 14.027 * * [simplify]: iters left: 3 (50 enodes) 14.043 * * [simplify]: iters left: 2 (136 enodes) 14.096 * * [simplify]: Extracting #0: cost 1 inf + 0 14.096 * * [simplify]: Extracting #1: cost 19 inf + 0 14.096 * * [simplify]: Extracting #2: cost 68 inf + 0 14.097 * * [simplify]: Extracting #3: cost 105 inf + 404 14.097 * * [simplify]: Extracting #4: cost 144 inf + 3212 14.099 * * [simplify]: Extracting #5: cost 141 inf + 17509 14.106 * * [simplify]: Extracting #6: cost 62 inf + 102535 14.119 * * [simplify]: Extracting #7: cost 9 inf + 195869 14.130 * * [simplify]: Extracting #8: cost 0 inf + 216465 14.141 * * [simplify]: Extracting #9: cost 0 inf + 216025 14.158 * [simplify]: Simplified to (/.p16 (+.p16 c (/.p16 (+.p16 b (+.p16 a c)) (real->posit16 2))) (-.p16 (/.p16 (+.p16 b (+.p16 a c)) (real->posit16 2)) c)) 14.158 * [simplify]: Simplified (2 1 2 2) to (λ (a b c) (sqrt.p16 (*.p16 (*.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) a)) (/.p16 (-.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2))) (*.p16 b b)) (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) b))) (/.p16 (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) c) (/.p16 (+.p16 c (/.p16 (+.p16 b (+.p16 a c)) (real->posit16 2))) (-.p16 (/.p16 (+.p16 b (+.p16 a c)) (real->posit16 2)) c)))))) 14.159 * * * * [progress]: [ 4 / 13 ] simplifiying candidate #posit16 2)) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) a)) (/.p16 (-.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2))) (*.p16 b b)) (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) b))) (/.p16 (-.p16 (*.p16 (*.p16 (/.p16 (+.p16 (+.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)))))))> 14.159 * [simplify]: Simplifying (*.p16 (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) c) (+.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2))) (*.p16 c c))) 14.159 * * [simplify]: iters left: 6 (13 enodes) 14.165 * * [simplify]: iters left: 5 (37 enodes) 14.178 * * [simplify]: iters left: 4 (103 enodes) 14.210 * * [simplify]: iters left: 3 (299 enodes) 14.331 * * [simplify]: Extracting #0: cost 1 inf + 0 14.331 * * [simplify]: Extracting #1: cost 15 inf + 0 14.331 * * [simplify]: Extracting #2: cost 76 inf + 0 14.333 * * [simplify]: Extracting #3: cost 225 inf + 1 14.337 * * [simplify]: Extracting #4: cost 218 inf + 50046 14.356 * * [simplify]: Extracting #5: cost 20 inf + 255793 14.386 * * [simplify]: Extracting #6: cost 0 inf + 279953 14.408 * [simplify]: Simplified to (*.p16 (+.p16 c (/.p16 (+.p16 (+.p16 b a) c) (real->posit16 2))) (+.p16 (*.p16 c c) (*.p16 (/.p16 (+.p16 (+.p16 b a) c) (real->posit16 2)) (/.p16 (+.p16 (+.p16 b a) c) (real->posit16 2))))) 14.408 * [simplify]: Simplified (2 1 2 2) to (λ (a b c) (sqrt.p16 (*.p16 (*.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) a)) (/.p16 (-.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2))) (*.p16 b b)) (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) b))) (/.p16 (-.p16 (*.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2))) (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)))) (*.p16 (*.p16 c c) (*.p16 c c))) (*.p16 (+.p16 c (/.p16 (+.p16 (+.p16 b a) c) (real->posit16 2))) (+.p16 (*.p16 c c) (*.p16 (/.p16 (+.p16 (+.p16 b a) c) (real->posit16 2)) (/.p16 (+.p16 (+.p16 b a) c) (real->posit16 2))))))))) 14.408 * * * * [progress]: [ 5 / 13 ] simplifiying candidate #posit16 2)) (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (neg.p16 a))) (/.p16 (-.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2))) (*.p16 b b)) (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) b))) (/.p16 (-.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2))) (*.p16 c c)) (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) c)))))> 14.409 * [simplify]: Simplifying (neg.p16 a) 14.409 * * [simplify]: iters left: 1 (2 enodes) 14.409 * * [simplify]: Extracting #0: cost 1 inf + 0 14.409 * * [simplify]: Extracting #1: cost 2 inf + 0 14.409 * * [simplify]: Extracting #2: cost 1 inf + 1 14.409 * * [simplify]: Extracting #3: cost 0 inf + 82 14.409 * [simplify]: Simplified to (neg.p16 a) 14.409 * [simplify]: Simplified (2 1 1 1 2 2) to (λ (a b c) (sqrt.p16 (*.p16 (*.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (neg.p16 a))) (/.p16 (-.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2))) (*.p16 b b)) (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) b))) (/.p16 (-.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2))) (*.p16 c c)) (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) c))))) 14.409 * * * * [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)))))> 14.410 * [simplify]: Simplifying (-.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2))) (*.p16 a a)) 14.410 * * [simplify]: iters left: 5 (11 enodes) 14.412 * * [simplify]: iters left: 4 (36 enodes) 14.420 * * [simplify]: iters left: 3 (93 enodes) 14.457 * * [simplify]: iters left: 2 (310 enodes) 14.634 * * [simplify]: Extracting #0: cost 1 inf + 0 14.634 * * [simplify]: Extracting #1: cost 32 inf + 0 14.635 * * [simplify]: Extracting #2: cost 177 inf + 0 14.636 * * [simplify]: Extracting #3: cost 262 inf + 323 14.639 * * [simplify]: Extracting #4: cost 416 inf + 51663 14.665 * * [simplify]: Extracting #5: cost 116 inf + 501475 14.706 * * [simplify]: Extracting #6: cost 0 inf + 713857 14.754 * * [simplify]: Extracting #7: cost 0 inf + 713577 14.796 * [simplify]: Simplified to (*.p16 (+.p16 a (/.p16 (+.p16 (+.p16 b a) c) (real->posit16 2))) (-.p16 (/.p16 (+.p16 (+.p16 b a) c) (real->posit16 2)) a)) 14.797 * [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 a (/.p16 (+.p16 (+.p16 b a) c) (real->posit16 2))) (-.p16 (/.p16 (+.p16 (+.p16 b 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 (+.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))))) 14.797 * [simplify]: Simplifying (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) a) 14.797 * * [simplify]: iters left: 4 (9 enodes) 14.800 * * [simplify]: iters left: 3 (21 enodes) 14.803 * * [simplify]: iters left: 2 (27 enodes) 14.807 * * [simplify]: iters left: 1 (28 enodes) 14.811 * * [simplify]: Extracting #0: cost 1 inf + 0 14.811 * * [simplify]: Extracting #1: cost 3 inf + 0 14.811 * * [simplify]: Extracting #2: cost 4 inf + 1 14.811 * * [simplify]: Extracting #3: cost 10 inf + 1 14.811 * * [simplify]: Extracting #4: cost 1 inf + 738 14.811 * * [simplify]: Extracting #5: cost 0 inf + 1302 14.811 * [simplify]: Simplified to (+.p16 a (/.p16 (+.p16 (+.p16 b a) c) (real->posit16 2))) 14.811 * [simplify]: Simplified (2 1 1 1 2 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 a (/.p16 (+.p16 (+.p16 b a) 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 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))))) 14.811 * * * * [progress]: [ 7 / 13 ] simplifiying candidate #posit16 2)) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) a)) (/.p16 (-.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (/.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)) c) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) c)) (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) c)))))> 14.812 * [simplify]: Simplifying (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) c) 14.812 * * [simplify]: iters left: 4 (9 enodes) 14.814 * * [simplify]: iters left: 3 (21 enodes) 14.817 * * [simplify]: iters left: 2 (27 enodes) 14.820 * * [simplify]: iters left: 1 (28 enodes) 14.824 * * [simplify]: Extracting #0: cost 1 inf + 0 14.824 * * [simplify]: Extracting #1: cost 3 inf + 0 14.824 * * [simplify]: Extracting #2: cost 4 inf + 1 14.824 * * [simplify]: Extracting #3: cost 10 inf + 1 14.824 * * [simplify]: Extracting #4: cost 5 inf + 47 14.824 * * [simplify]: Extracting #5: cost 1 inf + 738 14.824 * * [simplify]: Extracting #6: cost 0 inf + 1302 14.825 * [simplify]: Simplified to (+.p16 c (/.p16 (+.p16 a (+.p16 c b)) (real->posit16 2))) 14.825 * [simplify]: Simplified (2 1 2 1 1) to (λ (a b c) (sqrt.p16 (*.p16 (*.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) a)) (/.p16 (-.p16 (*.p16 (/.p16 (+.p16 (+.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 c (/.p16 (+.p16 a (+.p16 c b)) (real->posit16 2))) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) c)) (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) c))))) 14.825 * [simplify]: Simplifying (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) c) 14.825 * * [simplify]: iters left: 4 (9 enodes) 14.827 * * [simplify]: iters left: 3 (27 enodes) 14.831 * * [simplify]: iters left: 2 (47 enodes) 14.839 * * [simplify]: iters left: 1 (123 enodes) 14.870 * * [simplify]: Extracting #0: cost 1 inf + 0 14.871 * * [simplify]: Extracting #1: cost 15 inf + 0 14.871 * * [simplify]: Extracting #2: cost 52 inf + 82 14.871 * * [simplify]: Extracting #3: cost 87 inf + 1044 14.871 * * [simplify]: Extracting #4: cost 138 inf + 5615 14.872 * * [simplify]: Extracting #5: cost 116 inf + 19272 14.876 * * [simplify]: Extracting #6: cost 57 inf + 78898 14.883 * * [simplify]: Extracting #7: cost 8 inf + 156974 14.892 * * [simplify]: Extracting #8: cost 0 inf + 175966 14.901 * [simplify]: Simplified to (-.p16 (/.p16 (+.p16 b (+.p16 a c)) (real->posit16 2)) c) 14.901 * [simplify]: Simplified (2 1 2 1 2) to (λ (a b c) (sqrt.p16 (*.p16 (*.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) a)) (/.p16 (-.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (/.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)) c) (-.p16 (/.p16 (+.p16 b (+.p16 a c)) (real->posit16 2)) c)) (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) c))))) 14.902 * * * * [progress]: [ 8 / 13 ] simplifiying candidate #posit16 2)) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) a)) (/.p16 (-.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2))) (*.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))) (neg.p16 (*.p16 c c))) (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) c)))))> 14.902 * [simplify]: Simplifying (neg.p16 (*.p16 c c)) 14.902 * * [simplify]: iters left: 2 (3 enodes) 14.902 * * [simplify]: iters left: 1 (5 enodes) 14.903 * * [simplify]: Extracting #0: cost 1 inf + 0 14.903 * * [simplify]: Extracting #1: cost 2 inf + 0 14.903 * * [simplify]: Extracting #2: cost 3 inf + 0 14.903 * * [simplify]: Extracting #3: cost 2 inf + 1 14.903 * * [simplify]: Extracting #4: cost 0 inf + 723 14.903 * [simplify]: Simplified to (neg.p16 (*.p16 c c)) 14.903 * [simplify]: Simplified (2 1 2 1 2) to (λ (a b c) (sqrt.p16 (*.p16 (*.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) a)) (/.p16 (-.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (/.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))) (neg.p16 (*.p16 c c))) (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) c))))) 14.904 * * * * [progress]: [ 9 / 13 ] simplifiying candidate #posit16 2)) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) a)) (/.p16 (-.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2))) (*.p16 b b)) (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) b))) (/.p16 (/.p16 (-.p16 (*.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2))) (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)))) (*.p16 (*.p16 c c) (*.p16 c c))) (+.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2))) (*.p16 c c))) (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) c)))))> 14.904 * [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))) 14.904 * * [simplify]: iters left: 6 (13 enodes) 14.907 * * [simplify]: iters left: 5 (46 enodes) 14.916 * * [simplify]: iters left: 4 (130 enodes) 14.953 * * [simplify]: Extracting #0: cost 1 inf + 0 14.953 * * [simplify]: Extracting #1: cost 25 inf + 0 14.953 * * [simplify]: Extracting #2: cost 62 inf + 0 14.954 * * [simplify]: Extracting #3: cost 156 inf + 82 14.956 * * [simplify]: Extracting #4: cost 155 inf + 20973 14.967 * * [simplify]: Extracting #5: cost 51 inf + 151607 14.987 * * [simplify]: Extracting #6: cost 3 inf + 236996 15.000 * * [simplify]: Extracting #7: cost 0 inf + 246088 15.012 * [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))) 15.012 * [simplify]: Simplified (2 1 2 1 1) to (λ (a b c) (sqrt.p16 (*.p16 (*.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) a)) (/.p16 (-.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2))) (*.p16 b b)) (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) b))) (/.p16 (/.p16 (-.p16 (*.p16 (*.p16 (/.p16 (+.p16 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)) (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2))) (*.p16 c c))) (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) c))))) 15.013 * [simplify]: Simplifying (+.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2))) (*.p16 c c)) 15.013 * * [simplify]: iters left: 5 (11 enodes) 15.018 * * [simplify]: iters left: 4 (27 enodes) 15.023 * * [simplify]: iters left: 3 (53 enodes) 15.033 * * [simplify]: iters left: 2 (121 enodes) 15.058 * * [simplify]: iters left: 1 (313 enodes) 15.193 * * [simplify]: Extracting #0: cost 1 inf + 0 15.193 * * [simplify]: Extracting #1: cost 21 inf + 0 15.194 * * [simplify]: Extracting #2: cost 48 inf + 0 15.195 * * [simplify]: Extracting #3: cost 201 inf + 324 15.200 * * [simplify]: Extracting #4: cost 143 inf + 47287 15.215 * * [simplify]: Extracting #5: cost 17 inf + 136312 15.225 * * [simplify]: Extracting #6: cost 0 inf + 151168 15.235 * [simplify]: Simplified to (+.p16 (*.p16 c c) (*.p16 (/.p16 (+.p16 (+.p16 b a) c) (real->posit16 2)) (/.p16 (+.p16 (+.p16 b a) c) (real->posit16 2)))) 15.235 * [simplify]: Simplified (2 1 2 1 2) to (λ (a b c) (sqrt.p16 (*.p16 (*.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) a)) (/.p16 (-.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2))) (*.p16 b b)) (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) b))) (/.p16 (/.p16 (-.p16 (*.p16 (*.p16 (/.p16 (+.p16 (+.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 c c) (*.p16 (/.p16 (+.p16 (+.p16 b a) c) (real->posit16 2)) (/.p16 (+.p16 (+.p16 b a) c) (real->posit16 2))))) (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) c))))) 15.235 * * * * [progress]: [ 10 / 13 ] simplifiying candidate #posit16 2)) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) a)) (/.p16 (-.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2))) (*.p16 b b)) (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) b))) (/.p16 (-.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2))) (*.p16 c c)) (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) c)))))> 15.236 * [simplify]: Simplifying (-.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2))) (*.p16 b b)) 15.236 * * [simplify]: iters left: 5 (11 enodes) 15.239 * * [simplify]: iters left: 4 (36 enodes) 15.246 * * [simplify]: iters left: 3 (93 enodes) 15.287 * * [simplify]: iters left: 2 (310 enodes) 15.517 * * [simplify]: Extracting #0: cost 1 inf + 0 15.518 * * [simplify]: Extracting #1: cost 32 inf + 0 15.518 * * [simplify]: Extracting #2: cost 177 inf + 0 15.520 * * [simplify]: Extracting #3: cost 260 inf + 323 15.523 * * [simplify]: Extracting #4: cost 456 inf + 5597 15.544 * * [simplify]: Extracting #5: cost 278 inf + 236939 15.609 * * [simplify]: Extracting #6: cost 27 inf + 652788 15.688 * * [simplify]: Extracting #7: cost 2 inf + 706688 15.772 * * [simplify]: Extracting #8: cost 0 inf + 713376 15.853 * [simplify]: Simplified to (*.p16 (+.p16 (/.p16 (+.p16 (+.p16 b a) c) (real->posit16 2)) b) (-.p16 (/.p16 (+.p16 (+.p16 b a) c) (real->posit16 2)) b)) 15.853 * [simplify]: Simplified (2 1 1 2 1) to (λ (a b c) (sqrt.p16 (*.p16 (*.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) a)) (/.p16 (*.p16 (+.p16 (/.p16 (+.p16 (+.p16 b a) c) (real->posit16 2)) b) (-.p16 (/.p16 (+.p16 (+.p16 b a) c) (real->posit16 2)) b)) (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) b))) (/.p16 (-.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2))) (*.p16 c c)) (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) c))))) 15.853 * [simplify]: Simplifying (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) b) 15.853 * * [simplify]: iters left: 4 (9 enodes) 15.858 * * [simplify]: iters left: 3 (21 enodes) 15.864 * * [simplify]: iters left: 2 (27 enodes) 15.872 * * [simplify]: iters left: 1 (28 enodes) 15.880 * * [simplify]: Extracting #0: cost 1 inf + 0 15.880 * * [simplify]: Extracting #1: cost 3 inf + 0 15.880 * * [simplify]: Extracting #2: cost 4 inf + 1 15.880 * * [simplify]: Extracting #3: cost 10 inf + 1 15.880 * * [simplify]: Extracting #4: cost 5 inf + 47 15.880 * * [simplify]: Extracting #5: cost 1 inf + 738 15.881 * * [simplify]: Extracting #6: cost 0 inf + 1302 15.881 * [simplify]: Simplified to (+.p16 (/.p16 (+.p16 a (+.p16 c b)) (real->posit16 2)) b) 15.881 * [simplify]: Simplified (2 1 1 2 2) to (λ (a b c) (sqrt.p16 (*.p16 (*.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) a)) (/.p16 (-.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2))) (*.p16 b b)) (+.p16 (/.p16 (+.p16 a (+.p16 c b)) (real->posit16 2)) b))) (/.p16 (-.p16 (*.p16 (/.p16 (+.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))))) 15.881 * * * * [progress]: [ 11 / 13 ] simplifiying candidate #posit16 2)) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) a)) (/.p16 (-.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2))) (*.p16 b b)) (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) b))) (/.p16 (-.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2))) (*.p16 c c)) (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) c)))))> 15.882 * [simplify]: Simplifying (-.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2))) (*.p16 b b)) 15.882 * * [simplify]: iters left: 5 (11 enodes) 15.888 * * [simplify]: iters left: 4 (36 enodes) 15.905 * * [simplify]: iters left: 3 (93 enodes) 15.946 * * [simplify]: iters left: 2 (310 enodes) 16.193 * * [simplify]: Extracting #0: cost 1 inf + 0 16.193 * * [simplify]: Extracting #1: cost 32 inf + 0 16.194 * * [simplify]: Extracting #2: cost 177 inf + 0 16.194 * * [simplify]: Extracting #3: cost 260 inf + 323 16.196 * * [simplify]: Extracting #4: cost 456 inf + 5597 16.207 * * [simplify]: Extracting #5: cost 278 inf + 236939 16.243 * * [simplify]: Extracting #6: cost 27 inf + 652788 16.285 * * [simplify]: Extracting #7: cost 2 inf + 706688 16.327 * * [simplify]: Extracting #8: cost 0 inf + 713376 16.380 * [simplify]: Simplified to (*.p16 (+.p16 (/.p16 (+.p16 (+.p16 b a) c) (real->posit16 2)) b) (-.p16 (/.p16 (+.p16 (+.p16 b a) c) (real->posit16 2)) b)) 16.380 * [simplify]: Simplified (2 1 1 2 1) to (λ (a b c) (sqrt.p16 (*.p16 (*.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) a)) (/.p16 (*.p16 (+.p16 (/.p16 (+.p16 (+.p16 b a) c) (real->posit16 2)) b) (-.p16 (/.p16 (+.p16 (+.p16 b a) c) (real->posit16 2)) b)) (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) b))) (/.p16 (-.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2))) (*.p16 c c)) (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) c))))) 16.381 * [simplify]: Simplifying (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) b) 16.381 * * [simplify]: iters left: 4 (9 enodes) 16.385 * * [simplify]: iters left: 3 (21 enodes) 16.392 * * [simplify]: iters left: 2 (27 enodes) 16.399 * * [simplify]: iters left: 1 (28 enodes) 16.407 * * [simplify]: Extracting #0: cost 1 inf + 0 16.407 * * [simplify]: Extracting #1: cost 3 inf + 0 16.407 * * [simplify]: Extracting #2: cost 4 inf + 1 16.407 * * [simplify]: Extracting #3: cost 10 inf + 1 16.407 * * [simplify]: Extracting #4: cost 5 inf + 47 16.407 * * [simplify]: Extracting #5: cost 1 inf + 738 16.407 * * [simplify]: Extracting #6: cost 0 inf + 1302 16.408 * [simplify]: Simplified to (+.p16 (/.p16 (+.p16 a (+.p16 c b)) (real->posit16 2)) b) 16.408 * [simplify]: Simplified (2 1 1 2 2) to (λ (a b c) (sqrt.p16 (*.p16 (*.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) a)) (/.p16 (-.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2))) (*.p16 b b)) (+.p16 (/.p16 (+.p16 a (+.p16 c b)) (real->posit16 2)) b))) (/.p16 (-.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2))) (*.p16 c c)) (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) c))))) 16.408 * * * * [progress]: [ 12 / 13 ] simplifiying candidate #posit16 2)) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) a)) (/.p16 (-.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2))) (*.p16 b b)) (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) b))) (/.p16 (-.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2))) (*.p16 c c)) (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) c)))))> 16.408 * [simplify]: Simplifying (-.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2))) (*.p16 b b)) 16.408 * * [simplify]: iters left: 5 (11 enodes) 16.413 * * [simplify]: iters left: 4 (36 enodes) 16.426 * * [simplify]: iters left: 3 (93 enodes) 16.465 * * [simplify]: iters left: 2 (310 enodes) 16.635 * * [simplify]: Extracting #0: cost 1 inf + 0 16.635 * * [simplify]: Extracting #1: cost 32 inf + 0 16.636 * * [simplify]: Extracting #2: cost 177 inf + 0 16.636 * * [simplify]: Extracting #3: cost 260 inf + 323 16.638 * * [simplify]: Extracting #4: cost 456 inf + 5597 16.658 * * [simplify]: Extracting #5: cost 278 inf + 236939 16.724 * * [simplify]: Extracting #6: cost 27 inf + 652788 16.788 * * [simplify]: Extracting #7: cost 2 inf + 706688 16.854 * * [simplify]: Extracting #8: cost 0 inf + 713376 16.909 * [simplify]: Simplified to (*.p16 (+.p16 (/.p16 (+.p16 (+.p16 b a) c) (real->posit16 2)) b) (-.p16 (/.p16 (+.p16 (+.p16 b a) c) (real->posit16 2)) b)) 16.910 * [simplify]: Simplified (2 1 1 2 1) to (λ (a b c) (sqrt.p16 (*.p16 (*.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) a)) (/.p16 (*.p16 (+.p16 (/.p16 (+.p16 (+.p16 b a) c) (real->posit16 2)) b) (-.p16 (/.p16 (+.p16 (+.p16 b a) c) (real->posit16 2)) b)) (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) b))) (/.p16 (-.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2))) (*.p16 c c)) (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) c))))) 16.910 * [simplify]: Simplifying (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) b) 16.910 * * [simplify]: iters left: 4 (9 enodes) 16.915 * * [simplify]: iters left: 3 (21 enodes) 16.918 * * [simplify]: iters left: 2 (27 enodes) 16.922 * * [simplify]: iters left: 1 (28 enodes) 16.927 * * [simplify]: Extracting #0: cost 1 inf + 0 16.927 * * [simplify]: Extracting #1: cost 3 inf + 0 16.927 * * [simplify]: Extracting #2: cost 4 inf + 1 16.927 * * [simplify]: Extracting #3: cost 10 inf + 1 16.927 * * [simplify]: Extracting #4: cost 5 inf + 47 16.927 * * [simplify]: Extracting #5: cost 1 inf + 738 16.927 * * [simplify]: Extracting #6: cost 0 inf + 1302 16.927 * [simplify]: Simplified to (+.p16 (/.p16 (+.p16 a (+.p16 c b)) (real->posit16 2)) b) 16.927 * [simplify]: Simplified (2 1 1 2 2) to (λ (a b c) (sqrt.p16 (*.p16 (*.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) a)) (/.p16 (-.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2))) (*.p16 b b)) (+.p16 (/.p16 (+.p16 a (+.p16 c b)) (real->posit16 2)) b))) (/.p16 (-.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2))) (*.p16 c c)) (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) c))))) 16.928 * * * * [progress]: [ 13 / 13 ] simplifiying candidate #posit16 2)) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) a)) (/.p16 (-.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2))) (*.p16 b b)) (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) b))) (/.p16 (-.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2))) (*.p16 c c)) (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) c)))))> 16.928 * [simplify]: Simplifying (-.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2))) (*.p16 b b)) 16.928 * * [simplify]: iters left: 5 (11 enodes) 16.930 * * [simplify]: iters left: 4 (36 enodes) 16.937 * * [simplify]: iters left: 3 (93 enodes) 16.964 * * [simplify]: iters left: 2 (310 enodes) 17.142 * * [simplify]: Extracting #0: cost 1 inf + 0 17.142 * * [simplify]: Extracting #1: cost 32 inf + 0 17.143 * * [simplify]: Extracting #2: cost 177 inf + 0 17.143 * * [simplify]: Extracting #3: cost 260 inf + 323 17.145 * * [simplify]: Extracting #4: cost 456 inf + 5597 17.159 * * [simplify]: Extracting #5: cost 278 inf + 236939 17.212 * * [simplify]: Extracting #6: cost 27 inf + 652788 17.274 * * [simplify]: Extracting #7: cost 2 inf + 706688 17.325 * * [simplify]: Extracting #8: cost 0 inf + 713376 17.377 * [simplify]: Simplified to (*.p16 (+.p16 (/.p16 (+.p16 (+.p16 b a) c) (real->posit16 2)) b) (-.p16 (/.p16 (+.p16 (+.p16 b a) c) (real->posit16 2)) b)) 17.377 * [simplify]: Simplified (2 1 1 2 1) to (λ (a b c) (sqrt.p16 (*.p16 (*.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) a)) (/.p16 (*.p16 (+.p16 (/.p16 (+.p16 (+.p16 b a) c) (real->posit16 2)) b) (-.p16 (/.p16 (+.p16 (+.p16 b a) c) (real->posit16 2)) b)) (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) b))) (/.p16 (-.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2))) (*.p16 c c)) (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) c))))) 17.377 * [simplify]: Simplifying (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) b) 17.377 * * [simplify]: iters left: 4 (9 enodes) 17.380 * * [simplify]: iters left: 3 (21 enodes) 17.383 * * [simplify]: iters left: 2 (27 enodes) 17.387 * * [simplify]: iters left: 1 (28 enodes) 17.391 * * [simplify]: Extracting #0: cost 1 inf + 0 17.391 * * [simplify]: Extracting #1: cost 3 inf + 0 17.391 * * [simplify]: Extracting #2: cost 4 inf + 1 17.391 * * [simplify]: Extracting #3: cost 10 inf + 1 17.391 * * [simplify]: Extracting #4: cost 5 inf + 47 17.391 * * [simplify]: Extracting #5: cost 1 inf + 738 17.391 * * [simplify]: Extracting #6: cost 0 inf + 1302 17.391 * [simplify]: Simplified to (+.p16 (/.p16 (+.p16 a (+.p16 c b)) (real->posit16 2)) b) 17.391 * [simplify]: Simplified (2 1 1 2 2) to (λ (a b c) (sqrt.p16 (*.p16 (*.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) a)) (/.p16 (-.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2))) (*.p16 b b)) (+.p16 (/.p16 (+.p16 a (+.p16 c b)) (real->posit16 2)) b))) (/.p16 (-.p16 (*.p16 (/.p16 (+.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))))) 17.392 * * * [progress]: adding candidates to table 17.894 * * [progress]: iteration 4 / 4 17.894 * * * [progress]: picking best candidate 17.961 * * * * [pick]: Picked #posit16 2)) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) a)) (-.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (/.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))))> 17.961 * * * [progress]: localizing error 18.456 * * * [progress]: generating rewritten candidates 18.456 * * * * [progress]: [ 1 / 4 ] rewriting at (2 1 1) 18.533 * * * * [progress]: [ 2 / 4 ] rewriting at (2 1 2) 18.554 * * * * [progress]: [ 3 / 4 ] rewriting at (2 1 1 1 1 2) 18.576 * * * * [progress]: [ 4 / 4 ] rewriting at (2 1 1 1 2) 18.579 * * * [progress]: generating series expansions 18.579 * * * * [progress]: [ 1 / 4 ] generating series at (2 1 1) 18.579 * * * * [progress]: [ 2 / 4 ] generating series at (2 1 2) 18.579 * * * * [progress]: [ 3 / 4 ] generating series at (2 1 1 1 1 2) 18.579 * * * * [progress]: [ 4 / 4 ] generating series at (2 1 1 1 2) 18.580 * * * [progress]: simplifying candidates 18.580 * * * * [progress]: [ 1 / 15 ] simplifiying candidate #posit16 2)) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) a)) (/.p16 (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) b) (-.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2))) (*.p16 b b)))) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) c))))> 18.580 * [simplify]: Simplifying (/.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))) 18.580 * * [simplify]: iters left: 6 (13 enodes) 18.583 * * [simplify]: iters left: 5 (38 enodes) 18.590 * * [simplify]: iters left: 4 (98 enodes) 18.613 * * [simplify]: iters left: 3 (338 enodes) 18.756 * * [simplify]: Extracting #0: cost 1 inf + 0 18.756 * * [simplify]: Extracting #1: cost 35 inf + 0 18.757 * * [simplify]: Extracting #2: cost 156 inf + 0 18.758 * * [simplify]: Extracting #3: cost 274 inf + 84 18.760 * * [simplify]: Extracting #4: cost 383 inf + 50741 18.778 * * [simplify]: Extracting #5: cost 266 inf + 387303 18.852 * * [simplify]: Extracting #6: cost 7 inf + 795558 18.926 * * [simplify]: Extracting #7: cost 0 inf + 812709 18.986 * [simplify]: Simplified to (/.p16 (real->posit16 1.0) (-.p16 (/.p16 (+.p16 (+.p16 b a) c) (real->posit16 2)) b)) 18.986 * [simplify]: Simplified (2 1 1 2) to (λ (a b c) (sqrt.p16 (*.p16 (/.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) a)) (/.p16 (real->posit16 1.0) (-.p16 (/.p16 (+.p16 (+.p16 b a) c) (real->posit16 2)) b))) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) c)))) 18.986 * * * * [progress]: [ 2 / 15 ] 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 (/.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))))> 18.986 * [simplify]: Simplifying (*.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))) 18.986 * * [simplify]: iters left: 6 (13 enodes) 18.990 * * [simplify]: iters left: 5 (37 enodes) 18.999 * * [simplify]: iters left: 4 (103 enodes) 19.044 * * [simplify]: iters left: 3 (299 enodes) 19.226 * * [simplify]: Extracting #0: cost 1 inf + 0 19.226 * * [simplify]: Extracting #1: cost 15 inf + 0 19.227 * * [simplify]: Extracting #2: cost 76 inf + 0 19.228 * * [simplify]: Extracting #3: cost 226 inf + 1 19.233 * * [simplify]: Extracting #4: cost 226 inf + 48319 19.257 * * [simplify]: Extracting #5: cost 17 inf + 267948 19.290 * * [simplify]: Extracting #6: cost 0 inf + 289975 19.322 * [simplify]: Simplified to (*.p16 (+.p16 (/.p16 (+.p16 (+.p16 b a) c) (real->posit16 2)) b) (+.p16 (*.p16 b b) (*.p16 (/.p16 (+.p16 (+.p16 b a) c) (real->posit16 2)) (/.p16 (+.p16 (+.p16 b a) c) (real->posit16 2))))) 19.322 * [simplify]: Simplified (2 1 1 2) to (λ (a b c) (sqrt.p16 (*.p16 (/.p16 (*.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) a)) (-.p16 (*.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2))) (*.p16 (/.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 b a) c) (real->posit16 2)) 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 a b) c) (real->posit16 2)) c)))) 19.323 * * * * [progress]: [ 3 / 15 ] simplifiying candidate #posit16 2)) (-.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2))) (*.p16 a a))) (-.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2))) (*.p16 b b))) (*.p16 (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) b) (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) a))) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) c))))> 19.323 * [simplify]: Simplifying (*.p16 (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) b) (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) a)) 19.323 * * [simplify]: iters left: 5 (11 enodes) 19.328 * * [simplify]: iters left: 4 (31 enodes) 19.339 * * [simplify]: iters left: 3 (66 enodes) 19.364 * * [simplify]: iters left: 2 (156 enodes) 19.429 * * [simplify]: iters left: 1 (357 enodes) 19.637 * * [simplify]: Extracting #0: cost 1 inf + 0 19.637 * * [simplify]: Extracting #1: cost 17 inf + 0 19.638 * * [simplify]: Extracting #2: cost 57 inf + 0 19.639 * * [simplify]: Extracting #3: cost 159 inf + 2 19.641 * * [simplify]: Extracting #4: cost 163 inf + 6930 19.649 * * [simplify]: Extracting #5: cost 79 inf + 87240 19.669 * * [simplify]: Extracting #6: cost 1 inf + 183630 19.692 * * [simplify]: Extracting #7: cost 0 inf + 184554 19.715 * [simplify]: Simplified to (*.p16 (+.p16 (/.p16 (+.p16 b (+.p16 a c)) (real->posit16 2)) b) (+.p16 a (/.p16 (+.p16 b (+.p16 a c)) (real->posit16 2)))) 19.715 * [simplify]: Simplified (2 1 1 2) to (λ (a b c) (sqrt.p16 (*.p16 (/.p16 (*.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (-.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2))) (*.p16 a a))) (-.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2))) (*.p16 b b))) (*.p16 (+.p16 (/.p16 (+.p16 b (+.p16 a c)) (real->posit16 2)) b) (+.p16 a (/.p16 (+.p16 b (+.p16 a c)) (real->posit16 2))))) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) c)))) 19.715 * * * * [progress]: [ 4 / 15 ] simplifiying candidate #posit16 2)) a)) (-.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2))) (*.p16 b b))) (*.p16 (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) b) (real->posit16 2))) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) c))))> 19.715 * [simplify]: Simplifying (*.p16 (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) b) (real->posit16 2)) 19.716 * * [simplify]: iters left: 5 (10 enodes) 19.721 * * [simplify]: iters left: 4 (23 enodes) 19.731 * * [simplify]: iters left: 3 (37 enodes) 19.743 * * [simplify]: iters left: 2 (42 enodes) 19.754 * * [simplify]: iters left: 1 (68 enodes) 19.776 * * [simplify]: Extracting #0: cost 1 inf + 0 19.776 * * [simplify]: Extracting #1: cost 5 inf + 0 19.776 * * [simplify]: Extracting #2: cost 12 inf + 0 19.776 * * [simplify]: Extracting #3: cost 19 inf + 325 19.777 * * [simplify]: Extracting #4: cost 15 inf + 769 19.777 * * [simplify]: Extracting #5: cost 2 inf + 4368 19.778 * * [simplify]: Extracting #6: cost 0 inf + 5456 19.779 * [simplify]: Simplified to (+.p16 (*.p16 (real->posit16 1.0) (+.p16 (+.p16 b a) c)) (*.p16 (real->posit16 2) b)) 19.779 * [simplify]: Simplified (2 1 1 2) to (λ (a b c) (sqrt.p16 (*.p16 (/.p16 (*.p16 (*.p16 (+.p16 (+.p16 a b) c) (-.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 b b))) (+.p16 (*.p16 (real->posit16 1.0) (+.p16 (+.p16 b a) c)) (*.p16 (real->posit16 2) b))) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) c)))) 19.780 * * * * [progress]: [ 5 / 15 ] simplifiying candidate #posit16 2)) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) a)) (-.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2))) (*.p16 b b))) (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) b)) (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (neg.p16 c)))))> 19.780 * [simplify]: Simplifying (neg.p16 c) 19.780 * * [simplify]: iters left: 1 (2 enodes) 19.781 * * [simplify]: Extracting #0: cost 1 inf + 0 19.781 * * [simplify]: Extracting #1: cost 2 inf + 0 19.781 * * [simplify]: Extracting #2: cost 1 inf + 1 19.781 * * [simplify]: Extracting #3: cost 0 inf + 82 19.781 * [simplify]: Simplified to (neg.p16 c) 19.781 * [simplify]: Simplified (2 1 2 2) to (λ (a b c) (sqrt.p16 (*.p16 (/.p16 (*.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) a)) (-.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2))) (*.p16 b b))) (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) b)) (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (neg.p16 c))))) 19.781 * * * * [progress]: [ 6 / 15 ] simplifiying candidate #posit16 2)) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) a)) (-.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (/.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)))))> 19.782 * [simplify]: Simplifying (-.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2))) (*.p16 c c)) 19.782 * * [simplify]: iters left: 5 (11 enodes) 19.787 * * [simplify]: iters left: 4 (36 enodes) 19.800 * * [simplify]: iters left: 3 (93 enodes) 19.840 * * [simplify]: iters left: 2 (310 enodes) 20.069 * * [simplify]: Extracting #0: cost 1 inf + 0 20.069 * * [simplify]: Extracting #1: cost 32 inf + 0 20.070 * * [simplify]: Extracting #2: cost 177 inf + 0 20.072 * * [simplify]: Extracting #3: cost 262 inf + 323 20.082 * * [simplify]: Extracting #4: cost 417 inf + 52622 20.122 * * [simplify]: Extracting #5: cost 157 inf + 465463 20.198 * * [simplify]: Extracting #6: cost 2 inf + 707329 20.279 * * [simplify]: Extracting #7: cost 0 inf + 711417 20.357 * [simplify]: Simplified to (*.p16 (+.p16 c (/.p16 (+.p16 (+.p16 b a) c) (real->posit16 2))) (-.p16 (/.p16 (+.p16 (+.p16 b a) c) (real->posit16 2)) c)) 20.358 * [simplify]: Simplified (2 1 2 1) to (λ (a b c) (sqrt.p16 (*.p16 (/.p16 (*.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) a)) (-.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (/.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 c (/.p16 (+.p16 (+.p16 b a) c) (real->posit16 2))) (-.p16 (/.p16 (+.p16 (+.p16 b a) c) (real->posit16 2)) c)) (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) c))))) 20.358 * [simplify]: Simplifying (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) c) 20.358 * * [simplify]: iters left: 4 (9 enodes) 20.363 * * [simplify]: iters left: 3 (21 enodes) 20.369 * * [simplify]: iters left: 2 (27 enodes) 20.377 * * [simplify]: iters left: 1 (28 enodes) 20.385 * * [simplify]: Extracting #0: cost 1 inf + 0 20.385 * * [simplify]: Extracting #1: cost 3 inf + 0 20.385 * * [simplify]: Extracting #2: cost 4 inf + 1 20.385 * * [simplify]: Extracting #3: cost 10 inf + 1 20.385 * * [simplify]: Extracting #4: cost 5 inf + 47 20.386 * * [simplify]: Extracting #5: cost 1 inf + 738 20.386 * * [simplify]: Extracting #6: cost 0 inf + 1302 20.386 * [simplify]: Simplified to (+.p16 c (/.p16 (+.p16 a (+.p16 c b)) (real->posit16 2))) 20.386 * [simplify]: Simplified (2 1 2 2) to (λ (a b c) (sqrt.p16 (*.p16 (/.p16 (*.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) a)) (-.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (/.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 c (/.p16 (+.p16 a (+.p16 c b)) (real->posit16 2))))))) 20.387 * * * * [progress]: [ 7 / 15 ] simplifiying candidate #posit16 2)) (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (neg.p16 a))) (-.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (/.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))))> 20.387 * [simplify]: Simplifying (neg.p16 a) 20.387 * * [simplify]: iters left: 1 (2 enodes) 20.388 * * [simplify]: Extracting #0: cost 1 inf + 0 20.388 * * [simplify]: Extracting #1: cost 2 inf + 0 20.388 * * [simplify]: Extracting #2: cost 1 inf + 1 20.388 * * [simplify]: Extracting #3: cost 0 inf + 82 20.388 * [simplify]: Simplified to (neg.p16 a) 20.388 * [simplify]: Simplified (2 1 1 1 1 2 2) to (λ (a b c) (sqrt.p16 (*.p16 (/.p16 (*.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (neg.p16 a))) (-.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (/.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)))) 20.388 * * * * [progress]: [ 8 / 15 ] 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)) (/.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))))> 20.389 * [simplify]: Simplifying (-.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2))) (*.p16 a a)) 20.389 * * [simplify]: iters left: 5 (11 enodes) 20.394 * * [simplify]: iters left: 4 (36 enodes) 20.408 * * [simplify]: iters left: 3 (93 enodes) 20.453 * * [simplify]: iters left: 2 (310 enodes) 20.711 * * [simplify]: Extracting #0: cost 1 inf + 0 20.711 * * [simplify]: Extracting #1: cost 32 inf + 0 20.711 * * [simplify]: Extracting #2: cost 177 inf + 0 20.712 * * [simplify]: Extracting #3: cost 262 inf + 323 20.717 * * [simplify]: Extracting #4: cost 416 inf + 51663 20.740 * * [simplify]: Extracting #5: cost 116 inf + 501475 20.805 * * [simplify]: Extracting #6: cost 0 inf + 713857 20.885 * * [simplify]: Extracting #7: cost 0 inf + 713577 20.965 * [simplify]: Simplified to (*.p16 (+.p16 a (/.p16 (+.p16 (+.p16 b a) c) (real->posit16 2))) (-.p16 (/.p16 (+.p16 (+.p16 b a) c) (real->posit16 2)) a)) 20.965 * [simplify]: Simplified (2 1 1 1 1 2 1) to (λ (a b c) (sqrt.p16 (*.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 b a) c) (real->posit16 2)) a)) (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) a))) (-.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (/.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)))) 20.965 * [simplify]: Simplifying (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) a) 20.966 * * [simplify]: iters left: 4 (9 enodes) 20.970 * * [simplify]: iters left: 3 (21 enodes) 20.976 * * [simplify]: iters left: 2 (27 enodes) 20.984 * * [simplify]: iters left: 1 (28 enodes) 20.992 * * [simplify]: Extracting #0: cost 1 inf + 0 20.992 * * [simplify]: Extracting #1: cost 3 inf + 0 20.992 * * [simplify]: Extracting #2: cost 4 inf + 1 20.992 * * [simplify]: Extracting #3: cost 10 inf + 1 20.993 * * [simplify]: Extracting #4: cost 1 inf + 738 20.993 * * [simplify]: Extracting #5: cost 0 inf + 1302 20.993 * [simplify]: Simplified to (+.p16 a (/.p16 (+.p16 (+.p16 b a) c) (real->posit16 2))) 20.993 * [simplify]: Simplified (2 1 1 1 1 2 2) to (λ (a b c) (sqrt.p16 (*.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 a (/.p16 (+.p16 (+.p16 b a) c) (real->posit16 2))))) (-.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)))) 20.993 * * * * [progress]: [ 9 / 15 ] simplifiying candidate #posit16 2)) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) a)) (*.p16 (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) b) (-.p16 (/.p16 (+.p16 (+.p16 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))))> 20.994 * [simplify]: Simplifying (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) b) 20.994 * * [simplify]: iters left: 4 (9 enodes) 20.998 * * [simplify]: iters left: 3 (21 enodes) 21.006 * * [simplify]: iters left: 2 (27 enodes) 21.013 * * [simplify]: iters left: 1 (28 enodes) 21.021 * * [simplify]: Extracting #0: cost 1 inf + 0 21.021 * * [simplify]: Extracting #1: cost 3 inf + 0 21.021 * * [simplify]: Extracting #2: cost 4 inf + 1 21.021 * * [simplify]: Extracting #3: cost 10 inf + 1 21.021 * * [simplify]: Extracting #4: cost 5 inf + 47 21.021 * * [simplify]: Extracting #5: cost 1 inf + 738 21.022 * * [simplify]: Extracting #6: cost 0 inf + 1302 21.022 * [simplify]: Simplified to (+.p16 (/.p16 (+.p16 a (+.p16 c b)) (real->posit16 2)) b) 21.022 * [simplify]: Simplified (2 1 1 1 2 1) to (λ (a b c) (sqrt.p16 (*.p16 (/.p16 (*.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) a)) (*.p16 (+.p16 (/.p16 (+.p16 a (+.p16 c b)) (real->posit16 2)) b) (-.p16 (/.p16 (+.p16 (+.p16 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)))) 21.022 * [simplify]: Simplifying (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) b) 21.022 * * [simplify]: iters left: 4 (9 enodes) 21.027 * * [simplify]: iters left: 3 (27 enodes) 21.035 * * [simplify]: iters left: 2 (47 enodes) 21.053 * * [simplify]: iters left: 1 (123 enodes) 21.115 * * [simplify]: Extracting #0: cost 1 inf + 0 21.116 * * [simplify]: Extracting #1: cost 15 inf + 0 21.116 * * [simplify]: Extracting #2: cost 52 inf + 82 21.116 * * [simplify]: Extracting #3: cost 87 inf + 1044 21.117 * * [simplify]: Extracting #4: cost 138 inf + 5615 21.119 * * [simplify]: Extracting #5: cost 116 inf + 19352 21.125 * * [simplify]: Extracting #6: cost 58 inf + 77414 21.135 * * [simplify]: Extracting #7: cost 8 inf + 156974 21.146 * * [simplify]: Extracting #8: cost 0 inf + 175966 21.155 * [simplify]: Simplified to (-.p16 (/.p16 (+.p16 b (+.p16 a c)) (real->posit16 2)) b) 21.155 * [simplify]: Simplified (2 1 1 1 2 2) to (λ (a b c) (sqrt.p16 (*.p16 (/.p16 (*.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) a)) (*.p16 (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) b) (-.p16 (/.p16 (+.p16 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)))) 21.155 * * * * [progress]: [ 10 / 15 ] simplifiying candidate #posit16 2)) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) a)) (+.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (/.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))))> 21.155 * [simplify]: Simplifying (neg.p16 (*.p16 b b)) 21.156 * * [simplify]: iters left: 2 (3 enodes) 21.156 * * [simplify]: iters left: 1 (5 enodes) 21.157 * * [simplify]: Extracting #0: cost 1 inf + 0 21.157 * * [simplify]: Extracting #1: cost 2 inf + 0 21.157 * * [simplify]: Extracting #2: cost 3 inf + 0 21.157 * * [simplify]: Extracting #3: cost 2 inf + 1 21.157 * * [simplify]: Extracting #4: cost 0 inf + 723 21.157 * [simplify]: Simplified to (neg.p16 (*.p16 b b)) 21.157 * [simplify]: Simplified (2 1 1 1 2 2) to (λ (a b c) (sqrt.p16 (*.p16 (/.p16 (*.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) a)) (+.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (/.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)))) 21.157 * * * * [progress]: [ 11 / 15 ] simplifiying candidate #posit16 2)) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) a)) (/.p16 (-.p16 (*.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2))) (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)))) (*.p16 (*.p16 b b) (*.p16 b b))) (+.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (/.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))))> 21.157 * [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))) 21.157 * * [simplify]: iters left: 6 (13 enodes) 21.163 * * [simplify]: iters left: 5 (46 enodes) 21.181 * * [simplify]: iters left: 4 (130 enodes) 21.221 * * [simplify]: Extracting #0: cost 1 inf + 0 21.221 * * [simplify]: Extracting #1: cost 25 inf + 0 21.221 * * [simplify]: Extracting #2: cost 62 inf + 0 21.222 * * [simplify]: Extracting #3: cost 158 inf + 1 21.223 * * [simplify]: Extracting #4: cost 158 inf + 19530 21.230 * * [simplify]: Extracting #5: cost 53 inf + 149926 21.241 * * [simplify]: Extracting #6: cost 3 inf + 237757 21.260 * * [simplify]: Extracting #7: cost 0 inf + 247569 21.283 * [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 b b) (*.p16 b b))) 21.284 * [simplify]: Simplified (2 1 1 1 2 1) to (λ (a b c) (sqrt.p16 (*.p16 (/.p16 (*.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) a)) (/.p16 (-.p16 (*.p16 (*.p16 (/.p16 (+.p16 (+.p16 b a) c) (real->posit16 2)) (/.p16 (+.p16 (+.p16 b a) c) (real->posit16 2))) (*.p16 (/.p16 (+.p16 (+.p16 b a) c) (real->posit16 2)) (/.p16 (+.p16 (+.p16 b a) 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)))) 21.284 * [simplify]: Simplifying (+.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2))) (*.p16 b b)) 21.284 * * [simplify]: iters left: 5 (11 enodes) 21.289 * * [simplify]: iters left: 4 (27 enodes) 21.294 * * [simplify]: iters left: 3 (53 enodes) 21.304 * * [simplify]: iters left: 2 (121 enodes) 21.336 * * [simplify]: iters left: 1 (313 enodes) 21.512 * * [simplify]: Extracting #0: cost 1 inf + 0 21.512 * * [simplify]: Extracting #1: cost 21 inf + 0 21.512 * * [simplify]: Extracting #2: cost 48 inf + 0 21.513 * * [simplify]: Extracting #3: cost 201 inf + 324 21.517 * * [simplify]: Extracting #4: cost 146 inf + 44322 21.531 * * [simplify]: Extracting #5: cost 8 inf + 143661 21.548 * * [simplify]: Extracting #6: cost 0 inf + 151168 21.559 * [simplify]: Simplified to (+.p16 (*.p16 b b) (*.p16 (/.p16 (+.p16 (+.p16 b a) c) (real->posit16 2)) (/.p16 (+.p16 (+.p16 b a) c) (real->posit16 2)))) 21.559 * [simplify]: Simplified (2 1 1 1 2 2) to (λ (a b c) (sqrt.p16 (*.p16 (/.p16 (*.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) a)) (/.p16 (-.p16 (*.p16 (*.p16 (/.p16 (+.p16 (+.p16 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 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 a b) c) (real->posit16 2)) b)) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) c)))) 21.559 * * * * [progress]: [ 12 / 15 ] simplifiying candidate #posit16 2)) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) a)) (-.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (/.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))))> 21.559 * [simplify]: Simplifying (*.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) a)) (-.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2))) (*.p16 b b))) 21.559 * * [simplify]: iters left: 6 (14 enodes) 21.563 * * [simplify]: iters left: 5 (51 enodes) 21.575 * * [simplify]: iters left: 4 (171 enodes) 21.656 * * [simplify]: Extracting #0: cost 1 inf + 0 21.656 * * [simplify]: Extracting #1: cost 46 inf + 0 21.657 * * [simplify]: Extracting #2: cost 203 inf + 0 21.661 * * [simplify]: Extracting #3: cost 243 inf + 32533 21.683 * * [simplify]: Extracting #4: cost 117 inf + 241265 21.705 * * [simplify]: Extracting #5: cost 6 inf + 400335 21.736 * * [simplify]: Extracting #6: cost 0 inf + 412799 21.767 * [simplify]: Simplified to (*.p16 (-.p16 (/.p16 (+.p16 (+.p16 b a) c) (real->posit16 2)) a) (*.p16 (-.p16 (/.p16 (+.p16 (+.p16 b a) c) (real->posit16 2)) b) (*.p16 (+.p16 (/.p16 (+.p16 (+.p16 b a) c) (real->posit16 2)) b) (/.p16 (+.p16 (+.p16 b a) c) (real->posit16 2))))) 21.767 * [simplify]: Simplified (2 1 1 1) to (λ (a b c) (sqrt.p16 (*.p16 (/.p16 (*.p16 (-.p16 (/.p16 (+.p16 (+.p16 b a) c) (real->posit16 2)) a) (*.p16 (-.p16 (/.p16 (+.p16 (+.p16 b a) c) (real->posit16 2)) b) (*.p16 (+.p16 (/.p16 (+.p16 (+.p16 b a) c) (real->posit16 2)) b) (/.p16 (+.p16 (+.p16 b a) c) (real->posit16 2))))) (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) b)) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) c)))) 21.767 * * * * [progress]: [ 13 / 15 ] simplifiying candidate #posit16 2)) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) a)) (-.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (/.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))))> 21.768 * [simplify]: Simplifying (*.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) a)) (-.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2))) (*.p16 b b))) 21.768 * * [simplify]: iters left: 6 (14 enodes) 21.772 * * [simplify]: iters left: 5 (51 enodes) 21.783 * * [simplify]: iters left: 4 (171 enodes) 21.839 * * [simplify]: Extracting #0: cost 1 inf + 0 21.839 * * [simplify]: Extracting #1: cost 46 inf + 0 21.840 * * [simplify]: Extracting #2: cost 203 inf + 0 21.841 * * [simplify]: Extracting #3: cost 243 inf + 32533 21.860 * * [simplify]: Extracting #4: cost 117 inf + 241265 21.892 * * [simplify]: Extracting #5: cost 6 inf + 400335 21.916 * * [simplify]: Extracting #6: cost 0 inf + 412799 21.956 * [simplify]: Simplified to (*.p16 (-.p16 (/.p16 (+.p16 (+.p16 b a) c) (real->posit16 2)) a) (*.p16 (-.p16 (/.p16 (+.p16 (+.p16 b a) c) (real->posit16 2)) b) (*.p16 (+.p16 (/.p16 (+.p16 (+.p16 b a) c) (real->posit16 2)) b) (/.p16 (+.p16 (+.p16 b a) c) (real->posit16 2))))) 21.956 * [simplify]: Simplified (2 1 1 1) to (λ (a b c) (sqrt.p16 (*.p16 (/.p16 (*.p16 (-.p16 (/.p16 (+.p16 (+.p16 b a) c) (real->posit16 2)) a) (*.p16 (-.p16 (/.p16 (+.p16 (+.p16 b a) c) (real->posit16 2)) b) (*.p16 (+.p16 (/.p16 (+.p16 (+.p16 b a) c) (real->posit16 2)) b) (/.p16 (+.p16 (+.p16 b a) c) (real->posit16 2))))) (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) b)) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) c)))) 21.956 * * * * [progress]: [ 14 / 15 ] simplifiying candidate #posit16 2)) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) a)) (-.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (/.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))))> 21.957 * [simplify]: Simplifying (*.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) a)) (-.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2))) (*.p16 b b))) 21.957 * * [simplify]: iters left: 6 (14 enodes) 21.963 * * [simplify]: iters left: 5 (51 enodes) 21.978 * * [simplify]: iters left: 4 (171 enodes) 22.061 * * [simplify]: Extracting #0: cost 1 inf + 0 22.061 * * [simplify]: Extracting #1: cost 46 inf + 0 22.062 * * [simplify]: Extracting #2: cost 203 inf + 0 22.064 * * [simplify]: Extracting #3: cost 243 inf + 32533 22.075 * * [simplify]: Extracting #4: cost 117 inf + 241265 22.101 * * [simplify]: Extracting #5: cost 6 inf + 400335 22.124 * * [simplify]: Extracting #6: cost 0 inf + 412799 22.164 * [simplify]: Simplified to (*.p16 (-.p16 (/.p16 (+.p16 (+.p16 b a) c) (real->posit16 2)) a) (*.p16 (-.p16 (/.p16 (+.p16 (+.p16 b a) c) (real->posit16 2)) b) (*.p16 (+.p16 (/.p16 (+.p16 (+.p16 b a) c) (real->posit16 2)) b) (/.p16 (+.p16 (+.p16 b a) c) (real->posit16 2))))) 22.164 * [simplify]: Simplified (2 1 1 1) to (λ (a b c) (sqrt.p16 (*.p16 (/.p16 (*.p16 (-.p16 (/.p16 (+.p16 (+.p16 b a) c) (real->posit16 2)) a) (*.p16 (-.p16 (/.p16 (+.p16 (+.p16 b a) c) (real->posit16 2)) b) (*.p16 (+.p16 (/.p16 (+.p16 (+.p16 b a) c) (real->posit16 2)) b) (/.p16 (+.p16 (+.p16 b a) c) (real->posit16 2))))) (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) b)) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) c)))) 22.164 * * * * [progress]: [ 15 / 15 ] simplifiying candidate #posit16 2)) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) a)) (-.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (/.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))))> 22.165 * [simplify]: Simplifying (*.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) a)) (-.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2))) (*.p16 b b))) 22.165 * * [simplify]: iters left: 6 (14 enodes) 22.172 * * [simplify]: iters left: 5 (51 enodes) 22.190 * * [simplify]: iters left: 4 (171 enodes) 22.266 * * [simplify]: Extracting #0: cost 1 inf + 0 22.267 * * [simplify]: Extracting #1: cost 46 inf + 0 22.267 * * [simplify]: Extracting #2: cost 203 inf + 0 22.269 * * [simplify]: Extracting #3: cost 243 inf + 32533 22.281 * * [simplify]: Extracting #4: cost 117 inf + 241265 22.320 * * [simplify]: Extracting #5: cost 6 inf + 400335 22.364 * * [simplify]: Extracting #6: cost 0 inf + 412799 22.408 * [simplify]: Simplified to (*.p16 (-.p16 (/.p16 (+.p16 (+.p16 b a) c) (real->posit16 2)) a) (*.p16 (-.p16 (/.p16 (+.p16 (+.p16 b a) c) (real->posit16 2)) b) (*.p16 (+.p16 (/.p16 (+.p16 (+.p16 b a) c) (real->posit16 2)) b) (/.p16 (+.p16 (+.p16 b a) c) (real->posit16 2))))) 22.408 * [simplify]: Simplified (2 1 1 1) to (λ (a b c) (sqrt.p16 (*.p16 (/.p16 (*.p16 (-.p16 (/.p16 (+.p16 (+.p16 b a) c) (real->posit16 2)) a) (*.p16 (-.p16 (/.p16 (+.p16 (+.p16 b a) c) (real->posit16 2)) b) (*.p16 (+.p16 (/.p16 (+.p16 (+.p16 b a) c) (real->posit16 2)) b) (/.p16 (+.p16 (+.p16 b a) c) (real->posit16 2))))) (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) b)) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) c)))) 22.409 * * * [progress]: adding candidates to table 23.178 * [progress]: [Phase 3 of 3] Extracting. 23.178 * * [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 a b) c) (real->posit16 2)) (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2))) (*.p16 c c)) (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) c)))))> #posit16 2)) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) a)) (/.p16 (-.p16 (*.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2))) (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)))) (*.p16 (*.p16 b b) (*.p16 b b))) (*.p16 (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) b) (+.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2))) (*.p16 b b))))) (/.p16 (-.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2))) (*.p16 c c)) (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) c)))))> #posit16 2)) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) a)) (/.p16 (-.p16 (*.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2))) (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)))) (*.p16 (*.p16 b b) (*.p16 b b))) (+.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2))) (*.p16 b b)))) (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) b)) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) c))))> #posit16 2)) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) a)) (*.p16 (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) b) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) b))) (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) b)) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) c))))> #posit16 2)) (-.p16 (*.p16 (/.p16 (+.p16 (+.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)) a)) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) c))))> #posit16 2)) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) a)) (/.p16 (-.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2))) (*.p16 b b)) (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) b))) (/.p16 (-.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2))) (*.p16 c c)) (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) c)))))> #posit16 2)) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) a)) (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2))) (*.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) a)) (neg.p16 b))) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) c))))>) 23.189 * * * [regime-changes]: Trying 3 branch expressions: (c b a) 23.189 * * * * [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 a b) c) (real->posit16 2)) (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2))) (*.p16 c c)) (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) c)))))> #posit16 2)) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) a)) (/.p16 (-.p16 (*.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2))) (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)))) (*.p16 (*.p16 b b) (*.p16 b b))) (*.p16 (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) b) (+.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2))) (*.p16 b b))))) (/.p16 (-.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2))) (*.p16 c c)) (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) c)))))> #posit16 2)) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) a)) (/.p16 (-.p16 (*.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2))) (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)))) (*.p16 (*.p16 b b) (*.p16 b b))) (+.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2))) (*.p16 b b)))) (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) b)) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) c))))> #posit16 2)) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) a)) (*.p16 (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) b) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) b))) (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) b)) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) c))))> #posit16 2)) (-.p16 (*.p16 (/.p16 (+.p16 (+.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)) a)) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) c))))> #posit16 2)) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) a)) (/.p16 (-.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2))) (*.p16 b b)) (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) b))) (/.p16 (-.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2))) (*.p16 c c)) (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) c)))))> #posit16 2)) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) a)) (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2))) (*.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) a)) (neg.p16 b))) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) c))))>) 23.444 * * * * [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 a b) c) (real->posit16 2)) (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2))) (*.p16 c c)) (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) c)))))> #posit16 2)) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) a)) (/.p16 (-.p16 (*.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2))) (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)))) (*.p16 (*.p16 b b) (*.p16 b b))) (*.p16 (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) b) (+.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2))) (*.p16 b b))))) (/.p16 (-.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2))) (*.p16 c c)) (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) c)))))> #posit16 2)) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) a)) (/.p16 (-.p16 (*.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2))) (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)))) (*.p16 (*.p16 b b) (*.p16 b b))) (+.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2))) (*.p16 b b)))) (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) b)) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) c))))> #posit16 2)) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) a)) (*.p16 (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) b) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) b))) (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) b)) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) c))))> #posit16 2)) (-.p16 (*.p16 (/.p16 (+.p16 (+.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)) a)) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) c))))> #posit16 2)) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) a)) (/.p16 (-.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2))) (*.p16 b b)) (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) b))) (/.p16 (-.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2))) (*.p16 c c)) (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) c)))))> #posit16 2)) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) a)) (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2))) (*.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) a)) (neg.p16 b))) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) c))))>) 23.726 * * * * [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 a b) c) (real->posit16 2)) (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2))) (*.p16 c c)) (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) c)))))> #posit16 2)) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) a)) (/.p16 (-.p16 (*.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2))) (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)))) (*.p16 (*.p16 b b) (*.p16 b b))) (*.p16 (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) b) (+.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2))) (*.p16 b b))))) (/.p16 (-.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2))) (*.p16 c c)) (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) c)))))> #posit16 2)) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) a)) (/.p16 (-.p16 (*.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2))) (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)))) (*.p16 (*.p16 b b) (*.p16 b b))) (+.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2))) (*.p16 b b)))) (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) b)) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) c))))> #posit16 2)) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) a)) (*.p16 (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) b) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) b))) (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) b)) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) c))))> #posit16 2)) (-.p16 (*.p16 (/.p16 (+.p16 (+.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)) a)) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) c))))> #posit16 2)) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) a)) (/.p16 (-.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2))) (*.p16 b b)) (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) b))) (/.p16 (-.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2))) (*.p16 c c)) (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) c)))))> #posit16 2)) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) a)) (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2))) (*.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) a)) (neg.p16 b))) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) c))))>) 23.946 * * * [regime]: Found split indices: #