28:- lib(iso).  % load library for ISO compatibility
   29:- set_flag(occur_check,on).  % global occur check on
   30:- [def_mm].  % load program for clausal form translation
   31:- dynamic(pathlim/0), dynamic(lit/3).   32
   33
   34%%% prove matrix M / formula F
   35
   36prove(F,Proof) :- prove2(F,[cut,comp(7)],Proof).
   37
   38prove2(F,Set,Proof) :-
   39    (F=[_|_] -> M=F ; make_matrix(F,M,Set)),
   40    retract_all(lit(_,_,_)), (member([-(#)],M) -> S=conj ; S=pos),
   41    assert_clauses(M,S), prove(1,Set,Proof).
   42
   43prove(PathLim,Set,Proof) :-
   44    \+member(scut,Set) -> prove([-(#)],[],PathLim,[],Set,[Proof]) ;
   45    lit(#,C,_) -> prove(C,[-(#)],PathLim,[],Set,Proof1),
   46    Proof=[C|Proof1].
   47prove(PathLim,Set,Proof) :-
   48    member(comp(Limit),Set), PathLim=Limit -> prove(1,[],Proof) ;
   49    (member(comp(_),Set);retract(pathlim)) ->
   50    PathLim1 is PathLim+1, prove(PathLim1,Set,Proof).
   51
   52%%% leanCoP core prover
   53
   54prove([],_,_,_,_,[]).
   55
   56prove([Lit|Cla],Path,PathLim,Lem,Set,Proof) :-
   57    Proof=[[[NegLit|Cla1]|Proof1]|Proof2],
   58    \+ (member(LitC,[Lit|Cla]), member(LitP,Path), LitC==LitP),
   59    (-NegLit=Lit;-Lit=NegLit) ->
   60       ( member(LitL,Lem), Lit==LitL, Cla1=[], Proof1=[]
   61         ;
   62         member(NegL,Path), unify_with_occurs_check(NegL,NegLit),
   63         Cla1=[], Proof1=[]
   64         ;
   65         lit(NegLit,Cla1,Grnd1),
   66         ( Grnd1=g -> true ; length(Path,K), K<PathLim -> true ;
   67           \+ pathlim -> assert(pathlim), fail ),
   68         prove(Cla1,[Lit|Path],PathLim,Lem,Set,Proof1)
   69       ),
   70       ( member(cut,Set) -> ! ; true ),
   71       prove(Cla,Path,PathLim,[Lit|Lem],Set,Proof2).
   72
   73%%% write clauses into Prolog's database
   74
   75assert_clauses([],_).
   76assert_clauses([C|M],Set) :-
   77    (Set\=conj, \+member(-_,C) -> C1=[#|C] ; C1=C),
   78    (ground(C) -> G=g ; G=n), assert_clauses2(C1,[],G),
   79    assert_clauses(M,Set).
   80
   81assert_clauses2([],_,_).
   82assert_clauses2([L|C],C1,G) :-
   83    append(C1,C,C2), assert(lit(L,C2,G)), append(C1,[L],C3),
   84    assert_clauses2(C,C3,G)