# Lion and Unicorn with Prolog SAT Solver

@kuniaki.mukai posted a Prolog SAT solver solution to
the Lion and Unicorn riddle. Can this be further improved:

``````% ?- time(solve_lion_uncorn_puzzle_in_dnf(Ans)).
%@ % 8,188,821 inferences, 0.626 CPU in 0.647 seconds
(97% CPU, 13085762 Lips)
%@ Ans = today(thu) ;
%@ % 171 inferences, 0.004 CPU in 0.004 seconds (100% CPU, 47017 Lips)
%@ false.
``````

A SAT solver is a computer program which aims to
solve the Boolean satisfiability problem. Using Boolean
modelling I only got that far:

``````yesterday(0,0,0,1,1,0).
yesterday(0,0,1,0,0,0).
yesterday(0,1,0,0,0,1).
yesterday(0,1,1,0,1,0).
yesterday(1,0,0,0,1,1).
yesterday(1,0,1,1,0,0).
yesterday(1,1,0,1,0,1).

lying_day(0,0,0,1).
lying_day(0,0,1,0).
lying_day(0,0,1,1).
lying_day(1,1,0,0).
lying_day(1,1,0,1).
lying_day(1,1,1,0).

solve_for(T1,T2,T3) :- yesterday(T1,T2,T3,Y1,Y2,Y3)
, contrary(lying_day(0,T1,T2,T3), lying_day(0,Y1,Y2,Y3))
, contrary(lying_day(1,T1,T2,T3), lying_day(1,Y1,Y2,Y3)).

contrary(S,T) :- \+ S, T.
contrary(S,T) :- S, \+ T.
``````

And then:

``````?- time(solve_for(T1,T2,T3)).
% 32 inferences, 0.000 CPU in 0.000 seconds (0% CPU, Infinite Lips)
T1 = 1,
T2 = T3, T3 = 0 ;
% 17 inferences, 0.000 CPU in 0.000 seconds (0% CPU, Infinite Lips)
false.
``````

What now, how to use a SAT Solver?

Ok, I was using a SAT solver in a little unorthodox way.
Used it as a compiler for a formula, so that I got:

``````yesterday(0,0,0,1,1,0).
yesterday(0,0,1,0,0,0).
yesterday(0,1,0,0,0,1).
yesterday(0,1,1,0,1,0).
yesterday(1,0,0,0,1,1).
yesterday(1,0,1,1,0,0).
yesterday(1,1,0,1,0,1).

two_liars(T1,T2,T3,Y1,Y2,Y3) :-
T1=\=Y1,
T1=:=(T1/\Y2) xor (T1/\Y3) xor (Y2/\Y3),
Y1=:=(T2/\T3) xor (T2/\Y1) xor (T3/\Y1),
T1=\=(T1/\T2) xor (T1/\T3) xor T2 xor (T2/\T3) xor T3,
Y1=\=(Y1/\Y2) xor (Y1/\Y3) xor Y2 xor (Y2/\Y3) xor Y3.

solve_for(T1,T2,T3) :-
yesterday(T1,T2,T3,Y1,Y2,Y3),
two_liars(T1,T2,T3,Y1,Y2,Y3).
``````

Works fine and is fast with `optimise=true`:

``````/* SWI-Prolog 9.1.17, optimise=false */
?- time(solve_for(T1,T2,T3)).
% 16 inferences, 0.000 CPU in 0.000 seconds (0% CPU, Infinite Lips)
T1 = 1,
T2 = T3, T3 = 0 ;
% 10 inferences, 0.000 CPU in 0.000 seconds (0% CPU, Infinite Lips)
false.

/* SWI-Prolog 9.1.17, optimise=true */
?- time((between(1, 1000000, _), solve_for(T1,T2,T3), fail; true)).
% 9,999,999 inferences, 1.203 CPU in 1.199 seconds
(100% CPU, 8311687 Lips)
``````

Edit 14.11.2023
So how to use a SAT solver as a compiler. First model the problem
with `library(clpb)` as Boolean formulas.

``````lying_day(A, B, C, D, M) :- M = (
~A* ~B* ~C*D+
~A* ~B*C* ~D+
~A* ~B*C*D+
A*B* ~C* ~D+
A*B* ~C*D+
A*B*C* ~D).

