CnfFormula works only with VarIds now; basic interactive mode.