:- lib(iso), set_flag(occur_check,on), dynamic p/0,lit/3.

prove(F) :- prove2(F,[cut,comp(7)]).

prove2(F,S) :- (F=[_|_]->M=F;make_matrix(F,M,S)),
 retract_all(lit(_,_,_)), (member([-(#)],M)->T=conj;T=pos),
 ast(M,T), prove(1,S).

prove(I,S) :- \+member(scut,S) -> prove([-(#)],[],I,[],S) ;
    lit(#,C,_) -> prove(C,[-(#)],I,[],S).
prove(I,S) :- member(comp(L),S), I=L -> prove(1,[]) ;
    (member(comp(_),S);retract(p)) -> J is I+1, prove(J,S).
prove([],_,_,_,_).
prove([L|C],P,I,Q,S) :- \+ (member(A,[L|C]), member(B,P),
    A==B), (-N=L;-L=N) -> ( member(D,Q), L==D ;
    member(E,P), unify_with_occurs_check(E,N) ; lit(N,F,H),
    (H=g -> true ; length(P,K), K<I -> true ;
    \+p -> assert(p), fail), prove(F,[L|P],I,Q,S) ),
    (member(cut,S) -> ! ; true), prove(C,P,I,[L|Q],S).

ast([],_).
ast([C|M],S) :- (S\=conj,\+member(-_,C)->D=[#|C];D=C),
 (ground(C)->G=g;G=n), ast2(D,[],G), ast(M,S).
ast2([],_,_).
ast2([L|C],D,G) :-
 append(D,C,E), assert(lit(L,E,G)), append(D,[L],F), ast2(C,F,G).