(set-option :produce-models true) (set-logic QF_LIA) (set-info :source |remove at least one strict rule from (RULES c# b -> c#, a# a -> a#, d# b -> d#, b a ->= a c b, c b ->= b b c, c a ->= b a c, a a ->= d d d a, a d ->= c d d, c d d a ->= d a a a, f f e e ->= e e f f f, d b ->= d d) by arctic matrix interpretation with dimension 2|) (declare-fun f0m () Bool) (declare-fun f0c () Int) (declare-fun f1m () Bool) (declare-fun f1c () Int) (declare-fun f2m () Bool) (declare-fun f2c () Int) (declare-fun f3m () Bool) (declare-fun f3c () Int) (declare-fun f4m () Bool) (declare-fun f4c () Int) (declare-fun f5m () Bool) (declare-fun f5c () Int) (declare-fun f6m () Bool) (declare-fun f6c () Int) (declare-fun f7m () Bool) (declare-fun f7c () Int) (declare-fun f8m () Bool) (declare-fun f8c () Int) (declare-fun f9m () Bool) (declare-fun f9c () Int) (declare-fun f10m () Bool) (declare-fun f10c () Int) (declare-fun f11m () Bool) (declare-fun f11c () Int) (declare-fun f12m () Bool) (declare-fun f12c () Int) (declare-fun f13m () Bool) (declare-fun f13c () Int) (declare-fun f14m () Bool) (declare-fun f14c () Int) (declare-fun f15m () Bool) (declare-fun f15c () Int) (declare-fun f16m () Bool) (declare-fun f16c () Int) (declare-fun f17m () Bool) (declare-fun f17c () Int) (declare-fun f18m () Bool) (declare-fun f18c () Int) (declare-fun f19m () Bool) (declare-fun f19c () Int) (declare-fun f20m () Bool) (declare-fun f20c () Int) (declare-fun f21m () Bool) (declare-fun f21c () Int) (declare-fun f22m () Bool) (declare-fun f22c () Int) (declare-fun f23m () Bool) (declare-fun f23c () Int) (declare-fun f24m () Bool) (declare-fun f24c () Int) (declare-fun f25m () Bool) (declare-fun f25c () Int) (declare-fun f26m () Bool) (declare-fun f26c () Int) (declare-fun f27m () Bool) (declare-fun f27c () Int) (declare-fun f28m () Bool) (declare-fun f28c () Int) (declare-fun f29m () Bool) (declare-fun f29c () Int) (declare-fun f30m () Bool) (declare-fun f30c () Int) (declare-fun f31m () Bool) (declare-fun f31c () Int) (declare-fun f32m () Bool) (declare-fun f32c () Int) (declare-fun f33m () Bool) (declare-fun f33c () Int) (declare-fun f34m () Bool) (declare-fun f34c () Int) (declare-fun f35m () Bool) (declare-fun f35c () Int) (declare-fun f36m () Bool) (declare-fun f36c () Int) (declare-fun f37m () Bool) (declare-fun f37c () Int) (declare-fun f38m () Bool) (declare-fun f38c () Int) (declare-fun f39m () Bool) (declare-fun f39c () Int) (declare-fun f40m () Bool) (declare-fun f40c () Int) (declare-fun f41m () Bool) (declare-fun f41c () Int) (declare-fun f42m () Bool) (declare-fun f42c () Int) (declare-fun f43m () Bool) (declare-fun f43c () Int) (declare-fun f44m () Bool) (declare-fun f44c () Int) (declare-fun f45m () Bool) (declare-fun f45c () Int) (declare-fun f46m () Bool) (declare-fun f46c () Int) (declare-fun f47m () Bool) (declare-fun f47c () Int) (declare-fun f48m () Bool) (declare-fun f48c () Int) (declare-fun f49m () Bool) (declare-fun f49c () Int) (declare-fun f50m () Bool) (declare-fun f50c () Int) (declare-fun f51m () Bool) (declare-fun f51c () Int) (declare-fun f52m () Bool) (declare-fun f52c () Int) (declare-fun f53m () Bool) (declare-fun f53c () Int) (assert (and (or (and (not f18m) (>= f18c 0)) (and (not f22m) (>= f22c 0))) (or (and (not f6m) (>= f6c 0)) (and (not f10m) (>= f10c 0))) (or (and (not f30m) (>= f30c 0)) (and (not f34m) (>= f34c 0))) (or (and (not f36m) (>= f36c 0)) (and (not f40m) (>= f40c 0))) (or (and (not f48m) (>= f48c 0)) (and (not f52m) (>= f52c 0))) (or (and (not f42m) (>= f42c 0)) (and (not f46m) (>= f46c 0))) (or (and (not f12m) (>= f12c 0)) (and (not f16m) (>= f16c 0))) (or (and (not f0m) (>= f0c 0)) (and (not f4m) (>= f4c 0))) (or (and (not f24m) (>= f24c 0)) (and (not f28m) (>= f28c 0))))) (declare-fun l0m () Bool) (declare-fun l0c () Int) (assert (= l0m (or f0m f6m))) (assert (or l0m (= l0c (+ f0c f6c)))) (declare-fun l1m () Bool) (declare-fun l1c () Int) (assert (= l1m (or f1m f8m))) (assert (or l1m (= l1c (+ f1c f8c)))) (declare-fun l2m () Bool) (declare-fun l2c () Int) (assert (= l2m (and l0m l1m))) (assert (and (or l2m l0m (>= l2c l0c)) (or l2m l1m (>= l2c l1c)))) (assert (or l2m (and (not l0m) (= l2c l0c)) (and (not l1m) (= l2c l1c)))) (define-fun f54m () Bool l2m) (define-fun f54c () Int l2c) (declare-fun l3m () Bool) (declare-fun l3c () Int) (assert (= l3m (or f0m f7m))) (assert (or l3m (= l3c (+ f0c f7c)))) (declare-fun l4m () Bool) (declare-fun l4c () Int) (assert (= l4m (or f1m f9m))) (assert (or l4m (= l4c (+ f1c f9c)))) (declare-fun l5m () Bool) (declare-fun l5c () Int) (assert (= l5m (and l3m l4m))) (assert (and (or l5m l3m (>= l5c l3c)) (or l5m l4m (>= l5c l4c)))) (assert (or l5m (and (not l3m) (= l5c l3c)) (and (not l4m) (= l5c l4c)))) (define-fun f55m () Bool l5m) (define-fun f55c () Int l5c) (declare-fun l6m () Bool) (declare-fun l6c () Int) (assert (= l6m (or f2m f6m))) (assert (or l6m (= l6c (+ f2c f6c)))) (declare-fun l7m () Bool) (declare-fun l7c () Int) (assert (= l7m (or f3m f8m))) (assert (or l7m (= l7c (+ f3c f8c)))) (declare-fun l8m () Bool) (declare-fun l8c () Int) (assert (= l8m (and l6m l7m))) (assert (and (or l8m l6m (>= l8c l6c)) (or l8m l7m (>= l8c l7c)))) (assert (or l8m (and (not l6m) (= l8c l6c)) (and (not l7m) (= l8c l7c)))) (define-fun f56m () Bool l8m) (define-fun f56c () Int l8c) (declare-fun l9m () Bool) (declare-fun l9c () Int) (assert (= l9m (or f2m f7m))) (assert (or l9m (= l9c (+ f2c f7c)))) (declare-fun l10m () Bool) (declare-fun l10c () Int) (assert (= l10m (or f3m f9m))) (assert (or l10m (= l10c (+ f3c f9c)))) (declare-fun l11m () Bool) (declare-fun l11c () Int) (assert (= l11m (and l9m l10m))) (assert (and (or l11m l9m (>= l11c l9c)) (or l11m l10m (>= l11c l10c)))) (assert (or l11m (and (not l9m) (= l11c l9c)) (and (not l10m) (= l11c l10c)))) (define-fun f57m () Bool l11m) (define-fun f57c () Int l11c) (declare-fun l12m () Bool) (declare-fun l12c () Int) (assert (= l12m (or f0m f10m))) (assert (or l12m (= l12c (+ f0c f10c)))) (declare-fun l13m () Bool) (declare-fun l13c () Int) (assert (= l13m (or f1m f11m))) (assert (or l13m (= l13c (+ f1c f11c)))) (declare-fun l14m () Bool) (declare-fun l14c () Int) (assert (= l14m (and l12m l13m))) (assert (and (or l14m l12m (>= l14c l12c)) (or l14m l13m (>= l14c l13c)))) (assert (or l14m (and (not l12m) (= l14c l12c)) (and (not l13m) (= l14c l13c)))) (define-fun f58m () Bool l14m) (define-fun f58c () Int l14c) (declare-fun l15m () Bool) (declare-fun l15c () Int) (assert (= l15m (or f2m f10m))) (assert (or l15m (= l15c (+ f2c f10c)))) (declare-fun l16m () Bool) (declare-fun l16c () Int) (assert (= l16m (or f3m f11m))) (assert (or l16m (= l16c (+ f3c f11c)))) (declare-fun l17m () Bool) (declare-fun l17c () Int) (assert (= l17m (and l15m l16m))) (assert (and (or l17m l15m (>= l17c l15c)) (or l17m l16m (>= l17c l16c)))) (assert (or l17m (and (not l15m) (= l17c l15c)) (and (not l16m) (= l17c l16c)))) (define-fun f59m () Bool l17m) (define-fun f59c () Int l17c) (declare-fun l18m () Bool) (declare-fun l18c () Int) (assert (= l18m (and f4m f58m))) (assert (and (or l18m f4m (>= l18c f4c)) (or l18m f58m (>= l18c f58c)))) (assert (or l18m (and (not f4m) (= l18c f4c)) (and (not f58m) (= l18c f58c)))) (define-fun f60m () Bool l18m) (define-fun f60c () Int l18c) (declare-fun l19m () Bool) (declare-fun l19c () Int) (assert (= l19m (and f5m f59m))) (assert (and (or l19m f5m (>= l19c f5c)) (or l19m f59m (>= l19c f59c)))) (assert (or l19m (and (not f5m) (= l19c f5c)) (and (not f59m) (= l19c f59c)))) (define-fun f61m () Bool l19m) (define-fun f61c () Int l19c) (declare-fun l20m () Bool) (declare-fun l20c () Int) (assert (= l20m (or f12m f18m))) (assert (or l20m (= l20c (+ f12c f18c)))) (declare-fun l21m () Bool) (declare-fun l21c () Int) (assert (= l21m (or f13m f20m))) (assert (or l21m (= l21c (+ f13c f20c)))) (declare-fun l22m () Bool) (declare-fun l22c () Int) (assert (= l22m (and l20m l21m))) (assert (and (or l22m l20m (>= l22c l20c)) (or l22m l21m (>= l22c l21c)))) (assert (or l22m (and (not l20m) (= l22c l20c)) (and (not l21m) (= l22c l21c)))) (define-fun f62m () Bool l22m) (define-fun f62c () Int l22c) (declare-fun l23m () Bool) (declare-fun l23c () Int) (assert (= l23m (or f12m f19m))) (assert (or l23m (= l23c (+ f12c f19c)))) (declare-fun l24m () Bool) (declare-fun l24c () Int) (assert (= l24m (or f13m f21m))) (assert (or l24m (= l24c (+ f13c f21c)))) (declare-fun l25m () Bool) (declare-fun l25c () Int) (assert (= l25m (and l23m l24m))) (assert (and (or l25m l23m (>= l25c l23c)) (or l25m l24m (>= l25c l24c)))) (assert (or l25m (and (not l23m) (= l25c l23c)) (and (not l24m) (= l25c l24c)))) (define-fun f63m () Bool l25m) (define-fun f63c () Int l25c) (declare-fun l26m () Bool) (declare-fun l26c () Int) (assert (= l26m (or f14m f18m))) (assert (or l26m (= l26c (+ f14c f18c)))) (declare-fun l27m () Bool) (declare-fun l27c () Int) (assert (= l27m (or f15m f20m))) (assert (or l27m (= l27c (+ f15c f20c)))) (declare-fun l28m () Bool) (declare-fun l28c () Int) (assert (= l28m (and l26m l27m))) (assert (and (or l28m l26m (>= l28c l26c)) (or l28m l27m (>= l28c l27c)))) (assert (or l28m (and (not l26m) (= l28c l26c)) (and (not l27m) (= l28c l27c)))) (define-fun f64m () Bool l28m) (define-fun f64c () Int l28c) (declare-fun l29m () Bool) (declare-fun l29c () Int) (assert (= l29m (or f14m f19m))) (assert (or l29m (= l29c (+ f14c f19c)))) (declare-fun l30m () Bool) (declare-fun l30c () Int) (assert (= l30m (or f15m f21m))) (assert (or l30m (= l30c (+ f15c f21c)))) (declare-fun l31m () Bool) (declare-fun l31c () Int) (assert (= l31m (and l29m l30m))) (assert (and (or l31m l29m (>= l31c l29c)) (or l31m l30m (>= l31c l30c)))) (assert (or l31m (and (not l29m) (= l31c l29c)) (and (not l30m) (= l31c l30c)))) (define-fun f65m () Bool l31m) (define-fun f65c () Int l31c) (declare-fun l32m () Bool) (declare-fun l32c () Int) (assert (= l32m (or f12m f22m))) (assert (or l32m (= l32c (+ f12c f22c)))) (declare-fun l33m () Bool) (declare-fun l33c () Int) (assert (= l33m (or f13m f23m))) (assert (or l33m (= l33c (+ f13c f23c)))) (declare-fun l34m () Bool) (declare-fun l34c () Int) (assert (= l34m (and l32m l33m))) (assert (and (or l34m l32m (>= l34c l32c)) (or l34m l33m (>= l34c l33c)))) (assert (or l34m (and (not l32m) (= l34c l32c)) (and (not l33m) (= l34c l33c)))) (define-fun f66m () Bool l34m) (define-fun f66c () Int l34c) (declare-fun l35m () Bool) (declare-fun l35c () Int) (assert (= l35m (or f14m f22m))) (assert (or l35m (= l35c (+ f14c f22c)))) (declare-fun l36m () Bool) (declare-fun l36c () Int) (assert (= l36m (or f15m f23m))) (assert (or l36m (= l36c (+ f15c f23c)))) (declare-fun l37m () Bool) (declare-fun l37c () Int) (assert (= l37m (and l35m l36m))) (assert (and (or l37m l35m (>= l37c l35c)) (or l37m l36m (>= l37c l36c)))) (assert (or l37m (and (not l35m) (= l37c l35c)) (and (not l36m) (= l37c l36c)))) (define-fun f67m () Bool l37m) (define-fun f67c () Int l37c) (declare-fun l38m () Bool) (declare-fun l38c () Int) (assert (= l38m (and f16m f66m))) (assert (and (or l38m f16m (>= l38c f16c)) (or l38m f66m (>= l38c f66c)))) (assert (or l38m (and (not f16m) (= l38c f16c)) (and (not f66m) (= l38c f66c)))) (define-fun f68m () Bool l38m) (define-fun f68c () Int l38c) (declare-fun l39m () Bool) (declare-fun l39c () Int) (assert (= l39m (and f17m f67m))) (assert (and (or l39m f17m (>= l39c f17c)) (or l39m f67m (>= l39c f67c)))) (assert (or l39m (and (not f17m) (= l39c f17c)) (and (not f67m) (= l39c f67c)))) (define-fun f69m () Bool l39m) (define-fun f69c () Int l39c) (declare-fun l40m () Bool) (declare-fun l40c () Int) (assert (= l40m (or f24m f6m))) (assert (or l40m (= l40c (+ f24c f6c)))) (declare-fun l41m () Bool) (declare-fun l41c () Int) (assert (= l41m (or f25m f8m))) (assert (or l41m (= l41c (+ f25c f8c)))) (declare-fun l42m () Bool) (declare-fun l42c () Int) (assert (= l42m (and l40m l41m))) (assert (and (or l42m l40m (>= l42c l40c)) (or l42m l41m (>= l42c l41c)))) (assert (or l42m (and (not l40m) (= l42c l40c)) (and (not l41m) (= l42c l41c)))) (define-fun f70m () Bool l42m) (define-fun f70c () Int l42c) (declare-fun l43m () Bool) (declare-fun l43c () Int) (assert (= l43m (or f24m f7m))) (assert (or l43m (= l43c (+ f24c f7c)))) (declare-fun l44m () Bool) (declare-fun l44c () Int) (assert (= l44m (or f25m f9m))) (assert (or l44m (= l44c (+ f25c f9c)))) (declare-fun l45m () Bool) (declare-fun l45c () Int) (assert (= l45m (and l43m l44m))) (assert (and (or l45m l43m (>= l45c l43c)) (or l45m l44m (>= l45c l44c)))) (assert (or l45m (and (not l43m) (= l45c l43c)) (and (not l44m) (= l45c l44c)))) (define-fun f71m () Bool l45m) (define-fun f71c () Int l45c) (declare-fun l46m () Bool) (declare-fun l46c () Int) (assert (= l46m (or f26m f6m))) (assert (or l46m (= l46c (+ f26c f6c)))) (declare-fun l47m () Bool) (declare-fun l47c () Int) (assert (= l47m (or f27m f8m))) (assert (or l47m (= l47c (+ f27c f8c)))) (declare-fun l48m () Bool) (declare-fun l48c () Int) (assert (= l48m (and l46m l47m))) (assert (and (or l48m l46m (>= l48c l46c)) (or l48m l47m (>= l48c l47c)))) (assert (or l48m (and (not l46m) (= l48c l46c)) (and (not l47m) (= l48c l47c)))) (define-fun f72m () Bool l48m) (define-fun f72c () Int l48c) (declare-fun l49m () Bool) (declare-fun l49c () Int) (assert (= l49m (or f26m f7m))) (assert (or l49m (= l49c (+ f26c f7c)))) (declare-fun l50m () Bool) (declare-fun l50c () Int) (assert (= l50m (or f27m f9m))) (assert (or l50m (= l50c (+ f27c f9c)))) (declare-fun l51m () Bool) (declare-fun l51c () Int) (assert (= l51m (and l49m l50m))) (assert (and (or l51m l49m (>= l51c l49c)) (or l51m l50m (>= l51c l50c)))) (assert (or l51m (and (not l49m) (= l51c l49c)) (and (not l50m) (= l51c l50c)))) (define-fun f73m () Bool l51m) (define-fun f73c () Int l51c) (declare-fun l52m () Bool) (declare-fun l52c () Int) (assert (= l52m (or f24m f10m))) (assert (or l52m (= l52c (+ f24c f10c)))) (declare-fun l53m () Bool) (declare-fun l53c () Int) (assert (= l53m (or f25m f11m))) (assert (or l53m (= l53c (+ f25c f11c)))) (declare-fun l54m () Bool) (declare-fun l54c () Int) (assert (= l54m (and l52m l53m))) (assert (and (or l54m l52m (>= l54c l52c)) (or l54m l53m (>= l54c l53c)))) (assert (or l54m (and (not l52m) (= l54c l52c)) (and (not l53m) (= l54c l53c)))) (define-fun f74m () Bool l54m) (define-fun f74c () Int l54c) (declare-fun l55m () Bool) (declare-fun l55c () Int) (assert (= l55m (or f26m f10m))) (assert (or l55m (= l55c (+ f26c f10c)))) (declare-fun l56m () Bool) (declare-fun l56c () Int) (assert (= l56m (or f27m f11m))) (assert (or l56m (= l56c (+ f27c f11c)))) (declare-fun l57m () Bool) (declare-fun l57c () Int) (assert (= l57m (and l55m l56m))) (assert (and (or l57m l55m (>= l57c l55c)) (or l57m l56m (>= l57c l56c)))) (assert (or l57m (and (not l55m) (= l57c l55c)) (and (not l56m) (= l57c l56c)))) (define-fun f75m () Bool l57m) (define-fun f75c () Int l57c) (declare-fun l58m () Bool) (declare-fun l58c () Int) (assert (= l58m (and f28m f74m))) (assert (and (or l58m f28m (>= l58c f28c)) (or l58m f74m (>= l58c f74c)))) (assert (or l58m (and (not f28m) (= l58c f28c)) (and (not f74m) (= l58c f74c)))) (define-fun f76m () Bool l58m) (define-fun f76c () Int l58c) (declare-fun l59m () Bool) (declare-fun l59c () Int) (assert (= l59m (and f29m f75m))) (assert (and (or l59m f29m (>= l59c f29c)) (or l59m f75m (>= l59c f75c)))) (assert (or l59m (and (not f29m) (= l59c f29c)) (and (not f75m) (= l59c f75c)))) (define-fun f77m () Bool l59m) (define-fun f77c () Int l59c) (declare-fun l60m () Bool) (declare-fun l60c () Int) (assert (= l60m (or f6m f18m))) (assert (or l60m (= l60c (+ f6c f18c)))) (declare-fun l61m () Bool) (declare-fun l61c () Int) (assert (= l61m (or f7m f20m))) (assert (or l61m (= l61c (+ f7c f20c)))) (declare-fun l62m () Bool) (declare-fun l62c () Int) (assert (= l62m (and l60m l61m))) (assert (and (or l62m l60m (>= l62c l60c)) (or l62m l61m (>= l62c l61c)))) (assert (or l62m (and (not l60m) (= l62c l60c)) (and (not l61m) (= l62c l61c)))) (define-fun f78m () Bool l62m) (define-fun f78c () Int l62c) (declare-fun l63m () Bool) (declare-fun l63c () Int) (assert (= l63m (or f6m f19m))) (assert (or l63m (= l63c (+ f6c f19c)))) (declare-fun l64m () Bool) (declare-fun l64c () Int) (assert (= l64m (or f7m f21m))) (assert (or l64m (= l64c (+ f7c f21c)))) (declare-fun l65m () Bool) (declare-fun l65c () Int) (assert (= l65m (and l63m l64m))) (assert (and (or l65m l63m (>= l65c l63c)) (or l65m l64m (>= l65c l64c)))) (assert (or l65m (and (not l63m) (= l65c l63c)) (and (not l64m) (= l65c l64c)))) (define-fun f79m () Bool l65m) (define-fun f79c () Int l65c) (declare-fun l66m () Bool) (declare-fun l66c () Int) (assert (= l66m (or f8m f18m))) (assert (or l66m (= l66c (+ f8c f18c)))) (declare-fun l67m () Bool) (declare-fun l67c () Int) (assert (= l67m (or f9m f20m))) (assert (or l67m (= l67c (+ f9c f20c)))) (declare-fun l68m () Bool) (declare-fun l68c () Int) (assert (= l68m (and l66m l67m))) (assert (and (or l68m l66m (>= l68c l66c)) (or l68m l67m (>= l68c l67c)))) (assert (or l68m (and (not l66m) (= l68c l66c)) (and (not l67m) (= l68c l67c)))) (define-fun f80m () Bool l68m) (define-fun f80c () Int l68c) (declare-fun l69m () Bool) (declare-fun l69c () Int) (assert (= l69m (or f8m f19m))) (assert (or l69m (= l69c (+ f8c f19c)))) (declare-fun l70m () Bool) (declare-fun l70c () Int) (assert (= l70m (or f9m f21m))) (assert (or l70m (= l70c (+ f9c f21c)))) (declare-fun l71m () Bool) (declare-fun l71c () Int) (assert (= l71m (and l69m l70m))) (assert (and (or l71m l69m (>= l71c l69c)) (or l71m l70m (>= l71c l70c)))) (assert (or l71m (and (not l69m) (= l71c l69c)) (and (not l70m) (= l71c l70c)))) (define-fun f81m () Bool l71m) (define-fun f81c () Int l71c) (declare-fun l72m () Bool) (declare-fun l72c () Int) (assert (= l72m (or f6m f22m))) (assert (or l72m (= l72c (+ f6c f22c)))) (declare-fun l73m () Bool) (declare-fun l73c () Int) (assert (= l73m (or f7m f23m))) (assert (or l73m (= l73c (+ f7c f23c)))) (declare-fun l74m () Bool) (declare-fun l74c () Int) (assert (= l74m (and l72m l73m))) (assert (and (or l74m l72m (>= l74c l72c)) (or l74m l73m (>= l74c l73c)))) (assert (or l74m (and (not l72m) (= l74c l72c)) (and (not l73m) (= l74c l73c)))) (define-fun f82m () Bool l74m) (define-fun f82c () Int l74c) (declare-fun l75m () Bool) (declare-fun l75c () Int) (assert (= l75m (or f8m f22m))) (assert (or l75m (= l75c (+ f8c f22c)))) (declare-fun l76m () Bool) (declare-fun l76c () Int) (assert (= l76m (or f9m f23m))) (assert (or l76m (= l76c (+ f9c f23c)))) (declare-fun l77m () Bool) (declare-fun l77c () Int) (assert (= l77m (and l75m l76m))) (assert (and (or l77m l75m (>= l77c l75c)) (or l77m l76m (>= l77c l76c)))) (assert (or l77m (and (not l75m) (= l77c l75c)) (and (not l76m) (= l77c l76c)))) (define-fun f83m () Bool l77m) (define-fun f83c () Int l77c) (declare-fun l78m () Bool) (declare-fun l78c () Int) (assert (= l78m (and f10m f82m))) (assert (and (or l78m f10m (>= l78c f10c)) (or l78m f82m (>= l78c f82c)))) (assert (or l78m (and (not f10m) (= l78c f10c)) (and (not f82m) (= l78c f82c)))) (define-fun f84m () Bool l78m) (define-fun f84c () Int l78c) (declare-fun l79m () Bool) (declare-fun l79c () Int) (assert (= l79m (and f11m f83m))) (assert (and (or l79m f11m (>= l79c f11c)) (or l79m f83m (>= l79c f83c)))) (assert (or l79m (and (not f11m) (= l79c f11c)) (and (not f83m) (= l79c f83c)))) (define-fun f85m () Bool l79m) (define-fun f85c () Int l79c) (declare-fun l80m () Bool) (declare-fun l80c () Int) (assert (= l80m (or f30m f6m))) (assert (or l80m (= l80c (+ f30c f6c)))) (declare-fun l81m () Bool) (declare-fun l81c () Int) (assert (= l81m (or f31m f8m))) (assert (or l81m (= l81c (+ f31c f8c)))) (declare-fun l82m () Bool) (declare-fun l82c () Int) (assert (= l82m (and l80m l81m))) (assert (and (or l82m l80m (>= l82c l80c)) (or l82m l81m (>= l82c l81c)))) (assert (or l82m (and (not l80m) (= l82c l80c)) (and (not l81m) (= l82c l81c)))) (define-fun f86m () Bool l82m) (define-fun f86c () Int l82c) (declare-fun l83m () Bool) (declare-fun l83c () Int) (assert (= l83m (or f30m f7m))) (assert (or l83m (= l83c (+ f30c f7c)))) (declare-fun l84m () Bool) (declare-fun l84c () Int) (assert (= l84m (or f31m f9m))) (assert (or l84m (= l84c (+ f31c f9c)))) (declare-fun l85m () Bool) (declare-fun l85c () Int) (assert (= l85m (and l83m l84m))) (assert (and (or l85m l83m (>= l85c l83c)) (or l85m l84m (>= l85c l84c)))) (assert (or l85m (and (not l83m) (= l85c l83c)) (and (not l84m) (= l85c l84c)))) (define-fun f87m () Bool l85m) (define-fun f87c () Int l85c) (declare-fun l86m () Bool) (declare-fun l86c () Int) (assert (= l86m (or f32m f6m))) (assert (or l86m (= l86c (+ f32c f6c)))) (declare-fun l87m () Bool) (declare-fun l87c () Int) (assert (= l87m (or f33m f8m))) (assert (or l87m (= l87c (+ f33c f8c)))) (declare-fun l88m () Bool) (declare-fun l88c () Int) (assert (= l88m (and l86m l87m))) (assert (and (or l88m l86m (>= l88c l86c)) (or l88m l87m (>= l88c l87c)))) (assert (or l88m (and (not l86m) (= l88c l86c)) (and (not l87m) (= l88c l87c)))) (define-fun f88m () Bool l88m) (define-fun f88c () Int l88c) (declare-fun l89m () Bool) (declare-fun l89c () Int) (assert (= l89m (or f32m f7m))) (assert (or l89m (= l89c (+ f32c f7c)))) (declare-fun l90m () Bool) (declare-fun l90c () Int) (assert (= l90m (or f33m f9m))) (assert (or l90m (= l90c (+ f33c f9c)))) (declare-fun l91m () Bool) (declare-fun l91c () Int) (assert (= l91m (and l89m l90m))) (assert (and (or l91m l89m (>= l91c l89c)) (or l91m l90m (>= l91c l90c)))) (assert (or l91m (and (not l89m) (= l91c l89c)) (and (not l90m) (= l91c l90c)))) (define-fun f89m () Bool l91m) (define-fun f89c () Int l91c) (declare-fun l92m () Bool) (declare-fun l92c () Int) (assert (= l92m (or f30m f10m))) (assert (or l92m (= l92c (+ f30c f10c)))) (declare-fun l93m () Bool) (declare-fun l93c () Int) (assert (= l93m (or f31m f11m))) (assert (or l93m (= l93c (+ f31c f11c)))) (declare-fun l94m () Bool) (declare-fun l94c () Int) (assert (= l94m (and l92m l93m))) (assert (and (or l94m l92m (>= l94c l92c)) (or l94m l93m (>= l94c l93c)))) (assert (or l94m (and (not l92m) (= l94c l92c)) (and (not l93m) (= l94c l93c)))) (define-fun f90m () Bool l94m) (define-fun f90c () Int l94c) (declare-fun l95m () Bool) (declare-fun l95c () Int) (assert (= l95m (or f32m f10m))) (assert (or l95m (= l95c (+ f32c f10c)))) (declare-fun l96m () Bool) (declare-fun l96c () Int) (assert (= l96m (or f33m f11m))) (assert (or l96m (= l96c (+ f33c f11c)))) (declare-fun l97m () Bool) (declare-fun l97c () Int) (assert (= l97m (and l95m l96m))) (assert (and (or l97m l95m (>= l97c l95c)) (or l97m l96m (>= l97c l96c)))) (assert (or l97m (and (not l95m) (= l97c l95c)) (and (not l96m) (= l97c l96c)))) (define-fun f91m () Bool l97m) (define-fun f91c () Int l97c) (declare-fun l98m () Bool) (declare-fun l98c () Int) (assert (= l98m (and f34m f90m))) (assert (and (or l98m f34m (>= l98c f34c)) (or l98m f90m (>= l98c f90c)))) (assert (or l98m (and (not f34m) (= l98c f34c)) (and (not f90m) (= l98c f90c)))) (define-fun f92m () Bool l98m) (define-fun f92c () Int l98c) (declare-fun l99m () Bool) (declare-fun l99c () Int) (assert (= l99m (and f35m f91m))) (assert (and (or l99m f35m (>= l99c f35c)) (or l99m f91m (>= l99c f91c)))) (assert (or l99m (and (not f35m) (= l99c f35c)) (and (not f91m) (= l99c f91c)))) (define-fun f93m () Bool l99m) (define-fun f93c () Int l99c) (declare-fun l100m () Bool) (declare-fun l100c () Int) (assert (= l100m (or f18m f86m))) (assert (or l100m (= l100c (+ f18c f86c)))) (declare-fun l101m () Bool) (declare-fun l101c () Int) (assert (= l101m (or f19m f88m))) (assert (or l101m (= l101c (+ f19c f88c)))) (declare-fun l102m () Bool) (declare-fun l102c () Int) (assert (= l102m (and l100m l101m))) (assert (and (or l102m l100m (>= l102c l100c)) (or l102m l101m (>= l102c l101c)))) (assert (or l102m (and (not l100m) (= l102c l100c)) (and (not l101m) (= l102c l101c)))) (define-fun f94m () Bool l102m) (define-fun f94c () Int l102c) (declare-fun l103m () Bool) (declare-fun l103c () Int) (assert (= l103m (or f18m f87m))) (assert (or l103m (= l103c (+ f18c f87c)))) (declare-fun l104m () Bool) (declare-fun l104c () Int) (assert (= l104m (or f19m f89m))) (assert (or l104m (= l104c (+ f19c f89c)))) (declare-fun l105m () Bool) (declare-fun l105c () Int) (assert (= l105m (and l103m l104m))) (assert (and (or l105m l103m (>= l105c l103c)) (or l105m l104m (>= l105c l104c)))) (assert (or l105m (and (not l103m) (= l105c l103c)) (and (not l104m) (= l105c l104c)))) (define-fun f95m () Bool l105m) (define-fun f95c () Int l105c) (declare-fun l106m () Bool) (declare-fun l106c () Int) (assert (= l106m (or f20m f86m))) (assert (or l106m (= l106c (+ f20c f86c)))) (declare-fun l107m () Bool) (declare-fun l107c () Int) (assert (= l107m (or f21m f88m))) (assert (or l107m (= l107c (+ f21c f88c)))) (declare-fun l108m () Bool) (declare-fun l108c () Int) (assert (= l108m (and l106m l107m))) (assert (and (or l108m l106m (>= l108c l106c)) (or l108m l107m (>= l108c l107c)))) (assert (or l108m (and (not l106m) (= l108c l106c)) (and (not l107m) (= l108c l107c)))) (define-fun f96m () Bool l108m) (define-fun f96c () Int l108c) (declare-fun l109m () Bool) (declare-fun l109c () Int) (assert (= l109m (or f20m f87m))) (assert (or l109m (= l109c (+ f20c f87c)))) (declare-fun l110m () Bool) (declare-fun l110c () Int) (assert (= l110m (or f21m f89m))) (assert (or l110m (= l110c (+ f21c f89c)))) (declare-fun l111m () Bool) (declare-fun l111c () Int) (assert (= l111m (and l109m l110m))) (assert (and (or l111m l109m (>= l111c l109c)) (or l111m l110m (>= l111c l110c)))) (assert (or l111m (and (not l109m) (= l111c l109c)) (and (not l110m) (= l111c l110c)))) (define-fun f97m () Bool l111m) (define-fun f97c () Int l111c) (declare-fun l112m () Bool) (declare-fun l112c () Int) (assert (= l112m (or f18m f92m))) (assert (or l112m (= l112c (+ f18c f92c)))) (declare-fun l113m () Bool) (declare-fun l113c () Int) (assert (= l113m (or f19m f93m))) (assert (or l113m (= l113c (+ f19c f93c)))) (declare-fun l114m () Bool) (declare-fun l114c () Int) (assert (= l114m (and l112m l113m))) (assert (and (or l114m l112m (>= l114c l112c)) (or l114m l113m (>= l114c l113c)))) (assert (or l114m (and (not l112m) (= l114c l112c)) (and (not l113m) (= l114c l113c)))) (define-fun f98m () Bool l114m) (define-fun f98c () Int l114c) (declare-fun l115m () Bool) (declare-fun l115c () Int) (assert (= l115m (or f20m f92m))) (assert (or l115m (= l115c (+ f20c f92c)))) (declare-fun l116m () Bool) (declare-fun l116c () Int) (assert (= l116m (or f21m f93m))) (assert (or l116m (= l116c (+ f21c f93c)))) (declare-fun l117m () Bool) (declare-fun l117c () Int) (assert (= l117m (and l115m l116m))) (assert (and (or l117m l115m (>= l117c l115c)) (or l117m l116m (>= l117c l116c)))) (assert (or l117m (and (not l115m) (= l117c l115c)) (and (not l116m) (= l117c l116c)))) (define-fun f99m () Bool l117m) (define-fun f99c () Int l117c) (declare-fun l118m () Bool) (declare-fun l118c () Int) (assert (= l118m (and f22m f98m))) (assert (and (or l118m f22m (>= l118c f22c)) (or l118m f98m (>= l118c f98c)))) (assert (or l118m (and (not f22m) (= l118c f22c)) (and (not f98m) (= l118c f98c)))) (define-fun f100m () Bool l118m) (define-fun f100c () Int l118c) (declare-fun l119m () Bool) (declare-fun l119c () Int) (assert (= l119m (and f23m f99m))) (assert (and (or l119m f23m (>= l119c f23c)) (or l119m f99m (>= l119c f99c)))) (assert (or l119m (and (not f23m) (= l119c f23c)) (and (not f99m) (= l119c f99c)))) (define-fun f101m () Bool l119m) (define-fun f101c () Int l119c) (declare-fun l120m () Bool) (declare-fun l120c () Int) (assert (= l120m (or f30m f6m))) (assert (or l120m (= l120c (+ f30c f6c)))) (declare-fun l121m () Bool) (declare-fun l121c () Int) (assert (= l121m (or f31m f8m))) (assert (or l121m (= l121c (+ f31c f8c)))) (declare-fun l122m () Bool) (declare-fun l122c () Int) (assert (= l122m (and l120m l121m))) (assert (and (or l122m l120m (>= l122c l120c)) (or l122m l121m (>= l122c l121c)))) (assert (or l122m (and (not l120m) (= l122c l120c)) (and (not l121m) (= l122c l121c)))) (define-fun f102m () Bool l122m) (define-fun f102c () Int l122c) (declare-fun l123m () Bool) (declare-fun l123c () Int) (assert (= l123m (or f30m f7m))) (assert (or l123m (= l123c (+ f30c f7c)))) (declare-fun l124m () Bool) (declare-fun l124c () Int) (assert (= l124m (or f31m f9m))) (assert (or l124m (= l124c (+ f31c f9c)))) (declare-fun l125m () Bool) (declare-fun l125c () Int) (assert (= l125m (and l123m l124m))) (assert (and (or l125m l123m (>= l125c l123c)) (or l125m l124m (>= l125c l124c)))) (assert (or l125m (and (not l123m) (= l125c l123c)) (and (not l124m) (= l125c l124c)))) (define-fun f103m () Bool l125m) (define-fun f103c () Int l125c) (declare-fun l126m () Bool) (declare-fun l126c () Int) (assert (= l126m (or f32m f6m))) (assert (or l126m (= l126c (+ f32c f6c)))) (declare-fun l127m () Bool) (declare-fun l127c () Int) (assert (= l127m (or f33m f8m))) (assert (or l127m (= l127c (+ f33c f8c)))) (declare-fun l128m () Bool) (declare-fun l128c () Int) (assert (= l128m (and l126m l127m))) (assert (and (or l128m l126m (>= l128c l126c)) (or l128m l127m (>= l128c l127c)))) (assert (or l128m (and (not l126m) (= l128c l126c)) (and (not l127m) (= l128c l127c)))) (define-fun f104m () Bool l128m) (define-fun f104c () Int l128c) (declare-fun l129m () Bool) (declare-fun l129c () Int) (assert (= l129m (or f32m f7m))) (assert (or l129m (= l129c (+ f32c f7c)))) (declare-fun l130m () Bool) (declare-fun l130c () Int) (assert (= l130m (or f33m f9m))) (assert (or l130m (= l130c (+ f33c f9c)))) (declare-fun l131m () Bool) (declare-fun l131c () Int) (assert (= l131m (and l129m l130m))) (assert (and (or l131m l129m (>= l131c l129c)) (or l131m l130m (>= l131c l130c)))) (assert (or l131m (and (not l129m) (= l131c l129c)) (and (not l130m) (= l131c l130c)))) (define-fun f105m () Bool l131m) (define-fun f105c () Int l131c) (declare-fun l132m () Bool) (declare-fun l132c () Int) (assert (= l132m (or f30m f10m))) (assert (or l132m (= l132c (+ f30c f10c)))) (declare-fun l133m () Bool) (declare-fun l133c () Int) (assert (= l133m (or f31m f11m))) (assert (or l133m (= l133c (+ f31c f11c)))) (declare-fun l134m () Bool) (declare-fun l134c () Int) (assert (= l134m (and l132m l133m))) (assert (and (or l134m l132m (>= l134c l132c)) (or l134m l133m (>= l134c l133c)))) (assert (or l134m (and (not l132m) (= l134c l132c)) (and (not l133m) (= l134c l133c)))) (define-fun f106m () Bool l134m) (define-fun f106c () Int l134c) (declare-fun l135m () Bool) (declare-fun l135c () Int) (assert (= l135m (or f32m f10m))) (assert (or l135m (= l135c (+ f32c f10c)))) (declare-fun l136m () Bool) (declare-fun l136c () Int) (assert (= l136m (or f33m f11m))) (assert (or l136m (= l136c (+ f33c f11c)))) (declare-fun l137m () Bool) (declare-fun l137c () Int) (assert (= l137m (and l135m l136m))) (assert (and (or l137m l135m (>= l137c l135c)) (or l137m l136m (>= l137c l136c)))) (assert (or l137m (and (not l135m) (= l137c l135c)) (and (not l136m) (= l137c l136c)))) (define-fun f107m () Bool l137m) (define-fun f107c () Int l137c) (declare-fun l138m () Bool) (declare-fun l138c () Int) (assert (= l138m (and f34m f106m))) (assert (and (or l138m f34m (>= l138c f34c)) (or l138m f106m (>= l138c f106c)))) (assert (or l138m (and (not f34m) (= l138c f34c)) (and (not f106m) (= l138c f106c)))) (define-fun f108m () Bool l138m) (define-fun f108c () Int l138c) (declare-fun l139m () Bool) (declare-fun l139c () Int) (assert (= l139m (and f35m f107m))) (assert (and (or l139m f35m (>= l139c f35c)) (or l139m f107m (>= l139c f107c)))) (assert (or l139m (and (not f35m) (= l139c f35c)) (and (not f107m) (= l139c f107c)))) (define-fun f109m () Bool l139m) (define-fun f109c () Int l139c) (declare-fun l140m () Bool) (declare-fun l140c () Int) (assert (= l140m (or f6m f30m))) (assert (or l140m (= l140c (+ f6c f30c)))) (declare-fun l141m () Bool) (declare-fun l141c () Int) (assert (= l141m (or f7m f32m))) (assert (or l141m (= l141c (+ f7c f32c)))) (declare-fun l142m () Bool) (declare-fun l142c () Int) (assert (= l142m (and l140m l141m))) (assert (and (or l142m l140m (>= l142c l140c)) (or l142m l141m (>= l142c l141c)))) (assert (or l142m (and (not l140m) (= l142c l140c)) (and (not l141m) (= l142c l141c)))) (define-fun f110m () Bool l142m) (define-fun f110c () Int l142c) (declare-fun l143m () Bool) (declare-fun l143c () Int) (assert (= l143m (or f6m f31m))) (assert (or l143m (= l143c (+ f6c f31c)))) (declare-fun l144m () Bool) (declare-fun l144c () Int) (assert (= l144m (or f7m f33m))) (assert (or l144m (= l144c (+ f7c f33c)))) (declare-fun l145m () Bool) (declare-fun l145c () Int) (assert (= l145m (and l143m l144m))) (assert (and (or l145m l143m (>= l145c l143c)) (or l145m l144m (>= l145c l144c)))) (assert (or l145m (and (not l143m) (= l145c l143c)) (and (not l144m) (= l145c l144c)))) (define-fun f111m () Bool l145m) (define-fun f111c () Int l145c) (declare-fun l146m () Bool) (declare-fun l146c () Int) (assert (= l146m (or f8m f30m))) (assert (or l146m (= l146c (+ f8c f30c)))) (declare-fun l147m () Bool) (declare-fun l147c () Int) (assert (= l147m (or f9m f32m))) (assert (or l147m (= l147c (+ f9c f32c)))) (declare-fun l148m () Bool) (declare-fun l148c () Int) (assert (= l148m (and l146m l147m))) (assert (and (or l148m l146m (>= l148c l146c)) (or l148m l147m (>= l148c l147c)))) (assert (or l148m (and (not l146m) (= l148c l146c)) (and (not l147m) (= l148c l147c)))) (define-fun f112m () Bool l148m) (define-fun f112c () Int l148c) (declare-fun l149m () Bool) (declare-fun l149c () Int) (assert (= l149m (or f8m f31m))) (assert (or l149m (= l149c (+ f8c f31c)))) (declare-fun l150m () Bool) (declare-fun l150c () Int) (assert (= l150m (or f9m f33m))) (assert (or l150m (= l150c (+ f9c f33c)))) (declare-fun l151m () Bool) (declare-fun l151c () Int) (assert (= l151m (and l149m l150m))) (assert (and (or l151m l149m (>= l151c l149c)) (or l151m l150m (>= l151c l150c)))) (assert (or l151m (and (not l149m) (= l151c l149c)) (and (not l150m) (= l151c l150c)))) (define-fun f113m () Bool l151m) (define-fun f113c () Int l151c) (declare-fun l152m () Bool) (declare-fun l152c () Int) (assert (= l152m (or f6m f34m))) (assert (or l152m (= l152c (+ f6c f34c)))) (declare-fun l153m () Bool) (declare-fun l153c () Int) (assert (= l153m (or f7m f35m))) (assert (or l153m (= l153c (+ f7c f35c)))) (declare-fun l154m () Bool) (declare-fun l154c () Int) (assert (= l154m (and l152m l153m))) (assert (and (or l154m l152m (>= l154c l152c)) (or l154m l153m (>= l154c l153c)))) (assert (or l154m (and (not l152m) (= l154c l152c)) (and (not l153m) (= l154c l153c)))) (define-fun f114m () Bool l154m) (define-fun f114c () Int l154c) (declare-fun l155m () Bool) (declare-fun l155c () Int) (assert (= l155m (or f8m f34m))) (assert (or l155m (= l155c (+ f8c f34c)))) (declare-fun l156m () Bool) (declare-fun l156c () Int) (assert (= l156m (or f9m f35m))) (assert (or l156m (= l156c (+ f9c f35c)))) (declare-fun l157m () Bool) (declare-fun l157c () Int) (assert (= l157m (and l155m l156m))) (assert (and (or l157m l155m (>= l157c l155c)) (or l157m l156m (>= l157c l156c)))) (assert (or l157m (and (not l155m) (= l157c l155c)) (and (not l156m) (= l157c l156c)))) (define-fun f115m () Bool l157m) (define-fun f115c () Int l157c) (declare-fun l158m () Bool) (declare-fun l158c () Int) (assert (= l158m (and f10m f114m))) (assert (and (or l158m f10m (>= l158c f10c)) (or l158m f114m (>= l158c f114c)))) (assert (or l158m (and (not f10m) (= l158c f10c)) (and (not f114m) (= l158c f114c)))) (define-fun f116m () Bool l158m) (define-fun f116c () Int l158c) (declare-fun l159m () Bool) (declare-fun l159c () Int) (assert (= l159m (and f11m f115m))) (assert (and (or l159m f11m (>= l159c f11c)) (or l159m f115m (>= l159c f115c)))) (assert (or l159m (and (not f11m) (= l159c f11c)) (and (not f115m) (= l159c f115c)))) (define-fun f117m () Bool l159m) (define-fun f117c () Int l159c) (declare-fun l160m () Bool) (declare-fun l160c () Int) (assert (= l160m (or f6m f110m))) (assert (or l160m (= l160c (+ f6c f110c)))) (declare-fun l161m () Bool) (declare-fun l161c () Int) (assert (= l161m (or f7m f112m))) (assert (or l161m (= l161c (+ f7c f112c)))) (declare-fun l162m () Bool) (declare-fun l162c () Int) (assert (= l162m (and l160m l161m))) (assert (and (or l162m l160m (>= l162c l160c)) (or l162m l161m (>= l162c l161c)))) (assert (or l162m (and (not l160m) (= l162c l160c)) (and (not l161m) (= l162c l161c)))) (define-fun f118m () Bool l162m) (define-fun f118c () Int l162c) (declare-fun l163m () Bool) (declare-fun l163c () Int) (assert (= l163m (or f6m f111m))) (assert (or l163m (= l163c (+ f6c f111c)))) (declare-fun l164m () Bool) (declare-fun l164c () Int) (assert (= l164m (or f7m f113m))) (assert (or l164m (= l164c (+ f7c f113c)))) (declare-fun l165m () Bool) (declare-fun l165c () Int) (assert (= l165m (and l163m l164m))) (assert (and (or l165m l163m (>= l165c l163c)) (or l165m l164m (>= l165c l164c)))) (assert (or l165m (and (not l163m) (= l165c l163c)) (and (not l164m) (= l165c l164c)))) (define-fun f119m () Bool l165m) (define-fun f119c () Int l165c) (declare-fun l166m () Bool) (declare-fun l166c () Int) (assert (= l166m (or f8m f110m))) (assert (or l166m (= l166c (+ f8c f110c)))) (declare-fun l167m () Bool) (declare-fun l167c () Int) (assert (= l167m (or f9m f112m))) (assert (or l167m (= l167c (+ f9c f112c)))) (declare-fun l168m () Bool) (declare-fun l168c () Int) (assert (= l168m (and l166m l167m))) (assert (and (or l168m l166m (>= l168c l166c)) (or l168m l167m (>= l168c l167c)))) (assert (or l168m (and (not l166m) (= l168c l166c)) (and (not l167m) (= l168c l167c)))) (define-fun f120m () Bool l168m) (define-fun f120c () Int l168c) (declare-fun l169m () Bool) (declare-fun l169c () Int) (assert (= l169m (or f8m f111m))) (assert (or l169m (= l169c (+ f8c f111c)))) (declare-fun l170m () Bool) (declare-fun l170c () Int) (assert (= l170m (or f9m f113m))) (assert (or l170m (= l170c (+ f9c f113c)))) (declare-fun l171m () Bool) (declare-fun l171c () Int) (assert (= l171m (and l169m l170m))) (assert (and (or l171m l169m (>= l171c l169c)) (or l171m l170m (>= l171c l170c)))) (assert (or l171m (and (not l169m) (= l171c l169c)) (and (not l170m) (= l171c l170c)))) (define-fun f121m () Bool l171m) (define-fun f121c () Int l171c) (declare-fun l172m () Bool) (declare-fun l172c () Int) (assert (= l172m (or f6m f116m))) (assert (or l172m (= l172c (+ f6c f116c)))) (declare-fun l173m () Bool) (declare-fun l173c () Int) (assert (= l173m (or f7m f117m))) (assert (or l173m (= l173c (+ f7c f117c)))) (declare-fun l174m () Bool) (declare-fun l174c () Int) (assert (= l174m (and l172m l173m))) (assert (and (or l174m l172m (>= l174c l172c)) (or l174m l173m (>= l174c l173c)))) (assert (or l174m (and (not l172m) (= l174c l172c)) (and (not l173m) (= l174c l173c)))) (define-fun f122m () Bool l174m) (define-fun f122c () Int l174c) (declare-fun l175m () Bool) (declare-fun l175c () Int) (assert (= l175m (or f8m f116m))) (assert (or l175m (= l175c (+ f8c f116c)))) (declare-fun l176m () Bool) (declare-fun l176c () Int) (assert (= l176m (or f9m f117m))) (assert (or l176m (= l176c (+ f9c f117c)))) (declare-fun l177m () Bool) (declare-fun l177c () Int) (assert (= l177m (and l175m l176m))) (assert (and (or l177m l175m (>= l177c l175c)) (or l177m l176m (>= l177c l176c)))) (assert (or l177m (and (not l175m) (= l177c l175c)) (and (not l176m) (= l177c l176c)))) (define-fun f123m () Bool l177m) (define-fun f123c () Int l177c) (declare-fun l178m () Bool) (declare-fun l178c () Int) (assert (= l178m (and f10m f122m))) (assert (and (or l178m f10m (>= l178c f10c)) (or l178m f122m (>= l178c f122c)))) (assert (or l178m (and (not f10m) (= l178c f10c)) (and (not f122m) (= l178c f122c)))) (define-fun f124m () Bool l178m) (define-fun f124c () Int l178c) (declare-fun l179m () Bool) (declare-fun l179c () Int) (assert (= l179m (and f11m f123m))) (assert (and (or l179m f11m (>= l179c f11c)) (or l179m f123m (>= l179c f123c)))) (assert (or l179m (and (not f11m) (= l179c f11c)) (and (not f123m) (= l179c f123c)))) (define-fun f125m () Bool l179m) (define-fun f125c () Int l179c) (declare-fun l180m () Bool) (declare-fun l180c () Int) (assert (= l180m (or f30m f18m))) (assert (or l180m (= l180c (+ f30c f18c)))) (declare-fun l181m () Bool) (declare-fun l181c () Int) (assert (= l181m (or f31m f20m))) (assert (or l181m (= l181c (+ f31c f20c)))) (declare-fun l182m () Bool) (declare-fun l182c () Int) (assert (= l182m (and l180m l181m))) (assert (and (or l182m l180m (>= l182c l180c)) (or l182m l181m (>= l182c l181c)))) (assert (or l182m (and (not l180m) (= l182c l180c)) (and (not l181m) (= l182c l181c)))) (define-fun f126m () Bool l182m) (define-fun f126c () Int l182c) (declare-fun l183m () Bool) (declare-fun l183c () Int) (assert (= l183m (or f30m f19m))) (assert (or l183m (= l183c (+ f30c f19c)))) (declare-fun l184m () Bool) (declare-fun l184c () Int) (assert (= l184m (or f31m f21m))) (assert (or l184m (= l184c (+ f31c f21c)))) (declare-fun l185m () Bool) (declare-fun l185c () Int) (assert (= l185m (and l183m l184m))) (assert (and (or l185m l183m (>= l185c l183c)) (or l185m l184m (>= l185c l184c)))) (assert (or l185m (and (not l183m) (= l185c l183c)) (and (not l184m) (= l185c l184c)))) (define-fun f127m () Bool l185m) (define-fun f127c () Int l185c) (declare-fun l186m () Bool) (declare-fun l186c () Int) (assert (= l186m (or f32m f18m))) (assert (or l186m (= l186c (+ f32c f18c)))) (declare-fun l187m () Bool) (declare-fun l187c () Int) (assert (= l187m (or f33m f20m))) (assert (or l187m (= l187c (+ f33c f20c)))) (declare-fun l188m () Bool) (declare-fun l188c () Int) (assert (= l188m (and l186m l187m))) (assert (and (or l188m l186m (>= l188c l186c)) (or l188m l187m (>= l188c l187c)))) (assert (or l188m (and (not l186m) (= l188c l186c)) (and (not l187m) (= l188c l187c)))) (define-fun f128m () Bool l188m) (define-fun f128c () Int l188c) (declare-fun l189m () Bool) (declare-fun l189c () Int) (assert (= l189m (or f32m f19m))) (assert (or l189m (= l189c (+ f32c f19c)))) (declare-fun l190m () Bool) (declare-fun l190c () Int) (assert (= l190m (or f33m f21m))) (assert (or l190m (= l190c (+ f33c f21c)))) (declare-fun l191m () Bool) (declare-fun l191c () Int) (assert (= l191m (and l189m l190m))) (assert (and (or l191m l189m (>= l191c l189c)) (or l191m l190m (>= l191c l190c)))) (assert (or l191m (and (not l189m) (= l191c l189c)) (and (not l190m) (= l191c l190c)))) (define-fun f129m () Bool l191m) (define-fun f129c () Int l191c) (declare-fun l192m () Bool) (declare-fun l192c () Int) (assert (= l192m (or f30m f22m))) (assert (or l192m (= l192c (+ f30c f22c)))) (declare-fun l193m () Bool) (declare-fun l193c () Int) (assert (= l193m (or f31m f23m))) (assert (or l193m (= l193c (+ f31c f23c)))) (declare-fun l194m () Bool) (declare-fun l194c () Int) (assert (= l194m (and l192m l193m))) (assert (and (or l194m l192m (>= l194c l192c)) (or l194m l193m (>= l194c l193c)))) (assert (or l194m (and (not l192m) (= l194c l192c)) (and (not l193m) (= l194c l193c)))) (define-fun f130m () Bool l194m) (define-fun f130c () Int l194c) (declare-fun l195m () Bool) (declare-fun l195c () Int) (assert (= l195m (or f32m f22m))) (assert (or l195m (= l195c (+ f32c f22c)))) (declare-fun l196m () Bool) (declare-fun l196c () Int) (assert (= l196m (or f33m f23m))) (assert (or l196m (= l196c (+ f33c f23c)))) (declare-fun l197m () Bool) (declare-fun l197c () Int) (assert (= l197m (and l195m l196m))) (assert (and (or l197m l195m (>= l197c l195c)) (or l197m l196m (>= l197c l196c)))) (assert (or l197m (and (not l195m) (= l197c l195c)) (and (not l196m) (= l197c l196c)))) (define-fun f131m () Bool l197m) (define-fun f131c () Int l197c) (declare-fun l198m () Bool) (declare-fun l198c () Int) (assert (= l198m (and f34m f130m))) (assert (and (or l198m f34m (>= l198c f34c)) (or l198m f130m (>= l198c f130c)))) (assert (or l198m (and (not f34m) (= l198c f34c)) (and (not f130m) (= l198c f130c)))) (define-fun f132m () Bool l198m) (define-fun f132c () Int l198c) (declare-fun l199m () Bool) (declare-fun l199c () Int) (assert (= l199m (and f35m f131m))) (assert (and (or l199m f35m (>= l199c f35c)) (or l199m f131m (>= l199c f131c)))) (assert (or l199m (and (not f35m) (= l199c f35c)) (and (not f131m) (= l199c f131c)))) (define-fun f133m () Bool l199m) (define-fun f133c () Int l199c) (declare-fun l200m () Bool) (declare-fun l200c () Int) (assert (= l200m (or f18m f30m))) (assert (or l200m (= l200c (+ f18c f30c)))) (declare-fun l201m () Bool) (declare-fun l201c () Int) (assert (= l201m (or f19m f32m))) (assert (or l201m (= l201c (+ f19c f32c)))) (declare-fun l202m () Bool) (declare-fun l202c () Int) (assert (= l202m (and l200m l201m))) (assert (and (or l202m l200m (>= l202c l200c)) (or l202m l201m (>= l202c l201c)))) (assert (or l202m (and (not l200m) (= l202c l200c)) (and (not l201m) (= l202c l201c)))) (define-fun f134m () Bool l202m) (define-fun f134c () Int l202c) (declare-fun l203m () Bool) (declare-fun l203c () Int) (assert (= l203m (or f18m f31m))) (assert (or l203m (= l203c (+ f18c f31c)))) (declare-fun l204m () Bool) (declare-fun l204c () Int) (assert (= l204m (or f19m f33m))) (assert (or l204m (= l204c (+ f19c f33c)))) (declare-fun l205m () Bool) (declare-fun l205c () Int) (assert (= l205m (and l203m l204m))) (assert (and (or l205m l203m (>= l205c l203c)) (or l205m l204m (>= l205c l204c)))) (assert (or l205m (and (not l203m) (= l205c l203c)) (and (not l204m) (= l205c l204c)))) (define-fun f135m () Bool l205m) (define-fun f135c () Int l205c) (declare-fun l206m () Bool) (declare-fun l206c () Int) (assert (= l206m (or f20m f30m))) (assert (or l206m (= l206c (+ f20c f30c)))) (declare-fun l207m () Bool) (declare-fun l207c () Int) (assert (= l207m (or f21m f32m))) (assert (or l207m (= l207c (+ f21c f32c)))) (declare-fun l208m () Bool) (declare-fun l208c () Int) (assert (= l208m (and l206m l207m))) (assert (and (or l208m l206m (>= l208c l206c)) (or l208m l207m (>= l208c l207c)))) (assert (or l208m (and (not l206m) (= l208c l206c)) (and (not l207m) (= l208c l207c)))) (define-fun f136m () Bool l208m) (define-fun f136c () Int l208c) (declare-fun l209m () Bool) (declare-fun l209c () Int) (assert (= l209m (or f20m f31m))) (assert (or l209m (= l209c (+ f20c f31c)))) (declare-fun l210m () Bool) (declare-fun l210c () Int) (assert (= l210m (or f21m f33m))) (assert (or l210m (= l210c (+ f21c f33c)))) (declare-fun l211m () Bool) (declare-fun l211c () Int) (assert (= l211m (and l209m l210m))) (assert (and (or l211m l209m (>= l211c l209c)) (or l211m l210m (>= l211c l210c)))) (assert (or l211m (and (not l209m) (= l211c l209c)) (and (not l210m) (= l211c l210c)))) (define-fun f137m () Bool l211m) (define-fun f137c () Int l211c) (declare-fun l212m () Bool) (declare-fun l212c () Int) (assert (= l212m (or f18m f34m))) (assert (or l212m (= l212c (+ f18c f34c)))) (declare-fun l213m () Bool) (declare-fun l213c () Int) (assert (= l213m (or f19m f35m))) (assert (or l213m (= l213c (+ f19c f35c)))) (declare-fun l214m () Bool) (declare-fun l214c () Int) (assert (= l214m (and l212m l213m))) (assert (and (or l214m l212m (>= l214c l212c)) (or l214m l213m (>= l214c l213c)))) (assert (or l214m (and (not l212m) (= l214c l212c)) (and (not l213m) (= l214c l213c)))) (define-fun f138m () Bool l214m) (define-fun f138c () Int l214c) (declare-fun l215m () Bool) (declare-fun l215c () Int) (assert (= l215m (or f20m f34m))) (assert (or l215m (= l215c (+ f20c f34c)))) (declare-fun l216m () Bool) (declare-fun l216c () Int) (assert (= l216m (or f21m f35m))) (assert (or l216m (= l216c (+ f21c f35c)))) (declare-fun l217m () Bool) (declare-fun l217c () Int) (assert (= l217m (and l215m l216m))) (assert (and (or l217m l215m (>= l217c l215c)) (or l217m l216m (>= l217c l216c)))) (assert (or l217m (and (not l215m) (= l217c l215c)) (and (not l216m) (= l217c l216c)))) (define-fun f139m () Bool l217m) (define-fun f139c () Int l217c) (declare-fun l218m () Bool) (declare-fun l218c () Int) (assert (= l218m (and f22m f138m))) (assert (and (or l218m f22m (>= l218c f22c)) (or l218m f138m (>= l218c f138c)))) (assert (or l218m (and (not f22m) (= l218c f22c)) (and (not f138m) (= l218c f138c)))) (define-fun f140m () Bool l218m) (define-fun f140c () Int l218c) (declare-fun l219m () Bool) (declare-fun l219c () Int) (assert (= l219m (and f23m f139m))) (assert (and (or l219m f23m (>= l219c f23c)) (or l219m f139m (>= l219c f139c)))) (assert (or l219m (and (not f23m) (= l219c f23c)) (and (not f139m) (= l219c f139c)))) (define-fun f141m () Bool l219m) (define-fun f141c () Int l219c) (declare-fun l220m () Bool) (declare-fun l220c () Int) (assert (= l220m (or f6m f134m))) (assert (or l220m (= l220c (+ f6c f134c)))) (declare-fun l221m () Bool) (declare-fun l221c () Int) (assert (= l221m (or f7m f136m))) (assert (or l221m (= l221c (+ f7c f136c)))) (declare-fun l222m () Bool) (declare-fun l222c () Int) (assert (= l222m (and l220m l221m))) (assert (and (or l222m l220m (>= l222c l220c)) (or l222m l221m (>= l222c l221c)))) (assert (or l222m (and (not l220m) (= l222c l220c)) (and (not l221m) (= l222c l221c)))) (define-fun f142m () Bool l222m) (define-fun f142c () Int l222c) (declare-fun l223m () Bool) (declare-fun l223c () Int) (assert (= l223m (or f6m f135m))) (assert (or l223m (= l223c (+ f6c f135c)))) (declare-fun l224m () Bool) (declare-fun l224c () Int) (assert (= l224m (or f7m f137m))) (assert (or l224m (= l224c (+ f7c f137c)))) (declare-fun l225m () Bool) (declare-fun l225c () Int) (assert (= l225m (and l223m l224m))) (assert (and (or l225m l223m (>= l225c l223c)) (or l225m l224m (>= l225c l224c)))) (assert (or l225m (and (not l223m) (= l225c l223c)) (and (not l224m) (= l225c l224c)))) (define-fun f143m () Bool l225m) (define-fun f143c () Int l225c) (declare-fun l226m () Bool) (declare-fun l226c () Int) (assert (= l226m (or f8m f134m))) (assert (or l226m (= l226c (+ f8c f134c)))) (declare-fun l227m () Bool) (declare-fun l227c () Int) (assert (= l227m (or f9m f136m))) (assert (or l227m (= l227c (+ f9c f136c)))) (declare-fun l228m () Bool) (declare-fun l228c () Int) (assert (= l228m (and l226m l227m))) (assert (and (or l228m l226m (>= l228c l226c)) (or l228m l227m (>= l228c l227c)))) (assert (or l228m (and (not l226m) (= l228c l226c)) (and (not l227m) (= l228c l227c)))) (define-fun f144m () Bool l228m) (define-fun f144c () Int l228c) (declare-fun l229m () Bool) (declare-fun l229c () Int) (assert (= l229m (or f8m f135m))) (assert (or l229m (= l229c (+ f8c f135c)))) (declare-fun l230m () Bool) (declare-fun l230c () Int) (assert (= l230m (or f9m f137m))) (assert (or l230m (= l230c (+ f9c f137c)))) (declare-fun l231m () Bool) (declare-fun l231c () Int) (assert (= l231m (and l229m l230m))) (assert (and (or l231m l229m (>= l231c l229c)) (or l231m l230m (>= l231c l230c)))) (assert (or l231m (and (not l229m) (= l231c l229c)) (and (not l230m) (= l231c l230c)))) (define-fun f145m () Bool l231m) (define-fun f145c () Int l231c) (declare-fun l232m () Bool) (declare-fun l232c () Int) (assert (= l232m (or f6m f140m))) (assert (or l232m (= l232c (+ f6c f140c)))) (declare-fun l233m () Bool) (declare-fun l233c () Int) (assert (= l233m (or f7m f141m))) (assert (or l233m (= l233c (+ f7c f141c)))) (declare-fun l234m () Bool) (declare-fun l234c () Int) (assert (= l234m (and l232m l233m))) (assert (and (or l234m l232m (>= l234c l232c)) (or l234m l233m (>= l234c l233c)))) (assert (or l234m (and (not l232m) (= l234c l232c)) (and (not l233m) (= l234c l233c)))) (define-fun f146m () Bool l234m) (define-fun f146c () Int l234c) (declare-fun l235m () Bool) (declare-fun l235c () Int) (assert (= l235m (or f8m f140m))) (assert (or l235m (= l235c (+ f8c f140c)))) (declare-fun l236m () Bool) (declare-fun l236c () Int) (assert (= l236m (or f9m f141m))) (assert (or l236m (= l236c (+ f9c f141c)))) (declare-fun l237m () Bool) (declare-fun l237c () Int) (assert (= l237m (and l235m l236m))) (assert (and (or l237m l235m (>= l237c l235c)) (or l237m l236m (>= l237c l236c)))) (assert (or l237m (and (not l235m) (= l237c l235c)) (and (not l236m) (= l237c l236c)))) (define-fun f147m () Bool l237m) (define-fun f147c () Int l237c) (declare-fun l238m () Bool) (declare-fun l238c () Int) (assert (= l238m (and f10m f146m))) (assert (and (or l238m f10m (>= l238c f10c)) (or l238m f146m (>= l238c f146c)))) (assert (or l238m (and (not f10m) (= l238c f10c)) (and (not f146m) (= l238c f146c)))) (define-fun f148m () Bool l238m) (define-fun f148c () Int l238c) (declare-fun l239m () Bool) (declare-fun l239c () Int) (assert (= l239m (and f11m f147m))) (assert (and (or l239m f11m (>= l239c f11c)) (or l239m f147m (>= l239c f147c)))) (assert (or l239m (and (not f11m) (= l239c f11c)) (and (not f147m) (= l239c f147c)))) (define-fun f149m () Bool l239m) (define-fun f149c () Int l239c) (declare-fun l240m () Bool) (declare-fun l240c () Int) (assert (= l240m (or f18m f18m))) (assert (or l240m (= l240c (+ f18c f18c)))) (declare-fun l241m () Bool) (declare-fun l241c () Int) (assert (= l241m (or f19m f20m))) (assert (or l241m (= l241c (+ f19c f20c)))) (declare-fun l242m () Bool) (declare-fun l242c () Int) (assert (= l242m (and l240m l241m))) (assert (and (or l242m l240m (>= l242c l240c)) (or l242m l241m (>= l242c l241c)))) (assert (or l242m (and (not l240m) (= l242c l240c)) (and (not l241m) (= l242c l241c)))) (define-fun f150m () Bool l242m) (define-fun f150c () Int l242c) (declare-fun l243m () Bool) (declare-fun l243c () Int) (assert (= l243m (or f18m f19m))) (assert (or l243m (= l243c (+ f18c f19c)))) (declare-fun l244m () Bool) (declare-fun l244c () Int) (assert (= l244m (or f19m f21m))) (assert (or l244m (= l244c (+ f19c f21c)))) (declare-fun l245m () Bool) (declare-fun l245c () Int) (assert (= l245m (and l243m l244m))) (assert (and (or l245m l243m (>= l245c l243c)) (or l245m l244m (>= l245c l244c)))) (assert (or l245m (and (not l243m) (= l245c l243c)) (and (not l244m) (= l245c l244c)))) (define-fun f151m () Bool l245m) (define-fun f151c () Int l245c) (declare-fun l246m () Bool) (declare-fun l246c () Int) (assert (= l246m (or f20m f18m))) (assert (or l246m (= l246c (+ f20c f18c)))) (declare-fun l247m () Bool) (declare-fun l247c () Int) (assert (= l247m (or f21m f20m))) (assert (or l247m (= l247c (+ f21c f20c)))) (declare-fun l248m () Bool) (declare-fun l248c () Int) (assert (= l248m (and l246m l247m))) (assert (and (or l248m l246m (>= l248c l246c)) (or l248m l247m (>= l248c l247c)))) (assert (or l248m (and (not l246m) (= l248c l246c)) (and (not l247m) (= l248c l247c)))) (define-fun f152m () Bool l248m) (define-fun f152c () Int l248c) (declare-fun l249m () Bool) (declare-fun l249c () Int) (assert (= l249m (or f20m f19m))) (assert (or l249m (= l249c (+ f20c f19c)))) (declare-fun l250m () Bool) (declare-fun l250c () Int) (assert (= l250m (or f21m f21m))) (assert (or l250m (= l250c (+ f21c f21c)))) (declare-fun l251m () Bool) (declare-fun l251c () Int) (assert (= l251m (and l249m l250m))) (assert (and (or l251m l249m (>= l251c l249c)) (or l251m l250m (>= l251c l250c)))) (assert (or l251m (and (not l249m) (= l251c l249c)) (and (not l250m) (= l251c l250c)))) (define-fun f153m () Bool l251m) (define-fun f153c () Int l251c) (declare-fun l252m () Bool) (declare-fun l252c () Int) (assert (= l252m (or f18m f22m))) (assert (or l252m (= l252c (+ f18c f22c)))) (declare-fun l253m () Bool) (declare-fun l253c () Int) (assert (= l253m (or f19m f23m))) (assert (or l253m (= l253c (+ f19c f23c)))) (declare-fun l254m () Bool) (declare-fun l254c () Int) (assert (= l254m (and l252m l253m))) (assert (and (or l254m l252m (>= l254c l252c)) (or l254m l253m (>= l254c l253c)))) (assert (or l254m (and (not l252m) (= l254c l252c)) (and (not l253m) (= l254c l253c)))) (define-fun f154m () Bool l254m) (define-fun f154c () Int l254c) (declare-fun l255m () Bool) (declare-fun l255c () Int) (assert (= l255m (or f20m f22m))) (assert (or l255m (= l255c (+ f20c f22c)))) (declare-fun l256m () Bool) (declare-fun l256c () Int) (assert (= l256m (or f21m f23m))) (assert (or l256m (= l256c (+ f21c f23c)))) (declare-fun l257m () Bool) (declare-fun l257c () Int) (assert (= l257m (and l255m l256m))) (assert (and (or l257m l255m (>= l257c l255c)) (or l257m l256m (>= l257c l256c)))) (assert (or l257m (and (not l255m) (= l257c l255c)) (and (not l256m) (= l257c l256c)))) (define-fun f155m () Bool l257m) (define-fun f155c () Int l257c) (declare-fun l258m () Bool) (declare-fun l258c () Int) (assert (= l258m (and f22m f154m))) (assert (and (or l258m f22m (>= l258c f22c)) (or l258m f154m (>= l258c f154c)))) (assert (or l258m (and (not f22m) (= l258c f22c)) (and (not f154m) (= l258c f154c)))) (define-fun f156m () Bool l258m) (define-fun f156c () Int l258c) (declare-fun l259m () Bool) (declare-fun l259c () Int) (assert (= l259m (and f23m f155m))) (assert (and (or l259m f23m (>= l259c f23c)) (or l259m f155m (>= l259c f155c)))) (assert (or l259m (and (not f23m) (= l259c f23c)) (and (not f155m) (= l259c f155c)))) (define-fun f157m () Bool l259m) (define-fun f157c () Int l259c) (declare-fun l260m () Bool) (declare-fun l260c () Int) (assert (= l260m (or f36m f18m))) (assert (or l260m (= l260c (+ f36c f18c)))) (declare-fun l261m () Bool) (declare-fun l261c () Int) (assert (= l261m (or f37m f20m))) (assert (or l261m (= l261c (+ f37c f20c)))) (declare-fun l262m () Bool) (declare-fun l262c () Int) (assert (= l262m (and l260m l261m))) (assert (and (or l262m l260m (>= l262c l260c)) (or l262m l261m (>= l262c l261c)))) (assert (or l262m (and (not l260m) (= l262c l260c)) (and (not l261m) (= l262c l261c)))) (define-fun f158m () Bool l262m) (define-fun f158c () Int l262c) (declare-fun l263m () Bool) (declare-fun l263c () Int) (assert (= l263m (or f36m f19m))) (assert (or l263m (= l263c (+ f36c f19c)))) (declare-fun l264m () Bool) (declare-fun l264c () Int) (assert (= l264m (or f37m f21m))) (assert (or l264m (= l264c (+ f37c f21c)))) (declare-fun l265m () Bool) (declare-fun l265c () Int) (assert (= l265m (and l263m l264m))) (assert (and (or l265m l263m (>= l265c l263c)) (or l265m l264m (>= l265c l264c)))) (assert (or l265m (and (not l263m) (= l265c l263c)) (and (not l264m) (= l265c l264c)))) (define-fun f159m () Bool l265m) (define-fun f159c () Int l265c) (declare-fun l266m () Bool) (declare-fun l266c () Int) (assert (= l266m (or f38m f18m))) (assert (or l266m (= l266c (+ f38c f18c)))) (declare-fun l267m () Bool) (declare-fun l267c () Int) (assert (= l267m (or f39m f20m))) (assert (or l267m (= l267c (+ f39c f20c)))) (declare-fun l268m () Bool) (declare-fun l268c () Int) (assert (= l268m (and l266m l267m))) (assert (and (or l268m l266m (>= l268c l266c)) (or l268m l267m (>= l268c l267c)))) (assert (or l268m (and (not l266m) (= l268c l266c)) (and (not l267m) (= l268c l267c)))) (define-fun f160m () Bool l268m) (define-fun f160c () Int l268c) (declare-fun l269m () Bool) (declare-fun l269c () Int) (assert (= l269m (or f38m f19m))) (assert (or l269m (= l269c (+ f38c f19c)))) (declare-fun l270m () Bool) (declare-fun l270c () Int) (assert (= l270m (or f39m f21m))) (assert (or l270m (= l270c (+ f39c f21c)))) (declare-fun l271m () Bool) (declare-fun l271c () Int) (assert (= l271m (and l269m l270m))) (assert (and (or l271m l269m (>= l271c l269c)) (or l271m l270m (>= l271c l270c)))) (assert (or l271m (and (not l269m) (= l271c l269c)) (and (not l270m) (= l271c l270c)))) (define-fun f161m () Bool l271m) (define-fun f161c () Int l271c) (declare-fun l272m () Bool) (declare-fun l272c () Int) (assert (= l272m (or f36m f22m))) (assert (or l272m (= l272c (+ f36c f22c)))) (declare-fun l273m () Bool) (declare-fun l273c () Int) (assert (= l273m (or f37m f23m))) (assert (or l273m (= l273c (+ f37c f23c)))) (declare-fun l274m () Bool) (declare-fun l274c () Int) (assert (= l274m (and l272m l273m))) (assert (and (or l274m l272m (>= l274c l272c)) (or l274m l273m (>= l274c l273c)))) (assert (or l274m (and (not l272m) (= l274c l272c)) (and (not l273m) (= l274c l273c)))) (define-fun f162m () Bool l274m) (define-fun f162c () Int l274c) (declare-fun l275m () Bool) (declare-fun l275c () Int) (assert (= l275m (or f38m f22m))) (assert (or l275m (= l275c (+ f38c f22c)))) (declare-fun l276m () Bool) (declare-fun l276c () Int) (assert (= l276m (or f39m f23m))) (assert (or l276m (= l276c (+ f39c f23c)))) (declare-fun l277m () Bool) (declare-fun l277c () Int) (assert (= l277m (and l275m l276m))) (assert (and (or l277m l275m (>= l277c l275c)) (or l277m l276m (>= l277c l276c)))) (assert (or l277m (and (not l275m) (= l277c l275c)) (and (not l276m) (= l277c l276c)))) (define-fun f163m () Bool l277m) (define-fun f163c () Int l277c) (declare-fun l278m () Bool) (declare-fun l278c () Int) (assert (= l278m (and f40m f162m))) (assert (and (or l278m f40m (>= l278c f40c)) (or l278m f162m (>= l278c f162c)))) (assert (or l278m (and (not f40m) (= l278c f40c)) (and (not f162m) (= l278c f162c)))) (define-fun f164m () Bool l278m) (define-fun f164c () Int l278c) (declare-fun l279m () Bool) (declare-fun l279c () Int) (assert (= l279m (and f41m f163m))) (assert (and (or l279m f41m (>= l279c f41c)) (or l279m f163m (>= l279c f163c)))) (assert (or l279m (and (not f41m) (= l279c f41c)) (and (not f163m) (= l279c f163c)))) (define-fun f165m () Bool l279m) (define-fun f165c () Int l279c) (declare-fun l280m () Bool) (declare-fun l280c () Int) (assert (= l280m (or f36m f158m))) (assert (or l280m (= l280c (+ f36c f158c)))) (declare-fun l281m () Bool) (declare-fun l281c () Int) (assert (= l281m (or f37m f160m))) (assert (or l281m (= l281c (+ f37c f160c)))) (declare-fun l282m () Bool) (declare-fun l282c () Int) (assert (= l282m (and l280m l281m))) (assert (and (or l282m l280m (>= l282c l280c)) (or l282m l281m (>= l282c l281c)))) (assert (or l282m (and (not l280m) (= l282c l280c)) (and (not l281m) (= l282c l281c)))) (define-fun f166m () Bool l282m) (define-fun f166c () Int l282c) (declare-fun l283m () Bool) (declare-fun l283c () Int) (assert (= l283m (or f36m f159m))) (assert (or l283m (= l283c (+ f36c f159c)))) (declare-fun l284m () Bool) (declare-fun l284c () Int) (assert (= l284m (or f37m f161m))) (assert (or l284m (= l284c (+ f37c f161c)))) (declare-fun l285m () Bool) (declare-fun l285c () Int) (assert (= l285m (and l283m l284m))) (assert (and (or l285m l283m (>= l285c l283c)) (or l285m l284m (>= l285c l284c)))) (assert (or l285m (and (not l283m) (= l285c l283c)) (and (not l284m) (= l285c l284c)))) (define-fun f167m () Bool l285m) (define-fun f167c () Int l285c) (declare-fun l286m () Bool) (declare-fun l286c () Int) (assert (= l286m (or f38m f158m))) (assert (or l286m (= l286c (+ f38c f158c)))) (declare-fun l287m () Bool) (declare-fun l287c () Int) (assert (= l287m (or f39m f160m))) (assert (or l287m (= l287c (+ f39c f160c)))) (declare-fun l288m () Bool) (declare-fun l288c () Int) (assert (= l288m (and l286m l287m))) (assert (and (or l288m l286m (>= l288c l286c)) (or l288m l287m (>= l288c l287c)))) (assert (or l288m (and (not l286m) (= l288c l286c)) (and (not l287m) (= l288c l287c)))) (define-fun f168m () Bool l288m) (define-fun f168c () Int l288c) (declare-fun l289m () Bool) (declare-fun l289c () Int) (assert (= l289m (or f38m f159m))) (assert (or l289m (= l289c (+ f38c f159c)))) (declare-fun l290m () Bool) (declare-fun l290c () Int) (assert (= l290m (or f39m f161m))) (assert (or l290m (= l290c (+ f39c f161c)))) (declare-fun l291m () Bool) (declare-fun l291c () Int) (assert (= l291m (and l289m l290m))) (assert (and (or l291m l289m (>= l291c l289c)) (or l291m l290m (>= l291c l290c)))) (assert (or l291m (and (not l289m) (= l291c l289c)) (and (not l290m) (= l291c l290c)))) (define-fun f169m () Bool l291m) (define-fun f169c () Int l291c) (declare-fun l292m () Bool) (declare-fun l292c () Int) (assert (= l292m (or f36m f164m))) (assert (or l292m (= l292c (+ f36c f164c)))) (declare-fun l293m () Bool) (declare-fun l293c () Int) (assert (= l293m (or f37m f165m))) (assert (or l293m (= l293c (+ f37c f165c)))) (declare-fun l294m () Bool) (declare-fun l294c () Int) (assert (= l294m (and l292m l293m))) (assert (and (or l294m l292m (>= l294c l292c)) (or l294m l293m (>= l294c l293c)))) (assert (or l294m (and (not l292m) (= l294c l292c)) (and (not l293m) (= l294c l293c)))) (define-fun f170m () Bool l294m) (define-fun f170c () Int l294c) (declare-fun l295m () Bool) (declare-fun l295c () Int) (assert (= l295m (or f38m f164m))) (assert (or l295m (= l295c (+ f38c f164c)))) (declare-fun l296m () Bool) (declare-fun l296c () Int) (assert (= l296m (or f39m f165m))) (assert (or l296m (= l296c (+ f39c f165c)))) (declare-fun l297m () Bool) (declare-fun l297c () Int) (assert (= l297m (and l295m l296m))) (assert (and (or l297m l295m (>= l297c l295c)) (or l297m l296m (>= l297c l296c)))) (assert (or l297m (and (not l295m) (= l297c l295c)) (and (not l296m) (= l297c l296c)))) (define-fun f171m () Bool l297m) (define-fun f171c () Int l297c) (declare-fun l298m () Bool) (declare-fun l298c () Int) (assert (= l298m (and f40m f170m))) (assert (and (or l298m f40m (>= l298c f40c)) (or l298m f170m (>= l298c f170c)))) (assert (or l298m (and (not f40m) (= l298c f40c)) (and (not f170m) (= l298c f170c)))) (define-fun f172m () Bool l298m) (define-fun f172c () Int l298c) (declare-fun l299m () Bool) (declare-fun l299c () Int) (assert (= l299m (and f41m f171m))) (assert (and (or l299m f41m (>= l299c f41c)) (or l299m f171m (>= l299c f171c)))) (assert (or l299m (and (not f41m) (= l299c f41c)) (and (not f171m) (= l299c f171c)))) (define-fun f173m () Bool l299m) (define-fun f173c () Int l299c) (declare-fun l300m () Bool) (declare-fun l300c () Int) (assert (= l300m (or f36m f166m))) (assert (or l300m (= l300c (+ f36c f166c)))) (declare-fun l301m () Bool) (declare-fun l301c () Int) (assert (= l301m (or f37m f168m))) (assert (or l301m (= l301c (+ f37c f168c)))) (declare-fun l302m () Bool) (declare-fun l302c () Int) (assert (= l302m (and l300m l301m))) (assert (and (or l302m l300m (>= l302c l300c)) (or l302m l301m (>= l302c l301c)))) (assert (or l302m (and (not l300m) (= l302c l300c)) (and (not l301m) (= l302c l301c)))) (define-fun f174m () Bool l302m) (define-fun f174c () Int l302c) (declare-fun l303m () Bool) (declare-fun l303c () Int) (assert (= l303m (or f36m f167m))) (assert (or l303m (= l303c (+ f36c f167c)))) (declare-fun l304m () Bool) (declare-fun l304c () Int) (assert (= l304m (or f37m f169m))) (assert (or l304m (= l304c (+ f37c f169c)))) (declare-fun l305m () Bool) (declare-fun l305c () Int) (assert (= l305m (and l303m l304m))) (assert (and (or l305m l303m (>= l305c l303c)) (or l305m l304m (>= l305c l304c)))) (assert (or l305m (and (not l303m) (= l305c l303c)) (and (not l304m) (= l305c l304c)))) (define-fun f175m () Bool l305m) (define-fun f175c () Int l305c) (declare-fun l306m () Bool) (declare-fun l306c () Int) (assert (= l306m (or f38m f166m))) (assert (or l306m (= l306c (+ f38c f166c)))) (declare-fun l307m () Bool) (declare-fun l307c () Int) (assert (= l307m (or f39m f168m))) (assert (or l307m (= l307c (+ f39c f168c)))) (declare-fun l308m () Bool) (declare-fun l308c () Int) (assert (= l308m (and l306m l307m))) (assert (and (or l308m l306m (>= l308c l306c)) (or l308m l307m (>= l308c l307c)))) (assert (or l308m (and (not l306m) (= l308c l306c)) (and (not l307m) (= l308c l307c)))) (define-fun f176m () Bool l308m) (define-fun f176c () Int l308c) (declare-fun l309m () Bool) (declare-fun l309c () Int) (assert (= l309m (or f38m f167m))) (assert (or l309m (= l309c (+ f38c f167c)))) (declare-fun l310m () Bool) (declare-fun l310c () Int) (assert (= l310m (or f39m f169m))) (assert (or l310m (= l310c (+ f39c f169c)))) (declare-fun l311m () Bool) (declare-fun l311c () Int) (assert (= l311m (and l309m l310m))) (assert (and (or l311m l309m (>= l311c l309c)) (or l311m l310m (>= l311c l310c)))) (assert (or l311m (and (not l309m) (= l311c l309c)) (and (not l310m) (= l311c l310c)))) (define-fun f177m () Bool l311m) (define-fun f177c () Int l311c) (declare-fun l312m () Bool) (declare-fun l312c () Int) (assert (= l312m (or f36m f172m))) (assert (or l312m (= l312c (+ f36c f172c)))) (declare-fun l313m () Bool) (declare-fun l313c () Int) (assert (= l313m (or f37m f173m))) (assert (or l313m (= l313c (+ f37c f173c)))) (declare-fun l314m () Bool) (declare-fun l314c () Int) (assert (= l314m (and l312m l313m))) (assert (and (or l314m l312m (>= l314c l312c)) (or l314m l313m (>= l314c l313c)))) (assert (or l314m (and (not l312m) (= l314c l312c)) (and (not l313m) (= l314c l313c)))) (define-fun f178m () Bool l314m) (define-fun f178c () Int l314c) (declare-fun l315m () Bool) (declare-fun l315c () Int) (assert (= l315m (or f38m f172m))) (assert (or l315m (= l315c (+ f38c f172c)))) (declare-fun l316m () Bool) (declare-fun l316c () Int) (assert (= l316m (or f39m f173m))) (assert (or l316m (= l316c (+ f39c f173c)))) (declare-fun l317m () Bool) (declare-fun l317c () Int) (assert (= l317m (and l315m l316m))) (assert (and (or l317m l315m (>= l317c l315c)) (or l317m l316m (>= l317c l316c)))) (assert (or l317m (and (not l315m) (= l317c l315c)) (and (not l316m) (= l317c l316c)))) (define-fun f179m () Bool l317m) (define-fun f179c () Int l317c) (declare-fun l318m () Bool) (declare-fun l318c () Int) (assert (= l318m (and f40m f178m))) (assert (and (or l318m f40m (>= l318c f40c)) (or l318m f178m (>= l318c f178c)))) (assert (or l318m (and (not f40m) (= l318c f40c)) (and (not f178m) (= l318c f178c)))) (define-fun f180m () Bool l318m) (define-fun f180c () Int l318c) (declare-fun l319m () Bool) (declare-fun l319c () Int) (assert (= l319m (and f41m f179m))) (assert (and (or l319m f41m (>= l319c f41c)) (or l319m f179m (>= l319c f179c)))) (assert (or l319m (and (not f41m) (= l319c f41c)) (and (not f179m) (= l319c f179c)))) (define-fun f181m () Bool l319m) (define-fun f181c () Int l319c) (declare-fun l320m () Bool) (declare-fun l320c () Int) (assert (= l320m (or f18m f36m))) (assert (or l320m (= l320c (+ f18c f36c)))) (declare-fun l321m () Bool) (declare-fun l321c () Int) (assert (= l321m (or f19m f38m))) (assert (or l321m (= l321c (+ f19c f38c)))) (declare-fun l322m () Bool) (declare-fun l322c () Int) (assert (= l322m (and l320m l321m))) (assert (and (or l322m l320m (>= l322c l320c)) (or l322m l321m (>= l322c l321c)))) (assert (or l322m (and (not l320m) (= l322c l320c)) (and (not l321m) (= l322c l321c)))) (define-fun f182m () Bool l322m) (define-fun f182c () Int l322c) (declare-fun l323m () Bool) (declare-fun l323c () Int) (assert (= l323m (or f18m f37m))) (assert (or l323m (= l323c (+ f18c f37c)))) (declare-fun l324m () Bool) (declare-fun l324c () Int) (assert (= l324m (or f19m f39m))) (assert (or l324m (= l324c (+ f19c f39c)))) (declare-fun l325m () Bool) (declare-fun l325c () Int) (assert (= l325m (and l323m l324m))) (assert (and (or l325m l323m (>= l325c l323c)) (or l325m l324m (>= l325c l324c)))) (assert (or l325m (and (not l323m) (= l325c l323c)) (and (not l324m) (= l325c l324c)))) (define-fun f183m () Bool l325m) (define-fun f183c () Int l325c) (declare-fun l326m () Bool) (declare-fun l326c () Int) (assert (= l326m (or f20m f36m))) (assert (or l326m (= l326c (+ f20c f36c)))) (declare-fun l327m () Bool) (declare-fun l327c () Int) (assert (= l327m (or f21m f38m))) (assert (or l327m (= l327c (+ f21c f38c)))) (declare-fun l328m () Bool) (declare-fun l328c () Int) (assert (= l328m (and l326m l327m))) (assert (and (or l328m l326m (>= l328c l326c)) (or l328m l327m (>= l328c l327c)))) (assert (or l328m (and (not l326m) (= l328c l326c)) (and (not l327m) (= l328c l327c)))) (define-fun f184m () Bool l328m) (define-fun f184c () Int l328c) (declare-fun l329m () Bool) (declare-fun l329c () Int) (assert (= l329m (or f20m f37m))) (assert (or l329m (= l329c (+ f20c f37c)))) (declare-fun l330m () Bool) (declare-fun l330c () Int) (assert (= l330m (or f21m f39m))) (assert (or l330m (= l330c (+ f21c f39c)))) (declare-fun l331m () Bool) (declare-fun l331c () Int) (assert (= l331m (and l329m l330m))) (assert (and (or l331m l329m (>= l331c l329c)) (or l331m l330m (>= l331c l330c)))) (assert (or l331m (and (not l329m) (= l331c l329c)) (and (not l330m) (= l331c l330c)))) (define-fun f185m () Bool l331m) (define-fun f185c () Int l331c) (declare-fun l332m () Bool) (declare-fun l332c () Int) (assert (= l332m (or f18m f40m))) (assert (or l332m (= l332c (+ f18c f40c)))) (declare-fun l333m () Bool) (declare-fun l333c () Int) (assert (= l333m (or f19m f41m))) (assert (or l333m (= l333c (+ f19c f41c)))) (declare-fun l334m () Bool) (declare-fun l334c () Int) (assert (= l334m (and l332m l333m))) (assert (and (or l334m l332m (>= l334c l332c)) (or l334m l333m (>= l334c l333c)))) (assert (or l334m (and (not l332m) (= l334c l332c)) (and (not l333m) (= l334c l333c)))) (define-fun f186m () Bool l334m) (define-fun f186c () Int l334c) (declare-fun l335m () Bool) (declare-fun l335c () Int) (assert (= l335m (or f20m f40m))) (assert (or l335m (= l335c (+ f20c f40c)))) (declare-fun l336m () Bool) (declare-fun l336c () Int) (assert (= l336m (or f21m f41m))) (assert (or l336m (= l336c (+ f21c f41c)))) (declare-fun l337m () Bool) (declare-fun l337c () Int) (assert (= l337m (and l335m l336m))) (assert (and (or l337m l335m (>= l337c l335c)) (or l337m l336m (>= l337c l336c)))) (assert (or l337m (and (not l335m) (= l337c l335c)) (and (not l336m) (= l337c l336c)))) (define-fun f187m () Bool l337m) (define-fun f187c () Int l337c) (declare-fun l338m () Bool) (declare-fun l338c () Int) (assert (= l338m (and f22m f186m))) (assert (and (or l338m f22m (>= l338c f22c)) (or l338m f186m (>= l338c f186c)))) (assert (or l338m (and (not f22m) (= l338c f22c)) (and (not f186m) (= l338c f186c)))) (define-fun f188m () Bool l338m) (define-fun f188c () Int l338c) (declare-fun l339m () Bool) (declare-fun l339c () Int) (assert (= l339m (and f23m f187m))) (assert (and (or l339m f23m (>= l339c f23c)) (or l339m f187m (>= l339c f187c)))) (assert (or l339m (and (not f23m) (= l339c f23c)) (and (not f187m) (= l339c f187c)))) (define-fun f189m () Bool l339m) (define-fun f189c () Int l339c) (declare-fun l340m () Bool) (declare-fun l340c () Int) (assert (= l340m (or f36m f36m))) (assert (or l340m (= l340c (+ f36c f36c)))) (declare-fun l341m () Bool) (declare-fun l341c () Int) (assert (= l341m (or f37m f38m))) (assert (or l341m (= l341c (+ f37c f38c)))) (declare-fun l342m () Bool) (declare-fun l342c () Int) (assert (= l342m (and l340m l341m))) (assert (and (or l342m l340m (>= l342c l340c)) (or l342m l341m (>= l342c l341c)))) (assert (or l342m (and (not l340m) (= l342c l340c)) (and (not l341m) (= l342c l341c)))) (define-fun f190m () Bool l342m) (define-fun f190c () Int l342c) (declare-fun l343m () Bool) (declare-fun l343c () Int) (assert (= l343m (or f36m f37m))) (assert (or l343m (= l343c (+ f36c f37c)))) (declare-fun l344m () Bool) (declare-fun l344c () Int) (assert (= l344m (or f37m f39m))) (assert (or l344m (= l344c (+ f37c f39c)))) (declare-fun l345m () Bool) (declare-fun l345c () Int) (assert (= l345m (and l343m l344m))) (assert (and (or l345m l343m (>= l345c l343c)) (or l345m l344m (>= l345c l344c)))) (assert (or l345m (and (not l343m) (= l345c l343c)) (and (not l344m) (= l345c l344c)))) (define-fun f191m () Bool l345m) (define-fun f191c () Int l345c) (declare-fun l346m () Bool) (declare-fun l346c () Int) (assert (= l346m (or f38m f36m))) (assert (or l346m (= l346c (+ f38c f36c)))) (declare-fun l347m () Bool) (declare-fun l347c () Int) (assert (= l347m (or f39m f38m))) (assert (or l347m (= l347c (+ f39c f38c)))) (declare-fun l348m () Bool) (declare-fun l348c () Int) (assert (= l348m (and l346m l347m))) (assert (and (or l348m l346m (>= l348c l346c)) (or l348m l347m (>= l348c l347c)))) (assert (or l348m (and (not l346m) (= l348c l346c)) (and (not l347m) (= l348c l347c)))) (define-fun f192m () Bool l348m) (define-fun f192c () Int l348c) (declare-fun l349m () Bool) (declare-fun l349c () Int) (assert (= l349m (or f38m f37m))) (assert (or l349m (= l349c (+ f38c f37c)))) (declare-fun l350m () Bool) (declare-fun l350c () Int) (assert (= l350m (or f39m f39m))) (assert (or l350m (= l350c (+ f39c f39c)))) (declare-fun l351m () Bool) (declare-fun l351c () Int) (assert (= l351m (and l349m l350m))) (assert (and (or l351m l349m (>= l351c l349c)) (or l351m l350m (>= l351c l350c)))) (assert (or l351m (and (not l349m) (= l351c l349c)) (and (not l350m) (= l351c l350c)))) (define-fun f193m () Bool l351m) (define-fun f193c () Int l351c) (declare-fun l352m () Bool) (declare-fun l352c () Int) (assert (= l352m (or f36m f40m))) (assert (or l352m (= l352c (+ f36c f40c)))) (declare-fun l353m () Bool) (declare-fun l353c () Int) (assert (= l353m (or f37m f41m))) (assert (or l353m (= l353c (+ f37c f41c)))) (declare-fun l354m () Bool) (declare-fun l354c () Int) (assert (= l354m (and l352m l353m))) (assert (and (or l354m l352m (>= l354c l352c)) (or l354m l353m (>= l354c l353c)))) (assert (or l354m (and (not l352m) (= l354c l352c)) (and (not l353m) (= l354c l353c)))) (define-fun f194m () Bool l354m) (define-fun f194c () Int l354c) (declare-fun l355m () Bool) (declare-fun l355c () Int) (assert (= l355m (or f38m f40m))) (assert (or l355m (= l355c (+ f38c f40c)))) (declare-fun l356m () Bool) (declare-fun l356c () Int) (assert (= l356m (or f39m f41m))) (assert (or l356m (= l356c (+ f39c f41c)))) (declare-fun l357m () Bool) (declare-fun l357c () Int) (assert (= l357m (and l355m l356m))) (assert (and (or l357m l355m (>= l357c l355c)) (or l357m l356m (>= l357c l356c)))) (assert (or l357m (and (not l355m) (= l357c l355c)) (and (not l356m) (= l357c l356c)))) (define-fun f195m () Bool l357m) (define-fun f195c () Int l357c) (declare-fun l358m () Bool) (declare-fun l358c () Int) (assert (= l358m (and f40m f194m))) (assert (and (or l358m f40m (>= l358c f40c)) (or l358m f194m (>= l358c f194c)))) (assert (or l358m (and (not f40m) (= l358c f40c)) (and (not f194m) (= l358c f194c)))) (define-fun f196m () Bool l358m) (define-fun f196c () Int l358c) (declare-fun l359m () Bool) (declare-fun l359c () Int) (assert (= l359m (and f41m f195m))) (assert (and (or l359m f41m (>= l359c f41c)) (or l359m f195m (>= l359c f195c)))) (assert (or l359m (and (not f41m) (= l359c f41c)) (and (not f195m) (= l359c f195c)))) (define-fun f197m () Bool l359m) (define-fun f197c () Int l359c) (declare-fun l360m () Bool) (declare-fun l360c () Int) (assert (= l360m (or f30m f190m))) (assert (or l360m (= l360c (+ f30c f190c)))) (declare-fun l361m () Bool) (declare-fun l361c () Int) (assert (= l361m (or f31m f192m))) (assert (or l361m (= l361c (+ f31c f192c)))) (declare-fun l362m () Bool) (declare-fun l362c () Int) (assert (= l362m (and l360m l361m))) (assert (and (or l362m l360m (>= l362c l360c)) (or l362m l361m (>= l362c l361c)))) (assert (or l362m (and (not l360m) (= l362c l360c)) (and (not l361m) (= l362c l361c)))) (define-fun f198m () Bool l362m) (define-fun f198c () Int l362c) (declare-fun l363m () Bool) (declare-fun l363c () Int) (assert (= l363m (or f30m f191m))) (assert (or l363m (= l363c (+ f30c f191c)))) (declare-fun l364m () Bool) (declare-fun l364c () Int) (assert (= l364m (or f31m f193m))) (assert (or l364m (= l364c (+ f31c f193c)))) (declare-fun l365m () Bool) (declare-fun l365c () Int) (assert (= l365m (and l363m l364m))) (assert (and (or l365m l363m (>= l365c l363c)) (or l365m l364m (>= l365c l364c)))) (assert (or l365m (and (not l363m) (= l365c l363c)) (and (not l364m) (= l365c l364c)))) (define-fun f199m () Bool l365m) (define-fun f199c () Int l365c) (declare-fun l366m () Bool) (declare-fun l366c () Int) (assert (= l366m (or f32m f190m))) (assert (or l366m (= l366c (+ f32c f190c)))) (declare-fun l367m () Bool) (declare-fun l367c () Int) (assert (= l367m (or f33m f192m))) (assert (or l367m (= l367c (+ f33c f192c)))) (declare-fun l368m () Bool) (declare-fun l368c () Int) (assert (= l368m (and l366m l367m))) (assert (and (or l368m l366m (>= l368c l366c)) (or l368m l367m (>= l368c l367c)))) (assert (or l368m (and (not l366m) (= l368c l366c)) (and (not l367m) (= l368c l367c)))) (define-fun f200m () Bool l368m) (define-fun f200c () Int l368c) (declare-fun l369m () Bool) (declare-fun l369c () Int) (assert (= l369m (or f32m f191m))) (assert (or l369m (= l369c (+ f32c f191c)))) (declare-fun l370m () Bool) (declare-fun l370c () Int) (assert (= l370m (or f33m f193m))) (assert (or l370m (= l370c (+ f33c f193c)))) (declare-fun l371m () Bool) (declare-fun l371c () Int) (assert (= l371m (and l369m l370m))) (assert (and (or l371m l369m (>= l371c l369c)) (or l371m l370m (>= l371c l370c)))) (assert (or l371m (and (not l369m) (= l371c l369c)) (and (not l370m) (= l371c l370c)))) (define-fun f201m () Bool l371m) (define-fun f201c () Int l371c) (declare-fun l372m () Bool) (declare-fun l372c () Int) (assert (= l372m (or f30m f196m))) (assert (or l372m (= l372c (+ f30c f196c)))) (declare-fun l373m () Bool) (declare-fun l373c () Int) (assert (= l373m (or f31m f197m))) (assert (or l373m (= l373c (+ f31c f197c)))) (declare-fun l374m () Bool) (declare-fun l374c () Int) (assert (= l374m (and l372m l373m))) (assert (and (or l374m l372m (>= l374c l372c)) (or l374m l373m (>= l374c l373c)))) (assert (or l374m (and (not l372m) (= l374c l372c)) (and (not l373m) (= l374c l373c)))) (define-fun f202m () Bool l374m) (define-fun f202c () Int l374c) (declare-fun l375m () Bool) (declare-fun l375c () Int) (assert (= l375m (or f32m f196m))) (assert (or l375m (= l375c (+ f32c f196c)))) (declare-fun l376m () Bool) (declare-fun l376c () Int) (assert (= l376m (or f33m f197m))) (assert (or l376m (= l376c (+ f33c f197c)))) (declare-fun l377m () Bool) (declare-fun l377c () Int) (assert (= l377m (and l375m l376m))) (assert (and (or l377m l375m (>= l377c l375c)) (or l377m l376m (>= l377c l376c)))) (assert (or l377m (and (not l375m) (= l377c l375c)) (and (not l376m) (= l377c l376c)))) (define-fun f203m () Bool l377m) (define-fun f203c () Int l377c) (declare-fun l378m () Bool) (declare-fun l378c () Int) (assert (= l378m (and f34m f202m))) (assert (and (or l378m f34m (>= l378c f34c)) (or l378m f202m (>= l378c f202c)))) (assert (or l378m (and (not f34m) (= l378c f34c)) (and (not f202m) (= l378c f202c)))) (define-fun f204m () Bool l378m) (define-fun f204c () Int l378c) (declare-fun l379m () Bool) (declare-fun l379c () Int) (assert (= l379m (and f35m f203m))) (assert (and (or l379m f35m (>= l379c f35c)) (or l379m f203m (>= l379c f203c)))) (assert (or l379m (and (not f35m) (= l379c f35c)) (and (not f203m) (= l379c f203c)))) (define-fun f205m () Bool l379m) (define-fun f205c () Int l379c) (declare-fun l380m () Bool) (declare-fun l380c () Int) (assert (= l380m (or f36m f18m))) (assert (or l380m (= l380c (+ f36c f18c)))) (declare-fun l381m () Bool) (declare-fun l381c () Int) (assert (= l381m (or f37m f20m))) (assert (or l381m (= l381c (+ f37c f20c)))) (declare-fun l382m () Bool) (declare-fun l382c () Int) (assert (= l382m (and l380m l381m))) (assert (and (or l382m l380m (>= l382c l380c)) (or l382m l381m (>= l382c l381c)))) (assert (or l382m (and (not l380m) (= l382c l380c)) (and (not l381m) (= l382c l381c)))) (define-fun f206m () Bool l382m) (define-fun f206c () Int l382c) (declare-fun l383m () Bool) (declare-fun l383c () Int) (assert (= l383m (or f36m f19m))) (assert (or l383m (= l383c (+ f36c f19c)))) (declare-fun l384m () Bool) (declare-fun l384c () Int) (assert (= l384m (or f37m f21m))) (assert (or l384m (= l384c (+ f37c f21c)))) (declare-fun l385m () Bool) (declare-fun l385c () Int) (assert (= l385m (and l383m l384m))) (assert (and (or l385m l383m (>= l385c l383c)) (or l385m l384m (>= l385c l384c)))) (assert (or l385m (and (not l383m) (= l385c l383c)) (and (not l384m) (= l385c l384c)))) (define-fun f207m () Bool l385m) (define-fun f207c () Int l385c) (declare-fun l386m () Bool) (declare-fun l386c () Int) (assert (= l386m (or f38m f18m))) (assert (or l386m (= l386c (+ f38c f18c)))) (declare-fun l387m () Bool) (declare-fun l387c () Int) (assert (= l387m (or f39m f20m))) (assert (or l387m (= l387c (+ f39c f20c)))) (declare-fun l388m () Bool) (declare-fun l388c () Int) (assert (= l388m (and l386m l387m))) (assert (and (or l388m l386m (>= l388c l386c)) (or l388m l387m (>= l388c l387c)))) (assert (or l388m (and (not l386m) (= l388c l386c)) (and (not l387m) (= l388c l387c)))) (define-fun f208m () Bool l388m) (define-fun f208c () Int l388c) (declare-fun l389m () Bool) (declare-fun l389c () Int) (assert (= l389m (or f38m f19m))) (assert (or l389m (= l389c (+ f38c f19c)))) (declare-fun l390m () Bool) (declare-fun l390c () Int) (assert (= l390m (or f39m f21m))) (assert (or l390m (= l390c (+ f39c f21c)))) (declare-fun l391m () Bool) (declare-fun l391c () Int) (assert (= l391m (and l389m l390m))) (assert (and (or l391m l389m (>= l391c l389c)) (or l391m l390m (>= l391c l390c)))) (assert (or l391m (and (not l389m) (= l391c l389c)) (and (not l390m) (= l391c l390c)))) (define-fun f209m () Bool l391m) (define-fun f209c () Int l391c) (declare-fun l392m () Bool) (declare-fun l392c () Int) (assert (= l392m (or f36m f22m))) (assert (or l392m (= l392c (+ f36c f22c)))) (declare-fun l393m () Bool) (declare-fun l393c () Int) (assert (= l393m (or f37m f23m))) (assert (or l393m (= l393c (+ f37c f23c)))) (declare-fun l394m () Bool) (declare-fun l394c () Int) (assert (= l394m (and l392m l393m))) (assert (and (or l394m l392m (>= l394c l392c)) (or l394m l393m (>= l394c l393c)))) (assert (or l394m (and (not l392m) (= l394c l392c)) (and (not l393m) (= l394c l393c)))) (define-fun f210m () Bool l394m) (define-fun f210c () Int l394c) (declare-fun l395m () Bool) (declare-fun l395c () Int) (assert (= l395m (or f38m f22m))) (assert (or l395m (= l395c (+ f38c f22c)))) (declare-fun l396m () Bool) (declare-fun l396c () Int) (assert (= l396m (or f39m f23m))) (assert (or l396m (= l396c (+ f39c f23c)))) (declare-fun l397m () Bool) (declare-fun l397c () Int) (assert (= l397m (and l395m l396m))) (assert (and (or l397m l395m (>= l397c l395c)) (or l397m l396m (>= l397c l396c)))) (assert (or l397m (and (not l395m) (= l397c l395c)) (and (not l396m) (= l397c l396c)))) (define-fun f211m () Bool l397m) (define-fun f211c () Int l397c) (declare-fun l398m () Bool) (declare-fun l398c () Int) (assert (= l398m (and f40m f210m))) (assert (and (or l398m f40m (>= l398c f40c)) (or l398m f210m (>= l398c f210c)))) (assert (or l398m (and (not f40m) (= l398c f40c)) (and (not f210m) (= l398c f210c)))) (define-fun f212m () Bool l398m) (define-fun f212c () Int l398c) (declare-fun l399m () Bool) (declare-fun l399c () Int) (assert (= l399m (and f41m f211m))) (assert (and (or l399m f41m (>= l399c f41c)) (or l399m f211m (>= l399c f211c)))) (assert (or l399m (and (not f41m) (= l399c f41c)) (and (not f211m) (= l399c f211c)))) (define-fun f213m () Bool l399m) (define-fun f213c () Int l399c) (declare-fun l400m () Bool) (declare-fun l400c () Int) (assert (= l400m (or f36m f206m))) (assert (or l400m (= l400c (+ f36c f206c)))) (declare-fun l401m () Bool) (declare-fun l401c () Int) (assert (= l401m (or f37m f208m))) (assert (or l401m (= l401c (+ f37c f208c)))) (declare-fun l402m () Bool) (declare-fun l402c () Int) (assert (= l402m (and l400m l401m))) (assert (and (or l402m l400m (>= l402c l400c)) (or l402m l401m (>= l402c l401c)))) (assert (or l402m (and (not l400m) (= l402c l400c)) (and (not l401m) (= l402c l401c)))) (define-fun f214m () Bool l402m) (define-fun f214c () Int l402c) (declare-fun l403m () Bool) (declare-fun l403c () Int) (assert (= l403m (or f36m f207m))) (assert (or l403m (= l403c (+ f36c f207c)))) (declare-fun l404m () Bool) (declare-fun l404c () Int) (assert (= l404m (or f37m f209m))) (assert (or l404m (= l404c (+ f37c f209c)))) (declare-fun l405m () Bool) (declare-fun l405c () Int) (assert (= l405m (and l403m l404m))) (assert (and (or l405m l403m (>= l405c l403c)) (or l405m l404m (>= l405c l404c)))) (assert (or l405m (and (not l403m) (= l405c l403c)) (and (not l404m) (= l405c l404c)))) (define-fun f215m () Bool l405m) (define-fun f215c () Int l405c) (declare-fun l406m () Bool) (declare-fun l406c () Int) (assert (= l406m (or f38m f206m))) (assert (or l406m (= l406c (+ f38c f206c)))) (declare-fun l407m () Bool) (declare-fun l407c () Int) (assert (= l407m (or f39m f208m))) (assert (or l407m (= l407c (+ f39c f208c)))) (declare-fun l408m () Bool) (declare-fun l408c () Int) (assert (= l408m (and l406m l407m))) (assert (and (or l408m l406m (>= l408c l406c)) (or l408m l407m (>= l408c l407c)))) (assert (or l408m (and (not l406m) (= l408c l406c)) (and (not l407m) (= l408c l407c)))) (define-fun f216m () Bool l408m) (define-fun f216c () Int l408c) (declare-fun l409m () Bool) (declare-fun l409c () Int) (assert (= l409m (or f38m f207m))) (assert (or l409m (= l409c (+ f38c f207c)))) (declare-fun l410m () Bool) (declare-fun l410c () Int) (assert (= l410m (or f39m f209m))) (assert (or l410m (= l410c (+ f39c f209c)))) (declare-fun l411m () Bool) (declare-fun l411c () Int) (assert (= l411m (and l409m l410m))) (assert (and (or l411m l409m (>= l411c l409c)) (or l411m l410m (>= l411c l410c)))) (assert (or l411m (and (not l409m) (= l411c l409c)) (and (not l410m) (= l411c l410c)))) (define-fun f217m () Bool l411m) (define-fun f217c () Int l411c) (declare-fun l412m () Bool) (declare-fun l412c () Int) (assert (= l412m (or f36m f212m))) (assert (or l412m (= l412c (+ f36c f212c)))) (declare-fun l413m () Bool) (declare-fun l413c () Int) (assert (= l413m (or f37m f213m))) (assert (or l413m (= l413c (+ f37c f213c)))) (declare-fun l414m () Bool) (declare-fun l414c () Int) (assert (= l414m (and l412m l413m))) (assert (and (or l414m l412m (>= l414c l412c)) (or l414m l413m (>= l414c l413c)))) (assert (or l414m (and (not l412m) (= l414c l412c)) (and (not l413m) (= l414c l413c)))) (define-fun f218m () Bool l414m) (define-fun f218c () Int l414c) (declare-fun l415m () Bool) (declare-fun l415c () Int) (assert (= l415m (or f38m f212m))) (assert (or l415m (= l415c (+ f38c f212c)))) (declare-fun l416m () Bool) (declare-fun l416c () Int) (assert (= l416m (or f39m f213m))) (assert (or l416m (= l416c (+ f39c f213c)))) (declare-fun l417m () Bool) (declare-fun l417c () Int) (assert (= l417m (and l415m l416m))) (assert (and (or l417m l415m (>= l417c l415c)) (or l417m l416m (>= l417c l416c)))) (assert (or l417m (and (not l415m) (= l417c l415c)) (and (not l416m) (= l417c l416c)))) (define-fun f219m () Bool l417m) (define-fun f219c () Int l417c) (declare-fun l418m () Bool) (declare-fun l418c () Int) (assert (= l418m (and f40m f218m))) (assert (and (or l418m f40m (>= l418c f40c)) (or l418m f218m (>= l418c f218c)))) (assert (or l418m (and (not f40m) (= l418c f40c)) (and (not f218m) (= l418c f218c)))) (define-fun f220m () Bool l418m) (define-fun f220c () Int l418c) (declare-fun l419m () Bool) (declare-fun l419c () Int) (assert (= l419m (and f41m f219m))) (assert (and (or l419m f41m (>= l419c f41c)) (or l419m f219m (>= l419c f219c)))) (assert (or l419m (and (not f41m) (= l419c f41c)) (and (not f219m) (= l419c f219c)))) (define-fun f221m () Bool l419m) (define-fun f221c () Int l419c) (declare-fun l420m () Bool) (declare-fun l420c () Int) (assert (= l420m (or f30m f214m))) (assert (or l420m (= l420c (+ f30c f214c)))) (declare-fun l421m () Bool) (declare-fun l421c () Int) (assert (= l421m (or f31m f216m))) (assert (or l421m (= l421c (+ f31c f216c)))) (declare-fun l422m () Bool) (declare-fun l422c () Int) (assert (= l422m (and l420m l421m))) (assert (and (or l422m l420m (>= l422c l420c)) (or l422m l421m (>= l422c l421c)))) (assert (or l422m (and (not l420m) (= l422c l420c)) (and (not l421m) (= l422c l421c)))) (define-fun f222m () Bool l422m) (define-fun f222c () Int l422c) (declare-fun l423m () Bool) (declare-fun l423c () Int) (assert (= l423m (or f30m f215m))) (assert (or l423m (= l423c (+ f30c f215c)))) (declare-fun l424m () Bool) (declare-fun l424c () Int) (assert (= l424m (or f31m f217m))) (assert (or l424m (= l424c (+ f31c f217c)))) (declare-fun l425m () Bool) (declare-fun l425c () Int) (assert (= l425m (and l423m l424m))) (assert (and (or l425m l423m (>= l425c l423c)) (or l425m l424m (>= l425c l424c)))) (assert (or l425m (and (not l423m) (= l425c l423c)) (and (not l424m) (= l425c l424c)))) (define-fun f223m () Bool l425m) (define-fun f223c () Int l425c) (declare-fun l426m () Bool) (declare-fun l426c () Int) (assert (= l426m (or f32m f214m))) (assert (or l426m (= l426c (+ f32c f214c)))) (declare-fun l427m () Bool) (declare-fun l427c () Int) (assert (= l427m (or f33m f216m))) (assert (or l427m (= l427c (+ f33c f216c)))) (declare-fun l428m () Bool) (declare-fun l428c () Int) (assert (= l428m (and l426m l427m))) (assert (and (or l428m l426m (>= l428c l426c)) (or l428m l427m (>= l428c l427c)))) (assert (or l428m (and (not l426m) (= l428c l426c)) (and (not l427m) (= l428c l427c)))) (define-fun f224m () Bool l428m) (define-fun f224c () Int l428c) (declare-fun l429m () Bool) (declare-fun l429c () Int) (assert (= l429m (or f32m f215m))) (assert (or l429m (= l429c (+ f32c f215c)))) (declare-fun l430m () Bool) (declare-fun l430c () Int) (assert (= l430m (or f33m f217m))) (assert (or l430m (= l430c (+ f33c f217c)))) (declare-fun l431m () Bool) (declare-fun l431c () Int) (assert (= l431m (and l429m l430m))) (assert (and (or l431m l429m (>= l431c l429c)) (or l431m l430m (>= l431c l430c)))) (assert (or l431m (and (not l429m) (= l431c l429c)) (and (not l430m) (= l431c l430c)))) (define-fun f225m () Bool l431m) (define-fun f225c () Int l431c) (declare-fun l432m () Bool) (declare-fun l432c () Int) (assert (= l432m (or f30m f220m))) (assert (or l432m (= l432c (+ f30c f220c)))) (declare-fun l433m () Bool) (declare-fun l433c () Int) (assert (= l433m (or f31m f221m))) (assert (or l433m (= l433c (+ f31c f221c)))) (declare-fun l434m () Bool) (declare-fun l434c () Int) (assert (= l434m (and l432m l433m))) (assert (and (or l434m l432m (>= l434c l432c)) (or l434m l433m (>= l434c l433c)))) (assert (or l434m (and (not l432m) (= l434c l432c)) (and (not l433m) (= l434c l433c)))) (define-fun f226m () Bool l434m) (define-fun f226c () Int l434c) (declare-fun l435m () Bool) (declare-fun l435c () Int) (assert (= l435m (or f32m f220m))) (assert (or l435m (= l435c (+ f32c f220c)))) (declare-fun l436m () Bool) (declare-fun l436c () Int) (assert (= l436m (or f33m f221m))) (assert (or l436m (= l436c (+ f33c f221c)))) (declare-fun l437m () Bool) (declare-fun l437c () Int) (assert (= l437m (and l435m l436m))) (assert (and (or l437m l435m (>= l437c l435c)) (or l437m l436m (>= l437c l436c)))) (assert (or l437m (and (not l435m) (= l437c l435c)) (and (not l436m) (= l437c l436c)))) (define-fun f227m () Bool l437m) (define-fun f227c () Int l437c) (declare-fun l438m () Bool) (declare-fun l438c () Int) (assert (= l438m (and f34m f226m))) (assert (and (or l438m f34m (>= l438c f34c)) (or l438m f226m (>= l438c f226c)))) (assert (or l438m (and (not f34m) (= l438c f34c)) (and (not f226m) (= l438c f226c)))) (define-fun f228m () Bool l438m) (define-fun f228c () Int l438c) (declare-fun l439m () Bool) (declare-fun l439c () Int) (assert (= l439m (and f35m f227m))) (assert (and (or l439m f35m (>= l439c f35c)) (or l439m f227m (>= l439c f227c)))) (assert (or l439m (and (not f35m) (= l439c f35c)) (and (not f227m) (= l439c f227c)))) (define-fun f229m () Bool l439m) (define-fun f229c () Int l439c) (declare-fun l440m () Bool) (declare-fun l440c () Int) (assert (= l440m (or f18m f18m))) (assert (or l440m (= l440c (+ f18c f18c)))) (declare-fun l441m () Bool) (declare-fun l441c () Int) (assert (= l441m (or f19m f20m))) (assert (or l441m (= l441c (+ f19c f20c)))) (declare-fun l442m () Bool) (declare-fun l442c () Int) (assert (= l442m (and l440m l441m))) (assert (and (or l442m l440m (>= l442c l440c)) (or l442m l441m (>= l442c l441c)))) (assert (or l442m (and (not l440m) (= l442c l440c)) (and (not l441m) (= l442c l441c)))) (define-fun f230m () Bool l442m) (define-fun f230c () Int l442c) (declare-fun l443m () Bool) (declare-fun l443c () Int) (assert (= l443m (or f18m f19m))) (assert (or l443m (= l443c (+ f18c f19c)))) (declare-fun l444m () Bool) (declare-fun l444c () Int) (assert (= l444m (or f19m f21m))) (assert (or l444m (= l444c (+ f19c f21c)))) (declare-fun l445m () Bool) (declare-fun l445c () Int) (assert (= l445m (and l443m l444m))) (assert (and (or l445m l443m (>= l445c l443c)) (or l445m l444m (>= l445c l444c)))) (assert (or l445m (and (not l443m) (= l445c l443c)) (and (not l444m) (= l445c l444c)))) (define-fun f231m () Bool l445m) (define-fun f231c () Int l445c) (declare-fun l446m () Bool) (declare-fun l446c () Int) (assert (= l446m (or f20m f18m))) (assert (or l446m (= l446c (+ f20c f18c)))) (declare-fun l447m () Bool) (declare-fun l447c () Int) (assert (= l447m (or f21m f20m))) (assert (or l447m (= l447c (+ f21c f20c)))) (declare-fun l448m () Bool) (declare-fun l448c () Int) (assert (= l448m (and l446m l447m))) (assert (and (or l448m l446m (>= l448c l446c)) (or l448m l447m (>= l448c l447c)))) (assert (or l448m (and (not l446m) (= l448c l446c)) (and (not l447m) (= l448c l447c)))) (define-fun f232m () Bool l448m) (define-fun f232c () Int l448c) (declare-fun l449m () Bool) (declare-fun l449c () Int) (assert (= l449m (or f20m f19m))) (assert (or l449m (= l449c (+ f20c f19c)))) (declare-fun l450m () Bool) (declare-fun l450c () Int) (assert (= l450m (or f21m f21m))) (assert (or l450m (= l450c (+ f21c f21c)))) (declare-fun l451m () Bool) (declare-fun l451c () Int) (assert (= l451m (and l449m l450m))) (assert (and (or l451m l449m (>= l451c l449c)) (or l451m l450m (>= l451c l450c)))) (assert (or l451m (and (not l449m) (= l451c l449c)) (and (not l450m) (= l451c l450c)))) (define-fun f233m () Bool l451m) (define-fun f233c () Int l451c) (declare-fun l452m () Bool) (declare-fun l452c () Int) (assert (= l452m (or f18m f22m))) (assert (or l452m (= l452c (+ f18c f22c)))) (declare-fun l453m () Bool) (declare-fun l453c () Int) (assert (= l453m (or f19m f23m))) (assert (or l453m (= l453c (+ f19c f23c)))) (declare-fun l454m () Bool) (declare-fun l454c () Int) (assert (= l454m (and l452m l453m))) (assert (and (or l454m l452m (>= l454c l452c)) (or l454m l453m (>= l454c l453c)))) (assert (or l454m (and (not l452m) (= l454c l452c)) (and (not l453m) (= l454c l453c)))) (define-fun f234m () Bool l454m) (define-fun f234c () Int l454c) (declare-fun l455m () Bool) (declare-fun l455c () Int) (assert (= l455m (or f20m f22m))) (assert (or l455m (= l455c (+ f20c f22c)))) (declare-fun l456m () Bool) (declare-fun l456c () Int) (assert (= l456m (or f21m f23m))) (assert (or l456m (= l456c (+ f21c f23c)))) (declare-fun l457m () Bool) (declare-fun l457c () Int) (assert (= l457m (and l455m l456m))) (assert (and (or l457m l455m (>= l457c l455c)) (or l457m l456m (>= l457c l456c)))) (assert (or l457m (and (not l455m) (= l457c l455c)) (and (not l456m) (= l457c l456c)))) (define-fun f235m () Bool l457m) (define-fun f235c () Int l457c) (declare-fun l458m () Bool) (declare-fun l458c () Int) (assert (= l458m (and f22m f234m))) (assert (and (or l458m f22m (>= l458c f22c)) (or l458m f234m (>= l458c f234c)))) (assert (or l458m (and (not f22m) (= l458c f22c)) (and (not f234m) (= l458c f234c)))) (define-fun f236m () Bool l458m) (define-fun f236c () Int l458c) (declare-fun l459m () Bool) (declare-fun l459c () Int) (assert (= l459m (and f23m f235m))) (assert (and (or l459m f23m (>= l459c f23c)) (or l459m f235m (>= l459c f235c)))) (assert (or l459m (and (not f23m) (= l459c f23c)) (and (not f235m) (= l459c f235c)))) (define-fun f237m () Bool l459m) (define-fun f237c () Int l459c) (declare-fun l460m () Bool) (declare-fun l460c () Int) (assert (= l460m (or f18m f230m))) (assert (or l460m (= l460c (+ f18c f230c)))) (declare-fun l461m () Bool) (declare-fun l461c () Int) (assert (= l461m (or f19m f232m))) (assert (or l461m (= l461c (+ f19c f232c)))) (declare-fun l462m () Bool) (declare-fun l462c () Int) (assert (= l462m (and l460m l461m))) (assert (and (or l462m l460m (>= l462c l460c)) (or l462m l461m (>= l462c l461c)))) (assert (or l462m (and (not l460m) (= l462c l460c)) (and (not l461m) (= l462c l461c)))) (define-fun f238m () Bool l462m) (define-fun f238c () Int l462c) (declare-fun l463m () Bool) (declare-fun l463c () Int) (assert (= l463m (or f18m f231m))) (assert (or l463m (= l463c (+ f18c f231c)))) (declare-fun l464m () Bool) (declare-fun l464c () Int) (assert (= l464m (or f19m f233m))) (assert (or l464m (= l464c (+ f19c f233c)))) (declare-fun l465m () Bool) (declare-fun l465c () Int) (assert (= l465m (and l463m l464m))) (assert (and (or l465m l463m (>= l465c l463c)) (or l465m l464m (>= l465c l464c)))) (assert (or l465m (and (not l463m) (= l465c l463c)) (and (not l464m) (= l465c l464c)))) (define-fun f239m () Bool l465m) (define-fun f239c () Int l465c) (declare-fun l466m () Bool) (declare-fun l466c () Int) (assert (= l466m (or f20m f230m))) (assert (or l466m (= l466c (+ f20c f230c)))) (declare-fun l467m () Bool) (declare-fun l467c () Int) (assert (= l467m (or f21m f232m))) (assert (or l467m (= l467c (+ f21c f232c)))) (declare-fun l468m () Bool) (declare-fun l468c () Int) (assert (= l468m (and l466m l467m))) (assert (and (or l468m l466m (>= l468c l466c)) (or l468m l467m (>= l468c l467c)))) (assert (or l468m (and (not l466m) (= l468c l466c)) (and (not l467m) (= l468c l467c)))) (define-fun f240m () Bool l468m) (define-fun f240c () Int l468c) (declare-fun l469m () Bool) (declare-fun l469c () Int) (assert (= l469m (or f20m f231m))) (assert (or l469m (= l469c (+ f20c f231c)))) (declare-fun l470m () Bool) (declare-fun l470c () Int) (assert (= l470m (or f21m f233m))) (assert (or l470m (= l470c (+ f21c f233c)))) (declare-fun l471m () Bool) (declare-fun l471c () Int) (assert (= l471m (and l469m l470m))) (assert (and (or l471m l469m (>= l471c l469c)) (or l471m l470m (>= l471c l470c)))) (assert (or l471m (and (not l469m) (= l471c l469c)) (and (not l470m) (= l471c l470c)))) (define-fun f241m () Bool l471m) (define-fun f241c () Int l471c) (declare-fun l472m () Bool) (declare-fun l472c () Int) (assert (= l472m (or f18m f236m))) (assert (or l472m (= l472c (+ f18c f236c)))) (declare-fun l473m () Bool) (declare-fun l473c () Int) (assert (= l473m (or f19m f237m))) (assert (or l473m (= l473c (+ f19c f237c)))) (declare-fun l474m () Bool) (declare-fun l474c () Int) (assert (= l474m (and l472m l473m))) (assert (and (or l474m l472m (>= l474c l472c)) (or l474m l473m (>= l474c l473c)))) (assert (or l474m (and (not l472m) (= l474c l472c)) (and (not l473m) (= l474c l473c)))) (define-fun f242m () Bool l474m) (define-fun f242c () Int l474c) (declare-fun l475m () Bool) (declare-fun l475c () Int) (assert (= l475m (or f20m f236m))) (assert (or l475m (= l475c (+ f20c f236c)))) (declare-fun l476m () Bool) (declare-fun l476c () Int) (assert (= l476m (or f21m f237m))) (assert (or l476m (= l476c (+ f21c f237c)))) (declare-fun l477m () Bool) (declare-fun l477c () Int) (assert (= l477m (and l475m l476m))) (assert (and (or l477m l475m (>= l477c l475c)) (or l477m l476m (>= l477c l476c)))) (assert (or l477m (and (not l475m) (= l477c l475c)) (and (not l476m) (= l477c l476c)))) (define-fun f243m () Bool l477m) (define-fun f243c () Int l477c) (declare-fun l478m () Bool) (declare-fun l478c () Int) (assert (= l478m (and f22m f242m))) (assert (and (or l478m f22m (>= l478c f22c)) (or l478m f242m (>= l478c f242c)))) (assert (or l478m (and (not f22m) (= l478c f22c)) (and (not f242m) (= l478c f242c)))) (define-fun f244m () Bool l478m) (define-fun f244c () Int l478c) (declare-fun l479m () Bool) (declare-fun l479c () Int) (assert (= l479m (and f23m f243m))) (assert (and (or l479m f23m (>= l479c f23c)) (or l479m f243m (>= l479c f243c)))) (assert (or l479m (and (not f23m) (= l479c f23c)) (and (not f243m) (= l479c f243c)))) (define-fun f245m () Bool l479m) (define-fun f245c () Int l479c) (declare-fun l480m () Bool) (declare-fun l480c () Int) (assert (= l480m (or f36m f238m))) (assert (or l480m (= l480c (+ f36c f238c)))) (declare-fun l481m () Bool) (declare-fun l481c () Int) (assert (= l481m (or f37m f240m))) (assert (or l481m (= l481c (+ f37c f240c)))) (declare-fun l482m () Bool) (declare-fun l482c () Int) (assert (= l482m (and l480m l481m))) (assert (and (or l482m l480m (>= l482c l480c)) (or l482m l481m (>= l482c l481c)))) (assert (or l482m (and (not l480m) (= l482c l480c)) (and (not l481m) (= l482c l481c)))) (define-fun f246m () Bool l482m) (define-fun f246c () Int l482c) (declare-fun l483m () Bool) (declare-fun l483c () Int) (assert (= l483m (or f36m f239m))) (assert (or l483m (= l483c (+ f36c f239c)))) (declare-fun l484m () Bool) (declare-fun l484c () Int) (assert (= l484m (or f37m f241m))) (assert (or l484m (= l484c (+ f37c f241c)))) (declare-fun l485m () Bool) (declare-fun l485c () Int) (assert (= l485m (and l483m l484m))) (assert (and (or l485m l483m (>= l485c l483c)) (or l485m l484m (>= l485c l484c)))) (assert (or l485m (and (not l483m) (= l485c l483c)) (and (not l484m) (= l485c l484c)))) (define-fun f247m () Bool l485m) (define-fun f247c () Int l485c) (declare-fun l486m () Bool) (declare-fun l486c () Int) (assert (= l486m (or f38m f238m))) (assert (or l486m (= l486c (+ f38c f238c)))) (declare-fun l487m () Bool) (declare-fun l487c () Int) (assert (= l487m (or f39m f240m))) (assert (or l487m (= l487c (+ f39c f240c)))) (declare-fun l488m () Bool) (declare-fun l488c () Int) (assert (= l488m (and l486m l487m))) (assert (and (or l488m l486m (>= l488c l486c)) (or l488m l487m (>= l488c l487c)))) (assert (or l488m (and (not l486m) (= l488c l486c)) (and (not l487m) (= l488c l487c)))) (define-fun f248m () Bool l488m) (define-fun f248c () Int l488c) (declare-fun l489m () Bool) (declare-fun l489c () Int) (assert (= l489m (or f38m f239m))) (assert (or l489m (= l489c (+ f38c f239c)))) (declare-fun l490m () Bool) (declare-fun l490c () Int) (assert (= l490m (or f39m f241m))) (assert (or l490m (= l490c (+ f39c f241c)))) (declare-fun l491m () Bool) (declare-fun l491c () Int) (assert (= l491m (and l489m l490m))) (assert (and (or l491m l489m (>= l491c l489c)) (or l491m l490m (>= l491c l490c)))) (assert (or l491m (and (not l489m) (= l491c l489c)) (and (not l490m) (= l491c l490c)))) (define-fun f249m () Bool l491m) (define-fun f249c () Int l491c) (declare-fun l492m () Bool) (declare-fun l492c () Int) (assert (= l492m (or f36m f244m))) (assert (or l492m (= l492c (+ f36c f244c)))) (declare-fun l493m () Bool) (declare-fun l493c () Int) (assert (= l493m (or f37m f245m))) (assert (or l493m (= l493c (+ f37c f245c)))) (declare-fun l494m () Bool) (declare-fun l494c () Int) (assert (= l494m (and l492m l493m))) (assert (and (or l494m l492m (>= l494c l492c)) (or l494m l493m (>= l494c l493c)))) (assert (or l494m (and (not l492m) (= l494c l492c)) (and (not l493m) (= l494c l493c)))) (define-fun f250m () Bool l494m) (define-fun f250c () Int l494c) (declare-fun l495m () Bool) (declare-fun l495c () Int) (assert (= l495m (or f38m f244m))) (assert (or l495m (= l495c (+ f38c f244c)))) (declare-fun l496m () Bool) (declare-fun l496c () Int) (assert (= l496m (or f39m f245m))) (assert (or l496m (= l496c (+ f39c f245c)))) (declare-fun l497m () Bool) (declare-fun l497c () Int) (assert (= l497m (and l495m l496m))) (assert (and (or l497m l495m (>= l497c l495c)) (or l497m l496m (>= l497c l496c)))) (assert (or l497m (and (not l495m) (= l497c l495c)) (and (not l496m) (= l497c l496c)))) (define-fun f251m () Bool l497m) (define-fun f251c () Int l497c) (declare-fun l498m () Bool) (declare-fun l498c () Int) (assert (= l498m (and f40m f250m))) (assert (and (or l498m f40m (>= l498c f40c)) (or l498m f250m (>= l498c f250c)))) (assert (or l498m (and (not f40m) (= l498c f40c)) (and (not f250m) (= l498c f250c)))) (define-fun f252m () Bool l498m) (define-fun f252c () Int l498c) (declare-fun l499m () Bool) (declare-fun l499c () Int) (assert (= l499m (and f41m f251m))) (assert (and (or l499m f41m (>= l499c f41c)) (or l499m f251m (>= l499c f251c)))) (assert (or l499m (and (not f41m) (= l499c f41c)) (and (not f251m) (= l499c f251c)))) (define-fun f253m () Bool l499m) (define-fun f253c () Int l499c) (declare-fun l500m () Bool) (declare-fun l500c () Int) (assert (= l500m (or f48m f48m))) (assert (or l500m (= l500c (+ f48c f48c)))) (declare-fun l501m () Bool) (declare-fun l501c () Int) (assert (= l501m (or f49m f50m))) (assert (or l501m (= l501c (+ f49c f50c)))) (declare-fun l502m () Bool) (declare-fun l502c () Int) (assert (= l502m (and l500m l501m))) (assert (and (or l502m l500m (>= l502c l500c)) (or l502m l501m (>= l502c l501c)))) (assert (or l502m (and (not l500m) (= l502c l500c)) (and (not l501m) (= l502c l501c)))) (define-fun f254m () Bool l502m) (define-fun f254c () Int l502c) (declare-fun l503m () Bool) (declare-fun l503c () Int) (assert (= l503m (or f48m f49m))) (assert (or l503m (= l503c (+ f48c f49c)))) (declare-fun l504m () Bool) (declare-fun l504c () Int) (assert (= l504m (or f49m f51m))) (assert (or l504m (= l504c (+ f49c f51c)))) (declare-fun l505m () Bool) (declare-fun l505c () Int) (assert (= l505m (and l503m l504m))) (assert (and (or l505m l503m (>= l505c l503c)) (or l505m l504m (>= l505c l504c)))) (assert (or l505m (and (not l503m) (= l505c l503c)) (and (not l504m) (= l505c l504c)))) (define-fun f255m () Bool l505m) (define-fun f255c () Int l505c) (declare-fun l506m () Bool) (declare-fun l506c () Int) (assert (= l506m (or f50m f48m))) (assert (or l506m (= l506c (+ f50c f48c)))) (declare-fun l507m () Bool) (declare-fun l507c () Int) (assert (= l507m (or f51m f50m))) (assert (or l507m (= l507c (+ f51c f50c)))) (declare-fun l508m () Bool) (declare-fun l508c () Int) (assert (= l508m (and l506m l507m))) (assert (and (or l508m l506m (>= l508c l506c)) (or l508m l507m (>= l508c l507c)))) (assert (or l508m (and (not l506m) (= l508c l506c)) (and (not l507m) (= l508c l507c)))) (define-fun f256m () Bool l508m) (define-fun f256c () Int l508c) (declare-fun l509m () Bool) (declare-fun l509c () Int) (assert (= l509m (or f50m f49m))) (assert (or l509m (= l509c (+ f50c f49c)))) (declare-fun l510m () Bool) (declare-fun l510c () Int) (assert (= l510m (or f51m f51m))) (assert (or l510m (= l510c (+ f51c f51c)))) (declare-fun l511m () Bool) (declare-fun l511c () Int) (assert (= l511m (and l509m l510m))) (assert (and (or l511m l509m (>= l511c l509c)) (or l511m l510m (>= l511c l510c)))) (assert (or l511m (and (not l509m) (= l511c l509c)) (and (not l510m) (= l511c l510c)))) (define-fun f257m () Bool l511m) (define-fun f257c () Int l511c) (declare-fun l512m () Bool) (declare-fun l512c () Int) (assert (= l512m (or f48m f52m))) (assert (or l512m (= l512c (+ f48c f52c)))) (declare-fun l513m () Bool) (declare-fun l513c () Int) (assert (= l513m (or f49m f53m))) (assert (or l513m (= l513c (+ f49c f53c)))) (declare-fun l514m () Bool) (declare-fun l514c () Int) (assert (= l514m (and l512m l513m))) (assert (and (or l514m l512m (>= l514c l512c)) (or l514m l513m (>= l514c l513c)))) (assert (or l514m (and (not l512m) (= l514c l512c)) (and (not l513m) (= l514c l513c)))) (define-fun f258m () Bool l514m) (define-fun f258c () Int l514c) (declare-fun l515m () Bool) (declare-fun l515c () Int) (assert (= l515m (or f50m f52m))) (assert (or l515m (= l515c (+ f50c f52c)))) (declare-fun l516m () Bool) (declare-fun l516c () Int) (assert (= l516m (or f51m f53m))) (assert (or l516m (= l516c (+ f51c f53c)))) (declare-fun l517m () Bool) (declare-fun l517c () Int) (assert (= l517m (and l515m l516m))) (assert (and (or l517m l515m (>= l517c l515c)) (or l517m l516m (>= l517c l516c)))) (assert (or l517m (and (not l515m) (= l517c l515c)) (and (not l516m) (= l517c l516c)))) (define-fun f259m () Bool l517m) (define-fun f259c () Int l517c) (declare-fun l518m () Bool) (declare-fun l518c () Int) (assert (= l518m (and f52m f258m))) (assert (and (or l518m f52m (>= l518c f52c)) (or l518m f258m (>= l518c f258c)))) (assert (or l518m (and (not f52m) (= l518c f52c)) (and (not f258m) (= l518c f258c)))) (define-fun f260m () Bool l518m) (define-fun f260c () Int l518c) (declare-fun l519m () Bool) (declare-fun l519c () Int) (assert (= l519m (and f53m f259m))) (assert (and (or l519m f53m (>= l519c f53c)) (or l519m f259m (>= l519c f259c)))) (assert (or l519m (and (not f53m) (= l519c f53c)) (and (not f259m) (= l519c f259c)))) (define-fun f261m () Bool l519m) (define-fun f261c () Int l519c) (declare-fun l520m () Bool) (declare-fun l520c () Int) (assert (= l520m (or f42m f254m))) (assert (or l520m (= l520c (+ f42c f254c)))) (declare-fun l521m () Bool) (declare-fun l521c () Int) (assert (= l521m (or f43m f256m))) (assert (or l521m (= l521c (+ f43c f256c)))) (declare-fun l522m () Bool) (declare-fun l522c () Int) (assert (= l522m (and l520m l521m))) (assert (and (or l522m l520m (>= l522c l520c)) (or l522m l521m (>= l522c l521c)))) (assert (or l522m (and (not l520m) (= l522c l520c)) (and (not l521m) (= l522c l521c)))) (define-fun f262m () Bool l522m) (define-fun f262c () Int l522c) (declare-fun l523m () Bool) (declare-fun l523c () Int) (assert (= l523m (or f42m f255m))) (assert (or l523m (= l523c (+ f42c f255c)))) (declare-fun l524m () Bool) (declare-fun l524c () Int) (assert (= l524m (or f43m f257m))) (assert (or l524m (= l524c (+ f43c f257c)))) (declare-fun l525m () Bool) (declare-fun l525c () Int) (assert (= l525m (and l523m l524m))) (assert (and (or l525m l523m (>= l525c l523c)) (or l525m l524m (>= l525c l524c)))) (assert (or l525m (and (not l523m) (= l525c l523c)) (and (not l524m) (= l525c l524c)))) (define-fun f263m () Bool l525m) (define-fun f263c () Int l525c) (declare-fun l526m () Bool) (declare-fun l526c () Int) (assert (= l526m (or f44m f254m))) (assert (or l526m (= l526c (+ f44c f254c)))) (declare-fun l527m () Bool) (declare-fun l527c () Int) (assert (= l527m (or f45m f256m))) (assert (or l527m (= l527c (+ f45c f256c)))) (declare-fun l528m () Bool) (declare-fun l528c () Int) (assert (= l528m (and l526m l527m))) (assert (and (or l528m l526m (>= l528c l526c)) (or l528m l527m (>= l528c l527c)))) (assert (or l528m (and (not l526m) (= l528c l526c)) (and (not l527m) (= l528c l527c)))) (define-fun f264m () Bool l528m) (define-fun f264c () Int l528c) (declare-fun l529m () Bool) (declare-fun l529c () Int) (assert (= l529m (or f44m f255m))) (assert (or l529m (= l529c (+ f44c f255c)))) (declare-fun l530m () Bool) (declare-fun l530c () Int) (assert (= l530m (or f45m f257m))) (assert (or l530m (= l530c (+ f45c f257c)))) (declare-fun l531m () Bool) (declare-fun l531c () Int) (assert (= l531m (and l529m l530m))) (assert (and (or l531m l529m (>= l531c l529c)) (or l531m l530m (>= l531c l530c)))) (assert (or l531m (and (not l529m) (= l531c l529c)) (and (not l530m) (= l531c l530c)))) (define-fun f265m () Bool l531m) (define-fun f265c () Int l531c) (declare-fun l532m () Bool) (declare-fun l532c () Int) (assert (= l532m (or f42m f260m))) (assert (or l532m (= l532c (+ f42c f260c)))) (declare-fun l533m () Bool) (declare-fun l533c () Int) (assert (= l533m (or f43m f261m))) (assert (or l533m (= l533c (+ f43c f261c)))) (declare-fun l534m () Bool) (declare-fun l534c () Int) (assert (= l534m (and l532m l533m))) (assert (and (or l534m l532m (>= l534c l532c)) (or l534m l533m (>= l534c l533c)))) (assert (or l534m (and (not l532m) (= l534c l532c)) (and (not l533m) (= l534c l533c)))) (define-fun f266m () Bool l534m) (define-fun f266c () Int l534c) (declare-fun l535m () Bool) (declare-fun l535c () Int) (assert (= l535m (or f44m f260m))) (assert (or l535m (= l535c (+ f44c f260c)))) (declare-fun l536m () Bool) (declare-fun l536c () Int) (assert (= l536m (or f45m f261m))) (assert (or l536m (= l536c (+ f45c f261c)))) (declare-fun l537m () Bool) (declare-fun l537c () Int) (assert (= l537m (and l535m l536m))) (assert (and (or l537m l535m (>= l537c l535c)) (or l537m l536m (>= l537c l536c)))) (assert (or l537m (and (not l535m) (= l537c l535c)) (and (not l536m) (= l537c l536c)))) (define-fun f267m () Bool l537m) (define-fun f267c () Int l537c) (declare-fun l538m () Bool) (declare-fun l538c () Int) (assert (= l538m (and f46m f266m))) (assert (and (or l538m f46m (>= l538c f46c)) (or l538m f266m (>= l538c f266c)))) (assert (or l538m (and (not f46m) (= l538c f46c)) (and (not f266m) (= l538c f266c)))) (define-fun f268m () Bool l538m) (define-fun f268c () Int l538c) (declare-fun l539m () Bool) (declare-fun l539c () Int) (assert (= l539m (and f47m f267m))) (assert (and (or l539m f47m (>= l539c f47c)) (or l539m f267m (>= l539c f267c)))) (assert (or l539m (and (not f47m) (= l539c f47c)) (and (not f267m) (= l539c f267c)))) (define-fun f269m () Bool l539m) (define-fun f269c () Int l539c) (declare-fun l540m () Bool) (declare-fun l540c () Int) (assert (= l540m (or f42m f262m))) (assert (or l540m (= l540c (+ f42c f262c)))) (declare-fun l541m () Bool) (declare-fun l541c () Int) (assert (= l541m (or f43m f264m))) (assert (or l541m (= l541c (+ f43c f264c)))) (declare-fun l542m () Bool) (declare-fun l542c () Int) (assert (= l542m (and l540m l541m))) (assert (and (or l542m l540m (>= l542c l540c)) (or l542m l541m (>= l542c l541c)))) (assert (or l542m (and (not l540m) (= l542c l540c)) (and (not l541m) (= l542c l541c)))) (define-fun f270m () Bool l542m) (define-fun f270c () Int l542c) (declare-fun l543m () Bool) (declare-fun l543c () Int) (assert (= l543m (or f42m f263m))) (assert (or l543m (= l543c (+ f42c f263c)))) (declare-fun l544m () Bool) (declare-fun l544c () Int) (assert (= l544m (or f43m f265m))) (assert (or l544m (= l544c (+ f43c f265c)))) (declare-fun l545m () Bool) (declare-fun l545c () Int) (assert (= l545m (and l543m l544m))) (assert (and (or l545m l543m (>= l545c l543c)) (or l545m l544m (>= l545c l544c)))) (assert (or l545m (and (not l543m) (= l545c l543c)) (and (not l544m) (= l545c l544c)))) (define-fun f271m () Bool l545m) (define-fun f271c () Int l545c) (declare-fun l546m () Bool) (declare-fun l546c () Int) (assert (= l546m (or f44m f262m))) (assert (or l546m (= l546c (+ f44c f262c)))) (declare-fun l547m () Bool) (declare-fun l547c () Int) (assert (= l547m (or f45m f264m))) (assert (or l547m (= l547c (+ f45c f264c)))) (declare-fun l548m () Bool) (declare-fun l548c () Int) (assert (= l548m (and l546m l547m))) (assert (and (or l548m l546m (>= l548c l546c)) (or l548m l547m (>= l548c l547c)))) (assert (or l548m (and (not l546m) (= l548c l546c)) (and (not l547m) (= l548c l547c)))) (define-fun f272m () Bool l548m) (define-fun f272c () Int l548c) (declare-fun l549m () Bool) (declare-fun l549c () Int) (assert (= l549m (or f44m f263m))) (assert (or l549m (= l549c (+ f44c f263c)))) (declare-fun l550m () Bool) (declare-fun l550c () Int) (assert (= l550m (or f45m f265m))) (assert (or l550m (= l550c (+ f45c f265c)))) (declare-fun l551m () Bool) (declare-fun l551c () Int) (assert (= l551m (and l549m l550m))) (assert (and (or l551m l549m (>= l551c l549c)) (or l551m l550m (>= l551c l550c)))) (assert (or l551m (and (not l549m) (= l551c l549c)) (and (not l550m) (= l551c l550c)))) (define-fun f273m () Bool l551m) (define-fun f273c () Int l551c) (declare-fun l552m () Bool) (declare-fun l552c () Int) (assert (= l552m (or f42m f268m))) (assert (or l552m (= l552c (+ f42c f268c)))) (declare-fun l553m () Bool) (declare-fun l553c () Int) (assert (= l553m (or f43m f269m))) (assert (or l553m (= l553c (+ f43c f269c)))) (declare-fun l554m () Bool) (declare-fun l554c () Int) (assert (= l554m (and l552m l553m))) (assert (and (or l554m l552m (>= l554c l552c)) (or l554m l553m (>= l554c l553c)))) (assert (or l554m (and (not l552m) (= l554c l552c)) (and (not l553m) (= l554c l553c)))) (define-fun f274m () Bool l554m) (define-fun f274c () Int l554c) (declare-fun l555m () Bool) (declare-fun l555c () Int) (assert (= l555m (or f44m f268m))) (assert (or l555m (= l555c (+ f44c f268c)))) (declare-fun l556m () Bool) (declare-fun l556c () Int) (assert (= l556m (or f45m f269m))) (assert (or l556m (= l556c (+ f45c f269c)))) (declare-fun l557m () Bool) (declare-fun l557c () Int) (assert (= l557m (and l555m l556m))) (assert (and (or l557m l555m (>= l557c l555c)) (or l557m l556m (>= l557c l556c)))) (assert (or l557m (and (not l555m) (= l557c l555c)) (and (not l556m) (= l557c l556c)))) (define-fun f275m () Bool l557m) (define-fun f275c () Int l557c) (declare-fun l558m () Bool) (declare-fun l558c () Int) (assert (= l558m (and f46m f274m))) (assert (and (or l558m f46m (>= l558c f46c)) (or l558m f274m (>= l558c f274c)))) (assert (or l558m (and (not f46m) (= l558c f46c)) (and (not f274m) (= l558c f274c)))) (define-fun f276m () Bool l558m) (define-fun f276c () Int l558c) (declare-fun l559m () Bool) (declare-fun l559c () Int) (assert (= l559m (and f47m f275m))) (assert (and (or l559m f47m (>= l559c f47c)) (or l559m f275m (>= l559c f275c)))) (assert (or l559m (and (not f47m) (= l559c f47c)) (and (not f275m) (= l559c f275c)))) (define-fun f277m () Bool l559m) (define-fun f277c () Int l559c) (declare-fun l560m () Bool) (declare-fun l560c () Int) (assert (= l560m (or f42m f42m))) (assert (or l560m (= l560c (+ f42c f42c)))) (declare-fun l561m () Bool) (declare-fun l561c () Int) (assert (= l561m (or f43m f44m))) (assert (or l561m (= l561c (+ f43c f44c)))) (declare-fun l562m () Bool) (declare-fun l562c () Int) (assert (= l562m (and l560m l561m))) (assert (and (or l562m l560m (>= l562c l560c)) (or l562m l561m (>= l562c l561c)))) (assert (or l562m (and (not l560m) (= l562c l560c)) (and (not l561m) (= l562c l561c)))) (define-fun f278m () Bool l562m) (define-fun f278c () Int l562c) (declare-fun l563m () Bool) (declare-fun l563c () Int) (assert (= l563m (or f42m f43m))) (assert (or l563m (= l563c (+ f42c f43c)))) (declare-fun l564m () Bool) (declare-fun l564c () Int) (assert (= l564m (or f43m f45m))) (assert (or l564m (= l564c (+ f43c f45c)))) (declare-fun l565m () Bool) (declare-fun l565c () Int) (assert (= l565m (and l563m l564m))) (assert (and (or l565m l563m (>= l565c l563c)) (or l565m l564m (>= l565c l564c)))) (assert (or l565m (and (not l563m) (= l565c l563c)) (and (not l564m) (= l565c l564c)))) (define-fun f279m () Bool l565m) (define-fun f279c () Int l565c) (declare-fun l566m () Bool) (declare-fun l566c () Int) (assert (= l566m (or f44m f42m))) (assert (or l566m (= l566c (+ f44c f42c)))) (declare-fun l567m () Bool) (declare-fun l567c () Int) (assert (= l567m (or f45m f44m))) (assert (or l567m (= l567c (+ f45c f44c)))) (declare-fun l568m () Bool) (declare-fun l568c () Int) (assert (= l568m (and l566m l567m))) (assert (and (or l568m l566m (>= l568c l566c)) (or l568m l567m (>= l568c l567c)))) (assert (or l568m (and (not l566m) (= l568c l566c)) (and (not l567m) (= l568c l567c)))) (define-fun f280m () Bool l568m) (define-fun f280c () Int l568c) (declare-fun l569m () Bool) (declare-fun l569c () Int) (assert (= l569m (or f44m f43m))) (assert (or l569m (= l569c (+ f44c f43c)))) (declare-fun l570m () Bool) (declare-fun l570c () Int) (assert (= l570m (or f45m f45m))) (assert (or l570m (= l570c (+ f45c f45c)))) (declare-fun l571m () Bool) (declare-fun l571c () Int) (assert (= l571m (and l569m l570m))) (assert (and (or l571m l569m (>= l571c l569c)) (or l571m l570m (>= l571c l570c)))) (assert (or l571m (and (not l569m) (= l571c l569c)) (and (not l570m) (= l571c l570c)))) (define-fun f281m () Bool l571m) (define-fun f281c () Int l571c) (declare-fun l572m () Bool) (declare-fun l572c () Int) (assert (= l572m (or f42m f46m))) (assert (or l572m (= l572c (+ f42c f46c)))) (declare-fun l573m () Bool) (declare-fun l573c () Int) (assert (= l573m (or f43m f47m))) (assert (or l573m (= l573c (+ f43c f47c)))) (declare-fun l574m () Bool) (declare-fun l574c () Int) (assert (= l574m (and l572m l573m))) (assert (and (or l574m l572m (>= l574c l572c)) (or l574m l573m (>= l574c l573c)))) (assert (or l574m (and (not l572m) (= l574c l572c)) (and (not l573m) (= l574c l573c)))) (define-fun f282m () Bool l574m) (define-fun f282c () Int l574c) (declare-fun l575m () Bool) (declare-fun l575c () Int) (assert (= l575m (or f44m f46m))) (assert (or l575m (= l575c (+ f44c f46c)))) (declare-fun l576m () Bool) (declare-fun l576c () Int) (assert (= l576m (or f45m f47m))) (assert (or l576m (= l576c (+ f45c f47c)))) (declare-fun l577m () Bool) (declare-fun l577c () Int) (assert (= l577m (and l575m l576m))) (assert (and (or l577m l575m (>= l577c l575c)) (or l577m l576m (>= l577c l576c)))) (assert (or l577m (and (not l575m) (= l577c l575c)) (and (not l576m) (= l577c l576c)))) (define-fun f283m () Bool l577m) (define-fun f283c () Int l577c) (declare-fun l578m () Bool) (declare-fun l578c () Int) (assert (= l578m (and f46m f282m))) (assert (and (or l578m f46m (>= l578c f46c)) (or l578m f282m (>= l578c f282c)))) (assert (or l578m (and (not f46m) (= l578c f46c)) (and (not f282m) (= l578c f282c)))) (define-fun f284m () Bool l578m) (define-fun f284c () Int l578c) (declare-fun l579m () Bool) (declare-fun l579c () Int) (assert (= l579m (and f47m f283m))) (assert (and (or l579m f47m (>= l579c f47c)) (or l579m f283m (>= l579c f283c)))) (assert (or l579m (and (not f47m) (= l579c f47c)) (and (not f283m) (= l579c f283c)))) (define-fun f285m () Bool l579m) (define-fun f285c () Int l579c) (declare-fun l580m () Bool) (declare-fun l580c () Int) (assert (= l580m (or f42m f278m))) (assert (or l580m (= l580c (+ f42c f278c)))) (declare-fun l581m () Bool) (declare-fun l581c () Int) (assert (= l581m (or f43m f280m))) (assert (or l581m (= l581c (+ f43c f280c)))) (declare-fun l582m () Bool) (declare-fun l582c () Int) (assert (= l582m (and l580m l581m))) (assert (and (or l582m l580m (>= l582c l580c)) (or l582m l581m (>= l582c l581c)))) (assert (or l582m (and (not l580m) (= l582c l580c)) (and (not l581m) (= l582c l581c)))) (define-fun f286m () Bool l582m) (define-fun f286c () Int l582c) (declare-fun l583m () Bool) (declare-fun l583c () Int) (assert (= l583m (or f42m f279m))) (assert (or l583m (= l583c (+ f42c f279c)))) (declare-fun l584m () Bool) (declare-fun l584c () Int) (assert (= l584m (or f43m f281m))) (assert (or l584m (= l584c (+ f43c f281c)))) (declare-fun l585m () Bool) (declare-fun l585c () Int) (assert (= l585m (and l583m l584m))) (assert (and (or l585m l583m (>= l585c l583c)) (or l585m l584m (>= l585c l584c)))) (assert (or l585m (and (not l583m) (= l585c l583c)) (and (not l584m) (= l585c l584c)))) (define-fun f287m () Bool l585m) (define-fun f287c () Int l585c) (declare-fun l586m () Bool) (declare-fun l586c () Int) (assert (= l586m (or f44m f278m))) (assert (or l586m (= l586c (+ f44c f278c)))) (declare-fun l587m () Bool) (declare-fun l587c () Int) (assert (= l587m (or f45m f280m))) (assert (or l587m (= l587c (+ f45c f280c)))) (declare-fun l588m () Bool) (declare-fun l588c () Int) (assert (= l588m (and l586m l587m))) (assert (and (or l588m l586m (>= l588c l586c)) (or l588m l587m (>= l588c l587c)))) (assert (or l588m (and (not l586m) (= l588c l586c)) (and (not l587m) (= l588c l587c)))) (define-fun f288m () Bool l588m) (define-fun f288c () Int l588c) (declare-fun l589m () Bool) (declare-fun l589c () Int) (assert (= l589m (or f44m f279m))) (assert (or l589m (= l589c (+ f44c f279c)))) (declare-fun l590m () Bool) (declare-fun l590c () Int) (assert (= l590m (or f45m f281m))) (assert (or l590m (= l590c (+ f45c f281c)))) (declare-fun l591m () Bool) (declare-fun l591c () Int) (assert (= l591m (and l589m l590m))) (assert (and (or l591m l589m (>= l591c l589c)) (or l591m l590m (>= l591c l590c)))) (assert (or l591m (and (not l589m) (= l591c l589c)) (and (not l590m) (= l591c l590c)))) (define-fun f289m () Bool l591m) (define-fun f289c () Int l591c) (declare-fun l592m () Bool) (declare-fun l592c () Int) (assert (= l592m (or f42m f284m))) (assert (or l592m (= l592c (+ f42c f284c)))) (declare-fun l593m () Bool) (declare-fun l593c () Int) (assert (= l593m (or f43m f285m))) (assert (or l593m (= l593c (+ f43c f285c)))) (declare-fun l594m () Bool) (declare-fun l594c () Int) (assert (= l594m (and l592m l593m))) (assert (and (or l594m l592m (>= l594c l592c)) (or l594m l593m (>= l594c l593c)))) (assert (or l594m (and (not l592m) (= l594c l592c)) (and (not l593m) (= l594c l593c)))) (define-fun f290m () Bool l594m) (define-fun f290c () Int l594c) (declare-fun l595m () Bool) (declare-fun l595c () Int) (assert (= l595m (or f44m f284m))) (assert (or l595m (= l595c (+ f44c f284c)))) (declare-fun l596m () Bool) (declare-fun l596c () Int) (assert (= l596m (or f45m f285m))) (assert (or l596m (= l596c (+ f45c f285c)))) (declare-fun l597m () Bool) (declare-fun l597c () Int) (assert (= l597m (and l595m l596m))) (assert (and (or l597m l595m (>= l597c l595c)) (or l597m l596m (>= l597c l596c)))) (assert (or l597m (and (not l595m) (= l597c l595c)) (and (not l596m) (= l597c l596c)))) (define-fun f291m () Bool l597m) (define-fun f291c () Int l597c) (declare-fun l598m () Bool) (declare-fun l598c () Int) (assert (= l598m (and f46m f290m))) (assert (and (or l598m f46m (>= l598c f46c)) (or l598m f290m (>= l598c f290c)))) (assert (or l598m (and (not f46m) (= l598c f46c)) (and (not f290m) (= l598c f290c)))) (define-fun f292m () Bool l598m) (define-fun f292c () Int l598c) (declare-fun l599m () Bool) (declare-fun l599c () Int) (assert (= l599m (and f47m f291m))) (assert (and (or l599m f47m (>= l599c f47c)) (or l599m f291m (>= l599c f291c)))) (assert (or l599m (and (not f47m) (= l599c f47c)) (and (not f291m) (= l599c f291c)))) (define-fun f293m () Bool l599m) (define-fun f293c () Int l599c) (declare-fun l600m () Bool) (declare-fun l600c () Int) (assert (= l600m (or f48m f286m))) (assert (or l600m (= l600c (+ f48c f286c)))) (declare-fun l601m () Bool) (declare-fun l601c () Int) (assert (= l601m (or f49m f288m))) (assert (or l601m (= l601c (+ f49c f288c)))) (declare-fun l602m () Bool) (declare-fun l602c () Int) (assert (= l602m (and l600m l601m))) (assert (and (or l602m l600m (>= l602c l600c)) (or l602m l601m (>= l602c l601c)))) (assert (or l602m (and (not l600m) (= l602c l600c)) (and (not l601m) (= l602c l601c)))) (define-fun f294m () Bool l602m) (define-fun f294c () Int l602c) (declare-fun l603m () Bool) (declare-fun l603c () Int) (assert (= l603m (or f48m f287m))) (assert (or l603m (= l603c (+ f48c f287c)))) (declare-fun l604m () Bool) (declare-fun l604c () Int) (assert (= l604m (or f49m f289m))) (assert (or l604m (= l604c (+ f49c f289c)))) (declare-fun l605m () Bool) (declare-fun l605c () Int) (assert (= l605m (and l603m l604m))) (assert (and (or l605m l603m (>= l605c l603c)) (or l605m l604m (>= l605c l604c)))) (assert (or l605m (and (not l603m) (= l605c l603c)) (and (not l604m) (= l605c l604c)))) (define-fun f295m () Bool l605m) (define-fun f295c () Int l605c) (declare-fun l606m () Bool) (declare-fun l606c () Int) (assert (= l606m (or f50m f286m))) (assert (or l606m (= l606c (+ f50c f286c)))) (declare-fun l607m () Bool) (declare-fun l607c () Int) (assert (= l607m (or f51m f288m))) (assert (or l607m (= l607c (+ f51c f288c)))) (declare-fun l608m () Bool) (declare-fun l608c () Int) (assert (= l608m (and l606m l607m))) (assert (and (or l608m l606m (>= l608c l606c)) (or l608m l607m (>= l608c l607c)))) (assert (or l608m (and (not l606m) (= l608c l606c)) (and (not l607m) (= l608c l607c)))) (define-fun f296m () Bool l608m) (define-fun f296c () Int l608c) (declare-fun l609m () Bool) (declare-fun l609c () Int) (assert (= l609m (or f50m f287m))) (assert (or l609m (= l609c (+ f50c f287c)))) (declare-fun l610m () Bool) (declare-fun l610c () Int) (assert (= l610m (or f51m f289m))) (assert (or l610m (= l610c (+ f51c f289c)))) (declare-fun l611m () Bool) (declare-fun l611c () Int) (assert (= l611m (and l609m l610m))) (assert (and (or l611m l609m (>= l611c l609c)) (or l611m l610m (>= l611c l610c)))) (assert (or l611m (and (not l609m) (= l611c l609c)) (and (not l610m) (= l611c l610c)))) (define-fun f297m () Bool l611m) (define-fun f297c () Int l611c) (declare-fun l612m () Bool) (declare-fun l612c () Int) (assert (= l612m (or f48m f292m))) (assert (or l612m (= l612c (+ f48c f292c)))) (declare-fun l613m () Bool) (declare-fun l613c () Int) (assert (= l613m (or f49m f293m))) (assert (or l613m (= l613c (+ f49c f293c)))) (declare-fun l614m () Bool) (declare-fun l614c () Int) (assert (= l614m (and l612m l613m))) (assert (and (or l614m l612m (>= l614c l612c)) (or l614m l613m (>= l614c l613c)))) (assert (or l614m (and (not l612m) (= l614c l612c)) (and (not l613m) (= l614c l613c)))) (define-fun f298m () Bool l614m) (define-fun f298c () Int l614c) (declare-fun l615m () Bool) (declare-fun l615c () Int) (assert (= l615m (or f50m f292m))) (assert (or l615m (= l615c (+ f50c f292c)))) (declare-fun l616m () Bool) (declare-fun l616c () Int) (assert (= l616m (or f51m f293m))) (assert (or l616m (= l616c (+ f51c f293c)))) (declare-fun l617m () Bool) (declare-fun l617c () Int) (assert (= l617m (and l615m l616m))) (assert (and (or l617m l615m (>= l617c l615c)) (or l617m l616m (>= l617c l616c)))) (assert (or l617m (and (not l615m) (= l617c l615c)) (and (not l616m) (= l617c l616c)))) (define-fun f299m () Bool l617m) (define-fun f299c () Int l617c) (declare-fun l618m () Bool) (declare-fun l618c () Int) (assert (= l618m (and f52m f298m))) (assert (and (or l618m f52m (>= l618c f52c)) (or l618m f298m (>= l618c f298c)))) (assert (or l618m (and (not f52m) (= l618c f52c)) (and (not f298m) (= l618c f298c)))) (define-fun f300m () Bool l618m) (define-fun f300c () Int l618c) (declare-fun l619m () Bool) (declare-fun l619c () Int) (assert (= l619m (and f53m f299m))) (assert (and (or l619m f53m (>= l619c f53c)) (or l619m f299m (>= l619c f299c)))) (assert (or l619m (and (not f53m) (= l619c f53c)) (and (not f299m) (= l619c f299c)))) (define-fun f301m () Bool l619m) (define-fun f301c () Int l619c) (declare-fun l620m () Bool) (declare-fun l620c () Int) (assert (= l620m (or f48m f294m))) (assert (or l620m (= l620c (+ f48c f294c)))) (declare-fun l621m () Bool) (declare-fun l621c () Int) (assert (= l621m (or f49m f296m))) (assert (or l621m (= l621c (+ f49c f296c)))) (declare-fun l622m () Bool) (declare-fun l622c () Int) (assert (= l622m (and l620m l621m))) (assert (and (or l622m l620m (>= l622c l620c)) (or l622m l621m (>= l622c l621c)))) (assert (or l622m (and (not l620m) (= l622c l620c)) (and (not l621m) (= l622c l621c)))) (define-fun f302m () Bool l622m) (define-fun f302c () Int l622c) (declare-fun l623m () Bool) (declare-fun l623c () Int) (assert (= l623m (or f48m f295m))) (assert (or l623m (= l623c (+ f48c f295c)))) (declare-fun l624m () Bool) (declare-fun l624c () Int) (assert (= l624m (or f49m f297m))) (assert (or l624m (= l624c (+ f49c f297c)))) (declare-fun l625m () Bool) (declare-fun l625c () Int) (assert (= l625m (and l623m l624m))) (assert (and (or l625m l623m (>= l625c l623c)) (or l625m l624m (>= l625c l624c)))) (assert (or l625m (and (not l623m) (= l625c l623c)) (and (not l624m) (= l625c l624c)))) (define-fun f303m () Bool l625m) (define-fun f303c () Int l625c) (declare-fun l626m () Bool) (declare-fun l626c () Int) (assert (= l626m (or f50m f294m))) (assert (or l626m (= l626c (+ f50c f294c)))) (declare-fun l627m () Bool) (declare-fun l627c () Int) (assert (= l627m (or f51m f296m))) (assert (or l627m (= l627c (+ f51c f296c)))) (declare-fun l628m () Bool) (declare-fun l628c () Int) (assert (= l628m (and l626m l627m))) (assert (and (or l628m l626m (>= l628c l626c)) (or l628m l627m (>= l628c l627c)))) (assert (or l628m (and (not l626m) (= l628c l626c)) (and (not l627m) (= l628c l627c)))) (define-fun f304m () Bool l628m) (define-fun f304c () Int l628c) (declare-fun l629m () Bool) (declare-fun l629c () Int) (assert (= l629m (or f50m f295m))) (assert (or l629m (= l629c (+ f50c f295c)))) (declare-fun l630m () Bool) (declare-fun l630c () Int) (assert (= l630m (or f51m f297m))) (assert (or l630m (= l630c (+ f51c f297c)))) (declare-fun l631m () Bool) (declare-fun l631c () Int) (assert (= l631m (and l629m l630m))) (assert (and (or l631m l629m (>= l631c l629c)) (or l631m l630m (>= l631c l630c)))) (assert (or l631m (and (not l629m) (= l631c l629c)) (and (not l630m) (= l631c l630c)))) (define-fun f305m () Bool l631m) (define-fun f305c () Int l631c) (declare-fun l632m () Bool) (declare-fun l632c () Int) (assert (= l632m (or f48m f300m))) (assert (or l632m (= l632c (+ f48c f300c)))) (declare-fun l633m () Bool) (declare-fun l633c () Int) (assert (= l633m (or f49m f301m))) (assert (or l633m (= l633c (+ f49c f301c)))) (declare-fun l634m () Bool) (declare-fun l634c () Int) (assert (= l634m (and l632m l633m))) (assert (and (or l634m l632m (>= l634c l632c)) (or l634m l633m (>= l634c l633c)))) (assert (or l634m (and (not l632m) (= l634c l632c)) (and (not l633m) (= l634c l633c)))) (define-fun f306m () Bool l634m) (define-fun f306c () Int l634c) (declare-fun l635m () Bool) (declare-fun l635c () Int) (assert (= l635m (or f50m f300m))) (assert (or l635m (= l635c (+ f50c f300c)))) (declare-fun l636m () Bool) (declare-fun l636c () Int) (assert (= l636m (or f51m f301m))) (assert (or l636m (= l636c (+ f51c f301c)))) (declare-fun l637m () Bool) (declare-fun l637c () Int) (assert (= l637m (and l635m l636m))) (assert (and (or l637m l635m (>= l637c l635c)) (or l637m l636m (>= l637c l636c)))) (assert (or l637m (and (not l635m) (= l637c l635c)) (and (not l636m) (= l637c l636c)))) (define-fun f307m () Bool l637m) (define-fun f307c () Int l637c) (declare-fun l638m () Bool) (declare-fun l638c () Int) (assert (= l638m (and f52m f306m))) (assert (and (or l638m f52m (>= l638c f52c)) (or l638m f306m (>= l638c f306c)))) (assert (or l638m (and (not f52m) (= l638c f52c)) (and (not f306m) (= l638c f306c)))) (define-fun f308m () Bool l638m) (define-fun f308c () Int l638c) (declare-fun l639m () Bool) (declare-fun l639c () Int) (assert (= l639m (and f53m f307m))) (assert (and (or l639m f53m (>= l639c f53c)) (or l639m f307m (>= l639c f307c)))) (assert (or l639m (and (not f53m) (= l639c f53c)) (and (not f307m) (= l639c f307c)))) (define-fun f309m () Bool l639m) (define-fun f309c () Int l639c) (declare-fun l640m () Bool) (declare-fun l640c () Int) (assert (= l640m (or f36m f6m))) (assert (or l640m (= l640c (+ f36c f6c)))) (declare-fun l641m () Bool) (declare-fun l641c () Int) (assert (= l641m (or f37m f8m))) (assert (or l641m (= l641c (+ f37c f8c)))) (declare-fun l642m () Bool) (declare-fun l642c () Int) (assert (= l642m (and l640m l641m))) (assert (and (or l642m l640m (>= l642c l640c)) (or l642m l641m (>= l642c l641c)))) (assert (or l642m (and (not l640m) (= l642c l640c)) (and (not l641m) (= l642c l641c)))) (define-fun f310m () Bool l642m) (define-fun f310c () Int l642c) (declare-fun l643m () Bool) (declare-fun l643c () Int) (assert (= l643m (or f36m f7m))) (assert (or l643m (= l643c (+ f36c f7c)))) (declare-fun l644m () Bool) (declare-fun l644c () Int) (assert (= l644m (or f37m f9m))) (assert (or l644m (= l644c (+ f37c f9c)))) (declare-fun l645m () Bool) (declare-fun l645c () Int) (assert (= l645m (and l643m l644m))) (assert (and (or l645m l643m (>= l645c l643c)) (or l645m l644m (>= l645c l644c)))) (assert (or l645m (and (not l643m) (= l645c l643c)) (and (not l644m) (= l645c l644c)))) (define-fun f311m () Bool l645m) (define-fun f311c () Int l645c) (declare-fun l646m () Bool) (declare-fun l646c () Int) (assert (= l646m (or f38m f6m))) (assert (or l646m (= l646c (+ f38c f6c)))) (declare-fun l647m () Bool) (declare-fun l647c () Int) (assert (= l647m (or f39m f8m))) (assert (or l647m (= l647c (+ f39c f8c)))) (declare-fun l648m () Bool) (declare-fun l648c () Int) (assert (= l648m (and l646m l647m))) (assert (and (or l648m l646m (>= l648c l646c)) (or l648m l647m (>= l648c l647c)))) (assert (or l648m (and (not l646m) (= l648c l646c)) (and (not l647m) (= l648c l647c)))) (define-fun f312m () Bool l648m) (define-fun f312c () Int l648c) (declare-fun l649m () Bool) (declare-fun l649c () Int) (assert (= l649m (or f38m f7m))) (assert (or l649m (= l649c (+ f38c f7c)))) (declare-fun l650m () Bool) (declare-fun l650c () Int) (assert (= l650m (or f39m f9m))) (assert (or l650m (= l650c (+ f39c f9c)))) (declare-fun l651m () Bool) (declare-fun l651c () Int) (assert (= l651m (and l649m l650m))) (assert (and (or l651m l649m (>= l651c l649c)) (or l651m l650m (>= l651c l650c)))) (assert (or l651m (and (not l649m) (= l651c l649c)) (and (not l650m) (= l651c l650c)))) (define-fun f313m () Bool l651m) (define-fun f313c () Int l651c) (declare-fun l652m () Bool) (declare-fun l652c () Int) (assert (= l652m (or f36m f10m))) (assert (or l652m (= l652c (+ f36c f10c)))) (declare-fun l653m () Bool) (declare-fun l653c () Int) (assert (= l653m (or f37m f11m))) (assert (or l653m (= l653c (+ f37c f11c)))) (declare-fun l654m () Bool) (declare-fun l654c () Int) (assert (= l654m (and l652m l653m))) (assert (and (or l654m l652m (>= l654c l652c)) (or l654m l653m (>= l654c l653c)))) (assert (or l654m (and (not l652m) (= l654c l652c)) (and (not l653m) (= l654c l653c)))) (define-fun f314m () Bool l654m) (define-fun f314c () Int l654c) (declare-fun l655m () Bool) (declare-fun l655c () Int) (assert (= l655m (or f38m f10m))) (assert (or l655m (= l655c (+ f38c f10c)))) (declare-fun l656m () Bool) (declare-fun l656c () Int) (assert (= l656m (or f39m f11m))) (assert (or l656m (= l656c (+ f39c f11c)))) (declare-fun l657m () Bool) (declare-fun l657c () Int) (assert (= l657m (and l655m l656m))) (assert (and (or l657m l655m (>= l657c l655c)) (or l657m l656m (>= l657c l656c)))) (assert (or l657m (and (not l655m) (= l657c l655c)) (and (not l656m) (= l657c l656c)))) (define-fun f315m () Bool l657m) (define-fun f315c () Int l657c) (declare-fun l658m () Bool) (declare-fun l658c () Int) (assert (= l658m (and f40m f314m))) (assert (and (or l658m f40m (>= l658c f40c)) (or l658m f314m (>= l658c f314c)))) (assert (or l658m (and (not f40m) (= l658c f40c)) (and (not f314m) (= l658c f314c)))) (define-fun f316m () Bool l658m) (define-fun f316c () Int l658c) (declare-fun l659m () Bool) (declare-fun l659c () Int) (assert (= l659m (and f41m f315m))) (assert (and (or l659m f41m (>= l659c f41c)) (or l659m f315m (>= l659c f315c)))) (assert (or l659m (and (not f41m) (= l659c f41c)) (and (not f315m) (= l659c f315c)))) (define-fun f317m () Bool l659m) (define-fun f317c () Int l659c) (declare-fun l660m () Bool) (declare-fun l660c () Int) (assert (= l660m (or f36m f36m))) (assert (or l660m (= l660c (+ f36c f36c)))) (declare-fun l661m () Bool) (declare-fun l661c () Int) (assert (= l661m (or f37m f38m))) (assert (or l661m (= l661c (+ f37c f38c)))) (declare-fun l662m () Bool) (declare-fun l662c () Int) (assert (= l662m (and l660m l661m))) (assert (and (or l662m l660m (>= l662c l660c)) (or l662m l661m (>= l662c l661c)))) (assert (or l662m (and (not l660m) (= l662c l660c)) (and (not l661m) (= l662c l661c)))) (define-fun f318m () Bool l662m) (define-fun f318c () Int l662c) (declare-fun l663m () Bool) (declare-fun l663c () Int) (assert (= l663m (or f36m f37m))) (assert (or l663m (= l663c (+ f36c f37c)))) (declare-fun l664m () Bool) (declare-fun l664c () Int) (assert (= l664m (or f37m f39m))) (assert (or l664m (= l664c (+ f37c f39c)))) (declare-fun l665m () Bool) (declare-fun l665c () Int) (assert (= l665m (and l663m l664m))) (assert (and (or l665m l663m (>= l665c l663c)) (or l665m l664m (>= l665c l664c)))) (assert (or l665m (and (not l663m) (= l665c l663c)) (and (not l664m) (= l665c l664c)))) (define-fun f319m () Bool l665m) (define-fun f319c () Int l665c) (declare-fun l666m () Bool) (declare-fun l666c () Int) (assert (= l666m (or f38m f36m))) (assert (or l666m (= l666c (+ f38c f36c)))) (declare-fun l667m () Bool) (declare-fun l667c () Int) (assert (= l667m (or f39m f38m))) (assert (or l667m (= l667c (+ f39c f38c)))) (declare-fun l668m () Bool) (declare-fun l668c () Int) (assert (= l668m (and l666m l667m))) (assert (and (or l668m l666m (>= l668c l666c)) (or l668m l667m (>= l668c l667c)))) (assert (or l668m (and (not l666m) (= l668c l666c)) (and (not l667m) (= l668c l667c)))) (define-fun f320m () Bool l668m) (define-fun f320c () Int l668c) (declare-fun l669m () Bool) (declare-fun l669c () Int) (assert (= l669m (or f38m f37m))) (assert (or l669m (= l669c (+ f38c f37c)))) (declare-fun l670m () Bool) (declare-fun l670c () Int) (assert (= l670m (or f39m f39m))) (assert (or l670m (= l670c (+ f39c f39c)))) (declare-fun l671m () Bool) (declare-fun l671c () Int) (assert (= l671m (and l669m l670m))) (assert (and (or l671m l669m (>= l671c l669c)) (or l671m l670m (>= l671c l670c)))) (assert (or l671m (and (not l669m) (= l671c l669c)) (and (not l670m) (= l671c l670c)))) (define-fun f321m () Bool l671m) (define-fun f321c () Int l671c) (declare-fun l672m () Bool) (declare-fun l672c () Int) (assert (= l672m (or f36m f40m))) (assert (or l672m (= l672c (+ f36c f40c)))) (declare-fun l673m () Bool) (declare-fun l673c () Int) (assert (= l673m (or f37m f41m))) (assert (or l673m (= l673c (+ f37c f41c)))) (declare-fun l674m () Bool) (declare-fun l674c () Int) (assert (= l674m (and l672m l673m))) (assert (and (or l674m l672m (>= l674c l672c)) (or l674m l673m (>= l674c l673c)))) (assert (or l674m (and (not l672m) (= l674c l672c)) (and (not l673m) (= l674c l673c)))) (define-fun f322m () Bool l674m) (define-fun f322c () Int l674c) (declare-fun l675m () Bool) (declare-fun l675c () Int) (assert (= l675m (or f38m f40m))) (assert (or l675m (= l675c (+ f38c f40c)))) (declare-fun l676m () Bool) (declare-fun l676c () Int) (assert (= l676m (or f39m f41m))) (assert (or l676m (= l676c (+ f39c f41c)))) (declare-fun l677m () Bool) (declare-fun l677c () Int) (assert (= l677m (and l675m l676m))) (assert (and (or l677m l675m (>= l677c l675c)) (or l677m l676m (>= l677c l676c)))) (assert (or l677m (and (not l675m) (= l677c l675c)) (and (not l676m) (= l677c l676c)))) (define-fun f323m () Bool l677m) (define-fun f323c () Int l677c) (declare-fun l678m () Bool) (declare-fun l678c () Int) (assert (= l678m (and f40m f322m))) (assert (and (or l678m f40m (>= l678c f40c)) (or l678m f322m (>= l678c f322c)))) (assert (or l678m (and (not f40m) (= l678c f40c)) (and (not f322m) (= l678c f322c)))) (define-fun f324m () Bool l678m) (define-fun f324c () Int l678c) (declare-fun l679m () Bool) (declare-fun l679c () Int) (assert (= l679m (and f41m f323m))) (assert (and (or l679m f41m (>= l679c f41c)) (or l679m f323m (>= l679c f323c)))) (assert (or l679m (and (not f41m) (= l679c f41c)) (and (not f323m) (= l679c f323c)))) (define-fun f325m () Bool l679m) (define-fun f325c () Int l679c) (assert (and (and (and (and (or f0m (and (not f54m) (>= f54c f0c))) (or f1m (and (not f55m) (>= f55c f1c)))) (and (or f2m (and (not f56m) (>= f56c f2c))) (or f3m (and (not f57m) (>= f57c f3c))))) (and (or f4m (and (not f60m) (>= f60c f4c))) (or f5m (and (not f61m) (>= f61c f5c))))) (and (and (and (or f12m (and (not f62m) (>= f62c f12c))) (or f13m (and (not f63m) (>= f63c f13c)))) (and (or f14m (and (not f64m) (>= f64c f14c))) (or f15m (and (not f65m) (>= f65c f15c))))) (and (or f16m (and (not f68m) (>= f68c f16c))) (or f17m (and (not f69m) (>= f69c f17c))))) (and (and (and (or f24m (and (not f70m) (>= f70c f24c))) (or f25m (and (not f71m) (>= f71c f25c)))) (and (or f26m (and (not f72m) (>= f72c f26c))) (or f27m (and (not f73m) (>= f73c f27c))))) (and (or f28m (and (not f76m) (>= f76c f28c))) (or f29m (and (not f77m) (>= f77c f29c))))) (and (and (and (or f94m (and (not f78m) (>= f78c f94c))) (or f95m (and (not f79m) (>= f79c f95c)))) (and (or f96m (and (not f80m) (>= f80c f96c))) (or f97m (and (not f81m) (>= f81c f97c))))) (and (or f100m (and (not f84m) (>= f84c f100c))) (or f101m (and (not f85m) (>= f85c f101c))))) (and (and (and (or f118m (and (not f102m) (>= f102c f118c))) (or f119m (and (not f103m) (>= f103c f119c)))) (and (or f120m (and (not f104m) (>= f104c f120c))) (or f121m (and (not f105m) (>= f105c f121c))))) (and (or f124m (and (not f108m) (>= f108c f124c))) (or f125m (and (not f109m) (>= f109c f125c))))) (and (and (and (or f142m (and (not f126m) (>= f126c f142c))) (or f143m (and (not f127m) (>= f127c f143c)))) (and (or f144m (and (not f128m) (>= f128c f144c))) (or f145m (and (not f129m) (>= f129c f145c))))) (and (or f148m (and (not f132m) (>= f132c f148c))) (or f149m (and (not f133m) (>= f133c f149c))))) (and (and (and (or f174m (and (not f150m) (>= f150c f174c))) (or f175m (and (not f151m) (>= f151c f175c)))) (and (or f176m (and (not f152m) (>= f152c f176c))) (or f177m (and (not f153m) (>= f153c f177c))))) (and (or f180m (and (not f156m) (>= f156c f180c))) (or f181m (and (not f157m) (>= f157c f181c))))) (and (and (and (or f198m (and (not f182m) (>= f182c f198c))) (or f199m (and (not f183m) (>= f183c f199c)))) (and (or f200m (and (not f184m) (>= f184c f200c))) (or f201m (and (not f185m) (>= f185c f201c))))) (and (or f204m (and (not f188m) (>= f188c f204c))) (or f205m (and (not f189m) (>= f189c f205c))))) (and (and (and (or f246m (and (not f222m) (>= f222c f246c))) (or f247m (and (not f223m) (>= f223c f247c)))) (and (or f248m (and (not f224m) (>= f224c f248c))) (or f249m (and (not f225m) (>= f225c f249c))))) (and (or f252m (and (not f228m) (>= f228c f252c))) (or f253m (and (not f229m) (>= f229c f253c))))) (and (and (and (or f302m (and (not f270m) (>= f270c f302c))) (or f303m (and (not f271m) (>= f271c f303c)))) (and (or f304m (and (not f272m) (>= f272c f304c))) (or f305m (and (not f273m) (>= f273c f305c))))) (and (or f308m (and (not f276m) (>= f276c f308c))) (or f309m (and (not f277m) (>= f277c f309c))))) (and (and (and (or f318m (and (not f310m) (>= f310c f318c))) (or f319m (and (not f311m) (>= f311c f319c)))) (and (or f320m (and (not f312m) (>= f312c f320c))) (or f321m (and (not f313m) (>= f313c f321c))))) (and (or f324m (and (not f316m) (>= f316c f324c))) (or f325m (and (not f317m) (>= f317c f325c))))))) (assert (or (and (and (and (or f0m (and (not f54m) (> f54c f0c))) (or f1m (and (not f55m) (> f55c f1c)))) (and (or f2m (and (not f56m) (> f56c f2c))) (or f3m (and (not f57m) (> f57c f3c))))) (and (or f4m (and (not f60m) (> f60c f4c))) (or f5m (and (not f61m) (> f61c f5c))))) (and (and (and (or f12m (and (not f62m) (> f62c f12c))) (or f13m (and (not f63m) (> f63c f13c)))) (and (or f14m (and (not f64m) (> f64c f14c))) (or f15m (and (not f65m) (> f65c f15c))))) (and (or f16m (and (not f68m) (> f68c f16c))) (or f17m (and (not f69m) (> f69c f17c))))) (and (and (and (or f24m (and (not f70m) (> f70c f24c))) (or f25m (and (not f71m) (> f71c f25c)))) (and (or f26m (and (not f72m) (> f72c f26c))) (or f27m (and (not f73m) (> f73c f27c))))) (and (or f28m (and (not f76m) (> f76c f28c))) (or f29m (and (not f77m) (> f77c f29c))))))) (check-sat) (get-value (f0m f0c f1m f1c f2m f2c f3m f3c f4m f4c f5m f5c f6m f6c f7m f7c f8m f8c f9m f9c f10m f10c f11m f11c f12m f12c f13m f13c f14m f14c f15m f15c f16m f16c f17m f17c f18m f18c f19m f19c f20m f20c f21m f21c f22m f22c f23m f23c f24m f24c f25m f25c f26m f26c f27m f27c f28m f28c f29m f29c f30m f30c f31m f31c f32m f32c f33m f33c f34m f34c f35m f35c f36m f36c f37m f37c f38m f38c f39m f39c f40m f40c f41m f41c f42m f42c f43m f43c f44m f44c f45m f45c f46m f46c f47m f47c f48m f48c f49m f49c f50m f50c f51m f51c f52m f52c f53m f53c f54m f54c f55m f55c f56m f56c f57m f57c f58m f58c f59m f59c f60m f60c f61m f61c f62m f62c f63m f63c f64m f64c f65m f65c f66m f66c f67m f67c f68m f68c f69m f69c f70m f70c f71m f71c f72m f72c f73m f73c f74m f74c f75m f75c f76m f76c f77m f77c f78m f78c f79m f79c f80m f80c f81m f81c f82m f82c f83m f83c f84m f84c f85m f85c f86m f86c f87m f87c f88m f88c f89m f89c f90m f90c f91m f91c f92m f92c f93m f93c f94m f94c f95m f95c f96m f96c f97m f97c f98m f98c f99m f99c f100m f100c f101m f101c f102m f102c f103m f103c f104m f104c f105m f105c f106m f106c f107m f107c f108m f108c f109m f109c f110m f110c f111m f111c f112m f112c f113m f113c f114m f114c f115m f115c f116m f116c f117m f117c f118m f118c f119m f119c f120m f120c f121m f121c f122m f122c f123m f123c f124m f124c f125m f125c f126m f126c f127m f127c f128m f128c f129m f129c f130m f130c f131m f131c f132m f132c f133m f133c f134m f134c f135m f135c f136m f136c f137m f137c f138m f138c f139m f139c f140m f140c f141m f141c f142m f142c f143m f143c f144m f144c f145m f145c f146m f146c f147m f147c f148m f148c f149m f149c f150m f150c f151m f151c f152m f152c f153m f153c f154m f154c f155m f155c f156m f156c f157m f157c f158m f158c f159m f159c f160m f160c f161m f161c f162m f162c f163m f163c f164m f164c f165m f165c f166m f166c f167m f167c f168m f168c f169m f169c f170m f170c f171m f171c f172m f172c f173m f173c f174m f174c f175m f175c f176m f176c f177m f177c f178m f178c f179m f179c f180m f180c f181m f181c f182m f182c f183m f183c f184m f184c f185m f185c f186m f186c f187m f187c f188m f188c f189m f189c f190m f190c f191m f191c f192m f192c f193m f193c f194m f194c f195m f195c f196m f196c f197m f197c f198m f198c f199m f199c f200m f200c f201m f201c f202m f202c f203m f203c f204m f204c f205m f205c f206m f206c f207m f207c f208m f208c f209m f209c f210m f210c f211m f211c f212m f212c f213m f213c f214m f214c f215m f215c f216m f216c f217m f217c f218m f218c f219m f219c f220m f220c f221m f221c f222m f222c f223m f223c f224m f224c f225m f225c f226m f226c f227m f227c f228m f228c f229m f229c f230m f230c f231m f231c f232m f232c f233m f233c f234m f234c f235m f235c f236m f236c f237m f237c f238m f238c f239m f239c f240m f240c f241m f241c f242m f242c f243m f243c f244m f244c f245m f245c f246m f246c f247m f247c f248m f248c f249m f249c f250m f250c f251m f251c f252m f252c f253m f253c f254m f254c f255m f255c f256m f256c f257m f257c f258m f258c f259m f259c f260m f260c f261m f261c f262m f262c f263m f263c f264m f264c f265m f265c f266m f266c f267m f267c f268m f268c f269m f269c f270m f270c f271m f271c f272m f272c f273m f273c f274m f274c f275m f275c f276m f276c f277m f277c f278m f278c f279m f279c f280m f280c f281m f281c f282m f282c f283m f283c f284m f284c f285m f285c f286m f286c f287m f287c f288m f288c f289m f289c f290m f290c f291m f291c f292m f292c f293m f293c f294m f294c f295m f295c f296m f296c f297m f297c f298m f298c f299m f299c f300m f300c f301m f301c f302m f302c f303m f303c f304m f304c f305m f305c f306m f306c f307m f307c f308m f308c f309m f309c f310m f310c f311m f311c f312m f312c f313m f313c f314m f314c f315m f315c f316m f316c f317m f317c f318m f318c f319m f319c f320m f320c f321m f321c f322m f322c f323m f323c f324m f324c f325m f325c))