--------------------------SPASS-START----------------------------- Input Problem: 1[0:Inp] || -> RigidHistory(HPlace(Ob1))*. 2[0:Inp] || -> Lt(Ta1,Tb1)*. 3[0:Inp] || RigidObject(U) -> Object(U)*. 4[0:Inp] || RigidHistory(U) -> History(U)*. 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] || -> Cavity(Rc1,Slice(Ta1,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] || Lt(U,V) -> Leq(U,V)*. 37[0:Inp] || equal(U,V) -> Leq(U,V)*. 38[0:Inp] || -> RigidHistory(skf1(U,V,W,X,Y))*. 39[0:Inp] || SkP2(U,V,W,X)* -> Time(X). 40[0:Inp] || SkP2(U,V,W,X)* -> Time(W). 41[0:Inp] || SkP2(U,V,W,X)* -> History(V). 42[0:Inp] || SkP2(U,V,W,X)* -> History(U). 43[0:Inp] || Leq3(U,V,W)* -> Leq(U,V). 44[0:Inp] || Leq3(U,V,W)* -> Leq(V,W). 45[0:Inp] || Region(U) Region(V) -> Region(RUnion(U,V))*. 46[0:Inp] || Time(U) Object(V) -> Region(Place(U,V))*. 47[0:Inp] || Time(U) History(V) -> Region(Slice(U,V))*. 48[0:Inp] || Leq(U,V)* -> Lt(U,V) equal(U,V). 49[0:Inp] || NoExitCavity(U,V,W,X) -> SkP2(X,W,V,U)*. 50[0:Inp] || NoEntranceCavity(U,V,W,X) -> SkP2(X,W,V,U)*. 51[0:Inp] || PersistentCavity(U,V,W,X) -> SkP2(X,W,V,U)*. 52[0:Inp] || PersistentCavity(U,V,W,X)* -> NoExitCavity(U,V,W,X). 53[0:Inp] || PersistentCavity(U,V,W,X) -> NoEntranceCavity(U,V,W,X)*. 54[0:Inp] || Leq(U,V) Leq(W,U) -> Leq3(W,U,V)*. 55[0:Inp] || equal(Slice(Ta1,U),Rc1) NoExitCavity(Ta1,Tb1,U,HPlace(Ob1))* -> . 56[0:Inp] || NoExitCavity(U,V,W,X) NoEntranceCavity(U,V,W,X)* -> PersistentCavity(U,V,W,X). 57[0:Inp] || Cavity(U,Slice(V,W)) RigidHistory(W) Leq3(X,V,Y) -> equal(Slice(V,skf1(V,U,W,Y,X)),U)**. 58[0:Inp] || Cavity(U,Slice(V,W)) RigidHistory(W) Leq3(X,V,Y) -> PersistentCavity(X,Y,skf1(V,U,W,Y,X),W)*. This is a first-order Non-Horn problem containing equality. This is a problem that contains sort information. Axiom clauses: 57 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: skf1 > skf0 > Slice > Place > RUnion > HPlace > Singleton > Region > Time > Ordered > History > ObjectSet > Object > SkP2 > NoEntranceCavity > PersistentCavity > NoExitCavity > Leq3 > Leq > Lt > SkP0 > P > SkP1 > Cavity > OSPlace > ClosedContainer > CContained > RigidObject > RigidHistory > O > EC > DR > Outside > Hc1 > Rc1 > Tb1 > Ta1 > Ob1 > Ox1 Ordering : KBO Processed Problem: Worked Off Clauses: Usable Clauses: 2[0:Inp] || -> Lt(Ta1,Tb1)*. 1[0:Inp] || -> RigidHistory(HPlace(Ob1))*. 3[0:Inp] RigidObject(U) || -> Object(U)*. 4[0:Inp] RigidHistory(U) || -> History(U)*. 17[0:Inp] || -> Cavity(Rc1,Slice(Ta1,HPlace(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)*. 37[0:Inp] || equal(U,V) -> Leq(U,V)*. 36[0:Inp] || Lt(U,V) -> Leq(U,V)*. 35[0:Inp] || CContained(U,V,W)* -> ObjectSet(W). 31[0:Inp] || ClosedContainer(U,V,W)* -> ObjectSet(V). 28[0:Inp] || OSPlace(U,V,W)* -> ObjectSet(V). 34[0:Inp] || CContained(U,V,W)* -> Object(V). 32[0:Inp] || ClosedContainer(U,V,W)* -> Region(W). 29[0:Inp] || OSPlace(U,V,W)* -> Region(W). 33[0:Inp] || CContained(U,V,W)* -> Time(U). 30[0:Inp] || ClosedContainer(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). 38[0:Inp] || -> RigidHistory(skf1(U,V,W,X,Y))*. 44[0:Inp] || Leq3(U,V,W)* -> Leq(V,W). 43[0:Inp] || Leq3(U,V,W)* -> Leq(U,V). 42[0:Inp] || SkP2(U,V,W,X)* -> History(U). 41[0:Inp] || SkP2(U,V,W,X)* -> History(V). 40[0:Inp] || SkP2(U,V,W,X)* -> Time(W). 39[0:Inp] || SkP2(U,V,W,X)* -> Time(X). 45[0:Inp] Region(U) Region(V) || -> Region(RUnion(V,U))*. 47[0:Inp] History(U) Time(V) || -> Region(Slice(V,U))*. 46[0:Inp] Object(U) Time(V) || -> Region(Place(V,U))*. 48[0:Inp] || Leq(U,V)* -> equal(U,V) Lt(U,V). 53[0:Inp] || PersistentCavity(U,V,W,X) -> NoEntranceCavity(U,V,W,X)*. 52[0:Inp] || PersistentCavity(U,V,W,X)* -> NoExitCavity(U,V,W,X). 50[0:Inp] || NoEntranceCavity(U,V,W,X) -> SkP2(X,W,V,U)*. 49[0:Inp] || NoExitCavity(U,V,W,X) -> SkP2(X,W,V,U)*. 51[0:Inp] || PersistentCavity(U,V,W,X) -> SkP2(X,W,V,U)*. 54[0:Inp] || Leq(U,V) Leq(V,W) -> Leq3(U,V,W)*. 55[0:Inp] || equal(Slice(Ta1,U),Rc1) NoExitCavity(Ta1,Tb1,U,HPlace(Ob1))* -> . 56[0:Inp] || NoEntranceCavity(U,V,W,X)* NoExitCavity(U,V,W,X) -> PersistentCavity(U,V,W,X). 58[0:Inp] RigidHistory(U) || Cavity(V,Slice(W,U)) Leq3(X,W,Y) -> PersistentCavity(X,Y,skf1(W,V,U,Y,X),U)*. 57[0:Inp] RigidHistory(U) || Cavity(V,Slice(W,U)) Leq3(X,W,Y) -> equal(Slice(W,skf1(W,V,U,Y,X)),V)**. Given clause: 2[0:Inp] || -> Lt(Ta1,Tb1)*. Given clause: 1[0:Inp] || -> RigidHistory(HPlace(Ob1))*. Given clause: 3[0:Inp] RigidObject(U) || -> Object(U)*. Given clause: 4[0:Inp] RigidHistory(U) || -> History(U)*. Given clause: 17[0:Inp] || -> Cavity(Rc1,Slice(Ta1,HPlace(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: 59[0:Res:2.0,6.0] || -> Time(Tb1)*. Given clause: 60[0:Res:2.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: 61[0:Res:26.1,13.0] || Outside(U,V)* -> Region(U). Given clause: 62[0:Res:26.1,14.0] || Outside(U,V)* -> Region(V). Given clause: 25[0:Inp] || Cavity(U,V) -> SkP1(V,U)*. Given clause: 63[0:Res:25.1,13.0] || Cavity(U,V)* -> Region(U). Given clause: 24[0:Inp] || DR(U,V) -> SkP0(V,U)*. Given clause: 65[0:Res:17.0,63.0] || -> Region(Rc1)*. Given clause: 64[0:Res:25.1,14.0] || Cavity(U,V)* -> Region(V). Given clause: 68[0:Res:17.0,64.0] || -> Region(Slice(Ta1,HPlace(Ob1)))*. Given clause: 66[0:Res:24.1,11.0] || DR(U,V)* -> Region(U). Given clause: 23[0:Inp] || EC(U,V) -> SkP0(V,U)*. Given clause: 67[0:Res:24.1,12.0] || DR(U,V)* -> Region(V). Given clause: 69[0:Res:23.1,11.0] || EC(U,V)* -> Region(U). Given clause: 70[0:Res:23.1,12.0] || EC(U,V)* -> Region(V). Given clause: 22[0:Inp] || O(U,V) -> SkP0(V,U)*. Given clause: 21[0:Inp] || P(U,V) -> SkP0(V,U)*. Given clause: 71[0:Res:22.1,11.0] || O(U,V)* -> Region(U). Given clause: 72[0:Res:22.1,12.0] || O(U,V)* -> Region(V). Given clause: 73[0:Res:21.1,11.0] || P(U,V)* -> Region(U). Given clause: 74[0:Res:21.1,12.0] || P(U,V)* -> Region(V). Given clause: 37[0:Inp] || equal(U,V) -> Leq(U,V)*. Given clause: 77[0:AED:75.0] || -> Time(U)*. Given clause: 78[0:MRR:47.1,77.0] History(U) || -> Region(Slice(V,U))*. Given clause: 79[0:MRR:46.1,77.0] Object(U) || -> Region(Place(V,U))*. Given clause: 36[0:Inp] || Lt(U,V) -> Leq(U,V)*. Given clause: 35[0:Inp] || CContained(U,V,W)* -> ObjectSet(W). Given clause: 31[0:Inp] || ClosedContainer(U,V,W)* -> ObjectSet(V). Given clause: 28[0:Inp] || OSPlace(U,V,W)* -> ObjectSet(V). Given clause: 34[0:Inp] || CContained(U,V,W)* -> Object(V). Given clause: 32[0:Inp] || ClosedContainer(U,V,W)* -> Region(W). Given clause: 29[0:Inp] || OSPlace(U,V,W)* -> Region(W). Given clause: 38[0:Inp] || -> RigidHistory(skf1(U,V,W,X,Y))*. Given clause: 44[0:Inp] || Leq3(U,V,W)* -> Leq(V,W). Given clause: 43[0:Inp] || Leq3(U,V,W)* -> Leq(U,V). Given clause: 42[0:Inp] || SkP2(U,V,W,X)* -> History(U). Given clause: 41[0:Inp] || SkP2(U,V,W,X)* -> History(V). Given clause: 45[0:Inp] Region(U) Region(V) || -> Region(RUnion(V,U))*. Given clause: 48[0:Inp] || Leq(U,V)* -> equal(U,V) Lt(U,V). Given clause: 53[0:Inp] || PersistentCavity(U,V,W,X) -> NoEntranceCavity(U,V,W,X)*. Given clause: 52[0:Inp] || PersistentCavity(U,V,W,X)* -> NoExitCavity(U,V,W,X). Given clause: 50[0:Inp] || NoEntranceCavity(U,V,W,X) -> SkP2(X,W,V,U)*. Given clause: 83[0:Res:50.1,41.0] || NoEntranceCavity(U,V,W,X)* -> History(W). Given clause: 84[0:Res:50.1,42.0] || NoEntranceCavity(U,V,W,X)* -> History(X). Given clause: 85[0:Res:53.1,83.0] || PersistentCavity(U,V,W,X)* -> History(W). Given clause: 86[0:Res:53.1,84.0] || PersistentCavity(U,V,W,X)* -> History(X). Given clause: 49[0:Inp] || NoExitCavity(U,V,W,X) -> SkP2(X,W,V,U)*. Given clause: 87[0:Res:49.1,41.0] || NoExitCavity(U,V,W,X)* -> History(W). Given clause: 88[0:Res:49.1,42.0] || NoExitCavity(U,V,W,X)* -> History(X). Given clause: 51[0:Inp] || PersistentCavity(U,V,W,X) -> SkP2(X,W,V,U)*. Given clause: 54[0:Inp] || Leq(U,V) Leq(V,W) -> Leq3(U,V,W)*. Given clause: 55[0:Inp] || equal(Slice(Ta1,U),Rc1) NoExitCavity(Ta1,Tb1,U,HPlace(Ob1))* -> . Given clause: 56[0:Inp] || NoEntranceCavity(U,V,W,X)* NoExitCavity(U,V,W,X) -> PersistentCavity(U,V,W,X). Given clause: 57[0:Inp] RigidHistory(U) || Cavity(V,Slice(W,U)) Leq3(X,W,Y) -> equal(Slice(W,skf1(W,V,U,Y,X)),V)**. Given clause: 58[0:Inp] RigidHistory(U) || Cavity(V,Slice(W,U)) Leq3(X,W,Y) -> PersistentCavity(X,Y,skf1(W,V,U,Y,X),U)*. Given clause: 97[0:Res:58.3,85.0] RigidHistory(U) || Cavity(V,Slice(W,U)) Leq3(X,W,Y) -> History(skf1(W,V,U,Y,X))*. Given clause: 98[0:Res:58.3,52.0] RigidHistory(U) || Cavity(V,Slice(W,U)) Leq3(X,W,Y) -> NoExitCavity(X,Y,skf1(W,V,U,Y,X),U)*. Given clause: 102[0:SSi:101.0,1.0] || Cavity(U,Slice(V,HPlace(Ob1))) Leq3(Ta1,V,Tb1) equal(Slice(Ta1,skf1(V,U,HPlace(Ob1),Tb1,Ta1)),Rc1)** -> . Given clause: 105[0:SSi:104.0,1.0] || Cavity(U,Slice(Ta1,HPlace(Ob1)))* Leq3(Ta1,Ta1,Tb1) equal(U,Rc1) -> . Given clause: 107[0:Obv:106.1] || Leq3(Ta1,Ta1,Tb1)* -> . Given clause: 108[0:Res:54.2,107.0] || Leq(Ta1,Ta1) Leq(Ta1,Tb1)* -> . Given clause: 111[0:MRR:109.0,2.0] || Leq(Ta1,Ta1)* -> . SPASS V 3.7 SPASS beiseite: Proof found. Problem: Scenario1_Part2.txt SPASS derived 48 clauses, backtracked 0 clauses, performed 0 splits and kept 92 clauses. SPASS allocated 52316 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 7, length 23 : 1[0:Inp] || -> RigidHistory(HPlace(Ob1))*. 2[0:Inp] || -> Lt(Ta1,Tb1)*. 17[0:Inp] || -> Cavity(Rc1,Slice(Ta1,HPlace(Ob1)))*. 36[0:Inp] || Lt(U,V) -> Leq(U,V)*. 37[0:Inp] || equal(U,V) -> Leq(U,V)*. 52[0:Inp] || PersistentCavity(U,V,W,X)* -> NoExitCavity(U,V,W,X). 54[0:Inp] || Leq(U,V) Leq(V,W) -> Leq3(U,V,W)*. 55[0:Inp] || equal(Slice(Ta1,U),Rc1) NoExitCavity(Ta1,Tb1,U,HPlace(Ob1))* -> . 57[0:Inp] RigidHistory(U) || Cavity(V,Slice(W,U)) Leq3(X,W,Y) -> equal(Slice(W,skf1(W,V,U,Y,X)),V)**. 58[0:Inp] RigidHistory(U) || Cavity(V,Slice(W,U)) Leq3(X,W,Y) -> PersistentCavity(X,Y,skf1(W,V,U,Y,X),U)*. 98[0:Res:58.3,52.0] RigidHistory(U) || Cavity(V,Slice(W,U)) Leq3(X,W,Y) -> NoExitCavity(X,Y,skf1(W,V,U,Y,X),U)*. 101[0:Res:98.3,55.1] RigidHistory(HPlace(Ob1)) || Cavity(U,Slice(V,HPlace(Ob1))) Leq3(Ta1,V,Tb1) equal(Slice(Ta1,skf1(V,U,HPlace(Ob1),Tb1,Ta1)),Rc1)** -> . 102[0:SSi:101.0,1.0] || Cavity(U,Slice(V,HPlace(Ob1))) Leq3(Ta1,V,Tb1) equal(Slice(Ta1,skf1(V,U,HPlace(Ob1),Tb1,Ta1)),Rc1)** -> . 103[0:SpL:57.3,102.2] RigidHistory(HPlace(Ob1)) || Cavity(U,Slice(Ta1,HPlace(Ob1)))* Leq3(Ta1,Ta1,Tb1) Cavity(U,Slice(Ta1,HPlace(Ob1)))* Leq3(Ta1,Ta1,Tb1) equal(U,Rc1) -> . 104[0:Obv:103.2] RigidHistory(HPlace(Ob1)) || Cavity(U,Slice(Ta1,HPlace(Ob1)))* Leq3(Ta1,Ta1,Tb1) equal(U,Rc1) -> . 105[0:SSi:104.0,1.0] || Cavity(U,Slice(Ta1,HPlace(Ob1)))* Leq3(Ta1,Ta1,Tb1) equal(U,Rc1) -> . 106[0:Res:17.0,105.0] || Leq3(Ta1,Ta1,Tb1)* equal(Rc1,Rc1) -> . 107[0:Obv:106.1] || Leq3(Ta1,Ta1,Tb1)* -> . 108[0:Res:54.2,107.0] || Leq(Ta1,Ta1) Leq(Ta1,Tb1)* -> . 109[0:Res:36.1,108.1] || Lt(Ta1,Tb1) Leq(Ta1,Ta1)* -> . 111[0:MRR:109.0,2.0] || Leq(Ta1,Ta1)* -> . 113[0:Res:37.1,111.0] || equal(Ta1,Ta1)* -> . 114[0:Obv:113.0] || -> . Formulae used in the proof : axiom17 axiom20 axiom18 axiom21 axiom19 axiom22 conjecture0 axiom23 --------------------------SPASS-STOP------------------------------