0.004 * [progress]: [Phase 1 of 3] Setting up. 0.005 * * * [progress]: [1/2] Preparing points 0.007 * * * * [points]: Sampling 256 additional inputs, on iter 0 have 0 / 256 0.010 * * * * [points]: Computing exacts on every 16 of 256 points to ramp up precision 0.101 * * * * [points]: Setting MPFR precision to 64 0.104 * * * * [points]: Setting MPFR precision to 320 0.106 * * * * [points]: Computing exacts on every 8 of 256 points to ramp up precision 0.108 * * * * [points]: Setting MPFR precision to 64 0.111 * * * * [points]: Setting MPFR precision to 320 0.113 * * * * [points]: Computing exacts on every 4 of 256 points to ramp up precision 0.115 * * * * [points]: Setting MPFR precision to 64 0.119 * * * * [points]: Setting MPFR precision to 320 0.122 * * * * [points]: Computing exacts on every 2 of 256 points to ramp up precision 0.124 * * * * [points]: Setting MPFR precision to 64 0.130 * * * * [points]: Setting MPFR precision to 320 0.136 * * * * [points]: Computing exacts for 256 points 0.139 * * * * [points]: Setting MPFR precision to 64 0.172 * * * * [points]: Setting MPFR precision to 320 0.204 * * * * [points]: Filtering points with unrepresentable outputs 0.206 * * * * [points]: Sampled 256 points with exact outputs 0.207 * * * [progress]: [2/2] Setting up program. 0.240 * [progress]: [Phase 2 of 3] Improving. 0.240 * * * * [progress]: [ 1 / 1 ] simplifiying candidate #posit16 4) (*.p16 a c))))) (*.p16 (real->posit16 2) a)))> 0.241 * [simplify]: Simplifying (/.p16 (-.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c))))) (*.p16 (real->posit16 2) a)) 0.242 * * [simplify]: iters left: 6 (16 enodes) 0.273 * * [simplify]: iters left: 5 (45 enodes) 0.283 * * [simplify]: iters left: 4 (91 enodes) 0.305 * * [simplify]: iters left: 3 (310 enodes) 0.530 * * [simplify]: Extracting #0: cost 1 inf + 0 0.530 * * [simplify]: Extracting #1: cost 31 inf + 0 0.531 * * [simplify]: Extracting #2: cost 123 inf + 1 0.531 * * [simplify]: Extracting #3: cost 204 inf + 405 0.532 * * [simplify]: Extracting #4: cost 266 inf + 7226 0.535 * * [simplify]: Extracting #5: cost 283 inf + 80479 0.550 * * [simplify]: Extracting #6: cost 199 inf + 369645 0.580 * * [simplify]: Extracting #7: cost 13 inf + 704259 0.619 * * [simplify]: Extracting #8: cost 0 inf + 731309 0.668 * [simplify]: Simplified to (/.p16 (-.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4))))) (*.p16 (real->posit16 2) a)) 0.669 * [simplify]: Simplified (2) to (λ (a b c) (/.p16 (-.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4))))) (*.p16 (real->posit16 2) a))) 0.688 * * [progress]: iteration 1 / 4 0.689 * * * [progress]: picking best candidate 0.723 * * * * [pick]: Picked #posit16 4) (*.p16 a c))))) (*.p16 (real->posit16 2) a)))> 0.723 * * * [progress]: localizing error 1.046 * * * [progress]: generating rewritten candidates 1.047 * * * * [progress]: [ 1 / 4 ] rewriting at (2 1) 1.052 * * * * [progress]: [ 2 / 4 ] rewriting at (2) 1.059 * * * * [progress]: [ 3 / 4 ] rewriting at (2 1 2 1 2) 1.067 * * * * [progress]: [ 4 / 4 ] rewriting at (2 1 2) 1.069 * * * [progress]: generating series expansions 1.069 * * * * [progress]: [ 1 / 4 ] generating series at (2 1) 1.070 * * * * [progress]: [ 2 / 4 ] generating series at (2) 1.070 * * * * [progress]: [ 3 / 4 ] generating series at (2 1 2 1 2) 1.070 * * * * [progress]: [ 4 / 4 ] generating series at (2 1 2) 1.070 * * * [progress]: simplifying candidates 1.070 * * * * [progress]: [ 1 / 10 ] simplifiying candidate #posit16 4) (*.p16 a c)))))) (*.p16 (real->posit16 2) a)))> 1.070 * * * * [progress]: [ 2 / 10 ] simplifiying candidate #posit16 4) (*.p16 a c)))) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c)))))) (+.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c)))))) (*.p16 (real->posit16 2) a)))> 1.070 * * * * [progress]: [ 3 / 10 ] simplifiying candidate #posit16 4) (*.p16 a c))))) (real->posit16 2)) a))> 1.070 * * * * [progress]: [ 4 / 10 ] simplifiying candidate #posit16 4) (*.p16 a c)))) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c)))))) (*.p16 (*.p16 (real->posit16 2) a) (+.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c))))))))> 1.071 * [simplify]: Simplifying (-.p16 (*.p16 (neg.p16 b) (neg.p16 b)) (*.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c)))) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c)))))) 1.071 * * [simplify]: iters left: 6 (14 enodes) 1.077 * * [simplify]: iters left: 5 (42 enodes) 1.094 * * [simplify]: iters left: 4 (117 enodes) 1.154 * * [simplify]: iters left: 3 (426 enodes) 1.471 * * [simplify]: Extracting #0: cost 1 inf + 0 1.471 * * [simplify]: Extracting #1: cost 51 inf + 0 1.472 * * [simplify]: Extracting #2: cost 242 inf + 0 1.474 * * [simplify]: Extracting #3: cost 410 inf + 5216 1.491 * * [simplify]: Extracting #4: cost 403 inf + 280282 1.545 * * [simplify]: Extracting #5: cost 149 inf + 977818 1.619 * * [simplify]: Extracting #6: cost 1 inf + 1265775 1.690 * * [simplify]: Extracting #7: cost 0 inf + 1268699 1.762 * [simplify]: Simplified to (+.p16 (*.p16 (+.p16 (neg.p16 b) b) (+.p16 (neg.p16 b) (neg.p16 b))) (*.p16 (real->posit16 4) (*.p16 a c))) 1.762 * [simplify]: Simplified (2 1) to (λ (a b c) (/.p16 (+.p16 (*.p16 (+.p16 (neg.p16 b) b) (+.p16 (neg.p16 b) (neg.p16 b))) (*.p16 (real->posit16 4) (*.p16 a c))) (*.p16 (*.p16 (real->posit16 2) a) (+.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c)))))))) 1.762 * * * * [progress]: [ 5 / 10 ] simplifiying candidate #posit16 4) a) c)))) (*.p16 (real->posit16 2) a)))> 1.762 * * * * [progress]: [ 6 / 10 ] simplifiying candidate #posit16 4))))) (*.p16 (real->posit16 2) a)))> 1.763 * * * * [progress]: [ 7 / 10 ] simplifiying candidate #posit16 4) (*.p16 a c))))) (*.p16 (real->posit16 2) a)))> 1.763 * [simplify]: Simplifying (/.p16 (-.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c))))) (*.p16 (real->posit16 2) a)) 1.763 * * [simplify]: iters left: 6 (16 enodes) 1.769 * * [simplify]: iters left: 5 (45 enodes) 1.777 * * [simplify]: iters left: 4 (91 enodes) 1.798 * * [simplify]: iters left: 3 (310 enodes) 1.974 * * [simplify]: Extracting #0: cost 1 inf + 0 1.974 * * [simplify]: Extracting #1: cost 31 inf + 0 1.975 * * [simplify]: Extracting #2: cost 123 inf + 1 1.976 * * [simplify]: Extracting #3: cost 204 inf + 405 1.978 * * [simplify]: Extracting #4: cost 266 inf + 7226 1.984 * * [simplify]: Extracting #5: cost 283 inf + 80479 2.017 * * [simplify]: Extracting #6: cost 199 inf + 369645 2.072 * * [simplify]: Extracting #7: cost 13 inf + 704259 2.130 * * [simplify]: Extracting #8: cost 0 inf + 731309 2.170 * [simplify]: Simplified to (/.p16 (-.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4))))) (*.p16 (real->posit16 2) a)) 2.170 * [simplify]: Simplified (2) to (λ (a b c) (/.p16 (-.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4))))) (*.p16 (real->posit16 2) a))) 2.170 * * * * [progress]: [ 8 / 10 ] simplifiying candidate #posit16 4) (*.p16 a c))))) (*.p16 (real->posit16 2) a)))> 2.171 * [simplify]: Simplifying (/.p16 (-.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c))))) (*.p16 (real->posit16 2) a)) 2.171 * * [simplify]: iters left: 6 (16 enodes) 2.179 * * [simplify]: iters left: 5 (45 enodes) 2.195 * * [simplify]: iters left: 4 (91 enodes) 2.233 * * [simplify]: iters left: 3 (310 enodes) 2.888 * * [simplify]: Extracting #0: cost 1 inf + 0 2.888 * * [simplify]: Extracting #1: cost 31 inf + 0 2.889 * * [simplify]: Extracting #2: cost 123 inf + 1 2.890 * * [simplify]: Extracting #3: cost 204 inf + 405 2.891 * * [simplify]: Extracting #4: cost 266 inf + 7226 2.894 * * [simplify]: Extracting #5: cost 283 inf + 80479 2.908 * * [simplify]: Extracting #6: cost 199 inf + 369645 2.942 * * [simplify]: Extracting #7: cost 13 inf + 704259 2.990 * * [simplify]: Extracting #8: cost 0 inf + 731309 3.024 * [simplify]: Simplified to (/.p16 (-.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4))))) (*.p16 (real->posit16 2) a)) 3.024 * [simplify]: Simplified (2) to (λ (a b c) (/.p16 (-.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4))))) (*.p16 (real->posit16 2) a))) 3.024 * * * * [progress]: [ 9 / 10 ] simplifiying candidate #posit16 4) (*.p16 a c))))) (*.p16 (real->posit16 2) a)))> 3.024 * [simplify]: Simplifying (/.p16 (-.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c))))) (*.p16 (real->posit16 2) a)) 3.025 * * [simplify]: iters left: 6 (16 enodes) 3.033 * * [simplify]: iters left: 5 (45 enodes) 3.042 * * [simplify]: iters left: 4 (91 enodes) 3.061 * * [simplify]: iters left: 3 (310 enodes) 3.169 * * [simplify]: Extracting #0: cost 1 inf + 0 3.169 * * [simplify]: Extracting #1: cost 31 inf + 0 3.170 * * [simplify]: Extracting #2: cost 123 inf + 1 3.171 * * [simplify]: Extracting #3: cost 204 inf + 405 3.173 * * [simplify]: Extracting #4: cost 266 inf + 7226 3.179 * * [simplify]: Extracting #5: cost 283 inf + 80479 3.202 * * [simplify]: Extracting #6: cost 199 inf + 369645 3.233 * * [simplify]: Extracting #7: cost 13 inf + 704259 3.265 * * [simplify]: Extracting #8: cost 0 inf + 731309 3.306 * [simplify]: Simplified to (/.p16 (-.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4))))) (*.p16 (real->posit16 2) a)) 3.306 * [simplify]: Simplified (2) to (λ (a b c) (/.p16 (-.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4))))) (*.p16 (real->posit16 2) a))) 3.306 * * * * [progress]: [ 10 / 10 ] simplifiying candidate #posit16 4) (*.p16 a c))))) (*.p16 (real->posit16 2) a)))> 3.306 * [simplify]: Simplifying (/.p16 (-.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c))))) (*.p16 (real->posit16 2) a)) 3.306 * * [simplify]: iters left: 6 (16 enodes) 3.310 * * [simplify]: iters left: 5 (45 enodes) 3.320 * * [simplify]: iters left: 4 (91 enodes) 3.345 * * [simplify]: iters left: 3 (310 enodes) 3.548 * * [simplify]: Extracting #0: cost 1 inf + 0 3.548 * * [simplify]: Extracting #1: cost 31 inf + 0 3.549 * * [simplify]: Extracting #2: cost 123 inf + 1 3.550 * * [simplify]: Extracting #3: cost 204 inf + 405 3.552 * * [simplify]: Extracting #4: cost 266 inf + 7226 3.558 * * [simplify]: Extracting #5: cost 283 inf + 80479 3.585 * * [simplify]: Extracting #6: cost 199 inf + 369645 3.640 * * [simplify]: Extracting #7: cost 13 inf + 704259 3.699 * * [simplify]: Extracting #8: cost 0 inf + 731309 3.733 * [simplify]: Simplified to (/.p16 (-.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4))))) (*.p16 (real->posit16 2) a)) 3.733 * [simplify]: Simplified (2) to (λ (a b c) (/.p16 (-.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4))))) (*.p16 (real->posit16 2) a))) 3.733 * * * [progress]: adding candidates to table 4.188 * * [progress]: iteration 2 / 4 4.188 * * * [progress]: picking best candidate 4.262 * * * * [pick]: Picked #posit16 4) (*.p16 a c))) (*.p16 (*.p16 (real->posit16 2) a) (+.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c))))))))> 4.262 * * * [progress]: localizing error 4.548 * * * [progress]: generating rewritten candidates 4.548 * * * * [progress]: [ 1 / 4 ] rewriting at (2 2 2) 4.551 * * * * [progress]: [ 2 / 4 ] rewriting at (2) 4.554 * * * * [progress]: [ 3 / 4 ] rewriting at (2 2 2 2 1 2) 4.558 * * * * [progress]: [ 4 / 4 ] rewriting at (2 1 2) 4.569 * * * [progress]: generating series expansions 4.569 * * * * [progress]: [ 1 / 4 ] generating series at (2 2 2) 4.569 * * * * [progress]: [ 2 / 4 ] generating series at (2) 4.569 * * * * [progress]: [ 3 / 4 ] generating series at (2 2 2 2 1 2) 4.569 * * * * [progress]: [ 4 / 4 ] generating series at (2 1 2) 4.569 * * * [progress]: simplifying candidates 4.569 * * * * [progress]: [ 1 / 10 ] simplifiying candidate #posit16 4) (*.p16 a c))) (*.p16 (*.p16 (real->posit16 2) a) (+.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c)))) (neg.p16 b)))))> 4.569 * * * * [progress]: [ 2 / 10 ] simplifiying candidate #posit16 4) (*.p16 a c))) (*.p16 (real->posit16 2) a)) (+.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c)))))))> 4.570 * [simplify]: Simplifying (+.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c))))) 4.570 * * [simplify]: iters left: 5 (12 enodes) 4.574 * * [simplify]: iters left: 4 (31 enodes) 4.579 * * [simplify]: iters left: 3 (64 enodes) 4.593 * * [simplify]: iters left: 2 (183 enodes) 4.668 * * [simplify]: Extracting #0: cost 1 inf + 0 4.668 * * [simplify]: Extracting #1: cost 6 inf + 0 4.668 * * [simplify]: Extracting #2: cost 10 inf + 1 4.668 * * [simplify]: Extracting #3: cost 22 inf + 804 4.669 * * [simplify]: Extracting #4: cost 64 inf + 1445 4.669 * * [simplify]: Extracting #5: cost 140 inf + 3371 4.670 * * [simplify]: Extracting #6: cost 220 inf + 13396 4.674 * * [simplify]: Extracting #7: cost 134 inf + 134080 4.687 * * [simplify]: Extracting #8: cost 16 inf + 340223 4.704 * * [simplify]: Extracting #9: cost 0 inf + 376165 4.733 * [simplify]: Simplified to (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b) 4.733 * [simplify]: Simplified (2 2) to (λ (a b c) (/.p16 (/.p16 (+.p16 (*.p16 (+.p16 (neg.p16 b) b) (+.p16 (neg.p16 b) (neg.p16 b))) (*.p16 (real->posit16 4) (*.p16 a c))) (*.p16 (real->posit16 2) a)) (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b))) 4.733 * * * * [progress]: [ 3 / 10 ] simplifiying candidate #posit16 4) (*.p16 a c))) (*.p16 (*.p16 (real->posit16 2) a) (+.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 (real->posit16 4) a) c)))))))> 4.734 * * * * [progress]: [ 4 / 10 ] simplifiying candidate #posit16 4) (*.p16 a c))) (*.p16 (*.p16 (real->posit16 2) a) (+.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 a c) (real->posit16 4))))))))> 4.734 * * * * [progress]: [ 5 / 10 ] simplifiying candidate #posit16 4) a) c)) (*.p16 (*.p16 (real->posit16 2) a) (+.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c))))))))> 4.734 * * * * [progress]: [ 6 / 10 ] simplifiying candidate #posit16 4))) (*.p16 (*.p16 (real->posit16 2) a) (+.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c))))))))> 4.734 * * * * [progress]: [ 7 / 10 ] simplifiying candidate #posit16 4) (*.p16 a c))) (*.p16 (*.p16 (real->posit16 2) a) (+.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c))))))))> 4.734 * [simplify]: Simplifying (/.p16 (+.p16 (*.p16 (+.p16 (neg.p16 b) b) (+.p16 (neg.p16 b) (neg.p16 b))) (*.p16 (real->posit16 4) (*.p16 a c))) (*.p16 (*.p16 (real->posit16 2) a) (+.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c))))))) 4.734 * * [simplify]: iters left: 6 (21 enodes) 4.748 * * [simplify]: iters left: 5 (61 enodes) 4.772 * * [simplify]: iters left: 4 (154 enodes) 4.838 * * [simplify]: iters left: 3 (373 enodes) 5.112 * * [simplify]: Extracting #0: cost 1 inf + 0 5.112 * * [simplify]: Extracting #1: cost 7 inf + 0 5.112 * * [simplify]: Extracting #2: cost 59 inf + 0 5.113 * * [simplify]: Extracting #3: cost 119 inf + 83 5.115 * * [simplify]: Extracting #4: cost 138 inf + 10191 5.118 * * [simplify]: Extracting #5: cost 197 inf + 27270 5.126 * * [simplify]: Extracting #6: cost 245 inf + 77508 5.151 * * [simplify]: Extracting #7: cost 63 inf + 363789 5.188 * * [simplify]: Extracting #8: cost 1 inf + 486187 5.226 * * [simplify]: Extracting #9: cost 0 inf + 486671 5.245 * [simplify]: Simplified to (/.p16 (+.p16 (*.p16 (real->posit16 4) (*.p16 c a)) (real->posit16 0.0)) (*.p16 (real->posit16 2) (*.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 c a)))) b) a))) 5.246 * [simplify]: Simplified (2) to (λ (a b c) (/.p16 (+.p16 (*.p16 (real->posit16 4) (*.p16 c a)) (real->posit16 0.0)) (*.p16 (real->posit16 2) (*.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 c a)))) b) a)))) 5.246 * * * * [progress]: [ 8 / 10 ] simplifiying candidate #posit16 4) (*.p16 a c))) (*.p16 (*.p16 (real->posit16 2) a) (+.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c))))))))> 5.246 * [simplify]: Simplifying (/.p16 (+.p16 (*.p16 (+.p16 (neg.p16 b) b) (+.p16 (neg.p16 b) (neg.p16 b))) (*.p16 (real->posit16 4) (*.p16 a c))) (*.p16 (*.p16 (real->posit16 2) a) (+.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c))))))) 5.246 * * [simplify]: iters left: 6 (21 enodes) 5.256 * * [simplify]: iters left: 5 (61 enodes) 5.281 * * [simplify]: iters left: 4 (154 enodes) 5.348 * * [simplify]: iters left: 3 (373 enodes) 5.621 * * [simplify]: Extracting #0: cost 1 inf + 0 5.621 * * [simplify]: Extracting #1: cost 7 inf + 0 5.621 * * [simplify]: Extracting #2: cost 59 inf + 0 5.622 * * [simplify]: Extracting #3: cost 119 inf + 83 5.624 * * [simplify]: Extracting #4: cost 138 inf + 10191 5.627 * * [simplify]: Extracting #5: cost 197 inf + 27270 5.635 * * [simplify]: Extracting #6: cost 245 inf + 77508 5.653 * * [simplify]: Extracting #7: cost 63 inf + 363789 5.674 * * [simplify]: Extracting #8: cost 1 inf + 486187 5.700 * * [simplify]: Extracting #9: cost 0 inf + 486671 5.726 * [simplify]: Simplified to (/.p16 (+.p16 (*.p16 (real->posit16 4) (*.p16 c a)) (real->posit16 0.0)) (*.p16 (real->posit16 2) (*.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 c a)))) b) a))) 5.726 * [simplify]: Simplified (2) to (λ (a b c) (/.p16 (+.p16 (*.p16 (real->posit16 4) (*.p16 c a)) (real->posit16 0.0)) (*.p16 (real->posit16 2) (*.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 c a)))) b) a)))) 5.727 * * * * [progress]: [ 9 / 10 ] simplifiying candidate #posit16 4) (*.p16 a c))) (*.p16 (*.p16 (real->posit16 2) a) (+.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c))))))))> 5.727 * [simplify]: Simplifying (/.p16 (+.p16 (*.p16 (+.p16 (neg.p16 b) b) (+.p16 (neg.p16 b) (neg.p16 b))) (*.p16 (real->posit16 4) (*.p16 a c))) (*.p16 (*.p16 (real->posit16 2) a) (+.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c))))))) 5.727 * * [simplify]: iters left: 6 (21 enodes) 5.737 * * [simplify]: iters left: 5 (61 enodes) 5.761 * * [simplify]: iters left: 4 (154 enodes) 5.826 * * [simplify]: iters left: 3 (373 enodes) 5.998 * * [simplify]: Extracting #0: cost 1 inf + 0 5.998 * * [simplify]: Extracting #1: cost 7 inf + 0 5.998 * * [simplify]: Extracting #2: cost 59 inf + 0 5.999 * * [simplify]: Extracting #3: cost 119 inf + 83 5.999 * * [simplify]: Extracting #4: cost 138 inf + 10191 6.001 * * [simplify]: Extracting #5: cost 197 inf + 27270 6.005 * * [simplify]: Extracting #6: cost 245 inf + 77508 6.018 * * [simplify]: Extracting #7: cost 63 inf + 363789 6.037 * * [simplify]: Extracting #8: cost 1 inf + 486187 6.061 * * [simplify]: Extracting #9: cost 0 inf + 486671 6.088 * [simplify]: Simplified to (/.p16 (+.p16 (*.p16 (real->posit16 4) (*.p16 c a)) (real->posit16 0.0)) (*.p16 (real->posit16 2) (*.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 c a)))) b) a))) 6.088 * [simplify]: Simplified (2) to (λ (a b c) (/.p16 (+.p16 (*.p16 (real->posit16 4) (*.p16 c a)) (real->posit16 0.0)) (*.p16 (real->posit16 2) (*.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 c a)))) b) a)))) 6.088 * * * * [progress]: [ 10 / 10 ] simplifiying candidate #posit16 4) (*.p16 a c))) (*.p16 (*.p16 (real->posit16 2) a) (+.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c))))))))> 6.088 * [simplify]: Simplifying (/.p16 (+.p16 (*.p16 (+.p16 (neg.p16 b) b) (+.p16 (neg.p16 b) (neg.p16 b))) (*.p16 (real->posit16 4) (*.p16 a c))) (*.p16 (*.p16 (real->posit16 2) a) (+.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c))))))) 6.089 * * [simplify]: iters left: 6 (21 enodes) 6.094 * * [simplify]: iters left: 5 (61 enodes) 6.107 * * [simplify]: iters left: 4 (154 enodes) 6.139 * * [simplify]: iters left: 3 (373 enodes) 6.343 * * [simplify]: Extracting #0: cost 1 inf + 0 6.343 * * [simplify]: Extracting #1: cost 7 inf + 0 6.343 * * [simplify]: Extracting #2: cost 59 inf + 0 6.344 * * [simplify]: Extracting #3: cost 119 inf + 83 6.344 * * [simplify]: Extracting #4: cost 138 inf + 10191 6.346 * * [simplify]: Extracting #5: cost 197 inf + 27270 6.350 * * [simplify]: Extracting #6: cost 245 inf + 77508 6.372 * * [simplify]: Extracting #7: cost 63 inf + 363789 6.408 * * [simplify]: Extracting #8: cost 1 inf + 486187 6.428 * * [simplify]: Extracting #9: cost 0 inf + 486671 6.456 * [simplify]: Simplified to (/.p16 (+.p16 (*.p16 (real->posit16 4) (*.p16 c a)) (real->posit16 0.0)) (*.p16 (real->posit16 2) (*.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 c a)))) b) a))) 6.456 * [simplify]: Simplified (2) to (λ (a b c) (/.p16 (+.p16 (*.p16 (real->posit16 4) (*.p16 c a)) (real->posit16 0.0)) (*.p16 (real->posit16 2) (*.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 c a)))) b) a)))) 6.457 * * * [progress]: adding candidates to table 6.972 * * [progress]: iteration 3 / 4 6.972 * * * [progress]: picking best candidate 7.101 * * * * [pick]: Picked #posit16 4) (*.p16 a c))) (*.p16 (real->posit16 2) a)) (+.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c)))))))> 7.101 * * * [progress]: localizing error 7.409 * * * [progress]: generating rewritten candidates 7.409 * * * * [progress]: [ 1 / 4 ] rewriting at (2 2) 7.414 * * * * [progress]: [ 2 / 4 ] rewriting at (2 1) 7.419 * * * * [progress]: [ 3 / 4 ] rewriting at (2 2 2 1 2) 7.426 * * * * [progress]: [ 4 / 4 ] rewriting at (2 1 1 2) 7.433 * * * [progress]: generating series expansions 7.433 * * * * [progress]: [ 1 / 4 ] generating series at (2 2) 7.434 * * * * [progress]: [ 2 / 4 ] generating series at (2 1) 7.434 * * * * [progress]: [ 3 / 4 ] generating series at (2 2 2 1 2) 7.434 * * * * [progress]: [ 4 / 4 ] generating series at (2 1 1 2) 7.434 * * * [progress]: simplifying candidates 7.434 * * * * [progress]: [ 1 / 10 ] simplifiying candidate #posit16 4) (*.p16 a c))) (*.p16 (real->posit16 2) a)) (+.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c)))) (neg.p16 b))))> 7.434 * * * * [progress]: [ 2 / 10 ] simplifiying candidate #posit16 4) (*.p16 a c))) (real->posit16 2)) a) (+.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c)))))))> 7.434 * * * * [progress]: [ 3 / 10 ] simplifiying candidate #posit16 4) (*.p16 a c))) (*.p16 (real->posit16 2) a)) (+.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 (real->posit16 4) a) c))))))> 7.434 * * * * [progress]: [ 4 / 10 ] simplifiying candidate #posit16 4) (*.p16 a c))) (*.p16 (real->posit16 2) a)) (+.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 a c) (real->posit16 4)))))))> 7.434 * * * * [progress]: [ 5 / 10 ] simplifiying candidate #posit16 4) a) c)) (*.p16 (real->posit16 2) a)) (+.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c)))))))> 7.434 * * * * [progress]: [ 6 / 10 ] simplifiying candidate #posit16 4))) (*.p16 (real->posit16 2) a)) (+.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c)))))))> 7.434 * * * * [progress]: [ 7 / 10 ] simplifiying candidate #posit16 4) (*.p16 a c))) (*.p16 (real->posit16 2) a)) (+.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c)))))))> 7.434 * [simplify]: Simplifying (+.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c))))) 7.434 * * [simplify]: iters left: 5 (12 enodes) 7.437 * * [simplify]: iters left: 4 (31 enodes) 7.442 * * [simplify]: iters left: 3 (64 enodes) 7.455 * * [simplify]: iters left: 2 (183 enodes) 7.533 * * [simplify]: Extracting #0: cost 1 inf + 0 7.534 * * [simplify]: Extracting #1: cost 6 inf + 0 7.534 * * [simplify]: Extracting #2: cost 10 inf + 1 7.534 * * [simplify]: Extracting #3: cost 22 inf + 804 7.534 * * [simplify]: Extracting #4: cost 64 inf + 1445 7.535 * * [simplify]: Extracting #5: cost 140 inf + 3371 7.537 * * [simplify]: Extracting #6: cost 220 inf + 13396 7.546 * * [simplify]: Extracting #7: cost 134 inf + 134080 7.572 * * [simplify]: Extracting #8: cost 16 inf + 340223 7.589 * * [simplify]: Extracting #9: cost 0 inf + 376165 7.603 * [simplify]: Simplified to (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b) 7.603 * [simplify]: Simplified (2 2) to (λ (a b c) (/.p16 (/.p16 (+.p16 (*.p16 (+.p16 (neg.p16 b) b) (+.p16 (neg.p16 b) (neg.p16 b))) (*.p16 (real->posit16 4) (*.p16 a c))) (*.p16 (real->posit16 2) a)) (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b))) 7.603 * * * * [progress]: [ 8 / 10 ] simplifiying candidate #posit16 4) (*.p16 a c))) (*.p16 (real->posit16 2) a)) (+.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c)))))))> 7.603 * [simplify]: Simplifying (+.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c))))) 7.603 * * [simplify]: iters left: 5 (12 enodes) 7.606 * * [simplify]: iters left: 4 (31 enodes) 7.612 * * [simplify]: iters left: 3 (64 enodes) 7.626 * * [simplify]: iters left: 2 (183 enodes) 7.687 * * [simplify]: Extracting #0: cost 1 inf + 0 7.687 * * [simplify]: Extracting #1: cost 6 inf + 0 7.687 * * [simplify]: Extracting #2: cost 10 inf + 1 7.687 * * [simplify]: Extracting #3: cost 22 inf + 804 7.688 * * [simplify]: Extracting #4: cost 64 inf + 1445 7.688 * * [simplify]: Extracting #5: cost 140 inf + 3371 7.689 * * [simplify]: Extracting #6: cost 220 inf + 13396 7.694 * * [simplify]: Extracting #7: cost 134 inf + 134080 7.707 * * [simplify]: Extracting #8: cost 16 inf + 340223 7.721 * * [simplify]: Extracting #9: cost 0 inf + 376165 7.736 * [simplify]: Simplified to (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b) 7.736 * [simplify]: Simplified (2 2) to (λ (a b c) (/.p16 (/.p16 (+.p16 (*.p16 (+.p16 (neg.p16 b) b) (+.p16 (neg.p16 b) (neg.p16 b))) (*.p16 (real->posit16 4) (*.p16 a c))) (*.p16 (real->posit16 2) a)) (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b))) 7.736 * * * * [progress]: [ 9 / 10 ] simplifiying candidate #posit16 4) (*.p16 a c))) (*.p16 (real->posit16 2) a)) (+.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c)))))))> 7.736 * [simplify]: Simplifying (+.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c))))) 7.736 * * [simplify]: iters left: 5 (12 enodes) 7.739 * * [simplify]: iters left: 4 (31 enodes) 7.744 * * [simplify]: iters left: 3 (64 enodes) 7.770 * * [simplify]: iters left: 2 (183 enodes) 7.895 * * [simplify]: Extracting #0: cost 1 inf + 0 7.895 * * [simplify]: Extracting #1: cost 6 inf + 0 7.895 * * [simplify]: Extracting #2: cost 10 inf + 1 7.895 * * [simplify]: Extracting #3: cost 22 inf + 804 7.895 * * [simplify]: Extracting #4: cost 64 inf + 1445 7.896 * * [simplify]: Extracting #5: cost 140 inf + 3371 7.898 * * [simplify]: Extracting #6: cost 220 inf + 13396 7.907 * * [simplify]: Extracting #7: cost 134 inf + 134080 7.931 * * [simplify]: Extracting #8: cost 16 inf + 340223 7.961 * * [simplify]: Extracting #9: cost 0 inf + 376165 7.988 * [simplify]: Simplified to (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b) 7.988 * [simplify]: Simplified (2 2) to (λ (a b c) (/.p16 (/.p16 (+.p16 (*.p16 (+.p16 (neg.p16 b) b) (+.p16 (neg.p16 b) (neg.p16 b))) (*.p16 (real->posit16 4) (*.p16 a c))) (*.p16 (real->posit16 2) a)) (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b))) 7.988 * * * * [progress]: [ 10 / 10 ] simplifiying candidate #posit16 4) (*.p16 a c))) (*.p16 (real->posit16 2) a)) (+.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c)))))))> 7.989 * [simplify]: Simplifying (+.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c))))) 7.989 * * [simplify]: iters left: 5 (12 enodes) 7.992 * * [simplify]: iters left: 4 (31 enodes) 7.998 * * [simplify]: iters left: 3 (64 enodes) 8.011 * * [simplify]: iters left: 2 (183 enodes) 8.095 * * [simplify]: Extracting #0: cost 1 inf + 0 8.095 * * [simplify]: Extracting #1: cost 6 inf + 0 8.096 * * [simplify]: Extracting #2: cost 10 inf + 1 8.096 * * [simplify]: Extracting #3: cost 22 inf + 804 8.096 * * [simplify]: Extracting #4: cost 64 inf + 1445 8.097 * * [simplify]: Extracting #5: cost 140 inf + 3371 8.099 * * [simplify]: Extracting #6: cost 220 inf + 13396 8.108 * * [simplify]: Extracting #7: cost 134 inf + 134080 8.130 * * [simplify]: Extracting #8: cost 16 inf + 340223 8.161 * * [simplify]: Extracting #9: cost 0 inf + 376165 8.189 * [simplify]: Simplified to (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b) 8.190 * [simplify]: Simplified (2 2) to (λ (a b c) (/.p16 (/.p16 (+.p16 (*.p16 (+.p16 (neg.p16 b) b) (+.p16 (neg.p16 b) (neg.p16 b))) (*.p16 (real->posit16 4) (*.p16 a c))) (*.p16 (real->posit16 2) a)) (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b))) 8.190 * * * [progress]: adding candidates to table 8.882 * * [progress]: iteration 4 / 4 8.882 * * * [progress]: picking best candidate 9.057 * * * * [pick]: Picked #posit16 4) a) c)) (*.p16 (real->posit16 2) a)) (+.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c)))))))> 9.057 * * * [progress]: localizing error 9.458 * * * [progress]: generating rewritten candidates 9.458 * * * * [progress]: [ 1 / 4 ] rewriting at (2 2) 9.461 * * * * [progress]: [ 2 / 4 ] rewriting at (2 1) 9.463 * * * * [progress]: [ 3 / 4 ] rewriting at (2 2 2 1 2) 9.467 * * * * [progress]: [ 4 / 4 ] rewriting at (2 2 2) 9.468 * * * [progress]: generating series expansions 9.468 * * * * [progress]: [ 1 / 4 ] generating series at (2 2) 9.468 * * * * [progress]: [ 2 / 4 ] generating series at (2 1) 9.468 * * * * [progress]: [ 3 / 4 ] generating series at (2 2 2 1 2) 9.468 * * * * [progress]: [ 4 / 4 ] generating series at (2 2 2) 9.468 * * * [progress]: simplifying candidates 9.468 * * * * [progress]: [ 1 / 8 ] simplifiying candidate #posit16 4) a) c)) (*.p16 (real->posit16 2) a)) (+.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c)))) (neg.p16 b))))> 9.468 * * * * [progress]: [ 2 / 8 ] simplifiying candidate #posit16 4) a) c)) (real->posit16 2)) a) (+.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c)))))))> 9.468 * * * * [progress]: [ 3 / 8 ] simplifiying candidate #posit16 4) a) c)) (*.p16 (real->posit16 2) a)) (+.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 (real->posit16 4) a) c))))))> 9.468 * * * * [progress]: [ 4 / 8 ] simplifiying candidate #posit16 4) a) c)) (*.p16 (real->posit16 2) a)) (+.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 a c) (real->posit16 4)))))))> 9.469 * * * * [progress]: [ 5 / 8 ] simplifiying candidate #posit16 4) a) c)) (*.p16 (real->posit16 2) a)) (+.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c)))))))> 9.469 * * * * [progress]: [ 6 / 8 ] simplifiying candidate #posit16 4) a) c)) (*.p16 (real->posit16 2) a)) (+.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c)))))))> 9.469 * * * * [progress]: [ 7 / 8 ] simplifiying candidate #posit16 4) a) c)) (*.p16 (real->posit16 2) a)) (+.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c)))))))> 9.469 * * * * [progress]: [ 8 / 8 ] simplifiying candidate #posit16 4) a) c)) (*.p16 (real->posit16 2) a)) (+.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c)))))))> 9.469 * * * [progress]: adding candidates to table 9.994 * [progress]: [Phase 3 of 3] Extracting. 9.995 * * [regime]: Finding splitpoints for: (#posit16 4) (*.p16 a c)))) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c)))))) (+.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c)))))) (*.p16 (real->posit16 2) a)))> #posit16 4) a) c)) (real->posit16 2)) a) (+.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c)))))))> #posit16 4) a) c)))) (*.p16 (real->posit16 2) a)))> #posit16 4) (*.p16 a c))))) (real->posit16 2)) a))> #posit16 4) a) c)) (*.p16 (real->posit16 2) a)) (+.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 (real->posit16 4) a) c))))))> #posit16 4) a) c)) (*.p16 (*.p16 (real->posit16 2) a) (+.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c))))))))> #posit16 4) (*.p16 a c))) (*.p16 (*.p16 (real->posit16 2) a) (+.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c))))))))> #posit16 4) (*.p16 a c))) (real->posit16 2)) a) (+.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c)))))))>) 10.001 * * * [regime-changes]: Trying 3 branch expressions: (c a b) 10.002 * * * * [regimes]: Trying to branch on c from (#posit16 4) (*.p16 a c)))) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c)))))) (+.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c)))))) (*.p16 (real->posit16 2) a)))> #posit16 4) a) c)) (real->posit16 2)) a) (+.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c)))))))> #posit16 4) a) c)))) (*.p16 (real->posit16 2) a)))> #posit16 4) (*.p16 a c))))) (real->posit16 2)) a))> #posit16 4) a) c)) (*.p16 (real->posit16 2) a)) (+.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 (real->posit16 4) a) c))))))> #posit16 4) a) c)) (*.p16 (*.p16 (real->posit16 2) a) (+.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c))))))))> #posit16 4) (*.p16 a c))) (*.p16 (*.p16 (real->posit16 2) a) (+.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c))))))))> #posit16 4) (*.p16 a c))) (real->posit16 2)) a) (+.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c)))))))>) 10.321 * * * * [regimes]: Trying to branch on a from (#posit16 4) (*.p16 a c)))) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c)))))) (+.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c)))))) (*.p16 (real->posit16 2) a)))> #posit16 4) a) c)) (real->posit16 2)) a) (+.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c)))))))> #posit16 4) a) c)))) (*.p16 (real->posit16 2) a)))> #posit16 4) (*.p16 a c))))) (real->posit16 2)) a))> #posit16 4) a) c)) (*.p16 (real->posit16 2) a)) (+.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 (real->posit16 4) a) c))))))> #posit16 4) a) c)) (*.p16 (*.p16 (real->posit16 2) a) (+.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c))))))))> #posit16 4) (*.p16 a c))) (*.p16 (*.p16 (real->posit16 2) a) (+.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c))))))))> #posit16 4) (*.p16 a c))) (real->posit16 2)) a) (+.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c)))))))>) 10.686 * * * * [regimes]: Trying to branch on b from (#posit16 4) (*.p16 a c)))) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c)))))) (+.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c)))))) (*.p16 (real->posit16 2) a)))> #posit16 4) a) c)) (real->posit16 2)) a) (+.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c)))))))> #posit16 4) a) c)))) (*.p16 (real->posit16 2) a)))> #posit16 4) (*.p16 a c))))) (real->posit16 2)) a))> #posit16 4) a) c)) (*.p16 (real->posit16 2) a)) (+.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 (real->posit16 4) a) c))))))> #posit16 4) a) c)) (*.p16 (*.p16 (real->posit16 2) a) (+.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c))))))))> #posit16 4) (*.p16 a c))) (*.p16 (*.p16 (real->posit16 2) a) (+.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c))))))))> #posit16 4) (*.p16 a c))) (real->posit16 2)) a) (+.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c)))))))>) 11.017 * * * [regime]: Found split indices: #