/
voids_extended.all.tptp
168 lines (168 loc) · 18.1 KB
/
voids_extended.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
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
% cl-imports multidim_space_codi/codi_basic.clif
% cl-imports multidim_space_codi/definitions/epp.clif
fof(sos10,axiom,( ! [X12] : ( (max(X12)) <=> ((s(X12) & ~ (zex(X12)) & ( ! [X11] : ~ (pp(X12, X11))) )) )) ).
fof(sos20,axiom,( ! [X22] : ( (min(X22)) <=> ((s(X22) & ~ (zex(X22)) & ( ! [X21] : ~ (pp(X21, X22))) )) )) ).
% cl-imports multidim_space_dim/dim_prime_linear_unbounded.clif
% cl-imports multidim_space_dim/definitions/dim_basic_defs.clif
fof(sos30,axiom,( ! [X32] : ! [X31] : ( (covers(X32, X31)) <=> ((lt(X31, X32) & ( ! [X33] : ( (s(X33)) => (~ ((lt(X31, X33) & lt(X33, X32)))) )) )) )) ).
% cl-imports multidim_space_space/space.clif
fof(sos40,axiom,( ! [X41] : s(ch(X41))) ).
fof(sos50,axiom,( ! [X51] : (ch(X51)=ch(r(X51)))) ).
fof(sos60,axiom,( ! [X61] : ( (~ (zex(X61))) => (icon(ch(X61))) )) ).
fof(sos70,axiom,( ! [X71] : (ch(X71)=ch(ch(X71)))) ).
fof(sos80,axiom,( ! [X81] : ( (~ (zex(X81))) => (cont(r(X81), ch(X81))) )) ).
fof(sos90,axiom,( ! [X91] : ( ((~ (zex(X91)) & ~ (closed(r(X91))))) => (tcont(r(X91), ch(X91))) )) ).
fof(sos100,axiom,( ! [X102] : ! [X101] : ( (cont(r(X102), r(X101))) => (cont(ch(X102), ch(X101))) )) ).
fof(sos110,axiom,( ! [X112] : ! [X111] : ( (((ch(X112)=ch(X111)) & ~ (zex(X112)))) => (c(r(X112), r(X111))) )) ).
fof(sos120,axiom,( ! [X122] : ! [X121] : ( ((maxdim(r(X122)) & maxdim(r(X121)) & (r(X122)=ch(X122)) & (r(X121)=ch(X121)))) => ((intersection(ch(X122), ch(X121))=ch(intersection(ch(X122), ch(X121))))) )) ).
fof(sos130,axiom,( ! [X132] : ! [X131] : ( ((icont(r(X132), r(X131)) & ~ (closed(difference(r(X131), r(X132)))))) => (~ ((difference(r(X131), r(X132))=ch(difference(r(X131), r(X132)))))) )) ).
fof(sos140,axiom,( ! [X142] : ! [X141] : ( ((icont(r(X142), r(X141)) & maxdim(r(X142)) & maxdim(r(X141)))) => (cont(r(X142), ch(difference(r(X141), r(X142))))) )) ).
fof(sos150,axiom,( ! [X152] : ! [X151] : ( ((~ (zex(X152)) | ~ (zex(X151)))) => (( ? [X153] : ? [X154] : (tsum(r(X152), r(X151), r(X153)) & tsum(ch(X152), ch(X151), r(X154)) & cont(X154, ch(X153)))) ) )) ).
fof(sos160,axiom,( ! [X162] : ! [X161] : ! [X163] : ! [X165] : ! [X164] : ( ((eqdim(X162, X161) & eqdim(X161, X163) & sc(X162, X161) & sc(X161, X163) & ~ (c(X162, X163)) & tsum(X162, X161, X165) & tsum(X161, X163, X164) & (X165=ch(X165)) & (X164=ch(X164)))) => ((X161=ch(X161))) )) ).
% cl-imports multidim_space_dim/definitions/eq_dim.clif
fof(sos170,axiom,( ! [X172] : ! [X171] : ( (gt(X172, X171)) <=> (lt(X171, X172)) )) ).
fof(sos180,axiom,( ! [X182] : ! [X181] : ( (geq(X182, X181)) <=> (leq(X181, X182)) )) ).
fof(sos190,axiom,( ! [X192] : ! [X191] : ( (lt(X192, X191)) <=> ((leq(X192, X191) & ~ (eqdim(X192, X191)))) )) ).
% cl-imports multidim_space_codi/codi_basic.clif
% cl-imports multidim_space_codi/definitions/ep.clif
fof(sos200,axiom,( ! [X202] : ! [X201] : ( (pp(X202, X201)) <=> ((p(X202, X201) & ~ ((X202=X201)))) )) ).
% cl-imports multidim_space_spch/spch.clif
fof(sos210,axiom,( ! [X212] : ! [X211] : ( (vs(X212, X211)) <=> ((ped(X212) & s(X211) & cont(X211, ch(X212)) & ~ (po(X211, r(X212))))) )) ).
fof(sos220,axiom,( ! [X222] : ! [X221] : ( (simplev(X221)) <=> ((icon(r(X221)) & ( ? [X222] : hostsv(X222, X221)) )) )) ).
fof(sos230,axiom,( ! [X232] : ! [X231] : ( (complexv(X231)) <=> ((~ (icon(r(X231))) & ( ? [X232] : hostsv(X232, X231)) )) )) ).
fof(sos240,axiom,( ! [X241] : ( (v(X241)) <=> ((simplev(X241) | complexv(X241))) )) ).
fof(sos250,axiom,( ! [X252] : ! [X251] : ( (hostsv(X252, X251)) => ((hosts(X252, X251) & vs(X252, r(X251)) & strongc(r(X252), r(X251)))) )) ).
fof(sos260,axiom,( ! [X262] : ! [X261] : ! [X263] : ( ((hostsv(X262, X261) & complexv(X261) & po(r(X263), r(X261)))) => (( ? [X264] : (hostsv(X262, X264) & simplev(X264) & po(r(X263), r(X264)))) ) )) ).
fof(sos270,axiom,( ! [X272] : ! [X271] : ( ((hosts(X272, X271) & v(X271))) => (~ (v(X272))) )) ).
fof(sos280,axiom,( ! [X282] : ! [X281] : ( ((hostsv(X282, X281) & rpf(X282))) => (( ? [X283] : (hosts(X283, X282) & ~ (f(X283)) & hostsv(X283, X281))) ) )) ).
fof(sos290,axiom,( ! [X292] : ! [X291] : ( ((hostsv(X292, X291) & ~ (f(X292)))) => (( ? [X293] : (hosts(X292, X293) & rpf(X293) & hostsv(X293, X291))) ) )) ).
fof(sos300,axiom,( ! [X302] : ! [X301] : ! [X303] : ( ((hostsv(X302, X301) & hostsv(X302, X303) & po(r(X301), r(X303)))) => ((cont(r(X301), r(X303)) | cont(r(X303), r(X301)))) )) ).
fof(sos310,axiom,( ! [X312] : ! [X311] : ! [X314] : ( ((hostsv(X312, X311) & p(r(X312), r(X311)) & ped(X311) & ~ (dpf(X311)) & ~ (cont(r(X314), r(X311))))) => (( ? [X313] : (cont(difference(r(X314), r(X311)), r(X313)) & hostsv(X311, X313))) ) )) ).
fof(sos320,axiom,( ! [X322] : ! [X321] : ! [X324] : ( ((hostsv(X322, X324) & p(r(X321), r(X322)) & ped(X321) & ~ (dpf(X321)) & po(r(X324), ch(X321)))) => (( ? [X323] : ((r(X323)=intersection(r(X324), ch(X321))) & hostsv(X321, X323))) ) )) ).
% cl-imports multidim_space_cont/cont_basic.clif
% cl-imports multidim_space_dim/dim_prime_linear.clif
fof(sos330,axiom,( ! [X332] : ! [X331] : ( (cont(X332, X331)) => ((lt(X332, X331) | eqdim(X332, X331))) )) ).
% cl-imports multidim_space_voids/voids.clif
fof(sos340,axiom,( ! [X342] : ! [X341] : ( (hostsh(X342, X341)) <=> ((hostsv(X342, X341) & icon(r(X342)))) )) ).
fof(sos350,axiom,( ! [X352] : ! [X351] : ( (hostsg(X352, X351)) <=> ((hostsv(X352, X351) & ~ (icon(r(X352))))) )) ).
fof(sos360,axiom,( ! [X361] : ( (hole(X361)) <=> (( ? [X362] : hostsh(X362, X361)) ) )) ).
fof(sos370,axiom,( ! [X371] : ( (gap(X371)) <=> (( ? [X372] : hostsg(X372, X371)) ) )) ).
fof(sos380,axiom,( ! [X381] : ! [X382] : ( (hostsv(X381, X382)) => ((op(X381, X382)=intersection(r(X382), difference(cuni, sum(r(X381), r(X382)))))) )) ).
fof(sos390,axiom,( ! [X392] : ! [X391] : ( (hostscavity(X392, X391)) <=> ((hostsv(X392, X391) & ~ (covers(r(X392), op(X392, X391))))) )) ).
fof(sos400,axiom,( ! [X401] : ( (cavity(X401)) <=> (( ? [X402] : hostscavity(X402, X401)) ) )) ).
fof(sos410,axiom,( ! [X412] : ! [X411] : ( (hostscavityi(X412, X411)) <=> ((hostscavity(X412, X411) & zex(op(X412, X411)))) )) ).
fof(sos420,axiom,( ! [X422] : ! [X421] : ( (hostscavityt(X422, X421)) <=> ((hostscavity(X422, X421) & ~ (zex(op(X422, X421))))) )) ).
fof(sos430,axiom,( ! [X432] : ! [X431] : ( (hostshollow(X432, X431)) <=> ((hostsv(X432, X431) & covers(r(X432), op(X432, X431)) & icon(op(X432, X431)))) )) ).
fof(sos440,axiom,( ! [X441] : ( (hol(X441)) <=> (( ? [X442] : hostshollow(X442, X441)) ) )) ).
fof(sos450,axiom,( ! [X452] : ! [X451] : ( (hoststunnel(X452, X451)) <=> ((hostsv(X452, X451) & covers(r(X452), op(X452, X451)) & ~ (icon(op(X452, X451))))) )) ).
fof(sos460,axiom,( ! [X461] : ( (tun(X461)) <=> (( ? [X462] : hoststunnel(X462, X461)) ) )) ).
fof(sos470,axiom,( ! [X472] : ! [X471] : ( (hostsve(X472, X471)) <=> ((hostsv(X472, X471) & ( ? [X473] : (p(X473, op(X472, X471)) & ( ! [X474] : ( ((hostsv(X472, X474) & eqdim(intersection(X473, r(X474)), X473))) => ((po(r(X471), r(X474)) & cont(intersection(X473, r(X474)), op(X472, X474)))) )) )) )) )) ).
fof(sos480,axiom,( ! [X482] : ! [X481] : ( (hostsvi(X482, X481)) <=> ((hostsv(X482, X481) & ~ (hostsve(X482, X481)))) )) ).
fof(sos490,axiom,( ! [X494] : ! [X493] : ( (po(X494, porespace(X493))) <=> (( ? [X492] : (dk1(X492, X493) & ( ! [X491] : ( (hostsv(X493, X491)) => (~ (po(X494, r(X491)))) )) & ( ? [X491] : (hostsv(X492, X491) & po(X494, r(X491)))) )) ) )) ).
fof(sos500,axiom,( ! [X503] : ! [X502] : ( (po(X503, voidspace(X502))) <=> ((po(X503, porespace(X502)) | ( ? [X501] : (hostsv(X502, X501) & po(X503, r(X501)))) )) )) ).
fof(sos510,axiom,( ! [X512] : ( (~ (zex(porespace(X512)))) => (( ? [X513] : ? [X511] : ((r(X513)=porespace(X512)) & hostsv(X511, X513) & dk1(X511, X512))) ) )) ).
fof(sos520,axiom,( ! [X522] : ( (~ (zex(voidspace(X522)))) => (( ? [X523] : ? [X521] : ((r(X523)=voidspace(X522)) & hostsv(X521, X523) & dk1(X521, X522))) ) )) ).
fof(sos530,axiom,( ! [X533] : ! [X532] : ( (po(X533, convoidspace(X532))) <=> (( ? [X531] : (po(X533, X531) & icon(X531) & cont(X531, voidspace(X532)) & strongc(X531, difference(cuni, sum(r(X532), voidspace(X532)))))) ) )) ).
fof(sos540,axiom,( ! [X543] : ! [X542] : ( (po(X543, conporespace(X542))) <=> (( ? [X541] : (po(X543, X541) & icon(X541) & cont(X541, porespace(X542)) & strongc(X541, difference(cuni, sum(r(X542), porespace(X542)))))) ) )) ).
% cl-imports multidim_space_ped/ped.clif
% cl-imports multidim_space_codib/codib_updown.clif
% cl-imports multidim_space_codi/definitions/icon.clif
fof(sos550,axiom,( ! [X551] : (~ (ped(X551)) | ~ (s(X551)))) ).
fof(sos560,axiom,( ! [X561] : s(r(X561))) ).
fof(sos570,axiom,( ! [X571] : ( (s(X571)) <=> ((X571=r(X571))) )) ).
fof(sos580,axiom,( ! [X582] : ! [X581] : ( (cont(X582, X581)) => ((s(X582) & s(X581))) )) ).
fof(sos590,axiom,( ! [X592] : ! [X591] : ( (lt(X592, X591)) => ((s(X592) & s(X591))) )) ).
fof(sos600,axiom,( ! [X601] : ( (zex(X601)) => (s(X601)) )) ).
fof(sos610,axiom,( ! [X612] : ! [X611] : ( (bcont(X612, X611)) => ((s(X612) & s(X611))) )) ).
fof(sos620,axiom,( ! [X621] : ( (ped(X621)) => (maxdim(r(X621))) )) ).
fof(sos630,axiom,( ! [X632] : ! [X631] : ( (dk1(X632, X631)) => (p(r(X632), r(X631))) )) ).
fof(sos640,axiom,( ! [X642] : ! [X641] : ( (hosts(X642, X641)) => (( (rpf(X641)) <=> (p(r(X642), r(X641))) )) )) ).
fof(sos650,axiom,( ! [X652] : ! [X651] : ! [X653] : ! [X654] : ( ((hosts(X652, X651) & rpf(X651) & dk1(X653, X652) & dk1(X654, X651))) => (p(r(X654), r(X653))) )) ).
fof(sos660,axiom,( ! [X662] : ! [X661] : ( (hosts(X662, X661)) => (( (dpf(X661)) <=> (~ (po(r(X662), r(X661)))) )) )) ).
% cl-imports multidim_space_codi/codi_basic.clif
% cl-imports multidim_space_codi/definitions/ep.clif
fof(sos670,axiom,( ! [X672] : ! [X671] : ( (po(X672, X671)) <=> (( ? [X673] : (p(X673, X672) & p(X673, X671))) ) )) ).
fof(sos680,axiom,( ! [X682] : ! [X681] : ( (leq(X682, X681)) => (s(X682)) )) ).
fof(sos690,axiom,( ! [X692] : ! [X691] : ( (leq(X692, X691)) => (s(X691)) )) ).
fof(sos700,axiom,( ! [X701] : ( (zex(X701)) => (s(X701)) )) ).
fof(sos710,axiom,( ! [X711] : ( (s(X711)) => (leq(X711, X711)) )) ).
fof(sos720,axiom,( ! [X722] : ! [X721] : ! [X723] : ( ((leq(X722, X721) & leq(X721, X723))) => (leq(X722, X723)) )) ).
fof(sos730,axiom,( ! [X732] : ! [X731] : ( ((zex(X732) & zex(X731))) => ((X732=X731)) )) ).
fof(sos740,axiom,( ! [X742] : ! [X741] : ( ((zex(X742) & s(X741))) => (leq(X742, X741)) )) ).
% cl-imports multidim_space_codi/codi_down.clif
% cl-imports multidim_space_codi/definitions/epp.clif
% cl-imports multidim_space_codi/definitions/sc.clif
fof(sos750,axiom,( ! [X752] : ( (con(X752)) <=> ((s(X752) & ( ! [X751] : ( (pp(X751, X752)) => (sc(X751, difference(X752, X751))) )) )) )) ).
% cl-imports multidim_space_cont/cont_basic.clif
fof(sos760,axiom,( ! [X762] : ! [X761] : ( (c(X762, X761)) <=> (( ? [X763] : (cont(X763, X762) & cont(X763, X761))) ) )) ).
% cl-imports multidim_space_codi/codi_basic.clif
fof(sos770,axiom,( ! [X772] : ! [X771] : ( (sc(X772, X771)) <=> ((( ? [X773] : (cont(X773, X772) & cont(X773, X771))) & ( ! [X773] : ( ((cont(X773, X772) & cont(X773, X771))) => ((lt(X773, X772) & lt(X773, X771))) )) )) )) ).
% cl-imports multidim_space_codi/codi_basic.clif
% cl-imports multidim_space_codi/definitions/ep.clif
fof(sos780,axiom,( ! [X782] : ! [X781] : ( (inc(X782, X781)) <=> ((( ? [X783] : (lt(X783, X782) & cont(X783, X782) & p(X783, X781))) | ( ? [X783] : (lt(X783, X781) & cont(X783, X781) & p(X783, X782))) )) )) ).
% cl-imports multidim_space_dim/dim_prime_linear_unbounded.clif
% cl-imports multidim_space_dim/definitions/dim_basic_defs.clif
fof(sos790,axiom,( ! [X792] : ( (maxdim(X792)) <=> ((s(X792) & ~ (( ? [X791] : (s(X791) & lt(X792, X791))) ))) )) ).
fof(sos800,axiom,( ! [X802] : ( (mindim(X802)) <=> ((s(X802) & ~ (zex(X802)) & ( ! [X801] : ( ((s(X801) & lt(X801, X802))) => (zex(X801)) )) )) )) ).
% cl-imports multidim_space_dim/dim_prime_linear_unbounded.clif
% cl-imports multidim_space_dim/definitions/min_max_dim.clif
fof(sos810,axiom,( ? [X811] : mindim(X811)) ).
% cl-imports multidim_space_dim/dim_prime_linear_unbounded.clif
fof(sos820,axiom,( ! [X822] : ! [X821] : ( (eqdim(X822, X821)) <=> ((leq(X822, X821) & leq(X821, X822))) )) ).
% cl-imports multidim_space_codi/codi_down.clif
% cl-imports multidim_space_codi/definitions/min_max_in_dim.clif
% cl-imports multidim_space_codi/definitions/connected.clif
% cl-imports multidim_space_codi/definitions/epp.clif
% cl-imports multidim_space_codi/definitions/sc.clif
% cl-imports multidim_space_dim/definitions/covers.clif
fof(sos830,axiom,( ! [X832] : ( (icon(X832)) <=> ((con(X832) & ( ! [X831] : ( (pp(X831, X832)) => (covers(X832, intersection(X831, difference(X832, X831)))) )) )) )) ).
fof(sos840,axiom,( ! [X842] : ( (ucon(X842)) <=> ((con(X842) & ( ! [X841] : ! [X843] : ( ((pp(X841, X842) & cont(X843, X841) & cont(X843, difference(X842, X841)))) => (cont(X843, intersection(X841, difference(X842, X841)))) )) )) )) ).
fof(sos850,axiom,( ! [X852] : ! [X851] : ( (strongc(X852, X851)) <=> ((sc(X852, X851) & eqdim(X852, X851) & covers(X852, intersection(X852, X851)))) )) ).
fof(sos860,axiom,( ! [X862] : ! [X861] : ! [X863] : ! [X864] : ( ((tsum(X862, X861, X863) & tsum(X862, X861, X864))) => ((s(X862) & s(X861) & s(X863) & (X864=X863))) )) ).
fof(sos870,axiom,( ! [X872] : ! [X871] : ! [X873] : ( (tsum(X872, X871, X873)) => (tsum(X871, X872, X873)) )) ).
fof(sos880,axiom,( ! [X882] : ! [X881] : ( (lt(X882, X881)) => (tsum(X882, X881, X881)) )) ).
fof(sos890,axiom,( ! [X892] : ! [X891] : ! [X893] : ! [X894] : ( ((tsum(X892, X891, X893) & leq(X892, X891) & cont(X894, X891))) => (cont(X894, X893)) )) ).
fof(sos900,axiom,( ! [X902] : ! [X901] : ! [X903] : ! [X904] : ( ((tsum(X902, X901, X903) & cont(X904, X903) & ~ (cont(X904, X902)))) => (cont(difference(X904, X902), X901)) )) ).
fof(sos910,axiom,( ! [X912] : ! [X911] : ! [X913] : ( ((s(X913) & eqdim(X912, X911) & ( ! [X914] : ( (po(X914, X913)) <=> ((po(X914, X912) | po(X914, X911))) )) )) => (tsum(X912, X911, X913)) )) ).
fof(sos920,axiom,( ! [X922] : ! [X921] : ( ((eqdim(X922, X921) & ( ! [X923] : ( ((cont(X923, X922) & cont(X923, X921) & min(X923))) => (( ? [X924] : ? [X925] : (p(X924, X922) & p(X925, X921) & bcont(X923, X924) & bcont(X923, X925))) ) )) )) => (( ? [X923] : tsum(X922, X921, X923)) ) )) ).
fof(sos930,axiom,( ! [X931] : ( ((s(X931) & ~ (zex(X931)))) => (cont(X931, cuni)) )) ).
% cl-imports multidim_space_codi/codi_basic.clif
fof(sos940,axiom,( ! [X942] : ! [X941] : ( (p(X942, X941)) <=> ((cont(X942, X941) & eqdim(X942, X941))) )) ).
fof(sos950,axiom,( ! [X951] : ( (ped(X951)) => ((pob(X951) | m(X951) | f(X951))) )) ).
fof(sos960,axiom,( ! [X961] : ( (pob(X961)) => (ped(X961)) )) ).
fof(sos970,axiom,( ! [X971] : ( (m(X971)) => (ped(X971)) )) ).
fof(sos980,axiom,( ! [X981] : ( (f(X981)) => (ped(X981)) )) ).
fof(sos990,axiom,( ! [X991] : ( (pob(X991)) => (~ (m(X991))) )) ).
fof(sos1000,axiom,( ! [X1001] : ( (pob(X1001)) => (~ (f(X1001))) )) ).
fof(sos1010,axiom,( ! [X1011] : ( (m(X1011)) => (~ (f(X1011))) )) ).
fof(sos1020,axiom,( ! [X1021] : ( (napo(X1021)) => (pob(X1021)) )) ).
fof(sos1030,axiom,( ! [X1032] : ! [X1031] : ( (hosts(X1032, X1031)) => ((ped(X1032) & f(X1031))) )) ).
fof(sos1040,axiom,( ! [X1042] : ( (f(X1042)) <=> (( ? [X1041] : hosts(X1041, X1042)) ) )) ).
fof(sos1050,axiom,( ! [X1052] : ! [X1051] : ( (hosts(X1052, X1051)) => (~ (hosts(X1051, X1052))) )) ).
fof(sos1060,axiom,( ! [X1061] : ( (f(X1061)) <=> ((rpf(X1061) | dpf(X1061))) )) ).
fof(sos1070,axiom,( ! [X1071] : (~ (rpf(X1071)) | ~ (dpf(X1071)))) ).
fof(sos1080,axiom,( ! [X1082] : ! [X1081] : ( (dk1(X1082, X1081)) => (m(X1082)) )) ).
fof(sos1090,axiom,( ! [X1092] : ! [X1091] : ( (dk1(X1092, X1091)) => ((pob(X1091) | rpf(X1091))) )) ).
fof(sos1100,axiom,( ! [X1102] : ! [X1101] : ! [X1103] : ( ((dk1(X1102, X1101) & dk1(X1103, X1101))) => ((X1102=X1103)) )) ).
fof(sos1110,axiom,( ! [X1111] : ( ((pob(X1111) | rpf(X1111))) => (( ? [X1112] : dk1(X1112, X1111)) ) )) ).
fof(sos1120,axiom,( ! [X1121] : ( ((s(X1121) & ~ (zex(X1121)))) <=> (cont(X1121, X1121)) )) ).
fof(sos1130,axiom,( ! [X1132] : ! [X1131] : ( ((cont(X1132, X1131) & cont(X1131, X1132))) => ((X1132=X1131)) )) ).
fof(sos1140,axiom,( ! [X1142] : ! [X1141] : ! [X1143] : ( ((cont(X1142, X1141) & cont(X1141, X1143))) => (cont(X1142, X1143)) )) ).
fof(sos1150,axiom,( ! [X1152] : ! [X1151] : ( (zex(X1152)) => ((s(X1152) & ~ (cont(X1151, X1152)) & ~ (cont(X1152, X1151)))) )) ).
fof(sos1160,axiom,( ! [X1162] : ! [X1161] : ( ((zex(X1162) & zex(X1161))) => ((X1162=X1161)) )) ).
% cl-imports multidim_space_codi/codi_basic.clif
% cl-imports multidim_space_cont/definitions/c.clif
% cl-imports multidim_space_codi/definitions/po.clif
% cl-imports multidim_space_codi/definitions/inc.clif
% cl-imports multidim_space_codi/definitions/sc.clif
% cl-imports multidim_space_codi/definitions/min_max_in_dim.clif
fof(sos1170,axiom,( ! [X1172] : ! [X1171] : ( ((s(X1172) & s(X1171) & ~ (c(X1172, X1171)))) <=> (zex(intersection(X1172, X1171))) )) ).
fof(sos1180,axiom,( ! [X1182] : ! [X1181] : ( ((s(X1182) & s(X1181) & ~ (zex(intersection(X1182, X1181))))) => (cont(intersection(X1182, X1181), X1182)) )) ).
fof(sos1190,axiom,( ! [X1192] : ! [X1191] : ! [X1193] : ( ((cont(X1193, X1192) & cont(X1193, X1191))) => (leq(X1193, intersection(X1192, X1191))) )) ).
fof(sos1200,axiom,( ! [X1202] : ! [X1201] : ! [X1203] : ( ((cont(X1203, X1202) & cont(X1203, X1201) & eqdim(X1203, intersection(X1202, X1201)))) <=> (p(X1203, intersection(X1202, X1201))) )) ).
fof(sos1210,axiom,( ! [X1212] : ! [X1211] : ( ((s(X1212) & s(X1211) & ~ (zex(difference(X1212, X1211))))) => (eqdim(X1212, difference(X1212, X1211))) )) ).
fof(sos1220,axiom,( ! [X1222] : ! [X1221] : ( (lt(X1221, X1222)) => ((X1222=difference(X1222, X1221))) )) ).
fof(sos1230,axiom,( ! [X1232] : ! [X1231] : ! [X1233] : ( ((leq(X1232, X1231) & cont(X1233, X1232) & lt(intersection(X1233, X1231), X1233))) => (cont(X1233, difference(X1232, X1231))) )) ).
fof(sos1240,axiom,( ! [X1242] : ! [X1241] : ! [X1243] : ( ((leq(X1242, X1241) & cont(X1243, difference(X1242, X1241)))) => (cont(X1243, X1242)) )) ).
fof(sos1250,axiom,( ! [X1252] : ! [X1251] : ! [X1253] : ( ((leq(X1252, X1251) & p(X1253, difference(X1252, X1251)))) => (lt(intersection(X1253, X1251), X1253)) )) ).
fof(sos1260,axiom,( ! [X1262] : ! [X1261] : ( (zex(difference(X1262, X1261))) <=> ((zex(X1262) | cont(X1262, X1261))) )) ).