(>= (f208 (var x3)) (var x3))
(>=
 (f209 (var x3))
 (f208 (var x3)))
(>= (f210 (var x42)) (var x42))
(>= (f211 (var x43)) (var x43))
(>=
 (f1 (var x42) (f212))
 (+ (f210 (var x42)) 1))
(>=
 (+
  (f2 (var x42) (f212))
  (var x43))
 (f211 (var x43)))
(>=
 (f213 (var x3))
 (f209 (var x3)))
(>= (f214 (var x2)) (var x2))
(>= (f215 (var x1)) (var x1))
(>=
 (f216
  (var x1)
  (var x2)
  (var x3)
  (var x42)
  (var x43))
 (+
  (f6
   (f212)
   (f215 (var x1))
   (f214 (var x2))
   (f216
    (var x1)
    (var x2)
    (var x3)
    (var x42)
    (var x43)))
  (f213 (var x3))))
(>=
 (f217
  (var x1)
  (var x2)
  (var x3)
  (var x42)
  (var x43))
 (+
  (f5
   (f212)
   (f215 (var x1))
   (f214 (var x2)))
  (f216
   (var x1)
   (var x2)
   (var x3)
   (var x42)
   (var x43))))
(>=
 (f8 (var x1) (var x2))
 (f4
  (f212)
  (f215 (var x1))
  (f214 (var x2))))
(>=
 (f7 (var x1) (var x2))
 (f3
  (f212)
  (f215 (var x1))
  (f214 (var x2))))
(>=
 (+
  (f9 (var x1) (var x2))
  (var x3))
 (+
  (f217
   (var x1)
   (var x2)
   (var x3)
   (var x42)
   (var x43))
  1))
(>= (f218 (var x7)) (var x7))
(>=
 (f219 (var x7))
 (f218 (var x7)))
(>= (f220 (var x85)) (var x85))
(>= (f221 (var x86)) (var x86))
(>=
 (f1 (var x85) (f222 (var x4)))
 (f1 (f220 (var x85)) (var x4)))
(>=
 (+
  (f2 (var x85) (f222 (var x4)))
  (var x86))
 (+
  (f2 (f220 (var x85)) (var x4))
  (f221 (var x86))))
(>=
 (f223 (var x7))
 (f219 (var x7)))
(>= (f224 (var x9)) (var x9))
(>= (f225 (var x5)) (var x5))
(>=
 (f226
  (var x4)
  (var x5)
  (var x7)
  (var x9)
  (var x85)
  (var x86))
 (+
  (f6
   (f222 (var x4))
   (f225 (var x5))
   (f224 (var x9))
   (f226
    (var x4)
    (var x5)
    (var x7)
    (var x9)
    (var x85)
    (var x86)))
  (f223 (var x7))))
(>=
 (f227
  (var x4)
  (var x5)
  (var x9)
  (var x85)
  (var x86))
 (f4
  (f222 (var x4))
  (f225 (var x5))
  (f224 (var x9))))
(>=
 (f228
  (var x4)
  (var x5)
  (var x9)
  (var x10)
  (var x85)
  (var x86)
  (var x134)
  (var x135))
 (f3
  (f222 (var x4))
  (f225 (var x5))
  (f224 (var x9))))
(>=
 (f229
  (var x4)
  (var x5)
  (var x7)
  (var x9)
  (var x85)
  (var x86))
 (+
  (f5
   (f222 (var x4))
   (f225 (var x5))
   (f224 (var x9)))
  (f226
   (var x4)
   (var x5)
   (var x7)
   (var x9)
   (var x85)
   (var x86))))
(>=
 (f230
  (var x4)
  (var x5)
  (var x7)
  (var x9)
  (var x85)
  (var x86))
 (f229
  (var x4)
  (var x5)
  (var x7)
  (var x9)
  (var x85)
  (var x86)))
(>=
 (f231 (var x134))
 (var x134))
(>=
 (f232 (var x135))
 (var x135))
(>=
 (f1 (var x134) (f233 (var x4)))
 (f1
  (f231 (var x134))
  (var x4)))
(>=
 (+
  (f2 (var x134) (f233 (var x4)))
  (var x135))
 (+
  (f2 (f231 (var x134)) (var x4))
  (f232 (var x135))))
