1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
|
begin_problem(Pelletier54).
list_of_descriptions.
name({*Pelletier's Problem No. 54*}).
author({*Christoph Weidenbach*}).
status(unsatisfiable).
description({*Problem taken in revised form from the "Pelletier Collection", Journal of Automated
Reasoning, Vol. 2, No. 2, pages 191-216*}).
end_of_list.
list_of_symbols.
predicates[(F,2)].
end_of_list.
list_of_formulae(axioms).
formula(forall([U],exists([V],forall([W],equiv(F(W,V),equal(W,U)))))).
end_of_list.
list_of_formulae(conjectures).
formula(not(exists([U],forall([V],equiv(F(V,U),forall([W],implies(F(V,W),exists([X],and(F(X,W),not(exists([Y],and(F(Y,W),F(Y,X))))))))))))).
end_of_list.
end_problem.
|
