mirror of
https://github.com/c-cube/sidekick.git
synced 2025-12-05 19:00:33 -05:00
test: update some tests
This commit is contained in:
Simon Cruanes
parent
5865151247
commit
26b4f677e0
14 changed files with 739 additions and 1 deletions
|
|
@ -7,4 +7,4 @@ c Hypotheses
|
|||
2 0
|
||||
c Lemmas
|
||||
|
||||
|
||||
c :status unsat
|
||||
|
|
|
|||
|
|
@ -1038,3 +1038,4 @@ p cnf 435 1027
|
|||
-42 -286 -267 -43 -278 0
|
||||
60 65 122 117 127 0
|
||||
87 88 90 156 92 0
|
||||
c :status unsat
|
||||
|
|
|
|||
|
|
@ -3332,3 +3332,4 @@ p cnf 1359 3321
|
|||
-462 -463 -456 -459 -464 0
|
||||
-821 -1063 -1061 -943 -1177 0
|
||||
-921 -1264 -1167 -1262 -1266 0
|
||||
c :status unsat
|
||||
|
|
|
|||
|
|
@ -2326,3 +2326,4 @@ p cnf 986 2315
|
|||
-325 -450 -333 -328 -331 0
|
||||
124 131 125 126 122 0
|
||||
127 132 264 129 262 0
|
||||
c :status unsat
|
||||
|
|
|
|||
|
|
@ -34249,3 +34249,4 @@ p cnf 10410 34238
|
|||
-10407 10404 10401 10398 10395 10408 0
|
||||
-10408 10392 10389 10386 10383 10409 0
|
||||
-10409 10380 10377 10374 10371 10410 0
|
||||
c :status unsat
|
||||
|
|
|
|||
23
tests/unsat/SEQ035_size4.smt2
Normal file
23
tests/unsat/SEQ035_size4.smt2
Normal file
|
|
@ -0,0 +1,23 @@
|
|||
(set-logic QF_UF)
|
||||
(set-info :source |
|
||||
CADE ATP System competition. See http://www.cs.miami.edu/~tptp/CASC
|
||||
for more information.
|
||||
|
||||
This benchmark was obtained by trying to find a finite model of a first-order
|
||||
formula (Albert Oliveras).
|
||||
|)
|
||||
(set-info :smt-lib-version 2.0)
|
||||
(set-info :category "crafted")
|
||||
(set-info :status unsat)
|
||||
(declare-sort U 0)
|
||||
(declare-fun f1 (U U) U)
|
||||
(declare-fun c2 () U)
|
||||
(declare-fun c3 () U)
|
||||
(declare-fun c4 () U)
|
||||
(declare-fun c_0 () U)
|
||||
(declare-fun c_1 () U)
|
||||
(declare-fun c_2 () U)
|
||||
(declare-fun c_3 () U)
|
||||
(assert (let ((?v_2 (f1 c_0 c_0))) (let ((?v_0 (f1 c_0 ?v_2))) (let ((?v_1 (f1 c_0 ?v_0)) (?v_4 (f1 c_0 c_1)) (?v_5 (f1 c_0 c_2)) (?v_6 (f1 c_0 c_3)) (?v_12 (f1 c_1 c_1))) (let ((?v_11 (f1 c_0 ?v_12))) (let ((?v_3 (f1 c_0 ?v_11)) (?v_9 (f1 c_1 ?v_2)) (?v_18 (f1 c_2 c_2))) (let ((?v_24 (f1 c_0 ?v_18))) (let ((?v_7 (f1 c_0 ?v_24)) (?v_22 (f1 c_2 ?v_2)) (?v_20 (f1 c_3 c_3))) (let ((?v_36 (f1 c_0 ?v_20))) (let ((?v_8 (f1 c_0 ?v_36)) (?v_34 (f1 c_3 ?v_2)) (?v_10 (f1 c_1 ?v_9)) (?v_13 (f1 c_1 c_0)) (?v_16 (f1 c_1 c_2)) (?v_17 (f1 c_1 c_3)) (?v_15 (f1 c_1 ?v_12))) (let ((?v_14 (f1 c_1 ?v_15)) (?v_29 (f1 c_1 ?v_18))) (let ((?v_19 (f1 c_1 ?v_29)) (?v_25 (f1 c_2 ?v_12)) (?v_42 (f1 c_1 ?v_20))) (let ((?v_21 (f1 c_1 ?v_42)) (?v_37 (f1 c_3 ?v_12)) (?v_23 (f1 c_2 ?v_22)) (?v_26 (f1 c_2 c_0)) (?v_28 (f1 c_2 c_1)) (?v_30 (f1 c_2 c_3)) (?v_27 (f1 c_2 ?v_25)) (?v_32 (f1 c_2 ?v_18))) (let ((?v_31 (f1 c_2 ?v_32)) (?v_45 (f1 c_2 ?v_20))) (let ((?v_33 (f1 c_2 ?v_45)) (?v_43 (f1 c_3 ?v_18)) (?v_35 (f1 c_3 ?v_34)) (?v_38 (f1 c_3 c_0)) (?v_40 (f1 c_3 c_1)) (?v_41 (f1 c_3 c_2)) (?v_39 (f1 c_3 ?v_37))) (let ((?v_44 (f1 c_3 ?v_43)) (?v_47 (f1 c_3 ?v_20))) (let ((?v_46 (f1 c_3 ?v_47))) (and (distinct c_0 c_1 c_2 c_3) (= (f1 ?v_1 ?v_0) c_0) (= (f1 ?v_1 (f1 c_0 ?v_4)) c_0) (= (f1 ?v_1 (f1 c_0 ?v_5)) c_0) (= (f1 ?v_1 (f1 c_0 ?v_6)) c_0) (= (f1 ?v_3 ?v_9) c_1) (= (f1 ?v_3 (f1 c_1 ?v_4)) c_1) (= (f1 ?v_3 (f1 c_1 ?v_5)) c_1) (= (f1 ?v_3 (f1 c_1 ?v_6)) c_1) (= (f1 ?v_7 ?v_22) c_2) (= (f1 ?v_7 (f1 c_2 ?v_4)) c_2) (= (f1 ?v_7 (f1 c_2 ?v_5)) c_2) (= (f1 ?v_7 (f1 c_2 ?v_6)) c_2) (= (f1 ?v_8 ?v_34) c_3) (= (f1 ?v_8 (f1 c_3 ?v_4)) c_3) (= (f1 ?v_8 (f1 c_3 ?v_5)) c_3) (= (f1 ?v_8 (f1 c_3 ?v_6)) c_3) (= (f1 ?v_10 (f1 c_0 ?v_13)) c_0) (= (f1 ?v_10 ?v_11) c_0) (= (f1 ?v_10 (f1 c_0 ?v_16)) c_0) (= (f1 ?v_10 (f1 c_0 ?v_17)) c_0) (= (f1 ?v_14 (f1 c_1 ?v_13)) c_1) (= (f1 ?v_14 ?v_15) c_1) (= (f1 ?v_14 (f1 c_1 ?v_16)) c_1) (= (f1 ?v_14 (f1 c_1 ?v_17)) c_1) (= (f1 ?v_19 (f1 c_2 ?v_13)) c_2) (= (f1 ?v_19 ?v_25) c_2) (= (f1 ?v_19 (f1 c_2 ?v_16)) c_2) (= (f1 ?v_19 (f1 c_2 ?v_17)) c_2) (= (f1 ?v_21 (f1 c_3 ?v_13)) c_3) (= (f1 ?v_21 ?v_37) c_3) (= (f1 ?v_21 (f1 c_3 ?v_16)) c_3) (= (f1 ?v_21 (f1 c_3 ?v_17)) c_3) (= (f1 ?v_23 (f1 c_0 ?v_26)) c_0) (= (f1 ?v_23 (f1 c_0 ?v_28)) c_0) (= (f1 ?v_23 ?v_24) c_0) (= (f1 ?v_23 (f1 c_0 ?v_30)) c_0) (= (f1 ?v_27 (f1 c_1 ?v_26)) c_1) (= (f1 ?v_27 (f1 c_1 ?v_28)) c_1) (= (f1 ?v_27 ?v_29) c_1) (= (f1 ?v_27 (f1 c_1 ?v_30)) c_1) (= (f1 ?v_31 (f1 c_2 ?v_26)) c_2) (= (f1 ?v_31 (f1 c_2 ?v_28)) c_2) (= (f1 ?v_31 ?v_32) c_2) (= (f1 ?v_31 (f1 c_2 ?v_30)) c_2) (= (f1 ?v_33 (f1 c_3 ?v_26)) c_3) (= (f1 ?v_33 (f1 c_3 ?v_28)) c_3) (= (f1 ?v_33 ?v_43) c_3) (= (f1 ?v_33 (f1 c_3 ?v_30)) c_3) (= (f1 ?v_35 (f1 c_0 ?v_38)) c_0) (= (f1 ?v_35 (f1 c_0 ?v_40)) c_0) (= (f1 ?v_35 (f1 c_0 ?v_41)) c_0) (= (f1 ?v_35 ?v_36) c_0) (= (f1 ?v_39 (f1 c_1 ?v_38)) c_1) (= (f1 ?v_39 (f1 c_1 ?v_40)) c_1) (= (f1 ?v_39 (f1 c_1 ?v_41)) c_1) (= (f1 ?v_39 ?v_42) c_1) (= (f1 ?v_44 (f1 c_2 ?v_38)) c_2) (= (f1 ?v_44 (f1 c_2 ?v_40)) c_2) (= (f1 ?v_44 (f1 c_2 ?v_41)) c_2) (= (f1 ?v_44 ?v_45) c_2) (= (f1 ?v_46 (f1 c_3 ?v_38)) c_3) (= (f1 ?v_46 (f1 c_3 ?v_40)) c_3) (= (f1 ?v_46 (f1 c_3 ?v_41)) c_3) (= (f1 ?v_46 ?v_47) c_3) (or (not (= (f1 (f1 c2 c2) (f1 c3 c2)) c2)) (not (= (f1 c2 (f1 c3 (f1 c2 c4))) (f1 (f1 (f1 c4 c3) c3) c2)))) (or (= ?v_2 c_0) (= ?v_2 c_1) (= ?v_2 c_2) (= ?v_2 c_3)) (or (= ?v_4 c_0) (= ?v_4 c_1) (= ?v_4 c_2) (= ?v_4 c_3)) (or (= ?v_5 c_0) (= ?v_5 c_1) (= ?v_5 c_2) (= ?v_5 c_3)) (or (= ?v_6 c_0) (= ?v_6 c_1) (= ?v_6 c_2) (= ?v_6 c_3)) (or (= ?v_13 c_0) (= ?v_13 c_1) (= ?v_13 c_2) (= ?v_13 c_3)) (or (= ?v_12 c_0) (= ?v_12 c_1) (= ?v_12 c_2) (= ?v_12 c_3)) (or (= ?v_16 c_0) (= ?v_16 c_1) (= ?v_16 c_2) (= ?v_16 c_3)) (or (= ?v_17 c_0) (= ?v_17 c_1) (= ?v_17 c_2) (= ?v_17 c_3)) (or (= ?v_26 c_0) (= ?v_26 c_1) (= ?v_26 c_2) (= ?v_26 c_3)) (or (= ?v_28 c_0) (= ?v_28 c_1) (= ?v_28 c_2) (= ?v_28 c_3)) (or (= ?v_18 c_0) (= ?v_18 c_1) (= ?v_18 c_2) (= ?v_18 c_3)) (or (= ?v_30 c_0) (= ?v_30 c_1) (= ?v_30 c_2) (= ?v_30 c_3)) (or (= ?v_38 c_0) (= ?v_38 c_1) (= ?v_38 c_2) (= ?v_38 c_3)) (or (= ?v_40 c_0) (= ?v_40 c_1) (= ?v_40 c_2) (= ?v_40 c_3)) (or (= ?v_41 c_0) (= ?v_41 c_1) (= ?v_41 c_2) (= ?v_41 c_3)) (or (= ?v_20 c_0) (= ?v_20 c_1) (= ?v_20 c_2) (= ?v_20 c_3)) (or (= c2 c_0) (= c2 c_1) (= c2 c_2) (= c2 c_3)) (or (= c3 c_0) (= c3 c_1) (= c3 c_2) (= c3 c_3)) (or (= c4 c_0) (= c4 c_1) (= c4 c_2) (= c4 c_3))))))))))))))))))))
|
||||
(check-sat)
|
||||
(exit)
|
||||
57
tests/unsat/eq_diamond15.smt2
Normal file
57
tests/unsat/eq_diamond15.smt2
Normal file
|
|
@ -0,0 +1,57 @@
|
|||
(set-info :smt-lib-version 2.6)
|
||||
(set-logic QF_UF)
|
||||
(set-info :source |
|
||||
Generating minimum transitivity constraints in P-time for deciding Equality Logic,
|
||||
Ofer Strichman and Mirron Rozanov,
|
||||
SMT Workshop 2005.
|
||||
|
||||
Translator: Leonardo de Moura. |)
|
||||
(set-info :category "crafted")
|
||||
(set-info :status unsat)
|
||||
(declare-sort U 0)
|
||||
(declare-fun x0 () U)
|
||||
(declare-fun y0 () U)
|
||||
(declare-fun z0 () U)
|
||||
(declare-fun x1 () U)
|
||||
(declare-fun y1 () U)
|
||||
(declare-fun z1 () U)
|
||||
(declare-fun x2 () U)
|
||||
(declare-fun y2 () U)
|
||||
(declare-fun z2 () U)
|
||||
(declare-fun x3 () U)
|
||||
(declare-fun y3 () U)
|
||||
(declare-fun z3 () U)
|
||||
(declare-fun x4 () U)
|
||||
(declare-fun y4 () U)
|
||||
(declare-fun z4 () U)
|
||||
(declare-fun x5 () U)
|
||||
(declare-fun y5 () U)
|
||||
(declare-fun z5 () U)
|
||||
(declare-fun x6 () U)
|
||||
(declare-fun y6 () U)
|
||||
(declare-fun z6 () U)
|
||||
(declare-fun x7 () U)
|
||||
(declare-fun y7 () U)
|
||||
(declare-fun z7 () U)
|
||||
(declare-fun x8 () U)
|
||||
(declare-fun y8 () U)
|
||||
(declare-fun z8 () U)
|
||||
(declare-fun x9 () U)
|
||||
(declare-fun y9 () U)
|
||||
(declare-fun z9 () U)
|
||||
(declare-fun x10 () U)
|
||||
(declare-fun y10 () U)
|
||||
(declare-fun z10 () U)
|
||||
(declare-fun x11 () U)
|
||||
(declare-fun y11 () U)
|
||||
(declare-fun z11 () U)
|
||||
(declare-fun x12 () U)
|
||||
(declare-fun y12 () U)
|
||||
(declare-fun z12 () U)
|
||||
(declare-fun x13 () U)
|
||||
(declare-fun y13 () U)
|
||||
(declare-fun z13 () U)
|
||||
(declare-fun x14 () U)
|
||||
(assert (and (or (and (= x0 y0) (= y0 x1)) (and (= x0 z0) (= z0 x1))) (or (and (= x1 y1) (= y1 x2)) (and (= x1 z1) (= z1 x2))) (or (and (= x2 y2) (= y2 x3)) (and (= x2 z2) (= z2 x3))) (or (and (= x3 y3) (= y3 x4)) (and (= x3 z3) (= z3 x4))) (or (and (= x4 y4) (= y4 x5)) (and (= x4 z4) (= z4 x5))) (or (and (= x5 y5) (= y5 x6)) (and (= x5 z5) (= z5 x6))) (or (and (= x6 y6) (= y6 x7)) (and (= x6 z6) (= z6 x7))) (or (and (= x7 y7) (= y7 x8)) (and (= x7 z7) (= z7 x8))) (or (and (= x8 y8) (= y8 x9)) (and (= x8 z8) (= z8 x9))) (or (and (= x9 y9) (= y9 x10)) (and (= x9 z9) (= z9 x10))) (or (and (= x10 y10) (= y10 x11)) (and (= x10 z10) (= z10 x11))) (or (and (= x11 y11) (= y11 x12)) (and (= x11 z11) (= z11 x12))) (or (and (= x12 y12) (= y12 x13)) (and (= x12 z12) (= z12 x13))) (or (and (= x13 y13) (= y13 x14)) (and (= x13 z13) (= z13 x14))) (not (= x0 x14))))
|
||||
(check-sat)
|
||||
(exit)
|
||||
20
tests/unsat/eq_diamond2.smt2
Normal file
20
tests/unsat/eq_diamond2.smt2
Normal file
|
|
@ -0,0 +1,20 @@
|
|||
(set-info :smt-lib-version 2.6)
|
||||
(set-logic QF_UF)
|
||||
(set-info :source |
|
||||
Generating minimum transitivity constraints in P-time for deciding Equality Logic,
|
||||
Ofer Strichman and Mirron Rozanov,
|
||||
SMT Workshop 2005.
|
||||
|
||||
Translator: Leonardo de Moura. |)
|
||||
(set-info :category "crafted")
|
||||
(set-info :status unsat)
|
||||
(declare-sort U 0)
|
||||
(declare-fun x0 () U)
|
||||
(declare-fun y0 () U)
|
||||
(declare-fun z0 () U)
|
||||
(declare-fun x1 () U)
|
||||
(declare-fun y1 () U)
|
||||
(declare-fun z1 () U)
|
||||
(assert (and (or (and (= x0 y0) (= y0 x1)) (and (= x0 z0) (= z0 x1))) (not (= x0 x1))))
|
||||
(check-sat)
|
||||
(exit)
|
||||
74
tests/unsat/eq_diamond20.smt2
Normal file
74
tests/unsat/eq_diamond20.smt2
Normal file
|
|
@ -0,0 +1,74 @@
|
|||
(set-info :smt-lib-version 2.6)
|
||||
(set-logic QF_UF)
|
||||
(set-info :source |
|
||||
Generating minimum transitivity constraints in P-time for deciding Equality Logic,
|
||||
Ofer Strichman and Mirron Rozanov,
|
||||
SMT Workshop 2005.
|
||||
|
||||
Translator: Leonardo de Moura. |)
|
||||
(set-info :category "crafted")
|
||||
(set-info :status unsat)
|
||||
(declare-sort U 0)
|
||||
(declare-fun x0 () U)
|
||||
(declare-fun y0 () U)
|
||||
(declare-fun z0 () U)
|
||||
(declare-fun x1 () U)
|
||||
(declare-fun y1 () U)
|
||||
(declare-fun z1 () U)
|
||||
(declare-fun x2 () U)
|
||||
(declare-fun y2 () U)
|
||||
(declare-fun z2 () U)
|
||||
(declare-fun x3 () U)
|
||||
(declare-fun y3 () U)
|
||||
(declare-fun z3 () U)
|
||||
(declare-fun x4 () U)
|
||||
(declare-fun y4 () U)
|
||||
(declare-fun z4 () U)
|
||||
(declare-fun x5 () U)
|
||||
(declare-fun y5 () U)
|
||||
(declare-fun z5 () U)
|
||||
(declare-fun x6 () U)
|
||||
(declare-fun y6 () U)
|
||||
(declare-fun z6 () U)
|
||||
(declare-fun x7 () U)
|
||||
(declare-fun y7 () U)
|
||||
(declare-fun z7 () U)
|
||||
(declare-fun x8 () U)
|
||||
(declare-fun y8 () U)
|
||||
(declare-fun z8 () U)
|
||||
(declare-fun x9 () U)
|
||||
(declare-fun y9 () U)
|
||||
(declare-fun z9 () U)
|
||||
(declare-fun x10 () U)
|
||||
(declare-fun y10 () U)
|
||||
(declare-fun z10 () U)
|
||||
(declare-fun x11 () U)
|
||||
(declare-fun y11 () U)
|
||||
(declare-fun z11 () U)
|
||||
(declare-fun x12 () U)
|
||||
(declare-fun y12 () U)
|
||||
(declare-fun z12 () U)
|
||||
(declare-fun x13 () U)
|
||||
(declare-fun y13 () U)
|
||||
(declare-fun z13 () U)
|
||||
(declare-fun x14 () U)
|
||||
(declare-fun y14 () U)
|
||||
(declare-fun z14 () U)
|
||||
(declare-fun x15 () U)
|
||||
(declare-fun y15 () U)
|
||||
(declare-fun z15 () U)
|
||||
(declare-fun x16 () U)
|
||||
(declare-fun y16 () U)
|
||||
(declare-fun z16 () U)
|
||||
(declare-fun x17 () U)
|
||||
(declare-fun y17 () U)
|
||||
(declare-fun z17 () U)
|
||||
(declare-fun x18 () U)
|
||||
(declare-fun y18 () U)
|
||||
(declare-fun z18 () U)
|
||||
(declare-fun x19 () U)
|
||||
(declare-fun y19 () U)
|
||||
(declare-fun z19 () U)
|
||||
(assert (and (or (and (= x0 y0) (= y0 x1)) (and (= x0 z0) (= z0 x1))) (or (and (= x1 y1) (= y1 x2)) (and (= x1 z1) (= z1 x2))) (or (and (= x2 y2) (= y2 x3)) (and (= x2 z2) (= z2 x3))) (or (and (= x3 y3) (= y3 x4)) (and (= x3 z3) (= z3 x4))) (or (and (= x4 y4) (= y4 x5)) (and (= x4 z4) (= z4 x5))) (or (and (= x5 y5) (= y5 x6)) (and (= x5 z5) (= z5 x6))) (or (and (= x6 y6) (= y6 x7)) (and (= x6 z6) (= z6 x7))) (or (and (= x7 y7) (= y7 x8)) (and (= x7 z7) (= z7 x8))) (or (and (= x8 y8) (= y8 x9)) (and (= x8 z8) (= z8 x9))) (or (and (= x9 y9) (= y9 x10)) (and (= x9 z9) (= z9 x10))) (or (and (= x10 y10) (= y10 x11)) (and (= x10 z10) (= z10 x11))) (or (and (= x11 y11) (= y11 x12)) (and (= x11 z11) (= z11 x12))) (or (and (= x12 y12) (= y12 x13)) (and (= x12 z12) (= z12 x13))) (or (and (= x13 y13) (= y13 x14)) (and (= x13 z13) (= z13 x14))) (or (and (= x14 y14) (= y14 x15)) (and (= x14 z14) (= z14 x15))) (or (and (= x15 y15) (= y15 x16)) (and (= x15 z15) (= z15 x16))) (or (and (= x16 y16) (= y16 x17)) (and (= x16 z16) (= z16 x17))) (or (and (= x17 y17) (= y17 x18)) (and (= x17 z17) (= z17 x18))) (or (and (= x18 y18) (= y18 x19)) (and (= x18 z18) (= z18 x19))) (not (= x0 x19))))
|
||||
(check-sat)
|
||||
(exit)
|
||||
32
tests/unsat/eq_diamond3.smt2
Normal file
32
tests/unsat/eq_diamond3.smt2
Normal file
|
|
@ -0,0 +1,32 @@
|
|||
(set-logic QF_UF)
|
||||
(set-info :source |
|
||||
Generating minimum transitivity constraints in P-time for deciding Equality Logic,
|
||||
Ofer Strichman and Mirron Rozanov,
|
||||
SMT Workshop 2005.
|
||||
|
||||
Translator: Leonardo de Moura. |)
|
||||
(set-info :smt-lib-version 2.0)
|
||||
(set-info :category "crafted")
|
||||
(set-info :status unsat)
|
||||
(declare-sort U 0)
|
||||
(declare-fun x0 () U)
|
||||
(declare-fun y0 () U)
|
||||
(declare-fun z0 () U)
|
||||
(declare-fun x1 () U)
|
||||
(declare-fun y1 () U)
|
||||
(declare-fun z1 () U)
|
||||
(declare-fun x2 () U)
|
||||
(declare-fun y2 () U)
|
||||
(declare-fun z2 () U)
|
||||
(declare-fun x3 () U)
|
||||
(declare-fun y3 () U)
|
||||
(declare-fun z3 () U)
|
||||
(assert
|
||||
(and
|
||||
(or (and (= x0 y0) (= y0 x1)) (and (= x0 z0) (= z0 x1)))
|
||||
(or (and (= x1 y1) (= y1 x2)) (and (= x1 z1) (= z1 x2)))
|
||||
(or (and (= x2 y2) (= y2 x3)) (and (= x2 z2) (= z2 x3)))
|
||||
(not (= x0 x3))))
|
||||
(check-sat)
|
||||
(exit)
|
||||
; :status unsat
|
||||
104
tests/unsat/eq_diamond30.smt2
Normal file
104
tests/unsat/eq_diamond30.smt2
Normal file
|
|
@ -0,0 +1,104 @@
|
|||
(set-info :smt-lib-version 2.6)
|
||||
(set-logic QF_UF)
|
||||
(set-info :source |
|
||||
Generating minimum transitivity constraints in P-time for deciding Equality Logic,
|
||||
Ofer Strichman and Mirron Rozanov,
|
||||
SMT Workshop 2005.
|
||||
|
||||
Translator: Leonardo de Moura. |)
|
||||
(set-info :category "crafted")
|
||||
(set-info :status unsat)
|
||||
(declare-sort U 0)
|
||||
(declare-fun x0 () U)
|
||||
(declare-fun y0 () U)
|
||||
(declare-fun z0 () U)
|
||||
(declare-fun x1 () U)
|
||||
(declare-fun y1 () U)
|
||||
(declare-fun z1 () U)
|
||||
(declare-fun x2 () U)
|
||||
(declare-fun y2 () U)
|
||||
(declare-fun z2 () U)
|
||||
(declare-fun x3 () U)
|
||||
(declare-fun y3 () U)
|
||||
(declare-fun z3 () U)
|
||||
(declare-fun x4 () U)
|
||||
(declare-fun y4 () U)
|
||||
(declare-fun z4 () U)
|
||||
(declare-fun x5 () U)
|
||||
(declare-fun y5 () U)
|
||||
(declare-fun z5 () U)
|
||||
(declare-fun x6 () U)
|
||||
(declare-fun y6 () U)
|
||||
(declare-fun z6 () U)
|
||||
(declare-fun x7 () U)
|
||||
(declare-fun y7 () U)
|
||||
(declare-fun z7 () U)
|
||||
(declare-fun x8 () U)
|
||||
(declare-fun y8 () U)
|
||||
(declare-fun z8 () U)
|
||||
(declare-fun x9 () U)
|
||||
(declare-fun y9 () U)
|
||||
(declare-fun z9 () U)
|
||||
(declare-fun x10 () U)
|
||||
(declare-fun y10 () U)
|
||||
(declare-fun z10 () U)
|
||||
(declare-fun x11 () U)
|
||||
(declare-fun y11 () U)
|
||||
(declare-fun z11 () U)
|
||||
(declare-fun x12 () U)
|
||||
(declare-fun y12 () U)
|
||||
(declare-fun z12 () U)
|
||||
(declare-fun x13 () U)
|
||||
(declare-fun y13 () U)
|
||||
(declare-fun z13 () U)
|
||||
(declare-fun x14 () U)
|
||||
(declare-fun y14 () U)
|
||||
(declare-fun z14 () U)
|
||||
(declare-fun x15 () U)
|
||||
(declare-fun y15 () U)
|
||||
(declare-fun z15 () U)
|
||||
(declare-fun x16 () U)
|
||||
(declare-fun y16 () U)
|
||||
(declare-fun z16 () U)
|
||||
(declare-fun x17 () U)
|
||||
(declare-fun y17 () U)
|
||||
(declare-fun z17 () U)
|
||||
(declare-fun x18 () U)
|
||||
(declare-fun y18 () U)
|
||||
(declare-fun z18 () U)
|
||||
(declare-fun x19 () U)
|
||||
(declare-fun y19 () U)
|
||||
(declare-fun z19 () U)
|
||||
(declare-fun x20 () U)
|
||||
(declare-fun y20 () U)
|
||||
(declare-fun z20 () U)
|
||||
(declare-fun x21 () U)
|
||||
(declare-fun y21 () U)
|
||||
(declare-fun z21 () U)
|
||||
(declare-fun x22 () U)
|
||||
(declare-fun y22 () U)
|
||||
(declare-fun z22 () U)
|
||||
(declare-fun x23 () U)
|
||||
(declare-fun y23 () U)
|
||||
(declare-fun z23 () U)
|
||||
(declare-fun x24 () U)
|
||||
(declare-fun y24 () U)
|
||||
(declare-fun z24 () U)
|
||||
(declare-fun x25 () U)
|
||||
(declare-fun y25 () U)
|
||||
(declare-fun z25 () U)
|
||||
(declare-fun x26 () U)
|
||||
(declare-fun y26 () U)
|
||||
(declare-fun z26 () U)
|
||||
(declare-fun x27 () U)
|
||||
(declare-fun y27 () U)
|
||||
(declare-fun z27 () U)
|
||||
(declare-fun x28 () U)
|
||||
(declare-fun y28 () U)
|
||||
(declare-fun z28 () U)
|
||||
(declare-fun x29 () U)
|
||||
(declare-fun y29 () U)
|
||||
(declare-fun z29 () U)
|
||||
(assert (and (or (and (= x0 y0) (= y0 x1)) (and (= x0 z0) (= z0 x1))) (or (and (= x1 y1) (= y1 x2)) (and (= x1 z1) (= z1 x2))) (or (and (= x2 y2) (= y2 x3)) (and (= x2 z2) (= z2 x3))) (or (and (= x3 y3) (= y3 x4)) (and (= x3 z3) (= z3 x4))) (or (and (= x4 y4) (= y4 x5)) (and (= x4 z4) (= z4 x5))) (or (and (= x5 y5) (= y5 x6)) (and (= x5 z5) (= z5 x6))) (or (and (= x6 y6) (= y6 x7)) (and (= x6 z6) (= z6 x7))) (or (and (= x7 y7) (= y7 x8)) (and (= x7 z7) (= z7 x8))) (or (and (= x8 y8) (= y8 x9)) (and (= x8 z8) (= z8 x9))) (or (and (= x9 y9) (= y9 x10)) (and (= x9 z9) (= z9 x10))) (or (and (= x10 y10) (= y10 x11)) (and (= x10 z10) (= z10 x11))) (or (and (= x11 y11) (= y11 x12)) (and (= x11 z11) (= z11 x12))) (or (and (= x12 y12) (= y12 x13)) (and (= x12 z12) (= z12 x13))) (or (and (= x13 y13) (= y13 x14)) (and (= x13 z13) (= z13 x14))) (or (and (= x14 y14) (= y14 x15)) (and (= x14 z14) (= z14 x15))) (or (and (= x15 y15) (= y15 x16)) (and (= x15 z15) (= z15 x16))) (or (and (= x16 y16) (= y16 x17)) (and (= x16 z16) (= z16 x17))) (or (and (= x17 y17) (= y17 x18)) (and (= x17 z17) (= z17 x18))) (or (and (= x18 y18) (= y18 x19)) (and (= x18 z18) (= z18 x19))) (or (and (= x19 y19) (= y19 x20)) (and (= x19 z19) (= z19 x20))) (or (and (= x20 y20) (= y20 x21)) (and (= x20 z20) (= z20 x21))) (or (and (= x21 y21) (= y21 x22)) (and (= x21 z21) (= z21 x22))) (or (and (= x22 y22) (= y22 x23)) (and (= x22 z22) (= z22 x23))) (or (and (= x23 y23) (= y23 x24)) (and (= x23 z23) (= z23 x24))) (or (and (= x24 y24) (= y24 x25)) (and (= x24 z24) (= z24 x25))) (or (and (= x25 y25) (= y25 x26)) (and (= x25 z25) (= z25 x26))) (or (and (= x26 y26) (= y26 x27)) (and (= x26 z26) (= z26 x27))) (or (and (= x27 y27) (= y27 x28)) (and (= x27 z27) (= z27 x28))) (or (and (= x28 y28) (= y28 x29)) (and (= x28 z28) (= z28 x29))) (not (= x0 x29))))
|
||||
(check-sat)
|
||||
(exit)
|
||||
36
tests/unsat/eq_diamond4.smt2
Normal file
36
tests/unsat/eq_diamond4.smt2
Normal file
|
|
@ -0,0 +1,36 @@
|
|||
(set-logic QF_UF)
|
||||
(set-info :source |
|
||||
Generating minimum transitivity constraints in P-time for deciding Equality Logic,
|
||||
Ofer Strichman and Mirron Rozanov,
|
||||
SMT Workshop 2005.
|
||||
|
||||
Translator: Leonardo de Moura. |)
|
||||
(set-info :smt-lib-version 2.0)
|
||||
(set-info :category "crafted")
|
||||
(set-info :status unsat)
|
||||
(declare-sort U 0)
|
||||
(declare-fun x0 () U)
|
||||
(declare-fun y0 () U)
|
||||
(declare-fun z0 () U)
|
||||
(declare-fun x1 () U)
|
||||
(declare-fun y1 () U)
|
||||
(declare-fun z1 () U)
|
||||
(declare-fun x2 () U)
|
||||
(declare-fun y2 () U)
|
||||
(declare-fun z2 () U)
|
||||
(declare-fun x3 () U)
|
||||
(declare-fun y3 () U)
|
||||
(declare-fun z3 () U)
|
||||
(declare-fun x4 () U)
|
||||
(declare-fun y4 () U)
|
||||
(declare-fun z4 () U)
|
||||
(assert
|
||||
(and
|
||||
(or (and (= x0 y0) (= y0 x1)) (and (= x0 z0) (= z0 x1)))
|
||||
(or (and (= x1 y1) (= y1 x2)) (and (= x1 z1) (= z1 x2)))
|
||||
(or (and (= x2 y2) (= y2 x3)) (and (= x2 z2) (= z2 x3)))
|
||||
(or (and (= x3 y3) (= y3 x4)) (and (= x3 z3) (= z3 x4)))
|
||||
(not (= x1 x4))))
|
||||
(check-sat)
|
||||
(exit)
|
||||
; :status unsat
|
||||
164
tests/unsat/eq_diamond50.smt2
Normal file
164
tests/unsat/eq_diamond50.smt2
Normal file
|
|
@ -0,0 +1,164 @@
|
|||
(set-info :smt-lib-version 2.6)
|
||||
(set-logic QF_UF)
|
||||
(set-info :source |
|
||||
Generating minimum transitivity constraints in P-time for deciding Equality Logic,
|
||||
Ofer Strichman and Mirron Rozanov,
|
||||
SMT Workshop 2005.
|
||||
|
||||
Translator: Leonardo de Moura. |)
|
||||
(set-info :category "crafted")
|
||||
(set-info :status unsat)
|
||||
(declare-sort U 0)
|
||||
(declare-fun x0 () U)
|
||||
(declare-fun y0 () U)
|
||||
(declare-fun z0 () U)
|
||||
(declare-fun x1 () U)
|
||||
(declare-fun y1 () U)
|
||||
(declare-fun z1 () U)
|
||||
(declare-fun x2 () U)
|
||||
(declare-fun y2 () U)
|
||||
(declare-fun z2 () U)
|
||||
(declare-fun x3 () U)
|
||||
(declare-fun y3 () U)
|
||||
(declare-fun z3 () U)
|
||||
(declare-fun x4 () U)
|
||||
(declare-fun y4 () U)
|
||||
(declare-fun z4 () U)
|
||||
(declare-fun x5 () U)
|
||||
(declare-fun y5 () U)
|
||||
(declare-fun z5 () U)
|
||||
(declare-fun x6 () U)
|
||||
(declare-fun y6 () U)
|
||||
(declare-fun z6 () U)
|
||||
(declare-fun x7 () U)
|
||||
(declare-fun y7 () U)
|
||||
(declare-fun z7 () U)
|
||||
(declare-fun x8 () U)
|
||||
(declare-fun y8 () U)
|
||||
(declare-fun z8 () U)
|
||||
(declare-fun x9 () U)
|
||||
(declare-fun y9 () U)
|
||||
(declare-fun z9 () U)
|
||||
(declare-fun x10 () U)
|
||||
(declare-fun y10 () U)
|
||||
(declare-fun z10 () U)
|
||||
(declare-fun x11 () U)
|
||||
(declare-fun y11 () U)
|
||||
(declare-fun z11 () U)
|
||||
(declare-fun x12 () U)
|
||||
(declare-fun y12 () U)
|
||||
(declare-fun z12 () U)
|
||||
(declare-fun x13 () U)
|
||||
(declare-fun y13 () U)
|
||||
(declare-fun z13 () U)
|
||||
(declare-fun x14 () U)
|
||||
(declare-fun y14 () U)
|
||||
(declare-fun z14 () U)
|
||||
(declare-fun x15 () U)
|
||||
(declare-fun y15 () U)
|
||||
(declare-fun z15 () U)
|
||||
(declare-fun x16 () U)
|
||||
(declare-fun y16 () U)
|
||||
(declare-fun z16 () U)
|
||||
(declare-fun x17 () U)
|
||||
(declare-fun y17 () U)
|
||||
(declare-fun z17 () U)
|
||||
(declare-fun x18 () U)
|
||||
(declare-fun y18 () U)
|
||||
(declare-fun z18 () U)
|
||||
(declare-fun x19 () U)
|
||||
(declare-fun y19 () U)
|
||||
(declare-fun z19 () U)
|
||||
(declare-fun x20 () U)
|
||||
(declare-fun y20 () U)
|
||||
(declare-fun z20 () U)
|
||||
(declare-fun x21 () U)
|
||||
(declare-fun y21 () U)
|
||||
(declare-fun z21 () U)
|
||||
(declare-fun x22 () U)
|
||||
(declare-fun y22 () U)
|
||||
(declare-fun z22 () U)
|
||||
(declare-fun x23 () U)
|
||||
(declare-fun y23 () U)
|
||||
(declare-fun z23 () U)
|
||||
(declare-fun x24 () U)
|
||||
(declare-fun y24 () U)
|
||||
(declare-fun z24 () U)
|
||||
(declare-fun x25 () U)
|
||||
(declare-fun y25 () U)
|
||||
(declare-fun z25 () U)
|
||||
(declare-fun x26 () U)
|
||||
(declare-fun y26 () U)
|
||||
(declare-fun z26 () U)
|
||||
(declare-fun x27 () U)
|
||||
(declare-fun y27 () U)
|
||||
(declare-fun z27 () U)
|
||||
(declare-fun x28 () U)
|
||||
(declare-fun y28 () U)
|
||||
(declare-fun z28 () U)
|
||||
(declare-fun x29 () U)
|
||||
(declare-fun y29 () U)
|
||||
(declare-fun z29 () U)
|
||||
(declare-fun x30 () U)
|
||||
(declare-fun y30 () U)
|
||||
(declare-fun z30 () U)
|
||||
(declare-fun x31 () U)
|
||||
(declare-fun y31 () U)
|
||||
(declare-fun z31 () U)
|
||||
(declare-fun x32 () U)
|
||||
(declare-fun y32 () U)
|
||||
(declare-fun z32 () U)
|
||||
(declare-fun x33 () U)
|
||||
(declare-fun y33 () U)
|
||||
(declare-fun z33 () U)
|
||||
(declare-fun x34 () U)
|
||||
(declare-fun y34 () U)
|
||||
(declare-fun z34 () U)
|
||||
(declare-fun x35 () U)
|
||||
(declare-fun y35 () U)
|
||||
(declare-fun z35 () U)
|
||||
(declare-fun x36 () U)
|
||||
(declare-fun y36 () U)
|
||||
(declare-fun z36 () U)
|
||||
(declare-fun x37 () U)
|
||||
(declare-fun y37 () U)
|
||||
(declare-fun z37 () U)
|
||||
(declare-fun x38 () U)
|
||||
(declare-fun y38 () U)
|
||||
(declare-fun z38 () U)
|
||||
(declare-fun x39 () U)
|
||||
(declare-fun y39 () U)
|
||||
(declare-fun z39 () U)
|
||||
(declare-fun x40 () U)
|
||||
(declare-fun y40 () U)
|
||||
(declare-fun z40 () U)
|
||||
(declare-fun x41 () U)
|
||||
(declare-fun y41 () U)
|
||||
(declare-fun z41 () U)
|
||||
(declare-fun x42 () U)
|
||||
(declare-fun y42 () U)
|
||||
(declare-fun z42 () U)
|
||||
(declare-fun x43 () U)
|
||||
(declare-fun y43 () U)
|
||||
(declare-fun z43 () U)
|
||||
(declare-fun x44 () U)
|
||||
(declare-fun y44 () U)
|
||||
(declare-fun z44 () U)
|
||||
(declare-fun x45 () U)
|
||||
(declare-fun y45 () U)
|
||||
(declare-fun z45 () U)
|
||||
(declare-fun x46 () U)
|
||||
(declare-fun y46 () U)
|
||||
(declare-fun z46 () U)
|
||||
(declare-fun x47 () U)
|
||||
(declare-fun y47 () U)
|
||||
(declare-fun z47 () U)
|
||||
(declare-fun x48 () U)
|
||||
(declare-fun y48 () U)
|
||||
(declare-fun z48 () U)
|
||||
(declare-fun x49 () U)
|
||||
(declare-fun y49 () U)
|
||||
(declare-fun z49 () U)
|
||||
(assert (and (or (and (= x0 y0) (= y0 x1)) (and (= x0 z0) (= z0 x1))) (or (and (= x1 y1) (= y1 x2)) (and (= x1 z1) (= z1 x2))) (or (and (= x2 y2) (= y2 x3)) (and (= x2 z2) (= z2 x3))) (or (and (= x3 y3) (= y3 x4)) (and (= x3 z3) (= z3 x4))) (or (and (= x4 y4) (= y4 x5)) (and (= x4 z4) (= z4 x5))) (or (and (= x5 y5) (= y5 x6)) (and (= x5 z5) (= z5 x6))) (or (and (= x6 y6) (= y6 x7)) (and (= x6 z6) (= z6 x7))) (or (and (= x7 y7) (= y7 x8)) (and (= x7 z7) (= z7 x8))) (or (and (= x8 y8) (= y8 x9)) (and (= x8 z8) (= z8 x9))) (or (and (= x9 y9) (= y9 x10)) (and (= x9 z9) (= z9 x10))) (or (and (= x10 y10) (= y10 x11)) (and (= x10 z10) (= z10 x11))) (or (and (= x11 y11) (= y11 x12)) (and (= x11 z11) (= z11 x12))) (or (and (= x12 y12) (= y12 x13)) (and (= x12 z12) (= z12 x13))) (or (and (= x13 y13) (= y13 x14)) (and (= x13 z13) (= z13 x14))) (or (and (= x14 y14) (= y14 x15)) (and (= x14 z14) (= z14 x15))) (or (and (= x15 y15) (= y15 x16)) (and (= x15 z15) (= z15 x16))) (or (and (= x16 y16) (= y16 x17)) (and (= x16 z16) (= z16 x17))) (or (and (= x17 y17) (= y17 x18)) (and (= x17 z17) (= z17 x18))) (or (and (= x18 y18) (= y18 x19)) (and (= x18 z18) (= z18 x19))) (or (and (= x19 y19) (= y19 x20)) (and (= x19 z19) (= z19 x20))) (or (and (= x20 y20) (= y20 x21)) (and (= x20 z20) (= z20 x21))) (or (and (= x21 y21) (= y21 x22)) (and (= x21 z21) (= z21 x22))) (or (and (= x22 y22) (= y22 x23)) (and (= x22 z22) (= z22 x23))) (or (and (= x23 y23) (= y23 x24)) (and (= x23 z23) (= z23 x24))) (or (and (= x24 y24) (= y24 x25)) (and (= x24 z24) (= z24 x25))) (or (and (= x25 y25) (= y25 x26)) (and (= x25 z25) (= z25 x26))) (or (and (= x26 y26) (= y26 x27)) (and (= x26 z26) (= z26 x27))) (or (and (= x27 y27) (= y27 x28)) (and (= x27 z27) (= z27 x28))) (or (and (= x28 y28) (= y28 x29)) (and (= x28 z28) (= z28 x29))) (or (and (= x29 y29) (= y29 x30)) (and (= x29 z29) (= z29 x30))) (or (and (= x30 y30) (= y30 x31)) (and (= x30 z30) (= z30 x31))) (or (and (= x31 y31) (= y31 x32)) (and (= x31 z31) (= z31 x32))) (or (and (= x32 y32) (= y32 x33)) (and (= x32 z32) (= z32 x33))) (or (and (= x33 y33) (= y33 x34)) (and (= x33 z33) (= z33 x34))) (or (and (= x34 y34) (= y34 x35)) (and (= x34 z34) (= z34 x35))) (or (and (= x35 y35) (= y35 x36)) (and (= x35 z35) (= z35 x36))) (or (and (= x36 y36) (= y36 x37)) (and (= x36 z36) (= z36 x37))) (or (and (= x37 y37) (= y37 x38)) (and (= x37 z37) (= z37 x38))) (or (and (= x38 y38) (= y38 x39)) (and (= x38 z38) (= z38 x39))) (or (and (= x39 y39) (= y39 x40)) (and (= x39 z39) (= z39 x40))) (or (and (= x40 y40) (= y40 x41)) (and (= x40 z40) (= z40 x41))) (or (and (= x41 y41) (= y41 x42)) (and (= x41 z41) (= z41 x42))) (or (and (= x42 y42) (= y42 x43)) (and (= x42 z42) (= z42 x43))) (or (and (= x43 y43) (= y43 x44)) (and (= x43 z43) (= z43 x44))) (or (and (= x44 y44) (= y44 x45)) (and (= x44 z44) (= z44 x45))) (or (and (= x45 y45) (= y45 x46)) (and (= x45 z45) (= z45 x46))) (or (and (= x46 y46) (= y46 x47)) (and (= x46 z46) (= z46 x47))) (or (and (= x47 y47) (= y47 x48)) (and (= x47 z47) (= z47 x48))) (or (and (= x48 y48) (= y48 x49)) (and (= x48 z48) (= z48 x49))) (not (= x0 x49))))
|
||||
(check-sat)
|
||||
(exit)
|
||||
224
tests/unsat/eq_diamond70.smt2
Normal file
224
tests/unsat/eq_diamond70.smt2
Normal file
|
|
@ -0,0 +1,224 @@
|
|||
(set-info :smt-lib-version 2.6)
|
||||
(set-logic QF_UF)
|
||||
(set-info :source |
|
||||
Generating minimum transitivity constraints in P-time for deciding Equality Logic,
|
||||
Ofer Strichman and Mirron Rozanov,
|
||||
SMT Workshop 2005.
|
||||
|
||||
Translator: Leonardo de Moura. |)
|
||||
(set-info :category "crafted")
|
||||
(set-info :status unsat)
|
||||
(declare-sort U 0)
|
||||
(declare-fun x0 () U)
|
||||
(declare-fun y0 () U)
|
||||
(declare-fun z0 () U)
|
||||
(declare-fun x1 () U)
|
||||
(declare-fun y1 () U)
|
||||
(declare-fun z1 () U)
|
||||
(declare-fun x2 () U)
|
||||
(declare-fun y2 () U)
|
||||
(declare-fun z2 () U)
|
||||
(declare-fun x3 () U)
|
||||
(declare-fun y3 () U)
|
||||
(declare-fun z3 () U)
|
||||
(declare-fun x4 () U)
|
||||
(declare-fun y4 () U)
|
||||
(declare-fun z4 () U)
|
||||
(declare-fun x5 () U)
|
||||
(declare-fun y5 () U)
|
||||
(declare-fun z5 () U)
|
||||
(declare-fun x6 () U)
|
||||
(declare-fun y6 () U)
|
||||
(declare-fun z6 () U)
|
||||
(declare-fun x7 () U)
|
||||
(declare-fun y7 () U)
|
||||
(declare-fun z7 () U)
|
||||
(declare-fun x8 () U)
|
||||
(declare-fun y8 () U)
|
||||
(declare-fun z8 () U)
|
||||
(declare-fun x9 () U)
|
||||
(declare-fun y9 () U)
|
||||
(declare-fun z9 () U)
|
||||
(declare-fun x10 () U)
|
||||
(declare-fun y10 () U)
|
||||
(declare-fun z10 () U)
|
||||
(declare-fun x11 () U)
|
||||
(declare-fun y11 () U)
|
||||
(declare-fun z11 () U)
|
||||
(declare-fun x12 () U)
|
||||
(declare-fun y12 () U)
|
||||
(declare-fun z12 () U)
|
||||
(declare-fun x13 () U)
|
||||
(declare-fun y13 () U)
|
||||
(declare-fun z13 () U)
|
||||
(declare-fun x14 () U)
|
||||
(declare-fun y14 () U)
|
||||
(declare-fun z14 () U)
|
||||
(declare-fun x15 () U)
|
||||
(declare-fun y15 () U)
|
||||
(declare-fun z15 () U)
|
||||
(declare-fun x16 () U)
|
||||
(declare-fun y16 () U)
|
||||
(declare-fun z16 () U)
|
||||
(declare-fun x17 () U)
|
||||
(declare-fun y17 () U)
|
||||
(declare-fun z17 () U)
|
||||
(declare-fun x18 () U)
|
||||
(declare-fun y18 () U)
|
||||
(declare-fun z18 () U)
|
||||
(declare-fun x19 () U)
|
||||
(declare-fun y19 () U)
|
||||
(declare-fun z19 () U)
|
||||
(declare-fun x20 () U)
|
||||
(declare-fun y20 () U)
|
||||
(declare-fun z20 () U)
|
||||
(declare-fun x21 () U)
|
||||
(declare-fun y21 () U)
|
||||
(declare-fun z21 () U)
|
||||
(declare-fun x22 () U)
|
||||
(declare-fun y22 () U)
|
||||
(declare-fun z22 () U)
|
||||
(declare-fun x23 () U)
|
||||
(declare-fun y23 () U)
|
||||
(declare-fun z23 () U)
|
||||
(declare-fun x24 () U)
|
||||
(declare-fun y24 () U)
|
||||
(declare-fun z24 () U)
|
||||
(declare-fun x25 () U)
|
||||
(declare-fun y25 () U)
|
||||
(declare-fun z25 () U)
|
||||
(declare-fun x26 () U)
|
||||
(declare-fun y26 () U)
|
||||
(declare-fun z26 () U)
|
||||
(declare-fun x27 () U)
|
||||
(declare-fun y27 () U)
|
||||
(declare-fun z27 () U)
|
||||
(declare-fun x28 () U)
|
||||
(declare-fun y28 () U)
|
||||
(declare-fun z28 () U)
|
||||
(declare-fun x29 () U)
|
||||
(declare-fun y29 () U)
|
||||
(declare-fun z29 () U)
|
||||
(declare-fun x30 () U)
|
||||
(declare-fun y30 () U)
|
||||
(declare-fun z30 () U)
|
||||
(declare-fun x31 () U)
|
||||
(declare-fun y31 () U)
|
||||
(declare-fun z31 () U)
|
||||
(declare-fun x32 () U)
|
||||
(declare-fun y32 () U)
|
||||
(declare-fun z32 () U)
|
||||
(declare-fun x33 () U)
|
||||
(declare-fun y33 () U)
|
||||
(declare-fun z33 () U)
|
||||
(declare-fun x34 () U)
|
||||
(declare-fun y34 () U)
|
||||
(declare-fun z34 () U)
|
||||
(declare-fun x35 () U)
|
||||
(declare-fun y35 () U)
|
||||
(declare-fun z35 () U)
|
||||
(declare-fun x36 () U)
|
||||
(declare-fun y36 () U)
|
||||
(declare-fun z36 () U)
|
||||
(declare-fun x37 () U)
|
||||
(declare-fun y37 () U)
|
||||
(declare-fun z37 () U)
|
||||
(declare-fun x38 () U)
|
||||
(declare-fun y38 () U)
|
||||
(declare-fun z38 () U)
|
||||
(declare-fun x39 () U)
|
||||
(declare-fun y39 () U)
|
||||
(declare-fun z39 () U)
|
||||
(declare-fun x40 () U)
|
||||
(declare-fun y40 () U)
|
||||
(declare-fun z40 () U)
|
||||
(declare-fun x41 () U)
|
||||
(declare-fun y41 () U)
|
||||
(declare-fun z41 () U)
|
||||
(declare-fun x42 () U)
|
||||
(declare-fun y42 () U)
|
||||
(declare-fun z42 () U)
|
||||
(declare-fun x43 () U)
|
||||
(declare-fun y43 () U)
|
||||
(declare-fun z43 () U)
|
||||
(declare-fun x44 () U)
|
||||
(declare-fun y44 () U)
|
||||
(declare-fun z44 () U)
|
||||
(declare-fun x45 () U)
|
||||
(declare-fun y45 () U)
|
||||
(declare-fun z45 () U)
|
||||
(declare-fun x46 () U)
|
||||
(declare-fun y46 () U)
|
||||
(declare-fun z46 () U)
|
||||
(declare-fun x47 () U)
|
||||
(declare-fun y47 () U)
|
||||
(declare-fun z47 () U)
|
||||
(declare-fun x48 () U)
|
||||
(declare-fun y48 () U)
|
||||
(declare-fun z48 () U)
|
||||
(declare-fun x49 () U)
|
||||
(declare-fun y49 () U)
|
||||
(declare-fun z49 () U)
|
||||
(declare-fun x50 () U)
|
||||
(declare-fun y50 () U)
|
||||
(declare-fun z50 () U)
|
||||
(declare-fun x51 () U)
|
||||
(declare-fun y51 () U)
|
||||
(declare-fun z51 () U)
|
||||
(declare-fun x52 () U)
|
||||
(declare-fun y52 () U)
|
||||
(declare-fun z52 () U)
|
||||
(declare-fun x53 () U)
|
||||
(declare-fun y53 () U)
|
||||
(declare-fun z53 () U)
|
||||
(declare-fun x54 () U)
|
||||
(declare-fun y54 () U)
|
||||
(declare-fun z54 () U)
|
||||
(declare-fun x55 () U)
|
||||
(declare-fun y55 () U)
|
||||
(declare-fun z55 () U)
|
||||
(declare-fun x56 () U)
|
||||
(declare-fun y56 () U)
|
||||
(declare-fun z56 () U)
|
||||
(declare-fun x57 () U)
|
||||
(declare-fun y57 () U)
|
||||
(declare-fun z57 () U)
|
||||
(declare-fun x58 () U)
|
||||
(declare-fun y58 () U)
|
||||
(declare-fun z58 () U)
|
||||
(declare-fun x59 () U)
|
||||
(declare-fun y59 () U)
|
||||
(declare-fun z59 () U)
|
||||
(declare-fun x60 () U)
|
||||
(declare-fun y60 () U)
|
||||
(declare-fun z60 () U)
|
||||
(declare-fun x61 () U)
|
||||
(declare-fun y61 () U)
|
||||
(declare-fun z61 () U)
|
||||
(declare-fun x62 () U)
|
||||
(declare-fun y62 () U)
|
||||
(declare-fun z62 () U)
|
||||
(declare-fun x63 () U)
|
||||
(declare-fun y63 () U)
|
||||
(declare-fun z63 () U)
|
||||
(declare-fun x64 () U)
|
||||
(declare-fun y64 () U)
|
||||
(declare-fun z64 () U)
|
||||
(declare-fun x65 () U)
|
||||
(declare-fun y65 () U)
|
||||
(declare-fun z65 () U)
|
||||
(declare-fun x66 () U)
|
||||
(declare-fun y66 () U)
|
||||
(declare-fun z66 () U)
|
||||
(declare-fun x67 () U)
|
||||
(declare-fun y67 () U)
|
||||
(declare-fun z67 () U)
|
||||
(declare-fun x68 () U)
|
||||
(declare-fun y68 () U)
|
||||
(declare-fun z68 () U)
|
||||
(declare-fun x69 () U)
|
||||
(declare-fun y69 () U)
|
||||
(declare-fun z69 () U)
|
||||
(assert (and (or (and (= x0 y0) (= y0 x1)) (and (= x0 z0) (= z0 x1))) (or (and (= x1 y1) (= y1 x2)) (and (= x1 z1) (= z1 x2))) (or (and (= x2 y2) (= y2 x3)) (and (= x2 z2) (= z2 x3))) (or (and (= x3 y3) (= y3 x4)) (and (= x3 z3) (= z3 x4))) (or (and (= x4 y4) (= y4 x5)) (and (= x4 z4) (= z4 x5))) (or (and (= x5 y5) (= y5 x6)) (and (= x5 z5) (= z5 x6))) (or (and (= x6 y6) (= y6 x7)) (and (= x6 z6) (= z6 x7))) (or (and (= x7 y7) (= y7 x8)) (and (= x7 z7) (= z7 x8))) (or (and (= x8 y8) (= y8 x9)) (and (= x8 z8) (= z8 x9))) (or (and (= x9 y9) (= y9 x10)) (and (= x9 z9) (= z9 x10))) (or (and (= x10 y10) (= y10 x11)) (and (= x10 z10) (= z10 x11))) (or (and (= x11 y11) (= y11 x12)) (and (= x11 z11) (= z11 x12))) (or (and (= x12 y12) (= y12 x13)) (and (= x12 z12) (= z12 x13))) (or (and (= x13 y13) (= y13 x14)) (and (= x13 z13) (= z13 x14))) (or (and (= x14 y14) (= y14 x15)) (and (= x14 z14) (= z14 x15))) (or (and (= x15 y15) (= y15 x16)) (and (= x15 z15) (= z15 x16))) (or (and (= x16 y16) (= y16 x17)) (and (= x16 z16) (= z16 x17))) (or (and (= x17 y17) (= y17 x18)) (and (= x17 z17) (= z17 x18))) (or (and (= x18 y18) (= y18 x19)) (and (= x18 z18) (= z18 x19))) (or (and (= x19 y19) (= y19 x20)) (and (= x19 z19) (= z19 x20))) (or (and (= x20 y20) (= y20 x21)) (and (= x20 z20) (= z20 x21))) (or (and (= x21 y21) (= y21 x22)) (and (= x21 z21) (= z21 x22))) (or (and (= x22 y22) (= y22 x23)) (and (= x22 z22) (= z22 x23))) (or (and (= x23 y23) (= y23 x24)) (and (= x23 z23) (= z23 x24))) (or (and (= x24 y24) (= y24 x25)) (and (= x24 z24) (= z24 x25))) (or (and (= x25 y25) (= y25 x26)) (and (= x25 z25) (= z25 x26))) (or (and (= x26 y26) (= y26 x27)) (and (= x26 z26) (= z26 x27))) (or (and (= x27 y27) (= y27 x28)) (and (= x27 z27) (= z27 x28))) (or (and (= x28 y28) (= y28 x29)) (and (= x28 z28) (= z28 x29))) (or (and (= x29 y29) (= y29 x30)) (and (= x29 z29) (= z29 x30))) (or (and (= x30 y30) (= y30 x31)) (and (= x30 z30) (= z30 x31))) (or (and (= x31 y31) (= y31 x32)) (and (= x31 z31) (= z31 x32))) (or (and (= x32 y32) (= y32 x33)) (and (= x32 z32) (= z32 x33))) (or (and (= x33 y33) (= y33 x34)) (and (= x33 z33) (= z33 x34))) (or (and (= x34 y34) (= y34 x35)) (and (= x34 z34) (= z34 x35))) (or (and (= x35 y35) (= y35 x36)) (and (= x35 z35) (= z35 x36))) (or (and (= x36 y36) (= y36 x37)) (and (= x36 z36) (= z36 x37))) (or (and (= x37 y37) (= y37 x38)) (and (= x37 z37) (= z37 x38))) (or (and (= x38 y38) (= y38 x39)) (and (= x38 z38) (= z38 x39))) (or (and (= x39 y39) (= y39 x40)) (and (= x39 z39) (= z39 x40))) (or (and (= x40 y40) (= y40 x41)) (and (= x40 z40) (= z40 x41))) (or (and (= x41 y41) (= y41 x42)) (and (= x41 z41) (= z41 x42))) (or (and (= x42 y42) (= y42 x43)) (and (= x42 z42) (= z42 x43))) (or (and (= x43 y43) (= y43 x44)) (and (= x43 z43) (= z43 x44))) (or (and (= x44 y44) (= y44 x45)) (and (= x44 z44) (= z44 x45))) (or (and (= x45 y45) (= y45 x46)) (and (= x45 z45) (= z45 x46))) (or (and (= x46 y46) (= y46 x47)) (and (= x46 z46) (= z46 x47))) (or (and (= x47 y47) (= y47 x48)) (and (= x47 z47) (= z47 x48))) (or (and (= x48 y48) (= y48 x49)) (and (= x48 z48) (= z48 x49))) (or (and (= x49 y49) (= y49 x50)) (and (= x49 z49) (= z49 x50))) (or (and (= x50 y50) (= y50 x51)) (and (= x50 z50) (= z50 x51))) (or (and (= x51 y51) (= y51 x52)) (and (= x51 z51) (= z51 x52))) (or (and (= x52 y52) (= y52 x53)) (and (= x52 z52) (= z52 x53))) (or (and (= x53 y53) (= y53 x54)) (and (= x53 z53) (= z53 x54))) (or (and (= x54 y54) (= y54 x55)) (and (= x54 z54) (= z54 x55))) (or (and (= x55 y55) (= y55 x56)) (and (= x55 z55) (= z55 x56))) (or (and (= x56 y56) (= y56 x57)) (and (= x56 z56) (= z56 x57))) (or (and (= x57 y57) (= y57 x58)) (and (= x57 z57) (= z57 x58))) (or (and (= x58 y58) (= y58 x59)) (and (= x58 z58) (= z58 x59))) (or (and (= x59 y59) (= y59 x60)) (and (= x59 z59) (= z59 x60))) (or (and (= x60 y60) (= y60 x61)) (and (= x60 z60) (= z60 x61))) (or (and (= x61 y61) (= y61 x62)) (and (= x61 z61) (= z61 x62))) (or (and (= x62 y62) (= y62 x63)) (and (= x62 z62) (= z62 x63))) (or (and (= x63 y63) (= y63 x64)) (and (= x63 z63) (= z63 x64))) (or (and (= x64 y64) (= y64 x65)) (and (= x64 z64) (= z64 x65))) (or (and (= x65 y65) (= y65 x66)) (and (= x65 z65) (= z65 x66))) (or (and (= x66 y66) (= y66 x67)) (and (= x66 z66) (= z66 x67))) (or (and (= x67 y67) (= y67 x68)) (and (= x67 z67) (= z67 x68))) (or (and (= x68 y68) (= y68 x69)) (and (= x68 z68) (= z68 x69))) (not (= x0 x69))))
|
||||
(check-sat)
|
||||
(exit)
|
||||
Loading…
Add table
Reference in a new issue