110.925 * [progress]: [Phase 1 of 3] Setting up.
0.002 * * * [progress]: [1/2] Preparing points
0.002 * * * * [points]: Sampling 256 additional inputs, on iter 0 have 0 / 256
0.002 * * * * [points]: Computing exacts on every 16 of 256 points to ramp up precision
0.004 * * * * [points]: Setting MPFR precision to 64
0.005 * * * * [points]: Setting MPFR precision to 320
0.006 * * * * [points]: Computing exacts on every 8 of 256 points to ramp up precision
0.008 * * * * [points]: Setting MPFR precision to 64
0.010 * * * * [points]: Setting MPFR precision to 320
0.012 * * * * [points]: Computing exacts on every 4 of 256 points to ramp up precision
0.013 * * * * [points]: Setting MPFR precision to 64
0.016 * * * * [points]: Setting MPFR precision to 320
0.020 * * * * [points]: Computing exacts on every 2 of 256 points to ramp up precision
0.021 * * * * [points]: Setting MPFR precision to 64
0.027 * * * * [points]: Setting MPFR precision to 320
0.032 * * * * [points]: Computing exacts for 256 points
0.034 * * * * [points]: Setting MPFR precision to 64
0.062 * * * * [points]: Setting MPFR precision to 320
0.079 * * * * [points]: Filtering points with unrepresentable outputs
0.080 * * * * [points]: Sampled 256 points with exact outputs
0.080 * * * [progress]: [2/2] Setting up program.
0.085 * [progress]: [Phase 2 of 3] Improving.
0.086 * * * * [progress]: [ 1 / 1 ] simplifiying candidate #<alt (λ (x.re x.im) (-.p16 (*.p16 (-.p16 (*.p16 x.re x.re) (*.p16 x.im x.im)) x.re) (*.p16 (+.p16 (*.p16 x.re x.im) (*.p16 x.im x.re)) x.im)))>
0.086 * [simplify]: Simplifying:
  (-.p16 (*.p16 (-.p16 (*.p16 x.re x.re) (*.p16 x.im x.im)) x.re) (*.p16 (+.p16 (*.p16 x.re x.im) (*.p16 x.im x.re)) x.im))
0.086 * * [simplify]: iteration 1: (11 enodes)
0.088 * * [simplify]: iteration 2: (21 enodes)
0.092 * * [simplify]: iteration 3: (51 enodes)
0.102 * * [simplify]: iteration 4: (106 enodes)
0.127 * * [simplify]: iteration 5: (223 enodes)
0.231 * * [simplify]: iteration 6: (622 enodes)
0.494 * * [simplify]: iteration 7: (1485 enodes)
3.264 * * [simplify]: Extracting #0: cost 1 inf + 0
3.265 * * [simplify]: Extracting #1: cost 169 inf + 0
3.268 * * [simplify]: Extracting #2: cost 423 inf + 1
3.273 * * [simplify]: Extracting #3: cost 418 inf + 47997
3.298 * * [simplify]: Extracting #4: cost 181 inf + 300968
3.348 * * [simplify]: Extracting #5: cost 6 inf + 541596
3.422 * * [simplify]: Extracting #6: cost 0 inf + 546728
3.493 * * [simplify]: Extracting #7: cost 0 inf + 546408
3.565 * [simplify]: Simplified to:
  (*.p16 x.re (-.p16 (*.p16 x.re x.re) (+.p16 (+.p16 (*.p16 x.im x.im) (*.p16 x.im x.im)) (*.p16 x.im x.im))))
3.583 * * [progress]: iteration 1 / 4
3.583 * * * [progress]: picking best candidate
3.599 * * * * [pick]: Picked  #<alt (λ (x.re x.im) (-.p16 (*.p16 (-.p16 (*.p16 x.re x.re) (*.p16 x.im x.im)) x.re) (*.p16 (+.p16 (*.p16 x.re x.im) (*.p16 x.im x.re)) x.im)))>
3.599 * * * [progress]: localizing error
3.826 * * * [progress]: generating rewritten candidates
3.826 * * * * [progress]: [ 1 / 4 ] rewriting at (2 1 1)
3.830 * * * * [progress]: [ 2 / 4 ] rewriting at (2)
3.833 * * * * [progress]: [ 3 / 4 ] rewriting at (2 1)
3.837 * * * * [progress]: [ 4 / 4 ] rewriting at (2 2 1)
3.843 * * * [progress]: generating series expansions
3.843 * * * * [progress]: [ 1 / 4 ] generating series at (2 1 1)
3.843 * * * * [progress]: [ 2 / 4 ] generating series at (2)
3.843 * * * * [progress]: [ 3 / 4 ] generating series at (2 1)
3.843 * * * * [progress]: [ 4 / 4 ] generating series at (2 2 1)
3.843 * * * [progress]: simplifying candidates
3.843 * * * * [progress]: [ 1 / 73 ] simplifiying candidate #<alt (λ (x.re x.im) (-.p16 (*.p16 (*.p16 (+.p16 x.re x.im) (-.p16 x.re x.im)) x.re) (*.p16 (+.p16 (*.p16 x.re x.im) (*.p16 x.im x.re)) x.im)))>
3.843 * * * * [progress]: [ 2 / 73 ] simplifiying candidate #<alt (λ (x.re x.im) (-.p16 (*.p16 (-.p16 (-.p16 (*.p16 x.re x.re) (real->posit16 0.0)) (*.p16 x.im x.im)) x.re) (*.p16 (+.p16 (*.p16 x.re x.im) (*.p16 x.im x.re)) x.im)))>
3.843 * * * * [progress]: [ 3 / 73 ] simplifiying candidate #<alt (λ (x.re x.im) (-.p16 (*.p16 (-.p16 (-.p16 (*.p16 x.re x.re) (*.p16 x.im x.im)) (real->posit16 0.0)) x.re) (*.p16 (+.p16 (*.p16 x.re x.im) (*.p16 x.im x.re)) x.im)))>
3.843 * * * * [progress]: [ 4 / 73 ] simplifiying candidate #<alt (λ (x.re x.im) (-.p16 (*.p16 (+.p16 (real->posit16 0.0) (-.p16 (*.p16 x.re x.re) (*.p16 x.im x.im))) x.re) (*.p16 (+.p16 (*.p16 x.re x.im) (*.p16 x.im x.re)) x.im)))>
3.843 * * * * [progress]: [ 5 / 73 ] simplifiying candidate #<alt (λ (x.re x.im) (-.p16 (*.p16 (+.p16 (*.p16 x.re x.re) (-.p16 (real->posit16 0.0) (*.p16 x.im x.im))) x.re) (*.p16 (+.p16 (*.p16 x.re x.im) (*.p16 x.im x.re)) x.im)))>
3.843 * * * * [progress]: [ 6 / 73 ] simplifiying candidate #<alt (λ (x.re x.im) (-.p16 (*.p16 (-.p16 (*.p16 x.re x.re) (+.p16 (real->posit16 0.0) (*.p16 x.im x.im))) x.re) (*.p16 (+.p16 (*.p16 x.re x.im) (*.p16 x.im x.re)) x.im)))>
3.843 * * * * [progress]: [ 7 / 73 ] simplifiying candidate #<alt (λ (x.re x.im) (-.p16 (*.p16 (+.p16 (-.p16 (*.p16 x.re x.re) (*.p16 x.im x.im)) (real->posit16 0.0)) x.re) (*.p16 (+.p16 (*.p16 x.re x.im) (*.p16 x.im x.re)) x.im)))>
3.843 * * * * [progress]: [ 8 / 73 ] simplifiying candidate #<alt (λ (x.re x.im) (-.p16 (*.p16 (+.p16 (*.p16 x.re x.re) (neg.p16 (*.p16 x.im x.im))) x.re) (*.p16 (+.p16 (*.p16 x.re x.im) (*.p16 x.im x.re)) x.im)))>
3.843 * * * * [progress]: [ 9 / 73 ] simplifiying candidate #<alt (λ (x.re x.im) (-.p16 (*.p16 (/.p16 (-.p16 (*.p16 (*.p16 x.re x.re) (*.p16 x.re x.re)) (*.p16 (*.p16 x.im x.im) (*.p16 x.im x.im))) (+.p16 (*.p16 x.re x.re) (*.p16 x.im x.im))) x.re) (*.p16 (+.p16 (*.p16 x.re x.im) (*.p16 x.im x.re)) x.im)))>
3.843 * * * * [progress]: [ 10 / 73 ] simplifiying candidate #<alt (λ (x.re x.im) (-.p16 (*.p16 (*.p16 (real->posit16 1.0) (-.p16 (*.p16 x.re x.re) (*.p16 x.im x.im))) x.re) (*.p16 (+.p16 (*.p16 x.re x.im) (*.p16 x.im x.re)) x.im)))>
3.843 * * * * [progress]: [ 11 / 73 ] simplifiying candidate #<alt (λ (x.re x.im) (-.p16 (*.p16 (quire16->posit16 (posit16->quire16 (-.p16 (*.p16 x.re x.re) (*.p16 x.im x.im)))) x.re) (*.p16 (+.p16 (*.p16 x.re x.im) (*.p16 x.im x.re)) x.im)))>
3.843 * * * * [progress]: [ 12 / 73 ] simplifiying candidate #<alt (λ (x.re x.im) (-.p16 (*.p16 (quire16->posit16 (quire16-mul-sub (posit16->quire16 (*.p16 x.re x.re)) (*.p16 x.im x.im) (real->posit16 1.0))) x.re) (*.p16 (+.p16 (*.p16 x.re x.im) (*.p16 x.im x.re)) x.im)))>
3.843 * * * * [progress]: [ 13 / 73 ] simplifiying candidate #<alt (λ (x.re x.im) (-.p16 (*.p16 (quire16->posit16 (quire16-mul-sub (posit16->quire16 (*.p16 x.re x.re)) x.im x.im)) x.re) (*.p16 (+.p16 (*.p16 x.re x.im) (*.p16 x.im x.re)) x.im)))>
3.843 * * * * [progress]: [ 14 / 73 ] simplifiying candidate #<alt (λ (x.re x.im) (-.p16 (*.p16 (+.p16 (real->posit16 0.0) (-.p16 (*.p16 x.re x.re) (*.p16 x.im x.im))) x.re) (*.p16 (+.p16 (*.p16 x.re x.im) (*.p16 x.im x.re)) x.im)))>
3.843 * * * * [progress]: [ 15 / 73 ] simplifiying candidate #<alt (λ (x.re x.im) (-.p16 (*.p16 (+.p16 (-.p16 (*.p16 x.re x.re) (*.p16 x.im x.im)) (real->posit16 0.0)) x.re) (*.p16 (+.p16 (*.p16 x.re x.im) (*.p16 x.im x.re)) x.im)))>
3.843 * * * * [progress]: [ 16 / 73 ] simplifiying candidate #<alt (λ (x.re x.im) (-.p16 (*.p16 (-.p16 (-.p16 (*.p16 x.re x.re) (*.p16 x.im x.im)) (real->posit16 0.0)) x.re) (*.p16 (+.p16 (*.p16 x.re x.im) (*.p16 x.im x.re)) x.im)))>
3.843 * * * * [progress]: [ 17 / 73 ] simplifiying candidate #<alt (λ (x.re x.im) (-.p16 (*.p16 (*.p16 (real->posit16 1.0) (-.p16 (*.p16 x.re x.re) (*.p16 x.im x.im))) x.re) (*.p16 (+.p16 (*.p16 x.re x.im) (*.p16 x.im x.re)) x.im)))>
3.843 * * * * [progress]: [ 18 / 73 ] simplifiying candidate #<alt (λ (x.re x.im) (-.p16 (*.p16 (*.p16 (-.p16 (*.p16 x.re x.re) (*.p16 x.im x.im)) (real->posit16 1.0)) x.re) (*.p16 (+.p16 (*.p16 x.re x.im) (*.p16 x.im x.re)) x.im)))>
3.843 * * * * [progress]: [ 19 / 73 ] simplifiying candidate #<alt (λ (x.re x.im) (-.p16 (*.p16 (/.p16 (-.p16 (*.p16 x.re x.re) (*.p16 x.im x.im)) (real->posit16 1.0)) x.re) (*.p16 (+.p16 (*.p16 x.re x.im) (*.p16 x.im x.re)) x.im)))>
3.844 * * * * [progress]: [ 20 / 73 ] simplifiying candidate #<alt (λ (x.re x.im) (-.p16 (-.p16 (*.p16 (-.p16 (*.p16 x.re x.re) (*.p16 x.im x.im)) x.re) (real->posit16 0.0)) (*.p16 (+.p16 (*.p16 x.re x.im) (*.p16 x.im x.re)) x.im)))>
3.844 * * * * [progress]: [ 21 / 73 ] simplifiying candidate #<alt (λ (x.re x.im) (-.p16 (-.p16 (*.p16 (-.p16 (*.p16 x.re x.re) (*.p16 x.im x.im)) x.re) (*.p16 (+.p16 (*.p16 x.re x.im) (*.p16 x.im x.re)) x.im)) (real->posit16 0.0)))>
3.844 * * * * [progress]: [ 22 / 73 ] simplifiying candidate #<alt (λ (x.re x.im) (+.p16 (real->posit16 0.0) (-.p16 (*.p16 (-.p16 (*.p16 x.re x.re) (*.p16 x.im x.im)) x.re) (*.p16 (+.p16 (*.p16 x.re x.im) (*.p16 x.im x.re)) x.im))))>
3.844 * * * * [progress]: [ 23 / 73 ] simplifiying candidate #<alt (λ (x.re x.im) (+.p16 (*.p16 (-.p16 (*.p16 x.re x.re) (*.p16 x.im x.im)) x.re) (-.p16 (real->posit16 0.0) (*.p16 (+.p16 (*.p16 x.re x.im) (*.p16 x.im x.re)) x.im))))>
3.844 * * * * [progress]: [ 24 / 73 ] simplifiying candidate #<alt (λ (x.re x.im) (-.p16 (*.p16 (-.p16 (*.p16 x.re x.re) (*.p16 x.im x.im)) x.re) (+.p16 (real->posit16 0.0) (*.p16 (+.p16 (*.p16 x.re x.im) (*.p16 x.im x.re)) x.im))))>
3.844 * * * * [progress]: [ 25 / 73 ] simplifiying candidate #<alt (λ (x.re x.im) (+.p16 (-.p16 (*.p16 (-.p16 (*.p16 x.re x.re) (*.p16 x.im x.im)) x.re) (*.p16 (+.p16 (*.p16 x.re x.im) (*.p16 x.im x.re)) x.im)) (real->posit16 0.0)))>
3.844 * * * * [progress]: [ 26 / 73 ] simplifiying candidate #<alt (λ (x.re x.im) (+.p16 (*.p16 (-.p16 (*.p16 x.re x.re) (*.p16 x.im x.im)) x.re) (neg.p16 (*.p16 (+.p16 (*.p16 x.re x.im) (*.p16 x.im x.re)) x.im))))>
3.844 * * * * [progress]: [ 27 / 73 ] simplifiying candidate #<alt (λ (x.re x.im) (/.p16 (-.p16 (*.p16 (*.p16 (-.p16 (*.p16 x.re x.re) (*.p16 x.im x.im)) x.re) (*.p16 (-.p16 (*.p16 x.re x.re) (*.p16 x.im x.im)) x.re)) (*.p16 (*.p16 (+.p16 (*.p16 x.re x.im) (*.p16 x.im x.re)) x.im) (*.p16 (+.p16 (*.p16 x.re x.im) (*.p16 x.im x.re)) x.im))) (+.p16 (*.p16 (-.p16 (*.p16 x.re x.re) (*.p16 x.im x.im)) x.re) (*.p16 (+.p16 (*.p16 x.re x.im) (*.p16 x.im x.re)) x.im))))>
3.844 * * * * [progress]: [ 28 / 73 ] simplifiying candidate #<alt (λ (x.re x.im) (*.p16 (real->posit16 1.0) (-.p16 (*.p16 (-.p16 (*.p16 x.re x.re) (*.p16 x.im x.im)) x.re) (*.p16 (+.p16 (*.p16 x.re x.im) (*.p16 x.im x.re)) x.im))))>
3.844 * * * * [progress]: [ 29 / 73 ] simplifiying candidate #<alt (λ (x.re x.im) (quire16->posit16 (posit16->quire16 (-.p16 (*.p16 (-.p16 (*.p16 x.re x.re) (*.p16 x.im x.im)) x.re) (*.p16 (+.p16 (*.p16 x.re x.im) (*.p16 x.im x.re)) x.im)))))>
3.844 * * * * [progress]: [ 30 / 73 ] simplifiying candidate #<alt (λ (x.re x.im) (quire16->posit16 (quire16-mul-sub (posit16->quire16 (*.p16 (-.p16 (*.p16 x.re x.re) (*.p16 x.im x.im)) x.re)) (*.p16 (+.p16 (*.p16 x.re x.im) (*.p16 x.im x.re)) x.im) (real->posit16 1.0))))>
3.844 * * * * [progress]: [ 31 / 73 ] simplifiying candidate #<alt (λ (x.re x.im) (quire16->posit16 (quire16-mul-sub (posit16->quire16 (*.p16 (-.p16 (*.p16 x.re x.re) (*.p16 x.im x.im)) x.re)) (+.p16 (*.p16 x.re x.im) (*.p16 x.im x.re)) x.im)))>
3.844 * * * * [progress]: [ 32 / 73 ] simplifiying candidate #<alt (λ (x.re x.im) (+.p16 (real->posit16 0.0) (-.p16 (*.p16 (-.p16 (*.p16 x.re x.re) (*.p16 x.im x.im)) x.re) (*.p16 (+.p16 (*.p16 x.re x.im) (*.p16 x.im x.re)) x.im))))>
3.844 * * * * [progress]: [ 33 / 73 ] simplifiying candidate #<alt (λ (x.re x.im) (+.p16 (-.p16 (*.p16 (-.p16 (*.p16 x.re x.re) (*.p16 x.im x.im)) x.re) (*.p16 (+.p16 (*.p16 x.re x.im) (*.p16 x.im x.re)) x.im)) (real->posit16 0.0)))>
3.844 * * * * [progress]: [ 34 / 73 ] simplifiying candidate #<alt (λ (x.re x.im) (-.p16 (-.p16 (*.p16 (-.p16 (*.p16 x.re x.re) (*.p16 x.im x.im)) x.re) (*.p16 (+.p16 (*.p16 x.re x.im) (*.p16 x.im x.re)) x.im)) (real->posit16 0.0)))>
3.844 * * * * [progress]: [ 35 / 73 ] simplifiying candidate #<alt (λ (x.re x.im) (*.p16 (real->posit16 1.0) (-.p16 (*.p16 (-.p16 (*.p16 x.re x.re) (*.p16 x.im x.im)) x.re) (*.p16 (+.p16 (*.p16 x.re x.im) (*.p16 x.im x.re)) x.im))))>
3.844 * * * * [progress]: [ 36 / 73 ] simplifiying candidate #<alt (λ (x.re x.im) (*.p16 (-.p16 (*.p16 (-.p16 (*.p16 x.re x.re) (*.p16 x.im x.im)) x.re) (*.p16 (+.p16 (*.p16 x.re x.im) (*.p16 x.im x.re)) x.im)) (real->posit16 1.0)))>
3.844 * * * * [progress]: [ 37 / 73 ] simplifiying candidate #<alt (λ (x.re x.im) (/.p16 (-.p16 (*.p16 (-.p16 (*.p16 x.re x.re) (*.p16 x.im x.im)) x.re) (*.p16 (+.p16 (*.p16 x.re x.im) (*.p16 x.im x.re)) x.im)) (real->posit16 1.0)))>
3.844 * * * * [progress]: [ 38 / 73 ] simplifiying candidate #<alt (λ (x.re x.im) (-.p16 (*.p16 (+.p16 x.re x.im) (*.p16 (-.p16 x.re x.im) x.re)) (*.p16 (+.p16 (*.p16 x.re x.im) (*.p16 x.im x.re)) x.im)))>
3.844 * * * * [progress]: [ 39 / 73 ] simplifiying candidate #<alt (λ (x.re x.im) (-.p16 (*.p16 (real->posit16 1.0) (*.p16 (-.p16 (*.p16 x.re x.re) (*.p16 x.im x.im)) x.re)) (*.p16 (+.p16 (*.p16 x.re x.im) (*.p16 x.im x.re)) x.im)))>
3.844 * * * * [progress]: [ 40 / 73 ] simplifiying candidate #<alt (λ (x.re x.im) (-.p16 (*.p16 (real->posit16 1.0) (*.p16 (-.p16 (*.p16 x.re x.re) (*.p16 x.im x.im)) x.re)) (*.p16 (+.p16 (*.p16 x.re x.im) (*.p16 x.im x.re)) x.im)))>
3.844 * * * * [progress]: [ 41 / 73 ] simplifiying candidate #<alt (λ (x.re x.im) (-.p16 (*.p16 (-.p16 (*.p16 x.re x.re) (*.p16 x.im x.im)) (*.p16 (real->posit16 1.0) x.re)) (*.p16 (+.p16 (*.p16 x.re x.im) (*.p16 x.im x.re)) x.im)))>
3.844 * * * * [progress]: [ 42 / 73 ] simplifiying candidate #<alt (λ (x.re x.im) (-.p16 (/.p16 (*.p16 (-.p16 (*.p16 (*.p16 x.re x.re) (*.p16 x.re x.re)) (*.p16 (*.p16 x.im x.im) (*.p16 x.im x.im))) x.re) (+.p16 (*.p16 x.re x.re) (*.p16 x.im x.im))) (*.p16 (+.p16 (*.p16 x.re x.im) (*.p16 x.im x.re)) x.im)))>
3.844 * * * * [progress]: [ 43 / 73 ] simplifiying candidate #<alt (λ (x.re x.im) (-.p16 (/.p16 (*.p16 (-.p16 (*.p16 x.re x.re) (*.p16 x.im x.im)) x.re) (real->posit16 1.0)) (*.p16 (+.p16 (*.p16 x.re x.im) (*.p16 x.im x.re)) x.im)))>
3.844 * * * * [progress]: [ 44 / 73 ] simplifiying candidate #<alt (λ (x.re x.im) (-.p16 (*.p16 (real->posit16 1.0) (*.p16 (-.p16 (*.p16 x.re x.re) (*.p16 x.im x.im)) x.re)) (*.p16 (+.p16 (*.p16 x.re x.im) (*.p16 x.im x.re)) x.im)))>
3.844 * * * * [progress]: [ 45 / 73 ] simplifiying candidate #<alt (λ (x.re x.im) (-.p16 (quire16->posit16 (posit16->quire16 (*.p16 (-.p16 (*.p16 x.re x.re) (*.p16 x.im x.im)) x.re))) (*.p16 (+.p16 (*.p16 x.re x.im) (*.p16 x.im x.re)) x.im)))>
3.845 * * * * [progress]: [ 46 / 73 ] simplifiying candidate #<alt (λ (x.re x.im) (-.p16 (+.p16 (real->posit16 0.0) (*.p16 (-.p16 (*.p16 x.re x.re) (*.p16 x.im x.im)) x.re)) (*.p16 (+.p16 (*.p16 x.re x.im) (*.p16 x.im x.re)) x.im)))>
3.845 * * * * [progress]: [ 47 / 73 ] simplifiying candidate #<alt (λ (x.re x.im) (-.p16 (+.p16 (*.p16 (-.p16 (*.p16 x.re x.re) (*.p16 x.im x.im)) x.re) (real->posit16 0.0)) (*.p16 (+.p16 (*.p16 x.re x.im) (*.p16 x.im x.re)) x.im)))>
3.845 * * * * [progress]: [ 48 / 73 ] simplifiying candidate #<alt (λ (x.re x.im) (-.p16 (-.p16 (*.p16 (-.p16 (*.p16 x.re x.re) (*.p16 x.im x.im)) x.re) (real->posit16 0.0)) (*.p16 (+.p16 (*.p16 x.re x.im) (*.p16 x.im x.re)) x.im)))>
3.845 * * * * [progress]: [ 49 / 73 ] simplifiying candidate #<alt (λ (x.re x.im) (-.p16 (*.p16 (real->posit16 1.0) (*.p16 (-.p16 (*.p16 x.re x.re) (*.p16 x.im x.im)) x.re)) (*.p16 (+.p16 (*.p16 x.re x.im) (*.p16 x.im x.re)) x.im)))>
3.845 * * * * [progress]: [ 50 / 73 ] simplifiying candidate #<alt (λ (x.re x.im) (-.p16 (*.p16 (*.p16 (-.p16 (*.p16 x.re x.re) (*.p16 x.im x.im)) x.re) (real->posit16 1.0)) (*.p16 (+.p16 (*.p16 x.re x.im) (*.p16 x.im x.re)) x.im)))>
3.845 * * * * [progress]: [ 51 / 73 ] simplifiying candidate #<alt (λ (x.re x.im) (-.p16 (/.p16 (*.p16 (-.p16 (*.p16 x.re x.re) (*.p16 x.im x.im)) x.re) (real->posit16 1.0)) (*.p16 (+.p16 (*.p16 x.re x.im) (*.p16 x.im x.re)) x.im)))>
3.845 * * * * [progress]: [ 52 / 73 ] simplifiying candidate #<alt (λ (x.re x.im) (-.p16 (*.p16 x.re (-.p16 (*.p16 x.re x.re) (*.p16 x.im x.im))) (*.p16 (+.p16 (*.p16 x.re x.im) (*.p16 x.im x.re)) x.im)))>
3.845 * * * * [progress]: [ 53 / 73 ] simplifiying candidate #<alt (λ (x.re x.im) (-.p16 (*.p16 (-.p16 (*.p16 x.re x.re) (*.p16 x.im x.im)) x.re) (*.p16 (+.p16 (+.p16 (*.p16 x.re x.im) (real->posit16 0.0)) (*.p16 x.im x.re)) x.im)))>
3.845 * * * * [progress]: [ 54 / 73 ] simplifiying candidate #<alt (λ (x.re x.im) (-.p16 (*.p16 (-.p16 (*.p16 x.re x.re) (*.p16 x.im x.im)) x.re) (*.p16 (+.p16 (+.p16 (*.p16 x.re x.im) (*.p16 x.im x.re)) (real->posit16 0.0)) x.im)))>
3.845 * * * * [progress]: [ 55 / 73 ] simplifiying candidate #<alt (λ (x.re x.im) (-.p16 (*.p16 (-.p16 (*.p16 x.re x.re) (*.p16 x.im x.im)) x.re) (*.p16 (+.p16 (real->posit16 0.0) (+.p16 (*.p16 x.re x.im) (*.p16 x.im x.re))) x.im)))>
3.845 * * * * [progress]: [ 56 / 73 ] simplifiying candidate #<alt (λ (x.re x.im) (-.p16 (*.p16 (-.p16 (*.p16 x.re x.re) (*.p16 x.im x.im)) x.re) (*.p16 (+.p16 (*.p16 x.re x.im) (+.p16 (real->posit16 0.0) (*.p16 x.im x.re))) x.im)))>
3.845 * * * * [progress]: [ 57 / 73 ] simplifiying candidate #<alt (λ (x.re x.im) (-.p16 (*.p16 (-.p16 (*.p16 x.re x.re) (*.p16 x.im x.im)) x.re) (*.p16 (-.p16 (+.p16 (*.p16 x.re x.im) (*.p16 x.im x.re)) (real->posit16 0.0)) x.im)))>
3.845 * * * * [progress]: [ 58 / 73 ] simplifiying candidate #<alt (λ (x.re x.im) (-.p16 (*.p16 (-.p16 (*.p16 x.re x.re) (*.p16 x.im x.im)) x.re) (*.p16 (-.p16 (*.p16 x.re x.im) (-.p16 (real->posit16 0.0) (*.p16 x.im x.re))) x.im)))>
3.845 * * * * [progress]: [ 59 / 73 ] simplifiying candidate #<alt (λ (x.re x.im) (-.p16 (*.p16 (-.p16 (*.p16 x.re x.re) (*.p16 x.im x.im)) x.re) (*.p16 (*.p16 (real->posit16 1.0) (+.p16 (*.p16 x.re x.im) (*.p16 x.im x.re))) x.im)))>
3.845 * * * * [progress]: [ 60 / 73 ] simplifiying candidate #<alt (λ (x.re x.im) (-.p16 (*.p16 (-.p16 (*.p16 x.re x.re) (*.p16 x.im x.im)) x.re) (*.p16 (quire16->posit16 (posit16->quire16 (+.p16 (*.p16 x.re x.im) (*.p16 x.im x.re)))) x.im)))>
3.845 * * * * [progress]: [ 61 / 73 ] simplifiying candidate #<alt (λ (x.re x.im) (-.p16 (*.p16 (-.p16 (*.p16 x.re x.re) (*.p16 x.im x.im)) x.re) (*.p16 (quire16->posit16 (quire16-mul-add (posit16->quire16 (*.p16 x.re x.im)) (*.p16 x.im x.re) (real->posit16 1.0))) x.im)))>
3.845 * * * * [progress]: [ 62 / 73 ] simplifiying candidate #<alt (λ (x.re x.im) (-.p16 (*.p16 (-.p16 (*.p16 x.re x.re) (*.p16 x.im x.im)) x.re) (*.p16 (quire16->posit16 (quire16-mul-add (posit16->quire16 (*.p16 x.re x.im)) x.im x.re)) x.im)))>
3.845 * * * * [progress]: [ 63 / 73 ] simplifiying candidate #<alt (λ (x.re x.im) (-.p16 (*.p16 (-.p16 (*.p16 x.re x.re) (*.p16 x.im x.im)) x.re) (*.p16 (+.p16 (real->posit16 0.0) (+.p16 (*.p16 x.re x.im) (*.p16 x.im x.re))) x.im)))>
3.845 * * * * [progress]: [ 64 / 73 ] simplifiying candidate #<alt (λ (x.re x.im) (-.p16 (*.p16 (-.p16 (*.p16 x.re x.re) (*.p16 x.im x.im)) x.re) (*.p16 (+.p16 (+.p16 (*.p16 x.re x.im) (*.p16 x.im x.re)) (real->posit16 0.0)) x.im)))>
3.845 * * * * [progress]: [ 65 / 73 ] simplifiying candidate #<alt (λ (x.re x.im) (-.p16 (*.p16 (-.p16 (*.p16 x.re x.re) (*.p16 x.im x.im)) x.re) (*.p16 (-.p16 (+.p16 (*.p16 x.re x.im) (*.p16 x.im x.re)) (real->posit16 0.0)) x.im)))>
3.845 * * * * [progress]: [ 66 / 73 ] simplifiying candidate #<alt (λ (x.re x.im) (-.p16 (*.p16 (-.p16 (*.p16 x.re x.re) (*.p16 x.im x.im)) x.re) (*.p16 (*.p16 (real->posit16 1.0) (+.p16 (*.p16 x.re x.im) (*.p16 x.im x.re))) x.im)))>
3.845 * * * * [progress]: [ 67 / 73 ] simplifiying candidate #<alt (λ (x.re x.im) (-.p16 (*.p16 (-.p16 (*.p16 x.re x.re) (*.p16 x.im x.im)) x.re) (*.p16 (*.p16 (+.p16 (*.p16 x.re x.im) (*.p16 x.im x.re)) (real->posit16 1.0)) x.im)))>
3.845 * * * * [progress]: [ 68 / 73 ] simplifiying candidate #<alt (λ (x.re x.im) (-.p16 (*.p16 (-.p16 (*.p16 x.re x.re) (*.p16 x.im x.im)) x.re) (*.p16 (/.p16 (+.p16 (*.p16 x.re x.im) (*.p16 x.im x.re)) (real->posit16 1.0)) x.im)))>
3.845 * * * * [progress]: [ 69 / 73 ] simplifiying candidate #<alt (λ (x.re x.im) (-.p16 (*.p16 (-.p16 (*.p16 x.re x.re) (*.p16 x.im x.im)) x.re) (*.p16 (+.p16 (*.p16 x.im x.re) (*.p16 x.re x.im)) x.im)))>
3.845 * * * * [progress]: [ 70 / 73 ] simplifiying candidate #<alt (λ (x.re x.im) (-.p16 (*.p16 (-.p16 (*.p16 x.re x.re) (*.p16 x.im x.im)) x.re) (*.p16 (+.p16 (*.p16 x.re x.im) (*.p16 x.im x.re)) x.im)))>
3.845 * * * * [progress]: [ 71 / 73 ] simplifiying candidate #<alt (λ (x.re x.im) (-.p16 (*.p16 (-.p16 (*.p16 x.re x.re) (*.p16 x.im x.im)) x.re) (*.p16 (+.p16 (*.p16 x.re x.im) (*.p16 x.im x.re)) x.im)))>
3.845 * * * * [progress]: [ 72 / 73 ] simplifiying candidate #<alt (λ (x.re x.im) (-.p16 (*.p16 (-.p16 (*.p16 x.re x.re) (*.p16 x.im x.im)) x.re) (*.p16 (+.p16 (*.p16 x.re x.im) (*.p16 x.im x.re)) x.im)))>
3.845 * * * * [progress]: [ 73 / 73 ] simplifiying candidate #<alt (λ (x.re x.im) (-.p16 (*.p16 (-.p16 (*.p16 x.re x.re) (*.p16 x.im x.im)) x.re) (*.p16 (+.p16 (*.p16 x.re x.im) (*.p16 x.im x.re)) x.im)))>
3.846 * [simplify]: Simplifying:
  (+.p16 x.re x.im)
  (-.p16 x.re x.im)
  (-.p16 (*.p16 x.re x.re) (real->posit16 0.0))
  (-.p16 (*.p16 x.re x.re) (*.p16 x.im x.im))
  (-.p16 (*.p16 x.re x.re) (*.p16 x.im x.im))
  (-.p16 (real->posit16 0.0) (*.p16 x.im x.im))
  (+.p16 (real->posit16 0.0) (*.p16 x.im x.im))
  (-.p16 (*.p16 x.re x.re) (*.p16 x.im x.im))
  (neg.p16 (*.p16 x.im x.im))
  (-.p16 (*.p16 (*.p16 x.re x.re) (*.p16 x.re x.re)) (*.p16 (*.p16 x.im x.im) (*.p16 x.im x.im)))
  (+.p16 (*.p16 x.re x.re) (*.p16 x.im x.im))
  (real->posit16 1.0)
  (posit16->quire16 (-.p16 (*.p16 x.re x.re) (*.p16 x.im x.im)))
  (quire16-mul-sub (posit16->quire16 (*.p16 x.re x.re)) (*.p16 x.im x.im) (real->posit16 1.0))
  (quire16-mul-sub (posit16->quire16 (*.p16 x.re x.re)) x.im x.im)
  (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 (*.p16 x.re x.re) (*.p16 x.im x.im)) x.re) (real->posit16 0.0))
  (-.p16 (*.p16 (-.p16 (*.p16 x.re x.re) (*.p16 x.im x.im)) x.re) (*.p16 (+.p16 (*.p16 x.re x.im) (*.p16 x.im x.re)) x.im))
  (-.p16 (*.p16 (-.p16 (*.p16 x.re x.re) (*.p16 x.im x.im)) x.re) (*.p16 (+.p16 (*.p16 x.re x.im) (*.p16 x.im x.re)) x.im))
  (-.p16 (real->posit16 0.0) (*.p16 (+.p16 (*.p16 x.re x.im) (*.p16 x.im x.re)) x.im))
  (+.p16 (real->posit16 0.0) (*.p16 (+.p16 (*.p16 x.re x.im) (*.p16 x.im x.re)) x.im))
  (-.p16 (*.p16 (-.p16 (*.p16 x.re x.re) (*.p16 x.im x.im)) x.re) (*.p16 (+.p16 (*.p16 x.re x.im) (*.p16 x.im x.re)) x.im))
  (neg.p16 (*.p16 (+.p16 (*.p16 x.re x.im) (*.p16 x.im x.re)) x.im))
  (-.p16 (*.p16 (*.p16 (-.p16 (*.p16 x.re x.re) (*.p16 x.im x.im)) x.re) (*.p16 (-.p16 (*.p16 x.re x.re) (*.p16 x.im x.im)) x.re)) (*.p16 (*.p16 (+.p16 (*.p16 x.re x.im) (*.p16 x.im x.re)) x.im) (*.p16 (+.p16 (*.p16 x.re x.im) (*.p16 x.im x.re)) x.im)))
  (+.p16 (*.p16 (-.p16 (*.p16 x.re x.re) (*.p16 x.im x.im)) x.re) (*.p16 (+.p16 (*.p16 x.re x.im) (*.p16 x.im x.re)) x.im))
  (real->posit16 1.0)
  (posit16->quire16 (-.p16 (*.p16 (-.p16 (*.p16 x.re x.re) (*.p16 x.im x.im)) x.re) (*.p16 (+.p16 (*.p16 x.re x.im) (*.p16 x.im x.re)) x.im)))
  (quire16-mul-sub (posit16->quire16 (*.p16 (-.p16 (*.p16 x.re x.re) (*.p16 x.im x.im)) x.re)) (*.p16 (+.p16 (*.p16 x.re x.im) (*.p16 x.im x.re)) x.im) (real->posit16 1.0))
  (quire16-mul-sub (posit16->quire16 (*.p16 (-.p16 (*.p16 x.re x.re) (*.p16 x.im x.im)) x.re)) (+.p16 (*.p16 x.re x.im) (*.p16 x.im x.re)) x.im)
  (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 x.re x.im) x.re)
  (*.p16 (-.p16 (*.p16 x.re x.re) (*.p16 x.im x.im)) x.re)
  (*.p16 (-.p16 (*.p16 x.re x.re) (*.p16 x.im x.im)) x.re)
  (*.p16 (real->posit16 1.0) x.re)
  (*.p16 (-.p16 (*.p16 (*.p16 x.re x.re) (*.p16 x.re x.re)) (*.p16 (*.p16 x.im x.im) (*.p16 x.im x.im))) x.re)
  (*.p16 (-.p16 (*.p16 x.re x.re) (*.p16 x.im x.im)) x.re)
  (real->posit16 1.0)
  (posit16->quire16 (*.p16 (-.p16 (*.p16 x.re x.re) (*.p16 x.im x.im)) x.re))
  (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 x.re x.im) (real->posit16 0.0))
  (+.p16 (*.p16 x.re x.im) (*.p16 x.im x.re))
  (+.p16 (*.p16 x.re x.im) (*.p16 x.im x.re))
  (+.p16 (real->posit16 0.0) (*.p16 x.im x.re))
  (+.p16 (*.p16 x.re x.im) (*.p16 x.im x.re))
  (-.p16 (real->posit16 0.0) (*.p16 x.im x.re))
  (real->posit16 1.0)
  (posit16->quire16 (+.p16 (*.p16 x.re x.im) (*.p16 x.im x.re)))
  (quire16-mul-add (posit16->quire16 (*.p16 x.re x.im)) (*.p16 x.im x.re) (real->posit16 1.0))
  (quire16-mul-add (posit16->quire16 (*.p16 x.re x.im)) x.im x.re)
  (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 (*.p16 x.re x.re) (*.p16 x.im x.im)) x.re) (*.p16 (+.p16 (*.p16 x.re x.im) (*.p16 x.im x.re)) x.im))
  (-.p16 (*.p16 (-.p16 (*.p16 x.re x.re) (*.p16 x.im x.im)) x.re) (*.p16 (+.p16 (*.p16 x.re x.im) (*.p16 x.im x.re)) x.im))
  (-.p16 (*.p16 (-.p16 (*.p16 x.re x.re) (*.p16 x.im x.im)) x.re) (*.p16 (+.p16 (*.p16 x.re x.im) (*.p16 x.im x.re)) x.im))
  (-.p16 (*.p16 (-.p16 (*.p16 x.re x.re) (*.p16 x.im x.im)) x.re) (*.p16 (+.p16 (*.p16 x.re x.im) (*.p16 x.im x.re)) x.im))
