1.512 * [progress]: [Phase 1 of 3] Setting up.
0.003 * * * [progress]: [1/2] Preparing points
0.003 * * * * [points]: Sampling 256 additional inputs, on iter 0 have 0 / 256
0.005 * * * * [points]: Computing exacts on every 16 of 256 points to ramp up precision
0.065 * * * * [points]: Setting MPFR precision to 64
0.069 * * * * [points]: Setting MPFR precision to 320
0.071 * * * * [points]: Computing exacts on every 8 of 256 points to ramp up precision
0.073 * * * * [points]: Setting MPFR precision to 64
0.076 * * * * [points]: Setting MPFR precision to 320
0.080 * * * * [points]: Computing exacts on every 4 of 256 points to ramp up precision
0.084 * * * * [points]: Setting MPFR precision to 64
0.090 * * * * [points]: Setting MPFR precision to 320
0.094 * * * * [points]: Computing exacts on every 2 of 256 points to ramp up precision
0.095 * * * * [points]: Setting MPFR precision to 64
0.101 * * * * [points]: Setting MPFR precision to 320
0.107 * * * * [points]: Computing exacts for 256 points
0.109 * * * * [points]: Setting MPFR precision to 64
0.127 * * * * [points]: Setting MPFR precision to 320
0.153 * * * * [points]: Filtering points with unrepresentable outputs
0.154 * * * * [points]: Sampled 256 points with exact outputs
0.155 * * * [progress]: [2/2] Setting up program.
0.202 * [progress]: [Phase 2 of 3] Improving.
0.203 * * * * [progress]: [ 1 / 1 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (+.p16 (neg.p16 b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c)))) a))>
0.205 * [simplify]: Simplifying:
  (/.p16 (+.p16 (neg.p16 b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c)))) a)
0.206 * * [simplify]: iteration 1: (10 enodes)
0.213 * * [simplify]: iteration 2: (14 enodes)
0.215 * * [simplify]: iteration 3: (16 enodes)
0.218 * * [simplify]: Extracting #0: cost 1 inf + 0
0.218 * * [simplify]: Extracting #1: cost 3 inf + 0
0.218 * * [simplify]: Extracting #2: cost 5 inf + 1
0.218 * * [simplify]: Extracting #3: cost 5 inf + 2
0.218 * * [simplify]: Extracting #4: cost 7 inf + 83
0.218 * * [simplify]: Extracting #5: cost 7 inf + 404
0.219 * * [simplify]: Extracting #6: cost 0 inf + 4741
0.219 * [simplify]: Simplified to:
  (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) a)
0.232 * * [progress]: iteration 1 / 4
0.232 * * * [progress]: picking best candidate
0.237 * * * * [pick]: Picked  #<alt (λ (a b_2 c) (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) a))>
0.237 * * * [progress]: localizing error
0.364 * * * [progress]: generating rewritten candidates
0.364 * * * * [progress]: [ 1 / 4 ] rewriting at (2 1)
0.368 * * * * [progress]: [ 2 / 4 ] rewriting at (2 1 1 1)
0.371 * * * * [progress]: [ 3 / 4 ] rewriting at (2)
0.375 * * * * [progress]: [ 4 / 4 ] rewriting at (2 1 1)
0.377 * * * [progress]: generating series expansions
0.377 * * * * [progress]: [ 1 / 4 ] generating series at (2 1)
0.378 * * * * [progress]: [ 2 / 4 ] generating series at (2 1 1 1)
0.378 * * * * [progress]: [ 3 / 4 ] generating series at (2)
0.378 * * * * [progress]: [ 4 / 4 ] generating series at (2 1 1)
0.378 * * * [progress]: simplifying candidates
0.378 * * * * [progress]: [ 1 / 57 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (+.p16 (real->posit16 0.0) (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)) a))>
0.378 * * * * [progress]: [ 2 / 57 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) (-.p16 (real->posit16 0.0) b_2)) a))>
0.378 * * * * [progress]: [ 3 / 57 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) (+.p16 (real->posit16 0.0) b_2)) a))>
0.378 * * * * [progress]: [ 4 / 57 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) (neg.p16 b_2)) a))>
0.378 * * * * [progress]: [ 5 / 57 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (/.p16 (-.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) (*.p16 b_2 b_2)) (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)) a))>
0.378 * * * * [progress]: [ 6 / 57 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (*.p16 (real->posit16 1.0) (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)) a))>
0.378 * * * * [progress]: [ 7 / 57 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (quire16->posit16 (posit16->quire16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2))) a))>
0.378 * * * * [progress]: [ 8 / 57 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (quire16->posit16 (quire16-mul-sub (posit16->quire16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) b_2 (real->posit16 1.0))) a))>
0.378 * * * * [progress]: [ 9 / 57 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (+.p16 (real->posit16 0.0) (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)) a))>
0.378 * * * * [progress]: [ 10 / 57 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (+.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) (real->posit16 0.0)) a))>
0.378 * * * * [progress]: [ 11 / 57 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (-.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) (real->posit16 0.0)) a))>
0.378 * * * * [progress]: [ 12 / 57 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (*.p16 (real->posit16 1.0) (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)) a))>
0.378 * * * * [progress]: [ 13 / 57 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (*.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) (real->posit16 1.0)) a))>
0.378 * * * * [progress]: [ 14 / 57 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) (real->posit16 1.0)) a))>
0.378 * * * * [progress]: [ 15 / 57 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (-.p16 (sqrt.p16 (-.p16 (-.p16 (*.p16 b_2 b_2) (real->posit16 0.0)) (*.p16 c a))) b_2) a))>
0.378 * * * * [progress]: [ 16 / 57 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (-.p16 (sqrt.p16 (-.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)) (real->posit16 0.0))) b_2) a))>
0.378 * * * * [progress]: [ 17 / 57 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (-.p16 (sqrt.p16 (+.p16 (real->posit16 0.0) (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) b_2) a))>
0.378 * * * * [progress]: [ 18 / 57 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (-.p16 (sqrt.p16 (+.p16 (*.p16 b_2 b_2) (-.p16 (real->posit16 0.0) (*.p16 c a)))) b_2) a))>
0.379 * * * * [progress]: [ 19 / 57 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (+.p16 (real->posit16 0.0) (*.p16 c a)))) b_2) a))>
0.379 * * * * [progress]: [ 20 / 57 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (-.p16 (sqrt.p16 (+.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)) (real->posit16 0.0))) b_2) a))>
0.379 * * * * [progress]: [ 21 / 57 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (-.p16 (sqrt.p16 (+.p16 (*.p16 b_2 b_2) (neg.p16 (*.p16 c a)))) b_2) a))>
0.379 * * * * [progress]: [ 22 / 57 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (-.p16 (sqrt.p16 (/.p16 (-.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 c a) (*.p16 c a))) (+.p16 (*.p16 b_2 b_2) (*.p16 c a)))) b_2) a))>
0.379 * * * * [progress]: [ 23 / 57 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (-.p16 (sqrt.p16 (*.p16 (real->posit16 1.0) (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) b_2) a))>
0.379 * * * * [progress]: [ 24 / 57 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (-.p16 (sqrt.p16 (quire16->posit16 (posit16->quire16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))))) b_2) a))>
0.379 * * * * [progress]: [ 25 / 57 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (-.p16 (sqrt.p16 (quire16->posit16 (quire16-mul-sub (posit16->quire16 (*.p16 b_2 b_2)) (*.p16 c a) (real->posit16 1.0)))) b_2) a))>
0.379 * * * * [progress]: [ 26 / 57 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (-.p16 (sqrt.p16 (quire16->posit16 (quire16-mul-sub (posit16->quire16 (*.p16 b_2 b_2)) c a))) b_2) a))>
0.379 * * * * [progress]: [ 27 / 57 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (-.p16 (sqrt.p16 (+.p16 (real->posit16 0.0) (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) b_2) a))>
0.379 * * * * [progress]: [ 28 / 57 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (-.p16 (sqrt.p16 (+.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)) (real->posit16 0.0))) b_2) a))>
0.379 * * * * [progress]: [ 29 / 57 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (-.p16 (sqrt.p16 (-.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)) (real->posit16 0.0))) b_2) a))>
0.379 * * * * [progress]: [ 30 / 57 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (-.p16 (sqrt.p16 (*.p16 (real->posit16 1.0) (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) b_2) a))>
0.379 * * * * [progress]: [ 31 / 57 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (-.p16 (sqrt.p16 (*.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)) (real->posit16 1.0))) b_2) a))>
0.379 * * * * [progress]: [ 32 / 57 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (-.p16 (sqrt.p16 (/.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)) (real->posit16 1.0))) b_2) a))>
0.379 * * * * [progress]: [ 33 / 57 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (real->posit16 1.0) (/.p16 a (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2))))>
0.379 * * * * [progress]: [ 34 / 57 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (real->posit16 1.0) (/.p16 a (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2))))>
0.379 * * * * [progress]: [ 35 / 57 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) (/.p16 a (real->posit16 1.0))))>
0.379 * * * * [progress]: [ 36 / 57 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (-.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) (*.p16 b_2 b_2)) (*.p16 a (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2))))>
0.379 * * * * [progress]: [ 37 / 57 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) (*.p16 a (real->posit16 1.0))))>
0.379 * * * * [progress]: [ 38 / 57 ] simplifiying candidate #<alt (λ (a b_2 c) (*.p16 (real->posit16 1.0) (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) a)))>
0.379 * * * * [progress]: [ 39 / 57 ] simplifiying candidate #<alt (λ (a b_2 c) (quire16->posit16 (posit16->quire16 (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) a))))>
0.379 * * * * [progress]: [ 40 / 57 ] simplifiying candidate #<alt (λ (a b_2 c) (+.p16 (real->posit16 0.0) (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) a)))>
0.379 * * * * [progress]: [ 41 / 57 ] simplifiying candidate #<alt (λ (a b_2 c) (+.p16 (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) a) (real->posit16 0.0)))>
0.379 * * * * [progress]: [ 42 / 57 ] simplifiying candidate #<alt (λ (a b_2 c) (-.p16 (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) a) (real->posit16 0.0)))>
0.379 * * * * [progress]: [ 43 / 57 ] simplifiying candidate #<alt (λ (a b_2 c) (*.p16 (real->posit16 1.0) (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) a)))>
0.379 * * * * [progress]: [ 44 / 57 ] simplifiying candidate #<alt (λ (a b_2 c) (*.p16 (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) a) (real->posit16 1.0)))>
0.379 * * * * [progress]: [ 45 / 57 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) a) (real->posit16 1.0)))>
0.380 * * * * [progress]: [ 46 / 57 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (-.p16 (*.p16 (real->posit16 1.0) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) b_2) a))>
0.380 * * * * [progress]: [ 47 / 57 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (-.p16 (quire16->posit16 (posit16->quire16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))))) b_2) a))>
0.380 * * * * [progress]: [ 48 / 57 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (-.p16 (+.p16 (real->posit16 0.0) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) b_2) a))>
0.380 * * * * [progress]: [ 49 / 57 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (-.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) (real->posit16 0.0)) b_2) a))>
0.380 * * * * [progress]: [ 50 / 57 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (-.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) (real->posit16 0.0)) b_2) a))>
0.380 * * * * [progress]: [ 51 / 57 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (-.p16 (*.p16 (real->posit16 1.0) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) b_2) a))>
0.380 * * * * [progress]: [ 52 / 57 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (-.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) (real->posit16 1.0)) b_2) a))>
0.380 * * * * [progress]: [ 53 / 57 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (-.p16 (/.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) (real->posit16 1.0)) b_2) a))>
0.380 * * * * [progress]: [ 54 / 57 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) a))>
0.380 * * * * [progress]: [ 55 / 57 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) a))>
0.380 * * * * [progress]: [ 56 / 57 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) a))>
0.380 * * * * [progress]: [ 57 / 57 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) a))>
0.381 * [simplify]: Simplifying:
  (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)
  (-.p16 (real->posit16 0.0) b_2)
  (+.p16 (real->posit16 0.0) b_2)
  (neg.p16 b_2)
  (-.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) (*.p16 b_2 b_2))
  (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)
  (real->posit16 1.0)
  (posit16->quire16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2))
  (quire16-mul-sub (posit16->quire16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) b_2 (real->posit16 1.0))
  (real->posit16 0.0)
  (real->posit16 0.0)
  (real->posit16 0.0)
  (real->posit16 1.0)
  (real->posit16 1.0)
  (real->posit16 1.0)
  (-.p16 (*.p16 b_2 b_2) (real->posit16 0.0))
  (-.p16 (*.p16 b_2 b_2) (*.p16 c a))
  (-.p16 (*.p16 b_2 b_2) (*.p16 c a))
  (-.p16 (real->posit16 0.0) (*.p16 c a))
  (+.p16 (real->posit16 0.0) (*.p16 c a))
  (-.p16 (*.p16 b_2 b_2) (*.p16 c a))
  (neg.p16 (*.p16 c a))
  (-.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 c a) (*.p16 c a)))
  (+.p16 (*.p16 b_2 b_2) (*.p16 c a))
  (real->posit16 1.0)
  (posit16->quire16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))
  (quire16-mul-sub (posit16->quire16 (*.p16 b_2 b_2)) (*.p16 c a) (real->posit16 1.0))
  (quire16-mul-sub (posit16->quire16 (*.p16 b_2 b_2)) c a)
  (real->posit16 0.0)
  (real->posit16 0.0)
  (real->posit16 0.0)
  (real->posit16 1.0)
  (real->posit16 1.0)
  (real->posit16 1.0)
  (/.p16 a (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2))
  (/.p16 a (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2))
  (/.p16 a (real->posit16 1.0))
  (*.p16 a (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2))
  (*.p16 a (real->posit16 1.0))
  (real->posit16 1.0)
  (posit16->quire16 (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) a))
  (real->posit16 0.0)
  (real->posit16 0.0)
  (real->posit16 0.0)
  (real->posit16 1.0)
  (real->posit16 1.0)
  (real->posit16 1.0)
  (real->posit16 1.0)
  (posit16->quire16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))))
  (real->posit16 0.0)
  (real->posit16 0.0)
  (real->posit16 0.0)
  (real->posit16 1.0)
  (real->posit16 1.0)
  (real->posit16 1.0)
  (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) a)
  (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) a)
  (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) a)
  (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) a)
