indep_vars_2.cnf « cnf-files « tests « cryptominisat-5.6.3 « cryptominisat5 - cvc5.git - CVC4 is an efficient open-source automatic theorem prover for satisfiability modulo theories (SMT) problems.

index : cvc5.git

CVC4 is an efficient open-source automatic theorem prover for satisfiability modulo theories (SMT) problems.

git repository hosting

summary refs log tree commit diff

path: root/cryptominisat5/cryptominisat-5.6.3/tests/cnf-files/indep_vars_2.cnf

blob: 715211ef359c0a93bd65fffa5ce8c0a4113fdfaf (plain)

c RUN: %solver --maxsol 20 --verb=0 %s | %OutputCheck %s
c ind 1 2 3 0
1 2 3 0
-1 3 0
-1 2 0
2 3 0
-2 -3 0
c CHECK:     ^s SATISFIABLE$
c CHECK:     ^s SATISFIABLE$
c CHECK-NOT:     ^s SATISFIABLE$
c CHECK: UNSATISFIABLE

generated by cgit on debian on lair

contact matthew@masot.net with questions or feedback