:- ensure_loaded(pttp).

%% This  propositional example shows pttp proving r from {p=>r, q=>r, p or q}

% translate the clauses using pttp
:-  pttp((
        % p implies q
        % p => r
        (r ; not_p),

        % q imples r
        % q => r
        (r ; not_q),

       % p or q is true
       % p OR q
       (p ; q)
     )).

% Can we prove that r follows from the sentences in 100 steps?
hw6 :- prove(r, 100).