0.381 * * [simplify]: iteration 1: (39 enodes)
0.391 * * [simplify]: iteration 2: (72 enodes)
0.405 * * [simplify]: iteration 3: (191 enodes)
0.550 * * [simplify]: iteration 4: (986 enodes)
25.254 * * [simplify]: Extracting #0: cost 24 inf + 0
25.257 * * [simplify]: Extracting #1: cost 1413 inf + 2
25.268 * * [simplify]: Extracting #2: cost 3005 inf + 38150
25.314 * * [simplify]: Extracting #3: cost 1520 inf + 990960
25.417 * * [simplify]: Extracting #4: cost 188 inf + 1997621
25.575 * * [simplify]: Extracting #5: cost 0 inf + 2152672
25.803 * * [simplify]: Extracting #6: cost 0 inf + 2151712
26.034 * [simplify]: Simplified to:
  (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))) b_2)
  (neg.p16 b_2)
  b_2
  (neg.p16 b_2)
  (-.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c)))) (*.p16 b_2 b_2))
  (+.p16 b_2 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))))
  (real->posit16 1.0)
  (posit16->quire16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))) b_2))
  (quire16-mul-sub (posit16->quire16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c)))) b_2 (real->posit16 1.0))
  (real->posit16 0.0)
  (real->posit16 0.0)
  (real->posit16 0.0)
  (real->posit16 1.0)
  (real->posit16 1.0)
  (real->posit16 1.0)
  (*.p16 b_2 b_2)
  (-.p16 (*.p16 b_2 b_2) (*.p16 a c))
  (-.p16 (*.p16 b_2 b_2) (*.p16 a c))
  (neg.p16 (*.p16 a c))
  (*.p16 a c)
  (-.p16 (*.p16 b_2 b_2) (*.p16 a c))
  (neg.p16 (*.p16 a c))
  (*.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c)) (+.p16 (*.p16 a c) (*.p16 b_2 b_2)))
  (+.p16 (*.p16 b_2 b_2) (*.p16 a c))
  (real->posit16 1.0)
  (posit16->quire16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c)))
  (quire16-mul-sub (posit16->quire16 (*.p16 b_2 b_2)) (*.p16 a c) (real->posit16 1.0))
  (quire16-mul-sub (posit16->quire16 (*.p16 b_2 b_2)) c a)
  (real->posit16 0.0)
  (real->posit16 0.0)
  (real->posit16 0.0)
  (real->posit16 1.0)
  (real->posit16 1.0)
  (real->posit16 1.0)
  (/.p16 a (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))) b_2))
  (/.p16 a (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))) b_2))
  a
  (*.p16 (+.p16 b_2 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c)))) a)
  a
  (real->posit16 1.0)
  (posit16->quire16 (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))) b_2) a))
  (real->posit16 0.0)
  (real->posit16 0.0)
  (real->posit16 0.0)
  (real->posit16 1.0)
  (real->posit16 1.0)
  (real->posit16 1.0)
  (real->posit16 1.0)
  (posit16->quire16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))))
  (real->posit16 0.0)
  (real->posit16 0.0)
  (real->posit16 0.0)
  (real->posit16 1.0)
  (real->posit16 1.0)
  (real->posit16 1.0)
  (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))) b_2) a)
  (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))) b_2) a)
  (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))) b_2) a)
  (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))) b_2) a)
26.038 * * * [progress]: adding candidates to table
27.536 * * [progress]: iteration 2 / 4
27.536 * * * [progress]: picking best candidate
27.572 * * * * [pick]: Picked  #<alt (λ (a b_2 c) (/.p16 (-.p16 (sqrt.p16 (quire16->posit16 (quire16-mul-sub (posit16->quire16 (*.p16 b_2 b_2)) c a))) b_2) a))>
27.572 * * * [progress]: localizing error
27.780 * * * [progress]: generating rewritten candidates
27.781 * * * * [progress]: [ 1 / 4 ] rewriting at (2 1 1 1 1)
27.781 * * * * [progress]: [ 2 / 4 ] rewriting at (2 1)
27.786 * * * * [progress]: [ 3 / 4 ] rewriting at (2)
27.792 * * * * [progress]: [ 4 / 4 ] rewriting at (2 1 1)
27.793 * * * [progress]: generating series expansions
27.793 * * * * [progress]: [ 1 / 4 ] generating series at (2 1 1 1 1)
27.794 * * * * [progress]: [ 2 / 4 ] generating series at (2 1)
27.794 * * * * [progress]: [ 3 / 4 ] generating series at (2)
27.794 * * * * [progress]: [ 4 / 4 ] generating series at (2 1 1)
27.794 * * * [progress]: simplifying candidates
27.794 * * * * [progress]: [ 1 / 39 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (+.p16 (real->posit16 0.0) (-.p16 (sqrt.p16 (quire16->posit16 (quire16-mul-sub (posit16->quire16 (*.p16 b_2 b_2)) c a))) b_2)) a))>
27.794 * * * * [progress]: [ 2 / 39 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (+.p16 (sqrt.p16 (quire16->posit16 (quire16-mul-sub (posit16->quire16 (*.p16 b_2 b_2)) c a))) (-.p16 (real->posit16 0.0) b_2)) a))>
27.794 * * * * [progress]: [ 3 / 39 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (-.p16 (sqrt.p16 (quire16->posit16 (quire16-mul-sub (posit16->quire16 (*.p16 b_2 b_2)) c a))) (+.p16 (real->posit16 0.0) b_2)) a))>
27.794 * * * * [progress]: [ 4 / 39 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (+.p16 (sqrt.p16 (quire16->posit16 (quire16-mul-sub (posit16->quire16 (*.p16 b_2 b_2)) c a))) (neg.p16 b_2)) a))>
27.794 * * * * [progress]: [ 5 / 39 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (/.p16 (-.p16 (*.p16 (sqrt.p16 (quire16->posit16 (quire16-mul-sub (posit16->quire16 (*.p16 b_2 b_2)) c a))) (sqrt.p16 (quire16->posit16 (quire16-mul-sub (posit16->quire16 (*.p16 b_2 b_2)) c a)))) (*.p16 b_2 b_2)) (+.p16 (sqrt.p16 (quire16->posit16 (quire16-mul-sub (posit16->quire16 (*.p16 b_2 b_2)) c a))) b_2)) a))>
27.794 * * * * [progress]: [ 6 / 39 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (*.p16 (real->posit16 1.0) (-.p16 (sqrt.p16 (quire16->posit16 (quire16-mul-sub (posit16->quire16 (*.p16 b_2 b_2)) c a))) b_2)) a))>
27.794 * * * * [progress]: [ 7 / 39 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (quire16->posit16 (posit16->quire16 (-.p16 (sqrt.p16 (quire16->posit16 (quire16-mul-sub (posit16->quire16 (*.p16 b_2 b_2)) c a))) b_2))) a))>
27.794 * * * * [progress]: [ 8 / 39 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (quire16->posit16 (quire16-mul-sub (posit16->quire16 (sqrt.p16 (quire16->posit16 (quire16-mul-sub (posit16->quire16 (*.p16 b_2 b_2)) c a)))) b_2 (real->posit16 1.0))) a))>
27.794 * * * * [progress]: [ 9 / 39 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (+.p16 (real->posit16 0.0) (-.p16 (sqrt.p16 (quire16->posit16 (quire16-mul-sub (posit16->quire16 (*.p16 b_2 b_2)) c a))) b_2)) a))>
27.794 * * * * [progress]: [ 10 / 39 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (+.p16 (-.p16 (sqrt.p16 (quire16->posit16 (quire16-mul-sub (posit16->quire16 (*.p16 b_2 b_2)) c a))) b_2) (real->posit16 0.0)) a))>
27.794 * * * * [progress]: [ 11 / 39 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (-.p16 (-.p16 (sqrt.p16 (quire16->posit16 (quire16-mul-sub (posit16->quire16 (*.p16 b_2 b_2)) c a))) b_2) (real->posit16 0.0)) a))>
27.794 * * * * [progress]: [ 12 / 39 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (*.p16 (real->posit16 1.0) (-.p16 (sqrt.p16 (quire16->posit16 (quire16-mul-sub (posit16->quire16 (*.p16 b_2 b_2)) c a))) b_2)) a))>
27.795 * * * * [progress]: [ 13 / 39 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (*.p16 (-.p16 (sqrt.p16 (quire16->posit16 (quire16-mul-sub (posit16->quire16 (*.p16 b_2 b_2)) c a))) b_2) (real->posit16 1.0)) a))>
27.795 * * * * [progress]: [ 14 / 39 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (/.p16 (-.p16 (sqrt.p16 (quire16->posit16 (quire16-mul-sub (posit16->quire16 (*.p16 b_2 b_2)) c a))) b_2) (real->posit16 1.0)) a))>
27.795 * * * * [progress]: [ 15 / 39 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (real->posit16 1.0) (/.p16 a (-.p16 (sqrt.p16 (quire16->posit16 (quire16-mul-sub (posit16->quire16 (*.p16 b_2 b_2)) c a))) b_2))))>
27.795 * * * * [progress]: [ 16 / 39 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (real->posit16 1.0) (/.p16 a (-.p16 (sqrt.p16 (quire16->posit16 (quire16-mul-sub (posit16->quire16 (*.p16 b_2 b_2)) c a))) b_2))))>
27.795 * * * * [progress]: [ 17 / 39 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (-.p16 (sqrt.p16 (quire16->posit16 (quire16-mul-sub (posit16->quire16 (*.p16 b_2 b_2)) c a))) b_2) (/.p16 a (real->posit16 1.0))))>
27.795 * * * * [progress]: [ 18 / 39 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (-.p16 (*.p16 (sqrt.p16 (quire16->posit16 (quire16-mul-sub (posit16->quire16 (*.p16 b_2 b_2)) c a))) (sqrt.p16 (quire16->posit16 (quire16-mul-sub (posit16->quire16 (*.p16 b_2 b_2)) c a)))) (*.p16 b_2 b_2)) (*.p16 a (+.p16 (sqrt.p16 (quire16->posit16 (quire16-mul-sub (posit16->quire16 (*.p16 b_2 b_2)) c a))) b_2))))>
27.795 * * * * [progress]: [ 19 / 39 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (-.p16 (sqrt.p16 (quire16->posit16 (quire16-mul-sub (posit16->quire16 (*.p16 b_2 b_2)) c a))) b_2) (*.p16 a (real->posit16 1.0))))>
27.795 * * * * [progress]: [ 20 / 39 ] simplifiying candidate #<alt (λ (a b_2 c) (*.p16 (real->posit16 1.0) (/.p16 (-.p16 (sqrt.p16 (quire16->posit16 (quire16-mul-sub (posit16->quire16 (*.p16 b_2 b_2)) c a))) b_2) a)))>
27.795 * * * * [progress]: [ 21 / 39 ] simplifiying candidate #<alt (λ (a b_2 c) (quire16->posit16 (posit16->quire16 (/.p16 (-.p16 (sqrt.p16 (quire16->posit16 (quire16-mul-sub (posit16->quire16 (*.p16 b_2 b_2)) c a))) b_2) a))))>
27.796 * * * * [progress]: [ 22 / 39 ] simplifiying candidate #<alt (λ (a b_2 c) (+.p16 (real->posit16 0.0) (/.p16 (-.p16 (sqrt.p16 (quire16->posit16 (quire16-mul-sub (posit16->quire16 (*.p16 b_2 b_2)) c a))) b_2) a)))>
27.796 * * * * [progress]: [ 23 / 39 ] simplifiying candidate #<alt (λ (a b_2 c) (+.p16 (/.p16 (-.p16 (sqrt.p16 (quire16->posit16 (quire16-mul-sub (posit16->quire16 (*.p16 b_2 b_2)) c a))) b_2) a) (real->posit16 0.0)))>
27.796 * * * * [progress]: [ 24 / 39 ] simplifiying candidate #<alt (λ (a b_2 c) (-.p16 (/.p16 (-.p16 (sqrt.p16 (quire16->posit16 (quire16-mul-sub (posit16->quire16 (*.p16 b_2 b_2)) c a))) b_2) a) (real->posit16 0.0)))>
27.796 * * * * [progress]: [ 25 / 39 ] simplifiying candidate #<alt (λ (a b_2 c) (*.p16 (real->posit16 1.0) (/.p16 (-.p16 (sqrt.p16 (quire16->posit16 (quire16-mul-sub (posit16->quire16 (*.p16 b_2 b_2)) c a))) b_2) a)))>
27.796 * * * * [progress]: [ 26 / 39 ] simplifiying candidate #<alt (λ (a b_2 c) (*.p16 (/.p16 (-.p16 (sqrt.p16 (quire16->posit16 (quire16-mul-sub (posit16->quire16 (*.p16 b_2 b_2)) c a))) b_2) a) (real->posit16 1.0)))>
27.796 * * * * [progress]: [ 27 / 39 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (/.p16 (-.p16 (sqrt.p16 (quire16->posit16 (quire16-mul-sub (posit16->quire16 (*.p16 b_2 b_2)) c a))) b_2) a) (real->posit16 1.0)))>
27.796 * * * * [progress]: [ 28 / 39 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (-.p16 (*.p16 (real->posit16 1.0) (sqrt.p16 (quire16->posit16 (quire16-mul-sub (posit16->quire16 (*.p16 b_2 b_2)) c a)))) b_2) a))>
27.796 * * * * [progress]: [ 29 / 39 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (-.p16 (quire16->posit16 (posit16->quire16 (sqrt.p16 (quire16->posit16 (quire16-mul-sub (posit16->quire16 (*.p16 b_2 b_2)) c a))))) b_2) a))>
27.796 * * * * [progress]: [ 30 / 39 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (-.p16 (+.p16 (real->posit16 0.0) (sqrt.p16 (quire16->posit16 (quire16-mul-sub (posit16->quire16 (*.p16 b_2 b_2)) c a)))) b_2) a))>
27.796 * * * * [progress]: [ 31 / 39 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (-.p16 (+.p16 (sqrt.p16 (quire16->posit16 (quire16-mul-sub (posit16->quire16 (*.p16 b_2 b_2)) c a))) (real->posit16 0.0)) b_2) a))>
27.796 * * * * [progress]: [ 32 / 39 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (-.p16 (-.p16 (sqrt.p16 (quire16->posit16 (quire16-mul-sub (posit16->quire16 (*.p16 b_2 b_2)) c a))) (real->posit16 0.0)) b_2) a))>
27.796 * * * * [progress]: [ 33 / 39 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (-.p16 (*.p16 (real->posit16 1.0) (sqrt.p16 (quire16->posit16 (quire16-mul-sub (posit16->quire16 (*.p16 b_2 b_2)) c a)))) b_2) a))>
27.796 * * * * [progress]: [ 34 / 39 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (-.p16 (*.p16 (sqrt.p16 (quire16->posit16 (quire16-mul-sub (posit16->quire16 (*.p16 b_2 b_2)) c a))) (real->posit16 1.0)) b_2) a))>
27.796 * * * * [progress]: [ 35 / 39 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (-.p16 (/.p16 (sqrt.p16 (quire16->posit16 (quire16-mul-sub (posit16->quire16 (*.p16 b_2 b_2)) c a))) (real->posit16 1.0)) b_2) a))>
27.796 * * * * [progress]: [ 36 / 39 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (-.p16 (sqrt.p16 (quire16->posit16 (quire16-mul-sub (posit16->quire16 (*.p16 b_2 b_2)) c a))) b_2) a))>
27.796 * * * * [progress]: [ 37 / 39 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (-.p16 (sqrt.p16 (quire16->posit16 (quire16-mul-sub (posit16->quire16 (*.p16 b_2 b_2)) c a))) b_2) a))>
27.796 * * * * [progress]: [ 38 / 39 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (-.p16 (sqrt.p16 (quire16->posit16 (quire16-mul-sub (posit16->quire16 (*.p16 b_2 b_2)) c a))) b_2) a))>
27.796 * * * * [progress]: [ 39 / 39 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (-.p16 (sqrt.p16 (quire16->posit16 (quire16-mul-sub (posit16->quire16 (*.p16 b_2 b_2)) c a))) b_2) a))>
27.797 * [simplify]: Simplifying:
  (-.p16 (sqrt.p16 (quire16->posit16 (quire16-mul-sub (posit16->quire16 (*.p16 b_2 b_2)) c a))) b_2)
  (-.p16 (real->posit16 0.0) b_2)
  (+.p16 (real->posit16 0.0) b_2)
  (neg.p16 b_2)
  (-.p16 (*.p16 (sqrt.p16 (quire16->posit16 (quire16-mul-sub (posit16->quire16 (*.p16 b_2 b_2)) c a))) (sqrt.p16 (quire16->posit16 (quire16-mul-sub (posit16->quire16 (*.p16 b_2 b_2)) c a)))) (*.p16 b_2 b_2))
  (+.p16 (sqrt.p16 (quire16->posit16 (quire16-mul-sub (posit16->quire16 (*.p16 b_2 b_2)) c a))) b_2)
  (real->posit16 1.0)
  (posit16->quire16 (-.p16 (sqrt.p16 (quire16->posit16 (quire16-mul-sub (posit16->quire16 (*.p16 b_2 b_2)) c a))) b_2))
  (quire16-mul-sub (posit16->quire16 (sqrt.p16 (quire16->posit16 (quire16-mul-sub (posit16->quire16 (*.p16 b_2 b_2)) c a)))) b_2 (real->posit16 1.0))
  (real->posit16 0.0)
  (real->posit16 0.0)
  (real->posit16 0.0)
  (real->posit16 1.0)
  (real->posit16 1.0)
  (real->posit16 1.0)
  (/.p16 a (-.p16 (sqrt.p16 (quire16->posit16 (quire16-mul-sub (posit16->quire16 (*.p16 b_2 b_2)) c a))) b_2))
  (/.p16 a (-.p16 (sqrt.p16 (quire16->posit16 (quire16-mul-sub (posit16->quire16 (*.p16 b_2 b_2)) c a))) b_2))
  (/.p16 a (real->posit16 1.0))
  (*.p16 a (+.p16 (sqrt.p16 (quire16->posit16 (quire16-mul-sub (posit16->quire16 (*.p16 b_2 b_2)) c a))) b_2))
  (*.p16 a (real->posit16 1.0))
  (real->posit16 1.0)
  (posit16->quire16 (/.p16 (-.p16 (sqrt.p16 (quire16->posit16 (quire16-mul-sub (posit16->quire16 (*.p16 b_2 b_2)) c a))) b_2) a))
  (real->posit16 0.0)
  (real->posit16 0.0)
  (real->posit16 0.0)
  (real->posit16 1.0)
  (real->posit16 1.0)
  (real->posit16 1.0)
  (real->posit16 1.0)
  (posit16->quire16 (sqrt.p16 (quire16->posit16 (quire16-mul-sub (posit16->quire16 (*.p16 b_2 b_2)) c a))))
  (real->posit16 0.0)
  (real->posit16 0.0)
  (real->posit16 0.0)
  (real->posit16 1.0)
  (real->posit16 1.0)
  (real->posit16 1.0)
  (quire16-mul-sub (posit16->quire16 (*.p16 b_2 b_2)) c a)
  (quire16-mul-sub (posit16->quire16 (*.p16 b_2 b_2)) c a)
  (quire16-mul-sub (posit16->quire16 (*.p16 b_2 b_2)) c a)
  (quire16-mul-sub (posit16->quire16 (*.p16 b_2 b_2)) c a)