3.847 * * [simplify]: iteration 1: (51 enodes)
3.865 * * [simplify]: iteration 2: (101 enodes)
3.899 * * [simplify]: iteration 3: (356 enodes)
4.405 * * [simplify]: iteration 4: (1953 enodes)
39.517 * * [simplify]: Extracting #0: cost 32 inf + 0
39.525 * * [simplify]: Extracting #1: cost 2667 inf + 1
39.560 * * [simplify]: Extracting #2: cost 5231 inf + 52461
39.690 * * [simplify]: Extracting #3: cost 3500 inf + 1804195
40.694 * * [simplify]: Extracting #4: cost 735 inf + 4778347
41.207 * * [simplify]: Extracting #5: cost 36 inf + 5591798
41.699 * * [simplify]: Extracting #6: cost 0 inf + 5640335
42.208 * [simplify]: Simplified to:
  (+.p16 x.im x.re)
  (-.p16 x.re x.im)
  (*.p16 x.re x.re)
  (*.p16 (-.p16 x.re x.im) (+.p16 x.im x.re))
  (*.p16 (-.p16 x.re x.im) (+.p16 x.im x.re))
  (neg.p16 (*.p16 x.im x.im))
  (*.p16 x.im x.im)
  (*.p16 (-.p16 x.re x.im) (+.p16 x.im x.re))
  (neg.p16 (*.p16 x.im x.im))
  (*.p16 (+.p16 (*.p16 x.re x.re) (*.p16 x.im x.im)) (+.p16 (*.p16 x.re x.re) (neg.p16 (*.p16 x.im x.im))))
  (+.p16 (*.p16 x.re x.re) (*.p16 x.im x.im))
  (real->posit16 1.0)
  (posit16->quire16 (*.p16 (-.p16 x.re x.im) (+.p16 x.im x.re)))
  (quire16-mul-sub (posit16->quire16 (*.p16 x.re x.re)) (*.p16 x.im x.im) (real->posit16 1.0))
  (quire16-mul-sub (posit16->quire16 (*.p16 x.re x.re)) x.im x.im)
  (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 x.re (*.p16 (-.p16 x.re x.im) (+.p16 x.im x.re)))
  (*.p16 x.re (-.p16 (*.p16 (-.p16 x.re x.im) (+.p16 x.im x.re)) (*.p16 (+.p16 x.im x.im) x.im)))
  (*.p16 x.re (-.p16 (*.p16 (-.p16 x.re x.im) (+.p16 x.im x.re)) (*.p16 (+.p16 x.im x.im) x.im)))
  (neg.p16 (*.p16 x.re (*.p16 (+.p16 x.im x.im) x.im)))
  (*.p16 x.re (*.p16 (+.p16 x.im x.im) x.im))
  (*.p16 x.re (-.p16 (*.p16 (-.p16 x.re x.im) (+.p16 x.im x.re)) (*.p16 (+.p16 x.im x.im) x.im)))
  (neg.p16 (*.p16 x.re (*.p16 (+.p16 x.im x.im) x.im)))
  (*.p16 (*.p16 x.re (-.p16 (*.p16 (-.p16 x.re x.im) (+.p16 x.im x.re)) (*.p16 (+.p16 x.im x.im) x.im))) (*.p16 x.re (+.p16 (*.p16 (+.p16 x.im x.im) x.im) (*.p16 (-.p16 x.re x.im) (+.p16 x.im x.re)))))
  (*.p16 x.re (+.p16 (*.p16 (+.p16 x.im x.im) x.im) (*.p16 (-.p16 x.re x.im) (+.p16 x.im x.re))))
  (real->posit16 1.0)
  (posit16->quire16 (*.p16 x.re (-.p16 (*.p16 (-.p16 x.re x.im) (+.p16 x.im x.re)) (*.p16 (+.p16 x.im x.im) x.im))))
  (quire16-mul-sub (posit16->quire16 (*.p16 x.re (*.p16 (-.p16 x.re x.im) (+.p16 x.im x.re)))) (*.p16 x.re (*.p16 (+.p16 x.im x.im) x.im)) (real->posit16 1.0))
  (quire16-mul-sub (posit16->quire16 (*.p16 x.re (*.p16 (-.p16 x.re x.im) (+.p16 x.im x.re)))) (*.p16 (+.p16 x.im x.im) x.re) x.im)
  (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 x.re x.im) x.re)
  (*.p16 x.re (*.p16 (-.p16 x.re x.im) (+.p16 x.im x.re)))
  (*.p16 x.re (*.p16 (-.p16 x.re x.im) (+.p16 x.im x.re)))
  x.re
  (*.p16 x.re (*.p16 (+.p16 (*.p16 x.re x.re) (*.p16 x.im x.im)) (+.p16 (*.p16 x.re x.re) (neg.p16 (*.p16 x.im x.im)))))
  (*.p16 x.re (*.p16 (-.p16 x.re x.im) (+.p16 x.im x.re)))
  (real->posit16 1.0)
  (posit16->quire16 (*.p16 x.re (*.p16 (-.p16 x.re x.im) (+.p16 x.im x.re))))
  (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 x.im x.re)
  (*.p16 (+.p16 x.im x.im) x.re)
  (*.p16 (+.p16 x.im x.im) x.re)
  (*.p16 x.im x.re)
  (*.p16 (+.p16 x.im x.im) x.re)
  (neg.p16 (*.p16 x.im x.re))
  (real->posit16 1.0)
  (posit16->quire16 (*.p16 (+.p16 x.im x.im) x.re))
  (quire16-mul-add (posit16->quire16 (*.p16 x.im x.re)) (*.p16 x.im x.re) (real->posit16 1.0))
  (quire16-mul-add (posit16->quire16 (*.p16 x.im x.re)) x.im x.re)
  (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 x.re (-.p16 (*.p16 (-.p16 x.re x.im) (+.p16 x.im x.re)) (*.p16 (+.p16 x.im x.im) x.im)))
  (*.p16 x.re (-.p16 (*.p16 (-.p16 x.re x.im) (+.p16 x.im x.re)) (*.p16 (+.p16 x.im x.im) x.im)))
  (*.p16 x.re (-.p16 (*.p16 (-.p16 x.re x.im) (+.p16 x.im x.re)) (*.p16 (+.p16 x.im x.im) x.im)))
  (*.p16 x.re (-.p16 (*.p16 (-.p16 x.re x.im) (+.p16 x.im x.re)) (*.p16 (+.p16 x.im x.im) x.im)))