two_liars(T1, T2, T3, Y1, Y2, Y3, ((M1#M2)*(M3#M4))) :-
lying_day(0, T1, T2, T3, M1),
lying_day(0, Y1, Y2, Y3, M2),
lying_day(1, T1, T2, T3, M3),
lying_day(1, Y1, Y2, Y3, M4).
``````

Then look at the normalform:

``````?- two_liars(T1,T2,T3,Y1,Y2,Y3,M), sat(M).
sat(1#T2*T3#T2*Y1#T3*Y1#Y1),
sat(T1=:=T1*Y2#T1*Y3#Y2*Y3),
sat(T1=\=Y1),
sat(T1=\=T1*T2#T1*T3#T2#T2*T3#T3),
sat(Y1=\=Y1*Y2#Y1*Y3#Y2#Y2*Y3#Y3).
``````

Take the normalform, reorder the equations a little bit, fewer
variables first, and rewrite them into ISO core standard bitwise
operations, and then take profit.

I am busy on revising codes for DNF/CNF converter based on ZDD. They are still enough dirty or confused for me to remember details. However I hope it will drastically be improved in a week. I will upgrade package pac with it.

IMHO, SAT solving is to get DNF as normal form of the input formula. Therefore computational complexity must be high, perhaps NP-complete, though I am not sure on this. So I am not interested in efficiency of my approach, but in conceptual clearness.

For now I can only show an example below, where psa is
to show current dnf as normal form of SAT solving.

Sorry for not able to discussing about what you might want, which
might be too difficult for me to catch up with.

``````% ?- sat(a=:=b), psa, sat(b=:=c),psa, sat(c=:=d), psa.
%@  zid = 8
%@ 	[-a,-b]
%@ 	[a,b]
%@ -------------------
%@  zid = 16
%@ 	[-a,-b,-c]
%@ 	[a,b,c]
%@ -------------------
%@  zid = 26
%@ 	[-a,-b,-c,-d]
%@ 	[a,b,c,d]
%@ -------------------
%@ true.
``````

Yeah, I wonder what the CNF would be of this:

``````sat(1#T2*T3#T2*Y1#T3*Y1#Y1),
sat(T1=:=T1*Y2#T1*Y3#Y2*Y3),
sat(T1=\=Y1),
sat(T1=\=T1*T2#T1*T3#T2#T2*T3#T3),
sat(Y1=\=Y1*Y2#Y1*Y3#Y2#Y2*Y3#Y3).
``````

What Markus Triska shows is kind of a Boolean ring polynomial
M but factorized into M = M1*…*Mn, and then you have multiple
constraints and not a single constraint. Nice!

If you produce a CNF, actually a product sum form, you would
get also something of the form M = M1’*…*Mn’. Are these
M1’,…,Mn’ faster than the M1,…,Mn from

Markus Triskas library(clpb), when running the example?

Edit 14.11.2023
Whats also giving some speed, is introducing extra variables?
Tried this with SWI-Prolog:

``````two_liars(T1,T2,T3,Y1,Y2,Y3) :-
T1=\=Y1,
H is (Y2/\Y3),
T1=:=(T1/\Y2) xor (T1/\Y3) xor H,
J is (T2/\T3),
Y1=:=J xor (T2/\Y1) xor (T3/\Y1),
T1=\=(T1/\T2) xor (T1/\T3) xor T2 xor J xor T3,
Y1=\=(Y1/\Y2) xor (Y1/\Y3) xor Y2 xor H xor Y3.
``````

New benchmark results:

``````/* SWI-Prolog 9.1.17, optimise=true */
?- time((between(1, 1000000, _), solve_for(T1,T2,T3), fail; true)).
% 9,999,999 inferences, 1.203 CPU in 1.204 seconds (100% CPU, 8311687 Lips)
true.
``````

No speed up, possibly the additional temporary variables
are too expensive? Or the goals with the extra variable
are not enough often reached to amortisize?

Here is only query log for that as it is. ‘true’ is for 1.
I need time for understanding other parts of your posts.
I hope you could reproduce the query like this.

``````?- use_module(library(pac)).  % version 1.8.3
?- module(pac).
pac:  ?- use_module(zdd(zdd)).
?-  time((sat(.....
``````
query result
``````% ?- time((sat(true#T2*T3#T2*Y1#T3*Y1#Y1), psa,
%	sat(T1=:=T1*Y2#T1*Y3#Y2*Y3), psa,
%	sat(T1=\=Y1), psa,
%	sat(T1=\=T1*T2#T1*T3#T2#T2*T3#T3), psa,
%	sat(Y1=\=Y1*Y2#Y1*Y3#Y2#Y2*Y3#Y3), psa)).
%@  zid = 56
%@ 	[-B,-C]
%@ 	[-A,-C]
%@ 	[-A,-B,-C]
%@ 	[-A,B,C]
%@ 	[A,-B,C]
%@ 	[A,B,C]
%@ -------------------
%@  zid = 126
%@ 	[-B,-C,-D,-F]
%@ 	[-B,-C,-D,-E]
%@ 	[-B,-C,D,-E,F]
%@ 	[-B,-C,D,E,-F]
%@ 	[-B,-C,D,E,F]
%@ 	[-A,-C,-D,-F]
%@ 	[-A,-C,-D,-E]
%@ 	[-A,-C,D,-E,F]
%@ 	[-A,-C,D,E,-F]
%@ 	[-A,-C,D,E,F]
%@ 	[-A,-B,-C,-D,-F]
%@ 	[-A,-B,-C,-D,-E]
%@ 	[-A,-B,-C,D,-E,F]
%@ 	[-A,-B,-C,D,E,-F]
%@ 	[-A,-B,-C,D,E,F]
%@ 	[-A,B,C,-D,-F]
%@ 	[-A,B,C,-D,-E]
%@ 	[-A,B,C,D,-E,F]
%@ 	[-A,B,C,D,E,-F]
%@ 	[-A,B,C,D,E,F]
%@ 	[A,-B,C,-D,-F]
%@ 	[A,-B,C,-D,-E]
%@ 	[A,-B,C,D,-E,F]
%@ 	[A,-B,C,D,E,-F]
%@ 	[A,-B,C,D,E,F]
%@ 	[A,B,C,-D,-F]
%@ 	[A,B,C,-D,-E]
%@ 	[A,B,C,D,-E,F]
%@ 	[A,B,C,D,E,-F]
%@ 	[A,B,C,D,E,F]
%@ -------------------
%@  zid = 174
%@ 	[-B,-C,D,-E,F]
%@ 	[-B,-C,D,E,-F]
%@ 	[-B,-C,D,E,F]
%@ 	[-A,-C,D,-E,F]
%@ 	[-A,-C,D,E,-F]
%@ 	[-A,-C,D,E,F]
%@ 	[-A,-B,-C,D,-E,F]
%@ 	[-A,-B,-C,D,E,-F]
%@ 	[-A,-B,-C,D,E,F]
%@ 	[-A,B,C,-D,-F]
%@ 	[-A,B,C,-D,-E]
%@ 	[A,-B,C,-D,-F]
%@ 	[A,-B,C,-D,-E]
%@ 	[A,B,C,-D,-F]
%@ 	[A,B,C,-D,-E]
%@ -------------------
%@  zid = 336
%@ 	[-A,-B,-C,D,-E,F]
%@ 	[-A,-B,-C,D,E,-F]
%@ 	[-A,-B,-C,D,E,F]
%@ 	[-A,B,-C,D,-E,F]
%@ 	[-A,B,-C,D,E,-F]
%@ 	[-A,B,-C,D,E,F]
%@ 	[-A,B,C,-D,-F]
%@ 	[-A,B,C,-D,-E]
%@ 	[A,-B,-C,D,-E,F]
%@ 	[A,-B,-C,D,E,-F]
%@ 	[A,-B,-C,D,E,F]
%@ 	[A,-B,C,-D,-F]
%@ 	[A,-B,C,-D,-E]
%@ 	[A,B,C,-D,-F]
%@ 	[A,B,C,-D,-E]
%@ -------------------
%@  zid = 424
%@ 	[-A,-B,-C,D,-E,F]
%@ 	[-A,-B,-C,D,E,-F]
%@ 	[-A,-B,-C,D,E,F]
%@ 	[-A,B,-C,D,-E,F]
%@ 	[-A,B,-C,D,E,-F]
%@ 	[-A,B,-C,D,E,F]
%@ 	[-A,B,C,-D,-E,-F]
%@ 	[-A,B,C,-D,-E,F]
%@ 	[-A,B,C,-D,E,-F]
%@ 	[A,-B,-C,D,-E,F]
%@ 	[A,-B,-C,D,E,-F]
%@ 	[A,-B,-C,D,E,F]
%@ 	[A,-B,C,-D,-E,-F]
%@ 	[A,-B,C,-D,-E,F]
%@ 	[A,-B,C,-D,E,-F]
%@ 	[A,B,C,-D,-E,-F]
%@ 	[A,B,C,-D,-E,F]
%@ 	[A,B,C,-D,E,-F]
%@ -------------------
%@ % 63,375 inferences, 0.005 CPU in 0.007 seconds (72% CPU, 12708041 Lips)
%@ T2 = A,
%@ T3 = B,
%@ Y1 = C,
%@ T1 = D,
%@ Y2 = E,
%@ Y3 = F.
``````

In Markus Triskas library(clpb) the `(#)/2` is XOR.

Its quite easy, I have only run the contrary part of solve_for/3
through a SAT solver and not `yesterday/6`. And then I used the
SAT solver as a compiler and replaced the contrary part.

To run it through a SAT solver this here:

``````two_liars(T1, T2, T3, Y1, Y2, Y3) :-
contrary(lying_day(0,T1,T2,T3), lying_day(0,Y1,Y2,Y3))
, contrary(lying_day(1,T1,T2,T3), lying_day(1,Y1,Y2,Y3)).
``````

Became this here, returning a formula with XOR in the 7-th argument:

``````two_liars(T1, T2, T3, Y1, Y2, Y3, ((M1#M2)*(M3#M4))) :-
lying_day(0, T1, T2, T3, M1),
lying_day(0, Y1, Y2, Y3, M2),
lying_day(1, T1, T2, T3, M3),
lying_day(1, Y1, Y2, Y3, M4).
``````

The CNF seems to be much longer than the algebraic normal form,
Introduced by the Russian mathematician Ivan Ivanovich Zhegalkin
in 1927. No wonder the two liars is quite an XOR statement.

But I don’t have a paper right now at hand, that shows the further
factoring as in the result of Markus Triska, even don’t know whether
this is rather by accident or whether this is done more systematic?

It seems that the requested formula is tautology, though
I have tested based on my guess. Perhaps it is not relevant to what you might expected. I hope the current zdd library might be enough
for one to test such things for oneself.

``````% ?- F1 = (true#T2*T3#T2*Y1#T3*Y1#Y1),
% F2 = (T1=:=T1*Y2#T1*Y3#Y2*Y3),
% F3 = (T1=\=Y1),
% F4 = (T1=\=T1*T2#T1*T3#T2#T2*T3#T3),
% F5 = (Y1=\=Y1*Y2#Y1*Y3#Y2#Y2*Y3#Y3),
% time((ltr_zdd  X<< cnf(-(F1+F2+F3+F4+F5)))).
%@ % 38,038 inferences, 0.004 CPU in 0.005 seconds (65% CPU, 10699859 Lips)
%@ F1 = #(..),
%@ T2 = A,
%@ T3 = B,
%@ Y1 = C,
%@ F2 = #(..),
%@ T1 = D,
%@ Y2 = E,
%@ Y3 = F,
%@ F3 = (D=\=C),
%@ F4 = #(..),
%@ F5 = #(..),
%@ X = 1.
``````

There is a bug somewhere in your reasoning or how
you enter the formula or how you use your system to
check for tautology. The binary encoding is:

T1 T2 T3 weekday
0 0 0 sunday
0 0 1 monday
0 1 0 tuesday
0 1 1 wednesday
1 0 0 thursday
1 0 1 friday
1 1 0 saturday

Its obviously not a tautology. For example sunday / saturday
doesn’t satisfy the formula, refuting that it would be a tautology.
You can try yourself.

``````?- two_liars(0,0,0,1,1,0).
false.
``````

The only yesterday pair that satisfies the formula,
is thursday / wednesday, namely this here:

``````?- two_liars(1,0,0,0,1,1).
true.
``````

Or using the `solve_for/2` predicate which combines `two_liars/6`
with `yesterday/6`, we find, like in the 1986 paper:

``````̀?- solve_for(T1,T2,T3).
T1 = 1,
T2 = T3, T3 = 0 ;
false.
``````

Do you mean that F1+F2+F3+F4+F5 is not tautology ?
where

``````	F1 = (true#T2*T3#T2*Y1#T3*Y1#Y1),
F2 = (T1=:=T1*Y2#T1*Y3#Y2*Y3),
F3 = (T1=\=Y1),
F4 = (T1=\=T1*T2#T1*T3#T2#T2*T3#T3),
F5 = (Y1=\=Y1*Y2#Y1*Y3#Y2#Y2*Y3#Y3).
``````

If not tautology, I must take time (later) to see what happened.

(Nothing of importance)

Internally, disjunction AND( comma) disjunction
is converted to disjunction incremental way. SAT keeps
the DNF all the time as its normal form.

(Nothing of Importance)

If one of your questions which I can answer was what is the DNF of `(-F1)* (-F2) * (-F3) * (-F4) * (-F5)` ?,
where

``````F1 = (true#T2*T3#T2*Y1#T3*Y1#Y1),
F2 = (T1=:=T1*Y2#T1*Y3#Y2*Y3),
F3 = (T1=\=Y1),
F4 = (T1=\=T1*T2#T1*T3#T2#T2*T3#T3),
F5 = (Y1=\=Y1*Y2#Y1*Y3#Y2#Y2*Y3#Y3).
``````

The answer by my dnf is

``````%	 ( ltr_zdd X<< dnf((-F1)* (-F2) * (-F3) * (-F4) * (-F5)), psa(X)).
%@  zid = 0
%@ 	0
%@ -------------------
``````

which means that is “FALSE” (unsatisfible).

Seems you are totally off topic and not talking about the two Liars
from the riddle, namely this here what Alice in the forest hears
from the animals:

Lion: Yesterday was one of my lying days.
Unicorn: Yesterday was one of my lying days.

Thats why my predicate is called two_liars/6. First liar is Lion,
the second liar is Unicorn, in total we have two liars.

There is a bug somewhere in your reasoning or how you enter
the formula or how you use your system to check for antinomy.
Since you make a quite far off claim.

But the riddle gives a hint that it is satisfiable. Even uniquely
satisfiable, since the riddle says:

From these statements, Alice, who was a bright girl, was able to
deduce the day of the week. What was it?

You can also verify satisfiable via my Prolog code:

Or via library(clpb) by using the predicate which has this documentation:

labeling(+Vs)
Assigns truth values to the variables Vs such that all constraints are satisfied.

So if I use this SAT solver predicate I also find that it is satisfiable:

No. I am talking about propositional formula you gave. On the other hand, satisfiability of the puzzle was already shown by my SAT solver with my formulation of the puzzle in propositional logic, which I was satisfied enough not to have interest in other solutions. I need time to digest your idea.

You are using the wrong formula then. My formula is:

``````sat(1#T2*T3#T2*Y1#T3*Y1#Y1),
sat(T1=:=T1*Y2#T1*Y3#Y2*Y3),
sat(T1=\=Y1),
sat(T1=\=T1*T2#T1*T3#T2#T2*T3#T3),
sat(Y1=\=Y1*Y2#Y1*Y3#Y2#Y2*Y3#Y3)
``````

Which is the same as, i.e. conjunction. I already explained
at length that it is a conjunction, but you didn’t listen!

``````sat((1#T2*T3#T2*Y1#T3*Y1#Y1)
*(T1=:=T1*Y2#T1*Y3#Y2*Y3)
*(T1=\=Y1)
*(T1=\=T1*T2#T1*T3#T2#T2*T3#T3)
*(Y1=\=Y1*Y2#Y1*Y3#Y2#Y2*Y3#Y3)).
``````

Which is neither a tautology, i.e. always true, nor an antinomy,
i.e. always false. You can use this predicate from the documentation
to check that it is neither a tautology nor an antinomy:

taut(+Expr, -T)
If Expr is a tautology with respect to the posted constraints,
succeeds with T = 1. If Expr cannot be satisfied,
succeeds with T = 0. Otherwise, it fails.

I get this result, its neither a tautology nor an antinomy:

Sorry for that. I will check later when I come back home. I am taking coffee at a feed corner.

(Nothing of Importance)

Aster inserting parens by guess base, the test result is
as you said.

``````% ?- F =
%    (T1=\=Y1) *
%    ( T1=:=(T1*Y2) xor (T1*Y3) xor (Y2*Y3)) *
%    ( Y1=:=(T2*T3) xor (T2*Y1) xor (T3*Y1)) *
%    ( T1=\=(T1*T2) xor (T1*T3) xor T2 xor (T2*T3) xor T3) *
%    ( Y1=\=(Y1*Y2) xor (Y1*Y3) xor Y2 xor (Y2*Y3) xor Y3),
%	( ltr_zdd X<<dnf(F), psa(X), ltr_card(X, C)).
%@  zid = 491
%@ 	[-A,B,-C,-D,-E,F]
%@ 	[-A,B,-C,-D,E,-F]
%@ 	[-A,B,-C,-D,E,F]
%@ 	[-A,B,-C,D,-E,F]
%@ 	[-A,B,-C,D,E,-F]
%@ 	[-A,B,-C,D,E,F]
%@ 	[-A,B,C,-D,-E,F]
%@ 	[-A,B,C,-D,E,-F]
%@ 	[-A,B,C,-D,E,F]
%@ 	[A,-B,-C,D,-E,-F]
%@ 	[A,-B,-C,D,-E,F]
%@ 	[A,-B,-C,D,E,-F]
%@ 	[A,-B,C,-D,-E,-F]
%@ 	[A,-B,C,-D,-E,F]
%@ 	[A,-B,C,-D,E,-F]
%@ 	[A,-B,C,D,-E,-F]
%@ 	[A,-B,C,D,-E,F]
%@ 	[A,-B,C,D,E,-F]
%@ -------------------
%@ F = (A=\=B)*(A=:=A*C xor (A*D)xor(C*D))*(B=:=E*F xor (E*B)xor(F*B))*(A=\=A*E xor (A*F)xor E xor (E*F)xor F)*(B=\=B*C xor (B*D)xor C xor (C*D)xor D),
%@ T1 = A,
%@ Y1 = B,
%@ Y2 = C,
%@ Y3 = D,
%@ T2 = E,
%@ T3 = F,
%@ X = 491,
%@ C = 18.

% ?- F =
%    (T1=\=Y1) *
%    ( T1=:=(T1*Y2) xor (T1*Y3) xor (Y2*Y3)) *
%    ( Y1=:=(T2*T3) xor (T2*Y1) xor (T3*Y1)) *
%    ( T1=\=(T1*T2) xor (T1*T3) xor T2 xor (T2*T3) xor T3) *
%    ( Y1=\=(Y1*Y2) xor (Y1*Y3) xor Y2 xor (Y2*Y3) xor Y3),
%	 prove(F).
%@ INVALID
%@ F = (T1=\=Y1)*(T1=:=T1*Y2 xor (T1*Y3)xor(Y2*Y3))*(Y1=:=T2*T3 xor (T2*Y1)xor(T3*Y1))*(T1=\=T1*T2 xor (T1*T3)xor T2 xor (T2*T3)xor T3)*(Y1=\=Y1*Y2 xor (Y1*Y3)xor Y2 xor (Y2*Y3)xor Y3).
``````

It is not suprising that my DNF/CNF based on ZDD have drawbacks. However I noticed several merits of it due to high structure sharing caused by ZDD. Let me explain one of them.

Suppose 1, 2, 3, 4 ,… are propositional atoms,
and define `p(1) = (1 + -1)`. (`-` for negation).
`p(2) = (1 + 2)*(1 + -2)*(-1 + 2)*(-1 + -2)`
etc.

Clearly p(n) is a CNF and unsatisfiable. So refutation must be successful.

I tested this CNF p(n) on my prover.

``````% ?- N=2, numlist(1, N, Ns), time((	(ltr_zdd P << ltr_pow(Ns), psa(P), resolve(P)))).
%@  zid = 11
%@ 	[- 1,- 2]
%@ 	[- 1,2]
%@ 	[1,- 2]
%@ 	[1,2]
%@ -------------------
%@ % 1,177 inferences, 0.000 CPU in 0.000 seconds (86% CPU, 7133333 Lips)
%@ N = 2,
%@ Ns = [1, 2],
%@ P = 11.

It was surprising to see that it passed even for n=2000; the CNF has 2^2000 clauses.

% ?- N=2000, numlist(1, N, Ns), time((	(ltr_zdd P << ltr_pow(Ns), resolve(P)))).
%@ % 1,285,503,224 inferences, 124.254 CPU in 133.949 seconds (93% CPU, 10345745 Lips)
%@ N = 2000,
%@ Ns = [1, 2, 3, 4, 5, 6, 7, 8, 9|...],
%@ P = 13997.
``````

IMHO, this shows a merit of DNF/CNF based on ZDD.
One could reproduce this experiment on the package pac 1.8.3