(>= (f53 (var x2)) (var x2))
(>= (f54) 0)
(>=
 (f5 (var x2))
 (f6 (f53 (var x2)) (f54)))
(>= (f55 (var x7)) (var x7))
(>= (f56 (var x31)) (var x31))
(>=
 (f1 (var x31) (f57 (var x7)))
 (f6
  (f55 (var x7))
  (f56 (var x31))))
(>= (f58 (var x38)) (var x38))
(>=
 (f2 (var x38) (f59))
 (+ (f58 (var x38)) 1))
(>= (f60 (var x5)) (var x5))
(>=
 (f6 (+ (var x7) 1) (var x5))
 (f3
  (f57 (var x7))
  (f59)
  (f60 (var x5))))
(>= (f61 (var x10)) (var x10))
(>=
 (f6 0 (var x10))
 (f4 (f61 (var x10))))
(>= (f4 (var x13)) (var x13))
(>= (f62 (var x17)) (var x17))
(>=
 (f63 (var x16) (var x17))
 (f2 (f62 (var x17)) (var x16)))
(>=
 (f3
  (var x15)
  (var x16)
  (var x17))
 (f1
  (f63 (var x16) (var x17))
  (var x15)))