(>= (f65 (var x2)) (var x2))
(>= (f66) 0)
(>=
 (f5 (var x2))
 (f6 (f65 (var x2)) (f66)))
(>= (f67 (var x34)) (var x34))
(>= (f68 (var x35)) (var x35))
(>=
 (f1 (var x34) (var x35) (f69))
 (f6
  (f67 (var x34))
  (f68 (var x35))))
(>= (f70 (var x7)) (var x7))
(>= (f71 (var x43)) (var x43))
(>=
 (f2 (var x43) (f72))
 (+ (f71 (var x43)) 1))
(>= (f73 (var x5)) (var x5))
(>=
 (f6 (+ (var x7) 1) (var x5))
 (f3
  (f69)
  (f70 (var x7))
  (f72)
  (f73 (var x5))))
(>= (f74 (var x10)) (var x10))
(>=
 (f6 0 (var x10))
 (f4 (f74 (var x10))))
(>= (f4 (var x13)) (var x13))
(>= (f75 (var x16)) (var x16))
(>= (f76 (var x18)) (var x18))
(>=
 (f77 (var x17) (var x18))
 (f2 (f76 (var x18)) (var x17)))
(>=
 (f3
  (var x15)
  (var x16)
  (var x17)
  (var x18))
 (f1
  (f75 (var x16))
  (f77 (var x17) (var x18))
  (var x15)))