833.951 * [progress]: [Phase 1 of 3] Setting up.
0.001 * * * [progress]: [1/2] Preparing points
0.048 * * * [progress]: [2/2] Setting up program.
0.051 * [progress]: [Phase 2 of 3] Improving.
0.051 * [simplify]: Simplifying using  #<procedure:simplify-batch-regraph> :
   (/ (+ 1.0 (* (- 2.0 (/ (/ 2.0 t) (+ 1.0 (/ 1.0 t)))) (- 2.0 (/ (/ 2.0 t) (+ 1.0 (/ 1.0 t)))))) (+ 2.0 (* (- 2.0 (/ (/ 2.0 t) (+ 1.0 (/ 1.0 t)))) (- 2.0 (/ (/ 2.0 t) (+ 1.0 (/ 1.0 t)))))))
0.052 * * [simplify]: iteration  0 :  12  enodes  (cost  51 )
0.054 * * [simplify]: iteration  1 :  19  enodes  (cost  51 )
0.056 * * [simplify]: iteration  2 :  33  enodes  (cost  51 )
0.061 * * [simplify]: iteration  3 :  80  enodes  (cost  51 )
0.078 * * [simplify]: iteration  4 :  237  enodes  (cost  51 )
0.144 * * [simplify]: iteration  5 :  603  enodes  (cost  51 )
0.437 * * [simplify]: iteration  6 :  1418  enodes  (cost  51 )
1.844 * * [simplify]: iteration  7 :  3672  enodes  (cost  43 )
2.709 * * [simplify]: iteration  done :  5000  enodes  (cost  43 )
2.709 * [simplify]: Simplified to:
   (/ (+ (* (- 2.0 (/ 2.0 (* 1.0 (+ t 1)))) (- 2.0 (/ 2.0 (* 1.0 (+ t 1))))) 1.0) (+ 2.0 (* (- 2.0 (/ 2.0 (* 1.0 (+ t 1)))) (- 2.0 (/ 2.0 (* 1.0 (+ t 1)))))))
