prove(true).
prove((P,Q)) :- prove(P), prove(Q).

prove(P) :- 
    clause((P :- Q)),
    (cut_split(Q,Before,After)
        -> (prove(Before), !, prove(After))
        ;  prove(Q) ).

cut_split((!), true, true).
cut_split((P,Q), Before, (After,Q)) :- 
    cut_split(P, Before, After).
cut_split((P,Q), (P,Before), After) :-
    cut_split(Q, Before, After).



clause((mem2(A, [A|Rest]) :- !)).
clause((mem2(A, [B|Rest]) :- mem2(A, Rest))).

clause((member(A, [A|Rest]) :- true)).
clause((member(A, [B|Rest]) :- member(A, Rest))).