--------------------------SPASS-START----------------------------- Input Problem: 1[0:Inp] || -> Lt(Ta1,Tb1)*. 2[0:Inp] || RigidObject(U) -> Object(U)*. 3[0:Inp] || RigidHistory(U) -> History(U)*. 4[0:Inp] || CContained(Tb1,Ox1,Singleton(Ob1))* -> . 5[0:Inp] || Lt(U,V)* -> Time(U). 6[0:Inp] || Lt(U,V)* -> Time(V). 7[0:Inp] || Leq(U,V)* -> Time(U). 8[0:Inp] || Leq(U,V)* -> Time(V). 9[0:Inp] || Ordered(U,V)* -> Time(U). 10[0:Inp] || Ordered(U,V)* -> Time(V). 11[0:Inp] || SkP0(U,V)* -> Region(V). 12[0:Inp] || SkP0(U,V)* -> Region(U). 13[0:Inp] || SkP1(U,V)* -> Region(V). 14[0:Inp] || SkP1(U,V)* -> Region(U). 15[0:Inp] || Object(U) -> ObjectSet(Singleton(U))*. 16[0:Inp] || Object(U) -> History(HPlace(U))*. 17[0:Inp] || -> NoExitCavity(Ta1,Tb1,Hc1,HPlace(Ob1))*. 18[0:Inp] || Leq3(U,V,W)* -> Time(U). 19[0:Inp] || Leq3(U,V,W)* -> Time(V). 20[0:Inp] || Leq3(U,V,W)* -> Time(W). 21[0:Inp] || P(U,V) -> SkP0(V,U)*. 22[0:Inp] || O(U,V) -> SkP0(V,U)*. 23[0:Inp] || EC(U,V) -> SkP0(V,U)*. 24[0:Inp] || DR(U,V) -> SkP0(V,U)*. 25[0:Inp] || Cavity(U,V) -> SkP1(V,U)*. 26[0:Inp] || Outside(U,V) -> SkP1(V,U)*. 27[0:Inp] || OSPlace(U,V,W)* -> Time(U). 28[0:Inp] || OSPlace(U,V,W)* -> ObjectSet(V). 29[0:Inp] || OSPlace(U,V,W)* -> Region(W). 30[0:Inp] || ClosedContainer(U,V,W)* -> Time(U). 31[0:Inp] || ClosedContainer(U,V,W)* -> ObjectSet(V). 32[0:Inp] || ClosedContainer(U,V,W)* -> Region(W). 33[0:Inp] || CContained(U,V,W)* -> Time(U). 34[0:Inp] || CContained(U,V,W)* -> Object(V). 35[0:Inp] || CContained(U,V,W)* -> ObjectSet(W). 36[0:Inp] || SkP2(U,V,W)* -> Time(W). 37[0:Inp] || SkP2(U,V,W)* -> Time(V). 38[0:Inp] || SkP2(U,V,W)* -> History(U). 39[0:Inp] || Constant(U,V,W)* -> Time(U). 40[0:Inp] || Constant(U,V,W)* -> Time(V). 41[0:Inp] || Constant(U,V,W)* -> History(W). 42[0:Inp] || CContained(U,V,W)* -> Object(V). 43[0:Inp] || Lt(U,V) -> Leq(U,V)*. 44[0:Inp] || equal(U,V) -> Leq(U,V)*. 45[0:Inp] || SkP3(U,V,W,X)* -> Time(X). 46[0:Inp] || SkP3(U,V,W,X)* -> Time(W). 47[0:Inp] || SkP3(U,V,W,X)* -> History(V). 48[0:Inp] || SkP3(U,V,W,X)* -> History(U). 49[0:Inp] || -> P(Slice(Tb1,HPlace(Ox1)),Slice(Tb1,Hc1))*. 50[0:Inp] || Leq3(U,V,W)* -> Leq(U,V). 51[0:Inp] || Leq3(U,V,W)* -> Leq(V,W). 52[0:Inp] || Continuous(U,V,W) -> SkP2(W,V,U)*. 53[0:Inp] || WeaklyContinuous(U,V,W) -> SkP2(W,V,U)*. 54[0:Inp] || SkP4(U,V,W,X)* -> Lt(X,W). 55[0:Inp] || Region(U) Region(V) -> Region(RUnion(U,V))*. 56[0:Inp] || Time(U) Object(V) -> Region(Place(U,V))*. 57[0:Inp] || Time(U) History(V) -> Region(Slice(U,V))*. 58[0:Inp] || SkP4(U,V,W,X)* -> WeaklyContinuous(X,W,V). 59[0:Inp] || Leq(U,V)* -> Lt(U,V) equal(U,V). 60[0:Inp] || NoExitCavity(U,V,W,X) -> SkP3(X,W,V,U)*. 61[0:Inp] || NoEntranceCavity(U,V,W,X) -> SkP3(X,W,V,U)*. 62[0:Inp] || PersistentCavity(U,V,W,X) -> SkP3(X,W,V,U)*. 63[0:Inp] || NoExitCavity(U,V,W,X) -> SkP4(X,W,V,U)*. 64[0:Inp] || NoEntranceCavity(U,V,W,X) -> SkP4(X,W,V,U)*. 65[0:Inp] || ClosedContainer(U,V,W)* -> Cavity(W,skf2(W,X,Y))*. 66[0:Inp] || ClosedContainer(U,V,W) -> OSPlace(U,V,skf2(W,V,U))*. 67[0:Inp] || CContained(U,V,W) -> ClosedContainer(U,W,skf3(V,U,W))*. 68[0:Inp] || Leq(U,V) Leq(W,U) -> Leq3(W,U,V)*. 69[0:Inp] || OSPlace(U,V,W)* Cavity(X,W)* -> ClosedContainer(U,V,X)*. 70[0:Inp] || CContained(U,V,W)* -> P(Place(U,V),skf3(V,U,X))*. 71[0:Inp] || Time(U) Object(V) -> equal(Slice(U,HPlace(V)),Place(U,V))**. 72[0:Inp] || OSPlace(U,Singleton(V),W)* Time(U) Object(V) -> equal(Place(U,V),W). 73[0:Inp] || equal(Place(U,V),W) Time(U) Object(V) -> OSPlace(U,Singleton(V),W)*. 74[0:Inp] || Leq3(U,V,W)* SkP4(X,Y,W,U)* -> Cavity(Slice(V,Y),Slice(V,X))*. 75[0:Inp] || ClosedContainer(U,V,W)* P(Place(U,X),W)* Object(X) -> CContained(U,X,V)*. This is a first-order Non-Horn problem containing equality. This is a problem that contains sort information. The conjecture is ground. Axiom clauses: 74 Conjecture clauses: 1 Inferences: IEmS=1 ISoR=1 IEqR=1 IEqF=1 ISpR=1 ISpL=1 IORe=1 IOFc=1 Reductions: RFRew=1 RBRew=1 RFMRR=1 RBMRR=1 RObv=1 RUnC=1 RTaut=1 RSSi=1 RFSub=1 RBSub=1 RAED=1 RCon=1 Extras : Input Saturation, Dynamic Selection, Full 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 > Leq3 > Leq > Lt > RigidObject > RigidHistory > O > EC > DR > Outside > SkP2 > WeaklyContinuous > SkP4 > SkP3 > NoExitCavity > PersistentCavity > NoEntranceCavity > Continuous > Constant > skc6 > skc5 > skc4 > skc3 > skc2 > skc1 > skc0 > Hc1 > Tb1 > Ta1 > Ob1 > Ox1 Ordering : KBO Processed Problem: Worked Off Clauses: Usable Clauses: 1[0:Inp] || -> Lt(Ta1,Tb1)*. 3[0:Inp] RigidHistory(U) || -> History(U)*. 2[0:Inp] RigidObject(U) || -> Object(U)*. 17[0:Inp] || -> NoExitCavity(Ta1,Tb1,Hc1,HPlace(Ob1))*. 4[0:Inp] || CContained(Tb1,Ox1,Singleton(Ob1))* -> . 15[0:Inp] Object(U) || -> ObjectSet(Singleton(U))*. 16[0:Inp] Object(U) || -> History(HPlace(U))*. 14[0:Inp] || SkP1(U,V)* -> Region(U). 13[0:Inp] || SkP1(U,V)* -> Region(V). 12[0:Inp] || SkP0(U,V)* -> Region(U). 11[0:Inp] || SkP0(U,V)* -> Region(V). 10[0:Inp] || Ordered(U,V)* -> Time(V). 9[0:Inp] || Ordered(U,V)* -> Time(U). 6[0:Inp] || Lt(U,V)* -> Time(V). 5[0:Inp] || Lt(U,V)* -> Time(U). 8[0:Inp] || Leq(U,V)* -> Time(V). 7[0:Inp] || Leq(U,V)* -> Time(U). 26[0:Inp] || Outside(U,V) -> SkP1(V,U)*. 25[0:Inp] || Cavity(U,V) -> SkP1(V,U)*. 24[0:Inp] || DR(U,V) -> SkP0(V,U)*. 23[0:Inp] || EC(U,V) -> SkP0(V,U)*. 22[0:Inp] || O(U,V) -> SkP0(V,U)*. 21[0:Inp] || P(U,V) -> SkP0(V,U)*. 44[0:Inp] || equal(U,V) -> Leq(U,V)*. 43[0:Inp] || Lt(U,V) -> Leq(U,V)*. 35[0:Inp] || CContained(U,V,W)* -> ObjectSet(W). 28[0:Inp] || OSPlace(U,V,W)* -> ObjectSet(V). 31[0:Inp] || ClosedContainer(U,V,W)* -> ObjectSet(V). 41[0:Inp] || Constant(U,V,W)* -> History(W). 38[0:Inp] || SkP2(U,V,W)* -> History(U). 42[0:Inp] || CContained(U,V,W)* -> Object(V). 29[0:Inp] || OSPlace(U,V,W)* -> Region(W). 32[0:Inp] || ClosedContainer(U,V,W)* -> Region(W). 40[0:Inp] || Constant(U,V,W)* -> Time(V). 39[0:Inp] || Constant(U,V,W)* -> Time(U). 37[0:Inp] || SkP2(U,V,W)* -> Time(V). 36[0:Inp] || SkP2(U,V,W)* -> Time(W). 33[0:Inp] || CContained(U,V,W)* -> Time(U). 27[0:Inp] || OSPlace(U,V,W)* -> Time(U). 20[0:Inp] || Leq3(U,V,W)* -> Time(W). 19[0:Inp] || Leq3(U,V,W)* -> Time(V). 18[0:Inp] || Leq3(U,V,W)* -> Time(U). 30[0:Inp] || ClosedContainer(U,V,W)* -> Time(U). 49[0:Inp] || -> P(Slice(Tb1,HPlace(Ox1)),Slice(Tb1,Hc1))*. 51[0:Inp] || Leq3(U,V,W)* -> Leq(V,W). 50[0:Inp] || Leq3(U,V,W)* -> Leq(U,V). 48[0:Inp] || SkP3(U,V,W,X)* -> History(U). 47[0:Inp] || SkP3(U,V,W,X)* -> History(V). 46[0:Inp] || SkP3(U,V,W,X)* -> Time(W). 45[0:Inp] || SkP3(U,V,W,X)* -> Time(X). 52[0:Inp] || Continuous(U,V,W) -> SkP2(W,V,U)*. 53[0:Inp] || WeaklyContinuous(U,V,W) -> SkP2(W,V,U)*. 54[0:Inp] || SkP4(U,V,W,X)* -> Lt(X,W). 55[0:Inp] Region(U) Region(V) || -> Region(RUnion(V,U))*. 57[0:Inp] History(U) Time(V) || -> Region(Slice(V,U))*. 56[0:Inp] Object(U) Time(V) || -> Region(Place(V,U))*. 59[0:Inp] || Leq(U,V)* -> equal(U,V) Lt(U,V). 58[0:Inp] || SkP4(U,V,W,X)* -> WeaklyContinuous(X,W,V). 64[0:Inp] || NoEntranceCavity(U,V,W,X) -> SkP4(X,W,V,U)*. 63[0:Inp] || NoExitCavity(U,V,W,X) -> SkP4(X,W,V,U)*. 62[0:Inp] || PersistentCavity(U,V,W,X) -> SkP3(X,W,V,U)*. 61[0:Inp] || NoEntranceCavity(U,V,W,X) -> SkP3(X,W,V,U)*. 60[0:Inp] || NoExitCavity(U,V,W,X) -> SkP3(X,W,V,U)*. 65[0:Inp] || ClosedContainer(U,V,W)* -> Cavity(W,skf2(W,X,Y))*. 66[0:Inp] || ClosedContainer(U,V,W) -> OSPlace(U,V,skf2(W,V,U))*. 67[0:Inp] || CContained(U,V,W) -> ClosedContainer(U,W,skf3(V,U,W))*. 68[0:Inp] || Leq(U,V) Leq(V,W) -> Leq3(U,V,W)*. 70[0:Inp] || CContained(U,V,W)* -> P(Place(U,V),skf3(V,U,X))*. 69[0:Inp] || Cavity(U,V)* OSPlace(W,X,V)* -> ClosedContainer(W,X,U)*. 71[0:Inp] Object(U) Time(V) || -> equal(Slice(V,HPlace(U)),Place(V,U))**. 76[0:MRR:72.0,27.1] Object(U) || OSPlace(V,Singleton(U),W)* -> equal(Place(V,U),W). 77[0:Res:75.3,4.0] Object(Ox1) || P(Place(Tb1,Ox1),U) ClosedContainer(Tb1,Singleton(Ob1),U)* -> . 73[0:Inp] Object(U) Time(V) || equal(Place(V,U),W) -> OSPlace(V,Singleton(U),W)*. 75[0:Inp] Object(U) || P(Place(V,U),W)* ClosedContainer(V,X,W)* -> CContained(V,U,X)*. 74[0:Inp] || Leq3(U,V,W)* SkP4(X,Y,W,U)* -> Cavity(Slice(V,Y),Slice(V,X))*. Given clause: 1[0:Inp] || -> Lt(Ta1,Tb1)*. Given clause: 3[0:Inp] RigidHistory(U) || -> History(U)*. Given clause: 2[0:Inp] RigidObject(U) || -> Object(U)*. Given clause: 17[0:Inp] || -> NoExitCavity(Ta1,Tb1,Hc1,HPlace(Ob1))*. Given clause: 4[0:Inp] || CContained(Tb1,Ox1,Singleton(Ob1))* -> . Given clause: 15[0:Inp] Object(U) || -> ObjectSet(Singleton(U))*. Given clause: 16[0:Inp] Object(U) || -> History(HPlace(U))*. Given clause: 14[0:Inp] || SkP1(U,V)* -> Region(U). Given clause: 13[0:Inp] || SkP1(U,V)* -> Region(V). Given clause: 12[0:Inp] || SkP0(U,V)* -> Region(U). Given clause: 11[0:Inp] || SkP0(U,V)* -> Region(V). Given clause: 10[0:Inp] || Ordered(U,V)* -> Time(V). Given clause: 9[0:Inp] || Ordered(U,V)* -> Time(U). Given clause: 6[0:Inp] || Lt(U,V)* -> Time(V). Given clause: 5[0:Inp] || Lt(U,V)* -> Time(U). Given clause: 78[0:Res:1.0,6.0] || -> Time(Tb1)*. Given clause: 79[0:Res:1.0,5.0] || -> Time(Ta1)*. Given clause: 8[0:Inp] || Leq(U,V)* -> Time(V). Given clause: 7[0:Inp] || Leq(U,V)* -> Time(U). Given clause: 26[0:Inp] || Outside(U,V) -> SkP1(V,U)*. Given clause: 80[0:Res:26.1,13.0] || Outside(U,V)* -> Region(U). Given clause: 81[0:Res:26.1,14.0] || Outside(U,V)* -> Region(V). Given clause: 25[0:Inp] || Cavity(U,V) -> SkP1(V,U)*. Given clause: 82[0:Res:25.1,13.0] || Cavity(U,V)* -> Region(U). Given clause: 24[0:Inp] || DR(U,V) -> SkP0(V,U)*. Given clause: 83[0:Res:25.1,14.0] || Cavity(U,V)* -> Region(V). Given clause: 84[0:Res:24.1,11.0] || DR(U,V)* -> Region(U). Given clause: 85[0:Res:24.1,12.0] || DR(U,V)* -> Region(V). Given clause: 23[0:Inp] || EC(U,V) -> SkP0(V,U)*. Given clause: 22[0:Inp] || O(U,V) -> SkP0(V,U)*. Given clause: 86[0:Res:23.1,11.0] || EC(U,V)* -> Region(U). Given clause: 87[0:Res:23.1,12.0] || EC(U,V)* -> Region(V). Given clause: 88[0:Res:22.1,11.0] || O(U,V)* -> Region(U). Given clause: 89[0:Res:22.1,12.0] || O(U,V)* -> Region(V). Given clause: 21[0:Inp] || P(U,V) -> SkP0(V,U)*. Given clause: 90[0:Res:21.1,11.0] || P(U,V)* -> Region(U). Given clause: 91[0:Res:21.1,12.0] || P(U,V)* -> Region(V). Given clause: 44[0:Inp] || equal(U,V) -> Leq(U,V)*. Given clause: 94[0:AED:92.0] || -> Time(U)*. Given clause: 95[0:MRR:57.1,94.0] History(U) || -> Region(Slice(V,U))*. Given clause: 96[0:MRR:56.1,94.0] Object(U) || -> Region(Place(V,U))*. Given clause: 43[0:Inp] || Lt(U,V) -> Leq(U,V)*. Given clause: 35[0:Inp] || CContained(U,V,W)* -> ObjectSet(W). Given clause: 28[0:Inp] || OSPlace(U,V,W)* -> ObjectSet(V). Given clause: 31[0:Inp] || ClosedContainer(U,V,W)* -> ObjectSet(V). Given clause: 41[0:Inp] || Constant(U,V,W)* -> History(W). Given clause: 38[0:Inp] || SkP2(U,V,W)* -> History(U). Given clause: 42[0:Inp] || CContained(U,V,W)* -> Object(V). Given clause: 29[0:Inp] || OSPlace(U,V,W)* -> Region(W). Given clause: 32[0:Inp] || ClosedContainer(U,V,W)* -> Region(W). Given clause: 49[0:Inp] || -> P(Slice(Tb1,HPlace(Ox1)),Slice(Tb1,Hc1))*. Given clause: 100[0:Res:49.0,91.0] || -> Region(Slice(Tb1,Hc1))*. Given clause: 101[0:Res:49.0,90.0] || -> Region(Slice(Tb1,HPlace(Ox1)))*. Given clause: 51[0:Inp] || Leq3(U,V,W)* -> Leq(V,W). Given clause: 50[0:Inp] || Leq3(U,V,W)* -> Leq(U,V). Given clause: 48[0:Inp] || SkP3(U,V,W,X)* -> History(U). Given clause: 47[0:Inp] || SkP3(U,V,W,X)* -> History(V). Given clause: 52[0:Inp] || Continuous(U,V,W) -> SkP2(W,V,U)*. Given clause: 102[0:Res:52.1,38.0] || Continuous(U,V,W)* -> History(W). Given clause: 53[0:Inp] || WeaklyContinuous(U,V,W) -> SkP2(W,V,U)*. Given clause: 103[0:Res:53.1,38.0] || WeaklyContinuous(U,V,W)* -> History(W). Given clause: 54[0:Inp] || SkP4(U,V,W,X)* -> Lt(X,W). Given clause: 55[0:Inp] Region(U) Region(V) || -> Region(RUnion(V,U))*. Given clause: 59[0:Inp] || Leq(U,V)* -> equal(U,V) Lt(U,V). Given clause: 58[0:Inp] || SkP4(U,V,W,X)* -> WeaklyContinuous(X,W,V). Given clause: 97[0:MRR:71.1,94.0] Object(U) || -> equal(Slice(V,HPlace(U)),Place(V,U))**. Given clause: 108[0:SpR:97.1,49.0] Object(Ox1) || -> P(Place(Tb1,Ox1),Slice(Tb1,Hc1))*. Given clause: 110[0:SoR:108.0,2.1] RigidObject(Ox1) || -> P(Place(Tb1,Ox1),Slice(Tb1,Hc1))*. Given clause: 65[0:Inp] || ClosedContainer(U,V,W)*+ -> Cavity(W,skf2(W,X,Y))*. Given clause: 64[0:Inp] || NoEntranceCavity(U,V,W,X) -> SkP4(X,W,V,U)*. Given clause: 112[0:Res:64.1,54.0] || NoEntranceCavity(U,V,W,X)* -> Lt(U,V). Given clause: 111[0:Res:64.1,58.0] || NoEntranceCavity(U,V,W,X)* -> WeaklyContinuous(U,V,W). Given clause: 63[0:Inp] || NoExitCavity(U,V,W,X) -> SkP4(X,W,V,U)*. Given clause: 114[0:Res:63.1,54.0] || NoExitCavity(U,V,W,X)* -> Lt(U,V). Given clause: 62[0:Inp] || PersistentCavity(U,V,W,X) -> SkP3(X,W,V,U)*. Given clause: 116[0:Res:62.1,47.0] || PersistentCavity(U,V,W,X)* -> History(W). Given clause: 117[0:Res:62.1,48.0] || PersistentCavity(U,V,W,X)* -> History(X). Given clause: 113[0:Res:63.1,58.0] || NoExitCavity(U,V,W,X)* -> WeaklyContinuous(U,V,W). Given clause: 118[0:Res:17.0,113.0] || -> WeaklyContinuous(Ta1,Tb1,Hc1)*. Given clause: 61[0:Inp] || NoEntranceCavity(U,V,W,X) -> SkP3(X,W,V,U)*. Given clause: 119[0:Res:118.0,103.0] || -> History(Hc1)*. Given clause: 120[0:Res:61.1,47.0] || NoEntranceCavity(U,V,W,X)* -> History(W). Given clause: 121[0:Res:61.1,48.0] || NoEntranceCavity(U,V,W,X)* -> History(X). Given clause: 60[0:Inp] || NoExitCavity(U,V,W,X) -> SkP3(X,W,V,U)*. Given clause: 68[0:Inp] || Leq(U,V) Leq(V,W) -> Leq3(U,V,W)*. Given clause: 122[0:Res:60.1,47.0] || NoExitCavity(U,V,W,X)* -> History(W). Given clause: 123[0:Res:60.1,48.0] || NoExitCavity(U,V,W,X)* -> History(X). Given clause: 127[0:Res:17.0,123.0] || -> History(HPlace(Ob1))*. Given clause: 66[0:Inp] || ClosedContainer(U,V,W) -> OSPlace(U,V,skf2(W,V,U))*. Given clause: 67[0:Inp] || CContained(U,V,W) -> ClosedContainer(U,W,skf3(V,U,W))*. Given clause: 128[0:Res:66.1,29.0] || ClosedContainer(U,V,W) -> Region(skf2(W,V,U))*. Given clause: 131[0:Res:67.1,32.0] || CContained(U,V,W) -> Region(skf3(V,U,W))*. Given clause: 70[0:Inp] || CContained(U,V,W)*+ -> P(Place(U,V),skf3(V,U,X))*. Given clause: 69[0:Inp] || Cavity(U,V)* OSPlace(W,X,V)*+ -> ClosedContainer(W,X,U)*. Given clause: 76[0:MRR:72.0,27.1] Object(U) || OSPlace(V,Singleton(U),W)* -> equal(Place(V,U),W). Given clause: 98[0:MRR:73.1,94.0] Object(U) || equal(Place(V,U),W) -> OSPlace(V,Singleton(U),W)*. Given clause: 135[0:Res:98.2,29.0] Object(U) || equal(Place(V,U),W)*+ -> Region(W)*. Given clause: 77[0:Res:75.3,4.0] Object(Ox1) || P(Place(Tb1,Ox1),U) ClosedContainer(Tb1,Singleton(Ob1),U)* -> . Given clause: 141[0:SoR:77.0,2.1] RigidObject(Ox1) || P(Place(Tb1,Ox1),U) ClosedContainer(Tb1,Singleton(Ob1),U)* -> . Given clause: 75[0:Inp] Object(U) || P(Place(V,U),W)*+ ClosedContainer(V,X,W)* -> CContained(V,U,X)*. Given clause: 133[0:Res:66.1,69.1] || ClosedContainer(U,V,W) Cavity(X,skf2(W,V,U))* -> ClosedContainer(U,V,X). Given clause: 130[0:Res:67.1,65.0] || CContained(U,V,W) -> Cavity(skf3(V,U,W),skf2(skf3(V,U,W),X,Y))*. Given clause: 142[0:Res:130.1,83.0] || CContained(U,V,W) -> Region(skf2(skf3(V,U,W),X,Y))*. Given clause: 134[0:Res:66.1,76.1] Object(U) || ClosedContainer(V,Singleton(U),W) -> equal(skf2(W,Singleton(U),V),Place(V,U))**. Given clause: 74[0:Inp] || Leq3(U,V,W)* SkP4(X,Y,W,U)*+ -> Cavity(Slice(V,Y),Slice(V,X))*. Given clause: 152[0:Obv:145.1] Object(U) || ClosedContainer(V,Singleton(U),W)*+ -> OSPlace(V,Singleton(U),Place(V,U))*. Given clause: 156[0:Res:67.1,152.1] Object(U) || CContained(V,W,Singleton(U))*+ -> OSPlace(V,Singleton(U),Place(V,U))*. Given clause: 137[0:Res:98.2,69.1] Object(U) || equal(Place(V,U),W)*+ Cavity(X,W)* -> ClosedContainer(V,Singleton(U),X)*. Given clause: 157[0:EqR:137.1] Object(U) || Cavity(V,Place(W,U)) -> ClosedContainer(W,Singleton(U),V)*. Given clause: 154[0:Res:63.1,74.1] || NoExitCavity(U,V,W,X)*+ Leq3(U,Y,V)* -> Cavity(Slice(Y,W),Slice(Y,X))*. Given clause: 163[0:Res:17.0,154.0] || Leq3(Ta1,U,Tb1) -> Cavity(Slice(U,Hc1),Slice(U,HPlace(Ob1)))*. Given clause: 166[0:Res:163.1,82.0] || Leq3(Ta1,U,Tb1) -> Region(Slice(U,Hc1))*. Given clause: 165[0:Res:163.1,83.0] || Leq3(Ta1,U,Tb1) -> Region(Slice(U,HPlace(Ob1)))*. Given clause: 164[0:SpR:97.1,163.1] Object(Ob1) || Leq3(Ta1,U,Tb1) -> Cavity(Slice(U,Hc1),Place(U,Ob1))*. Given clause: 155[0:Res:64.1,74.1] || NoEntranceCavity(U,V,W,X)*+ Leq3(U,Y,V)* -> Cavity(Slice(Y,W),Slice(Y,X))*. Given clause: 168[0:SoR:164.0,2.1] RigidObject(Ob1) || Leq3(Ta1,U,Tb1) -> Cavity(Slice(U,Hc1),Place(U,Ob1))*. Given clause: 158[0:Res:157.2,65.0] Object(U) || Cavity(V,Place(W,U))*+ -> Cavity(V,skf2(V,X,Y))*. Given clause: 162[0:Obv:161.0] Object(U) || Cavity(V,Place(W,U))*+ -> OSPlace(W,Singleton(U),Place(W,U))*. Given clause: 148[0:SpR:134.2,130.1] Object(U) || ClosedContainer(V,Singleton(U),skf3(W,X,Y))* CContained(X,W,Y) -> Cavity(skf3(W,X,Y),Place(V,U)). Given clause: 171[0:Obv:169.1] Object(U) || CContained(V,W,Singleton(U)) -> Cavity(skf3(W,V,Singleton(U)),Place(V,U))*. SPASS V 3.7 SPASS beiseite: Completion found. Problem: Scenario1_Part4.txt SPASS derived 91 clauses, backtracked 0 clauses, performed 0 splits and kept 137 clauses. SPASS allocated 52391 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. The saturated set of worked-off clauses is : 171[0:Obv:169.1] Object(U) || CContained(V,W,Singleton(U)) -> Cavity(skf3(W,V,Singleton(U)),Place(V,U))*. 148[0:SpR:134.2,130.1] Object(U) || ClosedContainer(V,Singleton(U),skf3(W,X,Y))* CContained(X,W,Y) -> Cavity(skf3(W,X,Y),Place(V,U)). 162[0:Obv:161.0] Object(U) || Cavity(V,Place(W,U))*+ -> OSPlace(W,Singleton(U),Place(W,U))*. 158[0:Res:157.2,65.0] Object(U) || Cavity(V,Place(W,U))*+ -> Cavity(V,skf2(V,X,Y))*. 168[0:SoR:164.0,2.1] RigidObject(Ob1) || Leq3(Ta1,U,Tb1) -> Cavity(Slice(U,Hc1),Place(U,Ob1))*. 155[0:Res:64.1,74.1] || NoEntranceCavity(U,V,W,X)*+ Leq3(U,Y,V)* -> Cavity(Slice(Y,W),Slice(Y,X))*. 164[0:SpR:97.1,163.1] Object(Ob1) || Leq3(Ta1,U,Tb1) -> Cavity(Slice(U,Hc1),Place(U,Ob1))*. 165[0:Res:163.1,83.0] || Leq3(Ta1,U,Tb1) -> Region(Slice(U,HPlace(Ob1)))*. 166[0:Res:163.1,82.0] || Leq3(Ta1,U,Tb1) -> Region(Slice(U,Hc1))*. 163[0:Res:17.0,154.0] || Leq3(Ta1,U,Tb1) -> Cavity(Slice(U,Hc1),Slice(U,HPlace(Ob1)))*. 154[0:Res:63.1,74.1] || NoExitCavity(U,V,W,X)*+ Leq3(U,Y,V)* -> Cavity(Slice(Y,W),Slice(Y,X))*. 157[0:EqR:137.1] Object(U) || Cavity(V,Place(W,U)) -> ClosedContainer(W,Singleton(U),V)*. 137[0:Res:98.2,69.1] Object(U) || equal(Place(V,U),W)*+ Cavity(X,W)* -> ClosedContainer(V,Singleton(U),X)*. 156[0:Res:67.1,152.1] Object(U) || CContained(V,W,Singleton(U))*+ -> OSPlace(V,Singleton(U),Place(V,U))*. 152[0:Obv:145.1] Object(U) || ClosedContainer(V,Singleton(U),W)*+ -> OSPlace(V,Singleton(U),Place(V,U))*. 74[0:Inp] || Leq3(U,V,W)* SkP4(X,Y,W,U)*+ -> Cavity(Slice(V,Y),Slice(V,X))*. 134[0:Res:66.1,76.1] Object(U) || ClosedContainer(V,Singleton(U),W) -> equal(skf2(W,Singleton(U),V),Place(V,U))**. 142[0:Res:130.1,83.0] || CContained(U,V,W) -> Region(skf2(skf3(V,U,W),X,Y))*. 130[0:Res:67.1,65.0] || CContained(U,V,W) -> Cavity(skf3(V,U,W),skf2(skf3(V,U,W),X,Y))*. 133[0:Res:66.1,69.1] || ClosedContainer(U,V,W) Cavity(X,skf2(W,V,U))* -> ClosedContainer(U,V,X). 75[0:Inp] Object(U) || P(Place(V,U),W)*+ ClosedContainer(V,X,W)* -> CContained(V,U,X)*. 141[0:SoR:77.0,2.1] RigidObject(Ox1) || P(Place(Tb1,Ox1),U) ClosedContainer(Tb1,Singleton(Ob1),U)* -> . 77[0:Res:75.3,4.0] Object(Ox1) || P(Place(Tb1,Ox1),U) ClosedContainer(Tb1,Singleton(Ob1),U)* -> . 135[0:Res:98.2,29.0] Object(U) || equal(Place(V,U),W)*+ -> Region(W)*. 98[0:MRR:73.1,94.0] Object(U) || equal(Place(V,U),W) -> OSPlace(V,Singleton(U),W)*. 76[0:MRR:72.0,27.1] Object(U) || OSPlace(V,Singleton(U),W)* -> equal(Place(V,U),W). 69[0:Inp] || Cavity(U,V)* OSPlace(W,X,V)*+ -> ClosedContainer(W,X,U)*. 70[0:Inp] || CContained(U,V,W)*+ -> P(Place(U,V),skf3(V,U,X))*. 131[0:Res:67.1,32.0] || CContained(U,V,W) -> Region(skf3(V,U,W))*. 128[0:Res:66.1,29.0] || ClosedContainer(U,V,W) -> Region(skf2(W,V,U))*. 67[0:Inp] || CContained(U,V,W) -> ClosedContainer(U,W,skf3(V,U,W))*. 66[0:Inp] || ClosedContainer(U,V,W) -> OSPlace(U,V,skf2(W,V,U))*. 127[0:Res:17.0,123.0] || -> History(HPlace(Ob1))*. 123[0:Res:60.1,48.0] || NoExitCavity(U,V,W,X)* -> History(X). 122[0:Res:60.1,47.0] || NoExitCavity(U,V,W,X)* -> History(W). 68[0:Inp] || Leq(U,V) Leq(V,W) -> Leq3(U,V,W)*. 60[0:Inp] || NoExitCavity(U,V,W,X) -> SkP3(X,W,V,U)*. 121[0:Res:61.1,48.0] || NoEntranceCavity(U,V,W,X)* -> History(X). 120[0:Res:61.1,47.0] || NoEntranceCavity(U,V,W,X)* -> History(W). 119[0:Res:118.0,103.0] || -> History(Hc1)*. 61[0:Inp] || NoEntranceCavity(U,V,W,X) -> SkP3(X,W,V,U)*. 118[0:Res:17.0,113.0] || -> WeaklyContinuous(Ta1,Tb1,Hc1)*. 113[0:Res:63.1,58.0] || NoExitCavity(U,V,W,X)* -> WeaklyContinuous(U,V,W). 117[0:Res:62.1,48.0] || PersistentCavity(U,V,W,X)* -> History(X). 116[0:Res:62.1,47.0] || PersistentCavity(U,V,W,X)* -> History(W). 62[0:Inp] || PersistentCavity(U,V,W,X) -> SkP3(X,W,V,U)*. 114[0:Res:63.1,54.0] || NoExitCavity(U,V,W,X)* -> Lt(U,V). 63[0:Inp] || NoExitCavity(U,V,W,X) -> SkP4(X,W,V,U)*. 111[0:Res:64.1,58.0] || NoEntranceCavity(U,V,W,X)* -> WeaklyContinuous(U,V,W). 112[0:Res:64.1,54.0] || NoEntranceCavity(U,V,W,X)* -> Lt(U,V). 64[0:Inp] || NoEntranceCavity(U,V,W,X) -> SkP4(X,W,V,U)*. 65[0:Inp] || ClosedContainer(U,V,W)*+ -> Cavity(W,skf2(W,X,Y))*. 110[0:SoR:108.0,2.1] RigidObject(Ox1) || -> P(Place(Tb1,Ox1),Slice(Tb1,Hc1))*. 108[0:SpR:97.1,49.0] Object(Ox1) || -> P(Place(Tb1,Ox1),Slice(Tb1,Hc1))*. 97[0:MRR:71.1,94.0] Object(U) || -> equal(Slice(V,HPlace(U)),Place(V,U))**. 58[0:Inp] || SkP4(U,V,W,X)* -> WeaklyContinuous(X,W,V). 59[0:Inp] || Leq(U,V)* -> equal(U,V) Lt(U,V). 55[0:Inp] Region(U) Region(V) || -> Region(RUnion(V,U))*. 54[0:Inp] || SkP4(U,V,W,X)* -> Lt(X,W). 103[0:Res:53.1,38.0] || WeaklyContinuous(U,V,W)* -> History(W). 53[0:Inp] || WeaklyContinuous(U,V,W) -> SkP2(W,V,U)*. 102[0:Res:52.1,38.0] || Continuous(U,V,W)* -> History(W). 52[0:Inp] || Continuous(U,V,W) -> SkP2(W,V,U)*. 47[0:Inp] || SkP3(U,V,W,X)* -> History(V). 48[0:Inp] || SkP3(U,V,W,X)* -> History(U). 50[0:Inp] || Leq3(U,V,W)* -> Leq(U,V). 51[0:Inp] || Leq3(U,V,W)* -> Leq(V,W). 101[0:Res:49.0,90.0] || -> Region(Slice(Tb1,HPlace(Ox1)))*. 100[0:Res:49.0,91.0] || -> Region(Slice(Tb1,Hc1))*. 49[0:Inp] || -> P(Slice(Tb1,HPlace(Ox1)),Slice(Tb1,Hc1))*. 32[0:Inp] || ClosedContainer(U,V,W)* -> Region(W). 29[0:Inp] || OSPlace(U,V,W)* -> Region(W). 42[0:Inp] || CContained(U,V,W)* -> Object(V). 38[0:Inp] || SkP2(U,V,W)* -> History(U). 41[0:Inp] || Constant(U,V,W)* -> History(W). 31[0:Inp] || ClosedContainer(U,V,W)* -> ObjectSet(V). 28[0:Inp] || OSPlace(U,V,W)* -> ObjectSet(V). 35[0:Inp] || CContained(U,V,W)* -> ObjectSet(W). 43[0:Inp] || Lt(U,V) -> Leq(U,V)*. 96[0:MRR:56.1,94.0] Object(U) || -> Region(Place(V,U))*. 95[0:MRR:57.1,94.0] History(U) || -> Region(Slice(V,U))*. 94[0:AED:92.0] || -> Time(U)*. 44[0:Inp] || equal(U,V) -> Leq(U,V)*. 91[0:Res:21.1,12.0] || P(U,V)* -> Region(V). 90[0:Res:21.1,11.0] || P(U,V)* -> Region(U). 21[0:Inp] || P(U,V) -> SkP0(V,U)*. 89[0:Res:22.1,12.0] || O(U,V)* -> Region(V). 88[0:Res:22.1,11.0] || O(U,V)* -> Region(U). 87[0:Res:23.1,12.0] || EC(U,V)* -> Region(V). 86[0:Res:23.1,11.0] || EC(U,V)* -> Region(U). 22[0:Inp] || O(U,V) -> SkP0(V,U)*. 23[0:Inp] || EC(U,V) -> SkP0(V,U)*. 85[0:Res:24.1,12.0] || DR(U,V)* -> Region(V). 84[0:Res:24.1,11.0] || DR(U,V)* -> Region(U). 83[0:Res:25.1,14.0] || Cavity(U,V)* -> Region(V). 24[0:Inp] || DR(U,V) -> SkP0(V,U)*. 82[0:Res:25.1,13.0] || Cavity(U,V)* -> Region(U). 25[0:Inp] || Cavity(U,V) -> SkP1(V,U)*. 81[0:Res:26.1,14.0] || Outside(U,V)* -> Region(V). 80[0:Res:26.1,13.0] || Outside(U,V)* -> Region(U). 26[0:Inp] || Outside(U,V) -> SkP1(V,U)*. 11[0:Inp] || SkP0(U,V)* -> Region(V). 12[0:Inp] || SkP0(U,V)* -> Region(U). 13[0:Inp] || SkP1(U,V)* -> Region(V). 14[0:Inp] || SkP1(U,V)* -> Region(U). 16[0:Inp] Object(U) || -> History(HPlace(U))*. 15[0:Inp] Object(U) || -> ObjectSet(Singleton(U))*. 4[0:Inp] || CContained(Tb1,Ox1,Singleton(Ob1))* -> . 17[0:Inp] || -> NoExitCavity(Ta1,Tb1,Hc1,HPlace(Ob1))*. 2[0:Inp] RigidObject(U) || -> Object(U)*. 3[0:Inp] RigidHistory(U) || -> History(U)*. 1[0:Inp] || -> Lt(Ta1,Tb1)*. --------------------------SPASS-STOP------------------------------