--------------------------SPASS-START----------------------------- Input Problem: 1[0:Inp] || -> Object(skc5)*. 2[0:Inp] || -> Object(skc4)*. 3[0:Inp] || -> Time(skc3)*. 4[0:Inp] || -> Action(StandStill)*. 5[0:Inp] || Element(U,Null)* -> . 6[0:Inp] || SmallObject(U) -> Object(U)*. 7[0:Inp] || AllStable(U) -> Time(U)*. 8[0:Inp] || EmptyHanded(U) -> Time(U)*. 9[0:Inp] || -> Object(skf8(U,V,W))*. 10[0:Inp] || Region(U) -> Region(ConvexHull(U))*. 11[0:Inp] || Object(U) -> ObjectSet(Singleton(U))*. 12[0:Inp] || Region(U) -> Action(TravelTo(U))*. 13[0:Inp] || Object(U) -> History(HPlace(U))*. 14[0:Inp] || Feasible(U,V)* -> Time(U). 15[0:Inp] || Feasible(U,V)* -> Action(V). 16[0:Inp] || Element(U,V)* -> Object(U). 17[0:Inp] || Element(U,V)* -> ObjectSet(V). 18[0:Inp] || FeasiblePlace(U,V)* -> Object(U). 19[0:Inp] || FeasiblePlace(U,V)* -> Region(V). 20[0:Inp] || SafelyMovable(U,V)* -> Time(U). 21[0:Inp] || SafelyMovable(U,V)* -> Object(V). 22[0:Inp] || FullyOutside(U,V)* -> Region(U). 23[0:Inp] || FullyOutside(U,V)* -> Region(V). 24[0:Inp] || Reachable(U,V)* -> Time(U). 25[0:Inp] || Reachable(U,V)* -> Region(V). 26[0:Inp] || SkP2(U,V)* -> ObjectSet(V). 27[0:Inp] || SkP2(U,V)* -> Region(U). 28[0:Inp] || OMuchSmaller(U,V)* -> Object(U). 29[0:Inp] || OMuchSmaller(U,V)* -> Region(V). 30[0:Inp] || SkP3(U,V)* -> Region(V). 31[0:Inp] || SkP3(U,V)* -> Region(U). 32[0:Inp] || SkP4(U,V)* -> Region(V). 33[0:Inp] || SkP4(U,V)* -> Region(U). 34[0:Inp] || SkP5(U,V)* -> Region(V). 35[0:Inp] || SkP5(U,V)* -> Region(U). 36[0:Inp] || MuchSmaller(U,V)* -> Region(U). 37[0:Inp] || MuchSmaller(U,V)* -> Region(V). 38[0:Inp] || Stable(U,V)* -> Time(U). 39[0:Inp] || Stable(U,V)* -> Object(V). 40[0:Inp] || NoPartialContents(U,V)* -> Time(U). 41[0:Inp] || NoPartialContents(U,V)* -> Object(V). 42[0:Inp] || CanGrasp(U,V)* -> Time(U). 43[0:Inp] || CanGrasp(U,V)* -> Object(V). 44[0:Inp] || Grasp(U,V)* -> Time(U). 45[0:Inp] || Grasp(U,V)* -> Object(V). 46[0:Inp] || Graspable(U,V)* -> Time(U). 47[0:Inp] || Graspable(U,V)* -> Object(V). 48[0:Inp] || Occurs(U,V,W)* -> Time(U). 49[0:Inp] || Occurs(U,V,W)* -> Time(V). 50[0:Inp] || Occurs(U,V,W)* -> Action(W). 51[0:Inp] || OSPlace(U,V,W)* -> Time(U). 52[0:Inp] || OSPlace(U,V,W)* -> ObjectSet(V). 53[0:Inp] || OSPlace(U,V,W)* -> Region(W). 54[0:Inp] || UprightContainer(U,V,W)* -> Time(U). 55[0:Inp] || UprightContainer(U,V,W)* -> Object(V). 56[0:Inp] || UprightContainer(U,V,W)* -> Region(W). 57[0:Inp] || SkP0(U,V,W)* -> Time(W). 58[0:Inp] || SkP0(U,V,W)* -> Object(V). 59[0:Inp] || SkP0(U,V,W)* -> Object(U). 60[0:Inp] || BoxedIn(U,V,W)* -> Time(U). 61[0:Inp] || BoxedIn(U,V,W)* -> Object(V). 62[0:Inp] || BoxedIn(U,V,W)* -> Object(W). 63[0:Inp] || SkP1(U,V,W)* -> Time(W). 64[0:Inp] || SkP1(U,V,W)* -> Time(V). 65[0:Inp] || SkP1(U,V,W)* -> Object(U). 66[0:Inp] || Fits(U,V) -> SkP2(V,U)*. 67[0:Inp] || SmallSet(U,V) -> SkP2(V,U)*. 68[0:Inp] || P(U,V) -> SkP3(V,U)*. 69[0:Inp] || O(U,V) -> SkP3(V,U)*. 70[0:Inp] || OV(U,V) -> SkP3(V,U)*. 71[0:Inp] || OpenContained(U,V) -> SkP4(V,U)*. 72[0:Inp] || FullyOutside(U,V) -> SkP4(V,U)*. 73[0:Inp] || OpenContainerShape(U,V) -> SkP4(V,U)*. 74[0:Inp] || UprightContainerShape(U,V) -> SkP4(V,U)*. 75[0:Inp] || Cavity(U,V) -> SkP5(V,U)*. 76[0:Inp] || PartiallyContained(U,V) -> SkP5(V,U)*. 77[0:Inp] || Moves(U,V,W)* -> Time(U). 78[0:Inp] || Moves(U,V,W)* -> Time(V). 79[0:Inp] || Moves(U,V,W)* -> Object(W). 80[0:Inp] || SkP6(U,V,W)* -> Time(W). 81[0:Inp] || SkP6(U,V,W)* -> Time(V). 82[0:Inp] || SkP6(U,V,W)* -> Object(U). 83[0:Inp] || Grasps(U,V,W)* -> Time(U). 84[0:Inp] || Grasps(U,V,W)* -> Time(V). 85[0:Inp] || Grasps(U,V,W)* -> Object(W). 86[0:Inp] || Constant(U,V,W)* -> Time(U). 87[0:Inp] || Constant(U,V,W)* -> Time(V). 88[0:Inp] || Constant(U,V,W)* -> History(W). 89[0:Inp] || SafeManipulate(U,V,W,X)* -> Time(U). 90[0:Inp] || SafeManipulate(U,V,W,X)* -> Time(V). 91[0:Inp] || SafeManipulate(U,V,W,X)* -> Object(W). 92[0:Inp] || SafeManipulate(U,V,W,X)* -> Region(X). 93[0:Inp] || DynamicUContainer(U,V,W,X)* -> Time(U). 94[0:Inp] || DynamicUContainer(U,V,W,X)* -> Time(V). 95[0:Inp] || DynamicUContainer(U,V,W,X)* -> Object(W). 96[0:Inp] || DynamicUContainer(U,V,W,X)* -> History(X). 97[0:Inp] || Leq3(U,V,W)* -> Leq(U,V). 98[0:Inp] || Leq3(U,V,W)* -> Leq(V,W). 99[0:Inp] || CContained(U,V,W) -> SkP0(W,V,U)*. 100[0:Inp] || UContained(U,V,W) -> SkP0(W,V,U)*. 101[0:Inp] || BLContained(U,V,W) -> SkP0(W,V,U)*. 102[0:Inp] || PreserveCContents(U,V,W) -> SkP1(W,V,U)*. 103[0:Inp] || PreserveUContents(U,V,W) -> SkP1(W,V,U)*. 104[0:Inp] || PreserveBoxWithLid(U,V,W) -> SkP1(W,V,U)*. 105[0:Inp] || StableThroughout(U,V,W) -> SkP6(W,V,U)*. 106[0:Inp] || Released(U,V,W) -> SkP6(W,V,U)*. 107[0:Inp] || Motionless(U,V,W) -> SkP6(W,V,U)*. 108[0:Inp] || Action(U) Action(V) -> Action(Sequence(U,V))*. 109[0:Inp] || Region(U) Region(V) -> Region(RUnion(U,V))*. 110[0:Inp] || Object(U) Object(V) -> ObjectSet(Pair(U,V))*. 111[0:Inp] || ObjectSet(U) ObjectSet(V) -> ObjectSet(Union(U,V))*. 112[0:Inp] || Time(U) Object(V) -> Region(Place(U,V))*. 113[0:Inp] || Time(U) Region(V) -> ObjectSet(Contents(U,V))*. 114[0:Inp] || Time(U) ObjectSet(V) -> ObjectSet(CContents(U,V))*. 115[0:Inp] || Time(U) ObjectSet(V) -> ObjectSet(UContents(U,V))*. 116[0:Inp] || Object(U) Region(V) -> Action(ManipTo(U,V))*. 117[0:Inp] || Time(U) History(V) -> Region(Slice(U,V))*. 118[0:Inp] || History(U) History(V) -> History(HUnion(U,V))*. 119[0:Inp] || Time(U) Object(V) -> ObjectSet(MovingGroup(U,V))*. 120[0:Inp] || Object(U) Object(V) -> Action(PutInUC(U,V))*. 121[0:Inp] || Object(U) Object(V) -> Action(LoadUprightContainer(U,V))*. 122[0:Inp] || Lt(U,V)* Lt(V,W)* -> Lt(U,W)*. 123[0:Inp] || Leq(U,V) Leq(W,U) -> Leq3(W,U,V)*. 124[0:Inp] || OSPlace(skc3,Pair(skc5,skc4),RUnion(Place(skc3,skc5),Place(skc3,skc4)))* -> . 125[0:Inp] || Lt(U,V) Time(U) Time(V) -> Leq(U,V)*. 126[0:Inp] || equal(U,V) Time(U) Time(V) -> Leq(U,V)*. 127[0:Inp] || OSPlace(U,V,W)* -> Element(skf7(V,X,Y),V)* P(W,Z)*. 128[0:Inp] || Region(U) Region(V) -> P(V,W)* equal(W,RUnion(U,V))*. 129[0:Inp] || Region(U) Region(V) -> P(U,W)* equal(W,RUnion(U,V))*. 130[0:Inp] || ObjectSet(U) Time(V) -> OSPlace(V,U,skf6(U,V))* equal(U,Null). 131[0:Inp] || Leq(U,V)* Time(U) Time(V) -> Lt(U,V) equal(U,V). 132[0:Inp] || Object(U) Element(U,V)* OSPlace(W,V,X)* -> P(Place(W,U),X)*. 133[0:Inp] || P(Place(U,skf7(V,W,U)),W)* OSPlace(U,V,X)* -> P(X,W)*. 134[0:Inp] || P(U,skf10(U,V,W))* -> Element(skf8(U,X,Y),Y)* OSPlace(X,Y,U). 135[0:Inp] || Region(U) Region(V) -> P(U,skf11(W,U,X))* equal(W,RUnion(U,V))*. 136[0:Inp] || Region(U) Region(V) -> P(V,skf11(W,U,V))* equal(W,RUnion(U,V)). 137[0:Inp] || equal(U,V) Object(V) Object(W) Object(U) -> Element(U,Pair(V,W))*. 138[0:Inp] || equal(U,V) Object(W) Object(V) Object(U) -> Element(U,Pair(W,V))*. 139[0:Inp] || P(U,skf11(U,V,W))* Region(X) Region(Y) -> equal(U,RUnion(X,Y))*. 140[0:Inp] || OSPlace(U,V,W)* ObjectSet(V) Time(U) -> equal(W,skf6(V,U)) equal(V,Null). 141[0:Inp] || P(U,skf10(U,V,W))* P(Place(X,skf8(U,X,Y)),U)* -> OSPlace(X,Y,U). 142[0:Inp] || Element(U,Pair(V,W))* Object(V) Object(W) Object(U) -> equal(U,V) equal(U,W). 143[0:Inp] || Element(U,V) -> Element(skf8(W,X,V),V)* P(Place(X,U),skf10(W,X,V))* OSPlace(X,V,W). 144[0:Inp] || P(Place(U,skf8(V,U,W)),V)* Element(X,W) -> P(Place(U,X),skf10(V,U,W))* OSPlace(U,W,V). 145[0:Inp] || equal(U,RUnion(V,W))* P(V,X)* P(W,X)* P(W,U)* P(V,U)* Region(V) Region(W) -> P(U,X)*. This is a first-order Non-Horn problem containing equality. This is a problem that contains sort information. The conjecture is ground. Axiom clauses: 141 Conjecture clauses: 4 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: skf11 > skf10 > skf8 > skf7 > skf4 > skf3 > skf2 > skf1 > skf6 > skf0 > LoadUprightContainer > PutInUC > MovingGroup > HUnion > Slice > ManipTo > UContents > CContents > Union > Pair > RUnion > Place > Contents > Sequence > skf9 > skf5 > HPlace > TravelTo > Singleton > ConvexHull > Leq3 > Leq > Lt > Action > SkP3 > History > OSPlace > Element > P > ObjectSet > Region > Object > Time > UprightContainer > SkP4 > FullyOutside > SkP2 > SmallSet > AllStable > EmptyHanded > Graspable > Reachable > SafelyMovable > SmallObject > BoxedIn > NoPartialContents > Occurs > CanGrasp > UprightContainerShape > SkP0 > UContained > SkP6 > Motionless > Released > Grasp > Moves > Feasible > SafeManipulate > SkP5 > PartiallyContained > SkP1 > PreserveCContents > PreserveUContents > PreserveBoxWithLid > Stable > StableThroughout > Fits > MuchSmaller > OMuchSmaller > OpenContainerShape > OpenContained > CContained > BLContained > DynamicUContainer > O > Cavity > Constant > Grasps > FeasiblePlace > OV > skc18 > skc17 > skc16 > skc15 > skc14 > skc13 > skc12 > skc11 > skc10 > skc9 > skc8 > skc7 > skc6 > skc5 > skc4 > skc3 > skc2 > skc1 > skc0 > Ru > Su > Ob > Oa > T > Null > Rc1 > Ra4 > Tm2 > Tb > Ra1 > Tm1 > Agent > Ox4 > Rc4 > Ob4 > Ta4 > StandStill Ordering : KBO Processed Problem: Worked Off Clauses: Usable Clauses: 4[0:Inp] || -> Action(StandStill)*. 3[0:Inp] || -> Time(skc3)*. 2[0:Inp] || -> Object(skc4)*. 1[0:Inp] || -> Object(skc5)*. 170[0:Res:2.0,13.0] || -> History(HPlace(skc4))*. 189[0:Res:1.0,13.0] || -> History(HPlace(skc5))*. 169[0:Res:2.0,11.0] || -> ObjectSet(Singleton(skc4))*. 188[0:Res:1.0,11.0] || -> ObjectSet(Singleton(skc5))*. 298[0:Obv:206.0] || -> Leq(skc3,skc3)*. 5[0:Inp] || Element(U,Null)* -> . 230[0:Res:2.0,197.0] || -> Action(LoadUprightContainer(skc4,skc5))*. 231[0:Res:2.0,196.0] || -> Action(PutInUC(skc4,skc5))*. 233[0:Res:2.0,187.0] || -> Action(LoadUprightContainer(skc5,skc4))*. 234[0:Res:2.0,186.0] || -> Action(PutInUC(skc5,skc4))*. 210[0:Res:3.0,195.0] || -> ObjectSet(MovingGroup(skc3,skc5))*. 212[0:Res:3.0,176.0] || -> ObjectSet(MovingGroup(skc3,skc4))*. 232[0:Res:2.0,193.0] || -> ObjectSet(Pair(skc4,skc5))*. 235[0:Res:2.0,184.0] || -> ObjectSet(Pair(skc5,skc4))*. 211[0:Res:3.0,194.0] || -> Region(Place(skc3,skc5))*. 213[0:Res:3.0,175.0] || -> Region(Place(skc3,skc4))*. 236[0:Res:2.0,178.0] || -> Action(LoadUprightContainer(skc4,skc4))*. 237[0:Res:2.0,177.0] || -> Action(PutInUC(skc4,skc4))*. 272[0:Res:1.0,197.0] || -> Action(LoadUprightContainer(skc5,skc5))*. 273[0:Res:1.0,196.0] || -> Action(PutInUC(skc5,skc5))*. 238[0:Res:2.0,174.0] || -> ObjectSet(Pair(skc4,skc4))*. 274[0:Res:1.0,193.0] || -> ObjectSet(Pair(skc5,skc5))*. 8[0:Inp] EmptyHanded(U) || -> Time(U)*. 7[0:Inp] AllStable(U) || -> Time(U)*. 6[0:Inp] SmallObject(U) || -> Object(U)*. 9[0:Inp] || -> Object(skf8(U,V,W))*. 13[0:Inp] Object(U) || -> History(HPlace(U))*. 12[0:Inp] Region(U) || -> Action(TravelTo(U))*. 11[0:Inp] Object(U) || -> ObjectSet(Singleton(U))*. 10[0:Inp] Region(U) || -> Region(ConvexHull(U))*. 15[0:Inp] || Feasible(U,V)* -> Action(V). 26[0:Inp] || SkP2(U,V)* -> ObjectSet(V). 17[0:Inp] || Element(U,V)* -> ObjectSet(V). 37[0:Inp] || MuchSmaller(U,V)* -> Region(V). 36[0:Inp] || MuchSmaller(U,V)* -> Region(U). 29[0:Inp] || OMuchSmaller(U,V)* -> Region(V). 25[0:Inp] || Reachable(U,V)* -> Region(V). 19[0:Inp] || FeasiblePlace(U,V)* -> Region(V). 23[0:Inp] || FullyOutside(U,V)* -> Region(V). 22[0:Inp] || FullyOutside(U,V)* -> Region(U). 35[0:Inp] || SkP5(U,V)* -> Region(U). 34[0:Inp] || SkP5(U,V)* -> Region(V). 27[0:Inp] || SkP2(U,V)* -> Region(U). 31[0:Inp] || SkP3(U,V)* -> Region(U). 30[0:Inp] || SkP3(U,V)* -> Region(V). 33[0:Inp] || SkP4(U,V)* -> Region(U). 32[0:Inp] || SkP4(U,V)* -> Region(V). 46[0:Inp] || Graspable(U,V)* -> Time(U). 44[0:Inp] || Grasp(U,V)* -> Time(U). 42[0:Inp] || CanGrasp(U,V)* -> Time(U). 40[0:Inp] || NoPartialContents(U,V)* -> Time(U). 38[0:Inp] || Stable(U,V)* -> Time(U). 24[0:Inp] || Reachable(U,V)* -> Time(U). 20[0:Inp] || SafelyMovable(U,V)* -> Time(U). 14[0:Inp] || Feasible(U,V)* -> Time(U). 47[0:Inp] || Graspable(U,V)* -> Object(V). 45[0:Inp] || Grasp(U,V)* -> Object(V). 43[0:Inp] || CanGrasp(U,V)* -> Object(V). 41[0:Inp] || NoPartialContents(U,V)* -> Object(V). 39[0:Inp] || Stable(U,V)* -> Object(V). 28[0:Inp] || OMuchSmaller(U,V)* -> Object(U). 21[0:Inp] || SafelyMovable(U,V)* -> Object(V). 18[0:Inp] || FeasiblePlace(U,V)* -> Object(U). 16[0:Inp] || Element(U,V)* -> Object(U). 76[0:Inp] || PartiallyContained(U,V) -> SkP5(V,U)*. 75[0:Inp] || Cavity(U,V) -> SkP5(V,U)*. 67[0:Inp] || SmallSet(U,V) -> SkP2(V,U)*. 66[0:Inp] || Fits(U,V) -> SkP2(V,U)*. 70[0:Inp] || OV(U,V) -> SkP3(V,U)*. 69[0:Inp] || O(U,V) -> SkP3(V,U)*. 68[0:Inp] || P(U,V) -> SkP3(V,U)*. 74[0:Inp] || UprightContainerShape(U,V) -> SkP4(V,U)*. 73[0:Inp] || OpenContainerShape(U,V) -> SkP4(V,U)*. 71[0:Inp] || OpenContained(U,V) -> SkP4(V,U)*. 72[0:Inp] || FullyOutside(U,V) -> SkP4(V,U)*. 88[0:Inp] || Constant(U,V,W)* -> History(W). 50[0:Inp] || Occurs(U,V,W)* -> Action(W). 52[0:Inp] || OSPlace(U,V,W)* -> ObjectSet(V). 56[0:Inp] || UprightContainer(U,V,W)* -> Region(W). 53[0:Inp] || OSPlace(U,V,W)* -> Region(W). 87[0:Inp] || Constant(U,V,W)* -> Time(V). 86[0:Inp] || Constant(U,V,W)* -> Time(U). 84[0:Inp] || Grasps(U,V,W)* -> Time(V). 83[0:Inp] || Grasps(U,V,W)* -> Time(U). 78[0:Inp] || Moves(U,V,W)* -> Time(V). 77[0:Inp] || Moves(U,V,W)* -> Time(U). 60[0:Inp] || BoxedIn(U,V,W)* -> Time(U). 54[0:Inp] || UprightContainer(U,V,W)* -> Time(U). 49[0:Inp] || Occurs(U,V,W)* -> Time(V). 48[0:Inp] || Occurs(U,V,W)* -> Time(U). 81[0:Inp] || SkP6(U,V,W)* -> Time(V). 80[0:Inp] || SkP6(U,V,W)* -> Time(W). 64[0:Inp] || SkP1(U,V,W)* -> Time(V). 63[0:Inp] || SkP1(U,V,W)* -> Time(W). 57[0:Inp] || SkP0(U,V,W)* -> Time(W). 51[0:Inp] || OSPlace(U,V,W)* -> Time(U). 85[0:Inp] || Grasps(U,V,W)* -> Object(W). 79[0:Inp] || Moves(U,V,W)* -> Object(W). 62[0:Inp] || BoxedIn(U,V,W)* -> Object(W). 61[0:Inp] || BoxedIn(U,V,W)* -> Object(V). 55[0:Inp] || UprightContainer(U,V,W)* -> Object(V). 82[0:Inp] || SkP6(U,V,W)* -> Object(U). 65[0:Inp] || SkP1(U,V,W)* -> Object(U). 59[0:Inp] || SkP0(U,V,W)* -> Object(U). 58[0:Inp] || SkP0(U,V,W)* -> Object(V). 166[0:Res:2.0,116.0] Region(U) || -> Action(ManipTo(skc4,U))*. 185[0:Res:1.0,116.0] Region(U) || -> Action(ManipTo(skc5,U))*. 167[0:Res:2.0,120.0] Object(U) || -> Action(PutInUC(skc4,U))*. 168[0:Res:2.0,121.0] Object(U) || -> Action(LoadUprightContainer(skc4,U))*. 186[0:Res:1.0,120.0] Object(U) || -> Action(PutInUC(skc5,U))*. 187[0:Res:1.0,121.0] Object(U) || -> Action(LoadUprightContainer(skc5,U))*. 154[0:Res:3.0,114.0] ObjectSet(U) || -> ObjectSet(CContents(skc3,U))*. 155[0:Res:3.0,115.0] ObjectSet(U) || -> ObjectSet(UContents(skc3,U))*. 153[0:Res:3.0,113.0] Region(U) || -> ObjectSet(Contents(skc3,U))*. 157[0:Res:3.0,119.0] Object(U) || -> ObjectSet(MovingGroup(skc3,U))*. 165[0:Res:2.0,110.0] Object(U) || -> ObjectSet(Pair(skc4,U))*. 184[0:Res:1.0,110.0] Object(U) || -> ObjectSet(Pair(skc5,U))*. 156[0:Res:3.0,117.0] History(U) || -> Region(Slice(skc3,U))*. 152[0:Res:3.0,112.0] Object(U) || -> Region(Place(skc3,U))*. 177[0:Res:2.0,120.1] Object(U) || -> Action(PutInUC(U,skc4))*. 178[0:Res:2.0,121.1] Object(U) || -> Action(LoadUprightContainer(U,skc4))*. 196[0:Res:1.0,120.1] Object(U) || -> Action(PutInUC(U,skc5))*. 197[0:Res:1.0,121.1] Object(U) || -> Action(LoadUprightContainer(U,skc5))*. 176[0:Res:2.0,119.1] Time(U) || -> ObjectSet(MovingGroup(U,skc4))*. 195[0:Res:1.0,119.1] Time(U) || -> ObjectSet(MovingGroup(U,skc5))*. 174[0:Res:2.0,110.1] Object(U) || -> ObjectSet(Pair(U,skc4))*. 193[0:Res:1.0,110.1] Object(U) || -> ObjectSet(Pair(U,skc5))*. 175[0:Res:2.0,112.1] Time(U) || -> Region(Place(U,skc4))*. 194[0:Res:1.0,112.1] Time(U) || -> Region(Place(U,skc5))*. 98[0:Inp] || Leq3(U,V,W)* -> Leq(V,W). 97[0:Inp] || Leq3(U,V,W)* -> Leq(U,V). 96[0:Inp] || DynamicUContainer(U,V,W,X)* -> History(X). 92[0:Inp] || SafeManipulate(U,V,W,X)* -> Region(X). 94[0:Inp] || DynamicUContainer(U,V,W,X)* -> Time(V). 93[0:Inp] || DynamicUContainer(U,V,W,X)* -> Time(U). 90[0:Inp] || SafeManipulate(U,V,W,X)* -> Time(V). 89[0:Inp] || SafeManipulate(U,V,W,X)* -> Time(U). 95[0:Inp] || DynamicUContainer(U,V,W,X)* -> Object(W). 91[0:Inp] || SafeManipulate(U,V,W,X)* -> Object(W). 300[0:Obv:223.1] Object(U) || -> Element(skc4,Pair(skc4,U))*. 306[0:Obv:257.1] Object(U) || -> Element(skc5,Pair(skc5,U))*. 303[0:Obv:250.1] Object(U) || -> Element(skc4,Pair(U,skc4))*. 309[0:Obv:286.1] Object(U) || -> Element(skc5,Pair(U,skc5))*. 107[0:Inp] || Motionless(U,V,W) -> SkP6(W,V,U)*. 106[0:Inp] || Released(U,V,W) -> SkP6(W,V,U)*. 105[0:Inp] || StableThroughout(U,V,W) -> SkP6(W,V,U)*. 104[0:Inp] || PreserveBoxWithLid(U,V,W) -> SkP1(W,V,U)*. 103[0:Inp] || PreserveUContents(U,V,W) -> SkP1(W,V,U)*. 102[0:Inp] || PreserveCContents(U,V,W) -> SkP1(W,V,U)*. 101[0:Inp] || BLContained(U,V,W) -> SkP0(W,V,U)*. 100[0:Inp] || UContained(U,V,W) -> SkP0(W,V,U)*. 99[0:Inp] || CContained(U,V,W) -> SkP0(W,V,U)*. 301[0:Obv:226.1] || Element(U,Pair(skc4,skc4))* -> equal(U,skc4). 307[0:Obv:260.1] || Element(U,Pair(skc5,skc5))* -> equal(U,skc5). 118[0:Inp] History(U) History(V) || -> History(HUnion(V,U))*. 108[0:Inp] Action(U) Action(V) || -> Action(Sequence(V,U))*. 116[0:Inp] Region(U) Object(V) || -> Action(ManipTo(V,U))*. 121[0:Inp] Object(U) Object(V) || -> Action(LoadUprightContainer(V,U))*. 120[0:Inp] Object(U) Object(V) || -> Action(PutInUC(V,U))*. 111[0:Inp] ObjectSet(U) ObjectSet(V) || -> ObjectSet(Union(V,U))*. 115[0:Inp] ObjectSet(U) Time(V) || -> ObjectSet(UContents(V,U))*. 114[0:Inp] ObjectSet(U) Time(V) || -> ObjectSet(CContents(V,U))*. 113[0:Inp] Region(U) Time(V) || -> ObjectSet(Contents(V,U))*. 119[0:Inp] Object(U) Time(V) || -> ObjectSet(MovingGroup(V,U))*. 110[0:Inp] Object(U) Object(V) || -> ObjectSet(Pair(V,U))*. 109[0:Inp] Region(U) Region(V) || -> Region(RUnion(V,U))*. 117[0:Inp] History(U) Time(V) || -> Region(Slice(V,U))*. 112[0:Inp] Object(U) Time(V) || -> Region(Place(V,U))*. 151[0:Res:3.0,126.0] Time(U) || equal(skc3,U) -> Leq(skc3,U)*. 150[0:Res:3.0,125.0] Time(U) || Lt(skc3,U) -> Leq(skc3,U)*. 161[0:Res:3.0,126.1] Time(U) || equal(U,skc3) -> Leq(U,skc3)*. 160[0:Res:3.0,125.1] Time(U) || Lt(U,skc3) -> Leq(U,skc3)*. 122[0:Inp] || Lt(U,V)* Lt(W,U)* -> Lt(W,V)*. 123[0:Inp] || Leq(U,V) Leq(V,W) -> Leq3(U,V,W)*. 159[0:Res:3.0,130.1] ObjectSet(U) || -> equal(U,Null) OSPlace(skc3,U,skf6(U,skc3))*. 215[0:Res:2.0,198.0] Object(U) || equal(skc5,skc4) -> Element(skc5,Pair(skc4,U))*. 249[0:Res:2.0,182.1] Object(U) || equal(skc5,skc4) -> Element(skc4,Pair(skc5,U))*. 214[0:Res:2.0,199.0] Object(U) || equal(skc5,U) -> Element(skc5,Pair(skc4,U))*. 248[0:Res:2.0,183.1] Object(U) || equal(skc4,U) -> Element(skc4,Pair(skc5,U))*. 244[0:Res:2.0,199.1] Object(U) || equal(skc5,skc4) -> Element(skc5,Pair(U,skc4))*. 246[0:Res:2.0,192.1] Object(U) || equal(skc5,skc4) -> Element(skc4,Pair(U,skc5))*. 245[0:Res:2.0,198.1] Object(U) || equal(skc5,U) -> Element(skc5,Pair(U,skc4))*. 247[0:Res:2.0,191.1] Object(U) || equal(skc4,U) -> Element(skc4,Pair(U,skc5))*. 216[0:Res:2.0,192.0] Object(U) || equal(U,skc5) -> Element(U,Pair(skc4,skc5))*. 217[0:Res:2.0,191.0] Object(U) || equal(U,skc4) -> Element(U,Pair(skc4,skc5))*. 219[0:Res:2.0,183.0] Object(U) || equal(U,skc4) -> Element(U,Pair(skc5,skc4))*. 220[0:Res:2.0,182.0] Object(U) || equal(U,skc5) -> Element(U,Pair(skc5,skc4))*. 224[0:Res:2.0,173.0] Object(U) || equal(U,skc4) -> Element(U,Pair(skc4,skc4))*. 258[0:Res:1.0,192.0] Object(U) || equal(U,skc5) -> Element(U,Pair(skc5,skc5))*. 218[0:Res:2.0,190.0] || Element(U,Pair(skc4,skc5))* -> equal(U,skc5) equal(U,skc4). 221[0:Res:2.0,181.0] || Element(U,Pair(skc5,skc4))* -> equal(U,skc4) equal(U,skc5). 124[0:Inp] || OSPlace(skc3,Pair(skc5,skc4),RUnion(Place(skc3,skc5),Place(skc3,skc4)))* -> . 125[0:Inp] Time(U) Time(V) || Lt(V,U) -> Leq(V,U)*. 126[0:Inp] Time(U) Time(V) || equal(V,U) -> Leq(V,U)*. 147[0:MRR:140.0,140.1,52.1,51.1] || OSPlace(U,V,W)* -> equal(V,Null) equal(W,skf6(V,U)). 149[0:Res:3.0,131.0] Time(U) || Leq(skc3,U)* -> equal(skc3,U) Lt(skc3,U). 158[0:Res:3.0,131.1] Time(U) || Leq(U,skc3)* -> equal(U,skc3) Lt(U,skc3). 129[0:Inp] Region(U) Region(V) || -> P(V,W)* equal(W,RUnion(V,U))*. 128[0:Inp] Region(U) Region(V) || -> P(U,W)* equal(W,RUnion(V,U))*. 146[0:MRR:132.0,16.1] || Element(U,V)* OSPlace(W,V,X)* -> P(Place(W,U),X)*. 127[0:Inp] || OSPlace(U,V,W)* -> P(W,X)* Element(skf7(V,Y,Z),V)*. 130[0:Inp] Time(U) ObjectSet(V) || -> equal(V,Null) OSPlace(U,V,skf6(V,U))*. 179[0:Res:2.0,137.2] Object(U) Object(V) || equal(skc4,V) -> Element(skc4,Pair(V,U))*. 180[0:Res:2.0,138.2] Object(U) Object(V) || equal(skc4,U) -> Element(skc4,Pair(V,U))*. 198[0:Res:1.0,137.2] Object(U) Object(V) || equal(skc5,V) -> Element(skc5,Pair(V,U))*. 199[0:Res:1.0,138.2] Object(U) Object(V) || equal(skc5,U) -> Element(skc5,Pair(V,U))*. 163[0:Res:2.0,137.0] Object(U) Object(V) || equal(U,skc4) -> Element(U,Pair(skc4,V))*. 182[0:Res:1.0,137.0] Object(U) Object(V) || equal(U,skc5) -> Element(U,Pair(skc5,V))*. 164[0:Res:2.0,138.0] Object(U) Object(V) || equal(U,V) -> Element(U,Pair(skc4,V))*. 183[0:Res:1.0,138.0] Object(U) Object(V) || equal(U,V) -> Element(U,Pair(skc5,V))*. 173[0:Res:2.0,138.1] Object(U) Object(V) || equal(U,skc4) -> Element(U,Pair(V,skc4))*. 192[0:Res:1.0,138.1] Object(U) Object(V) || equal(U,skc5) -> Element(U,Pair(V,skc5))*. 172[0:Res:2.0,137.1] Object(U) Object(V) || equal(U,V) -> Element(U,Pair(V,skc4))*. 191[0:Res:1.0,137.1] Object(U) Object(V) || equal(U,V) -> Element(U,Pair(V,skc5))*. 162[0:Res:2.0,148.0] Object(U) || Element(V,Pair(skc4,U))* -> equal(V,U) equal(V,skc4). 181[0:Res:1.0,148.0] Object(U) || Element(V,Pair(skc5,U))* -> equal(V,U) equal(V,skc5). 171[0:Res:2.0,148.1] Object(U) || Element(V,Pair(U,skc4))* -> equal(V,U) equal(V,skc4). 190[0:Res:1.0,148.1] Object(U) || Element(V,Pair(U,skc5))* -> equal(V,U) equal(V,skc5). 131[0:Inp] Time(U) Time(V) || Leq(V,U)* -> equal(V,U) Lt(V,U). 136[0:Inp] Region(U) Region(V) || -> equal(W,RUnion(V,U)) P(U,skf11(W,V,U))*. 135[0:Inp] Region(U) Region(V) || -> equal(W,RUnion(V,U))* P(V,skf11(W,V,X))*. 133[0:Inp] || P(Place(U,skf7(V,W,U)),W)* OSPlace(U,V,X)* -> P(X,W)*. 134[0:Inp] || P(U,skf10(U,V,W))* -> Element(skf8(U,X,Y),Y)* OSPlace(X,Y,U). 138[0:Inp] Object(U) Object(V) Object(W) || equal(U,V) -> Element(U,Pair(W,V))*. 137[0:Inp] Object(U) Object(V) Object(W) || equal(U,W) -> Element(U,Pair(W,V))*. 148[0:MRR:142.2,16.1] Object(U) Object(V) || Element(W,Pair(V,U))* -> equal(W,U) equal(W,V). 139[0:Inp] Region(U) Region(V) || P(W,skf11(W,X,Y))* -> equal(W,RUnion(V,U))*. 141[0:Inp] || P(U,skf10(U,V,W))* P(Place(X,skf8(U,X,Y)),U)* -> OSPlace(X,Y,U). 143[0:Inp] || Element(U,V) -> P(Place(W,U),skf10(X,W,V))* Element(skf8(X,W,V),V)* OSPlace(W,V,X). 144[0:Inp] || Element(U,V) P(Place(W,skf8(X,W,V)),X)* -> P(Place(W,U),skf10(X,W,V))* OSPlace(W,V,X). 145[0:Inp] Region(U) Region(V) || P(V,W)* P(V,X)* P(U,X)* P(U,W)* equal(X,RUnion(V,U))* -> P(X,W)*. Given clause: 4[0:Inp] || -> Action(StandStill)*. Given clause: 3[0:Inp] || -> Time(skc3)*. Given clause: 2[0:Inp] || -> Object(skc4)*. Given clause: 1[0:Inp] || -> Object(skc5)*. Given clause: 5[0:Inp] || Element(U,Null)* -> . Given clause: 170[0:Res:2.0,13.0] || -> History(HPlace(skc4))*. Given clause: 189[0:Res:1.0,13.0] || -> History(HPlace(skc5))*. Given clause: 169[0:Res:2.0,11.0] || -> ObjectSet(Singleton(skc4))*. Given clause: 188[0:Res:1.0,11.0] || -> ObjectSet(Singleton(skc5))*. Given clause: 8[0:Inp] EmptyHanded(U) || -> Time(U)*. Given clause: 298[0:Obv:206.0] || -> Leq(skc3,skc3)*. Given clause: 230[0:Res:2.0,197.0] || -> Action(LoadUprightContainer(skc4,skc5))*. Given clause: 231[0:Res:2.0,196.0] || -> Action(PutInUC(skc4,skc5))*. Given clause: 233[0:Res:2.0,187.0] || -> Action(LoadUprightContainer(skc5,skc4))*. Given clause: 7[0:Inp] AllStable(U) || -> Time(U)*. Given clause: 234[0:Res:2.0,186.0] || -> Action(PutInUC(skc5,skc4))*. Given clause: 210[0:Res:3.0,195.0] || -> ObjectSet(MovingGroup(skc3,skc5))*. Given clause: 212[0:Res:3.0,176.0] || -> ObjectSet(MovingGroup(skc3,skc4))*. Given clause: 232[0:Res:2.0,193.0] || -> ObjectSet(Pair(skc4,skc5))*. Given clause: 6[0:Inp] SmallObject(U) || -> Object(U)*. Given clause: 235[0:Res:2.0,184.0] || -> ObjectSet(Pair(skc5,skc4))*. Given clause: 211[0:Res:3.0,194.0] || -> Region(Place(skc3,skc5))*. Given clause: 213[0:Res:3.0,175.0] || -> Region(Place(skc3,skc4))*. Given clause: 236[0:Res:2.0,178.0] || -> Action(LoadUprightContainer(skc4,skc4))*. Given clause: 9[0:Inp] || -> Object(skf8(U,V,W))*. Given clause: 237[0:Res:2.0,177.0] || -> Action(PutInUC(skc4,skc4))*. Given clause: 272[0:Res:1.0,197.0] || -> Action(LoadUprightContainer(skc5,skc5))*. Given clause: 273[0:Res:1.0,196.0] || -> Action(PutInUC(skc5,skc5))*. Given clause: 238[0:Res:2.0,174.0] || -> ObjectSet(Pair(skc4,skc4))*. Given clause: 13[0:Inp] Object(U) || -> History(HPlace(U))*. Given clause: 274[0:Res:1.0,193.0] || -> ObjectSet(Pair(skc5,skc5))*. Given clause: 12[0:Inp] Region(U) || -> Action(TravelTo(U))*. Given clause: 11[0:Inp] Object(U) || -> ObjectSet(Singleton(U))*. Given clause: 10[0:Inp] Region(U) || -> Region(ConvexHull(U))*. Given clause: 15[0:Inp] || Feasible(U,V)* -> Action(V). Given clause: 26[0:Inp] || SkP2(U,V)* -> ObjectSet(V). Given clause: 17[0:Inp] || Element(U,V)* -> ObjectSet(V). Given clause: 37[0:Inp] || MuchSmaller(U,V)* -> Region(V). Given clause: 36[0:Inp] || MuchSmaller(U,V)* -> Region(U). Given clause: 29[0:Inp] || OMuchSmaller(U,V)* -> Region(V). Given clause: 25[0:Inp] || Reachable(U,V)* -> Region(V). Given clause: 19[0:Inp] || FeasiblePlace(U,V)* -> Region(V). Given clause: 23[0:Inp] || FullyOutside(U,V)* -> Region(V). Given clause: 22[0:Inp] || FullyOutside(U,V)* -> Region(U). Given clause: 35[0:Inp] || SkP5(U,V)* -> Region(U). Given clause: 34[0:Inp] || SkP5(U,V)* -> Region(V). Given clause: 27[0:Inp] || SkP2(U,V)* -> Region(U). Given clause: 31[0:Inp] || SkP3(U,V)* -> Region(U). Given clause: 30[0:Inp] || SkP3(U,V)* -> Region(V). Given clause: 33[0:Inp] || SkP4(U,V)* -> Region(U). Given clause: 32[0:Inp] || SkP4(U,V)* -> Region(V). Given clause: 46[0:Inp] || Graspable(U,V)* -> Time(U). Given clause: 44[0:Inp] || Grasp(U,V)* -> Time(U). Given clause: 42[0:Inp] || CanGrasp(U,V)* -> Time(U). Given clause: 40[0:Inp] || NoPartialContents(U,V)* -> Time(U). Given clause: 38[0:Inp] || Stable(U,V)* -> Time(U). Given clause: 24[0:Inp] || Reachable(U,V)* -> Time(U). Given clause: 20[0:Inp] || SafelyMovable(U,V)* -> Time(U). Given clause: 14[0:Inp] || Feasible(U,V)* -> Time(U). Given clause: 47[0:Inp] || Graspable(U,V)* -> Object(V). Given clause: 45[0:Inp] || Grasp(U,V)* -> Object(V). Given clause: 43[0:Inp] || CanGrasp(U,V)* -> Object(V). Given clause: 41[0:Inp] || NoPartialContents(U,V)* -> Object(V). Given clause: 39[0:Inp] || Stable(U,V)* -> Object(V). Given clause: 28[0:Inp] || OMuchSmaller(U,V)* -> Object(U). Given clause: 21[0:Inp] || SafelyMovable(U,V)* -> Object(V). Given clause: 18[0:Inp] || FeasiblePlace(U,V)* -> Object(U). Given clause: 16[0:Inp] || Element(U,V)* -> Object(U). Given clause: 166[0:Res:2.0,116.0] Region(U) || -> Action(ManipTo(skc4,U))*. Given clause: 76[0:Inp] || PartiallyContained(U,V) -> SkP5(V,U)*. Given clause: 312[0:Res:76.1,34.0] || PartiallyContained(U,V)* -> Region(U). Given clause: 313[0:Res:76.1,35.0] || PartiallyContained(U,V)* -> Region(V). Given clause: 185[0:Res:1.0,116.0] Region(U) || -> Action(ManipTo(skc5,U))*. Given clause: 167[0:Res:2.0,120.0] Object(U) || -> Action(PutInUC(skc4,U))*. Given clause: 75[0:Inp] || Cavity(U,V) -> SkP5(V,U)*. Given clause: 314[0:Res:75.1,34.0] || Cavity(U,V)* -> Region(U). Given clause: 315[0:Res:75.1,35.0] || Cavity(U,V)* -> Region(V). Given clause: 168[0:Res:2.0,121.0] Object(U) || -> Action(LoadUprightContainer(skc4,U))*. Given clause: 186[0:Res:1.0,120.0] Object(U) || -> Action(PutInUC(skc5,U))*. Given clause: 67[0:Inp] || SmallSet(U,V) -> SkP2(V,U)*. Given clause: 316[0:Res:67.1,27.0] || SmallSet(U,V)* -> Region(V). Given clause: 317[0:Res:67.1,26.0] || SmallSet(U,V)* -> ObjectSet(U). Given clause: 187[0:Res:1.0,121.0] Object(U) || -> Action(LoadUprightContainer(skc5,U))*. Given clause: 154[0:Res:3.0,114.0] ObjectSet(U) || -> ObjectSet(CContents(skc3,U))*. Given clause: 66[0:Inp] || Fits(U,V) -> SkP2(V,U)*. Given clause: 318[0:Res:66.1,27.0] || Fits(U,V)* -> Region(V). Given clause: 319[0:Res:66.1,26.0] || Fits(U,V)* -> ObjectSet(U). Given clause: 155[0:Res:3.0,115.0] ObjectSet(U) || -> ObjectSet(UContents(skc3,U))*. Given clause: 153[0:Res:3.0,113.0] Region(U) || -> ObjectSet(Contents(skc3,U))*. Given clause: 70[0:Inp] || OV(U,V) -> SkP3(V,U)*. Given clause: 320[0:Res:70.1,30.0] || OV(U,V)* -> Region(U). Given clause: 321[0:Res:70.1,31.0] || OV(U,V)* -> Region(V). Given clause: 157[0:Res:3.0,119.0] Object(U) || -> ObjectSet(MovingGroup(skc3,U))*. Given clause: 165[0:Res:2.0,110.0] Object(U) || -> ObjectSet(Pair(skc4,U))*. Given clause: 69[0:Inp] || O(U,V) -> SkP3(V,U)*. Given clause: 322[0:Res:69.1,30.0] || O(U,V)* -> Region(U). Given clause: 323[0:Res:69.1,31.0] || O(U,V)* -> Region(V). Given clause: 184[0:Res:1.0,110.0] Object(U) || -> ObjectSet(Pair(skc5,U))*. Given clause: 156[0:Res:3.0,117.0] History(U) || -> Region(Slice(skc3,U))*. Given clause: 68[0:Inp] || P(U,V) -> SkP3(V,U)*. Given clause: 324[0:Res:68.1,30.0] || P(U,V)* -> Region(U). Given clause: 325[0:Res:68.1,31.0] || P(U,V)* -> Region(V). Given clause: 152[0:Res:3.0,112.0] Object(U) || -> Region(Place(skc3,U))*. Given clause: 177[0:Res:2.0,120.1] Object(U) || -> Action(PutInUC(U,skc4))*. Given clause: 74[0:Inp] || UprightContainerShape(U,V) -> SkP4(V,U)*. Given clause: 329[0:Res:74.1,32.0] || UprightContainerShape(U,V)* -> Region(U). Given clause: 330[0:Res:74.1,33.0] || UprightContainerShape(U,V)* -> Region(V). Given clause: 178[0:Res:2.0,121.1] Object(U) || -> Action(LoadUprightContainer(U,skc4))*. Given clause: 196[0:Res:1.0,120.1] Object(U) || -> Action(PutInUC(U,skc5))*. Given clause: 73[0:Inp] || OpenContainerShape(U,V) -> SkP4(V,U)*. Given clause: 331[0:Res:73.1,32.0] || OpenContainerShape(U,V)* -> Region(U). Given clause: 332[0:Res:73.1,33.0] || OpenContainerShape(U,V)* -> Region(V). Given clause: 197[0:Res:1.0,121.1] Object(U) || -> Action(LoadUprightContainer(U,skc5))*. Given clause: 176[0:Res:2.0,119.1] Time(U) || -> ObjectSet(MovingGroup(U,skc4))*. Given clause: 71[0:Inp] || OpenContained(U,V) -> SkP4(V,U)*. Given clause: 333[0:Res:71.1,32.0] || OpenContained(U,V)* -> Region(U). Given clause: 334[0:Res:71.1,33.0] || OpenContained(U,V)* -> Region(V). Given clause: 195[0:Res:1.0,119.1] Time(U) || -> ObjectSet(MovingGroup(U,skc5))*. Given clause: 174[0:Res:2.0,110.1] Object(U) || -> ObjectSet(Pair(U,skc4))*. Given clause: 72[0:Inp] || FullyOutside(U,V) -> SkP4(V,U)*. Given clause: 193[0:Res:1.0,110.1] Object(U) || -> ObjectSet(Pair(U,skc5))*. Given clause: 175[0:Res:2.0,112.1] Time(U) || -> Region(Place(U,skc4))*. Given clause: 194[0:Res:1.0,112.1] Time(U) || -> Region(Place(U,skc5))*. Given clause: 88[0:Inp] || Constant(U,V,W)* -> History(W). Given clause: 50[0:Inp] || Occurs(U,V,W)* -> Action(W). Given clause: 52[0:Inp] || OSPlace(U,V,W)* -> ObjectSet(V). Given clause: 56[0:Inp] || UprightContainer(U,V,W)* -> Region(W). Given clause: 53[0:Inp] || OSPlace(U,V,W)* -> Region(W). Given clause: 87[0:Inp] || Constant(U,V,W)* -> Time(V). Given clause: 86[0:Inp] || Constant(U,V,W)* -> Time(U). Given clause: 84[0:Inp] || Grasps(U,V,W)* -> Time(V). Given clause: 83[0:Inp] || Grasps(U,V,W)* -> Time(U). Given clause: 78[0:Inp] || Moves(U,V,W)* -> Time(V). Given clause: 77[0:Inp] || Moves(U,V,W)* -> Time(U). Given clause: 60[0:Inp] || BoxedIn(U,V,W)* -> Time(U). Given clause: 54[0:Inp] || UprightContainer(U,V,W)* -> Time(U). Given clause: 49[0:Inp] || Occurs(U,V,W)* -> Time(V). Given clause: 48[0:Inp] || Occurs(U,V,W)* -> Time(U). Given clause: 81[0:Inp] || SkP6(U,V,W)* -> Time(V). Given clause: 80[0:Inp] || SkP6(U,V,W)* -> Time(W). Given clause: 64[0:Inp] || SkP1(U,V,W)* -> Time(V). Given clause: 63[0:Inp] || SkP1(U,V,W)* -> Time(W). Given clause: 57[0:Inp] || SkP0(U,V,W)* -> Time(W). Given clause: 51[0:Inp] || OSPlace(U,V,W)* -> Time(U). Given clause: 85[0:Inp] || Grasps(U,V,W)* -> Object(W). Given clause: 79[0:Inp] || Moves(U,V,W)* -> Object(W). Given clause: 62[0:Inp] || BoxedIn(U,V,W)* -> Object(W). Given clause: 61[0:Inp] || BoxedIn(U,V,W)* -> Object(V). Given clause: 55[0:Inp] || UprightContainer(U,V,W)* -> Object(V). Given clause: 82[0:Inp] || SkP6(U,V,W)* -> Object(U). Given clause: 65[0:Inp] || SkP1(U,V,W)* -> Object(U). Given clause: 59[0:Inp] || SkP0(U,V,W)* -> Object(U). Given clause: 58[0:Inp] || SkP0(U,V,W)* -> Object(V). Given clause: 300[0:Obv:223.1] Object(U) || -> Element(skc4,Pair(skc4,U))*. Given clause: 98[0:Inp] || Leq3(U,V,W)* -> Leq(V,W). Given clause: 306[0:Obv:257.1] Object(U) || -> Element(skc5,Pair(skc5,U))*. Given clause: 303[0:Obv:250.1] Object(U) || -> Element(skc4,Pair(U,skc4))*. Given clause: 309[0:Obv:286.1] Object(U) || -> Element(skc5,Pair(U,skc5))*. Given clause: 97[0:Inp] || Leq3(U,V,W)* -> Leq(U,V). Given clause: 96[0:Inp] || DynamicUContainer(U,V,W,X)* -> History(X). Given clause: 92[0:Inp] || SafeManipulate(U,V,W,X)* -> Region(X). Given clause: 94[0:Inp] || DynamicUContainer(U,V,W,X)* -> Time(V). Given clause: 93[0:Inp] || DynamicUContainer(U,V,W,X)* -> Time(U). Given clause: 90[0:Inp] || SafeManipulate(U,V,W,X)* -> Time(V). Given clause: 89[0:Inp] || SafeManipulate(U,V,W,X)* -> Time(U). Given clause: 95[0:Inp] || DynamicUContainer(U,V,W,X)* -> Object(W). Given clause: 91[0:Inp] || SafeManipulate(U,V,W,X)* -> Object(W). Given clause: 301[0:Obv:226.1] || Element(U,Pair(skc4,skc4))* -> equal(U,skc4). Given clause: 307[0:Obv:260.1] || Element(U,Pair(skc5,skc5))* -> equal(U,skc5). Given clause: 107[0:Inp] || Motionless(U,V,W) -> SkP6(W,V,U)*. Given clause: 349[0:Res:107.1,82.0] || Motionless(U,V,W)* -> Object(W). Given clause: 350[0:Res:107.1,80.0] || Motionless(U,V,W)* -> Time(U). Given clause: 351[0:Res:107.1,81.0] || Motionless(U,V,W)* -> Time(V). Given clause: 106[0:Inp] || Released(U,V,W) -> SkP6(W,V,U)*. Given clause: 105[0:Inp] || StableThroughout(U,V,W) -> SkP6(W,V,U)*. Given clause: 352[0:Res:106.1,82.0] || Released(U,V,W)* -> Object(W). Given clause: 353[0:Res:106.1,80.0] || Released(U,V,W)* -> Time(U). Given clause: 354[0:Res:106.1,81.0] || Released(U,V,W)* -> Time(V). Given clause: 355[0:Res:105.1,82.0] || StableThroughout(U,V,W)* -> Object(W). Given clause: 104[0:Inp] || PreserveBoxWithLid(U,V,W) -> SkP1(W,V,U)*. Given clause: 356[0:Res:105.1,80.0] || StableThroughout(U,V,W)* -> Time(U). Given clause: 357[0:Res:105.1,81.0] || StableThroughout(U,V,W)* -> Time(V). Given clause: 358[0:Res:104.1,65.0] || PreserveBoxWithLid(U,V,W)* -> Object(W). Given clause: 359[0:Res:104.1,63.0] || PreserveBoxWithLid(U,V,W)* -> Time(U). Given clause: 103[0:Inp] || PreserveUContents(U,V,W) -> SkP1(W,V,U)*. Given clause: 360[0:Res:104.1,64.0] || PreserveBoxWithLid(U,V,W)* -> Time(V). Given clause: 361[0:Res:103.1,65.0] || PreserveUContents(U,V,W)* -> Object(W). Given clause: 362[0:Res:103.1,63.0] || PreserveUContents(U,V,W)* -> Time(U). Given clause: 363[0:Res:103.1,64.0] || PreserveUContents(U,V,W)* -> Time(V). Given clause: 102[0:Inp] || PreserveCContents(U,V,W) -> SkP1(W,V,U)*. Given clause: 364[0:Res:102.1,65.0] || PreserveCContents(U,V,W)* -> Object(W). Given clause: 365[0:Res:102.1,63.0] || PreserveCContents(U,V,W)* -> Time(U). Given clause: 366[0:Res:102.1,64.0] || PreserveCContents(U,V,W)* -> Time(V). Given clause: 101[0:Inp] || BLContained(U,V,W) -> SkP0(W,V,U)*. Given clause: 100[0:Inp] || UContained(U,V,W) -> SkP0(W,V,U)*. Given clause: 367[0:Res:101.1,58.0] || BLContained(U,V,W)* -> Object(V). Given clause: 368[0:Res:101.1,59.0] || BLContained(U,V,W)* -> Object(W). Given clause: 369[0:Res:101.1,57.0] || BLContained(U,V,W)* -> Time(U). Given clause: 370[0:Res:100.1,58.0] || UContained(U,V,W)* -> Object(V). Given clause: 99[0:Inp] || CContained(U,V,W) -> SkP0(W,V,U)*. Given clause: 371[0:Res:100.1,59.0] || UContained(U,V,W)* -> Object(W). Given clause: 372[0:Res:100.1,57.0] || UContained(U,V,W)* -> Time(U). Given clause: 373[0:Res:99.1,58.0] || CContained(U,V,W)* -> Object(V). Given clause: 374[0:Res:99.1,59.0] || CContained(U,V,W)* -> Object(W). Given clause: 118[0:Inp] History(U) History(V) || -> History(HUnion(V,U))*. Given clause: 375[0:Res:99.1,57.0] || CContained(U,V,W)* -> Time(U). Given clause: 151[0:Res:3.0,126.0] Time(U) || equal(skc3,U) -> Leq(skc3,U)*. Given clause: 150[0:Res:3.0,125.0] Time(U) || Lt(skc3,U) -> Leq(skc3,U)*. Given clause: 161[0:Res:3.0,126.1] Time(U) || equal(U,skc3) -> Leq(U,skc3)*. Given clause: 108[0:Inp] Action(U) Action(V) || -> Action(Sequence(V,U))*. Given clause: 160[0:Res:3.0,125.1] Time(U) || Lt(U,skc3) -> Leq(U,skc3)*. Given clause: 116[0:Inp] Region(U) Object(V) || -> Action(ManipTo(V,U))*. Given clause: 121[0:Inp] Object(U) Object(V) || -> Action(LoadUprightContainer(V,U))*. Given clause: 120[0:Inp] Object(U) Object(V) || -> Action(PutInUC(V,U))*. Given clause: 111[0:Inp] ObjectSet(U) ObjectSet(V) || -> ObjectSet(Union(V,U))*. Given clause: 115[0:Inp] ObjectSet(U) Time(V) || -> ObjectSet(UContents(V,U))*. Given clause: 114[0:Inp] ObjectSet(U) Time(V) || -> ObjectSet(CContents(V,U))*. Given clause: 113[0:Inp] Region(U) Time(V) || -> ObjectSet(Contents(V,U))*. Given clause: 119[0:Inp] Object(U) Time(V) || -> ObjectSet(MovingGroup(V,U))*. Given clause: 110[0:Inp] Object(U) Object(V) || -> ObjectSet(Pair(V,U))*. Given clause: 109[0:Inp] Region(U) Region(V) || -> Region(RUnion(V,U))*. Given clause: 117[0:Inp] History(U) Time(V) || -> Region(Slice(V,U))*. Given clause: 112[0:Inp] Object(U) Time(V) || -> Region(Place(V,U))*. Given clause: 122[0:Inp] || Lt(U,V)*+ Lt(W,U)* -> Lt(W,V)*. Given clause: 123[0:Inp] || Leq(U,V) Leq(V,W) -> Leq3(U,V,W)*. Given clause: 215[0:Res:2.0,198.0] Object(U) || equal(skc5,skc4) -> Element(skc5,Pair(skc4,U))*. Given clause: 249[0:Res:2.0,182.1] Object(U) || equal(skc5,skc4) -> Element(skc4,Pair(skc5,U))*. Given clause: 244[0:Res:2.0,199.1] Object(U) || equal(skc5,skc4) -> Element(skc5,Pair(U,skc4))*. Given clause: 246[0:Res:2.0,192.1] Object(U) || equal(skc5,skc4) -> Element(skc4,Pair(U,skc5))*. Given clause: 124[0:Inp] || OSPlace(skc3,Pair(skc5,skc4),RUnion(Place(skc3,skc5),Place(skc3,skc4)))* -> . Given clause: 214[0:Res:2.0,199.0] Object(U) || equal(skc5,U) -> Element(skc5,Pair(skc4,U))*. Given clause: 248[0:Res:2.0,183.1] Object(U) || equal(skc4,U) -> Element(skc4,Pair(skc5,U))*. Given clause: 245[0:Res:2.0,198.1] Object(U) || equal(skc5,U) -> Element(skc5,Pair(U,skc4))*. Given clause: 247[0:Res:2.0,191.1] Object(U) || equal(skc4,U) -> Element(skc4,Pair(U,skc5))*. Given clause: 125[0:Inp] Time(U) Time(V) || Lt(V,U) -> Leq(V,U)*. Given clause: 216[0:Res:2.0,192.0] Object(U) || equal(U,skc5) -> Element(U,Pair(skc4,skc5))*. Given clause: 217[0:Res:2.0,191.0] Object(U) || equal(U,skc4) -> Element(U,Pair(skc4,skc5))*. Given clause: 219[0:Res:2.0,183.0] Object(U) || equal(U,skc4) -> Element(U,Pair(skc5,skc4))*. Given clause: 220[0:Res:2.0,182.0] Object(U) || equal(U,skc5) -> Element(U,Pair(skc5,skc4))*. Given clause: 126[0:Inp] Time(U) Time(V) || equal(V,U) -> Leq(V,U)*. Given clause: 224[0:Res:2.0,173.0] Object(U) || equal(U,skc4) -> Element(U,Pair(skc4,skc4))*. Given clause: 258[0:Res:1.0,192.0] Object(U) || equal(U,skc5) -> Element(U,Pair(skc5,skc5))*. Given clause: 218[0:Res:2.0,190.0] || Element(U,Pair(skc4,skc5))* -> equal(U,skc5) equal(U,skc4). Given clause: 221[0:Res:2.0,181.0] || Element(U,Pair(skc5,skc4))* -> equal(U,skc4) equal(U,skc5). Given clause: 147[0:MRR:140.0,140.1,52.1,51.1] || OSPlace(U,V,W)* -> equal(V,Null) equal(W,skf6(V,U)). Given clause: 159[0:Res:3.0,130.1] ObjectSet(U) || -> equal(U,Null) OSPlace(skc3,U,skf6(U,skc3))*. Given clause: 434[0:Res:159.2,53.0] ObjectSet(U) || -> equal(U,Null) Region(skf6(U,skc3))*. Given clause: 149[0:Res:3.0,131.0] Time(U) || Leq(skc3,U)* -> equal(skc3,U) Lt(skc3,U). Given clause: 158[0:Res:3.0,131.1] Time(U) || Leq(U,skc3)* -> equal(U,skc3) Lt(U,skc3). Given clause: 129[0:Inp] Region(U) Region(V) || -> P(V,W)* equal(W,RUnion(V,U))*. Given clause: 541[0:MRR:540.1,325.0] Region(U) || -> Region(V)*. Given clause: 658[0:EmS:541.0,213.0] || -> Region(U)*. Given clause: 660[0:MRR:12.0,658.0] || -> Action(TravelTo(U))*. Given clause: 661[0:MRR:166.0,658.0] || -> Action(ManipTo(skc4,U))*. Given clause: 664[0:MRR:116.0,658.0] Object(U) || -> Action(ManipTo(U,V))*. Given clause: 662[0:MRR:185.0,658.0] || -> Action(ManipTo(skc5,U))*. Given clause: 663[0:MRR:153.0,658.0] || -> ObjectSet(Contents(skc3,U))*. Given clause: 665[0:MRR:113.0,658.0] Time(U) || -> ObjectSet(Contents(U,V))*. Given clause: 704[0:MRR:589.0,658.0] || -> P(U,TravelTo(V))* Action(RUnion(U,W))*. Given clause: 666[0:MRR:542.0,658.0] || -> P(U,V)* equal(V,RUnion(U,W))*. Given clause: 668[0:MRR:544.0,658.0] || -> P(U,V)* equal(V,RUnion(W,U))*. Given clause: 915[0:SpR:668.1,660.0] || -> P(U,TravelTo(V))* Action(RUnion(W,U))*. Given clause: 670[0:MRR:548.0,658.0] || -> P(U,LoadUprightContainer(skc4,skc5))* Action(RUnion(U,V))*. Given clause: 671[0:MRR:549.0,658.0] || -> P(U,LoadUprightContainer(skc5,skc5))* Action(RUnion(U,V))*. Given clause: 700[0:MRR:545.0,658.0] || -> equal(U,RUnion(V,W)) P(W,skf11(U,V,W))*. Given clause: 672[0:MRR:550.0,658.0] || -> P(U,LoadUprightContainer(skc5,skc4))* Action(RUnion(U,V))*. Given clause: 673[0:MRR:551.0,658.0] || -> P(U,LoadUprightContainer(skc4,skc4))* Action(RUnion(U,V))*. Given clause: 674[0:MRR:552.0,658.0] || -> P(U,PutInUC(skc4,skc5))* Action(RUnion(U,V))*. Given clause: 675[0:MRR:553.0,658.0] || -> P(U,PutInUC(skc5,skc5))* Action(RUnion(U,V))*. Given clause: 701[0:MRR:546.0,658.0] || -> equal(U,RUnion(V,W))* P(V,skf11(U,V,X))*. Given clause: 676[0:MRR:554.0,658.0] || -> P(U,PutInUC(skc5,skc4))* Action(RUnion(U,V))*. Given clause: 677[0:MRR:555.0,658.0] || -> P(U,PutInUC(skc4,skc4))* Action(RUnion(U,V))*. Given clause: 678[0:MRR:556.0,658.0] || -> P(U,MovingGroup(skc3,skc5))* ObjectSet(RUnion(U,V))*. Given clause: 679[0:MRR:557.0,658.0] || -> P(U,MovingGroup(skc3,skc4))* ObjectSet(RUnion(U,V))*. Given clause: 710[0:MRR:547.0,658.0] || P(U,skf11(U,V,W))*+ -> equal(U,RUnion(X,Y))*. Given clause: 680[0:MRR:558.0,658.0] || -> P(U,Pair(skc4,skc5))* ObjectSet(RUnion(U,V))*. Given clause: 681[0:MRR:559.0,658.0] || -> P(U,Pair(skc5,skc5))* ObjectSet(RUnion(U,V))*. Given clause: 682[0:MRR:560.0,658.0] || -> P(U,Pair(skc5,skc4))* ObjectSet(RUnion(U,V))*. Given clause: 683[0:MRR:561.0,658.0] || -> P(U,Pair(skc4,skc4))* ObjectSet(RUnion(U,V))*. Given clause: 1130[0:Rew:1127.0,710.0] || P(U,U)*+ -> equal(U,RUnion(V,W))*. Given clause: 852[0:SpR:668.1,230.0] || -> P(U,LoadUprightContainer(skc4,skc5))* Action(RUnion(V,U))*. Given clause: 853[0:SpR:668.1,272.0] || -> P(U,LoadUprightContainer(skc5,skc5))* Action(RUnion(V,U))*. Given clause: 855[0:SpR:668.1,233.0] || -> P(U,LoadUprightContainer(skc5,skc4))* Action(RUnion(V,U))*. Given clause: 856[0:SpR:668.1,236.0] || -> P(U,LoadUprightContainer(skc4,skc4))* Action(RUnion(V,U))*. Given clause: 146[0:MRR:132.0,16.1] || Element(U,V)* OSPlace(W,V,X)*+ -> P(Place(W,U),X)*. Given clause: 861[0:SpR:668.1,231.0] || -> P(U,PutInUC(skc4,skc5))* Action(RUnion(V,U))*. Given clause: 862[0:SpR:668.1,273.0] || -> P(U,PutInUC(skc5,skc5))* Action(RUnion(V,U))*. Given clause: 864[0:SpR:668.1,234.0] || -> P(U,PutInUC(skc5,skc4))* Action(RUnion(V,U))*. Given clause: 865[0:SpR:668.1,237.0] || -> P(U,PutInUC(skc4,skc4))* Action(RUnion(V,U))*. Given clause: 127[0:Inp] || OSPlace(U,V,W)*+ -> P(W,X)* Element(skf7(V,Y,Z),V)*. Given clause: 870[0:SpR:668.1,210.0] || -> P(U,MovingGroup(skc3,skc5))* ObjectSet(RUnion(V,U))*. Given clause: 871[0:SpR:668.1,212.0] || -> P(U,MovingGroup(skc3,skc4))* ObjectSet(RUnion(V,U))*. Given clause: 876[0:SpR:668.1,232.0] || -> P(U,Pair(skc4,skc5))* ObjectSet(RUnion(V,U))*. Given clause: 879[0:SpR:668.1,274.0] || -> P(U,Pair(skc5,skc5))* ObjectSet(RUnion(V,U))*. Given clause: 130[0:Inp] Time(U) ObjectSet(V) || -> equal(V,Null) OSPlace(U,V,skf6(V,U))*. Given clause: 885[0:SpR:668.1,235.0] || -> P(U,Pair(skc5,skc4))* ObjectSet(RUnion(V,U))*. Given clause: 888[0:SpR:668.1,238.0] || -> P(U,Pair(skc4,skc4))* ObjectSet(RUnion(V,U))*. Given clause: 727[0:MRR:606.0,658.0] || -> P(U,ManipTo(skc4,V))* Action(RUnion(U,W))*. Given clause: 728[0:MRR:607.0,658.0] || -> P(U,ManipTo(skc5,V))* Action(RUnion(U,W))*. Given clause: 131[0:Inp] Time(U) Time(V) || Leq(V,U)* -> equal(V,U) Lt(V,U). Given clause: 731[0:MRR:610.0,658.0] || -> P(U,Contents(skc3,V))* ObjectSet(RUnion(U,W))*. Given clause: 917[0:SpR:668.1,661.0] || -> P(U,ManipTo(skc4,V))* Action(RUnion(W,U))*. Given clause: 918[0:SpR:668.1,662.0] || -> P(U,ManipTo(skc5,V))* Action(RUnion(W,U))*. Given clause: 920[0:SpR:668.1,663.0] || -> P(U,Contents(skc3,V))* ObjectSet(RUnion(W,U))*. Given clause: 133[0:Inp] || P(Place(U,skf7(V,W,U)),W)*+ OSPlace(U,V,X)* -> P(X,W)*. Given clause: 922[0:SpR:668.1,704.1] || -> P(U,V)* P(W,TravelTo(X))* Action(V). Given clause: 1458[1:Spt:922.0,922.2] || -> P(U,V)* Action(V). Given clause: 1459[1:Res:1458.0,1130.0] || -> Action(U)* equal(U,RUnion(V,W))*. Given clause: 1653[1:Obv:1607.0] || -> P(U,TravelTo(V))* Action(W)*. Given clause: 1697[2:Spt:1653.1] || -> Action(U)*. Given clause: 923[0:SpR:668.1,666.1] || -> P(U,V)* P(W,X)* equal(X,V)*. Given clause: 134[0:Inp] || P(U,skf10(U,V,W))*+ -> Element(skf8(U,X,Y),Y)* OSPlace(X,Y,U). Given clause: 1109[0:SpR:668.1,678.1] || -> P(U,V)* P(W,MovingGroup(skc3,skc5))* ObjectSet(V). Given clause: 1911[3:Spt:1109.0,1109.2] || -> P(U,V)* ObjectSet(V). Given clause: 1912[3:Res:1911.0,1130.0] || -> ObjectSet(U)* equal(U,RUnion(V,W))*. Given clause: 2020[3:Obv:1994.0] || -> P(U,Pair(skc4,skc4))* ObjectSet(V)*. Given clause: 2047[4:Spt:2020.1] || -> ObjectSet(U)*. Given clause: 2049[4:MRR:159.0,2047.0] || -> equal(U,Null) OSPlace(skc3,U,skf6(U,skc3))*. Given clause: 2048[4:MRR:130.1,2047.0] Time(U) || -> equal(V,Null) OSPlace(U,V,skf6(V,U))*. Given clause: 698[0:MRR:562.0,658.0] || -> P(U,skf8(V,W,X))* Object(RUnion(U,Y))*. Given clause: 903[0:SpR:668.1,9.0] || -> P(U,skf8(V,W,X))* Object(RUnion(Y,U))*. Given clause: 1125[0:Res:700.1,710.0] || -> equal(RUnion(U,V),V)** equal(V,RUnion(W,X))*. Given clause: 2283[0:MRR:2165.0,2169.0] || -> equal(U,V)*. SPASS V 3.7 SPASS beiseite: Proof found. Problem: g.dfg SPASS derived 2075 clauses, backtracked 0 clauses, performed 4 splits and kept 1249 clauses. SPASS allocated 53911 KBytes. SPASS spent 0:00:00.22 on the problem. 0:00:00.01 for the input. 0:00:00.04 for the FLOTTER CNF translation. 0:00:00.01 for inferences. 0:00:00.00 for the backtracking. 0:00:00.12 for the reduction. Here is a proof with depth 3, length 44 : 1[0:Inp] || -> Object(skc5)*. 2[0:Inp] || -> Object(skc4)*. 3[0:Inp] || -> Time(skc3)*. 5[0:Inp] || Element(U,Null)* -> . 31[0:Inp] || SkP3(U,V)* -> Region(U). 68[0:Inp] || P(U,V) -> SkP3(V,U)*. 109[0:Inp] Region(U) Region(V) || -> Region(RUnion(V,U))*. 112[0:Inp] Object(U) Time(V) || -> Region(Place(V,U))*. 128[0:Inp] Region(U) Region(V) || -> P(U,W)* equal(W,RUnion(V,U))*. 129[0:Inp] Region(U) Region(V) || -> P(V,W)* equal(W,RUnion(V,U))*. 136[0:Inp] Region(U) Region(V) || -> equal(W,RUnion(V,U)) P(U,skf11(W,V,U))*. 138[0:Inp] Object(U) Object(V) Object(W) || equal(U,V) -> Element(U,Pair(W,V))*. 139[0:Inp] Region(U) Region(V) || P(W,skf11(W,X,Y))* -> equal(W,RUnion(V,U))*. 175[0:Res:2.0,112.1] Time(U) || -> Region(Place(U,skc4))*. 199[0:Res:1.0,138.2] Object(U) Object(V) || equal(skc5,U) -> Element(skc5,Pair(V,U))*. 213[0:Res:3.0,175.0] || -> Region(Place(skc3,skc4))*. 244[0:Res:2.0,199.1] Object(U) || equal(skc5,skc4) -> Element(skc5,Pair(U,skc4))*. 325[0:Res:68.1,31.0] || P(U,V)* -> Region(V). 528[0:SpR:129.3,109.2] Region(U) Region(V) Region(U) Region(V) || -> P(V,W)* Region(W). 539[0:Obv:528.1] Region(U) Region(V) || -> P(V,W)* Region(W). 540[0:Con:539.0] Region(U) || -> P(U,V)* Region(V). 541[0:MRR:540.1,325.0] Region(U) || -> Region(V)*. 542[0:MRR:129.0,541.1] Region(U) || -> P(U,V)* equal(V,RUnion(U,W))*. 544[0:MRR:128.1,541.1] Region(U) || -> P(U,V)* equal(V,RUnion(W,U))*. 545[0:MRR:136.1,541.1] Region(U) || -> equal(V,RUnion(W,U)) P(U,skf11(V,W,U))*. 547[0:MRR:139.1,541.1] Region(U) || P(V,skf11(V,W,X))* -> equal(V,RUnion(Y,U))*. 658[0:EmS:541.0,213.0] || -> Region(U)*. 666[0:MRR:542.0,658.0] || -> P(U,V)* equal(V,RUnion(U,W))*. 668[0:MRR:544.0,658.0] || -> P(U,V)* equal(V,RUnion(W,U))*. 700[0:MRR:545.0,658.0] || -> equal(U,RUnion(V,W)) P(W,skf11(U,V,W))*. 710[0:MRR:547.0,658.0] || P(U,skf11(U,V,W))*+ -> equal(U,RUnion(X,Y))*. 1123[0:Res:668.0,710.0] || -> equal(skf11(U,V,W),RUnion(X,U))* equal(U,RUnion(Y,Z))*. 1125[0:Res:700.1,710.0] || -> equal(RUnion(U,V),V)** equal(V,RUnion(W,X))*. 1127[0:Rew:1125.0,1123.0] || -> equal(skf11(U,V,W),U)** equal(U,RUnion(X,Y))*. 1130[0:Rew:1127.0,710.0] || P(U,U)*+ -> equal(U,RUnion(V,W))*. 2110[0:Fac:1125.0,1125.1] || -> equal(RUnion(U,V),V)**. 2165[0:Rew:2110.0,1130.1] || P(U,U)* -> equal(U,V)*. 2169[0:Rew:2110.0,666.1] || -> P(U,V)* equal(V,W)*. 2283[0:MRR:2165.0,2169.0] || -> equal(U,V)*. 2295[0:SpR:2283.0,2.0] || -> Object(U)*. 2391[0:SpR:2283.0,244.2] Object(U) || equal(skc5,skc4) -> Element(V,Pair(U,skc4))*. 2415[0:SpL:2283.0,5.0] || Element(U,V)* -> . 2751[0:MRR:2391.0,2391.2,2295.0,2415.0] || equal(skc5,skc4)** -> . 2752[0:UnC:2751.0,2283.0] || -> . Formulae used in the proof : Lem5G OSD1 axiom35 axiom1 axiom6 SBD6b OSD4 --------------------------SPASS-STOP------------------------------