read inputs F and C
if C ∈ F
    return true
let D = {x1,~x1,..,xn,~xn} be the set of literals occuring in F or C, and their negations
Contin := true
while Contin
    Contin ← false
    for (G,A) in S
        for h : {abs(x) : x ∈ B ∈ G ∨ x ∈ A} -> D # there are |D|^c such functions
            f(x) := (x > 0 ? h(x) : -h(-x))
            g(B) := {f(a) : a ∈ B}
            for B in G
                if g(B) ∉ G
                    continue in the for-loop where h is chosen
            if g(A) ∉ F
                push g(A) to F
                Contin ← true
if C ∈ F
    return true
else
    return false