Scrieți un predicat rezolvent/3 care să calculeze rezolventul a două clauze, dacă cele două clauze au un rezolvent, și false în caz contrar.

Pentru a calcula rezolventul, avem nevoie de o clauză C1 în care avem literalul p, și o clauză C2 în care avem literalul non(p) (sau invers, în C1 avem non(p) și în C2 avem p), unde p este orice variabilă propozițională (din Var).

Rezolventul este C1 reunit C2:

C1 reunit {p}, C2 reunit {non(p)} => Rezolvent = C1 reunit C2

?- rezolvent([a, non(b), c], [d, c, b, a], R).
R = [d, c, a]

?- rezolvent([b], [non(b)], R).
R = []

?- rezolvent([p, q, r], [p, q, s], R).
false

Observație: pentru a șterge un element dintr-o listă, puteți folosi predicatul select/3 (vezi detalii în breviar).

?- select(a, [b, a, c], Result).
Result = [b, c]

?- select(a, [b, c], Result).
false

Hint: alegere nedeterministă a literalului P. Dacă P ∈ C1 și non(P) ∈ C2 (sau invers), elimină-le cu select/3, concatenează resturile, elimină duplicatele. Un cut pe prima soluție.