2.714 * * [progress]: iteration 1 / 4
2.714 * * * [progress]: picking best candidate
2.717 * * * * [pick]: Picked  #<alt (λ (t) (/ (+ (* (- 2.0 (/ 2.0 (* 1.0 (+ t 1)))) (- 2.0 (/ 2.0 (* 1.0 (+ t 1))))) 1.0) (+ 2.0 (* (- 2.0 (/ 2.0 (* 1.0 (+ t 1)))) (- 2.0 (/ 2.0 (* 1.0 (+ t 1))))))))>
2.717 * * * [progress]: localizing error
2.728 * * * [progress]: generating rewritten candidates
2.729 * * * * [progress]: [ 1 / 4 ] rewriting at (2 2 2 2)
2.735 * * * * [progress]: [ 2 / 4 ] rewriting at (2 2 2 1)
2.742 * * * * [progress]: [ 3 / 4 ] rewriting at (2 1 1 2)
2.753 * * * * [progress]: [ 4 / 4 ] rewriting at (2 1 1 1)
2.761 * * * [progress]: generating series expansions
2.762 * * * * [progress]: [ 1 / 4 ] generating series at (2 2 2 2)
2.762 * [approximate]: Taking taylor expansion of (- 2.0 (* 2.0 (/ 1 (+ t 1)))) in (t) around 0
2.762 * [taylor]: Taking taylor expansion of (- 2.0 (* 2.0 (/ 1 (+ t 1)))) in t
2.762 * [taylor]: Taking taylor expansion of 2.0 in t
2.762 * [taylor]: Taking taylor expansion of (* 2.0 (/ 1 (+ t 1))) in t
2.762 * [taylor]: Taking taylor expansion of 2.0 in t
2.762 * [taylor]: Taking taylor expansion of (/ 1 (+ t 1)) in t
2.762 * [taylor]: Taking taylor expansion of (+ t 1) in t
2.762 * [taylor]: Taking taylor expansion of t in t
2.762 * [taylor]: Taking taylor expansion of 1 in t
2.762 * [taylor]: Taking taylor expansion of (- 2.0 (* 2.0 (/ 1 (+ t 1)))) in t
2.762 * [taylor]: Taking taylor expansion of 2.0 in t
2.762 * [taylor]: Taking taylor expansion of (* 2.0 (/ 1 (+ t 1))) in t
2.762 * [taylor]: Taking taylor expansion of 2.0 in t
2.762 * [taylor]: Taking taylor expansion of (/ 1 (+ t 1)) in t
2.762 * [taylor]: Taking taylor expansion of (+ t 1) in t
2.762 * [taylor]: Taking taylor expansion of t in t
2.762 * [taylor]: Taking taylor expansion of 1 in t
2.763 * [approximate]: Taking taylor expansion of (- 2.0 (* 2.0 (/ 1 (+ (/ 1 t) 1)))) in (t) around 0
2.763 * [taylor]: Taking taylor expansion of (- 2.0 (* 2.0 (/ 1 (+ (/ 1 t) 1)))) in t
2.763 * [taylor]: Taking taylor expansion of 2.0 in t
2.763 * [taylor]: Taking taylor expansion of (* 2.0 (/ 1 (+ (/ 1 t) 1))) in t
2.763 * [taylor]: Taking taylor expansion of 2.0 in t
2.763 * [taylor]: Taking taylor expansion of (/ 1 (+ (/ 1 t) 1)) in t
2.763 * [taylor]: Taking taylor expansion of (+ (/ 1 t) 1) in t
2.763 * [taylor]: Taking taylor expansion of (/ 1 t) in t
2.763 * [taylor]: Taking taylor expansion of t in t
2.763 * [taylor]: Taking taylor expansion of 1 in t
2.763 * [taylor]: Taking taylor expansion of (- 2.0 (* 2.0 (/ 1 (+ (/ 1 t) 1)))) in t
2.763 * [taylor]: Taking taylor expansion of 2.0 in t
2.763 * [taylor]: Taking taylor expansion of (* 2.0 (/ 1 (+ (/ 1 t) 1))) in t
2.763 * [taylor]: Taking taylor expansion of 2.0 in t
2.763 * [taylor]: Taking taylor expansion of (/ 1 (+ (/ 1 t) 1)) in t
2.763 * [taylor]: Taking taylor expansion of (+ (/ 1 t) 1) in t
2.763 * [taylor]: Taking taylor expansion of (/ 1 t) in t
2.763 * [taylor]: Taking taylor expansion of t in t
2.763 * [taylor]: Taking taylor expansion of 1 in t
2.764 * [approximate]: Taking taylor expansion of (- 2.0 (* 2.0 (/ 1 (- 1 (/ 1 t))))) in (t) around 0
2.764 * [taylor]: Taking taylor expansion of (- 2.0 (* 2.0 (/ 1 (- 1 (/ 1 t))))) in t
2.764 * [taylor]: Taking taylor expansion of 2.0 in t
2.764 * [taylor]: Taking taylor expansion of (* 2.0 (/ 1 (- 1 (/ 1 t)))) in t
2.764 * [taylor]: Taking taylor expansion of 2.0 in t
2.764 * [taylor]: Taking taylor expansion of (/ 1 (- 1 (/ 1 t))) in t
2.764 * [taylor]: Taking taylor expansion of (- 1 (/ 1 t)) in t
2.764 * [taylor]: Taking taylor expansion of 1 in t
2.764 * [taylor]: Taking taylor expansion of (/ 1 t) in t
2.764 * [taylor]: Taking taylor expansion of t in t
2.764 * [taylor]: Taking taylor expansion of (- 2.0 (* 2.0 (/ 1 (- 1 (/ 1 t))))) in t
2.764 * [taylor]: Taking taylor expansion of 2.0 in t
2.764 * [taylor]: Taking taylor expansion of (* 2.0 (/ 1 (- 1 (/ 1 t)))) in t
2.764 * [taylor]: Taking taylor expansion of 2.0 in t
2.764 * [taylor]: Taking taylor expansion of (/ 1 (- 1 (/ 1 t))) in t
2.764 * [taylor]: Taking taylor expansion of (- 1 (/ 1 t)) in t
2.764 * [taylor]: Taking taylor expansion of 1 in t
2.764 * [taylor]: Taking taylor expansion of (/ 1 t) in t
2.764 * [taylor]: Taking taylor expansion of t in t
2.765 * * * * [progress]: [ 2 / 4 ] generating series at (2 2 2 1)
2.765 * [approximate]: Taking taylor expansion of (- 2.0 (* 2.0 (/ 1 (+ t 1)))) in (t) around 0
2.765 * [taylor]: Taking taylor expansion of (- 2.0 (* 2.0 (/ 1 (+ t 1)))) in t
2.765 * [taylor]: Taking taylor expansion of 2.0 in t
2.765 * [taylor]: Taking taylor expansion of (* 2.0 (/ 1 (+ t 1))) in t
2.765 * [taylor]: Taking taylor expansion of 2.0 in t
2.765 * [taylor]: Taking taylor expansion of (/ 1 (+ t 1)) in t
2.765 * [taylor]: Taking taylor expansion of (+ t 1) in t
2.765 * [taylor]: Taking taylor expansion of t in t
2.765 * [taylor]: Taking taylor expansion of 1 in t
2.765 * [taylor]: Taking taylor expansion of (- 2.0 (* 2.0 (/ 1 (+ t 1)))) in t
2.765 * [taylor]: Taking taylor expansion of 2.0 in t
2.765 * [taylor]: Taking taylor expansion of (* 2.0 (/ 1 (+ t 1))) in t
2.765 * [taylor]: Taking taylor expansion of 2.0 in t
2.765 * [taylor]: Taking taylor expansion of (/ 1 (+ t 1)) in t
2.765 * [taylor]: Taking taylor expansion of (+ t 1) in t
2.765 * [taylor]: Taking taylor expansion of t in t
2.765 * [taylor]: Taking taylor expansion of 1 in t
2.766 * [approximate]: Taking taylor expansion of (- 2.0 (* 2.0 (/ 1 (+ (/ 1 t) 1)))) in (t) around 0
2.766 * [taylor]: Taking taylor expansion of (- 2.0 (* 2.0 (/ 1 (+ (/ 1 t) 1)))) in t
2.766 * [taylor]: Taking taylor expansion of 2.0 in t
2.766 * [taylor]: Taking taylor expansion of (* 2.0 (/ 1 (+ (/ 1 t) 1))) in t
2.766 * [taylor]: Taking taylor expansion of 2.0 in t
2.766 * [taylor]: Taking taylor expansion of (/ 1 (+ (/ 1 t) 1)) in t
2.766 * [taylor]: Taking taylor expansion of (+ (/ 1 t) 1) in t
2.766 * [taylor]: Taking taylor expansion of (/ 1 t) in t
2.766 * [taylor]: Taking taylor expansion of t in t
2.766 * [taylor]: Taking taylor expansion of 1 in t
2.766 * [taylor]: Taking taylor expansion of (- 2.0 (* 2.0 (/ 1 (+ (/ 1 t) 1)))) in t
2.766 * [taylor]: Taking taylor expansion of 2.0 in t
2.766 * [taylor]: Taking taylor expansion of (* 2.0 (/ 1 (+ (/ 1 t) 1))) in t
2.766 * [taylor]: Taking taylor expansion of 2.0 in t
2.766 * [taylor]: Taking taylor expansion of (/ 1 (+ (/ 1 t) 1)) in t
2.766 * [taylor]: Taking taylor expansion of (+ (/ 1 t) 1) in t
2.766 * [taylor]: Taking taylor expansion of (/ 1 t) in t
2.766 * [taylor]: Taking taylor expansion of t in t
2.766 * [taylor]: Taking taylor expansion of 1 in t
2.767 * [approximate]: Taking taylor expansion of (- 2.0 (* 2.0 (/ 1 (- 1 (/ 1 t))))) in (t) around 0
2.767 * [taylor]: Taking taylor expansion of (- 2.0 (* 2.0 (/ 1 (- 1 (/ 1 t))))) in t
2.767 * [taylor]: Taking taylor expansion of 2.0 in t
2.767 * [taylor]: Taking taylor expansion of (* 2.0 (/ 1 (- 1 (/ 1 t)))) in t
2.767 * [taylor]: Taking taylor expansion of 2.0 in t
2.767 * [taylor]: Taking taylor expansion of (/ 1 (- 1 (/ 1 t))) in t
2.767 * [taylor]: Taking taylor expansion of (- 1 (/ 1 t)) in t
2.767 * [taylor]: Taking taylor expansion of 1 in t
2.767 * [taylor]: Taking taylor expansion of (/ 1 t) in t
2.767 * [taylor]: Taking taylor expansion of t in t
2.767 * [taylor]: Taking taylor expansion of (- 2.0 (* 2.0 (/ 1 (- 1 (/ 1 t))))) in t
2.767 * [taylor]: Taking taylor expansion of 2.0 in t
2.767 * [taylor]: Taking taylor expansion of (* 2.0 (/ 1 (- 1 (/ 1 t)))) in t
2.767 * [taylor]: Taking taylor expansion of 2.0 in t
2.767 * [taylor]: Taking taylor expansion of (/ 1 (- 1 (/ 1 t))) in t
2.767 * [taylor]: Taking taylor expansion of (- 1 (/ 1 t)) in t
2.767 * [taylor]: Taking taylor expansion of 1 in t
2.767 * [taylor]: Taking taylor expansion of (/ 1 t) in t
2.767 * [taylor]: Taking taylor expansion of t in t
2.767 * * * * [progress]: [ 3 / 4 ] generating series at (2 1 1 2)
2.768 * [approximate]: Taking taylor expansion of (- 2.0 (* 2.0 (/ 1 (+ t 1)))) in (t) around 0
2.768 * [taylor]: Taking taylor expansion of (- 2.0 (* 2.0 (/ 1 (+ t 1)))) in t
2.768 * [taylor]: Taking taylor expansion of 2.0 in t
2.768 * [taylor]: Taking taylor expansion of (* 2.0 (/ 1 (+ t 1))) in t
2.768 * [taylor]: Taking taylor expansion of 2.0 in t
2.768 * [taylor]: Taking taylor expansion of (/ 1 (+ t 1)) in t
2.768 * [taylor]: Taking taylor expansion of (+ t 1) in t
2.768 * [taylor]: Taking taylor expansion of t in t
2.768 * [taylor]: Taking taylor expansion of 1 in t
2.768 * [taylor]: Taking taylor expansion of (- 2.0 (* 2.0 (/ 1 (+ t 1)))) in t
2.768 * [taylor]: Taking taylor expansion of 2.0 in t
2.768 * [taylor]: Taking taylor expansion of (* 2.0 (/ 1 (+ t 1))) in t
2.768 * [taylor]: Taking taylor expansion of 2.0 in t
2.768 * [taylor]: Taking taylor expansion of (/ 1 (+ t 1)) in t
2.768 * [taylor]: Taking taylor expansion of (+ t 1) in t
2.768 * [taylor]: Taking taylor expansion of t in t
2.768 * [taylor]: Taking taylor expansion of 1 in t
2.769 * [approximate]: Taking taylor expansion of (- 2.0 (* 2.0 (/ 1 (+ (/ 1 t) 1)))) in (t) around 0
2.769 * [taylor]: Taking taylor expansion of (- 2.0 (* 2.0 (/ 1 (+ (/ 1 t) 1)))) in t
2.769 * [taylor]: Taking taylor expansion of 2.0 in t
2.769 * [taylor]: Taking taylor expansion of (* 2.0 (/ 1 (+ (/ 1 t) 1))) in t
2.769 * [taylor]: Taking taylor expansion of 2.0 in t
2.769 * [taylor]: Taking taylor expansion of (/ 1 (+ (/ 1 t) 1)) in t
2.769 * [taylor]: Taking taylor expansion of (+ (/ 1 t) 1) in t
2.769 * [taylor]: Taking taylor expansion of (/ 1 t) in t
2.769 * [taylor]: Taking taylor expansion of t in t
2.769 * [taylor]: Taking taylor expansion of 1 in t
2.769 * [taylor]: Taking taylor expansion of (- 2.0 (* 2.0 (/ 1 (+ (/ 1 t) 1)))) in t
2.769 * [taylor]: Taking taylor expansion of 2.0 in t
2.769 * [taylor]: Taking taylor expansion of (* 2.0 (/ 1 (+ (/ 1 t) 1))) in t
2.769 * [taylor]: Taking taylor expansion of 2.0 in t
2.769 * [taylor]: Taking taylor expansion of (/ 1 (+ (/ 1 t) 1)) in t
2.769 * [taylor]: Taking taylor expansion of (+ (/ 1 t) 1) in t
2.769 * [taylor]: Taking taylor expansion of (/ 1 t) in t
2.769 * [taylor]: Taking taylor expansion of t in t
2.769 * [taylor]: Taking taylor expansion of 1 in t
2.769 * [approximate]: Taking taylor expansion of (- 2.0 (* 2.0 (/ 1 (- 1 (/ 1 t))))) in (t) around 0
2.769 * [taylor]: Taking taylor expansion of (- 2.0 (* 2.0 (/ 1 (- 1 (/ 1 t))))) in t
2.770 * [taylor]: Taking taylor expansion of 2.0 in t
2.770 * [taylor]: Taking taylor expansion of (* 2.0 (/ 1 (- 1 (/ 1 t)))) in t
2.770 * [taylor]: Taking taylor expansion of 2.0 in t
2.770 * [taylor]: Taking taylor expansion of (/ 1 (- 1 (/ 1 t))) in t
2.770 * [taylor]: Taking taylor expansion of (- 1 (/ 1 t)) in t
2.770 * [taylor]: Taking taylor expansion of 1 in t
2.770 * [taylor]: Taking taylor expansion of (/ 1 t) in t
2.770 * [taylor]: Taking taylor expansion of t in t
2.770 * [taylor]: Taking taylor expansion of (- 2.0 (* 2.0 (/ 1 (- 1 (/ 1 t))))) in t
2.770 * [taylor]: Taking taylor expansion of 2.0 in t
2.770 * [taylor]: Taking taylor expansion of (* 2.0 (/ 1 (- 1 (/ 1 t)))) in t
2.770 * [taylor]: Taking taylor expansion of 2.0 in t
2.770 * [taylor]: Taking taylor expansion of (/ 1 (- 1 (/ 1 t))) in t
2.770 * [taylor]: Taking taylor expansion of (- 1 (/ 1 t)) in t
2.770 * [taylor]: Taking taylor expansion of 1 in t
2.770 * [taylor]: Taking taylor expansion of (/ 1 t) in t
2.770 * [taylor]: Taking taylor expansion of t in t
2.770 * * * * [progress]: [ 4 / 4 ] generating series at (2 1 1 1)
2.770 * [approximate]: Taking taylor expansion of (- 2.0 (* 2.0 (/ 1 (+ t 1)))) in (t) around 0
2.770 * [taylor]: Taking taylor expansion of (- 2.0 (* 2.0 (/ 1 (+ t 1)))) in t
2.770 * [taylor]: Taking taylor expansion of 2.0 in t
2.770 * [taylor]: Taking taylor expansion of (* 2.0 (/ 1 (+ t 1))) in t
2.770 * [taylor]: Taking taylor expansion of 2.0 in t
2.771 * [taylor]: Taking taylor expansion of (/ 1 (+ t 1)) in t
2.771 * [taylor]: Taking taylor expansion of (+ t 1) in t
2.771 * [taylor]: Taking taylor expansion of t in t
2.771 * [taylor]: Taking taylor expansion of 1 in t
2.771 * [taylor]: Taking taylor expansion of (- 2.0 (* 2.0 (/ 1 (+ t 1)))) in t
2.771 * [taylor]: Taking taylor expansion of 2.0 in t
2.771 * [taylor]: Taking taylor expansion of (* 2.0 (/ 1 (+ t 1))) in t
2.771 * [taylor]: Taking taylor expansion of 2.0 in t
2.771 * [taylor]: Taking taylor expansion of (/ 1 (+ t 1)) in t
2.771 * [taylor]: Taking taylor expansion of (+ t 1) in t
2.771 * [taylor]: Taking taylor expansion of t in t
2.771 * [taylor]: Taking taylor expansion of 1 in t
2.771 * [approximate]: Taking taylor expansion of (- 2.0 (* 2.0 (/ 1 (+ (/ 1 t) 1)))) in (t) around 0
2.771 * [taylor]: Taking taylor expansion of (- 2.0 (* 2.0 (/ 1 (+ (/ 1 t) 1)))) in t
2.771 * [taylor]: Taking taylor expansion of 2.0 in t
2.772 * [taylor]: Taking taylor expansion of (* 2.0 (/ 1 (+ (/ 1 t) 1))) in t
2.772 * [taylor]: Taking taylor expansion of 2.0 in t
2.772 * [taylor]: Taking taylor expansion of (/ 1 (+ (/ 1 t) 1)) in t
2.772 * [taylor]: Taking taylor expansion of (+ (/ 1 t) 1) in t
2.772 * [taylor]: Taking taylor expansion of (/ 1 t) in t
2.772 * [taylor]: Taking taylor expansion of t in t
2.772 * [taylor]: Taking taylor expansion of 1 in t
2.772 * [taylor]: Taking taylor expansion of (- 2.0 (* 2.0 (/ 1 (+ (/ 1 t) 1)))) in t
2.772 * [taylor]: Taking taylor expansion of 2.0 in t
2.772 * [taylor]: Taking taylor expansion of (* 2.0 (/ 1 (+ (/ 1 t) 1))) in t
2.772 * [taylor]: Taking taylor expansion of 2.0 in t
2.772 * [taylor]: Taking taylor expansion of (/ 1 (+ (/ 1 t) 1)) in t
2.772 * [taylor]: Taking taylor expansion of (+ (/ 1 t) 1) in t
2.772 * [taylor]: Taking taylor expansion of (/ 1 t) in t
2.772 * [taylor]: Taking taylor expansion of t in t
2.772 * [taylor]: Taking taylor expansion of 1 in t
2.772 * [approximate]: Taking taylor expansion of (- 2.0 (* 2.0 (/ 1 (- 1 (/ 1 t))))) in (t) around 0
2.772 * [taylor]: Taking taylor expansion of (- 2.0 (* 2.0 (/ 1 (- 1 (/ 1 t))))) in t
2.772 * [taylor]: Taking taylor expansion of 2.0 in t
2.772 * [taylor]: Taking taylor expansion of (* 2.0 (/ 1 (- 1 (/ 1 t)))) in t
2.772 * [taylor]: Taking taylor expansion of 2.0 in t
2.772 * [taylor]: Taking taylor expansion of (/ 1 (- 1 (/ 1 t))) in t
2.772 * [taylor]: Taking taylor expansion of (- 1 (/ 1 t)) in t
2.772 * [taylor]: Taking taylor expansion of 1 in t
2.772 * [taylor]: Taking taylor expansion of (/ 1 t) in t
2.772 * [taylor]: Taking taylor expansion of t in t
2.773 * [taylor]: Taking taylor expansion of (- 2.0 (* 2.0 (/ 1 (- 1 (/ 1 t))))) in t
2.773 * [taylor]: Taking taylor expansion of 2.0 in t
2.773 * [taylor]: Taking taylor expansion of (* 2.0 (/ 1 (- 1 (/ 1 t)))) in t
2.773 * [taylor]: Taking taylor expansion of 2.0 in t
2.773 * [taylor]: Taking taylor expansion of (/ 1 (- 1 (/ 1 t))) in t
2.773 * [taylor]: Taking taylor expansion of (- 1 (/ 1 t)) in t
2.773 * [taylor]: Taking taylor expansion of 1 in t
2.773 * [taylor]: Taking taylor expansion of (/ 1 t) in t
2.773 * [taylor]: Taking taylor expansion of t in t
2.773 * * * [progress]: simplifying candidates
2.774 * [simplify]: Simplifying using  #<procedure:simplify-batch-regraph> :
   (/ (exp 2.0) (exp (/ 2.0 (* 1.0 (+ t 1)))))
  (log (- 2.0 (/ 2.0 (* 1.0 (+ t 1)))))
  (exp (- 2.0 (/ 2.0 (* 1.0 (+ t 1)))))
  (* (cbrt (- 2.0 (/ 2.0 (* 1.0 (+ t 1))))) (cbrt (- 2.0 (/ 2.0 (* 1.0 (+ t 1))))))
  (cbrt (- 2.0 (/ 2.0 (* 1.0 (+ t 1)))))
  (* (* (- 2.0 (/ 2.0 (* 1.0 (+ t 1)))) (- 2.0 (/ 2.0 (* 1.0 (+ t 1))))) (- 2.0 (/ 2.0 (* 1.0 (+ t 1)))))
  (sqrt (- 2.0 (/ 2.0 (* 1.0 (+ t 1)))))
  (sqrt (- 2.0 (/ 2.0 (* 1.0 (+ t 1)))))
  (- (pow 2.0 3) (pow (/ 2.0 (* 1.0 (+ t 1))) 3))
  (+ (* 2.0 2.0) (+ (* (/ 2.0 (* 1.0 (+ t 1))) (/ 2.0 (* 1.0 (+ t 1)))) (* 2.0 (/ 2.0 (* 1.0 (+ t 1))))))
  (neg (/ 2.0 (* 1.0 (+ t 1))))
  (- (* 2.0 2.0) (* (/ 2.0 (* 1.0 (+ t 1))) (/ 2.0 (* 1.0 (+ t 1)))))
  (+ 2.0 (/ 2.0 (* 1.0 (+ t 1))))
  (+ (sqrt 2.0) (sqrt (/ 2.0 (* 1.0 (+ t 1)))))
  (- (sqrt 2.0) (sqrt (/ 2.0 (* 1.0 (+ t 1)))))
  (- 2.0 (/ 2.0 (* 1.0 (+ t 1))))
  (neg (/ 2.0 (* 1.0 (+ t 1))))
  (/ (exp 2.0) (exp (/ 2.0 (* 1.0 (+ t 1)))))
  (log (- 2.0 (/ 2.0 (* 1.0 (+ t 1)))))
  (exp (- 2.0 (/ 2.0 (* 1.0 (+ t 1)))))
  (* (cbrt (- 2.0 (/ 2.0 (* 1.0 (+ t 1))))) (cbrt (- 2.0 (/ 2.0 (* 1.0 (+ t 1))))))
  (cbrt (- 2.0 (/ 2.0 (* 1.0 (+ t 1)))))
  (* (* (- 2.0 (/ 2.0 (* 1.0 (+ t 1)))) (- 2.0 (/ 2.0 (* 1.0 (+ t 1))))) (- 2.0 (/ 2.0 (* 1.0 (+ t 1)))))
  (sqrt (- 2.0 (/ 2.0 (* 1.0 (+ t 1)))))
  (sqrt (- 2.0 (/ 2.0 (* 1.0 (+ t 1)))))
  (- (pow 2.0 3) (pow (/ 2.0 (* 1.0 (+ t 1))) 3))
  (+ (* 2.0 2.0) (+ (* (/ 2.0 (* 1.0 (+ t 1))) (/ 2.0 (* 1.0 (+ t 1)))) (* 2.0 (/ 2.0 (* 1.0 (+ t 1))))))
  (neg (/ 2.0 (* 1.0 (+ t 1))))
  (- (* 2.0 2.0) (* (/ 2.0 (* 1.0 (+ t 1))) (/ 2.0 (* 1.0 (+ t 1)))))
  (+ 2.0 (/ 2.0 (* 1.0 (+ t 1))))
  (+ (sqrt 2.0) (sqrt (/ 2.0 (* 1.0 (+ t 1)))))
  (- (sqrt 2.0) (sqrt (/ 2.0 (* 1.0 (+ t 1)))))
  (- 2.0 (/ 2.0 (* 1.0 (+ t 1))))
  (neg (/ 2.0 (* 1.0 (+ t 1))))
  (/ (exp 2.0) (exp (/ 2.0 (* 1.0 (+ t 1)))))
  (log (- 2.0 (/ 2.0 (* 1.0 (+ t 1)))))
  (exp (- 2.0 (/ 2.0 (* 1.0 (+ t 1)))))
  (* (cbrt (- 2.0 (/ 2.0 (* 1.0 (+ t 1))))) (cbrt (- 2.0 (/ 2.0 (* 1.0 (+ t 1))))))
  (cbrt (- 2.0 (/ 2.0 (* 1.0 (+ t 1)))))
  (* (* (- 2.0 (/ 2.0 (* 1.0 (+ t 1)))) (- 2.0 (/ 2.0 (* 1.0 (+ t 1))))) (- 2.0 (/ 2.0 (* 1.0 (+ t 1)))))
  (sqrt (- 2.0 (/ 2.0 (* 1.0 (+ t 1)))))
  (sqrt (- 2.0 (/ 2.0 (* 1.0 (+ t 1)))))
  (- (pow 2.0 3) (pow (/ 2.0 (* 1.0 (+ t 1))) 3))
  (+ (* 2.0 2.0) (+ (* (/ 2.0 (* 1.0 (+ t 1))) (/ 2.0 (* 1.0 (+ t 1)))) (* 2.0 (/ 2.0 (* 1.0 (+ t 1))))))
  (neg (/ 2.0 (* 1.0 (+ t 1))))
  (- (* 2.0 2.0) (* (/ 2.0 (* 1.0 (+ t 1))) (/ 2.0 (* 1.0 (+ t 1)))))
  (+ 2.0 (/ 2.0 (* 1.0 (+ t 1))))
  (+ (sqrt 2.0) (sqrt (/ 2.0 (* 1.0 (+ t 1)))))
  (- (sqrt 2.0) (sqrt (/ 2.0 (* 1.0 (+ t 1)))))
  (- 2.0 (/ 2.0 (* 1.0 (+ t 1))))
  (neg (/ 2.0 (* 1.0 (+ t 1))))
  (/ (exp 2.0) (exp (/ 2.0 (* 1.0 (+ t 1)))))
  (log (- 2.0 (/ 2.0 (* 1.0 (+ t 1)))))
  (exp (- 2.0 (/ 2.0 (* 1.0 (+ t 1)))))
  (* (cbrt (- 2.0 (/ 2.0 (* 1.0 (+ t 1))))) (cbrt (- 2.0 (/ 2.0 (* 1.0 (+ t 1))))))
  (cbrt (- 2.0 (/ 2.0 (* 1.0 (+ t 1)))))
  (* (* (- 2.0 (/ 2.0 (* 1.0 (+ t 1)))) (- 2.0 (/ 2.0 (* 1.0 (+ t 1))))) (- 2.0 (/ 2.0 (* 1.0 (+ t 1)))))
  (sqrt (- 2.0 (/ 2.0 (* 1.0 (+ t 1)))))
  (sqrt (- 2.0 (/ 2.0 (* 1.0 (+ t 1)))))
  (- (pow 2.0 3) (pow (/ 2.0 (* 1.0 (+ t 1))) 3))
  (+ (* 2.0 2.0) (+ (* (/ 2.0 (* 1.0 (+ t 1))) (/ 2.0 (* 1.0 (+ t 1)))) (* 2.0 (/ 2.0 (* 1.0 (+ t 1))))))
  (neg (/ 2.0 (* 1.0 (+ t 1))))
  (- (* 2.0 2.0) (* (/ 2.0 (* 1.0 (+ t 1))) (/ 2.0 (* 1.0 (+ t 1)))))
  (+ 2.0 (/ 2.0 (* 1.0 (+ t 1))))
  (+ (sqrt 2.0) (sqrt (/ 2.0 (* 1.0 (+ t 1)))))
  (- (sqrt 2.0) (sqrt (/ 2.0 (* 1.0 (+ t 1)))))
  (- 2.0 (/ 2.0 (* 1.0 (+ t 1))))
  (neg (/ 2.0 (* 1.0 (+ t 1))))
  (- (+ (* 2.0 t) (* 2.0 (pow t 3))) (* 2.0 (pow t 2)))
  (- (+ (* 2.0 (/ 1 (pow t 2))) 2.0) (* 2.0 (/ 1 t)))
  (- (+ (* 2.0 (/ 1 (pow t 2))) 2.0) (* 2.0 (/ 1 t)))
  (- (+ (* 2.0 t) (* 2.0 (pow t 3))) (* 2.0 (pow t 2)))
  (- (+ (* 2.0 (/ 1 (pow t 2))) 2.0) (* 2.0 (/ 1 t)))
  (- (+ (* 2.0 (/ 1 (pow t 2))) 2.0) (* 2.0 (/ 1 t)))
  (- (+ (* 2.0 t) (* 2.0 (pow t 3))) (* 2.0 (pow t 2)))
  (- (+ (* 2.0 (/ 1 (pow t 2))) 2.0) (* 2.0 (/ 1 t)))
  (- (+ (* 2.0 (/ 1 (pow t 2))) 2.0) (* 2.0 (/ 1 t)))
  (- (+ (* 2.0 t) (* 2.0 (pow t 3))) (* 2.0 (pow t 2)))
  (- (+ (* 2.0 (/ 1 (pow t 2))) 2.0) (* 2.0 (/ 1 t)))
  (- (+ (* 2.0 (/ 1 (pow t 2))) 2.0) (* 2.0 (/ 1 t)))
