Commit ae7d0122 authored by Mathias Preiner's avatar Mathias Preiner
Browse files

Squashed commit of the following:

commit 05f95548
Author: Mathias Preiner <mathias.preiner@gmail.com>
Date:   Tue May 17 13:01:57 2022 -0700

    Add 2022 submissions.
parent b884d2a8
This diff is collapsed.
This diff is collapsed.
(set-info :smt-lib-version 2.6)
(set-logic QF_IDL)
(set-info :source | The instance is generated by a runtime predictive analysis system called RVPredict
This problem was added to SMT-LIB by Bohan Li.|)
(set-info :license "https://creativecommons.org/licenses/by/4.0/")
(set-info :category "industrial")
(set-info :status sat)
(declare-fun x2268370 () Int)
(declare-fun x2268375 () Int)
(declare-fun x2268379 () Int)
(declare-fun x2268384 () Int)
(declare-fun x2269583 () Int)
(declare-fun x2269586 () Int)
(declare-fun x2269597 () Int)
(declare-fun x2269640 () Int)
(declare-fun x2269656 () Int)
(declare-fun x2269754 () Int)
(declare-fun x2269773 () Int)
(declare-fun x2269890 () Int)
(declare-fun x2269968 () Int)
(declare-fun x2269987 () Int)
(declare-fun x2270051 () Int)
(declare-fun x2270067 () Int)
(declare-fun x2270124 () Int)
(declare-fun x2270143 () Int)
(declare-fun x2270303 () Int)
(declare-fun x2270320 () Int)
(declare-fun x2270338 () Int)
(declare-fun x2270362 () Int)
(declare-fun x2270527 () Int)
(declare-fun x2270543 () Int)
(declare-fun x2270817 () Int)
(declare-fun x2270834 () Int)
(declare-fun x2270843 () Int)
(declare-fun x2271766 () Int)
(declare-fun x2273501 () Int)
(declare-fun x2273504 () Int)
(declare-fun x2273506 () Int)
(declare-fun x2273569 () Int)
(declare-fun x2273573 () Int)
(declare-fun x2273736 () Int)
(declare-fun x2273756 () Int)
(declare-fun x2274113 () Int)
(declare-fun x2274242 () Int)
(declare-fun x2274246 () Int)
(declare-fun x2274313 () Int)
(declare-fun x2274328 () Int)
(declare-fun x2274332 () Int)
(declare-fun x2274584 () Int)
(declare-fun x2274589 () Int)
(declare-fun x2274730 () Int)
(declare-fun x2274734 () Int)
(declare-fun x2274751 () Int)
(declare-fun x2275074 () Int)
(declare-fun x2275079 () Int)
(declare-fun x2275081 () Int)
(declare-fun x2275083 () Int)
(declare-fun x2275129 () Int)
(declare-fun x2275133 () Int)
(declare-fun x2275166 () Int)
(declare-fun x2275169 () Int)
(declare-fun x2295309 () Int)
(declare-fun x2295312 () Int)
(declare-fun x2295316 () Int)
(declare-fun x2295322 () Int)
(declare-fun x2295323 () Int)
(declare-fun x2295325 () Int)
(declare-fun x2295326 () Int)
(declare-fun x2295327 () Int)
(declare-fun x2295329 () Int)
(declare-fun x2295333 () Int)
(declare-fun x2295334 () Int)
(declare-fun x2295335 () Int)
(declare-fun x2295338 () Int)
(declare-fun x2295339 () Int)
(declare-fun x2295340 () Int)
(declare-fun x2295342 () Int)
(declare-fun x2295343 () Int)
(declare-fun x2295345 () Int)
(declare-fun x2295350 () Int)
(declare-fun x2295355 () Int)
(declare-fun x2295358 () Int)
(declare-fun x2295376 () Int)
(declare-fun x2295379 () Int)
(declare-fun x2295422 () Int)
(declare-fun x2295463 () Int)
(declare-fun x2295465 () Int)
(declare-fun x2295467 () Int)
(declare-fun x2295468 () Int)
(declare-fun x2295471 () Int)
(declare-fun x2295472 () Int)
(declare-fun x2295474 () Int)
(declare-fun x2295478 () Int)
(declare-fun x2295480 () Int)
(declare-fun x2295484 () Int)
(declare-fun x2295488 () Int)
(declare-fun x2295515 () Int)
(declare-fun x2295519 () Int)
(declare-fun x2295523 () Int)
(declare-fun x2295530 () Int)
(declare-fun x2295536 () Int)
(declare-fun x2295568 () Int)
(declare-fun x2295571 () Int)
(declare-fun x2295572 () Int)
(declare-fun x2295574 () Int)
(declare-fun x2295577 () Int)
(declare-fun x2295578 () Int)
(declare-fun x2295580 () Int)
(declare-fun x2295583 () Int)
(declare-fun x2295587 () Int)
(declare-fun x2295618 () Int)
(declare-fun x2295622 () Int)
(declare-fun x2295649 () Int)
(declare-fun x2295755 () Int)
(declare-fun x2295759 () Int)
(declare-fun x2295760 () Int)
(declare-fun x2295761 () Int)
(declare-fun x2295762 () Int)
(declare-fun x2295765 () Int)
(declare-fun x2295766 () Int)
(declare-fun x2295768 () Int)
(declare-fun x2295769 () Int)
(declare-fun x2295773 () Int)
(declare-fun x2295774 () Int)
(declare-fun x2295777 () Int)
(declare-fun x2295778 () Int)
(declare-fun x2295780 () Int)
(declare-fun x2295783 () Int)
(declare-fun x2295786 () Int)
(declare-fun x2295831 () Int)
(declare-fun x2295835 () Int)
(declare-fun x2295877 () Int)
(declare-fun x2295879 () Int)
(declare-fun x2295933 () Int)
(declare-fun x2295970 () Int)
(declare-fun x2296016 () Int)
(declare-fun x2296030 () Int)
(declare-fun x2296037 () Int)
(declare-fun x2296051 () Int)
(declare-fun x2296061 () Int)
(declare-fun x2296090 () Int)
(declare-fun x2296128 () Int)
(declare-fun x2296130 () Int)
(declare-fun x2296139 () Int)
(declare-fun x2296147 () Int)
(declare-fun x2296184 () Int)
(declare-fun x2296310 () Int)
(assert
(> x2270124 x2268370)
)
(assert
(> x2270143 x2268379)
)
(assert
(> x2269640 x2268370)
)
(assert
(> x2269656 x2268379)
)
(assert (< x2270817 x2270834))
(assert (< x2270834 x2275166))
(assert (< x2275166 x2275169))
(assert (< x2275169 x2295358))
(assert (< x2295358 x2295463))
(assert (< x2295463 x2295465))
(assert (< x2295465 x2295467))
(assert (< x2295467 x2295471))
(assert (< x2295471 x2295879))
(assert (< x2295879 x2296016))
(assert (< x2270051 x2270067))
(assert (< x2270067 x2274328))
(assert (< x2274328 x2274332))
(assert (< x2274332 x2295474))
(assert (< x2295474 x2295478))
(assert (< x2295478 x2295480))
(assert (< x2295480 x2295484))
(assert (< x2295484 x2295488))
(assert (< x2295488 x2295530))
(assert (< x2295530 x2295536))
(assert (< x2295536 x2295571))
(assert (< x2295571 x2296051))
(assert (< x2270843 x2271766))
(assert (< x2271766 x2275074))
(assert (< x2275074 x2275079))
(assert (< x2275079 x2295329))
(assert (< x2295329 x2295333))
(assert (< x2295333 x2295335))
(assert (< x2295335 x2295339))
(assert (< x2295339 x2295343))
(assert (< x2295343 x2295376))
(assert (< x2295376 x2295379))
(assert (< x2295379 x2295422))
(assert (< x2295422 x2296030))
(assert (< x2270527 x2270543))
(assert (< x2270543 x2274751))
(assert (< x2270338 x2270362))
(assert (< x2270362 x2274584))
(assert (< x2274584 x2274589))
(assert (< x2274589 x2295468))
(assert (< x2295468 x2295472))
(assert (< x2295472 x2295568))
(assert (< x2295568 x2295572))
(assert (< x2295572 x2295577))
(assert (< x2295577 x2295618))
(assert (< x2295618 x2295622))
(assert (< x2295622 x2295649))
(assert (< x2295649 x2295760))
(assert (< x2268370 x2268375))
(assert (< x2268375 x2268379))
(assert (< x2268379 x2268384))
(assert (< x2268384 x2269754))
(assert (< x2269754 x2269773))
(assert (< x2269773 x2273501))
(assert (< x2273501 x2273504))
(assert (< x2273504 x2273506))
(assert (< x2273506 x2295309))
(assert (< x2295309 x2295312))
(assert (< x2295312 x2295316))
(assert (< x2295316 x2295322))
(assert (< x2295322 x2295325))
(assert (< x2295325 x2295327))
(assert (< x2295327 x2295515))
(assert (< x2295515 x2295519))
(assert (< x2295519 x2295523))
(assert (< x2295523 x2295831))
(assert (< x2295831 x2295835))
(assert (< x2295835 x2296130))
(assert (< x2296130 x2296310))
(assert (< x2269968 x2269987))
(assert (< x2269987 x2275129))
(assert (< x2275129 x2275133))
(assert (< x2275133 x2295574))
(assert (< x2295574 x2295578))
(assert (< x2295578 x2295580))
(assert (< x2295580 x2295583))
(assert (< x2295583 x2295587))
(assert (< x2295587 x2296037))
(assert (< x2296037 x2296184))
(assert (< x2270124 x2270143))
(assert (< x2270143 x2274242))
(assert (< x2274242 x2274246))
(assert (< x2274246 x2295773))
(assert (< x2295773 x2295777))
(assert (< x2295777 x2295780))
(assert (< x2295780 x2295783))
(assert (< x2295783 x2295786))
(assert (< x2295786 x2296061))
(assert (< x2296061 x2296139))
(assert (< x2269640 x2269656))
(assert (< x2269656 x2273569))
(assert (< x2273569 x2273573))
(assert (< x2273573 x2274113))
(assert (< x2274113 x2295323))
(assert (< x2295323 x2295326))
(assert (< x2295326 x2295334))
(assert (< x2295334 x2295338))
(assert (< x2295338 x2274242))
(assert (< x2274242 x2295342))
(assert (< x2295342 x2295345))
(assert (< x2295345 x2295350))
(assert (< x2295350 x2295355))
(assert (< x2295355 x2296090))
(assert (< x2296090 x2296128))
(assert (< x2270303 x2270320))
(assert (< x2270320 x2275081))
(assert (< x2275081 x2275083))
(assert (< x2275083 x2295755))
(assert (< x2295755 x2295759))
(assert (< x2295759 x2295762))
(assert (< x2295762 x2295765))
(assert (< x2295765 x2295769))
(assert (< x2295769 x2295933))
(assert (< x2295933 x2295970))
(assert (< x2269583 x2269890))
(assert (< x2269890 x2273736))
(assert (< x2273736 x2273756))
(assert (< x2273756 x2274313))
(assert (< x2269586 x2269597))
(assert (< x2269597 x2274730))
(assert (< x2274730 x2274734))
(assert (< x2274734 x2295761))
(assert (< x2295761 x2295766))
(assert (< x2295766 x2295768))
(assert (< x2295768 x2295774))
(assert (< x2295774 x2295778))
(assert (< x2295778 x2295877))
(assert (< x2295877 x2296147))
(assert (or (> x2273504 x2295333) (> x2275079 x2295327)))
(assert (or (> x2273504 x2295472) (> x2274589 x2295327)))
(assert (or (> x2273504 x2295478) (> x2274332 x2295327)))
(assert (or (> x2275079 x2295327) (> x2273504 x2295333)))
(assert (or (> x2275079 x2295472) (> x2274589 x2295333)))
(assert (or (> x2275079 x2295478) (> x2274332 x2295333)))
(assert (or (> x2274589 x2295327) (> x2273504 x2295472)))
(assert (or (> x2274589 x2295333) (> x2275079 x2295472)))
(assert (or (> x2274589 x2295478) (> x2274332 x2295472)))
(assert (or (> x2274332 x2295327) (> x2273504 x2295478)))
(assert (or (> x2274332 x2295333) (> x2275079 x2295478)))
(assert (or (> x2274332 x2295472) (> x2274589 x2295478)))
(assert (or (> x2273573 x2295463) (> x2275169 x2295342)))
(assert (or (> x2273573 x2295578) (> x2275133 x2295342)))
(assert (or (> x2273573 x2295759) (> x2275083 x2295342)))
(assert (or (> x2273573 x2295766) (> x2274734 x2295342)))
(assert (or (> x2273573 x2295777) (> x2274246 x2295342)))
(assert (or (> x2275169 x2295342) (> x2273573 x2295463)))
(assert (or (> x2275169 x2295578) (> x2275133 x2295463)))
(assert (or (> x2275169 x2295759) (> x2275083 x2295463)))
(assert (or (> x2275169 x2295766) (> x2274734 x2295463)))
(assert (or (> x2275169 x2295777) (> x2274246 x2295463)))
(assert (or (> x2275133 x2295342) (> x2273573 x2295578)))
(assert (or (> x2275133 x2295463) (> x2275169 x2295578)))
(assert (or (> x2275133 x2295759) (> x2275083 x2295578)))
(assert (or (> x2275133 x2295766) (> x2274734 x2295578)))
(assert (or (> x2275133 x2295777) (> x2274246 x2295578)))
(assert (or (> x2275083 x2295342) (> x2273573 x2295759)))
(assert (or (> x2275083 x2295463) (> x2275169 x2295759)))
(assert (or (> x2275083 x2295578) (> x2275133 x2295759)))
(assert (or (> x2275083 x2295766) (> x2274734 x2295759)))
(assert (or (> x2275083 x2295777) (> x2274246 x2295759)))
(assert (or (> x2274734 x2295342) (> x2273573 x2295766)))
(assert (or (> x2274734 x2295463) (> x2275169 x2295766)))
(assert (or (> x2274734 x2295578) (> x2275133 x2295766)))
(assert (or (> x2274734 x2295759) (> x2275083 x2295766)))
(assert (or (> x2274734 x2295777) (> x2274246 x2295766)))
(assert (or (> x2274246 x2295342) (> x2273573 x2295777)))
(assert (or (> x2274246 x2295463) (> x2275169 x2295777)))
(assert (or (> x2274246 x2295578) (> x2275133 x2295777)))
(assert (or (> x2274246 x2295759) (> x2275083 x2295777)))
(assert (or (> x2274246 x2295766) (> x2274734 x2295777)))
(check-sat)
(exit)
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
(set-info :smt-lib-version 2.6)
(set-logic QF_IDL)
(set-info :source | These instances are encoded from job shop scheduling problemencoded from job shop schedul-ing problem resembling 'https://clc-gitlab.cs.uiowa.edu:2443/SMT-LIB-benchmarks/QF_IDL/-/blob/master/job_shop/'.
Note that there exists a mistake in the encoding method of original instances, and we fix it in new instances.
This problem was added to SMT-LIB by Bohan Li.|)
(set-info :license "https://creativecommons.org/licenses/by/4.0/")
(set-info :category "crafted")
(set-info :status sat)
(declare-fun s1_1 () Int)
(declare-fun s1_2 () Int)
(declare-fun s2_1 () Int)
(declare-fun s2_2 () Int)
(declare-fun s3_1 () Int)
(declare-fun s3_2 () Int)
(declare-fun s4_1 () Int)
(declare-fun s4_2 () Int)
(declare-fun s5_1 () Int)
(declare-fun s5_2 () Int)
(declare-fun s6_1 () Int)
(declare-fun s6_2 () Int)
(declare-fun s7_1 () Int)
(declare-fun s7_2 () Int)
(declare-fun s8_1 () Int)
(declare-fun s8_2 () Int)
(declare-fun s9_1 () Int)
(declare-fun s9_2 () Int)
(declare-fun s10_1 () Int)
(declare-fun s10_2 () Int)
(declare-fun m1_1 () Int)
(declare-fun m1_2 () Int)
(declare-fun m2_1 () Int)
(declare-fun m2_2 () Int)
(declare-fun m3_1 () Int)
(declare-fun m3_2 () Int)
(declare-fun m4_1 () Int)
(declare-fun m4_2 () Int)
(declare-fun m5_1 () Int)
(declare-fun m5_2 () Int)
(declare-fun m6_1 () Int)
(declare-fun m6_2 () Int)
(declare-fun m7_1 () Int)
(declare-fun m7_2 () Int)
(declare-fun m8_1 () Int)
(declare-fun m8_2 () Int)
(declare-fun m9_1 () Int)
(declare-fun m9_2 () Int)
(declare-fun m10_1 () Int)
(declare-fun m10_2 () Int)
(declare-fun ref () Int)
(assert (and
(<= (- m1_1 ref) 4)
(>= (- m1_1 ref) 0)
(<= (- m1_2 ref) 4)
(>= (- m1_2 ref) 0)
(<= (- m2_1 ref) 4)
(>= (- m2_1 ref) 0)
(<= (- m2_2 ref) 4)
(>= (- m2_2 ref) 0)
(<= (- m3_1 ref) 4)
(>= (- m3_1 ref) 0)
(<= (- m3_2 ref) 4)
(>= (- m3_2 ref) 0)
(<= (- m4_1 ref) 4)
(>= (- m4_1 ref) 0)
(<= (- m4_2 ref) 4)
(>= (- m4_2 ref) 0)
(<= (- m5_1 ref) 4)
(>= (- m5_1 ref) 0)
(<= (- m5_2 ref) 4)
(>= (- m5_2 ref) 0)
(<= (- m6_1 ref) 4)
(>= (- m6_1 ref) 0)
(<= (- m6_2 ref) 4)
(>= (- m6_2 ref) 0)
(<= (- m7_1 ref) 4)
(>= (- m7_1 ref) 0)
(<= (- m7_2 ref) 4)
(>= (- m7_2 ref) 0)
(<= (- m8_1 ref) 4)
(>= (- m8_1 ref) 0)
(<= (- m8_2 ref) 4)
(>= (- m8_2 ref) 0)
(<= (- m9_1 ref) 4)
(>= (- m9_1 ref) 0)
(<= (- m9_2 ref) 4)
(>= (- m9_2 ref) 0)
(<= (- m10_1 ref) 4)
(>= (- m10_1 ref) 0)
(<= (- m10_2 ref) 4)
(>= (- m10_2 ref) 0)
(>= (- s1_1 ref) 0)
(>= (- s2_1 ref) 0)
(>= (- s3_1 ref) 0)
(>= (- s4_1 ref) 0)
(>= (- s5_1 ref) 0)
(>= (- s6_1 ref) 0)
(>= (- s7_1 ref) 0)
(>= (- s8_1 ref) 0)
(>= (- s9_1 ref) 0)
(>= (- s10_1 ref) 0)
(<= (- s1_2 ref) 9)
(<= (- s2_2 ref) 9)
(<= (- s3_2 ref) 9)
(<= (- s4_2 ref) 10)
(<= (- s5_2 ref) 9)
(<= (- s6_2 ref) 9)
(<= (- s7_2 ref) 9)
(<= (- s8_2 ref) 9)
(<= (- s9_2 ref) 10)
(<= (- s10_2 ref) 9)
(>= (- s1_2 s1_1) 3)
(>= (- s2_2 s2_1) 2)
(>= (- s3_2 s3_1) 4)
(>= (- s4_2 s4_1) 3)
(>= (- s5_2 s5_1) 2)
(>= (- s6_2 s6_1) 4)
(>= (- s7_2 s7_1) 4)
(>= (- s8_2 s8_1) 4)
(>= (- s9_2 s9_1) 2)
(>= (- s10_2 s10_1) 3)
(or (not (= (- m1_1 m2_1) 0)) (>= (- s1_1 s2_1) 2) (>= (- s2_1 s1_1) 3))
(or (not (= (- m1_1 m3_1) 0)) (>= (- s1_1 s3_1) 4) (>= (- s3_1 s1_1) 3))
(or (not (= (- m1_1 m4_1) 0)) (>= (- s1_1 s4_1) 3) (>= (- s4_1 s1_1) 3))
(or (not (= (- m1_1 m5_1) 0)) (>= (- s1_1 s5_1) 2) (>= (- s5_1 s1_1) 3))
(or (not (= (- m1_1 m6_1) 0)) (>= (- s1_1 s6_1) 4) (>= (- s6_1 s1_1) 3))
(or (not (= (- m1_1 m7_1) 0)) (>= (- s1_1 s7_1) 4) (>= (- s7_1 s1_1) 3))
(or (not (= (- m1_1 m8_1) 0)) (>= (- s1_1 s8_1) 4) (>= (- s8_1 s1_1) 3))
(or (not (= (- m1_1 m9_1) 0)) (>= (- s1_1 s9_1) 2) (>= (- s9_1 s1_1) 3))
(or (not (= (- m1_1 m10_1) 0)) (>= (- s1_1 s10_1) 3) (>= (- s10_1 s1_1) 3))
(or (not (= (- m2_1 m3_1) 0)) (>= (- s2_1 s3_1) 4) (>= (- s3_1 s2_1) 2))
(or (not (= (- m2_1 m4_1) 0)) (>= (- s2_1 s4_1) 3) (>= (- s4_1 s2_1) 2))
(or (not (= (- m2_1 m5_1) 0)) (>= (- s2_1 s5_1) 2) (>= (- s5_1 s2_1) 2))
(or (not (= (- m2_1 m6_1) 0)) (>= (- s2_1 s6_1) 4) (>= (- s6_1 s2_1) 2))
(or (not (= (- m2_1 m7_1) 0)) (>= (- s2_1 s7_1) 4) (>= (- s7_1 s2_1) 2))
(or (not (= (- m2_1 m8_1) 0)) (>= (- s2_1 s8_1) 4) (>= (- s8_1 s2_1) 2))
(or (not (= (- m2_1 m9_1) 0)) (>= (- s2_1 s9_1) 2) (>= (- s9_1 s2_1) 2))
(or (not (= (- m2_1 m10_1) 0)) (>= (- s2_1 s10_1) 3) (>= (- s10_1 s2_1) 2))
(or (not (= (- m3_1 m4_1) 0)) (>= (- s3_1 s4_1) 3) (>= (- s4_1 s3_1) 4))
(or (not (= (- m3_1 m5_1) 0)) (>= (- s3_1 s5_1) 2) (>= (- s5_1 s3_1) 4))
(or (not (= (- m3_1 m6_1) 0)) (>= (- s3_1 s6_1) 4) (>= (- s6_1 s3_1) 4))
(or (not (= (- m3_1 m7_1) 0)) (>= (- s3_1 s7_1) 4) (>= (- s7_1 s3_1) 4))
(or (not (= (- m3_1 m8_1) 0)) (>= (- s3_1 s8_1) 4) (>= (- s8_1 s3_1) 4))
(or (not (= (- m3_1 m9_1) 0)) (>= (- s3_1 s9_1) 2) (>= (- s9_1 s3_1) 4))
(or (not (= (- m3_1 m10_1) 0)) (>= (- s3_1 s10_1) 3) (>= (- s10_1 s3_1) 4))
(or (not (= (- m4_1 m5_1) 0)) (>= (- s4_1 s5_1) 2) (>= (- s5_1 s4_1) 3))
(or (not (= (- m4_1 m6_1) 0)) (>= (- s4_1 s6_1) 4) (>= (- s6_1 s4_1) 3))
(or (not (= (- m4_1 m7_1) 0)) (>= (- s4_1 s7_1) 4) (>= (- s7_1 s4_1) 3))
(or (not (= (- m4_1 m8_1) 0)) (>= (- s4_1 s8_1) 4) (>= (- s8_1 s4_1) 3))
(or (not (= (- m4_1 m9_1) 0)) (>= (- s4_1 s9_1) 2) (>= (- s9_1 s4_1) 3))
(or (not (= (- m4_1 m10_1) 0)) (>= (- s4_1 s10_1) 3) (>= (- s10_1 s4_1) 3))
(or (not (= (- m5_1 m6_1) 0)) (>= (- s5_1 s6_1) 4) (>= (- s6_1 s5_1) 2))
(or (not (= (- m5_1 m7_1) 0)) (>= (- s5_1 s7_1) 4) (>= (- s7_1 s5_1) 2))
(or (not (= (- m5_1 m8_1) 0)) (>= (- s5_1 s8_1) 4) (>= (- s8_1 s5_1) 2))
(or (not (= (- m5_1 m9_1) 0)) (>= (- s5_1 s9_1) 2) (>= (- s9_1 s5_1) 2))
(or (not (= (- m5_1 m10_1) 0)) (>= (- s5_1 s10_1) 3) (>= (- s10_1 s5_1) 2))
(or (not (= (- m6_1 m7_1) 0)) (>= (- s6_1 s7_1) 4) (>= (- s7_1 s6_1) 4))
(or (not (= (- m6_1 m8_1) 0)) (>= (- s6_1 s8_1) 4) (>= (- s8_1 s6_1) 4))
(or (not (= (- m6_1 m9_1) 0)) (>= (- s6_1 s9_1) 2) (>= (- s9_1 s6_1) 4))
(or (not (= (- m6_1 m10_1) 0)) (>= (- s6_1 s10_1) 3) (>= (- s10_1 s6_1) 4))
(or (not (= (- m7_1 m8_1) 0)) (>= (- s7_1 s8_1) 4) (>= (- s8_1 s7_1) 4))
(or (not (= (- m7_1 m9_1) 0)) (>= (- s7_1 s9_1) 2) (>= (- s9_1 s7_1) 4))
(or (not (= (- m7_1 m10_1) 0)) (>= (- s7_1 s10_1) 3) (>= (- s10_1 s7_1) 4))
(or (not (= (- m8_1 m9_1) 0)) (>= (- s8_1 s9_1) 2) (>= (- s9_1 s8_1) 4))
(or (not (= (- m8_1 m10_1) 0)) (>= (- s8_1 s10_1) 3) (>= (- s10_1 s8_1) 4))
(or (not (= (- m9_1 m10_1) 0)) (>= (- s9_1 s10_1) 3) (>= (- s10_1 s9_1) 2))
(or (not (= (- m1_1 m2_2) 0)) (>= (- s1_1 s2_2) 3) (>= (- s2_2 s1_1) 3))
(or (not (= (- m1_1 m3_2) 0)) (>= (- s1_1 s3_2) 3) (>= (- s3_2 s1_1) 3))
(or (not (= (- m1_1 m4_2) 0)) (>= (- s1_1 s4_2) 2) (>= (- s4_2 s1_1) 3))
(or (not (= (- m1_1 m5_2) 0)) (>= (- s1_1 s5_2) 3) (>= (- s5_2 s1_1) 3))
(or (not (= (- m1_1 m6_2) 0)) (>= (- s1_1 s6_2) 3) (>= (- s6_2 s1_1) 3))
(or (not (= (- m1_1 m7_2) 0)) (>= (- s1_1 s7_2) 3) (>= (- s7_2 s1_1) 3))
(or (not (= (- m1_1 m8_2) 0)) (>= (- s1_1 s8_2) 3) (>= (- s8_2 s1_1) 3))
(or (not (= (- m1_1 m9_2) 0)) (>= (- s1_1 s9_2) 2) (>= (- s9_2 s1_1) 3))
(or (not (= (- m1_1 m10_2) 0)) (>= (- s1_1 s10_2) 3) (>= (- s10_2 s1_1) 3))
(or (not (= (- m2_1 m3_2) 0)) (>= (- s2_1 s3_2) 3) (>= (- s3_2 s2_1) 2))
(or (not (= (- m2_1 m4_2) 0)) (>= (- s2_1 s4_2) 2) (>= (- s4_2 s2_1) 2))
(or (not (= (- m2_1 m5_2) 0)) (>= (- s2_1 s5_2) 3) (>= (- s5_2 s2_1) 2))
(or (not (= (- m2_1 m6_2) 0)) (>= (- s2_1 s6_2) 3) (>= (- s6_2 s2_1) 2))
(or (not (= (- m2_1 m7_2) 0)) (>= (- s2_1 s7_2) 3) (>= (- s7_2 s2_1) 2))
(or (not (= (- m2_1 m8_2) 0)) (>= (- s2_1 s8_2) 3) (>= (- s8_2 s2_1) 2))
(or (not (= (- m2_1 m9_2) 0)) (>= (- s2_1 s9_2) 2) (>= (- s9_2 s2_1) 2))
(or (not (= (- m2_1 m10_2) 0)) (>= (- s2_1 s10_2) 3) (>= (- s10_2 s2_1) 2))
(or (not (= (- m3_1 m4_2) 0)) (>= (- s3_1 s4_2) 2) (>= (- s4_2 s3_1) 4))
(or (not (= (- m3_1 m5_2) 0)) (>= (- s3_1 s5_2) 3) (>= (- s5_2 s3_1) 4))
(or (not (= (- m3_1 m6_2) 0)) (>= (- s3_1 s6_2) 3) (>= (- s6_2 s3_1) 4))
(or (not (= (- m3_1 m7_2) 0)) (>= (- s3_1 s7_2) 3) (>= (- s7_2 s3_1) 4))
(or (not (= (- m3_1 m8_2) 0)) (>= (- s3_1 s8_2) 3) (>= (- s8_2 s3_1) 4))
(or (not (= (- m3_1 m9_2) 0)) (>= (- s3_1 s9_2) 2) (>= (- s9_2 s3_1) 4))
(or (not (= (- m3_1 m10_2) 0)) (>= (- s3_1 s10_2) 3) (>= (- s10_2 s3_1) 4))
(or (not (= (- m4_1 m5_2) 0)) (>= (- s4_1 s5_2) 3) (>= (- s5_2 s4_1) 3))
(or (not (= (- m4_1 m6_2) 0)) (>= (- s4_1 s6_2) 3) (>= (- s6_2 s4_1) 3))
(or (not (= (- m4_1 m7_2) 0)) (>= (- s4_1 s7_2) 3) (>= (- s7_2 s4_1) 3))
(or (not (= (- m4_1 m8_2) 0)) (>= (- s4_1 s8_2) 3) (>= (- s8_2 s4_1) 3))
(or (not (= (- m4_1 m9_2) 0)) (>= (- s4_1 s9_2) 2) (>= (- s9_2 s4_1) 3))
(or (not (= (- m4_1 m10_2) 0)) (>= (- s4_1 s10_2) 3) (>= (- s10_2 s4_1) 3))
(or (not (= (- m5_1 m6_2) 0)) (>= (- s5_1 s6_2) 3) (>= (- s6_2 s5_1) 2))
(or (not (= (- m5_1 m7_2) 0)) (>= (- s5_1 s7_2) 3) (>= (- s7_2 s5_1) 2))
(or (not (= (- m5_1 m8_2) 0)) (>= (- s5_1 s8_2) 3) (>= (- s8_2 s5_1) 2))
(or (not (= (- m5_1 m9_2) 0)) (>= (- s5_1 s9_2) 2) (>= (- s9_2 s5_1) 2))
(or (not (= (- m5_1 m10_2) 0)) (>= (- s5_1 s10_2) 3) (>= (- s10_2 s5_1) 2))
(or (not (= (- m6_1 m7_2) 0)) (>= (- s6_1 s7_2) 3) (>= (- s7_2 s6_1) 4))
(or (not (= (- m6_1 m8_2) 0)) (>= (- s6_1 s8_2) 3) (>= (- s8_2 s6_1) 4))
(or (not (= (- m6_1 m9_2) 0)) (>= (- s6_1 s9_2) 2) (>= (- s9_2 s6_1) 4))
(or (not (= (- m6_1 m10_2) 0)) (>= (- s6_1 s10_2) 3) (>= (- s10_2 s6_1) 4))
(or (not (= (- m7_1 m8_2) 0)) (>= (- s7_1 s8_2) 3) (>= (- s8_2 s7_1) 4))
(or (not (= (- m7_1 m9_2) 0)) (>= (- s7_1 s9_2) 2) (>= (- s9_2 s7_1) 4))
(or (not (= (- m7_1 m10_2) 0)) (>= (- s7_1 s10_2) 3) (>= (- s10_2 s7_1) 4))
(or (not (= (- m8_1 m9_2) 0)) (>= (- s8_1 s9_2) 2) (>= (- s9_2 s8_1) 4))
(or (not (= (- m8_1 m10_2) 0)) (>= (- s8_1 s10_2) 3) (>= (- s10_2 s8_1) 4))
(or (not (= (- m9_1 m10_2) 0)) (>= (- s9_1 s10_2) 3) (>= (- s10_2 s9_1) 2))
(or (not (= (- m1_2 m2_1) 0)) (>= (- s1_2 s2_1) 2) (>= (- s2_1 s1_2) 3))
(or (not (= (- m1_2 m3_1) 0)) (>= (- s1_2 s3_1) 4) (>= (- s3_1 s1_2) 3))
(or (not (= (- m1_2 m4_1) 0)) (>= (- s1_2 s4_1) 3) (>= (- s4_1 s1_2) 3))
(or (not (= (- m1_2 m5_1) 0)) (>= (- s1_2 s5_1) 2) (>= (- s5_1 s1_2) 3))
(or (not (= (- m1_2 m6_1) 0)) (>= (- s1_2 s6_1) 4) (>= (- s6_1 s1_2) 3))
(or (not (= (- m1_2 m7_1) 0)) (>= (- s1_2 s7_1) 4) (>= (- s7_1 s1_2) 3))
(or (not (= (- m1_2 m8_1) 0)) (>= (- s1_2 s8_1) 4) (>= (- s8_1 s1_2) 3))
(or (not (= (- m1_2 m9_1) 0)) (>= (- s1_2 s9_1) 2) (>= (- s9_1 s1_2) 3))
(or (not (= (- m1_2 m10_1) 0)) (>= (- s1_2 s10_1) 3) (>= (- s10_1 s1_2) 3))
(or (not (= (- m2_2 m3_1) 0)) (>= (- s2_2 s3_1) 4) (>= (- s3_1 s2_2) 3))
(or (not (= (- m2_2 m4_1) 0)) (>= (- s2_2 s4_1) 3) (>= (- s4_1 s2_2) 3))
(or (not (= (- m2_2 m5_1) 0)) (>= (- s2_2 s5_1) 2) (>= (- s5_1 s2_2) 3))
(or (not (= (- m2_2 m6_1) 0)) (>= (- s2_2 s6_1) 4) (>= (- s6_1 s2_2) 3))
(or (not (= (- m2_2 m7_1) 0)) (>= (- s2_2 s7_1) 4) (>= (- s7_1 s2_2) 3))
(or (not (= (- m2_2 m8_1) 0)) (>= (- s2_2 s8_1) 4) (>= (- s8_1 s2_2) 3))
(or (not (= (- m2_2 m9_1) 0)) (>= (- s2_2 s9_1) 2) (>= (- s9_1 s2_2) 3))
(or (not (= (- m2_2 m10_1) 0)) (>= (- s2_2 s10_1) 3) (>= (- s10_1 s2_2) 3))
(or (not (= (- m3_2 m4_1) 0)) (>= (- s3_2 s4_1) 3) (>= (- s4_1 s3_2) 3))
(or (not (= (- m3_2 m5_1) 0)) (>= (- s3_2 s5_1) 2) (>= (- s5_1 s3_2) 3))
(or (not (= (- m3_2 m6_1) 0)) (>= (- s3_2 s6_1) 4) (>= (- s6_1 s3_2) 3))
(or (not (= (- m3_2 m7_1) 0)) (>= (- s3_2 s7_1) 4) (>= (- s7_1 s3_2) 3))
(or (not (= (- m3_2 m8_1) 0)) (>= (- s3_2 s8_1) 4) (>= (- s8_1 s3_2) 3))
(or (not (= (- m3_2 m9_1) 0)) (>= (- s3_2 s9_1) 2) (>= (- s9_1 s3_2) 3))
(or (not (= (- m3_2 m10_1) 0)) (>= (- s3_2 s10_1) 3) (>= (- s10_1 s3_2) 3))
(or (not (= (- m4_2 m5_1) 0)) (>= (- s4_2 s5_1) 2) (>= (- s5_1 s4_2) 2))
(or (not (= (- m4_2 m6_1) 0)) (>= (- s4_2 s6_1) 4) (>= (- s6_1 s4_2) 2))
(or (not (= (- m4_2 m7_1) 0)) (>= (- s4_2 s7_1) 4) (>= (- s7_1 s4_2) 2))
(or (not (= (- m4_2 m8_1) 0)) (>= (- s4_2 s8_1) 4) (>= (- s8_1 s4_2) 2))
(or (not (= (- m4_2 m9_1) 0)) (>= (- s4_2 s9_1) 2) (>= (- s9_1 s4_2) 2))
(or (not (= (- m4_2 m10_1) 0)) (>= (- s4_2 s10_1) 3) (>= (- s10_1 s4_2) 2))
(or (not (= (- m5_2 m6_1) 0)) (>= (- s5_2 s6_1) 4) (>= (- s6_1 s5_2) 3))
(or (not (= (- m5_2 m7_1) 0)) (>= (- s5_2 s7_1) 4) (>= (- s7_1 s5_2) 3))
(or (not (= (- m5_2 m8_1) 0)) (>= (- s5_2 s8_1) 4) (>= (- s8_1 s5_2) 3))
(or (not (= (- m5_2 m9_1) 0)) (>= (- s5_2 s9_1) 2) (>= (- s9_1 s5_2) 3))
(or (not (= (- m5_2 m10_1) 0)) (>= (- s5_2 s10_1) 3) (>= (- s10_1 s5_2) 3))
(or (not (= (- m6_2 m7_1) 0)) (>= (- s6_2 s7_1) 4) (>= (- s7_1 s6_2) 3))
(or (not (= (- m6_2 m8_1) 0)) (>= (- s6_2 s8_1) 4) (>= (- s8_1 s6_2) 3))
(or (not (= (- m6_2 m9_1) 0)) (>= (- s6_2 s9_1) 2) (>= (- s9_1 s6_2) 3))
(or (not (= (- m6_2 m10_1) 0)) (>= (- s6_2 s10_1) 3) (>= (- s10_1 s6_2) 3))
(or (not (= (- m7_2 m8_1) 0)) (>= (- s7_2 s8_1) 4) (>= (- s8_1 s7_2) 3))
(or (not (= (- m7_2 m9_1) 0)) (>= (- s7_2 s9_1) 2) (>= (- s9_1 s7_2) 3))
(or (not (= (- m7_2 m10_1) 0)) (>= (- s7_2 s10_1) 3) (>= (- s10_1 s7_2) 3))
(or (not (= (- m8_2 m9_1) 0)) (>= (- s8_2 s9_1) 2) (>= (- s9_1 s8_2) 3))
(or (not (= (- m8_2 m10_1) 0)) (>= (- s8_2 s10_1) 3) (>= (- s10_1 s8_2) 3))
(or (not (= (- m9_2 m10_1) 0)) (>= (- s9_2 s10_1) 3) (>= (- s10_1 s9_2) 2))