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