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!