11.720 * [progress]: [Phase 1 of 3] Setting up.
0.003 * * * [progress]: [1/2] Preparing points
0.083 * * * [progress]: [2/2] Setting up program.
0.086 * [progress]: [Phase 2 of 3] Improving.
0.086 * * * * [progress]: [ 1 / 1 ] simplifiying candidate #<alt (λ (v) (* (* (/ (sqrt 2) 4) (sqrt (- 1 (* 3 (* v v))))) (- 1 (* v v))))>
0.086 * [simplify]: Simplifying:
  (* (* (/ (sqrt 2) 4) (sqrt (- 1 (* 3 (* v v))))) (- 1 (* v v)))
0.086 * * [simplify]: iteration 0: 14 enodes
0.089 * * [simplify]: iteration 1: 29 enodes
0.094 * * [simplify]: iteration 2: 73 enodes
0.121 * * [simplify]: iteration 3: 223 enodes
0.219 * * [simplify]: iteration 4: 728 enodes
0.547 * * [simplify]: iteration 5: 1649 enodes
0.835 * * [simplify]: iteration 6: 2028 enodes
1.046 * * [simplify]: iteration complete: 2028 enodes
1.046 * * [simplify]: Extracting #0: cost 1 inf + 0
1.046 * * [simplify]: Extracting #1: cost 33 inf + 0
1.047 * * [simplify]: Extracting #2: cost 105 inf + 2
1.047 * * [simplify]: Extracting #3: cost 324 inf + 334
1.050 * * [simplify]: Extracting #4: cost 283 inf + 10818
1.055 * * [simplify]: Extracting #5: cost 165 inf + 27807
1.067 * * [simplify]: Extracting #6: cost 54 inf + 57728
1.084 * * [simplify]: Extracting #7: cost 3 inf + 73780
1.114 * * [simplify]: Extracting #8: cost 0 inf + 74955
1.134 * [simplify]: Simplified to:
  (/ (* (sqrt (- 1 (* (* v v) 3))) (* (- 1 (* v v)) (sqrt 2))) 4)
