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.005 * * * * [points]: Computing exacts on every 16 of 256 points to ramp up precision 0.006 * * * * [points]: Setting MPFR precision to 64 0.008 * * * * [points]: Setting MPFR precision to 320 0.010 * * * * [points]: Computing exacts on every 8 of 256 points to ramp up precision 0.011 * * * * [points]: Setting MPFR precision to 64 0.014 * * * * [points]: Setting MPFR precision to 320 0.017 * * * * [points]: Computing exacts on every 4 of 256 points to ramp up precision 0.019 * * * * [points]: Setting MPFR precision to 64 0.030 * * * * [points]: Setting MPFR precision to 320 0.035 * * * * [points]: Computing exacts on every 2 of 256 points to ramp up precision 0.036 * * * * [points]: Setting MPFR precision to 64 0.042 * * * * [points]: Setting MPFR precision to 320 0.051 * * * * [points]: Computing exacts for 256 points 0.052 * * * * [points]: Setting MPFR precision to 64 0.079 * * * * [points]: Setting MPFR precision to 320 0.103 * * * * [points]: Filtering points with unrepresentable outputs 0.104 * * * * [points]: Sampled 256 points with exact outputs 0.104 * * * [progress]: [2/2] Setting up program. 0.109 * [progress]: [Phase 2 of 3] Improving. 0.109 * * * * [progress]: [ 1 / 1 ] simplifiying candidate # 0.109 * [simplify]: Simplifying (-.p16 (+.p16 (-.p16 (*.p16 d1 d2) (*.p16 d1 d3)) (*.p16 d4 d1)) (*.p16 d1 d1)) 0.109 * * [simplify]: iters left: 4 (11 enodes) 0.112 * * [simplify]: iters left: 3 (43 enodes) 0.120 * * [simplify]: iters left: 2 (148 enodes) 0.180 * * [simplify]: Extracting #0: cost 1 inf + 0 0.180 * * [simplify]: Extracting #1: cost 40 inf + 0 0.180 * * [simplify]: Extracting #2: cost 128 inf + 322 0.181 * * [simplify]: Extracting #3: cost 222 inf + 10234 0.185 * * [simplify]: Extracting #4: cost 153 inf + 124713 0.193 * * [simplify]: Extracting #5: cost 28 inf + 253727 0.204 * * [simplify]: Extracting #6: cost 1 inf + 271088 0.221 * * [simplify]: Extracting #7: cost 0 inf + 269810 0.245 * * [simplify]: Extracting #8: cost 0 inf + 269170 0.261 * [simplify]: Simplified to (*.p16 d1 (+.p16 (-.p16 d2 d3) (-.p16 d4 d1))) 0.261 * [simplify]: Simplified (2) to (λ (d1 d2 d3 d4) (*.p16 d1 (+.p16 (-.p16 d2 d3) (-.p16 d4 d1)))) 0.281 * * [progress]: iteration 1 / 4 0.281 * * * [progress]: picking best candidate 0.299 * * * * [pick]: Picked # 0.300 * * * [progress]: localizing error 0.385 * * * [progress]: generating rewritten candidates 0.385 * * * * [progress]: [ 1 / 2 ] rewriting at (2 2) 0.392 * * * * [progress]: [ 2 / 2 ] rewriting at (2) 0.401 * * * [progress]: generating series expansions 0.401 * * * * [progress]: [ 1 / 2 ] generating series at (2 2) 0.401 * * * * [progress]: [ 2 / 2 ] generating series at (2) 0.402 * * * [progress]: simplifying candidates 0.402 * * * * [progress]: [ 1 / 10 ] simplifiying candidate # 0.402 * [simplify]: Simplifying (neg.p16 d1) 0.402 * * [simplify]: iters left: 1 (2 enodes) 0.402 * * [simplify]: Extracting #0: cost 1 inf + 0 0.402 * * [simplify]: Extracting #1: cost 2 inf + 0 0.402 * * [simplify]: Extracting #2: cost 1 inf + 1 0.402 * * [simplify]: Extracting #3: cost 0 inf + 82 0.402 * [simplify]: Simplified to (neg.p16 d1) 0.402 * [simplify]: Simplified (2 2 2) to (λ (d1 d2 d3 d4) (*.p16 d1 (+.p16 (+.p16 (-.p16 d2 d3) d4) (neg.p16 d1)))) 0.402 * * * * [progress]: [ 2 / 10 ] simplifiying candidate # 0.402 * * * * [progress]: [ 3 / 10 ] simplifiying candidate # 0.402 * * * * [progress]: [ 4 / 10 ] simplifiying candidate # 0.402 * * * * [progress]: [ 5 / 10 ] simplifiying candidate # 0.403 * * * * [progress]: [ 6 / 10 ] simplifiying candidate # 0.403 * [simplify]: Simplifying (*.p16 d1 (-.p16 d4 d1)) 0.403 * * [simplify]: iters left: 2 (4 enodes) 0.404 * * [simplify]: iters left: 1 (16 enodes) 0.406 * * [simplify]: Extracting #0: cost 1 inf + 0 0.406 * * [simplify]: Extracting #1: cost 10 inf + 0 0.406 * * [simplify]: Extracting #2: cost 12 inf + 1 0.406 * * [simplify]: Extracting #3: cost 11 inf + 1249 0.406 * * [simplify]: Extracting #4: cost 6 inf + 3901 0.407 * * [simplify]: Extracting #5: cost 1 inf + 7028 0.407 * * [simplify]: Extracting #6: cost 0 inf + 8390 0.407 * [simplify]: Simplified to (*.p16 d1 (-.p16 d4 d1)) 0.407 * [simplify]: Simplified (2 2) to (λ (d1 d2 d3 d4) (+.p16 (*.p16 d1 (-.p16 d2 d3)) (*.p16 d1 (-.p16 d4 d1)))) 0.407 * * * * [progress]: [ 7 / 10 ] simplifiying candidate # 0.407 * [simplify]: Simplifying (*.p16 (-.p16 d4 d1) d1) 0.408 * * [simplify]: iters left: 2 (4 enodes) 0.408 * * [simplify]: iters left: 1 (16 enodes) 0.411 * * [simplify]: Extracting #0: cost 1 inf + 0 0.411 * * [simplify]: Extracting #1: cost 10 inf + 0 0.411 * * [simplify]: Extracting #2: cost 12 inf + 1 0.411 * * [simplify]: Extracting #3: cost 13 inf + 885 0.411 * * [simplify]: Extracting #4: cost 8 inf + 2697 0.411 * * [simplify]: Extracting #5: cost 2 inf + 6266 0.412 * * [simplify]: Extracting #6: cost 0 inf + 8390 0.412 * [simplify]: Simplified to (*.p16 (-.p16 d4 d1) d1) 0.412 * [simplify]: Simplified (2 2) to (λ (d1 d2 d3 d4) (+.p16 (*.p16 (-.p16 d2 d3) d1) (*.p16 (-.p16 d4 d1) d1))) 0.412 * * * * [progress]: [ 8 / 10 ] simplifiying candidate # 0.412 * * * * [progress]: [ 9 / 10 ] simplifiying candidate # 0.412 * [simplify]: Simplifying (*.p16 d1 (+.p16 (-.p16 d2 d3) (-.p16 d4 d1))) 0.412 * * [simplify]: iters left: 3 (8 enodes) 0.414 * * [simplify]: iters left: 2 (42 enodes) 0.421 * * [simplify]: iters left: 1 (117 enodes) 0.449 * * [simplify]: Extracting #0: cost 1 inf + 0 0.449 * * [simplify]: Extracting #1: cost 24 inf + 0 0.449 * * [simplify]: Extracting #2: cost 56 inf + 1 0.450 * * [simplify]: Extracting #3: cost 108 inf + 1181 0.451 * * [simplify]: Extracting #4: cost 85 inf + 24120 0.456 * * [simplify]: Extracting #5: cost 33 inf + 70189 0.460 * * [simplify]: Extracting #6: cost 1 inf + 97168 0.465 * * [simplify]: Extracting #7: cost 0 inf + 98411 0.469 * [simplify]: Simplified to (*.p16 (+.p16 (-.p16 d2 d3) (-.p16 d4 d1)) d1) 0.469 * [simplify]: Simplified (2) to (λ (d1 d2 d3 d4) (*.p16 (+.p16 (-.p16 d2 d3) (-.p16 d4 d1)) d1)) 0.469 * * * * [progress]: [ 10 / 10 ] simplifiying candidate # 0.469 * [simplify]: Simplifying (*.p16 d1 (+.p16 (-.p16 d2 d3) (-.p16 d4 d1))) 0.469 * * [simplify]: iters left: 3 (8 enodes) 0.471 * * [simplify]: iters left: 2 (42 enodes) 0.480 * * [simplify]: iters left: 1 (117 enodes) 0.518 * * [simplify]: Extracting #0: cost 1 inf + 0 0.518 * * [simplify]: Extracting #1: cost 24 inf + 0 0.518 * * [simplify]: Extracting #2: cost 56 inf + 1 0.518 * * [simplify]: Extracting #3: cost 108 inf + 1181 0.520 * * [simplify]: Extracting #4: cost 85 inf + 24120 0.523 * * [simplify]: Extracting #5: cost 33 inf + 70189 0.527 * * [simplify]: Extracting #6: cost 1 inf + 97168 0.531 * * [simplify]: Extracting #7: cost 0 inf + 98411 0.535 * [simplify]: Simplified to (*.p16 (+.p16 (-.p16 d2 d3) (-.p16 d4 d1)) d1) 0.535 * [simplify]: Simplified (2) to (λ (d1 d2 d3 d4) (*.p16 (+.p16 (-.p16 d2 d3) (-.p16 d4 d1)) d1)) 0.535 * * * [progress]: adding candidates to table 0.692 * * [progress]: iteration 2 / 4 0.692 * * * [progress]: picking best candidate 0.710 * * * * [pick]: Picked # 0.710 * * * [progress]: localizing error 0.822 * * * [progress]: generating rewritten candidates 0.822 * * * * [progress]: [ 1 / 3 ] rewriting at (2 2) 0.825 * * * * [progress]: [ 2 / 3 ] rewriting at (2) 0.831 * * * * [progress]: [ 3 / 3 ] rewriting at (2 2 2) 0.835 * * * [progress]: generating series expansions 0.835 * * * * [progress]: [ 1 / 3 ] generating series at (2 2) 0.835 * * * * [progress]: [ 2 / 3 ] generating series at (2) 0.835 * * * * [progress]: [ 3 / 3 ] generating series at (2 2 2) 0.835 * * * [progress]: simplifying candidates 0.835 * * * * [progress]: [ 1 / 18 ] simplifiying candidate # 0.835 * * * * [progress]: [ 2 / 18 ] simplifiying candidate # 0.835 * [simplify]: Simplifying (neg.p16 (-.p16 d4 d1)) 0.835 * * [simplify]: iters left: 2 (4 enodes) 0.837 * * [simplify]: iters left: 1 (15 enodes) 0.841 * * [simplify]: Extracting #0: cost 1 inf + 0 0.841 * * [simplify]: Extracting #1: cost 2 inf + 0 0.841 * * [simplify]: Extracting #2: cost 7 inf + 0 0.841 * * [simplify]: Extracting #3: cost 9 inf + 83 0.842 * * [simplify]: Extracting #4: cost 4 inf + 2134 0.842 * * [simplify]: Extracting #5: cost 0 inf + 5180 0.842 * [simplify]: Simplified to (neg.p16 (-.p16 d4 d1)) 0.842 * [simplify]: Simplified (2 2 2) to (λ (d1 d2 d3 d4) (*.p16 d1 (-.p16 (-.p16 d2 d3) (neg.p16 (-.p16 d4 d1))))) 0.842 * * * * [progress]: [ 3 / 18 ] simplifiying candidate # 0.843 * [simplify]: Simplifying (-.p16 d4 d1) 0.843 * * [simplify]: iters left: 1 (3 enodes) 0.844 * * [simplify]: Extracting #0: cost 1 inf + 0 0.844 * * [simplify]: Extracting #1: cost 6 inf + 0 0.844 * * [simplify]: Extracting #2: cost 5 inf + 44 0.844 * * [simplify]: Extracting #3: cost 0 inf + 1571 0.844 * [simplify]: Simplified to (-.p16 d4 d1) 0.844 * [simplify]: Simplified (2 2 2) to (λ (d1 d2 d3 d4) (*.p16 d1 (+.p16 (-.p16 d2 d3) (-.p16 d4 d1)))) 0.844 * * * * [progress]: [ 4 / 18 ] simplifiying candidate # 0.845 * * * * [progress]: [ 5 / 18 ] simplifiying candidate # 0.845 * * * * [progress]: [ 6 / 18 ] simplifiying candidate # 0.845 * [simplify]: Simplifying (*.p16 d1 (-.p16 d4 d1)) 0.845 * * [simplify]: iters left: 2 (4 enodes) 0.847 * * [simplify]: iters left: 1 (16 enodes) 0.851 * * [simplify]: Extracting #0: cost 1 inf + 0 0.852 * * [simplify]: Extracting #1: cost 10 inf + 0 0.852 * * [simplify]: Extracting #2: cost 12 inf + 1 0.852 * * [simplify]: Extracting #3: cost 11 inf + 1249 0.852 * * [simplify]: Extracting #4: cost 6 inf + 3901 0.852 * * [simplify]: Extracting #5: cost 1 inf + 7028 0.853 * * [simplify]: Extracting #6: cost 0 inf + 8390 0.853 * [simplify]: Simplified to (*.p16 d1 (-.p16 d4 d1)) 0.853 * [simplify]: Simplified (2 2) to (λ (d1 d2 d3 d4) (+.p16 (*.p16 d1 (-.p16 d2 d3)) (*.p16 d1 (-.p16 d4 d1)))) 0.853 * * * * [progress]: [ 7 / 18 ] simplifiying candidate # 0.854 * [simplify]: Simplifying (*.p16 d1 (neg.p16 (-.p16 d3 (-.p16 d4 d1)))) 0.854 * * [simplify]: iters left: 4 (7 enodes) 0.857 * * [simplify]: iters left: 3 (30 enodes) 0.866 * * [simplify]: iters left: 2 (69 enodes) 0.887 * * [simplify]: iters left: 1 (247 enodes) 1.007 * * [simplify]: Extracting #0: cost 1 inf + 0 1.007 * * [simplify]: Extracting #1: cost 3 inf + 0 1.007 * * [simplify]: Extracting #2: cost 3 inf + 1 1.007 * * [simplify]: Extracting #3: cost 37 inf + 1 1.007 * * [simplify]: Extracting #4: cost 169 inf + 571 1.009 * * [simplify]: Extracting #5: cost 315 inf + 23094 1.021 * * [simplify]: Extracting #6: cost 214 inf + 199639 1.041 * * [simplify]: Extracting #7: cost 28 inf + 439637 1.068 * * [simplify]: Extracting #8: cost 0 inf + 479601 1.111 * [simplify]: Simplified to (*.p16 d1 (neg.p16 (-.p16 (+.p16 d3 d1) d4))) 1.111 * [simplify]: Simplified (2 2) to (λ (d1 d2 d3 d4) (+.p16 (*.p16 d1 d2) (*.p16 d1 (neg.p16 (-.p16 (+.p16 d3 d1) d4))))) 1.111 * * * * [progress]: [ 8 / 18 ] simplifiying candidate # 1.111 * [simplify]: Simplifying (*.p16 (-.p16 d4 d1) d1) 1.111 * * [simplify]: iters left: 2 (4 enodes) 1.113 * * [simplify]: iters left: 1 (16 enodes) 1.118 * * [simplify]: Extracting #0: cost 1 inf + 0 1.118 * * [simplify]: Extracting #1: cost 10 inf + 0 1.118 * * [simplify]: Extracting #2: cost 12 inf + 1 1.119 * * [simplify]: Extracting #3: cost 13 inf + 885 1.119 * * [simplify]: Extracting #4: cost 8 inf + 2697 1.119 * * [simplify]: Extracting #5: cost 2 inf + 6266 1.120 * * [simplify]: Extracting #6: cost 0 inf + 8390 1.120 * [simplify]: Simplified to (*.p16 (-.p16 d4 d1) d1) 1.120 * [simplify]: Simplified (2 2) to (λ (d1 d2 d3 d4) (+.p16 (*.p16 (-.p16 d2 d3) d1) (*.p16 (-.p16 d4 d1) d1))) 1.120 * * * * [progress]: [ 9 / 18 ] simplifiying candidate # 1.121 * [simplify]: Simplifying (*.p16 (neg.p16 (-.p16 d3 (-.p16 d4 d1))) d1) 1.121 * * [simplify]: iters left: 4 (7 enodes) 1.124 * * [simplify]: iters left: 3 (30 enodes) 1.134 * * [simplify]: iters left: 2 (69 enodes) 1.148 * * [simplify]: iters left: 1 (247 enodes) 1.268 * * [simplify]: Extracting #0: cost 1 inf + 0 1.268 * * [simplify]: Extracting #1: cost 3 inf + 0 1.269 * * [simplify]: Extracting #2: cost 3 inf + 1 1.269 * * [simplify]: Extracting #3: cost 37 inf + 1 1.270 * * [simplify]: Extracting #4: cost 170 inf + 449 1.273 * * [simplify]: Extracting #5: cost 322 inf + 18638 1.285 * * [simplify]: Extracting #6: cost 278 inf + 125122 1.317 * * [simplify]: Extracting #7: cost 38 inf + 422646 1.338 * * [simplify]: Extracting #8: cost 1 inf + 477317 1.367 * * [simplify]: Extracting #9: cost 0 inf + 479879 1.403 * [simplify]: Simplified to (*.p16 d1 (neg.p16 (-.p16 (+.p16 d1 d3) d4))) 1.403 * [simplify]: Simplified (2 2) to (λ (d1 d2 d3 d4) (+.p16 (*.p16 d2 d1) (*.p16 d1 (neg.p16 (-.p16 (+.p16 d1 d3) d4))))) 1.403 * * * * [progress]: [ 10 / 18 ] simplifiying candidate # 1.403 * [simplify]: Simplifying (+.p16 d2 (-.p16 d3 (-.p16 d4 d1))) 1.404 * * [simplify]: iters left: 3 (7 enodes) 1.406 * * [simplify]: iters left: 2 (34 enodes) 1.415 * * [simplify]: iters left: 1 (90 enodes) 1.436 * * [simplify]: Extracting #0: cost 1 inf + 0 1.436 * * [simplify]: Extracting #1: cost 22 inf + 0 1.436 * * [simplify]: Extracting #2: cost 52 inf + 167 1.437 * * [simplify]: Extracting #3: cost 73 inf + 7807 1.439 * * [simplify]: Extracting #4: cost 49 inf + 32248 1.443 * * [simplify]: Extracting #5: cost 5 inf + 71213 1.450 * * [simplify]: Extracting #6: cost 0 inf + 79303 1.457 * [simplify]: Simplified to (+.p16 (+.p16 d2 d1) (-.p16 d3 d4)) 1.457 * [simplify]: Simplified (2 2) to (λ (d1 d2 d3 d4) (/.p16 (*.p16 d1 (-.p16 (*.p16 d2 d2) (*.p16 (-.p16 d3 (-.p16 d4 d1)) (-.p16 d3 (-.p16 d4 d1))))) (+.p16 (+.p16 d2 d1) (-.p16 d3 d4)))) 1.457 * * * * [progress]: [ 11 / 18 ] simplifiying candidate # 1.457 * * * * [progress]: [ 12 / 18 ] simplifiying candidate # 1.458 * [simplify]: Simplifying (neg.p16 d1) 1.458 * * [simplify]: iters left: 1 (2 enodes) 1.459 * * [simplify]: Extracting #0: cost 1 inf + 0 1.459 * * [simplify]: Extracting #1: cost 2 inf + 0 1.459 * * [simplify]: Extracting #2: cost 1 inf + 1 1.459 * * [simplify]: Extracting #3: cost 0 inf + 82 1.459 * [simplify]: Simplified to (neg.p16 d1) 1.459 * [simplify]: Simplified (2 2 2 2) to (λ (d1 d2 d3 d4) (*.p16 d1 (-.p16 d2 (-.p16 (-.p16 d3 d4) (neg.p16 d1))))) 1.459 * * * * [progress]: [ 13 / 18 ] simplifiying candidate # 1.459 * * * * [progress]: [ 14 / 18 ] simplifiying candidate # 1.459 * * * * [progress]: [ 15 / 18 ] simplifiying candidate # 1.459 * * * * [progress]: [ 16 / 18 ] simplifiying candidate # 1.459 * * * * [progress]: [ 17 / 18 ] simplifiying candidate # 1.459 * * * * [progress]: [ 18 / 18 ] simplifiying candidate # 1.459 * * * [progress]: adding candidates to table 1.783 * * [progress]: iteration 3 / 4 1.783 * * * [progress]: picking best candidate 1.808 * * * * [pick]: Picked # 1.808 * * * [progress]: localizing error 1.926 * * * [progress]: generating rewritten candidates 1.926 * * * * [progress]: [ 1 / 3 ] rewriting at (2) 1.929 * * * * [progress]: [ 2 / 3 ] rewriting at (2 2) 1.931 * * * * [progress]: [ 3 / 3 ] rewriting at (2 2 2 1) 1.944 * * * [progress]: generating series expansions 1.944 * * * * [progress]: [ 1 / 3 ] generating series at (2) 1.944 * * * * [progress]: [ 2 / 3 ] generating series at (2 2) 1.944 * * * * [progress]: [ 3 / 3 ] generating series at (2 2 2 1) 1.944 * * * [progress]: simplifying candidates 1.944 * * * * [progress]: [ 1 / 8 ] simplifiying candidate # 1.944 * * * * [progress]: [ 2 / 8 ] simplifiying candidate # 1.944 * * * * [progress]: [ 3 / 8 ] simplifiying candidate # 1.944 * * * * [progress]: [ 4 / 8 ] simplifiying candidate # 1.944 * * * * [progress]: [ 5 / 8 ] simplifiying candidate # 1.944 * * * * [progress]: [ 6 / 8 ] simplifiying candidate # 1.945 * [simplify]: Simplifying (+.p16 (*.p16 d2 d1) (*.p16 d1 (neg.p16 (-.p16 (+.p16 d1 d3) d4)))) 1.945 * * [simplify]: iters left: 5 (10 enodes) 1.947 * * [simplify]: iters left: 4 (31 enodes) 1.951 * * [simplify]: iters left: 3 (67 enodes) 1.965 * * [simplify]: iters left: 2 (190 enodes) 2.071 * * [simplify]: Extracting #0: cost 1 inf + 0 2.071 * * [simplify]: Extracting #1: cost 5 inf + 0 2.072 * * [simplify]: Extracting #2: cost 22 inf + 1 2.072 * * [simplify]: Extracting #3: cost 42 inf + 4 2.073 * * [simplify]: Extracting #4: cost 143 inf + 4658 2.077 * * [simplify]: Extracting #5: cost 259 inf + 31799 2.093 * * [simplify]: Extracting #6: cost 42 inf + 214783 2.111 * * [simplify]: Extracting #7: cost 1 inf + 270921 2.124 * * [simplify]: Extracting #8: cost 0 inf + 273604 2.138 * [simplify]: Simplified to (*.p16 d1 (+.p16 (-.p16 d2 (+.p16 d3 d1)) d4)) 2.138 * [simplify]: Simplified (2) to (λ (d1 d2 d3 d4) (*.p16 d1 (+.p16 (-.p16 d2 (+.p16 d3 d1)) d4))) 2.138 * * * * [progress]: [ 7 / 8 ] simplifiying candidate # 2.138 * [simplify]: Simplifying (+.p16 (*.p16 d2 d1) (*.p16 d1 (neg.p16 (-.p16 (+.p16 d1 d3) d4)))) 2.138 * * [simplify]: iters left: 5 (10 enodes) 2.140 * * [simplify]: iters left: 4 (31 enodes) 2.145 * * [simplify]: iters left: 3 (67 enodes) 2.158 * * [simplify]: iters left: 2 (190 enodes) 2.227 * * [simplify]: Extracting #0: cost 1 inf + 0 2.227 * * [simplify]: Extracting #1: cost 5 inf + 0 2.227 * * [simplify]: Extracting #2: cost 22 inf + 1 2.227 * * [simplify]: Extracting #3: cost 42 inf + 4 2.228 * * [simplify]: Extracting #4: cost 143 inf + 4658 2.230 * * [simplify]: Extracting #5: cost 259 inf + 31799 2.238 * * [simplify]: Extracting #6: cost 42 inf + 214783 2.255 * * [simplify]: Extracting #7: cost 1 inf + 270921 2.277 * * [simplify]: Extracting #8: cost 0 inf + 273604 2.289 * [simplify]: Simplified to (*.p16 d1 (+.p16 (-.p16 d2 (+.p16 d3 d1)) d4)) 2.289 * [simplify]: Simplified (2) to (λ (d1 d2 d3 d4) (*.p16 d1 (+.p16 (-.p16 d2 (+.p16 d3 d1)) d4))) 2.289 * * * * [progress]: [ 8 / 8 ] simplifiying candidate # 2.289 * [simplify]: Simplifying (+.p16 (*.p16 d2 d1) (*.p16 d1 (neg.p16 (-.p16 (+.p16 d1 d3) d4)))) 2.289 * * [simplify]: iters left: 5 (10 enodes) 2.291 * * [simplify]: iters left: 4 (31 enodes) 2.297 * * [simplify]: iters left: 3 (67 enodes) 2.320 * * [simplify]: iters left: 2 (190 enodes) 2.390 * * [simplify]: Extracting #0: cost 1 inf + 0 2.390 * * [simplify]: Extracting #1: cost 5 inf + 0 2.390 * * [simplify]: Extracting #2: cost 22 inf + 1 2.390 * * [simplify]: Extracting #3: cost 42 inf + 4 2.390 * * [simplify]: Extracting #4: cost 143 inf + 4658 2.393 * * [simplify]: Extracting #5: cost 259 inf + 31799 2.401 * * [simplify]: Extracting #6: cost 42 inf + 214783 2.414 * * [simplify]: Extracting #7: cost 1 inf + 270921 2.428 * * [simplify]: Extracting #8: cost 0 inf + 273604 2.440 * [simplify]: Simplified to (*.p16 d1 (+.p16 (-.p16 d2 (+.p16 d3 d1)) d4)) 2.440 * [simplify]: Simplified (2) to (λ (d1 d2 d3 d4) (*.p16 d1 (+.p16 (-.p16 d2 (+.p16 d3 d1)) d4))) 2.441 * * * [progress]: adding candidates to table 2.647 * * [progress]: iteration 4 / 4 2.647 * * * [progress]: picking best candidate 2.689 * * * * [pick]: Picked # 2.689 * * * [progress]: localizing error 2.789 * * * [progress]: generating rewritten candidates 2.789 * * * * [progress]: [ 1 / 3 ] rewriting at (2) 2.795 * * * * [progress]: [ 2 / 3 ] rewriting at (2 2) 2.801 * * * * [progress]: [ 3 / 3 ] rewriting at (2 2 1) 2.815 * * * [progress]: generating series expansions 2.815 * * * * [progress]: [ 1 / 3 ] generating series at (2) 2.815 * * * * [progress]: [ 2 / 3 ] generating series at (2 2) 2.815 * * * * [progress]: [ 3 / 3 ] generating series at (2 2 1) 2.815 * * * [progress]: simplifying candidates 2.815 * * * * [progress]: [ 1 / 12 ] simplifiying candidate # 2.816 * [simplify]: Simplifying (*.p16 d1 d4) 2.816 * * [simplify]: iters left: 1 (3 enodes) 2.817 * * [simplify]: Extracting #0: cost 1 inf + 0 2.817 * * [simplify]: Extracting #1: cost 3 inf + 0 2.817 * * [simplify]: Extracting #2: cost 1 inf + 2 2.817 * * [simplify]: Extracting #3: cost 0 inf + 324 2.817 * [simplify]: Simplified to (*.p16 d4 d1) 2.817 * [simplify]: Simplified (2 2) to (λ (d1 d2 d3 d4) (+.p16 (*.p16 d1 (-.p16 d2 (+.p16 d3 d1))) (*.p16 d4 d1))) 2.817 * * * * [progress]: [ 2 / 12 ] simplifiying candidate # 2.818 * [simplify]: Simplifying (*.p16 d4 d1) 2.818 * * [simplify]: iters left: 1 (3 enodes) 2.819 * * [simplify]: Extracting #0: cost 1 inf + 0 2.819 * * [simplify]: Extracting #1: cost 3 inf + 0 2.819 * * [simplify]: Extracting #2: cost 1 inf + 2 2.819 * * [simplify]: Extracting #3: cost 0 inf + 324 2.820 * [simplify]: Simplified to (*.p16 d1 d4) 2.820 * [simplify]: Simplified (2 2) to (λ (d1 d2 d3 d4) (+.p16 (*.p16 (-.p16 d2 (+.p16 d3 d1)) d1) (*.p16 d1 d4))) 2.820 * * * * [progress]: [ 3 / 12 ] simplifiying candidate # 2.820 * * * * [progress]: [ 4 / 12 ] simplifiying candidate # 2.820 * * * * [progress]: [ 5 / 12 ] simplifiying candidate # 2.820 * * * * [progress]: [ 6 / 12 ] simplifiying candidate # 2.820 * * * * [progress]: [ 7 / 12 ] simplifiying candidate # 2.820 * * * * [progress]: [ 8 / 12 ] simplifiying candidate # 2.820 * * * * [progress]: [ 9 / 12 ] simplifiying candidate # 2.820 * * * * [progress]: [ 10 / 12 ] simplifiying candidate # 2.820 * [simplify]: Simplifying (*.p16 d1 (+.p16 (-.p16 d2 (+.p16 d3 d1)) d4)) 2.820 * * [simplify]: iters left: 4 (8 enodes) 2.824 * * [simplify]: iters left: 3 (36 enodes) 2.838 * * [simplify]: iters left: 2 (103 enodes) 2.879 * * [simplify]: iters left: 1 (345 enodes) 3.048 * * [simplify]: Extracting #0: cost 1 inf + 0 3.048 * * [simplify]: Extracting #1: cost 27 inf + 0 3.049 * * [simplify]: Extracting #2: cost 165 inf + 1 3.050 * * [simplify]: Extracting #3: cost 396 inf + 3691 3.056 * * [simplify]: Extracting #4: cost 421 inf + 104784 3.082 * * [simplify]: Extracting #5: cost 81 inf + 406266 3.133 * * [simplify]: Extracting #6: cost 3 inf + 500493 3.180 * * [simplify]: Extracting #7: cost 0 inf + 505062 3.215 * [simplify]: Simplified to (*.p16 (-.p16 (+.p16 d4 d2) (+.p16 d3 d1)) d1) 3.215 * [simplify]: Simplified (2) to (λ (d1 d2 d3 d4) (*.p16 (-.p16 (+.p16 d4 d2) (+.p16 d3 d1)) d1)) 3.215 * * * * [progress]: [ 11 / 12 ] simplifiying candidate # 3.215 * [simplify]: Simplifying (*.p16 d1 (+.p16 (-.p16 d2 (+.p16 d3 d1)) d4)) 3.216 * * [simplify]: iters left: 4 (8 enodes) 3.217 * * [simplify]: iters left: 3 (36 enodes) 3.224 * * [simplify]: iters left: 2 (103 enodes) 3.262 * * [simplify]: iters left: 1 (345 enodes) 3.483 * * [simplify]: Extracting #0: cost 1 inf + 0 3.483 * * [simplify]: Extracting #1: cost 27 inf + 0 3.483 * * [simplify]: Extracting #2: cost 165 inf + 1 3.484 * * [simplify]: Extracting #3: cost 396 inf + 3691 3.495 * * [simplify]: Extracting #4: cost 421 inf + 104784 3.526 * * [simplify]: Extracting #5: cost 81 inf + 406266 3.556 * * [simplify]: Extracting #6: cost 3 inf + 500493 3.596 * * [simplify]: Extracting #7: cost 0 inf + 505062 3.628 * [simplify]: Simplified to (*.p16 (-.p16 (+.p16 d4 d2) (+.p16 d3 d1)) d1) 3.628 * [simplify]: Simplified (2) to (λ (d1 d2 d3 d4) (*.p16 (-.p16 (+.p16 d4 d2) (+.p16 d3 d1)) d1)) 3.628 * * * * [progress]: [ 12 / 12 ] simplifiying candidate # 3.628 * [simplify]: Simplifying (*.p16 d1 (+.p16 (-.p16 d2 (+.p16 d3 d1)) d4)) 3.628 * * [simplify]: iters left: 4 (8 enodes) 3.630 * * [simplify]: iters left: 3 (36 enodes) 3.636 * * [simplify]: iters left: 2 (103 enodes) 3.663 * * [simplify]: iters left: 1 (345 enodes) 4.293 * * [simplify]: Extracting #0: cost 1 inf + 0 4.293 * * [simplify]: Extracting #1: cost 27 inf + 0 4.294 * * [simplify]: Extracting #2: cost 165 inf + 1 4.297 * * [simplify]: Extracting #3: cost 396 inf + 3691 4.307 * * [simplify]: Extracting #4: cost 421 inf + 104784 4.340 * * [simplify]: Extracting #5: cost 81 inf + 406266 4.371 * * [simplify]: Extracting #6: cost 3 inf + 500493 4.413 * * [simplify]: Extracting #7: cost 0 inf + 505062 4.443 * [simplify]: Simplified to (*.p16 (-.p16 (+.p16 d4 d2) (+.p16 d3 d1)) d1) 4.443 * [simplify]: Simplified (2) to (λ (d1 d2 d3 d4) (*.p16 (-.p16 (+.p16 d4 d2) (+.p16 d3 d1)) d1)) 4.443 * * * [progress]: adding candidates to table 4.644 * [progress]: [Phase 3 of 3] Extracting. 4.644 * * [regime]: Finding splitpoints for: (# # # # # # #) 4.646 * * * [regime-changes]: Trying 4 branch expressions: (d4 d3 d2 d1) 4.646 * * * * [regimes]: Trying to branch on d4 from (# # # # # # #) 4.840 * * * * [regimes]: Trying to branch on d3 from (# # # # # # #) 4.973 * * * * [regimes]: Trying to branch on d2 from (# # # # # # #) 5.091 * * * * [regimes]: Trying to branch on d1 from (# # # # # # #) 5.214 * * * [regime]: Found split indices: #