begin_problem(Relational_calculus_example).
list_of_descriptions.
  name({* Relational calculus example *}).
  author({* Renate Schmidt *}).
  status(unsatisfiable).
  description({* Demonstrating the syntax of relational formulae *}).
end_of_list.

list_of_symbols.
predicates[(r,0), (s,0)].
end_of_list.

list_of_special_formulae(axioms, EML).

    % r is a subrelation of s
    rel_formula(implies(r,s)).

    % r is transitive
    rel_formula(implies(comp(r,r),r)).

    % r is reflexive
    rel_formula(implies(id,r)).

    % r is symmetric
    rel_formula(implies(r,conv(r))).

end_of_list.

list_of_special_formulae(conjectures, EML).

    % valid 
    rel_formula(implies(id,s)).

    %% not valid 
    %rel_formula(implies(comp(s,s),s)).

end_of_list.

end_problem.