0.002 * [progress]: [Phase 1 of 3] Setting up. 0.002 * * * [progress]: [1/2] Preparing points 0.002 * * * * [points]: Sampling 256 additional inputs, on iter 0 have 0 / 256 0.004 * * * * [points]: Computing exacts on every 16 of 256 points to ramp up precision 0.008 * * * * [points]: Setting MPFR precision to 64 0.011 * * * * [points]: Setting MPFR precision to 320 0.012 * * * * [points]: Computing exacts on every 8 of 256 points to ramp up precision 0.018 * * * * [points]: Setting MPFR precision to 64 0.021 * * * * [points]: Setting MPFR precision to 320 0.024 * * * * [points]: Computing exacts on every 4 of 256 points to ramp up precision 0.030 * * * * [points]: Setting MPFR precision to 64 0.035 * * * * [points]: Setting MPFR precision to 320 0.041 * * * * [points]: Computing exacts on every 2 of 256 points to ramp up precision 0.047 * * * * [points]: Setting MPFR precision to 64 0.057 * * * * [points]: Setting MPFR precision to 320 0.078 * * * * [points]: Computing exacts for 256 points 0.081 * * * * [points]: Setting MPFR precision to 64 0.099 * * * * [points]: Setting MPFR precision to 320 0.116 * * * * [points]: Filtering points with unrepresentable outputs 0.116 * * * * [points]: Sampling 227 additional inputs, on iter 1 have 29 / 256 0.117 * * * * [points]: Computing exacts on every 14 of 227 points to ramp up precision 0.121 * * * * [points]: Setting MPFR precision to 64 0.122 * * * * [points]: Setting MPFR precision to 320 0.123 * * * * [points]: Computing exacts on every 7 of 227 points to ramp up precision 0.126 * * * * [points]: Setting MPFR precision to 64 0.129 * * * * [points]: Setting MPFR precision to 320 0.130 * * * * [points]: Computing exacts on every 3 of 227 points to ramp up precision 0.134 * * * * [points]: Setting MPFR precision to 64 0.137 * * * * [points]: Setting MPFR precision to 320 0.142 * * * * [points]: Computing exacts for 227 points 0.145 * * * * [points]: Setting MPFR precision to 64 0.160 * * * * [points]: Setting MPFR precision to 320 0.176 * * * * [points]: Filtering points with unrepresentable outputs 0.177 * * * * [points]: Sampling 199 additional inputs, on iter 2 have 57 / 256 0.474 * * * * [points]: Computing exacts on every 12 of 199 points to ramp up precision 0.480 * * * * [points]: Setting MPFR precision to 64 0.483 * * * * [points]: Setting MPFR precision to 320 0.485 * * * * [points]: Computing exacts on every 6 of 199 points to ramp up precision 0.491 * * * * [points]: Setting MPFR precision to 64 0.495 * * * * [points]: Setting MPFR precision to 320 0.499 * * * * [points]: Computing exacts on every 3 of 199 points to ramp up precision 0.505 * * * * [points]: Setting MPFR precision to 64 0.512 * * * * [points]: Setting MPFR precision to 320 0.519 * * * * [points]: Computing exacts for 199 points 0.525 * * * * [points]: Setting MPFR precision to 64 0.550 * * * * [points]: Setting MPFR precision to 320 0.577 * * * * [points]: Filtering points with unrepresentable outputs 0.577 * * * * [points]: Sampling 176 additional inputs, on iter 3 have 80 / 256 0.579 * * * * [points]: Computing exacts on every 11 of 176 points to ramp up precision 0.585 * * * * [points]: Setting MPFR precision to 64 0.587 * * * * [points]: Setting MPFR precision to 320 0.589 * * * * [points]: Computing exacts on every 5 of 176 points to ramp up precision 0.596 * * * * [points]: Setting MPFR precision to 64 0.600 * * * * [points]: Setting MPFR precision to 320 0.604 * * * * [points]: Computing exacts on every 2 of 176 points to ramp up precision 0.610 * * * * [points]: Setting MPFR precision to 64 0.617 * * * * [points]: Setting MPFR precision to 320 0.621 * * * * [points]: Computing exacts for 176 points 0.625 * * * * [points]: Setting MPFR precision to 64 0.658 * * * * [points]: Setting MPFR precision to 320 0.670 * * * * [points]: Filtering points with unrepresentable outputs 0.671 * * * * [points]: Sampling 158 additional inputs, on iter 4 have 98 / 256 0.671 * * * * [points]: Computing exacts on every 9 of 158 points to ramp up precision 0.675 * * * * [points]: Setting MPFR precision to 64 0.676 * * * * [points]: Setting MPFR precision to 320 0.677 * * * * [points]: Computing exacts on every 4 of 158 points to ramp up precision 0.682 * * * * [points]: Setting MPFR precision to 64 0.685 * * * * [points]: Setting MPFR precision to 320 0.689 * * * * [points]: Computing exacts on every 2 of 158 points to ramp up precision 0.695 * * * * [points]: Setting MPFR precision to 64 0.702 * * * * [points]: Setting MPFR precision to 320 0.708 * * * * [points]: Computing exacts for 158 points 0.715 * * * * [points]: Setting MPFR precision to 64 0.734 * * * * [points]: Setting MPFR precision to 320 0.752 * * * * [points]: Filtering points with unrepresentable outputs 0.752 * * * * [points]: Sampling 138 additional inputs, on iter 5 have 118 / 256 0.754 * * * * [points]: Computing exacts on every 8 of 138 points to ramp up precision 0.759 * * * * [points]: Setting MPFR precision to 64 0.761 * * * * [points]: Setting MPFR precision to 320 0.763 * * * * [points]: Computing exacts on every 4 of 138 points to ramp up precision 0.769 * * * * [points]: Setting MPFR precision to 64 0.772 * * * * [points]: Setting MPFR precision to 320 0.776 * * * * [points]: Computing exacts on every 2 of 138 points to ramp up precision 0.781 * * * * [points]: Setting MPFR precision to 64 0.787 * * * * [points]: Setting MPFR precision to 320 0.792 * * * * [points]: Computing exacts for 138 points 0.820 * * * * [points]: Setting MPFR precision to 64 0.837 * * * * [points]: Setting MPFR precision to 320 0.851 * * * * [points]: Filtering points with unrepresentable outputs 0.851 * * * * [points]: Sampling 120 additional inputs, on iter 6 have 136 / 256 0.852 * * * * [points]: Computing exacts on every 7 of 120 points to ramp up precision 0.855 * * * * [points]: Setting MPFR precision to 64 0.856 * * * * [points]: Setting MPFR precision to 320 0.858 * * * * [points]: Computing exacts on every 3 of 120 points to ramp up precision 0.861 * * * * [points]: Setting MPFR precision to 64 0.863 * * * * [points]: Setting MPFR precision to 320 0.865 * * * * [points]: Computing exacts for 120 points 0.868 * * * * [points]: Setting MPFR precision to 64 0.876 * * * * [points]: Setting MPFR precision to 320 0.885 * * * * [points]: Filtering points with unrepresentable outputs 0.885 * * * * [points]: Sampling 110 additional inputs, on iter 7 have 146 / 256 0.885 * * * * [points]: Computing exacts on every 6 of 110 points to ramp up precision 0.889 * * * * [points]: Setting MPFR precision to 64 0.890 * * * * [points]: Setting MPFR precision to 320 0.891 * * * * [points]: Computing exacts on every 3 of 110 points to ramp up precision 0.894 * * * * [points]: Setting MPFR precision to 64 0.896 * * * * [points]: Setting MPFR precision to 320 0.898 * * * * [points]: Computing exacts for 110 points 0.901 * * * * [points]: Setting MPFR precision to 64 0.908 * * * * [points]: Setting MPFR precision to 320 0.916 * * * * [points]: Filtering points with unrepresentable outputs 0.916 * * * * [points]: Sampling 96 additional inputs, on iter 8 have 160 / 256 0.916 * * * * [points]: Computing exacts on every 6 of 96 points to ramp up precision 0.920 * * * * [points]: Setting MPFR precision to 64 0.921 * * * * [points]: Setting MPFR precision to 320 0.922 * * * * [points]: Computing exacts on every 3 of 96 points to ramp up precision 0.946 * * * * [points]: Setting MPFR precision to 64 0.948 * * * * [points]: Setting MPFR precision to 320 0.950 * * * * [points]: Computing exacts for 96 points 0.953 * * * * [points]: Setting MPFR precision to 64 0.960 * * * * [points]: Setting MPFR precision to 320 0.967 * * * * [points]: Filtering points with unrepresentable outputs 0.967 * * * * [points]: Sampling 75 additional inputs, on iter 9 have 181 / 256 0.967 * * * * [points]: Computing exacts on every 4 of 75 points to ramp up precision 0.971 * * * * [points]: Setting MPFR precision to 64 0.972 * * * * [points]: Setting MPFR precision to 320 0.973 * * * * [points]: Computing exacts on every 2 of 75 points to ramp up precision 0.976 * * * * [points]: Setting MPFR precision to 64 0.978 * * * * [points]: Setting MPFR precision to 320 0.980 * * * * [points]: Computing exacts for 75 points 0.984 * * * * [points]: Setting MPFR precision to 64 0.989 * * * * [points]: Setting MPFR precision to 320 0.995 * * * * [points]: Filtering points with unrepresentable outputs 0.995 * * * * [points]: Sampling 64 additional inputs, on iter 10 have 192 / 256 0.995 * * * * [points]: Computing exacts on every 4 of 64 points to ramp up precision 0.998 * * * * [points]: Setting MPFR precision to 64 0.999 * * * * [points]: Setting MPFR precision to 320 1.000 * * * * [points]: Computing exacts on every 2 of 64 points to ramp up precision 1.003 * * * * [points]: Setting MPFR precision to 64 1.005 * * * * [points]: Setting MPFR precision to 320 1.006 * * * * [points]: Computing exacts for 64 points 1.009 * * * * [points]: Setting MPFR precision to 64 1.014 * * * * [points]: Setting MPFR precision to 320 1.018 * * * * [points]: Filtering points with unrepresentable outputs 1.018 * * * * [points]: Sampling 55 additional inputs, on iter 11 have 201 / 256 1.019 * * * * [points]: Computing exacts on every 3 of 55 points to ramp up precision 1.022 * * * * [points]: Setting MPFR precision to 64 1.023 * * * * [points]: Setting MPFR precision to 320 1.024 * * * * [points]: Computing exacts for 55 points 1.030 * * * * [points]: Setting MPFR precision to 64 1.037 * * * * [points]: Setting MPFR precision to 320 1.067 * * * * [points]: Filtering points with unrepresentable outputs 1.067 * * * * [points]: Sampling 49 additional inputs, on iter 12 have 207 / 256 1.067 * * * * [points]: Computing exacts on every 3 of 49 points to ramp up precision 1.071 * * * * [points]: Setting MPFR precision to 64 1.072 * * * * [points]: Setting MPFR precision to 320 1.073 * * * * [points]: Computing exacts for 49 points 1.076 * * * * [points]: Setting MPFR precision to 64 1.079 * * * * [points]: Setting MPFR precision to 320 1.083 * * * * [points]: Filtering points with unrepresentable outputs 1.083 * * * * [points]: Sampling 41 additional inputs, on iter 13 have 215 / 256 1.083 * * * * [points]: Computing exacts on every 2 of 41 points to ramp up precision 1.086 * * * * [points]: Setting MPFR precision to 64 1.087 * * * * [points]: Setting MPFR precision to 320 1.088 * * * * [points]: Computing exacts for 41 points 1.092 * * * * [points]: Setting MPFR precision to 64 1.094 * * * * [points]: Setting MPFR precision to 320 1.097 * * * * [points]: Filtering points with unrepresentable outputs 1.097 * * * * [points]: Sampling 37 additional inputs, on iter 14 have 219 / 256 1.097 * * * * [points]: Computing exacts on every 2 of 37 points to ramp up precision 1.101 * * * * [points]: Setting MPFR precision to 64 1.102 * * * * [points]: Setting MPFR precision to 320 1.102 * * * * [points]: Computing exacts for 37 points 1.106 * * * * [points]: Setting MPFR precision to 64 1.108 * * * * [points]: Setting MPFR precision to 320 1.111 * * * * [points]: Filtering points with unrepresentable outputs 1.111 * * * * [points]: Sampling 31 additional inputs, on iter 15 have 225 / 256 1.111 * * * * [points]: Computing exacts for 31 points 1.114 * * * * [points]: Setting MPFR precision to 64 1.116 * * * * [points]: Setting MPFR precision to 320 1.119 * * * * [points]: Filtering points with unrepresentable outputs 1.119 * * * * [points]: Sampling 25 additional inputs, on iter 16 have 231 / 256 1.119 * * * * [points]: Computing exacts for 25 points 1.122 * * * * [points]: Setting MPFR precision to 64 1.124 * * * * [points]: Setting MPFR precision to 320 1.126 * * * * [points]: Filtering points with unrepresentable outputs 1.126 * * * * [points]: Sampling 23 additional inputs, on iter 17 have 233 / 256 1.126 * * * * [points]: Computing exacts for 23 points 1.130 * * * * [points]: Setting MPFR precision to 64 1.131 * * * * [points]: Setting MPFR precision to 320 1.133 * * * * [points]: Filtering points with unrepresentable outputs 1.133 * * * * [points]: Sampling 20 additional inputs, on iter 18 have 236 / 256 1.133 * * * * [points]: Computing exacts for 20 points 1.137 * * * * [points]: Setting MPFR precision to 64 1.138 * * * * [points]: Setting MPFR precision to 320 1.139 * * * * [points]: Filtering points with unrepresentable outputs 1.139 * * * * [points]: Sampling 19 additional inputs, on iter 19 have 237 / 256 1.140 * * * * [points]: Computing exacts for 19 points 1.143 * * * * [points]: Setting MPFR precision to 64 1.144 * * * * [points]: Setting MPFR precision to 320 1.146 * * * * [points]: Filtering points with unrepresentable outputs 1.146 * * * * [points]: Sampling 14 additional inputs, on iter 20 have 242 / 256 1.146 * * * * [points]: Computing exacts for 14 points 1.165 * * * * [points]: Setting MPFR precision to 64 1.166 * * * * [points]: Setting MPFR precision to 320 1.167 * * * * [points]: Filtering points with unrepresentable outputs 1.167 * * * * [points]: Sampling 13 additional inputs, on iter 21 have 243 / 256 1.167 * * * * [points]: Computing exacts for 13 points 1.170 * * * * [points]: Setting MPFR precision to 64 1.171 * * * * [points]: Setting MPFR precision to 320 1.172 * * * * [points]: Filtering points with unrepresentable outputs 1.172 * * * * [points]: Sampling 12 additional inputs, on iter 22 have 244 / 256 1.172 * * * * [points]: Computing exacts for 12 points 1.176 * * * * [points]: Setting MPFR precision to 64 1.177 * * * * [points]: Setting MPFR precision to 320 1.177 * * * * [points]: Filtering points with unrepresentable outputs 1.178 * * * * [points]: Sampling 12 additional inputs, on iter 23 have 244 / 256 1.178 * * * * [points]: Computing exacts for 12 points 1.181 * * * * [points]: Setting MPFR precision to 64 1.182 * * * * [points]: Setting MPFR precision to 320 1.182 * * * * [points]: Filtering points with unrepresentable outputs 1.182 * * * * [points]: Sampling 9 additional inputs, on iter 24 have 247 / 256 1.183 * * * * [points]: Computing exacts for 9 points 1.186 * * * * [points]: Setting MPFR precision to 64 1.186 * * * * [points]: Setting MPFR precision to 320 1.187 * * * * [points]: Filtering points with unrepresentable outputs 1.187 * * * * [points]: Sampling 8 additional inputs, on iter 25 have 248 / 256 1.187 * * * * [points]: Computing exacts for 8 points 1.190 * * * * [points]: Setting MPFR precision to 64 1.191 * * * * [points]: Setting MPFR precision to 320 1.192 * * * * [points]: Filtering points with unrepresentable outputs 1.192 * * * * [points]: Sampling 8 additional inputs, on iter 26 have 248 / 256 1.192 * * * * [points]: Computing exacts for 8 points 1.195 * * * * [points]: Setting MPFR precision to 64 1.196 * * * * [points]: Setting MPFR precision to 320 1.196 * * * * [points]: Filtering points with unrepresentable outputs 1.196 * * * * [points]: Sampling 8 additional inputs, on iter 27 have 248 / 256 1.196 * * * * [points]: Computing exacts for 8 points 1.199 * * * * [points]: Setting MPFR precision to 64 1.200 * * * * [points]: Setting MPFR precision to 320 1.201 * * * * [points]: Filtering points with unrepresentable outputs 1.201 * * * * [points]: Sampling 7 additional inputs, on iter 28 have 249 / 256 1.201 * * * * [points]: Computing exacts for 7 points 1.204 * * * * [points]: Setting MPFR precision to 64 1.204 * * * * [points]: Setting MPFR precision to 320 1.205 * * * * [points]: Filtering points with unrepresentable outputs 1.205 * * * * [points]: Sampling 7 additional inputs, on iter 29 have 249 / 256 1.205 * * * * [points]: Computing exacts for 7 points 1.208 * * * * [points]: Setting MPFR precision to 64 1.209 * * * * [points]: Setting MPFR precision to 320 1.209 * * * * [points]: Filtering points with unrepresentable outputs 1.209 * * * * [points]: Sampling 5 additional inputs, on iter 30 have 251 / 256 1.209 * * * * [points]: Computing exacts for 5 points 1.212 * * * * [points]: Setting MPFR precision to 64 1.213 * * * * [points]: Setting MPFR precision to 320 1.213 * * * * [points]: Filtering points with unrepresentable outputs 1.213 * * * * [points]: Sampling 5 additional inputs, on iter 31 have 251 / 256 1.213 * * * * [points]: Computing exacts for 5 points 1.217 * * * * [points]: Setting MPFR precision to 64 1.217 * * * * [points]: Setting MPFR precision to 320 1.217 * * * * [points]: Filtering points with unrepresentable outputs 1.217 * * * * [points]: Sampling 4 additional inputs, on iter 32 have 252 / 256 1.217 * * * * [points]: Computing exacts for 4 points 1.221 * * * * [points]: Setting MPFR precision to 64 1.221 * * * * [points]: Setting MPFR precision to 320 1.221 * * * * [points]: Filtering points with unrepresentable outputs 1.221 * * * * [points]: Sampling 4 additional inputs, on iter 33 have 252 / 256 1.221 * * * * [points]: Computing exacts for 4 points 1.224 * * * * [points]: Setting MPFR precision to 64 1.225 * * * * [points]: Setting MPFR precision to 320 1.225 * * * * [points]: Filtering points with unrepresentable outputs 1.225 * * * * [points]: Sampling 4 additional inputs, on iter 34 have 252 / 256 1.225 * * * * [points]: Computing exacts for 4 points 1.228 * * * * [points]: Setting MPFR precision to 64 1.229 * * * * [points]: Setting MPFR precision to 320 1.229 * * * * [points]: Filtering points with unrepresentable outputs 1.229 * * * * [points]: Sampling 4 additional inputs, on iter 35 have 252 / 256 1.229 * * * * [points]: Computing exacts for 4 points 1.232 * * * * [points]: Setting MPFR precision to 64 1.233 * * * * [points]: Setting MPFR precision to 320 1.233 * * * * [points]: Filtering points with unrepresentable outputs 1.233 * * * * [points]: Sampling 4 additional inputs, on iter 36 have 252 / 256 1.233 * * * * [points]: Computing exacts for 4 points 1.246 * * * * [points]: Setting MPFR precision to 64 1.247 * * * * [points]: Setting MPFR precision to 320 1.247 * * * * [points]: Filtering points with unrepresentable outputs 1.247 * * * * [points]: Sampling 4 additional inputs, on iter 37 have 253 / 256 1.247 * * * * [points]: Computing exacts for 4 points 1.250 * * * * [points]: Setting MPFR precision to 64 1.250 * * * * [points]: Setting MPFR precision to 320 1.251 * * * * [points]: Filtering points with unrepresentable outputs 1.251 * * * * [points]: Sampling 4 additional inputs, on iter 38 have 254 / 256 1.251 * * * * [points]: Computing exacts for 4 points 1.254 * * * * [points]: Setting MPFR precision to 64 1.254 * * * * [points]: Setting MPFR precision to 320 1.254 * * * * [points]: Filtering points with unrepresentable outputs 1.254 * * * * [points]: Sampling 4 additional inputs, on iter 39 have 254 / 256 1.254 * * * * [points]: Computing exacts for 4 points 1.258 * * * * [points]: Setting MPFR precision to 64 1.258 * * * * [points]: Setting MPFR precision to 320 1.258 * * * * [points]: Filtering points with unrepresentable outputs 1.258 * * * * [points]: Sampled 257 points with exact outputs 1.258 * * * [progress]: [2/2] Setting up program. 1.268 * [progress]: [Phase 2 of 3] Improving. 1.268 * * * * [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.269 * [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.269 * * [simplify]: iters left: 6 (15 enodes) 1.272 * * [simplify]: iters left: 5 (54 enodes) 1.283 * * [simplify]: iters left: 4 (174 enodes) 1.370 * * [simplify]: Extracting #0: cost 1 inf + 0 1.370 * * [simplify]: Extracting #1: cost 2 inf + 0 1.370 * * [simplify]: Extracting #2: cost 52 inf + 0 1.370 * * [simplify]: Extracting #3: cost 218 inf + 0 1.371 * * [simplify]: Extracting #4: cost 350 inf + 488 1.376 * * [simplify]: Extracting #5: cost 271 inf + 83278 1.390 * * [simplify]: Extracting #6: cost 99 inf + 301152 1.431 * * [simplify]: Extracting #7: cost 13 inf + 445414 1.475 * * [simplify]: Extracting #8: cost 0 inf + 471346 1.530 * [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.530 * [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.557 * * [progress]: iteration 1 / 4 1.557 * * * [progress]: picking best candidate 1.568 * * * * [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.568 * * * [progress]: localizing error 1.771 * * * [progress]: generating rewritten candidates 1.771 * * * * [progress]: [ 1 / 4 ] rewriting at (2 1 2) 1.793 * * * * [progress]: [ 2 / 4 ] rewriting at (2 1 1 2) 1.819 * * * * [progress]: [ 3 / 4 ] rewriting at (2 1 1 1 2) 1.842 * * * * [progress]: [ 4 / 4 ] rewriting at (2 1 1) 1.870 * * * [progress]: generating series expansions 1.870 * * * * [progress]: [ 1 / 4 ] generating series at (2 1 2) 1.871 * * * * [progress]: [ 2 / 4 ] generating series at (2 1 1 2) 1.871 * * * * [progress]: [ 3 / 4 ] generating series at (2 1 1 1 2) 1.871 * * * * [progress]: [ 4 / 4 ] generating series at (2 1 1) 1.871 * * * [progress]: simplifying candidates 1.871 * * * * [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)))))> 1.871 * [simplify]: Simplifying (neg.p16 c) 1.871 * * [simplify]: iters left: 1 (2 enodes) 1.871 * * [simplify]: Extracting #0: cost 1 inf + 0 1.871 * * [simplify]: Extracting #1: cost 2 inf + 0 1.871 * * [simplify]: Extracting #2: cost 1 inf + 1 1.871 * * [simplify]: Extracting #3: cost 0 inf + 82 1.871 * [simplify]: Simplified to (neg.p16 c) 1.871 * [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))))) 1.872 * * * * [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)))))> 1.872 * [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)) 1.872 * * [simplify]: iters left: 5 (11 enodes) 1.874 * * [simplify]: iters left: 4 (36 enodes) 1.881 * * [simplify]: iters left: 3 (93 enodes) 1.902 * * [simplify]: iters left: 2 (310 enodes) 2.039 * * [simplify]: Extracting #0: cost 1 inf + 0 2.039 * * [simplify]: Extracting #1: cost 32 inf + 0 2.039 * * [simplify]: Extracting #2: cost 177 inf + 0 2.040 * * [simplify]: Extracting #3: cost 262 inf + 323 2.043 * * [simplify]: Extracting #4: cost 417 inf + 52622 2.067 * * [simplify]: Extracting #5: cost 157 inf + 465463 2.128 * * [simplify]: Extracting #6: cost 2 inf + 707329 2.182 * * [simplify]: Extracting #7: cost 0 inf + 711417 2.224 * [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.224 * [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.225 * [simplify]: Simplifying (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) c) 2.225 * * [simplify]: iters left: 4 (9 enodes) 2.227 * * [simplify]: iters left: 3 (21 enodes) 2.230 * * [simplify]: iters left: 2 (27 enodes) 2.234 * * [simplify]: iters left: 1 (28 enodes) 2.238 * * [simplify]: Extracting #0: cost 1 inf + 0 2.238 * * [simplify]: Extracting #1: cost 3 inf + 0 2.238 * * [simplify]: Extracting #2: cost 4 inf + 1 2.238 * * [simplify]: Extracting #3: cost 10 inf + 1 2.238 * * [simplify]: Extracting #4: cost 5 inf + 47 2.238 * * [simplify]: Extracting #5: cost 1 inf + 738 2.238 * * [simplify]: Extracting #6: cost 0 inf + 1302 2.238 * [simplify]: Simplified to (+.p16 c (/.p16 (+.p16 a (+.p16 c b)) (real->posit16 2))) 2.238 * [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.238 * * * * [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.238 * [simplify]: Simplifying (neg.p16 b) 2.238 * * [simplify]: iters left: 1 (2 enodes) 2.239 * * [simplify]: Extracting #0: cost 1 inf + 0 2.239 * * [simplify]: Extracting #1: cost 2 inf + 0 2.239 * * [simplify]: Extracting #2: cost 1 inf + 1 2.239 * * [simplify]: Extracting #3: cost 0 inf + 82 2.239 * [simplify]: Simplified to (neg.p16 b) 2.239 * [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.239 * * * * [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.239 * [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.239 * * [simplify]: iters left: 5 (11 enodes) 2.242 * * [simplify]: iters left: 4 (36 enodes) 2.248 * * [simplify]: iters left: 3 (93 enodes) 2.268 * * [simplify]: iters left: 2 (310 enodes) 2.471 * * [simplify]: Extracting #0: cost 1 inf + 0 2.471 * * [simplify]: Extracting #1: cost 32 inf + 0 2.471 * * [simplify]: Extracting #2: cost 177 inf + 0 2.472 * * [simplify]: Extracting #3: cost 260 inf + 323 2.475 * * [simplify]: Extracting #4: cost 456 inf + 5597 2.491 * * [simplify]: Extracting #5: cost 278 inf + 236939 2.525 * * [simplify]: Extracting #6: cost 27 inf + 652788 2.569 * * [simplify]: Extracting #7: cost 2 inf + 706688 2.610 * * [simplify]: Extracting #8: cost 0 inf + 713376 2.652 * [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)) 2.652 * [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)))) 2.653 * [simplify]: Simplifying (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) b) 2.653 * * [simplify]: iters left: 4 (9 enodes) 2.655 * * [simplify]: iters left: 3 (21 enodes) 2.658 * * [simplify]: iters left: 2 (27 enodes) 2.664 * * [simplify]: iters left: 1 (28 enodes) 2.670 * * [simplify]: Extracting #0: cost 1 inf + 0 2.670 * * [simplify]: Extracting #1: cost 3 inf + 0 2.670 * * [simplify]: Extracting #2: cost 4 inf + 1 2.670 * * [simplify]: Extracting #3: cost 10 inf + 1 2.670 * * [simplify]: Extracting #4: cost 5 inf + 47 2.670 * * [simplify]: Extracting #5: cost 1 inf + 738 2.671 * * [simplify]: Extracting #6: cost 0 inf + 1302 2.671 * [simplify]: Simplified to (+.p16 (/.p16 (+.p16 a (+.p16 c b)) (real->posit16 2)) b) 2.671 * [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)))) 2.671 * * * * [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))))> 2.671 * [simplify]: Simplifying (neg.p16 a) 2.671 * * [simplify]: iters left: 1 (2 enodes) 2.672 * * [simplify]: Extracting #0: cost 1 inf + 0 2.672 * * [simplify]: Extracting #1: cost 2 inf + 0 2.672 * * [simplify]: Extracting #2: cost 1 inf + 1 2.672 * * [simplify]: Extracting #3: cost 0 inf + 82 2.672 * [simplify]: Simplified to (neg.p16 a) 2.673 * [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)))) 2.673 * * * * [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))))> 2.673 * [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)) 2.673 * * [simplify]: iters left: 5 (11 enodes) 2.677 * * [simplify]: iters left: 4 (36 enodes) 2.685 * * [simplify]: iters left: 3 (93 enodes) 2.705 * * [simplify]: iters left: 2 (310 enodes) 2.834 * * [simplify]: Extracting #0: cost 1 inf + 0 2.834 * * [simplify]: Extracting #1: cost 32 inf + 0 2.835 * * [simplify]: Extracting #2: cost 177 inf + 0 2.835 * * [simplify]: Extracting #3: cost 262 inf + 323 2.839 * * [simplify]: Extracting #4: cost 416 inf + 51663 2.864 * * [simplify]: Extracting #5: cost 116 inf + 501475 2.903 * * [simplify]: Extracting #6: cost 0 inf + 713857 2.945 * * [simplify]: Extracting #7: cost 0 inf + 713577 2.987 * [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)) 2.987 * [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)))) 2.988 * [simplify]: Simplifying (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) a) 2.988 * * [simplify]: iters left: 4 (9 enodes) 2.990 * * [simplify]: iters left: 3 (21 enodes) 2.993 * * [simplify]: iters left: 2 (27 enodes) 2.997 * * [simplify]: iters left: 1 (28 enodes) 3.001 * * [simplify]: Extracting #0: cost 1 inf + 0 3.001 * * [simplify]: Extracting #1: cost 3 inf + 0 3.001 * * [simplify]: Extracting #2: cost 4 inf + 1 3.001 * * [simplify]: Extracting #3: cost 10 inf + 1 3.001 * * [simplify]: Extracting #4: cost 1 inf + 738 3.002 * * [simplify]: Extracting #5: cost 0 inf + 1302 3.002 * [simplify]: Simplified to (+.p16 a (/.p16 (+.p16 (+.p16 b a) c) (real->posit16 2))) 3.002 * [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.002 * * * * [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.002 * [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.002 * * [simplify]: iters left: 6 (11 enodes) 3.005 * * [simplify]: iters left: 5 (35 enodes) 3.011 * * [simplify]: iters left: 4 (99 enodes) 3.044 * * [simplify]: Extracting #0: cost 1 inf + 0 3.044 * * [simplify]: Extracting #1: cost 30 inf + 0 3.044 * * [simplify]: Extracting #2: cost 119 inf + 0 3.045 * * [simplify]: Extracting #3: cost 164 inf + 5280 3.049 * * [simplify]: Extracting #4: cost 60 inf + 113080 3.059 * * [simplify]: Extracting #5: cost 3 inf + 183806 3.069 * * [simplify]: Extracting #6: cost 0 inf + 189337 3.080 * [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.080 * [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.081 * [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.081 * * [simplify]: iters left: 6 (12 enodes) 3.084 * * [simplify]: iters left: 5 (36 enodes) 3.090 * * [simplify]: iters left: 4 (88 enodes) 3.117 * * [simplify]: iters left: 3 (326 enodes) 3.306 * * [simplify]: Extracting #0: cost 1 inf + 0 3.306 * * [simplify]: Extracting #1: cost 40 inf + 0 3.307 * * [simplify]: Extracting #2: cost 283 inf + 0 3.310 * * [simplify]: Extracting #3: cost 411 inf + 35676 3.323 * * [simplify]: Extracting #4: cost 171 inf + 301659 3.352 * * [simplify]: Extracting #5: cost 71 inf + 492019 3.400 * * [simplify]: Extracting #6: cost 2 inf + 616990 3.438 * * [simplify]: Extracting #7: cost 0 inf + 622758 3.478 * [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)))) 3.478 * [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)))) 3.479 * * * * [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))))> 3.479 * [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))) 3.479 * * [simplify]: iters left: 6 (11 enodes) 3.482 * * [simplify]: iters left: 5 (36 enodes) 3.490 * * [simplify]: iters left: 4 (93 enodes) 3.521 * * [simplify]: iters left: 3 (390 enodes) 3.799 * * [simplify]: Extracting #0: cost 1 inf + 0 3.800 * * [simplify]: Extracting #1: cost 44 inf + 0 3.801 * * [simplify]: Extracting #2: cost 324 inf + 0 3.806 * * [simplify]: Extracting #3: cost 576 inf + 34479 3.841 * * [simplify]: Extracting #4: cost 260 inf + 444609 3.889 * * [simplify]: Extracting #5: cost 4 inf + 812472 3.941 * * [simplify]: Extracting #6: cost 0 inf + 821045 3.992 * [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.992 * [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)))) 3.992 * [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))) 3.992 * * [simplify]: iters left: 6 (12 enodes) 3.996 * * [simplify]: iters left: 5 (36 enodes) 4.005 * * [simplify]: iters left: 4 (94 enodes) 4.036 * * [simplify]: iters left: 3 (374 enodes) 4.254 * * [simplify]: Extracting #0: cost 1 inf + 0 4.254 * * [simplify]: Extracting #1: cost 43 inf + 0 4.256 * * [simplify]: Extracting #2: cost 304 inf + 0 4.260 * * [simplify]: Extracting #3: cost 438 inf + 30239 4.281 * * [simplify]: Extracting #4: cost 124 inf + 416568 4.318 * * [simplify]: Extracting #5: cost 24 inf + 620451 4.356 * * [simplify]: Extracting #6: cost 0 inf + 654867 4.394 * [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))) 4.394 * [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)))) 4.394 * * * * [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))))> 4.394 * [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)) 4.394 * * [simplify]: iters left: 5 (11 enodes) 4.398 * * [simplify]: iters left: 4 (36 enodes) 4.409 * * [simplify]: iters left: 3 (85 enodes) 4.430 * * [simplify]: iters left: 2 (286 enodes) 4.527 * * [simplify]: Extracting #0: cost 1 inf + 0 4.527 * * [simplify]: Extracting #1: cost 64 inf + 0 4.528 * * [simplify]: Extracting #2: cost 296 inf + 0 4.530 * * [simplify]: Extracting #3: cost 414 inf + 1288 4.541 * * [simplify]: Extracting #4: cost 288 inf + 175558 4.575 * * [simplify]: Extracting #5: cost 49 inf + 536188 4.628 * * [simplify]: Extracting #6: cost 0 inf + 628584 4.688 * * [simplify]: Extracting #7: cost 0 inf + 627824 4.753 * [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)) 4.753 * [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)))) 4.753 * * * * [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))))> 4.753 * [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))) 4.754 * * [simplify]: iters left: 6 (14 enodes) 4.757 * * [simplify]: iters left: 5 (51 enodes) 4.767 * * [simplify]: iters left: 4 (171 enodes) 4.824 * * [simplify]: Extracting #0: cost 1 inf + 0 4.824 * * [simplify]: Extracting #1: cost 46 inf + 0 4.825 * * [simplify]: Extracting #2: cost 203 inf + 0 4.827 * * [simplify]: Extracting #3: cost 243 inf + 32533 4.842 * * [simplify]: Extracting #4: cost 117 inf + 241265 4.863 * * [simplify]: Extracting #5: cost 6 inf + 400335 4.888 * * [simplify]: Extracting #6: cost 0 inf + 412799 4.911 * [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))))) 4.911 * [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)))) 4.911 * * * * [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))))> 4.911 * [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)) 4.911 * * [simplify]: iters left: 6 (14 enodes) 4.915 * * [simplify]: iters left: 5 (51 enodes) 4.925 * * [simplify]: iters left: 4 (173 enodes) 4.983 * * [simplify]: Extracting #0: cost 1 inf + 0 4.983 * * [simplify]: Extracting #1: cost 48 inf + 0 4.984 * * [simplify]: Extracting #2: cost 196 inf + 0 4.987 * * [simplify]: Extracting #3: cost 239 inf + 46998 5.009 * * [simplify]: Extracting #4: cost 95 inf + 284642 5.046 * * [simplify]: Extracting #5: cost 4 inf + 421483 5.089 * * [simplify]: Extracting #6: cost 0 inf + 428092 5.122 * [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))) 5.122 * [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)))) 5.122 * * * * [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))))> 5.122 * [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)) 5.123 * * [simplify]: iters left: 6 (12 enodes) 5.129 * * [simplify]: iters left: 5 (40 enodes) 5.139 * * [simplify]: iters left: 4 (117 enodes) 5.190 * * [simplify]: Extracting #0: cost 1 inf + 0 5.190 * * [simplify]: Extracting #1: cost 47 inf + 0 5.190 * * [simplify]: Extracting #2: cost 171 inf + 0 5.191 * * [simplify]: Extracting #3: cost 247 inf + 1577 5.194 * * [simplify]: Extracting #4: cost 187 inf + 58448 5.205 * * [simplify]: Extracting #5: cost 28 inf + 257133 5.221 * * [simplify]: Extracting #6: cost 4 inf + 293508 5.238 * * [simplify]: Extracting #7: cost 0 inf + 302484 5.256 * [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))) 5.257 * [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)))) 5.257 * * * * [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))))> 5.257 * * * * [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))))> 5.257 * [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))) 5.257 * * [simplify]: iters left: 6 (15 enodes) 5.261 * * [simplify]: iters left: 5 (54 enodes) 5.272 * * [simplify]: iters left: 4 (174 enodes) 5.341 * * [simplify]: Extracting #0: cost 1 inf + 0 5.341 * * [simplify]: Extracting #1: cost 2 inf + 0 5.342 * * [simplify]: Extracting #2: cost 52 inf + 0 5.342 * * [simplify]: Extracting #3: cost 218 inf + 0 5.343 * * [simplify]: Extracting #4: cost 350 inf + 488 5.347 * * [simplify]: Extracting #5: cost 271 inf + 83278 5.361 * * [simplify]: Extracting #6: cost 99 inf + 301152 5.387 * * [simplify]: Extracting #7: cost 13 inf + 445414 5.416 * * [simplify]: Extracting #8: cost 0 inf + 471346 5.454 * [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))) 5.454 * [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)))) 5.455 * * * * [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))))> 5.455 * [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))) 5.455 * * [simplify]: iters left: 6 (15 enodes) 5.462 * * [simplify]: iters left: 5 (54 enodes) 5.473 * * [simplify]: iters left: 4 (174 enodes) 5.539 * * [simplify]: Extracting #0: cost 1 inf + 0 5.540 * * [simplify]: Extracting #1: cost 2 inf + 0 5.540 * * [simplify]: Extracting #2: cost 52 inf + 0 5.540 * * [simplify]: Extracting #3: cost 218 inf + 0 5.541 * * [simplify]: Extracting #4: cost 350 inf + 488 5.546 * * [simplify]: Extracting #5: cost 271 inf + 83278 5.563 * * [simplify]: Extracting #6: cost 99 inf + 301152 5.607 * * [simplify]: Extracting #7: cost 13 inf + 445414 5.642 * * [simplify]: Extracting #8: cost 0 inf + 471346 5.676 * [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))) 5.676 * [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)))) 5.676 * * * * [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))))> 5.677 * [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))) 5.677 * * [simplify]: iters left: 6 (15 enodes) 5.683 * * [simplify]: iters left: 5 (54 enodes) 5.695 * * [simplify]: iters left: 4 (174 enodes) 5.764 * * [simplify]: Extracting #0: cost 1 inf + 0 5.764 * * [simplify]: Extracting #1: cost 2 inf + 0 5.764 * * [simplify]: Extracting #2: cost 52 inf + 0 5.765 * * [simplify]: Extracting #3: cost 218 inf + 0 5.766 * * [simplify]: Extracting #4: cost 350 inf + 488 5.771 * * [simplify]: Extracting #5: cost 271 inf + 83278 5.784 * * [simplify]: Extracting #6: cost 99 inf + 301152 5.812 * * [simplify]: Extracting #7: cost 13 inf + 445414 5.856 * * [simplify]: Extracting #8: cost 0 inf + 471346 5.885 * [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))) 5.885 * [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)))) 5.885 * * * * [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))))> 5.885 * [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))) 5.885 * * [simplify]: iters left: 6 (15 enodes) 5.889 * * [simplify]: iters left: 5 (54 enodes) 5.899 * * [simplify]: iters left: 4 (174 enodes) 5.986 * * [simplify]: Extracting #0: cost 1 inf + 0 5.986 * * [simplify]: Extracting #1: cost 2 inf + 0 5.986 * * [simplify]: Extracting #2: cost 52 inf + 0 5.986 * * [simplify]: Extracting #3: cost 218 inf + 0 5.987 * * [simplify]: Extracting #4: cost 350 inf + 488 5.994 * * [simplify]: Extracting #5: cost 271 inf + 83278 6.012 * * [simplify]: Extracting #6: cost 99 inf + 301152 6.039 * * [simplify]: Extracting #7: cost 13 inf + 445414 6.074 * * [simplify]: Extracting #8: cost 0 inf + 471346 6.109 * [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.109 * [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.109 * * * [progress]: adding candidates to table 6.723 * * [progress]: iteration 2 / 4 6.723 * * * [progress]: picking best candidate 6.806 * * * * [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)))))> 6.806 * * * [progress]: localizing error 7.152 * * * [progress]: generating rewritten candidates 7.152 * * * * [progress]: [ 1 / 4 ] rewriting at (2 1 2) 7.235 * * * * [progress]: [ 2 / 4 ] rewriting at (2 1 1 2) 7.260 * * * * [progress]: [ 3 / 4 ] rewriting at (2 1 1 1 2) 7.281 * * * * [progress]: [ 4 / 4 ] rewriting at (2 1 2 1) 7.284 * * * [progress]: generating series expansions 7.284 * * * * [progress]: [ 1 / 4 ] generating series at (2 1 2) 7.284 * * * * [progress]: [ 2 / 4 ] generating series at (2 1 1 2) 7.284 * * * * [progress]: [ 3 / 4 ] generating series at (2 1 1 1 2) 7.284 * * * * [progress]: [ 4 / 4 ] generating series at (2 1 2 1) 7.284 * * * [progress]: simplifying candidates 7.284 * * * * [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))))))> 7.285 * [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)) 7.285 * * [simplify]: iters left: 5 (11 enodes) 7.287 * * [simplify]: iters left: 4 (29 enodes) 7.292 * * [simplify]: iters left: 3 (50 enodes) 7.301 * * [simplify]: iters left: 2 (136 enodes) 7.346 * * [simplify]: Extracting #0: cost 1 inf + 0 7.346 * * [simplify]: Extracting #1: cost 19 inf + 0 7.346 * * [simplify]: Extracting #2: cost 68 inf + 0 7.346 * * [simplify]: Extracting #3: cost 105 inf + 404 7.347 * * [simplify]: Extracting #4: cost 144 inf + 3212 7.348 * * [simplify]: Extracting #5: cost 141 inf + 17509 7.352 * * [simplify]: Extracting #6: cost 62 inf + 102535 7.362 * * [simplify]: Extracting #7: cost 9 inf + 195869 7.373 * * [simplify]: Extracting #8: cost 0 inf + 216465 7.386 * * [simplify]: Extracting #9: cost 0 inf + 216025 7.398 * [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)) 7.398 * [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)))))) 7.398 * * * * [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)))))))> 7.398 * [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))) 7.399 * * [simplify]: iters left: 6 (13 enodes) 7.402 * * [simplify]: iters left: 5 (37 enodes) 7.411 * * [simplify]: iters left: 4 (103 enodes) 7.434 * * [simplify]: iters left: 3 (299 enodes) 7.521 * * [simplify]: Extracting #0: cost 1 inf + 0 7.521 * * [simplify]: Extracting #1: cost 15 inf + 0 7.521 * * [simplify]: Extracting #2: cost 76 inf + 0 7.522 * * [simplify]: Extracting #3: cost 225 inf + 1 7.527 * * [simplify]: Extracting #4: cost 218 inf + 50046 7.538 * * [simplify]: Extracting #5: cost 20 inf + 255793 7.555 * * [simplify]: Extracting #6: cost 0 inf + 279953 7.571 * [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))))) 7.571 * [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))))))))) 7.572 * * * * [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)))))> 7.572 * [simplify]: Simplifying (neg.p16 b) 7.572 * * [simplify]: iters left: 1 (2 enodes) 7.572 * * [simplify]: Extracting #0: cost 1 inf + 0 7.572 * * [simplify]: Extracting #1: cost 2 inf + 0 7.572 * * [simplify]: Extracting #2: cost 1 inf + 1 7.572 * * [simplify]: Extracting #3: cost 0 inf + 82 7.572 * [simplify]: Simplified to (neg.p16 b) 7.572 * [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))))) 7.572 * * * * [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)))))> 7.573 * [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)) 7.573 * * [simplify]: iters left: 5 (11 enodes) 7.575 * * [simplify]: iters left: 4 (36 enodes) 7.582 * * [simplify]: iters left: 3 (93 enodes) 7.602 * * [simplify]: iters left: 2 (310 enodes) 7.746 * * [simplify]: Extracting #0: cost 1 inf + 0 7.746 * * [simplify]: Extracting #1: cost 32 inf + 0 7.747 * * [simplify]: Extracting #2: cost 177 inf + 0 7.748 * * [simplify]: Extracting #3: cost 260 inf + 323 7.749 * * [simplify]: Extracting #4: cost 456 inf + 5597 7.760 * * [simplify]: Extracting #5: cost 278 inf + 236939 7.794 * * [simplify]: Extracting #6: cost 27 inf + 652788 7.840 * * [simplify]: Extracting #7: cost 2 inf + 706688 7.920 * * [simplify]: Extracting #8: cost 0 inf + 713376 8.000 * [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)) 8.000 * [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))))) 8.000 * [simplify]: Simplifying (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) b) 8.000 * * [simplify]: iters left: 4 (9 enodes) 8.002 * * [simplify]: iters left: 3 (21 enodes) 8.007 * * [simplify]: iters left: 2 (27 enodes) 8.011 * * [simplify]: iters left: 1 (28 enodes) 8.014 * * [simplify]: Extracting #0: cost 1 inf + 0 8.015 * * [simplify]: Extracting #1: cost 3 inf + 0 8.015 * * [simplify]: Extracting #2: cost 4 inf + 1 8.015 * * [simplify]: Extracting #3: cost 10 inf + 1 8.015 * * [simplify]: Extracting #4: cost 5 inf + 47 8.015 * * [simplify]: Extracting #5: cost 1 inf + 738 8.015 * * [simplify]: Extracting #6: cost 0 inf + 1302 8.015 * [simplify]: Simplified to (+.p16 (/.p16 (+.p16 a (+.p16 c b)) (real->posit16 2)) b) 8.015 * [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))))) 8.015 * * * * [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)))))> 8.015 * [simplify]: Simplifying (neg.p16 a) 8.016 * * [simplify]: iters left: 1 (2 enodes) 8.016 * * [simplify]: Extracting #0: cost 1 inf + 0 8.016 * * [simplify]: Extracting #1: cost 2 inf + 0 8.016 * * [simplify]: Extracting #2: cost 1 inf + 1 8.016 * * [simplify]: Extracting #3: cost 0 inf + 82 8.016 * [simplify]: Simplified to (neg.p16 a) 8.016 * [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))))) 8.016 * * * * [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)))))> 8.016 * [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)) 8.016 * * [simplify]: iters left: 5 (11 enodes) 8.019 * * [simplify]: iters left: 4 (36 enodes) 8.026 * * [simplify]: iters left: 3 (93 enodes) 8.046 * * [simplify]: iters left: 2 (310 enodes) 8.177 * * [simplify]: Extracting #0: cost 1 inf + 0 8.177 * * [simplify]: Extracting #1: cost 32 inf + 0 8.178 * * [simplify]: Extracting #2: cost 177 inf + 0 8.178 * * [simplify]: Extracting #3: cost 262 inf + 323 8.181 * * [simplify]: Extracting #4: cost 416 inf + 51663 8.206 * * [simplify]: Extracting #5: cost 116 inf + 501475 8.248 * * [simplify]: Extracting #6: cost 0 inf + 713857 8.312 * * [simplify]: Extracting #7: cost 0 inf + 713577 8.360 * [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)) 8.360 * [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))))) 8.361 * [simplify]: Simplifying (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) a) 8.361 * * [simplify]: iters left: 4 (9 enodes) 8.363 * * [simplify]: iters left: 3 (21 enodes) 8.366 * * [simplify]: iters left: 2 (27 enodes) 8.371 * * [simplify]: iters left: 1 (28 enodes) 8.376 * * [simplify]: Extracting #0: cost 1 inf + 0 8.376 * * [simplify]: Extracting #1: cost 3 inf + 0 8.376 * * [simplify]: Extracting #2: cost 4 inf + 1 8.376 * * [simplify]: Extracting #3: cost 10 inf + 1 8.376 * * [simplify]: Extracting #4: cost 1 inf + 738 8.376 * * [simplify]: Extracting #5: cost 0 inf + 1302 8.376 * [simplify]: Simplified to (+.p16 a (/.p16 (+.p16 (+.p16 b a) c) (real->posit16 2))) 8.376 * [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))))) 8.377 * * * * [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)))))> 8.377 * [simplify]: Simplifying (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) c) 8.377 * * [simplify]: iters left: 4 (9 enodes) 8.379 * * [simplify]: iters left: 3 (21 enodes) 8.382 * * [simplify]: iters left: 2 (27 enodes) 8.386 * * [simplify]: iters left: 1 (28 enodes) 8.390 * * [simplify]: Extracting #0: cost 1 inf + 0 8.390 * * [simplify]: Extracting #1: cost 3 inf + 0 8.390 * * [simplify]: Extracting #2: cost 4 inf + 1 8.390 * * [simplify]: Extracting #3: cost 10 inf + 1 8.390 * * [simplify]: Extracting #4: cost 5 inf + 47 8.390 * * [simplify]: Extracting #5: cost 1 inf + 738 8.390 * * [simplify]: Extracting #6: cost 0 inf + 1302 8.391 * [simplify]: Simplified to (+.p16 c (/.p16 (+.p16 a (+.p16 c b)) (real->posit16 2))) 8.391 * [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))))) 8.391 * [simplify]: Simplifying (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) c) 8.391 * * [simplify]: iters left: 4 (9 enodes) 8.393 * * [simplify]: iters left: 3 (27 enodes) 8.398 * * [simplify]: iters left: 2 (47 enodes) 8.407 * * [simplify]: iters left: 1 (123 enodes) 8.466 * * [simplify]: Extracting #0: cost 1 inf + 0 8.466 * * [simplify]: Extracting #1: cost 15 inf + 0 8.466 * * [simplify]: Extracting #2: cost 52 inf + 82 8.467 * * [simplify]: Extracting #3: cost 87 inf + 1044 8.468 * * [simplify]: Extracting #4: cost 138 inf + 5615 8.469 * * [simplify]: Extracting #5: cost 116 inf + 19272 8.476 * * [simplify]: Extracting #6: cost 57 inf + 78898 8.491 * * [simplify]: Extracting #7: cost 8 inf + 156974 8.503 * * [simplify]: Extracting #8: cost 0 inf + 175966 8.514 * [simplify]: Simplified to (-.p16 (/.p16 (+.p16 b (+.p16 a c)) (real->posit16 2)) c) 8.514 * [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))))) 8.514 * * * * [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)))))> 8.514 * [simplify]: Simplifying (neg.p16 (*.p16 c c)) 8.514 * * [simplify]: iters left: 2 (3 enodes) 8.515 * * [simplify]: iters left: 1 (5 enodes) 8.515 * * [simplify]: Extracting #0: cost 1 inf + 0 8.516 * * [simplify]: Extracting #1: cost 2 inf + 0 8.516 * * [simplify]: Extracting #2: cost 3 inf + 0 8.516 * * [simplify]: Extracting #3: cost 2 inf + 1 8.516 * * [simplify]: Extracting #4: cost 0 inf + 723 8.516 * [simplify]: Simplified to (neg.p16 (*.p16 c c)) 8.516 * [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))))) 8.516 * * * * [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)))))> 8.516 * [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))) 8.516 * * [simplify]: iters left: 6 (13 enodes) 8.519 * * [simplify]: iters left: 5 (46 enodes) 8.529 * * [simplify]: iters left: 4 (130 enodes) 8.567 * * [simplify]: Extracting #0: cost 1 inf + 0 8.567 * * [simplify]: Extracting #1: cost 25 inf + 0 8.567 * * [simplify]: Extracting #2: cost 62 inf + 0 8.568 * * [simplify]: Extracting #3: cost 156 inf + 82 8.569 * * [simplify]: Extracting #4: cost 155 inf + 20973 8.579 * * [simplify]: Extracting #5: cost 51 inf + 151607 8.600 * * [simplify]: Extracting #6: cost 3 inf + 236996 8.623 * * [simplify]: Extracting #7: cost 0 inf + 246088 8.640 * [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))) 8.640 * [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))))) 8.641 * [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)) 8.641 * * [simplify]: iters left: 5 (11 enodes) 8.644 * * [simplify]: iters left: 4 (27 enodes) 8.649 * * [simplify]: iters left: 3 (53 enodes) 8.662 * * [simplify]: iters left: 2 (121 enodes) 8.690 * * [simplify]: iters left: 1 (313 enodes) 8.847 * * [simplify]: Extracting #0: cost 1 inf + 0 8.847 * * [simplify]: Extracting #1: cost 21 inf + 0 8.847 * * [simplify]: Extracting #2: cost 48 inf + 0 8.848 * * [simplify]: Extracting #3: cost 201 inf + 324 8.850 * * [simplify]: Extracting #4: cost 143 inf + 47287 8.860 * * [simplify]: Extracting #5: cost 17 inf + 136312 8.870 * * [simplify]: Extracting #6: cost 0 inf + 151168 8.887 * [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)))) 8.887 * [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))))) 8.887 * * * * [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)))))> 8.887 * [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)) 8.888 * * [simplify]: iters left: 5 (11 enodes) 8.893 * * [simplify]: iters left: 4 (36 enodes) 8.907 * * [simplify]: iters left: 3 (93 enodes) 8.945 * * [simplify]: iters left: 2 (310 enodes) 9.148 * * [simplify]: Extracting #0: cost 1 inf + 0 9.148 * * [simplify]: Extracting #1: cost 32 inf + 0 9.148 * * [simplify]: Extracting #2: cost 177 inf + 0 9.149 * * [simplify]: Extracting #3: cost 262 inf + 323 9.155 * * [simplify]: Extracting #4: cost 417 inf + 52622 9.175 * * [simplify]: Extracting #5: cost 157 inf + 465463 9.229 * * [simplify]: Extracting #6: cost 2 inf + 707329 9.282 * * [simplify]: Extracting #7: cost 0 inf + 711417 9.356 * [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)) 9.356 * [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))))) 9.356 * [simplify]: Simplifying (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) c) 9.356 * * [simplify]: iters left: 4 (9 enodes) 9.361 * * [simplify]: iters left: 3 (21 enodes) 9.367 * * [simplify]: iters left: 2 (27 enodes) 9.375 * * [simplify]: iters left: 1 (28 enodes) 9.382 * * [simplify]: Extracting #0: cost 1 inf + 0 9.382 * * [simplify]: Extracting #1: cost 3 inf + 0 9.382 * * [simplify]: Extracting #2: cost 4 inf + 1 9.382 * * [simplify]: Extracting #3: cost 10 inf + 1 9.382 * * [simplify]: Extracting #4: cost 5 inf + 47 9.382 * * [simplify]: Extracting #5: cost 1 inf + 738 9.383 * * [simplify]: Extracting #6: cost 0 inf + 1302 9.383 * [simplify]: Simplified to (+.p16 c (/.p16 (+.p16 a (+.p16 c b)) (real->posit16 2))) 9.383 * [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))))))) 9.383 * * * * [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)))))> 9.384 * [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)) 9.384 * * [simplify]: iters left: 5 (11 enodes) 9.389 * * [simplify]: iters left: 4 (36 enodes) 9.401 * * [simplify]: iters left: 3 (93 enodes) 9.442 * * [simplify]: iters left: 2 (310 enodes) 9.586 * * [simplify]: Extracting #0: cost 1 inf + 0 9.587 * * [simplify]: Extracting #1: cost 32 inf + 0 9.587 * * [simplify]: Extracting #2: cost 177 inf + 0 9.588 * * [simplify]: Extracting #3: cost 262 inf + 323 9.591 * * [simplify]: Extracting #4: cost 417 inf + 52622 9.616 * * [simplify]: Extracting #5: cost 157 inf + 465463 9.664 * * [simplify]: Extracting #6: cost 2 inf + 707329 9.717 * * [simplify]: Extracting #7: cost 0 inf + 711417 9.769 * [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)) 9.769 * [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))))) 9.770 * [simplify]: Simplifying (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) c) 9.770 * * [simplify]: iters left: 4 (9 enodes) 9.772 * * [simplify]: iters left: 3 (21 enodes) 9.775 * * [simplify]: iters left: 2 (27 enodes) 9.779 * * [simplify]: iters left: 1 (28 enodes) 9.783 * * [simplify]: Extracting #0: cost 1 inf + 0 9.783 * * [simplify]: Extracting #1: cost 3 inf + 0 9.783 * * [simplify]: Extracting #2: cost 4 inf + 1 9.783 * * [simplify]: Extracting #3: cost 10 inf + 1 9.783 * * [simplify]: Extracting #4: cost 5 inf + 47 9.783 * * [simplify]: Extracting #5: cost 1 inf + 738 9.783 * * [simplify]: Extracting #6: cost 0 inf + 1302 9.783 * [simplify]: Simplified to (+.p16 c (/.p16 (+.p16 a (+.p16 c b)) (real->posit16 2))) 9.783 * [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))))))) 9.783 * * * * [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)))))> 9.784 * [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)) 9.784 * * [simplify]: iters left: 5 (11 enodes) 9.786 * * [simplify]: iters left: 4 (36 enodes) 9.794 * * [simplify]: iters left: 3 (93 enodes) 9.815 * * [simplify]: iters left: 2 (310 enodes) 10.018 * * [simplify]: Extracting #0: cost 1 inf + 0 10.018 * * [simplify]: Extracting #1: cost 32 inf + 0 10.019 * * [simplify]: Extracting #2: cost 177 inf + 0 10.020 * * [simplify]: Extracting #3: cost 262 inf + 323 10.026 * * [simplify]: Extracting #4: cost 417 inf + 52622 10.060 * * [simplify]: Extracting #5: cost 157 inf + 465463 10.124 * * [simplify]: Extracting #6: cost 2 inf + 707329 10.187 * * [simplify]: Extracting #7: cost 0 inf + 711417 10.246 * [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.246 * [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.246 * [simplify]: Simplifying (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) c) 10.246 * * [simplify]: iters left: 4 (9 enodes) 10.248 * * [simplify]: iters left: 3 (21 enodes) 10.255 * * [simplify]: iters left: 2 (27 enodes) 10.262 * * [simplify]: iters left: 1 (28 enodes) 10.270 * * [simplify]: Extracting #0: cost 1 inf + 0 10.270 * * [simplify]: Extracting #1: cost 3 inf + 0 10.270 * * [simplify]: Extracting #2: cost 4 inf + 1 10.270 * * [simplify]: Extracting #3: cost 10 inf + 1 10.271 * * [simplify]: Extracting #4: cost 5 inf + 47 10.271 * * [simplify]: Extracting #5: cost 1 inf + 738 10.271 * * [simplify]: Extracting #6: cost 0 inf + 1302 10.271 * [simplify]: Simplified to (+.p16 c (/.p16 (+.p16 a (+.p16 c b)) (real->posit16 2))) 10.271 * [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.272 * * * * [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)))))> 10.272 * [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.272 * * [simplify]: iters left: 5 (11 enodes) 10.278 * * [simplify]: iters left: 4 (36 enodes) 10.291 * * [simplify]: iters left: 3 (93 enodes) 10.331 * * [simplify]: iters left: 2 (310 enodes) 10.596 * * [simplify]: Extracting #0: cost 1 inf + 0 10.597 * * [simplify]: Extracting #1: cost 32 inf + 0 10.597 * * [simplify]: Extracting #2: cost 177 inf + 0 10.599 * * [simplify]: Extracting #3: cost 262 inf + 323 10.605 * * [simplify]: Extracting #4: cost 417 inf + 52622 10.649 * * [simplify]: Extracting #5: cost 157 inf + 465463 10.721 * * [simplify]: Extracting #6: cost 2 inf + 707329 10.800 * * [simplify]: Extracting #7: cost 0 inf + 711417 10.882 * [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.882 * [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.883 * [simplify]: Simplifying (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) c) 10.883 * * [simplify]: iters left: 4 (9 enodes) 10.887 * * [simplify]: iters left: 3 (21 enodes) 10.893 * * [simplify]: iters left: 2 (27 enodes) 10.901 * * [simplify]: iters left: 1 (28 enodes) 10.908 * * [simplify]: Extracting #0: cost 1 inf + 0 10.908 * * [simplify]: Extracting #1: cost 3 inf + 0 10.909 * * [simplify]: Extracting #2: cost 4 inf + 1 10.909 * * [simplify]: Extracting #3: cost 10 inf + 1 10.909 * * [simplify]: Extracting #4: cost 5 inf + 47 10.909 * * [simplify]: Extracting #5: cost 1 inf + 738 10.909 * * [simplify]: Extracting #6: cost 0 inf + 1302 10.910 * [simplify]: Simplified to (+.p16 c (/.p16 (+.p16 a (+.p16 c b)) (real->posit16 2))) 10.910 * [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.910 * * * [progress]: adding candidates to table 11.446 * * [progress]: iteration 3 / 4 11.447 * * * [progress]: picking best candidate 11.566 * * * * [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)))))> 11.566 * * * [progress]: localizing error 12.156 * * * [progress]: generating rewritten candidates 12.156 * * * * [progress]: [ 1 / 4 ] rewriting at (2 1 1 2) 12.266 * * * * [progress]: [ 2 / 4 ] rewriting at (2 1 2) 12.382 * * * * [progress]: [ 3 / 4 ] rewriting at (2 1 1 1 2) 12.426 * * * * [progress]: [ 4 / 4 ] rewriting at (2 1 2 1) 12.432 * * * [progress]: generating series expansions 12.432 * * * * [progress]: [ 1 / 4 ] generating series at (2 1 1 2) 12.432 * * * * [progress]: [ 2 / 4 ] generating series at (2 1 2) 12.433 * * * * [progress]: [ 3 / 4 ] generating series at (2 1 1 1 2) 12.433 * * * * [progress]: [ 4 / 4 ] generating series at (2 1 2 1) 12.433 * * * [progress]: simplifying candidates 12.433 * * * * [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)))))> 12.433 * [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)) 12.433 * * [simplify]: iters left: 5 (11 enodes) 12.439 * * [simplify]: iters left: 4 (29 enodes) 12.449 * * [simplify]: iters left: 3 (50 enodes) 12.467 * * [simplify]: iters left: 2 (136 enodes) 12.518 * * [simplify]: Extracting #0: cost 1 inf + 0 12.518 * * [simplify]: Extracting #1: cost 19 inf + 0 12.518 * * [simplify]: Extracting #2: cost 68 inf + 0 12.518 * * [simplify]: Extracting #3: cost 107 inf + 2 12.519 * * [simplify]: Extracting #4: cost 146 inf + 1531 12.520 * * [simplify]: Extracting #5: cost 151 inf + 11530 12.524 * * [simplify]: Extracting #6: cost 63 inf + 103615 12.534 * * [simplify]: Extracting #7: cost 9 inf + 195949 12.546 * * [simplify]: Extracting #8: cost 0 inf + 216545 12.558 * * [simplify]: Extracting #9: cost 0 inf + 216105 12.570 * [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)) 12.570 * [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))))) 12.571 * * * * [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)))))> 12.571 * [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))) 12.571 * * [simplify]: iters left: 6 (13 enodes) 12.574 * * [simplify]: iters left: 5 (37 enodes) 12.586 * * [simplify]: iters left: 4 (103 enodes) 12.635 * * [simplify]: iters left: 3 (299 enodes) 12.796 * * [simplify]: Extracting #0: cost 1 inf + 0 12.796 * * [simplify]: Extracting #1: cost 15 inf + 0 12.796 * * [simplify]: Extracting #2: cost 76 inf + 0 12.797 * * [simplify]: Extracting #3: cost 226 inf + 1 12.799 * * [simplify]: Extracting #4: cost 226 inf + 48319 12.814 * * [simplify]: Extracting #5: cost 17 inf + 267948 12.831 * * [simplify]: Extracting #6: cost 0 inf + 289975 12.848 * [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))))) 12.848 * [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))))) 12.848 * * * * [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))))))> 12.848 * [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)) 12.848 * * [simplify]: iters left: 5 (11 enodes) 12.851 * * [simplify]: iters left: 4 (29 enodes) 12.856 * * [simplify]: iters left: 3 (50 enodes) 12.866 * * [simplify]: iters left: 2 (136 enodes) 12.904 * * [simplify]: Extracting #0: cost 1 inf + 0 12.904 * * [simplify]: Extracting #1: cost 19 inf + 0 12.904 * * [simplify]: Extracting #2: cost 68 inf + 0 12.904 * * [simplify]: Extracting #3: cost 105 inf + 404 12.905 * * [simplify]: Extracting #4: cost 144 inf + 3212 12.906 * * [simplify]: Extracting #5: cost 141 inf + 17509 12.910 * * [simplify]: Extracting #6: cost 62 inf + 102535 12.919 * * [simplify]: Extracting #7: cost 9 inf + 195869 12.931 * * [simplify]: Extracting #8: cost 0 inf + 216465 12.943 * * [simplify]: Extracting #9: cost 0 inf + 216025 12.954 * [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)) 12.954 * [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)))))) 12.955 * * * * [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)))))))> 12.955 * [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))) 12.955 * * [simplify]: iters left: 6 (13 enodes) 12.958 * * [simplify]: iters left: 5 (37 enodes) 12.965 * * [simplify]: iters left: 4 (103 enodes) 13.003 * * [simplify]: iters left: 3 (299 enodes) 13.176 * * [simplify]: Extracting #0: cost 1 inf + 0 13.176 * * [simplify]: Extracting #1: cost 15 inf + 0 13.176 * * [simplify]: Extracting #2: cost 76 inf + 0 13.177 * * [simplify]: Extracting #3: cost 225 inf + 1 13.182 * * [simplify]: Extracting #4: cost 218 inf + 50046 13.204 * * [simplify]: Extracting #5: cost 20 inf + 255793 13.238 * * [simplify]: Extracting #6: cost 0 inf + 279953 13.270 * [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))))) 13.270 * [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))))))))) 13.270 * * * * [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)))))> 13.271 * [simplify]: Simplifying (neg.p16 a) 13.271 * * [simplify]: iters left: 1 (2 enodes) 13.271 * * [simplify]: Extracting #0: cost 1 inf + 0 13.271 * * [simplify]: Extracting #1: cost 2 inf + 0 13.272 * * [simplify]: Extracting #2: cost 1 inf + 1 13.272 * * [simplify]: Extracting #3: cost 0 inf + 82 13.272 * [simplify]: Simplified to (neg.p16 a) 13.272 * [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))))) 13.272 * * * * [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)))))> 13.272 * [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)) 13.272 * * [simplify]: iters left: 5 (11 enodes) 13.278 * * [simplify]: iters left: 4 (36 enodes) 13.291 * * [simplify]: iters left: 3 (93 enodes) 13.333 * * [simplify]: iters left: 2 (310 enodes) 13.489 * * [simplify]: Extracting #0: cost 1 inf + 0 13.489 * * [simplify]: Extracting #1: cost 32 inf + 0 13.490 * * [simplify]: Extracting #2: cost 177 inf + 0 13.491 * * [simplify]: Extracting #3: cost 262 inf + 323 13.494 * * [simplify]: Extracting #4: cost 416 inf + 51663 13.525 * * [simplify]: Extracting #5: cost 116 inf + 501475 13.593 * * [simplify]: Extracting #6: cost 0 inf + 713857 13.649 * * [simplify]: Extracting #7: cost 0 inf + 713577 13.711 * [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)) 13.711 * [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))))) 13.712 * [simplify]: Simplifying (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) a) 13.712 * * [simplify]: iters left: 4 (9 enodes) 13.716 * * [simplify]: iters left: 3 (21 enodes) 13.723 * * [simplify]: iters left: 2 (27 enodes) 13.731 * * [simplify]: iters left: 1 (28 enodes) 13.738 * * [simplify]: Extracting #0: cost 1 inf + 0 13.738 * * [simplify]: Extracting #1: cost 3 inf + 0 13.738 * * [simplify]: Extracting #2: cost 4 inf + 1 13.738 * * [simplify]: Extracting #3: cost 10 inf + 1 13.739 * * [simplify]: Extracting #4: cost 1 inf + 738 13.739 * * [simplify]: Extracting #5: cost 0 inf + 1302 13.739 * [simplify]: Simplified to (+.p16 a (/.p16 (+.p16 (+.p16 b a) c) (real->posit16 2))) 13.739 * [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))))) 13.740 * * * * [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)))))> 13.740 * [simplify]: Simplifying (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) c) 13.740 * * [simplify]: iters left: 4 (9 enodes) 13.744 * * [simplify]: iters left: 3 (21 enodes) 13.750 * * [simplify]: iters left: 2 (27 enodes) 13.758 * * [simplify]: iters left: 1 (28 enodes) 13.765 * * [simplify]: Extracting #0: cost 1 inf + 0 13.765 * * [simplify]: Extracting #1: cost 3 inf + 0 13.765 * * [simplify]: Extracting #2: cost 4 inf + 1 13.766 * * [simplify]: Extracting #3: cost 10 inf + 1 13.766 * * [simplify]: Extracting #4: cost 5 inf + 47 13.766 * * [simplify]: Extracting #5: cost 1 inf + 738 13.766 * * [simplify]: Extracting #6: cost 0 inf + 1302 13.766 * [simplify]: Simplified to (+.p16 c (/.p16 (+.p16 a (+.p16 c b)) (real->posit16 2))) 13.766 * [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))))) 13.767 * [simplify]: Simplifying (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) c) 13.767 * * [simplify]: iters left: 4 (9 enodes) 13.771 * * [simplify]: iters left: 3 (27 enodes) 13.780 * * [simplify]: iters left: 2 (47 enodes) 13.798 * * [simplify]: iters left: 1 (123 enodes) 13.844 * * [simplify]: Extracting #0: cost 1 inf + 0 13.844 * * [simplify]: Extracting #1: cost 15 inf + 0 13.845 * * [simplify]: Extracting #2: cost 52 inf + 82 13.845 * * [simplify]: Extracting #3: cost 87 inf + 1044 13.845 * * [simplify]: Extracting #4: cost 138 inf + 5615 13.846 * * [simplify]: Extracting #5: cost 116 inf + 19272 13.849 * * [simplify]: Extracting #6: cost 57 inf + 78898 13.857 * * [simplify]: Extracting #7: cost 8 inf + 156974 13.866 * * [simplify]: Extracting #8: cost 0 inf + 175966 13.876 * [simplify]: Simplified to (-.p16 (/.p16 (+.p16 b (+.p16 a c)) (real->posit16 2)) c) 13.876 * [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))))) 13.876 * * * * [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)))))> 13.876 * [simplify]: Simplifying (neg.p16 (*.p16 c c)) 13.876 * * [simplify]: iters left: 2 (3 enodes) 13.877 * * [simplify]: iters left: 1 (5 enodes) 13.877 * * [simplify]: Extracting #0: cost 1 inf + 0 13.877 * * [simplify]: Extracting #1: cost 2 inf + 0 13.877 * * [simplify]: Extracting #2: cost 3 inf + 0 13.877 * * [simplify]: Extracting #3: cost 2 inf + 1 13.878 * * [simplify]: Extracting #4: cost 0 inf + 723 13.878 * [simplify]: Simplified to (neg.p16 (*.p16 c c)) 13.878 * [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))))) 13.878 * * * * [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)))))> 13.878 * [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))) 13.878 * * [simplify]: iters left: 6 (13 enodes) 13.883 * * [simplify]: iters left: 5 (46 enodes) 13.892 * * [simplify]: iters left: 4 (130 enodes) 13.926 * * [simplify]: Extracting #0: cost 1 inf + 0 13.927 * * [simplify]: Extracting #1: cost 25 inf + 0 13.927 * * [simplify]: Extracting #2: cost 62 inf + 0 13.927 * * [simplify]: Extracting #3: cost 156 inf + 82 13.928 * * [simplify]: Extracting #4: cost 155 inf + 20973 13.933 * * [simplify]: Extracting #5: cost 51 inf + 151607 13.944 * * [simplify]: Extracting #6: cost 3 inf + 236996 13.958 * * [simplify]: Extracting #7: cost 0 inf + 246088 13.971 * [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))) 13.971 * [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))))) 13.971 * [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)) 13.972 * * [simplify]: iters left: 5 (11 enodes) 13.974 * * [simplify]: iters left: 4 (27 enodes) 13.979 * * [simplify]: iters left: 3 (53 enodes) 13.989 * * [simplify]: iters left: 2 (121 enodes) 14.013 * * [simplify]: iters left: 1 (313 enodes) 14.131 * * [simplify]: Extracting #0: cost 1 inf + 0 14.131 * * [simplify]: Extracting #1: cost 21 inf + 0 14.131 * * [simplify]: Extracting #2: cost 48 inf + 0 14.132 * * [simplify]: Extracting #3: cost 201 inf + 324 14.134 * * [simplify]: Extracting #4: cost 143 inf + 47287 14.142 * * [simplify]: Extracting #5: cost 17 inf + 136312 14.152 * * [simplify]: Extracting #6: cost 0 inf + 151168 14.162 * [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)))) 14.162 * [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))))) 14.163 * * * * [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)))))> 14.163 * [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)) 14.163 * * [simplify]: iters left: 5 (11 enodes) 14.165 * * [simplify]: iters left: 4 (36 enodes) 14.172 * * [simplify]: iters left: 3 (93 enodes) 14.194 * * [simplify]: iters left: 2 (310 enodes) 14.325 * * [simplify]: Extracting #0: cost 1 inf + 0 14.325 * * [simplify]: Extracting #1: cost 32 inf + 0 14.326 * * [simplify]: Extracting #2: cost 177 inf + 0 14.326 * * [simplify]: Extracting #3: cost 260 inf + 323 14.328 * * [simplify]: Extracting #4: cost 456 inf + 5597 14.339 * * [simplify]: Extracting #5: cost 278 inf + 236939 14.374 * * [simplify]: Extracting #6: cost 27 inf + 652788 14.419 * * [simplify]: Extracting #7: cost 2 inf + 706688 14.461 * * [simplify]: Extracting #8: cost 0 inf + 713376 14.504 * [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)) 14.504 * [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))))) 14.504 * [simplify]: Simplifying (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) b) 14.505 * * [simplify]: iters left: 4 (9 enodes) 14.507 * * [simplify]: iters left: 3 (21 enodes) 14.511 * * [simplify]: iters left: 2 (27 enodes) 14.515 * * [simplify]: iters left: 1 (28 enodes) 14.519 * * [simplify]: Extracting #0: cost 1 inf + 0 14.519 * * [simplify]: Extracting #1: cost 3 inf + 0 14.519 * * [simplify]: Extracting #2: cost 4 inf + 1 14.519 * * [simplify]: Extracting #3: cost 10 inf + 1 14.519 * * [simplify]: Extracting #4: cost 5 inf + 47 14.519 * * [simplify]: Extracting #5: cost 1 inf + 738 14.519 * * [simplify]: Extracting #6: cost 0 inf + 1302 14.519 * [simplify]: Simplified to (+.p16 (/.p16 (+.p16 a (+.p16 c b)) (real->posit16 2)) b) 14.519 * [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))))) 14.520 * * * * [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)))))> 14.520 * [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)) 14.520 * * [simplify]: iters left: 5 (11 enodes) 14.523 * * [simplify]: iters left: 4 (36 enodes) 14.530 * * [simplify]: iters left: 3 (93 enodes) 14.558 * * [simplify]: iters left: 2 (310 enodes) 14.814 * * [simplify]: Extracting #0: cost 1 inf + 0 14.814 * * [simplify]: Extracting #1: cost 32 inf + 0 14.815 * * [simplify]: Extracting #2: cost 177 inf + 0 14.816 * * [simplify]: Extracting #3: cost 260 inf + 323 14.820 * * [simplify]: Extracting #4: cost 456 inf + 5597 14.845 * * [simplify]: Extracting #5: cost 278 inf + 236939 14.910 * * [simplify]: Extracting #6: cost 27 inf + 652788 14.990 * * [simplify]: Extracting #7: cost 2 inf + 706688 15.045 * * [simplify]: Extracting #8: cost 0 inf + 713376 15.088 * [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.088 * [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.089 * [simplify]: Simplifying (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) b) 15.089 * * [simplify]: iters left: 4 (9 enodes) 15.091 * * [simplify]: iters left: 3 (21 enodes) 15.094 * * [simplify]: iters left: 2 (27 enodes) 15.098 * * [simplify]: iters left: 1 (28 enodes) 15.102 * * [simplify]: Extracting #0: cost 1 inf + 0 15.102 * * [simplify]: Extracting #1: cost 3 inf + 0 15.102 * * [simplify]: Extracting #2: cost 4 inf + 1 15.102 * * [simplify]: Extracting #3: cost 10 inf + 1 15.102 * * [simplify]: Extracting #4: cost 5 inf + 47 15.102 * * [simplify]: Extracting #5: cost 1 inf + 738 15.102 * * [simplify]: Extracting #6: cost 0 inf + 1302 15.102 * [simplify]: Simplified to (+.p16 (/.p16 (+.p16 a (+.p16 c b)) (real->posit16 2)) b) 15.102 * [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.103 * * * * [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)))))> 15.103 * [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.103 * * [simplify]: iters left: 5 (11 enodes) 15.106 * * [simplify]: iters left: 4 (36 enodes) 15.112 * * [simplify]: iters left: 3 (93 enodes) 15.134 * * [simplify]: iters left: 2 (310 enodes) 15.267 * * [simplify]: Extracting #0: cost 1 inf + 0 15.267 * * [simplify]: Extracting #1: cost 32 inf + 0 15.268 * * [simplify]: Extracting #2: cost 177 inf + 0 15.269 * * [simplify]: Extracting #3: cost 260 inf + 323 15.271 * * [simplify]: Extracting #4: cost 456 inf + 5597 15.282 * * [simplify]: Extracting #5: cost 278 inf + 236939 15.350 * * [simplify]: Extracting #6: cost 27 inf + 652788 15.435 * * [simplify]: Extracting #7: cost 2 inf + 706688 15.518 * * [simplify]: Extracting #8: cost 0 inf + 713376 15.576 * [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.576 * [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.576 * [simplify]: Simplifying (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) b) 15.576 * * [simplify]: iters left: 4 (9 enodes) 15.579 * * [simplify]: iters left: 3 (21 enodes) 15.582 * * [simplify]: iters left: 2 (27 enodes) 15.586 * * [simplify]: iters left: 1 (28 enodes) 15.590 * * [simplify]: Extracting #0: cost 1 inf + 0 15.590 * * [simplify]: Extracting #1: cost 3 inf + 0 15.590 * * [simplify]: Extracting #2: cost 4 inf + 1 15.590 * * [simplify]: Extracting #3: cost 10 inf + 1 15.590 * * [simplify]: Extracting #4: cost 5 inf + 47 15.590 * * [simplify]: Extracting #5: cost 1 inf + 738 15.590 * * [simplify]: Extracting #6: cost 0 inf + 1302 15.590 * [simplify]: Simplified to (+.p16 (/.p16 (+.p16 a (+.p16 c b)) (real->posit16 2)) b) 15.590 * [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.591 * * * * [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)))))> 15.591 * [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.591 * * [simplify]: iters left: 5 (11 enodes) 15.593 * * [simplify]: iters left: 4 (36 enodes) 15.600 * * [simplify]: iters left: 3 (93 enodes) 15.621 * * [simplify]: iters left: 2 (310 enodes) 15.764 * * [simplify]: Extracting #0: cost 1 inf + 0 15.765 * * [simplify]: Extracting #1: cost 32 inf + 0 15.765 * * [simplify]: Extracting #2: cost 177 inf + 0 15.766 * * [simplify]: Extracting #3: cost 260 inf + 323 15.770 * * [simplify]: Extracting #4: cost 456 inf + 5597 15.781 * * [simplify]: Extracting #5: cost 278 inf + 236939 15.815 * * [simplify]: Extracting #6: cost 27 inf + 652788 15.857 * * [simplify]: Extracting #7: cost 2 inf + 706688 15.900 * * [simplify]: Extracting #8: cost 0 inf + 713376 15.943 * [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.943 * [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.943 * [simplify]: Simplifying (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) b) 15.944 * * [simplify]: iters left: 4 (9 enodes) 15.946 * * [simplify]: iters left: 3 (21 enodes) 15.953 * * [simplify]: iters left: 2 (27 enodes) 15.961 * * [simplify]: iters left: 1 (28 enodes) 15.969 * * [simplify]: Extracting #0: cost 1 inf + 0 15.970 * * [simplify]: Extracting #1: cost 3 inf + 0 15.970 * * [simplify]: Extracting #2: cost 4 inf + 1 15.970 * * [simplify]: Extracting #3: cost 10 inf + 1 15.970 * * [simplify]: Extracting #4: cost 5 inf + 47 15.970 * * [simplify]: Extracting #5: cost 1 inf + 738 15.970 * * [simplify]: Extracting #6: cost 0 inf + 1302 15.971 * [simplify]: Simplified to (+.p16 (/.p16 (+.p16 a (+.p16 c b)) (real->posit16 2)) b) 15.971 * [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.971 * * * [progress]: adding candidates to table 16.306 * * [progress]: iteration 4 / 4 16.306 * * * [progress]: picking best candidate 16.383 * * * * [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))))> 16.383 * * * [progress]: localizing error 17.232 * * * [progress]: generating rewritten candidates 17.232 * * * * [progress]: [ 1 / 4 ] rewriting at (2 1 1) 17.311 * * * * [progress]: [ 2 / 4 ] rewriting at (2 1 2) 17.333 * * * * [progress]: [ 3 / 4 ] rewriting at (2 1 1 1 1 2) 17.368 * * * * [progress]: [ 4 / 4 ] rewriting at (2 1 1 1 2) 17.372 * * * [progress]: generating series expansions 17.372 * * * * [progress]: [ 1 / 4 ] generating series at (2 1 1) 17.372 * * * * [progress]: [ 2 / 4 ] generating series at (2 1 2) 17.372 * * * * [progress]: [ 3 / 4 ] generating series at (2 1 1 1 1 2) 17.372 * * * * [progress]: [ 4 / 4 ] generating series at (2 1 1 1 2) 17.372 * * * [progress]: simplifying candidates 17.372 * * * * [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))))> 17.372 * [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))) 17.372 * * [simplify]: iters left: 6 (13 enodes) 17.375 * * [simplify]: iters left: 5 (38 enodes) 17.383 * * [simplify]: iters left: 4 (98 enodes) 17.414 * * [simplify]: iters left: 3 (338 enodes) 17.612 * * [simplify]: Extracting #0: cost 1 inf + 0 17.613 * * [simplify]: Extracting #1: cost 35 inf + 0 17.613 * * [simplify]: Extracting #2: cost 156 inf + 0 17.614 * * [simplify]: Extracting #3: cost 274 inf + 84 17.617 * * [simplify]: Extracting #4: cost 383 inf + 50741 17.653 * * [simplify]: Extracting #5: cost 266 inf + 387303 17.715 * * [simplify]: Extracting #6: cost 7 inf + 795558 17.797 * * [simplify]: Extracting #7: cost 0 inf + 812709 17.861 * [simplify]: Simplified to (/.p16 (real->posit16 1.0) (-.p16 (/.p16 (+.p16 (+.p16 b a) c) (real->posit16 2)) b)) 17.861 * [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)))) 17.862 * * * * [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))))> 17.862 * [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))) 17.862 * * [simplify]: iters left: 6 (13 enodes) 17.865 * * [simplify]: iters left: 5 (37 enodes) 17.873 * * [simplify]: iters left: 4 (103 enodes) 17.895 * * [simplify]: iters left: 3 (299 enodes) 18.038 * * [simplify]: Extracting #0: cost 1 inf + 0 18.038 * * [simplify]: Extracting #1: cost 15 inf + 0 18.038 * * [simplify]: Extracting #2: cost 76 inf + 0 18.040 * * [simplify]: Extracting #3: cost 226 inf + 1 18.044 * * [simplify]: Extracting #4: cost 226 inf + 48319 18.063 * * [simplify]: Extracting #5: cost 17 inf + 267948 18.080 * * [simplify]: Extracting #6: cost 0 inf + 289975 18.098 * [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))))) 18.098 * [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)))) 18.099 * * * * [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))))> 18.099 * [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)) 18.099 * * [simplify]: iters left: 5 (11 enodes) 18.102 * * [simplify]: iters left: 4 (31 enodes) 18.107 * * [simplify]: iters left: 3 (66 enodes) 18.120 * * [simplify]: iters left: 2 (156 enodes) 18.152 * * [simplify]: iters left: 1 (357 enodes) 18.267 * * [simplify]: Extracting #0: cost 1 inf + 0 18.267 * * [simplify]: Extracting #1: cost 17 inf + 0 18.268 * * [simplify]: Extracting #2: cost 57 inf + 0 18.268 * * [simplify]: Extracting #3: cost 159 inf + 2 18.269 * * [simplify]: Extracting #4: cost 163 inf + 6930 18.273 * * [simplify]: Extracting #5: cost 79 inf + 87240 18.284 * * [simplify]: Extracting #6: cost 1 inf + 183630 18.301 * * [simplify]: Extracting #7: cost 0 inf + 184554 18.325 * [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)))) 18.325 * [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)))) 18.325 * * * * [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))))> 18.326 * [simplify]: Simplifying (*.p16 (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) b) (real->posit16 2)) 18.326 * * [simplify]: iters left: 5 (10 enodes) 18.331 * * [simplify]: iters left: 4 (23 enodes) 18.338 * * [simplify]: iters left: 3 (37 enodes) 18.344 * * [simplify]: iters left: 2 (42 enodes) 18.350 * * [simplify]: iters left: 1 (68 enodes) 18.361 * * [simplify]: Extracting #0: cost 1 inf + 0 18.361 * * [simplify]: Extracting #1: cost 5 inf + 0 18.361 * * [simplify]: Extracting #2: cost 12 inf + 0 18.361 * * [simplify]: Extracting #3: cost 19 inf + 325 18.361 * * [simplify]: Extracting #4: cost 15 inf + 769 18.361 * * [simplify]: Extracting #5: cost 2 inf + 4368 18.362 * * [simplify]: Extracting #6: cost 0 inf + 5456 18.362 * [simplify]: Simplified to (+.p16 (*.p16 (real->posit16 1.0) (+.p16 (+.p16 b a) c)) (*.p16 (real->posit16 2) b)) 18.363 * [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)))) 18.363 * * * * [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)))))> 18.363 * [simplify]: Simplifying (neg.p16 c) 18.363 * * [simplify]: iters left: 1 (2 enodes) 18.363 * * [simplify]: Extracting #0: cost 1 inf + 0 18.363 * * [simplify]: Extracting #1: cost 2 inf + 0 18.363 * * [simplify]: Extracting #2: cost 1 inf + 1 18.363 * * [simplify]: Extracting #3: cost 0 inf + 82 18.363 * [simplify]: Simplified to (neg.p16 c) 18.363 * [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))))) 18.364 * * * * [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)))))> 18.364 * [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)) 18.364 * * [simplify]: iters left: 5 (11 enodes) 18.368 * * [simplify]: iters left: 4 (36 enodes) 18.381 * * [simplify]: iters left: 3 (93 enodes) 18.422 * * [simplify]: iters left: 2 (310 enodes) 18.656 * * [simplify]: Extracting #0: cost 1 inf + 0 18.657 * * [simplify]: Extracting #1: cost 32 inf + 0 18.657 * * [simplify]: Extracting #2: cost 177 inf + 0 18.659 * * [simplify]: Extracting #3: cost 262 inf + 323 18.665 * * [simplify]: Extracting #4: cost 417 inf + 52622 18.706 * * [simplify]: Extracting #5: cost 157 inf + 465463 18.774 * * [simplify]: Extracting #6: cost 2 inf + 707329 18.831 * * [simplify]: Extracting #7: cost 0 inf + 711417 18.892 * [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)) 18.893 * [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))))) 18.893 * [simplify]: Simplifying (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) c) 18.893 * * [simplify]: iters left: 4 (9 enodes) 18.895 * * [simplify]: iters left: 3 (21 enodes) 18.899 * * [simplify]: iters left: 2 (27 enodes) 18.903 * * [simplify]: iters left: 1 (28 enodes) 18.908 * * [simplify]: Extracting #0: cost 1 inf + 0 18.908 * * [simplify]: Extracting #1: cost 3 inf + 0 18.908 * * [simplify]: Extracting #2: cost 4 inf + 1 18.909 * * [simplify]: Extracting #3: cost 10 inf + 1 18.909 * * [simplify]: Extracting #4: cost 5 inf + 47 18.909 * * [simplify]: Extracting #5: cost 1 inf + 738 18.909 * * [simplify]: Extracting #6: cost 0 inf + 1302 18.909 * [simplify]: Simplified to (+.p16 c (/.p16 (+.p16 a (+.p16 c b)) (real->posit16 2))) 18.909 * [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))))))) 18.909 * * * * [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))))> 18.909 * [simplify]: Simplifying (neg.p16 a) 18.909 * * [simplify]: iters left: 1 (2 enodes) 18.910 * * [simplify]: Extracting #0: cost 1 inf + 0 18.910 * * [simplify]: Extracting #1: cost 2 inf + 0 18.910 * * [simplify]: Extracting #2: cost 1 inf + 1 18.910 * * [simplify]: Extracting #3: cost 0 inf + 82 18.910 * [simplify]: Simplified to (neg.p16 a) 18.910 * [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)))) 18.910 * * * * [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))))> 18.910 * [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)) 18.910 * * [simplify]: iters left: 5 (11 enodes) 18.913 * * [simplify]: iters left: 4 (36 enodes) 18.927 * * [simplify]: iters left: 3 (93 enodes) 18.957 * * [simplify]: iters left: 2 (310 enodes) 19.154 * * [simplify]: Extracting #0: cost 1 inf + 0 19.154 * * [simplify]: Extracting #1: cost 32 inf + 0 19.155 * * [simplify]: Extracting #2: cost 177 inf + 0 19.157 * * [simplify]: Extracting #3: cost 262 inf + 323 19.163 * * [simplify]: Extracting #4: cost 416 inf + 51663 19.195 * * [simplify]: Extracting #5: cost 116 inf + 501475 19.247 * * [simplify]: Extracting #6: cost 0 inf + 713857 19.319 * * [simplify]: Extracting #7: cost 0 inf + 713577 19.373 * [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)) 19.373 * [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)))) 19.374 * [simplify]: Simplifying (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) a) 19.374 * * [simplify]: iters left: 4 (9 enodes) 19.376 * * [simplify]: iters left: 3 (21 enodes) 19.379 * * [simplify]: iters left: 2 (27 enodes) 19.383 * * [simplify]: iters left: 1 (28 enodes) 19.387 * * [simplify]: Extracting #0: cost 1 inf + 0 19.387 * * [simplify]: Extracting #1: cost 3 inf + 0 19.387 * * [simplify]: Extracting #2: cost 4 inf + 1 19.387 * * [simplify]: Extracting #3: cost 10 inf + 1 19.387 * * [simplify]: Extracting #4: cost 1 inf + 738 19.388 * * [simplify]: Extracting #5: cost 0 inf + 1302 19.388 * [simplify]: Simplified to (+.p16 a (/.p16 (+.p16 (+.p16 b a) c) (real->posit16 2))) 19.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 (+.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)))) 19.388 * * * * [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))))> 19.388 * [simplify]: Simplifying (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) b) 19.388 * * [simplify]: iters left: 4 (9 enodes) 19.390 * * [simplify]: iters left: 3 (21 enodes) 19.394 * * [simplify]: iters left: 2 (27 enodes) 19.401 * * [simplify]: iters left: 1 (28 enodes) 19.409 * * [simplify]: Extracting #0: cost 1 inf + 0 19.409 * * [simplify]: Extracting #1: cost 3 inf + 0 19.409 * * [simplify]: Extracting #2: cost 4 inf + 1 19.409 * * [simplify]: Extracting #3: cost 10 inf + 1 19.409 * * [simplify]: Extracting #4: cost 5 inf + 47 19.410 * * [simplify]: Extracting #5: cost 1 inf + 738 19.410 * * [simplify]: Extracting #6: cost 0 inf + 1302 19.410 * [simplify]: Simplified to (+.p16 (/.p16 (+.p16 a (+.p16 c b)) (real->posit16 2)) b) 19.410 * [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)))) 19.411 * [simplify]: Simplifying (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) b) 19.411 * * [simplify]: iters left: 4 (9 enodes) 19.415 * * [simplify]: iters left: 3 (27 enodes) 19.424 * * [simplify]: iters left: 2 (47 enodes) 19.442 * * [simplify]: iters left: 1 (123 enodes) 19.495 * * [simplify]: Extracting #0: cost 1 inf + 0 19.495 * * [simplify]: Extracting #1: cost 15 inf + 0 19.495 * * [simplify]: Extracting #2: cost 52 inf + 82 19.495 * * [simplify]: Extracting #3: cost 87 inf + 1044 19.496 * * [simplify]: Extracting #4: cost 138 inf + 5615 19.497 * * [simplify]: Extracting #5: cost 116 inf + 19352 19.500 * * [simplify]: Extracting #6: cost 58 inf + 77414 19.508 * * [simplify]: Extracting #7: cost 8 inf + 156974 19.517 * * [simplify]: Extracting #8: cost 0 inf + 175966 19.526 * [simplify]: Simplified to (-.p16 (/.p16 (+.p16 b (+.p16 a c)) (real->posit16 2)) b) 19.526 * [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)))) 19.526 * * * * [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))))> 19.527 * [simplify]: Simplifying (neg.p16 (*.p16 b b)) 19.527 * * [simplify]: iters left: 2 (3 enodes) 19.527 * * [simplify]: iters left: 1 (5 enodes) 19.528 * * [simplify]: Extracting #0: cost 1 inf + 0 19.528 * * [simplify]: Extracting #1: cost 2 inf + 0 19.528 * * [simplify]: Extracting #2: cost 3 inf + 0 19.528 * * [simplify]: Extracting #3: cost 2 inf + 1 19.528 * * [simplify]: Extracting #4: cost 0 inf + 723 19.528 * [simplify]: Simplified to (neg.p16 (*.p16 b b)) 19.528 * [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)))) 19.528 * * * * [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))))> 19.529 * [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))) 19.529 * * [simplify]: iters left: 6 (13 enodes) 19.532 * * [simplify]: iters left: 5 (46 enodes) 19.541 * * [simplify]: iters left: 4 (130 enodes) 19.578 * * [simplify]: Extracting #0: cost 1 inf + 0 19.578 * * [simplify]: Extracting #1: cost 25 inf + 0 19.578 * * [simplify]: Extracting #2: cost 62 inf + 0 19.579 * * [simplify]: Extracting #3: cost 158 inf + 1 19.580 * * [simplify]: Extracting #4: cost 158 inf + 19530 19.586 * * [simplify]: Extracting #5: cost 53 inf + 149926 19.608 * * [simplify]: Extracting #6: cost 3 inf + 237757 19.633 * * [simplify]: Extracting #7: cost 0 inf + 247569 19.658 * [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))) 19.658 * [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)))) 19.659 * [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)) 19.659 * * [simplify]: iters left: 5 (11 enodes) 19.664 * * [simplify]: iters left: 4 (27 enodes) 19.673 * * [simplify]: iters left: 3 (53 enodes) 19.696 * * [simplify]: iters left: 2 (121 enodes) 19.721 * * [simplify]: iters left: 1 (313 enodes) 19.916 * * [simplify]: Extracting #0: cost 1 inf + 0 19.916 * * [simplify]: Extracting #1: cost 21 inf + 0 19.917 * * [simplify]: Extracting #2: cost 48 inf + 0 19.917 * * [simplify]: Extracting #3: cost 201 inf + 324 19.919 * * [simplify]: Extracting #4: cost 146 inf + 44322 19.927 * * [simplify]: Extracting #5: cost 8 inf + 143661 19.942 * * [simplify]: Extracting #6: cost 0 inf + 151168 19.963 * [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)))) 19.963 * [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)))) 19.963 * * * * [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))))> 19.964 * [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))) 19.964 * * [simplify]: iters left: 6 (14 enodes) 19.971 * * [simplify]: iters left: 5 (51 enodes) 19.992 * * [simplify]: iters left: 4 (171 enodes) 20.100 * * [simplify]: Extracting #0: cost 1 inf + 0 20.101 * * [simplify]: Extracting #1: cost 46 inf + 0 20.101 * * [simplify]: Extracting #2: cost 203 inf + 0 20.105 * * [simplify]: Extracting #3: cost 243 inf + 32533 20.128 * * [simplify]: Extracting #4: cost 117 inf + 241265 20.170 * * [simplify]: Extracting #5: cost 6 inf + 400335 20.215 * * [simplify]: Extracting #6: cost 0 inf + 412799 20.263 * [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))))) 20.263 * [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)))) 20.263 * * * * [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))))> 20.264 * [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))) 20.264 * * [simplify]: iters left: 6 (14 enodes) 20.271 * * [simplify]: iters left: 5 (51 enodes) 20.291 * * [simplify]: iters left: 4 (171 enodes) 20.375 * * [simplify]: Extracting #0: cost 1 inf + 0 20.375 * * [simplify]: Extracting #1: cost 46 inf + 0 20.376 * * [simplify]: Extracting #2: cost 203 inf + 0 20.380 * * [simplify]: Extracting #3: cost 243 inf + 32533 20.394 * * [simplify]: Extracting #4: cost 117 inf + 241265 20.425 * * [simplify]: Extracting #5: cost 6 inf + 400335 20.448 * * [simplify]: Extracting #6: cost 0 inf + 412799 20.481 * [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))))) 20.481 * [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)))) 20.481 * * * * [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))))> 20.482 * [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))) 20.482 * * [simplify]: iters left: 6 (14 enodes) 20.485 * * [simplify]: iters left: 5 (51 enodes) 20.496 * * [simplify]: iters left: 4 (171 enodes) 20.560 * * [simplify]: Extracting #0: cost 1 inf + 0 20.560 * * [simplify]: Extracting #1: cost 46 inf + 0 20.561 * * [simplify]: Extracting #2: cost 203 inf + 0 20.563 * * [simplify]: Extracting #3: cost 243 inf + 32533 20.574 * * [simplify]: Extracting #4: cost 117 inf + 241265 20.601 * * [simplify]: Extracting #5: cost 6 inf + 400335 20.627 * * [simplify]: Extracting #6: cost 0 inf + 412799 20.675 * [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))))) 20.675 * [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)))) 20.675 * * * * [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))))> 20.676 * [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))) 20.676 * * [simplify]: iters left: 6 (14 enodes) 20.683 * * [simplify]: iters left: 5 (51 enodes) 20.695 * * [simplify]: iters left: 4 (171 enodes) 20.786 * * [simplify]: Extracting #0: cost 1 inf + 0 20.786 * * [simplify]: Extracting #1: cost 46 inf + 0 20.787 * * [simplify]: Extracting #2: cost 203 inf + 0 20.791 * * [simplify]: Extracting #3: cost 243 inf + 32533 20.813 * * [simplify]: Extracting #4: cost 117 inf + 241265 20.854 * * [simplify]: Extracting #5: cost 6 inf + 400335 20.880 * * [simplify]: Extracting #6: cost 0 inf + 412799 20.907 * [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))))) 20.907 * [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)))) 20.907 * * * [progress]: adding candidates to table 21.492 * [progress]: [Phase 3 of 3] Extracting. 21.492 * * [regime]: Finding splitpoints for: (#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 (+.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 (+.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)) (-.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))))>) 21.503 * * * [regime-changes]: Trying 3 branch expressions: (c b a) 21.504 * * * * [regimes]: Trying to branch on c from (#posit16 2)) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) a)) (*.p16 (+.p16 (/.p16 (+.p16 (+.p16 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 (+.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 (+.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)) (-.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))))>) 21.755 * * * * [regimes]: Trying to branch on b from (#posit16 2)) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) a)) (*.p16 (+.p16 (/.p16 (+.p16 (+.p16 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 (+.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 (+.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)) (-.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))))>) 21.973 * * * * [regimes]: Trying to branch on a from (#posit16 2)) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) a)) (*.p16 (+.p16 (/.p16 (+.p16 (+.p16 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 (+.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 (+.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)) (-.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))))>) 22.139 * * * [regime]: Found split indices: #