Sätze werden in einem Suchbaum gespeichert. Wird ein neuer Satz erzeugt, so wird der Suchbaum danach durchsucht, ob der Satz schon aufgetreten ist. Falls ja enthält der Suchbaumeintrag einen Verweis auf die entsprechende Äquivalenzklasse. Äquivalenzklassen können allerdings vereinigt werden. Würden Äquivalenzklassen nun deshalb gelöscht, so würden die Verweise der Sätze im Suchbaum auf ihre Äquivalenzklassen ungültig. Das Problem wird so gelöst, dass bei der Vereinigung zweier Äquivalenzklassen der Inhalt einer auf die andere übertragen wird und die leere Äquivalenzklasse dann nur einen Verweis auf die andere Äquivalenzklasse enthält.
Nach einer neuen Regel taucht in der Ausgabe nach einer Weile
``Ergebnisse nachgeholt'' auf. Die gerade neu erzeugte Regel konnte
noch auf keinen Satz angewandt werden. Deshalb wird sie, sobald sie
erzeugt wurde, auf alle mit a gekennzeichneten Sätze
angewandt, siehe
Symbole.