27.798 * * [simplify]: iteration 1: (28 enodes)
27.810 * * [simplify]: iteration 2: (41 enodes)
27.823 * * [simplify]: iteration 3: (53 enodes)
27.840 * * [simplify]: iteration 4: (114 enodes)
27.882 * * [simplify]: iteration 5: (332 enodes)
28.128 * * [simplify]: iteration 6: (1681 enodes)
90.043 * * [simplify]: Extracting #0: cost 15 inf + 0
90.043 * * [simplify]: Extracting #1: cost 147 inf + 2
90.044 * * [simplify]: Extracting #2: cost 184 inf + 2340
90.047 * * [simplify]: Extracting #3: cost 133 inf + 44282
90.059 * * [simplify]: Extracting #4: cost 15 inf + 141244
90.080 * * [simplify]: Extracting #5: cost 1 inf + 156969
90.097 * * [simplify]: Extracting #6: cost 0 inf + 157812
90.127 * [simplify]: Simplified to:
  (-.p16 (sqrt.p16 (quire16->posit16 (quire16-mul-sub (posit16->quire16 (*.p16 b_2 b_2)) c a))) b_2)
  (neg.p16 b_2)
  b_2
  (neg.p16 b_2)
  (-.p16 (*.p16 (sqrt.p16 (quire16->posit16 (quire16-mul-sub (posit16->quire16 (*.p16 b_2 b_2)) c a))) (sqrt.p16 (quire16->posit16 (quire16-mul-sub (posit16->quire16 (*.p16 b_2 b_2)) c a)))) (*.p16 b_2 b_2))
  (+.p16 b_2 (sqrt.p16 (quire16->posit16 (quire16-mul-sub (posit16->quire16 (*.p16 b_2 b_2)) c a))))
  (real->posit16 1.0)
  (posit16->quire16 (-.p16 (sqrt.p16 (quire16->posit16 (quire16-mul-sub (posit16->quire16 (*.p16 b_2 b_2)) c a))) b_2))
  (quire16-mul-sub (posit16->quire16 (sqrt.p16 (quire16->posit16 (quire16-mul-sub (posit16->quire16 (*.p16 b_2 b_2)) c a)))) b_2 (real->posit16 1.0))
  (real->posit16 0.0)
  (real->posit16 0.0)
  (real->posit16 0.0)
  (real->posit16 1.0)
  (real->posit16 1.0)
  (real->posit16 1.0)
  (/.p16 a (-.p16 (sqrt.p16 (quire16->posit16 (quire16-mul-sub (posit16->quire16 (*.p16 b_2 b_2)) c a))) b_2))
  (/.p16 a (-.p16 (sqrt.p16 (quire16->posit16 (quire16-mul-sub (posit16->quire16 (*.p16 b_2 b_2)) c a))) b_2))
  a
  (*.p16 (+.p16 b_2 (sqrt.p16 (quire16->posit16 (quire16-mul-sub (posit16->quire16 (*.p16 b_2 b_2)) c a)))) a)
  a
  (real->posit16 1.0)
  (posit16->quire16 (/.p16 (-.p16 (sqrt.p16 (quire16->posit16 (quire16-mul-sub (posit16->quire16 (*.p16 b_2 b_2)) c a))) b_2) a))
  (real->posit16 0.0)
  (real->posit16 0.0)
  (real->posit16 0.0)
  (real->posit16 1.0)
  (real->posit16 1.0)
  (real->posit16 1.0)
  (real->posit16 1.0)
  (posit16->quire16 (sqrt.p16 (quire16->posit16 (quire16-mul-sub (posit16->quire16 (*.p16 b_2 b_2)) c a))))
  (real->posit16 0.0)
  (real->posit16 0.0)
  (real->posit16 0.0)
  (real->posit16 1.0)
  (real->posit16 1.0)
  (real->posit16 1.0)
  (quire16-mul-sub (posit16->quire16 (*.p16 b_2 b_2)) c a)
  (quire16-mul-sub (posit16->quire16 (*.p16 b_2 b_2)) c a)
  (quire16-mul-sub (posit16->quire16 (*.p16 b_2 b_2)) c a)
  (quire16-mul-sub (posit16->quire16 (*.p16 b_2 b_2)) c a)
