--------------------------SPASS-START----------------------------- Input Problem: 1[0:Inp] || -> Object(Ob1)*. 2[0:Inp] || -> Object(Ox1)*. 3[0:Inp] || -> Time(Ta1)*. 4[0:Inp] || -> Time(Tb1)*. 5[0:Inp] || -> History(Hc1)*. 6[0:Inp] || -> Lt(Ta1,Tb1)*. 7[0:Inp] || RigidObject(U) -> Object(U)*. 8[0:Inp] || RigidHistory(U) -> History(U)*. 9[0:Inp] || CContained(Tb1,Ox1,Singleton(Ob1))* -> . 10[0:Inp] || Lt(U,V)* -> Time(U). 11[0:Inp] || Lt(U,V)* -> Time(V). 12[0:Inp] || Leq(U,V)* -> Time(U). 13[0:Inp] || Leq(U,V)* -> Time(V). 14[0:Inp] || Ordered(U,V)* -> Time(U). 15[0:Inp] || Ordered(U,V)* -> Time(V). 16[0:Inp] || SkP0(U,V)* -> Region(V). 17[0:Inp] || SkP0(U,V)* -> Region(U). 18[0:Inp] || SkP1(U,V)* -> Region(V). 19[0:Inp] || SkP1(U,V)* -> Region(U). 20[0:Inp] || Object(U) -> ObjectSet(Singleton(U))*. 21[0:Inp] || Object(U) -> History(HPlace(U))*. 22[0:Inp] || -> NoExitCavity(Ta1,Tb1,Hc1,HPlace(Ob1))*. 23[0:Inp] || Leq(U,V)* -> Time(U). 24[0:Inp] || Leq(U,V)* -> Time(V). 25[0:Inp] || Leq3(U,V,W)* -> Time(U). 26[0:Inp] || Leq3(U,V,W)* -> Time(V). 27[0:Inp] || Leq3(U,V,W)* -> Time(W). 28[0:Inp] || P(U,V) -> SkP0(V,U)*. 29[0:Inp] || O(U,V) -> SkP0(V,U)*. 30[0:Inp] || EC(U,V) -> SkP0(V,U)*. 31[0:Inp] || DR(U,V) -> SkP0(V,U)*. 32[0:Inp] || Cavity(U,V) -> SkP1(V,U)*. 33[0:Inp] || Outside(U,V) -> SkP1(V,U)*. 34[0:Inp] || OSPlace(U,V,W)* -> Time(U). 35[0:Inp] || OSPlace(U,V,W)* -> ObjectSet(V). 36[0:Inp] || OSPlace(U,V,W)* -> Region(W). 37[0:Inp] || ClosedContainer(U,V,W)* -> Time(U). 38[0:Inp] || ClosedContainer(U,V,W)* -> ObjectSet(V). 39[0:Inp] || ClosedContainer(U,V,W)* -> Region(W). 40[0:Inp] || CContained(U,V,W)* -> Time(U). 41[0:Inp] || CContained(U,V,W)* -> Object(V). 42[0:Inp] || CContained(U,V,W)* -> ObjectSet(W). 43[0:Inp] || SkP2(U,V,W)* -> Time(W). 44[0:Inp] || SkP2(U,V,W)* -> Time(V). 45[0:Inp] || SkP2(U,V,W)* -> History(U). 46[0:Inp] || Constant(U,V,W)* -> Time(U). 47[0:Inp] || Constant(U,V,W)* -> Time(V). 48[0:Inp] || Constant(U,V,W)* -> History(W). 49[0:Inp] || ClosedContainer(U,V,W)* -> ObjectSet(V). 50[0:Inp] || ClosedContainer(U,V,W)* -> Time(U). 51[0:Inp] || CContained(U,V,W)* -> Object(V). 52[0:Inp] || SkP3(U,V,W,X)* -> Time(X). 53[0:Inp] || SkP3(U,V,W,X)* -> Time(W). 54[0:Inp] || SkP3(U,V,W,X)* -> History(V). 55[0:Inp] || SkP3(U,V,W,X)* -> History(U). 56[0:Inp] || -> P(Slice(Tb1,HPlace(Ox1)),Slice(Tb1,Hc1))*. 57[0:Inp] || Leq3(U,V,W)* -> Leq(U,V). 58[0:Inp] || Leq3(U,V,W)* -> Leq(V,W). 59[0:Inp] || Continuous(U,V,W) -> SkP2(W,V,U)*. 60[0:Inp] || WeaklyContinuous(U,V,W) -> SkP2(W,V,U)*. 61[0:Inp] || NoExitCavity(U,V,W,X)* -> Lt(U,V). 62[0:Inp] || Region(U) Region(V) -> Region(RUnion(U,V))*. 63[0:Inp] || Time(U) Object(V) -> Region(Place(U,V))*. 64[0:Inp] || Time(U) History(V) -> Region(Slice(U,V))*. 65[0:Inp] || NoExitCavity(U,V,W,X)* -> WeaklyContinuous(U,V,W). 66[0:Inp] || Leq(U,V)* -> Lt(U,V) equal(U,V). 67[0:Inp] || NoExitCavity(U,V,W,X) -> SkP3(X,W,V,U)*. 68[0:Inp] || NoEntranceCavity(U,V,W,X) -> SkP3(X,W,V,U)*. 69[0:Inp] || PersistentCavity(U,V,W,X) -> SkP3(X,W,V,U)*. 70[0:Inp] || ClosedContainer(U,V,W)* -> Cavity(W,skf2(W,X,Y))*. 71[0:Inp] || ClosedContainer(U,V,W) -> OSPlace(U,V,skf2(W,V,U))*. 72[0:Inp] || CContained(U,V,W) -> ClosedContainer(U,W,skf3(V,U,W))*. 73[0:Inp] || Leq(U,V) Leq(W,U) -> Leq3(W,U,V)*. 74[0:Inp] || CContained(U,V,W)* -> P(Place(U,V),skf3(V,U,X))*. 75[0:Inp] || Lt(U,V) Time(V) Time(U) -> Leq(U,V)*. 76[0:Inp] || equal(U,V) Time(V) Time(U) -> Leq(U,V)*. 77[0:Inp] || Time(U) Object(V) -> equal(Slice(U,HPlace(V)),Place(U,V))**. 78[0:Inp] || Time(U) Object(V) -> equal(Slice(U,HPlace(V)),Place(U,V))**. 79[0:Inp] || OSPlace(U,Singleton(V),W)* Time(U) Object(V) -> equal(Place(U,V),W). 80[0:Inp] || equal(Place(U,V),W) Time(U) Object(V) -> OSPlace(U,Singleton(V),W)*. 81[0:Inp] || Leq3(U,V,W)* NoExitCavity(U,W,X,Y)* -> Cavity(Slice(V,X),Slice(V,Y))*. 82[0:Inp] || ClosedContainer(U,V,W)* P(Place(U,X),W)* Object(X) -> CContained(U,X,V)*. 83[0:Inp] || OSPlace(U,V,W)* Cavity(X,W)* ObjectSet(V) Time(U) -> ClosedContainer(U,V,X)*. This is a first-order Non-Horn problem containing equality. This is a problem that contains sort information. The conjecture is ground. Axiom clauses: 82 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 > SkP1 > CContained > ClosedContainer > OSPlace > Cavity > P > Leq3 > Leq > Lt > ObjectSet > Object > Time > Ordered > RigidObject > RigidHistory > O > EC > DR > Outside > SkP3 > SkP2 > WeaklyContinuous > 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: 5[0:Inp] || -> History(Hc1)*. 2[0:Inp] || -> Object(Ox1)*. 1[0:Inp] || -> Object(Ob1)*. 4[0:Inp] || -> Time(Tb1)*. 3[0:Inp] || -> Time(Ta1)*. 6[0:Inp] || -> Lt(Ta1,Tb1)*. 8[0:Inp] RigidHistory(U) || -> History(U)*. 7[0:Inp] RigidObject(U) || -> Object(U)*. 22[0:Inp] || -> NoExitCavity(Ta1,Tb1,Hc1,HPlace(Ob1))*. 9[0:Inp] || CContained(Tb1,Ox1,Singleton(Ob1))* -> . 20[0:Inp] Object(U) || -> ObjectSet(Singleton(U))*. 21[0:Inp] Object(U) || -> History(HPlace(U))*. 19[0:Inp] || SkP1(U,V)* -> Region(U). 18[0:Inp] || SkP1(U,V)* -> Region(V). 17[0:Inp] || SkP0(U,V)* -> Region(U). 16[0:Inp] || SkP0(U,V)* -> Region(V). 15[0:Inp] || Ordered(U,V)* -> Time(V). 14[0:Inp] || Ordered(U,V)* -> Time(U). 11[0:Inp] || Lt(U,V)* -> Time(V). 10[0:Inp] || Lt(U,V)* -> Time(U). 24[0:Inp] || Leq(U,V)* -> Time(V). 23[0:Inp] || Leq(U,V)* -> Time(U). 33[0:Inp] || Outside(U,V) -> SkP1(V,U)*. 32[0:Inp] || Cavity(U,V) -> SkP1(V,U)*. 31[0:Inp] || DR(U,V) -> SkP0(V,U)*. 30[0:Inp] || EC(U,V) -> SkP0(V,U)*. 29[0:Inp] || O(U,V) -> SkP0(V,U)*. 28[0:Inp] || P(U,V) -> SkP0(V,U)*. 84[0:MRR:75.0,75.1,11.1,10.1] || Lt(U,V) -> Leq(U,V)*. 42[0:Inp] || CContained(U,V,W)* -> ObjectSet(W). 35[0:Inp] || OSPlace(U,V,W)* -> ObjectSet(V). 49[0:Inp] || ClosedContainer(U,V,W)* -> ObjectSet(V). 48[0:Inp] || Constant(U,V,W)* -> History(W). 45[0:Inp] || SkP2(U,V,W)* -> History(U). 51[0:Inp] || CContained(U,V,W)* -> Object(V). 36[0:Inp] || OSPlace(U,V,W)* -> Region(W). 39[0:Inp] || ClosedContainer(U,V,W)* -> Region(W). 47[0:Inp] || Constant(U,V,W)* -> Time(V). 46[0:Inp] || Constant(U,V,W)* -> Time(U). 44[0:Inp] || SkP2(U,V,W)* -> Time(V). 43[0:Inp] || SkP2(U,V,W)* -> Time(W). 40[0:Inp] || CContained(U,V,W)* -> Time(U). 34[0:Inp] || OSPlace(U,V,W)* -> Time(U). 27[0:Inp] || Leq3(U,V,W)* -> Time(W). 26[0:Inp] || Leq3(U,V,W)* -> Time(V). 25[0:Inp] || Leq3(U,V,W)* -> Time(U). 50[0:Inp] || ClosedContainer(U,V,W)* -> Time(U). 56[0:Inp] || -> P(Slice(Tb1,HPlace(Ox1)),Slice(Tb1,Hc1))*. 58[0:Inp] || Leq3(U,V,W)* -> Leq(V,W). 57[0:Inp] || Leq3(U,V,W)* -> Leq(U,V). 55[0:Inp] || SkP3(U,V,W,X)* -> History(U). 54[0:Inp] || SkP3(U,V,W,X)* -> History(V). 53[0:Inp] || SkP3(U,V,W,X)* -> Time(W). 52[0:Inp] || SkP3(U,V,W,X)* -> Time(X). 59[0:Inp] || Continuous(U,V,W) -> SkP2(W,V,U)*. 60[0:Inp] || WeaklyContinuous(U,V,W) -> SkP2(W,V,U)*. 61[0:Inp] || NoExitCavity(U,V,W,X)* -> Lt(U,V). 62[0:Inp] Region(U) Region(V) || -> Region(RUnion(V,U))*. 64[0:Inp] History(U) Time(V) || -> Region(Slice(V,U))*. 63[0:Inp] Object(U) Time(V) || -> Region(Place(V,U))*. 66[0:Inp] || Leq(U,V)* -> equal(U,V) Lt(U,V). 65[0:Inp] || NoExitCavity(U,V,W,X)* -> WeaklyContinuous(U,V,W). 69[0:Inp] || PersistentCavity(U,V,W,X) -> SkP3(X,W,V,U)*. 68[0:Inp] || NoEntranceCavity(U,V,W,X) -> SkP3(X,W,V,U)*. 67[0:Inp] || NoExitCavity(U,V,W,X) -> SkP3(X,W,V,U)*. 70[0:Inp] || ClosedContainer(U,V,W)* -> Cavity(W,skf2(W,X,Y))*. 71[0:Inp] || ClosedContainer(U,V,W) -> OSPlace(U,V,skf2(W,V,U))*. 72[0:Inp] || CContained(U,V,W) -> ClosedContainer(U,W,skf3(V,U,W))*. 73[0:Inp] || Leq(U,V) Leq(V,W) -> Leq3(U,V,W)*. 88[0:MRR:87.0,2.0] || P(Place(Tb1,Ox1),U) ClosedContainer(Tb1,Singleton(Ob1),U)* -> . 76[0:Inp] Time(U) Time(V) || equal(U,V) -> Leq(U,V)*. 74[0:Inp] || CContained(U,V,W)* -> P(Place(U,V),skf3(V,U,X))*. 86[0:MRR:83.0,83.1,35.1,34.1] || Cavity(U,V)* OSPlace(W,X,V)* -> ClosedContainer(W,X,U)*. 78[0:Inp] Object(U) Time(V) || -> equal(Slice(V,HPlace(U)),Place(V,U))**. 85[0:MRR:79.0,34.1] Object(U) || OSPlace(V,Singleton(U),W)* -> equal(Place(V,U),W). 80[0:Inp] Object(U) Time(V) || equal(Place(V,U),W) -> OSPlace(V,Singleton(U),W)*. 82[0:Inp] Object(U) || P(Place(V,U),W)* ClosedContainer(V,X,W)* -> CContained(V,U,X)*. 81[0:Inp] || Leq3(U,V,W)* NoExitCavity(U,W,X,Y)* -> Cavity(Slice(V,X),Slice(V,Y))*. Given clause: 5[0:Inp] || -> History(Hc1)*. Given clause: 2[0:Inp] || -> Object(Ox1)*. Given clause: 1[0:Inp] || -> Object(Ob1)*. Given clause: 4[0:Inp] || -> Time(Tb1)*. Given clause: 3[0:Inp] || -> Time(Ta1)*. Given clause: 6[0:Inp] || -> Lt(Ta1,Tb1)*. Given clause: 8[0:Inp] RigidHistory(U) || -> History(U)*. Given clause: 7[0:Inp] RigidObject(U) || -> Object(U)*. Given clause: 22[0:Inp] || -> NoExitCavity(Ta1,Tb1,Hc1,HPlace(Ob1))*. Given clause: 9[0:Inp] || CContained(Tb1,Ox1,Singleton(Ob1))* -> . Given clause: 20[0:Inp] Object(U) || -> ObjectSet(Singleton(U))*. Given clause: 21[0:Inp] Object(U) || -> History(HPlace(U))*. Given clause: 19[0:Inp] || SkP1(U,V)* -> Region(U). Given clause: 18[0:Inp] || SkP1(U,V)* -> Region(V). Given clause: 17[0:Inp] || SkP0(U,V)* -> Region(U). Given clause: 16[0:Inp] || SkP0(U,V)* -> Region(V). Given clause: 15[0:Inp] || Ordered(U,V)* -> Time(V). Given clause: 14[0:Inp] || Ordered(U,V)* -> Time(U). Given clause: 11[0:Inp] || Lt(U,V)* -> Time(V). Given clause: 10[0:Inp] || Lt(U,V)* -> Time(U). Given clause: 24[0:Inp] || Leq(U,V)* -> Time(V). Given clause: 23[0:Inp] || Leq(U,V)* -> Time(U). Given clause: 33[0:Inp] || Outside(U,V) -> SkP1(V,U)*. Given clause: 91[0:Res:33.1,18.0] || Outside(U,V)* -> Region(U). Given clause: 32[0:Inp] || Cavity(U,V) -> SkP1(V,U)*. Given clause: 92[0:Res:33.1,19.0] || Outside(U,V)* -> Region(V). Given clause: 93[0:Res:32.1,18.0] || Cavity(U,V)* -> Region(U). Given clause: 94[0:Res:32.1,19.0] || Cavity(U,V)* -> Region(V). Given clause: 31[0:Inp] || DR(U,V) -> SkP0(V,U)*. Given clause: 30[0:Inp] || EC(U,V) -> SkP0(V,U)*. Given clause: 95[0:Res:31.1,16.0] || DR(U,V)* -> Region(U). Given clause: 96[0:Res:31.1,17.0] || DR(U,V)* -> Region(V). Given clause: 97[0:Res:30.1,16.0] || EC(U,V)* -> Region(U). Given clause: 98[0:Res:30.1,17.0] || EC(U,V)* -> Region(V). Given clause: 29[0:Inp] || O(U,V) -> SkP0(V,U)*. Given clause: 99[0:Res:29.1,16.0] || O(U,V)* -> Region(U). Given clause: 100[0:Res:29.1,17.0] || O(U,V)* -> Region(V). Given clause: 28[0:Inp] || P(U,V) -> SkP0(V,U)*. Given clause: 101[0:Res:28.1,16.0] || P(U,V)* -> Region(U). Given clause: 84[0:MRR:75.0,75.1,11.1,10.1] || Lt(U,V) -> Leq(U,V)*. Given clause: 102[0:Res:28.1,17.0] || P(U,V)* -> Region(V). Given clause: 42[0:Inp] || CContained(U,V,W)* -> ObjectSet(W). Given clause: 35[0:Inp] || OSPlace(U,V,W)* -> ObjectSet(V). Given clause: 49[0:Inp] || ClosedContainer(U,V,W)* -> ObjectSet(V). Given clause: 48[0:Inp] || Constant(U,V,W)* -> History(W). Given clause: 45[0:Inp] || SkP2(U,V,W)* -> History(U). Given clause: 51[0:Inp] || CContained(U,V,W)* -> Object(V). Given clause: 36[0:Inp] || OSPlace(U,V,W)* -> Region(W). Given clause: 39[0:Inp] || ClosedContainer(U,V,W)* -> Region(W). Given clause: 47[0:Inp] || Constant(U,V,W)* -> Time(V). Given clause: 46[0:Inp] || Constant(U,V,W)* -> Time(U). Given clause: 44[0:Inp] || SkP2(U,V,W)* -> Time(V). Given clause: 43[0:Inp] || SkP2(U,V,W)* -> Time(W). Given clause: 40[0:Inp] || CContained(U,V,W)* -> Time(U). Given clause: 34[0:Inp] || OSPlace(U,V,W)* -> Time(U). Given clause: 27[0:Inp] || Leq3(U,V,W)* -> Time(W). Given clause: 26[0:Inp] || Leq3(U,V,W)* -> Time(V). Given clause: 25[0:Inp] || Leq3(U,V,W)* -> Time(U). Given clause: 50[0:Inp] || ClosedContainer(U,V,W)* -> Time(U). Given clause: 56[0:Inp] || -> P(Slice(Tb1,HPlace(Ox1)),Slice(Tb1,Hc1))*. Given clause: 105[0:Res:56.0,102.0] || -> Region(Slice(Tb1,Hc1))*. Given clause: 106[0:Res:56.0,101.0] || -> Region(Slice(Tb1,HPlace(Ox1)))*. Given clause: 58[0:Inp] || Leq3(U,V,W)* -> Leq(V,W). Given clause: 57[0:Inp] || Leq3(U,V,W)* -> Leq(U,V). Given clause: 55[0:Inp] || SkP3(U,V,W,X)* -> History(U). Given clause: 54[0:Inp] || SkP3(U,V,W,X)* -> History(V). Given clause: 53[0:Inp] || SkP3(U,V,W,X)* -> Time(W). Given clause: 52[0:Inp] || SkP3(U,V,W,X)* -> Time(X). Given clause: 59[0:Inp] || Continuous(U,V,W) -> SkP2(W,V,U)*. Given clause: 60[0:Inp] || WeaklyContinuous(U,V,W) -> SkP2(W,V,U)*. Given clause: 107[0:Res:59.1,43.0] || Continuous(U,V,W)* -> Time(U). Given clause: 108[0:Res:59.1,44.0] || Continuous(U,V,W)* -> Time(V). Given clause: 109[0:Res:59.1,45.0] || Continuous(U,V,W)* -> History(W). Given clause: 110[0:Res:60.1,43.0] || WeaklyContinuous(U,V,W)* -> Time(U). Given clause: 61[0:Inp] || NoExitCavity(U,V,W,X)* -> Lt(U,V). Given clause: 111[0:Res:60.1,44.0] || WeaklyContinuous(U,V,W)* -> Time(V). Given clause: 112[0:Res:60.1,45.0] || WeaklyContinuous(U,V,W)* -> History(W). Given clause: 62[0:Inp] Region(U) Region(V) || -> Region(RUnion(V,U))*. Given clause: 64[0:Inp] History(U) Time(V) || -> Region(Slice(V,U))*. Given clause: 63[0:Inp] Object(U) Time(V) || -> Region(Place(V,U))*. Given clause: 66[0:Inp] || Leq(U,V)* -> equal(U,V) Lt(U,V). Given clause: 65[0:Inp] || NoExitCavity(U,V,W,X)* -> WeaklyContinuous(U,V,W). Given clause: 115[0:Res:22.0,65.0] || -> WeaklyContinuous(Ta1,Tb1,Hc1)*. Given clause: 70[0:Inp] || ClosedContainer(U,V,W)*+ -> Cavity(W,skf2(W,X,Y))*. Given clause: 69[0:Inp] || PersistentCavity(U,V,W,X) -> SkP3(X,W,V,U)*. Given clause: 119[0:Res:69.1,52.0] || PersistentCavity(U,V,W,X)* -> Time(U). Given clause: 120[0:Res:69.1,53.0] || PersistentCavity(U,V,W,X)* -> Time(V). Given clause: 121[0:Res:69.1,54.0] || PersistentCavity(U,V,W,X)* -> History(W). Given clause: 122[0:Res:69.1,55.0] || PersistentCavity(U,V,W,X)* -> History(X). Given clause: 68[0:Inp] || NoEntranceCavity(U,V,W,X) -> SkP3(X,W,V,U)*. Given clause: 123[0:Res:68.1,52.0] || NoEntranceCavity(U,V,W,X)* -> Time(U). Given clause: 124[0:Res:68.1,53.0] || NoEntranceCavity(U,V,W,X)* -> Time(V). Given clause: 125[0:Res:68.1,54.0] || NoEntranceCavity(U,V,W,X)* -> History(W). Given clause: 126[0:Res:68.1,55.0] || NoEntranceCavity(U,V,W,X)* -> History(X). Given clause: 67[0:Inp] || NoExitCavity(U,V,W,X) -> SkP3(X,W,V,U)*. Given clause: 127[0:Res:67.1,52.0] || NoExitCavity(U,V,W,X)* -> Time(U). Given clause: 128[0:Res:67.1,53.0] || NoExitCavity(U,V,W,X)* -> Time(V). Given clause: 129[0:Res:67.1,54.0] || NoExitCavity(U,V,W,X)* -> History(W). Given clause: 130[0:Res:67.1,55.0] || NoExitCavity(U,V,W,X)* -> History(X). Given clause: 73[0:Inp] || Leq(U,V) Leq(V,W) -> Leq3(U,V,W)*. Given clause: 134[0:Res:22.0,130.0] || -> History(HPlace(Ob1))*. Given clause: 88[0:MRR:87.0,2.0] || P(Place(Tb1,Ox1),U) ClosedContainer(Tb1,Singleton(Ob1),U)* -> . Given clause: 71[0:Inp] || ClosedContainer(U,V,W) -> OSPlace(U,V,skf2(W,V,U))*. Given clause: 141[0:Res:71.1,36.0] || ClosedContainer(U,V,W) -> Region(skf2(W,V,U))*. Given clause: 72[0:Inp] || CContained(U,V,W) -> ClosedContainer(U,W,skf3(V,U,W))*. Given clause: 145[0:Res:72.1,39.0] || CContained(U,V,W) -> Region(skf3(V,U,W))*. Given clause: 76[0:Inp] Time(U) Time(V) || equal(U,V) -> Leq(U,V)*. Given clause: 74[0:Inp] || CContained(U,V,W)*+ -> P(Place(U,V),skf3(V,U,X))*. Given clause: 86[0:MRR:83.0,83.1,35.1,34.1] || Cavity(U,V)* OSPlace(W,X,V)*+ -> ClosedContainer(W,X,U)*. Given clause: 78[0:Inp] Object(U) Time(V) || -> equal(Slice(V,HPlace(U)),Place(V,U))**. Given clause: 156[0:SSi:152.1,152.0,4.0,2.0] || -> P(Place(Tb1,Ox1),Slice(Tb1,Hc1))*. Given clause: 159[0:Res:156.0,101.0] || -> Region(Place(Tb1,Ox1))*. Given clause: 85[0:MRR:79.0,34.1] Object(U) || OSPlace(V,Singleton(U),W)* -> equal(Place(V,U),W). Given clause: 147[0:Res:72.1,88.1] || CContained(Tb1,U,Singleton(Ob1)) P(Place(Tb1,Ox1),skf3(U,Tb1,Singleton(Ob1)))* -> . Given clause: 80[0:Inp] Object(U) Time(V) || equal(Place(V,U),W) -> OSPlace(V,Singleton(U),W)*. Given clause: 162[0:Res:80.3,36.0] Object(U) Time(V) || equal(Place(V,U),W)*+ -> Region(W)*. Given clause: 151[0:Res:71.1,86.1] || ClosedContainer(U,V,W) Cavity(X,skf2(W,V,U))* -> ClosedContainer(U,V,X). Given clause: 143[0:Res:72.1,70.0] || CContained(U,V,W) -> Cavity(skf3(V,U,W),skf2(skf3(V,U,W),X,Y))*. Given clause: 168[0:Res:143.1,94.0] || CContained(U,V,W) -> Region(skf2(skf3(V,U,W),X,Y))*. Given clause: 82[0:Inp] Object(U) || P(Place(V,U),W)*+ ClosedContainer(V,X,W)* -> CContained(V,U,X)*. Given clause: 172[0:SSi:171.0,2.0] || ClosedContainer(Tb1,U,Slice(Tb1,Hc1))* -> CContained(Tb1,Ox1,U). Given clause: 160[0:Res:71.1,85.1] Object(U) || ClosedContainer(V,Singleton(U),W) -> equal(skf2(W,Singleton(U),V),Place(V,U))**. Given clause: 179[0:Obv:174.1] Object(U) || ClosedContainer(V,Singleton(U),W)* -> Region(Place(V,U)). Given clause: 182[0:Res:72.1,179.1] Object(U) || CContained(V,W,Singleton(U))* -> Region(Place(V,U)). Given clause: 81[0:Inp] || Leq3(U,V,W)* NoExitCavity(U,W,X,Y)*+ -> Cavity(Slice(V,X),Slice(V,Y))*. Given clause: 183[0:Res:22.0,81.1] || Leq3(Ta1,U,Tb1) -> Cavity(Slice(U,Hc1),Slice(U,HPlace(Ob1)))*. Given clause: 186[0:Res:183.1,93.0] || Leq3(Ta1,U,Tb1) -> Region(Slice(U,Hc1))*. Given clause: 185[0:Res:183.1,94.0] || Leq3(Ta1,U,Tb1) -> Region(Slice(U,HPlace(Ob1)))*. Given clause: 188[0:MRR:187.0,26.1] || Leq3(Ta1,U,Tb1) -> Cavity(Slice(U,Hc1),Place(U,Ob1))*. Given clause: 164[0:Res:80.3,86.1] Object(U) Time(V) || equal(Place(V,U),W)*+ Cavity(X,W)* -> ClosedContainer(V,Singleton(U),X)*. Given clause: 190[0:Res:188.1,94.0] || Leq3(Ta1,U,Tb1) -> Region(Place(U,Ob1))*. Given clause: 180[0:Obv:173.1] Object(U) || ClosedContainer(V,Singleton(U),W)*+ -> OSPlace(V,Singleton(U),Place(V,U))*. Given clause: 193[0:Res:72.1,180.1] Object(U) || CContained(V,W,Singleton(U))*+ -> OSPlace(V,Singleton(U),Place(V,U))*. Given clause: 192[0:EqR:164.2] Object(U) Time(V) || Cavity(W,Place(V,U)) -> ClosedContainer(V,Singleton(U),W)*. Given clause: 181[0:Obv:178.1] Object(U) || ClosedContainer(V,Singleton(U),W)*+ Cavity(X,Place(V,U)) -> ClosedContainer(V,Singleton(U),X)*. Given clause: 202[0:SSi:198.1,198.0,4.0,1.0] || Cavity(U,Place(Tb1,Ob1))* P(Place(Tb1,Ox1),U) -> . Given clause: 211[0:MRR:210.1,156.0] || Leq3(Ta1,Tb1,Tb1)* -> . Given clause: 212[0:Res:73.2,211.0] || Leq(Ta1,Tb1) Leq(Tb1,Tb1)* -> . Given clause: 216[0:SSi:215.0,4.0] || Leq(Ta1,Tb1)* -> . SPASS V 3.7 SPASS beiseite: Proof found. Problem: C:\Users\ang\Documents\Courant\Case1-Piece4.dfg SPASS derived 113 clauses, backtracked 0 clauses, performed 0 splits and kept 147 clauses. SPASS allocated 30200 KBytes. SPASS spent 0:00:00.32 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.01 for the reduction. Here is a proof with depth 7, length 42 : 1[0:Inp] || -> Object(Ob1)*. 2[0:Inp] || -> Object(Ox1)*. 4[0:Inp] || -> Time(Tb1)*. 6[0:Inp] || -> Lt(Ta1,Tb1)*. 9[0:Inp] || CContained(Tb1,Ox1,Singleton(Ob1))* -> . 10[0:Inp] || Lt(U,V)* -> Time(U). 11[0:Inp] || Lt(U,V)* -> Time(V). 22[0:Inp] || -> NoExitCavity(Ta1,Tb1,Hc1,HPlace(Ob1))*. 26[0:Inp] || Leq3(U,V,W)* -> Time(V). 34[0:Inp] || OSPlace(U,V,W)* -> Time(U). 35[0:Inp] || OSPlace(U,V,W)* -> ObjectSet(V). 56[0:Inp] || -> P(Slice(Tb1,HPlace(Ox1)),Slice(Tb1,Hc1))*. 73[0:Inp] || Leq(U,V) Leq(V,W) -> Leq3(U,V,W)*. 75[0:Inp] Time(U) Time(V) || Lt(V,U) -> Leq(V,U)*. 76[0:Inp] Time(U) Time(V) || equal(U,V) -> Leq(U,V)*. 78[0:Inp] Object(U) Time(V) || -> equal(Slice(V,HPlace(U)),Place(V,U))**. 80[0:Inp] Object(U) Time(V) || equal(Place(V,U),W) -> OSPlace(V,Singleton(U),W)*. 81[0:Inp] || Leq3(U,V,W)* NoExitCavity(U,W,X,Y)*+ -> Cavity(Slice(V,X),Slice(V,Y))*. 82[0:Inp] Object(U) || P(Place(V,U),W)*+ ClosedContainer(V,X,W)* -> CContained(V,U,X)*. 83[0:Inp] ObjectSet(U) Time(V) || OSPlace(V,U,W)* Cavity(X,W)* -> ClosedContainer(V,U,X)*. 84[0:MRR:75.0,75.1,11.1,10.1] || Lt(U,V) -> Leq(U,V)*. 86[0:MRR:83.0,83.1,35.1,34.1] || Cavity(U,V)* OSPlace(W,X,V)*+ -> ClosedContainer(W,X,U)*. 87[0:Res:82.3,9.0] Object(Ox1) || P(Place(Tb1,Ox1),U) ClosedContainer(Tb1,Singleton(Ob1),U)* -> . 88[0:MRR:87.0,2.0] || P(Place(Tb1,Ox1),U) ClosedContainer(Tb1,Singleton(Ob1),U)* -> . 152[0:SpR:78.2,56.0] Object(Ox1) Time(Tb1) || -> P(Place(Tb1,Ox1),Slice(Tb1,Hc1))*. 156[0:SSi:152.1,152.0,4.0,2.0] || -> P(Place(Tb1,Ox1),Slice(Tb1,Hc1))*. 164[0:Res:80.3,86.1] Object(U) Time(V) || equal(Place(V,U),W)*+ Cavity(X,W)* -> ClosedContainer(V,Singleton(U),X)*. 183[0:Res:22.0,81.1] || Leq3(Ta1,U,Tb1) -> Cavity(Slice(U,Hc1),Slice(U,HPlace(Ob1)))*. 184[0:SpR:78.2,183.1] Object(Ob1) Time(U) || Leq3(Ta1,U,Tb1) -> Cavity(Slice(U,Hc1),Place(U,Ob1))*. 187[0:SSi:184.0,1.0] Time(U) || Leq3(Ta1,U,Tb1) -> Cavity(Slice(U,Hc1),Place(U,Ob1))*. 188[0:MRR:187.0,26.1] || Leq3(Ta1,U,Tb1) -> Cavity(Slice(U,Hc1),Place(U,Ob1))*. 192[0:EqR:164.2] Object(U) Time(V) || Cavity(W,Place(V,U)) -> ClosedContainer(V,Singleton(U),W)*. 198[0:Res:192.3,88.1] Object(Ob1) Time(Tb1) || Cavity(U,Place(Tb1,Ob1))* P(Place(Tb1,Ox1),U) -> . 202[0:SSi:198.1,198.0,4.0,1.0] || Cavity(U,Place(Tb1,Ob1))* P(Place(Tb1,Ox1),U) -> . 210[0:Res:188.1,202.0] || Leq3(Ta1,Tb1,Tb1) P(Place(Tb1,Ox1),Slice(Tb1,Hc1))* -> . 211[0:MRR:210.1,156.0] || Leq3(Ta1,Tb1,Tb1)* -> . 212[0:Res:73.2,211.0] || Leq(Ta1,Tb1) Leq(Tb1,Tb1)* -> . 213[0:Res:76.3,212.1] Time(Tb1) Time(Tb1) || equal(Tb1,Tb1) Leq(Ta1,Tb1)* -> . 215[0:Obv:213.2] Time(Tb1) || Leq(Ta1,Tb1)* -> . 216[0:SSi:215.0,4.0] || Leq(Ta1,Tb1)* -> . 218[0:Res:84.1,216.0] || Lt(Ta1,Tb1)* -> . 219[0:MRR:218.0,6.0] || -> . Formulae used in the proof : axiom19 axiom20 axiom22 axiom26 conjecture0 axiom0 axiom25 axiom3 axiom9 axiom24 axiom34 axiom33 axiom31 axiom29 axiom27 axiom32 axiom30 --------------------------SPASS-STOP------------------------------