1550842923.302 * [misc]progress: [Phase 1 of 3] Setting up. 1550842923.302 * * * [misc]progress: [1/2] Preparing points 1550842923.302 * * * * [misc]points: Sampling 256 additional inputs, on iter 0 have 0 / 256 1550842923.303 * * * * [misc]points: Computing exacts on every 16 of 256 points to ramp up precision 1550842923.305 * * * * [misc]points: Setting MPFR precision to 64 1550842923.310 * * * * [misc]points: Setting MPFR precision to 320 1550842923.312 * * * * [misc]points: Computing exacts on every 8 of 256 points to ramp up precision 1550842923.316 * * * * [misc]points: Setting MPFR precision to 64 1550842923.319 * * * * [misc]points: Setting MPFR precision to 320 1550842923.322 * * * * [misc]points: Computing exacts on every 4 of 256 points to ramp up precision 1550842923.326 * * * * [misc]points: Setting MPFR precision to 64 1550842923.331 * * * * [misc]points: Setting MPFR precision to 320 1550842923.338 * * * * [misc]points: Computing exacts on every 2 of 256 points to ramp up precision 1550842923.342 * * * * [misc]points: Setting MPFR precision to 64 1550842923.351 * * * * [misc]points: Setting MPFR precision to 320 1550842923.362 * * * * [misc]points: Computing exacts for 256 points 1550842923.366 * * * * [misc]points: Setting MPFR precision to 64 1550842923.391 * * * * [misc]points: Setting MPFR precision to 320 1550842923.411 * * * * [misc]points: Filtering points with unrepresentable outputs 1550842923.428 * * * * [misc]points: Sampling 4 additional inputs, on iter 1 have 255 / 256 1550842923.428 * * * * [misc]points: Computing exacts for 4 points 1550842923.430 * * * * [misc]points: Setting MPFR precision to 64 1550842923.431 * * * * [misc]points: Setting MPFR precision to 320 1550842923.431 * * * * [misc]points: Filtering points with unrepresentable outputs 1550842923.431 * * * * [exit]points: Sampled 259 points with exact outputs 1550842923.432 * * * [misc]progress: [2/2] Setting up program. 1550842923.455 * [misc]progress: [Phase 2 of 3] Improving. 1550842923.455 * * * * [misc]progress: [ 1 / 1 ] simplifiying candidate #posit16 5)) d1)) (*.p16 d1 (real->posit16 32))))> 1550842923.472 * [enter]simplify: Simplifying (+.p16 (+.p16 (*.p16 d1 d2) (*.p16 (+.p16 d3 (real->posit16 5)) d1)) (*.p16 d1 (real->posit16 32))) 1550842923.472 * * [misc]simplify: iters left: 5 (13 enodes) 1550842923.475 * * [misc]simplify: iters left: 4 (29 enodes) 1550842923.480 * * [misc]simplify: iters left: 3 (49 enodes) 1550842923.492 * * [misc]simplify: iters left: 2 (122 enodes) 1550842923.515 * * [misc]simplify: iters left: 1 (228 enodes) 1550842923.578 * * [misc]simplify: Extracting #0: cost 1 inf + 0 1550842923.578 * * [misc]simplify: Extracting #1: cost 23 inf + 0 1550842923.578 * * [misc]simplify: Extracting #2: cost 50 inf + 1 1550842923.578 * * [misc]simplify: Extracting #3: cost 49 inf + 325 1550842923.579 * * [misc]simplify: Extracting #4: cost 29 inf + 4935 1550842923.580 * * [misc]simplify: Extracting #5: cost 5 inf + 11608 1550842923.582 * * [misc]simplify: Extracting #6: cost 0 inf + 11542 1550842923.584 * [exit]simplify: Simplified to (*.p16 (+.p16 (+.p16 (real->posit16 5) (+.p16 d3 d2)) (real->posit16 32)) d1) 1550842923.584 * [misc]simplify: Simplified (2) to (λ (d1 d2 d3) (*.p16 (+.p16 (+.p16 (real->posit16 5) (+.p16 d3 d2)) (real->posit16 32)) d1)) 1550842923.633 * * [misc]progress: iteration 1 / 4 1550842923.633 * * * [misc]progress: picking best candidate 1550842923.682 * * * * [misc]pick: Picked #posit16 5)) d1)) (*.p16 d1 (real->posit16 32))))> 1550842923.682 * * * [misc]progress: localizing error 1550842923.959 * * * [misc]progress: generating rewritten candidates 1550842923.959 * * * * [misc]progress: [ 1 / 3 ] rewriting at (2 1) 1550842923.963 * * * * [misc]progress: [ 2 / 3 ] rewriting at (2 1 2) 1550842923.964 * * * * [misc]progress: [ 3 / 3 ] rewriting at (2) 1550842923.969 * * * [misc]progress: generating series expansions 1550842923.969 * * * * [misc]progress: [ 1 / 3 ] generating series at (2 1) 1550842923.969 * * * * [misc]progress: [ 2 / 3 ] generating series at (2 1 2) 1550842923.969 * * * * [misc]progress: [ 3 / 3 ] generating series at (2) 1550842923.969 * * * [misc]progress: simplifying candidates 1550842923.969 * * * * [misc]progress: [ 1 / 7 ] simplifiying candidate #posit16 5)) d1) (*.p16 d1 d2)) (*.p16 d1 (real->posit16 32))))> 1550842923.969 * * * * [misc]progress: [ 2 / 7 ] simplifiying candidate #posit16 5)))) (*.p16 d1 (real->posit16 32))))> 1550842923.969 * * * * [misc]progress: [ 3 / 7 ] simplifiying candidate #posit16 5)) d1) (*.p16 d1 (real->posit16 32)))))> 1550842923.969 * [enter]simplify: Simplifying (*.p16 d1 d2) 1550842923.969 * * [misc]simplify: iters left: 1 (3 enodes) 1550842923.970 * * [misc]simplify: Extracting #0: cost 1 inf + 0 1550842923.970 * * [misc]simplify: Extracting #1: cost 3 inf + 0 1550842923.970 * * [misc]simplify: Extracting #2: cost 1 inf + 2 1550842923.970 * * [misc]simplify: Extracting #3: cost 0 inf + 324 1550842923.970 * [exit]simplify: Simplified to (*.p16 d2 d1) 1550842923.970 * [misc]simplify: Simplified (2 1) to (λ (d1 d2 d3) (+.p16 (*.p16 d2 d1) (+.p16 (*.p16 (+.p16 d3 (real->posit16 5)) d1) (*.p16 d1 (real->posit16 32))))) 1550842923.970 * * * * [misc]progress: [ 4 / 7 ] simplifiying candidate #posit16 32)) (+.p16 (*.p16 d1 d2) (*.p16 (+.p16 d3 (real->posit16 5)) d1))))> 1550842923.970 * * * * [misc]progress: [ 5 / 7 ] simplifiying candidate #posit16 5)) d1)) (*.p16 d1 (real->posit16 32))))> 1550842923.970 * [enter]simplify: Simplifying (+.p16 (+.p16 (*.p16 d1 d2) (*.p16 (+.p16 d3 (real->posit16 5)) d1)) (*.p16 d1 (real->posit16 32))) 1550842923.970 * * [misc]simplify: iters left: 5 (13 enodes) 1550842923.974 * * [misc]simplify: iters left: 4 (29 enodes) 1550842923.978 * * [misc]simplify: iters left: 3 (49 enodes) 1550842923.989 * * [misc]simplify: iters left: 2 (122 enodes) 1550842924.019 * * [misc]simplify: iters left: 1 (228 enodes) 1550842924.100 * * [misc]simplify: Extracting #0: cost 1 inf + 0 1550842924.100 * * [misc]simplify: Extracting #1: cost 23 inf + 0 1550842924.101 * * [misc]simplify: Extracting #2: cost 50 inf + 1 1550842924.101 * * [misc]simplify: Extracting #3: cost 49 inf + 325 1550842924.102 * * [misc]simplify: Extracting #4: cost 29 inf + 4935 1550842924.104 * * [misc]simplify: Extracting #5: cost 5 inf + 11608 1550842924.108 * * [misc]simplify: Extracting #6: cost 0 inf + 11542 1550842924.111 * [exit]simplify: Simplified to (*.p16 (+.p16 (+.p16 (real->posit16 5) (+.p16 d3 d2)) (real->posit16 32)) d1) 1550842924.111 * [misc]simplify: Simplified (2) to (λ (d1 d2 d3) (*.p16 (+.p16 (+.p16 (real->posit16 5) (+.p16 d3 d2)) (real->posit16 32)) d1)) 1550842924.111 * * * * [misc]progress: [ 6 / 7 ] simplifiying candidate #posit16 5)) d1)) (*.p16 d1 (real->posit16 32))))> 1550842924.112 * [enter]simplify: Simplifying (+.p16 (+.p16 (*.p16 d1 d2) (*.p16 (+.p16 d3 (real->posit16 5)) d1)) (*.p16 d1 (real->posit16 32))) 1550842924.112 * * [misc]simplify: iters left: 5 (13 enodes) 1550842924.117 * * [misc]simplify: iters left: 4 (29 enodes) 1550842924.126 * * [misc]simplify: iters left: 3 (49 enodes) 1550842924.146 * * [misc]simplify: iters left: 2 (122 enodes) 1550842924.185 * * [misc]simplify: iters left: 1 (228 enodes) 1550842924.280 * * [misc]simplify: Extracting #0: cost 1 inf + 0 1550842924.280 * * [misc]simplify: Extracting #1: cost 23 inf + 0 1550842924.281 * * [misc]simplify: Extracting #2: cost 50 inf + 1 1550842924.281 * * [misc]simplify: Extracting #3: cost 49 inf + 325 1550842924.282 * * [misc]simplify: Extracting #4: cost 29 inf + 4935 1550842924.285 * * [misc]simplify: Extracting #5: cost 5 inf + 11608 1550842924.289 * * [misc]simplify: Extracting #6: cost 0 inf + 11542 1550842924.293 * [exit]simplify: Simplified to (*.p16 (+.p16 (+.p16 (real->posit16 5) (+.p16 d3 d2)) (real->posit16 32)) d1) 1550842924.293 * [misc]simplify: Simplified (2) to (λ (d1 d2 d3) (*.p16 (+.p16 (+.p16 (real->posit16 5) (+.p16 d3 d2)) (real->posit16 32)) d1)) 1550842924.293 * * * * [misc]progress: [ 7 / 7 ] simplifiying candidate #posit16 5)) d1)) (*.p16 d1 (real->posit16 32))))> 1550842924.294 * [enter]simplify: Simplifying (+.p16 (+.p16 (*.p16 d1 d2) (*.p16 (+.p16 d3 (real->posit16 5)) d1)) (*.p16 d1 (real->posit16 32))) 1550842924.294 * * [misc]simplify: iters left: 5 (13 enodes) 1550842924.299 * * [misc]simplify: iters left: 4 (29 enodes) 1550842924.309 * * [misc]simplify: iters left: 3 (49 enodes) 1550842924.330 * * [misc]simplify: iters left: 2 (122 enodes) 1550842924.358 * * [misc]simplify: iters left: 1 (228 enodes) 1550842924.449 * * [misc]simplify: Extracting #0: cost 1 inf + 0 1550842924.449 * * [misc]simplify: Extracting #1: cost 23 inf + 0 1550842924.450 * * [misc]simplify: Extracting #2: cost 50 inf + 1 1550842924.450 * * [misc]simplify: Extracting #3: cost 49 inf + 325 1550842924.451 * * [misc]simplify: Extracting #4: cost 29 inf + 4935 1550842924.454 * * [misc]simplify: Extracting #5: cost 5 inf + 11608 1550842924.458 * * [misc]simplify: Extracting #6: cost 0 inf + 11542 1550842924.462 * [exit]simplify: Simplified to (*.p16 (+.p16 (+.p16 (real->posit16 5) (+.p16 d3 d2)) (real->posit16 32)) d1) 1550842924.462 * [misc]simplify: Simplified (2) to (λ (d1 d2 d3) (*.p16 (+.p16 (+.p16 (real->posit16 5) (+.p16 d3 d2)) (real->posit16 32)) d1)) 1550842924.462 * * * [misc]progress: adding candidates to table 1550842924.862 * * [misc]progress: iteration 2 / 4 1550842924.862 * * * [misc]progress: picking best candidate 1550842924.940 * * * * [misc]pick: Picked #posit16 5) (+.p16 d3 d2)) (real->posit16 32)) d1))> 1550842924.940 * * * [misc]progress: localizing error 1550842925.113 * * * [misc]progress: generating rewritten candidates 1550842925.113 * * * * [misc]progress: [ 1 / 3 ] rewriting at (2) 1550842925.124 * * * * [misc]progress: [ 2 / 3 ] rewriting at (2 1 1) 1550842925.128 * * * * [misc]progress: [ 3 / 3 ] rewriting at (2 1) 1550842925.145 * * * [misc]progress: generating series expansions 1550842925.146 * * * * [misc]progress: [ 1 / 3 ] generating series at (2) 1550842925.146 * * * * [misc]progress: [ 2 / 3 ] generating series at (2 1 1) 1550842925.146 * * * * [misc]progress: [ 3 / 3 ] generating series at (2 1) 1550842925.146 * * * [misc]progress: simplifying candidates 1550842925.146 * * * * [misc]progress: [ 1 / 8 ] simplifiying candidate #posit16 5) (+.p16 d3 d2)) (real->posit16 32))))> 1550842925.146 * * * * [misc]progress: [ 2 / 8 ] simplifiying candidate #posit16 5) d3) d2) (real->posit16 32)) d1))> 1550842925.146 * * * * [misc]progress: [ 3 / 8 ] simplifiying candidate #posit16 5)) (real->posit16 32)) d1))> 1550842925.146 * * * * [misc]progress: [ 4 / 8 ] simplifiying candidate #posit16 5) (+.p16 (+.p16 d3 d2) (real->posit16 32))) d1))> 1550842925.146 * [enter]simplify: Simplifying (real->posit16 5) 1550842925.146 * * [misc]simplify: iters left: 1 (2 enodes) 1550842925.148 * * [misc]simplify: Extracting #0: cost 1 inf + 0 1550842925.148 * * [misc]simplify: Extracting #1: cost 2 inf + 0 1550842925.148 * * [misc]simplify: Extracting #2: cost 1 inf + 1 1550842925.148 * * [misc]simplify: Extracting #3: cost 0 inf + 2 1550842925.148 * [exit]simplify: Simplified to (real->posit16 5) 1550842925.148 * [misc]simplify: Simplified (2 1 1) to (λ (d1 d2 d3) (*.p16 (+.p16 (real->posit16 5) (+.p16 (+.p16 d3 d2) (real->posit16 32))) d1)) 1550842925.148 * * * * [misc]progress: [ 5 / 8 ] simplifiying candidate #posit16 32) (+.p16 (real->posit16 5) (+.p16 d3 d2))) d1))> 1550842925.148 * * * * [misc]progress: [ 6 / 8 ] simplifiying candidate #posit16 5) (+.p16 d3 d2)) (real->posit16 32)) d1))> 1550842925.148 * [enter]simplify: Simplifying (*.p16 (+.p16 (+.p16 (real->posit16 5) (+.p16 d3 d2)) (real->posit16 32)) d1) 1550842925.148 * * [misc]simplify: iters left: 4 (11 enodes) 1550842925.154 * * [misc]simplify: iters left: 3 (27 enodes) 1550842925.163 * * [misc]simplify: iters left: 2 (60 enodes) 1550842925.185 * * [misc]simplify: iters left: 1 (128 enodes) 1550842925.252 * * [misc]simplify: Extracting #0: cost 1 inf + 0 1550842925.252 * * [misc]simplify: Extracting #1: cost 23 inf + 0 1550842925.252 * * [misc]simplify: Extracting #2: cost 52 inf + 1 1550842925.253 * * [misc]simplify: Extracting #3: cost 48 inf + 1052 1550842925.253 * * [misc]simplify: Extracting #4: cost 43 inf + 1098 1550842925.255 * * [misc]simplify: Extracting #5: cost 8 inf + 10482 1550842925.259 * * [misc]simplify: Extracting #6: cost 0 inf + 13753 1550842925.263 * [exit]simplify: Simplified to (*.p16 (+.p16 d3 (+.p16 (+.p16 d2 (real->posit16 5)) (real->posit16 32))) d1) 1550842925.263 * [misc]simplify: Simplified (2) to (λ (d1 d2 d3) (*.p16 (+.p16 d3 (+.p16 (+.p16 d2 (real->posit16 5)) (real->posit16 32))) d1)) 1550842925.263 * * * * [misc]progress: [ 7 / 8 ] simplifiying candidate #posit16 5) (+.p16 d3 d2)) (real->posit16 32)) d1))> 1550842925.263 * [enter]simplify: Simplifying (*.p16 (+.p16 (+.p16 (real->posit16 5) (+.p16 d3 d2)) (real->posit16 32)) d1) 1550842925.264 * * [misc]simplify: iters left: 4 (11 enodes) 1550842925.269 * * [misc]simplify: iters left: 3 (27 enodes) 1550842925.278 * * [misc]simplify: iters left: 2 (60 enodes) 1550842925.292 * * [misc]simplify: iters left: 1 (128 enodes) 1550842925.326 * * [misc]simplify: Extracting #0: cost 1 inf + 0 1550842925.326 * * [misc]simplify: Extracting #1: cost 23 inf + 0 1550842925.327 * * [misc]simplify: Extracting #2: cost 52 inf + 1 1550842925.327 * * [misc]simplify: Extracting #3: cost 48 inf + 1052 1550842925.327 * * [misc]simplify: Extracting #4: cost 43 inf + 1098 1550842925.328 * * [misc]simplify: Extracting #5: cost 8 inf + 10482 1550842925.330 * * [misc]simplify: Extracting #6: cost 0 inf + 13753 1550842925.332 * [exit]simplify: Simplified to (*.p16 (+.p16 d3 (+.p16 (+.p16 d2 (real->posit16 5)) (real->posit16 32))) d1) 1550842925.332 * [misc]simplify: Simplified (2) to (λ (d1 d2 d3) (*.p16 (+.p16 d3 (+.p16 (+.p16 d2 (real->posit16 5)) (real->posit16 32))) d1)) 1550842925.332 * * * * [misc]progress: [ 8 / 8 ] simplifiying candidate #posit16 5) (+.p16 d3 d2)) (real->posit16 32)) d1))> 1550842925.332 * [enter]simplify: Simplifying (*.p16 (+.p16 (+.p16 (real->posit16 5) (+.p16 d3 d2)) (real->posit16 32)) d1) 1550842925.332 * * [misc]simplify: iters left: 4 (11 enodes) 1550842925.335 * * [misc]simplify: iters left: 3 (27 enodes) 1550842925.341 * * [misc]simplify: iters left: 2 (60 enodes) 1550842925.353 * * [misc]simplify: iters left: 1 (128 enodes) 1550842925.387 * * [misc]simplify: Extracting #0: cost 1 inf + 0 1550842925.387 * * [misc]simplify: Extracting #1: cost 23 inf + 0 1550842925.387 * * [misc]simplify: Extracting #2: cost 52 inf + 1 1550842925.387 * * [misc]simplify: Extracting #3: cost 48 inf + 1052 1550842925.388 * * [misc]simplify: Extracting #4: cost 43 inf + 1098 1550842925.389 * * [misc]simplify: Extracting #5: cost 8 inf + 10482 1550842925.391 * * [misc]simplify: Extracting #6: cost 0 inf + 13753 1550842925.392 * [exit]simplify: Simplified to (*.p16 (+.p16 d3 (+.p16 (+.p16 d2 (real->posit16 5)) (real->posit16 32))) d1) 1550842925.392 * [misc]simplify: Simplified (2) to (λ (d1 d2 d3) (*.p16 (+.p16 d3 (+.p16 (+.p16 d2 (real->posit16 5)) (real->posit16 32))) d1)) 1550842925.392 * * * [misc]progress: adding candidates to table 1550842925.808 * * [misc]progress: iteration 3 / 4 1550842925.808 * * * [misc]progress: picking best candidate 1550842925.911 * * * * [misc]pick: Picked #posit16 5) d3) d2) (real->posit16 32)) d1))> 1550842925.911 * * * [misc]progress: localizing error 1550842926.129 * * * [misc]progress: generating rewritten candidates 1550842926.129 * * * * [misc]progress: [ 1 / 3 ] rewriting at (2) 1550842926.189 * * * * [misc]progress: [ 2 / 3 ] rewriting at (2 1 1) 1550842926.202 * * * * [misc]progress: [ 3 / 3 ] rewriting at (2 1) 1550842926.259 * * * [misc]progress: generating series expansions 1550842926.259 * * * * [misc]progress: [ 1 / 3 ] generating series at (2) 1550842926.259 * * * * [misc]progress: [ 2 / 3 ] generating series at (2 1 1) 1550842926.259 * * * * [misc]progress: [ 3 / 3 ] generating series at (2 1) 1550842926.259 * * * [misc]progress: simplifying candidates 1550842926.259 * * * * [misc]progress: [ 1 / 8 ] simplifiying candidate #posit16 5) d3) d2) (real->posit16 32))))> 1550842926.259 * * * * [misc]progress: [ 2 / 8 ] simplifiying candidate #posit16 5) (+.p16 d3 d2)) (real->posit16 32)) d1))> 1550842926.259 * [enter]simplify: Simplifying (real->posit16 5) 1550842926.260 * * [misc]simplify: iters left: 1 (2 enodes) 1550842926.261 * * [misc]simplify: Extracting #0: cost 1 inf + 0 1550842926.261 * * [misc]simplify: Extracting #1: cost 2 inf + 0 1550842926.261 * * [misc]simplify: Extracting #2: cost 1 inf + 1 1550842926.261 * * [misc]simplify: Extracting #3: cost 0 inf + 2 1550842926.261 * [exit]simplify: Simplified to (real->posit16 5) 1550842926.262 * [misc]simplify: Simplified (2 1 1 1) to (λ (d1 d2 d3) (*.p16 (+.p16 (+.p16 (real->posit16 5) (+.p16 d3 d2)) (real->posit16 32)) d1)) 1550842926.262 * * * * [misc]progress: [ 3 / 8 ] simplifiying candidate #posit16 5) d3)) (real->posit16 32)) d1))> 1550842926.262 * * * * [misc]progress: [ 4 / 8 ] simplifiying candidate #posit16 5) d3) (+.p16 d2 (real->posit16 32))) d1))> 1550842926.262 * [enter]simplify: Simplifying (+.p16 (real->posit16 5) d3) 1550842926.262 * * [misc]simplify: iters left: 2 (4 enodes) 1550842926.264 * * [misc]simplify: iters left: 1 (8 enodes) 1550842926.267 * * [misc]simplify: Extracting #0: cost 1 inf + 0 1550842926.267 * * [misc]simplify: Extracting #1: cost 3 inf + 0 1550842926.267 * * [misc]simplify: Extracting #2: cost 3 inf + 1 1550842926.267 * * [misc]simplify: Extracting #3: cost 2 inf + 2 1550842926.267 * * [misc]simplify: Extracting #4: cost 0 inf + 45 1550842926.267 * [exit]simplify: Simplified to (+.p16 (real->posit16 5) d3) 1550842926.267 * [misc]simplify: Simplified (2 1 1) to (λ (d1 d2 d3) (*.p16 (+.p16 (+.p16 (real->posit16 5) d3) (+.p16 d2 (real->posit16 32))) d1)) 1550842926.268 * * * * [misc]progress: [ 5 / 8 ] simplifiying candidate #posit16 32) (+.p16 (+.p16 (real->posit16 5) d3) d2)) d1))> 1550842926.268 * * * * [misc]progress: [ 6 / 8 ] simplifiying candidate #posit16 5) d3) d2) (real->posit16 32)) d1))> 1550842926.268 * * * * [misc]progress: [ 7 / 8 ] simplifiying candidate #posit16 5) d3) d2) (real->posit16 32)) d1))> 1550842926.268 * * * * [misc]progress: [ 8 / 8 ] simplifiying candidate #posit16 5) d3) d2) (real->posit16 32)) d1))> 1550842926.268 * * * [misc]progress: adding candidates to table 1550842926.808 * * [misc]progress: iteration 4 / 4 1550842926.808 * * * [misc]progress: picking best candidate 1550842926.909 * * * * [misc]pick: Picked #posit16 5) (+.p16 (+.p16 d3 d2) (real->posit16 32))) d1))> 1550842926.909 * * * [misc]progress: localizing error 1550842927.034 * * * [misc]progress: generating rewritten candidates 1550842927.034 * * * * [misc]progress: [ 1 / 3 ] rewriting at (2) 1550842927.042 * * * * [misc]progress: [ 2 / 3 ] rewriting at (2 1 2) 1550842927.048 * * * * [misc]progress: [ 3 / 3 ] rewriting at (2 1) 1550842927.057 * * * [misc]progress: generating series expansions 1550842927.057 * * * * [misc]progress: [ 1 / 3 ] generating series at (2) 1550842927.057 * * * * [misc]progress: [ 2 / 3 ] generating series at (2 1 2) 1550842927.057 * * * * [misc]progress: [ 3 / 3 ] generating series at (2 1) 1550842927.057 * * * [misc]progress: simplifying candidates 1550842927.057 * * * * [misc]progress: [ 1 / 8 ] simplifiying candidate #posit16 5) (+.p16 (+.p16 d3 d2) (real->posit16 32)))))> 1550842927.057 * * * * [misc]progress: [ 2 / 8 ] simplifiying candidate #posit16 5) (+.p16 d3 (+.p16 d2 (real->posit16 32)))) d1))> 1550842927.057 * * * * [misc]progress: [ 3 / 8 ] simplifiying candidate #posit16 5) (+.p16 (real->posit16 32) (+.p16 d3 d2))) d1))> 1550842927.058 * * * * [misc]progress: [ 4 / 8 ] simplifiying candidate #posit16 5) (+.p16 d3 d2)) (real->posit16 32)) d1))> 1550842927.058 * [enter]simplify: Simplifying (real->posit16 32) 1550842927.058 * * [misc]simplify: iters left: 1 (2 enodes) 1550842927.059 * * [misc]simplify: Extracting #0: cost 1 inf + 0 1550842927.059 * * [misc]simplify: Extracting #1: cost 2 inf + 0 1550842927.059 * * [misc]simplify: Extracting #2: cost 1 inf + 1 1550842927.060 * * [misc]simplify: Extracting #3: cost 0 inf + 2 1550842927.060 * [exit]simplify: Simplified to (real->posit16 32) 1550842927.060 * [misc]simplify: Simplified (2 1 2) to (λ (d1 d2 d3) (*.p16 (+.p16 (+.p16 (real->posit16 5) (+.p16 d3 d2)) (real->posit16 32)) d1)) 1550842927.060 * * * * [misc]progress: [ 5 / 8 ] simplifiying candidate #posit16 32)) (real->posit16 5)) d1))> 1550842927.060 * * * * [misc]progress: [ 6 / 8 ] simplifiying candidate #posit16 5) (+.p16 (+.p16 d3 d2) (real->posit16 32))) d1))> 1550842927.060 * [enter]simplify: Simplifying (real->posit16 5) 1550842927.060 * * [misc]simplify: iters left: 1 (2 enodes) 1550842927.061 * * [misc]simplify: Extracting #0: cost 1 inf + 0 1550842927.061 * * [misc]simplify: Extracting #1: cost 2 inf + 0 1550842927.061 * * [misc]simplify: Extracting #2: cost 1 inf + 1 1550842927.061 * * [misc]simplify: Extracting #3: cost 0 inf + 2 1550842927.062 * [exit]simplify: Simplified to (real->posit16 5) 1550842927.062 * [misc]simplify: Simplified (2 1 1) to (λ (d1 d2 d3) (*.p16 (+.p16 (real->posit16 5) (+.p16 (+.p16 d3 d2) (real->posit16 32))) d1)) 1550842927.062 * * * * [misc]progress: [ 7 / 8 ] simplifiying candidate #posit16 5) (+.p16 (+.p16 d3 d2) (real->posit16 32))) d1))> 1550842927.062 * [enter]simplify: Simplifying (real->posit16 5) 1550842927.062 * * [misc]simplify: iters left: 1 (2 enodes) 1550842927.063 * * [misc]simplify: Extracting #0: cost 1 inf + 0 1550842927.063 * * [misc]simplify: Extracting #1: cost 2 inf + 0 1550842927.063 * * [misc]simplify: Extracting #2: cost 1 inf + 1 1550842927.063 * * [misc]simplify: Extracting #3: cost 0 inf + 2 1550842927.063 * [exit]simplify: Simplified to (real->posit16 5) 1550842927.063 * [misc]simplify: Simplified (2 1 1) to (λ (d1 d2 d3) (*.p16 (+.p16 (real->posit16 5) (+.p16 (+.p16 d3 d2) (real->posit16 32))) d1)) 1550842927.063 * * * * [misc]progress: [ 8 / 8 ] simplifiying candidate #posit16 5) (+.p16 (+.p16 d3 d2) (real->posit16 32))) d1))> 1550842927.064 * [enter]simplify: Simplifying (real->posit16 5) 1550842927.064 * * [misc]simplify: iters left: 1 (2 enodes) 1550842927.065 * * [misc]simplify: Extracting #0: cost 1 inf + 0 1550842927.065 * * [misc]simplify: Extracting #1: cost 2 inf + 0 1550842927.065 * * [misc]simplify: Extracting #2: cost 1 inf + 1 1550842927.065 * * [misc]simplify: Extracting #3: cost 0 inf + 2 1550842927.065 * [exit]simplify: Simplified to (real->posit16 5) 1550842927.065 * [misc]simplify: Simplified (2 1 1) to (λ (d1 d2 d3) (*.p16 (+.p16 (real->posit16 5) (+.p16 (+.p16 d3 d2) (real->posit16 32))) d1)) 1550842927.065 * * * [misc]progress: adding candidates to table 1550842927.535 * [misc]progress: [Phase 3 of 3] Extracting. 1550842927.535 * * [misc]regime: Finding splitpoints for: (#posit16 5) (+.p16 (+.p16 d3 d2) (real->posit16 32))) d1))> #posit16 5)) d1)) (*.p16 d1 (real->posit16 32))))> #posit16 5) d3) (+.p16 d2 (real->posit16 32))) d1))> #posit16 5)) d1) (*.p16 d1 (real->posit16 32)))))>) 1550842927.536 * * * [misc]regime-changes: Trying 3 branch expressions: (d3 d2 d1) 1550842927.536 * * * * [misc]regimes: Trying to branch on d3 from (#posit16 5) (+.p16 (+.p16 d3 d2) (real->posit16 32))) d1))> #posit16 5)) d1)) (*.p16 d1 (real->posit16 32))))> #posit16 5) d3) (+.p16 d2 (real->posit16 32))) d1))> #posit16 5)) d1) (*.p16 d1 (real->posit16 32)))))>) 1550842927.902 * * * * [misc]regimes: Trying to branch on d2 from (#posit16 5) (+.p16 (+.p16 d3 d2) (real->posit16 32))) d1))> #posit16 5)) d1)) (*.p16 d1 (real->posit16 32))))> #posit16 5) d3) (+.p16 d2 (real->posit16 32))) d1))> #posit16 5)) d1) (*.p16 d1 (real->posit16 32)))))>) 1550842928.240 * * * * [misc]regimes: Trying to branch on d1 from (#posit16 5) (+.p16 (+.p16 d3 d2) (real->posit16 32))) d1))> #posit16 5)) d1)) (*.p16 d1 (real->posit16 32))))> #posit16 5) d3) (+.p16 d2 (real->posit16 32))) d1))> #posit16 5)) d1) (*.p16 d1 (real->posit16 32)))))>) 1550842928.543 * * * [misc]regime: Found split indices: #