2.775 * * [simplify]: iteration  0 :  10  enodes  (cost  11 )
2.776 * * [simplify]: iteration  1 :  24  enodes  (cost  10 )
2.779 * * [simplify]: iteration  2 :  29  enodes  (cost  10 )
2.782 * * [simplify]: iteration  3 :  38  enodes  (cost  10 )
2.787 * * [simplify]: iteration  4 :  44  enodes  (cost  10 )
2.791 * * [simplify]: iteration  5 :  48  enodes  (cost  10 )
2.796 * * [simplify]: iteration  6 :  52  enodes  (cost  10 )
2.802 * * [simplify]: iteration  7 :  68  enodes  (cost  10 )
2.810 * * [simplify]: iteration  8 :  71  enodes  (cost  10 )
2.818 * * [simplify]: iteration  9 :  76  enodes  (cost  10 )
2.829 * * [simplify]: iteration  10 :  83  enodes  (cost  10 )
2.839 * * [simplify]: iteration  11 :  102  enodes  (cost  10 )
2.852 * * [simplify]: iteration  12 :  123  enodes  (cost  10 )
2.868 * * [simplify]: iteration  13 :  136  enodes  (cost  10 )
2.887 * * [simplify]: iteration  14 :  141  enodes  (cost  10 )
2.903 * * [simplify]: iteration  15 :  143  enodes  (cost  10 )
2.919 * * [simplify]: iteration  done :  143  enodes  (cost  10 )
2.919 * * [simplify]: iteration  0 :  9  enodes  (cost  10 )
2.920 * * [simplify]: iteration  1 :  23  enodes  (cost  10 )
2.923 * * [simplify]: iteration  2 :  31  enodes  (cost  10 )
2.927 * * [simplify]: iteration  3 :  37  enodes  (cost  10 )
2.931 * * [simplify]: iteration  done :  37  enodes  (cost  10 )
2.931 * * [simplify]: iteration  0 :  9  enodes  (cost  10 )
2.933 * * [simplify]: iteration  1 :  26  enodes  (cost  10 )
2.939 * * [simplify]: iteration  2 :  36  enodes  (cost  10 )
2.943 * * [simplify]: iteration  3 :  44  enodes  (cost  10 )
2.947 * * [simplify]: iteration  4 :  48  enodes  (cost  10 )
2.952 * * [simplify]: iteration  5 :  52  enodes  (cost  10 )
2.958 * * [simplify]: iteration  6 :  68  enodes  (cost  10 )
2.966 * * [simplify]: iteration  7 :  73  enodes  (cost  10 )
2.973 * * [simplify]: iteration  8 :  78  enodes  (cost  10 )
2.982 * * [simplify]: iteration  9 :  85  enodes  (cost  10 )
2.994 * * [simplify]: iteration  10 :  103  enodes  (cost  10 )
3.007 * * [simplify]: iteration  11 :  124  enodes  (cost  10 )
3.023 * * [simplify]: iteration  12 :  140  enodes  (cost  10 )
3.040 * * [simplify]: iteration  13 :  145  enodes  (cost  10 )
3.058 * * [simplify]: iteration  done :  145  enodes  (cost  10 )
3.059 * * [simplify]: iteration  0 :  10  enodes  (cost  21 )
3.060 * * [simplify]: iteration  1 :  24  enodes  (cost  21 )
3.063 * * [simplify]: iteration  2 :  32  enodes  (cost  21 )
3.067 * * [simplify]: iteration  3 :  38  enodes  (cost  21 )
3.070 * * [simplify]: iteration  done :  38  enodes  (cost  21 )
3.071 * * [simplify]: iteration  0 :  9  enodes  (cost  10 )
3.072 * * [simplify]: iteration  1 :  23  enodes  (cost  10 )
3.075 * * [simplify]: iteration  2 :  31  enodes  (cost  10 )
3.078 * * [simplify]: iteration  3 :  37  enodes  (cost  10 )
3.082 * * [simplify]: iteration  done :  37  enodes  (cost  10 )
3.083 * * [simplify]: iteration  0 :  10  enodes  (cost  29 )
3.084 * * [simplify]: iteration  1 :  25  enodes  (cost  29 )
3.088 * * [simplify]: iteration  2 :  47  enodes  (cost  11 )
3.095 * * [simplify]: iteration  3 :  112  enodes  (cost  11 )
3.127 * * [simplify]: iteration  4 :  399  enodes  (cost  11 )
3.338 * * [simplify]: iteration  5 :  1574  enodes  (cost  11 )
4.742 * * [simplify]: iteration  done :  5000  enodes  (cost  11 )
4.742 * * [simplify]: iteration  0 :  9  enodes  (cost  10 )
4.744 * * [simplify]: iteration  1 :  23  enodes  (cost  10 )
4.747 * * [simplify]: iteration  2 :  31  enodes  (cost  10 )
4.750 * * [simplify]: iteration  3 :  37  enodes  (cost  10 )
4.753 * * [simplify]: iteration  done :  37  enodes  (cost  10 )
4.754 * * [simplify]: iteration  0 :  9  enodes  (cost  10 )
4.760 * * [simplify]: iteration  1 :  23  enodes  (cost  10 )
4.763 * * [simplify]: iteration  2 :  31  enodes  (cost  10 )
4.766 * * [simplify]: iteration  3 :  37  enodes  (cost  10 )
4.770 * * [simplify]: iteration  done :  37  enodes  (cost  10 )
4.770 * * [simplify]: iteration  0 :  11  enodes  (cost  13 )
4.772 * * [simplify]: iteration  1 :  40  enodes  (cost  13 )
4.779 * * [simplify]: iteration  2 :  100  enodes  (cost  13 )
4.804 * * [simplify]: iteration  3 :  406  enodes  (cost  13 )
5.109 * * [simplify]: iteration  4 :  2479  enodes  (cost  13 )
6.505 * * [simplify]: iteration  done :  5000  enodes  (cost  13 )
6.506 * * [simplify]: iteration  0 :  12  enodes  (cost  29 )
6.508 * * [simplify]: iteration  1 :  33  enodes  (cost  21 )
6.514 * * [simplify]: iteration  2 :  79  enodes  (cost  21 )
6.531 * * [simplify]: iteration  3 :  210  enodes  (cost  21 )
6.604 * * [simplify]: iteration  4 :  451  enodes  (cost  21 )
6.767 * * [simplify]: iteration  5 :  694  enodes  (cost  21 )
7.124 * * [simplify]: iteration  6 :  1229  enodes  (cost  19 )
7.960 * * [simplify]: iteration  7 :  1893  enodes  (cost  19 )
9.158 * * [simplify]: iteration  8 :  2673  enodes  (cost  19 )
10.941 * * [simplify]: iteration  9 :  3249  enodes  (cost  19 )
12.516 * * [simplify]: iteration  10 :  3520  enodes  (cost  19 )
13.977 * * [simplify]: iteration  11 :  3535  enodes  (cost  19 )
15.442 * * [simplify]: iteration  12 :  3539  enodes  (cost  19 )
16.900 * * [simplify]: iteration  done :  3539  enodes  (cost  19 )
16.901 * * [simplify]: iteration  0 :  8  enodes  (cost  8 )
16.902 * * [simplify]: iteration  1 :  22  enodes  (cost  8 )
16.905 * * [simplify]: iteration  2 :  31  enodes  (cost  8 )
16.908 * * [simplify]: iteration  3 :  33  enodes  (cost  8 )
16.911 * * [simplify]: iteration  done :  33  enodes  (cost  8 )
16.912 * * [simplify]: iteration  0 :  10  enodes  (cost  19 )
16.913 * * [simplify]: iteration  1 :  31  enodes  (cost  19 )
16.918 * * [simplify]: iteration  2 :  66  enodes  (cost  19 )
16.931 * * [simplify]: iteration  3 :  198  enodes  (cost  19 )
16.998 * * [simplify]: iteration  4 :  531  enodes  (cost  17 )
17.254 * * [simplify]: iteration  5 :  1089  enodes  (cost  17 )
18.000 * * [simplify]: iteration  6 :  2262  enodes  (cost  17 )
20.201 * * [simplify]: iteration  7 :  4071  enodes  (cost  17 )
21.363 * * [simplify]: iteration  done :  5001  enodes  (cost  17 )
21.364 * * [simplify]: iteration  0 :  8  enodes  (cost  9 )
21.369 * * [simplify]: iteration  1 :  21  enodes  (cost  9 )
21.372 * * [simplify]: iteration  2 :  24  enodes  (cost  9 )
21.374 * * [simplify]: iteration  done :  24  enodes  (cost  9 )
21.375 * * [simplify]: iteration  0 :  10  enodes  (cost  11 )
21.376 * * [simplify]: iteration  1 :  23  enodes  (cost  11 )
21.379 * * [simplify]: iteration  2 :  26  enodes  (cost  11 )
21.382 * * [simplify]: iteration  done :  26  enodes  (cost  11 )
21.382 * * [simplify]: iteration  0 :  10  enodes  (cost  11 )
21.383 * * [simplify]: iteration  1 :  24  enodes  (cost  11 )
21.386 * * [simplify]: iteration  2 :  28  enodes  (cost  11 )
21.389 * * [simplify]: iteration  done :  28  enodes  (cost  11 )
21.390 * * [simplify]: iteration  0 :  8  enodes  (cost  9 )
21.391 * * [simplify]: iteration  1 :  22  enodes  (cost  9 )
21.394 * * [simplify]: iteration  2 :  30  enodes  (cost  9 )
21.397 * * [simplify]: iteration  3 :  36  enodes  (cost  9 )
21.400 * * [simplify]: iteration  done :  36  enodes  (cost  9 )
21.401 * * [simplify]: iteration  0 :  8  enodes  (cost  8 )
21.402 * * [simplify]: iteration  1 :  22  enodes  (cost  8 )
21.405 * * [simplify]: iteration  2 :  31  enodes  (cost  8 )
21.408 * * [simplify]: iteration  3 :  33  enodes  (cost  8 )
21.411 * * [simplify]: iteration  done :  33  enodes  (cost  8 )
21.412 * * [simplify]: iteration  0 :  10  enodes  (cost  11 )
21.413 * * [simplify]: iteration  1 :  24  enodes  (cost  10 )
21.416 * * [simplify]: iteration  2 :  29  enodes  (cost  10 )
21.419 * * [simplify]: iteration  3 :  38  enodes  (cost  10 )
21.423 * * [simplify]: iteration  4 :  44  enodes  (cost  10 )
21.430 * * [simplify]: iteration  5 :  48  enodes  (cost  10 )
21.436 * * [simplify]: iteration  6 :  52  enodes  (cost  10 )
21.442 * * [simplify]: iteration  7 :  68  enodes  (cost  10 )
21.450 * * [simplify]: iteration  8 :  71  enodes  (cost  10 )
21.457 * * [simplify]: iteration  9 :  76  enodes  (cost  10 )
21.466 * * [simplify]: iteration  10 :  83  enodes  (cost  10 )
21.476 * * [simplify]: iteration  11 :  102  enodes  (cost  10 )
21.491 * * [simplify]: iteration  12 :  123  enodes  (cost  10 )
21.508 * * [simplify]: iteration  13 :  136  enodes  (cost  10 )
21.524 * * [simplify]: iteration  14 :  141  enodes  (cost  10 )
21.540 * * [simplify]: iteration  15 :  143  enodes  (cost  10 )
21.559 * * [simplify]: iteration  done :  143  enodes  (cost  10 )
21.560 * * [simplify]: iteration  0 :  9  enodes  (cost  10 )
21.561 * * [simplify]: iteration  1 :  23  enodes  (cost  10 )
21.564 * * [simplify]: iteration  2 :  31  enodes  (cost  10 )
21.567 * * [simplify]: iteration  3 :  37  enodes  (cost  10 )
21.570 * * [simplify]: iteration  done :  37  enodes  (cost  10 )
21.571 * * [simplify]: iteration  0 :  9  enodes  (cost  10 )
21.572 * * [simplify]: iteration  1 :  26  enodes  (cost  10 )
21.575 * * [simplify]: iteration  2 :  36  enodes  (cost  10 )
21.579 * * [simplify]: iteration  3 :  44  enodes  (cost  10 )
21.584 * * [simplify]: iteration  4 :  48  enodes  (cost  10 )
21.589 * * [simplify]: iteration  5 :  52  enodes  (cost  10 )
21.594 * * [simplify]: iteration  6 :  68  enodes  (cost  10 )
21.606 * * [simplify]: iteration  7 :  73  enodes  (cost  10 )
21.614 * * [simplify]: iteration  8 :  78  enodes  (cost  10 )
21.622 * * [simplify]: iteration  9 :  85  enodes  (cost  10 )
21.632 * * [simplify]: iteration  10 :  103  enodes  (cost  10 )
21.644 * * [simplify]: iteration  11 :  124  enodes  (cost  10 )
21.664 * * [simplify]: iteration  12 :  140  enodes  (cost  10 )
21.681 * * [simplify]: iteration  13 :  145  enodes  (cost  10 )
21.696 * * [simplify]: iteration  done :  145  enodes  (cost  10 )
21.697 * * [simplify]: iteration  0 :  10  enodes  (cost  21 )
21.698 * * [simplify]: iteration  1 :  24  enodes  (cost  21 )
21.701 * * [simplify]: iteration  2 :  32  enodes  (cost  21 )
21.705 * * [simplify]: iteration  3 :  38  enodes  (cost  21 )
21.709 * * [simplify]: iteration  done :  38  enodes  (cost  21 )
21.710 * * [simplify]: iteration  0 :  9  enodes  (cost  10 )
21.711 * * [simplify]: iteration  1 :  23  enodes  (cost  10 )
21.714 * * [simplify]: iteration  2 :  31  enodes  (cost  10 )
21.717 * * [simplify]: iteration  3 :  37  enodes  (cost  10 )
21.724 * * [simplify]: iteration  done :  37  enodes  (cost  10 )
21.725 * * [simplify]: iteration  0 :  10  enodes  (cost  29 )
21.726 * * [simplify]: iteration  1 :  25  enodes  (cost  29 )
21.730 * * [simplify]: iteration  2 :  47  enodes  (cost  11 )
21.736 * * [simplify]: iteration  3 :  112  enodes  (cost  11 )
21.766 * * [simplify]: iteration  4 :  399  enodes  (cost  11 )
21.980 * * [simplify]: iteration  5 :  1574  enodes  (cost  11 )
23.397 * * [simplify]: iteration  done :  5000  enodes  (cost  11 )
23.397 * * [simplify]: iteration  0 :  9  enodes  (cost  10 )
23.398 * * [simplify]: iteration  1 :  23  enodes  (cost  10 )
23.401 * * [simplify]: iteration  2 :  31  enodes  (cost  10 )
23.404 * * [simplify]: iteration  3 :  37  enodes  (cost  10 )
23.408 * * [simplify]: iteration  done :  37  enodes  (cost  10 )
23.408 * * [simplify]: iteration  0 :  9  enodes  (cost  10 )
23.409 * * [simplify]: iteration  1 :  23  enodes  (cost  10 )
23.413 * * [simplify]: iteration  2 :  31  enodes  (cost  10 )
23.416 * * [simplify]: iteration  3 :  37  enodes  (cost  10 )
23.419 * * [simplify]: iteration  done :  37  enodes  (cost  10 )
23.420 * * [simplify]: iteration  0 :  11  enodes  (cost  13 )
23.421 * * [simplify]: iteration  1 :  40  enodes  (cost  13 )
23.428 * * [simplify]: iteration  2 :  100  enodes  (cost  13 )
23.458 * * [simplify]: iteration  3 :  406  enodes  (cost  13 )
23.766 * * [simplify]: iteration  4 :  2479  enodes  (cost  13 )
25.179 * * [simplify]: iteration  done :  5000  enodes  (cost  13 )
25.179 * * [simplify]: iteration  0 :  12  enodes  (cost  29 )
25.187 * * [simplify]: iteration  1 :  33  enodes  (cost  21 )
25.193 * * [simplify]: iteration  2 :  79  enodes  (cost  21 )
25.210 * * [simplify]: iteration  3 :  210  enodes  (cost  21 )
25.279 * * [simplify]: iteration  4 :  451  enodes  (cost  21 )
25.444 * * [simplify]: iteration  5 :  694  enodes  (cost  21 )
25.810 * * [simplify]: iteration  6 :  1229  enodes  (cost  19 )
26.649 * * [simplify]: iteration  7 :  1893  enodes  (cost  19 )
27.896 * * [simplify]: iteration  8 :  2673  enodes  (cost  19 )
29.680 * * [simplify]: iteration  9 :  3249  enodes  (cost  19 )
31.260 * * [simplify]: iteration  10 :  3520  enodes  (cost  19 )
32.724 * * [simplify]: iteration  11 :  3535  enodes  (cost  19 )
34.195 * * [simplify]: iteration  12 :  3539  enodes  (cost  19 )
35.657 * * [simplify]: iteration  done :  3539  enodes  (cost  19 )
35.658 * * [simplify]: iteration  0 :  8  enodes  (cost  8 )
35.659 * * [simplify]: iteration  1 :  22  enodes  (cost  8 )
35.662 * * [simplify]: iteration  2 :  31  enodes  (cost  8 )
35.665 * * [simplify]: iteration  3 :  33  enodes  (cost  8 )
35.668 * * [simplify]: iteration  done :  33  enodes  (cost  8 )
35.669 * * [simplify]: iteration  0 :  10  enodes  (cost  19 )
35.670 * * [simplify]: iteration  1 :  31  enodes  (cost  19 )
35.675 * * [simplify]: iteration  2 :  66  enodes  (cost  19 )
35.695 * * [simplify]: iteration  3 :  198  enodes  (cost  19 )
35.761 * * [simplify]: iteration  4 :  531  enodes  (cost  17 )
36.018 * * [simplify]: iteration  5 :  1089  enodes  (cost  17 )
36.777 * * [simplify]: iteration  6 :  2262  enodes  (cost  17 )
38.986 * * [simplify]: iteration  7 :  4071  enodes  (cost  17 )
40.178 * * [simplify]: iteration  done :  5001  enodes  (cost  17 )
40.179 * * [simplify]: iteration  0 :  8  enodes  (cost  9 )
40.180 * * [simplify]: iteration  1 :  21  enodes  (cost  9 )
40.183 * * [simplify]: iteration  2 :  24  enodes  (cost  9 )
40.185 * * [simplify]: iteration  done :  24  enodes  (cost  9 )
40.186 * * [simplify]: iteration  0 :  10  enodes  (cost  11 )
40.187 * * [simplify]: iteration  1 :  23  enodes  (cost  11 )
40.190 * * [simplify]: iteration  2 :  26  enodes  (cost  11 )
40.192 * * [simplify]: iteration  done :  26  enodes  (cost  11 )
40.193 * * [simplify]: iteration  0 :  10  enodes  (cost  11 )
40.194 * * [simplify]: iteration  1 :  24  enodes  (cost  11 )
40.198 * * [simplify]: iteration  2 :  28  enodes  (cost  11 )
40.201 * * [simplify]: iteration  done :  28  enodes  (cost  11 )
40.202 * * [simplify]: iteration  0 :  8  enodes  (cost  9 )
40.203 * * [simplify]: iteration  1 :  22  enodes  (cost  9 )
40.206 * * [simplify]: iteration  2 :  30  enodes  (cost  9 )
40.209 * * [simplify]: iteration  3 :  36  enodes  (cost  9 )
40.217 * * [simplify]: iteration  done :  36  enodes  (cost  9 )
40.218 * * [simplify]: iteration  0 :  8  enodes  (cost  8 )
40.219 * * [simplify]: iteration  1 :  22  enodes  (cost  8 )
40.222 * * [simplify]: iteration  2 :  31  enodes  (cost  8 )
40.225 * * [simplify]: iteration  3 :  33  enodes  (cost  8 )
40.228 * * [simplify]: iteration  done :  33  enodes  (cost  8 )
40.228 * * [simplify]: iteration  0 :  10  enodes  (cost  11 )
40.230 * * [simplify]: iteration  1 :  24  enodes  (cost  10 )
40.233 * * [simplify]: iteration  2 :  29  enodes  (cost  10 )
40.236 * * [simplify]: iteration  3 :  38  enodes  (cost  10 )
40.240 * * [simplify]: iteration  4 :  44  enodes  (cost  10 )
40.244 * * [simplify]: iteration  5 :  48  enodes  (cost  10 )
40.249 * * [simplify]: iteration  6 :  52  enodes  (cost  10 )
40.256 * * [simplify]: iteration  7 :  68  enodes  (cost  10 )
40.264 * * [simplify]: iteration  8 :  71  enodes  (cost  10 )
40.275 * * [simplify]: iteration  9 :  76  enodes  (cost  10 )
40.283 * * [simplify]: iteration  10 :  83  enodes  (cost  10 )
40.293 * * [simplify]: iteration  11 :  102  enodes  (cost  10 )
40.306 * * [simplify]: iteration  12 :  123  enodes  (cost  10 )
40.323 * * [simplify]: iteration  13 :  136  enodes  (cost  10 )
40.343 * * [simplify]: iteration  14 :  141  enodes  (cost  10 )
40.359 * * [simplify]: iteration  15 :  143  enodes  (cost  10 )
40.376 * * [simplify]: iteration  done :  143  enodes  (cost  10 )
40.376 * * [simplify]: iteration  0 :  9  enodes  (cost  10 )
40.377 * * [simplify]: iteration  1 :  23  enodes  (cost  10 )
40.380 * * [simplify]: iteration  2 :  31  enodes  (cost  10 )
40.383 * * [simplify]: iteration  3 :  37  enodes  (cost  10 )
40.387 * * [simplify]: iteration  done :  37  enodes  (cost  10 )
40.388 * * [simplify]: iteration  0 :  9  enodes  (cost  10 )
40.392 * * [simplify]: iteration  1 :  26  enodes  (cost  10 )
40.396 * * [simplify]: iteration  2 :  36  enodes  (cost  10 )
40.400 * * [simplify]: iteration  3 :  44  enodes  (cost  10 )
40.405 * * [simplify]: iteration  4 :  48  enodes  (cost  10 )
40.410 * * [simplify]: iteration  5 :  52  enodes  (cost  10 )
40.415 * * [simplify]: iteration  6 :  68  enodes  (cost  10 )
40.423 * * [simplify]: iteration  7 :  73  enodes  (cost  10 )
40.431 * * [simplify]: iteration  8 :  78  enodes  (cost  10 )
40.439 * * [simplify]: iteration  9 :  85  enodes  (cost  10 )
40.453 * * [simplify]: iteration  10 :  103  enodes  (cost  10 )
40.465 * * [simplify]: iteration  11 :  124  enodes  (cost  10 )
40.481 * * [simplify]: iteration  12 :  140  enodes  (cost  10 )
40.499 * * [simplify]: iteration  13 :  145  enodes  (cost  10 )
40.517 * * [simplify]: iteration  done :  145  enodes  (cost  10 )
40.517 * * [simplify]: iteration  0 :  10  enodes  (cost  21 )
40.519 * * [simplify]: iteration  1 :  24  enodes  (cost  21 )
40.522 * * [simplify]: iteration  2 :  32  enodes  (cost  21 )
40.525 * * [simplify]: iteration  3 :  38  enodes  (cost  21 )
40.529 * * [simplify]: iteration  done :  38  enodes  (cost  21 )
40.530 * * [simplify]: iteration  0 :  9  enodes  (cost  10 )
40.531 * * [simplify]: iteration  1 :  23  enodes  (cost  10 )
40.534 * * [simplify]: iteration  2 :  31  enodes  (cost  10 )
40.537 * * [simplify]: iteration  3 :  37  enodes  (cost  10 )
40.540 * * [simplify]: iteration  done :  37  enodes  (cost  10 )
40.541 * * [simplify]: iteration  0 :  10  enodes  (cost  29 )
40.542 * * [simplify]: iteration  1 :  25  enodes  (cost  29 )
40.546 * * [simplify]: iteration  2 :  47  enodes  (cost  11 )
40.554 * * [simplify]: iteration  3 :  112  enodes  (cost  11 )
40.587 * * [simplify]: iteration  4 :  399  enodes  (cost  11 )
40.799 * * [simplify]: iteration  5 :  1574  enodes  (cost  11 )
42.219 * * [simplify]: iteration  done :  5000  enodes  (cost  11 )
42.219 * * [simplify]: iteration  0 :  9  enodes  (cost  10 )
42.220 * * [simplify]: iteration  1 :  23  enodes  (cost  10 )
42.223 * * [simplify]: iteration  2 :  31  enodes  (cost  10 )
42.226 * * [simplify]: iteration  3 :  37  enodes  (cost  10 )
42.235 * * [simplify]: iteration  done :  37  enodes  (cost  10 )
42.236 * * [simplify]: iteration  0 :  9  enodes  (cost  10 )
42.237 * * [simplify]: iteration  1 :  23  enodes  (cost  10 )
42.240 * * [simplify]: iteration  2 :  31  enodes  (cost  10 )
42.243 * * [simplify]: iteration  3 :  37  enodes  (cost  10 )
42.247 * * [simplify]: iteration  done :  37  enodes  (cost  10 )
42.247 * * [simplify]: iteration  0 :  11  enodes  (cost  13 )
42.249 * * [simplify]: iteration  1 :  40  enodes  (cost  13 )
42.255 * * [simplify]: iteration  2 :  100  enodes  (cost  13 )
42.280 * * [simplify]: iteration  3 :  406  enodes  (cost  13 )
42.590 * * [simplify]: iteration  4 :  2479  enodes  (cost  13 )
43.998 * * [simplify]: iteration  done :  5000  enodes  (cost  13 )
43.999 * * [simplify]: iteration  0 :  12  enodes  (cost  29 )
44.001 * * [simplify]: iteration  1 :  33  enodes  (cost  21 )
44.006 * * [simplify]: iteration  2 :  79  enodes  (cost  21 )
44.025 * * [simplify]: iteration  3 :  210  enodes  (cost  21 )
44.097 * * [simplify]: iteration  4 :  451  enodes  (cost  21 )
44.261 * * [simplify]: iteration  5 :  694  enodes  (cost  21 )
44.627 * * [simplify]: iteration  6 :  1229  enodes  (cost  19 )
45.472 * * [simplify]: iteration  7 :  1893  enodes  (cost  19 )
46.505 * * [simplify]: iteration  8 :  2673  enodes  (cost  19 )
48.512 * * [simplify]: iteration  9 :  3249  enodes  (cost  19 )
50.093 * * [simplify]: iteration  10 :  3520  enodes  (cost  19 )
51.560 * * [simplify]: iteration  11 :  3535  enodes  (cost  19 )
53.043 * * [simplify]: iteration  12 :  3539  enodes  (cost  19 )
54.499 * * [simplify]: iteration  done :  3539  enodes  (cost  19 )
54.500 * * [simplify]: iteration  0 :  8  enodes  (cost  8 )
54.501 * * [simplify]: iteration  1 :  22  enodes  (cost  8 )
54.504 * * [simplify]: iteration  2 :  31  enodes  (cost  8 )
54.507 * * [simplify]: iteration  3 :  33  enodes  (cost  8 )
54.510 * * [simplify]: iteration  done :  33  enodes  (cost  8 )
54.511 * * [simplify]: iteration  0 :  10  enodes  (cost  19 )
54.512 * * [simplify]: iteration  1 :  31  enodes  (cost  19 )
54.517 * * [simplify]: iteration  2 :  66  enodes  (cost  19 )
54.530 * * [simplify]: iteration  3 :  198  enodes  (cost  19 )
54.596 * * [simplify]: iteration  4 :  531  enodes  (cost  17 )
54.850 * * [simplify]: iteration  5 :  1089  enodes  (cost  17 )
55.609 * * [simplify]: iteration  6 :  2262  enodes  (cost  17 )
57.813 * * [simplify]: iteration  7 :  4071  enodes  (cost  17 )
58.978 * * [simplify]: iteration  done :  5001  enodes  (cost  17 )
58.979 * * [simplify]: iteration  0 :  8  enodes  (cost  9 )
58.980 * * [simplify]: iteration  1 :  21  enodes  (cost  9 )
58.983 * * [simplify]: iteration  2 :  24  enodes  (cost  9 )
58.985 * * [simplify]: iteration  done :  24  enodes  (cost  9 )
58.985 * * [simplify]: iteration  0 :  10  enodes  (cost  11 )
58.986 * * [simplify]: iteration  1 :  23  enodes  (cost  11 )
58.989 * * [simplify]: iteration  2 :  26  enodes  (cost  11 )
58.992 * * [simplify]: iteration  done :  26  enodes  (cost  11 )
58.993 * * [simplify]: iteration  0 :  10  enodes  (cost  11 )
58.994 * * [simplify]: iteration  1 :  24  enodes  (cost  11 )
58.997 * * [simplify]: iteration  2 :  28  enodes  (cost  11 )
59.000 * * [simplify]: iteration  done :  28  enodes  (cost  11 )
59.001 * * [simplify]: iteration  0 :  8  enodes  (cost  9 )
59.002 * * [simplify]: iteration  1 :  22  enodes  (cost  9 )
59.005 * * [simplify]: iteration  2 :  30  enodes  (cost  9 )
59.008 * * [simplify]: iteration  3 :  36  enodes  (cost  9 )
59.011 * * [simplify]: iteration  done :  36  enodes  (cost  9 )
59.012 * * [simplify]: iteration  0 :  8  enodes  (cost  8 )
59.013 * * [simplify]: iteration  1 :  22  enodes  (cost  8 )
59.016 * * [simplify]: iteration  2 :  31  enodes  (cost  8 )
59.019 * * [simplify]: iteration  3 :  33  enodes  (cost  8 )
59.022 * * [simplify]: iteration  done :  33  enodes  (cost  8 )
59.023 * * [simplify]: iteration  0 :  10  enodes  (cost  11 )
59.024 * * [simplify]: iteration  1 :  24  enodes  (cost  10 )
59.027 * * [simplify]: iteration  2 :  29  enodes  (cost  10 )
59.030 * * [simplify]: iteration  3 :  38  enodes  (cost  10 )
59.037 * * [simplify]: iteration  4 :  44  enodes  (cost  10 )
59.042 * * [simplify]: iteration  5 :  48  enodes  (cost  10 )
59.047 * * [simplify]: iteration  6 :  52  enodes  (cost  10 )
59.053 * * [simplify]: iteration  7 :  68  enodes  (cost  10 )
59.062 * * [simplify]: iteration  8 :  71  enodes  (cost  10 )
59.069 * * [simplify]: iteration  9 :  76  enodes  (cost  10 )
59.077 * * [simplify]: iteration  10 :  83  enodes  (cost  10 )
59.087 * * [simplify]: iteration  11 :  102  enodes  (cost  10 )
59.103 * * [simplify]: iteration  12 :  123  enodes  (cost  10 )
59.120 * * [simplify]: iteration  13 :  136  enodes  (cost  10 )
59.136 * * [simplify]: iteration  14 :  141  enodes  (cost  10 )
59.155 * * [simplify]: iteration  15 :  143  enodes  (cost  10 )
59.171 * * [simplify]: iteration  done :  143  enodes  (cost  10 )
59.172 * * [simplify]: iteration  0 :  9  enodes  (cost  10 )
59.173 * * [simplify]: iteration  1 :  23  enodes  (cost  10 )
59.176 * * [simplify]: iteration  2 :  31  enodes  (cost  10 )
59.179 * * [simplify]: iteration  3 :  37  enodes  (cost  10 )
59.183 * * [simplify]: iteration  done :  37  enodes  (cost  10 )
59.183 * * [simplify]: iteration  0 :  9  enodes  (cost  10 )
59.185 * * [simplify]: iteration  1 :  26  enodes  (cost  10 )
59.188 * * [simplify]: iteration  2 :  36  enodes  (cost  10 )
59.192 * * [simplify]: iteration  3 :  44  enodes  (cost  10 )
59.197 * * [simplify]: iteration  4 :  48  enodes  (cost  10 )
59.202 * * [simplify]: iteration  5 :  52  enodes  (cost  10 )
59.208 * * [simplify]: iteration  6 :  68  enodes  (cost  10 )
59.218 * * [simplify]: iteration  7 :  73  enodes  (cost  10 )
59.226 * * [simplify]: iteration  8 :  78  enodes  (cost  10 )
59.234 * * [simplify]: iteration  9 :  85  enodes  (cost  10 )
59.245 * * [simplify]: iteration  10 :  103  enodes  (cost  10 )
59.257 * * [simplify]: iteration  11 :  124  enodes  (cost  10 )
59.276 * * [simplify]: iteration  12 :  140  enodes  (cost  10 )
59.293 * * [simplify]: iteration  13 :  145  enodes  (cost  10 )
59.309 * * [simplify]: iteration  done :  145  enodes  (cost  10 )
59.310 * * [simplify]: iteration  0 :  10  enodes  (cost  21 )
59.311 * * [simplify]: iteration  1 :  24  enodes  (cost  21 )
59.314 * * [simplify]: iteration  2 :  32  enodes  (cost  21 )
59.317 * * [simplify]: iteration  3 :  38  enodes  (cost  21 )
59.321 * * [simplify]: iteration  done :  38  enodes  (cost  21 )
59.321 * * [simplify]: iteration  0 :  9  enodes  (cost  10 )
59.322 * * [simplify]: iteration  1 :  23  enodes  (cost  10 )
59.329 * * [simplify]: iteration  2 :  31  enodes  (cost  10 )
59.332 * * [simplify]: iteration  3 :  37  enodes  (cost  10 )
59.336 * * [simplify]: iteration  done :  37  enodes  (cost  10 )
59.336 * * [simplify]: iteration  0 :  10  enodes  (cost  29 )
59.338 * * [simplify]: iteration  1 :  25  enodes  (cost  29 )
59.341 * * [simplify]: iteration  2 :  47  enodes  (cost  11 )
59.349 * * [simplify]: iteration  3 :  112  enodes  (cost  11 )
59.377 * * [simplify]: iteration  4 :  399  enodes  (cost  11 )
59.586 * * [simplify]: iteration  5 :  1574  enodes  (cost  11 )
61.011 * * [simplify]: iteration  done :  5000  enodes  (cost  11 )
61.012 * * [simplify]: iteration  0 :  9  enodes  (cost  10 )
61.013 * * [simplify]: iteration  1 :  23  enodes  (cost  10 )
61.016 * * [simplify]: iteration  2 :  31  enodes  (cost  10 )
61.019 * * [simplify]: iteration  3 :  37  enodes  (cost  10 )
61.023 * * [simplify]: iteration  done :  37  enodes  (cost  10 )
61.023 * * [simplify]: iteration  0 :  9  enodes  (cost  10 )
61.024 * * [simplify]: iteration  1 :  23  enodes  (cost  10 )
61.027 * * [simplify]: iteration  2 :  31  enodes  (cost  10 )
61.030 * * [simplify]: iteration  3 :  37  enodes  (cost  10 )
61.034 * * [simplify]: iteration  done :  37  enodes  (cost  10 )
61.034 * * [simplify]: iteration  0 :  11  enodes  (cost  13 )
61.036 * * [simplify]: iteration  1 :  40  enodes  (cost  13 )
61.043 * * [simplify]: iteration  2 :  100  enodes  (cost  13 )
61.072 * * [simplify]: iteration  3 :  406  enodes  (cost  13 )
61.380 * * [simplify]: iteration  4 :  2479  enodes  (cost  13 )
62.791 * * [simplify]: iteration  done :  5000  enodes  (cost  13 )
62.791 * * [simplify]: iteration  0 :  12  enodes  (cost  29 )
62.793 * * [simplify]: iteration  1 :  33  enodes  (cost  21 )
62.799 * * [simplify]: iteration  2 :  79  enodes  (cost  21 )
62.816 * * [simplify]: iteration  3 :  210  enodes  (cost  21 )
62.884 * * [simplify]: iteration  4 :  451  enodes  (cost  21 )
63.046 * * [simplify]: iteration  5 :  694  enodes  (cost  21 )
63.412 * * [simplify]: iteration  6 :  1229  enodes  (cost  19 )
64.254 * * [simplify]: iteration  7 :  1893  enodes  (cost  19 )
65.280 * * [simplify]: iteration  8 :  2673  enodes  (cost  19 )
67.067 * * [simplify]: iteration  9 :  3249  enodes  (cost  19 )
68.854 * * [simplify]: iteration  10 :  3520  enodes  (cost  19 )
70.307 * * [simplify]: iteration  11 :  3535  enodes  (cost  19 )
71.755 * * [simplify]: iteration  12 :  3539  enodes  (cost  19 )
73.200 * * [simplify]: iteration  done :  3539  enodes  (cost  19 )
73.201 * * [simplify]: iteration  0 :  8  enodes  (cost  8 )
73.202 * * [simplify]: iteration  1 :  22  enodes  (cost  8 )
73.205 * * [simplify]: iteration  2 :  31  enodes  (cost  8 )
73.208 * * [simplify]: iteration  3 :  33  enodes  (cost  8 )
73.211 * * [simplify]: iteration  done :  33  enodes  (cost  8 )
73.212 * * [simplify]: iteration  0 :  10  enodes  (cost  19 )
73.213 * * [simplify]: iteration  1 :  31  enodes  (cost  19 )
73.218 * * [simplify]: iteration  2 :  66  enodes  (cost  19 )
73.236 * * [simplify]: iteration  3 :  198  enodes  (cost  19 )
73.303 * * [simplify]: iteration  4 :  531  enodes  (cost  17 )
73.563 * * [simplify]: iteration  5 :  1089  enodes  (cost  17 )
74.308 * * [simplify]: iteration  6 :  2262  enodes  (cost  17 )
76.514 * * [simplify]: iteration  7 :  4071  enodes  (cost  17 )
77.672 * * [simplify]: iteration  done :  5001  enodes  (cost  17 )
77.672 * * [simplify]: iteration  0 :  8  enodes  (cost  9 )
77.673 * * [simplify]: iteration  1 :  21  enodes  (cost  9 )
77.676 * * [simplify]: iteration  2 :  24  enodes  (cost  9 )
77.678 * * [simplify]: iteration  done :  24  enodes  (cost  9 )
77.679 * * [simplify]: iteration  0 :  10  enodes  (cost  11 )
77.680 * * [simplify]: iteration  1 :  23  enodes  (cost  11 )
77.683 * * [simplify]: iteration  2 :  26  enodes  (cost  11 )
77.685 * * [simplify]: iteration  done :  26  enodes  (cost  11 )
77.686 * * [simplify]: iteration  0 :  10  enodes  (cost  11 )
77.687 * * [simplify]: iteration  1 :  24  enodes  (cost  11 )
77.690 * * [simplify]: iteration  2 :  28  enodes  (cost  11 )
77.698 * * [simplify]: iteration  done :  28  enodes  (cost  11 )
77.699 * * [simplify]: iteration  0 :  8  enodes  (cost  9 )
77.701 * * [simplify]: iteration  1 :  22  enodes  (cost  9 )
77.704 * * [simplify]: iteration  2 :  30  enodes  (cost  9 )
77.707 * * [simplify]: iteration  3 :  36  enodes  (cost  9 )
77.711 * * [simplify]: iteration  done :  36  enodes  (cost  9 )
77.711 * * [simplify]: iteration  0 :  8  enodes  (cost  8 )
77.712 * * [simplify]: iteration  1 :  22  enodes  (cost  8 )
77.715 * * [simplify]: iteration  2 :  31  enodes  (cost  8 )
77.718 * * [simplify]: iteration  3 :  33  enodes  (cost  8 )
77.721 * * [simplify]: iteration  done :  33  enodes  (cost  8 )
77.722 * * [simplify]: iteration  0 :  11  enodes  (cost  15 )
77.724 * * [simplify]: iteration  1 :  32  enodes  (cost  13 )
77.731 * * [simplify]: iteration  2 :  87  enodes  (cost  11 )
77.745 * * [simplify]: iteration  3 :  163  enodes  (cost  11 )
77.785 * * [simplify]: iteration  4 :  314  enodes  (cost  11 )
77.904 * * [simplify]: iteration  5 :  595  enodes  (cost  11 )
78.207 * * [simplify]: iteration  6 :  1447  enodes  (cost  11 )
80.104 * * [simplify]: iteration  done :  5000  enodes  (cost  11 )
80.104 * * [simplify]: iteration  0 :  11  enodes  (cost  15 )
80.106 * * [simplify]: iteration  1 :  27  enodes  (cost  15 )
80.111 * * [simplify]: iteration  2 :  63  enodes  (cost  11 )
80.122 * * [simplify]: iteration  3 :  134  enodes  (cost  11 )
80.159 * * [simplify]: iteration  4 :  281  enodes  (cost  11 )
80.276 * * [simplify]: iteration  5 :  781  enodes  (cost  9 )
82.330 * * [simplify]: iteration  6 :  4009  enodes  (cost  9 )
83.803 * * [simplify]: iteration  done :  5000  enodes  (cost  9 )
83.804 * * [simplify]: iteration  0 :  11  enodes  (cost  15 )
83.809 * * [simplify]: iteration  1 :  27  enodes  (cost  15 )
83.814 * * [simplify]: iteration  2 :  63  enodes  (cost  11 )
83.825 * * [simplify]: iteration  3 :  134  enodes  (cost  11 )
83.859 * * [simplify]: iteration  4 :  281  enodes  (cost  11 )
83.980 * * [simplify]: iteration  5 :  781  enodes  (cost  9 )
86.030 * * [simplify]: iteration  6 :  4009  enodes  (cost  9 )
87.737 * * [simplify]: iteration  done :  5000  enodes  (cost  9 )
87.737 * * [simplify]: iteration  0 :  11  enodes  (cost  15 )
87.739 * * [simplify]: iteration  1 :  32  enodes  (cost  13 )
87.746 * * [simplify]: iteration  2 :  87  enodes  (cost  11 )
87.765 * * [simplify]: iteration  3 :  163  enodes  (cost  11 )
87.802 * * [simplify]: iteration  4 :  314  enodes  (cost  11 )
87.921 * * [simplify]: iteration  5 :  595  enodes  (cost  11 )
88.232 * * [simplify]: iteration  6 :  1447  enodes  (cost  11 )
90.144 * * [simplify]: iteration  done :  5000  enodes  (cost  11 )
90.144 * * [simplify]: iteration  0 :  11  enodes  (cost  15 )
90.146 * * [simplify]: iteration  1 :  27  enodes  (cost  15 )
90.151 * * [simplify]: iteration  2 :  63  enodes  (cost  11 )
90.162 * * [simplify]: iteration  3 :  134  enodes  (cost  11 )
90.201 * * [simplify]: iteration  4 :  281  enodes  (cost  11 )
90.320 * * [simplify]: iteration  5 :  781  enodes  (cost  9 )
92.377 * * [simplify]: iteration  6 :  4009  enodes  (cost  9 )
93.858 * * [simplify]: iteration  done :  5000  enodes  (cost  9 )
93.859 * * [simplify]: iteration  0 :  11  enodes  (cost  15 )
93.861 * * [simplify]: iteration  1 :  27  enodes  (cost  15 )
93.865 * * [simplify]: iteration  2 :  63  enodes  (cost  11 )
93.877 * * [simplify]: iteration  3 :  134  enodes  (cost  11 )
93.915 * * [simplify]: iteration  4 :  281  enodes  (cost  11 )
94.033 * * [simplify]: iteration  5 :  781  enodes  (cost  9 )
96.087 * * [simplify]: iteration  6 :  4009  enodes  (cost  9 )
97.560 * * [simplify]: iteration  done :  5000  enodes  (cost  9 )
97.561 * * [simplify]: iteration  0 :  11  enodes  (cost  15 )
97.563 * * [simplify]: iteration  1 :  32  enodes  (cost  13 )
97.575 * * [simplify]: iteration  2 :  87  enodes  (cost  11 )
97.590 * * [simplify]: iteration  3 :  163  enodes  (cost  11 )
97.632 * * [simplify]: iteration  4 :  314  enodes  (cost  11 )
97.751 * * [simplify]: iteration  5 :  595  enodes  (cost  11 )
98.055 * * [simplify]: iteration  6 :  1447  enodes  (cost  11 )
99.968 * * [simplify]: iteration  done :  5000  enodes  (cost  11 )
99.969 * * [simplify]: iteration  0 :  11  enodes  (cost  15 )
99.970 * * [simplify]: iteration  1 :  27  enodes  (cost  15 )
99.975 * * [simplify]: iteration  2 :  63  enodes  (cost  11 )
99.992 * * [simplify]: iteration  3 :  134  enodes  (cost  11 )
100.026 * * [simplify]: iteration  4 :  281  enodes  (cost  11 )
100.146 * * [simplify]: iteration  5 :  781  enodes  (cost  9 )
102.195 * * [simplify]: iteration  6 :  4009  enodes  (cost  9 )
103.681 * * [simplify]: iteration  done :  5000  enodes  (cost  9 )
103.682 * * [simplify]: iteration  0 :  11  enodes  (cost  15 )
103.684 * * [simplify]: iteration  1 :  27  enodes  (cost  15 )
103.689 * * [simplify]: iteration  2 :  63  enodes  (cost  11 )
103.700 * * [simplify]: iteration  3 :  134  enodes  (cost  11 )
103.741 * * [simplify]: iteration  4 :  281  enodes  (cost  11 )
103.862 * * [simplify]: iteration  5 :  781  enodes  (cost  9 )
106.155 * * [simplify]: iteration  6 :  4009  enodes  (cost  9 )
107.641 * * [simplify]: iteration  done :  5000  enodes  (cost  9 )
107.642 * * [simplify]: iteration  0 :  11  enodes  (cost  15 )
107.644 * * [simplify]: iteration  1 :  32  enodes  (cost  13 )
107.651 * * [simplify]: iteration  2 :  87  enodes  (cost  11 )
107.665 * * [simplify]: iteration  3 :  163  enodes  (cost  11 )
107.706 * * [simplify]: iteration  4 :  314  enodes  (cost  11 )
107.825 * * [simplify]: iteration  5 :  595  enodes  (cost  11 )
108.136 * * [simplify]: iteration  6 :  1447  enodes  (cost  11 )
110.059 * * [simplify]: iteration  done :  5000  enodes  (cost  11 )
110.060 * * [simplify]: iteration  0 :  11  enodes  (cost  15 )
110.062 * * [simplify]: iteration  1 :  27  enodes  (cost  15 )
110.066 * * [simplify]: iteration  2 :  63  enodes  (cost  11 )
110.078 * * [simplify]: iteration  3 :  134  enodes  (cost  11 )
110.114 * * [simplify]: iteration  4 :  281  enodes  (cost  11 )
110.237 * * [simplify]: iteration  5 :  781  enodes  (cost  9 )
112.276 * * [simplify]: iteration  6 :  4009  enodes  (cost  9 )
113.761 * * [simplify]: iteration  done :  5000  enodes  (cost  9 )
113.761 * * [simplify]: iteration  0 :  11  enodes  (cost  15 )
113.763 * * [simplify]: iteration  1 :  27  enodes  (cost  15 )
113.768 * * [simplify]: iteration  2 :  63  enodes  (cost  11 )
113.784 * * [simplify]: iteration  3 :  134  enodes  (cost  11 )
113.820 * * [simplify]: iteration  4 :  281  enodes  (cost  11 )
113.940 * * [simplify]: iteration  5 :  781  enodes  (cost  9 )
116.007 * * [simplify]: iteration  6 :  4009  enodes  (cost  9 )
117.489 * * [simplify]: iteration  done :  5000  enodes  (cost  9 )
117.490 * [simplify]: Simplified to:
   (exp (- 2.0 (/ 2.0 (* 1.0 (+ t 1)))))
  (log (- 2.0 (/ 2.0 (* 1.0 (+ t 1)))))
  (exp (- 2.0 (/ 2.0 (* 1.0 (+ t 1)))))
  (* (cbrt (- 2.0 (/ 2.0 (* 1.0 (+ t 1))))) (cbrt (- 2.0 (/ 2.0 (* 1.0 (+ t 1))))))
  (cbrt (- 2.0 (/ 2.0 (* 1.0 (+ t 1)))))
  (pow (- 2.0 (/ 2.0 (* 1.0 (+ t 1)))) 3)
  (sqrt (- 2.0 (/ 2.0 (* 1.0 (+ t 1)))))
  (sqrt (- 2.0 (/ 2.0 (* 1.0 (+ t 1)))))
  (- (pow 2.0 3) (pow (/ 2.0 (* 1.0 (+ t 1))) 3))
  (* 2.0 (+ 2.0 (/ (+ (/ 2.0 (* 1.0 (+ t 1))) 2.0) (* 1.0 (+ t 1)))))
  (neg (/ 2.0 (* 1.0 (+ t 1))))
  (* 2.0 (- 2.0 (/ (/ 2.0 (* 1.0 (+ t 1))) (* 1.0 (+ t 1)))))
  (+ 2.0 (/ 2.0 (* 1.0 (+ t 1))))
  (+ (sqrt 2.0) (sqrt (/ 2.0 (* 1.0 (+ t 1)))))
  (- (sqrt 2.0) (sqrt (/ 2.0 (* 1.0 (+ t 1)))))
  (- 2.0 (/ 2.0 (* 1.0 (+ t 1))))
  (neg (/ 2.0 (* 1.0 (+ t 1))))
  (exp (- 2.0 (/ 2.0 (* 1.0 (+ t 1)))))
  (log (- 2.0 (/ 2.0 (* 1.0 (+ t 1)))))
  (exp (- 2.0 (/ 2.0 (* 1.0 (+ t 1)))))
  (* (cbrt (- 2.0 (/ 2.0 (* 1.0 (+ t 1))))) (cbrt (- 2.0 (/ 2.0 (* 1.0 (+ t 1))))))
  (cbrt (- 2.0 (/ 2.0 (* 1.0 (+ t 1)))))
  (pow (- 2.0 (/ 2.0 (* 1.0 (+ t 1)))) 3)
  (sqrt (- 2.0 (/ 2.0 (* 1.0 (+ t 1)))))
  (sqrt (- 2.0 (/ 2.0 (* 1.0 (+ t 1)))))
  (- (pow 2.0 3) (pow (/ 2.0 (* 1.0 (+ t 1))) 3))
  (* 2.0 (+ 2.0 (/ (+ (/ 2.0 (* 1.0 (+ t 1))) 2.0) (* 1.0 (+ t 1)))))
  (neg (/ 2.0 (* 1.0 (+ t 1))))
  (* 2.0 (- 2.0 (/ (/ 2.0 (* 1.0 (+ t 1))) (* 1.0 (+ t 1)))))
  (+ 2.0 (/ 2.0 (* 1.0 (+ t 1))))
  (+ (sqrt 2.0) (sqrt (/ 2.0 (* 1.0 (+ t 1)))))
  (- (sqrt 2.0) (sqrt (/ 2.0 (* 1.0 (+ t 1)))))
  (- 2.0 (/ 2.0 (* 1.0 (+ t 1))))
  (neg (/ 2.0 (* 1.0 (+ t 1))))
  (exp (- 2.0 (/ 2.0 (* 1.0 (+ t 1)))))
  (log (- 2.0 (/ 2.0 (* 1.0 (+ t 1)))))
  (exp (- 2.0 (/ 2.0 (* 1.0 (+ t 1)))))
  (* (cbrt (- 2.0 (/ 2.0 (* 1.0 (+ t 1))))) (cbrt (- 2.0 (/ 2.0 (* 1.0 (+ t 1))))))
  (cbrt (- 2.0 (/ 2.0 (* 1.0 (+ t 1)))))
  (pow (- 2.0 (/ 2.0 (* 1.0 (+ t 1)))) 3)
  (sqrt (- 2.0 (/ 2.0 (* 1.0 (+ t 1)))))
  (sqrt (- 2.0 (/ 2.0 (* 1.0 (+ t 1)))))
  (- (pow 2.0 3) (pow (/ 2.0 (* 1.0 (+ t 1))) 3))
  (* 2.0 (+ 2.0 (/ (+ (/ 2.0 (* 1.0 (+ t 1))) 2.0) (* 1.0 (+ t 1)))))
  (neg (/ 2.0 (* 1.0 (+ t 1))))
  (* 2.0 (- 2.0 (/ (/ 2.0 (* 1.0 (+ t 1))) (* 1.0 (+ t 1)))))
  (+ 2.0 (/ 2.0 (* 1.0 (+ t 1))))
  (+ (sqrt 2.0) (sqrt (/ 2.0 (* 1.0 (+ t 1)))))
  (- (sqrt 2.0) (sqrt (/ 2.0 (* 1.0 (+ t 1)))))
  (- 2.0 (/ 2.0 (* 1.0 (+ t 1))))
  (neg (/ 2.0 (* 1.0 (+ t 1))))
  (exp (- 2.0 (/ 2.0 (* 1.0 (+ t 1)))))
  (log (- 2.0 (/ 2.0 (* 1.0 (+ t 1)))))
  (exp (- 2.0 (/ 2.0 (* 1.0 (+ t 1)))))
  (* (cbrt (- 2.0 (/ 2.0 (* 1.0 (+ t 1))))) (cbrt (- 2.0 (/ 2.0 (* 1.0 (+ t 1))))))
  (cbrt (- 2.0 (/ 2.0 (* 1.0 (+ t 1)))))
  (pow (- 2.0 (/ 2.0 (* 1.0 (+ t 1)))) 3)
  (sqrt (- 2.0 (/ 2.0 (* 1.0 (+ t 1)))))
  (sqrt (- 2.0 (/ 2.0 (* 1.0 (+ t 1)))))
  (- (pow 2.0 3) (pow (/ 2.0 (* 1.0 (+ t 1))) 3))
  (* 2.0 (+ 2.0 (/ (+ (/ 2.0 (* 1.0 (+ t 1))) 2.0) (* 1.0 (+ t 1)))))
  (neg (/ 2.0 (* 1.0 (+ t 1))))
  (* 2.0 (- 2.0 (/ (/ 2.0 (* 1.0 (+ t 1))) (* 1.0 (+ t 1)))))
  (+ 2.0 (/ 2.0 (* 1.0 (+ t 1))))
  (+ (sqrt 2.0) (sqrt (/ 2.0 (* 1.0 (+ t 1)))))
  (- (sqrt 2.0) (sqrt (/ 2.0 (* 1.0 (+ t 1)))))
  (- 2.0 (/ 2.0 (* 1.0 (+ t 1))))
  (neg (/ 2.0 (* 1.0 (+ t 1))))
  (* 2.0 (- (+ t (pow t 3)) (pow t 2)))
  (+ 2.0 (/ (- (/ 2.0 t) 2.0) t))
  (+ 2.0 (/ (- (/ 2.0 t) 2.0) t))
  (* 2.0 (- (+ t (pow t 3)) (pow t 2)))
  (+ 2.0 (/ (- (/ 2.0 t) 2.0) t))
  (+ 2.0 (/ (- (/ 2.0 t) 2.0) t))
  (* 2.0 (- (+ t (pow t 3)) (pow t 2)))
  (+ 2.0 (/ (- (/ 2.0 t) 2.0) t))
  (+ 2.0 (/ (- (/ 2.0 t) 2.0) t))
  (* 2.0 (- (+ t (pow t 3)) (pow t 2)))
  (+ 2.0 (/ (- (/ 2.0 t) 2.0) t))
  (+ 2.0 (/ (- (/ 2.0 t) 2.0) t))
