--------------------------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] || -> RigidHistory(skf1(U,V,W,X))*. 19[0:Inp] || Leq3(U,V,W)* -> Time(U). 20[0:Inp] || Leq3(U,V,W)* -> Time(V). 21[0:Inp] || Leq3(U,V,W)* -> Time(W). 22[0:Inp] || P(U,V) -> SkP0(V,U)*. 23[0:Inp] || O(U,V) -> SkP0(V,U)*. 24[0:Inp] || EC(U,V) -> SkP0(V,U)*. 25[0:Inp] || DR(U,V) -> SkP0(V,U)*. 26[0:Inp] || Cavity(U,V) -> SkP1(V,U)*. 27[0:Inp] || Outside(U,V) -> SkP1(V,U)*. 28[0:Inp] || OSPlace(U,V,W)* -> Time(U). 29[0:Inp] || OSPlace(U,V,W)* -> ObjectSet(V). 30[0:Inp] || OSPlace(U,V,W)* -> Region(W). 31[0:Inp] || ClosedContainer(U,V,W)* -> Time(U). 32[0:Inp] || ClosedContainer(U,V,W)* -> ObjectSet(V). 33[0:Inp] || ClosedContainer(U,V,W)* -> Region(W). 34[0:Inp] || CContained(U,V,W)* -> Time(U). 35[0:Inp] || CContained(U,V,W)* -> Object(V). 36[0:Inp] || CContained(U,V,W)* -> ObjectSet(W). 37[0:Inp] || SkP2(U,V,W,X)* -> Time(X). 38[0:Inp] || SkP2(U,V,W,X)* -> Time(W). 39[0:Inp] || SkP2(U,V,W,X)* -> History(V). 40[0:Inp] || SkP2(U,V,W,X)* -> History(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] || NoExitCavity(U,V,W,X) -> SkP2(X,W,V,U)*. 45[0:Inp] || NoEntranceCavity(U,V,W,X) -> SkP2(X,W,V,U)*. 46[0:Inp] || PersistentCavity(U,V,W,X) -> SkP2(X,W,V,U)*. 47[0:Inp] || PersistentCavity(U,V,W,X)* -> NoExitCavity(U,V,W,X). 48[0:Inp] || PersistentCavity(U,V,W,X) -> NoEntranceCavity(U,V,W,X)*. 49[0:Inp] || PersistentCavity(U,V,W,X)* -> NoExitCavity(U,V,W,X). 50[0:Inp] || equal(Slice(Ta1,U),Rc1) NoExitCavity(Ta1,Tb1,U,HPlace(Ob1))* -> . 51[0:Inp] || NoExitCavity(U,V,W,X) NoEntranceCavity(U,V,W,X)* -> PersistentCavity(U,V,W,X). 52[0:Inp] || Cavity(U,Slice(V,W)) RigidHistory(W) Lt(V,X) -> equal(Slice(V,skf1(U,W,X,V)),U)**. 53[0:Inp] || Cavity(U,Slice(V,W)) RigidHistory(W) Lt(V,X) -> PersistentCavity(V,X,skf1(U,W,X,V),W)*. This is a first-order Horn problem containing equality. This is a problem that contains sort information. 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=1 RCon=1 Extras : Input Saturation, Dynamic Selection, No 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 > Lt > Leq > Leq3 > 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). 8[0:Inp] || Leq(U,V)* -> Time(V). 7[0:Inp] || Leq(U,V)* -> Time(U). 6[0:Inp] || Lt(U,V)* -> Time(V). 5[0:Inp] || Lt(U,V)* -> Time(U). 18[0:Inp] || -> RigidHistory(skf1(U,V,W,X))*. 27[0:Inp] || Outside(U,V) -> SkP1(V,U)*. 26[0:Inp] || Cavity(U,V) -> SkP1(V,U)*. 25[0:Inp] || DR(U,V) -> SkP0(V,U)*. 24[0:Inp] || EC(U,V) -> SkP0(V,U)*. 23[0:Inp] || O(U,V) -> SkP0(V,U)*. 22[0:Inp] || P(U,V) -> SkP0(V,U)*. 36[0:Inp] || CContained(U,V,W)* -> ObjectSet(W). 32[0:Inp] || ClosedContainer(U,V,W)* -> ObjectSet(V). 29[0:Inp] || OSPlace(U,V,W)* -> ObjectSet(V). 35[0:Inp] || CContained(U,V,W)* -> Object(V). 33[0:Inp] || ClosedContainer(U,V,W)* -> Region(W). 30[0:Inp] || OSPlace(U,V,W)* -> Region(W). 34[0:Inp] || CContained(U,V,W)* -> Time(U). 31[0:Inp] || ClosedContainer(U,V,W)* -> Time(U). 28[0:Inp] || OSPlace(U,V,W)* -> Time(U). 21[0:Inp] || Leq3(U,V,W)* -> Time(W). 20[0:Inp] || Leq3(U,V,W)* -> Time(V). 19[0:Inp] || Leq3(U,V,W)* -> Time(U). 40[0:Inp] || SkP2(U,V,W,X)* -> History(U). 39[0:Inp] || SkP2(U,V,W,X)* -> History(V). 38[0:Inp] || SkP2(U,V,W,X)* -> Time(W). 37[0:Inp] || SkP2(U,V,W,X)* -> Time(X). 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))*. 48[0:Inp] || PersistentCavity(U,V,W,X) -> NoEntranceCavity(U,V,W,X)*. 49[0:Inp] || PersistentCavity(U,V,W,X)* -> NoExitCavity(U,V,W,X). 45[0:Inp] || NoEntranceCavity(U,V,W,X) -> SkP2(X,W,V,U)*. 44[0:Inp] || NoExitCavity(U,V,W,X) -> SkP2(X,W,V,U)*. 46[0:Inp] || PersistentCavity(U,V,W,X) -> SkP2(X,W,V,U)*. 50[0:Inp] || equal(Slice(Ta1,U),Rc1) NoExitCavity(Ta1,Tb1,U,HPlace(Ob1))* -> . 51[0:Inp] || NoEntranceCavity(U,V,W,X)* NoExitCavity(U,V,W,X) -> PersistentCavity(U,V,W,X). 53[0:Inp] RigidHistory(U) || Lt(V,W) Cavity(X,Slice(V,U)) -> PersistentCavity(V,W,skf1(X,U,W,V),U)*. 52[0:Inp] RigidHistory(U) || Lt(V,W) Cavity(X,Slice(V,U)) -> equal(Slice(V,skf1(X,U,W,V)),X)**. 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: 8[0:Inp] || Leq(U,V)* -> Time(V). Given clause: 7[0:Inp] || Leq(U,V)* -> Time(U). Given clause: 6[0:Inp] || Lt(U,V)* -> Time(V). Given clause: 54[0:Res:2.0,6.0] || -> Time(Tb1)*. Given clause: 5[0:Inp] || Lt(U,V)* -> Time(U). Given clause: 55[0:Res:2.0,5.0] || -> Time(Ta1)*. Given clause: 18[0:Inp] || -> RigidHistory(skf1(U,V,W,X))*. Given clause: 27[0:Inp] || Outside(U,V) -> SkP1(V,U)*. Given clause: 56[0:Res:27.1,13.0] || Outside(U,V)* -> Region(U). Given clause: 57[0:Res:27.1,14.0] || Outside(U,V)* -> Region(V). Given clause: 26[0:Inp] || Cavity(U,V) -> SkP1(V,U)*. Given clause: 25[0:Inp] || DR(U,V) -> SkP0(V,U)*. Given clause: 58[0:Res:26.1,13.0] || Cavity(U,V)* -> Region(U). Given clause: 62[0:Res:17.0,58.0] || -> Region(Rc1)*. Given clause: 59[0:Res:26.1,14.0] || Cavity(U,V)* -> Region(V). Given clause: 63[0:Res:17.0,59.0] || -> Region(Slice(Ta1,HPlace(Ob1)))*. Given clause: 24[0:Inp] || EC(U,V) -> SkP0(V,U)*. Given clause: 60[0:Res:25.1,11.0] || DR(U,V)* -> Region(U). Given clause: 61[0:Res:25.1,12.0] || DR(U,V)* -> Region(V). Given clause: 64[0:Res:24.1,11.0] || EC(U,V)* -> Region(U). Given clause: 65[0:Res:24.1,12.0] || EC(U,V)* -> Region(V). Given clause: 23[0:Inp] || O(U,V) -> SkP0(V,U)*. Given clause: 66[0:Res:23.1,11.0] || O(U,V)* -> Region(U). Given clause: 67[0:Res:23.1,12.0] || O(U,V)* -> Region(V). Given clause: 22[0:Inp] || P(U,V) -> SkP0(V,U)*. Given clause: 68[0:Res:22.1,11.0] || P(U,V)* -> Region(U). Given clause: 36[0:Inp] || CContained(U,V,W)* -> ObjectSet(W). Given clause: 69[0:Res:22.1,12.0] || P(U,V)* -> Region(V). Given clause: 32[0:Inp] || ClosedContainer(U,V,W)* -> ObjectSet(V). Given clause: 29[0:Inp] || OSPlace(U,V,W)* -> ObjectSet(V). Given clause: 35[0:Inp] || CContained(U,V,W)* -> Object(V). Given clause: 33[0:Inp] || ClosedContainer(U,V,W)* -> Region(W). Given clause: 30[0:Inp] || OSPlace(U,V,W)* -> Region(W). Given clause: 34[0:Inp] || CContained(U,V,W)* -> Time(U). Given clause: 31[0:Inp] || ClosedContainer(U,V,W)* -> Time(U). Given clause: 28[0:Inp] || OSPlace(U,V,W)* -> Time(U). Given clause: 21[0:Inp] || Leq3(U,V,W)* -> Time(W). Given clause: 20[0:Inp] || Leq3(U,V,W)* -> Time(V). Given clause: 19[0:Inp] || Leq3(U,V,W)* -> Time(U). Given clause: 40[0:Inp] || SkP2(U,V,W,X)* -> History(U). Given clause: 39[0:Inp] || SkP2(U,V,W,X)* -> History(V). Given clause: 38[0:Inp] || SkP2(U,V,W,X)* -> Time(W). Given clause: 37[0:Inp] || SkP2(U,V,W,X)* -> Time(X). 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: 48[0:Inp] || PersistentCavity(U,V,W,X) -> NoEntranceCavity(U,V,W,X)*. Given clause: 49[0:Inp] || PersistentCavity(U,V,W,X)* -> NoExitCavity(U,V,W,X). Given clause: 45[0:Inp] || NoEntranceCavity(U,V,W,X) -> SkP2(X,W,V,U)*. Given clause: 70[0:Res:45.1,37.0] || NoEntranceCavity(U,V,W,X)* -> Time(U). Given clause: 71[0:Res:45.1,38.0] || NoEntranceCavity(U,V,W,X)* -> Time(V). Given clause: 44[0:Inp] || NoExitCavity(U,V,W,X) -> SkP2(X,W,V,U)*. Given clause: 72[0:Res:45.1,39.0] || NoEntranceCavity(U,V,W,X)* -> History(W). Given clause: 73[0:Res:45.1,40.0] || NoEntranceCavity(U,V,W,X)* -> History(X). Given clause: 74[0:Res:48.1,70.0] || PersistentCavity(U,V,W,X)* -> Time(U). Given clause: 75[0:Res:48.1,71.0] || PersistentCavity(U,V,W,X)* -> Time(V). Given clause: 46[0:Inp] || PersistentCavity(U,V,W,X) -> SkP2(X,W,V,U)*. Given clause: 76[0:Res:44.1,37.0] || NoExitCavity(U,V,W,X)* -> Time(U). Given clause: 77[0:Res:44.1,38.0] || NoExitCavity(U,V,W,X)* -> Time(V). Given clause: 78[0:Res:44.1,39.0] || NoExitCavity(U,V,W,X)* -> History(W). Given clause: 79[0:Res:44.1,40.0] || NoExitCavity(U,V,W,X)* -> History(X). Given clause: 50[0:Inp] || equal(Slice(Ta1,U),Rc1) NoExitCavity(Ta1,Tb1,U,HPlace(Ob1))* -> . Given clause: 80[0:Res:48.1,72.0] || PersistentCavity(U,V,W,X)* -> History(W). Given clause: 81[0:Res:48.1,73.0] || PersistentCavity(U,V,W,X)* -> History(X). Given clause: 51[0:Inp] || NoEntranceCavity(U,V,W,X)* NoExitCavity(U,V,W,X) -> PersistentCavity(U,V,W,X). Given clause: 52[0:Inp] RigidHistory(U) || Lt(V,W) Cavity(X,Slice(V,U)) -> equal(Slice(V,skf1(X,U,W,V)),X)**. Given clause: 53[0:Inp] RigidHistory(U) || Lt(V,W) Cavity(X,Slice(V,U)) -> PersistentCavity(V,W,skf1(X,U,W,V),U)*. Given clause: 90[0:Res:53.3,80.0] RigidHistory(U) || Lt(V,W) Cavity(X,Slice(V,U)) -> History(skf1(X,U,W,V))*. Given clause: 93[0:Res:53.3,49.0] RigidHistory(U) || Lt(V,W) Cavity(X,Slice(V,U)) -> NoExitCavity(V,W,skf1(X,U,W,V),U)*. Given clause: 101[0:MRR:100.0,2.0] || Cavity(U,Slice(Ta1,HPlace(Ob1)))* equal(U,Rc1) -> . SPASS V 3.7 SPASS beiseite: Proof found. Problem: C:\Users\ang\Documents\Courant\Case1-Piece2.dfg SPASS derived 46 clauses, backtracked 0 clauses, performed 0 splits and kept 84 clauses. SPASS allocated 30127 KBytes. SPASS spent 0:00:00.14 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 3, length 14 : 1[0:Inp] || -> RigidHistory(HPlace(Ob1))*. 2[0:Inp] || -> Lt(Ta1,Tb1)*. 17[0:Inp] || -> Cavity(Rc1,Slice(Ta1,HPlace(Ob1)))*. 49[0:Inp] || PersistentCavity(U,V,W,X)* -> NoExitCavity(U,V,W,X). 50[0:Inp] || equal(Slice(Ta1,U),Rc1) NoExitCavity(Ta1,Tb1,U,HPlace(Ob1))* -> . 52[0:Inp] RigidHistory(U) || Lt(V,W) Cavity(X,Slice(V,U)) -> equal(Slice(V,skf1(X,U,W,V)),X)**. 53[0:Inp] RigidHistory(U) || Lt(V,W) Cavity(X,Slice(V,U)) -> PersistentCavity(V,W,skf1(X,U,W,V),U)*. 93[0:Res:53.3,49.0] RigidHistory(U) || Lt(V,W) Cavity(X,Slice(V,U)) -> NoExitCavity(V,W,skf1(X,U,W,V),U)*. 98[0:Res:93.3,50.1] RigidHistory(HPlace(Ob1)) || Lt(Ta1,Tb1) Cavity(U,Slice(Ta1,HPlace(Ob1))) equal(Slice(Ta1,skf1(U,HPlace(Ob1),Tb1,Ta1)),Rc1)** -> . 99[0:Rew:52.3,98.3] RigidHistory(HPlace(Ob1)) || Lt(Ta1,Tb1) Cavity(U,Slice(Ta1,HPlace(Ob1)))* equal(U,Rc1) -> . 100[0:SSi:99.0,1.0] || Lt(Ta1,Tb1) Cavity(U,Slice(Ta1,HPlace(Ob1)))* equal(U,Rc1) -> . 101[0:MRR:100.0,2.0] || Cavity(U,Slice(Ta1,HPlace(Ob1)))* equal(U,Rc1) -> . 102[0:Res:17.0,101.0] || equal(Rc1,Rc1)* -> . 103[0:Obv:102.0] || -> . Formulae used in the proof : axiom18 axiom21 axiom19 axiom20 conjecture0 axiom22 --------------------------SPASS-STOP------------------------------