begin_problem(example1).
list_of_descriptions.
name({*Ground transitivity instance*}).
author({* Somebody *}).
status(unsatisfiable).
description({* example *}).
end_of_list.

list_of_symbols.
  functions[(a,0), (b,0), (c,0)].
  predicates[(equals,2)]. 
end_of_list.

list_of_formulae(axioms).
formula(equals(b,a)).
formula(equals(b,c)).
formula(forall([X], equals(X,X))).
formula(forall([X,Y], implies(equals(X,Y), equals(Y,X)))).
formula(forall([X,Y,Z], implies(and(equals(X,Y), equals(Y,Z)), equals(X,Z)))).
end_of_list.

list_of_formulae(conjectures).
formula(equals(a,c)).
end_of_list.

list_of_settings(SPASS).
{*
set_flag(Auto,0).
set_flag(ISRe,1).
set_flag(ISFc,1).
  set_flag(DocProof,1).
*}
end_of_list.


end_problem.