% Language Options

op(500, infix,   "\/").
op(490, infix,   "/\").
op(300, postfix, "'").
op(480, infix,   "*").
op(300, postfix, "^").
op(520, infix,   "<=").
op(520, infix,   "==").
op(510, prefix,  "in").

formulas(assumptions).

  all R all S (in(x,y,R \/ S) <-> (in(x,y,R) | in(x,y,S))).
  all R all S (in(x,y,R /\ S) <-> (in(x,y,R) & in(x,y,S))).
  all R       (in(x,y,R^)     <-> in(y,x,R)).

  in(x,y,I) <-> x=y.

  all R all S (R <= S <-> (all x all y (in(x,y,R) -> in(x,y,S)))).

end_of_list.

formulas(goals).
  all S ((all x all y ((in(x,y,S) & in(y,x,S)) -> x=y)) -> S /\ S^ <= I).
end_of_list.