-
Notifications
You must be signed in to change notification settings - Fork 35
/
codi_down_sum.all.tptp
56 lines (56 loc) · 5.94 KB
/
codi_down_sum.all.tptp
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
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
fof(axiom10, axiom, (! [X] : ! [Y] : (sum(X,Y)=sum(Y,X)))).
fof(axiom20, axiom, (! [X] : ! [Y] : ((~(lt(X,Y)) | Y=sum(X,Y))))).
fof(axiom30, axiom, (! [X] : ! [Y] : ! [Z] : ((~(leq(X,Y) & cont(Z,Y)) | cont(Z,sum(X,Y)))))).
fof(axiom40, axiom, (! [X] : ! [Y] : ! [Z] : ((~(cont(Z,sum(X,Y)) & ~(cont(Z,X))) | cont(difference(Z,X),Y))))).
fof(axiom50, axiom, (! [X] : ! [Y] : ((zex(difference(X,Y)) | eqdim(X,difference(X,Y)))))).
fof(axiom60, axiom, (! [X] : ! [Y] : ((~(lt(Y,X)) | X=difference(X,Y))))).
fof(axiom70, axiom, (! [X] : ! [Y] : ! [Z] : ((~(leq(X,Y) & cont(Z,X) & lt(intersection(Z,Y),Z)) | cont(Z,difference(X,Y)))))).
fof(axiom80, axiom, (! [X] : ! [Y] : ! [Z] : ((~(leq(X,Y) & cont(Z,difference(X,Y))) | cont(Z,X))))).
fof(axiom90, axiom, (! [X] : ! [Y] : ! [Z] : ((~(leq(X,Y) & p(Z,difference(X,Y))) | lt(intersection(Z,Y),Z))))).
fof(axiom100, axiom, (! [X] : ! [Y] : (((~(zex(difference(X,Y))) | zex(X) | cont(X,Y)) & (~(zex(X) | cont(X,Y)) | zex(difference(X,Y))))))).
fof(axiom680, axiom, (! [X] : ! [Y] : ((~(~(zex(X)) & (! [Z] : ((~(po(X,Z)) | po(Y,Z))))) | p(X,Y))))).
fof(axiom690, axiom, (! [X] : ! [Y] : ((~(! [Z] : (((~(po(X,Z)) | po(Y,Z)) & (~(po(Y,Z)) | po(X,Z))))) | X=Y)))).
fof(axiom700, axiom, (! [X] : ! [Y] : ((~(~(zex(X)) & ~(zex(Y)) & ~(cont(Y,X))) | (? [Z] : ((p(Z,Y) & lt(intersection(Z,X),Z)))))))).
fof(axiom3390, axiom, (! [X] : ! [Y] : ! [Z] : ((~(p(Y,X) & min(Z) & cont(Z,X)) | cont(Z,Y) | cont(Z,difference(X,Y)))))).
fof(axiom4030, axiom, (! [X] : (((~(max(X)) | (~(zex(X)) & (! [Y] : (~(pp(X,Y)))))) & (~(~(zex(X)) & (! [Y] : (~(pp(X,Y))))) | max(X)))))).
fof(axiom4040, axiom, (! [X] : (((~(min(X)) | (~(zex(X)) & (! [Y] : (~(pp(Y,X)))))) & (~(~(zex(X)) & (! [Y] : (~(pp(Y,X))))) | min(X)))))).
fof(axiom4050, axiom, (! [X] : ! [Y] : (((~(pp(X,Y)) | (p(X,Y) & ~(X=Y))) & (~(p(X,Y) & ~(X=Y)) | pp(X,Y)))))).
fof(axiom4060, axiom, (! [X] : ! [Y] : (((~(p(X,Y)) | (cont(X,Y) & eqdim(X,Y))) & (~(cont(X,Y) & eqdim(X,Y)) | p(X,Y)))))).
fof(axiom4070, axiom, (! [X] : ! [Y] : ((~(cont(X,Y)) | lt(X,Y) | eqdim(X,Y))))).
fof(axiom4080, axiom, (! [X] : (((zex(X) | cont(X,X)) & (~(cont(X,X)) | ~(zex(X))))))).
fof(axiom4090, axiom, (! [X] : ! [Y] : ((~(cont(X,Y) & cont(Y,X)) | X=Y)))).
fof(axiom4100, axiom, (! [X] : ! [Y] : ! [Z] : ((~(cont(X,Y) & cont(Y,Z)) | cont(X,Z))))).
fof(axiom4110, axiom, (! [X] : ! [Y] : ((~(zex(X)) | (~(cont(Y,X)) & ~(cont(X,Y))))))).
fof(axiom4120, axiom, (! [X] : ! [Y] : ((~(zex(X) & zex(Y)) | X=Y)))).
fof(axiom4130, axiom, (! [X] : ! [Y] : (((~(c(X,Y)) | (? [Z] : ((cont(Z,X) & cont(Z,Y))))) & (~(? [Z] : ((cont(Z,X) & cont(Z,Y)))) | c(X,Y)))))).
fof(axiom4190, axiom, (? [X] : (mindim(X)))).
fof(axiom4320, axiom, (! [X] : (leq(X,X)))).
fof(axiom4330, axiom, (! [X] : ! [Y] : ((leq(X,Y) | leq(Y,X))))).
fof(axiom4340, axiom, (! [X] : ! [Y] : ! [Z] : ((~(leq(X,Y) & leq(Y,Z)) | leq(X,Z))))).
fof(axiom4350, axiom, (! [X] : ! [Y] : ((~(zex(X) & zex(Y)) | X=Y)))).
fof(axiom4360, axiom, (! [X] : ! [Y] : ((~(zex(X)) | leq(X,Y))))).
fof(axiom4370, axiom, (! [X] : (((~(maxdim(X)) | (~(zex(X)) & (! [Y] : (leq(Y,X))))) & (~(~(zex(X)) & (! [Y] : (leq(Y,X)))) | maxdim(X)))))).
fof(axiom4380, axiom, (! [X] : (((~(mindim(X)) | (~(zex(X)) & (! [Y] : ((zex(Y) | leq(X,Y)))))) & (~(~(zex(X)) & (! [Y] : ((zex(Y) | leq(X,Y))))) | mindim(X)))))).
fof(axiom4440, axiom, (! [X] : ! [Y] : (((~(covers(X,Y)) | (lt(Y,X) & (! [Z] : (~(lt(Y,Z) & lt(Z,X)))))) & (~(lt(Y,X) & (! [Z] : (~(lt(Y,Z) & lt(Z,X))))) | covers(X,Y)))))).
fof(axiom4500, axiom, (! [X] : ! [Y] : (((~(lt(X,Y)) | (leq(X,Y) & ~(leq(Y,X)))) & (~(leq(X,Y) & ~(leq(Y,X))) | lt(X,Y)))))).
fof(axiom4510, axiom, (! [X] : ! [Y] : (((~(gt(X,Y)) | (leq(Y,X) & ~(leq(X,Y)))) & (~(leq(Y,X) & ~(leq(X,Y))) | gt(X,Y)))))).
fof(axiom4520, axiom, (! [X] : ! [Y] : (((~(geq(X,Y)) | leq(Y,X)) & (~(leq(Y,X)) | geq(X,Y)))))).
fof(axiom4530, axiom, (! [X] : ! [Y] : (((~(eqdim(X,Y)) | (leq(X,Y) & leq(Y,X))) & (~(leq(X,Y) & leq(Y,X)) | eqdim(X,Y)))))).
fof(axiom710, axiom, (! [X] : ! [Y] : ((~(~(zex(X)) & ~(zex(Y)) & ~(p(Y,X)) & eqdim(X,Y) & po(X,Y) & ~(pp(Y,X))) | (? [Z] : ((p(Z,Y) & ~(po(Z,X))))))))).
fof(axiom720, axiom, (! [X] : ! [Y] : ((~(~(zex(X)) & ~(zex(Y)) & ~(p(Y,X)) & eqdim(X,Y) & ~(po(X,Y))) | (? [Z] : ((p(Z,Y) & ~(po(Z,X))))))))).
fof(axiom730, axiom, (! [X] : ! [Y] : ((~(~(zex(X)) & ~(zex(Y)) & ~(p(Y,X)) & ~(eqdim(X,Y))) | (? [Z] : ((p(Z,Y) & ~(po(Z,X))))))))).
fof(axiom740, axiom, (! [X] : ! [Y] : ((~(zex(X) & ~(zex(Y)) & ~(p(Y,X)) & ~(eqdim(X,Y))) | (? [Z] : ((p(Z,Y) & ~(po(Z,X))))))))).
fof(axiom750, axiom, (! [X] : ! [Y] : ((~(pp(Y,X)) | (? [Z] : ((p(Z,X) & ~(po(Z,Y))))))))).
fof(axiom1390, axiom, (! [X] : ! [Y] : ((zex(difference(X,Y)) | p(difference(X,Y),X))))).
fof(axiom1400, axiom, (! [X] : ! [Y] : ((~(pp(Y,X) & ~(zex(difference(X,Y))) & p(difference(X,Y),X)) | pp(difference(X,Y),X))))).
fof(axiom1410, axiom, (! [X] : ! [Y] : ((~(pp(Y,X)) | pp(difference(X,Y),X))))).
fof(axiom2050, axiom, (! [X] : ! [Y] : ((~(~(zex(Y)) & ~(zex(difference(X,Y)))) | ~(po(Y,difference(X,Y))))))).
fof(axiom2060, axiom, (! [X] : ! [Y] : (~(po(intersection(X,Y),difference(X,Y)))))).
fof(axiom2070, axiom, (! [X] : ! [Y] : ! [Z] : ((~(p(Z,difference(X,Y))) | p(Z,X))))).
fof(axiom2080, axiom, (! [X] : ! [Y] : ! [Z] : ((~(p(Z,difference(X,Y))) | ~(po(Z,intersection(X,Y))))))).
fof(axiom2090, axiom, (! [X] : ! [Y] : ! [Z] : ((~(p(Z,X) & ~(po(Z,intersection(X,Y)))) | p(Z,difference(X,Y)))))).
fof(axiom110, axiom, (! [X] : ! [Y] : (((c(X,Y) | zex(intersection(X,Y))) & (~(zex(intersection(X,Y))) | ~(c(X,Y))))))).
fof(axiom120, axiom, (! [X] : ! [Y] : ((zex(intersection(X,Y)) | cont(intersection(X,Y),X))))).
fof(axiom130, axiom, (! [X] : ! [Y] : ! [Z] : ((~(cont(Z,X) & cont(Z,Y)) | leq(Z,intersection(X,Y)))))).
fof(axiom140, axiom, (! [X] : ! [Y] : ! [Z] : (((~(cont(Z,X) & cont(Z,Y) & eqdim(Z,intersection(X,Y))) | p(Z,intersection(X,Y))) & (~(p(Z,intersection(X,Y))) | (cont(Z,X) & cont(Z,Y) & eqdim(Z,intersection(X,Y)))))))).
fof(axiom670, axiom, (? [X] : (zex(X)))).