1 files changed, 99 insertions, 0 deletions
diff --git a/unit-tests/hole4.smt2 b/unit-tests/hole4.smt2
new file mode 100644
index 0000000..816bd39
--- /dev/null
+++ b/unit-tests/hole4.smt2
@@ -0,0 +1,99 @@
+(set-logic QF_UF)
+(declare-fun a1 () Bool)
+(declare-fun a2 () Bool)
+(declare-fun a3 () Bool)
+(declare-fun a4 () Bool)
+(declare-fun a5 () Bool)
+(declare-fun a6 () Bool)
+(declare-fun a7 () Bool)
+(declare-fun a8 () Bool)
+(declare-fun a9 () Bool)
+(declare-fun a10 () Bool)
+(declare-fun a11 () Bool)
+(declare-fun a12 () Bool)
+(declare-fun a13 () Bool)
+(declare-fun a14 () Bool)
+(declare-fun a15 () Bool)
+(declare-fun a16 () Bool)
+(declare-fun a17 () Bool)
+(declare-fun a18 () Bool)
+(declare-fun a19 () Bool)
+(declare-fun a20 () Bool)
+(assert (and
+(or a1 a2 a3 a4)
+(or a5 a6 a7 a8)
+(or a9 a10 a11 a12)
+(or a13 a14 a15 a16)
+(or a17 a18 a19 a20)
+(or (not a1) (not a2))
+(or (not a1) (not a3))
+(or (not a1) (not a4))
+(or (not a2) (not a3))
+(or (not a2) (not a4))
+(or (not a3) (not a4))
+(or (not a5) (not a6))
+(or (not a5) (not a7))
+(or (not a5) (not a8))
+(or (not a6) (not a7))
+(or (not a6) (not a8))
+(or (not a7) (not a8))
+(or (not a9) (not a10))
+(or (not a9) (not a11))
+(or (not a9) (not a12))
+(or (not a10) (not a11))
+(or (not a10) (not a12))
+(or (not a11) (not a12))
+(or (not a13) (not a14))
+(or (not a13) (not a15))
+(or (not a13) (not a16))
+(or (not a14) (not a15))
+(or (not a14) (not a16))
+(or (not a15) (not a16))
+(or (not a17) (not a18))
+(or (not a17) (not a19))
+(or (not a17) (not a20))
+(or (not a18) (not a19))
+(or (not a18) (not a20))
+(or (not a19) (not a20))
+(or (not a1) (not a5))
+(or (not a1) (not a9))
+(or (not a1) (not a13))
+(or (not a1) (not a17))
+(or (not a5) (not a9))
+(or (not a5) (not a13))
+(or (not a5) (not a17))
+(or (not a9) (not a13))
+(or (not a9) (not a17))
+(or (not a13) (not a17))
+(or (not a2) (not a6))
+(or (not a2) (not a10))
+(or (not a2) (not a14))
+(or (not a2) (not a18))
+(or (not a6) (not a10))
+(or (not a6) (not a14))
+(or (not a6) (not a18))
+(or (not a10) (not a14))
+(or (not a10) (not a18))
+(or (not a14) (not a18))
+(or (not a3) (not a7))
+(or (not a3) (not a11))
+(or (not a3) (not a15))
+(or (not a3) (not a19))
+(or (not a7) (not a11))
+(or (not a7) (not a15))
+(or (not a7) (not a19))
+(or (not a11) (not a15))
+(or (not a11) (not a19))
+(or (not a15) (not a19))
+(or (not a4) (not a8))
+(or (not a4) (not a12))
+(or (not a4) (not a16))
+(or (not a4) (not a20))
+(or (not a8) (not a12))
+(or (not a8) (not a16))
+(or (not a8) (not a20))
+(or (not a12) (not a16))
+(or (not a12) (not a20))
+(or (not a16) (not a20))))
+(check-sat)
+(exit)