app([],X,X).
app([E|R],Ys,[E|Zs]) :- app(R,Ys,Zs).

prove(true) :- !.
prove((G1,G2)) :- !, prove(G1), prove(G2).
prove(L) :- clause(L,G), prove(G).

% Beweislaenge berechnet:
lprove(true,0) :- !.
lprove((G1,G2),L) :- !, lprove(G1,L1), lprove(G2,L2), L is L1+L2.
lprove(L,Len) :- clause(L,G), lprove(G,GL), Len is GL+1.
