--------------------------SPASS-START----------------------------- Input Problem: 1[0:Inp] || -> Region(skc1)*. 2[0:Inp] || -> Action(StandStill)*. 3[0:Inp] || -> Time(Ta5)*. 4[0:Inp] || -> Time(Tb5)*. 5[0:Inp] || -> Object(Ob5)*. 6[0:Inp] || -> Object(Ol5)*. 7[0:Inp] || -> Region(Rc5)*. 8[0:Inp] || -> Object(Os5)*. 9[0:Inp] || -> History(Hu)*. 10[0:Inp] || -> History(Hc)*. 11[0:Inp] || -> Time(Tm)*. 12[0:Inp] || -> Object(Oa)*. 13[0:Inp] || -> Time(Tx)*. 14[0:Inp] || -> Object(Agent)*. 15[0:Inp] || -> ObjectSet(Su)*. 16[0:Inp] || P(skc1,skc1)* -> . 17[0:Inp] || SmallObject(U) -> Object(U)*. 18[0:Inp] || IntConn(U) -> Region(U)*. 19[0:Inp] || AllStable(U) -> Time(U)*. 20[0:Inp] || EmptyHanded(U) -> Time(U)*. 21[0:Inp] || RigidObject(U) -> Object(U)*. 22[0:Inp] || Region(U) -> Region(ConvexHull(U))*. 23[0:Inp] || Object(U) -> ObjectSet(Singleton(U))*. 24[0:Inp] || Region(U) -> Action(TravelTo(U))*. 25[0:Inp] || Object(U) -> History(HPlace(U))*. 26[0:Inp] || SkP0(U,V)* -> Time(V). 27[0:Inp] || SkP0(U,V)* -> Time(U). 28[0:Inp] || Feasible(U,V)* -> Time(U). 29[0:Inp] || Feasible(U,V)* -> Action(V). 30[0:Inp] || Element(U,V)* -> Object(U). 31[0:Inp] || Element(U,V)* -> ObjectSet(V). 32[0:Inp] || FeasiblePlace(U,V)* -> Object(U). 33[0:Inp] || FeasiblePlace(U,V)* -> Region(V). 34[0:Inp] || SkP2(U,V)* -> ObjectSet(V). 35[0:Inp] || SkP2(U,V)* -> Region(U). 36[0:Inp] || OMuchSmaller(U,V)* -> Object(U). 37[0:Inp] || OMuchSmaller(U,V)* -> Region(V). 38[0:Inp] || SafelyMovable(U,V)* -> Time(U). 39[0:Inp] || SafelyMovable(U,V)* -> Object(V). 40[0:Inp] || FullyOutside(U,V)* -> Region(U). 41[0:Inp] || FullyOutside(U,V)* -> Region(V). 42[0:Inp] || Reachable(U,V)* -> Time(U). 43[0:Inp] || Reachable(U,V)* -> Region(V). 44[0:Inp] || SkP4(U,V)* -> Region(V). 45[0:Inp] || SkP4(U,V)* -> Region(U). 46[0:Inp] || SkP5(U,V)* -> Region(V). 47[0:Inp] || SkP5(U,V)* -> Region(U). 48[0:Inp] || SkP6(U,V)* -> Region(V). 49[0:Inp] || SkP6(U,V)* -> Region(U). 50[0:Inp] || MuchSmaller(U,V)* -> Region(U). 51[0:Inp] || MuchSmaller(U,V)* -> Region(V). 52[0:Inp] || Stable(U,V)* -> Time(U). 53[0:Inp] || Stable(U,V)* -> Object(V). 54[0:Inp] || NoPartialContents(U,V)* -> Time(U). 55[0:Inp] || NoPartialContents(U,V)* -> Object(V). 56[0:Inp] || CanGrasp(U,V)* -> Time(U). 57[0:Inp] || CanGrasp(U,V)* -> Object(V). 58[0:Inp] || Grasp(U,V)* -> Time(U). 59[0:Inp] || Grasp(U,V)* -> Object(V). 60[0:Inp] || Graspable(U,V)* -> Time(U). 61[0:Inp] || Graspable(U,V)* -> Object(V). 62[0:Inp] || Lt(U,V) -> SkP0(V,U)*. 63[0:Inp] || Leq(U,V) -> SkP0(V,U)*. 64[0:Inp] || Leq3(U,V,W)* -> Time(U). 65[0:Inp] || Leq3(U,V,W)* -> Time(V). 66[0:Inp] || Leq3(U,V,W)* -> Time(W). 67[0:Inp] || Occurs(U,V,W)* -> Time(U). 68[0:Inp] || Occurs(U,V,W)* -> Time(V). 69[0:Inp] || Occurs(U,V,W)* -> Action(W). 70[0:Inp] || OSPlace(U,V,W)* -> Time(U). 71[0:Inp] || OSPlace(U,V,W)* -> ObjectSet(V). 72[0:Inp] || OSPlace(U,V,W)* -> Region(W). 73[0:Inp] || UprightContainer(U,V,W)* -> Time(U). 74[0:Inp] || UprightContainer(U,V,W)* -> Object(V). 75[0:Inp] || UprightContainer(U,V,W)* -> Region(W). 76[0:Inp] || SkP1(U,V,W)* -> Time(W). 77[0:Inp] || SkP1(U,V,W)* -> Object(V). 78[0:Inp] || SkP1(U,V,W)* -> Object(U). 79[0:Inp] || Fits(U,V) -> SkP2(V,U)*. 80[0:Inp] || SmallSet(U,V) -> SkP2(V,U)*. 81[0:Inp] || Isolates(U,V,W)* -> Time(U). 82[0:Inp] || Isolates(U,V,W)* -> ObjectSet(V). 83[0:Inp] || Isolates(U,V,W)* -> ObjectSet(W). 84[0:Inp] || BoxedIn(U,V,W)* -> Time(U). 85[0:Inp] || BoxedIn(U,V,W)* -> Object(V). 86[0:Inp] || BoxedIn(U,V,W)* -> Object(W). 87[0:Inp] || SkP3(U,V,W)* -> Time(W). 88[0:Inp] || SkP3(U,V,W)* -> Time(V). 89[0:Inp] || SkP3(U,V,W)* -> Object(U). 90[0:Inp] || DR(U,V) -> SkP4(V,U)*. 91[0:Inp] || EC(U,V) -> SkP4(V,U)*. 92[0:Inp] || C(U,V) -> SkP4(V,U)*. 93[0:Inp] || P(U,V) -> SkP4(V,U)*. 94[0:Inp] || O(U,V) -> SkP4(V,U)*. 95[0:Inp] || OV(U,V) -> SkP4(V,U)*. 96[0:Inp] || OpenContained(U,V) -> SkP5(V,U)*. 97[0:Inp] || FullyOutside(U,V) -> SkP5(V,U)*. 98[0:Inp] || OpenContainerShape(U,V) -> SkP5(V,U)*. 99[0:Inp] || UprightContainerShape(U,V) -> SkP5(V,U)*. 100[0:Inp] || Cavity(U,V) -> SkP6(V,U)*. 101[0:Inp] || PartiallyContained(U,V) -> SkP6(V,U)*. 102[0:Inp] || CombinedContainer(U,V,W)* -> Region(U). 103[0:Inp] || CombinedContainer(U,V,W)* -> Region(V). 104[0:Inp] || CombinedContainer(U,V,W)* -> Region(W). 105[0:Inp] || Moves(U,V,W)* -> Time(U). 106[0:Inp] || Moves(U,V,W)* -> Time(V). 107[0:Inp] || Moves(U,V,W)* -> Object(W). 108[0:Inp] || SkP7(U,V,W)* -> Time(W). 109[0:Inp] || SkP7(U,V,W)* -> Time(V). 110[0:Inp] || SkP7(U,V,W)* -> Object(U). 111[0:Inp] || SkP8(U,V,W)* -> Time(W). 112[0:Inp] || SkP8(U,V,W)* -> Time(V). 113[0:Inp] || SkP8(U,V,W)* -> ObjectSet(U). 114[0:Inp] || Grasps(U,V,W)* -> Time(U). 115[0:Inp] || Grasps(U,V,W)* -> Time(V). 116[0:Inp] || Grasps(U,V,W)* -> Object(W). 117[0:Inp] || Constant(U,V,W)* -> Time(U). 118[0:Inp] || Constant(U,V,W)* -> Time(V). 119[0:Inp] || Constant(U,V,W)* -> History(W). 120[0:Inp] || SkP9(U,V,W)* -> Time(W). 121[0:Inp] || SkP9(U,V,W)* -> Time(V). 122[0:Inp] || SkP9(U,V,W)* -> History(U). 123[0:Inp] || BoxWithLid(U,V,W)* -> Time(U). 124[0:Inp] || BoxWithLid(U,V,W)* -> Object(V). 125[0:Inp] || BoxWithLid(U,V,W)* -> Object(W). 126[0:Inp] || SafeManipulate(U,V,W,X)* -> Time(U). 127[0:Inp] || SafeManipulate(U,V,W,X)* -> Time(V). 128[0:Inp] || SafeManipulate(U,V,W,X)* -> Object(W). 129[0:Inp] || SafeManipulate(U,V,W,X)* -> Region(X). 130[0:Inp] || SkP10(U,V,W,X)* -> Time(X). 131[0:Inp] || SkP10(U,V,W,X)* -> Time(W). 132[0:Inp] || SkP10(U,V,W,X)* -> History(V). 133[0:Inp] || SkP10(U,V,W,X)* -> History(U). 134[0:Inp] || DynamicUContainer(U,V,W,X)* -> Time(U). 135[0:Inp] || DynamicUContainer(U,V,W,X)* -> Time(V). 136[0:Inp] || DynamicUContainer(U,V,W,X)* -> Object(W). 137[0:Inp] || DynamicUContainer(U,V,W,X)* -> History(X). 138[0:Inp] || BoxWithLidC(U,V,W,X)* -> Time(U). 139[0:Inp] || BoxWithLidC(U,V,W,X)* -> Object(V). 140[0:Inp] || BoxWithLidC(U,V,W,X)* -> Object(W). 141[0:Inp] || BoxWithLidC(U,V,W,X)* -> Region(X). 142[0:Inp] || Leq3(U,V,W)* -> Leq(U,V). 143[0:Inp] || Leq3(U,V,W)* -> Leq(V,W). 144[0:Inp] || CContained(U,V,W) -> SkP1(W,V,U)*. 145[0:Inp] || UContained(U,V,W) -> SkP1(W,V,U)*. 146[0:Inp] || BLContained(U,V,W) -> SkP1(W,V,U)*. 147[0:Inp] || PreserveCContents(U,V,W) -> SkP3(W,V,U)*. 148[0:Inp] || PreserveUContents(U,V,W) -> SkP3(W,V,U)*. 149[0:Inp] || PreserveBoxWithLid(U,V,W) -> SkP3(W,V,U)*. 150[0:Inp] || StableThroughout(U,V,W) -> SkP7(W,V,U)*. 151[0:Inp] || Released(U,V,W) -> SkP7(W,V,U)*. 152[0:Inp] || Motionless(U,V,W) -> SkP7(W,V,U)*. 153[0:Inp] || CausallyIsolated(U,V,W) -> SkP8(W,V,U)*. 154[0:Inp] || StaticCausallyIsolated(U,V,W) -> SkP8(W,V,U)*. 155[0:Inp] || AlwaysIntConn(U,V,W) -> SkP9(W,V,U)*. 156[0:Inp] || Continuous(U,V,W) -> SkP9(W,V,U)*. 157[0:Inp] || Action(U) Action(V) -> Action(Sequence(U,V))*. 158[0:Inp] || Region(U) Region(V) -> Region(RUnion(U,V))*. 159[0:Inp] || Object(U) Object(V) -> ObjectSet(Pair(U,V))*. 160[0:Inp] || ObjectSet(U) ObjectSet(V) -> ObjectSet(Union(U,V))*. 161[0:Inp] || Time(U) Object(V) -> Region(Place(U,V))*. 162[0:Inp] || Time(U) Region(V) -> ObjectSet(Contents(U,V))*. 163[0:Inp] || Time(U) ObjectSet(V) -> ObjectSet(CContents(U,V))*. 164[0:Inp] || Time(U) ObjectSet(V) -> ObjectSet(UContents(U,V))*. 165[0:Inp] || Object(U) Region(V) -> Action(ManipTo(U,V))*. 166[0:Inp] || Time(U) History(V) -> Region(Slice(U,V))*. 167[0:Inp] || History(U) History(V) -> History(HUnion(U,V))*. 168[0:Inp] || Time(U) Object(V) -> ObjectSet(MovingGroup(U,V))*. 169[0:Inp] || Object(U) Object(V) -> Action(PutInUC(U,V))*. 170[0:Inp] || Object(U) Object(V) -> Action(LoadUprightContainer(U,V))*. 171[0:Inp] || PersistentCavity(U,V,W,X) -> SkP10(X,W,V,U)*. 172[0:Inp] || NoExitCavity(U,V,W,X) -> SkP10(X,W,V,U)*. 173[0:Inp] || NoEntranceCavity(U,V,W,X) -> SkP10(X,W,V,U)*. 174[0:Inp] || Lt(U,V)* Lt(V,W)* -> Lt(U,W)*. 175[0:Inp] || Leq(U,V) Leq(W,U) -> Leq3(W,U,V)*. 176[0:Inp] || Lt(U,V) Time(U) Time(V) -> Leq(U,V)*. 177[0:Inp] || equal(U,V) Time(U) Time(V) -> Leq(U,V)*. 178[0:Inp] || Region(U) Region(V) -> C(skf1(U,W),U)* P(U,V)*. 179[0:Inp] || C(skf1(U,V),V)* Region(U) Region(V) -> P(U,V). 180[0:Inp] || Leq(U,V)* Time(U) Time(V) -> Lt(U,V) equal(U,V). 181[0:Inp] || P(U,V)* C(W,U)* Region(U) Region(V) -> C(W,V)*. This is a first-order Non-Horn problem containing equality. This is a problem that contains sort information. All equations are many sorted. The conjecture is ground. Axiom clauses: 179 Conjecture clauses: 2 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 RSST=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 > LoadUprightContainer > PutInUC > MovingGroup > HUnion > Slice > ManipTo > UContents > CContents > Union > Pair > RUnion > Place > Contents > Sequence > HPlace > TravelTo > Singleton > ConvexHull > ObjectSet > Action > SkP4 > C > P > Region > SkP0 > Leq3 > Leq > Lt > Time > History > Object > UprightContainer > SkP5 > FullyOutside > SkP2 > SmallSet > AllStable > EmptyHanded > Graspable > Reachable > SafelyMovable > SmallObject > BoxedIn > NoPartialContents > Occurs > CanGrasp > UprightContainerShape > SkP1 > UContained > Element > SkP7 > Motionless > Released > Grasp > Moves > Feasible > SafeManipulate > SkP6 > PartiallyContained > OSPlace > SkP3 > PreserveCContents > PreserveUContents > PreserveBoxWithLid > Stable > StableThroughout > Fits > MuchSmaller > OMuchSmaller > OpenContainerShape > OpenContained > CContained > BLContained > DynamicUContainer > O > Cavity > Constant > Grasps > FeasiblePlace > OV > BoxWithLidC > BoxWithLid > CombinedContainer > EC > SkP10 > PersistentCavity > NoExitCavity > NoEntranceCavity > DR > SkP9 > Continuous > AlwaysIntConn > IntConn > Isolates > ClosedContainer > SkP8 > CausallyIsolated > StaticCausallyIsolated > RigidObject > skc3 > skc2 > skc1 > skc0 > Su > Tx > Oa > Tm > Hc > Hu > Tb5 > Os5 > Rc5 > Ol5 > Ob5 > Ta5 > Rc1 > Ra4 > Tm2 > Tb > Ra1 > Tm1 > Agent > Ox4 > Rc4 > Ob4 > Ta4 > StandStill Ordering : KBO Processed Problem: Worked Off Clauses: Usable Clauses: 10[0:Inp] || -> History(Hc)*. 9[0:Inp] || -> History(Hu)*. 2[0:Inp] || -> Action(StandStill)*. 15[0:Inp] || -> ObjectSet(Su)*. 14[0:Inp] || -> Object(Agent)*. 12[0:Inp] || -> Object(Oa)*. 8[0:Inp] || -> Object(Os5)*. 6[0:Inp] || -> Object(Ol5)*. 5[0:Inp] || -> Object(Ob5)*. 7[0:Inp] || -> Region(Rc5)*. 1[0:Inp] || -> Region(skc1)*. 13[0:Inp] || -> Time(Tx)*. 11[0:Inp] || -> Time(Tm)*. 4[0:Inp] || -> Time(Tb5)*. 3[0:Inp] || -> Time(Ta5)*. 187[0:Res:1.0,24.0] || -> Action(TravelTo(skc1))*. 186[0:Res:1.0,22.0] || -> Region(ConvexHull(skc1))*. 16[0:Inp] || P(skc1,skc1)* -> . 21[0:Inp] RigidObject(U) || -> Object(U)*. 17[0:Inp] SmallObject(U) || -> Object(U)*. 18[0:Inp] IntConn(U) || -> Region(U)*. 20[0:Inp] EmptyHanded(U) || -> Time(U)*. 19[0:Inp] AllStable(U) || -> Time(U)*. 197[0:MRR:196.0,1.0] || -> C(skf1(skc1,U),skc1)*. 25[0:Inp] Object(U) || -> History(HPlace(U))*. 24[0:Inp] Region(U) || -> Action(TravelTo(U))*. 23[0:Inp] Object(U) || -> ObjectSet(Singleton(U))*. 22[0:Inp] Region(U) || -> Region(ConvexHull(U))*. 29[0:Inp] || Feasible(U,V)* -> Action(V). 31[0:Inp] || Element(U,V)* -> ObjectSet(V). 34[0:Inp] || SkP2(U,V)* -> ObjectSet(V). 61[0:Inp] || Graspable(U,V)* -> Object(V). 59[0:Inp] || Grasp(U,V)* -> Object(V). 57[0:Inp] || CanGrasp(U,V)* -> Object(V). 55[0:Inp] || NoPartialContents(U,V)* -> Object(V). 53[0:Inp] || Stable(U,V)* -> Object(V). 39[0:Inp] || SafelyMovable(U,V)* -> Object(V). 36[0:Inp] || OMuchSmaller(U,V)* -> Object(U). 32[0:Inp] || FeasiblePlace(U,V)* -> Object(U). 30[0:Inp] || Element(U,V)* -> Object(U). 51[0:Inp] || MuchSmaller(U,V)* -> Region(V). 50[0:Inp] || MuchSmaller(U,V)* -> Region(U). 43[0:Inp] || Reachable(U,V)* -> Region(V). 37[0:Inp] || OMuchSmaller(U,V)* -> Region(V). 33[0:Inp] || FeasiblePlace(U,V)* -> Region(V). 41[0:Inp] || FullyOutside(U,V)* -> Region(V). 40[0:Inp] || FullyOutside(U,V)* -> Region(U). 49[0:Inp] || SkP6(U,V)* -> Region(U). 48[0:Inp] || SkP6(U,V)* -> Region(V). 35[0:Inp] || SkP2(U,V)* -> Region(U). 47[0:Inp] || SkP5(U,V)* -> Region(U). 46[0:Inp] || SkP5(U,V)* -> Region(V). 45[0:Inp] || SkP4(U,V)* -> Region(U). 44[0:Inp] || SkP4(U,V)* -> Region(V). 60[0:Inp] || Graspable(U,V)* -> Time(U). 58[0:Inp] || Grasp(U,V)* -> Time(U). 56[0:Inp] || CanGrasp(U,V)* -> Time(U). 54[0:Inp] || NoPartialContents(U,V)* -> Time(U). 52[0:Inp] || Stable(U,V)* -> Time(U). 42[0:Inp] || Reachable(U,V)* -> Time(U). 38[0:Inp] || SafelyMovable(U,V)* -> Time(U). 28[0:Inp] || Feasible(U,V)* -> Time(U). 27[0:Inp] || SkP0(U,V)* -> Time(U). 26[0:Inp] || SkP0(U,V)* -> Time(V). 101[0:Inp] || PartiallyContained(U,V) -> SkP6(V,U)*. 100[0:Inp] || Cavity(U,V) -> SkP6(V,U)*. 80[0:Inp] || SmallSet(U,V) -> SkP2(V,U)*. 79[0:Inp] || Fits(U,V) -> SkP2(V,U)*. 62[0:Inp] || Lt(U,V) -> SkP0(V,U)*. 63[0:Inp] || Leq(U,V) -> SkP0(V,U)*. 99[0:Inp] || UprightContainerShape(U,V) -> SkP5(V,U)*. 98[0:Inp] || OpenContainerShape(U,V) -> SkP5(V,U)*. 96[0:Inp] || OpenContained(U,V) -> SkP5(V,U)*. 97[0:Inp] || FullyOutside(U,V) -> SkP5(V,U)*. 95[0:Inp] || OV(U,V) -> SkP4(V,U)*. 94[0:Inp] || O(U,V) -> SkP4(V,U)*. 91[0:Inp] || EC(U,V) -> SkP4(V,U)*. 90[0:Inp] || DR(U,V) -> SkP4(V,U)*. 93[0:Inp] || P(U,V) -> SkP4(V,U)*. 92[0:Inp] || C(U,V) -> SkP4(V,U)*. 119[0:Inp] || Constant(U,V,W)* -> History(W). 69[0:Inp] || Occurs(U,V,W)* -> Action(W). 122[0:Inp] || SkP9(U,V,W)* -> History(U). 83[0:Inp] || Isolates(U,V,W)* -> ObjectSet(W). 82[0:Inp] || Isolates(U,V,W)* -> ObjectSet(V). 71[0:Inp] || OSPlace(U,V,W)* -> ObjectSet(V). 113[0:Inp] || SkP8(U,V,W)* -> ObjectSet(U). 125[0:Inp] || BoxWithLid(U,V,W)* -> Object(W). 124[0:Inp] || BoxWithLid(U,V,W)* -> Object(V). 116[0:Inp] || Grasps(U,V,W)* -> Object(W). 107[0:Inp] || Moves(U,V,W)* -> Object(W). 86[0:Inp] || BoxedIn(U,V,W)* -> Object(W). 85[0:Inp] || BoxedIn(U,V,W)* -> Object(V). 74[0:Inp] || UprightContainer(U,V,W)* -> Object(V). 110[0:Inp] || SkP7(U,V,W)* -> Object(U). 89[0:Inp] || SkP3(U,V,W)* -> Object(U). 78[0:Inp] || SkP1(U,V,W)* -> Object(U). 77[0:Inp] || SkP1(U,V,W)* -> Object(V). 104[0:Inp] || CombinedContainer(U,V,W)* -> Region(W). 103[0:Inp] || CombinedContainer(U,V,W)* -> Region(V). 102[0:Inp] || CombinedContainer(U,V,W)* -> Region(U). 75[0:Inp] || UprightContainer(U,V,W)* -> Region(W). 72[0:Inp] || OSPlace(U,V,W)* -> Region(W). 123[0:Inp] || BoxWithLid(U,V,W)* -> Time(U). 118[0:Inp] || Constant(U,V,W)* -> Time(V). 117[0:Inp] || Constant(U,V,W)* -> Time(U). 115[0:Inp] || Grasps(U,V,W)* -> Time(V). 114[0:Inp] || Grasps(U,V,W)* -> Time(U). 106[0:Inp] || Moves(U,V,W)* -> Time(V). 105[0:Inp] || Moves(U,V,W)* -> Time(U). 84[0:Inp] || BoxedIn(U,V,W)* -> Time(U). 81[0:Inp] || Isolates(U,V,W)* -> Time(U). 73[0:Inp] || UprightContainer(U,V,W)* -> Time(U). 70[0:Inp] || OSPlace(U,V,W)* -> Time(U). 68[0:Inp] || Occurs(U,V,W)* -> Time(V). 67[0:Inp] || Occurs(U,V,W)* -> Time(U). 121[0:Inp] || SkP9(U,V,W)* -> Time(V). 120[0:Inp] || SkP9(U,V,W)* -> Time(W). 112[0:Inp] || SkP8(U,V,W)* -> Time(V). 111[0:Inp] || SkP8(U,V,W)* -> Time(W). 109[0:Inp] || SkP7(U,V,W)* -> Time(V). 108[0:Inp] || SkP7(U,V,W)* -> Time(W). 88[0:Inp] || SkP3(U,V,W)* -> Time(V). 87[0:Inp] || SkP3(U,V,W)* -> Time(W). 76[0:Inp] || SkP1(U,V,W)* -> Time(W). 66[0:Inp] || Leq3(U,V,W)* -> Time(W). 65[0:Inp] || Leq3(U,V,W)* -> Time(V). 64[0:Inp] || Leq3(U,V,W)* -> Time(U). 185[0:Res:1.0,158.0] Region(U) || -> Region(RUnion(skc1,U))*. 193[0:Res:1.0,165.1] Object(U) || -> Action(ManipTo(U,skc1))*. 192[0:Res:1.0,162.1] Time(U) || -> ObjectSet(Contents(U,skc1))*. 191[0:Res:1.0,158.1] Region(U) || -> Region(RUnion(U,skc1))*. 143[0:Inp] || Leq3(U,V,W)* -> Leq(V,W). 142[0:Inp] || Leq3(U,V,W)* -> Leq(U,V). 137[0:Inp] || DynamicUContainer(U,V,W,X)* -> History(X). 133[0:Inp] || SkP10(U,V,W,X)* -> History(U). 132[0:Inp] || SkP10(U,V,W,X)* -> History(V). 140[0:Inp] || BoxWithLidC(U,V,W,X)* -> Object(W). 139[0:Inp] || BoxWithLidC(U,V,W,X)* -> Object(V). 136[0:Inp] || DynamicUContainer(U,V,W,X)* -> Object(W). 128[0:Inp] || SafeManipulate(U,V,W,X)* -> Object(W). 141[0:Inp] || BoxWithLidC(U,V,W,X)* -> Region(X). 129[0:Inp] || SafeManipulate(U,V,W,X)* -> Region(X). 138[0:Inp] || BoxWithLidC(U,V,W,X)* -> Time(U). 135[0:Inp] || DynamicUContainer(U,V,W,X)* -> Time(V). 134[0:Inp] || DynamicUContainer(U,V,W,X)* -> Time(U). 127[0:Inp] || SafeManipulate(U,V,W,X)* -> Time(V). 126[0:Inp] || SafeManipulate(U,V,W,X)* -> Time(U). 131[0:Inp] || SkP10(U,V,W,X)* -> Time(W). 130[0:Inp] || SkP10(U,V,W,X)* -> Time(X). 156[0:Inp] || Continuous(U,V,W) -> SkP9(W,V,U)*. 155[0:Inp] || AlwaysIntConn(U,V,W) -> SkP9(W,V,U)*. 154[0:Inp] || StaticCausallyIsolated(U,V,W) -> SkP8(W,V,U)*. 153[0:Inp] || CausallyIsolated(U,V,W) -> SkP8(W,V,U)*. 152[0:Inp] || Motionless(U,V,W) -> SkP7(W,V,U)*. 151[0:Inp] || Released(U,V,W) -> SkP7(W,V,U)*. 150[0:Inp] || StableThroughout(U,V,W) -> SkP7(W,V,U)*. 149[0:Inp] || PreserveBoxWithLid(U,V,W) -> SkP3(W,V,U)*. 148[0:Inp] || PreserveUContents(U,V,W) -> SkP3(W,V,U)*. 147[0:Inp] || PreserveCContents(U,V,W) -> SkP3(W,V,U)*. 146[0:Inp] || BLContained(U,V,W) -> SkP1(W,V,U)*. 145[0:Inp] || UContained(U,V,W) -> SkP1(W,V,U)*. 144[0:Inp] || CContained(U,V,W) -> SkP1(W,V,U)*. 167[0:Inp] History(U) History(V) || -> History(HUnion(V,U))*. 157[0:Inp] Action(U) Action(V) || -> Action(Sequence(V,U))*. 170[0:Inp] Object(U) Object(V) || -> Action(LoadUprightContainer(V,U))*. 169[0:Inp] Object(U) Object(V) || -> Action(PutInUC(V,U))*. 165[0:Inp] Region(U) Object(V) || -> Action(ManipTo(V,U))*. 160[0:Inp] ObjectSet(U) ObjectSet(V) || -> ObjectSet(Union(V,U))*. 159[0:Inp] Object(U) Object(V) || -> ObjectSet(Pair(V,U))*. 164[0:Inp] ObjectSet(U) Time(V) || -> ObjectSet(UContents(V,U))*. 163[0:Inp] ObjectSet(U) Time(V) || -> ObjectSet(CContents(V,U))*. 168[0:Inp] Object(U) Time(V) || -> ObjectSet(MovingGroup(V,U))*. 162[0:Inp] Region(U) Time(V) || -> ObjectSet(Contents(V,U))*. 158[0:Inp] Region(U) Region(V) || -> Region(RUnion(V,U))*. 166[0:Inp] History(U) Time(V) || -> Region(Slice(V,U))*. 161[0:Inp] Object(U) Time(V) || -> Region(Place(V,U))*. 174[0:Inp] || Lt(U,V)* Lt(W,U)* -> Lt(W,V)*. 173[0:Inp] || NoEntranceCavity(U,V,W,X) -> SkP10(X,W,V,U)*. 172[0:Inp] || NoExitCavity(U,V,W,X) -> SkP10(X,W,V,U)*. 171[0:Inp] || PersistentCavity(U,V,W,X) -> SkP10(X,W,V,U)*. 190[0:Res:1.0,178.1] Region(U) || -> P(U,skc1) C(skf1(U,V),U)*. 175[0:Inp] || Leq(U,V) Leq(V,W) -> Leq3(U,V,W)*. 183[0:Res:1.0,179.0] Region(U) || C(skf1(skc1,U),U)* -> P(skc1,U). 189[0:Res:1.0,179.1] Region(U) || C(skf1(U,skc1),skc1)* -> P(U,skc1). 176[0:Inp] Time(U) Time(V) || Lt(V,U) -> Leq(V,U)*. 177[0:Inp] Time(U) Time(V) || equal(V,U) -> Leq(V,U)*. 178[0:Inp] Region(U) Region(V) || -> P(V,U)* C(skf1(V,W),V)*. 188[0:Res:1.0,181.1] Region(U) || C(V,U)* P(U,skc1) -> C(V,skc1)*. 182[0:Res:1.0,181.0] Region(U) || C(V,skc1)* P(skc1,U) -> C(V,U)*. 179[0:Inp] Region(U) Region(V) || C(skf1(V,U),U)* -> P(V,U). 180[0:Inp] Time(U) Time(V) || Leq(V,U)* -> equal(V,U) Lt(V,U). 181[0:Inp] Region(U) Region(V) || C(W,V)* P(V,U)* -> C(W,U)*. SPASS V 3.5 SPASS beiseite: Proof found. Problem: sb.dfg SPASS derived 14 clauses, backtracked 0 clauses, performed 0 splits and kept 193 clauses. SPASS allocated 55790 KBytes. SPASS spent 0:00:00.05 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 1, length 10 : 1[0:Inp] || -> Region(skc1)*. 16[0:Inp] || P(skc1,skc1)* -> . 178[0:Inp] Region(U) Region(V) || -> P(V,U)* C(skf1(V,W),V)*. 179[0:Inp] Region(U) Region(V) || C(skf1(V,U),U)* -> P(V,U). 194[0:Res:179.3,16.0] Region(skc1) Region(skc1) || C(skf1(skc1,skc1),skc1)* -> . 195[0:Res:178.3,16.0] Region(skc1) Region(skc1) || -> C(skf1(skc1,U),skc1)*. 196[0:Obv:195.0] Region(skc1) || -> C(skf1(skc1,U),skc1)*. 197[0:MRR:196.0,1.0] || -> C(skf1(skc1,U),skc1)*. 198[0:Obv:194.0] Region(skc1) || C(skf1(skc1,skc1),skc1)* -> . 199[0:MRR:198.0,198.1,1.0,197.0] || -> . Formulae used in the proof : LemSB SBD1 --------------------------SPASS-STOP------------------------------