1.134 * * [progress]: iteration 1 / 4
1.134 * * * [progress]: picking best candidate
1.137 * * * * [pick]: Picked  #<alt (λ (v) (* (* (/ (sqrt 2) 4) (sqrt (- 1 (* 3 (* v v))))) (- 1 (* v v))))>
1.137 * * * [progress]: localizing error
1.157 * * * [progress]: generating rewritten candidates
1.157 * * * * [progress]: [ 1 / 2 ] rewriting at (2 1 2 1 2)
1.176 * * * * [progress]: [ 2 / 2 ] rewriting at (2 1)
1.215 * * * [progress]: generating series expansions
1.215 * * * * [progress]: [ 1 / 2 ] generating series at (2 1 2 1 2)
1.216 * [backup-simplify]: Simplify (* 3 (* v v)) into (* 3 (pow v 2))
1.216 * [approximate]: Taking taylor expansion of (* 3 (pow v 2)) in (v) around 0
1.216 * [taylor]: Taking taylor expansion of (* 3 (pow v 2)) in v
1.216 * [taylor]: Taking taylor expansion of 3 in v
1.216 * [backup-simplify]: Simplify 3 into 3
1.216 * [taylor]: Taking taylor expansion of (pow v 2) in v
1.216 * [taylor]: Taking taylor expansion of v in v
1.216 * [backup-simplify]: Simplify 0 into 0
1.216 * [backup-simplify]: Simplify 1 into 1
1.216 * [taylor]: Taking taylor expansion of (* 3 (pow v 2)) in v
1.216 * [taylor]: Taking taylor expansion of 3 in v
1.216 * [backup-simplify]: Simplify 3 into 3
1.216 * [taylor]: Taking taylor expansion of (pow v 2) in v
1.216 * [taylor]: Taking taylor expansion of v in v
1.216 * [backup-simplify]: Simplify 0 into 0
1.216 * [backup-simplify]: Simplify 1 into 1
1.217 * [backup-simplify]: Simplify (* 1 1) into 1
1.217 * [backup-simplify]: Simplify (* 3 1) into 3
1.217 * [backup-simplify]: Simplify 3 into 3
1.218 * [backup-simplify]: Simplify (+ (* 1 0) (* 0 1)) into 0
1.219 * [backup-simplify]: Simplify (+ (* 3 0) (* 0 1)) into 0
1.219 * [backup-simplify]: Simplify 0 into 0
1.219 * [backup-simplify]: Simplify (+ (* 1 0) (+ (* 0 0) (* 0 1))) into 0
1.220 * [backup-simplify]: Simplify (+ (* 3 0) (+ (* 0 0) (* 0 1))) into 0
1.220 * [backup-simplify]: Simplify 0 into 0
1.222 * [backup-simplify]: Simplify (+ (* 1 0) (+ (* 0 0) (+ (* 0 0) (* 0 1)))) into 0
1.223 * [backup-simplify]: Simplify (+ (* 3 0) (+ (* 0 0) (+ (* 0 0) (* 0 1)))) into 0
1.223 * [backup-simplify]: Simplify 0 into 0
1.225 * [backup-simplify]: Simplify (+ (* 1 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (* 0 1))))) into 0
1.226 * [backup-simplify]: Simplify (+ (* 3 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (* 0 1))))) into 0
1.226 * [backup-simplify]: Simplify 0 into 0
1.227 * [backup-simplify]: Simplify (+ (* 1 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (* 0 1)))))) into 0
1.228 * [backup-simplify]: Simplify (+ (* 3 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (* 0 1)))))) into 0
1.229 * [backup-simplify]: Simplify 0 into 0
1.230 * [backup-simplify]: Simplify (+ (* 1 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (* 0 1))))))) into 0
1.232 * [backup-simplify]: Simplify (+ (* 3 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (* 0 1))))))) into 0
1.232 * [backup-simplify]: Simplify 0 into 0
1.232 * [backup-simplify]: Simplify (* 3 (pow v 2)) into (* 3 (pow v 2))
1.232 * [backup-simplify]: Simplify (* 3 (* (/ 1 v) (/ 1 v))) into (/ 3 (pow v 2))
1.232 * [approximate]: Taking taylor expansion of (/ 3 (pow v 2)) in (v) around 0
1.232 * [taylor]: Taking taylor expansion of (/ 3 (pow v 2)) in v
1.232 * [taylor]: Taking taylor expansion of 3 in v
1.232 * [backup-simplify]: Simplify 3 into 3
1.232 * [taylor]: Taking taylor expansion of (pow v 2) in v
1.232 * [taylor]: Taking taylor expansion of v in v
1.232 * [backup-simplify]: Simplify 0 into 0
1.232 * [backup-simplify]: Simplify 1 into 1
1.232 * [backup-simplify]: Simplify (* 1 1) into 1
1.233 * [backup-simplify]: Simplify (/ 3 1) into 3
1.233 * [taylor]: Taking taylor expansion of (/ 3 (pow v 2)) in v
1.233 * [taylor]: Taking taylor expansion of 3 in v
1.233 * [backup-simplify]: Simplify 3 into 3
1.233 * [taylor]: Taking taylor expansion of (pow v 2) in v
1.233 * [taylor]: Taking taylor expansion of v in v
1.233 * [backup-simplify]: Simplify 0 into 0
1.233 * [backup-simplify]: Simplify 1 into 1
1.233 * [backup-simplify]: Simplify (* 1 1) into 1
1.234 * [backup-simplify]: Simplify (/ 3 1) into 3
1.234 * [backup-simplify]: Simplify 3 into 3
1.234 * [backup-simplify]: Simplify (+ (* 1 0) (* 0 1)) into 0
1.235 * [backup-simplify]: Simplify (- (/ 0 1) (+ (* 3 (/ 0 1)))) into 0
1.235 * [backup-simplify]: Simplify 0 into 0
1.236 * [backup-simplify]: Simplify (+ (* 1 0) (+ (* 0 0) (* 0 1))) into 0
1.237 * [backup-simplify]: Simplify (- (/ 0 1) (+ (* 3 (/ 0 1)) (* 0 (/ 0 1)))) into 0
1.237 * [backup-simplify]: Simplify 0 into 0
1.238 * [backup-simplify]: Simplify (+ (* 1 0) (+ (* 0 0) (+ (* 0 0) (* 0 1)))) into 0
1.239 * [backup-simplify]: Simplify (- (/ 0 1) (+ (* 3 (/ 0 1)) (* 0 (/ 0 1)) (* 0 (/ 0 1)))) into 0
1.239 * [backup-simplify]: Simplify 0 into 0
1.240 * [backup-simplify]: Simplify (+ (* 1 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (* 0 1))))) into 0
1.240 * [backup-simplify]: Simplify (- (/ 0 1) (+ (* 3 (/ 0 1)) (* 0 (/ 0 1)) (* 0 (/ 0 1)) (* 0 (/ 0 1)))) into 0
1.240 * [backup-simplify]: Simplify 0 into 0
1.241 * [backup-simplify]: Simplify (+ (* 1 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (* 0 1)))))) into 0
1.242 * [backup-simplify]: Simplify (- (/ 0 1) (+ (* 3 (/ 0 1)) (* 0 (/ 0 1)) (* 0 (/ 0 1)) (* 0 (/ 0 1)) (* 0 (/ 0 1)))) into 0
1.242 * [backup-simplify]: Simplify 0 into 0
1.243 * [backup-simplify]: Simplify (+ (* 1 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (* 0 1))))))) into 0
1.243 * [backup-simplify]: Simplify (- (/ 0 1) (+ (* 3 (/ 0 1)) (* 0 (/ 0 1)) (* 0 (/ 0 1)) (* 0 (/ 0 1)) (* 0 (/ 0 1)) (* 0 (/ 0 1)))) into 0
1.244 * [backup-simplify]: Simplify 0 into 0
1.244 * [backup-simplify]: Simplify (* 3 (pow (/ 1 (/ 1 v)) 2)) into (* 3 (pow v 2))
1.244 * [backup-simplify]: Simplify (* 3 (* (/ 1 (- v)) (/ 1 (- v)))) into (/ 3 (pow v 2))
1.244 * [approximate]: Taking taylor expansion of (/ 3 (pow v 2)) in (v) around 0
1.244 * [taylor]: Taking taylor expansion of (/ 3 (pow v 2)) in v
1.244 * [taylor]: Taking taylor expansion of 3 in v
1.244 * [backup-simplify]: Simplify 3 into 3
1.244 * [taylor]: Taking taylor expansion of (pow v 2) in v
1.244 * [taylor]: Taking taylor expansion of v in v
1.244 * [backup-simplify]: Simplify 0 into 0
1.244 * [backup-simplify]: Simplify 1 into 1
1.244 * [backup-simplify]: Simplify (* 1 1) into 1
1.244 * [backup-simplify]: Simplify (/ 3 1) into 3
1.244 * [taylor]: Taking taylor expansion of (/ 3 (pow v 2)) in v
1.244 * [taylor]: Taking taylor expansion of 3 in v
1.244 * [backup-simplify]: Simplify 3 into 3
1.244 * [taylor]: Taking taylor expansion of (pow v 2) in v
1.244 * [taylor]: Taking taylor expansion of v in v
1.245 * [backup-simplify]: Simplify 0 into 0
1.245 * [backup-simplify]: Simplify 1 into 1
1.245 * [backup-simplify]: Simplify (* 1 1) into 1
1.245 * [backup-simplify]: Simplify (/ 3 1) into 3
1.245 * [backup-simplify]: Simplify 3 into 3
1.246 * [backup-simplify]: Simplify (+ (* 1 0) (* 0 1)) into 0
1.246 * [backup-simplify]: Simplify (- (/ 0 1) (+ (* 3 (/ 0 1)))) into 0
1.246 * [backup-simplify]: Simplify 0 into 0
1.247 * [backup-simplify]: Simplify (+ (* 1 0) (+ (* 0 0) (* 0 1))) into 0
1.247 * [backup-simplify]: Simplify (- (/ 0 1) (+ (* 3 (/ 0 1)) (* 0 (/ 0 1)))) into 0
1.247 * [backup-simplify]: Simplify 0 into 0
1.248 * [backup-simplify]: Simplify (+ (* 1 0) (+ (* 0 0) (+ (* 0 0) (* 0 1)))) into 0
1.249 * [backup-simplify]: Simplify (- (/ 0 1) (+ (* 3 (/ 0 1)) (* 0 (/ 0 1)) (* 0 (/ 0 1)))) into 0
1.249 * [backup-simplify]: Simplify 0 into 0
1.250 * [backup-simplify]: Simplify (+ (* 1 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (* 0 1))))) into 0
1.251 * [backup-simplify]: Simplify (- (/ 0 1) (+ (* 3 (/ 0 1)) (* 0 (/ 0 1)) (* 0 (/ 0 1)) (* 0 (/ 0 1)))) into 0
1.251 * [backup-simplify]: Simplify 0 into 0
1.252 * [backup-simplify]: Simplify (+ (* 1 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (* 0 1)))))) into 0
1.253 * [backup-simplify]: Simplify (- (/ 0 1) (+ (* 3 (/ 0 1)) (* 0 (/ 0 1)) (* 0 (/ 0 1)) (* 0 (/ 0 1)) (* 0 (/ 0 1)))) into 0
1.253 * [backup-simplify]: Simplify 0 into 0
1.255 * [backup-simplify]: Simplify (+ (* 1 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (* 0 1))))))) into 0
1.256 * [backup-simplify]: Simplify (- (/ 0 1) (+ (* 3 (/ 0 1)) (* 0 (/ 0 1)) (* 0 (/ 0 1)) (* 0 (/ 0 1)) (* 0 (/ 0 1)) (* 0 (/ 0 1)))) into 0
1.256 * [backup-simplify]: Simplify 0 into 0
1.256 * [backup-simplify]: Simplify (* 3 (pow (/ 1 (/ 1 (- v))) 2)) into (* 3 (pow v 2))
1.257 * * * * [progress]: [ 2 / 2 ] generating series at (2 1)
1.258 * [backup-simplify]: Simplify (* (/ (sqrt 2) 4) (sqrt (- 1 (* 3 (* v v))))) into (* 1/4 (* (sqrt (- 1 (* 3 (pow v 2)))) (sqrt 2)))
1.258 * [approximate]: Taking taylor expansion of (* 1/4 (* (sqrt (- 1 (* 3 (pow v 2)))) (sqrt 2))) in (v) around 0
1.258 * [taylor]: Taking taylor expansion of (* 1/4 (* (sqrt (- 1 (* 3 (pow v 2)))) (sqrt 2))) in v
1.258 * [taylor]: Taking taylor expansion of 1/4 in v
1.258 * [backup-simplify]: Simplify 1/4 into 1/4
1.258 * [taylor]: Taking taylor expansion of (* (sqrt (- 1 (* 3 (pow v 2)))) (sqrt 2)) in v
1.258 * [taylor]: Taking taylor expansion of (sqrt (- 1 (* 3 (pow v 2)))) in v
1.258 * [taylor]: Taking taylor expansion of (- 1 (* 3 (pow v 2))) in v
1.258 * [taylor]: Taking taylor expansion of 1 in v
1.258 * [backup-simplify]: Simplify 1 into 1
1.258 * [taylor]: Taking taylor expansion of (* 3 (pow v 2)) in v
1.258 * [taylor]: Taking taylor expansion of 3 in v
1.258 * [backup-simplify]: Simplify 3 into 3
1.258 * [taylor]: Taking taylor expansion of (pow v 2) in v
1.258 * [taylor]: Taking taylor expansion of v in v
1.258 * [backup-simplify]: Simplify 0 into 0
1.258 * [backup-simplify]: Simplify 1 into 1
1.258 * [backup-simplify]: Simplify (+ 1 0) into 1
1.259 * [backup-simplify]: Simplify (sqrt 1) into 1
1.259 * [backup-simplify]: Simplify (+ 0 0) into 0
1.260 * [backup-simplify]: Simplify (/ 0 (* 2 (sqrt 1))) into 0
1.260 * [taylor]: Taking taylor expansion of (sqrt 2) in v
1.260 * [taylor]: Taking taylor expansion of 2 in v
1.260 * [backup-simplify]: Simplify 2 into 2
1.260 * [backup-simplify]: Simplify (sqrt 2) into (sqrt 2)
1.261 * [backup-simplify]: Simplify (/ 0 (* 2 (sqrt 2))) into 0
1.261 * [taylor]: Taking taylor expansion of (* 1/4 (* (sqrt (- 1 (* 3 (pow v 2)))) (sqrt 2))) in v
1.261 * [taylor]: Taking taylor expansion of 1/4 in v
1.261 * [backup-simplify]: Simplify 1/4 into 1/4
1.261 * [taylor]: Taking taylor expansion of (* (sqrt (- 1 (* 3 (pow v 2)))) (sqrt 2)) in v
1.261 * [taylor]: Taking taylor expansion of (sqrt (- 1 (* 3 (pow v 2)))) in v
1.261 * [taylor]: Taking taylor expansion of (- 1 (* 3 (pow v 2))) in v
1.261 * [taylor]: Taking taylor expansion of 1 in v
1.261 * [backup-simplify]: Simplify 1 into 1
1.261 * [taylor]: Taking taylor expansion of (* 3 (pow v 2)) in v
1.261 * [taylor]: Taking taylor expansion of 3 in v
1.261 * [backup-simplify]: Simplify 3 into 3
1.261 * [taylor]: Taking taylor expansion of (pow v 2) in v
1.261 * [taylor]: Taking taylor expansion of v in v
1.261 * [backup-simplify]: Simplify 0 into 0
1.261 * [backup-simplify]: Simplify 1 into 1
1.262 * [backup-simplify]: Simplify (+ 1 0) into 1
1.262 * [backup-simplify]: Simplify (sqrt 1) into 1
1.263 * [backup-simplify]: Simplify (+ 0 0) into 0
1.263 * [backup-simplify]: Simplify (/ 0 (* 2 (sqrt 1))) into 0
1.263 * [taylor]: Taking taylor expansion of (sqrt 2) in v
1.263 * [taylor]: Taking taylor expansion of 2 in v
1.263 * [backup-simplify]: Simplify 2 into 2
1.264 * [backup-simplify]: Simplify (sqrt 2) into (sqrt 2)
1.264 * [backup-simplify]: Simplify (/ 0 (* 2 (sqrt 2))) into 0
1.265 * [backup-simplify]: Simplify (* 1 (sqrt 2)) into (sqrt 2)
1.266 * [backup-simplify]: Simplify (* 1/4 (sqrt 2)) into (* 1/4 (sqrt 2))
1.267 * [backup-simplify]: Simplify (* 1/4 (sqrt 2)) into (* 1/4 (sqrt 2))
1.268 * [backup-simplify]: Simplify (+ (* 1 0) (* 0 (sqrt 2))) into 0
1.269 * [backup-simplify]: Simplify (+ (* 1/4 0) (* 0 (sqrt 2))) into 0
1.269 * [backup-simplify]: Simplify 0 into 0
1.270 * [backup-simplify]: Simplify (/ (- 0 (pow 0 2) (+)) (* 2 (sqrt 2))) into 0
1.270 * [backup-simplify]: Simplify (* 1 1) into 1
1.270 * [backup-simplify]: Simplify (* 3 1) into 3
1.271 * [backup-simplify]: Simplify (- 3) into -3
1.271 * [backup-simplify]: Simplify (+ 0 -3) into -3
1.272 * [backup-simplify]: Simplify (/ (- -3 (pow 0 2) (+)) (* 2 1)) into -3/2
1.276 * [backup-simplify]: Simplify (+ (* 1 0) (+ (* 0 0) (* -3/2 (sqrt 2)))) into (- (* 3/2 (sqrt 2)))
1.280 * [backup-simplify]: Simplify (+ (* 1/4 (- (* 3/2 (sqrt 2)))) (+ (* 0 0) (* 0 (sqrt 2)))) into (- (* 3/8 (sqrt 2)))
1.281 * [backup-simplify]: Simplify (- (* 3/8 (sqrt 2))) into (- (* 3/8 (sqrt 2)))
1.283 * [backup-simplify]: Simplify (/ (- 0 (+ (* 2 (* 0 0)))) (* 2 (sqrt 2))) into 0
1.284 * [backup-simplify]: Simplify (+ (* 1 0) (* 0 1)) into 0
1.284 * [backup-simplify]: Simplify (+ (* 3 0) (* 0 1)) into 0
1.285 * [backup-simplify]: Simplify (- 0) into 0
1.285 * [backup-simplify]: Simplify (+ 0 0) into 0
1.286 * [backup-simplify]: Simplify (/ (- 0 (+ (* 2 (* 0 -3/2)))) (* 2 1)) into 0
1.288 * [backup-simplify]: Simplify (+ (* 1 0) (+ (* 0 0) (+ (* -3/2 0) (* 0 (sqrt 2))))) into 0
1.289 * [backup-simplify]: Simplify (+ (* 1/4 0) (+ (* 0 (- (* 3/2 (sqrt 2)))) (+ (* 0 0) (* 0 (sqrt 2))))) into 0
1.290 * [backup-simplify]: Simplify 0 into 0
1.291 * [backup-simplify]: Simplify (/ (- 0 (pow 0 2) (+ (* 2 (* 0 0)))) (* 2 (sqrt 2))) into 0
1.292 * [backup-simplify]: Simplify (+ (* 1 0) (+ (* 0 0) (* 0 1))) into 0
1.293 * [backup-simplify]: Simplify (+ (* 3 0) (+ (* 0 0) (* 0 1))) into 0
1.293 * [backup-simplify]: Simplify (- 0) into 0
1.293 * [backup-simplify]: Simplify (+ 0 0) into 0
1.295 * [backup-simplify]: Simplify (/ (- 0 (pow -3/2 2) (+ (* 2 (* 0 0)))) (* 2 1)) into -9/8
1.302 * [backup-simplify]: Simplify (+ (* 1 0) (+ (* 0 0) (+ (* -3/2 0) (+ (* 0 0) (* -9/8 (sqrt 2)))))) into (- (* 9/8 (sqrt 2)))
1.306 * [backup-simplify]: Simplify (+ (* 1/4 (- (* 9/8 (sqrt 2)))) (+ (* 0 0) (+ (* 0 (- (* 3/2 (sqrt 2)))) (+ (* 0 0) (* 0 (sqrt 2)))))) into (- (* 9/32 (sqrt 2)))
1.307 * [backup-simplify]: Simplify (- (* 9/32 (sqrt 2))) into (- (* 9/32 (sqrt 2)))
1.310 * [backup-simplify]: Simplify (+ (* (- (* 9/32 (sqrt 2))) (pow v 4)) (+ (* (- (* 3/8 (sqrt 2))) (pow v 2)) (* 1/4 (sqrt 2)))) into (- (* 1/4 (sqrt 2)) (+ (* 9/32 (* (sqrt 2) (pow v 4))) (* 3/8 (* (sqrt 2) (pow v 2)))))
1.314 * [backup-simplify]: Simplify (* (/ (sqrt 2) 4) (sqrt (- 1 (* 3 (* (/ 1 v) (/ 1 v)))))) into (* 1/4 (* (sqrt 2) (sqrt (- 1 (* 3 (/ 1 (pow v 2)))))))
1.314 * [approximate]: Taking taylor expansion of (* 1/4 (* (sqrt 2) (sqrt (- 1 (* 3 (/ 1 (pow v 2))))))) in (v) around 0
1.315 * [taylor]: Taking taylor expansion of (* 1/4 (* (sqrt 2) (sqrt (- 1 (* 3 (/ 1 (pow v 2))))))) in v
1.315 * [taylor]: Taking taylor expansion of 1/4 in v
1.315 * [backup-simplify]: Simplify 1/4 into 1/4
1.315 * [taylor]: Taking taylor expansion of (* (sqrt 2) (sqrt (- 1 (* 3 (/ 1 (pow v 2)))))) in v
1.315 * [taylor]: Taking taylor expansion of (sqrt 2) in v
1.315 * [taylor]: Taking taylor expansion of 2 in v
1.315 * [backup-simplify]: Simplify 2 into 2
1.315 * [backup-simplify]: Simplify (sqrt 2) into (sqrt 2)
1.315 * [backup-simplify]: Simplify (/ 0 (* 2 (sqrt 2))) into 0
1.315 * [taylor]: Taking taylor expansion of (sqrt (- 1 (* 3 (/ 1 (pow v 2))))) in v
1.315 * [taylor]: Taking taylor expansion of (- 1 (* 3 (/ 1 (pow v 2)))) in v
1.315 * [taylor]: Taking taylor expansion of 1 in v
1.315 * [backup-simplify]: Simplify 1 into 1
1.315 * [taylor]: Taking taylor expansion of (* 3 (/ 1 (pow v 2))) in v
1.315 * [taylor]: Taking taylor expansion of 3 in v
1.315 * [backup-simplify]: Simplify 3 into 3
1.315 * [taylor]: Taking taylor expansion of (/ 1 (pow v 2)) in v
1.315 * [taylor]: Taking taylor expansion of (pow v 2) in v
1.315 * [taylor]: Taking taylor expansion of v in v
1.315 * [backup-simplify]: Simplify 0 into 0
1.315 * [backup-simplify]: Simplify 1 into 1
1.316 * [backup-simplify]: Simplify (* 1 1) into 1
1.316 * [backup-simplify]: Simplify (/ 1 1) into 1
1.316 * [backup-simplify]: Simplify (* 3 1) into 3
1.316 * [backup-simplify]: Simplify (- 3) into -3
1.317 * [backup-simplify]: Simplify (+ 0 -3) into -3
1.317 * [backup-simplify]: Simplify (sqrt -3) into (sqrt -3)
1.317 * [backup-simplify]: Simplify (+ (* 1 0) (* 0 1)) into 0
1.318 * [backup-simplify]: Simplify (- (+ (* 1 (/ 0 1)))) into 0
1.318 * [backup-simplify]: Simplify (+ (* 3 0) (* 0 1)) into 0
1.319 * [backup-simplify]: Simplify (- 0) into 0
1.319 * [backup-simplify]: Simplify (+ 0 0) into 0
1.319 * [backup-simplify]: Simplify (/ 0 (* 2 (sqrt -3))) into 0
1.319 * [taylor]: Taking taylor expansion of (* 1/4 (* (sqrt 2) (sqrt (- 1 (* 3 (/ 1 (pow v 2))))))) in v
1.319 * [taylor]: Taking taylor expansion of 1/4 in v
1.320 * [backup-simplify]: Simplify 1/4 into 1/4
1.320 * [taylor]: Taking taylor expansion of (* (sqrt 2) (sqrt (- 1 (* 3 (/ 1 (pow v 2)))))) in v
1.320 * [taylor]: Taking taylor expansion of (sqrt 2) in v
1.320 * [taylor]: Taking taylor expansion of 2 in v
1.320 * [backup-simplify]: Simplify 2 into 2
1.320 * [backup-simplify]: Simplify (sqrt 2) into (sqrt 2)
1.320 * [backup-simplify]: Simplify (/ 0 (* 2 (sqrt 2))) into 0
1.320 * [taylor]: Taking taylor expansion of (sqrt (- 1 (* 3 (/ 1 (pow v 2))))) in v
1.320 * [taylor]: Taking taylor expansion of (- 1 (* 3 (/ 1 (pow v 2)))) in v
1.320 * [taylor]: Taking taylor expansion of 1 in v
1.320 * [backup-simplify]: Simplify 1 into 1
1.320 * [taylor]: Taking taylor expansion of (* 3 (/ 1 (pow v 2))) in v
1.320 * [taylor]: Taking taylor expansion of 3 in v
1.320 * [backup-simplify]: Simplify 3 into 3
1.320 * [taylor]: Taking taylor expansion of (/ 1 (pow v 2)) in v
1.320 * [taylor]: Taking taylor expansion of (pow v 2) in v
1.320 * [taylor]: Taking taylor expansion of v in v
1.320 * [backup-simplify]: Simplify 0 into 0
1.320 * [backup-simplify]: Simplify 1 into 1
1.321 * [backup-simplify]: Simplify (* 1 1) into 1
1.321 * [backup-simplify]: Simplify (/ 1 1) into 1
1.321 * [backup-simplify]: Simplify (* 3 1) into 3
1.321 * [backup-simplify]: Simplify (- 3) into -3
1.322 * [backup-simplify]: Simplify (+ 0 -3) into -3
1.322 * [backup-simplify]: Simplify (sqrt -3) into (sqrt -3)
1.322 * [backup-simplify]: Simplify (+ (* 1 0) (* 0 1)) into 0
1.323 * [backup-simplify]: Simplify (- (+ (* 1 (/ 0 1)))) into 0
1.323 * [backup-simplify]: Simplify (+ (* 3 0) (* 0 1)) into 0
1.324 * [backup-simplify]: Simplify (- 0) into 0
1.324 * [backup-simplify]: Simplify (+ 0 0) into 0
1.324 * [backup-simplify]: Simplify (/ 0 (* 2 (sqrt -3))) into 0
1.325 * [backup-simplify]: Simplify (* (sqrt 2) (sqrt -3)) into (* (sqrt 2) (sqrt -3))
1.327 * [backup-simplify]: Simplify (* 1/4 (* (sqrt 2) (sqrt -3))) into (* 1/4 (* (sqrt 2) (sqrt -3)))
1.328 * [backup-simplify]: Simplify (* 1/4 (* (sqrt 2) (sqrt -3))) into (* 1/4 (* (sqrt 2) (sqrt -3)))
1.329 * [backup-simplify]: Simplify (+ (* (sqrt 2) 0) (* 0 (sqrt -3))) into 0
1.329 * [backup-simplify]: Simplify (+ (* 1/4 0) (* 0 (* (sqrt 2) (sqrt -3)))) into 0
1.329 * [backup-simplify]: Simplify 0 into 0
1.330 * [backup-simplify]: Simplify (+ (* 1 0) (+ (* 0 0) (* 0 1))) into 0
1.330 * [backup-simplify]: Simplify (- (+ (* 1 (/ 0 1)) (* 0 (/ 0 1)))) into 0
1.331 * [backup-simplify]: Simplify (+ (* 3 0) (+ (* 0 0) (* 0 1))) into 0
1.331 * [backup-simplify]: Simplify (- 0) into 0
1.332 * [backup-simplify]: Simplify (+ 1 0) into 1
1.333 * [backup-simplify]: Simplify (/ (- 1 (pow 0 2) (+)) (* 2 (sqrt -3))) into (/ 1/2 (sqrt -3))
1.334 * [backup-simplify]: Simplify (/ (- 0 (pow 0 2) (+)) (* 2 (sqrt 2))) into 0
1.337 * [backup-simplify]: Simplify (+ (* (sqrt 2) (/ 1/2 (sqrt -3))) (+ (* 0 0) (* 0 (sqrt -3)))) into (* 1/2 (/ (sqrt 2) (sqrt -3)))
1.344 * [backup-simplify]: Simplify (+ (* 1/4 (* 1/2 (/ (sqrt 2) (sqrt -3)))) (+ (* 0 0) (* 0 (* (sqrt 2) (sqrt -3))))) into (* 1/8 (/ (sqrt 2) (sqrt -3)))
1.346 * [backup-simplify]: Simplify (* 1/8 (/ (sqrt 2) (sqrt -3))) into (* 1/8 (/ (sqrt 2) (sqrt -3)))
1.347 * [backup-simplify]: Simplify (+ (* 1 0) (+ (* 0 0) (+ (* 0 0) (* 0 1)))) into 0
1.348 * [backup-simplify]: Simplify (- (+ (* 1 (/ 0 1)) (* 0 (/ 0 1)) (* 0 (/ 0 1)))) into 0
1.349 * [backup-simplify]: Simplify (+ (* 3 0) (+ (* 0 0) (+ (* 0 0) (* 0 1)))) into 0
1.349 * [backup-simplify]: Simplify (- 0) into 0
1.350 * [backup-simplify]: Simplify (+ 0 0) into 0
1.351 * [backup-simplify]: Simplify (/ (- 0 (+ (* 2 (* 0 (/ 1/2 (sqrt -3)))))) (* 2 (sqrt -3))) into 0
1.352 * [backup-simplify]: Simplify (/ (- 0 (+ (* 2 (* 0 0)))) (* 2 (sqrt 2))) into 0
1.354 * [backup-simplify]: Simplify (+ (* (sqrt 2) 0) (+ (* 0 (/ 1/2 (sqrt -3))) (+ (* 0 0) (* 0 (sqrt -3))))) into 0
1.357 * [backup-simplify]: Simplify (+ (* 1/4 0) (+ (* 0 (* 1/2 (/ (sqrt 2) (sqrt -3)))) (+ (* 0 0) (* 0 (* (sqrt 2) (sqrt -3)))))) into 0
1.357 * [backup-simplify]: Simplify 0 into 0
1.358 * [backup-simplify]: Simplify (+ (* 1 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (* 0 1))))) into 0
1.359 * [backup-simplify]: Simplify (- (+ (* 1 (/ 0 1)) (* 0 (/ 0 1)) (* 0 (/ 0 1)) (* 0 (/ 0 1)))) into 0
1.360 * [backup-simplify]: Simplify (+ (* 3 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (* 0 1))))) into 0
1.360 * [backup-simplify]: Simplify (- 0) into 0
1.360 * [backup-simplify]: Simplify (+ 0 0) into 0
1.364 * [backup-simplify]: Simplify (/ (- 0 (pow (/ 1/2 (sqrt -3)) 2) (+ (* 2 (* 0 0)))) (* 2 (sqrt -3))) into (/ -1/8 (pow (sqrt -3) 3))
1.365 * [backup-simplify]: Simplify (/ (- 0 (pow 0 2) (+ (* 2 (* 0 0)))) (* 2 (sqrt 2))) into 0
1.370 * [backup-simplify]: Simplify (+ (* (sqrt 2) (/ -1/8 (pow (sqrt -3) 3))) (+ (* 0 0) (+ (* 0 (/ 1/2 (sqrt -3))) (+ (* 0 0) (* 0 (sqrt -3)))))) into (- (* 1/8 (/ (sqrt 2) (pow (sqrt -3) 3))))
1.382 * [backup-simplify]: Simplify (+ (* 1/4 (- (* 1/8 (/ (sqrt 2) (pow (sqrt -3) 3))))) (+ (* 0 0) (+ (* 0 (* 1/2 (/ (sqrt 2) (sqrt -3)))) (+ (* 0 0) (* 0 (* (sqrt 2) (sqrt -3))))))) into (- (* 1/32 (/ (sqrt 2) (pow (sqrt -3) 3))))
1.387 * [backup-simplify]: Simplify (- (* 1/32 (/ (sqrt 2) (pow (sqrt -3) 3)))) into (- (* 1/32 (/ (sqrt 2) (pow (sqrt -3) 3))))
1.396 * [backup-simplify]: Simplify (+ (* (- (* 1/32 (/ (sqrt 2) (pow (sqrt -3) 3)))) (pow (/ 1 v) 3)) (+ (* (* 1/8 (/ (sqrt 2) (sqrt -3))) (/ 1 v)) (* (* 1/4 (* (sqrt 2) (sqrt -3))) (/ 1 (/ 1 v))))) into (- (+ (* 1/4 (* (sqrt 2) (* v (sqrt -3)))) (* 1/8 (/ (sqrt 2) (* v (sqrt -3))))) (* 1/32 (/ (sqrt 2) (* (pow v 3) (pow (sqrt -3) 3)))))
1.397 * [backup-simplify]: Simplify (* (/ (sqrt 2) 4) (sqrt (- 1 (* 3 (* (/ 1 (- v)) (/ 1 (- v))))))) into (* 1/4 (* (sqrt 2) (sqrt (- 1 (* 3 (/ 1 (pow v 2)))))))
1.397 * [approximate]: Taking taylor expansion of (* 1/4 (* (sqrt 2) (sqrt (- 1 (* 3 (/ 1 (pow v 2))))))) in (v) around 0
1.397 * [taylor]: Taking taylor expansion of (* 1/4 (* (sqrt 2) (sqrt (- 1 (* 3 (/ 1 (pow v 2))))))) in v
1.397 * [taylor]: Taking taylor expansion of 1/4 in v
1.397 * [backup-simplify]: Simplify 1/4 into 1/4
1.397 * [taylor]: Taking taylor expansion of (* (sqrt 2) (sqrt (- 1 (* 3 (/ 1 (pow v 2)))))) in v
1.397 * [taylor]: Taking taylor expansion of (sqrt 2) in v
1.397 * [taylor]: Taking taylor expansion of 2 in v
1.398 * [backup-simplify]: Simplify 2 into 2
1.398 * [backup-simplify]: Simplify (sqrt 2) into (sqrt 2)
1.399 * [backup-simplify]: Simplify (/ 0 (* 2 (sqrt 2))) into 0
1.399 * [taylor]: Taking taylor expansion of (sqrt (- 1 (* 3 (/ 1 (pow v 2))))) in v
1.399 * [taylor]: Taking taylor expansion of (- 1 (* 3 (/ 1 (pow v 2)))) in v
1.399 * [taylor]: Taking taylor expansion of 1 in v
1.399 * [backup-simplify]: Simplify 1 into 1
1.399 * [taylor]: Taking taylor expansion of (* 3 (/ 1 (pow v 2))) in v
1.399 * [taylor]: Taking taylor expansion of 3 in v
1.399 * [backup-simplify]: Simplify 3 into 3
1.399 * [taylor]: Taking taylor expansion of (/ 1 (pow v 2)) in v
1.399 * [taylor]: Taking taylor expansion of (pow v 2) in v
1.399 * [taylor]: Taking taylor expansion of v in v
1.399 * [backup-simplify]: Simplify 0 into 0
1.399 * [backup-simplify]: Simplify 1 into 1
1.399 * [backup-simplify]: Simplify (* 1 1) into 1
1.400 * [backup-simplify]: Simplify (/ 1 1) into 1
1.400 * [backup-simplify]: Simplify (* 3 1) into 3
1.400 * [backup-simplify]: Simplify (- 3) into -3
1.401 * [backup-simplify]: Simplify (+ 0 -3) into -3
1.401 * [backup-simplify]: Simplify (sqrt -3) into (sqrt -3)
1.402 * [backup-simplify]: Simplify (+ (* 1 0) (* 0 1)) into 0
1.403 * [backup-simplify]: Simplify (- (+ (* 1 (/ 0 1)))) into 0
1.403 * [backup-simplify]: Simplify (+ (* 3 0) (* 0 1)) into 0
1.404 * [backup-simplify]: Simplify (- 0) into 0
1.404 * [backup-simplify]: Simplify (+ 0 0) into 0
1.405 * [backup-simplify]: Simplify (/ 0 (* 2 (sqrt -3))) into 0
1.405 * [taylor]: Taking taylor expansion of (* 1/4 (* (sqrt 2) (sqrt (- 1 (* 3 (/ 1 (pow v 2))))))) in v
1.405 * [taylor]: Taking taylor expansion of 1/4 in v
1.405 * [backup-simplify]: Simplify 1/4 into 1/4
1.405 * [taylor]: Taking taylor expansion of (* (sqrt 2) (sqrt (- 1 (* 3 (/ 1 (pow v 2)))))) in v
1.405 * [taylor]: Taking taylor expansion of (sqrt 2) in v
1.405 * [taylor]: Taking taylor expansion of 2 in v
1.405 * [backup-simplify]: Simplify 2 into 2
1.405 * [backup-simplify]: Simplify (sqrt 2) into (sqrt 2)
1.406 * [backup-simplify]: Simplify (/ 0 (* 2 (sqrt 2))) into 0
1.406 * [taylor]: Taking taylor expansion of (sqrt (- 1 (* 3 (/ 1 (pow v 2))))) in v
1.406 * [taylor]: Taking taylor expansion of (- 1 (* 3 (/ 1 (pow v 2)))) in v
1.406 * [taylor]: Taking taylor expansion of 1 in v
1.406 * [backup-simplify]: Simplify 1 into 1
1.406 * [taylor]: Taking taylor expansion of (* 3 (/ 1 (pow v 2))) in v
1.406 * [taylor]: Taking taylor expansion of 3 in v
1.406 * [backup-simplify]: Simplify 3 into 3
1.406 * [taylor]: Taking taylor expansion of (/ 1 (pow v 2)) in v
1.406 * [taylor]: Taking taylor expansion of (pow v 2) in v
1.406 * [taylor]: Taking taylor expansion of v in v
1.406 * [backup-simplify]: Simplify 0 into 0
1.406 * [backup-simplify]: Simplify 1 into 1
1.407 * [backup-simplify]: Simplify (* 1 1) into 1
1.407 * [backup-simplify]: Simplify (/ 1 1) into 1
1.408 * [backup-simplify]: Simplify (* 3 1) into 3
1.408 * [backup-simplify]: Simplify (- 3) into -3
1.408 * [backup-simplify]: Simplify (+ 0 -3) into -3
1.409 * [backup-simplify]: Simplify (sqrt -3) into (sqrt -3)
1.409 * [backup-simplify]: Simplify (+ (* 1 0) (* 0 1)) into 0
1.410 * [backup-simplify]: Simplify (- (+ (* 1 (/ 0 1)))) into 0
1.411 * [backup-simplify]: Simplify (+ (* 3 0) (* 0 1)) into 0
1.411 * [backup-simplify]: Simplify (- 0) into 0
1.412 * [backup-simplify]: Simplify (+ 0 0) into 0
1.413 * [backup-simplify]: Simplify (/ 0 (* 2 (sqrt -3))) into 0
1.414 * [backup-simplify]: Simplify (* (sqrt 2) (sqrt -3)) into (* (sqrt 2) (sqrt -3))
1.416 * [backup-simplify]: Simplify (* 1/4 (* (sqrt 2) (sqrt -3))) into (* 1/4 (* (sqrt 2) (sqrt -3)))
1.418 * [backup-simplify]: Simplify (* 1/4 (* (sqrt 2) (sqrt -3))) into (* 1/4 (* (sqrt 2) (sqrt -3)))
1.419 * [backup-simplify]: Simplify (+ (* (sqrt 2) 0) (* 0 (sqrt -3))) into 0
1.421 * [backup-simplify]: Simplify (+ (* 1/4 0) (* 0 (* (sqrt 2) (sqrt -3)))) into 0
1.421 * [backup-simplify]: Simplify 0 into 0
1.422 * [backup-simplify]: Simplify (+ (* 1 0) (+ (* 0 0) (* 0 1))) into 0
1.423 * [backup-simplify]: Simplify (- (+ (* 1 (/ 0 1)) (* 0 (/ 0 1)))) into 0
1.424 * [backup-simplify]: Simplify (+ (* 3 0) (+ (* 0 0) (* 0 1))) into 0
1.424 * [backup-simplify]: Simplify (- 0) into 0
1.425 * [backup-simplify]: Simplify (+ 1 0) into 1
1.428 * [backup-simplify]: Simplify (/ (- 1 (pow 0 2) (+)) (* 2 (sqrt -3))) into (/ 1/2 (sqrt -3))
1.429 * [backup-simplify]: Simplify (/ (- 0 (pow 0 2) (+)) (* 2 (sqrt 2))) into 0
1.439 * [backup-simplify]: Simplify (+ (* (sqrt 2) (/ 1/2 (sqrt -3))) (+ (* 0 0) (* 0 (sqrt -3)))) into (* 1/2 (/ (sqrt 2) (sqrt -3)))
1.446 * [backup-simplify]: Simplify (+ (* 1/4 (* 1/2 (/ (sqrt 2) (sqrt -3)))) (+ (* 0 0) (* 0 (* (sqrt 2) (sqrt -3))))) into (* 1/8 (/ (sqrt 2) (sqrt -3)))
1.448 * [backup-simplify]: Simplify (* 1/8 (/ (sqrt 2) (sqrt -3))) into (* 1/8 (/ (sqrt 2) (sqrt -3)))
1.449 * [backup-simplify]: Simplify (+ (* 1 0) (+ (* 0 0) (+ (* 0 0) (* 0 1)))) into 0
1.450 * [backup-simplify]: Simplify (- (+ (* 1 (/ 0 1)) (* 0 (/ 0 1)) (* 0 (/ 0 1)))) into 0
1.451 * [backup-simplify]: Simplify (+ (* 3 0) (+ (* 0 0) (+ (* 0 0) (* 0 1)))) into 0
1.452 * [backup-simplify]: Simplify (- 0) into 0
1.452 * [backup-simplify]: Simplify (+ 0 0) into 0
1.454 * [backup-simplify]: Simplify (/ (- 0 (+ (* 2 (* 0 (/ 1/2 (sqrt -3)))))) (* 2 (sqrt -3))) into 0
1.455 * [backup-simplify]: Simplify (/ (- 0 (+ (* 2 (* 0 0)))) (* 2 (sqrt 2))) into 0
1.457 * [backup-simplify]: Simplify (+ (* (sqrt 2) 0) (+ (* 0 (/ 1/2 (sqrt -3))) (+ (* 0 0) (* 0 (sqrt -3))))) into 0
1.460 * [backup-simplify]: Simplify (+ (* 1/4 0) (+ (* 0 (* 1/2 (/ (sqrt 2) (sqrt -3)))) (+ (* 0 0) (* 0 (* (sqrt 2) (sqrt -3)))))) into 0
1.460 * [backup-simplify]: Simplify 0 into 0
1.461 * [backup-simplify]: Simplify (+ (* 1 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (* 0 1))))) into 0
1.462 * [backup-simplify]: Simplify (- (+ (* 1 (/ 0 1)) (* 0 (/ 0 1)) (* 0 (/ 0 1)) (* 0 (/ 0 1)))) into 0
1.464 * [backup-simplify]: Simplify (+ (* 3 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (* 0 1))))) into 0
1.464 * [backup-simplify]: Simplify (- 0) into 0
1.464 * [backup-simplify]: Simplify (+ 0 0) into 0
1.471 * [backup-simplify]: Simplify (/ (- 0 (pow (/ 1/2 (sqrt -3)) 2) (+ (* 2 (* 0 0)))) (* 2 (sqrt -3))) into (/ -1/8 (pow (sqrt -3) 3))
1.472 * [backup-simplify]: Simplify (/ (- 0 (pow 0 2) (+ (* 2 (* 0 0)))) (* 2 (sqrt 2))) into 0
1.480 * [backup-simplify]: Simplify (+ (* (sqrt 2) (/ -1/8 (pow (sqrt -3) 3))) (+ (* 0 0) (+ (* 0 (/ 1/2 (sqrt -3))) (+ (* 0 0) (* 0 (sqrt -3)))))) into (- (* 1/8 (/ (sqrt 2) (pow (sqrt -3) 3))))
1.491 * [backup-simplify]: Simplify (+ (* 1/4 (- (* 1/8 (/ (sqrt 2) (pow (sqrt -3) 3))))) (+ (* 0 0) (+ (* 0 (* 1/2 (/ (sqrt 2) (sqrt -3)))) (+ (* 0 0) (* 0 (* (sqrt 2) (sqrt -3))))))) into (- (* 1/32 (/ (sqrt 2) (pow (sqrt -3) 3))))
1.496 * [backup-simplify]: Simplify (- (* 1/32 (/ (sqrt 2) (pow (sqrt -3) 3)))) into (- (* 1/32 (/ (sqrt 2) (pow (sqrt -3) 3))))
1.505 * [backup-simplify]: Simplify (+ (* (- (* 1/32 (/ (sqrt 2) (pow (sqrt -3) 3)))) (pow (/ 1 (- v)) 3)) (+ (* (* 1/8 (/ (sqrt 2) (sqrt -3))) (/ 1 (- v))) (* (* 1/4 (* (sqrt 2) (sqrt -3))) (/ 1 (/ 1 (- v)))))) into (- (* 1/32 (/ (sqrt 2) (* (pow v 3) (pow (sqrt -3) 3)))) (+ (* 1/4 (* (sqrt 2) (* v (sqrt -3)))) (* 1/8 (/ (sqrt 2) (* v (sqrt -3))))))
1.505 * * * [progress]: simplifying candidates
1.505 * * * * [progress]: [ 1 / 79 ] simplifiying candidate #<alt (λ (v) (* (* (/ (sqrt 2) 4) (sqrt (- 1 (pow (* 3 (* v v)) 1)))) (- 1 (* v v))))>
1.505 * * * * [progress]: [ 2 / 79 ] simplifiying candidate #<alt (λ (v) (* (* (/ (sqrt 2) 4) (sqrt (- 1 (pow (* 3 (* v v)) 1)))) (- 1 (* v v))))>
1.505 * * * * [progress]: [ 3 / 79 ] simplifiying candidate #<alt (λ (v) (* (* (/ (sqrt 2) 4) (sqrt (- 1 (pow (* 3 (* v v)) 1)))) (- 1 (* v v))))>
1.505 * * * * [progress]: [ 4 / 79 ] simplifiying candidate #<alt (λ (v) (* (* (/ (sqrt 2) 4) (sqrt (- 1 (exp (+ (log 3) (+ (log v) (log v))))))) (- 1 (* v v))))>
1.505 * * * * [progress]: [ 5 / 79 ] simplifiying candidate #<alt (λ (v) (* (* (/ (sqrt 2) 4) (sqrt (- 1 (exp (+ (log 3) (log (* v v))))))) (- 1 (* v v))))>
1.505 * * * * [progress]: [ 6 / 79 ] simplifiying candidate #<alt (λ (v) (* (* (/ (sqrt 2) 4) (sqrt (- 1 (exp (log (* 3 (* v v))))))) (- 1 (* v v))))>
1.505 * * * * [progress]: [ 7 / 79 ] simplifiying candidate #<alt (λ (v) (* (* (/ (sqrt 2) 4) (sqrt (- 1 (log (exp (* 3 (* v v))))))) (- 1 (* v v))))>
1.505 * * * * [progress]: [ 8 / 79 ] simplifiying candidate #<alt (λ (v) (* (* (/ (sqrt 2) 4) (sqrt (- 1 (cbrt (* (* (* 3 3) 3) (* (* (* v v) v) (* (* v v) v))))))) (- 1 (* v v))))>
1.505 * * * * [progress]: [ 9 / 79 ] simplifiying candidate #<alt (λ (v) (* (* (/ (sqrt 2) 4) (sqrt (- 1 (cbrt (* (* (* 3 3) 3) (* (* (* v v) (* v v)) (* v v))))))) (- 1 (* v v))))>
1.505 * * * * [progress]: [ 10 / 79 ] simplifiying candidate #<alt (λ (v) (* (* (/ (sqrt 2) 4) (sqrt (- 1 (* (* (cbrt (* 3 (* v v))) (cbrt (* 3 (* v v)))) (cbrt (* 3 (* v v))))))) (- 1 (* v v))))>
1.506 * * * * [progress]: [ 11 / 79 ] simplifiying candidate #<alt (λ (v) (* (* (/ (sqrt 2) 4) (sqrt (- 1 (cbrt (* (* (* 3 (* v v)) (* 3 (* v v))) (* 3 (* v v))))))) (- 1 (* v v))))>
1.506 * * * * [progress]: [ 12 / 79 ] simplifiying candidate #<alt (λ (v) (* (* (/ (sqrt 2) 4) (sqrt (- 1 (* (sqrt (* 3 (* v v))) (sqrt (* 3 (* v v))))))) (- 1 (* v v))))>
1.506 * * * * [progress]: [ 13 / 79 ] simplifiying candidate #<alt (λ (v) (* (* (/ (sqrt 2) 4) (sqrt (- 1 (* 1 (* 3 (* v v)))))) (- 1 (* v v))))>
1.506 * * * * [progress]: [ 14 / 79 ] simplifiying candidate #<alt (λ (v) (* (* (/ (sqrt 2) 4) (sqrt (- 1 (* (* (sqrt 3) v) (* (sqrt 3) v))))) (- 1 (* v v))))>
1.506 * * * * [progress]: [ 15 / 79 ] simplifiying candidate #<alt (λ (v) (* (* (/ (sqrt 2) 4) (sqrt (- 1 (* (* 3 v) v)))) (- 1 (* v v))))>
1.506 * * * * [progress]: [ 16 / 79 ] simplifiying candidate #<alt (λ (v) (* (* (/ (sqrt 2) 4) (sqrt (- 1 (* (* (cbrt 3) (cbrt 3)) (* (cbrt 3) (* v v)))))) (- 1 (* v v))))>
1.506 * * * * [progress]: [ 17 / 79 ] simplifiying candidate #<alt (λ (v) (* (* (/ (sqrt 2) 4) (sqrt (- 1 (* (sqrt 3) (* (sqrt 3) (* v v)))))) (- 1 (* v v))))>
1.506 * * * * [progress]: [ 18 / 79 ] simplifiying candidate #<alt (λ (v) (* (* (/ (sqrt 2) 4) (sqrt (- 1 (* 1 (* 3 (* v v)))))) (- 1 (* v v))))>
1.506 * * * * [progress]: [ 19 / 79 ] simplifiying candidate #<alt (λ (v) (* (* (/ (sqrt 2) 4) (sqrt (- 1 (posit16->real (real->posit16 (* 3 (* v v))))))) (- 1 (* v v))))>
1.506 * * * * [progress]: [ 20 / 79 ] simplifiying candidate #<alt (λ (v) (* (* (/ (sqrt 2) 4) (sqrt (- 1 (* (* v v) 3)))) (- 1 (* v v))))>
1.506 * * * * [progress]: [ 21 / 79 ] simplifiying candidate #<alt (λ (v) (* (pow (* (/ (sqrt 2) 4) (sqrt (- 1 (* 3 (* v v))))) 1) (- 1 (* v v))))>
1.506 * * * * [progress]: [ 22 / 79 ] simplifiying candidate #<alt (λ (v) (* (pow (* (/ (sqrt 2) 4) (sqrt (- 1 (* 3 (* v v))))) 1) (- 1 (* v v))))>
1.506 * * * * [progress]: [ 23 / 79 ] simplifiying candidate #<alt (λ (v) (* (exp (+ (- (log (sqrt 2)) (log 4)) (log (sqrt (- 1 (* 3 (* v v))))))) (- 1 (* v v))))>
1.506 * * * * [progress]: [ 24 / 79 ] simplifiying candidate #<alt (λ (v) (* (exp (+ (log (/ (sqrt 2) 4)) (log (sqrt (- 1 (* 3 (* v v))))))) (- 1 (* v v))))>
1.506 * * * * [progress]: [ 25 / 79 ] simplifiying candidate #<alt (λ (v) (* (exp (log (* (/ (sqrt 2) 4) (sqrt (- 1 (* 3 (* v v))))))) (- 1 (* v v))))>
1.506 * * * * [progress]: [ 26 / 79 ] simplifiying candidate #<alt (λ (v) (* (log (exp (* (/ (sqrt 2) 4) (sqrt (- 1 (* 3 (* v v))))))) (- 1 (* v v))))>
1.506 * * * * [progress]: [ 27 / 79 ] simplifiying candidate #<alt (λ (v) (* (cbrt (* (/ (* (* (sqrt 2) (sqrt 2)) (sqrt 2)) (* (* 4 4) 4)) (* (* (sqrt (- 1 (* 3 (* v v)))) (sqrt (- 1 (* 3 (* v v))))) (sqrt (- 1 (* 3 (* v v))))))) (- 1 (* v v))))>
1.507 * * * * [progress]: [ 28 / 79 ] simplifiying candidate #<alt (λ (v) (* (cbrt (* (* (* (/ (sqrt 2) 4) (/ (sqrt 2) 4)) (/ (sqrt 2) 4)) (* (* (sqrt (- 1 (* 3 (* v v)))) (sqrt (- 1 (* 3 (* v v))))) (sqrt (- 1 (* 3 (* v v))))))) (- 1 (* v v))))>
1.507 * * * * [progress]: [ 29 / 79 ] simplifiying candidate #<alt (λ (v) (* (* (* (cbrt (* (/ (sqrt 2) 4) (sqrt (- 1 (* 3 (* v v)))))) (cbrt (* (/ (sqrt 2) 4) (sqrt (- 1 (* 3 (* v v))))))) (cbrt (* (/ (sqrt 2) 4) (sqrt (- 1 (* 3 (* v v))))))) (- 1 (* v v))))>
1.507 * * * * [progress]: [ 30 / 79 ] simplifiying candidate #<alt (λ (v) (* (cbrt (* (* (* (/ (sqrt 2) 4) (sqrt (- 1 (* 3 (* v v))))) (* (/ (sqrt 2) 4) (sqrt (- 1 (* 3 (* v v)))))) (* (/ (sqrt 2) 4) (sqrt (- 1 (* 3 (* v v))))))) (- 1 (* v v))))>
1.507 * * * * [progress]: [ 31 / 79 ] simplifiying candidate #<alt (λ (v) (* (* (sqrt (* (/ (sqrt 2) 4) (sqrt (- 1 (* 3 (* v v)))))) (sqrt (* (/ (sqrt 2) 4) (sqrt (- 1 (* 3 (* v v))))))) (- 1 (* v v))))>
1.507 * * * * [progress]: [ 32 / 79 ] simplifiying candidate #<alt (λ (v) (* (/ (* (sqrt 2) (sqrt (- (pow 1 3) (pow (* 3 (* v v)) 3)))) (* 4 (sqrt (+ (* 1 1) (+ (* (* 3 (* v v)) (* 3 (* v v))) (* 1 (* 3 (* v v)))))))) (- 1 (* v v))))>
1.507 * * * * [progress]: [ 33 / 79 ] simplifiying candidate #<alt (λ (v) (* (/ (* (sqrt 2) (sqrt (- (* 1 1) (* (* 3 (* v v)) (* 3 (* v v)))))) (* 4 (sqrt (+ 1 (* 3 (* v v)))))) (- 1 (* v v))))>
1.507 * * * * [progress]: [ 34 / 79 ] simplifiying candidate #<alt (λ (v) (* (* 1 (* (/ (sqrt 2) 4) (sqrt (- 1 (* 3 (* v v)))))) (- 1 (* v v))))>
1.507 * * * * [progress]: [ 35 / 79 ] simplifiying candidate #<alt (λ (v) (* (* (* (sqrt (/ (sqrt 2) 4)) (sqrt (sqrt (- 1 (* 3 (* v v)))))) (* (sqrt (/ (sqrt 2) 4)) (sqrt (sqrt (- 1 (* 3 (* v v))))))) (- 1 (* v v))))>
1.507 * * * * [progress]: [ 36 / 79 ] simplifiying candidate #<alt (λ (v) (* (* (* (sqrt (/ (sqrt 2) 4)) (sqrt (sqrt (- 1 (* 3 (* v v)))))) (* (sqrt (/ (sqrt 2) 4)) (sqrt (sqrt (- 1 (* 3 (* v v))))))) (- 1 (* v v))))>
1.507 * * * * [progress]: [ 37 / 79 ] simplifiying candidate #<alt (λ (v) (* (* (* (/ (sqrt (sqrt 2)) (sqrt 4)) (sqrt (sqrt (- 1 (* 3 (* v v)))))) (* (/ (sqrt (sqrt 2)) (sqrt 4)) (sqrt (sqrt (- 1 (* 3 (* v v))))))) (- 1 (* v v))))>
1.507 * * * * [progress]: [ 38 / 79 ] simplifiying candidate #<alt (λ (v) (* (* (* (/ (sqrt (sqrt 2)) (sqrt 4)) (sqrt (sqrt (- 1 (* 3 (* v v)))))) (* (/ (sqrt (sqrt 2)) (sqrt 4)) (sqrt (sqrt (- 1 (* 3 (* v v))))))) (- 1 (* v v))))>
1.507 * * * * [progress]: [ 39 / 79 ] simplifiying candidate #<alt (λ (v) (* (* (* (/ (sqrt (sqrt 2)) (sqrt 4)) (sqrt (sqrt (- 1 (* 3 (* v v)))))) (* (/ (sqrt (sqrt 2)) (sqrt 4)) (sqrt (sqrt (- 1 (* 3 (* v v))))))) (- 1 (* v v))))>
1.507 * * * * [progress]: [ 40 / 79 ] simplifiying candidate #<alt (λ (v) (* (* (* (/ (sqrt (sqrt 2)) (sqrt 4)) (sqrt (sqrt (- 1 (* 3 (* v v)))))) (* (/ (sqrt (sqrt 2)) (sqrt 4)) (sqrt (sqrt (- 1 (* 3 (* v v))))))) (- 1 (* v v))))>
1.507 * * * * [progress]: [ 41 / 79 ] simplifiying candidate #<alt (λ (v) (* (* (* (/ (sqrt 2) 4) (* (cbrt (sqrt (- 1 (* 3 (* v v))))) (cbrt (sqrt (- 1 (* 3 (* v v))))))) (cbrt (sqrt (- 1 (* 3 (* v v)))))) (- 1 (* v v))))>
1.507 * * * * [progress]: [ 42 / 79 ] simplifiying candidate #<alt (λ (v) (* (* (* (/ (sqrt 2) 4) (sqrt (* (cbrt (- 1 (* 3 (* v v)))) (cbrt (- 1 (* 3 (* v v))))))) (sqrt (cbrt (- 1 (* 3 (* v v)))))) (- 1 (* v v))))>
1.508 * * * * [progress]: [ 43 / 79 ] simplifiying candidate #<alt (λ (v) (* (* (* (/ (sqrt 2) 4) (sqrt (sqrt (- 1 (* 3 (* v v)))))) (sqrt (sqrt (- 1 (* 3 (* v v)))))) (- 1 (* v v))))>
1.508 * * * * [progress]: [ 44 / 79 ] simplifiying candidate #<alt (λ (v) (* (* (* (/ (sqrt 2) 4) (sqrt 1)) (sqrt (- 1 (* 3 (* v v))))) (- 1 (* v v))))>
1.508 * * * * [progress]: [ 45 / 79 ] simplifiying candidate #<alt (λ (v) (* (* (* (/ (sqrt 2) 4) (sqrt (sqrt (- 1 (* 3 (* v v)))))) (sqrt (sqrt (- 1 (* 3 (* v v)))))) (- 1 (* v v))))>
1.508 * * * * [progress]: [ 46 / 79 ] simplifiying candidate #<alt (λ (v) (* (* (* (/ (sqrt 2) 4) 1) (sqrt (- 1 (* 3 (* v v))))) (- 1 (* v v))))>
1.508 * * * * [progress]: [ 47 / 79 ] simplifiying candidate #<alt (λ (v) (* (* (* (cbrt (/ (sqrt 2) 4)) (cbrt (/ (sqrt 2) 4))) (* (cbrt (/ (sqrt 2) 4)) (sqrt (- 1 (* 3 (* v v)))))) (- 1 (* v v))))>
1.508 * * * * [progress]: [ 48 / 79 ] simplifiying candidate #<alt (λ (v) (* (* (sqrt (/ (sqrt 2) 4)) (* (sqrt (/ (sqrt 2) 4)) (sqrt (- 1 (* 3 (* v v)))))) (- 1 (* v v))))>
1.508 * * * * [progress]: [ 49 / 79 ] simplifiying candidate #<alt (λ (v) (* (* (/ (* (cbrt (sqrt 2)) (cbrt (sqrt 2))) (* (cbrt 4) (cbrt 4))) (* (/ (cbrt (sqrt 2)) (cbrt 4)) (sqrt (- 1 (* 3 (* v v)))))) (- 1 (* v v))))>
1.508 * * * * [progress]: [ 50 / 79 ] simplifiying candidate #<alt (λ (v) (* (* (/ (* (cbrt (sqrt 2)) (cbrt (sqrt 2))) (sqrt 4)) (* (/ (cbrt (sqrt 2)) (sqrt 4)) (sqrt (- 1 (* 3 (* v v)))))) (- 1 (* v v))))>
1.508 * * * * [progress]: [ 51 / 79 ] simplifiying candidate #<alt (λ (v) (* (* (/ (* (cbrt (sqrt 2)) (cbrt (sqrt 2))) 1) (* (/ (cbrt (sqrt 2)) 4) (sqrt (- 1 (* 3 (* v v)))))) (- 1 (* v v))))>
1.508 * * * * [progress]: [ 52 / 79 ] simplifiying candidate #<alt (λ (v) (* (* (/ (sqrt (* (cbrt 2) (cbrt 2))) (* (cbrt 4) (cbrt 4))) (* (/ (sqrt (cbrt 2)) (cbrt 4)) (sqrt (- 1 (* 3 (* v v)))))) (- 1 (* v v))))>
1.508 * * * * [progress]: [ 53 / 79 ] simplifiying candidate #<alt (λ (v) (* (* (/ (sqrt (* (cbrt 2) (cbrt 2))) (sqrt 4)) (* (/ (sqrt (cbrt 2)) (sqrt 4)) (sqrt (- 1 (* 3 (* v v)))))) (- 1 (* v v))))>
1.508 * * * * [progress]: [ 54 / 79 ] simplifiying candidate #<alt (λ (v) (* (* (/ (sqrt (* (cbrt 2) (cbrt 2))) 1) (* (/ (sqrt (cbrt 2)) 4) (sqrt (- 1 (* 3 (* v v)))))) (- 1 (* v v))))>
1.508 * * * * [progress]: [ 55 / 79 ] simplifiying candidate #<alt (λ (v) (* (* (/ (sqrt (sqrt 2)) (* (cbrt 4) (cbrt 4))) (* (/ (sqrt (sqrt 2)) (cbrt 4)) (sqrt (- 1 (* 3 (* v v)))))) (- 1 (* v v))))>
1.508 * * * * [progress]: [ 56 / 79 ] simplifiying candidate #<alt (λ (v) (* (* (/ (sqrt (sqrt 2)) (sqrt 4)) (* (/ (sqrt (sqrt 2)) (sqrt 4)) (sqrt (- 1 (* 3 (* v v)))))) (- 1 (* v v))))>
1.508 * * * * [progress]: [ 57 / 79 ] simplifiying candidate #<alt (λ (v) (* (* (/ (sqrt (sqrt 2)) 1) (* (/ (sqrt (sqrt 2)) 4) (sqrt (- 1 (* 3 (* v v)))))) (- 1 (* v v))))>
1.508 * * * * [progress]: [ 58 / 79 ] simplifiying candidate #<alt (λ (v) (* (* (/ (sqrt 1) (* (cbrt 4) (cbrt 4))) (* (/ (sqrt 2) (cbrt 4)) (sqrt (- 1 (* 3 (* v v)))))) (- 1 (* v v))))>
1.509 * * * * [progress]: [ 59 / 79 ] simplifiying candidate #<alt (λ (v) (* (* (/ (sqrt 1) (sqrt 4)) (* (/ (sqrt 2) (sqrt 4)) (sqrt (- 1 (* 3 (* v v)))))) (- 1 (* v v))))>
1.509 * * * * [progress]: [ 60 / 79 ] simplifiying candidate #<alt (λ (v) (* (* (/ (sqrt 1) 1) (* (/ (sqrt 2) 4) (sqrt (- 1 (* 3 (* v v)))))) (- 1 (* v v))))>
1.509 * * * * [progress]: [ 61 / 79 ] simplifiying candidate #<alt (λ (v) (* (* (/ (sqrt (sqrt 2)) (* (cbrt 4) (cbrt 4))) (* (/ (sqrt (sqrt 2)) (cbrt 4)) (sqrt (- 1 (* 3 (* v v)))))) (- 1 (* v v))))>
1.509 * * * * [progress]: [ 62 / 79 ] simplifiying candidate #<alt (λ (v) (* (* (/ (sqrt (sqrt 2)) (sqrt 4)) (* (/ (sqrt (sqrt 2)) (sqrt 4)) (sqrt (- 1 (* 3 (* v v)))))) (- 1 (* v v))))>
1.509 * * * * [progress]: [ 63 / 79 ] simplifiying candidate #<alt (λ (v) (* (* (/ (sqrt (sqrt 2)) 1) (* (/ (sqrt (sqrt 2)) 4) (sqrt (- 1 (* 3 (* v v)))))) (- 1 (* v v))))>
1.509 * * * * [progress]: [ 64 / 79 ] simplifiying candidate #<alt (λ (v) (* (* (/ 1 (* (cbrt 4) (cbrt 4))) (* (/ (sqrt 2) (cbrt 4)) (sqrt (- 1 (* 3 (* v v)))))) (- 1 (* v v))))>
1.509 * * * * [progress]: [ 65 / 79 ] simplifiying candidate #<alt (λ (v) (* (* (/ 1 (sqrt 4)) (* (/ (sqrt 2) (sqrt 4)) (sqrt (- 1 (* 3 (* v v)))))) (- 1 (* v v))))>
1.509 * * * * [progress]: [ 66 / 79 ] simplifiying candidate #<alt (λ (v) (* (* (/ 1 1) (* (/ (sqrt 2) 4) (sqrt (- 1 (* 3 (* v v)))))) (- 1 (* v v))))>
1.509 * * * * [progress]: [ 67 / 79 ] simplifiying candidate #<alt (λ (v) (* (* 1 (* (/ (sqrt 2) 4) (sqrt (- 1 (* 3 (* v v)))))) (- 1 (* v v))))>
1.509 * * * * [progress]: [ 68 / 79 ] simplifiying candidate #<alt (λ (v) (* (* (sqrt 2) (* (/ 1 4) (sqrt (- 1 (* 3 (* v v)))))) (- 1 (* v v))))>
1.509 * * * * [progress]: [ 69 / 79 ] simplifiying candidate #<alt (λ (v) (* (/ (* (/ (sqrt 2) 4) (sqrt (- (pow 1 3) (pow (* 3 (* v v)) 3)))) (sqrt (+ (* 1 1) (+ (* (* 3 (* v v)) (* 3 (* v v))) (* 1 (* 3 (* v v))))))) (- 1 (* v v))))>
1.509 * * * * [progress]: [ 70 / 79 ] simplifiying candidate #<alt (λ (v) (* (/ (* (/ (sqrt 2) 4) (sqrt (- (* 1 1) (* (* 3 (* v v)) (* 3 (* v v)))))) (sqrt (+ 1 (* 3 (* v v))))) (- 1 (* v v))))>
1.509 * * * * [progress]: [ 71 / 79 ] simplifiying candidate #<alt (λ (v) (* (/ (* (sqrt 2) (sqrt (- 1 (* 3 (* v v))))) 4) (- 1 (* v v))))>
1.509 * * * * [progress]: [ 72 / 79 ] simplifiying candidate #<alt (λ (v) (* (posit16->real (real->posit16 (* (/ (sqrt 2) 4) (sqrt (- 1 (* 3 (* v v))))))) (- 1 (* v v))))>
1.509 * * * * [progress]: [ 73 / 79 ] simplifiying candidate #<alt (λ (v) (* (* (sqrt (- 1 (* 3 (* v v)))) (/ (sqrt 2) 4)) (- 1 (* v v))))>
1.509 * * * * [progress]: [ 74 / 79 ] simplifiying candidate #<alt (λ (v) (* (* (/ (sqrt 2) 4) (sqrt (- 1 (* 3 (pow v 2))))) (- 1 (* v v))))>
1.509 * * * * [progress]: [ 75 / 79 ] simplifiying candidate #<alt (λ (v) (* (* (/ (sqrt 2) 4) (sqrt (- 1 (* 3 (pow v 2))))) (- 1 (* v v))))>
1.510 * * * * [progress]: [ 76 / 79 ] simplifiying candidate #<alt (λ (v) (* (* (/ (sqrt 2) 4) (sqrt (- 1 (* 3 (pow v 2))))) (- 1 (* v v))))>
1.510 * * * * [progress]: [ 77 / 79 ] simplifiying candidate #<alt (λ (v) (* (- (* 1/4 (sqrt 2)) (+ (* 9/32 (* (sqrt 2) (pow v 4))) (* 3/8 (* (sqrt 2) (pow v 2))))) (- 1 (* v v))))>
1.510 * * * * [progress]: [ 78 / 79 ] simplifiying candidate #<alt (λ (v) (* (- (+ (* 1/4 (* (sqrt 2) (* v (sqrt -3)))) (* 1/8 (/ (sqrt 2) (* v (sqrt -3))))) (* 1/32 (/ (sqrt 2) (* (pow v 3) (pow (sqrt -3) 3))))) (- 1 (* v v))))>
1.510 * * * * [progress]: [ 79 / 79 ] simplifiying candidate #<alt (λ (v) (* (- (* 1/32 (/ (sqrt 2) (* (pow v 3) (pow (sqrt -3) 3)))) (+ (* 1/4 (* (sqrt 2) (* v (sqrt -3)))) (* 1/8 (/ (sqrt 2) (* v (sqrt -3)))))) (- 1 (* v v))))>
1.511 * [simplify]: Simplifying:
  (* 3 (* v v))
  (* 3 (* v v))
  (+ (log 3) (+ (log v) (log v)))
  (+ (log 3) (log (* v v)))
  (log (* 3 (* v v)))
  (exp (* 3 (* v v)))
  (* (* (* 3 3) 3) (* (* (* v v) v) (* (* v v) v)))
  (* (* (* 3 3) 3) (* (* (* v v) (* v v)) (* v v)))
  (* (cbrt (* 3 (* v v))) (cbrt (* 3 (* v v))))
  (cbrt (* 3 (* v v)))
  (* (* (* 3 (* v v)) (* 3 (* v v))) (* 3 (* v v)))
  (sqrt (* 3 (* v v)))
  (sqrt (* 3 (* v v)))
  (* (sqrt 3) v)
  (* (sqrt 3) v)
  (* 3 v)
  (* (cbrt 3) (* v v))
  (* (sqrt 3) (* v v))
  (* 3 (* v v))
  (real->posit16 (* 3 (* v v)))
  (* (/ (sqrt 2) 4) (sqrt (- 1 (* 3 (* v v)))))
  (+ (- (log (sqrt 2)) (log 4)) (log (sqrt (- 1 (* 3 (* v v))))))
  (+ (log (/ (sqrt 2) 4)) (log (sqrt (- 1 (* 3 (* v v))))))
  (log (* (/ (sqrt 2) 4) (sqrt (- 1 (* 3 (* v v))))))
  (exp (* (/ (sqrt 2) 4) (sqrt (- 1 (* 3 (* v v))))))
  (* (/ (* (* (sqrt 2) (sqrt 2)) (sqrt 2)) (* (* 4 4) 4)) (* (* (sqrt (- 1 (* 3 (* v v)))) (sqrt (- 1 (* 3 (* v v))))) (sqrt (- 1 (* 3 (* v v))))))
  (* (* (* (/ (sqrt 2) 4) (/ (sqrt 2) 4)) (/ (sqrt 2) 4)) (* (* (sqrt (- 1 (* 3 (* v v)))) (sqrt (- 1 (* 3 (* v v))))) (sqrt (- 1 (* 3 (* v v))))))
  (* (cbrt (* (/ (sqrt 2) 4) (sqrt (- 1 (* 3 (* v v)))))) (cbrt (* (/ (sqrt 2) 4) (sqrt (- 1 (* 3 (* v v)))))))
  (cbrt (* (/ (sqrt 2) 4) (sqrt (- 1 (* 3 (* v v))))))
  (* (* (* (/ (sqrt 2) 4) (sqrt (- 1 (* 3 (* v v))))) (* (/ (sqrt 2) 4) (sqrt (- 1 (* 3 (* v v)))))) (* (/ (sqrt 2) 4) (sqrt (- 1 (* 3 (* v v))))))
  (sqrt (* (/ (sqrt 2) 4) (sqrt (- 1 (* 3 (* v v))))))
  (sqrt (* (/ (sqrt 2) 4) (sqrt (- 1 (* 3 (* v v))))))
  (* (sqrt 2) (sqrt (- (pow 1 3) (pow (* 3 (* v v)) 3))))
  (* 4 (sqrt (+ (* 1 1) (+ (* (* 3 (* v v)) (* 3 (* v v))) (* 1 (* 3 (* v v)))))))
  (* (sqrt 2) (sqrt (- (* 1 1) (* (* 3 (* v v)) (* 3 (* v v))))))
  (* 4 (sqrt (+ 1 (* 3 (* v v)))))
  (* (sqrt (/ (sqrt 2) 4)) (sqrt (sqrt (- 1 (* 3 (* v v))))))
  (* (sqrt (/ (sqrt 2) 4)) (sqrt (sqrt (- 1 (* 3 (* v v))))))
  (* (sqrt (/ (sqrt 2) 4)) (sqrt (sqrt (- 1 (* 3 (* v v))))))
  (* (sqrt (/ (sqrt 2) 4)) (sqrt (sqrt (- 1 (* 3 (* v v))))))
  (* (/ (sqrt (sqrt 2)) (sqrt 4)) (sqrt (sqrt (- 1 (* 3 (* v v))))))
  (* (/ (sqrt (sqrt 2)) (sqrt 4)) (sqrt (sqrt (- 1 (* 3 (* v v))))))
  (* (/ (sqrt (sqrt 2)) (sqrt 4)) (sqrt (sqrt (- 1 (* 3 (* v v))))))
  (* (/ (sqrt (sqrt 2)) (sqrt 4)) (sqrt (sqrt (- 1 (* 3 (* v v))))))
  (* (/ (sqrt (sqrt 2)) (sqrt 4)) (sqrt (sqrt (- 1 (* 3 (* v v))))))
  (* (/ (sqrt (sqrt 2)) (sqrt 4)) (sqrt (sqrt (- 1 (* 3 (* v v))))))
  (* (/ (sqrt (sqrt 2)) (sqrt 4)) (sqrt (sqrt (- 1 (* 3 (* v v))))))
  (* (/ (sqrt (sqrt 2)) (sqrt 4)) (sqrt (sqrt (- 1 (* 3 (* v v))))))
  (* (/ (sqrt 2) 4) (* (cbrt (sqrt (- 1 (* 3 (* v v))))) (cbrt (sqrt (- 1 (* 3 (* v v)))))))
  (* (/ (sqrt 2) 4) (sqrt (* (cbrt (- 1 (* 3 (* v v)))) (cbrt (- 1 (* 3 (* v v)))))))
  (* (/ (sqrt 2) 4) (sqrt (sqrt (- 1 (* 3 (* v v))))))
  (* (/ (sqrt 2) 4) (sqrt 1))
  (* (/ (sqrt 2) 4) (sqrt (sqrt (- 1 (* 3 (* v v))))))
  (* (/ (sqrt 2) 4) 1)
  (* (cbrt (/ (sqrt 2) 4)) (sqrt (- 1 (* 3 (* v v)))))
  (* (sqrt (/ (sqrt 2) 4)) (sqrt (- 1 (* 3 (* v v)))))
  (* (/ (cbrt (sqrt 2)) (cbrt 4)) (sqrt (- 1 (* 3 (* v v)))))
  (* (/ (cbrt (sqrt 2)) (sqrt 4)) (sqrt (- 1 (* 3 (* v v)))))
  (* (/ (cbrt (sqrt 2)) 4) (sqrt (- 1 (* 3 (* v v)))))
  (* (/ (sqrt (cbrt 2)) (cbrt 4)) (sqrt (- 1 (* 3 (* v v)))))
  (* (/ (sqrt (cbrt 2)) (sqrt 4)) (sqrt (- 1 (* 3 (* v v)))))
  (* (/ (sqrt (cbrt 2)) 4) (sqrt (- 1 (* 3 (* v v)))))
  (* (/ (sqrt (sqrt 2)) (cbrt 4)) (sqrt (- 1 (* 3 (* v v)))))
  (* (/ (sqrt (sqrt 2)) (sqrt 4)) (sqrt (- 1 (* 3 (* v v)))))
  (* (/ (sqrt (sqrt 2)) 4) (sqrt (- 1 (* 3 (* v v)))))
  (* (/ (sqrt 2) (cbrt 4)) (sqrt (- 1 (* 3 (* v v)))))
  (* (/ (sqrt 2) (sqrt 4)) (sqrt (- 1 (* 3 (* v v)))))
  (* (/ (sqrt 2) 4) (sqrt (- 1 (* 3 (* v v)))))
  (* (/ (sqrt (sqrt 2)) (cbrt 4)) (sqrt (- 1 (* 3 (* v v)))))
  (* (/ (sqrt (sqrt 2)) (sqrt 4)) (sqrt (- 1 (* 3 (* v v)))))
  (* (/ (sqrt (sqrt 2)) 4) (sqrt (- 1 (* 3 (* v v)))))
  (* (/ (sqrt 2) (cbrt 4)) (sqrt (- 1 (* 3 (* v v)))))
  (* (/ (sqrt 2) (sqrt 4)) (sqrt (- 1 (* 3 (* v v)))))
  (* (/ (sqrt 2) 4) (sqrt (- 1 (* 3 (* v v)))))
  (* (/ (sqrt 2) 4) (sqrt (- 1 (* 3 (* v v)))))
  (* (/ 1 4) (sqrt (- 1 (* 3 (* v v)))))
  (* (/ (sqrt 2) 4) (sqrt (- (pow 1 3) (pow (* 3 (* v v)) 3))))
  (* (/ (sqrt 2) 4) (sqrt (- (* 1 1) (* (* 3 (* v v)) (* 3 (* v v))))))
  (* (sqrt 2) (sqrt (- 1 (* 3 (* v v)))))
  (real->posit16 (* (/ (sqrt 2) 4) (sqrt (- 1 (* 3 (* v v))))))
  (* 3 (pow v 2))
  (* 3 (pow v 2))
  (* 3 (pow v 2))
  (- (* 1/4 (sqrt 2)) (+ (* 9/32 (* (sqrt 2) (pow v 4))) (* 3/8 (* (sqrt 2) (pow v 2)))))
  (- (+ (* 1/4 (* (sqrt 2) (* v (sqrt -3)))) (* 1/8 (/ (sqrt 2) (* v (sqrt -3))))) (* 1/32 (/ (sqrt 2) (* (pow v 3) (pow (sqrt -3) 3)))))
  (- (* 1/32 (/ (sqrt 2) (* (pow v 3) (pow (sqrt -3) 3)))) (+ (* 1/4 (* (sqrt 2) (* v (sqrt -3)))) (* 1/8 (/ (sqrt 2) (* v (sqrt -3))))))
