0.001 * [progress]: [Phase 1 of 3] Setting up.
0.001 * * * [progress]: [1/2] Preparing points
0.055 * * * [progress]: [2/2] Setting up program.
0.058 * [progress]: [Phase 2 of 3] Improving.
0.058 * * * * [progress]: [ 1 / 1 ] simplifiying candidate #<alt (λ (v) (* (* (/ (sqrt 2) 4) (sqrt (- 1 (* 3 (* v v))))) (- 1 (* v v))))>
0.058 * [simplify]: Simplifying (* (* (/ (sqrt 2) 4) (sqrt (- 1 (* 3 (* v v))))) (- 1 (* v v)))
0.058 * * [simplify]: iters left: 6 (14 enodes)
0.063 * * [simplify]: iters left: 5 (57 enodes)
0.074 * * [simplify]: iters left: 4 (113 enodes)
0.119 * * [simplify]: iters left: 3 (250 enodes)
0.642 * * [simplify]: Extracting #0: cost 1 inf + 0
0.642 * * [simplify]: Extracting #1: cost 38 inf + 0
0.643 * * [simplify]: Extracting #2: cost 96 inf + 359
0.644 * * [simplify]: Extracting #3: cost 86 inf + 2902
0.647 * * [simplify]: Extracting #4: cost 61 inf + 6953
0.655 * * [simplify]: Extracting #5: cost 22 inf + 15369
0.668 * * [simplify]: Extracting #6: cost 0 inf + 21255
0.681 * * [simplify]: Extracting #7: cost 0 inf + 21215
0.693 * [simplify]: Simplified to (* (/ (sqrt 2) (/ 4 (- 1 (* v v)))) (sqrt (fma (* v v) -3 1)))
0.693 * [simplify]: Simplified (2) to (λ (v) (* (/ (sqrt 2) (/ 4 (- 1 (* v v)))) (sqrt (fma (* v v) -3 1))))
0.699 * * [progress]: iteration 1 / 4
0.699 * * * [progress]: picking best candidate
0.701 * * * * [pick]: Picked  #<alt (λ (v) (* (* (/ (sqrt 2) 4) (sqrt (- 1 (* 3 (* v v))))) (- 1 (* v v))))>
0.701 * * * [progress]: localizing error
0.729 * * * [progress]: generating rewritten candidates
0.729 * * * * [progress]: [ 1 / 2 ] rewriting at (2 1 2 1 2)
0.753 * * * * [progress]: [ 2 / 2 ] rewriting at (2 1)
0.794 * * * [progress]: generating series expansions
0.794 * * * * [progress]: [ 1 / 2 ] generating series at (2 1 2 1 2)
0.795 * [backup-simplify]: Simplify (* 3 (* v v)) into (* 3 (pow v 2))
0.795 * [approximate]: Taking taylor expansion of (* 3 (pow v 2)) in (v) around 0
0.795 * [taylor]: Taking taylor expansion of (* 3 (pow v 2)) in v
0.795 * [taylor]: Taking taylor expansion of 3 in v
0.795 * [backup-simplify]: Simplify 3 into 3
0.795 * [taylor]: Taking taylor expansion of (pow v 2) in v
0.795 * [taylor]: Taking taylor expansion of v in v
0.795 * [backup-simplify]: Simplify 0 into 0
0.795 * [backup-simplify]: Simplify 1 into 1
0.795 * [taylor]: Taking taylor expansion of (* 3 (pow v 2)) in v
0.795 * [taylor]: Taking taylor expansion of 3 in v
0.795 * [backup-simplify]: Simplify 3 into 3
0.795 * [taylor]: Taking taylor expansion of (pow v 2) in v
0.795 * [taylor]: Taking taylor expansion of v in v
0.795 * [backup-simplify]: Simplify 0 into 0
0.795 * [backup-simplify]: Simplify 1 into 1
0.796 * [backup-simplify]: Simplify (* 1 1) into 1
0.796 * [backup-simplify]: Simplify (* 3 1) into 3
0.796 * [backup-simplify]: Simplify 3 into 3
0.797 * [backup-simplify]: Simplify (+ (* 1 0) (* 0 1)) into 0
0.798 * [backup-simplify]: Simplify (+ (* 3 0) (* 0 1)) into 0
0.798 * [backup-simplify]: Simplify 0 into 0
0.799 * [backup-simplify]: Simplify (+ (* 1 0) (+ (* 0 0) (* 0 1))) into 0
0.800 * [backup-simplify]: Simplify (+ (* 3 0) (+ (* 0 0) (* 0 1))) into 0
0.800 * [backup-simplify]: Simplify 0 into 0
0.801 * [backup-simplify]: Simplify (+ (* 1 0) (+ (* 0 0) (+ (* 0 0) (* 0 1)))) into 0
0.802 * [backup-simplify]: Simplify (+ (* 3 0) (+ (* 0 0) (+ (* 0 0) (* 0 1)))) into 0
0.802 * [backup-simplify]: Simplify 0 into 0
0.803 * [backup-simplify]: Simplify (+ (* 1 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (* 0 1))))) into 0
0.805 * [backup-simplify]: Simplify (+ (* 3 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (* 0 1))))) into 0
0.805 * [backup-simplify]: Simplify 0 into 0
0.806 * [backup-simplify]: Simplify (+ (* 1 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (* 0 1)))))) into 0
0.807 * [backup-simplify]: Simplify (+ (* 3 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (* 0 1)))))) into 0
0.807 * [backup-simplify]: Simplify 0 into 0
0.809 * [backup-simplify]: Simplify (+ (* 1 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (* 0 1))))))) into 0
0.811 * [backup-simplify]: Simplify (+ (* 3 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (* 0 1))))))) into 0
0.811 * [backup-simplify]: Simplify 0 into 0
0.811 * [backup-simplify]: Simplify (* 3 (pow v 2)) into (* 3 (pow v 2))
0.811 * [backup-simplify]: Simplify (* 3 (* (/ 1 v) (/ 1 v))) into (/ 3 (pow v 2))
0.811 * [approximate]: Taking taylor expansion of (/ 3 (pow v 2)) in (v) around 0
0.811 * [taylor]: Taking taylor expansion of (/ 3 (pow v 2)) in v
0.811 * [taylor]: Taking taylor expansion of 3 in v
0.811 * [backup-simplify]: Simplify 3 into 3
0.811 * [taylor]: Taking taylor expansion of (pow v 2) in v
0.811 * [taylor]: Taking taylor expansion of v in v
0.811 * [backup-simplify]: Simplify 0 into 0
0.811 * [backup-simplify]: Simplify 1 into 1
0.812 * [backup-simplify]: Simplify (* 1 1) into 1
0.812 * [backup-simplify]: Simplify (/ 3 1) into 3
0.812 * [taylor]: Taking taylor expansion of (/ 3 (pow v 2)) in v
0.812 * [taylor]: Taking taylor expansion of 3 in v
0.812 * [backup-simplify]: Simplify 3 into 3
0.812 * [taylor]: Taking taylor expansion of (pow v 2) in v
0.812 * [taylor]: Taking taylor expansion of v in v
0.812 * [backup-simplify]: Simplify 0 into 0
0.812 * [backup-simplify]: Simplify 1 into 1
0.813 * [backup-simplify]: Simplify (* 1 1) into 1
0.813 * [backup-simplify]: Simplify (/ 3 1) into 3
0.813 * [backup-simplify]: Simplify 3 into 3
0.814 * [backup-simplify]: Simplify (+ (* 1 0) (* 0 1)) into 0
0.815 * [backup-simplify]: Simplify (- (/ 0 1) (+ (* 3 (/ 0 1)))) into 0
0.815 * [backup-simplify]: Simplify 0 into 0
0.816 * [backup-simplify]: Simplify (+ (* 1 0) (+ (* 0 0) (* 0 1))) into 0
0.817 * [backup-simplify]: Simplify (- (/ 0 1) (+ (* 3 (/ 0 1)) (* 0 (/ 0 1)))) into 0
0.817 * [backup-simplify]: Simplify 0 into 0
0.818 * [backup-simplify]: Simplify (+ (* 1 0) (+ (* 0 0) (+ (* 0 0) (* 0 1)))) into 0
0.819 * [backup-simplify]: Simplify (- (/ 0 1) (+ (* 3 (/ 0 1)) (* 0 (/ 0 1)) (* 0 (/ 0 1)))) into 0
0.819 * [backup-simplify]: Simplify 0 into 0
0.820 * [backup-simplify]: Simplify (+ (* 1 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (* 0 1))))) into 0
0.821 * [backup-simplify]: Simplify (- (/ 0 1) (+ (* 3 (/ 0 1)) (* 0 (/ 0 1)) (* 0 (/ 0 1)) (* 0 (/ 0 1)))) into 0
0.821 * [backup-simplify]: Simplify 0 into 0
0.823 * [backup-simplify]: Simplify (+ (* 1 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (* 0 1)))))) into 0
0.824 * [backup-simplify]: Simplify (- (/ 0 1) (+ (* 3 (/ 0 1)) (* 0 (/ 0 1)) (* 0 (/ 0 1)) (* 0 (/ 0 1)) (* 0 (/ 0 1)))) into 0
0.824 * [backup-simplify]: Simplify 0 into 0
0.826 * [backup-simplify]: Simplify (+ (* 1 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (* 0 1))))))) into 0
0.827 * [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.827 * [backup-simplify]: Simplify 0 into 0
0.827 * [backup-simplify]: Simplify (* 3 (pow (/ 1 (/ 1 v)) 2)) into (* 3 (pow v 2))
0.827 * [backup-simplify]: Simplify (* 3 (* (/ 1 (- v)) (/ 1 (- v)))) into (/ 3 (pow v 2))
0.828 * [approximate]: Taking taylor expansion of (/ 3 (pow v 2)) in (v) around 0
0.828 * [taylor]: Taking taylor expansion of (/ 3 (pow v 2)) in v
0.828 * [taylor]: Taking taylor expansion of 3 in v
0.828 * [backup-simplify]: Simplify 3 into 3
0.828 * [taylor]: Taking taylor expansion of (pow v 2) in v
0.828 * [taylor]: Taking taylor expansion of v in v
0.828 * [backup-simplify]: Simplify 0 into 0
0.828 * [backup-simplify]: Simplify 1 into 1
0.828 * [backup-simplify]: Simplify (* 1 1) into 1
0.829 * [backup-simplify]: Simplify (/ 3 1) into 3
0.829 * [taylor]: Taking taylor expansion of (/ 3 (pow v 2)) in v
0.829 * [taylor]: Taking taylor expansion of 3 in v
0.829 * [backup-simplify]: Simplify 3 into 3
0.829 * [taylor]: Taking taylor expansion of (pow v 2) in v
0.829 * [taylor]: Taking taylor expansion of v in v
0.829 * [backup-simplify]: Simplify 0 into 0
0.829 * [backup-simplify]: Simplify 1 into 1
0.829 * [backup-simplify]: Simplify (* 1 1) into 1
0.830 * [backup-simplify]: Simplify (/ 3 1) into 3
0.830 * [backup-simplify]: Simplify 3 into 3
0.831 * [backup-simplify]: Simplify (+ (* 1 0) (* 0 1)) into 0
0.832 * [backup-simplify]: Simplify (- (/ 0 1) (+ (* 3 (/ 0 1)))) into 0
0.832 * [backup-simplify]: Simplify 0 into 0
0.833 * [backup-simplify]: Simplify (+ (* 1 0) (+ (* 0 0) (* 0 1))) into 0
0.834 * [backup-simplify]: Simplify (- (/ 0 1) (+ (* 3 (/ 0 1)) (* 0 (/ 0 1)))) into 0
0.834 * [backup-simplify]: Simplify 0 into 0
0.835 * [backup-simplify]: Simplify (+ (* 1 0) (+ (* 0 0) (+ (* 0 0) (* 0 1)))) into 0
0.836 * [backup-simplify]: Simplify (- (/ 0 1) (+ (* 3 (/ 0 1)) (* 0 (/ 0 1)) (* 0 (/ 0 1)))) into 0
0.836 * [backup-simplify]: Simplify 0 into 0
0.837 * [backup-simplify]: Simplify (+ (* 1 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (* 0 1))))) into 0
0.838 * [backup-simplify]: Simplify (- (/ 0 1) (+ (* 3 (/ 0 1)) (* 0 (/ 0 1)) (* 0 (/ 0 1)) (* 0 (/ 0 1)))) into 0
0.838 * [backup-simplify]: Simplify 0 into 0
0.840 * [backup-simplify]: Simplify (+ (* 1 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (* 0 1)))))) into 0
0.841 * [backup-simplify]: Simplify (- (/ 0 1) (+ (* 3 (/ 0 1)) (* 0 (/ 0 1)) (* 0 (/ 0 1)) (* 0 (/ 0 1)) (* 0 (/ 0 1)))) into 0
0.841 * [backup-simplify]: Simplify 0 into 0
0.843 * [backup-simplify]: Simplify (+ (* 1 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (* 0 1))))))) into 0
0.844 * [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.844 * [backup-simplify]: Simplify 0 into 0
0.844 * [backup-simplify]: Simplify (* 3 (pow (/ 1 (/ 1 (- v))) 2)) into (* 3 (pow v 2))
0.844 * * * * [progress]: [ 2 / 2 ] generating series at (2 1)
0.845 * [backup-simplify]: Simplify (* (/ (sqrt 2) 4) (sqrt (- 1 (* 3 (* v v))))) into (* 1/4 (* (sqrt (- 1 (* 3 (pow v 2)))) (sqrt 2)))
0.845 * [approximate]: Taking taylor expansion of (* 1/4 (* (sqrt (- 1 (* 3 (pow v 2)))) (sqrt 2))) in (v) around 0
0.845 * [taylor]: Taking taylor expansion of (* 1/4 (* (sqrt (- 1 (* 3 (pow v 2)))) (sqrt 2))) in v
0.845 * [taylor]: Taking taylor expansion of 1/4 in v
0.845 * [backup-simplify]: Simplify 1/4 into 1/4
0.845 * [taylor]: Taking taylor expansion of (* (sqrt (- 1 (* 3 (pow v 2)))) (sqrt 2)) in v
0.845 * [taylor]: Taking taylor expansion of (sqrt (- 1 (* 3 (pow v 2)))) in v
0.845 * [taylor]: Taking taylor expansion of (- 1 (* 3 (pow v 2))) in v
0.845 * [taylor]: Taking taylor expansion of 1 in v
0.845 * [backup-simplify]: Simplify 1 into 1
0.845 * [taylor]: Taking taylor expansion of (* 3 (pow v 2)) in v
0.845 * [taylor]: Taking taylor expansion of 3 in v
0.845 * [backup-simplify]: Simplify 3 into 3
0.845 * [taylor]: Taking taylor expansion of (pow v 2) in v
0.845 * [taylor]: Taking taylor expansion of v in v
0.845 * [backup-simplify]: Simplify 0 into 0
0.845 * [backup-simplify]: Simplify 1 into 1
0.846 * [backup-simplify]: Simplify (+ 1 0) into 1
0.846 * [backup-simplify]: Simplify (sqrt 1) into 1
0.847 * [backup-simplify]: Simplify (+ 0 0) into 0
0.847 * [backup-simplify]: Simplify (/ 0 (* 2 (sqrt 1))) into 0
0.847 * [taylor]: Taking taylor expansion of (sqrt 2) in v
0.847 * [taylor]: Taking taylor expansion of 2 in v
0.848 * [backup-simplify]: Simplify 2 into 2
0.848 * [backup-simplify]: Simplify (sqrt 2) into (sqrt 2)
0.849 * [backup-simplify]: Simplify (/ 0 (* 2 (sqrt 2))) into 0
0.849 * [taylor]: Taking taylor expansion of (* 1/4 (* (sqrt (- 1 (* 3 (pow v 2)))) (sqrt 2))) in v
0.849 * [taylor]: Taking taylor expansion of 1/4 in v
0.849 * [backup-simplify]: Simplify 1/4 into 1/4
0.849 * [taylor]: Taking taylor expansion of (* (sqrt (- 1 (* 3 (pow v 2)))) (sqrt 2)) in v
0.849 * [taylor]: Taking taylor expansion of (sqrt (- 1 (* 3 (pow v 2)))) in v
0.849 * [taylor]: Taking taylor expansion of (- 1 (* 3 (pow v 2))) in v
0.849 * [taylor]: Taking taylor expansion of 1 in v
0.849 * [backup-simplify]: Simplify 1 into 1
0.849 * [taylor]: Taking taylor expansion of (* 3 (pow v 2)) in v
0.849 * [taylor]: Taking taylor expansion of 3 in v
0.849 * [backup-simplify]: Simplify 3 into 3
0.849 * [taylor]: Taking taylor expansion of (pow v 2) in v
0.849 * [taylor]: Taking taylor expansion of v in v
0.849 * [backup-simplify]: Simplify 0 into 0
0.849 * [backup-simplify]: Simplify 1 into 1
0.849 * [backup-simplify]: Simplify (+ 1 0) into 1
0.850 * [backup-simplify]: Simplify (sqrt 1) into 1
0.850 * [backup-simplify]: Simplify (+ 0 0) into 0
0.851 * [backup-simplify]: Simplify (/ 0 (* 2 (sqrt 1))) into 0
0.851 * [taylor]: Taking taylor expansion of (sqrt 2) in v
0.851 * [taylor]: Taking taylor expansion of 2 in v
0.851 * [backup-simplify]: Simplify 2 into 2
0.851 * [backup-simplify]: Simplify (sqrt 2) into (sqrt 2)
0.852 * [backup-simplify]: Simplify (/ 0 (* 2 (sqrt 2))) into 0
0.857 * [backup-simplify]: Simplify (* 1 (sqrt 2)) into (sqrt 2)
0.858 * [backup-simplify]: Simplify (* 1/4 (sqrt 2)) into (* 1/4 (sqrt 2))
0.859 * [backup-simplify]: Simplify (* 1/4 (sqrt 2)) into (* 1/4 (sqrt 2))
0.860 * [backup-simplify]: Simplify (+ (* 1 0) (* 0 (sqrt 2))) into 0
0.861 * [backup-simplify]: Simplify (+ (* 1/4 0) (* 0 (sqrt 2))) into 0
0.861 * [backup-simplify]: Simplify 0 into 0
0.862 * [backup-simplify]: Simplify (/ (- 0 (pow 0 2) (+)) (* 2 (sqrt 2))) into 0
0.862 * [backup-simplify]: Simplify (* 1 1) into 1
0.863 * [backup-simplify]: Simplify (* 3 1) into 3
0.863 * [backup-simplify]: Simplify (- 3) into -3
0.863 * [backup-simplify]: Simplify (+ 0 -3) into -3
0.865 * [backup-simplify]: Simplify (/ (- -3 (pow 0 2) (+)) (* 2 1)) into -3/2
0.868 * [backup-simplify]: Simplify (+ (* 1 0) (+ (* 0 0) (* -3/2 (sqrt 2)))) into (- (* 3/2 (sqrt 2)))
0.873 * [backup-simplify]: Simplify (+ (* 1/4 (- (* 3/2 (sqrt 2)))) (+ (* 0 0) (* 0 (sqrt 2)))) into (- (* 3/8 (sqrt 2)))
0.875 * [backup-simplify]: Simplify (- (* 3/8 (sqrt 2))) into (- (* 3/8 (sqrt 2)))
0.876 * [backup-simplify]: Simplify (/ (- 0 (+ (* 2 (* 0 0)))) (* 2 (sqrt 2))) into 0
0.877 * [backup-simplify]: Simplify (+ (* 1 0) (* 0 1)) into 0
0.877 * [backup-simplify]: Simplify (+ (* 3 0) (* 0 1)) into 0
0.878 * [backup-simplify]: Simplify (- 0) into 0
0.878 * [backup-simplify]: Simplify (+ 0 0) into 0
0.880 * [backup-simplify]: Simplify (/ (- 0 (+ (* 2 (* 0 -3/2)))) (* 2 1)) into 0
0.881 * [backup-simplify]: Simplify (+ (* 1 0) (+ (* 0 0) (+ (* -3/2 0) (* 0 (sqrt 2))))) into 0
0.883 * [backup-simplify]: Simplify (+ (* 1/4 0) (+ (* 0 (- (* 3/2 (sqrt 2)))) (+ (* 0 0) (* 0 (sqrt 2))))) into 0
0.883 * [backup-simplify]: Simplify 0 into 0
0.884 * [backup-simplify]: Simplify (/ (- 0 (pow 0 2) (+ (* 2 (* 0 0)))) (* 2 (sqrt 2))) into 0
0.885 * [backup-simplify]: Simplify (+ (* 1 0) (+ (* 0 0) (* 0 1))) into 0
0.886 * [backup-simplify]: Simplify (+ (* 3 0) (+ (* 0 0) (* 0 1))) into 0
0.887 * [backup-simplify]: Simplify (- 0) into 0
0.888 * [backup-simplify]: Simplify (+ 0 0) into 0
0.889 * [backup-simplify]: Simplify (/ (- 0 (pow -3/2 2) (+ (* 2 (* 0 0)))) (* 2 1)) into -9/8
0.897 * [backup-simplify]: Simplify (+ (* 1 0) (+ (* 0 0) (+ (* -3/2 0) (+ (* 0 0) (* -9/8 (sqrt 2)))))) into (- (* 9/8 (sqrt 2)))
0.904 * [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.905 * [backup-simplify]: Simplify (- (* 9/32 (sqrt 2))) into (- (* 9/32 (sqrt 2)))
0.910 * [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.911 * [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.911 * [approximate]: Taking taylor expansion of (* 1/4 (* (sqrt 2) (sqrt (- 1 (* 3 (/ 1 (pow v 2))))))) in (v) around 0
0.911 * [taylor]: Taking taylor expansion of (* 1/4 (* (sqrt 2) (sqrt (- 1 (* 3 (/ 1 (pow v 2))))))) in v
0.911 * [taylor]: Taking taylor expansion of 1/4 in v
0.911 * [backup-simplify]: Simplify 1/4 into 1/4
0.911 * [taylor]: Taking taylor expansion of (* (sqrt 2) (sqrt (- 1 (* 3 (/ 1 (pow v 2)))))) in v
0.911 * [taylor]: Taking taylor expansion of (sqrt 2) in v
0.911 * [taylor]: Taking taylor expansion of 2 in v
0.911 * [backup-simplify]: Simplify 2 into 2
0.912 * [backup-simplify]: Simplify (sqrt 2) into (sqrt 2)
0.912 * [backup-simplify]: Simplify (/ 0 (* 2 (sqrt 2))) into 0
0.912 * [taylor]: Taking taylor expansion of (sqrt (- 1 (* 3 (/ 1 (pow v 2))))) in v
0.912 * [taylor]: Taking taylor expansion of (- 1 (* 3 (/ 1 (pow v 2)))) in v
0.912 * [taylor]: Taking taylor expansion of 1 in v
0.912 * [backup-simplify]: Simplify 1 into 1
0.912 * [taylor]: Taking taylor expansion of (* 3 (/ 1 (pow v 2))) in v
0.912 * [taylor]: Taking taylor expansion of 3 in v
0.912 * [backup-simplify]: Simplify 3 into 3
0.912 * [taylor]: Taking taylor expansion of (/ 1 (pow v 2)) in v
0.912 * [taylor]: Taking taylor expansion of (pow v 2) in v
0.912 * [taylor]: Taking taylor expansion of v in v
0.912 * [backup-simplify]: Simplify 0 into 0
0.912 * [backup-simplify]: Simplify 1 into 1
0.913 * [backup-simplify]: Simplify (* 1 1) into 1
0.913 * [backup-simplify]: Simplify (/ 1 1) into 1
0.914 * [backup-simplify]: Simplify (* 3 1) into 3
0.914 * [backup-simplify]: Simplify (- 3) into -3
0.914 * [backup-simplify]: Simplify (+ 0 -3) into -3
0.915 * [backup-simplify]: Simplify (sqrt -3) into (sqrt -3)
0.916 * [backup-simplify]: Simplify (+ (* 1 0) (* 0 1)) into 0
0.916 * [backup-simplify]: Simplify (- (+ (* 1 (/ 0 1)))) into 0
0.917 * [backup-simplify]: Simplify (+ (* 3 0) (* 0 1)) into 0
0.917 * [backup-simplify]: Simplify (- 0) into 0
0.918 * [backup-simplify]: Simplify (+ 0 0) into 0
0.918 * [backup-simplify]: Simplify (/ 0 (* 2 (sqrt -3))) into 0
0.918 * [taylor]: Taking taylor expansion of (* 1/4 (* (sqrt 2) (sqrt (- 1 (* 3 (/ 1 (pow v 2))))))) in v
0.918 * [taylor]: Taking taylor expansion of 1/4 in v
0.919 * [backup-simplify]: Simplify 1/4 into 1/4
0.919 * [taylor]: Taking taylor expansion of (* (sqrt 2) (sqrt (- 1 (* 3 (/ 1 (pow v 2)))))) in v
0.919 * [taylor]: Taking taylor expansion of (sqrt 2) in v
0.919 * [taylor]: Taking taylor expansion of 2 in v
0.919 * [backup-simplify]: Simplify 2 into 2
0.919 * [backup-simplify]: Simplify (sqrt 2) into (sqrt 2)
0.920 * [backup-simplify]: Simplify (/ 0 (* 2 (sqrt 2))) into 0
0.920 * [taylor]: Taking taylor expansion of (sqrt (- 1 (* 3 (/ 1 (pow v 2))))) in v
0.920 * [taylor]: Taking taylor expansion of (- 1 (* 3 (/ 1 (pow v 2)))) in v
0.920 * [taylor]: Taking taylor expansion of 1 in v
0.920 * [backup-simplify]: Simplify 1 into 1
0.920 * [taylor]: Taking taylor expansion of (* 3 (/ 1 (pow v 2))) in v
0.920 * [taylor]: Taking taylor expansion of 3 in v
0.920 * [backup-simplify]: Simplify 3 into 3
0.920 * [taylor]: Taking taylor expansion of (/ 1 (pow v 2)) in v
0.920 * [taylor]: Taking taylor expansion of (pow v 2) in v
0.920 * [taylor]: Taking taylor expansion of v in v
0.920 * [backup-simplify]: Simplify 0 into 0
0.920 * [backup-simplify]: Simplify 1 into 1
0.920 * [backup-simplify]: Simplify (* 1 1) into 1
0.921 * [backup-simplify]: Simplify (/ 1 1) into 1
0.921 * [backup-simplify]: Simplify (* 3 1) into 3
0.922 * [backup-simplify]: Simplify (- 3) into -3
0.922 * [backup-simplify]: Simplify (+ 0 -3) into -3
0.922 * [backup-simplify]: Simplify (sqrt -3) into (sqrt -3)
0.923 * [backup-simplify]: Simplify (+ (* 1 0) (* 0 1)) into 0
0.924 * [backup-simplify]: Simplify (- (+ (* 1 (/ 0 1)))) into 0
0.924 * [backup-simplify]: Simplify (+ (* 3 0) (* 0 1)) into 0
0.925 * [backup-simplify]: Simplify (- 0) into 0
0.925 * [backup-simplify]: Simplify (+ 0 0) into 0
0.926 * [backup-simplify]: Simplify (/ 0 (* 2 (sqrt -3))) into 0
0.927 * [backup-simplify]: Simplify (* (sqrt 2) (sqrt -3)) into (* (sqrt 2) (sqrt -3))
0.929 * [backup-simplify]: Simplify (* 1/4 (* (sqrt 2) (sqrt -3))) into (* 1/4 (* (sqrt 2) (sqrt -3)))
0.931 * [backup-simplify]: Simplify (* 1/4 (* (sqrt 2) (sqrt -3))) into (* 1/4 (* (sqrt 2) (sqrt -3)))
0.932 * [backup-simplify]: Simplify (+ (* (sqrt 2) 0) (* 0 (sqrt -3))) into 0
0.934 * [backup-simplify]: Simplify (+ (* 1/4 0) (* 0 (* (sqrt 2) (sqrt -3)))) into 0
0.934 * [backup-simplify]: Simplify 0 into 0
0.934 * [backup-simplify]: Simplify (+ (* 1 0) (+ (* 0 0) (* 0 1))) into 0
0.935 * [backup-simplify]: Simplify (- (+ (* 1 (/ 0 1)) (* 0 (/ 0 1)))) into 0
0.936 * [backup-simplify]: Simplify (+ (* 3 0) (+ (* 0 0) (* 0 1))) into 0
0.937 * [backup-simplify]: Simplify (- 0) into 0
0.937 * [backup-simplify]: Simplify (+ 1 0) into 1
0.940 * [backup-simplify]: Simplify (/ (- 1 (pow 0 2) (+)) (* 2 (sqrt -3))) into (/ 1/2 (sqrt -3))
0.941 * [backup-simplify]: Simplify (/ (- 0 (pow 0 2) (+)) (* 2 (sqrt 2))) into 0
0.946 * [backup-simplify]: Simplify (+ (* (sqrt 2) (/ 1/2 (sqrt -3))) (+ (* 0 0) (* 0 (sqrt -3)))) into (* 1/2 (/ (sqrt 2) (sqrt -3)))
0.953 * [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.955 * [backup-simplify]: Simplify (* 1/8 (/ (sqrt 2) (sqrt -3))) into (* 1/8 (/ (sqrt 2) (sqrt -3)))
0.956 * [backup-simplify]: Simplify (+ (* 1 0) (+ (* 0 0) (+ (* 0 0) (* 0 1)))) into 0
0.957 * [backup-simplify]: Simplify (- (+ (* 1 (/ 0 1)) (* 0 (/ 0 1)) (* 0 (/ 0 1)))) into 0
0.958 * [backup-simplify]: Simplify (+ (* 3 0) (+ (* 0 0) (+ (* 0 0) (* 0 1)))) into 0
0.958 * [backup-simplify]: Simplify (- 0) into 0
0.958 * [backup-simplify]: Simplify (+ 0 0) into 0
0.960 * [backup-simplify]: Simplify (/ (- 0 (+ (* 2 (* 0 (/ 1/2 (sqrt -3)))))) (* 2 (sqrt -3))) into 0
0.961 * [backup-simplify]: Simplify (/ (- 0 (+ (* 2 (* 0 0)))) (* 2 (sqrt 2))) into 0
0.963 * [backup-simplify]: Simplify (+ (* (sqrt 2) 0) (+ (* 0 (/ 1/2 (sqrt -3))) (+ (* 0 0) (* 0 (sqrt -3))))) into 0
0.965 * [backup-simplify]: Simplify (+ (* 1/4 0) (+ (* 0 (* 1/2 (/ (sqrt 2) (sqrt -3)))) (+ (* 0 0) (* 0 (* (sqrt 2) (sqrt -3)))))) into 0
0.965 * [backup-simplify]: Simplify 0 into 0
0.967 * [backup-simplify]: Simplify (+ (* 1 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (* 0 1))))) into 0
0.968 * [backup-simplify]: Simplify (- (+ (* 1 (/ 0 1)) (* 0 (/ 0 1)) (* 0 (/ 0 1)) (* 0 (/ 0 1)))) into 0
0.969 * [backup-simplify]: Simplify (+ (* 3 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (* 0 1))))) into 0
0.969 * [backup-simplify]: Simplify (- 0) into 0
0.969 * [backup-simplify]: Simplify (+ 0 0) into 0
0.975 * [backup-simplify]: Simplify (/ (- 0 (pow (/ 1/2 (sqrt -3)) 2) (+ (* 2 (* 0 0)))) (* 2 (sqrt -3))) into (/ -1/8 (pow (sqrt -3) 3))
0.977 * [backup-simplify]: Simplify (/ (- 0 (pow 0 2) (+ (* 2 (* 0 0)))) (* 2 (sqrt 2))) into 0
0.982 * [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.990 * [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.993 * [backup-simplify]: Simplify (- (* 1/32 (/ (sqrt 2) (pow (sqrt -3) 3)))) into (- (* 1/32 (/ (sqrt 2) (pow (sqrt -3) 3))))
0.998 * [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.999 * [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.999 * [approximate]: Taking taylor expansion of (* 1/4 (* (sqrt 2) (sqrt (- 1 (* 3 (/ 1 (pow v 2))))))) in (v) around 0
0.999 * [taylor]: Taking taylor expansion of (* 1/4 (* (sqrt 2) (sqrt (- 1 (* 3 (/ 1 (pow v 2))))))) in v
0.999 * [taylor]: Taking taylor expansion of 1/4 in v
0.999 * [backup-simplify]: Simplify 1/4 into 1/4
0.999 * [taylor]: Taking taylor expansion of (* (sqrt 2) (sqrt (- 1 (* 3 (/ 1 (pow v 2)))))) in v
0.999 * [taylor]: Taking taylor expansion of (sqrt 2) in v
0.999 * [taylor]: Taking taylor expansion of 2 in v
0.999 * [backup-simplify]: Simplify 2 into 2
0.999 * [backup-simplify]: Simplify (sqrt 2) into (sqrt 2)
1.000 * [backup-simplify]: Simplify (/ 0 (* 2 (sqrt 2))) into 0
1.000 * [taylor]: Taking taylor expansion of (sqrt (- 1 (* 3 (/ 1 (pow v 2))))) in v
1.000 * [taylor]: Taking taylor expansion of (- 1 (* 3 (/ 1 (pow v 2)))) in v
1.000 * [taylor]: Taking taylor expansion of 1 in v
1.000 * [backup-simplify]: Simplify 1 into 1
1.000 * [taylor]: Taking taylor expansion of (* 3 (/ 1 (pow v 2))) in v
1.000 * [taylor]: Taking taylor expansion of 3 in v
1.000 * [backup-simplify]: Simplify 3 into 3
1.000 * [taylor]: Taking taylor expansion of (/ 1 (pow v 2)) in v
1.000 * [taylor]: Taking taylor expansion of (pow v 2) in v
1.000 * [taylor]: Taking taylor expansion of v in v
1.000 * [backup-simplify]: Simplify 0 into 0
1.000 * [backup-simplify]: Simplify 1 into 1
1.000 * [backup-simplify]: Simplify (* 1 1) into 1
1.001 * [backup-simplify]: Simplify (/ 1 1) into 1
1.001 * [backup-simplify]: Simplify (* 3 1) into 3
1.001 * [backup-simplify]: Simplify (- 3) into -3
1.001 * [backup-simplify]: Simplify (+ 0 -3) into -3
1.002 * [backup-simplify]: Simplify (sqrt -3) into (sqrt -3)
1.002 * [backup-simplify]: Simplify (+ (* 1 0) (* 0 1)) into 0
1.002 * [backup-simplify]: Simplify (- (+ (* 1 (/ 0 1)))) into 0
1.003 * [backup-simplify]: Simplify (+ (* 3 0) (* 0 1)) into 0
1.003 * [backup-simplify]: Simplify (- 0) into 0
1.003 * [backup-simplify]: Simplify (+ 0 0) into 0
1.004 * [backup-simplify]: Simplify (/ 0 (* 2 (sqrt -3))) into 0
1.004 * [taylor]: Taking taylor expansion of (* 1/4 (* (sqrt 2) (sqrt (- 1 (* 3 (/ 1 (pow v 2))))))) in v
1.004 * [taylor]: Taking taylor expansion of 1/4 in v
1.004 * [backup-simplify]: Simplify 1/4 into 1/4
1.004 * [taylor]: Taking taylor expansion of (* (sqrt 2) (sqrt (- 1 (* 3 (/ 1 (pow v 2)))))) in v
1.004 * [taylor]: Taking taylor expansion of (sqrt 2) in v
1.004 * [taylor]: Taking taylor expansion of 2 in v
1.004 * [backup-simplify]: Simplify 2 into 2
1.004 * [backup-simplify]: Simplify (sqrt 2) into (sqrt 2)
1.004 * [backup-simplify]: Simplify (/ 0 (* 2 (sqrt 2))) into 0
1.004 * [taylor]: Taking taylor expansion of (sqrt (- 1 (* 3 (/ 1 (pow v 2))))) in v
1.004 * [taylor]: Taking taylor expansion of (- 1 (* 3 (/ 1 (pow v 2)))) in v
1.004 * [taylor]: Taking taylor expansion of 1 in v
1.004 * [backup-simplify]: Simplify 1 into 1
1.004 * [taylor]: Taking taylor expansion of (* 3 (/ 1 (pow v 2))) in v
1.004 * [taylor]: Taking taylor expansion of 3 in v
1.004 * [backup-simplify]: Simplify 3 into 3
1.004 * [taylor]: Taking taylor expansion of (/ 1 (pow v 2)) in v
1.004 * [taylor]: Taking taylor expansion of (pow v 2) in v
1.005 * [taylor]: Taking taylor expansion of v in v
1.005 * [backup-simplify]: Simplify 0 into 0
1.005 * [backup-simplify]: Simplify 1 into 1
1.005 * [backup-simplify]: Simplify (* 1 1) into 1
1.005 * [backup-simplify]: Simplify (/ 1 1) into 1
1.005 * [backup-simplify]: Simplify (* 3 1) into 3
1.005 * [backup-simplify]: Simplify (- 3) into -3
1.006 * [backup-simplify]: Simplify (+ 0 -3) into -3
1.006 * [backup-simplify]: Simplify (sqrt -3) into (sqrt -3)
1.006 * [backup-simplify]: Simplify (+ (* 1 0) (* 0 1)) into 0
1.007 * [backup-simplify]: Simplify (- (+ (* 1 (/ 0 1)))) into 0
1.007 * [backup-simplify]: Simplify (+ (* 3 0) (* 0 1)) into 0
1.007 * [backup-simplify]: Simplify (- 0) into 0
1.008 * [backup-simplify]: Simplify (+ 0 0) into 0
1.008 * [backup-simplify]: Simplify (/ 0 (* 2 (sqrt -3))) into 0
1.009 * [backup-simplify]: Simplify (* (sqrt 2) (sqrt -3)) into (* (sqrt 2) (sqrt -3))
1.010 * [backup-simplify]: Simplify (* 1/4 (* (sqrt 2) (sqrt -3))) into (* 1/4 (* (sqrt 2) (sqrt -3)))
1.012 * [backup-simplify]: Simplify (* 1/4 (* (sqrt 2) (sqrt -3))) into (* 1/4 (* (sqrt 2) (sqrt -3)))
1.013 * [backup-simplify]: Simplify (+ (* (sqrt 2) 0) (* 0 (sqrt -3))) into 0
1.015 * [backup-simplify]: Simplify (+ (* 1/4 0) (* 0 (* (sqrt 2) (sqrt -3)))) into 0
1.015 * [backup-simplify]: Simplify 0 into 0
1.015 * [backup-simplify]: Simplify (+ (* 1 0) (+ (* 0 0) (* 0 1))) into 0
1.016 * [backup-simplify]: Simplify (- (+ (* 1 (/ 0 1)) (* 0 (/ 0 1)))) into 0
1.018 * [backup-simplify]: Simplify (+ (* 3 0) (+ (* 0 0) (* 0 1))) into 0
1.018 * [backup-simplify]: Simplify (- 0) into 0
1.018 * [backup-simplify]: Simplify (+ 1 0) into 1
1.021 * [backup-simplify]: Simplify (/ (- 1 (pow 0 2) (+)) (* 2 (sqrt -3))) into (/ 1/2 (sqrt -3))
1.022 * [backup-simplify]: Simplify (/ (- 0 (pow 0 2) (+)) (* 2 (sqrt 2))) into 0
1.026 * [backup-simplify]: Simplify (+ (* (sqrt 2) (/ 1/2 (sqrt -3))) (+ (* 0 0) (* 0 (sqrt -3)))) into (* 1/2 (/ (sqrt 2) (sqrt -3)))
1.033 * [backup-simplify]: Simplify (+ (* 1/4 (* 1/2 (/ (sqrt 2) (sqrt -3)))) (+ (* 0 0) (* 0 (* (sqrt 2) (sqrt -3))))) into (* 1/8 (/ (sqrt 2) (sqrt -3)))
1.035 * [backup-simplify]: Simplify (* 1/8 (/ (sqrt 2) (sqrt -3))) into (* 1/8 (/ (sqrt 2) (sqrt -3)))
1.036 * [backup-simplify]: Simplify (+ (* 1 0) (+ (* 0 0) (+ (* 0 0) (* 0 1)))) into 0
1.037 * [backup-simplify]: Simplify (- (+ (* 1 (/ 0 1)) (* 0 (/ 0 1)) (* 0 (/ 0 1)))) into 0
1.038 * [backup-simplify]: Simplify (+ (* 3 0) (+ (* 0 0) (+ (* 0 0) (* 0 1)))) into 0
1.038 * [backup-simplify]: Simplify (- 0) into 0
1.039 * [backup-simplify]: Simplify (+ 0 0) into 0
1.040 * [backup-simplify]: Simplify (/ (- 0 (+ (* 2 (* 0 (/ 1/2 (sqrt -3)))))) (* 2 (sqrt -3))) into 0
1.041 * [backup-simplify]: Simplify (/ (- 0 (+ (* 2 (* 0 0)))) (* 2 (sqrt 2))) into 0
1.043 * [backup-simplify]: Simplify (+ (* (sqrt 2) 0) (+ (* 0 (/ 1/2 (sqrt -3))) (+ (* 0 0) (* 0 (sqrt -3))))) into 0
1.046 * [backup-simplify]: Simplify (+ (* 1/4 0) (+ (* 0 (* 1/2 (/ (sqrt 2) (sqrt -3)))) (+ (* 0 0) (* 0 (* (sqrt 2) (sqrt -3)))))) into 0
1.046 * [backup-simplify]: Simplify 0 into 0
1.047 * [backup-simplify]: Simplify (+ (* 1 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (* 0 1))))) into 0
1.048 * [backup-simplify]: Simplify (- (+ (* 1 (/ 0 1)) (* 0 (/ 0 1)) (* 0 (/ 0 1)) (* 0 (/ 0 1)))) into 0
1.049 * [backup-simplify]: Simplify (+ (* 3 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (* 0 1))))) into 0
1.050 * [backup-simplify]: Simplify (- 0) into 0
1.050 * [backup-simplify]: Simplify (+ 0 0) into 0
1.056 * [backup-simplify]: Simplify (/ (- 0 (pow (/ 1/2 (sqrt -3)) 2) (+ (* 2 (* 0 0)))) (* 2 (sqrt -3))) into (/ -1/8 (pow (sqrt -3) 3))
1.058 * [backup-simplify]: Simplify (/ (- 0 (pow 0 2) (+ (* 2 (* 0 0)))) (* 2 (sqrt 2))) into 0
1.065 * [backup-simplify]: Simplify (+ (* (sqrt 2) (/ -1/8 (pow (sqrt -3) 3))) (+ (* 0 0) (+ (* 0 (/ 1/2 (sqrt -3))) (+ (* 0 0) (* 0 (sqrt -3)))))) into (- (* 1/8 (/ (sqrt 2) (pow (sqrt -3) 3))))
1.077 * [backup-simplify]: Simplify (+ (* 1/4 (- (* 1/8 (/ (sqrt 2) (pow (sqrt -3) 3))))) (+ (* 0 0) (+ (* 0 (* 1/2 (/ (sqrt 2) (sqrt -3)))) (+ (* 0 0) (* 0 (* (sqrt 2) (sqrt -3))))))) into (- (* 1/32 (/ (sqrt 2) (pow (sqrt -3) 3))))
1.081 * [backup-simplify]: Simplify (- (* 1/32 (/ (sqrt 2) (pow (sqrt -3) 3)))) into (- (* 1/32 (/ (sqrt 2) (pow (sqrt -3) 3))))
1.091 * [backup-simplify]: Simplify (+ (* (- (* 1/32 (/ (sqrt 2) (pow (sqrt -3) 3)))) (pow (/ 1 (- v)) 3)) (+ (* (* 1/8 (/ (sqrt 2) (sqrt -3))) (/ 1 (- v))) (* (* 1/4 (* (sqrt 2) (sqrt -3))) (/ 1 (/ 1 (- v)))))) into (- (* 1/32 (/ (sqrt 2) (* (pow v 3) (pow (sqrt -3) 3)))) (+ (* 1/4 (* (sqrt 2) (* v (sqrt -3)))) (* 1/8 (/ (sqrt 2) (* v (sqrt -3))))))
1.091 * * * [progress]: simplifying candidates
1.091 * * * * [progress]: [ 1 / 83 ] simplifiying candidate #<alt (λ (v) (* (* (/ (sqrt 2) 4) (sqrt (- 1 (log1p (expm1 (* 3 (* v v))))))) (- 1 (* v v))))>
1.091 * * * * [progress]: [ 2 / 83 ] simplifiying candidate #<alt (λ (v) (* (* (/ (sqrt 2) 4) (sqrt (- 1 (expm1 (log1p (* 3 (* v v))))))) (- 1 (* v v))))>
1.091 * * * * [progress]: [ 3 / 83 ] simplifiying candidate #<alt (λ (v) (* (* (/ (sqrt 2) 4) (sqrt (- 1 (pow (* 3 (* v v)) 1)))) (- 1 (* v v))))>
1.091 * [simplify]: Simplifying (* 3 (* v v))
1.091 * * [simplify]: iters left: 4 (4 enodes)
1.094 * * [simplify]: iters left: 3 (15 enodes)
1.098 * * [simplify]: iters left: 2 (19 enodes)
1.104 * * [simplify]: Extracting #0: cost 1 inf + 0
1.104 * * [simplify]: Extracting #1: cost 6 inf + 0
1.104 * * [simplify]: Extracting #2: cost 5 inf + 43
1.104 * * [simplify]: Extracting #3: cost 0 inf + 332
1.104 * [simplify]: Simplified to (* 3 (* v v))
1.104 * [simplify]: Simplified (2 1 2 1 2 1) to (λ (v) (* (* (/ (sqrt 2) 4) (sqrt (- 1 (pow (* 3 (* v v)) 1)))) (- 1 (* v v))))
1.105 * * * * [progress]: [ 4 / 83 ] simplifiying candidate #<alt (λ (v) (* (* (/ (sqrt 2) 4) (sqrt (- 1 (pow (* 3 (* v v)) 1)))) (- 1 (* v v))))>
1.105 * [simplify]: Simplifying (* 3 (* v v))
1.105 * * [simplify]: iters left: 4 (4 enodes)
1.107 * * [simplify]: iters left: 3 (15 enodes)
1.112 * * [simplify]: iters left: 2 (19 enodes)
1.120 * * [simplify]: Extracting #0: cost 1 inf + 0
1.120 * * [simplify]: Extracting #1: cost 6 inf + 0
1.120 * * [simplify]: Extracting #2: cost 5 inf + 43
1.121 * * [simplify]: Extracting #3: cost 0 inf + 332
1.121 * [simplify]: Simplified to (* 3 (* v v))
1.121 * [simplify]: Simplified (2 1 2 1 2 1) to (λ (v) (* (* (/ (sqrt 2) 4) (sqrt (- 1 (pow (* 3 (* v v)) 1)))) (- 1 (* v v))))
1.121 * * * * [progress]: [ 5 / 83 ] simplifiying candidate #<alt (λ (v) (* (* (/ (sqrt 2) 4) (sqrt (- 1 (pow (* 3 (* v v)) 1)))) (- 1 (* v v))))>
1.121 * * * * [progress]: [ 6 / 83 ] simplifiying candidate #<alt (λ (v) (* (* (/ (sqrt 2) 4) (sqrt (- 1 (exp (+ (log 3) (+ (log v) (log v))))))) (- 1 (* v v))))>
1.121 * [simplify]: Simplifying (+ (log 3) (+ (log v) (log v)))
1.121 * * [simplify]: iters left: 5 (6 enodes)
1.125 * * [simplify]: iters left: 4 (21 enodes)
1.132 * * [simplify]: iters left: 3 (25 enodes)
1.139 * * [simplify]: Extracting #0: cost 1 inf + 0
1.139 * * [simplify]: Extracting #1: cost 6 inf + 0
1.139 * * [simplify]: Extracting #2: cost 12 inf + 0
1.139 * * [simplify]: Extracting #3: cost 10 inf + 2
1.140 * * [simplify]: Extracting #4: cost 0 inf + 1316
1.140 * [simplify]: Simplified to (+ (log 3) (+ (log v) (log v)))
1.140 * [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))))
1.140 * * * * [progress]: [ 7 / 83 ] simplifiying candidate #<alt (λ (v) (* (* (/ (sqrt 2) 4) (sqrt (- 1 (exp (+ (log 3) (log (* v v))))))) (- 1 (* v v))))>
1.141 * [simplify]: Simplifying (+ (log 3) (log (* v v)))
1.141 * * [simplify]: iters left: 5 (6 enodes)
1.144 * * [simplify]: iters left: 4 (21 enodes)
1.151 * * [simplify]: iters left: 3 (27 enodes)
1.160 * * [simplify]: iters left: 2 (32 enodes)
1.169 * * [simplify]: Extracting #0: cost 1 inf + 0
1.169 * * [simplify]: Extracting #1: cost 6 inf + 0
1.169 * * [simplify]: Extracting #2: cost 13 inf + 0
1.169 * * [simplify]: Extracting #3: cost 9 inf + 185
1.169 * * [simplify]: Extracting #4: cost 4 inf + 741
1.170 * * [simplify]: Extracting #5: cost 0 inf + 1398
1.170 * [simplify]: Simplified to (+ (log 3) (+ (log v) (log v)))
1.170 * [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))))
1.171 * * * * [progress]: [ 8 / 83 ] simplifiying candidate #<alt (λ (v) (* (* (/ (sqrt 2) 4) (sqrt (- 1 (exp (log (* 3 (* v v))))))) (- 1 (* v v))))>
1.171 * * * * [progress]: [ 9 / 83 ] simplifiying candidate #<alt (λ (v) (* (* (/ (sqrt 2) 4) (sqrt (- 1 (log (exp (* 3 (* v v))))))) (- 1 (* v v))))>
1.171 * * * * [progress]: [ 10 / 83 ] simplifiying candidate #<alt (λ (v) (* (* (/ (sqrt 2) 4) (sqrt (- 1 (cbrt (* (* (* 3 3) 3) (* (* (* v v) v) (* (* v v) v))))))) (- 1 (* v v))))>
1.171 * [simplify]: Simplifying (* (* (* 3 3) 3) (* (* (* v v) v) (* (* v v) v)))
1.171 * * [simplify]: iters left: 6 (8 enodes)
1.177 * * [simplify]: iters left: 5 (38 enodes)
1.196 * * [simplify]: iters left: 4 (96 enodes)
1.234 * * [simplify]: iters left: 3 (265 enodes)
1.365 * * [simplify]: Extracting #0: cost 1 inf + 0
1.365 * * [simplify]: Extracting #1: cost 54 inf + 0
1.366 * * [simplify]: Extracting #2: cost 83 inf + 1839
1.371 * * [simplify]: Extracting #3: cost 30 inf + 7514
1.377 * * [simplify]: Extracting #4: cost 8 inf + 12317
1.380 * * [simplify]: Extracting #5: cost 0 inf + 14739
1.384 * [simplify]: Simplified to (* 27 (* (* v (* v v)) (* v (* v v))))
1.384 * [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.384 * * * * [progress]: [ 11 / 83 ] simplifiying candidate #<alt (λ (v) (* (* (/ (sqrt 2) 4) (sqrt (- 1 (cbrt (* (* (* 3 3) 3) (* (* (* v v) (* v v)) (* v v))))))) (- 1 (* v v))))>
1.384 * [simplify]: Simplifying (* (* (* 3 3) 3) (* (* (* v v) (* v v)) (* v v)))
1.384 * * [simplify]: iters left: 6 (8 enodes)
1.387 * * [simplify]: iters left: 5 (39 enodes)
1.399 * * [simplify]: iters left: 4 (96 enodes)
1.427 * * [simplify]: iters left: 3 (269 enodes)
1.541 * * [simplify]: Extracting #0: cost 1 inf + 0
1.541 * * [simplify]: Extracting #1: cost 72 inf + 0
1.542 * * [simplify]: Extracting #2: cost 120 inf + 818
1.544 * * [simplify]: Extracting #3: cost 39 inf + 12504
1.548 * * [simplify]: Extracting #4: cost 1 inf + 19795
1.553 * * [simplify]: Extracting #5: cost 0 inf + 20047
1.557 * [simplify]: Simplified to (* (* v v) (* (* (* v v) (* v v)) 27))
1.557 * [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.557 * * * * [progress]: [ 12 / 83 ] simplifiying candidate #<alt (λ (v) (* (* (/ (sqrt 2) 4) (sqrt (- 1 (* (* (cbrt (* 3 (* v v))) (cbrt (* 3 (* v v)))) (cbrt (* 3 (* v v))))))) (- 1 (* v v))))>
1.557 * * * * [progress]: [ 13 / 83 ] simplifiying candidate #<alt (λ (v) (* (* (/ (sqrt 2) 4) (sqrt (- 1 (cbrt (* (* (* 3 (* v v)) (* 3 (* v v))) (* 3 (* v v))))))) (- 1 (* v v))))>
1.557 * * * * [progress]: [ 14 / 83 ] simplifiying candidate #<alt (λ (v) (* (* (/ (sqrt 2) 4) (sqrt (- 1 (* (sqrt (* 3 (* v v))) (sqrt (* 3 (* v v))))))) (- 1 (* v v))))>
1.557 * * * * [progress]: [ 15 / 83 ] simplifiying candidate #<alt (λ (v) (* (* (/ (sqrt 2) 4) (sqrt (- 1 (* 1 (* 3 (* v v)))))) (- 1 (* v v))))>
1.557 * * * * [progress]: [ 16 / 83 ] simplifiying candidate #<alt (λ (v) (* (* (/ (sqrt 2) 4) (sqrt (- 1 (* (* (sqrt 3) v) (* (sqrt 3) v))))) (- 1 (* v v))))>
1.557 * [simplify]: Simplifying (* (sqrt 3) v)
1.557 * * [simplify]: iters left: 3 (4 enodes)
1.559 * * [simplify]: iters left: 2 (13 enodes)
1.561 * * [simplify]: Extracting #0: cost 1 inf + 0
1.561 * * [simplify]: Extracting #1: cost 4 inf + 0
1.561 * * [simplify]: Extracting #2: cost 5 inf + 1
1.561 * * [simplify]: Extracting #3: cost 4 inf + 2
1.561 * * [simplify]: Extracting #4: cost 0 inf + 248
1.561 * [simplify]: Simplified to (* v (sqrt 3))
1.561 * [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.561 * [simplify]: Simplifying (* (sqrt 3) v)
1.561 * * [simplify]: iters left: 3 (4 enodes)
1.563 * * [simplify]: iters left: 2 (13 enodes)
1.565 * * [simplify]: Extracting #0: cost 1 inf + 0
1.565 * * [simplify]: Extracting #1: cost 4 inf + 0
1.565 * * [simplify]: Extracting #2: cost 5 inf + 1
1.565 * * [simplify]: Extracting #3: cost 4 inf + 2
1.565 * * [simplify]: Extracting #4: cost 0 inf + 248
1.565 * [simplify]: Simplified to (* v (sqrt 3))
1.565 * [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.565 * * * * [progress]: [ 17 / 83 ] simplifiying candidate #<alt (λ (v) (* (* (/ (sqrt 2) 4) (sqrt (- 1 (* (* 3 v) v)))) (- 1 (* v v))))>
1.565 * * * * [progress]: [ 18 / 83 ] simplifiying candidate #<alt (λ (v) (* (* (/ (sqrt 2) 4) (sqrt (- 1 (* (* (cbrt 3) (cbrt 3)) (* (cbrt 3) (* v v)))))) (- 1 (* v v))))>
1.565 * [simplify]: Simplifying (* (cbrt 3) (cbrt 3))
1.565 * * [simplify]: iters left: 3 (3 enodes)
1.566 * * [simplify]: iters left: 2 (9 enodes)
1.569 * * [simplify]: Extracting #0: cost 1 inf + 0
1.569 * * [simplify]: Extracting #1: cost 3 inf + 0
1.569 * * [simplify]: Extracting #2: cost 5 inf + 0
1.570 * * [simplify]: Extracting #3: cost 4 inf + 1
1.570 * * [simplify]: Extracting #4: cost 0 inf + 405
1.570 * [simplify]: Simplified to (* (cbrt 3) (cbrt 3))
1.570 * [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.570 * * * * [progress]: [ 19 / 83 ] simplifiying candidate #<alt (λ (v) (* (* (/ (sqrt 2) 4) (sqrt (- 1 (* (sqrt 3) (* (sqrt 3) (* v v)))))) (- 1 (* v v))))>
1.570 * [simplify]: Simplifying (sqrt 3)
1.570 * * [simplify]: iters left: 1 (2 enodes)
1.572 * * [simplify]: Extracting #0: cost 1 inf + 0
1.572 * * [simplify]: Extracting #1: cost 3 inf + 0
1.572 * * [simplify]: Extracting #2: cost 2 inf + 1
1.572 * * [simplify]: Extracting #3: cost 0 inf + 83
1.572 * [simplify]: Simplified to (sqrt 3)
1.572 * [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.572 * * * * [progress]: [ 20 / 83 ] simplifiying candidate #<alt (λ (v) (* (* (/ (sqrt 2) 4) (sqrt (- 1 (* 1 (* 3 (* v v)))))) (- 1 (* v v))))>
1.572 * * * * [progress]: [ 21 / 83 ] simplifiying candidate #<alt (λ (v) (* (* (/ (sqrt 2) 4) (sqrt (- 1 (posit16->real (real->posit16 (* 3 (* v v))))))) (- 1 (* v v))))>
1.573 * * * * [progress]: [ 22 / 83 ] simplifiying candidate #<alt (λ (v) (* (* (/ (sqrt 2) 4) (sqrt (- 1 (* (* v v) 3)))) (- 1 (* v v))))>
1.573 * * * * [progress]: [ 23 / 83 ] simplifiying candidate #<alt (λ (v) (* (log1p (expm1 (* (/ (sqrt 2) 4) (sqrt (- 1 (* 3 (* v v))))))) (- 1 (* v v))))>
1.573 * * * * [progress]: [ 24 / 83 ] simplifiying candidate #<alt (λ (v) (* (expm1 (log1p (* (/ (sqrt 2) 4) (sqrt (- 1 (* 3 (* v v))))))) (- 1 (* v v))))>
1.573 * * * * [progress]: [ 25 / 83 ] simplifiying candidate #<alt (λ (v) (* (pow (* (/ (sqrt 2) 4) (sqrt (- 1 (* 3 (* v v))))) 1) (- 1 (* v v))))>
1.573 * [simplify]: Simplifying (* (/ (sqrt 2) 4) (sqrt (- 1 (* 3 (* v v)))))
1.573 * * [simplify]: iters left: 6 (12 enodes)
1.580 * * [simplify]: iters left: 5 (46 enodes)
1.596 * * [simplify]: iters left: 4 (72 enodes)
1.622 * * [simplify]: iters left: 3 (98 enodes)
1.649 * * [simplify]: Extracting #0: cost 1 inf + 0
1.649 * * [simplify]: Extracting #1: cost 8 inf + 0
1.649 * * [simplify]: Extracting #2: cost 14 inf + 1
1.649 * * [simplify]: Extracting #3: cost 25 inf + 2
1.650 * * [simplify]: Extracting #4: cost 21 inf + 391
1.651 * * [simplify]: Extracting #5: cost 3 inf + 2301
1.652 * * [simplify]: Extracting #6: cost 0 inf + 2862
1.653 * [simplify]: Simplified to (* (sqrt (fma (* v v) -3 1)) (/ (sqrt 2) 4))
1.653 * [simplify]: Simplified (2 1 1) to (λ (v) (* (pow (* (sqrt (fma (* v v) -3 1)) (/ (sqrt 2) 4)) 1) (- 1 (* v v))))
1.653 * * * * [progress]: [ 26 / 83 ] simplifiying candidate #<alt (λ (v) (* (pow (* (/ (sqrt 2) 4) (sqrt (- 1 (* 3 (* v v))))) 1) (- 1 (* v v))))>
1.653 * * * * [progress]: [ 27 / 83 ] simplifiying candidate #<alt (λ (v) (* (exp (+ (- (log (sqrt 2)) (log 4)) (log (sqrt (- 1 (* 3 (* v v))))))) (- 1 (* v v))))>
1.654 * [simplify]: Simplifying (+ (- (log (sqrt 2)) (log 4)) (log (sqrt (- 1 (* 3 (* v v))))))
1.654 * * [simplify]: iters left: 6 (15 enodes)
1.662 * * [simplify]: iters left: 5 (57 enodes)
1.681 * * [simplify]: iters left: 4 (91 enodes)
1.711 * * [simplify]: iters left: 3 (134 enodes)
1.752 * * [simplify]: iters left: 2 (141 enodes)
1.786 * * [simplify]: iters left: 1 (145 enodes)
1.816 * * [simplify]: Extracting #0: cost 1 inf + 0
1.816 * * [simplify]: Extracting #1: cost 15 inf + 0
1.816 * * [simplify]: Extracting #2: cost 30 inf + 0
1.816 * * [simplify]: Extracting #3: cost 30 inf + 294
1.816 * * [simplify]: Extracting #4: cost 38 inf + 448
1.816 * * [simplify]: Extracting #5: cost 34 inf + 1532
1.817 * * [simplify]: Extracting #6: cost 8 inf + 6075
1.819 * * [simplify]: Extracting #7: cost 1 inf + 7953
1.820 * * [simplify]: Extracting #8: cost 0 inf + 8352
1.821 * [simplify]: Simplified to (+ (log (sqrt (fma (* v v) -3 1))) (- (log (sqrt 2)) (log 4)))
1.821 * [simplify]: Simplified (2 1 1) to (λ (v) (* (exp (+ (log (sqrt (fma (* v v) -3 1))) (- (log (sqrt 2)) (log 4)))) (- 1 (* v v))))
1.822 * * * * [progress]: [ 28 / 83 ] simplifiying candidate #<alt (λ (v) (* (exp (+ (log (/ (sqrt 2) 4)) (log (sqrt (- 1 (* 3 (* v v))))))) (- 1 (* v v))))>
1.822 * [simplify]: Simplifying (+ (log (/ (sqrt 2) 4)) (log (sqrt (- 1 (* 3 (* v v))))))
1.822 * * [simplify]: iters left: 6 (14 enodes)
1.826 * * [simplify]: iters left: 5 (53 enodes)
1.836 * * [simplify]: iters left: 4 (83 enodes)
1.853 * * [simplify]: iters left: 3 (122 enodes)
1.875 * * [simplify]: iters left: 2 (138 enodes)
1.900 * * [simplify]: iters left: 1 (141 enodes)
1.932 * * [simplify]: Extracting #0: cost 1 inf + 0
1.932 * * [simplify]: Extracting #1: cost 13 inf + 0
1.933 * * [simplify]: Extracting #2: cost 26 inf + 0
1.933 * * [simplify]: Extracting #3: cost 27 inf + 254
1.933 * * [simplify]: Extracting #4: cost 36 inf + 407
1.933 * * [simplify]: Extracting #5: cost 30 inf + 1265
1.935 * * [simplify]: Extracting #6: cost 5 inf + 5786
1.937 * * [simplify]: Extracting #7: cost 0 inf + 6763
1.940 * [simplify]: Simplified to (+ (log (sqrt (fma -3 (* v v) 1))) (log (/ (sqrt 2) 4)))
1.940 * [simplify]: Simplified (2 1 1) to (λ (v) (* (exp (+ (log (sqrt (fma -3 (* v v) 1))) (log (/ (sqrt 2) 4)))) (- 1 (* v v))))
1.940 * * * * [progress]: [ 29 / 83 ] simplifiying candidate #<alt (λ (v) (* (exp (log (* (/ (sqrt 2) 4) (sqrt (- 1 (* 3 (* v v))))))) (- 1 (* v v))))>
1.940 * * * * [progress]: [ 30 / 83 ] simplifiying candidate #<alt (λ (v) (* (log (exp (* (/ (sqrt 2) 4) (sqrt (- 1 (* 3 (* v v))))))) (- 1 (* v v))))>
1.940 * * * * [progress]: [ 31 / 83 ] simplifiying candidate #<alt (λ (v) (* (cbrt (* (/ (* (* (sqrt 2) (sqrt 2)) (sqrt 2)) (* (* 4 4) 4)) (* (* (sqrt (- 1 (* 3 (* v v)))) (sqrt (- 1 (* 3 (* v v))))) (sqrt (- 1 (* 3 (* v v))))))) (- 1 (* v v))))>
1.940 * [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))))))
1.941 * * [simplify]: iters left: 6 (18 enodes)
1.953 * * [simplify]: iters left: 5 (74 enodes)
1.973 * * [simplify]: iters left: 4 (177 enodes)
2.065 * * [simplify]: Extracting #0: cost 1 inf + 0
2.066 * * [simplify]: Extracting #1: cost 43 inf + 0
2.066 * * [simplify]: Extracting #2: cost 138 inf + 6
2.068 * * [simplify]: Extracting #3: cost 173 inf + 1364
2.072 * * [simplify]: Extracting #4: cost 111 inf + 9525
2.083 * * [simplify]: Extracting #5: cost 64 inf + 18636
2.097 * * [simplify]: Extracting #6: cost 7 inf + 33508
2.113 * * [simplify]: Extracting #7: cost 0 inf + 35401
2.129 * [simplify]: Simplified to (* (sqrt (fma (* v -3) v 1)) (/ (* (fma (* v -3) v 1) (sqrt 2)) 32))
2.129 * [simplify]: Simplified (2 1 1) to (λ (v) (* (cbrt (* (sqrt (fma (* v -3) v 1)) (/ (* (fma (* v -3) v 1) (sqrt 2)) 32))) (- 1 (* v v))))
2.129 * * * * [progress]: [ 32 / 83 ] simplifiying candidate #<alt (λ (v) (* (cbrt (* (* (* (/ (sqrt 2) 4) (/ (sqrt 2) 4)) (/ (sqrt 2) 4)) (* (* (sqrt (- 1 (* 3 (* v v)))) (sqrt (- 1 (* 3 (* v v))))) (sqrt (- 1 (* 3 (* v v))))))) (- 1 (* v v))))>
2.130 * [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.130 * * [simplify]: iters left: 6 (16 enodes)
2.140 * * [simplify]: iters left: 5 (66 enodes)
2.155 * * [simplify]: iters left: 4 (157 enodes)
2.235 * * [simplify]: iters left: 3 (475 enodes)
2.922 * * [simplify]: Extracting #0: cost 1 inf + 0
2.922 * * [simplify]: Extracting #1: cost 77 inf + 0
2.923 * * [simplify]: Extracting #2: cost 356 inf + 49
2.927 * * [simplify]: Extracting #3: cost 512 inf + 9160
2.947 * * [simplify]: Extracting #4: cost 217 inf + 75830
3.011 * * [simplify]: Extracting #5: cost 4 inf + 135130
3.042 * * [simplify]: Extracting #6: cost 0 inf + 129541
3.088 * * [simplify]: Extracting #7: cost 0 inf + 129489
3.133 * [simplify]: Simplified to (* (* (fma (* -3 v) v 1) (sqrt (fma (* -3 v) v 1))) (* 1/32 (sqrt 2)))
3.133 * [simplify]: Simplified (2 1 1) to (λ (v) (* (cbrt (* (* (fma (* -3 v) v 1) (sqrt (fma (* -3 v) v 1))) (* 1/32 (sqrt 2)))) (- 1 (* v v))))
3.133 * * * * [progress]: [ 33 / 83 ] simplifiying candidate #<alt (λ (v) (* (* (* (cbrt (* (/ (sqrt 2) 4) (sqrt (- 1 (* 3 (* v v)))))) (cbrt (* (/ (sqrt 2) 4) (sqrt (- 1 (* 3 (* v v))))))) (cbrt (* (/ (sqrt 2) 4) (sqrt (- 1 (* 3 (* v v))))))) (- 1 (* v v))))>
3.133 * * * * [progress]: [ 34 / 83 ] simplifiying candidate #<alt (λ (v) (* (cbrt (* (* (* (/ (sqrt 2) 4) (sqrt (- 1 (* 3 (* v v))))) (* (/ (sqrt 2) 4) (sqrt (- 1 (* 3 (* v v)))))) (* (/ (sqrt 2) 4) (sqrt (- 1 (* 3 (* v v))))))) (- 1 (* v v))))>
3.133 * * * * [progress]: [ 35 / 83 ] simplifiying candidate #<alt (λ (v) (* (* (sqrt (* (/ (sqrt 2) 4) (sqrt (- 1 (* 3 (* v v)))))) (sqrt (* (/ (sqrt 2) 4) (sqrt (- 1 (* 3 (* v v))))))) (- 1 (* v v))))>
3.134 * * * * [progress]: [ 36 / 83 ] simplifiying candidate #<alt (λ (v) (* (/ (* (sqrt 2) (sqrt (- (pow 1 3) (pow (* 3 (* v v)) 3)))) (* 4 (sqrt (+ (* 1 1) (+ (* (* 3 (* v v)) (* 3 (* v v))) (* 1 (* 3 (* v v)))))))) (- 1 (* v v))))>
3.134 * [simplify]: Simplifying (* (sqrt 2) (sqrt (- (pow 1 3) (pow (* 3 (* v v)) 3))))
3.134 * * [simplify]: iters left: 6 (12 enodes)
3.143 * * [simplify]: iters left: 5 (55 enodes)
3.161 * * [simplify]: iters left: 4 (132 enodes)
3.220 * * [simplify]: iters left: 3 (429 enodes)
3.487 * * [simplify]: Extracting #0: cost 1 inf + 0
3.487 * * [simplify]: Extracting #1: cost 4 inf + 0
3.487 * * [simplify]: Extracting #2: cost 8 inf + 0
3.487 * * [simplify]: Extracting #3: cost 17 inf + 1
3.488 * * [simplify]: Extracting #4: cost 96 inf + 43
3.489 * * [simplify]: Extracting #5: cost 182 inf + 2215
3.493 * * [simplify]: Extracting #6: cost 67 inf + 21556
3.502 * * [simplify]: Extracting #7: cost 7 inf + 34956
3.514 * * [simplify]: Extracting #8: cost 0 inf + 38671
3.523 * [simplify]: Simplified to (* (sqrt (- 1 (* (* (* v (* v v)) 27) (* v (* v v))))) (sqrt 2))
3.523 * [simplify]: Simplified (2 1 1) to (λ (v) (* (/ (* (sqrt (- 1 (* (* (* v (* v v)) 27) (* v (* v v))))) (sqrt 2)) (* 4 (sqrt (+ (* 1 1) (+ (* (* 3 (* v v)) (* 3 (* v v))) (* 1 (* 3 (* v v)))))))) (- 1 (* v v))))
3.524 * [simplify]: Simplifying (* 4 (sqrt (+ (* 1 1) (+ (* (* 3 (* v v)) (* 3 (* v v))) (* 1 (* 3 (* v v)))))))
3.524 * * [simplify]: iters left: 6 (13 enodes)
3.529 * * [simplify]: iters left: 5 (61 enodes)
3.553 * * [simplify]: iters left: 4 (156 enodes)
3.622 * * [simplify]: iters left: 3 (323 enodes)
3.734 * * [simplify]: iters left: 2 (479 enodes)
3.909 * * [simplify]: Extracting #0: cost 1 inf + 0
3.909 * * [simplify]: Extracting #1: cost 4 inf + 0
3.909 * * [simplify]: Extracting #2: cost 5 inf + 1
3.909 * * [simplify]: Extracting #3: cost 28 inf + 1
3.909 * * [simplify]: Extracting #4: cost 43 inf + 996
3.911 * * [simplify]: Extracting #5: cost 18 inf + 5141
3.914 * * [simplify]: Extracting #6: cost 9 inf + 5353
3.917 * * [simplify]: Extracting #7: cost 1 inf + 6937
3.920 * * [simplify]: Extracting #8: cost 0 inf + 7149
3.923 * [simplify]: Simplified to (* (sqrt (+ (fma (* 3 (* v v)) (* 3 (* v v)) (* 3 (* v v))) 1)) 4)
3.923 * [simplify]: Simplified (2 1 2) to (λ (v) (* (/ (* (sqrt (- 1 (* (* (* v (* v v)) 27) (* v (* v v))))) (sqrt 2)) (* (sqrt (+ (fma (* 3 (* v v)) (* 3 (* v v)) (* 3 (* v v))) 1)) 4)) (- 1 (* v v))))
3.923 * * * * [progress]: [ 37 / 83 ] simplifiying candidate #<alt (λ (v) (* (/ (* (sqrt 2) (sqrt (- (* 1 1) (* (* 3 (* v v)) (* 3 (* v v)))))) (* 4 (sqrt (+ 1 (* 3 (* v v)))))) (- 1 (* v v))))>
3.923 * [simplify]: Simplifying (* (sqrt 2) (sqrt (- (* 1 1) (* (* 3 (* v v)) (* 3 (* v v))))))
3.923 * * [simplify]: iters left: 6 (12 enodes)
3.928 * * [simplify]: iters left: 5 (51 enodes)
3.943 * * [simplify]: iters left: 4 (103 enodes)
3.988 * * [simplify]: iters left: 3 (219 enodes)
4.097 * * [simplify]: iters left: 2 (360 enodes)
4.218 * * [simplify]: iters left: 1 (420 enodes)
4.370 * * [simplify]: Extracting #0: cost 1 inf + 0
4.370 * * [simplify]: Extracting #1: cost 4 inf + 0
4.370 * * [simplify]: Extracting #2: cost 8 inf + 0
4.370 * * [simplify]: Extracting #3: cost 21 inf + 1
4.371 * * [simplify]: Extracting #4: cost 73 inf + 86
4.372 * * [simplify]: Extracting #5: cost 115 inf + 864
4.375 * * [simplify]: Extracting #6: cost 75 inf + 6065
4.382 * * [simplify]: Extracting #7: cost 32 inf + 16078
4.386 * * [simplify]: Extracting #8: cost 5 inf + 24470
4.390 * * [simplify]: Extracting #9: cost 0 inf + 25901
4.394 * [simplify]: Simplified to (* (sqrt (fma (* (* v v) -9) (* v v) 1)) (sqrt 2))
4.394 * [simplify]: Simplified (2 1 1) to (λ (v) (* (/ (* (sqrt (fma (* (* v v) -9) (* v v) 1)) (sqrt 2)) (* 4 (sqrt (+ 1 (* 3 (* v v)))))) (- 1 (* v v))))
4.395 * [simplify]: Simplifying (* 4 (sqrt (+ 1 (* 3 (* v v)))))
4.395 * * [simplify]: iters left: 6 (9 enodes)
4.398 * * [simplify]: iters left: 5 (34 enodes)
4.403 * * [simplify]: iters left: 4 (43 enodes)
4.410 * * [simplify]: Extracting #0: cost 1 inf + 0
4.410 * * [simplify]: Extracting #1: cost 4 inf + 0
4.410 * * [simplify]: Extracting #2: cost 5 inf + 1
4.410 * * [simplify]: Extracting #3: cost 12 inf + 1
4.410 * * [simplify]: Extracting #4: cost 11 inf + 46
4.410 * * [simplify]: Extracting #5: cost 5 inf + 545
4.410 * * [simplify]: Extracting #6: cost 0 inf + 1164
4.411 * [simplify]: Simplified to (* (sqrt (fma 3 (* v v) 1)) 4)
4.411 * [simplify]: Simplified (2 1 2) to (λ (v) (* (/ (* (sqrt (fma (* (* v v) -9) (* v v) 1)) (sqrt 2)) (* (sqrt (fma 3 (* v v) 1)) 4)) (- 1 (* v v))))
4.411 * * * * [progress]: [ 38 / 83 ] simplifiying candidate #<alt (λ (v) (* (* 1 (* (/ (sqrt 2) 4) (sqrt (- 1 (* 3 (* v v)))))) (- 1 (* v v))))>
4.411 * * * * [progress]: [ 39 / 83 ] simplifiying candidate #<alt (λ (v) (* (* (* (sqrt (/ (sqrt 2) 4)) (sqrt (sqrt (- 1 (* 3 (* v v)))))) (* (sqrt (/ (sqrt 2) 4)) (sqrt (sqrt (- 1 (* 3 (* v v))))))) (- 1 (* v v))))>
4.411 * [simplify]: Simplifying (* (sqrt (/ (sqrt 2) 4)) (sqrt (sqrt (- 1 (* 3 (* v v))))))
4.411 * * [simplify]: iters left: 6 (14 enodes)
4.416 * * [simplify]: iters left: 5 (50 enodes)
4.426 * * [simplify]: iters left: 4 (70 enodes)
4.453 * * [simplify]: iters left: 3 (94 enodes)
4.474 * * [simplify]: Extracting #0: cost 1 inf + 0
4.474 * * [simplify]: Extracting #1: cost 4 inf + 0
4.475 * * [simplify]: Extracting #2: cost 8 inf + 0
4.475 * * [simplify]: Extracting #3: cost 13 inf + 0
4.475 * * [simplify]: Extracting #4: cost 26 inf + 1
4.475 * * [simplify]: Extracting #5: cost 20 inf + 457
4.475 * * [simplify]: Extracting #6: cost 3 inf + 2226
4.476 * * [simplify]: Extracting #7: cost 0 inf + 2826
4.477 * [simplify]: Simplified to (* (sqrt (/ (sqrt 2) 4)) (sqrt (sqrt (fma (* v v) -3 1))))
4.477 * [simplify]: Simplified (2 1 1) to (λ (v) (* (* (* (sqrt (/ (sqrt 2) 4)) (sqrt (sqrt (fma (* v v) -3 1)))) (* (sqrt (/ (sqrt 2) 4)) (sqrt (sqrt (- 1 (* 3 (* v v))))))) (- 1 (* v v))))
4.477 * [simplify]: Simplifying (* (sqrt (/ (sqrt 2) 4)) (sqrt (sqrt (- 1 (* 3 (* v v))))))
4.477 * * [simplify]: iters left: 6 (14 enodes)
4.482 * * [simplify]: iters left: 5 (50 enodes)
4.491 * * [simplify]: iters left: 4 (70 enodes)
4.505 * * [simplify]: iters left: 3 (94 enodes)
4.532 * * [simplify]: Extracting #0: cost 1 inf + 0
4.532 * * [simplify]: Extracting #1: cost 4 inf + 0
4.532 * * [simplify]: Extracting #2: cost 8 inf + 0
4.532 * * [simplify]: Extracting #3: cost 13 inf + 0
4.532 * * [simplify]: Extracting #4: cost 26 inf + 1
4.533 * * [simplify]: Extracting #5: cost 20 inf + 457
4.533 * * [simplify]: Extracting #6: cost 3 inf + 2226
4.535 * * [simplify]: Extracting #7: cost 0 inf + 2826
4.536 * [simplify]: Simplified to (* (sqrt (/ (sqrt 2) 4)) (sqrt (sqrt (fma (* v v) -3 1))))
4.536 * [simplify]: Simplified (2 1 2) to (λ (v) (* (* (* (sqrt (/ (sqrt 2) 4)) (sqrt (sqrt (- 1 (* 3 (* v v)))))) (* (sqrt (/ (sqrt 2) 4)) (sqrt (sqrt (fma (* v v) -3 1))))) (- 1 (* v v))))
4.536 * * * * [progress]: [ 40 / 83 ] simplifiying candidate #<alt (λ (v) (* (* (* (sqrt (/ (sqrt 2) 4)) (sqrt (sqrt (- 1 (* 3 (* v v)))))) (* (sqrt (/ (sqrt 2) 4)) (sqrt (sqrt (- 1 (* 3 (* v v))))))) (- 1 (* v v))))>
4.536 * [simplify]: Simplifying (* (sqrt (/ (sqrt 2) 4)) (sqrt (sqrt (- 1 (* 3 (* v v))))))
4.536 * * [simplify]: iters left: 6 (14 enodes)
4.545 * * [simplify]: iters left: 5 (50 enodes)
4.561 * * [simplify]: iters left: 4 (70 enodes)
4.581 * * [simplify]: iters left: 3 (94 enodes)
4.596 * * [simplify]: Extracting #0: cost 1 inf + 0
4.596 * * [simplify]: Extracting #1: cost 4 inf + 0
4.596 * * [simplify]: Extracting #2: cost 8 inf + 0
4.596 * * [simplify]: Extracting #3: cost 13 inf + 0
4.596 * * [simplify]: Extracting #4: cost 26 inf + 1
4.596 * * [simplify]: Extracting #5: cost 20 inf + 457
4.596 * * [simplify]: Extracting #6: cost 3 inf + 2226
4.597 * * [simplify]: Extracting #7: cost 0 inf + 2826
4.598 * [simplify]: Simplified to (* (sqrt (/ (sqrt 2) 4)) (sqrt (sqrt (fma (* v v) -3 1))))
4.598 * [simplify]: Simplified (2 1 1) to (λ (v) (* (* (* (sqrt (/ (sqrt 2) 4)) (sqrt (sqrt (fma (* v v) -3 1)))) (* (sqrt (/ (sqrt 2) 4)) (sqrt (sqrt (- 1 (* 3 (* v v))))))) (- 1 (* v v))))
4.598 * [simplify]: Simplifying (* (sqrt (/ (sqrt 2) 4)) (sqrt (sqrt (- 1 (* 3 (* v v))))))
4.598 * * [simplify]: iters left: 6 (14 enodes)
4.602 * * [simplify]: iters left: 5 (50 enodes)
4.619 * * [simplify]: iters left: 4 (70 enodes)
4.640 * * [simplify]: iters left: 3 (94 enodes)
4.654 * * [simplify]: Extracting #0: cost 1 inf + 0
4.654 * * [simplify]: Extracting #1: cost 4 inf + 0
4.654 * * [simplify]: Extracting #2: cost 8 inf + 0
4.654 * * [simplify]: Extracting #3: cost 13 inf + 0
4.654 * * [simplify]: Extracting #4: cost 26 inf + 1
4.654 * * [simplify]: Extracting #5: cost 20 inf + 457
4.655 * * [simplify]: Extracting #6: cost 3 inf + 2226
4.655 * * [simplify]: Extracting #7: cost 0 inf + 2826
4.656 * [simplify]: Simplified to (* (sqrt (/ (sqrt 2) 4)) (sqrt (sqrt (fma (* v v) -3 1))))
4.656 * [simplify]: Simplified (2 1 2) to (λ (v) (* (* (* (sqrt (/ (sqrt 2) 4)) (sqrt (sqrt (- 1 (* 3 (* v v)))))) (* (sqrt (/ (sqrt 2) 4)) (sqrt (sqrt (fma (* v v) -3 1))))) (- 1 (* v v))))
4.656 * * * * [progress]: [ 41 / 83 ] simplifiying candidate #<alt (λ (v) (* (* (* (/ (sqrt (sqrt 2)) (sqrt 4)) (sqrt (sqrt (- 1 (* 3 (* v v)))))) (* (/ (sqrt (sqrt 2)) (sqrt 4)) (sqrt (sqrt (- 1 (* 3 (* v v))))))) (- 1 (* v v))))>
4.656 * [simplify]: Simplifying (* (/ (sqrt (sqrt 2)) (sqrt 4)) (sqrt (sqrt (- 1 (* 3 (* v v))))))
4.656 * * [simplify]: iters left: 6 (15 enodes)
4.662 * * [simplify]: iters left: 5 (55 enodes)
4.674 * * [simplify]: iters left: 4 (82 enodes)
4.693 * * [simplify]: iters left: 3 (108 enodes)
4.708 * * [simplify]: Extracting #0: cost 1 inf + 0
4.708 * * [simplify]: Extracting #1: cost 8 inf + 0
4.708 * * [simplify]: Extracting #2: cost 14 inf + 1
4.708 * * [simplify]: Extracting #3: cost 16 inf + 42
4.708 * * [simplify]: Extracting #4: cost 23 inf + 487
4.708 * * [simplify]: Extracting #5: cost 23 inf + 615
4.709 * * [simplify]: Extracting #6: cost 10 inf + 1662
4.709 * * [simplify]: Extracting #7: cost 0 inf + 3855
4.710 * [simplify]: Simplified to (* (/ (sqrt (sqrt 2)) 2) (sqrt (sqrt (fma (* v v) -3 1))))
4.710 * [simplify]: Simplified (2 1 1) to (λ (v) (* (* (* (/ (sqrt (sqrt 2)) 2) (sqrt (sqrt (fma (* v v) -3 1)))) (* (/ (sqrt (sqrt 2)) (sqrt 4)) (sqrt (sqrt (- 1 (* 3 (* v v))))))) (- 1 (* v v))))
4.710 * [simplify]: Simplifying (* (/ (sqrt (sqrt 2)) (sqrt 4)) (sqrt (sqrt (- 1 (* 3 (* v v))))))
4.711 * * [simplify]: iters left: 6 (15 enodes)
4.716 * * [simplify]: iters left: 5 (55 enodes)
4.725 * * [simplify]: iters left: 4 (82 enodes)
4.738 * * [simplify]: iters left: 3 (108 enodes)
4.759 * * [simplify]: Extracting #0: cost 1 inf + 0
4.759 * * [simplify]: Extracting #1: cost 8 inf + 0
4.759 * * [simplify]: Extracting #2: cost 14 inf + 1
4.759 * * [simplify]: Extracting #3: cost 16 inf + 42
4.759 * * [simplify]: Extracting #4: cost 23 inf + 487
4.760 * * [simplify]: Extracting #5: cost 23 inf + 615
4.760 * * [simplify]: Extracting #6: cost 10 inf + 1662
4.761 * * [simplify]: Extracting #7: cost 0 inf + 3855
4.762 * [simplify]: Simplified to (* (/ (sqrt (sqrt 2)) 2) (sqrt (sqrt (fma (* v v) -3 1))))
4.762 * [simplify]: Simplified (2 1 2) to (λ (v) (* (* (* (/ (sqrt (sqrt 2)) (sqrt 4)) (sqrt (sqrt (- 1 (* 3 (* v v)))))) (* (/ (sqrt (sqrt 2)) 2) (sqrt (sqrt (fma (* v v) -3 1))))) (- 1 (* v v))))
4.762 * * * * [progress]: [ 42 / 83 ] simplifiying candidate #<alt (λ (v) (* (* (* (/ (sqrt (sqrt 2)) (sqrt 4)) (sqrt (sqrt (- 1 (* 3 (* v v)))))) (* (/ (sqrt (sqrt 2)) (sqrt 4)) (sqrt (sqrt (- 1 (* 3 (* v v))))))) (- 1 (* v v))))>
4.762 * [simplify]: Simplifying (* (/ (sqrt (sqrt 2)) (sqrt 4)) (sqrt (sqrt (- 1 (* 3 (* v v))))))
4.762 * * [simplify]: iters left: 6 (15 enodes)
4.767 * * [simplify]: iters left: 5 (55 enodes)
4.778 * * [simplify]: iters left: 4 (82 enodes)
4.803 * * [simplify]: iters left: 3 (108 enodes)
4.832 * * [simplify]: Extracting #0: cost 1 inf + 0
4.833 * * [simplify]: Extracting #1: cost 8 inf + 0
4.833 * * [simplify]: Extracting #2: cost 14 inf + 1
4.833 * * [simplify]: Extracting #3: cost 16 inf + 42
4.833 * * [simplify]: Extracting #4: cost 23 inf + 487
4.833 * * [simplify]: Extracting #5: cost 23 inf + 615
4.834 * * [simplify]: Extracting #6: cost 10 inf + 1662
4.835 * * [simplify]: Extracting #7: cost 0 inf + 3855
4.837 * [simplify]: Simplified to (* (/ (sqrt (sqrt 2)) 2) (sqrt (sqrt (fma (* v v) -3 1))))
4.837 * [simplify]: Simplified (2 1 1) to (λ (v) (* (* (* (/ (sqrt (sqrt 2)) 2) (sqrt (sqrt (fma (* v v) -3 1)))) (* (/ (sqrt (sqrt 2)) (sqrt 4)) (sqrt (sqrt (- 1 (* 3 (* v v))))))) (- 1 (* v v))))
4.837 * [simplify]: Simplifying (* (/ (sqrt (sqrt 2)) (sqrt 4)) (sqrt (sqrt (- 1 (* 3 (* v v))))))
4.838 * * [simplify]: iters left: 6 (15 enodes)
4.848 * * [simplify]: iters left: 5 (55 enodes)
4.866 * * [simplify]: iters left: 4 (82 enodes)
4.894 * * [simplify]: iters left: 3 (108 enodes)
4.923 * * [simplify]: Extracting #0: cost 1 inf + 0
4.924 * * [simplify]: Extracting #1: cost 8 inf + 0
4.924 * * [simplify]: Extracting #2: cost 14 inf + 1
4.924 * * [simplify]: Extracting #3: cost 16 inf + 42
4.924 * * [simplify]: Extracting #4: cost 23 inf + 487
4.924 * * [simplify]: Extracting #5: cost 23 inf + 615
4.925 * * [simplify]: Extracting #6: cost 10 inf + 1662
4.927 * * [simplify]: Extracting #7: cost 0 inf + 3855
4.928 * [simplify]: Simplified to (* (/ (sqrt (sqrt 2)) 2) (sqrt (sqrt (fma (* v v) -3 1))))
4.929 * [simplify]: Simplified (2 1 2) to (λ (v) (* (* (* (/ (sqrt (sqrt 2)) (sqrt 4)) (sqrt (sqrt (- 1 (* 3 (* v v)))))) (* (/ (sqrt (sqrt 2)) 2) (sqrt (sqrt (fma (* v v) -3 1))))) (- 1 (* v v))))
4.929 * * * * [progress]: [ 43 / 83 ] simplifiying candidate #<alt (λ (v) (* (* (* (/ (sqrt (sqrt 2)) (sqrt 4)) (sqrt (sqrt (- 1 (* 3 (* v v)))))) (* (/ (sqrt (sqrt 2)) (sqrt 4)) (sqrt (sqrt (- 1 (* 3 (* v v))))))) (- 1 (* v v))))>
4.929 * [simplify]: Simplifying (* (/ (sqrt (sqrt 2)) (sqrt 4)) (sqrt (sqrt (- 1 (* 3 (* v v))))))
4.929 * * [simplify]: iters left: 6 (15 enodes)
4.940 * * [simplify]: iters left: 5 (55 enodes)
4.958 * * [simplify]: iters left: 4 (82 enodes)
4.984 * * [simplify]: iters left: 3 (108 enodes)
5.014 * * [simplify]: Extracting #0: cost 1 inf + 0
5.014 * * [simplify]: Extracting #1: cost 8 inf + 0
5.015 * * [simplify]: Extracting #2: cost 14 inf + 1
5.015 * * [simplify]: Extracting #3: cost 16 inf + 42
5.015 * * [simplify]: Extracting #4: cost 23 inf + 487
5.015 * * [simplify]: Extracting #5: cost 23 inf + 615
5.016 * * [simplify]: Extracting #6: cost 10 inf + 1662
5.017 * * [simplify]: Extracting #7: cost 0 inf + 3855
5.019 * [simplify]: Simplified to (* (/ (sqrt (sqrt 2)) 2) (sqrt (sqrt (fma (* v v) -3 1))))
5.019 * [simplify]: Simplified (2 1 1) to (λ (v) (* (* (* (/ (sqrt (sqrt 2)) 2) (sqrt (sqrt (fma (* v v) -3 1)))) (* (/ (sqrt (sqrt 2)) (sqrt 4)) (sqrt (sqrt (- 1 (* 3 (* v v))))))) (- 1 (* v v))))
5.019 * [simplify]: Simplifying (* (/ (sqrt (sqrt 2)) (sqrt 4)) (sqrt (sqrt (- 1 (* 3 (* v v))))))
5.020 * * [simplify]: iters left: 6 (15 enodes)
5.032 * * [simplify]: iters left: 5 (55 enodes)
5.045 * * [simplify]: iters left: 4 (82 enodes)
5.059 * * [simplify]: iters left: 3 (108 enodes)
5.074 * * [simplify]: Extracting #0: cost 1 inf + 0
5.074 * * [simplify]: Extracting #1: cost 8 inf + 0
5.074 * * [simplify]: Extracting #2: cost 14 inf + 1
5.075 * * [simplify]: Extracting #3: cost 16 inf + 42
5.075 * * [simplify]: Extracting #4: cost 23 inf + 487
5.075 * * [simplify]: Extracting #5: cost 23 inf + 615
5.075 * * [simplify]: Extracting #6: cost 10 inf + 1662
5.076 * * [simplify]: Extracting #7: cost 0 inf + 3855
5.077 * [simplify]: Simplified to (* (/ (sqrt (sqrt 2)) 2) (sqrt (sqrt (fma (* v v) -3 1))))
5.077 * [simplify]: Simplified (2 1 2) to (λ (v) (* (* (* (/ (sqrt (sqrt 2)) (sqrt 4)) (sqrt (sqrt (- 1 (* 3 (* v v)))))) (* (/ (sqrt (sqrt 2)) 2) (sqrt (sqrt (fma (* v v) -3 1))))) (- 1 (* v v))))
5.077 * * * * [progress]: [ 44 / 83 ] simplifiying candidate #<alt (λ (v) (* (* (* (/ (sqrt (sqrt 2)) (sqrt 4)) (sqrt (sqrt (- 1 (* 3 (* v v)))))) (* (/ (sqrt (sqrt 2)) (sqrt 4)) (sqrt (sqrt (- 1 (* 3 (* v v))))))) (- 1 (* v v))))>
5.077 * [simplify]: Simplifying (* (/ (sqrt (sqrt 2)) (sqrt 4)) (sqrt (sqrt (- 1 (* 3 (* v v))))))
5.077 * * [simplify]: iters left: 6 (15 enodes)
5.083 * * [simplify]: iters left: 5 (55 enodes)
5.093 * * [simplify]: iters left: 4 (82 enodes)
5.116 * * [simplify]: iters left: 3 (108 enodes)
5.149 * * [simplify]: Extracting #0: cost 1 inf + 0
5.150 * * [simplify]: Extracting #1: cost 8 inf + 0
5.150 * * [simplify]: Extracting #2: cost 14 inf + 1
5.150 * * [simplify]: Extracting #3: cost 16 inf + 42
5.150 * * [simplify]: Extracting #4: cost 23 inf + 487
5.151 * * [simplify]: Extracting #5: cost 23 inf + 615
5.151 * * [simplify]: Extracting #6: cost 10 inf + 1662
5.153 * * [simplify]: Extracting #7: cost 0 inf + 3855
5.154 * [simplify]: Simplified to (* (/ (sqrt (sqrt 2)) 2) (sqrt (sqrt (fma (* v v) -3 1))))
5.154 * [simplify]: Simplified (2 1 1) to (λ (v) (* (* (* (/ (sqrt (sqrt 2)) 2) (sqrt (sqrt (fma (* v v) -3 1)))) (* (/ (sqrt (sqrt 2)) (sqrt 4)) (sqrt (sqrt (- 1 (* 3 (* v v))))))) (- 1 (* v v))))
5.155 * [simplify]: Simplifying (* (/ (sqrt (sqrt 2)) (sqrt 4)) (sqrt (sqrt (- 1 (* 3 (* v v))))))
5.155 * * [simplify]: iters left: 6 (15 enodes)
5.165 * * [simplify]: iters left: 5 (55 enodes)
5.184 * * [simplify]: iters left: 4 (82 enodes)
5.203 * * [simplify]: iters left: 3 (108 enodes)
5.219 * * [simplify]: Extracting #0: cost 1 inf + 0
5.219 * * [simplify]: Extracting #1: cost 8 inf + 0
5.219 * * [simplify]: Extracting #2: cost 14 inf + 1
5.219 * * [simplify]: Extracting #3: cost 16 inf + 42
5.219 * * [simplify]: Extracting #4: cost 23 inf + 487
5.220 * * [simplify]: Extracting #5: cost 23 inf + 615
5.220 * * [simplify]: Extracting #6: cost 10 inf + 1662
5.221 * * [simplify]: Extracting #7: cost 0 inf + 3855
5.222 * [simplify]: Simplified to (* (/ (sqrt (sqrt 2)) 2) (sqrt (sqrt (fma (* v v) -3 1))))
5.222 * [simplify]: Simplified (2 1 2) to (λ (v) (* (* (* (/ (sqrt (sqrt 2)) (sqrt 4)) (sqrt (sqrt (- 1 (* 3 (* v v)))))) (* (/ (sqrt (sqrt 2)) 2) (sqrt (sqrt (fma (* v v) -3 1))))) (- 1 (* v v))))
5.222 * * * * [progress]: [ 45 / 83 ] simplifiying candidate #<alt (λ (v) (* (* (* (/ (sqrt 2) 4) (* (cbrt (sqrt (- 1 (* 3 (* v v))))) (cbrt (sqrt (- 1 (* 3 (* v v))))))) (cbrt (sqrt (- 1 (* 3 (* v v)))))) (- 1 (* v v))))>
5.223 * [simplify]: Simplifying (cbrt (sqrt (- 1 (* 3 (* v v)))))
5.223 * * [simplify]: iters left: 6 (8 enodes)
5.225 * * [simplify]: iters left: 5 (31 enodes)
5.235 * * [simplify]: iters left: 4 (51 enodes)
5.252 * * [simplify]: iters left: 3 (75 enodes)
5.275 * * [simplify]: Extracting #0: cost 1 inf + 0
5.275 * * [simplify]: Extracting #1: cost 3 inf + 0
5.275 * * [simplify]: Extracting #2: cost 5 inf + 0
5.275 * * [simplify]: Extracting #3: cost 17 inf + 0
5.275 * * [simplify]: Extracting #4: cost 17 inf + 128
5.276 * * [simplify]: Extracting #5: cost 5 inf + 924
5.277 * * [simplify]: Extracting #6: cost 0 inf + 1734
5.278 * [simplify]: Simplified to (cbrt (sqrt (fma (* v -3) v 1)))
5.278 * [simplify]: Simplified (2 1 2) to (λ (v) (* (* (* (/ (sqrt 2) 4) (* (cbrt (sqrt (- 1 (* 3 (* v v))))) (cbrt (sqrt (- 1 (* 3 (* v v))))))) (cbrt (sqrt (fma (* v -3) v 1)))) (- 1 (* v v))))
5.278 * * * * [progress]: [ 46 / 83 ] simplifiying candidate #<alt (λ (v) (* (* (* (/ (sqrt 2) 4) (sqrt (* (cbrt (- 1 (* 3 (* v v)))) (cbrt (- 1 (* 3 (* v v))))))) (sqrt (cbrt (- 1 (* 3 (* v v)))))) (- 1 (* v v))))>
5.278 * [simplify]: Simplifying (sqrt (cbrt (- 1 (* 3 (* v v)))))
5.278 * * [simplify]: iters left: 6 (8 enodes)
5.283 * * [simplify]: iters left: 5 (31 enodes)
5.294 * * [simplify]: iters left: 4 (51 enodes)
5.307 * * [simplify]: iters left: 3 (75 enodes)
5.319 * * [simplify]: Extracting #0: cost 1 inf + 0
5.319 * * [simplify]: Extracting #1: cost 3 inf + 0
5.319 * * [simplify]: Extracting #2: cost 5 inf + 0
5.319 * * [simplify]: Extracting #3: cost 17 inf + 0
5.319 * * [simplify]: Extracting #4: cost 17 inf + 128
5.319 * * [simplify]: Extracting #5: cost 5 inf + 924
5.320 * * [simplify]: Extracting #6: cost 0 inf + 1814
5.320 * [simplify]: Simplified to (sqrt (cbrt (fma (* v -3) v 1)))
5.320 * [simplify]: Simplified (2 1 2) to (λ (v) (* (* (* (/ (sqrt 2) 4) (sqrt (* (cbrt (- 1 (* 3 (* v v)))) (cbrt (- 1 (* 3 (* v v))))))) (sqrt (cbrt (fma (* v -3) v 1)))) (- 1 (* v v))))
5.320 * * * * [progress]: [ 47 / 83 ] simplifiying candidate #<alt (λ (v) (* (* (* (/ (sqrt 2) 4) (sqrt (sqrt (- 1 (* 3 (* v v)))))) (sqrt (sqrt (- 1 (* 3 (* v v)))))) (- 1 (* v v))))>
5.320 * [simplify]: Simplifying (sqrt (sqrt (- 1 (* 3 (* v v)))))
5.320 * * [simplify]: iters left: 6 (8 enodes)
5.323 * * [simplify]: iters left: 5 (31 enodes)
5.328 * * [simplify]: iters left: 4 (51 enodes)
5.337 * * [simplify]: iters left: 3 (75 enodes)
5.356 * * [simplify]: Extracting #0: cost 1 inf + 0
5.356 * * [simplify]: Extracting #1: cost 3 inf + 0
5.356 * * [simplify]: Extracting #2: cost 5 inf + 0
5.356 * * [simplify]: Extracting #3: cost 17 inf + 0
5.356 * * [simplify]: Extracting #4: cost 17 inf + 128
5.357 * * [simplify]: Extracting #5: cost 5 inf + 924
5.357 * * [simplify]: Extracting #6: cost 0 inf + 1654
5.358 * [simplify]: Simplified to (sqrt (sqrt (fma (* v -3) v 1)))
5.358 * [simplify]: Simplified (2 1 2) to (λ (v) (* (* (* (/ (sqrt 2) 4) (sqrt (sqrt (- 1 (* 3 (* v v)))))) (sqrt (sqrt (fma (* v -3) v 1)))) (- 1 (* v v))))
5.358 * * * * [progress]: [ 48 / 83 ] simplifiying candidate #<alt (λ (v) (* (* (* (/ (sqrt 2) 4) (sqrt 1)) (sqrt (- 1 (* 3 (* v v))))) (- 1 (* v v))))>
5.359 * [simplify]: Simplifying (sqrt (- 1 (* 3 (* v v))))
5.359 * * [simplify]: iters left: 6 (7 enodes)
5.363 * * [simplify]: iters left: 5 (28 enodes)
5.372 * * [simplify]: iters left: 4 (48 enodes)
5.380 * * [simplify]: iters left: 3 (72 enodes)
5.390 * * [simplify]: Extracting #0: cost 1 inf + 0
5.390 * * [simplify]: Extracting #1: cost 3 inf + 0
5.390 * * [simplify]: Extracting #2: cost 15 inf + 0
5.391 * * [simplify]: Extracting #3: cost 13 inf + 331
5.391 * * [simplify]: Extracting #4: cost 4 inf + 882
5.391 * * [simplify]: Extracting #5: cost 0 inf + 1298
5.392 * [simplify]: Simplified to (sqrt (fma (* v v) -3 1))
5.392 * [simplify]: Simplified (2 1 2) to (λ (v) (* (* (* (/ (sqrt 2) 4) (sqrt 1)) (sqrt (fma (* v v) -3 1))) (- 1 (* v v))))
5.392 * * * * [progress]: [ 49 / 83 ] simplifiying candidate #<alt (λ (v) (* (* (* (/ (sqrt 2) 4) (sqrt (sqrt (- 1 (* 3 (* v v)))))) (sqrt (sqrt (- 1 (* 3 (* v v)))))) (- 1 (* v v))))>
5.392 * [simplify]: Simplifying (sqrt (sqrt (- 1 (* 3 (* v v)))))
5.392 * * [simplify]: iters left: 6 (8 enodes)
5.394 * * [simplify]: iters left: 5 (31 enodes)
5.400 * * [simplify]: iters left: 4 (51 enodes)
5.414 * * [simplify]: iters left: 3 (75 enodes)
5.425 * * [simplify]: Extracting #0: cost 1 inf + 0
5.425 * * [simplify]: Extracting #1: cost 3 inf + 0
5.425 * * [simplify]: Extracting #2: cost 5 inf + 0
5.425 * * [simplify]: Extracting #3: cost 17 inf + 0
5.425 * * [simplify]: Extracting #4: cost 17 inf + 128
5.425 * * [simplify]: Extracting #5: cost 5 inf + 924
5.426 * * [simplify]: Extracting #6: cost 0 inf + 1654
5.426 * [simplify]: Simplified to (sqrt (sqrt (fma (* v -3) v 1)))
5.426 * [simplify]: Simplified (2 1 2) to (λ (v) (* (* (* (/ (sqrt 2) 4) (sqrt (sqrt (- 1 (* 3 (* v v)))))) (sqrt (sqrt (fma (* v -3) v 1)))) (- 1 (* v v))))
5.426 * * * * [progress]: [ 50 / 83 ] simplifiying candidate #<alt (λ (v) (* (* (* (/ (sqrt 2) 4) 1) (sqrt (- 1 (* 3 (* v v))))) (- 1 (* v v))))>
5.426 * [simplify]: Simplifying (sqrt (- 1 (* 3 (* v v))))
5.426 * * [simplify]: iters left: 6 (7 enodes)
5.429 * * [simplify]: iters left: 5 (28 enodes)
5.434 * * [simplify]: iters left: 4 (48 enodes)
5.442 * * [simplify]: iters left: 3 (72 enodes)
5.460 * * [simplify]: Extracting #0: cost 1 inf + 0
5.460 * * [simplify]: Extracting #1: cost 3 inf + 0
5.460 * * [simplify]: Extracting #2: cost 15 inf + 0
5.460 * * [simplify]: Extracting #3: cost 13 inf + 331
5.460 * * [simplify]: Extracting #4: cost 4 inf + 882
5.461 * * [simplify]: Extracting #5: cost 0 inf + 1298
5.461 * [simplify]: Simplified to (sqrt (fma (* v v) -3 1))
5.461 * [simplify]: Simplified (2 1 2) to (λ (v) (* (* (* (/ (sqrt 2) 4) 1) (sqrt (fma (* v v) -3 1))) (- 1 (* v v))))
5.461 * * * * [progress]: [ 51 / 83 ] simplifiying candidate #<alt (λ (v) (* (* (* (cbrt (/ (sqrt 2) 4)) (cbrt (/ (sqrt 2) 4))) (* (cbrt (/ (sqrt 2) 4)) (sqrt (- 1 (* 3 (* v v)))))) (- 1 (* v v))))>
5.462 * [simplify]: Simplifying (* (cbrt (/ (sqrt 2) 4)) (cbrt (/ (sqrt 2) 4)))
5.462 * * [simplify]: iters left: 6 (6 enodes)
5.464 * * [simplify]: iters left: 5 (18 enodes)
5.467 * * [simplify]: Extracting #0: cost 1 inf + 0
5.467 * * [simplify]: Extracting #1: cost 3 inf + 0
5.467 * * [simplify]: Extracting #2: cost 5 inf + 0
5.467 * * [simplify]: Extracting #3: cost 8 inf + 0
5.467 * * [simplify]: Extracting #4: cost 9 inf + 1
5.467 * * [simplify]: Extracting #5: cost 8 inf + 2
5.467 * * [simplify]: Extracting #6: cost 0 inf + 976
5.467 * [simplify]: Simplified to (* (cbrt (/ (sqrt 2) 4)) (cbrt (/ (sqrt 2) 4)))
5.467 * [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.467 * * * * [progress]: [ 52 / 83 ] simplifiying candidate #<alt (λ (v) (* (* (sqrt (/ (sqrt 2) 4)) (* (sqrt (/ (sqrt 2) 4)) (sqrt (- 1 (* 3 (* v v)))))) (- 1 (* v v))))>
5.467 * [simplify]: Simplifying (sqrt (/ (sqrt 2) 4))
5.468 * * [simplify]: iters left: 4 (5 enodes)
5.469 * * [simplify]: iters left: 3 (15 enodes)
5.472 * * [simplify]: Extracting #0: cost 1 inf + 0
5.472 * * [simplify]: Extracting #1: cost 3 inf + 0
5.472 * * [simplify]: Extracting #2: cost 6 inf + 0
5.472 * * [simplify]: Extracting #3: cost 7 inf + 1
5.472 * * [simplify]: Extracting #4: cost 6 inf + 2
5.472 * * [simplify]: Extracting #5: cost 0 inf + 492
5.472 * [simplify]: Simplified to (sqrt (/ (sqrt 2) 4))
5.472 * [simplify]: Simplified (2 1 1) to (λ (v) (* (* (sqrt (/ (sqrt 2) 4)) (* (sqrt (/ (sqrt 2) 4)) (sqrt (- 1 (* 3 (* v v)))))) (- 1 (* v v))))
5.472 * * * * [progress]: [ 53 / 83 ] simplifiying candidate #<alt (λ (v) (* (* (/ (* (cbrt (sqrt 2)) (cbrt (sqrt 2))) (* (cbrt 4) (cbrt 4))) (* (/ (cbrt (sqrt 2)) (cbrt 4)) (sqrt (- 1 (* 3 (* v v)))))) (- 1 (* v v))))>
5.472 * [simplify]: Simplifying (/ (* (cbrt (sqrt 2)) (cbrt (sqrt 2))) (* (cbrt 4) (cbrt 4)))
5.473 * * [simplify]: iters left: 6 (8 enodes)
5.475 * * [simplify]: iters left: 5 (30 enodes)
5.482 * * [simplify]: iters left: 4 (45 enodes)
5.490 * * [simplify]: iters left: 3 (52 enodes)
5.498 * * [simplify]: iters left: 2 (55 enodes)
5.506 * * [simplify]: Extracting #0: cost 1 inf + 0
5.506 * * [simplify]: Extracting #1: cost 11 inf + 0
5.506 * * [simplify]: Extracting #2: cost 22 inf + 0
5.506 * * [simplify]: Extracting #3: cost 22 inf + 82
5.506 * * [simplify]: Extracting #4: cost 17 inf + 447
5.507 * * [simplify]: Extracting #5: cost 5 inf + 3107
5.508 * * [simplify]: Extracting #6: cost 0 inf + 4276
5.509 * [simplify]: Simplified to (* (/ (cbrt (sqrt 2)) (cbrt 4)) (/ (cbrt (sqrt 2)) (cbrt 4)))
5.509 * [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.509 * * * * [progress]: [ 54 / 83 ] simplifiying candidate #<alt (λ (v) (* (* (/ (* (cbrt (sqrt 2)) (cbrt (sqrt 2))) (sqrt 4)) (* (/ (cbrt (sqrt 2)) (sqrt 4)) (sqrt (- 1 (* 3 (* v v)))))) (- 1 (* v v))))>
5.509 * [simplify]: Simplifying (/ (* (cbrt (sqrt 2)) (cbrt (sqrt 2))) (sqrt 4))
5.509 * * [simplify]: iters left: 6 (7 enodes)
5.514 * * [simplify]: iters left: 5 (23 enodes)
5.522 * * [simplify]: iters left: 4 (29 enodes)
5.530 * * [simplify]: iters left: 3 (34 enodes)
5.540 * * [simplify]: Extracting #0: cost 1 inf + 0
5.540 * * [simplify]: Extracting #1: cost 8 inf + 0
5.540 * * [simplify]: Extracting #2: cost 13 inf + 1
5.541 * * [simplify]: Extracting #3: cost 13 inf + 42
5.541 * * [simplify]: Extracting #4: cost 3 inf + 1452
5.541 * * [simplify]: Extracting #5: cost 1 inf + 1814
5.542 * * [simplify]: Extracting #6: cost 0 inf + 2015
5.542 * [simplify]: Simplified to (/ (cbrt (sqrt 2)) (/ 2 (cbrt (sqrt 2))))
5.542 * [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))))
5.542 * * * * [progress]: [ 55 / 83 ] simplifiying candidate #<alt (λ (v) (* (* (/ (* (cbrt (sqrt 2)) (cbrt (sqrt 2))) 1) (* (/ (cbrt (sqrt 2)) 4) (sqrt (- 1 (* 3 (* v v)))))) (- 1 (* v v))))>
5.543 * [simplify]: Simplifying (/ (* (cbrt (sqrt 2)) (cbrt (sqrt 2))) 1)
5.543 * * [simplify]: iters left: 6 (6 enodes)
5.547 * * [simplify]: iters left: 5 (20 enodes)
5.554 * * [simplify]: iters left: 4 (30 enodes)
5.563 * * [simplify]: iters left: 3 (31 enodes)
5.574 * * [simplify]: Extracting #0: cost 1 inf + 0
5.574 * * [simplify]: Extracting #1: cost 5 inf + 0
5.574 * * [simplify]: Extracting #2: cost 7 inf + 1
5.574 * * [simplify]: Extracting #3: cost 9 inf + 1
5.574 * * [simplify]: Extracting #4: cost 8 inf + 2
5.574 * * [simplify]: Extracting #5: cost 0 inf + 972
5.574 * [simplify]: Simplified to (* (cbrt (sqrt 2)) (cbrt (sqrt 2)))
5.575 * [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))))
5.575 * * * * [progress]: [ 56 / 83 ] simplifiying candidate #<alt (λ (v) (* (* (/ (sqrt (* (cbrt 2) (cbrt 2))) (* (cbrt 4) (cbrt 4))) (* (/ (sqrt (cbrt 2)) (cbrt 4)) (sqrt (- 1 (* 3 (* v v)))))) (- 1 (* v v))))>
5.575 * [simplify]: Simplifying (/ (sqrt (* (cbrt 2) (cbrt 2))) (* (cbrt 4) (cbrt 4)))
5.575 * * [simplify]: iters left: 6 (8 enodes)
5.580 * * [simplify]: iters left: 5 (27 enodes)
5.590 * * [simplify]: iters left: 4 (29 enodes)
5.600 * * [simplify]: Extracting #0: cost 1 inf + 0
5.600 * * [simplify]: Extracting #1: cost 6 inf + 0
5.600 * * [simplify]: Extracting #2: cost 13 inf + 0
5.600 * * [simplify]: Extracting #3: cost 14 inf + 82
5.600 * * [simplify]: Extracting #4: cost 11 inf + 285
5.600 * * [simplify]: Extracting #5: cost 4 inf + 1334
5.601 * * [simplify]: Extracting #6: cost 0 inf + 2100
5.601 * [simplify]: Simplified to (/ (fabs (cbrt 2)) (* (cbrt 4) (cbrt 4)))
5.601 * [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))))
5.602 * * * * [progress]: [ 57 / 83 ] simplifiying candidate #<alt (λ (v) (* (* (/ (sqrt (* (cbrt 2) (cbrt 2))) (sqrt 4)) (* (/ (sqrt (cbrt 2)) (sqrt 4)) (sqrt (- 1 (* 3 (* v v)))))) (- 1 (* v v))))>
5.602 * [simplify]: Simplifying (/ (sqrt (* (cbrt 2) (cbrt 2))) (sqrt 4))
5.602 * * [simplify]: iters left: 6 (7 enodes)
5.607 * * [simplify]: iters left: 5 (22 enodes)
5.614 * * [simplify]: Extracting #0: cost 1 inf + 0
5.614 * * [simplify]: Extracting #1: cost 4 inf + 0
5.614 * * [simplify]: Extracting #2: cost 6 inf + 1
5.615 * * [simplify]: Extracting #3: cost 3 inf + 606
5.615 * * [simplify]: Extracting #4: cost 0 inf + 969
5.615 * [simplify]: Simplified to (/ (fabs (cbrt 2)) 2)
5.615 * [simplify]: Simplified (2 1 1) to (λ (v) (* (* (/ (fabs (cbrt 2)) 2) (* (/ (sqrt (cbrt 2)) (sqrt 4)) (sqrt (- 1 (* 3 (* v v)))))) (- 1 (* v v))))
5.615 * * * * [progress]: [ 58 / 83 ] simplifiying candidate #<alt (λ (v) (* (* (/ (sqrt (* (cbrt 2) (cbrt 2))) 1) (* (/ (sqrt (cbrt 2)) 4) (sqrt (- 1 (* 3 (* v v)))))) (- 1 (* v v))))>
5.616 * [simplify]: Simplifying (/ (sqrt (* (cbrt 2) (cbrt 2))) 1)
5.616 * * [simplify]: iters left: 6 (6 enodes)
5.620 * * [simplify]: iters left: 5 (19 enodes)
5.627 * * [simplify]: iters left: 4 (23 enodes)
5.634 * * [simplify]: Extracting #0: cost 1 inf + 0
5.634 * * [simplify]: Extracting #1: cost 5 inf + 0
5.634 * * [simplify]: Extracting #2: cost 7 inf + 1
5.634 * * [simplify]: Extracting #3: cost 6 inf + 2
5.634 * * [simplify]: Extracting #4: cost 0 inf + 648
5.634 * [simplify]: Simplified to (fabs (cbrt 2))
5.634 * [simplify]: Simplified (2 1 1) to (λ (v) (* (* (fabs (cbrt 2)) (* (/ (sqrt (cbrt 2)) 4) (sqrt (- 1 (* 3 (* v v)))))) (- 1 (* v v))))
5.634 * * * * [progress]: [ 59 / 83 ] simplifiying candidate #<alt (λ (v) (* (* (/ (sqrt (sqrt 2)) (* (cbrt 4) (cbrt 4))) (* (/ (sqrt (sqrt 2)) (cbrt 4)) (sqrt (- 1 (* 3 (* v v)))))) (- 1 (* v v))))>
5.635 * [simplify]: Simplifying (/ (sqrt (sqrt 2)) (* (cbrt 4) (cbrt 4)))
5.635 * * [simplify]: iters left: 5 (7 enodes)
5.639 * * [simplify]: iters left: 4 (23 enodes)
5.647 * * [simplify]: iters left: 3 (25 enodes)
5.656 * * [simplify]: Extracting #0: cost 1 inf + 0
5.656 * * [simplify]: Extracting #1: cost 6 inf + 0
5.656 * * [simplify]: Extracting #2: cost 12 inf + 0
5.656 * * [simplify]: Extracting #3: cost 13 inf + 1
5.656 * * [simplify]: Extracting #4: cost 9 inf + 285
5.656 * * [simplify]: Extracting #5: cost 6 inf + 488
5.656 * * [simplify]: Extracting #6: cost 2 inf + 1094
5.657 * * [simplify]: Extracting #7: cost 0 inf + 1538
5.657 * [simplify]: Simplified to (/ (sqrt (sqrt 2)) (* (cbrt 4) (cbrt 4)))
5.657 * [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))))
5.657 * * * * [progress]: [ 60 / 83 ] simplifiying candidate #<alt (λ (v) (* (* (/ (sqrt (sqrt 2)) (sqrt 4)) (* (/ (sqrt (sqrt 2)) (sqrt 4)) (sqrt (- 1 (* 3 (* v v)))))) (- 1 (* v v))))>
5.658 * [simplify]: Simplifying (/ (sqrt (sqrt 2)) (sqrt 4))
5.658 * * [simplify]: iters left: 4 (6 enodes)
5.662 * * [simplify]: iters left: 3 (18 enodes)
5.667 * * [simplify]: Extracting #0: cost 1 inf + 0
5.667 * * [simplify]: Extracting #1: cost 4 inf + 0
5.667 * * [simplify]: Extracting #2: cost 5 inf + 1
5.668 * * [simplify]: Extracting #3: cost 1 inf + 446
5.668 * * [simplify]: Extracting #4: cost 0 inf + 487
5.668 * [simplify]: Simplified to (/ (sqrt (sqrt 2)) 2)
5.668 * [simplify]: Simplified (2 1 1) to (λ (v) (* (* (/ (sqrt (sqrt 2)) 2) (* (/ (sqrt (sqrt 2)) (sqrt 4)) (sqrt (- 1 (* 3 (* v v)))))) (- 1 (* v v))))
5.668 * * * * [progress]: [ 61 / 83 ] simplifiying candidate #<alt (λ (v) (* (* (/ (sqrt (sqrt 2)) 1) (* (/ (sqrt (sqrt 2)) 4) (sqrt (- 1 (* 3 (* v v)))))) (- 1 (* v v))))>
5.668 * [simplify]: Simplifying (/ (sqrt (sqrt 2)) 1)
5.669 * * [simplify]: iters left: 4 (5 enodes)
5.671 * * [simplify]: iters left: 3 (15 enodes)
5.676 * * [simplify]: iters left: 2 (17 enodes)
5.680 * * [simplify]: Extracting #0: cost 1 inf + 0
5.680 * * [simplify]: Extracting #1: cost 4 inf + 0
5.680 * * [simplify]: Extracting #2: cost 5 inf + 1
5.680 * * [simplify]: Extracting #3: cost 4 inf + 2
5.680 * * [simplify]: Extracting #4: cost 1 inf + 165
5.680 * * [simplify]: Extracting #5: cost 0 inf + 246
5.681 * [simplify]: Simplified to (sqrt (sqrt 2))
5.681 * [simplify]: Simplified (2 1 1) to (λ (v) (* (* (sqrt (sqrt 2)) (* (/ (sqrt (sqrt 2)) 4) (sqrt (- 1 (* 3 (* v v)))))) (- 1 (* v v))))
5.681 * * * * [progress]: [ 62 / 83 ] simplifiying candidate #<alt (λ (v) (* (* (/ (sqrt 1) (* (cbrt 4) (cbrt 4))) (* (/ (sqrt 2) (cbrt 4)) (sqrt (- 1 (* 3 (* v v)))))) (- 1 (* v v))))>
5.681 * [simplify]: Simplifying (/ (sqrt 1) (* (cbrt 4) (cbrt 4)))
5.681 * * [simplify]: iters left: 5 (6 enodes)
5.683 * * [simplify]: iters left: 4 (22 enodes)
5.687 * * [simplify]: iters left: 3 (29 enodes)
5.692 * * [simplify]: iters left: 2 (31 enodes)
5.697 * * [simplify]: Extracting #0: cost 1 inf + 0
5.697 * * [simplify]: Extracting #1: cost 7 inf + 0
5.697 * * [simplify]: Extracting #2: cost 11 inf + 1
5.697 * * [simplify]: Extracting #3: cost 10 inf + 2
5.697 * * [simplify]: Extracting #4: cost 2 inf + 935
5.697 * * [simplify]: Extracting #5: cost 0 inf + 1218
5.698 * [simplify]: Simplified to (/ 1 (* (cbrt 4) (cbrt 4)))
5.698 * [simplify]: Simplified (2 1 1) to (λ (v) (* (* (/ 1 (* (cbrt 4) (cbrt 4))) (* (/ (sqrt 2) (cbrt 4)) (sqrt (- 1 (* 3 (* v v)))))) (- 1 (* v v))))
5.698 * * * * [progress]: [ 63 / 83 ] simplifiying candidate #<alt (λ (v) (* (* (/ (sqrt 1) (sqrt 4)) (* (/ (sqrt 2) (sqrt 4)) (sqrt (- 1 (* 3 (* v v)))))) (- 1 (* v v))))>
5.698 * [simplify]: Simplifying (/ (sqrt 1) (sqrt 4))
5.698 * * [simplify]: iters left: 3 (5 enodes)
5.703 * * [simplify]: iters left: 2 (18 enodes)
5.707 * * [simplify]: iters left: 1 (21 enodes)
5.713 * * [simplify]: Extracting #0: cost 1 inf + 0
5.713 * * [simplify]: Extracting #1: cost 0 inf + 1
5.713 * [simplify]: Simplified to 1/2
5.713 * [simplify]: Simplified (2 1 1) to (λ (v) (* (* 1/2 (* (/ (sqrt 2) (sqrt 4)) (sqrt (- 1 (* 3 (* v v)))))) (- 1 (* v v))))
5.713 * * * * [progress]: [ 64 / 83 ] simplifiying candidate #<alt (λ (v) (* (* (/ (sqrt 1) 1) (* (/ (sqrt 2) 4) (sqrt (- 1 (* 3 (* v v)))))) (- 1 (* v v))))>
5.714 * [simplify]: Simplifying (/ (sqrt 1) 1)
5.714 * * [simplify]: iters left: 3 (3 enodes)
5.717 * * [simplify]: iters left: 2 (9 enodes)
5.720 * * [simplify]: iters left: 1 (11 enodes)
5.722 * * [simplify]: Extracting #0: cost 1 inf + 0
5.722 * * [simplify]: Extracting #1: cost 0 inf + 1
5.722 * [simplify]: Simplified to 1
5.722 * [simplify]: Simplified (2 1 1) to (λ (v) (* (* 1 (* (/ (sqrt 2) 4) (sqrt (- 1 (* 3 (* v v)))))) (- 1 (* v v))))
5.723 * * * * [progress]: [ 65 / 83 ] simplifiying candidate #<alt (λ (v) (* (* (/ (sqrt (sqrt 2)) (* (cbrt 4) (cbrt 4))) (* (/ (sqrt (sqrt 2)) (cbrt 4)) (sqrt (- 1 (* 3 (* v v)))))) (- 1 (* v v))))>
5.723 * [simplify]: Simplifying (/ (sqrt (sqrt 2)) (* (cbrt 4) (cbrt 4)))
5.723 * * [simplify]: iters left: 5 (7 enodes)
5.725 * * [simplify]: iters left: 4 (23 enodes)
5.729 * * [simplify]: iters left: 3 (25 enodes)
5.734 * * [simplify]: Extracting #0: cost 1 inf + 0
5.734 * * [simplify]: Extracting #1: cost 6 inf + 0
5.734 * * [simplify]: Extracting #2: cost 12 inf + 0
5.734 * * [simplify]: Extracting #3: cost 13 inf + 1
5.734 * * [simplify]: Extracting #4: cost 9 inf + 285
5.734 * * [simplify]: Extracting #5: cost 6 inf + 488
5.734 * * [simplify]: Extracting #6: cost 2 inf + 1094
5.734 * * [simplify]: Extracting #7: cost 0 inf + 1538
5.735 * [simplify]: Simplified to (/ (sqrt (sqrt 2)) (* (cbrt 4) (cbrt 4)))
5.735 * [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))))
5.735 * * * * [progress]: [ 66 / 83 ] simplifiying candidate #<alt (λ (v) (* (* (/ (sqrt (sqrt 2)) (sqrt 4)) (* (/ (sqrt (sqrt 2)) (sqrt 4)) (sqrt (- 1 (* 3 (* v v)))))) (- 1 (* v v))))>
5.735 * [simplify]: Simplifying (/ (sqrt (sqrt 2)) (sqrt 4))
5.735 * * [simplify]: iters left: 4 (6 enodes)
5.738 * * [simplify]: iters left: 3 (18 enodes)
5.741 * * [simplify]: Extracting #0: cost 1 inf + 0
5.741 * * [simplify]: Extracting #1: cost 4 inf + 0
5.741 * * [simplify]: Extracting #2: cost 5 inf + 1
5.741 * * [simplify]: Extracting #3: cost 1 inf + 446
5.742 * * [simplify]: Extracting #4: cost 0 inf + 487
5.742 * [simplify]: Simplified to (/ (sqrt (sqrt 2)) 2)
5.742 * [simplify]: Simplified (2 1 1) to (λ (v) (* (* (/ (sqrt (sqrt 2)) 2) (* (/ (sqrt (sqrt 2)) (sqrt 4)) (sqrt (- 1 (* 3 (* v v)))))) (- 1 (* v v))))
5.742 * * * * [progress]: [ 67 / 83 ] simplifiying candidate #<alt (λ (v) (* (* (/ (sqrt (sqrt 2)) 1) (* (/ (sqrt (sqrt 2)) 4) (sqrt (- 1 (* 3 (* v v)))))) (- 1 (* v v))))>
5.742 * [simplify]: Simplifying (/ (sqrt (sqrt 2)) 1)
5.742 * * [simplify]: iters left: 4 (5 enodes)
5.744 * * [simplify]: iters left: 3 (15 enodes)
5.747 * * [simplify]: iters left: 2 (17 enodes)
5.750 * * [simplify]: Extracting #0: cost 1 inf + 0
5.750 * * [simplify]: Extracting #1: cost 4 inf + 0
5.750 * * [simplify]: Extracting #2: cost 5 inf + 1
5.750 * * [simplify]: Extracting #3: cost 4 inf + 2
5.750 * * [simplify]: Extracting #4: cost 1 inf + 165
5.750 * * [simplify]: Extracting #5: cost 0 inf + 246
5.750 * [simplify]: Simplified to (sqrt (sqrt 2))
5.750 * [simplify]: Simplified (2 1 1) to (λ (v) (* (* (sqrt (sqrt 2)) (* (/ (sqrt (sqrt 2)) 4) (sqrt (- 1 (* 3 (* v v)))))) (- 1 (* v v))))
5.750 * * * * [progress]: [ 68 / 83 ] simplifiying candidate #<alt (λ (v) (* (* (/ 1 (* (cbrt 4) (cbrt 4))) (* (/ (sqrt 2) (cbrt 4)) (sqrt (- 1 (* 3 (* v v)))))) (- 1 (* v v))))>
5.751 * [simplify]: Simplifying (/ 1 (* (cbrt 4) (cbrt 4)))
5.751 * * [simplify]: iters left: 5 (5 enodes)
5.754 * * [simplify]: iters left: 4 (19 enodes)
5.761 * * [simplify]: iters left: 3 (23 enodes)
5.769 * * [simplify]: Extracting #0: cost 1 inf + 0
5.769 * * [simplify]: Extracting #1: cost 6 inf + 0
5.769 * * [simplify]: Extracting #2: cost 9 inf + 1
5.769 * * [simplify]: Extracting #3: cost 1 inf + 852
5.769 * * [simplify]: Extracting #4: cost 0 inf + 974
5.770 * [simplify]: Simplified to (/ 1 (* (cbrt 4) (cbrt 4)))
5.770 * [simplify]: Simplified (2 1 1) to (λ (v) (* (* (/ 1 (* (cbrt 4) (cbrt 4))) (* (/ (sqrt 2) (cbrt 4)) (sqrt (- 1 (* 3 (* v v)))))) (- 1 (* v v))))
5.770 * * * * [progress]: [ 69 / 83 ] simplifiying candidate #<alt (λ (v) (* (* (/ 1 (sqrt 4)) (* (/ (sqrt 2) (sqrt 4)) (sqrt (- 1 (* 3 (* v v)))))) (- 1 (* v v))))>
5.770 * [simplify]: Simplifying (/ 1 (sqrt 4))
5.770 * * [simplify]: iters left: 3 (4 enodes)
5.774 * * [simplify]: iters left: 2 (16 enodes)
5.779 * * [simplify]: iters left: 1 (18 enodes)
5.784 * * [simplify]: Extracting #0: cost 1 inf + 0
5.784 * * [simplify]: Extracting #1: cost 0 inf + 1
5.784 * [simplify]: Simplified to 1/2
5.784 * [simplify]: Simplified (2 1 1) to (λ (v) (* (* 1/2 (* (/ (sqrt 2) (sqrt 4)) (sqrt (- 1 (* 3 (* v v)))))) (- 1 (* v v))))
5.785 * * * * [progress]: [ 70 / 83 ] simplifiying candidate #<alt (λ (v) (* (* (/ 1 1) (* (/ (sqrt 2) 4) (sqrt (- 1 (* 3 (* v v)))))) (- 1 (* v v))))>
5.785 * [simplify]: Simplifying (/ 1 1)
5.785 * * [simplify]: iters left: 2 (2 enodes)
5.786 * * [simplify]: iters left: 1 (6 enodes)
5.787 * * [simplify]: Extracting #0: cost 1 inf + 0
5.787 * * [simplify]: Extracting #1: cost 0 inf + 1
5.787 * [simplify]: Simplified to 1
5.787 * [simplify]: Simplified (2 1 1) to (λ (v) (* (* 1 (* (/ (sqrt 2) 4) (sqrt (- 1 (* 3 (* v v)))))) (- 1 (* v v))))
5.787 * * * * [progress]: [ 71 / 83 ] simplifiying candidate #<alt (λ (v) (* (* 1 (* (/ (sqrt 2) 4) (sqrt (- 1 (* 3 (* v v)))))) (- 1 (* v v))))>
5.787 * * * * [progress]: [ 72 / 83 ] simplifiying candidate #<alt (λ (v) (* (* (sqrt 2) (* (/ 1 4) (sqrt (- 1 (* 3 (* v v)))))) (- 1 (* v v))))>
5.787 * [simplify]: Simplifying (sqrt 2)
5.787 * * [simplify]: iters left: 1 (2 enodes)
5.788 * * [simplify]: Extracting #0: cost 1 inf + 0
5.788 * * [simplify]: Extracting #1: cost 3 inf + 0
5.788 * * [simplify]: Extracting #2: cost 2 inf + 1
5.788 * * [simplify]: Extracting #3: cost 0 inf + 83
5.788 * [simplify]: Simplified to (sqrt 2)
5.788 * [simplify]: Simplified (2 1 1) to (λ (v) (* (* (sqrt 2) (* (/ 1 4) (sqrt (- 1 (* 3 (* v v)))))) (- 1 (* v v))))
5.788 * * * * [progress]: [ 73 / 83 ] simplifiying candidate #<alt (λ (v) (* (/ (* (/ (sqrt 2) 4) (sqrt (- (pow 1 3) (pow (* 3 (* v v)) 3)))) (sqrt (+ (* 1 1) (+ (* (* 3 (* v v)) (* 3 (* v v))) (* 1 (* 3 (* v v))))))) (- 1 (* v v))))>
5.788 * [simplify]: Simplifying (sqrt (+ (* 1 1) (+ (* (* 3 (* v v)) (* 3 (* v v))) (* 1 (* 3 (* v v))))))
5.788 * * [simplify]: iters left: 6 (11 enodes)
5.792 * * [simplify]: iters left: 5 (54 enodes)
5.805 * * [simplify]: iters left: 4 (149 enodes)
5.871 * * [simplify]: iters left: 3 (314 enodes)
6.007 * * [simplify]: iters left: 2 (461 enodes)
6.155 * * [simplify]: Extracting #0: cost 1 inf + 0
6.155 * * [simplify]: Extracting #1: cost 3 inf + 0
6.155 * * [simplify]: Extracting #2: cost 26 inf + 0
6.156 * * [simplify]: Extracting #3: cost 40 inf + 1003
6.160 * * [simplify]: Extracting #4: cost 18 inf + 3840
6.166 * * [simplify]: Extracting #5: cost 11 inf + 4641
6.172 * * [simplify]: Extracting #6: cost 6 inf + 5572
6.178 * * [simplify]: Extracting #7: cost 0 inf + 7127
6.184 * [simplify]: Simplified to (sqrt (+ 1 (fma (* (* v v) 3) (* (* v v) 3) (* (* v v) 3))))
6.184 * [simplify]: Simplified (2 1 2) to (λ (v) (* (/ (* (/ (sqrt 2) 4) (sqrt (- (pow 1 3) (pow (* 3 (* v v)) 3)))) (sqrt (+ 1 (fma (* (* v v) 3) (* (* v v) 3) (* (* v v) 3))))) (- 1 (* v v))))
6.184 * * * * [progress]: [ 74 / 83 ] simplifiying candidate #<alt (λ (v) (* (/ (* (/ (sqrt 2) 4) (sqrt (- (* 1 1) (* (* 3 (* v v)) (* 3 (* v v)))))) (sqrt (+ 1 (* 3 (* v v))))) (- 1 (* v v))))>
6.185 * [simplify]: Simplifying (sqrt (+ 1 (* 3 (* v v))))
6.185 * * [simplify]: iters left: 6 (7 enodes)
6.189 * * [simplify]: iters left: 5 (27 enodes)
6.198 * * [simplify]: iters left: 4 (36 enodes)
6.209 * * [simplify]: Extracting #0: cost 1 inf + 0
6.209 * * [simplify]: Extracting #1: cost 3 inf + 0
6.209 * * [simplify]: Extracting #2: cost 10 inf + 0
6.209 * * [simplify]: Extracting #3: cost 9 inf + 44
6.209 * * [simplify]: Extracting #4: cost 5 inf + 307
6.210 * * [simplify]: Extracting #5: cost 1 inf + 667
6.210 * * [simplify]: Extracting #6: cost 0 inf + 805
6.210 * [simplify]: Simplified to (sqrt (fma 3 (* v v) 1))
6.210 * [simplify]: Simplified (2 1 2) to (λ (v) (* (/ (* (/ (sqrt 2) 4) (sqrt (- (* 1 1) (* (* 3 (* v v)) (* 3 (* v v)))))) (sqrt (fma 3 (* v v) 1))) (- 1 (* v v))))
6.211 * * * * [progress]: [ 75 / 83 ] simplifiying candidate #<alt (λ (v) (* (/ (* (sqrt 2) (sqrt (- 1 (* 3 (* v v))))) 4) (- 1 (* v v))))>
6.211 * [simplify]: Simplifying (* (sqrt 2) (sqrt (- 1 (* 3 (* v v)))))
6.211 * * [simplify]: iters left: 6 (10 enodes)
6.217 * * [simplify]: iters left: 5 (38 enodes)
6.231 * * [simplify]: iters left: 4 (58 enodes)
6.250 * * [simplify]: iters left: 3 (82 enodes)
6.277 * * [simplify]: Extracting #0: cost 1 inf + 0
6.277 * * [simplify]: Extracting #1: cost 4 inf + 0
6.277 * * [simplify]: Extracting #2: cost 8 inf + 0
6.277 * * [simplify]: Extracting #3: cost 19 inf + 1
6.278 * * [simplify]: Extracting #4: cost 16 inf + 366
6.278 * * [simplify]: Extracting #5: cost 2 inf + 1600
6.279 * * [simplify]: Extracting #6: cost 0 inf + 1819
6.280 * [simplify]: Simplified to (* (sqrt (fma (* v v) -3 1)) (sqrt 2))
6.280 * [simplify]: Simplified (2 1 1) to (λ (v) (* (/ (* (sqrt (fma (* v v) -3 1)) (sqrt 2)) 4) (- 1 (* v v))))
6.280 * * * * [progress]: [ 76 / 83 ] simplifiying candidate #<alt (λ (v) (* (posit16->real (real->posit16 (* (/ (sqrt 2) 4) (sqrt (- 1 (* 3 (* v v))))))) (- 1 (* v v))))>
6.281 * * * * [progress]: [ 77 / 83 ] simplifiying candidate #<alt (λ (v) (* (* (sqrt (- 1 (* 3 (* v v)))) (/ (sqrt 2) 4)) (- 1 (* v v))))>
6.281 * * * * [progress]: [ 78 / 83 ] simplifiying candidate #<alt (λ (v) (* (* (/ (sqrt 2) 4) (sqrt (- 1 (* 3 (pow v 2))))) (- 1 (* v v))))>
6.281 * [simplify]: Simplifying (* 3 (pow v 2))
6.281 * * [simplify]: iters left: 3 (5 enodes)
6.285 * * [simplify]: iters left: 2 (21 enodes)
6.292 * * [simplify]: iters left: 1 (29 enodes)
6.301 * * [simplify]: Extracting #0: cost 1 inf + 0
6.301 * * [simplify]: Extracting #1: cost 6 inf + 0
6.302 * * [simplify]: Extracting #2: cost 6 inf + 43
6.302 * * [simplify]: Extracting #3: cost 0 inf + 333
6.302 * [simplify]: Simplified to (* (* v v) 3)
6.302 * [simplify]: Simplified (2 1 2 1 2) to (λ (v) (* (* (/ (sqrt 2) 4) (sqrt (- 1 (* (* v v) 3)))) (- 1 (* v v))))
6.302 * * * * [progress]: [ 79 / 83 ] simplifiying candidate #<alt (λ (v) (* (* (/ (sqrt 2) 4) (sqrt (- 1 (* 3 (pow v 2))))) (- 1 (* v v))))>
6.302 * [simplify]: Simplifying (* 3 (pow v 2))
6.303 * * [simplify]: iters left: 3 (5 enodes)
6.305 * * [simplify]: iters left: 2 (21 enodes)
6.308 * * [simplify]: iters left: 1 (29 enodes)
6.313 * * [simplify]: Extracting #0: cost 1 inf + 0
6.313 * * [simplify]: Extracting #1: cost 6 inf + 0
6.313 * * [simplify]: Extracting #2: cost 6 inf + 43
6.313 * * [simplify]: Extracting #3: cost 0 inf + 333
6.313 * [simplify]: Simplified to (* (* v v) 3)
6.313 * [simplify]: Simplified (2 1 2 1 2) to (λ (v) (* (* (/ (sqrt 2) 4) (sqrt (- 1 (* (* v v) 3)))) (- 1 (* v v))))
6.313 * * * * [progress]: [ 80 / 83 ] simplifiying candidate #<alt (λ (v) (* (* (/ (sqrt 2) 4) (sqrt (- 1 (* 3 (pow v 2))))) (- 1 (* v v))))>
6.313 * [simplify]: Simplifying (* 3 (pow v 2))
6.313 * * [simplify]: iters left: 3 (5 enodes)
6.316 * * [simplify]: iters left: 2 (21 enodes)
6.320 * * [simplify]: iters left: 1 (29 enodes)
6.324 * * [simplify]: Extracting #0: cost 1 inf + 0
6.324 * * [simplify]: Extracting #1: cost 6 inf + 0
6.325 * * [simplify]: Extracting #2: cost 6 inf + 43
6.325 * * [simplify]: Extracting #3: cost 0 inf + 333
6.325 * [simplify]: Simplified to (* (* v v) 3)
6.325 * [simplify]: Simplified (2 1 2 1 2) to (λ (v) (* (* (/ (sqrt 2) 4) (sqrt (- 1 (* (* v v) 3)))) (- 1 (* v v))))
6.325 * * * * [progress]: [ 81 / 83 ] simplifiying candidate #<alt (λ (v) (* (- (* 1/4 (sqrt 2)) (+ (* 9/32 (* (sqrt 2) (pow v 4))) (* 3/8 (* (sqrt 2) (pow v 2))))) (- 1 (* v v))))>
6.325 * [simplify]: Simplifying (- (* 1/4 (sqrt 2)) (+ (* 9/32 (* (sqrt 2) (pow v 4))) (* 3/8 (* (sqrt 2) (pow v 2)))))
6.325 * * [simplify]: iters left: 6 (16 enodes)
6.331 * * [simplify]: iters left: 5 (72 enodes)
6.356 * * [simplify]: iters left: 4 (121 enodes)
6.379 * * [simplify]: iters left: 3 (238 enodes)
6.493 * * [simplify]: Extracting #0: cost 1 inf + 0
6.493 * * [simplify]: Extracting #1: cost 51 inf + 0
6.494 * * [simplify]: Extracting #2: cost 115 inf + 128
6.496 * * [simplify]: Extracting #3: cost 95 inf + 2983
6.506 * * [simplify]: Extracting #4: cost 9 inf + 17469
6.520 * * [simplify]: Extracting #5: cost 0 inf + 19313
6.533 * * [simplify]: Extracting #6: cost 0 inf + 19258
6.547 * [simplify]: Simplified to (* (sqrt 2) (- 1/4 (* (* v v) (+ (* (* v v) 9/32) 3/8))))
6.547 * [simplify]: Simplified (2 1) to (λ (v) (* (* (sqrt 2) (- 1/4 (* (* v v) (+ (* (* v v) 9/32) 3/8)))) (- 1 (* v v))))
6.547 * * * * [progress]: [ 82 / 83 ] simplifiying candidate #<alt (λ (v) (* (- (+ (* 1/4 (* (sqrt 2) (* v (sqrt -3)))) (* 1/8 (/ (sqrt 2) (* v (sqrt -3))))) (* 1/32 (/ (sqrt 2) (* (pow v 3) (pow (sqrt -3) 3))))) (- 1 (* v v))))>
6.547 * [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)))))
6.547 * * [simplify]: iters left: 6 (21 enodes)
6.561 * * [simplify]: iters left: 5 (99 enodes)
6.603 * * [simplify]: iters left: 4 (247 enodes)
6.671 * * [simplify]: Extracting #0: cost 1 inf + 0
6.671 * * [simplify]: Extracting #1: cost 32 inf + 0
6.672 * * [simplify]: Extracting #2: cost 149 inf + 47
6.673 * * [simplify]: Extracting #3: cost 207 inf + 1649
6.676 * * [simplify]: Extracting #4: cost 120 inf + 14751
6.683 * * [simplify]: Extracting #5: cost 36 inf + 39050
6.701 * * [simplify]: Extracting #6: cost 8 inf + 49626
6.720 * * [simplify]: Extracting #7: cost 0 inf + 52681
6.739 * [simplify]: Simplified to (fma 1/8 (/ (/ (sqrt 2) v) (sqrt -3)) (- (* (* (* v (sqrt -3)) (sqrt 2)) 1/4) (/ (* (/ -1/96 (sqrt -3)) (/ (sqrt 2) v)) (* v v))))
6.739 * [simplify]: Simplified (2 1) to (λ (v) (* (fma 1/8 (/ (/ (sqrt 2) v) (sqrt -3)) (- (* (* (* v (sqrt -3)) (sqrt 2)) 1/4) (/ (* (/ -1/96 (sqrt -3)) (/ (sqrt 2) v)) (* v v)))) (- 1 (* v v))))
6.739 * * * * [progress]: [ 83 / 83 ] simplifiying candidate #<alt (λ (v) (* (- (* 1/32 (/ (sqrt 2) (* (pow v 3) (pow (sqrt -3) 3)))) (+ (* 1/4 (* (sqrt 2) (* v (sqrt -3)))) (* 1/8 (/ (sqrt 2) (* v (sqrt -3)))))) (- 1 (* v v))))>
6.740 * [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))))))
6.740 * * [simplify]: iters left: 6 (21 enodes)
6.754 * * [simplify]: iters left: 5 (100 enodes)
6.789 * * [simplify]: iters left: 4 (238 enodes)
6.867 * * [simplify]: Extracting #0: cost 1 inf + 0
6.867 * * [simplify]: Extracting #1: cost 19 inf + 0
6.867 * * [simplify]: Extracting #2: cost 148 inf + 1
6.868 * * [simplify]: Extracting #3: cost 226 inf + 378
6.871 * * [simplify]: Extracting #4: cost 128 inf + 13984
6.885 * * [simplify]: Extracting #5: cost 28 inf + 38842
6.903 * * [simplify]: Extracting #6: cost 1 inf + 50083
6.925 * * [simplify]: Extracting #7: cost 0 inf + 50417
6.936 * [simplify]: Simplified to (- (* (/ -1/96 (sqrt -3)) (/ (sqrt 2) (* v (* v v)))) (fma (* (sqrt 2) 1/4) (* v (sqrt -3)) (/ (* (sqrt 2) 1/8) (* v (sqrt -3)))))
6.936 * [simplify]: Simplified (2 1) to (λ (v) (* (- (* (/ -1/96 (sqrt -3)) (/ (sqrt 2) (* v (* v v)))) (fma (* (sqrt 2) 1/4) (* v (sqrt -3)) (/ (* (sqrt 2) 1/8) (* v (sqrt -3))))) (- 1 (* v v))))
6.937 * * * [progress]: adding candidates to table
7.718 * * [progress]: iteration 2 / 4
7.718 * * * [progress]: picking best candidate
7.724 * * * * [pick]: Picked  #<alt (λ (v) (* (* (* (cbrt (sqrt 2)) (cbrt (sqrt 2))) (* (/ (cbrt (sqrt 2)) 4) (sqrt (- 1 (* 3 (* v v)))))) (- 1 (* v v))))>
7.724 * * * [progress]: localizing error
7.768 * * * [progress]: generating rewritten candidates
7.768 * * * * [progress]: [ 1 / 1 ] rewriting at (2 1 2 2 1 2)
7.788 * * * [progress]: generating series expansions
7.788 * * * * [progress]: [ 1 / 1 ] generating series at (2 1 2 2 1 2)
7.788 * [backup-simplify]: Simplify (* 3 (* v v)) into (* 3 (pow v 2))
7.788 * [approximate]: Taking taylor expansion of (* 3 (pow v 2)) in (v) around 0
7.788 * [taylor]: Taking taylor expansion of (* 3 (pow v 2)) in v
7.788 * [taylor]: Taking taylor expansion of 3 in v
7.788 * [backup-simplify]: Simplify 3 into 3
7.788 * [taylor]: Taking taylor expansion of (pow v 2) in v
7.788 * [taylor]: Taking taylor expansion of v in v
7.788 * [backup-simplify]: Simplify 0 into 0
7.788 * [backup-simplify]: Simplify 1 into 1
7.788 * [taylor]: Taking taylor expansion of (* 3 (pow v 2)) in v
7.788 * [taylor]: Taking taylor expansion of 3 in v
7.788 * [backup-simplify]: Simplify 3 into 3
7.788 * [taylor]: Taking taylor expansion of (pow v 2) in v
7.788 * [taylor]: Taking taylor expansion of v in v
7.788 * [backup-simplify]: Simplify 0 into 0
7.788 * [backup-simplify]: Simplify 1 into 1
7.789 * [backup-simplify]: Simplify (* 1 1) into 1
7.790 * [backup-simplify]: Simplify (* 3 1) into 3
7.790 * [backup-simplify]: Simplify 3 into 3
7.791 * [backup-simplify]: Simplify (+ (* 1 0) (* 0 1)) into 0
7.791 * [backup-simplify]: Simplify (+ (* 3 0) (* 0 1)) into 0
7.791 * [backup-simplify]: Simplify 0 into 0
7.792 * [backup-simplify]: Simplify (+ (* 1 0) (+ (* 0 0) (* 0 1))) into 0
7.793 * [backup-simplify]: Simplify (+ (* 3 0) (+ (* 0 0) (* 0 1))) into 0
7.793 * [backup-simplify]: Simplify 0 into 0
7.794 * [backup-simplify]: Simplify (+ (* 1 0) (+ (* 0 0) (+ (* 0 0) (* 0 1)))) into 0
7.795 * [backup-simplify]: Simplify (+ (* 3 0) (+ (* 0 0) (+ (* 0 0) (* 0 1)))) into 0
7.795 * [backup-simplify]: Simplify 0 into 0
7.797 * [backup-simplify]: Simplify (+ (* 1 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (* 0 1))))) into 0
7.798 * [backup-simplify]: Simplify (+ (* 3 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (* 0 1))))) into 0
7.798 * [backup-simplify]: Simplify 0 into 0
7.799 * [backup-simplify]: Simplify (+ (* 1 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (* 0 1)))))) into 0
7.801 * [backup-simplify]: Simplify (+ (* 3 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (* 0 1)))))) into 0
7.801 * [backup-simplify]: Simplify 0 into 0
7.802 * [backup-simplify]: Simplify (+ (* 1 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (* 0 1))))))) into 0
7.804 * [backup-simplify]: Simplify (+ (* 3 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (* 0 1))))))) into 0
7.804 * [backup-simplify]: Simplify 0 into 0
7.804 * [backup-simplify]: Simplify (* 3 (pow v 2)) into (* 3 (pow v 2))
7.804 * [backup-simplify]: Simplify (* 3 (* (/ 1 v) (/ 1 v))) into (/ 3 (pow v 2))
7.804 * [approximate]: Taking taylor expansion of (/ 3 (pow v 2)) in (v) around 0
7.804 * [taylor]: Taking taylor expansion of (/ 3 (pow v 2)) in v
7.804 * [taylor]: Taking taylor expansion of 3 in v
7.804 * [backup-simplify]: Simplify 3 into 3
7.804 * [taylor]: Taking taylor expansion of (pow v 2) in v
7.805 * [taylor]: Taking taylor expansion of v in v
7.805 * [backup-simplify]: Simplify 0 into 0
7.805 * [backup-simplify]: Simplify 1 into 1
7.805 * [backup-simplify]: Simplify (* 1 1) into 1
7.805 * [backup-simplify]: Simplify (/ 3 1) into 3
7.805 * [taylor]: Taking taylor expansion of (/ 3 (pow v 2)) in v
7.805 * [taylor]: Taking taylor expansion of 3 in v
7.805 * [backup-simplify]: Simplify 3 into 3
7.805 * [taylor]: Taking taylor expansion of (pow v 2) in v
7.805 * [taylor]: Taking taylor expansion of v in v
7.805 * [backup-simplify]: Simplify 0 into 0
7.806 * [backup-simplify]: Simplify 1 into 1
7.806 * [backup-simplify]: Simplify (* 1 1) into 1
7.806 * [backup-simplify]: Simplify (/ 3 1) into 3
7.806 * [backup-simplify]: Simplify 3 into 3
7.807 * [backup-simplify]: Simplify (+ (* 1 0) (* 0 1)) into 0
7.808 * [backup-simplify]: Simplify (- (/ 0 1) (+ (* 3 (/ 0 1)))) into 0
7.808 * [backup-simplify]: Simplify 0 into 0
7.809 * [backup-simplify]: Simplify (+ (* 1 0) (+ (* 0 0) (* 0 1))) into 0
7.810 * [backup-simplify]: Simplify (- (/ 0 1) (+ (* 3 (/ 0 1)) (* 0 (/ 0 1)))) into 0
7.810 * [backup-simplify]: Simplify 0 into 0
7.811 * [backup-simplify]: Simplify (+ (* 1 0) (+ (* 0 0) (+ (* 0 0) (* 0 1)))) into 0
7.812 * [backup-simplify]: Simplify (- (/ 0 1) (+ (* 3 (/ 0 1)) (* 0 (/ 0 1)) (* 0 (/ 0 1)))) into 0
7.812 * [backup-simplify]: Simplify 0 into 0
7.813 * [backup-simplify]: Simplify (+ (* 1 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (* 0 1))))) into 0
7.814 * [backup-simplify]: Simplify (- (/ 0 1) (+ (* 3 (/ 0 1)) (* 0 (/ 0 1)) (* 0 (/ 0 1)) (* 0 (/ 0 1)))) into 0
7.814 * [backup-simplify]: Simplify 0 into 0
7.816 * [backup-simplify]: Simplify (+ (* 1 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (* 0 1)))))) into 0
7.817 * [backup-simplify]: Simplify (- (/ 0 1) (+ (* 3 (/ 0 1)) (* 0 (/ 0 1)) (* 0 (/ 0 1)) (* 0 (/ 0 1)) (* 0 (/ 0 1)))) into 0
7.817 * [backup-simplify]: Simplify 0 into 0
7.818 * [backup-simplify]: Simplify (+ (* 1 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (* 0 1))))))) into 0
7.819 * [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
7.819 * [backup-simplify]: Simplify 0 into 0
7.820 * [backup-simplify]: Simplify (* 3 (pow (/ 1 (/ 1 v)) 2)) into (* 3 (pow v 2))
7.820 * [backup-simplify]: Simplify (* 3 (* (/ 1 (- v)) (/ 1 (- v)))) into (/ 3 (pow v 2))
7.820 * [approximate]: Taking taylor expansion of (/ 3 (pow v 2)) in (v) around 0
7.820 * [taylor]: Taking taylor expansion of (/ 3 (pow v 2)) in v
7.820 * [taylor]: Taking taylor expansion of 3 in v
7.820 * [backup-simplify]: Simplify 3 into 3
7.820 * [taylor]: Taking taylor expansion of (pow v 2) in v
7.820 * [taylor]: Taking taylor expansion of v in v
7.820 * [backup-simplify]: Simplify 0 into 0
7.820 * [backup-simplify]: Simplify 1 into 1
7.820 * [backup-simplify]: Simplify (* 1 1) into 1
7.821 * [backup-simplify]: Simplify (/ 3 1) into 3
7.821 * [taylor]: Taking taylor expansion of (/ 3 (pow v 2)) in v
7.821 * [taylor]: Taking taylor expansion of 3 in v
7.821 * [backup-simplify]: Simplify 3 into 3
7.821 * [taylor]: Taking taylor expansion of (pow v 2) in v
7.821 * [taylor]: Taking taylor expansion of v in v
7.821 * [backup-simplify]: Simplify 0 into 0
7.821 * [backup-simplify]: Simplify 1 into 1
7.821 * [backup-simplify]: Simplify (* 1 1) into 1
7.822 * [backup-simplify]: Simplify (/ 3 1) into 3
7.822 * [backup-simplify]: Simplify 3 into 3
7.822 * [backup-simplify]: Simplify (+ (* 1 0) (* 0 1)) into 0
7.823 * [backup-simplify]: Simplify (- (/ 0 1) (+ (* 3 (/ 0 1)))) into 0
7.823 * [backup-simplify]: Simplify 0 into 0
7.824 * [backup-simplify]: Simplify (+ (* 1 0) (+ (* 0 0) (* 0 1))) into 0
7.824 * [backup-simplify]: Simplify (- (/ 0 1) (+ (* 3 (/ 0 1)) (* 0 (/ 0 1)))) into 0
7.824 * [backup-simplify]: Simplify 0 into 0
7.825 * [backup-simplify]: Simplify (+ (* 1 0) (+ (* 0 0) (+ (* 0 0) (* 0 1)))) into 0
7.825 * [backup-simplify]: Simplify (- (/ 0 1) (+ (* 3 (/ 0 1)) (* 0 (/ 0 1)) (* 0 (/ 0 1)))) into 0
7.825 * [backup-simplify]: Simplify 0 into 0
7.826 * [backup-simplify]: Simplify (+ (* 1 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (* 0 1))))) into 0
7.827 * [backup-simplify]: Simplify (- (/ 0 1) (+ (* 3 (/ 0 1)) (* 0 (/ 0 1)) (* 0 (/ 0 1)) (* 0 (/ 0 1)))) into 0
7.827 * [backup-simplify]: Simplify 0 into 0
7.827 * [backup-simplify]: Simplify (+ (* 1 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (* 0 1)))))) into 0
7.828 * [backup-simplify]: Simplify (- (/ 0 1) (+ (* 3 (/ 0 1)) (* 0 (/ 0 1)) (* 0 (/ 0 1)) (* 0 (/ 0 1)) (* 0 (/ 0 1)))) into 0
7.828 * [backup-simplify]: Simplify 0 into 0
7.829 * [backup-simplify]: Simplify (+ (* 1 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (* 0 1))))))) into 0
7.829 * [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
7.829 * [backup-simplify]: Simplify 0 into 0
7.829 * [backup-simplify]: Simplify (* 3 (pow (/ 1 (/ 1 (- v))) 2)) into (* 3 (pow v 2))
7.829 * * * [progress]: simplifying candidates
7.830 * * * * [progress]: [ 1 / 25 ] simplifiying candidate #<alt (λ (v) (* (* (* (cbrt (sqrt 2)) (cbrt (sqrt 2))) (* (/ (cbrt (sqrt 2)) 4) (sqrt (- 1 (log1p (expm1 (* 3 (* v v)))))))) (- 1 (* v v))))>
7.830 * * * * [progress]: [ 2 / 25 ] simplifiying candidate #<alt (λ (v) (* (* (* (cbrt (sqrt 2)) (cbrt (sqrt 2))) (* (/ (cbrt (sqrt 2)) 4) (sqrt (- 1 (expm1 (log1p (* 3 (* v v)))))))) (- 1 (* v v))))>
7.830 * * * * [progress]: [ 3 / 25 ] simplifiying candidate #<alt (λ (v) (* (* (* (cbrt (sqrt 2)) (cbrt (sqrt 2))) (* (/ (cbrt (sqrt 2)) 4) (sqrt (- 1 (pow (* 3 (* v v)) 1))))) (- 1 (* v v))))>
7.830 * [simplify]: Simplifying (* 3 (* v v))
7.830 * * [simplify]: iters left: 4 (4 enodes)
7.831 * * [simplify]: iters left: 3 (15 enodes)
7.834 * * [simplify]: iters left: 2 (19 enodes)
7.837 * * [simplify]: Extracting #0: cost 1 inf + 0
7.837 * * [simplify]: Extracting #1: cost 6 inf + 0
7.837 * * [simplify]: Extracting #2: cost 5 inf + 43
7.837 * * [simplify]: Extracting #3: cost 0 inf + 332
7.837 * [simplify]: Simplified to (* 3 (* v v))
7.837 * [simplify]: Simplified (2 1 2 2 1 2 1) to (λ (v) (* (* (* (cbrt (sqrt 2)) (cbrt (sqrt 2))) (* (/ (cbrt (sqrt 2)) 4) (sqrt (- 1 (pow (* 3 (* v v)) 1))))) (- 1 (* v v))))
7.837 * * * * [progress]: [ 4 / 25 ] simplifiying candidate #<alt (λ (v) (* (* (* (cbrt (sqrt 2)) (cbrt (sqrt 2))) (* (/ (cbrt (sqrt 2)) 4) (sqrt (- 1 (pow (* 3 (* v v)) 1))))) (- 1 (* v v))))>
7.838 * [simplify]: Simplifying (* 3 (* v v))
7.838 * * [simplify]: iters left: 4 (4 enodes)
7.839 * * [simplify]: iters left: 3 (15 enodes)
7.842 * * [simplify]: iters left: 2 (19 enodes)
7.845 * * [simplify]: Extracting #0: cost 1 inf + 0
7.845 * * [simplify]: Extracting #1: cost 6 inf + 0
7.845 * * [simplify]: Extracting #2: cost 5 inf + 43
7.845 * * [simplify]: Extracting #3: cost 0 inf + 332
7.845 * [simplify]: Simplified to (* 3 (* v v))
7.845 * [simplify]: Simplified (2 1 2 2 1 2 1) to (λ (v) (* (* (* (cbrt (sqrt 2)) (cbrt (sqrt 2))) (* (/ (cbrt (sqrt 2)) 4) (sqrt (- 1 (pow (* 3 (* v v)) 1))))) (- 1 (* v v))))
7.845 * * * * [progress]: [ 5 / 25 ] simplifiying candidate #<alt (λ (v) (* (* (* (cbrt (sqrt 2)) (cbrt (sqrt 2))) (* (/ (cbrt (sqrt 2)) 4) (sqrt (- 1 (pow (* 3 (* v v)) 1))))) (- 1 (* v v))))>
7.845 * * * * [progress]: [ 6 / 25 ] simplifiying candidate #<alt (λ (v) (* (* (* (cbrt (sqrt 2)) (cbrt (sqrt 2))) (* (/ (cbrt (sqrt 2)) 4) (sqrt (- 1 (exp (+ (log 3) (+ (log v) (log v)))))))) (- 1 (* v v))))>
7.845 * [simplify]: Simplifying (+ (log 3) (+ (log v) (log v)))
7.845 * * [simplify]: iters left: 5 (6 enodes)
7.847 * * [simplify]: iters left: 4 (21 enodes)
7.851 * * [simplify]: iters left: 3 (25 enodes)
7.858 * * [simplify]: Extracting #0: cost 1 inf + 0
7.858 * * [simplify]: Extracting #1: cost 6 inf + 0
7.858 * * [simplify]: Extracting #2: cost 12 inf + 0
7.858 * * [simplify]: Extracting #3: cost 10 inf + 2
7.859 * * [simplify]: Extracting #4: cost 0 inf + 1316
7.859 * [simplify]: Simplified to (+ (log 3) (+ (log v) (log v)))
7.859 * [simplify]: Simplified (2 1 2 2 1 2 1) to (λ (v) (* (* (* (cbrt (sqrt 2)) (cbrt (sqrt 2))) (* (/ (cbrt (sqrt 2)) 4) (sqrt (- 1 (exp (+ (log 3) (+ (log v) (log v)))))))) (- 1 (* v v))))
7.859 * * * * [progress]: [ 7 / 25 ] simplifiying candidate #<alt (λ (v) (* (* (* (cbrt (sqrt 2)) (cbrt (sqrt 2))) (* (/ (cbrt (sqrt 2)) 4) (sqrt (- 1 (exp (+ (log 3) (log (* v v)))))))) (- 1 (* v v))))>
7.859 * [simplify]: Simplifying (+ (log 3) (log (* v v)))
7.860 * * [simplify]: iters left: 5 (6 enodes)
7.863 * * [simplify]: iters left: 4 (21 enodes)
7.873 * * [simplify]: iters left: 3 (27 enodes)
7.880 * * [simplify]: iters left: 2 (32 enodes)
7.885 * * [simplify]: Extracting #0: cost 1 inf + 0
7.885 * * [simplify]: Extracting #1: cost 6 inf + 0
7.885 * * [simplify]: Extracting #2: cost 13 inf + 0
7.885 * * [simplify]: Extracting #3: cost 9 inf + 185
7.885 * * [simplify]: Extracting #4: cost 4 inf + 741
7.885 * * [simplify]: Extracting #5: cost 0 inf + 1398
7.885 * [simplify]: Simplified to (+ (log 3) (+ (log v) (log v)))
7.886 * [simplify]: Simplified (2 1 2 2 1 2 1) to (λ (v) (* (* (* (cbrt (sqrt 2)) (cbrt (sqrt 2))) (* (/ (cbrt (sqrt 2)) 4) (sqrt (- 1 (exp (+ (log 3) (+ (log v) (log v)))))))) (- 1 (* v v))))
7.886 * * * * [progress]: [ 8 / 25 ] simplifiying candidate #<alt (λ (v) (* (* (* (cbrt (sqrt 2)) (cbrt (sqrt 2))) (* (/ (cbrt (sqrt 2)) 4) (sqrt (- 1 (exp (log (* 3 (* v v)))))))) (- 1 (* v v))))>
7.886 * * * * [progress]: [ 9 / 25 ] simplifiying candidate #<alt (λ (v) (* (* (* (cbrt (sqrt 2)) (cbrt (sqrt 2))) (* (/ (cbrt (sqrt 2)) 4) (sqrt (- 1 (log (exp (* 3 (* v v)))))))) (- 1 (* v v))))>
7.886 * * * * [progress]: [ 10 / 25 ] simplifiying candidate #<alt (λ (v) (* (* (* (cbrt (sqrt 2)) (cbrt (sqrt 2))) (* (/ (cbrt (sqrt 2)) 4) (sqrt (- 1 (cbrt (* (* (* 3 3) 3) (* (* (* v v) v) (* (* v v) v)))))))) (- 1 (* v v))))>
7.886 * [simplify]: Simplifying (* (* (* 3 3) 3) (* (* (* v v) v) (* (* v v) v)))
7.886 * * [simplify]: iters left: 6 (8 enodes)
7.889 * * [simplify]: iters left: 5 (38 enodes)
7.899 * * [simplify]: iters left: 4 (96 enodes)
7.925 * * [simplify]: iters left: 3 (265 enodes)
8.073 * * [simplify]: Extracting #0: cost 1 inf + 0
8.073 * * [simplify]: Extracting #1: cost 54 inf + 0
8.074 * * [simplify]: Extracting #2: cost 83 inf + 1839
8.078 * * [simplify]: Extracting #3: cost 30 inf + 7514
8.085 * * [simplify]: Extracting #4: cost 8 inf + 12317
8.092 * * [simplify]: Extracting #5: cost 0 inf + 14739
8.099 * [simplify]: Simplified to (* 27 (* (* v (* v v)) (* v (* v v))))
8.099 * [simplify]: Simplified (2 1 2 2 1 2 1) to (λ (v) (* (* (* (cbrt (sqrt 2)) (cbrt (sqrt 2))) (* (/ (cbrt (sqrt 2)) 4) (sqrt (- 1 (cbrt (* 27 (* (* v (* v v)) (* v (* v v))))))))) (- 1 (* v v))))
8.100 * * * * [progress]: [ 11 / 25 ] simplifiying candidate #<alt (λ (v) (* (* (* (cbrt (sqrt 2)) (cbrt (sqrt 2))) (* (/ (cbrt (sqrt 2)) 4) (sqrt (- 1 (cbrt (* (* (* 3 3) 3) (* (* (* v v) (* v v)) (* v v)))))))) (- 1 (* v v))))>
8.100 * [simplify]: Simplifying (* (* (* 3 3) 3) (* (* (* v v) (* v v)) (* v v)))
8.100 * * [simplify]: iters left: 6 (8 enodes)
8.106 * * [simplify]: iters left: 5 (39 enodes)
8.124 * * [simplify]: iters left: 4 (96 enodes)
8.148 * * [simplify]: iters left: 3 (269 enodes)
8.322 * * [simplify]: Extracting #0: cost 1 inf + 0
8.322 * * [simplify]: Extracting #1: cost 72 inf + 0
8.323 * * [simplify]: Extracting #2: cost 120 inf + 818
8.326 * * [simplify]: Extracting #3: cost 39 inf + 12504
8.330 * * [simplify]: Extracting #4: cost 1 inf + 19795
8.337 * * [simplify]: Extracting #5: cost 0 inf + 20047
8.344 * [simplify]: Simplified to (* (* v v) (* (* (* v v) (* v v)) 27))
8.344 * [simplify]: Simplified (2 1 2 2 1 2 1) to (λ (v) (* (* (* (cbrt (sqrt 2)) (cbrt (sqrt 2))) (* (/ (cbrt (sqrt 2)) 4) (sqrt (- 1 (cbrt (* (* v v) (* (* (* v v) (* v v)) 27))))))) (- 1 (* v v))))
8.344 * * * * [progress]: [ 12 / 25 ] simplifiying candidate #<alt (λ (v) (* (* (* (cbrt (sqrt 2)) (cbrt (sqrt 2))) (* (/ (cbrt (sqrt 2)) 4) (sqrt (- 1 (* (* (cbrt (* 3 (* v v))) (cbrt (* 3 (* v v)))) (cbrt (* 3 (* v v)))))))) (- 1 (* v v))))>
8.344 * * * * [progress]: [ 13 / 25 ] simplifiying candidate #<alt (λ (v) (* (* (* (cbrt (sqrt 2)) (cbrt (sqrt 2))) (* (/ (cbrt (sqrt 2)) 4) (sqrt (- 1 (cbrt (* (* (* 3 (* v v)) (* 3 (* v v))) (* 3 (* v v)))))))) (- 1 (* v v))))>
8.344 * * * * [progress]: [ 14 / 25 ] simplifiying candidate #<alt (λ (v) (* (* (* (cbrt (sqrt 2)) (cbrt (sqrt 2))) (* (/ (cbrt (sqrt 2)) 4) (sqrt (- 1 (* (sqrt (* 3 (* v v))) (sqrt (* 3 (* v v)))))))) (- 1 (* v v))))>
8.344 * * * * [progress]: [ 15 / 25 ] simplifiying candidate #<alt (λ (v) (* (* (* (cbrt (sqrt 2)) (cbrt (sqrt 2))) (* (/ (cbrt (sqrt 2)) 4) (sqrt (- 1 (* 1 (* 3 (* v v))))))) (- 1 (* v v))))>
8.344 * * * * [progress]: [ 16 / 25 ] simplifiying candidate #<alt (λ (v) (* (* (* (cbrt (sqrt 2)) (cbrt (sqrt 2))) (* (/ (cbrt (sqrt 2)) 4) (sqrt (- 1 (* (* (sqrt 3) v) (* (sqrt 3) v)))))) (- 1 (* v v))))>
8.345 * [simplify]: Simplifying (* (sqrt 3) v)
8.345 * * [simplify]: iters left: 3 (4 enodes)
8.346 * * [simplify]: iters left: 2 (13 enodes)
8.348 * * [simplify]: Extracting #0: cost 1 inf + 0
8.348 * * [simplify]: Extracting #1: cost 4 inf + 0
8.348 * * [simplify]: Extracting #2: cost 5 inf + 1
8.349 * * [simplify]: Extracting #3: cost 4 inf + 2
8.349 * * [simplify]: Extracting #4: cost 0 inf + 248
8.349 * [simplify]: Simplified to (* v (sqrt 3))
8.349 * [simplify]: Simplified (2 1 2 2 1 2 1) to (λ (v) (* (* (* (cbrt (sqrt 2)) (cbrt (sqrt 2))) (* (/ (cbrt (sqrt 2)) 4) (sqrt (- 1 (* (* v (sqrt 3)) (* (sqrt 3) v)))))) (- 1 (* v v))))
8.349 * [simplify]: Simplifying (* (sqrt 3) v)
8.349 * * [simplify]: iters left: 3 (4 enodes)
8.351 * * [simplify]: iters left: 2 (13 enodes)
8.353 * * [simplify]: Extracting #0: cost 1 inf + 0
8.353 * * [simplify]: Extracting #1: cost 4 inf + 0
8.353 * * [simplify]: Extracting #2: cost 5 inf + 1
8.353 * * [simplify]: Extracting #3: cost 4 inf + 2
8.353 * * [simplify]: Extracting #4: cost 0 inf + 248
8.353 * [simplify]: Simplified to (* v (sqrt 3))
8.353 * [simplify]: Simplified (2 1 2 2 1 2 2) to (λ (v) (* (* (* (cbrt (sqrt 2)) (cbrt (sqrt 2))) (* (/ (cbrt (sqrt 2)) 4) (sqrt (- 1 (* (* (sqrt 3) v) (* v (sqrt 3))))))) (- 1 (* v v))))
8.353 * * * * [progress]: [ 17 / 25 ] simplifiying candidate #<alt (λ (v) (* (* (* (cbrt (sqrt 2)) (cbrt (sqrt 2))) (* (/ (cbrt (sqrt 2)) 4) (sqrt (- 1 (* (* 3 v) v))))) (- 1 (* v v))))>
8.354 * * * * [progress]: [ 18 / 25 ] simplifiying candidate #<alt (λ (v) (* (* (* (cbrt (sqrt 2)) (cbrt (sqrt 2))) (* (/ (cbrt (sqrt 2)) 4) (sqrt (- 1 (* (* (cbrt 3) (cbrt 3)) (* (cbrt 3) (* v v))))))) (- 1 (* v v))))>
8.354 * [simplify]: Simplifying (* (cbrt 3) (cbrt 3))
8.354 * * [simplify]: iters left: 3 (3 enodes)
8.355 * * [simplify]: iters left: 2 (9 enodes)
8.357 * * [simplify]: Extracting #0: cost 1 inf + 0
8.357 * * [simplify]: Extracting #1: cost 3 inf + 0
8.357 * * [simplify]: Extracting #2: cost 5 inf + 0
8.357 * * [simplify]: Extracting #3: cost 4 inf + 1
8.357 * * [simplify]: Extracting #4: cost 0 inf + 405
8.357 * [simplify]: Simplified to (* (cbrt 3) (cbrt 3))
8.357 * [simplify]: Simplified (2 1 2 2 1 2 1) to (λ (v) (* (* (* (cbrt (sqrt 2)) (cbrt (sqrt 2))) (* (/ (cbrt (sqrt 2)) 4) (sqrt (- 1 (* (* (cbrt 3) (cbrt 3)) (* (cbrt 3) (* v v))))))) (- 1 (* v v))))
8.358 * * * * [progress]: [ 19 / 25 ] simplifiying candidate #<alt (λ (v) (* (* (* (cbrt (sqrt 2)) (cbrt (sqrt 2))) (* (/ (cbrt (sqrt 2)) 4) (sqrt (- 1 (* (sqrt 3) (* (sqrt 3) (* v v))))))) (- 1 (* v v))))>
8.358 * [simplify]: Simplifying (sqrt 3)
8.358 * * [simplify]: iters left: 1 (2 enodes)
8.359 * * [simplify]: Extracting #0: cost 1 inf + 0
8.359 * * [simplify]: Extracting #1: cost 3 inf + 0
8.359 * * [simplify]: Extracting #2: cost 2 inf + 1
8.359 * * [simplify]: Extracting #3: cost 0 inf + 83
8.359 * [simplify]: Simplified to (sqrt 3)
8.359 * [simplify]: Simplified (2 1 2 2 1 2 1) to (λ (v) (* (* (* (cbrt (sqrt 2)) (cbrt (sqrt 2))) (* (/ (cbrt (sqrt 2)) 4) (sqrt (- 1 (* (sqrt 3) (* (sqrt 3) (* v v))))))) (- 1 (* v v))))
8.359 * * * * [progress]: [ 20 / 25 ] simplifiying candidate #<alt (λ (v) (* (* (* (cbrt (sqrt 2)) (cbrt (sqrt 2))) (* (/ (cbrt (sqrt 2)) 4) (sqrt (- 1 (* 1 (* 3 (* v v))))))) (- 1 (* v v))))>
8.359 * * * * [progress]: [ 21 / 25 ] simplifiying candidate #<alt (λ (v) (* (* (* (cbrt (sqrt 2)) (cbrt (sqrt 2))) (* (/ (cbrt (sqrt 2)) 4) (sqrt (- 1 (posit16->real (real->posit16 (* 3 (* v v)))))))) (- 1 (* v v))))>
8.359 * * * * [progress]: [ 22 / 25 ] simplifiying candidate #<alt (λ (v) (* (* (* (cbrt (sqrt 2)) (cbrt (sqrt 2))) (* (/ (cbrt (sqrt 2)) 4) (sqrt (- 1 (* (* v v) 3))))) (- 1 (* v v))))>
8.359 * * * * [progress]: [ 23 / 25 ] simplifiying candidate #<alt (λ (v) (* (* (* (cbrt (sqrt 2)) (cbrt (sqrt 2))) (* (/ (cbrt (sqrt 2)) 4) (sqrt (- 1 (* 3 (pow v 2)))))) (- 1 (* v v))))>
8.359 * [simplify]: Simplifying (* 3 (pow v 2))
8.359 * * [simplify]: iters left: 3 (5 enodes)
8.361 * * [simplify]: iters left: 2 (21 enodes)
8.365 * * [simplify]: iters left: 1 (29 enodes)
8.369 * * [simplify]: Extracting #0: cost 1 inf + 0
8.369 * * [simplify]: Extracting #1: cost 6 inf + 0
8.370 * * [simplify]: Extracting #2: cost 6 inf + 43
8.370 * * [simplify]: Extracting #3: cost 0 inf + 333
8.370 * [simplify]: Simplified to (* (* v v) 3)
8.370 * [simplify]: Simplified (2 1 2 2 1 2) to (λ (v) (* (* (* (cbrt (sqrt 2)) (cbrt (sqrt 2))) (* (/ (cbrt (sqrt 2)) 4) (sqrt (- 1 (* (* v v) 3))))) (- 1 (* v v))))
8.370 * * * * [progress]: [ 24 / 25 ] simplifiying candidate #<alt (λ (v) (* (* (* (cbrt (sqrt 2)) (cbrt (sqrt 2))) (* (/ (cbrt (sqrt 2)) 4) (sqrt (- 1 (* 3 (pow v 2)))))) (- 1 (* v v))))>
8.370 * [simplify]: Simplifying (* 3 (pow v 2))
8.370 * * [simplify]: iters left: 3 (5 enodes)
8.372 * * [simplify]: iters left: 2 (21 enodes)
8.376 * * [simplify]: iters left: 1 (29 enodes)
8.385 * * [simplify]: Extracting #0: cost 1 inf + 0
8.386 * * [simplify]: Extracting #1: cost 6 inf + 0
8.386 * * [simplify]: Extracting #2: cost 6 inf + 43
8.386 * * [simplify]: Extracting #3: cost 0 inf + 333
8.386 * [simplify]: Simplified to (* (* v v) 3)
8.386 * [simplify]: Simplified (2 1 2 2 1 2) to (λ (v) (* (* (* (cbrt (sqrt 2)) (cbrt (sqrt 2))) (* (/ (cbrt (sqrt 2)) 4) (sqrt (- 1 (* (* v v) 3))))) (- 1 (* v v))))
8.386 * * * * [progress]: [ 25 / 25 ] simplifiying candidate #<alt (λ (v) (* (* (* (cbrt (sqrt 2)) (cbrt (sqrt 2))) (* (/ (cbrt (sqrt 2)) 4) (sqrt (- 1 (* 3 (pow v 2)))))) (- 1 (* v v))))>
8.387 * [simplify]: Simplifying (* 3 (pow v 2))
8.387 * * [simplify]: iters left: 3 (5 enodes)
8.390 * * [simplify]: iters left: 2 (21 enodes)
8.398 * * [simplify]: iters left: 1 (29 enodes)
8.407 * * [simplify]: Extracting #0: cost 1 inf + 0
8.407 * * [simplify]: Extracting #1: cost 6 inf + 0
8.407 * * [simplify]: Extracting #2: cost 6 inf + 43
8.407 * * [simplify]: Extracting #3: cost 0 inf + 333
8.408 * [simplify]: Simplified to (* (* v v) 3)
8.408 * [simplify]: Simplified (2 1 2 2 1 2) to (λ (v) (* (* (* (cbrt (sqrt 2)) (cbrt (sqrt 2))) (* (/ (cbrt (sqrt 2)) 4) (sqrt (- 1 (* (* v v) 3))))) (- 1 (* v v))))
8.408 * * * [progress]: adding candidates to table
8.731 * [progress]: [Phase 3 of 3] Extracting.
8.738 * [simplify]: Simplifying (* (* (* (cbrt (sqrt 2)) (cbrt (sqrt 2))) (* (/ (cbrt (sqrt 2)) 4) (sqrt (- 1 (* 3 (* v v)))))) (- 1 (* v v)))
8.738 * * [simplify]: iters left: 6 (17 enodes)
8.740 * * [simplify]: iters left: 5 (23 enodes)
8.742 * * [simplify]: Extracting #0: cost 1 inf + 0
8.742 * * [simplify]: Extracting #1: cost 3 inf + 0
8.742 * * [simplify]: Extracting #2: cost 7 inf + 0
8.742 * * [simplify]: Extracting #3: cost 10 inf + 1
8.742 * * [simplify]: Extracting #4: cost 10 inf + 125
8.742 * * [simplify]: Extracting #5: cost 11 inf + 126
8.742 * * [simplify]: Extracting #6: cost 11 inf + 127
8.742 * * [simplify]: Extracting #7: cost 9 inf + 169
8.743 * * [simplify]: Extracting #8: cost 4 inf + 818
8.743 * * [simplify]: Extracting #9: cost 2 inf + 1346
8.744 * * [simplify]: Extracting #10: cost 0 inf + 2316
8.744 * [simplify]: Simplified to (* (- 1 (* v v)) (* (* (cbrt (sqrt 2)) (cbrt (sqrt 2))) (* (sqrt (- 1 (* (* v v) 3))) (/ (cbrt (sqrt 2)) 4))))
11.891 * [regime-testing]: Baseline error score: 0.013367272472009724
11.892 * [regime-testing]: Oracle error score: 0.013367272472009724
11.892 * [regime-testing]: End program error score: 0.013367272472009724