--------------------------SPASS-START----------------------------- Input Problem: 1[0:Inp] || -> RigidObject(Ob1)*. 2[0:Inp] || -> Lt(Ta1,Tb1)*. 3[0:Inp] || equal(Ob1,Ox1)** -> . 4[0:Inp] || RigidObject(U) -> Object(U)*. 5[0:Inp] || RigidHistory(U) -> History(U)*. 6[0:Inp] || -> CContained(Ta1,Ox1,Singleton(Ob1))*. 7[0:Inp] || Lt(U,V)* -> Time(U). 8[0:Inp] || Lt(U,V)* -> Time(V). 9[0:Inp] || Leq(U,V)* -> Time(U). 10[0:Inp] || Leq(U,V)* -> Time(V). 11[0:Inp] || Ordered(U,V)* -> Time(U). 12[0:Inp] || Ordered(U,V)* -> Time(V). 13[0:Inp] || SkP0(U,V)* -> Region(V). 14[0:Inp] || SkP0(U,V)* -> Region(U). 15[0:Inp] || SkP1(U,V)* -> Region(V). 16[0:Inp] || SkP1(U,V)* -> Region(U). 17[0:Inp] || Object(U) -> ObjectSet(Singleton(U))*. 18[0:Inp] || Object(U) -> History(HPlace(U))*. 19[0:Inp] || RigidObject(U) -> RigidHistory(HPlace(U))*. 20[0:Inp] || Leq3(U,V,W)* -> Time(U). 21[0:Inp] || Leq3(U,V,W)* -> Time(V). 22[0:Inp] || Leq3(U,V,W)* -> Time(W). 23[0:Inp] || P(U,V) -> SkP0(V,U)*. 24[0:Inp] || O(U,V) -> SkP0(V,U)*. 25[0:Inp] || EC(U,V) -> SkP0(V,U)*. 26[0:Inp] || DR(U,V) -> SkP0(V,U)*. 27[0:Inp] || Cavity(U,V) -> SkP1(V,U)*. 28[0:Inp] || Outside(U,V) -> SkP1(V,U)*. 29[0:Inp] || OSPlace(U,V,W)* -> Time(U). 30[0:Inp] || OSPlace(U,V,W)* -> ObjectSet(V). 31[0:Inp] || OSPlace(U,V,W)* -> Region(W). 32[0:Inp] || ClosedContainer(U,V,W)* -> Time(U). 33[0:Inp] || ClosedContainer(U,V,W)* -> ObjectSet(V). 34[0:Inp] || ClosedContainer(U,V,W)* -> Region(W). 35[0:Inp] || CContained(U,V,W)* -> Time(U). 36[0:Inp] || CContained(U,V,W)* -> Object(V). 37[0:Inp] || CContained(U,V,W)* -> ObjectSet(W). 38[0:Inp] || CContained(U,V,W)* -> Object(V). 39[0:Inp] || Region(U) Region(V) -> Region(RUnion(U,V))*. 40[0:Inp] || Time(U) Object(V) -> Region(Place(U,V))*. 41[0:Inp] || Time(U) History(V) -> Region(Slice(U,V))*. 42[0:Inp] || ClosedContainer(U,V,W)* -> Cavity(W,skf3(W,X,Y))*. 43[0:Inp] || CContained(U,V,W) -> ClosedContainer(U,W,skf2(V,U,W))*. 44[0:Inp] || ClosedContainer(U,V,W) -> OSPlace(U,V,skf3(W,V,U))*. 45[0:Inp] || Cavity(U,Slice(Ta1,HPlace(Ob1)))* P(Place(Ta1,Ox1),U) -> . 46[0:Inp] || CContained(U,V,W)* -> P(Place(U,V),skf2(V,U,X))*. 47[0:Inp] || OSPlace(U,V,W)* Cavity(X,W)* -> ClosedContainer(U,V,X)*. 48[0:Inp] || Time(U) Object(V) -> equal(Slice(U,HPlace(V)),Place(U,V))**. 49[0:Inp] || OSPlace(U,Singleton(V),W)* Time(U) Object(V) -> equal(Place(U,V),W). 50[0:Inp] || equal(Place(U,V),W) Time(U) Object(V) -> OSPlace(U,Singleton(V),W)*. 51[0:Inp] || ClosedContainer(U,V,W)* P(Place(U,X),W)* Object(X) -> CContained(U,X,V)*. This is a first-order Horn problem containing equality. This is a problem that has, if any, a non-trivial domain model. This is a problem that contains sort information. The following monadic predicates have finite extensions: RigidObject. Axiom clauses: 50 Conjecture clauses: 1 Inferences: IEmS=1 ISoR=1 IEqR=1 ISpR=1 ISpL=1 IORe=1 Reductions: RFRew=1 RBRew=1 RFMRR=1 RBMRR=1 RObv=1 RUnC=1 RTaut=1 RSSi=1 RFSub=1 RBSub=1 RAED=2 RCon=1 Extras : Input Saturation, Dynamic Selection, No Splitting, Full Reduction, Ratio: 5, FuncWeight: 1, VarWeight: 1 Precedence: skf3 > skf2 > skf1 > skf0 > Slice > Place > RUnion > HPlace > Singleton > Region > SkP0 > History > ObjectSet > SkP1 > CContained > ClosedContainer > OSPlace > Cavity > P > Object > Time > Ordered > Lt > Leq > Leq3 > RigidHistory > RigidObject > O > EC > DR > Outside > skc6 > skc5 > skc4 > skc3 > skc2 > skc1 > skc0 > Tb1 > Ta1 > Ob1 > Ox1 Ordering : KBO Processed Problem: Worked Off Clauses: Usable Clauses: 1[0:Inp] || -> RigidObject(Ob1)*. 2[0:Inp] || -> Lt(Ta1,Tb1)*. 3[0:Inp] || equal(Ob1,Ox1)** -> . 6[0:Inp] || -> CContained(Ta1,Ox1,Singleton(Ob1))*. 5[0:Inp] RigidHistory(U) || -> History(U)*. 4[0:Inp] RigidObject(U) || -> Object(U)*. 19[0:Inp] RigidObject(U) || -> RigidHistory(HPlace(U))*. 18[0:Inp] Object(U) || -> History(HPlace(U))*. 17[0:Inp] Object(U) || -> ObjectSet(Singleton(U))*. 16[0:Inp] || SkP1(U,V)* -> Region(U). 15[0:Inp] || SkP1(U,V)* -> Region(V). 14[0:Inp] || SkP0(U,V)* -> Region(U). 13[0:Inp] || SkP0(U,V)* -> Region(V). 12[0:Inp] || Ordered(U,V)* -> Time(V). 11[0:Inp] || Ordered(U,V)* -> Time(U). 10[0:Inp] || Leq(U,V)* -> Time(V). 9[0:Inp] || Leq(U,V)* -> Time(U). 8[0:Inp] || Lt(U,V)* -> Time(V). 7[0:Inp] || Lt(U,V)* -> Time(U). 28[0:Inp] || Outside(U,V) -> SkP1(V,U)*. 27[0:Inp] || Cavity(U,V) -> SkP1(V,U)*. 26[0:Inp] || DR(U,V) -> SkP0(V,U)*. 25[0:Inp] || EC(U,V) -> SkP0(V,U)*. 24[0:Inp] || O(U,V) -> SkP0(V,U)*. 23[0:Inp] || P(U,V) -> SkP0(V,U)*. 37[0:Inp] || CContained(U,V,W)* -> ObjectSet(W). 30[0:Inp] || OSPlace(U,V,W)* -> ObjectSet(V). 33[0:Inp] || ClosedContainer(U,V,W)* -> ObjectSet(V). 38[0:Inp] || CContained(U,V,W)* -> Object(V). 31[0:Inp] || OSPlace(U,V,W)* -> Region(W). 34[0:Inp] || ClosedContainer(U,V,W)* -> Region(W). 22[0:Inp] || Leq3(U,V,W)* -> Time(W). 21[0:Inp] || Leq3(U,V,W)* -> Time(V). 20[0:Inp] || Leq3(U,V,W)* -> Time(U). 35[0:Inp] || CContained(U,V,W)* -> Time(U). 29[0:Inp] || OSPlace(U,V,W)* -> Time(U). 32[0:Inp] || ClosedContainer(U,V,W)* -> Time(U). 39[0:Inp] Region(U) Region(V) || -> Region(RUnion(V,U))*. 41[0:Inp] History(U) Time(V) || -> Region(Slice(V,U))*. 40[0:Inp] Object(U) Time(V) || -> Region(Place(V,U))*. 42[0:Inp] || ClosedContainer(U,V,W)* -> Cavity(W,skf3(W,X,Y))*. 44[0:Inp] || ClosedContainer(U,V,W) -> OSPlace(U,V,skf3(W,V,U))*. 43[0:Inp] || CContained(U,V,W) -> ClosedContainer(U,W,skf2(V,U,W))*. 45[0:Inp] || Cavity(U,Slice(Ta1,HPlace(Ob1)))* P(Place(Ta1,Ox1),U) -> . 46[0:Inp] || CContained(U,V,W)* -> P(Place(U,V),skf2(V,U,X))*. 47[0:Inp] || Cavity(U,V)* OSPlace(W,X,V)* -> ClosedContainer(W,X,U)*. 48[0:Inp] Object(U) Time(V) || -> equal(Slice(V,HPlace(U)),Place(V,U))**. 52[0:MRR:49.0,29.1] Object(U) || OSPlace(V,Singleton(U),W)* -> equal(Place(V,U),W). 50[0:Inp] Object(U) Time(V) || equal(Place(V,U),W) -> OSPlace(V,Singleton(U),W)*. 51[0:Inp] Object(U) || P(Place(V,U),W)* ClosedContainer(V,X,W)* -> CContained(V,U,X)*. Given clause: 1[0:Inp] || -> RigidObject(Ob1)*. Given clause: 2[0:Inp] || -> Lt(Ta1,Tb1)*. Given clause: 3[0:Inp] || equal(Ob1,Ox1)** -> . Given clause: 6[0:Inp] || -> CContained(Ta1,Ox1,Singleton(Ob1))*. Given clause: 5[0:Inp] RigidHistory(U) || -> History(U)*. Given clause: 4[0:Inp] RigidObject(U) || -> Object(U)*. Given clause: 19[0:Inp] RigidObject(U) || -> RigidHistory(HPlace(U))*. Given clause: 18[0:Inp] Object(U) || -> History(HPlace(U))*. Given clause: 17[0:Inp] Object(U) || -> ObjectSet(Singleton(U))*. Given clause: 16[0:Inp] || SkP1(U,V)* -> Region(U). Given clause: 15[0:Inp] || SkP1(U,V)* -> Region(V). Given clause: 14[0:Inp] || SkP0(U,V)* -> Region(U). Given clause: 13[0:Inp] || SkP0(U,V)* -> Region(V). Given clause: 12[0:Inp] || Ordered(U,V)* -> Time(V). Given clause: 11[0:Inp] || Ordered(U,V)* -> Time(U). Given clause: 10[0:Inp] || Leq(U,V)* -> Time(V). Given clause: 9[0:Inp] || Leq(U,V)* -> Time(U). Given clause: 8[0:Inp] || Lt(U,V)* -> Time(V). Given clause: 53[0:Res:2.0,8.0] || -> Time(Tb1)*. Given clause: 7[0:Inp] || Lt(U,V)* -> Time(U). Given clause: 54[0:Res:2.0,7.0] || -> Time(Ta1)*. Given clause: 28[0:Inp] || Outside(U,V) -> SkP1(V,U)*. Given clause: 55[0:Res:28.1,15.0] || Outside(U,V)* -> Region(U). Given clause: 56[0:Res:28.1,16.0] || Outside(U,V)* -> Region(V). Given clause: 27[0:Inp] || Cavity(U,V) -> SkP1(V,U)*. Given clause: 57[0:Res:27.1,15.0] || Cavity(U,V)* -> Region(U). Given clause: 58[0:Res:27.1,16.0] || Cavity(U,V)* -> Region(V). Given clause: 26[0:Inp] || DR(U,V) -> SkP0(V,U)*. Given clause: 59[0:Res:26.1,13.0] || DR(U,V)* -> Region(U). Given clause: 25[0:Inp] || EC(U,V) -> SkP0(V,U)*. Given clause: 60[0:Res:26.1,14.0] || DR(U,V)* -> Region(V). Given clause: 61[0:Res:25.1,13.0] || EC(U,V)* -> Region(U). Given clause: 62[0:Res:25.1,14.0] || EC(U,V)* -> Region(V). Given clause: 24[0:Inp] || O(U,V) -> SkP0(V,U)*. Given clause: 23[0:Inp] || P(U,V) -> SkP0(V,U)*. Given clause: 63[0:Res:24.1,13.0] || O(U,V)* -> Region(U). Given clause: 64[0:Res:24.1,14.0] || O(U,V)* -> Region(V). Given clause: 65[0:Res:23.1,13.0] || P(U,V)* -> Region(U). Given clause: 66[0:Res:23.1,14.0] || P(U,V)* -> Region(V). Given clause: 37[0:Inp] || CContained(U,V,W)* -> ObjectSet(W). Given clause: 67[0:Res:6.0,37.0] || -> ObjectSet(Singleton(Ob1))*. Given clause: 30[0:Inp] || OSPlace(U,V,W)* -> ObjectSet(V). Given clause: 33[0:Inp] || ClosedContainer(U,V,W)* -> ObjectSet(V). Given clause: 38[0:Inp] || CContained(U,V,W)* -> Object(V). Given clause: 31[0:Inp] || OSPlace(U,V,W)* -> Region(W). Given clause: 68[0:Res:6.0,38.0] || -> Object(Ox1)*. Given clause: 34[0:Inp] || ClosedContainer(U,V,W)* -> Region(W). Given clause: 22[0:Inp] || Leq3(U,V,W)* -> Time(W). Given clause: 21[0:Inp] || Leq3(U,V,W)* -> Time(V). Given clause: 20[0:Inp] || Leq3(U,V,W)* -> Time(U). Given clause: 35[0:Inp] || CContained(U,V,W)* -> Time(U). Given clause: 29[0:Inp] || OSPlace(U,V,W)* -> Time(U). Given clause: 32[0:Inp] || ClosedContainer(U,V,W)* -> Time(U). Given clause: 39[0:Inp] Region(U) Region(V) || -> Region(RUnion(V,U))*. Given clause: 41[0:Inp] History(U) Time(V) || -> Region(Slice(V,U))*. Given clause: 40[0:Inp] Object(U) Time(V) || -> Region(Place(V,U))*. Given clause: 42[0:Inp] || ClosedContainer(U,V,W)*+ -> Cavity(W,skf3(W,X,Y))*. Given clause: 44[0:Inp] || ClosedContainer(U,V,W) -> OSPlace(U,V,skf3(W,V,U))*. Given clause: 71[0:Res:44.1,31.0] || ClosedContainer(U,V,W) -> Region(skf3(W,V,U))*. Given clause: 43[0:Inp] || CContained(U,V,W) -> ClosedContainer(U,W,skf2(V,U,W))*. Given clause: 75[0:Res:43.1,34.0] || CContained(U,V,W) -> Region(skf2(V,U,W))*. Given clause: 45[0:Inp] || Cavity(U,Slice(Ta1,HPlace(Ob1)))* P(Place(Ta1,Ox1),U) -> . Given clause: 46[0:Inp] || CContained(U,V,W)*+ -> P(Place(U,V),skf2(V,U,X))*. Given clause: 77[0:Res:6.0,46.0] || -> P(Place(Ta1,Ox1),skf2(Ox1,Ta1,U))*. Given clause: 47[0:Inp] || Cavity(U,V)* OSPlace(W,X,V)*+ -> ClosedContainer(W,X,U)*. Given clause: 79[0:Res:77.0,65.0] || -> Region(Place(Ta1,Ox1))*. Given clause: 78[0:Res:77.0,66.0] || -> Region(skf2(Ox1,Ta1,U))*. Given clause: 48[0:Inp] Object(U) Time(V) || -> equal(Slice(V,HPlace(U)),Place(V,U))**. Given clause: 85[0:SSi:83.1,83.0,54.0,4.1,1.0] || Cavity(U,Place(Ta1,Ob1))* P(Place(Ta1,Ox1),U) -> . Given clause: 52[0:MRR:49.0,29.1] Object(U) || OSPlace(V,Singleton(U),W)* -> equal(Place(V,U),W). Given clause: 80[0:Res:44.1,47.1] || ClosedContainer(U,V,W) Cavity(X,skf3(W,V,U))* -> ClosedContainer(U,V,X). Given clause: 50[0:Inp] Object(U) Time(V) || equal(Place(V,U),W) -> OSPlace(V,Singleton(U),W)*. Given clause: 88[0:Res:50.3,31.0] Object(U) Time(V) || equal(Place(V,U),W)*+ -> Region(W)*. Given clause: 73[0:Res:43.1,42.0] || CContained(U,V,W) -> Cavity(skf2(V,U,W),skf3(skf2(V,U,W),X,Y))*. Given clause: 51[0:Inp] Object(U) || P(Place(V,U),W)*+ ClosedContainer(V,X,W)* -> CContained(V,U,X)*. Given clause: 98[0:SSi:97.0,68.0] || ClosedContainer(Ta1,U,skf2(Ox1,Ta1,V))* -> CContained(Ta1,Ox1,U). Given clause: 94[0:Res:73.1,58.0] || CContained(U,V,W) -> Region(skf3(skf2(V,U,W),X,Y))*. Given clause: 86[0:Res:44.1,52.1] Object(U) || ClosedContainer(V,Singleton(U),W) -> equal(skf3(W,Singleton(U),V),Place(V,U))**. Given clause: 106[0:Obv:101.1] Object(U) || ClosedContainer(V,Singleton(U),W)* -> Region(Place(V,U)). Given clause: 90[0:Res:50.3,47.1] Object(U) Time(V) || equal(Place(V,U),W)*+ Cavity(X,W)* -> ClosedContainer(V,Singleton(U),X)*. Given clause: 109[0:Res:43.1,106.1] Object(U) || CContained(V,W,Singleton(U))* -> Region(Place(V,U)). Given clause: 112[0:SSi:111.0,4.0,1.1] || -> Region(Place(Ta1,Ob1))*. Given clause: 107[0:Obv:100.1] Object(U) || ClosedContainer(V,Singleton(U),W)*+ -> OSPlace(V,Singleton(U),Place(V,U))*. Given clause: 113[0:Res:43.1,107.1] Object(U) || CContained(V,W,Singleton(U))*+ -> OSPlace(V,Singleton(U),Place(V,U))*. Given clause: 110[0:EqR:90.2] Object(U) Time(V) || Cavity(W,Place(V,U)) -> ClosedContainer(V,Singleton(U),W)*. Given clause: 115[0:SSi:114.0,4.0,1.1] || -> OSPlace(Ta1,Singleton(Ob1),Place(Ta1,Ob1))*. Given clause: 129[0:Res:115.0,47.1] || Cavity(U,Place(Ta1,Ob1)) -> ClosedContainer(Ta1,Singleton(Ob1),U)*. Given clause: 131[0:Res:129.1,42.0] || Cavity(U,Place(Ta1,Ob1)) -> Cavity(U,skf3(U,V,W))*. Given clause: 139[0:Res:131.1,58.0] || Cavity(U,Place(Ta1,Ob1)) -> Region(skf3(U,V,W))*. Given clause: 108[0:Obv:105.1] Object(U) || ClosedContainer(V,Singleton(U),W)*+ Cavity(X,Place(V,U)) -> ClosedContainer(V,Singleton(U),X)*. Given clause: 124[0:SSi:120.1,54.0] Object(U) || Cavity(skf2(Ox1,Ta1,V),Place(Ta1,U))* -> CContained(Ta1,Ox1,Singleton(U)). Given clause: 116[0:Res:110.3,42.0] Object(U) Time(V) || Cavity(W,Place(V,U))*+ -> Cavity(W,skf3(W,X,Y))*. Given clause: 125[0:Obv:121.0] Time(U) Object(V) || Cavity(W,Place(U,V))*+ -> OSPlace(U,Singleton(V),Place(U,V))*. Given clause: 138[0:SpR:86.2,131.1] Object(U) || ClosedContainer(V,Singleton(U),W)* Cavity(W,Place(Ta1,Ob1)) -> Cavity(W,Place(V,U)). Given clause: 103[0:SpR:86.2,73.1] Object(U) || ClosedContainer(V,Singleton(U),skf2(W,X,Y))* CContained(X,W,Y) -> Cavity(skf2(W,X,Y),Place(V,U)). Given clause: 155[0:Obv:152.1] Object(U) || CContained(V,W,Singleton(U)) -> Cavity(skf2(W,V,Singleton(U)),Place(V,U))*. Given clause: 162[0:SSi:158.0,4.0,1.1] || CContained(Ta1,U,Singleton(Ob1)) P(Place(Ta1,Ox1),skf2(U,Ta1,Singleton(Ob1)))* -> . SPASS V 3.5 SPASS beiseite: Proof found. Problem: inference1_p1.dfg SPASS derived 94 clauses, backtracked 0 clauses, performed 0 splits and kept 100 clauses. SPASS allocated 52358 KBytes. SPASS spent 0:00:00.03 on the problem. 0:00:00.01 for the input. 0:00:00.01 for the FLOTTER CNF translation. 0:00:00.00 for inferences. 0:00:00.00 for the backtracking. 0:00:00.00 for the reduction. Here is a proof with depth 5, length 27 : 1[0:Inp] || -> RigidObject(Ob1)*. 2[0:Inp] || -> Lt(Ta1,Tb1)*. 4[0:Inp] RigidObject(U) || -> Object(U)*. 6[0:Inp] || -> CContained(Ta1,Ox1,Singleton(Ob1))*. 7[0:Inp] || Lt(U,V)* -> Time(U). 29[0:Inp] || OSPlace(U,V,W)* -> Time(U). 42[0:Inp] || ClosedContainer(U,V,W)*+ -> Cavity(W,skf3(W,X,Y))*. 43[0:Inp] || CContained(U,V,W) -> ClosedContainer(U,W,skf2(V,U,W))*. 44[0:Inp] || ClosedContainer(U,V,W) -> OSPlace(U,V,skf3(W,V,U))*. 45[0:Inp] || Cavity(U,Slice(Ta1,HPlace(Ob1)))* P(Place(Ta1,Ox1),U) -> . 46[0:Inp] || CContained(U,V,W)*+ -> P(Place(U,V),skf2(V,U,X))*. 48[0:Inp] Object(U) Time(V) || -> equal(Slice(V,HPlace(U)),Place(V,U))**. 49[0:Inp] Time(U) Object(V) || OSPlace(U,Singleton(V),W)* -> equal(Place(U,V),W). 52[0:MRR:49.0,29.1] Object(U) || OSPlace(V,Singleton(U),W)* -> equal(Place(V,U),W). 54[0:Res:2.0,7.0] || -> Time(Ta1)*. 73[0:Res:43.1,42.0] || CContained(U,V,W) -> Cavity(skf2(V,U,W),skf3(skf2(V,U,W),X,Y))*. 77[0:Res:6.0,46.0] || -> P(Place(Ta1,Ox1),skf2(Ox1,Ta1,U))*. 83[0:SpL:48.2,45.0] Object(Ob1) Time(Ta1) || Cavity(U,Place(Ta1,Ob1))* P(Place(Ta1,Ox1),U) -> . 85[0:SSi:83.1,83.0,54.0,4.1,1.0] || Cavity(U,Place(Ta1,Ob1))* P(Place(Ta1,Ox1),U) -> . 86[0:Res:44.1,52.1] Object(U) || ClosedContainer(V,Singleton(U),W) -> equal(skf3(W,Singleton(U),V),Place(V,U))**. 103[0:SpR:86.2,73.1] Object(U) || ClosedContainer(V,Singleton(U),skf2(W,X,Y))* CContained(X,W,Y) -> Cavity(skf2(W,X,Y),Place(V,U)). 152[0:Res:43.1,103.1] Object(U) || CContained(V,W,Singleton(U)) CContained(V,W,Singleton(U)) -> Cavity(skf2(W,V,Singleton(U)),Place(V,U))*. 155[0:Obv:152.1] Object(U) || CContained(V,W,Singleton(U)) -> Cavity(skf2(W,V,Singleton(U)),Place(V,U))*. 158[0:Res:155.2,85.0] Object(Ob1) || CContained(Ta1,U,Singleton(Ob1)) P(Place(Ta1,Ox1),skf2(U,Ta1,Singleton(Ob1)))* -> . 162[0:SSi:158.0,4.0,1.1] || CContained(Ta1,U,Singleton(Ob1)) P(Place(Ta1,Ox1),skf2(U,Ta1,Singleton(Ob1)))* -> . 165[0:Res:77.0,162.1] || CContained(Ta1,Ox1,Singleton(Ob1))* -> . 166[0:MRR:165.0,6.0] || -> . Formulae used in the proof : axiom16 axiom18 axiom14 axiom17 axiom0 axiom9 axiom22 axiom21 conjecture0 axiom23 axiom24 --------------------------SPASS-STOP------------------------------