Global eindeutige Namen

bei jeder Benutzung jeder Klausel müssen deren Variablen umbenannt werden (= durch „frische`` Namen ersetzt).

Globalen Zähler hinzufügen = Zustands-Monaden-Transformator anwenden.

single :: [Clause] -> Atom -> [Substitution]
single cs a = do 
    c <- cs

import Control.Monad.State
single :: [Clause] -> Atom
    -> StateT Int [] Substitution
single cs a = do 
    c <- lift cs