begin_problem(Scenario1_Piece3).

list_of_descriptions.
name({*Qualitative Reasoning About Containers - Case 1, Piece 3*}).
author({*Professor Ernest Davis, Angelica Chen, Casey McGinley*}).
status(unsatisfiable).
description({*November 25, 2014*}).
end_of_list.

list_of_symbols.
functions[(RUnion,2), (Singleton,1), (Place,2), (Slice,2), (HPlace,1), (Ox1,0), (Ob1,0), (Ta1,0), (Tb1,0), (Rc1,0), (Hc1,0)].
predicates[(Ordered,2), (Time,1), (Region,1), (History,1), (Object,1), (ObjectSet,1), (Lt,2), (Leq,2), (Leq3,3), (P,2), (Cavity,2), (OSPlace,3), (ClosedContainer,3), (CContained,3), (RigidObject,1), (RigidHistory,1), (O,2), (EC,2), (DR,2), (Outside,2), (NoExitCavity,4), (PersistentCavity,4), (NoEntranceCavity,4), (Continuous,3), (WeaklyContinuous,3), (Constant,3), (AlwaysIntConn,3), (IntConn,1)].
end_of_list.

list_of_formulae(axioms).
% Time Ordering
% Sortal axioms
% TISA
formula(forall([x,y], implies(Lt(x,y), and(Time(x), Time(y))))).
% TISB
formula(forall([x,y], implies(Leq(x,y), and(Time(x), Time(y))))).
% TISC
formula(forall([x,y], implies(Ordered(x,y), and(Time(x), Time(y))))).
% TISD
formula(forall([x,y,z], implies(Leq3(x,y,z), and(Time(x), Time(y), Time(z))))).

% Space
% Basic spatial relations
% Sortal axioms
% SBSA
formula(forall([u,v], implies(or(P(u,v), O(u,v), EC(u,v), DR(u,v)), and(Region(u), Region(v))))).
% SBSB
formula(forall([u,v], implies(and(Region(u), Region(v)), Region(RUnion(u,v))))).

% Spatial Containment
% Sortal axioms
% SCSA
formula(forall([u,v], implies(or(Cavity(u,v), Outside(u,v)), and(Region(u), Region(v))))).
% SCSB
formula(forall([r], implies(IntConn(r), Region(r)))).

% Objects
% Object Sets
% Sortal axioms
% OSSA
formula(forall([x], implies(Object(x), ObjectSet(Singleton(x))))).

% Objects and Object Sets: Spatio-Temporal
% Sortal axioms
% OTSA
formula(forall([t,o], implies(and(Time(t), Object(o)), Region(Place(t,o))))).
% OTSB
formula(forall([t,s,r], implies(OSPlace(t,s,r), and(Time(t), ObjectSet(s), Region(r))))).

% Objects containing regions
% Sortal axiom
% ORSA
formula(forall([t,s,r], implies(ClosedContainer(t,s,r), and(Time(t), ObjectSet(s), Region(r))))).

% Object Containment
% Sortal axiom
% OCSA
formula(forall([t,ox,s], implies(CContained(t,ox,s), and(Time(t), Object(ox), ObjectSet(s))))).

% Histories
% Sortal axioms
% HISA
formula(forall([t,h], implies(and(Time(t), History(h)), Region(Slice(t,h))))).
% HISB
formula(forall([ta,tb,h], implies(or(Continuous(ta,tb,h), WeaklyContinuous(ta,tb,h)), and(Time(ta), Time(tb), History(h))))).
% HISC
formula(forall([o], implies(Object(o), History(HPlace(o))))).
% HISD
formula(forall([t1,t2,h], implies(Constant(t1,t2,h), and(Time(t1), Time(t2), History(h))))).
% HISE
formula(forall([t1,t2,h], implies(AlwaysIntConn(t1,t2,h), and(Time(t1), Time(t2), History(h))))).

% Evolving cavities
% Sortal axioms
% HCSA
formula(forall([t1,t2,hc,ho], implies(or(NoExitCavity(t1,t2,hc,ho), NoEntranceCavity(t1,t2,hc,ho), PersistentCavity(t1,t2,hc,ho)), and(Time(t1), Time(t2), History(hc), History(ho))))).

% Rigid Objects
% Sortal axioms
% RGSA
formula(forall([o], implies(RigidObject(o), Object(o)))).
% RGSB
formula(forall([h], implies(RigidHistory(h), History(h)))).

% P.3.1 - proved by Part2
formula(NoExitCavity(Ta1,Tb1,Hc1,HPlace(Ob1))).
% P.3.2 - proved by Part1
formula(P(Place(Ta1,Ox1),Rc1)).
% P.3.3 - proved by Part2
formula(equal(Rc1, Slice(Ta1,Hc1))).
% C1A3 - given
formula(Lt(Ta1,Tb1)).
% C1A4 - given
formula(not(equal(Ox1, Ob1))).
% HIA1
formula(forall([ta,tb,o], implies(and(Object(o), Lt(ta,tb)), Continuous(ta,tb,HPlace(o))))).
% HIA2
formula(forall([t,o], implies(and(Time(t), Object(o)), equal(Place(t,o), Slice(t,HPlace(o)))))).
% OTA2
formula(forall([p,q,t], implies(and(Object(p), Object(q), Time(t), not(equal(p,q))), DR(Place(t,p), Place(t,q))))).
% SBD3
formula(forall([u,v], equiv(DR(u,v), and(Region(u), Region(v), not(O(u,v)))))).
% SCD1
formula(forall([u,v], equiv(Cavity(u,v), and(IntConn(u), DR(u,v), forall([r], implies(and(IntConn(r), O(r,u), DR(r,v)), P(r,u))))))).
% HID4
formula(forall([t1,t2,h], equiv(AlwaysIntConn(t1,t2,h), and(History(h), Lt(t1,t2), forall([t], implies(Leq3(t1,t,t2), IntConn(Slice(t,h)))))))).
% HCA2
formula(forall([t1,t2,hc,hb,hs], implies(and(NoExitCavity(t1,t2,hc,hb), Continuous(t1,t2,hs), AlwaysIntConn(t1,t2,hs), P(Slice(t1,hs),Slice(t1,hc)), not(P(Slice(t2,hs),Slice(t2,hc)))), exists([tm], and(Lt(t1,tm), Lt(tm,t2), O(Slice(tm,hs),Slice(tm,hb))))))).
end_of_list.

list_of_formulae(conjectures).
formula(P(Slice(Tb1,HPlace(Ox1)), Slice(Tb1,Hc1))).
end_of_list.

list_of_settings(SPASS).
{*set_flag(DocProof,1).*}
end_of_list.

end_problem.