1554305027.080 * [misc]progress: [Phase 1 of 3] Setting up. 1554305027.080 * * * [misc]progress: [1/2] Preparing points 1554305027.080 * * * * [misc]points: Sampling 256 additional inputs, on iter 0 have 0 / 256 1554305027.081 * * * * [misc]points: Computing exacts on every 16 of 256 points to ramp up precision 1554305027.083 * * * * [misc]points: Setting MPFR precision to 64 1554305027.084 * * * * [misc]points: Setting MPFR precision to 320 1554305027.086 * * * * [misc]points: Computing exacts on every 8 of 256 points to ramp up precision 1554305027.088 * * * * [misc]points: Setting MPFR precision to 64 1554305027.090 * * * * [misc]points: Setting MPFR precision to 320 1554305027.092 * * * * [misc]points: Computing exacts on every 4 of 256 points to ramp up precision 1554305027.094 * * * * [misc]points: Setting MPFR precision to 64 1554305027.098 * * * * [misc]points: Setting MPFR precision to 320 1554305027.102 * * * * [misc]points: Computing exacts on every 2 of 256 points to ramp up precision 1554305027.104 * * * * [misc]points: Setting MPFR precision to 64 1554305027.110 * * * * [misc]points: Setting MPFR precision to 320 1554305027.116 * * * * [misc]points: Computing exacts for 256 points 1554305027.118 * * * * [misc]points: Setting MPFR precision to 64 1554305027.137 * * * * [misc]points: Setting MPFR precision to 320 1554305027.154 * * * * [misc]points: Filtering points with unrepresentable outputs 1554305027.155 * * * * [exit]points: Sampled 256 points with exact outputs 1554305027.155 * * * [misc]progress: [2/2] Setting up program. 1554305027.167 * [misc]progress: [Phase 2 of 3] Improving. 1554305027.168 * * * * [misc]progress: [ 1 / 1 ] simplifiying candidate #posit16 1))) (sqrt.p16 x)))> 1554305027.168 * [enter]simplify: Simplifying (-.p16 (sqrt.p16 (+.p16 x (real->posit16 1))) (sqrt.p16 x)) 1554305027.168 * * [misc]simplify: iters left: 4 (7 enodes) 1554305027.171 * * [misc]simplify: iters left: 3 (20 enodes) 1554305027.177 * * [misc]simplify: iters left: 2 (32 enodes) 1554305027.189 * * [misc]simplify: iters left: 1 (92 enodes) 1554305027.237 * * [misc]simplify: Extracting #0: cost 1 inf + 0 1554305027.238 * * [misc]simplify: Extracting #1: cost 13 inf + 0 1554305027.238 * * [misc]simplify: Extracting #2: cost 67 inf + 0 1554305027.238 * * [misc]simplify: Extracting #3: cost 111 inf + 723 1554305027.239 * * [misc]simplify: Extracting #4: cost 94 inf + 7692 1554305027.241 * * [misc]simplify: Extracting #5: cost 25 inf + 47669 1554305027.246 * * [misc]simplify: Extracting #6: cost 0 inf + 67124 1554305027.251 * [exit]simplify: Simplified to (-.p16 (sqrt.p16 (+.p16 (real->posit16 1) x)) (sqrt.p16 x)) 1554305027.251 * [misc]simplify: Simplified (2) to (λ (x) (-.p16 (sqrt.p16 (+.p16 (real->posit16 1) x)) (sqrt.p16 x))) 1554305027.260 * * [misc]progress: iteration 1 / 4 1554305027.260 * * * [misc]progress: picking best candidate 1554305027.276 * * * * [misc]pick: Picked #posit16 1))) (sqrt.p16 x)))> 1554305027.276 * * * [misc]progress: localizing error 1554305027.437 * * * [misc]progress: generating rewritten candidates 1554305027.437 * * * * [misc]progress: [ 1 / 2 ] rewriting at (2) 1554305027.441 * * * * [misc]progress: [ 2 / 2 ] rewriting at (2 1) 1554305027.441 * * * [misc]progress: generating series expansions 1554305027.441 * * * * [misc]progress: [ 1 / 2 ] generating series at (2) 1554305027.441 * * * * [misc]progress: [ 2 / 2 ] generating series at (2 1) 1554305027.442 * * * [misc]progress: simplifying candidates 1554305027.442 * * * * [misc]progress: [ 1 / 4 ] simplifiying candidate #posit16 1))) (neg.p16 (sqrt.p16 x))))> 1554305027.442 * * * * [misc]progress: [ 2 / 4 ] simplifiying candidate #posit16 1))) (sqrt.p16 (+.p16 x (real->posit16 1)))) (*.p16 (sqrt.p16 x) (sqrt.p16 x))) (+.p16 (sqrt.p16 (+.p16 x (real->posit16 1))) (sqrt.p16 x))))> 1554305027.442 * * * * [misc]progress: [ 3 / 4 ] simplifiying candidate #posit16 1))) (sqrt.p16 x)))> 1554305027.442 * [enter]simplify: Simplifying (-.p16 (sqrt.p16 (+.p16 x (real->posit16 1))) (sqrt.p16 x)) 1554305027.442 * * [misc]simplify: iters left: 4 (7 enodes) 1554305027.445 * * [misc]simplify: iters left: 3 (20 enodes) 1554305027.452 * * [misc]simplify: iters left: 2 (32 enodes) 1554305027.463 * * [misc]simplify: iters left: 1 (92 enodes) 1554305027.509 * * [misc]simplify: Extracting #0: cost 1 inf + 0 1554305027.509 * * [misc]simplify: Extracting #1: cost 13 inf + 0 1554305027.509 * * [misc]simplify: Extracting #2: cost 67 inf + 0 1554305027.510 * * [misc]simplify: Extracting #3: cost 111 inf + 723 1554305027.511 * * [misc]simplify: Extracting #4: cost 94 inf + 7692 1554305027.516 * * [misc]simplify: Extracting #5: cost 25 inf + 47669 1554305027.525 * * [misc]simplify: Extracting #6: cost 0 inf + 67124 1554305027.534 * [exit]simplify: Simplified to (-.p16 (sqrt.p16 (+.p16 (real->posit16 1) x)) (sqrt.p16 x)) 1554305027.534 * [misc]simplify: Simplified (2) to (λ (x) (-.p16 (sqrt.p16 (+.p16 (real->posit16 1) x)) (sqrt.p16 x))) 1554305027.534 * * * * [misc]progress: [ 4 / 4 ] simplifiying candidate #posit16 1))) (sqrt.p16 x)))> 1554305027.534 * [enter]simplify: Simplifying (-.p16 (sqrt.p16 (+.p16 x (real->posit16 1))) (sqrt.p16 x)) 1554305027.534 * * [misc]simplify: iters left: 4 (7 enodes) 1554305027.538 * * [misc]simplify: iters left: 3 (20 enodes) 1554305027.545 * * [misc]simplify: iters left: 2 (32 enodes) 1554305027.556 * * [misc]simplify: iters left: 1 (92 enodes) 1554305027.605 * * [misc]simplify: Extracting #0: cost 1 inf + 0 1554305027.605 * * [misc]simplify: Extracting #1: cost 13 inf + 0 1554305027.605 * * [misc]simplify: Extracting #2: cost 67 inf + 0 1554305027.606 * * [misc]simplify: Extracting #3: cost 111 inf + 723 1554305027.607 * * [misc]simplify: Extracting #4: cost 94 inf + 7692 1554305027.612 * * [misc]simplify: Extracting #5: cost 25 inf + 47669 1554305027.621 * * [misc]simplify: Extracting #6: cost 0 inf + 67124 1554305027.631 * [exit]simplify: Simplified to (-.p16 (sqrt.p16 (+.p16 (real->posit16 1) x)) (sqrt.p16 x)) 1554305027.632 * [misc]simplify: Simplified (2) to (λ (x) (-.p16 (sqrt.p16 (+.p16 (real->posit16 1) x)) (sqrt.p16 x))) 1554305027.632 * * * [misc]progress: adding candidates to table 1554305027.748 * * [misc]progress: iteration 2 / 4 1554305027.748 * * * [misc]progress: picking best candidate 1554305027.765 * * * * [misc]pick: Picked #posit16 1))) (sqrt.p16 (+.p16 x (real->posit16 1)))) (*.p16 (sqrt.p16 x) (sqrt.p16 x))) (+.p16 (sqrt.p16 (+.p16 x (real->posit16 1))) (sqrt.p16 x))))> 1554305027.766 * * * [misc]progress: localizing error 1554305027.939 * * * [misc]progress: generating rewritten candidates 1554305027.939 * * * * [misc]progress: [ 1 / 4 ] rewriting at (2 1) 1554305027.944 * * * * [misc]progress: [ 2 / 4 ] rewriting at (2 1 1) 1554305027.948 * * * * [misc]progress: [ 3 / 4 ] rewriting at (2 1 2) 1554305027.961 * * * * [misc]progress: [ 4 / 4 ] rewriting at (2) 1554305027.970 * * * [misc]progress: generating series expansions 1554305027.970 * * * * [misc]progress: [ 1 / 4 ] generating series at (2 1) 1554305027.970 * * * * [misc]progress: [ 2 / 4 ] generating series at (2 1 1) 1554305027.970 * * * * [misc]progress: [ 3 / 4 ] generating series at (2 1 2) 1554305027.970 * * * * [misc]progress: [ 4 / 4 ] generating series at (2) 1554305027.970 * * * [misc]progress: simplifying candidates 1554305027.970 * * * * [misc]progress: [ 1 / 13 ] simplifiying candidate #posit16 1))) (sqrt.p16 x)) (-.p16 (sqrt.p16 (+.p16 x (real->posit16 1))) (sqrt.p16 x))) (+.p16 (sqrt.p16 (+.p16 x (real->posit16 1))) (sqrt.p16 x))))> 1554305027.971 * [enter]simplify: Simplifying (+.p16 (sqrt.p16 (+.p16 x (real->posit16 1))) (sqrt.p16 x)) 1554305027.971 * * [misc]simplify: iters left: 4 (7 enodes) 1554305027.974 * * [misc]simplify: iters left: 3 (14 enodes) 1554305027.978 * * [misc]simplify: iters left: 2 (16 enodes) 1554305027.983 * * [misc]simplify: Extracting #0: cost 1 inf + 0 1554305027.983 * * [misc]simplify: Extracting #1: cost 3 inf + 0 1554305027.983 * * [misc]simplify: Extracting #2: cost 5 inf + 0 1554305027.983 * * [misc]simplify: Extracting #3: cost 5 inf + 1 1554305027.983 * * [misc]simplify: Extracting #4: cost 5 inf + 42 1554305027.983 * * [misc]simplify: Extracting #5: cost 0 inf + 330 1554305027.983 * [exit]simplify: Simplified to (+.p16 (sqrt.p16 (+.p16 (real->posit16 1) x)) (sqrt.p16 x)) 1554305027.983 * [misc]simplify: Simplified (2 1 1) to (λ (x) (/.p16 (*.p16 (+.p16 (sqrt.p16 (+.p16 (real->posit16 1) x)) (sqrt.p16 x)) (-.p16 (sqrt.p16 (+.p16 x (real->posit16 1))) (sqrt.p16 x))) (+.p16 (sqrt.p16 (+.p16 x (real->posit16 1))) (sqrt.p16 x)))) 1554305027.984 * [enter]simplify: Simplifying (-.p16 (sqrt.p16 (+.p16 x (real->posit16 1))) (sqrt.p16 x)) 1554305027.984 * * [misc]simplify: iters left: 4 (7 enodes) 1554305027.987 * * [misc]simplify: iters left: 3 (20 enodes) 1554305027.994 * * [misc]simplify: iters left: 2 (32 enodes) 1554305028.005 * * [misc]simplify: iters left: 1 (92 enodes) 1554305028.050 * * [misc]simplify: Extracting #0: cost 1 inf + 0 1554305028.050 * * [misc]simplify: Extracting #1: cost 13 inf + 0 1554305028.050 * * [misc]simplify: Extracting #2: cost 67 inf + 0 1554305028.051 * * [misc]simplify: Extracting #3: cost 111 inf + 723 1554305028.052 * * [misc]simplify: Extracting #4: cost 94 inf + 7692 1554305028.057 * * [misc]simplify: Extracting #5: cost 25 inf + 47669 1554305028.066 * * [misc]simplify: Extracting #6: cost 0 inf + 67124 1554305028.075 * [exit]simplify: Simplified to (-.p16 (sqrt.p16 (+.p16 (real->posit16 1) x)) (sqrt.p16 x)) 1554305028.075 * [misc]simplify: Simplified (2 1 2) to (λ (x) (/.p16 (*.p16 (+.p16 (sqrt.p16 (+.p16 x (real->posit16 1))) (sqrt.p16 x)) (-.p16 (sqrt.p16 (+.p16 (real->posit16 1) x)) (sqrt.p16 x))) (+.p16 (sqrt.p16 (+.p16 x (real->posit16 1))) (sqrt.p16 x)))) 1554305028.075 * * * * [misc]progress: [ 2 / 13 ] simplifiying candidate #posit16 1))) (sqrt.p16 (+.p16 x (real->posit16 1)))) (neg.p16 (*.p16 (sqrt.p16 x) (sqrt.p16 x)))) (+.p16 (sqrt.p16 (+.p16 x (real->posit16 1))) (sqrt.p16 x))))> 1554305028.075 * * * * [misc]progress: [ 3 / 13 ] simplifiying candidate #posit16 1))) (sqrt.p16 (+.p16 x (real->posit16 1)))) (*.p16 (sqrt.p16 (+.p16 x (real->posit16 1))) (sqrt.p16 (+.p16 x (real->posit16 1))))) (*.p16 (*.p16 (sqrt.p16 x) (sqrt.p16 x)) (*.p16 (sqrt.p16 x) (sqrt.p16 x)))) (+.p16 (*.p16 (sqrt.p16 (+.p16 x (real->posit16 1))) (sqrt.p16 (+.p16 x (real->posit16 1)))) (*.p16 (sqrt.p16 x) (sqrt.p16 x)))) (+.p16 (sqrt.p16 (+.p16 x (real->posit16 1))) (sqrt.p16 x))))> 1554305028.075 * * * * [misc]progress: [ 4 / 13 ] simplifiying candidate #posit16 1)) (*.p16 (sqrt.p16 x) (sqrt.p16 x))) (+.p16 (sqrt.p16 (+.p16 x (real->posit16 1))) (sqrt.p16 x))))> 1554305028.076 * [enter]simplify: Simplifying (real->posit16 1) 1554305028.076 * * [misc]simplify: iters left: 1 (2 enodes) 1554305028.077 * * [misc]simplify: Extracting #0: cost 1 inf + 0 1554305028.077 * * [misc]simplify: Extracting #1: cost 2 inf + 0 1554305028.077 * * [misc]simplify: Extracting #2: cost 1 inf + 1 1554305028.077 * * [misc]simplify: Extracting #3: cost 0 inf + 2 1554305028.077 * [exit]simplify: Simplified to (real->posit16 1) 1554305028.077 * [misc]simplify: Simplified (2 1 1 2) to (λ (x) (/.p16 (-.p16 (+.p16 x (real->posit16 1)) (*.p16 (sqrt.p16 x) (sqrt.p16 x))) (+.p16 (sqrt.p16 (+.p16 x (real->posit16 1))) (sqrt.p16 x)))) 1554305028.078 * * * * [misc]progress: [ 5 / 13 ] simplifiying candidate #posit16 1))) (sqrt.p16 (+.p16 x (real->posit16 1)))) (*.p16 (sqrt.p16 x) (sqrt.p16 x))) (+.p16 (sqrt.p16 (+.p16 x (real->posit16 1))) (sqrt.p16 x))))> 1554305028.078 * * * * [misc]progress: [ 6 / 13 ] simplifiying candidate #posit16 1))) (sqrt.p16 (+.p16 x (real->posit16 1)))) x) (+.p16 (sqrt.p16 (+.p16 x (real->posit16 1))) (sqrt.p16 x))))> 1554305028.078 * * * * [misc]progress: [ 7 / 13 ] simplifiying candidate #posit16 1))) (sqrt.p16 (+.p16 x (real->posit16 1)))) (*.p16 (sqrt.p16 x) (sqrt.p16 x))) (+.p16 (sqrt.p16 (+.p16 x (real->posit16 1))) (sqrt.p16 x))))> 1554305028.078 * * * * [misc]progress: [ 8 / 13 ] simplifiying candidate #posit16 1))) (sqrt.p16 x)) (/.p16 (+.p16 (sqrt.p16 (+.p16 x (real->posit16 1))) (sqrt.p16 x)) (-.p16 (sqrt.p16 (+.p16 x (real->posit16 1))) (sqrt.p16 x)))))> 1554305028.078 * [enter]simplify: Simplifying (+.p16 (sqrt.p16 (+.p16 x (real->posit16 1))) (sqrt.p16 x)) 1554305028.078 * * [misc]simplify: iters left: 4 (7 enodes) 1554305028.081 * * [misc]simplify: iters left: 3 (14 enodes) 1554305028.085 * * [misc]simplify: iters left: 2 (16 enodes) 1554305028.090 * * [misc]simplify: Extracting #0: cost 1 inf + 0 1554305028.090 * * [misc]simplify: Extracting #1: cost 3 inf + 0 1554305028.090 * * [misc]simplify: Extracting #2: cost 5 inf + 0 1554305028.090 * * [misc]simplify: Extracting #3: cost 5 inf + 1 1554305028.090 * * [misc]simplify: Extracting #4: cost 5 inf + 42 1554305028.090 * * [misc]simplify: Extracting #5: cost 0 inf + 330 1554305028.091 * [exit]simplify: Simplified to (+.p16 (sqrt.p16 (+.p16 (real->posit16 1) x)) (sqrt.p16 x)) 1554305028.091 * [misc]simplify: Simplified (2 1) to (λ (x) (/.p16 (+.p16 (sqrt.p16 (+.p16 (real->posit16 1) x)) (sqrt.p16 x)) (/.p16 (+.p16 (sqrt.p16 (+.p16 x (real->posit16 1))) (sqrt.p16 x)) (-.p16 (sqrt.p16 (+.p16 x (real->posit16 1))) (sqrt.p16 x))))) 1554305028.091 * * * * [misc]progress: [ 9 / 13 ] simplifiying candidate #posit16 1))) (sqrt.p16 (+.p16 x (real->posit16 1)))) (*.p16 (sqrt.p16 (+.p16 x (real->posit16 1))) (sqrt.p16 (+.p16 x (real->posit16 1))))) (*.p16 (*.p16 (sqrt.p16 x) (sqrt.p16 x)) (*.p16 (sqrt.p16 x) (sqrt.p16 x)))) (*.p16 (+.p16 (sqrt.p16 (+.p16 x (real->posit16 1))) (sqrt.p16 x)) (+.p16 (*.p16 (sqrt.p16 (+.p16 x (real->posit16 1))) (sqrt.p16 (+.p16 x (real->posit16 1)))) (*.p16 (sqrt.p16 x) (sqrt.p16 x))))))> 1554305028.091 * [enter]simplify: Simplifying (-.p16 (*.p16 (*.p16 (sqrt.p16 (+.p16 x (real->posit16 1))) (sqrt.p16 (+.p16 x (real->posit16 1)))) (*.p16 (sqrt.p16 (+.p16 x (real->posit16 1))) (sqrt.p16 (+.p16 x (real->posit16 1))))) (*.p16 (*.p16 (sqrt.p16 x) (sqrt.p16 x)) (*.p16 (sqrt.p16 x) (sqrt.p16 x)))) 1554305028.091 * * [misc]simplify: iters left: 6 (11 enodes) 1554305028.097 * * [misc]simplify: iters left: 5 (36 enodes) 1554305028.114 * * [misc]simplify: iters left: 4 (113 enodes) 1554305028.186 * * [misc]simplify: Extracting #0: cost 1 inf + 0 1554305028.186 * * [misc]simplify: Extracting #1: cost 47 inf + 0 1554305028.187 * * [misc]simplify: Extracting #2: cost 86 inf + 0 1554305028.188 * * [misc]simplify: Extracting #3: cost 135 inf + 444 1554305028.189 * * [misc]simplify: Extracting #4: cost 135 inf + 19159 1554305028.196 * * [misc]simplify: Extracting #5: cost 41 inf + 89813 1554305028.208 * * [misc]simplify: Extracting #6: cost 4 inf + 126851 1554305028.222 * * [misc]simplify: Extracting #7: cost 0 inf + 133619 1554305028.235 * [exit]simplify: Simplified to (*.p16 (+.p16 (real->posit16 0.0) (real->posit16 1)) (+.p16 (+.p16 x x) (real->posit16 1))) 1554305028.235 * [misc]simplify: Simplified (2 1) to (λ (x) (/.p16 (*.p16 (+.p16 (real->posit16 0.0) (real->posit16 1)) (+.p16 (+.p16 x x) (real->posit16 1))) (*.p16 (+.p16 (sqrt.p16 (+.p16 x (real->posit16 1))) (sqrt.p16 x)) (+.p16 (*.p16 (sqrt.p16 (+.p16 x (real->posit16 1))) (sqrt.p16 (+.p16 x (real->posit16 1)))) (*.p16 (sqrt.p16 x) (sqrt.p16 x)))))) 1554305028.235 * * * * [misc]progress: [ 10 / 13 ] simplifiying candidate #posit16 1))) (sqrt.p16 (+.p16 x (real->posit16 1)))) (*.p16 (sqrt.p16 x) (sqrt.p16 x))) (+.p16 (sqrt.p16 (+.p16 x (real->posit16 1))) (sqrt.p16 x))))> 1554305028.236 * * * * [misc]progress: [ 11 / 13 ] simplifiying candidate #posit16 1))) (sqrt.p16 (+.p16 x (real->posit16 1)))) (*.p16 (sqrt.p16 x) (sqrt.p16 x))) (+.p16 (sqrt.p16 (+.p16 x (real->posit16 1))) (sqrt.p16 x))))> 1554305028.236 * * * * [misc]progress: [ 12 / 13 ] simplifiying candidate #posit16 1))) (sqrt.p16 (+.p16 x (real->posit16 1)))) (*.p16 (sqrt.p16 x) (sqrt.p16 x))) (+.p16 (sqrt.p16 (+.p16 x (real->posit16 1))) (sqrt.p16 x))))> 1554305028.236 * * * * [misc]progress: [ 13 / 13 ] simplifiying candidate #posit16 1))) (sqrt.p16 (+.p16 x (real->posit16 1)))) (*.p16 (sqrt.p16 x) (sqrt.p16 x))) (+.p16 (sqrt.p16 (+.p16 x (real->posit16 1))) (sqrt.p16 x))))> 1554305028.236 * * * [misc]progress: adding candidates to table 1554305028.703 * * [misc]progress: iteration 3 / 4 1554305028.703 * * * [misc]progress: picking best candidate 1554305028.790 * * * * [misc]pick: Picked #posit16 0.0) (real->posit16 1)) (+.p16 (+.p16 x x) (real->posit16 1))) (*.p16 (+.p16 (sqrt.p16 (+.p16 x (real->posit16 1))) (sqrt.p16 x)) (+.p16 (*.p16 (sqrt.p16 (+.p16 x (real->posit16 1))) (sqrt.p16 (+.p16 x (real->posit16 1)))) (*.p16 (sqrt.p16 x) (sqrt.p16 x))))))> 1554305028.790 * * * [misc]progress: localizing error 1554305029.083 * * * [misc]progress: generating rewritten candidates 1554305029.083 * * * * [misc]progress: [ 1 / 4 ] rewriting at (2) 1554305029.092 * * * * [misc]progress: [ 2 / 4 ] rewriting at (2 2 2 1) 1554305029.097 * * * * [misc]progress: [ 3 / 4 ] rewriting at (2 2 2 2) 1554305029.101 * * * * [misc]progress: [ 4 / 4 ] rewriting at (2 2) 1554305029.109 * * * [misc]progress: generating series expansions 1554305029.109 * * * * [misc]progress: [ 1 / 4 ] generating series at (2) 1554305029.109 * * * * [misc]progress: [ 2 / 4 ] generating series at (2 2 2 1) 1554305029.109 * * * * [misc]progress: [ 3 / 4 ] generating series at (2 2 2 2) 1554305029.109 * * * * [misc]progress: [ 4 / 4 ] generating series at (2 2) 1554305029.109 * * * [misc]progress: simplifying candidates 1554305029.109 * * * * [misc]progress: [ 1 / 14 ] simplifiying candidate #posit16 0.0) (real->posit16 1)) (+.p16 (+.p16 x x) (real->posit16 1))) (+.p16 (sqrt.p16 (+.p16 x (real->posit16 1))) (sqrt.p16 x))) (+.p16 (*.p16 (sqrt.p16 (+.p16 x (real->posit16 1))) (sqrt.p16 (+.p16 x (real->posit16 1)))) (*.p16 (sqrt.p16 x) (sqrt.p16 x)))))> 1554305029.110 * [enter]simplify: Simplifying (+.p16 (*.p16 (sqrt.p16 (+.p16 x (real->posit16 1))) (sqrt.p16 (+.p16 x (real->posit16 1)))) (*.p16 (sqrt.p16 x) (sqrt.p16 x))) 1554305029.110 * * [misc]simplify: iters left: 5 (9 enodes) 1554305029.114 * * [misc]simplify: iters left: 4 (16 enodes) 1554305029.119 * * [misc]simplify: iters left: 3 (20 enodes) 1554305029.125 * * [misc]simplify: iters left: 2 (21 enodes) 1554305029.131 * * [misc]simplify: Extracting #0: cost 1 inf + 0 1554305029.131 * * [misc]simplify: Extracting #1: cost 5 inf + 0 1554305029.131 * * [misc]simplify: Extracting #2: cost 5 inf + 42 1554305029.131 * * [misc]simplify: Extracting #3: cost 4 inf + 43 1554305029.131 * * [misc]simplify: Extracting #4: cost 1 inf + 168 1554305029.132 * * [misc]simplify: Extracting #5: cost 0 inf + 250 1554305029.132 * [exit]simplify: Simplified to (+.p16 x (+.p16 (real->posit16 1) x)) 1554305029.132 * [misc]simplify: Simplified (2 2) to (λ (x) (/.p16 (/.p16 (*.p16 (+.p16 (real->posit16 0.0) (real->posit16 1)) (+.p16 (+.p16 x x) (real->posit16 1))) (+.p16 (sqrt.p16 (+.p16 x (real->posit16 1))) (sqrt.p16 x))) (+.p16 x (+.p16 (real->posit16 1) x)))) 1554305029.132 * * * * [misc]progress: [ 2 / 14 ] simplifiying candidate #posit16 0.0) (real->posit16 1)) (/.p16 (*.p16 (+.p16 (sqrt.p16 (+.p16 x (real->posit16 1))) (sqrt.p16 x)) (+.p16 (*.p16 (sqrt.p16 (+.p16 x (real->posit16 1))) (sqrt.p16 (+.p16 x (real->posit16 1)))) (*.p16 (sqrt.p16 x) (sqrt.p16 x)))) (+.p16 (+.p16 x x) (real->posit16 1)))))> 1554305029.132 * [enter]simplify: Simplifying (+.p16 (real->posit16 0.0) (real->posit16 1)) 1554305029.132 * * [misc]simplify: iters left: 2 (5 enodes) 1554305029.134 * * [misc]simplify: iters left: 1 (10 enodes) 1554305029.136 * * [misc]simplify: Extracting #0: cost 1 inf + 0 1554305029.137 * * [misc]simplify: Extracting #1: cost 4 inf + 0 1554305029.137 * * [misc]simplify: Extracting #2: cost 3 inf + 2 1554305029.137 * * [misc]simplify: Extracting #3: cost 2 inf + 3 1554305029.137 * * [misc]simplify: Extracting #4: cost 0 inf + 45 1554305029.137 * [exit]simplify: Simplified to (real->posit16 1) 1554305029.137 * [misc]simplify: Simplified (2 1) to (λ (x) (/.p16 (real->posit16 1) (/.p16 (*.p16 (+.p16 (sqrt.p16 (+.p16 x (real->posit16 1))) (sqrt.p16 x)) (+.p16 (*.p16 (sqrt.p16 (+.p16 x (real->posit16 1))) (sqrt.p16 (+.p16 x (real->posit16 1)))) (*.p16 (sqrt.p16 x) (sqrt.p16 x)))) (+.p16 (+.p16 x x) (real->posit16 1))))) 1554305029.137 * * * * [misc]progress: [ 3 / 14 ] simplifiying candidate #posit16 0.0) (real->posit16 1)) (+.p16 (sqrt.p16 (+.p16 x (real->posit16 1))) (sqrt.p16 x))) (/.p16 (+.p16 (+.p16 x x) (real->posit16 1)) (+.p16 (*.p16 (sqrt.p16 (+.p16 x (real->posit16 1))) (sqrt.p16 (+.p16 x (real->posit16 1)))) (*.p16 (sqrt.p16 x) (sqrt.p16 x))))))> 1554305029.137 * [enter]simplify: Simplifying (/.p16 (+.p16 (real->posit16 0.0) (real->posit16 1)) (+.p16 (sqrt.p16 (+.p16 x (real->posit16 1))) (sqrt.p16 x))) 1554305029.137 * * [misc]simplify: iters left: 5 (11 enodes) 1554305029.140 * * [misc]simplify: iters left: 4 (20 enodes) 1554305029.144 * * [misc]simplify: iters left: 3 (28 enodes) 1554305029.150 * * [misc]simplify: iters left: 2 (39 enodes) 1554305029.158 * * [misc]simplify: iters left: 1 (47 enodes) 1554305029.171 * * [misc]simplify: Extracting #0: cost 1 inf + 0 1554305029.171 * * [misc]simplify: Extracting #1: cost 3 inf + 0 1554305029.171 * * [misc]simplify: Extracting #2: cost 7 inf + 0 1554305029.171 * * [misc]simplify: Extracting #3: cost 8 inf + 2 1554305029.171 * * [misc]simplify: Extracting #4: cost 12 inf + 4 1554305029.171 * * [misc]simplify: Extracting #5: cost 4 inf + 458 1554305029.172 * * [misc]simplify: Extracting #6: cost 0 inf + 1186 1554305029.172 * [exit]simplify: Simplified to (/.p16 (real->posit16 1) (+.p16 (sqrt.p16 (+.p16 (real->posit16 1) x)) (sqrt.p16 x))) 1554305029.172 * [misc]simplify: Simplified (2 1) to (λ (x) (*.p16 (/.p16 (real->posit16 1) (+.p16 (sqrt.p16 (+.p16 (real->posit16 1) x)) (sqrt.p16 x))) (/.p16 (+.p16 (+.p16 x x) (real->posit16 1)) (+.p16 (*.p16 (sqrt.p16 (+.p16 x (real->posit16 1))) (sqrt.p16 (+.p16 x (real->posit16 1)))) (*.p16 (sqrt.p16 x) (sqrt.p16 x)))))) 1554305029.173 * [enter]simplify: Simplifying (/.p16 (+.p16 (+.p16 x x) (real->posit16 1)) (+.p16 (*.p16 (sqrt.p16 (+.p16 x (real->posit16 1))) (sqrt.p16 (+.p16 x (real->posit16 1)))) (*.p16 (sqrt.p16 x) (sqrt.p16 x)))) 1554305029.173 * * [misc]simplify: iters left: 6 (12 enodes) 1554305029.179 * * [misc]simplify: iters left: 5 (21 enodes) 1554305029.186 * * [misc]simplify: iters left: 4 (23 enodes) 1554305029.193 * * [misc]simplify: Extracting #0: cost 1 inf + 0 1554305029.193 * * [misc]simplify: Extracting #1: cost 2 inf + 0 1554305029.193 * * [misc]simplify: Extracting #2: cost 6 inf + 0 1554305029.193 * * [misc]simplify: Extracting #3: cost 7 inf + 1 1554305029.193 * * [misc]simplify: Extracting #4: cost 1 inf + 690 1554305029.193 * * [misc]simplify: Extracting #5: cost 0 inf + 772 1554305029.194 * [exit]simplify: Simplified to (/.p16 (+.p16 (real->posit16 1) (+.p16 x x)) (+.p16 (real->posit16 1) (+.p16 x x))) 1554305029.194 * [misc]simplify: Simplified (2 2) to (λ (x) (*.p16 (/.p16 (+.p16 (real->posit16 0.0) (real->posit16 1)) (+.p16 (sqrt.p16 (+.p16 x (real->posit16 1))) (sqrt.p16 x))) (/.p16 (+.p16 (real->posit16 1) (+.p16 x x)) (+.p16 (real->posit16 1) (+.p16 x x))))) 1554305029.194 * * * * [misc]progress: [ 4 / 14 ] simplifiying candidate #posit16 0.0) (real->posit16 1)) (+.p16 (+.p16 x x) (real->posit16 1))) (*.p16 (+.p16 (sqrt.p16 (+.p16 x (real->posit16 1))) (sqrt.p16 x)) (+.p16 (+.p16 x (real->posit16 1)) (*.p16 (sqrt.p16 x) (sqrt.p16 x))))))> 1554305029.194 * [enter]simplify: Simplifying (real->posit16 1) 1554305029.194 * * [misc]simplify: iters left: 1 (2 enodes) 1554305029.196 * * [misc]simplify: Extracting #0: cost 1 inf + 0 1554305029.196 * * [misc]simplify: Extracting #1: cost 2 inf + 0 1554305029.196 * * [misc]simplify: Extracting #2: cost 1 inf + 1 1554305029.196 * * [misc]simplify: Extracting #3: cost 0 inf + 2 1554305029.196 * [exit]simplify: Simplified to (real->posit16 1) 1554305029.196 * [misc]simplify: Simplified (2 2 2 1 2) to (λ (x) (/.p16 (*.p16 (+.p16 (real->posit16 0.0) (real->posit16 1)) (+.p16 (+.p16 x x) (real->posit16 1))) (*.p16 (+.p16 (sqrt.p16 (+.p16 x (real->posit16 1))) (sqrt.p16 x)) (+.p16 (+.p16 x (real->posit16 1)) (*.p16 (sqrt.p16 x) (sqrt.p16 x)))))) 1554305029.196 * * * * [misc]progress: [ 5 / 14 ] simplifiying candidate #posit16 0.0) (real->posit16 1)) (+.p16 (+.p16 x x) (real->posit16 1))) (*.p16 (+.p16 (sqrt.p16 (+.p16 x (real->posit16 1))) (sqrt.p16 x)) (+.p16 (*.p16 (sqrt.p16 (+.p16 x (real->posit16 1))) (sqrt.p16 (+.p16 x (real->posit16 1)))) (*.p16 (sqrt.p16 x) (sqrt.p16 x))))))> 1554305029.196 * * * * [misc]progress: [ 6 / 14 ] simplifiying candidate #posit16 0.0) (real->posit16 1)) (+.p16 (+.p16 x x) (real->posit16 1))) (*.p16 (+.p16 (sqrt.p16 (+.p16 x (real->posit16 1))) (sqrt.p16 x)) (+.p16 (*.p16 (sqrt.p16 (+.p16 x (real->posit16 1))) (sqrt.p16 (+.p16 x (real->posit16 1)))) x))))> 1554305029.196 * * * * [misc]progress: [ 7 / 14 ] simplifiying candidate #posit16 0.0) (real->posit16 1)) (+.p16 (+.p16 x x) (real->posit16 1))) (*.p16 (+.p16 (sqrt.p16 (+.p16 x (real->posit16 1))) (sqrt.p16 x)) (+.p16 (*.p16 (sqrt.p16 (+.p16 x (real->posit16 1))) (sqrt.p16 (+.p16 x (real->posit16 1)))) (*.p16 (sqrt.p16 x) (sqrt.p16 x))))))> 1554305029.196 * * * * [misc]progress: [ 8 / 14 ] simplifiying candidate #posit16 0.0) (real->posit16 1)) (+.p16 (+.p16 x x) (real->posit16 1))) (+.p16 (*.p16 (+.p16 (sqrt.p16 (+.p16 x (real->posit16 1))) (sqrt.p16 x)) (*.p16 (sqrt.p16 (+.p16 x (real->posit16 1))) (sqrt.p16 (+.p16 x (real->posit16 1))))) (*.p16 (+.p16 (sqrt.p16 (+.p16 x (real->posit16 1))) (sqrt.p16 x)) (*.p16 (sqrt.p16 x) (sqrt.p16 x))))))> 1554305029.197 * [enter]simplify: Simplifying (*.p16 (+.p16 (sqrt.p16 (+.p16 x (real->posit16 1))) (sqrt.p16 x)) (*.p16 (sqrt.p16 x) (sqrt.p16 x))) 1554305029.197 * * [misc]simplify: iters left: 5 (9 enodes) 1554305029.201 * * [misc]simplify: iters left: 4 (19 enodes) 1554305029.208 * * [misc]simplify: iters left: 3 (30 enodes) 1554305029.217 * * [misc]simplify: iters left: 2 (37 enodes) 1554305029.232 * * [misc]simplify: iters left: 1 (49 enodes) 1554305029.244 * * [misc]simplify: Extracting #0: cost 1 inf + 0 1554305029.244 * * [misc]simplify: Extracting #1: cost 7 inf + 0 1554305029.244 * * [misc]simplify: Extracting #2: cost 8 inf + 1 1554305029.244 * * [misc]simplify: Extracting #3: cost 8 inf + 42 1554305029.245 * * [misc]simplify: Extracting #4: cost 8 inf + 403 1554305029.245 * * [misc]simplify: Extracting #5: cost 9 inf + 403 1554305029.245 * * [misc]simplify: Extracting #6: cost 8 inf + 404 1554305029.245 * * [misc]simplify: Extracting #7: cost 4 inf + 931 1554305029.246 * * [misc]simplify: Extracting #8: cost 0 inf + 2499 1554305029.246 * [exit]simplify: Simplified to (*.p16 (+.p16 (sqrt.p16 (+.p16 (real->posit16 1) x)) (sqrt.p16 x)) x) 1554305029.246 * [misc]simplify: Simplified (2 2 2) to (λ (x) (/.p16 (*.p16 (+.p16 (real->posit16 0.0) (real->posit16 1)) (+.p16 (+.p16 x x) (real->posit16 1))) (+.p16 (*.p16 (+.p16 (sqrt.p16 (+.p16 x (real->posit16 1))) (sqrt.p16 x)) (*.p16 (sqrt.p16 (+.p16 x (real->posit16 1))) (sqrt.p16 (+.p16 x (real->posit16 1))))) (*.p16 (+.p16 (sqrt.p16 (+.p16 (real->posit16 1) x)) (sqrt.p16 x)) x)))) 1554305029.247 * * * * [misc]progress: [ 9 / 14 ] simplifiying candidate #posit16 0.0) (real->posit16 1)) (+.p16 (+.p16 x x) (real->posit16 1))) (+.p16 (*.p16 (*.p16 (sqrt.p16 (+.p16 x (real->posit16 1))) (sqrt.p16 (+.p16 x (real->posit16 1)))) (+.p16 (sqrt.p16 (+.p16 x (real->posit16 1))) (sqrt.p16 x))) (*.p16 (*.p16 (sqrt.p16 x) (sqrt.p16 x)) (+.p16 (sqrt.p16 (+.p16 x (real->posit16 1))) (sqrt.p16 x))))))> 1554305029.247 * [enter]simplify: Simplifying (*.p16 (*.p16 (sqrt.p16 x) (sqrt.p16 x)) (+.p16 (sqrt.p16 (+.p16 x (real->posit16 1))) (sqrt.p16 x))) 1554305029.247 * * [misc]simplify: iters left: 5 (9 enodes) 1554305029.252 * * [misc]simplify: iters left: 4 (25 enodes) 1554305029.261 * * [misc]simplify: iters left: 3 (55 enodes) 1554305029.279 * * [misc]simplify: iters left: 2 (74 enodes) 1554305029.295 * * [misc]simplify: iters left: 1 (94 enodes) 1554305029.304 * * [misc]simplify: Extracting #0: cost 1 inf + 0 1554305029.304 * * [misc]simplify: Extracting #1: cost 10 inf + 0 1554305029.304 * * [misc]simplify: Extracting #2: cost 11 inf + 1 1554305029.304 * * [misc]simplify: Extracting #3: cost 9 inf + 764 1554305029.304 * * [misc]simplify: Extracting #4: cost 10 inf + 764 1554305029.304 * * [misc]simplify: Extracting #5: cost 11 inf + 764 1554305029.304 * * [misc]simplify: Extracting #6: cost 10 inf + 765 1554305029.304 * * [misc]simplify: Extracting #7: cost 8 inf + 808 1554305029.305 * * [misc]simplify: Extracting #8: cost 3 inf + 2658 1554305029.305 * * [misc]simplify: Extracting #9: cost 0 inf + 3744 1554305029.306 * [exit]simplify: Simplified to (*.p16 (+.p16 (sqrt.p16 x) (sqrt.p16 (+.p16 x (real->posit16 1)))) x) 1554305029.306 * [misc]simplify: Simplified (2 2 2) to (λ (x) (/.p16 (*.p16 (+.p16 (real->posit16 0.0) (real->posit16 1)) (+.p16 (+.p16 x x) (real->posit16 1))) (+.p16 (*.p16 (*.p16 (sqrt.p16 (+.p16 x (real->posit16 1))) (sqrt.p16 (+.p16 x (real->posit16 1)))) (+.p16 (sqrt.p16 (+.p16 x (real->posit16 1))) (sqrt.p16 x))) (*.p16 (+.p16 (sqrt.p16 x) (sqrt.p16 (+.p16 x (real->posit16 1)))) x)))) 1554305029.306 * * * * [misc]progress: [ 10 / 14 ] simplifiying candidate #posit16 0.0) (real->posit16 1)) (+.p16 (+.p16 x x) (real->posit16 1))) (*.p16 (+.p16 (*.p16 (sqrt.p16 (+.p16 x (real->posit16 1))) (sqrt.p16 (+.p16 x (real->posit16 1)))) (*.p16 (sqrt.p16 x) (sqrt.p16 x))) (+.p16 (sqrt.p16 (+.p16 x (real->posit16 1))) (sqrt.p16 x)))))> 1554305029.306 * * * * [misc]progress: [ 11 / 14 ] simplifiying candidate #posit16 0.0) (real->posit16 1)) (+.p16 (+.p16 x x) (real->posit16 1))) (*.p16 (+.p16 (sqrt.p16 (+.p16 x (real->posit16 1))) (sqrt.p16 x)) (+.p16 (*.p16 (sqrt.p16 (+.p16 x (real->posit16 1))) (sqrt.p16 (+.p16 x (real->posit16 1)))) (*.p16 (sqrt.p16 x) (sqrt.p16 x))))))> 1554305029.306 * [enter]simplify: Simplifying (/.p16 (*.p16 (+.p16 (real->posit16 0.0) (real->posit16 1)) (+.p16 (+.p16 x x) (real->posit16 1))) (*.p16 (+.p16 (sqrt.p16 (+.p16 x (real->posit16 1))) (sqrt.p16 x)) (+.p16 (*.p16 (sqrt.p16 (+.p16 x (real->posit16 1))) (sqrt.p16 (+.p16 x (real->posit16 1)))) (*.p16 (sqrt.p16 x) (sqrt.p16 x))))) 1554305029.306 * * [misc]simplify: iters left: 6 (18 enodes) 1554305029.311 * * [misc]simplify: iters left: 5 (51 enodes) 1554305029.324 * * [misc]simplify: iters left: 4 (194 enodes) 1554305029.504 * * [misc]simplify: Extracting #0: cost 1 inf + 0 1554305029.504 * * [misc]simplify: Extracting #1: cost 32 inf + 0 1554305029.505 * * [misc]simplify: Extracting #2: cost 117 inf + 0 1554305029.506 * * [misc]simplify: Extracting #3: cost 292 inf + 5 1554305029.508 * * [misc]simplify: Extracting #4: cost 270 inf + 5836 1554305029.516 * * [misc]simplify: Extracting #5: cost 65 inf + 70892 1554305029.537 * * [misc]simplify: Extracting #6: cost 8 inf + 112697 1554305029.556 * * [misc]simplify: Extracting #7: cost 0 inf + 121075 1554305029.574 * [exit]simplify: Simplified to (*.p16 (/.p16 (real->posit16 1) (+.p16 (sqrt.p16 (+.p16 (real->posit16 1) x)) (sqrt.p16 x))) (real->posit16 1.0)) 1554305029.574 * [misc]simplify: Simplified (2) to (λ (x) (*.p16 (/.p16 (real->posit16 1) (+.p16 (sqrt.p16 (+.p16 (real->posit16 1) x)) (sqrt.p16 x))) (real->posit16 1.0))) 1554305029.574 * * * * [misc]progress: [ 12 / 14 ] simplifiying candidate #posit16 0.0) (real->posit16 1)) (+.p16 (+.p16 x x) (real->posit16 1))) (*.p16 (+.p16 (sqrt.p16 (+.p16 x (real->posit16 1))) (sqrt.p16 x)) (+.p16 (*.p16 (sqrt.p16 (+.p16 x (real->posit16 1))) (sqrt.p16 (+.p16 x (real->posit16 1)))) (*.p16 (sqrt.p16 x) (sqrt.p16 x))))))> 1554305029.575 * [enter]simplify: Simplifying (/.p16 (*.p16 (+.p16 (real->posit16 0.0) (real->posit16 1)) (+.p16 (+.p16 x x) (real->posit16 1))) (*.p16 (+.p16 (sqrt.p16 (+.p16 x (real->posit16 1))) (sqrt.p16 x)) (+.p16 (*.p16 (sqrt.p16 (+.p16 x (real->posit16 1))) (sqrt.p16 (+.p16 x (real->posit16 1)))) (*.p16 (sqrt.p16 x) (sqrt.p16 x))))) 1554305029.575 * * [misc]simplify: iters left: 6 (18 enodes) 1554305029.581 * * [misc]simplify: iters left: 5 (51 enodes) 1554305029.594 * * [misc]simplify: iters left: 4 (194 enodes) 1554305029.798 * * [misc]simplify: Extracting #0: cost 1 inf + 0 1554305029.798 * * [misc]simplify: Extracting #1: cost 32 inf + 0 1554305029.799 * * [misc]simplify: Extracting #2: cost 117 inf + 0 1554305029.801 * * [misc]simplify: Extracting #3: cost 292 inf + 5 1554305029.803 * * [misc]simplify: Extracting #4: cost 270 inf + 5836 1554305029.813 * * [misc]simplify: Extracting #5: cost 65 inf + 70892 1554305029.830 * * [misc]simplify: Extracting #6: cost 8 inf + 112697 1554305029.849 * * [misc]simplify: Extracting #7: cost 0 inf + 121075 1554305029.867 * [exit]simplify: Simplified to (*.p16 (/.p16 (real->posit16 1) (+.p16 (sqrt.p16 (+.p16 (real->posit16 1) x)) (sqrt.p16 x))) (real->posit16 1.0)) 1554305029.867 * [misc]simplify: Simplified (2) to (λ (x) (*.p16 (/.p16 (real->posit16 1) (+.p16 (sqrt.p16 (+.p16 (real->posit16 1) x)) (sqrt.p16 x))) (real->posit16 1.0))) 1554305029.868 * * * * [misc]progress: [ 13 / 14 ] simplifiying candidate #posit16 0.0) (real->posit16 1)) (+.p16 (+.p16 x x) (real->posit16 1))) (*.p16 (+.p16 (sqrt.p16 (+.p16 x (real->posit16 1))) (sqrt.p16 x)) (+.p16 (*.p16 (sqrt.p16 (+.p16 x (real->posit16 1))) (sqrt.p16 (+.p16 x (real->posit16 1)))) (*.p16 (sqrt.p16 x) (sqrt.p16 x))))))> 1554305029.868 * [enter]simplify: Simplifying (/.p16 (*.p16 (+.p16 (real->posit16 0.0) (real->posit16 1)) (+.p16 (+.p16 x x) (real->posit16 1))) (*.p16 (+.p16 (sqrt.p16 (+.p16 x (real->posit16 1))) (sqrt.p16 x)) (+.p16 (*.p16 (sqrt.p16 (+.p16 x (real->posit16 1))) (sqrt.p16 (+.p16 x (real->posit16 1)))) (*.p16 (sqrt.p16 x) (sqrt.p16 x))))) 1554305029.868 * * [misc]simplify: iters left: 6 (18 enodes) 1554305029.881 * * [misc]simplify: iters left: 5 (51 enodes) 1554305029.905 * * [misc]simplify: iters left: 4 (194 enodes) 1554305030.130 * * [misc]simplify: Extracting #0: cost 1 inf + 0 1554305030.130 * * [misc]simplify: Extracting #1: cost 32 inf + 0 1554305030.131 * * [misc]simplify: Extracting #2: cost 117 inf + 0 1554305030.132 * * [misc]simplify: Extracting #3: cost 292 inf + 5 1554305030.135 * * [misc]simplify: Extracting #4: cost 270 inf + 5836 1554305030.143 * * [misc]simplify: Extracting #5: cost 65 inf + 70892 1554305030.159 * * [misc]simplify: Extracting #6: cost 8 inf + 112697 1554305030.177 * * [misc]simplify: Extracting #7: cost 0 inf + 121075 1554305030.197 * [exit]simplify: Simplified to (*.p16 (/.p16 (real->posit16 1) (+.p16 (sqrt.p16 (+.p16 (real->posit16 1) x)) (sqrt.p16 x))) (real->posit16 1.0)) 1554305030.197 * [misc]simplify: Simplified (2) to (λ (x) (*.p16 (/.p16 (real->posit16 1) (+.p16 (sqrt.p16 (+.p16 (real->posit16 1) x)) (sqrt.p16 x))) (real->posit16 1.0))) 1554305030.197 * * * * [misc]progress: [ 14 / 14 ] simplifiying candidate #posit16 0.0) (real->posit16 1)) (+.p16 (+.p16 x x) (real->posit16 1))) (*.p16 (+.p16 (sqrt.p16 (+.p16 x (real->posit16 1))) (sqrt.p16 x)) (+.p16 (*.p16 (sqrt.p16 (+.p16 x (real->posit16 1))) (sqrt.p16 (+.p16 x (real->posit16 1)))) (*.p16 (sqrt.p16 x) (sqrt.p16 x))))))> 1554305030.197 * [enter]simplify: Simplifying (/.p16 (*.p16 (+.p16 (real->posit16 0.0) (real->posit16 1)) (+.p16 (+.p16 x x) (real->posit16 1))) (*.p16 (+.p16 (sqrt.p16 (+.p16 x (real->posit16 1))) (sqrt.p16 x)) (+.p16 (*.p16 (sqrt.p16 (+.p16 x (real->posit16 1))) (sqrt.p16 (+.p16 x (real->posit16 1)))) (*.p16 (sqrt.p16 x) (sqrt.p16 x))))) 1554305030.197 * * [misc]simplify: iters left: 6 (18 enodes) 1554305030.207 * * [misc]simplify: iters left: 5 (51 enodes) 1554305030.232 * * [misc]simplify: iters left: 4 (194 enodes) 1554305030.379 * * [misc]simplify: Extracting #0: cost 1 inf + 0 1554305030.379 * * [misc]simplify: Extracting #1: cost 32 inf + 0 1554305030.380 * * [misc]simplify: Extracting #2: cost 117 inf + 0 1554305030.380 * * [misc]simplify: Extracting #3: cost 292 inf + 5 1554305030.381 * * [misc]simplify: Extracting #4: cost 270 inf + 5836 1554305030.385 * * [misc]simplify: Extracting #5: cost 65 inf + 70892 1554305030.394 * * [misc]simplify: Extracting #6: cost 8 inf + 112697 1554305030.414 * * [misc]simplify: Extracting #7: cost 0 inf + 121075 1554305030.433 * [exit]simplify: Simplified to (*.p16 (/.p16 (real->posit16 1) (+.p16 (sqrt.p16 (+.p16 (real->posit16 1) x)) (sqrt.p16 x))) (real->posit16 1.0)) 1554305030.433 * [misc]simplify: Simplified (2) to (λ (x) (*.p16 (/.p16 (real->posit16 1) (+.p16 (sqrt.p16 (+.p16 (real->posit16 1) x)) (sqrt.p16 x))) (real->posit16 1.0))) 1554305030.433 * * * [misc]progress: adding candidates to table 1554305031.052 * * [misc]progress: iteration 4 / 4 1554305031.052 * * * [misc]progress: picking best candidate 1554305031.141 * * * * [misc]pick: Picked #posit16 1) (+.p16 (sqrt.p16 (+.p16 (real->posit16 1) x)) (sqrt.p16 x))) (real->posit16 1.0)))> 1554305031.141 * * * [misc]progress: localizing error 1554305031.350 * * * [misc]progress: generating rewritten candidates 1554305031.350 * * * * [misc]progress: [ 1 / 3 ] rewriting at (2 1) 1554305031.354 * * * * [misc]progress: [ 2 / 3 ] rewriting at (2 1 2) 1554305031.359 * * * * [misc]progress: [ 3 / 3 ] rewriting at (2 1 2 1) 1554305031.360 * * * [misc]progress: generating series expansions 1554305031.360 * * * * [misc]progress: [ 1 / 3 ] generating series at (2 1) 1554305031.360 * * * * [misc]progress: [ 2 / 3 ] generating series at (2 1 2) 1554305031.360 * * * * [misc]progress: [ 3 / 3 ] generating series at (2 1 2 1) 1554305031.360 * * * [misc]progress: simplifying candidates 1554305031.360 * * * * [misc]progress: [ 1 / 4 ] simplifiying candidate #posit16 1) (+.p16 (sqrt.p16 x) (sqrt.p16 (+.p16 (real->posit16 1) x)))) (real->posit16 1.0)))> 1554305031.360 * * * * [misc]progress: [ 2 / 4 ] simplifiying candidate #posit16 1) (+.p16 (sqrt.p16 (+.p16 (real->posit16 1) x)) (sqrt.p16 x))) (real->posit16 1.0)))> 1554305031.361 * [enter]simplify: Simplifying (*.p16 (/.p16 (real->posit16 1) (+.p16 (sqrt.p16 (+.p16 (real->posit16 1) x)) (sqrt.p16 x))) (real->posit16 1.0)) 1554305031.361 * * [misc]simplify: iters left: 6 (11 enodes) 1554305031.366 * * [misc]simplify: iters left: 5 (22 enodes) 1554305031.375 * * [misc]simplify: iters left: 4 (38 enodes) 1554305031.402 * * [misc]simplify: iters left: 3 (63 enodes) 1554305031.418 * * [misc]simplify: iters left: 2 (100 enodes) 1554305031.549 * * [misc]simplify: iters left: 1 (268 enodes) 1554305031.597 * * [misc]simplify: Extracting #0: cost 1 inf + 0 1554305031.597 * * [misc]simplify: Extracting #1: cost 7 inf + 0 1554305031.597 * * [misc]simplify: Extracting #2: cost 18 inf + 0 1554305031.597 * * [misc]simplify: Extracting #3: cost 12 inf + 1292 1554305031.598 * * [misc]simplify: Extracting #4: cost 6 inf + 2341 1554305031.599 * * [misc]simplify: Extracting #5: cost 1 inf + 4713 1554305031.600 * * [misc]simplify: Extracting #6: cost 0 inf + 5315 1554305031.600 * [exit]simplify: Simplified to (/.p16 (real->posit16 1) (+.p16 (sqrt.p16 (+.p16 (real->posit16 1) x)) (sqrt.p16 x))) 1554305031.600 * [misc]simplify: Simplified (2) to (λ (x) (/.p16 (real->posit16 1) (+.p16 (sqrt.p16 (+.p16 (real->posit16 1) x)) (sqrt.p16 x)))) 1554305031.601 * * * * [misc]progress: [ 3 / 4 ] simplifiying candidate #posit16 1) (+.p16 (sqrt.p16 (+.p16 (real->posit16 1) x)) (sqrt.p16 x))) (real->posit16 1.0)))> 1554305031.601 * [enter]simplify: Simplifying (*.p16 (/.p16 (real->posit16 1) (+.p16 (sqrt.p16 (+.p16 (real->posit16 1) x)) (sqrt.p16 x))) (real->posit16 1.0)) 1554305031.601 * * [misc]simplify: iters left: 6 (11 enodes) 1554305031.606 * * [misc]simplify: iters left: 5 (22 enodes) 1554305031.616 * * [misc]simplify: iters left: 4 (38 enodes) 1554305031.634 * * [misc]simplify: iters left: 3 (63 enodes) 1554305031.646 * * [misc]simplify: iters left: 2 (100 enodes) 1554305031.718 * * [misc]simplify: iters left: 1 (268 enodes) 1554305031.755 * * [misc]simplify: Extracting #0: cost 1 inf + 0 1554305031.755 * * [misc]simplify: Extracting #1: cost 7 inf + 0 1554305031.755 * * [misc]simplify: Extracting #2: cost 18 inf + 0 1554305031.755 * * [misc]simplify: Extracting #3: cost 12 inf + 1292 1554305031.755 * * [misc]simplify: Extracting #4: cost 6 inf + 2341 1554305031.756 * * [misc]simplify: Extracting #5: cost 1 inf + 4713 1554305031.756 * * [misc]simplify: Extracting #6: cost 0 inf + 5315 1554305031.756 * [exit]simplify: Simplified to (/.p16 (real->posit16 1) (+.p16 (sqrt.p16 (+.p16 (real->posit16 1) x)) (sqrt.p16 x))) 1554305031.757 * [misc]simplify: Simplified (2) to (λ (x) (/.p16 (real->posit16 1) (+.p16 (sqrt.p16 (+.p16 (real->posit16 1) x)) (sqrt.p16 x)))) 1554305031.757 * * * * [misc]progress: [ 4 / 4 ] simplifiying candidate #posit16 1) (+.p16 (sqrt.p16 (+.p16 (real->posit16 1) x)) (sqrt.p16 x))) (real->posit16 1.0)))> 1554305031.757 * [enter]simplify: Simplifying (*.p16 (/.p16 (real->posit16 1) (+.p16 (sqrt.p16 (+.p16 (real->posit16 1) x)) (sqrt.p16 x))) (real->posit16 1.0)) 1554305031.757 * * [misc]simplify: iters left: 6 (11 enodes) 1554305031.760 * * [misc]simplify: iters left: 5 (22 enodes) 1554305031.764 * * [misc]simplify: iters left: 4 (38 enodes) 1554305031.776 * * [misc]simplify: iters left: 3 (63 enodes) 1554305031.784 * * [misc]simplify: iters left: 2 (100 enodes) 1554305031.867 * * [misc]simplify: iters left: 1 (268 enodes) 1554305031.901 * * [misc]simplify: Extracting #0: cost 1 inf + 0 1554305031.901 * * [misc]simplify: Extracting #1: cost 7 inf + 0 1554305031.901 * * [misc]simplify: Extracting #2: cost 18 inf + 0 1554305031.901 * * [misc]simplify: Extracting #3: cost 12 inf + 1292 1554305031.902 * * [misc]simplify: Extracting #4: cost 6 inf + 2341 1554305031.902 * * [misc]simplify: Extracting #5: cost 1 inf + 4713 1554305031.903 * * [misc]simplify: Extracting #6: cost 0 inf + 5315 1554305031.904 * [exit]simplify: Simplified to (/.p16 (real->posit16 1) (+.p16 (sqrt.p16 (+.p16 (real->posit16 1) x)) (sqrt.p16 x))) 1554305031.904 * [misc]simplify: Simplified (2) to (λ (x) (/.p16 (real->posit16 1) (+.p16 (sqrt.p16 (+.p16 (real->posit16 1) x)) (sqrt.p16 x)))) 1554305031.904 * * * [misc]progress: adding candidates to table 1554305032.044 * [misc]progress: [Phase 3 of 3] Extracting. 1554305032.044 * * [misc]regime: Finding splitpoints for: (#posit16 1))) (sqrt.p16 (+.p16 x (real->posit16 1)))) (*.p16 (sqrt.p16 (+.p16 x (real->posit16 1))) (sqrt.p16 (+.p16 x (real->posit16 1))))) (*.p16 (*.p16 (sqrt.p16 x) (sqrt.p16 x)) (*.p16 (sqrt.p16 x) (sqrt.p16 x)))) (+.p16 (*.p16 (sqrt.p16 (+.p16 x (real->posit16 1))) (sqrt.p16 (+.p16 x (real->posit16 1)))) (*.p16 (sqrt.p16 x) (sqrt.p16 x)))) (+.p16 (sqrt.p16 (+.p16 x (real->posit16 1))) (sqrt.p16 x))))> #posit16 1))) (sqrt.p16 x)))> #posit16 0.0) (real->posit16 1)) (+.p16 (+.p16 x x) (real->posit16 1))) (*.p16 (+.p16 (sqrt.p16 (+.p16 x (real->posit16 1))) (sqrt.p16 x)) (+.p16 (*.p16 (sqrt.p16 (+.p16 x (real->posit16 1))) (sqrt.p16 (+.p16 x (real->posit16 1)))) (*.p16 (sqrt.p16 x) (sqrt.p16 x))))))> #posit16 1)) (*.p16 (sqrt.p16 x) (sqrt.p16 x))) (+.p16 (sqrt.p16 (+.p16 x (real->posit16 1))) (sqrt.p16 x))))> #posit16 1))) (sqrt.p16 x)) (/.p16 (+.p16 (sqrt.p16 (+.p16 x (real->posit16 1))) (sqrt.p16 x)) (-.p16 (sqrt.p16 (+.p16 x (real->posit16 1))) (sqrt.p16 x)))))> #posit16 1) (+.p16 (sqrt.p16 (+.p16 (real->posit16 1) x)) (sqrt.p16 x))) (real->posit16 1.0)))> #posit16 0.0) (real->posit16 1)) (+.p16 (+.p16 x x) (real->posit16 1))) (+.p16 (sqrt.p16 (+.p16 x (real->posit16 1))) (sqrt.p16 x))) (+.p16 x (+.p16 (real->posit16 1) x))))>) 1554305032.046 * * * [misc]regime-changes: Trying 1 branch expressions: (x) 1554305032.046 * * * * [misc]regimes: Trying to branch on x from (#posit16 1))) (sqrt.p16 (+.p16 x (real->posit16 1)))) (*.p16 (sqrt.p16 (+.p16 x (real->posit16 1))) (sqrt.p16 (+.p16 x (real->posit16 1))))) (*.p16 (*.p16 (sqrt.p16 x) (sqrt.p16 x)) (*.p16 (sqrt.p16 x) (sqrt.p16 x)))) (+.p16 (*.p16 (sqrt.p16 (+.p16 x (real->posit16 1))) (sqrt.p16 (+.p16 x (real->posit16 1)))) (*.p16 (sqrt.p16 x) (sqrt.p16 x)))) (+.p16 (sqrt.p16 (+.p16 x (real->posit16 1))) (sqrt.p16 x))))> #posit16 1))) (sqrt.p16 x)))> #posit16 0.0) (real->posit16 1)) (+.p16 (+.p16 x x) (real->posit16 1))) (*.p16 (+.p16 (sqrt.p16 (+.p16 x (real->posit16 1))) (sqrt.p16 x)) (+.p16 (*.p16 (sqrt.p16 (+.p16 x (real->posit16 1))) (sqrt.p16 (+.p16 x (real->posit16 1)))) (*.p16 (sqrt.p16 x) (sqrt.p16 x))))))> #posit16 1)) (*.p16 (sqrt.p16 x) (sqrt.p16 x))) (+.p16 (sqrt.p16 (+.p16 x (real->posit16 1))) (sqrt.p16 x))))> #posit16 1))) (sqrt.p16 x)) (/.p16 (+.p16 (sqrt.p16 (+.p16 x (real->posit16 1))) (sqrt.p16 x)) (-.p16 (sqrt.p16 (+.p16 x (real->posit16 1))) (sqrt.p16 x)))))> #posit16 1) (+.p16 (sqrt.p16 (+.p16 (real->posit16 1) x)) (sqrt.p16 x))) (real->posit16 1.0)))> #posit16 0.0) (real->posit16 1)) (+.p16 (+.p16 x x) (real->posit16 1))) (+.p16 (sqrt.p16 (+.p16 x (real->posit16 1))) (sqrt.p16 x))) (+.p16 x (+.p16 (real->posit16 1) x))))>) 1554305032.238 * * * [misc]regime: Found split indices: #