Here is the instantiation of the general proof schema for SPASS style resolution proofs.
| user_reference | ::= | number |
| user_result | ::= | cnf_clause |
| user_rule_appl | ::= | GeR | SpL | SpR | EqF | Rew | Obv |
| user_parent | ::= | number |
| user_proof_type | ::= | SPASS_resolution |
The association list as well as the key/value list is not used. Figure 3 shows an example for a DFG-problem together with a SPASS style resolution proof. The rule application identifiers name the SPASS inference/simplification/reduction rules general resolution (GeR), superposition left (SpL), superposition right (SpR), equality factoring (EqF), rewriting (Rew), obvious reduction (Obv) and clause reduction (ClR). Clauses are labelled with numbers and references inside of proof steps refer to these numbers.