(>=
 (f234
  (var x4)
  (var x5)
  (var x7)
  (var x9)
  (var x85)
  (var x86))
 (f230
  (var x4)
  (var x5)
  (var x7)
  (var x9)
  (var x85)
  (var x86)))
(>= (f235 (var x10)) (var x10))
(>= (f236 (var x5)) (var x5))
(>=
 (f237
  (var x4)
  (var x5)
  (var x7)
  (var x9)
  (var x10)
  (var x85)
  (var x86)
  (var x134)
  (var x135))
 (+
  (f6
   (f233 (var x4))
   (f236 (var x5))
   (f235 (var x10))
   (f237
    (var x4)
    (var x5)
    (var x7)
    (var x9)
    (var x10)
    (var x85)
    (var x86)
    (var x134)
    (var x135)))
  (f234
   (var x4)
   (var x5)
   (var x7)
   (var x9)
   (var x85)
   (var x86))))
(>=
 (f238
  (var x4)
  (var x5)
  (var x10)
  (var x134)
  (var x135))
 (f4
  (f233 (var x4))
  (f236 (var x5))
  (f235 (var x10))))
(>=
 (f228
  (var x4)
  (var x5)
  (var x9)
  (var x10)
  (var x85)
  (var x86)
  (var x134)
  (var x135))
 (f3
  (f233 (var x4))
  (f236 (var x5))
  (f235 (var x10))))
(>=
 (f239
  (var x4)
  (var x5)
  (var x7)
  (var x9)
  (var x10)
  (var x85)
  (var x86)
  (var x134)
  (var x135))
 (+
  (f5
   (f233 (var x4))
   (f236 (var x5))
   (f235 (var x10)))
  (f237
   (var x4)
   (var x5)
   (var x7)
   (var x9)
   (var x10)
   (var x85)
   (var x86)
   (var x134)
   (var x135))))
(>=
 (f240
  (var x4)
  (var x5)
  (var x7)
  (var x9)
  (var x10)
  (var x85)
  (var x86)
  (var x134)
  (var x135))
 (f239
  (var x4)
  (var x5)
  (var x7)
  (var x9)
  (var x10)
  (var x85)
  (var x86)
  (var x134)
  (var x135)))
(>=
 (f4
  (var x4)
  (var x5)
  (+ (+ (var x9) (var x10)) 1))
 (+
  (+
   (f227
    (var x4)
    (var x5)
    (var x9)
    (var x85)
    (var x86))
   (f238
    (var x4)
    (var x5)
    (var x10)
    (var x134)
    (var x135)))
  1))
(>=
 (f3
  (var x4)
  (var x5)
  (+ (+ (var x9) (var x10)) 1))
 (f228
  (var x4)
  (var x5)
  (var x9)
  (var x10)
  (var x85)
  (var x86)
  (var x134)
  (var x135)))
(>=
 (+
  (f5
   (var x4)
   (var x5)
   (+ (+ (var x9) (var x10)) 1))
  (var x7))
 (+
  (f240
   (var x4)
   (var x5)
   (var x7)
   (var x9)
   (var x10)
   (var x85)
   (var x86)
   (var x134)
   (var x135))
  1))
(>= (f241 (var x16)) (var x16))
(>= (f242 (var x14)) (var x14))
(>=
 (f243 (var x16))
 (f241 (var x16)))
(>=
 (f244 (var x13) (var x14))
 (f1
  (f242 (var x14))
  (var x13)))
(>=
 (f245
  (var x13)
  (var x14)
  (var x16))
 (+
  (f2 (f242 (var x14)) (var x13))
  (f243 (var x16))))
(>=
 (f246
  (var x13)
  (var x14)
  (var x16))
 (f245
  (var x13)
  (var x14)
  (var x16)))
(>=
 (f4 (var x13) (var x14) 0)
 0)
(>=
 (f3 (var x13) (var x14) 0)
 (f244 (var x13) (var x14)))
(>=
 (+
  (f5 (var x13) (var x14) 0)
  (var x16))
 (+
  (f246
   (var x13)
   (var x14)
   (var x16))
  1))