1.513 * * [simplify]: iteration 0: 164 enodes
1.588 * * [simplify]: iteration 1: 421 enodes
1.763 * * [simplify]: iteration 2: 1199 enodes
1.980 * * [simplify]: iteration 3: 2041 enodes
2.384 * * [simplify]: iteration complete: 2041 enodes
2.384 * * [simplify]: Extracting #0: cost 51 inf + 0
2.385 * * [simplify]: Extracting #1: cost 280 inf + 0
2.388 * * [simplify]: Extracting #2: cost 641 inf + 795
2.404 * * [simplify]: Extracting #3: cost 689 inf + 24924
2.426 * * [simplify]: Extracting #4: cost 444 inf + 71510
2.464 * * [simplify]: Extracting #5: cost 196 inf + 124184
2.516 * * [simplify]: Extracting #6: cost 22 inf + 178293
2.559 * * [simplify]: Extracting #7: cost 0 inf + 188802
2.605 * [simplify]: Simplified to:
  (* (* v v) 3)
  (* (* v v) 3)
  (log (* (* v v) 3))
  (log (* (* v v) 3))
  (log (* (* v v) 3))
  (exp (* (* v v) 3))
  (* (* (* (* v v) (* v v)) 27) (* v v))
  (* (* (* (* v v) (* v v)) 27) (* v v))
  (* (cbrt (* (* v v) 3)) (cbrt (* (* v v) 3)))
  (cbrt (* (* v v) 3))
  (* (* (* (* v v) (* v v)) 27) (* v v))
  (sqrt (* (* v v) 3))
  (sqrt (* (* v v) 3))
  (* v (sqrt 3))
  (* v (sqrt 3))
  (* 3 v)
  (* (cbrt 3) (* v v))
  (* (* v (sqrt 3)) v)
  (* (* v v) 3)
  (real->posit16 (* (* v v) 3))
  (/ (sqrt (- 1 (* (* v v) 3))) (/ 4 (sqrt 2)))
  (log (/ (sqrt (- 1 (* (* v v) 3))) (/ 4 (sqrt 2))))
  (log (/ (sqrt (- 1 (* (* v v) 3))) (/ 4 (sqrt 2))))
  (log (/ (sqrt (- 1 (* (* v v) 3))) (/ 4 (sqrt 2))))
  (exp (/ (sqrt (- 1 (* (* v v) 3))) (/ 4 (sqrt 2))))
  (* (sqrt (- 1 (* (* v v) 3))) (* (- 1 (* (* v v) 3)) (* 1/32 (sqrt 2))))
  (* (* (/ (sqrt 2) 4) (* (/ (sqrt 2) 4) (/ (sqrt 2) 4))) (* (sqrt (- 1 (* (* v v) 3))) (- 1 (* (* v v) 3))))
  (* (cbrt (/ (sqrt (- 1 (* (* v v) 3))) (/ 4 (sqrt 2)))) (cbrt (/ (sqrt (- 1 (* (* v v) 3))) (/ 4 (sqrt 2)))))
  (cbrt (/ (sqrt (- 1 (* (* v v) 3))) (/ 4 (sqrt 2))))
  (* (* (/ (sqrt 2) 4) (* (/ (sqrt 2) 4) (/ (sqrt 2) 4))) (* (sqrt (- 1 (* (* v v) 3))) (- 1 (* (* v v) 3))))
  (sqrt (/ (sqrt (- 1 (* (* v v) 3))) (/ 4 (sqrt 2))))
  (sqrt (/ (sqrt (- 1 (* (* v v) 3))) (/ 4 (sqrt 2))))
  (* (sqrt 2) (sqrt (- 1 (* (* (* (* v v) (* v v)) 27) (* v v)))))
  (* 4 (sqrt (+ (* (+ 1 (* (* v v) 3)) (* (* v v) 3)) 1)))
  (* (sqrt 2) (sqrt (- 1 (* (* (* v v) (* v v)) 9))))
  (* (sqrt (+ 1 (* (* v v) 3))) 4)
  (* (sqrt (/ (sqrt 2) 4)) (sqrt (sqrt (- 1 (* (* v v) 3)))))
  (* (sqrt (/ (sqrt 2) 4)) (sqrt (sqrt (- 1 (* (* v v) 3)))))
  (* (sqrt (/ (sqrt 2) 4)) (sqrt (sqrt (- 1 (* (* v v) 3)))))
  (* (sqrt (/ (sqrt 2) 4)) (sqrt (sqrt (- 1 (* (* v v) 3)))))
  (/ (* (sqrt (sqrt (- 1 (* (* v v) 3)))) (sqrt (sqrt 2))) 2)
  (/ (* (sqrt (sqrt (- 1 (* (* v v) 3)))) (sqrt (sqrt 2))) 2)
  (/ (* (sqrt (sqrt (- 1 (* (* v v) 3)))) (sqrt (sqrt 2))) 2)
  (/ (* (sqrt (sqrt (- 1 (* (* v v) 3)))) (sqrt (sqrt 2))) 2)
  (/ (* (sqrt (sqrt (- 1 (* (* v v) 3)))) (sqrt (sqrt 2))) 2)
  (/ (* (sqrt (sqrt (- 1 (* (* v v) 3)))) (sqrt (sqrt 2))) 2)
  (/ (* (sqrt (sqrt (- 1 (* (* v v) 3)))) (sqrt (sqrt 2))) 2)
  (/ (* (sqrt (sqrt (- 1 (* (* v v) 3)))) (sqrt (sqrt 2))) 2)
  (* (* (cbrt (sqrt (- 1 (* (* v v) 3)))) (cbrt (sqrt (- 1 (* (* v v) 3))))) (/ (sqrt 2) 4))
  (/ (sqrt 2) (/ 4 (fabs (cbrt (- 1 (* (* v v) 3))))))
  (/ (* (sqrt (sqrt (- 1 (* (* v v) 3)))) (sqrt 2)) 4)
  (/ (sqrt 2) 4)
  (/ (* (sqrt (sqrt (- 1 (* (* v v) 3)))) (sqrt 2)) 4)
  (/ (sqrt 2) 4)
  (* (sqrt (- 1 (* (* v v) 3))) (cbrt (/ (sqrt 2) 4)))
  (* (sqrt (- 1 (* (* v v) 3))) (sqrt (/ (sqrt 2) 4)))
  (* (sqrt (- 1 (* (* v v) 3))) (/ (cbrt (sqrt 2)) (cbrt 4)))
  (* (sqrt (- 1 (* (* v v) 3))) (/ (cbrt (sqrt 2)) 2))
  (* (sqrt (- 1 (* (* v v) 3))) (/ (cbrt (sqrt 2)) 4))
  (/ (* (sqrt (- 1 (* (* v v) 3))) (sqrt (cbrt 2))) (cbrt 4))
  (/ (* (sqrt (- 1 (* (* v v) 3))) (sqrt (cbrt 2))) 2)
  (* (/ (sqrt (cbrt 2)) 4) (sqrt (- 1 (* (* v v) 3))))
  (* (sqrt (- 1 (* (* v v) 3))) (/ (sqrt (sqrt 2)) (cbrt 4)))
  (* (/ (sqrt (sqrt 2)) 2) (sqrt (- 1 (* (* v v) 3))))
  (* (/ (sqrt (sqrt 2)) 4) (sqrt (- 1 (* (* v v) 3))))
  (* (sqrt (- 1 (* (* v v) 3))) (/ (sqrt 2) (cbrt 4)))
  (/ (sqrt (- 1 (* (* v v) 3))) (/ 2 (sqrt 2)))
  (/ (sqrt (- 1 (* (* v v) 3))) (/ 4 (sqrt 2)))
  (* (sqrt (- 1 (* (* v v) 3))) (/ (sqrt (sqrt 2)) (cbrt 4)))
  (* (/ (sqrt (sqrt 2)) 2) (sqrt (- 1 (* (* v v) 3))))
  (* (/ (sqrt (sqrt 2)) 4) (sqrt (- 1 (* (* v v) 3))))
  (* (sqrt (- 1 (* (* v v) 3))) (/ (sqrt 2) (cbrt 4)))
  (/ (sqrt (- 1 (* (* v v) 3))) (/ 2 (sqrt 2)))
  (/ (sqrt (- 1 (* (* v v) 3))) (/ 4 (sqrt 2)))
  (/ (sqrt (- 1 (* (* v v) 3))) (/ 4 (sqrt 2)))
  (* (sqrt (- 1 (* (* v v) 3))) 1/4)
  (/ (sqrt (- 1 (* (* (* (* v v) (* v v)) 27) (* v v)))) (/ 4 (sqrt 2)))
  (/ (sqrt (- 1 (* (* (* v v) (* v v)) 9))) (/ 4 (sqrt 2)))
  (* (sqrt (- 1 (* (* v v) 3))) (sqrt 2))
  (real->posit16 (/ (sqrt (- 1 (* (* v v) 3))) (/ 4 (sqrt 2))))
  (* (* v v) 3)
  (* (* v v) 3)
  (* (* v v) 3)
  (- (- (* (sqrt 2) 1/4) (* 3/8 (* (sqrt 2) (* v v)))) (* (* (sqrt 2) 9/32) (* (* v v) (* v v))))
  (+ (+ (/ (* 1/8 (sqrt 2)) (* (sqrt -3) v)) (* (/ (/ (sqrt 2) (* (* v v) v)) (* (sqrt -3) -3)) -1/32)) (* (* (* (sqrt 2) 1/4) v) (sqrt -3)))
  (- (- (* (/ 1/32 (* v v)) (/ (sqrt 2) (* v (* (sqrt -3) -3)))) (* (* (* (sqrt 2) 1/4) v) (sqrt -3))) (/ (* 1/8 (sqrt 2)) (* (sqrt -3) v)))