42.213 * * * [progress]: adding candidates to table
44.010 * * [progress]: iteration 2 / 4
44.011 * * * [progress]: picking best candidate
44.083 * * * * [pick]: Picked  #<alt (λ (x.re x.im) (quire16->posit16 (posit16->quire16 (*.p16 x.re (-.p16 (*.p16 (-.p16 x.re x.im) (+.p16 x.im x.re)) (*.p16 (+.p16 x.im x.im) x.im))))))>
44.084 * * * [progress]: localizing error
44.280 * * * [progress]: generating rewritten candidates
44.280 * * * * [progress]: [ 1 / 4 ] rewriting at (2 1 1 2)
44.292 * * * * [progress]: [ 2 / 4 ] rewriting at (2 1 1)
44.295 * * * * [progress]: [ 3 / 4 ] rewriting at (2 1 1 2 1)
44.298 * * * * [progress]: [ 4 / 4 ] rewriting at (2 1 1 2 2)
44.304 * * * [progress]: generating series expansions
44.304 * * * * [progress]: [ 1 / 4 ] generating series at (2 1 1 2)
44.304 * * * * [progress]: [ 2 / 4 ] generating series at (2 1 1)
44.304 * * * * [progress]: [ 3 / 4 ] generating series at (2 1 1 2 1)
44.304 * * * * [progress]: [ 4 / 4 ] generating series at (2 1 1 2 2)
44.304 * * * [progress]: simplifying candidates
44.304 * * * * [progress]: [ 1 / 87 ] simplifiying candidate #<alt (λ (x.re x.im) (quire16->posit16 (posit16->quire16 (*.p16 x.re (-.p16 (-.p16 (*.p16 (-.p16 x.re x.im) (+.p16 x.im x.re)) (real->posit16 0.0)) (*.p16 (+.p16 x.im x.im) x.im))))))>
44.304 * * * * [progress]: [ 2 / 87 ] simplifiying candidate #<alt (λ (x.re x.im) (quire16->posit16 (posit16->quire16 (*.p16 x.re (-.p16 (-.p16 (*.p16 (-.p16 x.re x.im) (+.p16 x.im x.re)) (*.p16 (+.p16 x.im x.im) x.im)) (real->posit16 0.0))))))>
44.304 * * * * [progress]: [ 3 / 87 ] simplifiying candidate #<alt (λ (x.re x.im) (quire16->posit16 (posit16->quire16 (*.p16 x.re (+.p16 (*.p16 (-.p16 x.re x.im) x.im) (-.p16 (*.p16 (-.p16 x.re x.im) x.re) (*.p16 (+.p16 x.im x.im) x.im)))))))>
44.304 * * * * [progress]: [ 4 / 87 ] simplifiying candidate #<alt (λ (x.re x.im) (quire16->posit16 (posit16->quire16 (*.p16 x.re (+.p16 (*.p16 x.im (-.p16 x.re x.im)) (-.p16 (*.p16 x.re (-.p16 x.re x.im)) (*.p16 (+.p16 x.im x.im) x.im)))))))>
44.304 * * * * [progress]: [ 5 / 87 ] simplifiying candidate #<alt (λ (x.re x.im) (quire16->posit16 (posit16->quire16 (*.p16 x.re (+.p16 (real->posit16 0.0) (-.p16 (*.p16 (-.p16 x.re x.im) (+.p16 x.im x.re)) (*.p16 (+.p16 x.im x.im) x.im)))))))>
44.304 * * * * [progress]: [ 6 / 87 ] simplifiying candidate #<alt (λ (x.re x.im) (quire16->posit16 (posit16->quire16 (*.p16 x.re (+.p16 (*.p16 (-.p16 x.re x.im) (+.p16 x.im x.re)) (-.p16 (real->posit16 0.0) (*.p16 (+.p16 x.im x.im) x.im)))))))>
44.304 * * * * [progress]: [ 7 / 87 ] simplifiying candidate #<alt (λ (x.re x.im) (quire16->posit16 (posit16->quire16 (*.p16 x.re (-.p16 (*.p16 (-.p16 x.re x.im) (+.p16 x.im x.re)) (+.p16 (real->posit16 0.0) (*.p16 (+.p16 x.im x.im) x.im)))))))>
44.304 * * * * [progress]: [ 8 / 87 ] simplifiying candidate #<alt (λ (x.re x.im) (quire16->posit16 (posit16->quire16 (*.p16 x.re (+.p16 (-.p16 (*.p16 (-.p16 x.re x.im) (+.p16 x.im x.re)) (*.p16 (+.p16 x.im x.im) x.im)) (real->posit16 0.0))))))>
44.304 * * * * [progress]: [ 9 / 87 ] simplifiying candidate #<alt (λ (x.re x.im) (quire16->posit16 (posit16->quire16 (*.p16 x.re (+.p16 (*.p16 (-.p16 x.re x.im) (+.p16 x.im x.re)) (neg.p16 (*.p16 (+.p16 x.im x.im) x.im)))))))>
44.304 * * * * [progress]: [ 10 / 87 ] simplifiying candidate #<alt (λ (x.re x.im) (quire16->posit16 (posit16->quire16 (*.p16 x.re (/.p16 (-.p16 (*.p16 (*.p16 (-.p16 x.re x.im) (+.p16 x.im x.re)) (*.p16 (-.p16 x.re x.im) (+.p16 x.im x.re))) (*.p16 (*.p16 (+.p16 x.im x.im) x.im) (*.p16 (+.p16 x.im x.im) x.im))) (+.p16 (*.p16 (-.p16 x.re x.im) (+.p16 x.im x.re)) (*.p16 (+.p16 x.im x.im) x.im)))))))>
44.304 * * * * [progress]: [ 11 / 87 ] simplifiying candidate #<alt (λ (x.re x.im) (quire16->posit16 (posit16->quire16 (*.p16 x.re (*.p16 (real->posit16 1.0) (-.p16 (*.p16 (-.p16 x.re x.im) (+.p16 x.im x.re)) (*.p16 (+.p16 x.im x.im) x.im)))))))>
44.304 * * * * [progress]: [ 12 / 87 ] simplifiying candidate #<alt (λ (x.re x.im) (quire16->posit16 (posit16->quire16 (*.p16 x.re (quire16->posit16 (posit16->quire16 (-.p16 (*.p16 (-.p16 x.re x.im) (+.p16 x.im x.re)) (*.p16 (+.p16 x.im x.im) x.im))))))))>
44.304 * * * * [progress]: [ 13 / 87 ] simplifiying candidate #<alt (λ (x.re x.im) (quire16->posit16 (posit16->quire16 (*.p16 x.re (quire16->posit16 (quire16-mul-sub (posit16->quire16 (*.p16 (-.p16 x.re x.im) (+.p16 x.im x.re))) (*.p16 (+.p16 x.im x.im) x.im) (real->posit16 1.0)))))))>
44.304 * * * * [progress]: [ 14 / 87 ] simplifiying candidate #<alt (λ (x.re x.im) (quire16->posit16 (posit16->quire16 (*.p16 x.re (quire16->posit16 (quire16-mul-sub (posit16->quire16 (*.p16 (-.p16 x.re x.im) (+.p16 x.im x.re))) (+.p16 x.im x.im) x.im))))))>
44.304 * * * * [progress]: [ 15 / 87 ] simplifiying candidate #<alt (λ (x.re x.im) (quire16->posit16 (posit16->quire16 (*.p16 x.re (+.p16 (real->posit16 0.0) (-.p16 (*.p16 (-.p16 x.re x.im) (+.p16 x.im x.re)) (*.p16 (+.p16 x.im x.im) x.im)))))))>
44.304 * * * * [progress]: [ 16 / 87 ] simplifiying candidate #<alt (λ (x.re x.im) (quire16->posit16 (posit16->quire16 (*.p16 x.re (+.p16 (-.p16 (*.p16 (-.p16 x.re x.im) (+.p16 x.im x.re)) (*.p16 (+.p16 x.im x.im) x.im)) (real->posit16 0.0))))))>
44.304 * * * * [progress]: [ 17 / 87 ] simplifiying candidate #<alt (λ (x.re x.im) (quire16->posit16 (posit16->quire16 (*.p16 x.re (-.p16 (-.p16 (*.p16 (-.p16 x.re x.im) (+.p16 x.im x.re)) (*.p16 (+.p16 x.im x.im) x.im)) (real->posit16 0.0))))))>
44.304 * * * * [progress]: [ 18 / 87 ] simplifiying candidate #<alt (λ (x.re x.im) (quire16->posit16 (posit16->quire16 (*.p16 x.re (*.p16 (real->posit16 1.0) (-.p16 (*.p16 (-.p16 x.re x.im) (+.p16 x.im x.re)) (*.p16 (+.p16 x.im x.im) x.im)))))))>
44.305 * * * * [progress]: [ 19 / 87 ] simplifiying candidate #<alt (λ (x.re x.im) (quire16->posit16 (posit16->quire16 (*.p16 x.re (*.p16 (-.p16 (*.p16 (-.p16 x.re x.im) (+.p16 x.im x.re)) (*.p16 (+.p16 x.im x.im) x.im)) (real->posit16 1.0))))))>
44.305 * * * * [progress]: [ 20 / 87 ] simplifiying candidate #<alt (λ (x.re x.im) (quire16->posit16 (posit16->quire16 (*.p16 x.re (/.p16 (-.p16 (*.p16 (-.p16 x.re x.im) (+.p16 x.im x.re)) (*.p16 (+.p16 x.im x.im) x.im)) (real->posit16 1.0))))))>
44.305 * * * * [progress]: [ 21 / 87 ] simplifiying candidate #<alt (λ (x.re x.im) (quire16->posit16 (posit16->quire16 (+.p16 (*.p16 x.re (*.p16 (-.p16 x.re x.im) x.im)) (*.p16 x.re (-.p16 (*.p16 (-.p16 x.re x.im) x.re) (*.p16 (+.p16 x.im x.im) x.im)))))))>
44.305 * * * * [progress]: [ 22 / 87 ] simplifiying candidate #<alt (λ (x.re x.im) (quire16->posit16 (posit16->quire16 (+.p16 (*.p16 x.re (*.p16 x.im (-.p16 x.re x.im))) (*.p16 x.re (-.p16 (*.p16 x.re (-.p16 x.re x.im)) (*.p16 (+.p16 x.im x.im) x.im)))))))>
44.305 * * * * [progress]: [ 23 / 87 ] simplifiying candidate #<alt (λ (x.re x.im) (quire16->posit16 (posit16->quire16 (+.p16 (*.p16 x.re (real->posit16 0.0)) (*.p16 x.re (-.p16 (*.p16 (-.p16 x.re x.im) (+.p16 x.im x.re)) (*.p16 (+.p16 x.im x.im) x.im)))))))>
44.305 * * * * [progress]: [ 24 / 87 ] simplifiying candidate #<alt (λ (x.re x.im) (quire16->posit16 (posit16->quire16 (+.p16 (*.p16 x.re (*.p16 (-.p16 x.re x.im) (+.p16 x.im x.re))) (*.p16 x.re (-.p16 (real->posit16 0.0) (*.p16 (+.p16 x.im x.im) x.im)))))))>
44.305 * * * * [progress]: [ 25 / 87 ] simplifiying candidate #<alt (λ (x.re x.im) (quire16->posit16 (posit16->quire16 (+.p16 (*.p16 x.re (-.p16 (*.p16 (-.p16 x.re x.im) (+.p16 x.im x.re)) (*.p16 (+.p16 x.im x.im) x.im))) (*.p16 x.re (real->posit16 0.0))))))>
44.305 * * * * [progress]: [ 26 / 87 ] simplifiying candidate #<alt (λ (x.re x.im) (quire16->posit16 (posit16->quire16 (+.p16 (*.p16 x.re (*.p16 (-.p16 x.re x.im) (+.p16 x.im x.re))) (*.p16 x.re (neg.p16 (*.p16 (+.p16 x.im x.im) x.im)))))))>
44.305 * * * * [progress]: [ 27 / 87 ] simplifiying candidate #<alt (λ (x.re x.im) (quire16->posit16 (posit16->quire16 (+.p16 (*.p16 x.re (real->posit16 0.0)) (*.p16 x.re (-.p16 (*.p16 (-.p16 x.re x.im) (+.p16 x.im x.re)) (*.p16 (+.p16 x.im x.im) x.im)))))))>
44.305 * * * * [progress]: [ 28 / 87 ] simplifiying candidate #<alt (λ (x.re x.im) (quire16->posit16 (posit16->quire16 (+.p16 (*.p16 x.re (-.p16 (*.p16 (-.p16 x.re x.im) (+.p16 x.im x.re)) (*.p16 (+.p16 x.im x.im) x.im))) (*.p16 x.re (real->posit16 0.0))))))>
44.305 * * * * [progress]: [ 29 / 87 ] simplifiying candidate #<alt (λ (x.re x.im) (quire16->posit16 (posit16->quire16 (+.p16 (*.p16 (*.p16 (-.p16 x.re x.im) x.im) x.re) (*.p16 (-.p16 (*.p16 (-.p16 x.re x.im) x.re) (*.p16 (+.p16 x.im x.im) x.im)) x.re)))))>
44.305 * * * * [progress]: [ 30 / 87 ] simplifiying candidate #<alt (λ (x.re x.im) (quire16->posit16 (posit16->quire16 (+.p16 (*.p16 (*.p16 x.im (-.p16 x.re x.im)) x.re) (*.p16 (-.p16 (*.p16 x.re (-.p16 x.re x.im)) (*.p16 (+.p16 x.im x.im) x.im)) x.re)))))>
44.305 * * * * [progress]: [ 31 / 87 ] simplifiying candidate #<alt (λ (x.re x.im) (quire16->posit16 (posit16->quire16 (+.p16 (*.p16 (real->posit16 0.0) x.re) (*.p16 (-.p16 (*.p16 (-.p16 x.re x.im) (+.p16 x.im x.re)) (*.p16 (+.p16 x.im x.im) x.im)) x.re)))))>
44.305 * * * * [progress]: [ 32 / 87 ] simplifiying candidate #<alt (λ (x.re x.im) (quire16->posit16 (posit16->quire16 (+.p16 (*.p16 (*.p16 (-.p16 x.re x.im) (+.p16 x.im x.re)) x.re) (*.p16 (-.p16 (real->posit16 0.0) (*.p16 (+.p16 x.im x.im) x.im)) x.re)))))>
44.305 * * * * [progress]: [ 33 / 87 ] simplifiying candidate #<alt (λ (x.re x.im) (quire16->posit16 (posit16->quire16 (+.p16 (*.p16 (-.p16 (*.p16 (-.p16 x.re x.im) (+.p16 x.im x.re)) (*.p16 (+.p16 x.im x.im) x.im)) x.re) (*.p16 (real->posit16 0.0) x.re)))))>
44.305 * * * * [progress]: [ 34 / 87 ] simplifiying candidate #<alt (λ (x.re x.im) (quire16->posit16 (posit16->quire16 (+.p16 (*.p16 (*.p16 (-.p16 x.re x.im) (+.p16 x.im x.re)) x.re) (*.p16 (neg.p16 (*.p16 (+.p16 x.im x.im) x.im)) x.re)))))>
44.305 * * * * [progress]: [ 35 / 87 ] simplifiying candidate #<alt (λ (x.re x.im) (quire16->posit16 (posit16->quire16 (+.p16 (*.p16 (real->posit16 0.0) x.re) (*.p16 (-.p16 (*.p16 (-.p16 x.re x.im) (+.p16 x.im x.re)) (*.p16 (+.p16 x.im x.im) x.im)) x.re)))))>
44.305 * * * * [progress]: [ 36 / 87 ] simplifiying candidate #<alt (λ (x.re x.im) (quire16->posit16 (posit16->quire16 (+.p16 (*.p16 (-.p16 (*.p16 (-.p16 x.re x.im) (+.p16 x.im x.re)) (*.p16 (+.p16 x.im x.im) x.im)) x.re) (*.p16 (real->posit16 0.0) x.re)))))>
44.305 * * * * [progress]: [ 37 / 87 ] simplifiying candidate #<alt (λ (x.re x.im) (quire16->posit16 (posit16->quire16 (*.p16 (*.p16 x.re (real->posit16 1.0)) (-.p16 (*.p16 (-.p16 x.re x.im) (+.p16 x.im x.re)) (*.p16 (+.p16 x.im x.im) x.im))))))>
44.305 * * * * [progress]: [ 38 / 87 ] simplifiying candidate #<alt (λ (x.re x.im) (quire16->posit16 (posit16->quire16 (*.p16 (*.p16 x.re (real->posit16 1.0)) (-.p16 (*.p16 (-.p16 x.re x.im) (+.p16 x.im x.re)) (*.p16 (+.p16 x.im x.im) x.im))))))>
44.305 * * * * [progress]: [ 39 / 87 ] simplifiying candidate #<alt (λ (x.re x.im) (quire16->posit16 (posit16->quire16 (*.p16 (*.p16 x.re (-.p16 (*.p16 (-.p16 x.re x.im) (+.p16 x.im x.re)) (*.p16 (+.p16 x.im x.im) x.im))) (real->posit16 1.0)))))>
44.305 * * * * [progress]: [ 40 / 87 ] simplifiying candidate #<alt (λ (x.re x.im) (quire16->posit16 (posit16->quire16 (/.p16 (*.p16 x.re (-.p16 (*.p16 (*.p16 (-.p16 x.re x.im) (+.p16 x.im x.re)) (*.p16 (-.p16 x.re x.im) (+.p16 x.im x.re))) (*.p16 (*.p16 (+.p16 x.im x.im) x.im) (*.p16 (+.p16 x.im x.im) x.im)))) (+.p16 (*.p16 (-.p16 x.re x.im) (+.p16 x.im x.re)) (*.p16 (+.p16 x.im x.im) x.im))))))>
44.305 * * * * [progress]: [ 41 / 87 ] simplifiying candidate #<alt (λ (x.re x.im) (quire16->posit16 (posit16->quire16 (/.p16 (*.p16 x.re (-.p16 (*.p16 (-.p16 x.re x.im) (+.p16 x.im x.re)) (*.p16 (+.p16 x.im x.im) x.im))) (real->posit16 1.0)))))>
44.305 * * * * [progress]: [ 42 / 87 ] simplifiying candidate #<alt (λ (x.re x.im) (quire16->posit16 (posit16->quire16 (*.p16 (real->posit16 1.0) (*.p16 x.re (-.p16 (*.p16 (-.p16 x.re x.im) (+.p16 x.im x.re)) (*.p16 (+.p16 x.im x.im) x.im)))))))>
44.305 * * * * [progress]: [ 43 / 87 ] simplifiying candidate #<alt (λ (x.re x.im) (quire16->posit16 (posit16->quire16 (quire16->posit16 (posit16->quire16 (*.p16 x.re (-.p16 (*.p16 (-.p16 x.re x.im) (+.p16 x.im x.re)) (*.p16 (+.p16 x.im x.im) x.im))))))))>
44.305 * * * * [progress]: [ 44 / 87 ] simplifiying candidate #<alt (λ (x.re x.im) (quire16->posit16 (posit16->quire16 (+.p16 (real->posit16 0.0) (*.p16 x.re (-.p16 (*.p16 (-.p16 x.re x.im) (+.p16 x.im x.re)) (*.p16 (+.p16 x.im x.im) x.im)))))))>
44.305 * * * * [progress]: [ 45 / 87 ] simplifiying candidate #<alt (λ (x.re x.im) (quire16->posit16 (posit16->quire16 (+.p16 (*.p16 x.re (-.p16 (*.p16 (-.p16 x.re x.im) (+.p16 x.im x.re)) (*.p16 (+.p16 x.im x.im) x.im))) (real->posit16 0.0)))))>
44.306 * * * * [progress]: [ 46 / 87 ] simplifiying candidate #<alt (λ (x.re x.im) (quire16->posit16 (posit16->quire16 (-.p16 (*.p16 x.re (-.p16 (*.p16 (-.p16 x.re x.im) (+.p16 x.im x.re)) (*.p16 (+.p16 x.im x.im) x.im))) (real->posit16 0.0)))))>
44.306 * * * * [progress]: [ 47 / 87 ] simplifiying candidate #<alt (λ (x.re x.im) (quire16->posit16 (posit16->quire16 (*.p16 (real->posit16 1.0) (*.p16 x.re (-.p16 (*.p16 (-.p16 x.re x.im) (+.p16 x.im x.re)) (*.p16 (+.p16 x.im x.im) x.im)))))))>
44.306 * * * * [progress]: [ 48 / 87 ] simplifiying candidate #<alt (λ (x.re x.im) (quire16->posit16 (posit16->quire16 (*.p16 (*.p16 x.re (-.p16 (*.p16 (-.p16 x.re x.im) (+.p16 x.im x.re)) (*.p16 (+.p16 x.im x.im) x.im))) (real->posit16 1.0)))))>
44.306 * * * * [progress]: [ 49 / 87 ] simplifiying candidate #<alt (λ (x.re x.im) (quire16->posit16 (posit16->quire16 (/.p16 (*.p16 x.re (-.p16 (*.p16 (-.p16 x.re x.im) (+.p16 x.im x.re)) (*.p16 (+.p16 x.im x.im) x.im))) (real->posit16 1.0)))))>
44.306 * * * * [progress]: [ 50 / 87 ] simplifiying candidate #<alt (λ (x.re x.im) (quire16->posit16 (posit16->quire16 (*.p16 (-.p16 (*.p16 (-.p16 x.re x.im) (+.p16 x.im x.re)) (*.p16 (+.p16 x.im x.im) x.im)) x.re))))>
44.306 * * * * [progress]: [ 51 / 87 ] simplifiying candidate #<alt (λ (x.re x.im) (quire16->posit16 (posit16->quire16 (*.p16 x.re (-.p16 (+.p16 (*.p16 (-.p16 x.re x.im) x.im) (*.p16 (-.p16 x.re x.im) x.re)) (*.p16 (+.p16 x.im x.im) x.im))))))>
44.306 * * * * [progress]: [ 52 / 87 ] simplifiying candidate #<alt (λ (x.re x.im) (quire16->posit16 (posit16->quire16 (*.p16 x.re (-.p16 (+.p16 (*.p16 x.im (-.p16 x.re x.im)) (*.p16 x.re (-.p16 x.re x.im))) (*.p16 (+.p16 x.im x.im) x.im))))))>
44.306 * * * * [progress]: [ 53 / 87 ] simplifiying candidate #<alt (λ (x.re x.im) (quire16->posit16 (posit16->quire16 (*.p16 x.re (-.p16 (*.p16 (*.p16 (-.p16 x.re x.im) (real->posit16 1.0)) (+.p16 x.im x.re)) (*.p16 (+.p16 x.im x.im) x.im))))))>
44.306 * * * * [progress]: [ 54 / 87 ] simplifiying candidate #<alt (λ (x.re x.im) (quire16->posit16 (posit16->quire16 (*.p16 x.re (-.p16 (*.p16 (*.p16 (-.p16 x.re x.im) (real->posit16 1.0)) (+.p16 x.im x.re)) (*.p16 (+.p16 x.im x.im) x.im))))))>
44.306 * * * * [progress]: [ 55 / 87 ] simplifiying candidate #<alt (λ (x.re x.im) (quire16->posit16 (posit16->quire16 (*.p16 x.re (-.p16 (*.p16 (*.p16 (-.p16 x.re x.im) (+.p16 x.im x.re)) (real->posit16 1.0)) (*.p16 (+.p16 x.im x.im) x.im))))))>
44.306 * * * * [progress]: [ 56 / 87 ] simplifiying candidate #<alt (λ (x.re x.im) (quire16->posit16 (posit16->quire16 (*.p16 x.re (-.p16 (*.p16 (real->posit16 1.0) (*.p16 (-.p16 x.re x.im) (+.p16 x.im x.re))) (*.p16 (+.p16 x.im x.im) x.im))))))>
44.306 * * * * [progress]: [ 57 / 87 ] simplifiying candidate #<alt (λ (x.re x.im) (quire16->posit16 (posit16->quire16 (*.p16 x.re (-.p16 (*.p16 (real->posit16 1.0) (*.p16 (-.p16 x.re x.im) (+.p16 x.im x.re))) (*.p16 (+.p16 x.im x.im) x.im))))))>
44.306 * * * * [progress]: [ 58 / 87 ] simplifiying candidate #<alt (λ (x.re x.im) (quire16->posit16 (posit16->quire16 (*.p16 x.re (-.p16 (*.p16 (-.p16 x.re x.im) (*.p16 (real->posit16 1.0) (+.p16 x.im x.re))) (*.p16 (+.p16 x.im x.im) x.im))))))>
44.306 * * * * [progress]: [ 59 / 87 ] simplifiying candidate #<alt (λ (x.re x.im) (quire16->posit16 (posit16->quire16 (*.p16 x.re (-.p16 (/.p16 (*.p16 (-.p16 x.re x.im) (+.p16 x.im x.re)) (real->posit16 1.0)) (*.p16 (+.p16 x.im x.im) x.im))))))>
44.306 * * * * [progress]: [ 60 / 87 ] simplifiying candidate #<alt (λ (x.re x.im) (quire16->posit16 (posit16->quire16 (*.p16 x.re (-.p16 (/.p16 (*.p16 (-.p16 (*.p16 x.re x.re) (*.p16 x.im x.im)) (+.p16 x.im x.re)) (+.p16 x.re x.im)) (*.p16 (+.p16 x.im x.im) x.im))))))>
44.306 * * * * [progress]: [ 61 / 87 ] simplifiying candidate #<alt (λ (x.re x.im) (quire16->posit16 (posit16->quire16 (*.p16 x.re (-.p16 (/.p16 (*.p16 (-.p16 x.re x.im) (+.p16 x.im x.re)) (real->posit16 1.0)) (*.p16 (+.p16 x.im x.im) x.im))))))>
44.306 * * * * [progress]: [ 62 / 87 ] simplifiying candidate #<alt (λ (x.re x.im) (quire16->posit16 (posit16->quire16 (*.p16 x.re (-.p16 (*.p16 (real->posit16 1.0) (*.p16 (-.p16 x.re x.im) (+.p16 x.im x.re))) (*.p16 (+.p16 x.im x.im) x.im))))))>
44.306 * * * * [progress]: [ 63 / 87 ] simplifiying candidate #<alt (λ (x.re x.im) (quire16->posit16 (posit16->quire16 (*.p16 x.re (-.p16 (quire16->posit16 (posit16->quire16 (*.p16 (-.p16 x.re x.im) (+.p16 x.im x.re)))) (*.p16 (+.p16 x.im x.im) x.im))))))>
44.306 * * * * [progress]: [ 64 / 87 ] simplifiying candidate #<alt (λ (x.re x.im) (quire16->posit16 (posit16->quire16 (*.p16 x.re (-.p16 (+.p16 (real->posit16 0.0) (*.p16 (-.p16 x.re x.im) (+.p16 x.im x.re))) (*.p16 (+.p16 x.im x.im) x.im))))))>
44.306 * * * * [progress]: [ 65 / 87 ] simplifiying candidate #<alt (λ (x.re x.im) (quire16->posit16 (posit16->quire16 (*.p16 x.re (-.p16 (+.p16 (*.p16 (-.p16 x.re x.im) (+.p16 x.im x.re)) (real->posit16 0.0)) (*.p16 (+.p16 x.im x.im) x.im))))))>
44.306 * * * * [progress]: [ 66 / 87 ] simplifiying candidate #<alt (λ (x.re x.im) (quire16->posit16 (posit16->quire16 (*.p16 x.re (-.p16 (-.p16 (*.p16 (-.p16 x.re x.im) (+.p16 x.im x.re)) (real->posit16 0.0)) (*.p16 (+.p16 x.im x.im) x.im))))))>
44.306 * * * * [progress]: [ 67 / 87 ] simplifiying candidate #<alt (λ (x.re x.im) (quire16->posit16 (posit16->quire16 (*.p16 x.re (-.p16 (*.p16 (real->posit16 1.0) (*.p16 (-.p16 x.re x.im) (+.p16 x.im x.re))) (*.p16 (+.p16 x.im x.im) x.im))))))>
44.306 * * * * [progress]: [ 68 / 87 ] simplifiying candidate #<alt (λ (x.re x.im) (quire16->posit16 (posit16->quire16 (*.p16 x.re (-.p16 (*.p16 (*.p16 (-.p16 x.re x.im) (+.p16 x.im x.re)) (real->posit16 1.0)) (*.p16 (+.p16 x.im x.im) x.im))))))>
44.306 * * * * [progress]: [ 69 / 87 ] simplifiying candidate #<alt (λ (x.re x.im) (quire16->posit16 (posit16->quire16 (*.p16 x.re (-.p16 (/.p16 (*.p16 (-.p16 x.re x.im) (+.p16 x.im x.re)) (real->posit16 1.0)) (*.p16 (+.p16 x.im x.im) x.im))))))>
44.306 * * * * [progress]: [ 70 / 87 ] simplifiying candidate #<alt (λ (x.re x.im) (quire16->posit16 (posit16->quire16 (*.p16 x.re (-.p16 (*.p16 (+.p16 x.im x.re) (-.p16 x.re x.im)) (*.p16 (+.p16 x.im x.im) x.im))))))>
44.306 * * * * [progress]: [ 71 / 87 ] simplifiying candidate #<alt (λ (x.re x.im) (quire16->posit16 (posit16->quire16 (*.p16 x.re (-.p16 (*.p16 (-.p16 x.re x.im) (+.p16 x.im x.re)) (*.p16 (real->posit16 1.0) (*.p16 (+.p16 x.im x.im) x.im)))))))>
44.306 * * * * [progress]: [ 72 / 87 ] simplifiying candidate #<alt (λ (x.re x.im) (quire16->posit16 (posit16->quire16 (*.p16 x.re (-.p16 (*.p16 (-.p16 x.re x.im) (+.p16 x.im x.re)) (*.p16 (real->posit16 1.0) (*.p16 (+.p16 x.im x.im) x.im)))))))>
44.307 * * * * [progress]: [ 73 / 87 ] simplifiying candidate #<alt (λ (x.re x.im) (quire16->posit16 (posit16->quire16 (*.p16 x.re (-.p16 (*.p16 (-.p16 x.re x.im) (+.p16 x.im x.re)) (*.p16 (+.p16 x.im x.im) (*.p16 (real->posit16 1.0) x.im)))))))>
44.307 * * * * [progress]: [ 74 / 87 ] simplifiying candidate #<alt (λ (x.re x.im) (quire16->posit16 (posit16->quire16 (*.p16 x.re (-.p16 (*.p16 (-.p16 x.re x.im) (+.p16 x.im x.re)) (/.p16 (*.p16 (+.p16 x.im x.im) x.im) (real->posit16 1.0)))))))>
44.307 * * * * [progress]: [ 75 / 87 ] simplifiying candidate #<alt (λ (x.re x.im) (quire16->posit16 (posit16->quire16 (*.p16 x.re (-.p16 (*.p16 (-.p16 x.re x.im) (+.p16 x.im x.re)) (*.p16 (real->posit16 1.0) (*.p16 (+.p16 x.im x.im) x.im)))))))>
44.307 * * * * [progress]: [ 76 / 87 ] simplifiying candidate #<alt (λ (x.re x.im) (quire16->posit16 (posit16->quire16 (*.p16 x.re (-.p16 (*.p16 (-.p16 x.re x.im) (+.p16 x.im x.re)) (quire16->posit16 (posit16->quire16 (*.p16 (+.p16 x.im x.im) x.im))))))))>
44.307 * * * * [progress]: [ 77 / 87 ] simplifiying candidate #<alt (λ (x.re x.im) (quire16->posit16 (posit16->quire16 (*.p16 x.re (-.p16 (*.p16 (-.p16 x.re x.im) (+.p16 x.im x.re)) (+.p16 (real->posit16 0.0) (*.p16 (+.p16 x.im x.im) x.im)))))))>
44.307 * * * * [progress]: [ 78 / 87 ] simplifiying candidate #<alt (λ (x.re x.im) (quire16->posit16 (posit16->quire16 (*.p16 x.re (-.p16 (*.p16 (-.p16 x.re x.im) (+.p16 x.im x.re)) (+.p16 (*.p16 (+.p16 x.im x.im) x.im) (real->posit16 0.0)))))))>
44.307 * * * * [progress]: [ 79 / 87 ] simplifiying candidate #<alt (λ (x.re x.im) (quire16->posit16 (posit16->quire16 (*.p16 x.re (-.p16 (*.p16 (-.p16 x.re x.im) (+.p16 x.im x.re)) (-.p16 (*.p16 (+.p16 x.im x.im) x.im) (real->posit16 0.0)))))))>
44.307 * * * * [progress]: [ 80 / 87 ] simplifiying candidate #<alt (λ (x.re x.im) (quire16->posit16 (posit16->quire16 (*.p16 x.re (-.p16 (*.p16 (-.p16 x.re x.im) (+.p16 x.im x.re)) (*.p16 (real->posit16 1.0) (*.p16 (+.p16 x.im x.im) x.im)))))))>
44.307 * * * * [progress]: [ 81 / 87 ] simplifiying candidate #<alt (λ (x.re x.im) (quire16->posit16 (posit16->quire16 (*.p16 x.re (-.p16 (*.p16 (-.p16 x.re x.im) (+.p16 x.im x.re)) (*.p16 (*.p16 (+.p16 x.im x.im) x.im) (real->posit16 1.0)))))))>
44.307 * * * * [progress]: [ 82 / 87 ] simplifiying candidate #<alt (λ (x.re x.im) (quire16->posit16 (posit16->quire16 (*.p16 x.re (-.p16 (*.p16 (-.p16 x.re x.im) (+.p16 x.im x.re)) (/.p16 (*.p16 (+.p16 x.im x.im) x.im) (real->posit16 1.0)))))))>
44.307 * * * * [progress]: [ 83 / 87 ] simplifiying candidate #<alt (λ (x.re x.im) (quire16->posit16 (posit16->quire16 (*.p16 x.re (-.p16 (*.p16 (-.p16 x.re x.im) (+.p16 x.im x.re)) (*.p16 x.im (+.p16 x.im x.im)))))))>
44.307 * * * * [progress]: [ 84 / 87 ] simplifiying candidate #<alt (λ (x.re x.im) (quire16->posit16 (posit16->quire16 (*.p16 x.re (-.p16 (*.p16 (-.p16 x.re x.im) (+.p16 x.im x.re)) (*.p16 (+.p16 x.im x.im) x.im))))))>
44.307 * * * * [progress]: [ 85 / 87 ] simplifiying candidate #<alt (λ (x.re x.im) (quire16->posit16 (posit16->quire16 (*.p16 x.re (-.p16 (*.p16 (-.p16 x.re x.im) (+.p16 x.im x.re)) (*.p16 (+.p16 x.im x.im) x.im))))))>
44.307 * * * * [progress]: [ 86 / 87 ] simplifiying candidate #<alt (λ (x.re x.im) (quire16->posit16 (posit16->quire16 (*.p16 x.re (-.p16 (*.p16 (-.p16 x.re x.im) (+.p16 x.im x.re)) (*.p16 (+.p16 x.im x.im) x.im))))))>
44.307 * * * * [progress]: [ 87 / 87 ] simplifiying candidate #<alt (λ (x.re x.im) (quire16->posit16 (posit16->quire16 (*.p16 x.re (-.p16 (*.p16 (-.p16 x.re x.im) (+.p16 x.im x.re)) (*.p16 (+.p16 x.im x.im) x.im))))))>
44.308 * [simplify]: Simplifying:
  (-.p16 (*.p16 (-.p16 x.re x.im) (+.p16 x.im x.re)) (real->posit16 0.0))
  (-.p16 (*.p16 (-.p16 x.re x.im) (+.p16 x.im x.re)) (*.p16 (+.p16 x.im x.im) x.im))
  (-.p16 (*.p16 (-.p16 x.re x.im) x.re) (*.p16 (+.p16 x.im x.im) x.im))
  (-.p16 (*.p16 x.re (-.p16 x.re x.im)) (*.p16 (+.p16 x.im x.im) x.im))
  (-.p16 (*.p16 (-.p16 x.re x.im) (+.p16 x.im x.re)) (*.p16 (+.p16 x.im x.im) x.im))
  (-.p16 (real->posit16 0.0) (*.p16 (+.p16 x.im x.im) x.im))
  (+.p16 (real->posit16 0.0) (*.p16 (+.p16 x.im x.im) x.im))
  (-.p16 (*.p16 (-.p16 x.re x.im) (+.p16 x.im x.re)) (*.p16 (+.p16 x.im x.im) x.im))
  (neg.p16 (*.p16 (+.p16 x.im x.im) x.im))
  (-.p16 (*.p16 (*.p16 (-.p16 x.re x.im) (+.p16 x.im x.re)) (*.p16 (-.p16 x.re x.im) (+.p16 x.im x.re))) (*.p16 (*.p16 (+.p16 x.im x.im) x.im) (*.p16 (+.p16 x.im x.im) x.im)))
  (+.p16 (*.p16 (-.p16 x.re x.im) (+.p16 x.im x.re)) (*.p16 (+.p16 x.im x.im) x.im))
  (real->posit16 1.0)
  (posit16->quire16 (-.p16 (*.p16 (-.p16 x.re x.im) (+.p16 x.im x.re)) (*.p16 (+.p16 x.im x.im) x.im)))
  (quire16-mul-sub (posit16->quire16 (*.p16 (-.p16 x.re x.im) (+.p16 x.im x.re))) (*.p16 (+.p16 x.im x.im) x.im) (real->posit16 1.0))
  (quire16-mul-sub (posit16->quire16 (*.p16 (-.p16 x.re x.im) (+.p16 x.im x.re))) (+.p16 x.im x.im) x.im)
  (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 x.re (*.p16 (-.p16 x.re x.im) x.im))
  (*.p16 x.re (-.p16 (*.p16 (-.p16 x.re x.im) x.re) (*.p16 (+.p16 x.im x.im) x.im)))
  (*.p16 x.re (*.p16 x.im (-.p16 x.re x.im)))
  (*.p16 x.re (-.p16 (*.p16 x.re (-.p16 x.re x.im)) (*.p16 (+.p16 x.im x.im) x.im)))
  (*.p16 x.re (real->posit16 0.0))
  (*.p16 x.re (-.p16 (*.p16 (-.p16 x.re x.im) (+.p16 x.im x.re)) (*.p16 (+.p16 x.im x.im) x.im)))
  (*.p16 x.re (*.p16 (-.p16 x.re x.im) (+.p16 x.im x.re)))
  (*.p16 x.re (-.p16 (real->posit16 0.0) (*.p16 (+.p16 x.im x.im) x.im)))
  (*.p16 x.re (-.p16 (*.p16 (-.p16 x.re x.im) (+.p16 x.im x.re)) (*.p16 (+.p16 x.im x.im) x.im)))
  (*.p16 x.re (real->posit16 0.0))
  (*.p16 x.re (*.p16 (-.p16 x.re x.im) (+.p16 x.im x.re)))
  (*.p16 x.re (neg.p16 (*.p16 (+.p16 x.im x.im) x.im)))
  (*.p16 x.re (real->posit16 0.0))
  (*.p16 x.re (-.p16 (*.p16 (-.p16 x.re x.im) (+.p16 x.im x.re)) (*.p16 (+.p16 x.im x.im) x.im)))
  (*.p16 x.re (-.p16 (*.p16 (-.p16 x.re x.im) (+.p16 x.im x.re)) (*.p16 (+.p16 x.im x.im) x.im)))
  (*.p16 x.re (real->posit16 0.0))
  (*.p16 (*.p16 (-.p16 x.re x.im) x.im) x.re)
  (*.p16 (-.p16 (*.p16 (-.p16 x.re x.im) x.re) (*.p16 (+.p16 x.im x.im) x.im)) x.re)
  (*.p16 (*.p16 x.im (-.p16 x.re x.im)) x.re)
  (*.p16 (-.p16 (*.p16 x.re (-.p16 x.re x.im)) (*.p16 (+.p16 x.im x.im) x.im)) x.re)
  (*.p16 (real->posit16 0.0) x.re)
  (*.p16 (-.p16 (*.p16 (-.p16 x.re x.im) (+.p16 x.im x.re)) (*.p16 (+.p16 x.im x.im) x.im)) x.re)
  (*.p16 (*.p16 (-.p16 x.re x.im) (+.p16 x.im x.re)) x.re)
  (*.p16 (-.p16 (real->posit16 0.0) (*.p16 (+.p16 x.im x.im) x.im)) x.re)
  (*.p16 (-.p16 (*.p16 (-.p16 x.re x.im) (+.p16 x.im x.re)) (*.p16 (+.p16 x.im x.im) x.im)) x.re)
  (*.p16 (real->posit16 0.0) x.re)
  (*.p16 (*.p16 (-.p16 x.re x.im) (+.p16 x.im x.re)) x.re)
  (*.p16 (neg.p16 (*.p16 (+.p16 x.im x.im) x.im)) x.re)
  (*.p16 (real->posit16 0.0) x.re)
  (*.p16 (-.p16 (*.p16 (-.p16 x.re x.im) (+.p16 x.im x.re)) (*.p16 (+.p16 x.im x.im) x.im)) x.re)
  (*.p16 (-.p16 (*.p16 (-.p16 x.re x.im) (+.p16 x.im x.re)) (*.p16 (+.p16 x.im x.im) x.im)) x.re)
  (*.p16 (real->posit16 0.0) x.re)
  (*.p16 x.re (real->posit16 1.0))
  (*.p16 x.re (real->posit16 1.0))
  (*.p16 x.re (-.p16 (*.p16 (-.p16 x.re x.im) (+.p16 x.im x.re)) (*.p16 (+.p16 x.im x.im) x.im)))
  (*.p16 x.re (-.p16 (*.p16 (*.p16 (-.p16 x.re x.im) (+.p16 x.im x.re)) (*.p16 (-.p16 x.re x.im) (+.p16 x.im x.re))) (*.p16 (*.p16 (+.p16 x.im x.im) x.im) (*.p16 (+.p16 x.im x.im) x.im))))
  (*.p16 x.re (-.p16 (*.p16 (-.p16 x.re x.im) (+.p16 x.im x.re)) (*.p16 (+.p16 x.im x.im) x.im)))
  (real->posit16 1.0)
  (posit16->quire16 (*.p16 x.re (-.p16 (*.p16 (-.p16 x.re x.im) (+.p16 x.im x.re)) (*.p16 (+.p16 x.im x.im) x.im))))
  (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 x.re x.im) x.im)
  (*.p16 (-.p16 x.re x.im) x.re)
  (*.p16 x.im (-.p16 x.re x.im))
  (*.p16 x.re (-.p16 x.re x.im))
  (*.p16 (-.p16 x.re x.im) (real->posit16 1.0))
  (*.p16 (-.p16 x.re x.im) (real->posit16 1.0))
  (*.p16 (-.p16 x.re x.im) (+.p16 x.im x.re))
  (*.p16 (-.p16 x.re x.im) (+.p16 x.im x.re))
  (*.p16 (-.p16 x.re x.im) (+.p16 x.im x.re))
  (*.p16 (real->posit16 1.0) (+.p16 x.im x.re))
  (*.p16 (-.p16 x.re x.im) (+.p16 x.im x.re))
  (*.p16 (-.p16 (*.p16 x.re x.re) (*.p16 x.im x.im)) (+.p16 x.im x.re))
  (*.p16 (-.p16 x.re x.im) (+.p16 x.im x.re))
  (real->posit16 1.0)
  (posit16->quire16 (*.p16 (-.p16 x.re x.im) (+.p16 x.im x.re)))
  (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 x.im x.im) x.im)
  (*.p16 (+.p16 x.im x.im) x.im)
  (*.p16 (real->posit16 1.0) x.im)
  (*.p16 (+.p16 x.im x.im) x.im)
  (real->posit16 1.0)
  (posit16->quire16 (*.p16 (+.p16 x.im x.im) x.im))
  (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->posit16 (posit16->quire16 (*.p16 x.re (-.p16 (*.p16 (-.p16 x.re x.im) (+.p16 x.im x.re)) (*.p16 (+.p16 x.im x.im) x.im)))))
  (quire16->posit16 (posit16->quire16 (*.p16 x.re (-.p16 (*.p16 (-.p16 x.re x.im) (+.p16 x.im x.re)) (*.p16 (+.p16 x.im x.im) x.im)))))
  (quire16->posit16 (posit16->quire16 (*.p16 x.re (-.p16 (*.p16 (-.p16 x.re x.im) (+.p16 x.im x.re)) (*.p16 (+.p16 x.im x.im) x.im)))))
  (quire16->posit16 (posit16->quire16 (*.p16 x.re (-.p16 (*.p16 (-.p16 x.re x.im) (+.p16 x.im x.re)) (*.p16 (+.p16 x.im x.im) x.im)))))