117.491 * * * [progress]: adding candidates to table
117.658 * [progress]: [Phase 3 of 3] Extracting.
117.661 * [simplify]: Simplifying using  #<procedure:simplify-batch-regraph> :
   (/ (+ (* (- 2.0 (/ 2.0 (* 1.0 (+ t 1)))) (- 2.0 (/ 2.0 (* 1.0 (+ t 1))))) 1.0) (+ 2.0 (* (- 2.0 (/ 2.0 (* 1.0 (+ t 1)))) (- 2.0 (/ 2.0 (* 1.0 (+ t 1)))))))
117.662 * * [simplify]: iteration  0 :  12  enodes  (cost  43 )
117.662 * * [simplify]: iteration  1 :  18  enodes  (cost  43 )
117.663 * * [simplify]: iteration  done :  18  enodes  (cost  43 )
117.663 * [simplify]: Simplified to:
   (/ (+ (* (- 2.0 (/ 2.0 (* 1.0 (+ t 1)))) (- 2.0 (/ 2.0 (* 1.0 (+ t 1))))) 1.0) (+ 2.0 (* (- 2.0 (/ 2.0 (* 1.0 (+ t 1)))) (- 2.0 (/ 2.0 (* 1.0 (+ t 1)))))))
119.205 * [regime-testing]: End program error score: 0.01050131266408301