223.133 * [progress]: [Phase 1 of 3] Setting up. 0.001 * * * [progress]: [1/2] Preparing points 0.015 * * * [progress]: [2/2] Setting up program. 0.017 * [progress]: [Phase 2 of 3] Improving. 0.017 * [simplify]: Simplifying using # : (+ (* x (* x x)) (* x x)) 0.017 * * [simplify]: iteration 0 : 4 enodes (cost 9 ) 0.018 * * [simplify]: iteration 1 : 13 enodes (cost 7 ) 0.020 * * [simplify]: iteration 2 : 26 enodes (cost 7 ) 0.024 * * [simplify]: iteration 3 : 39 enodes (cost 7 ) 0.029 * * [simplify]: iteration 4 : 57 enodes (cost 7 ) 0.047 * * [simplify]: iteration 5 : 112 enodes (cost 7 ) 0.068 * * [simplify]: iteration 6 : 206 enodes (cost 7 ) 0.190 * * [simplify]: iteration 7 : 584 enodes (cost 7 ) 1.370 * * [simplify]: iteration 8 : 1892 enodes (cost 7 ) 4.047 * * [simplify]: iteration done : 5000 enodes (cost 7 ) 4.047 * [simplify]: Simplified to: (+ (pow x 3) (* x x)) 4.051 * * [progress]: iteration 1 / 4 4.051 * * * [progress]: picking best candidate 4.053 * * * * [pick]: Picked # 4.053 * * * [progress]: localizing error 4.057 * * * [progress]: generating rewritten candidates 4.057 * * * * [progress]: [ 1 / 1 ] rewriting at (2) 4.065 * * * [progress]: generating series expansions 4.065 * * * * [progress]: [ 1 / 1 ] generating series at (2) 4.065 * [approximate]: Taking taylor expansion of (+ (pow x 2) (pow x 3)) in (x) around 0 4.065 * [taylor]: Taking taylor expansion of (+ (pow x 2) (pow x 3)) in x 4.065 * [taylor]: Taking taylor expansion of (pow x 2) in x 4.065 * [taylor]: Taking taylor expansion of x in x 4.065 * [taylor]: Taking taylor expansion of (pow x 3) in x 4.065 * [taylor]: Taking taylor expansion of x in x 4.065 * [taylor]: Taking taylor expansion of (+ (pow x 2) (pow x 3)) in x 4.065 * [taylor]: Taking taylor expansion of (pow x 2) in x 4.065 * [taylor]: Taking taylor expansion of x in x 4.065 * [taylor]: Taking taylor expansion of (pow x 3) in x 4.065 * [taylor]: Taking taylor expansion of x in x 4.066 * [approximate]: Taking taylor expansion of (+ (/ 1 (pow x 2)) (/ 1 (pow x 3))) in (x) around 0 4.066 * [taylor]: Taking taylor expansion of (+ (/ 1 (pow x 2)) (/ 1 (pow x 3))) in x 4.066 * [taylor]: Taking taylor expansion of (/ 1 (pow x 2)) in x 4.066 * [taylor]: Taking taylor expansion of (pow x 2) in x 4.066 * [taylor]: Taking taylor expansion of x in x 4.067 * [taylor]: Taking taylor expansion of (/ 1 (pow x 3)) in x 4.067 * [taylor]: Taking taylor expansion of (pow x 3) in x 4.067 * [taylor]: Taking taylor expansion of x in x 4.067 * [taylor]: Taking taylor expansion of (+ (/ 1 (pow x 2)) (/ 1 (pow x 3))) in x 4.067 * [taylor]: Taking taylor expansion of (/ 1 (pow x 2)) in x 4.067 * [taylor]: Taking taylor expansion of (pow x 2) in x 4.067 * [taylor]: Taking taylor expansion of x in x 4.067 * [taylor]: Taking taylor expansion of (/ 1 (pow x 3)) in x 4.067 * [taylor]: Taking taylor expansion of (pow x 3) in x 4.067 * [taylor]: Taking taylor expansion of x in x 4.069 * [approximate]: Taking taylor expansion of (- (/ 1 (pow x 2)) (/ 1 (pow x 3))) in (x) around 0 4.069 * [taylor]: Taking taylor expansion of (- (/ 1 (pow x 2)) (/ 1 (pow x 3))) in x 4.069 * [taylor]: Taking taylor expansion of (/ 1 (pow x 2)) in x 4.069 * [taylor]: Taking taylor expansion of (pow x 2) in x 4.069 * [taylor]: Taking taylor expansion of x in x 4.069 * [taylor]: Taking taylor expansion of (/ 1 (pow x 3)) in x 4.069 * [taylor]: Taking taylor expansion of (pow x 3) in x 4.069 * [taylor]: Taking taylor expansion of x in x 4.069 * [taylor]: Taking taylor expansion of (- (/ 1 (pow x 2)) (/ 1 (pow x 3))) in x 4.069 * [taylor]: Taking taylor expansion of (/ 1 (pow x 2)) in x 4.069 * [taylor]: Taking taylor expansion of (pow x 2) in x 4.069 * [taylor]: Taking taylor expansion of x in x 4.069 * [taylor]: Taking taylor expansion of (/ 1 (pow x 3)) in x 4.069 * [taylor]: Taking taylor expansion of (pow x 3) in x 4.069 * [taylor]: Taking taylor expansion of x in x 4.072 * * * [progress]: simplifying candidates 4.072 * [simplify]: Simplifying using # : (* (exp (pow x 3)) (exp (* x x))) (log (+ (pow x 3) (* x x))) (exp (+ (pow x 3) (* x x))) (* (cbrt (+ (pow x 3) (* x x))) (cbrt (+ (pow x 3) (* x x)))) (cbrt (+ (pow x 3) (* x x))) (* (* (+ (pow x 3) (* x x)) (+ (pow x 3) (* x x))) (+ (pow x 3) (* x x))) (sqrt (+ (pow x 3) (* x x))) (sqrt (+ (pow x 3) (* x x))) (+ (pow (pow x 3) 3) (pow (* x x) 3)) (+ (* (pow x 3) (pow x 3)) (- (* (* x x) (* x x)) (* (pow x 3) (* x x)))) (- (* (pow x 3) (pow x 3)) (* (* x x) (* x x))) (- (pow x 3) (* x x)) (+ (* x x) x) (+ (* x x) x) (+ x 1) (+ (pow x 2) (pow x 3)) (+ (pow x 2) (pow x 3)) (+ (pow x 2) (pow x 3)) 4.073 * * [simplify]: iteration 0 : 7 enodes (cost 9 ) 4.074 * * [simplify]: iteration 1 : 19 enodes (cost 8 ) 4.076 * * [simplify]: iteration 2 : 38 enodes (cost 8 ) 4.081 * * [simplify]: iteration 3 : 79 enodes (cost 8 ) 4.094 * * [simplify]: iteration 4 : 215 enodes (cost 8 ) 4.164 * * [simplify]: iteration 5 : 651 enodes (cost 8 ) 4.808 * * [simplify]: iteration 6 : 2689 enodes (cost 8 ) 5.937 * * [simplify]: iteration done : 5000 enodes (cost 8 ) 5.938 * * [simplify]: iteration 0 : 6 enodes (cost 8 ) 5.939 * * [simplify]: iteration 1 : 14 enodes (cost 8 ) 5.946 * * [simplify]: iteration 2 : 27 enodes (cost 8 ) 5.950 * * [simplify]: iteration 3 : 51 enodes (cost 8 ) 5.956 * * [simplify]: iteration 4 : 85 enodes (cost 8 ) 5.970 * * [simplify]: iteration 5 : 155 enodes (cost 8 ) 6.029 * * [simplify]: iteration 6 : 404 enodes (cost 8 ) 6.529 * * [simplify]: iteration 7 : 1446 enodes (cost 8 ) 8.480 * * [simplify]: iteration done : 5000 enodes (cost 8 ) 8.481 * * [simplify]: iteration 0 : 6 enodes (cost 8 ) 8.482 * * [simplify]: iteration 1 : 17 enodes (cost 8 ) 8.484 * * [simplify]: iteration 2 : 37 enodes (cost 8 ) 8.489 * * [simplify]: iteration 3 : 72 enodes (cost 8 ) 8.505 * * [simplify]: iteration 4 : 173 enodes (cost 8 ) 8.546 * * [simplify]: iteration 5 : 479 enodes (cost 8 ) 8.851 * * [simplify]: iteration 6 : 1670 enodes (cost 8 ) 9.843 * * [simplify]: iteration done : 5001 enodes (cost 8 ) 9.844 * * [simplify]: iteration 0 : 7 enodes (cost 17 ) 9.845 * * [simplify]: iteration 1 : 15 enodes (cost 17 ) 9.847 * * [simplify]: iteration 2 : 28 enodes (cost 17 ) 9.850 * * [simplify]: iteration 3 : 46 enodes (cost 17 ) 9.855 * * [simplify]: iteration 4 : 76 enodes (cost 17 ) 9.869 * * [simplify]: iteration 5 : 148 enodes (cost 17 ) 9.929 * * [simplify]: iteration 6 : 398 enodes (cost 17 ) 10.404 * * [simplify]: iteration 7 : 1405 enodes (cost 17 ) 12.371 * * [simplify]: iteration done : 5000 enodes (cost 17 ) 12.372 * * [simplify]: iteration 0 : 6 enodes (cost 8 ) 12.373 * * [simplify]: iteration 1 : 14 enodes (cost 8 ) 12.375 * * [simplify]: iteration 2 : 27 enodes (cost 8 ) 12.379 * * [simplify]: iteration 3 : 45 enodes (cost 8 ) 12.384 * * [simplify]: iteration 4 : 75 enodes (cost 8 ) 12.397 * * [simplify]: iteration 5 : 145 enodes (cost 8 ) 12.459 * * [simplify]: iteration 6 : 388 enodes (cost 8 ) 12.963 * * [simplify]: iteration 7 : 1409 enodes (cost 8 ) 15.064 * * [simplify]: iteration done : 5000 enodes (cost 8 ) 15.065 * * [simplify]: iteration 0 : 7 enodes (cost 23 ) 15.066 * * [simplify]: iteration 1 : 28 enodes (cost 23 ) 15.076 * * [simplify]: iteration 2 : 100 enodes (cost 9 ) 15.113 * * [simplify]: iteration 3 : 354 enodes (cost 9 ) 15.493 * * [simplify]: iteration 4 : 1586 enodes (cost 9 ) 17.284 * * [simplify]: iteration done : 5000 enodes (cost 9 ) 17.285 * * [simplify]: iteration 0 : 6 enodes (cost 8 ) 17.285 * * [simplify]: iteration 1 : 14 enodes (cost 8 ) 17.287 * * [simplify]: iteration 2 : 27 enodes (cost 8 ) 17.291 * * [simplify]: iteration 3 : 45 enodes (cost 8 ) 17.296 * * [simplify]: iteration 4 : 75 enodes (cost 8 ) 17.313 * * [simplify]: iteration 5 : 145 enodes (cost 8 ) 17.372 * * [simplify]: iteration 6 : 388 enodes (cost 8 ) 17.881 * * [simplify]: iteration 7 : 1409 enodes (cost 8 ) 20.014 * * [simplify]: iteration done : 5000 enodes (cost 8 ) 20.014 * * [simplify]: iteration 0 : 6 enodes (cost 8 ) 20.015 * * [simplify]: iteration 1 : 14 enodes (cost 8 ) 20.017 * * [simplify]: iteration 2 : 27 enodes (cost 8 ) 20.021 * * [simplify]: iteration 3 : 45 enodes (cost 8 ) 20.026 * * [simplify]: iteration 4 : 75 enodes (cost 8 ) 20.039 * * [simplify]: iteration 5 : 145 enodes (cost 8 ) 20.096 * * [simplify]: iteration 6 : 388 enodes (cost 8 ) 20.599 * * [simplify]: iteration 7 : 1409 enodes (cost 8 ) 22.731 * * [simplify]: iteration done : 5000 enodes (cost 8 ) 22.732 * * [simplify]: iteration 0 : 7 enodes (cost 11 ) 22.733 * * [simplify]: iteration 1 : 25 enodes (cost 11 ) 22.739 * * [simplify]: iteration 2 : 88 enodes (cost 9 ) 22.777 * * [simplify]: iteration 3 : 292 enodes (cost 9 ) 23.047 * * [simplify]: iteration 4 : 1151 enodes (cost 9 ) 25.388 * * [simplify]: iteration done : 5001 enodes (cost 9 ) 25.388 * * [simplify]: iteration 0 : 9 enodes (cost 23 ) 25.390 * * [simplify]: iteration 1 : 31 enodes (cost 15 ) 25.399 * * [simplify]: iteration 2 : 94 enodes (cost 13 ) 25.426 * * [simplify]: iteration 3 : 314 enodes (cost 11 ) 25.638 * * [simplify]: iteration 4 : 1086 enodes (cost 11 ) 27.377 * * [simplify]: iteration 5 : 4725 enodes (cost 11 ) 29.083 * * [simplify]: iteration done : 5000 enodes (cost 11 ) 29.084 * * [simplify]: iteration 0 : 7 enodes (cost 15 ) 29.085 * * [simplify]: iteration 1 : 24 enodes (cost 9 ) 29.089 * * [simplify]: iteration 2 : 73 enodes (cost 7 ) 29.112 * * [simplify]: iteration 3 : 210 enodes (cost 7 ) 29.213 * * [simplify]: iteration 4 : 687 enodes (cost 7 ) 29.951 * * [simplify]: iteration 5 : 2869 enodes (cost 7 ) 31.628 * * [simplify]: iteration done : 5000 enodes (cost 7 ) 31.629 * * [simplify]: iteration 0 : 5 enodes (cost 7 ) 31.630 * * [simplify]: iteration 1 : 14 enodes (cost 7 ) 31.632 * * [simplify]: iteration 2 : 29 enodes (cost 7 ) 31.635 * * [simplify]: iteration 3 : 46 enodes (cost 7 ) 31.642 * * [simplify]: iteration 4 : 85 enodes (cost 7 ) 31.658 * * [simplify]: iteration 5 : 199 enodes (cost 7 ) 31.738 * * [simplify]: iteration 6 : 639 enodes (cost 7 ) 32.524 * * [simplify]: iteration 7 : 2554 enodes (cost 7 ) 34.514 * * [simplify]: iteration done : 5000 enodes (cost 7 ) 34.515 * * [simplify]: iteration 0 : 3 enodes (cost 5 ) 34.516 * * [simplify]: iteration 1 : 7 enodes (cost 5 ) 34.516 * * [simplify]: iteration 2 : 11 enodes (cost 5 ) 34.518 * * [simplify]: iteration 3 : 17 enodes (cost 5 ) 34.520 * * [simplify]: iteration done : 17 enodes (cost 5 ) 34.521 * * [simplify]: iteration 0 : 3 enodes (cost 5 ) 34.521 * * [simplify]: iteration 1 : 7 enodes (cost 5 ) 34.522 * * [simplify]: iteration 2 : 11 enodes (cost 5 ) 34.523 * * [simplify]: iteration 3 : 17 enodes (cost 5 ) 34.525 * * [simplify]: iteration done : 17 enodes (cost 5 ) 34.526 * * [simplify]: iteration 0 : 3 enodes (cost 3 ) 34.526 * * [simplify]: iteration 1 : 6 enodes (cost 3 ) 34.527 * * [simplify]: iteration done : 6 enodes (cost 3 ) 34.527 * * [simplify]: iteration 0 : 6 enodes (cost 7 ) 34.528 * * [simplify]: iteration 1 : 18 enodes (cost 7 ) 34.532 * * [simplify]: iteration 2 : 42 enodes (cost 7 ) 34.535 * * [simplify]: iteration 3 : 61 enodes (cost 7 ) 34.541 * * [simplify]: iteration 4 : 92 enodes (cost 7 ) 34.558 * * [simplify]: iteration 5 : 169 enodes (cost 7 ) 34.612 * * [simplify]: iteration 6 : 397 enodes (cost 7 ) 35.075 * * [simplify]: iteration 7 : 1413 enodes (cost 7 ) 37.413 * * [simplify]: iteration done : 5000 enodes (cost 7 ) 37.413 * * [simplify]: iteration 0 : 6 enodes (cost 7 ) 37.414 * * [simplify]: iteration 1 : 18 enodes (cost 7 ) 37.418 * * [simplify]: iteration 2 : 42 enodes (cost 7 ) 37.421 * * [simplify]: iteration 3 : 61 enodes (cost 7 ) 37.427 * * [simplify]: iteration 4 : 92 enodes (cost 7 ) 37.439 * * [simplify]: iteration 5 : 169 enodes (cost 7 ) 37.492 * * [simplify]: iteration 6 : 397 enodes (cost 7 ) 37.953 * * [simplify]: iteration 7 : 1413 enodes (cost 7 ) 40.085 * * [simplify]: iteration done : 5000 enodes (cost 7 ) 40.086 * * [simplify]: iteration 0 : 6 enodes (cost 7 ) 40.087 * * [simplify]: iteration 1 : 18 enodes (cost 7 ) 40.090 * * [simplify]: iteration 2 : 42 enodes (cost 7 ) 40.093 * * [simplify]: iteration 3 : 61 enodes (cost 7 ) 40.104 * * [simplify]: iteration 4 : 92 enodes (cost 7 ) 40.117 * * [simplify]: iteration 5 : 169 enodes (cost 7 ) 40.170 * * [simplify]: iteration 6 : 397 enodes (cost 7 ) 40.637 * * [simplify]: iteration 7 : 1413 enodes (cost 7 ) 42.778 * * [simplify]: iteration done : 5000 enodes (cost 7 ) 42.778 * [simplify]: Simplified to: (exp (+ (pow x 3) (* x x))) (log (+ (pow x 3) (* x x))) (exp (+ (pow x 3) (* x x))) (* (cbrt (+ (pow x 3) (* x x))) (cbrt (+ (pow x 3) (* x x)))) (cbrt (+ (pow x 3) (* x x))) (pow (+ (pow x 3) (* x x)) 3) (sqrt (+ (pow x 3) (* x x))) (sqrt (+ (pow x 3) (* x x))) (+ (pow (pow x 3) 3) (pow x 6)) (+ (pow x 6) (- (pow x 4) (pow x 5))) (- (pow x 6) (pow x 4)) (- (pow x 3) (* x x)) (+ (* x x) x) (+ (* x x) x) (+ x 1) (+ (pow x 2) (pow x 3)) (+ (pow x 2) (pow x 3)) (+ (pow x 2) (pow x 3)) 42.778 * * * [progress]: adding candidates to table 42.802 * * [progress]: iteration 2 / 4 42.802 * * * [progress]: picking best candidate 42.806 * * * * [pick]: Picked # 42.806 * * * [progress]: localizing error 42.820 * * * [progress]: generating rewritten candidates 42.820 * * * * [progress]: [ 1 / 4 ] rewriting at (2 2) 42.827 * * * * [progress]: [ 2 / 4 ] rewriting at (2 1 2) 42.834 * * * * [progress]: [ 3 / 4 ] rewriting at (2 1 1) 42.843 * * * * [progress]: [ 4 / 4 ] rewriting at (2 1) 42.866 * * * [progress]: generating series expansions 42.866 * * * * [progress]: [ 1 / 4 ] generating series at (2 2) 42.866 * [approximate]: Taking taylor expansion of (pow (+ (pow x 2) (pow x 3)) 1/3) in (x) around 0 42.866 * [taylor]: Taking taylor expansion of (pow (+ (pow x 2) (pow x 3)) 1/3) in x 42.866 * [taylor]: Taking taylor expansion of (exp (* 1/3 (log (+ (pow x 2) (pow x 3))))) in x 42.867 * [taylor]: Taking taylor expansion of (* 1/3 (log (+ (pow x 2) (pow x 3)))) in x 42.867 * [taylor]: Taking taylor expansion of 1/3 in x 42.867 * [taylor]: Taking taylor expansion of (log (+ (pow x 2) (pow x 3))) in x 42.867 * [taylor]: Taking taylor expansion of (+ (pow x 2) (pow x 3)) in x 42.867 * [taylor]: Taking taylor expansion of (pow x 2) in x 42.867 * [taylor]: Taking taylor expansion of x in x 42.867 * [taylor]: Taking taylor expansion of (pow x 3) in x 42.867 * [taylor]: Taking taylor expansion of x in x 42.867 * [taylor]: Taking taylor expansion of (pow (+ (pow x 2) (pow x 3)) 1/3) in x 42.867 * [taylor]: Taking taylor expansion of (exp (* 1/3 (log (+ (pow x 2) (pow x 3))))) in x 42.867 * [taylor]: Taking taylor expansion of (* 1/3 (log (+ (pow x 2) (pow x 3)))) in x 42.867 * [taylor]: Taking taylor expansion of 1/3 in x 42.867 * [taylor]: Taking taylor expansion of (log (+ (pow x 2) (pow x 3))) in x 42.867 * [taylor]: Taking taylor expansion of (+ (pow x 2) (pow x 3)) in x 42.867 * [taylor]: Taking taylor expansion of (pow x 2) in x 42.867 * [taylor]: Taking taylor expansion of x in x 42.867 * [taylor]: Taking taylor expansion of (pow x 3) in x 42.867 * [taylor]: Taking taylor expansion of x in x 42.870 * [approximate]: Taking taylor expansion of (pow (+ (/ 1 (pow x 2)) (/ 1 (pow x 3))) 1/3) in (x) around 0 42.871 * [taylor]: Taking taylor expansion of (pow (+ (/ 1 (pow x 2)) (/ 1 (pow x 3))) 1/3) in x 42.871 * [taylor]: Taking taylor expansion of (exp (* 1/3 (log (+ (/ 1 (pow x 2)) (/ 1 (pow x 3)))))) in x 42.871 * [taylor]: Taking taylor expansion of (* 1/3 (log (+ (/ 1 (pow x 2)) (/ 1 (pow x 3))))) in x 42.871 * [taylor]: Taking taylor expansion of 1/3 in x 42.871 * [taylor]: Taking taylor expansion of (log (+ (/ 1 (pow x 2)) (/ 1 (pow x 3)))) in x 42.871 * [taylor]: Taking taylor expansion of (+ (/ 1 (pow x 2)) (/ 1 (pow x 3))) in x 42.871 * [taylor]: Taking taylor expansion of (/ 1 (pow x 2)) in x 42.871 * [taylor]: Taking taylor expansion of (pow x 2) in x 42.871 * [taylor]: Taking taylor expansion of x in x 42.871 * [taylor]: Taking taylor expansion of (/ 1 (pow x 3)) in x 42.871 * [taylor]: Taking taylor expansion of (pow x 3) in x 42.871 * [taylor]: Taking taylor expansion of x in x 42.871 * [taylor]: Taking taylor expansion of (pow (+ (/ 1 (pow x 2)) (/ 1 (pow x 3))) 1/3) in x 42.871 * [taylor]: Taking taylor expansion of (exp (* 1/3 (log (+ (/ 1 (pow x 2)) (/ 1 (pow x 3)))))) in x 42.871 * [taylor]: Taking taylor expansion of (* 1/3 (log (+ (/ 1 (pow x 2)) (/ 1 (pow x 3))))) in x 42.871 * [taylor]: Taking taylor expansion of 1/3 in x 42.871 * [taylor]: Taking taylor expansion of (log (+ (/ 1 (pow x 2)) (/ 1 (pow x 3)))) in x 42.871 * [taylor]: Taking taylor expansion of (+ (/ 1 (pow x 2)) (/ 1 (pow x 3))) in x 42.871 * [taylor]: Taking taylor expansion of (/ 1 (pow x 2)) in x 42.871 * [taylor]: Taking taylor expansion of (pow x 2) in x 42.871 * [taylor]: Taking taylor expansion of x in x 42.871 * [taylor]: Taking taylor expansion of (/ 1 (pow x 3)) in x 42.871 * [taylor]: Taking taylor expansion of (pow x 3) in x 42.871 * [taylor]: Taking taylor expansion of x in x 42.874 * [approximate]: Taking taylor expansion of (pow (- (/ 1 (pow x 2)) (/ 1 (pow x 3))) 1/3) in (x) around 0 42.874 * [taylor]: Taking taylor expansion of (pow (- (/ 1 (pow x 2)) (/ 1 (pow x 3))) 1/3) in x 42.874 * [taylor]: Taking taylor expansion of (exp (* 1/3 (log (- (/ 1 (pow x 2)) (/ 1 (pow x 3)))))) in x 42.874 * [taylor]: Taking taylor expansion of (* 1/3 (log (- (/ 1 (pow x 2)) (/ 1 (pow x 3))))) in x 42.874 * [taylor]: Taking taylor expansion of 1/3 in x 42.874 * [taylor]: Taking taylor expansion of (log (- (/ 1 (pow x 2)) (/ 1 (pow x 3)))) in x 42.874 * [taylor]: Taking taylor expansion of (- (/ 1 (pow x 2)) (/ 1 (pow x 3))) in x 42.874 * [taylor]: Taking taylor expansion of (/ 1 (pow x 2)) in x 42.874 * [taylor]: Taking taylor expansion of (pow x 2) in x 42.874 * [taylor]: Taking taylor expansion of x in x 42.874 * [taylor]: Taking taylor expansion of (/ 1 (pow x 3)) in x 42.874 * [taylor]: Taking taylor expansion of (pow x 3) in x 42.874 * [taylor]: Taking taylor expansion of x in x 42.874 * [taylor]: Taking taylor expansion of (pow (- (/ 1 (pow x 2)) (/ 1 (pow x 3))) 1/3) in x 42.874 * [taylor]: Taking taylor expansion of (exp (* 1/3 (log (- (/ 1 (pow x 2)) (/ 1 (pow x 3)))))) in x 42.874 * [taylor]: Taking taylor expansion of (* 1/3 (log (- (/ 1 (pow x 2)) (/ 1 (pow x 3))))) in x 42.874 * [taylor]: Taking taylor expansion of 1/3 in x 42.874 * [taylor]: Taking taylor expansion of (log (- (/ 1 (pow x 2)) (/ 1 (pow x 3)))) in x 42.874 * [taylor]: Taking taylor expansion of (- (/ 1 (pow x 2)) (/ 1 (pow x 3))) in x 42.874 * [taylor]: Taking taylor expansion of (/ 1 (pow x 2)) in x 42.874 * [taylor]: Taking taylor expansion of (pow x 2) in x 42.874 * [taylor]: Taking taylor expansion of x in x 42.874 * [taylor]: Taking taylor expansion of (/ 1 (pow x 3)) in x 42.874 * [taylor]: Taking taylor expansion of (pow x 3) in x 42.874 * [taylor]: Taking taylor expansion of x in x 42.876 * * * * [progress]: [ 2 / 4 ] generating series at (2 1 2) 42.877 * [approximate]: Taking taylor expansion of (pow (+ (pow x 2) (pow x 3)) 1/3) in (x) around 0 42.877 * [taylor]: Taking taylor expansion of (pow (+ (pow x 2) (pow x 3)) 1/3) in x 42.877 * [taylor]: Taking taylor expansion of (exp (* 1/3 (log (+ (pow x 2) (pow x 3))))) in x 42.877 * [taylor]: Taking taylor expansion of (* 1/3 (log (+ (pow x 2) (pow x 3)))) in x 42.877 * [taylor]: Taking taylor expansion of 1/3 in x 42.877 * [taylor]: Taking taylor expansion of (log (+ (pow x 2) (pow x 3))) in x 42.877 * [taylor]: Taking taylor expansion of (+ (pow x 2) (pow x 3)) in x 42.877 * [taylor]: Taking taylor expansion of (pow x 2) in x 42.877 * [taylor]: Taking taylor expansion of x in x 42.877 * [taylor]: Taking taylor expansion of (pow x 3) in x 42.877 * [taylor]: Taking taylor expansion of x in x 42.877 * [taylor]: Taking taylor expansion of (pow (+ (pow x 2) (pow x 3)) 1/3) in x 42.877 * [taylor]: Taking taylor expansion of (exp (* 1/3 (log (+ (pow x 2) (pow x 3))))) in x 42.877 * [taylor]: Taking taylor expansion of (* 1/3 (log (+ (pow x 2) (pow x 3)))) in x 42.877 * [taylor]: Taking taylor expansion of 1/3 in x 42.877 * [taylor]: Taking taylor expansion of (log (+ (pow x 2) (pow x 3))) in x 42.877 * [taylor]: Taking taylor expansion of (+ (pow x 2) (pow x 3)) in x 42.877 * [taylor]: Taking taylor expansion of (pow x 2) in x 42.877 * [taylor]: Taking taylor expansion of x in x 42.877 * [taylor]: Taking taylor expansion of (pow x 3) in x 42.877 * [taylor]: Taking taylor expansion of x in x 42.879 * [approximate]: Taking taylor expansion of (pow (+ (/ 1 (pow x 2)) (/ 1 (pow x 3))) 1/3) in (x) around 0 42.879 * [taylor]: Taking taylor expansion of (pow (+ (/ 1 (pow x 2)) (/ 1 (pow x 3))) 1/3) in x 42.879 * [taylor]: Taking taylor expansion of (exp (* 1/3 (log (+ (/ 1 (pow x 2)) (/ 1 (pow x 3)))))) in x 42.879 * [taylor]: Taking taylor expansion of (* 1/3 (log (+ (/ 1 (pow x 2)) (/ 1 (pow x 3))))) in x 42.879 * [taylor]: Taking taylor expansion of 1/3 in x 42.879 * [taylor]: Taking taylor expansion of (log (+ (/ 1 (pow x 2)) (/ 1 (pow x 3)))) in x 42.879 * [taylor]: Taking taylor expansion of (+ (/ 1 (pow x 2)) (/ 1 (pow x 3))) in x 42.879 * [taylor]: Taking taylor expansion of (/ 1 (pow x 2)) in x 42.879 * [taylor]: Taking taylor expansion of (pow x 2) in x 42.879 * [taylor]: Taking taylor expansion of x in x 42.879 * [taylor]: Taking taylor expansion of (/ 1 (pow x 3)) in x 42.879 * [taylor]: Taking taylor expansion of (pow x 3) in x 42.879 * [taylor]: Taking taylor expansion of x in x 42.880 * [taylor]: Taking taylor expansion of (pow (+ (/ 1 (pow x 2)) (/ 1 (pow x 3))) 1/3) in x 42.880 * [taylor]: Taking taylor expansion of (exp (* 1/3 (log (+ (/ 1 (pow x 2)) (/ 1 (pow x 3)))))) in x 42.880 * [taylor]: Taking taylor expansion of (* 1/3 (log (+ (/ 1 (pow x 2)) (/ 1 (pow x 3))))) in x 42.880 * [taylor]: Taking taylor expansion of 1/3 in x 42.880 * [taylor]: Taking taylor expansion of (log (+ (/ 1 (pow x 2)) (/ 1 (pow x 3)))) in x 42.880 * [taylor]: Taking taylor expansion of (+ (/ 1 (pow x 2)) (/ 1 (pow x 3))) in x 42.880 * [taylor]: Taking taylor expansion of (/ 1 (pow x 2)) in x 42.880 * [taylor]: Taking taylor expansion of (pow x 2) in x 42.880 * [taylor]: Taking taylor expansion of x in x 42.880 * [taylor]: Taking taylor expansion of (/ 1 (pow x 3)) in x 42.880 * [taylor]: Taking taylor expansion of (pow x 3) in x 42.880 * [taylor]: Taking taylor expansion of x in x 42.882 * [approximate]: Taking taylor expansion of (pow (- (/ 1 (pow x 2)) (/ 1 (pow x 3))) 1/3) in (x) around 0 42.882 * [taylor]: Taking taylor expansion of (pow (- (/ 1 (pow x 2)) (/ 1 (pow x 3))) 1/3) in x 42.882 * [taylor]: Taking taylor expansion of (exp (* 1/3 (log (- (/ 1 (pow x 2)) (/ 1 (pow x 3)))))) in x 42.882 * [taylor]: Taking taylor expansion of (* 1/3 (log (- (/ 1 (pow x 2)) (/ 1 (pow x 3))))) in x 42.882 * [taylor]: Taking taylor expansion of 1/3 in x 42.882 * [taylor]: Taking taylor expansion of (log (- (/ 1 (pow x 2)) (/ 1 (pow x 3)))) in x 42.882 * [taylor]: Taking taylor expansion of (- (/ 1 (pow x 2)) (/ 1 (pow x 3))) in x 42.882 * [taylor]: Taking taylor expansion of (/ 1 (pow x 2)) in x 42.882 * [taylor]: Taking taylor expansion of (pow x 2) in x 42.882 * [taylor]: Taking taylor expansion of x in x 42.882 * [taylor]: Taking taylor expansion of (/ 1 (pow x 3)) in x 42.883 * [taylor]: Taking taylor expansion of (pow x 3) in x 42.883 * [taylor]: Taking taylor expansion of x in x 42.883 * [taylor]: Taking taylor expansion of (pow (- (/ 1 (pow x 2)) (/ 1 (pow x 3))) 1/3) in x 42.883 * [taylor]: Taking taylor expansion of (exp (* 1/3 (log (- (/ 1 (pow x 2)) (/ 1 (pow x 3)))))) in x 42.883 * [taylor]: Taking taylor expansion of (* 1/3 (log (- (/ 1 (pow x 2)) (/ 1 (pow x 3))))) in x 42.883 * [taylor]: Taking taylor expansion of 1/3 in x 42.883 * [taylor]: Taking taylor expansion of (log (- (/ 1 (pow x 2)) (/ 1 (pow x 3)))) in x 42.883 * [taylor]: Taking taylor expansion of (- (/ 1 (pow x 2)) (/ 1 (pow x 3))) in x 42.883 * [taylor]: Taking taylor expansion of (/ 1 (pow x 2)) in x 42.883 * [taylor]: Taking taylor expansion of (pow x 2) in x 42.883 * [taylor]: Taking taylor expansion of x in x 42.883 * [taylor]: Taking taylor expansion of (/ 1 (pow x 3)) in x 42.883 * [taylor]: Taking taylor expansion of (pow x 3) in x 42.883 * [taylor]: Taking taylor expansion of x in x 42.885 * * * * [progress]: [ 3 / 4 ] generating series at (2 1 1) 42.885 * [approximate]: Taking taylor expansion of (pow (+ (pow x 2) (pow x 3)) 1/3) in (x) around 0 42.885 * [taylor]: Taking taylor expansion of (pow (+ (pow x 2) (pow x 3)) 1/3) in x 42.885 * [taylor]: Taking taylor expansion of (exp (* 1/3 (log (+ (pow x 2) (pow x 3))))) in x 42.885 * [taylor]: Taking taylor expansion of (* 1/3 (log (+ (pow x 2) (pow x 3)))) in x 42.885 * [taylor]: Taking taylor expansion of 1/3 in x 42.885 * [taylor]: Taking taylor expansion of (log (+ (pow x 2) (pow x 3))) in x 42.885 * [taylor]: Taking taylor expansion of (+ (pow x 2) (pow x 3)) in x 42.885 * [taylor]: Taking taylor expansion of (pow x 2) in x 42.885 * [taylor]: Taking taylor expansion of x in x 42.885 * [taylor]: Taking taylor expansion of (pow x 3) in x 42.885 * [taylor]: Taking taylor expansion of x in x 42.886 * [taylor]: Taking taylor expansion of (pow (+ (pow x 2) (pow x 3)) 1/3) in x 42.886 * [taylor]: Taking taylor expansion of (exp (* 1/3 (log (+ (pow x 2) (pow x 3))))) in x 42.886 * [taylor]: Taking taylor expansion of (* 1/3 (log (+ (pow x 2) (pow x 3)))) in x 42.886 * [taylor]: Taking taylor expansion of 1/3 in x 42.886 * [taylor]: Taking taylor expansion of (log (+ (pow x 2) (pow x 3))) in x 42.886 * [taylor]: Taking taylor expansion of (+ (pow x 2) (pow x 3)) in x 42.886 * [taylor]: Taking taylor expansion of (pow x 2) in x 42.886 * [taylor]: Taking taylor expansion of x in x 42.886 * [taylor]: Taking taylor expansion of (pow x 3) in x 42.886 * [taylor]: Taking taylor expansion of x in x 42.888 * [approximate]: Taking taylor expansion of (pow (+ (/ 1 (pow x 2)) (/ 1 (pow x 3))) 1/3) in (x) around 0 42.888 * [taylor]: Taking taylor expansion of (pow (+ (/ 1 (pow x 2)) (/ 1 (pow x 3))) 1/3) in x 42.888 * [taylor]: Taking taylor expansion of (exp (* 1/3 (log (+ (/ 1 (pow x 2)) (/ 1 (pow x 3)))))) in x 42.888 * [taylor]: Taking taylor expansion of (* 1/3 (log (+ (/ 1 (pow x 2)) (/ 1 (pow x 3))))) in x 42.888 * [taylor]: Taking taylor expansion of 1/3 in x 42.888 * [taylor]: Taking taylor expansion of (log (+ (/ 1 (pow x 2)) (/ 1 (pow x 3)))) in x 42.888 * [taylor]: Taking taylor expansion of (+ (/ 1 (pow x 2)) (/ 1 (pow x 3))) in x 42.888 * [taylor]: Taking taylor expansion of (/ 1 (pow x 2)) in x 42.888 * [taylor]: Taking taylor expansion of (pow x 2) in x 42.888 * [taylor]: Taking taylor expansion of x in x 42.888 * [taylor]: Taking taylor expansion of (/ 1 (pow x 3)) in x 42.888 * [taylor]: Taking taylor expansion of (pow x 3) in x 42.888 * [taylor]: Taking taylor expansion of x in x 42.888 * [taylor]: Taking taylor expansion of (pow (+ (/ 1 (pow x 2)) (/ 1 (pow x 3))) 1/3) in x 42.888 * [taylor]: Taking taylor expansion of (exp (* 1/3 (log (+ (/ 1 (pow x 2)) (/ 1 (pow x 3)))))) in x 42.888 * [taylor]: Taking taylor expansion of (* 1/3 (log (+ (/ 1 (pow x 2)) (/ 1 (pow x 3))))) in x 42.888 * [taylor]: Taking taylor expansion of 1/3 in x 42.888 * [taylor]: Taking taylor expansion of (log (+ (/ 1 (pow x 2)) (/ 1 (pow x 3)))) in x 42.888 * [taylor]: Taking taylor expansion of (+ (/ 1 (pow x 2)) (/ 1 (pow x 3))) in x 42.888 * [taylor]: Taking taylor expansion of (/ 1 (pow x 2)) in x 42.888 * [taylor]: Taking taylor expansion of (pow x 2) in x 42.888 * [taylor]: Taking taylor expansion of x in x 42.889 * [taylor]: Taking taylor expansion of (/ 1 (pow x 3)) in x 42.889 * [taylor]: Taking taylor expansion of (pow x 3) in x 42.889 * [taylor]: Taking taylor expansion of x in x 42.891 * [approximate]: Taking taylor expansion of (pow (- (/ 1 (pow x 2)) (/ 1 (pow x 3))) 1/3) in (x) around 0 42.891 * [taylor]: Taking taylor expansion of (pow (- (/ 1 (pow x 2)) (/ 1 (pow x 3))) 1/3) in x 42.891 * [taylor]: Taking taylor expansion of (exp (* 1/3 (log (- (/ 1 (pow x 2)) (/ 1 (pow x 3)))))) in x 42.891 * [taylor]: Taking taylor expansion of (* 1/3 (log (- (/ 1 (pow x 2)) (/ 1 (pow x 3))))) in x 42.891 * [taylor]: Taking taylor expansion of 1/3 in x 42.891 * [taylor]: Taking taylor expansion of (log (- (/ 1 (pow x 2)) (/ 1 (pow x 3)))) in x 42.891 * [taylor]: Taking taylor expansion of (- (/ 1 (pow x 2)) (/ 1 (pow x 3))) in x 42.891 * [taylor]: Taking taylor expansion of (/ 1 (pow x 2)) in x 42.891 * [taylor]: Taking taylor expansion of (pow x 2) in x 42.891 * [taylor]: Taking taylor expansion of x in x 42.891 * [taylor]: Taking taylor expansion of (/ 1 (pow x 3)) in x 42.891 * [taylor]: Taking taylor expansion of (pow x 3) in x 42.891 * [taylor]: Taking taylor expansion of x in x 42.891 * [taylor]: Taking taylor expansion of (pow (- (/ 1 (pow x 2)) (/ 1 (pow x 3))) 1/3) in x 42.891 * [taylor]: Taking taylor expansion of (exp (* 1/3 (log (- (/ 1 (pow x 2)) (/ 1 (pow x 3)))))) in x 42.891 * [taylor]: Taking taylor expansion of (* 1/3 (log (- (/ 1 (pow x 2)) (/ 1 (pow x 3))))) in x 42.891 * [taylor]: Taking taylor expansion of 1/3 in x 42.891 * [taylor]: Taking taylor expansion of (log (- (/ 1 (pow x 2)) (/ 1 (pow x 3)))) in x 42.891 * [taylor]: Taking taylor expansion of (- (/ 1 (pow x 2)) (/ 1 (pow x 3))) in x 42.891 * [taylor]: Taking taylor expansion of (/ 1 (pow x 2)) in x 42.891 * [taylor]: Taking taylor expansion of (pow x 2) in x 42.891 * [taylor]: Taking taylor expansion of x in x 42.891 * [taylor]: Taking taylor expansion of (/ 1 (pow x 3)) in x 42.891 * [taylor]: Taking taylor expansion of (pow x 3) in x 42.891 * [taylor]: Taking taylor expansion of x in x 42.894 * * * * [progress]: [ 4 / 4 ] generating series at (2 1) 42.894 * [approximate]: Taking taylor expansion of (pow (pow (+ (pow x 2) (pow x 3)) 2) 1/3) in (x) around 0 42.894 * [taylor]: Taking taylor expansion of (pow (pow (+ (pow x 2) (pow x 3)) 2) 1/3) in x 42.894 * [taylor]: Taking taylor expansion of (exp (* 1/3 (log (pow (+ (pow x 2) (pow x 3)) 2)))) in x 42.894 * [taylor]: Taking taylor expansion of (* 1/3 (log (pow (+ (pow x 2) (pow x 3)) 2))) in x 42.894 * [taylor]: Taking taylor expansion of 1/3 in x 42.894 * [taylor]: Taking taylor expansion of (log (pow (+ (pow x 2) (pow x 3)) 2)) in x 42.894 * [taylor]: Taking taylor expansion of (pow (+ (pow x 2) (pow x 3)) 2) in x 42.894 * [taylor]: Taking taylor expansion of (+ (pow x 2) (pow x 3)) in x 42.894 * [taylor]: Taking taylor expansion of (pow x 2) in x 42.894 * [taylor]: Taking taylor expansion of x in x 42.894 * [taylor]: Taking taylor expansion of (pow x 3) in x 42.894 * [taylor]: Taking taylor expansion of x in x 42.894 * [taylor]: Taking taylor expansion of (pow (pow (+ (pow x 2) (pow x 3)) 2) 1/3) in x 42.894 * [taylor]: Taking taylor expansion of (exp (* 1/3 (log (pow (+ (pow x 2) (pow x 3)) 2)))) in x 42.894 * [taylor]: Taking taylor expansion of (* 1/3 (log (pow (+ (pow x 2) (pow x 3)) 2))) in x 42.894 * [taylor]: Taking taylor expansion of 1/3 in x 42.894 * [taylor]: Taking taylor expansion of (log (pow (+ (pow x 2) (pow x 3)) 2)) in x 42.894 * [taylor]: Taking taylor expansion of (pow (+ (pow x 2) (pow x 3)) 2) in x 42.894 * [taylor]: Taking taylor expansion of (+ (pow x 2) (pow x 3)) in x 42.894 * [taylor]: Taking taylor expansion of (pow x 2) in x 42.894 * [taylor]: Taking taylor expansion of x in x 42.894 * [taylor]: Taking taylor expansion of (pow x 3) in x 42.894 * [taylor]: Taking taylor expansion of x in x 42.897 * [approximate]: Taking taylor expansion of (pow (pow (+ (/ 1 (pow x 2)) (/ 1 (pow x 3))) 2) 1/3) in (x) around 0 42.897 * [taylor]: Taking taylor expansion of (pow (pow (+ (/ 1 (pow x 2)) (/ 1 (pow x 3))) 2) 1/3) in x 42.897 * [taylor]: Taking taylor expansion of (exp (* 1/3 (log (pow (+ (/ 1 (pow x 2)) (/ 1 (pow x 3))) 2)))) in x 42.897 * [taylor]: Taking taylor expansion of (* 1/3 (log (pow (+ (/ 1 (pow x 2)) (/ 1 (pow x 3))) 2))) in x 42.897 * [taylor]: Taking taylor expansion of 1/3 in x 42.897 * [taylor]: Taking taylor expansion of (log (pow (+ (/ 1 (pow x 2)) (/ 1 (pow x 3))) 2)) in x 42.897 * [taylor]: Taking taylor expansion of (pow (+ (/ 1 (pow x 2)) (/ 1 (pow x 3))) 2) in x 42.897 * [taylor]: Taking taylor expansion of (+ (/ 1 (pow x 2)) (/ 1 (pow x 3))) in x 42.897 * [taylor]: Taking taylor expansion of (/ 1 (pow x 2)) in x 42.897 * [taylor]: Taking taylor expansion of (pow x 2) in x 42.897 * [taylor]: Taking taylor expansion of x in x 42.897 * [taylor]: Taking taylor expansion of (/ 1 (pow x 3)) in x 42.897 * [taylor]: Taking taylor expansion of (pow x 3) in x 42.897 * [taylor]: Taking taylor expansion of x in x 42.897 * [taylor]: Taking taylor expansion of (pow (pow (+ (/ 1 (pow x 2)) (/ 1 (pow x 3))) 2) 1/3) in x 42.897 * [taylor]: Taking taylor expansion of (exp (* 1/3 (log (pow (+ (/ 1 (pow x 2)) (/ 1 (pow x 3))) 2)))) in x 42.897 * [taylor]: Taking taylor expansion of (* 1/3 (log (pow (+ (/ 1 (pow x 2)) (/ 1 (pow x 3))) 2))) in x 42.897 * [taylor]: Taking taylor expansion of 1/3 in x 42.897 * [taylor]: Taking taylor expansion of (log (pow (+ (/ 1 (pow x 2)) (/ 1 (pow x 3))) 2)) in x 42.897 * [taylor]: Taking taylor expansion of (pow (+ (/ 1 (pow x 2)) (/ 1 (pow x 3))) 2) in x 42.897 * [taylor]: Taking taylor expansion of (+ (/ 1 (pow x 2)) (/ 1 (pow x 3))) in x 42.897 * [taylor]: Taking taylor expansion of (/ 1 (pow x 2)) in x 42.897 * [taylor]: Taking taylor expansion of (pow x 2) in x 42.897 * [taylor]: Taking taylor expansion of x in x 42.897 * [taylor]: Taking taylor expansion of (/ 1 (pow x 3)) in x 42.897 * [taylor]: Taking taylor expansion of (pow x 3) in x 42.897 * [taylor]: Taking taylor expansion of x in x 42.900 * [approximate]: Taking taylor expansion of (pow (pow (- (/ 1 (pow x 2)) (/ 1 (pow x 3))) 2) 1/3) in (x) around 0 42.900 * [taylor]: Taking taylor expansion of (pow (pow (- (/ 1 (pow x 2)) (/ 1 (pow x 3))) 2) 1/3) in x 42.900 * [taylor]: Taking taylor expansion of (exp (* 1/3 (log (pow (- (/ 1 (pow x 2)) (/ 1 (pow x 3))) 2)))) in x 42.900 * [taylor]: Taking taylor expansion of (* 1/3 (log (pow (- (/ 1 (pow x 2)) (/ 1 (pow x 3))) 2))) in x 42.900 * [taylor]: Taking taylor expansion of 1/3 in x 42.900 * [taylor]: Taking taylor expansion of (log (pow (- (/ 1 (pow x 2)) (/ 1 (pow x 3))) 2)) in x 42.900 * [taylor]: Taking taylor expansion of (pow (- (/ 1 (pow x 2)) (/ 1 (pow x 3))) 2) in x 42.900 * [taylor]: Taking taylor expansion of (- (/ 1 (pow x 2)) (/ 1 (pow x 3))) in x 42.900 * [taylor]: Taking taylor expansion of (/ 1 (pow x 2)) in x 42.900 * [taylor]: Taking taylor expansion of (pow x 2) in x 42.900 * [taylor]: Taking taylor expansion of x in x 42.900 * [taylor]: Taking taylor expansion of (/ 1 (pow x 3)) in x 42.900 * [taylor]: Taking taylor expansion of (pow x 3) in x 42.900 * [taylor]: Taking taylor expansion of x in x 42.900 * [taylor]: Taking taylor expansion of (pow (pow (- (/ 1 (pow x 2)) (/ 1 (pow x 3))) 2) 1/3) in x 42.900 * [taylor]: Taking taylor expansion of (exp (* 1/3 (log (pow (- (/ 1 (pow x 2)) (/ 1 (pow x 3))) 2)))) in x 42.900 * [taylor]: Taking taylor expansion of (* 1/3 (log (pow (- (/ 1 (pow x 2)) (/ 1 (pow x 3))) 2))) in x 42.900 * [taylor]: Taking taylor expansion of 1/3 in x 42.900 * [taylor]: Taking taylor expansion of (log (pow (- (/ 1 (pow x 2)) (/ 1 (pow x 3))) 2)) in x 42.900 * [taylor]: Taking taylor expansion of (pow (- (/ 1 (pow x 2)) (/ 1 (pow x 3))) 2) in x 42.900 * [taylor]: Taking taylor expansion of (- (/ 1 (pow x 2)) (/ 1 (pow x 3))) in x 42.900 * [taylor]: Taking taylor expansion of (/ 1 (pow x 2)) in x 42.900 * [taylor]: Taking taylor expansion of (pow x 2) in x 42.900 * [taylor]: Taking taylor expansion of x in x 42.900 * [taylor]: Taking taylor expansion of (/ 1 (pow x 3)) in x 42.900 * [taylor]: Taking taylor expansion of (pow x 3) in x 42.900 * [taylor]: Taking taylor expansion of x in x 42.902 * * * [progress]: simplifying candidates 42.904 * [simplify]: Simplifying using # : (log (cbrt (+ (pow x 3) (* x x)))) (exp (cbrt (+ (pow x 3) (* x x)))) (cbrt (* (cbrt (+ (pow x 3) (* x x))) (cbrt (+ (pow x 3) (* x x))))) (cbrt (cbrt (+ (pow x 3) (* x x)))) (cbrt (sqrt (+ (pow x 3) (* x x)))) (cbrt (sqrt (+ (pow x 3) (* x x)))) (cbrt 1) (cbrt (+ (pow x 3) (* x x))) (cbrt x) (cbrt (+ (* x x) x)) (cbrt x) (cbrt (+ (* x x) x)) (cbrt (+ x 1)) (cbrt (* x x)) (cbrt (+ (pow (pow x 3) 3) (pow (* x x) 3))) (cbrt (+ (* (pow x 3) (pow x 3)) (- (* (* x x) (* x x)) (* (pow x 3) (* x x))))) (cbrt (- (* (pow x 3) (pow x 3)) (* (* x x) (* x x)))) (cbrt (- (pow x 3) (* x x))) (* (cbrt (cbrt (+ (pow x 3) (* x x)))) (cbrt (cbrt (+ (pow x 3) (* x x))))) (cbrt (cbrt (+ (pow x 3) (* x x)))) (* (* (cbrt (+ (pow x 3) (* x x))) (cbrt (+ (pow x 3) (* x x)))) (cbrt (+ (pow x 3) (* x x)))) (sqrt (cbrt (+ (pow x 3) (* x x)))) (sqrt (cbrt (+ (pow x 3) (* x x)))) (log (cbrt (+ (pow x 3) (* x x)))) (exp (cbrt (+ (pow x 3) (* x x)))) (cbrt (* (cbrt (+ (pow x 3) (* x x))) (cbrt (+ (pow x 3) (* x x))))) (cbrt (cbrt (+ (pow x 3) (* x x)))) (cbrt (sqrt (+ (pow x 3) (* x x)))) (cbrt (sqrt (+ (pow x 3) (* x x)))) (cbrt 1) (cbrt (+ (pow x 3) (* x x))) (cbrt x) (cbrt (+ (* x x) x)) (cbrt x) (cbrt (+ (* x x) x)) (cbrt (+ x 1)) (cbrt (* x x)) (cbrt (+ (pow (pow x 3) 3) (pow (* x x) 3))) (cbrt (+ (* (pow x 3) (pow x 3)) (- (* (* x x) (* x x)) (* (pow x 3) (* x x))))) (cbrt (- (* (pow x 3) (pow x 3)) (* (* x x) (* x x)))) (cbrt (- (pow x 3) (* x x))) (* (cbrt (cbrt (+ (pow x 3) (* x x)))) (cbrt (cbrt (+ (pow x 3) (* x x))))) (cbrt (cbrt (+ (pow x 3) (* x x)))) (* (* (cbrt (+ (pow x 3) (* x x))) (cbrt (+ (pow x 3) (* x x)))) (cbrt (+ (pow x 3) (* x x)))) (sqrt (cbrt (+ (pow x 3) (* x x)))) (sqrt (cbrt (+ (pow x 3) (* x x)))) (log (cbrt (+ (pow x 3) (* x x)))) (exp (cbrt (+ (pow x 3) (* x x)))) (cbrt (* (cbrt (+ (pow x 3) (* x x))) (cbrt (+ (pow x 3) (* x x))))) (cbrt (cbrt (+ (pow x 3) (* x x)))) (cbrt (sqrt (+ (pow x 3) (* x x)))) (cbrt (sqrt (+ (pow x 3) (* x x)))) (cbrt 1) (cbrt (+ (pow x 3) (* x x))) (cbrt x) (cbrt (+ (* x x) x)) (cbrt x) (cbrt (+ (* x x) x)) (cbrt (+ x 1)) (cbrt (* x x)) (cbrt (+ (pow (pow x 3) 3) (pow (* x x) 3))) (cbrt (+ (* (pow x 3) (pow x 3)) (- (* (* x x) (* x x)) (* (pow x 3) (* x x))))) (cbrt (- (* (pow x 3) (pow x 3)) (* (* x x) (* x x)))) (cbrt (- (pow x 3) (* x x))) (* (cbrt (cbrt (+ (pow x 3) (* x x)))) (cbrt (cbrt (+ (pow x 3) (* x x))))) (cbrt (cbrt (+ (pow x 3) (* x x)))) (* (* (cbrt (+ (pow x 3) (* x x))) (cbrt (+ (pow x 3) (* x x)))) (cbrt (+ (pow x 3) (* x x)))) (sqrt (cbrt (+ (pow x 3) (* x x)))) (sqrt (cbrt (+ (pow x 3) (* x x)))) (+ 1/3 1/3) (+ 1 1) (* (+ (pow x 3) (* x x)) (+ (pow x 3) (* x x))) (* (cbrt (+ (pow x 3) (* x x))) (cbrt (+ (pow x 3) (* x x)))) (+ 1 1) (+ (log (cbrt (+ (pow x 3) (* x x)))) (log (cbrt (+ (pow x 3) (* x x))))) (log (* (cbrt (+ (pow x 3) (* x x))) (cbrt (+ (pow x 3) (* x x))))) (exp (* (cbrt (+ (pow x 3) (* x x))) (cbrt (+ (pow x 3) (* x x))))) (* (+ (pow x 3) (* x x)) (+ (pow x 3) (* x x))) (* (cbrt (* (cbrt (+ (pow x 3) (* x x))) (cbrt (+ (pow x 3) (* x x))))) (cbrt (* (cbrt (+ (pow x 3) (* x x))) (cbrt (+ (pow x 3) (* x x)))))) (cbrt (* (cbrt (+ (pow x 3) (* x x))) (cbrt (+ (pow x 3) (* x x))))) (* (* (* (cbrt (+ (pow x 3) (* x x))) (cbrt (+ (pow x 3) (* x x)))) (* (cbrt (+ (pow x 3) (* x x))) (cbrt (+ (pow x 3) (* x x))))) (* (cbrt (+ (pow x 3) (* x x))) (cbrt (+ (pow x 3) (* x x))))) (sqrt (* (cbrt (+ (pow x 3) (* x x))) (cbrt (+ (pow x 3) (* x x))))) (sqrt (* (cbrt (+ (pow x 3) (* x x))) (cbrt (+ (pow x 3) (* x x))))) (* (cbrt (+ (pow (pow x 3) 3) (pow (* x x) 3))) (cbrt (+ (pow (pow x 3) 3) (pow (* x x) 3)))) (* (cbrt (+ (* (pow x 3) (pow x 3)) (- (* (* x x) (* x x)) (* (pow x 3) (* x x))))) (cbrt (+ (* (pow x 3) (pow x 3)) (- (* (* x x) (* x x)) (* (pow x 3) (* x x)))))) (* (cbrt (+ (pow (pow x 3) 3) (pow (* x x) 3))) (cbrt (- (* (pow x 3) (pow x 3)) (* (* x x) (* x x))))) (* (cbrt (+ (* (pow x 3) (pow x 3)) (- (* (* x x) (* x x)) (* (pow x 3) (* x x))))) (cbrt (- (pow x 3) (* x x)))) (* (cbrt (- (* (pow x 3) (pow x 3)) (* (* x x) (* x x)))) (cbrt (+ (pow (pow x 3) 3) (pow (* x x) 3)))) (* (cbrt (- (pow x 3) (* x x))) (cbrt (+ (* (pow x 3) (pow x 3)) (- (* (* x x) (* x x)) (* (pow x 3) (* x x)))))) (* (cbrt (- (* (pow x 3) (pow x 3)) (* (* x x) (* x x)))) (cbrt (- (* (pow x 3) (pow x 3)) (* (* x x) (* x x))))) (* (cbrt (- (pow x 3) (* x x))) (cbrt (- (pow x 3) (* x x)))) (* (cbrt (* (cbrt (+ (pow x 3) (* x x))) (cbrt (+ (pow x 3) (* x x))))) (cbrt (* (cbrt (+ (pow x 3) (* x x))) (cbrt (+ (pow x 3) (* x x)))))) (* (cbrt (cbrt (+ (pow x 3) (* x x)))) (cbrt (cbrt (+ (pow x 3) (* x x))))) (* (cbrt (sqrt (+ (pow x 3) (* x x)))) (cbrt (sqrt (+ (pow x 3) (* x x))))) (* (cbrt (sqrt (+ (pow x 3) (* x x)))) (cbrt (sqrt (+ (pow x 3) (* x x))))) (* (cbrt 1) (cbrt 1)) (* (cbrt (+ (pow x 3) (* x x))) (cbrt (+ (pow x 3) (* x x)))) (* (cbrt x) (cbrt x)) (* (cbrt (+ (* x x) x)) (cbrt (+ (* x x) x))) (* (cbrt x) (cbrt x)) (* (cbrt (+ (* x x) x)) (cbrt (+ (* x x) x))) (* (cbrt x) (cbrt x)) (* (cbrt (+ (* x x) x)) (cbrt (+ (* x x) x))) (* (cbrt x) (cbrt x)) (* (cbrt (+ (* x x) x)) (cbrt (+ (* x x) x))) (* (cbrt (+ x 1)) (cbrt (+ x 1))) (* (cbrt (* x x)) (cbrt (* x x))) (* (* (cbrt (cbrt (+ (pow x 3) (* x x)))) (cbrt (cbrt (+ (pow x 3) (* x x))))) (* (cbrt (cbrt (+ (pow x 3) (* x x)))) (cbrt (cbrt (+ (pow x 3) (* x x)))))) (* (cbrt (cbrt (+ (pow x 3) (* x x)))) (cbrt (cbrt (+ (pow x 3) (* x x))))) (* (sqrt (cbrt (+ (pow x 3) (* x x)))) (sqrt (cbrt (+ (pow x 3) (* x x))))) (* (sqrt (cbrt (+ (pow x 3) (* x x)))) (sqrt (cbrt (+ (pow x 3) (* x x))))) (* 1 1) (* (cbrt (+ (pow x 3) (* x x))) (cbrt (+ (pow x 3) (* x x)))) (* (cbrt (sqrt (+ (pow x 3) (* x x)))) (cbrt (sqrt (+ (pow x 3) (* x x))))) (* (cbrt (sqrt (+ (pow x 3) (* x x)))) (cbrt (sqrt (+ (pow x 3) (* x x))))) (* (cbrt (sqrt (+ (pow x 3) (* x x)))) (sqrt (cbrt (+ (pow x 3) (* x x))))) (* (cbrt (sqrt (+ (pow x 3) (* x x)))) (sqrt (cbrt (+ (pow x 3) (* x x))))) (* (sqrt (cbrt (+ (pow x 3) (* x x)))) (cbrt (sqrt (+ (pow x 3) (* x x))))) (* (sqrt (cbrt (+ (pow x 3) (* x x)))) (cbrt (sqrt (+ (pow x 3) (* x x))))) (* (sqrt (cbrt (+ (pow x 3) (* x x)))) (sqrt (cbrt (+ (pow x 3) (* x x))))) (* (sqrt (cbrt (+ (pow x 3) (* x x)))) (sqrt (cbrt (+ (pow x 3) (* x x))))) (* 2 1/3) (* 2 1) (* (cbrt (+ (pow x 3) (* x x))) (cbrt (* (cbrt (+ (pow x 3) (* x x))) (cbrt (+ (pow x 3) (* x x)))))) (* (cbrt (+ (pow x 3) (* x x))) (cbrt (sqrt (+ (pow x 3) (* x x))))) (* (cbrt (+ (pow x 3) (* x x))) (cbrt 1)) (* (cbrt (+ (pow x 3) (* x x))) (cbrt x)) (* (cbrt (+ (pow x 3) (* x x))) (cbrt x)) (* (cbrt (+ (pow x 3) (* x x))) (cbrt (+ x 1))) (* (cbrt (+ (pow x 3) (* x x))) (* (cbrt (cbrt (+ (pow x 3) (* x x)))) (cbrt (cbrt (+ (pow x 3) (* x x)))))) (* (cbrt (+ (pow x 3) (* x x))) (sqrt (cbrt (+ (pow x 3) (* x x))))) (* (cbrt (+ (pow x 3) (* x x))) 1) (* (cbrt (cbrt (+ (pow x 3) (* x x)))) (cbrt (+ (pow x 3) (* x x)))) (* (cbrt (sqrt (+ (pow x 3) (* x x)))) (cbrt (+ (pow x 3) (* x x)))) (* (cbrt (+ (pow x 3) (* x x))) (cbrt (+ (pow x 3) (* x x)))) (* (cbrt (+ (* x x) x)) (cbrt (+ (pow x 3) (* x x)))) (* (cbrt (+ (* x x) x)) (cbrt (+ (pow x 3) (* x x)))) (* (cbrt (* x x)) (cbrt (+ (pow x 3) (* x x)))) (* (cbrt (cbrt (+ (pow x 3) (* x x)))) (cbrt (+ (pow x 3) (* x x)))) (* (sqrt (cbrt (+ (pow x 3) (* x x)))) (cbrt (+ (pow x 3) (* x x)))) (* (cbrt (+ (pow x 3) (* x x))) (cbrt (+ (pow x 3) (* x x)))) (* (cbrt (+ (pow x 3) (* x x))) (cbrt (+ (pow (pow x 3) 3) (pow (* x x) 3)))) (* (cbrt (+ (pow x 3) (* x x))) (cbrt (- (* (pow x 3) (pow x 3)) (* (* x x) (* x x))))) (* (cbrt (+ (pow (pow x 3) 3) (pow (* x x) 3))) (cbrt (+ (pow x 3) (* x x)))) (* (cbrt (- (* (pow x 3) (pow x 3)) (* (* x x) (* x x)))) (cbrt (+ (pow x 3) (* x x)))) (- (+ (* 1/3 (* x (exp (* 1/3 (+ (log 1) (* 2 (log x))))))) (exp (* 1/3 (+ (log 1) (* 2 (log x)))))) (* 1/9 (* (pow x 2) (exp (* 1/3 (+ (log 1) (* 2 (log x)))))))) (- (+ (exp (* 1/3 (- (log 1) (* 3 (log (/ 1 x)))))) (* 1/3 (/ (exp (* 1/3 (- (log 1) (* 3 (log (/ 1 x)))))) x))) (* 1/9 (/ (exp (* 1/3 (- (log 1) (* 3 (log (/ 1 x)))))) (pow x 2)))) (- (+ (exp (* 1/3 (- (log (neg 1)) (* 3 (log (/ -1 x)))))) (* 1/3 (/ (exp (* 1/3 (- (log (neg 1)) (* 3 (log (/ -1 x)))))) x))) (* 1/9 (/ (exp (* 1/3 (- (log (neg 1)) (* 3 (log (/ -1 x)))))) (pow x 2)))) (- (+ (* 1/3 (* x (exp (* 1/3 (+ (log 1) (* 2 (log x))))))) (exp (* 1/3 (+ (log 1) (* 2 (log x)))))) (* 1/9 (* (pow x 2) (exp (* 1/3 (+ (log 1) (* 2 (log x)))))))) (- (+ (exp (* 1/3 (- (log 1) (* 3 (log (/ 1 x)))))) (* 1/3 (/ (exp (* 1/3 (- (log 1) (* 3 (log (/ 1 x)))))) x))) (* 1/9 (/ (exp (* 1/3 (- (log 1) (* 3 (log (/ 1 x)))))) (pow x 2)))) (- (+ (exp (* 1/3 (- (log (neg 1)) (* 3 (log (/ -1 x)))))) (* 1/3 (/ (exp (* 1/3 (- (log (neg 1)) (* 3 (log (/ -1 x)))))) x))) (* 1/9 (/ (exp (* 1/3 (- (log (neg 1)) (* 3 (log (/ -1 x)))))) (pow x 2)))) (- (+ (* 1/3 (* x (exp (* 1/3 (+ (log 1) (* 2 (log x))))))) (exp (* 1/3 (+ (log 1) (* 2 (log x)))))) (* 1/9 (* (pow x 2) (exp (* 1/3 (+ (log 1) (* 2 (log x)))))))) (- (+ (exp (* 1/3 (- (log 1) (* 3 (log (/ 1 x)))))) (* 1/3 (/ (exp (* 1/3 (- (log 1) (* 3 (log (/ 1 x)))))) x))) (* 1/9 (/ (exp (* 1/3 (- (log 1) (* 3 (log (/ 1 x)))))) (pow x 2)))) (- (+ (exp (* 1/3 (- (log (neg 1)) (* 3 (log (/ -1 x)))))) (* 1/3 (/ (exp (* 1/3 (- (log (neg 1)) (* 3 (log (/ -1 x)))))) x))) (* 1/9 (/ (exp (* 1/3 (- (log (neg 1)) (* 3 (log (/ -1 x)))))) (pow x 2)))) (- (+ (* 2/3 (* (exp (* 1/3 (+ (log 1) (* 4 (log x))))) x)) (exp (* 1/3 (+ (log 1) (* 4 (log x)))))) (* 1/9 (* (exp (* 1/3 (+ (log 1) (* 4 (log x))))) (pow x 2)))) (- (+ (* 2/3 (/ (exp (* 1/3 (- (log 1) (* 6 (log (/ 1 x)))))) x)) (exp (* 1/3 (- (log 1) (* 6 (log (/ 1 x))))))) (* 1/9 (/ (exp (* 1/3 (- (log 1) (* 6 (log (/ 1 x)))))) (pow x 2)))) (- (+ (* 2/3 (/ (exp (* 1/3 (- (log 1) (* 6 (log (/ -1 x)))))) x)) (exp (* 1/3 (- (log 1) (* 6 (log (/ -1 x))))))) (* 1/9 (/ (exp (* 1/3 (- (log 1) (* 6 (log (/ -1 x)))))) (pow x 2)))) 42.905 * * [simplify]: iteration 0 : 7 enodes (cost 9 ) 42.906 * * [simplify]: iteration 1 : 15 enodes (cost 9 ) 42.908 * * [simplify]: iteration 2 : 28 enodes (cost 9 ) 42.911 * * [simplify]: iteration 3 : 46 enodes (cost 9 ) 42.922 * * [simplify]: iteration 4 : 76 enodes (cost 9 ) 42.935 * * [simplify]: iteration 5 : 148 enodes (cost 9 ) 42.995 * * [simplify]: iteration 6 : 398 enodes (cost 9 ) 43.465 * * [simplify]: iteration 7 : 1405 enodes (cost 9 ) 45.413 * * [simplify]: iteration done : 5000 enodes (cost 9 ) 45.414 * * [simplify]: iteration 0 : 7 enodes (cost 9 ) 45.415 * * [simplify]: iteration 1 : 15 enodes (cost 9 ) 45.416 * * [simplify]: iteration 2 : 28 enodes (cost 9 ) 45.420 * * [simplify]: iteration 3 : 46 enodes (cost 9 ) 45.425 * * [simplify]: iteration 4 : 76 enodes (cost 9 ) 45.439 * * [simplify]: iteration 5 : 148 enodes (cost 9 ) 45.499 * * [simplify]: iteration 6 : 398 enodes (cost 9 ) 45.971 * * [simplify]: iteration 7 : 1405 enodes (cost 9 ) 47.940 * * [simplify]: iteration done : 5000 enodes (cost 9 ) 47.941 * * [simplify]: iteration 0 : 8 enodes (cost 18 ) 47.942 * * [simplify]: iteration 1 : 16 enodes (cost 18 ) 47.944 * * [simplify]: iteration 2 : 29 enodes (cost 18 ) 47.947 * * [simplify]: iteration 3 : 47 enodes (cost 18 ) 47.953 * * [simplify]: iteration 4 : 77 enodes (cost 18 ) 47.970 * * [simplify]: iteration 5 : 145 enodes (cost 18 ) 48.030 * * [simplify]: iteration 6 : 395 enodes (cost 18 ) 48.528 * * [simplify]: iteration 7 : 1407 enodes (cost 18 ) 50.528 * * [simplify]: iteration done : 5000 enodes (cost 18 ) 50.529 * * [simplify]: iteration 0 : 7 enodes (cost 9 ) 50.530 * * [simplify]: iteration 1 : 15 enodes (cost 9 ) 50.532 * * [simplify]: iteration 2 : 28 enodes (cost 9 ) 50.535 * * [simplify]: iteration 3 : 46 enodes (cost 9 ) 50.541 * * [simplify]: iteration 4 : 76 enodes (cost 9 ) 50.555 * * [simplify]: iteration 5 : 148 enodes (cost 9 ) 50.616 * * [simplify]: iteration 6 : 398 enodes (cost 9 ) 51.093 * * [simplify]: iteration 7 : 1405 enodes (cost 9 ) 53.069 * * [simplify]: iteration done : 5000 enodes (cost 9 ) 53.069 * * [simplify]: iteration 0 : 7 enodes (cost 9 ) 53.070 * * [simplify]: iteration 1 : 15 enodes (cost 9 ) 53.072 * * [simplify]: iteration 2 : 28 enodes (cost 9 ) 53.076 * * [simplify]: iteration 3 : 46 enodes (cost 9 ) 53.082 * * [simplify]: iteration 4 : 76 enodes (cost 9 ) 53.100 * * [simplify]: iteration 5 : 148 enodes (cost 9 ) 53.162 * * [simplify]: iteration 6 : 398 enodes (cost 9 ) 53.640 * * [simplify]: iteration 7 : 1405 enodes (cost 9 ) 55.622 * * [simplify]: iteration done : 5000 enodes (cost 9 ) 55.623 * * [simplify]: iteration 0 : 7 enodes (cost 9 ) 55.624 * * [simplify]: iteration 1 : 15 enodes (cost 9 ) 55.626 * * [simplify]: iteration 2 : 28 enodes (cost 9 ) 55.630 * * [simplify]: iteration 3 : 46 enodes (cost 9 ) 55.635 * * [simplify]: iteration 4 : 76 enodes (cost 9 ) 55.648 * * [simplify]: iteration 5 : 148 enodes (cost 9 ) 55.708 * * [simplify]: iteration 6 : 398 enodes (cost 9 ) 56.196 * * [simplify]: iteration 7 : 1405 enodes (cost 9 ) 58.193 * * [simplify]: iteration done : 5000 enodes (cost 9 ) 58.193 * * [simplify]: iteration 0 : 2 enodes (cost 2 ) 58.193 * * [simplify]: iteration 1 : 4 enodes (cost 1 ) 58.194 * * [simplify]: iteration done : 4 enodes (cost 1 ) 58.194 * * [simplify]: iteration 0 : 6 enodes (cost 8 ) 58.195 * * [simplify]: iteration 1 : 14 enodes (cost 8 ) 58.197 * * [simplify]: iteration 2 : 27 enodes (cost 8 ) 58.200 * * [simplify]: iteration 3 : 45 enodes (cost 8 ) 58.205 * * [simplify]: iteration 4 : 75 enodes (cost 8 ) 58.223 * * [simplify]: iteration 5 : 145 enodes (cost 8 ) 58.282 * * [simplify]: iteration 6 : 388 enodes (cost 8 ) 58.787 * * [simplify]: iteration 7 : 1409 enodes (cost 8 ) 60.889 * * [simplify]: iteration done : 5000 enodes (cost 8 ) 60.890 * * [simplify]: iteration 0 : 2 enodes (cost 2 ) 60.890 * * [simplify]: iteration done : 2 enodes (cost 2 ) 60.891 * * [simplify]: iteration 0 : 4 enodes (cost 6 ) 60.892 * * [simplify]: iteration 1 : 8 enodes (cost 6 ) 60.893 * * [simplify]: iteration 2 : 12 enodes (cost 6 ) 60.894 * * [simplify]: iteration 3 : 18 enodes (cost 6 ) 60.896 * * [simplify]: iteration done : 18 enodes (cost 6 ) 60.897 * * [simplify]: iteration 0 : 2 enodes (cost 2 ) 60.897 * * [simplify]: iteration done : 2 enodes (cost 2 ) 60.898 * * [simplify]: iteration 0 : 4 enodes (cost 6 ) 60.898 * * [simplify]: iteration 1 : 8 enodes (cost 6 ) 60.899 * * [simplify]: iteration 2 : 12 enodes (cost 6 ) 60.900 * * [simplify]: iteration 3 : 18 enodes (cost 6 ) 60.903 * * [simplify]: iteration done : 18 enodes (cost 6 ) 60.903 * * [simplify]: iteration 0 : 4 enodes (cost 4 ) 60.904 * * [simplify]: iteration 1 : 7 enodes (cost 4 ) 60.904 * * [simplify]: iteration done : 7 enodes (cost 4 ) 60.905 * * [simplify]: iteration 0 : 3 enodes (cost 4 ) 60.905 * * [simplify]: iteration done : 3 enodes (cost 4 ) 60.905 * * [simplify]: iteration 0 : 8 enodes (cost 12 ) 60.907 * * [simplify]: iteration 1 : 26 enodes (cost 12 ) 60.912 * * [simplify]: iteration 2 : 91 enodes (cost 10 ) 60.949 * * [simplify]: iteration 3 : 292 enodes (cost 10 ) 61.414 * * [simplify]: iteration 4 : 1121 enodes (cost 10 ) 63.704 * * [simplify]: iteration done : 5000 enodes (cost 10 ) 63.705 * * [simplify]: iteration 0 : 10 enodes (cost 24 ) 63.707 * * [simplify]: iteration 1 : 32 enodes (cost 16 ) 63.717 * * [simplify]: iteration 2 : 95 enodes (cost 14 ) 63.743 * * [simplify]: iteration 3 : 313 enodes (cost 12 ) 63.957 * * [simplify]: iteration 4 : 1090 enodes (cost 12 ) 65.715 * * [simplify]: iteration 5 : 4690 enodes (cost 12 ) 67.468 * * [simplify]: iteration done : 5000 enodes (cost 12 ) 67.469 * * [simplify]: iteration 0 : 8 enodes (cost 16 ) 67.471 * * [simplify]: iteration 1 : 25 enodes (cost 10 ) 67.475 * * [simplify]: iteration 2 : 74 enodes (cost 8 ) 67.491 * * [simplify]: iteration 3 : 211 enodes (cost 8 ) 67.595 * * [simplify]: iteration 4 : 688 enodes (cost 8 ) 68.366 * * [simplify]: iteration 5 : 2881 enodes (cost 8 ) 70.191 * * [simplify]: iteration done : 5000 enodes (cost 8 ) 70.191 * * [simplify]: iteration 0 : 6 enodes (cost 8 ) 70.192 * * [simplify]: iteration 1 : 15 enodes (cost 8 ) 70.194 * * [simplify]: iteration 2 : 30 enodes (cost 8 ) 70.198 * * [simplify]: iteration 3 : 47 enodes (cost 8 ) 70.204 * * [simplify]: iteration 4 : 86 enodes (cost 8 ) 70.225 * * [simplify]: iteration 5 : 200 enodes (cost 8 ) 70.303 * * [simplify]: iteration 6 : 634 enodes (cost 8 ) 71.108 * * [simplify]: iteration 7 : 2555 enodes (cost 8 ) 73.283 * * [simplify]: iteration done : 5001 enodes (cost 8 ) 73.284 * * [simplify]: iteration 0 : 8 enodes (cost 19 ) 73.285 * * [simplify]: iteration 1 : 16 enodes (cost 19 ) 73.287 * * [simplify]: iteration 2 : 29 enodes (cost 19 ) 73.291 * * [simplify]: iteration 3 : 47 enodes (cost 19 ) 73.301 * * [simplify]: iteration 4 : 77 enodes (cost 19 ) 73.314 * * [simplify]: iteration 5 : 145 enodes (cost 19 ) 73.374 * * [simplify]: iteration 6 : 395 enodes (cost 19 ) 73.890 * * [simplify]: iteration 7 : 1407 enodes (cost 19 ) 75.922 * * [simplify]: iteration done : 5000 enodes (cost 19 ) 75.923 * * [simplify]: iteration 0 : 7 enodes (cost 9 ) 75.924 * * [simplify]: iteration 1 : 15 enodes (cost 9 ) 75.926 * * [simplify]: iteration 2 : 28 enodes (cost 9 ) 75.929 * * [simplify]: iteration 3 : 46 enodes (cost 9 ) 75.934 * * [simplify]: iteration 4 : 76 enodes (cost 9 ) 75.948 * * [simplify]: iteration 5 : 148 enodes (cost 9 ) 76.014 * * [simplify]: iteration 6 : 398 enodes (cost 9 ) 76.507 * * [simplify]: iteration 7 : 1405 enodes (cost 9 ) 78.503 * * [simplify]: iteration done : 5000 enodes (cost 9 ) 78.504 * * [simplify]: iteration 0 : 8 enodes (cost 26 ) 78.505 * * [simplify]: iteration 1 : 17 enodes (cost 26 ) 78.507 * * [simplify]: iteration 2 : 31 enodes (cost 10 ) 78.517 * * [simplify]: iteration 3 : 51 enodes (cost 7 ) 78.524 * * [simplify]: iteration 4 : 83 enodes (cost 7 ) 78.540 * * [simplify]: iteration 5 : 161 enodes (cost 7 ) 78.603 * * [simplify]: iteration 6 : 416 enodes (cost 7 ) 79.140 * * [simplify]: iteration 7 : 1522 enodes (cost 7 ) 80.999 * * [simplify]: iteration done : 5000 enodes (cost 7 ) 81.000 * * [simplify]: iteration 0 : 7 enodes (cost 9 ) 81.001 * * [simplify]: iteration 1 : 15 enodes (cost 9 ) 81.003 * * [simplify]: iteration 2 : 28 enodes (cost 9 ) 81.006 * * [simplify]: iteration 3 : 46 enodes (cost 9 ) 81.012 * * [simplify]: iteration 4 : 76 enodes (cost 9 ) 81.025 * * [simplify]: iteration 5 : 148 enodes (cost 9 ) 81.090 * * [simplify]: iteration 6 : 398 enodes (cost 9 ) 81.574 * * [simplify]: iteration 7 : 1405 enodes (cost 9 ) 83.827 * * [simplify]: iteration done : 5000 enodes (cost 9 ) 83.828 * * [simplify]: iteration 0 : 7 enodes (cost 9 ) 83.828 * * [simplify]: iteration 1 : 15 enodes (cost 9 ) 83.830 * * [simplify]: iteration 2 : 28 enodes (cost 9 ) 83.839 * * [simplify]: iteration 3 : 46 enodes (cost 9 ) 83.845 * * [simplify]: iteration 4 : 76 enodes (cost 9 ) 83.858 * * [simplify]: iteration 5 : 148 enodes (cost 9 ) 83.920 * * [simplify]: iteration 6 : 398 enodes (cost 9 ) 84.405 * * [simplify]: iteration 7 : 1405 enodes (cost 9 ) 86.448 * * [simplify]: iteration done : 5000 enodes (cost 9 ) 86.449 * * [simplify]: iteration 0 : 7 enodes (cost 9 ) 86.450 * * [simplify]: iteration 1 : 15 enodes (cost 9 ) 86.452 * * [simplify]: iteration 2 : 28 enodes (cost 9 ) 86.455 * * [simplify]: iteration 3 : 46 enodes (cost 9 ) 86.461 * * [simplify]: iteration 4 : 76 enodes (cost 9 ) 86.474 * * [simplify]: iteration 5 : 148 enodes (cost 9 ) 86.535 * * [simplify]: iteration 6 : 398 enodes (cost 9 ) 87.018 * * [simplify]: iteration 7 : 1405 enodes (cost 9 ) 89.009 * * [simplify]: iteration done : 5000 enodes (cost 9 ) 89.010 * * [simplify]: iteration 0 : 7 enodes (cost 9 ) 89.011 * * [simplify]: iteration 1 : 15 enodes (cost 9 ) 89.013 * * [simplify]: iteration 2 : 28 enodes (cost 9 ) 89.017 * * [simplify]: iteration 3 : 46 enodes (cost 9 ) 89.022 * * [simplify]: iteration 4 : 76 enodes (cost 9 ) 89.042 * * [simplify]: iteration 5 : 148 enodes (cost 9 ) 89.102 * * [simplify]: iteration 6 : 398 enodes (cost 9 ) 89.582 * * [simplify]: iteration 7 : 1405 enodes (cost 9 ) 91.594 * * [simplify]: iteration done : 5000 enodes (cost 9 ) 91.595 * * [simplify]: iteration 0 : 8 enodes (cost 18 ) 91.596 * * [simplify]: iteration 1 : 16 enodes (cost 18 ) 91.598 * * [simplify]: iteration 2 : 29 enodes (cost 18 ) 91.601 * * [simplify]: iteration 3 : 47 enodes (cost 18 ) 91.607 * * [simplify]: iteration 4 : 77 enodes (cost 18 ) 91.620 * * [simplify]: iteration 5 : 145 enodes (cost 18 ) 91.682 * * [simplify]: iteration 6 : 395 enodes (cost 18 ) 92.185 * * [simplify]: iteration 7 : 1407 enodes (cost 18 ) 94.199 * * [simplify]: iteration done : 5000 enodes (cost 18 ) 94.200 * * [simplify]: iteration 0 : 7 enodes (cost 9 ) 94.200 * * [simplify]: iteration 1 : 15 enodes (cost 9 ) 94.202 * * [simplify]: iteration 2 : 28 enodes (cost 9 ) 94.206 * * [simplify]: iteration 3 : 46 enodes (cost 9 ) 94.216 * * [simplify]: iteration 4 : 76 enodes (cost 9 ) 94.230 * * [simplify]: iteration 5 : 148 enodes (cost 9 ) 94.290 * * [simplify]: iteration 6 : 398 enodes (cost 9 ) 94.760 * * [simplify]: iteration 7 : 1405 enodes (cost 9 ) 96.740 * * [simplify]: iteration done : 5000 enodes (cost 9 ) 96.741 * * [simplify]: iteration 0 : 7 enodes (cost 9 ) 96.742 * * [simplify]: iteration 1 : 15 enodes (cost 9 ) 96.744 * * [simplify]: iteration 2 : 28 enodes (cost 9 ) 96.748 * * [simplify]: iteration 3 : 46 enodes (cost 9 ) 96.754 * * [simplify]: iteration 4 : 76 enodes (cost 9 ) 96.767 * * [simplify]: iteration 5 : 148 enodes (cost 9 ) 96.828 * * [simplify]: iteration 6 : 398 enodes (cost 9 ) 97.301 * * [simplify]: iteration 7 : 1405 enodes (cost 9 ) 99.280 * * [simplify]: iteration done : 5000 enodes (cost 9 ) 99.281 * * [simplify]: iteration 0 : 7 enodes (cost 9 ) 99.282 * * [simplify]: iteration 1 : 15 enodes (cost 9 ) 99.284 * * [simplify]: iteration 2 : 28 enodes (cost 9 ) 99.287 * * [simplify]: iteration 3 : 46 enodes (cost 9 ) 99.293 * * [simplify]: iteration 4 : 76 enodes (cost 9 ) 99.311 * * [simplify]: iteration 5 : 148 enodes (cost 9 ) 99.371 * * [simplify]: iteration 6 : 398 enodes (cost 9 ) 99.846 * * [simplify]: iteration 7 : 1405 enodes (cost 9 ) 101.858 * * [simplify]: iteration done : 5000 enodes (cost 9 ) 101.859 * * [simplify]: iteration 0 : 2 enodes (cost 2 ) 101.860 * * [simplify]: iteration 1 : 4 enodes (cost 1 ) 101.860 * * [simplify]: iteration done : 4 enodes (cost 1 ) 101.860 * * [simplify]: iteration 0 : 6 enodes (cost 8 ) 101.861 * * [simplify]: iteration 1 : 14 enodes (cost 8 ) 101.863 * * [simplify]: iteration 2 : 27 enodes (cost 8 ) 101.867 * * [simplify]: iteration 3 : 45 enodes (cost 8 ) 101.872 * * [simplify]: iteration 4 : 75 enodes (cost 8 ) 101.885 * * [simplify]: iteration 5 : 145 enodes (cost 8 ) 101.944 * * [simplify]: iteration 6 : 388 enodes (cost 8 ) 102.439 * * [simplify]: iteration 7 : 1409 enodes (cost 8 ) 104.577 * * [simplify]: iteration done : 5000 enodes (cost 8 ) 104.577 * * [simplify]: iteration 0 : 2 enodes (cost 2 ) 104.578 * * [simplify]: iteration done : 2 enodes (cost 2 ) 104.578 * * [simplify]: iteration 0 : 4 enodes (cost 6 ) 104.579 * * [simplify]: iteration 1 : 8 enodes (cost 6 ) 104.580 * * [simplify]: iteration 2 : 12 enodes (cost 6 ) 104.581 * * [simplify]: iteration 3 : 18 enodes (cost 6 ) 104.584 * * [simplify]: iteration done : 18 enodes (cost 6 ) 104.584 * * [simplify]: iteration 0 : 2 enodes (cost 2 ) 104.584 * * [simplify]: iteration done : 2 enodes (cost 2 ) 104.585 * * [simplify]: iteration 0 : 4 enodes (cost 6 ) 104.585 * * [simplify]: iteration 1 : 8 enodes (cost 6 ) 104.586 * * [simplify]: iteration 2 : 12 enodes (cost 6 ) 104.588 * * [simplify]: iteration 3 : 18 enodes (cost 6 ) 104.590 * * [simplify]: iteration done : 18 enodes (cost 6 ) 104.591 * * [simplify]: iteration 0 : 4 enodes (cost 4 ) 104.591 * * [simplify]: iteration 1 : 7 enodes (cost 4 ) 104.592 * * [simplify]: iteration done : 7 enodes (cost 4 ) 104.592 * * [simplify]: iteration 0 : 3 enodes (cost 4 ) 104.593 * * [simplify]: iteration done : 3 enodes (cost 4 ) 104.593 * * [simplify]: iteration 0 : 8 enodes (cost 12 ) 104.594 * * [simplify]: iteration 1 : 26 enodes (cost 12 ) 104.600 * * [simplify]: iteration 2 : 91 enodes (cost 10 ) 104.639 * * [simplify]: iteration 3 : 292 enodes (cost 10 ) 104.904 * * [simplify]: iteration 4 : 1121 enodes (cost 10 ) 107.186 * * [simplify]: iteration done : 5000 enodes (cost 10 ) 107.186 * * [simplify]: iteration 0 : 10 enodes (cost 24 ) 107.188 * * [simplify]: iteration 1 : 32 enodes (cost 16 ) 107.195 * * [simplify]: iteration 2 : 95 enodes (cost 14 ) 107.227 * * [simplify]: iteration 3 : 313 enodes (cost 12 ) 107.447 * * [simplify]: iteration 4 : 1090 enodes (cost 12 ) 109.412 * * [simplify]: iteration 5 : 4690 enodes (cost 12 ) 111.190 * * [simplify]: iteration done : 5000 enodes (cost 12 ) 111.191 * * [simplify]: iteration 0 : 8 enodes (cost 16 ) 111.192 * * [simplify]: iteration 1 : 25 enodes (cost 10 ) 111.197 * * [simplify]: iteration 2 : 74 enodes (cost 8 ) 111.212 * * [simplify]: iteration 3 : 211 enodes (cost 8 ) 111.314 * * [simplify]: iteration 4 : 688 enodes (cost 8 ) 112.087 * * [simplify]: iteration 5 : 2881 enodes (cost 8 ) 113.942 * * [simplify]: iteration done : 5000 enodes (cost 8 ) 113.942 * * [simplify]: iteration 0 : 6 enodes (cost 8 ) 113.943 * * [simplify]: iteration 1 : 15 enodes (cost 8 ) 113.945 * * [simplify]: iteration 2 : 30 enodes (cost 8 ) 113.949 * * [simplify]: iteration 3 : 47 enodes (cost 8 ) 113.956 * * [simplify]: iteration 4 : 86 enodes (cost 8 ) 113.972 * * [simplify]: iteration 5 : 200 enodes (cost 8 ) 114.055 * * [simplify]: iteration 6 : 634 enodes (cost 8 ) 114.852 * * [simplify]: iteration 7 : 2555 enodes (cost 8 ) 117.018 * * [simplify]: iteration done : 5001 enodes (cost 8 ) 117.019 * * [simplify]: iteration 0 : 8 enodes (cost 19 ) 117.021 * * [simplify]: iteration 1 : 16 enodes (cost 19 ) 117.023 * * [simplify]: iteration 2 : 29 enodes (cost 19 ) 117.026 * * [simplify]: iteration 3 : 47 enodes (cost 19 ) 117.032 * * [simplify]: iteration 4 : 77 enodes (cost 19 ) 117.046 * * [simplify]: iteration 5 : 145 enodes (cost 19 ) 117.111 * * [simplify]: iteration 6 : 395 enodes (cost 19 ) 117.628 * * [simplify]: iteration 7 : 1407 enodes (cost 19 ) 119.668 * * [simplify]: iteration done : 5000 enodes (cost 19 ) 119.669 * * [simplify]: iteration 0 : 7 enodes (cost 9 ) 119.670 * * [simplify]: iteration 1 : 15 enodes (cost 9 ) 119.672 * * [simplify]: iteration 2 : 28 enodes (cost 9 ) 119.675 * * [simplify]: iteration 3 : 46 enodes (cost 9 ) 119.681 * * [simplify]: iteration 4 : 76 enodes (cost 9 ) 119.695 * * [simplify]: iteration 5 : 148 enodes (cost 9 ) 119.756 * * [simplify]: iteration 6 : 398 enodes (cost 9 ) 120.237 * * [simplify]: iteration 7 : 1405 enodes (cost 9 ) 122.234 * * [simplify]: iteration done : 5000 enodes (cost 9 ) 122.234 * * [simplify]: iteration 0 : 8 enodes (cost 26 ) 122.235 * * [simplify]: iteration 1 : 17 enodes (cost 26 ) 122.238 * * [simplify]: iteration 2 : 31 enodes (cost 10 ) 122.242 * * [simplify]: iteration 3 : 51 enodes (cost 7 ) 122.248 * * [simplify]: iteration 4 : 83 enodes (cost 7 ) 122.269 * * [simplify]: iteration 5 : 161 enodes (cost 7 ) 122.333 * * [simplify]: iteration 6 : 416 enodes (cost 7 ) 122.862 * * [simplify]: iteration 7 : 1522 enodes (cost 7 ) 124.726 * * [simplify]: iteration done : 5000 enodes (cost 7 ) 124.726 * * [simplify]: iteration 0 : 7 enodes (cost 9 ) 124.727 * * [simplify]: iteration 1 : 15 enodes (cost 9 ) 124.729 * * [simplify]: iteration 2 : 28 enodes (cost 9 ) 124.734 * * [simplify]: iteration 3 : 46 enodes (cost 9 ) 124.739 * * [simplify]: iteration 4 : 76 enodes (cost 9 ) 124.753 * * [simplify]: iteration 5 : 148 enodes (cost 9 ) 124.814 * * [simplify]: iteration 6 : 398 enodes (cost 9 ) 125.300 * * [simplify]: iteration 7 : 1405 enodes (cost 9 ) 127.302 * * [simplify]: iteration done : 5000 enodes (cost 9 ) 127.303 * * [simplify]: iteration 0 : 7 enodes (cost 9 ) 127.304 * * [simplify]: iteration 1 : 15 enodes (cost 9 ) 127.305 * * [simplify]: iteration 2 : 28 enodes (cost 9 ) 127.309 * * [simplify]: iteration 3 : 46 enodes (cost 9 ) 127.314 * * [simplify]: iteration 4 : 76 enodes (cost 9 ) 127.332 * * [simplify]: iteration 5 : 148 enodes (cost 9 ) 127.393 * * [simplify]: iteration 6 : 398 enodes (cost 9 ) 127.877 * * [simplify]: iteration 7 : 1405 enodes (cost 9 ) 130.099 * * [simplify]: iteration done : 5000 enodes (cost 9 ) 130.100 * * [simplify]: iteration 0 : 7 enodes (cost 9 ) 130.101 * * [simplify]: iteration 1 : 15 enodes (cost 9 ) 130.103 * * [simplify]: iteration 2 : 28 enodes (cost 9 ) 130.106 * * [simplify]: iteration 3 : 46 enodes (cost 9 ) 130.111 * * [simplify]: iteration 4 : 76 enodes (cost 9 ) 130.124 * * [simplify]: iteration 5 : 148 enodes (cost 9 ) 130.185 * * [simplify]: iteration 6 : 398 enodes (cost 9 ) 130.675 * * [simplify]: iteration 7 : 1405 enodes (cost 9 ) 132.700 * * [simplify]: iteration done : 5000 enodes (cost 9 ) 132.701 * * [simplify]: iteration 0 : 7 enodes (cost 9 ) 132.702 * * [simplify]: iteration 1 : 15 enodes (cost 9 ) 132.704 * * [simplify]: iteration 2 : 28 enodes (cost 9 ) 132.708 * * [simplify]: iteration 3 : 46 enodes (cost 9 ) 132.713 * * [simplify]: iteration 4 : 76 enodes (cost 9 ) 132.727 * * [simplify]: iteration 5 : 148 enodes (cost 9 ) 132.793 * * [simplify]: iteration 6 : 398 enodes (cost 9 ) 133.275 * * [simplify]: iteration 7 : 1405 enodes (cost 9 ) 135.273 * * [simplify]: iteration done : 5000 enodes (cost 9 ) 135.273 * * [simplify]: iteration 0 : 8 enodes (cost 18 ) 135.274 * * [simplify]: iteration 1 : 16 enodes (cost 18 ) 135.282 * * [simplify]: iteration 2 : 29 enodes (cost 18 ) 135.286 * * [simplify]: iteration 3 : 47 enodes (cost 18 ) 135.291 * * [simplify]: iteration 4 : 77 enodes (cost 18 ) 135.304 * * [simplify]: iteration 5 : 145 enodes (cost 18 ) 135.365 * * [simplify]: iteration 6 : 395 enodes (cost 18 ) 135.876 * * [simplify]: iteration 7 : 1407 enodes (cost 18 ) 137.902 * * [simplify]: iteration done : 5000 enodes (cost 18 ) 137.902 * * [simplify]: iteration 0 : 7 enodes (cost 9 ) 137.903 * * [simplify]: iteration 1 : 15 enodes (cost 9 ) 137.905 * * [simplify]: iteration 2 : 28 enodes (cost 9 ) 137.909 * * [simplify]: iteration 3 : 46 enodes (cost 9 ) 137.914 * * [simplify]: iteration 4 : 76 enodes (cost 9 ) 137.933 * * [simplify]: iteration 5 : 148 enodes (cost 9 ) 137.992 * * [simplify]: iteration 6 : 398 enodes (cost 9 ) 138.463 * * [simplify]: iteration 7 : 1405 enodes (cost 9 ) 140.447 * * [simplify]: iteration done : 5000 enodes (cost 9 ) 140.448 * * [simplify]: iteration 0 : 7 enodes (cost 9 ) 140.449 * * [simplify]: iteration 1 : 15 enodes (cost 9 ) 140.451 * * [simplify]: iteration 2 : 28 enodes (cost 9 ) 140.455 * * [simplify]: iteration 3 : 46 enodes (cost 9 ) 140.460 * * [simplify]: iteration 4 : 76 enodes (cost 9 ) 140.473 * * [simplify]: iteration 5 : 148 enodes (cost 9 ) 140.533 * * [simplify]: iteration 6 : 398 enodes (cost 9 ) 141.004 * * [simplify]: iteration 7 : 1405 enodes (cost 9 ) 142.989 * * [simplify]: iteration done : 5000 enodes (cost 9 ) 142.990 * * [simplify]: iteration 0 : 7 enodes (cost 9 ) 142.991 * * [simplify]: iteration 1 : 15 enodes (cost 9 ) 142.993 * * [simplify]: iteration 2 : 28 enodes (cost 9 ) 142.996 * * [simplify]: iteration 3 : 46 enodes (cost 9 ) 143.001 * * [simplify]: iteration 4 : 76 enodes (cost 9 ) 143.015 * * [simplify]: iteration 5 : 148 enodes (cost 9 ) 143.079 * * [simplify]: iteration 6 : 398 enodes (cost 9 ) 143.553 * * [simplify]: iteration 7 : 1405 enodes (cost 9 ) 145.549 * * [simplify]: iteration done : 5000 enodes (cost 9 ) 145.550 * * [simplify]: iteration 0 : 2 enodes (cost 2 ) 145.550 * * [simplify]: iteration 1 : 4 enodes (cost 1 ) 145.550 * * [simplify]: iteration done : 4 enodes (cost 1 ) 145.551 * * [simplify]: iteration 0 : 6 enodes (cost 8 ) 145.552 * * [simplify]: iteration 1 : 14 enodes (cost 8 ) 145.559 * * [simplify]: iteration 2 : 27 enodes (cost 8 ) 145.562 * * [simplify]: iteration 3 : 45 enodes (cost 8 ) 145.568 * * [simplify]: iteration 4 : 75 enodes (cost 8 ) 145.582 * * [simplify]: iteration 5 : 145 enodes (cost 8 ) 145.641 * * [simplify]: iteration 6 : 388 enodes (cost 8 ) 146.144 * * [simplify]: iteration 7 : 1409 enodes (cost 8 ) 148.238 * * [simplify]: iteration done : 5000 enodes (cost 8 ) 148.239 * * [simplify]: iteration 0 : 2 enodes (cost 2 ) 148.239 * * [simplify]: iteration done : 2 enodes (cost 2 ) 148.239 * * [simplify]: iteration 0 : 4 enodes (cost 6 ) 148.240 * * [simplify]: iteration 1 : 8 enodes (cost 6 ) 148.241 * * [simplify]: iteration 2 : 12 enodes (cost 6 ) 148.242 * * [simplify]: iteration 3 : 18 enodes (cost 6 ) 148.245 * * [simplify]: iteration done : 18 enodes (cost 6 ) 148.245 * * [simplify]: iteration 0 : 2 enodes (cost 2 ) 148.245 * * [simplify]: iteration done : 2 enodes (cost 2 ) 148.246 * * [simplify]: iteration 0 : 4 enodes (cost 6 ) 148.247 * * [simplify]: iteration 1 : 8 enodes (cost 6 ) 148.247 * * [simplify]: iteration 2 : 12 enodes (cost 6 ) 148.249 * * [simplify]: iteration 3 : 18 enodes (cost 6 ) 148.251 * * [simplify]: iteration done : 18 enodes (cost 6 ) 148.251 * * [simplify]: iteration 0 : 4 enodes (cost 4 ) 148.252 * * [simplify]: iteration 1 : 7 enodes (cost 4 ) 148.252 * * [simplify]: iteration done : 7 enodes (cost 4 ) 148.253 * * [simplify]: iteration 0 : 3 enodes (cost 4 ) 148.253 * * [simplify]: iteration done : 3 enodes (cost 4 ) 148.254 * * [simplify]: iteration 0 : 8 enodes (cost 12 ) 148.255 * * [simplify]: iteration 1 : 26 enodes (cost 12 ) 148.261 * * [simplify]: iteration 2 : 91 enodes (cost 10 ) 148.299 * * [simplify]: iteration 3 : 292 enodes (cost 10 ) 148.569 * * [simplify]: iteration 4 : 1121 enodes (cost 10 ) 150.822 * * [simplify]: iteration done : 5000 enodes (cost 10 ) 150.823 * * [simplify]: iteration 0 : 10 enodes (cost 24 ) 150.825 * * [simplify]: iteration 1 : 32 enodes (cost 16 ) 150.831 * * [simplify]: iteration 2 : 95 enodes (cost 14 ) 150.861 * * [simplify]: iteration 3 : 313 enodes (cost 12 ) 151.074 * * [simplify]: iteration 4 : 1090 enodes (cost 12 ) 152.783 * * [simplify]: iteration 5 : 4690 enodes (cost 12 ) 154.771 * * [simplify]: iteration done : 5000 enodes (cost 12 ) 154.772 * * [simplify]: iteration 0 : 8 enodes (cost 16 ) 154.773 * * [simplify]: iteration 1 : 25 enodes (cost 10 ) 154.778 * * [simplify]: iteration 2 : 74 enodes (cost 8 ) 154.793 * * [simplify]: iteration 3 : 211 enodes (cost 8 ) 154.896 * * [simplify]: iteration 4 : 688 enodes (cost 8 ) 155.665 * * [simplify]: iteration 5 : 2881 enodes (cost 8 ) 157.511 * * [simplify]: iteration done : 5000 enodes (cost 8 ) 157.512 * * [simplify]: iteration 0 : 6 enodes (cost 8 ) 157.513 * * [simplify]: iteration 1 : 15 enodes (cost 8 ) 157.515 * * [simplify]: iteration 2 : 30 enodes (cost 8 ) 157.518 * * [simplify]: iteration 3 : 47 enodes (cost 8 ) 157.525 * * [simplify]: iteration 4 : 86 enodes (cost 8 ) 157.540 * * [simplify]: iteration 5 : 200 enodes (cost 8 ) 157.619 * * [simplify]: iteration 6 : 634 enodes (cost 8 ) 158.407 * * [simplify]: iteration 7 : 2555 enodes (cost 8 ) 160.566 * * [simplify]: iteration done : 5001 enodes (cost 8 ) 160.567 * * [simplify]: iteration 0 : 8 enodes (cost 19 ) 160.568 * * [simplify]: iteration 1 : 16 enodes (cost 19 ) 160.570 * * [simplify]: iteration 2 : 29 enodes (cost 19 ) 160.574 * * [simplify]: iteration 3 : 47 enodes (cost 19 ) 160.579 * * [simplify]: iteration 4 : 77 enodes (cost 19 ) 160.592 * * [simplify]: iteration 5 : 145 enodes (cost 19 ) 160.656 * * [simplify]: iteration 6 : 395 enodes (cost 19 ) 161.169 * * [simplify]: iteration 7 : 1407 enodes (cost 19 ) 163.209 * * [simplify]: iteration done : 5000 enodes (cost 19 ) 163.210 * * [simplify]: iteration 0 : 7 enodes (cost 9 ) 163.211 * * [simplify]: iteration 1 : 15 enodes (cost 9 ) 163.212 * * [simplify]: iteration 2 : 28 enodes (cost 9 ) 163.216 * * [simplify]: iteration 3 : 46 enodes (cost 9 ) 163.221 * * [simplify]: iteration 4 : 76 enodes (cost 9 ) 163.235 * * [simplify]: iteration 5 : 148 enodes (cost 9 ) 163.295 * * [simplify]: iteration 6 : 398 enodes (cost 9 ) 163.777 * * [simplify]: iteration 7 : 1405 enodes (cost 9 ) 165.771 * * [simplify]: iteration done : 5000 enodes (cost 9 ) 165.771 * * [simplify]: iteration 0 : 8 enodes (cost 26 ) 165.773 * * [simplify]: iteration 1 : 17 enodes (cost 26 ) 165.775 * * [simplify]: iteration 2 : 31 enodes (cost 10 ) 165.779 * * [simplify]: iteration 3 : 51 enodes (cost 7 ) 165.785 * * [simplify]: iteration 4 : 83 enodes (cost 7 ) 165.807 * * [simplify]: iteration 5 : 161 enodes (cost 7 ) 165.869 * * [simplify]: iteration 6 : 416 enodes (cost 7 ) 166.398 * * [simplify]: iteration 7 : 1522 enodes (cost 7 ) 168.248 * * [simplify]: iteration done : 5000 enodes (cost 7 ) 168.249 * * [simplify]: iteration 0 : 7 enodes (cost 9 ) 168.250 * * [simplify]: iteration 1 : 15 enodes (cost 9 ) 168.252 * * [simplify]: iteration 2 : 28 enodes (cost 9 ) 168.256 * * [simplify]: iteration 3 : 46 enodes (cost 9 ) 168.261 * * [simplify]: iteration 4 : 76 enodes (cost 9 ) 168.274 * * [simplify]: iteration 5 : 148 enodes (cost 9 ) 168.335 * * [simplify]: iteration 6 : 398 enodes (cost 9 ) 168.817 * * [simplify]: iteration 7 : 1405 enodes (cost 9 ) 170.813 * * [simplify]: iteration done : 5000 enodes (cost 9 ) 170.814 * * [simplify]: iteration 0 : 7 enodes (cost 9 ) 170.814 * * [simplify]: iteration 1 : 15 enodes (cost 9 ) 170.817 * * [simplify]: iteration 2 : 28 enodes (cost 9 ) 170.820 * * [simplify]: iteration 3 : 46 enodes (cost 9 ) 170.826 * * [simplify]: iteration 4 : 76 enodes (cost 9 ) 170.844 * * [simplify]: iteration 5 : 148 enodes (cost 9 ) 170.905 * * [simplify]: iteration 6 : 398 enodes (cost 9 ) 171.378 * * [simplify]: iteration 7 : 1405 enodes (cost 9 ) 173.380 * * [simplify]: iteration done : 5000 enodes (cost 9 ) 173.381 * * [simplify]: iteration 0 : 2 enodes (cost 3 ) 173.381 * * [simplify]: iteration 1 : 5 enodes (cost 1 ) 173.381 * * [simplify]: iteration done : 5 enodes (cost 1 ) 173.382 * * [simplify]: iteration 0 : 2 enodes (cost 3 ) 173.382 * * [simplify]: iteration 1 : 6 enodes (cost 1 ) 173.383 * * [simplify]: iteration done : 6 enodes (cost 1 ) 173.383 * * [simplify]: iteration 0 : 6 enodes (cost 15 ) 173.384 * * [simplify]: iteration 1 : 20 enodes (cost 15 ) 173.388 * * [simplify]: iteration 2 : 58 enodes (cost 15 ) 173.403 * * [simplify]: iteration 3 : 171 enodes (cost 13 ) 173.478 * * [simplify]: iteration 4 : 534 enodes (cost 11 ) 174.249 * * [simplify]: iteration 5 : 2197 enodes (cost 11 ) 176.064 * * [simplify]: iteration done : 5000 enodes (cost 11 ) 176.065 * * [simplify]: iteration 0 : 7 enodes (cost 17 ) 176.066 * * [simplify]: iteration 1 : 15 enodes (cost 17 ) 176.068 * * [simplify]: iteration 2 : 28 enodes (cost 17 ) 176.071 * * [simplify]: iteration 3 : 46 enodes (cost 17 ) 176.081 * * [simplify]: iteration 4 : 76 enodes (cost 17 ) 176.094 * * [simplify]: iteration 5 : 148 enodes (cost 17 ) 176.153 * * [simplify]: iteration 6 : 398 enodes (cost 17 ) 176.614 * * [simplify]: iteration 7 : 1405 enodes (cost 17 ) 178.788 * * [simplify]: iteration done : 5000 enodes (cost 17 ) 178.789 * * [simplify]: iteration 0 : 2 enodes (cost 3 ) 178.789 * * [simplify]: iteration 1 : 6 enodes (cost 1 ) 178.790 * * [simplify]: iteration done : 6 enodes (cost 1 ) 178.790 * * [simplify]: iteration 0 : 8 enodes (cost 19 ) 178.791 * * [simplify]: iteration 1 : 17 enodes (cost 11 ) 178.793 * * [simplify]: iteration 2 : 31 enodes (cost 11 ) 178.797 * * [simplify]: iteration 3 : 49 enodes (cost 11 ) 178.803 * * [simplify]: iteration 4 : 79 enodes (cost 11 ) 178.816 * * [simplify]: iteration 5 : 149 enodes (cost 11 ) 178.874 * * [simplify]: iteration 6 : 391 enodes (cost 11 ) 179.369 * * [simplify]: iteration 7 : 1389 enodes (cost 11 ) 181.275 * * [simplify]: iteration done : 5000 enodes (cost 11 ) 181.276 * * [simplify]: iteration 0 : 8 enodes (cost 18 ) 181.277 * * [simplify]: iteration 1 : 18 enodes (cost 18 ) 181.279 * * [simplify]: iteration 2 : 32 enodes (cost 11 ) 181.283 * * [simplify]: iteration 3 : 51 enodes (cost 11 ) 181.289 * * [simplify]: iteration 4 : 81 enodes (cost 11 ) 181.306 * * [simplify]: iteration 5 : 149 enodes (cost 11 ) 181.364 * * [simplify]: iteration 6 : 387 enodes (cost 11 ) 181.878 * * [simplify]: iteration 7 : 1408 enodes (cost 11 ) 183.913 * * [simplify]: iteration done : 5000 enodes (cost 11 ) 183.914 * * [simplify]: iteration 0 : 8 enodes (cost 18 ) 183.915 * * [simplify]: iteration 1 : 18 enodes (cost 18 ) 183.918 * * [simplify]: iteration 2 : 34 enodes (cost 18 ) 183.922 * * [simplify]: iteration 3 : 57 enodes (cost 18 ) 183.935 * * [simplify]: iteration 4 : 105 enodes (cost 18 ) 183.954 * * [simplify]: iteration 5 : 212 enodes (cost 18 ) 184.035 * * [simplify]: iteration 6 : 541 enodes (cost 18 ) 184.621 * * [simplify]: iteration 7 : 1913 enodes (cost 18 ) 186.147 * * [simplify]: iteration done : 5000 enodes (cost 18 ) 186.147 * * [simplify]: iteration 0 : 6 enodes (cost 15 ) 186.148 * * [simplify]: iteration 1 : 20 enodes (cost 15 ) 186.152 * * [simplify]: iteration 2 : 58 enodes (cost 15 ) 186.166 * * [simplify]: iteration 3 : 171 enodes (cost 13 ) 186.240 * * [simplify]: iteration 4 : 534 enodes (cost 11 ) 186.980 * * [simplify]: iteration 5 : 2197 enodes (cost 11 ) 188.760 * * [simplify]: iteration done : 5000 enodes (cost 11 ) 188.760 * * [simplify]: iteration 0 : 9 enodes (cost 37 ) 188.762 * * [simplify]: iteration 1 : 17 enodes (cost 37 ) 188.764 * * [simplify]: iteration 2 : 30 enodes (cost 37 ) 188.767 * * [simplify]: iteration 3 : 48 enodes (cost 37 ) 188.777 * * [simplify]: iteration 4 : 78 enodes (cost 37 ) 188.790 * * [simplify]: iteration 5 : 150 enodes (cost 37 ) 188.848 * * [simplify]: iteration 6 : 392 enodes (cost 37 ) 189.338 * * [simplify]: iteration 7 : 1410 enodes (cost 37 ) 191.232 * * [simplify]: iteration done : 5000 enodes (cost 37 ) 191.232 * * [simplify]: iteration 0 : 8 enodes (cost 18 ) 191.233 * * [simplify]: iteration 1 : 16 enodes (cost 18 ) 191.235 * * [simplify]: iteration 2 : 29 enodes (cost 18 ) 191.239 * * [simplify]: iteration 3 : 47 enodes (cost 18 ) 191.244 * * [simplify]: iteration 4 : 77 enodes (cost 18 ) 191.263 * * [simplify]: iteration 5 : 145 enodes (cost 18 ) 191.322 * * [simplify]: iteration 6 : 395 enodes (cost 18 ) 191.817 * * [simplify]: iteration 7 : 1407 enodes (cost 18 ) 193.782 * * [simplify]: iteration done : 5000 enodes (cost 18 ) 193.783 * * [simplify]: iteration 0 : 9 enodes (cost 53 ) 193.785 * * [simplify]: iteration 1 : 25 enodes (cost 53 ) 193.788 * * [simplify]: iteration 2 : 44 enodes (cost 19 ) 193.795 * * [simplify]: iteration 3 : 72 enodes (cost 10 ) 193.810 * * [simplify]: iteration 4 : 202 enodes (cost 10 ) 193.915 * * [simplify]: iteration 5 : 698 enodes (cost 10 ) 194.754 * * [simplify]: iteration 6 : 2718 enodes (cost 10 ) 195.978 * * [simplify]: iteration done : 5000 enodes (cost 10 ) 195.978 * * [simplify]: iteration 0 : 8 enodes (cost 18 ) 195.983 * * [simplify]: iteration 1 : 17 enodes (cost 9 ) 195.985 * * [simplify]: iteration 2 : 30 enodes (cost 9 ) 195.989 * * [simplify]: iteration 3 : 48 enodes (cost 9 ) 195.994 * * [simplify]: iteration 4 : 78 enodes (cost 9 ) 196.008 * * [simplify]: iteration 5 : 150 enodes (cost 9 ) 196.068 * * [simplify]: iteration 6 : 394 enodes (cost 9 ) 196.549 * * [simplify]: iteration 7 : 1403 enodes (cost 9 ) 198.615 * * [simplify]: iteration done : 5000 enodes (cost 9 ) 198.616 * * [simplify]: iteration 0 : 8 enodes (cost 18 ) 198.617 * * [simplify]: iteration 1 : 17 enodes (cost 9 ) 198.619 * * [simplify]: iteration 2 : 30 enodes (cost 9 ) 198.623 * * [simplify]: iteration 3 : 48 enodes (cost 9 ) 198.629 * * [simplify]: iteration 4 : 78 enodes (cost 9 ) 198.642 * * [simplify]: iteration 5 : 150 enodes (cost 9 ) 198.701 * * [simplify]: iteration 6 : 394 enodes (cost 9 ) 199.188 * * [simplify]: iteration 7 : 1403 enodes (cost 9 ) 201.467 * * [simplify]: iteration done : 5000 enodes (cost 9 ) 201.468 * * [simplify]: iteration 0 : 9 enodes (cost 25 ) 201.469 * * [simplify]: iteration 1 : 27 enodes (cost 25 ) 201.476 * * [simplify]: iteration 2 : 92 enodes (cost 21 ) 201.514 * * [simplify]: iteration 3 : 295 enodes (cost 21 ) 201.772 * * [simplify]: iteration 4 : 1124 enodes (cost 21 ) 204.041 * * [simplify]: iteration done : 5001 enodes (cost 21 ) 204.042 * * [simplify]: iteration 0 : 11 enodes (cost 49 ) 204.044 * * [simplify]: iteration 1 : 33 enodes (cost 33 ) 204.050 * * [simplify]: iteration 2 : 96 enodes (cost 29 ) 204.082 * * [simplify]: iteration 3 : 314 enodes (cost 25 ) 204.294 * * [simplify]: iteration 4 : 1085 enodes (cost 25 ) 206.037 * * [simplify]: iteration 5 : 4700 enodes (cost 25 ) 207.776 * * [simplify]: iteration done : 5000 enodes (cost 25 ) 207.777 * * [simplify]: iteration 0 : 13 enodes (cost 29 ) 207.779 * * [simplify]: iteration 1 : 40 enodes (cost 21 ) 207.788 * * [simplify]: iteration 2 : 138 enodes (cost 19 ) 207.851 * * [simplify]: iteration 3 : 471 enodes (cost 19 ) 208.278 * * [simplify]: iteration 4 : 1789 enodes (cost 19 ) 209.716 * * [simplify]: iteration done : 5000 enodes (cost 19 ) 209.717 * * [simplify]: iteration 0 : 13 enodes (cost 33 ) 209.719 * * [simplify]: iteration 1 : 38 enodes (cost 25 ) 209.726 * * [simplify]: iteration 2 : 108 enodes (cost 23 ) 209.761 * * [simplify]: iteration 3 : 330 enodes (cost 21 ) 209.975 * * [simplify]: iteration 4 : 1112 enodes (cost 21 ) 211.651 * * [simplify]: iteration 5 : 4850 enodes (cost 21 ) 213.350 * * [simplify]: iteration done : 5000 enodes (cost 21 ) 213.351 * * [simplify]: iteration 0 : 13 enodes (cost 29 ) 213.353 * * [simplify]: iteration 1 : 40 enodes (cost 21 ) 213.362 * * [simplify]: iteration 2 : 138 enodes (cost 19 ) 213.419 * * [simplify]: iteration 3 : 476 enodes (cost 19 ) 213.856 * * [simplify]: iteration 4 : 1830 enodes (cost 19 ) 215.291 * * [simplify]: iteration done : 5001 enodes (cost 19 ) 215.292 * * [simplify]: iteration 0 : 13 enodes (cost 33 ) 215.294 * * [simplify]: iteration 1 : 38 enodes (cost 25 ) 215.301 * * [simplify]: iteration 2 : 108 enodes (cost 23 ) 215.334 * * [simplify]: iteration 3 : 330 enodes (cost 21 ) 215.544 * * [simplify]: iteration 4 : 1114 enodes (cost 21 ) 217.232 * * [simplify]: iteration 5 : 4840 enodes (cost 21 ) 218.891 * * [simplify]: iteration done : 5000 enodes (cost 21 ) 218.892 * * [simplify]: iteration 0 : 9 enodes (cost 33 ) 218.893 * * [simplify]: iteration 1 : 26 enodes (cost 21 ) 218.898 * * [simplify]: iteration 2 : 75 enodes (cost 17 ) 218.914 * * [simplify]: iteration 3 : 212 enodes (cost 17 ) 219.014 * * [simplify]: iteration 4 : 701 enodes (cost 17 ) 219.972 * * [simplify]: iteration 5 : 2901 enodes (cost 17 ) 221.555 * * [simplify]: iteration done : 5000 enodes (cost 17 ) 221.556 * * [simplify]: iteration 0 : 7 enodes (cost 17 ) 221.562 * * [simplify]: iteration 1 : 16 enodes (cost 17 ) 221.564 * * [simplify]: iteration 2 : 31 enodes (cost 17 ) 221.568 * * [simplify]: iteration 3 : 48 enodes (cost 17 ) 221.581 * * [simplify]: iteration 4 : 87 enodes (cost 17 ) 221.596 * * [simplify]: iteration 5 : 197 enodes (cost 17 ) 221.672 * * [simplify]: iteration 6 : 636 enodes (cost 17 ) 222.471 * * [simplify]: iteration 7 : 2554 enodes (cost 17 ) 224.347 * * [simplify]: iteration done : 5000 enodes (cost 17 ) 224.347 * * [simplify]: iteration 0 : 9 enodes (cost 37 ) 224.349 * * [simplify]: iteration 1 : 17 enodes (cost 37 ) 224.356 * * [simplify]: iteration 2 : 30 enodes (cost 37 ) 224.359 * * [simplify]: iteration 3 : 48 enodes (cost 37 ) 224.365 * * [simplify]: iteration 4 : 78 enodes (cost 37 ) 224.379 * * [simplify]: iteration 5 : 150 enodes (cost 37 ) 224.438 * * [simplify]: iteration 6 : 392 enodes (cost 37 ) 224.935 * * [simplify]: iteration 7 : 1410 enodes (cost 37 ) 226.841 * * [simplify]: iteration done : 5000 enodes (cost 37 ) 226.842 * * [simplify]: iteration 0 : 8 enodes (cost 19 ) 226.843 * * [simplify]: iteration 1 : 16 enodes (cost 19 ) 226.845 * * [simplify]: iteration 2 : 29 enodes (cost 19 ) 226.855 * * [simplify]: iteration 3 : 47 enodes (cost 19 ) 226.860 * * [simplify]: iteration 4 : 77 enodes (cost 19 ) 226.873 * * [simplify]: iteration 5 : 145 enodes (cost 19 ) 226.934 * * [simplify]: iteration 6 : 395 enodes (cost 19 ) 227.433 * * [simplify]: iteration 7 : 1407 enodes (cost 19 ) 229.412 * * [simplify]: iteration done : 5000 enodes (cost 19 ) 229.412 * * [simplify]: iteration 0 : 8 enodes (cost 19 ) 229.413 * * [simplify]: iteration 1 : 16 enodes (cost 19 ) 229.415 * * [simplify]: iteration 2 : 29 enodes (cost 19 ) 229.419 * * [simplify]: iteration 3 : 47 enodes (cost 19 ) 229.424 * * [simplify]: iteration 4 : 77 enodes (cost 19 ) 229.444 * * [simplify]: iteration 5 : 145 enodes (cost 19 ) 229.504 * * [simplify]: iteration 6 : 395 enodes (cost 19 ) 230.005 * * [simplify]: iteration 7 : 1407 enodes (cost 19 ) 231.994 * * [simplify]: iteration done : 5000 enodes (cost 19 ) 231.995 * * [simplify]: iteration 0 : 8 enodes (cost 19 ) 231.996 * * [simplify]: iteration 1 : 16 enodes (cost 19 ) 231.998 * * [simplify]: iteration 2 : 29 enodes (cost 19 ) 232.001 * * [simplify]: iteration 3 : 47 enodes (cost 19 ) 232.006 * * [simplify]: iteration 4 : 77 enodes (cost 19 ) 232.020 * * [simplify]: iteration 5 : 145 enodes (cost 19 ) 232.079 * * [simplify]: iteration 6 : 395 enodes (cost 19 ) 232.579 * * [simplify]: iteration 7 : 1407 enodes (cost 19 ) 234.567 * * [simplify]: iteration done : 5000 enodes (cost 19 ) 234.568 * * [simplify]: iteration 0 : 3 enodes (cost 5 ) 234.568 * * [simplify]: iteration 1 : 5 enodes (cost 3 ) 234.569 * * [simplify]: iteration done : 5 enodes (cost 1 ) 234.569 * * [simplify]: iteration 0 : 7 enodes (cost 17 ) 234.570 * * [simplify]: iteration 1 : 15 enodes (cost 17 ) 234.572 * * [simplify]: iteration 2 : 28 enodes (cost 17 ) 234.576 * * [simplify]: iteration 3 : 46 enodes (cost 17 ) 234.581 * * [simplify]: iteration 4 : 76 enodes (cost 17 ) 234.595 * * [simplify]: iteration 5 : 148 enodes (cost 17 ) 234.655 * * [simplify]: iteration 6 : 398 enodes (cost 17 ) 235.124 * * [simplify]: iteration 7 : 1405 enodes (cost 17 ) 237.098 * * [simplify]: iteration done : 5000 enodes (cost 17 ) 237.098 * * [simplify]: iteration 0 : 3 enodes (cost 5 ) 237.099 * * [simplify]: iteration done : 3 enodes (cost 5 ) 237.099 * * [simplify]: iteration 0 : 5 enodes (cost 13 ) 237.100 * * [simplify]: iteration 1 : 9 enodes (cost 13 ) 237.101 * * [simplify]: iteration 2 : 13 enodes (cost 13 ) 237.102 * * [simplify]: iteration 3 : 19 enodes (cost 13 ) 237.105 * * [simplify]: iteration done : 19 enodes (cost 13 ) 237.105 * * [simplify]: iteration 0 : 3 enodes (cost 5 ) 237.106 * * [simplify]: iteration done : 3 enodes (cost 5 ) 237.106 * * [simplify]: iteration 0 : 5 enodes (cost 13 ) 237.107 * * [simplify]: iteration 1 : 9 enodes (cost 13 ) 237.108 * * [simplify]: iteration 2 : 13 enodes (cost 13 ) 237.109 * * [simplify]: iteration 3 : 19 enodes (cost 13 ) 237.112 * * [simplify]: iteration done : 19 enodes (cost 13 ) 237.112 * * [simplify]: iteration 0 : 3 enodes (cost 5 ) 237.113 * * [simplify]: iteration done : 3 enodes (cost 5 ) 237.113 * * [simplify]: iteration 0 : 5 enodes (cost 13 ) 237.114 * * [simplify]: iteration 1 : 9 enodes (cost 13 ) 237.115 * * [simplify]: iteration 2 : 13 enodes (cost 13 ) 237.116 * * [simplify]: iteration 3 : 19 enodes (cost 13 ) 237.119 * * [simplify]: iteration done : 19 enodes (cost 13 ) 237.119 * * [simplify]: iteration 0 : 3 enodes (cost 5 ) 237.120 * * [simplify]: iteration done : 3 enodes (cost 5 ) 237.120 * * [simplify]: iteration 0 : 5 enodes (cost 13 ) 237.121 * * [simplify]: iteration 1 : 9 enodes (cost 13 ) 237.122 * * [simplify]: iteration 2 : 13 enodes (cost 13 ) 237.128 * * [simplify]: iteration 3 : 19 enodes (cost 13 ) 237.130 * * [simplify]: iteration done : 19 enodes (cost 13 ) 237.131 * * [simplify]: iteration 0 : 5 enodes (cost 9 ) 237.132 * * [simplify]: iteration 1 : 8 enodes (cost 9 ) 237.133 * * [simplify]: iteration done : 8 enodes (cost 9 ) 237.133 * * [simplify]: iteration 0 : 4 enodes (cost 9 ) 237.134 * * [simplify]: iteration done : 4 enodes (cost 9 ) 237.134 * * [simplify]: iteration 0 : 9 enodes (cost 39 ) 237.136 * * [simplify]: iteration 1 : 21 enodes (cost 39 ) 237.139 * * [simplify]: iteration 2 : 35 enodes (cost 21 ) 237.143 * * [simplify]: iteration 3 : 58 enodes (cost 11 ) 237.150 * * [simplify]: iteration 4 : 97 enodes (cost 11 ) 237.167 * * [simplify]: iteration 5 : 189 enodes (cost 11 ) 237.240 * * [simplify]: iteration 6 : 504 enodes (cost 11 ) 237.748 * * [simplify]: iteration 7 : 1698 enodes (cost 11 ) 239.443 * * [simplify]: iteration done : 5000 enodes (cost 11 ) 239.444 * * [simplify]: iteration 0 : 8 enodes (cost 19 ) 239.445 * * [simplify]: iteration 1 : 16 enodes (cost 19 ) 239.447 * * [simplify]: iteration 2 : 29 enodes (cost 19 ) 239.450 * * [simplify]: iteration 3 : 47 enodes (cost 19 ) 239.456 * * [simplify]: iteration 4 : 77 enodes (cost 19 ) 239.475 * * [simplify]: iteration 5 : 145 enodes (cost 19 ) 239.535 * * [simplify]: iteration 6 : 395 enodes (cost 19 ) 240.027 * * [simplify]: iteration 7 : 1407 enodes (cost 19 ) 242.003 * * [simplify]: iteration done : 5000 enodes (cost 19 ) 242.004 * * [simplify]: iteration 0 : 8 enodes (cost 19 ) 242.005 * * [simplify]: iteration 1 : 16 enodes (cost 8 ) 242.007 * * [simplify]: iteration 2 : 30 enodes (cost 8 ) 242.010 * * [simplify]: iteration 3 : 48 enodes (cost 8 ) 242.015 * * [simplify]: iteration 4 : 78 enodes (cost 8 ) 242.029 * * [simplify]: iteration 5 : 150 enodes (cost 8 ) 242.092 * * [simplify]: iteration 6 : 394 enodes (cost 8 ) 242.567 * * [simplify]: iteration 7 : 1404 enodes (cost 8 ) 244.937 * * [simplify]: iteration done : 5000 enodes (cost 8 ) 244.938 * * [simplify]: iteration 0 : 8 enodes (cost 19 ) 244.939 * * [simplify]: iteration 1 : 16 enodes (cost 8 ) 244.941 * * [simplify]: iteration 2 : 30 enodes (cost 8 ) 244.944 * * [simplify]: iteration 3 : 48 enodes (cost 8 ) 244.955 * * [simplify]: iteration 4 : 78 enodes (cost 8 ) 244.968 * * [simplify]: iteration 5 : 150 enodes (cost 8 ) 245.026 * * [simplify]: iteration 6 : 394 enodes (cost 8 ) 245.509 * * [simplify]: iteration 7 : 1404 enodes (cost 8 ) 247.646 * * [simplify]: iteration done : 5000 enodes (cost 8 ) 247.646 * * [simplify]: iteration 0 : 2 enodes (cost 3 ) 247.647 * * [simplify]: iteration 1 : 4 enodes (cost 1 ) 247.647 * * [simplify]: iteration done : 4 enodes (cost 1 ) 247.648 * * [simplify]: iteration 0 : 7 enodes (cost 17 ) 247.649 * * [simplify]: iteration 1 : 15 enodes (cost 17 ) 247.651 * * [simplify]: iteration 2 : 28 enodes (cost 17 ) 247.655 * * [simplify]: iteration 3 : 46 enodes (cost 17 ) 247.660 * * [simplify]: iteration 4 : 76 enodes (cost 17 ) 247.673 * * [simplify]: iteration 5 : 148 enodes (cost 17 ) 247.732 * * [simplify]: iteration 6 : 398 enodes (cost 17 ) 248.207 * * [simplify]: iteration 7 : 1405 enodes (cost 17 ) 250.156 * * [simplify]: iteration done : 5000 enodes (cost 17 ) 250.157 * * [simplify]: iteration 0 : 8 enodes (cost 19 ) 250.158 * * [simplify]: iteration 1 : 16 enodes (cost 19 ) 250.160 * * [simplify]: iteration 2 : 29 enodes (cost 19 ) 250.163 * * [simplify]: iteration 3 : 47 enodes (cost 19 ) 250.169 * * [simplify]: iteration 4 : 77 enodes (cost 19 ) 250.187 * * [simplify]: iteration 5 : 145 enodes (cost 19 ) 250.246 * * [simplify]: iteration 6 : 395 enodes (cost 19 ) 250.741 * * [simplify]: iteration 7 : 1407 enodes (cost 19 ) 252.724 * * [simplify]: iteration done : 5000 enodes (cost 19 ) 252.725 * * [simplify]: iteration 0 : 8 enodes (cost 19 ) 252.726 * * [simplify]: iteration 1 : 16 enodes (cost 19 ) 252.728 * * [simplify]: iteration 2 : 29 enodes (cost 19 ) 252.732 * * [simplify]: iteration 3 : 47 enodes (cost 19 ) 252.737 * * [simplify]: iteration 4 : 77 enodes (cost 19 ) 252.751 * * [simplify]: iteration 5 : 145 enodes (cost 19 ) 252.813 * * [simplify]: iteration 6 : 395 enodes (cost 19 ) 253.311 * * [simplify]: iteration 7 : 1407 enodes (cost 19 ) 255.303 * * [simplify]: iteration done : 5000 enodes (cost 19 ) 255.304 * * [simplify]: iteration 0 : 10 enodes (cost 19 ) 255.305 * * [simplify]: iteration 1 : 19 enodes (cost 19 ) 255.308 * * [simplify]: iteration 2 : 32 enodes (cost 19 ) 255.311 * * [simplify]: iteration 3 : 50 enodes (cost 19 ) 255.317 * * [simplify]: iteration 4 : 80 enodes (cost 19 ) 255.331 * * [simplify]: iteration 5 : 150 enodes (cost 19 ) 255.391 * * [simplify]: iteration 6 : 397 enodes (cost 19 ) 255.889 * * [simplify]: iteration 7 : 1406 enodes (cost 19 ) 257.781 * * [simplify]: iteration done : 5000 enodes (cost 19 ) 257.782 * * [simplify]: iteration 0 : 10 enodes (cost 19 ) 257.788 * * [simplify]: iteration 1 : 19 enodes (cost 19 ) 257.791 * * [simplify]: iteration 2 : 32 enodes (cost 19 ) 257.794 * * [simplify]: iteration 3 : 50 enodes (cost 19 ) 257.800 * * [simplify]: iteration 4 : 80 enodes (cost 19 ) 257.814 * * [simplify]: iteration 5 : 150 enodes (cost 19 ) 257.874 * * [simplify]: iteration 6 : 397 enodes (cost 19 ) 258.367 * * [simplify]: iteration 7 : 1406 enodes (cost 19 ) 260.269 * * [simplify]: iteration done : 5000 enodes (cost 19 ) 260.270 * * [simplify]: iteration 0 : 10 enodes (cost 19 ) 260.271 * * [simplify]: iteration 1 : 19 enodes (cost 19 ) 260.274 * * [simplify]: iteration 2 : 32 enodes (cost 19 ) 260.277 * * [simplify]: iteration 3 : 50 enodes (cost 19 ) 260.283 * * [simplify]: iteration 4 : 80 enodes (cost 19 ) 260.297 * * [simplify]: iteration 5 : 150 enodes (cost 19 ) 260.357 * * [simplify]: iteration 6 : 397 enodes (cost 19 ) 260.847 * * [simplify]: iteration 7 : 1406 enodes (cost 19 ) 262.741 * * [simplify]: iteration done : 5000 enodes (cost 19 ) 262.742 * * [simplify]: iteration 0 : 10 enodes (cost 19 ) 262.743 * * [simplify]: iteration 1 : 19 enodes (cost 19 ) 262.746 * * [simplify]: iteration 2 : 32 enodes (cost 19 ) 262.749 * * [simplify]: iteration 3 : 50 enodes (cost 19 ) 262.755 * * [simplify]: iteration 4 : 80 enodes (cost 19 ) 262.768 * * [simplify]: iteration 5 : 150 enodes (cost 19 ) 262.828 * * [simplify]: iteration 6 : 397 enodes (cost 19 ) 263.314 * * [simplify]: iteration 7 : 1406 enodes (cost 19 ) 265.204 * * [simplify]: iteration done : 5000 enodes (cost 19 ) 265.205 * * [simplify]: iteration 0 : 8 enodes (cost 19 ) 265.206 * * [simplify]: iteration 1 : 16 enodes (cost 8 ) 265.208 * * [simplify]: iteration 2 : 30 enodes (cost 8 ) 265.211 * * [simplify]: iteration 3 : 48 enodes (cost 8 ) 265.216 * * [simplify]: iteration 4 : 78 enodes (cost 8 ) 265.229 * * [simplify]: iteration 5 : 150 enodes (cost 8 ) 265.288 * * [simplify]: iteration 6 : 394 enodes (cost 8 ) 265.769 * * [simplify]: iteration 7 : 1404 enodes (cost 8 ) 267.912 * * [simplify]: iteration done : 5000 enodes (cost 8 ) 267.913 * * [simplify]: iteration 0 : 8 enodes (cost 19 ) 267.914 * * [simplify]: iteration 1 : 16 enodes (cost 8 ) 267.916 * * [simplify]: iteration 2 : 30 enodes (cost 8 ) 267.920 * * [simplify]: iteration 3 : 48 enodes (cost 8 ) 267.925 * * [simplify]: iteration 4 : 78 enodes (cost 8 ) 267.944 * * [simplify]: iteration 5 : 150 enodes (cost 8 ) 268.003 * * [simplify]: iteration 6 : 394 enodes (cost 8 ) 268.488 * * [simplify]: iteration 7 : 1404 enodes (cost 8 ) 270.859 * * [simplify]: iteration done : 5000 enodes (cost 8 ) 270.859 * * [simplify]: iteration 0 : 3 enodes (cost 3 ) 270.860 * * [simplify]: iteration 1 : 5 enodes (cost 1 ) 270.860 * * [simplify]: iteration done : 5 enodes (cost 1 ) 270.861 * * [simplify]: iteration 0 : 3 enodes (cost 3 ) 270.861 * * [simplify]: iteration 1 : 6 enodes (cost 1 ) 270.861 * * [simplify]: iteration done : 6 enodes (cost 1 ) 270.862 * * [simplify]: iteration 0 : 9 enodes (cost 27 ) 270.863 * * [simplify]: iteration 1 : 18 enodes (cost 27 ) 270.865 * * [simplify]: iteration 2 : 31 enodes (cost 27 ) 270.873 * * [simplify]: iteration 3 : 49 enodes (cost 27 ) 270.879 * * [simplify]: iteration 4 : 79 enodes (cost 27 ) 270.892 * * [simplify]: iteration 5 : 151 enodes (cost 27 ) 270.950 * * [simplify]: iteration 6 : 394 enodes (cost 27 ) 271.436 * * [simplify]: iteration 7 : 1412 enodes (cost 27 ) 273.225 * * [simplify]: iteration done : 5001 enodes (cost 27 ) 273.225 * * [simplify]: iteration 0 : 9 enodes (cost 18 ) 273.227 * * [simplify]: iteration 1 : 18 enodes (cost 18 ) 273.229 * * [simplify]: iteration 2 : 31 enodes (cost 18 ) 273.232 * * [simplify]: iteration 3 : 49 enodes (cost 18 ) 273.238 * * [simplify]: iteration 4 : 79 enodes (cost 18 ) 273.255 * * [simplify]: iteration 5 : 151 enodes (cost 18 ) 273.313 * * [simplify]: iteration 6 : 394 enodes (cost 18 ) 273.792 * * [simplify]: iteration 7 : 1412 enodes (cost 18 ) 275.579 * * [simplify]: iteration done : 5001 enodes (cost 18 ) 275.580 * * [simplify]: iteration 0 : 9 enodes (cost 11 ) 275.581 * * [simplify]: iteration 1 : 20 enodes (cost 10 ) 275.583 * * [simplify]: iteration 2 : 32 enodes (cost 10 ) 275.587 * * [simplify]: iteration 3 : 48 enodes (cost 8 ) 275.592 * * [simplify]: iteration 4 : 81 enodes (cost 8 ) 275.606 * * [simplify]: iteration 5 : 155 enodes (cost 8 ) 275.663 * * [simplify]: iteration 6 : 384 enodes (cost 8 ) 276.155 * * [simplify]: iteration 7 : 1407 enodes (cost 8 ) 278.087 * * [simplify]: iteration done : 5000 enodes (cost 8 ) 278.088 * * [simplify]: iteration 0 : 8 enodes (cost 11 ) 278.089 * * [simplify]: iteration 1 : 17 enodes (cost 11 ) 278.091 * * [simplify]: iteration 2 : 30 enodes (cost 11 ) 278.094 * * [simplify]: iteration 3 : 48 enodes (cost 11 ) 278.100 * * [simplify]: iteration 4 : 78 enodes (cost 11 ) 278.113 * * [simplify]: iteration 5 : 150 enodes (cost 11 ) 278.172 * * [simplify]: iteration 6 : 393 enodes (cost 11 ) 278.656 * * [simplify]: iteration 7 : 1403 enodes (cost 11 ) 280.659 * * [simplify]: iteration done : 5000 enodes (cost 11 ) 280.660 * * [simplify]: iteration 0 : 8 enodes (cost 11 ) 280.661 * * [simplify]: iteration 1 : 17 enodes (cost 11 ) 280.663 * * [simplify]: iteration 2 : 30 enodes (cost 11 ) 280.666 * * [simplify]: iteration 3 : 48 enodes (cost 11 ) 280.672 * * [simplify]: iteration 4 : 78 enodes (cost 11 ) 280.690 * * [simplify]: iteration 5 : 150 enodes (cost 11 ) 280.749 * * [simplify]: iteration 6 : 393 enodes (cost 11 ) 281.240 * * [simplify]: iteration 7 : 1403 enodes (cost 11 ) 283.250 * * [simplify]: iteration done : 5000 enodes (cost 11 ) 283.251 * * [simplify]: iteration 0 : 10 enodes (cost 13 ) 283.257 * * [simplify]: iteration 1 : 22 enodes (cost 13 ) 283.260 * * [simplify]: iteration 2 : 33 enodes (cost 13 ) 283.263 * * [simplify]: iteration 3 : 48 enodes (cost 13 ) 283.269 * * [simplify]: iteration 4 : 78 enodes (cost 13 ) 283.282 * * [simplify]: iteration 5 : 148 enodes (cost 13 ) 283.340 * * [simplify]: iteration 6 : 390 enodes (cost 13 ) 283.829 * * [simplify]: iteration 7 : 1409 enodes (cost 13 ) 285.745 * * [simplify]: iteration done : 5000 enodes (cost 13 ) 285.745 * * [simplify]: iteration 0 : 9 enodes (cost 28 ) 285.747 * * [simplify]: iteration 1 : 20 enodes (cost 28 ) 285.749 * * [simplify]: iteration 2 : 35 enodes (cost 28 ) 285.754 * * [simplify]: iteration 3 : 53 enodes (cost 28 ) 285.760 * * [simplify]: iteration 4 : 83 enodes (cost 28 ) 285.774 * * [simplify]: iteration 5 : 153 enodes (cost 28 ) 285.831 * * [simplify]: iteration 6 : 387 enodes (cost 28 ) 286.321 * * [simplify]: iteration 7 : 1422 enodes (cost 28 ) 288.141 * * [simplify]: iteration done : 5000 enodes (cost 28 ) 288.141 * * [simplify]: iteration 0 : 8 enodes (cost 18 ) 288.142 * * [simplify]: iteration 1 : 17 enodes (cost 18 ) 288.145 * * [simplify]: iteration 2 : 30 enodes (cost 18 ) 288.153 * * [simplify]: iteration 3 : 48 enodes (cost 18 ) 288.158 * * [simplify]: iteration 4 : 78 enodes (cost 18 ) 288.172 * * [simplify]: iteration 5 : 150 enodes (cost 18 ) 288.232 * * [simplify]: iteration 6 : 393 enodes (cost 18 ) 288.730 * * [simplify]: iteration 7 : 1403 enodes (cost 18 ) 290.758 * * [simplify]: iteration done : 5000 enodes (cost 18 ) 290.759 * * [simplify]: iteration 0 : 8 enodes (cost 10 ) 290.760 * * [simplify]: iteration 1 : 19 enodes (cost 8 ) 290.762 * * [simplify]: iteration 2 : 34 enodes (cost 8 ) 290.766 * * [simplify]: iteration 3 : 50 enodes (cost 8 ) 290.772 * * [simplify]: iteration 4 : 80 enodes (cost 8 ) 290.785 * * [simplify]: iteration 5 : 150 enodes (cost 8 ) 290.847 * * [simplify]: iteration 6 : 391 enodes (cost 8 ) 291.329 * * [simplify]: iteration 7 : 1402 enodes (cost 8 ) 293.248 * * [simplify]: iteration done : 5000 enodes (cost 8 ) 293.248 * * [simplify]: iteration 0 : 8 enodes (cost 18 ) 293.249 * * [simplify]: iteration 1 : 17 enodes (cost 18 ) 293.252 * * [simplify]: iteration 2 : 30 enodes (cost 18 ) 293.255 * * [simplify]: iteration 3 : 48 enodes (cost 18 ) 293.261 * * [simplify]: iteration 4 : 78 enodes (cost 18 ) 293.275 * * [simplify]: iteration 5 : 150 enodes (cost 18 ) 293.333 * * [simplify]: iteration 6 : 393 enodes (cost 18 ) 293.834 * * [simplify]: iteration 7 : 1403 enodes (cost 18 ) 296.118 * * [simplify]: iteration done : 5000 enodes (cost 18 ) 296.119 * * [simplify]: iteration 0 : 9 enodes (cost 18 ) 296.120 * * [simplify]: iteration 1 : 18 enodes (cost 18 ) 296.122 * * [simplify]: iteration 2 : 31 enodes (cost 18 ) 296.126 * * [simplify]: iteration 3 : 49 enodes (cost 18 ) 296.131 * * [simplify]: iteration 4 : 79 enodes (cost 18 ) 296.150 * * [simplify]: iteration 5 : 151 enodes (cost 18 ) 296.210 * * [simplify]: iteration 6 : 394 enodes (cost 18 ) 296.708 * * [simplify]: iteration 7 : 1412 enodes (cost 18 ) 298.567 * * [simplify]: iteration done : 5001 enodes (cost 18 ) 298.568 * * [simplify]: iteration 0 : 7 enodes (cost 17 ) 298.569 * * [simplify]: iteration 1 : 15 enodes (cost 17 ) 298.571 * * [simplify]: iteration 2 : 28 enodes (cost 17 ) 298.574 * * [simplify]: iteration 3 : 46 enodes (cost 17 ) 298.579 * * [simplify]: iteration 4 : 76 enodes (cost 17 ) 298.592 * * [simplify]: iteration 5 : 148 enodes (cost 17 ) 298.652 * * [simplify]: iteration 6 : 398 enodes (cost 17 ) 299.125 * * [simplify]: iteration 7 : 1405 enodes (cost 17 ) 301.103 * * [simplify]: iteration done : 5000 enodes (cost 17 ) 301.103 * * [simplify]: iteration 0 : 9 enodes (cost 15 ) 301.105 * * [simplify]: iteration 1 : 22 enodes (cost 15 ) 301.107 * * [simplify]: iteration 2 : 34 enodes (cost 15 ) 301.111 * * [simplify]: iteration 3 : 52 enodes (cost 15 ) 301.124 * * [simplify]: iteration 4 : 89 enodes (cost 15 ) 301.139 * * [simplify]: iteration 5 : 146 enodes (cost 15 ) 301.190 * * [simplify]: iteration 6 : 367 enodes (cost 15 ) 301.679 * * [simplify]: iteration 7 : 1385 enodes (cost 15 ) 303.728 * * [simplify]: iteration done : 5001 enodes (cost 15 ) 303.728 * * [simplify]: iteration 0 : 9 enodes (cost 15 ) 303.730 * * [simplify]: iteration 1 : 22 enodes (cost 15 ) 303.732 * * [simplify]: iteration 2 : 34 enodes (cost 15 ) 303.736 * * [simplify]: iteration 3 : 52 enodes (cost 15 ) 303.744 * * [simplify]: iteration 4 : 89 enodes (cost 15 ) 303.763 * * [simplify]: iteration 5 : 146 enodes (cost 15 ) 303.813 * * [simplify]: iteration 6 : 367 enodes (cost 15 ) 304.294 * * [simplify]: iteration 7 : 1385 enodes (cost 15 ) 306.345 * * [simplify]: iteration done : 5001 enodes (cost 15 ) 306.346 * * [simplify]: iteration 0 : 8 enodes (cost 13 ) 306.347 * * [simplify]: iteration 1 : 17 enodes (cost 13 ) 306.349 * * [simplify]: iteration 2 : 30 enodes (cost 13 ) 306.353 * * [simplify]: iteration 3 : 48 enodes (cost 13 ) 306.358 * * [simplify]: iteration 4 : 76 enodes (cost 13 ) 306.370 * * [simplify]: iteration 5 : 142 enodes (cost 13 ) 306.428 * * [simplify]: iteration 6 : 374 enodes (cost 13 ) 306.926 * * [simplify]: iteration 7 : 1386 enodes (cost 13 ) 308.934 * * [simplify]: iteration done : 5000 enodes (cost 13 ) 308.935 * * [simplify]: iteration 0 : 8 enodes (cost 18 ) 308.936 * * [simplify]: iteration 1 : 17 enodes (cost 18 ) 308.939 * * [simplify]: iteration 2 : 30 enodes (cost 18 ) 308.943 * * [simplify]: iteration 3 : 48 enodes (cost 18 ) 308.948 * * [simplify]: iteration 4 : 78 enodes (cost 18 ) 308.961 * * [simplify]: iteration 5 : 150 enodes (cost 18 ) 309.020 * * [simplify]: iteration 6 : 393 enodes (cost 18 ) 309.510 * * [simplify]: iteration 7 : 1403 enodes (cost 18 ) 311.550 * * [simplify]: iteration done : 5000 enodes (cost 18 ) 311.551 * * [simplify]: iteration 0 : 8 enodes (cost 18 ) 311.552 * * [simplify]: iteration 1 : 17 enodes (cost 18 ) 311.554 * * [simplify]: iteration 2 : 30 enodes (cost 18 ) 311.557 * * [simplify]: iteration 3 : 48 enodes (cost 18 ) 311.563 * * [simplify]: iteration 4 : 78 enodes (cost 18 ) 311.582 * * [simplify]: iteration 5 : 150 enodes (cost 18 ) 311.640 * * [simplify]: iteration 6 : 393 enodes (cost 18 ) 312.135 * * [simplify]: iteration 7 : 1403 enodes (cost 18 ) 314.189 * * [simplify]: iteration done : 5000 enodes (cost 18 ) 314.189 * * [simplify]: iteration 0 : 7 enodes (cost 17 ) 314.190 * * [simplify]: iteration 1 : 15 enodes (cost 17 ) 314.192 * * [simplify]: iteration 2 : 28 enodes (cost 17 ) 314.196 * * [simplify]: iteration 3 : 46 enodes (cost 17 ) 314.201 * * [simplify]: iteration 4 : 76 enodes (cost 17 ) 314.214 * * [simplify]: iteration 5 : 148 enodes (cost 17 ) 314.273 * * [simplify]: iteration 6 : 398 enodes (cost 17 ) 314.755 * * [simplify]: iteration 7 : 1405 enodes (cost 17 ) 316.729 * * [simplify]: iteration done : 5000 enodes (cost 17 ) 316.730 * * [simplify]: iteration 0 : 11 enodes (cost 21 ) 316.731 * * [simplify]: iteration 1 : 31 enodes (cost 21 ) 316.738 * * [simplify]: iteration 2 : 103 enodes (cost 19 ) 316.780 * * [simplify]: iteration 3 : 333 enodes (cost 19 ) 317.046 * * [simplify]: iteration 4 : 1182 enodes (cost 19 ) 319.307 * * [simplify]: iteration done : 5000 enodes (cost 19 ) 319.307 * * [simplify]: iteration 0 : 11 enodes (cost 25 ) 319.309 * * [simplify]: iteration 1 : 29 enodes (cost 19 ) 319.314 * * [simplify]: iteration 2 : 79 enodes (cost 17 ) 319.330 * * [simplify]: iteration 3 : 218 enodes (cost 17 ) 319.428 * * [simplify]: iteration 4 : 702 enodes (cost 17 ) 320.192 * * [simplify]: iteration 5 : 2924 enodes (cost 17 ) 322.006 * * [simplify]: iteration done : 5001 enodes (cost 17 ) 322.006 * * [simplify]: iteration 0 : 11 enodes (cost 21 ) 322.008 * * [simplify]: iteration 1 : 31 enodes (cost 21 ) 322.015 * * [simplify]: iteration 2 : 103 enodes (cost 19 ) 322.050 * * [simplify]: iteration 3 : 311 enodes (cost 19 ) 322.330 * * [simplify]: iteration 4 : 1183 enodes (cost 19 ) 324.587 * * [simplify]: iteration done : 5000 enodes (cost 19 ) 324.588 * * [simplify]: iteration 0 : 11 enodes (cost 25 ) 324.590 * * [simplify]: iteration 1 : 29 enodes (cost 19 ) 324.600 * * [simplify]: iteration 2 : 79 enodes (cost 17 ) 324.617 * * [simplify]: iteration 3 : 218 enodes (cost 17 ) 324.715 * * [simplify]: iteration 4 : 705 enodes (cost 17 ) 325.469 * * [simplify]: iteration 5 : 2916 enodes (cost 17 ) 327.152 * * [simplify]: iteration done : 5001 enodes (cost 17 ) 327.153 * * [simplify]: iteration 0 : 18 enodes (cost 42 ) 327.156 * * [simplify]: iteration 1 : 48 enodes (cost 39 ) 327.170 * * [simplify]: iteration 2 : 112 enodes (cost 23 ) 327.199 * * [simplify]: iteration 3 : 364 enodes (cost 15 ) 327.703 * * [simplify]: iteration 4 : 1695 enodes (cost 13 ) 328.938 * * [simplify]: iteration done : 5000 enodes (cost 13 ) 328.939 * * [simplify]: iteration 0 : 20 enodes (cost 48 ) 328.941 * * [simplify]: iteration 1 : 46 enodes (cost 42 ) 328.948 * * [simplify]: iteration 2 : 109 enodes (cost 36 ) 328.968 * * [simplify]: iteration 3 : 314 enodes (cost 19 ) 329.140 * * [simplify]: iteration 4 : 1061 enodes (cost 11 ) 330.341 * * [simplify]: iteration done : 5000 enodes (cost 11 ) 330.342 * * [simplify]: iteration 0 : 22 enodes (cost 51 ) 330.349 * * [simplify]: iteration 1 : 48 enodes (cost 48 ) 330.355 * * [simplify]: iteration 2 : 108 enodes (cost 48 ) 330.371 * * [simplify]: iteration 3 : 288 enodes (cost 31 ) 330.496 * * [simplify]: iteration 4 : 1035 enodes (cost 25 ) 331.361 * * [simplify]: iteration done : 5000 enodes (cost 19 ) 331.362 * * [simplify]: iteration 0 : 18 enodes (cost 42 ) 331.364 * * [simplify]: iteration 1 : 48 enodes (cost 39 ) 331.372 * * [simplify]: iteration 2 : 112 enodes (cost 23 ) 331.406 * * [simplify]: iteration 3 : 364 enodes (cost 15 ) 331.911 * * [simplify]: iteration 4 : 1695 enodes (cost 13 ) 333.133 * * [simplify]: iteration done : 5000 enodes (cost 13 ) 333.134 * * [simplify]: iteration 0 : 20 enodes (cost 48 ) 333.137 * * [simplify]: iteration 1 : 46 enodes (cost 42 ) 333.149 * * [simplify]: iteration 2 : 109 enodes (cost 36 ) 333.168 * * [simplify]: iteration 3 : 314 enodes (cost 19 ) 333.340 * * [simplify]: iteration 4 : 1061 enodes (cost 11 ) 334.526 * * [simplify]: iteration done : 5000 enodes (cost 11 ) 334.527 * * [simplify]: iteration 0 : 22 enodes (cost 51 ) 334.530 * * [simplify]: iteration 1 : 48 enodes (cost 48 ) 334.542 * * [simplify]: iteration 2 : 108 enodes (cost 48 ) 334.558 * * [simplify]: iteration 3 : 288 enodes (cost 31 ) 334.677 * * [simplify]: iteration 4 : 1035 enodes (cost 25 ) 335.529 * * [simplify]: iteration done : 5000 enodes (cost 19 ) 335.530 * * [simplify]: iteration 0 : 18 enodes (cost 42 ) 335.538 * * [simplify]: iteration 1 : 48 enodes (cost 39 ) 335.550 * * [simplify]: iteration 2 : 112 enodes (cost 23 ) 335.579 * * [simplify]: iteration 3 : 364 enodes (cost 15 ) 336.083 * * [simplify]: iteration 4 : 1695 enodes (cost 13 ) 337.305 * * [simplify]: iteration done : 5000 enodes (cost 13 ) 337.306 * * [simplify]: iteration 0 : 20 enodes (cost 48 ) 337.309 * * [simplify]: iteration 1 : 46 enodes (cost 42 ) 337.315 * * [simplify]: iteration 2 : 109 enodes (cost 36 ) 337.334 * * [simplify]: iteration 3 : 314 enodes (cost 19 ) 337.506 * * [simplify]: iteration 4 : 1061 enodes (cost 11 ) 338.682 * * [simplify]: iteration done : 5000 enodes (cost 11 ) 338.683 * * [simplify]: iteration 0 : 22 enodes (cost 51 ) 338.685 * * [simplify]: iteration 1 : 48 enodes (cost 48 ) 338.691 * * [simplify]: iteration 2 : 108 enodes (cost 48 ) 338.708 * * [simplify]: iteration 3 : 288 enodes (cost 31 ) 339.062 * * [simplify]: iteration 4 : 1035 enodes (cost 25 ) 339.937 * * [simplify]: iteration done : 5000 enodes (cost 19 ) 339.938 * * [simplify]: iteration 0 : 20 enodes (cost 42 ) 339.941 * * [simplify]: iteration 1 : 50 enodes (cost 39 ) 339.948 * * [simplify]: iteration 2 : 112 enodes (cost 27 ) 339.978 * * [simplify]: iteration 3 : 340 enodes (cost 17 ) 340.368 * * [simplify]: iteration 4 : 1468 enodes (cost 13 ) 341.608 * * [simplify]: iteration done : 5001 enodes (cost 13 ) 341.609 * * [simplify]: iteration 0 : 21 enodes (cost 48 ) 341.612 * * [simplify]: iteration 1 : 47 enodes (cost 42 ) 341.619 * * [simplify]: iteration 2 : 110 enodes (cost 36 ) 341.640 * * [simplify]: iteration 3 : 314 enodes (cost 19 ) 341.783 * * [simplify]: iteration 4 : 1061 enodes (cost 15 ) 342.521 * * [simplify]: iteration done : 5000 enodes (cost 15 ) 342.522 * * [simplify]: iteration 0 : 22 enodes (cost 48 ) 342.525 * * [simplify]: iteration 1 : 48 enodes (cost 45 ) 342.531 * * [simplify]: iteration 2 : 108 enodes (cost 39 ) 342.555 * * [simplify]: iteration 3 : 311 enodes (cost 21 ) 342.689 * * [simplify]: iteration 4 : 1106 enodes (cost 19 ) 343.477 * * [simplify]: iteration done : 5000 enodes (cost 17 ) 343.479 * [simplify]: Simplified to: (log (cbrt (+ (pow x 3) (* x x)))) (exp (cbrt (+ (pow x 3) (* x x)))) (cbrt (* (cbrt (+ (pow x 3) (* x x))) (cbrt (+ (pow x 3) (* x x))))) (cbrt (cbrt (+ (pow x 3) (* x x)))) (cbrt (sqrt (+ (pow x 3) (* x x)))) (cbrt (sqrt (+ (pow x 3) (* x x)))) 1 (cbrt (+ (pow x 3) (* x x))) (cbrt x) (cbrt (+ (* x x) x)) (cbrt x) (cbrt (+ (* x x) x)) (cbrt (+ x 1)) (cbrt (* x x)) (cbrt (+ (pow (pow x 3) 3) (pow x 6))) (cbrt (+ (pow x 6) (- (pow x 4) (pow x 5)))) (cbrt (- (pow x 6) (pow x 4))) (cbrt (- (pow x 3) (* x x))) (* (cbrt (cbrt (+ (pow x 3) (* x x)))) (cbrt (cbrt (+ (pow x 3) (* x x))))) (cbrt (cbrt (+ (pow x 3) (* x x)))) (+ (pow x 3) (* x x)) (sqrt (cbrt (+ (pow x 3) (* x x)))) (sqrt (cbrt (+ (pow x 3) (* x x)))) (log (cbrt (+ (pow x 3) (* x x)))) (exp (cbrt (+ (pow x 3) (* x x)))) (cbrt (* (cbrt (+ (pow x 3) (* x x))) (cbrt (+ (pow x 3) (* x x))))) (cbrt (cbrt (+ (pow x 3) (* x x)))) (cbrt (sqrt (+ (pow x 3) (* x x)))) (cbrt (sqrt (+ (pow x 3) (* x x)))) 1 (cbrt (+ (pow x 3) (* x x))) (cbrt x) (cbrt (+ (* x x) x)) (cbrt x) (cbrt (+ (* x x) x)) (cbrt (+ x 1)) (cbrt (* x x)) (cbrt (+ (pow (pow x 3) 3) (pow x 6))) (cbrt (+ (pow x 6) (- (pow x 4) (pow x 5)))) (cbrt (- (pow x 6) (pow x 4))) (cbrt (- (pow x 3) (* x x))) (* (cbrt (cbrt (+ (pow x 3) (* x x)))) (cbrt (cbrt (+ (pow x 3) (* x x))))) (cbrt (cbrt (+ (pow x 3) (* x x)))) (+ (pow x 3) (* x x)) (sqrt (cbrt (+ (pow x 3) (* x x)))) (sqrt (cbrt (+ (pow x 3) (* x x)))) (log (cbrt (+ (pow x 3) (* x x)))) (exp (cbrt (+ (pow x 3) (* x x)))) (cbrt (* (cbrt (+ (pow x 3) (* x x))) (cbrt (+ (pow x 3) (* x x))))) (cbrt (cbrt (+ (pow x 3) (* x x)))) (cbrt (sqrt (+ (pow x 3) (* x x)))) (cbrt (sqrt (+ (pow x 3) (* x x)))) 1 (cbrt (+ (pow x 3) (* x x))) (cbrt x) (cbrt (+ (* x x) x)) (cbrt x) (cbrt (+ (* x x) x)) (cbrt (+ x 1)) (cbrt (* x x)) (cbrt (+ (pow (pow x 3) 3) (pow x 6))) (cbrt (+ (pow x 6) (- (pow x 4) (pow x 5)))) (cbrt (- (pow x 6) (pow x 4))) (cbrt (- (pow x 3) (* x x))) (* (cbrt (cbrt (+ (pow x 3) (* x x)))) (cbrt (cbrt (+ (pow x 3) (* x x))))) (cbrt (cbrt (+ (pow x 3) (* x x)))) (+ (pow x 3) (* x x)) (sqrt (cbrt (+ (pow x 3) (* x x)))) (sqrt (cbrt (+ (pow x 3) (* x x)))) 2/3 2 (* (pow x 4) (* (+ x 1) (+ x 1))) (* (cbrt (+ (pow x 3) (* x x))) (cbrt (+ (pow x 3) (* x x)))) 2 (* 2 (log (cbrt (+ (pow x 3) (* x x))))) (* 2 (log (cbrt (+ (pow x 3) (* x x))))) (exp (* (cbrt (+ (pow x 3) (* x x))) (cbrt (+ (pow x 3) (* x x))))) (* (pow x 4) (* (+ x 1) (+ x 1))) (* (cbrt (* (cbrt (+ (pow x 3) (* x x))) (cbrt (+ (pow x 3) (* x x))))) (cbrt (* (cbrt (+ (pow x 3) (* x x))) (cbrt (+ (pow x 3) (* x x)))))) (cbrt (* (cbrt (+ (pow x 3) (* x x))) (cbrt (+ (pow x 3) (* x x))))) (pow (cbrt (+ (pow x 3) (* x x))) 6) (fabs (cbrt (+ (pow x 3) (* x x)))) (fabs (cbrt (+ (pow x 3) (* x x)))) (* (cbrt (+ (pow (pow x 3) 3) (pow x 6))) (cbrt (+ (pow (pow x 3) 3) (pow x 6)))) (* (cbrt (+ (pow x 6) (- (pow x 4) (pow x 5)))) (cbrt (+ (pow x 6) (- (pow x 4) (pow x 5))))) (* (cbrt (- (pow x 6) (pow x 4))) (cbrt (+ (pow (pow x 3) 3) (pow x 6)))) (* (cbrt (- (pow x 3) (* x x))) (cbrt (- (+ (pow x 6) (pow x 4)) (pow x 5)))) (* (cbrt (+ (pow (pow x 3) 3) (pow x 6))) (cbrt (- (pow x 6) (pow x 4)))) (* (cbrt (- (pow x 3) (* x x))) (cbrt (- (+ (pow x 4) (pow x 6)) (pow x 5)))) (* (cbrt (- (pow x 6) (pow x 4))) (cbrt (- (pow x 6) (pow x 4)))) (* (cbrt (- (pow x 3) (* x x))) (cbrt (- (pow x 3) (* x x)))) (* (cbrt (* (cbrt (+ (pow x 3) (* x x))) (cbrt (+ (pow x 3) (* x x))))) (cbrt (* (cbrt (+ (pow x 3) (* x x))) (cbrt (+ (pow x 3) (* x x)))))) (* (cbrt (cbrt (+ (pow x 3) (* x x)))) (cbrt (cbrt (+ (pow x 3) (* x x))))) (* (cbrt (sqrt (+ (pow x 3) (* x x)))) (cbrt (sqrt (+ (pow x 3) (* x x))))) (* (cbrt (sqrt (+ (pow x 3) (* x x)))) (cbrt (sqrt (+ (pow x 3) (* x x))))) 1 (* (cbrt (+ (pow x 3) (* x x))) (cbrt (+ (pow x 3) (* x x)))) (* (cbrt x) (cbrt x)) (* (cbrt (+ (* x x) x)) (cbrt (+ (* x x) x))) (* (cbrt x) (cbrt x)) (* (cbrt (+ (* x x) x)) (cbrt (+ (* x x) x))) (* (cbrt x) (cbrt x)) (* (cbrt (+ (* x x) x)) (cbrt (+ (* x x) x))) (* (cbrt x) (cbrt x)) (* (cbrt (+ (* x x) x)) (cbrt (+ (* x x) x))) (* (cbrt (+ x 1)) (cbrt (+ x 1))) (* (cbrt (* x x)) (cbrt (* x x))) (pow (cbrt (cbrt (+ (pow x 3) (* x x)))) 4) (* (cbrt (cbrt (+ (pow x 3) (* x x)))) (cbrt (cbrt (+ (pow x 3) (* x x))))) (cbrt (+ (pow x 3) (* x x))) (cbrt (+ (pow x 3) (* x x))) 1 (* (cbrt (+ (pow x 3) (* x x))) (cbrt (+ (pow x 3) (* x x)))) (* (cbrt (sqrt (+ (pow x 3) (* x x)))) (cbrt (sqrt (+ (pow x 3) (* x x))))) (* (cbrt (sqrt (+ (pow x 3) (* x x)))) (cbrt (sqrt (+ (pow x 3) (* x x))))) (* (cbrt (sqrt (+ (pow x 3) (* x x)))) (sqrt (cbrt (+ (pow x 3) (* x x))))) (* (cbrt (sqrt (+ (pow x 3) (* x x)))) (sqrt (cbrt (+ (pow x 3) (* x x))))) (* (sqrt (cbrt (+ (pow x 3) (* x x)))) (cbrt (sqrt (+ (pow x 3) (* x x))))) (* (sqrt (cbrt (+ (pow x 3) (* x x)))) (cbrt (sqrt (+ (pow x 3) (* x x))))) (cbrt (+ (pow x 3) (* x x))) (cbrt (+ (pow x 3) (* x x))) 2/3 2 (* (cbrt (+ (pow x 3) (* x x))) (cbrt (* (cbrt (+ (pow x 3) (* x x))) (cbrt (+ (pow x 3) (* x x)))))) (* (cbrt (+ (pow x 3) (* x x))) (cbrt (sqrt (+ (pow x 3) (* x x))))) (cbrt (+ (pow x 3) (* x x))) (* (cbrt (+ (pow x 3) (* x x))) (cbrt x)) (* (cbrt (+ (pow x 3) (* x x))) (cbrt x)) (* (cbrt (+ (pow x 3) (* x x))) (cbrt (+ x 1))) (* (cbrt (+ (pow x 3) (* x x))) (* (cbrt (cbrt (+ (pow x 3) (* x x)))) (cbrt (cbrt (+ (pow x 3) (* x x)))))) (* (cbrt (+ (pow x 3) (* x x))) (sqrt (cbrt (+ (pow x 3) (* x x))))) (cbrt (+ (pow x 3) (* x x))) (* (cbrt (cbrt (+ (pow x 3) (* x x)))) (cbrt (+ (pow x 3) (* x x)))) (* (cbrt (sqrt (+ (pow x 3) (* x x)))) (cbrt (+ (pow x 3) (* x x)))) (* (cbrt (+ (pow x 3) (* x x))) (cbrt (+ (pow x 3) (* x x)))) (* (cbrt (+ (* x x) x)) (cbrt (+ (pow x 3) (* x x)))) (* (cbrt (+ (* x x) x)) (cbrt (+ (pow x 3) (* x x)))) (* (cbrt (* x x)) (cbrt (+ (pow x 3) (* x x)))) (* (cbrt (cbrt (+ (pow x 3) (* x x)))) (cbrt (+ (pow x 3) (* x x)))) (* (sqrt (cbrt (+ (pow x 3) (* x x)))) (cbrt (+ (pow x 3) (* x x)))) (* (cbrt (+ (pow x 3) (* x x))) (cbrt (+ (pow x 3) (* x x)))) (* (cbrt (+ (pow x 6) (pow (pow x 3) 3))) (cbrt (+ (pow x 3) (* x x)))) (* (cbrt (- (pow x 6) (pow x 4))) (cbrt (+ (pow x 3) (* x x)))) (* (cbrt (+ (pow (pow x 3) 3) (pow x 6))) (cbrt (+ (pow x 3) (* x x)))) (* (cbrt (- (pow x 6) (pow x 4))) (cbrt (+ (pow x 3) (* x x)))) (* (+ 1 (* x (- 1/3 (* 1/9 x)))) (pow x 2/3)) (+ x (* (- 1/3 (/ 1/9 x)) (/ x x))) (* (cbrt (neg (pow (/ -1 x) -3))) (- (+ (/ 1/3 x) 1) (/ 1/9 (pow x 2)))) (* (+ 1 (* x (- 1/3 (* 1/9 x)))) (pow x 2/3)) (+ x (* (- 1/3 (/ 1/9 x)) (/ x x))) (* (cbrt (neg (pow (/ -1 x) -3))) (- (+ (/ 1/3 x) 1) (/ 1/9 (pow x 2)))) (* (+ 1 (* x (- 1/3 (* 1/9 x)))) (pow x 2/3)) (+ x (* (- 1/3 (/ 1/9 x)) (/ x x))) (* (cbrt (neg (pow (/ -1 x) -3))) (- (+ (/ 1/3 x) 1) (/ 1/9 (pow x 2)))) (- (pow x 4/3) (* (pow x 7/3) (- (* 1/9 x) 2/3))) (+ (pow x 2) (* (- 2/3 (/ 1/9 x)) (/ (* x x) x))) (* (pow (/ -1 x) -2) (- 1 (- (/ 1/9 (pow x 2)) (/ 2/3 x)))) 343.480 * * * [progress]: adding candidates to table 343.784 * [progress]: [Phase 3 of 3] Extracting. 343.784 * * [regime]: Finding splitpoints for: (# #) 343.785 * * * [regime-changes]: Trying 1 branch expressions: (x) 343.785 * * * * [regimes]: Trying to branch on x from (# #) 343.811 * * * [regime]: Found split indices: #