44.309 * * [simplify]: iteration 1: (60 enodes)
44.338 * * [simplify]: iteration 2: (118 enodes)
44.401 * * [simplify]: iteration 3: (476 enodes)
45.808 * * [simplify]: Extracting #0: cost 29 inf + 0
45.810 * * [simplify]: Extracting #1: cost 429 inf + 2
45.816 * * [simplify]: Extracting #2: cost 621 inf + 46874
45.853 * * [simplify]: Extracting #3: cost 145 inf + 504194
45.898 * * [simplify]: Extracting #4: cost 19 inf + 635155
45.950 * * [simplify]: Extracting #5: cost 0 inf + 650671
45.999 * [simplify]: Simplified to:
  (*.p16 (-.p16 x.re x.im) (+.p16 x.im x.re))
  (-.p16 (*.p16 (-.p16 x.re x.im) (+.p16 x.im x.re)) (*.p16 (+.p16 x.im x.im) x.im))
  (-.p16 (*.p16 x.re (-.p16 x.re x.im)) (*.p16 (+.p16 x.im x.im) x.im))
  (-.p16 (*.p16 x.re (-.p16 x.re x.im)) (*.p16 (+.p16 x.im x.im) x.im))
  (-.p16 (*.p16 (-.p16 x.re x.im) (+.p16 x.im x.re)) (*.p16 (+.p16 x.im x.im) x.im))
  (neg.p16 (*.p16 (+.p16 x.im x.im) x.im))
  (*.p16 (+.p16 x.im x.im) x.im)
  (-.p16 (*.p16 (-.p16 x.re x.im) (+.p16 x.im x.re)) (*.p16 (+.p16 x.im x.im) x.im))
  (neg.p16 (*.p16 (+.p16 x.im x.im) x.im))
  (-.p16 (*.p16 (*.p16 (-.p16 x.re x.im) (+.p16 x.im x.re)) (*.p16 (-.p16 x.re x.im) (+.p16 x.im x.re))) (*.p16 (*.p16 (+.p16 x.im x.im) x.im) (*.p16 (+.p16 x.im x.im) x.im)))
  (+.p16 (+.p16 (*.p16 (-.p16 x.re x.im) (+.p16 x.im x.re)) (*.p16 x.im x.im)) (*.p16 x.im x.im))
  (real->posit16 1.0)
  (posit16->quire16 (-.p16 (*.p16 (-.p16 x.re x.im) (+.p16 x.im x.re)) (*.p16 (+.p16 x.im x.im) x.im)))
  (quire16-mul-sub (posit16->quire16 (*.p16 (-.p16 x.re x.im) (+.p16 x.im x.re))) (*.p16 (+.p16 x.im x.im) x.im) (real->posit16 1.0))
  (quire16-mul-sub (posit16->quire16 (*.p16 (-.p16 x.re x.im) (+.p16 x.im x.re))) (+.p16 x.im x.im) x.im)
  (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 x.re x.im) (-.p16 x.re x.im))
  (*.p16 x.re (-.p16 (*.p16 x.re (-.p16 x.re x.im)) (*.p16 (+.p16 x.im x.im) x.im)))
  (*.p16 (*.p16 x.re x.im) (-.p16 x.re x.im))
  (*.p16 x.re (-.p16 (*.p16 x.re (-.p16 x.re x.im)) (*.p16 (+.p16 x.im x.im) x.im)))
  (real->posit16 0.0)
  (*.p16 (-.p16 (*.p16 (-.p16 x.re x.im) (+.p16 x.im x.re)) (*.p16 (+.p16 x.im x.im) x.im)) x.re)
  (*.p16 (*.p16 (-.p16 x.re x.im) (+.p16 x.im x.re)) x.re)
  (*.p16 (neg.p16 (*.p16 (+.p16 x.im x.im) x.im)) x.re)
  (*.p16 (-.p16 (*.p16 (-.p16 x.re x.im) (+.p16 x.im x.re)) (*.p16 (+.p16 x.im x.im) x.im)) x.re)
  (real->posit16 0.0)
  (*.p16 (*.p16 (-.p16 x.re x.im) (+.p16 x.im x.re)) x.re)
  (*.p16 (neg.p16 (*.p16 (+.p16 x.im x.im) x.im)) x.re)
  (real->posit16 0.0)
  (*.p16 (-.p16 (*.p16 (-.p16 x.re x.im) (+.p16 x.im x.re)) (*.p16 (+.p16 x.im x.im) x.im)) x.re)
  (*.p16 (-.p16 (*.p16 (-.p16 x.re x.im) (+.p16 x.im x.re)) (*.p16 (+.p16 x.im x.im) x.im)) x.re)
  (real->posit16 0.0)
  (*.p16 (*.p16 x.re x.im) (-.p16 x.re x.im))
  (*.p16 x.re (-.p16 (*.p16 x.re (-.p16 x.re x.im)) (*.p16 (+.p16 x.im x.im) x.im)))
  (*.p16 (*.p16 x.re x.im) (-.p16 x.re x.im))
  (*.p16 x.re (-.p16 (*.p16 x.re (-.p16 x.re x.im)) (*.p16 (+.p16 x.im x.im) x.im)))
  (real->posit16 0.0)
  (*.p16 (-.p16 (*.p16 (-.p16 x.re x.im) (+.p16 x.im x.re)) (*.p16 (+.p16 x.im x.im) x.im)) x.re)
  (*.p16 (*.p16 (-.p16 x.re x.im) (+.p16 x.im x.re)) x.re)
  (*.p16 (neg.p16 (*.p16 (+.p16 x.im x.im) x.im)) x.re)
  (*.p16 (-.p16 (*.p16 (-.p16 x.re x.im) (+.p16 x.im x.re)) (*.p16 (+.p16 x.im x.im) x.im)) x.re)
  (real->posit16 0.0)
  (*.p16 (*.p16 (-.p16 x.re x.im) (+.p16 x.im x.re)) x.re)
  (*.p16 (neg.p16 (*.p16 (+.p16 x.im x.im) x.im)) x.re)
  (real->posit16 0.0)
  (*.p16 (-.p16 (*.p16 (-.p16 x.re x.im) (+.p16 x.im x.re)) (*.p16 (+.p16 x.im x.im) x.im)) x.re)
  (*.p16 (-.p16 (*.p16 (-.p16 x.re x.im) (+.p16 x.im x.re)) (*.p16 (+.p16 x.im x.im) x.im)) x.re)
  (real->posit16 0.0)
  x.re
  x.re
  (*.p16 (-.p16 (*.p16 (-.p16 x.re x.im) (+.p16 x.im x.re)) (*.p16 (+.p16 x.im x.im) x.im)) x.re)
  (*.p16 (-.p16 (*.p16 (*.p16 (-.p16 x.re x.im) (+.p16 x.im x.re)) (*.p16 (-.p16 x.re x.im) (+.p16 x.im x.re))) (*.p16 (*.p16 (+.p16 x.im x.im) x.im) (*.p16 (+.p16 x.im x.im) x.im))) x.re)
  (*.p16 (-.p16 (*.p16 (-.p16 x.re x.im) (+.p16 x.im x.re)) (*.p16 (+.p16 x.im x.im) x.im)) x.re)
  (real->posit16 1.0)
  (posit16->quire16 (*.p16 (-.p16 (*.p16 (-.p16 x.re x.im) (+.p16 x.im x.re)) (*.p16 (+.p16 x.im x.im) x.im)) x.re))
  (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 x.re x.im) x.im)
  (*.p16 x.re (-.p16 x.re x.im))
  (*.p16 (-.p16 x.re x.im) x.im)
  (*.p16 x.re (-.p16 x.re x.im))
  (-.p16 x.re x.im)
  (-.p16 x.re x.im)
  (*.p16 (-.p16 x.re x.im) (+.p16 x.im x.re))
  (*.p16 (-.p16 x.re x.im) (+.p16 x.im x.re))
  (*.p16 (-.p16 x.re x.im) (+.p16 x.im x.re))
  (+.p16 x.im x.re)
  (*.p16 (-.p16 x.re x.im) (+.p16 x.im x.re))
  (*.p16 (*.p16 (-.p16 x.re x.im) (+.p16 x.im x.re)) (+.p16 x.im x.re))
  (*.p16 (-.p16 x.re x.im) (+.p16 x.im x.re))
  (real->posit16 1.0)
  (posit16->quire16 (*.p16 (-.p16 x.re x.im) (+.p16 x.im x.re)))
  (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 x.im x.im) x.im)
  (*.p16 (+.p16 x.im x.im) x.im)
  x.im
  (*.p16 (+.p16 x.im x.im) x.im)
  (real->posit16 1.0)
  (posit16->quire16 (*.p16 (+.p16 x.im x.im) x.im))
  (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->posit16 (posit16->quire16 (*.p16 (-.p16 (*.p16 (-.p16 x.re x.im) (+.p16 x.im x.re)) (*.p16 (+.p16 x.im x.im) x.im)) x.re)))
  (quire16->posit16 (posit16->quire16 (*.p16 (-.p16 (*.p16 (-.p16 x.re x.im) (+.p16 x.im x.re)) (*.p16 (+.p16 x.im x.im) x.im)) x.re)))
  (quire16->posit16 (posit16->quire16 (*.p16 (-.p16 (*.p16 (-.p16 x.re x.im) (+.p16 x.im x.re)) (*.p16 (+.p16 x.im x.im) x.im)) x.re)))
  (quire16->posit16 (posit16->quire16 (*.p16 (-.p16 (*.p16 (-.p16 x.re x.im) (+.p16 x.im x.re)) (*.p16 (+.p16 x.im x.im) x.im)) x.re)))