90.130 * * * [progress]: adding candidates to table
91.326 * * [progress]: iteration 3 / 4
91.326 * * * [progress]: picking best candidate
91.392 * * * * [pick]: Picked  #<alt (λ (a b_2 c) (/.p16 (real->posit16 1.0) (/.p16 a (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2))))>
91.392 * * * [progress]: localizing error
91.569 * * * [progress]: generating rewritten candidates
91.569 * * * * [progress]: [ 1 / 4 ] rewriting at (2 2 2)
91.572 * * * * [progress]: [ 2 / 4 ] rewriting at (2 2)
91.575 * * * * [progress]: [ 3 / 4 ] rewriting at (2 2 2 1 1)
91.579 * * * * [progress]: [ 4 / 4 ] rewriting at (2 2 2 1)
91.580 * * * [progress]: generating series expansions
91.580 * * * * [progress]: [ 1 / 4 ] generating series at (2 2 2)
91.580 * * * * [progress]: [ 2 / 4 ] generating series at (2 2)
91.580 * * * * [progress]: [ 3 / 4 ] generating series at (2 2 2 1 1)
91.580 * * * * [progress]: [ 4 / 4 ] generating series at (2 2 2 1)
91.580 * * * [progress]: simplifying candidates
91.580 * * * * [progress]: [ 1 / 57 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (real->posit16 1.0) (/.p16 a (+.p16 (real->posit16 0.0) (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)))))>
91.580 * * * * [progress]: [ 2 / 57 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (real->posit16 1.0) (/.p16 a (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) (-.p16 (real->posit16 0.0) b_2)))))>
91.580 * * * * [progress]: [ 3 / 57 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (real->posit16 1.0) (/.p16 a (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) (+.p16 (real->posit16 0.0) b_2)))))>
91.580 * * * * [progress]: [ 4 / 57 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (real->posit16 1.0) (/.p16 a (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) (neg.p16 b_2)))))>
91.580 * * * * [progress]: [ 5 / 57 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (real->posit16 1.0) (/.p16 a (/.p16 (-.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) (*.p16 b_2 b_2)) (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)))))>
91.580 * * * * [progress]: [ 6 / 57 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (real->posit16 1.0) (/.p16 a (*.p16 (real->posit16 1.0) (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)))))>
91.580 * * * * [progress]: [ 7 / 57 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (real->posit16 1.0) (/.p16 a (quire16->posit16 (posit16->quire16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2))))))>
91.580 * * * * [progress]: [ 8 / 57 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (real->posit16 1.0) (/.p16 a (quire16->posit16 (quire16-mul-sub (posit16->quire16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) b_2 (real->posit16 1.0))))))>
91.580 * * * * [progress]: [ 9 / 57 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (real->posit16 1.0) (/.p16 a (+.p16 (real->posit16 0.0) (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)))))>
91.580 * * * * [progress]: [ 10 / 57 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (real->posit16 1.0) (/.p16 a (+.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) (real->posit16 0.0)))))>
91.581 * * * * [progress]: [ 11 / 57 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (real->posit16 1.0) (/.p16 a (-.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) (real->posit16 0.0)))))>
91.581 * * * * [progress]: [ 12 / 57 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (real->posit16 1.0) (/.p16 a (*.p16 (real->posit16 1.0) (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)))))>
91.581 * * * * [progress]: [ 13 / 57 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (real->posit16 1.0) (/.p16 a (*.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) (real->posit16 1.0)))))>
91.581 * * * * [progress]: [ 14 / 57 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (real->posit16 1.0) (/.p16 a (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) (real->posit16 1.0)))))>
91.581 * * * * [progress]: [ 15 / 57 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (real->posit16 1.0) (/.p16 (/.p16 a (real->posit16 1.0)) (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2))))>
91.581 * * * * [progress]: [ 16 / 57 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (real->posit16 1.0) (/.p16 (/.p16 a (real->posit16 1.0)) (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2))))>
91.581 * * * * [progress]: [ 17 / 57 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (real->posit16 1.0) (/.p16 (/.p16 a (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)) (real->posit16 1.0))))>
91.581 * * * * [progress]: [ 18 / 57 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (real->posit16 1.0) (*.p16 (/.p16 a (-.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) (*.p16 b_2 b_2))) (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2))))>
91.581 * * * * [progress]: [ 19 / 57 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (real->posit16 1.0) (*.p16 (/.p16 a (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)) (real->posit16 1.0))))>
91.581 * * * * [progress]: [ 20 / 57 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (real->posit16 1.0) (*.p16 (real->posit16 1.0) (/.p16 a (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)))))>
91.581 * * * * [progress]: [ 21 / 57 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (real->posit16 1.0) (quire16->posit16 (posit16->quire16 (/.p16 a (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2))))))>
91.581 * * * * [progress]: [ 22 / 57 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (real->posit16 1.0) (+.p16 (real->posit16 0.0) (/.p16 a (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)))))>
91.581 * * * * [progress]: [ 23 / 57 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (real->posit16 1.0) (+.p16 (/.p16 a (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)) (real->posit16 0.0))))>
91.581 * * * * [progress]: [ 24 / 57 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (real->posit16 1.0) (-.p16 (/.p16 a (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)) (real->posit16 0.0))))>
91.581 * * * * [progress]: [ 25 / 57 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (real->posit16 1.0) (*.p16 (real->posit16 1.0) (/.p16 a (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)))))>
91.581 * * * * [progress]: [ 26 / 57 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (real->posit16 1.0) (*.p16 (/.p16 a (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)) (real->posit16 1.0))))>
91.581 * * * * [progress]: [ 27 / 57 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (real->posit16 1.0) (/.p16 (/.p16 a (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)) (real->posit16 1.0))))>
91.581 * * * * [progress]: [ 28 / 57 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (real->posit16 1.0) (/.p16 a (-.p16 (sqrt.p16 (-.p16 (-.p16 (*.p16 b_2 b_2) (real->posit16 0.0)) (*.p16 c a))) b_2))))>
91.581 * * * * [progress]: [ 29 / 57 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (real->posit16 1.0) (/.p16 a (-.p16 (sqrt.p16 (-.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)) (real->posit16 0.0))) b_2))))>
91.581 * * * * [progress]: [ 30 / 57 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (real->posit16 1.0) (/.p16 a (-.p16 (sqrt.p16 (+.p16 (real->posit16 0.0) (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) b_2))))>
91.581 * * * * [progress]: [ 31 / 57 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (real->posit16 1.0) (/.p16 a (-.p16 (sqrt.p16 (+.p16 (*.p16 b_2 b_2) (-.p16 (real->posit16 0.0) (*.p16 c a)))) b_2))))>
91.581 * * * * [progress]: [ 32 / 57 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (real->posit16 1.0) (/.p16 a (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (+.p16 (real->posit16 0.0) (*.p16 c a)))) b_2))))>
91.581 * * * * [progress]: [ 33 / 57 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (real->posit16 1.0) (/.p16 a (-.p16 (sqrt.p16 (+.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)) (real->posit16 0.0))) b_2))))>
91.581 * * * * [progress]: [ 34 / 57 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (real->posit16 1.0) (/.p16 a (-.p16 (sqrt.p16 (+.p16 (*.p16 b_2 b_2) (neg.p16 (*.p16 c a)))) b_2))))>
91.581 * * * * [progress]: [ 35 / 57 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (real->posit16 1.0) (/.p16 a (-.p16 (sqrt.p16 (/.p16 (-.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 c a) (*.p16 c a))) (+.p16 (*.p16 b_2 b_2) (*.p16 c a)))) b_2))))>
91.581 * * * * [progress]: [ 36 / 57 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (real->posit16 1.0) (/.p16 a (-.p16 (sqrt.p16 (*.p16 (real->posit16 1.0) (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) b_2))))>
91.582 * * * * [progress]: [ 37 / 57 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (real->posit16 1.0) (/.p16 a (-.p16 (sqrt.p16 (quire16->posit16 (posit16->quire16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))))) b_2))))>
91.582 * * * * [progress]: [ 38 / 57 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (real->posit16 1.0) (/.p16 a (-.p16 (sqrt.p16 (quire16->posit16 (quire16-mul-sub (posit16->quire16 (*.p16 b_2 b_2)) (*.p16 c a) (real->posit16 1.0)))) b_2))))>
91.582 * * * * [progress]: [ 39 / 57 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (real->posit16 1.0) (/.p16 a (-.p16 (sqrt.p16 (quire16->posit16 (quire16-mul-sub (posit16->quire16 (*.p16 b_2 b_2)) c a))) b_2))))>
91.582 * * * * [progress]: [ 40 / 57 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (real->posit16 1.0) (/.p16 a (-.p16 (sqrt.p16 (+.p16 (real->posit16 0.0) (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) b_2))))>
91.582 * * * * [progress]: [ 41 / 57 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (real->posit16 1.0) (/.p16 a (-.p16 (sqrt.p16 (+.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)) (real->posit16 0.0))) b_2))))>
91.582 * * * * [progress]: [ 42 / 57 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (real->posit16 1.0) (/.p16 a (-.p16 (sqrt.p16 (-.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)) (real->posit16 0.0))) b_2))))>
91.582 * * * * [progress]: [ 43 / 57 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (real->posit16 1.0) (/.p16 a (-.p16 (sqrt.p16 (*.p16 (real->posit16 1.0) (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) b_2))))>
91.582 * * * * [progress]: [ 44 / 57 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (real->posit16 1.0) (/.p16 a (-.p16 (sqrt.p16 (*.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)) (real->posit16 1.0))) b_2))))>
91.582 * * * * [progress]: [ 45 / 57 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (real->posit16 1.0) (/.p16 a (-.p16 (sqrt.p16 (/.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)) (real->posit16 1.0))) b_2))))>
91.582 * * * * [progress]: [ 46 / 57 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (real->posit16 1.0) (/.p16 a (-.p16 (*.p16 (real->posit16 1.0) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) b_2))))>
91.582 * * * * [progress]: [ 47 / 57 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (real->posit16 1.0) (/.p16 a (-.p16 (quire16->posit16 (posit16->quire16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))))) b_2))))>
91.582 * * * * [progress]: [ 48 / 57 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (real->posit16 1.0) (/.p16 a (-.p16 (+.p16 (real->posit16 0.0) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) b_2))))>
91.582 * * * * [progress]: [ 49 / 57 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (real->posit16 1.0) (/.p16 a (-.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) (real->posit16 0.0)) b_2))))>
91.582 * * * * [progress]: [ 50 / 57 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (real->posit16 1.0) (/.p16 a (-.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) (real->posit16 0.0)) b_2))))>
91.582 * * * * [progress]: [ 51 / 57 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (real->posit16 1.0) (/.p16 a (-.p16 (*.p16 (real->posit16 1.0) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) b_2))))>
91.582 * * * * [progress]: [ 52 / 57 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (real->posit16 1.0) (/.p16 a (-.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) (real->posit16 1.0)) b_2))))>
91.582 * * * * [progress]: [ 53 / 57 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (real->posit16 1.0) (/.p16 a (-.p16 (/.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) (real->posit16 1.0)) b_2))))>
91.582 * * * * [progress]: [ 54 / 57 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (real->posit16 1.0) (/.p16 a (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2))))>
91.582 * * * * [progress]: [ 55 / 57 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (real->posit16 1.0) (/.p16 a (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2))))>
91.582 * * * * [progress]: [ 56 / 57 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (real->posit16 1.0) (/.p16 a (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2))))>
91.582 * * * * [progress]: [ 57 / 57 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (real->posit16 1.0) (/.p16 a (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2))))>
91.583 * [simplify]: Simplifying:
  (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)
  (-.p16 (real->posit16 0.0) b_2)
  (+.p16 (real->posit16 0.0) b_2)
  (neg.p16 b_2)
  (-.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) (*.p16 b_2 b_2))
  (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)
  (real->posit16 1.0)
  (posit16->quire16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2))
  (quire16-mul-sub (posit16->quire16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) b_2 (real->posit16 1.0))
  (real->posit16 0.0)
  (real->posit16 0.0)
  (real->posit16 0.0)
  (real->posit16 1.0)
  (real->posit16 1.0)
  (real->posit16 1.0)
  (/.p16 a (real->posit16 1.0))
  (/.p16 a (real->posit16 1.0))
  (/.p16 a (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2))
  (/.p16 a (-.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) (*.p16 b_2 b_2)))
  (/.p16 a (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2))
  (real->posit16 1.0)
  (posit16->quire16 (/.p16 a (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)))
  (real->posit16 0.0)
  (real->posit16 0.0)
  (real->posit16 0.0)
  (real->posit16 1.0)
  (real->posit16 1.0)
  (real->posit16 1.0)
  (-.p16 (*.p16 b_2 b_2) (real->posit16 0.0))
  (-.p16 (*.p16 b_2 b_2) (*.p16 c a))
  (-.p16 (*.p16 b_2 b_2) (*.p16 c a))
  (-.p16 (real->posit16 0.0) (*.p16 c a))
  (+.p16 (real->posit16 0.0) (*.p16 c a))
  (-.p16 (*.p16 b_2 b_2) (*.p16 c a))
  (neg.p16 (*.p16 c a))
  (-.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 c a) (*.p16 c a)))
  (+.p16 (*.p16 b_2 b_2) (*.p16 c a))
  (real->posit16 1.0)
  (posit16->quire16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))
  (quire16-mul-sub (posit16->quire16 (*.p16 b_2 b_2)) (*.p16 c a) (real->posit16 1.0))
  (quire16-mul-sub (posit16->quire16 (*.p16 b_2 b_2)) c a)
  (real->posit16 0.0)
  (real->posit16 0.0)
  (real->posit16 0.0)
  (real->posit16 1.0)
  (real->posit16 1.0)
  (real->posit16 1.0)
  (real->posit16 1.0)
  (posit16->quire16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))))
  (real->posit16 0.0)
  (real->posit16 0.0)
  (real->posit16 0.0)
  (real->posit16 1.0)
  (real->posit16 1.0)
  (real->posit16 1.0)
  (/.p16 a (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2))
  (/.p16 a (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2))
  (/.p16 a (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2))
  (/.p16 a (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2))
91.583 * * [simplify]: iteration 1: (37 enodes)
91.599 * * [simplify]: iteration 2: (63 enodes)
91.611 * * [simplify]: iteration 3: (182 enodes)
91.763 * * [simplify]: iteration 4: (936 enodes)
102.219 * * [simplify]: Extracting #0: cost 23 inf + 0
102.221 * * [simplify]: Extracting #1: cost 1078 inf + 2
102.235 * * [simplify]: Extracting #2: cost 1361 inf + 125594
102.301 * * [simplify]: Extracting #3: cost 418 inf + 697441
102.389 * * [simplify]: Extracting #4: cost 48 inf + 963298
102.460 * * [simplify]: Extracting #5: cost 0 inf + 1007989
102.529 * [simplify]: Simplified to:
  (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))) b_2)
  (neg.p16 b_2)
  b_2
  (neg.p16 b_2)
  (-.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c)))) (*.p16 b_2 b_2))
  (+.p16 b_2 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))))
  (real->posit16 1.0)
  (posit16->quire16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))) b_2))
  (quire16-mul-sub (posit16->quire16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c)))) b_2 (real->posit16 1.0))
  (real->posit16 0.0)
  (real->posit16 0.0)
  (real->posit16 0.0)
  (real->posit16 1.0)
  (real->posit16 1.0)
  (real->posit16 1.0)
  a
  a
  (/.p16 a (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))) b_2))
  (/.p16 a (-.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c)))) (*.p16 b_2 b_2)))
  (/.p16 a (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))) b_2))
  (real->posit16 1.0)
  (posit16->quire16 (/.p16 a (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))) b_2)))
  (real->posit16 0.0)
  (real->posit16 0.0)
  (real->posit16 0.0)
  (real->posit16 1.0)
  (real->posit16 1.0)
  (real->posit16 1.0)
  (*.p16 b_2 b_2)
  (-.p16 (*.p16 b_2 b_2) (*.p16 a c))
  (-.p16 (*.p16 b_2 b_2) (*.p16 a c))
  (neg.p16 (*.p16 a c))
  (*.p16 a c)
  (-.p16 (*.p16 b_2 b_2) (*.p16 a c))
  (neg.p16 (*.p16 a c))
  (*.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c)) (+.p16 (*.p16 a c) (*.p16 b_2 b_2)))
  (+.p16 (*.p16 a c) (*.p16 b_2 b_2))
  (real->posit16 1.0)
  (posit16->quire16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c)))
  (quire16-mul-sub (posit16->quire16 (*.p16 b_2 b_2)) (*.p16 a c) (real->posit16 1.0))
  (quire16-mul-sub (posit16->quire16 (*.p16 b_2 b_2)) c a)
  (real->posit16 0.0)
  (real->posit16 0.0)
  (real->posit16 0.0)
  (real->posit16 1.0)
  (real->posit16 1.0)
  (real->posit16 1.0)
  (real->posit16 1.0)
  (posit16->quire16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))))
  (real->posit16 0.0)
  (real->posit16 0.0)
  (real->posit16 0.0)
  (real->posit16 1.0)
  (real->posit16 1.0)
  (real->posit16 1.0)
  (/.p16 a (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))) b_2))
  (/.p16 a (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))) b_2))
  (/.p16 a (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))) b_2))
  (/.p16 a (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))) b_2))