2.615 * * * [progress]: adding candidates to table
2.931 * * [progress]: iteration 2 / 4
2.931 * * * [progress]: picking best candidate
2.934 * * * * [pick]: Picked  #<alt (λ (v) (* (cbrt (* (sqrt (- 1 (* (* v v) 3))) (* (- 1 (* (* v v) 3)) (* 1/32 (sqrt 2))))) (- 1 (* v v))))>
2.934 * * * [progress]: localizing error
2.962 * * * [progress]: generating rewritten candidates
2.962 * * * * [progress]: [ 1 / 2 ] rewriting at (2 1 1 2 1 2)
2.982 * * * * [progress]: [ 2 / 2 ] rewriting at (2 1 1 1 1 2)
3.011 * * * [progress]: generating series expansions
3.011 * * * * [progress]: [ 1 / 2 ] generating series at (2 1 1 2 1 2)
3.012 * [backup-simplify]: Simplify (* (* v v) 3) into (* 3 (pow v 2))
3.012 * [approximate]: Taking taylor expansion of (* 3 (pow v 2)) in (v) around 0
3.012 * [taylor]: Taking taylor expansion of (* 3 (pow v 2)) in v
3.012 * [taylor]: Taking taylor expansion of 3 in v
3.012 * [backup-simplify]: Simplify 3 into 3
3.012 * [taylor]: Taking taylor expansion of (pow v 2) in v
3.012 * [taylor]: Taking taylor expansion of v in v
3.012 * [backup-simplify]: Simplify 0 into 0
3.012 * [backup-simplify]: Simplify 1 into 1
3.012 * [taylor]: Taking taylor expansion of (* 3 (pow v 2)) in v
3.012 * [taylor]: Taking taylor expansion of 3 in v
3.012 * [backup-simplify]: Simplify 3 into 3
3.012 * [taylor]: Taking taylor expansion of (pow v 2) in v
3.012 * [taylor]: Taking taylor expansion of v in v
3.012 * [backup-simplify]: Simplify 0 into 0
3.012 * [backup-simplify]: Simplify 1 into 1
3.013 * [backup-simplify]: Simplify (* 1 1) into 1
3.013 * [backup-simplify]: Simplify (* 3 1) into 3
3.013 * [backup-simplify]: Simplify 3 into 3
3.014 * [backup-simplify]: Simplify (+ (* 1 0) (* 0 1)) into 0
3.015 * [backup-simplify]: Simplify (+ (* 3 0) (* 0 1)) into 0
3.015 * [backup-simplify]: Simplify 0 into 0
3.016 * [backup-simplify]: Simplify (+ (* 1 0) (+ (* 0 0) (* 0 1))) into 0
3.017 * [backup-simplify]: Simplify (+ (* 3 0) (+ (* 0 0) (* 0 1))) into 0
3.017 * [backup-simplify]: Simplify 0 into 0
3.018 * [backup-simplify]: Simplify (+ (* 1 0) (+ (* 0 0) (+ (* 0 0) (* 0 1)))) into 0
3.019 * [backup-simplify]: Simplify (+ (* 3 0) (+ (* 0 0) (+ (* 0 0) (* 0 1)))) into 0
3.019 * [backup-simplify]: Simplify 0 into 0
3.021 * [backup-simplify]: Simplify (+ (* 1 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (* 0 1))))) into 0
3.022 * [backup-simplify]: Simplify (+ (* 3 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (* 0 1))))) into 0
3.022 * [backup-simplify]: Simplify 0 into 0
3.023 * [backup-simplify]: Simplify (+ (* 1 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (* 0 1)))))) into 0
3.032 * [backup-simplify]: Simplify (+ (* 3 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (* 0 1)))))) into 0
3.032 * [backup-simplify]: Simplify 0 into 0
3.033 * [backup-simplify]: Simplify (+ (* 1 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (* 0 1))))))) into 0
3.035 * [backup-simplify]: Simplify (+ (* 3 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (* 0 1))))))) into 0
3.035 * [backup-simplify]: Simplify 0 into 0
3.035 * [backup-simplify]: Simplify (* 3 (pow v 2)) into (* 3 (pow v 2))
3.036 * [backup-simplify]: Simplify (* (* (/ 1 v) (/ 1 v)) 3) into (/ 3 (pow v 2))
3.036 * [approximate]: Taking taylor expansion of (/ 3 (pow v 2)) in (v) around 0
3.036 * [taylor]: Taking taylor expansion of (/ 3 (pow v 2)) in v
3.036 * [taylor]: Taking taylor expansion of 3 in v
3.036 * [backup-simplify]: Simplify 3 into 3
3.036 * [taylor]: Taking taylor expansion of (pow v 2) in v
3.036 * [taylor]: Taking taylor expansion of v in v
3.036 * [backup-simplify]: Simplify 0 into 0
3.036 * [backup-simplify]: Simplify 1 into 1
3.036 * [backup-simplify]: Simplify (* 1 1) into 1
3.037 * [backup-simplify]: Simplify (/ 3 1) into 3
3.037 * [taylor]: Taking taylor expansion of (/ 3 (pow v 2)) in v
3.037 * [taylor]: Taking taylor expansion of 3 in v
3.037 * [backup-simplify]: Simplify 3 into 3
3.037 * [taylor]: Taking taylor expansion of (pow v 2) in v
3.037 * [taylor]: Taking taylor expansion of v in v
3.037 * [backup-simplify]: Simplify 0 into 0
3.037 * [backup-simplify]: Simplify 1 into 1
3.037 * [backup-simplify]: Simplify (* 1 1) into 1
3.038 * [backup-simplify]: Simplify (/ 3 1) into 3
3.038 * [backup-simplify]: Simplify 3 into 3
3.038 * [backup-simplify]: Simplify (+ (* 1 0) (* 0 1)) into 0
3.039 * [backup-simplify]: Simplify (- (/ 0 1) (+ (* 3 (/ 0 1)))) into 0
3.039 * [backup-simplify]: Simplify 0 into 0
3.040 * [backup-simplify]: Simplify (+ (* 1 0) (+ (* 0 0) (* 0 1))) into 0
3.041 * [backup-simplify]: Simplify (- (/ 0 1) (+ (* 3 (/ 0 1)) (* 0 (/ 0 1)))) into 0
3.041 * [backup-simplify]: Simplify 0 into 0
3.042 * [backup-simplify]: Simplify (+ (* 1 0) (+ (* 0 0) (+ (* 0 0) (* 0 1)))) into 0
3.043 * [backup-simplify]: Simplify (- (/ 0 1) (+ (* 3 (/ 0 1)) (* 0 (/ 0 1)) (* 0 (/ 0 1)))) into 0
3.044 * [backup-simplify]: Simplify 0 into 0
3.045 * [backup-simplify]: Simplify (+ (* 1 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (* 0 1))))) into 0
3.046 * [backup-simplify]: Simplify (- (/ 0 1) (+ (* 3 (/ 0 1)) (* 0 (/ 0 1)) (* 0 (/ 0 1)) (* 0 (/ 0 1)))) into 0
3.046 * [backup-simplify]: Simplify 0 into 0
3.047 * [backup-simplify]: Simplify (+ (* 1 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (* 0 1)))))) into 0
3.049 * [backup-simplify]: Simplify (- (/ 0 1) (+ (* 3 (/ 0 1)) (* 0 (/ 0 1)) (* 0 (/ 0 1)) (* 0 (/ 0 1)) (* 0 (/ 0 1)))) into 0
3.049 * [backup-simplify]: Simplify 0 into 0
3.050 * [backup-simplify]: Simplify (+ (* 1 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (* 0 1))))))) into 0
3.052 * [backup-simplify]: Simplify (- (/ 0 1) (+ (* 3 (/ 0 1)) (* 0 (/ 0 1)) (* 0 (/ 0 1)) (* 0 (/ 0 1)) (* 0 (/ 0 1)) (* 0 (/ 0 1)))) into 0
3.052 * [backup-simplify]: Simplify 0 into 0
3.052 * [backup-simplify]: Simplify (* 3 (pow (/ 1 (/ 1 v)) 2)) into (* 3 (pow v 2))
3.052 * [backup-simplify]: Simplify (* (* (/ 1 (- v)) (/ 1 (- v))) 3) into (/ 3 (pow v 2))
3.052 * [approximate]: Taking taylor expansion of (/ 3 (pow v 2)) in (v) around 0
3.052 * [taylor]: Taking taylor expansion of (/ 3 (pow v 2)) in v
3.052 * [taylor]: Taking taylor expansion of 3 in v
3.052 * [backup-simplify]: Simplify 3 into 3
3.052 * [taylor]: Taking taylor expansion of (pow v 2) in v
3.052 * [taylor]: Taking taylor expansion of v in v
3.052 * [backup-simplify]: Simplify 0 into 0
3.052 * [backup-simplify]: Simplify 1 into 1
3.053 * [backup-simplify]: Simplify (* 1 1) into 1
3.053 * [backup-simplify]: Simplify (/ 3 1) into 3
3.053 * [taylor]: Taking taylor expansion of (/ 3 (pow v 2)) in v
3.053 * [taylor]: Taking taylor expansion of 3 in v
3.053 * [backup-simplify]: Simplify 3 into 3
3.053 * [taylor]: Taking taylor expansion of (pow v 2) in v
3.053 * [taylor]: Taking taylor expansion of v in v
3.053 * [backup-simplify]: Simplify 0 into 0
3.053 * [backup-simplify]: Simplify 1 into 1
3.054 * [backup-simplify]: Simplify (* 1 1) into 1
3.054 * [backup-simplify]: Simplify (/ 3 1) into 3
3.054 * [backup-simplify]: Simplify 3 into 3
3.055 * [backup-simplify]: Simplify (+ (* 1 0) (* 0 1)) into 0
3.056 * [backup-simplify]: Simplify (- (/ 0 1) (+ (* 3 (/ 0 1)))) into 0
3.056 * [backup-simplify]: Simplify 0 into 0
3.057 * [backup-simplify]: Simplify (+ (* 1 0) (+ (* 0 0) (* 0 1))) into 0
3.058 * [backup-simplify]: Simplify (- (/ 0 1) (+ (* 3 (/ 0 1)) (* 0 (/ 0 1)))) into 0
3.058 * [backup-simplify]: Simplify 0 into 0
3.059 * [backup-simplify]: Simplify (+ (* 1 0) (+ (* 0 0) (+ (* 0 0) (* 0 1)))) into 0
3.060 * [backup-simplify]: Simplify (- (/ 0 1) (+ (* 3 (/ 0 1)) (* 0 (/ 0 1)) (* 0 (/ 0 1)))) into 0
3.060 * [backup-simplify]: Simplify 0 into 0
3.062 * [backup-simplify]: Simplify (+ (* 1 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (* 0 1))))) into 0
3.063 * [backup-simplify]: Simplify (- (/ 0 1) (+ (* 3 (/ 0 1)) (* 0 (/ 0 1)) (* 0 (/ 0 1)) (* 0 (/ 0 1)))) into 0
3.063 * [backup-simplify]: Simplify 0 into 0
3.065 * [backup-simplify]: Simplify (+ (* 1 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (* 0 1)))))) into 0
3.066 * [backup-simplify]: Simplify (- (/ 0 1) (+ (* 3 (/ 0 1)) (* 0 (/ 0 1)) (* 0 (/ 0 1)) (* 0 (/ 0 1)) (* 0 (/ 0 1)))) into 0
3.066 * [backup-simplify]: Simplify 0 into 0
3.067 * [backup-simplify]: Simplify (+ (* 1 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (* 0 1))))))) into 0
3.068 * [backup-simplify]: Simplify (- (/ 0 1) (+ (* 3 (/ 0 1)) (* 0 (/ 0 1)) (* 0 (/ 0 1)) (* 0 (/ 0 1)) (* 0 (/ 0 1)) (* 0 (/ 0 1)))) into 0
3.069 * [backup-simplify]: Simplify 0 into 0
3.069 * [backup-simplify]: Simplify (* 3 (pow (/ 1 (/ 1 (- v))) 2)) into (* 3 (pow v 2))
3.069 * * * * [progress]: [ 2 / 2 ] generating series at (2 1 1 1 1 2)
3.069 * [backup-simplify]: Simplify (* (* v v) 3) into (* 3 (pow v 2))
3.069 * [approximate]: Taking taylor expansion of (* 3 (pow v 2)) in (v) around 0
3.069 * [taylor]: Taking taylor expansion of (* 3 (pow v 2)) in v
3.069 * [taylor]: Taking taylor expansion of 3 in v
3.069 * [backup-simplify]: Simplify 3 into 3
3.069 * [taylor]: Taking taylor expansion of (pow v 2) in v
3.069 * [taylor]: Taking taylor expansion of v in v
3.069 * [backup-simplify]: Simplify 0 into 0
3.069 * [backup-simplify]: Simplify 1 into 1
3.069 * [taylor]: Taking taylor expansion of (* 3 (pow v 2)) in v
3.069 * [taylor]: Taking taylor expansion of 3 in v
3.069 * [backup-simplify]: Simplify 3 into 3
3.069 * [taylor]: Taking taylor expansion of (pow v 2) in v
3.069 * [taylor]: Taking taylor expansion of v in v
3.069 * [backup-simplify]: Simplify 0 into 0
3.069 * [backup-simplify]: Simplify 1 into 1
3.070 * [backup-simplify]: Simplify (* 1 1) into 1
3.070 * [backup-simplify]: Simplify (* 3 1) into 3
3.070 * [backup-simplify]: Simplify 3 into 3
3.071 * [backup-simplify]: Simplify (+ (* 1 0) (* 0 1)) into 0
3.072 * [backup-simplify]: Simplify (+ (* 3 0) (* 0 1)) into 0
3.072 * [backup-simplify]: Simplify 0 into 0
3.073 * [backup-simplify]: Simplify (+ (* 1 0) (+ (* 0 0) (* 0 1))) into 0
3.074 * [backup-simplify]: Simplify (+ (* 3 0) (+ (* 0 0) (* 0 1))) into 0
3.074 * [backup-simplify]: Simplify 0 into 0
3.075 * [backup-simplify]: Simplify (+ (* 1 0) (+ (* 0 0) (+ (* 0 0) (* 0 1)))) into 0
3.076 * [backup-simplify]: Simplify (+ (* 3 0) (+ (* 0 0) (+ (* 0 0) (* 0 1)))) into 0
3.076 * [backup-simplify]: Simplify 0 into 0
3.077 * [backup-simplify]: Simplify (+ (* 1 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (* 0 1))))) into 0
3.079 * [backup-simplify]: Simplify (+ (* 3 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (* 0 1))))) into 0
3.079 * [backup-simplify]: Simplify 0 into 0
3.080 * [backup-simplify]: Simplify (+ (* 1 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (* 0 1)))))) into 0
3.082 * [backup-simplify]: Simplify (+ (* 3 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (* 0 1)))))) into 0
3.082 * [backup-simplify]: Simplify 0 into 0
3.084 * [backup-simplify]: Simplify (+ (* 1 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (* 0 1))))))) into 0
3.086 * [backup-simplify]: Simplify (+ (* 3 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (* 0 1))))))) into 0
3.086 * [backup-simplify]: Simplify 0 into 0
3.086 * [backup-simplify]: Simplify (* 3 (pow v 2)) into (* 3 (pow v 2))
3.086 * [backup-simplify]: Simplify (* (* (/ 1 v) (/ 1 v)) 3) into (/ 3 (pow v 2))
3.086 * [approximate]: Taking taylor expansion of (/ 3 (pow v 2)) in (v) around 0
3.086 * [taylor]: Taking taylor expansion of (/ 3 (pow v 2)) in v
3.086 * [taylor]: Taking taylor expansion of 3 in v
3.086 * [backup-simplify]: Simplify 3 into 3
3.086 * [taylor]: Taking taylor expansion of (pow v 2) in v
3.086 * [taylor]: Taking taylor expansion of v in v
3.086 * [backup-simplify]: Simplify 0 into 0
3.086 * [backup-simplify]: Simplify 1 into 1
3.087 * [backup-simplify]: Simplify (* 1 1) into 1
3.087 * [backup-simplify]: Simplify (/ 3 1) into 3
3.087 * [taylor]: Taking taylor expansion of (/ 3 (pow v 2)) in v
3.087 * [taylor]: Taking taylor expansion of 3 in v
3.087 * [backup-simplify]: Simplify 3 into 3
3.087 * [taylor]: Taking taylor expansion of (pow v 2) in v
3.087 * [taylor]: Taking taylor expansion of v in v
3.087 * [backup-simplify]: Simplify 0 into 0
3.087 * [backup-simplify]: Simplify 1 into 1
3.088 * [backup-simplify]: Simplify (* 1 1) into 1
3.088 * [backup-simplify]: Simplify (/ 3 1) into 3
3.088 * [backup-simplify]: Simplify 3 into 3
3.089 * [backup-simplify]: Simplify (+ (* 1 0) (* 0 1)) into 0
3.090 * [backup-simplify]: Simplify (- (/ 0 1) (+ (* 3 (/ 0 1)))) into 0
3.090 * [backup-simplify]: Simplify 0 into 0
3.091 * [backup-simplify]: Simplify (+ (* 1 0) (+ (* 0 0) (* 0 1))) into 0
3.092 * [backup-simplify]: Simplify (- (/ 0 1) (+ (* 3 (/ 0 1)) (* 0 (/ 0 1)))) into 0
3.092 * [backup-simplify]: Simplify 0 into 0
3.093 * [backup-simplify]: Simplify (+ (* 1 0) (+ (* 0 0) (+ (* 0 0) (* 0 1)))) into 0
3.094 * [backup-simplify]: Simplify (- (/ 0 1) (+ (* 3 (/ 0 1)) (* 0 (/ 0 1)) (* 0 (/ 0 1)))) into 0
3.094 * [backup-simplify]: Simplify 0 into 0
3.095 * [backup-simplify]: Simplify (+ (* 1 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (* 0 1))))) into 0
3.096 * [backup-simplify]: Simplify (- (/ 0 1) (+ (* 3 (/ 0 1)) (* 0 (/ 0 1)) (* 0 (/ 0 1)) (* 0 (/ 0 1)))) into 0
3.097 * [backup-simplify]: Simplify 0 into 0
3.098 * [backup-simplify]: Simplify (+ (* 1 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (* 0 1)))))) into 0
3.099 * [backup-simplify]: Simplify (- (/ 0 1) (+ (* 3 (/ 0 1)) (* 0 (/ 0 1)) (* 0 (/ 0 1)) (* 0 (/ 0 1)) (* 0 (/ 0 1)))) into 0
3.099 * [backup-simplify]: Simplify 0 into 0
3.101 * [backup-simplify]: Simplify (+ (* 1 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (* 0 1))))))) into 0
3.102 * [backup-simplify]: Simplify (- (/ 0 1) (+ (* 3 (/ 0 1)) (* 0 (/ 0 1)) (* 0 (/ 0 1)) (* 0 (/ 0 1)) (* 0 (/ 0 1)) (* 0 (/ 0 1)))) into 0
3.102 * [backup-simplify]: Simplify 0 into 0
3.102 * [backup-simplify]: Simplify (* 3 (pow (/ 1 (/ 1 v)) 2)) into (* 3 (pow v 2))
3.102 * [backup-simplify]: Simplify (* (* (/ 1 (- v)) (/ 1 (- v))) 3) into (/ 3 (pow v 2))
3.102 * [approximate]: Taking taylor expansion of (/ 3 (pow v 2)) in (v) around 0
3.102 * [taylor]: Taking taylor expansion of (/ 3 (pow v 2)) in v
3.102 * [taylor]: Taking taylor expansion of 3 in v
3.103 * [backup-simplify]: Simplify 3 into 3
3.103 * [taylor]: Taking taylor expansion of (pow v 2) in v
3.103 * [taylor]: Taking taylor expansion of v in v
3.103 * [backup-simplify]: Simplify 0 into 0
3.103 * [backup-simplify]: Simplify 1 into 1
3.103 * [backup-simplify]: Simplify (* 1 1) into 1
3.103 * [backup-simplify]: Simplify (/ 3 1) into 3
3.104 * [taylor]: Taking taylor expansion of (/ 3 (pow v 2)) in v
3.104 * [taylor]: Taking taylor expansion of 3 in v
3.104 * [backup-simplify]: Simplify 3 into 3
3.104 * [taylor]: Taking taylor expansion of (pow v 2) in v
3.104 * [taylor]: Taking taylor expansion of v in v
3.104 * [backup-simplify]: Simplify 0 into 0
3.104 * [backup-simplify]: Simplify 1 into 1
3.104 * [backup-simplify]: Simplify (* 1 1) into 1
3.104 * [backup-simplify]: Simplify (/ 3 1) into 3
3.105 * [backup-simplify]: Simplify 3 into 3
3.105 * [backup-simplify]: Simplify (+ (* 1 0) (* 0 1)) into 0
3.106 * [backup-simplify]: Simplify (- (/ 0 1) (+ (* 3 (/ 0 1)))) into 0
3.106 * [backup-simplify]: Simplify 0 into 0
3.107 * [backup-simplify]: Simplify (+ (* 1 0) (+ (* 0 0) (* 0 1))) into 0
3.108 * [backup-simplify]: Simplify (- (/ 0 1) (+ (* 3 (/ 0 1)) (* 0 (/ 0 1)))) into 0
3.108 * [backup-simplify]: Simplify 0 into 0
3.109 * [backup-simplify]: Simplify (+ (* 1 0) (+ (* 0 0) (+ (* 0 0) (* 0 1)))) into 0
3.110 * [backup-simplify]: Simplify (- (/ 0 1) (+ (* 3 (/ 0 1)) (* 0 (/ 0 1)) (* 0 (/ 0 1)))) into 0
3.110 * [backup-simplify]: Simplify 0 into 0
3.112 * [backup-simplify]: Simplify (+ (* 1 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (* 0 1))))) into 0
3.113 * [backup-simplify]: Simplify (- (/ 0 1) (+ (* 3 (/ 0 1)) (* 0 (/ 0 1)) (* 0 (/ 0 1)) (* 0 (/ 0 1)))) into 0
3.113 * [backup-simplify]: Simplify 0 into 0
3.115 * [backup-simplify]: Simplify (+ (* 1 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (* 0 1)))))) into 0
3.116 * [backup-simplify]: Simplify (- (/ 0 1) (+ (* 3 (/ 0 1)) (* 0 (/ 0 1)) (* 0 (/ 0 1)) (* 0 (/ 0 1)) (* 0 (/ 0 1)))) into 0
3.116 * [backup-simplify]: Simplify 0 into 0
3.118 * [backup-simplify]: Simplify (+ (* 1 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (* 0 1))))))) into 0
3.119 * [backup-simplify]: Simplify (- (/ 0 1) (+ (* 3 (/ 0 1)) (* 0 (/ 0 1)) (* 0 (/ 0 1)) (* 0 (/ 0 1)) (* 0 (/ 0 1)) (* 0 (/ 0 1)))) into 0
3.119 * [backup-simplify]: Simplify 0 into 0
3.119 * [backup-simplify]: Simplify (* 3 (pow (/ 1 (/ 1 (- v))) 2)) into (* 3 (pow v 2))
3.119 * * * [progress]: simplifying candidates
3.119 * * * * [progress]: [ 1 / 46 ] simplifiying candidate #<alt (λ (v) (* (cbrt (* (sqrt (- 1 (* (* v v) 3))) (* (- 1 (pow (* (* v v) 3) 1)) (* 1/32 (sqrt 2))))) (- 1 (* v v))))>
3.119 * * * * [progress]: [ 2 / 46 ] simplifiying candidate #<alt (λ (v) (* (cbrt (* (sqrt (- 1 (* (* v v) 3))) (* (- 1 (pow (* (* v v) 3) 1)) (* 1/32 (sqrt 2))))) (- 1 (* v v))))>
3.119 * * * * [progress]: [ 3 / 46 ] simplifiying candidate #<alt (λ (v) (* (cbrt (* (sqrt (- 1 (* (* v v) 3))) (* (- 1 (pow (* (* v v) 3) 1)) (* 1/32 (sqrt 2))))) (- 1 (* v v))))>
3.119 * * * * [progress]: [ 4 / 46 ] simplifiying candidate #<alt (λ (v) (* (cbrt (* (sqrt (- 1 (* (* v v) 3))) (* (- 1 (exp (+ (+ (log v) (log v)) (log 3)))) (* 1/32 (sqrt 2))))) (- 1 (* v v))))>
3.119 * * * * [progress]: [ 5 / 46 ] simplifiying candidate #<alt (λ (v) (* (cbrt (* (sqrt (- 1 (* (* v v) 3))) (* (- 1 (exp (+ (log (* v v)) (log 3)))) (* 1/32 (sqrt 2))))) (- 1 (* v v))))>
3.119 * * * * [progress]: [ 6 / 46 ] simplifiying candidate #<alt (λ (v) (* (cbrt (* (sqrt (- 1 (* (* v v) 3))) (* (- 1 (exp (log (* (* v v) 3)))) (* 1/32 (sqrt 2))))) (- 1 (* v v))))>
3.120 * * * * [progress]: [ 7 / 46 ] simplifiying candidate #<alt (λ (v) (* (cbrt (* (sqrt (- 1 (* (* v v) 3))) (* (- 1 (log (exp (* (* v v) 3)))) (* 1/32 (sqrt 2))))) (- 1 (* v v))))>
3.120 * * * * [progress]: [ 8 / 46 ] simplifiying candidate #<alt (λ (v) (* (cbrt (* (sqrt (- 1 (* (* v v) 3))) (* (- 1 (cbrt (* (* (* (* v v) v) (* (* v v) v)) (* (* 3 3) 3)))) (* 1/32 (sqrt 2))))) (- 1 (* v v))))>
3.120 * * * * [progress]: [ 9 / 46 ] simplifiying candidate #<alt (λ (v) (* (cbrt (* (sqrt (- 1 (* (* v v) 3))) (* (- 1 (cbrt (* (* (* (* v v) (* v v)) (* v v)) (* (* 3 3) 3)))) (* 1/32 (sqrt 2))))) (- 1 (* v v))))>
3.120 * * * * [progress]: [ 10 / 46 ] simplifiying candidate #<alt (λ (v) (* (cbrt (* (sqrt (- 1 (* (* v v) 3))) (* (- 1 (* (* (cbrt (* (* v v) 3)) (cbrt (* (* v v) 3))) (cbrt (* (* v v) 3)))) (* 1/32 (sqrt 2))))) (- 1 (* v v))))>
3.120 * * * * [progress]: [ 11 / 46 ] simplifiying candidate #<alt (λ (v) (* (cbrt (* (sqrt (- 1 (* (* v v) 3))) (* (- 1 (cbrt (* (* (* (* v v) 3) (* (* v v) 3)) (* (* v v) 3)))) (* 1/32 (sqrt 2))))) (- 1 (* v v))))>
3.120 * * * * [progress]: [ 12 / 46 ] simplifiying candidate #<alt (λ (v) (* (cbrt (* (sqrt (- 1 (* (* v v) 3))) (* (- 1 (* (sqrt (* (* v v) 3)) (sqrt (* (* v v) 3)))) (* 1/32 (sqrt 2))))) (- 1 (* v v))))>
3.120 * * * * [progress]: [ 13 / 46 ] simplifiying candidate #<alt (λ (v) (* (cbrt (* (sqrt (- 1 (* (* v v) 3))) (* (- 1 (* 1 (* (* v v) 3))) (* 1/32 (sqrt 2))))) (- 1 (* v v))))>
3.120 * * * * [progress]: [ 14 / 46 ] simplifiying candidate #<alt (λ (v) (* (cbrt (* (sqrt (- 1 (* (* v v) 3))) (* (- 1 (* (* v (sqrt 3)) (* v (sqrt 3)))) (* 1/32 (sqrt 2))))) (- 1 (* v v))))>
3.120 * * * * [progress]: [ 15 / 46 ] simplifiying candidate #<alt (λ (v) (* (cbrt (* (sqrt (- 1 (* (* v v) 3))) (* (- 1 (* (* (* v v) (* (cbrt 3) (cbrt 3))) (cbrt 3))) (* 1/32 (sqrt 2))))) (- 1 (* v v))))>
3.120 * * * * [progress]: [ 16 / 46 ] simplifiying candidate #<alt (λ (v) (* (cbrt (* (sqrt (- 1 (* (* v v) 3))) (* (- 1 (* (* (* v v) (sqrt 3)) (sqrt 3))) (* 1/32 (sqrt 2))))) (- 1 (* v v))))>
3.120 * * * * [progress]: [ 17 / 46 ] simplifiying candidate #<alt (λ (v) (* (cbrt (* (sqrt (- 1 (* (* v v) 3))) (* (- 1 (* (* (* v v) 1) 3)) (* 1/32 (sqrt 2))))) (- 1 (* v v))))>
3.120 * * * * [progress]: [ 18 / 46 ] simplifiying candidate #<alt (λ (v) (* (cbrt (* (sqrt (- 1 (* (* v v) 3))) (* (- 1 (* v (* v 3))) (* 1/32 (sqrt 2))))) (- 1 (* v v))))>
3.120 * * * * [progress]: [ 19 / 46 ] simplifiying candidate #<alt (λ (v) (* (cbrt (* (sqrt (- 1 (* (* v v) 3))) (* (- 1 (posit16->real (real->posit16 (* (* v v) 3)))) (* 1/32 (sqrt 2))))) (- 1 (* v v))))>
3.120 * * * * [progress]: [ 20 / 46 ] simplifiying candidate #<alt (λ (v) (* (cbrt (* (sqrt (- 1 (* (* v v) 3))) (* (- 1 (* 3 (* v v))) (* 1/32 (sqrt 2))))) (- 1 (* v v))))>
3.120 * * * * [progress]: [ 21 / 46 ] simplifiying candidate #<alt (λ (v) (* (cbrt (* (sqrt (- 1 (pow (* (* v v) 3) 1))) (* (- 1 (* (* v v) 3)) (* 1/32 (sqrt 2))))) (- 1 (* v v))))>
3.120 * * * * [progress]: [ 22 / 46 ] simplifiying candidate #<alt (λ (v) (* (cbrt (* (sqrt (- 1 (pow (* (* v v) 3) 1))) (* (- 1 (* (* v v) 3)) (* 1/32 (sqrt 2))))) (- 1 (* v v))))>
3.121 * * * * [progress]: [ 23 / 46 ] simplifiying candidate #<alt (λ (v) (* (cbrt (* (sqrt (- 1 (pow (* (* v v) 3) 1))) (* (- 1 (* (* v v) 3)) (* 1/32 (sqrt 2))))) (- 1 (* v v))))>
3.121 * * * * [progress]: [ 24 / 46 ] simplifiying candidate #<alt (λ (v) (* (cbrt (* (sqrt (- 1 (exp (+ (+ (log v) (log v)) (log 3))))) (* (- 1 (* (* v v) 3)) (* 1/32 (sqrt 2))))) (- 1 (* v v))))>
3.121 * * * * [progress]: [ 25 / 46 ] simplifiying candidate #<alt (λ (v) (* (cbrt (* (sqrt (- 1 (exp (+ (log (* v v)) (log 3))))) (* (- 1 (* (* v v) 3)) (* 1/32 (sqrt 2))))) (- 1 (* v v))))>
3.121 * * * * [progress]: [ 26 / 46 ] simplifiying candidate #<alt (λ (v) (* (cbrt (* (sqrt (- 1 (exp (log (* (* v v) 3))))) (* (- 1 (* (* v v) 3)) (* 1/32 (sqrt 2))))) (- 1 (* v v))))>
3.121 * * * * [progress]: [ 27 / 46 ] simplifiying candidate #<alt (λ (v) (* (cbrt (* (sqrt (- 1 (log (exp (* (* v v) 3))))) (* (- 1 (* (* v v) 3)) (* 1/32 (sqrt 2))))) (- 1 (* v v))))>
3.121 * * * * [progress]: [ 28 / 46 ] simplifiying candidate #<alt (λ (v) (* (cbrt (* (sqrt (- 1 (cbrt (* (* (* (* v v) v) (* (* v v) v)) (* (* 3 3) 3))))) (* (- 1 (* (* v v) 3)) (* 1/32 (sqrt 2))))) (- 1 (* v v))))>
3.121 * * * * [progress]: [ 29 / 46 ] simplifiying candidate #<alt (λ (v) (* (cbrt (* (sqrt (- 1 (cbrt (* (* (* (* v v) (* v v)) (* v v)) (* (* 3 3) 3))))) (* (- 1 (* (* v v) 3)) (* 1/32 (sqrt 2))))) (- 1 (* v v))))>
3.121 * * * * [progress]: [ 30 / 46 ] simplifiying candidate #<alt (λ (v) (* (cbrt (* (sqrt (- 1 (* (* (cbrt (* (* v v) 3)) (cbrt (* (* v v) 3))) (cbrt (* (* v v) 3))))) (* (- 1 (* (* v v) 3)) (* 1/32 (sqrt 2))))) (- 1 (* v v))))>
3.121 * * * * [progress]: [ 31 / 46 ] simplifiying candidate #<alt (λ (v) (* (cbrt (* (sqrt (- 1 (cbrt (* (* (* (* v v) 3) (* (* v v) 3)) (* (* v v) 3))))) (* (- 1 (* (* v v) 3)) (* 1/32 (sqrt 2))))) (- 1 (* v v))))>
3.121 * * * * [progress]: [ 32 / 46 ] simplifiying candidate #<alt (λ (v) (* (cbrt (* (sqrt (- 1 (* (sqrt (* (* v v) 3)) (sqrt (* (* v v) 3))))) (* (- 1 (* (* v v) 3)) (* 1/32 (sqrt 2))))) (- 1 (* v v))))>
3.121 * * * * [progress]: [ 33 / 46 ] simplifiying candidate #<alt (λ (v) (* (cbrt (* (sqrt (- 1 (* 1 (* (* v v) 3)))) (* (- 1 (* (* v v) 3)) (* 1/32 (sqrt 2))))) (- 1 (* v v))))>
3.121 * * * * [progress]: [ 34 / 46 ] simplifiying candidate #<alt (λ (v) (* (cbrt (* (sqrt (- 1 (* (* v (sqrt 3)) (* v (sqrt 3))))) (* (- 1 (* (* v v) 3)) (* 1/32 (sqrt 2))))) (- 1 (* v v))))>
3.121 * * * * [progress]: [ 35 / 46 ] simplifiying candidate #<alt (λ (v) (* (cbrt (* (sqrt (- 1 (* (* (* v v) (* (cbrt 3) (cbrt 3))) (cbrt 3)))) (* (- 1 (* (* v v) 3)) (* 1/32 (sqrt 2))))) (- 1 (* v v))))>
3.121 * * * * [progress]: [ 36 / 46 ] simplifiying candidate #<alt (λ (v) (* (cbrt (* (sqrt (- 1 (* (* (* v v) (sqrt 3)) (sqrt 3)))) (* (- 1 (* (* v v) 3)) (* 1/32 (sqrt 2))))) (- 1 (* v v))))>
3.121 * * * * [progress]: [ 37 / 46 ] simplifiying candidate #<alt (λ (v) (* (cbrt (* (sqrt (- 1 (* (* (* v v) 1) 3))) (* (- 1 (* (* v v) 3)) (* 1/32 (sqrt 2))))) (- 1 (* v v))))>
3.121 * * * * [progress]: [ 38 / 46 ] simplifiying candidate #<alt (λ (v) (* (cbrt (* (sqrt (- 1 (* v (* v 3)))) (* (- 1 (* (* v v) 3)) (* 1/32 (sqrt 2))))) (- 1 (* v v))))>
3.122 * * * * [progress]: [ 39 / 46 ] simplifiying candidate #<alt (λ (v) (* (cbrt (* (sqrt (- 1 (posit16->real (real->posit16 (* (* v v) 3))))) (* (- 1 (* (* v v) 3)) (* 1/32 (sqrt 2))))) (- 1 (* v v))))>
3.122 * * * * [progress]: [ 40 / 46 ] simplifiying candidate #<alt (λ (v) (* (cbrt (* (sqrt (- 1 (* 3 (* v v)))) (* (- 1 (* (* v v) 3)) (* 1/32 (sqrt 2))))) (- 1 (* v v))))>
3.122 * * * * [progress]: [ 41 / 46 ] simplifiying candidate #<alt (λ (v) (* (cbrt (* (sqrt (- 1 (* (* v v) 3))) (* (- 1 (* 3 (pow v 2))) (* 1/32 (sqrt 2))))) (- 1 (* v v))))>
3.122 * * * * [progress]: [ 42 / 46 ] simplifiying candidate #<alt (λ (v) (* (cbrt (* (sqrt (- 1 (* (* v v) 3))) (* (- 1 (* 3 (pow v 2))) (* 1/32 (sqrt 2))))) (- 1 (* v v))))>
3.122 * * * * [progress]: [ 43 / 46 ] simplifiying candidate #<alt (λ (v) (* (cbrt (* (sqrt (- 1 (* (* v v) 3))) (* (- 1 (* 3 (pow v 2))) (* 1/32 (sqrt 2))))) (- 1 (* v v))))>
3.122 * * * * [progress]: [ 44 / 46 ] simplifiying candidate #<alt (λ (v) (* (cbrt (* (sqrt (- 1 (* 3 (pow v 2)))) (* (- 1 (* (* v v) 3)) (* 1/32 (sqrt 2))))) (- 1 (* v v))))>
3.122 * * * * [progress]: [ 45 / 46 ] simplifiying candidate #<alt (λ (v) (* (cbrt (* (sqrt (- 1 (* 3 (pow v 2)))) (* (- 1 (* (* v v) 3)) (* 1/32 (sqrt 2))))) (- 1 (* v v))))>
3.122 * * * * [progress]: [ 46 / 46 ] simplifiying candidate #<alt (λ (v) (* (cbrt (* (sqrt (- 1 (* 3 (pow v 2)))) (* (- 1 (* (* v v) 3)) (* 1/32 (sqrt 2))))) (- 1 (* v v))))>
3.123 * [simplify]: Simplifying:
  (* (* v v) 3)
  (* (* v v) 3)
  (+ (+ (log v) (log v)) (log 3))
  (+ (log (* v v)) (log 3))
  (log (* (* v v) 3))
  (exp (* (* v v) 3))
  (* (* (* (* v v) v) (* (* v v) v)) (* (* 3 3) 3))
  (* (* (* (* v v) (* v v)) (* v v)) (* (* 3 3) 3))
  (* (cbrt (* (* v v) 3)) (cbrt (* (* v v) 3)))
  (cbrt (* (* v v) 3))
  (* (* (* (* v v) 3) (* (* v v) 3)) (* (* v v) 3))
  (sqrt (* (* v v) 3))
  (sqrt (* (* v v) 3))
  (* v (sqrt 3))
  (* v (sqrt 3))
  (* (* v v) (* (cbrt 3) (cbrt 3)))
  (* (* v v) (sqrt 3))
  (* (* v v) 1)
  (* v 3)
  (real->posit16 (* (* v v) 3))
  (* (* v v) 3)
  (* (* v v) 3)
  (+ (+ (log v) (log v)) (log 3))
  (+ (log (* v v)) (log 3))
  (log (* (* v v) 3))
  (exp (* (* v v) 3))
  (* (* (* (* v v) v) (* (* v v) v)) (* (* 3 3) 3))
  (* (* (* (* v v) (* v v)) (* v v)) (* (* 3 3) 3))
  (* (cbrt (* (* v v) 3)) (cbrt (* (* v v) 3)))
  (cbrt (* (* v v) 3))
  (* (* (* (* v v) 3) (* (* v v) 3)) (* (* v v) 3))
  (sqrt (* (* v v) 3))
  (sqrt (* (* v v) 3))
  (* v (sqrt 3))
  (* v (sqrt 3))
  (* (* v v) (* (cbrt 3) (cbrt 3)))
  (* (* v v) (sqrt 3))
  (* (* v v) 1)
  (* v 3)
  (real->posit16 (* (* v v) 3))
  (* 3 (pow v 2))
  (* 3 (pow v 2))
  (* 3 (pow v 2))
  (* 3 (pow v 2))
  (* 3 (pow v 2))
  (* 3 (pow v 2))
