1 eleb(P) :- rule(_,pos(P)).
   2 
   3 nhold(conjunction(S)) :- eleb(conjunction(S)), not hold(P), set(S,pos(P)).
   4 nhold(conjunction(S)) :- eleb(conjunction(S)),     hold(P), set(S,neg(P)).
   5  hold(conjunction(S)) :- eleb(conjunction(S)), not nhold(conjunction(S)).
   6 
   7 hold(atom(A))                     :- rule(pos(atom(A)),   pos(B)), hold(B).
   8                                   :- rule(pos(false),     pos(B)), hold(B).
   9 { hold(P) : wlist(S,_,pos(P),_) } :- rule(pos(sum(_,S,_)),pos(B)), hold(B).
  10 
  11 elem(E) :- eleb(E).
  12 elem(E) :- rule(pos(E),_).
  13 elem(P) :- rule(pos(sum(_,S,_)),_), wlist(S,_,pos(P),_).
  14 elem(P) :- minimize(J,S),           wlist(S,_,pos(P),W).
  15 
  16 supp(atom(A),B) :- rule(pos(atom(A)),   pos(B)).
  17 supp(atom(A),B) :- rule(pos(sum(_,S,_)),pos(B)), wlist(S,_,pos(atom(A)),_).
  18 
  19 supp(atom(A))   :- supp(atom(A),B).
  20 
  21 set(S) :- set(S,E).
  22 fact(atom(A))   :- rule(pos(atom(A)),pos(conjunction(S))), not set(S).
  23 
  24 true(atom(A))                 :- fact(atom(A)).
  25 true(atom(A)) | fail(atom(A)) :- supp(atom(A)), not fact(atom(A)).
  26                 fail(atom(A)) :- elem(atom(A)), not supp(atom(A)).
  27 
  28 fail(false).
  29 
  30 sett(S,0,P)    :- set(S,P).
  31 sett(S,N+1,P2) :- sett(S,N,P1), sett(S,N,P2), P1 < P2.
  32 
  33 setn(S,N,P) :- sett(S,N,P), not sett(S,N+1,P).
  34 setn(S,N)  :- setn(S,N,_).
  35 
  36 true(conjunction(S),N+1) :- elem(conjunction(S)), setn(S,N), not setn(S,N+1).
  37 true(conjunction(S),N)   :- elem(conjunction(S)), true(P), setn(S,N,pos(P)), true(conjunction(S),N+1).
  38 true(conjunction(S),N)   :- elem(conjunction(S)), fail(P), setn(S,N,neg(P)), true(conjunction(S),N+1).
  39 
  40 true(conjunction(S)) :- true(conjunction(S),0).
  41 fail(conjunction(S)) :- elem(conjunction(S)), set(S,pos(P)), fail(P).
  42 fail(conjunction(S)) :- elem(conjunction(S)), set(S,neg(N)), true(N).
  43 
  44 suppt(S,0,P)    :- supp(S,P).
  45 suppt(S,N+1,P2) :- suppt(S,N,P1), suppt(S,N,P2), P1 < P2.
  46 
  47 suppn(S,N,P) :- suppt(S,N,P), not suppt(S,N+1,P).
  48 suppn(S,N)  :- suppn(S,N,_).
  49 
  50 suppf(S,N+1) :- suppn(S,N), not suppn(S,N+1).
  51 suppf(S,N)   :- fail(P), suppn(S,N,P), suppf(S,N+1).
  52 
  53 bot :- true(atom(A)), suppf(atom(A),0).
  54 bot :- rule(pos(H),pos(B)), true(B), fail(H).
  55 
  56 true(atom(A)) :- supp(atom(A)), not fact(atom(A)), bot.
  57 fail(atom(A)) :- supp(atom(A)), not fact(atom(A)), bot.
  58 
  59 target(P,N) :- minimize(_,S), wlist(S,N,pos(P),_).
  60 target(N) :- target(P,N).
  61 
  62 equal(N+1) :- target(N), not target(N+1).
  63 equal(N) :- target(P,N), true(P),     hold(P), equal(N+1).
  64 equal(N) :- target(P,N), fail(P), not hold(P), equal(N+1).
  65 
  66 bot :- equal(0).
  67 bot :- target(P,_), true(P), not hold(P).
  68 
  69 :- not bot.