102.533 * * * [progress]: adding candidates to table
104.566 * * [progress]: iteration 4 / 4
104.566 * * * [progress]: picking best candidate
104.646 * * * * [pick]: Picked  #<alt (λ (a b_2 c) (/.p16 (-.p16 (sqrt.p16 (/.p16 (-.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 c a) (*.p16 c a))) (+.p16 (*.p16 b_2 b_2) (*.p16 c a)))) b_2) a))>
104.646 * * * [progress]: localizing error
104.846 * * * [progress]: generating rewritten candidates
104.846 * * * * [progress]: [ 1 / 4 ] rewriting at (2 1 1 1)
104.855 * * * * [progress]: [ 2 / 4 ] rewriting at (2 1)
104.858 * * * * [progress]: [ 3 / 4 ] rewriting at (2)
104.861 * * * * [progress]: [ 4 / 4 ] rewriting at (2 1 1)
104.862 * * * [progress]: generating series expansions
104.862 * * * * [progress]: [ 1 / 4 ] generating series at (2 1 1 1)
104.862 * * * * [progress]: [ 2 / 4 ] generating series at (2 1)
104.862 * * * * [progress]: [ 3 / 4 ] generating series at (2)
104.862 * * * * [progress]: [ 4 / 4 ] generating series at (2 1 1)
104.862 * * * [progress]: simplifying candidates
104.862 * * * * [progress]: [ 1 / 69 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (-.p16 (sqrt.p16 (/.p16 (/.p16 (-.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 c a) (*.p16 c a))) (real->posit16 1.0)) (+.p16 (*.p16 b_2 b_2) (*.p16 c a)))) b_2) a))>
104.862 * * * * [progress]: [ 2 / 69 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (-.p16 (sqrt.p16 (/.p16 (/.p16 (-.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 c a) (*.p16 c a))) (real->posit16 1.0)) (+.p16 (*.p16 b_2 b_2) (*.p16 c a)))) b_2) a))>
104.862 * * * * [progress]: [ 3 / 69 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (-.p16 (sqrt.p16 (/.p16 (/.p16 (-.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 c a) (*.p16 c a))) (+.p16 (*.p16 b_2 b_2) (*.p16 c a))) (real->posit16 1.0))) b_2) a))>
104.862 * * * * [progress]: [ 4 / 69 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (-.p16 (sqrt.p16 (/.p16 (+.p16 (*.p16 b_2 b_2) (*.p16 c a)) (/.p16 (+.p16 (*.p16 b_2 b_2) (*.p16 c a)) (-.p16 (*.p16 b_2 b_2) (*.p16 c a))))) b_2) a))>
104.862 * * * * [progress]: [ 5 / 69 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (-.p16 (sqrt.p16 (/.p16 (real->posit16 1.0) (/.p16 (+.p16 (*.p16 b_2 b_2) (*.p16 c a)) (-.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 c a) (*.p16 c a)))))) b_2) a))>
104.862 * * * * [progress]: [ 6 / 69 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (-.p16 (sqrt.p16 (/.p16 (real->posit16 1.0) (/.p16 (+.p16 (*.p16 b_2 b_2) (*.p16 c a)) (-.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 c a) (*.p16 c a)))))) b_2) a))>
104.863 * * * * [progress]: [ 7 / 69 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (-.p16 (sqrt.p16 (/.p16 (-.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 c a) (*.p16 c a))) (/.p16 (+.p16 (*.p16 b_2 b_2) (*.p16 c a)) (real->posit16 1.0)))) b_2) a))>
104.863 * * * * [progress]: [ 8 / 69 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (-.p16 (sqrt.p16 (*.p16 (/.p16 (-.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 c a) (*.p16 c a))) (+.p16 (*.p16 b_2 b_2) (*.p16 c a))) (real->posit16 1.0))) b_2) a))>
104.863 * * * * [progress]: [ 9 / 69 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (-.p16 (sqrt.p16 (/.p16 (-.p16 (*.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2))) (*.p16 (*.p16 (*.p16 c a) (*.p16 c a)) (*.p16 (*.p16 c a) (*.p16 c a)))) (*.p16 (+.p16 (*.p16 b_2 b_2) (*.p16 c a)) (+.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 c a) (*.p16 c a)))))) b_2) a))>
104.863 * * * * [progress]: [ 10 / 69 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (-.p16 (sqrt.p16 (/.p16 (-.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 c a) (*.p16 c a))) (*.p16 (+.p16 (*.p16 b_2 b_2) (*.p16 c a)) (real->posit16 1.0)))) b_2) a))>
104.863 * * * * [progress]: [ 11 / 69 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (-.p16 (sqrt.p16 (*.p16 (real->posit16 1.0) (/.p16 (-.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 c a) (*.p16 c a))) (+.p16 (*.p16 b_2 b_2) (*.p16 c a))))) b_2) a))>
104.863 * * * * [progress]: [ 12 / 69 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (-.p16 (sqrt.p16 (*.p16 (/.p16 (+.p16 (*.p16 b_2 b_2) (*.p16 c a)) (real->posit16 1.0)) (/.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)) (+.p16 (*.p16 b_2 b_2) (*.p16 c a))))) b_2) a))>
104.863 * * * * [progress]: [ 13 / 69 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (-.p16 (sqrt.p16 (*.p16 (/.p16 (+.p16 (*.p16 b_2 b_2) (*.p16 c a)) (real->posit16 1.0)) (/.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)) (+.p16 (*.p16 b_2 b_2) (*.p16 c a))))) b_2) a))>
104.863 * * * * [progress]: [ 14 / 69 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (-.p16 (sqrt.p16 (*.p16 (/.p16 (+.p16 (*.p16 b_2 b_2) (*.p16 c a)) (+.p16 (*.p16 b_2 b_2) (*.p16 c a))) (/.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)) (real->posit16 1.0)))) b_2) a))>
104.863 * * * * [progress]: [ 15 / 69 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (-.p16 (sqrt.p16 (*.p16 (/.p16 (real->posit16 1.0) (real->posit16 1.0)) (/.p16 (-.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 c a) (*.p16 c a))) (+.p16 (*.p16 b_2 b_2) (*.p16 c a))))) b_2) a))>
104.863 * * * * [progress]: [ 16 / 69 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (-.p16 (sqrt.p16 (*.p16 (/.p16 (real->posit16 1.0) (real->posit16 1.0)) (/.p16 (-.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 c a) (*.p16 c a))) (+.p16 (*.p16 b_2 b_2) (*.p16 c a))))) b_2) a))>
104.863 * * * * [progress]: [ 17 / 69 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (-.p16 (sqrt.p16 (*.p16 (/.p16 (real->posit16 1.0) (+.p16 (*.p16 b_2 b_2) (*.p16 c a))) (/.p16 (-.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 c a) (*.p16 c a))) (real->posit16 1.0)))) b_2) a))>
104.863 * * * * [progress]: [ 18 / 69 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (-.p16 (sqrt.p16 (*.p16 (/.p16 (real->posit16 1.0) (real->posit16 1.0)) (/.p16 (-.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 c a) (*.p16 c a))) (+.p16 (*.p16 b_2 b_2) (*.p16 c a))))) b_2) a))>
104.863 * * * * [progress]: [ 19 / 69 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (-.p16 (sqrt.p16 (*.p16 (/.p16 (real->posit16 1.0) (real->posit16 1.0)) (/.p16 (-.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 c a) (*.p16 c a))) (+.p16 (*.p16 b_2 b_2) (*.p16 c a))))) b_2) a))>
104.863 * * * * [progress]: [ 20 / 69 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (-.p16 (sqrt.p16 (*.p16 (/.p16 (real->posit16 1.0) (+.p16 (*.p16 b_2 b_2) (*.p16 c a))) (/.p16 (-.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 c a) (*.p16 c a))) (real->posit16 1.0)))) b_2) a))>
104.863 * * * * [progress]: [ 21 / 69 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (-.p16 (sqrt.p16 (*.p16 (/.p16 (-.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 c a) (*.p16 c a))) (real->posit16 1.0)) (/.p16 (real->posit16 1.0) (+.p16 (*.p16 b_2 b_2) (*.p16 c a))))) b_2) a))>
104.863 * * * * [progress]: [ 22 / 69 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (-.p16 (sqrt.p16 (*.p16 (/.p16 (-.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 c a) (*.p16 c a))) (real->posit16 1.0)) (/.p16 (real->posit16 1.0) (+.p16 (*.p16 b_2 b_2) (*.p16 c a))))) b_2) a))>
104.863 * * * * [progress]: [ 23 / 69 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (-.p16 (sqrt.p16 (*.p16 (/.p16 (-.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 c a) (*.p16 c a))) (+.p16 (*.p16 b_2 b_2) (*.p16 c a))) (/.p16 (real->posit16 1.0) (real->posit16 1.0)))) b_2) a))>
104.863 * * * * [progress]: [ 24 / 69 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (-.p16 (sqrt.p16 (quire16->posit16 (posit16->quire16 (/.p16 (-.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 c a) (*.p16 c a))) (+.p16 (*.p16 b_2 b_2) (*.p16 c a)))))) b_2) a))>
104.863 * * * * [progress]: [ 25 / 69 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (-.p16 (sqrt.p16 (+.p16 (real->posit16 0.0) (/.p16 (-.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 c a) (*.p16 c a))) (+.p16 (*.p16 b_2 b_2) (*.p16 c a))))) b_2) a))>
104.863 * * * * [progress]: [ 26 / 69 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (-.p16 (sqrt.p16 (+.p16 (/.p16 (-.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 c a) (*.p16 c a))) (+.p16 (*.p16 b_2 b_2) (*.p16 c a))) (real->posit16 0.0))) b_2) a))>
104.863 * * * * [progress]: [ 27 / 69 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (-.p16 (sqrt.p16 (-.p16 (/.p16 (-.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 c a) (*.p16 c a))) (+.p16 (*.p16 b_2 b_2) (*.p16 c a))) (real->posit16 0.0))) b_2) a))>
104.863 * * * * [progress]: [ 28 / 69 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (-.p16 (sqrt.p16 (*.p16 (real->posit16 1.0) (/.p16 (-.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 c a) (*.p16 c a))) (+.p16 (*.p16 b_2 b_2) (*.p16 c a))))) b_2) a))>
104.863 * * * * [progress]: [ 29 / 69 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (-.p16 (sqrt.p16 (*.p16 (/.p16 (-.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 c a) (*.p16 c a))) (+.p16 (*.p16 b_2 b_2) (*.p16 c a))) (real->posit16 1.0))) b_2) a))>
104.863 * * * * [progress]: [ 30 / 69 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (-.p16 (sqrt.p16 (/.p16 (/.p16 (-.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 c a) (*.p16 c a))) (+.p16 (*.p16 b_2 b_2) (*.p16 c a))) (real->posit16 1.0))) b_2) a))>
104.863 * * * * [progress]: [ 31 / 69 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (+.p16 (real->posit16 0.0) (-.p16 (sqrt.p16 (/.p16 (-.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 c a) (*.p16 c a))) (+.p16 (*.p16 b_2 b_2) (*.p16 c a)))) b_2)) a))>
104.864 * * * * [progress]: [ 32 / 69 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (+.p16 (sqrt.p16 (/.p16 (-.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 c a) (*.p16 c a))) (+.p16 (*.p16 b_2 b_2) (*.p16 c a)))) (-.p16 (real->posit16 0.0) b_2)) a))>
104.864 * * * * [progress]: [ 33 / 69 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (-.p16 (sqrt.p16 (/.p16 (-.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 c a) (*.p16 c a))) (+.p16 (*.p16 b_2 b_2) (*.p16 c a)))) (+.p16 (real->posit16 0.0) b_2)) a))>
104.864 * * * * [progress]: [ 34 / 69 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (+.p16 (sqrt.p16 (/.p16 (-.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 c a) (*.p16 c a))) (+.p16 (*.p16 b_2 b_2) (*.p16 c a)))) (neg.p16 b_2)) a))>
104.864 * * * * [progress]: [ 35 / 69 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (/.p16 (-.p16 (*.p16 (sqrt.p16 (/.p16 (-.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 c a) (*.p16 c a))) (+.p16 (*.p16 b_2 b_2) (*.p16 c a)))) (sqrt.p16 (/.p16 (-.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 c a) (*.p16 c a))) (+.p16 (*.p16 b_2 b_2) (*.p16 c a))))) (*.p16 b_2 b_2)) (+.p16 (sqrt.p16 (/.p16 (-.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 c a) (*.p16 c a))) (+.p16 (*.p16 b_2 b_2) (*.p16 c a)))) b_2)) a))>
104.864 * * * * [progress]: [ 36 / 69 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (*.p16 (real->posit16 1.0) (-.p16 (sqrt.p16 (/.p16 (-.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 c a) (*.p16 c a))) (+.p16 (*.p16 b_2 b_2) (*.p16 c a)))) b_2)) a))>
104.864 * * * * [progress]: [ 37 / 69 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (quire16->posit16 (posit16->quire16 (-.p16 (sqrt.p16 (/.p16 (-.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 c a) (*.p16 c a))) (+.p16 (*.p16 b_2 b_2) (*.p16 c a)))) b_2))) a))>
104.864 * * * * [progress]: [ 38 / 69 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (quire16->posit16 (quire16-mul-sub (posit16->quire16 (sqrt.p16 (/.p16 (-.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 c a) (*.p16 c a))) (+.p16 (*.p16 b_2 b_2) (*.p16 c a))))) b_2 (real->posit16 1.0))) a))>
104.864 * * * * [progress]: [ 39 / 69 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (+.p16 (real->posit16 0.0) (-.p16 (sqrt.p16 (/.p16 (-.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 c a) (*.p16 c a))) (+.p16 (*.p16 b_2 b_2) (*.p16 c a)))) b_2)) a))>
104.864 * * * * [progress]: [ 40 / 69 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (+.p16 (-.p16 (sqrt.p16 (/.p16 (-.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 c a) (*.p16 c a))) (+.p16 (*.p16 b_2 b_2) (*.p16 c a)))) b_2) (real->posit16 0.0)) a))>
104.864 * * * * [progress]: [ 41 / 69 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (-.p16 (-.p16 (sqrt.p16 (/.p16 (-.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 c a) (*.p16 c a))) (+.p16 (*.p16 b_2 b_2) (*.p16 c a)))) b_2) (real->posit16 0.0)) a))>
104.864 * * * * [progress]: [ 42 / 69 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (*.p16 (real->posit16 1.0) (-.p16 (sqrt.p16 (/.p16 (-.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 c a) (*.p16 c a))) (+.p16 (*.p16 b_2 b_2) (*.p16 c a)))) b_2)) a))>
104.864 * * * * [progress]: [ 43 / 69 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (*.p16 (-.p16 (sqrt.p16 (/.p16 (-.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 c a) (*.p16 c a))) (+.p16 (*.p16 b_2 b_2) (*.p16 c a)))) b_2) (real->posit16 1.0)) a))>
104.864 * * * * [progress]: [ 44 / 69 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (/.p16 (-.p16 (sqrt.p16 (/.p16 (-.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 c a) (*.p16 c a))) (+.p16 (*.p16 b_2 b_2) (*.p16 c a)))) b_2) (real->posit16 1.0)) a))>
104.864 * * * * [progress]: [ 45 / 69 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (real->posit16 1.0) (/.p16 a (-.p16 (sqrt.p16 (/.p16 (-.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 c a) (*.p16 c a))) (+.p16 (*.p16 b_2 b_2) (*.p16 c a)))) b_2))))>
104.864 * * * * [progress]: [ 46 / 69 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (real->posit16 1.0) (/.p16 a (-.p16 (sqrt.p16 (/.p16 (-.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 c a) (*.p16 c a))) (+.p16 (*.p16 b_2 b_2) (*.p16 c a)))) b_2))))>
104.864 * * * * [progress]: [ 47 / 69 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (-.p16 (sqrt.p16 (/.p16 (-.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 c a) (*.p16 c a))) (+.p16 (*.p16 b_2 b_2) (*.p16 c a)))) b_2) (/.p16 a (real->posit16 1.0))))>
104.864 * * * * [progress]: [ 48 / 69 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (-.p16 (*.p16 (sqrt.p16 (/.p16 (-.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 c a) (*.p16 c a))) (+.p16 (*.p16 b_2 b_2) (*.p16 c a)))) (sqrt.p16 (/.p16 (-.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 c a) (*.p16 c a))) (+.p16 (*.p16 b_2 b_2) (*.p16 c a))))) (*.p16 b_2 b_2)) (*.p16 a (+.p16 (sqrt.p16 (/.p16 (-.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 c a) (*.p16 c a))) (+.p16 (*.p16 b_2 b_2) (*.p16 c a)))) b_2))))>
104.864 * * * * [progress]: [ 49 / 69 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (-.p16 (sqrt.p16 (/.p16 (-.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 c a) (*.p16 c a))) (+.p16 (*.p16 b_2 b_2) (*.p16 c a)))) b_2) (*.p16 a (real->posit16 1.0))))>
104.864 * * * * [progress]: [ 50 / 69 ] simplifiying candidate #<alt (λ (a b_2 c) (*.p16 (real->posit16 1.0) (/.p16 (-.p16 (sqrt.p16 (/.p16 (-.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 c a) (*.p16 c a))) (+.p16 (*.p16 b_2 b_2) (*.p16 c a)))) b_2) a)))>
104.864 * * * * [progress]: [ 51 / 69 ] simplifiying candidate #<alt (λ (a b_2 c) (quire16->posit16 (posit16->quire16 (/.p16 (-.p16 (sqrt.p16 (/.p16 (-.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 c a) (*.p16 c a))) (+.p16 (*.p16 b_2 b_2) (*.p16 c a)))) b_2) a))))>
104.864 * * * * [progress]: [ 52 / 69 ] simplifiying candidate #<alt (λ (a b_2 c) (+.p16 (real->posit16 0.0) (/.p16 (-.p16 (sqrt.p16 (/.p16 (-.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 c a) (*.p16 c a))) (+.p16 (*.p16 b_2 b_2) (*.p16 c a)))) b_2) a)))>
104.864 * * * * [progress]: [ 53 / 69 ] simplifiying candidate #<alt (λ (a b_2 c) (+.p16 (/.p16 (-.p16 (sqrt.p16 (/.p16 (-.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 c a) (*.p16 c a))) (+.p16 (*.p16 b_2 b_2) (*.p16 c a)))) b_2) a) (real->posit16 0.0)))>
104.864 * * * * [progress]: [ 54 / 69 ] simplifiying candidate #<alt (λ (a b_2 c) (-.p16 (/.p16 (-.p16 (sqrt.p16 (/.p16 (-.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 c a) (*.p16 c a))) (+.p16 (*.p16 b_2 b_2) (*.p16 c a)))) b_2) a) (real->posit16 0.0)))>
104.864 * * * * [progress]: [ 55 / 69 ] simplifiying candidate #<alt (λ (a b_2 c) (*.p16 (real->posit16 1.0) (/.p16 (-.p16 (sqrt.p16 (/.p16 (-.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 c a) (*.p16 c a))) (+.p16 (*.p16 b_2 b_2) (*.p16 c a)))) b_2) a)))>
104.864 * * * * [progress]: [ 56 / 69 ] simplifiying candidate #<alt (λ (a b_2 c) (*.p16 (/.p16 (-.p16 (sqrt.p16 (/.p16 (-.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 c a) (*.p16 c a))) (+.p16 (*.p16 b_2 b_2) (*.p16 c a)))) b_2) a) (real->posit16 1.0)))>
104.864 * * * * [progress]: [ 57 / 69 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (/.p16 (-.p16 (sqrt.p16 (/.p16 (-.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 c a) (*.p16 c a))) (+.p16 (*.p16 b_2 b_2) (*.p16 c a)))) b_2) a) (real->posit16 1.0)))>
104.865 * * * * [progress]: [ 58 / 69 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (-.p16 (*.p16 (real->posit16 1.0) (sqrt.p16 (/.p16 (-.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 c a) (*.p16 c a))) (+.p16 (*.p16 b_2 b_2) (*.p16 c a))))) b_2) a))>
104.865 * * * * [progress]: [ 59 / 69 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (-.p16 (quire16->posit16 (posit16->quire16 (sqrt.p16 (/.p16 (-.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 c a) (*.p16 c a))) (+.p16 (*.p16 b_2 b_2) (*.p16 c a)))))) b_2) a))>
104.865 * * * * [progress]: [ 60 / 69 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (-.p16 (+.p16 (real->posit16 0.0) (sqrt.p16 (/.p16 (-.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 c a) (*.p16 c a))) (+.p16 (*.p16 b_2 b_2) (*.p16 c a))))) b_2) a))>
104.865 * * * * [progress]: [ 61 / 69 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (-.p16 (+.p16 (sqrt.p16 (/.p16 (-.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 c a) (*.p16 c a))) (+.p16 (*.p16 b_2 b_2) (*.p16 c a)))) (real->posit16 0.0)) b_2) a))>
104.865 * * * * [progress]: [ 62 / 69 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (-.p16 (-.p16 (sqrt.p16 (/.p16 (-.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 c a) (*.p16 c a))) (+.p16 (*.p16 b_2 b_2) (*.p16 c a)))) (real->posit16 0.0)) b_2) a))>
104.865 * * * * [progress]: [ 63 / 69 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (-.p16 (*.p16 (real->posit16 1.0) (sqrt.p16 (/.p16 (-.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 c a) (*.p16 c a))) (+.p16 (*.p16 b_2 b_2) (*.p16 c a))))) b_2) a))>
104.865 * * * * [progress]: [ 64 / 69 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (-.p16 (*.p16 (sqrt.p16 (/.p16 (-.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 c a) (*.p16 c a))) (+.p16 (*.p16 b_2 b_2) (*.p16 c a)))) (real->posit16 1.0)) b_2) a))>
104.865 * * * * [progress]: [ 65 / 69 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (-.p16 (/.p16 (sqrt.p16 (/.p16 (-.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 c a) (*.p16 c a))) (+.p16 (*.p16 b_2 b_2) (*.p16 c a)))) (real->posit16 1.0)) b_2) a))>
104.865 * * * * [progress]: [ 66 / 69 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (-.p16 (sqrt.p16 (/.p16 (-.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 c a) (*.p16 c a))) (+.p16 (*.p16 b_2 b_2) (*.p16 c a)))) b_2) a))>
104.865 * * * * [progress]: [ 67 / 69 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (-.p16 (sqrt.p16 (/.p16 (-.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 c a) (*.p16 c a))) (+.p16 (*.p16 b_2 b_2) (*.p16 c a)))) b_2) a))>
104.865 * * * * [progress]: [ 68 / 69 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (-.p16 (sqrt.p16 (/.p16 (-.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 c a) (*.p16 c a))) (+.p16 (*.p16 b_2 b_2) (*.p16 c a)))) b_2) a))>
104.865 * * * * [progress]: [ 69 / 69 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (-.p16 (sqrt.p16 (/.p16 (-.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 c a) (*.p16 c a))) (+.p16 (*.p16 b_2 b_2) (*.p16 c a)))) b_2) a))>
104.866 * [simplify]: Simplifying:
  (/.p16 (-.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 c a) (*.p16 c a))) (real->posit16 1.0))
  (/.p16 (-.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 c a) (*.p16 c a))) (real->posit16 1.0))
  (/.p16 (-.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 c a) (*.p16 c a))) (+.p16 (*.p16 b_2 b_2) (*.p16 c a)))
  (/.p16 (+.p16 (*.p16 b_2 b_2) (*.p16 c a)) (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))
  (/.p16 (+.p16 (*.p16 b_2 b_2) (*.p16 c a)) (-.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 c a) (*.p16 c a))))
  (/.p16 (+.p16 (*.p16 b_2 b_2) (*.p16 c a)) (-.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 c a) (*.p16 c a))))
  (/.p16 (+.p16 (*.p16 b_2 b_2) (*.p16 c a)) (real->posit16 1.0))
  (/.p16 (-.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 c a) (*.p16 c a))) (+.p16 (*.p16 b_2 b_2) (*.p16 c a)))
  (*.p16 (+.p16 (*.p16 b_2 b_2) (*.p16 c a)) (+.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 c a) (*.p16 c a))))
  (*.p16 (+.p16 (*.p16 b_2 b_2) (*.p16 c a)) (real->posit16 1.0))
  (real->posit16 1.0)
  (/.p16 (+.p16 (*.p16 b_2 b_2) (*.p16 c a)) (real->posit16 1.0))
  (/.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)) (+.p16 (*.p16 b_2 b_2) (*.p16 c a)))
  (/.p16 (+.p16 (*.p16 b_2 b_2) (*.p16 c a)) (real->posit16 1.0))
  (/.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)) (+.p16 (*.p16 b_2 b_2) (*.p16 c a)))
  (/.p16 (+.p16 (*.p16 b_2 b_2) (*.p16 c a)) (+.p16 (*.p16 b_2 b_2) (*.p16 c a)))
  (/.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)) (real->posit16 1.0))
  (/.p16 (real->posit16 1.0) (real->posit16 1.0))
  (/.p16 (-.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 c a) (*.p16 c a))) (+.p16 (*.p16 b_2 b_2) (*.p16 c a)))
  (/.p16 (real->posit16 1.0) (real->posit16 1.0))
  (/.p16 (-.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 c a) (*.p16 c a))) (+.p16 (*.p16 b_2 b_2) (*.p16 c a)))
  (/.p16 (real->posit16 1.0) (+.p16 (*.p16 b_2 b_2) (*.p16 c a)))
  (/.p16 (-.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 c a) (*.p16 c a))) (real->posit16 1.0))
  (/.p16 (real->posit16 1.0) (real->posit16 1.0))
  (/.p16 (-.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 c a) (*.p16 c a))) (+.p16 (*.p16 b_2 b_2) (*.p16 c a)))
  (/.p16 (real->posit16 1.0) (real->posit16 1.0))
  (/.p16 (-.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 c a) (*.p16 c a))) (+.p16 (*.p16 b_2 b_2) (*.p16 c a)))
  (/.p16 (real->posit16 1.0) (+.p16 (*.p16 b_2 b_2) (*.p16 c a)))
  (/.p16 (-.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 c a) (*.p16 c a))) (real->posit16 1.0))
  (/.p16 (-.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 c a) (*.p16 c a))) (real->posit16 1.0))
  (/.p16 (real->posit16 1.0) (+.p16 (*.p16 b_2 b_2) (*.p16 c a)))
  (/.p16 (-.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 c a) (*.p16 c a))) (real->posit16 1.0))
  (/.p16 (real->posit16 1.0) (+.p16 (*.p16 b_2 b_2) (*.p16 c a)))
  (/.p16 (-.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 c a) (*.p16 c a))) (+.p16 (*.p16 b_2 b_2) (*.p16 c a)))
  (/.p16 (real->posit16 1.0) (real->posit16 1.0))
  (posit16->quire16 (/.p16 (-.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 c a) (*.p16 c a))) (+.p16 (*.p16 b_2 b_2) (*.p16 c a))))
  (real->posit16 0.0)
  (real->posit16 0.0)
  (real->posit16 0.0)
  (real->posit16 1.0)
  (real->posit16 1.0)
  (real->posit16 1.0)
  (-.p16 (sqrt.p16 (/.p16 (-.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 c a) (*.p16 c a))) (+.p16 (*.p16 b_2 b_2) (*.p16 c a)))) b_2)
  (-.p16 (real->posit16 0.0) b_2)
  (+.p16 (real->posit16 0.0) b_2)
  (neg.p16 b_2)
  (-.p16 (*.p16 (sqrt.p16 (/.p16 (-.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 c a) (*.p16 c a))) (+.p16 (*.p16 b_2 b_2) (*.p16 c a)))) (sqrt.p16 (/.p16 (-.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 c a) (*.p16 c a))) (+.p16 (*.p16 b_2 b_2) (*.p16 c a))))) (*.p16 b_2 b_2))
  (+.p16 (sqrt.p16 (/.p16 (-.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 c a) (*.p16 c a))) (+.p16 (*.p16 b_2 b_2) (*.p16 c a)))) b_2)
  (real->posit16 1.0)
  (posit16->quire16 (-.p16 (sqrt.p16 (/.p16 (-.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 c a) (*.p16 c a))) (+.p16 (*.p16 b_2 b_2) (*.p16 c a)))) b_2))
  (quire16-mul-sub (posit16->quire16 (sqrt.p16 (/.p16 (-.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 c a) (*.p16 c a))) (+.p16 (*.p16 b_2 b_2) (*.p16 c a))))) b_2 (real->posit16 1.0))
  (real->posit16 0.0)
  (real->posit16 0.0)
  (real->posit16 0.0)
  (real->posit16 1.0)
  (real->posit16 1.0)
  (real->posit16 1.0)
  (/.p16 a (-.p16 (sqrt.p16 (/.p16 (-.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 c a) (*.p16 c a))) (+.p16 (*.p16 b_2 b_2) (*.p16 c a)))) b_2))
  (/.p16 a (-.p16 (sqrt.p16 (/.p16 (-.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 c a) (*.p16 c a))) (+.p16 (*.p16 b_2 b_2) (*.p16 c a)))) b_2))
  (/.p16 a (real->posit16 1.0))
  (*.p16 a (+.p16 (sqrt.p16 (/.p16 (-.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 c a) (*.p16 c a))) (+.p16 (*.p16 b_2 b_2) (*.p16 c a)))) b_2))
  (*.p16 a (real->posit16 1.0))
  (real->posit16 1.0)
  (posit16->quire16 (/.p16 (-.p16 (sqrt.p16 (/.p16 (-.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 c a) (*.p16 c a))) (+.p16 (*.p16 b_2 b_2) (*.p16 c a)))) b_2) a))
  (real->posit16 0.0)
  (real->posit16 0.0)
  (real->posit16 0.0)
  (real->posit16 1.0)
  (real->posit16 1.0)
  (real->posit16 1.0)
  (real->posit16 1.0)
  (posit16->quire16 (sqrt.p16 (/.p16 (-.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 c a) (*.p16 c a))) (+.p16 (*.p16 b_2 b_2) (*.p16 c a)))))
  (real->posit16 0.0)
  (real->posit16 0.0)
  (real->posit16 0.0)
  (real->posit16 1.0)
  (real->posit16 1.0)
  (real->posit16 1.0)
  (-.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 c a) (*.p16 c a)))
  (+.p16 (*.p16 b_2 b_2) (*.p16 c a))
  (-.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 c a) (*.p16 c a)))
  (+.p16 (*.p16 b_2 b_2) (*.p16 c a))
  (-.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 c a) (*.p16 c a)))
  (+.p16 (*.p16 b_2 b_2) (*.p16 c a))
  (-.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 c a) (*.p16 c a)))
  (+.p16 (*.p16 b_2 b_2) (*.p16 c a))