46.010 * * * [progress]: adding candidates to table
49.302 * * [progress]: iteration 3 / 4
49.302 * * * [progress]: picking best candidate
49.416 * * * * [pick]: Picked  #<alt (λ (x.re x.im) (quire16->posit16 (posit16->quire16 (*.p16 x.re (quire16->posit16 (quire16-mul-sub (posit16->quire16 (*.p16 (-.p16 x.re x.im) (+.p16 x.im x.re))) (+.p16 x.im x.im) x.im))))))>
49.416 * * * [progress]: localizing error
49.646 * * * [progress]: generating rewritten candidates
49.646 * * * * [progress]: [ 1 / 3 ] rewriting at (2 1 1 2 1)
49.647 * * * * [progress]: [ 2 / 3 ] rewriting at (2 1 1)
49.651 * * * * [progress]: [ 3 / 3 ] rewriting at (2 1 1 2 1 1 1)
49.655 * * * [progress]: generating series expansions
49.655 * * * * [progress]: [ 1 / 3 ] generating series at (2 1 1 2 1)
49.656 * * * * [progress]: [ 2 / 3 ] generating series at (2 1 1)
49.656 * * * * [progress]: [ 3 / 3 ] generating series at (2 1 1 2 1 1 1)
49.656 * * * [progress]: simplifying candidates
49.656 * * * * [progress]: [ 1 / 40 ] simplifiying candidate #<alt (λ (x.re x.im) (quire16->posit16 (posit16->quire16 (+.p16 (*.p16 x.re (real->posit16 0.0)) (*.p16 x.re (quire16->posit16 (quire16-mul-sub (posit16->quire16 (*.p16 (-.p16 x.re x.im) (+.p16 x.im x.re))) (+.p16 x.im x.im) x.im)))))))>
49.656 * * * * [progress]: [ 2 / 40 ] simplifiying candidate #<alt (λ (x.re x.im) (quire16->posit16 (posit16->quire16 (+.p16 (*.p16 x.re (quire16->posit16 (quire16-mul-sub (posit16->quire16 (*.p16 (-.p16 x.re x.im) (+.p16 x.im x.re))) (+.p16 x.im x.im) x.im))) (*.p16 x.re (real->posit16 0.0))))))>
49.656 * * * * [progress]: [ 3 / 40 ] simplifiying candidate #<alt (λ (x.re x.im) (quire16->posit16 (posit16->quire16 (+.p16 (*.p16 (real->posit16 0.0) x.re) (*.p16 (quire16->posit16 (quire16-mul-sub (posit16->quire16 (*.p16 (-.p16 x.re x.im) (+.p16 x.im x.re))) (+.p16 x.im x.im) x.im)) x.re)))))>
49.656 * * * * [progress]: [ 4 / 40 ] simplifiying candidate #<alt (λ (x.re x.im) (quire16->posit16 (posit16->quire16 (+.p16 (*.p16 (quire16->posit16 (quire16-mul-sub (posit16->quire16 (*.p16 (-.p16 x.re x.im) (+.p16 x.im x.re))) (+.p16 x.im x.im) x.im)) x.re) (*.p16 (real->posit16 0.0) x.re)))))>
49.656 * * * * [progress]: [ 5 / 40 ] simplifiying candidate #<alt (λ (x.re x.im) (quire16->posit16 (posit16->quire16 (*.p16 (*.p16 x.re (real->posit16 1.0)) (quire16->posit16 (quire16-mul-sub (posit16->quire16 (*.p16 (-.p16 x.re x.im) (+.p16 x.im x.re))) (+.p16 x.im x.im) x.im))))))>
49.656 * * * * [progress]: [ 6 / 40 ] simplifiying candidate #<alt (λ (x.re x.im) (quire16->posit16 (posit16->quire16 (*.p16 (*.p16 x.re (real->posit16 1.0)) (quire16->posit16 (quire16-mul-sub (posit16->quire16 (*.p16 (-.p16 x.re x.im) (+.p16 x.im x.re))) (+.p16 x.im x.im) x.im))))))>
49.656 * * * * [progress]: [ 7 / 40 ] simplifiying candidate #<alt (λ (x.re x.im) (quire16->posit16 (posit16->quire16 (*.p16 (*.p16 x.re (quire16->posit16 (quire16-mul-sub (posit16->quire16 (*.p16 (-.p16 x.re x.im) (+.p16 x.im x.re))) (+.p16 x.im x.im) x.im))) (real->posit16 1.0)))))>
49.656 * * * * [progress]: [ 8 / 40 ] simplifiying candidate #<alt (λ (x.re x.im) (quire16->posit16 (posit16->quire16 (/.p16 (*.p16 x.re (quire16->posit16 (quire16-mul-sub (posit16->quire16 (*.p16 (-.p16 x.re x.im) (+.p16 x.im x.re))) (+.p16 x.im x.im) x.im))) (real->posit16 1.0)))))>
49.656 * * * * [progress]: [ 9 / 40 ] simplifiying candidate #<alt (λ (x.re x.im) (quire16->posit16 (posit16->quire16 (*.p16 (real->posit16 1.0) (*.p16 x.re (quire16->posit16 (quire16-mul-sub (posit16->quire16 (*.p16 (-.p16 x.re x.im) (+.p16 x.im x.re))) (+.p16 x.im x.im) x.im)))))))>
49.656 * * * * [progress]: [ 10 / 40 ] simplifiying candidate #<alt (λ (x.re x.im) (quire16->posit16 (posit16->quire16 (quire16->posit16 (posit16->quire16 (*.p16 x.re (quire16->posit16 (quire16-mul-sub (posit16->quire16 (*.p16 (-.p16 x.re x.im) (+.p16 x.im x.re))) (+.p16 x.im x.im) x.im))))))))>
49.656 * * * * [progress]: [ 11 / 40 ] simplifiying candidate #<alt (λ (x.re x.im) (quire16->posit16 (posit16->quire16 (+.p16 (real->posit16 0.0) (*.p16 x.re (quire16->posit16 (quire16-mul-sub (posit16->quire16 (*.p16 (-.p16 x.re x.im) (+.p16 x.im x.re))) (+.p16 x.im x.im) x.im)))))))>
49.656 * * * * [progress]: [ 12 / 40 ] simplifiying candidate #<alt (λ (x.re x.im) (quire16->posit16 (posit16->quire16 (+.p16 (*.p16 x.re (quire16->posit16 (quire16-mul-sub (posit16->quire16 (*.p16 (-.p16 x.re x.im) (+.p16 x.im x.re))) (+.p16 x.im x.im) x.im))) (real->posit16 0.0)))))>
49.656 * * * * [progress]: [ 13 / 40 ] simplifiying candidate #<alt (λ (x.re x.im) (quire16->posit16 (posit16->quire16 (-.p16 (*.p16 x.re (quire16->posit16 (quire16-mul-sub (posit16->quire16 (*.p16 (-.p16 x.re x.im) (+.p16 x.im x.re))) (+.p16 x.im x.im) x.im))) (real->posit16 0.0)))))>
49.656 * * * * [progress]: [ 14 / 40 ] simplifiying candidate #<alt (λ (x.re x.im) (quire16->posit16 (posit16->quire16 (*.p16 (real->posit16 1.0) (*.p16 x.re (quire16->posit16 (quire16-mul-sub (posit16->quire16 (*.p16 (-.p16 x.re x.im) (+.p16 x.im x.re))) (+.p16 x.im x.im) x.im)))))))>
49.656 * * * * [progress]: [ 15 / 40 ] simplifiying candidate #<alt (λ (x.re x.im) (quire16->posit16 (posit16->quire16 (*.p16 (*.p16 x.re (quire16->posit16 (quire16-mul-sub (posit16->quire16 (*.p16 (-.p16 x.re x.im) (+.p16 x.im x.re))) (+.p16 x.im x.im) x.im))) (real->posit16 1.0)))))>
49.656 * * * * [progress]: [ 16 / 40 ] simplifiying candidate #<alt (λ (x.re x.im) (quire16->posit16 (posit16->quire16 (/.p16 (*.p16 x.re (quire16->posit16 (quire16-mul-sub (posit16->quire16 (*.p16 (-.p16 x.re x.im) (+.p16 x.im x.re))) (+.p16 x.im x.im) x.im))) (real->posit16 1.0)))))>
49.656 * * * * [progress]: [ 17 / 40 ] simplifiying candidate #<alt (λ (x.re x.im) (quire16->posit16 (posit16->quire16 (*.p16 (quire16->posit16 (quire16-mul-sub (posit16->quire16 (*.p16 (-.p16 x.re x.im) (+.p16 x.im x.re))) (+.p16 x.im x.im) x.im)) x.re))))>
49.656 * * * * [progress]: [ 18 / 40 ] simplifiying candidate #<alt (λ (x.re x.im) (quire16->posit16 (posit16->quire16 (*.p16 x.re (quire16->posit16 (quire16-mul-sub (posit16->quire16 (+.p16 (*.p16 (-.p16 x.re x.im) x.im) (*.p16 (-.p16 x.re x.im) x.re))) (+.p16 x.im x.im) x.im))))))>
49.656 * * * * [progress]: [ 19 / 40 ] simplifiying candidate #<alt (λ (x.re x.im) (quire16->posit16 (posit16->quire16 (*.p16 x.re (quire16->posit16 (quire16-mul-sub (posit16->quire16 (+.p16 (*.p16 x.im (-.p16 x.re x.im)) (*.p16 x.re (-.p16 x.re x.im)))) (+.p16 x.im x.im) x.im))))))>
49.656 * * * * [progress]: [ 20 / 40 ] simplifiying candidate #<alt (λ (x.re x.im) (quire16->posit16 (posit16->quire16 (*.p16 x.re (quire16->posit16 (quire16-mul-sub (posit16->quire16 (*.p16 (*.p16 (-.p16 x.re x.im) (real->posit16 1.0)) (+.p16 x.im x.re))) (+.p16 x.im x.im) x.im))))))>
49.656 * * * * [progress]: [ 21 / 40 ] simplifiying candidate #<alt (λ (x.re x.im) (quire16->posit16 (posit16->quire16 (*.p16 x.re (quire16->posit16 (quire16-mul-sub (posit16->quire16 (*.p16 (*.p16 (-.p16 x.re x.im) (real->posit16 1.0)) (+.p16 x.im x.re))) (+.p16 x.im x.im) x.im))))))>
49.656 * * * * [progress]: [ 22 / 40 ] simplifiying candidate #<alt (λ (x.re x.im) (quire16->posit16 (posit16->quire16 (*.p16 x.re (quire16->posit16 (quire16-mul-sub (posit16->quire16 (*.p16 (*.p16 (-.p16 x.re x.im) (+.p16 x.im x.re)) (real->posit16 1.0))) (+.p16 x.im x.im) x.im))))))>
49.656 * * * * [progress]: [ 23 / 40 ] simplifiying candidate #<alt (λ (x.re x.im) (quire16->posit16 (posit16->quire16 (*.p16 x.re (quire16->posit16 (quire16-mul-sub (posit16->quire16 (*.p16 (real->posit16 1.0) (*.p16 (-.p16 x.re x.im) (+.p16 x.im x.re)))) (+.p16 x.im x.im) x.im))))))>
49.657 * * * * [progress]: [ 24 / 40 ] simplifiying candidate #<alt (λ (x.re x.im) (quire16->posit16 (posit16->quire16 (*.p16 x.re (quire16->posit16 (quire16-mul-sub (posit16->quire16 (*.p16 (real->posit16 1.0) (*.p16 (-.p16 x.re x.im) (+.p16 x.im x.re)))) (+.p16 x.im x.im) x.im))))))>
49.657 * * * * [progress]: [ 25 / 40 ] simplifiying candidate #<alt (λ (x.re x.im) (quire16->posit16 (posit16->quire16 (*.p16 x.re (quire16->posit16 (quire16-mul-sub (posit16->quire16 (*.p16 (-.p16 x.re x.im) (*.p16 (real->posit16 1.0) (+.p16 x.im x.re)))) (+.p16 x.im x.im) x.im))))))>
49.657 * * * * [progress]: [ 26 / 40 ] simplifiying candidate #<alt (λ (x.re x.im) (quire16->posit16 (posit16->quire16 (*.p16 x.re (quire16->posit16 (quire16-mul-sub (posit16->quire16 (/.p16 (*.p16 (-.p16 x.re x.im) (+.p16 x.im x.re)) (real->posit16 1.0))) (+.p16 x.im x.im) x.im))))))>
49.657 * * * * [progress]: [ 27 / 40 ] simplifiying candidate #<alt (λ (x.re x.im) (quire16->posit16 (posit16->quire16 (*.p16 x.re (quire16->posit16 (quire16-mul-sub (posit16->quire16 (/.p16 (*.p16 (-.p16 (*.p16 x.re x.re) (*.p16 x.im x.im)) (+.p16 x.im x.re)) (+.p16 x.re x.im))) (+.p16 x.im x.im) x.im))))))>
49.657 * * * * [progress]: [ 28 / 40 ] simplifiying candidate #<alt (λ (x.re x.im) (quire16->posit16 (posit16->quire16 (*.p16 x.re (quire16->posit16 (quire16-mul-sub (posit16->quire16 (/.p16 (*.p16 (-.p16 x.re x.im) (+.p16 x.im x.re)) (real->posit16 1.0))) (+.p16 x.im x.im) x.im))))))>
49.657 * * * * [progress]: [ 29 / 40 ] simplifiying candidate #<alt (λ (x.re x.im) (quire16->posit16 (posit16->quire16 (*.p16 x.re (quire16->posit16 (quire16-mul-sub (posit16->quire16 (*.p16 (real->posit16 1.0) (*.p16 (-.p16 x.re x.im) (+.p16 x.im x.re)))) (+.p16 x.im x.im) x.im))))))>
49.657 * * * * [progress]: [ 30 / 40 ] simplifiying candidate #<alt (λ (x.re x.im) (quire16->posit16 (posit16->quire16 (*.p16 x.re (quire16->posit16 (quire16-mul-sub (posit16->quire16 (quire16->posit16 (posit16->quire16 (*.p16 (-.p16 x.re x.im) (+.p16 x.im x.re))))) (+.p16 x.im x.im) x.im))))))>
49.657 * * * * [progress]: [ 31 / 40 ] simplifiying candidate #<alt (λ (x.re x.im) (quire16->posit16 (posit16->quire16 (*.p16 x.re (quire16->posit16 (quire16-mul-sub (posit16->quire16 (+.p16 (real->posit16 0.0) (*.p16 (-.p16 x.re x.im) (+.p16 x.im x.re)))) (+.p16 x.im x.im) x.im))))))>
49.657 * * * * [progress]: [ 32 / 40 ] simplifiying candidate #<alt (λ (x.re x.im) (quire16->posit16 (posit16->quire16 (*.p16 x.re (quire16->posit16 (quire16-mul-sub (posit16->quire16 (+.p16 (*.p16 (-.p16 x.re x.im) (+.p16 x.im x.re)) (real->posit16 0.0))) (+.p16 x.im x.im) x.im))))))>
49.657 * * * * [progress]: [ 33 / 40 ] simplifiying candidate #<alt (λ (x.re x.im) (quire16->posit16 (posit16->quire16 (*.p16 x.re (quire16->posit16 (quire16-mul-sub (posit16->quire16 (-.p16 (*.p16 (-.p16 x.re x.im) (+.p16 x.im x.re)) (real->posit16 0.0))) (+.p16 x.im x.im) x.im))))))>
49.657 * * * * [progress]: [ 34 / 40 ] simplifiying candidate #<alt (λ (x.re x.im) (quire16->posit16 (posit16->quire16 (*.p16 x.re (quire16->posit16 (quire16-mul-sub (posit16->quire16 (*.p16 (real->posit16 1.0) (*.p16 (-.p16 x.re x.im) (+.p16 x.im x.re)))) (+.p16 x.im x.im) x.im))))))>
49.657 * * * * [progress]: [ 35 / 40 ] simplifiying candidate #<alt (λ (x.re x.im) (quire16->posit16 (posit16->quire16 (*.p16 x.re (quire16->posit16 (quire16-mul-sub (posit16->quire16 (*.p16 (*.p16 (-.p16 x.re x.im) (+.p16 x.im x.re)) (real->posit16 1.0))) (+.p16 x.im x.im) x.im))))))>
49.657 * * * * [progress]: [ 36 / 40 ] simplifiying candidate #<alt (λ (x.re x.im) (quire16->posit16 (posit16->quire16 (*.p16 x.re (quire16->posit16 (quire16-mul-sub (posit16->quire16 (/.p16 (*.p16 (-.p16 x.re x.im) (+.p16 x.im x.re)) (real->posit16 1.0))) (+.p16 x.im x.im) x.im))))))>
49.657 * * * * [progress]: [ 37 / 40 ] simplifiying candidate #<alt (λ (x.re x.im) (quire16->posit16 (posit16->quire16 (*.p16 x.re (quire16->posit16 (quire16-mul-sub (posit16->quire16 (*.p16 (+.p16 x.im x.re) (-.p16 x.re x.im))) (+.p16 x.im x.im) x.im))))))>
49.657 * * * * [progress]: [ 38 / 40 ] simplifiying candidate #<alt (λ (x.re x.im) (quire16->posit16 (posit16->quire16 (*.p16 x.re (quire16->posit16 (quire16-mul-sub (posit16->quire16 (*.p16 (-.p16 x.re x.im) (+.p16 x.im x.re))) (+.p16 x.im x.im) x.im))))))>
49.657 * * * * [progress]: [ 39 / 40 ] simplifiying candidate #<alt (λ (x.re x.im) (quire16->posit16 (posit16->quire16 (*.p16 x.re (quire16->posit16 (quire16-mul-sub (posit16->quire16 (*.p16 (-.p16 x.re x.im) (+.p16 x.im x.re))) (+.p16 x.im x.im) x.im))))))>
49.657 * * * * [progress]: [ 40 / 40 ] simplifiying candidate #<alt (λ (x.re x.im) (quire16->posit16 (posit16->quire16 (*.p16 x.re (quire16->posit16 (quire16-mul-sub (posit16->quire16 (*.p16 (-.p16 x.re x.im) (+.p16 x.im x.re))) (+.p16 x.im x.im) x.im))))))>
49.658 * [simplify]: Simplifying:
  (*.p16 x.re (real->posit16 0.0))
  (*.p16 x.re (quire16->posit16 (quire16-mul-sub (posit16->quire16 (*.p16 (-.p16 x.re x.im) (+.p16 x.im x.re))) (+.p16 x.im x.im) x.im)))
  (*.p16 x.re (quire16->posit16 (quire16-mul-sub (posit16->quire16 (*.p16 (-.p16 x.re x.im) (+.p16 x.im x.re))) (+.p16 x.im x.im) x.im)))
  (*.p16 x.re (real->posit16 0.0))
  (*.p16 (real->posit16 0.0) x.re)
  (*.p16 (quire16->posit16 (quire16-mul-sub (posit16->quire16 (*.p16 (-.p16 x.re x.im) (+.p16 x.im x.re))) (+.p16 x.im x.im) x.im)) x.re)
  (*.p16 (quire16->posit16 (quire16-mul-sub (posit16->quire16 (*.p16 (-.p16 x.re x.im) (+.p16 x.im x.re))) (+.p16 x.im x.im) x.im)) x.re)
  (*.p16 (real->posit16 0.0) x.re)
  (*.p16 x.re (real->posit16 1.0))
  (*.p16 x.re (real->posit16 1.0))
  (*.p16 x.re (quire16->posit16 (quire16-mul-sub (posit16->quire16 (*.p16 (-.p16 x.re x.im) (+.p16 x.im x.re))) (+.p16 x.im x.im) x.im)))
  (*.p16 x.re (quire16->posit16 (quire16-mul-sub (posit16->quire16 (*.p16 (-.p16 x.re x.im) (+.p16 x.im x.re))) (+.p16 x.im x.im) x.im)))
  (real->posit16 1.0)
  (posit16->quire16 (*.p16 x.re (quire16->posit16 (quire16-mul-sub (posit16->quire16 (*.p16 (-.p16 x.re x.im) (+.p16 x.im x.re))) (+.p16 x.im x.im) x.im))))
  (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 x.re x.im) x.im)
  (*.p16 (-.p16 x.re x.im) x.re)
  (*.p16 x.im (-.p16 x.re x.im))
  (*.p16 x.re (-.p16 x.re x.im))
  (*.p16 (-.p16 x.re x.im) (real->posit16 1.0))
  (*.p16 (-.p16 x.re x.im) (real->posit16 1.0))
  (*.p16 (-.p16 x.re x.im) (+.p16 x.im x.re))
  (*.p16 (-.p16 x.re x.im) (+.p16 x.im x.re))
  (*.p16 (-.p16 x.re x.im) (+.p16 x.im x.re))
  (*.p16 (real->posit16 1.0) (+.p16 x.im x.re))
  (*.p16 (-.p16 x.re x.im) (+.p16 x.im x.re))
  (*.p16 (-.p16 (*.p16 x.re x.re) (*.p16 x.im x.im)) (+.p16 x.im x.re))
  (*.p16 (-.p16 x.re x.im) (+.p16 x.im x.re))
  (real->posit16 1.0)
  (posit16->quire16 (*.p16 (-.p16 x.re x.im) (+.p16 x.im x.re)))
  (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 (-.p16 x.re x.im) (+.p16 x.im x.re))) (+.p16 x.im x.im) x.im)
  (quire16-mul-sub (posit16->quire16 (*.p16 (-.p16 x.re x.im) (+.p16 x.im x.re))) (+.p16 x.im x.im) x.im)
  (quire16-mul-sub (posit16->quire16 (*.p16 (-.p16 x.re x.im) (+.p16 x.im x.re))) (+.p16 x.im x.im) x.im)
