0.002 * [progress]: [Phase 1 of 3] Setting up. 0.002 * * * [progress]: [1/2] Preparing points 0.003 * * * * [points]: Sampling 256 additional inputs, on iter 0 have 0 / 256 0.005 * * * * [points]: Computing exacts on every 16 of 256 points to ramp up precision 0.008 * * * * [points]: Setting MPFR precision to 64 0.010 * * * * [points]: Setting MPFR precision to 320 0.012 * * * * [points]: Computing exacts on every 8 of 256 points to ramp up precision 0.014 * * * * [points]: Setting MPFR precision to 64 0.017 * * * * [points]: Setting MPFR precision to 320 0.021 * * * * [points]: Computing exacts on every 4 of 256 points to ramp up precision 0.023 * * * * [points]: Setting MPFR precision to 64 0.029 * * * * [points]: Setting MPFR precision to 320 0.036 * * * * [points]: Computing exacts on every 2 of 256 points to ramp up precision 0.038 * * * * [points]: Setting MPFR precision to 64 0.049 * * * * [points]: Setting MPFR precision to 320 0.072 * * * * [points]: Computing exacts for 256 points 0.075 * * * * [points]: Setting MPFR precision to 64 0.106 * * * * [points]: Setting MPFR precision to 320 0.138 * * * * [points]: Filtering points with unrepresentable outputs 0.140 * * * * [points]: Sampled 256 points with exact outputs 0.140 * * * [progress]: [2/2] Setting up program. 0.151 * [progress]: [Phase 2 of 3] Improving. 0.152 * * * * [progress]: [ 1 / 1 ] simplifiying candidate # 0.152 * [simplify]: Simplifying (-.p16 (+.p16 (-.p16 (*.p16 d1 d2) (*.p16 d1 d3)) (*.p16 d4 d1)) (*.p16 d1 d1)) 0.152 * * [simplify]: iters left: 4 (11 enodes) 0.157 * * [simplify]: iters left: 3 (43 enodes) 0.174 * * [simplify]: iters left: 2 (148 enodes) 0.267 * * [simplify]: Extracting #0: cost 1 inf + 0 0.268 * * [simplify]: Extracting #1: cost 40 inf + 0 0.268 * * [simplify]: Extracting #2: cost 128 inf + 322 0.269 * * [simplify]: Extracting #3: cost 222 inf + 10234 0.272 * * [simplify]: Extracting #4: cost 153 inf + 124713 0.280 * * [simplify]: Extracting #5: cost 28 inf + 253727 0.294 * * [simplify]: Extracting #6: cost 1 inf + 271088 0.315 * * [simplify]: Extracting #7: cost 0 inf + 269810 0.334 * * [simplify]: Extracting #8: cost 0 inf + 269170 0.347 * [simplify]: Simplified to (*.p16 d1 (+.p16 (-.p16 d2 d3) (-.p16 d4 d1))) 0.347 * [simplify]: Simplified (2) to (λ (d1 d2 d3 d4) (*.p16 d1 (+.p16 (-.p16 d2 d3) (-.p16 d4 d1)))) 0.361 * * [progress]: iteration 1 / 4 0.361 * * * [progress]: picking best candidate 0.370 * * * * [pick]: Picked # 0.371 * * * [progress]: localizing error 0.450 * * * [progress]: generating rewritten candidates 0.450 * * * * [progress]: [ 1 / 2 ] rewriting at (2 2) 0.464 * * * * [progress]: [ 2 / 2 ] rewriting at (2) 0.470 * * * [progress]: generating series expansions 0.470 * * * * [progress]: [ 1 / 2 ] generating series at (2 2) 0.470 * * * * [progress]: [ 2 / 2 ] generating series at (2) 0.470 * * * [progress]: simplifying candidates 0.470 * * * * [progress]: [ 1 / 10 ] simplifiying candidate # 0.470 * [simplify]: Simplifying (+.p16 (-.p16 d2 d3) d4) 0.471 * * [simplify]: iters left: 2 (5 enodes) 0.472 * * [simplify]: iters left: 1 (21 enodes) 0.475 * * [simplify]: Extracting #0: cost 1 inf + 0 0.475 * * [simplify]: Extracting #1: cost 12 inf + 0 0.475 * * [simplify]: Extracting #2: cost 13 inf + 328 0.475 * * [simplify]: Extracting #3: cost 7 inf + 2190 0.475 * * [simplify]: Extracting #4: cost 3 inf + 5400 0.476 * * [simplify]: Extracting #5: cost 0 inf + 8044 0.476 * [simplify]: Simplified to (-.p16 (+.p16 d4 d2) d3) 0.476 * [simplify]: Simplified (2 2 1) to (λ (d1 d2 d3 d4) (*.p16 d1 (+.p16 (-.p16 (+.p16 d4 d2) d3) (neg.p16 d1)))) 0.476 * * * * [progress]: [ 2 / 10 ] simplifiying candidate # 0.476 * [simplify]: Simplifying (+.p16 (neg.p16 d3) (-.p16 d4 d1)) 0.476 * * [simplify]: iters left: 2 (6 enodes) 0.477 * * [simplify]: iters left: 1 (22 enodes) 0.481 * * [simplify]: Extracting #0: cost 1 inf + 0 0.481 * * [simplify]: Extracting #1: cost 12 inf + 0 0.481 * * [simplify]: Extracting #2: cost 10 inf + 329 0.481 * * [simplify]: Extracting #3: cost 10 inf + 975 0.481 * * [simplify]: Extracting #4: cost 4 inf + 3871 0.481 * * [simplify]: Extracting #5: cost 0 inf + 7197 0.482 * [simplify]: Simplified to (-.p16 (-.p16 d4 d1) d3) 0.482 * [simplify]: Simplified (2 2 2) to (λ (d1 d2 d3 d4) (*.p16 d1 (+.p16 d2 (-.p16 (-.p16 d4 d1) d3)))) 0.482 * * * * [progress]: [ 3 / 10 ] simplifiying candidate # 0.482 * [simplify]: Simplifying (+.p16 (-.p16 d2 d3) d4) 0.482 * * [simplify]: iters left: 2 (5 enodes) 0.483 * * [simplify]: iters left: 1 (21 enodes) 0.486 * * [simplify]: Extracting #0: cost 1 inf + 0 0.486 * * [simplify]: Extracting #1: cost 12 inf + 0 0.486 * * [simplify]: Extracting #2: cost 13 inf + 328 0.486 * * [simplify]: Extracting #3: cost 7 inf + 2190 0.486 * * [simplify]: Extracting #4: cost 3 inf + 5400 0.487 * * [simplify]: Extracting #5: cost 0 inf + 8044 0.487 * [simplify]: Simplified to (-.p16 (+.p16 d4 d2) d3) 0.487 * [simplify]: Simplified (2 2 1) to (λ (d1 d2 d3 d4) (*.p16 d1 (-.p16 (-.p16 (+.p16 d4 d2) d3) d1))) 0.487 * * * * [progress]: [ 4 / 10 ] simplifiying candidate # 0.487 * [simplify]: Simplifying (-.p16 d3 (-.p16 d4 d1)) 0.487 * * [simplify]: iters left: 2 (5 enodes) 0.488 * * [simplify]: iters left: 1 (27 enodes) 0.493 * * [simplify]: Extracting #0: cost 1 inf + 0 0.493 * * [simplify]: Extracting #1: cost 9 inf + 0 0.493 * * [simplify]: Extracting #2: cost 17 inf + 83 0.493 * * [simplify]: Extracting #3: cost 23 inf + 854 0.493 * * [simplify]: Extracting #4: cost 9 inf + 7364 0.494 * * [simplify]: Extracting #5: cost 0 inf + 14983 0.494 * [simplify]: Simplified to (+.p16 (-.p16 d3 d4) d1) 0.494 * [simplify]: Simplified (2 2 2) to (λ (d1 d2 d3 d4) (*.p16 d1 (-.p16 d2 (+.p16 (-.p16 d3 d4) d1)))) 0.494 * * * * [progress]: [ 5 / 10 ] simplifiying candidate # 0.494 * * * * [progress]: [ 6 / 10 ] simplifiying candidate # 0.494 * [simplify]: Simplifying (*.p16 d1 (-.p16 d2 d3)) 0.495 * * [simplify]: iters left: 2 (5 enodes) 0.496 * * [simplify]: iters left: 1 (19 enodes) 0.498 * * [simplify]: Extracting #0: cost 1 inf + 0 0.498 * * [simplify]: Extracting #1: cost 10 inf + 0 0.498 * * [simplify]: Extracting #2: cost 13 inf + 1 0.498 * * [simplify]: Extracting #3: cost 12 inf + 890 0.499 * * [simplify]: Extracting #4: cost 4 inf + 5070 0.499 * * [simplify]: Extracting #5: cost 1 inf + 7034 0.499 * * [simplify]: Extracting #6: cost 0 inf + 8396 0.499 * [simplify]: Simplified to (*.p16 (-.p16 d2 d3) d1) 0.499 * [simplify]: Simplified (2 1) to (λ (d1 d2 d3 d4) (+.p16 (*.p16 (-.p16 d2 d3) d1) (*.p16 d1 (-.p16 d4 d1)))) 0.500 * [simplify]: Simplifying (*.p16 d1 (-.p16 d4 d1)) 0.500 * * [simplify]: iters left: 2 (4 enodes) 0.500 * * [simplify]: iters left: 1 (16 enodes) 0.503 * * [simplify]: Extracting #0: cost 1 inf + 0 0.503 * * [simplify]: Extracting #1: cost 10 inf + 0 0.503 * * [simplify]: Extracting #2: cost 12 inf + 1 0.503 * * [simplify]: Extracting #3: cost 11 inf + 1249 0.503 * * [simplify]: Extracting #4: cost 6 inf + 3901 0.503 * * [simplify]: Extracting #5: cost 1 inf + 7028 0.504 * * [simplify]: Extracting #6: cost 0 inf + 8390 0.504 * [simplify]: Simplified to (*.p16 d1 (-.p16 d4 d1)) 0.504 * [simplify]: Simplified (2 2) to (λ (d1 d2 d3 d4) (+.p16 (*.p16 d1 (-.p16 d2 d3)) (*.p16 d1 (-.p16 d4 d1)))) 0.504 * * * * [progress]: [ 7 / 10 ] simplifiying candidate # 0.504 * [simplify]: Simplifying (*.p16 (-.p16 d2 d3) d1) 0.504 * * [simplify]: iters left: 2 (5 enodes) 0.505 * * [simplify]: iters left: 1 (19 enodes) 0.508 * * [simplify]: Extracting #0: cost 1 inf + 0 0.508 * * [simplify]: Extracting #1: cost 10 inf + 0 0.508 * * [simplify]: Extracting #2: cost 13 inf + 1 0.508 * * [simplify]: Extracting #3: cost 14 inf + 486 0.508 * * [simplify]: Extracting #4: cost 4 inf + 5070 0.508 * * [simplify]: Extracting #5: cost 1 inf + 7034 0.509 * * [simplify]: Extracting #6: cost 0 inf + 8396 0.509 * [simplify]: Simplified to (*.p16 d1 (-.p16 d2 d3)) 0.509 * [simplify]: Simplified (2 1) to (λ (d1 d2 d3 d4) (+.p16 (*.p16 d1 (-.p16 d2 d3)) (*.p16 (-.p16 d4 d1) d1))) 0.509 * [simplify]: Simplifying (*.p16 (-.p16 d4 d1) d1) 0.509 * * [simplify]: iters left: 2 (4 enodes) 0.510 * * [simplify]: iters left: 1 (16 enodes) 0.512 * * [simplify]: Extracting #0: cost 1 inf + 0 0.513 * * [simplify]: Extracting #1: cost 10 inf + 0 0.513 * * [simplify]: Extracting #2: cost 12 inf + 1 0.513 * * [simplify]: Extracting #3: cost 13 inf + 885 0.513 * * [simplify]: Extracting #4: cost 8 inf + 2697 0.513 * * [simplify]: Extracting #5: cost 2 inf + 6266 0.513 * * [simplify]: Extracting #6: cost 0 inf + 8390 0.513 * [simplify]: Simplified to (*.p16 (-.p16 d4 d1) d1) 0.514 * [simplify]: Simplified (2 2) to (λ (d1 d2 d3 d4) (+.p16 (*.p16 (-.p16 d2 d3) d1) (*.p16 (-.p16 d4 d1) d1))) 0.514 * * * * [progress]: [ 8 / 10 ] simplifiying candidate # 0.514 * * * * [progress]: [ 9 / 10 ] simplifiying candidate # 0.514 * [simplify]: Simplifying (*.p16 d1 (+.p16 (-.p16 d2 d3) (-.p16 d4 d1))) 0.514 * * [simplify]: iters left: 3 (8 enodes) 0.516 * * [simplify]: iters left: 2 (42 enodes) 0.523 * * [simplify]: iters left: 1 (117 enodes) 0.567 * * [simplify]: Extracting #0: cost 1 inf + 0 0.567 * * [simplify]: Extracting #1: cost 24 inf + 0 0.568 * * [simplify]: Extracting #2: cost 56 inf + 1 0.568 * * [simplify]: Extracting #3: cost 108 inf + 1181 0.571 * * [simplify]: Extracting #4: cost 85 inf + 24120 0.577 * * [simplify]: Extracting #5: cost 33 inf + 70189 0.585 * * [simplify]: Extracting #6: cost 1 inf + 97168 0.593 * * [simplify]: Extracting #7: cost 0 inf + 98411 0.602 * [simplify]: Simplified to (*.p16 (+.p16 (-.p16 d2 d3) (-.p16 d4 d1)) d1) 0.602 * [simplify]: Simplified (2) to (λ (d1 d2 d3 d4) (*.p16 (+.p16 (-.p16 d2 d3) (-.p16 d4 d1)) d1)) 0.602 * * * * [progress]: [ 10 / 10 ] simplifiying candidate # 0.602 * [simplify]: Simplifying (*.p16 d1 (+.p16 (-.p16 d2 d3) (-.p16 d4 d1))) 0.603 * * [simplify]: iters left: 3 (8 enodes) 0.606 * * [simplify]: iters left: 2 (42 enodes) 0.622 * * [simplify]: iters left: 1 (117 enodes) 0.672 * * [simplify]: Extracting #0: cost 1 inf + 0 0.672 * * [simplify]: Extracting #1: cost 24 inf + 0 0.672 * * [simplify]: Extracting #2: cost 56 inf + 1 0.673 * * [simplify]: Extracting #3: cost 108 inf + 1181 0.675 * * [simplify]: Extracting #4: cost 85 inf + 24120 0.681 * * [simplify]: Extracting #5: cost 33 inf + 70189 0.689 * * [simplify]: Extracting #6: cost 1 inf + 97168 0.693 * * [simplify]: Extracting #7: cost 0 inf + 98411 0.697 * [simplify]: Simplified to (*.p16 (+.p16 (-.p16 d2 d3) (-.p16 d4 d1)) d1) 0.697 * [simplify]: Simplified (2) to (λ (d1 d2 d3 d4) (*.p16 (+.p16 (-.p16 d2 d3) (-.p16 d4 d1)) d1)) 0.697 * * * [progress]: adding candidates to table 0.874 * * [progress]: iteration 2 / 4 0.874 * * * [progress]: picking best candidate 0.909 * * * * [pick]: Picked # 0.909 * * * [progress]: localizing error 1.002 * * * [progress]: generating rewritten candidates 1.002 * * * * [progress]: [ 1 / 3 ] rewriting at (2) 1.006 * * * * [progress]: [ 2 / 3 ] rewriting at (2 2) 1.007 * * * * [progress]: [ 3 / 3 ] rewriting at (2 2 2) 1.013 * * * [progress]: generating series expansions 1.013 * * * * [progress]: [ 1 / 3 ] generating series at (2) 1.013 * * * * [progress]: [ 2 / 3 ] generating series at (2 2) 1.013 * * * * [progress]: [ 3 / 3 ] generating series at (2 2 2) 1.013 * * * [progress]: simplifying candidates 1.013 * * * * [progress]: [ 1 / 16 ] simplifiying candidate # 1.014 * [simplify]: Simplifying (*.p16 d1 (-.p16 d2 d3)) 1.014 * * [simplify]: iters left: 2 (5 enodes) 1.015 * * [simplify]: iters left: 1 (19 enodes) 1.017 * * [simplify]: Extracting #0: cost 1 inf + 0 1.017 * * [simplify]: Extracting #1: cost 10 inf + 0 1.018 * * [simplify]: Extracting #2: cost 13 inf + 1 1.018 * * [simplify]: Extracting #3: cost 12 inf + 890 1.018 * * [simplify]: Extracting #4: cost 4 inf + 5070 1.018 * * [simplify]: Extracting #5: cost 1 inf + 7034 1.018 * * [simplify]: Extracting #6: cost 0 inf + 8396 1.019 * [simplify]: Simplified to (*.p16 (-.p16 d2 d3) d1) 1.019 * [simplify]: Simplified (2 1) to (λ (d1 d2 d3 d4) (+.p16 (*.p16 (-.p16 d2 d3) d1) (*.p16 d1 (-.p16 d4 d1)))) 1.019 * [simplify]: Simplifying (*.p16 d1 (-.p16 d4 d1)) 1.019 * * [simplify]: iters left: 2 (4 enodes) 1.020 * * [simplify]: iters left: 1 (16 enodes) 1.022 * * [simplify]: Extracting #0: cost 1 inf + 0 1.022 * * [simplify]: Extracting #1: cost 10 inf + 0 1.022 * * [simplify]: Extracting #2: cost 12 inf + 1 1.022 * * [simplify]: Extracting #3: cost 11 inf + 1249 1.022 * * [simplify]: Extracting #4: cost 6 inf + 3901 1.023 * * [simplify]: Extracting #5: cost 1 inf + 7028 1.023 * * [simplify]: Extracting #6: cost 0 inf + 8390 1.023 * [simplify]: Simplified to (*.p16 d1 (-.p16 d4 d1)) 1.023 * [simplify]: Simplified (2 2) to (λ (d1 d2 d3 d4) (+.p16 (*.p16 d1 (-.p16 d2 d3)) (*.p16 d1 (-.p16 d4 d1)))) 1.023 * * * * [progress]: [ 2 / 16 ] simplifiying candidate # 1.023 * [simplify]: Simplifying (*.p16 d1 d2) 1.023 * * [simplify]: iters left: 1 (3 enodes) 1.024 * * [simplify]: Extracting #0: cost 1 inf + 0 1.024 * * [simplify]: Extracting #1: cost 3 inf + 0 1.024 * * [simplify]: Extracting #2: cost 1 inf + 2 1.024 * * [simplify]: Extracting #3: cost 0 inf + 324 1.024 * [simplify]: Simplified to (*.p16 d2 d1) 1.024 * [simplify]: Simplified (2 1) to (λ (d1 d2 d3 d4) (+.p16 (*.p16 d2 d1) (*.p16 d1 (neg.p16 (+.p16 (-.p16 d3 d4) d1))))) 1.024 * [simplify]: Simplifying (*.p16 d1 (neg.p16 (+.p16 (-.p16 d3 d4) d1))) 1.024 * * [simplify]: iters left: 4 (7 enodes) 1.026 * * [simplify]: iters left: 3 (24 enodes) 1.029 * * [simplify]: iters left: 2 (51 enodes) 1.042 * * [simplify]: iters left: 1 (120 enodes) 1.070 * * [simplify]: Extracting #0: cost 1 inf + 0 1.070 * * [simplify]: Extracting #1: cost 3 inf + 0 1.070 * * [simplify]: Extracting #2: cost 3 inf + 1 1.070 * * [simplify]: Extracting #3: cost 24 inf + 1 1.070 * * [simplify]: Extracting #4: cost 69 inf + 491 1.071 * * [simplify]: Extracting #5: cost 92 inf + 17146 1.073 * * [simplify]: Extracting #6: cost 53 inf + 72859 1.078 * * [simplify]: Extracting #7: cost 10 inf + 127073 1.083 * * [simplify]: Extracting #8: cost 0 inf + 139724 1.088 * [simplify]: Simplified to (*.p16 d1 (neg.p16 (+.p16 d1 (-.p16 d3 d4)))) 1.088 * [simplify]: Simplified (2 2) to (λ (d1 d2 d3 d4) (+.p16 (*.p16 d1 d2) (*.p16 d1 (neg.p16 (+.p16 d1 (-.p16 d3 d4)))))) 1.088 * * * * [progress]: [ 3 / 16 ] simplifiying candidate # 1.088 * [simplify]: Simplifying (*.p16 (-.p16 d2 d3) d1) 1.088 * * [simplify]: iters left: 2 (5 enodes) 1.090 * * [simplify]: iters left: 1 (19 enodes) 1.092 * * [simplify]: Extracting #0: cost 1 inf + 0 1.092 * * [simplify]: Extracting #1: cost 10 inf + 0 1.092 * * [simplify]: Extracting #2: cost 13 inf + 1 1.092 * * [simplify]: Extracting #3: cost 14 inf + 486 1.093 * * [simplify]: Extracting #4: cost 4 inf + 5070 1.093 * * [simplify]: Extracting #5: cost 1 inf + 7034 1.093 * * [simplify]: Extracting #6: cost 0 inf + 8396 1.093 * [simplify]: Simplified to (*.p16 d1 (-.p16 d2 d3)) 1.093 * [simplify]: Simplified (2 1) to (λ (d1 d2 d3 d4) (+.p16 (*.p16 d1 (-.p16 d2 d3)) (*.p16 (-.p16 d4 d1) d1))) 1.094 * [simplify]: Simplifying (*.p16 (-.p16 d4 d1) d1) 1.094 * * [simplify]: iters left: 2 (4 enodes) 1.095 * * [simplify]: iters left: 1 (16 enodes) 1.097 * * [simplify]: Extracting #0: cost 1 inf + 0 1.097 * * [simplify]: Extracting #1: cost 10 inf + 0 1.097 * * [simplify]: Extracting #2: cost 12 inf + 1 1.097 * * [simplify]: Extracting #3: cost 13 inf + 885 1.097 * * [simplify]: Extracting #4: cost 8 inf + 2697 1.097 * * [simplify]: Extracting #5: cost 2 inf + 6266 1.098 * * [simplify]: Extracting #6: cost 0 inf + 8390 1.098 * [simplify]: Simplified to (*.p16 (-.p16 d4 d1) d1) 1.098 * [simplify]: Simplified (2 2) to (λ (d1 d2 d3 d4) (+.p16 (*.p16 (-.p16 d2 d3) d1) (*.p16 (-.p16 d4 d1) d1))) 1.098 * * * * [progress]: [ 4 / 16 ] simplifiying candidate # 1.098 * [simplify]: Simplifying (*.p16 d2 d1) 1.098 * * [simplify]: iters left: 1 (3 enodes) 1.099 * * [simplify]: Extracting #0: cost 1 inf + 0 1.099 * * [simplify]: Extracting #1: cost 3 inf + 0 1.099 * * [simplify]: Extracting #2: cost 1 inf + 2 1.099 * * [simplify]: Extracting #3: cost 0 inf + 324 1.099 * [simplify]: Simplified to (*.p16 d1 d2) 1.099 * [simplify]: Simplified (2 1) to (λ (d1 d2 d3 d4) (+.p16 (*.p16 d1 d2) (*.p16 (neg.p16 (+.p16 (-.p16 d3 d4) d1)) d1))) 1.099 * [simplify]: Simplifying (*.p16 (neg.p16 (+.p16 (-.p16 d3 d4) d1)) d1) 1.099 * * [simplify]: iters left: 4 (7 enodes) 1.101 * * [simplify]: iters left: 3 (24 enodes) 1.106 * * [simplify]: iters left: 2 (51 enodes) 1.114 * * [simplify]: iters left: 1 (120 enodes) 1.141 * * [simplify]: Extracting #0: cost 1 inf + 0 1.141 * * [simplify]: Extracting #1: cost 3 inf + 0 1.141 * * [simplify]: Extracting #2: cost 3 inf + 1 1.141 * * [simplify]: Extracting #3: cost 24 inf + 1 1.142 * * [simplify]: Extracting #4: cost 71 inf + 207 1.143 * * [simplify]: Extracting #5: cost 93 inf + 16907 1.145 * * [simplify]: Extracting #6: cost 61 inf + 66401 1.149 * * [simplify]: Extracting #7: cost 15 inf + 121180 1.155 * * [simplify]: Extracting #8: cost 0 inf + 140604 1.160 * [simplify]: Simplified to (*.p16 (neg.p16 (+.p16 d3 (-.p16 d1 d4))) d1) 1.160 * [simplify]: Simplified (2 2) to (λ (d1 d2 d3 d4) (+.p16 (*.p16 d2 d1) (*.p16 (neg.p16 (+.p16 d3 (-.p16 d1 d4))) d1))) 1.160 * * * * [progress]: [ 5 / 16 ] simplifiying candidate # 1.160 * [simplify]: Simplifying (*.p16 d1 (-.p16 (*.p16 d2 d2) (*.p16 (+.p16 (-.p16 d3 d4) d1) (+.p16 (-.p16 d3 d4) d1)))) 1.160 * * [simplify]: iters left: 5 (10 enodes) 1.164 * * [simplify]: iters left: 4 (45 enodes) 1.183 * * [simplify]: iters left: 3 (164 enodes) 1.286 * * [simplify]: Extracting #0: cost 1 inf + 0 1.287 * * [simplify]: Extracting #1: cost 23 inf + 0 1.287 * * [simplify]: Extracting #2: cost 127 inf + 1 1.289 * * [simplify]: Extracting #3: cost 223 inf + 4440 1.296 * * [simplify]: Extracting #4: cost 232 inf + 73668 1.316 * * [simplify]: Extracting #5: cost 41 inf + 241847 1.344 * * [simplify]: Extracting #6: cost 3 inf + 278505 1.370 * * [simplify]: Extracting #7: cost 0 inf + 282911 1.396 * [simplify]: Simplified to (*.p16 d1 (*.p16 (+.p16 d1 (-.p16 (+.p16 d3 d2) d4)) (+.p16 (-.p16 d2 (+.p16 d1 d3)) d4))) 1.396 * [simplify]: Simplified (2 1) to (λ (d1 d2 d3 d4) (/.p16 (*.p16 d1 (*.p16 (+.p16 d1 (-.p16 (+.p16 d3 d2) d4)) (+.p16 (-.p16 d2 (+.p16 d1 d3)) d4))) (+.p16 d2 (+.p16 (-.p16 d3 d4) d1)))) 1.396 * * * * [progress]: [ 6 / 16 ] simplifiying candidate # 1.397 * * * * [progress]: [ 7 / 16 ] simplifiying candidate # 1.397 * [simplify]: Simplifying (-.p16 d2 (-.p16 d3 d4)) 1.397 * * [simplify]: iters left: 2 (5 enodes) 1.399 * * [simplify]: iters left: 1 (27 enodes) 1.408 * * [simplify]: Extracting #0: cost 1 inf + 0 1.408 * * [simplify]: Extracting #1: cost 9 inf + 0 1.409 * * [simplify]: Extracting #2: cost 17 inf + 83 1.409 * * [simplify]: Extracting #3: cost 23 inf + 854 1.409 * * [simplify]: Extracting #4: cost 9 inf + 7364 1.410 * * [simplify]: Extracting #5: cost 0 inf + 14983 1.411 * [simplify]: Simplified to (+.p16 (-.p16 d2 d3) d4) 1.411 * [simplify]: Simplified (2 2 1) to (λ (d1 d2 d3 d4) (*.p16 d1 (-.p16 (+.p16 (-.p16 d2 d3) d4) d1))) 1.412 * * * * [progress]: [ 8 / 16 ] simplifiying candidate # 1.412 * [simplify]: Simplifying (-.p16 d2 d3) 1.412 * * [simplify]: iters left: 1 (3 enodes) 1.413 * * [simplify]: Extracting #0: cost 1 inf + 0 1.413 * * [simplify]: Extracting #1: cost 6 inf + 0 1.413 * * [simplify]: Extracting #2: cost 5 inf + 44 1.414 * * [simplify]: Extracting #3: cost 0 inf + 1571 1.414 * [simplify]: Simplified to (-.p16 d2 d3) 1.414 * [simplify]: Simplified (2 2 1) to (λ (d1 d2 d3 d4) (*.p16 d1 (+.p16 (-.p16 d2 d3) (-.p16 d4 d1)))) 1.414 * * * * [progress]: [ 9 / 16 ] simplifiying candidate # 1.414 * [simplify]: Simplifying (neg.p16 (+.p16 (-.p16 d3 d4) d1)) 1.414 * * [simplify]: iters left: 3 (6 enodes) 1.417 * * [simplify]: iters left: 2 (22 enodes) 1.424 * * [simplify]: iters left: 1 (49 enodes) 1.441 * * [simplify]: Extracting #0: cost 1 inf + 0 1.441 * * [simplify]: Extracting #1: cost 2 inf + 0 1.441 * * [simplify]: Extracting #2: cost 14 inf + 0 1.441 * * [simplify]: Extracting #3: cost 22 inf + 84 1.442 * * [simplify]: Extracting #4: cost 33 inf + 2911 1.443 * * [simplify]: Extracting #5: cost 15 inf + 15999 1.445 * * [simplify]: Extracting #6: cost 1 inf + 28018 1.447 * * [simplify]: Extracting #7: cost 0 inf + 30020 1.449 * [simplify]: Simplified to (neg.p16 (-.p16 (+.p16 d3 d1) d4)) 1.449 * [simplify]: Simplified (2 2 2) to (λ (d1 d2 d3 d4) (*.p16 d1 (+.p16 d2 (neg.p16 (-.p16 (+.p16 d3 d1) d4))))) 1.449 * * * * [progress]: [ 10 / 16 ] simplifiying candidate # 1.449 * [simplify]: Simplifying (-.p16 (*.p16 d2 d2) (*.p16 (+.p16 (-.p16 d3 d4) d1) (+.p16 (-.p16 d3 d4) d1))) 1.450 * * [simplify]: iters left: 4 (9 enodes) 1.454 * * [simplify]: iters left: 3 (43 enodes) 1.472 * * [simplify]: iters left: 2 (148 enodes) 1.563 * * [simplify]: Extracting #0: cost 1 inf + 0 1.563 * * [simplify]: Extracting #1: cost 45 inf + 0 1.564 * * [simplify]: Extracting #2: cost 168 inf + 0 1.566 * * [simplify]: Extracting #3: cost 265 inf + 4279 1.575 * * [simplify]: Extracting #4: cost 150 inf + 111910 1.586 * * [simplify]: Extracting #5: cost 18 inf + 234540 1.602 * * [simplify]: Extracting #6: cost 4 inf + 247766 1.614 * * [simplify]: Extracting #7: cost 0 inf + 254736 1.626 * [simplify]: Simplified to (*.p16 (+.p16 (-.p16 d2 (+.p16 d1 d3)) d4) (+.p16 d2 (+.p16 (-.p16 d3 d4) d1))) 1.626 * [simplify]: Simplified (2 2 1) to (λ (d1 d2 d3 d4) (*.p16 d1 (/.p16 (*.p16 (+.p16 (-.p16 d2 (+.p16 d1 d3)) d4) (+.p16 d2 (+.p16 (-.p16 d3 d4) d1))) (+.p16 d2 (+.p16 (-.p16 d3 d4) d1))))) 1.626 * [simplify]: Simplifying (+.p16 d2 (+.p16 (-.p16 d3 d4) d1)) 1.627 * * [simplify]: iters left: 3 (7 enodes) 1.628 * * [simplify]: iters left: 2 (28 enodes) 1.632 * * [simplify]: iters left: 1 (67 enodes) 1.645 * * [simplify]: Extracting #0: cost 1 inf + 0 1.645 * * [simplify]: Extracting #1: cost 31 inf + 0 1.645 * * [simplify]: Extracting #2: cost 42 inf + 575 1.646 * * [simplify]: Extracting #3: cost 39 inf + 6292 1.647 * * [simplify]: Extracting #4: cost 20 inf + 18789 1.649 * * [simplify]: Extracting #5: cost 2 inf + 33577 1.650 * * [simplify]: Extracting #6: cost 0 inf + 37022 1.652 * [simplify]: Simplified to (+.p16 d2 (-.p16 (+.p16 d1 d3) d4)) 1.652 * [simplify]: Simplified (2 2 2) to (λ (d1 d2 d3 d4) (*.p16 d1 (/.p16 (*.p16 (+.p16 (-.p16 d2 (+.p16 d1 d3)) d4) (+.p16 d2 (+.p16 (-.p16 d3 d4) d1))) (+.p16 d2 (-.p16 (+.p16 d1 d3) d4))))) 1.652 * * * * [progress]: [ 11 / 16 ] simplifiying candidate # 1.652 * [simplify]: Simplifying (+.p16 (neg.p16 d4) d1) 1.652 * * [simplify]: iters left: 2 (4 enodes) 1.653 * * [simplify]: iters left: 1 (9 enodes) 1.654 * * [simplify]: Extracting #0: cost 1 inf + 0 1.654 * * [simplify]: Extracting #1: cost 4 inf + 0 1.655 * * [simplify]: Extracting #2: cost 2 inf + 2 1.655 * * [simplify]: Extracting #3: cost 0 inf + 165 1.655 * [simplify]: Simplified to (-.p16 d1 d4) 1.655 * [simplify]: Simplified (2 2 2 2) to (λ (d1 d2 d3 d4) (*.p16 d1 (-.p16 d2 (+.p16 d3 (-.p16 d1 d4))))) 1.655 * * * * [progress]: [ 12 / 16 ] simplifiying candidate # 1.655 * [simplify]: Simplifying (-.p16 d4 d1) 1.655 * * [simplify]: iters left: 1 (3 enodes) 1.656 * * [simplify]: Extracting #0: cost 1 inf + 0 1.656 * * [simplify]: Extracting #1: cost 6 inf + 0 1.656 * * [simplify]: Extracting #2: cost 5 inf + 44 1.656 * * [simplify]: Extracting #3: cost 0 inf + 1571 1.656 * [simplify]: Simplified to (-.p16 d4 d1) 1.656 * [simplify]: Simplified (2 2 2 2) to (λ (d1 d2 d3 d4) (*.p16 d1 (-.p16 d2 (-.p16 d3 (-.p16 d4 d1))))) 1.656 * * * * [progress]: [ 13 / 16 ] simplifiying candidate # 1.656 * * * * [progress]: [ 14 / 16 ] simplifiying candidate # 1.656 * [simplify]: Simplifying (*.p16 d1 (-.p16 d2 (+.p16 (-.p16 d3 d4) d1))) 1.656 * * [simplify]: iters left: 4 (8 enodes) 1.658 * * [simplify]: iters left: 3 (36 enodes) 1.664 * * [simplify]: iters left: 2 (109 enodes) 1.714 * * [simplify]: iters left: 1 (447 enodes) 2.154 * * [simplify]: Extracting #0: cost 1 inf + 0 2.154 * * [simplify]: Extracting #1: cost 41 inf + 0 2.154 * * [simplify]: Extracting #2: cost 380 inf + 1 2.158 * * [simplify]: Extracting #3: cost 784 inf + 45283 2.186 * * [simplify]: Extracting #4: cost 445 inf + 454294 2.238 * * [simplify]: Extracting #5: cost 148 inf + 754097 2.301 * * [simplify]: Extracting #6: cost 48 inf + 876432 2.396 * * [simplify]: Extracting #7: cost 1 inf + 946084 2.458 * * [simplify]: Extracting #8: cost 0 inf + 948726 2.554 * [simplify]: Simplified to (*.p16 (+.p16 d4 (-.p16 d2 (+.p16 d3 d1))) d1) 2.554 * [simplify]: Simplified (2) to (λ (d1 d2 d3 d4) (*.p16 (+.p16 d4 (-.p16 d2 (+.p16 d3 d1))) d1)) 2.554 * * * * [progress]: [ 15 / 16 ] simplifiying candidate # 2.554 * [simplify]: Simplifying (*.p16 d1 (-.p16 d2 (+.p16 (-.p16 d3 d4) d1))) 2.554 * * [simplify]: iters left: 4 (8 enodes) 2.558 * * [simplify]: iters left: 3 (36 enodes) 2.571 * * [simplify]: iters left: 2 (109 enodes) 2.624 * * [simplify]: iters left: 1 (447 enodes) 2.963 * * [simplify]: Extracting #0: cost 1 inf + 0 2.963 * * [simplify]: Extracting #1: cost 41 inf + 0 2.968 * * [simplify]: Extracting #2: cost 380 inf + 1 2.972 * * [simplify]: Extracting #3: cost 784 inf + 45283 3.016 * * [simplify]: Extracting #4: cost 445 inf + 454294 3.084 * * [simplify]: Extracting #5: cost 148 inf + 754097 3.146 * * [simplify]: Extracting #6: cost 48 inf + 876432 3.223 * * [simplify]: Extracting #7: cost 1 inf + 946084 3.312 * * [simplify]: Extracting #8: cost 0 inf + 948726 3.381 * [simplify]: Simplified to (*.p16 (+.p16 d4 (-.p16 d2 (+.p16 d3 d1))) d1) 3.381 * [simplify]: Simplified (2) to (λ (d1 d2 d3 d4) (*.p16 (+.p16 d4 (-.p16 d2 (+.p16 d3 d1))) d1)) 3.381 * * * * [progress]: [ 16 / 16 ] simplifiying candidate # 3.381 * [simplify]: Simplifying (*.p16 d1 (-.p16 d2 (+.p16 (-.p16 d3 d4) d1))) 3.381 * * [simplify]: iters left: 4 (8 enodes) 3.383 * * [simplify]: iters left: 3 (36 enodes) 3.389 * * [simplify]: iters left: 2 (109 enodes) 3.422 * * [simplify]: iters left: 1 (447 enodes) 3.825 * * [simplify]: Extracting #0: cost 1 inf + 0 3.826 * * [simplify]: Extracting #1: cost 41 inf + 0 3.827 * * [simplify]: Extracting #2: cost 380 inf + 1 3.835 * * [simplify]: Extracting #3: cost 784 inf + 45283 3.877 * * [simplify]: Extracting #4: cost 445 inf + 454294 3.916 * * [simplify]: Extracting #5: cost 148 inf + 754097 4.000 * * [simplify]: Extracting #6: cost 48 inf + 876432 4.079 * * [simplify]: Extracting #7: cost 1 inf + 946084 4.175 * * [simplify]: Extracting #8: cost 0 inf + 948726 4.243 * [simplify]: Simplified to (*.p16 (+.p16 d4 (-.p16 d2 (+.p16 d3 d1))) d1) 4.243 * [simplify]: Simplified (2) to (λ (d1 d2 d3 d4) (*.p16 (+.p16 d4 (-.p16 d2 (+.p16 d3 d1))) d1)) 4.243 * * * [progress]: adding candidates to table 4.573 * * [progress]: iteration 3 / 4 4.573 * * * [progress]: picking best candidate 4.637 * * * * [pick]: Picked # 4.637 * * * [progress]: localizing error 4.719 * * * [progress]: generating rewritten candidates 4.719 * * * * [progress]: [ 1 / 3 ] rewriting at (2) 4.723 * * * * [progress]: [ 2 / 3 ] rewriting at (2 1 2) 4.725 * * * * [progress]: [ 3 / 3 ] rewriting at (2 1) 4.735 * * * [progress]: generating series expansions 4.735 * * * * [progress]: [ 1 / 3 ] generating series at (2) 4.735 * * * * [progress]: [ 2 / 3 ] generating series at (2 1 2) 4.735 * * * * [progress]: [ 3 / 3 ] generating series at (2 1) 4.736 * * * [progress]: simplifying candidates 4.736 * * * * [progress]: [ 1 / 10 ] simplifiying candidate # 4.736 * * * * [progress]: [ 2 / 10 ] simplifiying candidate # 4.736 * [simplify]: Simplifying (-.p16 d2 d3) 4.736 * * [simplify]: iters left: 1 (3 enodes) 4.736 * * [simplify]: Extracting #0: cost 1 inf + 0 4.737 * * [simplify]: Extracting #1: cost 6 inf + 0 4.737 * * [simplify]: Extracting #2: cost 5 inf + 44 4.737 * * [simplify]: Extracting #3: cost 0 inf + 1571 4.737 * [simplify]: Simplified to (-.p16 d2 d3) 4.737 * [simplify]: Simplified (2 1 2 1) to (λ (d1 d2 d3 d4) (*.p16 (+.p16 d4 (-.p16 (-.p16 d2 d3) d1)) d1)) 4.737 * * * * [progress]: [ 3 / 10 ] simplifiying candidate # 4.737 * [simplify]: Simplifying (neg.p16 (+.p16 d3 d1)) 4.737 * * [simplify]: iters left: 2 (4 enodes) 4.738 * * [simplify]: iters left: 1 (9 enodes) 4.739 * * [simplify]: Extracting #0: cost 1 inf + 0 4.739 * * [simplify]: Extracting #1: cost 2 inf + 0 4.739 * * [simplify]: Extracting #2: cost 4 inf + 0 4.739 * * [simplify]: Extracting #3: cost 2 inf + 2 4.739 * * [simplify]: Extracting #4: cost 0 inf + 166 4.739 * [simplify]: Simplified to (neg.p16 (+.p16 d1 d3)) 4.739 * [simplify]: Simplified (2 1 2 2) to (λ (d1 d2 d3 d4) (*.p16 (+.p16 d4 (+.p16 d2 (neg.p16 (+.p16 d1 d3)))) d1)) 4.739 * * * * [progress]: [ 4 / 10 ] simplifiying candidate # 4.739 * [simplify]: Simplifying (-.p16 (*.p16 d2 d2) (*.p16 (+.p16 d3 d1) (+.p16 d3 d1))) 4.739 * * [simplify]: iters left: 3 (7 enodes) 4.741 * * [simplify]: iters left: 2 (30 enodes) 4.747 * * [simplify]: iters left: 1 (95 enodes) 4.771 * * [simplify]: Extracting #0: cost 1 inf + 0 4.771 * * [simplify]: Extracting #1: cost 41 inf + 0 4.771 * * [simplify]: Extracting #2: cost 97 inf + 0 4.771 * * [simplify]: Extracting #3: cost 118 inf + 4232 4.773 * * [simplify]: Extracting #4: cost 52 inf + 60368 4.778 * * [simplify]: Extracting #5: cost 1 inf + 115651 4.782 * * [simplify]: Extracting #6: cost 0 inf + 117454 4.787 * [simplify]: Simplified to (*.p16 (-.p16 d2 (+.p16 d3 d1)) (+.p16 d2 (+.p16 d3 d1))) 4.787 * [simplify]: Simplified (2 1 2 1) to (λ (d1 d2 d3 d4) (*.p16 (+.p16 d4 (/.p16 (*.p16 (-.p16 d2 (+.p16 d3 d1)) (+.p16 d2 (+.p16 d3 d1))) (+.p16 d2 (+.p16 d3 d1)))) d1)) 4.787 * [simplify]: Simplifying (+.p16 d2 (+.p16 d3 d1)) 4.787 * * [simplify]: iters left: 2 (5 enodes) 4.788 * * [simplify]: iters left: 1 (15 enodes) 4.790 * * [simplify]: Extracting #0: cost 1 inf + 0 4.790 * * [simplify]: Extracting #1: cost 8 inf + 0 4.790 * * [simplify]: Extracting #2: cost 4 inf + 45 4.790 * * [simplify]: Extracting #3: cost 0 inf + 254 4.790 * [simplify]: Simplified to (+.p16 d3 (+.p16 d1 d2)) 4.790 * [simplify]: Simplified (2 1 2 2) to (λ (d1 d2 d3 d4) (*.p16 (+.p16 d4 (/.p16 (*.p16 (-.p16 d2 (+.p16 d3 d1)) (+.p16 d2 (+.p16 d3 d1))) (+.p16 d3 (+.p16 d1 d2)))) d1)) 4.790 * * * * [progress]: [ 5 / 10 ] simplifiying candidate # 4.791 * [simplify]: Simplifying (+.p16 d4 d2) 4.791 * * [simplify]: iters left: 1 (3 enodes) 4.791 * * [simplify]: Extracting #0: cost 1 inf + 0 4.791 * * [simplify]: Extracting #1: cost 3 inf + 0 4.791 * * [simplify]: Extracting #2: cost 1 inf + 2 4.791 * * [simplify]: Extracting #3: cost 0 inf + 44 4.791 * [simplify]: Simplified to (+.p16 d2 d4) 4.792 * [simplify]: Simplified (2 1 1) to (λ (d1 d2 d3 d4) (*.p16 (+.p16 (+.p16 d2 d4) (neg.p16 (+.p16 d3 d1))) d1)) 4.792 * * * * [progress]: [ 6 / 10 ] simplifiying candidate # 4.792 * [simplify]: Simplifying (+.p16 d4 d2) 4.792 * * [simplify]: iters left: 1 (3 enodes) 4.792 * * [simplify]: Extracting #0: cost 1 inf + 0 4.792 * * [simplify]: Extracting #1: cost 3 inf + 0 4.792 * * [simplify]: Extracting #2: cost 1 inf + 2 4.792 * * [simplify]: Extracting #3: cost 0 inf + 44 4.793 * [simplify]: Simplified to (+.p16 d2 d4) 4.793 * [simplify]: Simplified (2 1 1) to (λ (d1 d2 d3 d4) (*.p16 (-.p16 (+.p16 d2 d4) (+.p16 d3 d1)) d1)) 4.793 * * * * [progress]: [ 7 / 10 ] simplifiying candidate # 4.793 * * * * [progress]: [ 8 / 10 ] simplifiying candidate # 4.793 * [simplify]: Simplifying (*.p16 (+.p16 d4 (-.p16 d2 (+.p16 d3 d1))) d1) 4.793 * * [simplify]: iters left: 4 (8 enodes) 4.794 * * [simplify]: iters left: 3 (30 enodes) 4.799 * * [simplify]: iters left: 2 (87 enodes) 4.820 * * [simplify]: iters left: 1 (299 enodes) 4.966 * * [simplify]: Extracting #0: cost 1 inf + 0 4.966 * * [simplify]: Extracting #1: cost 33 inf + 0 4.967 * * [simplify]: Extracting #2: cost 175 inf + 1 4.969 * * [simplify]: Extracting #3: cost 298 inf + 3459 4.982 * * [simplify]: Extracting #4: cost 365 inf + 63464 4.995 * * [simplify]: Extracting #5: cost 78 inf + 302431 5.012 * * [simplify]: Extracting #6: cost 7 inf + 389376 5.032 * * [simplify]: Extracting #7: cost 0 inf + 400751 5.050 * [simplify]: Simplified to (*.p16 (+.p16 d4 (-.p16 d2 (+.p16 d3 d1))) d1) 5.050 * [simplify]: Simplified (2) to (λ (d1 d2 d3 d4) (*.p16 (+.p16 d4 (-.p16 d2 (+.p16 d3 d1))) d1)) 5.050 * * * * [progress]: [ 9 / 10 ] simplifiying candidate # 5.050 * [simplify]: Simplifying (*.p16 (+.p16 d4 (-.p16 d2 (+.p16 d3 d1))) d1) 5.050 * * [simplify]: iters left: 4 (8 enodes) 5.053 * * [simplify]: iters left: 3 (30 enodes) 5.058 * * [simplify]: iters left: 2 (87 enodes) 5.077 * * [simplify]: iters left: 1 (299 enodes) 5.179 * * [simplify]: Extracting #0: cost 1 inf + 0 5.179 * * [simplify]: Extracting #1: cost 33 inf + 0 5.180 * * [simplify]: Extracting #2: cost 175 inf + 1 5.181 * * [simplify]: Extracting #3: cost 298 inf + 3459 5.185 * * [simplify]: Extracting #4: cost 365 inf + 63464 5.204 * * [simplify]: Extracting #5: cost 78 inf + 302431 5.239 * * [simplify]: Extracting #6: cost 7 inf + 389376 5.277 * * [simplify]: Extracting #7: cost 0 inf + 400751 5.296 * [simplify]: Simplified to (*.p16 (+.p16 d4 (-.p16 d2 (+.p16 d3 d1))) d1) 5.296 * [simplify]: Simplified (2) to (λ (d1 d2 d3 d4) (*.p16 (+.p16 d4 (-.p16 d2 (+.p16 d3 d1))) d1)) 5.296 * * * * [progress]: [ 10 / 10 ] simplifiying candidate # 5.297 * [simplify]: Simplifying (*.p16 (+.p16 d4 (-.p16 d2 (+.p16 d3 d1))) d1) 5.297 * * [simplify]: iters left: 4 (8 enodes) 5.298 * * [simplify]: iters left: 3 (30 enodes) 5.303 * * [simplify]: iters left: 2 (87 enodes) 5.339 * * [simplify]: iters left: 1 (299 enodes) 5.489 * * [simplify]: Extracting #0: cost 1 inf + 0 5.489 * * [simplify]: Extracting #1: cost 33 inf + 0 5.490 * * [simplify]: Extracting #2: cost 175 inf + 1 5.491 * * [simplify]: Extracting #3: cost 298 inf + 3459 5.495 * * [simplify]: Extracting #4: cost 365 inf + 63464 5.507 * * [simplify]: Extracting #5: cost 78 inf + 302431 5.525 * * [simplify]: Extracting #6: cost 7 inf + 389376 5.545 * * [simplify]: Extracting #7: cost 0 inf + 400751 5.566 * [simplify]: Simplified to (*.p16 (+.p16 d4 (-.p16 d2 (+.p16 d3 d1))) d1) 5.566 * [simplify]: Simplified (2) to (λ (d1 d2 d3 d4) (*.p16 (+.p16 d4 (-.p16 d2 (+.p16 d3 d1))) d1)) 5.566 * * * [progress]: adding candidates to table 5.673 * * [progress]: iteration 4 / 4 5.673 * * * [progress]: picking best candidate 5.707 * * * * [pick]: Picked # 5.707 * * * [progress]: localizing error 5.800 * * * [progress]: generating rewritten candidates 5.800 * * * * [progress]: [ 1 / 2 ] rewriting at (2 1) 5.806 * * * * [progress]: [ 2 / 2 ] rewriting at (2) 5.813 * * * [progress]: generating series expansions 5.813 * * * * [progress]: [ 1 / 2 ] generating series at (2 1) 5.813 * * * * [progress]: [ 2 / 2 ] generating series at (2) 5.813 * * * [progress]: simplifying candidates 5.813 * * * * [progress]: [ 1 / 8 ] simplifiying candidate # 5.813 * [simplify]: Simplifying (-.p16 (+.p16 d4 d2) d3) 5.813 * * [simplify]: iters left: 2 (5 enodes) 5.814 * * [simplify]: iters left: 1 (21 enodes) 5.818 * * [simplify]: Extracting #0: cost 1 inf + 0 5.818 * * [simplify]: Extracting #1: cost 11 inf + 0 5.818 * * [simplify]: Extracting #2: cost 14 inf + 166 5.818 * * [simplify]: Extracting #3: cost 11 inf + 1908 5.818 * * [simplify]: Extracting #4: cost 0 inf + 8249 5.819 * [simplify]: Simplified to (+.p16 d4 (-.p16 d2 d3)) 5.819 * [simplify]: Simplified (2 1 1) to (λ (d1 d2 d3 d4) (*.p16 (-.p16 (+.p16 d4 (-.p16 d2 d3)) d1) d1)) 5.819 * * * * [progress]: [ 2 / 8 ] simplifiying candidate # 5.819 * [simplify]: Simplifying (-.p16 d2 (+.p16 d3 d1)) 5.819 * * [simplify]: iters left: 2 (5 enodes) 5.820 * * [simplify]: iters left: 1 (21 enodes) 5.823 * * [simplify]: Extracting #0: cost 1 inf + 0 5.823 * * [simplify]: Extracting #1: cost 11 inf + 0 5.823 * * [simplify]: Extracting #2: cost 16 inf + 84 5.823 * * [simplify]: Extracting #3: cost 12 inf + 1707 5.824 * * [simplify]: Extracting #4: cost 1 inf + 7969 5.830 * * [simplify]: Extracting #5: cost 0 inf + 8371 5.830 * [simplify]: Simplified to (-.p16 d2 (+.p16 d3 d1)) 5.830 * [simplify]: Simplified (2 1 2) to (λ (d1 d2 d3 d4) (*.p16 (+.p16 d4 (-.p16 d2 (+.p16 d3 d1))) d1)) 5.830 * * * * [progress]: [ 3 / 8 ] simplifiying candidate # 5.831 * [simplify]: Simplifying (neg.p16 (+.p16 d3 d1)) 5.831 * * [simplify]: iters left: 2 (4 enodes) 5.831 * * [simplify]: iters left: 1 (9 enodes) 5.832 * * [simplify]: Extracting #0: cost 1 inf + 0 5.832 * * [simplify]: Extracting #1: cost 2 inf + 0 5.832 * * [simplify]: Extracting #2: cost 4 inf + 0 5.832 * * [simplify]: Extracting #3: cost 2 inf + 2 5.833 * * [simplify]: Extracting #4: cost 0 inf + 166 5.833 * [simplify]: Simplified to (neg.p16 (+.p16 d1 d3)) 5.833 * [simplify]: Simplified (2 1 2) to (λ (d1 d2 d3 d4) (*.p16 (+.p16 (+.p16 d4 d2) (neg.p16 (+.p16 d1 d3))) d1)) 5.833 * * * * [progress]: [ 4 / 8 ] simplifiying candidate # 5.833 * [simplify]: Simplifying (-.p16 (*.p16 (+.p16 d4 d2) (+.p16 d4 d2)) (*.p16 (+.p16 d3 d1) (+.p16 d3 d1))) 5.833 * * [simplify]: iters left: 3 (9 enodes) 5.835 * * [simplify]: iters left: 2 (41 enodes) 5.843 * * [simplify]: iters left: 1 (152 enodes) 5.888 * * [simplify]: Extracting #0: cost 1 inf + 0 5.888 * * [simplify]: Extracting #1: cost 69 inf + 0 5.888 * * [simplify]: Extracting #2: cost 164 inf + 0 5.889 * * [simplify]: Extracting #3: cost 223 inf + 8418 5.896 * * [simplify]: Extracting #4: cost 88 inf + 134879 5.905 * * [simplify]: Extracting #5: cost 2 inf + 215279 5.914 * * [simplify]: Extracting #6: cost 0 inf + 217247 5.924 * * [simplify]: Extracting #7: cost 0 inf + 216847 5.933 * [simplify]: Simplified to (*.p16 (+.p16 d2 (-.p16 d4 (+.p16 d3 d1))) (+.p16 (+.p16 d2 d4) (+.p16 d3 d1))) 5.933 * [simplify]: Simplified (2 1 1) to (λ (d1 d2 d3 d4) (*.p16 (/.p16 (*.p16 (+.p16 d2 (-.p16 d4 (+.p16 d3 d1))) (+.p16 (+.p16 d2 d4) (+.p16 d3 d1))) (+.p16 (+.p16 d4 d2) (+.p16 d3 d1))) d1)) 5.933 * [simplify]: Simplifying (+.p16 (+.p16 d4 d2) (+.p16 d3 d1)) 5.933 * * [simplify]: iters left: 2 (7 enodes) 5.935 * * [simplify]: iters left: 1 (22 enodes) 5.938 * * [simplify]: Extracting #0: cost 1 inf + 0 5.938 * * [simplify]: Extracting #1: cost 13 inf + 0 5.938 * * [simplify]: Extracting #2: cost 10 inf + 129 5.938 * * [simplify]: Extracting #3: cost 0 inf + 836 5.938 * [simplify]: Simplified to (+.p16 (+.p16 d1 d3) (+.p16 d2 d4)) 5.938 * [simplify]: Simplified (2 1 2) to (λ (d1 d2 d3 d4) (*.p16 (/.p16 (*.p16 (+.p16 d2 (-.p16 d4 (+.p16 d3 d1))) (+.p16 (+.p16 d2 d4) (+.p16 d3 d1))) (+.p16 (+.p16 d1 d3) (+.p16 d2 d4))) d1)) 5.938 * * * * [progress]: [ 5 / 8 ] simplifiying candidate # 5.939 * [simplify]: Simplifying (*.p16 (-.p16 (*.p16 (+.p16 d4 d2) (+.p16 d4 d2)) (*.p16 (+.p16 d3 d1) (+.p16 d3 d1))) d1) 5.939 * * [simplify]: iters left: 4 (10 enodes) 5.941 * * [simplify]: iters left: 3 (43 enodes) 5.957 * * [simplify]: iters left: 2 (168 enodes) 6.023 * * [simplify]: Extracting #0: cost 1 inf + 0 6.023 * * [simplify]: Extracting #1: cost 31 inf + 0 6.023 * * [simplify]: Extracting #2: cost 165 inf + 1 6.025 * * [simplify]: Extracting #3: cost 234 inf + 12147 6.030 * * [simplify]: Extracting #4: cost 105 inf + 138464 6.040 * * [simplify]: Extracting #5: cost 4 inf + 235558 6.053 * * [simplify]: Extracting #6: cost 0 inf + 243654 6.065 * [simplify]: Simplified to (*.p16 (+.p16 d2 (-.p16 d4 (+.p16 d3 d1))) (*.p16 (+.p16 d1 (+.p16 (+.p16 d2 d4) d3)) d1)) 6.065 * [simplify]: Simplified (2 1) to (λ (d1 d2 d3 d4) (/.p16 (*.p16 (+.p16 d2 (-.p16 d4 (+.p16 d3 d1))) (*.p16 (+.p16 d1 (+.p16 (+.p16 d2 d4) d3)) d1)) (+.p16 (+.p16 d4 d2) (+.p16 d3 d1)))) 6.065 * * * * [progress]: [ 6 / 8 ] simplifiying candidate # 6.065 * * * * [progress]: [ 7 / 8 ] simplifiying candidate # 6.065 * [simplify]: Simplifying (+.p16 d4 d2) 6.065 * * [simplify]: iters left: 1 (3 enodes) 6.066 * * [simplify]: Extracting #0: cost 1 inf + 0 6.066 * * [simplify]: Extracting #1: cost 3 inf + 0 6.066 * * [simplify]: Extracting #2: cost 1 inf + 2 6.066 * * [simplify]: Extracting #3: cost 0 inf + 44 6.066 * [simplify]: Simplified to (+.p16 d2 d4) 6.066 * [simplify]: Simplified (2 1 1) to (λ (d1 d2 d3 d4) (*.p16 (-.p16 (+.p16 d2 d4) (+.p16 d3 d1)) d1)) 6.066 * * * * [progress]: [ 8 / 8 ] simplifiying candidate # 6.066 * [simplify]: Simplifying (+.p16 d4 d2) 6.066 * * [simplify]: iters left: 1 (3 enodes) 6.067 * * [simplify]: Extracting #0: cost 1 inf + 0 6.067 * * [simplify]: Extracting #1: cost 3 inf + 0 6.067 * * [simplify]: Extracting #2: cost 1 inf + 2 6.067 * * [simplify]: Extracting #3: cost 0 inf + 44 6.067 * [simplify]: Simplified to (+.p16 d2 d4) 6.067 * [simplify]: Simplified (2 1 1) to (λ (d1 d2 d3 d4) (*.p16 (-.p16 (+.p16 d2 d4) (+.p16 d3 d1)) d1)) 6.067 * * * [progress]: adding candidates to table 6.163 * [progress]: [Phase 3 of 3] Extracting. 6.163 * * [regime]: Finding splitpoints for: (# # # # # # #) 6.164 * * * [regime-changes]: Trying 4 branch expressions: (d4 d3 d2 d1) 6.164 * * * * [regimes]: Trying to branch on d4 from (# # # # # # #) 6.262 * * * * [regimes]: Trying to branch on d3 from (# # # # # # #) 6.364 * * * * [regimes]: Trying to branch on d2 from (# # # # # # #) 6.489 * * * * [regimes]: Trying to branch on d1 from (# # # # # # #) 6.587 * * * [regime]: Found split indices: #