0.002 * [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.004 * * * * [points]: Computing exacts on every 16 of 256 points to ramp up precision 0.005 * * * * [points]: Setting MPFR precision to 64 0.006 * * * * [points]: Setting MPFR precision to 320 0.007 * * * * [points]: Computing exacts on every 8 of 256 points to ramp up precision 0.007 * * * * [points]: Setting MPFR precision to 64 0.009 * * * * [points]: Setting MPFR precision to 320 0.011 * * * * [points]: Computing exacts on every 4 of 256 points to ramp up precision 0.012 * * * * [points]: Setting MPFR precision to 64 0.015 * * * * [points]: Setting MPFR precision to 320 0.019 * * * * [points]: Computing exacts on every 2 of 256 points to ramp up precision 0.020 * * * * [points]: Setting MPFR precision to 64 0.026 * * * * [points]: Setting MPFR precision to 320 0.032 * * * * [points]: Computing exacts for 256 points 0.033 * * * * [points]: Setting MPFR precision to 64 0.050 * * * * [points]: Setting MPFR precision to 320 0.078 * * * * [points]: Filtering points with unrepresentable outputs 0.079 * * * * [points]: Sampled 256 points with exact outputs 0.079 * * * [progress]: [2/2] Setting up program. 0.085 * [progress]: [Phase 2 of 3] Improving. 0.085 * * * * [progress]: [ 1 / 1 ] simplifiying candidate # 0.085 * [simplify]: Simplifying (-.p16 (*.p16 x.re y.re) (*.p16 x.im y.im)) 0.085 * * [simplify]: iteration 1: (7 enodes) 0.087 * * [simplify]: iteration 2: (24 enodes) 0.092 * * [simplify]: iteration 3: (50 enodes) 0.104 * * [simplify]: iteration 4: (119 enodes) 0.134 * * [simplify]: iteration 5: (466 enodes) 0.435 * * [simplify]: Extracting #0: cost 1 inf + 0 0.436 * * [simplify]: Extracting #1: cost 48 inf + 0 0.436 * * [simplify]: Extracting #2: cost 268 inf + 0 0.440 * * [simplify]: Extracting #3: cost 485 inf + 16619 0.460 * * [simplify]: Extracting #4: cost 380 inf + 348231 0.516 * * [simplify]: Extracting #5: cost 34 inf + 1030232 0.578 * * [simplify]: Extracting #6: cost 0 inf + 1113444 0.640 * [simplify]: Simplified to (-.p16 (*.p16 y.re x.re) (*.p16 y.im x.im)) 0.640 * * * * [progress]: [ 1 / 1 ] simplifiying candidate # 0.640 * [simplify]: Simplified (2) to (λ (x.re x.im y.re y.im) (-.p16 (*.p16 y.re x.re) (*.p16 y.im x.im))) 0.647 * * [progress]: iteration 1 / 4 0.647 * * * [progress]: picking best candidate 0.653 * * * * [pick]: Picked # 0.653 * * * [progress]: localizing error 0.719 * * * [progress]: generating rewritten candidates 0.719 * * * * [progress]: [ 1 / 1 ] rewriting at (2) 0.722 * * * [progress]: generating series expansions 0.722 * * * * [progress]: [ 1 / 1 ] generating series at (2) 0.722 * * * [progress]: simplifying candidates 0.722 * * * * [progress]: [ 1 / 3 ] simplifiying candidate # 0.722 * * * * [progress]: [ 2 / 3 ] simplifiying candidate # 0.722 * * * * [progress]: [ 3 / 3 ] simplifiying candidate # 0.723 * [simplify]: Simplifying (neg.p16 (*.p16 x.im y.im)), (-.p16 (*.p16 (*.p16 x.re y.re) (*.p16 x.re y.re)) (*.p16 (*.p16 x.im y.im) (*.p16 x.im y.im))), (+.p16 (*.p16 x.re y.re) (*.p16 x.im y.im)), (-.p16 (*.p16 x.re y.re) (*.p16 x.im y.im)) 0.723 * * [simplify]: iteration 1: (12 enodes) 0.726 * * [simplify]: iteration 2: (41 enodes) 0.736 * * [simplify]: iteration 3: (103 enodes) 0.771 * * [simplify]: iteration 4: (379 enodes) 1.031 * * [simplify]: Extracting #0: cost 4 inf + 0 1.032 * * [simplify]: Extracting #1: cost 95 inf + 0 1.033 * * [simplify]: Extracting #2: cost 330 inf + 0 1.038 * * [simplify]: Extracting #3: cost 495 inf + 53575 1.062 * * [simplify]: Extracting #4: cost 273 inf + 483366 1.121 * * [simplify]: Extracting #5: cost 13 inf + 1029919 1.170 * * [simplify]: Extracting #6: cost 0 inf + 1051197 1.230 * [simplify]: Simplified to (neg.p16 (*.p16 y.im x.im)), (*.p16 (+.p16 (*.p16 y.im x.im) (*.p16 x.re y.re)) (-.p16 (*.p16 x.re y.re) (*.p16 y.im x.im))), (+.p16 (*.p16 y.im x.im) (*.p16 x.re y.re)), (-.p16 (*.p16 x.re y.re) (*.p16 y.im x.im)) 1.230 * * * * [progress]: [ 1 / 3 ] simplifiying candidate # 1.230 * [simplify]: Simplified (2 2) to (λ (x.re x.im y.re y.im) (+.p16 (*.p16 x.re y.re) (neg.p16 (*.p16 y.im x.im)))) 1.230 * * * * [progress]: [ 2 / 3 ] simplifiying candidate # 1.230 * [simplify]: Simplified (2 1) to (λ (x.re x.im y.re y.im) (/.p16 (*.p16 (+.p16 (*.p16 y.im x.im) (*.p16 x.re y.re)) (-.p16 (*.p16 x.re y.re) (*.p16 y.im x.im))) (+.p16 (*.p16 x.re y.re) (*.p16 x.im y.im)))) 1.230 * [simplify]: Simplified (2 2) to (λ (x.re x.im y.re y.im) (/.p16 (-.p16 (*.p16 (*.p16 x.re y.re) (*.p16 x.re y.re)) (*.p16 (*.p16 x.im y.im) (*.p16 x.im y.im))) (+.p16 (*.p16 y.im x.im) (*.p16 x.re y.re)))) 1.230 * * * * [progress]: [ 3 / 3 ] simplifiying candidate # 1.230 * [simplify]: Simplified (2) to (λ (x.re x.im y.re y.im) (-.p16 (*.p16 x.re y.re) (*.p16 y.im x.im))) 1.230 * * * [progress]: adding candidates to table 1.283 * * [progress]: iteration 2 / 4 1.283 * * * [progress]: picking best candidate 1.291 * * * * [pick]: Picked # 1.291 * * * [progress]: localizing error 1.465 * * * [progress]: generating rewritten candidates 1.465 * * * * [progress]: [ 1 / 4 ] rewriting at (2) 1.471 * * * * [progress]: [ 2 / 4 ] rewriting at (2 2) 1.474 * * * * [progress]: [ 3 / 4 ] rewriting at (2 1) 1.483 * * * * [progress]: [ 4 / 4 ] rewriting at (2 1 2) 1.491 * * * [progress]: generating series expansions 1.491 * * * * [progress]: [ 1 / 4 ] generating series at (2) 1.491 * * * * [progress]: [ 2 / 4 ] generating series at (2 2) 1.491 * * * * [progress]: [ 3 / 4 ] generating series at (2 1) 1.491 * * * * [progress]: [ 4 / 4 ] generating series at (2 1 2) 1.492 * * * [progress]: simplifying candidates 1.492 * * * * [progress]: [ 1 / 13 ] simplifiying candidate # 1.492 * * * * [progress]: [ 2 / 13 ] simplifiying candidate # 1.492 * * * * [progress]: [ 3 / 13 ] simplifiying candidate # 1.492 * * * * [progress]: [ 4 / 13 ] simplifiying candidate # 1.492 * * * * [progress]: [ 5 / 13 ] simplifiying candidate # 1.492 * * * * [progress]: [ 6 / 13 ] simplifiying candidate # 1.492 * * * * [progress]: [ 7 / 13 ] simplifiying candidate # 1.492 * * * * [progress]: [ 8 / 13 ] simplifiying candidate # 1.492 * * * * [progress]: [ 9 / 13 ] simplifiying candidate # 1.492 * * * * [progress]: [ 10 / 13 ] simplifiying candidate # 1.492 * * * * [progress]: [ 11 / 13 ] simplifiying candidate # 1.492 * * * * [progress]: [ 12 / 13 ] simplifiying candidate # 1.492 * * * * [progress]: [ 13 / 13 ] simplifiying candidate # 1.493 * [simplify]: Simplifying (/.p16 (+.p16 (*.p16 x.re y.re) (*.p16 x.im y.im)) (-.p16 (*.p16 x.re y.re) (*.p16 x.im y.im))), (*.p16 (+.p16 (*.p16 x.re y.re) (*.p16 x.im y.im)) (+.p16 (*.p16 (*.p16 x.re y.re) (*.p16 x.re y.re)) (*.p16 (*.p16 x.im y.im) (*.p16 x.im y.im)))), (+.p16 (*.p16 x.re y.re) (*.p16 x.im y.im)), (-.p16 (*.p16 x.re y.re) (*.p16 x.im y.im)), (neg.p16 (*.p16 (*.p16 x.im y.im) (*.p16 x.im y.im))), (-.p16 (*.p16 (*.p16 (*.p16 x.re y.re) (*.p16 x.re y.re)) (*.p16 (*.p16 x.re y.re) (*.p16 x.re y.re))) (*.p16 (*.p16 (*.p16 x.im y.im) (*.p16 x.im y.im)) (*.p16 (*.p16 x.im y.im) (*.p16 x.im y.im)))), (+.p16 (*.p16 (*.p16 x.re y.re) (*.p16 x.re y.re)) (*.p16 (*.p16 x.im y.im) (*.p16 x.im y.im))), (*.p16 (*.p16 x.im y.im) x.im), (*.p16 y.im (*.p16 x.im y.im)), (-.p16 (*.p16 (*.p16 x.re y.re) (*.p16 x.re y.re)) (*.p16 (*.p16 x.im y.im) (*.p16 x.im y.im))), (+.p16 (*.p16 x.re y.re) (*.p16 x.im y.im)), (-.p16 (*.p16 (*.p16 x.re y.re) (*.p16 x.re y.re)) (*.p16 (*.p16 x.im y.im) (*.p16 x.im y.im))), (+.p16 (*.p16 x.re y.re) (*.p16 x.im y.im)), (-.p16 (*.p16 (*.p16 x.re y.re) (*.p16 x.re y.re)) (*.p16 (*.p16 x.im y.im) (*.p16 x.im y.im))), (+.p16 (*.p16 x.re y.re) (*.p16 x.im y.im)), (-.p16 (*.p16 (*.p16 x.re y.re) (*.p16 x.re y.re)) (*.p16 (*.p16 x.im y.im) (*.p16 x.im y.im))), (+.p16 (*.p16 x.re y.re) (*.p16 x.im y.im)) 1.493 * * [simplify]: iteration 1: (20 enodes) 1.499 * * [simplify]: iteration 2: (71 enodes) 1.522 * * [simplify]: iteration 3: (228 enodes) 1.606 * * [simplify]: Extracting #0: cost 10 inf + 0 1.607 * * [simplify]: Extracting #1: cost 107 inf + 0 1.607 * * [simplify]: Extracting #2: cost 232 inf + 324 1.611 * * [simplify]: Extracting #3: cost 219 inf + 115852 1.629 * * [simplify]: Extracting #4: cost 73 inf + 410500 1.657 * * [simplify]: Extracting #5: cost 0 inf + 551566 1.686 * [simplify]: Simplified to (/.p16 (+.p16 (*.p16 y.im x.im) (*.p16 y.re x.re)) (-.p16 (*.p16 y.re x.re) (*.p16 y.im x.im))), (*.p16 (+.p16 (*.p16 y.im x.im) (*.p16 y.re x.re)) (+.p16 (*.p16 (*.p16 y.im x.im) (*.p16 y.im x.im)) (*.p16 (*.p16 y.re x.re) (*.p16 y.re x.re)))), (+.p16 (*.p16 y.im x.im) (*.p16 y.re x.re)), (-.p16 (*.p16 y.re x.re) (*.p16 y.im x.im)), (neg.p16 (*.p16 (*.p16 y.im x.im) (*.p16 y.im x.im))), (-.p16 (*.p16 (*.p16 (*.p16 y.re x.re) (*.p16 y.re x.re)) (*.p16 (*.p16 y.re x.re) (*.p16 y.re x.re))) (*.p16 (*.p16 (*.p16 y.im x.im) (*.p16 y.im x.im)) (*.p16 (*.p16 y.im x.im) (*.p16 y.im x.im)))), (+.p16 (*.p16 (*.p16 y.im x.im) (*.p16 y.im x.im)) (*.p16 (*.p16 y.re x.re) (*.p16 y.re x.re))), (*.p16 y.im (*.p16 x.im x.im)), (*.p16 x.im (*.p16 y.im y.im)), (*.p16 (+.p16 (*.p16 y.im x.im) (*.p16 y.re x.re)) (-.p16 (*.p16 y.re x.re) (*.p16 y.im x.im))), (+.p16 (*.p16 y.im x.im) (*.p16 y.re x.re)), (*.p16 (+.p16 (*.p16 y.im x.im) (*.p16 y.re x.re)) (-.p16 (*.p16 y.re x.re) (*.p16 y.im x.im))), (+.p16 (*.p16 y.im x.im) (*.p16 y.re x.re)), (*.p16 (+.p16 (*.p16 y.im x.im) (*.p16 y.re x.re)) (-.p16 (*.p16 y.re x.re) (*.p16 y.im x.im))), (+.p16 (*.p16 y.im x.im) (*.p16 y.re x.re)), (*.p16 (+.p16 (*.p16 y.im x.im) (*.p16 y.re x.re)) (-.p16 (*.p16 y.re x.re) (*.p16 y.im x.im))), (+.p16 (*.p16 y.im x.im) (*.p16 y.re x.re)) 1.686 * * * * [progress]: [ 1 / 13 ] simplifiying candidate # 1.686 * [simplify]: Simplified (2 2) to (λ (x.re x.im y.re y.im) (/.p16 (+.p16 (*.p16 x.re y.re) (*.p16 x.im y.im)) (/.p16 (+.p16 (*.p16 y.im x.im) (*.p16 y.re x.re)) (-.p16 (*.p16 y.re x.re) (*.p16 y.im x.im))))) 1.686 * * * * [progress]: [ 2 / 13 ] simplifiying candidate # 1.686 * [simplify]: Simplified (2 2) to (λ (x.re x.im y.re y.im) (/.p16 (-.p16 (*.p16 (*.p16 (*.p16 x.re y.re) (*.p16 x.re y.re)) (*.p16 (*.p16 x.re y.re) (*.p16 x.re y.re))) (*.p16 (*.p16 (*.p16 x.im y.im) (*.p16 x.im y.im)) (*.p16 (*.p16 x.im y.im) (*.p16 x.im y.im)))) (*.p16 (+.p16 (*.p16 y.im x.im) (*.p16 y.re x.re)) (+.p16 (*.p16 (*.p16 y.im x.im) (*.p16 y.im x.im)) (*.p16 (*.p16 y.re x.re) (*.p16 y.re x.re)))))) 1.686 * * * * [progress]: [ 3 / 13 ] simplifiying candidate # 1.686 * * * * [progress]: [ 4 / 13 ] simplifiying candidate # 1.686 * [simplify]: Simplified (2 1 1) to (λ (x.re x.im y.re y.im) (/.p16 (*.p16 (+.p16 (*.p16 y.im x.im) (*.p16 y.re x.re)) (-.p16 (*.p16 x.re y.re) (*.p16 x.im y.im))) (+.p16 (*.p16 x.re y.re) (*.p16 x.im y.im)))) 1.686 * [simplify]: Simplified (2 1 2) to (λ (x.re x.im y.re y.im) (/.p16 (*.p16 (+.p16 (*.p16 x.re y.re) (*.p16 x.im y.im)) (-.p16 (*.p16 y.re x.re) (*.p16 y.im x.im))) (+.p16 (*.p16 x.re y.re) (*.p16 x.im y.im)))) 1.686 * * * * [progress]: [ 5 / 13 ] simplifiying candidate # 1.686 * [simplify]: Simplified (2 1 2) to (λ (x.re x.im y.re y.im) (/.p16 (+.p16 (*.p16 (*.p16 x.re y.re) (*.p16 x.re y.re)) (neg.p16 (*.p16 (*.p16 y.im x.im) (*.p16 y.im x.im)))) (+.p16 (*.p16 x.re y.re) (*.p16 x.im y.im)))) 1.687 * * * * [progress]: [ 6 / 13 ] simplifiying candidate # 1.687 * [simplify]: Simplified (2 1 1) to (λ (x.re x.im y.re y.im) (/.p16 (/.p16 (-.p16 (*.p16 (*.p16 (*.p16 y.re x.re) (*.p16 y.re x.re)) (*.p16 (*.p16 y.re x.re) (*.p16 y.re x.re))) (*.p16 (*.p16 (*.p16 y.im x.im) (*.p16 y.im x.im)) (*.p16 (*.p16 y.im x.im) (*.p16 y.im x.im)))) (+.p16 (*.p16 (*.p16 x.re y.re) (*.p16 x.re y.re)) (*.p16 (*.p16 x.im y.im) (*.p16 x.im y.im)))) (+.p16 (*.p16 x.re y.re) (*.p16 x.im y.im)))) 1.687 * [simplify]: Simplified (2 1 2) to (λ (x.re x.im y.re y.im) (/.p16 (/.p16 (-.p16 (*.p16 (*.p16 (*.p16 x.re y.re) (*.p16 x.re y.re)) (*.p16 (*.p16 x.re y.re) (*.p16 x.re y.re))) (*.p16 (*.p16 (*.p16 x.im y.im) (*.p16 x.im y.im)) (*.p16 (*.p16 x.im y.im) (*.p16 x.im y.im)))) (+.p16 (*.p16 (*.p16 y.im x.im) (*.p16 y.im x.im)) (*.p16 (*.p16 y.re x.re) (*.p16 y.re x.re)))) (+.p16 (*.p16 x.re y.re) (*.p16 x.im y.im)))) 1.687 * * * * [progress]: [ 7 / 13 ] simplifiying candidate # 1.687 * [simplify]: Simplified (2 1 2 1) to (λ (x.re x.im y.re y.im) (/.p16 (-.p16 (*.p16 (*.p16 x.re y.re) (*.p16 x.re y.re)) (*.p16 (*.p16 y.im (*.p16 x.im x.im)) y.im)) (+.p16 (*.p16 x.re y.re) (*.p16 x.im y.im)))) 1.687 * * * * [progress]: [ 8 / 13 ] simplifiying candidate # 1.687 * [simplify]: Simplified (2 1 2 2) to (λ (x.re x.im y.re y.im) (/.p16 (-.p16 (*.p16 (*.p16 x.re y.re) (*.p16 x.re y.re)) (*.p16 x.im (*.p16 x.im (*.p16 y.im y.im)))) (+.p16 (*.p16 x.re y.re) (*.p16 x.im y.im)))) 1.687 * * * * [progress]: [ 9 / 13 ] simplifiying candidate # 1.687 * * * * [progress]: [ 10 / 13 ] simplifiying candidate # 1.687 * [simplify]: Simplified (2 1) to (λ (x.re x.im y.re y.im) (/.p16 (*.p16 (+.p16 (*.p16 y.im x.im) (*.p16 y.re x.re)) (-.p16 (*.p16 y.re x.re) (*.p16 y.im x.im))) (+.p16 (*.p16 x.re y.re) (*.p16 x.im y.im)))) 1.687 * [simplify]: Simplified (2 2) to (λ (x.re x.im y.re y.im) (/.p16 (-.p16 (*.p16 (*.p16 x.re y.re) (*.p16 x.re y.re)) (*.p16 (*.p16 x.im y.im) (*.p16 x.im y.im))) (+.p16 (*.p16 y.im x.im) (*.p16 y.re x.re)))) 1.687 * * * * [progress]: [ 11 / 13 ] simplifiying candidate # 1.688 * [simplify]: Simplified (2 1) to (λ (x.re x.im y.re y.im) (/.p16 (*.p16 (+.p16 (*.p16 y.im x.im) (*.p16 y.re x.re)) (-.p16 (*.p16 y.re x.re) (*.p16 y.im x.im))) (+.p16 (*.p16 x.re y.re) (*.p16 x.im y.im)))) 1.688 * [simplify]: Simplified (2 2) to (λ (x.re x.im y.re y.im) (/.p16 (-.p16 (*.p16 (*.p16 x.re y.re) (*.p16 x.re y.re)) (*.p16 (*.p16 x.im y.im) (*.p16 x.im y.im))) (+.p16 (*.p16 y.im x.im) (*.p16 y.re x.re)))) 1.688 * * * * [progress]: [ 12 / 13 ] simplifiying candidate # 1.688 * [simplify]: Simplified (2 1) to (λ (x.re x.im y.re y.im) (/.p16 (*.p16 (+.p16 (*.p16 y.im x.im) (*.p16 y.re x.re)) (-.p16 (*.p16 y.re x.re) (*.p16 y.im x.im))) (+.p16 (*.p16 x.re y.re) (*.p16 x.im y.im)))) 1.688 * [simplify]: Simplified (2 2) to (λ (x.re x.im y.re y.im) (/.p16 (-.p16 (*.p16 (*.p16 x.re y.re) (*.p16 x.re y.re)) (*.p16 (*.p16 x.im y.im) (*.p16 x.im y.im))) (+.p16 (*.p16 y.im x.im) (*.p16 y.re x.re)))) 1.688 * * * * [progress]: [ 13 / 13 ] simplifiying candidate # 1.688 * [simplify]: Simplified (2 1) to (λ (x.re x.im y.re y.im) (/.p16 (*.p16 (+.p16 (*.p16 y.im x.im) (*.p16 y.re x.re)) (-.p16 (*.p16 y.re x.re) (*.p16 y.im x.im))) (+.p16 (*.p16 x.re y.re) (*.p16 x.im y.im)))) 1.688 * [simplify]: Simplified (2 2) to (λ (x.re x.im y.re y.im) (/.p16 (-.p16 (*.p16 (*.p16 x.re y.re) (*.p16 x.re y.re)) (*.p16 (*.p16 x.im y.im) (*.p16 x.im y.im))) (+.p16 (*.p16 y.im x.im) (*.p16 y.re x.re)))) 1.688 * * * [progress]: adding candidates to table 1.899 * * [progress]: iteration 3 / 4 1.899 * * * [progress]: picking best candidate 1.931 * * * * [pick]: Picked # 1.931 * * * [progress]: localizing error 2.075 * * * [progress]: generating rewritten candidates 2.075 * * * * [progress]: [ 1 / 4 ] rewriting at (2 2) 2.077 * * * * [progress]: [ 2 / 4 ] rewriting at (2) 2.080 * * * * [progress]: [ 3 / 4 ] rewriting at (2 2 2) 2.083 * * * * [progress]: [ 4 / 4 ] rewriting at (2 2 1) 2.088 * * * [progress]: generating series expansions 2.088 * * * * [progress]: [ 1 / 4 ] generating series at (2 2) 2.088 * * * * [progress]: [ 2 / 4 ] generating series at (2) 2.088 * * * * [progress]: [ 3 / 4 ] generating series at (2 2 2) 2.088 * * * * [progress]: [ 4 / 4 ] generating series at (2 2 1) 2.088 * * * [progress]: simplifying candidates 2.088 * * * * [progress]: [ 1 / 10 ] simplifiying candidate # 2.089 * * * * [progress]: [ 2 / 10 ] simplifiying candidate # 2.089 * * * * [progress]: [ 3 / 10 ] simplifiying candidate # 2.089 * * * * [progress]: [ 4 / 10 ] simplifiying candidate # 2.089 * * * * [progress]: [ 5 / 10 ] simplifiying candidate # 2.089 * * * * [progress]: [ 6 / 10 ] simplifiying candidate # 2.089 * * * * [progress]: [ 7 / 10 ] simplifiying candidate # 2.089 * * * * [progress]: [ 8 / 10 ] simplifiying candidate # 2.089 * * * * [progress]: [ 9 / 10 ] simplifiying candidate # 2.089 * * * * [progress]: [ 10 / 10 ] simplifiying candidate # 2.089 * [simplify]: Simplifying (/.p16 (+.p16 (*.p16 x.re y.re) (*.p16 x.im y.im)) (-.p16 (*.p16 (*.p16 x.re y.re) (*.p16 x.re y.re)) (*.p16 (*.p16 x.im y.im) (*.p16 x.im y.im)))), (/.p16 (+.p16 (*.p16 x.re y.re) (*.p16 x.im y.im)) (/.p16 (+.p16 (*.p16 x.re y.re) (*.p16 x.im y.im)) (-.p16 (*.p16 (*.p16 x.re y.re) (*.p16 x.re y.re)) (*.p16 (*.p16 x.im y.im) (*.p16 x.im y.im))))), (/.p16 (+.p16 (*.p16 x.re y.re) (*.p16 x.im y.im)) (+.p16 (*.p16 x.re y.re) (*.p16 x.im y.im))), (neg.p16 (*.p16 x.im y.im)), (-.p16 (*.p16 (*.p16 x.re y.re) (*.p16 x.re y.re)) (*.p16 (*.p16 x.im y.im) (*.p16 x.im y.im))), (+.p16 (*.p16 x.re y.re) (*.p16 x.im y.im)), (/.p16 (+.p16 (*.p16 x.re y.re) (*.p16 x.im y.im)) (-.p16 (*.p16 x.re y.re) (*.p16 x.im y.im))), (/.p16 (+.p16 (*.p16 x.re y.re) (*.p16 x.im y.im)) (-.p16 (*.p16 x.re y.re) (*.p16 x.im y.im))), (/.p16 (+.p16 (*.p16 x.re y.re) (*.p16 x.im y.im)) (-.p16 (*.p16 x.re y.re) (*.p16 x.im y.im))), (/.p16 (+.p16 (*.p16 x.re y.re) (*.p16 x.im y.im)) (-.p16 (*.p16 x.re y.re) (*.p16 x.im y.im))) 2.090 * * [simplify]: iteration 1: (16 enodes) 2.095 * * [simplify]: iteration 2: (48 enodes) 2.107 * * [simplify]: iteration 3: (125 enodes) 2.173 * * [simplify]: iteration 4: (571 enodes) 3.293 * * [simplify]: Extracting #0: cost 6 inf + 0 3.294 * * [simplify]: Extracting #1: cost 211 inf + 0 3.297 * * [simplify]: Extracting #2: cost 797 inf + 1 3.302 * * [simplify]: Extracting #3: cost 1127 inf + 6791 3.311 * * [simplify]: Extracting #4: cost 1121 inf + 168672 3.349 * * [simplify]: Extracting #5: cost 499 inf + 1104125 3.418 * * [simplify]: Extracting #6: cost 105 inf + 1873539 3.542 * * [simplify]: Extracting #7: cost 1 inf + 2140973 3.675 * * [simplify]: Extracting #8: cost 0 inf + 2144457 3.773 * [simplify]: Simplified to (/.p16 (real->posit16 1.0) (-.p16 (*.p16 x.re y.re) (*.p16 y.im x.im))), (*.p16 (+.p16 (*.p16 y.im x.im) (*.p16 x.re y.re)) (-.p16 (*.p16 x.re y.re) (*.p16 y.im x.im))), (real->posit16 1.0), (neg.p16 (*.p16 y.im x.im)), (*.p16 (+.p16 (*.p16 y.im x.im) (*.p16 x.re y.re)) (-.p16 (*.p16 x.re y.re) (*.p16 y.im x.im))), (+.p16 (*.p16 y.im x.im) (*.p16 x.re y.re)), (/.p16 (+.p16 (*.p16 y.im x.im) (*.p16 x.re y.re)) (-.p16 (*.p16 x.re y.re) (*.p16 y.im x.im))), (/.p16 (+.p16 (*.p16 y.im x.im) (*.p16 x.re y.re)) (-.p16 (*.p16 x.re y.re) (*.p16 y.im x.im))), (/.p16 (+.p16 (*.p16 y.im x.im) (*.p16 x.re y.re)) (-.p16 (*.p16 x.re y.re) (*.p16 y.im x.im))), (/.p16 (+.p16 (*.p16 y.im x.im) (*.p16 x.re y.re)) (-.p16 (*.p16 x.re y.re) (*.p16 y.im x.im))) 3.773 * * * * [progress]: [ 1 / 10 ] simplifiying candidate # 3.773 * [simplify]: Simplified (2 2 1) to (λ (x.re x.im y.re y.im) (/.p16 (+.p16 (*.p16 x.re y.re) (*.p16 x.im y.im)) (*.p16 (/.p16 (real->posit16 1.0) (-.p16 (*.p16 x.re y.re) (*.p16 y.im x.im))) (+.p16 (*.p16 x.re y.re) (*.p16 x.im y.im))))) 3.773 * * * * [progress]: [ 2 / 10 ] simplifiying candidate # 3.774 * [simplify]: Simplified (2 1) to (λ (x.re x.im y.re y.im) (/.p16 (*.p16 (+.p16 (*.p16 y.im x.im) (*.p16 x.re y.re)) (-.p16 (*.p16 x.re y.re) (*.p16 y.im x.im))) (+.p16 (*.p16 x.re y.re) (*.p16 x.im y.im)))) 3.774 * * * * [progress]: [ 3 / 10 ] simplifiying candidate # 3.774 * [simplify]: Simplified (2 1) to (λ (x.re x.im y.re y.im) (*.p16 (real->posit16 1.0) (-.p16 (*.p16 x.re y.re) (*.p16 x.im y.im)))) 3.774 * * * * [progress]: [ 4 / 10 ] simplifiying candidate # 3.774 * [simplify]: Simplified (2 2 2 2) to (λ (x.re x.im y.re y.im) (/.p16 (+.p16 (*.p16 x.re y.re) (*.p16 x.im y.im)) (/.p16 (+.p16 (*.p16 x.re y.re) (*.p16 x.im y.im)) (+.p16 (*.p16 x.re y.re) (neg.p16 (*.p16 y.im x.im)))))) 3.774 * * * * [progress]: [ 5 / 10 ] simplifiying candidate # 3.774 * [simplify]: Simplified (2 2 2 1) to (λ (x.re x.im y.re y.im) (/.p16 (+.p16 (*.p16 x.re y.re) (*.p16 x.im y.im)) (/.p16 (+.p16 (*.p16 x.re y.re) (*.p16 x.im y.im)) (/.p16 (*.p16 (+.p16 (*.p16 y.im x.im) (*.p16 x.re y.re)) (-.p16 (*.p16 x.re y.re) (*.p16 y.im x.im))) (+.p16 (*.p16 x.re y.re) (*.p16 x.im y.im)))))) 3.774 * [simplify]: Simplified (2 2 2 2) to (λ (x.re x.im y.re y.im) (/.p16 (+.p16 (*.p16 x.re y.re) (*.p16 x.im y.im)) (/.p16 (+.p16 (*.p16 x.re y.re) (*.p16 x.im y.im)) (/.p16 (-.p16 (*.p16 (*.p16 x.re y.re) (*.p16 x.re y.re)) (*.p16 (*.p16 x.im y.im) (*.p16 x.im y.im))) (+.p16 (*.p16 y.im x.im) (*.p16 x.re y.re)))))) 3.774 * * * * [progress]: [ 6 / 10 ] simplifiying candidate # 3.774 * * * * [progress]: [ 7 / 10 ] simplifiying candidate # 3.774 * [simplify]: Simplified (2 2) to (λ (x.re x.im y.re y.im) (/.p16 (+.p16 (*.p16 x.re y.re) (*.p16 x.im y.im)) (/.p16 (+.p16 (*.p16 y.im x.im) (*.p16 x.re y.re)) (-.p16 (*.p16 x.re y.re) (*.p16 y.im x.im))))) 3.774 * * * * [progress]: [ 8 / 10 ] simplifiying candidate # 3.774 * [simplify]: Simplified (2 2) to (λ (x.re x.im y.re y.im) (/.p16 (+.p16 (*.p16 x.re y.re) (*.p16 x.im y.im)) (/.p16 (+.p16 (*.p16 y.im x.im) (*.p16 x.re y.re)) (-.p16 (*.p16 x.re y.re) (*.p16 y.im x.im))))) 3.774 * * * * [progress]: [ 9 / 10 ] simplifiying candidate # 3.774 * [simplify]: Simplified (2 2) to (λ (x.re x.im y.re y.im) (/.p16 (+.p16 (*.p16 x.re y.re) (*.p16 x.im y.im)) (/.p16 (+.p16 (*.p16 y.im x.im) (*.p16 x.re y.re)) (-.p16 (*.p16 x.re y.re) (*.p16 y.im x.im))))) 3.774 * * * * [progress]: [ 10 / 10 ] simplifiying candidate # 3.774 * [simplify]: Simplified (2 2) to (λ (x.re x.im y.re y.im) (/.p16 (+.p16 (*.p16 x.re y.re) (*.p16 x.im y.im)) (/.p16 (+.p16 (*.p16 y.im x.im) (*.p16 x.re y.re)) (-.p16 (*.p16 x.re y.re) (*.p16 y.im x.im))))) 3.774 * * * [progress]: adding candidates to table 3.946 * * [progress]: iteration 4 / 4 3.947 * * * [progress]: picking best candidate 3.998 * * * * [pick]: Picked #posit16 1.0) (-.p16 (*.p16 x.re y.re) (*.p16 y.im x.im))) (+.p16 (*.p16 x.re y.re) (*.p16 x.im y.im)))))> 3.998 * * * [progress]: localizing error 4.258 * * * [progress]: generating rewritten candidates 4.258 * * * * [progress]: [ 1 / 4 ] rewriting at (2 2) 4.262 * * * * [progress]: [ 2 / 4 ] rewriting at (2) 4.266 * * * * [progress]: [ 3 / 4 ] rewriting at (2 2 1) 4.269 * * * * [progress]: [ 4 / 4 ] rewriting at (2 2 1 2) 4.273 * * * [progress]: generating series expansions 4.273 * * * * [progress]: [ 1 / 4 ] generating series at (2 2) 4.273 * * * * [progress]: [ 2 / 4 ] generating series at (2) 4.273 * * * * [progress]: [ 3 / 4 ] generating series at (2 2 1) 4.273 * * * * [progress]: [ 4 / 4 ] generating series at (2 2 1 2) 4.273 * * * [progress]: simplifying candidates 4.273 * * * * [progress]: [ 1 / 14 ] simplifiying candidate #posit16 1.0) (-.p16 (*.p16 x.re y.re) (*.p16 y.im x.im))) (*.p16 x.re y.re)) (*.p16 (/.p16 (real->posit16 1.0) (-.p16 (*.p16 x.re y.re) (*.p16 y.im x.im))) (*.p16 x.im y.im)))))> 4.273 * * * * [progress]: [ 2 / 14 ] simplifiying candidate #posit16 1.0) (-.p16 (*.p16 x.re y.re) (*.p16 y.im x.im)))) (*.p16 (*.p16 x.im y.im) (/.p16 (real->posit16 1.0) (-.p16 (*.p16 x.re y.re) (*.p16 y.im x.im)))))))> 4.273 * * * * [progress]: [ 3 / 14 ] simplifiying candidate #posit16 1.0) (-.p16 (*.p16 (*.p16 x.re y.re) (*.p16 x.re y.re)) (*.p16 (*.p16 y.im x.im) (*.p16 y.im x.im)))) (*.p16 (+.p16 (*.p16 x.re y.re) (*.p16 y.im x.im)) (+.p16 (*.p16 x.re y.re) (*.p16 x.im y.im))))))> 4.273 * * * * [progress]: [ 4 / 14 ] simplifiying candidate #posit16 1.0) (+.p16 (*.p16 x.re y.re) (*.p16 x.im y.im))) (-.p16 (*.p16 x.re y.re) (*.p16 y.im x.im)))))> 4.273 * * * * [progress]: [ 5 / 14 ] simplifiying candidate #posit16 1.0) (-.p16 (*.p16 x.re y.re) (*.p16 y.im x.im))))))> 4.273 * * * * [progress]: [ 6 / 14 ] simplifiying candidate #posit16 1.0) (-.p16 (*.p16 x.re y.re) (*.p16 y.im x.im)))) (+.p16 (*.p16 x.re y.re) (*.p16 x.im y.im))))> 4.273 * * * * [progress]: [ 7 / 14 ] simplifiying candidate #posit16 1.0) (+.p16 (*.p16 x.re y.re) (*.p16 x.im y.im)))) (-.p16 (*.p16 x.re y.re) (*.p16 y.im x.im))))> 4.274 * * * * [progress]: [ 8 / 14 ] simplifiying candidate #posit16 1.0) (-.p16 (*.p16 (*.p16 x.re y.re) (*.p16 x.re y.re)) (*.p16 (*.p16 y.im x.im) (*.p16 y.im x.im)))) (+.p16 (*.p16 x.re y.re) (*.p16 y.im x.im))) (+.p16 (*.p16 x.re y.re) (*.p16 x.im y.im)))))> 4.274 * * * * [progress]: [ 9 / 14 ] simplifiying candidate #posit16 1.0) (+.p16 (*.p16 x.re y.re) (neg.p16 (*.p16 y.im x.im)))) (+.p16 (*.p16 x.re y.re) (*.p16 x.im y.im)))))> 4.274 * * * * [progress]: [ 10 / 14 ] simplifiying candidate #posit16 1.0) (/.p16 (-.p16 (*.p16 (*.p16 x.re y.re) (*.p16 x.re y.re)) (*.p16 (*.p16 y.im x.im) (*.p16 y.im x.im))) (+.p16 (*.p16 x.re y.re) (*.p16 y.im x.im)))) (+.p16 (*.p16 x.re y.re) (*.p16 x.im y.im)))))> 4.274 * * * * [progress]: [ 11 / 14 ] simplifiying candidate #posit16 1.0) (-.p16 (*.p16 x.re y.re) (*.p16 y.im x.im))) (+.p16 (*.p16 x.re y.re) (*.p16 x.im y.im)))))> 4.274 * * * * [progress]: [ 12 / 14 ] simplifiying candidate #posit16 1.0) (-.p16 (*.p16 x.re y.re) (*.p16 y.im x.im))) (+.p16 (*.p16 x.re y.re) (*.p16 x.im y.im)))))> 4.274 * * * * [progress]: [ 13 / 14 ] simplifiying candidate #posit16 1.0) (-.p16 (*.p16 x.re y.re) (*.p16 y.im x.im))) (+.p16 (*.p16 x.re y.re) (*.p16 x.im y.im)))))> 4.274 * * * * [progress]: [ 14 / 14 ] simplifiying candidate #posit16 1.0) (-.p16 (*.p16 x.re y.re) (*.p16 y.im x.im))) (+.p16 (*.p16 x.re y.re) (*.p16 x.im y.im)))))> 4.274 * [simplify]: Simplifying (*.p16 (/.p16 (real->posit16 1.0) (-.p16 (*.p16 x.re y.re) (*.p16 y.im x.im))) (*.p16 x.re y.re)), (*.p16 (/.p16 (real->posit16 1.0) (-.p16 (*.p16 x.re y.re) (*.p16 y.im x.im))) (*.p16 x.im y.im)), (*.p16 (*.p16 x.re y.re) (/.p16 (real->posit16 1.0) (-.p16 (*.p16 x.re y.re) (*.p16 y.im x.im)))), (*.p16 (*.p16 x.im y.im) (/.p16 (real->posit16 1.0) (-.p16 (*.p16 x.re y.re) (*.p16 y.im x.im)))), (*.p16 (+.p16 (*.p16 x.re y.re) (*.p16 y.im x.im)) (+.p16 (*.p16 x.re y.re) (*.p16 x.im y.im))), (*.p16 (real->posit16 1.0) (+.p16 (*.p16 x.re y.re) (*.p16 x.im y.im))), (/.p16 (+.p16 (*.p16 x.re y.re) (*.p16 x.im y.im)) (/.p16 (real->posit16 1.0) (-.p16 (*.p16 x.re y.re) (*.p16 y.im x.im)))), (/.p16 (+.p16 (*.p16 x.re y.re) (*.p16 x.im y.im)) (*.p16 (real->posit16 1.0) (+.p16 (*.p16 x.re y.re) (*.p16 x.im y.im)))), (/.p16 (real->posit16 1.0) (-.p16 (*.p16 (*.p16 x.re y.re) (*.p16 x.re y.re)) (*.p16 (*.p16 y.im x.im) (*.p16 y.im x.im)))), (neg.p16 (*.p16 y.im x.im)), (-.p16 (*.p16 (*.p16 x.re y.re) (*.p16 x.re y.re)) (*.p16 (*.p16 y.im x.im) (*.p16 y.im x.im))), (+.p16 (*.p16 x.re y.re) (*.p16 y.im x.im)), (/.p16 (+.p16 (*.p16 x.re y.re) (*.p16 x.im y.im)) (*.p16 (/.p16 (real->posit16 1.0) (-.p16 (*.p16 x.re y.re) (*.p16 y.im x.im))) (+.p16 (*.p16 x.re y.re) (*.p16 x.im y.im)))), (/.p16 (+.p16 (*.p16 x.re y.re) (*.p16 x.im y.im)) (*.p16 (/.p16 (real->posit16 1.0) (-.p16 (*.p16 x.re y.re) (*.p16 y.im x.im))) (+.p16 (*.p16 x.re y.re) (*.p16 x.im y.im)))), (/.p16 (+.p16 (*.p16 x.re y.re) (*.p16 x.im y.im)) (*.p16 (/.p16 (real->posit16 1.0) (-.p16 (*.p16 x.re y.re) (*.p16 y.im x.im))) (+.p16 (*.p16 x.re y.re) (*.p16 x.im y.im)))), (/.p16 (+.p16 (*.p16 x.re y.re) (*.p16 x.im y.im)) (*.p16 (/.p16 (real->posit16 1.0) (-.p16 (*.p16 x.re y.re) (*.p16 y.im x.im))) (+.p16 (*.p16 x.re y.re) (*.p16 x.im y.im)))) 4.275 * * [simplify]: iteration 1: (28 enodes) 4.287 * * [simplify]: iteration 2: (92 enodes) 4.341 * * [simplify]: iteration 3: (386 enodes) 5.044 * * [simplify]: Extracting #0: cost 9 inf + 0 5.045 * * [simplify]: Extracting #1: cost 312 inf + 0 5.048 * * [simplify]: Extracting #2: cost 921 inf + 447 5.057 * * [simplify]: Extracting #3: cost 734 inf + 161639 5.087 * * [simplify]: Extracting #4: cost 231 inf + 629095 5.135 * * [simplify]: Extracting #5: cost 8 inf + 951600 5.185 * * [simplify]: Extracting #6: cost 0 inf + 953991 5.238 * [simplify]: Simplified to (/.p16 (*.p16 y.re x.re) (-.p16 (*.p16 y.re x.re) (*.p16 x.im y.im))), (/.p16 (*.p16 x.im y.im) (-.p16 (*.p16 y.re x.re) (*.p16 x.im y.im))), (/.p16 (*.p16 y.re x.re) (-.p16 (*.p16 y.re x.re) (*.p16 x.im y.im))), (/.p16 (*.p16 x.im y.im) (-.p16 (*.p16 y.re x.re) (*.p16 x.im y.im))), (*.p16 (+.p16 (*.p16 x.im y.im) (*.p16 y.re x.re)) (+.p16 (*.p16 x.im y.im) (*.p16 y.re x.re))), (+.p16 (*.p16 x.im y.im) (*.p16 y.re x.re)), (*.p16 (-.p16 (*.p16 y.re x.re) (*.p16 x.im y.im)) (+.p16 (*.p16 x.im y.im) (*.p16 y.re x.re))), (real->posit16 1.0), (/.p16 (real->posit16 1.0) (*.p16 (-.p16 (*.p16 y.re x.re) (*.p16 x.im y.im)) (+.p16 (*.p16 x.im y.im) (*.p16 y.re x.re)))), (neg.p16 (*.p16 x.im y.im)), (*.p16 (-.p16 (*.p16 y.re x.re) (*.p16 x.im y.im)) (+.p16 (*.p16 x.im y.im) (*.p16 y.re x.re))), (+.p16 (*.p16 x.im y.im) (*.p16 y.re x.re)), (-.p16 (*.p16 y.re x.re) (*.p16 x.im y.im)), (-.p16 (*.p16 y.re x.re) (*.p16 x.im y.im)), (-.p16 (*.p16 y.re x.re) (*.p16 x.im y.im)), (-.p16 (*.p16 y.re x.re) (*.p16 x.im y.im)) 5.238 * * * * [progress]: [ 1 / 14 ] simplifiying candidate #posit16 1.0) (-.p16 (*.p16 x.re y.re) (*.p16 y.im x.im))) (*.p16 x.re y.re)) (*.p16 (/.p16 (real->posit16 1.0) (-.p16 (*.p16 x.re y.re) (*.p16 y.im x.im))) (*.p16 x.im y.im)))))> 5.238 * [simplify]: Simplified (2 2 1) to (λ (x.re x.im y.re y.im) (/.p16 (+.p16 (*.p16 x.re y.re) (*.p16 x.im y.im)) (+.p16 (/.p16 (*.p16 y.re x.re) (-.p16 (*.p16 y.re x.re) (*.p16 x.im y.im))) (*.p16 (/.p16 (real->posit16 1.0) (-.p16 (*.p16 x.re y.re) (*.p16 y.im x.im))) (*.p16 x.im y.im))))) 5.238 * [simplify]: Simplified (2 2 2) to (λ (x.re x.im y.re y.im) (/.p16 (+.p16 (*.p16 x.re y.re) (*.p16 x.im y.im)) (+.p16 (*.p16 (/.p16 (real->posit16 1.0) (-.p16 (*.p16 x.re y.re) (*.p16 y.im x.im))) (*.p16 x.re y.re)) (/.p16 (*.p16 x.im y.im) (-.p16 (*.p16 y.re x.re) (*.p16 x.im y.im)))))) 5.238 * * * * [progress]: [ 2 / 14 ] simplifiying candidate #posit16 1.0) (-.p16 (*.p16 x.re y.re) (*.p16 y.im x.im)))) (*.p16 (*.p16 x.im y.im) (/.p16 (real->posit16 1.0) (-.p16 (*.p16 x.re y.re) (*.p16 y.im x.im)))))))> 5.238 * [simplify]: Simplified (2 2 1) to (λ (x.re x.im y.re y.im) (/.p16 (+.p16 (*.p16 x.re y.re) (*.p16 x.im y.im)) (+.p16 (/.p16 (*.p16 y.re x.re) (-.p16 (*.p16 y.re x.re) (*.p16 x.im y.im))) (*.p16 (*.p16 x.im y.im) (/.p16 (real->posit16 1.0) (-.p16 (*.p16 x.re y.re) (*.p16 y.im x.im))))))) 5.239 * [simplify]: Simplified (2 2 2) to (λ (x.re x.im y.re y.im) (/.p16 (+.p16 (*.p16 x.re y.re) (*.p16 x.im y.im)) (+.p16 (*.p16 (*.p16 x.re y.re) (/.p16 (real->posit16 1.0) (-.p16 (*.p16 x.re y.re) (*.p16 y.im x.im)))) (/.p16 (*.p16 x.im y.im) (-.p16 (*.p16 y.re x.re) (*.p16 x.im y.im)))))) 5.239 * * * * [progress]: [ 3 / 14 ] simplifiying candidate #posit16 1.0) (-.p16 (*.p16 (*.p16 x.re y.re) (*.p16 x.re y.re)) (*.p16 (*.p16 y.im x.im) (*.p16 y.im x.im)))) (*.p16 (+.p16 (*.p16 x.re y.re) (*.p16 y.im x.im)) (+.p16 (*.p16 x.re y.re) (*.p16 x.im y.im))))))> 5.239 * [simplify]: Simplified (2 2 2) to (λ (x.re x.im y.re y.im) (/.p16 (+.p16 (*.p16 x.re y.re) (*.p16 x.im y.im)) (*.p16 (/.p16 (real->posit16 1.0) (-.p16 (*.p16 (*.p16 x.re y.re) (*.p16 x.re y.re)) (*.p16 (*.p16 y.im x.im) (*.p16 y.im x.im)))) (*.p16 (+.p16 (*.p16 x.im y.im) (*.p16 y.re x.re)) (+.p16 (*.p16 x.im y.im) (*.p16 y.re x.re)))))) 5.239 * * * * [progress]: [ 4 / 14 ] simplifiying candidate #posit16 1.0) (+.p16 (*.p16 x.re y.re) (*.p16 x.im y.im))) (-.p16 (*.p16 x.re y.re) (*.p16 y.im x.im)))))> 5.239 * [simplify]: Simplified (2 2 1) to (λ (x.re x.im y.re y.im) (/.p16 (+.p16 (*.p16 x.re y.re) (*.p16 x.im y.im)) (/.p16 (+.p16 (*.p16 x.im y.im) (*.p16 y.re x.re)) (-.p16 (*.p16 x.re y.re) (*.p16 y.im x.im))))) 5.239 * * * * [progress]: [ 5 / 14 ] simplifiying candidate #posit16 1.0) (-.p16 (*.p16 x.re y.re) (*.p16 y.im x.im))))))> 5.239 * * * * [progress]: [ 6 / 14 ] simplifiying candidate #posit16 1.0) (-.p16 (*.p16 x.re y.re) (*.p16 y.im x.im)))) (+.p16 (*.p16 x.re y.re) (*.p16 x.im y.im))))> 5.239 * [simplify]: Simplified (2 1) to (λ (x.re x.im y.re y.im) (/.p16 (*.p16 (-.p16 (*.p16 y.re x.re) (*.p16 x.im y.im)) (+.p16 (*.p16 x.im y.im) (*.p16 y.re x.re))) (+.p16 (*.p16 x.re y.re) (*.p16 x.im y.im)))) 5.239 * * * * [progress]: [ 7 / 14 ] simplifiying candidate #posit16 1.0) (+.p16 (*.p16 x.re y.re) (*.p16 x.im y.im)))) (-.p16 (*.p16 x.re y.re) (*.p16 y.im x.im))))> 5.239 * [simplify]: Simplified (2 1) to (λ (x.re x.im y.re y.im) (*.p16 (real->posit16 1.0) (-.p16 (*.p16 x.re y.re) (*.p16 y.im x.im)))) 5.239 * * * * [progress]: [ 8 / 14 ] simplifiying candidate #posit16 1.0) (-.p16 (*.p16 (*.p16 x.re y.re) (*.p16 x.re y.re)) (*.p16 (*.p16 y.im x.im) (*.p16 y.im x.im)))) (+.p16 (*.p16 x.re y.re) (*.p16 y.im x.im))) (+.p16 (*.p16 x.re y.re) (*.p16 x.im y.im)))))> 5.240 * [simplify]: Simplified (2 2 1 1) to (λ (x.re x.im y.re y.im) (/.p16 (+.p16 (*.p16 x.re y.re) (*.p16 x.im y.im)) (*.p16 (*.p16 (/.p16 (real->posit16 1.0) (*.p16 (-.p16 (*.p16 y.re x.re) (*.p16 x.im y.im)) (+.p16 (*.p16 x.im y.im) (*.p16 y.re x.re)))) (+.p16 (*.p16 x.re y.re) (*.p16 y.im x.im))) (+.p16 (*.p16 x.re y.re) (*.p16 x.im y.im))))) 5.240 * * * * [progress]: [ 9 / 14 ] simplifiying candidate #posit16 1.0) (+.p16 (*.p16 x.re y.re) (neg.p16 (*.p16 y.im x.im)))) (+.p16 (*.p16 x.re y.re) (*.p16 x.im y.im)))))> 5.240 * [simplify]: Simplified (2 2 1 2 2) to (λ (x.re x.im y.re y.im) (/.p16 (+.p16 (*.p16 x.re y.re) (*.p16 x.im y.im)) (*.p16 (/.p16 (real->posit16 1.0) (+.p16 (*.p16 x.re y.re) (neg.p16 (*.p16 x.im y.im)))) (+.p16 (*.p16 x.re y.re) (*.p16 x.im y.im))))) 5.240 * * * * [progress]: [ 10 / 14 ] simplifiying candidate #posit16 1.0) (/.p16 (-.p16 (*.p16 (*.p16 x.re y.re) (*.p16 x.re y.re)) (*.p16 (*.p16 y.im x.im) (*.p16 y.im x.im))) (+.p16 (*.p16 x.re y.re) (*.p16 y.im x.im)))) (+.p16 (*.p16 x.re y.re) (*.p16 x.im y.im)))))> 5.240 * [simplify]: Simplified (2 2 1 2 1) to (λ (x.re x.im y.re y.im) (/.p16 (+.p16 (*.p16 x.re y.re) (*.p16 x.im y.im)) (*.p16 (/.p16 (real->posit16 1.0) (/.p16 (*.p16 (-.p16 (*.p16 y.re x.re) (*.p16 x.im y.im)) (+.p16 (*.p16 x.im y.im) (*.p16 y.re x.re))) (+.p16 (*.p16 x.re y.re) (*.p16 y.im x.im)))) (+.p16 (*.p16 x.re y.re) (*.p16 x.im y.im))))) 5.240 * [simplify]: Simplified (2 2 1 2 2) to (λ (x.re x.im y.re y.im) (/.p16 (+.p16 (*.p16 x.re y.re) (*.p16 x.im y.im)) (*.p16 (/.p16 (real->posit16 1.0) (/.p16 (-.p16 (*.p16 (*.p16 x.re y.re) (*.p16 x.re y.re)) (*.p16 (*.p16 y.im x.im) (*.p16 y.im x.im))) (+.p16 (*.p16 x.im y.im) (*.p16 y.re x.re)))) (+.p16 (*.p16 x.re y.re) (*.p16 x.im y.im))))) 5.240 * * * * [progress]: [ 11 / 14 ] simplifiying candidate #posit16 1.0) (-.p16 (*.p16 x.re y.re) (*.p16 y.im x.im))) (+.p16 (*.p16 x.re y.re) (*.p16 x.im y.im)))))> 5.240 * [simplify]: Simplified (2) to (λ (x.re x.im y.re y.im) (-.p16 (*.p16 y.re x.re) (*.p16 x.im y.im))) 5.240 * * * * [progress]: [ 12 / 14 ] simplifiying candidate #posit16 1.0) (-.p16 (*.p16 x.re y.re) (*.p16 y.im x.im))) (+.p16 (*.p16 x.re y.re) (*.p16 x.im y.im)))))> 5.240 * [simplify]: Simplified (2) to (λ (x.re x.im y.re y.im) (-.p16 (*.p16 y.re x.re) (*.p16 x.im y.im))) 5.241 * * * * [progress]: [ 13 / 14 ] simplifiying candidate #posit16 1.0) (-.p16 (*.p16 x.re y.re) (*.p16 y.im x.im))) (+.p16 (*.p16 x.re y.re) (*.p16 x.im y.im)))))> 5.241 * [simplify]: Simplified (2) to (λ (x.re x.im y.re y.im) (-.p16 (*.p16 y.re x.re) (*.p16 x.im y.im))) 5.241 * * * * [progress]: [ 14 / 14 ] simplifiying candidate #posit16 1.0) (-.p16 (*.p16 x.re y.re) (*.p16 y.im x.im))) (+.p16 (*.p16 x.re y.re) (*.p16 x.im y.im)))))> 5.241 * [simplify]: Simplified (2) to (λ (x.re x.im y.re y.im) (-.p16 (*.p16 y.re x.re) (*.p16 x.im y.im))) 5.241 * * * [progress]: adding candidates to table 5.601 * [progress]: [Phase 3 of 3] Extracting. 5.602 * * [regime]: Finding splitpoints for: (# # # #posit16 1.0) (-.p16 (*.p16 x.re y.re) (*.p16 y.im x.im))) (*.p16 x.re y.re)) (*.p16 (/.p16 (real->posit16 1.0) (-.p16 (*.p16 x.re y.re) (*.p16 y.im x.im))) (*.p16 x.im y.im)))))> # # #posit16 1.0) (-.p16 (*.p16 (*.p16 x.re y.re) (*.p16 x.re y.re)) (*.p16 (*.p16 y.im x.im) (*.p16 y.im x.im)))) (*.p16 (+.p16 (*.p16 x.re y.re) (*.p16 y.im x.im)) (+.p16 (*.p16 x.re y.re) (*.p16 x.im y.im))))))>) 5.605 * * * [regime-changes]: Trying 4 branch expressions: (y.im x.im y.re x.re) 5.605 * * * * [regimes]: Trying to branch on y.im from (# # # #posit16 1.0) (-.p16 (*.p16 x.re y.re) (*.p16 y.im x.im))) (*.p16 x.re y.re)) (*.p16 (/.p16 (real->posit16 1.0) (-.p16 (*.p16 x.re y.re) (*.p16 y.im x.im))) (*.p16 x.im y.im)))))> # # #posit16 1.0) (-.p16 (*.p16 (*.p16 x.re y.re) (*.p16 x.re y.re)) (*.p16 (*.p16 y.im x.im) (*.p16 y.im x.im)))) (*.p16 (+.p16 (*.p16 x.re y.re) (*.p16 y.im x.im)) (+.p16 (*.p16 x.re y.re) (*.p16 x.im y.im))))))>) 5.750 * * * * [regimes]: Trying to branch on x.im from (# # # #posit16 1.0) (-.p16 (*.p16 x.re y.re) (*.p16 y.im x.im))) (*.p16 x.re y.re)) (*.p16 (/.p16 (real->posit16 1.0) (-.p16 (*.p16 x.re y.re) (*.p16 y.im x.im))) (*.p16 x.im y.im)))))> # # #posit16 1.0) (-.p16 (*.p16 (*.p16 x.re y.re) (*.p16 x.re y.re)) (*.p16 (*.p16 y.im x.im) (*.p16 y.im x.im)))) (*.p16 (+.p16 (*.p16 x.re y.re) (*.p16 y.im x.im)) (+.p16 (*.p16 x.re y.re) (*.p16 x.im y.im))))))>) 5.871 * * * * [regimes]: Trying to branch on y.re from (# # # #posit16 1.0) (-.p16 (*.p16 x.re y.re) (*.p16 y.im x.im))) (*.p16 x.re y.re)) (*.p16 (/.p16 (real->posit16 1.0) (-.p16 (*.p16 x.re y.re) (*.p16 y.im x.im))) (*.p16 x.im y.im)))))> # # #posit16 1.0) (-.p16 (*.p16 (*.p16 x.re y.re) (*.p16 x.re y.re)) (*.p16 (*.p16 y.im x.im) (*.p16 y.im x.im)))) (*.p16 (+.p16 (*.p16 x.re y.re) (*.p16 y.im x.im)) (+.p16 (*.p16 x.re y.re) (*.p16 x.im y.im))))))>) 5.987 * * * * [regimes]: Trying to branch on x.re from (# # # #posit16 1.0) (-.p16 (*.p16 x.re y.re) (*.p16 y.im x.im))) (*.p16 x.re y.re)) (*.p16 (/.p16 (real->posit16 1.0) (-.p16 (*.p16 x.re y.re) (*.p16 y.im x.im))) (*.p16 x.im y.im)))))> # # #posit16 1.0) (-.p16 (*.p16 (*.p16 x.re y.re) (*.p16 x.re y.re)) (*.p16 (*.p16 y.im x.im) (*.p16 y.im x.im)))) (*.p16 (+.p16 (*.p16 x.re y.re) (*.p16 y.im x.im)) (+.p16 (*.p16 x.re y.re) (*.p16 x.im y.im))))))>) 6.118 * * * [regime]: Found split indices: #