1550699423.419 * [misc]progress: [Phase 1 of 3] Setting up. 1550699423.421 * * * [misc]progress: [1/2] Preparing points 1550699423.423 * * * * [misc]points: Sampling 256 additional inputs, on iter 0 have 0 / 256 1550699423.435 * * * * [misc]points: Computing exacts on every 16 of 256 points to ramp up precision 1550699423.622 * * * * [misc]points: Setting MPFR precision to 64 1550699423.712 * * * * [misc]points: Setting MPFR precision to 320 1550699423.767 * * * * [misc]points: Computing exacts on every 8 of 256 points to ramp up precision 1550699423.876 * * * * [misc]points: Setting MPFR precision to 64 1550699423.881 * * * * [misc]points: Setting MPFR precision to 320 1550699423.949 * * * * [misc]points: Computing exacts on every 4 of 256 points to ramp up precision 1550699424.081 * * * * [misc]points: Setting MPFR precision to 64 1550699424.090 * * * * [misc]points: Setting MPFR precision to 320 1550699424.102 * * * * [misc]points: Computing exacts on every 2 of 256 points to ramp up precision 1550699424.109 * * * * [misc]points: Setting MPFR precision to 64 1550699424.120 * * * * [misc]points: Setting MPFR precision to 320 1550699424.133 * * * * [misc]points: Computing exacts for 256 points 1550699424.178 * * * * [misc]points: Setting MPFR precision to 64 1550699424.224 * * * * [misc]points: Setting MPFR precision to 320 1550699424.268 * * * * [misc]points: Filtering points with unrepresentable outputs 1550699424.294 * * * * [misc]points: Sampling 84 additional inputs, on iter 1 have 172 / 256 1550699424.295 * * * * [misc]points: Computing exacts on every 5 of 84 points to ramp up precision 1550699424.301 * * * * [misc]points: Setting MPFR precision to 64 1550699424.303 * * * * [misc]points: Setting MPFR precision to 320 1550699424.306 * * * * [misc]points: Computing exacts on every 2 of 84 points to ramp up precision 1550699424.311 * * * * [misc]points: Setting MPFR precision to 64 1550699424.315 * * * * [misc]points: Setting MPFR precision to 320 1550699424.320 * * * * [misc]points: Computing exacts for 84 points 1550699424.325 * * * * [misc]points: Setting MPFR precision to 64 1550699424.338 * * * * [misc]points: Setting MPFR precision to 320 1550699424.353 * * * * [misc]points: Filtering points with unrepresentable outputs 1550699424.406 * * * * [misc]points: Sampling 23 additional inputs, on iter 2 have 233 / 256 1550699424.406 * * * * [misc]points: Computing exacts for 23 points 1550699424.411 * * * * [misc]points: Setting MPFR precision to 64 1550699424.415 * * * * [misc]points: Setting MPFR precision to 320 1550699424.421 * * * * [misc]points: Filtering points with unrepresentable outputs 1550699424.423 * * * * [misc]points: Sampling 7 additional inputs, on iter 3 have 249 / 256 1550699424.424 * * * * [misc]points: Computing exacts for 7 points 1550699424.429 * * * * [misc]points: Setting MPFR precision to 64 1550699424.430 * * * * [misc]points: Setting MPFR precision to 320 1550699424.432 * * * * [misc]points: Filtering points with unrepresentable outputs 1550699424.432 * * * * [misc]points: Sampling 4 additional inputs, on iter 4 have 252 / 256 1550699424.432 * * * * [misc]points: Computing exacts for 4 points 1550699424.437 * * * * [misc]points: Setting MPFR precision to 64 1550699424.438 * * * * [misc]points: Setting MPFR precision to 320 1550699424.438 * * * * [misc]points: Filtering points with unrepresentable outputs 1550699424.439 * * * * [misc]points: Sampling 4 additional inputs, on iter 5 have 255 / 256 1550699424.439 * * * * [misc]points: Computing exacts for 4 points 1550699424.444 * * * * [misc]points: Setting MPFR precision to 64 1550699424.445 * * * * [misc]points: Setting MPFR precision to 320 1550699424.445 * * * * [misc]points: Filtering points with unrepresentable outputs 1550699424.446 * * * * [exit]points: Sampled 259 points with exact outputs 1550699424.447 * * * [misc]progress: [2/2] Setting up program. 1550699424.500 * [misc]progress: [Phase 2 of 3] Improving. 1550699424.500 * * * * [misc]progress: [ 1 / 1 ] simplifiying candidate #posit16 4) (*.p16 a c))))) (*.p16 (real->posit16 2) a)))> 1550699424.502 * [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)) 1550699424.504 * * [misc]simplify: iters left: 6 (16 enodes) 1550699424.520 * * [misc]simplify: iters left: 5 (39 enodes) 1550699424.535 * * [misc]simplify: iters left: 4 (72 enodes) 1550699424.565 * * [misc]simplify: iters left: 3 (196 enodes) 1550699425.227 * * [misc]simplify: Extracting #0: cost 1 inf + 0 1550699425.227 * * [misc]simplify: Extracting #1: cost 5 inf + 0 1550699425.228 * * [misc]simplify: Extracting #2: cost 11 inf + 1 1550699425.228 * * [misc]simplify: Extracting #3: cost 16 inf + 2 1550699425.228 * * [misc]simplify: Extracting #4: cost 26 inf + 807 1550699425.229 * * [misc]simplify: Extracting #5: cost 66 inf + 1770 1550699425.230 * * [misc]simplify: Extracting #6: cost 135 inf + 3695 1550699425.232 * * [misc]simplify: Extracting #7: cost 209 inf + 14082 1550699425.238 * * [misc]simplify: Extracting #8: cost 138 inf + 107732 1550699425.268 * * [misc]simplify: Extracting #9: cost 36 inf + 289941 1550699425.293 * * [misc]simplify: Extracting #10: cost 2 inf + 355093 1550699425.318 * * [misc]simplify: Extracting #11: cost 1 inf + 357016 1550699425.343 * * [misc]simplify: Extracting #12: cost 0 inf + 360620 1550699425.367 * [exit]simplify: Simplified to (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b) (*.p16 (real->posit16 2) a)) 1550699425.368 * [misc]simplify: Simplified (2) to (λ (a b c) (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b) (*.p16 (real->posit16 2) a))) 1550699425.457 * * [misc]progress: iteration 1 / 4 1550699425.457 * * * [misc]progress: picking best candidate 1550699425.496 * * * * [misc]pick: Picked #posit16 4)))) b) (*.p16 (real->posit16 2) a)))> 1550699425.497 * * * [misc]progress: localizing error 1550699425.989 * * * [misc]progress: generating rewritten candidates 1550699425.990 * * * * [misc]progress: [ 1 / 4 ] rewriting at (2 1) 1550699425.994 * * * * [misc]progress: [ 2 / 4 ] rewriting at (2 1 1) 1550699425.995 * * * * [misc]progress: [ 3 / 4 ] rewriting at (2) 1550699426.000 * * * * [misc]progress: [ 4 / 4 ] rewriting at (2 1 1 1 2) 1550699426.006 * * * [misc]progress: generating series expansions 1550699426.006 * * * * [misc]progress: [ 1 / 4 ] generating series at (2 1) 1550699426.006 * * * * [misc]progress: [ 2 / 4 ] generating series at (2 1 1) 1550699426.006 * * * * [misc]progress: [ 3 / 4 ] generating series at (2) 1550699426.007 * * * * [misc]progress: [ 4 / 4 ] generating series at (2 1 1 1 2) 1550699426.007 * * * [misc]progress: simplifying candidates 1550699426.007 * * * * [misc]progress: [ 1 / 10 ] simplifiying candidate #posit16 4)))) (neg.p16 b)) (*.p16 (real->posit16 2) a)))> 1550699426.007 * * * * [misc]progress: [ 2 / 10 ] simplifiying candidate #posit16 4)))) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4))))) (*.p16 b b)) (+.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b)) (*.p16 (real->posit16 2) a)))> 1550699426.007 * * * * [misc]progress: [ 3 / 10 ] simplifiying candidate #posit16 4)))) b) (real->posit16 2)) a))> 1550699426.007 * * * * [misc]progress: [ 4 / 10 ] simplifiying candidate #posit16 4)))) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4))))) (*.p16 b b)) (*.p16 (*.p16 (real->posit16 2) a) (+.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b))))> 1550699426.007 * [enter]simplify: Simplifying (-.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4))))) (*.p16 b b)) 1550699426.007 * * [misc]simplify: iters left: 6 (12 enodes) 1550699426.014 * * [misc]simplify: iters left: 5 (39 enodes) 1550699426.028 * * [misc]simplify: iters left: 4 (111 enodes) 1550699426.096 * * [misc]simplify: iters left: 3 (427 enodes) 1550699426.523 * * [misc]simplify: Extracting #0: cost 1 inf + 0 1550699426.523 * * [misc]simplify: Extracting #1: cost 47 inf + 0 1550699426.524 * * [misc]simplify: Extracting #2: cost 231 inf + 0 1550699426.526 * * [misc]simplify: Extracting #3: cost 400 inf + 3216 1550699426.541 * * [misc]simplify: Extracting #4: cost 473 inf + 191470 1550699426.618 * * [misc]simplify: Extracting #5: cost 180 inf + 866467 1550699426.727 * * [misc]simplify: Extracting #6: cost 4 inf + 1232579 1550699426.843 * * [misc]simplify: Extracting #7: cost 0 inf + 1241757 1550699426.958 * [exit]simplify: Simplified to (-.p16 (real->posit16 0.0) (*.p16 (*.p16 a c) (real->posit16 4))) 1550699426.958 * [misc]simplify: Simplified (2 1) to (λ (a b c) (/.p16 (-.p16 (real->posit16 0.0) (*.p16 (*.p16 a c) (real->posit16 4))) (*.p16 (*.p16 (real->posit16 2) a) (+.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b)))) 1550699426.958 * * * * [misc]progress: [ 5 / 10 ] simplifiying candidate #posit16 4))))) b) (*.p16 (real->posit16 2) a)))> 1550699426.958 * * * * [misc]progress: [ 6 / 10 ] simplifiying candidate #posit16 4) (*.p16 c a)))) b) (*.p16 (real->posit16 2) a)))> 1550699426.959 * * * * [misc]progress: [ 7 / 10 ] simplifiying candidate #posit16 4)))) b) (*.p16 (real->posit16 2) a)))> 1550699426.959 * [enter]simplify: Simplifying (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b) (*.p16 (real->posit16 2) a)) 1550699426.959 * * [misc]simplify: iters left: 6 (15 enodes) 1550699426.966 * * [misc]simplify: iters left: 5 (43 enodes) 1550699426.982 * * [misc]simplify: iters left: 4 (88 enodes) 1550699427.022 * * [misc]simplify: iters left: 3 (307 enodes) 1550699427.232 * * [misc]simplify: Extracting #0: cost 1 inf + 0 1550699427.232 * * [misc]simplify: Extracting #1: cost 31 inf + 0 1550699427.232 * * [misc]simplify: Extracting #2: cost 125 inf + 1 1550699427.234 * * [misc]simplify: Extracting #3: cost 193 inf + 2734 1550699427.236 * * [misc]simplify: Extracting #4: cost 253 inf + 8433 1550699427.241 * * [misc]simplify: Extracting #5: cost 273 inf + 63950 1550699427.273 * * [misc]simplify: Extracting #6: cost 175 inf + 356651 1550699427.326 * * [misc]simplify: Extracting #7: cost 6 inf + 666712 1550699427.381 * * [misc]simplify: Extracting #8: cost 0 inf + 674735 1550699427.439 * [exit]simplify: Simplified to (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 a c) (real->posit16 4)))) b) (*.p16 a (real->posit16 2))) 1550699427.439 * [misc]simplify: Simplified (2) to (λ (a b c) (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 a c) (real->posit16 4)))) b) (*.p16 a (real->posit16 2)))) 1550699427.439 * * * * [misc]progress: [ 8 / 10 ] simplifiying candidate #posit16 4)))) b) (*.p16 (real->posit16 2) a)))> 1550699427.440 * [enter]simplify: Simplifying (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b) (*.p16 (real->posit16 2) a)) 1550699427.440 * * [misc]simplify: iters left: 6 (15 enodes) 1550699427.447 * * [misc]simplify: iters left: 5 (43 enodes) 1550699427.462 * * [misc]simplify: iters left: 4 (88 enodes) 1550699427.500 * * [misc]simplify: iters left: 3 (307 enodes) 1550699427.720 * * [misc]simplify: Extracting #0: cost 1 inf + 0 1550699427.720 * * [misc]simplify: Extracting #1: cost 31 inf + 0 1550699427.720 * * [misc]simplify: Extracting #2: cost 125 inf + 1 1550699427.722 * * [misc]simplify: Extracting #3: cost 193 inf + 2734 1550699427.724 * * [misc]simplify: Extracting #4: cost 253 inf + 8433 1550699427.729 * * [misc]simplify: Extracting #5: cost 273 inf + 63950 1550699427.755 * * [misc]simplify: Extracting #6: cost 175 inf + 356651 1550699427.807 * * [misc]simplify: Extracting #7: cost 6 inf + 666712 1550699427.868 * * [misc]simplify: Extracting #8: cost 0 inf + 674735 1550699427.924 * [exit]simplify: Simplified to (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 a c) (real->posit16 4)))) b) (*.p16 a (real->posit16 2))) 1550699427.924 * [misc]simplify: Simplified (2) to (λ (a b c) (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 a c) (real->posit16 4)))) b) (*.p16 a (real->posit16 2)))) 1550699427.925 * * * * [misc]progress: [ 9 / 10 ] simplifiying candidate #posit16 4)))) b) (*.p16 (real->posit16 2) a)))> 1550699427.925 * [enter]simplify: Simplifying (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b) (*.p16 (real->posit16 2) a)) 1550699427.925 * * [misc]simplify: iters left: 6 (15 enodes) 1550699427.932 * * [misc]simplify: iters left: 5 (43 enodes) 1550699427.948 * * [misc]simplify: iters left: 4 (88 enodes) 1550699427.985 * * [misc]simplify: iters left: 3 (307 enodes) 1550699428.201 * * [misc]simplify: Extracting #0: cost 1 inf + 0 1550699428.201 * * [misc]simplify: Extracting #1: cost 31 inf + 0 1550699428.202 * * [misc]simplify: Extracting #2: cost 125 inf + 1 1550699428.203 * * [misc]simplify: Extracting #3: cost 193 inf + 2734 1550699428.205 * * [misc]simplify: Extracting #4: cost 253 inf + 8433 1550699428.210 * * [misc]simplify: Extracting #5: cost 273 inf + 63950 1550699428.236 * * [misc]simplify: Extracting #6: cost 175 inf + 356651 1550699428.292 * * [misc]simplify: Extracting #7: cost 6 inf + 666712 1550699428.350 * * [misc]simplify: Extracting #8: cost 0 inf + 674735 1550699428.406 * [exit]simplify: Simplified to (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 a c) (real->posit16 4)))) b) (*.p16 a (real->posit16 2))) 1550699428.406 * [misc]simplify: Simplified (2) to (λ (a b c) (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 a c) (real->posit16 4)))) b) (*.p16 a (real->posit16 2)))) 1550699428.406 * * * * [misc]progress: [ 10 / 10 ] simplifiying candidate #posit16 4)))) b) (*.p16 (real->posit16 2) a)))> 1550699428.407 * [enter]simplify: Simplifying (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b) (*.p16 (real->posit16 2) a)) 1550699428.407 * * [misc]simplify: iters left: 6 (15 enodes) 1550699428.414 * * [misc]simplify: iters left: 5 (43 enodes) 1550699428.429 * * [misc]simplify: iters left: 4 (88 enodes) 1550699428.470 * * [misc]simplify: iters left: 3 (307 enodes) 1550699428.683 * * [misc]simplify: Extracting #0: cost 1 inf + 0 1550699428.683 * * [misc]simplify: Extracting #1: cost 31 inf + 0 1550699428.684 * * [misc]simplify: Extracting #2: cost 125 inf + 1 1550699428.685 * * [misc]simplify: Extracting #3: cost 193 inf + 2734 1550699428.687 * * [misc]simplify: Extracting #4: cost 253 inf + 8433 1550699428.693 * * [misc]simplify: Extracting #5: cost 273 inf + 63950 1550699428.725 * * [misc]simplify: Extracting #6: cost 175 inf + 356651 1550699428.775 * * [misc]simplify: Extracting #7: cost 6 inf + 666712 1550699428.831 * * [misc]simplify: Extracting #8: cost 0 inf + 674735 1550699428.889 * [exit]simplify: Simplified to (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 a c) (real->posit16 4)))) b) (*.p16 a (real->posit16 2))) 1550699428.890 * [misc]simplify: Simplified (2) to (λ (a b c) (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 a c) (real->posit16 4)))) b) (*.p16 a (real->posit16 2)))) 1550699428.890 * * * [misc]progress: adding candidates to table 1550699429.783 * * [misc]progress: iteration 2 / 4 1550699429.783 * * * [misc]progress: picking best candidate 1550699429.966 * * * * [misc]pick: Picked #posit16 4))))) b) (*.p16 (real->posit16 2) a)))> 1550699429.966 * * * [misc]progress: localizing error 1550699430.307 * * * [misc]progress: generating rewritten candidates 1550699430.307 * * * * [misc]progress: [ 1 / 4 ] rewriting at (2 1) 1550699430.310 * * * * [misc]progress: [ 2 / 4 ] rewriting at (2 1 1) 1550699430.310 * * * * [misc]progress: [ 3 / 4 ] rewriting at (2) 1550699430.315 * * * * [misc]progress: [ 4 / 4 ] rewriting at (2 1 1 1) 1550699430.321 * * * [misc]progress: generating series expansions 1550699430.321 * * * * [misc]progress: [ 1 / 4 ] generating series at (2 1) 1550699430.321 * * * * [misc]progress: [ 2 / 4 ] generating series at (2 1 1) 1550699430.321 * * * * [misc]progress: [ 3 / 4 ] generating series at (2) 1550699430.321 * * * * [misc]progress: [ 4 / 4 ] generating series at (2 1 1 1) 1550699430.321 * * * [misc]progress: simplifying candidates 1550699430.321 * * * * [misc]progress: [ 1 / 10 ] simplifiying candidate #posit16 4))))) (neg.p16 b)) (*.p16 (real->posit16 2) a)))> 1550699430.322 * * * * [misc]progress: [ 2 / 10 ] simplifiying candidate #posit16 4))))) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4)))))) (*.p16 b b)) (+.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4))))) b)) (*.p16 (real->posit16 2) a)))> 1550699430.322 * * * * [misc]progress: [ 3 / 10 ] simplifiying candidate #posit16 4))))) b) (real->posit16 2)) a))> 1550699430.322 * * * * [misc]progress: [ 4 / 10 ] simplifiying candidate #posit16 4))))) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4)))))) (*.p16 b b)) (*.p16 (*.p16 (real->posit16 2) a) (+.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4))))) b))))> 1550699430.322 * [enter]simplify: Simplifying (-.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4))))) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4)))))) (*.p16 b b)) 1550699430.322 * * [misc]simplify: iters left: 6 (12 enodes) 1550699430.328 * * [misc]simplify: iters left: 5 (39 enodes) 1550699430.343 * * [misc]simplify: iters left: 4 (111 enodes) 1550699430.397 * * [misc]simplify: iters left: 3 (424 enodes) 1550699430.828 * * [misc]simplify: Extracting #0: cost 1 inf + 0 1550699430.829 * * [misc]simplify: Extracting #1: cost 47 inf + 0 1550699430.830 * * [misc]simplify: Extracting #2: cost 231 inf + 0 1550699430.832 * * [misc]simplify: Extracting #3: cost 400 inf + 3615 1550699430.847 * * [misc]simplify: Extracting #4: cost 466 inf + 182833 1550699430.913 * * [misc]simplify: Extracting #5: cost 208 inf + 789169 1550699431.028 * * [misc]simplify: Extracting #6: cost 3 inf + 1219441 1550699431.142 * * [misc]simplify: Extracting #7: cost 0 inf + 1225733 1550699431.260 * [exit]simplify: Simplified to (-.p16 (real->posit16 0.0) (*.p16 (*.p16 (real->posit16 4) a) c)) 1550699431.260 * [misc]simplify: Simplified (2 1) to (λ (a b c) (/.p16 (-.p16 (real->posit16 0.0) (*.p16 (*.p16 (real->posit16 4) a) c)) (*.p16 (*.p16 (real->posit16 2) a) (+.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4))))) b)))) 1550699431.260 * * * * [misc]progress: [ 5 / 10 ] simplifiying candidate #posit16 4)))))) b) (*.p16 (real->posit16 2) a)))> 1550699431.260 * * * * [misc]progress: [ 6 / 10 ] simplifiying candidate #posit16 4))) (*.p16 c (*.p16 a (real->posit16 4))))) (+.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4)))))) b) (*.p16 (real->posit16 2) a)))> 1550699431.260 * * * * [misc]progress: [ 7 / 10 ] simplifiying candidate #posit16 4))))) b) (*.p16 (real->posit16 2) a)))> 1550699431.260 * * * * [misc]progress: [ 8 / 10 ] simplifiying candidate #posit16 4))))) b) (*.p16 (real->posit16 2) a)))> 1550699431.260 * * * * [misc]progress: [ 9 / 10 ] simplifiying candidate #posit16 4))))) b) (*.p16 (real->posit16 2) a)))> 1550699431.260 * * * * [misc]progress: [ 10 / 10 ] simplifiying candidate #posit16 4))))) b) (*.p16 (real->posit16 2) a)))> 1550699431.260 * * * [misc]progress: adding candidates to table 1550699431.969 * * [misc]progress: iteration 3 / 4 1550699431.969 * * * [misc]progress: picking best candidate 1550699432.186 * * * * [misc]pick: Picked #posit16 4)))) b) (real->posit16 2)) a))> 1550699432.187 * * * [misc]progress: localizing error 1550699432.307 * * * [misc]progress: generating rewritten candidates 1550699432.307 * * * * [misc]progress: [ 1 / 4 ] rewriting at (2 1 1) 1550699432.310 * * * * [misc]progress: [ 2 / 4 ] rewriting at (2 1 1 1) 1550699432.310 * * * * [misc]progress: [ 3 / 4 ] rewriting at (2) 1550699432.315 * * * * [misc]progress: [ 4 / 4 ] rewriting at (2 1 1 1 1 2) 1550699432.319 * * * [misc]progress: generating series expansions 1550699432.319 * * * * [misc]progress: [ 1 / 4 ] generating series at (2 1 1) 1550699432.319 * * * * [misc]progress: [ 2 / 4 ] generating series at (2 1 1 1) 1550699432.319 * * * * [misc]progress: [ 3 / 4 ] generating series at (2) 1550699432.319 * * * * [misc]progress: [ 4 / 4 ] generating series at (2 1 1 1 1 2) 1550699432.319 * * * [misc]progress: simplifying candidates 1550699432.319 * * * * [misc]progress: [ 1 / 9 ] simplifiying candidate #posit16 4)))) (neg.p16 b)) (real->posit16 2)) a))> 1550699432.319 * * * * [misc]progress: [ 2 / 9 ] simplifiying candidate #posit16 4)))) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4))))) (*.p16 b b)) (+.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b)) (real->posit16 2)) a))> 1550699432.319 * * * * [misc]progress: [ 3 / 9 ] simplifiying candidate #posit16 4)))) b) (*.p16 a (real->posit16 2))))> 1550699432.319 * [enter]simplify: Simplifying (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b) 1550699432.320 * * [misc]simplify: iters left: 5 (11 enodes) 1550699432.325 * * [misc]simplify: iters left: 4 (35 enodes) 1550699432.337 * * [misc]simplify: iters left: 3 (76 enodes) 1550699432.371 * * [misc]simplify: iters left: 2 (261 enodes) 1550699432.551 * * [misc]simplify: Extracting #0: cost 1 inf + 0 1550699432.551 * * [misc]simplify: Extracting #1: cost 12 inf + 0 1550699432.551 * * [misc]simplify: Extracting #2: cost 66 inf + 1 1550699432.552 * * [misc]simplify: Extracting #3: cost 146 inf + 403 1550699432.554 * * [misc]simplify: Extracting #4: cost 205 inf + 4899 1550699432.557 * * [misc]simplify: Extracting #5: cost 241 inf + 36908 1550699432.576 * * [misc]simplify: Extracting #6: cost 176 inf + 271128 1550699432.618 * * [misc]simplify: Extracting #7: cost 10 inf + 555810 1550699432.665 * * [misc]simplify: Extracting #8: cost 0 inf + 573768 1550699432.714 * [exit]simplify: Simplified to (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 a c) (real->posit16 4)))) b) 1550699432.715 * [misc]simplify: Simplified (2 1) to (λ (a b c) (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 a c) (real->posit16 4)))) b) (*.p16 a (real->posit16 2)))) 1550699432.715 * * * * [misc]progress: [ 4 / 9 ] simplifiying candidate #posit16 4))))) b) (real->posit16 2)) a))> 1550699432.715 * * * * [misc]progress: [ 5 / 9 ] simplifiying candidate #posit16 4) (*.p16 c a)))) b) (real->posit16 2)) a))> 1550699432.715 * * * * [misc]progress: [ 6 / 9 ] simplifiying candidate #posit16 4)))) b) (real->posit16 2)) a))> 1550699432.715 * * * * [misc]progress: [ 7 / 9 ] simplifiying candidate #posit16 4)))) b) (real->posit16 2)) a))> 1550699432.715 * * * * [misc]progress: [ 8 / 9 ] simplifiying candidate #posit16 4)))) b) (real->posit16 2)) a))> 1550699432.715 * * * * [misc]progress: [ 9 / 9 ] simplifiying candidate #posit16 4)))) b) (real->posit16 2)) a))> 1550699432.715 * * * [misc]progress: adding candidates to table 1550699433.339 * * [misc]progress: iteration 4 / 4 1550699433.339 * * * [misc]progress: picking best candidate 1550699433.564 * * * * [misc]pick: Picked #posit16 4)))) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4))))) (*.p16 b b)) (+.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b)) (real->posit16 2)) a))> 1550699433.565 * * * [misc]progress: localizing error 1550699433.872 * * * [misc]progress: generating rewritten candidates 1550699433.873 * * * * [misc]progress: [ 1 / 4 ] rewriting at (2 1 1 1) 1550699433.876 * * * * [misc]progress: [ 2 / 4 ] rewriting at (2 1 1 2) 1550699433.879 * * * * [misc]progress: [ 3 / 4 ] rewriting at (2 1 1) 1550699433.886 * * * * [misc]progress: [ 4 / 4 ] rewriting at (2 1 1 2 1) 1550699433.886 * * * [misc]progress: generating series expansions 1550699433.886 * * * * [misc]progress: [ 1 / 4 ] generating series at (2 1 1 1) 1550699433.887 * * * * [misc]progress: [ 2 / 4 ] generating series at (2 1 1 2) 1550699433.887 * * * * [misc]progress: [ 3 / 4 ] generating series at (2 1 1) 1550699433.887 * * * * [misc]progress: [ 4 / 4 ] generating series at (2 1 1 2 1) 1550699433.887 * * * [misc]progress: simplifying candidates 1550699433.887 * * * * [misc]progress: [ 1 / 10 ] simplifiying candidate #posit16 4)))) b) (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b)) (+.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b)) (real->posit16 2)) a))> 1550699433.887 * [enter]simplify: Simplifying (+.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b) 1550699433.887 * * [misc]simplify: iters left: 5 (11 enodes) 1550699433.893 * * [misc]simplify: iters left: 4 (30 enodes) 1550699433.903 * * [misc]simplify: iters left: 3 (62 enodes) 1550699433.931 * * [misc]simplify: iters left: 2 (181 enodes) 1550699434.059 * * [misc]simplify: Extracting #0: cost 1 inf + 0 1550699434.060 * * [misc]simplify: Extracting #1: cost 3 inf + 0 1550699434.060 * * [misc]simplify: Extracting #2: cost 3 inf + 1 1550699434.060 * * [misc]simplify: Extracting #3: cost 17 inf + 1 1550699434.060 * * [misc]simplify: Extracting #4: cost 59 inf + 322 1550699434.061 * * [misc]simplify: Extracting #5: cost 133 inf + 1287 1550699434.063 * * [misc]simplify: Extracting #6: cost 191 inf + 13674 1550699434.069 * * [misc]simplify: Extracting #7: cost 131 inf + 89074 1550699434.089 * * [misc]simplify: Extracting #8: cost 15 inf + 300176 1550699434.115 * * [misc]simplify: Extracting #9: cost 0 inf + 335752 1550699434.140 * [exit]simplify: Simplified to (+.p16 b (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 a c) (real->posit16 4))))) 1550699434.140 * [misc]simplify: Simplified (2 1 1 1 1) to (λ (a b c) (/.p16 (/.p16 (/.p16 (*.p16 (+.p16 b (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 a c) (real->posit16 4))))) (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b)) (+.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b)) (real->posit16 2)) a)) 1550699434.141 * [enter]simplify: Simplifying (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b) 1550699434.141 * * [misc]simplify: iters left: 5 (11 enodes) 1550699434.146 * * [misc]simplify: iters left: 4 (35 enodes) 1550699434.159 * * [misc]simplify: iters left: 3 (76 enodes) 1550699434.192 * * [misc]simplify: iters left: 2 (261 enodes) 1550699434.370 * * [misc]simplify: Extracting #0: cost 1 inf + 0 1550699434.370 * * [misc]simplify: Extracting #1: cost 12 inf + 0 1550699434.370 * * [misc]simplify: Extracting #2: cost 66 inf + 1 1550699434.371 * * [misc]simplify: Extracting #3: cost 146 inf + 403 1550699434.373 * * [misc]simplify: Extracting #4: cost 205 inf + 4899 1550699434.382 * * [misc]simplify: Extracting #5: cost 241 inf + 36908 1550699434.399 * * [misc]simplify: Extracting #6: cost 176 inf + 271128 1550699434.437 * * [misc]simplify: Extracting #7: cost 10 inf + 555810 1550699434.485 * * [misc]simplify: Extracting #8: cost 0 inf + 573768 1550699434.533 * [exit]simplify: Simplified to (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 a c) (real->posit16 4)))) b) 1550699434.533 * [misc]simplify: Simplified (2 1 1 1 2) to (λ (a b c) (/.p16 (/.p16 (/.p16 (*.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b) (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 a c) (real->posit16 4)))) b)) (+.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b)) (real->posit16 2)) a)) 1550699434.533 * * * * [misc]progress: [ 2 / 10 ] simplifiying candidate #posit16 4)))) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4))))) (neg.p16 (*.p16 b b))) (+.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b)) (real->posit16 2)) a))> 1550699434.533 * * * * [misc]progress: [ 3 / 10 ] simplifiying candidate #posit16 4)))) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4))))) (*.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))))) (*.p16 (*.p16 b b) (*.p16 b b))) (+.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4))))) (*.p16 b b))) (+.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b)) (real->posit16 2)) a))> 1550699434.533 * * * * [misc]progress: [ 4 / 10 ] simplifiying candidate #posit16 4)))) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4))))) (*.p16 b b)) (+.p16 b (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))))) (real->posit16 2)) a))> 1550699434.533 * * * * [misc]progress: [ 5 / 10 ] simplifiying candidate #posit16 4)))) b) (/.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b) (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b))) (real->posit16 2)) a))> 1550699434.534 * [enter]simplify: Simplifying (+.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b) 1550699434.534 * * [misc]simplify: iters left: 5 (11 enodes) 1550699434.539 * * [misc]simplify: iters left: 4 (30 enodes) 1550699434.553 * * [misc]simplify: iters left: 3 (62 enodes) 1550699434.579 * * [misc]simplify: iters left: 2 (181 enodes) 1550699434.702 * * [misc]simplify: Extracting #0: cost 1 inf + 0 1550699434.702 * * [misc]simplify: Extracting #1: cost 3 inf + 0 1550699434.702 * * [misc]simplify: Extracting #2: cost 3 inf + 1 1550699434.702 * * [misc]simplify: Extracting #3: cost 17 inf + 1 1550699434.702 * * [misc]simplify: Extracting #4: cost 59 inf + 322 1550699434.703 * * [misc]simplify: Extracting #5: cost 133 inf + 1287 1550699434.705 * * [misc]simplify: Extracting #6: cost 191 inf + 13674 1550699434.710 * * [misc]simplify: Extracting #7: cost 131 inf + 89074 1550699434.729 * * [misc]simplify: Extracting #8: cost 15 inf + 300176 1550699434.754 * * [misc]simplify: Extracting #9: cost 0 inf + 335752 1550699434.780 * [exit]simplify: Simplified to (+.p16 b (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 a c) (real->posit16 4))))) 1550699434.780 * [misc]simplify: Simplified (2 1 1 1) to (λ (a b c) (/.p16 (/.p16 (/.p16 (+.p16 b (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 a c) (real->posit16 4))))) (/.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b) (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b))) (real->posit16 2)) a)) 1550699434.780 * * * * [misc]progress: [ 6 / 10 ] simplifiying candidate #posit16 4)))) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4))))) (*.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))))) (*.p16 (*.p16 b b) (*.p16 b b))) (*.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b) (+.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4))))) (*.p16 b b)))) (real->posit16 2)) a))> 1550699434.781 * [enter]simplify: Simplifying (-.p16 (*.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4))))) (*.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))))) (*.p16 (*.p16 b b) (*.p16 b b))) 1550699434.781 * * [misc]simplify: iters left: 6 (14 enodes) 1550699434.788 * * [misc]simplify: iters left: 5 (50 enodes) 1550699434.809 * * [misc]simplify: iters left: 4 (159 enodes) 1550699434.908 * * [misc]simplify: Extracting #0: cost 1 inf + 0 1550699434.908 * * [misc]simplify: Extracting #1: cost 28 inf + 0 1550699434.909 * * [misc]simplify: Extracting #2: cost 80 inf + 0 1550699434.909 * * [misc]simplify: Extracting #3: cost 153 inf + 322 1550699434.911 * * [misc]simplify: Extracting #4: cost 182 inf + 8818 1550699434.916 * * [misc]simplify: Extracting #5: cost 166 inf + 64938 1550699434.933 * * [misc]simplify: Extracting #6: cost 44 inf + 258136 1550699434.961 * * [misc]simplify: Extracting #7: cost 1 inf + 350866 1550699434.991 * * [misc]simplify: Extracting #8: cost 0 inf + 351990 1550699435.017 * [exit]simplify: Simplified to (*.p16 (-.p16 (*.p16 b b) (+.p16 (*.p16 (*.p16 a c) (real->posit16 4)) (*.p16 b b))) (+.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 a c) (real->posit16 4))) (*.p16 b b))) 1550699435.017 * [misc]simplify: Simplified (2 1 1 1) to (λ (a b c) (/.p16 (/.p16 (/.p16 (*.p16 (-.p16 (*.p16 b b) (+.p16 (*.p16 (*.p16 a c) (real->posit16 4)) (*.p16 b b))) (+.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 a c) (real->posit16 4))) (*.p16 b b))) (*.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b) (+.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4))))) (*.p16 b b)))) (real->posit16 2)) a)) 1550699435.017 * * * * [misc]progress: [ 7 / 10 ] simplifiying candidate #posit16 4)))) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4))))) (*.p16 b b)) (+.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b)) (real->posit16 2)) a))> 1550699435.018 * * * * [misc]progress: [ 8 / 10 ] simplifiying candidate #posit16 4)))) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4))))) (*.p16 b b)) (+.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b)) (real->posit16 2)) a))> 1550699435.018 * * * * [misc]progress: [ 9 / 10 ] simplifiying candidate #posit16 4)))) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4))))) (*.p16 b b)) (+.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b)) (real->posit16 2)) a))> 1550699435.018 * * * * [misc]progress: [ 10 / 10 ] simplifiying candidate #posit16 4)))) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4))))) (*.p16 b b)) (+.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b)) (real->posit16 2)) a))> 1550699435.018 * * * [misc]progress: adding candidates to table 1550699435.922 * [misc]progress: [Phase 3 of 3] Extracting. 1550699435.923 * * [misc]regime: Finding splitpoints for: (#posit16 4)))) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4))))) (*.p16 b b)) (+.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b)) (*.p16 (real->posit16 2) a)))> #posit16 4)))) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4))))) (*.p16 b b)) (*.p16 (*.p16 (real->posit16 2) a) (+.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b))))> #posit16 4)))) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4))))) (*.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))))) (*.p16 (*.p16 b b) (*.p16 b b))) (+.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4))))) (*.p16 b b))) (+.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b)) (real->posit16 2)) a))> #posit16 4))) (*.p16 c (*.p16 a (real->posit16 4))))) (+.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4)))))) b) (*.p16 (real->posit16 2) a)))> #posit16 4))))) b) (*.p16 (real->posit16 2) a)))> #posit16 4)))) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4))))) (*.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))))) (*.p16 (*.p16 b b) (*.p16 b b))) (*.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b) (+.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4))))) (*.p16 b b)))) (real->posit16 2)) a))> #posit16 4)))) b) (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b)) (+.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b)) (real->posit16 2)) a))> #posit16 4))))) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4)))))) (*.p16 b b)) (*.p16 (*.p16 (real->posit16 2) a) (+.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4))))) b))))> #posit16 4)))) b) (/.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b) (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b))) (real->posit16 2)) a))>) 1550699435.932 * * * [misc]regime-changes: Trying 3 branch expressions: (c a b) 1550699435.933 * * * * [misc]regimes: Trying to branch on c from (#posit16 4)))) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4))))) (*.p16 b b)) (+.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b)) (*.p16 (real->posit16 2) a)))> #posit16 4)))) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4))))) (*.p16 b b)) (*.p16 (*.p16 (real->posit16 2) a) (+.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b))))> #posit16 4)))) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4))))) (*.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))))) (*.p16 (*.p16 b b) (*.p16 b b))) (+.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4))))) (*.p16 b b))) (+.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b)) (real->posit16 2)) a))> #posit16 4))) (*.p16 c (*.p16 a (real->posit16 4))))) (+.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4)))))) b) (*.p16 (real->posit16 2) a)))> #posit16 4))))) b) (*.p16 (real->posit16 2) a)))> #posit16 4)))) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4))))) (*.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))))) (*.p16 (*.p16 b b) (*.p16 b b))) (*.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b) (+.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4))))) (*.p16 b b)))) (real->posit16 2)) a))> #posit16 4)))) b) (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b)) (+.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b)) (real->posit16 2)) a))> #posit16 4))))) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4)))))) (*.p16 b b)) (*.p16 (*.p16 (real->posit16 2) a) (+.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4))))) b))))> #posit16 4)))) b) (/.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b) (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b))) (real->posit16 2)) a))>) 1550699436.644 * * * * [misc]regimes: Trying to branch on a from (#posit16 4)))) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4))))) (*.p16 b b)) (+.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b)) (*.p16 (real->posit16 2) a)))> #posit16 4)))) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4))))) (*.p16 b b)) (*.p16 (*.p16 (real->posit16 2) a) (+.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b))))> #posit16 4)))) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4))))) (*.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))))) (*.p16 (*.p16 b b) (*.p16 b b))) (+.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4))))) (*.p16 b b))) (+.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b)) (real->posit16 2)) a))> #posit16 4))) (*.p16 c (*.p16 a (real->posit16 4))))) (+.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4)))))) b) (*.p16 (real->posit16 2) a)))> #posit16 4))))) b) (*.p16 (real->posit16 2) a)))> #posit16 4)))) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4))))) (*.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))))) (*.p16 (*.p16 b b) (*.p16 b b))) (*.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b) (+.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4))))) (*.p16 b b)))) (real->posit16 2)) a))> #posit16 4)))) b) (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b)) (+.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b)) (real->posit16 2)) a))> #posit16 4))))) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4)))))) (*.p16 b b)) (*.p16 (*.p16 (real->posit16 2) a) (+.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4))))) b))))> #posit16 4)))) b) (/.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b) (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b))) (real->posit16 2)) a))>) 1550699437.343 * * * * [misc]regimes: Trying to branch on b from (#posit16 4)))) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4))))) (*.p16 b b)) (+.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b)) (*.p16 (real->posit16 2) a)))> #posit16 4)))) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4))))) (*.p16 b b)) (*.p16 (*.p16 (real->posit16 2) a) (+.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b))))> #posit16 4)))) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4))))) (*.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))))) (*.p16 (*.p16 b b) (*.p16 b b))) (+.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4))))) (*.p16 b b))) (+.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b)) (real->posit16 2)) a))> #posit16 4))) (*.p16 c (*.p16 a (real->posit16 4))))) (+.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4)))))) b) (*.p16 (real->posit16 2) a)))> #posit16 4))))) b) (*.p16 (real->posit16 2) a)))> #posit16 4)))) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4))))) (*.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))))) (*.p16 (*.p16 b b) (*.p16 b b))) (*.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b) (+.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4))))) (*.p16 b b)))) (real->posit16 2)) a))> #posit16 4)))) b) (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b)) (+.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b)) (real->posit16 2)) a))> #posit16 4))))) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4)))))) (*.p16 b b)) (*.p16 (*.p16 (real->posit16 2) a) (+.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4))))) b))))> #posit16 4)))) b) (/.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b) (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b))) (real->posit16 2)) a))>) 1550699438.050 * * * [misc]regime: Found split indices: #