(>= (f82 (var x38)) (var x38))
(>=
 (f1 (var x38) (f83))
 (+ (f82 (var x38)) 1))
(>= (f84 (var x2)) (var x2))
(>= (f85) 0)
(>=
 (f86 (var x2) (var x38))
 (f2
  (f83)
  (f84 (var x2))
  (f85)))
(>= (f87) 0)
(>=
 (f3 (var x2))
 (f4
  (f86 (var x2) (var x38))
  (f87)))
(>= (f88 (var x51)) (var x51))
(>=
 (f1 (var x51) (f89 (var x4)))
 (f1 (f88 (var x51)) (var x4)))
(>= (f90 (var x9)) (var x9))
(>= (f91 (var x63)) (var x63))
(>=
 (f1 (var x63) (f92 (var x4)))
 (f1 (f91 (var x63)) (var x4)))
(>= (f93 (var x8)) (var x8))
(>= (f94 (var x6)) (var x6))
(>=
 (f95
  (var x4)
  (var x6)
  (var x8)
  (var x63))
 (f2
  (f92 (var x4))
  (f93 (var x8))
  (f94 (var x6))))
(>=
 (f2
  (var x4)
  (+ (+ (var x8) (var x9)) 1)
  (var x6))
 (f2
  (f89 (var x4))
  (f90 (var x9))
  (f95
   (var x4)
   (var x6)
   (var x8)
   (var x63))))
(>= (f96 (var x14)) (var x14))
(>=
 (f2 (var x12) 0 (var x14))
 (f1 (f96 (var x14)) (var x12)))
(>= (f97 (var x21)) (var x21))
(>= (f98 (var x19)) (var x19))
(>=
 (f99 (var x19))
 (+ (f98 (var x19)) 1))
(>=
 (f4 (+ (var x21) 1) (var x19))
 (f4
  (f97 (var x21))
  (f99 (var x19))))
(>= (f4 0 (var x24)) (var x24))