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
28
29
30
|
fof(trivial,conjecture,fx=fx).
------------------
fof(irrelevant,conjecture,fz=fz).
fof(trivial,axiom,![Xx]:Xx=Xx).
------------------
fof(alsotrivial,conjecture,fy=fy).
fof(irrelevant,axiom,![Xz]:Xz=Xz).
fof(trivial,axiom,![Xx]:Xx=Xx).
------------------
fof(alsotrivial,conjecture,fy=fy).
fof(trivial,axiom,![Xx]:Xx=Xx).
------------------
fof(alsotrivial,conjecture,fy=fy).
fof(irrelevant,axiom,![Xz]:Xz=Xz).
fof(trivial,axiom,![Xx]:Xx=Xx).
fof(alsotrivial1,axiom,fy=fy).
------------------
fof(trivial_biconditionals,conjecture,fy=fy).
fof(alsotrivial,axiom,![Xy]:Xy=Xy).
fof(irrelevant,axiom,![Xz]:Xz=Xz).
fof(trivial,axiom,![Xx]:Xx=Xx).
------------------
fof(trivial_biconditionals,conjecture,fy=fy).
fof(trivial,axiom,![Xx]:Xx=Xx).
------------------
fof(trivial_biconditionals,conjecture,fy=fy).
fof(alsotrivial,axiom,![Xy]:Xy=Xy).
fof(irrelevant,axiom,![Xz]:Xz=Xz).
fof(trivial,axiom,![Xx]:Xx=Xx).
fof(trivial_biconditionals1,axiom,fy=fy<=>fy=fy).
|
