The options for the type of a problem are:
For DPLL try out 200 variables or more. Truth table solvers start running into trouble with more than 20 variables. The resolution provers are a bit better than the truth table solvers, yet much worse than the DPLL solvers.
You can also browse and read the contents of a file into the input area: essentially copy-paste from a file.
(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 -2