17.903 * [progress]: [Phase 1 of 3] Setting up. 0.001 * * * [progress]: [1/2] Preparing points 0.010 * * * [progress]: [2/2] Setting up program. 0.012 * [progress]: [Phase 2 of 3] Improving. 0.013 * [simplify]: Simplifying using # : (/ (+ x 16.0) 116.0) 0.013 * * [simplify]: iteration 0 : 5 enodes (cost 5 ) 0.014 * * [simplify]: iteration 1 : 6 enodes (cost 5 ) 0.014 * * [simplify]: iteration done : 6 enodes (cost 5 ) 0.014 * [simplify]: Simplified to: (/ (+ x 16.0) 116.0) 0.015 * * [progress]: iteration 1 / 4 0.015 * * * [progress]: picking best candidate 0.017 * * * * [pick]: Picked # 0.017 * * * [progress]: localizing error 0.021 * * * [progress]: generating rewritten candidates 0.021 * * * * [progress]: [ 1 / 1 ] rewriting at (2) 0.028 * * * [progress]: generating series expansions 0.028 * * * * [progress]: [ 1 / 1 ] generating series at (2) 0.028 * [approximate]: Taking taylor expansion of (* 0.008620689655172414 (+ x 16.0)) in (x) around 0 0.028 * [taylor]: Taking taylor expansion of (* 0.008620689655172414 (+ x 16.0)) in x 0.028 * [taylor]: Taking taylor expansion of 0.008620689655172414 in x 0.028 * [taylor]: Taking taylor expansion of (+ x 16.0) in x 0.028 * [taylor]: Taking taylor expansion of x in x 0.028 * [taylor]: Taking taylor expansion of 16.0 in x 0.028 * [taylor]: Taking taylor expansion of (* 0.008620689655172414 (+ x 16.0)) in x 0.028 * [taylor]: Taking taylor expansion of 0.008620689655172414 in x 0.028 * [taylor]: Taking taylor expansion of (+ x 16.0) in x 0.028 * [taylor]: Taking taylor expansion of x in x 0.028 * [taylor]: Taking taylor expansion of 16.0 in x 0.029 * [approximate]: Taking taylor expansion of (* 0.008620689655172414 (+ (/ 1 x) 16.0)) in (x) around 0 0.029 * [taylor]: Taking taylor expansion of (* 0.008620689655172414 (+ (/ 1 x) 16.0)) in x 0.029 * [taylor]: Taking taylor expansion of 0.008620689655172414 in x 0.029 * [taylor]: Taking taylor expansion of (+ (/ 1 x) 16.0) in x 0.029 * [taylor]: Taking taylor expansion of (/ 1 x) in x 0.029 * [taylor]: Taking taylor expansion of x in x 0.029 * [taylor]: Taking taylor expansion of 16.0 in x 0.029 * [taylor]: Taking taylor expansion of (* 0.008620689655172414 (+ (/ 1 x) 16.0)) in x 0.029 * [taylor]: Taking taylor expansion of 0.008620689655172414 in x 0.029 * [taylor]: Taking taylor expansion of (+ (/ 1 x) 16.0) in x 0.029 * [taylor]: Taking taylor expansion of (/ 1 x) in x 0.029 * [taylor]: Taking taylor expansion of x in x 0.029 * [taylor]: Taking taylor expansion of 16.0 in x 0.031 * [approximate]: Taking taylor expansion of (* 0.008620689655172414 (- 16.0 (/ 1 x))) in (x) around 0 0.031 * [taylor]: Taking taylor expansion of (* 0.008620689655172414 (- 16.0 (/ 1 x))) in x 0.031 * [taylor]: Taking taylor expansion of 0.008620689655172414 in x 0.031 * [taylor]: Taking taylor expansion of (- 16.0 (/ 1 x)) in x 0.031 * [taylor]: Taking taylor expansion of 16.0 in x 0.031 * [taylor]: Taking taylor expansion of (/ 1 x) in x 0.031 * [taylor]: Taking taylor expansion of x in x 0.031 * [taylor]: Taking taylor expansion of (* 0.008620689655172414 (- 16.0 (/ 1 x))) in x 0.031 * [taylor]: Taking taylor expansion of 0.008620689655172414 in x 0.031 * [taylor]: Taking taylor expansion of (- 16.0 (/ 1 x)) in x 0.031 * [taylor]: Taking taylor expansion of 16.0 in x 0.031 * [taylor]: Taking taylor expansion of (/ 1 x) in x 0.031 * [taylor]: Taking taylor expansion of x in x 0.032 * * * [progress]: simplifying candidates 0.033 * [simplify]: Simplifying using # : (- (log (+ x 16.0)) (log 116.0)) (log (/ (+ x 16.0) 116.0)) (exp (/ (+ x 16.0) 116.0)) (/ (* (* (+ x 16.0) (+ x 16.0)) (+ x 16.0)) (* (* 116.0 116.0) 116.0)) (* (cbrt (/ (+ x 16.0) 116.0)) (cbrt (/ (+ x 16.0) 116.0))) (cbrt (/ (+ x 16.0) 116.0)) (* (* (/ (+ x 16.0) 116.0) (/ (+ x 16.0) 116.0)) (/ (+ x 16.0) 116.0)) (sqrt (/ (+ x 16.0) 116.0)) (sqrt (/ (+ x 16.0) 116.0)) (neg (+ x 16.0)) (neg 116.0) (/ (* (cbrt (+ x 16.0)) (cbrt (+ x 16.0))) (* (cbrt 116.0) (cbrt 116.0))) (/ (cbrt (+ x 16.0)) (cbrt 116.0)) (/ (* (cbrt (+ x 16.0)) (cbrt (+ x 16.0))) (sqrt 116.0)) (/ (cbrt (+ x 16.0)) (sqrt 116.0)) (/ (* (cbrt (+ x 16.0)) (cbrt (+ x 16.0))) 1) (/ (cbrt (+ x 16.0)) 116.0) (/ (sqrt (+ x 16.0)) (* (cbrt 116.0) (cbrt 116.0))) (/ (sqrt (+ x 16.0)) (cbrt 116.0)) (/ (sqrt (+ x 16.0)) (sqrt 116.0)) (/ (sqrt (+ x 16.0)) (sqrt 116.0)) (/ (sqrt (+ x 16.0)) 1) (/ (sqrt (+ x 16.0)) 116.0) (/ 1 (* (cbrt 116.0) (cbrt 116.0))) (/ (+ x 16.0) (cbrt 116.0)) (/ 1 (sqrt 116.0)) (/ (+ x 16.0) (sqrt 116.0)) (/ 1 1) (/ (+ x 16.0) 116.0) (/ 1 (* (cbrt 116.0) (cbrt 116.0))) (/ (+ x 16.0) (cbrt 116.0)) (/ 1 (sqrt 116.0)) (/ (+ x 16.0) (sqrt 116.0)) (/ 1 1) (/ (+ x 16.0) 116.0) (/ 1 116.0) (/ 116.0 (+ x 16.0)) (/ (+ x 16.0) (* (cbrt 116.0) (cbrt 116.0))) (/ (+ x 16.0) (sqrt 116.0)) (/ (+ x 16.0) 1) (/ 116.0 (cbrt (+ x 16.0))) (/ 116.0 (sqrt (+ x 16.0))) (/ 116.0 (+ x 16.0)) (/ 116.0 (+ x 16.0)) (* 116.0 (+ (* x x) (- (* 16.0 16.0) (* x 16.0)))) (* 116.0 (- x 16.0)) (+ (* 0.008620689655172414 x) 0.13793103448275862) (+ (* 0.008620689655172414 x) 0.13793103448275862) (+ (* 0.008620689655172414 x) 0.13793103448275862) 0.033 * * [simplify]: iteration 0 : 7 enodes (cost 7 ) 0.034 * * [simplify]: iteration 1 : 10 enodes (cost 7 ) 0.035 * * [simplify]: iteration 2 : 11 enodes (cost 7 ) 0.036 * * [simplify]: iteration done : 11 enodes (cost 7 ) 0.036 * * [simplify]: iteration 0 : 6 enodes (cost 6 ) 0.037 * * [simplify]: iteration 1 : 10 enodes (cost 6 ) 0.038 * * [simplify]: iteration 2 : 12 enodes (cost 6 ) 0.039 * * [simplify]: iteration 3 : 13 enodes (cost 6 ) 0.040 * * [simplify]: iteration done : 13 enodes (cost 6 ) 0.041 * * [simplify]: iteration 0 : 6 enodes (cost 6 ) 0.042 * * [simplify]: iteration 1 : 7 enodes (cost 6 ) 0.042 * * [simplify]: iteration done : 7 enodes (cost 6 ) 0.043 * * [simplify]: iteration 0 : 9 enodes (cost 17 ) 0.044 * * [simplify]: iteration 1 : 31 enodes (cost 17 ) 0.051 * * [simplify]: iteration 2 : 93 enodes (cost 9 ) 0.076 * * [simplify]: iteration 3 : 236 enodes (cost 7 ) 0.154 * * [simplify]: iteration 4 : 620 enodes (cost 7 ) 0.492 * * [simplify]: iteration 5 : 1689 enodes (cost 7 ) 1.955 * * [simplify]: iteration 6 : 4465 enodes (cost 7 ) 3.180 * * [simplify]: iteration done : 5001 enodes (cost 7 ) 3.181 * * [simplify]: iteration 0 : 7 enodes (cost 13 ) 3.182 * * [simplify]: iteration 1 : 8 enodes (cost 13 ) 3.183 * * [simplify]: iteration done : 8 enodes (cost 13 ) 3.184 * * [simplify]: iteration 0 : 6 enodes (cost 6 ) 3.184 * * [simplify]: iteration 1 : 7 enodes (cost 6 ) 3.185 * * [simplify]: iteration done : 7 enodes (cost 6 ) 3.186 * * [simplify]: iteration 0 : 7 enodes (cost 17 ) 3.186 * * [simplify]: iteration 1 : 15 enodes (cost 17 ) 3.190 * * [simplify]: iteration 2 : 47 enodes (cost 7 ) 3.199 * * [simplify]: iteration 3 : 119 enodes (cost 7 ) 3.227 * * [simplify]: iteration 4 : 298 enodes (cost 7 ) 3.320 * * [simplify]: iteration 5 : 589 enodes (cost 7 ) 3.577 * * [simplify]: iteration 6 : 1238 enodes (cost 7 ) 4.408 * * [simplify]: iteration 7 : 3090 enodes (cost 7 ) 5.610 * * [simplify]: iteration done : 5000 enodes (cost 7 ) 5.611 * * [simplify]: iteration 0 : 6 enodes (cost 6 ) 5.611 * * [simplify]: iteration 1 : 7 enodes (cost 6 ) 5.612 * * [simplify]: iteration done : 7 enodes (cost 6 ) 5.612 * * [simplify]: iteration 0 : 6 enodes (cost 6 ) 5.613 * * [simplify]: iteration 1 : 7 enodes (cost 6 ) 5.614 * * [simplify]: iteration done : 7 enodes (cost 6 ) 5.615 * * [simplify]: iteration 0 : 4 enodes (cost 4 ) 5.615 * * [simplify]: iteration 1 : 8 enodes (cost 4 ) 5.616 * * [simplify]: iteration 2 : 10 enodes (cost 4 ) 5.617 * * [simplify]: iteration 3 : 11 enodes (cost 4 ) 5.618 * * [simplify]: iteration done : 11 enodes (cost 4 ) 5.619 * * [simplify]: iteration 0 : 2 enodes (cost 2 ) 5.619 * * [simplify]: iteration done : 2 enodes (cost 2 ) 5.619 * * [simplify]: iteration 0 : 9 enodes (cost 15 ) 5.620 * * [simplify]: iteration 1 : 16 enodes (cost 15 ) 5.622 * * [simplify]: iteration 2 : 25 enodes (cost 15 ) 5.625 * * [simplify]: iteration 3 : 31 enodes (cost 15 ) 5.629 * * [simplify]: iteration done : 31 enodes (cost 15 ) 5.630 * * [simplify]: iteration 0 : 7 enodes (cost 7 ) 5.631 * * [simplify]: iteration 1 : 8 enodes (cost 7 ) 5.631 * * [simplify]: iteration done : 8 enodes (cost 7 ) 5.632 * * [simplify]: iteration 0 : 8 enodes (cost 12 ) 5.633 * * [simplify]: iteration 1 : 11 enodes (cost 12 ) 5.634 * * [simplify]: iteration 2 : 13 enodes (cost 12 ) 5.635 * * [simplify]: iteration 3 : 14 enodes (cost 12 ) 5.637 * * [simplify]: iteration done : 14 enodes (cost 12 ) 5.637 * * [simplify]: iteration 0 : 7 enodes (cost 7 ) 5.638 * * [simplify]: iteration 1 : 8 enodes (cost 7 ) 5.639 * * [simplify]: iteration done : 8 enodes (cost 7 ) 5.639 * * [simplify]: iteration 0 : 7 enodes (cost 11 ) 5.640 * * [simplify]: iteration 1 : 12 enodes (cost 9 ) 5.641 * * [simplify]: iteration 2 : 18 enodes (cost 9 ) 5.643 * * [simplify]: iteration 3 : 23 enodes (cost 9 ) 5.645 * * [simplify]: iteration done : 23 enodes (cost 9 ) 5.646 * * [simplify]: iteration 0 : 6 enodes (cost 6 ) 5.646 * * [simplify]: iteration 1 : 7 enodes (cost 6 ) 5.647 * * [simplify]: iteration done : 7 enodes (cost 6 ) 5.647 * * [simplify]: iteration 0 : 8 enodes (cost 10 ) 5.648 * * [simplify]: iteration 1 : 11 enodes (cost 10 ) 5.649 * * [simplify]: iteration done : 11 enodes (cost 10 ) 5.650 * * [simplify]: iteration 0 : 7 enodes (cost 7 ) 5.650 * * [simplify]: iteration 1 : 8 enodes (cost 7 ) 5.651 * * [simplify]: iteration done : 8 enodes (cost 7 ) 5.652 * * [simplify]: iteration 0 : 7 enodes (cost 7 ) 5.652 * * [simplify]: iteration 1 : 8 enodes (cost 7 ) 5.653 * * [simplify]: iteration done : 8 enodes (cost 7 ) 5.654 * * [simplify]: iteration 0 : 7 enodes (cost 7 ) 5.654 * * [simplify]: iteration 1 : 8 enodes (cost 7 ) 5.655 * * [simplify]: iteration done : 8 enodes (cost 7 ) 5.656 * * [simplify]: iteration 0 : 6 enodes (cost 6 ) 5.656 * * [simplify]: iteration 1 : 9 enodes (cost 4 ) 5.657 * * [simplify]: iteration 2 : 11 enodes (cost 4 ) 5.658 * * [simplify]: iteration done : 11 enodes (cost 4 ) 5.658 * * [simplify]: iteration 0 : 6 enodes (cost 6 ) 5.659 * * [simplify]: iteration 1 : 7 enodes (cost 6 ) 5.660 * * [simplify]: iteration done : 7 enodes (cost 6 ) 5.660 * * [simplify]: iteration 0 : 5 enodes (cost 7 ) 5.661 * * [simplify]: iteration 1 : 9 enodes (cost 7 ) 5.662 * * [simplify]: iteration done : 9 enodes (cost 7 ) 5.662 * * [simplify]: iteration 0 : 6 enodes (cost 6 ) 5.663 * * [simplify]: iteration 1 : 7 enodes (cost 6 ) 5.664 * * [simplify]: iteration done : 7 enodes (cost 6 ) 5.664 * * [simplify]: iteration 0 : 4 enodes (cost 4 ) 5.665 * * [simplify]: iteration 1 : 6 enodes (cost 4 ) 5.665 * * [simplify]: iteration done : 6 enodes (cost 4 ) 5.666 * * [simplify]: iteration 0 : 6 enodes (cost 6 ) 5.666 * * [simplify]: iteration 1 : 7 enodes (cost 6 ) 5.667 * * [simplify]: iteration done : 7 enodes (cost 6 ) 5.667 * * [simplify]: iteration 0 : 2 enodes (cost 3 ) 5.668 * * [simplify]: iteration 1 : 4 enodes (cost 1 ) 5.668 * * [simplify]: iteration done : 4 enodes (cost 1 ) 5.668 * * [simplify]: iteration 0 : 5 enodes (cost 5 ) 5.671 * * [simplify]: iteration 1 : 6 enodes (cost 5 ) 5.672 * * [simplify]: iteration done : 6 enodes (cost 5 ) 5.673 * * [simplify]: iteration 0 : 5 enodes (cost 7 ) 5.673 * * [simplify]: iteration 1 : 9 enodes (cost 7 ) 5.674 * * [simplify]: iteration done : 9 enodes (cost 7 ) 5.675 * * [simplify]: iteration 0 : 6 enodes (cost 6 ) 5.675 * * [simplify]: iteration 1 : 7 enodes (cost 6 ) 5.676 * * [simplify]: iteration done : 7 enodes (cost 6 ) 5.677 * * [simplify]: iteration 0 : 4 enodes (cost 4 ) 5.677 * * [simplify]: iteration 1 : 6 enodes (cost 4 ) 5.678 * * [simplify]: iteration done : 6 enodes (cost 4 ) 5.678 * * [simplify]: iteration 0 : 6 enodes (cost 6 ) 5.679 * * [simplify]: iteration 1 : 7 enodes (cost 6 ) 5.680 * * [simplify]: iteration done : 7 enodes (cost 6 ) 5.680 * * [simplify]: iteration 0 : 2 enodes (cost 3 ) 5.681 * * [simplify]: iteration 1 : 4 enodes (cost 1 ) 5.681 * * [simplify]: iteration done : 4 enodes (cost 1 ) 5.681 * * [simplify]: iteration 0 : 5 enodes (cost 5 ) 5.682 * * [simplify]: iteration 1 : 6 enodes (cost 5 ) 5.682 * * [simplify]: iteration done : 6 enodes (cost 5 ) 5.683 * * [simplify]: iteration 0 : 3 enodes (cost 3 ) 5.683 * * [simplify]: iteration 1 : 5 enodes (cost 3 ) 5.684 * * [simplify]: iteration done : 5 enodes (cost 3 ) 5.684 * * [simplify]: iteration 0 : 5 enodes (cost 5 ) 5.685 * * [simplify]: iteration 1 : 6 enodes (cost 5 ) 5.685 * * [simplify]: iteration done : 6 enodes (cost 5 ) 5.686 * * [simplify]: iteration 0 : 7 enodes (cost 9 ) 5.687 * * [simplify]: iteration 1 : 10 enodes (cost 9 ) 5.688 * * [simplify]: iteration done : 10 enodes (cost 9 ) 5.689 * * [simplify]: iteration 0 : 6 enodes (cost 6 ) 5.689 * * [simplify]: iteration 1 : 7 enodes (cost 6 ) 5.690 * * [simplify]: iteration done : 7 enodes (cost 6 ) 5.691 * * [simplify]: iteration 0 : 5 enodes (cost 5 ) 5.691 * * [simplify]: iteration 1 : 8 enodes (cost 3 ) 5.692 * * [simplify]: iteration 2 : 10 enodes (cost 3 ) 5.692 * * [simplify]: iteration done : 10 enodes (cost 3 ) 5.693 * * [simplify]: iteration 0 : 6 enodes (cost 6 ) 5.694 * * [simplify]: iteration 1 : 7 enodes (cost 6 ) 5.694 * * [simplify]: iteration done : 7 enodes (cost 6 ) 5.695 * * [simplify]: iteration 0 : 6 enodes (cost 6 ) 5.695 * * [simplify]: iteration 1 : 7 enodes (cost 6 ) 5.696 * * [simplify]: iteration done : 7 enodes (cost 6 ) 5.697 * * [simplify]: iteration 0 : 5 enodes (cost 5 ) 5.697 * * [simplify]: iteration 1 : 6 enodes (cost 5 ) 5.698 * * [simplify]: iteration done : 6 enodes (cost 5 ) 5.698 * * [simplify]: iteration 0 : 5 enodes (cost 5 ) 5.699 * * [simplify]: iteration 1 : 6 enodes (cost 5 ) 5.699 * * [simplify]: iteration done : 6 enodes (cost 5 ) 5.700 * * [simplify]: iteration 0 : 9 enodes (cost 13 ) 5.701 * * [simplify]: iteration 1 : 24 enodes (cost 11 ) 5.705 * * [simplify]: iteration 2 : 54 enodes (cost 11 ) 5.714 * * [simplify]: iteration 3 : 102 enodes (cost 11 ) 5.739 * * [simplify]: iteration 4 : 155 enodes (cost 11 ) 5.771 * * [simplify]: iteration 5 : 207 enodes (cost 11 ) 5.825 * * [simplify]: iteration 6 : 262 enodes (cost 11 ) 5.882 * * [simplify]: iteration 7 : 326 enodes (cost 11 ) 5.974 * * [simplify]: iteration 8 : 461 enodes (cost 11 ) 6.143 * * [simplify]: iteration 9 : 708 enodes (cost 11 ) 6.343 * * [simplify]: iteration 10 : 784 enodes (cost 11 ) 6.513 * * [simplify]: iteration 11 : 785 enodes (cost 11 ) 6.678 * * [simplify]: iteration done : 785 enodes (cost 11 ) 6.679 * * [simplify]: iteration 0 : 5 enodes (cost 5 ) 6.680 * * [simplify]: iteration 1 : 8 enodes (cost 5 ) 6.681 * * [simplify]: iteration 2 : 15 enodes (cost 5 ) 6.683 * * [simplify]: iteration 3 : 20 enodes (cost 5 ) 6.685 * * [simplify]: iteration 4 : 24 enodes (cost 5 ) 6.688 * * [simplify]: iteration done : 24 enodes (cost 5 ) 6.689 * * [simplify]: iteration 0 : 5 enodes (cost 5 ) 6.689 * * [simplify]: iteration 1 : 7 enodes (cost 5 ) 6.690 * * [simplify]: iteration done : 7 enodes (cost 5 ) 6.691 * * [simplify]: iteration 0 : 5 enodes (cost 5 ) 6.691 * * [simplify]: iteration 1 : 7 enodes (cost 5 ) 6.692 * * [simplify]: iteration done : 7 enodes (cost 5 ) 6.692 * * [simplify]: iteration 0 : 5 enodes (cost 5 ) 6.693 * * [simplify]: iteration 1 : 7 enodes (cost 5 ) 6.694 * * [simplify]: iteration done : 7 enodes (cost 5 ) 6.694 * [simplify]: Simplified to: (- (log (+ x 16.0)) (log 116.0)) (log (/ (+ x 16.0) 116.0)) (exp (/ (+ x 16.0) 116.0)) (pow (/ (+ x 16.0) 116.0) 3) (* (cbrt (/ (+ x 16.0) 116.0)) (cbrt (/ (+ x 16.0) 116.0))) (cbrt (/ (+ x 16.0) 116.0)) (pow (/ (+ x 16.0) 116.0) 3) (sqrt (/ (+ x 16.0) 116.0)) (sqrt (/ (+ x 16.0) 116.0)) (neg (+ x 16.0)) (neg 116.0) (/ (* (cbrt (+ x 16.0)) (cbrt (+ x 16.0))) (* (cbrt 116.0) (cbrt 116.0))) (/ (cbrt (+ x 16.0)) (cbrt 116.0)) (/ (* (cbrt (+ x 16.0)) (cbrt (+ x 16.0))) (sqrt 116.0)) (/ (cbrt (+ x 16.0)) (sqrt 116.0)) (* (cbrt (+ x 16.0)) (cbrt (+ x 16.0))) (/ (cbrt (+ x 16.0)) 116.0) (/ (sqrt (+ x 16.0)) (* (cbrt 116.0) (cbrt 116.0))) (/ (sqrt (+ x 16.0)) (cbrt 116.0)) (/ (sqrt (+ x 16.0)) (sqrt 116.0)) (/ (sqrt (+ x 16.0)) (sqrt 116.0)) (sqrt (+ x 16.0)) (/ (sqrt (+ x 16.0)) 116.0) (/ 1 (* (cbrt 116.0) (cbrt 116.0))) (/ (+ x 16.0) (cbrt 116.0)) (/ 1 (sqrt 116.0)) (/ (+ x 16.0) (sqrt 116.0)) 1 (/ (+ x 16.0) 116.0) (/ 1 (* (cbrt 116.0) (cbrt 116.0))) (/ (+ x 16.0) (cbrt 116.0)) (/ 1 (sqrt 116.0)) (/ (+ x 16.0) (sqrt 116.0)) 1 (/ (+ x 16.0) 116.0) (/ 1 116.0) (/ 116.0 (+ x 16.0)) (/ (+ x 16.0) (* (cbrt 116.0) (cbrt 116.0))) (/ (+ x 16.0) (sqrt 116.0)) (+ x 16.0) (/ 116.0 (cbrt (+ x 16.0))) (/ 116.0 (sqrt (+ x 16.0))) (/ 116.0 (+ x 16.0)) (/ 116.0 (+ x 16.0)) (* (+ (* 16.0 (- 16.0 x)) (* x x)) 116.0) (* 116.0 (- x 16.0)) (+ (* 0.008620689655172414 x) 0.13793103448275862) (+ (* 0.008620689655172414 x) 0.13793103448275862) (+ (* 0.008620689655172414 x) 0.13793103448275862) 6.694 * * * [progress]: adding candidates to table 6.744 * * [progress]: iteration 2 / 4 6.744 * * * [progress]: picking best candidate 6.747 * * * * [pick]: Picked # 6.747 * * * [progress]: localizing error 6.751 * * * [progress]: generating rewritten candidates 6.751 * * * * [progress]: [ 1 / 1 ] rewriting at (2) 6.755 * * * [progress]: generating series expansions 6.755 * * * * [progress]: [ 1 / 1 ] generating series at (2) 6.755 * [approximate]: Taking taylor expansion of (+ (* 0.008620689655172414 x) 0.13793103448275862) in (x) around 0 6.755 * [taylor]: Taking taylor expansion of (+ (* 0.008620689655172414 x) 0.13793103448275862) in x 6.755 * [taylor]: Taking taylor expansion of (* 0.008620689655172414 x) in x 6.755 * [taylor]: Taking taylor expansion of 0.008620689655172414 in x 6.756 * [taylor]: Taking taylor expansion of x in x 6.756 * [taylor]: Taking taylor expansion of 0.13793103448275862 in x 6.756 * [taylor]: Taking taylor expansion of (+ (* 0.008620689655172414 x) 0.13793103448275862) in x 6.756 * [taylor]: Taking taylor expansion of (* 0.008620689655172414 x) in x 6.756 * [taylor]: Taking taylor expansion of 0.008620689655172414 in x 6.756 * [taylor]: Taking taylor expansion of x in x 6.756 * [taylor]: Taking taylor expansion of 0.13793103448275862 in x 6.756 * [approximate]: Taking taylor expansion of (+ (* 0.008620689655172414 (/ 1 x)) 0.13793103448275862) in (x) around 0 6.756 * [taylor]: Taking taylor expansion of (+ (* 0.008620689655172414 (/ 1 x)) 0.13793103448275862) in x 6.756 * [taylor]: Taking taylor expansion of (* 0.008620689655172414 (/ 1 x)) in x 6.756 * [taylor]: Taking taylor expansion of 0.008620689655172414 in x 6.756 * [taylor]: Taking taylor expansion of (/ 1 x) in x 6.756 * [taylor]: Taking taylor expansion of x in x 6.756 * [taylor]: Taking taylor expansion of 0.13793103448275862 in x 6.757 * [taylor]: Taking taylor expansion of (+ (* 0.008620689655172414 (/ 1 x)) 0.13793103448275862) in x 6.757 * [taylor]: Taking taylor expansion of (* 0.008620689655172414 (/ 1 x)) in x 6.757 * [taylor]: Taking taylor expansion of 0.008620689655172414 in x 6.757 * [taylor]: Taking taylor expansion of (/ 1 x) in x 6.757 * [taylor]: Taking taylor expansion of x in x 6.757 * [taylor]: Taking taylor expansion of 0.13793103448275862 in x 6.758 * [approximate]: Taking taylor expansion of (- 0.13793103448275862 (* 0.008620689655172414 (/ 1 x))) in (x) around 0 6.758 * [taylor]: Taking taylor expansion of (- 0.13793103448275862 (* 0.008620689655172414 (/ 1 x))) in x 6.758 * [taylor]: Taking taylor expansion of 0.13793103448275862 in x 6.758 * [taylor]: Taking taylor expansion of (* 0.008620689655172414 (/ 1 x)) in x 6.758 * [taylor]: Taking taylor expansion of 0.008620689655172414 in x 6.758 * [taylor]: Taking taylor expansion of (/ 1 x) in x 6.758 * [taylor]: Taking taylor expansion of x in x 6.758 * [taylor]: Taking taylor expansion of (- 0.13793103448275862 (* 0.008620689655172414 (/ 1 x))) in x 6.758 * [taylor]: Taking taylor expansion of 0.13793103448275862 in x 6.758 * [taylor]: Taking taylor expansion of (* 0.008620689655172414 (/ 1 x)) in x 6.758 * [taylor]: Taking taylor expansion of 0.008620689655172414 in x 6.758 * [taylor]: Taking taylor expansion of (/ 1 x) in x 6.758 * [taylor]: Taking taylor expansion of x in x 6.759 * * * [progress]: simplifying candidates 6.760 * [simplify]: Simplifying using # : (* (exp (* 0.008620689655172414 x)) (exp 0.13793103448275862)) (log (+ (* 0.008620689655172414 x) 0.13793103448275862)) (exp (+ (* 0.008620689655172414 x) 0.13793103448275862)) (* (cbrt (+ (* 0.008620689655172414 x) 0.13793103448275862)) (cbrt (+ (* 0.008620689655172414 x) 0.13793103448275862))) (cbrt (+ (* 0.008620689655172414 x) 0.13793103448275862)) (* (* (+ (* 0.008620689655172414 x) 0.13793103448275862) (+ (* 0.008620689655172414 x) 0.13793103448275862)) (+ (* 0.008620689655172414 x) 0.13793103448275862)) (sqrt (+ (* 0.008620689655172414 x) 0.13793103448275862)) (sqrt (+ (* 0.008620689655172414 x) 0.13793103448275862)) (+ (pow (* 0.008620689655172414 x) 3) (pow 0.13793103448275862 3)) (+ (* (* 0.008620689655172414 x) (* 0.008620689655172414 x)) (- (* 0.13793103448275862 0.13793103448275862) (* (* 0.008620689655172414 x) 0.13793103448275862))) (- (* (* 0.008620689655172414 x) (* 0.008620689655172414 x)) (* 0.13793103448275862 0.13793103448275862)) (- (* 0.008620689655172414 x) 0.13793103448275862) (+ (* 0.008620689655172414 x) 0.13793103448275862) (+ (* 0.008620689655172414 x) 0.13793103448275862) (+ (* 0.008620689655172414 x) 0.13793103448275862) 6.760 * * [simplify]: iteration 0 : 7 enodes (cost 7 ) 6.761 * * [simplify]: iteration 1 : 13 enodes (cost 6 ) 6.763 * * [simplify]: iteration 2 : 20 enodes (cost 6 ) 6.765 * * [simplify]: iteration 3 : 32 enodes (cost 6 ) 6.770 * * [simplify]: iteration 4 : 67 enodes (cost 6 ) 6.782 * * [simplify]: iteration 5 : 154 enodes (cost 6 ) 6.847 * * [simplify]: iteration 6 : 405 enodes (cost 6 ) 7.179 * * [simplify]: iteration 7 : 1261 enodes (cost 6 ) 9.967 * * [simplify]: iteration 8 : 4687 enodes (cost 6 ) 12.079 * * [simplify]: iteration done : 5000 enodes (cost 6 ) 12.080 * * [simplify]: iteration 0 : 6 enodes (cost 6 ) 12.081 * * [simplify]: iteration 1 : 8 enodes (cost 6 ) 12.082 * * [simplify]: iteration done : 8 enodes (cost 6 ) 12.082 * * [simplify]: iteration 0 : 6 enodes (cost 6 ) 12.083 * * [simplify]: iteration 1 : 11 enodes (cost 6 ) 12.084 * * [simplify]: iteration 2 : 16 enodes (cost 6 ) 12.086 * * [simplify]: iteration 3 : 23 enodes (cost 6 ) 12.089 * * [simplify]: iteration 4 : 41 enodes (cost 6 ) 12.095 * * [simplify]: iteration 5 : 95 enodes (cost 6 ) 12.119 * * [simplify]: iteration 6 : 220 enodes (cost 6 ) 12.218 * * [simplify]: iteration 7 : 590 enodes (cost 6 ) 12.800 * * [simplify]: iteration 8 : 1950 enodes (cost 6 ) 14.175 * * [simplify]: iteration done : 5000 enodes (cost 6 ) 14.176 * * [simplify]: iteration 0 : 7 enodes (cost 13 ) 14.177 * * [simplify]: iteration 1 : 9 enodes (cost 13 ) 14.177 * * [simplify]: iteration done : 9 enodes (cost 13 ) 14.178 * * [simplify]: iteration 0 : 6 enodes (cost 6 ) 14.179 * * [simplify]: iteration 1 : 8 enodes (cost 6 ) 14.180 * * [simplify]: iteration done : 8 enodes (cost 6 ) 14.180 * * [simplify]: iteration 0 : 7 enodes (cost 17 ) 14.181 * * [simplify]: iteration 1 : 22 enodes (cost 17 ) 14.186 * * [simplify]: iteration 2 : 70 enodes (cost 7 ) 14.208 * * [simplify]: iteration 3 : 223 enodes (cost 7 ) 14.305 * * [simplify]: iteration 4 : 603 enodes (cost 7 ) 14.682 * * [simplify]: iteration 5 : 1509 enodes (cost 7 ) 15.995 * * [simplify]: iteration 6 : 3228 enodes (cost 7 ) 19.064 * * [simplify]: iteration done : 5001 enodes (cost 7 ) 19.065 * * [simplify]: iteration 0 : 6 enodes (cost 6 ) 19.065 * * [simplify]: iteration 1 : 8 enodes (cost 6 ) 19.066 * * [simplify]: iteration done : 8 enodes (cost 6 ) 19.067 * * [simplify]: iteration 0 : 6 enodes (cost 6 ) 19.067 * * [simplify]: iteration 1 : 8 enodes (cost 6 ) 19.068 * * [simplify]: iteration done : 8 enodes (cost 6 ) 19.069 * * [simplify]: iteration 0 : 8 enodes (cost 9 ) 19.070 * * [simplify]: iteration 1 : 26 enodes (cost 9 ) 19.075 * * [simplify]: iteration 2 : 64 enodes (cost 9 ) 19.089 * * [simplify]: iteration 3 : 141 enodes (cost 9 ) 19.139 * * [simplify]: iteration 4 : 268 enodes (cost 9 ) 19.274 * * [simplify]: iteration 5 : 709 enodes (cost 9 ) 20.075 * * [simplify]: iteration 6 : 2669 enodes (cost 9 ) 21.652 * * [simplify]: iteration done : 5000 enodes (cost 9 ) 21.653 * * [simplify]: iteration 0 : 9 enodes (cost 17 ) 21.654 * * [simplify]: iteration 1 : 27 enodes (cost 15 ) 21.659 * * [simplify]: iteration 2 : 63 enodes (cost 15 ) 21.671 * * [simplify]: iteration 3 : 107 enodes (cost 13 ) 21.700 * * [simplify]: iteration 4 : 181 enodes (cost 13 ) 21.754 * * [simplify]: iteration 5 : 307 enodes (cost 13 ) 21.905 * * [simplify]: iteration 6 : 470 enodes (cost 13 ) 22.002 * * [simplify]: iteration 7 : 527 enodes (cost 13 ) 22.348 * * [simplify]: iteration 8 : 626 enodes (cost 13 ) 22.567 * * [simplify]: iteration 9 : 730 enodes (cost 13 ) 22.709 * * [simplify]: iteration done : 730 enodes (cost 13 ) 22.710 * * [simplify]: iteration 0 : 7 enodes (cost 11 ) 22.711 * * [simplify]: iteration 1 : 20 enodes (cost 11 ) 22.714 * * [simplify]: iteration 2 : 38 enodes (cost 11 ) 22.720 * * [simplify]: iteration 3 : 53 enodes (cost 11 ) 22.730 * * [simplify]: iteration 4 : 94 enodes (cost 11 ) 22.754 * * [simplify]: iteration 5 : 171 enodes (cost 11 ) 22.803 * * [simplify]: iteration 6 : 259 enodes (cost 11 ) 22.894 * * [simplify]: iteration 7 : 487 enodes (cost 11 ) 23.719 * * [simplify]: iteration 8 : 1905 enodes (cost 11 ) 27.921 * * [simplify]: iteration done : 5001 enodes (cost 11 ) 27.922 * * [simplify]: iteration 0 : 5 enodes (cost 5 ) 27.923 * * [simplify]: iteration 1 : 8 enodes (cost 5 ) 27.924 * * [simplify]: iteration 2 : 9 enodes (cost 5 ) 27.925 * * [simplify]: iteration done : 9 enodes (cost 5 ) 27.926 * * [simplify]: iteration 0 : 5 enodes (cost 5 ) 27.926 * * [simplify]: iteration 1 : 7 enodes (cost 5 ) 27.927 * * [simplify]: iteration done : 7 enodes (cost 5 ) 27.928 * * [simplify]: iteration 0 : 5 enodes (cost 5 ) 27.928 * * [simplify]: iteration 1 : 7 enodes (cost 5 ) 27.929 * * [simplify]: iteration done : 7 enodes (cost 5 ) 27.930 * * [simplify]: iteration 0 : 5 enodes (cost 5 ) 27.930 * * [simplify]: iteration 1 : 7 enodes (cost 5 ) 27.931 * * [simplify]: iteration done : 7 enodes (cost 5 ) 27.931 * [simplify]: Simplified to: (exp (+ (* 0.008620689655172414 x) 0.13793103448275862)) (log (+ (* 0.008620689655172414 x) 0.13793103448275862)) (exp (+ (* 0.008620689655172414 x) 0.13793103448275862)) (* (cbrt (+ (* 0.008620689655172414 x) 0.13793103448275862)) (cbrt (+ (* 0.008620689655172414 x) 0.13793103448275862))) (cbrt (+ (* 0.008620689655172414 x) 0.13793103448275862)) (pow (+ (* 0.008620689655172414 x) 0.13793103448275862) 3) (sqrt (+ (* 0.008620689655172414 x) 0.13793103448275862)) (sqrt (+ (* 0.008620689655172414 x) 0.13793103448275862)) (+ (pow (* 0.008620689655172414 x) 3) (pow 0.13793103448275862 3)) (- (* 0.13793103448275862 0.13793103448275862) (* (* 0.008620689655172414 x) (- 0.13793103448275862 (* 0.008620689655172414 x)))) (* (+ (* 0.008620689655172414 x) 0.13793103448275862) (- (* 0.008620689655172414 x) 0.13793103448275862)) (- (* 0.008620689655172414 x) 0.13793103448275862) (+ (* 0.008620689655172414 x) 0.13793103448275862) (+ (* 0.008620689655172414 x) 0.13793103448275862) (+ (* 0.008620689655172414 x) 0.13793103448275862) 27.931 * * * [progress]: adding candidates to table 27.951 * * [progress]: iteration 3 / 4 27.951 * * * [progress]: picking best candidate 27.953 * * * * [pick]: Picked # 27.953 * * * [progress]: localizing error 27.958 * * * [progress]: generating rewritten candidates 27.958 * * * * [progress]: [ 1 / 2 ] rewriting at (2) 27.968 * * * * [progress]: [ 2 / 2 ] rewriting at (2 2) 27.980 * * * [progress]: generating series expansions 27.980 * * * * [progress]: [ 1 / 2 ] generating series at (2) 27.980 * [approximate]: Taking taylor expansion of (* 0.008620689655172414 (+ x 16.0)) in (x) around 0 27.980 * [taylor]: Taking taylor expansion of (* 0.008620689655172414 (+ x 16.0)) in x 27.980 * [taylor]: Taking taylor expansion of 0.008620689655172414 in x 27.980 * [taylor]: Taking taylor expansion of (+ x 16.0) in x 27.980 * [taylor]: Taking taylor expansion of x in x 27.980 * [taylor]: Taking taylor expansion of 16.0 in x 27.980 * [taylor]: Taking taylor expansion of (* 0.008620689655172414 (+ x 16.0)) in x 27.980 * [taylor]: Taking taylor expansion of 0.008620689655172414 in x 27.980 * [taylor]: Taking taylor expansion of (+ x 16.0) in x 27.980 * [taylor]: Taking taylor expansion of x in x 27.980 * [taylor]: Taking taylor expansion of 16.0 in x 27.981 * [approximate]: Taking taylor expansion of (* 0.008620689655172414 (+ (/ 1 x) 16.0)) in (x) around 0 27.981 * [taylor]: Taking taylor expansion of (* 0.008620689655172414 (+ (/ 1 x) 16.0)) in x 27.981 * [taylor]: Taking taylor expansion of 0.008620689655172414 in x 27.981 * [taylor]: Taking taylor expansion of (+ (/ 1 x) 16.0) in x 27.981 * [taylor]: Taking taylor expansion of (/ 1 x) in x 27.981 * [taylor]: Taking taylor expansion of x in x 27.981 * [taylor]: Taking taylor expansion of 16.0 in x 27.981 * [taylor]: Taking taylor expansion of (* 0.008620689655172414 (+ (/ 1 x) 16.0)) in x 27.981 * [taylor]: Taking taylor expansion of 0.008620689655172414 in x 27.981 * [taylor]: Taking taylor expansion of (+ (/ 1 x) 16.0) in x 27.981 * [taylor]: Taking taylor expansion of (/ 1 x) in x 27.981 * [taylor]: Taking taylor expansion of x in x 27.981 * [taylor]: Taking taylor expansion of 16.0 in x 27.983 * [approximate]: Taking taylor expansion of (* 0.008620689655172414 (- 16.0 (/ 1 x))) in (x) around 0 27.983 * [taylor]: Taking taylor expansion of (* 0.008620689655172414 (- 16.0 (/ 1 x))) in x 27.983 * [taylor]: Taking taylor expansion of 0.008620689655172414 in x 27.983 * [taylor]: Taking taylor expansion of (- 16.0 (/ 1 x)) in x 27.983 * [taylor]: Taking taylor expansion of 16.0 in x 27.983 * [taylor]: Taking taylor expansion of (/ 1 x) in x 27.983 * [taylor]: Taking taylor expansion of x in x 27.983 * [taylor]: Taking taylor expansion of (* 0.008620689655172414 (- 16.0 (/ 1 x))) in x 27.983 * [taylor]: Taking taylor expansion of 0.008620689655172414 in x 27.983 * [taylor]: Taking taylor expansion of (- 16.0 (/ 1 x)) in x 27.983 * [taylor]: Taking taylor expansion of 16.0 in x 27.983 * [taylor]: Taking taylor expansion of (/ 1 x) in x 27.983 * [taylor]: Taking taylor expansion of x in x 27.985 * * * * [progress]: [ 2 / 2 ] generating series at (2 2) 27.985 * [approximate]: Taking taylor expansion of (/ 116.0 (+ x 16.0)) in (x) around 0 27.985 * [taylor]: Taking taylor expansion of (/ 116.0 (+ x 16.0)) in x 27.985 * [taylor]: Taking taylor expansion of 116.0 in x 27.985 * [taylor]: Taking taylor expansion of (+ x 16.0) in x 27.985 * [taylor]: Taking taylor expansion of x in x 27.985 * [taylor]: Taking taylor expansion of 16.0 in x 27.985 * [taylor]: Taking taylor expansion of (/ 116.0 (+ x 16.0)) in x 27.985 * [taylor]: Taking taylor expansion of 116.0 in x 27.985 * [taylor]: Taking taylor expansion of (+ x 16.0) in x 27.985 * [taylor]: Taking taylor expansion of x in x 27.985 * [taylor]: Taking taylor expansion of 16.0 in x 27.985 * [approximate]: Taking taylor expansion of (/ 116.0 (+ (/ 1 x) 16.0)) in (x) around 0 27.985 * [taylor]: Taking taylor expansion of (/ 116.0 (+ (/ 1 x) 16.0)) in x 27.985 * [taylor]: Taking taylor expansion of 116.0 in x 27.985 * [taylor]: Taking taylor expansion of (+ (/ 1 x) 16.0) in x 27.985 * [taylor]: Taking taylor expansion of (/ 1 x) in x 27.985 * [taylor]: Taking taylor expansion of x in x 27.986 * [taylor]: Taking taylor expansion of 16.0 in x 27.986 * [taylor]: Taking taylor expansion of (/ 116.0 (+ (/ 1 x) 16.0)) in x 27.986 * [taylor]: Taking taylor expansion of 116.0 in x 27.986 * [taylor]: Taking taylor expansion of (+ (/ 1 x) 16.0) in x 27.986 * [taylor]: Taking taylor expansion of (/ 1 x) in x 27.986 * [taylor]: Taking taylor expansion of x in x 27.986 * [taylor]: Taking taylor expansion of 16.0 in x 27.986 * [approximate]: Taking taylor expansion of (/ 116.0 (- 16.0 (/ 1 x))) in (x) around 0 27.986 * [taylor]: Taking taylor expansion of (/ 116.0 (- 16.0 (/ 1 x))) in x 27.986 * [taylor]: Taking taylor expansion of 116.0 in x 27.986 * [taylor]: Taking taylor expansion of (- 16.0 (/ 1 x)) in x 27.986 * [taylor]: Taking taylor expansion of 16.0 in x 27.986 * [taylor]: Taking taylor expansion of (/ 1 x) in x 27.986 * [taylor]: Taking taylor expansion of x in x 27.986 * [taylor]: Taking taylor expansion of (/ 116.0 (- 16.0 (/ 1 x))) in x 27.986 * [taylor]: Taking taylor expansion of 116.0 in x 27.986 * [taylor]: Taking taylor expansion of (- 16.0 (/ 1 x)) in x 27.986 * [taylor]: Taking taylor expansion of 16.0 in x 27.987 * [taylor]: Taking taylor expansion of (/ 1 x) in x 27.987 * [taylor]: Taking taylor expansion of x in x 27.987 * * * [progress]: simplifying candidates 27.989 * [simplify]: Simplifying using # : (neg 1) (neg (- (log 116.0) (log (+ x 16.0)))) (neg (log (/ 116.0 (+ x 16.0)))) (- 0 (- (log 116.0) (log (+ x 16.0)))) (- 0 (log (/ 116.0 (+ x 16.0)))) (- (log 1) (- (log 116.0) (log (+ x 16.0)))) (- (log 1) (log (/ 116.0 (+ x 16.0)))) (log (/ 1 (/ 116.0 (+ x 16.0)))) (exp (/ 1 (/ 116.0 (+ x 16.0)))) (/ (* (* 1 1) 1) (/ (* (* 116.0 116.0) 116.0) (* (* (+ x 16.0) (+ x 16.0)) (+ x 16.0)))) (/ (* (* 1 1) 1) (* (* (/ 116.0 (+ x 16.0)) (/ 116.0 (+ x 16.0))) (/ 116.0 (+ x 16.0)))) (* (cbrt (/ 1 (/ 116.0 (+ x 16.0)))) (cbrt (/ 1 (/ 116.0 (+ x 16.0))))) (cbrt (/ 1 (/ 116.0 (+ x 16.0)))) (* (* (/ 1 (/ 116.0 (+ x 16.0))) (/ 1 (/ 116.0 (+ x 16.0)))) (/ 1 (/ 116.0 (+ x 16.0)))) (sqrt (/ 1 (/ 116.0 (+ x 16.0)))) (sqrt (/ 1 (/ 116.0 (+ x 16.0)))) (neg 1) (neg (/ 116.0 (+ x 16.0))) (/ (* (cbrt 1) (cbrt 1)) (* (cbrt (/ 116.0 (+ x 16.0))) (cbrt (/ 116.0 (+ x 16.0))))) (/ (cbrt 1) (cbrt (/ 116.0 (+ x 16.0)))) (/ (* (cbrt 1) (cbrt 1)) (sqrt (/ 116.0 (+ x 16.0)))) (/ (cbrt 1) (sqrt (/ 116.0 (+ x 16.0)))) (/ (* (cbrt 1) (cbrt 1)) (/ (* (cbrt 116.0) (cbrt 116.0)) (* (cbrt (+ x 16.0)) (cbrt (+ x 16.0))))) (/ (cbrt 1) (/ (cbrt 116.0) (cbrt (+ x 16.0)))) (/ (* (cbrt 1) (cbrt 1)) (/ (* (cbrt 116.0) (cbrt 116.0)) (sqrt (+ x 16.0)))) (/ (cbrt 1) (/ (cbrt 116.0) (sqrt (+ x 16.0)))) (/ (* (cbrt 1) (cbrt 1)) (/ (* (cbrt 116.0) (cbrt 116.0)) 1)) (/ (cbrt 1) (/ (cbrt 116.0) (+ x 16.0))) (/ (* (cbrt 1) (cbrt 1)) (/ (* (cbrt 116.0) (cbrt 116.0)) 1)) (/ (cbrt 1) (/ (cbrt 116.0) (+ x 16.0))) (/ (* (cbrt 1) (cbrt 1)) (/ (sqrt 116.0) (* (cbrt (+ x 16.0)) (cbrt (+ x 16.0))))) (/ (cbrt 1) (/ (sqrt 116.0) (cbrt (+ x 16.0)))) (/ (* (cbrt 1) (cbrt 1)) (/ (sqrt 116.0) (sqrt (+ x 16.0)))) (/ (cbrt 1) (/ (sqrt 116.0) (sqrt (+ x 16.0)))) (/ (* (cbrt 1) (cbrt 1)) (/ (sqrt 116.0) 1)) (/ (cbrt 1) (/ (sqrt 116.0) (+ x 16.0))) (/ (* (cbrt 1) (cbrt 1)) (/ (sqrt 116.0) 1)) (/ (cbrt 1) (/ (sqrt 116.0) (+ x 16.0))) (/ (* (cbrt 1) (cbrt 1)) (/ 1 (* (cbrt (+ x 16.0)) (cbrt (+ x 16.0))))) (/ (cbrt 1) (/ 116.0 (cbrt (+ x 16.0)))) (/ (* (cbrt 1) (cbrt 1)) (/ 1 (sqrt (+ x 16.0)))) (/ (cbrt 1) (/ 116.0 (sqrt (+ x 16.0)))) (/ (* (cbrt 1) (cbrt 1)) (/ 1 1)) (/ (cbrt 1) (/ 116.0 (+ x 16.0))) (/ (* (cbrt 1) (cbrt 1)) (/ 1 1)) (/ (cbrt 1) (/ 116.0 (+ x 16.0))) (/ (* (cbrt 1) (cbrt 1)) 1) (/ (cbrt 1) (/ 116.0 (+ x 16.0))) (/ (* (cbrt 1) (cbrt 1)) 116.0) (/ (cbrt 1) (/ 1 (+ x 16.0))) (/ (* (cbrt 1) (cbrt 1)) (/ 116.0 (+ (pow x 3) (pow 16.0 3)))) (/ (cbrt 1) (+ (* x x) (- (* 16.0 16.0) (* x 16.0)))) (/ (* (cbrt 1) (cbrt 1)) (/ 116.0 (- (* x x) (* 16.0 16.0)))) (/ (cbrt 1) (- x 16.0)) (/ (sqrt 1) (* (cbrt (/ 116.0 (+ x 16.0))) (cbrt (/ 116.0 (+ x 16.0))))) (/ (sqrt 1) (cbrt (/ 116.0 (+ x 16.0)))) (/ (sqrt 1) (sqrt (/ 116.0 (+ x 16.0)))) (/ (sqrt 1) (sqrt (/ 116.0 (+ x 16.0)))) (/ (sqrt 1) (/ (* (cbrt 116.0) (cbrt 116.0)) (* (cbrt (+ x 16.0)) (cbrt (+ x 16.0))))) (/ (sqrt 1) (/ (cbrt 116.0) (cbrt (+ x 16.0)))) (/ (sqrt 1) (/ (* (cbrt 116.0) (cbrt 116.0)) (sqrt (+ x 16.0)))) (/ (sqrt 1) (/ (cbrt 116.0) (sqrt (+ x 16.0)))) (/ (sqrt 1) (/ (* (cbrt 116.0) (cbrt 116.0)) 1)) (/ (sqrt 1) (/ (cbrt 116.0) (+ x 16.0))) (/ (sqrt 1) (/ (* (cbrt 116.0) (cbrt 116.0)) 1)) (/ (sqrt 1) (/ (cbrt 116.0) (+ x 16.0))) (/ (sqrt 1) (/ (sqrt 116.0) (* (cbrt (+ x 16.0)) (cbrt (+ x 16.0))))) (/ (sqrt 1) (/ (sqrt 116.0) (cbrt (+ x 16.0)))) (/ (sqrt 1) (/ (sqrt 116.0) (sqrt (+ x 16.0)))) (/ (sqrt 1) (/ (sqrt 116.0) (sqrt (+ x 16.0)))) (/ (sqrt 1) (/ (sqrt 116.0) 1)) (/ (sqrt 1) (/ (sqrt 116.0) (+ x 16.0))) (/ (sqrt 1) (/ (sqrt 116.0) 1)) (/ (sqrt 1) (/ (sqrt 116.0) (+ x 16.0))) (/ (sqrt 1) (/ 1 (* (cbrt (+ x 16.0)) (cbrt (+ x 16.0))))) (/ (sqrt 1) (/ 116.0 (cbrt (+ x 16.0)))) (/ (sqrt 1) (/ 1 (sqrt (+ x 16.0)))) (/ (sqrt 1) (/ 116.0 (sqrt (+ x 16.0)))) (/ (sqrt 1) (/ 1 1)) (/ (sqrt 1) (/ 116.0 (+ x 16.0))) (/ (sqrt 1) (/ 1 1)) (/ (sqrt 1) (/ 116.0 (+ x 16.0))) (/ (sqrt 1) 1) (/ (sqrt 1) (/ 116.0 (+ x 16.0))) (/ (sqrt 1) 116.0) (/ (sqrt 1) (/ 1 (+ x 16.0))) (/ (sqrt 1) (/ 116.0 (+ (pow x 3) (pow 16.0 3)))) (/ (sqrt 1) (+ (* x x) (- (* 16.0 16.0) (* x 16.0)))) (/ (sqrt 1) (/ 116.0 (- (* x x) (* 16.0 16.0)))) (/ (sqrt 1) (- x 16.0)) (/ 1 (* (cbrt (/ 116.0 (+ x 16.0))) (cbrt (/ 116.0 (+ x 16.0))))) (/ 1 (cbrt (/ 116.0 (+ x 16.0)))) (/ 1 (sqrt (/ 116.0 (+ x 16.0)))) (/ 1 (sqrt (/ 116.0 (+ x 16.0)))) (/ 1 (/ (* (cbrt 116.0) (cbrt 116.0)) (* (cbrt (+ x 16.0)) (cbrt (+ x 16.0))))) (/ 1 (/ (cbrt 116.0) (cbrt (+ x 16.0)))) (/ 1 (/ (* (cbrt 116.0) (cbrt 116.0)) (sqrt (+ x 16.0)))) (/ 1 (/ (cbrt 116.0) (sqrt (+ x 16.0)))) (/ 1 (/ (* (cbrt 116.0) (cbrt 116.0)) 1)) (/ 1 (/ (cbrt 116.0) (+ x 16.0))) (/ 1 (/ (* (cbrt 116.0) (cbrt 116.0)) 1)) (/ 1 (/ (cbrt 116.0) (+ x 16.0))) (/ 1 (/ (sqrt 116.0) (* (cbrt (+ x 16.0)) (cbrt (+ x 16.0))))) (/ 1 (/ (sqrt 116.0) (cbrt (+ x 16.0)))) (/ 1 (/ (sqrt 116.0) (sqrt (+ x 16.0)))) (/ 1 (/ (sqrt 116.0) (sqrt (+ x 16.0)))) (/ 1 (/ (sqrt 116.0) 1)) (/ 1 (/ (sqrt 116.0) (+ x 16.0))) (/ 1 (/ (sqrt 116.0) 1)) (/ 1 (/ (sqrt 116.0) (+ x 16.0))) (/ 1 (/ 1 (* (cbrt (+ x 16.0)) (cbrt (+ x 16.0))))) (/ 1 (/ 116.0 (cbrt (+ x 16.0)))) (/ 1 (/ 1 (sqrt (+ x 16.0)))) (/ 1 (/ 116.0 (sqrt (+ x 16.0)))) (/ 1 (/ 1 1)) (/ 1 (/ 116.0 (+ x 16.0))) (/ 1 (/ 1 1)) (/ 1 (/ 116.0 (+ x 16.0))) (/ 1 1) (/ 1 (/ 116.0 (+ x 16.0))) (/ 1 116.0) (/ 1 (/ 1 (+ x 16.0))) (/ 1 (/ 116.0 (+ (pow x 3) (pow 16.0 3)))) (/ 1 (+ (* x x) (- (* 16.0 16.0) (* x 16.0)))) (/ 1 (/ 116.0 (- (* x x) (* 16.0 16.0)))) (/ 1 (- x 16.0)) (/ 1 (/ 116.0 (+ x 16.0))) (/ (/ 116.0 (+ x 16.0)) 1) (/ 1 (* (cbrt (/ 116.0 (+ x 16.0))) (cbrt (/ 116.0 (+ x 16.0))))) (/ 1 (sqrt (/ 116.0 (+ x 16.0)))) (/ 1 (/ (* (cbrt 116.0) (cbrt 116.0)) (* (cbrt (+ x 16.0)) (cbrt (+ x 16.0))))) (/ 1 (/ (* (cbrt 116.0) (cbrt 116.0)) (sqrt (+ x 16.0)))) (/ 1 (/ (* (cbrt 116.0) (cbrt 116.0)) 1)) (/ 1 (/ (* (cbrt 116.0) (cbrt 116.0)) 1)) (/ 1 (/ (sqrt 116.0) (* (cbrt (+ x 16.0)) (cbrt (+ x 16.0))))) (/ 1 (/ (sqrt 116.0) (sqrt (+ x 16.0)))) (/ 1 (/ (sqrt 116.0) 1)) (/ 1 (/ (sqrt 116.0) 1)) (/ 1 (/ 1 (* (cbrt (+ x 16.0)) (cbrt (+ x 16.0))))) (/ 1 (/ 1 (sqrt (+ x 16.0)))) (/ 1 (/ 1 1)) (/ 1 (/ 1 1)) (/ 1 1) (/ 1 116.0) (/ 1 (/ 116.0 (+ (pow x 3) (pow 16.0 3)))) (/ 1 (/ 116.0 (- (* x x) (* 16.0 16.0)))) (/ (/ 116.0 (+ x 16.0)) (cbrt 1)) (/ (/ 116.0 (+ x 16.0)) (sqrt 1)) (/ (/ 116.0 (+ x 16.0)) 1) (/ 1 116.0) (- (log 116.0) (log (+ x 16.0))) (log (/ 116.0 (+ x 16.0))) (exp (/ 116.0 (+ x 16.0))) (/ (* (* 116.0 116.0) 116.0) (* (* (+ x 16.0) (+ x 16.0)) (+ x 16.0))) (* (cbrt (/ 116.0 (+ x 16.0))) (cbrt (/ 116.0 (+ x 16.0)))) (cbrt (/ 116.0 (+ x 16.0))) (* (* (/ 116.0 (+ x 16.0)) (/ 116.0 (+ x 16.0))) (/ 116.0 (+ x 16.0))) (sqrt (/ 116.0 (+ x 16.0))) (sqrt (/ 116.0 (+ x 16.0))) (neg 116.0) (neg (+ x 16.0)) (/ (* (cbrt 116.0) (cbrt 116.0)) (* (cbrt (+ x 16.0)) (cbrt (+ x 16.0)))) (/ (cbrt 116.0) (cbrt (+ x 16.0))) (/ (* (cbrt 116.0) (cbrt 116.0)) (sqrt (+ x 16.0))) (/ (cbrt 116.0) (sqrt (+ x 16.0))) (/ (* (cbrt 116.0) (cbrt 116.0)) 1) (/ (cbrt 116.0) (+ x 16.0)) (/ (* (cbrt 116.0) (cbrt 116.0)) 1) (/ (cbrt 116.0) (+ x 16.0)) (/ (sqrt 116.0) (* (cbrt (+ x 16.0)) (cbrt (+ x 16.0)))) (/ (sqrt 116.0) (cbrt (+ x 16.0))) (/ (sqrt 116.0) (sqrt (+ x 16.0))) (/ (sqrt 116.0) (sqrt (+ x 16.0))) (/ (sqrt 116.0) 1) (/ (sqrt 116.0) (+ x 16.0)) (/ (sqrt 116.0) 1) (/ (sqrt 116.0) (+ x 16.0)) (/ 1 (* (cbrt (+ x 16.0)) (cbrt (+ x 16.0)))) (/ 116.0 (cbrt (+ x 16.0))) (/ 1 (sqrt (+ x 16.0))) (/ 116.0 (sqrt (+ x 16.0))) (/ 1 1) (/ 116.0 (+ x 16.0)) (/ 1 1) (/ 116.0 (+ x 16.0)) (/ 1 (+ x 16.0)) (/ (+ x 16.0) 116.0) (/ 116.0 (* (cbrt (+ x 16.0)) (cbrt (+ x 16.0)))) (/ 116.0 (sqrt (+ x 16.0))) (/ 116.0 1) (/ 116.0 1) (/ (+ x 16.0) (cbrt 116.0)) (/ (+ x 16.0) (sqrt 116.0)) (/ (+ x 16.0) 116.0) (/ 116.0 (+ (pow x 3) (pow 16.0 3))) (/ 116.0 (- (* x x) (* 16.0 16.0))) (+ (* 0.008620689655172414 x) 0.13793103448275862) (+ (* 0.008620689655172414 x) 0.13793103448275862) (+ (* 0.008620689655172414 x) 0.13793103448275862) (- (+ (* 0.0283203125 (pow x 2)) 7.25) (* 0.453125 x)) (- (+ (* 116.0 (/ 1 x)) (* 29696.0 (/ 1 (pow x 3)))) (* 1856.0 (/ 1 (pow x 2)))) (- (+ (* 116.0 (/ 1 x)) (* 29696.0 (/ 1 (pow x 3)))) (* 1856.0 (/ 1 (pow x 2)))) 27.990 * * [simplify]: iteration 0 : 2 enodes (cost 2 ) 27.990 * * [simplify]: iteration 1 : 5 enodes (cost 1 ) 27.990 * * [simplify]: iteration done : 5 enodes (cost 1 ) 27.991 * * [simplify]: iteration 0 : 8 enodes (cost 8 ) 27.992 * * [simplify]: iteration 1 : 11 enodes (cost 8 ) 27.993 * * [simplify]: iteration 2 : 15 enodes (cost 8 ) 27.994 * * [simplify]: iteration 3 : 17 enodes (cost 8 ) 27.996 * * [simplify]: iteration 4 : 18 enodes (cost 7 ) 27.998 * * [simplify]: iteration done : 18 enodes (cost 7 ) 27.998 * * [simplify]: iteration 0 : 7 enodes (cost 7 ) 27.999 * * [simplify]: iteration 1 : 11 enodes (cost 7 ) 28.000 * * [simplify]: iteration 2 : 13 enodes (cost 7 ) 28.001 * * [simplify]: iteration 3 : 17 enodes (cost 7 ) 28.003 * * [simplify]: iteration 4 : 19 enodes (cost 7 ) 28.005 * * [simplify]: iteration 5 : 20 enodes (cost 7 ) 28.006 * * [simplify]: iteration done : 20 enodes (cost 7 ) 28.007 * * [simplify]: iteration 0 : 9 enodes (cost 9 ) 28.008 * * [simplify]: iteration 1 : 16 enodes (cost 8 ) 28.010 * * [simplify]: iteration 2 : 29 enodes (cost 8 ) 28.019 * * [simplify]: iteration 3 : 48 enodes (cost 7 ) 28.030 * * [simplify]: iteration 4 : 77 enodes (cost 7 ) 28.040 * * [simplify]: iteration 5 : 104 enodes (cost 7 ) 28.050 * * [simplify]: iteration 6 : 113 enodes (cost 7 ) 28.062 * * [simplify]: iteration 7 : 129 enodes (cost 7 ) 28.077 * * [simplify]: iteration done : 129 enodes (cost 7 ) 28.077 * * [simplify]: iteration 0 : 8 enodes (cost 8 ) 28.078 * * [simplify]: iteration 1 : 14 enodes (cost 7 ) 28.080 * * [simplify]: iteration 2 : 22 enodes (cost 7 ) 28.082 * * [simplify]: iteration 3 : 35 enodes (cost 7 ) 28.089 * * [simplify]: iteration 4 : 61 enodes (cost 7 ) 28.100 * * [simplify]: iteration 5 : 91 enodes (cost 7 ) 28.109 * * [simplify]: iteration 6 : 97 enodes (cost 7 ) 28.119 * * [simplify]: iteration 7 : 103 enodes (cost 7 ) 28.137 * * [simplify]: iteration 8 : 119 enodes (cost 7 ) 28.149 * * [simplify]: iteration done : 119 enodes (cost 7 ) 28.149 * * [simplify]: iteration 0 : 10 enodes (cost 10 ) 28.151 * * [simplify]: iteration 1 : 19 enodes (cost 9 ) 28.153 * * [simplify]: iteration 2 : 27 enodes (cost 8 ) 28.158 * * [simplify]: iteration 3 : 52 enodes (cost 7 ) 28.169 * * [simplify]: iteration 4 : 82 enodes (cost 7 ) 28.179 * * [simplify]: iteration 5 : 108 enodes (cost 7 ) 28.193 * * [simplify]: iteration 6 : 118 enodes (cost 7 ) 28.205 * * [simplify]: iteration 7 : 134 enodes (cost 7 ) 28.216 * * [simplify]: iteration done : 134 enodes (cost 7 ) 28.217 * * [simplify]: iteration 0 : 9 enodes (cost 9 ) 28.218 * * [simplify]: iteration 1 : 17 enodes (cost 8 ) 28.219 * * [simplify]: iteration 2 : 22 enodes (cost 7 ) 28.222 * * [simplify]: iteration 3 : 39 enodes (cost 7 ) 28.229 * * [simplify]: iteration 4 : 65 enodes (cost 7 ) 28.240 * * [simplify]: iteration 5 : 95 enodes (cost 7 ) 28.253 * * [simplify]: iteration 6 : 101 enodes (cost 7 ) 28.263 * * [simplify]: iteration 7 : 107 enodes (cost 7 ) 28.277 * * [simplify]: iteration 8 : 123 enodes (cost 7 ) 28.289 * * [simplify]: iteration done : 123 enodes (cost 7 ) 28.289 * * [simplify]: iteration 0 : 8 enodes (cost 8 ) 28.290 * * [simplify]: iteration 1 : 17 enodes (cost 7 ) 28.292 * * [simplify]: iteration 2 : 34 enodes (cost 7 ) 28.297 * * [simplify]: iteration 3 : 60 enodes (cost 6 ) 28.307 * * [simplify]: iteration 4 : 111 enodes (cost 6 ) 28.328 * * [simplify]: iteration 5 : 152 enodes (cost 6 ) 28.345 * * [simplify]: iteration 6 : 167 enodes (cost 6 ) 28.361 * * [simplify]: iteration 7 : 171 enodes (cost 6 ) 28.384 * * [simplify]: iteration 8 : 180 enodes (cost 6 ) 28.402 * * [simplify]: iteration done : 180 enodes (cost 6 ) 28.403 * * [simplify]: iteration 0 : 8 enodes (cost 8 ) 28.404 * * [simplify]: iteration 1 : 13 enodes (cost 8 ) 28.405 * * [simplify]: iteration 2 : 26 enodes (cost 8 ) 28.409 * * [simplify]: iteration 3 : 49 enodes (cost 6 ) 28.418 * * [simplify]: iteration 4 : 107 enodes (cost 6 ) 28.439 * * [simplify]: iteration 5 : 170 enodes (cost 6 ) 28.475 * * [simplify]: iteration 6 : 334 enodes (cost 6 ) 28.632 * * [simplify]: iteration 7 : 823 enodes (cost 6 ) 29.603 * * [simplify]: iteration 8 : 2839 enodes (cost 6 ) 31.573 * * [simplify]: iteration done : 5000 enodes (cost 6 ) 31.574 * * [simplify]: iteration 0 : 13 enodes (cost 23 ) 31.576 * * [simplify]: iteration 1 : 42 enodes (cost 19 ) 31.585 * * [simplify]: iteration 2 : 134 enodes (cost 11 ) 31.642 * * [simplify]: iteration 3 : 473 enodes (cost 9 ) 32.178 * * [simplify]: iteration 4 : 1797 enodes (cost 9 ) 34.236 * * [simplify]: iteration done : 5000 enodes (cost 9 ) 34.237 * * [simplify]: iteration 0 : 11 enodes (cost 23 ) 34.238 * * [simplify]: iteration 1 : 28 enodes (cost 19 ) 34.243 * * [simplify]: iteration 2 : 64 enodes (cost 9 ) 34.264 * * [simplify]: iteration 3 : 224 enodes (cost 9 ) 34.434 * * [simplify]: iteration 4 : 666 enodes (cost 9 ) 35.004 * * [simplify]: iteration 5 : 1431 enodes (cost 7 ) 37.023 * * [simplify]: iteration 6 : 2976 enodes (cost 7 ) 38.963 * * [simplify]: iteration done : 5000 enodes (cost 7 ) 38.964 * * [simplify]: iteration 0 : 9 enodes (cost 17 ) 38.965 * * [simplify]: iteration 1 : 14 enodes (cost 17 ) 38.966 * * [simplify]: iteration 2 : 25 enodes (cost 17 ) 38.970 * * [simplify]: iteration 3 : 38 enodes (cost 13 ) 38.977 * * [simplify]: iteration 4 : 73 enodes (cost 13 ) 38.986 * * [simplify]: iteration 5 : 84 enodes (cost 13 ) 38.998 * * [simplify]: iteration done : 84 enodes (cost 13 ) 38.999 * * [simplify]: iteration 0 : 8 enodes (cost 8 ) 39.000 * * [simplify]: iteration 1 : 13 enodes (cost 8 ) 39.001 * * [simplify]: iteration 2 : 24 enodes (cost 8 ) 39.004 * * [simplify]: iteration 3 : 37 enodes (cost 6 ) 39.012 * * [simplify]: iteration 4 : 72 enodes (cost 6 ) 39.021 * * [simplify]: iteration 5 : 83 enodes (cost 6 ) 39.028 * * [simplify]: iteration done : 83 enodes (cost 6 ) 39.029 * * [simplify]: iteration 0 : 9 enodes (cost 23 ) 39.030 * * [simplify]: iteration 1 : 21 enodes (cost 23 ) 39.034 * * [simplify]: iteration 2 : 67 enodes (cost 9 ) 39.081 * * [simplify]: iteration 3 : 318 enodes (cost 7 ) 39.346 * * [simplify]: iteration 4 : 1011 enodes (cost 7 ) 40.297 * * [simplify]: iteration 5 : 2058 enodes (cost 7 ) 43.650 * * [simplify]: iteration done : 5001 enodes (cost 7 ) 43.650 * * [simplify]: iteration 0 : 8 enodes (cost 8 ) 43.651 * * [simplify]: iteration 1 : 13 enodes (cost 8 ) 43.653 * * [simplify]: iteration 2 : 24 enodes (cost 8 ) 43.656 * * [simplify]: iteration 3 : 37 enodes (cost 6 ) 43.663 * * [simplify]: iteration 4 : 72 enodes (cost 6 ) 43.671 * * [simplify]: iteration 5 : 83 enodes (cost 6 ) 43.678 * * [simplify]: iteration done : 83 enodes (cost 6 ) 43.679 * * [simplify]: iteration 0 : 8 enodes (cost 8 ) 43.680 * * [simplify]: iteration 1 : 13 enodes (cost 8 ) 43.682 * * [simplify]: iteration 2 : 24 enodes (cost 8 ) 43.685 * * [simplify]: iteration 3 : 37 enodes (cost 6 ) 43.692 * * [simplify]: iteration 4 : 72 enodes (cost 6 ) 43.704 * * [simplify]: iteration 5 : 83 enodes (cost 6 ) 43.712 * * [simplify]: iteration done : 83 enodes (cost 6 ) 43.713 * * [simplify]: iteration 0 : 2 enodes (cost 2 ) 43.713 * * [simplify]: iteration 1 : 5 enodes (cost 1 ) 43.713 * * [simplify]: iteration done : 5 enodes (cost 1 ) 43.714 * * [simplify]: iteration 0 : 6 enodes (cost 6 ) 43.715 * * [simplify]: iteration 1 : 9 enodes (cost 6 ) 43.716 * * [simplify]: iteration done : 9 enodes (cost 6 ) 43.716 * * [simplify]: iteration 0 : 11 enodes (cost 19 ) 43.717 * * [simplify]: iteration 1 : 20 enodes (cost 17 ) 43.720 * * [simplify]: iteration 2 : 29 enodes (cost 15 ) 43.723 * * [simplify]: iteration 3 : 35 enodes (cost 15 ) 43.727 * * [simplify]: iteration done : 35 enodes (cost 15 ) 43.727 * * [simplify]: iteration 0 : 9 enodes (cost 9 ) 43.728 * * [simplify]: iteration 1 : 12 enodes (cost 8 ) 43.729 * * [simplify]: iteration done : 12 enodes (cost 8 ) 43.730 * * [simplify]: iteration 0 : 10 enodes (cost 12 ) 43.731 * * [simplify]: iteration 1 : 15 enodes (cost 10 ) 43.732 * * [simplify]: iteration 2 : 17 enodes (cost 8 ) 43.734 * * [simplify]: iteration 3 : 18 enodes (cost 8 ) 43.735 * * [simplify]: iteration done : 18 enodes (cost 8 ) 43.736 * * [simplify]: iteration 0 : 9 enodes (cost 9 ) 43.737 * * [simplify]: iteration 1 : 12 enodes (cost 8 ) 43.738 * * [simplify]: iteration done : 12 enodes (cost 8 ) 43.739 * * [simplify]: iteration 0 : 13 enodes (cost 21 ) 43.740 * * [simplify]: iteration 1 : 26 enodes (cost 19 ) 43.744 * * [simplify]: iteration 2 : 62 enodes (cost 17 ) 43.758 * * [simplify]: iteration 3 : 132 enodes (cost 15 ) 43.800 * * [simplify]: iteration 4 : 188 enodes (cost 15 ) 43.834 * * [simplify]: iteration done : 188 enodes (cost 15 ) 43.835 * * [simplify]: iteration 0 : 10 enodes (cost 10 ) 43.836 * * [simplify]: iteration 1 : 15 enodes (cost 9 ) 43.837 * * [simplify]: iteration 2 : 18 enodes (cost 9 ) 43.839 * * [simplify]: iteration 3 : 19 enodes (cost 7 ) 43.841 * * [simplify]: iteration 4 : 32 enodes (cost 7 ) 43.845 * * [simplify]: iteration 5 : 39 enodes (cost 7 ) 43.849 * * [simplify]: iteration done : 39 enodes (cost 7 ) 43.849 * * [simplify]: iteration 0 : 12 enodes (cost 16 ) 43.851 * * [simplify]: iteration 1 : 21 enodes (cost 14 ) 43.854 * * [simplify]: iteration 2 : 39 enodes (cost 12 ) 43.861 * * [simplify]: iteration 3 : 72 enodes (cost 10 ) 43.874 * * [simplify]: iteration 4 : 93 enodes (cost 10 ) 43.889 * * [simplify]: iteration done : 93 enodes (cost 10 ) 43.890 * * [simplify]: iteration 0 : 10 enodes (cost 10 ) 43.891 * * [simplify]: iteration 1 : 15 enodes (cost 9 ) 43.892 * * [simplify]: iteration 2 : 18 enodes (cost 9 ) 43.894 * * [simplify]: iteration 3 : 19 enodes (cost 7 ) 43.896 * * [simplify]: iteration 4 : 32 enodes (cost 7 ) 43.901 * * [simplify]: iteration 5 : 39 enodes (cost 7 ) 43.904 * * [simplify]: iteration done : 39 enodes (cost 7 ) 43.905 * * [simplify]: iteration 0 : 8 enodes (cost 13 ) 43.906 * * [simplify]: iteration 1 : 16 enodes (cost 7 ) 43.909 * * [simplify]: iteration 2 : 30 enodes (cost 7 ) 43.912 * * [simplify]: iteration 3 : 39 enodes (cost 7 ) 43.915 * * [simplify]: iteration done : 39 enodes (cost 7 ) 43.915 * * [simplify]: iteration 0 : 9 enodes (cost 9 ) 43.916 * * [simplify]: iteration 1 : 14 enodes (cost 8 ) 43.918 * * [simplify]: iteration 2 : 25 enodes (cost 8 ) 43.921 * * [simplify]: iteration 3 : 38 enodes (cost 6 ) 43.928 * * [simplify]: iteration 4 : 73 enodes (cost 6 ) 43.936 * * [simplify]: iteration 5 : 84 enodes (cost 6 ) 43.948 * * [simplify]: iteration done : 84 enodes (cost 6 ) 43.949 * * [simplify]: iteration 0 : 8 enodes (cost 13 ) 43.950 * * [simplify]: iteration 1 : 16 enodes (cost 7 ) 43.952 * * [simplify]: iteration 2 : 30 enodes (cost 7 ) 43.955 * * [simplify]: iteration 3 : 39 enodes (cost 7 ) 43.958 * * [simplify]: iteration done : 39 enodes (cost 7 ) 43.958 * * [simplify]: iteration 0 : 9 enodes (cost 9 ) 43.959 * * [simplify]: iteration 1 : 14 enodes (cost 8 ) 43.961 * * [simplify]: iteration 2 : 25 enodes (cost 8 ) 43.964 * * [simplify]: iteration 3 : 38 enodes (cost 6 ) 43.971 * * [simplify]: iteration 4 : 73 enodes (cost 6 ) 43.980 * * [simplify]: iteration 5 : 84 enodes (cost 6 ) 43.988 * * [simplify]: iteration done : 84 enodes (cost 6 ) 43.988 * * [simplify]: iteration 0 : 12 enodes (cost 18 ) 43.990 * * [simplify]: iteration 1 : 21 enodes (cost 16 ) 43.992 * * [simplify]: iteration 2 : 36 enodes (cost 14 ) 43.997 * * [simplify]: iteration 3 : 56 enodes (cost 12 ) 44.009 * * [simplify]: iteration 4 : 59 enodes (cost 12 ) 44.017 * * [simplify]: iteration done : 59 enodes (cost 12 ) 44.017 * * [simplify]: iteration 0 : 10 enodes (cost 10 ) 44.018 * * [simplify]: iteration 1 : 15 enodes (cost 9 ) 44.020 * * [simplify]: iteration 2 : 18 enodes (cost 9 ) 44.021 * * [simplify]: iteration 3 : 19 enodes (cost 7 ) 44.023 * * [simplify]: iteration 4 : 32 enodes (cost 7 ) 44.028 * * [simplify]: iteration 5 : 39 enodes (cost 7 ) 44.032 * * [simplify]: iteration done : 39 enodes (cost 7 ) 44.032 * * [simplify]: iteration 0 : 11 enodes (cost 13 ) 44.033 * * [simplify]: iteration 1 : 18 enodes (cost 11 ) 44.036 * * [simplify]: iteration 2 : 27 enodes (cost 9 ) 44.039 * * [simplify]: iteration 3 : 35 enodes (cost 7 ) 44.043 * * [simplify]: iteration 4 : 36 enodes (cost 7 ) 44.046 * * [simplify]: iteration done : 36 enodes (cost 7 ) 44.047 * * [simplify]: iteration 0 : 10 enodes (cost 10 ) 44.048 * * [simplify]: iteration 1 : 15 enodes (cost 9 ) 44.049 * * [simplify]: iteration 2 : 18 enodes (cost 9 ) 44.050 * * [simplify]: iteration 3 : 19 enodes (cost 7 ) 44.053 * * [simplify]: iteration 4 : 32 enodes (cost 7 ) 44.057 * * [simplify]: iteration 5 : 39 enodes (cost 7 ) 44.064 * * [simplify]: iteration done : 39 enodes (cost 7 ) 44.065 * * [simplify]: iteration 0 : 7 enodes (cost 10 ) 44.066 * * [simplify]: iteration 1 : 13 enodes (cost 4 ) 44.068 * * [simplify]: iteration 2 : 18 enodes (cost 4 ) 44.069 * * [simplify]: iteration done : 18 enodes (cost 4 ) 44.070 * * [simplify]: iteration 0 : 9 enodes (cost 9 ) 44.071 * * [simplify]: iteration 1 : 14 enodes (cost 8 ) 44.072 * * [simplify]: iteration 2 : 25 enodes (cost 8 ) 44.075 * * [simplify]: iteration 3 : 38 enodes (cost 6 ) 44.082 * * [simplify]: iteration 4 : 73 enodes (cost 6 ) 44.091 * * [simplify]: iteration 5 : 84 enodes (cost 6 ) 44.099 * * [simplify]: iteration done : 84 enodes (cost 6 ) 44.099 * * [simplify]: iteration 0 : 7 enodes (cost 10 ) 44.100 * * [simplify]: iteration 1 : 13 enodes (cost 4 ) 44.102 * * [simplify]: iteration 2 : 18 enodes (cost 4 ) 44.103 * * [simplify]: iteration done : 18 enodes (cost 4 ) 44.104 * * [simplify]: iteration 0 : 9 enodes (cost 9 ) 44.104 * * [simplify]: iteration 1 : 14 enodes (cost 8 ) 44.106 * * [simplify]: iteration 2 : 25 enodes (cost 8 ) 44.109 * * [simplify]: iteration 3 : 38 enodes (cost 6 ) 44.116 * * [simplify]: iteration 4 : 73 enodes (cost 6 ) 44.129 * * [simplify]: iteration 5 : 84 enodes (cost 6 ) 44.137 * * [simplify]: iteration done : 84 enodes (cost 6 ) 44.138 * * [simplify]: iteration 0 : 10 enodes (cost 17 ) 44.139 * * [simplify]: iteration 1 : 19 enodes (cost 15 ) 44.142 * * [simplify]: iteration 2 : 34 enodes (cost 11 ) 44.147 * * [simplify]: iteration 3 : 50 enodes (cost 9 ) 44.152 * * [simplify]: iteration 4 : 58 enodes (cost 9 ) 44.159 * * [simplify]: iteration 5 : 59 enodes (cost 9 ) 44.165 * * [simplify]: iteration done : 59 enodes (cost 9 ) 44.166 * * [simplify]: iteration 0 : 9 enodes (cost 9 ) 44.167 * * [simplify]: iteration 1 : 14 enodes (cost 8 ) 44.168 * * [simplify]: iteration 2 : 17 enodes (cost 8 ) 44.169 * * [simplify]: iteration 3 : 18 enodes (cost 6 ) 44.171 * * [simplify]: iteration 4 : 31 enodes (cost 6 ) 44.176 * * [simplify]: iteration 5 : 36 enodes (cost 6 ) 44.179 * * [simplify]: iteration done : 36 enodes (cost 6 ) 44.180 * * [simplify]: iteration 0 : 9 enodes (cost 12 ) 44.181 * * [simplify]: iteration 1 : 16 enodes (cost 10 ) 44.187 * * [simplify]: iteration 2 : 25 enodes (cost 6 ) 44.190 * * [simplify]: iteration 3 : 33 enodes (cost 4 ) 44.192 * * [simplify]: iteration done : 33 enodes (cost 4 ) 44.193 * * [simplify]: iteration 0 : 9 enodes (cost 9 ) 44.194 * * [simplify]: iteration 1 : 14 enodes (cost 8 ) 44.195 * * [simplify]: iteration 2 : 17 enodes (cost 8 ) 44.197 * * [simplify]: iteration 3 : 18 enodes (cost 6 ) 44.199 * * [simplify]: iteration 4 : 31 enodes (cost 6 ) 44.203 * * [simplify]: iteration 5 : 36 enodes (cost 6 ) 44.206 * * [simplify]: iteration done : 36 enodes (cost 6 ) 44.207 * * [simplify]: iteration 0 : 5 enodes (cost 9 ) 44.208 * * [simplify]: iteration 1 : 11 enodes (cost 1 ) 44.208 * * [simplify]: iteration done : 11 enodes (cost 1 ) 44.208 * * [simplify]: iteration 0 : 8 enodes (cost 8 ) 44.209 * * [simplify]: iteration 1 : 13 enodes (cost 7 ) 44.211 * * [simplify]: iteration 2 : 24 enodes (cost 7 ) 44.214 * * [simplify]: iteration 3 : 37 enodes (cost 5 ) 44.221 * * [simplify]: iteration 4 : 72 enodes (cost 5 ) 44.230 * * [simplify]: iteration 5 : 83 enodes (cost 5 ) 44.237 * * [simplify]: iteration done : 83 enodes (cost 5 ) 44.238 * * [simplify]: iteration 0 : 5 enodes (cost 9 ) 44.239 * * [simplify]: iteration 1 : 11 enodes (cost 1 ) 44.239 * * [simplify]: iteration done : 11 enodes (cost 1 ) 44.240 * * [simplify]: iteration 0 : 8 enodes (cost 8 ) 44.241 * * [simplify]: iteration 1 : 13 enodes (cost 7 ) 44.242 * * [simplify]: iteration 2 : 24 enodes (cost 7 ) 44.249 * * [simplify]: iteration 3 : 37 enodes (cost 5 ) 44.256 * * [simplify]: iteration 4 : 72 enodes (cost 5 ) 44.264 * * [simplify]: iteration 5 : 83 enodes (cost 5 ) 44.271 * * [simplify]: iteration done : 83 enodes (cost 5 ) 44.272 * * [simplify]: iteration 0 : 4 enodes (cost 7 ) 44.273 * * [simplify]: iteration 1 : 8 enodes (cost 3 ) 44.274 * * [simplify]: iteration 2 : 12 enodes (cost 1 ) 44.274 * * [simplify]: iteration done : 12 enodes (cost 1 ) 44.274 * * [simplify]: iteration 0 : 8 enodes (cost 8 ) 44.276 * * [simplify]: iteration 1 : 13 enodes (cost 7 ) 44.277 * * [simplify]: iteration 2 : 24 enodes (cost 7 ) 44.280 * * [simplify]: iteration 3 : 37 enodes (cost 5 ) 44.287 * * [simplify]: iteration 4 : 72 enodes (cost 5 ) 44.296 * * [simplify]: iteration 5 : 83 enodes (cost 5 ) 44.304 * * [simplify]: iteration done : 83 enodes (cost 5 ) 44.304 * * [simplify]: iteration 0 : 5 enodes (cost 7 ) 44.309 * * [simplify]: iteration 1 : 9 enodes (cost 5 ) 44.309 * * [simplify]: iteration 2 : 11 enodes (cost 3 ) 44.310 * * [simplify]: iteration 3 : 12 enodes (cost 3 ) 44.311 * * [simplify]: iteration done : 12 enodes (cost 3 ) 44.312 * * [simplify]: iteration 0 : 7 enodes (cost 8 ) 44.313 * * [simplify]: iteration 1 : 12 enodes (cost 7 ) 44.314 * * [simplify]: iteration 2 : 23 enodes (cost 5 ) 44.317 * * [simplify]: iteration 3 : 28 enodes (cost 3 ) 44.321 * * [simplify]: iteration 4 : 40 enodes (cost 3 ) 44.323 * * [simplify]: iteration done : 40 enodes (cost 3 ) 44.324 * * [simplify]: iteration 0 : 12 enodes (cost 15 ) 44.325 * * [simplify]: iteration 1 : 32 enodes (cost 13 ) 44.330 * * [simplify]: iteration 2 : 58 enodes (cost 11 ) 44.339 * * [simplify]: iteration 3 : 123 enodes (cost 9 ) 44.363 * * [simplify]: iteration 4 : 298 enodes (cost 9 ) 44.564 * * [simplify]: iteration 5 : 919 enodes (cost 9 ) 45.517 * * [simplify]: iteration 6 : 2645 enodes (cost 9 ) 47.498 * * [simplify]: iteration done : 5001 enodes (cost 9 ) 47.499 * * [simplify]: iteration 0 : 10 enodes (cost 14 ) 47.500 * * [simplify]: iteration 1 : 20 enodes (cost 11 ) 47.508 * * [simplify]: iteration 2 : 35 enodes (cost 11 ) 47.514 * * [simplify]: iteration 3 : 48 enodes (cost 11 ) 47.522 * * [simplify]: iteration 4 : 68 enodes (cost 11 ) 47.533 * * [simplify]: iteration 5 : 89 enodes (cost 11 ) 47.549 * * [simplify]: iteration 6 : 106 enodes (cost 11 ) 47.565 * * [simplify]: iteration 7 : 129 enodes (cost 11 ) 47.587 * * [simplify]: iteration 8 : 172 enodes (cost 11 ) 47.624 * * [simplify]: iteration 9 : 234 enodes (cost 11 ) 47.654 * * [simplify]: iteration 10 : 235 enodes (cost 11 ) 47.688 * * [simplify]: iteration done : 235 enodes (cost 11 ) 47.689 * * [simplify]: iteration 0 : 11 enodes (cost 15 ) 47.691 * * [simplify]: iteration 1 : 22 enodes (cost 13 ) 47.693 * * [simplify]: iteration 2 : 48 enodes (cost 11 ) 47.703 * * [simplify]: iteration 3 : 133 enodes (cost 9 ) 47.755 * * [simplify]: iteration 4 : 370 enodes (cost 9 ) 47.940 * * [simplify]: iteration 5 : 747 enodes (cost 9 ) 48.173 * * [simplify]: iteration 6 : 1030 enodes (cost 9 ) 48.699 * * [simplify]: iteration 7 : 1638 enodes (cost 9 ) 51.336 * * [simplify]: iteration 8 : 4753 enodes (cost 9 ) 52.958 * * [simplify]: iteration done : 5000 enodes (cost 9 ) 52.959 * * [simplify]: iteration 0 : 6 enodes (cost 6 ) 52.960 * * [simplify]: iteration 1 : 10 enodes (cost 5 ) 52.961 * * [simplify]: iteration 2 : 11 enodes (cost 5 ) 52.961 * * [simplify]: iteration done : 11 enodes (cost 5 ) 52.962 * * [simplify]: iteration 0 : 10 enodes (cost 16 ) 52.963 * * [simplify]: iteration 1 : 15 enodes (cost 15 ) 52.964 * * [simplify]: iteration done : 15 enodes (cost 15 ) 52.965 * * [simplify]: iteration 0 : 9 enodes (cost 9 ) 52.966 * * [simplify]: iteration 1 : 12 enodes (cost 8 ) 52.967 * * [simplify]: iteration done : 12 enodes (cost 8 ) 52.967 * * [simplify]: iteration 0 : 9 enodes (cost 9 ) 52.968 * * [simplify]: iteration 1 : 12 enodes (cost 8 ) 52.969 * * [simplify]: iteration done : 12 enodes (cost 8 ) 52.970 * * [simplify]: iteration 0 : 9 enodes (cost 9 ) 52.971 * * [simplify]: iteration 1 : 12 enodes (cost 8 ) 52.971 * * [simplify]: iteration done : 12 enodes (cost 8 ) 52.972 * * [simplify]: iteration 0 : 12 enodes (cost 18 ) 52.973 * * [simplify]: iteration 1 : 23 enodes (cost 17 ) 52.976 * * [simplify]: iteration 2 : 44 enodes (cost 17 ) 52.983 * * [simplify]: iteration 3 : 73 enodes (cost 15 ) 53.000 * * [simplify]: iteration 4 : 133 enodes (cost 15 ) 53.044 * * [simplify]: iteration 5 : 198 enodes (cost 15 ) 53.077 * * [simplify]: iteration done : 198 enodes (cost 15 ) 53.078 * * [simplify]: iteration 0 : 10 enodes (cost 10 ) 53.079 * * [simplify]: iteration 1 : 15 enodes (cost 9 ) 53.080 * * [simplify]: iteration 2 : 18 enodes (cost 9 ) 53.082 * * [simplify]: iteration 3 : 19 enodes (cost 7 ) 53.084 * * [simplify]: iteration 4 : 32 enodes (cost 7 ) 53.089 * * [simplify]: iteration 5 : 39 enodes (cost 7 ) 53.092 * * [simplify]: iteration done : 39 enodes (cost 7 ) 53.093 * * [simplify]: iteration 0 : 11 enodes (cost 13 ) 53.095 * * [simplify]: iteration 1 : 18 enodes (cost 12 ) 53.097 * * [simplify]: iteration 2 : 26 enodes (cost 12 ) 53.100 * * [simplify]: iteration 3 : 39 enodes (cost 10 ) 53.106 * * [simplify]: iteration 4 : 66 enodes (cost 10 ) 53.123 * * [simplify]: iteration 5 : 97 enodes (cost 10 ) 53.137 * * [simplify]: iteration done : 97 enodes (cost 10 ) 53.138 * * [simplify]: iteration 0 : 10 enodes (cost 10 ) 53.139 * * [simplify]: iteration 1 : 15 enodes (cost 9 ) 53.140 * * [simplify]: iteration 2 : 18 enodes (cost 9 ) 53.142 * * [simplify]: iteration 3 : 19 enodes (cost 7 ) 53.144 * * [simplify]: iteration 4 : 32 enodes (cost 7 ) 53.148 * * [simplify]: iteration 5 : 39 enodes (cost 7 ) 53.152 * * [simplify]: iteration done : 39 enodes (cost 7 ) 53.153 * * [simplify]: iteration 0 : 7 enodes (cost 10 ) 53.154 * * [simplify]: iteration 1 : 13 enodes (cost 7 ) 53.156 * * [simplify]: iteration 2 : 24 enodes (cost 7 ) 53.158 * * [simplify]: iteration 3 : 33 enodes (cost 7 ) 53.161 * * [simplify]: iteration done : 33 enodes (cost 7 ) 53.162 * * [simplify]: iteration 0 : 9 enodes (cost 9 ) 53.163 * * [simplify]: iteration 1 : 14 enodes (cost 8 ) 53.164 * * [simplify]: iteration 2 : 25 enodes (cost 8 ) 53.167 * * [simplify]: iteration 3 : 38 enodes (cost 6 ) 53.175 * * [simplify]: iteration 4 : 73 enodes (cost 6 ) 53.184 * * [simplify]: iteration 5 : 84 enodes (cost 6 ) 53.195 * * [simplify]: iteration done : 84 enodes (cost 6 ) 53.196 * * [simplify]: iteration 0 : 7 enodes (cost 10 ) 53.196 * * [simplify]: iteration 1 : 13 enodes (cost 7 ) 53.198 * * [simplify]: iteration 2 : 24 enodes (cost 7 ) 53.201 * * [simplify]: iteration 3 : 33 enodes (cost 7 ) 53.203 * * [simplify]: iteration done : 33 enodes (cost 7 ) 53.204 * * [simplify]: iteration 0 : 9 enodes (cost 9 ) 53.205 * * [simplify]: iteration 1 : 14 enodes (cost 8 ) 53.206 * * [simplify]: iteration 2 : 25 enodes (cost 8 ) 53.209 * * [simplify]: iteration 3 : 38 enodes (cost 6 ) 53.217 * * [simplify]: iteration 4 : 73 enodes (cost 6 ) 53.226 * * [simplify]: iteration 5 : 84 enodes (cost 6 ) 53.234 * * [simplify]: iteration done : 84 enodes (cost 6 ) 53.235 * * [simplify]: iteration 0 : 11 enodes (cost 15 ) 53.236 * * [simplify]: iteration 1 : 18 enodes (cost 14 ) 53.238 * * [simplify]: iteration 2 : 25 enodes (cost 14 ) 53.241 * * [simplify]: iteration 3 : 33 enodes (cost 12 ) 53.245 * * [simplify]: iteration 4 : 57 enodes (cost 12 ) 53.259 * * [simplify]: iteration 5 : 74 enodes (cost 12 ) 53.266 * * [simplify]: iteration done : 74 enodes (cost 12 ) 53.267 * * [simplify]: iteration 0 : 10 enodes (cost 10 ) 53.268 * * [simplify]: iteration 1 : 15 enodes (cost 9 ) 53.270 * * [simplify]: iteration 2 : 18 enodes (cost 9 ) 53.271 * * [simplify]: iteration 3 : 19 enodes (cost 7 ) 53.273 * * [simplify]: iteration 4 : 32 enodes (cost 7 ) 53.278 * * [simplify]: iteration 5 : 39 enodes (cost 7 ) 53.282 * * [simplify]: iteration done : 39 enodes (cost 7 ) 53.283 * * [simplify]: iteration 0 : 10 enodes (cost 10 ) 53.284 * * [simplify]: iteration 1 : 15 enodes (cost 9 ) 53.285 * * [simplify]: iteration 2 : 18 enodes (cost 9 ) 53.287 * * [simplify]: iteration 3 : 19 enodes (cost 7 ) 53.290 * * [simplify]: iteration 4 : 32 enodes (cost 7 ) 53.294 * * [simplify]: iteration 5 : 39 enodes (cost 7 ) 53.298 * * [simplify]: iteration done : 39 enodes (cost 7 ) 53.298 * * [simplify]: iteration 0 : 10 enodes (cost 10 ) 53.299 * * [simplify]: iteration 1 : 15 enodes (cost 9 ) 53.300 * * [simplify]: iteration 2 : 18 enodes (cost 9 ) 53.302 * * [simplify]: iteration 3 : 19 enodes (cost 7 ) 53.304 * * [simplify]: iteration 4 : 32 enodes (cost 7 ) 53.309 * * [simplify]: iteration 5 : 39 enodes (cost 7 ) 53.315 * * [simplify]: iteration done : 39 enodes (cost 7 ) 53.316 * * [simplify]: iteration 0 : 6 enodes (cost 7 ) 53.316 * * [simplify]: iteration 1 : 10 enodes (cost 4 ) 53.317 * * [simplify]: iteration 2 : 15 enodes (cost 4 ) 53.318 * * [simplify]: iteration done : 15 enodes (cost 4 ) 53.319 * * [simplify]: iteration 0 : 9 enodes (cost 9 ) 53.320 * * [simplify]: iteration 1 : 14 enodes (cost 8 ) 53.321 * * [simplify]: iteration 2 : 25 enodes (cost 8 ) 53.324 * * [simplify]: iteration 3 : 38 enodes (cost 6 ) 53.332 * * [simplify]: iteration 4 : 73 enodes (cost 6 ) 53.347 * * [simplify]: iteration 5 : 84 enodes (cost 6 ) 53.355 * * [simplify]: iteration done : 84 enodes (cost 6 ) 53.355 * * [simplify]: iteration 0 : 6 enodes (cost 7 ) 53.356 * * [simplify]: iteration 1 : 10 enodes (cost 4 ) 53.357 * * [simplify]: iteration 2 : 15 enodes (cost 4 ) 53.358 * * [simplify]: iteration done : 15 enodes (cost 4 ) 53.359 * * [simplify]: iteration 0 : 9 enodes (cost 9 ) 53.360 * * [simplify]: iteration 1 : 14 enodes (cost 8 ) 53.361 * * [simplify]: iteration 2 : 25 enodes (cost 8 ) 53.364 * * [simplify]: iteration 3 : 38 enodes (cost 6 ) 53.371 * * [simplify]: iteration 4 : 73 enodes (cost 6 ) 53.384 * * [simplify]: iteration 5 : 84 enodes (cost 6 ) 53.392 * * [simplify]: iteration done : 84 enodes (cost 6 ) 53.393 * * [simplify]: iteration 0 : 9 enodes (cost 14 ) 53.394 * * [simplify]: iteration 1 : 16 enodes (cost 13 ) 53.395 * * [simplify]: iteration 2 : 23 enodes (cost 11 ) 53.398 * * [simplify]: iteration 3 : 32 enodes (cost 9 ) 53.402 * * [simplify]: iteration 4 : 45 enodes (cost 9 ) 53.409 * * [simplify]: iteration 5 : 47 enodes (cost 9 ) 53.414 * * [simplify]: iteration done : 47 enodes (cost 9 ) 53.415 * * [simplify]: iteration 0 : 9 enodes (cost 9 ) 53.416 * * [simplify]: iteration 1 : 14 enodes (cost 8 ) 53.417 * * [simplify]: iteration 2 : 17 enodes (cost 8 ) 53.419 * * [simplify]: iteration 3 : 18 enodes (cost 6 ) 53.421 * * [simplify]: iteration 4 : 31 enodes (cost 6 ) 53.425 * * [simplify]: iteration 5 : 36 enodes (cost 6 ) 53.429 * * [simplify]: iteration done : 36 enodes (cost 6 ) 53.430 * * [simplify]: iteration 0 : 8 enodes (cost 9 ) 53.431 * * [simplify]: iteration 1 : 13 enodes (cost 8 ) 53.432 * * [simplify]: iteration 2 : 16 enodes (cost 6 ) 53.433 * * [simplify]: iteration 3 : 21 enodes (cost 4 ) 53.436 * * [simplify]: iteration 4 : 25 enodes (cost 4 ) 53.438 * * [simplify]: iteration done : 25 enodes (cost 4 ) 53.438 * * [simplify]: iteration 0 : 9 enodes (cost 9 ) 53.442 * * [simplify]: iteration 1 : 14 enodes (cost 8 ) 53.444 * * [simplify]: iteration 2 : 17 enodes (cost 8 ) 53.445 * * [simplify]: iteration 3 : 18 enodes (cost 6 ) 53.447 * * [simplify]: iteration 4 : 31 enodes (cost 6 ) 53.452 * * [simplify]: iteration 5 : 36 enodes (cost 6 ) 53.455 * * [simplify]: iteration done : 36 enodes (cost 6 ) 53.455 * * [simplify]: iteration 0 : 4 enodes (cost 6 ) 53.456 * * [simplify]: iteration 1 : 8 enodes (cost 1 ) 53.456 * * [simplify]: iteration done : 8 enodes (cost 1 ) 53.457 * * [simplify]: iteration 0 : 8 enodes (cost 8 ) 53.458 * * [simplify]: iteration 1 : 13 enodes (cost 7 ) 53.459 * * [simplify]: iteration 2 : 24 enodes (cost 7 ) 53.462 * * [simplify]: iteration 3 : 37 enodes (cost 5 ) 53.469 * * [simplify]: iteration 4 : 72 enodes (cost 5 ) 53.478 * * [simplify]: iteration 5 : 83 enodes (cost 5 ) 53.486 * * [simplify]: iteration done : 83 enodes (cost 5 ) 53.487 * * [simplify]: iteration 0 : 4 enodes (cost 6 ) 53.487 * * [simplify]: iteration 1 : 8 enodes (cost 1 ) 53.487 * * [simplify]: iteration done : 8 enodes (cost 1 ) 53.488 * * [simplify]: iteration 0 : 8 enodes (cost 8 ) 53.489 * * [simplify]: iteration 1 : 13 enodes (cost 7 ) 53.490 * * [simplify]: iteration 2 : 24 enodes (cost 7 ) 53.493 * * [simplify]: iteration 3 : 37 enodes (cost 5 ) 53.503 * * [simplify]: iteration 4 : 72 enodes (cost 5 ) 53.512 * * [simplify]: iteration 5 : 83 enodes (cost 5 ) 53.519 * * [simplify]: iteration done : 83 enodes (cost 5 ) 53.519 * * [simplify]: iteration 0 : 3 enodes (cost 4 ) 53.520 * * [simplify]: iteration 1 : 5 enodes (cost 1 ) 53.520 * * [simplify]: iteration done : 5 enodes (cost 1 ) 53.521 * * [simplify]: iteration 0 : 8 enodes (cost 8 ) 53.522 * * [simplify]: iteration 1 : 13 enodes (cost 7 ) 53.523 * * [simplify]: iteration 2 : 24 enodes (cost 7 ) 53.526 * * [simplify]: iteration 3 : 37 enodes (cost 5 ) 53.533 * * [simplify]: iteration 4 : 72 enodes (cost 5 ) 53.542 * * [simplify]: iteration 5 : 83 enodes (cost 5 ) 53.549 * * [simplify]: iteration done : 83 enodes (cost 5 ) 53.550 * * [simplify]: iteration 0 : 4 enodes (cost 4 ) 53.550 * * [simplify]: iteration 1 : 6 enodes (cost 3 ) 53.551 * * [simplify]: iteration done : 6 enodes (cost 3 ) 53.551 * * [simplify]: iteration 0 : 7 enodes (cost 8 ) 53.552 * * [simplify]: iteration 1 : 12 enodes (cost 7 ) 53.553 * * [simplify]: iteration 2 : 23 enodes (cost 5 ) 53.557 * * [simplify]: iteration 3 : 28 enodes (cost 3 ) 53.563 * * [simplify]: iteration 4 : 40 enodes (cost 3 ) 53.565 * * [simplify]: iteration done : 40 enodes (cost 3 ) 53.566 * * [simplify]: iteration 0 : 11 enodes (cost 12 ) 53.568 * * [simplify]: iteration 1 : 29 enodes (cost 11 ) 53.571 * * [simplify]: iteration 2 : 49 enodes (cost 11 ) 53.578 * * [simplify]: iteration 3 : 103 enodes (cost 9 ) 53.600 * * [simplify]: iteration 4 : 275 enodes (cost 9 ) 53.810 * * [simplify]: iteration 5 : 928 enodes (cost 9 ) 54.800 * * [simplify]: iteration 6 : 2691 enodes (cost 9 ) 56.785 * * [simplify]: iteration done : 5001 enodes (cost 9 ) 56.786 * * [simplify]: iteration 0 : 10 enodes (cost 14 ) 56.787 * * [simplify]: iteration 1 : 20 enodes (cost 11 ) 56.790 * * [simplify]: iteration 2 : 35 enodes (cost 11 ) 56.795 * * [simplify]: iteration 3 : 48 enodes (cost 11 ) 56.803 * * [simplify]: iteration 4 : 68 enodes (cost 11 ) 56.814 * * [simplify]: iteration 5 : 89 enodes (cost 11 ) 56.831 * * [simplify]: iteration 6 : 106 enodes (cost 11 ) 56.846 * * [simplify]: iteration 7 : 129 enodes (cost 11 ) 56.868 * * [simplify]: iteration 8 : 172 enodes (cost 11 ) 56.906 * * [simplify]: iteration 9 : 234 enodes (cost 11 ) 56.937 * * [simplify]: iteration 10 : 235 enodes (cost 11 ) 56.968 * * [simplify]: iteration done : 235 enodes (cost 11 ) 56.969 * * [simplify]: iteration 0 : 10 enodes (cost 12 ) 56.970 * * [simplify]: iteration 1 : 19 enodes (cost 11 ) 56.972 * * [simplify]: iteration 2 : 39 enodes (cost 11 ) 56.979 * * [simplify]: iteration 3 : 109 enodes (cost 9 ) 57.020 * * [simplify]: iteration 4 : 331 enodes (cost 9 ) 57.205 * * [simplify]: iteration 5 : 750 enodes (cost 9 ) 57.424 * * [simplify]: iteration 6 : 1032 enodes (cost 9 ) 57.897 * * [simplify]: iteration 7 : 1598 enodes (cost 9 ) 60.476 * * [simplify]: iteration 8 : 4794 enodes (cost 9 ) 62.331 * * [simplify]: iteration done : 5000 enodes (cost 9 ) 62.332 * * [simplify]: iteration 0 : 6 enodes (cost 6 ) 62.333 * * [simplify]: iteration 1 : 10 enodes (cost 5 ) 62.334 * * [simplify]: iteration 2 : 11 enodes (cost 5 ) 62.334 * * [simplify]: iteration done : 11 enodes (cost 5 ) 62.335 * * [simplify]: iteration 0 : 9 enodes (cost 15 ) 62.336 * * [simplify]: iteration 1 : 14 enodes (cost 15 ) 62.337 * * [simplify]: iteration done : 14 enodes (cost 15 ) 62.338 * * [simplify]: iteration 0 : 8 enodes (cost 8 ) 62.339 * * [simplify]: iteration 1 : 11 enodes (cost 8 ) 62.340 * * [simplify]: iteration done : 11 enodes (cost 8 ) 62.340 * * [simplify]: iteration 0 : 8 enodes (cost 8 ) 62.341 * * [simplify]: iteration 1 : 11 enodes (cost 8 ) 62.342 * * [simplify]: iteration done : 11 enodes (cost 8 ) 62.342 * * [simplify]: iteration 0 : 8 enodes (cost 8 ) 62.343 * * [simplify]: iteration 1 : 11 enodes (cost 8 ) 62.344 * * [simplify]: iteration done : 11 enodes (cost 8 ) 62.345 * * [simplify]: iteration 0 : 11 enodes (cost 17 ) 62.347 * * [simplify]: iteration 1 : 22 enodes (cost 17 ) 62.349 * * [simplify]: iteration 2 : 43 enodes (cost 17 ) 62.359 * * [simplify]: iteration 3 : 72 enodes (cost 15 ) 62.375 * * [simplify]: iteration 4 : 132 enodes (cost 15 ) 62.420 * * [simplify]: iteration 5 : 205 enodes (cost 15 ) 62.451 * * [simplify]: iteration done : 205 enodes (cost 15 ) 62.452 * * [simplify]: iteration 0 : 9 enodes (cost 9 ) 62.453 * * [simplify]: iteration 1 : 14 enodes (cost 9 ) 62.454 * * [simplify]: iteration 2 : 17 enodes (cost 9 ) 62.455 * * [simplify]: iteration 3 : 18 enodes (cost 7 ) 62.457 * * [simplify]: iteration 4 : 31 enodes (cost 7 ) 62.462 * * [simplify]: iteration 5 : 36 enodes (cost 7 ) 62.468 * * [simplify]: iteration done : 36 enodes (cost 7 ) 62.469 * * [simplify]: iteration 0 : 10 enodes (cost 12 ) 62.470 * * [simplify]: iteration 1 : 17 enodes (cost 12 ) 62.472 * * [simplify]: iteration 2 : 25 enodes (cost 12 ) 62.475 * * [simplify]: iteration 3 : 38 enodes (cost 10 ) 62.481 * * [simplify]: iteration 4 : 65 enodes (cost 10 ) 62.498 * * [simplify]: iteration 5 : 105 enodes (cost 10 ) 62.510 * * [simplify]: iteration done : 105 enodes (cost 10 ) 62.510 * * [simplify]: iteration 0 : 9 enodes (cost 9 ) 62.511 * * [simplify]: iteration 1 : 14 enodes (cost 9 ) 62.512 * * [simplify]: iteration 2 : 17 enodes (cost 9 ) 62.514 * * [simplify]: iteration 3 : 18 enodes (cost 7 ) 62.516 * * [simplify]: iteration 4 : 31 enodes (cost 7 ) 62.521 * * [simplify]: iteration 5 : 36 enodes (cost 7 ) 62.527 * * [simplify]: iteration done : 36 enodes (cost 7 ) 62.527 * * [simplify]: iteration 0 : 6 enodes (cost 9 ) 62.528 * * [simplify]: iteration 1 : 12 enodes (cost 7 ) 62.530 * * [simplify]: iteration 2 : 23 enodes (cost 7 ) 62.533 * * [simplify]: iteration 3 : 32 enodes (cost 7 ) 62.535 * * [simplify]: iteration done : 32 enodes (cost 7 ) 62.536 * * [simplify]: iteration 0 : 8 enodes (cost 8 ) 62.537 * * [simplify]: iteration 1 : 13 enodes (cost 8 ) 62.538 * * [simplify]: iteration 2 : 24 enodes (cost 8 ) 62.541 * * [simplify]: iteration 3 : 37 enodes (cost 6 ) 62.549 * * [simplify]: iteration 4 : 72 enodes (cost 6 ) 62.557 * * [simplify]: iteration 5 : 83 enodes (cost 6 ) 62.565 * * [simplify]: iteration done : 83 enodes (cost 6 ) 62.566 * * [simplify]: iteration 0 : 6 enodes (cost 9 ) 62.566 * * [simplify]: iteration 1 : 12 enodes (cost 7 ) 62.568 * * [simplify]: iteration 2 : 23 enodes (cost 7 ) 62.571 * * [simplify]: iteration 3 : 32 enodes (cost 7 ) 62.573 * * [simplify]: iteration done : 32 enodes (cost 7 ) 62.574 * * [simplify]: iteration 0 : 8 enodes (cost 8 ) 62.575 * * [simplify]: iteration 1 : 13 enodes (cost 8 ) 62.576 * * [simplify]: iteration 2 : 24 enodes (cost 8 ) 62.579 * * [simplify]: iteration 3 : 37 enodes (cost 6 ) 62.589 * * [simplify]: iteration 4 : 72 enodes (cost 6 ) 62.598 * * [simplify]: iteration 5 : 83 enodes (cost 6 ) 62.606 * * [simplify]: iteration done : 83 enodes (cost 6 ) 62.607 * * [simplify]: iteration 0 : 10 enodes (cost 14 ) 62.608 * * [simplify]: iteration 1 : 17 enodes (cost 14 ) 62.610 * * [simplify]: iteration 2 : 24 enodes (cost 14 ) 62.612 * * [simplify]: iteration 3 : 32 enodes (cost 12 ) 62.618 * * [simplify]: iteration 4 : 56 enodes (cost 12 ) 62.627 * * [simplify]: iteration 5 : 75 enodes (cost 12 ) 62.635 * * [simplify]: iteration done : 75 enodes (cost 12 ) 62.636 * * [simplify]: iteration 0 : 9 enodes (cost 9 ) 62.636 * * [simplify]: iteration 1 : 14 enodes (cost 9 ) 62.638 * * [simplify]: iteration 2 : 17 enodes (cost 9 ) 62.639 * * [simplify]: iteration 3 : 18 enodes (cost 7 ) 62.644 * * [simplify]: iteration 4 : 31 enodes (cost 7 ) 62.649 * * [simplify]: iteration 5 : 36 enodes (cost 7 ) 62.652 * * [simplify]: iteration done : 36 enodes (cost 7 ) 62.653 * * [simplify]: iteration 0 : 9 enodes (cost 9 ) 62.654 * * [simplify]: iteration 1 : 14 enodes (cost 9 ) 62.655 * * [simplify]: iteration 2 : 17 enodes (cost 9 ) 62.657 * * [simplify]: iteration 3 : 18 enodes (cost 7 ) 62.659 * * [simplify]: iteration 4 : 31 enodes (cost 7 ) 62.664 * * [simplify]: iteration 5 : 36 enodes (cost 7 ) 62.668 * * [simplify]: iteration done : 36 enodes (cost 7 ) 62.668 * * [simplify]: iteration 0 : 9 enodes (cost 9 ) 62.669 * * [simplify]: iteration 1 : 14 enodes (cost 9 ) 62.670 * * [simplify]: iteration 2 : 17 enodes (cost 9 ) 62.672 * * [simplify]: iteration 3 : 18 enodes (cost 7 ) 62.674 * * [simplify]: iteration 4 : 31 enodes (cost 7 ) 62.679 * * [simplify]: iteration 5 : 36 enodes (cost 7 ) 62.682 * * [simplify]: iteration done : 36 enodes (cost 7 ) 62.683 * * [simplify]: iteration 0 : 5 enodes (cost 6 ) 62.684 * * [simplify]: iteration 1 : 9 enodes (cost 4 ) 62.685 * * [simplify]: iteration 2 : 14 enodes (cost 4 ) 62.685 * * [simplify]: iteration done : 14 enodes (cost 4 ) 62.686 * * [simplify]: iteration 0 : 8 enodes (cost 8 ) 62.687 * * [simplify]: iteration 1 : 13 enodes (cost 8 ) 62.688 * * [simplify]: iteration 2 : 24 enodes (cost 8 ) 62.692 * * [simplify]: iteration 3 : 37 enodes (cost 6 ) 62.698 * * [simplify]: iteration 4 : 72 enodes (cost 6 ) 62.710 * * [simplify]: iteration 5 : 83 enodes (cost 6 ) 62.718 * * [simplify]: iteration done : 83 enodes (cost 6 ) 62.718 * * [simplify]: iteration 0 : 5 enodes (cost 6 ) 62.719 * * [simplify]: iteration 1 : 9 enodes (cost 4 ) 62.720 * * [simplify]: iteration 2 : 14 enodes (cost 4 ) 62.721 * * [simplify]: iteration done : 14 enodes (cost 4 ) 62.721 * * [simplify]: iteration 0 : 8 enodes (cost 8 ) 62.722 * * [simplify]: iteration 1 : 13 enodes (cost 8 ) 62.724 * * [simplify]: iteration 2 : 24 enodes (cost 8 ) 62.727 * * [simplify]: iteration 3 : 37 enodes (cost 6 ) 62.734 * * [simplify]: iteration 4 : 72 enodes (cost 6 ) 62.742 * * [simplify]: iteration 5 : 83 enodes (cost 6 ) 62.750 * * [simplify]: iteration done : 83 enodes (cost 6 ) 62.751 * * [simplify]: iteration 0 : 8 enodes (cost 13 ) 62.752 * * [simplify]: iteration 1 : 15 enodes (cost 9 ) 62.753 * * [simplify]: iteration 2 : 24 enodes (cost 9 ) 62.757 * * [simplify]: iteration 3 : 37 enodes (cost 9 ) 62.764 * * [simplify]: iteration 4 : 46 enodes (cost 9 ) 62.771 * * [simplify]: iteration 5 : 47 enodes (cost 9 ) 62.776 * * [simplify]: iteration done : 47 enodes (cost 9 ) 62.777 * * [simplify]: iteration 0 : 8 enodes (cost 8 ) 62.778 * * [simplify]: iteration 1 : 13 enodes (cost 8 ) 62.779 * * [simplify]: iteration 2 : 16 enodes (cost 8 ) 62.781 * * [simplify]: iteration 3 : 17 enodes (cost 6 ) 62.783 * * [simplify]: iteration 4 : 30 enodes (cost 6 ) 62.787 * * [simplify]: iteration 5 : 35 enodes (cost 6 ) 62.791 * * [simplify]: iteration done : 35 enodes (cost 6 ) 62.791 * * [simplify]: iteration 0 : 7 enodes (cost 8 ) 62.792 * * [simplify]: iteration 1 : 12 enodes (cost 4 ) 62.793 * * [simplify]: iteration 2 : 17 enodes (cost 4 ) 62.795 * * [simplify]: iteration 3 : 19 enodes (cost 4 ) 62.797 * * [simplify]: iteration 4 : 20 enodes (cost 4 ) 62.799 * * [simplify]: iteration done : 20 enodes (cost 4 ) 62.799 * * [simplify]: iteration 0 : 8 enodes (cost 8 ) 62.800 * * [simplify]: iteration 1 : 13 enodes (cost 8 ) 62.801 * * [simplify]: iteration 2 : 16 enodes (cost 8 ) 62.803 * * [simplify]: iteration 3 : 17 enodes (cost 6 ) 62.805 * * [simplify]: iteration 4 : 30 enodes (cost 6 ) 62.810 * * [simplify]: iteration 5 : 35 enodes (cost 6 ) 62.813 * * [simplify]: iteration done : 35 enodes (cost 6 ) 62.814 * * [simplify]: iteration 0 : 3 enodes (cost 5 ) 62.815 * * [simplify]: iteration 1 : 6 enodes (cost 1 ) 62.815 * * [simplify]: iteration done : 6 enodes (cost 1 ) 62.815 * * [simplify]: iteration 0 : 7 enodes (cost 7 ) 62.816 * * [simplify]: iteration 1 : 12 enodes (cost 7 ) 62.818 * * [simplify]: iteration 2 : 23 enodes (cost 7 ) 62.821 * * [simplify]: iteration 3 : 36 enodes (cost 5 ) 62.831 * * [simplify]: iteration 4 : 71 enodes (cost 5 ) 62.839 * * [simplify]: iteration 5 : 82 enodes (cost 5 ) 62.847 * * [simplify]: iteration done : 82 enodes (cost 5 ) 62.847 * * [simplify]: iteration 0 : 3 enodes (cost 5 ) 62.848 * * [simplify]: iteration 1 : 6 enodes (cost 1 ) 62.848 * * [simplify]: iteration done : 6 enodes (cost 1 ) 62.849 * * [simplify]: iteration 0 : 7 enodes (cost 7 ) 62.849 * * [simplify]: iteration 1 : 12 enodes (cost 7 ) 62.851 * * [simplify]: iteration 2 : 23 enodes (cost 7 ) 62.854 * * [simplify]: iteration 3 : 36 enodes (cost 5 ) 62.861 * * [simplify]: iteration 4 : 71 enodes (cost 5 ) 62.869 * * [simplify]: iteration 5 : 82 enodes (cost 5 ) 62.878 * * [simplify]: iteration done : 82 enodes (cost 5 ) 62.878 * * [simplify]: iteration 0 : 2 enodes (cost 3 ) 62.879 * * [simplify]: iteration 1 : 4 enodes (cost 1 ) 62.879 * * [simplify]: iteration done : 4 enodes (cost 1 ) 62.879 * * [simplify]: iteration 0 : 7 enodes (cost 7 ) 62.880 * * [simplify]: iteration 1 : 12 enodes (cost 7 ) 62.882 * * [simplify]: iteration 2 : 23 enodes (cost 7 ) 62.888 * * [simplify]: iteration 3 : 36 enodes (cost 5 ) 62.895 * * [simplify]: iteration 4 : 71 enodes (cost 5 ) 62.904 * * [simplify]: iteration 5 : 82 enodes (cost 5 ) 62.911 * * [simplify]: iteration done : 82 enodes (cost 5 ) 62.911 * * [simplify]: iteration 0 : 3 enodes (cost 3 ) 62.912 * * [simplify]: iteration 1 : 5 enodes (cost 3 ) 62.912 * * [simplify]: iteration done : 5 enodes (cost 3 ) 62.912 * * [simplify]: iteration 0 : 6 enodes (cost 7 ) 62.913 * * [simplify]: iteration 1 : 11 enodes (cost 3 ) 62.915 * * [simplify]: iteration 2 : 24 enodes (cost 3 ) 62.918 * * [simplify]: iteration 3 : 34 enodes (cost 3 ) 62.920 * * [simplify]: iteration 4 : 35 enodes (cost 3 ) 62.923 * * [simplify]: iteration done : 35 enodes (cost 3 ) 62.923 * * [simplify]: iteration 0 : 10 enodes (cost 11 ) 62.925 * * [simplify]: iteration 1 : 28 enodes (cost 11 ) 62.928 * * [simplify]: iteration 2 : 48 enodes (cost 11 ) 62.936 * * [simplify]: iteration 3 : 102 enodes (cost 9 ) 62.962 * * [simplify]: iteration 4 : 276 enodes (cost 9 ) 63.183 * * [simplify]: iteration 5 : 933 enodes (cost 9 ) 64.157 * * [simplify]: iteration 6 : 2661 enodes (cost 9 ) 66.138 * * [simplify]: iteration done : 5001 enodes (cost 9 ) 66.139 * * [simplify]: iteration 0 : 9 enodes (cost 13 ) 66.140 * * [simplify]: iteration 1 : 19 enodes (cost 11 ) 66.143 * * [simplify]: iteration 2 : 34 enodes (cost 11 ) 66.148 * * [simplify]: iteration 3 : 47 enodes (cost 11 ) 66.156 * * [simplify]: iteration 4 : 67 enodes (cost 11 ) 66.167 * * [simplify]: iteration 5 : 88 enodes (cost 11 ) 66.187 * * [simplify]: iteration 6 : 105 enodes (cost 11 ) 66.200 * * [simplify]: iteration 7 : 128 enodes (cost 11 ) 66.220 * * [simplify]: iteration 8 : 171 enodes (cost 11 ) 66.259 * * [simplify]: iteration 9 : 233 enodes (cost 11 ) 66.292 * * [simplify]: iteration 10 : 234 enodes (cost 11 ) 66.321 * * [simplify]: iteration done : 234 enodes (cost 11 ) 66.322 * * [simplify]: iteration 0 : 9 enodes (cost 11 ) 66.323 * * [simplify]: iteration 1 : 18 enodes (cost 11 ) 66.325 * * [simplify]: iteration 2 : 38 enodes (cost 11 ) 66.332 * * [simplify]: iteration 3 : 108 enodes (cost 9 ) 66.374 * * [simplify]: iteration 4 : 326 enodes (cost 9 ) 66.552 * * [simplify]: iteration 5 : 743 enodes (cost 9 ) 66.773 * * [simplify]: iteration 6 : 1042 enodes (cost 9 ) 67.249 * * [simplify]: iteration 7 : 1607 enodes (cost 9 ) 69.787 * * [simplify]: iteration 8 : 4734 enodes (cost 9 ) 71.501 * * [simplify]: iteration done : 5000 enodes (cost 9 ) 71.502 * * [simplify]: iteration 0 : 5 enodes (cost 5 ) 71.503 * * [simplify]: iteration 1 : 9 enodes (cost 5 ) 71.504 * * [simplify]: iteration 2 : 10 enodes (cost 5 ) 71.505 * * [simplify]: iteration done : 10 enodes (cost 5 ) 71.505 * * [simplify]: iteration 0 : 7 enodes (cost 7 ) 71.506 * * [simplify]: iteration 1 : 12 enodes (cost 7 ) 71.507 * * [simplify]: iteration 2 : 23 enodes (cost 7 ) 71.510 * * [simplify]: iteration 3 : 36 enodes (cost 5 ) 71.524 * * [simplify]: iteration 4 : 71 enodes (cost 5 ) 71.533 * * [simplify]: iteration 5 : 82 enodes (cost 5 ) 71.540 * * [simplify]: iteration done : 82 enodes (cost 5 ) 71.541 * * [simplify]: iteration 0 : 7 enodes (cost 7 ) 71.542 * * [simplify]: iteration 1 : 12 enodes (cost 5 ) 71.544 * * [simplify]: iteration 2 : 27 enodes (cost 5 ) 71.548 * * [simplify]: iteration 3 : 37 enodes (cost 5 ) 71.550 * * [simplify]: iteration done : 37 enodes (cost 5 ) 71.550 * * [simplify]: iteration 0 : 9 enodes (cost 15 ) 71.551 * * [simplify]: iteration 1 : 14 enodes (cost 15 ) 71.552 * * [simplify]: iteration done : 14 enodes (cost 15 ) 71.553 * * [simplify]: iteration 0 : 8 enodes (cost 8 ) 71.554 * * [simplify]: iteration 1 : 11 enodes (cost 8 ) 71.555 * * [simplify]: iteration done : 11 enodes (cost 8 ) 71.555 * * [simplify]: iteration 0 : 11 enodes (cost 17 ) 71.557 * * [simplify]: iteration 1 : 22 enodes (cost 17 ) 71.559 * * [simplify]: iteration 2 : 43 enodes (cost 17 ) 71.566 * * [simplify]: iteration 3 : 72 enodes (cost 15 ) 71.585 * * [simplify]: iteration 4 : 132 enodes (cost 15 ) 71.627 * * [simplify]: iteration 5 : 205 enodes (cost 15 ) 71.658 * * [simplify]: iteration done : 205 enodes (cost 15 ) 71.659 * * [simplify]: iteration 0 : 10 enodes (cost 12 ) 71.660 * * [simplify]: iteration 1 : 17 enodes (cost 12 ) 71.661 * * [simplify]: iteration 2 : 25 enodes (cost 12 ) 71.665 * * [simplify]: iteration 3 : 38 enodes (cost 10 ) 71.671 * * [simplify]: iteration 4 : 65 enodes (cost 10 ) 71.690 * * [simplify]: iteration 5 : 105 enodes (cost 10 ) 71.701 * * [simplify]: iteration done : 105 enodes (cost 10 ) 71.702 * * [simplify]: iteration 0 : 6 enodes (cost 9 ) 71.703 * * [simplify]: iteration 1 : 12 enodes (cost 7 ) 71.704 * * [simplify]: iteration 2 : 23 enodes (cost 7 ) 71.707 * * [simplify]: iteration 3 : 32 enodes (cost 7 ) 71.710 * * [simplify]: iteration done : 32 enodes (cost 7 ) 71.710 * * [simplify]: iteration 0 : 6 enodes (cost 9 ) 71.711 * * [simplify]: iteration 1 : 12 enodes (cost 7 ) 71.713 * * [simplify]: iteration 2 : 23 enodes (cost 7 ) 71.716 * * [simplify]: iteration 3 : 32 enodes (cost 7 ) 71.719 * * [simplify]: iteration done : 32 enodes (cost 7 ) 71.720 * * [simplify]: iteration 0 : 10 enodes (cost 14 ) 71.721 * * [simplify]: iteration 1 : 17 enodes (cost 14 ) 71.722 * * [simplify]: iteration 2 : 24 enodes (cost 14 ) 71.725 * * [simplify]: iteration 3 : 32 enodes (cost 12 ) 71.730 * * [simplify]: iteration 4 : 56 enodes (cost 12 ) 71.740 * * [simplify]: iteration 5 : 75 enodes (cost 12 ) 71.749 * * [simplify]: iteration done : 75 enodes (cost 12 ) 71.750 * * [simplify]: iteration 0 : 9 enodes (cost 9 ) 71.751 * * [simplify]: iteration 1 : 14 enodes (cost 9 ) 71.752 * * [simplify]: iteration 2 : 17 enodes (cost 9 ) 71.754 * * [simplify]: iteration 3 : 18 enodes (cost 7 ) 71.756 * * [simplify]: iteration 4 : 31 enodes (cost 7 ) 71.761 * * [simplify]: iteration 5 : 36 enodes (cost 7 ) 71.764 * * [simplify]: iteration done : 36 enodes (cost 7 ) 71.765 * * [simplify]: iteration 0 : 5 enodes (cost 6 ) 71.765 * * [simplify]: iteration 1 : 9 enodes (cost 4 ) 71.766 * * [simplify]: iteration 2 : 14 enodes (cost 4 ) 71.767 * * [simplify]: iteration done : 14 enodes (cost 4 ) 71.768 * * [simplify]: iteration 0 : 5 enodes (cost 6 ) 71.768 * * [simplify]: iteration 1 : 9 enodes (cost 4 ) 71.769 * * [simplify]: iteration 2 : 14 enodes (cost 4 ) 71.770 * * [simplify]: iteration done : 14 enodes (cost 4 ) 71.771 * * [simplify]: iteration 0 : 8 enodes (cost 13 ) 71.772 * * [simplify]: iteration 1 : 15 enodes (cost 9 ) 71.774 * * [simplify]: iteration 2 : 24 enodes (cost 9 ) 71.777 * * [simplify]: iteration 3 : 37 enodes (cost 9 ) 71.782 * * [simplify]: iteration 4 : 46 enodes (cost 9 ) 71.788 * * [simplify]: iteration 5 : 47 enodes (cost 9 ) 71.794 * * [simplify]: iteration done : 47 enodes (cost 9 ) 71.795 * * [simplify]: iteration 0 : 7 enodes (cost 8 ) 71.796 * * [simplify]: iteration 1 : 12 enodes (cost 4 ) 71.797 * * [simplify]: iteration 2 : 17 enodes (cost 4 ) 71.798 * * [simplify]: iteration 3 : 19 enodes (cost 4 ) 71.800 * * [simplify]: iteration 4 : 20 enodes (cost 4 ) 71.802 * * [simplify]: iteration done : 20 enodes (cost 4 ) 71.803 * * [simplify]: iteration 0 : 3 enodes (cost 5 ) 71.804 * * [simplify]: iteration 1 : 6 enodes (cost 1 ) 71.804 * * [simplify]: iteration done : 6 enodes (cost 1 ) 71.804 * * [simplify]: iteration 0 : 3 enodes (cost 5 ) 71.807 * * [simplify]: iteration 1 : 6 enodes (cost 1 ) 71.808 * * [simplify]: iteration done : 6 enodes (cost 1 ) 71.808 * * [simplify]: iteration 0 : 2 enodes (cost 3 ) 71.809 * * [simplify]: iteration 1 : 4 enodes (cost 1 ) 71.809 * * [simplify]: iteration done : 4 enodes (cost 1 ) 71.809 * * [simplify]: iteration 0 : 3 enodes (cost 3 ) 71.810 * * [simplify]: iteration 1 : 5 enodes (cost 3 ) 71.810 * * [simplify]: iteration done : 5 enodes (cost 3 ) 71.811 * * [simplify]: iteration 0 : 10 enodes (cost 11 ) 71.812 * * [simplify]: iteration 1 : 28 enodes (cost 11 ) 71.816 * * [simplify]: iteration 2 : 48 enodes (cost 11 ) 71.823 * * [simplify]: iteration 3 : 102 enodes (cost 9 ) 71.845 * * [simplify]: iteration 4 : 276 enodes (cost 9 ) 72.059 * * [simplify]: iteration 5 : 933 enodes (cost 9 ) 73.015 * * [simplify]: iteration 6 : 2661 enodes (cost 9 ) 74.951 * * [simplify]: iteration done : 5001 enodes (cost 9 ) 74.952 * * [simplify]: iteration 0 : 9 enodes (cost 11 ) 74.953 * * [simplify]: iteration 1 : 18 enodes (cost 11 ) 74.955 * * [simplify]: iteration 2 : 38 enodes (cost 11 ) 74.966 * * [simplify]: iteration 3 : 108 enodes (cost 9 ) 75.006 * * [simplify]: iteration 4 : 326 enodes (cost 9 ) 75.191 * * [simplify]: iteration 5 : 743 enodes (cost 9 ) 75.418 * * [simplify]: iteration 6 : 1042 enodes (cost 9 ) 75.898 * * [simplify]: iteration 7 : 1607 enodes (cost 9 ) 78.455 * * [simplify]: iteration 8 : 4734 enodes (cost 9 ) 80.170 * * [simplify]: iteration done : 5000 enodes (cost 9 ) 80.171 * * [simplify]: iteration 0 : 8 enodes (cost 8 ) 80.171 * * [simplify]: iteration 1 : 13 enodes (cost 7 ) 80.173 * * [simplify]: iteration 2 : 24 enodes (cost 7 ) 80.176 * * [simplify]: iteration done : 24 enodes (cost 5 ) 80.177 * * [simplify]: iteration 0 : 8 enodes (cost 8 ) 80.178 * * [simplify]: iteration 1 : 13 enodes (cost 7 ) 80.179 * * [simplify]: iteration 2 : 24 enodes (cost 7 ) 80.183 * * [simplify]: iteration done : 24 enodes (cost 5 ) 80.183 * * [simplify]: iteration 0 : 7 enodes (cost 7 ) 80.184 * * [simplify]: iteration 1 : 12 enodes (cost 5 ) 80.185 * * [simplify]: iteration 2 : 27 enodes (cost 5 ) 80.190 * * [simplify]: iteration 3 : 37 enodes (cost 5 ) 80.191 * * [simplify]: iteration done : 37 enodes (cost 5 ) 80.192 * * [simplify]: iteration 0 : 3 enodes (cost 3 ) 80.192 * * [simplify]: iteration 1 : 5 enodes (cost 3 ) 80.193 * * [simplify]: iteration done : 5 enodes (cost 3 ) 80.193 * * [simplify]: iteration 0 : 7 enodes (cost 7 ) 80.194 * * [simplify]: iteration 1 : 10 enodes (cost 7 ) 80.195 * * [simplify]: iteration 2 : 11 enodes (cost 7 ) 80.196 * * [simplify]: iteration done : 11 enodes (cost 7 ) 80.197 * * [simplify]: iteration 0 : 6 enodes (cost 6 ) 80.197 * * [simplify]: iteration 1 : 10 enodes (cost 6 ) 80.198 * * [simplify]: iteration 2 : 12 enodes (cost 6 ) 80.199 * * [simplify]: iteration 3 : 13 enodes (cost 6 ) 80.201 * * [simplify]: iteration done : 13 enodes (cost 6 ) 80.201 * * [simplify]: iteration 0 : 6 enodes (cost 6 ) 80.202 * * [simplify]: iteration 1 : 7 enodes (cost 6 ) 80.202 * * [simplify]: iteration done : 7 enodes (cost 6 ) 80.203 * * [simplify]: iteration 0 : 9 enodes (cost 17 ) 80.205 * * [simplify]: iteration 1 : 31 enodes (cost 17 ) 80.211 * * [simplify]: iteration 2 : 93 enodes (cost 9 ) 80.235 * * [simplify]: iteration 3 : 220 enodes (cost 7 ) 80.304 * * [simplify]: iteration 4 : 496 enodes (cost 7 ) 80.559 * * [simplify]: iteration 5 : 1299 enodes (cost 7 ) 81.783 * * [simplify]: iteration 6 : 2986 enodes (cost 7 ) 82.909 * * [simplify]: iteration done : 5001 enodes (cost 7 ) 82.910 * * [simplify]: iteration 0 : 7 enodes (cost 13 ) 82.910 * * [simplify]: iteration 1 : 8 enodes (cost 13 ) 82.911 * * [simplify]: iteration done : 8 enodes (cost 13 ) 82.912 * * [simplify]: iteration 0 : 6 enodes (cost 6 ) 82.913 * * [simplify]: iteration 1 : 7 enodes (cost 6 ) 82.913 * * [simplify]: iteration done : 7 enodes (cost 6 ) 82.914 * * [simplify]: iteration 0 : 7 enodes (cost 17 ) 82.915 * * [simplify]: iteration 1 : 15 enodes (cost 17 ) 82.917 * * [simplify]: iteration 2 : 31 enodes (cost 7 ) 82.923 * * [simplify]: iteration 3 : 69 enodes (cost 7 ) 82.937 * * [simplify]: iteration 4 : 152 enodes (cost 7 ) 82.976 * * [simplify]: iteration 5 : 302 enodes (cost 7 ) 83.061 * * [simplify]: iteration 6 : 586 enodes (cost 7 ) 83.290 * * [simplify]: iteration 7 : 1368 enodes (cost 7 ) 84.609 * * [simplify]: iteration 8 : 4784 enodes (cost 7 ) 85.870 * * [simplify]: iteration done : 5000 enodes (cost 7 ) 85.871 * * [simplify]: iteration 0 : 6 enodes (cost 6 ) 85.872 * * [simplify]: iteration 1 : 7 enodes (cost 6 ) 85.872 * * [simplify]: iteration done : 7 enodes (cost 6 ) 85.873 * * [simplify]: iteration 0 : 6 enodes (cost 6 ) 85.874 * * [simplify]: iteration 1 : 7 enodes (cost 6 ) 85.874 * * [simplify]: iteration done : 7 enodes (cost 6 ) 85.875 * * [simplify]: iteration 0 : 2 enodes (cost 2 ) 85.875 * * [simplify]: iteration done : 2 enodes (cost 2 ) 85.876 * * [simplify]: iteration 0 : 4 enodes (cost 4 ) 85.876 * * [simplify]: iteration 1 : 8 enodes (cost 4 ) 85.877 * * [simplify]: iteration 2 : 10 enodes (cost 4 ) 85.878 * * [simplify]: iteration 3 : 11 enodes (cost 4 ) 85.879 * * [simplify]: iteration done : 11 enodes (cost 4 ) 85.880 * * [simplify]: iteration 0 : 9 enodes (cost 15 ) 85.881 * * [simplify]: iteration 1 : 16 enodes (cost 15 ) 85.883 * * [simplify]: iteration 2 : 25 enodes (cost 15 ) 85.886 * * [simplify]: iteration 3 : 31 enodes (cost 15 ) 85.890 * * [simplify]: iteration done : 31 enodes (cost 15 ) 85.890 * * [simplify]: iteration 0 : 7 enodes (cost 7 ) 85.891 * * [simplify]: iteration 1 : 8 enodes (cost 7 ) 85.892 * * [simplify]: iteration done : 8 enodes (cost 7 ) 85.892 * * [simplify]: iteration 0 : 8 enodes (cost 10 ) 85.893 * * [simplify]: iteration 1 : 11 enodes (cost 10 ) 85.895 * * [simplify]: iteration 2 : 13 enodes (cost 10 ) 85.896 * * [simplify]: iteration 3 : 14 enodes (cost 10 ) 85.897 * * [simplify]: iteration done : 14 enodes (cost 10 ) 85.898 * * [simplify]: iteration 0 : 7 enodes (cost 7 ) 85.899 * * [simplify]: iteration 1 : 8 enodes (cost 7 ) 85.899 * * [simplify]: iteration done : 8 enodes (cost 7 ) 85.900 * * [simplify]: iteration 0 : 5 enodes (cost 7 ) 85.901 * * [simplify]: iteration 1 : 9 enodes (cost 5 ) 85.902 * * [simplify]: iteration 2 : 15 enodes (cost 5 ) 85.903 * * [simplify]: iteration 3 : 20 enodes (cost 5 ) 85.909 * * [simplify]: iteration done : 20 enodes (cost 5 ) 85.910 * * [simplify]: iteration 0 : 6 enodes (cost 6 ) 85.910 * * [simplify]: iteration 1 : 7 enodes (cost 6 ) 85.911 * * [simplify]: iteration done : 7 enodes (cost 6 ) 85.911 * * [simplify]: iteration 0 : 5 enodes (cost 7 ) 85.912 * * [simplify]: iteration 1 : 9 enodes (cost 5 ) 85.913 * * [simplify]: iteration 2 : 15 enodes (cost 5 ) 85.915 * * [simplify]: iteration 3 : 20 enodes (cost 5 ) 85.916 * * [simplify]: iteration done : 20 enodes (cost 5 ) 85.917 * * [simplify]: iteration 0 : 6 enodes (cost 6 ) 85.917 * * [simplify]: iteration 1 : 7 enodes (cost 6 ) 85.918 * * [simplify]: iteration done : 7 enodes (cost 6 ) 85.918 * * [simplify]: iteration 0 : 8 enodes (cost 12 ) 85.919 * * [simplify]: iteration 1 : 11 enodes (cost 12 ) 85.920 * * [simplify]: iteration done : 11 enodes (cost 12 ) 85.921 * * [simplify]: iteration 0 : 7 enodes (cost 7 ) 85.922 * * [simplify]: iteration 1 : 8 enodes (cost 7 ) 85.922 * * [simplify]: iteration done : 8 enodes (cost 7 ) 85.923 * * [simplify]: iteration 0 : 7 enodes (cost 7 ) 85.923 * * [simplify]: iteration 1 : 8 enodes (cost 7 ) 85.925 * * [simplify]: iteration done : 8 enodes (cost 7 ) 85.925 * * [simplify]: iteration 0 : 7 enodes (cost 7 ) 85.926 * * [simplify]: iteration 1 : 8 enodes (cost 7 ) 85.926 * * [simplify]: iteration done : 8 enodes (cost 7 ) 85.927 * * [simplify]: iteration 0 : 4 enodes (cost 4 ) 85.927 * * [simplify]: iteration 1 : 6 enodes (cost 2 ) 85.928 * * [simplify]: iteration 2 : 8 enodes (cost 2 ) 85.928 * * [simplify]: iteration done : 8 enodes (cost 2 ) 85.929 * * [simplify]: iteration 0 : 6 enodes (cost 6 ) 85.930 * * [simplify]: iteration 1 : 7 enodes (cost 6 ) 85.930 * * [simplify]: iteration done : 7 enodes (cost 6 ) 85.931 * * [simplify]: iteration 0 : 4 enodes (cost 4 ) 85.931 * * [simplify]: iteration 1 : 6 enodes (cost 2 ) 85.932 * * [simplify]: iteration 2 : 8 enodes (cost 2 ) 85.932 * * [simplify]: iteration done : 8 enodes (cost 2 ) 85.933 * * [simplify]: iteration 0 : 6 enodes (cost 6 ) 85.933 * * [simplify]: iteration 1 : 7 enodes (cost 6 ) 85.934 * * [simplify]: iteration done : 7 enodes (cost 6 ) 85.935 * * [simplify]: iteration 0 : 7 enodes (cost 11 ) 85.936 * * [simplify]: iteration 1 : 12 enodes (cost 11 ) 85.937 * * [simplify]: iteration done : 12 enodes (cost 11 ) 85.937 * * [simplify]: iteration 0 : 6 enodes (cost 6 ) 85.938 * * [simplify]: iteration 1 : 7 enodes (cost 6 ) 85.939 * * [simplify]: iteration done : 7 enodes (cost 6 ) 85.939 * * [simplify]: iteration 0 : 6 enodes (cost 6 ) 85.940 * * [simplify]: iteration 1 : 9 enodes (cost 6 ) 85.940 * * [simplify]: iteration done : 9 enodes (cost 6 ) 85.941 * * [simplify]: iteration 0 : 6 enodes (cost 6 ) 85.942 * * [simplify]: iteration 1 : 7 enodes (cost 6 ) 85.942 * * [simplify]: iteration done : 7 enodes (cost 6 ) 85.943 * * [simplify]: iteration 0 : 2 enodes (cost 3 ) 85.943 * * [simplify]: iteration 1 : 4 enodes (cost 1 ) 85.943 * * [simplify]: iteration done : 4 enodes (cost 1 ) 85.944 * * [simplify]: iteration 0 : 5 enodes (cost 5 ) 85.945 * * [simplify]: iteration 1 : 6 enodes (cost 5 ) 85.945 * * [simplify]: iteration done : 6 enodes (cost 5 ) 85.946 * * [simplify]: iteration 0 : 2 enodes (cost 3 ) 85.946 * * [simplify]: iteration 1 : 4 enodes (cost 1 ) 85.946 * * [simplify]: iteration done : 4 enodes (cost 1 ) 85.947 * * [simplify]: iteration 0 : 5 enodes (cost 5 ) 85.947 * * [simplify]: iteration 1 : 6 enodes (cost 5 ) 85.948 * * [simplify]: iteration done : 6 enodes (cost 5 ) 85.949 * * [simplify]: iteration 0 : 5 enodes (cost 5 ) 85.949 * * [simplify]: iteration 1 : 8 enodes (cost 5 ) 85.950 * * [simplify]: iteration done : 8 enodes (cost 5 ) 85.951 * * [simplify]: iteration 0 : 5 enodes (cost 5 ) 85.951 * * [simplify]: iteration 1 : 6 enodes (cost 5 ) 85.952 * * [simplify]: iteration done : 6 enodes (cost 5 ) 85.952 * * [simplify]: iteration 0 : 7 enodes (cost 11 ) 85.953 * * [simplify]: iteration 1 : 10 enodes (cost 11 ) 85.954 * * [simplify]: iteration done : 10 enodes (cost 11 ) 85.955 * * [simplify]: iteration 0 : 6 enodes (cost 6 ) 85.955 * * [simplify]: iteration 1 : 7 enodes (cost 6 ) 85.956 * * [simplify]: iteration done : 7 enodes (cost 6 ) 85.956 * * [simplify]: iteration 0 : 3 enodes (cost 3 ) 85.957 * * [simplify]: iteration 1 : 5 enodes (cost 1 ) 85.957 * * [simplify]: iteration done : 5 enodes (cost 1 ) 85.958 * * [simplify]: iteration 0 : 3 enodes (cost 3 ) 85.958 * * [simplify]: iteration 1 : 5 enodes (cost 1 ) 85.958 * * [simplify]: iteration done : 5 enodes (cost 1 ) 85.959 * * [simplify]: iteration 0 : 6 enodes (cost 6 ) 85.960 * * [simplify]: iteration 1 : 7 enodes (cost 6 ) 85.960 * * [simplify]: iteration done : 7 enodes (cost 6 ) 85.961 * * [simplify]: iteration 0 : 6 enodes (cost 6 ) 85.961 * * [simplify]: iteration 1 : 7 enodes (cost 6 ) 85.962 * * [simplify]: iteration done : 7 enodes (cost 6 ) 85.963 * * [simplify]: iteration 0 : 5 enodes (cost 5 ) 85.963 * * [simplify]: iteration 1 : 6 enodes (cost 5 ) 85.964 * * [simplify]: iteration done : 6 enodes (cost 5 ) 85.965 * * [simplify]: iteration 0 : 8 enodes (cost 9 ) 85.966 * * [simplify]: iteration 1 : 22 enodes (cost 9 ) 85.969 * * [simplify]: iteration 2 : 31 enodes (cost 9 ) 85.973 * * [simplify]: iteration 3 : 48 enodes (cost 9 ) 85.983 * * [simplify]: iteration 4 : 89 enodes (cost 9 ) 86.004 * * [simplify]: iteration 5 : 204 enodes (cost 9 ) 86.101 * * [simplify]: iteration 6 : 605 enodes (cost 9 ) 87.039 * * [simplify]: iteration 7 : 2437 enodes (cost 9 ) 89.003 * * [simplify]: iteration done : 5000 enodes (cost 9 ) 89.003 * * [simplify]: iteration 0 : 7 enodes (cost 9 ) 89.004 * * [simplify]: iteration 1 : 12 enodes (cost 9 ) 89.006 * * [simplify]: iteration 2 : 21 enodes (cost 9 ) 89.009 * * [simplify]: iteration 3 : 38 enodes (cost 9 ) 89.016 * * [simplify]: iteration 4 : 63 enodes (cost 9 ) 89.031 * * [simplify]: iteration 5 : 104 enodes (cost 9 ) 89.059 * * [simplify]: iteration 6 : 160 enodes (cost 9 ) 89.115 * * [simplify]: iteration 7 : 328 enodes (cost 9 ) 89.843 * * [simplify]: iteration 8 : 1613 enodes (cost 9 ) 95.957 * * [simplify]: iteration done : 5000 enodes (cost 9 ) 95.958 * * [simplify]: iteration 0 : 5 enodes (cost 5 ) 95.959 * * [simplify]: iteration 1 : 7 enodes (cost 5 ) 95.959 * * [simplify]: iteration done : 7 enodes (cost 5 ) 95.960 * * [simplify]: iteration 0 : 5 enodes (cost 5 ) 95.961 * * [simplify]: iteration 1 : 7 enodes (cost 5 ) 95.961 * * [simplify]: iteration done : 7 enodes (cost 5 ) 95.962 * * [simplify]: iteration 0 : 5 enodes (cost 5 ) 95.963 * * [simplify]: iteration 1 : 7 enodes (cost 5 ) 95.964 * * [simplify]: iteration done : 7 enodes (cost 5 ) 95.964 * * [simplify]: iteration 0 : 10 enodes (cost 11 ) 95.966 * * [simplify]: iteration 1 : 22 enodes (cost 11 ) 95.970 * * [simplify]: iteration 2 : 51 enodes (cost 11 ) 95.977 * * [simplify]: iteration 3 : 62 enodes (cost 11 ) 95.985 * * [simplify]: iteration 4 : 82 enodes (cost 9 ) 95.997 * * [simplify]: iteration 5 : 120 enodes (cost 9 ) 96.019 * * [simplify]: iteration 6 : 189 enodes (cost 9 ) 96.075 * * [simplify]: iteration 7 : 313 enodes (cost 9 ) 96.152 * * [simplify]: iteration 8 : 549 enodes (cost 9 ) 96.658 * * [simplify]: iteration 9 : 1494 enodes (cost 9 ) 98.840 * * [simplify]: iteration done : 5000 enodes (cost 9 ) 98.841 * * [simplify]: iteration 0 : 17 enodes (cost 21 ) 98.844 * * [simplify]: iteration 1 : 43 enodes (cost 21 ) 98.852 * * [simplify]: iteration 2 : 107 enodes (cost 15 ) 98.884 * * [simplify]: iteration 3 : 269 enodes (cost 15 ) 99.073 * * [simplify]: iteration 4 : 865 enodes (cost 15 ) 99.920 * * [simplify]: iteration 5 : 2825 enodes (cost 13 ) 101.233 * * [simplify]: iteration done : 5001 enodes (cost 13 ) 101.234 * * [simplify]: iteration 0 : 17 enodes (cost 21 ) 101.242 * * [simplify]: iteration 1 : 43 enodes (cost 21 ) 101.250 * * [simplify]: iteration 2 : 107 enodes (cost 15 ) 101.282 * * [simplify]: iteration 3 : 269 enodes (cost 15 ) 101.475 * * [simplify]: iteration 4 : 865 enodes (cost 15 ) 102.359 * * [simplify]: iteration 5 : 2825 enodes (cost 13 ) 103.476 * * [simplify]: iteration done : 5001 enodes (cost 13 ) 103.477 * [simplify]: Simplified to: -1 (- (log (+ x 16.0)) (log 116.0)) (neg (log (/ 116.0 (+ x 16.0)))) (- (log (+ x 16.0)) (log 116.0)) (neg (log (/ 116.0 (+ x 16.0)))) (- (log (+ x 16.0)) (log 116.0)) (neg (log (/ 116.0 (+ x 16.0)))) (log (/ (+ x 16.0) 116.0)) (exp (/ (+ x 16.0) 116.0)) (/ (pow (+ x 16.0) 3) (pow 116.0 3)) (pow (/ (+ x 16.0) 116.0) 3) (* (cbrt (/ (+ x 16.0) 116.0)) (cbrt (/ (+ x 16.0) 116.0))) (cbrt (/ (+ x 16.0) 116.0)) (pow (/ (+ x 16.0) 116.0) 3) (sqrt (/ (+ x 16.0) 116.0)) (sqrt (/ (+ x 16.0) 116.0)) -1 (neg (/ 116.0 (+ x 16.0))) (/ 1 (* (cbrt (/ 116.0 (+ x 16.0))) (cbrt (/ 116.0 (+ x 16.0))))) (/ 1 (cbrt (/ 116.0 (+ x 16.0)))) (/ 1 (sqrt (/ 116.0 (+ x 16.0)))) (/ 1 (sqrt (/ 116.0 (+ x 16.0)))) (/ (cbrt (+ x 16.0)) (* (/ (cbrt 116.0) (cbrt (+ x 16.0))) (cbrt 116.0))) (/ (cbrt (+ x 16.0)) (cbrt 116.0)) (/ (sqrt (+ x 16.0)) (* (cbrt 116.0) (cbrt 116.0))) (/ (sqrt (+ x 16.0)) (cbrt 116.0)) (/ 1 (* (cbrt 116.0) (cbrt 116.0))) (/ (+ x 16.0) (cbrt 116.0)) (/ 1 (* (cbrt 116.0) (cbrt 116.0))) (/ (+ x 16.0) (cbrt 116.0)) (/ (* (cbrt (+ x 16.0)) (cbrt (+ x 16.0))) (sqrt 116.0)) (/ (cbrt (+ x 16.0)) (sqrt 116.0)) (/ (sqrt (+ x 16.0)) (sqrt 116.0)) (/ (sqrt (+ x 16.0)) (sqrt 116.0)) (/ 1 (sqrt 116.0)) (/ (+ x 16.0) (sqrt 116.0)) (/ 1 (sqrt 116.0)) (/ (+ x 16.0) (sqrt 116.0)) (* (cbrt (+ x 16.0)) (cbrt (+ x 16.0))) (/ (cbrt (+ x 16.0)) 116.0) (sqrt (+ x 16.0)) (/ (sqrt (+ x 16.0)) 116.0) 1 (/ (+ x 16.0) 116.0) 1 (/ (+ x 16.0) 116.0) 1 (/ (+ x 16.0) 116.0) (/ 1 116.0) (+ x 16.0) (/ (+ (pow 16.0 3) (pow x 3)) 116.0) (/ 1 (+ (* x x) (* 16.0 (- 16.0 x)))) (/ (- (* x x) (* 16.0 16.0)) 116.0) (/ 1 (- x 16.0)) (/ 1 (* (cbrt (/ 116.0 (+ x 16.0))) (cbrt (/ 116.0 (+ x 16.0))))) (/ 1 (cbrt (/ 116.0 (+ x 16.0)))) (/ 1 (sqrt (/ 116.0 (+ x 16.0)))) (/ 1 (sqrt (/ 116.0 (+ x 16.0)))) (/ (* (cbrt (+ x 16.0)) (cbrt (+ x 16.0))) (* (cbrt 116.0) (cbrt 116.0))) (/ (cbrt (+ x 16.0)) (cbrt 116.0)) (/ (sqrt (+ x 16.0)) (* (cbrt 116.0) (cbrt 116.0))) (/ (sqrt (+ x 16.0)) (cbrt 116.0)) (/ 1 (* (cbrt 116.0) (cbrt 116.0))) (/ (+ x 16.0) (cbrt 116.0)) (/ 1 (* (cbrt 116.0) (cbrt 116.0))) (/ (+ x 16.0) (cbrt 116.0)) (/ (* (cbrt (+ x 16.0)) (cbrt (+ x 16.0))) (sqrt 116.0)) (/ (cbrt (+ x 16.0)) (sqrt 116.0)) (/ (sqrt (+ x 16.0)) (sqrt 116.0)) (/ (sqrt (+ x 16.0)) (sqrt 116.0)) (/ 1 (sqrt 116.0)) (/ (+ x 16.0) (sqrt 116.0)) (/ 1 (sqrt 116.0)) (/ (+ x 16.0) (sqrt 116.0)) (* (cbrt (+ x 16.0)) (cbrt (+ x 16.0))) (/ (cbrt (+ x 16.0)) 116.0) (sqrt (+ x 16.0)) (/ (sqrt (+ x 16.0)) 116.0) 1 (/ (+ x 16.0) 116.0) 1 (/ (+ x 16.0) 116.0) 1 (/ (+ x 16.0) 116.0) (/ 1 116.0) (+ x 16.0) (/ (+ (pow x 3) (pow 16.0 3)) 116.0) (/ 1 (+ (* x x) (* 16.0 (- 16.0 x)))) (/ (- (* x x) (* 16.0 16.0)) 116.0) (/ 1 (- x 16.0)) (/ 1 (* (cbrt (/ 116.0 (+ x 16.0))) (cbrt (/ 116.0 (+ x 16.0))))) (/ 1 (cbrt (/ 116.0 (+ x 16.0)))) (/ 1 (sqrt (/ 116.0 (+ x 16.0)))) (/ 1 (sqrt (/ 116.0 (+ x 16.0)))) (/ (/ (* (cbrt (+ x 16.0)) (cbrt (+ x 16.0))) (cbrt 116.0)) (cbrt 116.0)) (/ (cbrt (+ x 16.0)) (cbrt 116.0)) (/ (sqrt (+ x 16.0)) (* (cbrt 116.0) (cbrt 116.0))) (/ (sqrt (+ x 16.0)) (cbrt 116.0)) (/ 1 (* (cbrt 116.0) (cbrt 116.0))) (/ (+ x 16.0) (cbrt 116.0)) (/ 1 (* (cbrt 116.0) (cbrt 116.0))) (/ (+ x 16.0) (cbrt 116.0)) (/ (* (cbrt (+ x 16.0)) (cbrt (+ x 16.0))) (sqrt 116.0)) (/ (cbrt (+ x 16.0)) (sqrt 116.0)) (/ (sqrt (+ x 16.0)) (sqrt 116.0)) (/ (sqrt (+ x 16.0)) (sqrt 116.0)) (/ 1 (sqrt 116.0)) (/ (+ x 16.0) (sqrt 116.0)) (/ 1 (sqrt 116.0)) (/ (+ x 16.0) (sqrt 116.0)) (* (cbrt (+ x 16.0)) (cbrt (+ x 16.0))) (/ (cbrt (+ x 16.0)) 116.0) (sqrt (+ x 16.0)) (/ (sqrt (+ x 16.0)) 116.0) 1 (/ (+ x 16.0) 116.0) 1 (/ (+ x 16.0) 116.0) 1 (/ (+ x 16.0) 116.0) (/ 1 116.0) (+ x 16.0) (/ (+ (pow x 3) (pow 16.0 3)) 116.0) (/ 1 (+ (* 16.0 (- 16.0 x)) (* x x))) (/ (- (* x x) (* 16.0 16.0)) 116.0) (/ 1 (- x 16.0)) (/ (+ x 16.0) 116.0) (/ 116.0 (+ x 16.0)) (/ 1 (* (cbrt (/ 116.0 (+ x 16.0))) (cbrt (/ 116.0 (+ x 16.0))))) (/ 1 (sqrt (/ 116.0 (+ x 16.0)))) (/ (/ (* (cbrt (+ x 16.0)) (cbrt (+ x 16.0))) (cbrt 116.0)) (cbrt 116.0)) (/ (sqrt (+ x 16.0)) (* (cbrt 116.0) (cbrt 116.0))) (/ 1 (* (cbrt 116.0) (cbrt 116.0))) (/ 1 (* (cbrt 116.0) (cbrt 116.0))) (/ (* (cbrt (+ x 16.0)) (cbrt (+ x 16.0))) (sqrt 116.0)) (/ (sqrt (+ x 16.0)) (sqrt 116.0)) (/ 1 (sqrt 116.0)) (/ 1 (sqrt 116.0)) (* (cbrt (+ x 16.0)) (cbrt (+ x 16.0))) (sqrt (+ x 16.0)) 1 1 1 (/ 1 116.0) (/ (+ (pow x 3) (pow 16.0 3)) 116.0) (/ (- (* x x) (* 16.0 16.0)) 116.0) (/ 116.0 (+ x 16.0)) (/ 116.0 (+ x 16.0)) (/ 116.0 (+ x 16.0)) (/ 1 116.0) (- (log 116.0) (log (+ x 16.0))) (log (/ 116.0 (+ x 16.0))) (exp (/ 116.0 (+ x 16.0))) (pow (/ 116.0 (+ x 16.0)) 3) (* (cbrt (/ 116.0 (+ x 16.0))) (cbrt (/ 116.0 (+ x 16.0)))) (cbrt (/ 116.0 (+ x 16.0))) (pow (/ 116.0 (+ x 16.0)) 3) (sqrt (/ 116.0 (+ x 16.0))) (sqrt (/ 116.0 (+ x 16.0))) (neg 116.0) (neg (+ x 16.0)) (/ (* (cbrt 116.0) (cbrt 116.0)) (* (cbrt (+ x 16.0)) (cbrt (+ x 16.0)))) (/ (cbrt 116.0) (cbrt (+ x 16.0))) (/ (* (cbrt 116.0) (cbrt 116.0)) (sqrt (+ x 16.0))) (/ (cbrt 116.0) (sqrt (+ x 16.0))) (* (cbrt 116.0) (cbrt 116.0)) (/ (cbrt 116.0) (+ x 16.0)) (* (cbrt 116.0) (cbrt 116.0)) (/ (cbrt 116.0) (+ x 16.0)) (/ (sqrt 116.0) (* (cbrt (+ x 16.0)) (cbrt (+ x 16.0)))) (/ (sqrt 116.0) (cbrt (+ x 16.0))) (/ (sqrt 116.0) (sqrt (+ x 16.0))) (/ (sqrt 116.0) (sqrt (+ x 16.0))) (sqrt 116.0) (/ (sqrt 116.0) (+ x 16.0)) (sqrt 116.0) (/ (sqrt 116.0) (+ x 16.0)) (/ 1 (* (cbrt (+ x 16.0)) (cbrt (+ x 16.0)))) (/ 116.0 (cbrt (+ x 16.0))) (/ 1 (sqrt (+ x 16.0))) (/ 116.0 (sqrt (+ x 16.0))) 1 (/ 116.0 (+ x 16.0)) 1 (/ 116.0 (+ x 16.0)) (/ 1 (+ x 16.0)) (/ (+ x 16.0) 116.0) (/ 116.0 (* (cbrt (+ x 16.0)) (cbrt (+ x 16.0)))) (/ 116.0 (sqrt (+ x 16.0))) 116.0 116.0 (/ (+ x 16.0) (cbrt 116.0)) (/ (+ x 16.0) (sqrt 116.0)) (/ (+ x 16.0) 116.0) (/ 116.0 (+ (pow x 3) (pow 16.0 3))) (/ 116.0 (- (* x x) (* 16.0 16.0))) (+ (* 0.008620689655172414 x) 0.13793103448275862) (+ (* 0.008620689655172414 x) 0.13793103448275862) (+ (* 0.008620689655172414 x) 0.13793103448275862) (- 7.25 (* x (- 0.453125 (* x 0.0283203125)))) (* (/ 1 x) (+ (/ (- (/ 29696.0 x) 1856.0) x) 116.0)) (* (/ 1 x) (+ (/ (- (/ 29696.0 x) 1856.0) x) 116.0)) 103.478 * * * [progress]: adding candidates to table 103.609 * [progress]: [Phase 3 of 3] Extracting. 103.609 * * [regime]: Finding splitpoints for: (# # #) 103.609 * * * [regime-changes]: Trying 3 branch expressions: ((+ x 16.0) (/ (+ x 16.0) 116.0) x) 103.609 * * * * [regimes]: Trying to branch on (+ x 16.0) from (# # #) 103.636 * * * * [regimes]: Trying to branch on (/ (+ x 16.0) 116.0) from (# # #) 103.663 * * * * [regimes]: Trying to branch on x from (# # #) 103.693 * * * [regime]: Found split indices: #