49.658 * * [simplify]: iteration 1: (29 enodes)
49.665 * * [simplify]: iteration 2: (53 enodes)
49.681 * * [simplify]: iteration 3: (148 enodes)
49.778 * * [simplify]: iteration 4: (562 enodes)
50.649 * * [simplify]: Extracting #0: cost 13 inf + 0
50.649 * * [simplify]: Extracting #1: cost 233 inf + 1
50.654 * * [simplify]: Extracting #2: cost 528 inf + 21344
50.676 * * [simplify]: Extracting #3: cost 132 inf + 228589
50.702 * * [simplify]: Extracting #4: cost 60 inf + 291526
50.734 * * [simplify]: Extracting #5: cost 2 inf + 365768
50.765 * * [simplify]: Extracting #6: cost 0 inf + 368574
50.799 * [simplify]: Simplified to:
  (real->posit16 0.0)
  (*.p16 x.re (quire16->posit16 (quire16-mul-sub (posit16->quire16 (*.p16 (-.p16 x.re x.im) (+.p16 x.im x.re))) (+.p16 x.im x.im) x.im)))
  (*.p16 x.re (quire16->posit16 (quire16-mul-sub (posit16->quire16 (*.p16 (-.p16 x.re x.im) (+.p16 x.im x.re))) (+.p16 x.im x.im) x.im)))
  (real->posit16 0.0)
  (real->posit16 0.0)
  (*.p16 x.re (quire16->posit16 (quire16-mul-sub (posit16->quire16 (*.p16 (-.p16 x.re x.im) (+.p16 x.im x.re))) (+.p16 x.im x.im) x.im)))
  (*.p16 x.re (quire16->posit16 (quire16-mul-sub (posit16->quire16 (*.p16 (-.p16 x.re x.im) (+.p16 x.im x.re))) (+.p16 x.im x.im) x.im)))
  (real->posit16 0.0)
  x.re
  x.re
  (*.p16 x.re (quire16->posit16 (quire16-mul-sub (posit16->quire16 (*.p16 (-.p16 x.re x.im) (+.p16 x.im x.re))) (+.p16 x.im x.im) x.im)))
  (*.p16 x.re (quire16->posit16 (quire16-mul-sub (posit16->quire16 (*.p16 (-.p16 x.re x.im) (+.p16 x.im x.re))) (+.p16 x.im x.im) x.im)))
  (real->posit16 1.0)
  (posit16->quire16 (*.p16 x.re (quire16->posit16 (quire16-mul-sub (posit16->quire16 (*.p16 (-.p16 x.re x.im) (+.p16 x.im x.re))) (+.p16 x.im x.im) x.im))))
  (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 x.im (-.p16 x.re x.im))
  (*.p16 x.re (-.p16 x.re x.im))
  (*.p16 x.im (-.p16 x.re x.im))
  (*.p16 x.re (-.p16 x.re x.im))
  (-.p16 x.re x.im)
  (-.p16 x.re x.im)
  (*.p16 (-.p16 x.re x.im) (+.p16 x.im x.re))
  (*.p16 (-.p16 x.re x.im) (+.p16 x.im x.re))
  (*.p16 (-.p16 x.re x.im) (+.p16 x.im x.re))
  (+.p16 x.re x.im)
  (*.p16 (-.p16 x.re x.im) (+.p16 x.im x.re))
  (*.p16 (*.p16 (-.p16 x.re x.im) (+.p16 x.im x.re)) (+.p16 x.im x.re))
  (*.p16 (-.p16 x.re x.im) (+.p16 x.im x.re))
  (real->posit16 1.0)
  (posit16->quire16 (*.p16 (-.p16 x.re x.im) (+.p16 x.im x.re)))
  (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 (-.p16 x.re x.im) (+.p16 x.im x.re))) (+.p16 x.im x.im) x.im)
  (quire16-mul-sub (posit16->quire16 (*.p16 (-.p16 x.re x.im) (+.p16 x.im x.re))) (+.p16 x.im x.im) x.im)
  (quire16-mul-sub (posit16->quire16 (*.p16 (-.p16 x.re x.im) (+.p16 x.im x.re))) (+.p16 x.im x.im) x.im)
