1538300352.641 * [misc]progress:  [Phase 1 of 3] Setting up.
1538300352.641 * * * [misc]progress:  [1/2] Preparing points
1538300352.641 * * * * [misc]points:  Sampling 256 additional inputs, on iter 0 have 0 / 256
1538300352.735 * * * * [misc]points:  Filtering points with unrepresentable outputs
1538300352.735 * * * * [misc]points:  Sampling 126 additional inputs, on iter 1 have 130 / 256
1538300352.810 * * * * [misc]points:  Filtering points with unrepresentable outputs
1538300352.810 * * * * [misc]points:  Sampling 61 additional inputs, on iter 2 have 195 / 256
1538300352.841 * * * * [misc]points:  Filtering points with unrepresentable outputs
1538300352.841 * * * * [misc]points:  Sampling 33 additional inputs, on iter 3 have 223 / 256
1538300352.863 * * * * [misc]points:  Filtering points with unrepresentable outputs
1538300352.863 * * * * [misc]points:  Sampling 17 additional inputs, on iter 4 have 239 / 256
1538300352.878 * * * * [misc]points:  Filtering points with unrepresentable outputs
1538300352.878 * * * * [misc]points:  Sampling 10 additional inputs, on iter 5 have 246 / 256
1538300352.889 * * * * [misc]points:  Filtering points with unrepresentable outputs
1538300352.889 * * * * [misc]points:  Sampling 4 additional inputs, on iter 6 have 252 / 256
1538300352.896 * * * * [misc]points:  Filtering points with unrepresentable outputs
1538300352.896 * * * * [misc]points:  Sampling 4 additional inputs, on iter 7 have 253 / 256
1538300352.900 * * * * [misc]points:  Filtering points with unrepresentable outputs
1538300352.900 * * * * [misc]points:  Sampling 4 additional inputs, on iter 8 have 255 / 256
1538300352.904 * * * * [misc]points:  Filtering points with unrepresentable outputs
1538300352.904 * * * * [exit]points:  Sampled 259 points with exact outputs
1538300352.905 * * * [misc]progress:  [2/2] Setting up program.
1538300352.912 * [misc]progress:  [Phase 2 of 3] Improving.
1538300352.912 * [enter]simplify:  Simplifying (/ 4 (* (* (* 3 PI) (- 1 (* v v))) (sqrt (- 2 (* 6 (* v v))))))
1538300352.913 * * [misc]simplify:  iters left: 6 (16 enodes)
1538300352.917 * * [misc]simplify:  iters left: 5 (34 enodes)
1538300352.960 * * [misc]simplify:  iters left: 4 (89 enodes)
1538300353.014 * * [misc]simplify:  iters left: 3 (198 enodes)
1538300353.220 * [exit]simplify:  Simplified to (/ (/ (/ 4/3 PI) (- 1 (* v v))) (sqrt (fma -6 (* v v) 2)))
1538300353.246 * * [misc]progress:  iteration 1 / 4
1538300353.246 * * * [misc]progress:  picking best candidate
1538300353.258 * * * * [misc]pick:  Picked  #<alt (λ (v) (/ (/ (/ 4/3 PI) (- 1 (* v v))) (sqrt (fma -6 (* v v) 2))))>
1538300353.258 * * * [misc]progress:  localizing error
1538300353.307 * * * [misc]progress:  generating rewritten candidates
1538300353.307 * * * * [misc]progress:  [ 1 / 2 ] rewriting at (2 1 1)
1538300353.309 * * * * [misc]progress:  [ 2 / 2 ] rewriting at (2 1)
1538300353.397 * * * [misc]progress:  generating series expansions
1538300353.397 * * * * [misc]progress:  [ 1 / 2 ] generating series at (2 1 1)
1538300353.397 * * * * [misc]progress:  [ 2 / 2 ] generating series at (2 1)
1538300353.398 * [misc]backup-simplify:  Simplify (/ (/ 4/3 PI) (- 1 (* v v))) into (/ 4/3 (* (- 1 (pow v 2)) PI))
1538300353.398 * [misc]approximate:  Taking taylor expansion of (/ 4/3 (* (- 1 (pow v 2)) PI)) in (v) around 0
1538300353.398 * [misc]taylor:  Taking taylor expansion of (/ 4/3 (* (- 1 (pow v 2)) PI)) in v
1538300353.398 * [misc]taylor:  Taking taylor expansion of 4/3 in v
1538300353.398 * [misc]backup-simplify:  Simplify 4/3 into 4/3
1538300353.398 * [misc]taylor:  Taking taylor expansion of (* (- 1 (pow v 2)) PI) in v
1538300353.398 * [misc]taylor:  Taking taylor expansion of (- 1 (pow v 2)) in v
1538300353.398 * [misc]taylor:  Taking taylor expansion of 1 in v
1538300353.398 * [misc]backup-simplify:  Simplify 1 into 1
1538300353.398 * [misc]taylor:  Taking taylor expansion of (pow v 2) in v
1538300353.398 * [misc]taylor:  Taking taylor expansion of v in v
1538300353.398 * [misc]backup-simplify:  Simplify 0 into 0
1538300353.398 * [misc]backup-simplify:  Simplify 1 into 1
1538300353.398 * [misc]taylor:  Taking taylor expansion of PI in v
1538300353.398 * [misc]backup-simplify:  Simplify PI into PI
1538300353.398 * [misc]backup-simplify:  Simplify (+ 1 0) into 1
1538300353.399 * [misc]backup-simplify:  Simplify (* 1 PI) into PI
1538300353.399 * [misc]backup-simplify:  Simplify (/ 4/3 PI) into (/ 4/3 PI)
1538300353.399 * [misc]taylor:  Taking taylor expansion of (/ 4/3 (* (- 1 (pow v 2)) PI)) in v
1538300353.399 * [misc]taylor:  Taking taylor expansion of 4/3 in v
1538300353.399 * [misc]backup-simplify:  Simplify 4/3 into 4/3
1538300353.399 * [misc]taylor:  Taking taylor expansion of (* (- 1 (pow v 2)) PI) in v
1538300353.399 * [misc]taylor:  Taking taylor expansion of (- 1 (pow v 2)) in v
1538300353.399 * [misc]taylor:  Taking taylor expansion of 1 in v
1538300353.399 * [misc]backup-simplify:  Simplify 1 into 1
1538300353.399 * [misc]taylor:  Taking taylor expansion of (pow v 2) in v
1538300353.399 * [misc]taylor:  Taking taylor expansion of v in v
1538300353.399 * [misc]backup-simplify:  Simplify 0 into 0
1538300353.399 * [misc]backup-simplify:  Simplify 1 into 1
1538300353.399 * [misc]taylor:  Taking taylor expansion of PI in v
1538300353.399 * [misc]backup-simplify:  Simplify PI into PI
1538300353.400 * [misc]backup-simplify:  Simplify (+ 1 0) into 1
1538300353.400 * [misc]backup-simplify:  Simplify (* 1 PI) into PI
1538300353.400 * [misc]backup-simplify:  Simplify (/ 4/3 PI) into (/ 4/3 PI)
1538300353.401 * [misc]backup-simplify:  Simplify (/ 4/3 PI) into (/ 4/3 PI)
1538300353.401 * [misc]backup-simplify:  Simplify (+ 0 0) into 0
1538300353.402 * [misc]backup-simplify:  Simplify (+ (* 1 0) (* 0 PI)) into 0
1538300353.403 * [misc]backup-simplify:  Simplify (- (/ 0 PI) (+ (* (/ 4/3 PI) (/ 0 PI)))) into 0
1538300353.403 * [misc]backup-simplify:  Simplify 0 into 0
1538300353.404 * [misc]backup-simplify:  Simplify (* 1 1) into 1
1538300353.404 * [misc]backup-simplify:  Simplify (- 1) into -1
1538300353.404 * [misc]backup-simplify:  Simplify (+ 0 -1) into -1
1538300353.405 * [misc]backup-simplify:  Simplify (+ (* 1 0) (+ (* 0 0) (* -1 PI))) into (- PI)
1538300353.408 * [misc]backup-simplify:  Simplify (- (/ 0 PI) (+ (* (/ 4/3 PI) (/ (- PI) PI)) (* 0 (/ 0 PI)))) into (* 4/3 (/ 1 PI))
1538300353.409 * [misc]backup-simplify:  Simplify (* 4/3 (/ 1 PI)) into (/ 4/3 PI)
1538300353.409 * [misc]backup-simplify:  Simplify (+ (* 1 0) (* 0 1)) into 0
1538300353.409 * [misc]backup-simplify:  Simplify (- 0) into 0
1538300353.409 * [misc]backup-simplify:  Simplify (+ 0 0) into 0
1538300353.411 * [misc]backup-simplify:  Simplify (+ (* 1 0) (+ (* 0 0) (+ (* -1 0) (* 0 PI)))) into 0
1538300353.415 * [misc]backup-simplify:  Simplify (- (/ 0 PI) (+ (* (/ 4/3 PI) (/ 0 PI)) (* 0 (/ (- PI) PI)) (* (* 4/3 (/ 1 PI)) (/ 0 PI)))) into 0
1538300353.415 * [misc]backup-simplify:  Simplify 0 into 0
1538300353.416 * [misc]backup-simplify:  Simplify (+ (* 1 0) (+ (* 0 0) (* 0 1))) into 0
1538300353.416 * [misc]backup-simplify:  Simplify (- 0) into 0
1538300353.416 * [misc]backup-simplify:  Simplify (+ 0 0) into 0
1538300353.418 * [misc]backup-simplify:  Simplify (+ (* 1 0) (+ (* 0 0) (+ (* -1 0) (+ (* 0 0) (* 0 PI))))) into 0
1538300353.423 * [misc]backup-simplify:  Simplify (- (/ 0 PI) (+ (* (/ 4/3 PI) (/ 0 PI)) (* 0 (/ 0 PI)) (* (* 4/3 (/ 1 PI)) (/ (- PI) PI)) (* 0 (/ 0 PI)))) into (* 4/3 (/ 1 PI))
1538300353.424 * [misc]backup-simplify:  Simplify (* 4/3 (/ 1 PI)) into (/ 4/3 PI)
1538300353.425 * [misc]backup-simplify:  Simplify (+ (* (/ 4/3 PI) (pow v 4)) (+ (* (/ 4/3 PI) (pow v 2)) (/ 4/3 PI))) into (+ (* 4/3 (/ (pow v 2) PI)) (+ (* 4/3 (/ 1 PI)) (* 4/3 (/ (pow v 4) PI))))
1538300353.426 * [misc]backup-simplify:  Simplify (/ (/ 4/3 PI) (- 1 (* (/ 1 v) (/ 1 v)))) into (/ 4/3 (* (- 1 (/ 1 (pow v 2))) PI))
1538300353.426 * [misc]approximate:  Taking taylor expansion of (/ 4/3 (* (- 1 (/ 1 (pow v 2))) PI)) in (v) around 0
1538300353.426 * [misc]taylor:  Taking taylor expansion of (/ 4/3 (* (- 1 (/ 1 (pow v 2))) PI)) in v
1538300353.426 * [misc]taylor:  Taking taylor expansion of 4/3 in v
1538300353.426 * [misc]backup-simplify:  Simplify 4/3 into 4/3
1538300353.426 * [misc]taylor:  Taking taylor expansion of (* (- 1 (/ 1 (pow v 2))) PI) in v
1538300353.426 * [misc]taylor:  Taking taylor expansion of (- 1 (/ 1 (pow v 2))) in v
1538300353.426 * [misc]taylor:  Taking taylor expansion of 1 in v
1538300353.426 * [misc]backup-simplify:  Simplify 1 into 1
1538300353.426 * [misc]taylor:  Taking taylor expansion of (/ 1 (pow v 2)) in v
1538300353.426 * [misc]taylor:  Taking taylor expansion of (pow v 2) in v
1538300353.426 * [misc]taylor:  Taking taylor expansion of v in v
1538300353.426 * [misc]backup-simplify:  Simplify 0 into 0
1538300353.426 * [misc]backup-simplify:  Simplify 1 into 1
1538300353.426 * [misc]backup-simplify:  Simplify (* 1 1) into 1
1538300353.426 * [misc]backup-simplify:  Simplify (/ 1 1) into 1
1538300353.426 * [misc]taylor:  Taking taylor expansion of PI in v
1538300353.427 * [misc]backup-simplify:  Simplify PI into PI
1538300353.427 * [misc]backup-simplify:  Simplify (- 1) into -1
1538300353.427 * [misc]backup-simplify:  Simplify (+ 0 -1) into -1
1538300353.427 * [misc]backup-simplify:  Simplify (* -1 PI) into (* -1 PI)
1538300353.428 * [misc]backup-simplify:  Simplify (/ 4/3 (* -1 PI)) into (/ -4/3 PI)
1538300353.428 * [misc]taylor:  Taking taylor expansion of (/ 4/3 (* (- 1 (/ 1 (pow v 2))) PI)) in v
1538300353.428 * [misc]taylor:  Taking taylor expansion of 4/3 in v
1538300353.428 * [misc]backup-simplify:  Simplify 4/3 into 4/3
1538300353.428 * [misc]taylor:  Taking taylor expansion of (* (- 1 (/ 1 (pow v 2))) PI) in v
1538300353.428 * [misc]taylor:  Taking taylor expansion of (- 1 (/ 1 (pow v 2))) in v
1538300353.428 * [misc]taylor:  Taking taylor expansion of 1 in v
1538300353.428 * [misc]backup-simplify:  Simplify 1 into 1
1538300353.428 * [misc]taylor:  Taking taylor expansion of (/ 1 (pow v 2)) in v
1538300353.428 * [misc]taylor:  Taking taylor expansion of (pow v 2) in v
1538300353.428 * [misc]taylor:  Taking taylor expansion of v in v
1538300353.428 * [misc]backup-simplify:  Simplify 0 into 0
1538300353.428 * [misc]backup-simplify:  Simplify 1 into 1
1538300353.428 * [misc]backup-simplify:  Simplify (* 1 1) into 1
1538300353.428 * [misc]backup-simplify:  Simplify (/ 1 1) into 1
1538300353.428 * [misc]taylor:  Taking taylor expansion of PI in v
1538300353.429 * [misc]backup-simplify:  Simplify PI into PI
1538300353.429 * [misc]backup-simplify:  Simplify (- 1) into -1
1538300353.429 * [misc]backup-simplify:  Simplify (+ 0 -1) into -1
1538300353.429 * [misc]backup-simplify:  Simplify (* -1 PI) into (* -1 PI)
1538300353.430 * [misc]backup-simplify:  Simplify (/ 4/3 (* -1 PI)) into (/ -4/3 PI)
1538300353.430 * [misc]backup-simplify:  Simplify (/ -4/3 PI) into (/ -4/3 PI)
1538300353.430 * [misc]backup-simplify:  Simplify (+ (* 1 0) (* 0 1)) into 0
1538300353.431 * [misc]backup-simplify:  Simplify (- (+ (* 1 (/ 0 1)))) into 0
1538300353.431 * [misc]backup-simplify:  Simplify (- 0) into 0
1538300353.431 * [misc]backup-simplify:  Simplify (+ 0 0) into 0
1538300353.432 * [misc]backup-simplify:  Simplify (+ (* -1 0) (* 0 PI)) into 0
1538300353.434 * [misc]backup-simplify:  Simplify (- (/ 0 (* -1 PI)) (+ (* (/ -4/3 PI) (/ 0 (* -1 PI))))) into 0
1538300353.434 * [misc]backup-simplify:  Simplify 0 into 0
1538300353.434 * [misc]backup-simplify:  Simplify (+ (* 1 0) (+ (* 0 0) (* 0 1))) into 0
1538300353.435 * [misc]backup-simplify:  Simplify (- (+ (* 1 (/ 0 1)) (* 0 (/ 0 1)))) into 0
1538300353.435 * [misc]backup-simplify:  Simplify (- 0) into 0
1538300353.435 * [misc]backup-simplify:  Simplify (+ 1 0) into 1
1538300353.437 * [misc]backup-simplify:  Simplify (+ (* -1 0) (+ (* 0 0) (* 1 PI))) into PI
1538300353.440 * [misc]backup-simplify:  Simplify (- (/ 0 (* -1 PI)) (+ (* (/ -4/3 PI) (/ PI (* -1 PI))) (* 0 (/ 0 (* -1 PI))))) into (- (* 4/3 (/ 1 PI)))
1538300353.441 * [misc]backup-simplify:  Simplify (- (* 4/3 (/ 1 PI))) into (- (* 4/3 (/ 1 PI)))
1538300353.442 * [misc]backup-simplify:  Simplify (+ (* 1 0) (+ (* 0 0) (+ (* 0 0) (* 0 1)))) into 0
1538300353.442 * [misc]backup-simplify:  Simplify (- (+ (* 1 (/ 0 1)) (* 0 (/ 0 1)) (* 0 (/ 0 1)))) into 0
1538300353.442 * [misc]backup-simplify:  Simplify (- 0) into 0
1538300353.442 * [misc]backup-simplify:  Simplify (+ 0 0) into 0
1538300353.444 * [misc]backup-simplify:  Simplify (+ (* -1 0) (+ (* 0 0) (+ (* 1 0) (* 0 PI)))) into 0
1538300353.450 * [misc]backup-simplify:  Simplify (- (/ 0 (* -1 PI)) (+ (* (/ -4/3 PI) (/ 0 (* -1 PI))) (* 0 (/ PI (* -1 PI))) (* (- (* 4/3 (/ 1 PI))) (/ 0 (* -1 PI))))) into 0
1538300353.450 * [misc]backup-simplify:  Simplify 0 into 0
1538300353.450 * [misc]backup-simplify:  Simplify (+ (* 1 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (* 0 1))))) into 0
1538300353.451 * [misc]backup-simplify:  Simplify (- (+ (* 1 (/ 0 1)) (* 0 (/ 0 1)) (* 0 (/ 0 1)) (* 0 (/ 0 1)))) into 0
1538300353.451 * [misc]backup-simplify:  Simplify (- 0) into 0
1538300353.451 * [misc]backup-simplify:  Simplify (+ 0 0) into 0
1538300353.453 * [misc]backup-simplify:  Simplify (+ (* -1 0) (+ (* 0 0) (+ (* 1 0) (+ (* 0 0) (* 0 PI))))) into 0
1538300353.460 * [misc]backup-simplify:  Simplify (- (/ 0 (* -1 PI)) (+ (* (/ -4/3 PI) (/ 0 (* -1 PI))) (* 0 (/ 0 (* -1 PI))) (* (- (* 4/3 (/ 1 PI))) (/ PI (* -1 PI))) (* 0 (/ 0 (* -1 PI))))) into (- (* 4/3 (/ 1 PI)))
1538300353.461 * [misc]backup-simplify:  Simplify (- (* 4/3 (/ 1 PI))) into (- (* 4/3 (/ 1 PI)))
1538300353.463 * [misc]backup-simplify:  Simplify (+ (* (- (* 4/3 (/ 1 PI))) (pow (/ 1 v) 6)) (+ (* (- (* 4/3 (/ 1 PI))) (pow (/ 1 v) 4)) (* (/ -4/3 PI) (pow (/ 1 v) 2)))) into (- (+ (* 4/3 (/ 1 (* (pow v 2) PI))) (+ (* 4/3 (/ 1 (* (pow v 4) PI))) (* 4/3 (/ 1 (* (pow v 6) PI))))))
1538300353.464 * [misc]backup-simplify:  Simplify (/ (/ 4/3 PI) (- 1 (* (/ 1 (- v)) (/ 1 (- v))))) into (/ 4/3 (* (- 1 (/ 1 (pow v 2))) PI))
1538300353.464 * [misc]approximate:  Taking taylor expansion of (/ 4/3 (* (- 1 (/ 1 (pow v 2))) PI)) in (v) around 0
1538300353.464 * [misc]taylor:  Taking taylor expansion of (/ 4/3 (* (- 1 (/ 1 (pow v 2))) PI)) in v
1538300353.464 * [misc]taylor:  Taking taylor expansion of 4/3 in v
1538300353.464 * [misc]backup-simplify:  Simplify 4/3 into 4/3
1538300353.464 * [misc]taylor:  Taking taylor expansion of (* (- 1 (/ 1 (pow v 2))) PI) in v
1538300353.464 * [misc]taylor:  Taking taylor expansion of (- 1 (/ 1 (pow v 2))) in v
1538300353.464 * [misc]taylor:  Taking taylor expansion of 1 in v
1538300353.464 * [misc]backup-simplify:  Simplify 1 into 1
1538300353.464 * [misc]taylor:  Taking taylor expansion of (/ 1 (pow v 2)) in v
1538300353.464 * [misc]taylor:  Taking taylor expansion of (pow v 2) in v
1538300353.464 * [misc]taylor:  Taking taylor expansion of v in v
1538300353.464 * [misc]backup-simplify:  Simplify 0 into 0
1538300353.464 * [misc]backup-simplify:  Simplify 1 into 1
1538300353.464 * [misc]backup-simplify:  Simplify (* 1 1) into 1
1538300353.464 * [misc]backup-simplify:  Simplify (/ 1 1) into 1
1538300353.464 * [misc]taylor:  Taking taylor expansion of PI in v
1538300353.464 * [misc]backup-simplify:  Simplify PI into PI
1538300353.465 * [misc]backup-simplify:  Simplify (- 1) into -1
1538300353.465 * [misc]backup-simplify:  Simplify (+ 0 -1) into -1
1538300353.465 * [misc]backup-simplify:  Simplify (* -1 PI) into (* -1 PI)
1538300353.465 * [misc]backup-simplify:  Simplify (/ 4/3 (* -1 PI)) into (/ -4/3 PI)
1538300353.465 * [misc]taylor:  Taking taylor expansion of (/ 4/3 (* (- 1 (/ 1 (pow v 2))) PI)) in v
1538300353.465 * [misc]taylor:  Taking taylor expansion of 4/3 in v
1538300353.465 * [misc]backup-simplify:  Simplify 4/3 into 4/3
1538300353.465 * [misc]taylor:  Taking taylor expansion of (* (- 1 (/ 1 (pow v 2))) PI) in v
1538300353.465 * [misc]taylor:  Taking taylor expansion of (- 1 (/ 1 (pow v 2))) in v
1538300353.465 * [misc]taylor:  Taking taylor expansion of 1 in v
1538300353.465 * [misc]backup-simplify:  Simplify 1 into 1
1538300353.465 * [misc]taylor:  Taking taylor expansion of (/ 1 (pow v 2)) in v
1538300353.465 * [misc]taylor:  Taking taylor expansion of (pow v 2) in v
1538300353.465 * [misc]taylor:  Taking taylor expansion of v in v
1538300353.465 * [misc]backup-simplify:  Simplify 0 into 0
1538300353.465 * [misc]backup-simplify:  Simplify 1 into 1
1538300353.466 * [misc]backup-simplify:  Simplify (* 1 1) into 1
1538300353.466 * [misc]backup-simplify:  Simplify (/ 1 1) into 1
1538300353.466 * [misc]taylor:  Taking taylor expansion of PI in v
1538300353.466 * [misc]backup-simplify:  Simplify PI into PI
1538300353.466 * [misc]backup-simplify:  Simplify (- 1) into -1
1538300353.466 * [misc]backup-simplify:  Simplify (+ 0 -1) into -1
1538300353.466 * [misc]backup-simplify:  Simplify (* -1 PI) into (* -1 PI)
1538300353.466 * [misc]backup-simplify:  Simplify (/ 4/3 (* -1 PI)) into (/ -4/3 PI)
1538300353.467 * [misc]backup-simplify:  Simplify (/ -4/3 PI) into (/ -4/3 PI)
1538300353.467 * [misc]backup-simplify:  Simplify (+ (* 1 0) (* 0 1)) into 0
1538300353.467 * [misc]backup-simplify:  Simplify (- (+ (* 1 (/ 0 1)))) into 0
1538300353.467 * [misc]backup-simplify:  Simplify (- 0) into 0
1538300353.467 * [misc]backup-simplify:  Simplify (+ 0 0) into 0
1538300353.468 * [misc]backup-simplify:  Simplify (+ (* -1 0) (* 0 PI)) into 0
1538300353.469 * [misc]backup-simplify:  Simplify (- (/ 0 (* -1 PI)) (+ (* (/ -4/3 PI) (/ 0 (* -1 PI))))) into 0
1538300353.469 * [misc]backup-simplify:  Simplify 0 into 0
1538300353.469 * [misc]backup-simplify:  Simplify (+ (* 1 0) (+ (* 0 0) (* 0 1))) into 0
1538300353.469 * [misc]backup-simplify:  Simplify (- (+ (* 1 (/ 0 1)) (* 0 (/ 0 1)))) into 0
1538300353.470 * [misc]backup-simplify:  Simplify (- 0) into 0
1538300353.470 * [misc]backup-simplify:  Simplify (+ 1 0) into 1
1538300353.470 * [misc]backup-simplify:  Simplify (+ (* -1 0) (+ (* 0 0) (* 1 PI))) into PI
1538300353.472 * [misc]backup-simplify:  Simplify (- (/ 0 (* -1 PI)) (+ (* (/ -4/3 PI) (/ PI (* -1 PI))) (* 0 (/ 0 (* -1 PI))))) into (- (* 4/3 (/ 1 PI)))
1538300353.473 * [misc]backup-simplify:  Simplify (- (* 4/3 (/ 1 PI))) into (- (* 4/3 (/ 1 PI)))
1538300353.473 * [misc]backup-simplify:  Simplify (+ (* 1 0) (+ (* 0 0) (+ (* 0 0) (* 0 1)))) into 0
1538300353.473 * [misc]backup-simplify:  Simplify (- (+ (* 1 (/ 0 1)) (* 0 (/ 0 1)) (* 0 (/ 0 1)))) into 0
1538300353.474 * [misc]backup-simplify:  Simplify (- 0) into 0
1538300353.474 * [misc]backup-simplify:  Simplify (+ 0 0) into 0
1538300353.475 * [misc]backup-simplify:  Simplify (+ (* -1 0) (+ (* 0 0) (+ (* 1 0) (* 0 PI)))) into 0
1538300353.478 * [misc]backup-simplify:  Simplify (- (/ 0 (* -1 PI)) (+ (* (/ -4/3 PI) (/ 0 (* -1 PI))) (* 0 (/ PI (* -1 PI))) (* (- (* 4/3 (/ 1 PI))) (/ 0 (* -1 PI))))) into 0
1538300353.478 * [misc]backup-simplify:  Simplify 0 into 0
1538300353.478 * [misc]backup-simplify:  Simplify (+ (* 1 0) (+ (* 0 0) (+ (* 0 0) (+ (* 0 0) (* 0 1))))) into 0
1538300353.478 * [misc]backup-simplify:  Simplify (- (+ (* 1 (/ 0 1)) (* 0 (/ 0 1)) (* 0 (/ 0 1)) (* 0 (/ 0 1)))) into 0
1538300353.479 * [misc]backup-simplify:  Simplify (- 0) into 0
1538300353.479 * [misc]backup-simplify:  Simplify (+ 0 0) into 0
1538300353.480 * [misc]backup-simplify:  Simplify (+ (* -1 0) (+ (* 0 0) (+ (* 1 0) (+ (* 0 0) (* 0 PI))))) into 0
1538300353.484 * [misc]backup-simplify:  Simplify (- (/ 0 (* -1 PI)) (+ (* (/ -4/3 PI) (/ 0 (* -1 PI))) (* 0 (/ 0 (* -1 PI))) (* (- (* 4/3 (/ 1 PI))) (/ PI (* -1 PI))) (* 0 (/ 0 (* -1 PI))))) into (- (* 4/3 (/ 1 PI)))
1538300353.484 * [misc]backup-simplify:  Simplify (- (* 4/3 (/ 1 PI))) into (- (* 4/3 (/ 1 PI)))
1538300353.490 * [misc]backup-simplify:  Simplify (+ (* (- (* 4/3 (/ 1 PI))) (pow (/ 1 (- v)) 6)) (+ (* (- (* 4/3 (/ 1 PI))) (pow (/ 1 (- v)) 4)) (* (/ -4/3 PI) (pow (/ 1 (- v)) 2)))) into (- (+ (* 4/3 (/ 1 (* (pow v 2) PI))) (+ (* 4/3 (/ 1 (* (pow v 4) PI))) (* 4/3 (/ 1 (* (pow v 6) PI))))))
1538300353.490 * * * [misc]progress:  simplifying candidates
1538300353.490 * * * * [misc]progress:  [ 1 / 52 ] simplifiying candidate #<alt (λ (v) (/ (/ (log1p (expm1 (/ 4/3 PI))) (- 1 (* v v))) (sqrt (fma -6 (* v v) 2))))>
1538300353.490 * * * * [misc]progress:  [ 2 / 52 ] simplifiying candidate #<alt (λ (v) (/ (/ (expm1 (log1p (/ 4/3 PI))) (- 1 (* v v))) (sqrt (fma -6 (* v v) 2))))>
1538300353.490 * * * * [misc]progress:  [ 3 / 52 ] simplifiying candidate #<alt (λ (v) (/ (/ (pow (/ 4/3 PI) 1) (- 1 (* v v))) (sqrt (fma -6 (* v v) 2))))>
1538300353.490 * * * * [misc]progress:  [ 4 / 52 ] simplifiying candidate #<alt (λ (v) (/ (/ (exp (log (/ 4/3 PI))) (- 1 (* v v))) (sqrt (fma -6 (* v v) 2))))>
1538300353.490 * * * * [misc]progress:  [ 5 / 52 ] simplifiying candidate #<alt (λ (v) (/ (/ (log (exp (/ 4/3 PI))) (- 1 (* v v))) (sqrt (fma -6 (* v v) 2))))>
1538300353.490 * * * * [misc]progress:  [ 6 / 52 ] simplifiying candidate #<alt (λ (v) (/ (/ (* (* (cbrt (/ 4/3 PI)) (cbrt (/ 4/3 PI))) (cbrt (/ 4/3 PI))) (- 1 (* v v))) (sqrt (fma -6 (* v v) 2))))>
1538300353.490 * * * * [misc]progress:  [ 7 / 52 ] simplifiying candidate #<alt (λ (v) (/ (/ (cbrt (* (* (/ 4/3 PI) (/ 4/3 PI)) (/ 4/3 PI))) (- 1 (* v v))) (sqrt (fma -6 (* v v) 2))))>
1538300353.490 * * * * [misc]progress:  [ 8 / 52 ] simplifiying candidate #<alt (λ (v) (/ (/ (* (sqrt (/ 4/3 PI)) (sqrt (/ 4/3 PI))) (- 1 (* v v))) (sqrt (fma -6 (* v v) 2))))>
1538300353.490 * * * * [misc]progress:  [ 9 / 52 ] simplifiying candidate #<alt (λ (v) (/ (/ (/ (- 4/3) (- PI)) (- 1 (* v v))) (sqrt (fma -6 (* v v) 2))))>
1538300353.490 * * * * [misc]progress:  [ 10 / 52 ] simplifiying candidate #<alt (λ (v) (/ (/ (* 1 (/ 4/3 PI)) (- 1 (* v v))) (sqrt (fma -6 (* v v) 2))))>
1538300353.490 * * * * [misc]progress:  [ 11 / 52 ] simplifiying candidate #<alt (λ (v) (/ (/ (* 4/3 (/ 1 PI)) (- 1 (* v v))) (sqrt (fma -6 (* v v) 2))))>
1538300353.490 * * * * [misc]progress:  [ 12 / 52 ] simplifiying candidate #<alt (λ (v) (/ (/ (/ 1 (/ PI 4/3)) (- 1 (* v v))) (sqrt (fma -6 (* v v) 2))))>
1538300353.490 * * * * [misc]progress:  [ 13 / 52 ] simplifiying candidate #<alt (λ (v) (/ (log1p (expm1 (/ (/ 4/3 PI) (- 1 (* v v))))) (sqrt (fma -6 (* v v) 2))))>
1538300353.491 * * * * [misc]progress:  [ 14 / 52 ] simplifiying candidate #<alt (λ (v) (/ (expm1 (log1p (/ (/ 4/3 PI) (- 1 (* v v))))) (sqrt (fma -6 (* v v) 2))))>
1538300353.491 * * * * [misc]progress:  [ 15 / 52 ] simplifiying candidate #<alt (λ (v) (/ (pow (/ (/ 4/3 PI) (- 1 (* v v))) 1) (sqrt (fma -6 (* v v) 2))))>
1538300353.491 * * * * [misc]progress:  [ 16 / 52 ] simplifiying candidate #<alt (λ (v) (/ (exp (- (log (/ 4/3 PI)) (log (- 1 (* v v))))) (sqrt (fma -6 (* v v) 2))))>
1538300353.491 * [enter]simplify:  Simplifying (- (log (/ 4/3 PI)) (log (- 1 (* v v))))
1538300353.491 * * [misc]simplify:  iters left: 6 (10 enodes)
1538300353.494 * * [misc]simplify:  iters left: 5 (19 enodes)
1538300353.499 * * [misc]simplify:  iters left: 4 (31 enodes)
1538300353.506 * * [misc]simplify:  iters left: 3 (48 enodes)
1538300353.514 * * [misc]simplify:  iters left: 2 (58 enodes)
1538300353.523 * * [misc]simplify:  iters left: 1 (73 enodes)
1538300353.535 * [exit]simplify:  Simplified to (- (log (/ 4/3 PI)) (log (- 1 (* v v))))
1538300353.535 * [misc]simplify:  Simplified (2 1 1) to (λ (v) (/ (exp (- (log (/ 4/3 PI)) (log (- 1 (* v v))))) (sqrt (fma -6 (* v v) 2))))
1538300353.535 * * * * [misc]progress:  [ 17 / 52 ] simplifiying candidate #<alt (λ (v) (/ (exp (log (/ (/ 4/3 PI) (- 1 (* v v))))) (sqrt (fma -6 (* v v) 2))))>
1538300353.535 * * * * [misc]progress:  [ 18 / 52 ] simplifiying candidate #<alt (λ (v) (/ (log (exp (/ (/ 4/3 PI) (- 1 (* v v))))) (sqrt (fma -6 (* v v) 2))))>
1538300353.535 * * * * [misc]progress:  [ 19 / 52 ] simplifiying candidate #<alt (λ (v) (/ (cbrt (/ (* (* (/ 4/3 PI) (/ 4/3 PI)) (/ 4/3 PI)) (* (* (- 1 (* v v)) (- 1 (* v v))) (- 1 (* v v))))) (sqrt (fma -6 (* v v) 2))))>
1538300353.535 * [enter]simplify:  Simplifying (/ (* (* (/ 4/3 PI) (/ 4/3 PI)) (/ 4/3 PI)) (* (* (- 1 (* v v)) (- 1 (* v v))) (- 1 (* v v))))
1538300353.536 * * [misc]simplify:  iters left: 6 (12 enodes)
1538300353.540 * * [misc]simplify:  iters left: 5 (31 enodes)
1538300353.553 * * [misc]simplify:  iters left: 4 (101 enodes)
1538300353.602 * * [misc]simplify:  iters left: 3 (331 enodes)
1538300354.123 * [exit]simplify:  Simplified to (/ (/ (/ (/ 64/27 PI) (* PI PI)) (- 1 (* v v))) (* (- 1 (* v v)) (- 1 (* v v))))
1538300354.123 * [misc]simplify:  Simplified (2 1 1) to (λ (v) (/ (cbrt (/ (/ (/ (/ 64/27 PI) (* PI PI)) (- 1 (* v v))) (* (- 1 (* v v)) (- 1 (* v v))))) (sqrt (fma -6 (* v v) 2))))
1538300354.123 * * * * [misc]progress:  [ 20 / 52 ] simplifiying candidate #<alt (λ (v) (/ (* (* (cbrt (/ (/ 4/3 PI) (- 1 (* v v)))) (cbrt (/ (/ 4/3 PI) (- 1 (* v v))))) (cbrt (/ (/ 4/3 PI) (- 1 (* v v))))) (sqrt (fma -6 (* v v) 2))))>
1538300354.124 * * * * [misc]progress:  [ 21 / 52 ] simplifiying candidate #<alt (λ (v) (/ (cbrt (* (* (/ (/ 4/3 PI) (- 1 (* v v))) (/ (/ 4/3 PI) (- 1 (* v v)))) (/ (/ 4/3 PI) (- 1 (* v v))))) (sqrt (fma -6 (* v v) 2))))>
1538300354.124 * * * * [misc]progress:  [ 22 / 52 ] simplifiying candidate #<alt (λ (v) (/ (* (sqrt (/ (/ 4/3 PI) (- 1 (* v v)))) (sqrt (/ (/ 4/3 PI) (- 1 (* v v))))) (sqrt (fma -6 (* v v) 2))))>
1538300354.124 * * * * [misc]progress:  [ 23 / 52 ] simplifiying candidate #<alt (λ (v) (/ (/ (- (/ 4/3 PI)) (- (- 1 (* v v)))) (sqrt (fma -6 (* v v) 2))))>
1538300354.124 * * * * [misc]progress:  [ 24 / 52 ] simplifiying candidate #<alt (λ (v) (/ (* (/ (* (cbrt (/ 4/3 PI)) (cbrt (/ 4/3 PI))) (* (cbrt (- 1 (* v v))) (cbrt (- 1 (* v v))))) (/ (cbrt (/ 4/3 PI)) (cbrt (- 1 (* v v))))) (sqrt (fma -6 (* v v) 2))))>
1538300354.124 * [enter]simplify:  Simplifying (/ (* (cbrt (/ 4/3 PI)) (cbrt (/ 4/3 PI))) (* (cbrt (- 1 (* v v))) (cbrt (- 1 (* v v)))))
1538300354.126 * * [misc]simplify:  iters left: 6 (12 enodes)
1538300354.132 * * [misc]simplify:  iters left: 5 (22 enodes)
1538300354.142 * * [misc]simplify:  iters left: 4 (35 enodes)
1538300354.154 * * [misc]simplify:  iters left: 3 (40 enodes)
1538300354.167 * * [misc]simplify:  iters left: 2 (43 enodes)
1538300354.184 * [exit]simplify:  Simplified to (* (/ (cbrt (/ 4/3 PI)) (cbrt (- 1 (* v v)))) (/ (cbrt (/ 4/3 PI)) (cbrt (- 1 (* v v)))))
1538300354.184 * [misc]simplify:  Simplified (2 1 1) to (λ (v) (/ (* (* (/ (cbrt (/ 4/3 PI)) (cbrt (- 1 (* v v)))) (/ (cbrt (/ 4/3 PI)) (cbrt (- 1 (* v v))))) (/ (cbrt (/ 4/3 PI)) (cbrt (- 1 (* v v))))) (sqrt (fma -6 (* v v) 2))))
1538300354.184 * [enter]simplify:  Simplifying (/ (cbrt (/ 4/3 PI)) (cbrt (- 1 (* v v))))
1538300354.185 * * [misc]simplify:  iters left: 6 (10 enodes)
1538300354.189 * * [misc]simplify:  iters left: 5 (14 enodes)
1538300354.195 * * [misc]simplify:  iters left: 4 (18 enodes)
1538300354.201 * * [misc]simplify:  iters left: 3 (20 enodes)
1538300354.208 * [exit]simplify:  Simplified to (/ (cbrt (/ 4/3 PI)) (cbrt (- 1 (* v v))))
1538300354.208 * [misc]simplify:  Simplified (2 1 2) to (λ (v) (/ (* (/ (* (cbrt (/ 4/3 PI)) (cbrt (/ 4/3 PI))) (* (cbrt (- 1 (* v v))) (cbrt (- 1 (* v v))))) (/ (cbrt (/ 4/3 PI)) (cbrt (- 1 (* v v))))) (sqrt (fma -6 (* v v) 2))))
1538300354.208 * * * * [misc]progress:  [ 25 / 52 ] simplifiying candidate #<alt (λ (v) (/ (* (/ (* (cbrt (/ 4/3 PI)) (cbrt (/ 4/3 PI))) (sqrt (- 1 (* v v)))) (/ (cbrt (/ 4/3 PI)) (sqrt (- 1 (* v v))))) (sqrt (fma -6 (* v v) 2))))>
1538300354.208 * [enter]simplify:  Simplifying (/ (* (cbrt (/ 4/3 PI)) (cbrt (/ 4/3 PI))) (sqrt (- 1 (* v v))))
1538300354.209 * * [misc]simplify:  iters left: 6 (11 enodes)
1538300354.214 * * [misc]simplify:  iters left: 5 (17 enodes)
1538300354.221 * * [misc]simplify:  iters left: 4 (23 enodes)
1538300354.228 * * [misc]simplify:  iters left: 3 (26 enodes)
1538300354.238 * [exit]simplify:  Simplified to (/ (* (cbrt (/ 4/3 PI)) (cbrt (/ 4/3 PI))) (sqrt (- 1 (* v v))))
1538300354.238 * [misc]simplify:  Simplified (2 1 1) to (λ (v) (/ (* (/ (* (cbrt (/ 4/3 PI)) (cbrt (/ 4/3 PI))) (sqrt (- 1 (* v v)))) (/ (cbrt (/ 4/3 PI)) (sqrt (- 1 (* v v))))) (sqrt (fma -6 (* v v) 2))))
1538300354.239 * [enter]simplify:  Simplifying (/ (cbrt (/ 4/3 PI)) (sqrt (- 1 (* v v))))
1538300354.240 * * [misc]simplify:  iters left: 6 (10 enodes)
1538300354.244 * * [misc]simplify:  iters left: 5 (14 enodes)
1538300354.249 * * [misc]simplify:  iters left: 4 (18 enodes)
1538300354.254 * * [misc]simplify:  iters left: 3 (20 enodes)
1538300354.261 * [exit]simplify:  Simplified to (/ (cbrt (/ 4/3 PI)) (sqrt (- 1 (* v v))))
1538300354.261 * [misc]simplify:  Simplified (2 1 2) to (λ (v) (/ (* (/ (* (cbrt (/ 4/3 PI)) (cbrt (/ 4/3 PI))) (sqrt (- 1 (* v v)))) (/ (cbrt (/ 4/3 PI)) (sqrt (- 1 (* v v))))) (sqrt (fma -6 (* v v) 2))))
1538300354.261 * * * * [misc]progress:  [ 26 / 52 ] simplifiying candidate #<alt (λ (v) (/ (* (/ (* (cbrt (/ 4/3 PI)) (cbrt (/ 4/3 PI))) 1) (/ (cbrt (/ 4/3 PI)) (- 1 (* v v)))) (sqrt (fma -6 (* v v) 2))))>
1538300354.262 * [enter]simplify:  Simplifying (/ (* (cbrt (/ 4/3 PI)) (cbrt (/ 4/3 PI))) 1)
1538300354.262 * * [misc]simplify:  iters left: 6 (7 enodes)
1538300354.266 * * [misc]simplify:  iters left: 5 (11 enodes)
1538300354.270 * * [misc]simplify:  iters left: 4 (17 enodes)
1538300354.277 * * [misc]simplify:  iters left: 3 (31 enodes)
1538300354.290 * * [misc]simplify:  iters left: 2 (57 enodes)
1538300354.310 * [exit]simplify:  Simplified to (* (cbrt (/ 4/3 PI)) (cbrt (/ 4/3 PI)))
1538300354.310 * [misc]simplify:  Simplified (2 1 1) to (λ (v) (/ (* (* (cbrt (/ 4/3 PI)) (cbrt (/ 4/3 PI))) (/ (cbrt (/ 4/3 PI)) (- 1 (* v v)))) (sqrt (fma -6 (* v v) 2))))
1538300354.311 * [enter]simplify:  Simplifying (/ (cbrt (/ 4/3 PI)) (- 1 (* v v)))
1538300354.312 * * [misc]simplify:  iters left: 6 (9 enodes)
1538300354.315 * * [misc]simplify:  iters left: 5 (13 enodes)
1538300354.320 * * [misc]simplify:  iters left: 4 (17 enodes)
1538300354.326 * * [misc]simplify:  iters left: 3 (19 enodes)
1538300354.332 * [exit]simplify:  Simplified to (/ (cbrt (/ 4/3 PI)) (- 1 (* v v)))
1538300354.332 * [misc]simplify:  Simplified (2 1 2) to (λ (v) (/ (* (* (cbrt (/ 4/3 PI)) (cbrt (/ 4/3 PI))) (/ (cbrt (/ 4/3 PI)) (- 1 (* v v)))) (sqrt (fma -6 (* v v) 2))))
1538300354.332 * * * * [misc]progress:  [ 27 / 52 ] simplifiying candidate #<alt (λ (v) (/ (* (/ (sqrt (/ 4/3 PI)) (* (cbrt (- 1 (* v v))) (cbrt (- 1 (* v v))))) (/ (sqrt (/ 4/3 PI)) (cbrt (- 1 (* v v))))) (sqrt (fma -6 (* v v) 2))))>
1538300354.332 * [enter]simplify:  Simplifying (/ (sqrt (/ 4/3 PI)) (* (cbrt (- 1 (* v v))) (cbrt (- 1 (* v v)))))
1538300354.334 * * [misc]simplify:  iters left: 6 (11 enodes)
1538300354.338 * * [misc]simplify:  iters left: 5 (17 enodes)
1538300354.344 * * [misc]simplify:  iters left: 4 (21 enodes)
1538300354.351 * * [misc]simplify:  iters left: 3 (23 enodes)
1538300354.360 * [exit]simplify:  Simplified to (/ (/ (sqrt (/ 4/3 PI)) (cbrt (- 1 (* v v)))) (cbrt (- 1 (* v v))))
1538300354.360 * [misc]simplify:  Simplified (2 1 1) to (λ (v) (/ (* (/ (/ (sqrt (/ 4/3 PI)) (cbrt (- 1 (* v v)))) (cbrt (- 1 (* v v)))) (/ (sqrt (/ 4/3 PI)) (cbrt (- 1 (* v v))))) (sqrt (fma -6 (* v v) 2))))
1538300354.360 * [enter]simplify:  Simplifying (/ (sqrt (/ 4/3 PI)) (cbrt (- 1 (* v v))))
1538300354.361 * * [misc]simplify:  iters left: 6 (10 enodes)
1538300354.365 * * [misc]simplify:  iters left: 5 (14 enodes)
1538300354.370 * * [misc]simplify:  iters left: 4 (18 enodes)
1538300354.376 * * [misc]simplify:  iters left: 3 (20 enodes)
1538300354.383 * [exit]simplify:  Simplified to (/ (sqrt (/ 4/3 PI)) (cbrt (- 1 (* v v))))
1538300354.383 * [misc]simplify:  Simplified (2 1 2) to (λ (v) (/ (* (/ (sqrt (/ 4/3 PI)) (* (cbrt (- 1 (* v v))) (cbrt (- 1 (* v v))))) (/ (sqrt (/ 4/3 PI)) (cbrt (- 1 (* v v))))) (sqrt (fma -6 (* v v) 2))))
1538300354.383 * * * * [misc]progress:  [ 28 / 52 ] simplifiying candidate #<alt (λ (v) (/ (* (/ (sqrt (/ 4/3 PI)) (sqrt (- 1 (* v v)))) (/ (sqrt (/ 4/3 PI)) (sqrt (- 1 (* v v))))) (sqrt (fma -6 (* v v) 2))))>
1538300354.383 * [enter]simplify:  Simplifying (/ (sqrt (/ 4/3 PI)) (sqrt (- 1 (* v v))))
1538300354.384 * * [misc]simplify:  iters left: 6 (10 enodes)
1538300354.388 * * [misc]simplify:  iters left: 5 (14 enodes)
1538300354.393 * * [misc]simplify:  iters left: 4 (18 enodes)
1538300354.399 * * [misc]simplify:  iters left: 3 (20 enodes)
1538300354.406 * [exit]simplify:  Simplified to (/ (sqrt (/ 4/3 PI)) (sqrt (- 1 (* v v))))
1538300354.406 * [misc]simplify:  Simplified (2 1 1) to (λ (v) (/ (* (/ (sqrt (/ 4/3 PI)) (sqrt (- 1 (* v v)))) (/ (sqrt (/ 4/3 PI)) (sqrt (- 1 (* v v))))) (sqrt (fma -6 (* v v) 2))))
1538300354.406 * [enter]simplify:  Simplifying (/ (sqrt (/ 4/3 PI)) (sqrt (- 1 (* v v))))
1538300354.407 * * [misc]simplify:  iters left: 6 (10 enodes)
1538300354.411 * * [misc]simplify:  iters left: 5 (14 enodes)
1538300354.417 * * [misc]simplify:  iters left: 4 (18 enodes)
1538300354.423 * * [misc]simplify:  iters left: 3 (20 enodes)
1538300354.430 * [exit]simplify:  Simplified to (/ (sqrt (/ 4/3 PI)) (sqrt (- 1 (* v v))))
1538300354.430 * [misc]simplify:  Simplified (2 1 2) to (λ (v) (/ (* (/ (sqrt (/ 4/3 PI)) (sqrt (- 1 (* v v)))) (/ (sqrt (/ 4/3 PI)) (sqrt (- 1 (* v v))))) (sqrt (fma -6 (* v v) 2))))
1538300354.430 * * * * [misc]progress:  [ 29 / 52 ] simplifiying candidate #<alt (λ (v) (/ (* (/ (sqrt (/ 4/3 PI)) 1) (/ (sqrt (/ 4/3 PI)) (- 1 (* v v)))) (sqrt (fma -6 (* v v) 2))))>
1538300354.430 * [enter]simplify:  Simplifying (/ (sqrt (/ 4/3 PI)) 1)
1538300354.431 * * [misc]simplify:  iters left: 5 (6 enodes)
1538300354.434 * * [misc]simplify:  iters left: 4 (8 enodes)
1538300354.437 * * [misc]simplify:  iters left: 3 (10 enodes)
1538300354.439 * [exit]simplify:  Simplified to (sqrt (/ 4/3 PI))
1538300354.440 * [misc]simplify:  Simplified (2 1 1) to (λ (v) (/ (* (sqrt (/ 4/3 PI)) (/ (sqrt (/ 4/3 PI)) (- 1 (* v v)))) (sqrt (fma -6 (* v v) 2))))
1538300354.440 * [enter]simplify:  Simplifying (/ (sqrt (/ 4/3 PI)) (- 1 (* v v)))
1538300354.443 * * [misc]simplify:  iters left: 6 (9 enodes)
1538300354.447 * * [misc]simplify:  iters left: 5 (13 enodes)
1538300354.452 * * [misc]simplify:  iters left: 4 (17 enodes)
1538300354.457 * * [misc]simplify:  iters left: 3 (19 enodes)
1538300354.464 * [exit]simplify:  Simplified to (/ (sqrt (/ 4/3 PI)) (- 1 (* v v)))
1538300354.464 * [misc]simplify:  Simplified (2 1 2) to (λ (v) (/ (* (sqrt (/ 4/3 PI)) (/ (sqrt (/ 4/3 PI)) (- 1 (* v v)))) (sqrt (fma -6 (* v v) 2))))
1538300354.464 * * * * [misc]progress:  [ 30 / 52 ] simplifiying candidate #<alt (λ (v) (/ (* (/ 1 (* (cbrt (- 1 (* v v))) (cbrt (- 1 (* v v))))) (/ (/ 4/3 PI) (cbrt (- 1 (* v v))))) (sqrt (fma -6 (* v v) 2))))>
1538300354.464 * [enter]simplify:  Simplifying (/ 1 (* (cbrt (- 1 (* v v))) (cbrt (- 1 (* v v)))))
1538300354.465 * * [misc]simplify:  iters left: 6 (7 enodes)
1538300354.468 * * [misc]simplify:  iters left: 5 (13 enodes)
1538300354.474 * * [misc]simplify:  iters left: 4 (17 enodes)
1538300354.479 * * [misc]simplify:  iters left: 3 (19 enodes)
1538300354.486 * [exit]simplify:  Simplified to (/ (/ 1 (cbrt (- 1 (* v v)))) (cbrt (- 1 (* v v))))
1538300354.486 * [misc]simplify:  Simplified (2 1 1) to (λ (v) (/ (* (/ (/ 1 (cbrt (- 1 (* v v)))) (cbrt (- 1 (* v v)))) (/ (/ 4/3 PI) (cbrt (- 1 (* v v))))) (sqrt (fma -6 (* v v) 2))))
1538300354.486 * [enter]simplify:  Simplifying (/ (/ 4/3 PI) (cbrt (- 1 (* v v))))
1538300354.487 * * [misc]simplify:  iters left: 6 (9 enodes)
1538300354.491 * * [misc]simplify:  iters left: 5 (15 enodes)
1538300354.497 * * [misc]simplify:  iters left: 4 (22 enodes)
1538300354.504 * * [misc]simplify:  iters left: 3 (24 enodes)
1538300354.512 * [exit]simplify:  Simplified to (/ (/ 4/3 PI) (cbrt (- 1 (* v v))))
1538300354.512 * [misc]simplify:  Simplified (2 1 2) to (λ (v) (/ (* (/ 1 (* (cbrt (- 1 (* v v))) (cbrt (- 1 (* v v))))) (/ (/ 4/3 PI) (cbrt (- 1 (* v v))))) (sqrt (fma -6 (* v v) 2))))
1538300354.512 * * * * [misc]progress:  [ 31 / 52 ] simplifiying candidate #<alt (λ (v) (/ (* (/ 1 (sqrt (- 1 (* v v)))) (/ (/ 4/3 PI) (sqrt (- 1 (* v v))))) (sqrt (fma -6 (* v v) 2))))>
1538300354.512 * [enter]simplify:  Simplifying (/ 1 (sqrt (- 1 (* v v))))
1538300354.513 * * [misc]simplify:  iters left: 6 (6 enodes)
1538300354.516 * * [misc]simplify:  iters left: 5 (10 enodes)
1538300354.519 * * [misc]simplify:  iters left: 4 (14 enodes)
1538300354.525 * * [misc]simplify:  iters left: 3 (16 enodes)
1538300354.530 * [exit]simplify:  Simplified to (/ 1 (sqrt (- 1 (* v v))))
1538300354.530 * [misc]simplify:  Simplified (2 1 1) to (λ (v) (/ (* (/ 1 (sqrt (- 1 (* v v)))) (/ (/ 4/3 PI) (sqrt (- 1 (* v v))))) (sqrt (fma -6 (* v v) 2))))
1538300354.530 * [enter]simplify:  Simplifying (/ (/ 4/3 PI) (sqrt (- 1 (* v v))))
1538300354.531 * * [misc]simplify:  iters left: 6 (9 enodes)
1538300354.535 * * [misc]simplify:  iters left: 5 (15 enodes)
1538300354.541 * * [misc]simplify:  iters left: 4 (22 enodes)
1538300354.548 * * [misc]simplify:  iters left: 3 (24 enodes)
1538300354.556 * [exit]simplify:  Simplified to (/ (/ 4/3 PI) (sqrt (- 1 (* v v))))
1538300354.556 * [misc]simplify:  Simplified (2 1 2) to (λ (v) (/ (* (/ 1 (sqrt (- 1 (* v v)))) (/ (/ 4/3 PI) (sqrt (- 1 (* v v))))) (sqrt (fma -6 (* v v) 2))))
1538300354.557 * * * * [misc]progress:  [ 32 / 52 ] simplifiying candidate #<alt (λ (v) (/ (* (/ 1 1) (/ (/ 4/3 PI) (- 1 (* v v)))) (sqrt (fma -6 (* v v) 2))))>
1538300354.557 * [enter]simplify:  Simplifying (/ 1 1)
1538300354.557 * * [misc]simplify:  iters left: 2 (2 enodes)
1538300354.558 * * [misc]simplify:  iters left: 1 (4 enodes)
1538300354.559 * [exit]simplify:  Simplified to 1
1538300354.559 * [misc]simplify:  Simplified (2 1 1) to (λ (v) (/ (* 1 (/ (/ 4/3 PI) (- 1 (* v v)))) (sqrt (fma -6 (* v v) 2))))
1538300354.559 * [enter]simplify:  Simplifying (/ (/ 4/3 PI) (- 1 (* v v)))
1538300354.560 * * [misc]simplify:  iters left: 6 (8 enodes)
1538300354.564 * * [misc]simplify:  iters left: 5 (14 enodes)
1538300354.569 * * [misc]simplify:  iters left: 4 (21 enodes)
1538300354.578 * * [misc]simplify:  iters left: 3 (31 enodes)
1538300354.596 * * [misc]simplify:  iters left: 2 (47 enodes)
1538300354.612 * * [misc]simplify:  iters left: 1 (58 enodes)
1538300354.632 * [exit]simplify:  Simplified to (/ (/ 4/3 PI) (- 1 (* v v)))
1538300354.632 * [misc]simplify:  Simplified (2 1 2) to (λ (v) (/ (* 1 (/ (/ 4/3 PI) (- 1 (* v v)))) (sqrt (fma -6 (* v v) 2))))
1538300354.632 * * * * [misc]progress:  [ 33 / 52 ] simplifiying candidate #<alt (λ (v) (/ (* (/ 4/3 (* (cbrt (- 1 (* v v))) (cbrt (- 1 (* v v))))) (/ (/ 1 PI) (cbrt (- 1 (* v v))))) (sqrt (fma -6 (* v v) 2))))>
1538300354.633 * [enter]simplify:  Simplifying (/ 4/3 (* (cbrt (- 1 (* v v))) (cbrt (- 1 (* v v)))))
1538300354.633 * * [misc]simplify:  iters left: 6 (8 enodes)
1538300354.637 * * [misc]simplify:  iters left: 5 (14 enodes)
1538300354.642 * * [misc]simplify:  iters left: 4 (18 enodes)
1538300354.648 * * [misc]simplify:  iters left: 3 (20 enodes)
1538300354.654 * [exit]simplify:  Simplified to (/ 4/3 (* (cbrt (- 1 (* v v))) (cbrt (- 1 (* v v)))))
1538300354.654 * [misc]simplify:  Simplified (2 1 1) to (λ (v) (/ (* (/ 4/3 (* (cbrt (- 1 (* v v))) (cbrt (- 1 (* v v))))) (/ (/ 1 PI) (cbrt (- 1 (* v v))))) (sqrt (fma -6 (* v v) 2))))
1538300354.654 * [enter]simplify:  Simplifying (/ (/ 1 PI) (cbrt (- 1 (* v v))))
1538300354.655 * * [misc]simplify:  iters left: 6 (8 enodes)
1538300354.659 * * [misc]simplify:  iters left: 5 (14 enodes)
1538300354.665 * * [misc]simplify:  iters left: 4 (21 enodes)
1538300354.671 * * [misc]simplify:  iters left: 3 (23 enodes)
1538300354.679 * [exit]simplify:  Simplified to (/ (/ 1 PI) (cbrt (- 1 (* v v))))
1538300354.679 * [misc]simplify:  Simplified (2 1 2) to (λ (v) (/ (* (/ 4/3 (* (cbrt (- 1 (* v v))) (cbrt (- 1 (* v v))))) (/ (/ 1 PI) (cbrt (- 1 (* v v))))) (sqrt (fma -6 (* v v) 2))))
1538300354.679 * * * * [misc]progress:  [ 34 / 52 ] simplifiying candidate #<alt (λ (v) (/ (* (/ 4/3 (sqrt (- 1 (* v v)))) (/ (/ 1 PI) (sqrt (- 1 (* v v))))) (sqrt (fma -6 (* v v) 2))))>
1538300354.680 * [enter]simplify:  Simplifying (/ 4/3 (sqrt (- 1 (* v v))))
1538300354.680 * * [misc]simplify:  iters left: 6 (7 enodes)
1538300354.683 * * [misc]simplify:  iters left: 5 (11 enodes)
1538300354.688 * * [misc]simplify:  iters left: 4 (15 enodes)
1538300354.692 * * [misc]simplify:  iters left: 3 (17 enodes)
1538300354.698 * [exit]simplify:  Simplified to (/ 4/3 (sqrt (- 1 (* v v))))
1538300354.698 * [misc]simplify:  Simplified (2 1 1) to (λ (v) (/ (* (/ 4/3 (sqrt (- 1 (* v v)))) (/ (/ 1 PI) (sqrt (- 1 (* v v))))) (sqrt (fma -6 (* v v) 2))))
1538300354.698 * [enter]simplify:  Simplifying (/ (/ 1 PI) (sqrt (- 1 (* v v))))
1538300354.699 * * [misc]simplify:  iters left: 6 (8 enodes)
1538300354.702 * * [misc]simplify:  iters left: 5 (14 enodes)
1538300354.708 * * [misc]simplify:  iters left: 4 (21 enodes)
1538300354.715 * * [misc]simplify:  iters left: 3 (23 enodes)
1538300354.724 * [exit]simplify:  Simplified to (/ (/ 1 PI) (sqrt (- 1 (* v v))))
1538300354.725 * [misc]simplify:  Simplified (2 1 2) to (λ (v) (/ (* (/ 4/3 (sqrt (- 1 (* v v)))) (/ (/ 1 PI) (sqrt (- 1 (* v v))))) (sqrt (fma -6 (* v v) 2))))
1538300354.725 * * * * [misc]progress:  [ 35 / 52 ] simplifiying candidate #<alt (λ (v) (/ (* (/ 4/3 1) (/ (/ 1 PI) (- 1 (* v v)))) (sqrt (fma -6 (* v v) 2))))>
1538300354.725 * [enter]simplify:  Simplifying (/ 4/3 1)
1538300354.725 * * [misc]simplify:  iters left: 2 (3 enodes)
1538300354.726 * * [misc]simplify:  iters left: 1 (5 enodes)
1538300354.727 * [exit]simplify:  Simplified to 4/3
1538300354.728 * [misc]simplify:  Simplified (2 1 1) to (λ (v) (/ (* 4/3 (/ (/ 1 PI) (- 1 (* v v)))) (sqrt (fma -6 (* v v) 2))))
1538300354.728 * [enter]simplify:  Simplifying (/ (/ 1 PI) (- 1 (* v v)))
1538300354.728 * * [misc]simplify:  iters left: 6 (7 enodes)
1538300354.732 * * [misc]simplify:  iters left: 5 (13 enodes)
1538300354.737 * * [misc]simplify:  iters left: 4 (20 enodes)
1538300354.745 * * [misc]simplify:  iters left: 3 (30 enodes)
1538300354.760 * * [misc]simplify:  iters left: 2 (46 enodes)
1538300354.776 * * [misc]simplify:  iters left: 1 (57 enodes)
1538300354.795 * [exit]simplify:  Simplified to (/ (/ 1 PI) (- 1 (* v v)))
1538300354.795 * [misc]simplify:  Simplified (2 1 2) to (λ (v) (/ (* 4/3 (/ (/ 1 PI) (- 1 (* v v)))) (sqrt (fma -6 (* v v) 2))))
1538300354.795 * * * * [misc]progress:  [ 36 / 52 ] simplifiying candidate #<alt (λ (v) (/ (* 1 (/ (/ 4/3 PI) (- 1 (* v v)))) (sqrt (fma -6 (* v v) 2))))>
1538300354.796 * * * * [misc]progress:  [ 37 / 52 ] simplifiying candidate #<alt (λ (v) (/ (* (/ 4/3 PI) (/ 1 (- 1 (* v v)))) (sqrt (fma -6 (* v v) 2))))>
1538300354.796 * * * * [misc]progress:  [ 38 / 52 ] simplifiying candidate #<alt (λ (v) (/ (/ 1 (/ (- 1 (* v v)) (/ 4/3 PI))) (sqrt (fma -6 (* v v) 2))))>
1538300354.796 * * * * [misc]progress:  [ 39 / 52 ] simplifiying candidate #<alt (λ (v) (/ (/ (/ (/ 4/3 PI) (* (cbrt (- 1 (* v v))) (cbrt (- 1 (* v v))))) (cbrt (- 1 (* v v)))) (sqrt (fma -6 (* v v) 2))))>
1538300354.796 * [enter]simplify:  Simplifying (cbrt (- 1 (* v v)))
1538300354.797 * * [misc]simplify:  iters left: 5 (5 enodes)
1538300354.799 * * [misc]simplify:  iters left: 4 (9 enodes)
1538300354.802 * * [misc]simplify:  iters left: 3 (13 enodes)
1538300354.807 * * [misc]simplify:  iters left: 2 (15 enodes)
1538300354.811 * [exit]simplify:  Simplified to (cbrt (- 1 (* v v)))
1538300354.811 * [misc]simplify:  Simplified (2 1 2) to (λ (v) (/ (/ (/ (/ 4/3 PI) (* (cbrt (- 1 (* v v))) (cbrt (- 1 (* v v))))) (cbrt (- 1 (* v v)))) (sqrt (fma -6 (* v v) 2))))
1538300354.811 * * * * [misc]progress:  [ 40 / 52 ] simplifiying candidate #<alt (λ (v) (/ (/ (/ (/ 4/3 PI) (sqrt (- 1 (* v v)))) (sqrt (- 1 (* v v)))) (sqrt (fma -6 (* v v) 2))))>
1538300354.812 * [enter]simplify:  Simplifying (sqrt (- 1 (* v v)))
1538300354.812 * * [misc]simplify:  iters left: 5 (5 enodes)
1538300354.815 * * [misc]simplify:  iters left: 4 (9 enodes)
1538300354.818 * * [misc]simplify:  iters left: 3 (13 enodes)
1538300354.823 * * [misc]simplify:  iters left: 2 (15 enodes)
1538300354.827 * [exit]simplify:  Simplified to (sqrt (- 1 (* v v)))
1538300354.827 * [misc]simplify:  Simplified (2 1 2) to (λ (v) (/ (/ (/ (/ 4/3 PI) (sqrt (- 1 (* v v)))) (sqrt (- 1 (* v v)))) (sqrt (fma -6 (* v v) 2))))
1538300354.827 * * * * [misc]progress:  [ 41 / 52 ] simplifiying candidate #<alt (λ (v) (/ (/ (/ (/ 4/3 PI) 1) (- 1 (* v v))) (sqrt (fma -6 (* v v) 2))))>
1538300354.828 * [enter]simplify:  Simplifying (- 1 (* v v))
1538300354.828 * * [misc]simplify:  iters left: 4 (4 enodes)
1538300354.830 * * [misc]simplify:  iters left: 3 (8 enodes)
1538300354.833 * * [misc]simplify:  iters left: 2 (12 enodes)
1538300354.837 * * [misc]simplify:  iters left: 1 (14 enodes)
1538300354.841 * [exit]simplify:  Simplified to (- 1 (* v v))
1538300354.842 * [misc]simplify:  Simplified (2 1 2) to (λ (v) (/ (/ (/ (/ 4/3 PI) 1) (- 1 (* v v))) (sqrt (fma -6 (* v v) 2))))
1538300354.842 * * * * [misc]progress:  [ 42 / 52 ] simplifiying candidate #<alt (λ (v) (/ (/ (* (cbrt (/ 4/3 PI)) (cbrt (/ 4/3 PI))) (/ (- 1 (* v v)) (cbrt (/ 4/3 PI)))) (sqrt (fma -6 (* v v) 2))))>
1538300354.842 * [enter]simplify:  Simplifying (* (cbrt (/ 4/3 PI)) (cbrt (/ 4/3 PI)))
1538300354.842 * * [misc]simplify:  iters left: 5 (5 enodes)
1538300354.845 * [exit]simplify:  Simplified to (* (cbrt (/ 4/3 PI)) (cbrt (/ 4/3 PI)))
1538300354.845 * [misc]simplify:  Simplified (2 1 1) to (λ (v) (/ (/ (* (cbrt (/ 4/3 PI)) (cbrt (/ 4/3 PI))) (/ (- 1 (* v v)) (cbrt (/ 4/3 PI)))) (sqrt (fma -6 (* v v) 2))))
1538300354.845 * * * * [misc]progress:  [ 43 / 52 ] simplifiying candidate #<alt (λ (v) (/ (/ (sqrt (/ 4/3 PI)) (/ (- 1 (* v v)) (sqrt (/ 4/3 PI)))) (sqrt (fma -6 (* v v) 2))))>
1538300354.845 * [enter]simplify:  Simplifying (sqrt (/ 4/3 PI))
1538300354.846 * * [misc]simplify:  iters left: 3 (4 enodes)
1538300354.847 * [exit]simplify:  Simplified to (sqrt (/ 4/3 PI))
1538300354.847 * [misc]simplify:  Simplified (2 1 1) to (λ (v) (/ (/ (sqrt (/ 4/3 PI)) (/ (- 1 (* v v)) (sqrt (/ 4/3 PI)))) (sqrt (fma -6 (* v v) 2))))
1538300354.847 * * * * [misc]progress:  [ 44 / 52 ] simplifiying candidate #<alt (λ (v) (/ (/ 1 (/ (- 1 (* v v)) (/ 4/3 PI))) (sqrt (fma -6 (* v v) 2))))>
1538300354.847 * * * * [misc]progress:  [ 45 / 52 ] simplifiying candidate #<alt (λ (v) (/ (/ 4/3 (/ (- 1 (* v v)) (/ 1 PI))) (sqrt (fma -6 (* v v) 2))))>
1538300354.847 * * * * [misc]progress:  [ 46 / 52 ] simplifiying candidate #<alt (λ (v) (/ (* (/ (/ 4/3 PI) (- (pow 1 3) (pow (* v v) 3))) (+ (* 1 1) (+ (* (* v v) (* v v)) (* 1 (* v v))))) (sqrt (fma -6 (* v v) 2))))>
1538300354.848 * [enter]simplify:  Simplifying (+ (* 1 1) (+ (* (* v v) (* v v)) (* 1 (* v v))))
1538300354.849 * * [misc]simplify:  iters left: 6 (8 enodes)
1538300354.855 * * [misc]simplify:  iters left: 5 (25 enodes)
1538300354.874 * * [misc]simplify:  iters left: 4 (65 enodes)
1538300354.913 * * [misc]simplify:  iters left: 3 (129 enodes)
1538300354.987 * * [misc]simplify:  iters left: 2 (197 enodes)
1538300355.031 * * [misc]simplify:  iters left: 1 (243 enodes)
1538300355.072 * [exit]simplify:  Simplified to (fma (fma v v 1) (* v v) 1)
1538300355.072 * [misc]simplify:  Simplified (2 1 2) to (λ (v) (/ (* (/ (/ 4/3 PI) (- (pow 1 3) (pow (* v v) 3))) (fma (fma v v 1) (* v v) 1)) (sqrt (fma -6 (* v v) 2))))
1538300355.072 * * * * [misc]progress:  [ 47 / 52 ] simplifiying candidate #<alt (λ (v) (/ (* (/ (/ 4/3 PI) (- (* 1 1) (* (* v v) (* v v)))) (+ 1 (* v v))) (sqrt (fma -6 (* v v) 2))))>
1538300355.072 * [enter]simplify:  Simplifying (+ 1 (* v v))
1538300355.073 * * [misc]simplify:  iters left: 4 (4 enodes)
1538300355.074 * * [misc]simplify:  iters left: 3 (7 enodes)
1538300355.075 * * [misc]simplify:  iters left: 2 (8 enodes)
1538300355.076 * [exit]simplify:  Simplified to (fma v v 1)
1538300355.076 * [misc]simplify:  Simplified (2 1 2) to (λ (v) (/ (* (/ (/ 4/3 PI) (- (* 1 1) (* (* v v) (* v v)))) (fma v v 1)) (sqrt (fma -6 (* v v) 2))))
1538300355.077 * * * * [misc]progress:  [ 48 / 52 ] simplifiying candidate #<alt (λ (v) (/ (/ 4/3 (* (- 1 (* v v)) PI)) (sqrt (fma -6 (* v v) 2))))>
1538300355.077 * * * * [misc]progress:  [ 49 / 52 ] simplifiying candidate #<alt (λ (v) (/ (/ (/ 4/3 PI) (- 1 (* v v))) (sqrt (fma -6 (* v v) 2))))>
1538300355.077 * [enter]simplify:  Simplifying (/ (/ (/ 4/3 PI) (- 1 (* v v))) (sqrt (fma -6 (* v v) 2)))
1538300355.078 * * [misc]simplify:  iters left: 6 (13 enodes)
1538300355.084 * * [misc]simplify:  iters left: 5 (23 enodes)
1538300355.094 * * [misc]simplify:  iters left: 4 (43 enodes)
1538300355.117 * * [misc]simplify:  iters left: 3 (103 enodes)
1538300355.165 * * [misc]simplify:  iters left: 2 (199 enodes)
1538300355.258 * * [misc]simplify:  iters left: 1 (308 enodes)
1538300355.429 * [exit]simplify:  Simplified to (/ (/ (/ 4/3 PI) (- 1 (* v v))) (sqrt (fma (* v -6) v 2)))
1538300355.429 * [misc]simplify:  Simplified (2) to (λ (v) (/ (/ (/ 4/3 PI) (- 1 (* v v))) (sqrt (fma (* v -6) v 2))))
1538300355.429 * * * * [misc]progress:  [ 50 / 52 ] simplifiying candidate #<alt (λ (v) (/ (+ (* 4/3 (/ (pow v 2) PI)) (+ (* 4/3 (/ 1 PI)) (* 4/3 (/ (pow v 4) PI)))) (sqrt (fma -6 (* v v) 2))))>
1538300355.430 * [enter]simplify:  Simplifying (+ (* 4/3 (/ (pow v 2) PI)) (+ (* 4/3 (/ 1 PI)) (* 4/3 (/ (pow v 4) PI))))
1538300355.432 * * [misc]simplify:  iters left: 6 (16 enodes)
1538300355.443 * * [misc]simplify:  iters left: 5 (36 enodes)
1538300355.467 * * [misc]simplify:  iters left: 4 (72 enodes)
1538300355.510 * * [misc]simplify:  iters left: 3 (114 enodes)
1538300355.599 * * [misc]simplify:  iters left: 2 (170 enodes)
1538300355.676 * * [misc]simplify:  iters left: 1 (275 enodes)
1538300355.902 * [exit]simplify:  Simplified to (fma (/ 4/3 PI) (* v v) (fma (pow v 4) (/ 4/3 PI) (/ 4/3 PI)))
1538300355.902 * [misc]simplify:  Simplified (2 1) to (λ (v) (/ (fma (/ 4/3 PI) (* v v) (fma (pow v 4) (/ 4/3 PI) (/ 4/3 PI))) (sqrt (fma -6 (* v v) 2))))
1538300355.902 * * * * [misc]progress:  [ 51 / 52 ] simplifiying candidate #<alt (λ (v) (/ (- (+ (* 4/3 (/ 1 (* (pow v 2) PI))) (+ (* 4/3 (/ 1 (* (pow v 4) PI))) (* 4/3 (/ 1 (* (pow v 6) PI)))))) (sqrt (fma -6 (* v v) 2))))>
1538300355.902 * [enter]simplify:  Simplifying (- (+ (* 4/3 (/ 1 (* (pow v 2) PI))) (+ (* 4/3 (/ 1 (* (pow v 4) PI))) (* 4/3 (/ 1 (* (pow v 6) PI))))))
1538300355.903 * * [misc]simplify:  iters left: 6 (22 enodes)
1538300355.912 * * [misc]simplify:  iters left: 5 (52 enodes)
1538300355.931 * * [misc]simplify:  iters left: 4 (114 enodes)
1538300356.091 * * [misc]simplify:  iters left: 3 (271 enodes)
1538300356.674 * [exit]simplify:  Simplified to (- (/ -4/3 (* v (* v PI))) (+ (/ (/ 4/3 PI) (pow v 6)) (/ (/ 4/3 PI) (pow v 4))))
1538300356.674 * [misc]simplify:  Simplified (2 1) to (λ (v) (/ (- (/ -4/3 (* v (* v PI))) (+ (/ (/ 4/3 PI) (pow v 6)) (/ (/ 4/3 PI) (pow v 4)))) (sqrt (fma -6 (* v v) 2))))
1538300356.674 * * * * [misc]progress:  [ 52 / 52 ] simplifiying candidate #<alt (λ (v) (/ (- (+ (* 4/3 (/ 1 (* (pow v 2) PI))) (+ (* 4/3 (/ 1 (* (pow v 4) PI))) (* 4/3 (/ 1 (* (pow v 6) PI)))))) (sqrt (fma -6 (* v v) 2))))>
1538300356.674 * [enter]simplify:  Simplifying (- (+ (* 4/3 (/ 1 (* (pow v 2) PI))) (+ (* 4/3 (/ 1 (* (pow v 4) PI))) (* 4/3 (/ 1 (* (pow v 6) PI))))))
1538300356.676 * * [misc]simplify:  iters left: 6 (22 enodes)
1538300356.684 * * [misc]simplify:  iters left: 5 (52 enodes)
1538300356.704 * * [misc]simplify:  iters left: 4 (114 enodes)
1538300356.851 * * [misc]simplify:  iters left: 3 (271 enodes)
1538300357.545 * [exit]simplify:  Simplified to (- (/ -4/3 (* v (* v PI))) (+ (/ (/ 4/3 PI) (pow v 6)) (/ (/ 4/3 PI) (pow v 4))))
1538300357.545 * [misc]simplify:  Simplified (2 1) to (λ (v) (/ (- (/ -4/3 (* v (* v PI))) (+ (/ (/ 4/3 PI) (pow v 6)) (/ (/ 4/3 PI) (pow v 4)))) (sqrt (fma -6 (* v v) 2))))
1538300357.546 * * * [misc]progress:  adding candidates to table
1538300358.717 * [misc]progress:  [Phase 3 of 3] Extracting.
1538300358.729 * [enter]simplify:  Simplifying (/ (/ (/ 4/3 PI) (- 1 (* v v))) (sqrt (fma -6 (* v v) 2)))
1538300358.731 * * [misc]simplify:  iters left: 6 (13 enodes)
1538300358.732 * * [misc]simplify:  iters left: 5 (15 enodes)
1538300358.734 * [exit]simplify:  Simplified to (/ (/ (/ 4/3 PI) (- 1 (* v v))) (sqrt (fma -6 (* v v) 2)))
1538300358.734 * * * * [misc]points:  Sampling 8000 additional inputs, on iter 0 have 0 / 8000
1538300363.467 * * * * [misc]points:  Filtering points with unrepresentable outputs
1538300363.470 * * * * [misc]points:  Sampling 3990 additional inputs, on iter 1 have 4010 / 8000
1538300365.722 * * * * [misc]points:  Filtering points with unrepresentable outputs
1538300365.723 * * * * [misc]points:  Sampling 1979 additional inputs, on iter 2 have 6021 / 8000
1538300366.788 * * * * [misc]points:  Filtering points with unrepresentable outputs
1538300366.788 * * * * [misc]points:  Sampling 992 additional inputs, on iter 3 have 7008 / 8000
1538300367.282 * * * * [misc]points:  Filtering points with unrepresentable outputs
1538300367.282 * * * * [misc]points:  Sampling 499 additional inputs, on iter 4 have 7501 / 8000
1538300367.968 * * * * [misc]points:  Filtering points with unrepresentable outputs
1538300367.968 * * * * [misc]points:  Sampling 263 additional inputs, on iter 5 have 7737 / 8000
1538300368.092 * * * * [misc]points:  Filtering points with unrepresentable outputs
1538300368.093 * * * * [misc]points:  Sampling 137 additional inputs, on iter 6 have 7863 / 8000
1538300368.193 * * * * [misc]points:  Filtering points with unrepresentable outputs
1538300368.194 * * * * [misc]points:  Sampling 59 additional inputs, on iter 7 have 7941 / 8000
1538300368.219 * * * * [misc]points:  Filtering points with unrepresentable outputs
1538300368.219 * * * * [misc]points:  Sampling 34 additional inputs, on iter 8 have 7966 / 8000
1538300368.241 * * * * [misc]points:  Filtering points with unrepresentable outputs
1538300368.242 * * * * [misc]points:  Sampling 14 additional inputs, on iter 9 have 7986 / 8000
1538300368.254 * * * * [misc]points:  Filtering points with unrepresentable outputs
1538300368.254 * * * * [misc]points:  Sampling 8 additional inputs, on iter 10 have 7992 / 8000
1538300368.264 * * * * [misc]points:  Filtering points with unrepresentable outputs
1538300368.264 * * * * [misc]points:  Sampling 4 additional inputs, on iter 11 have 7996 / 8000
1538300368.273 * * * * [misc]points:  Filtering points with unrepresentable outputs
1538300368.273 * * * * [misc]points:  Sampling 4 additional inputs, on iter 12 have 7996 / 8000
1538300368.280 * * * * [misc]points:  Filtering points with unrepresentable outputs
1538300368.281 * * * * [misc]points:  Sampling 4 additional inputs, on iter 13 have 7999 / 8000
1538300368.288 * * * * [misc]points:  Filtering points with unrepresentable outputs
1538300368.288 * * * * [exit]points:  Sampled 8001 points with exact outputs