(>= (f60 (var x21)) (var x21))
(>=
 (f1 (var x21) (f61))
 (+ (f60 (var x21)) 1))
(>= (f62 (var x2)) (var x2))
(>= (f63 (var x1)) (var x1))
(>=
 (f5 (var x1) (var x2))
 (f3
  (f61)
  (f63 (var x1))
  (f62 (var x2))))
(>=
 (f4 (var x1) (var x2))
 (f2
  (f61)
  (f63 (var x1))
  (f62 (var x2))))
(>= (f64 (var x35)) (var x35))
(>=
 (f1 (var x35) (f65 (var x3)))
 (f1 (f64 (var x35)) (var x3)))
(>= (f66 (var x7)) (var x7))
(>= (f67 (var x4)) (var x4))
(>=
 (f68
  (var x3)
  (var x4)
  (var x7)
  (var x35))
 (f3
  (f65 (var x3))
  (f67 (var x4))
  (f66 (var x7))))
(>=
 (f69
  (var x3)
  (var x4)
  (var x7)
  (var x8)
  (var x35)
  (var x48))
 (f2
  (f65 (var x3))
  (f67 (var x4))
  (f66 (var x7))))
(>= (f70 (var x48)) (var x48))
(>=
 (f1 (var x48) (f71 (var x3)))
 (f1 (f70 (var x48)) (var x3)))
(>= (f72 (var x8)) (var x8))
(>= (f73 (var x4)) (var x4))
(>=
 (f74
  (var x3)
  (var x4)
  (var x8)
  (var x48))
 (f3
  (f71 (var x3))
  (f73 (var x4))
  (f72 (var x8))))
(>=
 (f69
  (var x3)
  (var x4)
  (var x7)
  (var x8)
  (var x35)
  (var x48))
 (f2
  (f71 (var x3))
  (f73 (var x4))
  (f72 (var x8))))
(>=
 (f3
  (var x3)
  (var x4)
  (+ (+ (var x7) (var x8)) 1))
 (+
  (+
   (f68
    (var x3)
    (var x4)
    (var x7)
    (var x35))
   (f74
    (var x3)
    (var x4)
    (var x8)
    (var x48)))
  1))
(>=
 (f2
  (var x3)
  (var x4)
  (+ (+ (var x7) (var x8)) 1))
 (f69
  (var x3)
  (var x4)
  (var x7)
  (var x8)
  (var x35)
  (var x48)))
(>= (f75 (var x11)) (var x11))
(>=
 (f76 (var x10) (var x11))
 (f1 (f75 (var x11)) (var x10)))
(>=
 (f3 (var x10) (var x11) 0)
 0)
(>=
 (f2 (var x10) (var x11) 0)
 (f76 (var x10) (var x11)))