50.803 * * * [progress]: adding candidates to table
52.671 * * [progress]: iteration 4 / 4
52.671 * * * [progress]: picking best candidate
52.760 * * * * [pick]: Picked  #<alt (λ (x.re x.im) (-.p16 (*.p16 (+.p16 x.re x.im) (*.p16 (-.p16 x.re x.im) x.re)) (*.p16 (+.p16 (*.p16 x.re x.im) (*.p16 x.im x.re)) x.im)))>
52.760 * * * [progress]: localizing error
53.010 * * * [progress]: generating rewritten candidates
53.010 * * * * [progress]: [ 1 / 4 ] rewriting at (2)
53.018 * * * * [progress]: [ 2 / 4 ] rewriting at (2 2 1)
53.024 * * * * [progress]: [ 3 / 4 ] rewriting at (2 1)
53.036 * * * * [progress]: [ 4 / 4 ] rewriting at (2 2)
53.042 * * * [progress]: generating series expansions
53.042 * * * * [progress]: [ 1 / 4 ] generating series at (2)
53.042 * * * * [progress]: [ 2 / 4 ] generating series at (2 2 1)
53.042 * * * * [progress]: [ 3 / 4 ] generating series at (2 1)
53.042 * * * * [progress]: [ 4 / 4 ] generating series at (2 2)
53.042 * * * [progress]: simplifying candidates
53.042 * * * * [progress]: [ 1 / 77 ] simplifiying candidate #<alt (λ (x.re x.im) (-.p16 (-.p16 (*.p16 (+.p16 x.re x.im) (*.p16 (-.p16 x.re x.im) x.re)) (real->posit16 0.0)) (*.p16 (+.p16 (*.p16 x.re x.im) (*.p16 x.im x.re)) x.im)))>
53.042 * * * * [progress]: [ 2 / 77 ] simplifiying candidate #<alt (λ (x.re x.im) (-.p16 (-.p16 (*.p16 (+.p16 x.re x.im) (*.p16 (-.p16 x.re x.im) x.re)) (*.p16 (+.p16 (*.p16 x.re x.im) (*.p16 x.im x.re)) x.im)) (real->posit16 0.0)))>
53.043 * * * * [progress]: [ 3 / 77 ] simplifiying candidate #<alt (λ (x.re x.im) (+.p16 (*.p16 (+.p16 x.re x.im) (real->posit16 0.0)) (-.p16 (*.p16 (+.p16 x.re x.im) (*.p16 (-.p16 x.re x.im) x.re)) (*.p16 (+.p16 (*.p16 x.re x.im) (*.p16 x.im x.re)) x.im))))>
53.043 * * * * [progress]: [ 4 / 77 ] simplifiying candidate #<alt (λ (x.re x.im) (+.p16 (*.p16 (+.p16 x.re x.im) (*.p16 (-.p16 x.re x.im) x.re)) (-.p16 (*.p16 (+.p16 x.re x.im) (real->posit16 0.0)) (*.p16 (+.p16 (*.p16 x.re x.im) (*.p16 x.im x.re)) x.im))))>
53.043 * * * * [progress]: [ 5 / 77 ] simplifiying candidate #<alt (λ (x.re x.im) (+.p16 (*.p16 (real->posit16 0.0) (+.p16 x.re x.im)) (-.p16 (*.p16 (*.p16 (-.p16 x.re x.im) x.re) (+.p16 x.re x.im)) (*.p16 (+.p16 (*.p16 x.re x.im) (*.p16 x.im x.re)) x.im))))>
53.043 * * * * [progress]: [ 6 / 77 ] simplifiying candidate #<alt (λ (x.re x.im) (+.p16 (*.p16 (*.p16 (-.p16 x.re x.im) x.re) (+.p16 x.re x.im)) (-.p16 (*.p16 (real->posit16 0.0) (+.p16 x.re x.im)) (*.p16 (+.p16 (*.p16 x.re x.im) (*.p16 x.im x.re)) x.im))))>
53.043 * * * * [progress]: [ 7 / 77 ] simplifiying candidate #<alt (λ (x.re x.im) (+.p16 (real->posit16 0.0) (-.p16 (*.p16 (+.p16 x.re x.im) (*.p16 (-.p16 x.re x.im) x.re)) (*.p16 (+.p16 (*.p16 x.re x.im) (*.p16 x.im x.re)) x.im))))>
53.043 * * * * [progress]: [ 8 / 77 ] simplifiying candidate #<alt (λ (x.re x.im) (+.p16 (*.p16 (+.p16 x.re x.im) (*.p16 (-.p16 x.re x.im) x.re)) (-.p16 (real->posit16 0.0) (*.p16 (+.p16 (*.p16 x.re x.im) (*.p16 x.im x.re)) x.im))))>
53.043 * * * * [progress]: [ 9 / 77 ] simplifiying candidate #<alt (λ (x.re x.im) (-.p16 (*.p16 (+.p16 x.re x.im) (*.p16 (-.p16 x.re x.im) x.re)) (+.p16 (real->posit16 0.0) (*.p16 (+.p16 (*.p16 x.re x.im) (*.p16 x.im x.re)) x.im))))>
53.043 * * * * [progress]: [ 10 / 77 ] simplifiying candidate #<alt (λ (x.re x.im) (+.p16 (-.p16 (*.p16 (+.p16 x.re x.im) (*.p16 (-.p16 x.re x.im) x.re)) (*.p16 (+.p16 (*.p16 x.re x.im) (*.p16 x.im x.re)) x.im)) (real->posit16 0.0)))>
53.043 * * * * [progress]: [ 11 / 77 ] simplifiying candidate #<alt (λ (x.re x.im) (+.p16 (*.p16 (+.p16 x.re x.im) (*.p16 (-.p16 x.re x.im) x.re)) (neg.p16 (*.p16 (+.p16 (*.p16 x.re x.im) (*.p16 x.im x.re)) x.im))))>
53.043 * * * * [progress]: [ 12 / 77 ] simplifiying candidate #<alt (λ (x.re x.im) (/.p16 (-.p16 (*.p16 (*.p16 (+.p16 x.re x.im) (*.p16 (-.p16 x.re x.im) x.re)) (*.p16 (+.p16 x.re x.im) (*.p16 (-.p16 x.re x.im) x.re))) (*.p16 (*.p16 (+.p16 (*.p16 x.re x.im) (*.p16 x.im x.re)) x.im) (*.p16 (+.p16 (*.p16 x.re x.im) (*.p16 x.im x.re)) x.im))) (+.p16 (*.p16 (+.p16 x.re x.im) (*.p16 (-.p16 x.re x.im) x.re)) (*.p16 (+.p16 (*.p16 x.re x.im) (*.p16 x.im x.re)) x.im))))>
53.043 * * * * [progress]: [ 13 / 77 ] simplifiying candidate #<alt (λ (x.re x.im) (*.p16 (real->posit16 1.0) (-.p16 (*.p16 (+.p16 x.re x.im) (*.p16 (-.p16 x.re x.im) x.re)) (*.p16 (+.p16 (*.p16 x.re x.im) (*.p16 x.im x.re)) x.im))))>
53.043 * * * * [progress]: [ 14 / 77 ] simplifiying candidate #<alt (λ (x.re x.im) (quire16->posit16 (posit16->quire16 (-.p16 (*.p16 (+.p16 x.re x.im) (*.p16 (-.p16 x.re x.im) x.re)) (*.p16 (+.p16 (*.p16 x.re x.im) (*.p16 x.im x.re)) x.im)))))>
53.043 * * * * [progress]: [ 15 / 77 ] simplifiying candidate #<alt (λ (x.re x.im) (quire16->posit16 (quire16-mul-sub (posit16->quire16 (*.p16 (+.p16 x.re x.im) (*.p16 (-.p16 x.re x.im) x.re))) (*.p16 (+.p16 (*.p16 x.re x.im) (*.p16 x.im x.re)) x.im) (real->posit16 1.0))))>
53.044 * * * * [progress]: [ 16 / 77 ] simplifiying candidate #<alt (λ (x.re x.im) (quire16->posit16 (quire16-mul-sub (posit16->quire16 (*.p16 (+.p16 x.re x.im) (*.p16 (-.p16 x.re x.im) x.re))) (+.p16 (*.p16 x.re x.im) (*.p16 x.im x.re)) x.im)))>
53.044 * * * * [progress]: [ 17 / 77 ] simplifiying candidate #<alt (λ (x.re x.im) (+.p16 (real->posit16 0.0) (-.p16 (*.p16 (+.p16 x.re x.im) (*.p16 (-.p16 x.re x.im) x.re)) (*.p16 (+.p16 (*.p16 x.re x.im) (*.p16 x.im x.re)) x.im))))>
53.044 * * * * [progress]: [ 18 / 77 ] simplifiying candidate #<alt (λ (x.re x.im) (+.p16 (-.p16 (*.p16 (+.p16 x.re x.im) (*.p16 (-.p16 x.re x.im) x.re)) (*.p16 (+.p16 (*.p16 x.re x.im) (*.p16 x.im x.re)) x.im)) (real->posit16 0.0)))>
53.044 * * * * [progress]: [ 19 / 77 ] simplifiying candidate #<alt (λ (x.re x.im) (-.p16 (-.p16 (*.p16 (+.p16 x.re x.im) (*.p16 (-.p16 x.re x.im) x.re)) (*.p16 (+.p16 (*.p16 x.re x.im) (*.p16 x.im x.re)) x.im)) (real->posit16 0.0)))>
53.044 * * * * [progress]: [ 20 / 77 ] simplifiying candidate #<alt (λ (x.re x.im) (*.p16 (real->posit16 1.0) (-.p16 (*.p16 (+.p16 x.re x.im) (*.p16 (-.p16 x.re x.im) x.re)) (*.p16 (+.p16 (*.p16 x.re x.im) (*.p16 x.im x.re)) x.im))))>
53.044 * * * * [progress]: [ 21 / 77 ] simplifiying candidate #<alt (λ (x.re x.im) (*.p16 (-.p16 (*.p16 (+.p16 x.re x.im) (*.p16 (-.p16 x.re x.im) x.re)) (*.p16 (+.p16 (*.p16 x.re x.im) (*.p16 x.im x.re)) x.im)) (real->posit16 1.0)))>
53.044 * * * * [progress]: [ 22 / 77 ] simplifiying candidate #<alt (λ (x.re x.im) (/.p16 (-.p16 (*.p16 (+.p16 x.re x.im) (*.p16 (-.p16 x.re x.im) x.re)) (*.p16 (+.p16 (*.p16 x.re x.im) (*.p16 x.im x.re)) x.im)) (real->posit16 1.0)))>
53.044 * * * * [progress]: [ 23 / 77 ] simplifiying candidate #<alt (λ (x.re x.im) (-.p16 (*.p16 (+.p16 x.re x.im) (*.p16 (-.p16 x.re x.im) x.re)) (*.p16 (+.p16 (+.p16 (*.p16 x.re x.im) (real->posit16 0.0)) (*.p16 x.im x.re)) x.im)))>
53.044 * * * * [progress]: [ 24 / 77 ] simplifiying candidate #<alt (λ (x.re x.im) (-.p16 (*.p16 (+.p16 x.re x.im) (*.p16 (-.p16 x.re x.im) x.re)) (*.p16 (+.p16 (+.p16 (*.p16 x.re x.im) (*.p16 x.im x.re)) (real->posit16 0.0)) x.im)))>
53.044 * * * * [progress]: [ 25 / 77 ] simplifiying candidate #<alt (λ (x.re x.im) (-.p16 (*.p16 (+.p16 x.re x.im) (*.p16 (-.p16 x.re x.im) x.re)) (*.p16 (+.p16 (real->posit16 0.0) (+.p16 (*.p16 x.re x.im) (*.p16 x.im x.re))) x.im)))>
53.044 * * * * [progress]: [ 26 / 77 ] simplifiying candidate #<alt (λ (x.re x.im) (-.p16 (*.p16 (+.p16 x.re x.im) (*.p16 (-.p16 x.re x.im) x.re)) (*.p16 (+.p16 (*.p16 x.re x.im) (+.p16 (real->posit16 0.0) (*.p16 x.im x.re))) x.im)))>
53.044 * * * * [progress]: [ 27 / 77 ] simplifiying candidate #<alt (λ (x.re x.im) (-.p16 (*.p16 (+.p16 x.re x.im) (*.p16 (-.p16 x.re x.im) x.re)) (*.p16 (-.p16 (+.p16 (*.p16 x.re x.im) (*.p16 x.im x.re)) (real->posit16 0.0)) x.im)))>
53.044 * * * * [progress]: [ 28 / 77 ] simplifiying candidate #<alt (λ (x.re x.im) (-.p16 (*.p16 (+.p16 x.re x.im) (*.p16 (-.p16 x.re x.im) x.re)) (*.p16 (-.p16 (*.p16 x.re x.im) (-.p16 (real->posit16 0.0) (*.p16 x.im x.re))) x.im)))>
53.045 * * * * [progress]: [ 29 / 77 ] simplifiying candidate #<alt (λ (x.re x.im) (-.p16 (*.p16 (+.p16 x.re x.im) (*.p16 (-.p16 x.re x.im) x.re)) (*.p16 (*.p16 (real->posit16 1.0) (+.p16 (*.p16 x.re x.im) (*.p16 x.im x.re))) x.im)))>
53.045 * * * * [progress]: [ 30 / 77 ] simplifiying candidate #<alt (λ (x.re x.im) (-.p16 (*.p16 (+.p16 x.re x.im) (*.p16 (-.p16 x.re x.im) x.re)) (*.p16 (quire16->posit16 (posit16->quire16 (+.p16 (*.p16 x.re x.im) (*.p16 x.im x.re)))) x.im)))>
53.045 * * * * [progress]: [ 31 / 77 ] simplifiying candidate #<alt (λ (x.re x.im) (-.p16 (*.p16 (+.p16 x.re x.im) (*.p16 (-.p16 x.re x.im) x.re)) (*.p16 (quire16->posit16 (quire16-mul-add (posit16->quire16 (*.p16 x.re x.im)) (*.p16 x.im x.re) (real->posit16 1.0))) x.im)))>
53.045 * * * * [progress]: [ 32 / 77 ] simplifiying candidate #<alt (λ (x.re x.im) (-.p16 (*.p16 (+.p16 x.re x.im) (*.p16 (-.p16 x.re x.im) x.re)) (*.p16 (quire16->posit16 (quire16-mul-add (posit16->quire16 (*.p16 x.re x.im)) x.im x.re)) x.im)))>
53.045 * * * * [progress]: [ 33 / 77 ] simplifiying candidate #<alt (λ (x.re x.im) (-.p16 (*.p16 (+.p16 x.re x.im) (*.p16 (-.p16 x.re x.im) x.re)) (*.p16 (+.p16 (real->posit16 0.0) (+.p16 (*.p16 x.re x.im) (*.p16 x.im x.re))) x.im)))>
53.045 * * * * [progress]: [ 34 / 77 ] simplifiying candidate #<alt (λ (x.re x.im) (-.p16 (*.p16 (+.p16 x.re x.im) (*.p16 (-.p16 x.re x.im) x.re)) (*.p16 (+.p16 (+.p16 (*.p16 x.re x.im) (*.p16 x.im x.re)) (real->posit16 0.0)) x.im)))>
53.045 * * * * [progress]: [ 35 / 77 ] simplifiying candidate #<alt (λ (x.re x.im) (-.p16 (*.p16 (+.p16 x.re x.im) (*.p16 (-.p16 x.re x.im) x.re)) (*.p16 (-.p16 (+.p16 (*.p16 x.re x.im) (*.p16 x.im x.re)) (real->posit16 0.0)) x.im)))>
53.045 * * * * [progress]: [ 36 / 77 ] simplifiying candidate #<alt (λ (x.re x.im) (-.p16 (*.p16 (+.p16 x.re x.im) (*.p16 (-.p16 x.re x.im) x.re)) (*.p16 (*.p16 (real->posit16 1.0) (+.p16 (*.p16 x.re x.im) (*.p16 x.im x.re))) x.im)))>
53.045 * * * * [progress]: [ 37 / 77 ] simplifiying candidate #<alt (λ (x.re x.im) (-.p16 (*.p16 (+.p16 x.re x.im) (*.p16 (-.p16 x.re x.im) x.re)) (*.p16 (*.p16 (+.p16 (*.p16 x.re x.im) (*.p16 x.im x.re)) (real->posit16 1.0)) x.im)))>
53.045 * * * * [progress]: [ 38 / 77 ] simplifiying candidate #<alt (λ (x.re x.im) (-.p16 (*.p16 (+.p16 x.re x.im) (*.p16 (-.p16 x.re x.im) x.re)) (*.p16 (/.p16 (+.p16 (*.p16 x.re x.im) (*.p16 x.im x.re)) (real->posit16 1.0)) x.im)))>
53.045 * * * * [progress]: [ 39 / 77 ] simplifiying candidate #<alt (λ (x.re x.im) (-.p16 (*.p16 (+.p16 x.re x.im) (*.p16 (-.p16 x.re x.im) x.re)) (*.p16 (+.p16 (*.p16 x.im x.re) (*.p16 x.re x.im)) x.im)))>
53.045 * * * * [progress]: [ 40 / 77 ] simplifiying candidate #<alt (λ (x.re x.im) (-.p16 (+.p16 (*.p16 (+.p16 x.re x.im) (real->posit16 0.0)) (*.p16 (+.p16 x.re x.im) (*.p16 (-.p16 x.re x.im) x.re))) (*.p16 (+.p16 (*.p16 x.re x.im) (*.p16 x.im x.re)) x.im)))>
53.045 * * * * [progress]: [ 41 / 77 ] simplifiying candidate #<alt (λ (x.re x.im) (-.p16 (+.p16 (*.p16 (+.p16 x.re x.im) (*.p16 (-.p16 x.re x.im) x.re)) (*.p16 (+.p16 x.re x.im) (real->posit16 0.0))) (*.p16 (+.p16 (*.p16 x.re x.im) (*.p16 x.im x.re)) x.im)))>
53.045 * * * * [progress]: [ 42 / 77 ] simplifiying candidate #<alt (λ (x.re x.im) (-.p16 (+.p16 (*.p16 (real->posit16 0.0) (+.p16 x.re x.im)) (*.p16 (*.p16 (-.p16 x.re x.im) x.re) (+.p16 x.re x.im))) (*.p16 (+.p16 (*.p16 x.re x.im) (*.p16 x.im x.re)) x.im)))>
53.045 * * * * [progress]: [ 43 / 77 ] simplifiying candidate #<alt (λ (x.re x.im) (-.p16 (+.p16 (*.p16 (*.p16 (-.p16 x.re x.im) x.re) (+.p16 x.re x.im)) (*.p16 (real->posit16 0.0) (+.p16 x.re x.im))) (*.p16 (+.p16 (*.p16 x.re x.im) (*.p16 x.im x.re)) x.im)))>
53.045 * * * * [progress]: [ 44 / 77 ] simplifiying candidate #<alt (λ (x.re x.im) (-.p16 (*.p16 (*.p16 (+.p16 x.re x.im) (-.p16 x.re x.im)) x.re) (*.p16 (+.p16 (*.p16 x.re x.im) (*.p16 x.im x.re)) x.im)))>
53.045 * * * * [progress]: [ 45 / 77 ] simplifiying candidate #<alt (λ (x.re x.im) (-.p16 (*.p16 (real->posit16 1.0) (*.p16 (+.p16 x.re x.im) (*.p16 (-.p16 x.re x.im) x.re))) (*.p16 (+.p16 (*.p16 x.re x.im) (*.p16 x.im x.re)) x.im)))>
53.046 * * * * [progress]: [ 46 / 77 ] simplifiying candidate #<alt (λ (x.re x.im) (-.p16 (*.p16 (real->posit16 1.0) (*.p16 (+.p16 x.re x.im) (*.p16 (-.p16 x.re x.im) x.re))) (*.p16 (+.p16 (*.p16 x.re x.im) (*.p16 x.im x.re)) x.im)))>
53.046 * * * * [progress]: [ 47 / 77 ] simplifiying candidate #<alt (λ (x.re x.im) (-.p16 (*.p16 (+.p16 x.re x.im) (*.p16 (real->posit16 1.0) (*.p16 (-.p16 x.re x.im) x.re))) (*.p16 (+.p16 (*.p16 x.re x.im) (*.p16 x.im x.re)) x.im)))>
53.046 * * * * [progress]: [ 48 / 77 ] simplifiying candidate #<alt (λ (x.re x.im) (-.p16 (/.p16 (*.p16 (+.p16 x.re x.im) (*.p16 (-.p16 (*.p16 x.re x.re) (*.p16 x.im x.im)) x.re)) (+.p16 x.re x.im)) (*.p16 (+.p16 (*.p16 x.re x.im) (*.p16 x.im x.re)) x.im)))>
53.046 * * * * [progress]: [ 49 / 77 ] simplifiying candidate #<alt (λ (x.re x.im) (-.p16 (/.p16 (*.p16 (+.p16 x.re x.im) (*.p16 (-.p16 x.re x.im) x.re)) (real->posit16 1.0)) (*.p16 (+.p16 (*.p16 x.re x.im) (*.p16 x.im x.re)) x.im)))>
53.046 * * * * [progress]: [ 50 / 77 ] simplifiying candidate #<alt (λ (x.re x.im) (-.p16 (/.p16 (*.p16 (+.p16 x.re x.im) (*.p16 (-.p16 x.re x.im) x.re)) (real->posit16 1.0)) (*.p16 (+.p16 (*.p16 x.re x.im) (*.p16 x.im x.re)) x.im)))>
53.046 * * * * [progress]: [ 51 / 77 ] simplifiying candidate #<alt (λ (x.re x.im) (-.p16 (/.p16 (*.p16 (+.p16 x.re x.im) (*.p16 (-.p16 x.re x.im) x.re)) (real->posit16 1.0)) (*.p16 (+.p16 (*.p16 x.re x.im) (*.p16 x.im x.re)) x.im)))>
53.046 * * * * [progress]: [ 52 / 77 ] simplifiying candidate #<alt (λ (x.re x.im) (-.p16 (*.p16 (real->posit16 1.0) (*.p16 (+.p16 x.re x.im) (*.p16 (-.p16 x.re x.im) x.re))) (*.p16 (+.p16 (*.p16 x.re x.im) (*.p16 x.im x.re)) x.im)))>
53.046 * * * * [progress]: [ 53 / 77 ] simplifiying candidate #<alt (λ (x.re x.im) (-.p16 (quire16->posit16 (posit16->quire16 (*.p16 (+.p16 x.re x.im) (*.p16 (-.p16 x.re x.im) x.re)))) (*.p16 (+.p16 (*.p16 x.re x.im) (*.p16 x.im x.re)) x.im)))>
53.046 * * * * [progress]: [ 54 / 77 ] simplifiying candidate #<alt (λ (x.re x.im) (-.p16 (+.p16 (real->posit16 0.0) (*.p16 (+.p16 x.re x.im) (*.p16 (-.p16 x.re x.im) x.re))) (*.p16 (+.p16 (*.p16 x.re x.im) (*.p16 x.im x.re)) x.im)))>
53.046 * * * * [progress]: [ 55 / 77 ] simplifiying candidate #<alt (λ (x.re x.im) (-.p16 (+.p16 (*.p16 (+.p16 x.re x.im) (*.p16 (-.p16 x.re x.im) x.re)) (real->posit16 0.0)) (*.p16 (+.p16 (*.p16 x.re x.im) (*.p16 x.im x.re)) x.im)))>
53.046 * * * * [progress]: [ 56 / 77 ] simplifiying candidate #<alt (λ (x.re x.im) (-.p16 (-.p16 (*.p16 (+.p16 x.re x.im) (*.p16 (-.p16 x.re x.im) x.re)) (real->posit16 0.0)) (*.p16 (+.p16 (*.p16 x.re x.im) (*.p16 x.im x.re)) x.im)))>
53.046 * * * * [progress]: [ 57 / 77 ] simplifiying candidate #<alt (λ (x.re x.im) (-.p16 (*.p16 (real->posit16 1.0) (*.p16 (+.p16 x.re x.im) (*.p16 (-.p16 x.re x.im) x.re))) (*.p16 (+.p16 (*.p16 x.re x.im) (*.p16 x.im x.re)) x.im)))>
53.046 * * * * [progress]: [ 58 / 77 ] simplifiying candidate #<alt (λ (x.re x.im) (-.p16 (*.p16 (*.p16 (+.p16 x.re x.im) (*.p16 (-.p16 x.re x.im) x.re)) (real->posit16 1.0)) (*.p16 (+.p16 (*.p16 x.re x.im) (*.p16 x.im x.re)) x.im)))>
53.046 * * * * [progress]: [ 59 / 77 ] simplifiying candidate #<alt (λ (x.re x.im) (-.p16 (/.p16 (*.p16 (+.p16 x.re x.im) (*.p16 (-.p16 x.re x.im) x.re)) (real->posit16 1.0)) (*.p16 (+.p16 (*.p16 x.re x.im) (*.p16 x.im x.re)) x.im)))>
53.047 * * * * [progress]: [ 60 / 77 ] simplifiying candidate #<alt (λ (x.re x.im) (-.p16 (*.p16 (*.p16 (-.p16 x.re x.im) x.re) (+.p16 x.re x.im)) (*.p16 (+.p16 (*.p16 x.re x.im) (*.p16 x.im x.re)) x.im)))>
53.047 * * * * [progress]: [ 61 / 77 ] simplifiying candidate #<alt (λ (x.re x.im) (-.p16 (*.p16 (+.p16 x.re x.im) (*.p16 (-.p16 x.re x.im) x.re)) (*.p16 (real->posit16 1.0) (*.p16 (+.p16 (*.p16 x.re x.im) (*.p16 x.im x.re)) x.im))))>
53.047 * * * * [progress]: [ 62 / 77 ] simplifiying candidate #<alt (λ (x.re x.im) (-.p16 (*.p16 (+.p16 x.re x.im) (*.p16 (-.p16 x.re x.im) x.re)) (*.p16 (real->posit16 1.0) (*.p16 (+.p16 (*.p16 x.re x.im) (*.p16 x.im x.re)) x.im))))>
53.047 * * * * [progress]: [ 63 / 77 ] simplifiying candidate #<alt (λ (x.re x.im) (-.p16 (*.p16 (+.p16 x.re x.im) (*.p16 (-.p16 x.re x.im) x.re)) (*.p16 (+.p16 (*.p16 x.re x.im) (*.p16 x.im x.re)) (*.p16 (real->posit16 1.0) x.im))))>
53.047 * * * * [progress]: [ 64 / 77 ] simplifiying candidate #<alt (λ (x.re x.im) (-.p16 (*.p16 (+.p16 x.re x.im) (*.p16 (-.p16 x.re x.im) x.re)) (/.p16 (*.p16 (+.p16 (*.p16 x.re x.im) (*.p16 x.im x.re)) x.im) (real->posit16 1.0))))>
53.047 * * * * [progress]: [ 65 / 77 ] simplifiying candidate #<alt (λ (x.re x.im) (-.p16 (*.p16 (+.p16 x.re x.im) (*.p16 (-.p16 x.re x.im) x.re)) (*.p16 (real->posit16 1.0) (*.p16 (+.p16 (*.p16 x.re x.im) (*.p16 x.im x.re)) x.im))))>
53.047 * * * * [progress]: [ 66 / 77 ] simplifiying candidate #<alt (λ (x.re x.im) (-.p16 (*.p16 (+.p16 x.re x.im) (*.p16 (-.p16 x.re x.im) x.re)) (quire16->posit16 (posit16->quire16 (*.p16 (+.p16 (*.p16 x.re x.im) (*.p16 x.im x.re)) x.im)))))>
53.047 * * * * [progress]: [ 67 / 77 ] simplifiying candidate #<alt (λ (x.re x.im) (-.p16 (*.p16 (+.p16 x.re x.im) (*.p16 (-.p16 x.re x.im) x.re)) (+.p16 (real->posit16 0.0) (*.p16 (+.p16 (*.p16 x.re x.im) (*.p16 x.im x.re)) x.im))))>
53.047 * * * * [progress]: [ 68 / 77 ] simplifiying candidate #<alt (λ (x.re x.im) (-.p16 (*.p16 (+.p16 x.re x.im) (*.p16 (-.p16 x.re x.im) x.re)) (+.p16 (*.p16 (+.p16 (*.p16 x.re x.im) (*.p16 x.im x.re)) x.im) (real->posit16 0.0))))>
53.047 * * * * [progress]: [ 69 / 77 ] simplifiying candidate #<alt (λ (x.re x.im) (-.p16 (*.p16 (+.p16 x.re x.im) (*.p16 (-.p16 x.re x.im) x.re)) (-.p16 (*.p16 (+.p16 (*.p16 x.re x.im) (*.p16 x.im x.re)) x.im) (real->posit16 0.0))))>
53.047 * * * * [progress]: [ 70 / 77 ] simplifiying candidate #<alt (λ (x.re x.im) (-.p16 (*.p16 (+.p16 x.re x.im) (*.p16 (-.p16 x.re x.im) x.re)) (*.p16 (real->posit16 1.0) (*.p16 (+.p16 (*.p16 x.re x.im) (*.p16 x.im x.re)) x.im))))>
53.047 * * * * [progress]: [ 71 / 77 ] simplifiying candidate #<alt (λ (x.re x.im) (-.p16 (*.p16 (+.p16 x.re x.im) (*.p16 (-.p16 x.re x.im) x.re)) (*.p16 (*.p16 (+.p16 (*.p16 x.re x.im) (*.p16 x.im x.re)) x.im) (real->posit16 1.0))))>
53.047 * * * * [progress]: [ 72 / 77 ] simplifiying candidate #<alt (λ (x.re x.im) (-.p16 (*.p16 (+.p16 x.re x.im) (*.p16 (-.p16 x.re x.im) x.re)) (/.p16 (*.p16 (+.p16 (*.p16 x.re x.im) (*.p16 x.im x.re)) x.im) (real->posit16 1.0))))>
53.047 * * * * [progress]: [ 73 / 77 ] simplifiying candidate #<alt (λ (x.re x.im) (-.p16 (*.p16 (+.p16 x.re x.im) (*.p16 (-.p16 x.re x.im) x.re)) (*.p16 x.im (+.p16 (*.p16 x.re x.im) (*.p16 x.im x.re)))))>
53.048 * * * * [progress]: [ 74 / 77 ] simplifiying candidate #<alt (λ (x.re x.im) (-.p16 (*.p16 (+.p16 x.re x.im) (*.p16 (-.p16 x.re x.im) x.re)) (*.p16 (+.p16 (*.p16 x.re x.im) (*.p16 x.im x.re)) x.im)))>
53.048 * * * * [progress]: [ 75 / 77 ] simplifiying candidate #<alt (λ (x.re x.im) (-.p16 (*.p16 (+.p16 x.re x.im) (*.p16 (-.p16 x.re x.im) x.re)) (*.p16 (+.p16 (*.p16 x.re x.im) (*.p16 x.im x.re)) x.im)))>
53.048 * * * * [progress]: [ 76 / 77 ] simplifiying candidate #<alt (λ (x.re x.im) (-.p16 (*.p16 (+.p16 x.re x.im) (*.p16 (-.p16 x.re x.im) x.re)) (*.p16 (+.p16 (*.p16 x.re x.im) (*.p16 x.im x.re)) x.im)))>
53.048 * * * * [progress]: [ 77 / 77 ] simplifiying candidate #<alt (λ (x.re x.im) (-.p16 (*.p16 (+.p16 x.re x.im) (*.p16 (-.p16 x.re x.im) x.re)) (*.p16 (+.p16 (*.p16 x.re x.im) (*.p16 x.im x.re)) x.im)))>
53.049 * [simplify]: Simplifying:
  (-.p16 (*.p16 (+.p16 x.re x.im) (*.p16 (-.p16 x.re x.im) x.re)) (real->posit16 0.0))
  (-.p16 (*.p16 (+.p16 x.re x.im) (*.p16 (-.p16 x.re x.im) x.re)) (*.p16 (+.p16 (*.p16 x.re x.im) (*.p16 x.im x.re)) x.im))
  (-.p16 (*.p16 (+.p16 x.re x.im) (*.p16 (-.p16 x.re x.im) x.re)) (*.p16 (+.p16 (*.p16 x.re x.im) (*.p16 x.im x.re)) x.im))
  (-.p16 (*.p16 (+.p16 x.re x.im) (real->posit16 0.0)) (*.p16 (+.p16 (*.p16 x.re x.im) (*.p16 x.im x.re)) x.im))
  (-.p16 (*.p16 (*.p16 (-.p16 x.re x.im) x.re) (+.p16 x.re x.im)) (*.p16 (+.p16 (*.p16 x.re x.im) (*.p16 x.im x.re)) x.im))
  (-.p16 (*.p16 (real->posit16 0.0) (+.p16 x.re x.im)) (*.p16 (+.p16 (*.p16 x.re x.im) (*.p16 x.im x.re)) x.im))
  (-.p16 (*.p16 (+.p16 x.re x.im) (*.p16 (-.p16 x.re x.im) x.re)) (*.p16 (+.p16 (*.p16 x.re x.im) (*.p16 x.im x.re)) x.im))
  (-.p16 (real->posit16 0.0) (*.p16 (+.p16 (*.p16 x.re x.im) (*.p16 x.im x.re)) x.im))
  (+.p16 (real->posit16 0.0) (*.p16 (+.p16 (*.p16 x.re x.im) (*.p16 x.im x.re)) x.im))
  (-.p16 (*.p16 (+.p16 x.re x.im) (*.p16 (-.p16 x.re x.im) x.re)) (*.p16 (+.p16 (*.p16 x.re x.im) (*.p16 x.im x.re)) x.im))
  (neg.p16 (*.p16 (+.p16 (*.p16 x.re x.im) (*.p16 x.im x.re)) x.im))
  (-.p16 (*.p16 (*.p16 (+.p16 x.re x.im) (*.p16 (-.p16 x.re x.im) x.re)) (*.p16 (+.p16 x.re x.im) (*.p16 (-.p16 x.re x.im) x.re))) (*.p16 (*.p16 (+.p16 (*.p16 x.re x.im) (*.p16 x.im x.re)) x.im) (*.p16 (+.p16 (*.p16 x.re x.im) (*.p16 x.im x.re)) x.im)))
  (+.p16 (*.p16 (+.p16 x.re x.im) (*.p16 (-.p16 x.re x.im) x.re)) (*.p16 (+.p16 (*.p16 x.re x.im) (*.p16 x.im x.re)) x.im))
  (real->posit16 1.0)
  (posit16->quire16 (-.p16 (*.p16 (+.p16 x.re x.im) (*.p16 (-.p16 x.re x.im) x.re)) (*.p16 (+.p16 (*.p16 x.re x.im) (*.p16 x.im x.re)) x.im)))
  (quire16-mul-sub (posit16->quire16 (*.p16 (+.p16 x.re x.im) (*.p16 (-.p16 x.re x.im) x.re))) (*.p16 (+.p16 (*.p16 x.re x.im) (*.p16 x.im x.re)) x.im) (real->posit16 1.0))
  (quire16-mul-sub (posit16->quire16 (*.p16 (+.p16 x.re x.im) (*.p16 (-.p16 x.re x.im) x.re))) (+.p16 (*.p16 x.re x.im) (*.p16 x.im x.re)) x.im)
  (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 x.re x.im) (real->posit16 0.0))
  (+.p16 (*.p16 x.re x.im) (*.p16 x.im x.re))
  (+.p16 (*.p16 x.re x.im) (*.p16 x.im x.re))
  (+.p16 (real->posit16 0.0) (*.p16 x.im x.re))
  (+.p16 (*.p16 x.re x.im) (*.p16 x.im x.re))
  (-.p16 (real->posit16 0.0) (*.p16 x.im x.re))
  (real->posit16 1.0)
  (posit16->quire16 (+.p16 (*.p16 x.re x.im) (*.p16 x.im x.re)))
  (quire16-mul-add (posit16->quire16 (*.p16 x.re x.im)) (*.p16 x.im x.re) (real->posit16 1.0))
  (quire16-mul-add (posit16->quire16 (*.p16 x.re x.im)) x.im x.re)
  (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 x.re x.im) (real->posit16 0.0))
  (*.p16 (+.p16 x.re x.im) (*.p16 (-.p16 x.re x.im) x.re))
  (*.p16 (+.p16 x.re x.im) (*.p16 (-.p16 x.re x.im) x.re))
  (*.p16 (+.p16 x.re x.im) (real->posit16 0.0))
  (*.p16 (real->posit16 0.0) (+.p16 x.re x.im))
  (*.p16 (*.p16 (-.p16 x.re x.im) x.re) (+.p16 x.re x.im))
  (*.p16 (*.p16 (-.p16 x.re x.im) x.re) (+.p16 x.re x.im))
  (*.p16 (real->posit16 0.0) (+.p16 x.re x.im))
  (*.p16 (+.p16 x.re x.im) (-.p16 x.re x.im))
  (*.p16 (+.p16 x.re x.im) (*.p16 (-.p16 x.re x.im) x.re))
  (*.p16 (+.p16 x.re x.im) (*.p16 (-.p16 x.re x.im) x.re))
  (*.p16 (real->posit16 1.0) (*.p16 (-.p16 x.re x.im) x.re))
  (*.p16 (+.p16 x.re x.im) (*.p16 (-.p16 (*.p16 x.re x.re) (*.p16 x.im x.im)) x.re))
  (*.p16 (+.p16 x.re x.im) (*.p16 (-.p16 x.re x.im) x.re))
  (*.p16 (+.p16 x.re x.im) (*.p16 (-.p16 x.re x.im) x.re))
  (*.p16 (+.p16 x.re x.im) (*.p16 (-.p16 x.re x.im) x.re))
  (real->posit16 1.0)
  (posit16->quire16 (*.p16 (+.p16 x.re x.im) (*.p16 (-.p16 x.re x.im) x.re)))
  (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 x.re x.im) (*.p16 x.im x.re)) x.im)
  (*.p16 (+.p16 (*.p16 x.re x.im) (*.p16 x.im x.re)) x.im)
  (*.p16 (real->posit16 1.0) x.im)
  (*.p16 (+.p16 (*.p16 x.re x.im) (*.p16 x.im x.re)) x.im)
  (real->posit16 1.0)
  (posit16->quire16 (*.p16 (+.p16 (*.p16 x.re x.im) (*.p16 x.im x.re)) x.im))
  (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 x.re x.im) x.re)
  (*.p16 (-.p16 x.re x.im) x.re)
  (*.p16 (-.p16 x.re x.im) x.re)
  (*.p16 (-.p16 x.re x.im) x.re)
