File: problem54.dfg

package info (click to toggle)
spass 3.7-2
  • links: PTS
  • area: main
  • in suites: squeeze
  • size: 5,500 kB
  • ctags: 5,981
  • sloc: ansic: 50,634; yacc: 3,038; sh: 1,072; lex: 430; perl: 407; makefile: 394
file content (27 lines) | stat: -rw-r--r-- 669 bytes parent folder | download | duplicates (4) 
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.