--------------------------SPASS-START----------------------------- Input Problem: 1[0:Inp] || -> RigidObject(Ob2b)*. 2[0:Inp] || -> Ordered(Ta2,Tb2)*. 3[0:Inp] || RigidObject(U) -> Object(U)*. 4[0:Inp] || RigidHistory(U) -> History(U)*. 5[0:Inp] || -> CContained(Ta2,Os2,Singleton(Ob2a))*. 6[0:Inp] || -> CContained(Ta2,Ob2a,Singleton(Ob2b))*. 7[0:Inp] || CContained(Tb2,Os2,Singleton(Ob2b))* -> . 8[0:Inp] || Lt(U,V)* -> Time(U). 9[0:Inp] || Lt(U,V)* -> Time(V). 10[0:Inp] || Leq(U,V)* -> Time(U). 11[0:Inp] || Leq(U,V)* -> Time(V). 12[0:Inp] || Ordered(U,V)* -> Time(U). 13[0:Inp] || Ordered(U,V)* -> Time(V). 14[0:Inp] || SkP0(U,V)* -> Region(V). 15[0:Inp] || SkP0(U,V)* -> Region(U). 16[0:Inp] || SkP1(U,V)* -> Region(V). 17[0:Inp] || SkP1(U,V)* -> Region(U). 18[0:Inp] || Object(U) -> ObjectSet(Singleton(U))*. 19[0:Inp] || Object(U) -> History(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] || Contained(U,V) -> SkP1(V,U)*. 28[0:Inp] || Cavity(U,V) -> SkP1(V,U)*. 29[0:Inp] || Outside(U,V) -> SkP1(V,U)*. 30[0:Inp] || OSPlace(U,V,W)* -> Time(U). 31[0:Inp] || OSPlace(U,V,W)* -> ObjectSet(V). 32[0:Inp] || OSPlace(U,V,W)* -> Region(W). 33[0:Inp] || ClosedContainer(U,V,W)* -> Time(U). 34[0:Inp] || ClosedContainer(U,V,W)* -> ObjectSet(V). 35[0:Inp] || ClosedContainer(U,V,W)* -> Region(W). 36[0:Inp] || CContained(U,V,W)* -> Time(U). 37[0:Inp] || CContained(U,V,W)* -> Object(V). 38[0:Inp] || CContained(U,V,W)* -> ObjectSet(W). 39[0:Inp] || Region(U) Region(V) -> Region(RUnion(U,V))*. 40[0:Inp] || Time(U) Object(V) -> Region(Place(U,V))*. 41[0:Inp] || Time(U) History(V) -> Region(Slice(U,V))*. 42[0:Inp] || Contained(U,V)* Contained(V,W)* -> Contained(U,W)*. 43[0:Inp] || CContained(U,V,Singleton(W))* RigidObject(W) Ordered(U,X)* -> CContained(X,V,Singleton(W))*. 44[0:Inp] || Contained(Place(U,V),Place(U,W))* Time(U) Object(V) Object(W) -> CContained(U,V,Singleton(W)). 45[0:Inp] || CContained(U,V,Singleton(W)) Time(U) Object(V) Object(W) -> Contained(Place(U,V),Place(U,W))*. This is a first-order Horn problem without equality. This is a problem that contains sort information. The conjecture is ground. The following monadic predicates have finite extensions: RigidObject. Axiom clauses: 44 Conjecture clauses: 1 Inferences: IEmS=1 ISoR=1 IORe=1 Reductions: RFMRR=1 RBMRR=1 RObv=1 RUnC=1 RTaut=1 RSST=1 RSSi=1 RFSub=1 RBSub=1 RCon=1 Extras : Input Saturation, Dynamic Selection, No Splitting, Full Reduction, Ratio: 5, FuncWeight: 1, VarWeight: 1 Precedence: Singleton > HPlace > RUnion > Place > Slice > ObjectSet > Region > History > SkP1 > Object > Contained > CContained > Time > RigidObject > Ordered > Lt > Leq > Leq3 > SkP0 > P > Cavity > OSPlace > ClosedContainer > RigidHistory > O > EC > DR > Outside > Os2 > Ob2a > Ob2b > Ta2 > Tb2 Ordering : KBO Processed Problem: Worked Off Clauses: Usable Clauses: 1[0:Inp] || -> RigidObject(Ob2b)*. 2[0:Inp] || -> Ordered(Ta2,Tb2)*. 6[0:Inp] || -> CContained(Ta2,Ob2a,Singleton(Ob2b))*. 5[0:Inp] || -> CContained(Ta2,Os2,Singleton(Ob2a))*. 4[0:Inp] RigidHistory(U) || -> History(U)*. 3[0:Inp] RigidObject(U) || -> Object(U)*. 7[0:Inp] || CContained(Tb2,Os2,Singleton(Ob2b))* -> . 19[0:Inp] Object(U) || -> History(HPlace(U))*. 18[0:Inp] Object(U) || -> ObjectSet(Singleton(U))*. 17[0:Inp] || SkP1(U,V)* -> Region(U). 16[0:Inp] || SkP1(U,V)* -> Region(V). 15[0:Inp] || SkP0(U,V)* -> Region(U). 14[0:Inp] || SkP0(U,V)* -> Region(V). 11[0:Inp] || Leq(U,V)* -> Time(V). 10[0:Inp] || Leq(U,V)* -> Time(U). 9[0:Inp] || Lt(U,V)* -> Time(V). 8[0:Inp] || Lt(U,V)* -> Time(U). 13[0:Inp] || Ordered(U,V)* -> Time(V). 12[0:Inp] || Ordered(U,V)* -> Time(U). 29[0:Inp] || Outside(U,V) -> SkP1(V,U)*. 28[0:Inp] || Cavity(U,V) -> SkP1(V,U)*. 27[0:Inp] || Contained(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)*. 34[0:Inp] || ClosedContainer(U,V,W)* -> ObjectSet(V). 31[0:Inp] || OSPlace(U,V,W)* -> ObjectSet(V). 38[0:Inp] || CContained(U,V,W)* -> ObjectSet(W). 37[0:Inp] || CContained(U,V,W)* -> Object(V). 35[0:Inp] || ClosedContainer(U,V,W)* -> Region(W). 32[0:Inp] || OSPlace(U,V,W)* -> Region(W). 33[0:Inp] || ClosedContainer(U,V,W)* -> Time(U). 30[0:Inp] || OSPlace(U,V,W)* -> Time(U). 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). 36[0:Inp] || CContained(U,V,W)* -> Time(U). 39[0:Inp] Region(U) Region(V) || -> Region(RUnion(V,U))*. 41[0:Inp] History(U) Time(V) || -> Region(Slice(V,U))*. 40[0:Inp] Object(U) Time(V) || -> Region(Place(V,U))*. 49[0:MRR:47.0,1.0] || Ordered(U,Tb2) CContained(U,Os2,Singleton(Ob2b))* -> . 42[0:Inp] || Contained(U,V)* Contained(W,U)* -> Contained(W,V)*. 46[0:MRR:45.0,45.1,36.1,37.1] Object(U) || CContained(V,W,Singleton(U)) -> Contained(Place(V,W),Place(V,U))*. 48[0:Res:44.4,7.0] Object(Ob2b) Object(Os2) Time(Tb2) || Contained(Place(Tb2,Os2),Place(Tb2,Ob2b))* -> . 43[0:Inp] RigidObject(U) || Ordered(V,W)* CContained(V,X,Singleton(U))* -> CContained(W,X,Singleton(U))*. 44[0:Inp] Object(U) Object(V) Time(W) || Contained(Place(W,V),Place(W,U))* -> CContained(W,V,Singleton(U)). Given clause: 1[0:Inp] || -> RigidObject(Ob2b)*. Given clause: 2[0:Inp] || -> Ordered(Ta2,Tb2)*. Given clause: 6[0:Inp] || -> CContained(Ta2,Ob2a,Singleton(Ob2b))*. Given clause: 5[0:Inp] || -> CContained(Ta2,Os2,Singleton(Ob2a))*. Given clause: 4[0:Inp] RigidHistory(U) || -> History(U)*. Given clause: 3[0:Inp] RigidObject(U) || -> Object(U)*. Given clause: 7[0:Inp] || CContained(Tb2,Os2,Singleton(Ob2b))* -> . Given clause: 19[0:Inp] Object(U) || -> History(HPlace(U))*. Given clause: 18[0:Inp] Object(U) || -> ObjectSet(Singleton(U))*. Given clause: 17[0:Inp] || SkP1(U,V)* -> Region(U). Given clause: 16[0:Inp] || SkP1(U,V)* -> Region(V). Given clause: 15[0:Inp] || SkP0(U,V)* -> Region(U). Given clause: 14[0:Inp] || SkP0(U,V)* -> Region(V). Given clause: 11[0:Inp] || Leq(U,V)* -> Time(V). Given clause: 10[0:Inp] || Leq(U,V)* -> Time(U). Given clause: 9[0:Inp] || Lt(U,V)* -> Time(V). Given clause: 8[0:Inp] || Lt(U,V)* -> Time(U). Given clause: 13[0:Inp] || Ordered(U,V)* -> Time(V). Given clause: 80[0:Res:2.0,13.0] || -> Time(Tb2)*. Given clause: 12[0:Inp] || Ordered(U,V)* -> Time(U). Given clause: 83[0:Res:2.0,12.0] || -> Time(Ta2)*. Given clause: 29[0:Inp] || Outside(U,V) -> SkP1(V,U)*. Given clause: 84[0:Res:29.1,16.0] || Outside(U,V)* -> Region(U). Given clause: 85[0:Res:29.1,17.0] || Outside(U,V)* -> Region(V). Given clause: 28[0:Inp] || Cavity(U,V) -> SkP1(V,U)*. Given clause: 86[0:Res:28.1,16.0] || Cavity(U,V)* -> Region(U). Given clause: 87[0:Res:28.1,17.0] || Cavity(U,V)* -> Region(V). Given clause: 27[0:Inp] || Contained(U,V) -> SkP1(V,U)*. Given clause: 88[0:Res:27.1,16.0] || Contained(U,V)* -> Region(U). Given clause: 26[0:Inp] || DR(U,V) -> SkP0(V,U)*. Given clause: 89[0:Res:27.1,17.0] || Contained(U,V)* -> Region(V). Given clause: 90[0:Res:26.1,14.0] || DR(U,V)* -> Region(U). Given clause: 91[0:Res:26.1,15.0] || DR(U,V)* -> Region(V). Given clause: 25[0:Inp] || EC(U,V) -> SkP0(V,U)*. Given clause: 24[0:Inp] || O(U,V) -> SkP0(V,U)*. Given clause: 92[0:Res:25.1,14.0] || EC(U,V)* -> Region(U). Given clause: 93[0:Res:25.1,15.0] || EC(U,V)* -> Region(V). Given clause: 94[0:Res:24.1,14.0] || O(U,V)* -> Region(U). Given clause: 95[0:Res:24.1,15.0] || O(U,V)* -> Region(V). Given clause: 23[0:Inp] || P(U,V) -> SkP0(V,U)*. Given clause: 96[0:Res:23.1,14.0] || P(U,V)* -> Region(U). Given clause: 97[0:Res:23.1,15.0] || P(U,V)* -> Region(V). Given clause: 34[0:Inp] || ClosedContainer(U,V,W)* -> ObjectSet(V). Given clause: 31[0:Inp] || OSPlace(U,V,W)* -> ObjectSet(V). Given clause: 38[0:Inp] || CContained(U,V,W)* -> ObjectSet(W). Given clause: 98[0:Res:6.0,38.0] || -> ObjectSet(Singleton(Ob2b))*. Given clause: 99[0:Res:5.0,38.0] || -> ObjectSet(Singleton(Ob2a))*. Given clause: 37[0:Inp] || CContained(U,V,W)* -> Object(V). Given clause: 100[0:Res:6.0,37.0] || -> Object(Ob2a)*. Given clause: 35[0:Inp] || ClosedContainer(U,V,W)* -> Region(W). Given clause: 101[0:Res:5.0,37.0] || -> Object(Os2)*. Given clause: 32[0:Inp] || OSPlace(U,V,W)* -> Region(W). Given clause: 33[0:Inp] || ClosedContainer(U,V,W)* -> Time(U). Given clause: 30[0:Inp] || OSPlace(U,V,W)* -> Time(U). 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: 36[0:Inp] || CContained(U,V,W)* -> Time(U). Given clause: 102[0:MRR:82.0,101.0] || Contained(Place(Tb2,Os2),Place(Tb2,Ob2b))* -> . Given clause: 39[0:Inp] Region(U) Region(V) || -> Region(RUnion(V,U))*. Given clause: 49[0:MRR:47.0,1.0] || Ordered(U,Tb2) CContained(U,Os2,Singleton(Ob2b))* -> . Given clause: 41[0:Inp] History(U) Time(V) || -> Region(Slice(V,U))*. Given clause: 40[0:Inp] Object(U) Time(V) || -> Region(Place(V,U))*. Given clause: 42[0:Inp] || Contained(U,V)*+ Contained(W,U)* -> Contained(W,V)*. Given clause: 46[0:MRR:45.0,45.1,36.1,37.1] Object(U) || CContained(V,W,Singleton(U)) -> Contained(Place(V,W),Place(V,U))*. Given clause: 106[0:Res:46.2,89.0] Object(U) || CContained(V,W,Singleton(U))* -> Region(Place(V,U)). Given clause: 111[0:SSi:109.0,3.0,1.1] || -> Region(Place(Ta2,Ob2b))*. Given clause: 112[0:SSi:110.0,100.0] || -> Region(Place(Ta2,Ob2a))*. Given clause: 107[0:Res:46.2,88.0] Object(U) || CContained(V,W,Singleton(U))* -> Region(Place(V,W)). Given clause: 43[0:Inp] RigidObject(U) || Ordered(V,W)* CContained(V,X,Singleton(U))*+ -> CContained(W,X,Singleton(U))*. Given clause: 115[0:SSi:114.0,100.0] || -> Region(Place(Ta2,Os2))*. Given clause: 118[0:SSi:116.0,1.0] || Ordered(Ta2,U) -> CContained(U,Ob2a,Singleton(Ob2b))*. Given clause: 125[0:SSi:119.0,3.0,1.1] || Ordered(Ta2,U) -> Region(Place(U,Ob2a))*. Given clause: 126[0:SSi:120.0,3.0,1.1] || Ordered(Ta2,U) -> Region(Place(U,Ob2b))*. Given clause: 44[0:Inp] Object(U) Object(V) Time(W) || Contained(Place(W,V),Place(W,U))* -> CContained(W,V,Singleton(U)). Given clause: 127[0:SSi:121.0,1.0] || Ordered(Ta2,U)*+ Ordered(U,V)* -> CContained(V,Ob2a,Singleton(Ob2b))*. Given clause: 129[0:Res:2.0,127.0] || Ordered(Tb2,U) -> CContained(U,Ob2a,Singleton(Ob2b))*. Given clause: 136[0:SSi:130.0,3.0,1.1] || Ordered(Tb2,U) -> Region(Place(U,Ob2a))*. Given clause: 137[0:SSi:131.0,3.0,1.1] || Ordered(Tb2,U) -> Region(Place(U,Ob2b))*. Given clause: 105[0:Res:46.2,42.0] Object(U) || CContained(V,W,Singleton(U))*+ Contained(X,Place(V,W))* -> Contained(X,Place(V,U))*. Given clause: 143[0:SSi:139.0,3.0,1.1] || Contained(U,Place(Ta2,Ob2a))* -> Contained(U,Place(Ta2,Ob2b)). Given clause: 144[0:SSi:140.0,100.0] || Contained(U,Place(Ta2,Os2))* -> Contained(U,Place(Ta2,Ob2a)). Given clause: 148[0:SSi:147.0,100.0] || CContained(Ta2,U,Singleton(Ob2a)) -> Contained(Place(Ta2,U),Place(Ta2,Ob2b))*. Given clause: 153[0:Res:148.1,88.0] || CContained(Ta2,U,Singleton(Ob2a))* -> Region(Place(Ta2,U)). Given clause: 146[0:SSi:142.0,3.0,1.1] || Ordered(Ta2,U) Contained(V,Place(U,Ob2a))* -> Contained(V,Place(U,Ob2b)). Given clause: 156[0:MRR:155.0,37.1] || CContained(Ta2,U,Singleton(Ob2a))* -> CContained(Ta2,U,Singleton(Ob2b)). Given clause: 160[0:Res:5.0,156.0] || -> CContained(Ta2,Os2,Singleton(Ob2b))*. SPASS V 3.7 SPASS beiseite: Proof found. Problem: inference2.dfg SPASS derived 71 clauses, backtracked 0 clauses, performed 0 splits and kept 97 clauses. SPASS allocated 52341 KBytes. SPASS spent 0:00:00.05 on the problem. 0:00:00.02 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 6, length 29 : 1[0:Inp] || -> RigidObject(Ob2b)*. 2[0:Inp] || -> Ordered(Ta2,Tb2)*. 3[0:Inp] RigidObject(U) || -> Object(U)*. 5[0:Inp] || -> CContained(Ta2,Os2,Singleton(Ob2a))*. 6[0:Inp] || -> CContained(Ta2,Ob2a,Singleton(Ob2b))*. 7[0:Inp] || CContained(Tb2,Os2,Singleton(Ob2b))* -> . 12[0:Inp] || Ordered(U,V)* -> Time(U). 36[0:Inp] || CContained(U,V,W)* -> Time(U). 37[0:Inp] || CContained(U,V,W)* -> Object(V). 42[0:Inp] || Contained(U,V)*+ Contained(W,U)* -> Contained(W,V)*. 43[0:Inp] RigidObject(U) || Ordered(V,W)* CContained(V,X,Singleton(U))*+ -> CContained(W,X,Singleton(U))*. 44[0:Inp] Object(U) Object(V) Time(W) || Contained(Place(W,V),Place(W,U))* -> CContained(W,V,Singleton(U)). 45[0:Inp] Time(U) Object(V) Object(W) || CContained(U,V,Singleton(W)) -> Contained(Place(U,V),Place(U,W))*. 46[0:MRR:45.0,45.1,36.1,37.1] Object(U) || CContained(V,W,Singleton(U)) -> Contained(Place(V,W),Place(V,U))*. 47[0:Res:43.3,7.0] RigidObject(Ob2b) || CContained(U,Os2,Singleton(Ob2b))* Ordered(U,Tb2) -> . 49[0:MRR:47.0,1.0] || Ordered(U,Tb2) CContained(U,Os2,Singleton(Ob2b))* -> . 83[0:Res:2.0,12.0] || -> Time(Ta2)*. 100[0:Res:6.0,37.0] || -> Object(Ob2a)*. 105[0:Res:46.2,42.0] Object(U) || CContained(V,W,Singleton(U))*+ Contained(X,Place(V,W))* -> Contained(X,Place(V,U))*. 139[0:Res:6.0,105.1] Object(Ob2b) || Contained(U,Place(Ta2,Ob2a))* -> Contained(U,Place(Ta2,Ob2b)). 143[0:SSi:139.0,3.0,1.1] || Contained(U,Place(Ta2,Ob2a))* -> Contained(U,Place(Ta2,Ob2b)). 147[0:Res:46.2,143.0] Object(Ob2a) || CContained(Ta2,U,Singleton(Ob2a)) -> Contained(Place(Ta2,U),Place(Ta2,Ob2b))*. 148[0:SSi:147.0,100.0] || CContained(Ta2,U,Singleton(Ob2a)) -> Contained(Place(Ta2,U),Place(Ta2,Ob2b))*. 154[0:Res:148.1,44.3] Object(Ob2b) Object(U) Time(Ta2) || CContained(Ta2,U,Singleton(Ob2a))* -> CContained(Ta2,U,Singleton(Ob2b)). 155[0:SSi:154.2,154.0,83.0,3.1,1.0] Object(U) || CContained(Ta2,U,Singleton(Ob2a))* -> CContained(Ta2,U,Singleton(Ob2b)). 156[0:MRR:155.0,37.1] || CContained(Ta2,U,Singleton(Ob2a))* -> CContained(Ta2,U,Singleton(Ob2b)). 160[0:Res:5.0,156.0] || -> CContained(Ta2,Os2,Singleton(Ob2b))*. 161[0:Res:160.0,49.1] || Ordered(Ta2,Tb2)* -> . 169[0:MRR:161.0,2.0] || -> . Formulae used in the proof : C2A1 C2A4 axiom14 C2A2 C2A3 conjecture0 axiom2 axiom11 SCA1 Lem2E Lem2B --------------------------SPASS-STOP------------------------------