53.050 * * [simplify]: iteration 1: (49 enodes)
53.074 * * [simplify]: iteration 2: (109 enodes)
53.133 * * [simplify]: iteration 3: (443 enodes)
55.711 * * [simplify]: Extracting #0: cost 23 inf + 0
55.712 * * [simplify]: Extracting #1: cost 358 inf + 1
55.714 * * [simplify]: Extracting #2: cost 500 inf + 22535
55.725 * * [simplify]: Extracting #3: cost 319 inf + 290499
55.765 * * [simplify]: Extracting #4: cost 2 inf + 654463
55.795 * * [simplify]: Extracting #5: cost 0 inf + 656027
55.826 * [simplify]: Simplified to:
  (*.p16 (+.p16 x.im x.re) (*.p16 (-.p16 x.re x.im) x.re))
  (-.p16 (*.p16 (+.p16 x.im x.re) (*.p16 (-.p16 x.re x.im) x.re)) (*.p16 (*.p16 (+.p16 x.im x.im) x.re) x.im))
  (-.p16 (*.p16 (+.p16 x.im x.re) (*.p16 (-.p16 x.re x.im) x.re)) (*.p16 (*.p16 (+.p16 x.im x.im) x.re) x.im))
  (neg.p16 (*.p16 (*.p16 (+.p16 x.im x.im) x.re) x.im))
  (-.p16 (*.p16 (+.p16 x.im x.re) (*.p16 (-.p16 x.re x.im) x.re)) (*.p16 (*.p16 (+.p16 x.im x.im) x.re) x.im))
  (neg.p16 (*.p16 (*.p16 (+.p16 x.im x.im) x.re) x.im))
  (-.p16 (*.p16 (+.p16 x.im x.re) (*.p16 (-.p16 x.re x.im) x.re)) (*.p16 (*.p16 (+.p16 x.im x.im) x.re) x.im))
  (neg.p16 (*.p16 (*.p16 (+.p16 x.im x.im) x.re) x.im))
  (*.p16 (*.p16 (+.p16 x.im x.im) x.re) x.im)
  (-.p16 (*.p16 (+.p16 x.im x.re) (*.p16 (-.p16 x.re x.im) x.re)) (*.p16 (*.p16 (+.p16 x.im x.im) x.re) x.im))
  (neg.p16 (*.p16 (*.p16 (+.p16 x.im x.im) x.re) x.im))
  (*.p16 (-.p16 (*.p16 (+.p16 x.im x.re) (*.p16 (-.p16 x.re x.im) x.re)) (*.p16 (*.p16 (+.p16 x.im x.im) x.re) x.im)) (+.p16 (*.p16 (+.p16 x.im x.re) (*.p16 (-.p16 x.re x.im) x.re)) (*.p16 (*.p16 (+.p16 x.im x.im) x.re) x.im)))
  (+.p16 (*.p16 (+.p16 x.im x.re) (*.p16 (-.p16 x.re x.im) x.re)) (*.p16 (*.p16 (+.p16 x.im x.im) x.re) x.im))
  (real->posit16 1.0)
  (posit16->quire16 (-.p16 (*.p16 (+.p16 x.im x.re) (*.p16 (-.p16 x.re x.im) x.re)) (*.p16 (*.p16 (+.p16 x.im x.im) x.re) x.im)))
  (quire16-mul-sub (posit16->quire16 (*.p16 (+.p16 x.im x.re) (*.p16 (-.p16 x.re x.im) x.re))) (*.p16 (*.p16 (+.p16 x.im x.im) x.re) x.im) (real->posit16 1.0))
  (quire16-mul-sub (posit16->quire16 (*.p16 (+.p16 x.im x.re) (*.p16 (-.p16 x.re x.im) x.re))) (*.p16 (+.p16 x.im x.im) x.re) x.im)
  (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 x.im x.re)
  (*.p16 (+.p16 x.im x.im) x.re)
  (*.p16 (+.p16 x.im x.im) x.re)
  (*.p16 x.im x.re)
  (*.p16 (+.p16 x.im x.im) x.re)
  (neg.p16 (*.p16 x.im x.re))
  (real->posit16 1.0)
  (posit16->quire16 (*.p16 (+.p16 x.im x.im) x.re))
  (quire16-mul-add (posit16->quire16 (*.p16 x.im x.re)) (*.p16 x.im x.re) (real->posit16 1.0))
  (quire16-mul-add (posit16->quire16 (*.p16 x.im x.re)) x.im x.re)
  (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 0.0)
  (*.p16 (+.p16 x.im x.re) (*.p16 (-.p16 x.re x.im) x.re))
  (*.p16 (+.p16 x.im x.re) (*.p16 (-.p16 x.re x.im) x.re))
  (real->posit16 0.0)
  (real->posit16 0.0)
  (*.p16 (+.p16 x.im x.re) (*.p16 (-.p16 x.re x.im) x.re))
  (*.p16 (+.p16 x.im x.re) (*.p16 (-.p16 x.re x.im) x.re))
  (real->posit16 0.0)
  (*.p16 (+.p16 x.im x.re) (-.p16 x.re x.im))
  (*.p16 (+.p16 x.im x.re) (*.p16 (-.p16 x.re x.im) x.re))
  (*.p16 (+.p16 x.im x.re) (*.p16 (-.p16 x.re x.im) x.re))
  (*.p16 (-.p16 x.re x.im) x.re)
  (*.p16 x.re (*.p16 (*.p16 (+.p16 x.im x.re) (+.p16 x.im x.re)) (-.p16 x.re x.im)))
  (*.p16 (+.p16 x.im x.re) (*.p16 (-.p16 x.re x.im) x.re))
  (*.p16 (+.p16 x.im x.re) (*.p16 (-.p16 x.re x.im) x.re))
  (*.p16 (+.p16 x.im x.re) (*.p16 (-.p16 x.re x.im) x.re))
  (real->posit16 1.0)
  (posit16->quire16 (*.p16 (+.p16 x.im x.re) (*.p16 (-.p16 x.re x.im) x.re)))
  (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 x.im x.im) x.re) x.im)
  (*.p16 (*.p16 (+.p16 x.im x.im) x.re) x.im)
  x.im
  (*.p16 (*.p16 (+.p16 x.im x.im) x.re) x.im)
  (real->posit16 1.0)
  (posit16->quire16 (*.p16 (*.p16 (+.p16 x.im x.im) x.re) x.im))
  (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 x.re x.im) x.re)
  (*.p16 (-.p16 x.re x.im) x.re)
  (*.p16 (-.p16 x.re x.im) x.re)
  (*.p16 (-.p16 x.re x.im) x.re)
55.830 * * * [progress]: adding candidates to table
57.667 * [progress]: [Phase 3 of 3] Extracting.
57.668 * * [regime]: Finding splitpoints for: (#<alt (λ (x.re x.im) (quire16->posit16 (posit16->quire16 (/.p16 (*.p16 x.re (-.p16 (*.p16 (*.p16 (-.p16 x.re x.im) (+.p16 x.im x.re)) (*.p16 (-.p16 x.re x.im) (+.p16 x.im x.re))) (*.p16 (*.p16 (+.p16 x.im x.im) x.im) (*.p16 (+.p16 x.im x.im) x.im)))) (+.p16 (*.p16 (-.p16 x.re x.im) (+.p16 x.im x.re)) (*.p16 (+.p16 x.im x.im) x.im))))))> #<alt (λ (x.re x.im) (-.p16 (*.p16 (+.p16 x.re x.im) (*.p16 (-.p16 x.re x.im) x.re)) (*.p16 (+.p16 (*.p16 x.re x.im) (*.p16 x.im x.re)) x.im)))> #<alt (λ (x.re x.im) (quire16->posit16 (quire16-mul-sub (posit16->quire16 (*.p16 x.re (*.p16 (-.p16 x.re x.im) (+.p16 x.im x.re)))) (*.p16 (+.p16 x.im x.im) x.re) x.im)))> #<alt (λ (x.re x.im) (quire16->posit16 (posit16->quire16 (*.p16 x.re (/.p16 (-.p16 (*.p16 (*.p16 (-.p16 x.re x.im) (+.p16 x.im x.re)) (*.p16 (-.p16 x.re x.im) (+.p16 x.im x.re))) (*.p16 (*.p16 (+.p16 x.im x.im) x.im) (*.p16 (+.p16 x.im x.im) x.im))) (+.p16 (*.p16 (-.p16 x.re x.im) (+.p16 x.im x.re)) (*.p16 (+.p16 x.im x.im) x.im)))))))> #<alt (λ (x.re x.im) (quire16->posit16 (posit16->quire16 (*.p16 x.re (quire16->posit16 (quire16-mul-sub (posit16->quire16 (*.p16 (-.p16 x.re x.im) (+.p16 x.im x.re))) (+.p16 x.im x.im) x.im))))))> #<alt (λ (x.re x.im) (-.p16 (*.p16 (-.p16 (*.p16 x.re x.re) (*.p16 x.im x.im)) x.re) (*.p16 x.re (*.p16 (+.p16 x.im x.im) x.im))))> #<alt (λ (x.re x.im) (/.p16 (-.p16 (*.p16 (*.p16 (-.p16 (*.p16 x.re x.re) (*.p16 x.im x.im)) x.re) (*.p16 (-.p16 (*.p16 x.re x.re) (*.p16 x.im x.im)) x.re)) (*.p16 (*.p16 (+.p16 (*.p16 x.re x.im) (*.p16 x.im x.re)) x.im) (*.p16 (+.p16 (*.p16 x.re x.im) (*.p16 x.im x.re)) x.im))) (+.p16 (*.p16 (-.p16 (*.p16 x.re x.re) (*.p16 x.im x.im)) x.re) (*.p16 (+.p16 (*.p16 x.re x.im) (*.p16 x.im x.re)) x.im))))> #<alt (λ (x.re x.im) (*.p16 x.re (-.p16 (*.p16 x.re x.re) (+.p16 (+.p16 (*.p16 x.im x.im) (*.p16 x.im x.im)) (*.p16 x.im x.im)))))> #<alt (λ (x.re x.im) (quire16->posit16 (posit16->quire16 (+.p16 (*.p16 x.re (*.p16 x.im (-.p16 x.re x.im))) (*.p16 x.re (-.p16 (*.p16 x.re (-.p16 x.re x.im)) (*.p16 (+.p16 x.im x.im) x.im)))))))>)
57.670 * * * [regime-changes]: Trying 2 branch expressions: (x.im x.re)
57.670 * * * * [regimes]: Trying to branch on x.im from (#<alt (λ (x.re x.im) (quire16->posit16 (posit16->quire16 (/.p16 (*.p16 x.re (-.p16 (*.p16 (*.p16 (-.p16 x.re x.im) (+.p16 x.im x.re)) (*.p16 (-.p16 x.re x.im) (+.p16 x.im x.re))) (*.p16 (*.p16 (+.p16 x.im x.im) x.im) (*.p16 (+.p16 x.im x.im) x.im)))) (+.p16 (*.p16 (-.p16 x.re x.im) (+.p16 x.im x.re)) (*.p16 (+.p16 x.im x.im) x.im))))))> #<alt (λ (x.re x.im) (-.p16 (*.p16 (+.p16 x.re x.im) (*.p16 (-.p16 x.re x.im) x.re)) (*.p16 (+.p16 (*.p16 x.re x.im) (*.p16 x.im x.re)) x.im)))> #<alt (λ (x.re x.im) (quire16->posit16 (quire16-mul-sub (posit16->quire16 (*.p16 x.re (*.p16 (-.p16 x.re x.im) (+.p16 x.im x.re)))) (*.p16 (+.p16 x.im x.im) x.re) x.im)))> #<alt (λ (x.re x.im) (quire16->posit16 (posit16->quire16 (*.p16 x.re (/.p16 (-.p16 (*.p16 (*.p16 (-.p16 x.re x.im) (+.p16 x.im x.re)) (*.p16 (-.p16 x.re x.im) (+.p16 x.im x.re))) (*.p16 (*.p16 (+.p16 x.im x.im) x.im) (*.p16 (+.p16 x.im x.im) x.im))) (+.p16 (*.p16 (-.p16 x.re x.im) (+.p16 x.im x.re)) (*.p16 (+.p16 x.im x.im) x.im)))))))> #<alt (λ (x.re x.im) (quire16->posit16 (posit16->quire16 (*.p16 x.re (quire16->posit16 (quire16-mul-sub (posit16->quire16 (*.p16 (-.p16 x.re x.im) (+.p16 x.im x.re))) (+.p16 x.im x.im) x.im))))))> #<alt (λ (x.re x.im) (-.p16 (*.p16 (-.p16 (*.p16 x.re x.re) (*.p16 x.im x.im)) x.re) (*.p16 x.re (*.p16 (+.p16 x.im x.im) x.im))))> #<alt (λ (x.re x.im) (/.p16 (-.p16 (*.p16 (*.p16 (-.p16 (*.p16 x.re x.re) (*.p16 x.im x.im)) x.re) (*.p16 (-.p16 (*.p16 x.re x.re) (*.p16 x.im x.im)) x.re)) (*.p16 (*.p16 (+.p16 (*.p16 x.re x.im) (*.p16 x.im x.re)) x.im) (*.p16 (+.p16 (*.p16 x.re x.im) (*.p16 x.im x.re)) x.im))) (+.p16 (*.p16 (-.p16 (*.p16 x.re x.re) (*.p16 x.im x.im)) x.re) (*.p16 (+.p16 (*.p16 x.re x.im) (*.p16 x.im x.re)) x.im))))> #<alt (λ (x.re x.im) (*.p16 x.re (-.p16 (*.p16 x.re x.re) (+.p16 (+.p16 (*.p16 x.im x.im) (*.p16 x.im x.im)) (*.p16 x.im x.im)))))> #<alt (λ (x.re x.im) (quire16->posit16 (posit16->quire16 (+.p16 (*.p16 x.re (*.p16 x.im (-.p16 x.re x.im))) (*.p16 x.re (-.p16 (*.p16 x.re (-.p16 x.re x.im)) (*.p16 (+.p16 x.im x.im) x.im)))))))>)
57.800 * * * * [regimes]: Trying to branch on x.re from (#<alt (λ (x.re x.im) (quire16->posit16 (posit16->quire16 (/.p16 (*.p16 x.re (-.p16 (*.p16 (*.p16 (-.p16 x.re x.im) (+.p16 x.im x.re)) (*.p16 (-.p16 x.re x.im) (+.p16 x.im x.re))) (*.p16 (*.p16 (+.p16 x.im x.im) x.im) (*.p16 (+.p16 x.im x.im) x.im)))) (+.p16 (*.p16 (-.p16 x.re x.im) (+.p16 x.im x.re)) (*.p16 (+.p16 x.im x.im) x.im))))))> #<alt (λ (x.re x.im) (-.p16 (*.p16 (+.p16 x.re x.im) (*.p16 (-.p16 x.re x.im) x.re)) (*.p16 (+.p16 (*.p16 x.re x.im) (*.p16 x.im x.re)) x.im)))> #<alt (λ (x.re x.im) (quire16->posit16 (quire16-mul-sub (posit16->quire16 (*.p16 x.re (*.p16 (-.p16 x.re x.im) (+.p16 x.im x.re)))) (*.p16 (+.p16 x.im x.im) x.re) x.im)))> #<alt (λ (x.re x.im) (quire16->posit16 (posit16->quire16 (*.p16 x.re (/.p16 (-.p16 (*.p16 (*.p16 (-.p16 x.re x.im) (+.p16 x.im x.re)) (*.p16 (-.p16 x.re x.im) (+.p16 x.im x.re))) (*.p16 (*.p16 (+.p16 x.im x.im) x.im) (*.p16 (+.p16 x.im x.im) x.im))) (+.p16 (*.p16 (-.p16 x.re x.im) (+.p16 x.im x.re)) (*.p16 (+.p16 x.im x.im) x.im)))))))> #<alt (λ (x.re x.im) (quire16->posit16 (posit16->quire16 (*.p16 x.re (quire16->posit16 (quire16-mul-sub (posit16->quire16 (*.p16 (-.p16 x.re x.im) (+.p16 x.im x.re))) (+.p16 x.im x.im) x.im))))))> #<alt (λ (x.re x.im) (-.p16 (*.p16 (-.p16 (*.p16 x.re x.re) (*.p16 x.im x.im)) x.re) (*.p16 x.re (*.p16 (+.p16 x.im x.im) x.im))))> #<alt (λ (x.re x.im) (/.p16 (-.p16 (*.p16 (*.p16 (-.p16 (*.p16 x.re x.re) (*.p16 x.im x.im)) x.re) (*.p16 (-.p16 (*.p16 x.re x.re) (*.p16 x.im x.im)) x.re)) (*.p16 (*.p16 (+.p16 (*.p16 x.re x.im) (*.p16 x.im x.re)) x.im) (*.p16 (+.p16 (*.p16 x.re x.im) (*.p16 x.im x.re)) x.im))) (+.p16 (*.p16 (-.p16 (*.p16 x.re x.re) (*.p16 x.im x.im)) x.re) (*.p16 (+.p16 (*.p16 x.re x.im) (*.p16 x.im x.re)) x.im))))> #<alt (λ (x.re x.im) (*.p16 x.re (-.p16 (*.p16 x.re x.re) (+.p16 (+.p16 (*.p16 x.im x.im) (*.p16 x.im x.im)) (*.p16 x.im x.im)))))> #<alt (λ (x.re x.im) (quire16->posit16 (posit16->quire16 (+.p16 (*.p16 x.re (*.p16 x.im (-.p16 x.re x.im))) (*.p16 x.re (-.p16 (*.p16 x.re (-.p16 x.re x.im)) (*.p16 (+.p16 x.im x.im) x.im)))))))>)
57.931 * * * [regime]: Found split indices: #<option (#s(si 4 256))>
57.931 * [simplify]: Simplifying:
  (quire16->posit16 (posit16->quire16 (*.p16 x.re (quire16->posit16 (quire16-mul-sub (posit16->quire16 (*.p16 (-.p16 x.re x.im) (+.p16 x.im x.re))) (+.p16 x.im x.im) x.im)))))
57.931 * * [simplify]: iteration 1: (12 enodes)
57.931 * * [simplify]: Extracting #0: cost 1 inf + 0
57.931 * * [simplify]: Extracting #1: cost 2 inf + 0
57.931 * * [simplify]: Extracting #2: cost 3 inf + 0
57.931 * * [simplify]: Extracting #3: cost 5 inf + 0
57.931 * * [simplify]: Extracting #4: cost 5 inf + 1
57.932 * * [simplify]: Extracting #5: cost 8 inf + 1
57.932 * * [simplify]: Extracting #6: cost 7 inf + 43
57.932 * * [simplify]: Extracting #7: cost 9 inf + 43
57.932 * * [simplify]: Extracting #8: cost 0 inf + 4421
57.932 * [simplify]: Simplified to:
  (quire16->posit16 (posit16->quire16 (*.p16 x.re (quire16->posit16 (quire16-mul-sub (posit16->quire16 (*.p16 (-.p16 x.re x.im) (+.p16 x.im x.re))) (+.p16 x.im x.im) x.im)))))
57.932 * * * * [points]: Sampling 8000 additional inputs, on iter 0 have 0 / 8000
57.956 * * * * [points]: Computing exacts on every 500 of 8000 points to ramp up precision
57.957 * * * * [points]: Setting MPFR precision to 64
57.958 * * * * [points]: Setting MPFR precision to 320
57.959 * * * * [points]: Computing exacts on every 250 of 8000 points to ramp up precision
57.961 * * * * [points]: Setting MPFR precision to 64
57.964 * * * * [points]: Setting MPFR precision to 320
57.968 * * * * [points]: Computing exacts on every 125 of 8000 points to ramp up precision
57.970 * * * * [points]: Setting MPFR precision to 64
57.976 * * * * [points]: Setting MPFR precision to 320
57.982 * * * * [points]: Computing exacts on every 62 of 8000 points to ramp up precision
57.985 * * * * [points]: Setting MPFR precision to 64
57.994 * * * * [points]: Setting MPFR precision to 320
58.001 * * * * [points]: Computing exacts on every 31 of 8000 points to ramp up precision
58.003 * * * * [points]: Setting MPFR precision to 64
58.050 * * * * [points]: Setting MPFR precision to 320
58.071 * * * * [points]: Computing exacts on every 15 of 8000 points to ramp up precision
58.073 * * * * [points]: Setting MPFR precision to 64
58.102 * * * * [points]: Setting MPFR precision to 320
58.134 * * * * [points]: Computing exacts on every 7 of 8000 points to ramp up precision
58.135 * * * * [points]: Setting MPFR precision to 64
58.253 * * * * [points]: Setting MPFR precision to 320
58.333 * * * * [points]: Computing exacts on every 3 of 8000 points to ramp up precision
58.336 * * * * [points]: Setting MPFR precision to 64
58.939 * * * * [points]: Setting MPFR precision to 320
59.182 * * * * [points]: Computing exacts for 8000 points
59.184 * * * * [points]: Setting MPFR precision to 64
60.170 * * * * [points]: Setting MPFR precision to 320
61.095 * * * * [points]: Filtering points with unrepresentable outputs
61.126 * * * * [points]: Sampled 8000 points with exact outputs
65.236 * [regime-testing]: Baseline error score: 0.32959027867747337
65.238 * [regime-testing]: Oracle error score: 0.035725464900548856
65.243 * [regime-testing]: End program error score: 0.32959027867747337