--------------------------SPASS-START----------------------------- Input Problem: 1[0:Inp] || -> Action(StandStill)*. 2[0:Inp] || -> Region(Ra)*. 3[0:Inp] || -> Region(Rb)*. 4[0:Inp] || -> Region(Rc)*. 5[0:Inp] || -> DR(skc3,skc5)*. 6[0:Inp] || -> DR(skc3,skc4)*. 7[0:Inp] || SmallObject(U) -> Object(U)*. 8[0:Inp] || IntConn(U) -> Region(U)*. 9[0:Inp] || AllStable(U) -> Time(U)*. 10[0:Inp] || EmptyHanded(U) -> Time(U)*. 11[0:Inp] || RigidObject(U) -> Object(U)*. 12[0:Inp] || DR(skc3,RUnion(skc5,skc4))* -> . 13[0:Inp] || Region(U) -> Region(ConvexHull(U))*. 14[0:Inp] || Object(U) -> ObjectSet(Singleton(U))*. 15[0:Inp] || Region(U) -> Action(TravelTo(U))*. 16[0:Inp] || Object(U) -> History(HPlace(U))*. 17[0:Inp] || SkP0(U,V)* -> Time(V). 18[0:Inp] || SkP0(U,V)* -> Time(U). 19[0:Inp] || Feasible(U,V)* -> Time(U). 20[0:Inp] || Feasible(U,V)* -> Action(V). 21[0:Inp] || Element(U,V)* -> Object(U). 22[0:Inp] || Element(U,V)* -> ObjectSet(V). 23[0:Inp] || FeasiblePlace(U,V)* -> Object(U). 24[0:Inp] || FeasiblePlace(U,V)* -> Region(V). 25[0:Inp] || SkP2(U,V)* -> ObjectSet(V). 26[0:Inp] || SkP2(U,V)* -> Region(U). 27[0:Inp] || OMuchSmaller(U,V)* -> Object(U). 28[0:Inp] || OMuchSmaller(U,V)* -> Region(V). 29[0:Inp] || SafelyMovable(U,V)* -> Time(U). 30[0:Inp] || SafelyMovable(U,V)* -> Object(V). 31[0:Inp] || FullyOutside(U,V)* -> Region(U). 32[0:Inp] || FullyOutside(U,V)* -> Region(V). 33[0:Inp] || Reachable(U,V)* -> Time(U). 34[0:Inp] || Reachable(U,V)* -> Region(V). 35[0:Inp] || SkP4(U,V)* -> Region(V). 36[0:Inp] || SkP4(U,V)* -> Region(U). 37[0:Inp] || SkP5(U,V)* -> Region(V). 38[0:Inp] || SkP5(U,V)* -> Region(U). 39[0:Inp] || SkP6(U,V)* -> Region(V). 40[0:Inp] || SkP6(U,V)* -> Region(U). 41[0:Inp] || MuchSmaller(U,V)* -> Region(U). 42[0:Inp] || MuchSmaller(U,V)* -> Region(V). 43[0:Inp] || Stable(U,V)* -> Time(U). 44[0:Inp] || Stable(U,V)* -> Object(V). 45[0:Inp] || NoPartialContents(U,V)* -> Time(U). 46[0:Inp] || NoPartialContents(U,V)* -> Object(V). 47[0:Inp] || CanGrasp(U,V)* -> Time(U). 48[0:Inp] || CanGrasp(U,V)* -> Object(V). 49[0:Inp] || Grasp(U,V)* -> Time(U). 50[0:Inp] || Grasp(U,V)* -> Object(V). 51[0:Inp] || Graspable(U,V)* -> Time(U). 52[0:Inp] || Graspable(U,V)* -> Object(V). 53[0:Inp] || Lt(U,V) -> SkP0(V,U)*. 54[0:Inp] || Leq(U,V) -> SkP0(V,U)*. 55[0:Inp] || Leq3(U,V,W)* -> Time(U). 56[0:Inp] || Leq3(U,V,W)* -> Time(V). 57[0:Inp] || Leq3(U,V,W)* -> Time(W). 58[0:Inp] || Occurs(U,V,W)* -> Time(U). 59[0:Inp] || Occurs(U,V,W)* -> Time(V). 60[0:Inp] || Occurs(U,V,W)* -> Action(W). 61[0:Inp] || OSPlace(U,V,W)* -> Time(U). 62[0:Inp] || OSPlace(U,V,W)* -> ObjectSet(V). 63[0:Inp] || OSPlace(U,V,W)* -> Region(W). 64[0:Inp] || UprightContainer(U,V,W)* -> Time(U). 65[0:Inp] || UprightContainer(U,V,W)* -> Object(V). 66[0:Inp] || UprightContainer(U,V,W)* -> Region(W). 67[0:Inp] || SkP1(U,V,W)* -> Time(W). 68[0:Inp] || SkP1(U,V,W)* -> Object(V). 69[0:Inp] || SkP1(U,V,W)* -> Object(U). 70[0:Inp] || Fits(U,V) -> SkP2(V,U)*. 71[0:Inp] || SmallSet(U,V) -> SkP2(V,U)*. 72[0:Inp] || Isolates(U,V,W)* -> Time(U). 73[0:Inp] || Isolates(U,V,W)* -> ObjectSet(V). 74[0:Inp] || Isolates(U,V,W)* -> ObjectSet(W). 75[0:Inp] || BoxedIn(U,V,W)* -> Time(U). 76[0:Inp] || BoxedIn(U,V,W)* -> Object(V). 77[0:Inp] || BoxedIn(U,V,W)* -> Object(W). 78[0:Inp] || SkP3(U,V,W)* -> Time(W). 79[0:Inp] || SkP3(U,V,W)* -> Time(V). 80[0:Inp] || SkP3(U,V,W)* -> Object(U). 81[0:Inp] || DR(U,V) -> SkP4(V,U)*. 82[0:Inp] || DC(U,V) -> SkP4(V,U)*. 83[0:Inp] || EC(U,V) -> SkP4(V,U)*. 84[0:Inp] || C(U,V) -> SkP4(V,U)*. 85[0:Inp] || P(U,V) -> SkP4(V,U)*. 86[0:Inp] || O(U,V) -> SkP4(V,U)*. 87[0:Inp] || OV(U,V) -> SkP4(V,U)*. 88[0:Inp] || OpenContained(U,V) -> SkP5(V,U)*. 89[0:Inp] || FullyOutside(U,V) -> SkP5(V,U)*. 90[0:Inp] || OpenContainerShape(U,V) -> SkP5(V,U)*. 91[0:Inp] || UprightContainerShape(U,V) -> SkP5(V,U)*. 92[0:Inp] || Cavity(U,V) -> SkP6(V,U)*. 93[0:Inp] || Outside(U,V) -> SkP6(V,U)*. 94[0:Inp] || PartiallyContained(U,V) -> SkP6(V,U)*. 95[0:Inp] || CombinedContainer(U,V,W)* -> Region(U). 96[0:Inp] || CombinedContainer(U,V,W)* -> Region(V). 97[0:Inp] || CombinedContainer(U,V,W)* -> Region(W). 98[0:Inp] || Moves(U,V,W)* -> Time(U). 99[0:Inp] || Moves(U,V,W)* -> Time(V). 100[0:Inp] || Moves(U,V,W)* -> Object(W). 101[0:Inp] || SkP7(U,V,W)* -> Time(W). 102[0:Inp] || SkP7(U,V,W)* -> Time(V). 103[0:Inp] || SkP7(U,V,W)* -> Object(U). 104[0:Inp] || SkP8(U,V,W)* -> Time(W). 105[0:Inp] || SkP8(U,V,W)* -> Time(V). 106[0:Inp] || SkP8(U,V,W)* -> ObjectSet(U). 107[0:Inp] || Grasps(U,V,W)* -> Time(U). 108[0:Inp] || Grasps(U,V,W)* -> Time(V). 109[0:Inp] || Grasps(U,V,W)* -> Object(W). 110[0:Inp] || Constant(U,V,W)* -> Time(U). 111[0:Inp] || Constant(U,V,W)* -> Time(V). 112[0:Inp] || Constant(U,V,W)* -> History(W). 113[0:Inp] || SkP9(U,V,W)* -> Time(W). 114[0:Inp] || SkP9(U,V,W)* -> Time(V). 115[0:Inp] || SkP9(U,V,W)* -> History(U). 116[0:Inp] || BoxWithLid(U,V,W)* -> Time(U). 117[0:Inp] || BoxWithLid(U,V,W)* -> Object(V). 118[0:Inp] || BoxWithLid(U,V,W)* -> Object(W). 119[0:Inp] || SafeManipulate(U,V,W,X)* -> Time(U). 120[0:Inp] || SafeManipulate(U,V,W,X)* -> Time(V). 121[0:Inp] || SafeManipulate(U,V,W,X)* -> Object(W). 122[0:Inp] || SafeManipulate(U,V,W,X)* -> Region(X). 123[0:Inp] || SkP10(U,V,W,X)* -> Time(X). 124[0:Inp] || SkP10(U,V,W,X)* -> Time(W). 125[0:Inp] || SkP10(U,V,W,X)* -> History(V). 126[0:Inp] || SkP10(U,V,W,X)* -> History(U). 127[0:Inp] || DynamicUContainer(U,V,W,X)* -> Time(U). 128[0:Inp] || DynamicUContainer(U,V,W,X)* -> Time(V). 129[0:Inp] || DynamicUContainer(U,V,W,X)* -> Object(W). 130[0:Inp] || DynamicUContainer(U,V,W,X)* -> History(X). 131[0:Inp] || BoxWithLidC(U,V,W,X)* -> Time(U). 132[0:Inp] || BoxWithLidC(U,V,W,X)* -> Object(V). 133[0:Inp] || BoxWithLidC(U,V,W,X)* -> Object(W). 134[0:Inp] || BoxWithLidC(U,V,W,X)* -> Region(X). 135[0:Inp] || Leq3(U,V,W)* -> Leq(U,V). 136[0:Inp] || Leq3(U,V,W)* -> Leq(V,W). 137[0:Inp] || CContained(U,V,W) -> SkP1(W,V,U)*. 138[0:Inp] || UContained(U,V,W) -> SkP1(W,V,U)*. 139[0:Inp] || BLContained(U,V,W) -> SkP1(W,V,U)*. 140[0:Inp] || PreserveCContents(U,V,W) -> SkP3(W,V,U)*. 141[0:Inp] || PreserveUContents(U,V,W) -> SkP3(W,V,U)*. 142[0:Inp] || PreserveBoxWithLid(U,V,W) -> SkP3(W,V,U)*. 143[0:Inp] || StableThroughout(U,V,W) -> SkP7(W,V,U)*. 144[0:Inp] || Released(U,V,W) -> SkP7(W,V,U)*. 145[0:Inp] || Motionless(U,V,W) -> SkP7(W,V,U)*. 146[0:Inp] || CausallyIsolated(U,V,W) -> SkP8(W,V,U)*. 147[0:Inp] || StaticCausallyIsolated(U,V,W) -> SkP8(W,V,U)*. 148[0:Inp] || AlwaysIntConn(U,V,W) -> SkP9(W,V,U)*. 149[0:Inp] || Continuous(U,V,W) -> SkP9(W,V,U)*. 150[0:Inp] || Action(U) Action(V) -> Action(Sequence(U,V))*. 151[0:Inp] || Region(U) Region(V) -> Region(RUnion(U,V))*. 152[0:Inp] || Object(U) Object(V) -> ObjectSet(Pair(U,V))*. 153[0:Inp] || ObjectSet(U) ObjectSet(V) -> ObjectSet(Union(U,V))*. 154[0:Inp] || Time(U) Object(V) -> Region(Place(U,V))*. 155[0:Inp] || Time(U) Region(V) -> ObjectSet(Contents(U,V))*. 156[0:Inp] || Time(U) ObjectSet(V) -> ObjectSet(CContents(U,V))*. 157[0:Inp] || Time(U) ObjectSet(V) -> ObjectSet(UContents(U,V))*. 158[0:Inp] || Object(U) Region(V) -> Action(ManipTo(U,V))*. 159[0:Inp] || Time(U) History(V) -> Region(Slice(U,V))*. 160[0:Inp] || History(U) History(V) -> History(HUnion(U,V))*. 161[0:Inp] || Time(U) Object(V) -> ObjectSet(MovingGroup(U,V))*. 162[0:Inp] || Object(U) Object(V) -> Action(PutInUC(U,V))*. 163[0:Inp] || Object(U) Object(V) -> Action(LoadUprightContainer(U,V))*. 164[0:Inp] || PersistentCavity(U,V,W,X) -> SkP10(X,W,V,U)*. 165[0:Inp] || NoExitCavity(U,V,W,X) -> SkP10(X,W,V,U)*. 166[0:Inp] || NoEntranceCavity(U,V,W,X) -> SkP10(X,W,V,U)*. 167[0:Inp] || Lt(U,V)* Lt(V,W)* -> Lt(U,W)*. 168[0:Inp] || Leq(U,V) Leq(W,U) -> Leq3(W,U,V)*. 169[0:Inp] || Region(U) Region(V) -> O(U,V) DR(U,V)*. 170[0:Inp] || O(U,RUnion(V,W))* -> O(U,V) O(U,W). 171[0:Inp] || Lt(U,V) Time(U) Time(V) -> Leq(U,V)*. 172[0:Inp] || equal(U,V) Time(U) Time(V) -> Leq(U,V)*. 173[0:Inp] || DR(U,V)* O(U,V) Region(U) Region(V) -> . 174[0:Inp] || Leq(U,V)* Time(U) Time(V) -> Lt(U,V) equal(U,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: 171 Conjecture clauses: 3 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: LoadUprightContainer > PutInUC > MovingGroup > HUnion > Slice > ManipTo > UContents > CContents > Union > Pair > RUnion > Place > Contents > Sequence > HPlace > TravelTo > Singleton > ConvexHull > ObjectSet > Action > SkP4 > DR > O > 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 > P > 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 > Cavity > Constant > Grasps > FeasiblePlace > OV > BoxWithLidC > BoxWithLid > CombinedContainer > EC > SkP10 > PersistentCavity > NoExitCavity > NoEntranceCavity > SkP9 > Continuous > AlwaysIntConn > IntConn > Isolates > ClosedContainer > SkP8 > CausallyIsolated > StaticCausallyIsolated > RigidObject > C > Outside > DC > skc5 > skc4 > skc3 > skc2 > skc1 > skc0 > Su > Tx > Oa > Tm > Hc > Hu > Tb5 > Os5 > Rc5 > Ol5 > Ob5 > Ta5 > Rc > Rb > Tm2 > Tb > Ra > Tm1 > Agent > Ox4 > Rc4 > Ob4 > Ta4 > StandStill Ordering : KBO Processed Problem: Worked Off Clauses: Usable Clauses: 1[0:Inp] || -> Action(StandStill)*. 4[0:Inp] || -> Region(Rc)*. 3[0:Inp] || -> Region(Rb)*. 2[0:Inp] || -> Region(Ra)*. 6[0:Inp] || -> DR(skc3,skc4)*. 5[0:Inp] || -> DR(skc3,skc5)*. 176[0:Res:6.0,81.0] || -> SkP4(skc4,skc3)*. 178[0:Res:5.0,81.0] || -> SkP4(skc5,skc3)*. 11[0:Inp] RigidObject(U) || -> Object(U)*. 7[0:Inp] SmallObject(U) || -> Object(U)*. 8[0:Inp] IntConn(U) || -> Region(U)*. 10[0:Inp] EmptyHanded(U) || -> Time(U)*. 9[0:Inp] AllStable(U) || -> Time(U)*. 12[0:Inp] || DR(skc3,RUnion(skc5,skc4))* -> . 16[0:Inp] Object(U) || -> History(HPlace(U))*. 15[0:Inp] Region(U) || -> Action(TravelTo(U))*. 14[0:Inp] Object(U) || -> ObjectSet(Singleton(U))*. 13[0:Inp] Region(U) || -> Region(ConvexHull(U))*. 20[0:Inp] || Feasible(U,V)* -> Action(V). 22[0:Inp] || Element(U,V)* -> ObjectSet(V). 25[0:Inp] || SkP2(U,V)* -> ObjectSet(V). 52[0:Inp] || Graspable(U,V)* -> Object(V). 50[0:Inp] || Grasp(U,V)* -> Object(V). 48[0:Inp] || CanGrasp(U,V)* -> Object(V). 46[0:Inp] || NoPartialContents(U,V)* -> Object(V). 44[0:Inp] || Stable(U,V)* -> Object(V). 30[0:Inp] || SafelyMovable(U,V)* -> Object(V). 27[0:Inp] || OMuchSmaller(U,V)* -> Object(U). 23[0:Inp] || FeasiblePlace(U,V)* -> Object(U). 21[0:Inp] || Element(U,V)* -> Object(U). 42[0:Inp] || MuchSmaller(U,V)* -> Region(V). 41[0:Inp] || MuchSmaller(U,V)* -> Region(U). 34[0:Inp] || Reachable(U,V)* -> Region(V). 28[0:Inp] || OMuchSmaller(U,V)* -> Region(V). 24[0:Inp] || FeasiblePlace(U,V)* -> Region(V). 32[0:Inp] || FullyOutside(U,V)* -> Region(V). 31[0:Inp] || FullyOutside(U,V)* -> Region(U). 26[0:Inp] || SkP2(U,V)* -> Region(U). 40[0:Inp] || SkP6(U,V)* -> Region(U). 39[0:Inp] || SkP6(U,V)* -> Region(V). 38[0:Inp] || SkP5(U,V)* -> Region(U). 37[0:Inp] || SkP5(U,V)* -> Region(V). 36[0:Inp] || SkP4(U,V)* -> Region(U). 35[0:Inp] || SkP4(U,V)* -> Region(V). 51[0:Inp] || Graspable(U,V)* -> Time(U). 49[0:Inp] || Grasp(U,V)* -> Time(U). 47[0:Inp] || CanGrasp(U,V)* -> Time(U). 45[0:Inp] || NoPartialContents(U,V)* -> Time(U). 43[0:Inp] || Stable(U,V)* -> Time(U). 33[0:Inp] || Reachable(U,V)* -> Time(U). 29[0:Inp] || SafelyMovable(U,V)* -> Time(U). 19[0:Inp] || Feasible(U,V)* -> Time(U). 18[0:Inp] || SkP0(U,V)* -> Time(U). 17[0:Inp] || SkP0(U,V)* -> Time(V). 71[0:Inp] || SmallSet(U,V) -> SkP2(V,U)*. 70[0:Inp] || Fits(U,V) -> SkP2(V,U)*. 53[0:Inp] || Lt(U,V) -> SkP0(V,U)*. 54[0:Inp] || Leq(U,V) -> SkP0(V,U)*. 94[0:Inp] || PartiallyContained(U,V) -> SkP6(V,U)*. 93[0:Inp] || Outside(U,V) -> SkP6(V,U)*. 92[0:Inp] || Cavity(U,V) -> SkP6(V,U)*. 91[0:Inp] || UprightContainerShape(U,V) -> SkP5(V,U)*. 90[0:Inp] || OpenContainerShape(U,V) -> SkP5(V,U)*. 88[0:Inp] || OpenContained(U,V) -> SkP5(V,U)*. 89[0:Inp] || FullyOutside(U,V) -> SkP5(V,U)*. 87[0:Inp] || OV(U,V) -> SkP4(V,U)*. 85[0:Inp] || P(U,V) -> SkP4(V,U)*. 84[0:Inp] || C(U,V) -> SkP4(V,U)*. 83[0:Inp] || EC(U,V) -> SkP4(V,U)*. 82[0:Inp] || DC(U,V) -> SkP4(V,U)*. 81[0:Inp] || DR(U,V) -> SkP4(V,U)*. 86[0:Inp] || O(U,V) -> SkP4(V,U)*. 112[0:Inp] || Constant(U,V,W)* -> History(W). 60[0:Inp] || Occurs(U,V,W)* -> Action(W). 115[0:Inp] || SkP9(U,V,W)* -> History(U). 74[0:Inp] || Isolates(U,V,W)* -> ObjectSet(W). 73[0:Inp] || Isolates(U,V,W)* -> ObjectSet(V). 62[0:Inp] || OSPlace(U,V,W)* -> ObjectSet(V). 106[0:Inp] || SkP8(U,V,W)* -> ObjectSet(U). 118[0:Inp] || BoxWithLid(U,V,W)* -> Object(W). 117[0:Inp] || BoxWithLid(U,V,W)* -> Object(V). 109[0:Inp] || Grasps(U,V,W)* -> Object(W). 100[0:Inp] || Moves(U,V,W)* -> Object(W). 77[0:Inp] || BoxedIn(U,V,W)* -> Object(W). 76[0:Inp] || BoxedIn(U,V,W)* -> Object(V). 65[0:Inp] || UprightContainer(U,V,W)* -> Object(V). 103[0:Inp] || SkP7(U,V,W)* -> Object(U). 80[0:Inp] || SkP3(U,V,W)* -> Object(U). 69[0:Inp] || SkP1(U,V,W)* -> Object(U). 68[0:Inp] || SkP1(U,V,W)* -> Object(V). 97[0:Inp] || CombinedContainer(U,V,W)* -> Region(W). 96[0:Inp] || CombinedContainer(U,V,W)* -> Region(V). 95[0:Inp] || CombinedContainer(U,V,W)* -> Region(U). 66[0:Inp] || UprightContainer(U,V,W)* -> Region(W). 63[0:Inp] || OSPlace(U,V,W)* -> Region(W). 116[0:Inp] || BoxWithLid(U,V,W)* -> Time(U). 111[0:Inp] || Constant(U,V,W)* -> Time(V). 110[0:Inp] || Constant(U,V,W)* -> Time(U). 108[0:Inp] || Grasps(U,V,W)* -> Time(V). 107[0:Inp] || Grasps(U,V,W)* -> Time(U). 99[0:Inp] || Moves(U,V,W)* -> Time(V). 98[0:Inp] || Moves(U,V,W)* -> Time(U). 75[0:Inp] || BoxedIn(U,V,W)* -> Time(U). 72[0:Inp] || Isolates(U,V,W)* -> Time(U). 64[0:Inp] || UprightContainer(U,V,W)* -> Time(U). 61[0:Inp] || OSPlace(U,V,W)* -> Time(U). 59[0:Inp] || Occurs(U,V,W)* -> Time(V). 58[0:Inp] || Occurs(U,V,W)* -> Time(U). 114[0:Inp] || SkP9(U,V,W)* -> Time(V). 113[0:Inp] || SkP9(U,V,W)* -> Time(W). 105[0:Inp] || SkP8(U,V,W)* -> Time(V). 104[0:Inp] || SkP8(U,V,W)* -> Time(W). 102[0:Inp] || SkP7(U,V,W)* -> Time(V). 101[0:Inp] || SkP7(U,V,W)* -> Time(W). 79[0:Inp] || SkP3(U,V,W)* -> Time(V). 78[0:Inp] || SkP3(U,V,W)* -> Time(W). 67[0:Inp] || SkP1(U,V,W)* -> Time(W). 57[0:Inp] || Leq3(U,V,W)* -> Time(W). 56[0:Inp] || Leq3(U,V,W)* -> Time(V). 55[0:Inp] || Leq3(U,V,W)* -> Time(U). 136[0:Inp] || Leq3(U,V,W)* -> Leq(V,W). 135[0:Inp] || Leq3(U,V,W)* -> Leq(U,V). 130[0:Inp] || DynamicUContainer(U,V,W,X)* -> History(X). 126[0:Inp] || SkP10(U,V,W,X)* -> History(U). 125[0:Inp] || SkP10(U,V,W,X)* -> History(V). 133[0:Inp] || BoxWithLidC(U,V,W,X)* -> Object(W). 132[0:Inp] || BoxWithLidC(U,V,W,X)* -> Object(V). 129[0:Inp] || DynamicUContainer(U,V,W,X)* -> Object(W). 121[0:Inp] || SafeManipulate(U,V,W,X)* -> Object(W). 134[0:Inp] || BoxWithLidC(U,V,W,X)* -> Region(X). 122[0:Inp] || SafeManipulate(U,V,W,X)* -> Region(X). 131[0:Inp] || BoxWithLidC(U,V,W,X)* -> Time(U). 128[0:Inp] || DynamicUContainer(U,V,W,X)* -> Time(V). 127[0:Inp] || DynamicUContainer(U,V,W,X)* -> Time(U). 120[0:Inp] || SafeManipulate(U,V,W,X)* -> Time(V). 119[0:Inp] || SafeManipulate(U,V,W,X)* -> Time(U). 124[0:Inp] || SkP10(U,V,W,X)* -> Time(W). 123[0:Inp] || SkP10(U,V,W,X)* -> Time(X). 149[0:Inp] || Continuous(U,V,W) -> SkP9(W,V,U)*. 148[0:Inp] || AlwaysIntConn(U,V,W) -> SkP9(W,V,U)*. 147[0:Inp] || StaticCausallyIsolated(U,V,W) -> SkP8(W,V,U)*. 146[0:Inp] || CausallyIsolated(U,V,W) -> SkP8(W,V,U)*. 145[0:Inp] || Motionless(U,V,W) -> SkP7(W,V,U)*. 144[0:Inp] || Released(U,V,W) -> SkP7(W,V,U)*. 143[0:Inp] || StableThroughout(U,V,W) -> SkP7(W,V,U)*. 142[0:Inp] || PreserveBoxWithLid(U,V,W) -> SkP3(W,V,U)*. 141[0:Inp] || PreserveUContents(U,V,W) -> SkP3(W,V,U)*. 140[0:Inp] || PreserveCContents(U,V,W) -> SkP3(W,V,U)*. 139[0:Inp] || BLContained(U,V,W) -> SkP1(W,V,U)*. 138[0:Inp] || UContained(U,V,W) -> SkP1(W,V,U)*. 137[0:Inp] || CContained(U,V,W) -> SkP1(W,V,U)*. 160[0:Inp] History(U) History(V) || -> History(HUnion(V,U))*. 150[0:Inp] Action(U) Action(V) || -> Action(Sequence(V,U))*. 163[0:Inp] Object(U) Object(V) || -> Action(LoadUprightContainer(V,U))*. 162[0:Inp] Object(U) Object(V) || -> Action(PutInUC(V,U))*. 158[0:Inp] Region(U) Object(V) || -> Action(ManipTo(V,U))*. 153[0:Inp] ObjectSet(U) ObjectSet(V) || -> ObjectSet(Union(V,U))*. 152[0:Inp] Object(U) Object(V) || -> ObjectSet(Pair(V,U))*. 157[0:Inp] ObjectSet(U) Time(V) || -> ObjectSet(UContents(V,U))*. 156[0:Inp] ObjectSet(U) Time(V) || -> ObjectSet(CContents(V,U))*. 161[0:Inp] Object(U) Time(V) || -> ObjectSet(MovingGroup(V,U))*. 155[0:Inp] Region(U) Time(V) || -> ObjectSet(Contents(V,U))*. 151[0:Inp] Region(U) Region(V) || -> Region(RUnion(V,U))*. 159[0:Inp] History(U) Time(V) || -> Region(Slice(V,U))*. 154[0:Inp] Object(U) Time(V) || -> Region(Place(V,U))*. 175[0:Res:6.0,173.2] Region(skc4) Region(skc3) || O(skc3,skc4)* -> . 177[0:Res:5.0,173.2] Region(skc5) Region(skc3) || O(skc3,skc5)* -> . 167[0:Inp] || Lt(U,V)* Lt(W,U)* -> Lt(W,V)*. 166[0:Inp] || NoEntranceCavity(U,V,W,X) -> SkP10(X,W,V,U)*. 165[0:Inp] || NoExitCavity(U,V,W,X) -> SkP10(X,W,V,U)*. 164[0:Inp] || PersistentCavity(U,V,W,X) -> SkP10(X,W,V,U)*. 169[0:Inp] Region(U) Region(V) || -> DR(V,U)* O(V,U). 170[0:Inp] || O(U,RUnion(V,W))* -> O(U,W) O(U,V). 168[0:Inp] || Leq(U,V) Leq(V,W) -> Leq3(U,V,W)*. 171[0:Inp] Time(U) Time(V) || Lt(V,U) -> Leq(V,U)*. 172[0:Inp] Time(U) Time(V) || equal(V,U) -> Leq(V,U)*. 179[0:Res:169.3,12.0] Region(skc3) Region(RUnion(skc5,skc4)) || -> O(skc3,RUnion(skc5,skc4))*. 173[0:Inp] Region(U) Region(V) || O(V,U) DR(V,U)* -> . 174[0:Inp] Time(U) Time(V) || Leq(V,U)* -> equal(V,U) Lt(V,U). Given clause: 1[0:Inp] || -> Action(StandStill)*. Given clause: 4[0:Inp] || -> Region(Rc)*. Given clause: 3[0:Inp] || -> Region(Rb)*. Given clause: 2[0:Inp] || -> Region(Ra)*. Given clause: 6[0:Inp] || -> DR(skc3,skc4)*. Given clause: 5[0:Inp] || -> DR(skc3,skc5)*. Given clause: 176[0:Res:6.0,81.0] || -> SkP4(skc4,skc3)*. Given clause: 178[0:Res:5.0,81.0] || -> SkP4(skc5,skc3)*. Given clause: 11[0:Inp] RigidObject(U) || -> Object(U)*. Given clause: 7[0:Inp] SmallObject(U) || -> Object(U)*. Given clause: 8[0:Inp] IntConn(U) || -> Region(U)*. Given clause: 10[0:Inp] EmptyHanded(U) || -> Time(U)*. Given clause: 9[0:Inp] AllStable(U) || -> Time(U)*. Given clause: 12[0:Inp] || DR(skc3,RUnion(skc5,skc4))* -> . Given clause: 16[0:Inp] Object(U) || -> History(HPlace(U))*. Given clause: 15[0:Inp] Region(U) || -> Action(TravelTo(U))*. Given clause: 14[0:Inp] Object(U) || -> ObjectSet(Singleton(U))*. Given clause: 13[0:Inp] Region(U) || -> Region(ConvexHull(U))*. Given clause: 20[0:Inp] || Feasible(U,V)* -> Action(V). Given clause: 22[0:Inp] || Element(U,V)* -> ObjectSet(V). Given clause: 25[0:Inp] || SkP2(U,V)* -> ObjectSet(V). Given clause: 52[0:Inp] || Graspable(U,V)* -> Object(V). Given clause: 50[0:Inp] || Grasp(U,V)* -> Object(V). Given clause: 48[0:Inp] || CanGrasp(U,V)* -> Object(V). Given clause: 46[0:Inp] || NoPartialContents(U,V)* -> Object(V). Given clause: 44[0:Inp] || Stable(U,V)* -> Object(V). Given clause: 30[0:Inp] || SafelyMovable(U,V)* -> Object(V). Given clause: 27[0:Inp] || OMuchSmaller(U,V)* -> Object(U). Given clause: 23[0:Inp] || FeasiblePlace(U,V)* -> Object(U). Given clause: 21[0:Inp] || Element(U,V)* -> Object(U). Given clause: 42[0:Inp] || MuchSmaller(U,V)* -> Region(V). Given clause: 41[0:Inp] || MuchSmaller(U,V)* -> Region(U). Given clause: 34[0:Inp] || Reachable(U,V)* -> Region(V). Given clause: 28[0:Inp] || OMuchSmaller(U,V)* -> Region(V). Given clause: 24[0:Inp] || FeasiblePlace(U,V)* -> Region(V). Given clause: 32[0:Inp] || FullyOutside(U,V)* -> Region(V). Given clause: 31[0:Inp] || FullyOutside(U,V)* -> Region(U). Given clause: 26[0:Inp] || SkP2(U,V)* -> Region(U). Given clause: 40[0:Inp] || SkP6(U,V)* -> Region(U). Given clause: 39[0:Inp] || SkP6(U,V)* -> Region(V). Given clause: 38[0:Inp] || SkP5(U,V)* -> Region(U). Given clause: 37[0:Inp] || SkP5(U,V)* -> Region(V). Given clause: 36[0:Inp] || SkP4(U,V)* -> Region(U). Given clause: 307[0:Res:176.0,36.0] || -> Region(skc4)*. Given clause: 35[0:Inp] || SkP4(U,V)* -> Region(V). Given clause: 308[0:Res:178.0,36.0] || -> Region(skc5)*. Given clause: 311[0:Res:176.0,35.0] || -> Region(skc3)*. Given clause: 314[0:MRR:309.0,311.0] || O(skc3,skc4)* -> . Given clause: 315[0:MRR:310.0,311.0] || O(skc3,skc5)* -> . Given clause: 51[0:Inp] || Graspable(U,V)* -> Time(U). Given clause: 49[0:Inp] || Grasp(U,V)* -> Time(U). Given clause: 47[0:Inp] || CanGrasp(U,V)* -> Time(U). Given clause: 45[0:Inp] || NoPartialContents(U,V)* -> Time(U). Given clause: 43[0:Inp] || Stable(U,V)* -> Time(U). Given clause: 33[0:Inp] || Reachable(U,V)* -> Time(U). Given clause: 29[0:Inp] || SafelyMovable(U,V)* -> Time(U). Given clause: 19[0:Inp] || Feasible(U,V)* -> Time(U). Given clause: 18[0:Inp] || SkP0(U,V)* -> Time(U). Given clause: 17[0:Inp] || SkP0(U,V)* -> Time(V). Given clause: 71[0:Inp] || SmallSet(U,V) -> SkP2(V,U)*. Given clause: 316[0:Res:71.1,26.0] || SmallSet(U,V)* -> Region(V). Given clause: 317[0:Res:71.1,25.0] || SmallSet(U,V)* -> ObjectSet(U). Given clause: 70[0:Inp] || Fits(U,V) -> SkP2(V,U)*. Given clause: 318[0:Res:70.1,26.0] || Fits(U,V)* -> Region(V). Given clause: 53[0:Inp] || Lt(U,V) -> SkP0(V,U)*. Given clause: 319[0:Res:70.1,25.0] || Fits(U,V)* -> ObjectSet(U). Given clause: 320[0:Res:53.1,17.0] || Lt(U,V)* -> Time(U). Given clause: 321[0:Res:53.1,18.0] || Lt(U,V)* -> Time(V). Given clause: 54[0:Inp] || Leq(U,V) -> SkP0(V,U)*. Given clause: 94[0:Inp] || PartiallyContained(U,V) -> SkP6(V,U)*. Given clause: 324[0:Res:54.1,17.0] || Leq(U,V)* -> Time(U). Given clause: 325[0:Res:54.1,18.0] || Leq(U,V)* -> Time(V). Given clause: 328[0:Res:94.1,39.0] || PartiallyContained(U,V)* -> Region(U). Given clause: 329[0:Res:94.1,40.0] || PartiallyContained(U,V)* -> Region(V). Given clause: 93[0:Inp] || Outside(U,V) -> SkP6(V,U)*. Given clause: 330[0:Res:93.1,39.0] || Outside(U,V)* -> Region(U). Given clause: 331[0:Res:93.1,40.0] || Outside(U,V)* -> Region(V). Given clause: 92[0:Inp] || Cavity(U,V) -> SkP6(V,U)*. Given clause: 332[0:Res:92.1,39.0] || Cavity(U,V)* -> Region(U). Given clause: 91[0:Inp] || UprightContainerShape(U,V) -> SkP5(V,U)*. Given clause: 333[0:Res:92.1,40.0] || Cavity(U,V)* -> Region(V). Given clause: 334[0:Res:91.1,37.0] || UprightContainerShape(U,V)* -> Region(U). Given clause: 335[0:Res:91.1,38.0] || UprightContainerShape(U,V)* -> Region(V). Given clause: 90[0:Inp] || OpenContainerShape(U,V) -> SkP5(V,U)*. Given clause: 88[0:Inp] || OpenContained(U,V) -> SkP5(V,U)*. Given clause: 336[0:Res:90.1,37.0] || OpenContainerShape(U,V)* -> Region(U). Given clause: 337[0:Res:90.1,38.0] || OpenContainerShape(U,V)* -> Region(V). Given clause: 338[0:Res:88.1,37.0] || OpenContained(U,V)* -> Region(U). Given clause: 339[0:Res:88.1,38.0] || OpenContained(U,V)* -> Region(V). Given clause: 89[0:Inp] || FullyOutside(U,V) -> SkP5(V,U)*. Given clause: 87[0:Inp] || OV(U,V) -> SkP4(V,U)*. Given clause: 342[0:Res:87.1,35.0] || OV(U,V)* -> Region(U). Given clause: 343[0:Res:87.1,36.0] || OV(U,V)* -> Region(V). Given clause: 85[0:Inp] || P(U,V) -> SkP4(V,U)*. Given clause: 84[0:Inp] || C(U,V) -> SkP4(V,U)*. Given clause: 344[0:Res:85.1,35.0] || P(U,V)* -> Region(U). Given clause: 345[0:Res:85.1,36.0] || P(U,V)* -> Region(V). Given clause: 346[0:Res:84.1,35.0] || C(U,V)* -> Region(U). Given clause: 347[0:Res:84.1,36.0] || C(U,V)* -> Region(V). Given clause: 83[0:Inp] || EC(U,V) -> SkP4(V,U)*. Given clause: 348[0:Res:83.1,35.0] || EC(U,V)* -> Region(U). Given clause: 349[0:Res:83.1,36.0] || EC(U,V)* -> Region(V). Given clause: 82[0:Inp] || DC(U,V) -> SkP4(V,U)*. Given clause: 350[0:Res:82.1,35.0] || DC(U,V)* -> Region(U). Given clause: 81[0:Inp] || DR(U,V) -> SkP4(V,U)*. Given clause: 351[0:Res:82.1,36.0] || DC(U,V)* -> Region(V). Given clause: 352[0:Res:81.1,35.0] || DR(U,V)* -> Region(U). Given clause: 353[0:Res:81.1,36.0] || DR(U,V)* -> Region(V). Given clause: 86[0:Inp] || O(U,V) -> SkP4(V,U)*. Given clause: 112[0:Inp] || Constant(U,V,W)* -> History(W). Given clause: 360[0:Res:86.1,35.0] || O(U,V)* -> Region(U). Given clause: 361[0:Res:86.1,36.0] || O(U,V)* -> Region(V). Given clause: 60[0:Inp] || Occurs(U,V,W)* -> Action(W). Given clause: 115[0:Inp] || SkP9(U,V,W)* -> History(U). Given clause: 74[0:Inp] || Isolates(U,V,W)* -> ObjectSet(W). Given clause: 73[0:Inp] || Isolates(U,V,W)* -> ObjectSet(V). Given clause: 62[0:Inp] || OSPlace(U,V,W)* -> ObjectSet(V). Given clause: 106[0:Inp] || SkP8(U,V,W)* -> ObjectSet(U). Given clause: 118[0:Inp] || BoxWithLid(U,V,W)* -> Object(W). Given clause: 117[0:Inp] || BoxWithLid(U,V,W)* -> Object(V). Given clause: 109[0:Inp] || Grasps(U,V,W)* -> Object(W). Given clause: 100[0:Inp] || Moves(U,V,W)* -> Object(W). Given clause: 77[0:Inp] || BoxedIn(U,V,W)* -> Object(W). Given clause: 76[0:Inp] || BoxedIn(U,V,W)* -> Object(V). Given clause: 65[0:Inp] || UprightContainer(U,V,W)* -> Object(V). Given clause: 103[0:Inp] || SkP7(U,V,W)* -> Object(U). Given clause: 80[0:Inp] || SkP3(U,V,W)* -> Object(U). Given clause: 69[0:Inp] || SkP1(U,V,W)* -> Object(U). Given clause: 68[0:Inp] || SkP1(U,V,W)* -> Object(V). Given clause: 97[0:Inp] || CombinedContainer(U,V,W)* -> Region(W). Given clause: 96[0:Inp] || CombinedContainer(U,V,W)* -> Region(V). Given clause: 95[0:Inp] || CombinedContainer(U,V,W)* -> Region(U). Given clause: 66[0:Inp] || UprightContainer(U,V,W)* -> Region(W). Given clause: 63[0:Inp] || OSPlace(U,V,W)* -> Region(W). Given clause: 116[0:Inp] || BoxWithLid(U,V,W)* -> Time(U). Given clause: 111[0:Inp] || Constant(U,V,W)* -> Time(V). Given clause: 110[0:Inp] || Constant(U,V,W)* -> Time(U). Given clause: 108[0:Inp] || Grasps(U,V,W)* -> Time(V). Given clause: 107[0:Inp] || Grasps(U,V,W)* -> Time(U). Given clause: 99[0:Inp] || Moves(U,V,W)* -> Time(V). Given clause: 98[0:Inp] || Moves(U,V,W)* -> Time(U). Given clause: 75[0:Inp] || BoxedIn(U,V,W)* -> Time(U). Given clause: 72[0:Inp] || Isolates(U,V,W)* -> Time(U). Given clause: 64[0:Inp] || UprightContainer(U,V,W)* -> Time(U). Given clause: 61[0:Inp] || OSPlace(U,V,W)* -> Time(U). Given clause: 59[0:Inp] || Occurs(U,V,W)* -> Time(V). Given clause: 58[0:Inp] || Occurs(U,V,W)* -> Time(U). Given clause: 114[0:Inp] || SkP9(U,V,W)* -> Time(V). Given clause: 113[0:Inp] || SkP9(U,V,W)* -> Time(W). Given clause: 105[0:Inp] || SkP8(U,V,W)* -> Time(V). Given clause: 104[0:Inp] || SkP8(U,V,W)* -> Time(W). Given clause: 102[0:Inp] || SkP7(U,V,W)* -> Time(V). Given clause: 101[0:Inp] || SkP7(U,V,W)* -> Time(W). Given clause: 79[0:Inp] || SkP3(U,V,W)* -> Time(V). Given clause: 78[0:Inp] || SkP3(U,V,W)* -> Time(W). Given clause: 67[0:Inp] || SkP1(U,V,W)* -> Time(W). Given clause: 57[0:Inp] || Leq3(U,V,W)* -> Time(W). Given clause: 56[0:Inp] || Leq3(U,V,W)* -> Time(V). Given clause: 55[0:Inp] || Leq3(U,V,W)* -> Time(U). Given clause: 323[0:MRR:322.0,321.1] || Lt(U,V) -> Leq(U,V)*. Given clause: 355[0:MRR:354.0,353.1] || O(U,V) DR(U,V)* -> . Given clause: 136[0:Inp] || Leq3(U,V,W)* -> Leq(V,W). Given clause: 135[0:Inp] || Leq3(U,V,W)* -> Leq(U,V). Given clause: 130[0:Inp] || DynamicUContainer(U,V,W,X)* -> History(X). Given clause: 126[0:Inp] || SkP10(U,V,W,X)* -> History(U). Given clause: 125[0:Inp] || SkP10(U,V,W,X)* -> History(V). Given clause: 133[0:Inp] || BoxWithLidC(U,V,W,X)* -> Object(W). Given clause: 132[0:Inp] || BoxWithLidC(U,V,W,X)* -> Object(V). Given clause: 129[0:Inp] || DynamicUContainer(U,V,W,X)* -> Object(W). Given clause: 121[0:Inp] || SafeManipulate(U,V,W,X)* -> Object(W). Given clause: 134[0:Inp] || BoxWithLidC(U,V,W,X)* -> Region(X). Given clause: 122[0:Inp] || SafeManipulate(U,V,W,X)* -> Region(X). Given clause: 131[0:Inp] || BoxWithLidC(U,V,W,X)* -> Time(U). Given clause: 128[0:Inp] || DynamicUContainer(U,V,W,X)* -> Time(V). Given clause: 127[0:Inp] || DynamicUContainer(U,V,W,X)* -> Time(U). Given clause: 120[0:Inp] || SafeManipulate(U,V,W,X)* -> Time(V). Given clause: 119[0:Inp] || SafeManipulate(U,V,W,X)* -> Time(U). Given clause: 124[0:Inp] || SkP10(U,V,W,X)* -> Time(W). Given clause: 123[0:Inp] || SkP10(U,V,W,X)* -> Time(X). Given clause: 149[0:Inp] || Continuous(U,V,W) -> SkP9(W,V,U)*. Given clause: 366[0:Res:149.1,113.0] || Continuous(U,V,W)* -> Time(U). Given clause: 367[0:Res:149.1,114.0] || Continuous(U,V,W)* -> Time(V). Given clause: 368[0:Res:149.1,115.0] || Continuous(U,V,W)* -> History(W). Given clause: 148[0:Inp] || AlwaysIntConn(U,V,W) -> SkP9(W,V,U)*. Given clause: 147[0:Inp] || StaticCausallyIsolated(U,V,W) -> SkP8(W,V,U)*. Given clause: 369[0:Res:148.1,113.0] || AlwaysIntConn(U,V,W)* -> Time(U). Given clause: 370[0:Res:148.1,114.0] || AlwaysIntConn(U,V,W)* -> Time(V). Given clause: 371[0:Res:148.1,115.0] || AlwaysIntConn(U,V,W)* -> History(W). Given clause: 372[0:Res:147.1,104.0] || StaticCausallyIsolated(U,V,W)* -> Time(U). Given clause: 146[0:Inp] || CausallyIsolated(U,V,W) -> SkP8(W,V,U)*. Given clause: 373[0:Res:147.1,105.0] || StaticCausallyIsolated(U,V,W)* -> Time(V). Given clause: 374[0:Res:147.1,106.0] || StaticCausallyIsolated(U,V,W)* -> ObjectSet(W). Given clause: 375[0:Res:146.1,104.0] || CausallyIsolated(U,V,W)* -> Time(U). Given clause: 376[0:Res:146.1,105.0] || CausallyIsolated(U,V,W)* -> Time(V). Given clause: 145[0:Inp] || Motionless(U,V,W) -> SkP7(W,V,U)*. Given clause: 377[0:Res:146.1,106.0] || CausallyIsolated(U,V,W)* -> ObjectSet(W). Given clause: 378[0:Res:145.1,101.0] || Motionless(U,V,W)* -> Time(U). Given clause: 379[0:Res:145.1,102.0] || Motionless(U,V,W)* -> Time(V). Given clause: 380[0:Res:145.1,103.0] || Motionless(U,V,W)* -> Object(W). Given clause: 144[0:Inp] || Released(U,V,W) -> SkP7(W,V,U)*. Given clause: 381[0:Res:144.1,101.0] || Released(U,V,W)* -> Time(U). Given clause: 382[0:Res:144.1,102.0] || Released(U,V,W)* -> Time(V). Given clause: 383[0:Res:144.1,103.0] || Released(U,V,W)* -> Object(W). Given clause: 143[0:Inp] || StableThroughout(U,V,W) -> SkP7(W,V,U)*. Given clause: 142[0:Inp] || PreserveBoxWithLid(U,V,W) -> SkP3(W,V,U)*. Given clause: 384[0:Res:143.1,101.0] || StableThroughout(U,V,W)* -> Time(U). Given clause: 385[0:Res:143.1,102.0] || StableThroughout(U,V,W)* -> Time(V). Given clause: 386[0:Res:143.1,103.0] || StableThroughout(U,V,W)* -> Object(W). Given clause: 387[0:Res:142.1,78.0] || PreserveBoxWithLid(U,V,W)* -> Time(U). Given clause: 141[0:Inp] || PreserveUContents(U,V,W) -> SkP3(W,V,U)*. Given clause: 388[0:Res:142.1,79.0] || PreserveBoxWithLid(U,V,W)* -> Time(V). Given clause: 389[0:Res:142.1,80.0] || PreserveBoxWithLid(U,V,W)* -> Object(W). Given clause: 390[0:Res:141.1,78.0] || PreserveUContents(U,V,W)* -> Time(U). Given clause: 391[0:Res:141.1,79.0] || PreserveUContents(U,V,W)* -> Time(V). Given clause: 140[0:Inp] || PreserveCContents(U,V,W) -> SkP3(W,V,U)*. Given clause: 392[0:Res:141.1,80.0] || PreserveUContents(U,V,W)* -> Object(W). Given clause: 393[0:Res:140.1,78.0] || PreserveCContents(U,V,W)* -> Time(U). Given clause: 394[0:Res:140.1,79.0] || PreserveCContents(U,V,W)* -> Time(V). Given clause: 395[0:Res:140.1,80.0] || PreserveCContents(U,V,W)* -> Object(W). Given clause: 139[0:Inp] || BLContained(U,V,W) -> SkP1(W,V,U)*. Given clause: 396[0:Res:139.1,67.0] || BLContained(U,V,W)* -> Time(U). Given clause: 397[0:Res:139.1,68.0] || BLContained(U,V,W)* -> Object(V). Given clause: 398[0:Res:139.1,69.0] || BLContained(U,V,W)* -> Object(W). Given clause: 138[0:Inp] || UContained(U,V,W) -> SkP1(W,V,U)*. Given clause: 137[0:Inp] || CContained(U,V,W) -> SkP1(W,V,U)*. Given clause: 399[0:Res:138.1,67.0] || UContained(U,V,W)* -> Time(U). Given clause: 400[0:Res:138.1,68.0] || UContained(U,V,W)* -> Object(V). Given clause: 401[0:Res:138.1,69.0] || UContained(U,V,W)* -> Object(W). Given clause: 402[0:Res:137.1,67.0] || CContained(U,V,W)* -> Time(U). Given clause: 160[0:Inp] History(U) History(V) || -> History(HUnion(V,U))*. Given clause: 403[0:Res:137.1,68.0] || CContained(U,V,W)* -> Object(V). Given clause: 404[0:Res:137.1,69.0] || CContained(U,V,W)* -> Object(W). Given clause: 313[0:MRR:179.0,311.0] Region(RUnion(skc5,skc4)) || -> O(skc3,RUnion(skc5,skc4))*. Given clause: 405[0:SoR:313.0,8.1] IntConn(RUnion(skc5,skc4)) || -> O(skc3,RUnion(skc5,skc4))*. Given clause: 150[0:Inp] Action(U) Action(V) || -> Action(Sequence(V,U))*. Given clause: 163[0:Inp] Object(U) Object(V) || -> Action(LoadUprightContainer(V,U))*. Given clause: 162[0:Inp] Object(U) Object(V) || -> Action(PutInUC(V,U))*. Given clause: 158[0:Inp] Region(U) Object(V) || -> Action(ManipTo(V,U))*. Given clause: 153[0:Inp] ObjectSet(U) ObjectSet(V) || -> ObjectSet(Union(V,U))*. Given clause: 152[0:Inp] Object(U) Object(V) || -> ObjectSet(Pair(V,U))*. Given clause: 157[0:Inp] ObjectSet(U) Time(V) || -> ObjectSet(UContents(V,U))*. Given clause: 156[0:Inp] ObjectSet(U) Time(V) || -> ObjectSet(CContents(V,U))*. Given clause: 161[0:Inp] Object(U) Time(V) || -> ObjectSet(MovingGroup(V,U))*. Given clause: 155[0:Inp] Region(U) Time(V) || -> ObjectSet(Contents(V,U))*. Given clause: 151[0:Inp] Region(U) Region(V) || -> Region(RUnion(V,U))*. Given clause: 407[0:SSi:406.1,406.0,307.0,308.0] || -> O(skc3,RUnion(skc5,skc4))*. Given clause: 408[0:Res:407.0,361.0] || -> Region(RUnion(skc5,skc4))*. Given clause: 159[0:Inp] History(U) Time(V) || -> Region(Slice(V,U))*. Given clause: 154[0:Inp] Object(U) Time(V) || -> Region(Place(V,U))*. Given clause: 327[0:MRR:326.0,325.1] || Leq(U,V)* -> equal(U,V) Lt(U,V). Given clause: 167[0:Inp] || Lt(U,V)*+ Lt(W,U)* -> Lt(W,V)*. Given clause: 166[0:Inp] || NoEntranceCavity(U,V,W,X) -> SkP10(X,W,V,U)*. Given clause: 411[0:Res:166.1,123.0] || NoEntranceCavity(U,V,W,X)* -> Time(U). Given clause: 412[0:Res:166.1,124.0] || NoEntranceCavity(U,V,W,X)* -> Time(V). Given clause: 165[0:Inp] || NoExitCavity(U,V,W,X) -> SkP10(X,W,V,U)*. Given clause: 413[0:Res:166.1,125.0] || NoEntranceCavity(U,V,W,X)* -> History(W). Given clause: 414[0:Res:166.1,126.0] || NoEntranceCavity(U,V,W,X)* -> History(X). Given clause: 415[0:Res:165.1,123.0] || NoExitCavity(U,V,W,X)* -> Time(U). Given clause: 416[0:Res:165.1,124.0] || NoExitCavity(U,V,W,X)* -> Time(V). Given clause: 164[0:Inp] || PersistentCavity(U,V,W,X) -> SkP10(X,W,V,U)*. Given clause: 417[0:Res:165.1,125.0] || NoExitCavity(U,V,W,X)* -> History(W). Given clause: 418[0:Res:165.1,126.0] || NoExitCavity(U,V,W,X)* -> History(X). Given clause: 419[0:Res:164.1,123.0] || PersistentCavity(U,V,W,X)* -> Time(U). Given clause: 420[0:Res:164.1,124.0] || PersistentCavity(U,V,W,X)* -> Time(V). Given clause: 169[0:Inp] Region(U) Region(V) || -> DR(V,U)* O(V,U). Given clause: 421[0:Res:164.1,125.0] || PersistentCavity(U,V,W,X)* -> History(W). Given clause: 422[0:Res:164.1,126.0] || PersistentCavity(U,V,W,X)* -> History(X). Given clause: 170[0:Inp] || O(U,RUnion(V,W))* -> O(U,W) O(U,V). SPASS V 3.5 SPASS beiseite: Proof found. Problem: sh.dfg SPASS derived 122 clauses, backtracked 0 clauses, performed 0 splits and kept 279 clauses. SPASS allocated 55670 KBytes. SPASS spent 0:00:00.09 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 3, length 27 : 5[0:Inp] || -> DR(skc3,skc5)*. 6[0:Inp] || -> DR(skc3,skc4)*. 12[0:Inp] || DR(skc3,RUnion(skc5,skc4))* -> . 35[0:Inp] || SkP4(U,V)* -> Region(V). 36[0:Inp] || SkP4(U,V)* -> Region(U). 81[0:Inp] || DR(U,V) -> SkP4(V,U)*. 151[0:Inp] Region(U) Region(V) || -> Region(RUnion(V,U))*. 169[0:Inp] Region(U) Region(V) || -> DR(V,U)* O(V,U). 170[0:Inp] || O(U,RUnion(V,W))* -> O(U,W) O(U,V). 173[0:Inp] Region(U) Region(V) || O(V,U) DR(V,U)* -> . 175[0:Res:6.0,173.2] Region(skc4) Region(skc3) || O(skc3,skc4)* -> . 176[0:Res:6.0,81.0] || -> SkP4(skc4,skc3)*. 177[0:Res:5.0,173.2] Region(skc5) Region(skc3) || O(skc3,skc5)* -> . 178[0:Res:5.0,81.0] || -> SkP4(skc5,skc3)*. 179[0:Res:169.3,12.0] Region(skc3) Region(RUnion(skc5,skc4)) || -> O(skc3,RUnion(skc5,skc4))*. 307[0:Res:176.0,36.0] || -> Region(skc4)*. 308[0:Res:178.0,36.0] || -> Region(skc5)*. 309[0:MRR:175.0,307.0] Region(skc3) || O(skc3,skc4)* -> . 310[0:MRR:177.0,308.0] Region(skc3) || O(skc3,skc5)* -> . 311[0:Res:176.0,35.0] || -> Region(skc3)*. 313[0:MRR:179.0,311.0] Region(RUnion(skc5,skc4)) || -> O(skc3,RUnion(skc5,skc4))*. 314[0:MRR:309.0,311.0] || O(skc3,skc4)* -> . 315[0:MRR:310.0,311.0] || O(skc3,skc5)* -> . 406[0:SoR:313.0,151.2] Region(skc5) Region(skc4) || -> O(skc3,RUnion(skc5,skc4))*. 407[0:SSi:406.1,406.0,307.0,308.0] || -> O(skc3,RUnion(skc5,skc4))*. 427[0:Res:407.0,170.0] || -> O(skc3,skc4) O(skc3,skc5)*. 428[0:MRR:427.0,427.1,314.0,315.0] || -> . Formulae used in the proof : LemSH axiom38 axiom1 SBD3 SBA4 --------------------------SPASS-STOP------------------------------