0.006 * [progress]: [Phase 1 of 3] Setting up.
0.008 * * * [progress]: [1/2] Preparing points
0.010 * * * * [points]: Sampling 256 additional inputs, on iter 0 have 0 / 256
0.013 * * * * [points]: Computing exacts on every 16 of 256 points to ramp up precision
0.129 * * * * [points]: Setting MPFR precision to 64
0.133 * * * * [points]: Setting MPFR precision to 320
0.134 * * * * [points]: Computing exacts on every 8 of 256 points to ramp up precision
0.137 * * * * [points]: Setting MPFR precision to 64
0.140 * * * * [points]: Setting MPFR precision to 320
0.142 * * * * [points]: Computing exacts on every 4 of 256 points to ramp up precision
0.145 * * * * [points]: Setting MPFR precision to 64
0.149 * * * * [points]: Setting MPFR precision to 320
0.155 * * * * [points]: Computing exacts on every 2 of 256 points to ramp up precision
0.158 * * * * [points]: Setting MPFR precision to 64
0.165 * * * * [points]: Setting MPFR precision to 320
0.176 * * * * [points]: Computing exacts for 256 points
0.178 * * * * [points]: Setting MPFR precision to 64
0.196 * * * * [points]: Setting MPFR precision to 320
0.220 * * * * [points]: Filtering points with unrepresentable outputs
0.221 * * * * [points]: Sampled 256 points with exact outputs
0.222 * * * [progress]: [2/2] Setting up program.
0.284 * [progress]: [Phase 2 of 3] Improving.
0.284 * * * * [progress]: [ 1 / 1 ] simplifiying candidate #<alt (λ (a b c) (/.p16 (+.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c))))) (*.p16 (real->posit16 2) a)))>
0.286 * [simplify]: Simplifying (/.p16 (+.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c))))) (*.p16 (real->posit16 2) a))
0.287 * * [simplify]: iteration 1: (16 enodes)
0.297 * * [simplify]: iteration 2: (39 enodes)
0.312 * * [simplify]: iteration 3: (72 enodes)
0.343 * * [simplify]: iteration 4: (196 enodes)
0.473 * * [simplify]: iteration 5: (779 enodes)
1.837 * * [simplify]: Extracting #0: cost 1 inf + 0
1.837 * * [simplify]: Extracting #1: cost 5 inf + 0
1.837 * * [simplify]: Extracting #2: cost 18 inf + 1
1.838 * * [simplify]: Extracting #3: cost 44 inf + 83
1.838 * * [simplify]: Extracting #4: cost 110 inf + 2612
1.839 * * [simplify]: Extracting #5: cost 329 inf + 5940
1.841 * * [simplify]: Extracting #6: cost 753 inf + 12354
1.848 * * [simplify]: Extracting #7: cost 1123 inf + 34787
1.888 * * [simplify]: Extracting #8: cost 885 inf + 426469
2.006 * * [simplify]: Extracting #9: cost 201 inf + 2033217
2.166 * * [simplify]: Extracting #10: cost 8 inf + 2319465
2.357 * * [simplify]: Extracting #11: cost 0 inf + 2306138
2.524 * [simplify]: Simplified to (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b) (*.p16 (real->posit16 2) a))
2.524 * * * * [progress]: [ 1 / 1 ] simplifiying candidate #<alt (λ (a b c) (/.p16 (+.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c))))) (*.p16 (real->posit16 2) a)))>
2.524 * [simplify]: Simplified (2) to (λ (a b c) (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b) (*.p16 (real->posit16 2) a)))
2.557 * * [progress]: iteration 1 / 4
2.557 * * * [progress]: picking best candidate
2.574 * * * * [pick]: Picked  #<alt (λ (a b c) (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b) (*.p16 (real->posit16 2) a)))>
2.574 * * * [progress]: localizing error
2.757 * * * [progress]: generating rewritten candidates
2.757 * * * * [progress]: [ 1 / 4 ] rewriting at (2 1)
2.760 * * * * [progress]: [ 2 / 4 ] rewriting at (2)
2.764 * * * * [progress]: [ 3 / 4 ] rewriting at (2 1 1 1)
2.768 * * * * [progress]: [ 4 / 4 ] rewriting at (2 1 1)
2.770 * * * [progress]: generating series expansions
2.770 * * * * [progress]: [ 1 / 4 ] generating series at (2 1)
2.770 * * * * [progress]: [ 2 / 4 ] generating series at (2)
2.770 * * * * [progress]: [ 3 / 4 ] generating series at (2 1 1 1)
2.770 * * * * [progress]: [ 4 / 4 ] generating series at (2 1 1)
2.770 * * * [progress]: simplifying candidates
2.770 * * * * [progress]: [ 1 / 10 ] simplifiying candidate #<alt (λ (a b c) (/.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) (neg.p16 b)) (*.p16 (real->posit16 2) a)))>
2.770 * * * * [progress]: [ 2 / 10 ] simplifiying candidate #<alt (λ (a b c) (/.p16 (/.p16 (-.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4))))) (*.p16 b b)) (+.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b)) (*.p16 (real->posit16 2) a)))>
2.770 * * * * [progress]: [ 3 / 10 ] simplifiying candidate #<alt (λ (a b c) (/.p16 (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b) (real->posit16 2)) a))>
2.770 * * * * [progress]: [ 4 / 10 ] simplifiying candidate #<alt (λ (a b c) (/.p16 (-.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4))))) (*.p16 b b)) (*.p16 (*.p16 (real->posit16 2) a) (+.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b))))>
2.770 * * * * [progress]: [ 5 / 10 ] simplifiying candidate #<alt (λ (a b c) (/.p16 (-.p16 (sqrt.p16 (+.p16 (*.p16 b b) (neg.p16 (*.p16 (*.p16 c a) (real->posit16 4))))) b) (*.p16 (real->posit16 2) a)))>
2.770 * * * * [progress]: [ 6 / 10 ] simplifiying candidate #<alt (λ (a b c) (/.p16 (-.p16 (sqrt.p16 (/.p16 (-.p16 (*.p16 (*.p16 b b) (*.p16 b b)) (*.p16 (*.p16 (*.p16 c a) (real->posit16 4)) (*.p16 (*.p16 c a) (real->posit16 4)))) (+.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4))))) b) (*.p16 (real->posit16 2) a)))>
2.771 * * * * [progress]: [ 7 / 10 ] simplifiying candidate #<alt (λ (a b c) (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b) (*.p16 (real->posit16 2) a)))>
2.771 * * * * [progress]: [ 8 / 10 ] simplifiying candidate #<alt (λ (a b c) (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b) (*.p16 (real->posit16 2) a)))>
2.771 * * * * [progress]: [ 9 / 10 ] simplifiying candidate #<alt (λ (a b c) (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b) (*.p16 (real->posit16 2) a)))>
2.771 * * * * [progress]: [ 10 / 10 ] simplifiying candidate #<alt (λ (a b c) (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b) (*.p16 (real->posit16 2) a)))>
2.771 * [simplify]: Simplifying (neg.p16 b), (-.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4))))) (*.p16 b b)), (+.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b), (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b) (real->posit16 2)), (*.p16 (*.p16 (real->posit16 2) a) (+.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b)), (neg.p16 (*.p16 (*.p16 c a) (real->posit16 4))), (-.p16 (*.p16 (*.p16 b b) (*.p16 b b)) (*.p16 (*.p16 (*.p16 c a) (real->posit16 4)) (*.p16 (*.p16 c a) (real->posit16 4)))), (+.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4))), (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b) (*.p16 (real->posit16 2) a)), (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b) (*.p16 (real->posit16 2) a)), (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b) (*.p16 (real->posit16 2) a)), (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b) (*.p16 (real->posit16 2) a))
2.771 * * [simplify]: iteration 1: (26 enodes)
2.778 * * [simplify]: iteration 2: (78 enodes)
2.795 * * [simplify]: iteration 3: (228 enodes)
2.866 * * [simplify]: iteration 4: (901 enodes)
3.696 * * [simplify]: Extracting #0: cost 9 inf + 0
3.697 * * [simplify]: Extracting #1: cost 291 inf + 0
3.702 * * [simplify]: Extracting #2: cost 944 inf + 2248
3.712 * * [simplify]: Extracting #3: cost 1457 inf + 9871
3.729 * * [simplify]: Extracting #4: cost 1868 inf + 38653
3.784 * * [simplify]: Extracting #5: cost 1515 inf + 638793
3.923 * * [simplify]: Extracting #6: cost 466 inf + 2863153
4.228 * * [simplify]: Extracting #7: cost 12 inf + 3986234
4.498 * * [simplify]: Extracting #8: cost 0 inf + 4009041
4.791 * [simplify]: Simplified to (neg.p16 b), (-.p16 (real->posit16 0.0) (*.p16 (*.p16 a c) (real->posit16 4))), (+.p16 b (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 a c) (real->posit16 4))))), (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 a c) (real->posit16 4)))) b) (real->posit16 2)), (*.p16 (*.p16 (+.p16 b (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 a c) (real->posit16 4))))) a) (real->posit16 2)), (neg.p16 (*.p16 (*.p16 a c) (real->posit16 4))), (*.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 a c) (real->posit16 4))) (+.p16 (*.p16 (*.p16 a c) (real->posit16 4)) (*.p16 b b))), (+.p16 (*.p16 (*.p16 a c) (real->posit16 4)) (*.p16 b b)), (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 a c) (real->posit16 4)))) b) (*.p16 (real->posit16 2) a)), (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 a c) (real->posit16 4)))) b) (*.p16 (real->posit16 2) a)), (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 a c) (real->posit16 4)))) b) (*.p16 (real->posit16 2) a)), (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 a c) (real->posit16 4)))) b) (*.p16 (real->posit16 2) a))
4.791 * * * * [progress]: [ 1 / 10 ] simplifiying candidate #<alt (λ (a b c) (/.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) (neg.p16 b)) (*.p16 (real->posit16 2) a)))>
4.791 * [simplify]: Simplified (2 1 2) to (λ (a b c) (/.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) (neg.p16 b)) (*.p16 (real->posit16 2) a)))
4.791 * * * * [progress]: [ 2 / 10 ] simplifiying candidate #<alt (λ (a b c) (/.p16 (/.p16 (-.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4))))) (*.p16 b b)) (+.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b)) (*.p16 (real->posit16 2) a)))>
4.791 * [simplify]: Simplified (2 1 1) to (λ (a b c) (/.p16 (/.p16 (-.p16 (real->posit16 0.0) (*.p16 (*.p16 a c) (real->posit16 4))) (+.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b)) (*.p16 (real->posit16 2) a)))
4.792 * [simplify]: Simplified (2 1 2) to (λ (a b c) (/.p16 (/.p16 (-.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4))))) (*.p16 b b)) (+.p16 b (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 a c) (real->posit16 4)))))) (*.p16 (real->posit16 2) a)))
4.792 * * * * [progress]: [ 3 / 10 ] simplifiying candidate #<alt (λ (a b c) (/.p16 (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b) (real->posit16 2)) a))>
4.792 * [simplify]: Simplified (2 1) to (λ (a b c) (/.p16 (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 a c) (real->posit16 4)))) b) (real->posit16 2)) a))
4.792 * * * * [progress]: [ 4 / 10 ] simplifiying candidate #<alt (λ (a b c) (/.p16 (-.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4))))) (*.p16 b b)) (*.p16 (*.p16 (real->posit16 2) a) (+.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b))))>
4.792 * [simplify]: Simplified (2 2) to (λ (a b c) (/.p16 (-.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4))))) (*.p16 b b)) (*.p16 (*.p16 (+.p16 b (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 a c) (real->posit16 4))))) a) (real->posit16 2))))
4.792 * * * * [progress]: [ 5 / 10 ] simplifiying candidate #<alt (λ (a b c) (/.p16 (-.p16 (sqrt.p16 (+.p16 (*.p16 b b) (neg.p16 (*.p16 (*.p16 c a) (real->posit16 4))))) b) (*.p16 (real->posit16 2) a)))>
4.792 * [simplify]: Simplified (2 1 1 1 2) to (λ (a b c) (/.p16 (-.p16 (sqrt.p16 (+.p16 (*.p16 b b) (neg.p16 (*.p16 (*.p16 a c) (real->posit16 4))))) b) (*.p16 (real->posit16 2) a)))
4.792 * * * * [progress]: [ 6 / 10 ] simplifiying candidate #<alt (λ (a b c) (/.p16 (-.p16 (sqrt.p16 (/.p16 (-.p16 (*.p16 (*.p16 b b) (*.p16 b b)) (*.p16 (*.p16 (*.p16 c a) (real->posit16 4)) (*.p16 (*.p16 c a) (real->posit16 4)))) (+.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4))))) b) (*.p16 (real->posit16 2) a)))>
4.792 * [simplify]: Simplified (2 1 1 1 1) to (λ (a b c) (/.p16 (-.p16 (sqrt.p16 (/.p16 (*.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 a c) (real->posit16 4))) (+.p16 (*.p16 (*.p16 a c) (real->posit16 4)) (*.p16 b b))) (+.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4))))) b) (*.p16 (real->posit16 2) a)))
4.792 * [simplify]: Simplified (2 1 1 1 2) to (λ (a b c) (/.p16 (-.p16 (sqrt.p16 (/.p16 (-.p16 (*.p16 (*.p16 b b) (*.p16 b b)) (*.p16 (*.p16 (*.p16 c a) (real->posit16 4)) (*.p16 (*.p16 c a) (real->posit16 4)))) (+.p16 (*.p16 (*.p16 a c) (real->posit16 4)) (*.p16 b b)))) b) (*.p16 (real->posit16 2) a)))
4.792 * * * * [progress]: [ 7 / 10 ] simplifiying candidate #<alt (λ (a b c) (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b) (*.p16 (real->posit16 2) a)))>
4.792 * [simplify]: Simplified (2) to (λ (a b c) (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 a c) (real->posit16 4)))) b) (*.p16 (real->posit16 2) a)))
4.792 * * * * [progress]: [ 8 / 10 ] simplifiying candidate #<alt (λ (a b c) (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b) (*.p16 (real->posit16 2) a)))>
4.792 * [simplify]: Simplified (2) to (λ (a b c) (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 a c) (real->posit16 4)))) b) (*.p16 (real->posit16 2) a)))
4.793 * * * * [progress]: [ 9 / 10 ] simplifiying candidate #<alt (λ (a b c) (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b) (*.p16 (real->posit16 2) a)))>
4.793 * [simplify]: Simplified (2) to (λ (a b c) (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 a c) (real->posit16 4)))) b) (*.p16 (real->posit16 2) a)))
4.793 * * * * [progress]: [ 10 / 10 ] simplifiying candidate #<alt (λ (a b c) (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b) (*.p16 (real->posit16 2) a)))>
4.793 * [simplify]: Simplified (2) to (λ (a b c) (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 a c) (real->posit16 4)))) b) (*.p16 (real->posit16 2) a)))
4.793 * * * [progress]: adding candidates to table
5.130 * * [progress]: iteration 2 / 4
5.130 * * * [progress]: picking best candidate
5.213 * * * * [pick]: Picked  #<alt (λ (a b c) (/.p16 (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b) (real->posit16 2)) a))>
5.213 * * * [progress]: localizing error
5.523 * * * [progress]: generating rewritten candidates
5.524 * * * * [progress]: [ 1 / 4 ] rewriting at (2 1 1)
5.525 * * * * [progress]: [ 2 / 4 ] rewriting at (2 1 1 1 1)
5.530 * * * * [progress]: [ 3 / 4 ] rewriting at (2 1 1 1)
5.530 * * * * [progress]: [ 4 / 4 ] rewriting at (2 1 1 1 1 2)
5.533 * * * [progress]: generating series expansions
5.534 * * * * [progress]: [ 1 / 4 ] generating series at (2 1 1)
5.534 * * * * [progress]: [ 2 / 4 ] generating series at (2 1 1 1 1)
5.534 * * * * [progress]: [ 3 / 4 ] generating series at (2 1 1 1)
5.534 * * * * [progress]: [ 4 / 4 ] generating series at (2 1 1 1 1 2)
5.534 * * * [progress]: simplifying candidates
5.534 * * * * [progress]: [ 1 / 10 ] simplifiying candidate #<alt (λ (a b c) (/.p16 (/.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) (neg.p16 b)) (real->posit16 2)) a))>
5.534 * * * * [progress]: [ 2 / 10 ] simplifiying candidate #<alt (λ (a b c) (/.p16 (/.p16 (/.p16 (-.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4))))) (*.p16 b b)) (+.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b)) (real->posit16 2)) a))>
5.534 * * * * [progress]: [ 3 / 10 ] simplifiying candidate #<alt (λ (a b c) (/.p16 (/.p16 (-.p16 (sqrt.p16 (+.p16 (*.p16 b b) (neg.p16 (*.p16 (*.p16 c a) (real->posit16 4))))) b) (real->posit16 2)) a))>
5.534 * * * * [progress]: [ 4 / 10 ] simplifiying candidate #<alt (λ (a b c) (/.p16 (/.p16 (-.p16 (sqrt.p16 (/.p16 (-.p16 (*.p16 (*.p16 b b) (*.p16 b b)) (*.p16 (*.p16 (*.p16 c a) (real->posit16 4)) (*.p16 (*.p16 c a) (real->posit16 4)))) (+.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4))))) b) (real->posit16 2)) a))>
5.534 * * * * [progress]: [ 5 / 10 ] simplifiying candidate #<alt (λ (a b c) (/.p16 (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4))))) b) (real->posit16 2)) a))>
5.534 * * * * [progress]: [ 6 / 10 ] simplifiying candidate #<alt (λ (a b c) (/.p16 (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 c a)))) b) (real->posit16 2)) a))>
5.534 * * * * [progress]: [ 7 / 10 ] simplifiying candidate #<alt (λ (a b c) (/.p16 (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b) (real->posit16 2)) a))>
5.534 * * * * [progress]: [ 8 / 10 ] simplifiying candidate #<alt (λ (a b c) (/.p16 (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b) (real->posit16 2)) a))>
5.534 * * * * [progress]: [ 9 / 10 ] simplifiying candidate #<alt (λ (a b c) (/.p16 (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b) (real->posit16 2)) a))>
5.534 * * * * [progress]: [ 10 / 10 ] simplifiying candidate #<alt (λ (a b c) (/.p16 (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b) (real->posit16 2)) a))>
5.534 * [simplify]: Simplifying (neg.p16 b), (-.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4))))) (*.p16 b b)), (+.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b), (neg.p16 (*.p16 (*.p16 c a) (real->posit16 4))), (-.p16 (*.p16 (*.p16 b b) (*.p16 b b)) (*.p16 (*.p16 (*.p16 c a) (real->posit16 4)) (*.p16 (*.p16 c a) (real->posit16 4)))), (+.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4))), (*.p16 a (real->posit16 4)), (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b) (real->posit16 2)), (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b) (real->posit16 2)), (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b) (real->posit16 2)), (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b) (real->posit16 2))
5.535 * * [simplify]: iteration 1: (24 enodes)
5.547 * * [simplify]: iteration 2: (65 enodes)
5.569 * * [simplify]: iteration 3: (185 enodes)
5.649 * * [simplify]: iteration 4: (838 enodes)
6.429 * * [simplify]: Extracting #0: cost 8 inf + 0
6.430 * * [simplify]: Extracting #1: cost 188 inf + 0
6.434 * * [simplify]: Extracting #2: cost 791 inf + 2328
6.438 * * [simplify]: Extracting #3: cost 1267 inf + 16377
6.462 * * [simplify]: Extracting #4: cost 1396 inf + 578636
6.607 * * [simplify]: Extracting #5: cost 570 inf + 2453345
6.866 * * [simplify]: Extracting #6: cost 108 inf + 3475578
7.165 * * [simplify]: Extracting #7: cost 2 inf + 3688944
7.426 * * [simplify]: Extracting #8: cost 0 inf + 3693992
7.721 * [simplify]: Simplified to (neg.p16 b), (-.p16 (real->posit16 0.0) (*.p16 a (*.p16 (real->posit16 4) c))), (+.p16 b (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 a (*.p16 (real->posit16 4) c))))), (neg.p16 (*.p16 a (*.p16 (real->posit16 4) c))), (*.p16 (+.p16 (*.p16 a (*.p16 (real->posit16 4) c)) (*.p16 b b)) (-.p16 (*.p16 b b) (*.p16 a (*.p16 (real->posit16 4) c)))), (+.p16 (*.p16 a (*.p16 (real->posit16 4) c)) (*.p16 b b)), (*.p16 (real->posit16 4) a), (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 a (*.p16 (real->posit16 4) c)))) b) (real->posit16 2)), (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 a (*.p16 (real->posit16 4) c)))) b) (real->posit16 2)), (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 a (*.p16 (real->posit16 4) c)))) b) (real->posit16 2)), (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 a (*.p16 (real->posit16 4) c)))) b) (real->posit16 2))
7.721 * * * * [progress]: [ 1 / 10 ] simplifiying candidate #<alt (λ (a b c) (/.p16 (/.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) (neg.p16 b)) (real->posit16 2)) a))>
7.721 * [simplify]: Simplified (2 1 1 2) to (λ (a b c) (/.p16 (/.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) (neg.p16 b)) (real->posit16 2)) a))
7.722 * * * * [progress]: [ 2 / 10 ] simplifiying candidate #<alt (λ (a b c) (/.p16 (/.p16 (/.p16 (-.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4))))) (*.p16 b b)) (+.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b)) (real->posit16 2)) a))>
7.722 * [simplify]: Simplified (2 1 1 1) to (λ (a b c) (/.p16 (/.p16 (/.p16 (-.p16 (real->posit16 0.0) (*.p16 a (*.p16 (real->posit16 4) c))) (+.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b)) (real->posit16 2)) a))
7.722 * [simplify]: Simplified (2 1 1 2) to (λ (a b c) (/.p16 (/.p16 (/.p16 (-.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4))))) (*.p16 b b)) (+.p16 b (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 a (*.p16 (real->posit16 4) c)))))) (real->posit16 2)) a))
7.722 * * * * [progress]: [ 3 / 10 ] simplifiying candidate #<alt (λ (a b c) (/.p16 (/.p16 (-.p16 (sqrt.p16 (+.p16 (*.p16 b b) (neg.p16 (*.p16 (*.p16 c a) (real->posit16 4))))) b) (real->posit16 2)) a))>
7.722 * [simplify]: Simplified (2 1 1 1 1 2) to (λ (a b c) (/.p16 (/.p16 (-.p16 (sqrt.p16 (+.p16 (*.p16 b b) (neg.p16 (*.p16 a (*.p16 (real->posit16 4) c))))) b) (real->posit16 2)) a))
7.722 * * * * [progress]: [ 4 / 10 ] simplifiying candidate #<alt (λ (a b c) (/.p16 (/.p16 (-.p16 (sqrt.p16 (/.p16 (-.p16 (*.p16 (*.p16 b b) (*.p16 b b)) (*.p16 (*.p16 (*.p16 c a) (real->posit16 4)) (*.p16 (*.p16 c a) (real->posit16 4)))) (+.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4))))) b) (real->posit16 2)) a))>
7.722 * [simplify]: Simplified (2 1 1 1 1 1) to (λ (a b c) (/.p16 (/.p16 (-.p16 (sqrt.p16 (/.p16 (*.p16 (+.p16 (*.p16 a (*.p16 (real->posit16 4) c)) (*.p16 b b)) (-.p16 (*.p16 b b) (*.p16 a (*.p16 (real->posit16 4) c)))) (+.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4))))) b) (real->posit16 2)) a))
7.722 * [simplify]: Simplified (2 1 1 1 1 2) to (λ (a b c) (/.p16 (/.p16 (-.p16 (sqrt.p16 (/.p16 (-.p16 (*.p16 (*.p16 b b) (*.p16 b b)) (*.p16 (*.p16 (*.p16 c a) (real->posit16 4)) (*.p16 (*.p16 c a) (real->posit16 4)))) (+.p16 (*.p16 a (*.p16 (real->posit16 4) c)) (*.p16 b b)))) b) (real->posit16 2)) a))
7.722 * * * * [progress]: [ 5 / 10 ] simplifiying candidate #<alt (λ (a b c) (/.p16 (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4))))) b) (real->posit16 2)) a))>
7.722 * [simplify]: Simplified (2 1 1 1 1 2 2) to (λ (a b c) (/.p16 (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 c (*.p16 (real->posit16 4) a)))) b) (real->posit16 2)) a))
7.722 * * * * [progress]: [ 6 / 10 ] simplifiying candidate #<alt (λ (a b c) (/.p16 (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 c a)))) b) (real->posit16 2)) a))>
7.722 * * * * [progress]: [ 7 / 10 ] simplifiying candidate #<alt (λ (a b c) (/.p16 (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b) (real->posit16 2)) a))>
7.722 * [simplify]: Simplified (2 1) to (λ (a b c) (/.p16 (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 a (*.p16 (real->posit16 4) c)))) b) (real->posit16 2)) a))
7.722 * * * * [progress]: [ 8 / 10 ] simplifiying candidate #<alt (λ (a b c) (/.p16 (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b) (real->posit16 2)) a))>
7.723 * [simplify]: Simplified (2 1) to (λ (a b c) (/.p16 (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 a (*.p16 (real->posit16 4) c)))) b) (real->posit16 2)) a))
7.723 * * * * [progress]: [ 9 / 10 ] simplifiying candidate #<alt (λ (a b c) (/.p16 (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b) (real->posit16 2)) a))>
7.723 * [simplify]: Simplified (2 1) to (λ (a b c) (/.p16 (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 a (*.p16 (real->posit16 4) c)))) b) (real->posit16 2)) a))
7.723 * * * * [progress]: [ 10 / 10 ] simplifiying candidate #<alt (λ (a b c) (/.p16 (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b) (real->posit16 2)) a))>
7.723 * [simplify]: Simplified (2 1) to (λ (a b c) (/.p16 (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 a (*.p16 (real->posit16 4) c)))) b) (real->posit16 2)) a))
7.723 * * * [progress]: adding candidates to table
8.137 * * [progress]: iteration 3 / 4
8.137 * * * [progress]: picking best candidate
8.234 * * * * [pick]: Picked  #<alt (λ (a b c) (/.p16 (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4))))) b) (real->posit16 2)) a))>
8.235 * * * [progress]: localizing error
8.491 * * * [progress]: generating rewritten candidates
8.491 * * * * [progress]: [ 1 / 4 ] rewriting at (2 1 1)
8.493 * * * * [progress]: [ 2 / 4 ] rewriting at (2 1 1 1 1)
8.498 * * * * [progress]: [ 3 / 4 ] rewriting at (2 1 1 1)
8.498 * * * * [progress]: [ 4 / 4 ] rewriting at (2)
8.502 * * * [progress]: generating series expansions
8.502 * * * * [progress]: [ 1 / 4 ] generating series at (2 1 1)
8.502 * * * * [progress]: [ 2 / 4 ] generating series at (2 1 1 1 1)
8.502 * * * * [progress]: [ 3 / 4 ] generating series at (2 1 1 1)
8.502 * * * * [progress]: [ 4 / 4 ] generating series at (2)
8.502 * * * [progress]: simplifying candidates
8.502 * * * * [progress]: [ 1 / 9 ] simplifiying candidate #<alt (λ (a b c) (/.p16 (/.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4))))) (neg.p16 b)) (real->posit16 2)) a))>
8.502 * * * * [progress]: [ 2 / 9 ] simplifiying candidate #<alt (λ (a b c) (/.p16 (/.p16 (/.p16 (-.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4))))) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4)))))) (*.p16 b b)) (+.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4))))) b)) (real->posit16 2)) a))>
8.502 * * * * [progress]: [ 3 / 9 ] simplifiying candidate #<alt (λ (a b c) (/.p16 (/.p16 (-.p16 (sqrt.p16 (+.p16 (*.p16 b b) (neg.p16 (*.p16 c (*.p16 a (real->posit16 4)))))) b) (real->posit16 2)) a))>
8.502 * * * * [progress]: [ 4 / 9 ] simplifiying candidate #<alt (λ (a b c) (/.p16 (/.p16 (-.p16 (sqrt.p16 (/.p16 (-.p16 (*.p16 (*.p16 b b) (*.p16 b b)) (*.p16 (*.p16 c (*.p16 a (real->posit16 4))) (*.p16 c (*.p16 a (real->posit16 4))))) (+.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4)))))) b) (real->posit16 2)) a))>
8.502 * * * * [progress]: [ 5 / 9 ] simplifiying candidate #<alt (λ (a b c) (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4))))) b) (*.p16 a (real->posit16 2))))>
8.502 * * * * [progress]: [ 6 / 9 ] simplifiying candidate #<alt (λ (a b c) (/.p16 (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4))))) b) (real->posit16 2)) a))>
8.502 * * * * [progress]: [ 7 / 9 ] simplifiying candidate #<alt (λ (a b c) (/.p16 (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4))))) b) (real->posit16 2)) a))>
8.502 * * * * [progress]: [ 8 / 9 ] simplifiying candidate #<alt (λ (a b c) (/.p16 (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4))))) b) (real->posit16 2)) a))>
8.502 * * * * [progress]: [ 9 / 9 ] simplifiying candidate #<alt (λ (a b c) (/.p16 (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4))))) b) (real->posit16 2)) a))>
8.502 * [simplify]: Simplifying (neg.p16 b), (-.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4))))) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4)))))) (*.p16 b b)), (+.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4))))) b), (neg.p16 (*.p16 c (*.p16 a (real->posit16 4)))), (-.p16 (*.p16 (*.p16 b b) (*.p16 b b)) (*.p16 (*.p16 c (*.p16 a (real->posit16 4))) (*.p16 c (*.p16 a (real->posit16 4))))), (+.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4)))), (*.p16 a (real->posit16 2)), (*.p16 a (real->posit16 4)), (*.p16 a (real->posit16 4)), (*.p16 a (real->posit16 4)), (*.p16 a (real->posit16 4))
8.503 * * [simplify]: iteration 1: (22 enodes)
8.508 * * [simplify]: iteration 2: (63 enodes)
8.520 * * [simplify]: iteration 3: (175 enodes)
8.589 * * [simplify]: iteration 4: (778 enodes)
9.423 * * [simplify]: Extracting #0: cost 8 inf + 0
9.423 * * [simplify]: Extracting #1: cost 120 inf + 0
9.425 * * [simplify]: Extracting #2: cost 609 inf + 805
9.435 * * [simplify]: Extracting #3: cost 912 inf + 206694
9.556 * * [simplify]: Extracting #4: cost 768 inf + 1468852
9.801 * * [simplify]: Extracting #5: cost 58 inf + 3119886
10.105 * * [simplify]: Extracting #6: cost 0 inf + 3259661
10.304 * [simplify]: Simplified to (neg.p16 b), (-.p16 (real->posit16 0.0) (*.p16 (*.p16 a (real->posit16 4)) c)), (+.p16 b (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 a (real->posit16 4)) c)))), (neg.p16 (*.p16 (*.p16 a (real->posit16 4)) c)), (*.p16 (+.p16 (*.p16 (*.p16 a (real->posit16 4)) c) (*.p16 b b)) (-.p16 (*.p16 b b) (*.p16 (*.p16 a (real->posit16 4)) c))), (+.p16 (*.p16 (*.p16 a (real->posit16 4)) c) (*.p16 b b)), (*.p16 (real->posit16 2) a), (*.p16 a (real->posit16 4)), (*.p16 a (real->posit16 4)), (*.p16 a (real->posit16 4)), (*.p16 a (real->posit16 4))
10.304 * * * * [progress]: [ 1 / 9 ] simplifiying candidate #<alt (λ (a b c) (/.p16 (/.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4))))) (neg.p16 b)) (real->posit16 2)) a))>
10.304 * [simplify]: Simplified (2 1 1 2) to (λ (a b c) (/.p16 (/.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4))))) (neg.p16 b)) (real->posit16 2)) a))
10.305 * * * * [progress]: [ 2 / 9 ] simplifiying candidate #<alt (λ (a b c) (/.p16 (/.p16 (/.p16 (-.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4))))) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4)))))) (*.p16 b b)) (+.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4))))) b)) (real->posit16 2)) a))>
10.305 * [simplify]: Simplified (2 1 1 1) to (λ (a b c) (/.p16 (/.p16 (/.p16 (-.p16 (real->posit16 0.0) (*.p16 (*.p16 a (real->posit16 4)) c)) (+.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4))))) b)) (real->posit16 2)) a))
10.305 * [simplify]: Simplified (2 1 1 2) to (λ (a b c) (/.p16 (/.p16 (/.p16 (-.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4))))) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4)))))) (*.p16 b b)) (+.p16 b (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 a (real->posit16 4)) c))))) (real->posit16 2)) a))
10.305 * * * * [progress]: [ 3 / 9 ] simplifiying candidate #<alt (λ (a b c) (/.p16 (/.p16 (-.p16 (sqrt.p16 (+.p16 (*.p16 b b) (neg.p16 (*.p16 c (*.p16 a (real->posit16 4)))))) b) (real->posit16 2)) a))>
10.305 * [simplify]: Simplified (2 1 1 1 1 2) to (λ (a b c) (/.p16 (/.p16 (-.p16 (sqrt.p16 (+.p16 (*.p16 b b) (neg.p16 (*.p16 (*.p16 a (real->posit16 4)) c)))) b) (real->posit16 2)) a))
10.305 * * * * [progress]: [ 4 / 9 ] simplifiying candidate #<alt (λ (a b c) (/.p16 (/.p16 (-.p16 (sqrt.p16 (/.p16 (-.p16 (*.p16 (*.p16 b b) (*.p16 b b)) (*.p16 (*.p16 c (*.p16 a (real->posit16 4))) (*.p16 c (*.p16 a (real->posit16 4))))) (+.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4)))))) b) (real->posit16 2)) a))>
10.305 * [simplify]: Simplified (2 1 1 1 1 1) to (λ (a b c) (/.p16 (/.p16 (-.p16 (sqrt.p16 (/.p16 (*.p16 (+.p16 (*.p16 (*.p16 a (real->posit16 4)) c) (*.p16 b b)) (-.p16 (*.p16 b b) (*.p16 (*.p16 a (real->posit16 4)) c))) (+.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4)))))) b) (real->posit16 2)) a))
10.306 * [simplify]: Simplified (2 1 1 1 1 2) to (λ (a b c) (/.p16 (/.p16 (-.p16 (sqrt.p16 (/.p16 (-.p16 (*.p16 (*.p16 b b) (*.p16 b b)) (*.p16 (*.p16 c (*.p16 a (real->posit16 4))) (*.p16 c (*.p16 a (real->posit16 4))))) (+.p16 (*.p16 (*.p16 a (real->posit16 4)) c) (*.p16 b b)))) b) (real->posit16 2)) a))
10.306 * * * * [progress]: [ 5 / 9 ] simplifiying candidate #<alt (λ (a b c) (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4))))) b) (*.p16 a (real->posit16 2))))>
10.306 * [simplify]: Simplified (2 2) to (λ (a b c) (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4))))) b) (*.p16 (real->posit16 2) a)))
10.306 * * * * [progress]: [ 6 / 9 ] simplifiying candidate #<alt (λ (a b c) (/.p16 (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4))))) b) (real->posit16 2)) a))>
10.306 * [simplify]: Simplified (2 1 1 1 1 2 2) to (λ (a b c) (/.p16 (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4))))) b) (real->posit16 2)) a))
10.306 * * * * [progress]: [ 7 / 9 ] simplifiying candidate #<alt (λ (a b c) (/.p16 (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4))))) b) (real->posit16 2)) a))>
10.306 * [simplify]: Simplified (2 1 1 1 1 2 2) to (λ (a b c) (/.p16 (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4))))) b) (real->posit16 2)) a))
10.306 * * * * [progress]: [ 8 / 9 ] simplifiying candidate #<alt (λ (a b c) (/.p16 (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4))))) b) (real->posit16 2)) a))>
10.306 * [simplify]: Simplified (2 1 1 1 1 2 2) to (λ (a b c) (/.p16 (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4))))) b) (real->posit16 2)) a))
10.307 * * * * [progress]: [ 9 / 9 ] simplifiying candidate #<alt (λ (a b c) (/.p16 (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4))))) b) (real->posit16 2)) a))>
10.307 * [simplify]: Simplified (2 1 1 1 1 2 2) to (λ (a b c) (/.p16 (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4))))) b) (real->posit16 2)) a))
10.307 * * * [progress]: adding candidates to table
10.677 * * [progress]: iteration 4 / 4
10.677 * * * [progress]: picking best candidate
10.751 * * * * [pick]: Picked  #<alt (λ (a b c) (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4))))) b) (*.p16 a (real->posit16 2))))>
10.751 * * * [progress]: localizing error
10.945 * * * [progress]: generating rewritten candidates
10.945 * * * * [progress]: [ 1 / 4 ] rewriting at (2 1)
10.947 * * * * [progress]: [ 2 / 4 ] rewriting at (2)
10.951 * * * * [progress]: [ 3 / 4 ] rewriting at (2 1 1 1)
10.956 * * * * [progress]: [ 4 / 4 ] rewriting at (2 1 1)
10.956 * * * [progress]: generating series expansions
10.956 * * * * [progress]: [ 1 / 4 ] generating series at (2 1)
10.956 * * * * [progress]: [ 2 / 4 ] generating series at (2)
10.956 * * * * [progress]: [ 3 / 4 ] generating series at (2 1 1 1)
10.956 * * * * [progress]: [ 4 / 4 ] generating series at (2 1 1)
10.956 * * * [progress]: simplifying candidates
10.956 * * * * [progress]: [ 1 / 10 ] simplifiying candidate #<alt (λ (a b c) (/.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4))))) (neg.p16 b)) (*.p16 a (real->posit16 2))))>
10.956 * * * * [progress]: [ 2 / 10 ] simplifiying candidate #<alt (λ (a b c) (/.p16 (/.p16 (-.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4))))) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4)))))) (*.p16 b b)) (+.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4))))) b)) (*.p16 a (real->posit16 2))))>
10.956 * * * * [progress]: [ 3 / 10 ] simplifiying candidate #<alt (λ (a b c) (/.p16 (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4))))) b) a) (real->posit16 2)))>
10.956 * * * * [progress]: [ 4 / 10 ] simplifiying candidate #<alt (λ (a b c) (/.p16 (-.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4))))) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4)))))) (*.p16 b b)) (*.p16 (*.p16 a (real->posit16 2)) (+.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4))))) b))))>
10.956 * * * * [progress]: [ 5 / 10 ] simplifiying candidate #<alt (λ (a b c) (/.p16 (-.p16 (sqrt.p16 (+.p16 (*.p16 b b) (neg.p16 (*.p16 c (*.p16 a (real->posit16 4)))))) b) (*.p16 a (real->posit16 2))))>
10.956 * * * * [progress]: [ 6 / 10 ] simplifiying candidate #<alt (λ (a b c) (/.p16 (-.p16 (sqrt.p16 (/.p16 (-.p16 (*.p16 (*.p16 b b) (*.p16 b b)) (*.p16 (*.p16 c (*.p16 a (real->posit16 4))) (*.p16 c (*.p16 a (real->posit16 4))))) (+.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4)))))) b) (*.p16 a (real->posit16 2))))>
10.956 * * * * [progress]: [ 7 / 10 ] simplifiying candidate #<alt (λ (a b c) (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4))))) b) (*.p16 a (real->posit16 2))))>
10.956 * * * * [progress]: [ 8 / 10 ] simplifiying candidate #<alt (λ (a b c) (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4))))) b) (*.p16 a (real->posit16 2))))>
10.957 * * * * [progress]: [ 9 / 10 ] simplifiying candidate #<alt (λ (a b c) (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4))))) b) (*.p16 a (real->posit16 2))))>
10.957 * * * * [progress]: [ 10 / 10 ] simplifiying candidate #<alt (λ (a b c) (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4))))) b) (*.p16 a (real->posit16 2))))>
10.957 * [simplify]: Simplifying (neg.p16 b), (-.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4))))) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4)))))) (*.p16 b b)), (+.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4))))) b), (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4))))) b) a), (*.p16 (*.p16 a (real->posit16 2)) (+.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4))))) b)), (neg.p16 (*.p16 c (*.p16 a (real->posit16 4)))), (-.p16 (*.p16 (*.p16 b b) (*.p16 b b)) (*.p16 (*.p16 c (*.p16 a (real->posit16 4))) (*.p16 c (*.p16 a (real->posit16 4))))), (+.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4)))), (*.p16 a (real->posit16 2)), (*.p16 a (real->posit16 2)), (*.p16 a (real->posit16 2)), (*.p16 a (real->posit16 2))
10.957 * * [simplify]: iteration 1: (25 enodes)
10.964 * * [simplify]: iteration 2: (76 enodes)
10.979 * * [simplify]: iteration 3: (230 enodes)
11.045 * * [simplify]: iteration 4: (925 enodes)
12.519 * * [simplify]: Extracting #0: cost 9 inf + 0
12.520 * * [simplify]: Extracting #1: cost 190 inf + 0
12.522 * * [simplify]: Extracting #2: cost 764 inf + 1847
12.527 * * [simplify]: Extracting #3: cost 1260 inf + 11483
12.536 * * [simplify]: Extracting #4: cost 1723 inf + 45745
12.553 * * [simplify]: Extracting #5: cost 1713 inf + 108113
12.599 * * [simplify]: Extracting #6: cost 1307 inf + 872389
12.864 * * [simplify]: Extracting #7: cost 284 inf + 3282020
13.224 * * [simplify]: Extracting #8: cost 1 inf + 3754098
13.586 * * [simplify]: Extracting #9: cost 0 inf + 3728382
13.861 * * [simplify]: Extracting #10: cost 0 inf + 3728062
14.097 * [simplify]: Simplified to (neg.p16 b), (-.p16 (real->posit16 0.0) (*.p16 a (*.p16 (real->posit16 4) c))), (+.p16 b (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 a (*.p16 (real->posit16 4) c))))), (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 a (*.p16 (real->posit16 4) c)))) b) a), (*.p16 (+.p16 b (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 a (*.p16 (real->posit16 4) c))))) (*.p16 a (real->posit16 2))), (neg.p16 (*.p16 a (*.p16 (real->posit16 4) c))), (*.p16 (-.p16 (*.p16 b b) (*.p16 a (*.p16 (real->posit16 4) c))) (+.p16 (*.p16 a (*.p16 (real->posit16 4) c)) (*.p16 b b))), (+.p16 (*.p16 a (*.p16 (real->posit16 4) c)) (*.p16 b b)), (*.p16 a (real->posit16 2)), (*.p16 a (real->posit16 2)), (*.p16 a (real->posit16 2)), (*.p16 a (real->posit16 2))
14.097 * * * * [progress]: [ 1 / 10 ] simplifiying candidate #<alt (λ (a b c) (/.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4))))) (neg.p16 b)) (*.p16 a (real->posit16 2))))>
14.097 * [simplify]: Simplified (2 1 2) to (λ (a b c) (/.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4))))) (neg.p16 b)) (*.p16 a (real->posit16 2))))
14.097 * * * * [progress]: [ 2 / 10 ] simplifiying candidate #<alt (λ (a b c) (/.p16 (/.p16 (-.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4))))) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4)))))) (*.p16 b b)) (+.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4))))) b)) (*.p16 a (real->posit16 2))))>
14.097 * [simplify]: Simplified (2 1 1) to (λ (a b c) (/.p16 (/.p16 (-.p16 (real->posit16 0.0) (*.p16 a (*.p16 (real->posit16 4) c))) (+.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4))))) b)) (*.p16 a (real->posit16 2))))
14.097 * [simplify]: Simplified (2 1 2) to (λ (a b c) (/.p16 (/.p16 (-.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4))))) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4)))))) (*.p16 b b)) (+.p16 b (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 a (*.p16 (real->posit16 4) c)))))) (*.p16 a (real->posit16 2))))
14.097 * * * * [progress]: [ 3 / 10 ] simplifiying candidate #<alt (λ (a b c) (/.p16 (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4))))) b) a) (real->posit16 2)))>
14.097 * [simplify]: Simplified (2 1) to (λ (a b c) (/.p16 (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 a (*.p16 (real->posit16 4) c)))) b) a) (real->posit16 2)))
14.098 * * * * [progress]: [ 4 / 10 ] simplifiying candidate #<alt (λ (a b c) (/.p16 (-.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4))))) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4)))))) (*.p16 b b)) (*.p16 (*.p16 a (real->posit16 2)) (+.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4))))) b))))>
14.098 * [simplify]: Simplified (2 2) to (λ (a b c) (/.p16 (-.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4))))) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4)))))) (*.p16 b b)) (*.p16 (+.p16 b (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 a (*.p16 (real->posit16 4) c))))) (*.p16 a (real->posit16 2)))))
14.098 * * * * [progress]: [ 5 / 10 ] simplifiying candidate #<alt (λ (a b c) (/.p16 (-.p16 (sqrt.p16 (+.p16 (*.p16 b b) (neg.p16 (*.p16 c (*.p16 a (real->posit16 4)))))) b) (*.p16 a (real->posit16 2))))>
14.098 * [simplify]: Simplified (2 1 1 1 2) to (λ (a b c) (/.p16 (-.p16 (sqrt.p16 (+.p16 (*.p16 b b) (neg.p16 (*.p16 a (*.p16 (real->posit16 4) c))))) b) (*.p16 a (real->posit16 2))))
14.098 * * * * [progress]: [ 6 / 10 ] simplifiying candidate #<alt (λ (a b c) (/.p16 (-.p16 (sqrt.p16 (/.p16 (-.p16 (*.p16 (*.p16 b b) (*.p16 b b)) (*.p16 (*.p16 c (*.p16 a (real->posit16 4))) (*.p16 c (*.p16 a (real->posit16 4))))) (+.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4)))))) b) (*.p16 a (real->posit16 2))))>
14.098 * [simplify]: Simplified (2 1 1 1 1) to (λ (a b c) (/.p16 (-.p16 (sqrt.p16 (/.p16 (*.p16 (-.p16 (*.p16 b b) (*.p16 a (*.p16 (real->posit16 4) c))) (+.p16 (*.p16 a (*.p16 (real->posit16 4) c)) (*.p16 b b))) (+.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4)))))) b) (*.p16 a (real->posit16 2))))
14.099 * [simplify]: Simplified (2 1 1 1 2) to (λ (a b c) (/.p16 (-.p16 (sqrt.p16 (/.p16 (-.p16 (*.p16 (*.p16 b b) (*.p16 b b)) (*.p16 (*.p16 c (*.p16 a (real->posit16 4))) (*.p16 c (*.p16 a (real->posit16 4))))) (+.p16 (*.p16 a (*.p16 (real->posit16 4) c)) (*.p16 b b)))) b) (*.p16 a (real->posit16 2))))
14.099 * * * * [progress]: [ 7 / 10 ] simplifiying candidate #<alt (λ (a b c) (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4))))) b) (*.p16 a (real->posit16 2))))>
14.099 * [simplify]: Simplified (2 2) to (λ (a b c) (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4))))) b) (*.p16 a (real->posit16 2))))
14.099 * * * * [progress]: [ 8 / 10 ] simplifiying candidate #<alt (λ (a b c) (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4))))) b) (*.p16 a (real->posit16 2))))>
14.099 * [simplify]: Simplified (2 2) to (λ (a b c) (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4))))) b) (*.p16 a (real->posit16 2))))
14.099 * * * * [progress]: [ 9 / 10 ] simplifiying candidate #<alt (λ (a b c) (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4))))) b) (*.p16 a (real->posit16 2))))>
14.099 * [simplify]: Simplified (2 2) to (λ (a b c) (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4))))) b) (*.p16 a (real->posit16 2))))
14.099 * * * * [progress]: [ 10 / 10 ] simplifiying candidate #<alt (λ (a b c) (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4))))) b) (*.p16 a (real->posit16 2))))>
14.099 * [simplify]: Simplified (2 2) to (λ (a b c) (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4))))) b) (*.p16 a (real->posit16 2))))
14.100 * * * [progress]: adding candidates to table
14.706 * [progress]: [Phase 3 of 3] Extracting.
14.706 * * [regime]: Finding splitpoints for: (#<alt (λ (a b c) (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b) (*.p16 (real->posit16 2) a)))> #<alt (λ (a b c) (/.p16 (/.p16 (-.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4))))) (*.p16 b b)) (+.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b)) (*.p16 (real->posit16 2) a)))> #<alt (λ (a b c) (/.p16 (/.p16 (/.p16 (-.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4))))) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4)))))) (*.p16 b b)) (+.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4))))) b)) (real->posit16 2)) a))> #<alt (λ (a b c) (/.p16 (-.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4))))) (*.p16 b b)) (*.p16 (*.p16 (real->posit16 2) a) (+.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b))))> #<alt (λ (a b c) (/.p16 (/.p16 (-.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4))))) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4)))))) (*.p16 b b)) (+.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4))))) b)) (*.p16 a (real->posit16 2))))> #<alt (λ (a b c) (/.p16 (-.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4))))) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4)))))) (*.p16 b b)) (*.p16 (*.p16 a (real->posit16 2)) (+.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4))))) b))))> #<alt (λ (a b c) (/.p16 (-.p16 (sqrt.p16 (/.p16 (-.p16 (*.p16 (*.p16 b b) (*.p16 b b)) (*.p16 (*.p16 c (*.p16 a (real->posit16 4))) (*.p16 c (*.p16 a (real->posit16 4))))) (+.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4)))))) b) (*.p16 a (real->posit16 2))))> #<alt (λ (a b c) (/.p16 (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4))))) b) a) (real->posit16 2)))>)
14.713 * * * [regime-changes]: Trying 3 branch expressions: (c a b)
14.713 * * * * [regimes]: Trying to branch on c from (#<alt (λ (a b c) (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b) (*.p16 (real->posit16 2) a)))> #<alt (λ (a b c) (/.p16 (/.p16 (-.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4))))) (*.p16 b b)) (+.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b)) (*.p16 (real->posit16 2) a)))> #<alt (λ (a b c) (/.p16 (/.p16 (/.p16 (-.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4))))) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4)))))) (*.p16 b b)) (+.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4))))) b)) (real->posit16 2)) a))> #<alt (λ (a b c) (/.p16 (-.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4))))) (*.p16 b b)) (*.p16 (*.p16 (real->posit16 2) a) (+.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b))))> #<alt (λ (a b c) (/.p16 (/.p16 (-.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4))))) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4)))))) (*.p16 b b)) (+.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4))))) b)) (*.p16 a (real->posit16 2))))> #<alt (λ (a b c) (/.p16 (-.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4))))) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4)))))) (*.p16 b b)) (*.p16 (*.p16 a (real->posit16 2)) (+.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4))))) b))))> #<alt (λ (a b c) (/.p16 (-.p16 (sqrt.p16 (/.p16 (-.p16 (*.p16 (*.p16 b b) (*.p16 b b)) (*.p16 (*.p16 c (*.p16 a (real->posit16 4))) (*.p16 c (*.p16 a (real->posit16 4))))) (+.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4)))))) b) (*.p16 a (real->posit16 2))))> #<alt (λ (a b c) (/.p16 (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4))))) b) a) (real->posit16 2)))>)
14.959 * * * * [regimes]: Trying to branch on a from (#<alt (λ (a b c) (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b) (*.p16 (real->posit16 2) a)))> #<alt (λ (a b c) (/.p16 (/.p16 (-.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4))))) (*.p16 b b)) (+.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b)) (*.p16 (real->posit16 2) a)))> #<alt (λ (a b c) (/.p16 (/.p16 (/.p16 (-.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4))))) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4)))))) (*.p16 b b)) (+.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4))))) b)) (real->posit16 2)) a))> #<alt (λ (a b c) (/.p16 (-.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4))))) (*.p16 b b)) (*.p16 (*.p16 (real->posit16 2) a) (+.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b))))> #<alt (λ (a b c) (/.p16 (/.p16 (-.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4))))) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4)))))) (*.p16 b b)) (+.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4))))) b)) (*.p16 a (real->posit16 2))))> #<alt (λ (a b c) (/.p16 (-.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4))))) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4)))))) (*.p16 b b)) (*.p16 (*.p16 a (real->posit16 2)) (+.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4))))) b))))> #<alt (λ (a b c) (/.p16 (-.p16 (sqrt.p16 (/.p16 (-.p16 (*.p16 (*.p16 b b) (*.p16 b b)) (*.p16 (*.p16 c (*.p16 a (real->posit16 4))) (*.p16 c (*.p16 a (real->posit16 4))))) (+.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4)))))) b) (*.p16 a (real->posit16 2))))> #<alt (λ (a b c) (/.p16 (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4))))) b) a) (real->posit16 2)))>)
15.162 * * * * [regimes]: Trying to branch on b from (#<alt (λ (a b c) (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b) (*.p16 (real->posit16 2) a)))> #<alt (λ (a b c) (/.p16 (/.p16 (-.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4))))) (*.p16 b b)) (+.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b)) (*.p16 (real->posit16 2) a)))> #<alt (λ (a b c) (/.p16 (/.p16 (/.p16 (-.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4))))) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4)))))) (*.p16 b b)) (+.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4))))) b)) (real->posit16 2)) a))> #<alt (λ (a b c) (/.p16 (-.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4))))) (*.p16 b b)) (*.p16 (*.p16 (real->posit16 2) a) (+.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b))))> #<alt (λ (a b c) (/.p16 (/.p16 (-.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4))))) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4)))))) (*.p16 b b)) (+.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4))))) b)) (*.p16 a (real->posit16 2))))> #<alt (λ (a b c) (/.p16 (-.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4))))) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4)))))) (*.p16 b b)) (*.p16 (*.p16 a (real->posit16 2)) (+.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4))))) b))))> #<alt (λ (a b c) (/.p16 (-.p16 (sqrt.p16 (/.p16 (-.p16 (*.p16 (*.p16 b b) (*.p16 b b)) (*.p16 (*.p16 c (*.p16 a (real->posit16 4))) (*.p16 c (*.p16 a (real->posit16 4))))) (+.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4)))))) b) (*.p16 a (real->posit16 2))))> #<alt (λ (a b c) (/.p16 (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4))))) b) a) (real->posit16 2)))>)
15.398 * * * [regime]: Found split indices: #<option (#s(si 7 256))>
15.399 * [simplify]: Simplifying (/.p16 (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4))))) b) a) (real->posit16 2))
15.399 * * [simplify]: iteration 1: (15 enodes)
15.400 * * [simplify]: Extracting #0: cost 1 inf + 0
15.400 * * [simplify]: Extracting #1: cost 3 inf + 0
15.400 * * [simplify]: Extracting #2: cost 6 inf + 0
15.400 * * [simplify]: Extracting #3: cost 5 inf + 3
15.400 * * [simplify]: Extracting #4: cost 5 inf + 4
15.400 * * [simplify]: Extracting #5: cost 7 inf + 4
15.400 * * [simplify]: Extracting #6: cost 8 inf + 325
15.400 * * [simplify]: Extracting #7: cost 8 inf + 326
15.401 * * [simplify]: Extracting #8: cost 9 inf + 326
15.401 * * [simplify]: Extracting #9: cost 7 inf + 328
15.401 * * [simplify]: Extracting #10: cost 5 inf + 1293
15.401 * * [simplify]: Extracting #11: cost 3 inf + 3421
15.401 * * [simplify]: Extracting #12: cost 1 inf + 6189
15.401 * * [simplify]: Extracting #13: cost 0 inf + 8234
15.401 * [simplify]: Simplified to (/.p16 (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4))))) b) a) (real->posit16 2))
15.401 * * * * [points]: Sampling 8000 additional inputs, on iter 0 have 0 / 8000
15.443 * * * * [points]: Computing exacts on every 500 of 8000 points to ramp up precision
15.447 * * * * [points]: Setting MPFR precision to 64
15.449 * * * * [points]: Setting MPFR precision to 320
15.450 * * * * [points]: Computing exacts on every 250 of 8000 points to ramp up precision
15.452 * * * * [points]: Setting MPFR precision to 64
15.454 * * * * [points]: Setting MPFR precision to 320
15.456 * * * * [points]: Computing exacts on every 125 of 8000 points to ramp up precision
15.459 * * * * [points]: Setting MPFR precision to 64
15.463 * * * * [points]: Setting MPFR precision to 320
15.467 * * * * [points]: Computing exacts on every 62 of 8000 points to ramp up precision
15.470 * * * * [points]: Setting MPFR precision to 64
15.478 * * * * [points]: Setting MPFR precision to 320
15.501 * * * * [points]: Computing exacts on every 31 of 8000 points to ramp up precision
15.504 * * * * [points]: Setting MPFR precision to 64
15.522 * * * * [points]: Setting MPFR precision to 320
15.539 * * * * [points]: Computing exacts on every 15 of 8000 points to ramp up precision
15.541 * * * * [points]: Setting MPFR precision to 64
15.574 * * * * [points]: Setting MPFR precision to 320
15.608 * * * * [points]: Computing exacts on every 7 of 8000 points to ramp up precision
15.611 * * * * [points]: Setting MPFR precision to 64
15.709 * * * * [points]: Setting MPFR precision to 320
15.813 * * * * [points]: Computing exacts on every 3 of 8000 points to ramp up precision
15.816 * * * * [points]: Setting MPFR precision to 64
16.034 * * * * [points]: Setting MPFR precision to 320
16.291 * * * * [points]: Computing exacts for 8000 points
16.294 * * * * [points]: Setting MPFR precision to 64
17.139 * * * * [points]: Setting MPFR precision to 320
18.589 * * * * [points]: Filtering points with unrepresentable outputs
18.629 * * * * [points]: Sampled 8000 points with exact outputs
24.592 * [regime-testing]: Baseline error score: 64.0
24.598 * [regime-testing]: Oracle error score: 64.0
24.612 * [regime-testing]: End program error score: 1.53861151671579