SPASS test

begin_problem(Pelletier54).

list_of_descriptions.
name({*Test*}).
author({*michalk93*}).
status(unsatisfiable).
description({*Test FOL knowledgebase*}).
end_of_list.

list_of_symbols.
  predicates[(A,0), (B, 0), (C, 0)].
end_of_list.

list_of_formulae(axioms).
formula(forall([X], implies(A, B))).
formula(forall([X], implies(B, not(A)))).
formula(forall([X], implies(B, C))).
formula(forall([X], implies(C, not(B)))).
end_of_list.


list_of_formulae(conjectures).
formula(exists([X], implies(B, A))).
end_of_list.

list_of_settings(SPASS).
{*
set_flag(PGiven,1).
set_flag(DocProof,1).
set_flag(PProblem,0).
*}
end_of_list.

end_problem.