3.123 * * [simplify]: iteration 0: 38 enodes
3.143 * * [simplify]: iteration 1: 107 enodes
3.185 * * [simplify]: iteration 2: 326 enodes
3.421 * * [simplify]: iteration 3: 1012 enodes
3.763 * * [simplify]: iteration 4: 2002 enodes
4.198 * * [simplify]: iteration complete: 2002 enodes
4.198 * * [simplify]: Extracting #0: cost 13 inf + 0
4.198 * * [simplify]: Extracting #1: cost 179 inf + 0
4.202 * * [simplify]: Extracting #2: cost 572 inf + 5976
4.217 * * [simplify]: Extracting #3: cost 221 inf + 48749
4.242 * * [simplify]: Extracting #4: cost 23 inf + 76355
4.276 * * [simplify]: Extracting #5: cost 6 inf + 79144
4.290 * * [simplify]: Extracting #6: cost 0 inf + 81322
4.304 * [simplify]: Simplified to:
  (* (* v 3) v)
  (* (* v 3) v)
  (log (* (* v 3) v))
  (log (* (* v 3) v))
  (log (* (* v 3) v))
  (exp (* (* v 3) v))
  (* 27 (* (* v (* v v)) (* v (* v v))))
  (* 27 (* (* v (* v v)) (* v (* v v))))
  (* (cbrt (* (* v 3) v)) (cbrt (* (* v 3) v)))
  (cbrt (* (* v 3) v))
  (* 27 (* (* v (* v v)) (* v (* v v))))
  (sqrt (* (* v 3) v))
  (sqrt (* (* v 3) v))
  (* v (sqrt 3))
  (* v (sqrt 3))
  (* (* (cbrt 3) v) (* (cbrt 3) v))
  (* v (* (sqrt 3) v))
  (* v v)
  (* v 3)
  (real->posit16 (* (* v 3) v))
  (* (* v 3) v)
  (* (* v 3) v)
  (log (* (* v 3) v))
  (log (* (* v 3) v))
  (log (* (* v 3) v))
  (exp (* (* v 3) v))
  (* 27 (* (* v (* v v)) (* v (* v v))))
  (* 27 (* (* v (* v v)) (* v (* v v))))
  (* (cbrt (* (* v 3) v)) (cbrt (* (* v 3) v)))
  (cbrt (* (* v 3) v))
  (* 27 (* (* v (* v v)) (* v (* v v))))
  (sqrt (* (* v 3) v))
  (sqrt (* (* v 3) v))
  (* v (sqrt 3))
  (* v (sqrt 3))
  (* (* (cbrt 3) v) (* (cbrt 3) v))
  (* v (* (sqrt 3) v))
  (* v v)
  (* v 3)
  (real->posit16 (* (* v 3) v))
  (* (* v 3) v)
  (* (* v 3) v)
  (* (* v 3) v)
  (* (* v 3) v)
  (* (* v 3) v)
  (* (* v 3) v)
