Program = PList(Outcome) EOF. Outcome = Assignment CNF. Assignment = PList(Literal). CNF = *l "cnf" PList(Clause) [*l "sat" ClauseCount] [*l "unsat" ClauseCount]. Clause = *l Weight PList(Literal). Literal : Pos | Neg common Variable. Pos = . Neg = "!". Variable = Ident. Weight = int. ClauseCount = int. PList(S) ~ "(" {S} ")". Main = String.