1550699424.647 * [misc]progress: [Phase 1 of 3] Setting up. 1550699424.650 * * * [misc]progress: [1/2] Preparing points 1550699424.651 * * * * [misc]points: Sampling 256 additional inputs, on iter 0 have 0 / 256 1550699424.661 * * * * [misc]points: Computing exacts on every 16 of 256 points to ramp up precision 1550699424.745 * * * * [misc]points: Setting MPFR precision to 64 1550699424.749 * * * * [misc]points: Setting MPFR precision to 320 1550699424.753 * * * * [misc]points: Computing exacts on every 8 of 256 points to ramp up precision 1550699424.759 * * * * [misc]points: Setting MPFR precision to 64 1550699424.762 * * * * [misc]points: Setting MPFR precision to 320 1550699424.823 * * * * [misc]points: Computing exacts on every 4 of 256 points to ramp up precision 1550699424.829 * * * * [misc]points: Setting MPFR precision to 64 1550699424.836 * * * * [misc]points: Setting MPFR precision to 320 1550699424.845 * * * * [misc]points: Computing exacts on every 2 of 256 points to ramp up precision 1550699424.850 * * * * [misc]points: Setting MPFR precision to 64 1550699424.861 * * * * [misc]points: Setting MPFR precision to 320 1550699424.875 * * * * [misc]points: Computing exacts for 256 points 1550699424.881 * * * * [misc]points: Setting MPFR precision to 64 1550699424.911 * * * * [misc]points: Setting MPFR precision to 320 1550699424.947 * * * * [misc]points: Filtering points with unrepresentable outputs 1550699424.967 * * * * [misc]points: Sampling 84 additional inputs, on iter 1 have 172 / 256 1550699424.968 * * * * [misc]points: Computing exacts on every 5 of 84 points to ramp up precision 1550699424.973 * * * * [misc]points: Setting MPFR precision to 64 1550699424.975 * * * * [misc]points: Setting MPFR precision to 320 1550699424.977 * * * * [misc]points: Computing exacts on every 2 of 84 points to ramp up precision 1550699424.982 * * * * [misc]points: Setting MPFR precision to 64 1550699424.989 * * * * [misc]points: Setting MPFR precision to 320 1550699424.993 * * * * [misc]points: Computing exacts for 84 points 1550699424.999 * * * * [misc]points: Setting MPFR precision to 64 1550699425.010 * * * * [misc]points: Setting MPFR precision to 320 1550699425.069 * * * * [misc]points: Filtering points with unrepresentable outputs 1550699425.076 * * * * [misc]points: Sampling 23 additional inputs, on iter 2 have 233 / 256 1550699425.077 * * * * [misc]points: Computing exacts for 23 points 1550699425.084 * * * * [misc]points: Setting MPFR precision to 64 1550699425.088 * * * * [misc]points: Setting MPFR precision to 320 1550699425.091 * * * * [misc]points: Filtering points with unrepresentable outputs 1550699425.093 * * * * [misc]points: Sampling 7 additional inputs, on iter 3 have 249 / 256 1550699425.094 * * * * [misc]points: Computing exacts for 7 points 1550699425.099 * * * * [misc]points: Setting MPFR precision to 64 1550699425.100 * * * * [misc]points: Setting MPFR precision to 320 1550699425.101 * * * * [misc]points: Filtering points with unrepresentable outputs 1550699425.101 * * * * [misc]points: Sampling 4 additional inputs, on iter 4 have 252 / 256 1550699425.102 * * * * [misc]points: Computing exacts for 4 points 1550699425.107 * * * * [misc]points: Setting MPFR precision to 64 1550699425.107 * * * * [misc]points: Setting MPFR precision to 320 1550699425.108 * * * * [misc]points: Filtering points with unrepresentable outputs 1550699425.109 * * * * [misc]points: Sampling 4 additional inputs, on iter 5 have 255 / 256 1550699425.109 * * * * [misc]points: Computing exacts for 4 points 1550699425.114 * * * * [misc]points: Setting MPFR precision to 64 1550699425.115 * * * * [misc]points: Setting MPFR precision to 320 1550699425.115 * * * * [misc]points: Filtering points with unrepresentable outputs 1550699425.116 * * * * [exit]points: Sampled 259 points with exact outputs 1550699425.117 * * * [misc]progress: [2/2] Setting up program. 1550699425.168 * [misc]progress: [Phase 2 of 3] Improving. 1550699425.168 * * * * [misc]progress: [ 1 / 1 ] simplifiying candidate #posit16 4) (*.p16 a c))))) (*.p16 (real->posit16 2) a)))> 1550699425.170 * [enter]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)) 1550699425.172 * * [misc]simplify: iters left: 6 (16 enodes) 1550699425.185 * * [misc]simplify: iters left: 5 (45 enodes) 1550699425.203 * * [misc]simplify: iters left: 4 (91 enodes) 1550699425.262 * * [misc]simplify: iters left: 3 (310 enodes) 1550699425.460 * * [misc]simplify: Extracting #0: cost 1 inf + 0 1550699425.460 * * [misc]simplify: Extracting #1: cost 31 inf + 0 1550699425.461 * * [misc]simplify: Extracting #2: cost 123 inf + 1 1550699425.462 * * [misc]simplify: Extracting #3: cost 201 inf + 1129 1550699425.464 * * [misc]simplify: Extracting #4: cost 263 inf + 9871 1550699425.470 * * [misc]simplify: Extracting #5: cost 270 inf + 82040 1550699425.499 * * [misc]simplify: Extracting #6: cost 192 inf + 363234 1550699425.559 * * [misc]simplify: Extracting #7: cost 15 inf + 679901 1550699425.618 * * [misc]simplify: Extracting #8: cost 0 inf + 712557 1550699425.678 * [exit]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)) 1550699425.679 * [misc]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))) 1550699425.740 * * [misc]progress: iteration 1 / 4 1550699425.740 * * * [misc]progress: picking best candidate 1550699425.789 * * * * [misc]pick: Picked #posit16 4) (*.p16 a c))))) (*.p16 (real->posit16 2) a)))> 1550699425.789 * * * [misc]progress: localizing error 1550699426.344 * * * [misc]progress: generating rewritten candidates 1550699426.344 * * * * [misc]progress: [ 1 / 4 ] rewriting at (2 1) 1550699426.350 * * * * [misc]progress: [ 2 / 4 ] rewriting at (2 1 2) 1550699426.351 * * * * [misc]progress: [ 3 / 4 ] rewriting at (2) 1550699426.357 * * * * [misc]progress: [ 4 / 4 ] rewriting at (2 1 2 1 2) 1550699426.362 * * * [misc]progress: generating series expansions 1550699426.362 * * * * [misc]progress: [ 1 / 4 ] generating series at (2 1) 1550699426.363 * * * * [misc]progress: [ 2 / 4 ] generating series at (2 1 2) 1550699426.363 * * * * [misc]progress: [ 3 / 4 ] generating series at (2) 1550699426.363 * * * * [misc]progress: [ 4 / 4 ] generating series at (2 1 2 1 2) 1550699426.363 * * * [misc]progress: simplifying candidates 1550699426.363 * * * * [misc]progress: [ 1 / 10 ] simplifiying candidate #posit16 4) (*.p16 a c)))))) (*.p16 (real->posit16 2) a)))> 1550699426.363 * * * * [misc]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)))> 1550699426.363 * * * * [misc]progress: [ 3 / 10 ] simplifiying candidate #posit16 4) (*.p16 a c))))) (real->posit16 2)) a))> 1550699426.363 * * * * [misc]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))))))))> 1550699426.364 * [enter]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)))))) 1550699426.364 * * [misc]simplify: iters left: 6 (14 enodes) 1550699426.370 * * [misc]simplify: iters left: 5 (42 enodes) 1550699426.387 * * [misc]simplify: iters left: 4 (117 enodes) 1550699426.457 * * [misc]simplify: iters left: 3 (426 enodes) 1550699426.836 * * [misc]simplify: Extracting #0: cost 1 inf + 0 1550699426.836 * * [misc]simplify: Extracting #1: cost 51 inf + 0 1550699426.837 * * [misc]simplify: Extracting #2: cost 242 inf + 0 1550699426.839 * * [misc]simplify: Extracting #3: cost 408 inf + 4895 1550699426.860 * * [misc]simplify: Extracting #4: cost 386 inf + 288425 1550699426.945 * * [misc]simplify: Extracting #5: cost 133 inf + 992840 1550699427.062 * * [misc]simplify: Extracting #6: cost 2 inf + 1243260 1550699427.177 * * [misc]simplify: Extracting #7: cost 0 inf + 1250148 1550699427.293 * [exit]simplify: Simplified to (+.p16 (*.p16 (+.p16 (neg.p16 b) b) (+.p16 (neg.p16 b) (neg.p16 b))) (*.p16 (real->posit16 4) (*.p16 a c))) 1550699427.293 * [misc]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)))))))) 1550699427.293 * * * * [misc]progress: [ 5 / 10 ] simplifiying candidate #posit16 4) a) c)))) (*.p16 (real->posit16 2) a)))> 1550699427.294 * * * * [misc]progress: [ 6 / 10 ] simplifiying candidate #posit16 4))))) (*.p16 (real->posit16 2) a)))> 1550699427.294 * * * * [misc]progress: [ 7 / 10 ] simplifiying candidate #posit16 4) (*.p16 a c))))) (*.p16 (real->posit16 2) a)))> 1550699427.294 * [enter]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)) 1550699427.294 * * [misc]simplify: iters left: 6 (16 enodes) 1550699427.302 * * [misc]simplify: iters left: 5 (45 enodes) 1550699427.318 * * [misc]simplify: iters left: 4 (91 enodes) 1550699427.358 * * [misc]simplify: iters left: 3 (310 enodes) 1550699427.552 * * [misc]simplify: Extracting #0: cost 1 inf + 0 1550699427.552 * * [misc]simplify: Extracting #1: cost 31 inf + 0 1550699427.553 * * [misc]simplify: Extracting #2: cost 123 inf + 1 1550699427.554 * * [misc]simplify: Extracting #3: cost 201 inf + 1129 1550699427.556 * * [misc]simplify: Extracting #4: cost 263 inf + 9871 1550699427.563 * * [misc]simplify: Extracting #5: cost 270 inf + 82040 1550699427.591 * * [misc]simplify: Extracting #6: cost 192 inf + 363234 1550699427.652 * * [misc]simplify: Extracting #7: cost 15 inf + 679901 1550699427.713 * * [misc]simplify: Extracting #8: cost 0 inf + 712557 1550699427.772 * [exit]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)) 1550699427.772 * [misc]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))) 1550699427.772 * * * * [misc]progress: [ 8 / 10 ] simplifiying candidate #posit16 4) (*.p16 a c))))) (*.p16 (real->posit16 2) a)))> 1550699427.773 * [enter]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)) 1550699427.773 * * [misc]simplify: iters left: 6 (16 enodes) 1550699427.780 * * [misc]simplify: iters left: 5 (45 enodes) 1550699427.796 * * [misc]simplify: iters left: 4 (91 enodes) 1550699427.835 * * [misc]simplify: iters left: 3 (310 enodes) 1550699428.030 * * [misc]simplify: Extracting #0: cost 1 inf + 0 1550699428.030 * * [misc]simplify: Extracting #1: cost 31 inf + 0 1550699428.030 * * [misc]simplify: Extracting #2: cost 123 inf + 1 1550699428.032 * * [misc]simplify: Extracting #3: cost 201 inf + 1129 1550699428.034 * * [misc]simplify: Extracting #4: cost 263 inf + 9871 1550699428.039 * * [misc]simplify: Extracting #5: cost 270 inf + 82040 1550699428.073 * * [misc]simplify: Extracting #6: cost 192 inf + 363234 1550699428.128 * * [misc]simplify: Extracting #7: cost 15 inf + 679901 1550699428.189 * * [misc]simplify: Extracting #8: cost 0 inf + 712557 1550699428.249 * [exit]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)) 1550699428.249 * [misc]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))) 1550699428.249 * * * * [misc]progress: [ 9 / 10 ] simplifiying candidate #posit16 4) (*.p16 a c))))) (*.p16 (real->posit16 2) a)))> 1550699428.249 * [enter]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)) 1550699428.250 * * [misc]simplify: iters left: 6 (16 enodes) 1550699428.257 * * [misc]simplify: iters left: 5 (45 enodes) 1550699428.272 * * [misc]simplify: iters left: 4 (91 enodes) 1550699428.310 * * [misc]simplify: iters left: 3 (310 enodes) 1550699428.513 * * [misc]simplify: Extracting #0: cost 1 inf + 0 1550699428.513 * * [misc]simplify: Extracting #1: cost 31 inf + 0 1550699428.514 * * [misc]simplify: Extracting #2: cost 123 inf + 1 1550699428.515 * * [misc]simplify: Extracting #3: cost 201 inf + 1129 1550699428.517 * * [misc]simplify: Extracting #4: cost 263 inf + 9871 1550699428.523 * * [misc]simplify: Extracting #5: cost 270 inf + 82040 1550699428.551 * * [misc]simplify: Extracting #6: cost 192 inf + 363234 1550699428.606 * * [misc]simplify: Extracting #7: cost 15 inf + 679901 1550699428.665 * * [misc]simplify: Extracting #8: cost 0 inf + 712557 1550699428.728 * [exit]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)) 1550699428.728 * [misc]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))) 1550699428.728 * * * * [misc]progress: [ 10 / 10 ] simplifiying candidate #posit16 4) (*.p16 a c))))) (*.p16 (real->posit16 2) a)))> 1550699428.728 * [enter]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)) 1550699428.728 * * [misc]simplify: iters left: 6 (16 enodes) 1550699428.735 * * [misc]simplify: iters left: 5 (45 enodes) 1550699428.751 * * [misc]simplify: iters left: 4 (91 enodes) 1550699428.789 * * [misc]simplify: iters left: 3 (310 enodes) 1550699428.991 * * [misc]simplify: Extracting #0: cost 1 inf + 0 1550699428.991 * * [misc]simplify: Extracting #1: cost 31 inf + 0 1550699428.992 * * [misc]simplify: Extracting #2: cost 123 inf + 1 1550699428.993 * * [misc]simplify: Extracting #3: cost 201 inf + 1129 1550699428.995 * * [misc]simplify: Extracting #4: cost 263 inf + 9871 1550699429.002 * * [misc]simplify: Extracting #5: cost 270 inf + 82040 1550699429.030 * * [misc]simplify: Extracting #6: cost 192 inf + 363234 1550699429.082 * * [misc]simplify: Extracting #7: cost 15 inf + 679901 1550699429.146 * * [misc]simplify: Extracting #8: cost 0 inf + 712557 1550699429.205 * [exit]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)) 1550699429.205 * [misc]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))) 1550699429.205 * * * [misc]progress: adding candidates to table 1550699430.247 * * [misc]progress: iteration 2 / 4 1550699430.247 * * * [misc]progress: picking best candidate 1550699430.465 * * * * [misc]pick: Picked #posit16 4) (*.p16 a c))))) (real->posit16 2)) a))> 1550699430.465 * * * [misc]progress: localizing error 1550699430.576 * * * [misc]progress: generating rewritten candidates 1550699430.576 * * * * [misc]progress: [ 1 / 4 ] rewriting at (2 1 1) 1550699430.579 * * * * [misc]progress: [ 2 / 4 ] rewriting at (2 1 1 2) 1550699430.580 * * * * [misc]progress: [ 3 / 4 ] rewriting at (2) 1550699430.586 * * * * [misc]progress: [ 4 / 4 ] rewriting at (2 1 1 2 1 2) 1550699430.589 * * * [misc]progress: generating series expansions 1550699430.590 * * * * [misc]progress: [ 1 / 4 ] generating series at (2 1 1) 1550699430.590 * * * * [misc]progress: [ 2 / 4 ] generating series at (2 1 1 2) 1550699430.590 * * * * [misc]progress: [ 3 / 4 ] generating series at (2) 1550699430.590 * * * * [misc]progress: [ 4 / 4 ] generating series at (2 1 1 2 1 2) 1550699430.590 * * * [misc]progress: simplifying candidates 1550699430.590 * * * * [misc]progress: [ 1 / 9 ] simplifiying candidate #posit16 4) (*.p16 a c)))))) (real->posit16 2)) a))> 1550699430.590 * * * * [misc]progress: [ 2 / 9 ] 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)))))) (real->posit16 2)) a))> 1550699430.590 * * * * [misc]progress: [ 3 / 9 ] simplifiying candidate #posit16 4) (*.p16 a c))))) (*.p16 a (real->posit16 2))))> 1550699430.590 * [enter]simplify: Simplifying (-.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c))))) 1550699430.591 * * [misc]simplify: iters left: 5 (12 enodes) 1550699430.597 * * [misc]simplify: iters left: 4 (37 enodes) 1550699430.611 * * [misc]simplify: iters left: 3 (79 enodes) 1550699430.660 * * [misc]simplify: iters left: 2 (262 enodes) 1550699430.841 * * [misc]simplify: Extracting #0: cost 1 inf + 0 1550699430.841 * * [misc]simplify: Extracting #1: cost 17 inf + 0 1550699430.842 * * [misc]simplify: Extracting #2: cost 88 inf + 1 1550699430.843 * * [misc]simplify: Extracting #3: cost 166 inf + 804 1550699430.844 * * [misc]simplify: Extracting #4: cost 230 inf + 3734 1550699430.850 * * [misc]simplify: Extracting #5: cost 225 inf + 64494 1550699430.875 * * [misc]simplify: Extracting #6: cost 137 inf + 332479 1550699430.919 * * [misc]simplify: Extracting #7: cost 1 inf + 596662 1550699430.976 * * [misc]simplify: Extracting #8: cost 0 inf + 599226 1550699431.028 * [exit]simplify: Simplified to (-.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4))))) 1550699431.028 * [misc]simplify: Simplified (2 1) to (λ (a b c) (/.p16 (-.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4))))) (*.p16 a (real->posit16 2)))) 1550699431.028 * * * * [misc]progress: [ 4 / 9 ] simplifiying candidate #posit16 4) a) c)))) (real->posit16 2)) a))> 1550699431.028 * * * * [misc]progress: [ 5 / 9 ] simplifiying candidate #posit16 4))))) (real->posit16 2)) a))> 1550699431.028 * * * * [misc]progress: [ 6 / 9 ] simplifiying candidate #posit16 4) (*.p16 a c))))) (real->posit16 2)) a))> 1550699431.028 * * * * [misc]progress: [ 7 / 9 ] simplifiying candidate #posit16 4) (*.p16 a c))))) (real->posit16 2)) a))> 1550699431.029 * * * * [misc]progress: [ 8 / 9 ] simplifiying candidate #posit16 4) (*.p16 a c))))) (real->posit16 2)) a))> 1550699431.029 * * * * [misc]progress: [ 9 / 9 ] simplifiying candidate #posit16 4) (*.p16 a c))))) (real->posit16 2)) a))> 1550699431.029 * * * [misc]progress: adding candidates to table 1550699431.735 * * [misc]progress: iteration 3 / 4 1550699431.736 * * * [misc]progress: picking best candidate 1550699431.924 * * * * [misc]pick: Picked #posit16 4) a) c)))) (*.p16 (real->posit16 2) a)))> 1550699431.924 * * * [misc]progress: localizing error 1550699432.207 * * * [misc]progress: generating rewritten candidates 1550699432.207 * * * * [misc]progress: [ 1 / 4 ] rewriting at (2 1) 1550699432.210 * * * * [misc]progress: [ 2 / 4 ] rewriting at (2 1 2) 1550699432.211 * * * * [misc]progress: [ 3 / 4 ] rewriting at (2) 1550699432.216 * * * * [misc]progress: [ 4 / 4 ] rewriting at (2 1 2 1) 1550699432.235 * * * [misc]progress: generating series expansions 1550699432.235 * * * * [misc]progress: [ 1 / 4 ] generating series at (2 1) 1550699432.235 * * * * [misc]progress: [ 2 / 4 ] generating series at (2 1 2) 1550699432.235 * * * * [misc]progress: [ 3 / 4 ] generating series at (2) 1550699432.235 * * * * [misc]progress: [ 4 / 4 ] generating series at (2 1 2 1) 1550699432.235 * * * [misc]progress: simplifying candidates 1550699432.235 * * * * [misc]progress: [ 1 / 10 ] simplifiying candidate #posit16 4) a) c))))) (*.p16 (real->posit16 2) a)))> 1550699432.235 * * * * [misc]progress: [ 2 / 10 ] simplifiying candidate #posit16 4) a) c))) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 (real->posit16 4) a) c))))) (+.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 (real->posit16 4) a) c))))) (*.p16 (real->posit16 2) a)))> 1550699432.235 * * * * [misc]progress: [ 3 / 10 ] simplifiying candidate #posit16 4) a) c)))) (real->posit16 2)) a))> 1550699432.235 * * * * [misc]progress: [ 4 / 10 ] simplifiying candidate #posit16 4) a) c))) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 (real->posit16 4) 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)))))))> 1550699432.236 * [enter]simplify: Simplifying (-.p16 (*.p16 (neg.p16 b) (neg.p16 b)) (*.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 (real->posit16 4) a) c))) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 (real->posit16 4) a) c))))) 1550699432.236 * * [misc]simplify: iters left: 6 (14 enodes) 1550699432.243 * * [misc]simplify: iters left: 5 (42 enodes) 1550699432.258 * * [misc]simplify: iters left: 4 (117 enodes) 1550699432.310 * * [misc]simplify: iters left: 3 (432 enodes) 1550699432.663 * * [misc]simplify: Extracting #0: cost 1 inf + 0 1550699432.664 * * [misc]simplify: Extracting #1: cost 51 inf + 0 1550699432.665 * * [misc]simplify: Extracting #2: cost 242 inf + 0 1550699432.667 * * [misc]simplify: Extracting #3: cost 412 inf + 3092 1550699432.684 * * [misc]simplify: Extracting #4: cost 427 inf + 239293 1550699432.761 * * [misc]simplify: Extracting #5: cost 159 inf + 940878 1550699432.868 * * [misc]simplify: Extracting #6: cost 1 inf + 1259592 1550699432.982 * * [misc]simplify: Extracting #7: cost 0 inf + 1262236 1550699433.093 * [exit]simplify: Simplified to (+.p16 (*.p16 (+.p16 (neg.p16 b) b) (+.p16 (neg.p16 b) (neg.p16 b))) (*.p16 c (*.p16 a (real->posit16 4)))) 1550699433.093 * [misc]simplify: Simplified (2 1) to (λ (a b c) (/.p16 (+.p16 (*.p16 (+.p16 (neg.p16 b) b) (+.p16 (neg.p16 b) (neg.p16 b))) (*.p16 c (*.p16 a (real->posit16 4)))) (*.p16 (*.p16 (real->posit16 2) a) (+.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 (real->posit16 4) a) c))))))) 1550699433.093 * * * * [misc]progress: [ 5 / 10 ] simplifiying candidate #posit16 4) a) c))))) (*.p16 (real->posit16 2) a)))> 1550699433.093 * * * * [misc]progress: [ 6 / 10 ] simplifiying candidate #posit16 4) a) c) (*.p16 (*.p16 (real->posit16 4) a) c))) (+.p16 (*.p16 b b) (*.p16 (*.p16 (real->posit16 4) a) c))))) (*.p16 (real->posit16 2) a)))> 1550699433.093 * * * * [misc]progress: [ 7 / 10 ] simplifiying candidate #posit16 4) a) c)))) (*.p16 (real->posit16 2) a)))> 1550699433.093 * * * * [misc]progress: [ 8 / 10 ] simplifiying candidate #posit16 4) a) c)))) (*.p16 (real->posit16 2) a)))> 1550699433.093 * * * * [misc]progress: [ 9 / 10 ] simplifiying candidate #posit16 4) a) c)))) (*.p16 (real->posit16 2) a)))> 1550699433.093 * * * * [misc]progress: [ 10 / 10 ] simplifiying candidate #posit16 4) a) c)))) (*.p16 (real->posit16 2) a)))> 1550699433.093 * * * [misc]progress: adding candidates to table 1550699433.876 * * [misc]progress: iteration 4 / 4 1550699433.876 * * * [misc]progress: picking best candidate 1550699434.126 * * * * [misc]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))))))))> 1550699434.126 * * * [misc]progress: localizing error 1550699434.481 * * * [misc]progress: generating rewritten candidates 1550699434.481 * * * * [misc]progress: [ 1 / 4 ] rewriting at (2 2 2) 1550699434.486 * * * * [misc]progress: [ 2 / 4 ] rewriting at (2) 1550699434.491 * * * * [misc]progress: [ 3 / 4 ] rewriting at (2 2 2 2) 1550699434.492 * * * * [misc]progress: [ 4 / 4 ] rewriting at (2 2 2 2 1 2) 1550699434.495 * * * [misc]progress: generating series expansions 1550699434.495 * * * * [misc]progress: [ 1 / 4 ] generating series at (2 2 2) 1550699434.495 * * * * [misc]progress: [ 2 / 4 ] generating series at (2) 1550699434.495 * * * * [misc]progress: [ 3 / 4 ] generating series at (2 2 2 2) 1550699434.495 * * * * [misc]progress: [ 4 / 4 ] generating series at (2 2 2 2 1 2) 1550699434.495 * * * [misc]progress: simplifying candidates 1550699434.495 * * * * [misc]progress: [ 1 / 8 ] 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)))))> 1550699434.495 * * * * [misc]progress: [ 2 / 8 ] 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)))))))> 1550699434.496 * [enter]simplify: Simplifying (+.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c))))) 1550699434.496 * * [misc]simplify: iters left: 5 (12 enodes) 1550699434.501 * * [misc]simplify: iters left: 4 (31 enodes) 1550699434.511 * * [misc]simplify: iters left: 3 (64 enodes) 1550699434.536 * * [misc]simplify: iters left: 2 (183 enodes) 1550699434.650 * * [misc]simplify: Extracting #0: cost 1 inf + 0 1550699434.650 * * [misc]simplify: Extracting #1: cost 6 inf + 0 1550699434.650 * * [misc]simplify: Extracting #2: cost 10 inf + 1 1550699434.651 * * [misc]simplify: Extracting #3: cost 22 inf + 804 1550699434.651 * * [misc]simplify: Extracting #4: cost 64 inf + 1445 1550699434.652 * * [misc]simplify: Extracting #5: cost 132 inf + 3371 1550699434.654 * * [misc]simplify: Extracting #6: cost 212 inf + 14038 1550699434.661 * * [misc]simplify: Extracting #7: cost 133 inf + 122101 1550699434.684 * * [misc]simplify: Extracting #8: cost 13 inf + 330931 1550699434.711 * * [misc]simplify: Extracting #9: cost 0 inf + 360062 1550699434.738 * [exit]simplify: Simplified to (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b) 1550699434.738 * [misc]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))) 1550699434.738 * * * * [misc]progress: [ 3 / 8 ] 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)))))))> 1550699434.738 * * * * [misc]progress: [ 4 / 8 ] 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))))))))> 1550699434.738 * * * * [misc]progress: [ 5 / 8 ] 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))))))))> 1550699434.739 * [enter]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))))))) 1550699434.739 * * [misc]simplify: iters left: 6 (21 enodes) 1550699434.749 * * [misc]simplify: iters left: 5 (61 enodes) 1550699434.774 * * [misc]simplify: iters left: 4 (154 enodes) 1550699434.845 * * [misc]simplify: iters left: 3 (373 enodes) 1550699435.138 * * [misc]simplify: Extracting #0: cost 1 inf + 0 1550699435.138 * * [misc]simplify: Extracting #1: cost 7 inf + 0 1550699435.139 * * [misc]simplify: Extracting #2: cost 59 inf + 0 1550699435.139 * * [misc]simplify: Extracting #3: cost 119 inf + 83 1550699435.141 * * [misc]simplify: Extracting #4: cost 137 inf + 11032 1550699435.144 * * [misc]simplify: Extracting #5: cost 183 inf + 27270 1550699435.152 * * [misc]simplify: Extracting #6: cost 223 inf + 84764 1550699435.174 * * [misc]simplify: Extracting #7: cost 60 inf + 347389 1550699435.210 * * [misc]simplify: Extracting #8: cost 1 inf + 460459 1550699435.243 * * [misc]simplify: Extracting #9: cost 0 inf + 461583 1550699435.277 * [exit]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))) 1550699435.277 * [misc]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)))) 1550699435.277 * * * * [misc]progress: [ 6 / 8 ] 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))))))))> 1550699435.278 * [enter]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))))))) 1550699435.278 * * [misc]simplify: iters left: 6 (21 enodes) 1550699435.286 * * [misc]simplify: iters left: 5 (61 enodes) 1550699435.308 * * [misc]simplify: iters left: 4 (154 enodes) 1550699435.371 * * [misc]simplify: iters left: 3 (373 enodes) 1550699435.629 * * [misc]simplify: Extracting #0: cost 1 inf + 0 1550699435.630 * * [misc]simplify: Extracting #1: cost 7 inf + 0 1550699435.630 * * [misc]simplify: Extracting #2: cost 59 inf + 0 1550699435.631 * * [misc]simplify: Extracting #3: cost 119 inf + 83 1550699435.632 * * [misc]simplify: Extracting #4: cost 137 inf + 11032 1550699435.636 * * [misc]simplify: Extracting #5: cost 183 inf + 27270 1550699435.645 * * [misc]simplify: Extracting #6: cost 223 inf + 84764 1550699435.670 * * [misc]simplify: Extracting #7: cost 60 inf + 347389 1550699435.710 * * [misc]simplify: Extracting #8: cost 1 inf + 460459 1550699435.748 * * [misc]simplify: Extracting #9: cost 0 inf + 461583 1550699435.786 * [exit]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))) 1550699435.786 * [misc]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)))) 1550699435.786 * * * * [misc]progress: [ 7 / 8 ] 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))))))))> 1550699435.786 * [enter]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))))))) 1550699435.787 * * [misc]simplify: iters left: 6 (21 enodes) 1550699435.796 * * [misc]simplify: iters left: 5 (61 enodes) 1550699435.821 * * [misc]simplify: iters left: 4 (154 enodes) 1550699435.889 * * [misc]simplify: iters left: 3 (373 enodes) 1550699436.170 * * [misc]simplify: Extracting #0: cost 1 inf + 0 1550699436.170 * * [misc]simplify: Extracting #1: cost 7 inf + 0 1550699436.171 * * [misc]simplify: Extracting #2: cost 59 inf + 0 1550699436.171 * * [misc]simplify: Extracting #3: cost 119 inf + 83 1550699436.173 * * [misc]simplify: Extracting #4: cost 137 inf + 11032 1550699436.177 * * [misc]simplify: Extracting #5: cost 183 inf + 27270 1550699436.185 * * [misc]simplify: Extracting #6: cost 223 inf + 84764 1550699436.210 * * [misc]simplify: Extracting #7: cost 60 inf + 347389 1550699436.724 * * [misc]simplify: Extracting #8: cost 1 inf + 460459 1550699436.760 * * [misc]simplify: Extracting #9: cost 0 inf + 461583 1550699436.794 * [exit]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))) 1550699436.794 * [misc]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)))) 1550699436.794 * * * * [misc]progress: [ 8 / 8 ] 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))))))))> 1550699436.795 * [enter]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))))))) 1550699436.795 * * [misc]simplify: iters left: 6 (21 enodes) 1550699436.804 * * [misc]simplify: iters left: 5 (61 enodes) 1550699436.828 * * [misc]simplify: iters left: 4 (154 enodes) 1550699436.892 * * [misc]simplify: iters left: 3 (373 enodes) 1550699437.159 * * [misc]simplify: Extracting #0: cost 1 inf + 0 1550699437.160 * * [misc]simplify: Extracting #1: cost 7 inf + 0 1550699437.160 * * [misc]simplify: Extracting #2: cost 59 inf + 0 1550699437.161 * * [misc]simplify: Extracting #3: cost 119 inf + 83 1550699437.162 * * [misc]simplify: Extracting #4: cost 137 inf + 11032 1550699437.166 * * [misc]simplify: Extracting #5: cost 183 inf + 27270 1550699437.175 * * [misc]simplify: Extracting #6: cost 223 inf + 84764 1550699437.200 * * [misc]simplify: Extracting #7: cost 60 inf + 347389 1550699437.239 * * [misc]simplify: Extracting #8: cost 1 inf + 460459 1550699437.277 * * [misc]simplify: Extracting #9: cost 0 inf + 461583 1550699437.315 * [exit]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))) 1550699437.315 * [misc]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)))) 1550699437.316 * * * [misc]progress: adding candidates to table 1550699438.196 * [misc]progress: [Phase 3 of 3] Extracting. 1550699438.197 * * [misc]regime: Finding splitpoints for: (#posit16 4) (*.p16 a c))))) (real->posit16 2)) a))> #posit16 4) a) c))) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 (real->posit16 4) 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)))))))> #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)))) (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)))))) (real->posit16 2)) a))> #posit16 4) a) c) (*.p16 (*.p16 (real->posit16 4) a) c))) (+.p16 (*.p16 b b) (*.p16 (*.p16 (real->posit16 4) a) c))))) (*.p16 (real->posit16 2) a)))> #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)))))))> #posit16 4) a) c)))) (*.p16 (real->posit16 2) a)))> #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))))>) 1550699438.203 * * * [misc]regime-changes: Trying 3 branch expressions: (c a b) 1550699438.204 * * * * [misc]regimes: Trying to branch on c from (#posit16 4) (*.p16 a c))))) (real->posit16 2)) a))> #posit16 4) a) c))) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 (real->posit16 4) 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)))))))> #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)))) (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)))))) (real->posit16 2)) a))> #posit16 4) a) c) (*.p16 (*.p16 (real->posit16 4) a) c))) (+.p16 (*.p16 b b) (*.p16 (*.p16 (real->posit16 4) a) c))))) (*.p16 (real->posit16 2) a)))> #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)))))))> #posit16 4) a) c)))) (*.p16 (real->posit16 2) a)))> #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))))>) 1550699438.842 * * * * [misc]regimes: Trying to branch on a from (#posit16 4) (*.p16 a c))))) (real->posit16 2)) a))> #posit16 4) a) c))) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 (real->posit16 4) 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)))))))> #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)))) (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)))))) (real->posit16 2)) a))> #posit16 4) a) c) (*.p16 (*.p16 (real->posit16 4) a) c))) (+.p16 (*.p16 b b) (*.p16 (*.p16 (real->posit16 4) a) c))))) (*.p16 (real->posit16 2) a)))> #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)))))))> #posit16 4) a) c)))) (*.p16 (real->posit16 2) a)))> #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))))>) 1550699439.542 * * * * [misc]regimes: Trying to branch on b from (#posit16 4) (*.p16 a c))))) (real->posit16 2)) a))> #posit16 4) a) c))) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 (real->posit16 4) 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)))))))> #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)))) (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)))))) (real->posit16 2)) a))> #posit16 4) a) c) (*.p16 (*.p16 (real->posit16 4) a) c))) (+.p16 (*.p16 b b) (*.p16 (*.p16 (real->posit16 4) a) c))))) (*.p16 (real->posit16 2) a)))> #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)))))))> #posit16 4) a) c)))) (*.p16 (real->posit16 2) a)))> #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))))>) 1550699440.233 * * * [misc]regime: Found split indices: #