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.