Simple CNF input file to use with MiniSat

problem.cnf

c
c lines starting with c are comments
c
c A sample problem in CNF form, to use as input to minisat
c Usage:
c $ ./minisat problem.cnf solution.out
c solution.out will read "SAT" is there is a solution and the values
c that the variables take in that case
c further solutions can be found, for example, adding another line
c containing the negated solution obtained in the first case
c
c the first line after the comments is always "p cnf NUMBER_OF_VARIABLES NUMBER_OF_CLAUSES"
c lines after that are clauses, and must end with a space and a 0
c 1 means variable x1 and -3 means the negation of variable x3

p cnf 5 3
1 -5 4 0
-1 5 3 4 0
-3 -4 0