104.866 * * [simplify]: iteration 1: (45 enodes)
104.882 * * [simplify]: iteration 2: (82 enodes)
104.898 * * [simplify]: iteration 3: (240 enodes)
105.099 * * [simplify]: iteration 4: (1096 enodes)
107.765 * * [simplify]: Extracting #0: cost 23 inf + 0
107.767 * * [simplify]: Extracting #1: cost 340 inf + 2
107.772 * * [simplify]: Extracting #2: cost 1099 inf + 2504
107.784 * * [simplify]: Extracting #3: cost 1298 inf + 101125
107.817 * * [simplify]: Extracting #4: cost 494 inf + 841687
107.903 * * [simplify]: Extracting #5: cost 72 inf + 1581475
107.998 * * [simplify]: Extracting #6: cost 0 inf + 1731349
108.123 * * [simplify]: Extracting #7: cost 0 inf + 1729749
108.239 * [simplify]: Simplified to:
  (*.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c)) (+.p16 (*.p16 b_2 b_2) (*.p16 a c)))
  (*.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c)) (+.p16 (*.p16 b_2 b_2) (*.p16 a c)))
  (-.p16 (*.p16 b_2 b_2) (*.p16 a c))
  (/.p16 (+.p16 (*.p16 b_2 b_2) (*.p16 a c)) (-.p16 (*.p16 b_2 b_2) (*.p16 a c)))
  (/.p16 (real->posit16 1.0) (-.p16 (*.p16 b_2 b_2) (*.p16 a c)))
  (/.p16 (real->posit16 1.0) (-.p16 (*.p16 b_2 b_2) (*.p16 a c)))
  (+.p16 (*.p16 b_2 b_2) (*.p16 a c))
  (-.p16 (*.p16 b_2 b_2) (*.p16 a c))
  (*.p16 (+.p16 (*.p16 (*.p16 a c) (*.p16 a c)) (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2))) (+.p16 (*.p16 b_2 b_2) (*.p16 a c)))
  (+.p16 (*.p16 b_2 b_2) (*.p16 a c))
  (real->posit16 1.0)
  (+.p16 (*.p16 b_2 b_2) (*.p16 a c))
  (/.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c)) (+.p16 (*.p16 b_2 b_2) (*.p16 a c)))
  (+.p16 (*.p16 b_2 b_2) (*.p16 a c))
  (/.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c)) (+.p16 (*.p16 b_2 b_2) (*.p16 a c)))
  (real->posit16 1.0)
  (-.p16 (*.p16 b_2 b_2) (*.p16 a c))
  (real->posit16 1.0)
  (-.p16 (*.p16 b_2 b_2) (*.p16 a c))
  (real->posit16 1.0)
  (-.p16 (*.p16 b_2 b_2) (*.p16 a c))
  (/.p16 (real->posit16 1.0) (+.p16 (*.p16 b_2 b_2) (*.p16 a c)))
  (*.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c)) (+.p16 (*.p16 b_2 b_2) (*.p16 a c)))
  (real->posit16 1.0)
  (-.p16 (*.p16 b_2 b_2) (*.p16 a c))
  (real->posit16 1.0)
  (-.p16 (*.p16 b_2 b_2) (*.p16 a c))
  (/.p16 (real->posit16 1.0) (+.p16 (*.p16 b_2 b_2) (*.p16 a c)))
  (*.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c)) (+.p16 (*.p16 b_2 b_2) (*.p16 a c)))
  (*.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c)) (+.p16 (*.p16 b_2 b_2) (*.p16 a c)))
  (/.p16 (real->posit16 1.0) (+.p16 (*.p16 b_2 b_2) (*.p16 a c)))
  (*.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c)) (+.p16 (*.p16 b_2 b_2) (*.p16 a c)))
  (/.p16 (real->posit16 1.0) (+.p16 (*.p16 b_2 b_2) (*.p16 a c)))
  (-.p16 (*.p16 b_2 b_2) (*.p16 a c))
  (real->posit16 1.0)
  (posit16->quire16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c)))
  (real->posit16 0.0)
  (real->posit16 0.0)
  (real->posit16 0.0)
  (real->posit16 1.0)
  (real->posit16 1.0)
  (real->posit16 1.0)
  (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))) b_2)
  (neg.p16 b_2)
  b_2
  (neg.p16 b_2)
  (-.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c)))) (*.p16 b_2 b_2))
  (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))) b_2)
  (real->posit16 1.0)
  (posit16->quire16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))) b_2))
  (quire16-mul-sub (posit16->quire16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c)))) b_2 (real->posit16 1.0))
  (real->posit16 0.0)
  (real->posit16 0.0)
  (real->posit16 0.0)
  (real->posit16 1.0)
  (real->posit16 1.0)
  (real->posit16 1.0)
  (/.p16 a (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))) b_2))
  (/.p16 a (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))) b_2))
  a
  (*.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))) b_2) a)
  a
  (real->posit16 1.0)
  (posit16->quire16 (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))) b_2) a))
  (real->posit16 0.0)
  (real->posit16 0.0)
  (real->posit16 0.0)
  (real->posit16 1.0)
  (real->posit16 1.0)
  (real->posit16 1.0)
  (real->posit16 1.0)
  (posit16->quire16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))))
  (real->posit16 0.0)
  (real->posit16 0.0)
  (real->posit16 0.0)
  (real->posit16 1.0)
  (real->posit16 1.0)
  (real->posit16 1.0)
  (*.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c)) (+.p16 (*.p16 b_2 b_2) (*.p16 a c)))
  (+.p16 (*.p16 b_2 b_2) (*.p16 a c))
  (*.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c)) (+.p16 (*.p16 b_2 b_2) (*.p16 a c)))
  (+.p16 (*.p16 b_2 b_2) (*.p16 a c))
  (*.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c)) (+.p16 (*.p16 b_2 b_2) (*.p16 a c)))
  (+.p16 (*.p16 b_2 b_2) (*.p16 a c))
  (*.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c)) (+.p16 (*.p16 b_2 b_2) (*.p16 a c)))
  (+.p16 (*.p16 b_2 b_2) (*.p16 a c))