4.308 * * * [progress]: adding candidates to table
4.537 * [progress]: [Phase 3 of 3] Extracting.
4.540 * [simplify]: Simplifying:
  (* (cbrt (* (sqrt (- 1 (* (* v v) 3))) (* (- 1 (* (* v v) 3)) (* 1/32 (sqrt 2))))) (- 1 (* v v)))
4.540 * * [simplify]: iteration 0: 16 enodes
4.541 * * [simplify]: iteration 1: 23 enodes
4.542 * * [simplify]: iteration complete: 23 enodes
4.542 * * [simplify]: Extracting #0: cost 1 inf + 0
4.542 * * [simplify]: Extracting #1: cost 3 inf + 0
4.542 * * [simplify]: Extracting #2: cost 6 inf + 0
4.542 * * [simplify]: Extracting #3: cost 8 inf + 1
4.542 * * [simplify]: Extracting #4: cost 7 inf + 125
4.543 * * [simplify]: Extracting #5: cost 10 inf + 125
4.543 * * [simplify]: Extracting #6: cost 11 inf + 126
4.543 * * [simplify]: Extracting #7: cost 8 inf + 169
4.543 * * [simplify]: Extracting #8: cost 4 inf + 701
4.543 * * [simplify]: Extracting #9: cost 0 inf + 2079
4.543 * [simplify]: Simplified to:
  (* (- 1 (* v v)) (cbrt (* (* (- 1 (* (* v v) 3)) (* (sqrt 2) 1/32)) (sqrt (- 1 (* (* v v) 3))))))
7.758 * [regime-testing]: Baseline error score: 0.019726714279218814
7.760 * [regime-testing]: Oracle error score: 0.019726714279218814
7.760 * [regime-testing]: End program error score: 0.019726714279218814