% 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).

% in()-predicate
  all R all S (in(x,y,R * S)  <-> exists z (in(x,z,R) & in(z,y,S))).
  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 all z (in(x,y,S) & in(y,z,S) -> in(x,z,S))) <-> S*S <= S).

end_of_list.