Output = Solution Diagnostics EOF. 
Solution: SAT | UNSAT.

SAT = "SAT" Assignment.
Assignment = List(Literal).
Literal : Pos | Neg common Variable.
Pos = .
Neg = "!".
Variable = <v> Ident.

UNSAT = "UNSAT" OptionalProof.

Diagnostics = UP  D  SSR B TSSR NV.
// Total # of UnitPropagations 
UP = "UP:" <up> Number. 
// Total # of Decisions
D = "D:" <d> Number.
// Total # of SSR
SSR = "SSR:" <ssr> Number.

// the outsourcing team is paid based on the number
// of calls to their software:

// bias count
// number of calls to either calculateBias or updateBias
B = "bias" "count:" <b> Number.

// total number of literals in unabbreviated semi-superresolvents
TSSR = "learned" "literals:" <tssr> Number.

// new variables introduced to shorten SSRs
NV = "new" "vars:" <nv> Number.

OptionalProof: Proof | Nothing.
//Text has be enclosed beteen {{ and }} in your input
Proof = <proof> Text.
Nothing = .

List(S) ~ {S}.
Main = .