654.615 * [progress]: [Phase 1 of 3] Setting up. 0.001 * * * [progress]: [1/2] Preparing points 0.175 * * * [progress]: [2/2] Setting up program. 0.177 * [progress]: [Phase 2 of 3] Improving. 0.178 * [simplify]: Simplifying using # : (/ (- 1.0 (cos x)) (sin x)) 0.178 * * [simplify]: iteration 0 : 6 enodes (cost 7 ) 0.179 * * [simplify]: iteration 1 : 11 enodes (cost 7 ) 0.180 * * [simplify]: iteration 2 : 14 enodes (cost 7 ) 0.182 * * [simplify]: iteration 3 : 16 enodes (cost 7 ) 0.183 * * [simplify]: iteration done : 16 enodes (cost 7 ) 0.183 * [simplify]: Simplified to: (/ (- 1.0 (cos x)) (sin x)) 0.184 * * [progress]: iteration 1 / 4 0.184 * * * [progress]: picking best candidate 0.187 * * * * [pick]: Picked # 0.187 * * * [progress]: localizing error 0.194 * * * [progress]: generating rewritten candidates 0.194 * * * * [progress]: [ 1 / 3 ] rewriting at (2 1) 0.198 * * * * [progress]: [ 2 / 3 ] rewriting at (2) 0.205 * * * * [progress]: [ 3 / 3 ] rewriting at (2 2) 0.209 * * * [progress]: generating series expansions 0.209 * * * * [progress]: [ 1 / 3 ] generating series at (2 1) 0.209 * [approximate]: Taking taylor expansion of (- 1.0 (cos x)) in (x) around 0 0.209 * [taylor]: Taking taylor expansion of (- 1.0 (cos x)) in x 0.209 * [taylor]: Taking taylor expansion of 1.0 in x 0.209 * [taylor]: Taking taylor expansion of (cos x) in x 0.209 * [taylor]: Taking taylor expansion of x in x 0.209 * [taylor]: Taking taylor expansion of (- 1.0 (cos x)) in x 0.209 * [taylor]: Taking taylor expansion of 1.0 in x 0.209 * [taylor]: Taking taylor expansion of (cos x) in x 0.209 * [taylor]: Taking taylor expansion of x in x 0.211 * [approximate]: Taking taylor expansion of (- 1.0 (cos (/ 1 x))) in (x) around 0 0.211 * [taylor]: Taking taylor expansion of (- 1.0 (cos (/ 1 x))) in x 0.211 * [taylor]: Taking taylor expansion of 1.0 in x 0.211 * [taylor]: Taking taylor expansion of (cos (/ 1 x)) in x 0.211 * [taylor]: Taking taylor expansion of (/ 1 x) in x 0.211 * [taylor]: Taking taylor expansion of x in x 0.211 * [taylor]: Taking taylor expansion of (- 1.0 (cos (/ 1 x))) in x 0.211 * [taylor]: Taking taylor expansion of 1.0 in x 0.211 * [taylor]: Taking taylor expansion of (cos (/ 1 x)) in x 0.211 * [taylor]: Taking taylor expansion of (/ 1 x) in x 0.211 * [taylor]: Taking taylor expansion of x in x 0.211 * [approximate]: Taking taylor expansion of (- 1.0 (cos (/ -1 x))) in (x) around 0 0.211 * [taylor]: Taking taylor expansion of (- 1.0 (cos (/ -1 x))) in x 0.211 * [taylor]: Taking taylor expansion of 1.0 in x 0.211 * [taylor]: Taking taylor expansion of (cos (/ -1 x)) in x 0.211 * [taylor]: Taking taylor expansion of (/ -1 x) in x 0.212 * [taylor]: Taking taylor expansion of -1 in x 0.212 * [taylor]: Taking taylor expansion of x in x 0.212 * [taylor]: Taking taylor expansion of (- 1.0 (cos (/ -1 x))) in x 0.212 * [taylor]: Taking taylor expansion of 1.0 in x 0.212 * [taylor]: Taking taylor expansion of (cos (/ -1 x)) in x 0.212 * [taylor]: Taking taylor expansion of (/ -1 x) in x 0.212 * [taylor]: Taking taylor expansion of -1 in x 0.212 * [taylor]: Taking taylor expansion of x in x 0.212 * * * * [progress]: [ 2 / 3 ] generating series at (2) 0.212 * [approximate]: Taking taylor expansion of (/ (- 1.0 (cos x)) (sin x)) in (x) around 0 0.212 * [taylor]: Taking taylor expansion of (/ (- 1.0 (cos x)) (sin x)) in x 0.212 * [taylor]: Taking taylor expansion of (- 1.0 (cos x)) in x 0.212 * [taylor]: Taking taylor expansion of 1.0 in x 0.212 * [taylor]: Taking taylor expansion of (cos x) in x 0.212 * [taylor]: Taking taylor expansion of x in x 0.212 * [taylor]: Taking taylor expansion of (sin x) in x 0.212 * [taylor]: Taking taylor expansion of x in x 0.213 * [taylor]: Taking taylor expansion of (/ (- 1.0 (cos x)) (sin x)) in x 0.213 * [taylor]: Taking taylor expansion of (- 1.0 (cos x)) in x 0.213 * [taylor]: Taking taylor expansion of 1.0 in x 0.213 * [taylor]: Taking taylor expansion of (cos x) in x 0.213 * [taylor]: Taking taylor expansion of x in x 0.213 * [taylor]: Taking taylor expansion of (sin x) in x 0.213 * [taylor]: Taking taylor expansion of x in x 0.216 * [approximate]: Taking taylor expansion of (/ (- 1.0 (cos (/ 1 x))) (sin (/ 1 x))) in (x) around 0 0.216 * [taylor]: Taking taylor expansion of (/ (- 1.0 (cos (/ 1 x))) (sin (/ 1 x))) in x 0.216 * [taylor]: Taking taylor expansion of (- 1.0 (cos (/ 1 x))) in x 0.216 * [taylor]: Taking taylor expansion of 1.0 in x 0.216 * [taylor]: Taking taylor expansion of (cos (/ 1 x)) in x 0.216 * [taylor]: Taking taylor expansion of (/ 1 x) in x 0.216 * [taylor]: Taking taylor expansion of x in x 0.216 * [taylor]: Taking taylor expansion of (sin (/ 1 x)) in x 0.216 * [taylor]: Taking taylor expansion of (/ 1 x) in x 0.216 * [taylor]: Taking taylor expansion of x in x 0.217 * [taylor]: Taking taylor expansion of (/ (- 1.0 (cos (/ 1 x))) (sin (/ 1 x))) in x 0.217 * [taylor]: Taking taylor expansion of (- 1.0 (cos (/ 1 x))) in x 0.217 * [taylor]: Taking taylor expansion of 1.0 in x 0.217 * [taylor]: Taking taylor expansion of (cos (/ 1 x)) in x 0.217 * [taylor]: Taking taylor expansion of (/ 1 x) in x 0.217 * [taylor]: Taking taylor expansion of x in x 0.217 * [taylor]: Taking taylor expansion of (sin (/ 1 x)) in x 0.217 * [taylor]: Taking taylor expansion of (/ 1 x) in x 0.217 * [taylor]: Taking taylor expansion of x in x 0.219 * [approximate]: Taking taylor expansion of (/ (- 1.0 (cos (/ -1 x))) (sin (/ -1 x))) in (x) around 0 0.219 * [taylor]: Taking taylor expansion of (/ (- 1.0 (cos (/ -1 x))) (sin (/ -1 x))) in x 0.219 * [taylor]: Taking taylor expansion of (- 1.0 (cos (/ -1 x))) in x 0.219 * [taylor]: Taking taylor expansion of 1.0 in x 0.219 * [taylor]: Taking taylor expansion of (cos (/ -1 x)) in x 0.219 * [taylor]: Taking taylor expansion of (/ -1 x) in x 0.219 * [taylor]: Taking taylor expansion of -1 in x 0.219 * [taylor]: Taking taylor expansion of x in x 0.219 * [taylor]: Taking taylor expansion of (sin (/ -1 x)) in x 0.219 * [taylor]: Taking taylor expansion of (/ -1 x) in x 0.219 * [taylor]: Taking taylor expansion of -1 in x 0.219 * [taylor]: Taking taylor expansion of x in x 0.220 * [taylor]: Taking taylor expansion of (/ (- 1.0 (cos (/ -1 x))) (sin (/ -1 x))) in x 0.220 * [taylor]: Taking taylor expansion of (- 1.0 (cos (/ -1 x))) in x 0.220 * [taylor]: Taking taylor expansion of 1.0 in x 0.220 * [taylor]: Taking taylor expansion of (cos (/ -1 x)) in x 0.220 * [taylor]: Taking taylor expansion of (/ -1 x) in x 0.220 * [taylor]: Taking taylor expansion of -1 in x 0.220 * [taylor]: Taking taylor expansion of x in x 0.220 * [taylor]: Taking taylor expansion of (sin (/ -1 x)) in x 0.220 * [taylor]: Taking taylor expansion of (/ -1 x) in x 0.220 * [taylor]: Taking taylor expansion of -1 in x 0.220 * [taylor]: Taking taylor expansion of x in x 0.222 * * * * [progress]: [ 3 / 3 ] generating series at (2 2) 0.222 * [approximate]: Taking taylor expansion of (sin x) in (x) around 0 0.222 * [taylor]: Taking taylor expansion of (sin x) in x 0.222 * [taylor]: Taking taylor expansion of x in x 0.222 * [taylor]: Taking taylor expansion of (sin x) in x 0.222 * [taylor]: Taking taylor expansion of x in x 0.223 * [approximate]: Taking taylor expansion of (sin (/ 1 x)) in (x) around 0 0.223 * [taylor]: Taking taylor expansion of (sin (/ 1 x)) in x 0.223 * [taylor]: Taking taylor expansion of (/ 1 x) in x 0.223 * [taylor]: Taking taylor expansion of x in x 0.223 * [taylor]: Taking taylor expansion of (sin (/ 1 x)) in x 0.223 * [taylor]: Taking taylor expansion of (/ 1 x) in x 0.223 * [taylor]: Taking taylor expansion of x in x 0.223 * [approximate]: Taking taylor expansion of (sin (/ -1 x)) in (x) around 0 0.223 * [taylor]: Taking taylor expansion of (sin (/ -1 x)) in x 0.223 * [taylor]: Taking taylor expansion of (/ -1 x) in x 0.223 * [taylor]: Taking taylor expansion of -1 in x 0.223 * [taylor]: Taking taylor expansion of x in x 0.223 * [taylor]: Taking taylor expansion of (sin (/ -1 x)) in x 0.223 * [taylor]: Taking taylor expansion of (/ -1 x) in x 0.223 * [taylor]: Taking taylor expansion of -1 in x 0.224 * [taylor]: Taking taylor expansion of x in x 0.224 * * * [progress]: simplifying candidates 0.225 * [simplify]: Simplifying using # : (/ (exp 1.0) (exp (cos x))) (log (- 1.0 (cos x))) (exp (- 1.0 (cos x))) (* (cbrt (- 1.0 (cos x))) (cbrt (- 1.0 (cos x)))) (cbrt (- 1.0 (cos x))) (* (* (- 1.0 (cos x)) (- 1.0 (cos x))) (- 1.0 (cos x))) (sqrt (- 1.0 (cos x))) (sqrt (- 1.0 (cos x))) (- (pow 1.0 3) (pow (cos x) 3)) (+ (* 1.0 1.0) (+ (* (cos x) (cos x)) (* 1.0 (cos x)))) (neg (cos x)) (- (* 1.0 1.0) (* (cos x) (cos x))) (+ 1.0 (cos x)) (+ (sqrt 1.0) (sqrt (cos x))) (- (sqrt 1.0) (sqrt (cos x))) (- 1.0 (cos x)) (neg (cos x)) (- (log (- 1.0 (cos x))) (log (sin x))) (log (/ (- 1.0 (cos x)) (sin x))) (exp (/ (- 1.0 (cos x)) (sin x))) (/ (* (* (- 1.0 (cos x)) (- 1.0 (cos x))) (- 1.0 (cos x))) (* (* (sin x) (sin x)) (sin x))) (* (cbrt (/ (- 1.0 (cos x)) (sin x))) (cbrt (/ (- 1.0 (cos x)) (sin x)))) (cbrt (/ (- 1.0 (cos x)) (sin x))) (* (* (/ (- 1.0 (cos x)) (sin x)) (/ (- 1.0 (cos x)) (sin x))) (/ (- 1.0 (cos x)) (sin x))) (sqrt (/ (- 1.0 (cos x)) (sin x))) (sqrt (/ (- 1.0 (cos x)) (sin x))) (neg (- 1.0 (cos x))) (neg (sin x)) (/ 1.0 (sin x)) (/ (cos x) (sin x)) (/ (* (cbrt (- 1.0 (cos x))) (cbrt (- 1.0 (cos x)))) (* (cbrt (sin x)) (cbrt (sin x)))) (/ (cbrt (- 1.0 (cos x))) (cbrt (sin x))) (/ (* (cbrt (- 1.0 (cos x))) (cbrt (- 1.0 (cos x)))) (sqrt (sin x))) (/ (cbrt (- 1.0 (cos x))) (sqrt (sin x))) (/ (* (cbrt (- 1.0 (cos x))) (cbrt (- 1.0 (cos x)))) 1) (/ (cbrt (- 1.0 (cos x))) (sin x)) (/ (sqrt (- 1.0 (cos x))) (* (cbrt (sin x)) (cbrt (sin x)))) (/ (sqrt (- 1.0 (cos x))) (cbrt (sin x))) (/ (sqrt (- 1.0 (cos x))) (sqrt (sin x))) (/ (sqrt (- 1.0 (cos x))) (sqrt (sin x))) (/ (sqrt (- 1.0 (cos x))) 1) (/ (sqrt (- 1.0 (cos x))) (sin x)) (/ 1 (* (cbrt (sin x)) (cbrt (sin x)))) (/ (- 1.0 (cos x)) (cbrt (sin x))) (/ 1 (sqrt (sin x))) (/ (- 1.0 (cos x)) (sqrt (sin x))) (/ 1 1) (/ (- 1.0 (cos x)) (sin x)) (/ (+ (sqrt 1.0) (sqrt (cos x))) (* (cbrt (sin x)) (cbrt (sin x)))) (/ (- (sqrt 1.0) (sqrt (cos x))) (cbrt (sin x))) (/ (+ (sqrt 1.0) (sqrt (cos x))) (sqrt (sin x))) (/ (- (sqrt 1.0) (sqrt (cos x))) (sqrt (sin x))) (/ (+ (sqrt 1.0) (sqrt (cos x))) 1) (/ (- (sqrt 1.0) (sqrt (cos x))) (sin x)) (/ 1 (* (cbrt (sin x)) (cbrt (sin x)))) (/ (- 1.0 (cos x)) (cbrt (sin x))) (/ 1 (sqrt (sin x))) (/ (- 1.0 (cos x)) (sqrt (sin x))) (/ 1 1) (/ (- 1.0 (cos x)) (sin x)) (/ 1 (sin x)) (/ (sin x) (- 1.0 (cos x))) (/ (- 1.0 (cos x)) (* (cbrt (sin x)) (cbrt (sin x)))) (/ (- 1.0 (cos x)) (sqrt (sin x))) (/ (- 1.0 (cos x)) 1) (/ (sin x) (cbrt (- 1.0 (cos x)))) (/ (sin x) (sqrt (- 1.0 (cos x)))) (/ (sin x) (- 1.0 (cos x))) (/ (sin x) (- (sqrt 1.0) (sqrt (cos x)))) (/ (sin x) (- 1.0 (cos x))) (* (sin x) (+ (* 1.0 1.0) (+ (* (cos x) (cos x)) (* 1.0 (cos x))))) (* (sin x) (+ 1.0 (cos x))) (log (sin x)) (exp (sin x)) (* (cbrt (sin x)) (cbrt (sin x))) (cbrt (sin x)) (* (* (sin x) (sin x)) (sin x)) (sqrt (sin x)) (sqrt (sin x)) (- (+ (* 1/2 (pow x 2)) (* 1/720 (pow x 6))) (* 1/24 (pow x 4))) (- 1.0 (cos x)) (- 1.0 (cos x)) (+ (* 1/2 x) (+ (* 1/24 (pow x 3)) (* 1/240 (pow x 5)))) (/ (- 1.0 (cos x)) (sin x)) (/ (- 1.0 (cos x)) (sin x)) (- (+ x (* 1/120 (pow x 5))) (* 1/6 (pow x 3))) (sin x) (sin x) 0.225 * * [simplify]: iteration 0 : 6 enodes (cost 6 ) 0.226 * * [simplify]: iteration 1 : 8 enodes (cost 5 ) 0.227 * * [simplify]: iteration 2 : 10 enodes (cost 5 ) 0.228 * * [simplify]: iteration 3 : 13 enodes (cost 5 ) 0.229 * * [simplify]: iteration 4 : 16 enodes (cost 5 ) 0.231 * * [simplify]: iteration 5 : 22 enodes (cost 5 ) 0.233 * * [simplify]: iteration 6 : 26 enodes (cost 5 ) 0.237 * * [simplify]: iteration 7 : 42 enodes (cost 5 ) 0.242 * * [simplify]: iteration 8 : 46 enodes (cost 5 ) 0.251 * * [simplify]: iteration 9 : 51 enodes (cost 5 ) 0.258 * * [simplify]: iteration 10 : 58 enodes (cost 5 ) 0.265 * * [simplify]: iteration 11 : 76 enodes (cost 5 ) 0.275 * * [simplify]: iteration 12 : 97 enodes (cost 5 ) 0.288 * * [simplify]: iteration 13 : 115 enodes (cost 5 ) 0.303 * * [simplify]: iteration 14 : 118 enodes (cost 5 ) 0.320 * * [simplify]: iteration done : 118 enodes (cost 5 ) 0.321 * * [simplify]: iteration 0 : 5 enodes (cost 5 ) 0.321 * * [simplify]: iteration 1 : 7 enodes (cost 5 ) 0.322 * * [simplify]: iteration 2 : 8 enodes (cost 5 ) 0.323 * * [simplify]: iteration done : 8 enodes (cost 5 ) 0.323 * * [simplify]: iteration 0 : 5 enodes (cost 5 ) 0.324 * * [simplify]: iteration 1 : 10 enodes (cost 5 ) 0.325 * * [simplify]: iteration 2 : 13 enodes (cost 5 ) 0.326 * * [simplify]: iteration 3 : 16 enodes (cost 5 ) 0.328 * * [simplify]: iteration 4 : 22 enodes (cost 5 ) 0.330 * * [simplify]: iteration 5 : 26 enodes (cost 5 ) 0.334 * * [simplify]: iteration 6 : 42 enodes (cost 5 ) 0.339 * * [simplify]: iteration 7 : 46 enodes (cost 5 ) 0.343 * * [simplify]: iteration 8 : 51 enodes (cost 5 ) 0.349 * * [simplify]: iteration 9 : 58 enodes (cost 5 ) 0.356 * * [simplify]: iteration 10 : 77 enodes (cost 5 ) 0.370 * * [simplify]: iteration 11 : 98 enodes (cost 5 ) 0.384 * * [simplify]: iteration 12 : 111 enodes (cost 5 ) 0.398 * * [simplify]: iteration 13 : 114 enodes (cost 5 ) 0.411 * * [simplify]: iteration done : 114 enodes (cost 5 ) 0.412 * * [simplify]: iteration 0 : 6 enodes (cost 11 ) 0.412 * * [simplify]: iteration 1 : 8 enodes (cost 11 ) 0.413 * * [simplify]: iteration 2 : 9 enodes (cost 11 ) 0.414 * * [simplify]: iteration done : 9 enodes (cost 11 ) 0.414 * * [simplify]: iteration 0 : 5 enodes (cost 5 ) 0.415 * * [simplify]: iteration 1 : 7 enodes (cost 5 ) 0.416 * * [simplify]: iteration 2 : 8 enodes (cost 5 ) 0.416 * * [simplify]: iteration done : 8 enodes (cost 5 ) 0.417 * * [simplify]: iteration 0 : 6 enodes (cost 14 ) 0.418 * * [simplify]: iteration 1 : 9 enodes (cost 14 ) 0.419 * * [simplify]: iteration 2 : 24 enodes (cost 6 ) 0.423 * * [simplify]: iteration 3 : 67 enodes (cost 6 ) 0.442 * * [simplify]: iteration 4 : 176 enodes (cost 6 ) 0.509 * * [simplify]: iteration 5 : 500 enodes (cost 6 ) 0.982 * * [simplify]: iteration 6 : 1723 enodes (cost 6 ) 4.113 * * [simplify]: iteration 7 : 4988 enodes (cost 6 ) 5.324 * * [simplify]: iteration done : 5000 enodes (cost 6 ) 5.325 * * [simplify]: iteration 0 : 5 enodes (cost 5 ) 5.326 * * [simplify]: iteration 1 : 7 enodes (cost 5 ) 5.326 * * [simplify]: iteration 2 : 8 enodes (cost 5 ) 5.327 * * [simplify]: iteration done : 8 enodes (cost 5 ) 5.327 * * [simplify]: iteration 0 : 5 enodes (cost 5 ) 5.328 * * [simplify]: iteration 1 : 7 enodes (cost 5 ) 5.329 * * [simplify]: iteration 2 : 8 enodes (cost 5 ) 5.329 * * [simplify]: iteration done : 8 enodes (cost 5 ) 5.330 * * [simplify]: iteration 0 : 7 enodes (cost 8 ) 5.331 * * [simplify]: iteration 1 : 22 enodes (cost 8 ) 5.334 * * [simplify]: iteration 2 : 44 enodes (cost 8 ) 5.340 * * [simplify]: iteration 3 : 78 enodes (cost 8 ) 5.354 * * [simplify]: iteration 4 : 165 enodes (cost 8 ) 5.405 * * [simplify]: iteration 5 : 500 enodes (cost 8 ) 5.762 * * [simplify]: iteration 6 : 2253 enodes (cost 8 ) 6.941 * * [simplify]: iteration done : 5001 enodes (cost 8 ) 6.942 * * [simplify]: iteration 0 : 8 enodes (cost 14 ) 6.943 * * [simplify]: iteration 1 : 15 enodes (cost 11 ) 6.945 * * [simplify]: iteration 2 : 23 enodes (cost 11 ) 6.949 * * [simplify]: iteration 3 : 26 enodes (cost 11 ) 6.953 * * [simplify]: iteration 4 : 27 enodes (cost 11 ) 6.957 * * [simplify]: iteration done : 27 enodes (cost 11 ) 6.957 * * [simplify]: iteration 0 : 3 enodes (cost 3 ) 6.957 * * [simplify]: iteration done : 3 enodes (cost 3 ) 6.958 * * [simplify]: iteration 0 : 6 enodes (cost 9 ) 6.959 * * [simplify]: iteration 1 : 11 enodes (cost 9 ) 6.960 * * [simplify]: iteration 2 : 18 enodes (cost 9 ) 6.963 * * [simplify]: iteration 3 : 33 enodes (cost 9 ) 6.974 * * [simplify]: iteration 4 : 58 enodes (cost 9 ) 6.985 * * [simplify]: iteration 5 : 99 enodes (cost 9 ) 7.009 * * [simplify]: iteration 6 : 161 enodes (cost 9 ) 7.065 * * [simplify]: iteration 7 : 329 enodes (cost 9 ) 7.805 * * [simplify]: iteration 8 : 1606 enodes (cost 9 ) 13.918 * * [simplify]: iteration done : 5000 enodes (cost 9 ) 13.918 * * [simplify]: iteration 0 : 4 enodes (cost 4 ) 13.924 * * [simplify]: iteration 1 : 5 enodes (cost 4 ) 13.929 * * [simplify]: iteration done : 5 enodes (cost 4 ) 13.929 * * [simplify]: iteration 0 : 6 enodes (cost 6 ) 13.930 * * [simplify]: iteration 1 : 7 enodes (cost 6 ) 13.931 * * [simplify]: iteration done : 7 enodes (cost 6 ) 13.931 * * [simplify]: iteration 0 : 6 enodes (cost 6 ) 13.932 * * [simplify]: iteration 1 : 8 enodes (cost 6 ) 13.932 * * [simplify]: iteration 2 : 9 enodes (cost 6 ) 13.933 * * [simplify]: iteration done : 9 enodes (cost 6 ) 13.934 * * [simplify]: iteration 0 : 4 enodes (cost 4 ) 13.934 * * [simplify]: iteration 1 : 6 enodes (cost 4 ) 13.935 * * [simplify]: iteration 2 : 7 enodes (cost 4 ) 13.936 * * [simplify]: iteration done : 7 enodes (cost 4 ) 13.936 * * [simplify]: iteration 0 : 3 enodes (cost 3 ) 13.936 * * [simplify]: iteration done : 3 enodes (cost 3 ) 13.937 * * [simplify]: iteration 0 : 8 enodes (cost 9 ) 13.938 * * [simplify]: iteration 1 : 12 enodes (cost 9 ) 13.939 * * [simplify]: iteration 2 : 14 enodes (cost 9 ) 13.940 * * [simplify]: iteration done : 14 enodes (cost 9 ) 13.941 * * [simplify]: iteration 0 : 7 enodes (cost 8 ) 13.942 * * [simplify]: iteration 1 : 15 enodes (cost 8 ) 13.943 * * [simplify]: iteration 2 : 20 enodes (cost 8 ) 13.945 * * [simplify]: iteration 3 : 23 enodes (cost 8 ) 13.948 * * [simplify]: iteration done : 23 enodes (cost 8 ) 13.948 * * [simplify]: iteration 0 : 7 enodes (cost 8 ) 13.949 * * [simplify]: iteration 1 : 12 enodes (cost 8 ) 13.950 * * [simplify]: iteration 2 : 18 enodes (cost 8 ) 13.952 * * [simplify]: iteration 3 : 22 enodes (cost 8 ) 13.954 * * [simplify]: iteration 4 : 25 enodes (cost 8 ) 13.957 * * [simplify]: iteration 5 : 31 enodes (cost 8 ) 13.961 * * [simplify]: iteration 6 : 35 enodes (cost 8 ) 13.965 * * [simplify]: iteration 7 : 51 enodes (cost 8 ) 13.971 * * [simplify]: iteration 8 : 55 enodes (cost 8 ) 13.978 * * [simplify]: iteration 9 : 62 enodes (cost 8 ) 13.985 * * [simplify]: iteration 10 : 71 enodes (cost 8 ) 13.997 * * [simplify]: iteration 11 : 91 enodes (cost 8 ) 14.008 * * [simplify]: iteration 12 : 112 enodes (cost 8 ) 14.023 * * [simplify]: iteration 13 : 126 enodes (cost 8 ) 14.040 * * [simplify]: iteration 14 : 133 enodes (cost 8 ) 14.058 * * [simplify]: iteration 15 : 139 enodes (cost 8 ) 14.074 * * [simplify]: iteration 16 : 143 enodes (cost 8 ) 14.090 * * [simplify]: iteration done : 143 enodes (cost 8 ) 14.090 * * [simplify]: iteration 0 : 10 enodes (cost 23 ) 14.092 * * [simplify]: iteration 1 : 21 enodes (cost 23 ) 14.096 * * [simplify]: iteration 2 : 69 enodes (cost 11 ) 14.113 * * [simplify]: iteration 3 : 204 enodes (cost 9 ) 14.174 * * [simplify]: iteration 4 : 563 enodes (cost 9 ) 14.505 * * [simplify]: iteration 5 : 2032 enodes (cost 9 ) 15.843 * * [simplify]: iteration done : 5000 enodes (cost 9 ) 15.844 * * [simplify]: iteration 0 : 8 enodes (cost 17 ) 15.845 * * [simplify]: iteration 1 : 13 enodes (cost 17 ) 15.850 * * [simplify]: iteration 2 : 16 enodes (cost 17 ) 15.851 * * [simplify]: iteration 3 : 18 enodes (cost 17 ) 15.853 * * [simplify]: iteration done : 18 enodes (cost 17 ) 15.854 * * [simplify]: iteration 0 : 7 enodes (cost 8 ) 15.854 * * [simplify]: iteration 1 : 12 enodes (cost 8 ) 15.856 * * [simplify]: iteration 2 : 15 enodes (cost 8 ) 15.857 * * [simplify]: iteration 3 : 17 enodes (cost 8 ) 15.859 * * [simplify]: iteration done : 17 enodes (cost 8 ) 15.860 * * [simplify]: iteration 0 : 8 enodes (cost 23 ) 15.861 * * [simplify]: iteration 1 : 20 enodes (cost 23 ) 15.864 * * [simplify]: iteration 2 : 51 enodes (cost 9 ) 15.875 * * [simplify]: iteration 3 : 177 enodes (cost 9 ) 15.934 * * [simplify]: iteration 4 : 572 enodes (cost 9 ) 16.258 * * [simplify]: iteration 5 : 1721 enodes (cost 9 ) 17.865 * * [simplify]: iteration done : 5000 enodes (cost 9 ) 17.866 * * [simplify]: iteration 0 : 7 enodes (cost 8 ) 17.867 * * [simplify]: iteration 1 : 12 enodes (cost 8 ) 17.868 * * [simplify]: iteration 2 : 15 enodes (cost 8 ) 17.869 * * [simplify]: iteration 3 : 17 enodes (cost 8 ) 17.871 * * [simplify]: iteration done : 17 enodes (cost 8 ) 17.872 * * [simplify]: iteration 0 : 7 enodes (cost 8 ) 17.872 * * [simplify]: iteration 1 : 12 enodes (cost 8 ) 17.874 * * [simplify]: iteration 2 : 15 enodes (cost 8 ) 17.875 * * [simplify]: iteration 3 : 17 enodes (cost 8 ) 17.877 * * [simplify]: iteration done : 17 enodes (cost 8 ) 17.878 * * [simplify]: iteration 0 : 5 enodes (cost 5 ) 17.878 * * [simplify]: iteration 1 : 7 enodes (cost 5 ) 17.879 * * [simplify]: iteration 2 : 11 enodes (cost 5 ) 17.880 * * [simplify]: iteration 3 : 13 enodes (cost 5 ) 17.881 * * [simplify]: iteration 4 : 14 enodes (cost 4 ) 17.883 * * [simplify]: iteration done : 14 enodes (cost 4 ) 17.883 * * [simplify]: iteration 0 : 3 enodes (cost 3 ) 17.884 * * [simplify]: iteration done : 3 enodes (cost 3 ) 17.884 * * [simplify]: iteration 0 : 4 enodes (cost 4 ) 17.885 * * [simplify]: iteration done : 4 enodes (cost 4 ) 17.885 * * [simplify]: iteration 0 : 4 enodes (cost 5 ) 17.886 * * [simplify]: iteration done : 4 enodes (cost 5 ) 17.886 * * [simplify]: iteration 0 : 10 enodes (cost 19 ) 17.888 * * [simplify]: iteration 1 : 18 enodes (cost 19 ) 17.890 * * [simplify]: iteration 2 : 28 enodes (cost 19 ) 17.893 * * [simplify]: iteration 3 : 34 enodes (cost 19 ) 17.897 * * [simplify]: iteration done : 34 enodes (cost 19 ) 17.898 * * [simplify]: iteration 0 : 8 enodes (cost 9 ) 17.898 * * [simplify]: iteration 1 : 10 enodes (cost 9 ) 17.899 * * [simplify]: iteration 2 : 11 enodes (cost 9 ) 17.900 * * [simplify]: iteration done : 11 enodes (cost 9 ) 17.901 * * [simplify]: iteration 0 : 9 enodes (cost 15 ) 17.902 * * [simplify]: iteration 1 : 13 enodes (cost 15 ) 17.903 * * [simplify]: iteration 2 : 16 enodes (cost 15 ) 17.905 * * [simplify]: iteration 3 : 17 enodes (cost 15 ) 17.906 * * [simplify]: iteration done : 17 enodes (cost 15 ) 17.907 * * [simplify]: iteration 0 : 8 enodes (cost 9 ) 17.908 * * [simplify]: iteration 1 : 10 enodes (cost 9 ) 17.909 * * [simplify]: iteration 2 : 11 enodes (cost 9 ) 17.910 * * [simplify]: iteration done : 11 enodes (cost 9 ) 17.910 * * [simplify]: iteration 0 : 8 enodes (cost 13 ) 17.911 * * [simplify]: iteration 1 : 14 enodes (cost 11 ) 17.913 * * [simplify]: iteration 2 : 21 enodes (cost 11 ) 17.916 * * [simplify]: iteration 3 : 26 enodes (cost 11 ) 17.918 * * [simplify]: iteration done : 26 enodes (cost 11 ) 17.919 * * [simplify]: iteration 0 : 7 enodes (cost 8 ) 17.920 * * [simplify]: iteration 1 : 9 enodes (cost 8 ) 17.920 * * [simplify]: iteration 2 : 10 enodes (cost 8 ) 17.921 * * [simplify]: iteration done : 10 enodes (cost 8 ) 17.922 * * [simplify]: iteration 0 : 9 enodes (cost 13 ) 17.923 * * [simplify]: iteration 1 : 13 enodes (cost 13 ) 17.924 * * [simplify]: iteration 2 : 14 enodes (cost 13 ) 17.926 * * [simplify]: iteration done : 14 enodes (cost 13 ) 17.926 * * [simplify]: iteration 0 : 8 enodes (cost 9 ) 17.927 * * [simplify]: iteration 1 : 10 enodes (cost 9 ) 17.928 * * [simplify]: iteration 2 : 11 enodes (cost 9 ) 17.929 * * [simplify]: iteration done : 11 enodes (cost 9 ) 17.930 * * [simplify]: iteration 0 : 8 enodes (cost 9 ) 17.931 * * [simplify]: iteration 1 : 10 enodes (cost 9 ) 17.932 * * [simplify]: iteration 2 : 11 enodes (cost 9 ) 17.932 * * [simplify]: iteration done : 11 enodes (cost 9 ) 17.933 * * [simplify]: iteration 0 : 8 enodes (cost 9 ) 17.934 * * [simplify]: iteration 1 : 10 enodes (cost 9 ) 17.935 * * [simplify]: iteration 2 : 11 enodes (cost 9 ) 17.936 * * [simplify]: iteration done : 11 enodes (cost 9 ) 17.937 * * [simplify]: iteration 0 : 7 enodes (cost 7 ) 17.937 * * [simplify]: iteration 1 : 11 enodes (cost 5 ) 17.938 * * [simplify]: iteration 2 : 14 enodes (cost 5 ) 17.939 * * [simplify]: iteration done : 14 enodes (cost 5 ) 17.940 * * [simplify]: iteration 0 : 7 enodes (cost 8 ) 17.941 * * [simplify]: iteration 1 : 9 enodes (cost 8 ) 17.942 * * [simplify]: iteration 2 : 10 enodes (cost 8 ) 17.943 * * [simplify]: iteration done : 10 enodes (cost 8 ) 17.943 * * [simplify]: iteration 0 : 6 enodes (cost 9 ) 17.944 * * [simplify]: iteration 1 : 10 enodes (cost 9 ) 17.945 * * [simplify]: iteration done : 10 enodes (cost 9 ) 17.945 * * [simplify]: iteration 0 : 7 enodes (cost 8 ) 17.946 * * [simplify]: iteration 1 : 12 enodes (cost 8 ) 17.947 * * [simplify]: iteration 2 : 15 enodes (cost 8 ) 17.949 * * [simplify]: iteration 3 : 17 enodes (cost 8 ) 17.950 * * [simplify]: iteration done : 17 enodes (cost 8 ) 17.951 * * [simplify]: iteration 0 : 5 enodes (cost 5 ) 17.951 * * [simplify]: iteration 1 : 7 enodes (cost 5 ) 17.952 * * [simplify]: iteration done : 7 enodes (cost 5 ) 17.953 * * [simplify]: iteration 0 : 7 enodes (cost 8 ) 17.953 * * [simplify]: iteration 1 : 12 enodes (cost 8 ) 17.955 * * [simplify]: iteration 2 : 15 enodes (cost 8 ) 17.956 * * [simplify]: iteration 3 : 17 enodes (cost 8 ) 17.958 * * [simplify]: iteration done : 17 enodes (cost 8 ) 17.958 * * [simplify]: iteration 0 : 2 enodes (cost 3 ) 17.959 * * [simplify]: iteration 1 : 4 enodes (cost 1 ) 17.959 * * [simplify]: iteration done : 4 enodes (cost 1 ) 17.959 * * [simplify]: iteration 0 : 6 enodes (cost 7 ) 17.960 * * [simplify]: iteration 1 : 11 enodes (cost 7 ) 17.961 * * [simplify]: iteration 2 : 14 enodes (cost 7 ) 17.963 * * [simplify]: iteration 3 : 16 enodes (cost 7 ) 17.964 * * [simplify]: iteration done : 16 enodes (cost 7 ) 17.965 * * [simplify]: iteration 0 : 10 enodes (cost 14 ) 17.966 * * [simplify]: iteration 1 : 13 enodes (cost 14 ) 17.967 * * [simplify]: iteration done : 13 enodes (cost 14 ) 17.968 * * [simplify]: iteration 0 : 9 enodes (cost 10 ) 17.969 * * [simplify]: iteration 1 : 14 enodes (cost 10 ) 17.970 * * [simplify]: iteration 2 : 17 enodes (cost 10 ) 17.971 * * [simplify]: iteration 3 : 19 enodes (cost 10 ) 17.973 * * [simplify]: iteration done : 19 enodes (cost 10 ) 17.974 * * [simplify]: iteration 0 : 9 enodes (cost 10 ) 17.975 * * [simplify]: iteration 1 : 10 enodes (cost 10 ) 17.975 * * [simplify]: iteration done : 10 enodes (cost 10 ) 17.976 * * [simplify]: iteration 0 : 9 enodes (cost 10 ) 17.977 * * [simplify]: iteration 1 : 14 enodes (cost 10 ) 17.978 * * [simplify]: iteration 2 : 17 enodes (cost 10 ) 17.980 * * [simplify]: iteration 3 : 19 enodes (cost 10 ) 17.985 * * [simplify]: iteration done : 19 enodes (cost 10 ) 17.985 * * [simplify]: iteration 0 : 8 enodes (cost 8 ) 17.986 * * [simplify]: iteration 1 : 11 enodes (cost 6 ) 17.987 * * [simplify]: iteration 2 : 13 enodes (cost 6 ) 17.988 * * [simplify]: iteration done : 13 enodes (cost 6 ) 17.989 * * [simplify]: iteration 0 : 8 enodes (cost 9 ) 17.989 * * [simplify]: iteration 1 : 13 enodes (cost 9 ) 17.991 * * [simplify]: iteration 2 : 16 enodes (cost 9 ) 17.992 * * [simplify]: iteration 3 : 18 enodes (cost 9 ) 17.994 * * [simplify]: iteration done : 18 enodes (cost 9 ) 17.994 * * [simplify]: iteration 0 : 6 enodes (cost 9 ) 17.995 * * [simplify]: iteration 1 : 10 enodes (cost 9 ) 17.996 * * [simplify]: iteration done : 10 enodes (cost 9 ) 17.997 * * [simplify]: iteration 0 : 7 enodes (cost 8 ) 17.997 * * [simplify]: iteration 1 : 12 enodes (cost 8 ) 17.999 * * [simplify]: iteration 2 : 15 enodes (cost 8 ) 18.000 * * [simplify]: iteration 3 : 17 enodes (cost 8 ) 18.002 * * [simplify]: iteration done : 17 enodes (cost 8 ) 18.003 * * [simplify]: iteration 0 : 5 enodes (cost 5 ) 18.003 * * [simplify]: iteration 1 : 7 enodes (cost 5 ) 18.004 * * [simplify]: iteration done : 7 enodes (cost 5 ) 18.004 * * [simplify]: iteration 0 : 7 enodes (cost 8 ) 18.005 * * [simplify]: iteration 1 : 12 enodes (cost 8 ) 18.006 * * [simplify]: iteration 2 : 15 enodes (cost 8 ) 18.008 * * [simplify]: iteration 3 : 17 enodes (cost 8 ) 18.009 * * [simplify]: iteration done : 17 enodes (cost 8 ) 18.010 * * [simplify]: iteration 0 : 2 enodes (cost 3 ) 18.010 * * [simplify]: iteration 1 : 4 enodes (cost 1 ) 18.010 * * [simplify]: iteration done : 4 enodes (cost 1 ) 18.011 * * [simplify]: iteration 0 : 6 enodes (cost 7 ) 18.012 * * [simplify]: iteration 1 : 11 enodes (cost 7 ) 18.013 * * [simplify]: iteration 2 : 14 enodes (cost 7 ) 18.015 * * [simplify]: iteration 3 : 16 enodes (cost 7 ) 18.016 * * [simplify]: iteration done : 16 enodes (cost 7 ) 18.017 * * [simplify]: iteration 0 : 4 enodes (cost 4 ) 18.017 * * [simplify]: iteration 1 : 6 enodes (cost 4 ) 18.018 * * [simplify]: iteration done : 6 enodes (cost 4 ) 18.018 * * [simplify]: iteration 0 : 6 enodes (cost 7 ) 18.019 * * [simplify]: iteration 1 : 8 enodes (cost 7 ) 18.020 * * [simplify]: iteration 2 : 9 enodes (cost 7 ) 18.020 * * [simplify]: iteration done : 9 enodes (cost 7 ) 18.021 * * [simplify]: iteration 0 : 8 enodes (cost 12 ) 18.022 * * [simplify]: iteration 1 : 15 enodes (cost 12 ) 18.024 * * [simplify]: iteration 2 : 23 enodes (cost 12 ) 18.026 * * [simplify]: iteration 3 : 28 enodes (cost 12 ) 18.029 * * [simplify]: iteration 4 : 31 enodes (cost 12 ) 18.033 * * [simplify]: iteration done : 31 enodes (cost 12 ) 18.033 * * [simplify]: iteration 0 : 7 enodes (cost 8 ) 18.034 * * [simplify]: iteration 1 : 12 enodes (cost 8 ) 18.035 * * [simplify]: iteration 2 : 15 enodes (cost 8 ) 18.037 * * [simplify]: iteration 3 : 17 enodes (cost 8 ) 18.039 * * [simplify]: iteration done : 17 enodes (cost 8 ) 18.040 * * [simplify]: iteration 0 : 6 enodes (cost 6 ) 18.040 * * [simplify]: iteration 1 : 13 enodes (cost 4 ) 18.042 * * [simplify]: iteration 2 : 18 enodes (cost 4 ) 18.043 * * [simplify]: iteration 3 : 19 enodes (cost 4 ) 18.044 * * [simplify]: iteration done : 19 enodes (cost 4 ) 18.045 * * [simplify]: iteration 0 : 7 enodes (cost 8 ) 18.045 * * [simplify]: iteration 1 : 9 enodes (cost 8 ) 18.046 * * [simplify]: iteration 2 : 10 enodes (cost 8 ) 18.047 * * [simplify]: iteration done : 10 enodes (cost 8 ) 18.048 * * [simplify]: iteration 0 : 7 enodes (cost 8 ) 18.051 * * [simplify]: iteration 1 : 9 enodes (cost 8 ) 18.052 * * [simplify]: iteration 2 : 10 enodes (cost 8 ) 18.053 * * [simplify]: iteration done : 10 enodes (cost 8 ) 18.053 * * [simplify]: iteration 0 : 6 enodes (cost 7 ) 18.054 * * [simplify]: iteration 1 : 8 enodes (cost 7 ) 18.055 * * [simplify]: iteration 2 : 9 enodes (cost 7 ) 18.056 * * [simplify]: iteration done : 9 enodes (cost 7 ) 18.056 * * [simplify]: iteration 0 : 8 enodes (cost 9 ) 18.057 * * [simplify]: iteration 1 : 10 enodes (cost 9 ) 18.058 * * [simplify]: iteration 2 : 11 enodes (cost 9 ) 18.059 * * [simplify]: iteration done : 11 enodes (cost 9 ) 18.060 * * [simplify]: iteration 0 : 6 enodes (cost 7 ) 18.061 * * [simplify]: iteration 1 : 8 enodes (cost 7 ) 18.061 * * [simplify]: iteration 2 : 9 enodes (cost 7 ) 18.062 * * [simplify]: iteration done : 9 enodes (cost 7 ) 18.063 * * [simplify]: iteration 0 : 10 enodes (cost 17 ) 18.064 * * [simplify]: iteration 1 : 24 enodes (cost 14 ) 18.068 * * [simplify]: iteration 2 : 53 enodes (cost 14 ) 18.078 * * [simplify]: iteration 3 : 79 enodes (cost 14 ) 18.094 * * [simplify]: iteration 4 : 90 enodes (cost 14 ) 18.111 * * [simplify]: iteration 5 : 92 enodes (cost 14 ) 18.127 * * [simplify]: iteration done : 92 enodes (cost 14 ) 18.128 * * [simplify]: iteration 0 : 6 enodes (cost 7 ) 18.129 * * [simplify]: iteration 1 : 14 enodes (cost 7 ) 18.130 * * [simplify]: iteration 2 : 15 enodes (cost 7 ) 18.132 * * [simplify]: iteration done : 15 enodes (cost 7 ) 18.133 * * [simplify]: iteration 0 : 3 enodes (cost 3 ) 18.133 * * [simplify]: iteration done : 3 enodes (cost 3 ) 18.134 * * [simplify]: iteration 0 : 3 enodes (cost 3 ) 18.134 * * [simplify]: iteration done : 3 enodes (cost 3 ) 18.134 * * [simplify]: iteration 0 : 4 enodes (cost 7 ) 18.135 * * [simplify]: iteration done : 4 enodes (cost 7 ) 18.135 * * [simplify]: iteration 0 : 3 enodes (cost 3 ) 18.136 * * [simplify]: iteration done : 3 enodes (cost 3 ) 18.136 * * [simplify]: iteration 0 : 4 enodes (cost 8 ) 18.137 * * [simplify]: iteration 1 : 5 enodes (cost 8 ) 18.138 * * [simplify]: iteration 2 : 7 enodes (cost 4 ) 18.139 * * [simplify]: iteration 3 : 12 enodes (cost 4 ) 18.140 * * [simplify]: iteration 4 : 18 enodes (cost 4 ) 18.142 * * [simplify]: iteration 5 : 28 enodes (cost 4 ) 18.145 * * [simplify]: iteration 6 : 49 enodes (cost 4 ) 18.154 * * [simplify]: iteration 7 : 108 enodes (cost 4 ) 18.199 * * [simplify]: iteration 8 : 316 enodes (cost 4 ) 18.650 * * [simplify]: iteration 9 : 1236 enodes (cost 4 ) 21.029 * * [simplify]: iteration done : 5000 enodes (cost 4 ) 21.029 * * [simplify]: iteration 0 : 3 enodes (cost 3 ) 21.030 * * [simplify]: iteration done : 3 enodes (cost 3 ) 21.030 * * [simplify]: iteration 0 : 3 enodes (cost 3 ) 21.031 * * [simplify]: iteration done : 3 enodes (cost 3 ) 21.031 * * [simplify]: iteration 0 : 15 enodes (cost 17 ) 21.033 * * [simplify]: iteration 1 : 35 enodes (cost 17 ) 21.040 * * [simplify]: iteration 2 : 92 enodes (cost 17 ) 21.054 * * [simplify]: iteration 3 : 193 enodes (cost 17 ) 21.117 * * [simplify]: iteration 4 : 496 enodes (cost 17 ) 21.406 * * [simplify]: iteration 5 : 1268 enodes (cost 17 ) 22.991 * * [simplify]: iteration 6 : 3919 enodes (cost 17 ) 25.172 * * [simplify]: iteration done : 5001 enodes (cost 17 ) 25.173 * * [simplify]: iteration 0 : 4 enodes (cost 4 ) 25.173 * * [simplify]: iteration 1 : 6 enodes (cost 4 ) 25.174 * * [simplify]: iteration 2 : 7 enodes (cost 4 ) 25.174 * * [simplify]: iteration done : 7 enodes (cost 4 ) 25.175 * * [simplify]: iteration 0 : 4 enodes (cost 4 ) 25.176 * * [simplify]: iteration 1 : 6 enodes (cost 4 ) 25.176 * * [simplify]: iteration 2 : 7 enodes (cost 4 ) 25.177 * * [simplify]: iteration done : 7 enodes (cost 4 ) 25.177 * * [simplify]: iteration 0 : 13 enodes (cost 15 ) 25.179 * * [simplify]: iteration 1 : 32 enodes (cost 15 ) 25.183 * * [simplify]: iteration 2 : 66 enodes (cost 15 ) 25.194 * * [simplify]: iteration 3 : 114 enodes (cost 15 ) 25.214 * * [simplify]: iteration 4 : 209 enodes (cost 15 ) 25.278 * * [simplify]: iteration 5 : 504 enodes (cost 15 ) 25.690 * * [simplify]: iteration 6 : 1563 enodes (cost 15 ) 27.302 * * [simplify]: iteration done : 5000 enodes (cost 15 ) 27.302 * * [simplify]: iteration 0 : 6 enodes (cost 7 ) 27.303 * * [simplify]: iteration 1 : 11 enodes (cost 7 ) 27.304 * * [simplify]: iteration 2 : 14 enodes (cost 7 ) 27.306 * * [simplify]: iteration 3 : 16 enodes (cost 7 ) 27.307 * * [simplify]: iteration done : 16 enodes (cost 7 ) 27.308 * * [simplify]: iteration 0 : 6 enodes (cost 7 ) 27.308 * * [simplify]: iteration 1 : 11 enodes (cost 7 ) 27.310 * * [simplify]: iteration 2 : 14 enodes (cost 7 ) 27.311 * * [simplify]: iteration 3 : 16 enodes (cost 7 ) 27.313 * * [simplify]: iteration done : 16 enodes (cost 7 ) 27.313 * * [simplify]: iteration 0 : 11 enodes (cost 13 ) 27.315 * * [simplify]: iteration 1 : 30 enodes (cost 13 ) 27.324 * * [simplify]: iteration 2 : 72 enodes (cost 13 ) 27.336 * * [simplify]: iteration 3 : 158 enodes (cost 13 ) 27.385 * * [simplify]: iteration 4 : 345 enodes (cost 13 ) 27.537 * * [simplify]: iteration 5 : 852 enodes (cost 13 ) 28.552 * * [simplify]: iteration 6 : 2834 enodes (cost 13 ) 30.507 * * [simplify]: iteration done : 5001 enodes (cost 13 ) 30.507 * * [simplify]: iteration 0 : 2 enodes (cost 2 ) 30.508 * * [simplify]: iteration done : 2 enodes (cost 2 ) 30.508 * * [simplify]: iteration 0 : 2 enodes (cost 2 ) 30.508 * * [simplify]: iteration done : 2 enodes (cost 2 ) 30.509 * [simplify]: Simplified to: (exp (- 1.0 (cos x))) (log (- 1.0 (cos x))) (exp (- 1.0 (cos x))) (* (cbrt (- 1.0 (cos x))) (cbrt (- 1.0 (cos x)))) (cbrt (- 1.0 (cos x))) (pow (- 1.0 (cos x)) 3) (sqrt (- 1.0 (cos x))) (sqrt (- 1.0 (cos x))) (- (pow 1.0 3) (pow (cos x) 3)) (+ (* 1.0 1.0) (* (cos x) (+ (cos x) 1.0))) (neg (cos x)) (- (* 1.0 1.0) (* (cos x) (cos x))) (+ 1.0 (cos x)) (+ (sqrt 1.0) (sqrt (cos x))) (- (sqrt 1.0) (sqrt (cos x))) (- 1.0 (cos x)) (neg (cos x)) (- (log (- 1.0 (cos x))) (log (sin x))) (log (/ (- 1.0 (cos x)) (sin x))) (exp (/ (- 1.0 (cos x)) (sin x))) (pow (/ (- 1.0 (cos x)) (sin x)) 3) (* (cbrt (/ (- 1.0 (cos x)) (sin x))) (cbrt (/ (- 1.0 (cos x)) (sin x)))) (cbrt (/ (- 1.0 (cos x)) (sin x))) (pow (/ (- 1.0 (cos x)) (sin x)) 3) (sqrt (/ (- 1.0 (cos x)) (sin x))) (sqrt (/ (- 1.0 (cos x)) (sin x))) (- (cos x) 1.0) (neg (sin x)) (/ 1.0 (sin x)) (/ (cos x) (sin x)) (/ (* (cbrt (- 1.0 (cos x))) (cbrt (- 1.0 (cos x)))) (* (cbrt (sin x)) (cbrt (sin x)))) (/ (cbrt (- 1.0 (cos x))) (cbrt (sin x))) (/ (* (cbrt (- 1.0 (cos x))) (cbrt (- 1.0 (cos x)))) (sqrt (sin x))) (/ (cbrt (- 1.0 (cos x))) (sqrt (sin x))) (* (cbrt (- 1.0 (cos x))) (cbrt (- 1.0 (cos x)))) (/ (cbrt (- 1.0 (cos x))) (sin x)) (/ (sqrt (- 1.0 (cos x))) (* (cbrt (sin x)) (cbrt (sin x)))) (/ (sqrt (- 1.0 (cos x))) (cbrt (sin x))) (/ (sqrt (- 1.0 (cos x))) (sqrt (sin x))) (/ (sqrt (- 1.0 (cos x))) (sqrt (sin x))) (sqrt (- 1.0 (cos x))) (/ (sqrt (- 1.0 (cos x))) (sin x)) (/ 1 (* (cbrt (sin x)) (cbrt (sin x)))) (/ (- 1.0 (cos x)) (cbrt (sin x))) (/ 1 (sqrt (sin x))) (/ (- 1.0 (cos x)) (sqrt (sin x))) 1 (/ (- 1.0 (cos x)) (sin x)) (/ (+ (sqrt 1.0) (sqrt (cos x))) (* (cbrt (sin x)) (cbrt (sin x)))) (/ (- (sqrt 1.0) (sqrt (cos x))) (cbrt (sin x))) (/ (+ (sqrt 1.0) (sqrt (cos x))) (sqrt (sin x))) (/ (- (sqrt 1.0) (sqrt (cos x))) (sqrt (sin x))) (+ (sqrt 1.0) (sqrt (cos x))) (/ (- (sqrt 1.0) (sqrt (cos x))) (sin x)) (/ 1 (* (cbrt (sin x)) (cbrt (sin x)))) (/ (- 1.0 (cos x)) (cbrt (sin x))) (/ 1 (sqrt (sin x))) (/ (- 1.0 (cos x)) (sqrt (sin x))) 1 (/ (- 1.0 (cos x)) (sin x)) (/ 1 (sin x)) (/ (sin x) (- 1.0 (cos x))) (/ (- 1.0 (cos x)) (* (cbrt (sin x)) (cbrt (sin x)))) (/ (- 1.0 (cos x)) (sqrt (sin x))) (- 1.0 (cos x)) (/ (sin x) (cbrt (- 1.0 (cos x)))) (/ (sin x) (sqrt (- 1.0 (cos x)))) (/ (sin x) (- 1.0 (cos x))) (/ (sin x) (- (sqrt 1.0) (sqrt (cos x)))) (/ (sin x) (- 1.0 (cos x))) (* (+ (* 1.0 1.0) (* (cos x) (+ (cos x) 1.0))) (sin x)) (* (sin x) (+ 1.0 (cos x))) (log (sin x)) (exp (sin x)) (* (cbrt (sin x)) (cbrt (sin x))) (cbrt (sin x)) (pow (sin x) 3) (sqrt (sin x)) (sqrt (sin x)) (- (+ (* 1/2 (pow x 2)) (* 1/720 (pow x 6))) (* 1/24 (pow x 4))) (- 1.0 (cos x)) (- 1.0 (cos x)) (+ (* 1/2 x) (+ (* 1/24 (pow x 3)) (* 1/240 (pow x 5)))) (/ (- 1.0 (cos x)) (sin x)) (/ (- 1.0 (cos x)) (sin x)) (- (+ x (* 1/120 (pow x 5))) (* 1/6 (pow x 3))) (sin x) (sin x) 30.509 * * * [progress]: adding candidates to table 30.620 * * [progress]: iteration 2 / 4 30.620 * * * [progress]: picking best candidate 30.660 * * * * [pick]: Picked # 30.660 * * * [progress]: localizing error 30.671 * * * [progress]: generating rewritten candidates 30.671 * * * * [progress]: [ 1 / 2 ] rewriting at (2 2 1) 30.678 * * * * [progress]: [ 2 / 2 ] rewriting at (2 2 2) 30.686 * * * [progress]: generating series expansions 30.686 * * * * [progress]: [ 1 / 2 ] generating series at (2 2 1) 30.686 * [approximate]: Taking taylor expansion of (* 1/24 (pow x 3)) in (x) around 0 30.686 * [taylor]: Taking taylor expansion of (* 1/24 (pow x 3)) in x 30.686 * [taylor]: Taking taylor expansion of 1/24 in x 30.686 * [taylor]: Taking taylor expansion of (pow x 3) in x 30.686 * [taylor]: Taking taylor expansion of x in x 30.686 * [taylor]: Taking taylor expansion of (* 1/24 (pow x 3)) in x 30.686 * [taylor]: Taking taylor expansion of 1/24 in x 30.686 * [taylor]: Taking taylor expansion of (pow x 3) in x 30.686 * [taylor]: Taking taylor expansion of x in x 30.688 * [approximate]: Taking taylor expansion of (/ 1/24 (pow x 3)) in (x) around 0 30.688 * [taylor]: Taking taylor expansion of (/ 1/24 (pow x 3)) in x 30.688 * [taylor]: Taking taylor expansion of 1/24 in x 30.688 * [taylor]: Taking taylor expansion of (pow x 3) in x 30.688 * [taylor]: Taking taylor expansion of x in x 30.691 * [taylor]: Taking taylor expansion of (/ 1/24 (pow x 3)) in x 30.691 * [taylor]: Taking taylor expansion of 1/24 in x 30.691 * [taylor]: Taking taylor expansion of (pow x 3) in x 30.691 * [taylor]: Taking taylor expansion of x in x 30.692 * [approximate]: Taking taylor expansion of (/ -1/24 (pow x 3)) in (x) around 0 30.692 * [taylor]: Taking taylor expansion of (/ -1/24 (pow x 3)) in x 30.692 * [taylor]: Taking taylor expansion of -1/24 in x 30.692 * [taylor]: Taking taylor expansion of (pow x 3) in x 30.692 * [taylor]: Taking taylor expansion of x in x 30.692 * [taylor]: Taking taylor expansion of (/ -1/24 (pow x 3)) in x 30.692 * [taylor]: Taking taylor expansion of -1/24 in x 30.692 * [taylor]: Taking taylor expansion of (pow x 3) in x 30.692 * [taylor]: Taking taylor expansion of x in x 30.693 * * * * [progress]: [ 2 / 2 ] generating series at (2 2 2) 30.694 * [approximate]: Taking taylor expansion of (* 1/240 (pow x 5)) in (x) around 0 30.694 * [taylor]: Taking taylor expansion of (* 1/240 (pow x 5)) in x 30.694 * [taylor]: Taking taylor expansion of 1/240 in x 30.694 * [taylor]: Taking taylor expansion of (pow x 5) in x 30.694 * [taylor]: Taking taylor expansion of x in x 30.694 * [taylor]: Taking taylor expansion of (* 1/240 (pow x 5)) in x 30.694 * [taylor]: Taking taylor expansion of 1/240 in x 30.694 * [taylor]: Taking taylor expansion of (pow x 5) in x 30.694 * [taylor]: Taking taylor expansion of x in x 30.695 * [approximate]: Taking taylor expansion of (/ 1/240 (pow x 5)) in (x) around 0 30.695 * [taylor]: Taking taylor expansion of (/ 1/240 (pow x 5)) in x 30.695 * [taylor]: Taking taylor expansion of 1/240 in x 30.695 * [taylor]: Taking taylor expansion of (pow x 5) in x 30.695 * [taylor]: Taking taylor expansion of x in x 30.695 * [taylor]: Taking taylor expansion of (/ 1/240 (pow x 5)) in x 30.695 * [taylor]: Taking taylor expansion of 1/240 in x 30.695 * [taylor]: Taking taylor expansion of (pow x 5) in x 30.695 * [taylor]: Taking taylor expansion of x in x 30.697 * [approximate]: Taking taylor expansion of (/ -1/240 (pow x 5)) in (x) around 0 30.697 * [taylor]: Taking taylor expansion of (/ -1/240 (pow x 5)) in x 30.697 * [taylor]: Taking taylor expansion of -1/240 in x 30.697 * [taylor]: Taking taylor expansion of (pow x 5) in x 30.697 * [taylor]: Taking taylor expansion of x in x 30.697 * [taylor]: Taking taylor expansion of (/ -1/240 (pow x 5)) in x 30.697 * [taylor]: Taking taylor expansion of -1/240 in x 30.697 * [taylor]: Taking taylor expansion of (pow x 5) in x 30.697 * [taylor]: Taking taylor expansion of x in x 30.699 * * * [progress]: simplifying candidates 30.699 * [simplify]: Simplifying using # : (+ (log 1/24) (* (log x) 3)) (+ (log 1/24) (* (log x) 3)) (+ (log 1/24) (log (pow x 3))) (log (* 1/24 (pow x 3))) (exp (* 1/24 (pow x 3))) (* (* (* 1/24 1/24) 1/24) (* (* (pow x 3) (pow x 3)) (pow x 3))) (* (cbrt (* 1/24 (pow x 3))) (cbrt (* 1/24 (pow x 3)))) (cbrt (* 1/24 (pow x 3))) (* (* (* 1/24 (pow x 3)) (* 1/24 (pow x 3))) (* 1/24 (pow x 3))) (sqrt (* 1/24 (pow x 3))) (sqrt (* 1/24 (pow x 3))) (* (sqrt 1/24) (pow (sqrt x) 3)) (* (sqrt 1/24) (pow (sqrt x) 3)) (* (sqrt 1/24) (pow (sqrt x) 3)) (* (sqrt 1/24) (pow (sqrt x) 3)) (* (sqrt 1/24) (sqrt (pow x 3))) (* (sqrt 1/24) (sqrt (pow x 3))) (* (sqrt 1/24) (pow x (/ 3 2))) (* (sqrt 1/24) (pow x (/ 3 2))) (* 1/24 (pow (* (cbrt x) (cbrt x)) 3)) (* 1/24 (pow (sqrt x) 3)) (* 1/24 (pow 1 3)) (* 1/24 (* x x)) (* 1/24 (* (cbrt (pow x 3)) (cbrt (pow x 3)))) (* 1/24 (pow (* (cbrt x) (cbrt x)) 3)) (* 1/24 (pow (sqrt x) 3)) (* 1/24 (pow 1 3)) (* 1/24 x) (* 1/24 (sqrt (pow x 3))) (* 1/24 1) (* 1/24 (pow x (/ 3 2))) (* (cbrt 1/24) (pow x 3)) (* (sqrt 1/24) (pow x 3)) (* 1/24 (pow x 3)) (+ (log 1/240) (* (log x) 5)) (+ (log 1/240) (* (log x) 5)) (+ (log 1/240) (log (pow x 5))) (log (* 1/240 (pow x 5))) (exp (* 1/240 (pow x 5))) (* (* (* 1/240 1/240) 1/240) (* (* (pow x 5) (pow x 5)) (pow x 5))) (* (cbrt (* 1/240 (pow x 5))) (cbrt (* 1/240 (pow x 5)))) (cbrt (* 1/240 (pow x 5))) (* (* (* 1/240 (pow x 5)) (* 1/240 (pow x 5))) (* 1/240 (pow x 5))) (sqrt (* 1/240 (pow x 5))) (sqrt (* 1/240 (pow x 5))) (* (sqrt 1/240) (pow (sqrt x) 5)) (* (sqrt 1/240) (pow (sqrt x) 5)) (* (sqrt 1/240) (sqrt (pow x 5))) (* (sqrt 1/240) (sqrt (pow x 5))) (* (sqrt 1/240) (pow x (/ 5 2))) (* (sqrt 1/240) (pow x (/ 5 2))) (* 1/240 (pow (* (cbrt x) (cbrt x)) 5)) (* 1/240 (pow (sqrt x) 5)) (* 1/240 (pow 1 5)) (* 1/240 (* (cbrt (pow x 5)) (cbrt (pow x 5)))) (* 1/240 (sqrt (pow x 5))) (* 1/240 1) (* 1/240 (pow x (/ 5 2))) (* (cbrt 1/240) (pow x 5)) (* (sqrt 1/240) (pow x 5)) (* 1/240 (pow x 5)) (* 1/24 (pow x 3)) (* 1/24 (pow x 3)) (* 1/24 (pow x 3)) (* 1/240 (pow x 5)) (* 1/240 (pow x 5)) (* 1/240 (pow x 5)) 30.700 * * [simplify]: iteration 0 : 7 enodes (cost 7 ) 30.701 * * [simplify]: iteration 1 : 9 enodes (cost 7 ) 30.702 * * [simplify]: iteration done : 9 enodes (cost 7 ) 30.703 * * [simplify]: iteration 0 : 7 enodes (cost 7 ) 30.703 * * [simplify]: iteration 1 : 9 enodes (cost 7 ) 30.704 * * [simplify]: iteration done : 9 enodes (cost 7 ) 30.705 * * [simplify]: iteration 0 : 7 enodes (cost 7 ) 30.706 * * [simplify]: iteration 1 : 18 enodes (cost 7 ) 30.708 * * [simplify]: iteration 2 : 30 enodes (cost 7 ) 30.711 * * [simplify]: iteration 3 : 57 enodes (cost 7 ) 30.720 * * [simplify]: iteration 4 : 111 enodes (cost 7 ) 30.745 * * [simplify]: iteration 5 : 257 enodes (cost 7 ) 30.871 * * [simplify]: iteration 6 : 736 enodes (cost 7 ) 31.859 * * [simplify]: iteration 7 : 2804 enodes (cost 7 ) 33.491 * * [simplify]: iteration done : 5000 enodes (cost 7 ) 33.492 * * [simplify]: iteration 0 : 6 enodes (cost 6 ) 33.492 * * [simplify]: iteration 1 : 18 enodes (cost 6 ) 33.495 * * [simplify]: iteration 2 : 44 enodes (cost 6 ) 33.501 * * [simplify]: iteration 3 : 92 enodes (cost 6 ) 33.523 * * [simplify]: iteration 4 : 181 enodes (cost 6 ) 33.576 * * [simplify]: iteration 5 : 434 enodes (cost 6 ) 33.867 * * [simplify]: iteration 6 : 1321 enodes (cost 6 ) 36.602 * * [simplify]: iteration done : 5001 enodes (cost 6 ) 36.603 * * [simplify]: iteration 0 : 6 enodes (cost 6 ) 36.604 * * [simplify]: iteration 1 : 17 enodes (cost 6 ) 36.606 * * [simplify]: iteration 2 : 40 enodes (cost 6 ) 36.613 * * [simplify]: iteration 3 : 93 enodes (cost 6 ) 36.630 * * [simplify]: iteration 4 : 231 enodes (cost 6 ) 36.696 * * [simplify]: iteration 5 : 697 enodes (cost 6 ) 37.362 * * [simplify]: iteration 6 : 2747 enodes (cost 6 ) 38.496 * * [simplify]: iteration done : 5000 enodes (cost 6 ) 38.496 * * [simplify]: iteration 0 : 9 enodes (cost 17 ) 38.498 * * [simplify]: iteration 1 : 29 enodes (cost 9 ) 38.502 * * [simplify]: iteration 2 : 87 enodes (cost 7 ) 38.537 * * [simplify]: iteration 3 : 358 enodes (cost 7 ) 38.939 * * [simplify]: iteration 4 : 1597 enodes (cost 7 ) 40.984 * * [simplify]: iteration done : 5000 enodes (cost 7 ) 40.984 * * [simplify]: iteration 0 : 7 enodes (cost 13 ) 40.985 * * [simplify]: iteration 1 : 16 enodes (cost 13 ) 40.987 * * [simplify]: iteration 2 : 34 enodes (cost 13 ) 40.992 * * [simplify]: iteration 3 : 58 enodes (cost 13 ) 41.001 * * [simplify]: iteration 4 : 102 enodes (cost 13 ) 41.033 * * [simplify]: iteration 5 : 244 enodes (cost 13 ) 41.228 * * [simplify]: iteration 6 : 769 enodes (cost 13 ) 43.285 * * [simplify]: iteration 7 : 3060 enodes (cost 13 ) 46.085 * * [simplify]: iteration done : 5001 enodes (cost 13 ) 46.085 * * [simplify]: iteration 0 : 6 enodes (cost 6 ) 46.086 * * [simplify]: iteration 1 : 15 enodes (cost 6 ) 46.088 * * [simplify]: iteration 2 : 33 enodes (cost 6 ) 46.098 * * [simplify]: iteration 3 : 56 enodes (cost 6 ) 46.107 * * [simplify]: iteration 4 : 103 enodes (cost 6 ) 46.137 * * [simplify]: iteration 5 : 241 enodes (cost 6 ) 46.343 * * [simplify]: iteration 6 : 766 enodes (cost 6 ) 48.464 * * [simplify]: iteration 7 : 3067 enodes (cost 6 ) 51.895 * * [simplify]: iteration done : 5000 enodes (cost 6 ) 51.896 * * [simplify]: iteration 0 : 7 enodes (cost 17 ) 51.897 * * [simplify]: iteration 1 : 27 enodes (cost 15 ) 51.903 * * [simplify]: iteration 2 : 107 enodes (cost 7 ) 51.958 * * [simplify]: iteration 3 : 511 enodes (cost 7 ) 52.887 * * [simplify]: iteration 4 : 2469 enodes (cost 7 ) 55.047 * * [simplify]: iteration done : 5000 enodes (cost 7 ) 55.048 * * [simplify]: iteration 0 : 6 enodes (cost 6 ) 55.049 * * [simplify]: iteration 1 : 15 enodes (cost 6 ) 55.051 * * [simplify]: iteration 2 : 33 enodes (cost 6 ) 55.056 * * [simplify]: iteration 3 : 56 enodes (cost 6 ) 55.065 * * [simplify]: iteration 4 : 103 enodes (cost 6 ) 55.096 * * [simplify]: iteration 5 : 241 enodes (cost 6 ) 55.294 * * [simplify]: iteration 6 : 766 enodes (cost 6 ) 57.378 * * [simplify]: iteration 7 : 3067 enodes (cost 6 ) 60.797 * * [simplify]: iteration done : 5000 enodes (cost 6 ) 60.797 * * [simplify]: iteration 0 : 6 enodes (cost 6 ) 60.798 * * [simplify]: iteration 1 : 15 enodes (cost 6 ) 60.800 * * [simplify]: iteration 2 : 33 enodes (cost 6 ) 60.805 * * [simplify]: iteration 3 : 56 enodes (cost 6 ) 60.815 * * [simplify]: iteration 4 : 103 enodes (cost 6 ) 60.848 * * [simplify]: iteration 5 : 241 enodes (cost 6 ) 61.050 * * [simplify]: iteration 6 : 766 enodes (cost 6 ) 63.143 * * [simplify]: iteration 7 : 3067 enodes (cost 6 ) 66.547 * * [simplify]: iteration done : 5000 enodes (cost 6 ) 66.547 * * [simplify]: iteration 0 : 7 enodes (cost 7 ) 66.548 * * [simplify]: iteration 1 : 16 enodes (cost 7 ) 66.550 * * [simplify]: iteration 2 : 34 enodes (cost 7 ) 66.554 * * [simplify]: iteration 3 : 52 enodes (cost 7 ) 66.564 * * [simplify]: iteration 4 : 100 enodes (cost 7 ) 66.595 * * [simplify]: iteration 5 : 246 enodes (cost 7 ) 66.785 * * [simplify]: iteration 6 : 764 enodes (cost 7 ) 68.818 * * [simplify]: iteration 7 : 3053 enodes (cost 7 ) 73.131 * * [simplify]: iteration done : 5000 enodes (cost 7 ) 73.131 * * [simplify]: iteration 0 : 7 enodes (cost 7 ) 73.132 * * [simplify]: iteration 1 : 16 enodes (cost 7 ) 73.135 * * [simplify]: iteration 2 : 34 enodes (cost 7 ) 73.139 * * [simplify]: iteration 3 : 52 enodes (cost 7 ) 73.148 * * [simplify]: iteration 4 : 100 enodes (cost 7 ) 73.180 * * [simplify]: iteration 5 : 246 enodes (cost 7 ) 73.371 * * [simplify]: iteration 6 : 764 enodes (cost 7 ) 75.437 * * [simplify]: iteration 7 : 3053 enodes (cost 7 ) 79.558 * * [simplify]: iteration done : 5000 enodes (cost 7 ) 79.559 * * [simplify]: iteration 0 : 7 enodes (cost 7 ) 79.560 * * [simplify]: iteration 1 : 16 enodes (cost 7 ) 79.562 * * [simplify]: iteration 2 : 34 enodes (cost 7 ) 79.567 * * [simplify]: iteration 3 : 52 enodes (cost 7 ) 79.575 * * [simplify]: iteration 4 : 100 enodes (cost 7 ) 79.603 * * [simplify]: iteration 5 : 246 enodes (cost 7 ) 79.795 * * [simplify]: iteration 6 : 764 enodes (cost 7 ) 81.823 * * [simplify]: iteration 7 : 3053 enodes (cost 7 ) 85.866 * * [simplify]: iteration done : 5000 enodes (cost 7 ) 85.866 * * [simplify]: iteration 0 : 7 enodes (cost 7 ) 85.867 * * [simplify]: iteration 1 : 16 enodes (cost 7 ) 85.870 * * [simplify]: iteration 2 : 34 enodes (cost 7 ) 85.874 * * [simplify]: iteration 3 : 52 enodes (cost 7 ) 85.883 * * [simplify]: iteration 4 : 100 enodes (cost 7 ) 85.914 * * [simplify]: iteration 5 : 246 enodes (cost 7 ) 86.101 * * [simplify]: iteration 6 : 764 enodes (cost 7 ) 88.135 * * [simplify]: iteration 7 : 3053 enodes (cost 7 ) 92.174 * * [simplify]: iteration done : 5000 enodes (cost 7 ) 92.175 * * [simplify]: iteration 0 : 7 enodes (cost 7 ) 92.176 * * [simplify]: iteration 1 : 16 enodes (cost 7 ) 92.178 * * [simplify]: iteration 2 : 23 enodes (cost 7 ) 92.180 * * [simplify]: iteration 3 : 33 enodes (cost 7 ) 92.184 * * [simplify]: iteration 4 : 54 enodes (cost 7 ) 92.193 * * [simplify]: iteration 5 : 114 enodes (cost 7 ) 92.240 * * [simplify]: iteration 6 : 316 enodes (cost 7 ) 92.700 * * [simplify]: iteration 7 : 1251 enodes (cost 7 ) 95.018 * * [simplify]: iteration done : 5000 enodes (cost 7 ) 95.019 * * [simplify]: iteration 0 : 7 enodes (cost 7 ) 95.020 * * [simplify]: iteration 1 : 16 enodes (cost 7 ) 95.021 * * [simplify]: iteration 2 : 23 enodes (cost 7 ) 95.024 * * [simplify]: iteration 3 : 33 enodes (cost 7 ) 95.028 * * [simplify]: iteration 4 : 54 enodes (cost 7 ) 95.037 * * [simplify]: iteration 5 : 114 enodes (cost 7 ) 95.084 * * [simplify]: iteration 6 : 316 enodes (cost 7 ) 95.538 * * [simplify]: iteration 7 : 1251 enodes (cost 7 ) 97.842 * * [simplify]: iteration done : 5000 enodes (cost 7 ) 97.842 * * [simplify]: iteration 0 : 8 enodes (cost 8 ) 97.848 * * [simplify]: iteration 1 : 14 enodes (cost 6 ) 97.850 * * [simplify]: iteration 2 : 24 enodes (cost 6 ) 97.852 * * [simplify]: iteration 3 : 44 enodes (cost 6 ) 97.858 * * [simplify]: iteration 4 : 88 enodes (cost 6 ) 97.900 * * [simplify]: iteration 5 : 230 enodes (cost 6 ) 98.088 * * [simplify]: iteration 6 : 750 enodes (cost 6 ) 100.075 * * [simplify]: iteration 7 : 3051 enodes (cost 6 ) 103.986 * * [simplify]: iteration done : 5000 enodes (cost 6 ) 103.986 * * [simplify]: iteration 0 : 8 enodes (cost 8 ) 103.987 * * [simplify]: iteration 1 : 14 enodes (cost 6 ) 103.989 * * [simplify]: iteration 2 : 24 enodes (cost 6 ) 103.992 * * [simplify]: iteration 3 : 44 enodes (cost 6 ) 103.998 * * [simplify]: iteration 4 : 88 enodes (cost 6 ) 104.023 * * [simplify]: iteration 5 : 230 enodes (cost 6 ) 104.216 * * [simplify]: iteration 6 : 750 enodes (cost 6 ) 106.231 * * [simplify]: iteration 7 : 3051 enodes (cost 6 ) 109.928 * * [simplify]: iteration done : 5000 enodes (cost 6 ) 109.929 * * [simplify]: iteration 0 : 7 enodes (cost 9 ) 109.930 * * [simplify]: iteration 1 : 18 enodes (cost 9 ) 109.933 * * [simplify]: iteration 2 : 55 enodes (cost 5 ) 109.943 * * [simplify]: iteration 3 : 111 enodes (cost 5 ) 109.968 * * [simplify]: iteration 4 : 166 enodes (cost 5 ) 110.026 * * [simplify]: iteration 5 : 320 enodes (cost 5 ) 110.263 * * [simplify]: iteration 6 : 852 enodes (cost 5 ) 112.397 * * [simplify]: iteration 7 : 3190 enodes (cost 5 ) 115.683 * * [simplify]: iteration done : 5000 enodes (cost 5 ) 115.684 * * [simplify]: iteration 0 : 6 enodes (cost 6 ) 115.684 * * [simplify]: iteration 1 : 15 enodes (cost 6 ) 115.686 * * [simplify]: iteration 2 : 33 enodes (cost 6 ) 115.691 * * [simplify]: iteration 3 : 57 enodes (cost 6 ) 115.699 * * [simplify]: iteration 4 : 101 enodes (cost 6 ) 115.728 * * [simplify]: iteration 5 : 246 enodes (cost 6 ) 115.925 * * [simplify]: iteration 6 : 775 enodes (cost 6 ) 117.961 * * [simplify]: iteration 7 : 3072 enodes (cost 6 ) 120.914 * * [simplify]: iteration done : 5000 enodes (cost 6 ) 120.915 * * [simplify]: iteration 0 : 5 enodes (cost 5 ) 120.916 * * [simplify]: iteration 1 : 16 enodes (cost 1 ) 120.917 * * [simplify]: iteration 2 : 20 enodes (cost 1 ) 120.917 * * [simplify]: iteration done : 20 enodes (cost 1 ) 120.918 * * [simplify]: iteration 0 : 4 enodes (cost 5 ) 120.919 * * [simplify]: iteration 1 : 7 enodes (cost 5 ) 120.919 * * [simplify]: iteration 2 : 9 enodes (cost 5 ) 120.921 * * [simplify]: iteration done : 9 enodes (cost 5 ) 120.922 * * [simplify]: iteration 0 : 7 enodes (cost 11 ) 120.923 * * [simplify]: iteration 1 : 17 enodes (cost 5 ) 120.925 * * [simplify]: iteration 2 : 25 enodes (cost 5 ) 120.928 * * [simplify]: iteration 3 : 35 enodes (cost 5 ) 120.932 * * [simplify]: iteration 4 : 56 enodes (cost 5 ) 120.941 * * [simplify]: iteration 5 : 116 enodes (cost 5 ) 120.990 * * [simplify]: iteration 6 : 325 enodes (cost 5 ) 121.439 * * [simplify]: iteration 7 : 1246 enodes (cost 5 ) 123.873 * * [simplify]: iteration done : 5000 enodes (cost 5 ) 123.874 * * [simplify]: iteration 0 : 7 enodes (cost 9 ) 123.880 * * [simplify]: iteration 1 : 18 enodes (cost 9 ) 123.883 * * [simplify]: iteration 2 : 55 enodes (cost 5 ) 123.894 * * [simplify]: iteration 3 : 111 enodes (cost 5 ) 123.919 * * [simplify]: iteration 4 : 166 enodes (cost 5 ) 123.977 * * [simplify]: iteration 5 : 320 enodes (cost 5 ) 124.214 * * [simplify]: iteration 6 : 852 enodes (cost 5 ) 126.358 * * [simplify]: iteration 7 : 3190 enodes (cost 5 ) 129.889 * * [simplify]: iteration done : 5000 enodes (cost 5 ) 129.890 * * [simplify]: iteration 0 : 6 enodes (cost 6 ) 129.891 * * [simplify]: iteration 1 : 15 enodes (cost 6 ) 129.893 * * [simplify]: iteration 2 : 33 enodes (cost 6 ) 129.898 * * [simplify]: iteration 3 : 57 enodes (cost 6 ) 129.906 * * [simplify]: iteration 4 : 101 enodes (cost 6 ) 129.934 * * [simplify]: iteration 5 : 246 enodes (cost 6 ) 130.134 * * [simplify]: iteration 6 : 775 enodes (cost 6 ) 132.184 * * [simplify]: iteration 7 : 3072 enodes (cost 6 ) 135.094 * * [simplify]: iteration done : 5000 enodes (cost 6 ) 135.095 * * [simplify]: iteration 0 : 5 enodes (cost 5 ) 135.096 * * [simplify]: iteration 1 : 16 enodes (cost 1 ) 135.097 * * [simplify]: iteration 2 : 20 enodes (cost 1 ) 135.097 * * [simplify]: iteration done : 20 enodes (cost 1 ) 135.098 * * [simplify]: iteration 0 : 3 enodes (cost 3 ) 135.098 * * [simplify]: iteration 1 : 4 enodes (cost 3 ) 135.099 * * [simplify]: iteration done : 4 enodes (cost 3 ) 135.099 * * [simplify]: iteration 0 : 6 enodes (cost 6 ) 135.100 * * [simplify]: iteration 1 : 15 enodes (cost 6 ) 135.102 * * [simplify]: iteration 2 : 22 enodes (cost 6 ) 135.104 * * [simplify]: iteration 3 : 32 enodes (cost 6 ) 135.108 * * [simplify]: iteration 4 : 53 enodes (cost 6 ) 135.118 * * [simplify]: iteration 5 : 114 enodes (cost 6 ) 135.167 * * [simplify]: iteration 6 : 324 enodes (cost 6 ) 135.627 * * [simplify]: iteration 7 : 1259 enodes (cost 6 ) 137.971 * * [simplify]: iteration done : 5000 enodes (cost 6 ) 137.971 * * [simplify]: iteration 0 : 3 enodes (cost 3 ) 137.972 * * [simplify]: iteration 1 : 6 enodes (cost 1 ) 137.972 * * [simplify]: iteration done : 6 enodes (cost 1 ) 137.973 * * [simplify]: iteration 0 : 7 enodes (cost 7 ) 137.973 * * [simplify]: iteration 1 : 13 enodes (cost 5 ) 137.975 * * [simplify]: iteration 2 : 23 enodes (cost 5 ) 137.977 * * [simplify]: iteration 3 : 41 enodes (cost 5 ) 137.983 * * [simplify]: iteration 4 : 87 enodes (cost 5 ) 138.013 * * [simplify]: iteration 5 : 227 enodes (cost 5 ) 138.205 * * [simplify]: iteration 6 : 762 enodes (cost 5 ) 140.259 * * [simplify]: iteration 7 : 3059 enodes (cost 5 ) 142.724 * * [simplify]: iteration done : 5001 enodes (cost 5 ) 142.725 * * [simplify]: iteration 0 : 6 enodes (cost 6 ) 142.726 * * [simplify]: iteration 1 : 15 enodes (cost 6 ) 142.727 * * [simplify]: iteration 2 : 33 enodes (cost 6 ) 142.732 * * [simplify]: iteration 3 : 61 enodes (cost 6 ) 142.742 * * [simplify]: iteration 4 : 107 enodes (cost 6 ) 142.777 * * [simplify]: iteration 5 : 252 enodes (cost 6 ) 142.977 * * [simplify]: iteration 6 : 785 enodes (cost 6 ) 145.083 * * [simplify]: iteration 7 : 3076 enodes (cost 6 ) 147.615 * * [simplify]: iteration done : 5001 enodes (cost 6 ) 147.615 * * [simplify]: iteration 0 : 6 enodes (cost 6 ) 147.616 * * [simplify]: iteration 1 : 15 enodes (cost 6 ) 147.618 * * [simplify]: iteration 2 : 33 enodes (cost 6 ) 147.623 * * [simplify]: iteration 3 : 61 enodes (cost 6 ) 147.632 * * [simplify]: iteration 4 : 107 enodes (cost 6 ) 147.667 * * [simplify]: iteration 5 : 252 enodes (cost 6 ) 147.861 * * [simplify]: iteration 6 : 785 enodes (cost 6 ) 149.943 * * [simplify]: iteration 7 : 3076 enodes (cost 6 ) 152.471 * * [simplify]: iteration done : 5001 enodes (cost 6 ) 152.471 * * [simplify]: iteration 0 : 5 enodes (cost 5 ) 152.472 * * [simplify]: iteration 1 : 14 enodes (cost 5 ) 152.474 * * [simplify]: iteration 2 : 32 enodes (cost 5 ) 152.484 * * [simplify]: iteration 3 : 54 enodes (cost 5 ) 152.494 * * [simplify]: iteration 4 : 101 enodes (cost 5 ) 152.523 * * [simplify]: iteration 5 : 244 enodes (cost 5 ) 152.714 * * [simplify]: iteration 6 : 773 enodes (cost 5 ) 155.020 * * [simplify]: iteration 7 : 3060 enodes (cost 5 ) 158.308 * * [simplify]: iteration done : 5001 enodes (cost 5 ) 158.309 * * [simplify]: iteration 0 : 7 enodes (cost 7 ) 158.310 * * [simplify]: iteration 1 : 9 enodes (cost 7 ) 158.310 * * [simplify]: iteration done : 9 enodes (cost 7 ) 158.311 * * [simplify]: iteration 0 : 7 enodes (cost 7 ) 158.312 * * [simplify]: iteration 1 : 9 enodes (cost 7 ) 158.313 * * [simplify]: iteration done : 9 enodes (cost 7 ) 158.313 * * [simplify]: iteration 0 : 7 enodes (cost 7 ) 158.314 * * [simplify]: iteration 1 : 15 enodes (cost 7 ) 158.316 * * [simplify]: iteration 2 : 24 enodes (cost 7 ) 158.318 * * [simplify]: iteration 3 : 42 enodes (cost 7 ) 158.324 * * [simplify]: iteration 4 : 91 enodes (cost 7 ) 158.345 * * [simplify]: iteration 5 : 241 enodes (cost 7 ) 158.469 * * [simplify]: iteration 6 : 737 enodes (cost 7 ) 159.438 * * [simplify]: iteration 7 : 2752 enodes (cost 7 ) 161.190 * * [simplify]: iteration done : 5000 enodes (cost 7 ) 161.191 * * [simplify]: iteration 0 : 6 enodes (cost 6 ) 161.191 * * [simplify]: iteration 1 : 15 enodes (cost 6 ) 161.193 * * [simplify]: iteration 2 : 30 enodes (cost 6 ) 161.202 * * [simplify]: iteration 3 : 60 enodes (cost 6 ) 161.213 * * [simplify]: iteration 4 : 144 enodes (cost 6 ) 161.259 * * [simplify]: iteration 5 : 405 enodes (cost 6 ) 161.553 * * [simplify]: iteration 6 : 1301 enodes (cost 6 ) 164.376 * * [simplify]: iteration 7 : 4933 enodes (cost 6 ) 166.077 * * [simplify]: iteration done : 5000 enodes (cost 6 ) 166.077 * * [simplify]: iteration 0 : 6 enodes (cost 6 ) 166.078 * * [simplify]: iteration 1 : 14 enodes (cost 6 ) 166.080 * * [simplify]: iteration 2 : 29 enodes (cost 6 ) 166.083 * * [simplify]: iteration 3 : 63 enodes (cost 6 ) 166.094 * * [simplify]: iteration 4 : 165 enodes (cost 6 ) 166.141 * * [simplify]: iteration 5 : 543 enodes (cost 6 ) 166.660 * * [simplify]: iteration 6 : 2400 enodes (cost 6 ) 167.766 * * [simplify]: iteration done : 5001 enodes (cost 6 ) 167.767 * * [simplify]: iteration 0 : 9 enodes (cost 17 ) 167.769 * * [simplify]: iteration 1 : 26 enodes (cost 9 ) 167.772 * * [simplify]: iteration 2 : 62 enodes (cost 7 ) 167.791 * * [simplify]: iteration 3 : 173 enodes (cost 7 ) 167.894 * * [simplify]: iteration 4 : 656 enodes (cost 7 ) 169.171 * * [simplify]: iteration 5 : 2869 enodes (cost 7 ) 171.517 * * [simplify]: iteration done : 5000 enodes (cost 7 ) 171.518 * * [simplify]: iteration 0 : 7 enodes (cost 13 ) 171.519 * * [simplify]: iteration 1 : 13 enodes (cost 13 ) 171.520 * * [simplify]: iteration 2 : 23 enodes (cost 13 ) 171.523 * * [simplify]: iteration 3 : 41 enodes (cost 13 ) 171.529 * * [simplify]: iteration 4 : 89 enodes (cost 13 ) 171.558 * * [simplify]: iteration 5 : 228 enodes (cost 13 ) 171.757 * * [simplify]: iteration 6 : 758 enodes (cost 13 ) 173.862 * * [simplify]: iteration 7 : 3065 enodes (cost 13 ) 178.265 * * [simplify]: iteration done : 5001 enodes (cost 13 ) 178.265 * * [simplify]: iteration 0 : 6 enodes (cost 6 ) 178.266 * * [simplify]: iteration 1 : 12 enodes (cost 6 ) 178.267 * * [simplify]: iteration 2 : 22 enodes (cost 6 ) 178.270 * * [simplify]: iteration 3 : 40 enodes (cost 6 ) 178.276 * * [simplify]: iteration 4 : 85 enodes (cost 6 ) 178.305 * * [simplify]: iteration 5 : 232 enodes (cost 6 ) 178.500 * * [simplify]: iteration 6 : 761 enodes (cost 6 ) 180.633 * * [simplify]: iteration 7 : 3051 enodes (cost 6 ) 183.551 * * [simplify]: iteration done : 5001 enodes (cost 6 ) 183.552 * * [simplify]: iteration 0 : 7 enodes (cost 17 ) 183.553 * * [simplify]: iteration 1 : 24 enodes (cost 15 ) 183.557 * * [simplify]: iteration 2 : 74 enodes (cost 7 ) 183.585 * * [simplify]: iteration 3 : 249 enodes (cost 7 ) 183.826 * * [simplify]: iteration 4 : 962 enodes (cost 7 ) 186.624 * * [simplify]: iteration 5 : 4036 enodes (cost 7 ) 189.568 * * [simplify]: iteration done : 5001 enodes (cost 7 ) 189.568 * * [simplify]: iteration 0 : 6 enodes (cost 6 ) 189.569 * * [simplify]: iteration 1 : 12 enodes (cost 6 ) 189.571 * * [simplify]: iteration 2 : 22 enodes (cost 6 ) 189.573 * * [simplify]: iteration 3 : 40 enodes (cost 6 ) 189.579 * * [simplify]: iteration 4 : 85 enodes (cost 6 ) 189.609 * * [simplify]: iteration 5 : 232 enodes (cost 6 ) 189.809 * * [simplify]: iteration 6 : 761 enodes (cost 6 ) 191.922 * * [simplify]: iteration 7 : 3051 enodes (cost 6 ) 194.811 * * [simplify]: iteration done : 5001 enodes (cost 6 ) 194.812 * * [simplify]: iteration 0 : 6 enodes (cost 6 ) 194.813 * * [simplify]: iteration 1 : 12 enodes (cost 6 ) 194.814 * * [simplify]: iteration 2 : 22 enodes (cost 6 ) 194.816 * * [simplify]: iteration 3 : 40 enodes (cost 6 ) 194.823 * * [simplify]: iteration 4 : 85 enodes (cost 6 ) 194.853 * * [simplify]: iteration 5 : 232 enodes (cost 6 ) 195.046 * * [simplify]: iteration 6 : 761 enodes (cost 6 ) 197.150 * * [simplify]: iteration 7 : 3051 enodes (cost 6 ) 200.043 * * [simplify]: iteration done : 5001 enodes (cost 6 ) 200.044 * * [simplify]: iteration 0 : 7 enodes (cost 7 ) 200.045 * * [simplify]: iteration 1 : 13 enodes (cost 7 ) 200.046 * * [simplify]: iteration 2 : 23 enodes (cost 7 ) 200.048 * * [simplify]: iteration 3 : 41 enodes (cost 7 ) 200.055 * * [simplify]: iteration 4 : 88 enodes (cost 7 ) 200.085 * * [simplify]: iteration 5 : 233 enodes (cost 7 ) 200.278 * * [simplify]: iteration 6 : 762 enodes (cost 7 ) 202.510 * * [simplify]: iteration 7 : 3059 enodes (cost 7 ) 206.259 * * [simplify]: iteration done : 5000 enodes (cost 7 ) 206.260 * * [simplify]: iteration 0 : 7 enodes (cost 7 ) 206.261 * * [simplify]: iteration 1 : 13 enodes (cost 7 ) 206.262 * * [simplify]: iteration 2 : 23 enodes (cost 7 ) 206.265 * * [simplify]: iteration 3 : 41 enodes (cost 7 ) 206.277 * * [simplify]: iteration 4 : 88 enodes (cost 7 ) 206.302 * * [simplify]: iteration 5 : 233 enodes (cost 7 ) 206.501 * * [simplify]: iteration 6 : 762 enodes (cost 7 ) 208.515 * * [simplify]: iteration 7 : 3059 enodes (cost 7 ) 212.186 * * [simplify]: iteration done : 5000 enodes (cost 7 ) 212.187 * * [simplify]: iteration 0 : 7 enodes (cost 7 ) 212.188 * * [simplify]: iteration 1 : 13 enodes (cost 7 ) 212.189 * * [simplify]: iteration 2 : 20 enodes (cost 7 ) 212.191 * * [simplify]: iteration 3 : 30 enodes (cost 7 ) 212.194 * * [simplify]: iteration 4 : 52 enodes (cost 7 ) 212.203 * * [simplify]: iteration 5 : 116 enodes (cost 7 ) 212.251 * * [simplify]: iteration 6 : 331 enodes (cost 7 ) 212.699 * * [simplify]: iteration 7 : 1268 enodes (cost 7 ) 214.997 * * [simplify]: iteration done : 5001 enodes (cost 7 ) 214.998 * * [simplify]: iteration 0 : 7 enodes (cost 7 ) 215.000 * * [simplify]: iteration 1 : 13 enodes (cost 7 ) 215.001 * * [simplify]: iteration 2 : 20 enodes (cost 7 ) 215.003 * * [simplify]: iteration 3 : 30 enodes (cost 7 ) 215.006 * * [simplify]: iteration 4 : 52 enodes (cost 7 ) 215.019 * * [simplify]: iteration 5 : 116 enodes (cost 7 ) 215.063 * * [simplify]: iteration 6 : 331 enodes (cost 7 ) 215.512 * * [simplify]: iteration 7 : 1268 enodes (cost 7 ) 217.818 * * [simplify]: iteration done : 5001 enodes (cost 7 ) 217.819 * * [simplify]: iteration 0 : 8 enodes (cost 8 ) 217.825 * * [simplify]: iteration 1 : 14 enodes (cost 6 ) 217.827 * * [simplify]: iteration 2 : 24 enodes (cost 6 ) 217.830 * * [simplify]: iteration 3 : 44 enodes (cost 6 ) 217.836 * * [simplify]: iteration 4 : 89 enodes (cost 6 ) 217.861 * * [simplify]: iteration 5 : 233 enodes (cost 6 ) 218.048 * * [simplify]: iteration 6 : 758 enodes (cost 6 ) 219.988 * * [simplify]: iteration 7 : 3055 enodes (cost 6 ) 223.282 * * [simplify]: iteration done : 5001 enodes (cost 6 ) 223.282 * * [simplify]: iteration 0 : 8 enodes (cost 8 ) 223.283 * * [simplify]: iteration 1 : 14 enodes (cost 6 ) 223.289 * * [simplify]: iteration 2 : 24 enodes (cost 6 ) 223.291 * * [simplify]: iteration 3 : 44 enodes (cost 6 ) 223.298 * * [simplify]: iteration 4 : 89 enodes (cost 6 ) 223.323 * * [simplify]: iteration 5 : 233 enodes (cost 6 ) 223.511 * * [simplify]: iteration 6 : 758 enodes (cost 6 ) 225.447 * * [simplify]: iteration 7 : 3055 enodes (cost 6 ) 228.754 * * [simplify]: iteration done : 5001 enodes (cost 6 ) 228.755 * * [simplify]: iteration 0 : 7 enodes (cost 9 ) 228.755 * * [simplify]: iteration 1 : 13 enodes (cost 9 ) 228.757 * * [simplify]: iteration 2 : 23 enodes (cost 9 ) 228.759 * * [simplify]: iteration 3 : 41 enodes (cost 9 ) 228.770 * * [simplify]: iteration 4 : 88 enodes (cost 9 ) 228.794 * * [simplify]: iteration 5 : 233 enodes (cost 9 ) 229.002 * * [simplify]: iteration 6 : 764 enodes (cost 9 ) 231.260 * * [simplify]: iteration 7 : 3068 enodes (cost 9 ) 235.056 * * [simplify]: iteration done : 5001 enodes (cost 9 ) 235.056 * * [simplify]: iteration 0 : 6 enodes (cost 6 ) 235.057 * * [simplify]: iteration 1 : 12 enodes (cost 6 ) 235.058 * * [simplify]: iteration 2 : 22 enodes (cost 6 ) 235.061 * * [simplify]: iteration 3 : 42 enodes (cost 6 ) 235.067 * * [simplify]: iteration 4 : 88 enodes (cost 6 ) 235.092 * * [simplify]: iteration 5 : 238 enodes (cost 6 ) 235.285 * * [simplify]: iteration 6 : 769 enodes (cost 6 ) 237.299 * * [simplify]: iteration 7 : 3058 enodes (cost 6 ) 240.566 * * [simplify]: iteration done : 5001 enodes (cost 6 ) 240.566 * * [simplify]: iteration 0 : 5 enodes (cost 5 ) 240.567 * * [simplify]: iteration 1 : 13 enodes (cost 1 ) 240.568 * * [simplify]: iteration done : 13 enodes (cost 1 ) 240.568 * * [simplify]: iteration 0 : 7 enodes (cost 11 ) 240.569 * * [simplify]: iteration 1 : 15 enodes (cost 11 ) 240.576 * * [simplify]: iteration 2 : 23 enodes (cost 11 ) 240.579 * * [simplify]: iteration 3 : 33 enodes (cost 11 ) 240.583 * * [simplify]: iteration 4 : 55 enodes (cost 11 ) 240.592 * * [simplify]: iteration 5 : 117 enodes (cost 11 ) 240.640 * * [simplify]: iteration 6 : 326 enodes (cost 11 ) 241.096 * * [simplify]: iteration 7 : 1255 enodes (cost 11 ) 243.417 * * [simplify]: iteration done : 5001 enodes (cost 11 ) 243.418 * * [simplify]: iteration 0 : 6 enodes (cost 6 ) 243.419 * * [simplify]: iteration 1 : 12 enodes (cost 6 ) 243.420 * * [simplify]: iteration 2 : 19 enodes (cost 6 ) 243.422 * * [simplify]: iteration 3 : 29 enodes (cost 6 ) 243.425 * * [simplify]: iteration 4 : 51 enodes (cost 6 ) 243.438 * * [simplify]: iteration 5 : 115 enodes (cost 6 ) 243.481 * * [simplify]: iteration 6 : 328 enodes (cost 6 ) 243.925 * * [simplify]: iteration 7 : 1249 enodes (cost 6 ) 246.294 * * [simplify]: iteration done : 5000 enodes (cost 6 ) 246.295 * * [simplify]: iteration 0 : 3 enodes (cost 3 ) 246.295 * * [simplify]: iteration 1 : 6 enodes (cost 1 ) 246.295 * * [simplify]: iteration done : 6 enodes (cost 1 ) 246.296 * * [simplify]: iteration 0 : 7 enodes (cost 7 ) 246.297 * * [simplify]: iteration 1 : 13 enodes (cost 5 ) 246.298 * * [simplify]: iteration 2 : 23 enodes (cost 5 ) 246.300 * * [simplify]: iteration 3 : 41 enodes (cost 5 ) 246.307 * * [simplify]: iteration 4 : 88 enodes (cost 5 ) 246.335 * * [simplify]: iteration 5 : 230 enodes (cost 5 ) 246.525 * * [simplify]: iteration 6 : 762 enodes (cost 5 ) 248.653 * * [simplify]: iteration 7 : 3072 enodes (cost 5 ) 252.100 * * [simplify]: iteration done : 5000 enodes (cost 5 ) 252.101 * * [simplify]: iteration 0 : 6 enodes (cost 6 ) 252.102 * * [simplify]: iteration 1 : 12 enodes (cost 6 ) 252.103 * * [simplify]: iteration 2 : 22 enodes (cost 6 ) 252.105 * * [simplify]: iteration 3 : 42 enodes (cost 6 ) 252.111 * * [simplify]: iteration 4 : 88 enodes (cost 6 ) 252.142 * * [simplify]: iteration 5 : 238 enodes (cost 6 ) 252.332 * * [simplify]: iteration 6 : 767 enodes (cost 6 ) 254.310 * * [simplify]: iteration 7 : 3058 enodes (cost 6 ) 258.488 * * [simplify]: iteration done : 5000 enodes (cost 6 ) 258.489 * * [simplify]: iteration 0 : 6 enodes (cost 6 ) 258.490 * * [simplify]: iteration 1 : 12 enodes (cost 6 ) 258.491 * * [simplify]: iteration 2 : 22 enodes (cost 6 ) 258.499 * * [simplify]: iteration 3 : 42 enodes (cost 6 ) 258.505 * * [simplify]: iteration 4 : 88 enodes (cost 6 ) 258.530 * * [simplify]: iteration 5 : 238 enodes (cost 6 ) 258.724 * * [simplify]: iteration 6 : 767 enodes (cost 6 ) 260.752 * * [simplify]: iteration 7 : 3058 enodes (cost 6 ) 264.735 * * [simplify]: iteration done : 5000 enodes (cost 6 ) 264.736 * * [simplify]: iteration 0 : 5 enodes (cost 5 ) 264.736 * * [simplify]: iteration 1 : 11 enodes (cost 5 ) 264.738 * * [simplify]: iteration 2 : 21 enodes (cost 5 ) 264.740 * * [simplify]: iteration 3 : 39 enodes (cost 5 ) 264.746 * * [simplify]: iteration 4 : 87 enodes (cost 5 ) 264.775 * * [simplify]: iteration 5 : 230 enodes (cost 5 ) 264.975 * * [simplify]: iteration 6 : 754 enodes (cost 5 ) 267.099 * * [simplify]: iteration 7 : 3051 enodes (cost 5 ) 270.554 * * [simplify]: iteration done : 5001 enodes (cost 5 ) 270.555 * * [simplify]: iteration 0 : 5 enodes (cost 5 ) 270.555 * * [simplify]: iteration 1 : 14 enodes (cost 5 ) 270.557 * * [simplify]: iteration 2 : 32 enodes (cost 5 ) 270.562 * * [simplify]: iteration 3 : 54 enodes (cost 5 ) 270.571 * * [simplify]: iteration 4 : 101 enodes (cost 5 ) 270.606 * * [simplify]: iteration 5 : 244 enodes (cost 5 ) 270.802 * * [simplify]: iteration 6 : 773 enodes (cost 5 ) 272.936 * * [simplify]: iteration 7 : 3060 enodes (cost 5 ) 276.231 * * [simplify]: iteration done : 5001 enodes (cost 5 ) 276.231 * * [simplify]: iteration 0 : 5 enodes (cost 5 ) 276.232 * * [simplify]: iteration 1 : 14 enodes (cost 5 ) 276.234 * * [simplify]: iteration 2 : 32 enodes (cost 5 ) 276.238 * * [simplify]: iteration 3 : 54 enodes (cost 5 ) 276.253 * * [simplify]: iteration 4 : 101 enodes (cost 5 ) 276.283 * * [simplify]: iteration 5 : 244 enodes (cost 5 ) 276.481 * * [simplify]: iteration 6 : 773 enodes (cost 5 ) 278.618 * * [simplify]: iteration 7 : 3060 enodes (cost 5 ) 281.925 * * [simplify]: iteration done : 5001 enodes (cost 5 ) 281.926 * * [simplify]: iteration 0 : 5 enodes (cost 5 ) 281.927 * * [simplify]: iteration 1 : 14 enodes (cost 5 ) 281.929 * * [simplify]: iteration 2 : 32 enodes (cost 5 ) 281.933 * * [simplify]: iteration 3 : 54 enodes (cost 5 ) 281.943 * * [simplify]: iteration 4 : 101 enodes (cost 5 ) 281.977 * * [simplify]: iteration 5 : 244 enodes (cost 5 ) 282.169 * * [simplify]: iteration 6 : 773 enodes (cost 5 ) 284.246 * * [simplify]: iteration 7 : 3060 enodes (cost 5 ) 287.507 * * [simplify]: iteration done : 5001 enodes (cost 5 ) 287.507 * * [simplify]: iteration 0 : 5 enodes (cost 5 ) 287.508 * * [simplify]: iteration 1 : 11 enodes (cost 5 ) 287.509 * * [simplify]: iteration 2 : 21 enodes (cost 5 ) 287.512 * * [simplify]: iteration 3 : 39 enodes (cost 5 ) 287.519 * * [simplify]: iteration 4 : 87 enodes (cost 5 ) 287.548 * * [simplify]: iteration 5 : 230 enodes (cost 5 ) 287.744 * * [simplify]: iteration 6 : 754 enodes (cost 5 ) 290.072 * * [simplify]: iteration 7 : 3051 enodes (cost 5 ) 293.532 * * [simplify]: iteration done : 5001 enodes (cost 5 ) 293.532 * * [simplify]: iteration 0 : 5 enodes (cost 5 ) 293.533 * * [simplify]: iteration 1 : 11 enodes (cost 5 ) 293.534 * * [simplify]: iteration 2 : 21 enodes (cost 5 ) 293.537 * * [simplify]: iteration 3 : 39 enodes (cost 5 ) 293.543 * * [simplify]: iteration 4 : 87 enodes (cost 5 ) 293.572 * * [simplify]: iteration 5 : 230 enodes (cost 5 ) 293.769 * * [simplify]: iteration 6 : 754 enodes (cost 5 ) 295.860 * * [simplify]: iteration 7 : 3051 enodes (cost 5 ) 299.257 * * [simplify]: iteration done : 5001 enodes (cost 5 ) 299.258 * * [simplify]: iteration 0 : 5 enodes (cost 5 ) 299.258 * * [simplify]: iteration 1 : 11 enodes (cost 5 ) 299.260 * * [simplify]: iteration 2 : 21 enodes (cost 5 ) 299.262 * * [simplify]: iteration 3 : 39 enodes (cost 5 ) 299.269 * * [simplify]: iteration 4 : 87 enodes (cost 5 ) 299.297 * * [simplify]: iteration 5 : 230 enodes (cost 5 ) 299.496 * * [simplify]: iteration 6 : 754 enodes (cost 5 ) 301.585 * * [simplify]: iteration 7 : 3051 enodes (cost 5 ) 304.982 * * [simplify]: iteration done : 5001 enodes (cost 5 ) 304.983 * [simplify]: Simplified to: (+ (log 1/24) (* (log x) 3)) (+ (log 1/24) (* (log x) 3)) (+ (log 1/24) (log (pow x 3))) (log (* 1/24 (pow x 3))) (exp (* 1/24 (pow x 3))) (* (pow (pow x 3) 3) 1/13824) (* (cbrt (* 1/24 (pow x 3))) (cbrt (* 1/24 (pow x 3)))) (cbrt (* 1/24 (pow x 3))) (pow (* 1/24 (pow x 3)) 3) (sqrt (* 1/24 (pow x 3))) (sqrt (* 1/24 (pow x 3))) (* (sqrt 1/24) (pow (sqrt x) 3)) (* (sqrt 1/24) (pow (sqrt x) 3)) (* (sqrt 1/24) (pow (sqrt x) 3)) (* (sqrt 1/24) (pow (sqrt x) 3)) (* (sqrt 1/24) (sqrt (pow x 3))) (* (sqrt 1/24) (sqrt (pow x 3))) (* (sqrt 1/24) (pow x 3/2)) (* (sqrt 1/24) (pow x 3/2)) (* (* x x) 1/24) (* 1/24 (pow (sqrt x) 3)) 1/24 (* 1/24 (* x x)) (* (* x x) 1/24) (* (* x x) 1/24) (* 1/24 (pow (sqrt x) 3)) 1/24 (* 1/24 x) (* 1/24 (sqrt (pow x 3))) 1/24 (* (pow x 3/2) 1/24) (* (cbrt 1/24) (pow x 3)) (* (sqrt 1/24) (pow x 3)) (* 1/24 (pow x 3)) (+ (log 1/240) (* (log x) 5)) (+ (log 1/240) (* (log x) 5)) (+ (log 1/240) (log (pow x 5))) (log (* 1/240 (pow x 5))) (exp (* 1/240 (pow x 5))) (* (pow (pow x 5) 3) 1/13824000) (* (cbrt (* 1/240 (pow x 5))) (cbrt (* 1/240 (pow x 5)))) (cbrt (* 1/240 (pow x 5))) (pow (* 1/240 (pow x 5)) 3) (sqrt (* 1/240 (pow x 5))) (sqrt (* 1/240 (pow x 5))) (* (sqrt 1/240) (pow (sqrt x) 5)) (* (sqrt 1/240) (pow (sqrt x) 5)) (* (sqrt 1/240) (sqrt (pow x 5))) (* (sqrt 1/240) (sqrt (pow x 5))) (* (sqrt 1/240) (pow x 5/2)) (* (sqrt 1/240) (pow x 5/2)) (* 1/240 (pow (* (cbrt x) (cbrt x)) 5)) (* 1/240 (pow (sqrt x) 5)) 1/240 (* 1/240 (* (cbrt (pow x 5)) (cbrt (pow x 5)))) (* 1/240 (sqrt (pow x 5))) 1/240 (* (pow x 5/2) 1/240) (* (cbrt 1/240) (pow x 5)) (* (sqrt 1/240) (pow x 5)) (* 1/240 (pow x 5)) (* 1/24 (pow x 3)) (* 1/24 (pow x 3)) (* 1/24 (pow x 3)) (* 1/240 (pow x 5)) (* 1/240 (pow x 5)) (* 1/240 (pow x 5)) 304.983 * * * [progress]: adding candidates to table 305.090 * * [progress]: iteration 3 / 4 305.090 * * * [progress]: picking best candidate 305.131 * * * * [pick]: Picked # 305.131 * * * [progress]: localizing error 305.140 * * * [progress]: generating rewritten candidates 305.140 * * * * [progress]: [ 1 / 4 ] rewriting at (2 1) 305.144 * * * * [progress]: [ 2 / 4 ] rewriting at (2) 305.155 * * * * [progress]: [ 3 / 4 ] rewriting at (2 2) 305.160 * * * * [progress]: [ 4 / 4 ] rewriting at (2 2 2) 305.165 * * * [progress]: generating series expansions 305.165 * * * * [progress]: [ 1 / 4 ] generating series at (2 1) 305.165 * [approximate]: Taking taylor expansion of (- 1.0 (cos x)) in (x) around 0 305.165 * [taylor]: Taking taylor expansion of (- 1.0 (cos x)) in x 305.165 * [taylor]: Taking taylor expansion of 1.0 in x 305.165 * [taylor]: Taking taylor expansion of (cos x) in x 305.165 * [taylor]: Taking taylor expansion of x in x 305.165 * [taylor]: Taking taylor expansion of (- 1.0 (cos x)) in x 305.165 * [taylor]: Taking taylor expansion of 1.0 in x 305.165 * [taylor]: Taking taylor expansion of (cos x) in x 305.165 * [taylor]: Taking taylor expansion of x in x 305.167 * [approximate]: Taking taylor expansion of (- 1.0 (cos (/ 1 x))) in (x) around 0 305.167 * [taylor]: Taking taylor expansion of (- 1.0 (cos (/ 1 x))) in x 305.167 * [taylor]: Taking taylor expansion of 1.0 in x 305.167 * [taylor]: Taking taylor expansion of (cos (/ 1 x)) in x 305.167 * [taylor]: Taking taylor expansion of (/ 1 x) in x 305.167 * [taylor]: Taking taylor expansion of x in x 305.167 * [taylor]: Taking taylor expansion of (- 1.0 (cos (/ 1 x))) in x 305.167 * [taylor]: Taking taylor expansion of 1.0 in x 305.167 * [taylor]: Taking taylor expansion of (cos (/ 1 x)) in x 305.167 * [taylor]: Taking taylor expansion of (/ 1 x) in x 305.167 * [taylor]: Taking taylor expansion of x in x 305.168 * [approximate]: Taking taylor expansion of (- 1.0 (cos (/ -1 x))) in (x) around 0 305.168 * [taylor]: Taking taylor expansion of (- 1.0 (cos (/ -1 x))) in x 305.168 * [taylor]: Taking taylor expansion of 1.0 in x 305.168 * [taylor]: Taking taylor expansion of (cos (/ -1 x)) in x 305.168 * [taylor]: Taking taylor expansion of (/ -1 x) in x 305.168 * [taylor]: Taking taylor expansion of -1 in x 305.168 * [taylor]: Taking taylor expansion of x in x 305.168 * [taylor]: Taking taylor expansion of (- 1.0 (cos (/ -1 x))) in x 305.168 * [taylor]: Taking taylor expansion of 1.0 in x 305.168 * [taylor]: Taking taylor expansion of (cos (/ -1 x)) in x 305.168 * [taylor]: Taking taylor expansion of (/ -1 x) in x 305.168 * [taylor]: Taking taylor expansion of -1 in x 305.168 * [taylor]: Taking taylor expansion of x in x 305.168 * * * * [progress]: [ 2 / 4 ] generating series at (2) 305.168 * [approximate]: Taking taylor expansion of (/ (- 1.0 (cos x)) (sin x)) in (x) around 0 305.168 * [taylor]: Taking taylor expansion of (/ (- 1.0 (cos x)) (sin x)) in x 305.168 * [taylor]: Taking taylor expansion of (- 1.0 (cos x)) in x 305.168 * [taylor]: Taking taylor expansion of 1.0 in x 305.168 * [taylor]: Taking taylor expansion of (cos x) in x 305.168 * [taylor]: Taking taylor expansion of x in x 305.168 * [taylor]: Taking taylor expansion of (sin x) in x 305.168 * [taylor]: Taking taylor expansion of x in x 305.169 * [taylor]: Taking taylor expansion of (/ (- 1.0 (cos x)) (sin x)) in x 305.169 * [taylor]: Taking taylor expansion of (- 1.0 (cos x)) in x 305.169 * [taylor]: Taking taylor expansion of 1.0 in x 305.169 * [taylor]: Taking taylor expansion of (cos x) in x 305.169 * [taylor]: Taking taylor expansion of x in x 305.169 * [taylor]: Taking taylor expansion of (sin x) in x 305.169 * [taylor]: Taking taylor expansion of x in x 305.172 * [approximate]: Taking taylor expansion of (/ (- 1.0 (cos (/ 1 x))) (sin (/ 1 x))) in (x) around 0 305.172 * [taylor]: Taking taylor expansion of (/ (- 1.0 (cos (/ 1 x))) (sin (/ 1 x))) in x 305.172 * [taylor]: Taking taylor expansion of (- 1.0 (cos (/ 1 x))) in x 305.172 * [taylor]: Taking taylor expansion of 1.0 in x 305.172 * [taylor]: Taking taylor expansion of (cos (/ 1 x)) in x 305.172 * [taylor]: Taking taylor expansion of (/ 1 x) in x 305.172 * [taylor]: Taking taylor expansion of x in x 305.173 * [taylor]: Taking taylor expansion of (sin (/ 1 x)) in x 305.173 * [taylor]: Taking taylor expansion of (/ 1 x) in x 305.173 * [taylor]: Taking taylor expansion of x in x 305.173 * [taylor]: Taking taylor expansion of (/ (- 1.0 (cos (/ 1 x))) (sin (/ 1 x))) in x 305.173 * [taylor]: Taking taylor expansion of (- 1.0 (cos (/ 1 x))) in x 305.173 * [taylor]: Taking taylor expansion of 1.0 in x 305.173 * [taylor]: Taking taylor expansion of (cos (/ 1 x)) in x 305.173 * [taylor]: Taking taylor expansion of (/ 1 x) in x 305.173 * [taylor]: Taking taylor expansion of x in x 305.173 * [taylor]: Taking taylor expansion of (sin (/ 1 x)) in x 305.173 * [taylor]: Taking taylor expansion of (/ 1 x) in x 305.173 * [taylor]: Taking taylor expansion of x in x 305.175 * [approximate]: Taking taylor expansion of (/ (- 1.0 (cos (/ -1 x))) (sin (/ -1 x))) in (x) around 0 305.175 * [taylor]: Taking taylor expansion of (/ (- 1.0 (cos (/ -1 x))) (sin (/ -1 x))) in x 305.175 * [taylor]: Taking taylor expansion of (- 1.0 (cos (/ -1 x))) in x 305.176 * [taylor]: Taking taylor expansion of 1.0 in x 305.176 * [taylor]: Taking taylor expansion of (cos (/ -1 x)) in x 305.176 * [taylor]: Taking taylor expansion of (/ -1 x) in x 305.176 * [taylor]: Taking taylor expansion of -1 in x 305.176 * [taylor]: Taking taylor expansion of x in x 305.176 * [taylor]: Taking taylor expansion of (sin (/ -1 x)) in x 305.176 * [taylor]: Taking taylor expansion of (/ -1 x) in x 305.176 * [taylor]: Taking taylor expansion of -1 in x 305.176 * [taylor]: Taking taylor expansion of x in x 305.176 * [taylor]: Taking taylor expansion of (/ (- 1.0 (cos (/ -1 x))) (sin (/ -1 x))) in x 305.176 * [taylor]: Taking taylor expansion of (- 1.0 (cos (/ -1 x))) in x 305.176 * [taylor]: Taking taylor expansion of 1.0 in x 305.176 * [taylor]: Taking taylor expansion of (cos (/ -1 x)) in x 305.176 * [taylor]: Taking taylor expansion of (/ -1 x) in x 305.176 * [taylor]: Taking taylor expansion of -1 in x 305.176 * [taylor]: Taking taylor expansion of x in x 305.176 * [taylor]: Taking taylor expansion of (sin (/ -1 x)) in x 305.176 * [taylor]: Taking taylor expansion of (/ -1 x) in x 305.176 * [taylor]: Taking taylor expansion of -1 in x 305.176 * [taylor]: Taking taylor expansion of x in x 305.178 * * * * [progress]: [ 3 / 4 ] generating series at (2 2) 305.178 * [approximate]: Taking taylor expansion of (/ 1 (sin x)) in (x) around 0 305.178 * [taylor]: Taking taylor expansion of (/ 1 (sin x)) in x 305.178 * [taylor]: Taking taylor expansion of (sin x) in x 305.178 * [taylor]: Taking taylor expansion of x in x 305.178 * [taylor]: Taking taylor expansion of (/ 1 (sin x)) in x 305.178 * [taylor]: Taking taylor expansion of (sin x) in x 305.178 * [taylor]: Taking taylor expansion of x in x 305.180 * [approximate]: Taking taylor expansion of (/ 1 (sin (/ 1 x))) in (x) around 0 305.180 * [taylor]: Taking taylor expansion of (/ 1 (sin (/ 1 x))) in x 305.180 * [taylor]: Taking taylor expansion of (sin (/ 1 x)) in x 305.180 * [taylor]: Taking taylor expansion of (/ 1 x) in x 305.180 * [taylor]: Taking taylor expansion of x in x 305.180 * [taylor]: Taking taylor expansion of (/ 1 (sin (/ 1 x))) in x 305.180 * [taylor]: Taking taylor expansion of (sin (/ 1 x)) in x 305.180 * [taylor]: Taking taylor expansion of (/ 1 x) in x 305.180 * [taylor]: Taking taylor expansion of x in x 305.181 * [approximate]: Taking taylor expansion of (/ 1 (sin (/ -1 x))) in (x) around 0 305.182 * [taylor]: Taking taylor expansion of (/ 1 (sin (/ -1 x))) in x 305.182 * [taylor]: Taking taylor expansion of (sin (/ -1 x)) in x 305.182 * [taylor]: Taking taylor expansion of (/ -1 x) in x 305.182 * [taylor]: Taking taylor expansion of -1 in x 305.182 * [taylor]: Taking taylor expansion of x in x 305.182 * [taylor]: Taking taylor expansion of (/ 1 (sin (/ -1 x))) in x 305.182 * [taylor]: Taking taylor expansion of (sin (/ -1 x)) in x 305.182 * [taylor]: Taking taylor expansion of (/ -1 x) in x 305.182 * [taylor]: Taking taylor expansion of -1 in x 305.182 * [taylor]: Taking taylor expansion of x in x 305.183 * * * * [progress]: [ 4 / 4 ] generating series at (2 2 2) 305.183 * [approximate]: Taking taylor expansion of (sin x) in (x) around 0 305.183 * [taylor]: Taking taylor expansion of (sin x) in x 305.183 * [taylor]: Taking taylor expansion of x in x 305.183 * [taylor]: Taking taylor expansion of (sin x) in x 305.183 * [taylor]: Taking taylor expansion of x in x 305.184 * [approximate]: Taking taylor expansion of (sin (/ 1 x)) in (x) around 0 305.184 * [taylor]: Taking taylor expansion of (sin (/ 1 x)) in x 305.184 * [taylor]: Taking taylor expansion of (/ 1 x) in x 305.184 * [taylor]: Taking taylor expansion of x in x 305.184 * [taylor]: Taking taylor expansion of (sin (/ 1 x)) in x 305.184 * [taylor]: Taking taylor expansion of (/ 1 x) in x 305.184 * [taylor]: Taking taylor expansion of x in x 305.185 * [approximate]: Taking taylor expansion of (sin (/ -1 x)) in (x) around 0 305.185 * [taylor]: Taking taylor expansion of (sin (/ -1 x)) in x 305.185 * [taylor]: Taking taylor expansion of (/ -1 x) in x 305.185 * [taylor]: Taking taylor expansion of -1 in x 305.185 * [taylor]: Taking taylor expansion of x in x 305.185 * [taylor]: Taking taylor expansion of (sin (/ -1 x)) in x 305.185 * [taylor]: Taking taylor expansion of (/ -1 x) in x 305.185 * [taylor]: Taking taylor expansion of -1 in x 305.185 * [taylor]: Taking taylor expansion of x in x 305.185 * * * [progress]: simplifying candidates 305.186 * [simplify]: Simplifying using # : (/ (exp 1.0) (exp (cos x))) (log (- 1.0 (cos x))) (exp (- 1.0 (cos x))) (* (cbrt (- 1.0 (cos x))) (cbrt (- 1.0 (cos x)))) (cbrt (- 1.0 (cos x))) (* (* (- 1.0 (cos x)) (- 1.0 (cos x))) (- 1.0 (cos x))) (sqrt (- 1.0 (cos x))) (sqrt (- 1.0 (cos x))) (- (pow 1.0 3) (pow (cos x) 3)) (+ (* 1.0 1.0) (+ (* (cos x) (cos x)) (* 1.0 (cos x)))) (neg (cos x)) (- (* 1.0 1.0) (* (cos x) (cos x))) (+ 1.0 (cos x)) (+ (sqrt 1.0) (sqrt (cos x))) (- (sqrt 1.0) (sqrt (cos x))) (- 1.0 (cos x)) (neg (cos x)) (* (- 1.0 (cos x)) (/ 1 (sin x))) (+ (log (- 1.0 (cos x))) (neg (log (sin x)))) (+ (log (- 1.0 (cos x))) (- 0 (log (sin x)))) (+ (log (- 1.0 (cos x))) (- (log 1) (log (sin x)))) (+ (log (- 1.0 (cos x))) (log (/ 1 (sin x)))) (log (* (- 1.0 (cos x)) (/ 1 (sin x)))) (exp (* (- 1.0 (cos x)) (/ 1 (sin x)))) (* (* (* (- 1.0 (cos x)) (- 1.0 (cos x))) (- 1.0 (cos x))) (/ (* (* 1 1) 1) (* (* (sin x) (sin x)) (sin x)))) (* (* (* (- 1.0 (cos x)) (- 1.0 (cos x))) (- 1.0 (cos x))) (* (* (/ 1 (sin x)) (/ 1 (sin x))) (/ 1 (sin x)))) (* (cbrt (* (- 1.0 (cos x)) (/ 1 (sin x)))) (cbrt (* (- 1.0 (cos x)) (/ 1 (sin x))))) (cbrt (* (- 1.0 (cos x)) (/ 1 (sin x)))) (* (* (* (- 1.0 (cos x)) (/ 1 (sin x))) (* (- 1.0 (cos x)) (/ 1 (sin x)))) (* (- 1.0 (cos x)) (/ 1 (sin x)))) (sqrt (* (- 1.0 (cos x)) (/ 1 (sin x)))) (sqrt (* (- 1.0 (cos x)) (/ 1 (sin x)))) (* (- (pow 1.0 3) (pow (cos x) 3)) 1) (* (+ (* 1.0 1.0) (+ (* (cos x) (cos x)) (* 1.0 (cos x)))) (sin x)) (* (- (* 1.0 1.0) (* (cos x) (cos x))) 1) (* (+ 1.0 (cos x)) (sin x)) (* (sqrt (- 1.0 (cos x))) (sqrt (/ 1 (sin x)))) (* (sqrt (- 1.0 (cos x))) (sqrt (/ 1 (sin x)))) (* (sqrt (- 1.0 (cos x))) (/ (sqrt 1) (sqrt (sin x)))) (* (sqrt (- 1.0 (cos x))) (/ (sqrt 1) (sqrt (sin x)))) (* (sqrt (- 1.0 (cos x))) (/ 1 (sqrt (sin x)))) (* (sqrt (- 1.0 (cos x))) (/ 1 (sqrt (sin x)))) (* (- 1.0 (cos x)) (* (cbrt (/ 1 (sin x))) (cbrt (/ 1 (sin x))))) (* (- 1.0 (cos x)) (sqrt (/ 1 (sin x)))) (* (- 1.0 (cos x)) (/ (* (cbrt 1) (cbrt 1)) (* (cbrt (sin x)) (cbrt (sin x))))) (* (- 1.0 (cos x)) (/ (* (cbrt 1) (cbrt 1)) (sqrt (sin x)))) (* (- 1.0 (cos x)) (/ (* (cbrt 1) (cbrt 1)) 1)) (* (- 1.0 (cos x)) (/ (sqrt 1) (* (cbrt (sin x)) (cbrt (sin x))))) (* (- 1.0 (cos x)) (/ (sqrt 1) (sqrt (sin x)))) (* (- 1.0 (cos x)) (/ (sqrt 1) 1)) (* (- 1.0 (cos x)) (/ 1 (* (cbrt (sin x)) (cbrt (sin x))))) (* (- 1.0 (cos x)) (/ 1 (sqrt (sin x)))) (* (- 1.0 (cos x)) (/ 1 1)) (* (- 1.0 (cos x)) 1) (* (- 1.0 (cos x)) 1) (* (cbrt (- 1.0 (cos x))) (/ 1 (sin x))) (* (sqrt (- 1.0 (cos x))) (/ 1 (sin x))) (* (- 1.0 (cos x)) (/ 1 (sin x))) (* (- (sqrt 1.0) (sqrt (cos x))) (/ 1 (sin x))) (* (- 1.0 (cos x)) (/ 1 (sin x))) (* (- 1.0 (cos x)) 1) (* (- (pow 1.0 3) (pow (cos x) 3)) (/ 1 (sin x))) (* (- (* 1.0 1.0) (* (cos x) (cos x))) (/ 1 (sin x))) (neg 1) (neg (log (sin x))) (- 0 (log (sin x))) (- (log 1) (log (sin x))) (log (/ 1 (sin x))) (exp (/ 1 (sin x))) (/ (* (* 1 1) 1) (* (* (sin x) (sin x)) (sin x))) (* (cbrt (/ 1 (sin x))) (cbrt (/ 1 (sin x)))) (cbrt (/ 1 (sin x))) (* (* (/ 1 (sin x)) (/ 1 (sin x))) (/ 1 (sin x))) (sqrt (/ 1 (sin x))) (sqrt (/ 1 (sin x))) (neg 1) (neg (sin x)) (/ (* (cbrt 1) (cbrt 1)) (* (cbrt (sin x)) (cbrt (sin x)))) (/ (cbrt 1) (cbrt (sin x))) (/ (* (cbrt 1) (cbrt 1)) (sqrt (sin x))) (/ (cbrt 1) (sqrt (sin x))) (/ (* (cbrt 1) (cbrt 1)) 1) (/ (cbrt 1) (sin x)) (/ (sqrt 1) (* (cbrt (sin x)) (cbrt (sin x)))) (/ (sqrt 1) (cbrt (sin x))) (/ (sqrt 1) (sqrt (sin x))) (/ (sqrt 1) (sqrt (sin x))) (/ (sqrt 1) 1) (/ (sqrt 1) (sin x)) (/ 1 (* (cbrt (sin x)) (cbrt (sin x)))) (/ 1 (cbrt (sin x))) (/ 1 (sqrt (sin x))) (/ 1 (sqrt (sin x))) (/ 1 1) (/ 1 (sin x)) (/ 1 (sin x)) (/ (sin x) 1) (/ 1 (* (cbrt (sin x)) (cbrt (sin x)))) (/ 1 (sqrt (sin x))) (/ 1 1) (/ (sin x) (cbrt 1)) (/ (sin x) (sqrt 1)) (/ (sin x) 1) (log (sin x)) (exp (sin x)) (* (cbrt (sin x)) (cbrt (sin x))) (cbrt (sin x)) (* (* (sin x) (sin x)) (sin x)) (sqrt (sin x)) (sqrt (sin x)) (- (+ (* 1/2 (pow x 2)) (* 1/720 (pow x 6))) (* 1/24 (pow x 4))) (- 1.0 (cos x)) (- 1.0 (cos x)) (+ (* 1/2 x) (+ (* 1/24 (pow x 3)) (* 1/240 (pow x 5)))) (/ (- 1.0 (cos x)) (sin x)) (/ (- 1.0 (cos x)) (sin x)) (+ (* 1/6 x) (+ (/ 1 x) (* 7/360 (pow x 3)))) (/ 1 (sin x)) (/ 1 (sin x)) (- (+ x (* 1/120 (pow x 5))) (* 1/6 (pow x 3))) (sin x) (sin x) 305.187 * * [simplify]: iteration 0 : 6 enodes (cost 6 ) 305.192 * * [simplify]: iteration 1 : 8 enodes (cost 5 ) 305.193 * * [simplify]: iteration 2 : 10 enodes (cost 5 ) 305.194 * * [simplify]: iteration 3 : 13 enodes (cost 5 ) 305.195 * * [simplify]: iteration 4 : 16 enodes (cost 5 ) 305.197 * * [simplify]: iteration 5 : 22 enodes (cost 5 ) 305.199 * * [simplify]: iteration 6 : 26 enodes (cost 5 ) 305.203 * * [simplify]: iteration 7 : 42 enodes (cost 5 ) 305.208 * * [simplify]: iteration 8 : 46 enodes (cost 5 ) 305.212 * * [simplify]: iteration 9 : 51 enodes (cost 5 ) 305.218 * * [simplify]: iteration 10 : 58 enodes (cost 5 ) 305.225 * * [simplify]: iteration 11 : 76 enodes (cost 5 ) 305.235 * * [simplify]: iteration 12 : 97 enodes (cost 5 ) 305.253 * * [simplify]: iteration 13 : 115 enodes (cost 5 ) 305.267 * * [simplify]: iteration 14 : 118 enodes (cost 5 ) 305.280 * * [simplify]: iteration done : 118 enodes (cost 5 ) 305.280 * * [simplify]: iteration 0 : 5 enodes (cost 5 ) 305.281 * * [simplify]: iteration 1 : 7 enodes (cost 5 ) 305.281 * * [simplify]: iteration 2 : 8 enodes (cost 5 ) 305.282 * * [simplify]: iteration done : 8 enodes (cost 5 ) 305.283 * * [simplify]: iteration 0 : 5 enodes (cost 5 ) 305.283 * * [simplify]: iteration 1 : 10 enodes (cost 5 ) 305.285 * * [simplify]: iteration 2 : 13 enodes (cost 5 ) 305.286 * * [simplify]: iteration 3 : 16 enodes (cost 5 ) 305.288 * * [simplify]: iteration 4 : 22 enodes (cost 5 ) 305.291 * * [simplify]: iteration 5 : 26 enodes (cost 5 ) 305.294 * * [simplify]: iteration 6 : 42 enodes (cost 5 ) 305.299 * * [simplify]: iteration 7 : 46 enodes (cost 5 ) 305.303 * * [simplify]: iteration 8 : 51 enodes (cost 5 ) 305.312 * * [simplify]: iteration 9 : 58 enodes (cost 5 ) 305.319 * * [simplify]: iteration 10 : 77 enodes (cost 5 ) 305.329 * * [simplify]: iteration 11 : 98 enodes (cost 5 ) 305.342 * * [simplify]: iteration 12 : 111 enodes (cost 5 ) 305.355 * * [simplify]: iteration 13 : 114 enodes (cost 5 ) 305.373 * * [simplify]: iteration done : 114 enodes (cost 5 ) 305.373 * * [simplify]: iteration 0 : 6 enodes (cost 11 ) 305.374 * * [simplify]: iteration 1 : 8 enodes (cost 11 ) 305.375 * * [simplify]: iteration 2 : 9 enodes (cost 11 ) 305.376 * * [simplify]: iteration done : 9 enodes (cost 11 ) 305.376 * * [simplify]: iteration 0 : 5 enodes (cost 5 ) 305.377 * * [simplify]: iteration 1 : 7 enodes (cost 5 ) 305.377 * * [simplify]: iteration 2 : 8 enodes (cost 5 ) 305.378 * * [simplify]: iteration done : 8 enodes (cost 5 ) 305.379 * * [simplify]: iteration 0 : 6 enodes (cost 14 ) 305.379 * * [simplify]: iteration 1 : 9 enodes (cost 14 ) 305.381 * * [simplify]: iteration 2 : 24 enodes (cost 6 ) 305.385 * * [simplify]: iteration 3 : 67 enodes (cost 6 ) 305.399 * * [simplify]: iteration 4 : 176 enodes (cost 6 ) 305.464 * * [simplify]: iteration 5 : 500 enodes (cost 6 ) 305.939 * * [simplify]: iteration 6 : 1723 enodes (cost 6 ) 308.812 * * [simplify]: iteration 7 : 4988 enodes (cost 6 ) 310.019 * * [simplify]: iteration done : 5000 enodes (cost 6 ) 310.019 * * [simplify]: iteration 0 : 5 enodes (cost 5 ) 310.020 * * [simplify]: iteration 1 : 7 enodes (cost 5 ) 310.020 * * [simplify]: iteration 2 : 8 enodes (cost 5 ) 310.021 * * [simplify]: iteration done : 8 enodes (cost 5 ) 310.022 * * [simplify]: iteration 0 : 5 enodes (cost 5 ) 310.022 * * [simplify]: iteration 1 : 7 enodes (cost 5 ) 310.023 * * [simplify]: iteration 2 : 8 enodes (cost 5 ) 310.024 * * [simplify]: iteration done : 8 enodes (cost 5 ) 310.024 * * [simplify]: iteration 0 : 7 enodes (cost 8 ) 310.025 * * [simplify]: iteration 1 : 22 enodes (cost 8 ) 310.029 * * [simplify]: iteration 2 : 44 enodes (cost 8 ) 310.042 * * [simplify]: iteration 3 : 78 enodes (cost 8 ) 310.055 * * [simplify]: iteration 4 : 165 enodes (cost 8 ) 310.103 * * [simplify]: iteration 5 : 500 enodes (cost 8 ) 310.451 * * [simplify]: iteration 6 : 2253 enodes (cost 8 ) 311.614 * * [simplify]: iteration done : 5001 enodes (cost 8 ) 311.615 * * [simplify]: iteration 0 : 8 enodes (cost 14 ) 311.616 * * [simplify]: iteration 1 : 15 enodes (cost 11 ) 311.624 * * [simplify]: iteration 2 : 23 enodes (cost 11 ) 311.627 * * [simplify]: iteration 3 : 26 enodes (cost 11 ) 311.631 * * [simplify]: iteration 4 : 27 enodes (cost 11 ) 311.634 * * [simplify]: iteration done : 27 enodes (cost 11 ) 311.635 * * [simplify]: iteration 0 : 3 enodes (cost 3 ) 311.635 * * [simplify]: iteration done : 3 enodes (cost 3 ) 311.636 * * [simplify]: iteration 0 : 6 enodes (cost 9 ) 311.637 * * [simplify]: iteration 1 : 11 enodes (cost 9 ) 311.638 * * [simplify]: iteration 2 : 18 enodes (cost 9 ) 311.641 * * [simplify]: iteration 3 : 33 enodes (cost 9 ) 311.646 * * [simplify]: iteration 4 : 58 enodes (cost 9 ) 311.657 * * [simplify]: iteration 5 : 99 enodes (cost 9 ) 311.684 * * [simplify]: iteration 6 : 161 enodes (cost 9 ) 311.737 * * [simplify]: iteration 7 : 329 enodes (cost 9 ) 312.462 * * [simplify]: iteration 8 : 1606 enodes (cost 9 ) 318.851 * * [simplify]: iteration done : 5000 enodes (cost 9 ) 318.851 * * [simplify]: iteration 0 : 4 enodes (cost 4 ) 318.852 * * [simplify]: iteration 1 : 5 enodes (cost 4 ) 318.852 * * [simplify]: iteration done : 5 enodes (cost 4 ) 318.853 * * [simplify]: iteration 0 : 6 enodes (cost 6 ) 318.854 * * [simplify]: iteration 1 : 7 enodes (cost 6 ) 318.854 * * [simplify]: iteration done : 7 enodes (cost 6 ) 318.855 * * [simplify]: iteration 0 : 6 enodes (cost 6 ) 318.855 * * [simplify]: iteration 1 : 8 enodes (cost 6 ) 318.856 * * [simplify]: iteration 2 : 9 enodes (cost 6 ) 318.857 * * [simplify]: iteration done : 9 enodes (cost 6 ) 318.858 * * [simplify]: iteration 0 : 4 enodes (cost 4 ) 318.858 * * [simplify]: iteration 1 : 6 enodes (cost 4 ) 318.859 * * [simplify]: iteration 2 : 7 enodes (cost 4 ) 318.859 * * [simplify]: iteration done : 7 enodes (cost 4 ) 318.860 * * [simplify]: iteration 0 : 3 enodes (cost 3 ) 318.860 * * [simplify]: iteration done : 3 enodes (cost 3 ) 318.861 * * [simplify]: iteration 0 : 8 enodes (cost 9 ) 318.862 * * [simplify]: iteration 1 : 15 enodes (cost 9 ) 318.864 * * [simplify]: iteration 2 : 25 enodes (cost 7 ) 318.868 * * [simplify]: iteration 3 : 60 enodes (cost 7 ) 318.880 * * [simplify]: iteration 4 : 102 enodes (cost 7 ) 318.898 * * [simplify]: iteration 5 : 129 enodes (cost 7 ) 318.916 * * [simplify]: iteration 6 : 151 enodes (cost 7 ) 318.935 * * [simplify]: iteration 7 : 156 enodes (cost 7 ) 318.959 * * [simplify]: iteration 8 : 157 enodes (cost 7 ) 318.978 * * [simplify]: iteration done : 157 enodes (cost 7 ) 318.979 * * [simplify]: iteration 0 : 9 enodes (cost 10 ) 318.980 * * [simplify]: iteration 1 : 13 enodes (cost 9 ) 318.982 * * [simplify]: iteration 2 : 14 enodes (cost 9 ) 318.983 * * [simplify]: iteration done : 14 enodes (cost 9 ) 318.984 * * [simplify]: iteration 0 : 10 enodes (cost 11 ) 318.985 * * [simplify]: iteration 1 : 17 enodes (cost 10 ) 318.987 * * [simplify]: iteration 2 : 28 enodes (cost 9 ) 318.990 * * [simplify]: iteration 3 : 37 enodes (cost 9 ) 318.996 * * [simplify]: iteration 4 : 55 enodes (cost 9 ) 319.006 * * [simplify]: iteration 5 : 81 enodes (cost 9 ) 319.021 * * [simplify]: iteration 6 : 84 enodes (cost 9 ) 319.031 * * [simplify]: iteration 7 : 93 enodes (cost 9 ) 319.047 * * [simplify]: iteration 8 : 111 enodes (cost 9 ) 319.057 * * [simplify]: iteration done : 111 enodes (cost 9 ) 319.058 * * [simplify]: iteration 0 : 11 enodes (cost 12 ) 319.059 * * [simplify]: iteration 1 : 20 enodes (cost 11 ) 319.061 * * [simplify]: iteration 2 : 28 enodes (cost 9 ) 319.065 * * [simplify]: iteration 3 : 45 enodes (cost 9 ) 319.075 * * [simplify]: iteration 4 : 63 enodes (cost 9 ) 319.086 * * [simplify]: iteration 5 : 88 enodes (cost 9 ) 319.097 * * [simplify]: iteration 6 : 93 enodes (cost 9 ) 319.107 * * [simplify]: iteration 7 : 102 enodes (cost 9 ) 319.122 * * [simplify]: iteration 8 : 116 enodes (cost 9 ) 319.137 * * [simplify]: iteration done : 116 enodes (cost 9 ) 319.137 * * [simplify]: iteration 0 : 10 enodes (cost 11 ) 319.139 * * [simplify]: iteration 1 : 19 enodes (cost 10 ) 319.140 * * [simplify]: iteration 2 : 26 enodes (cost 9 ) 319.143 * * [simplify]: iteration 3 : 37 enodes (cost 9 ) 319.148 * * [simplify]: iteration 4 : 49 enodes (cost 9 ) 319.157 * * [simplify]: iteration 5 : 81 enodes (cost 9 ) 319.171 * * [simplify]: iteration 6 : 100 enodes (cost 9 ) 319.181 * * [simplify]: iteration 7 : 107 enodes (cost 9 ) 319.198 * * [simplify]: iteration 8 : 117 enodes (cost 9 ) 319.211 * * [simplify]: iteration done : 117 enodes (cost 9 ) 319.212 * * [simplify]: iteration 0 : 9 enodes (cost 10 ) 319.213 * * [simplify]: iteration 1 : 19 enodes (cost 10 ) 319.215 * * [simplify]: iteration 2 : 35 enodes (cost 8 ) 319.220 * * [simplify]: iteration 3 : 76 enodes (cost 8 ) 319.236 * * [simplify]: iteration 4 : 136 enodes (cost 8 ) 319.260 * * [simplify]: iteration 5 : 178 enodes (cost 8 ) 319.291 * * [simplify]: iteration 6 : 233 enodes (cost 8 ) 319.323 * * [simplify]: iteration 7 : 243 enodes (cost 8 ) 319.356 * * [simplify]: iteration 8 : 251 enodes (cost 8 ) 319.389 * * [simplify]: iteration done : 251 enodes (cost 8 ) 319.389 * * [simplify]: iteration 0 : 9 enodes (cost 10 ) 319.391 * * [simplify]: iteration 1 : 18 enodes (cost 10 ) 319.394 * * [simplify]: iteration 2 : 39 enodes (cost 8 ) 319.401 * * [simplify]: iteration 3 : 92 enodes (cost 8 ) 319.421 * * [simplify]: iteration 4 : 193 enodes (cost 8 ) 319.469 * * [simplify]: iteration 5 : 356 enodes (cost 8 ) 319.636 * * [simplify]: iteration 6 : 863 enodes (cost 8 ) 320.742 * * [simplify]: iteration 7 : 3112 enodes (cost 8 ) 321.998 * * [simplify]: iteration done : 5000 enodes (cost 8 ) 321.999 * * [simplify]: iteration 0 : 14 enodes (cost 29 ) 322.002 * * [simplify]: iteration 1 : 32 enodes (cost 25 ) 322.007 * * [simplify]: iteration 2 : 91 enodes (cost 11 ) 322.043 * * [simplify]: iteration 3 : 352 enodes (cost 11 ) 322.351 * * [simplify]: iteration 4 : 1235 enodes (cost 11 ) 324.494 * * [simplify]: iteration 5 : 4515 enodes (cost 9 ) 325.940 * * [simplify]: iteration done : 5001 enodes (cost 9 ) 325.941 * * [simplify]: iteration 0 : 12 enodes (cost 29 ) 325.943 * * [simplify]: iteration 1 : 29 enodes (cost 29 ) 325.948 * * [simplify]: iteration 2 : 91 enodes (cost 13 ) 325.987 * * [simplify]: iteration 3 : 304 enodes (cost 13 ) 326.219 * * [simplify]: iteration 4 : 1103 enodes (cost 9 ) 327.980 * * [simplify]: iteration 5 : 4248 enodes (cost 9 ) 329.513 * * [simplify]: iteration done : 5000 enodes (cost 9 ) 329.514 * * [simplify]: iteration 0 : 10 enodes (cost 21 ) 329.515 * * [simplify]: iteration 1 : 17 enodes (cost 21 ) 329.517 * * [simplify]: iteration 2 : 27 enodes (cost 17 ) 329.522 * * [simplify]: iteration 3 : 62 enodes (cost 17 ) 329.534 * * [simplify]: iteration 4 : 104 enodes (cost 17 ) 329.549 * * [simplify]: iteration 5 : 131 enodes (cost 17 ) 329.572 * * [simplify]: iteration 6 : 153 enodes (cost 17 ) 329.591 * * [simplify]: iteration 7 : 158 enodes (cost 17 ) 329.615 * * [simplify]: iteration 8 : 159 enodes (cost 17 ) 329.633 * * [simplify]: iteration done : 159 enodes (cost 17 ) 329.634 * * [simplify]: iteration 0 : 9 enodes (cost 10 ) 329.635 * * [simplify]: iteration 1 : 16 enodes (cost 10 ) 329.637 * * [simplify]: iteration 2 : 26 enodes (cost 8 ) 329.641 * * [simplify]: iteration 3 : 61 enodes (cost 8 ) 329.654 * * [simplify]: iteration 4 : 105 enodes (cost 8 ) 329.668 * * [simplify]: iteration 5 : 132 enodes (cost 8 ) 329.690 * * [simplify]: iteration 6 : 154 enodes (cost 8 ) 329.709 * * [simplify]: iteration 7 : 159 enodes (cost 8 ) 329.733 * * [simplify]: iteration 8 : 160 enodes (cost 8 ) 329.751 * * [simplify]: iteration done : 160 enodes (cost 8 ) 329.752 * * [simplify]: iteration 0 : 10 enodes (cost 29 ) 329.753 * * [simplify]: iteration 1 : 27 enodes (cost 29 ) 329.760 * * [simplify]: iteration 2 : 106 enodes (cost 9 ) 329.820 * * [simplify]: iteration 3 : 467 enodes (cost 9 ) 330.272 * * [simplify]: iteration 4 : 1616 enodes (cost 9 ) 332.875 * * [simplify]: iteration 5 : 4522 enodes (cost 9 ) 334.770 * * [simplify]: iteration done : 5000 enodes (cost 9 ) 334.771 * * [simplify]: iteration 0 : 9 enodes (cost 10 ) 334.772 * * [simplify]: iteration 1 : 16 enodes (cost 10 ) 334.773 * * [simplify]: iteration 2 : 26 enodes (cost 8 ) 334.778 * * [simplify]: iteration 3 : 61 enodes (cost 8 ) 334.796 * * [simplify]: iteration 4 : 105 enodes (cost 8 ) 334.810 * * [simplify]: iteration 5 : 132 enodes (cost 8 ) 334.829 * * [simplify]: iteration 6 : 154 enodes (cost 8 ) 334.851 * * [simplify]: iteration 7 : 159 enodes (cost 8 ) 334.871 * * [simplify]: iteration 8 : 160 enodes (cost 8 ) 334.889 * * [simplify]: iteration done : 160 enodes (cost 8 ) 334.889 * * [simplify]: iteration 0 : 9 enodes (cost 10 ) 334.890 * * [simplify]: iteration 1 : 16 enodes (cost 10 ) 334.893 * * [simplify]: iteration 2 : 26 enodes (cost 8 ) 334.900 * * [simplify]: iteration 3 : 61 enodes (cost 8 ) 334.913 * * [simplify]: iteration 4 : 105 enodes (cost 8 ) 334.927 * * [simplify]: iteration 5 : 132 enodes (cost 8 ) 334.945 * * [simplify]: iteration 6 : 154 enodes (cost 8 ) 334.968 * * [simplify]: iteration 7 : 159 enodes (cost 8 ) 334.987 * * [simplify]: iteration 8 : 160 enodes (cost 8 ) 335.006 * * [simplify]: iteration done : 160 enodes (cost 8 ) 335.006 * * [simplify]: iteration 0 : 9 enodes (cost 10 ) 335.008 * * [simplify]: iteration 1 : 27 enodes (cost 8 ) 335.016 * * [simplify]: iteration 2 : 58 enodes (cost 8 ) 335.026 * * [simplify]: iteration 3 : 143 enodes (cost 8 ) 335.088 * * [simplify]: iteration 4 : 377 enodes (cost 8 ) 335.280 * * [simplify]: iteration 5 : 997 enodes (cost 8 ) 336.537 * * [simplify]: iteration 6 : 3719 enodes (cost 8 ) 338.220 * * [simplify]: iteration done : 5001 enodes (cost 8 ) 338.221 * * [simplify]: iteration 0 : 10 enodes (cost 17 ) 338.222 * * [simplify]: iteration 1 : 18 enodes (cost 14 ) 338.225 * * [simplify]: iteration 2 : 40 enodes (cost 14 ) 338.233 * * [simplify]: iteration 3 : 74 enodes (cost 14 ) 338.247 * * [simplify]: iteration 4 : 89 enodes (cost 14 ) 338.262 * * [simplify]: iteration 5 : 91 enodes (cost 14 ) 338.281 * * [simplify]: iteration done : 91 enodes (cost 14 ) 338.282 * * [simplify]: iteration 0 : 8 enodes (cost 11 ) 338.283 * * [simplify]: iteration 1 : 16 enodes (cost 9 ) 338.285 * * [simplify]: iteration 2 : 36 enodes (cost 9 ) 338.293 * * [simplify]: iteration 3 : 93 enodes (cost 9 ) 338.319 * * [simplify]: iteration 4 : 183 enodes (cost 9 ) 338.350 * * [simplify]: iteration 5 : 240 enodes (cost 9 ) 338.408 * * [simplify]: iteration 6 : 340 enodes (cost 9 ) 338.537 * * [simplify]: iteration 7 : 565 enodes (cost 9 ) 339.527 * * [simplify]: iteration 8 : 2001 enodes (cost 9 ) 343.744 * * [simplify]: iteration done : 5000 enodes (cost 9 ) 343.745 * * [simplify]: iteration 0 : 6 enodes (cost 7 ) 343.746 * * [simplify]: iteration 1 : 8 enodes (cost 7 ) 343.747 * * [simplify]: iteration 2 : 16 enodes (cost 7 ) 343.749 * * [simplify]: iteration done : 16 enodes (cost 7 ) 343.749 * * [simplify]: iteration 0 : 10 enodes (cost 11 ) 343.754 * * [simplify]: iteration 1 : 15 enodes (cost 11 ) 343.756 * * [simplify]: iteration 2 : 16 enodes (cost 11 ) 343.757 * * [simplify]: iteration done : 16 enodes (cost 11 ) 343.758 * * [simplify]: iteration 0 : 10 enodes (cost 11 ) 343.759 * * [simplify]: iteration 1 : 15 enodes (cost 11 ) 343.760 * * [simplify]: iteration 2 : 16 enodes (cost 11 ) 343.761 * * [simplify]: iteration done : 16 enodes (cost 11 ) 343.762 * * [simplify]: iteration 0 : 11 enodes (cost 12 ) 343.763 * * [simplify]: iteration 1 : 18 enodes (cost 11 ) 343.765 * * [simplify]: iteration 2 : 22 enodes (cost 11 ) 343.768 * * [simplify]: iteration 3 : 26 enodes (cost 9 ) 343.771 * * [simplify]: iteration 4 : 37 enodes (cost 9 ) 343.775 * * [simplify]: iteration done : 37 enodes (cost 9 ) 343.776 * * [simplify]: iteration 0 : 11 enodes (cost 12 ) 343.777 * * [simplify]: iteration 1 : 18 enodes (cost 11 ) 343.778 * * [simplify]: iteration 2 : 22 enodes (cost 11 ) 343.781 * * [simplify]: iteration 3 : 26 enodes (cost 9 ) 343.784 * * [simplify]: iteration 4 : 37 enodes (cost 9 ) 343.788 * * [simplify]: iteration done : 37 enodes (cost 9 ) 343.789 * * [simplify]: iteration 0 : 10 enodes (cost 11 ) 343.790 * * [simplify]: iteration 1 : 17 enodes (cost 11 ) 343.791 * * [simplify]: iteration 2 : 21 enodes (cost 9 ) 343.794 * * [simplify]: iteration 3 : 36 enodes (cost 9 ) 343.798 * * [simplify]: iteration 4 : 39 enodes (cost 9 ) 343.802 * * [simplify]: iteration done : 39 enodes (cost 9 ) 343.803 * * [simplify]: iteration 0 : 10 enodes (cost 11 ) 343.804 * * [simplify]: iteration 1 : 17 enodes (cost 11 ) 343.805 * * [simplify]: iteration 2 : 21 enodes (cost 9 ) 343.808 * * [simplify]: iteration 3 : 36 enodes (cost 9 ) 343.812 * * [simplify]: iteration 4 : 39 enodes (cost 9 ) 343.819 * * [simplify]: iteration done : 39 enodes (cost 9 ) 343.819 * * [simplify]: iteration 0 : 10 enodes (cost 16 ) 343.820 * * [simplify]: iteration 1 : 17 enodes (cost 16 ) 343.823 * * [simplify]: iteration 2 : 26 enodes (cost 16 ) 343.826 * * [simplify]: iteration 3 : 43 enodes (cost 16 ) 343.833 * * [simplify]: iteration 4 : 57 enodes (cost 16 ) 343.841 * * [simplify]: iteration 5 : 67 enodes (cost 16 ) 343.850 * * [simplify]: iteration done : 67 enodes (cost 16 ) 343.851 * * [simplify]: iteration 0 : 9 enodes (cost 10 ) 343.852 * * [simplify]: iteration 1 : 14 enodes (cost 10 ) 343.853 * * [simplify]: iteration 2 : 21 enodes (cost 10 ) 343.855 * * [simplify]: iteration 3 : 26 enodes (cost 10 ) 343.858 * * [simplify]: iteration 4 : 30 enodes (cost 10 ) 343.861 * * [simplify]: iteration done : 30 enodes (cost 10 ) 343.862 * * [simplify]: iteration 0 : 12 enodes (cost 18 ) 343.863 * * [simplify]: iteration 1 : 25 enodes (cost 16 ) 343.867 * * [simplify]: iteration 2 : 61 enodes (cost 14 ) 343.887 * * [simplify]: iteration 3 : 142 enodes (cost 12 ) 343.921 * * [simplify]: iteration 4 : 253 enodes (cost 12 ) 343.970 * * [simplify]: iteration 5 : 323 enodes (cost 12 ) 344.046 * * [simplify]: iteration 6 : 412 enodes (cost 12 ) 344.122 * * [simplify]: iteration 7 : 435 enodes (cost 12 ) 344.201 * * [simplify]: iteration 8 : 451 enodes (cost 12 ) 344.283 * * [simplify]: iteration done : 451 enodes (cost 12 ) 344.284 * * [simplify]: iteration 0 : 11 enodes (cost 14 ) 344.285 * * [simplify]: iteration 1 : 20 enodes (cost 12 ) 344.287 * * [simplify]: iteration 2 : 37 enodes (cost 10 ) 344.293 * * [simplify]: iteration 3 : 78 enodes (cost 8 ) 344.310 * * [simplify]: iteration 4 : 144 enodes (cost 8 ) 344.335 * * [simplify]: iteration 5 : 184 enodes (cost 8 ) 344.354 * * [simplify]: iteration 6 : 208 enodes (cost 8 ) 344.373 * * [simplify]: iteration 7 : 213 enodes (cost 8 ) 344.396 * * [simplify]: iteration 8 : 214 enodes (cost 8 ) 344.414 * * [simplify]: iteration done : 214 enodes (cost 8 ) 344.414 * * [simplify]: iteration 0 : 9 enodes (cost 12 ) 344.416 * * [simplify]: iteration 1 : 18 enodes (cost 8 ) 344.419 * * [simplify]: iteration 2 : 40 enodes (cost 6 ) 344.424 * * [simplify]: iteration 3 : 58 enodes (cost 4 ) 344.429 * * [simplify]: iteration 4 : 73 enodes (cost 4 ) 344.435 * * [simplify]: iteration 5 : 82 enodes (cost 4 ) 344.445 * * [simplify]: iteration 6 : 91 enodes (cost 4 ) 344.454 * * [simplify]: iteration 7 : 105 enodes (cost 4 ) 344.463 * * [simplify]: iteration 8 : 106 enodes (cost 4 ) 344.473 * * [simplify]: iteration done : 106 enodes (cost 4 ) 344.473 * * [simplify]: iteration 0 : 11 enodes (cost 15 ) 344.475 * * [simplify]: iteration 1 : 20 enodes (cost 14 ) 344.477 * * [simplify]: iteration 2 : 38 enodes (cost 14 ) 344.483 * * [simplify]: iteration 3 : 86 enodes (cost 12 ) 344.510 * * [simplify]: iteration 4 : 194 enodes (cost 12 ) 344.553 * * [simplify]: iteration 5 : 282 enodes (cost 12 ) 344.620 * * [simplify]: iteration 6 : 365 enodes (cost 12 ) 344.693 * * [simplify]: iteration 7 : 386 enodes (cost 12 ) 344.773 * * [simplify]: iteration 8 : 393 enodes (cost 12 ) 344.851 * * [simplify]: iteration done : 393 enodes (cost 12 ) 344.852 * * [simplify]: iteration 0 : 10 enodes (cost 11 ) 344.853 * * [simplify]: iteration 1 : 17 enodes (cost 10 ) 344.855 * * [simplify]: iteration 2 : 27 enodes (cost 10 ) 344.858 * * [simplify]: iteration 3 : 51 enodes (cost 8 ) 344.869 * * [simplify]: iteration 4 : 99 enodes (cost 8 ) 344.882 * * [simplify]: iteration 5 : 126 enodes (cost 8 ) 344.902 * * [simplify]: iteration 6 : 148 enodes (cost 8 ) 344.921 * * [simplify]: iteration 7 : 153 enodes (cost 8 ) 344.942 * * [simplify]: iteration 8 : 154 enodes (cost 8 ) 344.963 * * [simplify]: iteration done : 154 enodes (cost 8 ) 344.964 * * [simplify]: iteration 0 : 8 enodes (cost 9 ) 344.965 * * [simplify]: iteration 1 : 15 enodes (cost 6 ) 344.966 * * [simplify]: iteration 2 : 27 enodes (cost 4 ) 344.971 * * [simplify]: iteration 3 : 45 enodes (cost 4 ) 344.976 * * [simplify]: iteration 4 : 56 enodes (cost 4 ) 344.981 * * [simplify]: iteration 5 : 65 enodes (cost 4 ) 344.987 * * [simplify]: iteration 6 : 74 enodes (cost 4 ) 344.997 * * [simplify]: iteration 7 : 88 enodes (cost 4 ) 345.006 * * [simplify]: iteration 8 : 89 enodes (cost 4 ) 345.019 * * [simplify]: iteration done : 89 enodes (cost 4 ) 345.020 * * [simplify]: iteration 0 : 10 enodes (cost 14 ) 345.021 * * [simplify]: iteration 1 : 19 enodes (cost 14 ) 345.023 * * [simplify]: iteration 2 : 36 enodes (cost 12 ) 345.031 * * [simplify]: iteration 3 : 101 enodes (cost 12 ) 345.062 * * [simplify]: iteration 4 : 206 enodes (cost 12 ) 345.111 * * [simplify]: iteration 5 : 281 enodes (cost 12 ) 345.176 * * [simplify]: iteration 6 : 363 enodes (cost 12 ) 345.256 * * [simplify]: iteration 7 : 385 enodes (cost 12 ) 345.337 * * [simplify]: iteration 8 : 392 enodes (cost 12 ) 345.414 * * [simplify]: iteration done : 392 enodes (cost 12 ) 345.415 * * [simplify]: iteration 0 : 9 enodes (cost 10 ) 345.416 * * [simplify]: iteration 1 : 16 enodes (cost 10 ) 345.418 * * [simplify]: iteration 2 : 26 enodes (cost 8 ) 345.422 * * [simplify]: iteration 3 : 61 enodes (cost 8 ) 345.435 * * [simplify]: iteration 4 : 105 enodes (cost 8 ) 345.450 * * [simplify]: iteration 5 : 132 enodes (cost 8 ) 345.471 * * [simplify]: iteration 6 : 154 enodes (cost 8 ) 345.490 * * [simplify]: iteration 7 : 159 enodes (cost 8 ) 345.510 * * [simplify]: iteration 8 : 160 enodes (cost 8 ) 345.531 * * [simplify]: iteration done : 160 enodes (cost 8 ) 345.531 * * [simplify]: iteration 0 : 7 enodes (cost 8 ) 345.532 * * [simplify]: iteration 1 : 14 enodes (cost 6 ) 345.534 * * [simplify]: iteration 2 : 26 enodes (cost 4 ) 345.538 * * [simplify]: iteration 3 : 44 enodes (cost 4 ) 345.543 * * [simplify]: iteration 4 : 55 enodes (cost 4 ) 345.548 * * [simplify]: iteration 5 : 64 enodes (cost 4 ) 345.555 * * [simplify]: iteration 6 : 73 enodes (cost 4 ) 345.563 * * [simplify]: iteration 7 : 87 enodes (cost 4 ) 345.573 * * [simplify]: iteration 8 : 88 enodes (cost 4 ) 345.586 * * [simplify]: iteration done : 88 enodes (cost 4 ) 345.587 * * [simplify]: iteration 0 : 6 enodes (cost 6 ) 345.587 * * [simplify]: iteration 1 : 11 enodes (cost 4 ) 345.589 * * [simplify]: iteration 2 : 21 enodes (cost 4 ) 345.591 * * [simplify]: iteration 3 : 32 enodes (cost 4 ) 345.594 * * [simplify]: iteration 4 : 41 enodes (cost 4 ) 345.597 * * [simplify]: iteration 5 : 47 enodes (cost 4 ) 345.600 * * [simplify]: iteration done : 47 enodes (cost 4 ) 345.600 * * [simplify]: iteration 0 : 6 enodes (cost 6 ) 345.601 * * [simplify]: iteration 1 : 11 enodes (cost 4 ) 345.602 * * [simplify]: iteration 2 : 21 enodes (cost 4 ) 345.605 * * [simplify]: iteration 3 : 32 enodes (cost 4 ) 345.608 * * [simplify]: iteration 4 : 41 enodes (cost 4 ) 345.611 * * [simplify]: iteration 5 : 47 enodes (cost 4 ) 345.614 * * [simplify]: iteration done : 47 enodes (cost 4 ) 345.615 * * [simplify]: iteration 0 : 9 enodes (cost 10 ) 345.616 * * [simplify]: iteration 1 : 16 enodes (cost 10 ) 345.617 * * [simplify]: iteration 2 : 20 enodes (cost 8 ) 345.620 * * [simplify]: iteration 3 : 35 enodes (cost 8 ) 345.624 * * [simplify]: iteration 4 : 38 enodes (cost 8 ) 345.628 * * [simplify]: iteration done : 38 enodes (cost 8 ) 345.628 * * [simplify]: iteration 0 : 9 enodes (cost 10 ) 345.629 * * [simplify]: iteration 1 : 16 enodes (cost 10 ) 345.631 * * [simplify]: iteration 2 : 20 enodes (cost 8 ) 345.634 * * [simplify]: iteration 3 : 35 enodes (cost 8 ) 345.641 * * [simplify]: iteration 4 : 38 enodes (cost 8 ) 345.645 * * [simplify]: iteration done : 38 enodes (cost 8 ) 345.645 * * [simplify]: iteration 0 : 8 enodes (cost 9 ) 345.646 * * [simplify]: iteration 1 : 15 enodes (cost 9 ) 345.648 * * [simplify]: iteration 2 : 25 enodes (cost 7 ) 345.652 * * [simplify]: iteration 3 : 60 enodes (cost 7 ) 345.665 * * [simplify]: iteration 4 : 102 enodes (cost 7 ) 345.679 * * [simplify]: iteration 5 : 129 enodes (cost 7 ) 345.700 * * [simplify]: iteration 6 : 151 enodes (cost 7 ) 345.719 * * [simplify]: iteration 7 : 156 enodes (cost 7 ) 345.738 * * [simplify]: iteration 8 : 157 enodes (cost 7 ) 345.759 * * [simplify]: iteration done : 157 enodes (cost 7 ) 345.760 * * [simplify]: iteration 0 : 10 enodes (cost 11 ) 345.761 * * [simplify]: iteration 1 : 17 enodes (cost 11 ) 345.762 * * [simplify]: iteration 2 : 27 enodes (cost 9 ) 345.767 * * [simplify]: iteration 3 : 62 enodes (cost 9 ) 345.779 * * [simplify]: iteration 4 : 104 enodes (cost 9 ) 345.794 * * [simplify]: iteration 5 : 132 enodes (cost 9 ) 345.817 * * [simplify]: iteration 6 : 154 enodes (cost 9 ) 345.837 * * [simplify]: iteration 7 : 159 enodes (cost 9 ) 345.857 * * [simplify]: iteration 8 : 160 enodes (cost 9 ) 345.880 * * [simplify]: iteration done : 160 enodes (cost 9 ) 345.880 * * [simplify]: iteration 0 : 8 enodes (cost 9 ) 345.881 * * [simplify]: iteration 1 : 15 enodes (cost 9 ) 345.883 * * [simplify]: iteration 2 : 25 enodes (cost 7 ) 345.887 * * [simplify]: iteration 3 : 60 enodes (cost 7 ) 345.899 * * [simplify]: iteration 4 : 102 enodes (cost 7 ) 345.913 * * [simplify]: iteration 5 : 129 enodes (cost 7 ) 345.935 * * [simplify]: iteration 6 : 151 enodes (cost 7 ) 345.954 * * [simplify]: iteration 7 : 156 enodes (cost 7 ) 345.976 * * [simplify]: iteration 8 : 157 enodes (cost 7 ) 345.995 * * [simplify]: iteration done : 157 enodes (cost 7 ) 345.996 * * [simplify]: iteration 0 : 6 enodes (cost 6 ) 345.997 * * [simplify]: iteration 1 : 11 enodes (cost 4 ) 345.998 * * [simplify]: iteration 2 : 21 enodes (cost 4 ) 346.001 * * [simplify]: iteration 3 : 32 enodes (cost 4 ) 346.004 * * [simplify]: iteration 4 : 41 enodes (cost 4 ) 346.007 * * [simplify]: iteration 5 : 47 enodes (cost 4 ) 346.009 * * [simplify]: iteration done : 47 enodes (cost 4 ) 346.010 * * [simplify]: iteration 0 : 11 enodes (cost 13 ) 346.012 * * [simplify]: iteration 1 : 31 enodes (cost 13 ) 346.016 * * [simplify]: iteration 2 : 62 enodes (cost 11 ) 346.027 * * [simplify]: iteration 3 : 179 enodes (cost 11 ) 346.090 * * [simplify]: iteration 4 : 540 enodes (cost 11 ) 346.579 * * [simplify]: iteration 5 : 1955 enodes (cost 11 ) 347.837 * * [simplify]: iteration done : 5001 enodes (cost 11 ) 347.838 * * [simplify]: iteration 0 : 10 enodes (cost 14 ) 347.839 * * [simplify]: iteration 1 : 20 enodes (cost 14 ) 347.842 * * [simplify]: iteration 2 : 42 enodes (cost 12 ) 347.852 * * [simplify]: iteration 3 : 144 enodes (cost 12 ) 347.906 * * [simplify]: iteration 4 : 370 enodes (cost 12 ) 348.081 * * [simplify]: iteration 5 : 756 enodes (cost 12 ) 348.332 * * [simplify]: iteration 6 : 1060 enodes (cost 12 ) 348.817 * * [simplify]: iteration 7 : 1593 enodes (cost 12 ) 351.483 * * [simplify]: iteration 8 : 4751 enodes (cost 12 ) 353.241 * * [simplify]: iteration done : 5000 enodes (cost 12 ) 353.243 * * [simplify]: iteration 0 : 2 enodes (cost 2 ) 353.243 * * [simplify]: iteration 1 : 5 enodes (cost 1 ) 353.243 * * [simplify]: iteration done : 5 enodes (cost 1 ) 353.244 * * [simplify]: iteration 0 : 4 enodes (cost 4 ) 353.244 * * [simplify]: iteration done : 4 enodes (cost 4 ) 353.245 * * [simplify]: iteration 0 : 5 enodes (cost 5 ) 353.245 * * [simplify]: iteration 1 : 7 enodes (cost 4 ) 353.246 * * [simplify]: iteration 2 : 11 enodes (cost 4 ) 353.247 * * [simplify]: iteration 3 : 13 enodes (cost 4 ) 353.248 * * [simplify]: iteration 4 : 19 enodes (cost 4 ) 353.250 * * [simplify]: iteration 5 : 24 enodes (cost 4 ) 353.252 * * [simplify]: iteration done : 24 enodes (cost 4 ) 353.253 * * [simplify]: iteration 0 : 6 enodes (cost 6 ) 353.253 * * [simplify]: iteration 1 : 10 enodes (cost 5 ) 353.254 * * [simplify]: iteration 2 : 11 enodes (cost 4 ) 353.255 * * [simplify]: iteration 3 : 17 enodes (cost 4 ) 353.257 * * [simplify]: iteration 4 : 23 enodes (cost 4 ) 353.259 * * [simplify]: iteration 5 : 28 enodes (cost 4 ) 353.261 * * [simplify]: iteration done : 28 enodes (cost 4 ) 353.261 * * [simplify]: iteration 0 : 5 enodes (cost 5 ) 353.262 * * [simplify]: iteration 1 : 11 enodes (cost 4 ) 353.263 * * [simplify]: iteration 2 : 12 enodes (cost 4 ) 353.264 * * [simplify]: iteration 3 : 16 enodes (cost 4 ) 353.265 * * [simplify]: iteration 4 : 18 enodes (cost 4 ) 353.267 * * [simplify]: iteration 5 : 24 enodes (cost 4 ) 353.269 * * [simplify]: iteration 6 : 29 enodes (cost 4 ) 353.271 * * [simplify]: iteration done : 29 enodes (cost 4 ) 353.272 * * [simplify]: iteration 0 : 5 enodes (cost 5 ) 353.272 * * [simplify]: iteration 1 : 7 enodes (cost 5 ) 353.273 * * [simplify]: iteration done : 7 enodes (cost 5 ) 353.273 * * [simplify]: iteration 0 : 8 enodes (cost 14 ) 353.275 * * [simplify]: iteration 1 : 18 enodes (cost 10 ) 353.276 * * [simplify]: iteration 2 : 30 enodes (cost 6 ) 353.281 * * [simplify]: iteration 3 : 53 enodes (cost 6 ) 353.294 * * [simplify]: iteration 4 : 80 enodes (cost 6 ) 353.305 * * [simplify]: iteration 5 : 106 enodes (cost 6 ) 353.323 * * [simplify]: iteration 6 : 177 enodes (cost 6 ) 353.382 * * [simplify]: iteration 7 : 393 enodes (cost 6 ) 353.793 * * [simplify]: iteration 8 : 1321 enodes (cost 6 ) 358.439 * * [simplify]: iteration done : 5000 enodes (cost 6 ) 358.440 * * [simplify]: iteration 0 : 6 enodes (cost 11 ) 358.440 * * [simplify]: iteration 1 : 8 enodes (cost 11 ) 358.441 * * [simplify]: iteration done : 8 enodes (cost 11 ) 358.442 * * [simplify]: iteration 0 : 5 enodes (cost 5 ) 358.442 * * [simplify]: iteration 1 : 7 enodes (cost 5 ) 358.443 * * [simplify]: iteration done : 7 enodes (cost 5 ) 358.443 * * [simplify]: iteration 0 : 6 enodes (cost 14 ) 358.445 * * [simplify]: iteration 1 : 15 enodes (cost 14 ) 358.447 * * [simplify]: iteration 2 : 31 enodes (cost 6 ) 358.454 * * [simplify]: iteration 3 : 68 enodes (cost 6 ) 358.468 * * [simplify]: iteration 4 : 84 enodes (cost 6 ) 358.479 * * [simplify]: iteration 5 : 114 enodes (cost 6 ) 358.497 * * [simplify]: iteration 6 : 177 enodes (cost 6 ) 358.542 * * [simplify]: iteration 7 : 338 enodes (cost 6 ) 358.709 * * [simplify]: iteration 8 : 826 enodes (cost 6 ) 359.985 * * [simplify]: iteration 9 : 2851 enodes (cost 6 ) 362.801 * * [simplify]: iteration done : 5000 enodes (cost 6 ) 362.801 * * [simplify]: iteration 0 : 5 enodes (cost 5 ) 362.802 * * [simplify]: iteration 1 : 7 enodes (cost 5 ) 362.803 * * [simplify]: iteration done : 7 enodes (cost 5 ) 362.803 * * [simplify]: iteration 0 : 5 enodes (cost 5 ) 362.804 * * [simplify]: iteration 1 : 7 enodes (cost 5 ) 362.804 * * [simplify]: iteration done : 7 enodes (cost 5 ) 362.805 * * [simplify]: iteration 0 : 2 enodes (cost 2 ) 362.805 * * [simplify]: iteration 1 : 5 enodes (cost 1 ) 362.805 * * [simplify]: iteration done : 5 enodes (cost 1 ) 362.806 * * [simplify]: iteration 0 : 3 enodes (cost 3 ) 362.806 * * [simplify]: iteration done : 3 enodes (cost 3 ) 362.807 * * [simplify]: iteration 0 : 8 enodes (cost 13 ) 362.808 * * [simplify]: iteration 1 : 16 enodes (cost 11 ) 362.814 * * [simplify]: iteration 2 : 25 enodes (cost 9 ) 362.818 * * [simplify]: iteration 3 : 31 enodes (cost 9 ) 362.821 * * [simplify]: iteration done : 31 enodes (cost 9 ) 362.821 * * [simplify]: iteration 0 : 6 enodes (cost 6 ) 362.822 * * [simplify]: iteration 1 : 8 enodes (cost 5 ) 362.822 * * [simplify]: iteration done : 8 enodes (cost 5 ) 362.823 * * [simplify]: iteration 0 : 7 enodes (cost 9 ) 362.824 * * [simplify]: iteration 1 : 11 enodes (cost 7 ) 362.825 * * [simplify]: iteration 2 : 13 enodes (cost 5 ) 362.826 * * [simplify]: iteration 3 : 14 enodes (cost 5 ) 362.827 * * [simplify]: iteration done : 14 enodes (cost 5 ) 362.828 * * [simplify]: iteration 0 : 6 enodes (cost 6 ) 362.828 * * [simplify]: iteration 1 : 8 enodes (cost 5 ) 362.829 * * [simplify]: iteration done : 8 enodes (cost 5 ) 362.829 * * [simplify]: iteration 0 : 4 enodes (cost 7 ) 362.830 * * [simplify]: iteration 1 : 8 enodes (cost 3 ) 362.831 * * [simplify]: iteration 2 : 12 enodes (cost 1 ) 362.831 * * [simplify]: iteration done : 12 enodes (cost 1 ) 362.832 * * [simplify]: iteration 0 : 5 enodes (cost 5 ) 362.833 * * [simplify]: iteration 1 : 7 enodes (cost 4 ) 362.833 * * [simplify]: iteration done : 7 enodes (cost 4 ) 362.834 * * [simplify]: iteration 0 : 7 enodes (cost 10 ) 362.834 * * [simplify]: iteration 1 : 11 enodes (cost 9 ) 362.835 * * [simplify]: iteration done : 11 enodes (cost 9 ) 362.836 * * [simplify]: iteration 0 : 6 enodes (cost 6 ) 362.836 * * [simplify]: iteration 1 : 8 enodes (cost 5 ) 362.837 * * [simplify]: iteration done : 8 enodes (cost 5 ) 362.838 * * [simplify]: iteration 0 : 6 enodes (cost 6 ) 362.838 * * [simplify]: iteration 1 : 8 enodes (cost 5 ) 362.839 * * [simplify]: iteration done : 8 enodes (cost 5 ) 362.839 * * [simplify]: iteration 0 : 6 enodes (cost 6 ) 362.840 * * [simplify]: iteration 1 : 8 enodes (cost 5 ) 362.841 * * [simplify]: iteration done : 8 enodes (cost 5 ) 362.841 * * [simplify]: iteration 0 : 3 enodes (cost 4 ) 362.841 * * [simplify]: iteration 1 : 5 enodes (cost 1 ) 362.842 * * [simplify]: iteration done : 5 enodes (cost 1 ) 362.842 * * [simplify]: iteration 0 : 5 enodes (cost 5 ) 362.843 * * [simplify]: iteration 1 : 7 enodes (cost 4 ) 362.843 * * [simplify]: iteration done : 7 enodes (cost 4 ) 362.844 * * [simplify]: iteration 0 : 6 enodes (cost 9 ) 362.844 * * [simplify]: iteration 1 : 10 enodes (cost 9 ) 362.845 * * [simplify]: iteration done : 10 enodes (cost 9 ) 362.846 * * [simplify]: iteration 0 : 5 enodes (cost 5 ) 362.846 * * [simplify]: iteration 1 : 7 enodes (cost 5 ) 362.847 * * [simplify]: iteration done : 7 enodes (cost 5 ) 362.847 * * [simplify]: iteration 0 : 5 enodes (cost 5 ) 362.848 * * [simplify]: iteration 1 : 7 enodes (cost 5 ) 362.848 * * [simplify]: iteration done : 7 enodes (cost 5 ) 362.849 * * [simplify]: iteration 0 : 5 enodes (cost 5 ) 362.850 * * [simplify]: iteration 1 : 7 enodes (cost 5 ) 362.851 * * [simplify]: iteration done : 7 enodes (cost 5 ) 362.851 * * [simplify]: iteration 0 : 2 enodes (cost 3 ) 362.852 * * [simplify]: iteration 1 : 4 enodes (cost 1 ) 362.852 * * [simplify]: iteration done : 4 enodes (cost 1 ) 362.852 * * [simplify]: iteration 0 : 4 enodes (cost 4 ) 362.853 * * [simplify]: iteration 1 : 6 enodes (cost 4 ) 362.853 * * [simplify]: iteration done : 6 enodes (cost 4 ) 362.854 * * [simplify]: iteration 0 : 4 enodes (cost 4 ) 362.854 * * [simplify]: iteration 1 : 6 enodes (cost 4 ) 362.855 * * [simplify]: iteration done : 6 enodes (cost 4 ) 362.855 * * [simplify]: iteration 0 : 4 enodes (cost 4 ) 362.856 * * [simplify]: iteration 1 : 6 enodes (cost 2 ) 362.856 * * [simplify]: iteration 2 : 8 enodes (cost 2 ) 362.857 * * [simplify]: iteration done : 8 enodes (cost 2 ) 362.857 * * [simplify]: iteration 0 : 6 enodes (cost 9 ) 362.858 * * [simplify]: iteration 1 : 10 enodes (cost 9 ) 362.859 * * [simplify]: iteration done : 10 enodes (cost 9 ) 362.859 * * [simplify]: iteration 0 : 5 enodes (cost 5 ) 362.860 * * [simplify]: iteration 1 : 7 enodes (cost 5 ) 362.860 * * [simplify]: iteration done : 7 enodes (cost 5 ) 362.861 * * [simplify]: iteration 0 : 2 enodes (cost 3 ) 362.861 * * [simplify]: iteration 1 : 4 enodes (cost 1 ) 362.862 * * [simplify]: iteration done : 4 enodes (cost 1 ) 362.862 * * [simplify]: iteration 0 : 5 enodes (cost 5 ) 362.863 * * [simplify]: iteration 1 : 7 enodes (cost 4 ) 362.863 * * [simplify]: iteration done : 7 enodes (cost 4 ) 362.864 * * [simplify]: iteration 0 : 5 enodes (cost 5 ) 362.864 * * [simplify]: iteration 1 : 7 enodes (cost 4 ) 362.865 * * [simplify]: iteration done : 7 enodes (cost 4 ) 362.865 * * [simplify]: iteration 0 : 4 enodes (cost 4 ) 362.866 * * [simplify]: iteration 1 : 6 enodes (cost 2 ) 362.866 * * [simplify]: iteration 2 : 8 enodes (cost 2 ) 362.867 * * [simplify]: iteration done : 8 enodes (cost 2 ) 362.867 * * [simplify]: iteration 0 : 3 enodes (cost 3 ) 362.868 * * [simplify]: iteration done : 3 enodes (cost 3 ) 362.868 * * [simplify]: iteration 0 : 3 enodes (cost 3 ) 362.869 * * [simplify]: iteration done : 3 enodes (cost 3 ) 362.869 * * [simplify]: iteration 0 : 4 enodes (cost 7 ) 362.870 * * [simplify]: iteration done : 4 enodes (cost 7 ) 362.870 * * [simplify]: iteration 0 : 3 enodes (cost 3 ) 362.870 * * [simplify]: iteration done : 3 enodes (cost 3 ) 362.871 * * [simplify]: iteration 0 : 4 enodes (cost 8 ) 362.872 * * [simplify]: iteration 1 : 5 enodes (cost 8 ) 362.872 * * [simplify]: iteration 2 : 7 enodes (cost 4 ) 362.873 * * [simplify]: iteration 3 : 12 enodes (cost 4 ) 362.874 * * [simplify]: iteration 4 : 18 enodes (cost 4 ) 362.876 * * [simplify]: iteration 5 : 28 enodes (cost 4 ) 362.880 * * [simplify]: iteration 6 : 49 enodes (cost 4 ) 362.893 * * [simplify]: iteration 7 : 108 enodes (cost 4 ) 362.935 * * [simplify]: iteration 8 : 316 enodes (cost 4 ) 363.391 * * [simplify]: iteration 9 : 1236 enodes (cost 4 ) 365.803 * * [simplify]: iteration done : 5000 enodes (cost 4 ) 365.803 * * [simplify]: iteration 0 : 3 enodes (cost 3 ) 365.804 * * [simplify]: iteration done : 3 enodes (cost 3 ) 365.804 * * [simplify]: iteration 0 : 3 enodes (cost 3 ) 365.805 * * [simplify]: iteration done : 3 enodes (cost 3 ) 365.805 * * [simplify]: iteration 0 : 15 enodes (cost 17 ) 365.807 * * [simplify]: iteration 1 : 35 enodes (cost 17 ) 365.820 * * [simplify]: iteration 2 : 92 enodes (cost 17 ) 365.834 * * [simplify]: iteration 3 : 193 enodes (cost 17 ) 365.894 * * [simplify]: iteration 4 : 496 enodes (cost 17 ) 366.192 * * [simplify]: iteration 5 : 1268 enodes (cost 17 ) 367.814 * * [simplify]: iteration 6 : 3919 enodes (cost 17 ) 369.787 * * [simplify]: iteration done : 5001 enodes (cost 17 ) 369.788 * * [simplify]: iteration 0 : 4 enodes (cost 4 ) 369.788 * * [simplify]: iteration 1 : 6 enodes (cost 4 ) 369.789 * * [simplify]: iteration 2 : 7 enodes (cost 4 ) 369.790 * * [simplify]: iteration done : 7 enodes (cost 4 ) 369.790 * * [simplify]: iteration 0 : 4 enodes (cost 4 ) 369.791 * * [simplify]: iteration 1 : 6 enodes (cost 4 ) 369.791 * * [simplify]: iteration 2 : 7 enodes (cost 4 ) 369.792 * * [simplify]: iteration done : 7 enodes (cost 4 ) 369.793 * * [simplify]: iteration 0 : 13 enodes (cost 15 ) 369.795 * * [simplify]: iteration 1 : 32 enodes (cost 15 ) 369.799 * * [simplify]: iteration 2 : 66 enodes (cost 15 ) 369.810 * * [simplify]: iteration 3 : 114 enodes (cost 15 ) 369.835 * * [simplify]: iteration 4 : 209 enodes (cost 15 ) 369.901 * * [simplify]: iteration 5 : 504 enodes (cost 15 ) 370.318 * * [simplify]: iteration 6 : 1563 enodes (cost 15 ) 371.965 * * [simplify]: iteration done : 5000 enodes (cost 15 ) 371.966 * * [simplify]: iteration 0 : 6 enodes (cost 7 ) 371.966 * * [simplify]: iteration 1 : 11 enodes (cost 7 ) 371.968 * * [simplify]: iteration 2 : 14 enodes (cost 7 ) 371.969 * * [simplify]: iteration 3 : 16 enodes (cost 7 ) 371.971 * * [simplify]: iteration done : 16 enodes (cost 7 ) 371.972 * * [simplify]: iteration 0 : 6 enodes (cost 7 ) 371.973 * * [simplify]: iteration 1 : 11 enodes (cost 7 ) 371.974 * * [simplify]: iteration 2 : 14 enodes (cost 7 ) 371.976 * * [simplify]: iteration 3 : 16 enodes (cost 7 ) 371.978 * * [simplify]: iteration done : 16 enodes (cost 7 ) 371.979 * * [simplify]: iteration 0 : 11 enodes (cost 13 ) 371.980 * * [simplify]: iteration 1 : 27 enodes (cost 13 ) 371.984 * * [simplify]: iteration 2 : 51 enodes (cost 13 ) 371.992 * * [simplify]: iteration 3 : 78 enodes (cost 13 ) 372.005 * * [simplify]: iteration 4 : 129 enodes (cost 13 ) 372.045 * * [simplify]: iteration 5 : 277 enodes (cost 13 ) 372.254 * * [simplify]: iteration 6 : 807 enodes (cost 13 ) 374.332 * * [simplify]: iteration 7 : 3108 enodes (cost 13 ) 378.138 * * [simplify]: iteration done : 5000 enodes (cost 13 ) 378.138 * * [simplify]: iteration 0 : 4 enodes (cost 4 ) 378.139 * * [simplify]: iteration 1 : 6 enodes (cost 4 ) 378.139 * * [simplify]: iteration done : 6 enodes (cost 4 ) 378.140 * * [simplify]: iteration 0 : 4 enodes (cost 4 ) 378.140 * * [simplify]: iteration 1 : 6 enodes (cost 4 ) 378.141 * * [simplify]: iteration done : 6 enodes (cost 4 ) 378.142 * * [simplify]: iteration 0 : 11 enodes (cost 13 ) 378.143 * * [simplify]: iteration 1 : 30 enodes (cost 13 ) 378.147 * * [simplify]: iteration 2 : 72 enodes (cost 13 ) 378.160 * * [simplify]: iteration 3 : 158 enodes (cost 13 ) 378.210 * * [simplify]: iteration 4 : 345 enodes (cost 13 ) 378.367 * * [simplify]: iteration 5 : 852 enodes (cost 13 ) 379.423 * * [simplify]: iteration 6 : 2834 enodes (cost 13 ) 381.648 * * [simplify]: iteration done : 5001 enodes (cost 13 ) 381.649 * * [simplify]: iteration 0 : 2 enodes (cost 2 ) 381.649 * * [simplify]: iteration done : 2 enodes (cost 2 ) 381.650 * * [simplify]: iteration 0 : 2 enodes (cost 2 ) 381.650 * * [simplify]: iteration done : 2 enodes (cost 2 ) 381.651 * [simplify]: Simplified to: (exp (- 1.0 (cos x))) (log (- 1.0 (cos x))) (exp (- 1.0 (cos x))) (* (cbrt (- 1.0 (cos x))) (cbrt (- 1.0 (cos x)))) (cbrt (- 1.0 (cos x))) (pow (- 1.0 (cos x)) 3) (sqrt (- 1.0 (cos x))) (sqrt (- 1.0 (cos x))) (- (pow 1.0 3) (pow (cos x) 3)) (+ (* 1.0 1.0) (* (cos x) (+ (cos x) 1.0))) (neg (cos x)) (- (* 1.0 1.0) (* (cos x) (cos x))) (+ 1.0 (cos x)) (+ (sqrt 1.0) (sqrt (cos x))) (- (sqrt 1.0) (sqrt (cos x))) (- 1.0 (cos x)) (neg (cos x)) (/ (- 1.0 (cos x)) (sin x)) (- (log (- 1.0 (cos x))) (log (sin x))) (- (log (- 1.0 (cos x))) (log (sin x))) (- (log (- 1.0 (cos x))) (log (sin x))) (- (log (- 1.0 (cos x))) (log (sin x))) (log (/ (- 1.0 (cos x)) (sin x))) (exp (/ (- 1.0 (cos x)) (sin x))) (pow (/ (- 1.0 (cos x)) (sin x)) 3) (pow (/ (- 1.0 (cos x)) (sin x)) 3) (* (cbrt (/ (- 1.0 (cos x)) (sin x))) (cbrt (/ (- 1.0 (cos x)) (sin x)))) (cbrt (/ (- 1.0 (cos x)) (sin x))) (pow (/ (- 1.0 (cos x)) (sin x)) 3) (sqrt (/ (- 1.0 (cos x)) (sin x))) (sqrt (/ (- 1.0 (cos x)) (sin x))) (- (pow 1.0 3) (pow (cos x) 3)) (* (sin x) (+ (* 1.0 1.0) (* (cos x) (+ (cos x) 1.0)))) (- (* 1.0 1.0) (* (cos x) (cos x))) (* (+ 1.0 (cos x)) (sin x)) (* (sqrt (- 1.0 (cos x))) (sqrt (/ 1 (sin x)))) (* (sqrt (- 1.0 (cos x))) (sqrt (/ 1 (sin x)))) (/ (sqrt (- 1.0 (cos x))) (sqrt (sin x))) (/ (sqrt (- 1.0 (cos x))) (sqrt (sin x))) (/ (sqrt (- 1.0 (cos x))) (sqrt (sin x))) (/ (sqrt (- 1.0 (cos x))) (sqrt (sin x))) (* (- 1.0 (cos x)) (* (cbrt (/ 1 (sin x))) (cbrt (/ 1 (sin x))))) (* (- 1.0 (cos x)) (sqrt (/ 1 (sin x)))) (/ (- 1.0 (cos x)) (* (cbrt (sin x)) (cbrt (sin x)))) (/ (- 1.0 (cos x)) (sqrt (sin x))) (- 1.0 (cos x)) (/ (/ (- 1.0 (cos x)) (cbrt (sin x))) (cbrt (sin x))) (/ (- 1.0 (cos x)) (sqrt (sin x))) (- 1.0 (cos x)) (/ (- 1.0 (cos x)) (* (cbrt (sin x)) (cbrt (sin x)))) (/ (- 1.0 (cos x)) (sqrt (sin x))) (- 1.0 (cos x)) (- 1.0 (cos x)) (- 1.0 (cos x)) (/ (cbrt (- 1.0 (cos x))) (sin x)) (/ (sqrt (- 1.0 (cos x))) (sin x)) (/ (- 1.0 (cos x)) (sin x)) (/ (- (sqrt 1.0) (sqrt (cos x))) (sin x)) (/ (- 1.0 (cos x)) (sin x)) (- 1.0 (cos x)) (/ (- (pow 1.0 3) (pow (cos x) 3)) (sin x)) (* (+ 1.0 (cos x)) (/ (- 1.0 (cos x)) (sin x))) -1 (neg (log (sin x))) (neg (log (sin x))) (neg (log (sin x))) (neg (log (sin x))) (exp (/ 1 (sin x))) (/ 1 (pow (sin x) 3)) (* (cbrt (/ 1 (sin x))) (cbrt (/ 1 (sin x)))) (cbrt (/ 1 (sin x))) (pow (/ 1 (sin x)) 3) (sqrt (/ 1 (sin x))) (sqrt (/ 1 (sin x))) -1 (neg (sin x)) (/ 1 (* (cbrt (sin x)) (cbrt (sin x)))) (/ 1 (cbrt (sin x))) (/ 1 (sqrt (sin x))) (/ 1 (sqrt (sin x))) 1 (/ 1 (sin x)) (/ 1 (* (cbrt (sin x)) (cbrt (sin x)))) (/ 1 (cbrt (sin x))) (/ 1 (sqrt (sin x))) (/ 1 (sqrt (sin x))) 1 (/ 1 (sin x)) (/ 1 (* (cbrt (sin x)) (cbrt (sin x)))) (/ 1 (cbrt (sin x))) (/ 1 (sqrt (sin x))) (/ 1 (sqrt (sin x))) 1 (/ 1 (sin x)) (/ 1 (sin x)) (sin x) (/ 1 (* (cbrt (sin x)) (cbrt (sin x)))) (/ 1 (sqrt (sin x))) 1 (/ (sin x) 1) (/ (sin x) 1) (sin x) (log (sin x)) (exp (sin x)) (* (cbrt (sin x)) (cbrt (sin x))) (cbrt (sin x)) (pow (sin x) 3) (sqrt (sin x)) (sqrt (sin x)) (- (+ (* 1/2 (pow x 2)) (* 1/720 (pow x 6))) (* 1/24 (pow x 4))) (- 1.0 (cos x)) (- 1.0 (cos x)) (+ (* 1/2 x) (+ (* 1/24 (pow x 3)) (* 1/240 (pow x 5)))) (/ (- 1.0 (cos x)) (sin x)) (/ (- 1.0 (cos x)) (sin x)) (+ (* 1/6 x) (+ (/ 1 x) (* 7/360 (pow x 3)))) (/ 1 (sin x)) (/ 1 (sin x)) (- (+ x (* 1/120 (pow x 5))) (* 1/6 (pow x 3))) (sin x) (sin x) 381.652 * * * [progress]: adding candidates to table 381.749 * * [progress]: iteration 4 / 4 381.749 * * * [progress]: picking best candidate 381.786 * * * * [pick]: Picked # 381.786 * * * [progress]: localizing error 381.802 * * * [progress]: generating rewritten candidates 381.802 * * * * [progress]: [ 1 / 4 ] rewriting at (2 1 1) 381.815 * * * * [progress]: [ 2 / 4 ] rewriting at (2 1 2 2 2) 381.820 * * * * [progress]: [ 3 / 4 ] rewriting at (2 1 1 2) 381.822 * * * * [progress]: [ 4 / 4 ] rewriting at (2 1 2 2) 381.837 * * * [progress]: generating series expansions 381.837 * * * * [progress]: [ 1 / 4 ] generating series at (2 1 1) 381.837 * [approximate]: Taking taylor expansion of (- 1.0 (pow (cos x) 3)) in (x) around 0 381.837 * [taylor]: Taking taylor expansion of (- 1.0 (pow (cos x) 3)) in x 381.837 * [taylor]: Taking taylor expansion of 1.0 in x 381.837 * [taylor]: Taking taylor expansion of (pow (cos x) 3) in x 381.837 * [taylor]: Taking taylor expansion of (cos x) in x 381.837 * [taylor]: Taking taylor expansion of x in x 381.837 * [taylor]: Taking taylor expansion of (- 1.0 (pow (cos x) 3)) in x 381.837 * [taylor]: Taking taylor expansion of 1.0 in x 381.837 * [taylor]: Taking taylor expansion of (pow (cos x) 3) in x 381.837 * [taylor]: Taking taylor expansion of (cos x) in x 381.837 * [taylor]: Taking taylor expansion of x in x 381.840 * [approximate]: Taking taylor expansion of (- 1.0 (pow (cos (/ 1 x)) 3)) in (x) around 0 381.840 * [taylor]: Taking taylor expansion of (- 1.0 (pow (cos (/ 1 x)) 3)) in x 381.840 * [taylor]: Taking taylor expansion of 1.0 in x 381.840 * [taylor]: Taking taylor expansion of (pow (cos (/ 1 x)) 3) in x 381.840 * [taylor]: Taking taylor expansion of (cos (/ 1 x)) in x 381.840 * [taylor]: Taking taylor expansion of (/ 1 x) in x 381.840 * [taylor]: Taking taylor expansion of x in x 381.840 * [taylor]: Taking taylor expansion of (- 1.0 (pow (cos (/ 1 x)) 3)) in x 381.840 * [taylor]: Taking taylor expansion of 1.0 in x 381.840 * [taylor]: Taking taylor expansion of (pow (cos (/ 1 x)) 3) in x 381.840 * [taylor]: Taking taylor expansion of (cos (/ 1 x)) in x 381.840 * [taylor]: Taking taylor expansion of (/ 1 x) in x 381.840 * [taylor]: Taking taylor expansion of x in x 381.843 * [approximate]: Taking taylor expansion of (- 1.0 (pow (cos (/ -1 x)) 3)) in (x) around 0 381.843 * [taylor]: Taking taylor expansion of (- 1.0 (pow (cos (/ -1 x)) 3)) in x 381.843 * [taylor]: Taking taylor expansion of 1.0 in x 381.843 * [taylor]: Taking taylor expansion of (pow (cos (/ -1 x)) 3) in x 381.843 * [taylor]: Taking taylor expansion of (cos (/ -1 x)) in x 381.843 * [taylor]: Taking taylor expansion of (/ -1 x) in x 381.843 * [taylor]: Taking taylor expansion of -1 in x 381.843 * [taylor]: Taking taylor expansion of x in x 381.843 * [taylor]: Taking taylor expansion of (- 1.0 (pow (cos (/ -1 x)) 3)) in x 381.843 * [taylor]: Taking taylor expansion of 1.0 in x 381.843 * [taylor]: Taking taylor expansion of (pow (cos (/ -1 x)) 3) in x 381.843 * [taylor]: Taking taylor expansion of (cos (/ -1 x)) in x 381.843 * [taylor]: Taking taylor expansion of (/ -1 x) in x 381.843 * [taylor]: Taking taylor expansion of -1 in x 381.843 * [taylor]: Taking taylor expansion of x in x 381.845 * * * * [progress]: [ 2 / 4 ] generating series at (2 1 2 2 2) 381.845 * [approximate]: Taking taylor expansion of (+ (cos x) 1.0) in (x) around 0 381.846 * [taylor]: Taking taylor expansion of (+ (cos x) 1.0) in x 381.846 * [taylor]: Taking taylor expansion of (cos x) in x 381.846 * [taylor]: Taking taylor expansion of x in x 381.846 * [taylor]: Taking taylor expansion of 1.0 in x 381.846 * [taylor]: Taking taylor expansion of (+ (cos x) 1.0) in x 381.846 * [taylor]: Taking taylor expansion of (cos x) in x 381.846 * [taylor]: Taking taylor expansion of x in x 381.846 * [taylor]: Taking taylor expansion of 1.0 in x 381.846 * [approximate]: Taking taylor expansion of (+ (cos (/ 1 x)) 1.0) in (x) around 0 381.846 * [taylor]: Taking taylor expansion of (+ (cos (/ 1 x)) 1.0) in x 381.846 * [taylor]: Taking taylor expansion of (cos (/ 1 x)) in x 381.847 * [taylor]: Taking taylor expansion of (/ 1 x) in x 381.847 * [taylor]: Taking taylor expansion of x in x 381.847 * [taylor]: Taking taylor expansion of 1.0 in x 381.847 * [taylor]: Taking taylor expansion of (+ (cos (/ 1 x)) 1.0) in x 381.847 * [taylor]: Taking taylor expansion of (cos (/ 1 x)) in x 381.847 * [taylor]: Taking taylor expansion of (/ 1 x) in x 381.847 * [taylor]: Taking taylor expansion of x in x 381.847 * [taylor]: Taking taylor expansion of 1.0 in x 381.847 * [approximate]: Taking taylor expansion of (+ (cos (/ -1 x)) 1.0) in (x) around 0 381.847 * [taylor]: Taking taylor expansion of (+ (cos (/ -1 x)) 1.0) in x 381.847 * [taylor]: Taking taylor expansion of (cos (/ -1 x)) in x 381.847 * [taylor]: Taking taylor expansion of (/ -1 x) in x 381.847 * [taylor]: Taking taylor expansion of -1 in x 381.847 * [taylor]: Taking taylor expansion of x in x 381.847 * [taylor]: Taking taylor expansion of 1.0 in x 381.847 * [taylor]: Taking taylor expansion of (+ (cos (/ -1 x)) 1.0) in x 381.847 * [taylor]: Taking taylor expansion of (cos (/ -1 x)) in x 381.847 * [taylor]: Taking taylor expansion of (/ -1 x) in x 381.847 * [taylor]: Taking taylor expansion of -1 in x 381.847 * [taylor]: Taking taylor expansion of x in x 381.847 * [taylor]: Taking taylor expansion of 1.0 in x 381.848 * * * * [progress]: [ 3 / 4 ] generating series at (2 1 1 2) 381.848 * [approximate]: Taking taylor expansion of (pow (cos x) 3) in (x) around 0 381.848 * [taylor]: Taking taylor expansion of (pow (cos x) 3) in x 381.848 * [taylor]: Taking taylor expansion of (cos x) in x 381.848 * [taylor]: Taking taylor expansion of x in x 381.848 * [taylor]: Taking taylor expansion of (pow (cos x) 3) in x 381.848 * [taylor]: Taking taylor expansion of (cos x) in x 381.848 * [taylor]: Taking taylor expansion of x in x 381.849 * [approximate]: Taking taylor expansion of (pow (cos (/ 1 x)) 3) in (x) around 0 381.849 * [taylor]: Taking taylor expansion of (pow (cos (/ 1 x)) 3) in x 381.849 * [taylor]: Taking taylor expansion of (cos (/ 1 x)) in x 381.849 * [taylor]: Taking taylor expansion of (/ 1 x) in x 381.849 * [taylor]: Taking taylor expansion of x in x 381.849 * [taylor]: Taking taylor expansion of (pow (cos (/ 1 x)) 3) in x 381.849 * [taylor]: Taking taylor expansion of (cos (/ 1 x)) in x 381.849 * [taylor]: Taking taylor expansion of (/ 1 x) in x 381.849 * [taylor]: Taking taylor expansion of x in x 381.851 * [approximate]: Taking taylor expansion of (pow (cos (/ -1 x)) 3) in (x) around 0 381.851 * [taylor]: Taking taylor expansion of (pow (cos (/ -1 x)) 3) in x 381.851 * [taylor]: Taking taylor expansion of (cos (/ -1 x)) in x 381.851 * [taylor]: Taking taylor expansion of (/ -1 x) in x 381.851 * [taylor]: Taking taylor expansion of -1 in x 381.851 * [taylor]: Taking taylor expansion of x in x 381.851 * [taylor]: Taking taylor expansion of (pow (cos (/ -1 x)) 3) in x 381.851 * [taylor]: Taking taylor expansion of (cos (/ -1 x)) in x 381.851 * [taylor]: Taking taylor expansion of (/ -1 x) in x 381.851 * [taylor]: Taking taylor expansion of -1 in x 381.851 * [taylor]: Taking taylor expansion of x in x 381.854 * * * * [progress]: [ 4 / 4 ] generating series at (2 1 2 2) 381.854 * [approximate]: Taking taylor expansion of (* (cos x) (+ (cos x) 1.0)) in (x) around 0 381.854 * [taylor]: Taking taylor expansion of (* (cos x) (+ (cos x) 1.0)) in x 381.854 * [taylor]: Taking taylor expansion of (cos x) in x 381.854 * [taylor]: Taking taylor expansion of x in x 381.854 * [taylor]: Taking taylor expansion of (+ (cos x) 1.0) in x 381.854 * [taylor]: Taking taylor expansion of (cos x) in x 381.854 * [taylor]: Taking taylor expansion of x in x 381.854 * [taylor]: Taking taylor expansion of 1.0 in x 381.854 * [taylor]: Taking taylor expansion of (* (cos x) (+ (cos x) 1.0)) in x 381.854 * [taylor]: Taking taylor expansion of (cos x) in x 381.854 * [taylor]: Taking taylor expansion of x in x 381.854 * [taylor]: Taking taylor expansion of (+ (cos x) 1.0) in x 381.854 * [taylor]: Taking taylor expansion of (cos x) in x 381.854 * [taylor]: Taking taylor expansion of x in x 381.854 * [taylor]: Taking taylor expansion of 1.0 in x 381.855 * [approximate]: Taking taylor expansion of (* (cos (/ 1 x)) (+ (cos (/ 1 x)) 1.0)) in (x) around 0 381.855 * [taylor]: Taking taylor expansion of (* (cos (/ 1 x)) (+ (cos (/ 1 x)) 1.0)) in x 381.856 * [taylor]: Taking taylor expansion of (cos (/ 1 x)) in x 381.856 * [taylor]: Taking taylor expansion of (/ 1 x) in x 381.856 * [taylor]: Taking taylor expansion of x in x 381.856 * [taylor]: Taking taylor expansion of (+ (cos (/ 1 x)) 1.0) in x 381.856 * [taylor]: Taking taylor expansion of (cos (/ 1 x)) in x 381.856 * [taylor]: Taking taylor expansion of (/ 1 x) in x 381.856 * [taylor]: Taking taylor expansion of x in x 381.856 * [taylor]: Taking taylor expansion of 1.0 in x 381.856 * [taylor]: Taking taylor expansion of (* (cos (/ 1 x)) (+ (cos (/ 1 x)) 1.0)) in x 381.856 * [taylor]: Taking taylor expansion of (cos (/ 1 x)) in x 381.856 * [taylor]: Taking taylor expansion of (/ 1 x) in x 381.856 * [taylor]: Taking taylor expansion of x in x 381.856 * [taylor]: Taking taylor expansion of (+ (cos (/ 1 x)) 1.0) in x 381.856 * [taylor]: Taking taylor expansion of (cos (/ 1 x)) in x 381.856 * [taylor]: Taking taylor expansion of (/ 1 x) in x 381.856 * [taylor]: Taking taylor expansion of x in x 381.856 * [taylor]: Taking taylor expansion of 1.0 in x 381.857 * [approximate]: Taking taylor expansion of (* (+ (cos (/ -1 x)) 1.0) (cos (/ -1 x))) in (x) around 0 381.857 * [taylor]: Taking taylor expansion of (* (+ (cos (/ -1 x)) 1.0) (cos (/ -1 x))) in x 381.857 * [taylor]: Taking taylor expansion of (+ (cos (/ -1 x)) 1.0) in x 381.857 * [taylor]: Taking taylor expansion of (cos (/ -1 x)) in x 381.857 * [taylor]: Taking taylor expansion of (/ -1 x) in x 381.857 * [taylor]: Taking taylor expansion of -1 in x 381.857 * [taylor]: Taking taylor expansion of x in x 381.857 * [taylor]: Taking taylor expansion of 1.0 in x 381.857 * [taylor]: Taking taylor expansion of (cos (/ -1 x)) in x 381.857 * [taylor]: Taking taylor expansion of (/ -1 x) in x 381.857 * [taylor]: Taking taylor expansion of -1 in x 381.857 * [taylor]: Taking taylor expansion of x in x 381.857 * [taylor]: Taking taylor expansion of (* (+ (cos (/ -1 x)) 1.0) (cos (/ -1 x))) in x 381.857 * [taylor]: Taking taylor expansion of (+ (cos (/ -1 x)) 1.0) in x 381.857 * [taylor]: Taking taylor expansion of (cos (/ -1 x)) in x 381.857 * [taylor]: Taking taylor expansion of (/ -1 x) in x 381.857 * [taylor]: Taking taylor expansion of -1 in x 381.857 * [taylor]: Taking taylor expansion of x in x 381.858 * [taylor]: Taking taylor expansion of 1.0 in x 381.858 * [taylor]: Taking taylor expansion of (cos (/ -1 x)) in x 381.858 * [taylor]: Taking taylor expansion of (/ -1 x) in x 381.858 * [taylor]: Taking taylor expansion of -1 in x 381.858 * [taylor]: Taking taylor expansion of x in x 381.859 * * * [progress]: simplifying candidates 381.860 * [simplify]: Simplifying using # : (/ (exp (pow 1.0 3)) (exp (pow (cos x) 3))) (log (- (pow 1.0 3) (pow (cos x) 3))) (exp (- (pow 1.0 3) (pow (cos x) 3))) (* (cbrt (- (pow 1.0 3) (pow (cos x) 3))) (cbrt (- (pow 1.0 3) (pow (cos x) 3)))) (cbrt (- (pow 1.0 3) (pow (cos x) 3))) (* (* (- (pow 1.0 3) (pow (cos x) 3)) (- (pow 1.0 3) (pow (cos x) 3))) (- (pow 1.0 3) (pow (cos x) 3))) (sqrt (- (pow 1.0 3) (pow (cos x) 3))) (sqrt (- (pow 1.0 3) (pow (cos x) 3))) (+ (* 1.0 1.0) (+ (* (cos x) (cos x)) (* 1.0 (cos x)))) (- 1.0 (cos x)) (- (pow (pow 1.0 3) 3) (pow (pow (cos x) 3) 3)) (+ (* (pow 1.0 3) (pow 1.0 3)) (+ (* (pow (cos x) 3) (pow (cos x) 3)) (* (pow 1.0 3) (pow (cos x) 3)))) (neg (pow (cos x) 3)) (- (* (pow 1.0 3) (pow 1.0 3)) (* (pow (cos x) 3) (pow (cos x) 3))) (+ (pow 1.0 3) (pow (cos x) 3)) (+ (pow (sqrt 1.0) 3) (pow (sqrt (cos x)) 3)) (- (pow (sqrt 1.0) 3) (pow (sqrt (cos x)) 3)) (+ (pow (sqrt 1.0) 3) (pow (sqrt (cos x)) 3)) (- (pow (sqrt 1.0) 3) (pow (sqrt (cos x)) 3)) (+ (pow (sqrt 1.0) 3) (sqrt (pow (cos x) 3))) (- (pow (sqrt 1.0) 3) (sqrt (pow (cos x) 3))) (+ (pow (sqrt 1.0) 3) (pow (cos x) (/ 3 2))) (- (pow (sqrt 1.0) 3) (pow (cos x) (/ 3 2))) (+ (pow (sqrt 1.0) 3) (pow (sqrt (cos x)) 3)) (- (pow (sqrt 1.0) 3) (pow (sqrt (cos x)) 3)) (+ (pow (sqrt 1.0) 3) (pow (sqrt (cos x)) 3)) (- (pow (sqrt 1.0) 3) (pow (sqrt (cos x)) 3)) (+ (pow (sqrt 1.0) 3) (sqrt (pow (cos x) 3))) (- (pow (sqrt 1.0) 3) (sqrt (pow (cos x) 3))) (+ (pow (sqrt 1.0) 3) (pow (cos x) (/ 3 2))) (- (pow (sqrt 1.0) 3) (pow (cos x) (/ 3 2))) (+ (sqrt (pow 1.0 3)) (pow (sqrt (cos x)) 3)) (- (sqrt (pow 1.0 3)) (pow (sqrt (cos x)) 3)) (+ (sqrt (pow 1.0 3)) (pow (sqrt (cos x)) 3)) (- (sqrt (pow 1.0 3)) (pow (sqrt (cos x)) 3)) (+ (sqrt (pow 1.0 3)) (sqrt (pow (cos x) 3))) (- (sqrt (pow 1.0 3)) (sqrt (pow (cos x) 3))) (+ (sqrt (pow 1.0 3)) (pow (cos x) (/ 3 2))) (- (sqrt (pow 1.0 3)) (pow (cos x) (/ 3 2))) (+ (pow 1.0 (/ 3 2)) (pow (sqrt (cos x)) 3)) (- (pow 1.0 (/ 3 2)) (pow (sqrt (cos x)) 3)) (+ (pow 1.0 (/ 3 2)) (pow (sqrt (cos x)) 3)) (- (pow 1.0 (/ 3 2)) (pow (sqrt (cos x)) 3)) (+ (pow 1.0 (/ 3 2)) (sqrt (pow (cos x) 3))) (- (pow 1.0 (/ 3 2)) (sqrt (pow (cos x) 3))) (+ (pow 1.0 (/ 3 2)) (pow (cos x) (/ 3 2))) (- (pow 1.0 (/ 3 2)) (pow (cos x) (/ 3 2))) (- (pow 1.0 3) (pow (cos x) 3)) (- (pow 1.0 3) (pow (cos x) 3)) (- (pow 1.0 3) (pow (cos x) 3)) (- (pow 1.0 3) (pow (cos x) 3)) (- (pow 1.0 3) (pow (cos x) 3)) (neg (pow (cos x) 3)) (* (exp (cos x)) (exp 1.0)) (log (+ (cos x) 1.0)) (exp (+ (cos x) 1.0)) (* (cbrt (+ (cos x) 1.0)) (cbrt (+ (cos x) 1.0))) (cbrt (+ (cos x) 1.0)) (* (* (+ (cos x) 1.0) (+ (cos x) 1.0)) (+ (cos x) 1.0)) (sqrt (+ (cos x) 1.0)) (sqrt (+ (cos x) 1.0)) (+ (pow (cos x) 3) (pow 1.0 3)) (+ (* (cos x) (cos x)) (- (* 1.0 1.0) (* (cos x) 1.0))) (- (* (cos x) (cos x)) (* 1.0 1.0)) (- (cos x) 1.0) (+ (cos x) 1.0) (* (log (cos x)) 3) (* (log (cos x)) 3) (* 1 3) (pow (cos x) (* (cbrt 3) (cbrt 3))) (pow (cos x) (sqrt 3)) (pow (cos x) 1) (pow (* (cbrt (cos x)) (cbrt (cos x))) 3) (pow (cbrt (cos x)) 3) (pow (sqrt (cos x)) 3) (pow (sqrt (cos x)) 3) (pow 1 3) (pow (cos x) 3) (* (cos x) (cos x)) (log (pow (cos x) 3)) (exp (pow (cos x) 3)) (* (cbrt (pow (cos x) 3)) (cbrt (pow (cos x) 3))) (cbrt (pow (cos x) 3)) (* (* (pow (cos x) 3) (pow (cos x) 3)) (pow (cos x) 3)) (pow (* (cbrt (cos x)) (cbrt (cos x))) 3) (pow (cbrt (cos x)) 3) (pow (sqrt (cos x)) 3) (pow (sqrt (cos x)) 3) (pow 1 3) (pow (cos x) 3) (* (cos x) (cos x)) (sqrt (pow (cos x) 3)) (sqrt (pow (cos x) 3)) (pow (cos x) (/ 3 2)) (pow (cos x) (/ 3 2)) (* (cos x) (+ (cos x) 1.0)) (+ (log (cos x)) (log (+ (cos x) 1.0))) (log (* (cos x) (+ (cos x) 1.0))) (exp (* (cos x) (+ (cos x) 1.0))) (* (* (* (cos x) (cos x)) (cos x)) (* (* (+ (cos x) 1.0) (+ (cos x) 1.0)) (+ (cos x) 1.0))) (* (cbrt (* (cos x) (+ (cos x) 1.0))) (cbrt (* (cos x) (+ (cos x) 1.0)))) (cbrt (* (cos x) (+ (cos x) 1.0))) (* (* (* (cos x) (+ (cos x) 1.0)) (* (cos x) (+ (cos x) 1.0))) (* (cos x) (+ (cos x) 1.0))) (sqrt (* (cos x) (+ (cos x) 1.0))) (sqrt (* (cos x) (+ (cos x) 1.0))) (* (sqrt (cos x)) (sqrt (+ (cos x) 1.0))) (* (sqrt (cos x)) (sqrt (+ (cos x) 1.0))) (* (cos x) (cos x)) (* (cos x) 1.0) (* (cos x) (cos x)) (* 1.0 (cos x)) (* (cos x) (* (cbrt (+ (cos x) 1.0)) (cbrt (+ (cos x) 1.0)))) (* (cos x) (sqrt (+ (cos x) 1.0))) (* (cos x) 1) (* (cos x) 1) (* (cbrt (cos x)) (+ (cos x) 1.0)) (* (sqrt (cos x)) (+ (cos x) 1.0)) (* (cos x) (+ (cos x) 1.0)) (* (cos x) (+ (pow (cos x) 3) (pow 1.0 3))) (* (cos x) (- (* (cos x) (cos x)) (* 1.0 1.0))) (- (+ (* 3/2 (pow x 2)) (* 61/240 (pow x 6))) (* 7/8 (pow x 4))) (- 1.0 (pow (cos x) 3)) (- 1.0 (pow (cos x) 3)) (- (+ 2.0 (* 1/24 (pow x 4))) (* 1/2 (pow x 2))) (+ (cos x) 1.0) (+ (cos x) 1.0) (- (+ 1 (* 7/8 (pow x 4))) (* 3/2 (pow x 2))) (pow (cos x) 3) (pow (cos x) 3) (- (+ 2.0 (* 0.375 (pow x 4))) (* 1.5 (pow x 2))) (* (cos x) (+ (cos x) 1.0)) (* (cos x) (+ (cos x) 1.0)) 381.861 * * [simplify]: iteration 0 : 9 enodes (cost 10 ) 381.862 * * [simplify]: iteration 1 : 24 enodes (cost 9 ) 381.865 * * [simplify]: iteration 2 : 50 enodes (cost 9 ) 381.872 * * [simplify]: iteration 3 : 111 enodes (cost 9 ) 381.891 * * [simplify]: iteration 4 : 306 enodes (cost 9 ) 381.980 * * [simplify]: iteration 5 : 1069 enodes (cost 9 ) 382.564 * * [simplify]: iteration done : 5000 enodes (cost 9 ) 382.565 * * [simplify]: iteration 0 : 8 enodes (cost 9 ) 382.566 * * [simplify]: iteration 1 : 23 enodes (cost 9 ) 382.569 * * [simplify]: iteration 2 : 45 enodes (cost 9 ) 382.581 * * [simplify]: iteration 3 : 82 enodes (cost 9 ) 382.595 * * [simplify]: iteration 4 : 176 enodes (cost 9 ) 382.646 * * [simplify]: iteration 5 : 520 enodes (cost 9 ) 382.987 * * [simplify]: iteration 6 : 2326 enodes (cost 9 ) 384.219 * * [simplify]: iteration done : 5001 enodes (cost 9 ) 384.220 * * [simplify]: iteration 0 : 8 enodes (cost 9 ) 384.221 * * [simplify]: iteration 1 : 26 enodes (cost 9 ) 384.225 * * [simplify]: iteration 2 : 62 enodes (cost 9 ) 384.235 * * [simplify]: iteration 3 : 134 enodes (cost 9 ) 384.258 * * [simplify]: iteration 4 : 366 enodes (cost 9 ) 384.384 * * [simplify]: iteration 5 : 1490 enodes (cost 9 ) 385.159 * * [simplify]: iteration done : 5000 enodes (cost 9 ) 385.160 * * [simplify]: iteration 0 : 9 enodes (cost 19 ) 385.162 * * [simplify]: iteration 1 : 24 enodes (cost 19 ) 385.171 * * [simplify]: iteration 2 : 46 enodes (cost 19 ) 385.178 * * [simplify]: iteration 3 : 80 enodes (cost 19 ) 385.192 * * [simplify]: iteration 4 : 172 enodes (cost 19 ) 385.242 * * [simplify]: iteration 5 : 498 enodes (cost 19 ) 385.587 * * [simplify]: iteration 6 : 2272 enodes (cost 19 ) 386.776 * * [simplify]: iteration done : 5000 enodes (cost 19 ) 386.777 * * [simplify]: iteration 0 : 8 enodes (cost 9 ) 386.778 * * [simplify]: iteration 1 : 23 enodes (cost 9 ) 386.782 * * [simplify]: iteration 2 : 45 enodes (cost 9 ) 386.788 * * [simplify]: iteration 3 : 79 enodes (cost 9 ) 386.802 * * [simplify]: iteration 4 : 169 enodes (cost 9 ) 386.852 * * [simplify]: iteration 5 : 502 enodes (cost 9 ) 387.197 * * [simplify]: iteration 6 : 2259 enodes (cost 9 ) 388.326 * * [simplify]: iteration done : 5000 enodes (cost 9 ) 388.327 * * [simplify]: iteration 0 : 9 enodes (cost 26 ) 388.329 * * [simplify]: iteration 1 : 25 enodes (cost 26 ) 388.340 * * [simplify]: iteration 2 : 60 enodes (cost 10 ) 388.353 * * [simplify]: iteration 3 : 230 enodes (cost 10 ) 388.476 * * [simplify]: iteration 4 : 1413 enodes (cost 10 ) 389.348 * * [simplify]: iteration done : 5001 enodes (cost 10 ) 389.348 * * [simplify]: iteration 0 : 8 enodes (cost 9 ) 389.349 * * [simplify]: iteration 1 : 23 enodes (cost 9 ) 389.359 * * [simplify]: iteration 2 : 45 enodes (cost 9 ) 389.366 * * [simplify]: iteration 3 : 79 enodes (cost 9 ) 389.379 * * [simplify]: iteration 4 : 169 enodes (cost 9 ) 389.428 * * [simplify]: iteration 5 : 502 enodes (cost 9 ) 389.775 * * [simplify]: iteration 6 : 2259 enodes (cost 9 ) 390.903 * * [simplify]: iteration done : 5000 enodes (cost 9 ) 390.903 * * [simplify]: iteration 0 : 8 enodes (cost 9 ) 390.904 * * [simplify]: iteration 1 : 23 enodes (cost 9 ) 390.908 * * [simplify]: iteration 2 : 45 enodes (cost 9 ) 390.914 * * [simplify]: iteration 3 : 79 enodes (cost 9 ) 390.933 * * [simplify]: iteration 4 : 169 enodes (cost 9 ) 390.983 * * [simplify]: iteration 5 : 502 enodes (cost 9 ) 391.326 * * [simplify]: iteration 6 : 2259 enodes (cost 9 ) 392.431 * * [simplify]: iteration done : 5000 enodes (cost 9 ) 392.432 * * [simplify]: iteration 0 : 8 enodes (cost 14 ) 392.433 * * [simplify]: iteration 1 : 15 enodes (cost 11 ) 392.435 * * [simplify]: iteration 2 : 23 enodes (cost 11 ) 392.439 * * [simplify]: iteration 3 : 26 enodes (cost 11 ) 392.442 * * [simplify]: iteration 4 : 27 enodes (cost 11 ) 392.446 * * [simplify]: iteration done : 27 enodes (cost 11 ) 392.447 * * [simplify]: iteration 0 : 4 enodes (cost 4 ) 392.448 * * [simplify]: iteration 1 : 6 enodes (cost 4 ) 392.448 * * [simplify]: iteration 2 : 7 enodes (cost 4 ) 392.449 * * [simplify]: iteration done : 7 enodes (cost 4 ) 392.449 * * [simplify]: iteration 0 : 9 enodes (cost 12 ) 392.451 * * [simplify]: iteration 1 : 34 enodes (cost 12 ) 392.464 * * [simplify]: iteration 2 : 134 enodes (cost 12 ) 392.525 * * [simplify]: iteration 3 : 525 enodes (cost 12 ) 393.043 * * [simplify]: iteration 4 : 2010 enodes (cost 12 ) 394.711 * * [simplify]: iteration done : 5000 enodes (cost 12 ) 394.712 * * [simplify]: iteration 0 : 11 enodes (cost 26 ) 394.714 * * [simplify]: iteration 1 : 35 enodes (cost 17 ) 394.720 * * [simplify]: iteration 2 : 121 enodes (cost 17 ) 394.755 * * [simplify]: iteration 3 : 358 enodes (cost 17 ) 394.908 * * [simplify]: iteration 4 : 972 enodes (cost 17 ) 395.931 * * [simplify]: iteration 5 : 3415 enodes (cost 15 ) 397.895 * * [simplify]: iteration done : 5001 enodes (cost 15 ) 397.896 * * [simplify]: iteration 0 : 5 enodes (cost 5 ) 397.897 * * [simplify]: iteration 1 : 13 enodes (cost 5 ) 397.898 * * [simplify]: iteration 2 : 28 enodes (cost 5 ) 397.902 * * [simplify]: iteration 3 : 49 enodes (cost 5 ) 397.909 * * [simplify]: iteration 4 : 91 enodes (cost 5 ) 397.938 * * [simplify]: iteration 5 : 224 enodes (cost 5 ) 398.111 * * [simplify]: iteration 6 : 741 enodes (cost 5 ) 400.080 * * [simplify]: iteration 7 : 3056 enodes (cost 5 ) 403.643 * * [simplify]: iteration done : 5000 enodes (cost 5 ) 403.644 * * [simplify]: iteration 0 : 9 enodes (cost 17 ) 403.645 * * [simplify]: iteration 1 : 31 enodes (cost 8 ) 403.652 * * [simplify]: iteration 2 : 85 enodes (cost 8 ) 403.675 * * [simplify]: iteration 3 : 233 enodes (cost 8 ) 403.769 * * [simplify]: iteration 4 : 806 enodes (cost 8 ) 404.573 * * [simplify]: iteration 5 : 3520 enodes (cost 8 ) 406.111 * * [simplify]: iteration done : 5000 enodes (cost 8 ) 406.112 * * [simplify]: iteration 0 : 7 enodes (cost 8 ) 406.113 * * [simplify]: iteration 1 : 21 enodes (cost 8 ) 406.116 * * [simplify]: iteration 2 : 30 enodes (cost 8 ) 406.120 * * [simplify]: iteration 3 : 47 enodes (cost 8 ) 406.126 * * [simplify]: iteration 4 : 88 enodes (cost 8 ) 406.146 * * [simplify]: iteration 5 : 210 enodes (cost 8 ) 406.241 * * [simplify]: iteration 6 : 614 enodes (cost 8 ) 407.171 * * [simplify]: iteration 7 : 2450 enodes (cost 8 ) 409.269 * * [simplify]: iteration done : 5000 enodes (cost 8 ) 409.270 * * [simplify]: iteration 0 : 9 enodes (cost 10 ) 409.271 * * [simplify]: iteration 1 : 23 enodes (cost 10 ) 409.274 * * [simplify]: iteration 2 : 32 enodes (cost 10 ) 409.277 * * [simplify]: iteration 3 : 50 enodes (cost 10 ) 409.284 * * [simplify]: iteration 4 : 89 enodes (cost 10 ) 409.304 * * [simplify]: iteration 5 : 206 enodes (cost 10 ) 409.400 * * [simplify]: iteration 6 : 616 enodes (cost 10 ) 410.326 * * [simplify]: iteration 7 : 2429 enodes (cost 10 ) 412.576 * * [simplify]: iteration done : 5001 enodes (cost 10 ) 412.576 * * [simplify]: iteration 0 : 9 enodes (cost 10 ) 412.578 * * [simplify]: iteration 1 : 24 enodes (cost 10 ) 412.581 * * [simplify]: iteration 2 : 46 enodes (cost 10 ) 412.587 * * [simplify]: iteration 3 : 81 enodes (cost 10 ) 412.601 * * [simplify]: iteration 4 : 171 enodes (cost 10 ) 412.651 * * [simplify]: iteration 5 : 509 enodes (cost 10 ) 413.005 * * [simplify]: iteration 6 : 2263 enodes (cost 10 ) 414.189 * * [simplify]: iteration done : 5001 enodes (cost 10 ) 414.190 * * [simplify]: iteration 0 : 9 enodes (cost 10 ) 414.192 * * [simplify]: iteration 1 : 23 enodes (cost 10 ) 414.195 * * [simplify]: iteration 2 : 32 enodes (cost 10 ) 414.203 * * [simplify]: iteration 3 : 50 enodes (cost 10 ) 414.210 * * [simplify]: iteration 4 : 89 enodes (cost 10 ) 414.229 * * [simplify]: iteration 5 : 206 enodes (cost 10 ) 414.328 * * [simplify]: iteration 6 : 616 enodes (cost 10 ) 415.251 * * [simplify]: iteration 7 : 2429 enodes (cost 10 ) 417.502 * * [simplify]: iteration done : 5001 enodes (cost 10 ) 417.502 * * [simplify]: iteration 0 : 9 enodes (cost 10 ) 417.503 * * [simplify]: iteration 1 : 24 enodes (cost 10 ) 417.507 * * [simplify]: iteration 2 : 46 enodes (cost 10 ) 417.514 * * [simplify]: iteration 3 : 81 enodes (cost 10 ) 417.527 * * [simplify]: iteration 4 : 171 enodes (cost 10 ) 417.577 * * [simplify]: iteration 5 : 509 enodes (cost 10 ) 417.933 * * [simplify]: iteration 6 : 2263 enodes (cost 10 ) 419.120 * * [simplify]: iteration done : 5001 enodes (cost 10 ) 419.120 * * [simplify]: iteration 0 : 9 enodes (cost 10 ) 419.122 * * [simplify]: iteration 1 : 23 enodes (cost 10 ) 419.124 * * [simplify]: iteration 2 : 33 enodes (cost 10 ) 419.128 * * [simplify]: iteration 3 : 50 enodes (cost 10 ) 419.134 * * [simplify]: iteration 4 : 89 enodes (cost 10 ) 419.157 * * [simplify]: iteration 5 : 202 enodes (cost 10 ) 419.252 * * [simplify]: iteration 6 : 610 enodes (cost 10 ) 420.175 * * [simplify]: iteration 7 : 2426 enodes (cost 10 ) 422.160 * * [simplify]: iteration done : 5000 enodes (cost 10 ) 422.161 * * [simplify]: iteration 0 : 9 enodes (cost 10 ) 422.162 * * [simplify]: iteration 1 : 24 enodes (cost 10 ) 422.165 * * [simplify]: iteration 2 : 35 enodes (cost 10 ) 422.169 * * [simplify]: iteration 3 : 52 enodes (cost 10 ) 422.176 * * [simplify]: iteration 4 : 91 enodes (cost 10 ) 422.199 * * [simplify]: iteration 5 : 200 enodes (cost 10 ) 422.293 * * [simplify]: iteration 6 : 605 enodes (cost 10 ) 423.226 * * [simplify]: iteration 7 : 2448 enodes (cost 10 ) 425.279 * * [simplify]: iteration done : 5000 enodes (cost 10 ) 425.280 * * [simplify]: iteration 0 : 10 enodes (cost 11 ) 425.281 * * [simplify]: iteration 1 : 21 enodes (cost 9 ) 425.284 * * [simplify]: iteration 2 : 31 enodes (cost 9 ) 425.287 * * [simplify]: iteration 3 : 47 enodes (cost 9 ) 425.293 * * [simplify]: iteration 4 : 85 enodes (cost 9 ) 425.315 * * [simplify]: iteration 5 : 200 enodes (cost 9 ) 425.410 * * [simplify]: iteration 6 : 608 enodes (cost 9 ) 426.337 * * [simplify]: iteration 7 : 2435 enodes (cost 9 ) 428.608 * * [simplify]: iteration done : 5001 enodes (cost 9 ) 428.609 * * [simplify]: iteration 0 : 10 enodes (cost 11 ) 428.611 * * [simplify]: iteration 1 : 21 enodes (cost 9 ) 428.613 * * [simplify]: iteration 2 : 38 enodes (cost 9 ) 428.618 * * [simplify]: iteration 3 : 73 enodes (cost 9 ) 428.630 * * [simplify]: iteration 4 : 163 enodes (cost 9 ) 428.676 * * [simplify]: iteration 5 : 499 enodes (cost 9 ) 429.023 * * [simplify]: iteration 6 : 2281 enodes (cost 9 ) 430.236 * * [simplify]: iteration done : 5000 enodes (cost 9 ) 430.237 * * [simplify]: iteration 0 : 9 enodes (cost 10 ) 430.238 * * [simplify]: iteration 1 : 23 enodes (cost 10 ) 430.241 * * [simplify]: iteration 2 : 32 enodes (cost 10 ) 430.244 * * [simplify]: iteration 3 : 50 enodes (cost 10 ) 430.251 * * [simplify]: iteration 4 : 89 enodes (cost 10 ) 430.274 * * [simplify]: iteration 5 : 206 enodes (cost 10 ) 430.367 * * [simplify]: iteration 6 : 616 enodes (cost 10 ) 431.297 * * [simplify]: iteration 7 : 2429 enodes (cost 10 ) 433.583 * * [simplify]: iteration done : 5001 enodes (cost 10 ) 433.583 * * [simplify]: iteration 0 : 9 enodes (cost 10 ) 433.585 * * [simplify]: iteration 1 : 24 enodes (cost 10 ) 433.588 * * [simplify]: iteration 2 : 46 enodes (cost 10 ) 433.594 * * [simplify]: iteration 3 : 81 enodes (cost 10 ) 433.612 * * [simplify]: iteration 4 : 171 enodes (cost 10 ) 433.662 * * [simplify]: iteration 5 : 509 enodes (cost 10 ) 434.013 * * [simplify]: iteration 6 : 2263 enodes (cost 10 ) 435.206 * * [simplify]: iteration done : 5001 enodes (cost 10 ) 435.207 * * [simplify]: iteration 0 : 9 enodes (cost 10 ) 435.208 * * [simplify]: iteration 1 : 23 enodes (cost 10 ) 435.211 * * [simplify]: iteration 2 : 32 enodes (cost 10 ) 435.215 * * [simplify]: iteration 3 : 50 enodes (cost 10 ) 435.221 * * [simplify]: iteration 4 : 89 enodes (cost 10 ) 435.240 * * [simplify]: iteration 5 : 206 enodes (cost 10 ) 435.337 * * [simplify]: iteration 6 : 616 enodes (cost 10 ) 436.270 * * [simplify]: iteration 7 : 2429 enodes (cost 10 ) 438.539 * * [simplify]: iteration done : 5001 enodes (cost 10 ) 438.540 * * [simplify]: iteration 0 : 9 enodes (cost 10 ) 438.541 * * [simplify]: iteration 1 : 24 enodes (cost 10 ) 438.544 * * [simplify]: iteration 2 : 46 enodes (cost 10 ) 438.551 * * [simplify]: iteration 3 : 81 enodes (cost 10 ) 438.565 * * [simplify]: iteration 4 : 171 enodes (cost 10 ) 438.615 * * [simplify]: iteration 5 : 509 enodes (cost 10 ) 438.964 * * [simplify]: iteration 6 : 2263 enodes (cost 10 ) 440.131 * * [simplify]: iteration done : 5001 enodes (cost 10 ) 440.131 * * [simplify]: iteration 0 : 9 enodes (cost 10 ) 440.133 * * [simplify]: iteration 1 : 23 enodes (cost 10 ) 440.135 * * [simplify]: iteration 2 : 33 enodes (cost 10 ) 440.139 * * [simplify]: iteration 3 : 50 enodes (cost 10 ) 440.145 * * [simplify]: iteration 4 : 89 enodes (cost 10 ) 440.163 * * [simplify]: iteration 5 : 202 enodes (cost 10 ) 440.255 * * [simplify]: iteration 6 : 610 enodes (cost 10 ) 441.160 * * [simplify]: iteration 7 : 2426 enodes (cost 10 ) 443.120 * * [simplify]: iteration done : 5000 enodes (cost 10 ) 443.121 * * [simplify]: iteration 0 : 9 enodes (cost 10 ) 443.122 * * [simplify]: iteration 1 : 24 enodes (cost 10 ) 443.125 * * [simplify]: iteration 2 : 35 enodes (cost 10 ) 443.129 * * [simplify]: iteration 3 : 52 enodes (cost 10 ) 443.136 * * [simplify]: iteration 4 : 91 enodes (cost 10 ) 443.154 * * [simplify]: iteration 5 : 200 enodes (cost 10 ) 443.247 * * [simplify]: iteration 6 : 605 enodes (cost 10 ) 444.185 * * [simplify]: iteration 7 : 2448 enodes (cost 10 ) 445.984 * * [simplify]: iteration done : 5000 enodes (cost 10 ) 445.984 * * [simplify]: iteration 0 : 10 enodes (cost 11 ) 445.986 * * [simplify]: iteration 1 : 21 enodes (cost 9 ) 445.988 * * [simplify]: iteration 2 : 31 enodes (cost 9 ) 445.991 * * [simplify]: iteration 3 : 47 enodes (cost 9 ) 445.997 * * [simplify]: iteration 4 : 85 enodes (cost 9 ) 446.015 * * [simplify]: iteration 5 : 200 enodes (cost 9 ) 446.106 * * [simplify]: iteration 6 : 608 enodes (cost 9 ) 447.012 * * [simplify]: iteration 7 : 2435 enodes (cost 9 ) 449.487 * * [simplify]: iteration done : 5001 enodes (cost 9 ) 449.488 * * [simplify]: iteration 0 : 10 enodes (cost 11 ) 449.489 * * [simplify]: iteration 1 : 21 enodes (cost 9 ) 449.497 * * [simplify]: iteration 2 : 38 enodes (cost 9 ) 449.502 * * [simplify]: iteration 3 : 73 enodes (cost 9 ) 449.513 * * [simplify]: iteration 4 : 163 enodes (cost 9 ) 449.557 * * [simplify]: iteration 5 : 499 enodes (cost 9 ) 449.903 * * [simplify]: iteration 6 : 2281 enodes (cost 9 ) 451.125 * * [simplify]: iteration done : 5000 enodes (cost 9 ) 451.126 * * [simplify]: iteration 0 : 9 enodes (cost 10 ) 451.127 * * [simplify]: iteration 1 : 23 enodes (cost 10 ) 451.130 * * [simplify]: iteration 2 : 33 enodes (cost 10 ) 451.142 * * [simplify]: iteration 3 : 51 enodes (cost 10 ) 451.148 * * [simplify]: iteration 4 : 92 enodes (cost 10 ) 451.166 * * [simplify]: iteration 5 : 210 enodes (cost 10 ) 451.261 * * [simplify]: iteration 6 : 618 enodes (cost 10 ) 452.195 * * [simplify]: iteration 7 : 2456 enodes (cost 10 ) 454.356 * * [simplify]: iteration done : 5001 enodes (cost 10 ) 454.357 * * [simplify]: iteration 0 : 9 enodes (cost 10 ) 454.363 * * [simplify]: iteration 1 : 24 enodes (cost 10 ) 454.366 * * [simplify]: iteration 2 : 44 enodes (cost 10 ) 454.372 * * [simplify]: iteration 3 : 73 enodes (cost 10 ) 454.389 * * [simplify]: iteration 4 : 138 enodes (cost 10 ) 454.423 * * [simplify]: iteration 5 : 329 enodes (cost 10 ) 454.659 * * [simplify]: iteration 6 : 1059 enodes (cost 10 ) 457.207 * * [simplify]: iteration 7 : 4329 enodes (cost 10 ) 459.658 * * [simplify]: iteration done : 5001 enodes (cost 10 ) 459.658 * * [simplify]: iteration 0 : 9 enodes (cost 10 ) 459.660 * * [simplify]: iteration 1 : 23 enodes (cost 10 ) 459.662 * * [simplify]: iteration 2 : 33 enodes (cost 10 ) 459.666 * * [simplify]: iteration 3 : 51 enodes (cost 10 ) 459.673 * * [simplify]: iteration 4 : 92 enodes (cost 10 ) 459.692 * * [simplify]: iteration 5 : 210 enodes (cost 10 ) 459.787 * * [simplify]: iteration 6 : 618 enodes (cost 10 ) 460.720 * * [simplify]: iteration 7 : 2456 enodes (cost 10 ) 462.870 * * [simplify]: iteration done : 5001 enodes (cost 10 ) 462.871 * * [simplify]: iteration 0 : 9 enodes (cost 10 ) 462.872 * * [simplify]: iteration 1 : 24 enodes (cost 10 ) 462.875 * * [simplify]: iteration 2 : 44 enodes (cost 10 ) 462.880 * * [simplify]: iteration 3 : 73 enodes (cost 10 ) 462.891 * * [simplify]: iteration 4 : 138 enodes (cost 10 ) 462.930 * * [simplify]: iteration 5 : 329 enodes (cost 10 ) 463.156 * * [simplify]: iteration 6 : 1059 enodes (cost 10 ) 465.657 * * [simplify]: iteration 7 : 4329 enodes (cost 10 ) 468.100 * * [simplify]: iteration done : 5001 enodes (cost 10 ) 468.100 * * [simplify]: iteration 0 : 9 enodes (cost 10 ) 468.102 * * [simplify]: iteration 1 : 23 enodes (cost 10 ) 468.104 * * [simplify]: iteration 2 : 34 enodes (cost 10 ) 468.108 * * [simplify]: iteration 3 : 51 enodes (cost 10 ) 468.114 * * [simplify]: iteration 4 : 92 enodes (cost 10 ) 468.138 * * [simplify]: iteration 5 : 204 enodes (cost 10 ) 468.232 * * [simplify]: iteration 6 : 606 enodes (cost 10 ) 469.145 * * [simplify]: iteration 7 : 2443 enodes (cost 10 ) 471.072 * * [simplify]: iteration done : 5000 enodes (cost 10 ) 471.073 * * [simplify]: iteration 0 : 9 enodes (cost 10 ) 471.075 * * [simplify]: iteration 1 : 24 enodes (cost 10 ) 471.078 * * [simplify]: iteration 2 : 36 enodes (cost 10 ) 471.082 * * [simplify]: iteration 3 : 53 enodes (cost 10 ) 471.089 * * [simplify]: iteration 4 : 94 enodes (cost 10 ) 471.107 * * [simplify]: iteration 5 : 210 enodes (cost 10 ) 471.203 * * [simplify]: iteration 6 : 619 enodes (cost 10 ) 472.342 * * [simplify]: iteration 7 : 2445 enodes (cost 10 ) 474.151 * * [simplify]: iteration done : 5000 enodes (cost 10 ) 474.152 * * [simplify]: iteration 0 : 10 enodes (cost 11 ) 474.153 * * [simplify]: iteration 1 : 21 enodes (cost 9 ) 474.156 * * [simplify]: iteration 2 : 32 enodes (cost 9 ) 474.159 * * [simplify]: iteration 3 : 48 enodes (cost 9 ) 474.165 * * [simplify]: iteration 4 : 90 enodes (cost 9 ) 474.182 * * [simplify]: iteration 5 : 211 enodes (cost 9 ) 474.274 * * [simplify]: iteration 6 : 620 enodes (cost 9 ) 475.177 * * [simplify]: iteration 7 : 2426 enodes (cost 9 ) 477.188 * * [simplify]: iteration done : 5000 enodes (cost 9 ) 477.189 * * [simplify]: iteration 0 : 10 enodes (cost 11 ) 477.190 * * [simplify]: iteration 1 : 21 enodes (cost 9 ) 477.193 * * [simplify]: iteration 2 : 37 enodes (cost 9 ) 477.197 * * [simplify]: iteration 3 : 65 enodes (cost 9 ) 477.206 * * [simplify]: iteration 4 : 127 enodes (cost 9 ) 477.241 * * [simplify]: iteration 5 : 316 enodes (cost 9 ) 477.477 * * [simplify]: iteration 6 : 1033 enodes (cost 9 ) 479.974 * * [simplify]: iteration 7 : 4258 enodes (cost 9 ) 482.449 * * [simplify]: iteration done : 5000 enodes (cost 9 ) 482.450 * * [simplify]: iteration 0 : 10 enodes (cost 11 ) 482.451 * * [simplify]: iteration 1 : 21 enodes (cost 9 ) 482.454 * * [simplify]: iteration 2 : 31 enodes (cost 9 ) 482.457 * * [simplify]: iteration 3 : 48 enodes (cost 9 ) 482.463 * * [simplify]: iteration 4 : 88 enodes (cost 9 ) 482.487 * * [simplify]: iteration 5 : 203 enodes (cost 9 ) 482.582 * * [simplify]: iteration 6 : 611 enodes (cost 9 ) 483.504 * * [simplify]: iteration 7 : 2444 enodes (cost 9 ) 485.412 * * [simplify]: iteration done : 5001 enodes (cost 9 ) 485.413 * * [simplify]: iteration 0 : 10 enodes (cost 11 ) 485.414 * * [simplify]: iteration 1 : 21 enodes (cost 9 ) 485.418 * * [simplify]: iteration 2 : 45 enodes (cost 9 ) 485.423 * * [simplify]: iteration 3 : 79 enodes (cost 9 ) 485.436 * * [simplify]: iteration 4 : 164 enodes (cost 9 ) 485.483 * * [simplify]: iteration 5 : 496 enodes (cost 9 ) 485.817 * * [simplify]: iteration 6 : 2241 enodes (cost 9 ) 486.993 * * [simplify]: iteration done : 5001 enodes (cost 9 ) 486.994 * * [simplify]: iteration 0 : 10 enodes (cost 11 ) 486.995 * * [simplify]: iteration 1 : 21 enodes (cost 9 ) 486.998 * * [simplify]: iteration 2 : 31 enodes (cost 9 ) 487.001 * * [simplify]: iteration 3 : 48 enodes (cost 9 ) 487.007 * * [simplify]: iteration 4 : 88 enodes (cost 9 ) 487.026 * * [simplify]: iteration 5 : 203 enodes (cost 9 ) 487.118 * * [simplify]: iteration 6 : 611 enodes (cost 9 ) 488.021 * * [simplify]: iteration 7 : 2444 enodes (cost 9 ) 489.941 * * [simplify]: iteration done : 5001 enodes (cost 9 ) 489.942 * * [simplify]: iteration 0 : 10 enodes (cost 11 ) 489.943 * * [simplify]: iteration 1 : 21 enodes (cost 9 ) 489.946 * * [simplify]: iteration 2 : 45 enodes (cost 9 ) 489.951 * * [simplify]: iteration 3 : 79 enodes (cost 9 ) 489.969 * * [simplify]: iteration 4 : 164 enodes (cost 9 ) 490.013 * * [simplify]: iteration 5 : 496 enodes (cost 9 ) 490.352 * * [simplify]: iteration 6 : 2241 enodes (cost 9 ) 491.532 * * [simplify]: iteration done : 5001 enodes (cost 9 ) 491.533 * * [simplify]: iteration 0 : 10 enodes (cost 11 ) 491.534 * * [simplify]: iteration 1 : 21 enodes (cost 9 ) 491.537 * * [simplify]: iteration 2 : 32 enodes (cost 9 ) 491.540 * * [simplify]: iteration 3 : 48 enodes (cost 9 ) 491.553 * * [simplify]: iteration 4 : 86 enodes (cost 9 ) 491.571 * * [simplify]: iteration 5 : 200 enodes (cost 9 ) 491.661 * * [simplify]: iteration 6 : 609 enodes (cost 9 ) 492.564 * * [simplify]: iteration 7 : 2441 enodes (cost 9 ) 494.926 * * [simplify]: iteration done : 5000 enodes (cost 9 ) 494.927 * * [simplify]: iteration 0 : 10 enodes (cost 11 ) 494.928 * * [simplify]: iteration 1 : 21 enodes (cost 9 ) 494.931 * * [simplify]: iteration 2 : 34 enodes (cost 9 ) 494.940 * * [simplify]: iteration 3 : 50 enodes (cost 9 ) 494.946 * * [simplify]: iteration 4 : 90 enodes (cost 9 ) 494.964 * * [simplify]: iteration 5 : 198 enodes (cost 9 ) 495.057 * * [simplify]: iteration 6 : 603 enodes (cost 9 ) 495.966 * * [simplify]: iteration 7 : 2428 enodes (cost 9 ) 498.092 * * [simplify]: iteration done : 5001 enodes (cost 9 ) 498.093 * * [simplify]: iteration 0 : 9 enodes (cost 12 ) 498.094 * * [simplify]: iteration 1 : 16 enodes (cost 8 ) 498.096 * * [simplify]: iteration 2 : 25 enodes (cost 8 ) 498.099 * * [simplify]: iteration 3 : 43 enodes (cost 8 ) 498.104 * * [simplify]: iteration 4 : 84 enodes (cost 8 ) 498.128 * * [simplify]: iteration 5 : 195 enodes (cost 8 ) 498.218 * * [simplify]: iteration 6 : 611 enodes (cost 8 ) 499.122 * * [simplify]: iteration 7 : 2463 enodes (cost 8 ) 501.252 * * [simplify]: iteration done : 5001 enodes (cost 8 ) 501.253 * * [simplify]: iteration 0 : 9 enodes (cost 12 ) 501.254 * * [simplify]: iteration 1 : 18 enodes (cost 8 ) 501.256 * * [simplify]: iteration 2 : 34 enodes (cost 8 ) 501.261 * * [simplify]: iteration 3 : 64 enodes (cost 8 ) 501.271 * * [simplify]: iteration 4 : 151 enodes (cost 8 ) 501.316 * * [simplify]: iteration 5 : 482 enodes (cost 8 ) 501.661 * * [simplify]: iteration 6 : 2285 enodes (cost 8 ) 502.779 * * [simplify]: iteration done : 5000 enodes (cost 8 ) 502.780 * * [simplify]: iteration 0 : 7 enodes (cost 8 ) 502.781 * * [simplify]: iteration 1 : 22 enodes (cost 8 ) 502.784 * * [simplify]: iteration 2 : 44 enodes (cost 8 ) 502.790 * * [simplify]: iteration 3 : 78 enodes (cost 8 ) 502.803 * * [simplify]: iteration 4 : 165 enodes (cost 8 ) 502.851 * * [simplify]: iteration 5 : 500 enodes (cost 8 ) 503.201 * * [simplify]: iteration 6 : 2253 enodes (cost 8 ) 504.345 * * [simplify]: iteration done : 5001 enodes (cost 8 ) 504.346 * * [simplify]: iteration 0 : 7 enodes (cost 8 ) 504.347 * * [simplify]: iteration 1 : 22 enodes (cost 8 ) 504.350 * * [simplify]: iteration 2 : 44 enodes (cost 8 ) 504.356 * * [simplify]: iteration 3 : 78 enodes (cost 8 ) 504.369 * * [simplify]: iteration 4 : 165 enodes (cost 8 ) 504.418 * * [simplify]: iteration 5 : 500 enodes (cost 8 ) 504.765 * * [simplify]: iteration 6 : 2253 enodes (cost 8 ) 505.918 * * [simplify]: iteration done : 5001 enodes (cost 8 ) 505.918 * * [simplify]: iteration 0 : 7 enodes (cost 8 ) 505.919 * * [simplify]: iteration 1 : 22 enodes (cost 8 ) 505.923 * * [simplify]: iteration 2 : 44 enodes (cost 8 ) 505.929 * * [simplify]: iteration 3 : 78 enodes (cost 8 ) 505.941 * * [simplify]: iteration 4 : 165 enodes (cost 8 ) 505.991 * * [simplify]: iteration 5 : 500 enodes (cost 8 ) 506.338 * * [simplify]: iteration 6 : 2253 enodes (cost 8 ) 507.491 * * [simplify]: iteration done : 5001 enodes (cost 8 ) 507.492 * * [simplify]: iteration 0 : 7 enodes (cost 8 ) 507.493 * * [simplify]: iteration 1 : 22 enodes (cost 8 ) 507.496 * * [simplify]: iteration 2 : 44 enodes (cost 8 ) 507.502 * * [simplify]: iteration 3 : 78 enodes (cost 8 ) 507.520 * * [simplify]: iteration 4 : 165 enodes (cost 8 ) 507.564 * * [simplify]: iteration 5 : 500 enodes (cost 8 ) 507.912 * * [simplify]: iteration 6 : 2253 enodes (cost 8 ) 509.072 * * [simplify]: iteration done : 5001 enodes (cost 8 ) 509.073 * * [simplify]: iteration 0 : 7 enodes (cost 8 ) 509.074 * * [simplify]: iteration 1 : 22 enodes (cost 8 ) 509.077 * * [simplify]: iteration 2 : 44 enodes (cost 8 ) 509.084 * * [simplify]: iteration 3 : 78 enodes (cost 8 ) 509.102 * * [simplify]: iteration 4 : 165 enodes (cost 8 ) 509.147 * * [simplify]: iteration 5 : 500 enodes (cost 8 ) 509.494 * * [simplify]: iteration 6 : 2253 enodes (cost 8 ) 510.653 * * [simplify]: iteration done : 5001 enodes (cost 8 ) 510.654 * * [simplify]: iteration 0 : 5 enodes (cost 5 ) 510.655 * * [simplify]: iteration 1 : 13 enodes (cost 5 ) 510.657 * * [simplify]: iteration 2 : 28 enodes (cost 5 ) 510.660 * * [simplify]: iteration 3 : 49 enodes (cost 5 ) 510.668 * * [simplify]: iteration 4 : 91 enodes (cost 5 ) 510.697 * * [simplify]: iteration 5 : 224 enodes (cost 5 ) 510.869 * * [simplify]: iteration 6 : 741 enodes (cost 5 ) 512.837 * * [simplify]: iteration 7 : 3056 enodes (cost 5 ) 516.374 * * [simplify]: iteration done : 5000 enodes (cost 5 ) 516.375 * * [simplify]: iteration 0 : 6 enodes (cost 6 ) 516.381 * * [simplify]: iteration 1 : 9 enodes (cost 5 ) 516.382 * * [simplify]: iteration 2 : 10 enodes (cost 5 ) 516.383 * * [simplify]: iteration done : 10 enodes (cost 5 ) 516.384 * * [simplify]: iteration 0 : 5 enodes (cost 5 ) 516.384 * * [simplify]: iteration 1 : 6 enodes (cost 5 ) 516.385 * * [simplify]: iteration done : 6 enodes (cost 5 ) 516.385 * * [simplify]: iteration 0 : 5 enodes (cost 5 ) 516.386 * * [simplify]: iteration 1 : 9 enodes (cost 5 ) 516.387 * * [simplify]: iteration 2 : 10 enodes (cost 5 ) 516.388 * * [simplify]: iteration done : 10 enodes (cost 5 ) 516.388 * * [simplify]: iteration 0 : 6 enodes (cost 11 ) 516.389 * * [simplify]: iteration 1 : 7 enodes (cost 11 ) 516.390 * * [simplify]: iteration done : 7 enodes (cost 11 ) 516.390 * * [simplify]: iteration 0 : 5 enodes (cost 5 ) 516.391 * * [simplify]: iteration 1 : 6 enodes (cost 5 ) 516.391 * * [simplify]: iteration done : 6 enodes (cost 5 ) 516.392 * * [simplify]: iteration 0 : 6 enodes (cost 14 ) 516.393 * * [simplify]: iteration 1 : 20 enodes (cost 14 ) 516.396 * * [simplify]: iteration 2 : 52 enodes (cost 6 ) 516.413 * * [simplify]: iteration 3 : 117 enodes (cost 6 ) 516.446 * * [simplify]: iteration 4 : 276 enodes (cost 6 ) 516.628 * * [simplify]: iteration 5 : 847 enodes (cost 6 ) 517.464 * * [simplify]: iteration 6 : 1937 enodes (cost 6 ) 519.124 * * [simplify]: iteration 7 : 2715 enodes (cost 6 ) 521.373 * * [simplify]: iteration 8 : 3202 enodes (cost 6 ) 524.273 * * [simplify]: iteration 9 : 4284 enodes (cost 6 ) 525.682 * * [simplify]: iteration done : 5001 enodes (cost 6 ) 525.683 * * [simplify]: iteration 0 : 5 enodes (cost 5 ) 525.683 * * [simplify]: iteration 1 : 6 enodes (cost 5 ) 525.684 * * [simplify]: iteration done : 6 enodes (cost 5 ) 525.689 * * [simplify]: iteration 0 : 5 enodes (cost 5 ) 525.689 * * [simplify]: iteration 1 : 6 enodes (cost 5 ) 525.690 * * [simplify]: iteration done : 6 enodes (cost 5 ) 525.690 * * [simplify]: iteration 0 : 7 enodes (cost 8 ) 525.692 * * [simplify]: iteration 1 : 21 enodes (cost 8 ) 525.694 * * [simplify]: iteration 2 : 30 enodes (cost 8 ) 525.698 * * [simplify]: iteration 3 : 47 enodes (cost 8 ) 525.705 * * [simplify]: iteration 4 : 88 enodes (cost 8 ) 525.723 * * [simplify]: iteration 5 : 201 enodes (cost 8 ) 525.824 * * [simplify]: iteration 6 : 602 enodes (cost 8 ) 526.744 * * [simplify]: iteration 7 : 2456 enodes (cost 8 ) 528.909 * * [simplify]: iteration done : 5000 enodes (cost 8 ) 528.910 * * [simplify]: iteration 0 : 8 enodes (cost 14 ) 528.911 * * [simplify]: iteration 1 : 16 enodes (cost 12 ) 528.916 * * [simplify]: iteration 2 : 31 enodes (cost 12 ) 528.921 * * [simplify]: iteration 3 : 44 enodes (cost 11 ) 528.928 * * [simplify]: iteration 4 : 64 enodes (cost 11 ) 528.940 * * [simplify]: iteration 5 : 85 enodes (cost 11 ) 528.957 * * [simplify]: iteration 6 : 102 enodes (cost 11 ) 528.972 * * [simplify]: iteration 7 : 135 enodes (cost 11 ) 528.997 * * [simplify]: iteration 8 : 190 enodes (cost 11 ) 529.037 * * [simplify]: iteration 9 : 222 enodes (cost 11 ) 529.068 * * [simplify]: iteration done : 222 enodes (cost 11 ) 529.069 * * [simplify]: iteration 0 : 6 enodes (cost 9 ) 529.070 * * [simplify]: iteration 1 : 11 enodes (cost 9 ) 529.071 * * [simplify]: iteration 2 : 18 enodes (cost 9 ) 529.074 * * [simplify]: iteration 3 : 33 enodes (cost 9 ) 529.079 * * [simplify]: iteration 4 : 58 enodes (cost 9 ) 529.093 * * [simplify]: iteration 5 : 99 enodes (cost 9 ) 529.118 * * [simplify]: iteration 6 : 161 enodes (cost 9 ) 529.171 * * [simplify]: iteration 7 : 329 enodes (cost 9 ) 529.900 * * [simplify]: iteration 8 : 1627 enodes (cost 9 ) 535.789 * * [simplify]: iteration done : 5000 enodes (cost 9 ) 535.789 * * [simplify]: iteration 0 : 4 enodes (cost 4 ) 535.790 * * [simplify]: iteration 1 : 6 enodes (cost 4 ) 535.791 * * [simplify]: iteration 2 : 7 enodes (cost 4 ) 535.791 * * [simplify]: iteration done : 7 enodes (cost 4 ) 535.792 * * [simplify]: iteration 0 : 4 enodes (cost 4 ) 535.792 * * [simplify]: iteration 1 : 5 enodes (cost 4 ) 535.793 * * [simplify]: iteration done : 5 enodes (cost 4 ) 535.793 * * [simplify]: iteration 0 : 5 enodes (cost 5 ) 535.794 * * [simplify]: iteration 1 : 6 enodes (cost 5 ) 535.794 * * [simplify]: iteration done : 6 enodes (cost 5 ) 535.795 * * [simplify]: iteration 0 : 5 enodes (cost 5 ) 535.795 * * [simplify]: iteration 1 : 6 enodes (cost 5 ) 535.796 * * [simplify]: iteration done : 6 enodes (cost 5 ) 535.796 * * [simplify]: iteration 0 : 3 enodes (cost 3 ) 535.797 * * [simplify]: iteration 1 : 6 enodes (cost 1 ) 535.797 * * [simplify]: iteration done : 6 enodes (cost 1 ) 535.798 * * [simplify]: iteration 0 : 6 enodes (cost 8 ) 535.798 * * [simplify]: iteration 1 : 10 enodes (cost 8 ) 535.800 * * [simplify]: iteration 2 : 17 enodes (cost 8 ) 535.807 * * [simplify]: iteration 3 : 41 enodes (cost 8 ) 535.814 * * [simplify]: iteration 4 : 97 enodes (cost 8 ) 535.849 * * [simplify]: iteration 5 : 255 enodes (cost 8 ) 536.070 * * [simplify]: iteration 6 : 872 enodes (cost 8 ) 537.859 * * [simplify]: iteration 7 : 3300 enodes (cost 8 ) 539.091 * * [simplify]: iteration done : 5000 enodes (cost 8 ) 539.091 * * [simplify]: iteration 0 : 5 enodes (cost 5 ) 539.092 * * [simplify]: iteration 1 : 9 enodes (cost 5 ) 539.093 * * [simplify]: iteration 2 : 14 enodes (cost 5 ) 539.095 * * [simplify]: iteration 3 : 32 enodes (cost 5 ) 539.099 * * [simplify]: iteration 4 : 71 enodes (cost 5 ) 539.125 * * [simplify]: iteration 5 : 175 enodes (cost 5 ) 539.217 * * [simplify]: iteration 6 : 548 enodes (cost 5 ) 540.070 * * [simplify]: iteration 7 : 2169 enodes (cost 5 ) 542.393 * * [simplify]: iteration done : 5000 enodes (cost 5 ) 542.393 * * [simplify]: iteration 0 : 4 enodes (cost 4 ) 542.394 * * [simplify]: iteration 1 : 11 enodes (cost 2 ) 542.395 * * [simplify]: iteration 2 : 18 enodes (cost 2 ) 542.396 * * [simplify]: iteration 3 : 29 enodes (cost 2 ) 542.399 * * [simplify]: iteration 4 : 51 enodes (cost 2 ) 542.409 * * [simplify]: iteration 5 : 112 enodes (cost 2 ) 542.454 * * [simplify]: iteration 6 : 321 enodes (cost 2 ) 542.906 * * [simplify]: iteration 7 : 1250 enodes (cost 2 ) 545.528 * * [simplify]: iteration done : 5000 enodes (cost 2 ) 545.529 * * [simplify]: iteration 0 : 6 enodes (cost 9 ) 545.530 * * [simplify]: iteration 1 : 16 enodes (cost 9 ) 545.532 * * [simplify]: iteration 2 : 37 enodes (cost 5 ) 545.538 * * [simplify]: iteration 3 : 70 enodes (cost 5 ) 545.556 * * [simplify]: iteration 4 : 145 enodes (cost 5 ) 545.609 * * [simplify]: iteration 5 : 372 enodes (cost 5 ) 545.887 * * [simplify]: iteration 6 : 1199 enodes (cost 5 ) 548.613 * * [simplify]: iteration done : 5000 enodes (cost 5 ) 548.614 * * [simplify]: iteration 0 : 5 enodes (cost 5 ) 548.615 * * [simplify]: iteration 1 : 13 enodes (cost 2 ) 548.616 * * [simplify]: iteration 2 : 19 enodes (cost 2 ) 548.618 * * [simplify]: iteration 3 : 29 enodes (cost 2 ) 548.622 * * [simplify]: iteration 4 : 50 enodes (cost 2 ) 548.631 * * [simplify]: iteration 5 : 108 enodes (cost 2 ) 548.679 * * [simplify]: iteration 6 : 312 enodes (cost 2 ) 549.142 * * [simplify]: iteration 7 : 1238 enodes (cost 2 ) 551.512 * * [simplify]: iteration done : 5000 enodes (cost 2 ) 551.513 * * [simplify]: iteration 0 : 5 enodes (cost 5 ) 551.514 * * [simplify]: iteration 1 : 13 enodes (cost 5 ) 551.515 * * [simplify]: iteration 2 : 19 enodes (cost 5 ) 551.517 * * [simplify]: iteration 3 : 30 enodes (cost 5 ) 551.520 * * [simplify]: iteration 4 : 51 enodes (cost 5 ) 551.534 * * [simplify]: iteration 5 : 112 enodes (cost 5 ) 551.577 * * [simplify]: iteration 6 : 322 enodes (cost 5 ) 552.030 * * [simplify]: iteration 7 : 1253 enodes (cost 5 ) 554.450 * * [simplify]: iteration done : 5000 enodes (cost 5 ) 554.451 * * [simplify]: iteration 0 : 5 enodes (cost 5 ) 554.452 * * [simplify]: iteration 1 : 13 enodes (cost 5 ) 554.453 * * [simplify]: iteration 2 : 19 enodes (cost 5 ) 554.455 * * [simplify]: iteration 3 : 30 enodes (cost 5 ) 554.459 * * [simplify]: iteration 4 : 51 enodes (cost 5 ) 554.468 * * [simplify]: iteration 5 : 112 enodes (cost 5 ) 554.515 * * [simplify]: iteration 6 : 322 enodes (cost 5 ) 554.967 * * [simplify]: iteration 7 : 1253 enodes (cost 5 ) 557.345 * * [simplify]: iteration done : 5000 enodes (cost 5 ) 557.345 * * [simplify]: iteration 0 : 3 enodes (cost 3 ) 557.346 * * [simplify]: iteration 1 : 13 enodes (cost 1 ) 557.346 * * [simplify]: iteration done : 13 enodes (cost 1 ) 557.347 * * [simplify]: iteration 0 : 4 enodes (cost 4 ) 557.347 * * [simplify]: iteration 1 : 12 enodes (cost 4 ) 557.354 * * [simplify]: iteration 2 : 18 enodes (cost 4 ) 557.356 * * [simplify]: iteration 3 : 28 enodes (cost 4 ) 557.360 * * [simplify]: iteration 4 : 49 enodes (cost 4 ) 557.370 * * [simplify]: iteration 5 : 111 enodes (cost 4 ) 557.417 * * [simplify]: iteration 6 : 325 enodes (cost 4 ) 557.875 * * [simplify]: iteration 7 : 1243 enodes (cost 4 ) 560.162 * * [simplify]: iteration done : 5000 enodes (cost 4 ) 560.163 * * [simplify]: iteration 0 : 3 enodes (cost 5 ) 560.163 * * [simplify]: iteration done : 3 enodes (cost 5 ) 560.164 * * [simplify]: iteration 0 : 5 enodes (cost 5 ) 560.164 * * [simplify]: iteration 1 : 15 enodes (cost 5 ) 560.167 * * [simplify]: iteration 2 : 27 enodes (cost 5 ) 560.176 * * [simplify]: iteration 3 : 42 enodes (cost 5 ) 560.182 * * [simplify]: iteration 4 : 82 enodes (cost 5 ) 560.200 * * [simplify]: iteration 5 : 194 enodes (cost 5 ) 560.292 * * [simplify]: iteration 6 : 565 enodes (cost 5 ) 560.993 * * [simplify]: iteration 7 : 2161 enodes (cost 5 ) 562.880 * * [simplify]: iteration done : 5000 enodes (cost 5 ) 562.881 * * [simplify]: iteration 0 : 5 enodes (cost 5 ) 562.881 * * [simplify]: iteration 1 : 13 enodes (cost 5 ) 562.883 * * [simplify]: iteration 2 : 25 enodes (cost 5 ) 562.886 * * [simplify]: iteration 3 : 47 enodes (cost 5 ) 562.892 * * [simplify]: iteration 4 : 97 enodes (cost 5 ) 562.914 * * [simplify]: iteration 5 : 255 enodes (cost 5 ) 563.037 * * [simplify]: iteration 6 : 808 enodes (cost 5 ) 564.022 * * [simplify]: iteration 7 : 3372 enodes (cost 5 ) 565.185 * * [simplify]: iteration done : 5000 enodes (cost 5 ) 565.185 * * [simplify]: iteration 0 : 6 enodes (cost 11 ) 565.186 * * [simplify]: iteration 1 : 13 enodes (cost 5 ) 565.188 * * [simplify]: iteration 2 : 19 enodes (cost 5 ) 565.190 * * [simplify]: iteration 3 : 29 enodes (cost 5 ) 565.193 * * [simplify]: iteration 4 : 50 enodes (cost 5 ) 565.202 * * [simplify]: iteration 5 : 110 enodes (cost 5 ) 565.250 * * [simplify]: iteration 6 : 319 enodes (cost 5 ) 565.713 * * [simplify]: iteration 7 : 1251 enodes (cost 5 ) 568.080 * * [simplify]: iteration done : 5001 enodes (cost 5 ) 568.081 * * [simplify]: iteration 0 : 5 enodes (cost 5 ) 568.082 * * [simplify]: iteration 1 : 13 enodes (cost 2 ) 568.083 * * [simplify]: iteration 2 : 19 enodes (cost 2 ) 568.085 * * [simplify]: iteration 3 : 29 enodes (cost 2 ) 568.089 * * [simplify]: iteration 4 : 50 enodes (cost 2 ) 568.103 * * [simplify]: iteration 5 : 106 enodes (cost 2 ) 568.146 * * [simplify]: iteration 6 : 321 enodes (cost 2 ) 568.590 * * [simplify]: iteration 7 : 1236 enodes (cost 2 ) 570.975 * * [simplify]: iteration done : 5000 enodes (cost 2 ) 570.976 * * [simplify]: iteration 0 : 6 enodes (cost 14 ) 570.977 * * [simplify]: iteration 1 : 18 enodes (cost 9 ) 570.986 * * [simplify]: iteration 2 : 57 enodes (cost 6 ) 571.000 * * [simplify]: iteration 3 : 165 enodes (cost 6 ) 571.097 * * [simplify]: iteration 4 : 517 enodes (cost 6 ) 571.936 * * [simplify]: iteration 5 : 1868 enodes (cost 4 ) 575.631 * * [simplify]: iteration done : 5001 enodes (cost 4 ) 575.632 * * [simplify]: iteration 0 : 6 enodes (cost 9 ) 575.633 * * [simplify]: iteration 1 : 16 enodes (cost 9 ) 575.635 * * [simplify]: iteration 2 : 37 enodes (cost 5 ) 575.641 * * [simplify]: iteration 3 : 70 enodes (cost 5 ) 575.653 * * [simplify]: iteration 4 : 145 enodes (cost 5 ) 575.706 * * [simplify]: iteration 5 : 372 enodes (cost 5 ) 575.985 * * [simplify]: iteration 6 : 1199 enodes (cost 5 ) 578.678 * * [simplify]: iteration done : 5000 enodes (cost 5 ) 578.679 * * [simplify]: iteration 0 : 5 enodes (cost 5 ) 578.680 * * [simplify]: iteration 1 : 13 enodes (cost 2 ) 578.681 * * [simplify]: iteration 2 : 19 enodes (cost 2 ) 578.683 * * [simplify]: iteration 3 : 29 enodes (cost 2 ) 578.692 * * [simplify]: iteration 4 : 50 enodes (cost 2 ) 578.702 * * [simplify]: iteration 5 : 108 enodes (cost 2 ) 578.749 * * [simplify]: iteration 6 : 312 enodes (cost 2 ) 579.196 * * [simplify]: iteration 7 : 1238 enodes (cost 2 ) 581.557 * * [simplify]: iteration done : 5000 enodes (cost 2 ) 581.558 * * [simplify]: iteration 0 : 5 enodes (cost 5 ) 581.559 * * [simplify]: iteration 1 : 13 enodes (cost 5 ) 581.560 * * [simplify]: iteration 2 : 19 enodes (cost 5 ) 581.562 * * [simplify]: iteration 3 : 30 enodes (cost 5 ) 581.566 * * [simplify]: iteration 4 : 51 enodes (cost 5 ) 581.575 * * [simplify]: iteration 5 : 112 enodes (cost 5 ) 581.623 * * [simplify]: iteration 6 : 322 enodes (cost 5 ) 582.071 * * [simplify]: iteration 7 : 1253 enodes (cost 5 ) 584.470 * * [simplify]: iteration done : 5000 enodes (cost 5 ) 584.470 * * [simplify]: iteration 0 : 5 enodes (cost 5 ) 584.471 * * [simplify]: iteration 1 : 13 enodes (cost 5 ) 584.473 * * [simplify]: iteration 2 : 19 enodes (cost 5 ) 584.475 * * [simplify]: iteration 3 : 30 enodes (cost 5 ) 584.478 * * [simplify]: iteration 4 : 51 enodes (cost 5 ) 584.487 * * [simplify]: iteration 5 : 112 enodes (cost 5 ) 584.534 * * [simplify]: iteration 6 : 322 enodes (cost 5 ) 584.979 * * [simplify]: iteration 7 : 1253 enodes (cost 5 ) 587.374 * * [simplify]: iteration done : 5000 enodes (cost 5 ) 587.374 * * [simplify]: iteration 0 : 3 enodes (cost 3 ) 587.375 * * [simplify]: iteration 1 : 13 enodes (cost 1 ) 587.375 * * [simplify]: iteration done : 13 enodes (cost 1 ) 587.376 * * [simplify]: iteration 0 : 4 enodes (cost 4 ) 587.377 * * [simplify]: iteration 1 : 12 enodes (cost 4 ) 587.378 * * [simplify]: iteration 2 : 18 enodes (cost 4 ) 587.380 * * [simplify]: iteration 3 : 28 enodes (cost 4 ) 587.383 * * [simplify]: iteration 4 : 49 enodes (cost 4 ) 587.393 * * [simplify]: iteration 5 : 111 enodes (cost 4 ) 587.442 * * [simplify]: iteration 6 : 325 enodes (cost 4 ) 587.896 * * [simplify]: iteration 7 : 1243 enodes (cost 4 ) 590.211 * * [simplify]: iteration done : 5000 enodes (cost 4 ) 590.212 * * [simplify]: iteration 0 : 3 enodes (cost 5 ) 590.217 * * [simplify]: iteration done : 3 enodes (cost 5 ) 590.218 * * [simplify]: iteration 0 : 5 enodes (cost 5 ) 590.219 * * [simplify]: iteration 1 : 13 enodes (cost 5 ) 590.220 * * [simplify]: iteration 2 : 20 enodes (cost 5 ) 590.222 * * [simplify]: iteration 3 : 30 enodes (cost 5 ) 590.226 * * [simplify]: iteration 4 : 51 enodes (cost 5 ) 590.235 * * [simplify]: iteration 5 : 113 enodes (cost 5 ) 590.283 * * [simplify]: iteration 6 : 323 enodes (cost 5 ) 590.734 * * [simplify]: iteration 7 : 1246 enodes (cost 5 ) 593.093 * * [simplify]: iteration done : 5000 enodes (cost 5 ) 593.094 * * [simplify]: iteration 0 : 5 enodes (cost 5 ) 593.094 * * [simplify]: iteration 1 : 13 enodes (cost 5 ) 593.096 * * [simplify]: iteration 2 : 20 enodes (cost 5 ) 593.103 * * [simplify]: iteration 3 : 30 enodes (cost 5 ) 593.107 * * [simplify]: iteration 4 : 51 enodes (cost 5 ) 593.116 * * [simplify]: iteration 5 : 113 enodes (cost 5 ) 593.163 * * [simplify]: iteration 6 : 323 enodes (cost 5 ) 593.613 * * [simplify]: iteration 7 : 1246 enodes (cost 5 ) 595.966 * * [simplify]: iteration done : 5000 enodes (cost 5 ) 595.967 * * [simplify]: iteration 0 : 6 enodes (cost 6 ) 595.968 * * [simplify]: iteration 1 : 11 enodes (cost 4 ) 595.969 * * [simplify]: iteration 2 : 17 enodes (cost 4 ) 595.970 * * [simplify]: iteration 3 : 27 enodes (cost 4 ) 595.973 * * [simplify]: iteration 4 : 50 enodes (cost 4 ) 595.981 * * [simplify]: iteration 5 : 112 enodes (cost 4 ) 596.029 * * [simplify]: iteration 6 : 329 enodes (cost 4 ) 596.489 * * [simplify]: iteration 7 : 1255 enodes (cost 4 ) 598.848 * * [simplify]: iteration done : 5001 enodes (cost 4 ) 598.849 * * [simplify]: iteration 0 : 6 enodes (cost 6 ) 598.850 * * [simplify]: iteration 1 : 11 enodes (cost 4 ) 598.851 * * [simplify]: iteration 2 : 17 enodes (cost 4 ) 598.852 * * [simplify]: iteration 3 : 27 enodes (cost 4 ) 598.855 * * [simplify]: iteration 4 : 50 enodes (cost 4 ) 598.869 * * [simplify]: iteration 5 : 112 enodes (cost 4 ) 598.912 * * [simplify]: iteration 6 : 329 enodes (cost 4 ) 599.394 * * [simplify]: iteration 7 : 1255 enodes (cost 4 ) 601.760 * * [simplify]: iteration done : 5001 enodes (cost 4 ) 601.761 * * [simplify]: iteration 0 : 5 enodes (cost 7 ) 601.762 * * [simplify]: iteration 1 : 12 enodes (cost 7 ) 601.763 * * [simplify]: iteration 2 : 13 enodes (cost 7 ) 601.765 * * [simplify]: iteration done : 13 enodes (cost 7 ) 601.765 * * [simplify]: iteration 0 : 7 enodes (cost 9 ) 601.766 * * [simplify]: iteration 1 : 9 enodes (cost 9 ) 601.767 * * [simplify]: iteration done : 9 enodes (cost 9 ) 601.767 * * [simplify]: iteration 0 : 6 enodes (cost 8 ) 601.768 * * [simplify]: iteration 1 : 16 enodes (cost 8 ) 601.770 * * [simplify]: iteration 2 : 18 enodes (cost 8 ) 601.772 * * [simplify]: iteration done : 18 enodes (cost 8 ) 601.773 * * [simplify]: iteration 0 : 6 enodes (cost 8 ) 601.774 * * [simplify]: iteration 1 : 15 enodes (cost 8 ) 601.776 * * [simplify]: iteration 2 : 25 enodes (cost 8 ) 601.779 * * [simplify]: iteration 3 : 40 enodes (cost 8 ) 601.785 * * [simplify]: iteration 4 : 70 enodes (cost 8 ) 601.796 * * [simplify]: iteration 5 : 164 enodes (cost 8 ) 601.862 * * [simplify]: iteration 6 : 405 enodes (cost 8 ) 602.128 * * [simplify]: iteration 7 : 1281 enodes (cost 8 ) 603.706 * * [simplify]: iteration done : 5000 enodes (cost 8 ) 603.706 * * [simplify]: iteration 0 : 9 enodes (cost 23 ) 603.708 * * [simplify]: iteration 1 : 29 enodes (cost 23 ) 603.714 * * [simplify]: iteration 2 : 107 enodes (cost 11 ) 603.752 * * [simplify]: iteration 3 : 319 enodes (cost 11 ) 603.956 * * [simplify]: iteration 4 : 1028 enodes (cost 9 ) 605.267 * * [simplify]: iteration 5 : 3569 enodes (cost 9 ) 606.946 * * [simplify]: iteration done : 5000 enodes (cost 9 ) 606.947 * * [simplify]: iteration 0 : 7 enodes (cost 17 ) 606.948 * * [simplify]: iteration 1 : 14 enodes (cost 17 ) 606.949 * * [simplify]: iteration 2 : 15 enodes (cost 17 ) 606.951 * * [simplify]: iteration done : 15 enodes (cost 17 ) 606.952 * * [simplify]: iteration 0 : 6 enodes (cost 8 ) 606.952 * * [simplify]: iteration 1 : 13 enodes (cost 8 ) 606.954 * * [simplify]: iteration 2 : 14 enodes (cost 8 ) 606.955 * * [simplify]: iteration done : 14 enodes (cost 8 ) 606.956 * * [simplify]: iteration 0 : 7 enodes (cost 23 ) 606.957 * * [simplify]: iteration 1 : 23 enodes (cost 23 ) 606.962 * * [simplify]: iteration 2 : 90 enodes (cost 9 ) 606.995 * * [simplify]: iteration 3 : 287 enodes (cost 9 ) 607.182 * * [simplify]: iteration 4 : 735 enodes (cost 9 ) 607.976 * * [simplify]: iteration 5 : 2081 enodes (cost 9 ) 609.788 * * [simplify]: iteration done : 5000 enodes (cost 9 ) 609.789 * * [simplify]: iteration 0 : 6 enodes (cost 8 ) 609.790 * * [simplify]: iteration 1 : 13 enodes (cost 8 ) 609.791 * * [simplify]: iteration 2 : 14 enodes (cost 8 ) 609.793 * * [simplify]: iteration done : 14 enodes (cost 8 ) 609.793 * * [simplify]: iteration 0 : 6 enodes (cost 8 ) 609.794 * * [simplify]: iteration 1 : 13 enodes (cost 8 ) 609.796 * * [simplify]: iteration 2 : 14 enodes (cost 8 ) 609.797 * * [simplify]: iteration done : 14 enodes (cost 8 ) 609.798 * * [simplify]: iteration 0 : 7 enodes (cost 9 ) 609.799 * * [simplify]: iteration 1 : 9 enodes (cost 9 ) 609.800 * * [simplify]: iteration done : 9 enodes (cost 9 ) 609.800 * * [simplify]: iteration 0 : 7 enodes (cost 9 ) 609.801 * * [simplify]: iteration 1 : 9 enodes (cost 9 ) 609.802 * * [simplify]: iteration done : 9 enodes (cost 9 ) 609.802 * * [simplify]: iteration 0 : 3 enodes (cost 5 ) 609.803 * * [simplify]: iteration done : 3 enodes (cost 5 ) 609.803 * * [simplify]: iteration 0 : 4 enodes (cost 4 ) 609.804 * * [simplify]: iteration 1 : 5 enodes (cost 4 ) 609.804 * * [simplify]: iteration done : 5 enodes (cost 4 ) 609.805 * * [simplify]: iteration 0 : 3 enodes (cost 5 ) 609.805 * * [simplify]: iteration done : 3 enodes (cost 5 ) 609.806 * * [simplify]: iteration 0 : 4 enodes (cost 4 ) 609.807 * * [simplify]: iteration 1 : 5 enodes (cost 4 ) 609.807 * * [simplify]: iteration done : 5 enodes (cost 4 ) 609.808 * * [simplify]: iteration 0 : 7 enodes (cost 14 ) 609.809 * * [simplify]: iteration 1 : 11 enodes (cost 14 ) 609.810 * * [simplify]: iteration 2 : 13 enodes (cost 14 ) 609.812 * * [simplify]: iteration done : 13 enodes (cost 14 ) 609.812 * * [simplify]: iteration 0 : 6 enodes (cost 8 ) 609.813 * * [simplify]: iteration 1 : 8 enodes (cost 8 ) 609.814 * * [simplify]: iteration done : 8 enodes (cost 8 ) 609.815 * * [simplify]: iteration 0 : 4 enodes (cost 4 ) 609.815 * * [simplify]: iteration 1 : 7 enodes (cost 2 ) 609.816 * * [simplify]: iteration 2 : 10 enodes (cost 2 ) 609.816 * * [simplify]: iteration done : 10 enodes (cost 2 ) 609.817 * * [simplify]: iteration 0 : 4 enodes (cost 4 ) 609.818 * * [simplify]: iteration 1 : 7 enodes (cost 2 ) 609.819 * * [simplify]: iteration 2 : 10 enodes (cost 2 ) 609.819 * * [simplify]: iteration done : 10 enodes (cost 2 ) 609.820 * * [simplify]: iteration 0 : 6 enodes (cost 8 ) 609.821 * * [simplify]: iteration 1 : 14 enodes (cost 8 ) 609.822 * * [simplify]: iteration 2 : 15 enodes (cost 8 ) 609.828 * * [simplify]: iteration done : 15 enodes (cost 8 ) 609.829 * * [simplify]: iteration 0 : 6 enodes (cost 8 ) 609.830 * * [simplify]: iteration 1 : 14 enodes (cost 8 ) 609.831 * * [simplify]: iteration 2 : 15 enodes (cost 8 ) 609.833 * * [simplify]: iteration done : 15 enodes (cost 8 ) 609.834 * * [simplify]: iteration 0 : 5 enodes (cost 7 ) 609.835 * * [simplify]: iteration 1 : 12 enodes (cost 7 ) 609.836 * * [simplify]: iteration 2 : 13 enodes (cost 7 ) 609.838 * * [simplify]: iteration done : 13 enodes (cost 7 ) 609.838 * * [simplify]: iteration 0 : 8 enodes (cost 11 ) 609.839 * * [simplify]: iteration 1 : 29 enodes (cost 11 ) 609.844 * * [simplify]: iteration 2 : 60 enodes (cost 11 ) 609.853 * * [simplify]: iteration 3 : 104 enodes (cost 11 ) 609.874 * * [simplify]: iteration 4 : 203 enodes (cost 11 ) 609.948 * * [simplify]: iteration 5 : 530 enodes (cost 11 ) 610.408 * * [simplify]: iteration 6 : 1809 enodes (cost 11 ) 611.922 * * [simplify]: iteration done : 5000 enodes (cost 11 ) 611.923 * * [simplify]: iteration 0 : 7 enodes (cost 12 ) 611.924 * * [simplify]: iteration 1 : 13 enodes (cost 12 ) 611.926 * * [simplify]: iteration 2 : 30 enodes (cost 12 ) 611.931 * * [simplify]: iteration 3 : 70 enodes (cost 12 ) 611.946 * * [simplify]: iteration 4 : 142 enodes (cost 11 ) 611.985 * * [simplify]: iteration 5 : 238 enodes (cost 11 ) 612.071 * * [simplify]: iteration 6 : 435 enodes (cost 11 ) 612.358 * * [simplify]: iteration 7 : 1135 enodes (cost 11 ) 615.778 * * [simplify]: iteration done : 5000 enodes (cost 11 ) 615.779 * * [simplify]: iteration 0 : 15 enodes (cost 17 ) 615.781 * * [simplify]: iteration 1 : 35 enodes (cost 17 ) 615.788 * * [simplify]: iteration 2 : 92 enodes (cost 17 ) 615.802 * * [simplify]: iteration 3 : 193 enodes (cost 17 ) 615.866 * * [simplify]: iteration 4 : 496 enodes (cost 17 ) 616.160 * * [simplify]: iteration 5 : 1268 enodes (cost 17 ) 617.813 * * [simplify]: iteration 6 : 3918 enodes (cost 17 ) 619.776 * * [simplify]: iteration done : 5000 enodes (cost 17 ) 619.777 * * [simplify]: iteration 0 : 6 enodes (cost 6 ) 619.777 * * [simplify]: iteration 1 : 16 enodes (cost 6 ) 619.779 * * [simplify]: iteration 2 : 32 enodes (cost 6 ) 619.784 * * [simplify]: iteration 3 : 53 enodes (cost 6 ) 619.792 * * [simplify]: iteration 4 : 95 enodes (cost 6 ) 619.823 * * [simplify]: iteration 5 : 229 enodes (cost 6 ) 620.006 * * [simplify]: iteration 6 : 746 enodes (cost 6 ) 622.133 * * [simplify]: iteration 7 : 3067 enodes (cost 6 ) 625.718 * * [simplify]: iteration done : 5000 enodes (cost 6 ) 625.719 * * [simplify]: iteration 0 : 6 enodes (cost 6 ) 625.719 * * [simplify]: iteration 1 : 16 enodes (cost 6 ) 625.721 * * [simplify]: iteration 2 : 32 enodes (cost 6 ) 625.726 * * [simplify]: iteration 3 : 53 enodes (cost 6 ) 625.735 * * [simplify]: iteration 4 : 95 enodes (cost 6 ) 625.764 * * [simplify]: iteration 5 : 229 enodes (cost 6 ) 625.943 * * [simplify]: iteration 6 : 746 enodes (cost 6 ) 628.072 * * [simplify]: iteration 7 : 3067 enodes (cost 6 ) 631.928 * * [simplify]: iteration done : 5000 enodes (cost 6 ) 631.928 * * [simplify]: iteration 0 : 12 enodes (cost 13 ) 631.930 * * [simplify]: iteration 1 : 27 enodes (cost 13 ) 631.936 * * [simplify]: iteration 2 : 74 enodes (cost 13 ) 631.949 * * [simplify]: iteration 3 : 119 enodes (cost 13 ) 631.970 * * [simplify]: iteration 4 : 163 enodes (cost 13 ) 631.995 * * [simplify]: iteration 5 : 209 enodes (cost 13 ) 632.032 * * [simplify]: iteration 6 : 331 enodes (cost 13 ) 632.151 * * [simplify]: iteration 7 : 786 enodes (cost 13 ) 633.318 * * [simplify]: iteration 8 : 2600 enodes (cost 13 ) 634.913 * * [simplify]: iteration done : 5000 enodes (cost 13 ) 634.914 * * [simplify]: iteration 0 : 4 enodes (cost 4 ) 634.914 * * [simplify]: iteration 1 : 5 enodes (cost 4 ) 634.915 * * [simplify]: iteration done : 5 enodes (cost 4 ) 634.915 * * [simplify]: iteration 0 : 4 enodes (cost 4 ) 634.916 * * [simplify]: iteration 1 : 5 enodes (cost 4 ) 634.916 * * [simplify]: iteration done : 5 enodes (cost 4 ) 634.917 * * [simplify]: iteration 0 : 12 enodes (cost 13 ) 634.918 * * [simplify]: iteration 1 : 28 enodes (cost 13 ) 634.923 * * [simplify]: iteration 2 : 74 enodes (cost 13 ) 634.938 * * [simplify]: iteration 3 : 187 enodes (cost 13 ) 635.058 * * [simplify]: iteration 4 : 552 enodes (cost 13 ) 635.324 * * [simplify]: iteration 5 : 1273 enodes (cost 13 ) 637.398 * * [simplify]: iteration 6 : 4407 enodes (cost 13 ) 639.975 * * [simplify]: iteration done : 5001 enodes (cost 13 ) 639.976 * * [simplify]: iteration 0 : 4 enodes (cost 4 ) 639.976 * * [simplify]: iteration 1 : 12 enodes (cost 4 ) 639.978 * * [simplify]: iteration 2 : 18 enodes (cost 4 ) 639.980 * * [simplify]: iteration 3 : 28 enodes (cost 4 ) 639.983 * * [simplify]: iteration 4 : 49 enodes (cost 4 ) 639.992 * * [simplify]: iteration 5 : 111 enodes (cost 4 ) 640.040 * * [simplify]: iteration 6 : 325 enodes (cost 4 ) 640.504 * * [simplify]: iteration 7 : 1243 enodes (cost 4 ) 642.847 * * [simplify]: iteration done : 5000 enodes (cost 4 ) 642.848 * * [simplify]: iteration 0 : 4 enodes (cost 4 ) 642.849 * * [simplify]: iteration 1 : 12 enodes (cost 4 ) 642.850 * * [simplify]: iteration 2 : 18 enodes (cost 4 ) 642.852 * * [simplify]: iteration 3 : 28 enodes (cost 4 ) 642.856 * * [simplify]: iteration 4 : 49 enodes (cost 4 ) 642.865 * * [simplify]: iteration 5 : 111 enodes (cost 4 ) 642.913 * * [simplify]: iteration 6 : 325 enodes (cost 4 ) 643.378 * * [simplify]: iteration 7 : 1243 enodes (cost 4 ) 645.711 * * [simplify]: iteration done : 5000 enodes (cost 4 ) 645.712 * * [simplify]: iteration 0 : 12 enodes (cost 13 ) 645.714 * * [simplify]: iteration 1 : 27 enodes (cost 13 ) 645.719 * * [simplify]: iteration 2 : 74 enodes (cost 13 ) 645.729 * * [simplify]: iteration 3 : 119 enodes (cost 13 ) 645.755 * * [simplify]: iteration 4 : 163 enodes (cost 13 ) 645.779 * * [simplify]: iteration 5 : 209 enodes (cost 13 ) 645.818 * * [simplify]: iteration 6 : 330 enodes (cost 13 ) 645.931 * * [simplify]: iteration 7 : 779 enodes (cost 13 ) 647.165 * * [simplify]: iteration 8 : 2603 enodes (cost 13 ) 649.125 * * [simplify]: iteration done : 5000 enodes (cost 13 ) 649.125 * * [simplify]: iteration 0 : 5 enodes (cost 7 ) 649.126 * * [simplify]: iteration 1 : 12 enodes (cost 7 ) 649.128 * * [simplify]: iteration 2 : 13 enodes (cost 7 ) 649.129 * * [simplify]: iteration done : 13 enodes (cost 7 ) 649.130 * * [simplify]: iteration 0 : 5 enodes (cost 7 ) 649.131 * * [simplify]: iteration 1 : 12 enodes (cost 7 ) 649.132 * * [simplify]: iteration 2 : 13 enodes (cost 7 ) 649.139 * * [simplify]: iteration done : 13 enodes (cost 7 ) 649.141 * [simplify]: Simplified to: (exp (- (pow 1.0 3) (pow (cos x) 3))) (log (- (pow 1.0 3) (pow (cos x) 3))) (exp (- (pow 1.0 3) (pow (cos x) 3))) (* (cbrt (- (pow 1.0 3) (pow (cos x) 3))) (cbrt (- (pow 1.0 3) (pow (cos x) 3)))) (cbrt (- (pow 1.0 3) (pow (cos x) 3))) (pow (- (pow 1.0 3) (pow (cos x) 3)) 3) (sqrt (- (pow 1.0 3) (pow (cos x) 3))) (sqrt (- (pow 1.0 3) (pow (cos x) 3))) (+ (* 1.0 1.0) (* (cos x) (+ (cos x) 1.0))) (- 1.0 (cos x)) (- (pow (pow 1.0 3) 3) (pow (pow (cos x) 3) 3)) (+ (pow (* (cos x) 1.0) 3) (+ (pow 1.0 6) (pow (cos x) 6))) (neg (pow (cos x) 3)) (- (pow 1.0 6) (pow (cos x) 6)) (+ (pow 1.0 3) (pow (cos x) 3)) (+ (pow (sqrt 1.0) 3) (pow (sqrt (cos x)) 3)) (- (pow (sqrt 1.0) 3) (pow (sqrt (cos x)) 3)) (+ (pow (sqrt 1.0) 3) (pow (sqrt (cos x)) 3)) (- (pow (sqrt 1.0) 3) (pow (sqrt (cos x)) 3)) (+ (pow (sqrt 1.0) 3) (sqrt (pow (cos x) 3))) (- (pow (sqrt 1.0) 3) (sqrt (pow (cos x) 3))) (+ (pow (cos x) 3/2) (pow (sqrt 1.0) 3)) (- (pow (sqrt 1.0) 3) (pow (cos x) 3/2)) (+ (pow (sqrt 1.0) 3) (pow (sqrt (cos x)) 3)) (- (pow (sqrt 1.0) 3) (pow (sqrt (cos x)) 3)) (+ (pow (sqrt 1.0) 3) (pow (sqrt (cos x)) 3)) (- (pow (sqrt 1.0) 3) (pow (sqrt (cos x)) 3)) (+ (pow (sqrt 1.0) 3) (sqrt (pow (cos x) 3))) (- (pow (sqrt 1.0) 3) (sqrt (pow (cos x) 3))) (+ (pow (cos x) 3/2) (pow (sqrt 1.0) 3)) (- (pow (sqrt 1.0) 3) (pow (cos x) 3/2)) (+ (sqrt (pow 1.0 3)) (pow (sqrt (cos x)) 3)) (- (sqrt (pow 1.0 3)) (pow (sqrt (cos x)) 3)) (+ (sqrt (pow 1.0 3)) (pow (sqrt (cos x)) 3)) (- (sqrt (pow 1.0 3)) (pow (sqrt (cos x)) 3)) (+ (sqrt (pow 1.0 3)) (sqrt (pow (cos x) 3))) (- (sqrt (pow 1.0 3)) (sqrt (pow (cos x) 3))) (+ (pow (cos x) 3/2) (sqrt (pow 1.0 3))) (- (sqrt (pow 1.0 3)) (pow (cos x) 3/2)) (+ (pow 1.0 3/2) (pow (sqrt (cos x)) 3)) (- (pow 1.0 3/2) (pow (sqrt (cos x)) 3)) (+ (pow 1.0 3/2) (pow (sqrt (cos x)) 3)) (- (pow 1.0 3/2) (pow (sqrt (cos x)) 3)) (+ (pow 1.0 3/2) (sqrt (pow (cos x) 3))) (- (pow 1.0 3/2) (sqrt (pow (cos x) 3))) (+ (pow (cos x) 3/2) (pow 1.0 3/2)) (- (pow 1.0 3/2) (pow (cos x) 3/2)) (- (pow 1.0 3) (pow (cos x) 3)) (- (pow 1.0 3) (pow (cos x) 3)) (- (pow 1.0 3) (pow (cos x) 3)) (- (pow 1.0 3) (pow (cos x) 3)) (- (pow 1.0 3) (pow (cos x) 3)) (neg (pow (cos x) 3)) (exp (+ (cos x) 1.0)) (log (+ (cos x) 1.0)) (exp (+ (cos x) 1.0)) (* (cbrt (+ (cos x) 1.0)) (cbrt (+ (cos x) 1.0))) (cbrt (+ (cos x) 1.0)) (pow (+ (cos x) 1.0) 3) (sqrt (+ (cos x) 1.0)) (sqrt (+ (cos x) 1.0)) (+ (pow (cos x) 3) (pow 1.0 3)) (- (* 1.0 1.0) (* (cos x) (- 1.0 (cos x)))) (* (- (cos x) 1.0) (+ (cos x) 1.0)) (- (cos x) 1.0) (+ (cos x) 1.0) (* (log (cos x)) 3) (* (log (cos x)) 3) 3 (pow (cos x) (* (cbrt 3) (cbrt 3))) (pow (cos x) (sqrt 3)) (cos x) (pow (cbrt (cos x)) 6) (cos x) (pow (sqrt (cos x)) 3) (pow (sqrt (cos x)) 3) 1 (pow (cos x) 3) (* (cos x) (cos x)) (log (pow (cos x) 3)) (exp (pow (cos x) 3)) (* (cos x) (cos x)) (cos x) (pow (cos x) 9) (pow (cbrt (cos x)) 6) (cos x) (pow (sqrt (cos x)) 3) (pow (sqrt (cos x)) 3) 1 (pow (cos x) 3) (* (cos x) (cos x)) (sqrt (pow (cos x) 3)) (sqrt (pow (cos x) 3)) (pow (cos x) 3/2) (pow (cos x) 3/2) (* (cos x) (+ (cos x) 1.0)) (+ (log (cos x)) (log (+ (cos x) 1.0))) (log (* (cos x) (+ (cos x) 1.0))) (exp (* (cos x) (+ (cos x) 1.0))) (pow (* (+ (cos x) 1.0) (cos x)) 3) (* (cbrt (* (cos x) (+ (cos x) 1.0))) (cbrt (* (cos x) (+ (cos x) 1.0)))) (cbrt (* (cos x) (+ (cos x) 1.0))) (pow (* (cos x) (+ (cos x) 1.0)) 3) (sqrt (* (cos x) (+ (cos x) 1.0))) (sqrt (* (cos x) (+ (cos x) 1.0))) (* (sqrt (cos x)) (sqrt (+ (cos x) 1.0))) (* (sqrt (cos x)) (sqrt (+ (cos x) 1.0))) (* (cos x) (cos x)) (* (cos x) 1.0) (* (cos x) (cos x)) (* 1.0 (cos x)) (* (cos x) (* (cbrt (+ (cos x) 1.0)) (cbrt (+ (cos x) 1.0)))) (* (cos x) (sqrt (+ (cos x) 1.0))) (cos x) (cos x) (* (cbrt (cos x)) (+ (cos x) 1.0)) (* (sqrt (cos x)) (+ (cos x) 1.0)) (* (cos x) (+ (cos x) 1.0)) (* (cos x) (+ (pow (cos x) 3) (pow 1.0 3))) (- (pow (cos x) 3) (* (* 1.0 1.0) (cos x))) (- (+ (* 3/2 (pow x 2)) (* 61/240 (pow x 6))) (* 7/8 (pow x 4))) (- 1.0 (pow (cos x) 3)) (- 1.0 (pow (cos x) 3)) (- (+ 2.0 (* 1/24 (pow x 4))) (* 1/2 (pow x 2))) (+ (cos x) 1.0) (+ (cos x) 1.0) (- (+ 1 (* 7/8 (pow x 4))) (* 3/2 (pow x 2))) (pow (cos x) 3) (pow (cos x) 3) (- (+ 2.0 (* 0.375 (pow x 4))) (* 1.5 (pow x 2))) (* (cos x) (+ (cos x) 1.0)) (* (cos x) (+ (cos x) 1.0)) 649.142 * * * [progress]: adding candidates to table 649.315 * [progress]: [Phase 3 of 3] Extracting. 649.315 * * [regime]: Finding splitpoints for: (# # # # # # # # # # # # # #) 649.318 * * * [regime-changes]: Trying 2 branch expressions: ((/ (- 1.0 (cos x)) (sin x)) x) 649.318 * * * * [regimes]: Trying to branch on (/ (- 1.0 (cos x)) (sin x)) from (# # # # # # # # # # # # # #) 649.417 * * * * [regimes]: Trying to branch on x from (# # # # # # # # # # # # # #) 649.514 * * * [regime]: Found split indices: #