begin_problem(Scenario4b). list_of_descriptions. name({*Qualitative Reasoning About Containers - Case 4b*}). author({*Professor Ernest Davis, Angelica Chen, Casey McGinley, Noah Frazier-Logue*}). status(unsatisfiable). description({*12 July 2016*}). end_of_list. list_of_symbols. functions[(Sequence,2), (Contents,2), (Place,2), (RUnion,2), (ConvexHull,1), (Singleton,1), (Pair,2), (Union,2), (CContents,2), (UContents,2), (TravelTo,1), (StandStill,0), (ManipTo,2), (Slice,2), (HPlace,1), (HUnion,2), (MovingGroup,2), (PutInUC,2), (LoadUprightContainer,2), (Place,2), (Union,2), (UContents,2), (Contents,2), (MovingGroup,2), (Ta4,0), (Ob4,0), (Rc4,0), (Ox4,0), (Agent,0), (TravelTo,1), (Tm1,0), (Ra1,0), (PutInUC,2), (LoadUprightContainer,2), (Sequence,2), (HPlace,1), (Slice,2), (StandStill,0), (Ta4,0), (Tb,0), (Tm1,0), (Tm2,0), (Ra4,0), (Rc1,0), (Rq,0), (Rx1,0), (Ox,0), (Rc2,0), (Hc1,0), (Tc,0)]. predicates[(Time,1), (Object,1), (Region,1), (UprightContainer,3), (FullyOutside,2), (SmallSet,2), (ObjectSet,1), (AllStable,1), (EmptyHanded,1), (Graspable,2), (Reachable,2), (FullyOutside,2), (SafelyMovable,2), (SmallObject,1), (BoxedIn,3), (NoPartialContents,2), (Occurs,3), (Action,1), (CanGrasp,2), (UprightContainerShape,2), (UContained,3), (P,2), (Element,2), (Lt,2), (Leq,2), (Leq3, 3), (Motionless,3), (Released,3), (Grasp,2), (Moves,3), (Feasible,2), (SafeManipulate,4), (PartiallyContained,2), (OSPlace,3), (PreserveCContents,3), (PreserveUContents,3), (PreserveBoxWithLid,3), (Stable,2), (StableThroughout,3), (SmallSet,2), (Fits,2), (MuchSmaller,2), (OMuchSmaller,2), (OpenContainerShape,2), (OpenContained,2), (CContained,3), (BLContained,3), (DynamicUContainer,4), (O,2), (Cavity,2), (History,1), (Constant,3), (Grasps,3), (FeasiblePlace,2), (OV,2)]. end_of_list. list_of_formulae(axioms). %%%% Sortal Axioms % Sequence formula(forall([a1,a2], implies(and(Action(a1), Action(a2)), Action(Sequence(a1,a2)))),Sequence). % RUnion formula(forall([u,v], implies(and(Region(u), Region(v)), Region(RUnion(u,v)))),RUnion). % ConvexHull formula(forall([r], implies(Region(r), Region(ConvexHull(r)))),ConvexHull). % Singleton formula(forall([x], implies(Object(x), ObjectSet(Singleton(x)))),Singleton). % Pair formula(forall([x,y], implies(and(Object(x), Object(y)), ObjectSet(Pair(x,y)))),Pair). % Union formula(forall([sa,sb], implies(and(ObjectSet(sa), ObjectSet(sb)), ObjectSet(Union(sa,sb)))),Union). % Place formula(forall([t,o], implies(and(Time(t), Object(o)), Region(Place(t,o)))),Place). % Contents formula(forall([t,r], implies(and(Time(t), Region(r)), ObjectSet(Contents(t,r)))),Contents). % CContents formula(forall([t,s], implies(and(Time(t), ObjectSet(s)), ObjectSet(CContents(t,s)))),CContents). % UContents formula(forall([t,s], implies(and(Time(t), Object(s)), ObjectSet(UContents(t,s)))),UContents). % TravelTo formula(forall([r], implies(Region(r), Action(TravelTo(r)))),TravelTo). % StandStill formula(Action(StandStill),StandStill). % ManipTo formula(forall([o,r], implies(and(Object(o), Region(r)), Action(ManipTo(o,r)))),ManipTo). % Slice formula(forall([t,h], implies(and(Time(t), History(h)), Region(Slice(t,h)))),Slice). % HPlace formula(forall([o], implies(Object(o), History(HPlace(o)))),HPlace). % HUnion formula(forall([ha,hb], implies(and(History(ha), History(hb)), History(HUnion(ha,hb)))),HUnion). % MovingGroup formula(forall([t,ox], implies(and(Time(t), Object(ox)), ObjectSet(MovingGroup(t,ox)))),MovingGroup). % PutInUC formula(forall([ox,ob], implies(and(Object(ox), Object(ob)), Action(PutInUC(ox,ob)))),PutInUC). % LoadUprightContainer formula(forall([ox,ob], implies(and(Object(ox), Object(ob)), Action(LoadUprightContainer(ox,ob)))),LoadUprightContainer). %%% Time %% Time ordering % TOSA formula(forall([x,y,z], implies(Leq3(x,y,z), and(Time(x), Time(y), Time(z)))),TOSA). % TOSB formula(forall([x,y], implies(or(Lt(x,y), Leq(x,y)), and(Time(x), Time(y)))),TOSB). %% Actions % TASA formula(forall([ta,tb,a], implies(Occurs(ta,tb,a), and(Time(ta), Time(tb), Action(a)))),TASA). % TASB formula(forall([t,a], implies(Feasible(t,a), and(Time(t), Action(a)))),TASB). %%% Objects %% Object sets % OSSA formula(forall([x,s], implies(Element(x,s), and(Object(x), ObjectSet(s)))),OSSA). %% Objects and object sets: spatio-temporal % OOSA formula(forall([t,s,r], implies(OSPlace(t,s,r), and(Time(t), ObjectSet(s), Region(r)))),OOSA). % OOSB formula(forall([o,r], implies(FeasiblePlace(o,r), and(Object(o), Region(r)))),OOSB). %% Objects containing regions % ORSA formula(forall([t,o,r], implies(UprightContainer(t,o,r), and(Time(t), Object(o), Region(r)))),ORSA). %% Object containment % OCSA formula(forall([t,ox,ob], implies(or(CContained(t,ox,ob), UContained(t,ox,ob), BLContained(t,ox,ob)), and(Time(t), Object(ox), Object(ob)))),OCSA). %%% Specific Actions %% Safe manipulation % ASSA formula(forall([t,o], implies(SafelyMovable(t,o), and(Time(t), Object(o)))),ASSA). % ASSB formula(forall([t,ox,ob], implies(BoxedIn(t,ox,ob), and(Time(t), Object(ox), Object(ob)))),ASSB). % ASSC formula(forall([ta,tb,o,r], implies(SafeManipulate(ta,tb,o,r), and(Time(ta), Time(tb), Object(o), Region(r)))),ASSC). % ASSD formula(forall([ta,tb,o], implies(or(PreserveCContents(ta,tb,o), PreserveUContents(ta,tb,o), PreserveBoxWithLid(ta,tb,o)), and(Time(ta), Time(tb), Object(o)))),ASSD). %% Loading an upright container % ALSA formula(forall([ra,rb], implies(FullyOutside(ra,rb), and(Region(ra), Region(rb)))),ALSA). % ALSB formula(forall([t,r], implies(Reachable(t,r), and(Time(t), Region(r)))),ALSB). %% Fits and small set % OFSA formula(forall([o], implies(SmallObject(o), Object(o))),OFSA). % OFSB formula(forall([s,r], implies(or(Fits(s,r), SmallSet(s,r)), and(ObjectSet(s), Region(r)))),OFSB). % OFSC formula(forall([o,r], implies(OMuchSmaller(o,r), and(Object(o), Region(r)))),OFSC). %%% Spatial Relations %% Basic Spatial Relations % SRSA formula(forall([u,v], implies(or(P(u,v),O(u,v), OV(u,v)), and(Region(u), Region(v)))),SRSA). %% Spatial containment % SCSA/B formula(forall([ra,rb], implies(or(OpenContained(ra,rb), FullyOutside(ra,rb), OpenContainerShape(ra,rb), UprightContainerShape(ra,rb)), and(Region(ra), Region(rb)))),SCSA). % SCSC formula(forall([ra,rb], implies(or(Cavity(ra,rb), PartiallyContained(ra,rb)), and(Region(ra), Region(rb)))),SCSC). %% Much smaller % SMSA formula(forall([ra,rb], implies(MuchSmaller(ra,rb), and(Region(ra), Region(rb)))),SMSA). %%% Motion and Manipulation %% Motion % MMSA formula(forall([ta,tb,o], implies(Moves(ta,tb,o), and(Time(ta), Time(tb), Object(o)))),MMSA). %% Stability and falling % MSSA formula(forall([t], implies(AllStable(t), Time(t))),MMSA). % MSSB formula(forall([t,o], implies(Stable(t,o), and(Time(t), Object(o)))),MMSB). %% Frame axioms % MFSA formula(forall([t,o], implies(NoPartialContents(t,o), and(Time(t), Object(o)))),MFSA). % MFSB formula(forall([ta,tb,o], implies(or(StableThroughout(ta,tb,o), Released(ta,tb,o), Motionless(ta,tb,o)), and(Time(ta), Time(tb), Object(o)))),MFSB). %% Grasping an object % MGSA formula(forall([t], implies(EmptyHanded(t), Time(t))),MGSA). % MGSB formula(forall([t,o], implies(CanGrasp(t,o), and(Time(t), Object(o)))),MGSB). % MGSC formula(forall([t,o], implies(Grasp(t,o), and(Time(t), Object(o)))),MGSC). % MGSD formula(forall([ta,tb,o], implies(Grasps(ta,tb,o), and(Time(ta), Time(tb), Object(o)))),MGSD). %% Feasibility of Traveling % MFSA formula(forall([t,o], implies(Graspable(t,o), and(Time(t),Object(o)))),MFSA). %%% Histories %% Basic properties of histories % HBSA formula(forall([t1,t2,h], implies(Constant(t1,t2,h), and(Time(t1), Time(t2), History(h)))),HBSA). %% Dynamic upright containers % HDSA formula(forall([ta,tb,ob,hc], implies(DynamicUContainer(ta,tb,ob,hc), and(Time(ta), Time(tb), Object(ob), History(hc)))),HDSA). % Temporal Axioms % TID3 formula(forall([x,y,z], equiv(Leq3(x,y,z), and(Leq(x,y), Leq(y,z)))),TID3). % TID1 formula(forall([x,y], implies(and(Time(x), Time(y)), equiv(Leq(x,y), or(Lt(x,y), equal(x,y))))),TID1). % TIA2 formula(forall([x,y,z], implies(and(Lt(x,y), Lt(y,z)), Lt(x,z))),TIA2). %%%% Specifications % C4A1 % formula(UprightContainer(Ta4,Ob4,Rc4),C4A1). % C4A2 % formula(FullyOutside(Place(Ta4,Ox4), Place(Ta4, Ob4)),C4A2). % C4A3 % formula(SmallSet(Union(Contents(Ta4,Rc4), MovingGroup(Ta4,Ox4)), Rc4),C4A3). % C4A4 % formula(AllStable(Ta4),C4A4). % C4A5 % formula(EmptyHanded(Ta4),C4A5). % C4A6 % formula(Graspable(Ta4,Ox4),C4A6). % C4A7 % formula(Reachable(Ta4,Rc4),C4A7). % C4A8 % formula(and(not(equal(Ox4,Agent)), not(equal(Agent,Ob4)), not(equal(Ox4,Ob4))),C4A8). % C4A9 % formula(FullyOutside(Place(Ta4,Agent), Place(Ta4,Ob4)),C4A9). % C4A10 % formula(SafelyMovable(Ta4,Ox4),C4A10). % C4A11 % formula(SmallObject(Ob4),C4A11). % C4A12 % formula(not(BoxedIn(Ta4,Agent,Ox4)),C4A12). % C4A13 % formula(NoPartialContents(Ta4,Ob4),C4A13). % Ta4 formula(Time(Ta4),Ta4). % Tb formula(Time(Tb),Tb). % Ox4 formula(Object(Ox4),Ox4). % Ob4 formula(Object(Ob4),Ob4). % Ra4 formula(Region(Ra4),Ra4). % Agent formula(Object(Agent),Agent). % Rq formula(Region(Rq),Rq). % Rc1 formula(Region(Rc1),Rc1). % Rx1 formula(Region(Rx1),Rx1). % Ox formula(Object(Ox),Ox). % Tm1 formula(Time(Tm1),Tm1). % Tm2 formula(Time(Tm2),Tm2). % Rc2 formula(Region(Rc2),Rc2). % Hc1 formula(History(Hc1),Hc1). % Tc formula(Time(Tc),Tc). % StandStill formula(Action(StandStill),StandStill). % 4.47 test formula(forall([o], implies(Object(o), implies(and(not(equal(o,Agent)), not(Element(o,MovingGroup(Tm1,Ox4)))), equal(Place(Tm1,o),Place(Tm2,o))))),4dot47). % 4.39 test formula(forall([o], implies(and(Object(o), not(equal(o,Agent))), equal(Place(Tm1,o), Place(Ta4,o)))),4dot39). % 4.42 formula(equal(MovingGroup(Tm1,Ox4), MovingGroup(Ta4,Ox4)),4dot42). end_of_list. list_of_formulae(conjectures). % 4.62 (NO proof) formula(forall([o], implies(Object(o), implies(and(not(equal(o,Agent)), not(Element(o,MovingGroup(Ta4,Ox4)))), equal(Place(Tm2,o),Place(Ta4,o)))))). end_of_list. list_of_settings(SPASS). {*set_flag(DocProof,1).*} end_of_list. end_problem.