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