(a -> b) & a & -bor a dimacs version of the clause normal form syntax like
-1 2 1 -2which is a conjunction of disjunction lines with numbers standing for variables: the last example means simply (-x1 v x2) & x1 & -x2
For conventional formula syntax:
For dimacs you may use or skip the initial comment lines starting with c,
the special p line and the final 0 symbols at the end of each disjunct.
We allow the trailing 0-s only at the end of a line.
I.e. you may use the full dimacs version like
c comment p cnf 2 3 -1 2 0 1 0 -2 0or just
-1 2 1 -2hide syntax