(>= (f46 (var x27)) (var x27))
(>=
 (f2 (var x27) (f47))
 (f4 (f46 (var x27))))
(>= (f48 (var x3)) (var x3))
(>=
 (f1 (var x3))
 (f3 (f47) (f48 (var x3))))
(>=
 (f4 (+ (var x7) 1))
 (var x7))
(>= (f49 (var x37)) (var x37))
(>=
 (f2 (var x37) (f50 (var x10)))
 (f2 (f49 (var x37)) (var x10)))
(>= (f51 (var x13)) (var x13))
(>=
 (f52 (var x10) (var x13))
 (f2 (f51 (var x13)) (var x10)))
(>=
 (f3 (var x10) (+ (var x13) 1))
 (f3
  (f50 (var x10))
  (f52 (var x10) (var x13))))
(>= (f3 (var x17) 0) 0)