0.002 * [progress]: [Phase 1 of 3] Setting up.
0.002 * * * [progress]: [1/2] Preparing points
0.070 * * * [progress]: [2/2] Setting up program.
0.076 * [progress]: [Phase 2 of 3] Improving.
0.076 * * * * [progress]: [ 1 / 1 ] simplifiying candidate #<alt (λ (v) (* (* (/ (sqrt 2) 4) (sqrt (- 1 (* 3 (* v v))))) (- 1 (* v v))))>
0.076 * [simplify]: Simplifying (* (* (/ (sqrt 2) 4) (sqrt (- 1 (* 3 (* v v))))) (- 1 (* v v)))
0.076 * * [simplify]: iteration 1: (14 enodes)
0.107 * * [simplify]: iteration 2: (57 enodes)
0.130 * * [simplify]: iteration 3: (113 enodes)
0.165 * * [simplify]: iteration 4: (251 enodes)
0.247 * * [simplify]: iteration 5: (566 enodes)
0.576 * * [simplify]: iteration 6: (1058 enodes)
1.392 * * [simplify]: iteration 7: (1592 enodes)
2.824 * * [simplify]: Extracting #0: cost 1 inf + 0
2.825 * * [simplify]: Extracting #1: cost 70 inf + 0
2.827 * * [simplify]: Extracting #2: cost 255 inf + 128
2.833 * * [simplify]: Extracting #3: cost 227 inf + 7058
2.850 * * [simplify]: Extracting #4: cost 111 inf + 26649
2.890 * * [simplify]: Extracting #5: cost 13 inf + 49890
2.940 * * [simplify]: Extracting #6: cost 0 inf + 53291
2.984 * [simplify]: Simplified to (* (- (/ (sqrt 2) 4) (* (/ (sqrt 2) 4) (* v v))) (sqrt (fma (* v v) -3 1)))
2.996 * * [progress]: iteration 1 / 4
2.996 * * * [progress]: picking best candidate
3.005 * * * * [pick]: Picked  #<alt (λ (v) (* (- (/ (sqrt 2) 4) (* (/ (sqrt 2) 4) (* v v))) (sqrt (fma (* v v) -3 1))))>
3.005 * * * [progress]: localizing error
3.046 * * * [progress]: generating rewritten candidates
3.046 * * * * [progress]: [ 1 / 2 ] rewriting at (2 1 2)
3.080 * * * * [progress]: [ 2 / 2 ] rewriting at (2 1)
3.110 * * * [progress]: generating series expansions
3.110 * * * * [progress]: [ 1 / 2 ] generating series at (2 1 2)
3.111 * [backup-simplify]: Simplify (* (/ (sqrt 2) 4) (* v v)) into (* 1/4 (* (sqrt 2) (pow v 2)))
3.111 * [approximate]: Taking taylor expansion of (* 1/4 (* (sqrt 2) (pow v 2))) in (v) around 0
3.112 * [taylor]: Taking taylor expansion of (* 1/4 (* (sqrt 2) (pow v 2))) in v
3.112 * [taylor]: Taking taylor expansion of 1/4 in v
3.112 * [backup-simplify]: Simplify 1/4 into 1/4
3.112 * [taylor]: Taking taylor expansion of (* (sqrt 2) (pow v 2)) in v
3.112 * [taylor]: Taking taylor expansion of (sqrt 2) in v
3.112 * [taylor]: Taking taylor expansion of 2 in v
3.112 * [backup-simplify]: Simplify 2 into 2
3.112 * [backup-simplify]: Simplify (sqrt 2) into (sqrt 2)
3.113 * [backup-simplify]: Simplify (/ 0 (* 2 (sqrt 2))) into 0
3.113 * [taylor]: Taking taylor expansion of (pow v 2) in v
3.113 * [taylor]: Taking taylor expansion of v in v
3.113 * [backup-simplify]: Simplify 0 into 0
3.113 * [backup-simplify]: Simplify 1 into 1
3.113 * [taylor]: Taking taylor expansion of (* 1/4 (* (sqrt 2) (pow v 2))) in v
3.113 * [taylor]: Taking taylor expansion of 1/4 in v
3.113 * [backup-simplify]: Simplify 1/4 into 1/4
3.113 * [taylor]: Taking taylor expansion of (* (sqrt 2) (pow v 2)) in v
3.113 * [taylor]: Taking taylor expansion of (sqrt 2) in v
3.113 * [taylor]: Taking taylor expansion of 2 in v
3.113 * [backup-simplify]: Simplify 2 into 2
3.113 * [backup-simplify]: Simplify (sqrt 2) into (sqrt 2)
3.114 * [backup-simplify]: Simplify (/ 0 (* 2 (sqrt 2))) into 0
3.114 * [taylor]: Taking taylor expansion of (pow v 2) in v
3.114 * [taylor]: Taking taylor expansion of v in v
3.114 * [backup-simplify]: Simplify 0 into 0
3.114 * [backup-simplify]: Simplify 1 into 1
3.115 * [backup-simplify]: Simplify (* 1 1) into 1
3.115 * [backup-simplify]: Simplify (* (sqrt 2) 1) into (sqrt 2)
3.116 * [backup-simplify]: Simplify (* 1/4 (sqrt 2)) into (* 1/4 (sqrt 2))
3.117 * [backup-simplify]: Simplify (* 1/4 (sqrt 2)) into (* 1/4 (sqrt 2))
3.118 * [backup-simplify]: Simplify (+ (* 1 0) (* 0 1)) into 0
3.119 * [backup-simplify]: Simplify (+ (* (sqrt 2) 0) (* 0 1)) into 0
3.120 * [backup-simplify]: Simplify (+ (* 1/4 0) (* 0 (sqrt 2))) into 0
3.120 * [backup-simplify]: Simplify 0 into 0
3.121 * [backup-simplify]: Simplify (+ (* 1 0) (+ (* 0 0) (* 0 1))) into 0
3.122 * [backup-simplify]: Simplify (/ (- 0 (pow 0 2) (+)) (* 2 (sqrt 2))) into 0
3.123 * [backup-simplify]: Simplify (+ (* (sqrt 2) 0) (+ (* 0 0) (* 0 1))) into 0
3.124 * [backup-simplify]: Simplify (+ (* 1/4 0) (+ (* 0 0) (* 0 (sqrt 2)))) into 0
3.124 * [backup-simplify]: Simplify 0 into 0
3.125 * [backup-simplify]: Simplify (+ (* 1 0) (+ (* 0 0) (+ (* 0 0) (* 0 1)))) into 0
3.126 * [backup-simplify]: Simplify (/ (- 0 (+ (* 2 (* 0 0)))) (* 2 (sqrt 2))) into 0
3.127 * [backup-simplify]: Simplify (+ (* (sqrt 2) 0) (+ (* 0 0) (+ (* 0 0) (* 0 1)))) into 0
3.129 * [backup-simplify]: Simplify (+ (* 1/4 0) (+ (* 0 0) (+ (* 0 0) (* 0 (sqrt 2))))) into 0
3.129 * [backup-simplify]: Simplify 0 into 0
3.130 * [backup-simplify]: Simplify (+ (* 1 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (* 0 1))))) into 0
3.131 * [backup-simplify]: Simplify (/ (- 0 (pow 0 2) (+ (* 2 (* 0 0)))) (* 2 (sqrt 2))) into 0
3.133 * [backup-simplify]: Simplify (+ (* (sqrt 2) 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (* 0 1))))) into 0
3.134 * [backup-simplify]: Simplify (+ (* 1/4 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (* 0 (sqrt 2)))))) into 0
3.135 * [backup-simplify]: Simplify 0 into 0
3.136 * [backup-simplify]: Simplify (+ (* 1 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (* 0 1)))))) into 0
3.137 * [backup-simplify]: Simplify (/ (- 0 (+ (* 2 (* 0 0)) (* 2 (* 0 0)))) (* 2 (sqrt 2))) into 0
3.139 * [backup-simplify]: Simplify (+ (* (sqrt 2) 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (* 0 1)))))) into 0
3.140 * [backup-simplify]: Simplify (+ (* 1/4 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (* 0 (sqrt 2))))))) into 0
3.140 * [backup-simplify]: Simplify 0 into 0
3.142 * [backup-simplify]: Simplify (+ (* 1 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (* 0 1))))))) into 0
3.143 * [backup-simplify]: Simplify (/ (- 0 (pow 0 2) (+ (* 2 (* 0 0)) (* 2 (* 0 0)))) (* 2 (sqrt 2))) into 0
3.145 * [backup-simplify]: Simplify (+ (* (sqrt 2) 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (* 0 1))))))) into 0
3.147 * [backup-simplify]: Simplify (+ (* 1/4 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (* 0 (sqrt 2)))))))) into 0
3.147 * [backup-simplify]: Simplify 0 into 0
3.148 * [backup-simplify]: Simplify (* (* 1/4 (sqrt 2)) (pow v 2)) into (* 1/4 (* (sqrt 2) (pow v 2)))
3.149 * [backup-simplify]: Simplify (* (/ (sqrt 2) 4) (* (/ 1 v) (/ 1 v))) into (* 1/4 (/ (sqrt 2) (pow v 2)))
3.149 * [approximate]: Taking taylor expansion of (* 1/4 (/ (sqrt 2) (pow v 2))) in (v) around 0
3.149 * [taylor]: Taking taylor expansion of (* 1/4 (/ (sqrt 2) (pow v 2))) in v
3.149 * [taylor]: Taking taylor expansion of 1/4 in v
3.149 * [backup-simplify]: Simplify 1/4 into 1/4
3.149 * [taylor]: Taking taylor expansion of (/ (sqrt 2) (pow v 2)) in v
3.149 * [taylor]: Taking taylor expansion of (sqrt 2) in v
3.149 * [taylor]: Taking taylor expansion of 2 in v
3.149 * [backup-simplify]: Simplify 2 into 2
3.150 * [backup-simplify]: Simplify (sqrt 2) into (sqrt 2)
3.150 * [backup-simplify]: Simplify (/ 0 (* 2 (sqrt 2))) into 0
3.150 * [taylor]: Taking taylor expansion of (pow v 2) in v
3.150 * [taylor]: Taking taylor expansion of v in v
3.150 * [backup-simplify]: Simplify 0 into 0
3.150 * [backup-simplify]: Simplify 1 into 1
3.151 * [backup-simplify]: Simplify (* 1 1) into 1
3.152 * [backup-simplify]: Simplify (/ (sqrt 2) 1) into (sqrt 2)
3.152 * [taylor]: Taking taylor expansion of (* 1/4 (/ (sqrt 2) (pow v 2))) in v
3.152 * [taylor]: Taking taylor expansion of 1/4 in v
3.152 * [backup-simplify]: Simplify 1/4 into 1/4
3.152 * [taylor]: Taking taylor expansion of (/ (sqrt 2) (pow v 2)) in v
3.152 * [taylor]: Taking taylor expansion of (sqrt 2) in v
3.152 * [taylor]: Taking taylor expansion of 2 in v
3.152 * [backup-simplify]: Simplify 2 into 2
3.152 * [backup-simplify]: Simplify (sqrt 2) into (sqrt 2)
3.153 * [backup-simplify]: Simplify (/ 0 (* 2 (sqrt 2))) into 0
3.153 * [taylor]: Taking taylor expansion of (pow v 2) in v
3.153 * [taylor]: Taking taylor expansion of v in v
3.153 * [backup-simplify]: Simplify 0 into 0
3.153 * [backup-simplify]: Simplify 1 into 1
3.153 * [backup-simplify]: Simplify (* 1 1) into 1
3.154 * [backup-simplify]: Simplify (/ (sqrt 2) 1) into (sqrt 2)
3.155 * [backup-simplify]: Simplify (* 1/4 (sqrt 2)) into (* 1/4 (sqrt 2))
3.156 * [backup-simplify]: Simplify (* 1/4 (sqrt 2)) into (* 1/4 (sqrt 2))
3.157 * [backup-simplify]: Simplify (+ (* 1 0) (* 0 1)) into 0
3.158 * [backup-simplify]: Simplify (- (/ 0 1) (+ (* (sqrt 2) (/ 0 1)))) into 0
3.158 * [backup-simplify]: Simplify (+ (* 1/4 0) (* 0 (sqrt 2))) into 0
3.158 * [backup-simplify]: Simplify 0 into 0
3.159 * [backup-simplify]: Simplify (/ (- 0 (pow 0 2) (+)) (* 2 (sqrt 2))) into 0
3.160 * [backup-simplify]: Simplify (+ (* 1 0) (+ (* 0 0) (* 0 1))) into 0
3.161 * [backup-simplify]: Simplify (- (/ 0 1) (+ (* (sqrt 2) (/ 0 1)) (* 0 (/ 0 1)))) into 0
3.163 * [backup-simplify]: Simplify (+ (* 1/4 0) (+ (* 0 0) (* 0 (sqrt 2)))) into 0
3.163 * [backup-simplify]: Simplify 0 into 0
3.169 * [backup-simplify]: Simplify (/ (- 0 (+ (* 2 (* 0 0)))) (* 2 (sqrt 2))) into 0
3.170 * [backup-simplify]: Simplify (+ (* 1 0) (+ (* 0 0) (+ (* 0 0) (* 0 1)))) into 0
3.171 * [backup-simplify]: Simplify (- (/ 0 1) (+ (* (sqrt 2) (/ 0 1)) (* 0 (/ 0 1)) (* 0 (/ 0 1)))) into 0
3.172 * [backup-simplify]: Simplify (+ (* 1/4 0) (+ (* 0 0) (+ (* 0 0) (* 0 (sqrt 2))))) into 0
3.172 * [backup-simplify]: Simplify 0 into 0
3.174 * [backup-simplify]: Simplify (/ (- 0 (pow 0 2) (+ (* 2 (* 0 0)))) (* 2 (sqrt 2))) into 0
3.175 * [backup-simplify]: Simplify (+ (* 1 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (* 0 1))))) into 0
3.176 * [backup-simplify]: Simplify (- (/ 0 1) (+ (* (sqrt 2) (/ 0 1)) (* 0 (/ 0 1)) (* 0 (/ 0 1)) (* 0 (/ 0 1)))) into 0
3.178 * [backup-simplify]: Simplify (+ (* 1/4 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (* 0 (sqrt 2)))))) into 0
3.178 * [backup-simplify]: Simplify 0 into 0
3.179 * [backup-simplify]: Simplify (/ (- 0 (+ (* 2 (* 0 0)) (* 2 (* 0 0)))) (* 2 (sqrt 2))) into 0
3.181 * [backup-simplify]: Simplify (+ (* 1 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (* 0 1)))))) into 0
3.182 * [backup-simplify]: Simplify (- (/ 0 1) (+ (* (sqrt 2) (/ 0 1)) (* 0 (/ 0 1)) (* 0 (/ 0 1)) (* 0 (/ 0 1)) (* 0 (/ 0 1)))) into 0
3.184 * [backup-simplify]: Simplify (+ (* 1/4 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (* 0 (sqrt 2))))))) into 0
3.184 * [backup-simplify]: Simplify 0 into 0
3.185 * [backup-simplify]: Simplify (/ (- 0 (pow 0 2) (+ (* 2 (* 0 0)) (* 2 (* 0 0)))) (* 2 (sqrt 2))) into 0
3.187 * [backup-simplify]: Simplify (+ (* 1 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (* 0 1))))))) into 0
3.188 * [backup-simplify]: Simplify (- (/ 0 1) (+ (* (sqrt 2) (/ 0 1)) (* 0 (/ 0 1)) (* 0 (/ 0 1)) (* 0 (/ 0 1)) (* 0 (/ 0 1)) (* 0 (/ 0 1)))) into 0
3.190 * [backup-simplify]: Simplify (+ (* 1/4 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (* 0 (sqrt 2)))))))) into 0
3.190 * [backup-simplify]: Simplify 0 into 0
3.191 * [backup-simplify]: Simplify (* (* 1/4 (sqrt 2)) (pow (/ 1 (/ 1 v)) 2)) into (* 1/4 (* (sqrt 2) (pow v 2)))
3.193 * [backup-simplify]: Simplify (* (/ (sqrt 2) 4) (* (/ 1 (- v)) (/ 1 (- v)))) into (* 1/4 (/ (sqrt 2) (pow v 2)))
3.193 * [approximate]: Taking taylor expansion of (* 1/4 (/ (sqrt 2) (pow v 2))) in (v) around 0
3.193 * [taylor]: Taking taylor expansion of (* 1/4 (/ (sqrt 2) (pow v 2))) in v
3.193 * [taylor]: Taking taylor expansion of 1/4 in v
3.193 * [backup-simplify]: Simplify 1/4 into 1/4
3.193 * [taylor]: Taking taylor expansion of (/ (sqrt 2) (pow v 2)) in v
3.193 * [taylor]: Taking taylor expansion of (sqrt 2) in v
3.193 * [taylor]: Taking taylor expansion of 2 in v
3.193 * [backup-simplify]: Simplify 2 into 2
3.194 * [backup-simplify]: Simplify (sqrt 2) into (sqrt 2)
3.194 * [backup-simplify]: Simplify (/ 0 (* 2 (sqrt 2))) into 0
3.194 * [taylor]: Taking taylor expansion of (pow v 2) in v
3.194 * [taylor]: Taking taylor expansion of v in v
3.194 * [backup-simplify]: Simplify 0 into 0
3.194 * [backup-simplify]: Simplify 1 into 1
3.195 * [backup-simplify]: Simplify (* 1 1) into 1
3.196 * [backup-simplify]: Simplify (/ (sqrt 2) 1) into (sqrt 2)
3.196 * [taylor]: Taking taylor expansion of (* 1/4 (/ (sqrt 2) (pow v 2))) in v
3.196 * [taylor]: Taking taylor expansion of 1/4 in v
3.196 * [backup-simplify]: Simplify 1/4 into 1/4
3.196 * [taylor]: Taking taylor expansion of (/ (sqrt 2) (pow v 2)) in v
3.196 * [taylor]: Taking taylor expansion of (sqrt 2) in v
3.196 * [taylor]: Taking taylor expansion of 2 in v
3.196 * [backup-simplify]: Simplify 2 into 2
3.197 * [backup-simplify]: Simplify (sqrt 2) into (sqrt 2)
3.197 * [backup-simplify]: Simplify (/ 0 (* 2 (sqrt 2))) into 0
3.197 * [taylor]: Taking taylor expansion of (pow v 2) in v
3.197 * [taylor]: Taking taylor expansion of v in v
3.197 * [backup-simplify]: Simplify 0 into 0
3.197 * [backup-simplify]: Simplify 1 into 1
3.198 * [backup-simplify]: Simplify (* 1 1) into 1
3.199 * [backup-simplify]: Simplify (/ (sqrt 2) 1) into (sqrt 2)
3.200 * [backup-simplify]: Simplify (* 1/4 (sqrt 2)) into (* 1/4 (sqrt 2))
3.201 * [backup-simplify]: Simplify (* 1/4 (sqrt 2)) into (* 1/4 (sqrt 2))
3.201 * [backup-simplify]: Simplify (+ (* 1 0) (* 0 1)) into 0
3.202 * [backup-simplify]: Simplify (- (/ 0 1) (+ (* (sqrt 2) (/ 0 1)))) into 0
3.203 * [backup-simplify]: Simplify (+ (* 1/4 0) (* 0 (sqrt 2))) into 0
3.203 * [backup-simplify]: Simplify 0 into 0
3.204 * [backup-simplify]: Simplify (/ (- 0 (pow 0 2) (+)) (* 2 (sqrt 2))) into 0
3.205 * [backup-simplify]: Simplify (+ (* 1 0) (+ (* 0 0) (* 0 1))) into 0
3.206 * [backup-simplify]: Simplify (- (/ 0 1) (+ (* (sqrt 2) (/ 0 1)) (* 0 (/ 0 1)))) into 0
3.207 * [backup-simplify]: Simplify (+ (* 1/4 0) (+ (* 0 0) (* 0 (sqrt 2)))) into 0
3.207 * [backup-simplify]: Simplify 0 into 0
3.208 * [backup-simplify]: Simplify (/ (- 0 (+ (* 2 (* 0 0)))) (* 2 (sqrt 2))) into 0
3.209 * [backup-simplify]: Simplify (+ (* 1 0) (+ (* 0 0) (+ (* 0 0) (* 0 1)))) into 0
3.210 * [backup-simplify]: Simplify (- (/ 0 1) (+ (* (sqrt 2) (/ 0 1)) (* 0 (/ 0 1)) (* 0 (/ 0 1)))) into 0
3.211 * [backup-simplify]: Simplify (+ (* 1/4 0) (+ (* 0 0) (+ (* 0 0) (* 0 (sqrt 2))))) into 0
3.211 * [backup-simplify]: Simplify 0 into 0
3.213 * [backup-simplify]: Simplify (/ (- 0 (pow 0 2) (+ (* 2 (* 0 0)))) (* 2 (sqrt 2))) into 0
3.214 * [backup-simplify]: Simplify (+ (* 1 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (* 0 1))))) into 0
3.215 * [backup-simplify]: Simplify (- (/ 0 1) (+ (* (sqrt 2) (/ 0 1)) (* 0 (/ 0 1)) (* 0 (/ 0 1)) (* 0 (/ 0 1)))) into 0
3.216 * [backup-simplify]: Simplify (+ (* 1/4 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (* 0 (sqrt 2)))))) into 0
3.216 * [backup-simplify]: Simplify 0 into 0
3.218 * [backup-simplify]: Simplify (/ (- 0 (+ (* 2 (* 0 0)) (* 2 (* 0 0)))) (* 2 (sqrt 2))) into 0
3.219 * [backup-simplify]: Simplify (+ (* 1 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (* 0 1)))))) into 0
3.220 * [backup-simplify]: Simplify (- (/ 0 1) (+ (* (sqrt 2) (/ 0 1)) (* 0 (/ 0 1)) (* 0 (/ 0 1)) (* 0 (/ 0 1)) (* 0 (/ 0 1)))) into 0
3.222 * [backup-simplify]: Simplify (+ (* 1/4 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (* 0 (sqrt 2))))))) into 0
3.222 * [backup-simplify]: Simplify 0 into 0
3.223 * [backup-simplify]: Simplify (/ (- 0 (pow 0 2) (+ (* 2 (* 0 0)) (* 2 (* 0 0)))) (* 2 (sqrt 2))) into 0
3.225 * [backup-simplify]: Simplify (+ (* 1 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (* 0 1))))))) into 0
3.226 * [backup-simplify]: Simplify (- (/ 0 1) (+ (* (sqrt 2) (/ 0 1)) (* 0 (/ 0 1)) (* 0 (/ 0 1)) (* 0 (/ 0 1)) (* 0 (/ 0 1)) (* 0 (/ 0 1)))) into 0
3.228 * [backup-simplify]: Simplify (+ (* 1/4 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (* 0 (sqrt 2)))))))) into 0
3.228 * [backup-simplify]: Simplify 0 into 0
3.229 * [backup-simplify]: Simplify (* (* 1/4 (sqrt 2)) (pow (/ 1 (/ 1 (- v))) 2)) into (* 1/4 (* (sqrt 2) (pow v 2)))
3.229 * * * * [progress]: [ 2 / 2 ] generating series at (2 1)
3.231 * [backup-simplify]: Simplify (- (/ (sqrt 2) 4) (* (/ (sqrt 2) 4) (* v v))) into (- (* 1/4 (sqrt 2)) (* 1/4 (* (sqrt 2) (pow v 2))))
3.231 * [approximate]: Taking taylor expansion of (- (* 1/4 (sqrt 2)) (* 1/4 (* (sqrt 2) (pow v 2)))) in (v) around 0
3.231 * [taylor]: Taking taylor expansion of (- (* 1/4 (sqrt 2)) (* 1/4 (* (sqrt 2) (pow v 2)))) in v
3.231 * [taylor]: Taking taylor expansion of (* 1/4 (sqrt 2)) in v
3.231 * [taylor]: Taking taylor expansion of 1/4 in v
3.231 * [backup-simplify]: Simplify 1/4 into 1/4
3.231 * [taylor]: Taking taylor expansion of (sqrt 2) in v
3.231 * [taylor]: Taking taylor expansion of 2 in v
3.231 * [backup-simplify]: Simplify 2 into 2
3.232 * [backup-simplify]: Simplify (sqrt 2) into (sqrt 2)
3.232 * [backup-simplify]: Simplify (/ 0 (* 2 (sqrt 2))) into 0
3.232 * [taylor]: Taking taylor expansion of (* 1/4 (* (sqrt 2) (pow v 2))) in v
3.232 * [taylor]: Taking taylor expansion of 1/4 in v
3.232 * [backup-simplify]: Simplify 1/4 into 1/4
3.232 * [taylor]: Taking taylor expansion of (* (sqrt 2) (pow v 2)) in v
3.232 * [taylor]: Taking taylor expansion of (sqrt 2) in v
3.232 * [taylor]: Taking taylor expansion of 2 in v
3.232 * [backup-simplify]: Simplify 2 into 2
3.233 * [backup-simplify]: Simplify (sqrt 2) into (sqrt 2)
3.233 * [backup-simplify]: Simplify (/ 0 (* 2 (sqrt 2))) into 0
3.234 * [taylor]: Taking taylor expansion of (pow v 2) in v
3.234 * [taylor]: Taking taylor expansion of v in v
3.234 * [backup-simplify]: Simplify 0 into 0
3.234 * [backup-simplify]: Simplify 1 into 1
3.234 * [taylor]: Taking taylor expansion of (- (* 1/4 (sqrt 2)) (* 1/4 (* (sqrt 2) (pow v 2)))) in v
3.234 * [taylor]: Taking taylor expansion of (* 1/4 (sqrt 2)) in v
3.234 * [taylor]: Taking taylor expansion of 1/4 in v
3.234 * [backup-simplify]: Simplify 1/4 into 1/4
3.234 * [taylor]: Taking taylor expansion of (sqrt 2) in v
3.234 * [taylor]: Taking taylor expansion of 2 in v
3.234 * [backup-simplify]: Simplify 2 into 2
3.234 * [backup-simplify]: Simplify (sqrt 2) into (sqrt 2)
3.235 * [backup-simplify]: Simplify (/ 0 (* 2 (sqrt 2))) into 0
3.235 * [taylor]: Taking taylor expansion of (* 1/4 (* (sqrt 2) (pow v 2))) in v
3.235 * [taylor]: Taking taylor expansion of 1/4 in v
3.235 * [backup-simplify]: Simplify 1/4 into 1/4
3.235 * [taylor]: Taking taylor expansion of (* (sqrt 2) (pow v 2)) in v
3.235 * [taylor]: Taking taylor expansion of (sqrt 2) in v
3.235 * [taylor]: Taking taylor expansion of 2 in v
3.235 * [backup-simplify]: Simplify 2 into 2
3.235 * [backup-simplify]: Simplify (sqrt 2) into (sqrt 2)
3.236 * [backup-simplify]: Simplify (/ 0 (* 2 (sqrt 2))) into 0
3.236 * [taylor]: Taking taylor expansion of (pow v 2) in v
3.236 * [taylor]: Taking taylor expansion of v in v
3.236 * [backup-simplify]: Simplify 0 into 0
3.236 * [backup-simplify]: Simplify 1 into 1
3.237 * [backup-simplify]: Simplify (* 1/4 (sqrt 2)) into (* 1/4 (sqrt 2))
3.239 * [backup-simplify]: Simplify (+ (* 1/4 (sqrt 2)) 0) into (* 1/4 (sqrt 2))
3.240 * [backup-simplify]: Simplify (* 1/4 (sqrt 2)) into (* 1/4 (sqrt 2))
3.241 * [backup-simplify]: Simplify (+ (* 1/4 0) (* 0 (sqrt 2))) into 0
3.241 * [backup-simplify]: Simplify (+ 0 0) into 0
3.241 * [backup-simplify]: Simplify 0 into 0
3.242 * [backup-simplify]: Simplify (/ (- 0 (pow 0 2) (+)) (* 2 (sqrt 2))) into 0
3.243 * [backup-simplify]: Simplify (+ (* 1/4 0) (+ (* 0 0) (* 0 (sqrt 2)))) into 0
3.243 * [backup-simplify]: Simplify (* 1 1) into 1
3.244 * [backup-simplify]: Simplify (* (sqrt 2) 1) into (sqrt 2)
3.245 * [backup-simplify]: Simplify (* 1/4 (sqrt 2)) into (* 1/4 (sqrt 2))
3.247 * [backup-simplify]: Simplify (- (* 1/4 (sqrt 2))) into (- (* 1/4 (sqrt 2)))
3.249 * [backup-simplify]: Simplify (+ 0 (- (* 1/4 (sqrt 2)))) into (- (* 1/4 (sqrt 2)))
3.251 * [backup-simplify]: Simplify (- (* 1/4 (sqrt 2))) into (- (* 1/4 (sqrt 2)))
3.252 * [backup-simplify]: Simplify (/ (- 0 (+ (* 2 (* 0 0)))) (* 2 (sqrt 2))) into 0
3.254 * [backup-simplify]: Simplify (+ (* 1/4 0) (+ (* 0 0) (+ (* 0 0) (* 0 (sqrt 2))))) into 0
3.254 * [backup-simplify]: Simplify (+ (* 1 0) (* 0 1)) into 0
3.255 * [backup-simplify]: Simplify (+ (* (sqrt 2) 0) (* 0 1)) into 0
3.256 * [backup-simplify]: Simplify (+ (* 1/4 0) (* 0 (sqrt 2))) into 0
3.256 * [backup-simplify]: Simplify (- 0) into 0
3.257 * [backup-simplify]: Simplify (+ 0 0) into 0
3.257 * [backup-simplify]: Simplify 0 into 0
3.258 * [backup-simplify]: Simplify (/ (- 0 (pow 0 2) (+ (* 2 (* 0 0)))) (* 2 (sqrt 2))) into 0
3.260 * [backup-simplify]: Simplify (+ (* 1/4 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (* 0 (sqrt 2)))))) into 0
3.261 * [backup-simplify]: Simplify (+ (* 1 0) (+ (* 0 0) (* 0 1))) into 0
3.262 * [backup-simplify]: Simplify (/ (- 0 (pow 0 2) (+)) (* 2 (sqrt 2))) into 0
3.263 * [backup-simplify]: Simplify (+ (* (sqrt 2) 0) (+ (* 0 0) (* 0 1))) into 0
3.264 * [backup-simplify]: Simplify (+ (* 1/4 0) (+ (* 0 0) (* 0 (sqrt 2)))) into 0
3.264 * [backup-simplify]: Simplify (- 0) into 0
3.265 * [backup-simplify]: Simplify (+ 0 0) into 0
3.265 * [backup-simplify]: Simplify 0 into 0
3.266 * [backup-simplify]: Simplify (/ (- 0 (+ (* 2 (* 0 0)) (* 2 (* 0 0)))) (* 2 (sqrt 2))) into 0
3.268 * [backup-simplify]: Simplify (+ (* 1/4 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (* 0 (sqrt 2))))))) into 0
3.269 * [backup-simplify]: Simplify (+ (* 1 0) (+ (* 0 0) (+ (* 0 0) (* 0 1)))) into 0
3.270 * [backup-simplify]: Simplify (/ (- 0 (+ (* 2 (* 0 0)))) (* 2 (sqrt 2))) into 0
3.271 * [backup-simplify]: Simplify (+ (* (sqrt 2) 0) (+ (* 0 0) (+ (* 0 0) (* 0 1)))) into 0
3.272 * [backup-simplify]: Simplify (+ (* 1/4 0) (+ (* 0 0) (+ (* 0 0) (* 0 (sqrt 2))))) into 0
3.273 * [backup-simplify]: Simplify (- 0) into 0
3.273 * [backup-simplify]: Simplify (+ 0 0) into 0
3.273 * [backup-simplify]: Simplify 0 into 0
3.275 * [backup-simplify]: Simplify (/ (- 0 (pow 0 2) (+ (* 2 (* 0 0)) (* 2 (* 0 0)))) (* 2 (sqrt 2))) into 0
3.277 * [backup-simplify]: Simplify (+ (* 1/4 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (* 0 (sqrt 2)))))))) into 0
3.278 * [backup-simplify]: Simplify (+ (* 1 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (* 0 1))))) into 0
3.280 * [backup-simplify]: Simplify (/ (- 0 (pow 0 2) (+ (* 2 (* 0 0)))) (* 2 (sqrt 2))) into 0
3.281 * [backup-simplify]: Simplify (+ (* (sqrt 2) 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (* 0 1))))) into 0
3.283 * [backup-simplify]: Simplify (+ (* 1/4 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (* 0 (sqrt 2)))))) into 0
3.283 * [backup-simplify]: Simplify (- 0) into 0
3.283 * [backup-simplify]: Simplify (+ 0 0) into 0
3.284 * [backup-simplify]: Simplify 0 into 0
3.285 * [backup-simplify]: Simplify (/ (- 0 (+ (* 2 (* 0 0)) (* 2 (* 0 0)) (* 2 (* 0 0)))) (* 2 (sqrt 2))) into 0
3.287 * [backup-simplify]: Simplify (+ (* 1/4 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (* 0 (sqrt 2))))))))) into 0
3.288 * [backup-simplify]: Simplify (+ (* 1 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (* 0 1)))))) into 0
3.289 * [backup-simplify]: Simplify (/ (- 0 (+ (* 2 (* 0 0)) (* 2 (* 0 0)))) (* 2 (sqrt 2))) into 0
3.291 * [backup-simplify]: Simplify (+ (* (sqrt 2) 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (* 0 1)))))) into 0
3.293 * [backup-simplify]: Simplify (+ (* 1/4 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (* 0 (sqrt 2))))))) into 0
3.293 * [backup-simplify]: Simplify (- 0) into 0
3.293 * [backup-simplify]: Simplify (+ 0 0) into 0
3.293 * [backup-simplify]: Simplify 0 into 0
3.295 * [backup-simplify]: Simplify (/ (- 0 (pow 0 2) (+ (* 2 (* 0 0)) (* 2 (* 0 0)) (* 2 (* 0 0)))) (* 2 (sqrt 2))) into 0
3.297 * [backup-simplify]: Simplify (+ (* 1/4 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (* 0 (sqrt 2)))))))))) into 0
3.299 * [backup-simplify]: Simplify (+ (* 1 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (* 0 1))))))) into 0
3.300 * [backup-simplify]: Simplify (/ (- 0 (pow 0 2) (+ (* 2 (* 0 0)) (* 2 (* 0 0)))) (* 2 (sqrt 2))) into 0
3.302 * [backup-simplify]: Simplify (+ (* (sqrt 2) 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (* 0 1))))))) into 0
3.304 * [backup-simplify]: Simplify (+ (* 1/4 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (* 0 (sqrt 2)))))))) into 0
3.304 * [backup-simplify]: Simplify (- 0) into 0
3.305 * [backup-simplify]: Simplify (+ 0 0) into 0
3.305 * [backup-simplify]: Simplify 0 into 0
3.307 * [backup-simplify]: Simplify (+ (* (- (* 1/4 (sqrt 2))) (pow v 2)) (* 1/4 (sqrt 2))) into (- (* 1/4 (sqrt 2)) (* 1/4 (* (sqrt 2) (pow v 2))))
3.309 * [backup-simplify]: Simplify (- (/ (sqrt 2) 4) (* (/ (sqrt 2) 4) (* (/ 1 v) (/ 1 v)))) into (- (* 1/4 (sqrt 2)) (* 1/4 (/ (sqrt 2) (pow v 2))))
3.309 * [approximate]: Taking taylor expansion of (- (* 1/4 (sqrt 2)) (* 1/4 (/ (sqrt 2) (pow v 2)))) in (v) around 0
3.309 * [taylor]: Taking taylor expansion of (- (* 1/4 (sqrt 2)) (* 1/4 (/ (sqrt 2) (pow v 2)))) in v
3.309 * [taylor]: Taking taylor expansion of (* 1/4 (sqrt 2)) in v
3.309 * [taylor]: Taking taylor expansion of 1/4 in v
3.309 * [backup-simplify]: Simplify 1/4 into 1/4
3.309 * [taylor]: Taking taylor expansion of (sqrt 2) in v
3.309 * [taylor]: Taking taylor expansion of 2 in v
3.309 * [backup-simplify]: Simplify 2 into 2
3.310 * [backup-simplify]: Simplify (sqrt 2) into (sqrt 2)
3.310 * [backup-simplify]: Simplify (/ 0 (* 2 (sqrt 2))) into 0
3.310 * [taylor]: Taking taylor expansion of (* 1/4 (/ (sqrt 2) (pow v 2))) in v
3.310 * [taylor]: Taking taylor expansion of 1/4 in v
3.310 * [backup-simplify]: Simplify 1/4 into 1/4
3.310 * [taylor]: Taking taylor expansion of (/ (sqrt 2) (pow v 2)) in v
3.310 * [taylor]: Taking taylor expansion of (sqrt 2) in v
3.310 * [taylor]: Taking taylor expansion of 2 in v
3.310 * [backup-simplify]: Simplify 2 into 2
3.311 * [backup-simplify]: Simplify (sqrt 2) into (sqrt 2)
3.317 * [backup-simplify]: Simplify (/ 0 (* 2 (sqrt 2))) into 0
3.317 * [taylor]: Taking taylor expansion of (pow v 2) in v
3.317 * [taylor]: Taking taylor expansion of v in v
3.317 * [backup-simplify]: Simplify 0 into 0
3.317 * [backup-simplify]: Simplify 1 into 1
3.318 * [backup-simplify]: Simplify (* 1 1) into 1
3.319 * [backup-simplify]: Simplify (/ (sqrt 2) 1) into (sqrt 2)
3.319 * [taylor]: Taking taylor expansion of (- (* 1/4 (sqrt 2)) (* 1/4 (/ (sqrt 2) (pow v 2)))) in v
3.319 * [taylor]: Taking taylor expansion of (* 1/4 (sqrt 2)) in v
3.319 * [taylor]: Taking taylor expansion of 1/4 in v
3.319 * [backup-simplify]: Simplify 1/4 into 1/4
3.319 * [taylor]: Taking taylor expansion of (sqrt 2) in v
3.319 * [taylor]: Taking taylor expansion of 2 in v
3.319 * [backup-simplify]: Simplify 2 into 2
3.320 * [backup-simplify]: Simplify (sqrt 2) into (sqrt 2)
3.320 * [backup-simplify]: Simplify (/ 0 (* 2 (sqrt 2))) into 0
3.320 * [taylor]: Taking taylor expansion of (* 1/4 (/ (sqrt 2) (pow v 2))) in v
3.321 * [taylor]: Taking taylor expansion of 1/4 in v
3.321 * [backup-simplify]: Simplify 1/4 into 1/4
3.321 * [taylor]: Taking taylor expansion of (/ (sqrt 2) (pow v 2)) in v
3.321 * [taylor]: Taking taylor expansion of (sqrt 2) in v
3.321 * [taylor]: Taking taylor expansion of 2 in v
3.321 * [backup-simplify]: Simplify 2 into 2
3.321 * [backup-simplify]: Simplify (sqrt 2) into (sqrt 2)
3.322 * [backup-simplify]: Simplify (/ 0 (* 2 (sqrt 2))) into 0
3.322 * [taylor]: Taking taylor expansion of (pow v 2) in v
3.322 * [taylor]: Taking taylor expansion of v in v
3.322 * [backup-simplify]: Simplify 0 into 0
3.322 * [backup-simplify]: Simplify 1 into 1
3.322 * [backup-simplify]: Simplify (* 1 1) into 1
3.323 * [backup-simplify]: Simplify (/ (sqrt 2) 1) into (sqrt 2)
3.324 * [backup-simplify]: Simplify (* 1/4 (sqrt 2)) into (* 1/4 (sqrt 2))
3.326 * [backup-simplify]: Simplify (- (* 1/4 (sqrt 2))) into (- (* 1/4 (sqrt 2)))
3.328 * [backup-simplify]: Simplify (+ 0 (- (* 1/4 (sqrt 2)))) into (- (* 1/4 (sqrt 2)))
3.330 * [backup-simplify]: Simplify (- (* 1/4 (sqrt 2))) into (- (* 1/4 (sqrt 2)))
3.331 * [backup-simplify]: Simplify (+ (* 1 0) (* 0 1)) into 0
3.332 * [backup-simplify]: Simplify (- (/ 0 1) (+ (* (sqrt 2) (/ 0 1)))) into 0
3.333 * [backup-simplify]: Simplify (+ (* 1/4 0) (* 0 (sqrt 2))) into 0
3.333 * [backup-simplify]: Simplify (- 0) into 0
3.334 * [backup-simplify]: Simplify (+ 0 0) into 0
3.334 * [backup-simplify]: Simplify 0 into 0
3.335 * [backup-simplify]: Simplify (* 1/4 (sqrt 2)) into (* 1/4 (sqrt 2))
3.335 * [backup-simplify]: Simplify (/ (- 0 (pow 0 2) (+)) (* 2 (sqrt 2))) into 0
3.336 * [backup-simplify]: Simplify (+ (* 1 0) (+ (* 0 0) (* 0 1))) into 0
3.336 * [backup-simplify]: Simplify (- (/ 0 1) (+ (* (sqrt 2) (/ 0 1)) (* 0 (/ 0 1)))) into 0
3.337 * [backup-simplify]: Simplify (+ (* 1/4 0) (+ (* 0 0) (* 0 (sqrt 2)))) into 0
3.337 * [backup-simplify]: Simplify (- 0) into 0
3.338 * [backup-simplify]: Simplify (+ (* 1/4 (sqrt 2)) 0) into (* 1/4 (sqrt 2))
3.339 * [backup-simplify]: Simplify (* 1/4 (sqrt 2)) into (* 1/4 (sqrt 2))
3.339 * [backup-simplify]: Simplify (+ (* 1/4 0) (* 0 (sqrt 2))) into 0
3.340 * [backup-simplify]: Simplify (/ (- 0 (+ (* 2 (* 0 0)))) (* 2 (sqrt 2))) into 0
3.341 * [backup-simplify]: Simplify (+ (* 1 0) (+ (* 0 0) (+ (* 0 0) (* 0 1)))) into 0
3.341 * [backup-simplify]: Simplify (- (/ 0 1) (+ (* (sqrt 2) (/ 0 1)) (* 0 (/ 0 1)) (* 0 (/ 0 1)))) into 0
3.342 * [backup-simplify]: Simplify (+ (* 1/4 0) (+ (* 0 0) (+ (* 0 0) (* 0 (sqrt 2))))) into 0
3.342 * [backup-simplify]: Simplify (- 0) into 0
3.342 * [backup-simplify]: Simplify (+ 0 0) into 0
3.342 * [backup-simplify]: Simplify 0 into 0
3.343 * [backup-simplify]: Simplify (/ (- 0 (pow 0 2) (+)) (* 2 (sqrt 2))) into 0
3.344 * [backup-simplify]: Simplify (+ (* 1/4 0) (+ (* 0 0) (* 0 (sqrt 2)))) into 0
3.345 * [backup-simplify]: Simplify (/ (- 0 (pow 0 2) (+ (* 2 (* 0 0)))) (* 2 (sqrt 2))) into 0
3.345 * [backup-simplify]: Simplify (+ (* 1 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (* 0 1))))) into 0
3.346 * [backup-simplify]: Simplify (- (/ 0 1) (+ (* (sqrt 2) (/ 0 1)) (* 0 (/ 0 1)) (* 0 (/ 0 1)) (* 0 (/ 0 1)))) into 0
3.347 * [backup-simplify]: Simplify (+ (* 1/4 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (* 0 (sqrt 2)))))) into 0
3.347 * [backup-simplify]: Simplify (- 0) into 0
3.347 * [backup-simplify]: Simplify (+ 0 0) into 0
3.347 * [backup-simplify]: Simplify 0 into 0
3.348 * [backup-simplify]: Simplify (/ (- 0 (+ (* 2 (* 0 0)))) (* 2 (sqrt 2))) into 0
3.349 * [backup-simplify]: Simplify (+ (* 1/4 0) (+ (* 0 0) (+ (* 0 0) (* 0 (sqrt 2))))) into 0
3.349 * [backup-simplify]: Simplify (/ (- 0 (+ (* 2 (* 0 0)) (* 2 (* 0 0)))) (* 2 (sqrt 2))) into 0
3.350 * [backup-simplify]: Simplify (+ (* 1 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (* 0 1)))))) into 0
3.351 * [backup-simplify]: Simplify (- (/ 0 1) (+ (* (sqrt 2) (/ 0 1)) (* 0 (/ 0 1)) (* 0 (/ 0 1)) (* 0 (/ 0 1)) (* 0 (/ 0 1)))) into 0
3.352 * [backup-simplify]: Simplify (+ (* 1/4 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (* 0 (sqrt 2))))))) into 0
3.352 * [backup-simplify]: Simplify (- 0) into 0
3.352 * [backup-simplify]: Simplify (+ 0 0) into 0
3.352 * [backup-simplify]: Simplify 0 into 0
3.353 * [backup-simplify]: Simplify (/ (- 0 (pow 0 2) (+ (* 2 (* 0 0)))) (* 2 (sqrt 2))) into 0
3.354 * [backup-simplify]: Simplify (+ (* 1/4 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (* 0 (sqrt 2)))))) into 0
3.355 * [backup-simplify]: Simplify (/ (- 0 (pow 0 2) (+ (* 2 (* 0 0)) (* 2 (* 0 0)))) (* 2 (sqrt 2))) into 0
3.355 * [backup-simplify]: Simplify (+ (* 1 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (* 0 1))))))) into 0
3.356 * [backup-simplify]: Simplify (- (/ 0 1) (+ (* (sqrt 2) (/ 0 1)) (* 0 (/ 0 1)) (* 0 (/ 0 1)) (* 0 (/ 0 1)) (* 0 (/ 0 1)) (* 0 (/ 0 1)))) into 0
3.357 * [backup-simplify]: Simplify (+ (* 1/4 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (* 0 (sqrt 2)))))))) into 0
3.357 * [backup-simplify]: Simplify (- 0) into 0
3.358 * [backup-simplify]: Simplify (+ 0 0) into 0
3.358 * [backup-simplify]: Simplify 0 into 0
3.358 * [backup-simplify]: Simplify (/ (- 0 (+ (* 2 (* 0 0)) (* 2 (* 0 0)))) (* 2 (sqrt 2))) into 0
3.359 * [backup-simplify]: Simplify (+ (* 1/4 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (* 0 (sqrt 2))))))) into 0
3.360 * [backup-simplify]: Simplify (/ (- 0 (+ (* 2 (* 0 0)) (* 2 (* 0 0)) (* 2 (* 0 0)))) (* 2 (sqrt 2))) into 0
3.361 * [backup-simplify]: Simplify (+ (* 1 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (* 0 1)))))))) into 0
3.362 * [backup-simplify]: Simplify (- (/ 0 1) (+ (* (sqrt 2) (/ 0 1)) (* 0 (/ 0 1)) (* 0 (/ 0 1)) (* 0 (/ 0 1)) (* 0 (/ 0 1)) (* 0 (/ 0 1)) (* 0 (/ 0 1)))) into 0
3.363 * [backup-simplify]: Simplify (+ (* 1/4 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (* 0 (sqrt 2))))))))) into 0
3.363 * [backup-simplify]: Simplify (- 0) into 0
3.364 * [backup-simplify]: Simplify (+ 0 0) into 0
3.364 * [backup-simplify]: Simplify 0 into 0
3.365 * [backup-simplify]: Simplify (/ (- 0 (pow 0 2) (+ (* 2 (* 0 0)) (* 2 (* 0 0)))) (* 2 (sqrt 2))) into 0
3.367 * [backup-simplify]: Simplify (+ (* 1/4 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (* 0 (sqrt 2)))))))) into 0
3.368 * [backup-simplify]: Simplify (/ (- 0 (pow 0 2) (+ (* 2 (* 0 0)) (* 2 (* 0 0)) (* 2 (* 0 0)))) (* 2 (sqrt 2))) into 0
3.370 * [backup-simplify]: Simplify (+ (* 1 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (* 0 1))))))))) into 0
3.372 * [backup-simplify]: Simplify (- (/ 0 1) (+ (* (sqrt 2) (/ 0 1)) (* 0 (/ 0 1)) (* 0 (/ 0 1)) (* 0 (/ 0 1)) (* 0 (/ 0 1)) (* 0 (/ 0 1)) (* 0 (/ 0 1)) (* 0 (/ 0 1)))) into 0
3.374 * [backup-simplify]: Simplify (+ (* 1/4 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (* 0 (sqrt 2)))))))))) into 0
3.374 * [backup-simplify]: Simplify (- 0) into 0
3.374 * [backup-simplify]: Simplify (+ 0 0) into 0
3.375 * [backup-simplify]: Simplify 0 into 0
3.377 * [backup-simplify]: Simplify (+ (* 1/4 (sqrt 2)) (* (- (* 1/4 (sqrt 2))) (pow (/ 1 (/ 1 v)) 2))) into (- (* 1/4 (sqrt 2)) (* 1/4 (* (sqrt 2) (pow v 2))))
3.378 * [backup-simplify]: Simplify (- (/ (sqrt 2) 4) (* (/ (sqrt 2) 4) (* (/ 1 (- v)) (/ 1 (- v))))) into (- (* 1/4 (sqrt 2)) (* 1/4 (/ (sqrt 2) (pow v 2))))
3.379 * [approximate]: Taking taylor expansion of (- (* 1/4 (sqrt 2)) (* 1/4 (/ (sqrt 2) (pow v 2)))) in (v) around 0
3.379 * [taylor]: Taking taylor expansion of (- (* 1/4 (sqrt 2)) (* 1/4 (/ (sqrt 2) (pow v 2)))) in v
3.379 * [taylor]: Taking taylor expansion of (* 1/4 (sqrt 2)) in v
3.379 * [taylor]: Taking taylor expansion of 1/4 in v
3.379 * [backup-simplify]: Simplify 1/4 into 1/4
3.379 * [taylor]: Taking taylor expansion of (sqrt 2) in v
3.379 * [taylor]: Taking taylor expansion of 2 in v
3.379 * [backup-simplify]: Simplify 2 into 2
3.379 * [backup-simplify]: Simplify (sqrt 2) into (sqrt 2)
3.380 * [backup-simplify]: Simplify (/ 0 (* 2 (sqrt 2))) into 0
3.380 * [taylor]: Taking taylor expansion of (* 1/4 (/ (sqrt 2) (pow v 2))) in v
3.380 * [taylor]: Taking taylor expansion of 1/4 in v
3.380 * [backup-simplify]: Simplify 1/4 into 1/4
3.380 * [taylor]: Taking taylor expansion of (/ (sqrt 2) (pow v 2)) in v
3.380 * [taylor]: Taking taylor expansion of (sqrt 2) in v
3.380 * [taylor]: Taking taylor expansion of 2 in v
3.380 * [backup-simplify]: Simplify 2 into 2
3.380 * [backup-simplify]: Simplify (sqrt 2) into (sqrt 2)
3.381 * [backup-simplify]: Simplify (/ 0 (* 2 (sqrt 2))) into 0
3.381 * [taylor]: Taking taylor expansion of (pow v 2) in v
3.381 * [taylor]: Taking taylor expansion of v in v
3.381 * [backup-simplify]: Simplify 0 into 0
3.381 * [backup-simplify]: Simplify 1 into 1
3.381 * [backup-simplify]: Simplify (* 1 1) into 1
3.382 * [backup-simplify]: Simplify (/ (sqrt 2) 1) into (sqrt 2)
3.382 * [taylor]: Taking taylor expansion of (- (* 1/4 (sqrt 2)) (* 1/4 (/ (sqrt 2) (pow v 2)))) in v
3.382 * [taylor]: Taking taylor expansion of (* 1/4 (sqrt 2)) in v
3.382 * [taylor]: Taking taylor expansion of 1/4 in v
3.382 * [backup-simplify]: Simplify 1/4 into 1/4
3.382 * [taylor]: Taking taylor expansion of (sqrt 2) in v
3.382 * [taylor]: Taking taylor expansion of 2 in v
3.382 * [backup-simplify]: Simplify 2 into 2
3.382 * [backup-simplify]: Simplify (sqrt 2) into (sqrt 2)
3.383 * [backup-simplify]: Simplify (/ 0 (* 2 (sqrt 2))) into 0
3.383 * [taylor]: Taking taylor expansion of (* 1/4 (/ (sqrt 2) (pow v 2))) in v
3.383 * [taylor]: Taking taylor expansion of 1/4 in v
3.383 * [backup-simplify]: Simplify 1/4 into 1/4
3.383 * [taylor]: Taking taylor expansion of (/ (sqrt 2) (pow v 2)) in v
3.383 * [taylor]: Taking taylor expansion of (sqrt 2) in v
3.383 * [taylor]: Taking taylor expansion of 2 in v
3.383 * [backup-simplify]: Simplify 2 into 2
3.384 * [backup-simplify]: Simplify (sqrt 2) into (sqrt 2)
3.384 * [backup-simplify]: Simplify (/ 0 (* 2 (sqrt 2))) into 0
3.384 * [taylor]: Taking taylor expansion of (pow v 2) in v
3.384 * [taylor]: Taking taylor expansion of v in v
3.384 * [backup-simplify]: Simplify 0 into 0
3.384 * [backup-simplify]: Simplify 1 into 1
3.385 * [backup-simplify]: Simplify (* 1 1) into 1
3.385 * [backup-simplify]: Simplify (/ (sqrt 2) 1) into (sqrt 2)
3.386 * [backup-simplify]: Simplify (* 1/4 (sqrt 2)) into (* 1/4 (sqrt 2))
3.388 * [backup-simplify]: Simplify (- (* 1/4 (sqrt 2))) into (- (* 1/4 (sqrt 2)))
3.390 * [backup-simplify]: Simplify (+ 0 (- (* 1/4 (sqrt 2)))) into (- (* 1/4 (sqrt 2)))
3.392 * [backup-simplify]: Simplify (- (* 1/4 (sqrt 2))) into (- (* 1/4 (sqrt 2)))
3.392 * [backup-simplify]: Simplify (+ (* 1 0) (* 0 1)) into 0
3.393 * [backup-simplify]: Simplify (- (/ 0 1) (+ (* (sqrt 2) (/ 0 1)))) into 0
3.394 * [backup-simplify]: Simplify (+ (* 1/4 0) (* 0 (sqrt 2))) into 0
3.395 * [backup-simplify]: Simplify (- 0) into 0
3.395 * [backup-simplify]: Simplify (+ 0 0) into 0
3.395 * [backup-simplify]: Simplify 0 into 0
3.396 * [backup-simplify]: Simplify (* 1/4 (sqrt 2)) into (* 1/4 (sqrt 2))
3.397 * [backup-simplify]: Simplify (/ (- 0 (pow 0 2) (+)) (* 2 (sqrt 2))) into 0
3.398 * [backup-simplify]: Simplify (+ (* 1 0) (+ (* 0 0) (* 0 1))) into 0
3.399 * [backup-simplify]: Simplify (- (/ 0 1) (+ (* (sqrt 2) (/ 0 1)) (* 0 (/ 0 1)))) into 0
3.400 * [backup-simplify]: Simplify (+ (* 1/4 0) (+ (* 0 0) (* 0 (sqrt 2)))) into 0
3.401 * [backup-simplify]: Simplify (- 0) into 0
3.402 * [backup-simplify]: Simplify (+ (* 1/4 (sqrt 2)) 0) into (* 1/4 (sqrt 2))
3.403 * [backup-simplify]: Simplify (* 1/4 (sqrt 2)) into (* 1/4 (sqrt 2))
3.404 * [backup-simplify]: Simplify (+ (* 1/4 0) (* 0 (sqrt 2))) into 0
3.405 * [backup-simplify]: Simplify (/ (- 0 (+ (* 2 (* 0 0)))) (* 2 (sqrt 2))) into 0
3.406 * [backup-simplify]: Simplify (+ (* 1 0) (+ (* 0 0) (+ (* 0 0) (* 0 1)))) into 0
3.407 * [backup-simplify]: Simplify (- (/ 0 1) (+ (* (sqrt 2) (/ 0 1)) (* 0 (/ 0 1)) (* 0 (/ 0 1)))) into 0
3.409 * [backup-simplify]: Simplify (+ (* 1/4 0) (+ (* 0 0) (+ (* 0 0) (* 0 (sqrt 2))))) into 0
3.409 * [backup-simplify]: Simplify (- 0) into 0
3.409 * [backup-simplify]: Simplify (+ 0 0) into 0
3.409 * [backup-simplify]: Simplify 0 into 0
3.410 * [backup-simplify]: Simplify (/ (- 0 (pow 0 2) (+)) (* 2 (sqrt 2))) into 0
3.411 * [backup-simplify]: Simplify (+ (* 1/4 0) (+ (* 0 0) (* 0 (sqrt 2)))) into 0
3.413 * [backup-simplify]: Simplify (/ (- 0 (pow 0 2) (+ (* 2 (* 0 0)))) (* 2 (sqrt 2))) into 0
3.414 * [backup-simplify]: Simplify (+ (* 1 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (* 0 1))))) into 0
3.415 * [backup-simplify]: Simplify (- (/ 0 1) (+ (* (sqrt 2) (/ 0 1)) (* 0 (/ 0 1)) (* 0 (/ 0 1)) (* 0 (/ 0 1)))) into 0
3.416 * [backup-simplify]: Simplify (+ (* 1/4 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (* 0 (sqrt 2)))))) into 0
3.416 * [backup-simplify]: Simplify (- 0) into 0
3.416 * [backup-simplify]: Simplify (+ 0 0) into 0
3.416 * [backup-simplify]: Simplify 0 into 0
3.417 * [backup-simplify]: Simplify (/ (- 0 (+ (* 2 (* 0 0)))) (* 2 (sqrt 2))) into 0
3.417 * [backup-simplify]: Simplify (+ (* 1/4 0) (+ (* 0 0) (+ (* 0 0) (* 0 (sqrt 2))))) into 0
3.418 * [backup-simplify]: Simplify (/ (- 0 (+ (* 2 (* 0 0)) (* 2 (* 0 0)))) (* 2 (sqrt 2))) into 0
3.419 * [backup-simplify]: Simplify (+ (* 1 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (* 0 1)))))) into 0
3.420 * [backup-simplify]: Simplify (- (/ 0 1) (+ (* (sqrt 2) (/ 0 1)) (* 0 (/ 0 1)) (* 0 (/ 0 1)) (* 0 (/ 0 1)) (* 0 (/ 0 1)))) into 0
3.420 * [backup-simplify]: Simplify (+ (* 1/4 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (* 0 (sqrt 2))))))) into 0
3.421 * [backup-simplify]: Simplify (- 0) into 0
3.421 * [backup-simplify]: Simplify (+ 0 0) into 0
3.421 * [backup-simplify]: Simplify 0 into 0
3.422 * [backup-simplify]: Simplify (/ (- 0 (pow 0 2) (+ (* 2 (* 0 0)))) (* 2 (sqrt 2))) into 0
3.422 * [backup-simplify]: Simplify (+ (* 1/4 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (* 0 (sqrt 2)))))) into 0
3.423 * [backup-simplify]: Simplify (/ (- 0 (pow 0 2) (+ (* 2 (* 0 0)) (* 2 (* 0 0)))) (* 2 (sqrt 2))) into 0
3.424 * [backup-simplify]: Simplify (+ (* 1 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (* 0 1))))))) into 0
3.425 * [backup-simplify]: Simplify (- (/ 0 1) (+ (* (sqrt 2) (/ 0 1)) (* 0 (/ 0 1)) (* 0 (/ 0 1)) (* 0 (/ 0 1)) (* 0 (/ 0 1)) (* 0 (/ 0 1)))) into 0
3.426 * [backup-simplify]: Simplify (+ (* 1/4 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (* 0 (sqrt 2)))))))) into 0
3.426 * [backup-simplify]: Simplify (- 0) into 0
3.431 * [backup-simplify]: Simplify (+ 0 0) into 0
3.431 * [backup-simplify]: Simplify 0 into 0
3.432 * [backup-simplify]: Simplify (/ (- 0 (+ (* 2 (* 0 0)) (* 2 (* 0 0)))) (* 2 (sqrt 2))) into 0
3.433 * [backup-simplify]: Simplify (+ (* 1/4 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (* 0 (sqrt 2))))))) into 0
3.433 * [backup-simplify]: Simplify (/ (- 0 (+ (* 2 (* 0 0)) (* 2 (* 0 0)) (* 2 (* 0 0)))) (* 2 (sqrt 2))) into 0
3.434 * [backup-simplify]: Simplify (+ (* 1 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (* 0 1)))))))) into 0
3.435 * [backup-simplify]: Simplify (- (/ 0 1) (+ (* (sqrt 2) (/ 0 1)) (* 0 (/ 0 1)) (* 0 (/ 0 1)) (* 0 (/ 0 1)) (* 0 (/ 0 1)) (* 0 (/ 0 1)) (* 0 (/ 0 1)))) into 0
3.436 * [backup-simplify]: Simplify (+ (* 1/4 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (* 0 (sqrt 2))))))))) into 0
3.437 * [backup-simplify]: Simplify (- 0) into 0
3.437 * [backup-simplify]: Simplify (+ 0 0) into 0
3.437 * [backup-simplify]: Simplify 0 into 0
3.438 * [backup-simplify]: Simplify (/ (- 0 (pow 0 2) (+ (* 2 (* 0 0)) (* 2 (* 0 0)))) (* 2 (sqrt 2))) into 0
3.439 * [backup-simplify]: Simplify (+ (* 1/4 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (* 0 (sqrt 2)))))))) into 0
3.439 * [backup-simplify]: Simplify (/ (- 0 (pow 0 2) (+ (* 2 (* 0 0)) (* 2 (* 0 0)) (* 2 (* 0 0)))) (* 2 (sqrt 2))) into 0
3.441 * [backup-simplify]: Simplify (+ (* 1 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (* 0 1))))))))) into 0
3.441 * [backup-simplify]: Simplify (- (/ 0 1) (+ (* (sqrt 2) (/ 0 1)) (* 0 (/ 0 1)) (* 0 (/ 0 1)) (* 0 (/ 0 1)) (* 0 (/ 0 1)) (* 0 (/ 0 1)) (* 0 (/ 0 1)) (* 0 (/ 0 1)))) into 0
3.443 * [backup-simplify]: Simplify (+ (* 1/4 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (* 0 (sqrt 2)))))))))) into 0
3.444 * [backup-simplify]: Simplify (- 0) into 0
3.444 * [backup-simplify]: Simplify (+ 0 0) into 0
3.444 * [backup-simplify]: Simplify 0 into 0
3.447 * [backup-simplify]: Simplify (+ (* 1/4 (sqrt 2)) (* (- (* 1/4 (sqrt 2))) (pow (/ 1 (/ 1 (- v))) 2))) into (- (* 1/4 (sqrt 2)) (* 1/4 (* (sqrt 2) (pow v 2))))
3.448 * * * [progress]: simplifying candidates
3.448 * * * * [progress]: [ 1 / 115 ] simplifiying candidate #<alt (λ (v) (* (- (/ (sqrt 2) 4) (log1p (expm1 (* (/ (sqrt 2) 4) (* v v))))) (sqrt (fma (* v v) -3 1))))>
3.448 * * * * [progress]: [ 2 / 115 ] simplifiying candidate #<alt (λ (v) (* (- (/ (sqrt 2) 4) (expm1 (log1p (* (/ (sqrt 2) 4) (* v v))))) (sqrt (fma (* v v) -3 1))))>
3.448 * * * * [progress]: [ 3 / 115 ] simplifiying candidate #<alt (λ (v) (* (- (/ (sqrt 2) 4) (pow (* (/ (sqrt 2) 4) (* v v)) 1)) (sqrt (fma (* v v) -3 1))))>
3.448 * * * * [progress]: [ 4 / 115 ] simplifiying candidate #<alt (λ (v) (* (- (/ (sqrt 2) 4) (pow (* (/ (sqrt 2) 4) (* v v)) 1)) (sqrt (fma (* v v) -3 1))))>
3.448 * * * * [progress]: [ 5 / 115 ] simplifiying candidate #<alt (λ (v) (* (- (/ (sqrt 2) 4) (pow (* (/ (sqrt 2) 4) (* v v)) 1)) (sqrt (fma (* v v) -3 1))))>
3.448 * * * * [progress]: [ 6 / 115 ] simplifiying candidate #<alt (λ (v) (* (- (/ (sqrt 2) 4) (exp (+ (- (log (sqrt 2)) (log 4)) (+ (log v) (log v))))) (sqrt (fma (* v v) -3 1))))>
3.448 * * * * [progress]: [ 7 / 115 ] simplifiying candidate #<alt (λ (v) (* (- (/ (sqrt 2) 4) (exp (+ (- (log (sqrt 2)) (log 4)) (log (* v v))))) (sqrt (fma (* v v) -3 1))))>
3.448 * * * * [progress]: [ 8 / 115 ] simplifiying candidate #<alt (λ (v) (* (- (/ (sqrt 2) 4) (exp (+ (log (/ (sqrt 2) 4)) (+ (log v) (log v))))) (sqrt (fma (* v v) -3 1))))>
3.448 * * * * [progress]: [ 9 / 115 ] simplifiying candidate #<alt (λ (v) (* (- (/ (sqrt 2) 4) (exp (+ (log (/ (sqrt 2) 4)) (log (* v v))))) (sqrt (fma (* v v) -3 1))))>
3.448 * * * * [progress]: [ 10 / 115 ] simplifiying candidate #<alt (λ (v) (* (- (/ (sqrt 2) 4) (exp (log (* (/ (sqrt 2) 4) (* v v))))) (sqrt (fma (* v v) -3 1))))>
3.448 * * * * [progress]: [ 11 / 115 ] simplifiying candidate #<alt (λ (v) (* (- (/ (sqrt 2) 4) (log (exp (* (/ (sqrt 2) 4) (* v v))))) (sqrt (fma (* v v) -3 1))))>
3.448 * * * * [progress]: [ 12 / 115 ] simplifiying candidate #<alt (λ (v) (* (- (/ (sqrt 2) 4) (cbrt (* (/ (* (* (sqrt 2) (sqrt 2)) (sqrt 2)) (* (* 4 4) 4)) (* (* (* v v) v) (* (* v v) v))))) (sqrt (fma (* v v) -3 1))))>
3.448 * * * * [progress]: [ 13 / 115 ] simplifiying candidate #<alt (λ (v) (* (- (/ (sqrt 2) 4) (cbrt (* (/ (* (* (sqrt 2) (sqrt 2)) (sqrt 2)) (* (* 4 4) 4)) (* (* (* v v) (* v v)) (* v v))))) (sqrt (fma (* v v) -3 1))))>
3.449 * * * * [progress]: [ 14 / 115 ] simplifiying candidate #<alt (λ (v) (* (- (/ (sqrt 2) 4) (cbrt (* (* (* (/ (sqrt 2) 4) (/ (sqrt 2) 4)) (/ (sqrt 2) 4)) (* (* (* v v) v) (* (* v v) v))))) (sqrt (fma (* v v) -3 1))))>
3.449 * * * * [progress]: [ 15 / 115 ] simplifiying candidate #<alt (λ (v) (* (- (/ (sqrt 2) 4) (cbrt (* (* (* (/ (sqrt 2) 4) (/ (sqrt 2) 4)) (/ (sqrt 2) 4)) (* (* (* v v) (* v v)) (* v v))))) (sqrt (fma (* v v) -3 1))))>
3.449 * * * * [progress]: [ 16 / 115 ] simplifiying candidate #<alt (λ (v) (* (- (/ (sqrt 2) 4) (* (* (cbrt (* (/ (sqrt 2) 4) (* v v))) (cbrt (* (/ (sqrt 2) 4) (* v v)))) (cbrt (* (/ (sqrt 2) 4) (* v v))))) (sqrt (fma (* v v) -3 1))))>
3.449 * * * * [progress]: [ 17 / 115 ] simplifiying candidate #<alt (λ (v) (* (- (/ (sqrt 2) 4) (cbrt (* (* (* (/ (sqrt 2) 4) (* v v)) (* (/ (sqrt 2) 4) (* v v))) (* (/ (sqrt 2) 4) (* v v))))) (sqrt (fma (* v v) -3 1))))>
3.449 * * * * [progress]: [ 18 / 115 ] simplifiying candidate #<alt (λ (v) (* (- (/ (sqrt 2) 4) (* (sqrt (* (/ (sqrt 2) 4) (* v v))) (sqrt (* (/ (sqrt 2) 4) (* v v))))) (sqrt (fma (* v v) -3 1))))>
3.449 * * * * [progress]: [ 19 / 115 ] simplifiying candidate #<alt (λ (v) (* (- (/ (sqrt 2) 4) (* 1 (* (/ (sqrt 2) 4) (* v v)))) (sqrt (fma (* v v) -3 1))))>
3.449 * * * * [progress]: [ 20 / 115 ] simplifiying candidate #<alt (λ (v) (* (- (/ (sqrt 2) 4) (* (* (sqrt (/ (sqrt 2) 4)) v) (* (sqrt (/ (sqrt 2) 4)) v))) (sqrt (fma (* v v) -3 1))))>
3.449 * * * * [progress]: [ 21 / 115 ] simplifiying candidate #<alt (λ (v) (* (- (/ (sqrt 2) 4) (* (* (/ (sqrt (sqrt 2)) (sqrt 4)) v) (* (/ (sqrt (sqrt 2)) (sqrt 4)) v))) (sqrt (fma (* v v) -3 1))))>
3.449 * * * * [progress]: [ 22 / 115 ] simplifiying candidate #<alt (λ (v) (* (- (/ (sqrt 2) 4) (* (* (/ (sqrt (sqrt 2)) (sqrt 4)) v) (* (/ (sqrt (sqrt 2)) (sqrt 4)) v))) (sqrt (fma (* v v) -3 1))))>
3.449 * * * * [progress]: [ 23 / 115 ] simplifiying candidate #<alt (λ (v) (* (- (/ (sqrt 2) 4) (* (* (/ (sqrt 2) 4) v) v)) (sqrt (fma (* v v) -3 1))))>
3.449 * * * * [progress]: [ 24 / 115 ] simplifiying candidate #<alt (λ (v) (* (- (/ (sqrt 2) 4) (* (* (cbrt (/ (sqrt 2) 4)) (cbrt (/ (sqrt 2) 4))) (* (cbrt (/ (sqrt 2) 4)) (* v v)))) (sqrt (fma (* v v) -3 1))))>
3.449 * * * * [progress]: [ 25 / 115 ] simplifiying candidate #<alt (λ (v) (* (- (/ (sqrt 2) 4) (* (sqrt (/ (sqrt 2) 4)) (* (sqrt (/ (sqrt 2) 4)) (* v v)))) (sqrt (fma (* v v) -3 1))))>
3.449 * * * * [progress]: [ 26 / 115 ] simplifiying candidate #<alt (λ (v) (* (- (/ (sqrt 2) 4) (* (/ (* (cbrt (sqrt 2)) (cbrt (sqrt 2))) (* (cbrt 4) (cbrt 4))) (* (/ (cbrt (sqrt 2)) (cbrt 4)) (* v v)))) (sqrt (fma (* v v) -3 1))))>
3.449 * * * * [progress]: [ 27 / 115 ] simplifiying candidate #<alt (λ (v) (* (- (/ (sqrt 2) 4) (* (/ (* (cbrt (sqrt 2)) (cbrt (sqrt 2))) (sqrt 4)) (* (/ (cbrt (sqrt 2)) (sqrt 4)) (* v v)))) (sqrt (fma (* v v) -3 1))))>
3.449 * * * * [progress]: [ 28 / 115 ] simplifiying candidate #<alt (λ (v) (* (- (/ (sqrt 2) 4) (* (/ (* (cbrt (sqrt 2)) (cbrt (sqrt 2))) 1) (* (/ (cbrt (sqrt 2)) 4) (* v v)))) (sqrt (fma (* v v) -3 1))))>
3.449 * * * * [progress]: [ 29 / 115 ] simplifiying candidate #<alt (λ (v) (* (- (/ (sqrt 2) 4) (* (/ (sqrt (* (cbrt 2) (cbrt 2))) (* (cbrt 4) (cbrt 4))) (* (/ (sqrt (cbrt 2)) (cbrt 4)) (* v v)))) (sqrt (fma (* v v) -3 1))))>
3.450 * * * * [progress]: [ 30 / 115 ] simplifiying candidate #<alt (λ (v) (* (- (/ (sqrt 2) 4) (* (/ (sqrt (* (cbrt 2) (cbrt 2))) (sqrt 4)) (* (/ (sqrt (cbrt 2)) (sqrt 4)) (* v v)))) (sqrt (fma (* v v) -3 1))))>
3.450 * * * * [progress]: [ 31 / 115 ] simplifiying candidate #<alt (λ (v) (* (- (/ (sqrt 2) 4) (* (/ (sqrt (* (cbrt 2) (cbrt 2))) 1) (* (/ (sqrt (cbrt 2)) 4) (* v v)))) (sqrt (fma (* v v) -3 1))))>
3.450 * * * * [progress]: [ 32 / 115 ] simplifiying candidate #<alt (λ (v) (* (- (/ (sqrt 2) 4) (* (/ (sqrt (sqrt 2)) (* (cbrt 4) (cbrt 4))) (* (/ (sqrt (sqrt 2)) (cbrt 4)) (* v v)))) (sqrt (fma (* v v) -3 1))))>
3.450 * * * * [progress]: [ 33 / 115 ] simplifiying candidate #<alt (λ (v) (* (- (/ (sqrt 2) 4) (* (/ (sqrt (sqrt 2)) (sqrt 4)) (* (/ (sqrt (sqrt 2)) (sqrt 4)) (* v v)))) (sqrt (fma (* v v) -3 1))))>
3.450 * * * * [progress]: [ 34 / 115 ] simplifiying candidate #<alt (λ (v) (* (- (/ (sqrt 2) 4) (* (/ (sqrt (sqrt 2)) 1) (* (/ (sqrt (sqrt 2)) 4) (* v v)))) (sqrt (fma (* v v) -3 1))))>
3.450 * * * * [progress]: [ 35 / 115 ] simplifiying candidate #<alt (λ (v) (* (- (/ (sqrt 2) 4) (* (/ (sqrt 1) (* (cbrt 4) (cbrt 4))) (* (/ (sqrt 2) (cbrt 4)) (* v v)))) (sqrt (fma (* v v) -3 1))))>
3.450 * * * * [progress]: [ 36 / 115 ] simplifiying candidate #<alt (λ (v) (* (- (/ (sqrt 2) 4) (* (/ (sqrt 1) (sqrt 4)) (* (/ (sqrt 2) (sqrt 4)) (* v v)))) (sqrt (fma (* v v) -3 1))))>
3.450 * * * * [progress]: [ 37 / 115 ] simplifiying candidate #<alt (λ (v) (* (- (/ (sqrt 2) 4) (* (/ (sqrt 1) 1) (* (/ (sqrt 2) 4) (* v v)))) (sqrt (fma (* v v) -3 1))))>
3.450 * * * * [progress]: [ 38 / 115 ] simplifiying candidate #<alt (λ (v) (* (- (/ (sqrt 2) 4) (* (/ (sqrt (sqrt 2)) (* (cbrt 4) (cbrt 4))) (* (/ (sqrt (sqrt 2)) (cbrt 4)) (* v v)))) (sqrt (fma (* v v) -3 1))))>
3.450 * * * * [progress]: [ 39 / 115 ] simplifiying candidate #<alt (λ (v) (* (- (/ (sqrt 2) 4) (* (/ (sqrt (sqrt 2)) (sqrt 4)) (* (/ (sqrt (sqrt 2)) (sqrt 4)) (* v v)))) (sqrt (fma (* v v) -3 1))))>
3.450 * * * * [progress]: [ 40 / 115 ] simplifiying candidate #<alt (λ (v) (* (- (/ (sqrt 2) 4) (* (/ (sqrt (sqrt 2)) 1) (* (/ (sqrt (sqrt 2)) 4) (* v v)))) (sqrt (fma (* v v) -3 1))))>
3.450 * * * * [progress]: [ 41 / 115 ] simplifiying candidate #<alt (λ (v) (* (- (/ (sqrt 2) 4) (* (/ 1 (* (cbrt 4) (cbrt 4))) (* (/ (sqrt 2) (cbrt 4)) (* v v)))) (sqrt (fma (* v v) -3 1))))>
3.450 * * * * [progress]: [ 42 / 115 ] simplifiying candidate #<alt (λ (v) (* (- (/ (sqrt 2) 4) (* (/ 1 (sqrt 4)) (* (/ (sqrt 2) (sqrt 4)) (* v v)))) (sqrt (fma (* v v) -3 1))))>
3.450 * * * * [progress]: [ 43 / 115 ] simplifiying candidate #<alt (λ (v) (* (- (/ (sqrt 2) 4) (* (/ 1 1) (* (/ (sqrt 2) 4) (* v v)))) (sqrt (fma (* v v) -3 1))))>
3.450 * * * * [progress]: [ 44 / 115 ] simplifiying candidate #<alt (λ (v) (* (- (/ (sqrt 2) 4) (* 1 (* (/ (sqrt 2) 4) (* v v)))) (sqrt (fma (* v v) -3 1))))>
3.451 * * * * [progress]: [ 45 / 115 ] simplifiying candidate #<alt (λ (v) (* (- (/ (sqrt 2) 4) (* (sqrt 2) (* (/ 1 4) (* v v)))) (sqrt (fma (* v v) -3 1))))>
3.451 * * * * [progress]: [ 46 / 115 ] simplifiying candidate #<alt (λ (v) (* (- (/ (sqrt 2) 4) (/ (* (sqrt 2) (* v v)) 4)) (sqrt (fma (* v v) -3 1))))>
3.451 * * * * [progress]: [ 47 / 115 ] simplifiying candidate #<alt (λ (v) (* (- (/ (sqrt 2) 4) (posit16->real (real->posit16 (* (/ (sqrt 2) 4) (* v v))))) (sqrt (fma (* v v) -3 1))))>
3.451 * * * * [progress]: [ 48 / 115 ] simplifiying candidate #<alt (λ (v) (* (- (/ (sqrt 2) 4) (* (* v v) (/ (sqrt 2) 4))) (sqrt (fma (* v v) -3 1))))>
3.451 * * * * [progress]: [ 49 / 115 ] simplifiying candidate #<alt (λ (v) (* (+ (fma (* (cbrt (/ (sqrt 2) 4)) (cbrt (/ (sqrt 2) 4))) (cbrt (/ (sqrt 2) 4)) (- (* (* v v) (/ (sqrt 2) 4)))) (fma (- (* v v)) (/ (sqrt 2) 4) (* (* v v) (/ (sqrt 2) 4)))) (sqrt (fma (* v v) -3 1))))>
3.451 * * * * [progress]: [ 50 / 115 ] simplifiying candidate #<alt (λ (v) (* (+ (fma (sqrt (/ (sqrt 2) 4)) (sqrt (/ (sqrt 2) 4)) (- (* (* v v) (/ (sqrt 2) 4)))) (fma (- (* v v)) (/ (sqrt 2) 4) (* (* v v) (/ (sqrt 2) 4)))) (sqrt (fma (* v v) -3 1))))>
3.451 * * * * [progress]: [ 51 / 115 ] simplifiying candidate #<alt (λ (v) (* (+ (fma (/ (* (cbrt (sqrt 2)) (cbrt (sqrt 2))) (* (cbrt 4) (cbrt 4))) (/ (cbrt (sqrt 2)) (cbrt 4)) (- (* (* v v) (/ (sqrt 2) 4)))) (fma (- (* v v)) (/ (sqrt 2) 4) (* (* v v) (/ (sqrt 2) 4)))) (sqrt (fma (* v v) -3 1))))>
3.451 * * * * [progress]: [ 52 / 115 ] simplifiying candidate #<alt (λ (v) (* (+ (fma (/ (* (cbrt (sqrt 2)) (cbrt (sqrt 2))) (sqrt 4)) (/ (cbrt (sqrt 2)) (sqrt 4)) (- (* (* v v) (/ (sqrt 2) 4)))) (fma (- (* v v)) (/ (sqrt 2) 4) (* (* v v) (/ (sqrt 2) 4)))) (sqrt (fma (* v v) -3 1))))>
3.451 * * * * [progress]: [ 53 / 115 ] simplifiying candidate #<alt (λ (v) (* (+ (fma (/ (* (cbrt (sqrt 2)) (cbrt (sqrt 2))) 1) (/ (cbrt (sqrt 2)) 4) (- (* (* v v) (/ (sqrt 2) 4)))) (fma (- (* v v)) (/ (sqrt 2) 4) (* (* v v) (/ (sqrt 2) 4)))) (sqrt (fma (* v v) -3 1))))>
3.451 * * * * [progress]: [ 54 / 115 ] simplifiying candidate #<alt (λ (v) (* (+ (fma (/ (sqrt (* (cbrt 2) (cbrt 2))) (* (cbrt 4) (cbrt 4))) (/ (sqrt (cbrt 2)) (cbrt 4)) (- (* (* v v) (/ (sqrt 2) 4)))) (fma (- (* v v)) (/ (sqrt 2) 4) (* (* v v) (/ (sqrt 2) 4)))) (sqrt (fma (* v v) -3 1))))>
3.451 * * * * [progress]: [ 55 / 115 ] simplifiying candidate #<alt (λ (v) (* (+ (fma (/ (sqrt (* (cbrt 2) (cbrt 2))) (sqrt 4)) (/ (sqrt (cbrt 2)) (sqrt 4)) (- (* (* v v) (/ (sqrt 2) 4)))) (fma (- (* v v)) (/ (sqrt 2) 4) (* (* v v) (/ (sqrt 2) 4)))) (sqrt (fma (* v v) -3 1))))>
3.451 * * * * [progress]: [ 56 / 115 ] simplifiying candidate #<alt (λ (v) (* (+ (fma (/ (sqrt (* (cbrt 2) (cbrt 2))) 1) (/ (sqrt (cbrt 2)) 4) (- (* (* v v) (/ (sqrt 2) 4)))) (fma (- (* v v)) (/ (sqrt 2) 4) (* (* v v) (/ (sqrt 2) 4)))) (sqrt (fma (* v v) -3 1))))>
3.451 * * * * [progress]: [ 57 / 115 ] simplifiying candidate #<alt (λ (v) (* (+ (fma (/ (sqrt (sqrt 2)) (* (cbrt 4) (cbrt 4))) (/ (sqrt (sqrt 2)) (cbrt 4)) (- (* (* v v) (/ (sqrt 2) 4)))) (fma (- (* v v)) (/ (sqrt 2) 4) (* (* v v) (/ (sqrt 2) 4)))) (sqrt (fma (* v v) -3 1))))>
3.451 * * * * [progress]: [ 58 / 115 ] simplifiying candidate #<alt (λ (v) (* (+ (fma (/ (sqrt (sqrt 2)) (sqrt 4)) (/ (sqrt (sqrt 2)) (sqrt 4)) (- (* (* v v) (/ (sqrt 2) 4)))) (fma (- (* v v)) (/ (sqrt 2) 4) (* (* v v) (/ (sqrt 2) 4)))) (sqrt (fma (* v v) -3 1))))>
3.452 * * * * [progress]: [ 59 / 115 ] simplifiying candidate #<alt (λ (v) (* (+ (fma (/ (sqrt (sqrt 2)) 1) (/ (sqrt (sqrt 2)) 4) (- (* (* v v) (/ (sqrt 2) 4)))) (fma (- (* v v)) (/ (sqrt 2) 4) (* (* v v) (/ (sqrt 2) 4)))) (sqrt (fma (* v v) -3 1))))>
3.452 * * * * [progress]: [ 60 / 115 ] simplifiying candidate #<alt (λ (v) (* (+ (fma (/ (sqrt 1) (* (cbrt 4) (cbrt 4))) (/ (sqrt 2) (cbrt 4)) (- (* (* v v) (/ (sqrt 2) 4)))) (fma (- (* v v)) (/ (sqrt 2) 4) (* (* v v) (/ (sqrt 2) 4)))) (sqrt (fma (* v v) -3 1))))>
3.452 * * * * [progress]: [ 61 / 115 ] simplifiying candidate #<alt (λ (v) (* (+ (fma (/ (sqrt 1) (sqrt 4)) (/ (sqrt 2) (sqrt 4)) (- (* (* v v) (/ (sqrt 2) 4)))) (fma (- (* v v)) (/ (sqrt 2) 4) (* (* v v) (/ (sqrt 2) 4)))) (sqrt (fma (* v v) -3 1))))>
3.452 * * * * [progress]: [ 62 / 115 ] simplifiying candidate #<alt (λ (v) (* (+ (fma (/ (sqrt 1) 1) (/ (sqrt 2) 4) (- (* (* v v) (/ (sqrt 2) 4)))) (fma (- (* v v)) (/ (sqrt 2) 4) (* (* v v) (/ (sqrt 2) 4)))) (sqrt (fma (* v v) -3 1))))>
3.452 * * * * [progress]: [ 63 / 115 ] simplifiying candidate #<alt (λ (v) (* (+ (fma (/ (sqrt (sqrt 2)) (* (cbrt 4) (cbrt 4))) (/ (sqrt (sqrt 2)) (cbrt 4)) (- (* (* v v) (/ (sqrt 2) 4)))) (fma (- (* v v)) (/ (sqrt 2) 4) (* (* v v) (/ (sqrt 2) 4)))) (sqrt (fma (* v v) -3 1))))>
3.452 * * * * [progress]: [ 64 / 115 ] simplifiying candidate #<alt (λ (v) (* (+ (fma (/ (sqrt (sqrt 2)) (sqrt 4)) (/ (sqrt (sqrt 2)) (sqrt 4)) (- (* (* v v) (/ (sqrt 2) 4)))) (fma (- (* v v)) (/ (sqrt 2) 4) (* (* v v) (/ (sqrt 2) 4)))) (sqrt (fma (* v v) -3 1))))>
3.452 * * * * [progress]: [ 65 / 115 ] simplifiying candidate #<alt (λ (v) (* (+ (fma (/ (sqrt (sqrt 2)) 1) (/ (sqrt (sqrt 2)) 4) (- (* (* v v) (/ (sqrt 2) 4)))) (fma (- (* v v)) (/ (sqrt 2) 4) (* (* v v) (/ (sqrt 2) 4)))) (sqrt (fma (* v v) -3 1))))>
3.452 * * * * [progress]: [ 66 / 115 ] simplifiying candidate #<alt (λ (v) (* (+ (fma (/ 1 (* (cbrt 4) (cbrt 4))) (/ (sqrt 2) (cbrt 4)) (- (* (* v v) (/ (sqrt 2) 4)))) (fma (- (* v v)) (/ (sqrt 2) 4) (* (* v v) (/ (sqrt 2) 4)))) (sqrt (fma (* v v) -3 1))))>
3.452 * * * * [progress]: [ 67 / 115 ] simplifiying candidate #<alt (λ (v) (* (+ (fma (/ 1 (sqrt 4)) (/ (sqrt 2) (sqrt 4)) (- (* (* v v) (/ (sqrt 2) 4)))) (fma (- (* v v)) (/ (sqrt 2) 4) (* (* v v) (/ (sqrt 2) 4)))) (sqrt (fma (* v v) -3 1))))>
3.452 * * * * [progress]: [ 68 / 115 ] simplifiying candidate #<alt (λ (v) (* (+ (fma (/ 1 1) (/ (sqrt 2) 4) (- (* (* v v) (/ (sqrt 2) 4)))) (fma (- (* v v)) (/ (sqrt 2) 4) (* (* v v) (/ (sqrt 2) 4)))) (sqrt (fma (* v v) -3 1))))>
3.452 * * * * [progress]: [ 69 / 115 ] simplifiying candidate #<alt (λ (v) (* (+ (fma 1 (/ (sqrt 2) 4) (- (* (* v v) (/ (sqrt 2) 4)))) (fma (- (* v v)) (/ (sqrt 2) 4) (* (* v v) (/ (sqrt 2) 4)))) (sqrt (fma (* v v) -3 1))))>
3.452 * * * * [progress]: [ 70 / 115 ] simplifiying candidate #<alt (λ (v) (* (+ (fma (sqrt 2) (/ 1 4) (- (* (* v v) (/ (sqrt 2) 4)))) (fma (- (* v v)) (/ (sqrt 2) 4) (* (* v v) (/ (sqrt 2) 4)))) (sqrt (fma (* v v) -3 1))))>
3.452 * * * * [progress]: [ 71 / 115 ] simplifiying candidate #<alt (λ (v) (* (log1p (expm1 (- (/ (sqrt 2) 4) (* (/ (sqrt 2) 4) (* v v))))) (sqrt (fma (* v v) -3 1))))>
3.452 * * * * [progress]: [ 72 / 115 ] simplifiying candidate #<alt (λ (v) (* (expm1 (log1p (- (/ (sqrt 2) 4) (* (/ (sqrt 2) 4) (* v v))))) (sqrt (fma (* v v) -3 1))))>
3.452 * * * * [progress]: [ 73 / 115 ] simplifiying candidate #<alt (λ (v) (* (fma (* (cbrt (/ (sqrt 2) 4)) (cbrt (/ (sqrt 2) 4))) (cbrt (/ (sqrt 2) 4)) (- (* (/ (sqrt 2) 4) (* v v)))) (sqrt (fma (* v v) -3 1))))>
3.453 * * * * [progress]: [ 74 / 115 ] simplifiying candidate #<alt (λ (v) (* (fma (sqrt (/ (sqrt 2) 4)) (sqrt (/ (sqrt 2) 4)) (- (* (/ (sqrt 2) 4) (* v v)))) (sqrt (fma (* v v) -3 1))))>
3.453 * * * * [progress]: [ 75 / 115 ] simplifiying candidate #<alt (λ (v) (* (fma (/ (* (cbrt (sqrt 2)) (cbrt (sqrt 2))) (* (cbrt 4) (cbrt 4))) (/ (cbrt (sqrt 2)) (cbrt 4)) (- (* (/ (sqrt 2) 4) (* v v)))) (sqrt (fma (* v v) -3 1))))>
3.453 * * * * [progress]: [ 76 / 115 ] simplifiying candidate #<alt (λ (v) (* (fma (/ (* (cbrt (sqrt 2)) (cbrt (sqrt 2))) (sqrt 4)) (/ (cbrt (sqrt 2)) (sqrt 4)) (- (* (/ (sqrt 2) 4) (* v v)))) (sqrt (fma (* v v) -3 1))))>
3.453 * * * * [progress]: [ 77 / 115 ] simplifiying candidate #<alt (λ (v) (* (fma (/ (* (cbrt (sqrt 2)) (cbrt (sqrt 2))) 1) (/ (cbrt (sqrt 2)) 4) (- (* (/ (sqrt 2) 4) (* v v)))) (sqrt (fma (* v v) -3 1))))>
3.453 * * * * [progress]: [ 78 / 115 ] simplifiying candidate #<alt (λ (v) (* (fma (/ (sqrt (* (cbrt 2) (cbrt 2))) (* (cbrt 4) (cbrt 4))) (/ (sqrt (cbrt 2)) (cbrt 4)) (- (* (/ (sqrt 2) 4) (* v v)))) (sqrt (fma (* v v) -3 1))))>
3.453 * * * * [progress]: [ 79 / 115 ] simplifiying candidate #<alt (λ (v) (* (fma (/ (sqrt (* (cbrt 2) (cbrt 2))) (sqrt 4)) (/ (sqrt (cbrt 2)) (sqrt 4)) (- (* (/ (sqrt 2) 4) (* v v)))) (sqrt (fma (* v v) -3 1))))>
3.453 * * * * [progress]: [ 80 / 115 ] simplifiying candidate #<alt (λ (v) (* (fma (/ (sqrt (* (cbrt 2) (cbrt 2))) 1) (/ (sqrt (cbrt 2)) 4) (- (* (/ (sqrt 2) 4) (* v v)))) (sqrt (fma (* v v) -3 1))))>
3.453 * * * * [progress]: [ 81 / 115 ] simplifiying candidate #<alt (λ (v) (* (fma (/ (sqrt (sqrt 2)) (* (cbrt 4) (cbrt 4))) (/ (sqrt (sqrt 2)) (cbrt 4)) (- (* (/ (sqrt 2) 4) (* v v)))) (sqrt (fma (* v v) -3 1))))>
3.453 * * * * [progress]: [ 82 / 115 ] simplifiying candidate #<alt (λ (v) (* (fma (/ (sqrt (sqrt 2)) (sqrt 4)) (/ (sqrt (sqrt 2)) (sqrt 4)) (- (* (/ (sqrt 2) 4) (* v v)))) (sqrt (fma (* v v) -3 1))))>
3.453 * * * * [progress]: [ 83 / 115 ] simplifiying candidate #<alt (λ (v) (* (fma (/ (sqrt (sqrt 2)) 1) (/ (sqrt (sqrt 2)) 4) (- (* (/ (sqrt 2) 4) (* v v)))) (sqrt (fma (* v v) -3 1))))>
3.453 * * * * [progress]: [ 84 / 115 ] simplifiying candidate #<alt (λ (v) (* (fma (/ (sqrt 1) (* (cbrt 4) (cbrt 4))) (/ (sqrt 2) (cbrt 4)) (- (* (/ (sqrt 2) 4) (* v v)))) (sqrt (fma (* v v) -3 1))))>
3.453 * * * * [progress]: [ 85 / 115 ] simplifiying candidate #<alt (λ (v) (* (fma (/ (sqrt 1) (sqrt 4)) (/ (sqrt 2) (sqrt 4)) (- (* (/ (sqrt 2) 4) (* v v)))) (sqrt (fma (* v v) -3 1))))>
3.453 * * * * [progress]: [ 86 / 115 ] simplifiying candidate #<alt (λ (v) (* (fma (/ (sqrt 1) 1) (/ (sqrt 2) 4) (- (* (/ (sqrt 2) 4) (* v v)))) (sqrt (fma (* v v) -3 1))))>
3.453 * * * * [progress]: [ 87 / 115 ] simplifiying candidate #<alt (λ (v) (* (fma (/ (sqrt (sqrt 2)) (* (cbrt 4) (cbrt 4))) (/ (sqrt (sqrt 2)) (cbrt 4)) (- (* (/ (sqrt 2) 4) (* v v)))) (sqrt (fma (* v v) -3 1))))>
3.453 * * * * [progress]: [ 88 / 115 ] simplifiying candidate #<alt (λ (v) (* (fma (/ (sqrt (sqrt 2)) (sqrt 4)) (/ (sqrt (sqrt 2)) (sqrt 4)) (- (* (/ (sqrt 2) 4) (* v v)))) (sqrt (fma (* v v) -3 1))))>
3.454 * * * * [progress]: [ 89 / 115 ] simplifiying candidate #<alt (λ (v) (* (fma (/ (sqrt (sqrt 2)) 1) (/ (sqrt (sqrt 2)) 4) (- (* (/ (sqrt 2) 4) (* v v)))) (sqrt (fma (* v v) -3 1))))>
3.454 * * * * [progress]: [ 90 / 115 ] simplifiying candidate #<alt (λ (v) (* (fma (/ 1 (* (cbrt 4) (cbrt 4))) (/ (sqrt 2) (cbrt 4)) (- (* (/ (sqrt 2) 4) (* v v)))) (sqrt (fma (* v v) -3 1))))>
3.454 * * * * [progress]: [ 91 / 115 ] simplifiying candidate #<alt (λ (v) (* (fma (/ 1 (sqrt 4)) (/ (sqrt 2) (sqrt 4)) (- (* (/ (sqrt 2) 4) (* v v)))) (sqrt (fma (* v v) -3 1))))>
3.454 * * * * [progress]: [ 92 / 115 ] simplifiying candidate #<alt (λ (v) (* (fma (/ 1 1) (/ (sqrt 2) 4) (- (* (/ (sqrt 2) 4) (* v v)))) (sqrt (fma (* v v) -3 1))))>
3.454 * * * * [progress]: [ 93 / 115 ] simplifiying candidate #<alt (λ (v) (* (fma 1 (/ (sqrt 2) 4) (- (* (/ (sqrt 2) 4) (* v v)))) (sqrt (fma (* v v) -3 1))))>
3.454 * * * * [progress]: [ 94 / 115 ] simplifiying candidate #<alt (λ (v) (* (fma (sqrt 2) (/ 1 4) (- (* (/ (sqrt 2) 4) (* v v)))) (sqrt (fma (* v v) -3 1))))>
3.454 * * * * [progress]: [ 95 / 115 ] simplifiying candidate #<alt (λ (v) (* (log (/ (exp (/ (sqrt 2) 4)) (exp (* (/ (sqrt 2) 4) (* v v))))) (sqrt (fma (* v v) -3 1))))>
3.454 * * * * [progress]: [ 96 / 115 ] simplifiying candidate #<alt (λ (v) (* (pow (- (/ (sqrt 2) 4) (* (/ (sqrt 2) 4) (* v v))) 1) (sqrt (fma (* v v) -3 1))))>
3.454 * * * * [progress]: [ 97 / 115 ] simplifiying candidate #<alt (λ (v) (* (exp (log (- (/ (sqrt 2) 4) (* (/ (sqrt 2) 4) (* v v))))) (sqrt (fma (* v v) -3 1))))>
3.454 * * * * [progress]: [ 98 / 115 ] simplifiying candidate #<alt (λ (v) (* (log (exp (- (/ (sqrt 2) 4) (* (/ (sqrt 2) 4) (* v v))))) (sqrt (fma (* v v) -3 1))))>
3.454 * * * * [progress]: [ 99 / 115 ] simplifiying candidate #<alt (λ (v) (* (* (* (cbrt (- (/ (sqrt 2) 4) (* (/ (sqrt 2) 4) (* v v)))) (cbrt (- (/ (sqrt 2) 4) (* (/ (sqrt 2) 4) (* v v))))) (cbrt (- (/ (sqrt 2) 4) (* (/ (sqrt 2) 4) (* v v))))) (sqrt (fma (* v v) -3 1))))>
3.454 * * * * [progress]: [ 100 / 115 ] simplifiying candidate #<alt (λ (v) (* (cbrt (* (* (- (/ (sqrt 2) 4) (* (/ (sqrt 2) 4) (* v v))) (- (/ (sqrt 2) 4) (* (/ (sqrt 2) 4) (* v v)))) (- (/ (sqrt 2) 4) (* (/ (sqrt 2) 4) (* v v))))) (sqrt (fma (* v v) -3 1))))>
3.454 * * * * [progress]: [ 101 / 115 ] simplifiying candidate #<alt (λ (v) (* (* (sqrt (- (/ (sqrt 2) 4) (* (/ (sqrt 2) 4) (* v v)))) (sqrt (- (/ (sqrt 2) 4) (* (/ (sqrt 2) 4) (* v v))))) (sqrt (fma (* v v) -3 1))))>
3.454 * * * * [progress]: [ 102 / 115 ] simplifiying candidate #<alt (λ (v) (* (/ (- (sqrt 2) (* (sqrt 2) (* v v))) 4) (sqrt (fma (* v v) -3 1))))>
3.454 * * * * [progress]: [ 103 / 115 ] simplifiying candidate #<alt (λ (v) (* (/ (- (* (sqrt 2) 4) (* 4 (* (sqrt 2) (* v v)))) (* 4 4)) (sqrt (fma (* v v) -3 1))))>
3.454 * * * * [progress]: [ 104 / 115 ] simplifiying candidate #<alt (λ (v) (* (/ (- (pow (/ (sqrt 2) 4) 3) (pow (* (/ (sqrt 2) 4) (* v v)) 3)) (+ (* (/ (sqrt 2) 4) (/ (sqrt 2) 4)) (+ (* (* (/ (sqrt 2) 4) (* v v)) (* (/ (sqrt 2) 4) (* v v))) (* (/ (sqrt 2) 4) (* (/ (sqrt 2) 4) (* v v)))))) (sqrt (fma (* v v) -3 1))))>
3.455 * * * * [progress]: [ 105 / 115 ] simplifiying candidate #<alt (λ (v) (* (+ (/ (sqrt 2) 4) (- (* (/ (sqrt 2) 4) (* v v)))) (sqrt (fma (* v v) -3 1))))>
3.455 * * * * [progress]: [ 106 / 115 ] simplifiying candidate #<alt (λ (v) (* (* 1 (- (/ (sqrt 2) 4) (* (/ (sqrt 2) 4) (* v v)))) (sqrt (fma (* v v) -3 1))))>
3.455 * * * * [progress]: [ 107 / 115 ] simplifiying candidate #<alt (λ (v) (* (/ (- (* (/ (sqrt 2) 4) (/ (sqrt 2) 4)) (* (* (/ (sqrt 2) 4) (* v v)) (* (/ (sqrt 2) 4) (* v v)))) (+ (/ (sqrt 2) 4) (* (/ (sqrt 2) 4) (* v v)))) (sqrt (fma (* v v) -3 1))))>
3.455 * * * * [progress]: [ 108 / 115 ] simplifiying candidate #<alt (λ (v) (* (+ (/ (sqrt 2) 4) (- (* (/ (sqrt 2) 4) (* v v)))) (sqrt (fma (* v v) -3 1))))>
3.455 * * * * [progress]: [ 109 / 115 ] simplifiying candidate #<alt (λ (v) (* (posit16->real (real->posit16 (- (/ (sqrt 2) 4) (* (/ (sqrt 2) 4) (* v v))))) (sqrt (fma (* v v) -3 1))))>
3.455 * * * * [progress]: [ 110 / 115 ] simplifiying candidate #<alt (λ (v) (* (- (/ (sqrt 2) 4) (* 1/4 (* (sqrt 2) (pow v 2)))) (sqrt (fma (* v v) -3 1))))>
3.455 * * * * [progress]: [ 111 / 115 ] simplifiying candidate #<alt (λ (v) (* (- (/ (sqrt 2) 4) (* 1/4 (* (sqrt 2) (pow v 2)))) (sqrt (fma (* v v) -3 1))))>
3.455 * * * * [progress]: [ 112 / 115 ] simplifiying candidate #<alt (λ (v) (* (- (/ (sqrt 2) 4) (* 1/4 (* (sqrt 2) (pow v 2)))) (sqrt (fma (* v v) -3 1))))>
3.455 * * * * [progress]: [ 113 / 115 ] simplifiying candidate #<alt (λ (v) (* (- (* 1/4 (sqrt 2)) (* 1/4 (* (sqrt 2) (pow v 2)))) (sqrt (fma (* v v) -3 1))))>
3.455 * * * * [progress]: [ 114 / 115 ] simplifiying candidate #<alt (λ (v) (* (- (* 1/4 (sqrt 2)) (* 1/4 (* (sqrt 2) (pow v 2)))) (sqrt (fma (* v v) -3 1))))>
3.455 * * * * [progress]: [ 115 / 115 ] simplifiying candidate #<alt (λ (v) (* (- (* 1/4 (sqrt 2)) (* 1/4 (* (sqrt 2) (pow v 2)))) (sqrt (fma (* v v) -3 1))))>
3.457 * [simplify]: Simplifying (expm1 (* (/ (sqrt 2) 4) (* v v))), (log1p (* (/ (sqrt 2) 4) (* v v))), (* (/ (sqrt 2) 4) (* v v)), (* (/ (sqrt 2) 4) (* v v)), (+ (- (log (sqrt 2)) (log 4)) (+ (log v) (log v))), (+ (- (log (sqrt 2)) (log 4)) (log (* v v))), (+ (log (/ (sqrt 2) 4)) (+ (log v) (log v))), (+ (log (/ (sqrt 2) 4)) (log (* v v))), (log (* (/ (sqrt 2) 4) (* v v))), (exp (* (/ (sqrt 2) 4) (* v v))), (* (/ (* (* (sqrt 2) (sqrt 2)) (sqrt 2)) (* (* 4 4) 4)) (* (* (* v v) v) (* (* v v) v))), (* (/ (* (* (sqrt 2) (sqrt 2)) (sqrt 2)) (* (* 4 4) 4)) (* (* (* v v) (* v v)) (* v v))), (* (* (* (/ (sqrt 2) 4) (/ (sqrt 2) 4)) (/ (sqrt 2) 4)) (* (* (* v v) v) (* (* v v) v))), (* (* (* (/ (sqrt 2) 4) (/ (sqrt 2) 4)) (/ (sqrt 2) 4)) (* (* (* v v) (* v v)) (* v v))), (* (cbrt (* (/ (sqrt 2) 4) (* v v))) (cbrt (* (/ (sqrt 2) 4) (* v v)))), (cbrt (* (/ (sqrt 2) 4) (* v v))), (* (* (* (/ (sqrt 2) 4) (* v v)) (* (/ (sqrt 2) 4) (* v v))) (* (/ (sqrt 2) 4) (* v v))), (sqrt (* (/ (sqrt 2) 4) (* v v))), (sqrt (* (/ (sqrt 2) 4) (* v v))), (* (sqrt (/ (sqrt 2) 4)) v), (* (sqrt (/ (sqrt 2) 4)) v), (* (/ (sqrt (sqrt 2)) (sqrt 4)) v), (* (/ (sqrt (sqrt 2)) (sqrt 4)) v), (* (/ (sqrt (sqrt 2)) (sqrt 4)) v), (* (/ (sqrt (sqrt 2)) (sqrt 4)) v), (* (/ (sqrt 2) 4) v), (* (cbrt (/ (sqrt 2) 4)) (* v v)), (* (sqrt (/ (sqrt 2) 4)) (* v v)), (* (/ (cbrt (sqrt 2)) (cbrt 4)) (* v v)), (* (/ (cbrt (sqrt 2)) (sqrt 4)) (* v v)), (* (/ (cbrt (sqrt 2)) 4) (* v v)), (* (/ (sqrt (cbrt 2)) (cbrt 4)) (* v v)), (* (/ (sqrt (cbrt 2)) (sqrt 4)) (* v v)), (* (/ (sqrt (cbrt 2)) 4) (* v v)), (* (/ (sqrt (sqrt 2)) (cbrt 4)) (* v v)), (* (/ (sqrt (sqrt 2)) (sqrt 4)) (* v v)), (* (/ (sqrt (sqrt 2)) 4) (* v v)), (* (/ (sqrt 2) (cbrt 4)) (* v v)), (* (/ (sqrt 2) (sqrt 4)) (* v v)), (* (/ (sqrt 2) 4) (* v v)), (* (/ (sqrt (sqrt 2)) (cbrt 4)) (* v v)), (* (/ (sqrt (sqrt 2)) (sqrt 4)) (* v v)), (* (/ (sqrt (sqrt 2)) 4) (* v v)), (* (/ (sqrt 2) (cbrt 4)) (* v v)), (* (/ (sqrt 2) (sqrt 4)) (* v v)), (* (/ (sqrt 2) 4) (* v v)), (* (/ (sqrt 2) 4) (* v v)), (* (/ 1 4) (* v v)), (* (sqrt 2) (* v v)), (real->posit16 (* (/ (sqrt 2) 4) (* v v))), (fma (* (cbrt (/ (sqrt 2) 4)) (cbrt (/ (sqrt 2) 4))) (cbrt (/ (sqrt 2) 4)) (- (* (* v v) (/ (sqrt 2) 4)))), (fma (- (* v v)) (/ (sqrt 2) 4) (* (* v v) (/ (sqrt 2) 4))), (fma (sqrt (/ (sqrt 2) 4)) (sqrt (/ (sqrt 2) 4)) (- (* (* v v) (/ (sqrt 2) 4)))), (fma (- (* v v)) (/ (sqrt 2) 4) (* (* v v) (/ (sqrt 2) 4))), (fma (/ (* (cbrt (sqrt 2)) (cbrt (sqrt 2))) (* (cbrt 4) (cbrt 4))) (/ (cbrt (sqrt 2)) (cbrt 4)) (- (* (* v v) (/ (sqrt 2) 4)))), (fma (- (* v v)) (/ (sqrt 2) 4) (* (* v v) (/ (sqrt 2) 4))), (fma (/ (* (cbrt (sqrt 2)) (cbrt (sqrt 2))) (sqrt 4)) (/ (cbrt (sqrt 2)) (sqrt 4)) (- (* (* v v) (/ (sqrt 2) 4)))), (fma (- (* v v)) (/ (sqrt 2) 4) (* (* v v) (/ (sqrt 2) 4))), (fma (/ (* (cbrt (sqrt 2)) (cbrt (sqrt 2))) 1) (/ (cbrt (sqrt 2)) 4) (- (* (* v v) (/ (sqrt 2) 4)))), (fma (- (* v v)) (/ (sqrt 2) 4) (* (* v v) (/ (sqrt 2) 4))), (fma (/ (sqrt (* (cbrt 2) (cbrt 2))) (* (cbrt 4) (cbrt 4))) (/ (sqrt (cbrt 2)) (cbrt 4)) (- (* (* v v) (/ (sqrt 2) 4)))), (fma (- (* v v)) (/ (sqrt 2) 4) (* (* v v) (/ (sqrt 2) 4))), (fma (/ (sqrt (* (cbrt 2) (cbrt 2))) (sqrt 4)) (/ (sqrt (cbrt 2)) (sqrt 4)) (- (* (* v v) (/ (sqrt 2) 4)))), (fma (- (* v v)) (/ (sqrt 2) 4) (* (* v v) (/ (sqrt 2) 4))), (fma (/ (sqrt (* (cbrt 2) (cbrt 2))) 1) (/ (sqrt (cbrt 2)) 4) (- (* (* v v) (/ (sqrt 2) 4)))), (fma (- (* v v)) (/ (sqrt 2) 4) (* (* v v) (/ (sqrt 2) 4))), (fma (/ (sqrt (sqrt 2)) (* (cbrt 4) (cbrt 4))) (/ (sqrt (sqrt 2)) (cbrt 4)) (- (* (* v v) (/ (sqrt 2) 4)))), (fma (- (* v v)) (/ (sqrt 2) 4) (* (* v v) (/ (sqrt 2) 4))), (fma (/ (sqrt (sqrt 2)) (sqrt 4)) (/ (sqrt (sqrt 2)) (sqrt 4)) (- (* (* v v) (/ (sqrt 2) 4)))), (fma (- (* v v)) (/ (sqrt 2) 4) (* (* v v) (/ (sqrt 2) 4))), (fma (/ (sqrt (sqrt 2)) 1) (/ (sqrt (sqrt 2)) 4) (- (* (* v v) (/ (sqrt 2) 4)))), (fma (- (* v v)) (/ (sqrt 2) 4) (* (* v v) (/ (sqrt 2) 4))), (fma (/ (sqrt 1) (* (cbrt 4) (cbrt 4))) (/ (sqrt 2) (cbrt 4)) (- (* (* v v) (/ (sqrt 2) 4)))), (fma (- (* v v)) (/ (sqrt 2) 4) (* (* v v) (/ (sqrt 2) 4))), (fma (/ (sqrt 1) (sqrt 4)) (/ (sqrt 2) (sqrt 4)) (- (* (* v v) (/ (sqrt 2) 4)))), (fma (- (* v v)) (/ (sqrt 2) 4) (* (* v v) (/ (sqrt 2) 4))), (fma (/ (sqrt 1) 1) (/ (sqrt 2) 4) (- (* (* v v) (/ (sqrt 2) 4)))), (fma (- (* v v)) (/ (sqrt 2) 4) (* (* v v) (/ (sqrt 2) 4))), (fma (/ (sqrt (sqrt 2)) (* (cbrt 4) (cbrt 4))) (/ (sqrt (sqrt 2)) (cbrt 4)) (- (* (* v v) (/ (sqrt 2) 4)))), (fma (- (* v v)) (/ (sqrt 2) 4) (* (* v v) (/ (sqrt 2) 4))), (fma (/ (sqrt (sqrt 2)) (sqrt 4)) (/ (sqrt (sqrt 2)) (sqrt 4)) (- (* (* v v) (/ (sqrt 2) 4)))), (fma (- (* v v)) (/ (sqrt 2) 4) (* (* v v) (/ (sqrt 2) 4))), (fma (/ (sqrt (sqrt 2)) 1) (/ (sqrt (sqrt 2)) 4) (- (* (* v v) (/ (sqrt 2) 4)))), (fma (- (* v v)) (/ (sqrt 2) 4) (* (* v v) (/ (sqrt 2) 4))), (fma (/ 1 (* (cbrt 4) (cbrt 4))) (/ (sqrt 2) (cbrt 4)) (- (* (* v v) (/ (sqrt 2) 4)))), (fma (- (* v v)) (/ (sqrt 2) 4) (* (* v v) (/ (sqrt 2) 4))), (fma (/ 1 (sqrt 4)) (/ (sqrt 2) (sqrt 4)) (- (* (* v v) (/ (sqrt 2) 4)))), (fma (- (* v v)) (/ (sqrt 2) 4) (* (* v v) (/ (sqrt 2) 4))), (fma (/ 1 1) (/ (sqrt 2) 4) (- (* (* v v) (/ (sqrt 2) 4)))), (fma (- (* v v)) (/ (sqrt 2) 4) (* (* v v) (/ (sqrt 2) 4))), (fma 1 (/ (sqrt 2) 4) (- (* (* v v) (/ (sqrt 2) 4)))), (fma (- (* v v)) (/ (sqrt 2) 4) (* (* v v) (/ (sqrt 2) 4))), (fma (sqrt 2) (/ 1 4) (- (* (* v v) (/ (sqrt 2) 4)))), (fma (- (* v v)) (/ (sqrt 2) 4) (* (* v v) (/ (sqrt 2) 4))), (expm1 (- (/ (sqrt 2) 4) (* (/ (sqrt 2) 4) (* v v)))), (log1p (- (/ (sqrt 2) 4) (* (/ (sqrt 2) 4) (* v v)))), (- (* (/ (sqrt 2) 4) (* v v))), (- (* (/ (sqrt 2) 4) (* v v))), (- (* (/ (sqrt 2) 4) (* v v))), (- (* (/ (sqrt 2) 4) (* v v))), (- (* (/ (sqrt 2) 4) (* v v))), (- (* (/ (sqrt 2) 4) (* v v))), (- (* (/ (sqrt 2) 4) (* v v))), (- (* (/ (sqrt 2) 4) (* v v))), (- (* (/ (sqrt 2) 4) (* v v))), (- (* (/ (sqrt 2) 4) (* v v))), (- (* (/ (sqrt 2) 4) (* v v))), (- (* (/ (sqrt 2) 4) (* v v))), (- (* (/ (sqrt 2) 4) (* v v))), (- (* (/ (sqrt 2) 4) (* v v))), (- (* (/ (sqrt 2) 4) (* v v))), (- (* (/ (sqrt 2) 4) (* v v))), (- (* (/ (sqrt 2) 4) (* v v))), (- (* (/ (sqrt 2) 4) (* v v))), (- (* (/ (sqrt 2) 4) (* v v))), (- (* (/ (sqrt 2) 4) (* v v))), (- (* (/ (sqrt 2) 4) (* v v))), (- (* (/ (sqrt 2) 4) (* v v))), (/ (exp (/ (sqrt 2) 4)) (exp (* (/ (sqrt 2) 4) (* v v)))), (log (- (/ (sqrt 2) 4) (* (/ (sqrt 2) 4) (* v v)))), (exp (- (/ (sqrt 2) 4) (* (/ (sqrt 2) 4) (* v v)))), (* (cbrt (- (/ (sqrt 2) 4) (* (/ (sqrt 2) 4) (* v v)))) (cbrt (- (/ (sqrt 2) 4) (* (/ (sqrt 2) 4) (* v v))))), (cbrt (- (/ (sqrt 2) 4) (* (/ (sqrt 2) 4) (* v v)))), (* (* (- (/ (sqrt 2) 4) (* (/ (sqrt 2) 4) (* v v))) (- (/ (sqrt 2) 4) (* (/ (sqrt 2) 4) (* v v)))) (- (/ (sqrt 2) 4) (* (/ (sqrt 2) 4) (* v v)))), (sqrt (- (/ (sqrt 2) 4) (* (/ (sqrt 2) 4) (* v v)))), (sqrt (- (/ (sqrt 2) 4) (* (/ (sqrt 2) 4) (* v v)))), (- (sqrt 2) (* (sqrt 2) (* v v))), (- (* (sqrt 2) 4) (* 4 (* (sqrt 2) (* v v)))), (* 4 4), (- (pow (/ (sqrt 2) 4) 3) (pow (* (/ (sqrt 2) 4) (* v v)) 3)), (+ (* (/ (sqrt 2) 4) (/ (sqrt 2) 4)) (+ (* (* (/ (sqrt 2) 4) (* v v)) (* (/ (sqrt 2) 4) (* v v))) (* (/ (sqrt 2) 4) (* (/ (sqrt 2) 4) (* v v))))), (- (* (/ (sqrt 2) 4) (* v v))), (- (* (/ (sqrt 2) 4) (/ (sqrt 2) 4)) (* (* (/ (sqrt 2) 4) (* v v)) (* (/ (sqrt 2) 4) (* v v)))), (+ (/ (sqrt 2) 4) (* (/ (sqrt 2) 4) (* v v))), (- (* (/ (sqrt 2) 4) (* v v))), (real->posit16 (- (/ (sqrt 2) 4) (* (/ (sqrt 2) 4) (* v v)))), (* 1/4 (* (sqrt 2) (pow v 2))), (* 1/4 (* (sqrt 2) (pow v 2))), (* 1/4 (* (sqrt 2) (pow v 2))), (- (* 1/4 (sqrt 2)) (* 1/4 (* (sqrt 2) (pow v 2)))), (- (* 1/4 (sqrt 2)) (* 1/4 (* (sqrt 2) (pow v 2)))), (- (* 1/4 (sqrt 2)) (* 1/4 (* (sqrt 2) (pow v 2))))
3.461 * * [simplify]: iteration 1: (158 enodes)
3.524 * * [simplify]: iteration 2: (701 enodes)
3.784 * * [simplify]: iteration 3: (1629 enodes)
5.245 * * [simplify]: Extracting #0: cost 56 inf + 0
5.247 * * [simplify]: Extracting #1: cost 442 inf + 1
5.257 * * [simplify]: Extracting #2: cost 954 inf + 12220
5.299 * * [simplify]: Extracting #3: cost 461 inf + 112262
5.369 * * [simplify]: Extracting #4: cost 90 inf + 206988
5.443 * * [simplify]: Extracting #5: cost 2 inf + 233497
5.521 * * [simplify]: Extracting #6: cost 0 inf + 233654
5.604 * [simplify]: Simplified to (expm1 (* v (/ (sqrt 2) (/ 4 v)))), (log1p (* v (/ (sqrt 2) (/ 4 v)))), (* v (/ (sqrt 2) (/ 4 v))), (* v (/ (sqrt 2) (/ 4 v))), (log (* v (/ (sqrt 2) (/ 4 v)))), (log (* v (/ (sqrt 2) (/ 4 v)))), (log (* v (/ (sqrt 2) (/ 4 v)))), (log (* v (/ (sqrt 2) (/ 4 v)))), (log (* v (/ (sqrt 2) (/ 4 v)))), (exp (* v (/ (sqrt 2) (/ 4 v)))), (* (* (* (* v v) v) (* (* v v) v)) (* 1/32 (sqrt 2))), (* (* (* (* v v) v) (* (* v v) v)) (* 1/32 (sqrt 2))), (* (* (* (* v v) v) (* (* v v) v)) (* 1/32 (sqrt 2))), (* (* (* (* v v) v) (* (* v v) v)) (* 1/32 (sqrt 2))), (* (cbrt (* v (/ (sqrt 2) (/ 4 v)))) (cbrt (* v (/ (sqrt 2) (/ 4 v))))), (cbrt (* v (/ (sqrt 2) (/ 4 v)))), (* (* (* (* v v) v) (* (* v v) v)) (* 1/32 (sqrt 2))), (sqrt (* v (/ (sqrt 2) (/ 4 v)))), (sqrt (* v (/ (sqrt 2) (/ 4 v)))), (* (sqrt (/ (sqrt 2) 4)) v), (* (sqrt (/ (sqrt 2) 4)) v), (* (/ v 2) (sqrt (sqrt 2))), (* (/ v 2) (sqrt (sqrt 2))), (* (/ v 2) (sqrt (sqrt 2))), (* (/ v 2) (sqrt (sqrt 2))), (/ (sqrt 2) (/ 4 v)), (* (cbrt (/ (sqrt 2) 4)) (* v v)), (* (* v v) (sqrt (/ (sqrt 2) 4))), (/ (* v (* v (cbrt (sqrt 2)))) (cbrt 4)), (/ (cbrt (sqrt 2)) (/ 2 (* v v))), (/ (cbrt (sqrt 2)) (/ (/ 4 v) v)), (/ (sqrt (cbrt 2)) (/ (cbrt 4) (* v v))), (/ (sqrt (cbrt 2)) (/ 2 (* v v))), (/ (sqrt (cbrt 2)) (/ (/ 4 v) v)), (/ (* (sqrt (sqrt 2)) (* v v)) (cbrt 4)), (/ (sqrt (sqrt 2)) (/ 2 (* v v))), (* v (* v (/ (sqrt (sqrt 2)) 4))), (* (* v (/ (sqrt 2) (cbrt 4))) v), (/ (sqrt 2) (/ 2 (* v v))), (* v (/ (sqrt 2) (/ 4 v))), (/ (* (sqrt (sqrt 2)) (* v v)) (cbrt 4)), (/ (sqrt (sqrt 2)) (/ 2 (* v v))), (* v (* v (/ (sqrt (sqrt 2)) 4))), (* (* v (/ (sqrt 2) (cbrt 4))) v), (/ (sqrt 2) (/ 2 (* v v))), (* v (/ (sqrt 2) (/ 4 v))), (* v (/ (sqrt 2) (/ 4 v))), (* (/ v 4) v), (* (sqrt 2) (* v v)), (real->posit16 (* v (/ (sqrt 2) (/ 4 v)))), (fma (cbrt (/ (sqrt 2) 4)) (* (cbrt (/ (sqrt 2) 4)) (cbrt (/ (sqrt 2) 4))) (* (* -1/4 (* (sqrt 2) v)) v)), (* (/ (sqrt 2) 4) (+ (- (* v v)) (* v v))), (* 1/4 (- (sqrt 2) (* (sqrt 2) (* v v)))), (* (/ (sqrt 2) 4) (+ (- (* v v)) (* v v))), (fma (/ (cbrt (sqrt 2)) (cbrt 4)) (* (/ (cbrt (sqrt 2)) (cbrt 4)) (/ (cbrt (sqrt 2)) (cbrt 4))) (* (* -1/4 (* (sqrt 2) v)) v)), (* (/ (sqrt 2) 4) (+ (- (* v v)) (* v v))), (+ (/ (/ (cbrt (sqrt 2)) (/ 2 (cbrt (sqrt 2)))) (/ 2 (cbrt (sqrt 2)))) (* (* -1/4 (* (sqrt 2) v)) v)), (* (/ (sqrt 2) 4) (+ (- (* v v)) (* v v))), (fma (/ (cbrt (sqrt 2)) 4) (* (cbrt (sqrt 2)) (cbrt (sqrt 2))) (* (* -1/4 (* (sqrt 2) v)) v)), (* (/ (sqrt 2) 4) (+ (- (* v v)) (* v v))), (fma (/ (fabs (cbrt 2)) (* (cbrt 4) (cbrt 4))) (/ (sqrt (cbrt 2)) (cbrt 4)) (* (* -1/4 (* (sqrt 2) v)) v)), (* (/ (sqrt 2) 4) (+ (- (* v v)) (* v v))), (fma (/ (sqrt (cbrt 2)) 2) (/ (fabs (cbrt 2)) 2) (* (* -1/4 (* (sqrt 2) v)) v)), (* (/ (sqrt 2) 4) (+ (- (* v v)) (* v v))), (fma (fabs (cbrt 2)) (/ (sqrt (cbrt 2)) 4) (* (* -1/4 (* (sqrt 2) v)) v)), (* (/ (sqrt 2) 4) (+ (- (* v v)) (* v v))), (- (/ (/ (/ (sqrt 2) (cbrt 4)) (cbrt 4)) (cbrt 4)) (* v (/ (sqrt 2) (/ 4 v)))), (* (/ (sqrt 2) 4) (+ (- (* v v)) (* v v))), (+ (* (* -1/4 (* (sqrt 2) v)) v) (/ (/ (sqrt 2) 2) 2)), (* (/ (sqrt 2) 4) (+ (- (* v v)) (* v v))), (* 1/4 (- (sqrt 2) (* (sqrt 2) (* v v)))), (* (/ (sqrt 2) 4) (+ (- (* v v)) (* v v))), (- (/ (/ (/ (sqrt 2) (cbrt 4)) (cbrt 4)) (cbrt 4)) (* v (/ (sqrt 2) (/ 4 v)))), (* (/ (sqrt 2) 4) (+ (- (* v v)) (* v v))), (* 1/4 (- (sqrt 2) (* (sqrt 2) (* v v)))), (* (/ (sqrt 2) 4) (+ (- (* v v)) (* v v))), (* 1/4 (- (sqrt 2) (* (sqrt 2) (* v v)))), (* (/ (sqrt 2) 4) (+ (- (* v v)) (* v v))), (- (/ (/ (/ (sqrt 2) (cbrt 4)) (cbrt 4)) (cbrt 4)) (* v (/ (sqrt 2) (/ 4 v)))), (* (/ (sqrt 2) 4) (+ (- (* v v)) (* v v))), (+ (* (* -1/4 (* (sqrt 2) v)) v) (/ (/ (sqrt 2) 2) 2)), (* (/ (sqrt 2) 4) (+ (- (* v v)) (* v v))), (* 1/4 (- (sqrt 2) (* (sqrt 2) (* v v)))), (* (/ (sqrt 2) 4) (+ (- (* v v)) (* v v))), (- (/ (/ (/ (sqrt 2) (cbrt 4)) (cbrt 4)) (cbrt 4)) (* v (/ (sqrt 2) (/ 4 v)))), (* (/ (sqrt 2) 4) (+ (- (* v v)) (* v v))), (* 1/4 (- (sqrt 2) (* (sqrt 2) (* v v)))), (* (/ (sqrt 2) 4) (+ (- (* v v)) (* v v))), (* 1/4 (- (sqrt 2) (* (sqrt 2) (* v v)))), (* (/ (sqrt 2) 4) (+ (- (* v v)) (* v v))), (* 1/4 (- (sqrt 2) (* (sqrt 2) (* v v)))), (* (/ (sqrt 2) 4) (+ (- (* v v)) (* v v))), (* 1/4 (- (sqrt 2) (* (sqrt 2) (* v v)))), (* (/ (sqrt 2) 4) (+ (- (* v v)) (* v v))), (expm1 (* 1/4 (- (sqrt 2) (* (sqrt 2) (* v v))))), (log1p (* 1/4 (- (sqrt 2) (* (sqrt 2) (* v v))))), (* (* -1/4 (* (sqrt 2) v)) v), (* (* -1/4 (* (sqrt 2) v)) v), (* (* -1/4 (* (sqrt 2) v)) v), (* (* -1/4 (* (sqrt 2) v)) v), (* (* -1/4 (* (sqrt 2) v)) v), (* (* -1/4 (* (sqrt 2) v)) v), (* (* -1/4 (* (sqrt 2) v)) v), (* (* -1/4 (* (sqrt 2) v)) v), (* (* -1/4 (* (sqrt 2) v)) v), (* (* -1/4 (* (sqrt 2) v)) v), (* (* -1/4 (* (sqrt 2) v)) v), (* (* -1/4 (* (sqrt 2) v)) v), (* (* -1/4 (* (sqrt 2) v)) v), (* (* -1/4 (* (sqrt 2) v)) v), (* (* -1/4 (* (sqrt 2) v)) v), (* (* -1/4 (* (sqrt 2) v)) v), (* (* -1/4 (* (sqrt 2) v)) v), (* (* -1/4 (* (sqrt 2) v)) v), (* (* -1/4 (* (sqrt 2) v)) v), (* (* -1/4 (* (sqrt 2) v)) v), (* (* -1/4 (* (sqrt 2) v)) v), (* (* -1/4 (* (sqrt 2) v)) v), (exp (* 1/4 (- (sqrt 2) (* (sqrt 2) (* v v))))), (log (* 1/4 (- (sqrt 2) (* (sqrt 2) (* v v))))), (exp (* 1/4 (- (sqrt 2) (* (sqrt 2) (* v v))))), (* (cbrt (* 1/4 (- (sqrt 2) (* (sqrt 2) (* v v))))) (cbrt (* 1/4 (- (sqrt 2) (* (sqrt 2) (* v v)))))), (cbrt (* 1/4 (- (sqrt 2) (* (sqrt 2) (* v v))))), (* (* (* 1/4 (- (sqrt 2) (* (sqrt 2) (* v v)))) (* 1/4 (- (sqrt 2) (* (sqrt 2) (* v v))))) (* 1/4 (- (sqrt 2) (* (sqrt 2) (* v v))))), (sqrt (* 1/4 (- (sqrt 2) (* (sqrt 2) (* v v))))), (sqrt (* 1/4 (- (sqrt 2) (* (sqrt 2) (* v v))))), (- (sqrt 2) (* (sqrt 2) (* v v))), (* (- (sqrt 2) (* (sqrt 2) (* v v))) 4), 16, (- (* 1/32 (sqrt 2)) (* (* (* (* v v) v) (* (* v v) v)) (* 1/32 (sqrt 2)))), (fma 1/8 (fma (* v v) (* v v) (* v v)) 1/8), (* (* -1/4 (* (sqrt 2) v)) v), (fma (* -1/8 (* v v)) (* v v) 1/8), (fma (/ (sqrt 2) 4) (* v v) (/ (sqrt 2) 4)), (* (* -1/4 (* (sqrt 2) v)) v), (real->posit16 (* 1/4 (- (sqrt 2) (* (sqrt 2) (* v v))))), (* v (/ (sqrt 2) (/ 4 v))), (* v (/ (sqrt 2) (/ 4 v))), (* v (/ (sqrt 2) (/ 4 v))), (* 1/4 (- (sqrt 2) (* (sqrt 2) (* v v)))), (* 1/4 (- (sqrt 2) (* (sqrt 2) (* v v)))), (* 1/4 (- (sqrt 2) (* (sqrt 2) (* v v))))
5.623 * * * [progress]: adding candidates to table
6.906 * * [progress]: iteration 2 / 4
6.906 * * * [progress]: picking best candidate
6.912 * * * * [pick]: Picked  #<alt (λ (v) (* (fma (sqrt (/ (sqrt 2) 4)) (sqrt (/ (sqrt 2) 4)) (- (* (/ (sqrt 2) 4) (* v v)))) (sqrt (fma (* v v) -3 1))))>
6.913 * * * [progress]: localizing error
6.943 * * * [progress]: generating rewritten candidates
6.943 * * * * [progress]: [ 1 / 2 ] rewriting at (2 1)
6.943 * * * * [progress]: [ 2 / 2 ] rewriting at (2 1 3 1)
6.983 * * * [progress]: generating series expansions
6.983 * * * * [progress]: [ 1 / 2 ] generating series at (2 1)
6.988 * [backup-simplify]: Simplify (fma (sqrt (/ (sqrt 2) 4)) (sqrt (/ (sqrt 2) 4)) (- (* (/ (sqrt 2) 4) (* v v)))) into (fma (* 1/2 (sqrt (sqrt 2))) (* 1/2 (sqrt (sqrt 2))) (- (* 1/4 (* (sqrt 2) (pow v 2)))))
6.988 * [approximate]: Taking taylor expansion of (fma (* 1/2 (sqrt (sqrt 2))) (* 1/2 (sqrt (sqrt 2))) (- (* 1/4 (* (sqrt 2) (pow v 2))))) in (v) around 0
6.988 * [taylor]: Taking taylor expansion of (fma (* 1/2 (sqrt (sqrt 2))) (* 1/2 (sqrt (sqrt 2))) (- (* 1/4 (* (sqrt 2) (pow v 2))))) in v
6.988 * [taylor]: Rewrote expression to (+ (* (* 1/2 (sqrt (sqrt 2))) (* 1/2 (sqrt (sqrt 2)))) (- (* 1/4 (* (sqrt 2) (pow v 2)))))
6.988 * [taylor]: Taking taylor expansion of (* (* 1/2 (sqrt (sqrt 2))) (* 1/2 (sqrt (sqrt 2)))) in v
6.988 * [taylor]: Taking taylor expansion of (* 1/2 (sqrt (sqrt 2))) in v
6.988 * [taylor]: Taking taylor expansion of 1/2 in v
6.988 * [backup-simplify]: Simplify 1/2 into 1/2
6.988 * [taylor]: Taking taylor expansion of (sqrt (sqrt 2)) in v
6.988 * [taylor]: Taking taylor expansion of (sqrt 2) in v
6.988 * [taylor]: Taking taylor expansion of 2 in v
6.988 * [backup-simplify]: Simplify 2 into 2
6.989 * [backup-simplify]: Simplify (sqrt 2) into (sqrt 2)
6.989 * [backup-simplify]: Simplify (/ 0 (* 2 (sqrt 2))) into 0
6.990 * [backup-simplify]: Simplify (sqrt (sqrt 2)) into (sqrt (sqrt 2))
6.991 * [backup-simplify]: Simplify (/ 0 (* 2 (sqrt (sqrt 2)))) into 0
6.991 * [taylor]: Taking taylor expansion of (* 1/2 (sqrt (sqrt 2))) in v
6.991 * [taylor]: Taking taylor expansion of 1/2 in v
6.991 * [backup-simplify]: Simplify 1/2 into 1/2
6.991 * [taylor]: Taking taylor expansion of (sqrt (sqrt 2)) in v
6.991 * [taylor]: Taking taylor expansion of (sqrt 2) in v
6.991 * [taylor]: Taking taylor expansion of 2 in v
6.991 * [backup-simplify]: Simplify 2 into 2
6.992 * [backup-simplify]: Simplify (sqrt 2) into (sqrt 2)
6.992 * [backup-simplify]: Simplify (/ 0 (* 2 (sqrt 2))) into 0
6.993 * [backup-simplify]: Simplify (sqrt (sqrt 2)) into (sqrt (sqrt 2))
6.994 * [backup-simplify]: Simplify (/ 0 (* 2 (sqrt (sqrt 2)))) into 0
6.994 * [taylor]: Taking taylor expansion of (- (* 1/4 (* (sqrt 2) (pow v 2)))) in v
6.994 * [taylor]: Taking taylor expansion of (* 1/4 (* (sqrt 2) (pow v 2))) in v
6.994 * [taylor]: Taking taylor expansion of 1/4 in v
6.994 * [backup-simplify]: Simplify 1/4 into 1/4
6.994 * [taylor]: Taking taylor expansion of (* (sqrt 2) (pow v 2)) in v
6.994 * [taylor]: Taking taylor expansion of (sqrt 2) in v
6.994 * [taylor]: Taking taylor expansion of 2 in v
6.994 * [backup-simplify]: Simplify 2 into 2
6.995 * [backup-simplify]: Simplify (sqrt 2) into (sqrt 2)
6.995 * [backup-simplify]: Simplify (/ 0 (* 2 (sqrt 2))) into 0
6.995 * [taylor]: Taking taylor expansion of (pow v 2) in v
6.995 * [taylor]: Taking taylor expansion of v in v
6.995 * [backup-simplify]: Simplify 0 into 0
6.995 * [backup-simplify]: Simplify 1 into 1
6.995 * [taylor]: Taking taylor expansion of (fma (* 1/2 (sqrt (sqrt 2))) (* 1/2 (sqrt (sqrt 2))) (- (* 1/4 (* (sqrt 2) (pow v 2))))) in v
6.995 * [taylor]: Rewrote expression to (+ (* (* 1/2 (sqrt (sqrt 2))) (* 1/2 (sqrt (sqrt 2)))) (- (* 1/4 (* (sqrt 2) (pow v 2)))))
6.996 * [taylor]: Taking taylor expansion of (* (* 1/2 (sqrt (sqrt 2))) (* 1/2 (sqrt (sqrt 2)))) in v
6.996 * [taylor]: Taking taylor expansion of (* 1/2 (sqrt (sqrt 2))) in v
6.996 * [taylor]: Taking taylor expansion of 1/2 in v
6.996 * [backup-simplify]: Simplify 1/2 into 1/2
6.996 * [taylor]: Taking taylor expansion of (sqrt (sqrt 2)) in v
6.996 * [taylor]: Taking taylor expansion of (sqrt 2) in v
6.996 * [taylor]: Taking taylor expansion of 2 in v
6.996 * [backup-simplify]: Simplify 2 into 2
6.996 * [backup-simplify]: Simplify (sqrt 2) into (sqrt 2)
6.997 * [backup-simplify]: Simplify (/ 0 (* 2 (sqrt 2))) into 0
6.998 * [backup-simplify]: Simplify (sqrt (sqrt 2)) into (sqrt (sqrt 2))
6.999 * [backup-simplify]: Simplify (/ 0 (* 2 (sqrt (sqrt 2)))) into 0
6.999 * [taylor]: Taking taylor expansion of (* 1/2 (sqrt (sqrt 2))) in v
6.999 * [taylor]: Taking taylor expansion of 1/2 in v
6.999 * [backup-simplify]: Simplify 1/2 into 1/2
6.999 * [taylor]: Taking taylor expansion of (sqrt (sqrt 2)) in v
6.999 * [taylor]: Taking taylor expansion of (sqrt 2) in v
6.999 * [taylor]: Taking taylor expansion of 2 in v
6.999 * [backup-simplify]: Simplify 2 into 2
6.999 * [backup-simplify]: Simplify (sqrt 2) into (sqrt 2)
7.000 * [backup-simplify]: Simplify (/ 0 (* 2 (sqrt 2))) into 0
7.001 * [backup-simplify]: Simplify (sqrt (sqrt 2)) into (sqrt (sqrt 2))
7.001 * [backup-simplify]: Simplify (/ 0 (* 2 (sqrt (sqrt 2)))) into 0
7.002 * [taylor]: Taking taylor expansion of (- (* 1/4 (* (sqrt 2) (pow v 2)))) in v
7.002 * [taylor]: Taking taylor expansion of (* 1/4 (* (sqrt 2) (pow v 2))) in v
7.002 * [taylor]: Taking taylor expansion of 1/4 in v
7.002 * [backup-simplify]: Simplify 1/4 into 1/4
7.002 * [taylor]: Taking taylor expansion of (* (sqrt 2) (pow v 2)) in v
7.002 * [taylor]: Taking taylor expansion of (sqrt 2) in v
7.002 * [taylor]: Taking taylor expansion of 2 in v
7.002 * [backup-simplify]: Simplify 2 into 2
7.002 * [backup-simplify]: Simplify (sqrt 2) into (sqrt 2)
7.003 * [backup-simplify]: Simplify (/ 0 (* 2 (sqrt 2))) into 0
7.003 * [taylor]: Taking taylor expansion of (pow v 2) in v
7.003 * [taylor]: Taking taylor expansion of v in v
7.003 * [backup-simplify]: Simplify 0 into 0
7.003 * [backup-simplify]: Simplify 1 into 1
7.004 * [backup-simplify]: Simplify (* 1/2 (sqrt (sqrt 2))) into (* 1/2 (sqrt (sqrt 2)))
7.006 * [backup-simplify]: Simplify (* 1/2 (sqrt (sqrt 2))) into (* 1/2 (sqrt (sqrt 2)))
7.010 * [backup-simplify]: Simplify (* (* 1/2 (sqrt (sqrt 2))) (* 1/2 (sqrt (sqrt 2)))) into (* 1/4 (sqrt 2))
7.011 * [backup-simplify]: Simplify (+ (* 1/4 (sqrt 2)) 0) into (* 1/4 (sqrt 2))
7.012 * [backup-simplify]: Simplify (* 1/4 (sqrt 2)) into (* 1/4 (sqrt 2))
7.014 * [backup-simplify]: Simplify (+ (* 1/2 0) (* 0 (sqrt (sqrt 2)))) into 0
7.015 * [backup-simplify]: Simplify (+ (* 1/2 0) (* 0 (sqrt (sqrt 2)))) into 0
7.016 * [backup-simplify]: Simplify (+ (* (* 1/2 (sqrt (sqrt 2))) 0) (* 0 (* 1/2 (sqrt (sqrt 2))))) into 0
7.016 * [backup-simplify]: Simplify (+ 0 0) into 0
7.016 * [backup-simplify]: Simplify 0 into 0
7.017 * [backup-simplify]: Simplify (/ (- 0 (pow 0 2) (+)) (* 2 (sqrt 2))) into 0
7.018 * [backup-simplify]: Simplify (/ (- 0 (pow 0 2) (+)) (* 2 (sqrt (sqrt 2)))) into 0
7.020 * [backup-simplify]: Simplify (+ (* 1/2 0) (+ (* 0 0) (* 0 (sqrt (sqrt 2))))) into 0
7.021 * [backup-simplify]: Simplify (/ (- 0 (pow 0 2) (+)) (* 2 (sqrt 2))) into 0
7.022 * [backup-simplify]: Simplify (/ (- 0 (pow 0 2) (+)) (* 2 (sqrt (sqrt 2)))) into 0
7.023 * [backup-simplify]: Simplify (+ (* 1/2 0) (+ (* 0 0) (* 0 (sqrt (sqrt 2))))) into 0
7.024 * [backup-simplify]: Simplify (+ (* (* 1/2 (sqrt (sqrt 2))) 0) (+ (* 0 0) (* 0 (* 1/2 (sqrt (sqrt 2)))))) into 0
7.024 * [backup-simplify]: Simplify (* 1 1) into 1
7.025 * [backup-simplify]: Simplify (* (sqrt 2) 1) into (sqrt 2)
7.026 * [backup-simplify]: Simplify (* 1/4 (sqrt 2)) into (* 1/4 (sqrt 2))
7.027 * [backup-simplify]: Simplify (- (* 1/4 (sqrt 2))) into (- (* 1/4 (sqrt 2)))
7.030 * [backup-simplify]: Simplify (+ 0 (- (* 1/4 (sqrt 2)))) into (- (* 1/4 (sqrt 2)))
7.031 * [backup-simplify]: Simplify (- (* 1/4 (sqrt 2))) into (- (* 1/4 (sqrt 2)))
7.032 * [backup-simplify]: Simplify (/ (- 0 (+ (* 2 (* 0 0)))) (* 2 (sqrt 2))) into 0
7.034 * [backup-simplify]: Simplify (/ (- 0 (+ (* 2 (* 0 0)))) (* 2 (sqrt (sqrt 2)))) into 0
7.035 * [backup-simplify]: Simplify (+ (* 1/2 0) (+ (* 0 0) (+ (* 0 0) (* 0 (sqrt (sqrt 2)))))) into 0
7.036 * [backup-simplify]: Simplify (/ (- 0 (+ (* 2 (* 0 0)))) (* 2 (sqrt 2))) into 0
7.038 * [backup-simplify]: Simplify (/ (- 0 (+ (* 2 (* 0 0)))) (* 2 (sqrt (sqrt 2)))) into 0
7.039 * [backup-simplify]: Simplify (+ (* 1/2 0) (+ (* 0 0) (+ (* 0 0) (* 0 (sqrt (sqrt 2)))))) into 0
7.041 * [backup-simplify]: Simplify (+ (* (* 1/2 (sqrt (sqrt 2))) 0) (+ (* 0 0) (+ (* 0 0) (* 0 (* 1/2 (sqrt (sqrt 2))))))) into 0
7.042 * [backup-simplify]: Simplify (+ (* 1 0) (* 0 1)) into 0
7.042 * [backup-simplify]: Simplify (+ (* (sqrt 2) 0) (* 0 1)) into 0
7.043 * [backup-simplify]: Simplify (+ (* 1/4 0) (* 0 (sqrt 2))) into 0
7.044 * [backup-simplify]: Simplify (- 0) into 0
7.044 * [backup-simplify]: Simplify (+ 0 0) into 0
7.044 * [backup-simplify]: Simplify 0 into 0
7.046 * [backup-simplify]: Simplify (/ (- 0 (pow 0 2) (+ (* 2 (* 0 0)))) (* 2 (sqrt 2))) into 0
7.048 * [backup-simplify]: Simplify (/ (- 0 (pow 0 2) (+ (* 2 (* 0 0)))) (* 2 (sqrt (sqrt 2)))) into 0
7.049 * [backup-simplify]: Simplify (+ (* 1/2 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (* 0 (sqrt (sqrt 2))))))) into 0
7.051 * [backup-simplify]: Simplify (/ (- 0 (pow 0 2) (+ (* 2 (* 0 0)))) (* 2 (sqrt 2))) into 0
7.052 * [backup-simplify]: Simplify (/ (- 0 (pow 0 2) (+ (* 2 (* 0 0)))) (* 2 (sqrt (sqrt 2)))) into 0
7.054 * [backup-simplify]: Simplify (+ (* 1/2 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (* 0 (sqrt (sqrt 2))))))) into 0
7.056 * [backup-simplify]: Simplify (+ (* (* 1/2 (sqrt (sqrt 2))) 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (* 0 (* 1/2 (sqrt (sqrt 2)))))))) into 0
7.057 * [backup-simplify]: Simplify (+ (* 1 0) (+ (* 0 0) (* 0 1))) into 0
7.058 * [backup-simplify]: Simplify (/ (- 0 (pow 0 2) (+)) (* 2 (sqrt 2))) into 0
7.060 * [backup-simplify]: Simplify (+ (* (sqrt 2) 0) (+ (* 0 0) (* 0 1))) into 0
7.061 * [backup-simplify]: Simplify (+ (* 1/4 0) (+ (* 0 0) (* 0 (sqrt 2)))) into 0
7.061 * [backup-simplify]: Simplify (- 0) into 0
7.061 * [backup-simplify]: Simplify (+ 0 0) into 0
7.062 * [backup-simplify]: Simplify 0 into 0
7.063 * [backup-simplify]: Simplify (/ (- 0 (+ (* 2 (* 0 0)) (* 2 (* 0 0)))) (* 2 (sqrt 2))) into 0
7.064 * [backup-simplify]: Simplify (/ (- 0 (+ (* 2 (* 0 0)) (* 2 (* 0 0)))) (* 2 (sqrt (sqrt 2)))) into 0
7.066 * [backup-simplify]: Simplify (+ (* 1/2 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (* 0 (sqrt (sqrt 2)))))))) into 0
7.067 * [backup-simplify]: Simplify (/ (- 0 (+ (* 2 (* 0 0)) (* 2 (* 0 0)))) (* 2 (sqrt 2))) into 0
7.069 * [backup-simplify]: Simplify (/ (- 0 (+ (* 2 (* 0 0)) (* 2 (* 0 0)))) (* 2 (sqrt (sqrt 2)))) into 0
7.070 * [backup-simplify]: Simplify (+ (* 1/2 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (* 0 (sqrt (sqrt 2)))))))) into 0
7.072 * [backup-simplify]: Simplify (+ (* (* 1/2 (sqrt (sqrt 2))) 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (* 0 (* 1/2 (sqrt (sqrt 2))))))))) into 0
7.074 * [backup-simplify]: Simplify (+ (* 1 0) (+ (* 0 0) (+ (* 0 0) (* 0 1)))) into 0
7.075 * [backup-simplify]: Simplify (/ (- 0 (+ (* 2 (* 0 0)))) (* 2 (sqrt 2))) into 0
7.076 * [backup-simplify]: Simplify (+ (* (sqrt 2) 0) (+ (* 0 0) (+ (* 0 0) (* 0 1)))) into 0
7.077 * [backup-simplify]: Simplify (+ (* 1/4 0) (+ (* 0 0) (+ (* 0 0) (* 0 (sqrt 2))))) into 0
7.078 * [backup-simplify]: Simplify (- 0) into 0
7.078 * [backup-simplify]: Simplify (+ 0 0) into 0
7.078 * [backup-simplify]: Simplify 0 into 0
7.080 * [backup-simplify]: Simplify (/ (- 0 (pow 0 2) (+ (* 2 (* 0 0)) (* 2 (* 0 0)))) (* 2 (sqrt 2))) into 0
7.081 * [backup-simplify]: Simplify (/ (- 0 (pow 0 2) (+ (* 2 (* 0 0)) (* 2 (* 0 0)))) (* 2 (sqrt (sqrt 2)))) into 0
7.083 * [backup-simplify]: Simplify (+ (* 1/2 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (* 0 (sqrt (sqrt 2))))))))) into 0
7.085 * [backup-simplify]: Simplify (/ (- 0 (pow 0 2) (+ (* 2 (* 0 0)) (* 2 (* 0 0)))) (* 2 (sqrt 2))) into 0
7.086 * [backup-simplify]: Simplify (/ (- 0 (pow 0 2) (+ (* 2 (* 0 0)) (* 2 (* 0 0)))) (* 2 (sqrt (sqrt 2)))) into 0
7.088 * [backup-simplify]: Simplify (+ (* 1/2 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (* 0 (sqrt (sqrt 2))))))))) into 0
7.091 * [backup-simplify]: Simplify (+ (* (* 1/2 (sqrt (sqrt 2))) 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (* 0 (* 1/2 (sqrt (sqrt 2)))))))))) into 0
7.092 * [backup-simplify]: Simplify (+ (* 1 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (* 0 1))))) into 0
7.093 * [backup-simplify]: Simplify (/ (- 0 (pow 0 2) (+ (* 2 (* 0 0)))) (* 2 (sqrt 2))) into 0
7.095 * [backup-simplify]: Simplify (+ (* (sqrt 2) 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (* 0 1))))) into 0
7.096 * [backup-simplify]: Simplify (+ (* 1/4 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (* 0 (sqrt 2)))))) into 0
7.097 * [backup-simplify]: Simplify (- 0) into 0
7.098 * [backup-simplify]: Simplify (+ 0 0) into 0
7.098 * [backup-simplify]: Simplify 0 into 0
7.099 * [backup-simplify]: Simplify (/ (- 0 (+ (* 2 (* 0 0)) (* 2 (* 0 0)) (* 2 (* 0 0)))) (* 2 (sqrt 2))) into 0
7.108 * [backup-simplify]: Simplify (/ (- 0 (+ (* 2 (* 0 0)) (* 2 (* 0 0)) (* 2 (* 0 0)))) (* 2 (sqrt (sqrt 2)))) into 0
7.110 * [backup-simplify]: Simplify (+ (* 1/2 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (* 0 (sqrt (sqrt 2)))))))))) into 0
7.112 * [backup-simplify]: Simplify (/ (- 0 (+ (* 2 (* 0 0)) (* 2 (* 0 0)) (* 2 (* 0 0)))) (* 2 (sqrt 2))) into 0
7.113 * [backup-simplify]: Simplify (/ (- 0 (+ (* 2 (* 0 0)) (* 2 (* 0 0)) (* 2 (* 0 0)))) (* 2 (sqrt (sqrt 2)))) into 0
7.115 * [backup-simplify]: Simplify (+ (* 1/2 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (* 0 (sqrt (sqrt 2)))))))))) into 0
7.116 * [backup-simplify]: Simplify (+ (* (* 1/2 (sqrt (sqrt 2))) 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (* 0 (* 1/2 (sqrt (sqrt 2))))))))))) into 0
7.117 * [backup-simplify]: Simplify (+ (* 1 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (* 0 1)))))) into 0
7.118 * [backup-simplify]: Simplify (/ (- 0 (+ (* 2 (* 0 0)) (* 2 (* 0 0)))) (* 2 (sqrt 2))) into 0
7.119 * [backup-simplify]: Simplify (+ (* (sqrt 2) 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (* 0 1)))))) into 0
7.120 * [backup-simplify]: Simplify (+ (* 1/4 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (* 0 (sqrt 2))))))) into 0
7.120 * [backup-simplify]: Simplify (- 0) into 0
7.121 * [backup-simplify]: Simplify (+ 0 0) into 0
7.121 * [backup-simplify]: Simplify 0 into 0
7.122 * [backup-simplify]: Simplify (/ (- 0 (pow 0 2) (+ (* 2 (* 0 0)) (* 2 (* 0 0)) (* 2 (* 0 0)))) (* 2 (sqrt 2))) into 0
7.123 * [backup-simplify]: Simplify (/ (- 0 (pow 0 2) (+ (* 2 (* 0 0)) (* 2 (* 0 0)) (* 2 (* 0 0)))) (* 2 (sqrt (sqrt 2)))) into 0
7.124 * [backup-simplify]: Simplify (+ (* 1/2 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (* 0 (sqrt (sqrt 2))))))))))) into 0
7.125 * [backup-simplify]: Simplify (/ (- 0 (pow 0 2) (+ (* 2 (* 0 0)) (* 2 (* 0 0)) (* 2 (* 0 0)))) (* 2 (sqrt 2))) into 0
7.126 * [backup-simplify]: Simplify (/ (- 0 (pow 0 2) (+ (* 2 (* 0 0)) (* 2 (* 0 0)) (* 2 (* 0 0)))) (* 2 (sqrt (sqrt 2)))) into 0
7.127 * [backup-simplify]: Simplify (+ (* 1/2 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (* 0 (sqrt (sqrt 2))))))))))) into 0
7.129 * [backup-simplify]: Simplify (+ (* (* 1/2 (sqrt (sqrt 2))) 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (* 0 (* 1/2 (sqrt (sqrt 2)))))))))))) into 0
7.130 * [backup-simplify]: Simplify (+ (* 1 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (* 0 1))))))) into 0
7.130 * [backup-simplify]: Simplify (/ (- 0 (pow 0 2) (+ (* 2 (* 0 0)) (* 2 (* 0 0)))) (* 2 (sqrt 2))) into 0
7.131 * [backup-simplify]: Simplify (+ (* (sqrt 2) 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (* 0 1))))))) into 0
7.132 * [backup-simplify]: Simplify (+ (* 1/4 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (* 0 (sqrt 2)))))))) into 0
7.133 * [backup-simplify]: Simplify (- 0) into 0
7.133 * [backup-simplify]: Simplify (+ 0 0) into 0
7.133 * [backup-simplify]: Simplify 0 into 0
7.135 * [backup-simplify]: Simplify (+ (* (- (* 1/4 (sqrt 2))) (pow v 2)) (* 1/4 (sqrt 2))) into (- (* 1/4 (sqrt 2)) (* 1/4 (* (sqrt 2) (pow v 2))))
7.137 * [backup-simplify]: Simplify (fma (sqrt (/ (sqrt 2) 4)) (sqrt (/ (sqrt 2) 4)) (- (* (/ (sqrt 2) 4) (* (/ 1 v) (/ 1 v))))) into (fma (* 1/2 (sqrt (sqrt 2))) (* 1/2 (sqrt (sqrt 2))) (- (* 1/4 (/ (sqrt 2) (pow v 2)))))
7.137 * [approximate]: Taking taylor expansion of (fma (* 1/2 (sqrt (sqrt 2))) (* 1/2 (sqrt (sqrt 2))) (- (* 1/4 (/ (sqrt 2) (pow v 2))))) in (v) around 0
7.137 * [taylor]: Taking taylor expansion of (fma (* 1/2 (sqrt (sqrt 2))) (* 1/2 (sqrt (sqrt 2))) (- (* 1/4 (/ (sqrt 2) (pow v 2))))) in v
7.137 * [taylor]: Rewrote expression to (+ (* (* 1/2 (sqrt (sqrt 2))) (* 1/2 (sqrt (sqrt 2)))) (- (* 1/4 (/ (sqrt 2) (pow v 2)))))
7.137 * [taylor]: Taking taylor expansion of (* (* 1/2 (sqrt (sqrt 2))) (* 1/2 (sqrt (sqrt 2)))) in v
7.137 * [taylor]: Taking taylor expansion of (* 1/2 (sqrt (sqrt 2))) in v
7.137 * [taylor]: Taking taylor expansion of 1/2 in v
7.137 * [backup-simplify]: Simplify 1/2 into 1/2
7.137 * [taylor]: Taking taylor expansion of (sqrt (sqrt 2)) in v
7.137 * [taylor]: Taking taylor expansion of (sqrt 2) in v
7.137 * [taylor]: Taking taylor expansion of 2 in v
7.137 * [backup-simplify]: Simplify 2 into 2
7.138 * [backup-simplify]: Simplify (sqrt 2) into (sqrt 2)
7.138 * [backup-simplify]: Simplify (/ 0 (* 2 (sqrt 2))) into 0
7.139 * [backup-simplify]: Simplify (sqrt (sqrt 2)) into (sqrt (sqrt 2))
7.139 * [backup-simplify]: Simplify (/ 0 (* 2 (sqrt (sqrt 2)))) into 0
7.139 * [taylor]: Taking taylor expansion of (* 1/2 (sqrt (sqrt 2))) in v
7.139 * [taylor]: Taking taylor expansion of 1/2 in v
7.139 * [backup-simplify]: Simplify 1/2 into 1/2
7.139 * [taylor]: Taking taylor expansion of (sqrt (sqrt 2)) in v
7.139 * [taylor]: Taking taylor expansion of (sqrt 2) in v
7.139 * [taylor]: Taking taylor expansion of 2 in v
7.139 * [backup-simplify]: Simplify 2 into 2
7.139 * [backup-simplify]: Simplify (sqrt 2) into (sqrt 2)
7.140 * [backup-simplify]: Simplify (/ 0 (* 2 (sqrt 2))) into 0
7.140 * [backup-simplify]: Simplify (sqrt (sqrt 2)) into (sqrt (sqrt 2))
7.141 * [backup-simplify]: Simplify (/ 0 (* 2 (sqrt (sqrt 2)))) into 0
7.141 * [taylor]: Taking taylor expansion of (- (* 1/4 (/ (sqrt 2) (pow v 2)))) in v
7.141 * [taylor]: Taking taylor expansion of (* 1/4 (/ (sqrt 2) (pow v 2))) in v
7.141 * [taylor]: Taking taylor expansion of 1/4 in v
7.141 * [backup-simplify]: Simplify 1/4 into 1/4
7.141 * [taylor]: Taking taylor expansion of (/ (sqrt 2) (pow v 2)) in v
7.141 * [taylor]: Taking taylor expansion of (sqrt 2) in v
7.141 * [taylor]: Taking taylor expansion of 2 in v
7.141 * [backup-simplify]: Simplify 2 into 2
7.141 * [backup-simplify]: Simplify (sqrt 2) into (sqrt 2)
7.141 * [backup-simplify]: Simplify (/ 0 (* 2 (sqrt 2))) into 0
7.142 * [taylor]: Taking taylor expansion of (pow v 2) in v
7.142 * [taylor]: Taking taylor expansion of v in v
7.142 * [backup-simplify]: Simplify 0 into 0
7.142 * [backup-simplify]: Simplify 1 into 1
7.142 * [backup-simplify]: Simplify (* 1 1) into 1
7.142 * [backup-simplify]: Simplify (/ (sqrt 2) 1) into (sqrt 2)
7.142 * [taylor]: Taking taylor expansion of (fma (* 1/2 (sqrt (sqrt 2))) (* 1/2 (sqrt (sqrt 2))) (- (* 1/4 (/ (sqrt 2) (pow v 2))))) in v
7.142 * [taylor]: Rewrote expression to (+ (* (* 1/2 (sqrt (sqrt 2))) (* 1/2 (sqrt (sqrt 2)))) (- (* 1/4 (/ (sqrt 2) (pow v 2)))))
7.142 * [taylor]: Taking taylor expansion of (* (* 1/2 (sqrt (sqrt 2))) (* 1/2 (sqrt (sqrt 2)))) in v
7.142 * [taylor]: Taking taylor expansion of (* 1/2 (sqrt (sqrt 2))) in v
7.143 * [taylor]: Taking taylor expansion of 1/2 in v
7.143 * [backup-simplify]: Simplify 1/2 into 1/2
7.143 * [taylor]: Taking taylor expansion of (sqrt (sqrt 2)) in v
7.143 * [taylor]: Taking taylor expansion of (sqrt 2) in v
7.143 * [taylor]: Taking taylor expansion of 2 in v
7.143 * [backup-simplify]: Simplify 2 into 2
7.143 * [backup-simplify]: Simplify (sqrt 2) into (sqrt 2)
7.143 * [backup-simplify]: Simplify (/ 0 (* 2 (sqrt 2))) into 0
7.144 * [backup-simplify]: Simplify (sqrt (sqrt 2)) into (sqrt (sqrt 2))
7.144 * [backup-simplify]: Simplify (/ 0 (* 2 (sqrt (sqrt 2)))) into 0
7.144 * [taylor]: Taking taylor expansion of (* 1/2 (sqrt (sqrt 2))) in v
7.144 * [taylor]: Taking taylor expansion of 1/2 in v
7.144 * [backup-simplify]: Simplify 1/2 into 1/2
7.144 * [taylor]: Taking taylor expansion of (sqrt (sqrt 2)) in v
7.144 * [taylor]: Taking taylor expansion of (sqrt 2) in v
7.144 * [taylor]: Taking taylor expansion of 2 in v
7.144 * [backup-simplify]: Simplify 2 into 2
7.145 * [backup-simplify]: Simplify (sqrt 2) into (sqrt 2)
7.145 * [backup-simplify]: Simplify (/ 0 (* 2 (sqrt 2))) into 0
7.145 * [backup-simplify]: Simplify (sqrt (sqrt 2)) into (sqrt (sqrt 2))
7.146 * [backup-simplify]: Simplify (/ 0 (* 2 (sqrt (sqrt 2)))) into 0
7.146 * [taylor]: Taking taylor expansion of (- (* 1/4 (/ (sqrt 2) (pow v 2)))) in v
7.146 * [taylor]: Taking taylor expansion of (* 1/4 (/ (sqrt 2) (pow v 2))) in v
7.146 * [taylor]: Taking taylor expansion of 1/4 in v
7.146 * [backup-simplify]: Simplify 1/4 into 1/4
7.146 * [taylor]: Taking taylor expansion of (/ (sqrt 2) (pow v 2)) in v
7.146 * [taylor]: Taking taylor expansion of (sqrt 2) in v
7.146 * [taylor]: Taking taylor expansion of 2 in v
7.146 * [backup-simplify]: Simplify 2 into 2
7.146 * [backup-simplify]: Simplify (sqrt 2) into (sqrt 2)
7.147 * [backup-simplify]: Simplify (/ 0 (* 2 (sqrt 2))) into 0
7.147 * [taylor]: Taking taylor expansion of (pow v 2) in v
7.147 * [taylor]: Taking taylor expansion of v in v
7.147 * [backup-simplify]: Simplify 0 into 0
7.147 * [backup-simplify]: Simplify 1 into 1
7.147 * [backup-simplify]: Simplify (* 1 1) into 1
7.148 * [backup-simplify]: Simplify (/ (sqrt 2) 1) into (sqrt 2)
7.148 * [backup-simplify]: Simplify (* 1/4 (sqrt 2)) into (* 1/4 (sqrt 2))
7.149 * [backup-simplify]: Simplify (- (* 1/4 (sqrt 2))) into (- (* 1/4 (sqrt 2)))
7.151 * [backup-simplify]: Simplify (+ 0 (- (* 1/4 (sqrt 2)))) into (- (* 1/4 (sqrt 2)))
7.152 * [backup-simplify]: Simplify (- (* 1/4 (sqrt 2))) into (- (* 1/4 (sqrt 2)))
7.152 * [backup-simplify]: Simplify (+ (* 1 0) (* 0 1)) into 0
7.153 * [backup-simplify]: Simplify (- (/ 0 1) (+ (* (sqrt 2) (/ 0 1)))) into 0
7.153 * [backup-simplify]: Simplify (+ (* 1/4 0) (* 0 (sqrt 2))) into 0
7.153 * [backup-simplify]: Simplify (- 0) into 0
7.154 * [backup-simplify]: Simplify (+ 0 0) into 0
7.154 * [backup-simplify]: Simplify 0 into 0
7.155 * [backup-simplify]: Simplify (* 1/2 (sqrt (sqrt 2))) into (* 1/2 (sqrt (sqrt 2)))
7.156 * [backup-simplify]: Simplify (* 1/2 (sqrt (sqrt 2))) into (* 1/2 (sqrt (sqrt 2)))
7.158 * [backup-simplify]: Simplify (* (* 1/2 (sqrt (sqrt 2))) (* 1/2 (sqrt (sqrt 2)))) into (* 1/4 (sqrt 2))
7.159 * [backup-simplify]: Simplify (/ (- 0 (pow 0 2) (+)) (* 2 (sqrt 2))) into 0
7.159 * [backup-simplify]: Simplify (+ (* 1 0) (+ (* 0 0) (* 0 1))) into 0
7.160 * [backup-simplify]: Simplify (- (/ 0 1) (+ (* (sqrt 2) (/ 0 1)) (* 0 (/ 0 1)))) into 0
7.160 * [backup-simplify]: Simplify (+ (* 1/4 0) (+ (* 0 0) (* 0 (sqrt 2)))) into 0
7.161 * [backup-simplify]: Simplify (- 0) into 0
7.162 * [backup-simplify]: Simplify (+ (* 1/4 (sqrt 2)) 0) into (* 1/4 (sqrt 2))
7.163 * [backup-simplify]: Simplify (* 1/4 (sqrt 2)) into (* 1/4 (sqrt 2))
7.164 * [backup-simplify]: Simplify (+ (* 1/2 0) (* 0 (sqrt (sqrt 2)))) into 0
7.164 * [backup-simplify]: Simplify (+ (* 1/2 0) (* 0 (sqrt (sqrt 2)))) into 0
7.165 * [backup-simplify]: Simplify (+ (* (* 1/2 (sqrt (sqrt 2))) 0) (* 0 (* 1/2 (sqrt (sqrt 2))))) into 0
7.165 * [backup-simplify]: Simplify (/ (- 0 (+ (* 2 (* 0 0)))) (* 2 (sqrt 2))) into 0
7.166 * [backup-simplify]: Simplify (+ (* 1 0) (+ (* 0 0) (+ (* 0 0) (* 0 1)))) into 0
7.167 * [backup-simplify]: Simplify (- (/ 0 1) (+ (* (sqrt 2) (/ 0 1)) (* 0 (/ 0 1)) (* 0 (/ 0 1)))) into 0
7.168 * [backup-simplify]: Simplify (+ (* 1/4 0) (+ (* 0 0) (+ (* 0 0) (* 0 (sqrt 2))))) into 0
7.168 * [backup-simplify]: Simplify (- 0) into 0
7.168 * [backup-simplify]: Simplify (+ 0 0) into 0
7.168 * [backup-simplify]: Simplify 0 into 0
7.169 * [backup-simplify]: Simplify (/ (- 0 (pow 0 2) (+)) (* 2 (sqrt 2))) into 0
7.169 * [backup-simplify]: Simplify (/ (- 0 (pow 0 2) (+)) (* 2 (sqrt (sqrt 2)))) into 0
7.170 * [backup-simplify]: Simplify (+ (* 1/2 0) (+ (* 0 0) (* 0 (sqrt (sqrt 2))))) into 0
7.171 * [backup-simplify]: Simplify (/ (- 0 (pow 0 2) (+)) (* 2 (sqrt 2))) into 0
7.172 * [backup-simplify]: Simplify (/ (- 0 (pow 0 2) (+)) (* 2 (sqrt (sqrt 2)))) into 0
7.172 * [backup-simplify]: Simplify (+ (* 1/2 0) (+ (* 0 0) (* 0 (sqrt (sqrt 2))))) into 0
7.173 * [backup-simplify]: Simplify (+ (* (* 1/2 (sqrt (sqrt 2))) 0) (+ (* 0 0) (* 0 (* 1/2 (sqrt (sqrt 2)))))) into 0
7.174 * [backup-simplify]: Simplify (/ (- 0 (pow 0 2) (+ (* 2 (* 0 0)))) (* 2 (sqrt 2))) into 0
7.175 * [backup-simplify]: Simplify (+ (* 1 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (* 0 1))))) into 0
7.175 * [backup-simplify]: Simplify (- (/ 0 1) (+ (* (sqrt 2) (/ 0 1)) (* 0 (/ 0 1)) (* 0 (/ 0 1)) (* 0 (/ 0 1)))) into 0
7.176 * [backup-simplify]: Simplify (+ (* 1/4 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (* 0 (sqrt 2)))))) into 0
7.177 * [backup-simplify]: Simplify (- 0) into 0
7.177 * [backup-simplify]: Simplify (+ 0 0) into 0
7.177 * [backup-simplify]: Simplify 0 into 0
7.178 * [backup-simplify]: Simplify (/ (- 0 (+ (* 2 (* 0 0)))) (* 2 (sqrt 2))) into 0
7.179 * [backup-simplify]: Simplify (/ (- 0 (+ (* 2 (* 0 0)))) (* 2 (sqrt (sqrt 2)))) into 0
7.179 * [backup-simplify]: Simplify (+ (* 1/2 0) (+ (* 0 0) (+ (* 0 0) (* 0 (sqrt (sqrt 2)))))) into 0
7.180 * [backup-simplify]: Simplify (/ (- 0 (+ (* 2 (* 0 0)))) (* 2 (sqrt 2))) into 0
7.181 * [backup-simplify]: Simplify (/ (- 0 (+ (* 2 (* 0 0)))) (* 2 (sqrt (sqrt 2)))) into 0
7.182 * [backup-simplify]: Simplify (+ (* 1/2 0) (+ (* 0 0) (+ (* 0 0) (* 0 (sqrt (sqrt 2)))))) into 0
7.182 * [backup-simplify]: Simplify (+ (* (* 1/2 (sqrt (sqrt 2))) 0) (+ (* 0 0) (+ (* 0 0) (* 0 (* 1/2 (sqrt (sqrt 2))))))) into 0
7.183 * [backup-simplify]: Simplify (/ (- 0 (+ (* 2 (* 0 0)) (* 2 (* 0 0)))) (* 2 (sqrt 2))) into 0
7.184 * [backup-simplify]: Simplify (+ (* 1 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (* 0 1)))))) into 0
7.185 * [backup-simplify]: Simplify (- (/ 0 1) (+ (* (sqrt 2) (/ 0 1)) (* 0 (/ 0 1)) (* 0 (/ 0 1)) (* 0 (/ 0 1)) (* 0 (/ 0 1)))) into 0
7.186 * [backup-simplify]: Simplify (+ (* 1/4 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (* 0 (sqrt 2))))))) into 0
7.186 * [backup-simplify]: Simplify (- 0) into 0
7.186 * [backup-simplify]: Simplify (+ 0 0) into 0
7.186 * [backup-simplify]: Simplify 0 into 0
7.187 * [backup-simplify]: Simplify (/ (- 0 (pow 0 2) (+ (* 2 (* 0 0)))) (* 2 (sqrt 2))) into 0
7.188 * [backup-simplify]: Simplify (/ (- 0 (pow 0 2) (+ (* 2 (* 0 0)))) (* 2 (sqrt (sqrt 2)))) into 0
7.189 * [backup-simplify]: Simplify (+ (* 1/2 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (* 0 (sqrt (sqrt 2))))))) into 0
7.189 * [backup-simplify]: Simplify (/ (- 0 (pow 0 2) (+ (* 2 (* 0 0)))) (* 2 (sqrt 2))) into 0
7.190 * [backup-simplify]: Simplify (/ (- 0 (pow 0 2) (+ (* 2 (* 0 0)))) (* 2 (sqrt (sqrt 2)))) into 0
7.191 * [backup-simplify]: Simplify (+ (* 1/2 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (* 0 (sqrt (sqrt 2))))))) into 0
7.192 * [backup-simplify]: Simplify (+ (* (* 1/2 (sqrt (sqrt 2))) 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (* 0 (* 1/2 (sqrt (sqrt 2)))))))) into 0
7.193 * [backup-simplify]: Simplify (/ (- 0 (pow 0 2) (+ (* 2 (* 0 0)) (* 2 (* 0 0)))) (* 2 (sqrt 2))) into 0
7.194 * [backup-simplify]: Simplify (+ (* 1 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (* 0 1))))))) into 0
7.194 * [backup-simplify]: Simplify (- (/ 0 1) (+ (* (sqrt 2) (/ 0 1)) (* 0 (/ 0 1)) (* 0 (/ 0 1)) (* 0 (/ 0 1)) (* 0 (/ 0 1)) (* 0 (/ 0 1)))) into 0
7.201 * [backup-simplify]: Simplify (+ (* 1/4 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (* 0 (sqrt 2)))))))) into 0
7.201 * [backup-simplify]: Simplify (- 0) into 0
7.201 * [backup-simplify]: Simplify (+ 0 0) into 0
7.201 * [backup-simplify]: Simplify 0 into 0
7.202 * [backup-simplify]: Simplify (/ (- 0 (+ (* 2 (* 0 0)) (* 2 (* 0 0)))) (* 2 (sqrt 2))) into 0
7.203 * [backup-simplify]: Simplify (/ (- 0 (+ (* 2 (* 0 0)) (* 2 (* 0 0)))) (* 2 (sqrt (sqrt 2)))) into 0
7.204 * [backup-simplify]: Simplify (+ (* 1/2 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (* 0 (sqrt (sqrt 2)))))))) into 0
7.205 * [backup-simplify]: Simplify (/ (- 0 (+ (* 2 (* 0 0)) (* 2 (* 0 0)))) (* 2 (sqrt 2))) into 0
7.206 * [backup-simplify]: Simplify (/ (- 0 (+ (* 2 (* 0 0)) (* 2 (* 0 0)))) (* 2 (sqrt (sqrt 2)))) into 0
7.207 * [backup-simplify]: Simplify (+ (* 1/2 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (* 0 (sqrt (sqrt 2)))))))) into 0
7.208 * [backup-simplify]: Simplify (+ (* (* 1/2 (sqrt (sqrt 2))) 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (* 0 (* 1/2 (sqrt (sqrt 2))))))))) into 0
7.209 * [backup-simplify]: Simplify (/ (- 0 (+ (* 2 (* 0 0)) (* 2 (* 0 0)) (* 2 (* 0 0)))) (* 2 (sqrt 2))) into 0
7.210 * [backup-simplify]: Simplify (+ (* 1 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (* 0 1)))))))) into 0
7.210 * [backup-simplify]: Simplify (- (/ 0 1) (+ (* (sqrt 2) (/ 0 1)) (* 0 (/ 0 1)) (* 0 (/ 0 1)) (* 0 (/ 0 1)) (* 0 (/ 0 1)) (* 0 (/ 0 1)) (* 0 (/ 0 1)))) into 0
7.212 * [backup-simplify]: Simplify (+ (* 1/4 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (* 0 (sqrt 2))))))))) into 0
7.212 * [backup-simplify]: Simplify (- 0) into 0
7.212 * [backup-simplify]: Simplify (+ 0 0) into 0
7.212 * [backup-simplify]: Simplify 0 into 0
7.213 * [backup-simplify]: Simplify (/ (- 0 (pow 0 2) (+ (* 2 (* 0 0)) (* 2 (* 0 0)))) (* 2 (sqrt 2))) into 0
7.214 * [backup-simplify]: Simplify (/ (- 0 (pow 0 2) (+ (* 2 (* 0 0)) (* 2 (* 0 0)))) (* 2 (sqrt (sqrt 2)))) into 0
7.215 * [backup-simplify]: Simplify (+ (* 1/2 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (* 0 (sqrt (sqrt 2))))))))) into 0
7.216 * [backup-simplify]: Simplify (/ (- 0 (pow 0 2) (+ (* 2 (* 0 0)) (* 2 (* 0 0)))) (* 2 (sqrt 2))) into 0
7.217 * [backup-simplify]: Simplify (/ (- 0 (pow 0 2) (+ (* 2 (* 0 0)) (* 2 (* 0 0)))) (* 2 (sqrt (sqrt 2)))) into 0
7.218 * [backup-simplify]: Simplify (+ (* 1/2 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (* 0 (sqrt (sqrt 2))))))))) into 0
7.219 * [backup-simplify]: Simplify (+ (* (* 1/2 (sqrt (sqrt 2))) 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (* 0 (* 1/2 (sqrt (sqrt 2)))))))))) into 0
7.220 * [backup-simplify]: Simplify (/ (- 0 (pow 0 2) (+ (* 2 (* 0 0)) (* 2 (* 0 0)) (* 2 (* 0 0)))) (* 2 (sqrt 2))) into 0
7.221 * [backup-simplify]: Simplify (+ (* 1 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (* 0 1))))))))) into 0
7.222 * [backup-simplify]: Simplify (- (/ 0 1) (+ (* (sqrt 2) (/ 0 1)) (* 0 (/ 0 1)) (* 0 (/ 0 1)) (* 0 (/ 0 1)) (* 0 (/ 0 1)) (* 0 (/ 0 1)) (* 0 (/ 0 1)) (* 0 (/ 0 1)))) into 0
7.223 * [backup-simplify]: Simplify (+ (* 1/4 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (* 0 (sqrt 2)))))))))) into 0
7.223 * [backup-simplify]: Simplify (- 0) into 0
7.224 * [backup-simplify]: Simplify (+ 0 0) into 0
7.224 * [backup-simplify]: Simplify 0 into 0
7.225 * [backup-simplify]: Simplify (+ (* 1/4 (sqrt 2)) (* (- (* 1/4 (sqrt 2))) (pow (/ 1 (/ 1 v)) 2))) into (- (* 1/4 (sqrt 2)) (* 1/4 (* (sqrt 2) (pow v 2))))
7.228 * [backup-simplify]: Simplify (fma (sqrt (/ (sqrt 2) 4)) (sqrt (/ (sqrt 2) 4)) (- (* (/ (sqrt 2) 4) (* (/ 1 (- v)) (/ 1 (- v)))))) into (fma (* 1/2 (sqrt (sqrt 2))) (* 1/2 (sqrt (sqrt 2))) (- (* 1/4 (/ (sqrt 2) (pow v 2)))))
7.228 * [approximate]: Taking taylor expansion of (fma (* 1/2 (sqrt (sqrt 2))) (* 1/2 (sqrt (sqrt 2))) (- (* 1/4 (/ (sqrt 2) (pow v 2))))) in (v) around 0
7.228 * [taylor]: Taking taylor expansion of (fma (* 1/2 (sqrt (sqrt 2))) (* 1/2 (sqrt (sqrt 2))) (- (* 1/4 (/ (sqrt 2) (pow v 2))))) in v
7.228 * [taylor]: Rewrote expression to (+ (* (* 1/2 (sqrt (sqrt 2))) (* 1/2 (sqrt (sqrt 2)))) (- (* 1/4 (/ (sqrt 2) (pow v 2)))))
7.228 * [taylor]: Taking taylor expansion of (* (* 1/2 (sqrt (sqrt 2))) (* 1/2 (sqrt (sqrt 2)))) in v
7.228 * [taylor]: Taking taylor expansion of (* 1/2 (sqrt (sqrt 2))) in v
7.228 * [taylor]: Taking taylor expansion of 1/2 in v
7.228 * [backup-simplify]: Simplify 1/2 into 1/2
7.228 * [taylor]: Taking taylor expansion of (sqrt (sqrt 2)) in v
7.228 * [taylor]: Taking taylor expansion of (sqrt 2) in v
7.228 * [taylor]: Taking taylor expansion of 2 in v
7.228 * [backup-simplify]: Simplify 2 into 2
7.228 * [backup-simplify]: Simplify (sqrt 2) into (sqrt 2)
7.229 * [backup-simplify]: Simplify (/ 0 (* 2 (sqrt 2))) into 0
7.229 * [backup-simplify]: Simplify (sqrt (sqrt 2)) into (sqrt (sqrt 2))
7.230 * [backup-simplify]: Simplify (/ 0 (* 2 (sqrt (sqrt 2)))) into 0
7.230 * [taylor]: Taking taylor expansion of (* 1/2 (sqrt (sqrt 2))) in v
7.230 * [taylor]: Taking taylor expansion of 1/2 in v
7.230 * [backup-simplify]: Simplify 1/2 into 1/2
7.230 * [taylor]: Taking taylor expansion of (sqrt (sqrt 2)) in v
7.230 * [taylor]: Taking taylor expansion of (sqrt 2) in v
7.230 * [taylor]: Taking taylor expansion of 2 in v
7.230 * [backup-simplify]: Simplify 2 into 2
7.230 * [backup-simplify]: Simplify (sqrt 2) into (sqrt 2)
7.230 * [backup-simplify]: Simplify (/ 0 (* 2 (sqrt 2))) into 0
7.231 * [backup-simplify]: Simplify (sqrt (sqrt 2)) into (sqrt (sqrt 2))
7.231 * [backup-simplify]: Simplify (/ 0 (* 2 (sqrt (sqrt 2)))) into 0
7.231 * [taylor]: Taking taylor expansion of (- (* 1/4 (/ (sqrt 2) (pow v 2)))) in v
7.231 * [taylor]: Taking taylor expansion of (* 1/4 (/ (sqrt 2) (pow v 2))) in v
7.231 * [taylor]: Taking taylor expansion of 1/4 in v
7.231 * [backup-simplify]: Simplify 1/4 into 1/4
7.232 * [taylor]: Taking taylor expansion of (/ (sqrt 2) (pow v 2)) in v
7.232 * [taylor]: Taking taylor expansion of (sqrt 2) in v
7.232 * [taylor]: Taking taylor expansion of 2 in v
7.232 * [backup-simplify]: Simplify 2 into 2
7.232 * [backup-simplify]: Simplify (sqrt 2) into (sqrt 2)
7.232 * [backup-simplify]: Simplify (/ 0 (* 2 (sqrt 2))) into 0
7.232 * [taylor]: Taking taylor expansion of (pow v 2) in v
7.232 * [taylor]: Taking taylor expansion of v in v
7.232 * [backup-simplify]: Simplify 0 into 0
7.232 * [backup-simplify]: Simplify 1 into 1
7.232 * [backup-simplify]: Simplify (* 1 1) into 1
7.233 * [backup-simplify]: Simplify (/ (sqrt 2) 1) into (sqrt 2)
7.233 * [taylor]: Taking taylor expansion of (fma (* 1/2 (sqrt (sqrt 2))) (* 1/2 (sqrt (sqrt 2))) (- (* 1/4 (/ (sqrt 2) (pow v 2))))) in v
7.233 * [taylor]: Rewrote expression to (+ (* (* 1/2 (sqrt (sqrt 2))) (* 1/2 (sqrt (sqrt 2)))) (- (* 1/4 (/ (sqrt 2) (pow v 2)))))
7.233 * [taylor]: Taking taylor expansion of (* (* 1/2 (sqrt (sqrt 2))) (* 1/2 (sqrt (sqrt 2)))) in v
7.233 * [taylor]: Taking taylor expansion of (* 1/2 (sqrt (sqrt 2))) in v
7.233 * [taylor]: Taking taylor expansion of 1/2 in v
7.233 * [backup-simplify]: Simplify 1/2 into 1/2
7.233 * [taylor]: Taking taylor expansion of (sqrt (sqrt 2)) in v
7.233 * [taylor]: Taking taylor expansion of (sqrt 2) in v
7.233 * [taylor]: Taking taylor expansion of 2 in v
7.233 * [backup-simplify]: Simplify 2 into 2
7.234 * [backup-simplify]: Simplify (sqrt 2) into (sqrt 2)
7.234 * [backup-simplify]: Simplify (/ 0 (* 2 (sqrt 2))) into 0
7.234 * [backup-simplify]: Simplify (sqrt (sqrt 2)) into (sqrt (sqrt 2))
7.235 * [backup-simplify]: Simplify (/ 0 (* 2 (sqrt (sqrt 2)))) into 0
7.235 * [taylor]: Taking taylor expansion of (* 1/2 (sqrt (sqrt 2))) in v
7.235 * [taylor]: Taking taylor expansion of 1/2 in v
7.235 * [backup-simplify]: Simplify 1/2 into 1/2
7.235 * [taylor]: Taking taylor expansion of (sqrt (sqrt 2)) in v
7.235 * [taylor]: Taking taylor expansion of (sqrt 2) in v
7.235 * [taylor]: Taking taylor expansion of 2 in v
7.235 * [backup-simplify]: Simplify 2 into 2
7.235 * [backup-simplify]: Simplify (sqrt 2) into (sqrt 2)
7.236 * [backup-simplify]: Simplify (/ 0 (* 2 (sqrt 2))) into 0
7.236 * [backup-simplify]: Simplify (sqrt (sqrt 2)) into (sqrt (sqrt 2))
7.237 * [backup-simplify]: Simplify (/ 0 (* 2 (sqrt (sqrt 2)))) into 0
7.237 * [taylor]: Taking taylor expansion of (- (* 1/4 (/ (sqrt 2) (pow v 2)))) in v
7.237 * [taylor]: Taking taylor expansion of (* 1/4 (/ (sqrt 2) (pow v 2))) in v
7.237 * [taylor]: Taking taylor expansion of 1/4 in v
7.237 * [backup-simplify]: Simplify 1/4 into 1/4
7.237 * [taylor]: Taking taylor expansion of (/ (sqrt 2) (pow v 2)) in v
7.237 * [taylor]: Taking taylor expansion of (sqrt 2) in v
7.237 * [taylor]: Taking taylor expansion of 2 in v
7.237 * [backup-simplify]: Simplify 2 into 2
7.237 * [backup-simplify]: Simplify (sqrt 2) into (sqrt 2)
7.237 * [backup-simplify]: Simplify (/ 0 (* 2 (sqrt 2))) into 0
7.237 * [taylor]: Taking taylor expansion of (pow v 2) in v
7.237 * [taylor]: Taking taylor expansion of v in v
7.237 * [backup-simplify]: Simplify 0 into 0
7.237 * [backup-simplify]: Simplify 1 into 1
7.238 * [backup-simplify]: Simplify (* 1 1) into 1
7.238 * [backup-simplify]: Simplify (/ (sqrt 2) 1) into (sqrt 2)
7.239 * [backup-simplify]: Simplify (* 1/4 (sqrt 2)) into (* 1/4 (sqrt 2))
7.240 * [backup-simplify]: Simplify (- (* 1/4 (sqrt 2))) into (- (* 1/4 (sqrt 2)))
7.241 * [backup-simplify]: Simplify (+ 0 (- (* 1/4 (sqrt 2)))) into (- (* 1/4 (sqrt 2)))
7.242 * [backup-simplify]: Simplify (- (* 1/4 (sqrt 2))) into (- (* 1/4 (sqrt 2)))
7.243 * [backup-simplify]: Simplify (+ (* 1 0) (* 0 1)) into 0
7.244 * [backup-simplify]: Simplify (- (/ 0 1) (+ (* (sqrt 2) (/ 0 1)))) into 0
7.245 * [backup-simplify]: Simplify (+ (* 1/4 0) (* 0 (sqrt 2))) into 0
7.245 * [backup-simplify]: Simplify (- 0) into 0
7.245 * [backup-simplify]: Simplify (+ 0 0) into 0
7.245 * [backup-simplify]: Simplify 0 into 0
7.247 * [backup-simplify]: Simplify (* 1/2 (sqrt (sqrt 2))) into (* 1/2 (sqrt (sqrt 2)))
7.248 * [backup-simplify]: Simplify (* 1/2 (sqrt (sqrt 2))) into (* 1/2 (sqrt (sqrt 2)))
7.250 * [backup-simplify]: Simplify (* (* 1/2 (sqrt (sqrt 2))) (* 1/2 (sqrt (sqrt 2)))) into (* 1/4 (sqrt 2))
7.250 * [backup-simplify]: Simplify (/ (- 0 (pow 0 2) (+)) (* 2 (sqrt 2))) into 0
7.251 * [backup-simplify]: Simplify (+ (* 1 0) (+ (* 0 0) (* 0 1))) into 0
7.252 * [backup-simplify]: Simplify (- (/ 0 1) (+ (* (sqrt 2) (/ 0 1)) (* 0 (/ 0 1)))) into 0
7.252 * [backup-simplify]: Simplify (+ (* 1/4 0) (+ (* 0 0) (* 0 (sqrt 2)))) into 0
7.253 * [backup-simplify]: Simplify (- 0) into 0
7.254 * [backup-simplify]: Simplify (+ (* 1/4 (sqrt 2)) 0) into (* 1/4 (sqrt 2))
7.254 * [backup-simplify]: Simplify (* 1/4 (sqrt 2)) into (* 1/4 (sqrt 2))
7.255 * [backup-simplify]: Simplify (+ (* 1/2 0) (* 0 (sqrt (sqrt 2)))) into 0
7.255 * [backup-simplify]: Simplify (+ (* 1/2 0) (* 0 (sqrt (sqrt 2)))) into 0
7.256 * [backup-simplify]: Simplify (+ (* (* 1/2 (sqrt (sqrt 2))) 0) (* 0 (* 1/2 (sqrt (sqrt 2))))) into 0
7.257 * [backup-simplify]: Simplify (/ (- 0 (+ (* 2 (* 0 0)))) (* 2 (sqrt 2))) into 0
7.257 * [backup-simplify]: Simplify (+ (* 1 0) (+ (* 0 0) (+ (* 0 0) (* 0 1)))) into 0
7.258 * [backup-simplify]: Simplify (- (/ 0 1) (+ (* (sqrt 2) (/ 0 1)) (* 0 (/ 0 1)) (* 0 (/ 0 1)))) into 0
7.259 * [backup-simplify]: Simplify (+ (* 1/4 0) (+ (* 0 0) (+ (* 0 0) (* 0 (sqrt 2))))) into 0
7.259 * [backup-simplify]: Simplify (- 0) into 0
7.259 * [backup-simplify]: Simplify (+ 0 0) into 0
7.259 * [backup-simplify]: Simplify 0 into 0
7.260 * [backup-simplify]: Simplify (/ (- 0 (pow 0 2) (+)) (* 2 (sqrt 2))) into 0
7.261 * [backup-simplify]: Simplify (/ (- 0 (pow 0 2) (+)) (* 2 (sqrt (sqrt 2)))) into 0
7.261 * [backup-simplify]: Simplify (+ (* 1/2 0) (+ (* 0 0) (* 0 (sqrt (sqrt 2))))) into 0
7.262 * [backup-simplify]: Simplify (/ (- 0 (pow 0 2) (+)) (* 2 (sqrt 2))) into 0
7.263 * [backup-simplify]: Simplify (/ (- 0 (pow 0 2) (+)) (* 2 (sqrt (sqrt 2)))) into 0
7.263 * [backup-simplify]: Simplify (+ (* 1/2 0) (+ (* 0 0) (* 0 (sqrt (sqrt 2))))) into 0
7.264 * [backup-simplify]: Simplify (+ (* (* 1/2 (sqrt (sqrt 2))) 0) (+ (* 0 0) (* 0 (* 1/2 (sqrt (sqrt 2)))))) into 0
7.265 * [backup-simplify]: Simplify (/ (- 0 (pow 0 2) (+ (* 2 (* 0 0)))) (* 2 (sqrt 2))) into 0
7.266 * [backup-simplify]: Simplify (+ (* 1 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (* 0 1))))) into 0
7.266 * [backup-simplify]: Simplify (- (/ 0 1) (+ (* (sqrt 2) (/ 0 1)) (* 0 (/ 0 1)) (* 0 (/ 0 1)) (* 0 (/ 0 1)))) into 0
7.267 * [backup-simplify]: Simplify (+ (* 1/4 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (* 0 (sqrt 2)))))) into 0
7.267 * [backup-simplify]: Simplify (- 0) into 0
7.268 * [backup-simplify]: Simplify (+ 0 0) into 0
7.268 * [backup-simplify]: Simplify 0 into 0
7.268 * [backup-simplify]: Simplify (/ (- 0 (+ (* 2 (* 0 0)))) (* 2 (sqrt 2))) into 0
7.269 * [backup-simplify]: Simplify (/ (- 0 (+ (* 2 (* 0 0)))) (* 2 (sqrt (sqrt 2)))) into 0
7.270 * [backup-simplify]: Simplify (+ (* 1/2 0) (+ (* 0 0) (+ (* 0 0) (* 0 (sqrt (sqrt 2)))))) into 0
7.271 * [backup-simplify]: Simplify (/ (- 0 (+ (* 2 (* 0 0)))) (* 2 (sqrt 2))) into 0
7.271 * [backup-simplify]: Simplify (/ (- 0 (+ (* 2 (* 0 0)))) (* 2 (sqrt (sqrt 2)))) into 0
7.272 * [backup-simplify]: Simplify (+ (* 1/2 0) (+ (* 0 0) (+ (* 0 0) (* 0 (sqrt (sqrt 2)))))) into 0
7.273 * [backup-simplify]: Simplify (+ (* (* 1/2 (sqrt (sqrt 2))) 0) (+ (* 0 0) (+ (* 0 0) (* 0 (* 1/2 (sqrt (sqrt 2))))))) into 0
7.274 * [backup-simplify]: Simplify (/ (- 0 (+ (* 2 (* 0 0)) (* 2 (* 0 0)))) (* 2 (sqrt 2))) into 0
7.275 * [backup-simplify]: Simplify (+ (* 1 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (* 0 1)))))) into 0
7.275 * [backup-simplify]: Simplify (- (/ 0 1) (+ (* (sqrt 2) (/ 0 1)) (* 0 (/ 0 1)) (* 0 (/ 0 1)) (* 0 (/ 0 1)) (* 0 (/ 0 1)))) into 0
7.276 * [backup-simplify]: Simplify (+ (* 1/4 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (* 0 (sqrt 2))))))) into 0
7.276 * [backup-simplify]: Simplify (- 0) into 0
7.277 * [backup-simplify]: Simplify (+ 0 0) into 0
7.277 * [backup-simplify]: Simplify 0 into 0
7.278 * [backup-simplify]: Simplify (/ (- 0 (pow 0 2) (+ (* 2 (* 0 0)))) (* 2 (sqrt 2))) into 0
7.279 * [backup-simplify]: Simplify (/ (- 0 (pow 0 2) (+ (* 2 (* 0 0)))) (* 2 (sqrt (sqrt 2)))) into 0
7.279 * [backup-simplify]: Simplify (+ (* 1/2 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (* 0 (sqrt (sqrt 2))))))) into 0
7.280 * [backup-simplify]: Simplify (/ (- 0 (pow 0 2) (+ (* 2 (* 0 0)))) (* 2 (sqrt 2))) into 0
7.281 * [backup-simplify]: Simplify (/ (- 0 (pow 0 2) (+ (* 2 (* 0 0)))) (* 2 (sqrt (sqrt 2)))) into 0
7.282 * [backup-simplify]: Simplify (+ (* 1/2 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (* 0 (sqrt (sqrt 2))))))) into 0
7.283 * [backup-simplify]: Simplify (+ (* (* 1/2 (sqrt (sqrt 2))) 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (* 0 (* 1/2 (sqrt (sqrt 2)))))))) into 0
7.284 * [backup-simplify]: Simplify (/ (- 0 (pow 0 2) (+ (* 2 (* 0 0)) (* 2 (* 0 0)))) (* 2 (sqrt 2))) into 0
7.285 * [backup-simplify]: Simplify (+ (* 1 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (* 0 1))))))) into 0
7.291 * [backup-simplify]: Simplify (- (/ 0 1) (+ (* (sqrt 2) (/ 0 1)) (* 0 (/ 0 1)) (* 0 (/ 0 1)) (* 0 (/ 0 1)) (* 0 (/ 0 1)) (* 0 (/ 0 1)))) into 0
7.292 * [backup-simplify]: Simplify (+ (* 1/4 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (* 0 (sqrt 2)))))))) into 0
7.293 * [backup-simplify]: Simplify (- 0) into 0
7.293 * [backup-simplify]: Simplify (+ 0 0) into 0
7.293 * [backup-simplify]: Simplify 0 into 0
7.294 * [backup-simplify]: Simplify (/ (- 0 (+ (* 2 (* 0 0)) (* 2 (* 0 0)))) (* 2 (sqrt 2))) into 0
7.295 * [backup-simplify]: Simplify (/ (- 0 (+ (* 2 (* 0 0)) (* 2 (* 0 0)))) (* 2 (sqrt (sqrt 2)))) into 0
7.296 * [backup-simplify]: Simplify (+ (* 1/2 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (* 0 (sqrt (sqrt 2)))))))) into 0
7.297 * [backup-simplify]: Simplify (/ (- 0 (+ (* 2 (* 0 0)) (* 2 (* 0 0)))) (* 2 (sqrt 2))) into 0
7.298 * [backup-simplify]: Simplify (/ (- 0 (+ (* 2 (* 0 0)) (* 2 (* 0 0)))) (* 2 (sqrt (sqrt 2)))) into 0
7.299 * [backup-simplify]: Simplify (+ (* 1/2 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (* 0 (sqrt (sqrt 2)))))))) into 0
7.300 * [backup-simplify]: Simplify (+ (* (* 1/2 (sqrt (sqrt 2))) 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (* 0 (* 1/2 (sqrt (sqrt 2))))))))) into 0
7.301 * [backup-simplify]: Simplify (/ (- 0 (+ (* 2 (* 0 0)) (* 2 (* 0 0)) (* 2 (* 0 0)))) (* 2 (sqrt 2))) into 0
7.302 * [backup-simplify]: Simplify (+ (* 1 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (* 0 1)))))))) into 0
7.303 * [backup-simplify]: Simplify (- (/ 0 1) (+ (* (sqrt 2) (/ 0 1)) (* 0 (/ 0 1)) (* 0 (/ 0 1)) (* 0 (/ 0 1)) (* 0 (/ 0 1)) (* 0 (/ 0 1)) (* 0 (/ 0 1)))) into 0
7.304 * [backup-simplify]: Simplify (+ (* 1/4 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (* 0 (sqrt 2))))))))) into 0
7.304 * [backup-simplify]: Simplify (- 0) into 0
7.304 * [backup-simplify]: Simplify (+ 0 0) into 0
7.304 * [backup-simplify]: Simplify 0 into 0
7.305 * [backup-simplify]: Simplify (/ (- 0 (pow 0 2) (+ (* 2 (* 0 0)) (* 2 (* 0 0)))) (* 2 (sqrt 2))) into 0
7.306 * [backup-simplify]: Simplify (/ (- 0 (pow 0 2) (+ (* 2 (* 0 0)) (* 2 (* 0 0)))) (* 2 (sqrt (sqrt 2)))) into 0
7.307 * [backup-simplify]: Simplify (+ (* 1/2 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (* 0 (sqrt (sqrt 2))))))))) into 0
7.309 * [backup-simplify]: Simplify (/ (- 0 (pow 0 2) (+ (* 2 (* 0 0)) (* 2 (* 0 0)))) (* 2 (sqrt 2))) into 0
7.310 * [backup-simplify]: Simplify (/ (- 0 (pow 0 2) (+ (* 2 (* 0 0)) (* 2 (* 0 0)))) (* 2 (sqrt (sqrt 2)))) into 0
7.312 * [backup-simplify]: Simplify (+ (* 1/2 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (* 0 (sqrt (sqrt 2))))))))) into 0
7.315 * [backup-simplify]: Simplify (+ (* (* 1/2 (sqrt (sqrt 2))) 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (* 0 (* 1/2 (sqrt (sqrt 2)))))))))) into 0
7.316 * [backup-simplify]: Simplify (/ (- 0 (pow 0 2) (+ (* 2 (* 0 0)) (* 2 (* 0 0)) (* 2 (* 0 0)))) (* 2 (sqrt 2))) into 0
7.318 * [backup-simplify]: Simplify (+ (* 1 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (* 0 1))))))))) into 0
7.319 * [backup-simplify]: Simplify (- (/ 0 1) (+ (* (sqrt 2) (/ 0 1)) (* 0 (/ 0 1)) (* 0 (/ 0 1)) (* 0 (/ 0 1)) (* 0 (/ 0 1)) (* 0 (/ 0 1)) (* 0 (/ 0 1)) (* 0 (/ 0 1)))) into 0
7.321 * [backup-simplify]: Simplify (+ (* 1/4 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (* 0 (sqrt 2)))))))))) into 0
7.322 * [backup-simplify]: Simplify (- 0) into 0
7.322 * [backup-simplify]: Simplify (+ 0 0) into 0
7.322 * [backup-simplify]: Simplify 0 into 0
7.325 * [backup-simplify]: Simplify (+ (* 1/4 (sqrt 2)) (* (- (* 1/4 (sqrt 2))) (pow (/ 1 (/ 1 (- v))) 2))) into (- (* 1/4 (sqrt 2)) (* 1/4 (* (sqrt 2) (pow v 2))))
7.325 * * * * [progress]: [ 2 / 2 ] generating series at (2 1 3 1)
7.325 * [backup-simplify]: Simplify (* (/ (sqrt 2) 4) (* v v)) into (* 1/4 (* (sqrt 2) (pow v 2)))
7.326 * [approximate]: Taking taylor expansion of (* 1/4 (* (sqrt 2) (pow v 2))) in (v) around 0
7.326 * [taylor]: Taking taylor expansion of (* 1/4 (* (sqrt 2) (pow v 2))) in v
7.326 * [taylor]: Taking taylor expansion of 1/4 in v
7.326 * [backup-simplify]: Simplify 1/4 into 1/4
7.326 * [taylor]: Taking taylor expansion of (* (sqrt 2) (pow v 2)) in v
7.326 * [taylor]: Taking taylor expansion of (sqrt 2) in v
7.326 * [taylor]: Taking taylor expansion of 2 in v
7.326 * [backup-simplify]: Simplify 2 into 2
7.326 * [backup-simplify]: Simplify (sqrt 2) into (sqrt 2)
7.327 * [backup-simplify]: Simplify (/ 0 (* 2 (sqrt 2))) into 0
7.327 * [taylor]: Taking taylor expansion of (pow v 2) in v
7.327 * [taylor]: Taking taylor expansion of v in v
7.327 * [backup-simplify]: Simplify 0 into 0
7.327 * [backup-simplify]: Simplify 1 into 1
7.327 * [taylor]: Taking taylor expansion of (* 1/4 (* (sqrt 2) (pow v 2))) in v
7.327 * [taylor]: Taking taylor expansion of 1/4 in v
7.327 * [backup-simplify]: Simplify 1/4 into 1/4
7.327 * [taylor]: Taking taylor expansion of (* (sqrt 2) (pow v 2)) in v
7.327 * [taylor]: Taking taylor expansion of (sqrt 2) in v
7.327 * [taylor]: Taking taylor expansion of 2 in v
7.327 * [backup-simplify]: Simplify 2 into 2
7.327 * [backup-simplify]: Simplify (sqrt 2) into (sqrt 2)
7.328 * [backup-simplify]: Simplify (/ 0 (* 2 (sqrt 2))) into 0
7.328 * [taylor]: Taking taylor expansion of (pow v 2) in v
7.328 * [taylor]: Taking taylor expansion of v in v
7.328 * [backup-simplify]: Simplify 0 into 0
7.328 * [backup-simplify]: Simplify 1 into 1
7.328 * [backup-simplify]: Simplify (* 1 1) into 1
7.329 * [backup-simplify]: Simplify (* (sqrt 2) 1) into (sqrt 2)
7.330 * [backup-simplify]: Simplify (* 1/4 (sqrt 2)) into (* 1/4 (sqrt 2))
7.331 * [backup-simplify]: Simplify (* 1/4 (sqrt 2)) into (* 1/4 (sqrt 2))
7.332 * [backup-simplify]: Simplify (+ (* 1 0) (* 0 1)) into 0
7.332 * [backup-simplify]: Simplify (+ (* (sqrt 2) 0) (* 0 1)) into 0
7.333 * [backup-simplify]: Simplify (+ (* 1/4 0) (* 0 (sqrt 2))) into 0
7.333 * [backup-simplify]: Simplify 0 into 0
7.334 * [backup-simplify]: Simplify (+ (* 1 0) (+ (* 0 0) (* 0 1))) into 0
7.335 * [backup-simplify]: Simplify (/ (- 0 (pow 0 2) (+)) (* 2 (sqrt 2))) into 0
7.336 * [backup-simplify]: Simplify (+ (* (sqrt 2) 0) (+ (* 0 0) (* 0 1))) into 0
7.338 * [backup-simplify]: Simplify (+ (* 1/4 0) (+ (* 0 0) (* 0 (sqrt 2)))) into 0
7.338 * [backup-simplify]: Simplify 0 into 0
7.339 * [backup-simplify]: Simplify (+ (* 1 0) (+ (* 0 0) (+ (* 0 0) (* 0 1)))) into 0
7.340 * [backup-simplify]: Simplify (/ (- 0 (+ (* 2 (* 0 0)))) (* 2 (sqrt 2))) into 0
7.341 * [backup-simplify]: Simplify (+ (* (sqrt 2) 0) (+ (* 0 0) (+ (* 0 0) (* 0 1)))) into 0
7.342 * [backup-simplify]: Simplify (+ (* 1/4 0) (+ (* 0 0) (+ (* 0 0) (* 0 (sqrt 2))))) into 0
7.342 * [backup-simplify]: Simplify 0 into 0
7.344 * [backup-simplify]: Simplify (+ (* 1 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (* 0 1))))) into 0
7.345 * [backup-simplify]: Simplify (/ (- 0 (pow 0 2) (+ (* 2 (* 0 0)))) (* 2 (sqrt 2))) into 0
7.346 * [backup-simplify]: Simplify (+ (* (sqrt 2) 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (* 0 1))))) into 0
7.347 * [backup-simplify]: Simplify (+ (* 1/4 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (* 0 (sqrt 2)))))) into 0
7.347 * [backup-simplify]: Simplify 0 into 0
7.348 * [backup-simplify]: Simplify (+ (* 1 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (* 0 1)))))) into 0
7.349 * [backup-simplify]: Simplify (/ (- 0 (+ (* 2 (* 0 0)) (* 2 (* 0 0)))) (* 2 (sqrt 2))) into 0
7.350 * [backup-simplify]: Simplify (+ (* (sqrt 2) 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (* 0 1)))))) into 0
7.351 * [backup-simplify]: Simplify (+ (* 1/4 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (* 0 (sqrt 2))))))) into 0
7.351 * [backup-simplify]: Simplify 0 into 0
7.352 * [backup-simplify]: Simplify (+ (* 1 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (* 0 1))))))) into 0
7.352 * [backup-simplify]: Simplify (/ (- 0 (pow 0 2) (+ (* 2 (* 0 0)) (* 2 (* 0 0)))) (* 2 (sqrt 2))) into 0
7.353 * [backup-simplify]: Simplify (+ (* (sqrt 2) 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (* 0 1))))))) into 0
7.354 * [backup-simplify]: Simplify (+ (* 1/4 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (* 0 (sqrt 2)))))))) into 0
7.354 * [backup-simplify]: Simplify 0 into 0
7.356 * [backup-simplify]: Simplify (* (* 1/4 (sqrt 2)) (pow v 2)) into (* 1/4 (* (sqrt 2) (pow v 2)))
7.357 * [backup-simplify]: Simplify (* (/ (sqrt 2) 4) (* (/ 1 v) (/ 1 v))) into (* 1/4 (/ (sqrt 2) (pow v 2)))
7.357 * [approximate]: Taking taylor expansion of (* 1/4 (/ (sqrt 2) (pow v 2))) in (v) around 0
7.357 * [taylor]: Taking taylor expansion of (* 1/4 (/ (sqrt 2) (pow v 2))) in v
7.357 * [taylor]: Taking taylor expansion of 1/4 in v
7.357 * [backup-simplify]: Simplify 1/4 into 1/4
7.357 * [taylor]: Taking taylor expansion of (/ (sqrt 2) (pow v 2)) in v
7.357 * [taylor]: Taking taylor expansion of (sqrt 2) in v
7.357 * [taylor]: Taking taylor expansion of 2 in v
7.357 * [backup-simplify]: Simplify 2 into 2
7.357 * [backup-simplify]: Simplify (sqrt 2) into (sqrt 2)
7.357 * [backup-simplify]: Simplify (/ 0 (* 2 (sqrt 2))) into 0
7.357 * [taylor]: Taking taylor expansion of (pow v 2) in v
7.357 * [taylor]: Taking taylor expansion of v in v
7.357 * [backup-simplify]: Simplify 0 into 0
7.357 * [backup-simplify]: Simplify 1 into 1
7.358 * [backup-simplify]: Simplify (* 1 1) into 1
7.358 * [backup-simplify]: Simplify (/ (sqrt 2) 1) into (sqrt 2)
7.358 * [taylor]: Taking taylor expansion of (* 1/4 (/ (sqrt 2) (pow v 2))) in v
7.358 * [taylor]: Taking taylor expansion of 1/4 in v
7.358 * [backup-simplify]: Simplify 1/4 into 1/4
7.358 * [taylor]: Taking taylor expansion of (/ (sqrt 2) (pow v 2)) in v
7.358 * [taylor]: Taking taylor expansion of (sqrt 2) in v
7.358 * [taylor]: Taking taylor expansion of 2 in v
7.358 * [backup-simplify]: Simplify 2 into 2
7.359 * [backup-simplify]: Simplify (sqrt 2) into (sqrt 2)
7.359 * [backup-simplify]: Simplify (/ 0 (* 2 (sqrt 2))) into 0
7.359 * [taylor]: Taking taylor expansion of (pow v 2) in v
7.359 * [taylor]: Taking taylor expansion of v in v
7.359 * [backup-simplify]: Simplify 0 into 0
7.359 * [backup-simplify]: Simplify 1 into 1
7.359 * [backup-simplify]: Simplify (* 1 1) into 1
7.360 * [backup-simplify]: Simplify (/ (sqrt 2) 1) into (sqrt 2)
7.360 * [backup-simplify]: Simplify (* 1/4 (sqrt 2)) into (* 1/4 (sqrt 2))
7.361 * [backup-simplify]: Simplify (* 1/4 (sqrt 2)) into (* 1/4 (sqrt 2))
7.361 * [backup-simplify]: Simplify (+ (* 1 0) (* 0 1)) into 0
7.362 * [backup-simplify]: Simplify (- (/ 0 1) (+ (* (sqrt 2) (/ 0 1)))) into 0
7.363 * [backup-simplify]: Simplify (+ (* 1/4 0) (* 0 (sqrt 2))) into 0
7.363 * [backup-simplify]: Simplify 0 into 0
7.363 * [backup-simplify]: Simplify (/ (- 0 (pow 0 2) (+)) (* 2 (sqrt 2))) into 0
7.364 * [backup-simplify]: Simplify (+ (* 1 0) (+ (* 0 0) (* 0 1))) into 0
7.365 * [backup-simplify]: Simplify (- (/ 0 1) (+ (* (sqrt 2) (/ 0 1)) (* 0 (/ 0 1)))) into 0
7.365 * [backup-simplify]: Simplify (+ (* 1/4 0) (+ (* 0 0) (* 0 (sqrt 2)))) into 0
7.365 * [backup-simplify]: Simplify 0 into 0
7.366 * [backup-simplify]: Simplify (/ (- 0 (+ (* 2 (* 0 0)))) (* 2 (sqrt 2))) into 0
7.367 * [backup-simplify]: Simplify (+ (* 1 0) (+ (* 0 0) (+ (* 0 0) (* 0 1)))) into 0
7.367 * [backup-simplify]: Simplify (- (/ 0 1) (+ (* (sqrt 2) (/ 0 1)) (* 0 (/ 0 1)) (* 0 (/ 0 1)))) into 0
7.368 * [backup-simplify]: Simplify (+ (* 1/4 0) (+ (* 0 0) (+ (* 0 0) (* 0 (sqrt 2))))) into 0
7.368 * [backup-simplify]: Simplify 0 into 0
7.369 * [backup-simplify]: Simplify (/ (- 0 (pow 0 2) (+ (* 2 (* 0 0)))) (* 2 (sqrt 2))) into 0
7.370 * [backup-simplify]: Simplify (+ (* 1 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (* 0 1))))) into 0
7.371 * [backup-simplify]: Simplify (- (/ 0 1) (+ (* (sqrt 2) (/ 0 1)) (* 0 (/ 0 1)) (* 0 (/ 0 1)) (* 0 (/ 0 1)))) into 0
7.371 * [backup-simplify]: Simplify (+ (* 1/4 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (* 0 (sqrt 2)))))) into 0
7.371 * [backup-simplify]: Simplify 0 into 0
7.372 * [backup-simplify]: Simplify (/ (- 0 (+ (* 2 (* 0 0)) (* 2 (* 0 0)))) (* 2 (sqrt 2))) into 0
7.373 * [backup-simplify]: Simplify (+ (* 1 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (* 0 1)))))) into 0
7.373 * [backup-simplify]: Simplify (- (/ 0 1) (+ (* (sqrt 2) (/ 0 1)) (* 0 (/ 0 1)) (* 0 (/ 0 1)) (* 0 (/ 0 1)) (* 0 (/ 0 1)))) into 0
7.374 * [backup-simplify]: Simplify (+ (* 1/4 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (* 0 (sqrt 2))))))) into 0
7.374 * [backup-simplify]: Simplify 0 into 0
7.375 * [backup-simplify]: Simplify (/ (- 0 (pow 0 2) (+ (* 2 (* 0 0)) (* 2 (* 0 0)))) (* 2 (sqrt 2))) into 0
7.376 * [backup-simplify]: Simplify (+ (* 1 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (* 0 1))))))) into 0
7.377 * [backup-simplify]: Simplify (- (/ 0 1) (+ (* (sqrt 2) (/ 0 1)) (* 0 (/ 0 1)) (* 0 (/ 0 1)) (* 0 (/ 0 1)) (* 0 (/ 0 1)) (* 0 (/ 0 1)))) into 0
7.378 * [backup-simplify]: Simplify (+ (* 1/4 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (* 0 (sqrt 2)))))))) into 0
7.378 * [backup-simplify]: Simplify 0 into 0
7.378 * [backup-simplify]: Simplify (* (* 1/4 (sqrt 2)) (pow (/ 1 (/ 1 v)) 2)) into (* 1/4 (* (sqrt 2) (pow v 2)))
7.379 * [backup-simplify]: Simplify (* (/ (sqrt 2) 4) (* (/ 1 (- v)) (/ 1 (- v)))) into (* 1/4 (/ (sqrt 2) (pow v 2)))
7.379 * [approximate]: Taking taylor expansion of (* 1/4 (/ (sqrt 2) (pow v 2))) in (v) around 0
7.380 * [taylor]: Taking taylor expansion of (* 1/4 (/ (sqrt 2) (pow v 2))) in v
7.380 * [taylor]: Taking taylor expansion of 1/4 in v
7.380 * [backup-simplify]: Simplify 1/4 into 1/4
7.380 * [taylor]: Taking taylor expansion of (/ (sqrt 2) (pow v 2)) in v
7.380 * [taylor]: Taking taylor expansion of (sqrt 2) in v
7.380 * [taylor]: Taking taylor expansion of 2 in v
7.380 * [backup-simplify]: Simplify 2 into 2
7.380 * [backup-simplify]: Simplify (sqrt 2) into (sqrt 2)
7.381 * [backup-simplify]: Simplify (/ 0 (* 2 (sqrt 2))) into 0
7.381 * [taylor]: Taking taylor expansion of (pow v 2) in v
7.381 * [taylor]: Taking taylor expansion of v in v
7.381 * [backup-simplify]: Simplify 0 into 0
7.381 * [backup-simplify]: Simplify 1 into 1
7.381 * [backup-simplify]: Simplify (* 1 1) into 1
7.382 * [backup-simplify]: Simplify (/ (sqrt 2) 1) into (sqrt 2)
7.382 * [taylor]: Taking taylor expansion of (* 1/4 (/ (sqrt 2) (pow v 2))) in v
7.382 * [taylor]: Taking taylor expansion of 1/4 in v
7.382 * [backup-simplify]: Simplify 1/4 into 1/4
7.382 * [taylor]: Taking taylor expansion of (/ (sqrt 2) (pow v 2)) in v
7.382 * [taylor]: Taking taylor expansion of (sqrt 2) in v
7.382 * [taylor]: Taking taylor expansion of 2 in v
7.382 * [backup-simplify]: Simplify 2 into 2
7.383 * [backup-simplify]: Simplify (sqrt 2) into (sqrt 2)
7.383 * [backup-simplify]: Simplify (/ 0 (* 2 (sqrt 2))) into 0
7.383 * [taylor]: Taking taylor expansion of (pow v 2) in v
7.383 * [taylor]: Taking taylor expansion of v in v
7.383 * [backup-simplify]: Simplify 0 into 0
7.383 * [backup-simplify]: Simplify 1 into 1
7.384 * [backup-simplify]: Simplify (* 1 1) into 1
7.385 * [backup-simplify]: Simplify (/ (sqrt 2) 1) into (sqrt 2)
7.386 * [backup-simplify]: Simplify (* 1/4 (sqrt 2)) into (* 1/4 (sqrt 2))
7.386 * [backup-simplify]: Simplify (* 1/4 (sqrt 2)) into (* 1/4 (sqrt 2))
7.387 * [backup-simplify]: Simplify (+ (* 1 0) (* 0 1)) into 0
7.388 * [backup-simplify]: Simplify (- (/ 0 1) (+ (* (sqrt 2) (/ 0 1)))) into 0
7.389 * [backup-simplify]: Simplify (+ (* 1/4 0) (* 0 (sqrt 2))) into 0
7.389 * [backup-simplify]: Simplify 0 into 0
7.390 * [backup-simplify]: Simplify (/ (- 0 (pow 0 2) (+)) (* 2 (sqrt 2))) into 0
7.391 * [backup-simplify]: Simplify (+ (* 1 0) (+ (* 0 0) (* 0 1))) into 0
7.392 * [backup-simplify]: Simplify (- (/ 0 1) (+ (* (sqrt 2) (/ 0 1)) (* 0 (/ 0 1)))) into 0
7.393 * [backup-simplify]: Simplify (+ (* 1/4 0) (+ (* 0 0) (* 0 (sqrt 2)))) into 0
7.393 * [backup-simplify]: Simplify 0 into 0
7.395 * [backup-simplify]: Simplify (/ (- 0 (+ (* 2 (* 0 0)))) (* 2 (sqrt 2))) into 0
7.396 * [backup-simplify]: Simplify (+ (* 1 0) (+ (* 0 0) (+ (* 0 0) (* 0 1)))) into 0
7.397 * [backup-simplify]: Simplify (- (/ 0 1) (+ (* (sqrt 2) (/ 0 1)) (* 0 (/ 0 1)) (* 0 (/ 0 1)))) into 0
7.398 * [backup-simplify]: Simplify (+ (* 1/4 0) (+ (* 0 0) (+ (* 0 0) (* 0 (sqrt 2))))) into 0
7.398 * [backup-simplify]: Simplify 0 into 0
7.400 * [backup-simplify]: Simplify (/ (- 0 (pow 0 2) (+ (* 2 (* 0 0)))) (* 2 (sqrt 2))) into 0
7.406 * [backup-simplify]: Simplify (+ (* 1 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (* 0 1))))) into 0
7.408 * [backup-simplify]: Simplify (- (/ 0 1) (+ (* (sqrt 2) (/ 0 1)) (* 0 (/ 0 1)) (* 0 (/ 0 1)) (* 0 (/ 0 1)))) into 0
7.410 * [backup-simplify]: Simplify (+ (* 1/4 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (* 0 (sqrt 2)))))) into 0
7.410 * [backup-simplify]: Simplify 0 into 0
7.411 * [backup-simplify]: Simplify (/ (- 0 (+ (* 2 (* 0 0)) (* 2 (* 0 0)))) (* 2 (sqrt 2))) into 0
7.413 * [backup-simplify]: Simplify (+ (* 1 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (* 0 1)))))) into 0
7.414 * [backup-simplify]: Simplify (- (/ 0 1) (+ (* (sqrt 2) (/ 0 1)) (* 0 (/ 0 1)) (* 0 (/ 0 1)) (* 0 (/ 0 1)) (* 0 (/ 0 1)))) into 0
7.416 * [backup-simplify]: Simplify (+ (* 1/4 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (* 0 (sqrt 2))))))) into 0
7.417 * [backup-simplify]: Simplify 0 into 0
7.418 * [backup-simplify]: Simplify (/ (- 0 (pow 0 2) (+ (* 2 (* 0 0)) (* 2 (* 0 0)))) (* 2 (sqrt 2))) into 0
7.421 * [backup-simplify]: Simplify (+ (* 1 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (* 0 1))))))) into 0
7.423 * [backup-simplify]: Simplify (- (/ 0 1) (+ (* (sqrt 2) (/ 0 1)) (* 0 (/ 0 1)) (* 0 (/ 0 1)) (* 0 (/ 0 1)) (* 0 (/ 0 1)) (* 0 (/ 0 1)))) into 0
7.425 * [backup-simplify]: Simplify (+ (* 1/4 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (* 0 (sqrt 2)))))))) into 0
7.425 * [backup-simplify]: Simplify 0 into 0
7.426 * [backup-simplify]: Simplify (* (* 1/4 (sqrt 2)) (pow (/ 1 (/ 1 (- v))) 2)) into (* 1/4 (* (sqrt 2) (pow v 2)))
7.426 * * * [progress]: simplifying candidates
7.426 * * * * [progress]: [ 1 / 65 ] simplifiying candidate #<alt (λ (v) (* (log1p (expm1 (fma (sqrt (/ (sqrt 2) 4)) (sqrt (/ (sqrt 2) 4)) (- (* (/ (sqrt 2) 4) (* v v)))))) (sqrt (fma (* v v) -3 1))))>
7.426 * * * * [progress]: [ 2 / 65 ] simplifiying candidate #<alt (λ (v) (* (expm1 (log1p (fma (sqrt (/ (sqrt 2) 4)) (sqrt (/ (sqrt 2) 4)) (- (* (/ (sqrt 2) 4) (* v v)))))) (sqrt (fma (* v v) -3 1))))>
7.426 * * * * [progress]: [ 3 / 65 ] simplifiying candidate #<alt (λ (v) (* (+ (* (sqrt (/ (sqrt 2) 4)) (sqrt (/ (sqrt 2) 4))) (- (* (/ (sqrt 2) 4) (* v v)))) (sqrt (fma (* v v) -3 1))))>
7.426 * * * * [progress]: [ 4 / 65 ] simplifiying candidate #<alt (λ (v) (* (pow (fma (sqrt (/ (sqrt 2) 4)) (sqrt (/ (sqrt 2) 4)) (- (* (/ (sqrt 2) 4) (* v v)))) 1) (sqrt (fma (* v v) -3 1))))>
7.426 * * * * [progress]: [ 5 / 65 ] simplifiying candidate #<alt (λ (v) (* (exp (log (fma (sqrt (/ (sqrt 2) 4)) (sqrt (/ (sqrt 2) 4)) (- (* (/ (sqrt 2) 4) (* v v)))))) (sqrt (fma (* v v) -3 1))))>
7.427 * * * * [progress]: [ 6 / 65 ] simplifiying candidate #<alt (λ (v) (* (log (exp (fma (sqrt (/ (sqrt 2) 4)) (sqrt (/ (sqrt 2) 4)) (- (* (/ (sqrt 2) 4) (* v v)))))) (sqrt (fma (* v v) -3 1))))>
7.427 * * * * [progress]: [ 7 / 65 ] simplifiying candidate #<alt (λ (v) (* (* (* (cbrt (fma (sqrt (/ (sqrt 2) 4)) (sqrt (/ (sqrt 2) 4)) (- (* (/ (sqrt 2) 4) (* v v))))) (cbrt (fma (sqrt (/ (sqrt 2) 4)) (sqrt (/ (sqrt 2) 4)) (- (* (/ (sqrt 2) 4) (* v v)))))) (cbrt (fma (sqrt (/ (sqrt 2) 4)) (sqrt (/ (sqrt 2) 4)) (- (* (/ (sqrt 2) 4) (* v v)))))) (sqrt (fma (* v v) -3 1))))>
7.427 * * * * [progress]: [ 8 / 65 ] simplifiying candidate #<alt (λ (v) (* (cbrt (* (* (fma (sqrt (/ (sqrt 2) 4)) (sqrt (/ (sqrt 2) 4)) (- (* (/ (sqrt 2) 4) (* v v)))) (fma (sqrt (/ (sqrt 2) 4)) (sqrt (/ (sqrt 2) 4)) (- (* (/ (sqrt 2) 4) (* v v))))) (fma (sqrt (/ (sqrt 2) 4)) (sqrt (/ (sqrt 2) 4)) (- (* (/ (sqrt 2) 4) (* v v)))))) (sqrt (fma (* v v) -3 1))))>
7.427 * * * * [progress]: [ 9 / 65 ] simplifiying candidate #<alt (λ (v) (* (* (sqrt (fma (sqrt (/ (sqrt 2) 4)) (sqrt (/ (sqrt 2) 4)) (- (* (/ (sqrt 2) 4) (* v v))))) (sqrt (fma (sqrt (/ (sqrt 2) 4)) (sqrt (/ (sqrt 2) 4)) (- (* (/ (sqrt 2) 4) (* v v)))))) (sqrt (fma (* v v) -3 1))))>
7.427 * * * * [progress]: [ 10 / 65 ] simplifiying candidate #<alt (λ (v) (* (* 1 (fma (sqrt (/ (sqrt 2) 4)) (sqrt (/ (sqrt 2) 4)) (- (* (/ (sqrt 2) 4) (* v v))))) (sqrt (fma (* v v) -3 1))))>
7.427 * * * * [progress]: [ 11 / 65 ] simplifiying candidate #<alt (λ (v) (* (posit16->real (real->posit16 (fma (sqrt (/ (sqrt 2) 4)) (sqrt (/ (sqrt 2) 4)) (- (* (/ (sqrt 2) 4) (* v v)))))) (sqrt (fma (* v v) -3 1))))>
7.427 * * * * [progress]: [ 12 / 65 ] simplifiying candidate #<alt (λ (v) (* (fma (sqrt (/ (sqrt 2) 4)) (sqrt (/ (sqrt 2) 4)) (- (log1p (expm1 (* (/ (sqrt 2) 4) (* v v)))))) (sqrt (fma (* v v) -3 1))))>
7.427 * * * * [progress]: [ 13 / 65 ] simplifiying candidate #<alt (λ (v) (* (fma (sqrt (/ (sqrt 2) 4)) (sqrt (/ (sqrt 2) 4)) (- (expm1 (log1p (* (/ (sqrt 2) 4) (* v v)))))) (sqrt (fma (* v v) -3 1))))>
7.427 * * * * [progress]: [ 14 / 65 ] simplifiying candidate #<alt (λ (v) (* (fma (sqrt (/ (sqrt 2) 4)) (sqrt (/ (sqrt 2) 4)) (- (pow (* (/ (sqrt 2) 4) (* v v)) 1))) (sqrt (fma (* v v) -3 1))))>
7.427 * * * * [progress]: [ 15 / 65 ] simplifiying candidate #<alt (λ (v) (* (fma (sqrt (/ (sqrt 2) 4)) (sqrt (/ (sqrt 2) 4)) (- (pow (* (/ (sqrt 2) 4) (* v v)) 1))) (sqrt (fma (* v v) -3 1))))>
7.427 * * * * [progress]: [ 16 / 65 ] simplifiying candidate #<alt (λ (v) (* (fma (sqrt (/ (sqrt 2) 4)) (sqrt (/ (sqrt 2) 4)) (- (pow (* (/ (sqrt 2) 4) (* v v)) 1))) (sqrt (fma (* v v) -3 1))))>
7.427 * * * * [progress]: [ 17 / 65 ] simplifiying candidate #<alt (λ (v) (* (fma (sqrt (/ (sqrt 2) 4)) (sqrt (/ (sqrt 2) 4)) (- (exp (+ (- (log (sqrt 2)) (log 4)) (+ (log v) (log v)))))) (sqrt (fma (* v v) -3 1))))>
7.427 * * * * [progress]: [ 18 / 65 ] simplifiying candidate #<alt (λ (v) (* (fma (sqrt (/ (sqrt 2) 4)) (sqrt (/ (sqrt 2) 4)) (- (exp (+ (- (log (sqrt 2)) (log 4)) (log (* v v)))))) (sqrt (fma (* v v) -3 1))))>
7.427 * * * * [progress]: [ 19 / 65 ] simplifiying candidate #<alt (λ (v) (* (fma (sqrt (/ (sqrt 2) 4)) (sqrt (/ (sqrt 2) 4)) (- (exp (+ (log (/ (sqrt 2) 4)) (+ (log v) (log v)))))) (sqrt (fma (* v v) -3 1))))>
7.428 * * * * [progress]: [ 20 / 65 ] simplifiying candidate #<alt (λ (v) (* (fma (sqrt (/ (sqrt 2) 4)) (sqrt (/ (sqrt 2) 4)) (- (exp (+ (log (/ (sqrt 2) 4)) (log (* v v)))))) (sqrt (fma (* v v) -3 1))))>
7.428 * * * * [progress]: [ 21 / 65 ] simplifiying candidate #<alt (λ (v) (* (fma (sqrt (/ (sqrt 2) 4)) (sqrt (/ (sqrt 2) 4)) (- (exp (log (* (/ (sqrt 2) 4) (* v v)))))) (sqrt (fma (* v v) -3 1))))>
7.428 * * * * [progress]: [ 22 / 65 ] simplifiying candidate #<alt (λ (v) (* (fma (sqrt (/ (sqrt 2) 4)) (sqrt (/ (sqrt 2) 4)) (- (log (exp (* (/ (sqrt 2) 4) (* v v)))))) (sqrt (fma (* v v) -3 1))))>
7.428 * * * * [progress]: [ 23 / 65 ] simplifiying candidate #<alt (λ (v) (* (fma (sqrt (/ (sqrt 2) 4)) (sqrt (/ (sqrt 2) 4)) (- (cbrt (* (/ (* (* (sqrt 2) (sqrt 2)) (sqrt 2)) (* (* 4 4) 4)) (* (* (* v v) v) (* (* v v) v)))))) (sqrt (fma (* v v) -3 1))))>
7.428 * * * * [progress]: [ 24 / 65 ] simplifiying candidate #<alt (λ (v) (* (fma (sqrt (/ (sqrt 2) 4)) (sqrt (/ (sqrt 2) 4)) (- (cbrt (* (/ (* (* (sqrt 2) (sqrt 2)) (sqrt 2)) (* (* 4 4) 4)) (* (* (* v v) (* v v)) (* v v)))))) (sqrt (fma (* v v) -3 1))))>
7.428 * * * * [progress]: [ 25 / 65 ] simplifiying candidate #<alt (λ (v) (* (fma (sqrt (/ (sqrt 2) 4)) (sqrt (/ (sqrt 2) 4)) (- (cbrt (* (* (* (/ (sqrt 2) 4) (/ (sqrt 2) 4)) (/ (sqrt 2) 4)) (* (* (* v v) v) (* (* v v) v)))))) (sqrt (fma (* v v) -3 1))))>
7.428 * * * * [progress]: [ 26 / 65 ] simplifiying candidate #<alt (λ (v) (* (fma (sqrt (/ (sqrt 2) 4)) (sqrt (/ (sqrt 2) 4)) (- (cbrt (* (* (* (/ (sqrt 2) 4) (/ (sqrt 2) 4)) (/ (sqrt 2) 4)) (* (* (* v v) (* v v)) (* v v)))))) (sqrt (fma (* v v) -3 1))))>
7.428 * * * * [progress]: [ 27 / 65 ] simplifiying candidate #<alt (λ (v) (* (fma (sqrt (/ (sqrt 2) 4)) (sqrt (/ (sqrt 2) 4)) (- (* (* (cbrt (* (/ (sqrt 2) 4) (* v v))) (cbrt (* (/ (sqrt 2) 4) (* v v)))) (cbrt (* (/ (sqrt 2) 4) (* v v)))))) (sqrt (fma (* v v) -3 1))))>
7.428 * * * * [progress]: [ 28 / 65 ] simplifiying candidate #<alt (λ (v) (* (fma (sqrt (/ (sqrt 2) 4)) (sqrt (/ (sqrt 2) 4)) (- (cbrt (* (* (* (/ (sqrt 2) 4) (* v v)) (* (/ (sqrt 2) 4) (* v v))) (* (/ (sqrt 2) 4) (* v v)))))) (sqrt (fma (* v v) -3 1))))>
7.428 * * * * [progress]: [ 29 / 65 ] simplifiying candidate #<alt (λ (v) (* (fma (sqrt (/ (sqrt 2) 4)) (sqrt (/ (sqrt 2) 4)) (- (* (sqrt (* (/ (sqrt 2) 4) (* v v))) (sqrt (* (/ (sqrt 2) 4) (* v v)))))) (sqrt (fma (* v v) -3 1))))>
7.428 * * * * [progress]: [ 30 / 65 ] simplifiying candidate #<alt (λ (v) (* (fma (sqrt (/ (sqrt 2) 4)) (sqrt (/ (sqrt 2) 4)) (- (* 1 (* (/ (sqrt 2) 4) (* v v))))) (sqrt (fma (* v v) -3 1))))>
7.428 * * * * [progress]: [ 31 / 65 ] simplifiying candidate #<alt (λ (v) (* (fma (sqrt (/ (sqrt 2) 4)) (sqrt (/ (sqrt 2) 4)) (- (* (* (sqrt (/ (sqrt 2) 4)) v) (* (sqrt (/ (sqrt 2) 4)) v)))) (sqrt (fma (* v v) -3 1))))>
7.428 * * * * [progress]: [ 32 / 65 ] simplifiying candidate #<alt (λ (v) (* (fma (sqrt (/ (sqrt 2) 4)) (sqrt (/ (sqrt 2) 4)) (- (* (* (/ (sqrt (sqrt 2)) (sqrt 4)) v) (* (/ (sqrt (sqrt 2)) (sqrt 4)) v)))) (sqrt (fma (* v v) -3 1))))>
7.429 * * * * [progress]: [ 33 / 65 ] simplifiying candidate #<alt (λ (v) (* (fma (sqrt (/ (sqrt 2) 4)) (sqrt (/ (sqrt 2) 4)) (- (* (* (/ (sqrt (sqrt 2)) (sqrt 4)) v) (* (/ (sqrt (sqrt 2)) (sqrt 4)) v)))) (sqrt (fma (* v v) -3 1))))>
7.429 * * * * [progress]: [ 34 / 65 ] simplifiying candidate #<alt (λ (v) (* (fma (sqrt (/ (sqrt 2) 4)) (sqrt (/ (sqrt 2) 4)) (- (* (* (/ (sqrt 2) 4) v) v))) (sqrt (fma (* v v) -3 1))))>
7.429 * * * * [progress]: [ 35 / 65 ] simplifiying candidate #<alt (λ (v) (* (fma (sqrt (/ (sqrt 2) 4)) (sqrt (/ (sqrt 2) 4)) (- (* (* (cbrt (/ (sqrt 2) 4)) (cbrt (/ (sqrt 2) 4))) (* (cbrt (/ (sqrt 2) 4)) (* v v))))) (sqrt (fma (* v v) -3 1))))>
7.429 * * * * [progress]: [ 36 / 65 ] simplifiying candidate #<alt (λ (v) (* (fma (sqrt (/ (sqrt 2) 4)) (sqrt (/ (sqrt 2) 4)) (- (* (sqrt (/ (sqrt 2) 4)) (* (sqrt (/ (sqrt 2) 4)) (* v v))))) (sqrt (fma (* v v) -3 1))))>
7.429 * * * * [progress]: [ 37 / 65 ] simplifiying candidate #<alt (λ (v) (* (fma (sqrt (/ (sqrt 2) 4)) (sqrt (/ (sqrt 2) 4)) (- (* (/ (* (cbrt (sqrt 2)) (cbrt (sqrt 2))) (* (cbrt 4) (cbrt 4))) (* (/ (cbrt (sqrt 2)) (cbrt 4)) (* v v))))) (sqrt (fma (* v v) -3 1))))>
7.429 * * * * [progress]: [ 38 / 65 ] simplifiying candidate #<alt (λ (v) (* (fma (sqrt (/ (sqrt 2) 4)) (sqrt (/ (sqrt 2) 4)) (- (* (/ (* (cbrt (sqrt 2)) (cbrt (sqrt 2))) (sqrt 4)) (* (/ (cbrt (sqrt 2)) (sqrt 4)) (* v v))))) (sqrt (fma (* v v) -3 1))))>
7.429 * * * * [progress]: [ 39 / 65 ] simplifiying candidate #<alt (λ (v) (* (fma (sqrt (/ (sqrt 2) 4)) (sqrt (/ (sqrt 2) 4)) (- (* (/ (* (cbrt (sqrt 2)) (cbrt (sqrt 2))) 1) (* (/ (cbrt (sqrt 2)) 4) (* v v))))) (sqrt (fma (* v v) -3 1))))>
7.429 * * * * [progress]: [ 40 / 65 ] simplifiying candidate #<alt (λ (v) (* (fma (sqrt (/ (sqrt 2) 4)) (sqrt (/ (sqrt 2) 4)) (- (* (/ (sqrt (* (cbrt 2) (cbrt 2))) (* (cbrt 4) (cbrt 4))) (* (/ (sqrt (cbrt 2)) (cbrt 4)) (* v v))))) (sqrt (fma (* v v) -3 1))))>
7.429 * * * * [progress]: [ 41 / 65 ] simplifiying candidate #<alt (λ (v) (* (fma (sqrt (/ (sqrt 2) 4)) (sqrt (/ (sqrt 2) 4)) (- (* (/ (sqrt (* (cbrt 2) (cbrt 2))) (sqrt 4)) (* (/ (sqrt (cbrt 2)) (sqrt 4)) (* v v))))) (sqrt (fma (* v v) -3 1))))>
7.429 * * * * [progress]: [ 42 / 65 ] simplifiying candidate #<alt (λ (v) (* (fma (sqrt (/ (sqrt 2) 4)) (sqrt (/ (sqrt 2) 4)) (- (* (/ (sqrt (* (cbrt 2) (cbrt 2))) 1) (* (/ (sqrt (cbrt 2)) 4) (* v v))))) (sqrt (fma (* v v) -3 1))))>
7.429 * * * * [progress]: [ 43 / 65 ] simplifiying candidate #<alt (λ (v) (* (fma (sqrt (/ (sqrt 2) 4)) (sqrt (/ (sqrt 2) 4)) (- (* (/ (sqrt (sqrt 2)) (* (cbrt 4) (cbrt 4))) (* (/ (sqrt (sqrt 2)) (cbrt 4)) (* v v))))) (sqrt (fma (* v v) -3 1))))>
7.429 * * * * [progress]: [ 44 / 65 ] simplifiying candidate #<alt (λ (v) (* (fma (sqrt (/ (sqrt 2) 4)) (sqrt (/ (sqrt 2) 4)) (- (* (/ (sqrt (sqrt 2)) (sqrt 4)) (* (/ (sqrt (sqrt 2)) (sqrt 4)) (* v v))))) (sqrt (fma (* v v) -3 1))))>
7.429 * * * * [progress]: [ 45 / 65 ] simplifiying candidate #<alt (λ (v) (* (fma (sqrt (/ (sqrt 2) 4)) (sqrt (/ (sqrt 2) 4)) (- (* (/ (sqrt (sqrt 2)) 1) (* (/ (sqrt (sqrt 2)) 4) (* v v))))) (sqrt (fma (* v v) -3 1))))>
7.430 * * * * [progress]: [ 46 / 65 ] simplifiying candidate #<alt (λ (v) (* (fma (sqrt (/ (sqrt 2) 4)) (sqrt (/ (sqrt 2) 4)) (- (* (/ (sqrt 1) (* (cbrt 4) (cbrt 4))) (* (/ (sqrt 2) (cbrt 4)) (* v v))))) (sqrt (fma (* v v) -3 1))))>
7.430 * * * * [progress]: [ 47 / 65 ] simplifiying candidate #<alt (λ (v) (* (fma (sqrt (/ (sqrt 2) 4)) (sqrt (/ (sqrt 2) 4)) (- (* (/ (sqrt 1) (sqrt 4)) (* (/ (sqrt 2) (sqrt 4)) (* v v))))) (sqrt (fma (* v v) -3 1))))>
7.430 * * * * [progress]: [ 48 / 65 ] simplifiying candidate #<alt (λ (v) (* (fma (sqrt (/ (sqrt 2) 4)) (sqrt (/ (sqrt 2) 4)) (- (* (/ (sqrt 1) 1) (* (/ (sqrt 2) 4) (* v v))))) (sqrt (fma (* v v) -3 1))))>
7.430 * * * * [progress]: [ 49 / 65 ] simplifiying candidate #<alt (λ (v) (* (fma (sqrt (/ (sqrt 2) 4)) (sqrt (/ (sqrt 2) 4)) (- (* (/ (sqrt (sqrt 2)) (* (cbrt 4) (cbrt 4))) (* (/ (sqrt (sqrt 2)) (cbrt 4)) (* v v))))) (sqrt (fma (* v v) -3 1))))>
7.430 * * * * [progress]: [ 50 / 65 ] simplifiying candidate #<alt (λ (v) (* (fma (sqrt (/ (sqrt 2) 4)) (sqrt (/ (sqrt 2) 4)) (- (* (/ (sqrt (sqrt 2)) (sqrt 4)) (* (/ (sqrt (sqrt 2)) (sqrt 4)) (* v v))))) (sqrt (fma (* v v) -3 1))))>
7.430 * * * * [progress]: [ 51 / 65 ] simplifiying candidate #<alt (λ (v) (* (fma (sqrt (/ (sqrt 2) 4)) (sqrt (/ (sqrt 2) 4)) (- (* (/ (sqrt (sqrt 2)) 1) (* (/ (sqrt (sqrt 2)) 4) (* v v))))) (sqrt (fma (* v v) -3 1))))>
7.430 * * * * [progress]: [ 52 / 65 ] simplifiying candidate #<alt (λ (v) (* (fma (sqrt (/ (sqrt 2) 4)) (sqrt (/ (sqrt 2) 4)) (- (* (/ 1 (* (cbrt 4) (cbrt 4))) (* (/ (sqrt 2) (cbrt 4)) (* v v))))) (sqrt (fma (* v v) -3 1))))>
7.430 * * * * [progress]: [ 53 / 65 ] simplifiying candidate #<alt (λ (v) (* (fma (sqrt (/ (sqrt 2) 4)) (sqrt (/ (sqrt 2) 4)) (- (* (/ 1 (sqrt 4)) (* (/ (sqrt 2) (sqrt 4)) (* v v))))) (sqrt (fma (* v v) -3 1))))>
7.430 * * * * [progress]: [ 54 / 65 ] simplifiying candidate #<alt (λ (v) (* (fma (sqrt (/ (sqrt 2) 4)) (sqrt (/ (sqrt 2) 4)) (- (* (/ 1 1) (* (/ (sqrt 2) 4) (* v v))))) (sqrt (fma (* v v) -3 1))))>
7.430 * * * * [progress]: [ 55 / 65 ] simplifiying candidate #<alt (λ (v) (* (fma (sqrt (/ (sqrt 2) 4)) (sqrt (/ (sqrt 2) 4)) (- (* 1 (* (/ (sqrt 2) 4) (* v v))))) (sqrt (fma (* v v) -3 1))))>
7.430 * * * * [progress]: [ 56 / 65 ] simplifiying candidate #<alt (λ (v) (* (fma (sqrt (/ (sqrt 2) 4)) (sqrt (/ (sqrt 2) 4)) (- (* (sqrt 2) (* (/ 1 4) (* v v))))) (sqrt (fma (* v v) -3 1))))>
7.430 * * * * [progress]: [ 57 / 65 ] simplifiying candidate #<alt (λ (v) (* (fma (sqrt (/ (sqrt 2) 4)) (sqrt (/ (sqrt 2) 4)) (- (/ (* (sqrt 2) (* v v)) 4))) (sqrt (fma (* v v) -3 1))))>
7.430 * * * * [progress]: [ 58 / 65 ] simplifiying candidate #<alt (λ (v) (* (fma (sqrt (/ (sqrt 2) 4)) (sqrt (/ (sqrt 2) 4)) (- (posit16->real (real->posit16 (* (/ (sqrt 2) 4) (* v v)))))) (sqrt (fma (* v v) -3 1))))>
7.431 * * * * [progress]: [ 59 / 65 ] simplifiying candidate #<alt (λ (v) (* (fma (sqrt (/ (sqrt 2) 4)) (sqrt (/ (sqrt 2) 4)) (- (* (* v v) (/ (sqrt 2) 4)))) (sqrt (fma (* v v) -3 1))))>
7.431 * * * * [progress]: [ 60 / 65 ] simplifiying candidate #<alt (λ (v) (* (- (* 1/4 (sqrt 2)) (* 1/4 (* (sqrt 2) (pow v 2)))) (sqrt (fma (* v v) -3 1))))>
7.431 * * * * [progress]: [ 61 / 65 ] simplifiying candidate #<alt (λ (v) (* (- (* 1/4 (sqrt 2)) (* 1/4 (* (sqrt 2) (pow v 2)))) (sqrt (fma (* v v) -3 1))))>
7.431 * * * * [progress]: [ 62 / 65 ] simplifiying candidate #<alt (λ (v) (* (- (* 1/4 (sqrt 2)) (* 1/4 (* (sqrt 2) (pow v 2)))) (sqrt (fma (* v v) -3 1))))>
7.431 * * * * [progress]: [ 63 / 65 ] simplifiying candidate #<alt (λ (v) (* (fma (sqrt (/ (sqrt 2) 4)) (sqrt (/ (sqrt 2) 4)) (- (* 1/4 (* (sqrt 2) (pow v 2))))) (sqrt (fma (* v v) -3 1))))>
7.431 * * * * [progress]: [ 64 / 65 ] simplifiying candidate #<alt (λ (v) (* (fma (sqrt (/ (sqrt 2) 4)) (sqrt (/ (sqrt 2) 4)) (- (* 1/4 (* (sqrt 2) (pow v 2))))) (sqrt (fma (* v v) -3 1))))>
7.431 * * * * [progress]: [ 65 / 65 ] simplifiying candidate #<alt (λ (v) (* (fma (sqrt (/ (sqrt 2) 4)) (sqrt (/ (sqrt 2) 4)) (- (* 1/4 (* (sqrt 2) (pow v 2))))) (sqrt (fma (* v v) -3 1))))>
7.432 * [simplify]: Simplifying (expm1 (fma (sqrt (/ (sqrt 2) 4)) (sqrt (/ (sqrt 2) 4)) (- (* (/ (sqrt 2) 4) (* v v))))), (log1p (fma (sqrt (/ (sqrt 2) 4)) (sqrt (/ (sqrt 2) 4)) (- (* (/ (sqrt 2) 4) (* v v))))), (* (sqrt (/ (sqrt 2) 4)) (sqrt (/ (sqrt 2) 4))), (log (fma (sqrt (/ (sqrt 2) 4)) (sqrt (/ (sqrt 2) 4)) (- (* (/ (sqrt 2) 4) (* v v))))), (exp (fma (sqrt (/ (sqrt 2) 4)) (sqrt (/ (sqrt 2) 4)) (- (* (/ (sqrt 2) 4) (* v v))))), (* (cbrt (fma (sqrt (/ (sqrt 2) 4)) (sqrt (/ (sqrt 2) 4)) (- (* (/ (sqrt 2) 4) (* v v))))) (cbrt (fma (sqrt (/ (sqrt 2) 4)) (sqrt (/ (sqrt 2) 4)) (- (* (/ (sqrt 2) 4) (* v v)))))), (cbrt (fma (sqrt (/ (sqrt 2) 4)) (sqrt (/ (sqrt 2) 4)) (- (* (/ (sqrt 2) 4) (* v v))))), (* (* (fma (sqrt (/ (sqrt 2) 4)) (sqrt (/ (sqrt 2) 4)) (- (* (/ (sqrt 2) 4) (* v v)))) (fma (sqrt (/ (sqrt 2) 4)) (sqrt (/ (sqrt 2) 4)) (- (* (/ (sqrt 2) 4) (* v v))))) (fma (sqrt (/ (sqrt 2) 4)) (sqrt (/ (sqrt 2) 4)) (- (* (/ (sqrt 2) 4) (* v v))))), (sqrt (fma (sqrt (/ (sqrt 2) 4)) (sqrt (/ (sqrt 2) 4)) (- (* (/ (sqrt 2) 4) (* v v))))), (sqrt (fma (sqrt (/ (sqrt 2) 4)) (sqrt (/ (sqrt 2) 4)) (- (* (/ (sqrt 2) 4) (* v v))))), (real->posit16 (fma (sqrt (/ (sqrt 2) 4)) (sqrt (/ (sqrt 2) 4)) (- (* (/ (sqrt 2) 4) (* v v))))), (expm1 (* (/ (sqrt 2) 4) (* v v))), (log1p (* (/ (sqrt 2) 4) (* v v))), (* (/ (sqrt 2) 4) (* v v)), (* (/ (sqrt 2) 4) (* v v)), (+ (- (log (sqrt 2)) (log 4)) (+ (log v) (log v))), (+ (- (log (sqrt 2)) (log 4)) (log (* v v))), (+ (log (/ (sqrt 2) 4)) (+ (log v) (log v))), (+ (log (/ (sqrt 2) 4)) (log (* v v))), (log (* (/ (sqrt 2) 4) (* v v))), (exp (* (/ (sqrt 2) 4) (* v v))), (* (/ (* (* (sqrt 2) (sqrt 2)) (sqrt 2)) (* (* 4 4) 4)) (* (* (* v v) v) (* (* v v) v))), (* (/ (* (* (sqrt 2) (sqrt 2)) (sqrt 2)) (* (* 4 4) 4)) (* (* (* v v) (* v v)) (* v v))), (* (* (* (/ (sqrt 2) 4) (/ (sqrt 2) 4)) (/ (sqrt 2) 4)) (* (* (* v v) v) (* (* v v) v))), (* (* (* (/ (sqrt 2) 4) (/ (sqrt 2) 4)) (/ (sqrt 2) 4)) (* (* (* v v) (* v v)) (* v v))), (* (cbrt (* (/ (sqrt 2) 4) (* v v))) (cbrt (* (/ (sqrt 2) 4) (* v v)))), (cbrt (* (/ (sqrt 2) 4) (* v v))), (* (* (* (/ (sqrt 2) 4) (* v v)) (* (/ (sqrt 2) 4) (* v v))) (* (/ (sqrt 2) 4) (* v v))), (sqrt (* (/ (sqrt 2) 4) (* v v))), (sqrt (* (/ (sqrt 2) 4) (* v v))), (* (sqrt (/ (sqrt 2) 4)) v), (* (sqrt (/ (sqrt 2) 4)) v), (* (/ (sqrt (sqrt 2)) (sqrt 4)) v), (* (/ (sqrt (sqrt 2)) (sqrt 4)) v), (* (/ (sqrt (sqrt 2)) (sqrt 4)) v), (* (/ (sqrt (sqrt 2)) (sqrt 4)) v), (* (/ (sqrt 2) 4) v), (* (cbrt (/ (sqrt 2) 4)) (* v v)), (* (sqrt (/ (sqrt 2) 4)) (* v v)), (* (/ (cbrt (sqrt 2)) (cbrt 4)) (* v v)), (* (/ (cbrt (sqrt 2)) (sqrt 4)) (* v v)), (* (/ (cbrt (sqrt 2)) 4) (* v v)), (* (/ (sqrt (cbrt 2)) (cbrt 4)) (* v v)), (* (/ (sqrt (cbrt 2)) (sqrt 4)) (* v v)), (* (/ (sqrt (cbrt 2)) 4) (* v v)), (* (/ (sqrt (sqrt 2)) (cbrt 4)) (* v v)), (* (/ (sqrt (sqrt 2)) (sqrt 4)) (* v v)), (* (/ (sqrt (sqrt 2)) 4) (* v v)), (* (/ (sqrt 2) (cbrt 4)) (* v v)), (* (/ (sqrt 2) (sqrt 4)) (* v v)), (* (/ (sqrt 2) 4) (* v v)), (* (/ (sqrt (sqrt 2)) (cbrt 4)) (* v v)), (* (/ (sqrt (sqrt 2)) (sqrt 4)) (* v v)), (* (/ (sqrt (sqrt 2)) 4) (* v v)), (* (/ (sqrt 2) (cbrt 4)) (* v v)), (* (/ (sqrt 2) (sqrt 4)) (* v v)), (* (/ (sqrt 2) 4) (* v v)), (* (/ (sqrt 2) 4) (* v v)), (* (/ 1 4) (* v v)), (* (sqrt 2) (* v v)), (real->posit16 (* (/ (sqrt 2) 4) (* v v))), (- (* 1/4 (sqrt 2)) (* 1/4 (* (sqrt 2) (pow v 2)))), (- (* 1/4 (sqrt 2)) (* 1/4 (* (sqrt 2) (pow v 2)))), (- (* 1/4 (sqrt 2)) (* 1/4 (* (sqrt 2) (pow v 2)))), (* 1/4 (* (sqrt 2) (pow v 2))), (* 1/4 (* (sqrt 2) (pow v 2))), (* 1/4 (* (sqrt 2) (pow v 2)))
7.434 * * [simplify]: iteration 1: (101 enodes)
7.468 * * [simplify]: iteration 2: (436 enodes)
7.579 * * [simplify]: iteration 3: (953 enodes)
8.027 * * [simplify]: Extracting #0: cost 39 inf + 0
8.029 * * [simplify]: Extracting #1: cost 332 inf + 0
8.035 * * [simplify]: Extracting #2: cost 666 inf + 6123
8.050 * * [simplify]: Extracting #3: cost 314 inf + 81145
8.088 * * [simplify]: Extracting #4: cost 45 inf + 143025
8.125 * * [simplify]: Extracting #5: cost 2 inf + 151861
8.161 * * [simplify]: Extracting #6: cost 0 inf + 152350
8.226 * [simplify]: Simplified to (expm1 (* 1/4 (- (sqrt 2) (* (* v (sqrt 2)) v)))), (log1p (* 1/4 (- (sqrt 2) (* (* v (sqrt 2)) v)))), (/ (sqrt 2) 4), (log (* 1/4 (- (sqrt 2) (* (* v (sqrt 2)) v)))), (exp (* 1/4 (- (sqrt 2) (* (* v (sqrt 2)) v)))), (* (cbrt (* 1/4 (- (sqrt 2) (* (* v (sqrt 2)) v)))) (cbrt (* 1/4 (- (sqrt 2) (* (* v (sqrt 2)) v))))), (cbrt (* 1/4 (- (sqrt 2) (* (* v (sqrt 2)) v)))), (* (* (* 1/4 (- (sqrt 2) (* (* v (sqrt 2)) v))) (* 1/4 (- (sqrt 2) (* (* v (sqrt 2)) v)))) (* 1/4 (- (sqrt 2) (* (* v (sqrt 2)) v)))), (sqrt (* 1/4 (- (sqrt 2) (* (* v (sqrt 2)) v)))), (sqrt (* 1/4 (- (sqrt 2) (* (* v (sqrt 2)) v)))), (real->posit16 (* 1/4 (- (sqrt 2) (* (* v (sqrt 2)) v)))), (expm1 (* (/ (* v (sqrt 2)) 4) v)), (log1p (* (/ (* v (sqrt 2)) 4) v)), (* (/ (* v (sqrt 2)) 4) v), (* (/ (* v (sqrt 2)) 4) v), (log (* (/ (* v (sqrt 2)) 4) v)), (log (* (/ (* v (sqrt 2)) 4) v)), (log (* (/ (* v (sqrt 2)) 4) v)), (log (* (/ (* v (sqrt 2)) 4) v)), (log (* (/ (* v (sqrt 2)) 4) v)), (exp (* (/ (* v (sqrt 2)) 4) v)), (* (* 1/32 (sqrt 2)) (* (* (* v v) (* v v)) (* v v))), (* (* 1/32 (sqrt 2)) (* (* (* v v) (* v v)) (* v v))), (* (* 1/32 (sqrt 2)) (* (* (* v v) (* v v)) (* v v))), (* (* 1/32 (sqrt 2)) (* (* (* v v) (* v v)) (* v v))), (* (cbrt (* (/ (* v (sqrt 2)) 4) v)) (cbrt (* (/ (* v (sqrt 2)) 4) v))), (cbrt (* (/ (* v (sqrt 2)) 4) v)), (* (* 1/32 (sqrt 2)) (* (* (* v v) (* v v)) (* v v))), (sqrt (* (/ (* v (sqrt 2)) 4) v)), (sqrt (* (/ (* v (sqrt 2)) 4) v)), (* (sqrt (/ (sqrt 2) 4)) v), (* (sqrt (/ (sqrt 2) 4)) v), (/ (sqrt (sqrt 2)) (/ 2 v)), (/ (sqrt (sqrt 2)) (/ 2 v)), (/ (sqrt (sqrt 2)) (/ 2 v)), (/ (sqrt (sqrt 2)) (/ 2 v)), (/ (* v (sqrt 2)) 4), (* v (* (cbrt (/ (sqrt 2) 4)) v)), (* (* v v) (sqrt (/ (sqrt 2) 4))), (/ (cbrt (sqrt 2)) (/ (cbrt 4) (* v v))), (* (/ (cbrt (sqrt 2)) 2) (* v v)), (* v (/ (cbrt (sqrt 2)) (/ 4 v))), (* v (/ (sqrt (cbrt 2)) (/ (cbrt 4) v))), (* (/ (sqrt (cbrt 2)) 2) (* v v)), (/ (sqrt (cbrt 2)) (/ 4 (* v v))), (/ (* (* v v) (sqrt (sqrt 2))) (cbrt 4)), (* (/ (sqrt (sqrt 2)) (/ 2 v)) v), (/ (sqrt (sqrt 2)) (/ 4 (* v v))), (/ (sqrt 2) (/ (cbrt 4) (* v v))), (/ (sqrt 2) (/ 2 (* v v))), (* (/ (* v (sqrt 2)) 4) v), (/ (* (* v v) (sqrt (sqrt 2))) (cbrt 4)), (* (/ (sqrt (sqrt 2)) (/ 2 v)) v), (/ (sqrt (sqrt 2)) (/ 4 (* v v))), (/ (sqrt 2) (/ (cbrt 4) (* v v))), (/ (sqrt 2) (/ 2 (* v v))), (* (/ (* v (sqrt 2)) 4) v), (* (/ (* v (sqrt 2)) 4) v), (/ (* v v) 4), (* (* v (sqrt 2)) v), (real->posit16 (* (/ (* v (sqrt 2)) 4) v)), (* 1/4 (- (sqrt 2) (* (* v (sqrt 2)) v))), (* 1/4 (- (sqrt 2) (* (* v (sqrt 2)) v))), (* 1/4 (- (sqrt 2) (* (* v (sqrt 2)) v))), (* (/ (* v (sqrt 2)) 4) v), (* (/ (* v (sqrt 2)) 4) v), (* (/ (* v (sqrt 2)) 4) v)
8.235 * * * [progress]: adding candidates to table
9.163 * [progress]: [Phase 3 of 3] Extracting.
9.163 * * [regime]: Finding splitpoints for: (#<alt (λ (v) (* (- (/ (sqrt 2) 4) (* (/ (sqrt 2) 4) (* v v))) (sqrt (fma (* v v) -3 1))))> #<alt (λ (v) (* (fma (sqrt (/ (sqrt 2) 4)) (sqrt (/ (sqrt 2) 4)) (- (* (/ (sqrt 2) 4) (* v v)))) (sqrt (fma (* v v) -3 1))))>)
9.163 * * * [regime-changes]: Trying 2 branch expressions: (v (* v v))
9.163 * * * * [regimes]: Trying to branch on v from (#<alt (λ (v) (* (- (/ (sqrt 2) 4) (* (/ (sqrt 2) 4) (* v v))) (sqrt (fma (* v v) -3 1))))> #<alt (λ (v) (* (fma (sqrt (/ (sqrt 2) 4)) (sqrt (/ (sqrt 2) 4)) (- (* (/ (sqrt 2) 4) (* v v)))) (sqrt (fma (* v v) -3 1))))>)
9.198 * * * * [regimes]: Trying to branch on (* v v) from (#<alt (λ (v) (* (- (/ (sqrt 2) 4) (* (/ (sqrt 2) 4) (* v v))) (sqrt (fma (* v v) -3 1))))> #<alt (λ (v) (* (fma (sqrt (/ (sqrt 2) 4)) (sqrt (/ (sqrt 2) 4)) (- (* (/ (sqrt 2) 4) (* v v)))) (sqrt (fma (* v v) -3 1))))>)
9.217 * * * [regime]: Found split indices: #<option (#s(si 0 255))>
9.217 * [simplify]: Simplifying (* (- (/ (sqrt 2) 4) (* (/ (sqrt 2) 4) (* v v))) (sqrt (fma (* v v) -3 1)))
9.217 * * [simplify]: iteration 1: (13 enodes)
9.218 * * [simplify]: iteration 2: (17 enodes)
9.219 * * [simplify]: Extracting #0: cost 1 inf + 0
9.219 * * [simplify]: Extracting #1: cost 3 inf + 0
9.219 * * [simplify]: Extracting #2: cost 6 inf + 0
9.219 * * [simplify]: Extracting #3: cost 11 inf + 0
9.219 * * [simplify]: Extracting #4: cost 10 inf + 3
9.219 * * [simplify]: Extracting #5: cost 7 inf + 46
9.219 * * [simplify]: Extracting #6: cost 3 inf + 405
9.219 * * [simplify]: Extracting #7: cost 1 inf + 771
9.219 * * [simplify]: Extracting #8: cost 0 inf + 1111
9.220 * [simplify]: Simplified to (* (sqrt (fma (* v v) -3 1)) (- (/ (sqrt 2) 4) (* (/ (sqrt 2) 4) (* v v))))
12.714 * [regime-testing]: Baseline error score: 0.013365031953445248
12.717 * [regime-testing]: Oracle error score: 0.0015001875234404302
12.721 * [regime-testing]: End program error score: 0.013365031953445248