```    1% ?- [misc(zdd)], module(zdd).
2%@ true.
3% ?- zdd((boole_to_cnf(a, X), cnf_dnf(X, Y))).
4% ?- zdd((boole_to_cnf(a+b, X), cnf_dnf(X, Y))).
5
6
7% ?- [misc(zdd)], module(zdd).
8
9% ?- z(({expand_macro(a=b, A), boole_to_cnf(A, X),  sets(X, S)})).
10% ?- z(({expand_macro(a=b, A), boole_to_dnf(A, X),  sets(X, S)})).
11% ?- z((cnf(a=b, X), sets(X, S))).
12% ?- z(({sets(true, X)})).
13% ?- z((cnf(a=b, X), sets(X, S))).
14% ?- z((dnf(a=b, X), sets(X, S))).
15% ?- z((dnf((a=b)*(b=c), X), sets(X, S))).
16% ?- z((dnf((a->b)*(b->c)*(c->a), X), sets(X, S))).
17% ?- zcon((dnf((-a + b)*(-b + a), X), card(X, C), sets(X, S))).
18% ?- zcon((dnf((-a + b)*(-b) + (-a + b) * a, X), card(X, C), sets(X, S))).
19% ?- zcon((dnf((-a + b)*(-b) + (-a + b) * a, X), card(X, C), sets(X, S))).
20% ?- zcon((dnf((-a + b)*(-b), A), dnf((-a + b) * a, B), sets(A, Sa))).
21% ?- zcon((dnf((-a + b)*(-b), A), dnf((-a + b) * a, B),
22%	sets(A, Sa), sets(B, Sb), dnf_join(A, B, C), sets(C, Sc))).
23% ?- zcon((dnf((-a + b)*(a), A), dnf((-a + b) * (-b), B),
24%	sets(A, Sa), sets(B, Sb), dnf_join(A, B, C), sets(C, Sc))).
25% ?- zcon((dnf((-a + b)*(a + -b), A), sets(A, Sa))).
26% ?- zcon((dnf((-a + b), A), dnf((a + -b), B),  dnf_merge(A, B, C),
27%	sets(A, Sa), sets(B, Sb), sets(C, Sc))).
28% ?- zcon((dnf((a + -b), B),  dnf((-a + b), A), dnf_merge(A, B, C),
29%	sets(A, Sa), sets(B, Sb), sets(C, Sc))).
30% ?- zcon((dnf((a + -b), B),  dnf((-a), A), dnf_merge(B, A,C),
31%	sets(A, Sa), sets(B, Sb), sets(C, Sc))).
32% ?- zcon((dnf(a+b, X), sets(X, S), card(X, C))).
33% ?- zcon((dnf(a*b, X), sets(X, S), card(X, C))).
34% ?- zcon((dnf(a+b+c, X), sets(X, S), card(X, C))).
35% ?- N=2, continue((problem(N, P), intern(P, P0), expand_macro(P0, P1),
36%	boole_to_dnf(P1, X), card(X, Count))).
37% ?- N=3, continue((problem(N, P), intern(P, P0), expand_macro(P0, P1),
38%	boole_to_dnf(P1, X), card(X, Count))).
39% ?- N=4, continue((problem(N, P), intern(P, P0), expand_macro(P0, P1),
40%	boole_to_cnf(P1, X), cnf_to_dnf(X, Y), card(Y, Count))).
41% ?- N=4, continue((problem(N, P), intern(P, P0), cnf(P0, X),
42%	cnf_to_dnf(X, Y), card(Y, Count))).
43% ?- N=5, continue((problem(N, P), intern(P, P0), expand_macro(P0, P1),
44%	boole_to_cnf(P1, X))).
45% ?- time((N=5, continue((problem(N, P), intern(P, P0), expand_macro(P0, P1),
46%	boole_to_cnf(P1, X))))).
47%@ % 2,735,010 inferences, 0.506 CPU in 0.518 seconds (98% CPU, 5403375 Lips)
48%@ N = 5,
49% ?- time((N=6, continue((problem(N, P), intern(P, P0), expand_macro(P0, P1),
50%	boole_to_cnf(P1, X))))).
51% ?- time((N=7, continue((problem(N, P), intern(P, P0), expand_macro(P0, P1),
52%	boole_to_cnf(P1, X))))).
53%@ % 125,070,803 inferences, 15.629 CPU in 15.769 seconds (99% CPU, 8002696 Lips)
54
55% ?- time((N=5, continue((problem(N, P), intern(P, P0), expand_macro(P0, P1),
56%	boole_to_cnf(P1, X), card(X, C), cnf_to_dnf(X, Y), card(Y, D))))).
57
58% ?- time((N=7, continue((problem(N, P), intern(P, P0), expand_macro(P0, P1),
59%	boole_to_cnf(P1, X))))).
60%@ % 200,468,499 inferences, 57.112 CPU in 57.614 seconds (99% CPU, 3510092 Lips)
61%@ N = 7,
62%@ X = 116269 .
63
64% ?- N = 4, profile(time(continue((problem(N, P), dnf(P, X), card(X, C))))).
65%@ % 2,597,494 inferences, 0.366 CPU in 0.372 seconds (98% CPU, 7098607 Lips)
66%@ X = 19140,
67%@ C = 48.
68
69% ?- N = 5, profile(time(continue((problem(N, P), dnf(P, X), card(X, C))))).
70%@ % 41,489,433 inferences, 7.197 CPU in 7.281 seconds (99% CPU, 5764730 Lips)
71
72% [2018/10/27]
73% ?- N = 6, profile(time(continue((problem(N, P), dnf(P, X), card(X, C))))).
74%@ % 528,789,284 inferences, 104.530 CPU
75%@ C = 23040.
76
77% ?- N = 6, profile(time(continue((problem(N, P), dnf(P, X), card(X, C))))).
78%@ % 658,341,726 inferences, 126.430 CPU in 128.935 seconds (98% CPU, 5207154 Lips)
79%@ % 884,280,094 inferences, 508.885 CPU in 514.144 seconds (99% CPU, 1737683 Lips)
80%@ C = 23040.
81
82% ?- [misc(zdd)], module(zdd).
83% ?- N = 1, profile(time(continue((problem(N, P), intern(P, P1), cnf(P1, X))))).
84% ?- N = 2, profile(time(continue((problem(N, P), intern(P, P1), cnf(P1, X))))).
85% ?- N = 2, profile(time(continue(( problem(N, P),
86%	intern(P, P1), cnf(P1, X), cnf_to_dnf(X, P2), card(P2, C))))).
87
88%@
89
90% ?- N = 3, profile(time(continue((problem(N, P), intern(P, P1), cnf(P1, X))))).
91
92% ?- N = 4, profile(time(continue((problem(N, P), intern(P, P1), cnf(P1, X))))).
93% ?- N = 5, profile(time(continue((problem(N, P), intern(P, P1), cnf(P1, X))))).
94% ?- N = 6, profile(time(continue((problem(N, P), intern(P, P1), cnf(P1, X))))).
95% ?- N = 7, profile(time(continue((problem(N, P), intern(P, P1), cnf(P1, X))))).
96
97% [2018/10/28]
98% ?- N = 8, profile(time(continue((problem(N, P), intern(P, P1), cnf(P1, X))))).
99%@ % 863,769,430 inferences, 156.970 CPU
100%@ X = 419824.
101%@ % 1,612,695,532 inferences, 519.781 CPU
102%@ X = 419944.
103%
104% ?- time(continue((problem(3, P), intern(P, Q), zdd_cnf(Q, X)))).
105% ?- time(continue((problem(4, P), intern(P, Q), zdd_cnf(Q, X)))).
106% ?- time(continue((problem(5, P), intern(P, Q), zdd_cnf(Q, X)))).
107% ?- time(continue((problem(6, P), intern(P, Q), zdd_cnf(Q, X)))).
108% ?- N=1, problem(N, P), continue((intern(P, P1),
109%	zdd_cnf(P1, Y), card(Y, C))).
110% ?- N=2, problem(N, P), continue((intern(P, P1),
111%	zdd_cnf(P1, Y), card(Y, C))).
112% ?- N=3, problem(N, P), continue((intern(P, P1),
113%	zdd_dnf(P1, Y), card(Y, C))).
114% ?- N=5, problem(N, P), continue((intern(P, P1),
115%	zdd_dnf(P1, Y), card(Y, C))).
116
117% ?- [misc(zdd)], module(zdd).
```
zdd_dnf(+X, -Y, +G) is det
Unify a ZDD Y with a ZDD of a disjunctive normal form of a formula X.
```  124% ?- continue((zdd_dnf(a* b, Y), sets(Y, S))).
125% ?- z((dnf(a* b, Y), sets(Y, S))).
126% ?- continue((zdd_dnf(a + b, Y), sets(Y, S))).
127% ?- N=1, problem(N, P), continue((intern(P, P1),
128%	zdd_dnf(P1, Y), card(Y, C))).
129% ?- N=2, problem(N, P), continue((intern(P, P1),
130%	zdd_dnf(P1, Y), card(Y, C))).
131% ?- N=3, problem(N, P), continue((intern(P, P1),
132%	zdd_dnf(P1, Y), card(Y, C))).
133% ?- N=5, problem(N, P), continue((intern(P, P1),
134%	zdd_dnf(P1, Y), card(Y, C))).
135
136
137% ?- [misc(zdd)], module(zdd).
138% ?- zcon((dnf(a+b, Y), sets(Y, Sy), dnf_to_cnf(Y, Z), sets(Z, S))).
139% ?- zcon((dnf((a+b+c)*(x+y), X), sets(X, Sx), maplist(writeln, Sx),
140%	dnf_to_cnf(X, Y), sets(Y, Sy))),
141%	maplist(writeln, Sy).
142% ?- zcon((cnf((a+b+c)*((-a)+ -(b)), X), cnf_to_dnf(X, Y), sets(Y, Sy))),
143%	maplist(writeln, Sy).
144% ?- zcon((dnf((a+b+c)*(x+y), X), dnf_to_cnf(X, Y),
145%	cnf_to_dnf(Y, Z),  sets(Y, Sy), sets(Z, Sz),
146%	maplist(writeln, Sy), maplist(writeln, Sz))).
147
148
149% ?- [misc(zdd)], module(zdd).
150% ?- trace, z((dnf(a+b, Y), card(Y, C))).
151% ?- N = 1, problem(N, P),  z((intern(P, P1), {cnf(P1, Y)})).
152% ?- N = 2, problem(N, P), zdd((intern(P, P1),
153%	cnf(P1, P2), cnf_to_dnf(P2, P3), sets(P2, Sp2), {maplist(writeln, Sp2)}
154% )).
155% ?- N = 2, problem(N, P), zdd((intern(P, P1),
156%	cnf(P1, P2), cnf_to_dnf(P2, P3), sets(P2, Sp2), Z=family(Sp2),
157%	sets(Z, Sz), {maplist(writeln, Sz)}, {Sp2=Sz}
158% )).
159% ?- N = 2, problem(N, P), zdd((intern(P, P1),
160%	cnf(P1, P2), cnf_to_dnf(P2, P3), sets(P2, Sp2), Z=family(Sp2),
161%	sets(Z, Sz), {maplist(writeln, Sz), maplist(writeln, Sz)},
162%	U = family(Sz), card(P3, C)
163% )).
164
165% ?- N = 2, problem(N, P), zdd((intern(P, P1),
166%	cnf(P1, P2), sets(P2, S2), {!},
167%	F2=family(S2), sets(F2, Sf2), cnf_to_dnf(P2, P3),
168%	sets(P3, S3), {Sf2=S2}, {maplist(writeln, S2)}
169% )).
170
171
172% ?- N = 2, problem(N, P), zdd((intern(P, P1),
173%	cnf(P1, P2), sets(P2, S2), {maplist(writeln, S2)},
174%	cnf_to_dnf(P2, D2), sets(D2, Sd2), {maplist(writeln, Sd2)}
175% )).
176
177% ?- N = 2, problem(N, P), zdd((intern(P, P1),
178%	cnf(P1, P2), sets(P2, S2), {maplist(writeln, S2)},
179%	cnf_to_dnf(P2, D2), sets(D2, Sd2), dnf_to_cnf(D2, C3),
180%	{maplist(writeln, Sd2)}
181% )).
182
183
184% ?- N = 2, problem(N, P),  continue((intern(P, P1),
185%	cnf(P1, X), cnf_dnf(X, Y))).
186%@ Y = false .
187
188% ?- zcon((cnf(a, A), neg_cnf_to_dnf(A, B), sets(B, S))).
189% ?- zcon((cnf(a+b, A),sets(A, Sa),  neg_cnf_to_dnf(A, B), sets(B, S))).
190% ?- zcon((cnf(a*b, A), sets(A, Sa), neg_cnf_to_dnf(A, B), sets(B, S))).
191% ?- zcon((cnf((a+b)*(c+d), A), neg_cnf_to_dnf(A, B), sets(B, S))).
192% ?- zcon((cnf((a+ -(b))*(c+ -d), A), neg_cnf_to_dnf(A, B), sets(B, S))).
193
194% ?- z((dnf(a, A), neg_dnf_to_cnf(A, B), sets(B, S))).
195% ?- z((dnf(a, A))).
196% ?- zcon((dnf(a+b, A), sets(A, Sa),  neg_dnf_to_cnf(A, B), sets(B, S))).
197% ?- zcon((dnf(a*b, A), sets(A, Sa), neg_dnf_to_cnf(A, B), sets(B, S))).
198% ?- zcon((dnf((a+b)*(c+d), A), neg_dnf_to_cnf(A, B), sets(B, S))).
199% ?- zcon((dnf((a+ -(b))*(c+ -d), A), neg_dnf_to_cnf(A, B), sets(B, S))).
200
201% ?- solve([X := [[1,2], [2,3]]]), zdd_unify(X, [2=3], Y),  sets(Y, S).
202% ?- solve([X := [[1,2], [2,3]]]), zdd_unify(X, [3=2], Y),  sets(Y, S).
203% ?- solve([X:=[[1,2],[3,4]]]), zdd_unify(X, [1=2,3=4], Y),  sets(Y, S).
204% ?- solve([X:=[[a-1,b-2],[a-3,b-4]]]),
205%	zdd_unify(X, [a-1=b-2,a-3=b-4], Y),  sets(Y, S).
206% ?- solve([X:=[[a-1,b-2],[a-3,b-4]]]),
207%	zdd_unify(X, [a-1=a-3,b-2=b-4], Y),  sets(Y, S).
208% ?- solve([X:=[[a-0,b-0],[a-0,b-1], [a-1,b-0],[a-1,b-1]]]),
209% zdd_unify(X, [a-0=b-0,a-1=b-1], Y),  sets(Y,S).
210
211
212% ?- continue(fos(b(1)+b(2), S)).
213% ?- continue(fos((-a)+(-b), S)).
214% ?- continue(fos((-a)+(-b), S, C)).
215% ?- continue(fos((-1)*(-2), _, C)).
216% ?- continue((zdd([X:=fos((-1)*(-2))]), sets(X, S))).
217% ?- continue((zdd([X:=fos((-1)+(-2))]), sets(X, S), card(X, C))).
218% ?- continue((zdd([X:=sat((-1)*(-2))]), sets(X, S))).
219% ?- continue((zdd([X:=fos(-(1)+ -(2))]), sets(X, S))).
220% ?- continue((zdd([X:=fos(-(1+2))]), sets(X, S))).
221% ?- continue((fos([X:=[[a]]]), zdd_path(X))).
222% ?- continue((fos([X:=pow([a,b,c]), Y:=pow([e,f]), join(X, Y, Z)]), zdd_path(Z))).
223
224% ?- continue(solc(true, X, [card(X)])).
225% ?- continue(solc(false, X, [card(X)])).
226% ?- continue(solc(a, X)).
227% ?- continue(solc(a+b, X)).
228% ?- continue((problem(1, P), solc(P, X))).
229% ?- continue((problem(2, P), solc(P, X))).
230% ?- continue((problem(3, P), solc(P, X))).
231% ?- continue((problem(4, P), solc(P, X))).
232% ?- continue((problem(5, P), solc(P, X))).
233% ?- continue((problem(6, P), solc(P, X))).
234% ?- time(continue((problem(7, P), solc(P, X)))).
235%@ % 366,853,945 inferences, 94.389 CPU in 96.556 seconds (98% CPU, 3886607 Lips)
236%@ X = 1451520 .
237% ?- time(continue((problem(7, P), solc(P, X)))).
238%@ % 366,853,944 inferences, 95.511 CPU in 97.224 seconds (98% CPU, 3840964 Lips)
239%@ X = 1451520 .
240
241
242% ?- continue(get_extra_key(varnum, D)).
243% ?- z(dnf(a, X)).
244% ?- continue((prepare_sat(2), zdd_memo(filter(2)-U), sets(U, S))).
245% ?- continue((prepare_sat(2), zdd_memo(filter(1)-U), sets(U, S))).
246% ?- continue((prepare_sat(3), zdd_memo(filter(1)-U), sets(U, S))).
247% ?- continue((prepare_sat(3), zdd_memo(filter(2)-U), sets(U, S))).
248% ?- continue((prepare_sat(3), zdd_memo(filter(3)-U), sets(U, S))).
249
250% ?- solc(a+b+c, C), zdd_path.
251% ?- solve([X:=pow([a, b, c])]), zdd_path.
252% ?- open_zdd(h), zdd([X:=pow([a, b])], h), zdd_path([global(h)]).
253% ?- rozdd(pow([a, b]), X), get_vector(rozdd, _, Vec), zdd_path(Vec, X).
254
255
256% ?- [misc(zdd)], module(zdd).
257% ?- zcon((cnf(false, X), sets(X, S))).
258% ?- zcon((cnf(true, X), sets(X, S))).
259% ?- zcon((cnf(a+b, X), sets(X, S))).
260% ?- zcon((cnf(a * (-a), X), sets(X, S))).
261% ?- zcon((cnf(a + (-a), X), sets(X, S))).
262% ?- zcon((cnf(-(a) + (-a), X), sets(X, S))).
263% ?- zcon((cnf(-(a) * a, X), sets(X, S))).
264% ?- zcon((cnf((a+b)*(a+b)*(a+b), X), sets(X, S))).
265% ?- zcon((cnf((a*b)+(a+b)+(a*b), X), sets(X, S))).
266% ?- zdd((cnf(-(a) * a, X), sets(X, S))).
267% ?- zdd((cnf((a+b)*(a+b)*(a+b), X), sets(X, S))).
268% ?- zdd((cnf((a*b)+(a+b)+(a*b), X), sets(X, S))).
269
270% ?- [misc(zdd)], module(zdd).
271% ?- zcon((dnf(false, X), sets(X, S))).
272% ?- zcon((dnf(true, X), sets(X, S))).
273% ?- zcon((dnf(a, X), sets(X, S))).
274% ?- zcon((dnf(-a, X), sets(X, S))).
275% ?- zcon((dnf(a+b, X), sets(X, S))).
276% ?- zcon((dnf(a * (-a), X), sets(X, S))).
277% ?- zcon((dnf(-(a) * a, X), sets(X, S))).
278% ?- zcon((dnf(a + (-a), X), sets(X, S))).
279% ?- zcon((dnf(a*b + (-a)*b, X), sets(X, S))).
280% ?- zcon((dnf(-(a) + (-a), X), sets(X, S))).
281
282% ?- z((X=[a], ltr_remove(a, X, Y), sets(Y, S))).
283% ?- z((X={[a]}, ltr_remove(a, X, Y), sets(Y, S))).
284% ?- z((X={[a,b,c]}, atom_eliminate(=(a), X, Y), sets(Y, S))).
285% ?- z((X={[a,1,c],[e,f],[g,2,k],[x,y]}, atom_eliminate(integer,X,Y), sets(Y, S))).
286% ?- z((X={[a]}, atom_eliminate(=(a), X, Y), sets(Y, S))).
287
288% ?- z((X={[a,1]}, atom_eliminate(=(a), X, Y), sets(Y, S).
289% ?- z((X={[a,1], [b, c], [d, 2, f]}, atom_eliminate(integer, X, Y), sets(Y, S).
290% ?- z((X={[1, a], [b, c], [2, d, f]}, atom_eliminate(=(b), X, Y), sets(Y, S))).
291% ?- z((X={[1, a], [b, c], [2, d, f]}, atom_eliminate(@=<(b), X, Y), sets(Y, S))).
292% ?- z((X={[1, a], [b, c], [2, d, f]}, atom_eliminate(integer, X, Y), sets(Y, S))).
293% ?- z((X={[1, a], [b, c], [2, d, f]}, atom_eliminate(atom, X, Y), sets(Y, S))).
294% ?- z((X={[1, a], [b, c], [2, d, f]}, atom_eliminate(atomic, X, Y), sets(Y, S))).
295
296
297% ?- z((M=pow([a,b,c,d]), zdd_filter(M, N, supset([a,b])), sets(N, S))).
298% ?- z((M=pow([a,b,c,d]), zdd_filter(M, N, supset([])), sets(N, S))),
299%	length(S, C).
300% ?- z((M=pow([a,b]), zdd_filter(M, N, subset([a])), sets(N, S))).
301% ?- z((M=pow([a,b,c]), zdd_filter(M, N, subset([a,b,c])), sets(N, S))),
302%	length(S, C).
303
304
305% ?- z((dag_to_zdd([1-[2,3], 2-[], 3-[]]),
306% zdd_memo(successors(1)-R), sets(R, S))).
307% ?- z((dag_to_zdd([1-[]]),
308% zdd_memo(successors(1)-R), sets(R, S), card(R, C))).
309% ?- z((dag_to_zdd([1-[2,3], 2-[3],3-[]]),
310% zdd_memo(successors(1)-R), card(R, C))).
311% ?- z((dag_to_zdd([a-[b,c], b-[c],c-[]]),
312% zdd_memo(successors(a)-R), card(R, C), sets(R, S))).
313
314
315% ?- z((X={[1,2],[3,4]},
316%		Y= [X],
317%		U= {[5,6],[7,8]},
318%		V= [U],
319%		meta_shift(4, Y, V),
320%		meta_shift(-4, V, Y))).
321
322
323% ?- z((A={[a]}, B={[b]}, X={[a,b]},
324%	zdd_blowup_plus([a-A, b-B], X, Y), sets(Y, S))).
325% ?- z((A={[c]}, B={[d]}, X={[a,b]},
326%	zdd_blowup_plus([a-A, b-B], X, Y), sets(Y, S))).
327% ?- [misc(zdd)], module(zdd).
328% ?-  z((A={[c]}, B={[d]}, X={[a,b,e]},
329%	zdd_blowup_plus([a-A, b-B], X, Y), sets(Y, S))).
330% ?-  z((X={[a,b,e]}, A={[a]}, B={[b]},
331%	zdd_blowup_plus([a-A], X, Y), sets(Y, S))).
332% ?- z((X={[a,b], [b]}, A={[a]}, B={[b]},
333%	zdd_blowup_plus([a-B, b-A], X, Y), sets(Y, S))).
334% ?- z((X={[a,b]}, A={[a]}, B={[b]},
335%	zdd_blowup_plus([a-B,b-A], X, Y), sets(Y, S))).
336% ?- z((X={[a]}, A={[a]}, B={[b]},
337%	zdd_blowup_plus([b-A], X, Y), sets(Y, S))).
338% ?- z((X={[a,b]}, A={[a]}, B={[b]},
339%	zdd_blowup_plus([a-false,b-false], X, Y), sets(Y, S))).
340% ?- z((X={[a,b]}, A={[a]}, B={[b]},
341%	zdd_blowup_plus([a-B,b-A], X, Y), sets(Y, S))).
342% ?- z((X={[a]}, A={[a]}, B={[b]},
343%	zdd_blowup_plus([a-true,b-true], X, Y), sets(Y, S))).
344% ?- z((X={[a,b]}, A={[a]}, B={[b]},
345%	zdd_blowup_plus([a-true,b-true], X, Y), sets(Y, S))).
346% ?- z((X={[a,b, c]}, A={[a]}, B={[b]},
347%	zdd_blowup_plus([a-true,b-true], X, Y), sets(Y, S))).
348% ?- [misc(zdd)], module(zdd).
349
350% ?- z((X = {[a,b]}, Y = {[c,d]},
351%	zdd_blowup([c-X], Y, Z),
352%	sets(Z, S))).
353% ?- z((Y ={[a,b, c]}, V={[b1,b2]},
354%	zdd_blowup([b-V], Y, Z),
355%	sets(Z, S))).
356% ?- z((Y ={[a,b,c]}, V={[b1],[b2]},
357%	zdd_blowup([b-V], Y, Z),
358%	sets(Z, S))).
359% ?- z((Y={[a,b]}, V={[a1],[a2]}, W={[b1],[b2],[b3]},
360%	zdd_blowup([a-V, b-W], Y, Z),
361%	sets(Z, S))).
362
363% ?-  continue((open_memo(powmove, 20),
364%   internal_power_move([a-[x-[x]]], R),
365%	raise_to_power([x], Init),
366%	power_move([Init], R),
367%	memochk(powmove(a, Init)-J, powmove),
368%	collect_moves_in_hash(H))).
369
370% ?- continue(( open_memo(powmove, 20),
371%   internal_power_move([a-[x-[y], y-[x]], b-[x-[y], y-[x]]], R),
372%	raise_to_power([x], I),
373%	raise_to_power([x,y], J),
374%	power_move([I,J], R),
375%	memo(powmove(a, I)-Ia, powmove),
376%	memo(powmove(a, J)-Ja, powmove),
377%	collect_moves_in_hash(H))).
378
379% ?- continue((open_memo(powmove, 20),
380%   internal_power_move([a-[x-[y], y-[x]], b-[x-[y], y-[x]]], R),
381%	raise_to_power([x], I),
382%	raise_to_power([x,y], J),
383%	power_move([I,J], R),
384%	memo(powmove(a, I)-Ia, powmove),
385%	memo(powmove(a, J)-Ja, powmove),
386%	collect_moves_in_hash(H))).
387
388% ?- continue(power_move_closure([a-[x-[y]], b-[y-[x]]], x, M)).
389% ?- continue((power_move_closure([a-[x-[y]], b-[y-[x]]], x, M),
390%  zdd_path(1), zdd_path(2))).
391
392% ?- [misc(zdd)], module(zdd).
393% ?- N = 1, problem(N, P), sat_count(P, C).
394% ?- N = 3, problem(N, P), sat_count(P, C).
395% ?- N = 4, problem(N, P), sat_count(P, C).
396% ?- N = 5, problem(N, P), sat_count(P, C).
397% ?- N = 6, problem(N, P), sat_count(P, C).
398% ?- N = 7, problem(N, P), time(sat_count(P, C)).  % [2018/10/28]
399%@ % 212,198,227 inferences, 34.801 CPU
400% ?- N = 7, problem(N, P), time(sat_count(P, C)).  % [2018/10/28]
401%@ % 262,658,691 inferences, 36.709 CPU
402% ?- N = 7, problem(N, P), time(sat_count(P, C)).  % [2018/10/26]
403%@ % 212,495,480 inferences, 34.610 CPU
404%@ C = 1451520 .  %% <== correct!
```