0.001 * [progress]: [Phase 1 of 3] Setting up. 0.001 * * * [progress]: [1/2] Preparing points 0.018 * * * [progress]: [2/2] Setting up program. 0.022 * [progress]: [Phase 2 of 3] Improving. 0.022 * * * * [progress]: [ 1 / 1 ] simplifiying candidate # 0.022 * [simplify]: Simplifying (/ 2 (+ (exp x) (exp (- x)))) 0.022 * * [simplify]: iters left: 6 (7 enodes) 0.026 * * [simplify]: iters left: 5 (24 enodes) 0.033 * * [simplify]: iters left: 4 (28 enodes) 0.042 * * [simplify]: iters left: 3 (30 enodes) 0.050 * * [simplify]: Extracting #0: cost 1 inf + 0 0.050 * * [simplify]: Extracting #1: cost 4 inf + 0 0.051 * * [simplify]: Extracting #2: cost 6 inf + 1 0.051 * * [simplify]: Extracting #3: cost 11 inf + 1 0.051 * * [simplify]: Extracting #4: cost 9 inf + 44 0.051 * * [simplify]: Extracting #5: cost 3 inf + 670 0.051 * * [simplify]: Extracting #6: cost 1 inf + 1153 0.052 * * [simplify]: Extracting #7: cost 0 inf + 1415 0.052 * [simplify]: Simplified to (/ 2 (+ (exp x) (exp (- x)))) 0.052 * [simplify]: Simplified (2) to (λ (x) (/ 2 (+ (exp x) (exp (- x))))) 0.057 * * [progress]: iteration 1 / 4 0.057 * * * [progress]: picking best candidate 0.061 * * * * [pick]: Picked # 0.061 * * * [progress]: localizing error 0.093 * * * [progress]: generating rewritten candidates 0.094 * * * * [progress]: [ 1 / 1 ] rewriting at (2) 0.124 * * * [progress]: generating series expansions 0.124 * * * * [progress]: [ 1 / 1 ] generating series at (2) 0.125 * [backup-simplify]: Simplify (/ 2 (+ (exp x) (exp (- x)))) into (/ 2 (+ (exp x) (exp (- x)))) 0.125 * [approximate]: Taking taylor expansion of (/ 2 (+ (exp x) (exp (- x)))) in (x) around 0 0.125 * [taylor]: Taking taylor expansion of (/ 2 (+ (exp x) (exp (- x)))) in x 0.125 * [taylor]: Taking taylor expansion of 2 in x 0.125 * [backup-simplify]: Simplify 2 into 2 0.125 * [taylor]: Taking taylor expansion of (+ (exp x) (exp (- x))) in x 0.125 * [taylor]: Taking taylor expansion of (exp x) in x 0.125 * [taylor]: Taking taylor expansion of x in x 0.125 * [backup-simplify]: Simplify 0 into 0 0.125 * [backup-simplify]: Simplify 1 into 1 0.125 * [backup-simplify]: Simplify (exp 0) into 1 0.125 * [taylor]: Taking taylor expansion of (exp (- x)) in x 0.125 * [taylor]: Taking taylor expansion of (- x) in x 0.125 * [taylor]: Taking taylor expansion of x in x 0.125 * [backup-simplify]: Simplify 0 into 0 0.125 * [backup-simplify]: Simplify 1 into 1 0.126 * [backup-simplify]: Simplify (- 0) into 0 0.126 * [backup-simplify]: Simplify (- 1) into -1 0.126 * [backup-simplify]: Simplify (exp 0) into 1 0.127 * [backup-simplify]: Simplify (+ 1 1) into 2 0.127 * [backup-simplify]: Simplify (/ 2 2) into 1 0.127 * [taylor]: Taking taylor expansion of (/ 2 (+ (exp x) (exp (- x)))) in x 0.127 * [taylor]: Taking taylor expansion of 2 in x 0.127 * [backup-simplify]: Simplify 2 into 2 0.127 * [taylor]: Taking taylor expansion of (+ (exp x) (exp (- x))) in x 0.128 * [taylor]: Taking taylor expansion of (exp x) in x 0.128 * [taylor]: Taking taylor expansion of x in x 0.128 * [backup-simplify]: Simplify 0 into 0 0.128 * [backup-simplify]: Simplify 1 into 1 0.128 * [backup-simplify]: Simplify (exp 0) into 1 0.128 * [taylor]: Taking taylor expansion of (exp (- x)) in x 0.128 * [taylor]: Taking taylor expansion of (- x) in x 0.128 * [taylor]: Taking taylor expansion of x in x 0.128 * [backup-simplify]: Simplify 0 into 0 0.128 * [backup-simplify]: Simplify 1 into 1 0.128 * [backup-simplify]: Simplify (- 0) into 0 0.128 * [backup-simplify]: Simplify (- 1) into -1 0.128 * [backup-simplify]: Simplify (exp 0) into 1 0.129 * [backup-simplify]: Simplify (+ 1 1) into 2 0.129 * [backup-simplify]: Simplify (/ 2 2) into 1 0.129 * [backup-simplify]: Simplify 1 into 1 0.131 * [backup-simplify]: Simplify (* (exp 0) (+ (* (/ (pow 1 1) 1)))) into 1 0.132 * [backup-simplify]: Simplify (- 1) into -1 0.133 * [backup-simplify]: Simplify (* (exp 0) (+ (* (/ (pow -1 1) 1)))) into -1 0.133 * [backup-simplify]: Simplify (+ 1 -1) into 0 0.134 * [backup-simplify]: Simplify (- (/ 0 2) (+ (* 1 (/ 0 2)))) into 0 0.134 * [backup-simplify]: Simplify 0 into 0 0.136 * [backup-simplify]: Simplify (* (exp 0) (+ (* (/ (pow 1 2) 2)) (* (/ (pow 0 1) 1)))) into 1/2 0.136 * [backup-simplify]: Simplify (- 1) into -1 0.137 * [backup-simplify]: Simplify (- 0) into 0 0.138 * [backup-simplify]: Simplify (* (exp 0) (+ (* (/ (pow -1 2) 2)) (* (/ (pow 0 1) 1)))) into 1/2 0.139 * [backup-simplify]: Simplify (+ 1/2 1/2) into 1 0.140 * [backup-simplify]: Simplify (- (/ 0 2) (+ (* 1 (/ 1 2)) (* 0 (/ 0 2)))) into -1/2 0.140 * [backup-simplify]: Simplify -1/2 into -1/2 0.143 * [backup-simplify]: Simplify (* (exp 0) (+ (* (/ (pow 1 3) 6)) (* (/ (pow 1 1) 1) (/ (pow 0 1) 1)) (* (/ (pow 0 1) 1)))) into 1/6 0.143 * [backup-simplify]: Simplify (- 1) into -1 0.144 * [backup-simplify]: Simplify (- 1) into -1 0.144 * [backup-simplify]: Simplify (- 0) into 0 0.144 * [backup-simplify]: Simplify (- 0) into 0 0.147 * [backup-simplify]: Simplify (* (exp 0) (+ (* (/ (pow -1 3) 6)) (* (/ (pow -1 1) 1) (/ (pow 0 1) 1)) (* (/ (pow 0 1) 1)))) into -1/6 0.147 * [backup-simplify]: Simplify (+ 1/6 -1/6) into 0 0.149 * [backup-simplify]: Simplify (- (/ 0 2) (+ (* 1 (/ 0 2)) (* 0 (/ 1 2)) (* -1/2 (/ 0 2)))) into 0 0.149 * [backup-simplify]: Simplify 0 into 0 0.153 * [backup-simplify]: Simplify (* (exp 0) (+ (* (/ (pow 1 4) 24)) (* (/ (pow 1 2) 2) (/ (pow 0 1) 1)) (* (/ (pow 1 1) 1) (/ (pow 0 1) 1)) (* (/ (pow 0 2) 2)) (* (/ (pow 0 1) 1)))) into 1/24 0.154 * [backup-simplify]: Simplify (- 1) into -1 0.154 * [backup-simplify]: Simplify (- 1) into -1 0.155 * [backup-simplify]: Simplify (- 0) into 0 0.155 * [backup-simplify]: Simplify (- 1) into -1 0.156 * [backup-simplify]: Simplify (- 0) into 0 0.156 * [backup-simplify]: Simplify (- 0) into 0 0.156 * [backup-simplify]: Simplify (- 0) into 0 0.159 * [backup-simplify]: Simplify (* (exp 0) (+ (* (/ (pow -1 4) 24)) (* (/ (pow -1 2) 2) (/ (pow 0 1) 1)) (* (/ (pow -1 1) 1) (/ (pow 0 1) 1)) (* (/ (pow 0 2) 2)) (* (/ (pow 0 1) 1)))) into 1/24 0.159 * [backup-simplify]: Simplify (+ 1/24 1/24) into 1/12 0.160 * [backup-simplify]: Simplify (- (/ 0 2) (+ (* 1 (/ 1/12 2)) (* 0 (/ 0 2)) (* -1/2 (/ 1 2)) (* 0 (/ 0 2)))) into 5/24 0.160 * [backup-simplify]: Simplify 5/24 into 5/24 0.160 * [backup-simplify]: Simplify (+ (* 5/24 (pow x 4)) (+ (* -1/2 (pow x 2)) 1)) into (- (+ (* 5/24 (pow x 4)) 1) (* 1/2 (pow x 2))) 0.160 * [backup-simplify]: Simplify (/ 2 (+ (exp (/ 1 x)) (exp (- (/ 1 x))))) into (/ 2 (+ (exp (/ 1 x)) (exp (- (/ 1 x))))) 0.160 * [approximate]: Taking taylor expansion of (/ 2 (+ (exp (/ 1 x)) (exp (- (/ 1 x))))) in (x) around 0 0.160 * [taylor]: Taking taylor expansion of (/ 2 (+ (exp (/ 1 x)) (exp (- (/ 1 x))))) in x 0.160 * [taylor]: Taking taylor expansion of 2 in x 0.160 * [backup-simplify]: Simplify 2 into 2 0.160 * [taylor]: Taking taylor expansion of (+ (exp (/ 1 x)) (exp (- (/ 1 x)))) in x 0.160 * [taylor]: Taking taylor expansion of (exp (/ 1 x)) in x 0.160 * [taylor]: Taking taylor expansion of (/ 1 x) in x 0.160 * [taylor]: Taking taylor expansion of x in x 0.160 * [backup-simplify]: Simplify 0 into 0 0.160 * [backup-simplify]: Simplify 1 into 1 0.161 * [backup-simplify]: Simplify (/ 1 1) into 1 0.161 * [backup-simplify]: Simplify (exp (/ 1 x)) into (exp (/ 1 x)) 0.161 * [taylor]: Taking taylor expansion of (exp (- (/ 1 x))) in x 0.161 * [taylor]: Taking taylor expansion of (- (/ 1 x)) in x 0.161 * [taylor]: Taking taylor expansion of (/ 1 x) in x 0.161 * [taylor]: Taking taylor expansion of x in x 0.161 * [backup-simplify]: Simplify 0 into 0 0.161 * [backup-simplify]: Simplify 1 into 1 0.161 * [backup-simplify]: Simplify (/ 1 1) into 1 0.161 * [backup-simplify]: Simplify (- 1) into -1 0.161 * [backup-simplify]: Simplify (exp (- (/ 1 x))) into (exp (- (/ 1 x))) 0.162 * [backup-simplify]: Simplify (+ (exp (/ 1 x)) (exp (- (/ 1 x)))) into (+ (exp (/ 1 x)) (exp (- (/ 1 x)))) 0.162 * [backup-simplify]: Simplify (/ 2 (+ (exp (/ 1 x)) (exp (- (/ 1 x))))) into (/ 2 (+ (exp (/ 1 x)) (exp (- (/ 1 x))))) 0.162 * [taylor]: Taking taylor expansion of (/ 2 (+ (exp (/ 1 x)) (exp (- (/ 1 x))))) in x 0.162 * [taylor]: Taking taylor expansion of 2 in x 0.162 * [backup-simplify]: Simplify 2 into 2 0.162 * [taylor]: Taking taylor expansion of (+ (exp (/ 1 x)) (exp (- (/ 1 x)))) in x 0.162 * [taylor]: Taking taylor expansion of (exp (/ 1 x)) in x 0.162 * [taylor]: Taking taylor expansion of (/ 1 x) in x 0.162 * [taylor]: Taking taylor expansion of x in x 0.162 * [backup-simplify]: Simplify 0 into 0 0.162 * [backup-simplify]: Simplify 1 into 1 0.162 * [backup-simplify]: Simplify (/ 1 1) into 1 0.162 * [backup-simplify]: Simplify (exp (/ 1 x)) into (exp (/ 1 x)) 0.162 * [taylor]: Taking taylor expansion of (exp (- (/ 1 x))) in x 0.162 * [taylor]: Taking taylor expansion of (- (/ 1 x)) in x 0.162 * [taylor]: Taking taylor expansion of (/ 1 x) in x 0.162 * [taylor]: Taking taylor expansion of x in x 0.162 * [backup-simplify]: Simplify 0 into 0 0.162 * [backup-simplify]: Simplify 1 into 1 0.162 * [backup-simplify]: Simplify (/ 1 1) into 1 0.163 * [backup-simplify]: Simplify (- 1) into -1 0.163 * [backup-simplify]: Simplify (exp (- (/ 1 x))) into (exp (- (/ 1 x))) 0.163 * [backup-simplify]: Simplify (+ (exp (/ 1 x)) (exp (- (/ 1 x)))) into (+ (exp (/ 1 x)) (exp (- (/ 1 x)))) 0.163 * [backup-simplify]: Simplify (/ 2 (+ (exp (/ 1 x)) (exp (- (/ 1 x))))) into (/ 2 (+ (exp (/ 1 x)) (exp (- (/ 1 x))))) 0.163 * [backup-simplify]: Simplify (/ 2 (+ (exp (/ 1 x)) (exp (- (/ 1 x))))) into (/ 2 (+ (exp (/ 1 x)) (exp (- (/ 1 x))))) 0.163 * [backup-simplify]: Simplify (+ 0 0) into 0 0.164 * [backup-simplify]: Simplify (- (/ 0 (+ (exp (/ 1 x)) (exp (- (/ 1 x))))) (+ (* (/ 2 (+ (exp (/ 1 x)) (exp (- (/ 1 x))))) (/ 0 (+ (exp (/ 1 x)) (exp (- (/ 1 x)))))))) into 0 0.164 * [backup-simplify]: Simplify 0 into 0 0.164 * [backup-simplify]: Simplify (+ 0 0) into 0 0.164 * [backup-simplify]: Simplify (- (/ 0 (+ (exp (/ 1 x)) (exp (- (/ 1 x))))) (+ (* (/ 2 (+ (exp (/ 1 x)) (exp (- (/ 1 x))))) (/ 0 (+ (exp (/ 1 x)) (exp (- (/ 1 x)))))) (* 0 (/ 0 (+ (exp (/ 1 x)) (exp (- (/ 1 x)))))))) into 0 0.164 * [backup-simplify]: Simplify 0 into 0 0.164 * [backup-simplify]: Simplify (+ 0 0) into 0 0.165 * [backup-simplify]: Simplify (- (/ 0 (+ (exp (/ 1 x)) (exp (- (/ 1 x))))) (+ (* (/ 2 (+ (exp (/ 1 x)) (exp (- (/ 1 x))))) (/ 0 (+ (exp (/ 1 x)) (exp (- (/ 1 x)))))) (* 0 (/ 0 (+ (exp (/ 1 x)) (exp (- (/ 1 x)))))) (* 0 (/ 0 (+ (exp (/ 1 x)) (exp (- (/ 1 x)))))))) into 0 0.165 * [backup-simplify]: Simplify 0 into 0 0.165 * [backup-simplify]: Simplify (+ 0 0) into 0 0.166 * [backup-simplify]: Simplify (- (/ 0 (+ (exp (/ 1 x)) (exp (- (/ 1 x))))) (+ (* (/ 2 (+ (exp (/ 1 x)) (exp (- (/ 1 x))))) (/ 0 (+ (exp (/ 1 x)) (exp (- (/ 1 x)))))) (* 0 (/ 0 (+ (exp (/ 1 x)) (exp (- (/ 1 x)))))) (* 0 (/ 0 (+ (exp (/ 1 x)) (exp (- (/ 1 x)))))) (* 0 (/ 0 (+ (exp (/ 1 x)) (exp (- (/ 1 x)))))))) into 0 0.166 * [backup-simplify]: Simplify 0 into 0 0.166 * [backup-simplify]: Simplify (+ 0 0) into 0 0.166 * [backup-simplify]: Simplify (- (/ 0 (+ (exp (/ 1 x)) (exp (- (/ 1 x))))) (+ (* (/ 2 (+ (exp (/ 1 x)) (exp (- (/ 1 x))))) (/ 0 (+ (exp (/ 1 x)) (exp (- (/ 1 x)))))) (* 0 (/ 0 (+ (exp (/ 1 x)) (exp (- (/ 1 x)))))) (* 0 (/ 0 (+ (exp (/ 1 x)) (exp (- (/ 1 x)))))) (* 0 (/ 0 (+ (exp (/ 1 x)) (exp (- (/ 1 x)))))) (* 0 (/ 0 (+ (exp (/ 1 x)) (exp (- (/ 1 x)))))))) into 0 0.166 * [backup-simplify]: Simplify 0 into 0 0.167 * [backup-simplify]: Simplify (+ 0 0) into 0 0.167 * [backup-simplify]: Simplify (- (/ 0 (+ (exp (/ 1 x)) (exp (- (/ 1 x))))) (+ (* (/ 2 (+ (exp (/ 1 x)) (exp (- (/ 1 x))))) (/ 0 (+ (exp (/ 1 x)) (exp (- (/ 1 x)))))) (* 0 (/ 0 (+ (exp (/ 1 x)) (exp (- (/ 1 x)))))) (* 0 (/ 0 (+ (exp (/ 1 x)) (exp (- (/ 1 x)))))) (* 0 (/ 0 (+ (exp (/ 1 x)) (exp (- (/ 1 x)))))) (* 0 (/ 0 (+ (exp (/ 1 x)) (exp (- (/ 1 x)))))) (* 0 (/ 0 (+ (exp (/ 1 x)) (exp (- (/ 1 x)))))))) into 0 0.167 * [backup-simplify]: Simplify 0 into 0 0.167 * [backup-simplify]: Simplify (/ 2 (+ (exp (/ 1 (/ 1 x))) (exp (- (/ 1 (/ 1 x)))))) into (/ 2 (+ (exp x) (exp (- x)))) 0.168 * [backup-simplify]: Simplify (/ 2 (+ (exp (/ 1 (- x))) (exp (- (/ 1 (- x)))))) into (/ 2 (+ (exp (/ 1 x)) (exp (/ -1 x)))) 0.168 * [approximate]: Taking taylor expansion of (/ 2 (+ (exp (/ 1 x)) (exp (/ -1 x)))) in (x) around 0 0.168 * [taylor]: Taking taylor expansion of (/ 2 (+ (exp (/ 1 x)) (exp (/ -1 x)))) in x 0.168 * [taylor]: Taking taylor expansion of 2 in x 0.168 * [backup-simplify]: Simplify 2 into 2 0.168 * [taylor]: Taking taylor expansion of (+ (exp (/ 1 x)) (exp (/ -1 x))) in x 0.168 * [taylor]: Taking taylor expansion of (exp (/ 1 x)) in x 0.168 * [taylor]: Taking taylor expansion of (/ 1 x) in x 0.168 * [taylor]: Taking taylor expansion of x in x 0.168 * [backup-simplify]: Simplify 0 into 0 0.168 * [backup-simplify]: Simplify 1 into 1 0.168 * [backup-simplify]: Simplify (/ 1 1) into 1 0.168 * [backup-simplify]: Simplify (exp (/ 1 x)) into (exp (/ 1 x)) 0.168 * [taylor]: Taking taylor expansion of (exp (/ -1 x)) in x 0.168 * [taylor]: Taking taylor expansion of (/ -1 x) in x 0.168 * [taylor]: Taking taylor expansion of -1 in x 0.168 * [backup-simplify]: Simplify -1 into -1 0.168 * [taylor]: Taking taylor expansion of x in x 0.168 * [backup-simplify]: Simplify 0 into 0 0.168 * [backup-simplify]: Simplify 1 into 1 0.169 * [backup-simplify]: Simplify (/ -1 1) into -1 0.169 * [backup-simplify]: Simplify (exp (/ -1 x)) into (exp (/ -1 x)) 0.169 * [backup-simplify]: Simplify (+ (exp (/ 1 x)) (exp (/ -1 x))) into (+ (exp (/ 1 x)) (exp (/ -1 x))) 0.169 * [backup-simplify]: Simplify (/ 2 (+ (exp (/ 1 x)) (exp (/ -1 x)))) into (/ 2 (+ (exp (/ 1 x)) (exp (/ -1 x)))) 0.169 * [taylor]: Taking taylor expansion of (/ 2 (+ (exp (/ 1 x)) (exp (/ -1 x)))) in x 0.169 * [taylor]: Taking taylor expansion of 2 in x 0.169 * [backup-simplify]: Simplify 2 into 2 0.169 * [taylor]: Taking taylor expansion of (+ (exp (/ 1 x)) (exp (/ -1 x))) in x 0.169 * [taylor]: Taking taylor expansion of (exp (/ 1 x)) in x 0.169 * [taylor]: Taking taylor expansion of (/ 1 x) in x 0.169 * [taylor]: Taking taylor expansion of x in x 0.169 * [backup-simplify]: Simplify 0 into 0 0.169 * [backup-simplify]: Simplify 1 into 1 0.169 * [backup-simplify]: Simplify (/ 1 1) into 1 0.169 * [backup-simplify]: Simplify (exp (/ 1 x)) into (exp (/ 1 x)) 0.169 * [taylor]: Taking taylor expansion of (exp (/ -1 x)) in x 0.169 * [taylor]: Taking taylor expansion of (/ -1 x) in x 0.169 * [taylor]: Taking taylor expansion of -1 in x 0.169 * [backup-simplify]: Simplify -1 into -1 0.169 * [taylor]: Taking taylor expansion of x in x 0.169 * [backup-simplify]: Simplify 0 into 0 0.169 * [backup-simplify]: Simplify 1 into 1 0.170 * [backup-simplify]: Simplify (/ -1 1) into -1 0.170 * [backup-simplify]: Simplify (exp (/ -1 x)) into (exp (/ -1 x)) 0.170 * [backup-simplify]: Simplify (+ (exp (/ 1 x)) (exp (/ -1 x))) into (+ (exp (/ 1 x)) (exp (/ -1 x))) 0.170 * [backup-simplify]: Simplify (/ 2 (+ (exp (/ 1 x)) (exp (/ -1 x)))) into (/ 2 (+ (exp (/ 1 x)) (exp (/ -1 x)))) 0.170 * [backup-simplify]: Simplify (/ 2 (+ (exp (/ 1 x)) (exp (/ -1 x)))) into (/ 2 (+ (exp (/ 1 x)) (exp (/ -1 x)))) 0.170 * [backup-simplify]: Simplify (+ 0 0) into 0 0.170 * [backup-simplify]: Simplify (- (/ 0 (+ (exp (/ 1 x)) (exp (/ -1 x)))) (+ (* (/ 2 (+ (exp (/ 1 x)) (exp (/ -1 x)))) (/ 0 (+ (exp (/ 1 x)) (exp (/ -1 x))))))) into 0 0.170 * [backup-simplify]: Simplify 0 into 0 0.171 * [backup-simplify]: Simplify (+ 0 0) into 0 0.171 * [backup-simplify]: Simplify (- (/ 0 (+ (exp (/ 1 x)) (exp (/ -1 x)))) (+ (* (/ 2 (+ (exp (/ 1 x)) (exp (/ -1 x)))) (/ 0 (+ (exp (/ 1 x)) (exp (/ -1 x))))) (* 0 (/ 0 (+ (exp (/ 1 x)) (exp (/ -1 x))))))) into 0 0.171 * [backup-simplify]: Simplify 0 into 0 0.171 * [backup-simplify]: Simplify (+ 0 0) into 0 0.172 * [backup-simplify]: Simplify (- (/ 0 (+ (exp (/ 1 x)) (exp (/ -1 x)))) (+ (* (/ 2 (+ (exp (/ 1 x)) (exp (/ -1 x)))) (/ 0 (+ (exp (/ 1 x)) (exp (/ -1 x))))) (* 0 (/ 0 (+ (exp (/ 1 x)) (exp (/ -1 x))))) (* 0 (/ 0 (+ (exp (/ 1 x)) (exp (/ -1 x))))))) into 0 0.172 * [backup-simplify]: Simplify 0 into 0 0.172 * [backup-simplify]: Simplify (+ 0 0) into 0 0.172 * [backup-simplify]: Simplify (- (/ 0 (+ (exp (/ 1 x)) (exp (/ -1 x)))) (+ (* (/ 2 (+ (exp (/ 1 x)) (exp (/ -1 x)))) (/ 0 (+ (exp (/ 1 x)) (exp (/ -1 x))))) (* 0 (/ 0 (+ (exp (/ 1 x)) (exp (/ -1 x))))) (* 0 (/ 0 (+ (exp (/ 1 x)) (exp (/ -1 x))))) (* 0 (/ 0 (+ (exp (/ 1 x)) (exp (/ -1 x))))))) into 0 0.172 * [backup-simplify]: Simplify 0 into 0 0.172 * [backup-simplify]: Simplify (+ 0 0) into 0 0.173 * [backup-simplify]: Simplify (- (/ 0 (+ (exp (/ 1 x)) (exp (/ -1 x)))) (+ (* (/ 2 (+ (exp (/ 1 x)) (exp (/ -1 x)))) (/ 0 (+ (exp (/ 1 x)) (exp (/ -1 x))))) (* 0 (/ 0 (+ (exp (/ 1 x)) (exp (/ -1 x))))) (* 0 (/ 0 (+ (exp (/ 1 x)) (exp (/ -1 x))))) (* 0 (/ 0 (+ (exp (/ 1 x)) (exp (/ -1 x))))) (* 0 (/ 0 (+ (exp (/ 1 x)) (exp (/ -1 x))))))) into 0 0.173 * [backup-simplify]: Simplify 0 into 0 0.173 * [backup-simplify]: Simplify (+ 0 0) into 0 0.174 * [backup-simplify]: Simplify (- (/ 0 (+ (exp (/ 1 x)) (exp (/ -1 x)))) (+ (* (/ 2 (+ (exp (/ 1 x)) (exp (/ -1 x)))) (/ 0 (+ (exp (/ 1 x)) (exp (/ -1 x))))) (* 0 (/ 0 (+ (exp (/ 1 x)) (exp (/ -1 x))))) (* 0 (/ 0 (+ (exp (/ 1 x)) (exp (/ -1 x))))) (* 0 (/ 0 (+ (exp (/ 1 x)) (exp (/ -1 x))))) (* 0 (/ 0 (+ (exp (/ 1 x)) (exp (/ -1 x))))) (* 0 (/ 0 (+ (exp (/ 1 x)) (exp (/ -1 x))))))) into 0 0.174 * [backup-simplify]: Simplify 0 into 0 0.174 * [backup-simplify]: Simplify (/ 2 (+ (exp (/ 1 (/ 1 (- x)))) (exp (/ -1 (/ 1 (- x)))))) into (/ 2 (+ (exp (* -1 x)) (exp x))) 0.174 * * * [progress]: simplifying candidates 0.174 * * * * [progress]: [ 1 / 37 ] simplifiying candidate # 0.174 * * * * [progress]: [ 2 / 37 ] simplifiying candidate # 0.174 * [simplify]: Simplifying (- (log 2) (log (+ (exp x) (exp (- x))))) 0.174 * * [simplify]: iters left: 6 (9 enodes) 0.177 * * [simplify]: iters left: 5 (32 enodes) 0.182 * * [simplify]: iters left: 4 (39 enodes) 0.188 * * [simplify]: iters left: 3 (41 enodes) 0.199 * * [simplify]: Extracting #0: cost 1 inf + 0 0.199 * * [simplify]: Extracting #1: cost 5 inf + 0 0.199 * * [simplify]: Extracting #2: cost 10 inf + 0 0.199 * * [simplify]: Extracting #3: cost 12 inf + 1 0.199 * * [simplify]: Extracting #4: cost 15 inf + 143 0.199 * * [simplify]: Extracting #5: cost 13 inf + 216 0.200 * * [simplify]: Extracting #6: cost 9 inf + 550 0.200 * * [simplify]: Extracting #7: cost 4 inf + 1655 0.200 * * [simplify]: Extracting #8: cost 0 inf + 3081 0.200 * [simplify]: Simplified to (- (log 2) (log (+ (exp x) (exp (- x))))) 0.200 * [simplify]: Simplified (2 1) to (λ (x) (exp (- (log 2) (log (+ (exp x) (exp (- x))))))) 0.200 * * * * [progress]: [ 3 / 37 ] simplifiying candidate # 0.201 * [simplify]: Simplifying (log (/ 2 (+ (exp x) (exp (- x))))) 0.201 * * [simplify]: iters left: 6 (8 enodes) 0.203 * * [simplify]: iters left: 5 (30 enodes) 0.208 * * [simplify]: iters left: 4 (40 enodes) 0.214 * * [simplify]: iters left: 3 (45 enodes) 0.220 * * [simplify]: Extracting #0: cost 1 inf + 0 0.221 * * [simplify]: Extracting #1: cost 6 inf + 0 0.221 * * [simplify]: Extracting #2: cost 12 inf + 0 0.221 * * [simplify]: Extracting #3: cost 13 inf + 72 0.221 * * [simplify]: Extracting #4: cost 17 inf + 143 0.221 * * [simplify]: Extracting #5: cost 15 inf + 186 0.221 * * [simplify]: Extracting #6: cost 9 inf + 992 0.221 * * [simplify]: Extracting #7: cost 1 inf + 3133 0.222 * * [simplify]: Extracting #8: cost 0 inf + 3465 0.222 * [simplify]: Simplified to (log (/ 2 (+ (exp x) (exp (- x))))) 0.222 * [simplify]: Simplified (2 1) to (λ (x) (exp (log (/ 2 (+ (exp x) (exp (- x))))))) 0.222 * * * * [progress]: [ 4 / 37 ] simplifiying candidate # 0.222 * [simplify]: Simplifying (exp (/ 2 (+ (exp x) (exp (- x))))) 0.222 * * [simplify]: iters left: 6 (8 enodes) 0.224 * * [simplify]: iters left: 5 (27 enodes) 0.229 * * [simplify]: iters left: 4 (31 enodes) 0.233 * * [simplify]: iters left: 3 (33 enodes) 0.238 * * [simplify]: Extracting #0: cost 1 inf + 0 0.238 * * [simplify]: Extracting #1: cost 3 inf + 0 0.238 * * [simplify]: Extracting #2: cost 6 inf + 0 0.238 * * [simplify]: Extracting #3: cost 8 inf + 1 0.238 * * [simplify]: Extracting #4: cost 13 inf + 1 0.238 * * [simplify]: Extracting #5: cost 11 inf + 44 0.239 * * [simplify]: Extracting #6: cost 5 inf + 670 0.239 * * [simplify]: Extracting #7: cost 1 inf + 1747 0.239 * * [simplify]: Extracting #8: cost 0 inf + 2079 0.239 * [simplify]: Simplified to (exp (/ 2 (+ (exp x) (exp (- x))))) 0.239 * [simplify]: Simplified (2 1) to (λ (x) (log (exp (/ 2 (+ (exp x) (exp (- x))))))) 0.239 * * * * [progress]: [ 5 / 37 ] simplifiying candidate # 0.239 * [simplify]: Simplifying (/ (* (* 2 2) 2) (* (* (+ (exp x) (exp (- x))) (+ (exp x) (exp (- x)))) (+ (exp x) (exp (- x))))) 0.240 * * [simplify]: iters left: 6 (11 enodes) 0.243 * * [simplify]: iters left: 5 (58 enodes) 0.257 * * [simplify]: iters left: 4 (181 enodes) 0.310 * * [simplify]: iters left: 3 (482 enodes) 0.619 * * [simplify]: Extracting #0: cost 1 inf + 0 0.619 * * [simplify]: Extracting #1: cost 66 inf + 0 0.620 * * [simplify]: Extracting #2: cost 164 inf + 4 0.621 * * [simplify]: Extracting #3: cost 247 inf + 5 0.621 * * [simplify]: Extracting #4: cost 253 inf + 1047 0.623 * * [simplify]: Extracting #5: cost 201 inf + 12109 0.637 * * [simplify]: Extracting #6: cost 55 inf + 56202 0.663 * * [simplify]: Extracting #7: cost 1 inf + 74359 0.689 * * [simplify]: Extracting #8: cost 0 inf + 74620 0.708 * [simplify]: Simplified to (/ 8 (* (+ (exp (- x)) (exp x)) (* (+ (exp (- x)) (exp x)) (+ (exp (- x)) (exp x))))) 0.708 * [simplify]: Simplified (2 1) to (λ (x) (cbrt (/ 8 (* (+ (exp (- x)) (exp x)) (* (+ (exp (- x)) (exp x)) (+ (exp (- x)) (exp x))))))) 0.708 * * * * [progress]: [ 6 / 37 ] simplifiying candidate # 0.709 * [simplify]: Simplifying (* (cbrt (/ 2 (+ (exp x) (exp (- x))))) (cbrt (/ 2 (+ (exp x) (exp (- x)))))) 0.709 * * [simplify]: iters left: 6 (9 enodes) 0.711 * * [simplify]: iters left: 5 (30 enodes) 0.718 * * [simplify]: iters left: 4 (34 enodes) 0.724 * * [simplify]: iters left: 3 (36 enodes) 0.729 * * [simplify]: Extracting #0: cost 1 inf + 0 0.729 * * [simplify]: Extracting #1: cost 3 inf + 0 0.729 * * [simplify]: Extracting #2: cost 5 inf + 0 0.729 * * [simplify]: Extracting #3: cost 8 inf + 0 0.729 * * [simplify]: Extracting #4: cost 10 inf + 1 0.729 * * [simplify]: Extracting #5: cost 15 inf + 1 0.729 * * [simplify]: Extracting #6: cost 13 inf + 44 0.729 * * [simplify]: Extracting #7: cost 8 inf + 559 0.729 * * [simplify]: Extracting #8: cost 4 inf + 1495 0.730 * * [simplify]: Extracting #9: cost 0 inf + 2863 0.730 * [simplify]: Simplified to (* (cbrt (/ 2 (+ (exp x) (exp (- x))))) (cbrt (/ 2 (+ (exp x) (exp (- x)))))) 0.730 * [simplify]: Simplified (2 1) to (λ (x) (* (* (cbrt (/ 2 (+ (exp x) (exp (- x))))) (cbrt (/ 2 (+ (exp x) (exp (- x)))))) (cbrt (/ 2 (+ (exp x) (exp (- x))))))) 0.730 * [simplify]: Simplifying (cbrt (/ 2 (+ (exp x) (exp (- x))))) 0.730 * * [simplify]: iters left: 6 (8 enodes) 0.733 * * [simplify]: iters left: 5 (27 enodes) 0.737 * * [simplify]: iters left: 4 (31 enodes) 0.745 * * [simplify]: iters left: 3 (33 enodes) 0.754 * * [simplify]: Extracting #0: cost 1 inf + 0 0.754 * * [simplify]: Extracting #1: cost 3 inf + 0 0.754 * * [simplify]: Extracting #2: cost 6 inf + 0 0.754 * * [simplify]: Extracting #3: cost 8 inf + 1 0.754 * * [simplify]: Extracting #4: cost 13 inf + 1 0.754 * * [simplify]: Extracting #5: cost 11 inf + 44 0.755 * * [simplify]: Extracting #6: cost 5 inf + 670 0.755 * * [simplify]: Extracting #7: cost 1 inf + 1757 0.755 * * [simplify]: Extracting #8: cost 0 inf + 2099 0.756 * [simplify]: Simplified to (cbrt (/ 2 (+ (exp x) (exp (- x))))) 0.756 * [simplify]: Simplified (2 2) to (λ (x) (* (* (cbrt (/ 2 (+ (exp x) (exp (- x))))) (cbrt (/ 2 (+ (exp x) (exp (- x)))))) (cbrt (/ 2 (+ (exp x) (exp (- x))))))) 0.756 * * * * [progress]: [ 7 / 37 ] simplifiying candidate # 0.756 * [simplify]: Simplifying (* (* (/ 2 (+ (exp x) (exp (- x)))) (/ 2 (+ (exp x) (exp (- x))))) (/ 2 (+ (exp x) (exp (- x))))) 0.757 * * [simplify]: iters left: 6 (9 enodes) 0.762 * * [simplify]: iters left: 5 (37 enodes) 0.771 * * [simplify]: iters left: 4 (68 enodes) 0.782 * * [simplify]: iters left: 3 (108 enodes) 0.809 * * [simplify]: iters left: 2 (199 enodes) 0.868 * * [simplify]: iters left: 1 (388 enodes) 0.971 * * [simplify]: Extracting #0: cost 1 inf + 0 0.971 * * [simplify]: Extracting #1: cost 37 inf + 0 0.972 * * [simplify]: Extracting #2: cost 118 inf + 4 0.974 * * [simplify]: Extracting #3: cost 171 inf + 8 0.976 * * [simplify]: Extracting #4: cost 157 inf + 3237 0.980 * * [simplify]: Extracting #5: cost 67 inf + 30733 0.989 * * [simplify]: Extracting #6: cost 1 inf + 57414 1.002 * * [simplify]: Extracting #7: cost 0 inf + 57619 1.012 * [simplify]: Simplified to (* (* (/ 2 (+ (exp x) (exp (- x)))) (/ 2 (+ (exp x) (exp (- x))))) (/ 2 (+ (exp x) (exp (- x))))) 1.012 * [simplify]: Simplified (2 1) to (λ (x) (cbrt (* (* (/ 2 (+ (exp x) (exp (- x)))) (/ 2 (+ (exp x) (exp (- x))))) (/ 2 (+ (exp x) (exp (- x))))))) 1.012 * * * * [progress]: [ 8 / 37 ] simplifiying candidate # 1.012 * [simplify]: Simplifying (sqrt (/ 2 (+ (exp x) (exp (- x))))) 1.012 * * [simplify]: iters left: 6 (8 enodes) 1.015 * * [simplify]: iters left: 5 (27 enodes) 1.019 * * [simplify]: iters left: 4 (31 enodes) 1.024 * * [simplify]: iters left: 3 (33 enodes) 1.029 * * [simplify]: Extracting #0: cost 1 inf + 0 1.029 * * [simplify]: Extracting #1: cost 3 inf + 0 1.029 * * [simplify]: Extracting #2: cost 6 inf + 0 1.029 * * [simplify]: Extracting #3: cost 8 inf + 1 1.029 * * [simplify]: Extracting #4: cost 13 inf + 1 1.029 * * [simplify]: Extracting #5: cost 11 inf + 44 1.029 * * [simplify]: Extracting #6: cost 5 inf + 670 1.029 * * [simplify]: Extracting #7: cost 1 inf + 1717 1.029 * * [simplify]: Extracting #8: cost 0 inf + 2019 1.030 * [simplify]: Simplified to (sqrt (/ 2 (+ (exp x) (exp (- x))))) 1.030 * [simplify]: Simplified (2 1) to (λ (x) (* (sqrt (/ 2 (+ (exp x) (exp (- x))))) (sqrt (/ 2 (+ (exp x) (exp (- x))))))) 1.030 * [simplify]: Simplifying (sqrt (/ 2 (+ (exp x) (exp (- x))))) 1.030 * * [simplify]: iters left: 6 (8 enodes) 1.032 * * [simplify]: iters left: 5 (27 enodes) 1.036 * * [simplify]: iters left: 4 (31 enodes) 1.041 * * [simplify]: iters left: 3 (33 enodes) 1.045 * * [simplify]: Extracting #0: cost 1 inf + 0 1.045 * * [simplify]: Extracting #1: cost 3 inf + 0 1.045 * * [simplify]: Extracting #2: cost 6 inf + 0 1.045 * * [simplify]: Extracting #3: cost 8 inf + 1 1.046 * * [simplify]: Extracting #4: cost 13 inf + 1 1.046 * * [simplify]: Extracting #5: cost 11 inf + 44 1.046 * * [simplify]: Extracting #6: cost 5 inf + 670 1.046 * * [simplify]: Extracting #7: cost 1 inf + 1717 1.046 * * [simplify]: Extracting #8: cost 0 inf + 2019 1.046 * [simplify]: Simplified to (sqrt (/ 2 (+ (exp x) (exp (- x))))) 1.046 * [simplify]: Simplified (2 2) to (λ (x) (* (sqrt (/ 2 (+ (exp x) (exp (- x))))) (sqrt (/ 2 (+ (exp x) (exp (- x))))))) 1.046 * * * * [progress]: [ 9 / 37 ] simplifiying candidate # 1.047 * [simplify]: Simplifying (- 2) 1.047 * * [simplify]: iters left: 2 (2 enodes) 1.048 * * [simplify]: iters left: 1 (7 enodes) 1.049 * * [simplify]: Extracting #0: cost 1 inf + 0 1.049 * * [simplify]: Extracting #1: cost 0 inf + 1 1.049 * [simplify]: Simplified to -2 1.049 * [simplify]: Simplified (2 1) to (λ (x) (/ -2 (- (+ (exp x) (exp (- x)))))) 1.049 * [simplify]: Simplifying (- (+ (exp x) (exp (- x)))) 1.049 * * [simplify]: iters left: 6 (6 enodes) 1.051 * * [simplify]: iters left: 5 (24 enodes) 1.056 * * [simplify]: iters left: 4 (37 enodes) 1.066 * * [simplify]: iters left: 3 (41 enodes) 1.071 * * [simplify]: Extracting #0: cost 1 inf + 0 1.071 * * [simplify]: Extracting #1: cost 6 inf + 0 1.071 * * [simplify]: Extracting #2: cost 14 inf + 0 1.071 * * [simplify]: Extracting #3: cost 15 inf + 2 1.072 * * [simplify]: Extracting #4: cost 9 inf + 481 1.072 * * [simplify]: Extracting #5: cost 2 inf + 1239 1.072 * * [simplify]: Extracting #6: cost 0 inf + 1583 1.072 * [simplify]: Simplified to (- (+ (exp x) (/ 1 (exp x)))) 1.072 * [simplify]: Simplified (2 2) to (λ (x) (/ -2 (- (+ (exp x) (/ 1 (exp x)))))) 1.072 * * * * [progress]: [ 10 / 37 ] simplifiying candidate # 1.073 * [simplify]: Simplifying (/ (* (cbrt 2) (cbrt 2)) (* (cbrt (+ (exp x) (exp (- x)))) (cbrt (+ (exp x) (exp (- x)))))) 1.073 * * [simplify]: iters left: 6 (11 enodes) 1.076 * * [simplify]: iters left: 5 (42 enodes) 1.082 * * [simplify]: iters left: 4 (61 enodes) 1.094 * * [simplify]: iters left: 3 (70 enodes) 1.113 * * [simplify]: iters left: 2 (73 enodes) 1.132 * * [simplify]: Extracting #0: cost 1 inf + 0 1.132 * * [simplify]: Extracting #1: cost 11 inf + 0 1.132 * * [simplify]: Extracting #2: cost 22 inf + 0 1.133 * * [simplify]: Extracting #3: cost 24 inf + 1 1.133 * * [simplify]: Extracting #4: cost 28 inf + 82 1.133 * * [simplify]: Extracting #5: cost 21 inf + 590 1.133 * * [simplify]: Extracting #6: cost 14 inf + 2138 1.135 * * [simplify]: Extracting #7: cost 2 inf + 7039 1.137 * * [simplify]: Extracting #8: cost 0 inf + 7963 1.139 * [simplify]: Simplified to (* (/ (cbrt 2) (cbrt (+ (exp (- x)) (exp x)))) (/ (cbrt 2) (cbrt (+ (exp (- x)) (exp x))))) 1.139 * [simplify]: Simplified (2 1) to (λ (x) (* (* (/ (cbrt 2) (cbrt (+ (exp (- x)) (exp x)))) (/ (cbrt 2) (cbrt (+ (exp (- x)) (exp x))))) (/ (cbrt 2) (cbrt (+ (exp x) (exp (- x))))))) 1.139 * [simplify]: Simplifying (/ (cbrt 2) (cbrt (+ (exp x) (exp (- x))))) 1.139 * * [simplify]: iters left: 6 (9 enodes) 1.144 * * [simplify]: iters left: 5 (30 enodes) 1.151 * * [simplify]: iters left: 4 (34 enodes) 1.157 * * [simplify]: iters left: 3 (36 enodes) 1.163 * * [simplify]: Extracting #0: cost 1 inf + 0 1.163 * * [simplify]: Extracting #1: cost 4 inf + 0 1.163 * * [simplify]: Extracting #2: cost 8 inf + 0 1.163 * * [simplify]: Extracting #3: cost 10 inf + 1 1.163 * * [simplify]: Extracting #4: cost 13 inf + 163 1.163 * * [simplify]: Extracting #5: cost 8 inf + 459 1.163 * * [simplify]: Extracting #6: cost 4 inf + 1133 1.164 * * [simplify]: Extracting #7: cost 0 inf + 2499 1.164 * [simplify]: Simplified to (/ (cbrt 2) (cbrt (+ (exp x) (exp (- x))))) 1.164 * [simplify]: Simplified (2 2) to (λ (x) (* (/ (* (cbrt 2) (cbrt 2)) (* (cbrt (+ (exp x) (exp (- x)))) (cbrt (+ (exp x) (exp (- x)))))) (/ (cbrt 2) (cbrt (+ (exp x) (exp (- x))))))) 1.164 * * * * [progress]: [ 11 / 37 ] simplifiying candidate # 1.164 * [simplify]: Simplifying (/ (* (cbrt 2) (cbrt 2)) (sqrt (+ (exp x) (exp (- x))))) 1.164 * * [simplify]: iters left: 6 (10 enodes) 1.167 * * [simplify]: iters left: 5 (35 enodes) 1.175 * * [simplify]: iters left: 4 (43 enodes) 1.183 * * [simplify]: iters left: 3 (48 enodes) 1.197 * * [simplify]: Extracting #0: cost 1 inf + 0 1.197 * * [simplify]: Extracting #1: cost 7 inf + 0 1.197 * * [simplify]: Extracting #2: cost 14 inf + 0 1.197 * * [simplify]: Extracting #3: cost 16 inf + 1 1.198 * * [simplify]: Extracting #4: cost 20 inf + 82 1.198 * * [simplify]: Extracting #5: cost 15 inf + 448 1.198 * * [simplify]: Extracting #6: cost 8 inf + 1295 1.199 * * [simplify]: Extracting #7: cost 1 inf + 3807 1.200 * * [simplify]: Extracting #8: cost 0 inf + 4189 1.201 * [simplify]: Simplified to (/ (cbrt 2) (/ (sqrt (+ (exp (- x)) (exp x))) (cbrt 2))) 1.201 * [simplify]: Simplified (2 1) to (λ (x) (* (/ (cbrt 2) (/ (sqrt (+ (exp (- x)) (exp x))) (cbrt 2))) (/ (cbrt 2) (sqrt (+ (exp x) (exp (- x))))))) 1.201 * [simplify]: Simplifying (/ (cbrt 2) (sqrt (+ (exp x) (exp (- x))))) 1.201 * * [simplify]: iters left: 6 (9 enodes) 1.206 * * [simplify]: iters left: 5 (30 enodes) 1.215 * * [simplify]: iters left: 4 (34 enodes) 1.220 * * [simplify]: iters left: 3 (36 enodes) 1.225 * * [simplify]: Extracting #0: cost 1 inf + 0 1.225 * * [simplify]: Extracting #1: cost 4 inf + 0 1.225 * * [simplify]: Extracting #2: cost 8 inf + 0 1.225 * * [simplify]: Extracting #3: cost 10 inf + 1 1.225 * * [simplify]: Extracting #4: cost 13 inf + 163 1.225 * * [simplify]: Extracting #5: cost 8 inf + 459 1.225 * * [simplify]: Extracting #6: cost 4 inf + 1093 1.226 * * [simplify]: Extracting #7: cost 0 inf + 2339 1.226 * [simplify]: Simplified to (/ (cbrt 2) (sqrt (+ (exp x) (exp (- x))))) 1.226 * [simplify]: Simplified (2 2) to (λ (x) (* (/ (* (cbrt 2) (cbrt 2)) (sqrt (+ (exp x) (exp (- x))))) (/ (cbrt 2) (sqrt (+ (exp x) (exp (- x))))))) 1.226 * * * * [progress]: [ 12 / 37 ] simplifiying candidate # 1.226 * [simplify]: Simplifying (/ (* (cbrt 2) (cbrt 2)) 1) 1.226 * * [simplify]: iters left: 5 (5 enodes) 1.228 * * [simplify]: iters left: 4 (17 enodes) 1.232 * * [simplify]: iters left: 3 (27 enodes) 1.236 * * [simplify]: iters left: 2 (28 enodes) 1.240 * * [simplify]: Extracting #0: cost 1 inf + 0 1.240 * * [simplify]: Extracting #1: cost 5 inf + 0 1.240 * * [simplify]: Extracting #2: cost 7 inf + 1 1.241 * * [simplify]: Extracting #3: cost 6 inf + 2 1.241 * * [simplify]: Extracting #4: cost 1 inf + 528 1.241 * * [simplify]: Extracting #5: cost 0 inf + 650 1.241 * [simplify]: Simplified to (* (cbrt 2) (cbrt 2)) 1.241 * [simplify]: Simplified (2 1) to (λ (x) (* (* (cbrt 2) (cbrt 2)) (/ (cbrt 2) (+ (exp x) (exp (- x)))))) 1.241 * [simplify]: Simplifying (/ (cbrt 2) (+ (exp x) (exp (- x)))) 1.241 * * [simplify]: iters left: 6 (8 enodes) 1.245 * * [simplify]: iters left: 5 (27 enodes) 1.254 * * [simplify]: iters left: 4 (31 enodes) 1.263 * * [simplify]: iters left: 3 (33 enodes) 1.272 * * [simplify]: Extracting #0: cost 1 inf + 0 1.272 * * [simplify]: Extracting #1: cost 4 inf + 0 1.272 * * [simplify]: Extracting #2: cost 9 inf + 0 1.272 * * [simplify]: Extracting #3: cost 13 inf + 1 1.272 * * [simplify]: Extracting #4: cost 8 inf + 307 1.273 * * [simplify]: Extracting #5: cost 1 inf + 1395 1.273 * * [simplify]: Extracting #6: cost 0 inf + 1737 1.274 * [simplify]: Simplified to (/ (cbrt 2) (+ (exp x) (exp (- x)))) 1.274 * [simplify]: Simplified (2 2) to (λ (x) (* (* (cbrt 2) (cbrt 2)) (/ (cbrt 2) (+ (exp x) (exp (- x)))))) 1.274 * * * * [progress]: [ 13 / 37 ] simplifiying candidate # 1.274 * [simplify]: Simplifying (/ (* (cbrt 2) (cbrt 2)) 1) 1.274 * * [simplify]: iters left: 5 (5 enodes) 1.277 * * [simplify]: iters left: 4 (17 enodes) 1.284 * * [simplify]: iters left: 3 (27 enodes) 1.292 * * [simplify]: iters left: 2 (28 enodes) 1.302 * * [simplify]: Extracting #0: cost 1 inf + 0 1.302 * * [simplify]: Extracting #1: cost 5 inf + 0 1.302 * * [simplify]: Extracting #2: cost 7 inf + 1 1.302 * * [simplify]: Extracting #3: cost 6 inf + 2 1.302 * * [simplify]: Extracting #4: cost 1 inf + 528 1.303 * * [simplify]: Extracting #5: cost 0 inf + 650 1.303 * [simplify]: Simplified to (* (cbrt 2) (cbrt 2)) 1.303 * [simplify]: Simplified (2 1) to (λ (x) (* (* (cbrt 2) (cbrt 2)) (/ (cbrt 2) (+ (exp x) (exp (- x)))))) 1.303 * [simplify]: Simplifying (/ (cbrt 2) (+ (exp x) (exp (- x)))) 1.303 * * [simplify]: iters left: 6 (8 enodes) 1.307 * * [simplify]: iters left: 5 (27 enodes) 1.316 * * [simplify]: iters left: 4 (31 enodes) 1.322 * * [simplify]: iters left: 3 (33 enodes) 1.327 * * [simplify]: Extracting #0: cost 1 inf + 0 1.327 * * [simplify]: Extracting #1: cost 4 inf + 0 1.327 * * [simplify]: Extracting #2: cost 9 inf + 0 1.327 * * [simplify]: Extracting #3: cost 13 inf + 1 1.327 * * [simplify]: Extracting #4: cost 8 inf + 307 1.327 * * [simplify]: Extracting #5: cost 1 inf + 1395 1.327 * * [simplify]: Extracting #6: cost 0 inf + 1737 1.328 * [simplify]: Simplified to (/ (cbrt 2) (+ (exp x) (exp (- x)))) 1.328 * [simplify]: Simplified (2 2) to (λ (x) (* (* (cbrt 2) (cbrt 2)) (/ (cbrt 2) (+ (exp x) (exp (- x)))))) 1.328 * * * * [progress]: [ 14 / 37 ] simplifiying candidate # 1.328 * [simplify]: Simplifying (/ (sqrt 2) (* (cbrt (+ (exp x) (exp (- x)))) (cbrt (+ (exp x) (exp (- x)))))) 1.328 * * [simplify]: iters left: 6 (10 enodes) 1.331 * * [simplify]: iters left: 5 (35 enodes) 1.336 * * [simplify]: iters left: 4 (41 enodes) 1.342 * * [simplify]: iters left: 3 (43 enodes) 1.352 * * [simplify]: Extracting #0: cost 1 inf + 0 1.352 * * [simplify]: Extracting #1: cost 6 inf + 0 1.352 * * [simplify]: Extracting #2: cost 12 inf + 0 1.352 * * [simplify]: Extracting #3: cost 14 inf + 1 1.352 * * [simplify]: Extracting #4: cost 18 inf + 42 1.352 * * [simplify]: Extracting #5: cost 12 inf + 419 1.353 * * [simplify]: Extracting #6: cost 7 inf + 1274 1.353 * * [simplify]: Extracting #7: cost 0 inf + 3865 1.354 * [simplify]: Simplified to (/ (/ (sqrt 2) (cbrt (+ (exp x) (exp (- x))))) (cbrt (+ (exp x) (exp (- x))))) 1.354 * [simplify]: Simplified (2 1) to (λ (x) (* (/ (/ (sqrt 2) (cbrt (+ (exp x) (exp (- x))))) (cbrt (+ (exp x) (exp (- x))))) (/ (sqrt 2) (cbrt (+ (exp x) (exp (- x))))))) 1.355 * [simplify]: Simplifying (/ (sqrt 2) (cbrt (+ (exp x) (exp (- x))))) 1.355 * * [simplify]: iters left: 6 (9 enodes) 1.359 * * [simplify]: iters left: 5 (30 enodes) 1.369 * * [simplify]: iters left: 4 (34 enodes) 1.379 * * [simplify]: iters left: 3 (36 enodes) 1.390 * * [simplify]: Extracting #0: cost 1 inf + 0 1.390 * * [simplify]: Extracting #1: cost 4 inf + 0 1.390 * * [simplify]: Extracting #2: cost 8 inf + 0 1.390 * * [simplify]: Extracting #3: cost 10 inf + 1 1.390 * * [simplify]: Extracting #4: cost 13 inf + 83 1.390 * * [simplify]: Extracting #5: cost 8 inf + 379 1.391 * * [simplify]: Extracting #6: cost 4 inf + 1053 1.391 * * [simplify]: Extracting #7: cost 0 inf + 2339 1.392 * [simplify]: Simplified to (/ (sqrt 2) (cbrt (+ (exp x) (exp (- x))))) 1.392 * [simplify]: Simplified (2 2) to (λ (x) (* (/ (/ (sqrt 2) (cbrt (+ (exp x) (exp (- x))))) (cbrt (+ (exp x) (exp (- x))))) (/ (sqrt 2) (cbrt (+ (exp x) (exp (- x))))))) 1.392 * * * * [progress]: [ 15 / 37 ] simplifiying candidate # 1.392 * [simplify]: Simplifying (/ (sqrt 2) (sqrt (+ (exp x) (exp (- x))))) 1.392 * * [simplify]: iters left: 6 (9 enodes) 1.397 * * [simplify]: iters left: 5 (30 enodes) 1.406 * * [simplify]: iters left: 4 (34 enodes) 1.417 * * [simplify]: iters left: 3 (36 enodes) 1.427 * * [simplify]: Extracting #0: cost 1 inf + 0 1.427 * * [simplify]: Extracting #1: cost 4 inf + 0 1.427 * * [simplify]: Extracting #2: cost 8 inf + 0 1.427 * * [simplify]: Extracting #3: cost 10 inf + 1 1.427 * * [simplify]: Extracting #4: cost 13 inf + 83 1.427 * * [simplify]: Extracting #5: cost 8 inf + 379 1.428 * * [simplify]: Extracting #6: cost 4 inf + 1013 1.428 * * [simplify]: Extracting #7: cost 0 inf + 2179 1.429 * [simplify]: Simplified to (/ (sqrt 2) (sqrt (+ (exp x) (exp (- x))))) 1.429 * [simplify]: Simplified (2 1) to (λ (x) (* (/ (sqrt 2) (sqrt (+ (exp x) (exp (- x))))) (/ (sqrt 2) (sqrt (+ (exp x) (exp (- x))))))) 1.431 * [simplify]: Simplifying (/ (sqrt 2) (sqrt (+ (exp x) (exp (- x))))) 1.431 * * [simplify]: iters left: 6 (9 enodes) 1.435 * * [simplify]: iters left: 5 (30 enodes) 1.445 * * [simplify]: iters left: 4 (34 enodes) 1.454 * * [simplify]: iters left: 3 (36 enodes) 1.465 * * [simplify]: Extracting #0: cost 1 inf + 0 1.465 * * [simplify]: Extracting #1: cost 4 inf + 0 1.465 * * [simplify]: Extracting #2: cost 8 inf + 0 1.465 * * [simplify]: Extracting #3: cost 10 inf + 1 1.465 * * [simplify]: Extracting #4: cost 13 inf + 83 1.465 * * [simplify]: Extracting #5: cost 8 inf + 379 1.465 * * [simplify]: Extracting #6: cost 4 inf + 1013 1.466 * * [simplify]: Extracting #7: cost 0 inf + 2179 1.466 * [simplify]: Simplified to (/ (sqrt 2) (sqrt (+ (exp x) (exp (- x))))) 1.467 * [simplify]: Simplified (2 2) to (λ (x) (* (/ (sqrt 2) (sqrt (+ (exp x) (exp (- x))))) (/ (sqrt 2) (sqrt (+ (exp x) (exp (- x))))))) 1.467 * * * * [progress]: [ 16 / 37 ] simplifiying candidate # 1.467 * [simplify]: Simplifying (/ (sqrt 2) 1) 1.467 * * [simplify]: iters left: 3 (4 enodes) 1.470 * * [simplify]: iters left: 2 (12 enodes) 1.474 * * [simplify]: iters left: 1 (14 enodes) 1.480 * * [simplify]: Extracting #0: cost 1 inf + 0 1.480 * * [simplify]: Extracting #1: cost 4 inf + 0 1.480 * * [simplify]: Extracting #2: cost 0 inf + 84 1.480 * [simplify]: Simplified to (sqrt 2) 1.480 * [simplify]: Simplified (2 1) to (λ (x) (* (sqrt 2) (/ (sqrt 2) (+ (exp x) (exp (- x)))))) 1.480 * [simplify]: Simplifying (/ (sqrt 2) (+ (exp x) (exp (- x)))) 1.481 * * [simplify]: iters left: 6 (8 enodes) 1.485 * * [simplify]: iters left: 5 (27 enodes) 1.493 * * [simplify]: iters left: 4 (31 enodes) 1.503 * * [simplify]: iters left: 3 (33 enodes) 1.513 * * [simplify]: Extracting #0: cost 1 inf + 0 1.513 * * [simplify]: Extracting #1: cost 4 inf + 0 1.513 * * [simplify]: Extracting #2: cost 9 inf + 0 1.513 * * [simplify]: Extracting #3: cost 13 inf + 1 1.513 * * [simplify]: Extracting #4: cost 8 inf + 267 1.514 * * [simplify]: Extracting #5: cost 1 inf + 1275 1.514 * * [simplify]: Extracting #6: cost 0 inf + 1577 1.515 * [simplify]: Simplified to (/ (sqrt 2) (+ (exp x) (exp (- x)))) 1.515 * [simplify]: Simplified (2 2) to (λ (x) (* (sqrt 2) (/ (sqrt 2) (+ (exp x) (exp (- x)))))) 1.515 * * * * [progress]: [ 17 / 37 ] simplifiying candidate # 1.515 * [simplify]: Simplifying (/ (sqrt 2) 1) 1.515 * * [simplify]: iters left: 3 (4 enodes) 1.518 * * [simplify]: iters left: 2 (12 enodes) 1.523 * * [simplify]: iters left: 1 (14 enodes) 1.528 * * [simplify]: Extracting #0: cost 1 inf + 0 1.528 * * [simplify]: Extracting #1: cost 4 inf + 0 1.528 * * [simplify]: Extracting #2: cost 0 inf + 84 1.528 * [simplify]: Simplified to (sqrt 2) 1.528 * [simplify]: Simplified (2 1) to (λ (x) (* (sqrt 2) (/ (sqrt 2) (+ (exp x) (exp (- x)))))) 1.528 * [simplify]: Simplifying (/ (sqrt 2) (+ (exp x) (exp (- x)))) 1.528 * * [simplify]: iters left: 6 (8 enodes) 1.533 * * [simplify]: iters left: 5 (27 enodes) 1.541 * * [simplify]: iters left: 4 (31 enodes) 1.550 * * [simplify]: iters left: 3 (33 enodes) 1.559 * * [simplify]: Extracting #0: cost 1 inf + 0 1.559 * * [simplify]: Extracting #1: cost 4 inf + 0 1.559 * * [simplify]: Extracting #2: cost 9 inf + 0 1.559 * * [simplify]: Extracting #3: cost 13 inf + 1 1.559 * * [simplify]: Extracting #4: cost 8 inf + 267 1.559 * * [simplify]: Extracting #5: cost 1 inf + 1275 1.560 * * [simplify]: Extracting #6: cost 0 inf + 1577 1.560 * [simplify]: Simplified to (/ (sqrt 2) (+ (exp x) (exp (- x)))) 1.560 * [simplify]: Simplified (2 2) to (λ (x) (* (sqrt 2) (/ (sqrt 2) (+ (exp x) (exp (- x)))))) 1.560 * * * * [progress]: [ 18 / 37 ] simplifiying candidate # 1.561 * [simplify]: Simplifying (/ 1 (* (cbrt (+ (exp x) (exp (- x)))) (cbrt (+ (exp x) (exp (- x)))))) 1.561 * * [simplify]: iters left: 6 (9 enodes) 1.565 * * [simplify]: iters left: 5 (33 enodes) 1.574 * * [simplify]: iters left: 4 (37 enodes) 1.585 * * [simplify]: Extracting #0: cost 1 inf + 0 1.585 * * [simplify]: Extracting #1: cost 6 inf + 0 1.585 * * [simplify]: Extracting #2: cost 9 inf + 1 1.585 * * [simplify]: Extracting #3: cost 12 inf + 1 1.585 * * [simplify]: Extracting #4: cost 16 inf + 1 1.585 * * [simplify]: Extracting #5: cost 15 inf + 43 1.585 * * [simplify]: Extracting #6: cost 8 inf + 890 1.586 * * [simplify]: Extracting #7: cost 2 inf + 2858 1.587 * * [simplify]: Extracting #8: cost 0 inf + 3622 1.587 * [simplify]: Simplified to (/ (/ 1 (cbrt (+ (exp x) (exp (- x))))) (cbrt (+ (exp x) (exp (- x))))) 1.587 * [simplify]: Simplified (2 1) to (λ (x) (* (/ (/ 1 (cbrt (+ (exp x) (exp (- x))))) (cbrt (+ (exp x) (exp (- x))))) (/ 2 (cbrt (+ (exp x) (exp (- x))))))) 1.588 * [simplify]: Simplifying (/ 2 (cbrt (+ (exp x) (exp (- x))))) 1.588 * * [simplify]: iters left: 6 (8 enodes) 1.592 * * [simplify]: iters left: 5 (27 enodes) 1.600 * * [simplify]: iters left: 4 (31 enodes) 1.609 * * [simplify]: iters left: 3 (33 enodes) 1.619 * * [simplify]: Extracting #0: cost 1 inf + 0 1.619 * * [simplify]: Extracting #1: cost 4 inf + 0 1.620 * * [simplify]: Extracting #2: cost 5 inf + 1 1.620 * * [simplify]: Extracting #3: cost 8 inf + 1 1.620 * * [simplify]: Extracting #4: cost 13 inf + 1 1.620 * * [simplify]: Extracting #5: cost 11 inf + 44 1.620 * * [simplify]: Extracting #6: cost 5 inf + 670 1.620 * * [simplify]: Extracting #7: cost 1 inf + 1835 1.621 * * [simplify]: Extracting #8: cost 0 inf + 2177 1.621 * [simplify]: Simplified to (/ 2 (cbrt (+ (exp x) (exp (- x))))) 1.621 * [simplify]: Simplified (2 2) to (λ (x) (* (/ 1 (* (cbrt (+ (exp x) (exp (- x)))) (cbrt (+ (exp x) (exp (- x)))))) (/ 2 (cbrt (+ (exp x) (exp (- x))))))) 1.621 * * * * [progress]: [ 19 / 37 ] simplifiying candidate # 1.622 * [simplify]: Simplifying (/ 1 (sqrt (+ (exp x) (exp (- x))))) 1.622 * * [simplify]: iters left: 6 (8 enodes) 1.626 * * [simplify]: iters left: 5 (28 enodes) 1.634 * * [simplify]: iters left: 4 (30 enodes) 1.642 * * [simplify]: Extracting #0: cost 1 inf + 0 1.642 * * [simplify]: Extracting #1: cost 4 inf + 0 1.642 * * [simplify]: Extracting #2: cost 5 inf + 1 1.642 * * [simplify]: Extracting #3: cost 8 inf + 1 1.642 * * [simplify]: Extracting #4: cost 12 inf + 1 1.642 * * [simplify]: Extracting #5: cost 11 inf + 43 1.642 * * [simplify]: Extracting #6: cost 6 inf + 558 1.643 * * [simplify]: Extracting #7: cost 2 inf + 1453 1.643 * * [simplify]: Extracting #8: cost 0 inf + 2016 1.644 * [simplify]: Simplified to (/ 1 (sqrt (+ (exp x) (exp (- x))))) 1.644 * [simplify]: Simplified (2 1) to (λ (x) (* (/ 1 (sqrt (+ (exp x) (exp (- x))))) (/ 2 (sqrt (+ (exp x) (exp (- x))))))) 1.644 * [simplify]: Simplifying (/ 2 (sqrt (+ (exp x) (exp (- x))))) 1.644 * * [simplify]: iters left: 6 (8 enodes) 1.648 * * [simplify]: iters left: 5 (27 enodes) 1.656 * * [simplify]: iters left: 4 (31 enodes) 1.665 * * [simplify]: iters left: 3 (33 enodes) 1.674 * * [simplify]: Extracting #0: cost 1 inf + 0 1.674 * * [simplify]: Extracting #1: cost 4 inf + 0 1.674 * * [simplify]: Extracting #2: cost 5 inf + 1 1.674 * * [simplify]: Extracting #3: cost 8 inf + 1 1.674 * * [simplify]: Extracting #4: cost 13 inf + 1 1.674 * * [simplify]: Extracting #5: cost 11 inf + 44 1.674 * * [simplify]: Extracting #6: cost 5 inf + 670 1.674 * * [simplify]: Extracting #7: cost 1 inf + 1715 1.675 * * [simplify]: Extracting #8: cost 0 inf + 2017 1.675 * [simplify]: Simplified to (/ 2 (sqrt (+ (exp x) (exp (- x))))) 1.675 * [simplify]: Simplified (2 2) to (λ (x) (* (/ 1 (sqrt (+ (exp x) (exp (- x))))) (/ 2 (sqrt (+ (exp x) (exp (- x))))))) 1.675 * * * * [progress]: [ 20 / 37 ] simplifiying candidate # 1.675 * [simplify]: Simplifying (/ 1 1) 1.675 * * [simplify]: iters left: 2 (2 enodes) 1.676 * * [simplify]: iters left: 1 (6 enodes) 1.677 * * [simplify]: Extracting #0: cost 1 inf + 0 1.677 * * [simplify]: Extracting #1: cost 0 inf + 1 1.677 * [simplify]: Simplified to 1 1.677 * [simplify]: Simplified (2 1) to (λ (x) (* 1 (/ 2 (+ (exp x) (exp (- x)))))) 1.677 * [simplify]: Simplifying (/ 2 (+ (exp x) (exp (- x)))) 1.677 * * [simplify]: iters left: 6 (7 enodes) 1.679 * * [simplify]: iters left: 5 (24 enodes) 1.683 * * [simplify]: iters left: 4 (28 enodes) 1.687 * * [simplify]: iters left: 3 (30 enodes) 1.692 * * [simplify]: Extracting #0: cost 1 inf + 0 1.692 * * [simplify]: Extracting #1: cost 4 inf + 0 1.692 * * [simplify]: Extracting #2: cost 6 inf + 1 1.692 * * [simplify]: Extracting #3: cost 11 inf + 1 1.692 * * [simplify]: Extracting #4: cost 9 inf + 44 1.692 * * [simplify]: Extracting #5: cost 3 inf + 670 1.692 * * [simplify]: Extracting #6: cost 1 inf + 1153 1.692 * * [simplify]: Extracting #7: cost 0 inf + 1415 1.692 * [simplify]: Simplified to (/ 2 (+ (exp x) (exp (- x)))) 1.692 * [simplify]: Simplified (2 2) to (λ (x) (* 1 (/ 2 (+ (exp x) (exp (- x)))))) 1.693 * * * * [progress]: [ 21 / 37 ] simplifiying candidate # 1.693 * [simplify]: Simplifying (/ 1 1) 1.693 * * [simplify]: iters left: 2 (2 enodes) 1.694 * * [simplify]: iters left: 1 (6 enodes) 1.695 * * [simplify]: Extracting #0: cost 1 inf + 0 1.695 * * [simplify]: Extracting #1: cost 0 inf + 1 1.695 * [simplify]: Simplified to 1 1.695 * [simplify]: Simplified (2 1) to (λ (x) (* 1 (/ 2 (+ (exp x) (exp (- x)))))) 1.695 * [simplify]: Simplifying (/ 2 (+ (exp x) (exp (- x)))) 1.695 * * [simplify]: iters left: 6 (7 enodes) 1.697 * * [simplify]: iters left: 5 (24 enodes) 1.700 * * [simplify]: iters left: 4 (28 enodes) 1.705 * * [simplify]: iters left: 3 (30 enodes) 1.711 * * [simplify]: Extracting #0: cost 1 inf + 0 1.711 * * [simplify]: Extracting #1: cost 4 inf + 0 1.711 * * [simplify]: Extracting #2: cost 6 inf + 1 1.711 * * [simplify]: Extracting #3: cost 11 inf + 1 1.711 * * [simplify]: Extracting #4: cost 9 inf + 44 1.711 * * [simplify]: Extracting #5: cost 3 inf + 670 1.711 * * [simplify]: Extracting #6: cost 1 inf + 1153 1.711 * * [simplify]: Extracting #7: cost 0 inf + 1415 1.711 * [simplify]: Simplified to (/ 2 (+ (exp x) (exp (- x)))) 1.711 * [simplify]: Simplified (2 2) to (λ (x) (* 1 (/ 2 (+ (exp x) (exp (- x)))))) 1.712 * * * * [progress]: [ 22 / 37 ] simplifiying candidate # 1.712 * * * * [progress]: [ 23 / 37 ] simplifiying candidate # 1.712 * [simplify]: Simplifying (/ 1 (+ (exp x) (exp (- x)))) 1.712 * * [simplify]: iters left: 6 (7 enodes) 1.714 * * [simplify]: iters left: 5 (25 enodes) 1.717 * * [simplify]: iters left: 4 (27 enodes) 1.722 * * [simplify]: Extracting #0: cost 1 inf + 0 1.722 * * [simplify]: Extracting #1: cost 4 inf + 0 1.722 * * [simplify]: Extracting #2: cost 6 inf + 1 1.722 * * [simplify]: Extracting #3: cost 10 inf + 1 1.722 * * [simplify]: Extracting #4: cost 1 inf + 1373 1.722 * * [simplify]: Extracting #5: cost 0 inf + 1414 1.722 * [simplify]: Simplified to (/ 1 (+ (exp x) (exp (- x)))) 1.722 * [simplify]: Simplified (2 2) to (λ (x) (* 2 (/ 1 (+ (exp x) (exp (- x)))))) 1.722 * * * * [progress]: [ 24 / 37 ] simplifiying candidate # 1.722 * [simplify]: Simplifying (/ (+ (exp x) (exp (- x))) 2) 1.722 * * [simplify]: iters left: 6 (7 enodes) 1.724 * * [simplify]: iters left: 5 (24 enodes) 1.728 * * [simplify]: iters left: 4 (28 enodes) 1.733 * * [simplify]: iters left: 3 (30 enodes) 1.737 * * [simplify]: Extracting #0: cost 1 inf + 0 1.737 * * [simplify]: Extracting #1: cost 4 inf + 0 1.737 * * [simplify]: Extracting #2: cost 6 inf + 1 1.738 * * [simplify]: Extracting #3: cost 11 inf + 1 1.738 * * [simplify]: Extracting #4: cost 10 inf + 3 1.738 * * [simplify]: Extracting #5: cost 4 inf + 449 1.738 * * [simplify]: Extracting #6: cost 1 inf + 1153 1.738 * * [simplify]: Extracting #7: cost 0 inf + 1415 1.738 * [simplify]: Simplified to (/ (+ (exp x) (exp (- x))) 2) 1.738 * [simplify]: Simplified (2 2) to (λ (x) (/ 1 (/ (+ (exp x) (exp (- x))) 2))) 1.738 * * * * [progress]: [ 25 / 37 ] simplifiying candidate # 1.738 * [simplify]: Simplifying (/ 2 (* (cbrt (+ (exp x) (exp (- x)))) (cbrt (+ (exp x) (exp (- x)))))) 1.739 * * [simplify]: iters left: 6 (9 enodes) 1.741 * * [simplify]: iters left: 5 (32 enodes) 1.746 * * [simplify]: iters left: 4 (38 enodes) 1.753 * * [simplify]: iters left: 3 (40 enodes) 1.764 * * [simplify]: Extracting #0: cost 1 inf + 0 1.764 * * [simplify]: Extracting #1: cost 6 inf + 0 1.764 * * [simplify]: Extracting #2: cost 9 inf + 1 1.764 * * [simplify]: Extracting #3: cost 12 inf + 1 1.764 * * [simplify]: Extracting #4: cost 17 inf + 1 1.764 * * [simplify]: Extracting #5: cost 15 inf + 44 1.765 * * [simplify]: Extracting #6: cost 9 inf + 780 1.765 * * [simplify]: Extracting #7: cost 4 inf + 2176 1.766 * * [simplify]: Extracting #8: cost 0 inf + 3623 1.766 * [simplify]: Simplified to (/ (/ 2 (cbrt (+ (exp x) (exp (- x))))) (cbrt (+ (exp x) (exp (- x))))) 1.767 * [simplify]: Simplified (2 1) to (λ (x) (/ (/ (/ 2 (cbrt (+ (exp x) (exp (- x))))) (cbrt (+ (exp x) (exp (- x))))) (cbrt (+ (exp x) (exp (- x)))))) 1.767 * * * * [progress]: [ 26 / 37 ] simplifiying candidate # 1.767 * [simplify]: Simplifying (/ 2 (sqrt (+ (exp x) (exp (- x))))) 1.767 * * [simplify]: iters left: 6 (8 enodes) 1.771 * * [simplify]: iters left: 5 (27 enodes) 1.779 * * [simplify]: iters left: 4 (31 enodes) 1.788 * * [simplify]: iters left: 3 (33 enodes) 1.798 * * [simplify]: Extracting #0: cost 1 inf + 0 1.798 * * [simplify]: Extracting #1: cost 4 inf + 0 1.798 * * [simplify]: Extracting #2: cost 5 inf + 1 1.798 * * [simplify]: Extracting #3: cost 8 inf + 1 1.798 * * [simplify]: Extracting #4: cost 13 inf + 1 1.798 * * [simplify]: Extracting #5: cost 11 inf + 44 1.799 * * [simplify]: Extracting #6: cost 5 inf + 670 1.799 * * [simplify]: Extracting #7: cost 1 inf + 1715 1.799 * * [simplify]: Extracting #8: cost 0 inf + 2017 1.800 * [simplify]: Simplified to (/ 2 (sqrt (+ (exp x) (exp (- x))))) 1.800 * [simplify]: Simplified (2 1) to (λ (x) (/ (/ 2 (sqrt (+ (exp x) (exp (- x))))) (sqrt (+ (exp x) (exp (- x)))))) 1.800 * * * * [progress]: [ 27 / 37 ] simplifiying candidate # 1.800 * [simplify]: Simplifying (/ 2 1) 1.800 * * [simplify]: iters left: 2 (3 enodes) 1.803 * * [simplify]: iters left: 1 (9 enodes) 1.806 * * [simplify]: Extracting #0: cost 1 inf + 0 1.806 * * [simplify]: Extracting #1: cost 0 inf + 1 1.806 * [simplify]: Simplified to 2 1.806 * [simplify]: Simplified (2 1) to (λ (x) (/ 2 (+ (exp x) (exp (- x))))) 1.806 * * * * [progress]: [ 28 / 37 ] simplifiying candidate # 1.806 * [simplify]: Simplifying (/ 2 1) 1.806 * * [simplify]: iters left: 2 (3 enodes) 1.809 * * [simplify]: iters left: 1 (9 enodes) 1.812 * * [simplify]: Extracting #0: cost 1 inf + 0 1.812 * * [simplify]: Extracting #1: cost 0 inf + 1 1.812 * [simplify]: Simplified to 2 1.812 * [simplify]: Simplified (2 1) to (λ (x) (/ 2 (+ (exp x) (exp (- x))))) 1.812 * * * * [progress]: [ 29 / 37 ] simplifiying candidate # 1.812 * [simplify]: Simplifying (/ (+ (exp x) (exp (- x))) (cbrt 2)) 1.812 * * [simplify]: iters left: 6 (8 enodes) 1.816 * * [simplify]: iters left: 5 (27 enodes) 1.821 * * [simplify]: iters left: 4 (31 enodes) 1.828 * * [simplify]: iters left: 3 (33 enodes) 1.833 * * [simplify]: Extracting #0: cost 1 inf + 0 1.833 * * [simplify]: Extracting #1: cost 4 inf + 0 1.833 * * [simplify]: Extracting #2: cost 9 inf + 0 1.833 * * [simplify]: Extracting #3: cost 12 inf + 82 1.833 * * [simplify]: Extracting #4: cost 10 inf + 165 1.833 * * [simplify]: Extracting #5: cost 6 inf + 429 1.834 * * [simplify]: Extracting #6: cost 1 inf + 1395 1.834 * * [simplify]: Extracting #7: cost 0 inf + 1737 1.834 * [simplify]: Simplified to (/ (+ (exp x) (exp (- x))) (cbrt 2)) 1.834 * [simplify]: Simplified (2 2) to (λ (x) (/ (* (cbrt 2) (cbrt 2)) (/ (+ (exp x) (exp (- x))) (cbrt 2)))) 1.834 * * * * [progress]: [ 30 / 37 ] simplifiying candidate # 1.834 * [simplify]: Simplifying (/ (+ (exp x) (exp (- x))) (sqrt 2)) 1.835 * * [simplify]: iters left: 6 (8 enodes) 1.837 * * [simplify]: iters left: 5 (27 enodes) 1.841 * * [simplify]: iters left: 4 (31 enodes) 1.846 * * [simplify]: iters left: 3 (33 enodes) 1.851 * * [simplify]: Extracting #0: cost 1 inf + 0 1.851 * * [simplify]: Extracting #1: cost 4 inf + 0 1.851 * * [simplify]: Extracting #2: cost 9 inf + 0 1.852 * * [simplify]: Extracting #3: cost 12 inf + 42 1.852 * * [simplify]: Extracting #4: cost 10 inf + 85 1.852 * * [simplify]: Extracting #5: cost 6 inf + 349 1.852 * * [simplify]: Extracting #6: cost 1 inf + 1275 1.852 * * [simplify]: Extracting #7: cost 0 inf + 1577 1.852 * [simplify]: Simplified to (/ (+ (exp x) (exp (- x))) (sqrt 2)) 1.852 * [simplify]: Simplified (2 2) to (λ (x) (/ (sqrt 2) (/ (+ (exp x) (exp (- x))) (sqrt 2)))) 1.852 * * * * [progress]: [ 31 / 37 ] simplifiying candidate # 1.853 * [simplify]: Simplifying (/ (+ (exp x) (exp (- x))) 2) 1.853 * * [simplify]: iters left: 6 (7 enodes) 1.856 * * [simplify]: iters left: 5 (24 enodes) 1.863 * * [simplify]: iters left: 4 (28 enodes) 1.872 * * [simplify]: iters left: 3 (30 enodes) 1.881 * * [simplify]: Extracting #0: cost 1 inf + 0 1.881 * * [simplify]: Extracting #1: cost 4 inf + 0 1.881 * * [simplify]: Extracting #2: cost 6 inf + 1 1.881 * * [simplify]: Extracting #3: cost 11 inf + 1 1.881 * * [simplify]: Extracting #4: cost 10 inf + 3 1.881 * * [simplify]: Extracting #5: cost 4 inf + 449 1.882 * * [simplify]: Extracting #6: cost 1 inf + 1153 1.882 * * [simplify]: Extracting #7: cost 0 inf + 1415 1.882 * [simplify]: Simplified to (/ (+ (exp x) (exp (- x))) 2) 1.882 * [simplify]: Simplified (2 2) to (λ (x) (/ 1 (/ (+ (exp x) (exp (- x))) 2))) 1.883 * * * * [progress]: [ 32 / 37 ] simplifiying candidate # 1.883 * [simplify]: Simplifying (/ 2 (+ (pow (exp x) 3) (pow (exp (- x)) 3))) 1.883 * * [simplify]: iters left: 6 (10 enodes) 1.889 * * [simplify]: iters left: 5 (45 enodes) 1.908 * * [simplify]: iters left: 4 (88 enodes) 1.945 * * [simplify]: iters left: 3 (168 enodes) 1.995 * * [simplify]: iters left: 2 (282 enodes) 2.077 * * [simplify]: Extracting #0: cost 1 inf + 0 2.078 * * [simplify]: Extracting #1: cost 4 inf + 0 2.078 * * [simplify]: Extracting #2: cost 6 inf + 1 2.078 * * [simplify]: Extracting #3: cost 58 inf + 1 2.078 * * [simplify]: Extracting #4: cost 110 inf + 4 2.079 * * [simplify]: Extracting #5: cost 95 inf + 5306 2.085 * * [simplify]: Extracting #6: cost 20 inf + 34261 2.092 * * [simplify]: Extracting #7: cost 1 inf + 43422 2.099 * * [simplify]: Extracting #8: cost 0 inf + 43844 2.107 * [simplify]: Simplified to (/ 2 (+ (exp (- (- x) (- x (- x)))) (* (exp x) (* (exp x) (exp x))))) 2.107 * [simplify]: Simplified (2 1) to (λ (x) (* (/ 2 (+ (exp (- (- x) (- x (- x)))) (* (exp x) (* (exp x) (exp x))))) (+ (* (exp x) (exp x)) (- (* (exp (- x)) (exp (- x))) (* (exp x) (exp (- x))))))) 2.107 * * * * [progress]: [ 33 / 37 ] simplifiying candidate # 2.107 * [simplify]: Simplifying (/ 2 (- (* (exp x) (exp x)) (* (exp (- x)) (exp (- x))))) 2.108 * * [simplify]: iters left: 6 (9 enodes) 2.112 * * [simplify]: iters left: 5 (38 enodes) 2.125 * * [simplify]: iters left: 4 (67 enodes) 2.143 * * [simplify]: iters left: 3 (103 enodes) 2.165 * * [simplify]: iters left: 2 (167 enodes) 2.215 * * [simplify]: iters left: 1 (237 enodes) 2.264 * * [simplify]: Extracting #0: cost 1 inf + 0 2.264 * * [simplify]: Extracting #1: cost 6 inf + 0 2.264 * * [simplify]: Extracting #2: cost 42 inf + 1 2.264 * * [simplify]: Extracting #3: cost 68 inf + 3 2.264 * * [simplify]: Extracting #4: cost 77 inf + 45 2.265 * * [simplify]: Extracting #5: cost 36 inf + 6786 2.267 * * [simplify]: Extracting #6: cost 4 inf + 13605 2.270 * * [simplify]: Extracting #7: cost 0 inf + 14593 2.273 * [simplify]: Simplified to (/ 2 (- (exp (+ x x)) (exp (- (+ x x))))) 2.273 * [simplify]: Simplified (2 1) to (λ (x) (* (/ 2 (- (exp (+ x x)) (exp (- (+ x x))))) (- (exp x) (exp (- x))))) 2.273 * * * * [progress]: [ 34 / 37 ] simplifiying candidate #real (real->posit16 (/ 2 (+ (exp x) (exp (- x)))))))> 2.273 * [simplify]: Simplifying (real->posit16 (/ 2 (+ (exp x) (exp (- x))))) 2.273 * * [simplify]: iters left: 6 (8 enodes) 2.275 * * [simplify]: iters left: 5 (24 enodes) 2.279 * * [simplify]: iters left: 4 (28 enodes) 2.283 * * [simplify]: iters left: 3 (30 enodes) 2.290 * * [simplify]: Extracting #0: cost 1 inf + 0 2.290 * * [simplify]: Extracting #1: cost 2 inf + 0 2.290 * * [simplify]: Extracting #2: cost 4 inf + 0 2.290 * * [simplify]: Extracting #3: cost 6 inf + 1 2.290 * * [simplify]: Extracting #4: cost 11 inf + 1 2.290 * * [simplify]: Extracting #5: cost 1 inf + 1374 2.290 * * [simplify]: Extracting #6: cost 0 inf + 1415 2.291 * [simplify]: Simplified to (real->posit16 (/ 2 (+ (exp x) (exp (- x))))) 2.291 * [simplify]: Simplified (2 1) to (λ (x) (posit16->real (real->posit16 (/ 2 (+ (exp x) (exp (- x))))))) 2.291 * * * * [progress]: [ 35 / 37 ] simplifiying candidate # 2.291 * [simplify]: Simplifying (- (+ (* 5/24 (pow x 4)) 1) (* 1/2 (pow x 2))) 2.292 * * [simplify]: iters left: 6 (12 enodes) 2.300 * * [simplify]: iters left: 5 (52 enodes) 2.318 * * [simplify]: iters left: 4 (79 enodes) 2.342 * * [simplify]: iters left: 3 (115 enodes) 2.372 * * [simplify]: iters left: 2 (163 enodes) 2.405 * * [simplify]: iters left: 1 (259 enodes) 2.496 * * [simplify]: Extracting #0: cost 1 inf + 0 2.496 * * [simplify]: Extracting #1: cost 16 inf + 0 2.496 * * [simplify]: Extracting #2: cost 56 inf + 1 2.497 * * [simplify]: Extracting #3: cost 79 inf + 129 2.499 * * [simplify]: Extracting #4: cost 29 inf + 5068 2.503 * * [simplify]: Extracting #5: cost 0 inf + 9151 2.507 * * [simplify]: Extracting #6: cost 0 inf + 9031 2.511 * [simplify]: Simplified to (- 1 (* (+ (* (* x x) -5/24) 1/2) (* x x))) 2.511 * [simplify]: Simplified (2) to (λ (x) (- 1 (* (+ (* (* x x) -5/24) 1/2) (* x x)))) 2.511 * * * * [progress]: [ 36 / 37 ] simplifiying candidate # 2.511 * [simplify]: Simplifying (/ 2 (+ (exp x) (exp (- x)))) 2.511 * * [simplify]: iters left: 6 (7 enodes) 2.514 * * [simplify]: iters left: 5 (24 enodes) 2.521 * * [simplify]: iters left: 4 (28 enodes) 2.529 * * [simplify]: iters left: 3 (30 enodes) 2.536 * * [simplify]: Extracting #0: cost 1 inf + 0 2.536 * * [simplify]: Extracting #1: cost 4 inf + 0 2.536 * * [simplify]: Extracting #2: cost 6 inf + 1 2.536 * * [simplify]: Extracting #3: cost 11 inf + 1 2.536 * * [simplify]: Extracting #4: cost 9 inf + 44 2.536 * * [simplify]: Extracting #5: cost 3 inf + 670 2.537 * * [simplify]: Extracting #6: cost 1 inf + 1153 2.537 * * [simplify]: Extracting #7: cost 0 inf + 1415 2.537 * [simplify]: Simplified to (/ 2 (+ (exp x) (exp (- x)))) 2.537 * [simplify]: Simplified (2) to (λ (x) (/ 2 (+ (exp x) (exp (- x))))) 2.537 * * * * [progress]: [ 37 / 37 ] simplifiying candidate # 2.538 * [simplify]: Simplifying (/ 2 (+ (exp (* -1 x)) (exp x))) 2.538 * * [simplify]: iters left: 6 (8 enodes) 2.542 * * [simplify]: iters left: 5 (29 enodes) 2.549 * * [simplify]: iters left: 4 (37 enodes) 2.559 * * [simplify]: iters left: 3 (50 enodes) 2.574 * * [simplify]: iters left: 2 (80 enodes) 2.602 * * [simplify]: iters left: 1 (144 enodes) 2.651 * * [simplify]: Extracting #0: cost 1 inf + 0 2.651 * * [simplify]: Extracting #1: cost 4 inf + 0 2.651 * * [simplify]: Extracting #2: cost 6 inf + 1 2.651 * * [simplify]: Extracting #3: cost 27 inf + 1 2.652 * * [simplify]: Extracting #4: cost 62 inf + 228 2.652 * * [simplify]: Extracting #5: cost 64 inf + 1536 2.654 * * [simplify]: Extracting #6: cost 27 inf + 9171 2.657 * * [simplify]: Extracting #7: cost 9 inf + 18092 2.661 * * [simplify]: Extracting #8: cost 0 inf + 23726 2.665 * [simplify]: Simplified to (/ 2 (+ (exp x) (exp (- x)))) 2.665 * [simplify]: Simplified (2) to (λ (x) (/ 2 (+ (exp x) (exp (- x))))) 2.665 * * * [progress]: adding candidates to table 3.007 * * [progress]: iteration 2 / 4 3.007 * * * [progress]: picking best candidate 3.010 * * * * [pick]: Picked # 3.010 * * * [progress]: localizing error 3.025 * * * [progress]: generating rewritten candidates 3.025 * * * * [progress]: [ 1 / 1 ] rewriting at (2) 3.081 * * * [progress]: generating series expansions 3.081 * * * * [progress]: [ 1 / 1 ] generating series at (2) 3.082 * [backup-simplify]: Simplify (* (sqrt 2) (/ (sqrt 2) (+ (exp x) (exp (- x))))) into (/ (pow (sqrt 2) 2) (+ (exp x) (exp (- x)))) 3.082 * [approximate]: Taking taylor expansion of (/ (pow (sqrt 2) 2) (+ (exp x) (exp (- x)))) in (x) around 0 3.082 * [taylor]: Taking taylor expansion of (/ (pow (sqrt 2) 2) (+ (exp x) (exp (- x)))) in x 3.082 * [taylor]: Taking taylor expansion of (pow (sqrt 2) 2) in x 3.082 * [taylor]: Taking taylor expansion of (sqrt 2) in x 3.082 * [taylor]: Taking taylor expansion of 2 in x 3.082 * [backup-simplify]: Simplify 2 into 2 3.082 * [backup-simplify]: Simplify (sqrt 2) into (sqrt 2) 3.083 * [backup-simplify]: Simplify (/ 0 (* 2 (sqrt 2))) into 0 3.083 * [taylor]: Taking taylor expansion of (+ (exp x) (exp (- x))) in x 3.083 * [taylor]: Taking taylor expansion of (exp x) in x 3.083 * [taylor]: Taking taylor expansion of x in x 3.083 * [backup-simplify]: Simplify 0 into 0 3.083 * [backup-simplify]: Simplify 1 into 1 3.083 * [backup-simplify]: Simplify (exp 0) into 1 3.083 * [taylor]: Taking taylor expansion of (exp (- x)) in x 3.083 * [taylor]: Taking taylor expansion of (- x) in x 3.083 * [taylor]: Taking taylor expansion of x in x 3.083 * [backup-simplify]: Simplify 0 into 0 3.083 * [backup-simplify]: Simplify 1 into 1 3.083 * [backup-simplify]: Simplify (- 0) into 0 3.083 * [backup-simplify]: Simplify (- 1) into -1 3.083 * [backup-simplify]: Simplify (exp 0) into 1 3.084 * [backup-simplify]: Simplify (* (sqrt 2) (sqrt 2)) into (pow (sqrt 2) 2) 3.084 * [backup-simplify]: Simplify (+ 1 1) into 2 3.085 * [backup-simplify]: Simplify (/ (pow (sqrt 2) 2) 2) into (* 1/2 (pow (sqrt 2) 2)) 3.085 * [taylor]: Taking taylor expansion of (/ (pow (sqrt 2) 2) (+ (exp x) (exp (- x)))) in x 3.085 * [taylor]: Taking taylor expansion of (pow (sqrt 2) 2) in x 3.085 * [taylor]: Taking taylor expansion of (sqrt 2) in x 3.085 * [taylor]: Taking taylor expansion of 2 in x 3.085 * [backup-simplify]: Simplify 2 into 2 3.085 * [backup-simplify]: Simplify (sqrt 2) into (sqrt 2) 3.086 * [backup-simplify]: Simplify (/ 0 (* 2 (sqrt 2))) into 0 3.086 * [taylor]: Taking taylor expansion of (+ (exp x) (exp (- x))) in x 3.086 * [taylor]: Taking taylor expansion of (exp x) in x 3.086 * [taylor]: Taking taylor expansion of x in x 3.086 * [backup-simplify]: Simplify 0 into 0 3.086 * [backup-simplify]: Simplify 1 into 1 3.086 * [backup-simplify]: Simplify (exp 0) into 1 3.086 * [taylor]: Taking taylor expansion of (exp (- x)) in x 3.086 * [taylor]: Taking taylor expansion of (- x) in x 3.086 * [taylor]: Taking taylor expansion of x in x 3.086 * [backup-simplify]: Simplify 0 into 0 3.086 * [backup-simplify]: Simplify 1 into 1 3.086 * [backup-simplify]: Simplify (- 0) into 0 3.087 * [backup-simplify]: Simplify (- 1) into -1 3.087 * [backup-simplify]: Simplify (exp 0) into 1 3.087 * [backup-simplify]: Simplify (* (sqrt 2) (sqrt 2)) into (pow (sqrt 2) 2) 3.088 * [backup-simplify]: Simplify (+ 1 1) into 2 3.088 * [backup-simplify]: Simplify (/ (pow (sqrt 2) 2) 2) into (* 1/2 (pow (sqrt 2) 2)) 3.089 * [backup-simplify]: Simplify (* 1/2 (pow (sqrt 2) 2)) into (* 1/2 (pow (sqrt 2) 2)) 3.090 * [backup-simplify]: Simplify (+ (* (sqrt 2) 0) (* 0 (sqrt 2))) into 0 3.090 * [backup-simplify]: Simplify (* (exp 0) (+ (* (/ (pow 1 1) 1)))) into 1 3.091 * [backup-simplify]: Simplify (- 1) into -1 3.091 * [backup-simplify]: Simplify (* (exp 0) (+ (* (/ (pow -1 1) 1)))) into -1 3.092 * [backup-simplify]: Simplify (+ 1 -1) into 0 3.092 * [backup-simplify]: Simplify (- (/ 0 2) (+ (* (* 1/2 (pow (sqrt 2) 2)) (/ 0 2)))) into 0 3.092 * [backup-simplify]: Simplify 0 into 0 3.093 * [backup-simplify]: Simplify (/ (- 0 (pow 0 2) (+)) (* 2 (sqrt 2))) into 0 3.094 * [backup-simplify]: Simplify (+ (* (sqrt 2) 0) (+ (* 0 0) (* 0 (sqrt 2)))) into 0 3.094 * [backup-simplify]: Simplify (* (exp 0) (+ (* (/ (pow 1 2) 2)) (* (/ (pow 0 1) 1)))) into 1/2 3.095 * [backup-simplify]: Simplify (- 1) into -1 3.095 * [backup-simplify]: Simplify (- 0) into 0 3.096 * [backup-simplify]: Simplify (* (exp 0) (+ (* (/ (pow -1 2) 2)) (* (/ (pow 0 1) 1)))) into 1/2 3.096 * [backup-simplify]: Simplify (+ 1/2 1/2) into 1 3.100 * [backup-simplify]: Simplify (- (/ 0 2) (+ (* (* 1/2 (pow (sqrt 2) 2)) (/ 1 2)) (* 0 (/ 0 2)))) into (- (* 1/4 (pow (sqrt 2) 2))) 3.101 * [backup-simplify]: Simplify (- (* 1/4 (pow (sqrt 2) 2))) into (- (* 1/4 (pow (sqrt 2) 2))) 3.102 * [backup-simplify]: Simplify (/ (- 0 (+ (* 2 (* 0 0)))) (* 2 (sqrt 2))) into 0 3.103 * [backup-simplify]: Simplify (+ (* (sqrt 2) 0) (+ (* 0 0) (+ (* 0 0) (* 0 (sqrt 2))))) into 0 3.104 * [backup-simplify]: Simplify (* (exp 0) (+ (* (/ (pow 1 3) 6)) (* (/ (pow 1 1) 1) (/ (pow 0 1) 1)) (* (/ (pow 0 1) 1)))) into 1/6 3.104 * [backup-simplify]: Simplify (- 1) into -1 3.105 * [backup-simplify]: Simplify (- 1) into -1 3.105 * [backup-simplify]: Simplify (- 0) into 0 3.105 * [backup-simplify]: Simplify (- 0) into 0 3.107 * [backup-simplify]: Simplify (* (exp 0) (+ (* (/ (pow -1 3) 6)) (* (/ (pow -1 1) 1) (/ (pow 0 1) 1)) (* (/ (pow 0 1) 1)))) into -1/6 3.107 * [backup-simplify]: Simplify (+ 1/6 -1/6) into 0 3.108 * [backup-simplify]: Simplify (- (/ 0 2) (+ (* (* 1/2 (pow (sqrt 2) 2)) (/ 0 2)) (* 0 (/ 1 2)) (* (- (* 1/4 (pow (sqrt 2) 2))) (/ 0 2)))) into 0 3.108 * [backup-simplify]: Simplify 0 into 0 3.109 * [backup-simplify]: Simplify (/ (- 0 (pow 0 2) (+ (* 2 (* 0 0)))) (* 2 (sqrt 2))) into 0 3.110 * [backup-simplify]: Simplify (+ (* (sqrt 2) 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (* 0 (sqrt 2)))))) into 0 3.112 * [backup-simplify]: Simplify (* (exp 0) (+ (* (/ (pow 1 4) 24)) (* (/ (pow 1 2) 2) (/ (pow 0 1) 1)) (* (/ (pow 1 1) 1) (/ (pow 0 1) 1)) (* (/ (pow 0 2) 2)) (* (/ (pow 0 1) 1)))) into 1/24 3.112 * [backup-simplify]: Simplify (- 1) into -1 3.112 * [backup-simplify]: Simplify (- 1) into -1 3.113 * [backup-simplify]: Simplify (- 0) into 0 3.113 * [backup-simplify]: Simplify (- 1) into -1 3.113 * [backup-simplify]: Simplify (- 0) into 0 3.113 * [backup-simplify]: Simplify (- 0) into 0 3.114 * [backup-simplify]: Simplify (- 0) into 0 3.116 * [backup-simplify]: Simplify (* (exp 0) (+ (* (/ (pow -1 4) 24)) (* (/ (pow -1 2) 2) (/ (pow 0 1) 1)) (* (/ (pow -1 1) 1) (/ (pow 0 1) 1)) (* (/ (pow 0 2) 2)) (* (/ (pow 0 1) 1)))) into 1/24 3.116 * [backup-simplify]: Simplify (+ 1/24 1/24) into 1/12 3.124 * [backup-simplify]: Simplify (- (/ 0 2) (+ (* (* 1/2 (pow (sqrt 2) 2)) (/ 1/12 2)) (* 0 (/ 0 2)) (* (- (* 1/4 (pow (sqrt 2) 2))) (/ 1 2)) (* 0 (/ 0 2)))) into (* 5/48 (pow (sqrt 2) 2)) 3.124 * [backup-simplify]: Simplify (* 5/48 (pow (sqrt 2) 2)) into (* 5/48 (pow (sqrt 2) 2)) 3.128 * [backup-simplify]: Simplify (+ (* (* 5/48 (pow (sqrt 2) 2)) (pow x 4)) (+ (* (- (* 1/4 (pow (sqrt 2) 2))) (pow x 2)) (* 1/2 (pow (sqrt 2) 2)))) into (- (+ (* 1/2 (pow (sqrt 2) 2)) (* 5/48 (* (pow (sqrt 2) 2) (pow x 4)))) (* 1/4 (* (pow (sqrt 2) 2) (pow x 2)))) 3.128 * [backup-simplify]: Simplify (* (sqrt 2) (/ (sqrt 2) (+ (exp (/ 1 x)) (exp (- (/ 1 x)))))) into (/ (pow (sqrt 2) 2) (+ (exp (/ 1 x)) (exp (- (/ 1 x))))) 3.128 * [approximate]: Taking taylor expansion of (/ (pow (sqrt 2) 2) (+ (exp (/ 1 x)) (exp (- (/ 1 x))))) in (x) around 0 3.128 * [taylor]: Taking taylor expansion of (/ (pow (sqrt 2) 2) (+ (exp (/ 1 x)) (exp (- (/ 1 x))))) in x 3.128 * [taylor]: Taking taylor expansion of (pow (sqrt 2) 2) in x 3.128 * [taylor]: Taking taylor expansion of (sqrt 2) in x 3.128 * [taylor]: Taking taylor expansion of 2 in x 3.128 * [backup-simplify]: Simplify 2 into 2 3.129 * [backup-simplify]: Simplify (sqrt 2) into (sqrt 2) 3.129 * [backup-simplify]: Simplify (/ 0 (* 2 (sqrt 2))) into 0 3.129 * [taylor]: Taking taylor expansion of (+ (exp (/ 1 x)) (exp (- (/ 1 x)))) in x 3.129 * [taylor]: Taking taylor expansion of (exp (/ 1 x)) in x 3.129 * [taylor]: Taking taylor expansion of (/ 1 x) in x 3.129 * [taylor]: Taking taylor expansion of x in x 3.129 * [backup-simplify]: Simplify 0 into 0 3.129 * [backup-simplify]: Simplify 1 into 1 3.129 * [backup-simplify]: Simplify (/ 1 1) into 1 3.129 * [backup-simplify]: Simplify (exp (/ 1 x)) into (exp (/ 1 x)) 3.129 * [taylor]: Taking taylor expansion of (exp (- (/ 1 x))) in x 3.129 * [taylor]: Taking taylor expansion of (- (/ 1 x)) in x 3.129 * [taylor]: Taking taylor expansion of (/ 1 x) in x 3.129 * [taylor]: Taking taylor expansion of x in x 3.129 * [backup-simplify]: Simplify 0 into 0 3.129 * [backup-simplify]: Simplify 1 into 1 3.130 * [backup-simplify]: Simplify (/ 1 1) into 1 3.130 * [backup-simplify]: Simplify (- 1) into -1 3.130 * [backup-simplify]: Simplify (exp (- (/ 1 x))) into (exp (- (/ 1 x))) 3.133 * [backup-simplify]: Simplify (* (sqrt 2) (sqrt 2)) into (pow (sqrt 2) 2) 3.133 * [backup-simplify]: Simplify (+ (exp (/ 1 x)) (exp (- (/ 1 x)))) into (+ (exp (/ 1 x)) (exp (- (/ 1 x)))) 3.134 * [backup-simplify]: Simplify (/ (pow (sqrt 2) 2) (+ (exp (/ 1 x)) (exp (- (/ 1 x))))) into (/ (pow (sqrt 2) 2) (+ (exp (/ 1 x)) (exp (- (/ 1 x))))) 3.134 * [taylor]: Taking taylor expansion of (/ (pow (sqrt 2) 2) (+ (exp (/ 1 x)) (exp (- (/ 1 x))))) in x 3.134 * [taylor]: Taking taylor expansion of (pow (sqrt 2) 2) in x 3.134 * [taylor]: Taking taylor expansion of (sqrt 2) in x 3.134 * [taylor]: Taking taylor expansion of 2 in x 3.134 * [backup-simplify]: Simplify 2 into 2 3.134 * [backup-simplify]: Simplify (sqrt 2) into (sqrt 2) 3.135 * [backup-simplify]: Simplify (/ 0 (* 2 (sqrt 2))) into 0 3.135 * [taylor]: Taking taylor expansion of (+ (exp (/ 1 x)) (exp (- (/ 1 x)))) in x 3.135 * [taylor]: Taking taylor expansion of (exp (/ 1 x)) in x 3.135 * [taylor]: Taking taylor expansion of (/ 1 x) in x 3.135 * [taylor]: Taking taylor expansion of x in x 3.135 * [backup-simplify]: Simplify 0 into 0 3.135 * [backup-simplify]: Simplify 1 into 1 3.135 * [backup-simplify]: Simplify (/ 1 1) into 1 3.135 * [backup-simplify]: Simplify (exp (/ 1 x)) into (exp (/ 1 x)) 3.135 * [taylor]: Taking taylor expansion of (exp (- (/ 1 x))) in x 3.135 * [taylor]: Taking taylor expansion of (- (/ 1 x)) in x 3.135 * [taylor]: Taking taylor expansion of (/ 1 x) in x 3.135 * [taylor]: Taking taylor expansion of x in x 3.135 * [backup-simplify]: Simplify 0 into 0 3.135 * [backup-simplify]: Simplify 1 into 1 3.135 * [backup-simplify]: Simplify (/ 1 1) into 1 3.135 * [backup-simplify]: Simplify (- 1) into -1 3.136 * [backup-simplify]: Simplify (exp (- (/ 1 x))) into (exp (- (/ 1 x))) 3.136 * [backup-simplify]: Simplify (* (sqrt 2) (sqrt 2)) into (pow (sqrt 2) 2) 3.136 * [backup-simplify]: Simplify (+ (exp (/ 1 x)) (exp (- (/ 1 x)))) into (+ (exp (/ 1 x)) (exp (- (/ 1 x)))) 3.137 * [backup-simplify]: Simplify (/ (pow (sqrt 2) 2) (+ (exp (/ 1 x)) (exp (- (/ 1 x))))) into (/ (pow (sqrt 2) 2) (+ (exp (/ 1 x)) (exp (- (/ 1 x))))) 3.138 * [backup-simplify]: Simplify (/ (pow (sqrt 2) 2) (+ (exp (/ 1 x)) (exp (- (/ 1 x))))) into (/ (pow (sqrt 2) 2) (+ (exp (/ 1 x)) (exp (- (/ 1 x))))) 3.138 * [backup-simplify]: Simplify (+ (* (sqrt 2) 0) (* 0 (sqrt 2))) into 0 3.139 * [backup-simplify]: Simplify (+ 0 0) into 0 3.139 * [backup-simplify]: Simplify (- (/ 0 (+ (exp (/ 1 x)) (exp (- (/ 1 x))))) (+ (* (/ (pow (sqrt 2) 2) (+ (exp (/ 1 x)) (exp (- (/ 1 x))))) (/ 0 (+ (exp (/ 1 x)) (exp (- (/ 1 x)))))))) into 0 3.139 * [backup-simplify]: Simplify 0 into 0 3.140 * [backup-simplify]: Simplify (/ (- 0 (pow 0 2) (+)) (* 2 (sqrt 2))) into 0 3.141 * [backup-simplify]: Simplify (+ (* (sqrt 2) 0) (+ (* 0 0) (* 0 (sqrt 2)))) into 0 3.141 * [backup-simplify]: Simplify (+ 0 0) into 0 3.142 * [backup-simplify]: Simplify (- (/ 0 (+ (exp (/ 1 x)) (exp (- (/ 1 x))))) (+ (* (/ (pow (sqrt 2) 2) (+ (exp (/ 1 x)) (exp (- (/ 1 x))))) (/ 0 (+ (exp (/ 1 x)) (exp (- (/ 1 x)))))) (* 0 (/ 0 (+ (exp (/ 1 x)) (exp (- (/ 1 x)))))))) into 0 3.142 * [backup-simplify]: Simplify 0 into 0 3.142 * [backup-simplify]: Simplify (/ (- 0 (+ (* 2 (* 0 0)))) (* 2 (sqrt 2))) into 0 3.143 * [backup-simplify]: Simplify (+ (* (sqrt 2) 0) (+ (* 0 0) (+ (* 0 0) (* 0 (sqrt 2))))) into 0 3.143 * [backup-simplify]: Simplify (+ 0 0) into 0 3.144 * [backup-simplify]: Simplify (- (/ 0 (+ (exp (/ 1 x)) (exp (- (/ 1 x))))) (+ (* (/ (pow (sqrt 2) 2) (+ (exp (/ 1 x)) (exp (- (/ 1 x))))) (/ 0 (+ (exp (/ 1 x)) (exp (- (/ 1 x)))))) (* 0 (/ 0 (+ (exp (/ 1 x)) (exp (- (/ 1 x)))))) (* 0 (/ 0 (+ (exp (/ 1 x)) (exp (- (/ 1 x)))))))) into 0 3.144 * [backup-simplify]: Simplify 0 into 0 3.145 * [backup-simplify]: Simplify (/ (- 0 (pow 0 2) (+ (* 2 (* 0 0)))) (* 2 (sqrt 2))) into 0 3.146 * [backup-simplify]: Simplify (+ (* (sqrt 2) 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (* 0 (sqrt 2)))))) into 0 3.147 * [backup-simplify]: Simplify (+ 0 0) into 0 3.149 * [backup-simplify]: Simplify (- (/ 0 (+ (exp (/ 1 x)) (exp (- (/ 1 x))))) (+ (* (/ (pow (sqrt 2) 2) (+ (exp (/ 1 x)) (exp (- (/ 1 x))))) (/ 0 (+ (exp (/ 1 x)) (exp (- (/ 1 x)))))) (* 0 (/ 0 (+ (exp (/ 1 x)) (exp (- (/ 1 x)))))) (* 0 (/ 0 (+ (exp (/ 1 x)) (exp (- (/ 1 x)))))) (* 0 (/ 0 (+ (exp (/ 1 x)) (exp (- (/ 1 x)))))))) into 0 3.149 * [backup-simplify]: Simplify 0 into 0 3.150 * [backup-simplify]: Simplify (/ (- 0 (+ (* 2 (* 0 0)) (* 2 (* 0 0)))) (* 2 (sqrt 2))) into 0 3.151 * [backup-simplify]: Simplify (+ (* (sqrt 2) 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (* 0 (sqrt 2))))))) into 0 3.152 * [backup-simplify]: Simplify (+ 0 0) into 0 3.153 * [backup-simplify]: Simplify (- (/ 0 (+ (exp (/ 1 x)) (exp (- (/ 1 x))))) (+ (* (/ (pow (sqrt 2) 2) (+ (exp (/ 1 x)) (exp (- (/ 1 x))))) (/ 0 (+ (exp (/ 1 x)) (exp (- (/ 1 x)))))) (* 0 (/ 0 (+ (exp (/ 1 x)) (exp (- (/ 1 x)))))) (* 0 (/ 0 (+ (exp (/ 1 x)) (exp (- (/ 1 x)))))) (* 0 (/ 0 (+ (exp (/ 1 x)) (exp (- (/ 1 x)))))) (* 0 (/ 0 (+ (exp (/ 1 x)) (exp (- (/ 1 x)))))))) into 0 3.154 * [backup-simplify]: Simplify 0 into 0 3.155 * [backup-simplify]: Simplify (/ (- 0 (pow 0 2) (+ (* 2 (* 0 0)) (* 2 (* 0 0)))) (* 2 (sqrt 2))) into 0 3.156 * [backup-simplify]: Simplify (+ (* (sqrt 2) 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (* 0 (sqrt 2)))))))) into 0 3.157 * [backup-simplify]: Simplify (+ 0 0) into 0 3.159 * [backup-simplify]: Simplify (- (/ 0 (+ (exp (/ 1 x)) (exp (- (/ 1 x))))) (+ (* (/ (pow (sqrt 2) 2) (+ (exp (/ 1 x)) (exp (- (/ 1 x))))) (/ 0 (+ (exp (/ 1 x)) (exp (- (/ 1 x)))))) (* 0 (/ 0 (+ (exp (/ 1 x)) (exp (- (/ 1 x)))))) (* 0 (/ 0 (+ (exp (/ 1 x)) (exp (- (/ 1 x)))))) (* 0 (/ 0 (+ (exp (/ 1 x)) (exp (- (/ 1 x)))))) (* 0 (/ 0 (+ (exp (/ 1 x)) (exp (- (/ 1 x)))))) (* 0 (/ 0 (+ (exp (/ 1 x)) (exp (- (/ 1 x)))))))) into 0 3.159 * [backup-simplify]: Simplify 0 into 0 3.160 * [backup-simplify]: Simplify (/ (pow (sqrt 2) 2) (+ (exp (/ 1 (/ 1 x))) (exp (- (/ 1 (/ 1 x)))))) into (/ (pow (sqrt 2) 2) (+ (exp x) (exp (- x)))) 3.161 * [backup-simplify]: Simplify (* (sqrt 2) (/ (sqrt 2) (+ (exp (/ 1 (- x))) (exp (- (/ 1 (- x))))))) into (/ (pow (sqrt 2) 2) (+ (exp (/ 1 x)) (exp (/ -1 x)))) 3.161 * [approximate]: Taking taylor expansion of (/ (pow (sqrt 2) 2) (+ (exp (/ 1 x)) (exp (/ -1 x)))) in (x) around 0 3.161 * [taylor]: Taking taylor expansion of (/ (pow (sqrt 2) 2) (+ (exp (/ 1 x)) (exp (/ -1 x)))) in x 3.161 * [taylor]: Taking taylor expansion of (pow (sqrt 2) 2) in x 3.161 * [taylor]: Taking taylor expansion of (sqrt 2) in x 3.161 * [taylor]: Taking taylor expansion of 2 in x 3.161 * [backup-simplify]: Simplify 2 into 2 3.162 * [backup-simplify]: Simplify (sqrt 2) into (sqrt 2) 3.162 * [backup-simplify]: Simplify (/ 0 (* 2 (sqrt 2))) into 0 3.162 * [taylor]: Taking taylor expansion of (+ (exp (/ 1 x)) (exp (/ -1 x))) in x 3.163 * [taylor]: Taking taylor expansion of (exp (/ 1 x)) in x 3.163 * [taylor]: Taking taylor expansion of (/ 1 x) in x 3.163 * [taylor]: Taking taylor expansion of x in x 3.163 * [backup-simplify]: Simplify 0 into 0 3.163 * [backup-simplify]: Simplify 1 into 1 3.163 * [backup-simplify]: Simplify (/ 1 1) into 1 3.163 * [backup-simplify]: Simplify (exp (/ 1 x)) into (exp (/ 1 x)) 3.163 * [taylor]: Taking taylor expansion of (exp (/ -1 x)) in x 3.163 * [taylor]: Taking taylor expansion of (/ -1 x) in x 3.163 * [taylor]: Taking taylor expansion of -1 in x 3.163 * [backup-simplify]: Simplify -1 into -1 3.163 * [taylor]: Taking taylor expansion of x in x 3.163 * [backup-simplify]: Simplify 0 into 0 3.163 * [backup-simplify]: Simplify 1 into 1 3.164 * [backup-simplify]: Simplify (/ -1 1) into -1 3.164 * [backup-simplify]: Simplify (exp (/ -1 x)) into (exp (/ -1 x)) 3.165 * [backup-simplify]: Simplify (* (sqrt 2) (sqrt 2)) into (pow (sqrt 2) 2) 3.165 * [backup-simplify]: Simplify (+ (exp (/ 1 x)) (exp (/ -1 x))) into (+ (exp (/ 1 x)) (exp (/ -1 x))) 3.166 * [backup-simplify]: Simplify (/ (pow (sqrt 2) 2) (+ (exp (/ 1 x)) (exp (/ -1 x)))) into (/ (pow (sqrt 2) 2) (+ (exp (/ 1 x)) (exp (/ -1 x)))) 3.166 * [taylor]: Taking taylor expansion of (/ (pow (sqrt 2) 2) (+ (exp (/ 1 x)) (exp (/ -1 x)))) in x 3.166 * [taylor]: Taking taylor expansion of (pow (sqrt 2) 2) in x 3.166 * [taylor]: Taking taylor expansion of (sqrt 2) in x 3.166 * [taylor]: Taking taylor expansion of 2 in x 3.167 * [backup-simplify]: Simplify 2 into 2 3.167 * [backup-simplify]: Simplify (sqrt 2) into (sqrt 2) 3.168 * [backup-simplify]: Simplify (/ 0 (* 2 (sqrt 2))) into 0 3.168 * [taylor]: Taking taylor expansion of (+ (exp (/ 1 x)) (exp (/ -1 x))) in x 3.168 * [taylor]: Taking taylor expansion of (exp (/ 1 x)) in x 3.168 * [taylor]: Taking taylor expansion of (/ 1 x) in x 3.168 * [taylor]: Taking taylor expansion of x in x 3.168 * [backup-simplify]: Simplify 0 into 0 3.168 * [backup-simplify]: Simplify 1 into 1 3.168 * [backup-simplify]: Simplify (/ 1 1) into 1 3.168 * [backup-simplify]: Simplify (exp (/ 1 x)) into (exp (/ 1 x)) 3.168 * [taylor]: Taking taylor expansion of (exp (/ -1 x)) in x 3.168 * [taylor]: Taking taylor expansion of (/ -1 x) in x 3.168 * [taylor]: Taking taylor expansion of -1 in x 3.168 * [backup-simplify]: Simplify -1 into -1 3.168 * [taylor]: Taking taylor expansion of x in x 3.168 * [backup-simplify]: Simplify 0 into 0 3.168 * [backup-simplify]: Simplify 1 into 1 3.169 * [backup-simplify]: Simplify (/ -1 1) into -1 3.169 * [backup-simplify]: Simplify (exp (/ -1 x)) into (exp (/ -1 x)) 3.170 * [backup-simplify]: Simplify (* (sqrt 2) (sqrt 2)) into (pow (sqrt 2) 2) 3.170 * [backup-simplify]: Simplify (+ (exp (/ 1 x)) (exp (/ -1 x))) into (+ (exp (/ 1 x)) (exp (/ -1 x))) 3.171 * [backup-simplify]: Simplify (/ (pow (sqrt 2) 2) (+ (exp (/ 1 x)) (exp (/ -1 x)))) into (/ (pow (sqrt 2) 2) (+ (exp (/ 1 x)) (exp (/ -1 x)))) 3.172 * [backup-simplify]: Simplify (/ (pow (sqrt 2) 2) (+ (exp (/ 1 x)) (exp (/ -1 x)))) into (/ (pow (sqrt 2) 2) (+ (exp (/ 1 x)) (exp (/ -1 x)))) 3.173 * [backup-simplify]: Simplify (+ (* (sqrt 2) 0) (* 0 (sqrt 2))) into 0 3.173 * [backup-simplify]: Simplify (+ 0 0) into 0 3.175 * [backup-simplify]: Simplify (- (/ 0 (+ (exp (/ 1 x)) (exp (/ -1 x)))) (+ (* (/ (pow (sqrt 2) 2) (+ (exp (/ 1 x)) (exp (/ -1 x)))) (/ 0 (+ (exp (/ 1 x)) (exp (/ -1 x))))))) into 0 3.175 * [backup-simplify]: Simplify 0 into 0 3.176 * [backup-simplify]: Simplify (/ (- 0 (pow 0 2) (+)) (* 2 (sqrt 2))) into 0 3.177 * [backup-simplify]: Simplify (+ (* (sqrt 2) 0) (+ (* 0 0) (* 0 (sqrt 2)))) into 0 3.177 * [backup-simplify]: Simplify (+ 0 0) into 0 3.178 * [backup-simplify]: Simplify (- (/ 0 (+ (exp (/ 1 x)) (exp (/ -1 x)))) (+ (* (/ (pow (sqrt 2) 2) (+ (exp (/ 1 x)) (exp (/ -1 x)))) (/ 0 (+ (exp (/ 1 x)) (exp (/ -1 x))))) (* 0 (/ 0 (+ (exp (/ 1 x)) (exp (/ -1 x))))))) into 0 3.178 * [backup-simplify]: Simplify 0 into 0 3.179 * [backup-simplify]: Simplify (/ (- 0 (+ (* 2 (* 0 0)))) (* 2 (sqrt 2))) into 0 3.181 * [backup-simplify]: Simplify (+ (* (sqrt 2) 0) (+ (* 0 0) (+ (* 0 0) (* 0 (sqrt 2))))) into 0 3.181 * [backup-simplify]: Simplify (+ 0 0) into 0 3.182 * [backup-simplify]: Simplify (- (/ 0 (+ (exp (/ 1 x)) (exp (/ -1 x)))) (+ (* (/ (pow (sqrt 2) 2) (+ (exp (/ 1 x)) (exp (/ -1 x)))) (/ 0 (+ (exp (/ 1 x)) (exp (/ -1 x))))) (* 0 (/ 0 (+ (exp (/ 1 x)) (exp (/ -1 x))))) (* 0 (/ 0 (+ (exp (/ 1 x)) (exp (/ -1 x))))))) into 0 3.182 * [backup-simplify]: Simplify 0 into 0 3.184 * [backup-simplify]: Simplify (/ (- 0 (pow 0 2) (+ (* 2 (* 0 0)))) (* 2 (sqrt 2))) into 0 3.185 * [backup-simplify]: Simplify (+ (* (sqrt 2) 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (* 0 (sqrt 2)))))) into 0 3.185 * [backup-simplify]: Simplify (+ 0 0) into 0 3.187 * [backup-simplify]: Simplify (- (/ 0 (+ (exp (/ 1 x)) (exp (/ -1 x)))) (+ (* (/ (pow (sqrt 2) 2) (+ (exp (/ 1 x)) (exp (/ -1 x)))) (/ 0 (+ (exp (/ 1 x)) (exp (/ -1 x))))) (* 0 (/ 0 (+ (exp (/ 1 x)) (exp (/ -1 x))))) (* 0 (/ 0 (+ (exp (/ 1 x)) (exp (/ -1 x))))) (* 0 (/ 0 (+ (exp (/ 1 x)) (exp (/ -1 x))))))) into 0 3.187 * [backup-simplify]: Simplify 0 into 0 3.189 * [backup-simplify]: Simplify (/ (- 0 (+ (* 2 (* 0 0)) (* 2 (* 0 0)))) (* 2 (sqrt 2))) into 0 3.190 * [backup-simplify]: Simplify (+ (* (sqrt 2) 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (* 0 (sqrt 2))))))) into 0 3.191 * [backup-simplify]: Simplify (+ 0 0) into 0 3.192 * [backup-simplify]: Simplify (- (/ 0 (+ (exp (/ 1 x)) (exp (/ -1 x)))) (+ (* (/ (pow (sqrt 2) 2) (+ (exp (/ 1 x)) (exp (/ -1 x)))) (/ 0 (+ (exp (/ 1 x)) (exp (/ -1 x))))) (* 0 (/ 0 (+ (exp (/ 1 x)) (exp (/ -1 x))))) (* 0 (/ 0 (+ (exp (/ 1 x)) (exp (/ -1 x))))) (* 0 (/ 0 (+ (exp (/ 1 x)) (exp (/ -1 x))))) (* 0 (/ 0 (+ (exp (/ 1 x)) (exp (/ -1 x))))))) into 0 3.192 * [backup-simplify]: Simplify 0 into 0 3.194 * [backup-simplify]: Simplify (/ (- 0 (pow 0 2) (+ (* 2 (* 0 0)) (* 2 (* 0 0)))) (* 2 (sqrt 2))) into 0 3.196 * [backup-simplify]: Simplify (+ (* (sqrt 2) 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (* 0 (sqrt 2)))))))) into 0 3.196 * [backup-simplify]: Simplify (+ 0 0) into 0 3.198 * [backup-simplify]: Simplify (- (/ 0 (+ (exp (/ 1 x)) (exp (/ -1 x)))) (+ (* (/ (pow (sqrt 2) 2) (+ (exp (/ 1 x)) (exp (/ -1 x)))) (/ 0 (+ (exp (/ 1 x)) (exp (/ -1 x))))) (* 0 (/ 0 (+ (exp (/ 1 x)) (exp (/ -1 x))))) (* 0 (/ 0 (+ (exp (/ 1 x)) (exp (/ -1 x))))) (* 0 (/ 0 (+ (exp (/ 1 x)) (exp (/ -1 x))))) (* 0 (/ 0 (+ (exp (/ 1 x)) (exp (/ -1 x))))) (* 0 (/ 0 (+ (exp (/ 1 x)) (exp (/ -1 x))))))) into 0 3.198 * [backup-simplify]: Simplify 0 into 0 3.199 * [backup-simplify]: Simplify (/ (pow (sqrt 2) 2) (+ (exp (/ 1 (/ 1 (- x)))) (exp (/ -1 (/ 1 (- x)))))) into (/ (pow (sqrt 2) 2) (+ (exp (* -1 x)) (exp x))) 3.199 * * * [progress]: simplifying candidates 3.199 * * * * [progress]: [ 1 / 60 ] simplifiying candidate # 3.199 * [simplify]: Simplifying (* (sqrt 2) (/ (sqrt 2) (+ (exp x) (exp (- x))))) 3.200 * * [simplify]: iters left: 6 (9 enodes) 3.204 * * [simplify]: iters left: 5 (33 enodes) 3.215 * * [simplify]: iters left: 4 (37 enodes) 3.225 * * [simplify]: iters left: 3 (39 enodes) 3.236 * * [simplify]: Extracting #0: cost 1 inf + 0 3.236 * * [simplify]: Extracting #1: cost 6 inf + 0 3.236 * * [simplify]: Extracting #2: cost 10 inf + 1 3.236 * * [simplify]: Extracting #3: cost 13 inf + 83 3.236 * * [simplify]: Extracting #4: cost 9 inf + 308 3.237 * * [simplify]: Extracting #5: cost 1 inf + 1799 3.238 * * [simplify]: Extracting #6: cost 0 inf + 2101 3.238 * [simplify]: Simplified to (/ 2 (+ (exp x) (exp (- x)))) 3.238 * [simplify]: Simplified (2 1) to (λ (x) (pow (/ 2 (+ (exp x) (exp (- x)))) 1)) 3.238 * * * * [progress]: [ 2 / 60 ] simplifiying candidate # 3.238 * * * * [progress]: [ 3 / 60 ] simplifiying candidate # 3.239 * [simplify]: Simplifying (+ (log (sqrt 2)) (- (log (sqrt 2)) (log (+ (exp x) (exp (- x)))))) 3.239 * * [simplify]: iters left: 6 (11 enodes) 3.244 * * [simplify]: iters left: 5 (41 enodes) 3.251 * * [simplify]: iters left: 4 (54 enodes) 3.261 * * [simplify]: iters left: 3 (61 enodes) 3.270 * * [simplify]: iters left: 2 (67 enodes) 3.284 * * [simplify]: iters left: 1 (78 enodes) 3.306 * * [simplify]: Extracting #0: cost 1 inf + 0 3.306 * * [simplify]: Extracting #1: cost 9 inf + 0 3.306 * * [simplify]: Extracting #2: cost 18 inf + 0 3.306 * * [simplify]: Extracting #3: cost 23 inf + 0 3.306 * * [simplify]: Extracting #4: cost 27 inf + 1 3.306 * * [simplify]: Extracting #5: cost 23 inf + 156 3.307 * * [simplify]: Extracting #6: cost 9 inf + 2672 3.308 * * [simplify]: Extracting #7: cost 0 inf + 5775 3.309 * [simplify]: Simplified to (- (log (sqrt 2)) (- (log (+ (exp (- x)) (exp x))) (log (sqrt 2)))) 3.309 * [simplify]: Simplified (2 1) to (λ (x) (exp (- (log (sqrt 2)) (- (log (+ (exp (- x)) (exp x))) (log (sqrt 2)))))) 3.309 * * * * [progress]: [ 4 / 60 ] simplifiying candidate # 3.310 * [simplify]: Simplifying (+ (log (sqrt 2)) (log (/ (sqrt 2) (+ (exp x) (exp (- x)))))) 3.310 * * [simplify]: iters left: 6 (11 enodes) 3.315 * * [simplify]: iters left: 5 (39 enodes) 3.326 * * [simplify]: iters left: 4 (51 enodes) 3.341 * * [simplify]: iters left: 3 (66 enodes) 3.359 * * [simplify]: iters left: 2 (75 enodes) 3.380 * * [simplify]: iters left: 1 (76 enodes) 3.402 * * [simplify]: Extracting #0: cost 1 inf + 0 3.402 * * [simplify]: Extracting #1: cost 11 inf + 0 3.403 * * [simplify]: Extracting #2: cost 22 inf + 0 3.403 * * [simplify]: Extracting #3: cost 28 inf + 0 3.403 * * [simplify]: Extracting #4: cost 31 inf + 42 3.403 * * [simplify]: Extracting #5: cost 22 inf + 902 3.404 * * [simplify]: Extracting #6: cost 8 inf + 4100 3.406 * * [simplify]: Extracting #7: cost 0 inf + 7474 3.408 * [simplify]: Simplified to (- (log (sqrt 2)) (- (log (+ (exp (- x)) (exp x))) (log (sqrt 2)))) 3.408 * [simplify]: Simplified (2 1) to (λ (x) (exp (- (log (sqrt 2)) (- (log (+ (exp (- x)) (exp x))) (log (sqrt 2)))))) 3.408 * * * * [progress]: [ 5 / 60 ] simplifiying candidate # 3.409 * [simplify]: Simplifying (log (* (sqrt 2) (/ (sqrt 2) (+ (exp x) (exp (- x)))))) 3.409 * * [simplify]: iters left: 6 (10 enodes) 3.414 * * [simplify]: iters left: 5 (39 enodes) 3.427 * * [simplify]: iters left: 4 (52 enodes) 3.436 * * [simplify]: iters left: 3 (65 enodes) 3.446 * * [simplify]: iters left: 2 (77 enodes) 3.458 * * [simplify]: iters left: 1 (84 enodes) 3.477 * * [simplify]: Extracting #0: cost 1 inf + 0 3.478 * * [simplify]: Extracting #1: cost 14 inf + 0 3.478 * * [simplify]: Extracting #2: cost 29 inf + 0 3.478 * * [simplify]: Extracting #3: cost 30 inf + 184 3.478 * * [simplify]: Extracting #4: cost 29 inf + 940 3.479 * * [simplify]: Extracting #5: cost 21 inf + 1729 3.480 * * [simplify]: Extracting #6: cost 12 inf + 3893 3.482 * * [simplify]: Extracting #7: cost 3 inf + 7338 3.484 * * [simplify]: Extracting #8: cost 0 inf + 8473 3.486 * [simplify]: Simplified to (log (/ 2 (+ (exp x) (exp (- x))))) 3.486 * [simplify]: Simplified (2 1) to (λ (x) (exp (log (/ 2 (+ (exp x) (exp (- x))))))) 3.487 * * * * [progress]: [ 6 / 60 ] simplifiying candidate # 3.487 * [simplify]: Simplifying (exp (* (sqrt 2) (/ (sqrt 2) (+ (exp x) (exp (- x)))))) 3.487 * * [simplify]: iters left: 6 (10 enodes) 3.492 * * [simplify]: iters left: 5 (38 enodes) 3.501 * * [simplify]: iters left: 4 (49 enodes) 3.508 * * [simplify]: iters left: 3 (64 enodes) 3.520 * * [simplify]: iters left: 2 (107 enodes) 3.554 * * [simplify]: iters left: 1 (220 enodes) 3.639 * * [simplify]: Extracting #0: cost 1 inf + 0 3.640 * * [simplify]: Extracting #1: cost 20 inf + 0 3.640 * * [simplify]: Extracting #2: cost 79 inf + 1 3.640 * * [simplify]: Extracting #3: cost 122 inf + 45 3.641 * * [simplify]: Extracting #4: cost 123 inf + 1246 3.643 * * [simplify]: Extracting #5: cost 107 inf + 3489 3.648 * * [simplify]: Extracting #6: cost 49 inf + 20794 3.660 * * [simplify]: Extracting #7: cost 9 inf + 47413 3.670 * * [simplify]: Extracting #8: cost 0 inf + 53537 3.678 * * [simplify]: Extracting #9: cost 0 inf + 52269 3.686 * [simplify]: Simplified to (exp (/ 2 (+ (exp x) (exp (- x))))) 3.686 * [simplify]: Simplified (2 1) to (λ (x) (log (exp (/ 2 (+ (exp x) (exp (- x))))))) 3.686 * * * * [progress]: [ 7 / 60 ] simplifiying candidate # 3.686 * [simplify]: Simplifying (* (* (* (sqrt 2) (sqrt 2)) (sqrt 2)) (/ (* (* (sqrt 2) (sqrt 2)) (sqrt 2)) (* (* (+ (exp x) (exp (- x))) (+ (exp x) (exp (- x)))) (+ (exp x) (exp (- x)))))) 3.687 * * [simplify]: iters left: 6 (13 enodes) 3.692 * * [simplify]: iters left: 5 (66 enodes) 3.725 * * [simplify]: iters left: 4 (234 enodes) 3.825 * * [simplify]: Extracting #0: cost 1 inf + 0 3.825 * * [simplify]: Extracting #1: cost 65 inf + 0 3.826 * * [simplify]: Extracting #2: cost 186 inf + 44 3.828 * * [simplify]: Extracting #3: cost 232 inf + 331 3.830 * * [simplify]: Extracting #4: cost 226 inf + 1196 3.838 * * [simplify]: Extracting #5: cost 104 inf + 36041 3.853 * * [simplify]: Extracting #6: cost 7 inf + 69787 3.865 * * [simplify]: Extracting #7: cost 0 inf + 72242 3.877 * [simplify]: Simplified to (/ 8 (* (+ (exp x) (exp (- x))) (* (+ (exp x) (exp (- x))) (+ (exp x) (exp (- x)))))) 3.877 * [simplify]: Simplified (2 1) to (λ (x) (cbrt (/ 8 (* (+ (exp x) (exp (- x))) (* (+ (exp x) (exp (- x))) (+ (exp x) (exp (- x)))))))) 3.877 * * * * [progress]: [ 8 / 60 ] simplifiying candidate # 3.877 * [simplify]: Simplifying (* (* (* (sqrt 2) (sqrt 2)) (sqrt 2)) (* (* (/ (sqrt 2) (+ (exp x) (exp (- x)))) (/ (sqrt 2) (+ (exp x) (exp (- x))))) (/ (sqrt 2) (+ (exp x) (exp (- x)))))) 3.878 * * [simplify]: iters left: 6 (13 enodes) 3.881 * * [simplify]: iters left: 5 (53 enodes) 3.901 * * [simplify]: iters left: 4 (115 enodes) 3.936 * * [simplify]: iters left: 3 (253 enodes) 4.042 * * [simplify]: Extracting #0: cost 1 inf + 0 4.042 * * [simplify]: Extracting #1: cost 48 inf + 0 4.043 * * [simplify]: Extracting #2: cost 120 inf + 44 4.044 * * [simplify]: Extracting #3: cost 119 inf + 617 4.045 * * [simplify]: Extracting #4: cost 106 inf + 2805 4.050 * * [simplify]: Extracting #5: cost 24 inf + 32295 4.059 * * [simplify]: Extracting #6: cost 0 inf + 41422 4.067 * [simplify]: Simplified to (* (* (/ 2 (+ (exp x) (exp (- x)))) (/ 2 (+ (exp x) (exp (- x))))) (/ 2 (+ (exp x) (exp (- x))))) 4.067 * [simplify]: Simplified (2 1) to (λ (x) (cbrt (* (* (/ 2 (+ (exp x) (exp (- x)))) (/ 2 (+ (exp x) (exp (- x))))) (/ 2 (+ (exp x) (exp (- x))))))) 4.067 * * * * [progress]: [ 9 / 60 ] simplifiying candidate # 4.068 * [simplify]: Simplifying (* (cbrt (* (sqrt 2) (/ (sqrt 2) (+ (exp x) (exp (- x)))))) (cbrt (* (sqrt 2) (/ (sqrt 2) (+ (exp x) (exp (- x))))))) 4.068 * * [simplify]: iters left: 6 (11 enodes) 4.071 * * [simplify]: iters left: 5 (39 enodes) 4.081 * * [simplify]: iters left: 4 (43 enodes) 4.092 * * [simplify]: iters left: 3 (45 enodes) 4.099 * * [simplify]: Extracting #0: cost 1 inf + 0 4.099 * * [simplify]: Extracting #1: cost 3 inf + 0 4.099 * * [simplify]: Extracting #2: cost 5 inf + 0 4.099 * * [simplify]: Extracting #3: cost 10 inf + 0 4.099 * * [simplify]: Extracting #4: cost 14 inf + 1 4.099 * * [simplify]: Extracting #5: cost 17 inf + 83 4.099 * * [simplify]: Extracting #6: cost 13 inf + 308 4.100 * * [simplify]: Extracting #7: cost 4 inf + 2141 4.100 * * [simplify]: Extracting #8: cost 0 inf + 3549 4.101 * [simplify]: Simplified to (* (cbrt (/ 2 (+ (exp x) (exp (- x))))) (cbrt (/ 2 (+ (exp x) (exp (- x)))))) 4.101 * [simplify]: Simplified (2 1) to (λ (x) (* (* (cbrt (/ 2 (+ (exp x) (exp (- x))))) (cbrt (/ 2 (+ (exp x) (exp (- x)))))) (cbrt (* (sqrt 2) (/ (sqrt 2) (+ (exp x) (exp (- x)))))))) 4.101 * [simplify]: Simplifying (cbrt (* (sqrt 2) (/ (sqrt 2) (+ (exp x) (exp (- x)))))) 4.101 * * [simplify]: iters left: 6 (10 enodes) 4.104 * * [simplify]: iters left: 5 (36 enodes) 4.110 * * [simplify]: iters left: 4 (40 enodes) 4.116 * * [simplify]: iters left: 3 (42 enodes) 4.129 * * [simplify]: Extracting #0: cost 1 inf + 0 4.129 * * [simplify]: Extracting #1: cost 3 inf + 0 4.129 * * [simplify]: Extracting #2: cost 8 inf + 0 4.129 * * [simplify]: Extracting #3: cost 12 inf + 1 4.129 * * [simplify]: Extracting #4: cost 16 inf + 42 4.129 * * [simplify]: Extracting #5: cost 10 inf + 419 4.130 * * [simplify]: Extracting #6: cost 0 inf + 2785 4.131 * [simplify]: Simplified to (cbrt (/ 2 (+ (exp x) (exp (- x))))) 4.131 * [simplify]: Simplified (2 2) to (λ (x) (* (* (cbrt (* (sqrt 2) (/ (sqrt 2) (+ (exp x) (exp (- x)))))) (cbrt (* (sqrt 2) (/ (sqrt 2) (+ (exp x) (exp (- x))))))) (cbrt (/ 2 (+ (exp x) (exp (- x))))))) 4.131 * * * * [progress]: [ 10 / 60 ] simplifiying candidate # 4.131 * [simplify]: Simplifying (* (* (* (sqrt 2) (/ (sqrt 2) (+ (exp x) (exp (- x))))) (* (sqrt 2) (/ (sqrt 2) (+ (exp x) (exp (- x)))))) (* (sqrt 2) (/ (sqrt 2) (+ (exp x) (exp (- x)))))) 4.131 * * [simplify]: iters left: 6 (11 enodes) 4.137 * * [simplify]: iters left: 5 (48 enodes) 4.155 * * [simplify]: iters left: 4 (89 enodes) 4.195 * * [simplify]: iters left: 3 (192 enodes) 4.268 * * [simplify]: iters left: 2 (332 enodes) 4.479 * * [simplify]: Extracting #0: cost 1 inf + 0 4.479 * * [simplify]: Extracting #1: cost 80 inf + 0 4.481 * * [simplify]: Extracting #2: cost 186 inf + 45 4.483 * * [simplify]: Extracting #3: cost 191 inf + 787 4.485 * * [simplify]: Extracting #4: cost 179 inf + 2222 4.496 * * [simplify]: Extracting #5: cost 110 inf + 28381 4.518 * * [simplify]: Extracting #6: cost 8 inf + 68411 4.542 * * [simplify]: Extracting #7: cost 0 inf + 71910 4.566 * [simplify]: Simplified to (/ (/ 8 (* (+ (exp x) (exp (- x))) (+ (exp x) (exp (- x))))) (+ (exp x) (exp (- x)))) 4.566 * [simplify]: Simplified (2 1) to (λ (x) (cbrt (/ (/ 8 (* (+ (exp x) (exp (- x))) (+ (exp x) (exp (- x))))) (+ (exp x) (exp (- x)))))) 4.566 * * * * [progress]: [ 11 / 60 ] simplifiying candidate # 4.567 * [simplify]: Simplifying (sqrt (* (sqrt 2) (/ (sqrt 2) (+ (exp x) (exp (- x)))))) 4.567 * * [simplify]: iters left: 6 (10 enodes) 4.572 * * [simplify]: iters left: 5 (36 enodes) 4.581 * * [simplify]: iters left: 4 (40 enodes) 4.592 * * [simplify]: iters left: 3 (42 enodes) 4.602 * * [simplify]: Extracting #0: cost 1 inf + 0 4.603 * * [simplify]: Extracting #1: cost 3 inf + 0 4.603 * * [simplify]: Extracting #2: cost 8 inf + 0 4.603 * * [simplify]: Extracting #3: cost 12 inf + 1 4.603 * * [simplify]: Extracting #4: cost 16 inf + 42 4.603 * * [simplify]: Extracting #5: cost 10 inf + 419 4.603 * * [simplify]: Extracting #6: cost 0 inf + 2705 4.604 * [simplify]: Simplified to (sqrt (/ 2 (+ (exp x) (exp (- x))))) 4.604 * [simplify]: Simplified (2 1) to (λ (x) (* (sqrt (/ 2 (+ (exp x) (exp (- x))))) (sqrt (* (sqrt 2) (/ (sqrt 2) (+ (exp x) (exp (- x)))))))) 4.604 * [simplify]: Simplifying (sqrt (* (sqrt 2) (/ (sqrt 2) (+ (exp x) (exp (- x)))))) 4.604 * * [simplify]: iters left: 6 (10 enodes) 4.609 * * [simplify]: iters left: 5 (36 enodes) 4.619 * * [simplify]: iters left: 4 (40 enodes) 4.629 * * [simplify]: iters left: 3 (42 enodes) 4.642 * * [simplify]: Extracting #0: cost 1 inf + 0 4.642 * * [simplify]: Extracting #1: cost 3 inf + 0 4.642 * * [simplify]: Extracting #2: cost 8 inf + 0 4.642 * * [simplify]: Extracting #3: cost 12 inf + 1 4.642 * * [simplify]: Extracting #4: cost 16 inf + 42 4.642 * * [simplify]: Extracting #5: cost 10 inf + 419 4.643 * * [simplify]: Extracting #6: cost 0 inf + 2705 4.643 * [simplify]: Simplified to (sqrt (/ 2 (+ (exp x) (exp (- x))))) 4.643 * [simplify]: Simplified (2 2) to (λ (x) (* (sqrt (* (sqrt 2) (/ (sqrt 2) (+ (exp x) (exp (- x)))))) (sqrt (/ 2 (+ (exp x) (exp (- x))))))) 4.643 * * * * [progress]: [ 12 / 60 ] simplifiying candidate # 4.643 * * * * [progress]: [ 13 / 60 ] simplifiying candidate # 4.644 * [simplify]: Simplifying (* (sqrt (sqrt 2)) (sqrt (/ (sqrt 2) (+ (exp x) (exp (- x)))))) 4.644 * * [simplify]: iters left: 6 (11 enodes) 4.649 * * [simplify]: iters left: 5 (37 enodes) 4.658 * * [simplify]: iters left: 4 (41 enodes) 4.669 * * [simplify]: iters left: 3 (43 enodes) 4.675 * * [simplify]: Extracting #0: cost 1 inf + 0 4.675 * * [simplify]: Extracting #1: cost 4 inf + 0 4.676 * * [simplify]: Extracting #2: cost 8 inf + 0 4.676 * * [simplify]: Extracting #3: cost 12 inf + 0 4.676 * * [simplify]: Extracting #4: cost 14 inf + 1 4.676 * * [simplify]: Extracting #5: cost 17 inf + 83 4.676 * * [simplify]: Extracting #6: cost 13 inf + 288 4.676 * * [simplify]: Extracting #7: cost 8 inf + 843 4.676 * * [simplify]: Extracting #8: cost 3 inf + 2081 4.677 * * [simplify]: Extracting #9: cost 0 inf + 3267 4.677 * [simplify]: Simplified to (* (sqrt (sqrt 2)) (sqrt (/ (sqrt 2) (+ (exp (- x)) (exp x))))) 4.677 * [simplify]: Simplified (2 1) to (λ (x) (* (* (sqrt (sqrt 2)) (sqrt (/ (sqrt 2) (+ (exp (- x)) (exp x))))) (* (sqrt (sqrt 2)) (sqrt (/ (sqrt 2) (+ (exp x) (exp (- x)))))))) 4.677 * [simplify]: Simplifying (* (sqrt (sqrt 2)) (sqrt (/ (sqrt 2) (+ (exp x) (exp (- x)))))) 4.677 * * [simplify]: iters left: 6 (11 enodes) 4.680 * * [simplify]: iters left: 5 (37 enodes) 4.690 * * [simplify]: iters left: 4 (41 enodes) 4.702 * * [simplify]: iters left: 3 (43 enodes) 4.714 * * [simplify]: Extracting #0: cost 1 inf + 0 4.715 * * [simplify]: Extracting #1: cost 4 inf + 0 4.715 * * [simplify]: Extracting #2: cost 8 inf + 0 4.715 * * [simplify]: Extracting #3: cost 12 inf + 0 4.715 * * [simplify]: Extracting #4: cost 14 inf + 1 4.715 * * [simplify]: Extracting #5: cost 17 inf + 83 4.715 * * [simplify]: Extracting #6: cost 13 inf + 288 4.715 * * [simplify]: Extracting #7: cost 8 inf + 843 4.716 * * [simplify]: Extracting #8: cost 3 inf + 2081 4.717 * * [simplify]: Extracting #9: cost 0 inf + 3267 4.718 * [simplify]: Simplified to (* (sqrt (sqrt 2)) (sqrt (/ (sqrt 2) (+ (exp (- x)) (exp x))))) 4.718 * [simplify]: Simplified (2 2) to (λ (x) (* (* (sqrt (sqrt 2)) (sqrt (/ (sqrt 2) (+ (exp x) (exp (- x)))))) (* (sqrt (sqrt 2)) (sqrt (/ (sqrt 2) (+ (exp (- x)) (exp x))))))) 4.718 * * * * [progress]: [ 14 / 60 ] simplifiying candidate # 4.718 * [simplify]: Simplifying (* (sqrt (sqrt 2)) (/ (sqrt (sqrt 2)) (sqrt (+ (exp x) (exp (- x)))))) 4.719 * * [simplify]: iters left: 6 (11 enodes) 4.724 * * [simplify]: iters left: 5 (39 enodes) 4.736 * * [simplify]: iters left: 4 (45 enodes) 4.749 * * [simplify]: iters left: 3 (50 enodes) 4.756 * * [simplify]: Extracting #0: cost 1 inf + 0 4.756 * * [simplify]: Extracting #1: cost 7 inf + 0 4.756 * * [simplify]: Extracting #2: cost 14 inf + 0 4.756 * * [simplify]: Extracting #3: cost 16 inf + 1 4.756 * * [simplify]: Extracting #4: cost 19 inf + 83 4.756 * * [simplify]: Extracting #5: cost 16 inf + 207 4.756 * * [simplify]: Extracting #6: cost 8 inf + 1135 4.757 * * [simplify]: Extracting #7: cost 1 inf + 3487 4.757 * * [simplify]: Extracting #8: cost 0 inf + 3869 4.758 * [simplify]: Simplified to (/ (sqrt 2) (sqrt (+ (exp (- x)) (exp x)))) 4.758 * [simplify]: Simplified (2 1) to (λ (x) (* (/ (sqrt 2) (sqrt (+ (exp (- x)) (exp x)))) (* (sqrt (sqrt 2)) (/ (sqrt (sqrt 2)) (sqrt (+ (exp x) (exp (- x)))))))) 4.758 * [simplify]: Simplifying (* (sqrt (sqrt 2)) (/ (sqrt (sqrt 2)) (sqrt (+ (exp x) (exp (- x)))))) 4.758 * * [simplify]: iters left: 6 (11 enodes) 4.761 * * [simplify]: iters left: 5 (39 enodes) 4.769 * * [simplify]: iters left: 4 (45 enodes) 4.776 * * [simplify]: iters left: 3 (50 enodes) 4.788 * * [simplify]: Extracting #0: cost 1 inf + 0 4.788 * * [simplify]: Extracting #1: cost 7 inf + 0 4.788 * * [simplify]: Extracting #2: cost 14 inf + 0 4.788 * * [simplify]: Extracting #3: cost 16 inf + 1 4.788 * * [simplify]: Extracting #4: cost 19 inf + 83 4.788 * * [simplify]: Extracting #5: cost 16 inf + 207 4.788 * * [simplify]: Extracting #6: cost 8 inf + 1135 4.789 * * [simplify]: Extracting #7: cost 1 inf + 3487 4.790 * * [simplify]: Extracting #8: cost 0 inf + 3869 4.791 * [simplify]: Simplified to (/ (sqrt 2) (sqrt (+ (exp (- x)) (exp x)))) 4.791 * [simplify]: Simplified (2 2) to (λ (x) (* (* (sqrt (sqrt 2)) (/ (sqrt (sqrt 2)) (sqrt (+ (exp x) (exp (- x)))))) (/ (sqrt 2) (sqrt (+ (exp (- x)) (exp x)))))) 4.791 * * * * [progress]: [ 15 / 60 ] simplifiying candidate # 4.791 * [simplify]: Simplifying (* (sqrt (sqrt 2)) (/ (sqrt (sqrt 2)) (sqrt (+ (exp x) (exp (- x)))))) 4.792 * * [simplify]: iters left: 6 (11 enodes) 4.797 * * [simplify]: iters left: 5 (39 enodes) 4.809 * * [simplify]: iters left: 4 (45 enodes) 4.818 * * [simplify]: iters left: 3 (50 enodes) 4.826 * * [simplify]: Extracting #0: cost 1 inf + 0 4.826 * * [simplify]: Extracting #1: cost 7 inf + 0 4.826 * * [simplify]: Extracting #2: cost 14 inf + 0 4.826 * * [simplify]: Extracting #3: cost 16 inf + 1 4.826 * * [simplify]: Extracting #4: cost 19 inf + 83 4.826 * * [simplify]: Extracting #5: cost 16 inf + 207 4.826 * * [simplify]: Extracting #6: cost 8 inf + 1135 4.826 * * [simplify]: Extracting #7: cost 1 inf + 3487 4.827 * * [simplify]: Extracting #8: cost 0 inf + 3869 4.827 * [simplify]: Simplified to (/ (sqrt 2) (sqrt (+ (exp (- x)) (exp x)))) 4.827 * [simplify]: Simplified (2 1) to (λ (x) (* (/ (sqrt 2) (sqrt (+ (exp (- x)) (exp x)))) (* (sqrt (sqrt 2)) (/ (sqrt (sqrt 2)) (sqrt (+ (exp x) (exp (- x)))))))) 4.828 * [simplify]: Simplifying (* (sqrt (sqrt 2)) (/ (sqrt (sqrt 2)) (sqrt (+ (exp x) (exp (- x)))))) 4.828 * * [simplify]: iters left: 6 (11 enodes) 4.831 * * [simplify]: iters left: 5 (39 enodes) 4.837 * * [simplify]: iters left: 4 (45 enodes) 4.845 * * [simplify]: iters left: 3 (50 enodes) 4.858 * * [simplify]: Extracting #0: cost 1 inf + 0 4.859 * * [simplify]: Extracting #1: cost 7 inf + 0 4.859 * * [simplify]: Extracting #2: cost 14 inf + 0 4.859 * * [simplify]: Extracting #3: cost 16 inf + 1 4.859 * * [simplify]: Extracting #4: cost 19 inf + 83 4.859 * * [simplify]: Extracting #5: cost 16 inf + 207 4.859 * * [simplify]: Extracting #6: cost 8 inf + 1135 4.860 * * [simplify]: Extracting #7: cost 1 inf + 3487 4.861 * * [simplify]: Extracting #8: cost 0 inf + 3869 4.862 * [simplify]: Simplified to (/ (sqrt 2) (sqrt (+ (exp (- x)) (exp x)))) 4.862 * [simplify]: Simplified (2 2) to (λ (x) (* (* (sqrt (sqrt 2)) (/ (sqrt (sqrt 2)) (sqrt (+ (exp x) (exp (- x)))))) (/ (sqrt 2) (sqrt (+ (exp (- x)) (exp x)))))) 4.862 * * * * [progress]: [ 16 / 60 ] simplifiying candidate # 4.863 * [simplify]: Simplifying (* (sqrt (sqrt 2)) (sqrt (/ (sqrt 2) (+ (exp x) (exp (- x)))))) 4.863 * * [simplify]: iters left: 6 (11 enodes) 4.871 * * [simplify]: iters left: 5 (37 enodes) 4.887 * * [simplify]: iters left: 4 (41 enodes) 4.899 * * [simplify]: iters left: 3 (43 enodes) 4.911 * * [simplify]: Extracting #0: cost 1 inf + 0 4.912 * * [simplify]: Extracting #1: cost 4 inf + 0 4.912 * * [simplify]: Extracting #2: cost 8 inf + 0 4.912 * * [simplify]: Extracting #3: cost 12 inf + 0 4.912 * * [simplify]: Extracting #4: cost 14 inf + 1 4.912 * * [simplify]: Extracting #5: cost 17 inf + 83 4.912 * * [simplify]: Extracting #6: cost 13 inf + 288 4.912 * * [simplify]: Extracting #7: cost 8 inf + 843 4.913 * * [simplify]: Extracting #8: cost 3 inf + 2081 4.913 * * [simplify]: Extracting #9: cost 0 inf + 3267 4.914 * [simplify]: Simplified to (* (sqrt (sqrt 2)) (sqrt (/ (sqrt 2) (+ (exp (- x)) (exp x))))) 4.914 * [simplify]: Simplified (2 1) to (λ (x) (* (* (sqrt (sqrt 2)) (sqrt (/ (sqrt 2) (+ (exp (- x)) (exp x))))) (* (sqrt (sqrt 2)) (sqrt (/ (sqrt 2) (+ (exp x) (exp (- x)))))))) 4.914 * [simplify]: Simplifying (* (sqrt (sqrt 2)) (sqrt (/ (sqrt 2) (+ (exp x) (exp (- x)))))) 4.914 * * [simplify]: iters left: 6 (11 enodes) 4.920 * * [simplify]: iters left: 5 (37 enodes) 4.931 * * [simplify]: iters left: 4 (41 enodes) 4.941 * * [simplify]: iters left: 3 (43 enodes) 4.947 * * [simplify]: Extracting #0: cost 1 inf + 0 4.947 * * [simplify]: Extracting #1: cost 4 inf + 0 4.947 * * [simplify]: Extracting #2: cost 8 inf + 0 4.947 * * [simplify]: Extracting #3: cost 12 inf + 0 4.947 * * [simplify]: Extracting #4: cost 14 inf + 1 4.947 * * [simplify]: Extracting #5: cost 17 inf + 83 4.947 * * [simplify]: Extracting #6: cost 13 inf + 288 4.947 * * [simplify]: Extracting #7: cost 8 inf + 843 4.948 * * [simplify]: Extracting #8: cost 3 inf + 2081 4.948 * * [simplify]: Extracting #9: cost 0 inf + 3267 4.948 * [simplify]: Simplified to (* (sqrt (sqrt 2)) (sqrt (/ (sqrt 2) (+ (exp (- x)) (exp x))))) 4.948 * [simplify]: Simplified (2 2) to (λ (x) (* (* (sqrt (sqrt 2)) (sqrt (/ (sqrt 2) (+ (exp x) (exp (- x)))))) (* (sqrt (sqrt 2)) (sqrt (/ (sqrt 2) (+ (exp (- x)) (exp x))))))) 4.948 * * * * [progress]: [ 17 / 60 ] simplifiying candidate # 4.949 * [simplify]: Simplifying (* (sqrt (sqrt 2)) (/ (sqrt (sqrt 2)) (sqrt (+ (exp x) (exp (- x)))))) 4.949 * * [simplify]: iters left: 6 (11 enodes) 4.952 * * [simplify]: iters left: 5 (39 enodes) 4.958 * * [simplify]: iters left: 4 (45 enodes) 4.964 * * [simplify]: iters left: 3 (50 enodes) 4.971 * * [simplify]: Extracting #0: cost 1 inf + 0 4.972 * * [simplify]: Extracting #1: cost 7 inf + 0 4.972 * * [simplify]: Extracting #2: cost 14 inf + 0 4.972 * * [simplify]: Extracting #3: cost 16 inf + 1 4.972 * * [simplify]: Extracting #4: cost 19 inf + 83 4.972 * * [simplify]: Extracting #5: cost 16 inf + 207 4.972 * * [simplify]: Extracting #6: cost 8 inf + 1135 4.972 * * [simplify]: Extracting #7: cost 1 inf + 3487 4.973 * * [simplify]: Extracting #8: cost 0 inf + 3869 4.973 * [simplify]: Simplified to (/ (sqrt 2) (sqrt (+ (exp (- x)) (exp x)))) 4.973 * [simplify]: Simplified (2 1) to (λ (x) (* (/ (sqrt 2) (sqrt (+ (exp (- x)) (exp x)))) (* (sqrt (sqrt 2)) (/ (sqrt (sqrt 2)) (sqrt (+ (exp x) (exp (- x)))))))) 4.974 * [simplify]: Simplifying (* (sqrt (sqrt 2)) (/ (sqrt (sqrt 2)) (sqrt (+ (exp x) (exp (- x)))))) 4.974 * * [simplify]: iters left: 6 (11 enodes) 4.976 * * [simplify]: iters left: 5 (39 enodes) 4.983 * * [simplify]: iters left: 4 (45 enodes) 4.991 * * [simplify]: iters left: 3 (50 enodes) 4.998 * * [simplify]: Extracting #0: cost 1 inf + 0 4.998 * * [simplify]: Extracting #1: cost 7 inf + 0 4.998 * * [simplify]: Extracting #2: cost 14 inf + 0 4.998 * * [simplify]: Extracting #3: cost 16 inf + 1 4.998 * * [simplify]: Extracting #4: cost 19 inf + 83 4.998 * * [simplify]: Extracting #5: cost 16 inf + 207 4.998 * * [simplify]: Extracting #6: cost 8 inf + 1135 4.999 * * [simplify]: Extracting #7: cost 1 inf + 3487 4.999 * * [simplify]: Extracting #8: cost 0 inf + 3869 4.999 * [simplify]: Simplified to (/ (sqrt 2) (sqrt (+ (exp (- x)) (exp x)))) 4.999 * [simplify]: Simplified (2 2) to (λ (x) (* (* (sqrt (sqrt 2)) (/ (sqrt (sqrt 2)) (sqrt (+ (exp x) (exp (- x)))))) (/ (sqrt 2) (sqrt (+ (exp (- x)) (exp x)))))) 5.000 * * * * [progress]: [ 18 / 60 ] simplifiying candidate # 5.000 * [simplify]: Simplifying (* (sqrt (sqrt 2)) (/ (sqrt (sqrt 2)) (sqrt (+ (exp x) (exp (- x)))))) 5.000 * * [simplify]: iters left: 6 (11 enodes) 5.003 * * [simplify]: iters left: 5 (39 enodes) 5.009 * * [simplify]: iters left: 4 (45 enodes) 5.015 * * [simplify]: iters left: 3 (50 enodes) 5.022 * * [simplify]: Extracting #0: cost 1 inf + 0 5.022 * * [simplify]: Extracting #1: cost 7 inf + 0 5.022 * * [simplify]: Extracting #2: cost 14 inf + 0 5.022 * * [simplify]: Extracting #3: cost 16 inf + 1 5.023 * * [simplify]: Extracting #4: cost 19 inf + 83 5.023 * * [simplify]: Extracting #5: cost 16 inf + 207 5.023 * * [simplify]: Extracting #6: cost 8 inf + 1135 5.023 * * [simplify]: Extracting #7: cost 1 inf + 3487 5.024 * * [simplify]: Extracting #8: cost 0 inf + 3869 5.024 * [simplify]: Simplified to (/ (sqrt 2) (sqrt (+ (exp (- x)) (exp x)))) 5.024 * [simplify]: Simplified (2 1) to (λ (x) (* (/ (sqrt 2) (sqrt (+ (exp (- x)) (exp x)))) (* (sqrt (sqrt 2)) (/ (sqrt (sqrt 2)) (sqrt (+ (exp x) (exp (- x)))))))) 5.024 * [simplify]: Simplifying (* (sqrt (sqrt 2)) (/ (sqrt (sqrt 2)) (sqrt (+ (exp x) (exp (- x)))))) 5.024 * * [simplify]: iters left: 6 (11 enodes) 5.027 * * [simplify]: iters left: 5 (39 enodes) 5.034 * * [simplify]: iters left: 4 (45 enodes) 5.047 * * [simplify]: iters left: 3 (50 enodes) 5.060 * * [simplify]: Extracting #0: cost 1 inf + 0 5.060 * * [simplify]: Extracting #1: cost 7 inf + 0 5.060 * * [simplify]: Extracting #2: cost 14 inf + 0 5.060 * * [simplify]: Extracting #3: cost 16 inf + 1 5.060 * * [simplify]: Extracting #4: cost 19 inf + 83 5.061 * * [simplify]: Extracting #5: cost 16 inf + 207 5.061 * * [simplify]: Extracting #6: cost 8 inf + 1135 5.062 * * [simplify]: Extracting #7: cost 1 inf + 3487 5.063 * * [simplify]: Extracting #8: cost 0 inf + 3869 5.063 * [simplify]: Simplified to (/ (sqrt 2) (sqrt (+ (exp (- x)) (exp x)))) 5.063 * [simplify]: Simplified (2 2) to (λ (x) (* (* (sqrt (sqrt 2)) (/ (sqrt (sqrt 2)) (sqrt (+ (exp x) (exp (- x)))))) (/ (sqrt 2) (sqrt (+ (exp (- x)) (exp x)))))) 5.064 * * * * [progress]: [ 19 / 60 ] simplifiying candidate # 5.064 * [simplify]: Simplifying (* (sqrt 2) (* (cbrt (/ (sqrt 2) (+ (exp x) (exp (- x))))) (cbrt (/ (sqrt 2) (+ (exp x) (exp (- x))))))) 5.064 * * [simplify]: iters left: 6 (11 enodes) 5.069 * * [simplify]: iters left: 5 (39 enodes) 5.081 * * [simplify]: iters left: 4 (47 enodes) 5.094 * * [simplify]: iters left: 3 (49 enodes) 5.108 * * [simplify]: Extracting #0: cost 1 inf + 0 5.108 * * [simplify]: Extracting #1: cost 6 inf + 0 5.108 * * [simplify]: Extracting #2: cost 12 inf + 0 5.108 * * [simplify]: Extracting #3: cost 13 inf + 1 5.108 * * [simplify]: Extracting #4: cost 14 inf + 83 5.108 * * [simplify]: Extracting #5: cost 19 inf + 83 5.109 * * [simplify]: Extracting #6: cost 15 inf + 308 5.109 * * [simplify]: Extracting #7: cost 9 inf + 1275 5.109 * * [simplify]: Extracting #8: cost 5 inf + 2763 5.110 * * [simplify]: Extracting #9: cost 0 inf + 4953 5.110 * [simplify]: Simplified to (* (* (cbrt (/ (sqrt 2) (+ (exp x) (exp (- x))))) (sqrt 2)) (cbrt (/ (sqrt 2) (+ (exp x) (exp (- x)))))) 5.110 * [simplify]: Simplified (2 1) to (λ (x) (* (* (* (cbrt (/ (sqrt 2) (+ (exp x) (exp (- x))))) (sqrt 2)) (cbrt (/ (sqrt 2) (+ (exp x) (exp (- x)))))) (cbrt (/ (sqrt 2) (+ (exp x) (exp (- x))))))) 5.110 * * * * [progress]: [ 20 / 60 ] simplifiying candidate # 5.110 * [simplify]: Simplifying (* (sqrt 2) (sqrt (/ (sqrt 2) (+ (exp x) (exp (- x)))))) 5.111 * * [simplify]: iters left: 6 (10 enodes) 5.113 * * [simplify]: iters left: 5 (34 enodes) 5.119 * * [simplify]: iters left: 4 (38 enodes) 5.124 * * [simplify]: iters left: 3 (40 enodes) 5.130 * * [simplify]: Extracting #0: cost 1 inf + 0 5.130 * * [simplify]: Extracting #1: cost 4 inf + 0 5.130 * * [simplify]: Extracting #2: cost 8 inf + 0 5.130 * * [simplify]: Extracting #3: cost 9 inf + 1 5.130 * * [simplify]: Extracting #4: cost 10 inf + 83 5.130 * * [simplify]: Extracting #5: cost 15 inf + 83 5.130 * * [simplify]: Extracting #6: cost 11 inf + 308 5.131 * * [simplify]: Extracting #7: cost 4 inf + 1577 5.131 * * [simplify]: Extracting #8: cost 0 inf + 3025 5.131 * [simplify]: Simplified to (* (sqrt (/ (sqrt 2) (+ (exp x) (exp (- x))))) (sqrt 2)) 5.131 * [simplify]: Simplified (2 1) to (λ (x) (* (* (sqrt (/ (sqrt 2) (+ (exp x) (exp (- x))))) (sqrt 2)) (sqrt (/ (sqrt 2) (+ (exp x) (exp (- x))))))) 5.131 * * * * [progress]: [ 21 / 60 ] simplifiying candidate # 5.132 * [simplify]: Simplifying (* (sqrt 2) (/ (* (cbrt (sqrt 2)) (cbrt (sqrt 2))) (* (cbrt (+ (exp x) (exp (- x)))) (cbrt (+ (exp x) (exp (- x))))))) 5.132 * * [simplify]: iters left: 6 (13 enodes) 5.135 * * [simplify]: iters left: 5 (51 enodes) 5.150 * * [simplify]: iters left: 4 (93 enodes) 5.176 * * [simplify]: iters left: 3 (154 enodes) 5.204 * * [simplify]: iters left: 2 (213 enodes) 5.267 * * [simplify]: iters left: 1 (258 enodes) 5.342 * * [simplify]: Extracting #0: cost 1 inf + 0 5.342 * * [simplify]: Extracting #1: cost 26 inf + 0 5.342 * * [simplify]: Extracting #2: cost 52 inf + 0 5.343 * * [simplify]: Extracting #3: cost 52 inf + 83 5.343 * * [simplify]: Extracting #4: cost 50 inf + 1170 5.344 * * [simplify]: Extracting #5: cost 41 inf + 2490 5.349 * * [simplify]: Extracting #6: cost 5 inf + 18907 5.357 * * [simplify]: Extracting #7: cost 0 inf + 21017 5.365 * * [simplify]: Extracting #8: cost 0 inf + 20977 5.373 * [simplify]: Simplified to (* (* (/ (cbrt (sqrt 2)) (cbrt (+ (exp x) (exp (- x))))) (/ (cbrt (sqrt 2)) (cbrt (+ (exp x) (exp (- x)))))) (sqrt 2)) 5.373 * [simplify]: Simplified (2 1) to (λ (x) (* (* (* (/ (cbrt (sqrt 2)) (cbrt (+ (exp x) (exp (- x))))) (/ (cbrt (sqrt 2)) (cbrt (+ (exp x) (exp (- x)))))) (sqrt 2)) (/ (cbrt (sqrt 2)) (cbrt (+ (exp x) (exp (- x))))))) 5.373 * * * * [progress]: [ 22 / 60 ] simplifiying candidate # 5.373 * [simplify]: Simplifying (* (sqrt 2) (/ (* (cbrt (sqrt 2)) (cbrt (sqrt 2))) (sqrt (+ (exp x) (exp (- x)))))) 5.373 * * [simplify]: iters left: 6 (12 enodes) 5.377 * * [simplify]: iters left: 5 (44 enodes) 5.384 * * [simplify]: iters left: 4 (63 enodes) 5.394 * * [simplify]: iters left: 3 (85 enodes) 5.411 * * [simplify]: iters left: 2 (103 enodes) 5.438 * * [simplify]: iters left: 1 (115 enodes) 5.454 * * [simplify]: Extracting #0: cost 1 inf + 0 5.454 * * [simplify]: Extracting #1: cost 16 inf + 0 5.454 * * [simplify]: Extracting #2: cost 32 inf + 0 5.454 * * [simplify]: Extracting #3: cost 33 inf + 42 5.454 * * [simplify]: Extracting #4: cost 31 inf + 969 5.454 * * [simplify]: Extracting #5: cost 27 inf + 1284 5.455 * * [simplify]: Extracting #6: cost 19 inf + 2522 5.455 * * [simplify]: Extracting #7: cost 5 inf + 8309 5.457 * * [simplify]: Extracting #8: cost 0 inf + 10539 5.458 * [simplify]: Simplified to (* (/ (sqrt 2) (sqrt (+ (exp x) (exp (- x))))) (* (cbrt (sqrt 2)) (cbrt (sqrt 2)))) 5.458 * [simplify]: Simplified (2 1) to (λ (x) (* (* (/ (sqrt 2) (sqrt (+ (exp x) (exp (- x))))) (* (cbrt (sqrt 2)) (cbrt (sqrt 2)))) (/ (cbrt (sqrt 2)) (sqrt (+ (exp x) (exp (- x))))))) 5.459 * * * * [progress]: [ 23 / 60 ] simplifiying candidate # 5.459 * [simplify]: Simplifying (* (sqrt 2) (/ (* (cbrt (sqrt 2)) (cbrt (sqrt 2))) 1)) 5.459 * * [simplify]: iters left: 6 (7 enodes) 5.461 * * [simplify]: iters left: 5 (26 enodes) 5.468 * * [simplify]: iters left: 4 (44 enodes) 5.480 * * [simplify]: iters left: 3 (62 enodes) 5.490 * * [simplify]: iters left: 2 (74 enodes) 5.504 * * [simplify]: iters left: 1 (88 enodes) 5.532 * * [simplify]: Extracting #0: cost 1 inf + 0 5.532 * * [simplify]: Extracting #1: cost 11 inf + 0 5.532 * * [simplify]: Extracting #2: cost 19 inf + 1 5.532 * * [simplify]: Extracting #3: cost 15 inf + 166 5.533 * * [simplify]: Extracting #4: cost 6 inf + 1580 5.534 * * [simplify]: Extracting #5: cost 1 inf + 2467 5.535 * * [simplify]: Extracting #6: cost 0 inf + 2668 5.536 * [simplify]: Simplified to (* (* (cbrt (sqrt 2)) (sqrt 2)) (cbrt (sqrt 2))) 5.536 * [simplify]: Simplified (2 1) to (λ (x) (* (* (* (cbrt (sqrt 2)) (sqrt 2)) (cbrt (sqrt 2))) (/ (cbrt (sqrt 2)) (+ (exp x) (exp (- x)))))) 5.536 * * * * [progress]: [ 24 / 60 ] simplifiying candidate # 5.537 * [simplify]: Simplifying (* (sqrt 2) (/ (* (cbrt (sqrt 2)) (cbrt (sqrt 2))) 1)) 5.537 * * [simplify]: iters left: 6 (7 enodes) 5.541 * * [simplify]: iters left: 5 (26 enodes) 5.551 * * [simplify]: iters left: 4 (44 enodes) 5.565 * * [simplify]: iters left: 3 (62 enodes) 5.584 * * [simplify]: iters left: 2 (74 enodes) 5.595 * * [simplify]: iters left: 1 (88 enodes) 5.610 * * [simplify]: Extracting #0: cost 1 inf + 0 5.610 * * [simplify]: Extracting #1: cost 11 inf + 0 5.610 * * [simplify]: Extracting #2: cost 19 inf + 1 5.610 * * [simplify]: Extracting #3: cost 15 inf + 166 5.610 * * [simplify]: Extracting #4: cost 6 inf + 1580 5.611 * * [simplify]: Extracting #5: cost 1 inf + 2467 5.611 * * [simplify]: Extracting #6: cost 0 inf + 2668 5.612 * [simplify]: Simplified to (* (* (cbrt (sqrt 2)) (sqrt 2)) (cbrt (sqrt 2))) 5.612 * [simplify]: Simplified (2 1) to (λ (x) (* (* (* (cbrt (sqrt 2)) (sqrt 2)) (cbrt (sqrt 2))) (/ (cbrt (sqrt 2)) (+ (exp x) (exp (- x)))))) 5.612 * * * * [progress]: [ 25 / 60 ] simplifiying candidate # 5.612 * [simplify]: Simplifying (* (sqrt 2) (/ (sqrt (* (cbrt 2) (cbrt 2))) (* (cbrt (+ (exp x) (exp (- x)))) (cbrt (+ (exp x) (exp (- x))))))) 5.612 * * [simplify]: iters left: 6 (14 enodes) 5.619 * * [simplify]: iters left: 5 (51 enodes) 5.636 * * [simplify]: iters left: 4 (71 enodes) 5.657 * * [simplify]: iters left: 3 (89 enodes) 5.672 * * [simplify]: iters left: 2 (103 enodes) 5.687 * * [simplify]: iters left: 1 (113 enodes) 5.711 * * [simplify]: Extracting #0: cost 1 inf + 0 5.711 * * [simplify]: Extracting #1: cost 16 inf + 0 5.712 * * [simplify]: Extracting #2: cost 34 inf + 0 5.712 * * [simplify]: Extracting #3: cost 37 inf + 42 5.712 * * [simplify]: Extracting #4: cost 36 inf + 608 5.713 * * [simplify]: Extracting #5: cost 32 inf + 1133 5.713 * * [simplify]: Extracting #6: cost 27 inf + 1468 5.714 * * [simplify]: Extracting #7: cost 24 inf + 2021 5.718 * * [simplify]: Extracting #8: cost 11 inf + 7583 5.721 * * [simplify]: Extracting #9: cost 0 inf + 12625 5.725 * [simplify]: Simplified to (* (/ (sqrt 2) (* (cbrt (+ (exp (- x)) (exp x))) (cbrt (+ (exp (- x)) (exp x))))) (fabs (cbrt 2))) 5.725 * [simplify]: Simplified (2 1) to (λ (x) (* (* (/ (sqrt 2) (* (cbrt (+ (exp (- x)) (exp x))) (cbrt (+ (exp (- x)) (exp x))))) (fabs (cbrt 2))) (/ (sqrt (cbrt 2)) (cbrt (+ (exp x) (exp (- x))))))) 5.725 * * * * [progress]: [ 26 / 60 ] simplifiying candidate # 5.726 * [simplify]: Simplifying (* (sqrt 2) (/ (sqrt (* (cbrt 2) (cbrt 2))) (sqrt (+ (exp x) (exp (- x)))))) 5.726 * * [simplify]: iters left: 6 (13 enodes) 5.733 * * [simplify]: iters left: 5 (46 enodes) 5.748 * * [simplify]: iters left: 4 (56 enodes) 5.764 * * [simplify]: iters left: 3 (62 enodes) 5.780 * * [simplify]: iters left: 2 (66 enodes) 5.790 * * [simplify]: iters left: 1 (69 enodes) 5.801 * * [simplify]: Extracting #0: cost 1 inf + 0 5.801 * * [simplify]: Extracting #1: cost 10 inf + 0 5.801 * * [simplify]: Extracting #2: cost 22 inf + 0 5.801 * * [simplify]: Extracting #3: cost 26 inf + 1 5.801 * * [simplify]: Extracting #4: cost 24 inf + 688 5.801 * * [simplify]: Extracting #5: cost 21 inf + 932 5.802 * * [simplify]: Extracting #6: cost 14 inf + 1759 5.803 * * [simplify]: Extracting #7: cost 3 inf + 5417 5.805 * * [simplify]: Extracting #8: cost 0 inf + 6603 5.806 * [simplify]: Simplified to (* (/ (sqrt 2) (sqrt (+ (exp (- x)) (exp x)))) (fabs (cbrt 2))) 5.806 * [simplify]: Simplified (2 1) to (λ (x) (* (* (/ (sqrt 2) (sqrt (+ (exp (- x)) (exp x)))) (fabs (cbrt 2))) (/ (sqrt (cbrt 2)) (sqrt (+ (exp x) (exp (- x))))))) 5.806 * * * * [progress]: [ 27 / 60 ] simplifiying candidate # 5.807 * [simplify]: Simplifying (* (sqrt 2) (/ (sqrt (* (cbrt 2) (cbrt 2))) 1)) 5.807 * * [simplify]: iters left: 6 (8 enodes) 5.812 * * [simplify]: iters left: 5 (27 enodes) 5.822 * * [simplify]: iters left: 4 (34 enodes) 5.832 * * [simplify]: iters left: 3 (38 enodes) 5.843 * * [simplify]: iters left: 2 (47 enodes) 5.860 * * [simplify]: iters left: 1 (50 enodes) 5.870 * * [simplify]: Extracting #0: cost 1 inf + 0 5.870 * * [simplify]: Extracting #1: cost 7 inf + 0 5.870 * * [simplify]: Extracting #2: cost 13 inf + 1 5.870 * * [simplify]: Extracting #3: cost 14 inf + 2 5.870 * * [simplify]: Extracting #4: cost 10 inf + 326 5.870 * * [simplify]: Extracting #5: cost 4 inf + 1013 5.870 * * [simplify]: Extracting #6: cost 0 inf + 1620 5.871 * [simplify]: Simplified to (* (sqrt 2) (fabs (cbrt 2))) 5.871 * [simplify]: Simplified (2 1) to (λ (x) (* (* (sqrt 2) (fabs (cbrt 2))) (/ (sqrt (cbrt 2)) (+ (exp x) (exp (- x)))))) 5.871 * * * * [progress]: [ 28 / 60 ] simplifiying candidate # 5.871 * [simplify]: Simplifying (* (sqrt 2) (/ (sqrt (* (cbrt 2) (cbrt 2))) 1)) 5.871 * * [simplify]: iters left: 6 (8 enodes) 5.874 * * [simplify]: iters left: 5 (27 enodes) 5.878 * * [simplify]: iters left: 4 (34 enodes) 5.884 * * [simplify]: iters left: 3 (38 enodes) 5.889 * * [simplify]: iters left: 2 (47 enodes) 5.899 * * [simplify]: iters left: 1 (50 enodes) 5.913 * * [simplify]: Extracting #0: cost 1 inf + 0 5.913 * * [simplify]: Extracting #1: cost 7 inf + 0 5.913 * * [simplify]: Extracting #2: cost 13 inf + 1 5.914 * * [simplify]: Extracting #3: cost 14 inf + 2 5.914 * * [simplify]: Extracting #4: cost 10 inf + 326 5.914 * * [simplify]: Extracting #5: cost 4 inf + 1013 5.914 * * [simplify]: Extracting #6: cost 0 inf + 1620 5.915 * [simplify]: Simplified to (* (sqrt 2) (fabs (cbrt 2))) 5.915 * [simplify]: Simplified (2 1) to (λ (x) (* (* (sqrt 2) (fabs (cbrt 2))) (/ (sqrt (cbrt 2)) (+ (exp x) (exp (- x)))))) 5.915 * * * * [progress]: [ 29 / 60 ] simplifiying candidate # 5.915 * [simplify]: Simplifying (* (sqrt 2) (/ (sqrt (sqrt 2)) (* (cbrt (+ (exp x) (exp (- x)))) (cbrt (+ (exp x) (exp (- x))))))) 5.916 * * [simplify]: iters left: 6 (12 enodes) 5.922 * * [simplify]: iters left: 5 (44 enodes) 5.936 * * [simplify]: iters left: 4 (64 enodes) 5.950 * * [simplify]: iters left: 3 (82 enodes) 5.962 * * [simplify]: iters left: 2 (96 enodes) 5.980 * * [simplify]: iters left: 1 (106 enodes) 6.009 * * [simplify]: Extracting #0: cost 1 inf + 0 6.009 * * [simplify]: Extracting #1: cost 16 inf + 0 6.009 * * [simplify]: Extracting #2: cost 32 inf + 0 6.009 * * [simplify]: Extracting #3: cost 33 inf + 42 6.010 * * [simplify]: Extracting #4: cost 33 inf + 487 6.010 * * [simplify]: Extracting #5: cost 29 inf + 672 6.010 * * [simplify]: Extracting #6: cost 17 inf + 4048 6.012 * * [simplify]: Extracting #7: cost 3 inf + 10035 6.013 * * [simplify]: Extracting #8: cost 0 inf + 11341 6.015 * [simplify]: Simplified to (* (/ (sqrt 2) (cbrt (+ (exp (- x)) (exp x)))) (/ (sqrt (sqrt 2)) (cbrt (+ (exp (- x)) (exp x))))) 6.015 * [simplify]: Simplified (2 1) to (λ (x) (* (* (/ (sqrt 2) (cbrt (+ (exp (- x)) (exp x)))) (/ (sqrt (sqrt 2)) (cbrt (+ (exp (- x)) (exp x))))) (/ (sqrt (sqrt 2)) (cbrt (+ (exp x) (exp (- x))))))) 6.015 * * * * [progress]: [ 30 / 60 ] simplifiying candidate # 6.015 * [simplify]: Simplifying (* (sqrt 2) (/ (sqrt (sqrt 2)) (sqrt (+ (exp x) (exp (- x)))))) 6.015 * * [simplify]: iters left: 6 (11 enodes) 6.018 * * [simplify]: iters left: 5 (39 enodes) 6.025 * * [simplify]: iters left: 4 (49 enodes) 6.032 * * [simplify]: iters left: 3 (55 enodes) 6.040 * * [simplify]: iters left: 2 (59 enodes) 6.055 * * [simplify]: iters left: 1 (62 enodes) 6.073 * * [simplify]: Extracting #0: cost 1 inf + 0 6.073 * * [simplify]: Extracting #1: cost 10 inf + 0 6.073 * * [simplify]: Extracting #2: cost 20 inf + 0 6.073 * * [simplify]: Extracting #3: cost 22 inf + 1 6.073 * * [simplify]: Extracting #4: cost 25 inf + 83 6.074 * * [simplify]: Extracting #5: cost 17 inf + 672 6.074 * * [simplify]: Extracting #6: cost 9 inf + 2442 6.077 * * [simplify]: Extracting #7: cost 0 inf + 5639 6.079 * [simplify]: Simplified to (* (sqrt 2) (/ (sqrt (sqrt 2)) (sqrt (+ (exp (- x)) (exp x))))) 6.079 * [simplify]: Simplified (2 1) to (λ (x) (* (* (sqrt 2) (/ (sqrt (sqrt 2)) (sqrt (+ (exp (- x)) (exp x))))) (/ (sqrt (sqrt 2)) (sqrt (+ (exp x) (exp (- x))))))) 6.079 * * * * [progress]: [ 31 / 60 ] simplifiying candidate # 6.079 * [simplify]: Simplifying (* (sqrt 2) (/ (sqrt (sqrt 2)) 1)) 6.080 * * [simplify]: iters left: 6 (6 enodes) 6.084 * * [simplify]: iters left: 5 (21 enodes) 6.091 * * [simplify]: iters left: 4 (25 enodes) 6.099 * * [simplify]: iters left: 3 (35 enodes) 6.105 * * [simplify]: iters left: 2 (37 enodes) 6.111 * * [simplify]: iters left: 1 (42 enodes) 6.117 * * [simplify]: Extracting #0: cost 1 inf + 0 6.117 * * [simplify]: Extracting #1: cost 7 inf + 0 6.117 * * [simplify]: Extracting #2: cost 11 inf + 1 6.117 * * [simplify]: Extracting #3: cost 10 inf + 2 6.117 * * [simplify]: Extracting #4: cost 1 inf + 774 6.118 * * [simplify]: Extracting #5: cost 0 inf + 896 6.118 * [simplify]: Simplified to (* (sqrt 2) (sqrt (sqrt 2))) 6.118 * [simplify]: Simplified (2 1) to (λ (x) (* (* (sqrt 2) (sqrt (sqrt 2))) (/ (sqrt (sqrt 2)) (+ (exp x) (exp (- x)))))) 6.118 * * * * [progress]: [ 32 / 60 ] simplifiying candidate # 6.118 * [simplify]: Simplifying (* (sqrt 2) (/ (sqrt (sqrt 2)) 1)) 6.118 * * [simplify]: iters left: 6 (6 enodes) 6.120 * * [simplify]: iters left: 5 (21 enodes) 6.126 * * [simplify]: iters left: 4 (25 enodes) 6.131 * * [simplify]: iters left: 3 (35 enodes) 6.136 * * [simplify]: iters left: 2 (37 enodes) 6.144 * * [simplify]: iters left: 1 (42 enodes) 6.155 * * [simplify]: Extracting #0: cost 1 inf + 0 6.155 * * [simplify]: Extracting #1: cost 7 inf + 0 6.155 * * [simplify]: Extracting #2: cost 11 inf + 1 6.155 * * [simplify]: Extracting #3: cost 10 inf + 2 6.156 * * [simplify]: Extracting #4: cost 1 inf + 774 6.156 * * [simplify]: Extracting #5: cost 0 inf + 896 6.157 * [simplify]: Simplified to (* (sqrt 2) (sqrt (sqrt 2))) 6.157 * [simplify]: Simplified (2 1) to (λ (x) (* (* (sqrt 2) (sqrt (sqrt 2))) (/ (sqrt (sqrt 2)) (+ (exp x) (exp (- x)))))) 6.157 * * * * [progress]: [ 33 / 60 ] simplifiying candidate # 6.157 * [simplify]: Simplifying (* (sqrt 2) (/ (sqrt 1) (* (cbrt (+ (exp x) (exp (- x)))) (cbrt (+ (exp x) (exp (- x))))))) 6.158 * * [simplify]: iters left: 6 (13 enodes) 6.166 * * [simplify]: iters left: 5 (48 enodes) 6.181 * * [simplify]: iters left: 4 (70 enodes) 6.196 * * [simplify]: iters left: 3 (106 enodes) 6.214 * * [simplify]: iters left: 2 (148 enodes) 6.254 * * [simplify]: iters left: 1 (189 enodes) 6.294 * * [simplify]: Extracting #0: cost 1 inf + 0 6.294 * * [simplify]: Extracting #1: cost 11 inf + 0 6.294 * * [simplify]: Extracting #2: cost 20 inf + 1 6.294 * * [simplify]: Extracting #3: cost 20 inf + 84 6.294 * * [simplify]: Extracting #4: cost 24 inf + 84 6.295 * * [simplify]: Extracting #5: cost 23 inf + 156 6.295 * * [simplify]: Extracting #6: cost 16 inf + 1053 6.296 * * [simplify]: Extracting #7: cost 5 inf + 4931 6.299 * * [simplify]: Extracting #8: cost 0 inf + 6921 6.301 * [simplify]: Simplified to (/ (/ (sqrt 2) (cbrt (+ (exp x) (exp (- x))))) (cbrt (+ (exp x) (exp (- x))))) 6.301 * [simplify]: Simplified (2 1) to (λ (x) (* (/ (/ (sqrt 2) (cbrt (+ (exp x) (exp (- x))))) (cbrt (+ (exp x) (exp (- x))))) (/ (sqrt 2) (cbrt (+ (exp x) (exp (- x))))))) 6.301 * * * * [progress]: [ 34 / 60 ] simplifiying candidate # 6.302 * [simplify]: Simplifying (* (sqrt 2) (/ (sqrt 1) (sqrt (+ (exp x) (exp (- x)))))) 6.302 * * [simplify]: iters left: 6 (12 enodes) 6.310 * * [simplify]: iters left: 5 (43 enodes) 6.322 * * [simplify]: iters left: 4 (51 enodes) 6.331 * * [simplify]: iters left: 3 (56 enodes) 6.338 * * [simplify]: iters left: 2 (60 enodes) 6.346 * * [simplify]: iters left: 1 (64 enodes) 6.358 * * [simplify]: Extracting #0: cost 1 inf + 0 6.359 * * [simplify]: Extracting #1: cost 7 inf + 0 6.359 * * [simplify]: Extracting #2: cost 12 inf + 1 6.359 * * [simplify]: Extracting #3: cost 14 inf + 2 6.359 * * [simplify]: Extracting #4: cost 17 inf + 43 6.359 * * [simplify]: Extracting #5: cost 13 inf + 308 6.360 * * [simplify]: Extracting #6: cost 4 inf + 2260 6.361 * * [simplify]: Extracting #7: cost 0 inf + 3467 6.362 * [simplify]: Simplified to (/ (sqrt 2) (sqrt (+ (exp x) (exp (- x))))) 6.362 * [simplify]: Simplified (2 1) to (λ (x) (* (/ (sqrt 2) (sqrt (+ (exp x) (exp (- x))))) (/ (sqrt 2) (sqrt (+ (exp x) (exp (- x))))))) 6.362 * * * * [progress]: [ 35 / 60 ] simplifiying candidate # 6.362 * [simplify]: Simplifying (* (sqrt 2) (/ (sqrt 1) 1)) 6.362 * * [simplify]: iters left: 5 (6 enodes) 6.368 * * [simplify]: iters left: 4 (21 enodes) 6.375 * * [simplify]: iters left: 3 (23 enodes) 6.383 * * [simplify]: iters left: 2 (29 enodes) 6.390 * * [simplify]: iters left: 1 (34 enodes) 6.401 * * [simplify]: Extracting #0: cost 1 inf + 0 6.401 * * [simplify]: Extracting #1: cost 5 inf + 0 6.401 * * [simplify]: Extracting #2: cost 2 inf + 125 6.401 * * [simplify]: Extracting #3: cost 0 inf + 248 6.401 * [simplify]: Simplified to (sqrt 2) 6.401 * [simplify]: Simplified (2 1) to (λ (x) (* (sqrt 2) (/ (sqrt 2) (+ (exp x) (exp (- x)))))) 6.402 * * * * [progress]: [ 36 / 60 ] simplifiying candidate # 6.402 * [simplify]: Simplifying (* (sqrt 2) (/ (sqrt 1) 1)) 6.402 * * [simplify]: iters left: 5 (6 enodes) 6.408 * * [simplify]: iters left: 4 (21 enodes) 6.414 * * [simplify]: iters left: 3 (23 enodes) 6.421 * * [simplify]: iters left: 2 (29 enodes) 6.425 * * [simplify]: iters left: 1 (34 enodes) 6.429 * * [simplify]: Extracting #0: cost 1 inf + 0 6.430 * * [simplify]: Extracting #1: cost 5 inf + 0 6.430 * * [simplify]: Extracting #2: cost 2 inf + 125 6.430 * * [simplify]: Extracting #3: cost 0 inf + 248 6.430 * [simplify]: Simplified to (sqrt 2) 6.430 * [simplify]: Simplified (2 1) to (λ (x) (* (sqrt 2) (/ (sqrt 2) (+ (exp x) (exp (- x)))))) 6.430 * * * * [progress]: [ 37 / 60 ] simplifiying candidate # 6.430 * [simplify]: Simplifying (* (sqrt 2) (/ (sqrt (sqrt 2)) (* (cbrt (+ (exp x) (exp (- x)))) (cbrt (+ (exp x) (exp (- x))))))) 6.430 * * [simplify]: iters left: 6 (12 enodes) 6.433 * * [simplify]: iters left: 5 (44 enodes) 6.441 * * [simplify]: iters left: 4 (64 enodes) 6.451 * * [simplify]: iters left: 3 (82 enodes) 6.462 * * [simplify]: iters left: 2 (96 enodes) 6.482 * * [simplify]: iters left: 1 (106 enodes) 6.513 * * [simplify]: Extracting #0: cost 1 inf + 0 6.513 * * [simplify]: Extracting #1: cost 16 inf + 0 6.513 * * [simplify]: Extracting #2: cost 32 inf + 0 6.513 * * [simplify]: Extracting #3: cost 33 inf + 42 6.513 * * [simplify]: Extracting #4: cost 33 inf + 487 6.514 * * [simplify]: Extracting #5: cost 29 inf + 672 6.515 * * [simplify]: Extracting #6: cost 17 inf + 4048 6.517 * * [simplify]: Extracting #7: cost 3 inf + 10035 6.520 * * [simplify]: Extracting #8: cost 0 inf + 11341 6.524 * [simplify]: Simplified to (* (/ (sqrt 2) (cbrt (+ (exp (- x)) (exp x)))) (/ (sqrt (sqrt 2)) (cbrt (+ (exp (- x)) (exp x))))) 6.524 * [simplify]: Simplified (2 1) to (λ (x) (* (* (/ (sqrt 2) (cbrt (+ (exp (- x)) (exp x)))) (/ (sqrt (sqrt 2)) (cbrt (+ (exp (- x)) (exp x))))) (/ (sqrt (sqrt 2)) (cbrt (+ (exp x) (exp (- x))))))) 6.524 * * * * [progress]: [ 38 / 60 ] simplifiying candidate # 6.524 * [simplify]: Simplifying (* (sqrt 2) (/ (sqrt (sqrt 2)) (sqrt (+ (exp x) (exp (- x)))))) 6.524 * * [simplify]: iters left: 6 (11 enodes) 6.531 * * [simplify]: iters left: 5 (39 enodes) 6.543 * * [simplify]: iters left: 4 (49 enodes) 6.551 * * [simplify]: iters left: 3 (55 enodes) 6.559 * * [simplify]: iters left: 2 (59 enodes) 6.568 * * [simplify]: iters left: 1 (62 enodes) 6.579 * * [simplify]: Extracting #0: cost 1 inf + 0 6.579 * * [simplify]: Extracting #1: cost 10 inf + 0 6.579 * * [simplify]: Extracting #2: cost 20 inf + 0 6.579 * * [simplify]: Extracting #3: cost 22 inf + 1 6.579 * * [simplify]: Extracting #4: cost 25 inf + 83 6.580 * * [simplify]: Extracting #5: cost 17 inf + 672 6.580 * * [simplify]: Extracting #6: cost 9 inf + 2442 6.581 * * [simplify]: Extracting #7: cost 0 inf + 5639 6.583 * [simplify]: Simplified to (* (sqrt 2) (/ (sqrt (sqrt 2)) (sqrt (+ (exp (- x)) (exp x))))) 6.583 * [simplify]: Simplified (2 1) to (λ (x) (* (* (sqrt 2) (/ (sqrt (sqrt 2)) (sqrt (+ (exp (- x)) (exp x))))) (/ (sqrt (sqrt 2)) (sqrt (+ (exp x) (exp (- x))))))) 6.583 * * * * [progress]: [ 39 / 60 ] simplifiying candidate # 6.583 * [simplify]: Simplifying (* (sqrt 2) (/ (sqrt (sqrt 2)) 1)) 6.583 * * [simplify]: iters left: 6 (6 enodes) 6.587 * * [simplify]: iters left: 5 (21 enodes) 6.595 * * [simplify]: iters left: 4 (25 enodes) 6.603 * * [simplify]: iters left: 3 (35 enodes) 6.614 * * [simplify]: iters left: 2 (37 enodes) 6.624 * * [simplify]: iters left: 1 (42 enodes) 6.637 * * [simplify]: Extracting #0: cost 1 inf + 0 6.637 * * [simplify]: Extracting #1: cost 7 inf + 0 6.637 * * [simplify]: Extracting #2: cost 11 inf + 1 6.637 * * [simplify]: Extracting #3: cost 10 inf + 2 6.637 * * [simplify]: Extracting #4: cost 1 inf + 774 6.638 * * [simplify]: Extracting #5: cost 0 inf + 896 6.638 * [simplify]: Simplified to (* (sqrt 2) (sqrt (sqrt 2))) 6.638 * [simplify]: Simplified (2 1) to (λ (x) (* (* (sqrt 2) (sqrt (sqrt 2))) (/ (sqrt (sqrt 2)) (+ (exp x) (exp (- x)))))) 6.639 * * * * [progress]: [ 40 / 60 ] simplifiying candidate # 6.639 * [simplify]: Simplifying (* (sqrt 2) (/ (sqrt (sqrt 2)) 1)) 6.639 * * [simplify]: iters left: 6 (6 enodes) 6.644 * * [simplify]: iters left: 5 (21 enodes) 6.650 * * [simplify]: iters left: 4 (25 enodes) 6.654 * * [simplify]: iters left: 3 (35 enodes) 6.660 * * [simplify]: iters left: 2 (37 enodes) 6.665 * * [simplify]: iters left: 1 (42 enodes) 6.671 * * [simplify]: Extracting #0: cost 1 inf + 0 6.671 * * [simplify]: Extracting #1: cost 7 inf + 0 6.671 * * [simplify]: Extracting #2: cost 11 inf + 1 6.671 * * [simplify]: Extracting #3: cost 10 inf + 2 6.671 * * [simplify]: Extracting #4: cost 1 inf + 774 6.671 * * [simplify]: Extracting #5: cost 0 inf + 896 6.671 * [simplify]: Simplified to (* (sqrt 2) (sqrt (sqrt 2))) 6.671 * [simplify]: Simplified (2 1) to (λ (x) (* (* (sqrt 2) (sqrt (sqrt 2))) (/ (sqrt (sqrt 2)) (+ (exp x) (exp (- x)))))) 6.671 * * * * [progress]: [ 41 / 60 ] simplifiying candidate # 6.672 * [simplify]: Simplifying (* (sqrt 2) (/ 1 (* (cbrt (+ (exp x) (exp (- x)))) (cbrt (+ (exp x) (exp (- x))))))) 6.672 * * [simplify]: iters left: 6 (12 enodes) 6.675 * * [simplify]: iters left: 5 (45 enodes) 6.687 * * [simplify]: iters left: 4 (59 enodes) 6.700 * * [simplify]: iters left: 3 (84 enodes) 6.714 * * [simplify]: iters left: 2 (97 enodes) 6.741 * * [simplify]: iters left: 1 (102 enodes) 6.765 * * [simplify]: Extracting #0: cost 1 inf + 0 6.765 * * [simplify]: Extracting #1: cost 11 inf + 0 6.765 * * [simplify]: Extracting #2: cost 20 inf + 1 6.765 * * [simplify]: Extracting #3: cost 22 inf + 2 6.765 * * [simplify]: Extracting #4: cost 25 inf + 43 6.766 * * [simplify]: Extracting #5: cost 21 inf + 268 6.766 * * [simplify]: Extracting #6: cost 14 inf + 1615 6.767 * * [simplify]: Extracting #7: cost 2 inf + 6117 6.770 * * [simplify]: Extracting #8: cost 0 inf + 6921 6.772 * [simplify]: Simplified to (/ (sqrt 2) (* (cbrt (+ (exp (- x)) (exp x))) (cbrt (+ (exp (- x)) (exp x))))) 6.772 * [simplify]: Simplified (2 1) to (λ (x) (* (/ (sqrt 2) (* (cbrt (+ (exp (- x)) (exp x))) (cbrt (+ (exp (- x)) (exp x))))) (/ (sqrt 2) (cbrt (+ (exp x) (exp (- x))))))) 6.772 * * * * [progress]: [ 42 / 60 ] simplifiying candidate # 6.773 * [simplify]: Simplifying (* (sqrt 2) (/ 1 (sqrt (+ (exp x) (exp (- x)))))) 6.773 * * [simplify]: iters left: 6 (11 enodes) 6.779 * * [simplify]: iters left: 5 (40 enodes) 6.791 * * [simplify]: iters left: 4 (46 enodes) 6.806 * * [simplify]: iters left: 3 (55 enodes) 6.821 * * [simplify]: iters left: 2 (57 enodes) 6.837 * * [simplify]: iters left: 1 (60 enodes) 6.852 * * [simplify]: Extracting #0: cost 1 inf + 0 6.852 * * [simplify]: Extracting #1: cost 7 inf + 0 6.852 * * [simplify]: Extracting #2: cost 12 inf + 1 6.852 * * [simplify]: Extracting #3: cost 14 inf + 2 6.852 * * [simplify]: Extracting #4: cost 17 inf + 43 6.853 * * [simplify]: Extracting #5: cost 15 inf + 126 6.853 * * [simplify]: Extracting #6: cost 8 inf + 973 6.853 * * [simplify]: Extracting #7: cost 4 inf + 2139 6.854 * * [simplify]: Extracting #8: cost 0 inf + 3467 6.855 * [simplify]: Simplified to (/ (sqrt 2) (sqrt (+ (exp (- x)) (exp x)))) 6.856 * [simplify]: Simplified (2 1) to (λ (x) (* (/ (sqrt 2) (sqrt (+ (exp (- x)) (exp x)))) (/ (sqrt 2) (sqrt (+ (exp x) (exp (- x))))))) 6.856 * * * * [progress]: [ 43 / 60 ] simplifiying candidate # 6.856 * [simplify]: Simplifying (* (sqrt 2) (/ 1 1)) 6.856 * * [simplify]: iters left: 4 (5 enodes) 6.859 * * [simplify]: iters left: 3 (16 enodes) 6.865 * * [simplify]: iters left: 2 (18 enodes) 6.874 * * [simplify]: iters left: 1 (21 enodes) 6.879 * * [simplify]: Extracting #0: cost 1 inf + 0 6.879 * * [simplify]: Extracting #1: cost 4 inf + 0 6.879 * * [simplify]: Extracting #2: cost 2 inf + 2 6.879 * * [simplify]: Extracting #3: cost 1 inf + 43 6.879 * * [simplify]: Extracting #4: cost 0 inf + 84 6.879 * [simplify]: Simplified to (sqrt 2) 6.879 * [simplify]: Simplified (2 1) to (λ (x) (* (sqrt 2) (/ (sqrt 2) (+ (exp x) (exp (- x)))))) 6.880 * * * * [progress]: [ 44 / 60 ] simplifiying candidate # 6.880 * [simplify]: Simplifying (* (sqrt 2) (/ 1 1)) 6.880 * * [simplify]: iters left: 4 (5 enodes) 6.883 * * [simplify]: iters left: 3 (16 enodes) 6.889 * * [simplify]: iters left: 2 (18 enodes) 6.894 * * [simplify]: iters left: 1 (21 enodes) 6.900 * * [simplify]: Extracting #0: cost 1 inf + 0 6.900 * * [simplify]: Extracting #1: cost 4 inf + 0 6.900 * * [simplify]: Extracting #2: cost 2 inf + 2 6.900 * * [simplify]: Extracting #3: cost 1 inf + 43 6.900 * * [simplify]: Extracting #4: cost 0 inf + 84 6.901 * [simplify]: Simplified to (sqrt 2) 6.901 * [simplify]: Simplified (2 1) to (λ (x) (* (sqrt 2) (/ (sqrt 2) (+ (exp x) (exp (- x)))))) 6.901 * * * * [progress]: [ 45 / 60 ] simplifiying candidate # 6.901 * [simplify]: Simplifying (* (sqrt 2) 1) 6.901 * * [simplify]: iters left: 3 (4 enodes) 6.904 * * [simplify]: iters left: 2 (13 enodes) 6.910 * * [simplify]: iters left: 1 (17 enodes) 6.915 * * [simplify]: Extracting #0: cost 1 inf + 0 6.915 * * [simplify]: Extracting #1: cost 4 inf + 0 6.915 * * [simplify]: Extracting #2: cost 0 inf + 84 6.915 * [simplify]: Simplified to (sqrt 2) 6.915 * [simplify]: Simplified (2 1) to (λ (x) (* (sqrt 2) (/ (sqrt 2) (+ (exp x) (exp (- x)))))) 6.915 * * * * [progress]: [ 46 / 60 ] simplifiying candidate # 6.916 * [simplify]: Simplifying (* (sqrt 2) (sqrt 2)) 6.916 * * [simplify]: iters left: 3 (3 enodes) 6.918 * * [simplify]: iters left: 2 (7 enodes) 6.920 * * [simplify]: Extracting #0: cost 1 inf + 0 6.920 * * [simplify]: Extracting #1: cost 0 inf + 1 6.920 * [simplify]: Simplified to 2 6.920 * [simplify]: Simplified (2 1) to (λ (x) (* 2 (/ 1 (+ (exp x) (exp (- x)))))) 6.920 * * * * [progress]: [ 47 / 60 ] simplifiying candidate # 6.921 * [simplify]: Simplifying (* (sqrt 2) (/ (sqrt 2) (+ (pow (exp x) 3) (pow (exp (- x)) 3)))) 6.921 * * [simplify]: iters left: 6 (12 enodes) 6.928 * * [simplify]: iters left: 5 (54 enodes) 6.949 * * [simplify]: iters left: 4 (97 enodes) 6.972 * * [simplify]: iters left: 3 (177 enodes) 7.031 * * [simplify]: iters left: 2 (293 enodes) 7.157 * * [simplify]: Extracting #0: cost 1 inf + 0 7.157 * * [simplify]: Extracting #1: cost 6 inf + 0 7.157 * * [simplify]: Extracting #2: cost 10 inf + 1 7.158 * * [simplify]: Extracting #3: cost 61 inf + 83 7.158 * * [simplify]: Extracting #4: cost 115 inf + 86 7.159 * * [simplify]: Extracting #5: cost 110 inf + 1402 7.162 * * [simplify]: Extracting #6: cost 59 inf + 14752 7.169 * * [simplify]: Extracting #7: cost 11 inf + 40051 7.177 * * [simplify]: Extracting #8: cost 0 inf + 47242 7.185 * [simplify]: Simplified to (/ 2 (+ (exp (+ x (+ x x))) (* (* (exp (- x)) (exp (- x))) (exp (- x))))) 7.185 * [simplify]: Simplified (2 1) to (λ (x) (* (/ 2 (+ (exp (+ x (+ x x))) (* (* (exp (- x)) (exp (- x))) (exp (- x))))) (+ (* (exp x) (exp x)) (- (* (exp (- x)) (exp (- x))) (* (exp x) (exp (- x))))))) 7.185 * * * * [progress]: [ 48 / 60 ] simplifiying candidate # 7.185 * [simplify]: Simplifying (* (sqrt 2) (/ (sqrt 2) (- (* (exp x) (exp x)) (* (exp (- x)) (exp (- x)))))) 7.186 * * [simplify]: iters left: 6 (11 enodes) 7.191 * * [simplify]: iters left: 5 (47 enodes) 7.207 * * [simplify]: iters left: 4 (76 enodes) 7.227 * * [simplify]: iters left: 3 (116 enodes) 7.248 * * [simplify]: iters left: 2 (188 enodes) 7.318 * * [simplify]: iters left: 1 (262 enodes) 7.415 * * [simplify]: Extracting #0: cost 1 inf + 0 7.415 * * [simplify]: Extracting #1: cost 18 inf + 0 7.415 * * [simplify]: Extracting #2: cost 62 inf + 2 7.416 * * [simplify]: Extracting #3: cost 86 inf + 85 7.417 * * [simplify]: Extracting #4: cost 69 inf + 4100 7.423 * * [simplify]: Extracting #5: cost 11 inf + 16618 7.430 * * [simplify]: Extracting #6: cost 1 inf + 18325 7.437 * * [simplify]: Extracting #7: cost 0 inf + 18518 7.444 * [simplify]: Simplified to (/ 2 (+ (/ -1 (* (exp x) (exp x))) (* (exp x) (exp x)))) 7.444 * [simplify]: Simplified (2 1) to (λ (x) (* (/ 2 (+ (/ -1 (* (exp x) (exp x))) (* (exp x) (exp x)))) (- (exp x) (exp (- x))))) 7.445 * * * * [progress]: [ 49 / 60 ] simplifiying candidate # 7.445 * [simplify]: Simplifying (* (cbrt (sqrt 2)) (/ (sqrt 2) (+ (exp x) (exp (- x))))) 7.445 * * [simplify]: iters left: 6 (10 enodes) 7.450 * * [simplify]: iters left: 5 (36 enodes) 7.461 * * [simplify]: iters left: 4 (46 enodes) 7.469 * * [simplify]: iters left: 3 (52 enodes) 7.477 * * [simplify]: iters left: 2 (56 enodes) 7.486 * * [simplify]: iters left: 1 (59 enodes) 7.503 * * [simplify]: Extracting #0: cost 1 inf + 0 7.503 * * [simplify]: Extracting #1: cost 10 inf + 0 7.503 * * [simplify]: Extracting #2: cost 21 inf + 0 7.503 * * [simplify]: Extracting #3: cost 25 inf + 1 7.503 * * [simplify]: Extracting #4: cost 20 inf + 227 7.504 * * [simplify]: Extracting #5: cost 6 inf + 3166 7.505 * * [simplify]: Extracting #6: cost 0 inf + 5117 7.506 * [simplify]: Simplified to (* (sqrt 2) (/ (cbrt (sqrt 2)) (+ (exp (- x)) (exp x)))) 7.506 * [simplify]: Simplified (2 2) to (λ (x) (* (* (cbrt (sqrt 2)) (cbrt (sqrt 2))) (* (sqrt 2) (/ (cbrt (sqrt 2)) (+ (exp (- x)) (exp x)))))) 7.506 * * * * [progress]: [ 50 / 60 ] simplifiying candidate # 7.507 * [simplify]: Simplifying (* (sqrt (cbrt 2)) (/ (sqrt 2) (+ (exp x) (exp (- x))))) 7.507 * * [simplify]: iters left: 6 (11 enodes) 7.513 * * [simplify]: iters left: 5 (39 enodes) 7.519 * * [simplify]: iters left: 4 (49 enodes) 7.526 * * [simplify]: iters left: 3 (55 enodes) 7.534 * * [simplify]: iters left: 2 (59 enodes) 7.549 * * [simplify]: iters left: 1 (62 enodes) 7.566 * * [simplify]: Extracting #0: cost 1 inf + 0 7.567 * * [simplify]: Extracting #1: cost 10 inf + 0 7.567 * * [simplify]: Extracting #2: cost 22 inf + 0 7.567 * * [simplify]: Extracting #3: cost 27 inf + 1 7.567 * * [simplify]: Extracting #4: cost 23 inf + 196 7.567 * * [simplify]: Extracting #5: cost 9 inf + 2272 7.569 * * [simplify]: Extracting #6: cost 0 inf + 5439 7.570 * [simplify]: Simplified to (* (/ (sqrt (cbrt 2)) (+ (exp x) (exp (- x)))) (sqrt 2)) 7.570 * [simplify]: Simplified (2 2) to (λ (x) (* (sqrt (* (cbrt 2) (cbrt 2))) (* (/ (sqrt (cbrt 2)) (+ (exp x) (exp (- x)))) (sqrt 2)))) 7.570 * * * * [progress]: [ 51 / 60 ] simplifiying candidate # 7.570 * [simplify]: Simplifying (* (sqrt (sqrt 2)) (/ (sqrt 2) (+ (exp x) (exp (- x))))) 7.570 * * [simplify]: iters left: 6 (10 enodes) 7.575 * * [simplify]: iters left: 5 (36 enodes) 7.588 * * [simplify]: iters left: 4 (46 enodes) 7.601 * * [simplify]: iters left: 3 (52 enodes) 7.613 * * [simplify]: iters left: 2 (56 enodes) 7.622 * * [simplify]: iters left: 1 (59 enodes) 7.631 * * [simplify]: Extracting #0: cost 1 inf + 0 7.631 * * [simplify]: Extracting #1: cost 10 inf + 0 7.631 * * [simplify]: Extracting #2: cost 21 inf + 0 7.631 * * [simplify]: Extracting #3: cost 25 inf + 1 7.631 * * [simplify]: Extracting #4: cost 20 inf + 227 7.632 * * [simplify]: Extracting #5: cost 6 inf + 2926 7.632 * * [simplify]: Extracting #6: cost 0 inf + 4717 7.633 * [simplify]: Simplified to (* (sqrt 2) (/ (sqrt (sqrt 2)) (+ (exp (- x)) (exp x)))) 7.633 * [simplify]: Simplified (2 2) to (λ (x) (* (sqrt (sqrt 2)) (* (sqrt 2) (/ (sqrt (sqrt 2)) (+ (exp (- x)) (exp x)))))) 7.633 * * * * [progress]: [ 52 / 60 ] simplifiying candidate # 7.633 * [simplify]: Simplifying (* (sqrt 2) (/ (sqrt 2) (+ (exp x) (exp (- x))))) 7.633 * * [simplify]: iters left: 6 (9 enodes) 7.636 * * [simplify]: iters left: 5 (33 enodes) 7.645 * * [simplify]: iters left: 4 (37 enodes) 7.656 * * [simplify]: iters left: 3 (39 enodes) 7.668 * * [simplify]: Extracting #0: cost 1 inf + 0 7.668 * * [simplify]: Extracting #1: cost 6 inf + 0 7.668 * * [simplify]: Extracting #2: cost 10 inf + 1 7.668 * * [simplify]: Extracting #3: cost 13 inf + 83 7.668 * * [simplify]: Extracting #4: cost 9 inf + 308 7.668 * * [simplify]: Extracting #5: cost 1 inf + 1799 7.669 * * [simplify]: Extracting #6: cost 0 inf + 2101 7.670 * [simplify]: Simplified to (/ 2 (+ (exp x) (exp (- x)))) 7.670 * [simplify]: Simplified (2 2) to (λ (x) (* (sqrt 1) (/ 2 (+ (exp x) (exp (- x)))))) 7.670 * * * * [progress]: [ 53 / 60 ] simplifiying candidate # 7.670 * [simplify]: Simplifying (* (sqrt (sqrt 2)) (/ (sqrt 2) (+ (exp x) (exp (- x))))) 7.670 * * [simplify]: iters left: 6 (10 enodes) 7.675 * * [simplify]: iters left: 5 (36 enodes) 7.686 * * [simplify]: iters left: 4 (46 enodes) 7.694 * * [simplify]: iters left: 3 (52 enodes) 7.701 * * [simplify]: iters left: 2 (56 enodes) 7.710 * * [simplify]: iters left: 1 (59 enodes) 7.722 * * [simplify]: Extracting #0: cost 1 inf + 0 7.722 * * [simplify]: Extracting #1: cost 10 inf + 0 7.722 * * [simplify]: Extracting #2: cost 21 inf + 0 7.722 * * [simplify]: Extracting #3: cost 25 inf + 1 7.723 * * [simplify]: Extracting #4: cost 20 inf + 227 7.723 * * [simplify]: Extracting #5: cost 6 inf + 2926 7.724 * * [simplify]: Extracting #6: cost 0 inf + 4717 7.725 * [simplify]: Simplified to (* (sqrt 2) (/ (sqrt (sqrt 2)) (+ (exp (- x)) (exp x)))) 7.725 * [simplify]: Simplified (2 2) to (λ (x) (* (sqrt (sqrt 2)) (* (sqrt 2) (/ (sqrt (sqrt 2)) (+ (exp (- x)) (exp x)))))) 7.725 * * * * [progress]: [ 54 / 60 ] simplifiying candidate # 7.725 * [simplify]: Simplifying (* (sqrt 2) (/ (sqrt 2) (+ (exp x) (exp (- x))))) 7.726 * * [simplify]: iters left: 6 (9 enodes) 7.728 * * [simplify]: iters left: 5 (33 enodes) 7.736 * * [simplify]: iters left: 4 (37 enodes) 7.742 * * [simplify]: iters left: 3 (39 enodes) 7.748 * * [simplify]: Extracting #0: cost 1 inf + 0 7.748 * * [simplify]: Extracting #1: cost 6 inf + 0 7.748 * * [simplify]: Extracting #2: cost 10 inf + 1 7.748 * * [simplify]: Extracting #3: cost 13 inf + 83 7.748 * * [simplify]: Extracting #4: cost 9 inf + 308 7.748 * * [simplify]: Extracting #5: cost 1 inf + 1799 7.748 * * [simplify]: Extracting #6: cost 0 inf + 2101 7.749 * [simplify]: Simplified to (/ 2 (+ (exp x) (exp (- x)))) 7.749 * [simplify]: Simplified (2 2) to (λ (x) (* 1 (/ 2 (+ (exp x) (exp (- x)))))) 7.749 * * * * [progress]: [ 55 / 60 ] simplifiying candidate # 7.749 * [simplify]: Simplifying (* (sqrt 2) (sqrt 2)) 7.749 * * [simplify]: iters left: 3 (3 enodes) 7.751 * * [simplify]: iters left: 2 (7 enodes) 7.752 * * [simplify]: Extracting #0: cost 1 inf + 0 7.752 * * [simplify]: Extracting #1: cost 0 inf + 1 7.752 * [simplify]: Simplified to 2 7.752 * [simplify]: Simplified (2 1) to (λ (x) (/ 2 (+ (exp x) (exp (- x))))) 7.752 * * * * [progress]: [ 56 / 60 ] simplifiying candidate #real (real->posit16 (* (sqrt 2) (/ (sqrt 2) (+ (exp x) (exp (- x))))))))> 7.753 * [simplify]: Simplifying (real->posit16 (* (sqrt 2) (/ (sqrt 2) (+ (exp x) (exp (- x)))))) 7.753 * * [simplify]: iters left: 6 (10 enodes) 7.755 * * [simplify]: iters left: 5 (33 enodes) 7.764 * * [simplify]: iters left: 4 (37 enodes) 7.775 * * [simplify]: iters left: 3 (39 enodes) 7.784 * * [simplify]: Extracting #0: cost 1 inf + 0 7.784 * * [simplify]: Extracting #1: cost 2 inf + 0 7.784 * * [simplify]: Extracting #2: cost 6 inf + 0 7.784 * * [simplify]: Extracting #3: cost 10 inf + 1 7.784 * * [simplify]: Extracting #4: cost 13 inf + 83 7.784 * * [simplify]: Extracting #5: cost 8 inf + 419 7.785 * * [simplify]: Extracting #6: cost 0 inf + 2101 7.785 * [simplify]: Simplified to (real->posit16 (/ 2 (+ (exp x) (exp (- x))))) 7.785 * [simplify]: Simplified (2 1) to (λ (x) (posit16->real (real->posit16 (/ 2 (+ (exp x) (exp (- x))))))) 7.785 * * * * [progress]: [ 57 / 60 ] simplifiying candidate # 7.785 * * * * [progress]: [ 58 / 60 ] simplifiying candidate # 7.785 * [simplify]: Simplifying (- (+ (* 1/2 (pow (sqrt 2) 2)) (* 5/48 (* (pow (sqrt 2) 2) (pow x 4)))) (* 1/4 (* (pow (sqrt 2) 2) (pow x 2)))) 7.785 * * [simplify]: iters left: 6 (17 enodes) 7.792 * * [simplify]: iters left: 5 (76 enodes) 7.822 * * [simplify]: iters left: 4 (144 enodes) 7.874 * * [simplify]: iters left: 3 (274 enodes) 7.976 * * [simplify]: Extracting #0: cost 1 inf + 0 7.977 * * [simplify]: Extracting #1: cost 14 inf + 0 7.977 * * [simplify]: Extracting #2: cost 73 inf + 1 7.981 * * [simplify]: Extracting #3: cost 92 inf + 136 7.983 * * [simplify]: Extracting #4: cost 46 inf + 3467 7.987 * * [simplify]: Extracting #5: cost 2 inf + 9257 7.992 * * [simplify]: Extracting #6: cost 0 inf + 9583 7.997 * [simplify]: Simplified to (+ (+ 1 (* (* (* x x) (* x x)) 5/24)) (* -1/2 (* x x))) 7.997 * [simplify]: Simplified (2) to (λ (x) (+ (+ 1 (* (* (* x x) (* x x)) 5/24)) (* -1/2 (* x x)))) 7.997 * * * * [progress]: [ 59 / 60 ] simplifiying candidate # 7.998 * [simplify]: Simplifying (/ (pow (sqrt 2) 2) (+ (exp x) (exp (- x)))) 7.998 * * [simplify]: iters left: 6 (9 enodes) 8.001 * * [simplify]: iters left: 5 (34 enodes) 8.007 * * [simplify]: iters left: 4 (44 enodes) 8.015 * * [simplify]: iters left: 3 (66 enodes) 8.028 * * [simplify]: iters left: 2 (104 enodes) 8.065 * * [simplify]: iters left: 1 (181 enodes) 8.121 * * [simplify]: Extracting #0: cost 1 inf + 0 8.121 * * [simplify]: Extracting #1: cost 4 inf + 0 8.121 * * [simplify]: Extracting #2: cost 6 inf + 1 8.121 * * [simplify]: Extracting #3: cost 11 inf + 1 8.121 * * [simplify]: Extracting #4: cost 7 inf + 186 8.121 * * [simplify]: Extracting #5: cost 3 inf + 670 8.122 * * [simplify]: Extracting #6: cost 0 inf + 1415 8.122 * [simplify]: Simplified to (/ 2 (+ (exp (- x)) (exp x))) 8.122 * [simplify]: Simplified (2) to (λ (x) (/ 2 (+ (exp (- x)) (exp x)))) 8.122 * * * * [progress]: [ 60 / 60 ] simplifiying candidate # 8.123 * [simplify]: Simplifying (/ (pow (sqrt 2) 2) (+ (exp (* -1 x)) (exp x))) 8.123 * * [simplify]: iters left: 6 (10 enodes) 8.129 * * [simplify]: iters left: 5 (40 enodes) 8.144 * * [simplify]: iters left: 4 (57 enodes) 8.156 * * [simplify]: iters left: 3 (88 enodes) 8.172 * * [simplify]: iters left: 2 (154 enodes) 8.226 * * [simplify]: iters left: 1 (293 enodes) 8.320 * * [simplify]: Extracting #0: cost 1 inf + 0 8.320 * * [simplify]: Extracting #1: cost 4 inf + 0 8.320 * * [simplify]: Extracting #2: cost 6 inf + 1 8.320 * * [simplify]: Extracting #3: cost 26 inf + 1 8.320 * * [simplify]: Extracting #4: cost 62 inf + 117 8.320 * * [simplify]: Extracting #5: cost 65 inf + 1513 8.322 * * [simplify]: Extracting #6: cost 24 inf + 12747 8.324 * * [simplify]: Extracting #7: cost 2 inf + 21298 8.326 * * [simplify]: Extracting #8: cost 0 inf + 22036 8.328 * [simplify]: Simplified to (/ 2 (+ (exp x) (exp (- x)))) 8.328 * [simplify]: Simplified (2) to (λ (x) (/ 2 (+ (exp x) (exp (- x))))) 8.329 * * * [progress]: adding candidates to table 8.820 * [progress]: [Phase 3 of 3] Extracting. 8.820 * * [regime]: Finding splitpoints for: (# #) 8.820 * * * [regime-changes]: Trying 3 branch expressions: (x (+ (exp x) (exp (- x))) (/ 2 (+ (exp x) (exp (- x))))) 8.820 * * * * [regimes]: Trying to branch on x from (# #) 8.846 * * * * [regimes]: Trying to branch on (+ (exp x) (exp (- x))) from (# #) 8.870 * * * * [regimes]: Trying to branch on (/ 2 (+ (exp x) (exp (- x)))) from (# #) 8.895 * * * [regime]: Found split indices: #