1554300797.646 * [misc]progress:  [Phase 1 of 3] Setting up.
1554300797.646 * * * [misc]progress:  [1/2] Preparing points
1554300797.647 * * * * [misc]points:  Sampling 256 additional inputs, on iter 0 have 0 / 256
1554300797.648 * * * * [misc]points:  Computing exacts on every 16 of 256 points to ramp up precision
1554300797.654 * * * * [misc]points:  Setting MPFR precision to 64
1554300797.655 * * * * [misc]points:  Setting MPFR precision to 320
1554300797.657 * * * * [misc]points:  Computing exacts on every 8 of 256 points to ramp up precision
1554300797.668 * * * * [misc]points:  Setting MPFR precision to 64
1554300797.671 * * * * [misc]points:  Setting MPFR precision to 320
1554300797.674 * * * * [misc]points:  Computing exacts on every 4 of 256 points to ramp up precision
1554300797.684 * * * * [misc]points:  Setting MPFR precision to 64
1554300797.688 * * * * [misc]points:  Setting MPFR precision to 320
1554300797.694 * * * * [misc]points:  Computing exacts on every 2 of 256 points to ramp up precision
1554300797.704 * * * * [misc]points:  Setting MPFR precision to 64
1554300797.713 * * * * [misc]points:  Setting MPFR precision to 320
1554300797.722 * * * * [misc]points:  Computing exacts for 256 points
1554300797.746 * * * * [misc]points:  Setting MPFR precision to 64
1554300797.774 * * * * [misc]points:  Setting MPFR precision to 320
1554300797.801 * * * * [misc]points:  Filtering points with unrepresentable outputs
1554300797.802 * * * * [exit]points:  Sampled 256 points with exact outputs
1554300797.802 * * * [misc]progress:  [2/2] Setting up program.
1554300797.835 * [misc]progress:  [Phase 2 of 3] Improving.
1554300797.835 * * * * [misc]progress:  [ 1 / 1 ] simplifiying candidate #<alt (λ (a rand) (*.p16 (-.p16 a (/.p16 (real->posit16 1.0) (real->posit16 3.0))) (+.p16 (real->posit16 1) (*.p16 (/.p16 (real->posit16 1) (sqrt.p16 (*.p16 (real->posit16 9) (-.p16 a (/.p16 (real->posit16 1.0) (real->posit16 3.0)))))) rand))))>
1554300797.835 * [enter]simplify:  Simplifying (*.p16 (-.p16 a (/.p16 (real->posit16 1.0) (real->posit16 3.0))) (+.p16 (real->posit16 1) (*.p16 (/.p16 (real->posit16 1) (sqrt.p16 (*.p16 (real->posit16 9) (-.p16 a (/.p16 (real->posit16 1.0) (real->posit16 3.0)))))) rand)))
1554300797.836 * * [misc]simplify:  iters left: 6 (18 enodes)
1554300797.844 * * [misc]simplify:  iters left: 5 (47 enodes)
1554300797.860 * * [misc]simplify:  iters left: 4 (121 enodes)
1554300797.907 * * [misc]simplify:  iters left: 3 (337 enodes)
1554300798.035 * * [misc]simplify:  Extracting #0: cost 1 inf + 0
1554300798.035 * * [misc]simplify:  Extracting #1: cost 34 inf + 0
1554300798.035 * * [misc]simplify:  Extracting #2: cost 204 inf + 0
1554300798.036 * * [misc]simplify:  Extracting #3: cost 326 inf + 1286
1554300798.038 * * [misc]simplify:  Extracting #4: cost 362 inf + 6740
1554300798.040 * * [misc]simplify:  Extracting #5: cost 377 inf + 18286
1554300798.046 * * [misc]simplify:  Extracting #6: cost 358 inf + 29885
1554300798.056 * * [misc]simplify:  Extracting #7: cost 252 inf + 186163
1554300798.085 * * [misc]simplify:  Extracting #8: cost 47 inf + 586692
1554300798.123 * * [misc]simplify:  Extracting #9: cost 0 inf + 696950
1554300798.172 * * [misc]simplify:  Extracting #10: cost 0 inf + 694590
1554300798.230 * [exit]simplify:  Simplified to (*.p16 (-.p16 a (/.p16 (real->posit16 1.0) (real->posit16 3.0))) (+.p16 (real->posit16 1) (/.p16 (*.p16 (real->posit16 1) rand) (sqrt.p16 (*.p16 (-.p16 a (/.p16 (real->posit16 1.0) (real->posit16 3.0))) (real->posit16 9))))))
1554300798.230 * [misc]simplify:  Simplified (2) to (λ (a rand) (*.p16 (-.p16 a (/.p16 (real->posit16 1.0) (real->posit16 3.0))) (+.p16 (real->posit16 1) (/.p16 (*.p16 (real->posit16 1) rand) (sqrt.p16 (*.p16 (-.p16 a (/.p16 (real->posit16 1.0) (real->posit16 3.0))) (real->posit16 9)))))))
1554300798.255 * * [misc]progress:  iteration 1 / 4
1554300798.255 * * * [misc]progress:  picking best candidate
1554300798.272 * * * * [misc]pick:  Picked  #<alt (λ (a rand) (*.p16 (-.p16 a (/.p16 (real->posit16 1.0) (real->posit16 3.0))) (+.p16 (real->posit16 1) (*.p16 (/.p16 (real->posit16 1) (sqrt.p16 (*.p16 (real->posit16 9) (-.p16 a (/.p16 (real->posit16 1.0) (real->posit16 3.0)))))) rand))))>
1554300798.272 * * * [misc]progress:  localizing error
1554300798.490 * * * [misc]progress:  generating rewritten candidates
1554300798.490 * * * * [misc]progress:  [ 1 / 4 ] rewriting at (2 2 2 1 2 1)
1554300798.492 * * * * [misc]progress:  [ 2 / 4 ] rewriting at (2 2 2 1 2 1 2)
1554300798.493 * * * * [misc]progress:  [ 3 / 4 ] rewriting at (2 1)
1554300798.493 * * * * [misc]progress:  [ 4 / 4 ] rewriting at (2 2 2 1 2)
1554300798.493 * * * [misc]progress:  generating series expansions
1554300798.494 * * * * [misc]progress:  [ 1 / 4 ] generating series at (2 2 2 1 2 1)
1554300798.494 * * * * [misc]progress:  [ 2 / 4 ] generating series at (2 2 2 1 2 1 2)
1554300798.494 * * * * [misc]progress:  [ 3 / 4 ] generating series at (2 1)
1554300798.494 * * * * [misc]progress:  [ 4 / 4 ] generating series at (2 2 2 1 2)
1554300798.494 * * * [misc]progress:  simplifying candidates
1554300798.494 * * * * [misc]progress:  [ 1 / 12 ] simplifiying candidate #<alt (λ (a rand) (*.p16 (-.p16 a (/.p16 (real->posit16 1.0) (real->posit16 3.0))) (+.p16 (real->posit16 1) (*.p16 (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 (*.p16 (real->posit16 9) a) (*.p16 (real->posit16 9) (neg.p16 (/.p16 (real->posit16 1.0) (real->posit16 3.0))))))) rand))))>
1554300798.494 * [enter]simplify:  Simplifying (*.p16 (real->posit16 9) (neg.p16 (/.p16 (real->posit16 1.0) (real->posit16 3.0))))
1554300798.494 * * [misc]simplify:  iters left: 4 (9 enodes)
1554300798.497 * * [misc]simplify:  iters left: 3 (13 enodes)
1554300798.499 * * [misc]simplify:  Extracting #0: cost 1 inf + 0
1554300798.499 * * [misc]simplify:  Extracting #1: cost 3 inf + 0
1554300798.499 * * [misc]simplify:  Extracting #2: cost 5 inf + 0
1554300798.499 * * [misc]simplify:  Extracting #3: cost 6 inf + 1
1554300798.499 * * [misc]simplify:  Extracting #4: cost 7 inf + 2
1554300798.499 * * [misc]simplify:  Extracting #5: cost 0 inf + 1813
1554300798.500 * [exit]simplify:  Simplified to (*.p16 (real->posit16 9) (neg.p16 (/.p16 (real->posit16 1.0) (real->posit16 3.0))))
1554300798.500 * [misc]simplify:  Simplified (2 2 2 1 2 1 2) to (λ (a rand) (*.p16 (-.p16 a (/.p16 (real->posit16 1.0) (real->posit16 3.0))) (+.p16 (real->posit16 1) (*.p16 (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 (*.p16 (real->posit16 9) a) (*.p16 (real->posit16 9) (neg.p16 (/.p16 (real->posit16 1.0) (real->posit16 3.0))))))) rand))))
1554300798.500 * * * * [misc]progress:  [ 2 / 12 ] simplifiying candidate #<alt (λ (a rand) (*.p16 (-.p16 a (/.p16 (real->posit16 1.0) (real->posit16 3.0))) (+.p16 (real->posit16 1) (*.p16 (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 (*.p16 a (real->posit16 9)) (*.p16 (neg.p16 (/.p16 (real->posit16 1.0) (real->posit16 3.0))) (real->posit16 9))))) rand))))>
1554300798.500 * [enter]simplify:  Simplifying (*.p16 (neg.p16 (/.p16 (real->posit16 1.0) (real->posit16 3.0))) (real->posit16 9))
1554300798.500 * * [misc]simplify:  iters left: 4 (9 enodes)
1554300798.502 * * [misc]simplify:  iters left: 3 (13 enodes)
1554300798.505 * * [misc]simplify:  Extracting #0: cost 1 inf + 0
1554300798.505 * * [misc]simplify:  Extracting #1: cost 3 inf + 0
1554300798.505 * * [misc]simplify:  Extracting #2: cost 5 inf + 0
1554300798.505 * * [misc]simplify:  Extracting #3: cost 5 inf + 2
1554300798.505 * * [misc]simplify:  Extracting #4: cost 7 inf + 2
1554300798.505 * * [misc]simplify:  Extracting #5: cost 4 inf + 5
1554300798.505 * * [misc]simplify:  Extracting #6: cost 0 inf + 1813
1554300798.505 * [exit]simplify:  Simplified to (*.p16 (neg.p16 (/.p16 (real->posit16 1.0) (real->posit16 3.0))) (real->posit16 9))
1554300798.505 * [misc]simplify:  Simplified (2 2 2 1 2 1 2) to (λ (a rand) (*.p16 (-.p16 a (/.p16 (real->posit16 1.0) (real->posit16 3.0))) (+.p16 (real->posit16 1) (*.p16 (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 (*.p16 a (real->posit16 9)) (*.p16 (neg.p16 (/.p16 (real->posit16 1.0) (real->posit16 3.0))) (real->posit16 9))))) rand))))
1554300798.505 * * * * [misc]progress:  [ 3 / 12 ] simplifiying candidate #<alt (λ (a rand) (*.p16 (-.p16 a (/.p16 (real->posit16 1.0) (real->posit16 3.0))) (+.p16 (real->posit16 1) (*.p16 (/.p16 (real->posit16 1) (sqrt.p16 (/.p16 (*.p16 (real->posit16 9) (-.p16 (*.p16 a a) (*.p16 (/.p16 (real->posit16 1.0) (real->posit16 3.0)) (/.p16 (real->posit16 1.0) (real->posit16 3.0))))) (+.p16 a (/.p16 (real->posit16 1.0) (real->posit16 3.0)))))) rand))))>
1554300798.505 * [enter]simplify:  Simplifying (+.p16 a (/.p16 (real->posit16 1.0) (real->posit16 3.0)))
1554300798.506 * * [misc]simplify:  iters left: 3 (7 enodes)
1554300798.507 * * [misc]simplify:  iters left: 2 (12 enodes)
1554300798.509 * * [misc]simplify:  Extracting #0: cost 1 inf + 0
1554300798.509 * * [misc]simplify:  Extracting #1: cost 3 inf + 0
1554300798.510 * * [misc]simplify:  Extracting #2: cost 4 inf + 1
1554300798.510 * * [misc]simplify:  Extracting #3: cost 6 inf + 1
1554300798.510 * * [misc]simplify:  Extracting #4: cost 0 inf + 930
1554300798.510 * [exit]simplify:  Simplified to (+.p16 a (/.p16 (real->posit16 1.0) (real->posit16 3.0)))
1554300798.510 * [misc]simplify:  Simplified (2 2 2 1 2 1 2) to (λ (a rand) (*.p16 (-.p16 a (/.p16 (real->posit16 1.0) (real->posit16 3.0))) (+.p16 (real->posit16 1) (*.p16 (/.p16 (real->posit16 1) (sqrt.p16 (/.p16 (*.p16 (real->posit16 9) (-.p16 (*.p16 a a) (*.p16 (/.p16 (real->posit16 1.0) (real->posit16 3.0)) (/.p16 (real->posit16 1.0) (real->posit16 3.0))))) (+.p16 a (/.p16 (real->posit16 1.0) (real->posit16 3.0)))))) rand))))
1554300798.510 * * * * [misc]progress:  [ 4 / 12 ] simplifiying candidate #<alt (λ (a rand) (*.p16 (-.p16 a (/.p16 (real->posit16 1.0) (real->posit16 3.0))) (+.p16 (real->posit16 1) (*.p16 (/.p16 (real->posit16 1) (sqrt.p16 (*.p16 (-.p16 a (/.p16 (real->posit16 1.0) (real->posit16 3.0))) (real->posit16 9)))) rand))))>
1554300798.510 * * * * [misc]progress:  [ 5 / 12 ] simplifiying candidate #<alt (λ (a rand) (*.p16 (-.p16 a (/.p16 (real->posit16 1.0) (real->posit16 3.0))) (+.p16 (real->posit16 1) (*.p16 (/.p16 (real->posit16 1) (sqrt.p16 (*.p16 (real->posit16 9) (+.p16 a (neg.p16 (/.p16 (real->posit16 1.0) (real->posit16 3.0))))))) rand))))>
1554300798.510 * * * * [misc]progress:  [ 6 / 12 ] simplifiying candidate #<alt (λ (a rand) (*.p16 (-.p16 a (/.p16 (real->posit16 1.0) (real->posit16 3.0))) (+.p16 (real->posit16 1) (*.p16 (/.p16 (real->posit16 1) (sqrt.p16 (*.p16 (real->posit16 9) (/.p16 (-.p16 (*.p16 a a) (*.p16 (/.p16 (real->posit16 1.0) (real->posit16 3.0)) (/.p16 (real->posit16 1.0) (real->posit16 3.0)))) (+.p16 a (/.p16 (real->posit16 1.0) (real->posit16 3.0))))))) rand))))>
1554300798.510 * * * * [misc]progress:  [ 7 / 12 ] simplifiying candidate #<alt (λ (a rand) (*.p16 (+.p16 a (neg.p16 (/.p16 (real->posit16 1.0) (real->posit16 3.0)))) (+.p16 (real->posit16 1) (*.p16 (/.p16 (real->posit16 1) (sqrt.p16 (*.p16 (real->posit16 9) (-.p16 a (/.p16 (real->posit16 1.0) (real->posit16 3.0)))))) rand))))>
1554300798.510 * * * * [misc]progress:  [ 8 / 12 ] simplifiying candidate #<alt (λ (a rand) (*.p16 (/.p16 (-.p16 (*.p16 a a) (*.p16 (/.p16 (real->posit16 1.0) (real->posit16 3.0)) (/.p16 (real->posit16 1.0) (real->posit16 3.0)))) (+.p16 a (/.p16 (real->posit16 1.0) (real->posit16 3.0)))) (+.p16 (real->posit16 1) (*.p16 (/.p16 (real->posit16 1) (sqrt.p16 (*.p16 (real->posit16 9) (-.p16 a (/.p16 (real->posit16 1.0) (real->posit16 3.0)))))) rand))))>
1554300798.510 * * * * [misc]progress:  [ 9 / 12 ] simplifiying candidate #<alt (λ (a rand) (*.p16 (-.p16 a (/.p16 (real->posit16 1.0) (real->posit16 3.0))) (+.p16 (real->posit16 1) (*.p16 (/.p16 (real->posit16 1) (sqrt.p16 (*.p16 (real->posit16 9) (-.p16 a (/.p16 (real->posit16 1.0) (real->posit16 3.0)))))) rand))))>
1554300798.510 * [enter]simplify:  Simplifying (*.p16 (-.p16 a (/.p16 (real->posit16 1.0) (real->posit16 3.0))) (+.p16 (real->posit16 1) (*.p16 (/.p16 (real->posit16 1) (sqrt.p16 (*.p16 (real->posit16 9) (-.p16 a (/.p16 (real->posit16 1.0) (real->posit16 3.0)))))) rand)))
1554300798.510 * * [misc]simplify:  iters left: 6 (18 enodes)
1554300798.515 * * [misc]simplify:  iters left: 5 (47 enodes)
1554300798.525 * * [misc]simplify:  iters left: 4 (121 enodes)
1554300798.558 * * [misc]simplify:  iters left: 3 (337 enodes)
1554300798.679 * * [misc]simplify:  Extracting #0: cost 1 inf + 0
1554300798.679 * * [misc]simplify:  Extracting #1: cost 34 inf + 0
1554300798.680 * * [misc]simplify:  Extracting #2: cost 204 inf + 0
1554300798.681 * * [misc]simplify:  Extracting #3: cost 326 inf + 1286
1554300798.682 * * [misc]simplify:  Extracting #4: cost 362 inf + 6740
1554300798.684 * * [misc]simplify:  Extracting #5: cost 377 inf + 18286
1554300798.687 * * [misc]simplify:  Extracting #6: cost 358 inf + 29885
1554300798.694 * * [misc]simplify:  Extracting #7: cost 252 inf + 186163
1554300798.725 * * [misc]simplify:  Extracting #8: cost 47 inf + 586692
1554300798.762 * * [misc]simplify:  Extracting #9: cost 0 inf + 696950
1554300798.805 * * [misc]simplify:  Extracting #10: cost 0 inf + 694590
1554300798.862 * [exit]simplify:  Simplified to (*.p16 (-.p16 a (/.p16 (real->posit16 1.0) (real->posit16 3.0))) (+.p16 (real->posit16 1) (/.p16 (*.p16 (real->posit16 1) rand) (sqrt.p16 (*.p16 (-.p16 a (/.p16 (real->posit16 1.0) (real->posit16 3.0))) (real->posit16 9))))))
1554300798.863 * [misc]simplify:  Simplified (2) to (λ (a rand) (*.p16 (-.p16 a (/.p16 (real->posit16 1.0) (real->posit16 3.0))) (+.p16 (real->posit16 1) (/.p16 (*.p16 (real->posit16 1) rand) (sqrt.p16 (*.p16 (-.p16 a (/.p16 (real->posit16 1.0) (real->posit16 3.0))) (real->posit16 9)))))))
1554300798.863 * * * * [misc]progress:  [ 10 / 12 ] simplifiying candidate #<alt (λ (a rand) (*.p16 (-.p16 a (/.p16 (real->posit16 1.0) (real->posit16 3.0))) (+.p16 (real->posit16 1) (*.p16 (/.p16 (real->posit16 1) (sqrt.p16 (*.p16 (real->posit16 9) (-.p16 a (/.p16 (real->posit16 1.0) (real->posit16 3.0)))))) rand))))>
1554300798.863 * [enter]simplify:  Simplifying (*.p16 (-.p16 a (/.p16 (real->posit16 1.0) (real->posit16 3.0))) (+.p16 (real->posit16 1) (*.p16 (/.p16 (real->posit16 1) (sqrt.p16 (*.p16 (real->posit16 9) (-.p16 a (/.p16 (real->posit16 1.0) (real->posit16 3.0)))))) rand)))
1554300798.863 * * [misc]simplify:  iters left: 6 (18 enodes)
1554300798.870 * * [misc]simplify:  iters left: 5 (47 enodes)
1554300798.883 * * [misc]simplify:  iters left: 4 (121 enodes)
1554300798.913 * * [misc]simplify:  iters left: 3 (337 enodes)
1554300799.033 * * [misc]simplify:  Extracting #0: cost 1 inf + 0
1554300799.033 * * [misc]simplify:  Extracting #1: cost 34 inf + 0
1554300799.034 * * [misc]simplify:  Extracting #2: cost 204 inf + 0
1554300799.035 * * [misc]simplify:  Extracting #3: cost 326 inf + 1286
1554300799.036 * * [misc]simplify:  Extracting #4: cost 362 inf + 6740
1554300799.038 * * [misc]simplify:  Extracting #5: cost 377 inf + 18286
1554300799.040 * * [misc]simplify:  Extracting #6: cost 358 inf + 29885
1554300799.047 * * [misc]simplify:  Extracting #7: cost 252 inf + 186163
1554300799.074 * * [misc]simplify:  Extracting #8: cost 47 inf + 586692
1554300799.112 * * [misc]simplify:  Extracting #9: cost 0 inf + 696950
1554300799.148 * * [misc]simplify:  Extracting #10: cost 0 inf + 694590
1554300799.183 * [exit]simplify:  Simplified to (*.p16 (-.p16 a (/.p16 (real->posit16 1.0) (real->posit16 3.0))) (+.p16 (real->posit16 1) (/.p16 (*.p16 (real->posit16 1) rand) (sqrt.p16 (*.p16 (-.p16 a (/.p16 (real->posit16 1.0) (real->posit16 3.0))) (real->posit16 9))))))
1554300799.183 * [misc]simplify:  Simplified (2) to (λ (a rand) (*.p16 (-.p16 a (/.p16 (real->posit16 1.0) (real->posit16 3.0))) (+.p16 (real->posit16 1) (/.p16 (*.p16 (real->posit16 1) rand) (sqrt.p16 (*.p16 (-.p16 a (/.p16 (real->posit16 1.0) (real->posit16 3.0))) (real->posit16 9)))))))
1554300799.184 * * * * [misc]progress:  [ 11 / 12 ] simplifiying candidate #<alt (λ (a rand) (*.p16 (-.p16 a (/.p16 (real->posit16 1.0) (real->posit16 3.0))) (+.p16 (real->posit16 1) (*.p16 (/.p16 (real->posit16 1) (sqrt.p16 (*.p16 (real->posit16 9) (-.p16 a (/.p16 (real->posit16 1.0) (real->posit16 3.0)))))) rand))))>
1554300799.184 * [enter]simplify:  Simplifying (*.p16 (-.p16 a (/.p16 (real->posit16 1.0) (real->posit16 3.0))) (+.p16 (real->posit16 1) (*.p16 (/.p16 (real->posit16 1) (sqrt.p16 (*.p16 (real->posit16 9) (-.p16 a (/.p16 (real->posit16 1.0) (real->posit16 3.0)))))) rand)))
1554300799.184 * * [misc]simplify:  iters left: 6 (18 enodes)
1554300799.189 * * [misc]simplify:  iters left: 5 (47 enodes)
1554300799.200 * * [misc]simplify:  iters left: 4 (121 enodes)
1554300799.229 * * [misc]simplify:  iters left: 3 (337 enodes)
1554300799.362 * * [misc]simplify:  Extracting #0: cost 1 inf + 0
1554300799.362 * * [misc]simplify:  Extracting #1: cost 34 inf + 0
1554300799.363 * * [misc]simplify:  Extracting #2: cost 204 inf + 0
1554300799.364 * * [misc]simplify:  Extracting #3: cost 326 inf + 1286
1554300799.365 * * [misc]simplify:  Extracting #4: cost 362 inf + 6740
1554300799.367 * * [misc]simplify:  Extracting #5: cost 377 inf + 18286
1554300799.370 * * [misc]simplify:  Extracting #6: cost 358 inf + 29885
1554300799.377 * * [misc]simplify:  Extracting #7: cost 252 inf + 186163
1554300799.403 * * [misc]simplify:  Extracting #8: cost 47 inf + 586692
1554300799.442 * * [misc]simplify:  Extracting #9: cost 0 inf + 696950
1554300799.486 * * [misc]simplify:  Extracting #10: cost 0 inf + 694590
1554300799.535 * [exit]simplify:  Simplified to (*.p16 (-.p16 a (/.p16 (real->posit16 1.0) (real->posit16 3.0))) (+.p16 (real->posit16 1) (/.p16 (*.p16 (real->posit16 1) rand) (sqrt.p16 (*.p16 (-.p16 a (/.p16 (real->posit16 1.0) (real->posit16 3.0))) (real->posit16 9))))))
1554300799.535 * [misc]simplify:  Simplified (2) to (λ (a rand) (*.p16 (-.p16 a (/.p16 (real->posit16 1.0) (real->posit16 3.0))) (+.p16 (real->posit16 1) (/.p16 (*.p16 (real->posit16 1) rand) (sqrt.p16 (*.p16 (-.p16 a (/.p16 (real->posit16 1.0) (real->posit16 3.0))) (real->posit16 9)))))))
1554300799.536 * * * * [misc]progress:  [ 12 / 12 ] simplifiying candidate #<alt (λ (a rand) (*.p16 (-.p16 a (/.p16 (real->posit16 1.0) (real->posit16 3.0))) (+.p16 (real->posit16 1) (*.p16 (/.p16 (real->posit16 1) (sqrt.p16 (*.p16 (real->posit16 9) (-.p16 a (/.p16 (real->posit16 1.0) (real->posit16 3.0)))))) rand))))>
1554300799.536 * [enter]simplify:  Simplifying (*.p16 (-.p16 a (/.p16 (real->posit16 1.0) (real->posit16 3.0))) (+.p16 (real->posit16 1) (*.p16 (/.p16 (real->posit16 1) (sqrt.p16 (*.p16 (real->posit16 9) (-.p16 a (/.p16 (real->posit16 1.0) (real->posit16 3.0)))))) rand)))
1554300799.537 * * [misc]simplify:  iters left: 6 (18 enodes)
1554300799.542 * * [misc]simplify:  iters left: 5 (47 enodes)
1554300799.552 * * [misc]simplify:  iters left: 4 (121 enodes)
1554300799.581 * * [misc]simplify:  iters left: 3 (337 enodes)
1554300799.758 * * [misc]simplify:  Extracting #0: cost 1 inf + 0
1554300799.758 * * [misc]simplify:  Extracting #1: cost 34 inf + 0
1554300799.759 * * [misc]simplify:  Extracting #2: cost 204 inf + 0
1554300799.760 * * [misc]simplify:  Extracting #3: cost 326 inf + 1286
1554300799.763 * * [misc]simplify:  Extracting #4: cost 362 inf + 6740
1554300799.766 * * [misc]simplify:  Extracting #5: cost 377 inf + 18286
1554300799.770 * * [misc]simplify:  Extracting #6: cost 358 inf + 29885
1554300799.782 * * [misc]simplify:  Extracting #7: cost 252 inf + 186163
1554300799.828 * * [misc]simplify:  Extracting #8: cost 47 inf + 586692
1554300799.878 * * [misc]simplify:  Extracting #9: cost 0 inf + 696950
1554300799.926 * * [misc]simplify:  Extracting #10: cost 0 inf + 694590
1554300799.977 * [exit]simplify:  Simplified to (*.p16 (-.p16 a (/.p16 (real->posit16 1.0) (real->posit16 3.0))) (+.p16 (real->posit16 1) (/.p16 (*.p16 (real->posit16 1) rand) (sqrt.p16 (*.p16 (-.p16 a (/.p16 (real->posit16 1.0) (real->posit16 3.0))) (real->posit16 9))))))
1554300799.977 * [misc]simplify:  Simplified (2) to (λ (a rand) (*.p16 (-.p16 a (/.p16 (real->posit16 1.0) (real->posit16 3.0))) (+.p16 (real->posit16 1) (/.p16 (*.p16 (real->posit16 1) rand) (sqrt.p16 (*.p16 (-.p16 a (/.p16 (real->posit16 1.0) (real->posit16 3.0))) (real->posit16 9)))))))
1554300799.977 * * * [misc]progress:  adding candidates to table
1554300800.462 * * [misc]progress:  iteration 2 / 4
1554300800.462 * * * [misc]progress:  picking best candidate
1554300800.524 * * * * [misc]pick:  Picked  #<alt (λ (a rand) (*.p16 (-.p16 a (/.p16 (real->posit16 1.0) (real->posit16 3.0))) (+.p16 (real->posit16 1) (*.p16 (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 (*.p16 a (real->posit16 9)) (*.p16 (neg.p16 (/.p16 (real->posit16 1.0) (real->posit16 3.0))) (real->posit16 9))))) rand))))>
1554300800.524 * * * [misc]progress:  localizing error
1554300800.694 * * * [misc]progress:  generating rewritten candidates
1554300800.694 * * * * [misc]progress:  [ 1 / 4 ] rewriting at (2 2 2 1 2 1)
1554300800.697 * * * * [misc]progress:  [ 2 / 4 ] rewriting at (2 1)
1554300800.698 * * * * [misc]progress:  [ 3 / 4 ] rewriting at (2 2 2 1 2)
1554300800.698 * * * * [misc]progress:  [ 4 / 4 ] rewriting at (2)
1554300800.701 * * * [misc]progress:  generating series expansions
1554300800.701 * * * * [misc]progress:  [ 1 / 4 ] generating series at (2 2 2 1 2 1)
1554300800.701 * * * * [misc]progress:  [ 2 / 4 ] generating series at (2 1)
1554300800.701 * * * * [misc]progress:  [ 3 / 4 ] generating series at (2 2 2 1 2)
1554300800.701 * * * * [misc]progress:  [ 4 / 4 ] generating series at (2)
1554300800.701 * * * [misc]progress:  simplifying candidates
1554300800.701 * * * * [misc]progress:  [ 1 / 12 ] simplifiying candidate #<alt (λ (a rand) (*.p16 (-.p16 a (/.p16 (real->posit16 1.0) (real->posit16 3.0))) (+.p16 (real->posit16 1) (*.p16 (/.p16 (real->posit16 1) (sqrt.p16 (*.p16 (real->posit16 9) (+.p16 a (neg.p16 (/.p16 (real->posit16 1.0) (real->posit16 3.0))))))) rand))))>
1554300800.701 * [enter]simplify:  Simplifying (real->posit16 9)
1554300800.701 * * [misc]simplify:  iters left: 1 (2 enodes)
1554300800.702 * * [misc]simplify:  Extracting #0: cost 1 inf + 0
1554300800.702 * * [misc]simplify:  Extracting #1: cost 2 inf + 0
1554300800.702 * * [misc]simplify:  Extracting #2: cost 1 inf + 1
1554300800.702 * * [misc]simplify:  Extracting #3: cost 0 inf + 2
1554300800.702 * [exit]simplify:  Simplified to (real->posit16 9)
1554300800.702 * [misc]simplify:  Simplified (2 2 2 1 2 1 1) to (λ (a rand) (*.p16 (-.p16 a (/.p16 (real->posit16 1.0) (real->posit16 3.0))) (+.p16 (real->posit16 1) (*.p16 (/.p16 (real->posit16 1) (sqrt.p16 (*.p16 (real->posit16 9) (+.p16 a (neg.p16 (/.p16 (real->posit16 1.0) (real->posit16 3.0))))))) rand))))
1554300800.703 * [enter]simplify:  Simplifying (+.p16 a (neg.p16 (/.p16 (real->posit16 1.0) (real->posit16 3.0))))
1554300800.703 * * [misc]simplify:  iters left: 4 (8 enodes)
1554300800.705 * * [misc]simplify:  iters left: 3 (14 enodes)
1554300800.708 * * [misc]simplify:  iters left: 2 (19 enodes)
1554300800.712 * * [misc]simplify:  iters left: 1 (32 enodes)
1554300800.719 * * [misc]simplify:  Extracting #0: cost 1 inf + 0
1554300800.719 * * [misc]simplify:  Extracting #1: cost 9 inf + 0
1554300800.719 * * [misc]simplify:  Extracting #2: cost 25 inf + 1
1554300800.719 * * [misc]simplify:  Extracting #3: cost 33 inf + 963
1554300800.719 * * [misc]simplify:  Extracting #4: cost 27 inf + 3209
1554300800.720 * * [misc]simplify:  Extracting #5: cost 12 inf + 14484
1554300800.722 * * [misc]simplify:  Extracting #6: cost 1 inf + 26872
1554300800.723 * * [misc]simplify:  Extracting #7: cost 0 inf + 29315
1554300800.724 * [exit]simplify:  Simplified to (-.p16 a (/.p16 (real->posit16 1.0) (real->posit16 3.0)))
1554300800.724 * [misc]simplify:  Simplified (2 2 2 1 2 1 2) to (λ (a rand) (*.p16 (-.p16 a (/.p16 (real->posit16 1.0) (real->posit16 3.0))) (+.p16 (real->posit16 1) (*.p16 (/.p16 (real->posit16 1) (sqrt.p16 (*.p16 (real->posit16 9) (-.p16 a (/.p16 (real->posit16 1.0) (real->posit16 3.0)))))) rand))))
1554300800.725 * * * * [misc]progress:  [ 2 / 12 ] simplifiying candidate #<alt (λ (a rand) (*.p16 (-.p16 a (/.p16 (real->posit16 1.0) (real->posit16 3.0))) (+.p16 (real->posit16 1) (*.p16 (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 (*.p16 (neg.p16 (/.p16 (real->posit16 1.0) (real->posit16 3.0))) (real->posit16 9)) (*.p16 a (real->posit16 9))))) rand))))>
1554300800.725 * * * * [misc]progress:  [ 3 / 12 ] simplifiying candidate #<alt (λ (a rand) (*.p16 (+.p16 a (neg.p16 (/.p16 (real->posit16 1.0) (real->posit16 3.0)))) (+.p16 (real->posit16 1) (*.p16 (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 (*.p16 a (real->posit16 9)) (*.p16 (neg.p16 (/.p16 (real->posit16 1.0) (real->posit16 3.0))) (real->posit16 9))))) rand))))>
1554300800.725 * * * * [misc]progress:  [ 4 / 12 ] simplifiying candidate #<alt (λ (a rand) (*.p16 (/.p16 (-.p16 (*.p16 a a) (*.p16 (/.p16 (real->posit16 1.0) (real->posit16 3.0)) (/.p16 (real->posit16 1.0) (real->posit16 3.0)))) (+.p16 a (/.p16 (real->posit16 1.0) (real->posit16 3.0)))) (+.p16 (real->posit16 1) (*.p16 (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 (*.p16 a (real->posit16 9)) (*.p16 (neg.p16 (/.p16 (real->posit16 1.0) (real->posit16 3.0))) (real->posit16 9))))) rand))))>
1554300800.725 * * * * [misc]progress:  [ 5 / 12 ] simplifiying candidate #<alt (λ (a rand) (+.p16 (*.p16 (-.p16 a (/.p16 (real->posit16 1.0) (real->posit16 3.0))) (real->posit16 1)) (*.p16 (-.p16 a (/.p16 (real->posit16 1.0) (real->posit16 3.0))) (*.p16 (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 (*.p16 a (real->posit16 9)) (*.p16 (neg.p16 (/.p16 (real->posit16 1.0) (real->posit16 3.0))) (real->posit16 9))))) rand))))>
1554300800.725 * [enter]simplify:  Simplifying (*.p16 (-.p16 a (/.p16 (real->posit16 1.0) (real->posit16 3.0))) (*.p16 (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 (*.p16 a (real->posit16 9)) (*.p16 (neg.p16 (/.p16 (real->posit16 1.0) (real->posit16 3.0))) (real->posit16 9))))) rand))
1554300800.725 * * [misc]simplify:  iters left: 6 (20 enodes)
1554300800.730 * * [misc]simplify:  iters left: 5 (46 enodes)
1554300800.749 * * [misc]simplify:  iters left: 4 (93 enodes)
1554300800.775 * * [misc]simplify:  iters left: 3 (261 enodes)
1554300800.919 * * [misc]simplify:  Extracting #0: cost 1 inf + 0
1554300800.919 * * [misc]simplify:  Extracting #1: cost 46 inf + 0
1554300800.920 * * [misc]simplify:  Extracting #2: cost 206 inf + 1
1554300800.922 * * [misc]simplify:  Extracting #3: cost 260 inf + 648
1554300800.924 * * [misc]simplify:  Extracting #4: cost 305 inf + 6747
1554300800.928 * * [misc]simplify:  Extracting #5: cost 257 inf + 43289
1554300800.942 * * [misc]simplify:  Extracting #6: cost 141 inf + 200788
1554300800.980 * * [misc]simplify:  Extracting #7: cost 16 inf + 437644
1554300801.006 * * [misc]simplify:  Extracting #8: cost 0 inf + 460444
1554300801.032 * * [misc]simplify:  Extracting #9: cost 0 inf + 457044
1554300801.058 * [exit]simplify:  Simplified to (/.p16 (*.p16 (-.p16 a (/.p16 (real->posit16 1.0) (real->posit16 3.0))) (*.p16 (real->posit16 1) rand)) (sqrt.p16 (*.p16 (-.p16 a (/.p16 (real->posit16 1.0) (real->posit16 3.0))) (real->posit16 9))))
1554300801.058 * [misc]simplify:  Simplified (2 2) to (λ (a rand) (+.p16 (*.p16 (-.p16 a (/.p16 (real->posit16 1.0) (real->posit16 3.0))) (real->posit16 1)) (/.p16 (*.p16 (-.p16 a (/.p16 (real->posit16 1.0) (real->posit16 3.0))) (*.p16 (real->posit16 1) rand)) (sqrt.p16 (*.p16 (-.p16 a (/.p16 (real->posit16 1.0) (real->posit16 3.0))) (real->posit16 9))))))
1554300801.058 * * * * [misc]progress:  [ 6 / 12 ] simplifiying candidate #<alt (λ (a rand) (+.p16 (*.p16 (real->posit16 1) (-.p16 a (/.p16 (real->posit16 1.0) (real->posit16 3.0)))) (*.p16 (*.p16 (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 (*.p16 a (real->posit16 9)) (*.p16 (neg.p16 (/.p16 (real->posit16 1.0) (real->posit16 3.0))) (real->posit16 9))))) rand) (-.p16 a (/.p16 (real->posit16 1.0) (real->posit16 3.0))))))>
1554300801.059 * [enter]simplify:  Simplifying (*.p16 (*.p16 (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 (*.p16 a (real->posit16 9)) (*.p16 (neg.p16 (/.p16 (real->posit16 1.0) (real->posit16 3.0))) (real->posit16 9))))) rand) (-.p16 a (/.p16 (real->posit16 1.0) (real->posit16 3.0))))
1554300801.059 * * [misc]simplify:  iters left: 6 (20 enodes)
1554300801.066 * * [misc]simplify:  iters left: 5 (46 enodes)
1554300801.077 * * [misc]simplify:  iters left: 4 (99 enodes)
1554300801.102 * * [misc]simplify:  iters left: 3 (283 enodes)
1554300801.204 * * [misc]simplify:  Extracting #0: cost 1 inf + 0
1554300801.204 * * [misc]simplify:  Extracting #1: cost 45 inf + 0
1554300801.205 * * [misc]simplify:  Extracting #2: cost 204 inf + 1
1554300801.207 * * [misc]simplify:  Extracting #3: cost 274 inf + 4
1554300801.209 * * [misc]simplify:  Extracting #4: cost 308 inf + 10273
1554300801.212 * * [misc]simplify:  Extracting #5: cost 292 inf + 21496
1554300801.219 * * [misc]simplify:  Extracting #6: cost 269 inf + 38708
1554300801.232 * * [misc]simplify:  Extracting #7: cost 145 inf + 207862
1554300801.268 * * [misc]simplify:  Extracting #8: cost 9 inf + 475349
1554300801.307 * * [misc]simplify:  Extracting #9: cost 0 inf + 483107
1554300801.345 * * [misc]simplify:  Extracting #10: cost 0 inf + 482187
1554300801.384 * [exit]simplify:  Simplified to (*.p16 (/.p16 (real->posit16 1) (sqrt.p16 (*.p16 (-.p16 a (/.p16 (real->posit16 1.0) (real->posit16 3.0))) (real->posit16 9)))) (*.p16 (-.p16 a (/.p16 (real->posit16 1.0) (real->posit16 3.0))) rand))
1554300801.384 * [misc]simplify:  Simplified (2 2) to (λ (a rand) (+.p16 (*.p16 (real->posit16 1) (-.p16 a (/.p16 (real->posit16 1.0) (real->posit16 3.0)))) (*.p16 (/.p16 (real->posit16 1) (sqrt.p16 (*.p16 (-.p16 a (/.p16 (real->posit16 1.0) (real->posit16 3.0))) (real->posit16 9)))) (*.p16 (-.p16 a (/.p16 (real->posit16 1.0) (real->posit16 3.0))) rand))))
1554300801.385 * * * * [misc]progress:  [ 7 / 12 ] simplifiying candidate #<alt (λ (a rand) (/.p16 (*.p16 (-.p16 (*.p16 a a) (*.p16 (/.p16 (real->posit16 1.0) (real->posit16 3.0)) (/.p16 (real->posit16 1.0) (real->posit16 3.0)))) (+.p16 (real->posit16 1) (*.p16 (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 (*.p16 a (real->posit16 9)) (*.p16 (neg.p16 (/.p16 (real->posit16 1.0) (real->posit16 3.0))) (real->posit16 9))))) rand))) (+.p16 a (/.p16 (real->posit16 1.0) (real->posit16 3.0)))))>
1554300801.385 * [enter]simplify:  Simplifying (*.p16 (-.p16 (*.p16 a a) (*.p16 (/.p16 (real->posit16 1.0) (real->posit16 3.0)) (/.p16 (real->posit16 1.0) (real->posit16 3.0)))) (+.p16 (real->posit16 1) (*.p16 (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 (*.p16 a (real->posit16 9)) (*.p16 (neg.p16 (/.p16 (real->posit16 1.0) (real->posit16 3.0))) (real->posit16 9))))) rand)))
1554300801.385 * * [misc]simplify:  iters left: 6 (23 enodes)
1554300801.394 * * [misc]simplify:  iters left: 5 (63 enodes)
1554300801.417 * * [misc]simplify:  iters left: 4 (160 enodes)
1554300801.488 * * [misc]simplify:  Extracting #0: cost 1 inf + 0
1554300801.488 * * [misc]simplify:  Extracting #1: cost 31 inf + 0
1554300801.488 * * [misc]simplify:  Extracting #2: cost 126 inf + 0
1554300801.489 * * [misc]simplify:  Extracting #3: cost 192 inf + 965
1554300801.489 * * [misc]simplify:  Extracting #4: cost 220 inf + 4817
1554300801.490 * * [misc]simplify:  Extracting #5: cost 206 inf + 16039
1554300801.492 * * [misc]simplify:  Extracting #6: cost 177 inf + 33734
1554300801.496 * * [misc]simplify:  Extracting #7: cost 103 inf + 117409
1554300801.506 * * [misc]simplify:  Extracting #8: cost 35 inf + 268230
1554300801.523 * * [misc]simplify:  Extracting #9: cost 0 inf + 358340
1554300801.540 * * [misc]simplify:  Extracting #10: cost 0 inf + 348740
1554300801.556 * [exit]simplify:  Simplified to (*.p16 (*.p16 (-.p16 a (/.p16 (real->posit16 1.0) (real->posit16 3.0))) (+.p16 a (/.p16 (real->posit16 1.0) (real->posit16 3.0)))) (+.p16 (real->posit16 1) (*.p16 (/.p16 (real->posit16 1) (sqrt.p16 (*.p16 (real->posit16 9) (-.p16 a (/.p16 (real->posit16 1.0) (real->posit16 3.0)))))) rand)))
1554300801.556 * [misc]simplify:  Simplified (2 1) to (λ (a rand) (/.p16 (*.p16 (*.p16 (-.p16 a (/.p16 (real->posit16 1.0) (real->posit16 3.0))) (+.p16 a (/.p16 (real->posit16 1.0) (real->posit16 3.0)))) (+.p16 (real->posit16 1) (*.p16 (/.p16 (real->posit16 1) (sqrt.p16 (*.p16 (real->posit16 9) (-.p16 a (/.p16 (real->posit16 1.0) (real->posit16 3.0)))))) rand))) (+.p16 a (/.p16 (real->posit16 1.0) (real->posit16 3.0)))))
1554300801.557 * * * * [misc]progress:  [ 8 / 12 ] simplifiying candidate #<alt (λ (a rand) (*.p16 (+.p16 (real->posit16 1) (*.p16 (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 (*.p16 a (real->posit16 9)) (*.p16 (neg.p16 (/.p16 (real->posit16 1.0) (real->posit16 3.0))) (real->posit16 9))))) rand)) (-.p16 a (/.p16 (real->posit16 1.0) (real->posit16 3.0)))))>
1554300801.557 * * * * [misc]progress:  [ 9 / 12 ] simplifiying candidate #<alt (λ (a rand) (*.p16 (-.p16 a (/.p16 (real->posit16 1.0) (real->posit16 3.0))) (+.p16 (real->posit16 1) (*.p16 (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 (*.p16 a (real->posit16 9)) (*.p16 (neg.p16 (/.p16 (real->posit16 1.0) (real->posit16 3.0))) (real->posit16 9))))) rand))))>
1554300801.557 * [enter]simplify:  Simplifying (*.p16 (neg.p16 (/.p16 (real->posit16 1.0) (real->posit16 3.0))) (real->posit16 9))
1554300801.557 * * [misc]simplify:  iters left: 4 (9 enodes)
1554300801.559 * * [misc]simplify:  iters left: 3 (13 enodes)
1554300801.562 * * [misc]simplify:  Extracting #0: cost 1 inf + 0
1554300801.562 * * [misc]simplify:  Extracting #1: cost 3 inf + 0
1554300801.562 * * [misc]simplify:  Extracting #2: cost 5 inf + 0
1554300801.562 * * [misc]simplify:  Extracting #3: cost 5 inf + 2
1554300801.562 * * [misc]simplify:  Extracting #4: cost 7 inf + 2
1554300801.562 * * [misc]simplify:  Extracting #5: cost 4 inf + 5
1554300801.562 * * [misc]simplify:  Extracting #6: cost 0 inf + 1813
1554300801.562 * [exit]simplify:  Simplified to (*.p16 (neg.p16 (/.p16 (real->posit16 1.0) (real->posit16 3.0))) (real->posit16 9))
1554300801.562 * [misc]simplify:  Simplified (2 2 2 1 2 1 2) to (λ (a rand) (*.p16 (-.p16 a (/.p16 (real->posit16 1.0) (real->posit16 3.0))) (+.p16 (real->posit16 1) (*.p16 (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 (*.p16 a (real->posit16 9)) (*.p16 (neg.p16 (/.p16 (real->posit16 1.0) (real->posit16 3.0))) (real->posit16 9))))) rand))))
1554300801.562 * * * * [misc]progress:  [ 10 / 12 ] simplifiying candidate #<alt (λ (a rand) (*.p16 (-.p16 a (/.p16 (real->posit16 1.0) (real->posit16 3.0))) (+.p16 (real->posit16 1) (*.p16 (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 (*.p16 a (real->posit16 9)) (*.p16 (neg.p16 (/.p16 (real->posit16 1.0) (real->posit16 3.0))) (real->posit16 9))))) rand))))>
1554300801.563 * [enter]simplify:  Simplifying (*.p16 (neg.p16 (/.p16 (real->posit16 1.0) (real->posit16 3.0))) (real->posit16 9))
1554300801.563 * * [misc]simplify:  iters left: 4 (9 enodes)
1554300801.567 * * [misc]simplify:  iters left: 3 (13 enodes)
1554300801.570 * * [misc]simplify:  Extracting #0: cost 1 inf + 0
1554300801.570 * * [misc]simplify:  Extracting #1: cost 3 inf + 0
1554300801.570 * * [misc]simplify:  Extracting #2: cost 5 inf + 0
1554300801.570 * * [misc]simplify:  Extracting #3: cost 5 inf + 2
1554300801.570 * * [misc]simplify:  Extracting #4: cost 7 inf + 2
1554300801.570 * * [misc]simplify:  Extracting #5: cost 4 inf + 5
1554300801.570 * * [misc]simplify:  Extracting #6: cost 0 inf + 1813
1554300801.570 * [exit]simplify:  Simplified to (*.p16 (neg.p16 (/.p16 (real->posit16 1.0) (real->posit16 3.0))) (real->posit16 9))
1554300801.570 * [misc]simplify:  Simplified (2 2 2 1 2 1 2) to (λ (a rand) (*.p16 (-.p16 a (/.p16 (real->posit16 1.0) (real->posit16 3.0))) (+.p16 (real->posit16 1) (*.p16 (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 (*.p16 a (real->posit16 9)) (*.p16 (neg.p16 (/.p16 (real->posit16 1.0) (real->posit16 3.0))) (real->posit16 9))))) rand))))
1554300801.570 * * * * [misc]progress:  [ 11 / 12 ] simplifiying candidate #<alt (λ (a rand) (*.p16 (-.p16 a (/.p16 (real->posit16 1.0) (real->posit16 3.0))) (+.p16 (real->posit16 1) (*.p16 (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 (*.p16 a (real->posit16 9)) (*.p16 (neg.p16 (/.p16 (real->posit16 1.0) (real->posit16 3.0))) (real->posit16 9))))) rand))))>
1554300801.570 * [enter]simplify:  Simplifying (*.p16 (neg.p16 (/.p16 (real->posit16 1.0) (real->posit16 3.0))) (real->posit16 9))
1554300801.570 * * [misc]simplify:  iters left: 4 (9 enodes)
1554300801.573 * * [misc]simplify:  iters left: 3 (13 enodes)
1554300801.576 * * [misc]simplify:  Extracting #0: cost 1 inf + 0
1554300801.576 * * [misc]simplify:  Extracting #1: cost 3 inf + 0
1554300801.576 * * [misc]simplify:  Extracting #2: cost 5 inf + 0
1554300801.576 * * [misc]simplify:  Extracting #3: cost 5 inf + 2
1554300801.576 * * [misc]simplify:  Extracting #4: cost 7 inf + 2
1554300801.576 * * [misc]simplify:  Extracting #5: cost 4 inf + 5
1554300801.576 * * [misc]simplify:  Extracting #6: cost 0 inf + 1813
1554300801.576 * [exit]simplify:  Simplified to (*.p16 (neg.p16 (/.p16 (real->posit16 1.0) (real->posit16 3.0))) (real->posit16 9))
1554300801.576 * [misc]simplify:  Simplified (2 2 2 1 2 1 2) to (λ (a rand) (*.p16 (-.p16 a (/.p16 (real->posit16 1.0) (real->posit16 3.0))) (+.p16 (real->posit16 1) (*.p16 (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 (*.p16 a (real->posit16 9)) (*.p16 (neg.p16 (/.p16 (real->posit16 1.0) (real->posit16 3.0))) (real->posit16 9))))) rand))))
1554300801.576 * * * * [misc]progress:  [ 12 / 12 ] simplifiying candidate #<alt (λ (a rand) (*.p16 (-.p16 a (/.p16 (real->posit16 1.0) (real->posit16 3.0))) (+.p16 (real->posit16 1) (*.p16 (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 (*.p16 a (real->posit16 9)) (*.p16 (neg.p16 (/.p16 (real->posit16 1.0) (real->posit16 3.0))) (real->posit16 9))))) rand))))>
1554300801.576 * [enter]simplify:  Simplifying (*.p16 (neg.p16 (/.p16 (real->posit16 1.0) (real->posit16 3.0))) (real->posit16 9))
1554300801.576 * * [misc]simplify:  iters left: 4 (9 enodes)
1554300801.579 * * [misc]simplify:  iters left: 3 (13 enodes)
1554300801.581 * * [misc]simplify:  Extracting #0: cost 1 inf + 0
1554300801.581 * * [misc]simplify:  Extracting #1: cost 3 inf + 0
1554300801.581 * * [misc]simplify:  Extracting #2: cost 5 inf + 0
1554300801.581 * * [misc]simplify:  Extracting #3: cost 5 inf + 2
1554300801.581 * * [misc]simplify:  Extracting #4: cost 7 inf + 2
1554300801.581 * * [misc]simplify:  Extracting #5: cost 4 inf + 5
1554300801.582 * * [misc]simplify:  Extracting #6: cost 0 inf + 1813
1554300801.582 * [exit]simplify:  Simplified to (*.p16 (neg.p16 (/.p16 (real->posit16 1.0) (real->posit16 3.0))) (real->posit16 9))
1554300801.582 * [misc]simplify:  Simplified (2 2 2 1 2 1 2) to (λ (a rand) (*.p16 (-.p16 a (/.p16 (real->posit16 1.0) (real->posit16 3.0))) (+.p16 (real->posit16 1) (*.p16 (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 (*.p16 a (real->posit16 9)) (*.p16 (neg.p16 (/.p16 (real->posit16 1.0) (real->posit16 3.0))) (real->posit16 9))))) rand))))
1554300801.582 * * * [misc]progress:  adding candidates to table
1554300802.039 * * [misc]progress:  iteration 3 / 4
1554300802.039 * * * [misc]progress:  picking best candidate
1554300802.125 * * * * [misc]pick:  Picked  #<alt (λ (a rand) (+.p16 (*.p16 (real->posit16 1) (-.p16 a (/.p16 (real->posit16 1.0) (real->posit16 3.0)))) (*.p16 (/.p16 (real->posit16 1) (sqrt.p16 (*.p16 (-.p16 a (/.p16 (real->posit16 1.0) (real->posit16 3.0))) (real->posit16 9)))) (*.p16 (-.p16 a (/.p16 (real->posit16 1.0) (real->posit16 3.0))) rand))))>
1554300802.125 * * * [misc]progress:  localizing error
1554300802.292 * * * [misc]progress:  generating rewritten candidates
1554300802.292 * * * * [misc]progress:  [ 1 / 4 ] rewriting at (2 2 1 2 1)
1554300802.295 * * * * [misc]progress:  [ 2 / 4 ] rewriting at (2 2 2 1)
1554300802.297 * * * * [misc]progress:  [ 3 / 4 ] rewriting at (2 2 1 2 1 1)
1554300802.298 * * * * [misc]progress:  [ 4 / 4 ] rewriting at (2 1 2)
1554300802.299 * * * [misc]progress:  generating series expansions
1554300802.299 * * * * [misc]progress:  [ 1 / 4 ] generating series at (2 2 1 2 1)
1554300802.299 * * * * [misc]progress:  [ 2 / 4 ] generating series at (2 2 2 1)
1554300802.299 * * * * [misc]progress:  [ 3 / 4 ] generating series at (2 2 1 2 1 1)
1554300802.299 * * * * [misc]progress:  [ 4 / 4 ] generating series at (2 1 2)
1554300802.299 * * * [misc]progress:  simplifying candidates
1554300802.299 * * * * [misc]progress:  [ 1 / 12 ] simplifiying candidate #<alt (λ (a rand) (+.p16 (*.p16 (real->posit16 1) (-.p16 a (/.p16 (real->posit16 1.0) (real->posit16 3.0)))) (*.p16 (/.p16 (real->posit16 1) (sqrt.p16 (/.p16 (*.p16 (-.p16 (*.p16 a a) (*.p16 (/.p16 (real->posit16 1.0) (real->posit16 3.0)) (/.p16 (real->posit16 1.0) (real->posit16 3.0)))) (real->posit16 9)) (+.p16 a (/.p16 (real->posit16 1.0) (real->posit16 3.0)))))) (*.p16 (-.p16 a (/.p16 (real->posit16 1.0) (real->posit16 3.0))) rand))))>
1554300802.300 * [enter]simplify:  Simplifying (*.p16 (-.p16 (*.p16 a a) (*.p16 (/.p16 (real->posit16 1.0) (real->posit16 3.0)) (/.p16 (real->posit16 1.0) (real->posit16 3.0)))) (real->posit16 9))
1554300802.300 * * [misc]simplify:  iters left: 5 (12 enodes)
1554300802.306 * * [misc]simplify:  iters left: 4 (32 enodes)
1554300802.319 * * [misc]simplify:  iters left: 3 (83 enodes)
1554300802.356 * * [misc]simplify:  iters left: 2 (328 enodes)
1554300802.709 * * [misc]simplify:  Extracting #0: cost 1 inf + 0
1554300802.709 * * [misc]simplify:  Extracting #1: cost 57 inf + 0
1554300802.710 * * [misc]simplify:  Extracting #2: cost 276 inf + 0
1554300802.711 * * [misc]simplify:  Extracting #3: cost 393 inf + 965
1554300802.713 * * [misc]simplify:  Extracting #4: cost 412 inf + 14118
1554300802.718 * * [misc]simplify:  Extracting #5: cost 371 inf + 47390
1554300802.727 * * [misc]simplify:  Extracting #6: cost 306 inf + 117500
1554300802.754 * * [misc]simplify:  Extracting #7: cost 113 inf + 438019
1554300802.801 * * [misc]simplify:  Extracting #8: cost 8 inf + 635803
1554300802.854 * * [misc]simplify:  Extracting #9: cost 0 inf + 657189
1554300802.908 * * [misc]simplify:  Extracting #10: cost 0 inf + 656909
1554300802.943 * [exit]simplify:  Simplified to (*.p16 (+.p16 a (/.p16 (real->posit16 1.0) (real->posit16 3.0))) (*.p16 (real->posit16 9) (-.p16 a (/.p16 (real->posit16 1.0) (real->posit16 3.0)))))
1554300802.943 * [misc]simplify:  Simplified (2 2 1 2 1 1) to (λ (a rand) (+.p16 (*.p16 (real->posit16 1) (-.p16 a (/.p16 (real->posit16 1.0) (real->posit16 3.0)))) (*.p16 (/.p16 (real->posit16 1) (sqrt.p16 (/.p16 (*.p16 (+.p16 a (/.p16 (real->posit16 1.0) (real->posit16 3.0))) (*.p16 (real->posit16 9) (-.p16 a (/.p16 (real->posit16 1.0) (real->posit16 3.0))))) (+.p16 a (/.p16 (real->posit16 1.0) (real->posit16 3.0)))))) (*.p16 (-.p16 a (/.p16 (real->posit16 1.0) (real->posit16 3.0))) rand))))
1554300802.944 * * * * [misc]progress:  [ 2 / 12 ] simplifiying candidate #<alt (λ (a rand) (+.p16 (*.p16 (real->posit16 1) (-.p16 a (/.p16 (real->posit16 1.0) (real->posit16 3.0)))) (*.p16 (/.p16 (real->posit16 1) (sqrt.p16 (*.p16 (real->posit16 9) (-.p16 a (/.p16 (real->posit16 1.0) (real->posit16 3.0)))))) (*.p16 (-.p16 a (/.p16 (real->posit16 1.0) (real->posit16 3.0))) rand))))>
1554300802.944 * * * * [misc]progress:  [ 3 / 12 ] simplifiying candidate #<alt (λ (a rand) (+.p16 (*.p16 (real->posit16 1) (-.p16 a (/.p16 (real->posit16 1.0) (real->posit16 3.0)))) (*.p16 (/.p16 (real->posit16 1) (sqrt.p16 (*.p16 (-.p16 a (/.p16 (real->posit16 1.0) (real->posit16 3.0))) (real->posit16 9)))) (*.p16 (+.p16 a (neg.p16 (/.p16 (real->posit16 1.0) (real->posit16 3.0)))) rand))))>
1554300802.944 * * * * [misc]progress:  [ 4 / 12 ] simplifiying candidate #<alt (λ (a rand) (+.p16 (*.p16 (real->posit16 1) (-.p16 a (/.p16 (real->posit16 1.0) (real->posit16 3.0)))) (*.p16 (/.p16 (real->posit16 1) (sqrt.p16 (*.p16 (-.p16 a (/.p16 (real->posit16 1.0) (real->posit16 3.0))) (real->posit16 9)))) (*.p16 (/.p16 (-.p16 (*.p16 a a) (*.p16 (/.p16 (real->posit16 1.0) (real->posit16 3.0)) (/.p16 (real->posit16 1.0) (real->posit16 3.0)))) (+.p16 a (/.p16 (real->posit16 1.0) (real->posit16 3.0)))) rand))))>
1554300802.944 * * * * [misc]progress:  [ 5 / 12 ] simplifiying candidate #<alt (λ (a rand) (+.p16 (*.p16 (real->posit16 1) (-.p16 a (/.p16 (real->posit16 1.0) (real->posit16 3.0)))) (*.p16 (/.p16 (real->posit16 1) (sqrt.p16 (*.p16 (+.p16 a (neg.p16 (/.p16 (real->posit16 1.0) (real->posit16 3.0)))) (real->posit16 9)))) (*.p16 (-.p16 a (/.p16 (real->posit16 1.0) (real->posit16 3.0))) rand))))>
1554300802.944 * * * * [misc]progress:  [ 6 / 12 ] simplifiying candidate #<alt (λ (a rand) (+.p16 (*.p16 (real->posit16 1) (-.p16 a (/.p16 (real->posit16 1.0) (real->posit16 3.0)))) (*.p16 (/.p16 (real->posit16 1) (sqrt.p16 (*.p16 (/.p16 (-.p16 (*.p16 a a) (*.p16 (/.p16 (real->posit16 1.0) (real->posit16 3.0)) (/.p16 (real->posit16 1.0) (real->posit16 3.0)))) (+.p16 a (/.p16 (real->posit16 1.0) (real->posit16 3.0)))) (real->posit16 9)))) (*.p16 (-.p16 a (/.p16 (real->posit16 1.0) (real->posit16 3.0))) rand))))>
1554300802.944 * * * * [misc]progress:  [ 7 / 12 ] simplifiying candidate #<alt (λ (a rand) (+.p16 (*.p16 (real->posit16 1) (+.p16 a (neg.p16 (/.p16 (real->posit16 1.0) (real->posit16 3.0))))) (*.p16 (/.p16 (real->posit16 1) (sqrt.p16 (*.p16 (-.p16 a (/.p16 (real->posit16 1.0) (real->posit16 3.0))) (real->posit16 9)))) (*.p16 (-.p16 a (/.p16 (real->posit16 1.0) (real->posit16 3.0))) rand))))>
1554300802.944 * * * * [misc]progress:  [ 8 / 12 ] simplifiying candidate #<alt (λ (a rand) (+.p16 (*.p16 (real->posit16 1) (/.p16 (-.p16 (*.p16 a a) (*.p16 (/.p16 (real->posit16 1.0) (real->posit16 3.0)) (/.p16 (real->posit16 1.0) (real->posit16 3.0)))) (+.p16 a (/.p16 (real->posit16 1.0) (real->posit16 3.0))))) (*.p16 (/.p16 (real->posit16 1) (sqrt.p16 (*.p16 (-.p16 a (/.p16 (real->posit16 1.0) (real->posit16 3.0))) (real->posit16 9)))) (*.p16 (-.p16 a (/.p16 (real->posit16 1.0) (real->posit16 3.0))) rand))))>
1554300802.944 * * * * [misc]progress:  [ 9 / 12 ] simplifiying candidate #<alt (λ (a rand) (+.p16 (*.p16 (real->posit16 1) (-.p16 a (/.p16 (real->posit16 1.0) (real->posit16 3.0)))) (*.p16 (/.p16 (real->posit16 1) (sqrt.p16 (*.p16 (-.p16 a (/.p16 (real->posit16 1.0) (real->posit16 3.0))) (real->posit16 9)))) (*.p16 (-.p16 a (/.p16 (real->posit16 1.0) (real->posit16 3.0))) rand))))>
1554300802.944 * [enter]simplify:  Simplifying (+.p16 (*.p16 (real->posit16 1) (-.p16 a (/.p16 (real->posit16 1.0) (real->posit16 3.0)))) (*.p16 (/.p16 (real->posit16 1) (sqrt.p16 (*.p16 (-.p16 a (/.p16 (real->posit16 1.0) (real->posit16 3.0))) (real->posit16 9)))) (*.p16 (-.p16 a (/.p16 (real->posit16 1.0) (real->posit16 3.0))) rand)))
1554300802.945 * * [misc]simplify:  iters left: 6 (19 enodes)
1554300802.951 * * [misc]simplify:  iters left: 5 (45 enodes)
1554300802.961 * * [misc]simplify:  iters left: 4 (113 enodes)
1554300802.990 * * [misc]simplify:  iters left: 3 (353 enodes)
1554300803.115 * * [misc]simplify:  Extracting #0: cost 1 inf + 0
1554300803.115 * * [misc]simplify:  Extracting #1: cost 28 inf + 0
1554300803.115 * * [misc]simplify:  Extracting #2: cost 109 inf + 0
1554300803.116 * * [misc]simplify:  Extracting #3: cost 307 inf + 324
1554300803.117 * * [misc]simplify:  Extracting #4: cost 358 inf + 6748
1554300803.119 * * [misc]simplify:  Extracting #5: cost 401 inf + 13486
1554300803.122 * * [misc]simplify:  Extracting #6: cost 366 inf + 43798
1554300803.133 * * [misc]simplify:  Extracting #7: cost 199 inf + 297008
1554300803.165 * * [misc]simplify:  Extracting #8: cost 9 inf + 638872
1554300803.197 * * [misc]simplify:  Extracting #9: cost 0 inf + 654033
1554300803.229 * [exit]simplify:  Simplified to (*.p16 (-.p16 a (/.p16 (real->posit16 1.0) (real->posit16 3.0))) (+.p16 (*.p16 (/.p16 (real->posit16 1) (sqrt.p16 (*.p16 (-.p16 a (/.p16 (real->posit16 1.0) (real->posit16 3.0))) (real->posit16 9)))) rand) (real->posit16 1)))
1554300803.229 * [misc]simplify:  Simplified (2) to (λ (a rand) (*.p16 (-.p16 a (/.p16 (real->posit16 1.0) (real->posit16 3.0))) (+.p16 (*.p16 (/.p16 (real->posit16 1) (sqrt.p16 (*.p16 (-.p16 a (/.p16 (real->posit16 1.0) (real->posit16 3.0))) (real->posit16 9)))) rand) (real->posit16 1))))
1554300803.229 * * * * [misc]progress:  [ 10 / 12 ] simplifiying candidate #<alt (λ (a rand) (+.p16 (*.p16 (real->posit16 1) (-.p16 a (/.p16 (real->posit16 1.0) (real->posit16 3.0)))) (*.p16 (/.p16 (real->posit16 1) (sqrt.p16 (*.p16 (-.p16 a (/.p16 (real->posit16 1.0) (real->posit16 3.0))) (real->posit16 9)))) (*.p16 (-.p16 a (/.p16 (real->posit16 1.0) (real->posit16 3.0))) rand))))>
1554300803.230 * [enter]simplify:  Simplifying (+.p16 (*.p16 (real->posit16 1) (-.p16 a (/.p16 (real->posit16 1.0) (real->posit16 3.0)))) (*.p16 (/.p16 (real->posit16 1) (sqrt.p16 (*.p16 (-.p16 a (/.p16 (real->posit16 1.0) (real->posit16 3.0))) (real->posit16 9)))) (*.p16 (-.p16 a (/.p16 (real->posit16 1.0) (real->posit16 3.0))) rand)))
1554300803.230 * * [misc]simplify:  iters left: 6 (19 enodes)
1554300803.235 * * [misc]simplify:  iters left: 5 (45 enodes)
1554300803.246 * * [misc]simplify:  iters left: 4 (113 enodes)
1554300803.275 * * [misc]simplify:  iters left: 3 (353 enodes)
1554300803.394 * * [misc]simplify:  Extracting #0: cost 1 inf + 0
1554300803.394 * * [misc]simplify:  Extracting #1: cost 28 inf + 0
1554300803.394 * * [misc]simplify:  Extracting #2: cost 109 inf + 0
1554300803.396 * * [misc]simplify:  Extracting #3: cost 307 inf + 324
1554300803.398 * * [misc]simplify:  Extracting #4: cost 358 inf + 6748
1554300803.401 * * [misc]simplify:  Extracting #5: cost 401 inf + 13486
1554300803.405 * * [misc]simplify:  Extracting #6: cost 366 inf + 43798
1554300803.424 * * [misc]simplify:  Extracting #7: cost 199 inf + 297008
1554300803.470 * * [misc]simplify:  Extracting #8: cost 9 inf + 638872
1554300803.525 * * [misc]simplify:  Extracting #9: cost 0 inf + 654033
1554300803.576 * [exit]simplify:  Simplified to (*.p16 (-.p16 a (/.p16 (real->posit16 1.0) (real->posit16 3.0))) (+.p16 (*.p16 (/.p16 (real->posit16 1) (sqrt.p16 (*.p16 (-.p16 a (/.p16 (real->posit16 1.0) (real->posit16 3.0))) (real->posit16 9)))) rand) (real->posit16 1)))
1554300803.576 * [misc]simplify:  Simplified (2) to (λ (a rand) (*.p16 (-.p16 a (/.p16 (real->posit16 1.0) (real->posit16 3.0))) (+.p16 (*.p16 (/.p16 (real->posit16 1) (sqrt.p16 (*.p16 (-.p16 a (/.p16 (real->posit16 1.0) (real->posit16 3.0))) (real->posit16 9)))) rand) (real->posit16 1))))
1554300803.577 * * * * [misc]progress:  [ 11 / 12 ] simplifiying candidate #<alt (λ (a rand) (+.p16 (*.p16 (real->posit16 1) (-.p16 a (/.p16 (real->posit16 1.0) (real->posit16 3.0)))) (*.p16 (/.p16 (real->posit16 1) (sqrt.p16 (*.p16 (-.p16 a (/.p16 (real->posit16 1.0) (real->posit16 3.0))) (real->posit16 9)))) (*.p16 (-.p16 a (/.p16 (real->posit16 1.0) (real->posit16 3.0))) rand))))>
1554300803.577 * [enter]simplify:  Simplifying (+.p16 (*.p16 (real->posit16 1) (-.p16 a (/.p16 (real->posit16 1.0) (real->posit16 3.0)))) (*.p16 (/.p16 (real->posit16 1) (sqrt.p16 (*.p16 (-.p16 a (/.p16 (real->posit16 1.0) (real->posit16 3.0))) (real->posit16 9)))) (*.p16 (-.p16 a (/.p16 (real->posit16 1.0) (real->posit16 3.0))) rand)))
1554300803.577 * * [misc]simplify:  iters left: 6 (19 enodes)
1554300803.585 * * [misc]simplify:  iters left: 5 (45 enodes)
1554300803.597 * * [misc]simplify:  iters left: 4 (113 enodes)
1554300803.628 * * [misc]simplify:  iters left: 3 (353 enodes)
1554300803.744 * * [misc]simplify:  Extracting #0: cost 1 inf + 0
1554300803.744 * * [misc]simplify:  Extracting #1: cost 28 inf + 0
1554300803.745 * * [misc]simplify:  Extracting #2: cost 109 inf + 0
1554300803.746 * * [misc]simplify:  Extracting #3: cost 307 inf + 324
1554300803.752 * * [misc]simplify:  Extracting #4: cost 358 inf + 6748
1554300803.754 * * [misc]simplify:  Extracting #5: cost 401 inf + 13486
1554300803.757 * * [misc]simplify:  Extracting #6: cost 366 inf + 43798
1554300803.770 * * [misc]simplify:  Extracting #7: cost 199 inf + 297008
1554300803.818 * * [misc]simplify:  Extracting #8: cost 9 inf + 638872
1554300803.856 * * [misc]simplify:  Extracting #9: cost 0 inf + 654033
1554300803.900 * [exit]simplify:  Simplified to (*.p16 (-.p16 a (/.p16 (real->posit16 1.0) (real->posit16 3.0))) (+.p16 (*.p16 (/.p16 (real->posit16 1) (sqrt.p16 (*.p16 (-.p16 a (/.p16 (real->posit16 1.0) (real->posit16 3.0))) (real->posit16 9)))) rand) (real->posit16 1)))
1554300803.900 * [misc]simplify:  Simplified (2) to (λ (a rand) (*.p16 (-.p16 a (/.p16 (real->posit16 1.0) (real->posit16 3.0))) (+.p16 (*.p16 (/.p16 (real->posit16 1) (sqrt.p16 (*.p16 (-.p16 a (/.p16 (real->posit16 1.0) (real->posit16 3.0))) (real->posit16 9)))) rand) (real->posit16 1))))
1554300803.900 * * * * [misc]progress:  [ 12 / 12 ] simplifiying candidate #<alt (λ (a rand) (+.p16 (*.p16 (real->posit16 1) (-.p16 a (/.p16 (real->posit16 1.0) (real->posit16 3.0)))) (*.p16 (/.p16 (real->posit16 1) (sqrt.p16 (*.p16 (-.p16 a (/.p16 (real->posit16 1.0) (real->posit16 3.0))) (real->posit16 9)))) (*.p16 (-.p16 a (/.p16 (real->posit16 1.0) (real->posit16 3.0))) rand))))>
1554300803.901 * [enter]simplify:  Simplifying (+.p16 (*.p16 (real->posit16 1) (-.p16 a (/.p16 (real->posit16 1.0) (real->posit16 3.0)))) (*.p16 (/.p16 (real->posit16 1) (sqrt.p16 (*.p16 (-.p16 a (/.p16 (real->posit16 1.0) (real->posit16 3.0))) (real->posit16 9)))) (*.p16 (-.p16 a (/.p16 (real->posit16 1.0) (real->posit16 3.0))) rand)))
1554300803.901 * * [misc]simplify:  iters left: 6 (19 enodes)
1554300803.908 * * [misc]simplify:  iters left: 5 (45 enodes)
1554300803.917 * * [misc]simplify:  iters left: 4 (113 enodes)
1554300803.948 * * [misc]simplify:  iters left: 3 (353 enodes)
1554300804.076 * * [misc]simplify:  Extracting #0: cost 1 inf + 0
1554300804.077 * * [misc]simplify:  Extracting #1: cost 28 inf + 0
1554300804.077 * * [misc]simplify:  Extracting #2: cost 109 inf + 0
1554300804.078 * * [misc]simplify:  Extracting #3: cost 307 inf + 324
1554300804.081 * * [misc]simplify:  Extracting #4: cost 358 inf + 6748
1554300804.084 * * [misc]simplify:  Extracting #5: cost 401 inf + 13486
1554300804.088 * * [misc]simplify:  Extracting #6: cost 366 inf + 43798
1554300804.106 * * [misc]simplify:  Extracting #7: cost 199 inf + 297008
1554300804.157 * * [misc]simplify:  Extracting #8: cost 9 inf + 638872
1554300804.210 * * [misc]simplify:  Extracting #9: cost 0 inf + 654033
1554300804.263 * [exit]simplify:  Simplified to (*.p16 (-.p16 a (/.p16 (real->posit16 1.0) (real->posit16 3.0))) (+.p16 (*.p16 (/.p16 (real->posit16 1) (sqrt.p16 (*.p16 (-.p16 a (/.p16 (real->posit16 1.0) (real->posit16 3.0))) (real->posit16 9)))) rand) (real->posit16 1)))
1554300804.263 * [misc]simplify:  Simplified (2) to (λ (a rand) (*.p16 (-.p16 a (/.p16 (real->posit16 1.0) (real->posit16 3.0))) (+.p16 (*.p16 (/.p16 (real->posit16 1) (sqrt.p16 (*.p16 (-.p16 a (/.p16 (real->posit16 1.0) (real->posit16 3.0))) (real->posit16 9)))) rand) (real->posit16 1))))
1554300804.263 * * * [misc]progress:  adding candidates to table
1554300804.860 * * [misc]progress:  iteration 4 / 4
1554300804.860 * * * [misc]progress:  picking best candidate
1554300804.930 * * * * [misc]pick:  Picked  #<alt (λ (a rand) (*.p16 (-.p16 a (/.p16 (real->posit16 1.0) (real->posit16 3.0))) (+.p16 (real->posit16 1) (*.p16 (/.p16 (real->posit16 1) (sqrt.p16 (/.p16 (*.p16 (real->posit16 9) (-.p16 (*.p16 a a) (*.p16 (/.p16 (real->posit16 1.0) (real->posit16 3.0)) (/.p16 (real->posit16 1.0) (real->posit16 3.0))))) (+.p16 a (/.p16 (real->posit16 1.0) (real->posit16 3.0)))))) rand))))>
1554300804.931 * * * [misc]progress:  localizing error
1554300805.207 * * * [misc]progress:  generating rewritten candidates
1554300805.207 * * * * [misc]progress:  [ 1 / 4 ] rewriting at (2 2 2 1 2 1 1 2 2)
1554300805.209 * * * * [misc]progress:  [ 2 / 4 ] rewriting at (2 2 2 1 2 1)
1554300805.212 * * * * [misc]progress:  [ 3 / 4 ] rewriting at (2 2 2 1 2 1 1)
1554300805.215 * * * * [misc]progress:  [ 4 / 4 ] rewriting at (2 2 2 1 2 1 1 2)
1554300805.217 * * * [misc]progress:  generating series expansions
1554300805.217 * * * * [misc]progress:  [ 1 / 4 ] generating series at (2 2 2 1 2 1 1 2 2)
1554300805.217 * * * * [misc]progress:  [ 2 / 4 ] generating series at (2 2 2 1 2 1)
1554300805.217 * * * * [misc]progress:  [ 3 / 4 ] generating series at (2 2 2 1 2 1 1)
1554300805.218 * * * * [misc]progress:  [ 4 / 4 ] generating series at (2 2 2 1 2 1 1 2)
1554300805.218 * * * [misc]progress:  simplifying candidates
1554300805.218 * * * * [misc]progress:  [ 1 / 17 ] simplifiying candidate #<alt (λ (a rand) (*.p16 (-.p16 a (/.p16 (real->posit16 1.0) (real->posit16 3.0))) (+.p16 (real->posit16 1) (*.p16 (/.p16 (real->posit16 1) (sqrt.p16 (/.p16 (*.p16 (real->posit16 9) (-.p16 (*.p16 a a) (/.p16 (*.p16 (/.p16 (real->posit16 1.0) (real->posit16 3.0)) (real->posit16 1.0)) (real->posit16 3.0)))) (+.p16 a (/.p16 (real->posit16 1.0) (real->posit16 3.0)))))) rand))))>
1554300805.218 * [enter]simplify:  Simplifying (real->posit16 3.0)
1554300805.218 * * [misc]simplify:  iters left: 1 (2 enodes)
1554300805.219 * * [misc]simplify:  Extracting #0: cost 1 inf + 0
1554300805.219 * * [misc]simplify:  Extracting #1: cost 2 inf + 0
1554300805.219 * * [misc]simplify:  Extracting #2: cost 1 inf + 1
1554300805.219 * * [misc]simplify:  Extracting #3: cost 0 inf + 2
1554300805.219 * [exit]simplify:  Simplified to (real->posit16 3.0)
1554300805.219 * [misc]simplify:  Simplified (2 2 2 1 2 1 1 2 2 2) to (λ (a rand) (*.p16 (-.p16 a (/.p16 (real->posit16 1.0) (real->posit16 3.0))) (+.p16 (real->posit16 1) (*.p16 (/.p16 (real->posit16 1) (sqrt.p16 (/.p16 (*.p16 (real->posit16 9) (-.p16 (*.p16 a a) (/.p16 (*.p16 (/.p16 (real->posit16 1.0) (real->posit16 3.0)) (real->posit16 1.0)) (real->posit16 3.0)))) (+.p16 a (/.p16 (real->posit16 1.0) (real->posit16 3.0)))))) rand))))
1554300805.219 * * * * [misc]progress:  [ 2 / 17 ] simplifiying candidate #<alt (λ (a rand) (*.p16 (-.p16 a (/.p16 (real->posit16 1.0) (real->posit16 3.0))) (+.p16 (real->posit16 1) (*.p16 (/.p16 (real->posit16 1) (sqrt.p16 (/.p16 (*.p16 (real->posit16 9) (-.p16 (*.p16 a a) (/.p16 (*.p16 (real->posit16 1.0) (/.p16 (real->posit16 1.0) (real->posit16 3.0))) (real->posit16 3.0)))) (+.p16 a (/.p16 (real->posit16 1.0) (real->posit16 3.0)))))) rand))))>
1554300805.219 * [enter]simplify:  Simplifying (*.p16 (real->posit16 1.0) (/.p16 (real->posit16 1.0) (real->posit16 3.0)))
1554300805.219 * * [misc]simplify:  iters left: 3 (6 enodes)
1554300805.221 * * [misc]simplify:  iters left: 2 (11 enodes)
1554300805.223 * * [misc]simplify:  iters left: 1 (19 enodes)
1554300805.227 * * [misc]simplify:  Extracting #0: cost 1 inf + 0
1554300805.227 * * [misc]simplify:  Extracting #1: cost 3 inf + 0
1554300805.227 * * [misc]simplify:  Extracting #2: cost 8 inf + 0
1554300805.227 * * [misc]simplify:  Extracting #3: cost 6 inf + 2
1554300805.227 * * [misc]simplify:  Extracting #4: cost 4 inf + 4
1554300805.227 * * [misc]simplify:  Extracting #5: cost 0 inf + 1530
1554300805.227 * [exit]simplify:  Simplified to (/.p16 (real->posit16 1.0) (real->posit16 3.0))
1554300805.227 * [misc]simplify:  Simplified (2 2 2 1 2 1 1 2 2 1) to (λ (a rand) (*.p16 (-.p16 a (/.p16 (real->posit16 1.0) (real->posit16 3.0))) (+.p16 (real->posit16 1) (*.p16 (/.p16 (real->posit16 1) (sqrt.p16 (/.p16 (*.p16 (real->posit16 9) (-.p16 (*.p16 a a) (/.p16 (/.p16 (real->posit16 1.0) (real->posit16 3.0)) (real->posit16 3.0)))) (+.p16 a (/.p16 (real->posit16 1.0) (real->posit16 3.0)))))) rand))))
1554300805.227 * * * * [misc]progress:  [ 3 / 17 ] simplifiying candidate #<alt (λ (a rand) (*.p16 (-.p16 a (/.p16 (real->posit16 1.0) (real->posit16 3.0))) (+.p16 (real->posit16 1) (*.p16 (/.p16 (real->posit16 1) (sqrt.p16 (/.p16 (*.p16 (real->posit16 9) (-.p16 (*.p16 a a) (*.p16 (/.p16 (real->posit16 1.0) (real->posit16 3.0)) (/.p16 (real->posit16 1.0) (real->posit16 3.0))))) (+.p16 a (/.p16 (real->posit16 1.0) (real->posit16 3.0)))))) rand))))>
1554300805.227 * * * * [misc]progress:  [ 4 / 17 ] simplifiying candidate #<alt (λ (a rand) (*.p16 (-.p16 a (/.p16 (real->posit16 1.0) (real->posit16 3.0))) (+.p16 (real->posit16 1) (*.p16 (/.p16 (real->posit16 1) (sqrt.p16 (/.p16 (real->posit16 9) (/.p16 (+.p16 a (/.p16 (real->posit16 1.0) (real->posit16 3.0))) (-.p16 (*.p16 a a) (*.p16 (/.p16 (real->posit16 1.0) (real->posit16 3.0)) (/.p16 (real->posit16 1.0) (real->posit16 3.0)))))))) rand))))>
1554300805.227 * [enter]simplify:  Simplifying (real->posit16 9)
1554300805.227 * * [misc]simplify:  iters left: 1 (2 enodes)
1554300805.228 * * [misc]simplify:  Extracting #0: cost 1 inf + 0
1554300805.228 * * [misc]simplify:  Extracting #1: cost 2 inf + 0
1554300805.228 * * [misc]simplify:  Extracting #2: cost 1 inf + 1
1554300805.228 * * [misc]simplify:  Extracting #3: cost 0 inf + 2
1554300805.228 * [exit]simplify:  Simplified to (real->posit16 9)
1554300805.228 * [misc]simplify:  Simplified (2 2 2 1 2 1 1) to (λ (a rand) (*.p16 (-.p16 a (/.p16 (real->posit16 1.0) (real->posit16 3.0))) (+.p16 (real->posit16 1) (*.p16 (/.p16 (real->posit16 1) (sqrt.p16 (/.p16 (real->posit16 9) (/.p16 (+.p16 a (/.p16 (real->posit16 1.0) (real->posit16 3.0))) (-.p16 (*.p16 a a) (*.p16 (/.p16 (real->posit16 1.0) (real->posit16 3.0)) (/.p16 (real->posit16 1.0) (real->posit16 3.0)))))))) rand))))
1554300805.228 * * * * [misc]progress:  [ 5 / 17 ] simplifiying candidate #<alt (λ (a rand) (*.p16 (-.p16 a (/.p16 (real->posit16 1.0) (real->posit16 3.0))) (+.p16 (real->posit16 1) (*.p16 (/.p16 (real->posit16 1) (sqrt.p16 (/.p16 (*.p16 (real->posit16 9) (-.p16 (*.p16 (*.p16 a a) (*.p16 a a)) (*.p16 (*.p16 (/.p16 (real->posit16 1.0) (real->posit16 3.0)) (/.p16 (real->posit16 1.0) (real->posit16 3.0))) (*.p16 (/.p16 (real->posit16 1.0) (real->posit16 3.0)) (/.p16 (real->posit16 1.0) (real->posit16 3.0)))))) (*.p16 (+.p16 a (/.p16 (real->posit16 1.0) (real->posit16 3.0))) (+.p16 (*.p16 a a) (*.p16 (/.p16 (real->posit16 1.0) (real->posit16 3.0)) (/.p16 (real->posit16 1.0) (real->posit16 3.0)))))))) rand))))>
1554300805.229 * [enter]simplify:  Simplifying (*.p16 (real->posit16 9) (-.p16 (*.p16 (*.p16 a a) (*.p16 a a)) (*.p16 (*.p16 (/.p16 (real->posit16 1.0) (real->posit16 3.0)) (/.p16 (real->posit16 1.0) (real->posit16 3.0))) (*.p16 (/.p16 (real->posit16 1.0) (real->posit16 3.0)) (/.p16 (real->posit16 1.0) (real->posit16 3.0))))))
1554300805.229 * * [misc]simplify:  iters left: 6 (14 enodes)
1554300805.232 * * [misc]simplify:  iters left: 5 (42 enodes)
1554300805.242 * * [misc]simplify:  iters left: 4 (124 enodes)
1554300805.287 * * [misc]simplify:  iters left: 3 (486 enodes)
1554300805.899 * * [misc]simplify:  Extracting #0: cost 1 inf + 0
1554300805.899 * * [misc]simplify:  Extracting #1: cost 81 inf + 0
1554300805.901 * * [misc]simplify:  Extracting #2: cost 389 inf + 0
1554300805.904 * * [misc]simplify:  Extracting #3: cost 599 inf + 6735
1554300805.911 * * [misc]simplify:  Extracting #4: cost 668 inf + 46772
1554300805.921 * * [misc]simplify:  Extracting #5: cost 583 inf + 119279
1554300805.949 * * [misc]simplify:  Extracting #6: cost 407 inf + 395443
1554300806.022 * * [misc]simplify:  Extracting #7: cost 67 inf + 1197512
1554300806.122 * * [misc]simplify:  Extracting #8: cost 1 inf + 1361954
1554300806.223 * * [misc]simplify:  Extracting #9: cost 0 inf + 1362437
1554300806.323 * [exit]simplify:  Simplified to (*.p16 (-.p16 (*.p16 (*.p16 a a) (*.p16 a a)) (/.p16 (real->posit16 1.0) (*.p16 (*.p16 (real->posit16 3.0) (real->posit16 3.0)) (*.p16 (real->posit16 3.0) (real->posit16 3.0))))) (real->posit16 9))
1554300806.323 * [misc]simplify:  Simplified (2 2 2 1 2 1 1) to (λ (a rand) (*.p16 (-.p16 a (/.p16 (real->posit16 1.0) (real->posit16 3.0))) (+.p16 (real->posit16 1) (*.p16 (/.p16 (real->posit16 1) (sqrt.p16 (/.p16 (*.p16 (-.p16 (*.p16 (*.p16 a a) (*.p16 a a)) (/.p16 (real->posit16 1.0) (*.p16 (*.p16 (real->posit16 3.0) (real->posit16 3.0)) (*.p16 (real->posit16 3.0) (real->posit16 3.0))))) (real->posit16 9)) (*.p16 (+.p16 a (/.p16 (real->posit16 1.0) (real->posit16 3.0))) (+.p16 (*.p16 a a) (*.p16 (/.p16 (real->posit16 1.0) (real->posit16 3.0)) (/.p16 (real->posit16 1.0) (real->posit16 3.0)))))))) rand))))
1554300806.324 * * * * [misc]progress:  [ 6 / 17 ] simplifiying candidate #<alt (λ (a rand) (*.p16 (-.p16 a (/.p16 (real->posit16 1.0) (real->posit16 3.0))) (+.p16 (real->posit16 1) (*.p16 (/.p16 (real->posit16 1) (sqrt.p16 (/.p16 (+.p16 (*.p16 (real->posit16 9) (*.p16 a a)) (*.p16 (real->posit16 9) (neg.p16 (*.p16 (/.p16 (real->posit16 1.0) (real->posit16 3.0)) (/.p16 (real->posit16 1.0) (real->posit16 3.0)))))) (+.p16 a (/.p16 (real->posit16 1.0) (real->posit16 3.0)))))) rand))))>
1554300806.324 * [enter]simplify:  Simplifying (*.p16 (real->posit16 9) (neg.p16 (*.p16 (/.p16 (real->posit16 1.0) (real->posit16 3.0)) (/.p16 (real->posit16 1.0) (real->posit16 3.0)))))
1554300806.324 * * [misc]simplify:  iters left: 5 (10 enodes)
1554300806.328 * * [misc]simplify:  iters left: 4 (18 enodes)
1554300806.334 * * [misc]simplify:  iters left: 3 (24 enodes)
1554300806.343 * * [misc]simplify:  iters left: 2 (59 enodes)
1554300806.365 * * [misc]simplify:  iters left: 1 (159 enodes)
1554300806.468 * * [misc]simplify:  Extracting #0: cost 1 inf + 0
1554300806.468 * * [misc]simplify:  Extracting #1: cost 3 inf + 0
1554300806.468 * * [misc]simplify:  Extracting #2: cost 5 inf + 0
1554300806.468 * * [misc]simplify:  Extracting #3: cost 24 inf + 1
1554300806.468 * * [misc]simplify:  Extracting #4: cost 87 inf + 2
1554300806.469 * * [misc]simplify:  Extracting #5: cost 77 inf + 2053
1554300806.470 * * [misc]simplify:  Extracting #6: cost 26 inf + 29454
1554300806.471 * * [misc]simplify:  Extracting #7: cost 0 inf + 49266
1554300806.473 * [exit]simplify:  Simplified to (*.p16 (neg.p16 (*.p16 (/.p16 (real->posit16 1.0) (real->posit16 3.0)) (/.p16 (real->posit16 1.0) (real->posit16 3.0)))) (real->posit16 9))
1554300806.473 * [misc]simplify:  Simplified (2 2 2 1 2 1 1 2) to (λ (a rand) (*.p16 (-.p16 a (/.p16 (real->posit16 1.0) (real->posit16 3.0))) (+.p16 (real->posit16 1) (*.p16 (/.p16 (real->posit16 1) (sqrt.p16 (/.p16 (+.p16 (*.p16 (real->posit16 9) (*.p16 a a)) (*.p16 (neg.p16 (*.p16 (/.p16 (real->posit16 1.0) (real->posit16 3.0)) (/.p16 (real->posit16 1.0) (real->posit16 3.0)))) (real->posit16 9))) (+.p16 a (/.p16 (real->posit16 1.0) (real->posit16 3.0)))))) rand))))
1554300806.473 * * * * [misc]progress:  [ 7 / 17 ] simplifiying candidate #<alt (λ (a rand) (*.p16 (-.p16 a (/.p16 (real->posit16 1.0) (real->posit16 3.0))) (+.p16 (real->posit16 1) (*.p16 (/.p16 (real->posit16 1) (sqrt.p16 (/.p16 (+.p16 (*.p16 (*.p16 a a) (real->posit16 9)) (*.p16 (neg.p16 (*.p16 (/.p16 (real->posit16 1.0) (real->posit16 3.0)) (/.p16 (real->posit16 1.0) (real->posit16 3.0)))) (real->posit16 9))) (+.p16 a (/.p16 (real->posit16 1.0) (real->posit16 3.0)))))) rand))))>
1554300806.474 * [enter]simplify:  Simplifying (*.p16 (neg.p16 (*.p16 (/.p16 (real->posit16 1.0) (real->posit16 3.0)) (/.p16 (real->posit16 1.0) (real->posit16 3.0)))) (real->posit16 9))
1554300806.474 * * [misc]simplify:  iters left: 5 (10 enodes)
1554300806.477 * * [misc]simplify:  iters left: 4 (18 enodes)
1554300806.480 * * [misc]simplify:  iters left: 3 (24 enodes)
1554300806.486 * * [misc]simplify:  iters left: 2 (60 enodes)
1554300806.503 * * [misc]simplify:  iters left: 1 (149 enodes)
1554300806.603 * * [misc]simplify:  Extracting #0: cost 1 inf + 0
1554300806.603 * * [misc]simplify:  Extracting #1: cost 3 inf + 0
1554300806.603 * * [misc]simplify:  Extracting #2: cost 5 inf + 0
1554300806.603 * * [misc]simplify:  Extracting #3: cost 9 inf + 2
1554300806.603 * * [misc]simplify:  Extracting #4: cost 62 inf + 2
1554300806.604 * * [misc]simplify:  Extracting #5: cost 55 inf + 969
1554300806.604 * * [misc]simplify:  Extracting #6: cost 20 inf + 15011
1554300806.606 * * [misc]simplify:  Extracting #7: cost 0 inf + 30251
1554300806.607 * [exit]simplify:  Simplified to (*.p16 (neg.p16 (/.p16 (real->posit16 1.0) (*.p16 (real->posit16 3.0) (real->posit16 3.0)))) (real->posit16 9))
1554300806.607 * [misc]simplify:  Simplified (2 2 2 1 2 1 1 2) to (λ (a rand) (*.p16 (-.p16 a (/.p16 (real->posit16 1.0) (real->posit16 3.0))) (+.p16 (real->posit16 1) (*.p16 (/.p16 (real->posit16 1) (sqrt.p16 (/.p16 (+.p16 (*.p16 (*.p16 a a) (real->posit16 9)) (*.p16 (neg.p16 (/.p16 (real->posit16 1.0) (*.p16 (real->posit16 3.0) (real->posit16 3.0)))) (real->posit16 9))) (+.p16 a (/.p16 (real->posit16 1.0) (real->posit16 3.0)))))) rand))))
1554300806.607 * * * * [misc]progress:  [ 8 / 17 ] simplifiying candidate #<alt (λ (a rand) (*.p16 (-.p16 a (/.p16 (real->posit16 1.0) (real->posit16 3.0))) (+.p16 (real->posit16 1) (*.p16 (/.p16 (real->posit16 1) (sqrt.p16 (/.p16 (*.p16 (*.p16 (real->posit16 9) (+.p16 a (/.p16 (real->posit16 1.0) (real->posit16 3.0)))) (-.p16 a (/.p16 (real->posit16 1.0) (real->posit16 3.0)))) (+.p16 a (/.p16 (real->posit16 1.0) (real->posit16 3.0)))))) rand))))>
1554300806.607 * [enter]simplify:  Simplifying (-.p16 a (/.p16 (real->posit16 1.0) (real->posit16 3.0)))
1554300806.607 * * [misc]simplify:  iters left: 3 (7 enodes)
1554300806.609 * * [misc]simplify:  iters left: 2 (18 enodes)
1554300806.612 * * [misc]simplify:  iters left: 1 (32 enodes)
1554300806.621 * * [misc]simplify:  Extracting #0: cost 1 inf + 0
1554300806.621 * * [misc]simplify:  Extracting #1: cost 9 inf + 0
1554300806.621 * * [misc]simplify:  Extracting #2: cost 25 inf + 1
1554300806.621 * * [misc]simplify:  Extracting #3: cost 34 inf + 322
1554300806.621 * * [misc]simplify:  Extracting #4: cost 27 inf + 3209
1554300806.622 * * [misc]simplify:  Extracting #5: cost 22 inf + 4898
1554300806.622 * * [misc]simplify:  Extracting #6: cost 11 inf + 15047
1554300806.623 * * [misc]simplify:  Extracting #7: cost 0 inf + 29315
1554300806.624 * [exit]simplify:  Simplified to (-.p16 a (/.p16 (real->posit16 1.0) (real->posit16 3.0)))
1554300806.624 * [misc]simplify:  Simplified (2 2 2 1 2 1 1 2) to (λ (a rand) (*.p16 (-.p16 a (/.p16 (real->posit16 1.0) (real->posit16 3.0))) (+.p16 (real->posit16 1) (*.p16 (/.p16 (real->posit16 1) (sqrt.p16 (/.p16 (*.p16 (*.p16 (real->posit16 9) (+.p16 a (/.p16 (real->posit16 1.0) (real->posit16 3.0)))) (-.p16 a (/.p16 (real->posit16 1.0) (real->posit16 3.0)))) (+.p16 a (/.p16 (real->posit16 1.0) (real->posit16 3.0)))))) rand))))
1554300806.625 * * * * [misc]progress:  [ 9 / 17 ] simplifiying candidate #<alt (λ (a rand) (*.p16 (-.p16 a (/.p16 (real->posit16 1.0) (real->posit16 3.0))) (+.p16 (real->posit16 1) (*.p16 (/.p16 (real->posit16 1) (sqrt.p16 (/.p16 (/.p16 (*.p16 (real->posit16 9) (-.p16 (*.p16 (*.p16 a a) (*.p16 a a)) (*.p16 (*.p16 (/.p16 (real->posit16 1.0) (real->posit16 3.0)) (/.p16 (real->posit16 1.0) (real->posit16 3.0))) (*.p16 (/.p16 (real->posit16 1.0) (real->posit16 3.0)) (/.p16 (real->posit16 1.0) (real->posit16 3.0)))))) (+.p16 (*.p16 a a) (*.p16 (/.p16 (real->posit16 1.0) (real->posit16 3.0)) (/.p16 (real->posit16 1.0) (real->posit16 3.0))))) (+.p16 a (/.p16 (real->posit16 1.0) (real->posit16 3.0)))))) rand))))>
1554300806.625 * [enter]simplify:  Simplifying (+.p16 (*.p16 a a) (*.p16 (/.p16 (real->posit16 1.0) (real->posit16 3.0)) (/.p16 (real->posit16 1.0) (real->posit16 3.0))))
1554300806.625 * * [misc]simplify:  iters left: 4 (9 enodes)
1554300806.627 * * [misc]simplify:  iters left: 3 (18 enodes)
1554300806.630 * * [misc]simplify:  iters left: 2 (24 enodes)
1554300806.636 * * [misc]simplify:  iters left: 1 (59 enodes)
1554300806.654 * * [misc]simplify:  Extracting #0: cost 1 inf + 0
1554300806.654 * * [misc]simplify:  Extracting #1: cost 3 inf + 0
1554300806.654 * * [misc]simplify:  Extracting #2: cost 30 inf + 0
1554300806.654 * * [misc]simplify:  Extracting #3: cost 68 inf + 322
1554300806.655 * * [misc]simplify:  Extracting #4: cost 34 inf + 13807
1554300806.656 * * [misc]simplify:  Extracting #5: cost 0 inf + 34348
1554300806.658 * [exit]simplify:  Simplified to (+.p16 (/.p16 (real->posit16 1.0) (*.p16 (real->posit16 3.0) (real->posit16 3.0))) (*.p16 a a))
1554300806.658 * [misc]simplify:  Simplified (2 2 2 1 2 1 1 2) to (λ (a rand) (*.p16 (-.p16 a (/.p16 (real->posit16 1.0) (real->posit16 3.0))) (+.p16 (real->posit16 1) (*.p16 (/.p16 (real->posit16 1) (sqrt.p16 (/.p16 (/.p16 (*.p16 (real->posit16 9) (-.p16 (*.p16 (*.p16 a a) (*.p16 a a)) (*.p16 (*.p16 (/.p16 (real->posit16 1.0) (real->posit16 3.0)) (/.p16 (real->posit16 1.0) (real->posit16 3.0))) (*.p16 (/.p16 (real->posit16 1.0) (real->posit16 3.0)) (/.p16 (real->posit16 1.0) (real->posit16 3.0)))))) (+.p16 (/.p16 (real->posit16 1.0) (*.p16 (real->posit16 3.0) (real->posit16 3.0))) (*.p16 a a))) (+.p16 a (/.p16 (real->posit16 1.0) (real->posit16 3.0)))))) rand))))
1554300806.658 * * * * [misc]progress:  [ 10 / 17 ] simplifiying candidate #<alt (λ (a rand) (*.p16 (-.p16 a (/.p16 (real->posit16 1.0) (real->posit16 3.0))) (+.p16 (real->posit16 1) (*.p16 (/.p16 (real->posit16 1) (sqrt.p16 (/.p16 (*.p16 (-.p16 (*.p16 a a) (*.p16 (/.p16 (real->posit16 1.0) (real->posit16 3.0)) (/.p16 (real->posit16 1.0) (real->posit16 3.0)))) (real->posit16 9)) (+.p16 a (/.p16 (real->posit16 1.0) (real->posit16 3.0)))))) rand))))>
1554300806.658 * * * * [misc]progress:  [ 11 / 17 ] simplifiying candidate #<alt (λ (a rand) (*.p16 (-.p16 a (/.p16 (real->posit16 1.0) (real->posit16 3.0))) (+.p16 (real->posit16 1) (*.p16 (/.p16 (real->posit16 1) (sqrt.p16 (/.p16 (*.p16 (real->posit16 9) (*.p16 (+.p16 a (/.p16 (real->posit16 1.0) (real->posit16 3.0))) (-.p16 a (/.p16 (real->posit16 1.0) (real->posit16 3.0))))) (+.p16 a (/.p16 (real->posit16 1.0) (real->posit16 3.0)))))) rand))))>
1554300806.658 * [enter]simplify:  Simplifying (+.p16 a (/.p16 (real->posit16 1.0) (real->posit16 3.0)))
1554300806.658 * * [misc]simplify:  iters left: 3 (7 enodes)
1554300806.660 * * [misc]simplify:  iters left: 2 (12 enodes)
1554300806.662 * * [misc]simplify:  Extracting #0: cost 1 inf + 0
1554300806.662 * * [misc]simplify:  Extracting #1: cost 3 inf + 0
1554300806.662 * * [misc]simplify:  Extracting #2: cost 4 inf + 1
1554300806.662 * * [misc]simplify:  Extracting #3: cost 6 inf + 1
1554300806.662 * * [misc]simplify:  Extracting #4: cost 0 inf + 930
1554300806.662 * [exit]simplify:  Simplified to (+.p16 a (/.p16 (real->posit16 1.0) (real->posit16 3.0)))
1554300806.662 * [misc]simplify:  Simplified (2 2 2 1 2 1 1 2 1) to (λ (a rand) (*.p16 (-.p16 a (/.p16 (real->posit16 1.0) (real->posit16 3.0))) (+.p16 (real->posit16 1) (*.p16 (/.p16 (real->posit16 1) (sqrt.p16 (/.p16 (*.p16 (real->posit16 9) (*.p16 (+.p16 a (/.p16 (real->posit16 1.0) (real->posit16 3.0))) (-.p16 a (/.p16 (real->posit16 1.0) (real->posit16 3.0))))) (+.p16 a (/.p16 (real->posit16 1.0) (real->posit16 3.0)))))) rand))))
1554300806.663 * [enter]simplify:  Simplifying (-.p16 a (/.p16 (real->posit16 1.0) (real->posit16 3.0)))
1554300806.663 * * [misc]simplify:  iters left: 3 (7 enodes)
1554300806.664 * * [misc]simplify:  iters left: 2 (18 enodes)
1554300806.668 * * [misc]simplify:  iters left: 1 (32 enodes)
1554300806.675 * * [misc]simplify:  Extracting #0: cost 1 inf + 0
1554300806.675 * * [misc]simplify:  Extracting #1: cost 9 inf + 0
1554300806.675 * * [misc]simplify:  Extracting #2: cost 25 inf + 1
1554300806.675 * * [misc]simplify:  Extracting #3: cost 34 inf + 322
1554300806.675 * * [misc]simplify:  Extracting #4: cost 27 inf + 3209
1554300806.675 * * [misc]simplify:  Extracting #5: cost 22 inf + 4898
1554300806.676 * * [misc]simplify:  Extracting #6: cost 11 inf + 15047
1554300806.677 * * [misc]simplify:  Extracting #7: cost 0 inf + 29315
1554300806.678 * [exit]simplify:  Simplified to (-.p16 a (/.p16 (real->posit16 1.0) (real->posit16 3.0)))
1554300806.678 * [misc]simplify:  Simplified (2 2 2 1 2 1 1 2 2) to (λ (a rand) (*.p16 (-.p16 a (/.p16 (real->posit16 1.0) (real->posit16 3.0))) (+.p16 (real->posit16 1) (*.p16 (/.p16 (real->posit16 1) (sqrt.p16 (/.p16 (*.p16 (real->posit16 9) (*.p16 (+.p16 a (/.p16 (real->posit16 1.0) (real->posit16 3.0))) (-.p16 a (/.p16 (real->posit16 1.0) (real->posit16 3.0))))) (+.p16 a (/.p16 (real->posit16 1.0) (real->posit16 3.0)))))) rand))))
1554300806.678 * * * * [misc]progress:  [ 12 / 17 ] simplifiying candidate #<alt (λ (a rand) (*.p16 (-.p16 a (/.p16 (real->posit16 1.0) (real->posit16 3.0))) (+.p16 (real->posit16 1) (*.p16 (/.p16 (real->posit16 1) (sqrt.p16 (/.p16 (*.p16 (real->posit16 9) (+.p16 (*.p16 a a) (neg.p16 (*.p16 (/.p16 (real->posit16 1.0) (real->posit16 3.0)) (/.p16 (real->posit16 1.0) (real->posit16 3.0)))))) (+.p16 a (/.p16 (real->posit16 1.0) (real->posit16 3.0)))))) rand))))>
1554300806.678 * * * * [misc]progress:  [ 13 / 17 ] simplifiying candidate #<alt (λ (a rand) (*.p16 (-.p16 a (/.p16 (real->posit16 1.0) (real->posit16 3.0))) (+.p16 (real->posit16 1) (*.p16 (/.p16 (real->posit16 1) (sqrt.p16 (/.p16 (*.p16 (real->posit16 9) (/.p16 (-.p16 (*.p16 (*.p16 a a) (*.p16 a a)) (*.p16 (*.p16 (/.p16 (real->posit16 1.0) (real->posit16 3.0)) (/.p16 (real->posit16 1.0) (real->posit16 3.0))) (*.p16 (/.p16 (real->posit16 1.0) (real->posit16 3.0)) (/.p16 (real->posit16 1.0) (real->posit16 3.0))))) (+.p16 (*.p16 a a) (*.p16 (/.p16 (real->posit16 1.0) (real->posit16 3.0)) (/.p16 (real->posit16 1.0) (real->posit16 3.0)))))) (+.p16 a (/.p16 (real->posit16 1.0) (real->posit16 3.0)))))) rand))))>
1554300806.678 * * * * [misc]progress:  [ 14 / 17 ] simplifiying candidate #<alt (λ (a rand) (*.p16 (-.p16 a (/.p16 (real->posit16 1.0) (real->posit16 3.0))) (+.p16 (real->posit16 1) (*.p16 (/.p16 (real->posit16 1) (sqrt.p16 (/.p16 (*.p16 (real->posit16 9) (-.p16 (*.p16 a a) (*.p16 (/.p16 (real->posit16 1.0) (real->posit16 3.0)) (/.p16 (real->posit16 1.0) (real->posit16 3.0))))) (+.p16 a (/.p16 (real->posit16 1.0) (real->posit16 3.0)))))) rand))))>
1554300806.678 * [enter]simplify:  Simplifying (+.p16 a (/.p16 (real->posit16 1.0) (real->posit16 3.0)))
1554300806.679 * * [misc]simplify:  iters left: 3 (7 enodes)
1554300806.680 * * [misc]simplify:  iters left: 2 (12 enodes)
1554300806.682 * * [misc]simplify:  Extracting #0: cost 1 inf + 0
1554300806.682 * * [misc]simplify:  Extracting #1: cost 3 inf + 0
1554300806.682 * * [misc]simplify:  Extracting #2: cost 4 inf + 1
1554300806.682 * * [misc]simplify:  Extracting #3: cost 6 inf + 1
1554300806.683 * * [misc]simplify:  Extracting #4: cost 0 inf + 930
1554300806.683 * [exit]simplify:  Simplified to (+.p16 a (/.p16 (real->posit16 1.0) (real->posit16 3.0)))
1554300806.683 * [misc]simplify:  Simplified (2 2 2 1 2 1 2) to (λ (a rand) (*.p16 (-.p16 a (/.p16 (real->posit16 1.0) (real->posit16 3.0))) (+.p16 (real->posit16 1) (*.p16 (/.p16 (real->posit16 1) (sqrt.p16 (/.p16 (*.p16 (real->posit16 9) (-.p16 (*.p16 a a) (*.p16 (/.p16 (real->posit16 1.0) (real->posit16 3.0)) (/.p16 (real->posit16 1.0) (real->posit16 3.0))))) (+.p16 a (/.p16 (real->posit16 1.0) (real->posit16 3.0)))))) rand))))
1554300806.683 * * * * [misc]progress:  [ 15 / 17 ] simplifiying candidate #<alt (λ (a rand) (*.p16 (-.p16 a (/.p16 (real->posit16 1.0) (real->posit16 3.0))) (+.p16 (real->posit16 1) (*.p16 (/.p16 (real->posit16 1) (sqrt.p16 (/.p16 (*.p16 (real->posit16 9) (-.p16 (*.p16 a a) (*.p16 (/.p16 (real->posit16 1.0) (real->posit16 3.0)) (/.p16 (real->posit16 1.0) (real->posit16 3.0))))) (+.p16 a (/.p16 (real->posit16 1.0) (real->posit16 3.0)))))) rand))))>
1554300806.683 * [enter]simplify:  Simplifying (+.p16 a (/.p16 (real->posit16 1.0) (real->posit16 3.0)))
1554300806.683 * * [misc]simplify:  iters left: 3 (7 enodes)
1554300806.685 * * [misc]simplify:  iters left: 2 (12 enodes)
1554300806.687 * * [misc]simplify:  Extracting #0: cost 1 inf + 0
1554300806.687 * * [misc]simplify:  Extracting #1: cost 3 inf + 0
1554300806.687 * * [misc]simplify:  Extracting #2: cost 4 inf + 1
1554300806.687 * * [misc]simplify:  Extracting #3: cost 6 inf + 1
1554300806.687 * * [misc]simplify:  Extracting #4: cost 0 inf + 930
1554300806.687 * [exit]simplify:  Simplified to (+.p16 a (/.p16 (real->posit16 1.0) (real->posit16 3.0)))
1554300806.687 * [misc]simplify:  Simplified (2 2 2 1 2 1 2) to (λ (a rand) (*.p16 (-.p16 a (/.p16 (real->posit16 1.0) (real->posit16 3.0))) (+.p16 (real->posit16 1) (*.p16 (/.p16 (real->posit16 1) (sqrt.p16 (/.p16 (*.p16 (real->posit16 9) (-.p16 (*.p16 a a) (*.p16 (/.p16 (real->posit16 1.0) (real->posit16 3.0)) (/.p16 (real->posit16 1.0) (real->posit16 3.0))))) (+.p16 a (/.p16 (real->posit16 1.0) (real->posit16 3.0)))))) rand))))
1554300806.687 * * * * [misc]progress:  [ 16 / 17 ] simplifiying candidate #<alt (λ (a rand) (*.p16 (-.p16 a (/.p16 (real->posit16 1.0) (real->posit16 3.0))) (+.p16 (real->posit16 1) (*.p16 (/.p16 (real->posit16 1) (sqrt.p16 (/.p16 (*.p16 (real->posit16 9) (-.p16 (*.p16 a a) (*.p16 (/.p16 (real->posit16 1.0) (real->posit16 3.0)) (/.p16 (real->posit16 1.0) (real->posit16 3.0))))) (+.p16 a (/.p16 (real->posit16 1.0) (real->posit16 3.0)))))) rand))))>
1554300806.687 * [enter]simplify:  Simplifying (+.p16 a (/.p16 (real->posit16 1.0) (real->posit16 3.0)))
1554300806.687 * * [misc]simplify:  iters left: 3 (7 enodes)
1554300806.689 * * [misc]simplify:  iters left: 2 (12 enodes)
1554300806.691 * * [misc]simplify:  Extracting #0: cost 1 inf + 0
1554300806.691 * * [misc]simplify:  Extracting #1: cost 3 inf + 0
1554300806.691 * * [misc]simplify:  Extracting #2: cost 4 inf + 1
1554300806.691 * * [misc]simplify:  Extracting #3: cost 6 inf + 1
1554300806.692 * * [misc]simplify:  Extracting #4: cost 0 inf + 930
1554300806.692 * [exit]simplify:  Simplified to (+.p16 a (/.p16 (real->posit16 1.0) (real->posit16 3.0)))
1554300806.692 * [misc]simplify:  Simplified (2 2 2 1 2 1 2) to (λ (a rand) (*.p16 (-.p16 a (/.p16 (real->posit16 1.0) (real->posit16 3.0))) (+.p16 (real->posit16 1) (*.p16 (/.p16 (real->posit16 1) (sqrt.p16 (/.p16 (*.p16 (real->posit16 9) (-.p16 (*.p16 a a) (*.p16 (/.p16 (real->posit16 1.0) (real->posit16 3.0)) (/.p16 (real->posit16 1.0) (real->posit16 3.0))))) (+.p16 a (/.p16 (real->posit16 1.0) (real->posit16 3.0)))))) rand))))
1554300806.692 * * * * [misc]progress:  [ 17 / 17 ] simplifiying candidate #<alt (λ (a rand) (*.p16 (-.p16 a (/.p16 (real->posit16 1.0) (real->posit16 3.0))) (+.p16 (real->posit16 1) (*.p16 (/.p16 (real->posit16 1) (sqrt.p16 (/.p16 (*.p16 (real->posit16 9) (-.p16 (*.p16 a a) (*.p16 (/.p16 (real->posit16 1.0) (real->posit16 3.0)) (/.p16 (real->posit16 1.0) (real->posit16 3.0))))) (+.p16 a (/.p16 (real->posit16 1.0) (real->posit16 3.0)))))) rand))))>
1554300806.692 * [enter]simplify:  Simplifying (+.p16 a (/.p16 (real->posit16 1.0) (real->posit16 3.0)))
1554300806.692 * * [misc]simplify:  iters left: 3 (7 enodes)
1554300806.695 * * [misc]simplify:  iters left: 2 (12 enodes)
1554300806.697 * * [misc]simplify:  Extracting #0: cost 1 inf + 0
1554300806.698 * * [misc]simplify:  Extracting #1: cost 3 inf + 0
1554300806.698 * * [misc]simplify:  Extracting #2: cost 4 inf + 1
1554300806.698 * * [misc]simplify:  Extracting #3: cost 6 inf + 1
1554300806.698 * * [misc]simplify:  Extracting #4: cost 0 inf + 930
1554300806.698 * [exit]simplify:  Simplified to (+.p16 a (/.p16 (real->posit16 1.0) (real->posit16 3.0)))
1554300806.698 * [misc]simplify:  Simplified (2 2 2 1 2 1 2) to (λ (a rand) (*.p16 (-.p16 a (/.p16 (real->posit16 1.0) (real->posit16 3.0))) (+.p16 (real->posit16 1) (*.p16 (/.p16 (real->posit16 1) (sqrt.p16 (/.p16 (*.p16 (real->posit16 9) (-.p16 (*.p16 a a) (*.p16 (/.p16 (real->posit16 1.0) (real->posit16 3.0)) (/.p16 (real->posit16 1.0) (real->posit16 3.0))))) (+.p16 a (/.p16 (real->posit16 1.0) (real->posit16 3.0)))))) rand))))
1554300806.698 * * * [misc]progress:  adding candidates to table
1554300807.481 * [misc]progress:  [Phase 3 of 3] Extracting.
1554300807.481 * * [misc]regime:  Finding splitpoints for: (#<alt (λ (a rand) (*.p16 (-.p16 a (/.p16 (real->posit16 1.0) (real->posit16 3.0))) (+.p16 (real->posit16 1) (*.p16 (/.p16 (real->posit16 1) (sqrt.p16 (/.p16 (*.p16 (real->posit16 9) (/.p16 (-.p16 (*.p16 (*.p16 a a) (*.p16 a a)) (*.p16 (*.p16 (/.p16 (real->posit16 1.0) (real->posit16 3.0)) (/.p16 (real->posit16 1.0) (real->posit16 3.0))) (*.p16 (/.p16 (real->posit16 1.0) (real->posit16 3.0)) (/.p16 (real->posit16 1.0) (real->posit16 3.0))))) (+.p16 (*.p16 a a) (*.p16 (/.p16 (real->posit16 1.0) (real->posit16 3.0)) (/.p16 (real->posit16 1.0) (real->posit16 3.0)))))) (+.p16 a (/.p16 (real->posit16 1.0) (real->posit16 3.0)))))) rand))))> #<alt (λ (a rand) (*.p16 (/.p16 (-.p16 (*.p16 a a) (*.p16 (/.p16 (real->posit16 1.0) (real->posit16 3.0)) (/.p16 (real->posit16 1.0) (real->posit16 3.0)))) (+.p16 a (/.p16 (real->posit16 1.0) (real->posit16 3.0)))) (+.p16 (real->posit16 1) (*.p16 (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 (*.p16 a (real->posit16 9)) (*.p16 (neg.p16 (/.p16 (real->posit16 1.0) (real->posit16 3.0))) (real->posit16 9))))) rand))))> #<alt (λ (a rand) (/.p16 (*.p16 (*.p16 (-.p16 a (/.p16 (real->posit16 1.0) (real->posit16 3.0))) (+.p16 a (/.p16 (real->posit16 1.0) (real->posit16 3.0)))) (+.p16 (real->posit16 1) (*.p16 (/.p16 (real->posit16 1) (sqrt.p16 (*.p16 (real->posit16 9) (-.p16 a (/.p16 (real->posit16 1.0) (real->posit16 3.0)))))) rand))) (+.p16 a (/.p16 (real->posit16 1.0) (real->posit16 3.0)))))> #<alt (λ (a rand) (+.p16 (*.p16 (real->posit16 1) (-.p16 a (/.p16 (real->posit16 1.0) (real->posit16 3.0)))) (*.p16 (/.p16 (real->posit16 1) (sqrt.p16 (*.p16 (-.p16 a (/.p16 (real->posit16 1.0) (real->posit16 3.0))) (real->posit16 9)))) (*.p16 (-.p16 a (/.p16 (real->posit16 1.0) (real->posit16 3.0))) rand))))> #<alt (λ (a rand) (*.p16 (-.p16 a (/.p16 (real->posit16 1.0) (real->posit16 3.0))) (+.p16 (real->posit16 1) (*.p16 (/.p16 (real->posit16 1) (sqrt.p16 (/.p16 (+.p16 (*.p16 (real->posit16 9) (*.p16 a a)) (*.p16 (real->posit16 9) (neg.p16 (*.p16 (/.p16 (real->posit16 1.0) (real->posit16 3.0)) (/.p16 (real->posit16 1.0) (real->posit16 3.0)))))) (+.p16 a (/.p16 (real->posit16 1.0) (real->posit16 3.0)))))) rand))))> #<alt (λ (a rand) (*.p16 (-.p16 a (/.p16 (real->posit16 1.0) (real->posit16 3.0))) (+.p16 (real->posit16 1) (*.p16 (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 (*.p16 a (real->posit16 9)) (*.p16 (neg.p16 (/.p16 (real->posit16 1.0) (real->posit16 3.0))) (real->posit16 9))))) rand))))>)
1554300807.483 * * * [misc]regime-changes:  Trying 2 branch expressions: (rand a)
1554300807.483 * * * * [misc]regimes:  Trying to branch on rand from (#<alt (λ (a rand) (*.p16 (-.p16 a (/.p16 (real->posit16 1.0) (real->posit16 3.0))) (+.p16 (real->posit16 1) (*.p16 (/.p16 (real->posit16 1) (sqrt.p16 (/.p16 (*.p16 (real->posit16 9) (/.p16 (-.p16 (*.p16 (*.p16 a a) (*.p16 a a)) (*.p16 (*.p16 (/.p16 (real->posit16 1.0) (real->posit16 3.0)) (/.p16 (real->posit16 1.0) (real->posit16 3.0))) (*.p16 (/.p16 (real->posit16 1.0) (real->posit16 3.0)) (/.p16 (real->posit16 1.0) (real->posit16 3.0))))) (+.p16 (*.p16 a a) (*.p16 (/.p16 (real->posit16 1.0) (real->posit16 3.0)) (/.p16 (real->posit16 1.0) (real->posit16 3.0)))))) (+.p16 a (/.p16 (real->posit16 1.0) (real->posit16 3.0)))))) rand))))> #<alt (λ (a rand) (*.p16 (/.p16 (-.p16 (*.p16 a a) (*.p16 (/.p16 (real->posit16 1.0) (real->posit16 3.0)) (/.p16 (real->posit16 1.0) (real->posit16 3.0)))) (+.p16 a (/.p16 (real->posit16 1.0) (real->posit16 3.0)))) (+.p16 (real->posit16 1) (*.p16 (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 (*.p16 a (real->posit16 9)) (*.p16 (neg.p16 (/.p16 (real->posit16 1.0) (real->posit16 3.0))) (real->posit16 9))))) rand))))> #<alt (λ (a rand) (/.p16 (*.p16 (*.p16 (-.p16 a (/.p16 (real->posit16 1.0) (real->posit16 3.0))) (+.p16 a (/.p16 (real->posit16 1.0) (real->posit16 3.0)))) (+.p16 (real->posit16 1) (*.p16 (/.p16 (real->posit16 1) (sqrt.p16 (*.p16 (real->posit16 9) (-.p16 a (/.p16 (real->posit16 1.0) (real->posit16 3.0)))))) rand))) (+.p16 a (/.p16 (real->posit16 1.0) (real->posit16 3.0)))))> #<alt (λ (a rand) (+.p16 (*.p16 (real->posit16 1) (-.p16 a (/.p16 (real->posit16 1.0) (real->posit16 3.0)))) (*.p16 (/.p16 (real->posit16 1) (sqrt.p16 (*.p16 (-.p16 a (/.p16 (real->posit16 1.0) (real->posit16 3.0))) (real->posit16 9)))) (*.p16 (-.p16 a (/.p16 (real->posit16 1.0) (real->posit16 3.0))) rand))))> #<alt (λ (a rand) (*.p16 (-.p16 a (/.p16 (real->posit16 1.0) (real->posit16 3.0))) (+.p16 (real->posit16 1) (*.p16 (/.p16 (real->posit16 1) (sqrt.p16 (/.p16 (+.p16 (*.p16 (real->posit16 9) (*.p16 a a)) (*.p16 (real->posit16 9) (neg.p16 (*.p16 (/.p16 (real->posit16 1.0) (real->posit16 3.0)) (/.p16 (real->posit16 1.0) (real->posit16 3.0)))))) (+.p16 a (/.p16 (real->posit16 1.0) (real->posit16 3.0)))))) rand))))> #<alt (λ (a rand) (*.p16 (-.p16 a (/.p16 (real->posit16 1.0) (real->posit16 3.0))) (+.p16 (real->posit16 1) (*.p16 (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 (*.p16 a (real->posit16 9)) (*.p16 (neg.p16 (/.p16 (real->posit16 1.0) (real->posit16 3.0))) (real->posit16 9))))) rand))))>)
1554300807.972 * * * * [misc]regimes:  Trying to branch on a from (#<alt (λ (a rand) (*.p16 (-.p16 a (/.p16 (real->posit16 1.0) (real->posit16 3.0))) (+.p16 (real->posit16 1) (*.p16 (/.p16 (real->posit16 1) (sqrt.p16 (/.p16 (*.p16 (real->posit16 9) (/.p16 (-.p16 (*.p16 (*.p16 a a) (*.p16 a a)) (*.p16 (*.p16 (/.p16 (real->posit16 1.0) (real->posit16 3.0)) (/.p16 (real->posit16 1.0) (real->posit16 3.0))) (*.p16 (/.p16 (real->posit16 1.0) (real->posit16 3.0)) (/.p16 (real->posit16 1.0) (real->posit16 3.0))))) (+.p16 (*.p16 a a) (*.p16 (/.p16 (real->posit16 1.0) (real->posit16 3.0)) (/.p16 (real->posit16 1.0) (real->posit16 3.0)))))) (+.p16 a (/.p16 (real->posit16 1.0) (real->posit16 3.0)))))) rand))))> #<alt (λ (a rand) (*.p16 (/.p16 (-.p16 (*.p16 a a) (*.p16 (/.p16 (real->posit16 1.0) (real->posit16 3.0)) (/.p16 (real->posit16 1.0) (real->posit16 3.0)))) (+.p16 a (/.p16 (real->posit16 1.0) (real->posit16 3.0)))) (+.p16 (real->posit16 1) (*.p16 (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 (*.p16 a (real->posit16 9)) (*.p16 (neg.p16 (/.p16 (real->posit16 1.0) (real->posit16 3.0))) (real->posit16 9))))) rand))))> #<alt (λ (a rand) (/.p16 (*.p16 (*.p16 (-.p16 a (/.p16 (real->posit16 1.0) (real->posit16 3.0))) (+.p16 a (/.p16 (real->posit16 1.0) (real->posit16 3.0)))) (+.p16 (real->posit16 1) (*.p16 (/.p16 (real->posit16 1) (sqrt.p16 (*.p16 (real->posit16 9) (-.p16 a (/.p16 (real->posit16 1.0) (real->posit16 3.0)))))) rand))) (+.p16 a (/.p16 (real->posit16 1.0) (real->posit16 3.0)))))> #<alt (λ (a rand) (+.p16 (*.p16 (real->posit16 1) (-.p16 a (/.p16 (real->posit16 1.0) (real->posit16 3.0)))) (*.p16 (/.p16 (real->posit16 1) (sqrt.p16 (*.p16 (-.p16 a (/.p16 (real->posit16 1.0) (real->posit16 3.0))) (real->posit16 9)))) (*.p16 (-.p16 a (/.p16 (real->posit16 1.0) (real->posit16 3.0))) rand))))> #<alt (λ (a rand) (*.p16 (-.p16 a (/.p16 (real->posit16 1.0) (real->posit16 3.0))) (+.p16 (real->posit16 1) (*.p16 (/.p16 (real->posit16 1) (sqrt.p16 (/.p16 (+.p16 (*.p16 (real->posit16 9) (*.p16 a a)) (*.p16 (real->posit16 9) (neg.p16 (*.p16 (/.p16 (real->posit16 1.0) (real->posit16 3.0)) (/.p16 (real->posit16 1.0) (real->posit16 3.0)))))) (+.p16 a (/.p16 (real->posit16 1.0) (real->posit16 3.0)))))) rand))))> #<alt (λ (a rand) (*.p16 (-.p16 a (/.p16 (real->posit16 1.0) (real->posit16 3.0))) (+.p16 (real->posit16 1) (*.p16 (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 (*.p16 a (real->posit16 9)) (*.p16 (neg.p16 (/.p16 (real->posit16 1.0) (real->posit16 3.0))) (real->posit16 9))))) rand))))>)
1554300808.213 * * * [misc]regime:  Found split indices: #<option (#s(si 5 256))>
1554300808.213 * [enter]simplify:  Simplifying (*.p16 (-.p16 a (/.p16 (real->posit16 1.0) (real->posit16 3.0))) (+.p16 (real->posit16 1) (*.p16 (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 (*.p16 a (real->posit16 9)) (*.p16 (neg.p16 (/.p16 (real->posit16 1.0) (real->posit16 3.0))) (real->posit16 9))))) rand)))
1554300808.214 * * [misc]simplify:  iters left: 6 (21 enodes)
1554300808.216 * * [misc]simplify:  iters left: 5 (23 enodes)
1554300808.219 * * [misc]simplify:  Extracting #0: cost 1 inf + 0
1554300808.219 * * [misc]simplify:  Extracting #1: cost 3 inf + 0
1554300808.219 * * [misc]simplify:  Extracting #2: cost 7 inf + 0
1554300808.219 * * [misc]simplify:  Extracting #3: cost 11 inf + 1
1554300808.219 * * [misc]simplify:  Extracting #4: cost 12 inf + 3
1554300808.219 * * [misc]simplify:  Extracting #5: cost 10 inf + 6
1554300808.219 * * [misc]simplify:  Extracting #6: cost 9 inf + 450
1554300808.219 * * [misc]simplify:  Extracting #7: cost 10 inf + 973
1554300808.220 * * [misc]simplify:  Extracting #8: cost 10 inf + 1495
1554300808.220 * * [misc]simplify:  Extracting #9: cost 9 inf + 1496
1554300808.220 * * [misc]simplify:  Extracting #10: cost 6 inf + 2662
1554300808.220 * * [misc]simplify:  Extracting #11: cost 4 inf + 5110
1554300808.221 * * [misc]simplify:  Extracting #12: cost 2 inf + 8801
1554300808.222 * * [misc]simplify:  Extracting #13: cost 0 inf + 13293
1554300808.222 * [exit]simplify:  Simplified to (*.p16 (-.p16 a (/.p16 (real->posit16 1.0) (real->posit16 3.0))) (+.p16 (real->posit16 1) (*.p16 (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 (*.p16 a (real->posit16 9)) (*.p16 (neg.p16 (/.p16 (real->posit16 1.0) (real->posit16 3.0))) (real->posit16 9))))) rand)))
1554300808.222 * * * * [misc]points:  Sampling 8000 additional inputs, on iter 0 have 0 / 8000
1554300808.255 * * * * [misc]points:  Computing exacts on every 500 of 8000 points to ramp up precision
1554300808.260 * * * * [misc]points:  Setting MPFR precision to 64
1554300808.261 * * * * [misc]points:  Setting MPFR precision to 320
1554300808.262 * * * * [misc]points:  Computing exacts on every 250 of 8000 points to ramp up precision
1554300808.267 * * * * [misc]points:  Setting MPFR precision to 64
1554300808.269 * * * * [misc]points:  Setting MPFR precision to 320
1554300808.271 * * * * [misc]points:  Computing exacts on every 125 of 8000 points to ramp up precision
1554300808.275 * * * * [misc]points:  Setting MPFR precision to 64
1554300808.279 * * * * [misc]points:  Setting MPFR precision to 320
1554300808.283 * * * * [misc]points:  Computing exacts on every 62 of 8000 points to ramp up precision
1554300808.288 * * * * [misc]points:  Setting MPFR precision to 64
1554300808.295 * * * * [misc]points:  Setting MPFR precision to 320
1554300808.302 * * * * [misc]points:  Computing exacts on every 31 of 8000 points to ramp up precision
1554300808.307 * * * * [misc]points:  Setting MPFR precision to 64
1554300808.321 * * * * [misc]points:  Setting MPFR precision to 320
1554300808.349 * * * * [misc]points:  Computing exacts on every 15 of 8000 points to ramp up precision
1554300808.356 * * * * [misc]points:  Setting MPFR precision to 64
1554300808.384 * * * * [misc]points:  Setting MPFR precision to 320
1554300808.412 * * * * [misc]points:  Computing exacts on every 7 of 8000 points to ramp up precision
1554300808.417 * * * * [misc]points:  Setting MPFR precision to 64
1554300808.506 * * * * [misc]points:  Setting MPFR precision to 320
1554300808.587 * * * * [misc]points:  Computing exacts on every 3 of 8000 points to ramp up precision
1554300808.595 * * * * [misc]points:  Setting MPFR precision to 64
1554300808.786 * * * * [misc]points:  Setting MPFR precision to 320
1554300808.986 * * * * [misc]points:  Computing exacts for 8000 points
1554300808.994 * * * * [misc]points:  Setting MPFR precision to 64
1554300809.632 * * * * [misc]points:  Setting MPFR precision to 320
1554300810.397 * * * * [misc]points:  Filtering points with unrepresentable outputs
1554300810.459 * * * * [exit]points:  Sampled 8000 points with exact outputs
1554300816.237 * [misc]regime-testing:  Baseline error score: 64.0
1554300816.239 * [misc]regime-testing:  Oracle error score: 64.0
1554300816.244 * [misc]regime-testing:  End program error score: 0.2060577834536844