% Extend Vanilla Interpreter to construct a Proof Tree (use sicstus3)

solve(true, true).

solve((A, B), (ProofA, ProofB)) :- 
	solve(A, ProofA), 
	solve(B, ProofB).

solve(A, (A :- Proof)) :-
	A \= true,
	A \= (_,_),
	clause(A, B),
	solve(B, Proof).