0.001 * [progress]: [Phase 1 of 3] Setting up. 0.001 * * * [progress]: [1/2] Preparing points 0.079 * * * [progress]: [2/2] Setting up program. 0.085 * [progress]: [Phase 2 of 3] Improving. 0.085 * * * * [progress]: [ 1 / 1 ] simplifiying candidate # 0.085 * [simplify]: Simplifying (* (* (/ (sqrt 2) 4) (sqrt (- 1 (* 3 (* v v))))) (- 1 (* v v))) 0.086 * * [simplify]: iters left: 6 (14 enodes) 0.115 * * [simplify]: iters left: 5 (57 enodes) 0.138 * * [simplify]: iters left: 4 (113 enodes) 0.182 * * [simplify]: iters left: 3 (238 enodes) 0.289 * * [simplify]: Extracting #0: cost 1 inf + 0 0.289 * * [simplify]: Extracting #1: cost 31 inf + 0 0.289 * * [simplify]: Extracting #2: cost 82 inf + 2 0.289 * * [simplify]: Extracting #3: cost 107 inf + 209 0.290 * * [simplify]: Extracting #4: cost 82 inf + 3474 0.291 * * [simplify]: Extracting #5: cost 63 inf + 6248 0.296 * * [simplify]: Extracting #6: cost 14 inf + 18680 0.302 * * [simplify]: Extracting #7: cost 0 inf + 22575 0.315 * [simplify]: Simplified to (- (* (sqrt (+ (* -3 (* v v)) 1)) (/ (sqrt 2) 4)) (* (* (sqrt (+ (* -3 (* v v)) 1)) (/ (sqrt 2) 4)) (* v v))) 0.315 * [simplify]: Simplified (2) to (λ (v) (- (* (sqrt (+ (* -3 (* v v)) 1)) (/ (sqrt 2) 4)) (* (* (sqrt (+ (* -3 (* v v)) 1)) (/ (sqrt 2) 4)) (* v v)))) 0.321 * * [progress]: iteration 1 / 4 0.322 * * * [progress]: picking best candidate 0.327 * * * * [pick]: Picked # 0.327 * * * [progress]: localizing error 0.369 * * * [progress]: generating rewritten candidates 0.369 * * * * [progress]: [ 1 / 3 ] rewriting at (2 1 2 1 2) 0.383 * * * * [progress]: [ 2 / 3 ] rewriting at (2 1 2) 0.387 * * * * [progress]: [ 3 / 3 ] rewriting at (2 1) 0.421 * * * [progress]: generating series expansions 0.421 * * * * [progress]: [ 1 / 3 ] generating series at (2 1 2 1 2) 0.421 * [backup-simplify]: Simplify (* 3 (* v v)) into (* 3 (pow v 2)) 0.421 * [approximate]: Taking taylor expansion of (* 3 (pow v 2)) in (v) around 0 0.421 * [taylor]: Taking taylor expansion of (* 3 (pow v 2)) in v 0.421 * [taylor]: Taking taylor expansion of 3 in v 0.421 * [backup-simplify]: Simplify 3 into 3 0.421 * [taylor]: Taking taylor expansion of (pow v 2) in v 0.421 * [taylor]: Taking taylor expansion of v in v 0.421 * [backup-simplify]: Simplify 0 into 0 0.421 * [backup-simplify]: Simplify 1 into 1 0.421 * [taylor]: Taking taylor expansion of (* 3 (pow v 2)) in v 0.421 * [taylor]: Taking taylor expansion of 3 in v 0.421 * [backup-simplify]: Simplify 3 into 3 0.421 * [taylor]: Taking taylor expansion of (pow v 2) in v 0.421 * [taylor]: Taking taylor expansion of v in v 0.421 * [backup-simplify]: Simplify 0 into 0 0.421 * [backup-simplify]: Simplify 1 into 1 0.422 * [backup-simplify]: Simplify (* 1 1) into 1 0.422 * [backup-simplify]: Simplify (* 3 1) into 3 0.423 * [backup-simplify]: Simplify 3 into 3 0.423 * [backup-simplify]: Simplify (+ (* 1 0) (* 0 1)) into 0 0.424 * [backup-simplify]: Simplify (+ (* 3 0) (* 0 1)) into 0 0.424 * [backup-simplify]: Simplify 0 into 0 0.425 * [backup-simplify]: Simplify (+ (* 1 0) (+ (* 0 0) (* 0 1))) into 0 0.426 * [backup-simplify]: Simplify (+ (* 3 0) (+ (* 0 0) (* 0 1))) into 0 0.426 * [backup-simplify]: Simplify 0 into 0 0.427 * [backup-simplify]: Simplify (+ (* 1 0) (+ (* 0 0) (+ (* 0 0) (* 0 1)))) into 0 0.428 * [backup-simplify]: Simplify (+ (* 3 0) (+ (* 0 0) (+ (* 0 0) (* 0 1)))) into 0 0.428 * [backup-simplify]: Simplify 0 into 0 0.429 * [backup-simplify]: Simplify (+ (* 1 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (* 0 1))))) into 0 0.431 * [backup-simplify]: Simplify (+ (* 3 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (* 0 1))))) into 0 0.431 * [backup-simplify]: Simplify 0 into 0 0.432 * [backup-simplify]: Simplify (+ (* 1 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (* 0 1)))))) into 0 0.433 * [backup-simplify]: Simplify (+ (* 3 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (* 0 1)))))) into 0 0.433 * [backup-simplify]: Simplify 0 into 0 0.434 * [backup-simplify]: Simplify (+ (* 1 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (* 0 1))))))) into 0 0.435 * [backup-simplify]: Simplify (+ (* 3 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (* 0 1))))))) into 0 0.435 * [backup-simplify]: Simplify 0 into 0 0.435 * [backup-simplify]: Simplify (* 3 (pow v 2)) into (* 3 (pow v 2)) 0.435 * [backup-simplify]: Simplify (* 3 (* (/ 1 v) (/ 1 v))) into (/ 3 (pow v 2)) 0.435 * [approximate]: Taking taylor expansion of (/ 3 (pow v 2)) in (v) around 0 0.435 * [taylor]: Taking taylor expansion of (/ 3 (pow v 2)) in v 0.435 * [taylor]: Taking taylor expansion of 3 in v 0.435 * [backup-simplify]: Simplify 3 into 3 0.435 * [taylor]: Taking taylor expansion of (pow v 2) in v 0.435 * [taylor]: Taking taylor expansion of v in v 0.436 * [backup-simplify]: Simplify 0 into 0 0.436 * [backup-simplify]: Simplify 1 into 1 0.436 * [backup-simplify]: Simplify (* 1 1) into 1 0.436 * [backup-simplify]: Simplify (/ 3 1) into 3 0.436 * [taylor]: Taking taylor expansion of (/ 3 (pow v 2)) in v 0.436 * [taylor]: Taking taylor expansion of 3 in v 0.436 * [backup-simplify]: Simplify 3 into 3 0.436 * [taylor]: Taking taylor expansion of (pow v 2) in v 0.436 * [taylor]: Taking taylor expansion of v in v 0.436 * [backup-simplify]: Simplify 0 into 0 0.436 * [backup-simplify]: Simplify 1 into 1 0.436 * [backup-simplify]: Simplify (* 1 1) into 1 0.437 * [backup-simplify]: Simplify (/ 3 1) into 3 0.437 * [backup-simplify]: Simplify 3 into 3 0.437 * [backup-simplify]: Simplify (+ (* 1 0) (* 0 1)) into 0 0.438 * [backup-simplify]: Simplify (- (/ 0 1) (+ (* 3 (/ 0 1)))) into 0 0.438 * [backup-simplify]: Simplify 0 into 0 0.438 * [backup-simplify]: Simplify (+ (* 1 0) (+ (* 0 0) (* 0 1))) into 0 0.439 * [backup-simplify]: Simplify (- (/ 0 1) (+ (* 3 (/ 0 1)) (* 0 (/ 0 1)))) into 0 0.439 * [backup-simplify]: Simplify 0 into 0 0.439 * [backup-simplify]: Simplify (+ (* 1 0) (+ (* 0 0) (+ (* 0 0) (* 0 1)))) into 0 0.440 * [backup-simplify]: Simplify (- (/ 0 1) (+ (* 3 (/ 0 1)) (* 0 (/ 0 1)) (* 0 (/ 0 1)))) into 0 0.440 * [backup-simplify]: Simplify 0 into 0 0.441 * [backup-simplify]: Simplify (+ (* 1 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (* 0 1))))) into 0 0.441 * [backup-simplify]: Simplify (- (/ 0 1) (+ (* 3 (/ 0 1)) (* 0 (/ 0 1)) (* 0 (/ 0 1)) (* 0 (/ 0 1)))) into 0 0.441 * [backup-simplify]: Simplify 0 into 0 0.442 * [backup-simplify]: Simplify (+ (* 1 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (* 0 1)))))) into 0 0.443 * [backup-simplify]: Simplify (- (/ 0 1) (+ (* 3 (/ 0 1)) (* 0 (/ 0 1)) (* 0 (/ 0 1)) (* 0 (/ 0 1)) (* 0 (/ 0 1)))) into 0 0.443 * [backup-simplify]: Simplify 0 into 0 0.446 * [backup-simplify]: Simplify (+ (* 1 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (* 0 1))))))) into 0 0.447 * [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 0.447 * [backup-simplify]: Simplify 0 into 0 0.447 * [backup-simplify]: Simplify (* 3 (pow (/ 1 (/ 1 v)) 2)) into (* 3 (pow v 2)) 0.447 * [backup-simplify]: Simplify (* 3 (* (/ 1 (- v)) (/ 1 (- v)))) into (/ 3 (pow v 2)) 0.447 * [approximate]: Taking taylor expansion of (/ 3 (pow v 2)) in (v) around 0 0.447 * [taylor]: Taking taylor expansion of (/ 3 (pow v 2)) in v 0.447 * [taylor]: Taking taylor expansion of 3 in v 0.447 * [backup-simplify]: Simplify 3 into 3 0.447 * [taylor]: Taking taylor expansion of (pow v 2) in v 0.447 * [taylor]: Taking taylor expansion of v in v 0.447 * [backup-simplify]: Simplify 0 into 0 0.447 * [backup-simplify]: Simplify 1 into 1 0.448 * [backup-simplify]: Simplify (* 1 1) into 1 0.448 * [backup-simplify]: Simplify (/ 3 1) into 3 0.448 * [taylor]: Taking taylor expansion of (/ 3 (pow v 2)) in v 0.448 * [taylor]: Taking taylor expansion of 3 in v 0.448 * [backup-simplify]: Simplify 3 into 3 0.448 * [taylor]: Taking taylor expansion of (pow v 2) in v 0.448 * [taylor]: Taking taylor expansion of v in v 0.448 * [backup-simplify]: Simplify 0 into 0 0.448 * [backup-simplify]: Simplify 1 into 1 0.448 * [backup-simplify]: Simplify (* 1 1) into 1 0.449 * [backup-simplify]: Simplify (/ 3 1) into 3 0.449 * [backup-simplify]: Simplify 3 into 3 0.449 * [backup-simplify]: Simplify (+ (* 1 0) (* 0 1)) into 0 0.450 * [backup-simplify]: Simplify (- (/ 0 1) (+ (* 3 (/ 0 1)))) into 0 0.450 * [backup-simplify]: Simplify 0 into 0 0.450 * [backup-simplify]: Simplify (+ (* 1 0) (+ (* 0 0) (* 0 1))) into 0 0.451 * [backup-simplify]: Simplify (- (/ 0 1) (+ (* 3 (/ 0 1)) (* 0 (/ 0 1)))) into 0 0.451 * [backup-simplify]: Simplify 0 into 0 0.451 * [backup-simplify]: Simplify (+ (* 1 0) (+ (* 0 0) (+ (* 0 0) (* 0 1)))) into 0 0.452 * [backup-simplify]: Simplify (- (/ 0 1) (+ (* 3 (/ 0 1)) (* 0 (/ 0 1)) (* 0 (/ 0 1)))) into 0 0.452 * [backup-simplify]: Simplify 0 into 0 0.453 * [backup-simplify]: Simplify (+ (* 1 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (* 0 1))))) into 0 0.453 * [backup-simplify]: Simplify (- (/ 0 1) (+ (* 3 (/ 0 1)) (* 0 (/ 0 1)) (* 0 (/ 0 1)) (* 0 (/ 0 1)))) into 0 0.453 * [backup-simplify]: Simplify 0 into 0 0.454 * [backup-simplify]: Simplify (+ (* 1 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (* 0 1)))))) into 0 0.455 * [backup-simplify]: Simplify (- (/ 0 1) (+ (* 3 (/ 0 1)) (* 0 (/ 0 1)) (* 0 (/ 0 1)) (* 0 (/ 0 1)) (* 0 (/ 0 1)))) into 0 0.455 * [backup-simplify]: Simplify 0 into 0 0.455 * [backup-simplify]: Simplify (+ (* 1 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (* 0 1))))))) into 0 0.456 * [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 0.456 * [backup-simplify]: Simplify 0 into 0 0.456 * [backup-simplify]: Simplify (* 3 (pow (/ 1 (/ 1 (- v))) 2)) into (* 3 (pow v 2)) 0.456 * * * * [progress]: [ 2 / 3 ] generating series at (2 1 2) 0.457 * [backup-simplify]: Simplify (sqrt (- 1 (* 3 (* v v)))) into (sqrt (- 1 (* 3 (pow v 2)))) 0.457 * [approximate]: Taking taylor expansion of (sqrt (- 1 (* 3 (pow v 2)))) in (v) around 0 0.457 * [taylor]: Taking taylor expansion of (sqrt (- 1 (* 3 (pow v 2)))) in v 0.457 * [taylor]: Taking taylor expansion of (- 1 (* 3 (pow v 2))) in v 0.457 * [taylor]: Taking taylor expansion of 1 in v 0.457 * [backup-simplify]: Simplify 1 into 1 0.457 * [taylor]: Taking taylor expansion of (* 3 (pow v 2)) in v 0.457 * [taylor]: Taking taylor expansion of 3 in v 0.457 * [backup-simplify]: Simplify 3 into 3 0.457 * [taylor]: Taking taylor expansion of (pow v 2) in v 0.457 * [taylor]: Taking taylor expansion of v in v 0.457 * [backup-simplify]: Simplify 0 into 0 0.457 * [backup-simplify]: Simplify 1 into 1 0.457 * [backup-simplify]: Simplify (+ 1 0) into 1 0.457 * [backup-simplify]: Simplify (sqrt 1) into 1 0.457 * [backup-simplify]: Simplify (+ 0 0) into 0 0.458 * [backup-simplify]: Simplify (/ 0 (* 2 (sqrt 1))) into 0 0.458 * [taylor]: Taking taylor expansion of (sqrt (- 1 (* 3 (pow v 2)))) in v 0.458 * [taylor]: Taking taylor expansion of (- 1 (* 3 (pow v 2))) in v 0.458 * [taylor]: Taking taylor expansion of 1 in v 0.458 * [backup-simplify]: Simplify 1 into 1 0.458 * [taylor]: Taking taylor expansion of (* 3 (pow v 2)) in v 0.458 * [taylor]: Taking taylor expansion of 3 in v 0.458 * [backup-simplify]: Simplify 3 into 3 0.458 * [taylor]: Taking taylor expansion of (pow v 2) in v 0.458 * [taylor]: Taking taylor expansion of v in v 0.458 * [backup-simplify]: Simplify 0 into 0 0.458 * [backup-simplify]: Simplify 1 into 1 0.458 * [backup-simplify]: Simplify (+ 1 0) into 1 0.459 * [backup-simplify]: Simplify (sqrt 1) into 1 0.459 * [backup-simplify]: Simplify (+ 0 0) into 0 0.459 * [backup-simplify]: Simplify (/ 0 (* 2 (sqrt 1))) into 0 0.459 * [backup-simplify]: Simplify 1 into 1 0.459 * [backup-simplify]: Simplify 0 into 0 0.460 * [backup-simplify]: Simplify (* 1 1) into 1 0.460 * [backup-simplify]: Simplify (* 3 1) into 3 0.460 * [backup-simplify]: Simplify (- 3) into -3 0.460 * [backup-simplify]: Simplify (+ 0 -3) into -3 0.461 * [backup-simplify]: Simplify (/ (- -3 (pow 0 2) (+)) (* 2 1)) into -3/2 0.461 * [backup-simplify]: Simplify -3/2 into -3/2 0.461 * [backup-simplify]: Simplify (+ (* 1 0) (* 0 1)) into 0 0.462 * [backup-simplify]: Simplify (+ (* 3 0) (* 0 1)) into 0 0.462 * [backup-simplify]: Simplify (- 0) into 0 0.463 * [backup-simplify]: Simplify (+ 0 0) into 0 0.464 * [backup-simplify]: Simplify (/ (- 0 (+ (* 2 (* 0 -3/2)))) (* 2 1)) into 0 0.464 * [backup-simplify]: Simplify 0 into 0 0.465 * [backup-simplify]: Simplify (+ (* 1 0) (+ (* 0 0) (* 0 1))) into 0 0.466 * [backup-simplify]: Simplify (+ (* 3 0) (+ (* 0 0) (* 0 1))) into 0 0.466 * [backup-simplify]: Simplify (- 0) into 0 0.467 * [backup-simplify]: Simplify (+ 0 0) into 0 0.468 * [backup-simplify]: Simplify (/ (- 0 (pow -3/2 2) (+ (* 2 (* 0 0)))) (* 2 1)) into -9/8 0.468 * [backup-simplify]: Simplify -9/8 into -9/8 0.468 * [backup-simplify]: Simplify (+ (* -9/8 (pow v 4)) (+ (* -3/2 (pow v 2)) 1)) into (- 1 (+ (* 9/8 (pow v 4)) (* 3/2 (pow v 2)))) 0.469 * [backup-simplify]: Simplify (sqrt (- 1 (* 3 (* (/ 1 v) (/ 1 v))))) into (sqrt (- 1 (* 3 (/ 1 (pow v 2))))) 0.469 * [approximate]: Taking taylor expansion of (sqrt (- 1 (* 3 (/ 1 (pow v 2))))) in (v) around 0 0.469 * [taylor]: Taking taylor expansion of (sqrt (- 1 (* 3 (/ 1 (pow v 2))))) in v 0.469 * [taylor]: Taking taylor expansion of (- 1 (* 3 (/ 1 (pow v 2)))) in v 0.469 * [taylor]: Taking taylor expansion of 1 in v 0.469 * [backup-simplify]: Simplify 1 into 1 0.469 * [taylor]: Taking taylor expansion of (* 3 (/ 1 (pow v 2))) in v 0.469 * [taylor]: Taking taylor expansion of 3 in v 0.469 * [backup-simplify]: Simplify 3 into 3 0.469 * [taylor]: Taking taylor expansion of (/ 1 (pow v 2)) in v 0.469 * [taylor]: Taking taylor expansion of (pow v 2) in v 0.469 * [taylor]: Taking taylor expansion of v in v 0.469 * [backup-simplify]: Simplify 0 into 0 0.469 * [backup-simplify]: Simplify 1 into 1 0.469 * [backup-simplify]: Simplify (* 1 1) into 1 0.470 * [backup-simplify]: Simplify (/ 1 1) into 1 0.470 * [backup-simplify]: Simplify (* 3 1) into 3 0.471 * [backup-simplify]: Simplify (- 3) into -3 0.471 * [backup-simplify]: Simplify (+ 0 -3) into -3 0.471 * [backup-simplify]: Simplify (sqrt -3) into (sqrt -3) 0.472 * [backup-simplify]: Simplify (+ (* 1 0) (* 0 1)) into 0 0.473 * [backup-simplify]: Simplify (- (+ (* 1 (/ 0 1)))) into 0 0.473 * [backup-simplify]: Simplify (+ (* 3 0) (* 0 1)) into 0 0.474 * [backup-simplify]: Simplify (- 0) into 0 0.474 * [backup-simplify]: Simplify (+ 0 0) into 0 0.475 * [backup-simplify]: Simplify (/ 0 (* 2 (sqrt -3))) into 0 0.475 * [taylor]: Taking taylor expansion of (sqrt (- 1 (* 3 (/ 1 (pow v 2))))) in v 0.475 * [taylor]: Taking taylor expansion of (- 1 (* 3 (/ 1 (pow v 2)))) in v 0.475 * [taylor]: Taking taylor expansion of 1 in v 0.475 * [backup-simplify]: Simplify 1 into 1 0.475 * [taylor]: Taking taylor expansion of (* 3 (/ 1 (pow v 2))) in v 0.475 * [taylor]: Taking taylor expansion of 3 in v 0.475 * [backup-simplify]: Simplify 3 into 3 0.475 * [taylor]: Taking taylor expansion of (/ 1 (pow v 2)) in v 0.475 * [taylor]: Taking taylor expansion of (pow v 2) in v 0.475 * [taylor]: Taking taylor expansion of v in v 0.475 * [backup-simplify]: Simplify 0 into 0 0.475 * [backup-simplify]: Simplify 1 into 1 0.476 * [backup-simplify]: Simplify (* 1 1) into 1 0.476 * [backup-simplify]: Simplify (/ 1 1) into 1 0.476 * [backup-simplify]: Simplify (* 3 1) into 3 0.477 * [backup-simplify]: Simplify (- 3) into -3 0.477 * [backup-simplify]: Simplify (+ 0 -3) into -3 0.478 * [backup-simplify]: Simplify (sqrt -3) into (sqrt -3) 0.478 * [backup-simplify]: Simplify (+ (* 1 0) (* 0 1)) into 0 0.479 * [backup-simplify]: Simplify (- (+ (* 1 (/ 0 1)))) into 0 0.480 * [backup-simplify]: Simplify (+ (* 3 0) (* 0 1)) into 0 0.480 * [backup-simplify]: Simplify (- 0) into 0 0.480 * [backup-simplify]: Simplify (+ 0 0) into 0 0.481 * [backup-simplify]: Simplify (/ 0 (* 2 (sqrt -3))) into 0 0.482 * [backup-simplify]: Simplify (sqrt -3) into (sqrt -3) 0.482 * [backup-simplify]: Simplify 0 into 0 0.483 * [backup-simplify]: Simplify (+ (* 1 0) (+ (* 0 0) (* 0 1))) into 0 0.483 * [backup-simplify]: Simplify (- (+ (* 1 (/ 0 1)) (* 0 (/ 0 1)))) into 0 0.484 * [backup-simplify]: Simplify (+ (* 3 0) (+ (* 0 0) (* 0 1))) into 0 0.485 * [backup-simplify]: Simplify (- 0) into 0 0.485 * [backup-simplify]: Simplify (+ 1 0) into 1 0.488 * [backup-simplify]: Simplify (/ (- 1 (pow 0 2) (+)) (* 2 (sqrt -3))) into (/ 1/2 (sqrt -3)) 0.489 * [backup-simplify]: Simplify (/ 1/2 (sqrt -3)) into (/ 1/2 (sqrt -3)) 0.490 * [backup-simplify]: Simplify (+ (* 1 0) (+ (* 0 0) (+ (* 0 0) (* 0 1)))) into 0 0.491 * [backup-simplify]: Simplify (- (+ (* 1 (/ 0 1)) (* 0 (/ 0 1)) (* 0 (/ 0 1)))) into 0 0.492 * [backup-simplify]: Simplify (+ (* 3 0) (+ (* 0 0) (+ (* 0 0) (* 0 1)))) into 0 0.493 * [backup-simplify]: Simplify (- 0) into 0 0.493 * [backup-simplify]: Simplify (+ 0 0) into 0 0.494 * [backup-simplify]: Simplify (/ (- 0 (+ (* 2 (* 0 (/ 1/2 (sqrt -3)))))) (* 2 (sqrt -3))) into 0 0.494 * [backup-simplify]: Simplify 0 into 0 0.495 * [backup-simplify]: Simplify (+ (* 1 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (* 0 1))))) into 0 0.495 * [backup-simplify]: Simplify (- (+ (* 1 (/ 0 1)) (* 0 (/ 0 1)) (* 0 (/ 0 1)) (* 0 (/ 0 1)))) into 0 0.496 * [backup-simplify]: Simplify (+ (* 3 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (* 0 1))))) into 0 0.496 * [backup-simplify]: Simplify (- 0) into 0 0.496 * [backup-simplify]: Simplify (+ 0 0) into 0 0.500 * [backup-simplify]: Simplify (/ (- 0 (pow (/ 1/2 (sqrt -3)) 2) (+ (* 2 (* 0 0)))) (* 2 (sqrt -3))) into (/ -1/8 (pow (sqrt -3) 3)) 0.501 * [backup-simplify]: Simplify (/ -1/8 (pow (sqrt -3) 3)) into (/ -1/8 (pow (sqrt -3) 3)) 0.503 * [backup-simplify]: Simplify (+ (* (/ -1/8 (pow (sqrt -3) 3)) (pow (/ 1 v) 3)) (+ (* (/ 1/2 (sqrt -3)) (/ 1 v)) (* (sqrt -3) (/ 1 (/ 1 v))))) into (- (+ (* 1/2 (/ 1 (* (sqrt -3) v))) (* (sqrt -3) v)) (* 1/8 (/ 1 (* (pow (sqrt -3) 3) (pow v 3))))) 0.504 * [backup-simplify]: Simplify (sqrt (- 1 (* 3 (* (/ 1 (- v)) (/ 1 (- v)))))) into (sqrt (- 1 (* 3 (/ 1 (pow v 2))))) 0.504 * [approximate]: Taking taylor expansion of (sqrt (- 1 (* 3 (/ 1 (pow v 2))))) in (v) around 0 0.504 * [taylor]: Taking taylor expansion of (sqrt (- 1 (* 3 (/ 1 (pow v 2))))) in v 0.504 * [taylor]: Taking taylor expansion of (- 1 (* 3 (/ 1 (pow v 2)))) in v 0.504 * [taylor]: Taking taylor expansion of 1 in v 0.504 * [backup-simplify]: Simplify 1 into 1 0.504 * [taylor]: Taking taylor expansion of (* 3 (/ 1 (pow v 2))) in v 0.504 * [taylor]: Taking taylor expansion of 3 in v 0.504 * [backup-simplify]: Simplify 3 into 3 0.504 * [taylor]: Taking taylor expansion of (/ 1 (pow v 2)) in v 0.504 * [taylor]: Taking taylor expansion of (pow v 2) in v 0.504 * [taylor]: Taking taylor expansion of v in v 0.504 * [backup-simplify]: Simplify 0 into 0 0.504 * [backup-simplify]: Simplify 1 into 1 0.504 * [backup-simplify]: Simplify (* 1 1) into 1 0.504 * [backup-simplify]: Simplify (/ 1 1) into 1 0.505 * [backup-simplify]: Simplify (* 3 1) into 3 0.505 * [backup-simplify]: Simplify (- 3) into -3 0.505 * [backup-simplify]: Simplify (+ 0 -3) into -3 0.505 * [backup-simplify]: Simplify (sqrt -3) into (sqrt -3) 0.506 * [backup-simplify]: Simplify (+ (* 1 0) (* 0 1)) into 0 0.506 * [backup-simplify]: Simplify (- (+ (* 1 (/ 0 1)))) into 0 0.507 * [backup-simplify]: Simplify (+ (* 3 0) (* 0 1)) into 0 0.507 * [backup-simplify]: Simplify (- 0) into 0 0.507 * [backup-simplify]: Simplify (+ 0 0) into 0 0.508 * [backup-simplify]: Simplify (/ 0 (* 2 (sqrt -3))) into 0 0.508 * [taylor]: Taking taylor expansion of (sqrt (- 1 (* 3 (/ 1 (pow v 2))))) in v 0.508 * [taylor]: Taking taylor expansion of (- 1 (* 3 (/ 1 (pow v 2)))) in v 0.508 * [taylor]: Taking taylor expansion of 1 in v 0.508 * [backup-simplify]: Simplify 1 into 1 0.508 * [taylor]: Taking taylor expansion of (* 3 (/ 1 (pow v 2))) in v 0.508 * [taylor]: Taking taylor expansion of 3 in v 0.508 * [backup-simplify]: Simplify 3 into 3 0.508 * [taylor]: Taking taylor expansion of (/ 1 (pow v 2)) in v 0.508 * [taylor]: Taking taylor expansion of (pow v 2) in v 0.508 * [taylor]: Taking taylor expansion of v in v 0.508 * [backup-simplify]: Simplify 0 into 0 0.508 * [backup-simplify]: Simplify 1 into 1 0.508 * [backup-simplify]: Simplify (* 1 1) into 1 0.508 * [backup-simplify]: Simplify (/ 1 1) into 1 0.509 * [backup-simplify]: Simplify (* 3 1) into 3 0.509 * [backup-simplify]: Simplify (- 3) into -3 0.509 * [backup-simplify]: Simplify (+ 0 -3) into -3 0.509 * [backup-simplify]: Simplify (sqrt -3) into (sqrt -3) 0.510 * [backup-simplify]: Simplify (+ (* 1 0) (* 0 1)) into 0 0.510 * [backup-simplify]: Simplify (- (+ (* 1 (/ 0 1)))) into 0 0.511 * [backup-simplify]: Simplify (+ (* 3 0) (* 0 1)) into 0 0.511 * [backup-simplify]: Simplify (- 0) into 0 0.511 * [backup-simplify]: Simplify (+ 0 0) into 0 0.512 * [backup-simplify]: Simplify (/ 0 (* 2 (sqrt -3))) into 0 0.512 * [backup-simplify]: Simplify (sqrt -3) into (sqrt -3) 0.512 * [backup-simplify]: Simplify 0 into 0 0.512 * [backup-simplify]: Simplify (+ (* 1 0) (+ (* 0 0) (* 0 1))) into 0 0.513 * [backup-simplify]: Simplify (- (+ (* 1 (/ 0 1)) (* 0 (/ 0 1)))) into 0 0.514 * [backup-simplify]: Simplify (+ (* 3 0) (+ (* 0 0) (* 0 1))) into 0 0.514 * [backup-simplify]: Simplify (- 0) into 0 0.514 * [backup-simplify]: Simplify (+ 1 0) into 1 0.516 * [backup-simplify]: Simplify (/ (- 1 (pow 0 2) (+)) (* 2 (sqrt -3))) into (/ 1/2 (sqrt -3)) 0.516 * [backup-simplify]: Simplify (/ 1/2 (sqrt -3)) into (/ 1/2 (sqrt -3)) 0.517 * [backup-simplify]: Simplify (+ (* 1 0) (+ (* 0 0) (+ (* 0 0) (* 0 1)))) into 0 0.517 * [backup-simplify]: Simplify (- (+ (* 1 (/ 0 1)) (* 0 (/ 0 1)) (* 0 (/ 0 1)))) into 0 0.518 * [backup-simplify]: Simplify (+ (* 3 0) (+ (* 0 0) (+ (* 0 0) (* 0 1)))) into 0 0.518 * [backup-simplify]: Simplify (- 0) into 0 0.519 * [backup-simplify]: Simplify (+ 0 0) into 0 0.519 * [backup-simplify]: Simplify (/ (- 0 (+ (* 2 (* 0 (/ 1/2 (sqrt -3)))))) (* 2 (sqrt -3))) into 0 0.519 * [backup-simplify]: Simplify 0 into 0 0.520 * [backup-simplify]: Simplify (+ (* 1 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (* 0 1))))) into 0 0.521 * [backup-simplify]: Simplify (- (+ (* 1 (/ 0 1)) (* 0 (/ 0 1)) (* 0 (/ 0 1)) (* 0 (/ 0 1)))) into 0 0.521 * [backup-simplify]: Simplify (+ (* 3 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (* 0 1))))) into 0 0.522 * [backup-simplify]: Simplify (- 0) into 0 0.522 * [backup-simplify]: Simplify (+ 0 0) into 0 0.526 * [backup-simplify]: Simplify (/ (- 0 (pow (/ 1/2 (sqrt -3)) 2) (+ (* 2 (* 0 0)))) (* 2 (sqrt -3))) into (/ -1/8 (pow (sqrt -3) 3)) 0.527 * [backup-simplify]: Simplify (/ -1/8 (pow (sqrt -3) 3)) into (/ -1/8 (pow (sqrt -3) 3)) 0.529 * [backup-simplify]: Simplify (+ (* (/ -1/8 (pow (sqrt -3) 3)) (pow (/ 1 (- v)) 3)) (+ (* (/ 1/2 (sqrt -3)) (/ 1 (- v))) (* (sqrt -3) (/ 1 (/ 1 (- v)))))) into (- (* 1/8 (/ 1 (* (pow (sqrt -3) 3) (pow v 3)))) (+ (* 1/2 (/ 1 (* (sqrt -3) v))) (* (sqrt -3) v))) 0.529 * * * * [progress]: [ 3 / 3 ] generating series at (2 1) 0.530 * [backup-simplify]: Simplify (* (/ (sqrt 2) 4) (sqrt (- 1 (* 3 (* v v))))) into (* 1/4 (* (sqrt (- 1 (* 3 (pow v 2)))) (sqrt 2))) 0.530 * [approximate]: Taking taylor expansion of (* 1/4 (* (sqrt (- 1 (* 3 (pow v 2)))) (sqrt 2))) in (v) around 0 0.530 * [taylor]: Taking taylor expansion of (* 1/4 (* (sqrt (- 1 (* 3 (pow v 2)))) (sqrt 2))) in v 0.530 * [taylor]: Taking taylor expansion of 1/4 in v 0.530 * [backup-simplify]: Simplify 1/4 into 1/4 0.530 * [taylor]: Taking taylor expansion of (* (sqrt (- 1 (* 3 (pow v 2)))) (sqrt 2)) in v 0.530 * [taylor]: Taking taylor expansion of (sqrt (- 1 (* 3 (pow v 2)))) in v 0.530 * [taylor]: Taking taylor expansion of (- 1 (* 3 (pow v 2))) in v 0.531 * [taylor]: Taking taylor expansion of 1 in v 0.531 * [backup-simplify]: Simplify 1 into 1 0.531 * [taylor]: Taking taylor expansion of (* 3 (pow v 2)) in v 0.531 * [taylor]: Taking taylor expansion of 3 in v 0.531 * [backup-simplify]: Simplify 3 into 3 0.531 * [taylor]: Taking taylor expansion of (pow v 2) in v 0.531 * [taylor]: Taking taylor expansion of v in v 0.531 * [backup-simplify]: Simplify 0 into 0 0.531 * [backup-simplify]: Simplify 1 into 1 0.531 * [backup-simplify]: Simplify (+ 1 0) into 1 0.532 * [backup-simplify]: Simplify (sqrt 1) into 1 0.532 * [backup-simplify]: Simplify (+ 0 0) into 0 0.533 * [backup-simplify]: Simplify (/ 0 (* 2 (sqrt 1))) into 0 0.533 * [taylor]: Taking taylor expansion of (sqrt 2) in v 0.533 * [taylor]: Taking taylor expansion of 2 in v 0.533 * [backup-simplify]: Simplify 2 into 2 0.533 * [backup-simplify]: Simplify (sqrt 2) into (sqrt 2) 0.534 * [backup-simplify]: Simplify (/ 0 (* 2 (sqrt 2))) into 0 0.534 * [taylor]: Taking taylor expansion of (* 1/4 (* (sqrt (- 1 (* 3 (pow v 2)))) (sqrt 2))) in v 0.534 * [taylor]: Taking taylor expansion of 1/4 in v 0.534 * [backup-simplify]: Simplify 1/4 into 1/4 0.534 * [taylor]: Taking taylor expansion of (* (sqrt (- 1 (* 3 (pow v 2)))) (sqrt 2)) in v 0.534 * [taylor]: Taking taylor expansion of (sqrt (- 1 (* 3 (pow v 2)))) in v 0.534 * [taylor]: Taking taylor expansion of (- 1 (* 3 (pow v 2))) in v 0.534 * [taylor]: Taking taylor expansion of 1 in v 0.534 * [backup-simplify]: Simplify 1 into 1 0.534 * [taylor]: Taking taylor expansion of (* 3 (pow v 2)) in v 0.534 * [taylor]: Taking taylor expansion of 3 in v 0.534 * [backup-simplify]: Simplify 3 into 3 0.534 * [taylor]: Taking taylor expansion of (pow v 2) in v 0.534 * [taylor]: Taking taylor expansion of v in v 0.534 * [backup-simplify]: Simplify 0 into 0 0.534 * [backup-simplify]: Simplify 1 into 1 0.535 * [backup-simplify]: Simplify (+ 1 0) into 1 0.535 * [backup-simplify]: Simplify (sqrt 1) into 1 0.535 * [backup-simplify]: Simplify (+ 0 0) into 0 0.536 * [backup-simplify]: Simplify (/ 0 (* 2 (sqrt 1))) into 0 0.536 * [taylor]: Taking taylor expansion of (sqrt 2) in v 0.536 * [taylor]: Taking taylor expansion of 2 in v 0.536 * [backup-simplify]: Simplify 2 into 2 0.536 * [backup-simplify]: Simplify (sqrt 2) into (sqrt 2) 0.537 * [backup-simplify]: Simplify (/ 0 (* 2 (sqrt 2))) into 0 0.538 * [backup-simplify]: Simplify (* 1 (sqrt 2)) into (sqrt 2) 0.539 * [backup-simplify]: Simplify (* 1/4 (sqrt 2)) into (* 1/4 (sqrt 2)) 0.540 * [backup-simplify]: Simplify (* 1/4 (sqrt 2)) into (* 1/4 (sqrt 2)) 0.541 * [backup-simplify]: Simplify (+ (* 1 0) (* 0 (sqrt 2))) into 0 0.542 * [backup-simplify]: Simplify (+ (* 1/4 0) (* 0 (sqrt 2))) into 0 0.542 * [backup-simplify]: Simplify 0 into 0 0.543 * [backup-simplify]: Simplify (/ (- 0 (pow 0 2) (+)) (* 2 (sqrt 2))) into 0 0.543 * [backup-simplify]: Simplify (* 1 1) into 1 0.543 * [backup-simplify]: Simplify (* 3 1) into 3 0.544 * [backup-simplify]: Simplify (- 3) into -3 0.544 * [backup-simplify]: Simplify (+ 0 -3) into -3 0.545 * [backup-simplify]: Simplify (/ (- -3 (pow 0 2) (+)) (* 2 1)) into -3/2 0.549 * [backup-simplify]: Simplify (+ (* 1 0) (+ (* 0 0) (* -3/2 (sqrt 2)))) into (- (* 3/2 (sqrt 2))) 0.556 * [backup-simplify]: Simplify (+ (* 1/4 (- (* 3/2 (sqrt 2)))) (+ (* 0 0) (* 0 (sqrt 2)))) into (- (* 3/8 (sqrt 2))) 0.558 * [backup-simplify]: Simplify (- (* 3/8 (sqrt 2))) into (- (* 3/8 (sqrt 2))) 0.559 * [backup-simplify]: Simplify (/ (- 0 (+ (* 2 (* 0 0)))) (* 2 (sqrt 2))) into 0 0.560 * [backup-simplify]: Simplify (+ (* 1 0) (* 0 1)) into 0 0.560 * [backup-simplify]: Simplify (+ (* 3 0) (* 0 1)) into 0 0.561 * [backup-simplify]: Simplify (- 0) into 0 0.561 * [backup-simplify]: Simplify (+ 0 0) into 0 0.562 * [backup-simplify]: Simplify (/ (- 0 (+ (* 2 (* 0 -3/2)))) (* 2 1)) into 0 0.563 * [backup-simplify]: Simplify (+ (* 1 0) (+ (* 0 0) (+ (* -3/2 0) (* 0 (sqrt 2))))) into 0 0.564 * [backup-simplify]: Simplify (+ (* 1/4 0) (+ (* 0 (- (* 3/2 (sqrt 2)))) (+ (* 0 0) (* 0 (sqrt 2))))) into 0 0.564 * [backup-simplify]: Simplify 0 into 0 0.565 * [backup-simplify]: Simplify (/ (- 0 (pow 0 2) (+ (* 2 (* 0 0)))) (* 2 (sqrt 2))) into 0 0.565 * [backup-simplify]: Simplify (+ (* 1 0) (+ (* 0 0) (* 0 1))) into 0 0.566 * [backup-simplify]: Simplify (+ (* 3 0) (+ (* 0 0) (* 0 1))) into 0 0.566 * [backup-simplify]: Simplify (- 0) into 0 0.566 * [backup-simplify]: Simplify (+ 0 0) into 0 0.567 * [backup-simplify]: Simplify (/ (- 0 (pow -3/2 2) (+ (* 2 (* 0 0)))) (* 2 1)) into -9/8 0.571 * [backup-simplify]: Simplify (+ (* 1 0) (+ (* 0 0) (+ (* -3/2 0) (+ (* 0 0) (* -9/8 (sqrt 2)))))) into (- (* 9/8 (sqrt 2))) 0.575 * [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))) 0.576 * [backup-simplify]: Simplify (- (* 9/32 (sqrt 2))) into (- (* 9/32 (sqrt 2))) 0.579 * [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))))) 0.579 * [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))))))) 0.579 * [approximate]: Taking taylor expansion of (* 1/4 (* (sqrt 2) (sqrt (- 1 (* 3 (/ 1 (pow v 2))))))) in (v) around 0 0.579 * [taylor]: Taking taylor expansion of (* 1/4 (* (sqrt 2) (sqrt (- 1 (* 3 (/ 1 (pow v 2))))))) in v 0.579 * [taylor]: Taking taylor expansion of 1/4 in v 0.579 * [backup-simplify]: Simplify 1/4 into 1/4 0.579 * [taylor]: Taking taylor expansion of (* (sqrt 2) (sqrt (- 1 (* 3 (/ 1 (pow v 2)))))) in v 0.579 * [taylor]: Taking taylor expansion of (sqrt 2) in v 0.579 * [taylor]: Taking taylor expansion of 2 in v 0.579 * [backup-simplify]: Simplify 2 into 2 0.580 * [backup-simplify]: Simplify (sqrt 2) into (sqrt 2) 0.580 * [backup-simplify]: Simplify (/ 0 (* 2 (sqrt 2))) into 0 0.580 * [taylor]: Taking taylor expansion of (sqrt (- 1 (* 3 (/ 1 (pow v 2))))) in v 0.580 * [taylor]: Taking taylor expansion of (- 1 (* 3 (/ 1 (pow v 2)))) in v 0.580 * [taylor]: Taking taylor expansion of 1 in v 0.580 * [backup-simplify]: Simplify 1 into 1 0.580 * [taylor]: Taking taylor expansion of (* 3 (/ 1 (pow v 2))) in v 0.580 * [taylor]: Taking taylor expansion of 3 in v 0.580 * [backup-simplify]: Simplify 3 into 3 0.580 * [taylor]: Taking taylor expansion of (/ 1 (pow v 2)) in v 0.580 * [taylor]: Taking taylor expansion of (pow v 2) in v 0.580 * [taylor]: Taking taylor expansion of v in v 0.580 * [backup-simplify]: Simplify 0 into 0 0.580 * [backup-simplify]: Simplify 1 into 1 0.580 * [backup-simplify]: Simplify (* 1 1) into 1 0.581 * [backup-simplify]: Simplify (/ 1 1) into 1 0.581 * [backup-simplify]: Simplify (* 3 1) into 3 0.581 * [backup-simplify]: Simplify (- 3) into -3 0.582 * [backup-simplify]: Simplify (+ 0 -3) into -3 0.582 * [backup-simplify]: Simplify (sqrt -3) into (sqrt -3) 0.582 * [backup-simplify]: Simplify (+ (* 1 0) (* 0 1)) into 0 0.583 * [backup-simplify]: Simplify (- (+ (* 1 (/ 0 1)))) into 0 0.583 * [backup-simplify]: Simplify (+ (* 3 0) (* 0 1)) into 0 0.583 * [backup-simplify]: Simplify (- 0) into 0 0.584 * [backup-simplify]: Simplify (+ 0 0) into 0 0.584 * [backup-simplify]: Simplify (/ 0 (* 2 (sqrt -3))) into 0 0.584 * [taylor]: Taking taylor expansion of (* 1/4 (* (sqrt 2) (sqrt (- 1 (* 3 (/ 1 (pow v 2))))))) in v 0.584 * [taylor]: Taking taylor expansion of 1/4 in v 0.584 * [backup-simplify]: Simplify 1/4 into 1/4 0.584 * [taylor]: Taking taylor expansion of (* (sqrt 2) (sqrt (- 1 (* 3 (/ 1 (pow v 2)))))) in v 0.584 * [taylor]: Taking taylor expansion of (sqrt 2) in v 0.584 * [taylor]: Taking taylor expansion of 2 in v 0.584 * [backup-simplify]: Simplify 2 into 2 0.584 * [backup-simplify]: Simplify (sqrt 2) into (sqrt 2) 0.585 * [backup-simplify]: Simplify (/ 0 (* 2 (sqrt 2))) into 0 0.585 * [taylor]: Taking taylor expansion of (sqrt (- 1 (* 3 (/ 1 (pow v 2))))) in v 0.585 * [taylor]: Taking taylor expansion of (- 1 (* 3 (/ 1 (pow v 2)))) in v 0.585 * [taylor]: Taking taylor expansion of 1 in v 0.585 * [backup-simplify]: Simplify 1 into 1 0.585 * [taylor]: Taking taylor expansion of (* 3 (/ 1 (pow v 2))) in v 0.585 * [taylor]: Taking taylor expansion of 3 in v 0.585 * [backup-simplify]: Simplify 3 into 3 0.585 * [taylor]: Taking taylor expansion of (/ 1 (pow v 2)) in v 0.585 * [taylor]: Taking taylor expansion of (pow v 2) in v 0.585 * [taylor]: Taking taylor expansion of v in v 0.585 * [backup-simplify]: Simplify 0 into 0 0.585 * [backup-simplify]: Simplify 1 into 1 0.585 * [backup-simplify]: Simplify (* 1 1) into 1 0.586 * [backup-simplify]: Simplify (/ 1 1) into 1 0.586 * [backup-simplify]: Simplify (* 3 1) into 3 0.586 * [backup-simplify]: Simplify (- 3) into -3 0.586 * [backup-simplify]: Simplify (+ 0 -3) into -3 0.587 * [backup-simplify]: Simplify (sqrt -3) into (sqrt -3) 0.587 * [backup-simplify]: Simplify (+ (* 1 0) (* 0 1)) into 0 0.587 * [backup-simplify]: Simplify (- (+ (* 1 (/ 0 1)))) into 0 0.588 * [backup-simplify]: Simplify (+ (* 3 0) (* 0 1)) into 0 0.588 * [backup-simplify]: Simplify (- 0) into 0 0.588 * [backup-simplify]: Simplify (+ 0 0) into 0 0.589 * [backup-simplify]: Simplify (/ 0 (* 2 (sqrt -3))) into 0 0.590 * [backup-simplify]: Simplify (* (sqrt 2) (sqrt -3)) into (* (sqrt 2) (sqrt -3)) 0.591 * [backup-simplify]: Simplify (* 1/4 (* (sqrt 2) (sqrt -3))) into (* 1/4 (* (sqrt 2) (sqrt -3))) 0.592 * [backup-simplify]: Simplify (* 1/4 (* (sqrt 2) (sqrt -3))) into (* 1/4 (* (sqrt 2) (sqrt -3))) 0.593 * [backup-simplify]: Simplify (+ (* (sqrt 2) 0) (* 0 (sqrt -3))) into 0 0.594 * [backup-simplify]: Simplify (+ (* 1/4 0) (* 0 (* (sqrt 2) (sqrt -3)))) into 0 0.594 * [backup-simplify]: Simplify 0 into 0 0.594 * [backup-simplify]: Simplify (+ (* 1 0) (+ (* 0 0) (* 0 1))) into 0 0.595 * [backup-simplify]: Simplify (- (+ (* 1 (/ 0 1)) (* 0 (/ 0 1)))) into 0 0.595 * [backup-simplify]: Simplify (+ (* 3 0) (+ (* 0 0) (* 0 1))) into 0 0.595 * [backup-simplify]: Simplify (- 0) into 0 0.596 * [backup-simplify]: Simplify (+ 1 0) into 1 0.597 * [backup-simplify]: Simplify (/ (- 1 (pow 0 2) (+)) (* 2 (sqrt -3))) into (/ 1/2 (sqrt -3)) 0.598 * [backup-simplify]: Simplify (/ (- 0 (pow 0 2) (+)) (* 2 (sqrt 2))) into 0 0.600 * [backup-simplify]: Simplify (+ (* (sqrt 2) (/ 1/2 (sqrt -3))) (+ (* 0 0) (* 0 (sqrt -3)))) into (* 1/2 (/ (sqrt 2) (sqrt -3))) 0.604 * [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))) 0.605 * [backup-simplify]: Simplify (* 1/8 (/ (sqrt 2) (sqrt -3))) into (* 1/8 (/ (sqrt 2) (sqrt -3))) 0.606 * [backup-simplify]: Simplify (+ (* 1 0) (+ (* 0 0) (+ (* 0 0) (* 0 1)))) into 0 0.607 * [backup-simplify]: Simplify (- (+ (* 1 (/ 0 1)) (* 0 (/ 0 1)) (* 0 (/ 0 1)))) into 0 0.607 * [backup-simplify]: Simplify (+ (* 3 0) (+ (* 0 0) (+ (* 0 0) (* 0 1)))) into 0 0.607 * [backup-simplify]: Simplify (- 0) into 0 0.608 * [backup-simplify]: Simplify (+ 0 0) into 0 0.609 * [backup-simplify]: Simplify (/ (- 0 (+ (* 2 (* 0 (/ 1/2 (sqrt -3)))))) (* 2 (sqrt -3))) into 0 0.609 * [backup-simplify]: Simplify (/ (- 0 (+ (* 2 (* 0 0)))) (* 2 (sqrt 2))) into 0 0.610 * [backup-simplify]: Simplify (+ (* (sqrt 2) 0) (+ (* 0 (/ 1/2 (sqrt -3))) (+ (* 0 0) (* 0 (sqrt -3))))) into 0 0.612 * [backup-simplify]: Simplify (+ (* 1/4 0) (+ (* 0 (* 1/2 (/ (sqrt 2) (sqrt -3)))) (+ (* 0 0) (* 0 (* (sqrt 2) (sqrt -3)))))) into 0 0.612 * [backup-simplify]: Simplify 0 into 0 0.612 * [backup-simplify]: Simplify (+ (* 1 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (* 0 1))))) into 0 0.613 * [backup-simplify]: Simplify (- (+ (* 1 (/ 0 1)) (* 0 (/ 0 1)) (* 0 (/ 0 1)) (* 0 (/ 0 1)))) into 0 0.614 * [backup-simplify]: Simplify (+ (* 3 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (* 0 1))))) into 0 0.614 * [backup-simplify]: Simplify (- 0) into 0 0.615 * [backup-simplify]: Simplify (+ 0 0) into 0 0.622 * [backup-simplify]: Simplify (/ (- 0 (pow (/ 1/2 (sqrt -3)) 2) (+ (* 2 (* 0 0)))) (* 2 (sqrt -3))) into (/ -1/8 (pow (sqrt -3) 3)) 0.623 * [backup-simplify]: Simplify (/ (- 0 (pow 0 2) (+ (* 2 (* 0 0)))) (* 2 (sqrt 2))) into 0 0.631 * [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)))) 0.642 * [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)))) 0.645 * [backup-simplify]: Simplify (- (* 1/32 (/ (sqrt 2) (pow (sqrt -3) 3)))) into (- (* 1/32 (/ (sqrt 2) (pow (sqrt -3) 3)))) 0.651 * [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))))) 0.653 * [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))))))) 0.653 * [approximate]: Taking taylor expansion of (* 1/4 (* (sqrt 2) (sqrt (- 1 (* 3 (/ 1 (pow v 2))))))) in (v) around 0 0.653 * [taylor]: Taking taylor expansion of (* 1/4 (* (sqrt 2) (sqrt (- 1 (* 3 (/ 1 (pow v 2))))))) in v 0.653 * [taylor]: Taking taylor expansion of 1/4 in v 0.653 * [backup-simplify]: Simplify 1/4 into 1/4 0.653 * [taylor]: Taking taylor expansion of (* (sqrt 2) (sqrt (- 1 (* 3 (/ 1 (pow v 2)))))) in v 0.653 * [taylor]: Taking taylor expansion of (sqrt 2) in v 0.653 * [taylor]: Taking taylor expansion of 2 in v 0.653 * [backup-simplify]: Simplify 2 into 2 0.653 * [backup-simplify]: Simplify (sqrt 2) into (sqrt 2) 0.654 * [backup-simplify]: Simplify (/ 0 (* 2 (sqrt 2))) into 0 0.654 * [taylor]: Taking taylor expansion of (sqrt (- 1 (* 3 (/ 1 (pow v 2))))) in v 0.654 * [taylor]: Taking taylor expansion of (- 1 (* 3 (/ 1 (pow v 2)))) in v 0.654 * [taylor]: Taking taylor expansion of 1 in v 0.654 * [backup-simplify]: Simplify 1 into 1 0.654 * [taylor]: Taking taylor expansion of (* 3 (/ 1 (pow v 2))) in v 0.654 * [taylor]: Taking taylor expansion of 3 in v 0.654 * [backup-simplify]: Simplify 3 into 3 0.654 * [taylor]: Taking taylor expansion of (/ 1 (pow v 2)) in v 0.654 * [taylor]: Taking taylor expansion of (pow v 2) in v 0.654 * [taylor]: Taking taylor expansion of v in v 0.654 * [backup-simplify]: Simplify 0 into 0 0.654 * [backup-simplify]: Simplify 1 into 1 0.654 * [backup-simplify]: Simplify (* 1 1) into 1 0.654 * [backup-simplify]: Simplify (/ 1 1) into 1 0.655 * [backup-simplify]: Simplify (* 3 1) into 3 0.655 * [backup-simplify]: Simplify (- 3) into -3 0.655 * [backup-simplify]: Simplify (+ 0 -3) into -3 0.655 * [backup-simplify]: Simplify (sqrt -3) into (sqrt -3) 0.656 * [backup-simplify]: Simplify (+ (* 1 0) (* 0 1)) into 0 0.656 * [backup-simplify]: Simplify (- (+ (* 1 (/ 0 1)))) into 0 0.657 * [backup-simplify]: Simplify (+ (* 3 0) (* 0 1)) into 0 0.657 * [backup-simplify]: Simplify (- 0) into 0 0.657 * [backup-simplify]: Simplify (+ 0 0) into 0 0.657 * [backup-simplify]: Simplify (/ 0 (* 2 (sqrt -3))) into 0 0.657 * [taylor]: Taking taylor expansion of (* 1/4 (* (sqrt 2) (sqrt (- 1 (* 3 (/ 1 (pow v 2))))))) in v 0.657 * [taylor]: Taking taylor expansion of 1/4 in v 0.657 * [backup-simplify]: Simplify 1/4 into 1/4 0.658 * [taylor]: Taking taylor expansion of (* (sqrt 2) (sqrt (- 1 (* 3 (/ 1 (pow v 2)))))) in v 0.658 * [taylor]: Taking taylor expansion of (sqrt 2) in v 0.658 * [taylor]: Taking taylor expansion of 2 in v 0.658 * [backup-simplify]: Simplify 2 into 2 0.658 * [backup-simplify]: Simplify (sqrt 2) into (sqrt 2) 0.658 * [backup-simplify]: Simplify (/ 0 (* 2 (sqrt 2))) into 0 0.658 * [taylor]: Taking taylor expansion of (sqrt (- 1 (* 3 (/ 1 (pow v 2))))) in v 0.658 * [taylor]: Taking taylor expansion of (- 1 (* 3 (/ 1 (pow v 2)))) in v 0.658 * [taylor]: Taking taylor expansion of 1 in v 0.658 * [backup-simplify]: Simplify 1 into 1 0.658 * [taylor]: Taking taylor expansion of (* 3 (/ 1 (pow v 2))) in v 0.658 * [taylor]: Taking taylor expansion of 3 in v 0.658 * [backup-simplify]: Simplify 3 into 3 0.658 * [taylor]: Taking taylor expansion of (/ 1 (pow v 2)) in v 0.658 * [taylor]: Taking taylor expansion of (pow v 2) in v 0.658 * [taylor]: Taking taylor expansion of v in v 0.658 * [backup-simplify]: Simplify 0 into 0 0.658 * [backup-simplify]: Simplify 1 into 1 0.659 * [backup-simplify]: Simplify (* 1 1) into 1 0.659 * [backup-simplify]: Simplify (/ 1 1) into 1 0.659 * [backup-simplify]: Simplify (* 3 1) into 3 0.659 * [backup-simplify]: Simplify (- 3) into -3 0.660 * [backup-simplify]: Simplify (+ 0 -3) into -3 0.660 * [backup-simplify]: Simplify (sqrt -3) into (sqrt -3) 0.660 * [backup-simplify]: Simplify (+ (* 1 0) (* 0 1)) into 0 0.661 * [backup-simplify]: Simplify (- (+ (* 1 (/ 0 1)))) into 0 0.661 * [backup-simplify]: Simplify (+ (* 3 0) (* 0 1)) into 0 0.661 * [backup-simplify]: Simplify (- 0) into 0 0.662 * [backup-simplify]: Simplify (+ 0 0) into 0 0.662 * [backup-simplify]: Simplify (/ 0 (* 2 (sqrt -3))) into 0 0.663 * [backup-simplify]: Simplify (* (sqrt 2) (sqrt -3)) into (* (sqrt 2) (sqrt -3)) 0.664 * [backup-simplify]: Simplify (* 1/4 (* (sqrt 2) (sqrt -3))) into (* 1/4 (* (sqrt 2) (sqrt -3))) 0.666 * [backup-simplify]: Simplify (* 1/4 (* (sqrt 2) (sqrt -3))) into (* 1/4 (* (sqrt 2) (sqrt -3))) 0.666 * [backup-simplify]: Simplify (+ (* (sqrt 2) 0) (* 0 (sqrt -3))) into 0 0.667 * [backup-simplify]: Simplify (+ (* 1/4 0) (* 0 (* (sqrt 2) (sqrt -3)))) into 0 0.667 * [backup-simplify]: Simplify 0 into 0 0.668 * [backup-simplify]: Simplify (+ (* 1 0) (+ (* 0 0) (* 0 1))) into 0 0.668 * [backup-simplify]: Simplify (- (+ (* 1 (/ 0 1)) (* 0 (/ 0 1)))) into 0 0.669 * [backup-simplify]: Simplify (+ (* 3 0) (+ (* 0 0) (* 0 1))) into 0 0.669 * [backup-simplify]: Simplify (- 0) into 0 0.670 * [backup-simplify]: Simplify (+ 1 0) into 1 0.673 * [backup-simplify]: Simplify (/ (- 1 (pow 0 2) (+)) (* 2 (sqrt -3))) into (/ 1/2 (sqrt -3)) 0.674 * [backup-simplify]: Simplify (/ (- 0 (pow 0 2) (+)) (* 2 (sqrt 2))) into 0 0.679 * [backup-simplify]: Simplify (+ (* (sqrt 2) (/ 1/2 (sqrt -3))) (+ (* 0 0) (* 0 (sqrt -3)))) into (* 1/2 (/ (sqrt 2) (sqrt -3))) 0.685 * [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))) 0.687 * [backup-simplify]: Simplify (* 1/8 (/ (sqrt 2) (sqrt -3))) into (* 1/8 (/ (sqrt 2) (sqrt -3))) 0.688 * [backup-simplify]: Simplify (+ (* 1 0) (+ (* 0 0) (+ (* 0 0) (* 0 1)))) into 0 0.689 * [backup-simplify]: Simplify (- (+ (* 1 (/ 0 1)) (* 0 (/ 0 1)) (* 0 (/ 0 1)))) into 0 0.691 * [backup-simplify]: Simplify (+ (* 3 0) (+ (* 0 0) (+ (* 0 0) (* 0 1)))) into 0 0.691 * [backup-simplify]: Simplify (- 0) into 0 0.691 * [backup-simplify]: Simplify (+ 0 0) into 0 0.693 * [backup-simplify]: Simplify (/ (- 0 (+ (* 2 (* 0 (/ 1/2 (sqrt -3)))))) (* 2 (sqrt -3))) into 0 0.694 * [backup-simplify]: Simplify (/ (- 0 (+ (* 2 (* 0 0)))) (* 2 (sqrt 2))) into 0 0.696 * [backup-simplify]: Simplify (+ (* (sqrt 2) 0) (+ (* 0 (/ 1/2 (sqrt -3))) (+ (* 0 0) (* 0 (sqrt -3))))) into 0 0.699 * [backup-simplify]: Simplify (+ (* 1/4 0) (+ (* 0 (* 1/2 (/ (sqrt 2) (sqrt -3)))) (+ (* 0 0) (* 0 (* (sqrt 2) (sqrt -3)))))) into 0 0.699 * [backup-simplify]: Simplify 0 into 0 0.700 * [backup-simplify]: Simplify (+ (* 1 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (* 0 1))))) into 0 0.701 * [backup-simplify]: Simplify (- (+ (* 1 (/ 0 1)) (* 0 (/ 0 1)) (* 0 (/ 0 1)) (* 0 (/ 0 1)))) into 0 0.702 * [backup-simplify]: Simplify (+ (* 3 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (* 0 1))))) into 0 0.703 * [backup-simplify]: Simplify (- 0) into 0 0.703 * [backup-simplify]: Simplify (+ 0 0) into 0 0.710 * [backup-simplify]: Simplify (/ (- 0 (pow (/ 1/2 (sqrt -3)) 2) (+ (* 2 (* 0 0)))) (* 2 (sqrt -3))) into (/ -1/8 (pow (sqrt -3) 3)) 0.711 * [backup-simplify]: Simplify (/ (- 0 (pow 0 2) (+ (* 2 (* 0 0)))) (* 2 (sqrt 2))) into 0 0.719 * [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)))) 0.732 * [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)))) 0.736 * [backup-simplify]: Simplify (- (* 1/32 (/ (sqrt 2) (pow (sqrt -3) 3)))) into (- (* 1/32 (/ (sqrt 2) (pow (sqrt -3) 3)))) 0.745 * [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)))))) 0.745 * * * [progress]: simplifying candidates 0.745 * * * * [progress]: [ 1 / 98 ] simplifiying candidate # 0.746 * [simplify]: Simplifying (* 3 (* v v)) 0.746 * * [simplify]: iters left: 4 (4 enodes) 0.748 * * [simplify]: iters left: 3 (15 enodes) 0.753 * * [simplify]: iters left: 2 (19 enodes) 0.758 * * [simplify]: Extracting #0: cost 1 inf + 0 0.758 * * [simplify]: Extracting #1: cost 6 inf + 0 0.758 * * [simplify]: Extracting #2: cost 5 inf + 43 0.758 * * [simplify]: Extracting #3: cost 0 inf + 332 0.759 * [simplify]: Simplified to (* 3 (* v v)) 0.759 * [simplify]: Simplified (2 1 2 1 2 1) to (λ (v) (* (* (/ (sqrt 2) 4) (sqrt (- 1 (pow (* 3 (* v v)) 1)))) (- 1 (* v v)))) 0.759 * * * * [progress]: [ 2 / 98 ] simplifiying candidate # 0.759 * [simplify]: Simplifying (* 3 (* v v)) 0.759 * * [simplify]: iters left: 4 (4 enodes) 0.762 * * [simplify]: iters left: 3 (15 enodes) 0.766 * * [simplify]: iters left: 2 (19 enodes) 0.771 * * [simplify]: Extracting #0: cost 1 inf + 0 0.771 * * [simplify]: Extracting #1: cost 6 inf + 0 0.771 * * [simplify]: Extracting #2: cost 5 inf + 43 0.772 * * [simplify]: Extracting #3: cost 0 inf + 332 0.772 * [simplify]: Simplified to (* 3 (* v v)) 0.772 * [simplify]: Simplified (2 1 2 1 2 1) to (λ (v) (* (* (/ (sqrt 2) 4) (sqrt (- 1 (pow (* 3 (* v v)) 1)))) (- 1 (* v v)))) 0.772 * * * * [progress]: [ 3 / 98 ] simplifiying candidate # 0.772 * * * * [progress]: [ 4 / 98 ] simplifiying candidate # 0.772 * [simplify]: Simplifying (+ (log 3) (+ (log v) (log v))) 0.772 * * [simplify]: iters left: 5 (6 enodes) 0.775 * * [simplify]: iters left: 4 (21 enodes) 0.782 * * [simplify]: iters left: 3 (25 enodes) 0.791 * * [simplify]: Extracting #0: cost 1 inf + 0 0.791 * * [simplify]: Extracting #1: cost 6 inf + 0 0.791 * * [simplify]: Extracting #2: cost 12 inf + 0 0.791 * * [simplify]: Extracting #3: cost 10 inf + 2 0.792 * * [simplify]: Extracting #4: cost 0 inf + 1316 0.792 * [simplify]: Simplified to (+ (log 3) (+ (log v) (log v))) 0.792 * [simplify]: Simplified (2 1 2 1 2 1) to (λ (v) (* (* (/ (sqrt 2) 4) (sqrt (- 1 (exp (+ (log 3) (+ (log v) (log v))))))) (- 1 (* v v)))) 0.792 * * * * [progress]: [ 5 / 98 ] simplifiying candidate # 0.793 * [simplify]: Simplifying (+ (log 3) (log (* v v))) 0.793 * * [simplify]: iters left: 5 (6 enodes) 0.796 * * [simplify]: iters left: 4 (21 enodes) 0.804 * * [simplify]: iters left: 3 (27 enodes) 0.813 * * [simplify]: iters left: 2 (32 enodes) 0.822 * * [simplify]: Extracting #0: cost 1 inf + 0 0.822 * * [simplify]: Extracting #1: cost 6 inf + 0 0.822 * * [simplify]: Extracting #2: cost 13 inf + 0 0.822 * * [simplify]: Extracting #3: cost 9 inf + 185 0.822 * * [simplify]: Extracting #4: cost 4 inf + 741 0.823 * * [simplify]: Extracting #5: cost 0 inf + 1398 0.823 * [simplify]: Simplified to (+ (log 3) (+ (log v) (log v))) 0.823 * [simplify]: Simplified (2 1 2 1 2 1) to (λ (v) (* (* (/ (sqrt 2) 4) (sqrt (- 1 (exp (+ (log 3) (+ (log v) (log v))))))) (- 1 (* v v)))) 0.823 * * * * [progress]: [ 6 / 98 ] simplifiying candidate # 0.823 * * * * [progress]: [ 7 / 98 ] simplifiying candidate # 0.823 * * * * [progress]: [ 8 / 98 ] simplifiying candidate # 0.824 * [simplify]: Simplifying (* (* (* 3 3) 3) (* (* (* v v) v) (* (* v v) v))) 0.824 * * [simplify]: iters left: 6 (8 enodes) 0.829 * * [simplify]: iters left: 5 (38 enodes) 0.842 * * [simplify]: iters left: 4 (96 enodes) 0.865 * * [simplify]: iters left: 3 (265 enodes) 1.048 * * [simplify]: Extracting #0: cost 1 inf + 0 1.048 * * [simplify]: Extracting #1: cost 54 inf + 0 1.050 * * [simplify]: Extracting #2: cost 83 inf + 1839 1.054 * * [simplify]: Extracting #3: cost 30 inf + 7514 1.057 * * [simplify]: Extracting #4: cost 8 inf + 12317 1.061 * * [simplify]: Extracting #5: cost 0 inf + 14739 1.065 * [simplify]: Simplified to (* 27 (* (* v (* v v)) (* v (* v v)))) 1.065 * [simplify]: Simplified (2 1 2 1 2 1) to (λ (v) (* (* (/ (sqrt 2) 4) (sqrt (- 1 (cbrt (* 27 (* (* v (* v v)) (* v (* v v)))))))) (- 1 (* v v)))) 1.065 * * * * [progress]: [ 9 / 98 ] simplifiying candidate # 1.065 * [simplify]: Simplifying (* (* (* 3 3) 3) (* (* (* v v) (* v v)) (* v v))) 1.065 * * [simplify]: iters left: 6 (8 enodes) 1.068 * * [simplify]: iters left: 5 (39 enodes) 1.079 * * [simplify]: iters left: 4 (96 enodes) 1.117 * * [simplify]: iters left: 3 (269 enodes) 1.287 * * [simplify]: Extracting #0: cost 1 inf + 0 1.287 * * [simplify]: Extracting #1: cost 72 inf + 0 1.287 * * [simplify]: Extracting #2: cost 120 inf + 818 1.290 * * [simplify]: Extracting #3: cost 39 inf + 12504 1.294 * * [simplify]: Extracting #4: cost 1 inf + 19795 1.298 * * [simplify]: Extracting #5: cost 0 inf + 20047 1.302 * [simplify]: Simplified to (* (* v v) (* (* (* v v) (* v v)) 27)) 1.303 * [simplify]: Simplified (2 1 2 1 2 1) to (λ (v) (* (* (/ (sqrt 2) 4) (sqrt (- 1 (cbrt (* (* v v) (* (* (* v v) (* v v)) 27)))))) (- 1 (* v v)))) 1.303 * * * * [progress]: [ 10 / 98 ] simplifiying candidate # 1.303 * * * * [progress]: [ 11 / 98 ] simplifiying candidate # 1.303 * * * * [progress]: [ 12 / 98 ] simplifiying candidate # 1.303 * * * * [progress]: [ 13 / 98 ] simplifiying candidate # 1.303 * * * * [progress]: [ 14 / 98 ] simplifiying candidate # 1.304 * [simplify]: Simplifying (* (sqrt 3) v) 1.304 * * [simplify]: iters left: 3 (4 enodes) 1.305 * * [simplify]: iters left: 2 (13 enodes) 1.310 * * [simplify]: Extracting #0: cost 1 inf + 0 1.310 * * [simplify]: Extracting #1: cost 4 inf + 0 1.310 * * [simplify]: Extracting #2: cost 5 inf + 1 1.310 * * [simplify]: Extracting #3: cost 4 inf + 2 1.310 * * [simplify]: Extracting #4: cost 0 inf + 248 1.310 * [simplify]: Simplified to (* v (sqrt 3)) 1.310 * [simplify]: Simplified (2 1 2 1 2 1) to (λ (v) (* (* (/ (sqrt 2) 4) (sqrt (- 1 (* (* v (sqrt 3)) (* (sqrt 3) v))))) (- 1 (* v v)))) 1.310 * [simplify]: Simplifying (* (sqrt 3) v) 1.310 * * [simplify]: iters left: 3 (4 enodes) 1.313 * * [simplify]: iters left: 2 (13 enodes) 1.317 * * [simplify]: Extracting #0: cost 1 inf + 0 1.317 * * [simplify]: Extracting #1: cost 4 inf + 0 1.317 * * [simplify]: Extracting #2: cost 5 inf + 1 1.317 * * [simplify]: Extracting #3: cost 4 inf + 2 1.318 * * [simplify]: Extracting #4: cost 0 inf + 248 1.318 * [simplify]: Simplified to (* v (sqrt 3)) 1.318 * [simplify]: Simplified (2 1 2 1 2 2) to (λ (v) (* (* (/ (sqrt 2) 4) (sqrt (- 1 (* (* (sqrt 3) v) (* v (sqrt 3)))))) (- 1 (* v v)))) 1.318 * * * * [progress]: [ 15 / 98 ] simplifiying candidate # 1.318 * * * * [progress]: [ 16 / 98 ] simplifiying candidate # 1.318 * [simplify]: Simplifying (* (cbrt 3) (cbrt 3)) 1.318 * * [simplify]: iters left: 3 (3 enodes) 1.320 * * [simplify]: iters left: 2 (9 enodes) 1.323 * * [simplify]: Extracting #0: cost 1 inf + 0 1.323 * * [simplify]: Extracting #1: cost 3 inf + 0 1.323 * * [simplify]: Extracting #2: cost 5 inf + 0 1.323 * * [simplify]: Extracting #3: cost 4 inf + 1 1.323 * * [simplify]: Extracting #4: cost 0 inf + 405 1.323 * [simplify]: Simplified to (* (cbrt 3) (cbrt 3)) 1.323 * [simplify]: Simplified (2 1 2 1 2 1) to (λ (v) (* (* (/ (sqrt 2) 4) (sqrt (- 1 (* (* (cbrt 3) (cbrt 3)) (* (cbrt 3) (* v v)))))) (- 1 (* v v)))) 1.323 * * * * [progress]: [ 17 / 98 ] simplifiying candidate # 1.323 * [simplify]: Simplifying (sqrt 3) 1.323 * * [simplify]: iters left: 1 (2 enodes) 1.324 * * [simplify]: Extracting #0: cost 1 inf + 0 1.324 * * [simplify]: Extracting #1: cost 3 inf + 0 1.324 * * [simplify]: Extracting #2: cost 2 inf + 1 1.324 * * [simplify]: Extracting #3: cost 0 inf + 83 1.325 * [simplify]: Simplified to (sqrt 3) 1.325 * [simplify]: Simplified (2 1 2 1 2 1) to (λ (v) (* (* (/ (sqrt 2) 4) (sqrt (- 1 (* (sqrt 3) (* (sqrt 3) (* v v)))))) (- 1 (* v v)))) 1.325 * * * * [progress]: [ 18 / 98 ] simplifiying candidate # 1.325 * * * * [progress]: [ 19 / 98 ] simplifiying candidate #real (real->posit16 (* 3 (* v v))))))) (- 1 (* v v))))> 1.325 * * * * [progress]: [ 20 / 98 ] simplifiying candidate # 1.325 * * * * [progress]: [ 21 / 98 ] simplifiying candidate # 1.325 * * * * [progress]: [ 22 / 98 ] simplifiying candidate # 1.325 * * * * [progress]: [ 23 / 98 ] simplifiying candidate # 1.325 * * * * [progress]: [ 24 / 98 ] simplifiying candidate # 1.325 * * * * [progress]: [ 25 / 98 ] simplifiying candidate # 1.325 * * * * [progress]: [ 26 / 98 ] simplifiying candidate # 1.325 * * * * [progress]: [ 27 / 98 ] simplifiying candidate # 1.325 * [simplify]: Simplifying (sqrt (* (cbrt (- 1 (* 3 (* v v)))) (cbrt (- 1 (* 3 (* v v)))))) 1.325 * * [simplify]: iters left: 6 (9 enodes) 1.328 * * [simplify]: iters left: 5 (35 enodes) 1.334 * * [simplify]: iters left: 4 (55 enodes) 1.343 * * [simplify]: iters left: 3 (73 enodes) 1.359 * * [simplify]: Extracting #0: cost 1 inf + 0 1.359 * * [simplify]: Extracting #1: cost 4 inf + 0 1.359 * * [simplify]: Extracting #2: cost 7 inf + 0 1.359 * * [simplify]: Extracting #3: cost 11 inf + 0 1.360 * * [simplify]: Extracting #4: cost 20 inf + 1 1.360 * * [simplify]: Extracting #5: cost 19 inf + 128 1.363 * * [simplify]: Extracting #6: cost 9 inf + 867 1.364 * * [simplify]: Extracting #7: cost 1 inf + 2207 1.365 * * [simplify]: Extracting #8: cost 0 inf + 2450 1.366 * [simplify]: Simplified to (fabs (cbrt (- 1 (* (* v v) 3)))) 1.367 * [simplify]: Simplified (2 1 2 1) to (λ (v) (* (* (/ (sqrt 2) 4) (* (fabs (cbrt (- 1 (* (* v v) 3)))) (sqrt (cbrt (- 1 (* 3 (* v v))))))) (- 1 (* v v)))) 1.367 * * * * [progress]: [ 28 / 98 ] simplifiying candidate # 1.367 * [simplify]: Simplifying (sqrt (sqrt (- 1 (* 3 (* v v))))) 1.367 * * [simplify]: iters left: 6 (8 enodes) 1.371 * * [simplify]: iters left: 5 (31 enodes) 1.377 * * [simplify]: iters left: 4 (51 enodes) 1.386 * * [simplify]: iters left: 3 (69 enodes) 1.397 * * [simplify]: Extracting #0: cost 1 inf + 0 1.397 * * [simplify]: Extracting #1: cost 3 inf + 0 1.397 * * [simplify]: Extracting #2: cost 5 inf + 0 1.397 * * [simplify]: Extracting #3: cost 9 inf + 0 1.397 * * [simplify]: Extracting #4: cost 18 inf + 1 1.397 * * [simplify]: Extracting #5: cost 17 inf + 128 1.397 * * [simplify]: Extracting #6: cost 6 inf + 868 1.398 * * [simplify]: Extracting #7: cost 0 inf + 1804 1.398 * [simplify]: Simplified to (sqrt (sqrt (- 1 (* (* v v) 3)))) 1.398 * [simplify]: Simplified (2 1 2 1) to (λ (v) (* (* (/ (sqrt 2) 4) (* (sqrt (sqrt (- 1 (* (* v v) 3)))) (sqrt (sqrt (- 1 (* 3 (* v v))))))) (- 1 (* v v)))) 1.398 * * * * [progress]: [ 29 / 98 ] simplifiying candidate # 1.398 * [simplify]: Simplifying (sqrt 1) 1.398 * * [simplify]: iters left: 1 (2 enodes) 1.400 * * [simplify]: Extracting #0: cost 1 inf + 0 1.400 * * [simplify]: Extracting #1: cost 0 inf + 1 1.400 * [simplify]: Simplified to 1 1.400 * [simplify]: Simplified (2 1 2 1) to (λ (v) (* (* (/ (sqrt 2) 4) (* 1 (sqrt (- 1 (* 3 (* v v)))))) (- 1 (* v v)))) 1.400 * * * * [progress]: [ 30 / 98 ] simplifiying candidate # 1.401 * [simplify]: Simplifying (sqrt (- (pow 1 3) (pow (* 3 (* v v)) 3))) 1.401 * * [simplify]: iters left: 6 (9 enodes) 1.407 * * [simplify]: iters left: 5 (46 enodes) 1.419 * * [simplify]: iters left: 4 (125 enodes) 1.472 * * [simplify]: iters left: 3 (400 enodes) 1.699 * * [simplify]: Extracting #0: cost 1 inf + 0 1.700 * * [simplify]: Extracting #1: cost 3 inf + 0 1.700 * * [simplify]: Extracting #2: cost 7 inf + 0 1.700 * * [simplify]: Extracting #3: cost 75 inf + 1 1.702 * * [simplify]: Extracting #4: cost 154 inf + 1794 1.710 * * [simplify]: Extracting #5: cost 73 inf + 13635 1.724 * * [simplify]: Extracting #6: cost 18 inf + 24926 1.742 * * [simplify]: Extracting #7: cost 5 inf + 31364 1.757 * * [simplify]: Extracting #8: cost 0 inf + 33782 1.773 * [simplify]: Simplified to (sqrt (- 1 (* (* (* v v) (* (* v v) 27)) (* v v)))) 1.773 * [simplify]: Simplified (2 1 2 1) to (λ (v) (* (* (/ (sqrt 2) 4) (/ (sqrt (- 1 (* (* (* v v) (* (* v v) 27)) (* v v)))) (sqrt (+ (* 1 1) (+ (* (* 3 (* v v)) (* 3 (* v v))) (* 1 (* 3 (* v v)))))))) (- 1 (* v v)))) 1.773 * * * * [progress]: [ 31 / 98 ] simplifiying candidate # 1.774 * [simplify]: Simplifying (sqrt (- (* 1 1) (* (* 3 (* v v)) (* 3 (* v v))))) 1.774 * * [simplify]: iters left: 6 (9 enodes) 1.780 * * [simplify]: iters left: 5 (40 enodes) 1.796 * * [simplify]: iters left: 4 (93 enodes) 1.836 * * [simplify]: iters left: 3 (204 enodes) 1.944 * * [simplify]: iters left: 2 (341 enodes) 2.094 * * [simplify]: iters left: 1 (395 enodes) 2.229 * * [simplify]: Extracting #0: cost 1 inf + 0 2.230 * * [simplify]: Extracting #1: cost 3 inf + 0 2.230 * * [simplify]: Extracting #2: cost 7 inf + 0 2.230 * * [simplify]: Extracting #3: cost 55 inf + 1 2.231 * * [simplify]: Extracting #4: cost 96 inf + 2081 2.235 * * [simplify]: Extracting #5: cost 73 inf + 4450 2.240 * * [simplify]: Extracting #6: cost 43 inf + 11008 2.247 * * [simplify]: Extracting #7: cost 5 inf + 21669 2.255 * * [simplify]: Extracting #8: cost 0 inf + 23895 2.262 * [simplify]: Simplified to (sqrt (- 1 (* 9 (* (* v v) (* v v))))) 2.262 * [simplify]: Simplified (2 1 2 1) to (λ (v) (* (* (/ (sqrt 2) 4) (/ (sqrt (- 1 (* 9 (* (* v v) (* v v))))) (sqrt (+ 1 (* 3 (* v v)))))) (- 1 (* v v)))) 2.262 * * * * [progress]: [ 32 / 98 ] simplifiying candidate # 2.263 * [simplify]: Simplifying (- 1 (* 3 (* v v))) 2.263 * * [simplify]: iters left: 6 (6 enodes) 2.267 * * [simplify]: iters left: 5 (25 enodes) 2.276 * * [simplify]: iters left: 4 (45 enodes) 2.291 * * [simplify]: iters left: 3 (63 enodes) 2.310 * * [simplify]: Extracting #0: cost 1 inf + 0 2.310 * * [simplify]: Extracting #1: cost 5 inf + 0 2.310 * * [simplify]: Extracting #2: cost 14 inf + 1 2.310 * * [simplify]: Extracting #3: cost 13 inf + 128 2.310 * * [simplify]: Extracting #4: cost 2 inf + 868 2.311 * * [simplify]: Extracting #5: cost 0 inf + 1072 2.312 * [simplify]: Simplified to (+ 1 (* (* v v) -3)) 2.312 * [simplify]: Simplified (2 1 2 1) to (λ (v) (* (* (/ (sqrt 2) 4) (pow (+ 1 (* (* v v) -3)) (/ 1 2))) (- 1 (* v v)))) 2.312 * * * * [progress]: [ 33 / 98 ] simplifiying candidate # 2.312 * * * * [progress]: [ 34 / 98 ] simplifiying candidate # 2.312 * [simplify]: Simplifying (sqrt (- 1 (* 3 (* v v)))) 2.312 * * [simplify]: iters left: 6 (7 enodes) 2.317 * * [simplify]: iters left: 5 (28 enodes) 2.327 * * [simplify]: iters left: 4 (48 enodes) 2.346 * * [simplify]: iters left: 3 (66 enodes) 2.358 * * [simplify]: Extracting #0: cost 1 inf + 0 2.358 * * [simplify]: Extracting #1: cost 3 inf + 0 2.358 * * [simplify]: Extracting #2: cost 7 inf + 0 2.359 * * [simplify]: Extracting #3: cost 16 inf + 1 2.359 * * [simplify]: Extracting #4: cost 13 inf + 331 2.359 * * [simplify]: Extracting #5: cost 4 inf + 907 2.359 * * [simplify]: Extracting #6: cost 0 inf + 1398 2.360 * [simplify]: Simplified to (sqrt (- 1 (* (* v v) 3))) 2.360 * [simplify]: Simplified (2 1 2 1) to (λ (v) (* (* (/ (sqrt 2) 4) (fabs (sqrt (- 1 (* (* v v) 3))))) (- 1 (* v v)))) 2.360 * * * * [progress]: [ 35 / 98 ] simplifiying candidate # 2.360 * * * * [progress]: [ 36 / 98 ] simplifiying candidate #real (real->posit16 (sqrt (- 1 (* 3 (* v v))))))) (- 1 (* v v))))> 2.360 * * * * [progress]: [ 37 / 98 ] simplifiying candidate # 2.360 * [simplify]: Simplifying (* (/ (sqrt 2) 4) (sqrt (- 1 (* 3 (* v v))))) 2.360 * * [simplify]: iters left: 6 (12 enodes) 2.364 * * [simplify]: iters left: 5 (46 enodes) 2.373 * * [simplify]: iters left: 4 (72 enodes) 2.393 * * [simplify]: iters left: 3 (92 enodes) 2.420 * * [simplify]: Extracting #0: cost 1 inf + 0 2.420 * * [simplify]: Extracting #1: cost 8 inf + 0 2.420 * * [simplify]: Extracting #2: cost 14 inf + 1 2.420 * * [simplify]: Extracting #3: cost 17 inf + 2 2.420 * * [simplify]: Extracting #4: cost 22 inf + 249 2.421 * * [simplify]: Extracting #5: cost 20 inf + 457 2.421 * * [simplify]: Extracting #6: cost 11 inf + 992 2.422 * * [simplify]: Extracting #7: cost 9 inf + 1197 2.423 * * [simplify]: Extracting #8: cost 2 inf + 2583 2.424 * * [simplify]: Extracting #9: cost 0 inf + 3112 2.425 * [simplify]: Simplified to (* (sqrt (+ 1 (* (* v v) -3))) (/ (sqrt 2) 4)) 2.425 * [simplify]: Simplified (2 1 1) to (λ (v) (* (pow (* (sqrt (+ 1 (* (* v v) -3))) (/ (sqrt 2) 4)) 1) (- 1 (* v v)))) 2.426 * * * * [progress]: [ 38 / 98 ] simplifiying candidate # 2.426 * * * * [progress]: [ 39 / 98 ] simplifiying candidate # 2.426 * [simplify]: Simplifying (+ (- (log (sqrt 2)) (log 4)) (log (sqrt (- 1 (* 3 (* v v)))))) 2.426 * * [simplify]: iters left: 6 (15 enodes) 2.435 * * [simplify]: iters left: 5 (57 enodes) 2.455 * * [simplify]: iters left: 4 (91 enodes) 2.488 * * [simplify]: iters left: 3 (128 enodes) 2.514 * * [simplify]: iters left: 2 (135 enodes) 2.535 * * [simplify]: iters left: 1 (139 enodes) 2.572 * * [simplify]: Extracting #0: cost 1 inf + 0 2.572 * * [simplify]: Extracting #1: cost 15 inf + 0 2.572 * * [simplify]: Extracting #2: cost 30 inf + 0 2.572 * * [simplify]: Extracting #3: cost 30 inf + 294 2.573 * * [simplify]: Extracting #4: cost 30 inf + 448 2.573 * * [simplify]: Extracting #5: cost 33 inf + 1528 2.574 * * [simplify]: Extracting #6: cost 31 inf + 2058 2.574 * * [simplify]: Extracting #7: cost 8 inf + 6047 2.576 * * [simplify]: Extracting #8: cost 0 inf + 8827 2.578 * [simplify]: Simplified to (+ (log (sqrt (- 1 (* (* v v) 3)))) (- (log (sqrt 2)) (log 4))) 2.578 * [simplify]: Simplified (2 1 1) to (λ (v) (* (exp (+ (log (sqrt (- 1 (* (* v v) 3)))) (- (log (sqrt 2)) (log 4)))) (- 1 (* v v)))) 2.578 * * * * [progress]: [ 40 / 98 ] simplifiying candidate # 2.578 * [simplify]: Simplifying (+ (log (/ (sqrt 2) 4)) (log (sqrt (- 1 (* 3 (* v v)))))) 2.578 * * [simplify]: iters left: 6 (14 enodes) 2.585 * * [simplify]: iters left: 5 (53 enodes) 2.595 * * [simplify]: iters left: 4 (83 enodes) 2.612 * * [simplify]: iters left: 3 (116 enodes) 2.647 * * [simplify]: iters left: 2 (132 enodes) 2.683 * * [simplify]: iters left: 1 (135 enodes) 2.709 * * [simplify]: Extracting #0: cost 1 inf + 0 2.709 * * [simplify]: Extracting #1: cost 13 inf + 0 2.709 * * [simplify]: Extracting #2: cost 26 inf + 0 2.709 * * [simplify]: Extracting #3: cost 27 inf + 254 2.709 * * [simplify]: Extracting #4: cost 28 inf + 407 2.709 * * [simplify]: Extracting #5: cost 29 inf + 1361 2.710 * * [simplify]: Extracting #6: cost 29 inf + 1447 2.710 * * [simplify]: Extracting #7: cost 18 inf + 2145 2.711 * * [simplify]: Extracting #8: cost 3 inf + 6187 2.712 * * [simplify]: Extracting #9: cost 0 inf + 7188 2.714 * [simplify]: Simplified to (+ (log (sqrt (+ 1 (* (* v -3) v)))) (log (/ (sqrt 2) 4))) 2.714 * [simplify]: Simplified (2 1 1) to (λ (v) (* (exp (+ (log (sqrt (+ 1 (* (* v -3) v)))) (log (/ (sqrt 2) 4)))) (- 1 (* v v)))) 2.714 * * * * [progress]: [ 41 / 98 ] simplifiying candidate # 2.714 * * * * [progress]: [ 42 / 98 ] simplifiying candidate # 2.714 * * * * [progress]: [ 43 / 98 ] simplifiying candidate # 2.714 * [simplify]: Simplifying (* (/ (* (* (sqrt 2) (sqrt 2)) (sqrt 2)) (* (* 4 4) 4)) (* (* (sqrt (- 1 (* 3 (* v v)))) (sqrt (- 1 (* 3 (* v v))))) (sqrt (- 1 (* 3 (* v v)))))) 2.714 * * [simplify]: iters left: 6 (18 enodes) 2.721 * * [simplify]: iters left: 5 (74 enodes) 2.747 * * [simplify]: iters left: 4 (177 enodes) 2.832 * * [simplify]: Extracting #0: cost 1 inf + 0 2.832 * * [simplify]: Extracting #1: cost 43 inf + 0 2.832 * * [simplify]: Extracting #2: cost 131 inf + 6 2.833 * * [simplify]: Extracting #3: cost 173 inf + 1237 2.834 * * [simplify]: Extracting #4: cost 145 inf + 4311 2.837 * * [simplify]: Extracting #5: cost 109 inf + 9619 2.841 * * [simplify]: Extracting #6: cost 58 inf + 21072 2.849 * * [simplify]: Extracting #7: cost 6 inf + 35578 2.865 * * [simplify]: Extracting #8: cost 0 inf + 37284 2.882 * [simplify]: Simplified to (* (+ 1 (* (* v v) -3)) (* (* (sqrt (+ 1 (* (* v v) -3))) 1/32) (sqrt 2))) 2.882 * [simplify]: Simplified (2 1 1) to (λ (v) (* (cbrt (* (+ 1 (* (* v v) -3)) (* (* (sqrt (+ 1 (* (* v v) -3))) 1/32) (sqrt 2)))) (- 1 (* v v)))) 2.882 * * * * [progress]: [ 44 / 98 ] simplifiying candidate # 2.882 * [simplify]: Simplifying (* (* (* (/ (sqrt 2) 4) (/ (sqrt 2) 4)) (/ (sqrt 2) 4)) (* (* (sqrt (- 1 (* 3 (* v v)))) (sqrt (- 1 (* 3 (* v v))))) (sqrt (- 1 (* 3 (* v v)))))) 2.882 * * [simplify]: iters left: 6 (16 enodes) 2.893 * * [simplify]: iters left: 5 (66 enodes) 2.919 * * [simplify]: iters left: 4 (157 enodes) 2.999 * * [simplify]: iters left: 3 (464 enodes) 3.558 * * [simplify]: Extracting #0: cost 1 inf + 0 3.559 * * [simplify]: Extracting #1: cost 74 inf + 0 3.561 * * [simplify]: Extracting #2: cost 344 inf + 49 3.566 * * [simplify]: Extracting #3: cost 498 inf + 6432 3.579 * * [simplify]: Extracting #4: cost 241 inf + 65854 3.624 * * [simplify]: Extracting #5: cost 6 inf + 133836 3.670 * * [simplify]: Extracting #6: cost 0 inf + 135142 3.702 * [simplify]: Simplified to (* (* (- 1 (* (* v v) 3)) (sqrt (- 1 (* (* v v) 3)))) (* 1/32 (sqrt 2))) 3.702 * [simplify]: Simplified (2 1 1) to (λ (v) (* (cbrt (* (* (- 1 (* (* v v) 3)) (sqrt (- 1 (* (* v v) 3)))) (* 1/32 (sqrt 2)))) (- 1 (* v v)))) 3.702 * * * * [progress]: [ 45 / 98 ] simplifiying candidate # 3.702 * * * * [progress]: [ 46 / 98 ] simplifiying candidate # 3.702 * * * * [progress]: [ 47 / 98 ] simplifiying candidate # 3.702 * * * * [progress]: [ 48 / 98 ] simplifiying candidate # 3.702 * [simplify]: Simplifying (* (sqrt 2) (sqrt (- (pow 1 3) (pow (* 3 (* v v)) 3)))) 3.702 * * [simplify]: iters left: 6 (12 enodes) 3.707 * * [simplify]: iters left: 5 (55 enodes) 3.720 * * [simplify]: iters left: 4 (132 enodes) 3.761 * * [simplify]: iters left: 3 (423 enodes) 4.005 * * [simplify]: Extracting #0: cost 1 inf + 0 4.005 * * [simplify]: Extracting #1: cost 4 inf + 0 4.005 * * [simplify]: Extracting #2: cost 8 inf + 0 4.005 * * [simplify]: Extracting #3: cost 11 inf + 1 4.005 * * [simplify]: Extracting #4: cost 77 inf + 84 4.007 * * [simplify]: Extracting #5: cost 179 inf + 1661 4.016 * * [simplify]: Extracting #6: cost 88 inf + 14678 4.032 * * [simplify]: Extracting #7: cost 16 inf + 32188 4.048 * * [simplify]: Extracting #8: cost 0 inf + 38038 4.065 * [simplify]: Simplified to (* (sqrt (- 1 (* (* v (* v v)) (* (* v (* v v)) 27)))) (sqrt 2)) 4.065 * [simplify]: Simplified (2 1 1) to (λ (v) (* (/ (* (sqrt (- 1 (* (* v (* v v)) (* (* v (* v v)) 27)))) (sqrt 2)) (* 4 (sqrt (+ (* 1 1) (+ (* (* 3 (* v v)) (* 3 (* v v))) (* 1 (* 3 (* v v)))))))) (- 1 (* v v)))) 4.066 * [simplify]: Simplifying (* 4 (sqrt (+ (* 1 1) (+ (* (* 3 (* v v)) (* 3 (* v v))) (* 1 (* 3 (* v v))))))) 4.066 * * [simplify]: iters left: 6 (13 enodes) 4.071 * * [simplify]: iters left: 5 (59 enodes) 4.085 * * [simplify]: iters left: 4 (143 enodes) 4.129 * * [simplify]: iters left: 3 (233 enodes) 4.220 * * [simplify]: iters left: 2 (315 enodes) 4.322 * * [simplify]: iters left: 1 (368 enodes) 4.402 * * [simplify]: Extracting #0: cost 1 inf + 0 4.402 * * [simplify]: Extracting #1: cost 4 inf + 0 4.402 * * [simplify]: Extracting #2: cost 5 inf + 1 4.402 * * [simplify]: Extracting #3: cost 12 inf + 1 4.402 * * [simplify]: Extracting #4: cost 41 inf + 2 4.403 * * [simplify]: Extracting #5: cost 69 inf + 511 4.403 * * [simplify]: Extracting #6: cost 47 inf + 3091 4.405 * * [simplify]: Extracting #7: cost 14 inf + 9995 4.408 * * [simplify]: Extracting #8: cost 0 inf + 13391 4.410 * [simplify]: Simplified to (* (sqrt (+ (* (+ 3 (* 9 (* v v))) (* v v)) 1)) 4) 4.410 * [simplify]: Simplified (2 1 2) to (λ (v) (* (/ (* (sqrt (- 1 (* (* v (* v v)) (* (* v (* v v)) 27)))) (sqrt 2)) (* (sqrt (+ (* (+ 3 (* 9 (* v v))) (* v v)) 1)) 4)) (- 1 (* v v)))) 4.411 * * * * [progress]: [ 49 / 98 ] simplifiying candidate # 4.411 * [simplify]: Simplifying (* (sqrt 2) (sqrt (- (* 1 1) (* (* 3 (* v v)) (* 3 (* v v)))))) 4.411 * * [simplify]: iters left: 6 (12 enodes) 4.415 * * [simplify]: iters left: 5 (50 enodes) 4.433 * * [simplify]: iters left: 4 (103 enodes) 4.462 * * [simplify]: iters left: 3 (215 enodes) 4.539 * * [simplify]: iters left: 2 (351 enodes) 4.653 * * [simplify]: iters left: 1 (430 enodes) 4.765 * * [simplify]: Extracting #0: cost 1 inf + 0 4.765 * * [simplify]: Extracting #1: cost 4 inf + 0 4.765 * * [simplify]: Extracting #2: cost 8 inf + 0 4.765 * * [simplify]: Extracting #3: cost 11 inf + 1 4.765 * * [simplify]: Extracting #4: cost 57 inf + 84 4.767 * * [simplify]: Extracting #5: cost 108 inf + 1069 4.770 * * [simplify]: Extracting #6: cost 68 inf + 6546 4.777 * * [simplify]: Extracting #7: cost 28 inf + 16516 4.784 * * [simplify]: Extracting #8: cost 11 inf + 21312 4.795 * * [simplify]: Extracting #9: cost 0 inf + 25342 4.802 * [simplify]: Simplified to (* (sqrt (- 1 (* (* (* v v) (* v v)) 9))) (sqrt 2)) 4.802 * [simplify]: Simplified (2 1 1) to (λ (v) (* (/ (* (sqrt (- 1 (* (* (* v v) (* v v)) 9))) (sqrt 2)) (* 4 (sqrt (+ 1 (* 3 (* v v)))))) (- 1 (* v v)))) 4.803 * [simplify]: Simplifying (* 4 (sqrt (+ 1 (* 3 (* v v))))) 4.803 * * [simplify]: iters left: 6 (9 enodes) 4.809 * * [simplify]: iters left: 5 (34 enodes) 4.817 * * [simplify]: iters left: 4 (40 enodes) 4.824 * * [simplify]: Extracting #0: cost 1 inf + 0 4.824 * * [simplify]: Extracting #1: cost 4 inf + 0 4.824 * * [simplify]: Extracting #2: cost 5 inf + 1 4.824 * * [simplify]: Extracting #3: cost 8 inf + 1 4.824 * * [simplify]: Extracting #4: cost 12 inf + 2 4.824 * * [simplify]: Extracting #5: cost 11 inf + 46 4.825 * * [simplify]: Extracting #6: cost 8 inf + 211 4.825 * * [simplify]: Extracting #7: cost 3 inf + 743 4.825 * * [simplify]: Extracting #8: cost 0 inf + 1314 4.825 * [simplify]: Simplified to (* (sqrt (+ 1 (* v (* 3 v)))) 4) 4.825 * [simplify]: Simplified (2 1 2) to (λ (v) (* (/ (* (sqrt 2) (sqrt (- (* 1 1) (* (* 3 (* v v)) (* 3 (* v v)))))) (* (sqrt (+ 1 (* v (* 3 v)))) 4)) (- 1 (* v v)))) 4.825 * * * * [progress]: [ 50 / 98 ] simplifiying candidate # 4.825 * * * * [progress]: [ 51 / 98 ] simplifiying candidate # 4.826 * [simplify]: Simplifying (* (sqrt (/ (sqrt 2) 4)) (sqrt (sqrt (- 1 (* 3 (* v v)))))) 4.826 * * [simplify]: iters left: 6 (14 enodes) 4.830 * * [simplify]: iters left: 5 (50 enodes) 4.840 * * [simplify]: iters left: 4 (70 enodes) 4.854 * * [simplify]: iters left: 3 (88 enodes) 4.878 * * [simplify]: Extracting #0: cost 1 inf + 0 4.878 * * [simplify]: Extracting #1: cost 4 inf + 0 4.878 * * [simplify]: Extracting #2: cost 8 inf + 0 4.878 * * [simplify]: Extracting #3: cost 13 inf + 0 4.878 * * [simplify]: Extracting #4: cost 18 inf + 1 4.878 * * [simplify]: Extracting #5: cost 23 inf + 167 4.878 * * [simplify]: Extracting #6: cost 17 inf + 743 4.879 * * [simplify]: Extracting #7: cost 2 inf + 2498 4.879 * * [simplify]: Extracting #8: cost 0 inf + 3026 4.880 * [simplify]: Simplified to (* (sqrt (/ (sqrt 2) 4)) (sqrt (sqrt (- 1 (* v (* v 3)))))) 4.880 * [simplify]: Simplified (2 1 1) to (λ (v) (* (* (* (sqrt (/ (sqrt 2) 4)) (sqrt (sqrt (- 1 (* v (* v 3)))))) (* (sqrt (/ (sqrt 2) 4)) (sqrt (sqrt (- 1 (* 3 (* v v))))))) (- 1 (* v v)))) 4.880 * [simplify]: Simplifying (* (sqrt (/ (sqrt 2) 4)) (sqrt (sqrt (- 1 (* 3 (* v v)))))) 4.880 * * [simplify]: iters left: 6 (14 enodes) 4.885 * * [simplify]: iters left: 5 (50 enodes) 4.894 * * [simplify]: iters left: 4 (70 enodes) 4.910 * * [simplify]: iters left: 3 (88 enodes) 4.929 * * [simplify]: Extracting #0: cost 1 inf + 0 4.929 * * [simplify]: Extracting #1: cost 4 inf + 0 4.929 * * [simplify]: Extracting #2: cost 8 inf + 0 4.929 * * [simplify]: Extracting #3: cost 13 inf + 0 4.929 * * [simplify]: Extracting #4: cost 18 inf + 1 4.929 * * [simplify]: Extracting #5: cost 23 inf + 167 4.929 * * [simplify]: Extracting #6: cost 17 inf + 743 4.930 * * [simplify]: Extracting #7: cost 2 inf + 2498 4.930 * * [simplify]: Extracting #8: cost 0 inf + 3026 4.931 * [simplify]: Simplified to (* (sqrt (/ (sqrt 2) 4)) (sqrt (sqrt (- 1 (* v (* v 3)))))) 4.931 * [simplify]: Simplified (2 1 2) to (λ (v) (* (* (* (sqrt (/ (sqrt 2) 4)) (sqrt (sqrt (- 1 (* 3 (* v v)))))) (* (sqrt (/ (sqrt 2) 4)) (sqrt (sqrt (- 1 (* v (* v 3))))))) (- 1 (* v v)))) 4.931 * * * * [progress]: [ 52 / 98 ] simplifiying candidate # 4.932 * [simplify]: Simplifying (* (sqrt (/ (sqrt 2) 4)) (sqrt (sqrt (- 1 (* 3 (* v v)))))) 4.932 * * [simplify]: iters left: 6 (14 enodes) 4.936 * * [simplify]: iters left: 5 (50 enodes) 4.946 * * [simplify]: iters left: 4 (70 enodes) 4.962 * * [simplify]: iters left: 3 (88 enodes) 4.977 * * [simplify]: Extracting #0: cost 1 inf + 0 4.977 * * [simplify]: Extracting #1: cost 4 inf + 0 4.977 * * [simplify]: Extracting #2: cost 8 inf + 0 4.977 * * [simplify]: Extracting #3: cost 13 inf + 0 4.977 * * [simplify]: Extracting #4: cost 18 inf + 1 4.977 * * [simplify]: Extracting #5: cost 23 inf + 167 4.977 * * [simplify]: Extracting #6: cost 17 inf + 743 4.977 * * [simplify]: Extracting #7: cost 2 inf + 2498 4.978 * * [simplify]: Extracting #8: cost 0 inf + 3026 4.979 * [simplify]: Simplified to (* (sqrt (/ (sqrt 2) 4)) (sqrt (sqrt (- 1 (* v (* v 3)))))) 4.979 * [simplify]: Simplified (2 1 1) to (λ (v) (* (* (* (sqrt (/ (sqrt 2) 4)) (sqrt (sqrt (- 1 (* v (* v 3)))))) (* (sqrt (/ (sqrt 2) 4)) (sqrt (sqrt (- 1 (* 3 (* v v))))))) (- 1 (* v v)))) 4.979 * [simplify]: Simplifying (* (sqrt (/ (sqrt 2) 4)) (sqrt (sqrt (- 1 (* 3 (* v v)))))) 4.979 * * [simplify]: iters left: 6 (14 enodes) 4.985 * * [simplify]: iters left: 5 (50 enodes) 5.004 * * [simplify]: iters left: 4 (70 enodes) 5.019 * * [simplify]: iters left: 3 (88 enodes) 5.034 * * [simplify]: Extracting #0: cost 1 inf + 0 5.034 * * [simplify]: Extracting #1: cost 4 inf + 0 5.034 * * [simplify]: Extracting #2: cost 8 inf + 0 5.034 * * [simplify]: Extracting #3: cost 13 inf + 0 5.034 * * [simplify]: Extracting #4: cost 18 inf + 1 5.034 * * [simplify]: Extracting #5: cost 23 inf + 167 5.035 * * [simplify]: Extracting #6: cost 17 inf + 743 5.035 * * [simplify]: Extracting #7: cost 2 inf + 2498 5.036 * * [simplify]: Extracting #8: cost 0 inf + 3026 5.036 * [simplify]: Simplified to (* (sqrt (/ (sqrt 2) 4)) (sqrt (sqrt (- 1 (* v (* v 3)))))) 5.036 * [simplify]: Simplified (2 1 2) to (λ (v) (* (* (* (sqrt (/ (sqrt 2) 4)) (sqrt (sqrt (- 1 (* 3 (* v v)))))) (* (sqrt (/ (sqrt 2) 4)) (sqrt (sqrt (- 1 (* v (* v 3))))))) (- 1 (* v v)))) 5.036 * * * * [progress]: [ 53 / 98 ] simplifiying candidate # 5.037 * [simplify]: Simplifying (* (/ (sqrt (sqrt 2)) (sqrt 4)) (sqrt (sqrt (- 1 (* 3 (* v v)))))) 5.037 * * [simplify]: iters left: 6 (15 enodes) 5.043 * * [simplify]: iters left: 5 (55 enodes) 5.062 * * [simplify]: iters left: 4 (82 enodes) 5.087 * * [simplify]: iters left: 3 (102 enodes) 5.117 * * [simplify]: Extracting #0: cost 1 inf + 0 5.117 * * [simplify]: Extracting #1: cost 8 inf + 0 5.117 * * [simplify]: Extracting #2: cost 14 inf + 1 5.117 * * [simplify]: Extracting #3: cost 16 inf + 42 5.117 * * [simplify]: Extracting #4: cost 15 inf + 487 5.118 * * [simplify]: Extracting #5: cost 24 inf + 488 5.118 * * [simplify]: Extracting #6: cost 23 inf + 615 5.119 * * [simplify]: Extracting #7: cost 11 inf + 1559 5.120 * * [simplify]: Extracting #8: cost 7 inf + 2088 5.121 * * [simplify]: Extracting #9: cost 0 inf + 4155 5.123 * [simplify]: Simplified to (* (/ (sqrt (sqrt 2)) 2) (sqrt (sqrt (- 1 (* (* v v) 3))))) 5.123 * [simplify]: Simplified (2 1 1) to (λ (v) (* (* (* (/ (sqrt (sqrt 2)) 2) (sqrt (sqrt (- 1 (* (* v v) 3))))) (* (/ (sqrt (sqrt 2)) (sqrt 4)) (sqrt (sqrt (- 1 (* 3 (* v v))))))) (- 1 (* v v)))) 5.124 * [simplify]: Simplifying (* (/ (sqrt (sqrt 2)) (sqrt 4)) (sqrt (sqrt (- 1 (* 3 (* v v)))))) 5.124 * * [simplify]: iters left: 6 (15 enodes) 5.135 * * [simplify]: iters left: 5 (55 enodes) 5.154 * * [simplify]: iters left: 4 (82 enodes) 5.178 * * [simplify]: iters left: 3 (102 enodes) 5.207 * * [simplify]: Extracting #0: cost 1 inf + 0 5.207 * * [simplify]: Extracting #1: cost 8 inf + 0 5.207 * * [simplify]: Extracting #2: cost 14 inf + 1 5.207 * * [simplify]: Extracting #3: cost 16 inf + 42 5.208 * * [simplify]: Extracting #4: cost 15 inf + 487 5.208 * * [simplify]: Extracting #5: cost 24 inf + 488 5.208 * * [simplify]: Extracting #6: cost 23 inf + 615 5.209 * * [simplify]: Extracting #7: cost 11 inf + 1559 5.210 * * [simplify]: Extracting #8: cost 7 inf + 2088 5.211 * * [simplify]: Extracting #9: cost 0 inf + 4155 5.213 * [simplify]: Simplified to (* (/ (sqrt (sqrt 2)) 2) (sqrt (sqrt (- 1 (* (* v v) 3))))) 5.213 * [simplify]: Simplified (2 1 2) to (λ (v) (* (* (* (/ (sqrt (sqrt 2)) (sqrt 4)) (sqrt (sqrt (- 1 (* 3 (* v v)))))) (* (/ (sqrt (sqrt 2)) 2) (sqrt (sqrt (- 1 (* (* v v) 3)))))) (- 1 (* v v)))) 5.214 * * * * [progress]: [ 54 / 98 ] simplifiying candidate # 5.214 * [simplify]: Simplifying (* (/ (sqrt (sqrt 2)) (sqrt 4)) (sqrt (sqrt (- 1 (* 3 (* v v)))))) 5.214 * * [simplify]: iters left: 6 (15 enodes) 5.225 * * [simplify]: iters left: 5 (55 enodes) 5.244 * * [simplify]: iters left: 4 (82 enodes) 5.270 * * [simplify]: iters left: 3 (102 enodes) 5.303 * * [simplify]: Extracting #0: cost 1 inf + 0 5.303 * * [simplify]: Extracting #1: cost 8 inf + 0 5.303 * * [simplify]: Extracting #2: cost 14 inf + 1 5.303 * * [simplify]: Extracting #3: cost 16 inf + 42 5.303 * * [simplify]: Extracting #4: cost 15 inf + 487 5.303 * * [simplify]: Extracting #5: cost 24 inf + 488 5.304 * * [simplify]: Extracting #6: cost 23 inf + 615 5.304 * * [simplify]: Extracting #7: cost 11 inf + 1559 5.305 * * [simplify]: Extracting #8: cost 7 inf + 2088 5.307 * * [simplify]: Extracting #9: cost 0 inf + 4155 5.309 * [simplify]: Simplified to (* (/ (sqrt (sqrt 2)) 2) (sqrt (sqrt (- 1 (* (* v v) 3))))) 5.309 * [simplify]: Simplified (2 1 1) to (λ (v) (* (* (* (/ (sqrt (sqrt 2)) 2) (sqrt (sqrt (- 1 (* (* v v) 3))))) (* (/ (sqrt (sqrt 2)) (sqrt 4)) (sqrt (sqrt (- 1 (* 3 (* v v))))))) (- 1 (* v v)))) 5.309 * [simplify]: Simplifying (* (/ (sqrt (sqrt 2)) (sqrt 4)) (sqrt (sqrt (- 1 (* 3 (* v v)))))) 5.309 * * [simplify]: iters left: 6 (15 enodes) 5.319 * * [simplify]: iters left: 5 (55 enodes) 5.337 * * [simplify]: iters left: 4 (82 enodes) 5.356 * * [simplify]: iters left: 3 (102 enodes) 5.373 * * [simplify]: Extracting #0: cost 1 inf + 0 5.373 * * [simplify]: Extracting #1: cost 8 inf + 0 5.373 * * [simplify]: Extracting #2: cost 14 inf + 1 5.373 * * [simplify]: Extracting #3: cost 16 inf + 42 5.373 * * [simplify]: Extracting #4: cost 15 inf + 487 5.373 * * [simplify]: Extracting #5: cost 24 inf + 488 5.373 * * [simplify]: Extracting #6: cost 23 inf + 615 5.374 * * [simplify]: Extracting #7: cost 11 inf + 1559 5.374 * * [simplify]: Extracting #8: cost 7 inf + 2088 5.375 * * [simplify]: Extracting #9: cost 0 inf + 4155 5.376 * [simplify]: Simplified to (* (/ (sqrt (sqrt 2)) 2) (sqrt (sqrt (- 1 (* (* v v) 3))))) 5.376 * [simplify]: Simplified (2 1 2) to (λ (v) (* (* (* (/ (sqrt (sqrt 2)) (sqrt 4)) (sqrt (sqrt (- 1 (* 3 (* v v)))))) (* (/ (sqrt (sqrt 2)) 2) (sqrt (sqrt (- 1 (* (* v v) 3)))))) (- 1 (* v v)))) 5.376 * * * * [progress]: [ 55 / 98 ] simplifiying candidate # 5.376 * [simplify]: Simplifying (* (/ (sqrt (sqrt 2)) (sqrt 4)) (sqrt (sqrt (- 1 (* 3 (* v v)))))) 5.376 * * [simplify]: iters left: 6 (15 enodes) 5.386 * * [simplify]: iters left: 5 (55 enodes) 5.398 * * [simplify]: iters left: 4 (82 enodes) 5.414 * * [simplify]: iters left: 3 (102 enodes) 5.440 * * [simplify]: Extracting #0: cost 1 inf + 0 5.440 * * [simplify]: Extracting #1: cost 8 inf + 0 5.440 * * [simplify]: Extracting #2: cost 14 inf + 1 5.440 * * [simplify]: Extracting #3: cost 16 inf + 42 5.440 * * [simplify]: Extracting #4: cost 15 inf + 487 5.440 * * [simplify]: Extracting #5: cost 24 inf + 488 5.440 * * [simplify]: Extracting #6: cost 23 inf + 615 5.441 * * [simplify]: Extracting #7: cost 11 inf + 1559 5.441 * * [simplify]: Extracting #8: cost 7 inf + 2088 5.442 * * [simplify]: Extracting #9: cost 0 inf + 4155 5.443 * [simplify]: Simplified to (* (/ (sqrt (sqrt 2)) 2) (sqrt (sqrt (- 1 (* (* v v) 3))))) 5.443 * [simplify]: Simplified (2 1 1) to (λ (v) (* (* (* (/ (sqrt (sqrt 2)) 2) (sqrt (sqrt (- 1 (* (* v v) 3))))) (* (/ (sqrt (sqrt 2)) (sqrt 4)) (sqrt (sqrt (- 1 (* 3 (* v v))))))) (- 1 (* v v)))) 5.443 * [simplify]: Simplifying (* (/ (sqrt (sqrt 2)) (sqrt 4)) (sqrt (sqrt (- 1 (* 3 (* v v)))))) 5.443 * * [simplify]: iters left: 6 (15 enodes) 5.449 * * [simplify]: iters left: 5 (55 enodes) 5.459 * * [simplify]: iters left: 4 (82 enodes) 5.475 * * [simplify]: iters left: 3 (102 enodes) 5.496 * * [simplify]: Extracting #0: cost 1 inf + 0 5.496 * * [simplify]: Extracting #1: cost 8 inf + 0 5.496 * * [simplify]: Extracting #2: cost 14 inf + 1 5.496 * * [simplify]: Extracting #3: cost 16 inf + 42 5.496 * * [simplify]: Extracting #4: cost 15 inf + 487 5.497 * * [simplify]: Extracting #5: cost 24 inf + 488 5.497 * * [simplify]: Extracting #6: cost 23 inf + 615 5.497 * * [simplify]: Extracting #7: cost 11 inf + 1559 5.498 * * [simplify]: Extracting #8: cost 7 inf + 2088 5.499 * * [simplify]: Extracting #9: cost 0 inf + 4155 5.500 * [simplify]: Simplified to (* (/ (sqrt (sqrt 2)) 2) (sqrt (sqrt (- 1 (* (* v v) 3))))) 5.500 * [simplify]: Simplified (2 1 2) to (λ (v) (* (* (* (/ (sqrt (sqrt 2)) (sqrt 4)) (sqrt (sqrt (- 1 (* 3 (* v v)))))) (* (/ (sqrt (sqrt 2)) 2) (sqrt (sqrt (- 1 (* (* v v) 3)))))) (- 1 (* v v)))) 5.500 * * * * [progress]: [ 56 / 98 ] simplifiying candidate # 5.500 * [simplify]: Simplifying (* (/ (sqrt (sqrt 2)) (sqrt 4)) (sqrt (sqrt (- 1 (* 3 (* v v)))))) 5.500 * * [simplify]: iters left: 6 (15 enodes) 5.507 * * [simplify]: iters left: 5 (55 enodes) 5.520 * * [simplify]: iters left: 4 (82 enodes) 5.545 * * [simplify]: iters left: 3 (102 enodes) 5.575 * * [simplify]: Extracting #0: cost 1 inf + 0 5.575 * * [simplify]: Extracting #1: cost 8 inf + 0 5.575 * * [simplify]: Extracting #2: cost 14 inf + 1 5.575 * * [simplify]: Extracting #3: cost 16 inf + 42 5.575 * * [simplify]: Extracting #4: cost 15 inf + 487 5.576 * * [simplify]: Extracting #5: cost 24 inf + 488 5.576 * * [simplify]: Extracting #6: cost 23 inf + 615 5.577 * * [simplify]: Extracting #7: cost 11 inf + 1559 5.578 * * [simplify]: Extracting #8: cost 7 inf + 2088 5.579 * * [simplify]: Extracting #9: cost 0 inf + 4155 5.581 * [simplify]: Simplified to (* (/ (sqrt (sqrt 2)) 2) (sqrt (sqrt (- 1 (* (* v v) 3))))) 5.581 * [simplify]: Simplified (2 1 1) to (λ (v) (* (* (* (/ (sqrt (sqrt 2)) 2) (sqrt (sqrt (- 1 (* (* v v) 3))))) (* (/ (sqrt (sqrt 2)) (sqrt 4)) (sqrt (sqrt (- 1 (* 3 (* v v))))))) (- 1 (* v v)))) 5.581 * [simplify]: Simplifying (* (/ (sqrt (sqrt 2)) (sqrt 4)) (sqrt (sqrt (- 1 (* 3 (* v v)))))) 5.582 * * [simplify]: iters left: 6 (15 enodes) 5.592 * * [simplify]: iters left: 5 (55 enodes) 5.610 * * [simplify]: iters left: 4 (82 enodes) 5.632 * * [simplify]: iters left: 3 (102 enodes) 5.650 * * [simplify]: Extracting #0: cost 1 inf + 0 5.650 * * [simplify]: Extracting #1: cost 8 inf + 0 5.650 * * [simplify]: Extracting #2: cost 14 inf + 1 5.650 * * [simplify]: Extracting #3: cost 16 inf + 42 5.651 * * [simplify]: Extracting #4: cost 15 inf + 487 5.651 * * [simplify]: Extracting #5: cost 24 inf + 488 5.651 * * [simplify]: Extracting #6: cost 23 inf + 615 5.651 * * [simplify]: Extracting #7: cost 11 inf + 1559 5.652 * * [simplify]: Extracting #8: cost 7 inf + 2088 5.653 * * [simplify]: Extracting #9: cost 0 inf + 4155 5.654 * [simplify]: Simplified to (* (/ (sqrt (sqrt 2)) 2) (sqrt (sqrt (- 1 (* (* v v) 3))))) 5.654 * [simplify]: Simplified (2 1 2) to (λ (v) (* (* (* (/ (sqrt (sqrt 2)) (sqrt 4)) (sqrt (sqrt (- 1 (* 3 (* v v)))))) (* (/ (sqrt (sqrt 2)) 2) (sqrt (sqrt (- 1 (* (* v v) 3)))))) (- 1 (* v v)))) 5.654 * * * * [progress]: [ 57 / 98 ] simplifiying candidate # 5.654 * [simplify]: Simplifying (cbrt (sqrt (- 1 (* 3 (* v v))))) 5.654 * * [simplify]: iters left: 6 (8 enodes) 5.659 * * [simplify]: iters left: 5 (31 enodes) 5.670 * * [simplify]: iters left: 4 (51 enodes) 5.687 * * [simplify]: iters left: 3 (69 enodes) 5.699 * * [simplify]: Extracting #0: cost 1 inf + 0 5.700 * * [simplify]: Extracting #1: cost 3 inf + 0 5.700 * * [simplify]: Extracting #2: cost 5 inf + 0 5.700 * * [simplify]: Extracting #3: cost 9 inf + 0 5.700 * * [simplify]: Extracting #4: cost 18 inf + 1 5.700 * * [simplify]: Extracting #5: cost 17 inf + 128 5.700 * * [simplify]: Extracting #6: cost 6 inf + 868 5.700 * * [simplify]: Extracting #7: cost 0 inf + 1884 5.701 * [simplify]: Simplified to (cbrt (sqrt (- 1 (* (* v v) 3)))) 5.701 * [simplify]: Simplified (2 1 2) to (λ (v) (* (* (* (/ (sqrt 2) 4) (* (cbrt (sqrt (- 1 (* 3 (* v v))))) (cbrt (sqrt (- 1 (* 3 (* v v))))))) (cbrt (sqrt (- 1 (* (* v v) 3))))) (- 1 (* v v)))) 5.701 * * * * [progress]: [ 58 / 98 ] simplifiying candidate # 5.701 * [simplify]: Simplifying (sqrt (cbrt (- 1 (* 3 (* v v))))) 5.701 * * [simplify]: iters left: 6 (8 enodes) 5.704 * * [simplify]: iters left: 5 (31 enodes) 5.710 * * [simplify]: iters left: 4 (51 enodes) 5.722 * * [simplify]: iters left: 3 (69 enodes) 5.739 * * [simplify]: Extracting #0: cost 1 inf + 0 5.739 * * [simplify]: Extracting #1: cost 3 inf + 0 5.739 * * [simplify]: Extracting #2: cost 5 inf + 0 5.739 * * [simplify]: Extracting #3: cost 9 inf + 0 5.739 * * [simplify]: Extracting #4: cost 18 inf + 1 5.739 * * [simplify]: Extracting #5: cost 17 inf + 128 5.740 * * [simplify]: Extracting #6: cost 6 inf + 868 5.740 * * [simplify]: Extracting #7: cost 0 inf + 1964 5.740 * [simplify]: Simplified to (sqrt (cbrt (- 1 (* (* v v) 3)))) 5.740 * [simplify]: Simplified (2 1 2) to (λ (v) (* (* (* (/ (sqrt 2) 4) (sqrt (* (cbrt (- 1 (* 3 (* v v)))) (cbrt (- 1 (* 3 (* v v))))))) (sqrt (cbrt (- 1 (* (* v v) 3))))) (- 1 (* v v)))) 5.741 * * * * [progress]: [ 59 / 98 ] simplifiying candidate # 5.741 * [simplify]: Simplifying (sqrt (sqrt (- 1 (* 3 (* v v))))) 5.741 * * [simplify]: iters left: 6 (8 enodes) 5.743 * * [simplify]: iters left: 5 (31 enodes) 5.750 * * [simplify]: iters left: 4 (51 enodes) 5.761 * * [simplify]: iters left: 3 (69 enodes) 5.781 * * [simplify]: Extracting #0: cost 1 inf + 0 5.781 * * [simplify]: Extracting #1: cost 3 inf + 0 5.781 * * [simplify]: Extracting #2: cost 5 inf + 0 5.781 * * [simplify]: Extracting #3: cost 9 inf + 0 5.781 * * [simplify]: Extracting #4: cost 18 inf + 1 5.782 * * [simplify]: Extracting #5: cost 17 inf + 128 5.782 * * [simplify]: Extracting #6: cost 6 inf + 868 5.783 * * [simplify]: Extracting #7: cost 0 inf + 1804 5.784 * [simplify]: Simplified to (sqrt (sqrt (- 1 (* (* v v) 3)))) 5.784 * [simplify]: Simplified (2 1 2) to (λ (v) (* (* (* (/ (sqrt 2) 4) (sqrt (sqrt (- 1 (* 3 (* v v)))))) (sqrt (sqrt (- 1 (* (* v v) 3))))) (- 1 (* v v)))) 5.784 * * * * [progress]: [ 60 / 98 ] simplifiying candidate # 5.784 * [simplify]: Simplifying (sqrt (- 1 (* 3 (* v v)))) 5.784 * * [simplify]: iters left: 6 (7 enodes) 5.788 * * [simplify]: iters left: 5 (28 enodes) 5.799 * * [simplify]: iters left: 4 (48 enodes) 5.815 * * [simplify]: iters left: 3 (66 enodes) 5.835 * * [simplify]: Extracting #0: cost 1 inf + 0 5.835 * * [simplify]: Extracting #1: cost 3 inf + 0 5.835 * * [simplify]: Extracting #2: cost 7 inf + 0 5.835 * * [simplify]: Extracting #3: cost 16 inf + 1 5.835 * * [simplify]: Extracting #4: cost 13 inf + 331 5.836 * * [simplify]: Extracting #5: cost 4 inf + 907 5.836 * * [simplify]: Extracting #6: cost 0 inf + 1398 5.837 * [simplify]: Simplified to (sqrt (- 1 (* (* v v) 3))) 5.837 * [simplify]: Simplified (2 1 2) to (λ (v) (* (* (* (/ (sqrt 2) 4) (sqrt 1)) (sqrt (- 1 (* (* v v) 3)))) (- 1 (* v v)))) 5.837 * * * * [progress]: [ 61 / 98 ] simplifiying candidate # 5.838 * [simplify]: Simplifying (sqrt (sqrt (- 1 (* 3 (* v v))))) 5.838 * * [simplify]: iters left: 6 (8 enodes) 5.842 * * [simplify]: iters left: 5 (31 enodes) 5.854 * * [simplify]: iters left: 4 (51 enodes) 5.865 * * [simplify]: iters left: 3 (69 enodes) 5.876 * * [simplify]: Extracting #0: cost 1 inf + 0 5.876 * * [simplify]: Extracting #1: cost 3 inf + 0 5.876 * * [simplify]: Extracting #2: cost 5 inf + 0 5.876 * * [simplify]: Extracting #3: cost 9 inf + 0 5.876 * * [simplify]: Extracting #4: cost 18 inf + 1 5.876 * * [simplify]: Extracting #5: cost 17 inf + 128 5.876 * * [simplify]: Extracting #6: cost 6 inf + 868 5.877 * * [simplify]: Extracting #7: cost 0 inf + 1804 5.877 * [simplify]: Simplified to (sqrt (sqrt (- 1 (* (* v v) 3)))) 5.877 * [simplify]: Simplified (2 1 2) to (λ (v) (* (* (* (/ (sqrt 2) 4) (sqrt (sqrt (- 1 (* 3 (* v v)))))) (sqrt (sqrt (- 1 (* (* v v) 3))))) (- 1 (* v v)))) 5.877 * * * * [progress]: [ 62 / 98 ] simplifiying candidate # 5.877 * [simplify]: Simplifying (sqrt (- 1 (* 3 (* v v)))) 5.877 * * [simplify]: iters left: 6 (7 enodes) 5.880 * * [simplify]: iters left: 5 (28 enodes) 5.891 * * [simplify]: iters left: 4 (48 enodes) 5.907 * * [simplify]: iters left: 3 (66 enodes) 5.927 * * [simplify]: Extracting #0: cost 1 inf + 0 5.927 * * [simplify]: Extracting #1: cost 3 inf + 0 5.927 * * [simplify]: Extracting #2: cost 7 inf + 0 5.927 * * [simplify]: Extracting #3: cost 16 inf + 1 5.928 * * [simplify]: Extracting #4: cost 13 inf + 331 5.929 * * [simplify]: Extracting #5: cost 4 inf + 907 5.929 * * [simplify]: Extracting #6: cost 0 inf + 1398 5.930 * [simplify]: Simplified to (sqrt (- 1 (* (* v v) 3))) 5.930 * [simplify]: Simplified (2 1 2) to (λ (v) (* (* (* (/ (sqrt 2) 4) 1) (sqrt (- 1 (* (* v v) 3)))) (- 1 (* v v)))) 5.930 * * * * [progress]: [ 63 / 98 ] simplifiying candidate # 5.931 * [simplify]: Simplifying (* (cbrt (/ (sqrt 2) 4)) (cbrt (/ (sqrt 2) 4))) 5.931 * * [simplify]: iters left: 6 (6 enodes) 5.935 * * [simplify]: iters left: 5 (18 enodes) 5.941 * * [simplify]: Extracting #0: cost 1 inf + 0 5.941 * * [simplify]: Extracting #1: cost 3 inf + 0 5.941 * * [simplify]: Extracting #2: cost 5 inf + 0 5.941 * * [simplify]: Extracting #3: cost 8 inf + 0 5.941 * * [simplify]: Extracting #4: cost 9 inf + 1 5.941 * * [simplify]: Extracting #5: cost 8 inf + 2 5.942 * * [simplify]: Extracting #6: cost 0 inf + 976 5.942 * [simplify]: Simplified to (* (cbrt (/ (sqrt 2) 4)) (cbrt (/ (sqrt 2) 4))) 5.942 * [simplify]: Simplified (2 1 1) to (λ (v) (* (* (* (cbrt (/ (sqrt 2) 4)) (cbrt (/ (sqrt 2) 4))) (* (cbrt (/ (sqrt 2) 4)) (sqrt (- 1 (* 3 (* v v)))))) (- 1 (* v v)))) 5.942 * * * * [progress]: [ 64 / 98 ] simplifiying candidate # 5.942 * [simplify]: Simplifying (sqrt (/ (sqrt 2) 4)) 5.942 * * [simplify]: iters left: 4 (5 enodes) 5.946 * * [simplify]: iters left: 3 (15 enodes) 5.951 * * [simplify]: Extracting #0: cost 1 inf + 0 5.951 * * [simplify]: Extracting #1: cost 3 inf + 0 5.951 * * [simplify]: Extracting #2: cost 6 inf + 0 5.951 * * [simplify]: Extracting #3: cost 7 inf + 1 5.951 * * [simplify]: Extracting #4: cost 6 inf + 2 5.952 * * [simplify]: Extracting #5: cost 0 inf + 492 5.952 * [simplify]: Simplified to (sqrt (/ (sqrt 2) 4)) 5.952 * [simplify]: Simplified (2 1 1) to (λ (v) (* (* (sqrt (/ (sqrt 2) 4)) (* (sqrt (/ (sqrt 2) 4)) (sqrt (- 1 (* 3 (* v v)))))) (- 1 (* v v)))) 5.952 * * * * [progress]: [ 65 / 98 ] simplifiying candidate # 5.952 * [simplify]: Simplifying (/ (* (cbrt (sqrt 2)) (cbrt (sqrt 2))) (* (cbrt 4) (cbrt 4))) 5.952 * * [simplify]: iters left: 6 (8 enodes) 5.958 * * [simplify]: iters left: 5 (30 enodes) 5.969 * * [simplify]: iters left: 4 (45 enodes) 5.979 * * [simplify]: iters left: 3 (52 enodes) 5.988 * * [simplify]: iters left: 2 (55 enodes) 5.997 * * [simplify]: Extracting #0: cost 1 inf + 0 5.997 * * [simplify]: Extracting #1: cost 11 inf + 0 5.997 * * [simplify]: Extracting #2: cost 22 inf + 0 5.997 * * [simplify]: Extracting #3: cost 22 inf + 82 5.997 * * [simplify]: Extracting #4: cost 17 inf + 447 5.998 * * [simplify]: Extracting #5: cost 5 inf + 3107 5.998 * * [simplify]: Extracting #6: cost 0 inf + 4276 5.999 * [simplify]: Simplified to (* (/ (cbrt (sqrt 2)) (cbrt 4)) (/ (cbrt (sqrt 2)) (cbrt 4))) 5.999 * [simplify]: Simplified (2 1 1) to (λ (v) (* (* (* (/ (cbrt (sqrt 2)) (cbrt 4)) (/ (cbrt (sqrt 2)) (cbrt 4))) (* (/ (cbrt (sqrt 2)) (cbrt 4)) (sqrt (- 1 (* 3 (* v v)))))) (- 1 (* v v)))) 5.999 * * * * [progress]: [ 66 / 98 ] simplifiying candidate # 5.999 * [simplify]: Simplifying (/ (* (cbrt (sqrt 2)) (cbrt (sqrt 2))) (sqrt 4)) 5.999 * * [simplify]: iters left: 6 (7 enodes) 6.002 * * [simplify]: iters left: 5 (23 enodes) 6.006 * * [simplify]: iters left: 4 (29 enodes) 6.018 * * [simplify]: iters left: 3 (34 enodes) 6.028 * * [simplify]: Extracting #0: cost 1 inf + 0 6.028 * * [simplify]: Extracting #1: cost 8 inf + 0 6.028 * * [simplify]: Extracting #2: cost 13 inf + 1 6.028 * * [simplify]: Extracting #3: cost 13 inf + 42 6.029 * * [simplify]: Extracting #4: cost 3 inf + 1452 6.029 * * [simplify]: Extracting #5: cost 1 inf + 1814 6.030 * * [simplify]: Extracting #6: cost 0 inf + 2015 6.030 * [simplify]: Simplified to (/ (cbrt (sqrt 2)) (/ 2 (cbrt (sqrt 2)))) 6.030 * [simplify]: Simplified (2 1 1) to (λ (v) (* (* (/ (cbrt (sqrt 2)) (/ 2 (cbrt (sqrt 2)))) (* (/ (cbrt (sqrt 2)) (sqrt 4)) (sqrt (- 1 (* 3 (* v v)))))) (- 1 (* v v)))) 6.030 * * * * [progress]: [ 67 / 98 ] simplifiying candidate # 6.031 * [simplify]: Simplifying (/ (* (cbrt (sqrt 2)) (cbrt (sqrt 2))) 1) 6.031 * * [simplify]: iters left: 6 (6 enodes) 6.035 * * [simplify]: iters left: 5 (20 enodes) 6.043 * * [simplify]: iters left: 4 (30 enodes) 6.053 * * [simplify]: iters left: 3 (31 enodes) 6.062 * * [simplify]: Extracting #0: cost 1 inf + 0 6.062 * * [simplify]: Extracting #1: cost 5 inf + 0 6.062 * * [simplify]: Extracting #2: cost 7 inf + 1 6.062 * * [simplify]: Extracting #3: cost 9 inf + 1 6.062 * * [simplify]: Extracting #4: cost 8 inf + 2 6.062 * * [simplify]: Extracting #5: cost 0 inf + 972 6.063 * [simplify]: Simplified to (* (cbrt (sqrt 2)) (cbrt (sqrt 2))) 6.063 * [simplify]: Simplified (2 1 1) to (λ (v) (* (* (* (cbrt (sqrt 2)) (cbrt (sqrt 2))) (* (/ (cbrt (sqrt 2)) 4) (sqrt (- 1 (* 3 (* v v)))))) (- 1 (* v v)))) 6.063 * * * * [progress]: [ 68 / 98 ] simplifiying candidate # 6.063 * [simplify]: Simplifying (/ (sqrt (* (cbrt 2) (cbrt 2))) (* (cbrt 4) (cbrt 4))) 6.063 * * [simplify]: iters left: 6 (8 enodes) 6.068 * * [simplify]: iters left: 5 (27 enodes) 6.077 * * [simplify]: iters left: 4 (29 enodes) 6.087 * * [simplify]: Extracting #0: cost 1 inf + 0 6.087 * * [simplify]: Extracting #1: cost 6 inf + 0 6.088 * * [simplify]: Extracting #2: cost 13 inf + 0 6.088 * * [simplify]: Extracting #3: cost 14 inf + 82 6.088 * * [simplify]: Extracting #4: cost 11 inf + 285 6.088 * * [simplify]: Extracting #5: cost 4 inf + 1334 6.089 * * [simplify]: Extracting #6: cost 0 inf + 2100 6.089 * [simplify]: Simplified to (/ (fabs (cbrt 2)) (* (cbrt 4) (cbrt 4))) 6.089 * [simplify]: Simplified (2 1 1) to (λ (v) (* (* (/ (fabs (cbrt 2)) (* (cbrt 4) (cbrt 4))) (* (/ (sqrt (cbrt 2)) (cbrt 4)) (sqrt (- 1 (* 3 (* v v)))))) (- 1 (* v v)))) 6.090 * * * * [progress]: [ 69 / 98 ] simplifiying candidate # 6.090 * [simplify]: Simplifying (/ (sqrt (* (cbrt 2) (cbrt 2))) (sqrt 4)) 6.090 * * [simplify]: iters left: 6 (7 enodes) 6.095 * * [simplify]: iters left: 5 (22 enodes) 6.102 * * [simplify]: Extracting #0: cost 1 inf + 0 6.102 * * [simplify]: Extracting #1: cost 4 inf + 0 6.102 * * [simplify]: Extracting #2: cost 6 inf + 1 6.102 * * [simplify]: Extracting #3: cost 3 inf + 606 6.102 * * [simplify]: Extracting #4: cost 0 inf + 969 6.102 * [simplify]: Simplified to (/ (fabs (cbrt 2)) 2) 6.102 * [simplify]: Simplified (2 1 1) to (λ (v) (* (* (/ (fabs (cbrt 2)) 2) (* (/ (sqrt (cbrt 2)) (sqrt 4)) (sqrt (- 1 (* 3 (* v v)))))) (- 1 (* v v)))) 6.103 * * * * [progress]: [ 70 / 98 ] simplifiying candidate # 6.103 * [simplify]: Simplifying (/ (sqrt (* (cbrt 2) (cbrt 2))) 1) 6.103 * * [simplify]: iters left: 6 (6 enodes) 6.107 * * [simplify]: iters left: 5 (19 enodes) 6.114 * * [simplify]: iters left: 4 (23 enodes) 6.121 * * [simplify]: Extracting #0: cost 1 inf + 0 6.121 * * [simplify]: Extracting #1: cost 5 inf + 0 6.121 * * [simplify]: Extracting #2: cost 7 inf + 1 6.121 * * [simplify]: Extracting #3: cost 6 inf + 2 6.121 * * [simplify]: Extracting #4: cost 0 inf + 648 6.121 * [simplify]: Simplified to (fabs (cbrt 2)) 6.121 * [simplify]: Simplified (2 1 1) to (λ (v) (* (* (fabs (cbrt 2)) (* (/ (sqrt (cbrt 2)) 4) (sqrt (- 1 (* 3 (* v v)))))) (- 1 (* v v)))) 6.122 * * * * [progress]: [ 71 / 98 ] simplifiying candidate # 6.122 * [simplify]: Simplifying (/ (sqrt (sqrt 2)) (* (cbrt 4) (cbrt 4))) 6.122 * * [simplify]: iters left: 5 (7 enodes) 6.126 * * [simplify]: iters left: 4 (23 enodes) 6.131 * * [simplify]: iters left: 3 (25 enodes) 6.135 * * [simplify]: Extracting #0: cost 1 inf + 0 6.135 * * [simplify]: Extracting #1: cost 6 inf + 0 6.135 * * [simplify]: Extracting #2: cost 12 inf + 0 6.135 * * [simplify]: Extracting #3: cost 13 inf + 1 6.135 * * [simplify]: Extracting #4: cost 9 inf + 285 6.136 * * [simplify]: Extracting #5: cost 6 inf + 488 6.136 * * [simplify]: Extracting #6: cost 2 inf + 1094 6.136 * * [simplify]: Extracting #7: cost 0 inf + 1538 6.136 * [simplify]: Simplified to (/ (sqrt (sqrt 2)) (* (cbrt 4) (cbrt 4))) 6.136 * [simplify]: Simplified (2 1 1) to (λ (v) (* (* (/ (sqrt (sqrt 2)) (* (cbrt 4) (cbrt 4))) (* (/ (sqrt (sqrt 2)) (cbrt 4)) (sqrt (- 1 (* 3 (* v v)))))) (- 1 (* v v)))) 6.136 * * * * [progress]: [ 72 / 98 ] simplifiying candidate # 6.136 * [simplify]: Simplifying (/ (sqrt (sqrt 2)) (sqrt 4)) 6.136 * * [simplify]: iters left: 4 (6 enodes) 6.140 * * [simplify]: iters left: 3 (18 enodes) 6.143 * * [simplify]: Extracting #0: cost 1 inf + 0 6.143 * * [simplify]: Extracting #1: cost 4 inf + 0 6.143 * * [simplify]: Extracting #2: cost 5 inf + 1 6.143 * * [simplify]: Extracting #3: cost 1 inf + 446 6.143 * * [simplify]: Extracting #4: cost 0 inf + 487 6.143 * [simplify]: Simplified to (/ (sqrt (sqrt 2)) 2) 6.143 * [simplify]: Simplified (2 1 1) to (λ (v) (* (* (/ (sqrt (sqrt 2)) 2) (* (/ (sqrt (sqrt 2)) (sqrt 4)) (sqrt (- 1 (* 3 (* v v)))))) (- 1 (* v v)))) 6.143 * * * * [progress]: [ 73 / 98 ] simplifiying candidate # 6.143 * [simplify]: Simplifying (/ (sqrt (sqrt 2)) 1) 6.144 * * [simplify]: iters left: 4 (5 enodes) 6.145 * * [simplify]: iters left: 3 (15 enodes) 6.148 * * [simplify]: iters left: 2 (17 enodes) 6.151 * * [simplify]: Extracting #0: cost 1 inf + 0 6.151 * * [simplify]: Extracting #1: cost 4 inf + 0 6.151 * * [simplify]: Extracting #2: cost 5 inf + 1 6.151 * * [simplify]: Extracting #3: cost 4 inf + 2 6.152 * * [simplify]: Extracting #4: cost 1 inf + 165 6.152 * * [simplify]: Extracting #5: cost 0 inf + 246 6.152 * [simplify]: Simplified to (sqrt (sqrt 2)) 6.152 * [simplify]: Simplified (2 1 1) to (λ (v) (* (* (sqrt (sqrt 2)) (* (/ (sqrt (sqrt 2)) 4) (sqrt (- 1 (* 3 (* v v)))))) (- 1 (* v v)))) 6.152 * * * * [progress]: [ 74 / 98 ] simplifiying candidate # 6.152 * [simplify]: Simplifying (/ (sqrt 1) (* (cbrt 4) (cbrt 4))) 6.152 * * [simplify]: iters left: 5 (6 enodes) 6.156 * * [simplify]: iters left: 4 (22 enodes) 6.161 * * [simplify]: iters left: 3 (29 enodes) 6.165 * * [simplify]: iters left: 2 (31 enodes) 6.170 * * [simplify]: Extracting #0: cost 1 inf + 0 6.170 * * [simplify]: Extracting #1: cost 7 inf + 0 6.170 * * [simplify]: Extracting #2: cost 11 inf + 1 6.170 * * [simplify]: Extracting #3: cost 10 inf + 2 6.171 * * [simplify]: Extracting #4: cost 2 inf + 935 6.171 * * [simplify]: Extracting #5: cost 0 inf + 1218 6.171 * [simplify]: Simplified to (/ 1 (* (cbrt 4) (cbrt 4))) 6.171 * [simplify]: Simplified (2 1 1) to (λ (v) (* (* (/ 1 (* (cbrt 4) (cbrt 4))) (* (/ (sqrt 2) (cbrt 4)) (sqrt (- 1 (* 3 (* v v)))))) (- 1 (* v v)))) 6.171 * * * * [progress]: [ 75 / 98 ] simplifiying candidate # 6.171 * [simplify]: Simplifying (/ (sqrt 1) (sqrt 4)) 6.171 * * [simplify]: iters left: 3 (5 enodes) 6.174 * * [simplify]: iters left: 2 (18 enodes) 6.178 * * [simplify]: iters left: 1 (21 enodes) 6.185 * * [simplify]: Extracting #0: cost 1 inf + 0 6.185 * * [simplify]: Extracting #1: cost 0 inf + 1 6.185 * [simplify]: Simplified to 1/2 6.185 * [simplify]: Simplified (2 1 1) to (λ (v) (* (* 1/2 (* (/ (sqrt 2) (sqrt 4)) (sqrt (- 1 (* 3 (* v v)))))) (- 1 (* v v)))) 6.185 * * * * [progress]: [ 76 / 98 ] simplifiying candidate # 6.186 * [simplify]: Simplifying (/ (sqrt 1) 1) 6.186 * * [simplify]: iters left: 3 (3 enodes) 6.189 * * [simplify]: iters left: 2 (9 enodes) 6.192 * * [simplify]: iters left: 1 (11 enodes) 6.195 * * [simplify]: Extracting #0: cost 1 inf + 0 6.195 * * [simplify]: Extracting #1: cost 0 inf + 1 6.195 * [simplify]: Simplified to 1 6.195 * [simplify]: Simplified (2 1 1) to (λ (v) (* (* 1 (* (/ (sqrt 2) 4) (sqrt (- 1 (* 3 (* v v)))))) (- 1 (* v v)))) 6.195 * * * * [progress]: [ 77 / 98 ] simplifiying candidate # 6.195 * [simplify]: Simplifying (/ (sqrt (sqrt 2)) (* (cbrt 4) (cbrt 4))) 6.195 * * [simplify]: iters left: 5 (7 enodes) 6.200 * * [simplify]: iters left: 4 (23 enodes) 6.208 * * [simplify]: iters left: 3 (25 enodes) 6.217 * * [simplify]: Extracting #0: cost 1 inf + 0 6.217 * * [simplify]: Extracting #1: cost 6 inf + 0 6.217 * * [simplify]: Extracting #2: cost 12 inf + 0 6.217 * * [simplify]: Extracting #3: cost 13 inf + 1 6.217 * * [simplify]: Extracting #4: cost 9 inf + 285 6.217 * * [simplify]: Extracting #5: cost 6 inf + 488 6.218 * * [simplify]: Extracting #6: cost 2 inf + 1094 6.218 * * [simplify]: Extracting #7: cost 0 inf + 1538 6.218 * [simplify]: Simplified to (/ (sqrt (sqrt 2)) (* (cbrt 4) (cbrt 4))) 6.219 * [simplify]: Simplified (2 1 1) to (λ (v) (* (* (/ (sqrt (sqrt 2)) (* (cbrt 4) (cbrt 4))) (* (/ (sqrt (sqrt 2)) (cbrt 4)) (sqrt (- 1 (* 3 (* v v)))))) (- 1 (* v v)))) 6.219 * * * * [progress]: [ 78 / 98 ] simplifiying candidate # 6.219 * [simplify]: Simplifying (/ (sqrt (sqrt 2)) (sqrt 4)) 6.219 * * [simplify]: iters left: 4 (6 enodes) 6.224 * * [simplify]: iters left: 3 (18 enodes) 6.230 * * [simplify]: Extracting #0: cost 1 inf + 0 6.230 * * [simplify]: Extracting #1: cost 4 inf + 0 6.230 * * [simplify]: Extracting #2: cost 5 inf + 1 6.230 * * [simplify]: Extracting #3: cost 1 inf + 446 6.231 * * [simplify]: Extracting #4: cost 0 inf + 487 6.231 * [simplify]: Simplified to (/ (sqrt (sqrt 2)) 2) 6.231 * [simplify]: Simplified (2 1 1) to (λ (v) (* (* (/ (sqrt (sqrt 2)) 2) (* (/ (sqrt (sqrt 2)) (sqrt 4)) (sqrt (- 1 (* 3 (* v v)))))) (- 1 (* v v)))) 6.231 * * * * [progress]: [ 79 / 98 ] simplifiying candidate # 6.231 * [simplify]: Simplifying (/ (sqrt (sqrt 2)) 1) 6.231 * * [simplify]: iters left: 4 (5 enodes) 6.234 * * [simplify]: iters left: 3 (15 enodes) 6.240 * * [simplify]: iters left: 2 (17 enodes) 6.246 * * [simplify]: Extracting #0: cost 1 inf + 0 6.246 * * [simplify]: Extracting #1: cost 4 inf + 0 6.246 * * [simplify]: Extracting #2: cost 5 inf + 1 6.246 * * [simplify]: Extracting #3: cost 4 inf + 2 6.246 * * [simplify]: Extracting #4: cost 1 inf + 165 6.246 * * [simplify]: Extracting #5: cost 0 inf + 246 6.246 * [simplify]: Simplified to (sqrt (sqrt 2)) 6.246 * [simplify]: Simplified (2 1 1) to (λ (v) (* (* (sqrt (sqrt 2)) (* (/ (sqrt (sqrt 2)) 4) (sqrt (- 1 (* 3 (* v v)))))) (- 1 (* v v)))) 6.246 * * * * [progress]: [ 80 / 98 ] simplifiying candidate # 6.247 * [simplify]: Simplifying (/ 1 (* (cbrt 4) (cbrt 4))) 6.247 * * [simplify]: iters left: 5 (5 enodes) 6.251 * * [simplify]: iters left: 4 (19 enodes) 6.258 * * [simplify]: iters left: 3 (23 enodes) 6.265 * * [simplify]: Extracting #0: cost 1 inf + 0 6.265 * * [simplify]: Extracting #1: cost 6 inf + 0 6.265 * * [simplify]: Extracting #2: cost 9 inf + 1 6.266 * * [simplify]: Extracting #3: cost 1 inf + 852 6.266 * * [simplify]: Extracting #4: cost 0 inf + 974 6.266 * [simplify]: Simplified to (/ 1 (* (cbrt 4) (cbrt 4))) 6.266 * [simplify]: Simplified (2 1 1) to (λ (v) (* (* (/ 1 (* (cbrt 4) (cbrt 4))) (* (/ (sqrt 2) (cbrt 4)) (sqrt (- 1 (* 3 (* v v)))))) (- 1 (* v v)))) 6.266 * * * * [progress]: [ 81 / 98 ] simplifiying candidate # 6.267 * [simplify]: Simplifying (/ 1 (sqrt 4)) 6.267 * * [simplify]: iters left: 3 (4 enodes) 6.271 * * [simplify]: iters left: 2 (16 enodes) 6.277 * * [simplify]: iters left: 1 (18 enodes) 6.283 * * [simplify]: Extracting #0: cost 1 inf + 0 6.283 * * [simplify]: Extracting #1: cost 0 inf + 1 6.283 * [simplify]: Simplified to 1/2 6.283 * [simplify]: Simplified (2 1 1) to (λ (v) (* (* 1/2 (* (/ (sqrt 2) (sqrt 4)) (sqrt (- 1 (* 3 (* v v)))))) (- 1 (* v v)))) 6.283 * * * * [progress]: [ 82 / 98 ] simplifiying candidate # 6.284 * [simplify]: Simplifying (/ 1 1) 6.284 * * [simplify]: iters left: 2 (2 enodes) 6.285 * * [simplify]: iters left: 1 (6 enodes) 6.287 * * [simplify]: Extracting #0: cost 1 inf + 0 6.287 * * [simplify]: Extracting #1: cost 0 inf + 1 6.287 * [simplify]: Simplified to 1 6.287 * [simplify]: Simplified (2 1 1) to (λ (v) (* (* 1 (* (/ (sqrt 2) 4) (sqrt (- 1 (* 3 (* v v)))))) (- 1 (* v v)))) 6.288 * * * * [progress]: [ 83 / 98 ] simplifiying candidate # 6.288 * * * * [progress]: [ 84 / 98 ] simplifiying candidate # 6.288 * [simplify]: Simplifying (sqrt 2) 6.288 * * [simplify]: iters left: 1 (2 enodes) 6.290 * * [simplify]: Extracting #0: cost 1 inf + 0 6.290 * * [simplify]: Extracting #1: cost 3 inf + 0 6.290 * * [simplify]: Extracting #2: cost 2 inf + 1 6.290 * * [simplify]: Extracting #3: cost 0 inf + 83 6.290 * [simplify]: Simplified to (sqrt 2) 6.290 * [simplify]: Simplified (2 1 1) to (λ (v) (* (* (sqrt 2) (* (/ 1 4) (sqrt (- 1 (* 3 (* v v)))))) (- 1 (* v v)))) 6.290 * * * * [progress]: [ 85 / 98 ] simplifiying candidate # 6.290 * [simplify]: Simplifying (sqrt (+ (* 1 1) (+ (* (* 3 (* v v)) (* 3 (* v v))) (* 1 (* 3 (* v v)))))) 6.291 * * [simplify]: iters left: 6 (11 enodes) 6.301 * * [simplify]: iters left: 5 (52 enodes) 6.325 * * [simplify]: iters left: 4 (136 enodes) 6.385 * * [simplify]: iters left: 3 (225 enodes) 6.464 * * [simplify]: iters left: 2 (308 enodes) 6.611 * * [simplify]: iters left: 1 (373 enodes) 6.739 * * [simplify]: Extracting #0: cost 1 inf + 0 6.739 * * [simplify]: Extracting #1: cost 3 inf + 0 6.739 * * [simplify]: Extracting #2: cost 10 inf + 0 6.739 * * [simplify]: Extracting #3: cost 38 inf + 1 6.740 * * [simplify]: Extracting #4: cost 72 inf + 413 6.742 * * [simplify]: Extracting #5: cost 38 inf + 5743 6.746 * * [simplify]: Extracting #6: cost 7 inf + 12323 6.748 * * [simplify]: Extracting #7: cost 0 inf + 13864 6.751 * [simplify]: Simplified to (sqrt (+ 1 (* (* (* 3 v) v) (+ 1 (* (* 3 v) v))))) 6.751 * [simplify]: Simplified (2 1 2) to (λ (v) (* (/ (* (/ (sqrt 2) 4) (sqrt (- (pow 1 3) (pow (* 3 (* v v)) 3)))) (sqrt (+ 1 (* (* (* 3 v) v) (+ 1 (* (* 3 v) v)))))) (- 1 (* v v)))) 6.751 * * * * [progress]: [ 86 / 98 ] simplifiying candidate # 6.751 * [simplify]: Simplifying (sqrt (+ 1 (* 3 (* v v)))) 6.751 * * [simplify]: iters left: 6 (7 enodes) 6.754 * * [simplify]: iters left: 5 (27 enodes) 6.758 * * [simplify]: iters left: 4 (33 enodes) 6.764 * * [simplify]: Extracting #0: cost 1 inf + 0 6.764 * * [simplify]: Extracting #1: cost 3 inf + 0 6.764 * * [simplify]: Extracting #2: cost 6 inf + 0 6.764 * * [simplify]: Extracting #3: cost 10 inf + 1 6.764 * * [simplify]: Extracting #4: cost 8 inf + 86 6.764 * * [simplify]: Extracting #5: cost 4 inf + 374 6.764 * * [simplify]: Extracting #6: cost 1 inf + 742 6.765 * * [simplify]: Extracting #7: cost 0 inf + 905 6.765 * [simplify]: Simplified to (sqrt (+ 1 (* (* v v) 3))) 6.765 * [simplify]: Simplified (2 1 2) to (λ (v) (* (/ (* (/ (sqrt 2) 4) (sqrt (- (* 1 1) (* (* 3 (* v v)) (* 3 (* v v)))))) (sqrt (+ 1 (* (* v v) 3)))) (- 1 (* v v)))) 6.765 * * * * [progress]: [ 87 / 98 ] simplifiying candidate # 6.765 * [simplify]: Simplifying (* (sqrt 2) (sqrt (- 1 (* 3 (* v v))))) 6.765 * * [simplify]: iters left: 6 (10 enodes) 6.768 * * [simplify]: iters left: 5 (38 enodes) 6.776 * * [simplify]: iters left: 4 (58 enodes) 6.786 * * [simplify]: iters left: 3 (76 enodes) 6.809 * * [simplify]: Extracting #0: cost 1 inf + 0 6.809 * * [simplify]: Extracting #1: cost 4 inf + 0 6.810 * * [simplify]: Extracting #2: cost 8 inf + 0 6.810 * * [simplify]: Extracting #3: cost 11 inf + 1 6.810 * * [simplify]: Extracting #4: cost 18 inf + 84 6.810 * * [simplify]: Extracting #5: cost 18 inf + 169 6.811 * * [simplify]: Extracting #6: cost 2 inf + 1725 6.812 * * [simplify]: Extracting #7: cost 0 inf + 1969 6.813 * [simplify]: Simplified to (* (sqrt (+ (* -3 (* v v)) 1)) (sqrt 2)) 6.813 * [simplify]: Simplified (2 1 1) to (λ (v) (* (/ (* (sqrt (+ (* -3 (* v v)) 1)) (sqrt 2)) 4) (- 1 (* v v)))) 6.813 * * * * [progress]: [ 88 / 98 ] simplifiying candidate #real (real->posit16 (* (/ (sqrt 2) 4) (sqrt (- 1 (* 3 (* v v))))))) (- 1 (* v v))))> 6.813 * * * * [progress]: [ 89 / 98 ] simplifiying candidate # 6.813 * * * * [progress]: [ 90 / 98 ] simplifiying candidate # 6.813 * [simplify]: Simplifying (* 3 (pow v 2)) 6.813 * * [simplify]: iters left: 3 (5 enodes) 6.820 * * [simplify]: iters left: 2 (21 enodes) 6.827 * * [simplify]: iters left: 1 (29 enodes) 6.836 * * [simplify]: Extracting #0: cost 1 inf + 0 6.836 * * [simplify]: Extracting #1: cost 6 inf + 0 6.837 * * [simplify]: Extracting #2: cost 6 inf + 43 6.837 * * [simplify]: Extracting #3: cost 0 inf + 333 6.837 * [simplify]: Simplified to (* (* v v) 3) 6.837 * [simplify]: Simplified (2 1 2 1 2) to (λ (v) (* (* (/ (sqrt 2) 4) (sqrt (- 1 (* (* v v) 3)))) (- 1 (* v v)))) 6.837 * * * * [progress]: [ 91 / 98 ] simplifiying candidate # 6.837 * [simplify]: Simplifying (* 3 (pow v 2)) 6.838 * * [simplify]: iters left: 3 (5 enodes) 6.841 * * [simplify]: iters left: 2 (21 enodes) 6.849 * * [simplify]: iters left: 1 (29 enodes) 6.858 * * [simplify]: Extracting #0: cost 1 inf + 0 6.858 * * [simplify]: Extracting #1: cost 6 inf + 0 6.858 * * [simplify]: Extracting #2: cost 6 inf + 43 6.858 * * [simplify]: Extracting #3: cost 0 inf + 333 6.859 * [simplify]: Simplified to (* (* v v) 3) 6.859 * [simplify]: Simplified (2 1 2 1 2) to (λ (v) (* (* (/ (sqrt 2) 4) (sqrt (- 1 (* (* v v) 3)))) (- 1 (* v v)))) 6.859 * * * * [progress]: [ 92 / 98 ] simplifiying candidate # 6.859 * [simplify]: Simplifying (* 3 (pow v 2)) 6.859 * * [simplify]: iters left: 3 (5 enodes) 6.863 * * [simplify]: iters left: 2 (21 enodes) 6.871 * * [simplify]: iters left: 1 (29 enodes) 6.880 * * [simplify]: Extracting #0: cost 1 inf + 0 6.880 * * [simplify]: Extracting #1: cost 6 inf + 0 6.880 * * [simplify]: Extracting #2: cost 6 inf + 43 6.881 * * [simplify]: Extracting #3: cost 0 inf + 333 6.881 * [simplify]: Simplified to (* (* v v) 3) 6.881 * [simplify]: Simplified (2 1 2 1 2) to (λ (v) (* (* (/ (sqrt 2) 4) (sqrt (- 1 (* (* v v) 3)))) (- 1 (* v v)))) 6.881 * * * * [progress]: [ 93 / 98 ] simplifiying candidate # 6.881 * [simplify]: Simplifying (- 1 (+ (* 9/8 (pow v 4)) (* 3/2 (pow v 2)))) 6.881 * * [simplify]: iters left: 6 (12 enodes) 6.888 * * [simplify]: iters left: 5 (52 enodes) 6.898 * * [simplify]: iters left: 4 (73 enodes) 6.912 * * [simplify]: iters left: 3 (117 enodes) 6.932 * * [simplify]: iters left: 2 (156 enodes) 6.969 * * [simplify]: iters left: 1 (207 enodes) 7.024 * * [simplify]: Extracting #0: cost 1 inf + 0 7.024 * * [simplify]: Extracting #1: cost 18 inf + 0 7.024 * * [simplify]: Extracting #2: cost 39 inf + 2 7.024 * * [simplify]: Extracting #3: cost 43 inf + 213 7.025 * * [simplify]: Extracting #4: cost 14 inf + 3555 7.026 * * [simplify]: Extracting #5: cost 0 inf + 5789 7.028 * [simplify]: Simplified to (- (* (* (* v v) (* v v)) -9/8) (- (* 3/2 (* v v)) 1)) 7.028 * [simplify]: Simplified (2 1 2) to (λ (v) (* (* (/ (sqrt 2) 4) (- (* (* (* v v) (* v v)) -9/8) (- (* 3/2 (* v v)) 1))) (- 1 (* v v)))) 7.028 * * * * [progress]: [ 94 / 98 ] simplifiying candidate # 7.028 * [simplify]: Simplifying (- (+ (* 1/2 (/ 1 (* (sqrt -3) v))) (* (sqrt -3) v)) (* 1/8 (/ 1 (* (pow (sqrt -3) 3) (pow v 3))))) 7.028 * * [simplify]: iters left: 6 (17 enodes) 7.035 * * [simplify]: iters left: 5 (83 enodes) 7.067 * * [simplify]: iters left: 4 (179 enodes) 7.109 * * [simplify]: iters left: 3 (426 enodes) 7.314 * * [simplify]: Extracting #0: cost 1 inf + 0 7.314 * * [simplify]: Extracting #1: cost 10 inf + 0 7.314 * * [simplify]: Extracting #2: cost 120 inf + 0 7.316 * * [simplify]: Extracting #3: cost 261 inf + 1073 7.321 * * [simplify]: Extracting #4: cost 248 inf + 10182 7.335 * * [simplify]: Extracting #5: cost 93 inf + 55399 7.358 * * [simplify]: Extracting #6: cost 13 inf + 92512 7.387 * * [simplify]: Extracting #7: cost 0 inf + 99051 7.411 * [simplify]: Simplified to (- (+ (* (sqrt -3) v) (/ (/ 1/2 (sqrt -3)) v)) (/ (/ (/ -1/24 (sqrt -3)) v) (* v v))) 7.411 * [simplify]: Simplified (2 1 2) to (λ (v) (* (* (/ (sqrt 2) 4) (- (+ (* (sqrt -3) v) (/ (/ 1/2 (sqrt -3)) v)) (/ (/ (/ -1/24 (sqrt -3)) v) (* v v)))) (- 1 (* v v)))) 7.411 * * * * [progress]: [ 95 / 98 ] simplifiying candidate # 7.412 * [simplify]: Simplifying (- (* 1/8 (/ 1 (* (pow (sqrt -3) 3) (pow v 3)))) (+ (* 1/2 (/ 1 (* (sqrt -3) v))) (* (sqrt -3) v))) 7.412 * * [simplify]: iters left: 6 (17 enodes) 7.421 * * [simplify]: iters left: 5 (83 enodes) 7.441 * * [simplify]: iters left: 4 (171 enodes) 7.493 * * [simplify]: iters left: 3 (416 enodes) 7.662 * * [simplify]: Extracting #0: cost 1 inf + 0 7.662 * * [simplify]: Extracting #1: cost 15 inf + 0 7.663 * * [simplify]: Extracting #2: cost 124 inf + 0 7.665 * * [simplify]: Extracting #3: cost 256 inf + 783 7.669 * * [simplify]: Extracting #4: cost 231 inf + 11396 7.684 * * [simplify]: Extracting #5: cost 87 inf + 55501 7.711 * * [simplify]: Extracting #6: cost 6 inf + 89983 7.722 * * [simplify]: Extracting #7: cost 0 inf + 92531 7.733 * [simplify]: Simplified to (- (/ -1/2 (* (sqrt -3) v)) (- (* (sqrt -3) v) (/ (/ -1/24 (sqrt -3)) (* v (* v v))))) 7.733 * [simplify]: Simplified (2 1 2) to (λ (v) (* (* (/ (sqrt 2) 4) (- (/ -1/2 (* (sqrt -3) v)) (- (* (sqrt -3) v) (/ (/ -1/24 (sqrt -3)) (* v (* v v)))))) (- 1 (* v v)))) 7.733 * * * * [progress]: [ 96 / 98 ] simplifiying candidate # 7.733 * [simplify]: Simplifying (- (* 1/4 (sqrt 2)) (+ (* 9/32 (* (sqrt 2) (pow v 4))) (* 3/8 (* (sqrt 2) (pow v 2))))) 7.733 * * [simplify]: iters left: 6 (16 enodes) 7.739 * * [simplify]: iters left: 5 (70 enodes) 7.762 * * [simplify]: iters left: 4 (111 enodes) 7.786 * * [simplify]: iters left: 3 (226 enodes) 7.850 * * [simplify]: iters left: 2 (459 enodes) 8.056 * * [simplify]: Extracting #0: cost 1 inf + 0 8.056 * * [simplify]: Extracting #1: cost 23 inf + 0 8.056 * * [simplify]: Extracting #2: cost 137 inf + 0 8.057 * * [simplify]: Extracting #3: cost 200 inf + 579 8.060 * * [simplify]: Extracting #4: cost 113 inf + 13402 8.073 * * [simplify]: Extracting #5: cost 8 inf + 33517 8.083 * * [simplify]: Extracting #6: cost 0 inf + 32281 8.091 * * [simplify]: Extracting #7: cost 0 inf + 31601 8.099 * [simplify]: Simplified to (* (+ 1/4 (* (* v v) (- (* (* v v) -9/32) 3/8))) (sqrt 2)) 8.099 * [simplify]: Simplified (2 1) to (λ (v) (* (* (+ 1/4 (* (* v v) (- (* (* v v) -9/32) 3/8))) (sqrt 2)) (- 1 (* v v)))) 8.099 * * * * [progress]: [ 97 / 98 ] simplifiying candidate # 8.100 * [simplify]: Simplifying (- (+ (* 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))))) 8.100 * * [simplify]: iters left: 6 (21 enodes) 8.112 * * [simplify]: iters left: 5 (98 enodes) 8.144 * * [simplify]: iters left: 4 (237 enodes) 8.233 * * [simplify]: Extracting #0: cost 1 inf + 0 8.233 * * [simplify]: Extracting #1: cost 10 inf + 0 8.234 * * [simplify]: Extracting #2: cost 134 inf + 0 8.235 * * [simplify]: Extracting #3: cost 222 inf + 417 8.240 * * [simplify]: Extracting #4: cost 137 inf + 12959 8.253 * * [simplify]: Extracting #5: cost 40 inf + 37829 8.274 * * [simplify]: Extracting #6: cost 7 inf + 50219 8.290 * * [simplify]: Extracting #7: cost 0 inf + 52861 8.299 * [simplify]: Simplified to (+ (- (* (* v (* (sqrt 2) (sqrt -3))) 1/4) (/ (* (/ -1/96 (sqrt -3)) (/ (sqrt 2) v)) (* v v))) (/ (* (sqrt 2) 1/8) (* v (sqrt -3)))) 8.299 * [simplify]: Simplified (2 1) to (λ (v) (* (+ (- (* (* v (* (sqrt 2) (sqrt -3))) 1/4) (/ (* (/ -1/96 (sqrt -3)) (/ (sqrt 2) v)) (* v v))) (/ (* (sqrt 2) 1/8) (* v (sqrt -3)))) (- 1 (* v v)))) 8.299 * * * * [progress]: [ 98 / 98 ] simplifiying candidate # 8.299 * [simplify]: Simplifying (- (* 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)))))) 8.299 * * [simplify]: iters left: 6 (21 enodes) 8.307 * * [simplify]: iters left: 5 (98 enodes) 8.336 * * [simplify]: iters left: 4 (229 enodes) 8.444 * * [simplify]: Extracting #0: cost 1 inf + 0 8.444 * * [simplify]: Extracting #1: cost 13 inf + 0 8.444 * * [simplify]: Extracting #2: cost 141 inf + 0 8.445 * * [simplify]: Extracting #3: cost 224 inf + 337 8.448 * * [simplify]: Extracting #4: cost 128 inf + 13652 8.455 * * [simplify]: Extracting #5: cost 31 inf + 38579 8.463 * * [simplify]: Extracting #6: cost 2 inf + 50163 8.472 * * [simplify]: Extracting #7: cost 0 inf + 50627 8.483 * [simplify]: Simplified to (- (/ (* (/ -1/96 (sqrt -3)) (/ (/ (sqrt 2) v) v)) v) (- (* v (* (sqrt 2) (* 1/4 (sqrt -3)))) (* (/ (/ (sqrt 2) v) (sqrt -3)) -1/8))) 8.483 * [simplify]: Simplified (2 1) to (λ (v) (* (- (/ (* (/ -1/96 (sqrt -3)) (/ (/ (sqrt 2) v) v)) v) (- (* v (* (sqrt 2) (* 1/4 (sqrt -3)))) (* (/ (/ (sqrt 2) v) (sqrt -3)) -1/8))) (- 1 (* v v)))) 8.484 * * * [progress]: adding candidates to table 9.533 * [progress]: [Phase 3 of 3] Extracting. 9.536 * [simplify]: Simplifying (* (* (/ (sqrt 2) 4) (sqrt (- 1 (* 3 (* v v))))) (- 1 (* v v))) 9.536 * * [simplify]: iters left: 6 (14 enodes) 9.537 * * [simplify]: iters left: 5 (19 enodes) 9.538 * * [simplify]: Extracting #0: cost 1 inf + 0 9.538 * * [simplify]: Extracting #1: cost 3 inf + 0 9.538 * * [simplify]: Extracting #2: cost 7 inf + 0 9.538 * * [simplify]: Extracting #3: cost 10 inf + 1 9.538 * * [simplify]: Extracting #4: cost 8 inf + 126 9.538 * * [simplify]: Extracting #5: cost 8 inf + 127 9.539 * * [simplify]: Extracting #6: cost 5 inf + 251 9.539 * * [simplify]: Extracting #7: cost 3 inf + 456 9.539 * * [simplify]: Extracting #8: cost 0 inf + 1269 9.539 * [simplify]: Simplified to (* (* (sqrt (- 1 (* (* v v) 3))) (/ (sqrt 2) 4)) (- 1 (* v v))) 13.208 * [regime-testing]: Baseline error score: 0.012095872921885669 13.213 * [regime-testing]: Oracle error score: 0.012095872921885669 13.213 * [regime-testing]: End program error score: 0.012095872921885669