/* EQUAL.

Test example for BREADT and HEURIS.
Symmetry can be inferred from reflexivity and twisted transitivity
(notes p62).

Alan Bundy  22.6.81 */

clause(hypothesis, [equal(x,y)], [], input ).   % Input clauses
clause(reflexive,  [equal(X,X)], [], input ).
clause(twisted,    [equal(U,W)], [equal(U,V), equal(W,V)], input ).

clause(goal,       [], [equal(y,x)], topclause).        % Top clause