conclude(true):-!.
conclude((A, B)):-!, conclude(A), conclude(B).
conclude(A):-prove(A).
conclude(A):-default((A:-B)), conclude(B), \+ contradiction(A).

prove(true):-!.
prove((A, B)):-!, prove(A), prove(B).
prove(A):-rule((A:-B)), prove(B).

contradiction(\+ A):-!, prove(A).
contradiction(A):-prove(\+ A).

default((flies(X):-bird(X))).
rule((\+ flies(X):-penguin(X))).
rule((bird(X):-penguin(X))).
rule((penguin(tweety):-true)).
rule((bird(opus):-true)).