108.245 * * * [progress]: adding candidates to table
110.148 * [progress]: [Phase 3 of 3] Extracting.
110.148 * * [regime]: Finding splitpoints for: (#<alt (λ (a b_2 c) (/.p16 (-.p16 (sqrt.p16 (/.p16 (-.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 c a) (*.p16 c a))) (+.p16 (*.p16 b_2 b_2) (*.p16 c a)))) b_2) a))> #<alt (λ (a b_2 c) (/.p16 (-.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) (*.p16 b_2 b_2)) (*.p16 a (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2))))> #<alt (λ (a b_2 c) (/.p16 (real->posit16 1.0) (/.p16 a (/.p16 (-.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) (*.p16 b_2 b_2)) (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)))))> #<alt (λ (a b_2 c) (/.p16 (real->posit16 1.0) (/.p16 a (-.p16 (sqrt.p16 (/.p16 (-.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 c a) (*.p16 c a))) (+.p16 (*.p16 b_2 b_2) (*.p16 c a)))) b_2))))> #<alt (λ (a b_2 c) (/.p16 (-.p16 (*.p16 (sqrt.p16 (quire16->posit16 (quire16-mul-sub (posit16->quire16 (*.p16 b_2 b_2)) c a))) (sqrt.p16 (quire16->posit16 (quire16-mul-sub (posit16->quire16 (*.p16 b_2 b_2)) c a)))) (*.p16 b_2 b_2)) (*.p16 a (+.p16 (sqrt.p16 (quire16->posit16 (quire16-mul-sub (posit16->quire16 (*.p16 b_2 b_2)) c a))) b_2))))> #<alt (λ (a b_2 c) (/.p16 (-.p16 (sqrt.p16 (quire16->posit16 (quire16-mul-sub (posit16->quire16 (*.p16 b_2 b_2)) c a))) b_2) a))> #<alt (λ (a b_2 c) (/.p16 (real->posit16 1.0) (/.p16 a (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2))))> #<alt (λ (a b_2 c) (/.p16 (-.p16 (sqrt.p16 (/.p16 (-.p16 (*.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2))) (*.p16 (*.p16 (*.p16 c a) (*.p16 c a)) (*.p16 (*.p16 c a) (*.p16 c a)))) (*.p16 (+.p16 (*.p16 b_2 b_2) (*.p16 c a)) (+.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 c a) (*.p16 c a)))))) b_2) a))> #<alt (λ (a b_2 c) (/.p16 (real->posit16 1.0) (*.p16 (/.p16 a (-.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) (*.p16 b_2 b_2))) (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2))))> #<alt (λ (a b_2 c) (/.p16 (-.p16 (*.p16 (sqrt.p16 (/.p16 (-.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 c a) (*.p16 c a))) (+.p16 (*.p16 b_2 b_2) (*.p16 c a)))) (sqrt.p16 (/.p16 (-.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 c a) (*.p16 c a))) (+.p16 (*.p16 b_2 b_2) (*.p16 c a))))) (*.p16 b_2 b_2)) (*.p16 a (+.p16 (sqrt.p16 (/.p16 (-.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 c a) (*.p16 c a))) (+.p16 (*.p16 b_2 b_2) (*.p16 c a)))) b_2))))>)
110.156 * * * [regime-changes]: Trying 3 branch expressions: (c b_2 a)
110.156 * * * * [regimes]: Trying to branch on c from (#<alt (λ (a b_2 c) (/.p16 (-.p16 (sqrt.p16 (/.p16 (-.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 c a) (*.p16 c a))) (+.p16 (*.p16 b_2 b_2) (*.p16 c a)))) b_2) a))> #<alt (λ (a b_2 c) (/.p16 (-.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) (*.p16 b_2 b_2)) (*.p16 a (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2))))> #<alt (λ (a b_2 c) (/.p16 (real->posit16 1.0) (/.p16 a (/.p16 (-.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) (*.p16 b_2 b_2)) (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)))))> #<alt (λ (a b_2 c) (/.p16 (real->posit16 1.0) (/.p16 a (-.p16 (sqrt.p16 (/.p16 (-.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 c a) (*.p16 c a))) (+.p16 (*.p16 b_2 b_2) (*.p16 c a)))) b_2))))> #<alt (λ (a b_2 c) (/.p16 (-.p16 (*.p16 (sqrt.p16 (quire16->posit16 (quire16-mul-sub (posit16->quire16 (*.p16 b_2 b_2)) c a))) (sqrt.p16 (quire16->posit16 (quire16-mul-sub (posit16->quire16 (*.p16 b_2 b_2)) c a)))) (*.p16 b_2 b_2)) (*.p16 a (+.p16 (sqrt.p16 (quire16->posit16 (quire16-mul-sub (posit16->quire16 (*.p16 b_2 b_2)) c a))) b_2))))> #<alt (λ (a b_2 c) (/.p16 (-.p16 (sqrt.p16 (quire16->posit16 (quire16-mul-sub (posit16->quire16 (*.p16 b_2 b_2)) c a))) b_2) a))> #<alt (λ (a b_2 c) (/.p16 (real->posit16 1.0) (/.p16 a (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2))))> #<alt (λ (a b_2 c) (/.p16 (-.p16 (sqrt.p16 (/.p16 (-.p16 (*.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2))) (*.p16 (*.p16 (*.p16 c a) (*.p16 c a)) (*.p16 (*.p16 c a) (*.p16 c a)))) (*.p16 (+.p16 (*.p16 b_2 b_2) (*.p16 c a)) (+.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 c a) (*.p16 c a)))))) b_2) a))> #<alt (λ (a b_2 c) (/.p16 (real->posit16 1.0) (*.p16 (/.p16 a (-.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) (*.p16 b_2 b_2))) (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2))))> #<alt (λ (a b_2 c) (/.p16 (-.p16 (*.p16 (sqrt.p16 (/.p16 (-.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 c a) (*.p16 c a))) (+.p16 (*.p16 b_2 b_2) (*.p16 c a)))) (sqrt.p16 (/.p16 (-.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 c a) (*.p16 c a))) (+.p16 (*.p16 b_2 b_2) (*.p16 c a))))) (*.p16 b_2 b_2)) (*.p16 a (+.p16 (sqrt.p16 (/.p16 (-.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 c a) (*.p16 c a))) (+.p16 (*.p16 b_2 b_2) (*.p16 c a)))) b_2))))>)
110.329 * * * * [regimes]: Trying to branch on b_2 from (#<alt (λ (a b_2 c) (/.p16 (-.p16 (sqrt.p16 (/.p16 (-.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 c a) (*.p16 c a))) (+.p16 (*.p16 b_2 b_2) (*.p16 c a)))) b_2) a))> #<alt (λ (a b_2 c) (/.p16 (-.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) (*.p16 b_2 b_2)) (*.p16 a (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2))))> #<alt (λ (a b_2 c) (/.p16 (real->posit16 1.0) (/.p16 a (/.p16 (-.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) (*.p16 b_2 b_2)) (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)))))> #<alt (λ (a b_2 c) (/.p16 (real->posit16 1.0) (/.p16 a (-.p16 (sqrt.p16 (/.p16 (-.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 c a) (*.p16 c a))) (+.p16 (*.p16 b_2 b_2) (*.p16 c a)))) b_2))))> #<alt (λ (a b_2 c) (/.p16 (-.p16 (*.p16 (sqrt.p16 (quire16->posit16 (quire16-mul-sub (posit16->quire16 (*.p16 b_2 b_2)) c a))) (sqrt.p16 (quire16->posit16 (quire16-mul-sub (posit16->quire16 (*.p16 b_2 b_2)) c a)))) (*.p16 b_2 b_2)) (*.p16 a (+.p16 (sqrt.p16 (quire16->posit16 (quire16-mul-sub (posit16->quire16 (*.p16 b_2 b_2)) c a))) b_2))))> #<alt (λ (a b_2 c) (/.p16 (-.p16 (sqrt.p16 (quire16->posit16 (quire16-mul-sub (posit16->quire16 (*.p16 b_2 b_2)) c a))) b_2) a))> #<alt (λ (a b_2 c) (/.p16 (real->posit16 1.0) (/.p16 a (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2))))> #<alt (λ (a b_2 c) (/.p16 (-.p16 (sqrt.p16 (/.p16 (-.p16 (*.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2))) (*.p16 (*.p16 (*.p16 c a) (*.p16 c a)) (*.p16 (*.p16 c a) (*.p16 c a)))) (*.p16 (+.p16 (*.p16 b_2 b_2) (*.p16 c a)) (+.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 c a) (*.p16 c a)))))) b_2) a))> #<alt (λ (a b_2 c) (/.p16 (real->posit16 1.0) (*.p16 (/.p16 a (-.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) (*.p16 b_2 b_2))) (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2))))> #<alt (λ (a b_2 c) (/.p16 (-.p16 (*.p16 (sqrt.p16 (/.p16 (-.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 c a) (*.p16 c a))) (+.p16 (*.p16 b_2 b_2) (*.p16 c a)))) (sqrt.p16 (/.p16 (-.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 c a) (*.p16 c a))) (+.p16 (*.p16 b_2 b_2) (*.p16 c a))))) (*.p16 b_2 b_2)) (*.p16 a (+.p16 (sqrt.p16 (/.p16 (-.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 c a) (*.p16 c a))) (+.p16 (*.p16 b_2 b_2) (*.p16 c a)))) b_2))))>)
110.476 * * * * [regimes]: Trying to branch on a from (#<alt (λ (a b_2 c) (/.p16 (-.p16 (sqrt.p16 (/.p16 (-.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 c a) (*.p16 c a))) (+.p16 (*.p16 b_2 b_2) (*.p16 c a)))) b_2) a))> #<alt (λ (a b_2 c) (/.p16 (-.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) (*.p16 b_2 b_2)) (*.p16 a (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2))))> #<alt (λ (a b_2 c) (/.p16 (real->posit16 1.0) (/.p16 a (/.p16 (-.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) (*.p16 b_2 b_2)) (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)))))> #<alt (λ (a b_2 c) (/.p16 (real->posit16 1.0) (/.p16 a (-.p16 (sqrt.p16 (/.p16 (-.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 c a) (*.p16 c a))) (+.p16 (*.p16 b_2 b_2) (*.p16 c a)))) b_2))))> #<alt (λ (a b_2 c) (/.p16 (-.p16 (*.p16 (sqrt.p16 (quire16->posit16 (quire16-mul-sub (posit16->quire16 (*.p16 b_2 b_2)) c a))) (sqrt.p16 (quire16->posit16 (quire16-mul-sub (posit16->quire16 (*.p16 b_2 b_2)) c a)))) (*.p16 b_2 b_2)) (*.p16 a (+.p16 (sqrt.p16 (quire16->posit16 (quire16-mul-sub (posit16->quire16 (*.p16 b_2 b_2)) c a))) b_2))))> #<alt (λ (a b_2 c) (/.p16 (-.p16 (sqrt.p16 (quire16->posit16 (quire16-mul-sub (posit16->quire16 (*.p16 b_2 b_2)) c a))) b_2) a))> #<alt (λ (a b_2 c) (/.p16 (real->posit16 1.0) (/.p16 a (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2))))> #<alt (λ (a b_2 c) (/.p16 (-.p16 (sqrt.p16 (/.p16 (-.p16 (*.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2))) (*.p16 (*.p16 (*.p16 c a) (*.p16 c a)) (*.p16 (*.p16 c a) (*.p16 c a)))) (*.p16 (+.p16 (*.p16 b_2 b_2) (*.p16 c a)) (+.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 c a) (*.p16 c a)))))) b_2) a))> #<alt (λ (a b_2 c) (/.p16 (real->posit16 1.0) (*.p16 (/.p16 a (-.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) (*.p16 b_2 b_2))) (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2))))> #<alt (λ (a b_2 c) (/.p16 (-.p16 (*.p16 (sqrt.p16 (/.p16 (-.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 c a) (*.p16 c a))) (+.p16 (*.p16 b_2 b_2) (*.p16 c a)))) (sqrt.p16 (/.p16 (-.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 c a) (*.p16 c a))) (+.p16 (*.p16 b_2 b_2) (*.p16 c a))))) (*.p16 b_2 b_2)) (*.p16 a (+.p16 (sqrt.p16 (/.p16 (-.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 c a) (*.p16 c a))) (+.p16 (*.p16 b_2 b_2) (*.p16 c a)))) b_2))))>)
110.709 * * * [regime]: Found split indices: #<option (#s(si 5 256))>
110.710 * [simplify]: Simplifying:
  (/.p16 (-.p16 (sqrt.p16 (quire16->posit16 (quire16-mul-sub (posit16->quire16 (*.p16 b_2 b_2)) c a))) b_2) a)
110.710 * * [simplify]: iteration 1: (10 enodes)
110.710 * * [simplify]: Extracting #0: cost 1 inf + 0
110.710 * * [simplify]: Extracting #1: cost 3 inf + 0
110.710 * * [simplify]: Extracting #2: cost 4 inf + 1
110.710 * * [simplify]: Extracting #3: cost 4 inf + 2
110.710 * * [simplify]: Extracting #4: cost 5 inf + 2
110.711 * * [simplify]: Extracting #5: cost 7 inf + 2
110.711 * * [simplify]: Extracting #6: cost 7 inf + 3
110.711 * * [simplify]: Extracting #7: cost 0 inf + 2980
110.711 * [simplify]: Simplified to:
  (/.p16 (-.p16 (sqrt.p16 (quire16->posit16 (quire16-mul-sub (posit16->quire16 (*.p16 b_2 b_2)) c a))) b_2) a)
110.711 * * * * [points]: Sampling 8000 additional inputs, on iter 0 have 0 / 8000
110.755 * * * * [points]: Computing exacts on every 500 of 8000 points to ramp up precision
110.756 * * * * [points]: Setting MPFR precision to 64
110.757 * * * * [points]: Setting MPFR precision to 320
110.758 * * * * [points]: Computing exacts on every 250 of 8000 points to ramp up precision
110.760 * * * * [points]: Setting MPFR precision to 64
110.762 * * * * [points]: Setting MPFR precision to 320
110.765 * * * * [points]: Computing exacts on every 125 of 8000 points to ramp up precision
110.767 * * * * [points]: Setting MPFR precision to 64
110.775 * * * * [points]: Setting MPFR precision to 320
110.798 * * * * [points]: Computing exacts on every 62 of 8000 points to ramp up precision
110.800 * * * * [points]: Setting MPFR precision to 64
110.814 * * * * [points]: Setting MPFR precision to 320
110.829 * * * * [points]: Computing exacts on every 31 of 8000 points to ramp up precision
110.831 * * * * [points]: Setting MPFR precision to 64
110.857 * * * * [points]: Setting MPFR precision to 320
110.883 * * * * [points]: Computing exacts on every 15 of 8000 points to ramp up precision
110.885 * * * * [points]: Setting MPFR precision to 64
110.934 * * * * [points]: Setting MPFR precision to 320
110.985 * * * * [points]: Computing exacts on every 7 of 8000 points to ramp up precision
110.986 * * * * [points]: Setting MPFR precision to 64
111.104 * * * * [points]: Setting MPFR precision to 320
111.247 * * * * [points]: Computing exacts on every 3 of 8000 points to ramp up precision
111.250 * * * * [points]: Setting MPFR precision to 64
111.540 * * * * [points]: Setting MPFR precision to 320
111.854 * * * * [points]: Computing exacts for 8000 points
111.856 * * * * [points]: Setting MPFR precision to 64
113.324 * * * * [points]: Setting MPFR precision to 320
114.356 * * * * [points]: Filtering points with unrepresentable outputs
114.434 * * * * [points]: Sampled 8000 points with exact outputs
118.488 * [regime-testing]: Baseline error score: 1.626049718193084
118.490 * [regime-testing]: Oracle error score: 1.2273782012599264
118.496 * [regime-testing]: End program error score: 1.626049718193084