The first line is always "CktQBF"; this identifies the file format.

Lines beginning with a pound sign ("#") are comments.

Every input variable and gate variable is assigned an even number.

Near the top of a file, a line such as "OutputGateLit 6072" means that gate variable 6072 corresponds to the output line of the entire circuit.  In the current version of the preprocessor, this should always be the positive form of a gate variable (although in earlier versions it could have been a negated gate variable).

For prenex instances, there such be exactly one line of the form "<q gate=X>", and X should be the variable identified by OutputGateLit.  (For non-prenex instances, multiple gates may have quantifier prefixes.)
