テスト用時田

formulas(sos).


end_of_list.

formulas(goals).

  ((all w1 (in(w1,xX) <-> in(w1,xY))) <-> ((all w1 (in(w1,xX) -> in(w1,xY))) & (all w1 (in(w1,xY) -> in(w1,xX))))).

end_of_list.