--------------------------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] || ClosedContainer(U,V,W)* -> ObjectSet(V). 40[0:Inp] || ClosedContainer(U,V,W)* -> Time(U). 41[0:Inp] || Region(U) Region(V) -> Region(RUnion(U,V))*. 42[0:Inp] || Time(U) Object(V) -> Region(Place(U,V))*. 43[0:Inp] || Time(U) History(V) -> Region(Slice(U,V))*. 44[0:Inp] || ClosedContainer(U,V,W)* -> Cavity(W,skf3(W,X,Y))*. 45[0:Inp] || CContained(U,V,W) -> ClosedContainer(U,W,skf2(V,U,W))*. 46[0:Inp] || ClosedContainer(U,V,W) -> OSPlace(U,V,skf3(W,V,U))*. 47[0:Inp] || Cavity(U,Slice(Ta1,HPlace(Ob1)))* P(Place(Ta1,Ox1),U) -> . 48[0:Inp] || CContained(U,V,W)* -> P(Place(U,V),skf2(V,U,X))*. 49[0:Inp] || Time(U) Object(V) -> equal(Slice(U,HPlace(V)),Place(U,V))**. 50[0:Inp] || OSPlace(U,Singleton(V),W)* Time(U) Object(V) -> equal(Place(U,V),W). 51[0:Inp] || equal(Place(U,V),W) Time(U) Object(V) -> OSPlace(U,Singleton(V),W)*. 52[0:Inp] || ClosedContainer(U,V,W)* P(Place(U,X),W)* Object(X) -> CContained(U,X,V)*. 53[0:Inp] || OSPlace(U,V,W)* Cavity(X,W)* ObjectSet(V) Time(U) -> ClosedContainer(U,V,X)*. 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: 52 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 > SkP1 > CContained > ClosedContainer > OSPlace > Cavity > P > ObjectSet > 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). 39[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). 40[0:Inp] || ClosedContainer(U,V,W)* -> Time(U). 41[0:Inp] Region(U) Region(V) || -> Region(RUnion(V,U))*. 43[0:Inp] History(U) Time(V) || -> Region(Slice(V,U))*. 42[0:Inp] Object(U) Time(V) || -> Region(Place(V,U))*. 44[0:Inp] || ClosedContainer(U,V,W)* -> Cavity(W,skf3(W,X,Y))*. 46[0:Inp] || ClosedContainer(U,V,W) -> OSPlace(U,V,skf3(W,V,U))*. 45[0:Inp] || CContained(U,V,W) -> ClosedContainer(U,W,skf2(V,U,W))*. 47[0:Inp] || Cavity(U,Slice(Ta1,HPlace(Ob1)))* P(Place(Ta1,Ox1),U) -> . 48[0:Inp] || CContained(U,V,W)* -> P(Place(U,V),skf2(V,U,X))*. 55[0:MRR:53.0,53.1,30.1,29.1] || Cavity(U,V)* OSPlace(W,X,V)* -> ClosedContainer(W,X,U)*. 49[0:Inp] Object(U) Time(V) || -> equal(Slice(V,HPlace(U)),Place(V,U))**. 54[0:MRR:50.0,29.1] Object(U) || OSPlace(V,Singleton(U),W)* -> equal(Place(V,U),W). 51[0:Inp] Object(U) Time(V) || equal(Place(V,U),W) -> OSPlace(V,Singleton(U),W)*. 52[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: 56[0:Res:2.0,8.0] || -> Time(Tb1)*. Given clause: 7[0:Inp] || Lt(U,V)* -> Time(U). Given clause: 57[0:Res:2.0,7.0] || -> Time(Ta1)*. Given clause: 28[0:Inp] || Outside(U,V) -> SkP1(V,U)*. Given clause: 58[0:Res:28.1,15.0] || Outside(U,V)* -> Region(U). Given clause: 59[0:Res:28.1,16.0] || Outside(U,V)* -> Region(V). Given clause: 27[0:Inp] || Cavity(U,V) -> SkP1(V,U)*. Given clause: 60[0:Res:27.1,15.0] || Cavity(U,V)* -> Region(U). Given clause: 61[0:Res:27.1,16.0] || Cavity(U,V)* -> Region(V). Given clause: 26[0:Inp] || DR(U,V) -> SkP0(V,U)*. Given clause: 62[0:Res:26.1,13.0] || DR(U,V)* -> Region(U). Given clause: 25[0:Inp] || EC(U,V) -> SkP0(V,U)*. Given clause: 63[0:Res:26.1,14.0] || DR(U,V)* -> Region(V). Given clause: 64[0:Res:25.1,13.0] || EC(U,V)* -> Region(U). Given clause: 65[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: 66[0:Res:24.1,13.0] || O(U,V)* -> Region(U). Given clause: 67[0:Res:24.1,14.0] || O(U,V)* -> Region(V). Given clause: 68[0:Res:23.1,13.0] || P(U,V)* -> Region(U). Given clause: 69[0:Res:23.1,14.0] || P(U,V)* -> Region(V). Given clause: 37[0:Inp] || CContained(U,V,W)* -> ObjectSet(W). Given clause: 70[0:Res:6.0,37.0] || -> ObjectSet(Singleton(Ob1))*. Given clause: 30[0:Inp] || OSPlace(U,V,W)* -> ObjectSet(V). Given clause: 39[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: 71[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: 40[0:Inp] || ClosedContainer(U,V,W)* -> Time(U). Given clause: 41[0:Inp] Region(U) Region(V) || -> Region(RUnion(V,U))*. Given clause: 43[0:Inp] History(U) Time(V) || -> Region(Slice(V,U))*. Given clause: 42[0:Inp] Object(U) Time(V) || -> Region(Place(V,U))*. Given clause: 44[0:Inp] || ClosedContainer(U,V,W)*+ -> Cavity(W,skf3(W,X,Y))*. Given clause: 46[0:Inp] || ClosedContainer(U,V,W) -> OSPlace(U,V,skf3(W,V,U))*. Given clause: 74[0:Res:46.1,31.0] || ClosedContainer(U,V,W) -> Region(skf3(W,V,U))*. Given clause: 45[0:Inp] || CContained(U,V,W) -> ClosedContainer(U,W,skf2(V,U,W))*. Given clause: 78[0:Res:45.1,34.0] || CContained(U,V,W) -> Region(skf2(V,U,W))*. Given clause: 47[0:Inp] || Cavity(U,Slice(Ta1,HPlace(Ob1)))* P(Place(Ta1,Ox1),U) -> . Given clause: 48[0:Inp] || CContained(U,V,W)*+ -> P(Place(U,V),skf2(V,U,X))*. Given clause: 80[0:Res:6.0,48.0] || -> P(Place(Ta1,Ox1),skf2(Ox1,Ta1,U))*. Given clause: 55[0:MRR:53.0,53.1,30.1,29.1] || Cavity(U,V)* OSPlace(W,X,V)*+ -> ClosedContainer(W,X,U)*. Given clause: 82[0:Res:80.0,68.0] || -> Region(Place(Ta1,Ox1))*. Given clause: 81[0:Res:80.0,69.0] || -> Region(skf2(Ox1,Ta1,U))*. Given clause: 49[0:Inp] Object(U) Time(V) || -> equal(Slice(V,HPlace(U)),Place(V,U))**. Given clause: 88[0:SSi:86.1,86.0,57.0,4.1,1.0] || Cavity(U,Place(Ta1,Ob1))* P(Place(Ta1,Ox1),U) -> . Given clause: 54[0:MRR:50.0,29.1] Object(U) || OSPlace(V,Singleton(U),W)* -> equal(Place(V,U),W). Given clause: 83[0:Res:46.1,55.1] || ClosedContainer(U,V,W) Cavity(X,skf3(W,V,U))* -> ClosedContainer(U,V,X). Given clause: 51[0:Inp] Object(U) Time(V) || equal(Place(V,U),W) -> OSPlace(V,Singleton(U),W)*. Given clause: 91[0:Res:51.3,31.0] Object(U) Time(V) || equal(Place(V,U),W)*+ -> Region(W)*. Given clause: 76[0:Res:45.1,44.0] || CContained(U,V,W) -> Cavity(skf2(V,U,W),skf3(skf2(V,U,W),X,Y))*. Given clause: 52[0:Inp] Object(U) || P(Place(V,U),W)*+ ClosedContainer(V,X,W)* -> CContained(V,U,X)*. Given clause: 101[0:SSi:100.0,71.0] || ClosedContainer(Ta1,U,skf2(Ox1,Ta1,V))* -> CContained(Ta1,Ox1,U). Given clause: 97[0:Res:76.1,61.0] || CContained(U,V,W) -> Region(skf3(skf2(V,U,W),X,Y))*. Given clause: 89[0:Res:46.1,54.1] Object(U) || ClosedContainer(V,Singleton(U),W) -> equal(skf3(W,Singleton(U),V),Place(V,U))**. Given clause: 109[0:Obv:104.1] Object(U) || ClosedContainer(V,Singleton(U),W)* -> Region(Place(V,U)). Given clause: 93[0:Res:51.3,55.1] Object(U) Time(V) || equal(Place(V,U),W)*+ Cavity(X,W)* -> ClosedContainer(V,Singleton(U),X)*. Given clause: 112[0:Res:45.1,109.1] Object(U) || CContained(V,W,Singleton(U))* -> Region(Place(V,U)). Given clause: 115[0:SSi:114.0,4.0,1.1] || -> Region(Place(Ta1,Ob1))*. Given clause: 110[0:Obv:103.1] Object(U) || ClosedContainer(V,Singleton(U),W)*+ -> OSPlace(V,Singleton(U),Place(V,U))*. Given clause: 116[0:Res:45.1,110.1] Object(U) || CContained(V,W,Singleton(U))*+ -> OSPlace(V,Singleton(U),Place(V,U))*. Given clause: 113[0:EqR:93.2] Object(U) Time(V) || Cavity(W,Place(V,U)) -> ClosedContainer(V,Singleton(U),W)*. Given clause: 118[0:SSi:117.0,4.0,1.1] || -> OSPlace(Ta1,Singleton(Ob1),Place(Ta1,Ob1))*. Given clause: 132[0:Res:118.0,55.1] || Cavity(U,Place(Ta1,Ob1)) -> ClosedContainer(Ta1,Singleton(Ob1),U)*. Given clause: 134[0:Res:132.1,44.0] || Cavity(U,Place(Ta1,Ob1)) -> Cavity(U,skf3(U,V,W))*. Given clause: 142[0:Res:134.1,61.0] || Cavity(U,Place(Ta1,Ob1)) -> Region(skf3(U,V,W))*. Given clause: 111[0:Obv:108.1] Object(U) || ClosedContainer(V,Singleton(U),W)*+ Cavity(X,Place(V,U)) -> ClosedContainer(V,Singleton(U),X)*. Given clause: 127[0:SSi:123.1,57.0] Object(U) || Cavity(skf2(Ox1,Ta1,V),Place(Ta1,U))* -> CContained(Ta1,Ox1,Singleton(U)). Given clause: 119[0:Res:113.3,44.0] Object(U) Time(V) || Cavity(W,Place(V,U))*+ -> Cavity(W,skf3(W,X,Y))*. Given clause: 128[0:Obv:124.0] Time(U) Object(V) || Cavity(W,Place(U,V))*+ -> OSPlace(U,Singleton(V),Place(U,V))*. Given clause: 141[0:SpR:89.2,134.1] Object(U) || ClosedContainer(V,Singleton(U),W)* Cavity(W,Place(Ta1,Ob1)) -> Cavity(W,Place(V,U)). Given clause: 106[0:SpR:89.2,76.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: 158[0:Obv:155.1] Object(U) || CContained(V,W,Singleton(U)) -> Cavity(skf2(W,V,Singleton(U)),Place(V,U))*. Given clause: 165[0:SSi:161.0,4.0,1.1] || CContained(Ta1,U,Singleton(Ob1)) P(Place(Ta1,Ox1),skf2(U,Ta1,Singleton(Ob1)))* -> . SPASS V 3.7 SPASS beiseite: Proof found. Problem: C:\Users\ang\Documents\Courant\Case1-Piece1.dfg SPASS derived 94 clauses, backtracked 0 clauses, performed 0 splits and kept 100 clauses. SPASS allocated 30165 KBytes. SPASS spent 0:00:00.20 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). 44[0:Inp] || ClosedContainer(U,V,W)*+ -> Cavity(W,skf3(W,X,Y))*. 45[0:Inp] || CContained(U,V,W) -> ClosedContainer(U,W,skf2(V,U,W))*. 46[0:Inp] || ClosedContainer(U,V,W) -> OSPlace(U,V,skf3(W,V,U))*. 47[0:Inp] || Cavity(U,Slice(Ta1,HPlace(Ob1)))* P(Place(Ta1,Ox1),U) -> . 48[0:Inp] || CContained(U,V,W)*+ -> P(Place(U,V),skf2(V,U,X))*. 49[0:Inp] Object(U) Time(V) || -> equal(Slice(V,HPlace(U)),Place(V,U))**. 50[0:Inp] Time(U) Object(V) || OSPlace(U,Singleton(V),W)* -> equal(Place(U,V),W). 54[0:MRR:50.0,29.1] Object(U) || OSPlace(V,Singleton(U),W)* -> equal(Place(V,U),W). 57[0:Res:2.0,7.0] || -> Time(Ta1)*. 76[0:Res:45.1,44.0] || CContained(U,V,W) -> Cavity(skf2(V,U,W),skf3(skf2(V,U,W),X,Y))*. 80[0:Res:6.0,48.0] || -> P(Place(Ta1,Ox1),skf2(Ox1,Ta1,U))*. 86[0:SpL:49.2,47.0] Object(Ob1) Time(Ta1) || Cavity(U,Place(Ta1,Ob1))* P(Place(Ta1,Ox1),U) -> . 88[0:SSi:86.1,86.0,57.0,4.1,1.0] || Cavity(U,Place(Ta1,Ob1))* P(Place(Ta1,Ox1),U) -> . 89[0:Res:46.1,54.1] Object(U) || ClosedContainer(V,Singleton(U),W) -> equal(skf3(W,Singleton(U),V),Place(V,U))**. 106[0:SpR:89.2,76.1] Object(U) || ClosedContainer(V,Singleton(U),skf2(W,X,Y))* CContained(X,W,Y) -> Cavity(skf2(W,X,Y),Place(V,U)). 155[0:Res:45.1,106.1] Object(U) || CContained(V,W,Singleton(U)) CContained(V,W,Singleton(U)) -> Cavity(skf2(W,V,Singleton(U)),Place(V,U))*. 158[0:Obv:155.1] Object(U) || CContained(V,W,Singleton(U)) -> Cavity(skf2(W,V,Singleton(U)),Place(V,U))*. 161[0:Res:158.2,88.0] Object(Ob1) || CContained(Ta1,U,Singleton(Ob1)) P(Place(Ta1,Ox1),skf2(U,Ta1,Singleton(Ob1)))* -> . 165[0:SSi:161.0,4.0,1.1] || CContained(Ta1,U,Singleton(Ob1)) P(Place(Ta1,Ox1),skf2(U,Ta1,Singleton(Ob1)))* -> . 168[0:Res:80.0,165.1] || CContained(Ta1,Ox1,Singleton(Ob1))* -> . 169[0:MRR:168.0,6.0] || -> . Formulae used in the proof : axiom16 axiom18 axiom14 axiom17 axiom0 axiom9 axiom22 axiom21 conjecture0 axiom23 axiom24 --------------------------SPASS-STOP------------------------------