%%%
%%% lolliCoP2 : a lean connection-method theorem prover
%%% 	        Lolli/LLP implementation of leanCoP
%%%
%%% Version : 1.0
%%%
%%% Author : Naoyuki Tamura  (tamura@kobe-u.ac.jp)
%%%          Joshua S. Hodas (hodas@cs.hmc.edu)
%%% 
%%% lolliCoP http://www.cs.hmc.edu/~hodas/research/lollicop/
%%% Lolli    http://www.cs.hmc.edu/~hodas/lolli/
%%% LLP      http://bach.seg.kobe-u.ac.jp/llp/
%%%

main :-
	read(f(Mat)),
	write('START lolliCoP2 1.0 '), nl,
	flush_output(user_output),
        prolog_flag(occurs_check, _, on),
        statistics(runtime, [T1|_]),
	(prove(Mat) ->
	    write('OK ')
	;
	    write('NG ')
	),
        statistics(runtime, [T2|_]),
        T is T2 - T1,
	write(T), nl.
	
prove(Mat) :-
        reverse(Mat, Mat1),
	(ground(Mat1) ->
	    propositional => pr(Mat1)
	;
	    pr(Mat1)
	).

pr([]) :-
        p(1).
pr([Cla|Mat]) :-
        (ground(Cla) ->
            (forall [PathLim] \ cl(Cla, PathLim)) -<> pr(Mat)
        ;
            (forall [Cla1,PathLim] \ cl(Cla1, PathLim) :-
                PathLim > 0, copy_term(Cla, Cla1))  => pr(Mat)
        ).

p(PathLim) :-
        cl(Cla1, PathLim),
        \+ member(-_, Cla1),
        prove(Cla1, PathLim).
p(PathLim) :-
	\+ propositional,
        PathLim1 is PathLim + 1,
        p(PathLim1).

prove([], _) :-
	erase.
prove([Lit|Cla], PathLim) :-
        (-NegLit=Lit; -Lit=NegLit) ->
        (
            path(NegLit),
            erase
        ;
            cl(Cla2, PathLim),
            append(ClaA, [NegLit|ClaB], Cla2),
            append(ClaA, ClaB, Cla3),
            PathLim1 is PathLim - 1,
            path(Lit) => prove(Cla3, PathLim1)
        )
        &
        prove(Cla, PathLim).

member(X, [X|_]).
member(X, [_|L]) :-
        member(X, L).

append([], Zs, Zs).
append([X|Xs], Ys, [X|Zs]) :-
        append(Xs, Ys, Zs).

reverse(Xs, Zs) :-
        reverse(Xs, [], Zs).

reverse([], Zs, Zs).
reverse([X|Xs], Ys, Zs) :-
        reverse(Xs, [X|Ys], Zs).