fol_cnf/2 (defined in library(pac)/util/fol-cnf.pl not yet uploaded) converts a FOL (first-order formula) to an equivalent CNF (conjunctive normal form), a set of sets of literals.
?- fol_cnf((a+b)->c, CNF).
CNF = [[-a, c], [-b, c]].
Although fol_cnf is not special but common,
on playing around fol_cnf, I noticed an interesting property like this.
?- fol_cnf(-P(n), Q(n)).
where, P(n) is a proposition built up of n+1 variables and logical equivalence connective ==/2, and Q(n) is CNF build up n+1 variables. P(n) and Q(n) should be clear and are defined around library(pac)/zdd/zdd.pl.
P(1) = ((p(1)==p(0))==p(1))==p(0)
P(2) = ((((p(2)==p(1))==p(0))==p(2))==p(1))==p(0)
Q(1) =[
[-p(0), -p(1)],
[p(1),-p(0)],
[p(0),-P(1)],
[p(0), p(1)]]
Q(2) =[
[-p(0),-p(1),-p(2)],
[p(2),-p(0),-p(1)],
[p(1),-p(0),-p(2)],
[p(1),p(2),-p(0)],
[p(0),-p(1),-p(2)],
[p(0),p(2),-p(1)],
[p(0),p(1),-p(2)],
[p(0),p(1),p(2)]]
P(n) is known as such that is difficult to be proved on its validity. In fact I was successful only up to P(13) taking many hours and 80GB memory. On the contrary I was successful to check Q(2000) for its unsatisfiability in a few second in CNF in ZDD.MHO, in general if problems are given directly in CNF, refutation on CNF should be extremely fast.
BTW, I have not yet proved fol_cnf(-P(n), Q(n)) for all n, but should not be difficult.