prove(clause(X, Y)):-clause(X, Y).
prove(A=A).
prove(\+ A):- \+ prove(A).
prove(Goal):-
	\+(Goal = true), \+(Goal = ','(_, _)), \+(Goal = \+(_)), 
	\+(Goal = '='(_, _)), \+(Goal = clause(_, _)),
	clause(Goal, Body), prove(Body).
prove((Goal1, Goal2)):-
	prove(Goal1),
	prove(Goal2).
prove(true).

male(mark).
parent_of(mark, jim).
father_of(X, Y):-parent_of(X, Y), male(X).