--------------------------SPASS-START-----------------------------
Input Problem:
1[0:Inp] ||  -> Object(Ob1)*.
2[0:Inp] ||  -> Object(Ox1)*.
3[0:Inp] ||  -> Time(Ta1)*.
4[0:Inp] ||  -> Time(Tb1)*.
5[0:Inp] ||  -> History(Hc1)*.
6[0:Inp] ||  -> Region(Rc1)*.
7[0:Inp] ||  -> Lt(Ta1,Tb1)*.
8[0:Inp] || equal(Ob1,Ox1)** -> .
9[0:Inp] || RigidObject(U) -> Object(U)*.
10[0:Inp] || RigidHistory(U) -> History(U)*.
11[0:Inp] ||  -> P(Place(Ta1,Ox1),Rc1)*.
12[0:Inp] ||  -> equal(Slice(Ta1,Hc1),Rc1)**.
13[0:Inp] || Lt(U,V)* -> Time(U).
14[0:Inp] || Lt(U,V)* -> Time(V).
15[0:Inp] || Leq(U,V)* -> Time(U).
16[0:Inp] || Leq(U,V)* -> Time(V).
17[0:Inp] || Ordered(U,V)* -> Time(U).
18[0:Inp] || Ordered(U,V)* -> Time(V).
19[0:Inp] || SkP0(U,V)* -> Region(V).
20[0:Inp] || SkP0(U,V)* -> Region(U).
21[0:Inp] || SkP1(U,V)* -> Region(V).
22[0:Inp] || SkP1(U,V)* -> Region(U).
23[0:Inp] || Object(U) -> ObjectSet(Singleton(U))*.
24[0:Inp] || Object(U) -> History(HPlace(U))*.
25[0:Inp] ||  -> NoExitCavity(Ta1,Tb1,Hc1,HPlace(Ob1))*.
26[0:Inp] || DR(U,V)* -> Region(U).
27[0:Inp] || DR(U,V)* -> Region(V).
28[0:Inp] || Leq3(U,V,W)* -> Time(U).
29[0:Inp] || Leq3(U,V,W)* -> Time(V).
30[0:Inp] || Leq3(U,V,W)* -> Time(W).
31[0:Inp] || P(U,V) -> SkP0(V,U)*.
32[0:Inp] || O(U,V) -> SkP0(V,U)*.
33[0:Inp] || EC(U,V) -> SkP0(V,U)*.
34[0:Inp] || DR(U,V) -> SkP0(V,U)*.
35[0:Inp] || Cavity(U,V) -> SkP1(V,U)*.
36[0:Inp] || Outside(U,V) -> SkP1(V,U)*.
37[0:Inp] || OSPlace(U,V,W)* -> Time(U).
38[0:Inp] || OSPlace(U,V,W)* -> ObjectSet(V).
39[0:Inp] || OSPlace(U,V,W)* -> Region(W).
40[0:Inp] || ClosedContainer(U,V,W)* -> Time(U).
41[0:Inp] || ClosedContainer(U,V,W)* -> ObjectSet(V).
42[0:Inp] || ClosedContainer(U,V,W)* -> Region(W).
43[0:Inp] || CContained(U,V,W)* -> Time(U).
44[0:Inp] || CContained(U,V,W)* -> Object(V).
45[0:Inp] || CContained(U,V,W)* -> ObjectSet(W).
46[0:Inp] || SkP2(U,V,W)* -> Time(W).
47[0:Inp] || SkP2(U,V,W)* -> Time(V).
48[0:Inp] || SkP2(U,V,W)* -> History(U).
49[0:Inp] || Constant(U,V,W)* -> Time(U).
50[0:Inp] || Constant(U,V,W)* -> Time(V).
51[0:Inp] || Constant(U,V,W)* -> History(W).
52[0:Inp] || SkP3(U,V,W,X)* -> Time(X).
53[0:Inp] || SkP3(U,V,W,X)* -> Time(W).
54[0:Inp] || SkP3(U,V,W,X)* -> History(V).
55[0:Inp] || SkP3(U,V,W,X)* -> History(U).
56[0:Inp] || O(U,V) DR(U,V)* -> .
57[0:Inp] || P(Slice(Tb1,HPlace(Ox1)),Slice(Tb1,Hc1))* -> .
58[0:Inp] || Continuous(U,V,W) -> SkP2(W,V,U)*.
59[0:Inp] || WeaklyContinuous(U,V,W) -> SkP2(W,V,U)*.
60[0:Inp] || Region(U) Region(V) -> Region(RUnion(U,V))*.
61[0:Inp] || Time(U) Object(V) -> Region(Place(U,V))*.
62[0:Inp] || Time(U) History(V) -> Region(Slice(U,V))*.
63[0:Inp] || NoExitCavity(U,V,W,X) -> SkP3(X,W,V,U)*.
64[0:Inp] || NoEntranceCavity(U,V,W,X) -> SkP3(X,W,V,U)*.
65[0:Inp] || PersistentCavity(U,V,W,X) -> SkP3(X,W,V,U)*.
66[0:Inp] || Lt(U,V) Object(W) -> Continuous(U,V,HPlace(W))*.
67[0:Inp] || Region(U) Region(V) -> O(V,U) DR(V,U)*.
68[0:Inp] || Time(U) Object(V) -> equal(Slice(U,HPlace(V)),Place(U,V))**.
69[0:Inp] || Object(U) Object(V) Time(W) -> equal(U,V) DR(Place(W,U),Place(W,V))*.
70[0:Inp] || NoExitCavity(U,V,W,X)* P(Slice(U,Y),Slice(U,W))* Continuous(U,V,Y)* -> Lt(skf1(U,V,Z,X1),V)* P(Slice(V,Y),Slice(V,W))*.
71[0:Inp] || NoExitCavity(U,V,W,X)* P(Slice(U,Y),Slice(U,W))* Continuous(U,V,Y)* -> Lt(U,skf1(U,Z,X1,X2))* P(Slice(V,Y),Slice(V,W))*.
72[0:Inp] || NoExitCavity(U,V,W,X)* P(Slice(U,Y),Slice(U,W))* Continuous(U,V,Y) -> O(Slice(skf1(U,V,X,Y),Y),Slice(skf1(U,V,X,Y),X))* P(Slice(V,Y),Slice(V,W))*.
 This is a first-order Non-Horn problem containing equality.
 This is a problem that has, if any, a non-trivial domain model.
 This is a problem that contains sort information.
 All equations are many sorted.
 The conjecture is ground.
 Axiom clauses: 71 Conjecture clauses: 1
 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=2 RCon=1 
 Extras    : Input Saturation, Dynamic Selection, Full Splitting, Full Reduction,  Ratio: 5, FuncWeight: 1, VarWeight: 1
 Precedence: skf1 > skf0 > Slice > Place > RUnion > HPlace > Singleton > SkP0 > DR > O > Region > Time > Ordered > History > SkP2 > Continuous > P > Lt > ObjectSet > Object > Leq > Leq3 > SkP1 > Cavity > OSPlace > ClosedContainer > CContained > RigidObject > RigidHistory > EC > Outside > SkP3 > NoExitCavity > PersistentCavity > NoEntranceCavity > WeaklyContinuous > Constant > skc3 > skc2 > skc1 > skc0 > Hc1 > Rc1 > Tb1 > Ta1 > Ob1 > Ox1
 Ordering  : KBO
Processed Problem:

Worked Off Clauses:

Usable Clauses:
5[0:Inp] ||  -> History(Hc1)*.
2[0:Inp] ||  -> Object(Ox1)*.
1[0:Inp] ||  -> Object(Ob1)*.
6[0:Inp] ||  -> Region(Rc1)*.
4[0:Inp] ||  -> Time(Tb1)*.
3[0:Inp] ||  -> Time(Ta1)*.
7[0:Inp] ||  -> Lt(Ta1,Tb1)*.
8[0:Inp] || equal(Ob1,Ox1)** -> .
12[0:Inp] ||  -> equal(Slice(Ta1,Hc1),Rc1)**.
11[0:Inp] ||  -> P(Place(Ta1,Ox1),Rc1)*.
10[0:Inp] RigidHistory(U) ||  -> History(U)*.
9[0:Inp] RigidObject(U) ||  -> Object(U)*.
25[0:Inp] ||  -> NoExitCavity(Ta1,Tb1,Hc1,HPlace(Ob1))*.
23[0:Inp] Object(U) ||  -> ObjectSet(Singleton(U))*.
24[0:Inp] Object(U) ||  -> History(HPlace(U))*.
22[0:Inp] || SkP1(U,V)* -> Region(U).
21[0:Inp] || SkP1(U,V)* -> Region(V).
27[0:Inp] || DR(U,V)* -> Region(V).
26[0:Inp] || DR(U,V)* -> Region(U).
20[0:Inp] || SkP0(U,V)* -> Region(U).
19[0:Inp] || SkP0(U,V)* -> Region(V).
18[0:Inp] || Ordered(U,V)* -> Time(V).
17[0:Inp] || Ordered(U,V)* -> Time(U).
16[0:Inp] || Leq(U,V)* -> Time(V).
15[0:Inp] || Leq(U,V)* -> Time(U).
14[0:Inp] || Lt(U,V)* -> Time(V).
13[0:Inp] || Lt(U,V)* -> Time(U).
36[0:Inp] || Outside(U,V) -> SkP1(V,U)*.
35[0:Inp] || Cavity(U,V) -> SkP1(V,U)*.
33[0:Inp] || EC(U,V) -> SkP0(V,U)*.
32[0:Inp] || O(U,V) -> SkP0(V,U)*.
34[0:Inp] || DR(U,V) -> SkP0(V,U)*.
31[0:Inp] || P(U,V) -> SkP0(V,U)*.
45[0:Inp] || CContained(U,V,W)* -> ObjectSet(W).
41[0:Inp] || ClosedContainer(U,V,W)* -> ObjectSet(V).
38[0:Inp] || OSPlace(U,V,W)* -> ObjectSet(V).
51[0:Inp] || Constant(U,V,W)* -> History(W).
48[0:Inp] || SkP2(U,V,W)* -> History(U).
44[0:Inp] || CContained(U,V,W)* -> Object(V).
42[0:Inp] || ClosedContainer(U,V,W)* -> Region(W).
39[0:Inp] || OSPlace(U,V,W)* -> Region(W).
50[0:Inp] || Constant(U,V,W)* -> Time(V).
49[0:Inp] || Constant(U,V,W)* -> Time(U).
43[0:Inp] || CContained(U,V,W)* -> Time(U).
40[0:Inp] || ClosedContainer(U,V,W)* -> Time(U).
37[0:Inp] || OSPlace(U,V,W)* -> Time(U).
30[0:Inp] || Leq3(U,V,W)* -> Time(W).
29[0:Inp] || Leq3(U,V,W)* -> Time(V).
28[0:Inp] || Leq3(U,V,W)* -> Time(U).
47[0:Inp] || SkP2(U,V,W)* -> Time(V).
46[0:Inp] || SkP2(U,V,W)* -> Time(W).
56[0:Inp] || DR(U,V)* O(U,V) -> .
55[0:Inp] || SkP3(U,V,W,X)* -> History(U).
54[0:Inp] || SkP3(U,V,W,X)* -> History(V).
53[0:Inp] || SkP3(U,V,W,X)* -> Time(W).
52[0:Inp] || SkP3(U,V,W,X)* -> Time(X).
57[0:Inp] || P(Slice(Tb1,HPlace(Ox1)),Slice(Tb1,Hc1))* -> .
59[0:Inp] || WeaklyContinuous(U,V,W) -> SkP2(W,V,U)*.
58[0:Inp] || Continuous(U,V,W) -> SkP2(W,V,U)*.
60[0:Inp] Region(U) Region(V) ||  -> Region(RUnion(V,U))*.
62[0:Inp] History(U) Time(V) ||  -> Region(Slice(V,U))*.
61[0:Inp] Object(U) Time(V) ||  -> Region(Place(V,U))*.
65[0:Inp] || PersistentCavity(U,V,W,X) -> SkP3(X,W,V,U)*.
64[0:Inp] || NoEntranceCavity(U,V,W,X) -> SkP3(X,W,V,U)*.
63[0:Inp] || NoExitCavity(U,V,W,X) -> SkP3(X,W,V,U)*.
67[0:Inp] Region(U) Region(V) ||  -> DR(U,V)* O(U,V).
66[0:Inp] Object(U) || Lt(V,W) -> Continuous(V,W,HPlace(U))*.
68[0:Inp] Object(U) Time(V) ||  -> equal(Slice(V,HPlace(U)),Place(V,U))**.
69[0:Inp] Time(U) Object(V) Object(W) ||  -> equal(W,V) DR(Place(U,W),Place(U,V))*.
75[0:Res:70.4,57.0] || P(Slice(U,HPlace(Ox1)),Slice(U,Hc1))* Continuous(U,Tb1,HPlace(Ox1)) NoExitCavity(U,Tb1,Hc1,V)* -> Lt(skf1(U,Tb1,W,X),Tb1)*.
74[0:Res:71.4,57.0] || P(Slice(U,HPlace(Ox1)),Slice(U,Hc1))* Continuous(U,Tb1,HPlace(Ox1)) NoExitCavity(U,Tb1,Hc1,V)* -> Lt(U,skf1(U,W,X,Y))*.
70[0:Inp] || P(Slice(U,V),Slice(U,W))* Continuous(U,X,V)* NoExitCavity(U,X,W,Y)* -> P(Slice(X,V),Slice(X,W))* Lt(skf1(U,X,Z,X1),X)*.
71[0:Inp] || P(Slice(U,V),Slice(U,W))* Continuous(U,X,V)* NoExitCavity(U,X,W,Y)* -> Lt(U,skf1(U,Z,X1,X2))* P(Slice(X,V),Slice(X,W))*.
72[0:Inp] || P(Slice(U,V),Slice(U,W))* Continuous(U,X,V) NoExitCavity(U,X,W,Y)* -> P(Slice(X,V),Slice(X,W))* O(Slice(skf1(U,X,Y,V),V),Slice(skf1(U,X,Y,V),Y))*.
	Given clause: 5[0:Inp] ||  -> History(Hc1)*.
	Given clause: 2[0:Inp] ||  -> Object(Ox1)*.
	Given clause: 1[0:Inp] ||  -> Object(Ob1)*.
	Given clause: 6[0:Inp] ||  -> Region(Rc1)*.
	Given clause: 4[0:Inp] ||  -> Time(Tb1)*.
	Given clause: 3[0:Inp] ||  -> Time(Ta1)*.
	Given clause: 7[0:Inp] ||  -> Lt(Ta1,Tb1)*.
	Given clause: 8[0:Inp] || equal(Ob1,Ox1)** -> .
	Given clause: 12[0:Inp] ||  -> equal(Slice(Ta1,Hc1),Rc1)**.
	Given clause: 11[0:Inp] ||  -> P(Place(Ta1,Ox1),Rc1)*.
	Given clause: 10[0:Inp] RigidHistory(U) ||  -> History(U)*.
	Given clause: 9[0:Inp] RigidObject(U) ||  -> Object(U)*.
	Given clause: 25[0:Inp] ||  -> NoExitCavity(Ta1,Tb1,Hc1,HPlace(Ob1))*.
	Given clause: 23[0:Inp] Object(U) ||  -> ObjectSet(Singleton(U))*.
	Given clause: 24[0:Inp] Object(U) ||  -> History(HPlace(U))*.
	Given clause: 22[0:Inp] || SkP1(U,V)* -> Region(U).
	Given clause: 21[0:Inp] || SkP1(U,V)* -> Region(V).
	Given clause: 27[0:Inp] || DR(U,V)* -> Region(V).
	Given clause: 26[0:Inp] || DR(U,V)* -> Region(U).
	Given clause: 20[0:Inp] || SkP0(U,V)* -> Region(U).
	Given clause: 19[0:Inp] || SkP0(U,V)* -> Region(V).
	Given clause: 18[0:Inp] || Ordered(U,V)* -> Time(V).
	Given clause: 17[0:Inp] || Ordered(U,V)* -> Time(U).
	Given clause: 16[0:Inp] || Leq(U,V)* -> Time(V).
	Given clause: 15[0:Inp] || Leq(U,V)* -> Time(U).
	Given clause: 14[0:Inp] || Lt(U,V)* -> Time(V).
	Given clause: 13[0:Inp] || Lt(U,V)* -> Time(U).
	Given clause: 36[0:Inp] || Outside(U,V) -> SkP1(V,U)*.
	Given clause: 126[0:Res:36.1,21.0] || Outside(U,V)* -> Region(U).
	Given clause: 35[0:Inp] || Cavity(U,V) -> SkP1(V,U)*.
	Given clause: 127[0:Res:36.1,22.0] || Outside(U,V)* -> Region(V).
	Given clause: 128[0:Res:35.1,21.0] || Cavity(U,V)* -> Region(U).
	Given clause: 129[0:Res:35.1,22.0] || Cavity(U,V)* -> Region(V).
	Given clause: 33[0:Inp] || EC(U,V) -> SkP0(V,U)*.
	Given clause: 32[0:Inp] || O(U,V) -> SkP0(V,U)*.
	Given clause: 130[0:Res:33.1,19.0] || EC(U,V)* -> Region(U).
	Given clause: 131[0:Res:33.1,20.0] || EC(U,V)* -> Region(V).
	Given clause: 132[0:Res:32.1,19.0] || O(U,V)* -> Region(U).
	Given clause: 133[0:Res:32.1,20.0] || O(U,V)* -> Region(V).
	Given clause: 34[0:Inp] || DR(U,V) -> SkP0(V,U)*.
	Given clause: 31[0:Inp] || P(U,V) -> SkP0(V,U)*.
	Given clause: 136[0:Res:31.1,19.0] || P(U,V)* -> Region(U).
	Given clause: 138[0:Res:11.0,136.0] ||  -> Region(Place(Ta1,Ox1))*.
	Given clause: 137[0:Res:31.1,20.0] || P(U,V)* -> Region(V).
	Given clause: 45[0:Inp] || CContained(U,V,W)* -> ObjectSet(W).
	Given clause: 41[0:Inp] || ClosedContainer(U,V,W)* -> ObjectSet(V).
	Given clause: 38[0:Inp] || OSPlace(U,V,W)* -> ObjectSet(V).
	Given clause: 51[0:Inp] || Constant(U,V,W)* -> History(W).
	Given clause: 48[0:Inp] || SkP2(U,V,W)* -> History(U).
	Given clause: 44[0:Inp] || CContained(U,V,W)* -> Object(V).
	Given clause: 42[0:Inp] || ClosedContainer(U,V,W)* -> Region(W).
	Given clause: 39[0:Inp] || OSPlace(U,V,W)* -> Region(W).
	Given clause: 50[0:Inp] || Constant(U,V,W)* -> Time(V).
	Given clause: 49[0:Inp] || Constant(U,V,W)* -> Time(U).
	Given clause: 43[0:Inp] || CContained(U,V,W)* -> Time(U).
	Given clause: 40[0:Inp] || ClosedContainer(U,V,W)* -> Time(U).
	Given clause: 37[0:Inp] || OSPlace(U,V,W)* -> Time(U).
	Given clause: 30[0:Inp] || Leq3(U,V,W)* -> Time(W).
	Given clause: 29[0:Inp] || Leq3(U,V,W)* -> Time(V).
	Given clause: 28[0:Inp] || Leq3(U,V,W)* -> Time(U).
	Given clause: 47[0:Inp] || SkP2(U,V,W)* -> Time(V).
	Given clause: 46[0:Inp] || SkP2(U,V,W)* -> Time(W).
	Given clause: 56[0:Inp] || DR(U,V)* O(U,V) -> .
	Given clause: 55[0:Inp] || SkP3(U,V,W,X)* -> History(U).
	Given clause: 54[0:Inp] || SkP3(U,V,W,X)* -> History(V).
	Given clause: 53[0:Inp] || SkP3(U,V,W,X)* -> Time(W).
	Given clause: 52[0:Inp] || SkP3(U,V,W,X)* -> Time(X).
	Given clause: 57[0:Inp] || P(Slice(Tb1,HPlace(Ox1)),Slice(Tb1,Hc1))* -> .
	Given clause: 59[0:Inp] || WeaklyContinuous(U,V,W) -> SkP2(W,V,U)*.
	Given clause: 58[0:Inp] || Continuous(U,V,W) -> SkP2(W,V,U)*.
	Given clause: 140[0:Res:59.1,46.0] || WeaklyContinuous(U,V,W)* -> Time(U).
	Given clause: 141[0:Res:59.1,47.0] || WeaklyContinuous(U,V,W)* -> Time(V).
	Given clause: 142[0:Res:59.1,48.0] || WeaklyContinuous(U,V,W)* -> History(W).
	Given clause: 143[0:Res:58.1,46.0] || Continuous(U,V,W)* -> Time(U).
	Given clause: 60[0:Inp] Region(U) Region(V) ||  -> Region(RUnion(V,U))*.
	Given clause: 144[0:Res:58.1,47.0] || Continuous(U,V,W)* -> Time(V).
	Given clause: 145[0:Res:58.1,48.0] || Continuous(U,V,W)* -> History(W).
	Given clause: 62[0:Inp] History(U) Time(V) ||  -> Region(Slice(V,U))*.
	Given clause: 61[0:Inp] Object(U) Time(V) ||  -> Region(Place(V,U))*.
	Given clause: 65[0:Inp] || PersistentCavity(U,V,W,X) -> SkP3(X,W,V,U)*.
	Given clause: 147[0:Res:65.1,52.0] || PersistentCavity(U,V,W,X)* -> Time(U).
	Given clause: 148[0:Res:65.1,53.0] || PersistentCavity(U,V,W,X)* -> Time(V).
	Given clause: 149[0:Res:65.1,54.0] || PersistentCavity(U,V,W,X)* -> History(W).
	Given clause: 150[0:Res:65.1,55.0] || PersistentCavity(U,V,W,X)* -> History(X).
	Given clause: 64[0:Inp] || NoEntranceCavity(U,V,W,X) -> SkP3(X,W,V,U)*.
	Given clause: 151[0:Res:64.1,52.0] || NoEntranceCavity(U,V,W,X)* -> Time(U).
	Given clause: 152[0:Res:64.1,53.0] || NoEntranceCavity(U,V,W,X)* -> Time(V).
	Given clause: 153[0:Res:64.1,54.0] || NoEntranceCavity(U,V,W,X)* -> History(W).
	Given clause: 154[0:Res:64.1,55.0] || NoEntranceCavity(U,V,W,X)* -> History(X).
	Given clause: 63[0:Inp] || NoExitCavity(U,V,W,X) -> SkP3(X,W,V,U)*.
	Given clause: 155[0:Res:63.1,52.0] || NoExitCavity(U,V,W,X)* -> Time(U).
	Given clause: 156[0:Res:63.1,53.0] || NoExitCavity(U,V,W,X)* -> Time(V).
	Given clause: 157[0:Res:63.1,54.0] || NoExitCavity(U,V,W,X)* -> History(W).
	Given clause: 158[0:Res:63.1,55.0] || NoExitCavity(U,V,W,X)* -> History(X).
	Given clause: 67[0:Inp] Region(U) Region(V) ||  -> DR(U,V)* O(U,V).
	Given clause: 162[0:Res:25.0,158.0] ||  -> History(HPlace(Ob1))*.
	Given clause: 66[0:Inp] Object(U) || Lt(V,W) -> Continuous(V,W,HPlace(U))*.
	Given clause: 68[0:Inp] Object(U) Time(V) ||  -> equal(Slice(V,HPlace(U)),Place(V,U))**.
	Given clause: 172[0:SSi:171.1,171.0,4.0,2.0] || P(Place(Tb1,Ox1),Slice(Tb1,Hc1))* -> .
	Given clause: 69[0:Inp] Time(U) Object(V) Object(W) ||  -> equal(W,V) DR(Place(U,W),Place(U,V))*.
	Given clause: 174[0:Res:69.4,56.0] Time(U) Object(V) Object(W) || O(Place(U,W),Place(U,V))* -> equal(W,V).
	Given clause: 75[0:Res:70.4,57.0] || P(Slice(U,HPlace(Ox1)),Slice(U,Hc1))*+ Continuous(U,Tb1,HPlace(Ox1)) NoExitCavity(U,Tb1,Hc1,V)* -> Lt(skf1(U,Tb1,W,X),Tb1)*.
	Given clause: 177[0:SpL:12.0,75.0] || P(Slice(Ta1,HPlace(Ox1)),Rc1)+ Continuous(Ta1,Tb1,HPlace(Ox1)) NoExitCavity(Ta1,Tb1,Hc1,U)* -> Lt(skf1(Ta1,Tb1,V,W),Tb1)*.
	Given clause: 183[0:MRR:182.0,11.0] || Continuous(Ta1,Tb1,HPlace(Ox1))+ NoExitCavity(Ta1,Tb1,Hc1,U)* -> Lt(skf1(Ta1,Tb1,V,W),Tb1)*.
	Given clause: 70[0:Inp] || P(Slice(U,V),Slice(U,W))*+ Continuous(U,X,V)* NoExitCavity(U,X,W,Y)* -> P(Slice(X,V),Slice(X,W))* Lt(skf1(U,X,Z,X1),X)*.
	Given clause: 186[0:MRR:185.0,7.0] || NoExitCavity(Ta1,Tb1,Hc1,U)*+ -> Lt(skf1(Ta1,Tb1,V,W),Tb1)*.
	Given clause: 193[0:Res:25.0,186.0] ||  -> Lt(skf1(Ta1,Tb1,U,V),Tb1)*.
	Given clause: 194[0:Res:193.0,13.0] ||  -> Time(skf1(Ta1,Tb1,U,V))*.
	Given clause: 180[0:MRR:179.0,155.1] || P(Place(U,Ox1),Slice(U,Hc1))*+ Continuous(U,Tb1,HPlace(Ox1)) NoExitCavity(U,Tb1,Hc1,V)* -> Lt(skf1(U,Tb1,W,X),Tb1)*.
	Given clause: 71[0:Inp] || P(Slice(U,V),Slice(U,W))*+ Continuous(U,X,V)* NoExitCavity(U,X,W,Y)* -> Lt(U,skf1(U,Z,X1,X2))* P(Slice(X,V),Slice(X,W))*.
	Given clause: 74[0:Res:71.4,57.0] || P(Slice(U,HPlace(Ox1)),Slice(U,Hc1))*+ Continuous(U,Tb1,HPlace(Ox1)) NoExitCavity(U,Tb1,Hc1,V)* -> Lt(U,skf1(U,W,X,Y))*.
	Given clause: 203[0:SpL:12.0,74.0] || P(Slice(Ta1,HPlace(Ox1)),Rc1)+ Continuous(Ta1,Tb1,HPlace(Ox1)) NoExitCavity(Ta1,Tb1,Hc1,U)* -> Lt(Ta1,skf1(Ta1,V,W,X))*.
	Given clause: 209[0:MRR:208.0,11.0] || Continuous(Ta1,Tb1,HPlace(Ox1))+ NoExitCavity(Ta1,Tb1,Hc1,U)* -> Lt(Ta1,skf1(Ta1,V,W,X))*.
	Given clause: 212[0:MRR:211.0,7.0] || NoExitCavity(Ta1,Tb1,Hc1,U)*+ -> Lt(Ta1,skf1(Ta1,V,W,X))*.
	Given clause: 72[0:Inp] || P(Slice(U,V),Slice(U,W))*+ Continuous(U,X,V) NoExitCavity(U,X,W,Y)* -> P(Slice(X,V),Slice(X,W))* O(Slice(skf1(U,X,Y,V),V),Slice(skf1(U,X,Y,V),Y))*.
	Given clause: 213[0:Res:25.0,212.0] ||  -> Lt(Ta1,skf1(Ta1,U,V,W))*.
	Given clause: 221[0:Res:213.0,14.0] ||  -> Time(skf1(Ta1,U,V,W))*.
	Given clause: 206[0:MRR:205.0,155.1] || P(Place(U,Ox1),Slice(U,Hc1))*+ Continuous(U,Tb1,HPlace(Ox1)) NoExitCavity(U,Tb1,Hc1,V)* -> Lt(U,skf1(U,W,X,Y))*.
	Given clause: 189[0:SpL:12.0,70.0] || P(Rc1,Slice(Ta1,U))+ Continuous(Ta1,V,Hc1) NoExitCavity(Ta1,V,U,W)* -> P(Slice(V,Hc1),Slice(V,U))* Lt(skf1(Ta1,V,X,Y),V)*.
	Given clause: 187[0:SpL:12.0,70.0] || P(Slice(Ta1,U),Rc1)+ Continuous(Ta1,V,U) NoExitCavity(Ta1,V,Hc1,W)* -> P(Slice(V,U),Slice(V,Hc1))* Lt(skf1(Ta1,V,X,Y),V)*.
	Given clause: 223[0:SpL:12.0,189.0] || P(Rc1,Rc1) Continuous(Ta1,U,Hc1) NoExitCavity(Ta1,U,Hc1,V)*+ -> P(Slice(U,Hc1),Slice(U,Hc1))* Lt(skf1(Ta1,U,W,X),U)*.
	Given clause: 225[0:SSi:224.1,3.0] Object(U) || P(Rc1,Place(Ta1,U)) Continuous(Ta1,V,Hc1) NoExitCavity(Ta1,V,HPlace(U),W)*+ -> P(Slice(V,Hc1),Slice(V,HPlace(U)))* Lt(skf1(Ta1,V,X,Y),V)*.
	Given clause: 228[0:SSi:227.1,3.0] Object(U) || P(Place(Ta1,U),Rc1)+ Continuous(Ta1,V,HPlace(U)) NoExitCavity(Ta1,V,Hc1,W)* -> P(Slice(V,HPlace(U)),Slice(V,Hc1))* Lt(skf1(Ta1,V,X,Y),V)*.
	Given clause: 231[0:SSi:230.0,2.0] || Continuous(Ta1,U,HPlace(Ox1))+ NoExitCavity(Ta1,U,Hc1,V)* -> P(Slice(U,HPlace(Ox1)),Slice(U,Hc1))* Lt(skf1(Ta1,U,W,X),U)*.
	Given clause: 191[0:MRR:190.1,155.1] Object(U) || P(Place(V,U),Slice(V,W))*+ Continuous(V,X,HPlace(U))* NoExitCavity(V,X,W,Y)* -> P(Slice(X,HPlace(U)),Slice(X,W))* Lt(skf1(V,X,Z,X1),X)*.
	Given clause: 233[0:SSi:232.0,2.0] || Lt(Ta1,U) NoExitCavity(Ta1,U,Hc1,V)*+ -> P(Slice(U,HPlace(Ox1)),Slice(U,Hc1))* Lt(skf1(Ta1,U,W,X),U)*.
	Given clause: 192[0:MRR:188.1,155.1] Object(U) || P(Slice(V,W),Place(V,U))*+ Continuous(V,X,W)* NoExitCavity(V,X,HPlace(U),Y)* -> P(Slice(X,W),Slice(X,HPlace(U)))* Lt(skf1(V,X,Z,X1),X)*.
	Given clause: 201[0:MRR:200.1,155.1] Object(U) || P(Place(V,U),Slice(V,W))*+ Continuous(V,X,HPlace(U))* NoExitCavity(V,X,W,Y)* -> Lt(V,skf1(V,Z,X1,X2))* P(Slice(X,HPlace(U)),Slice(X,W))*.
	Given clause: 202[0:MRR:198.1,155.1] Object(U) || P(Slice(V,W),Place(V,U))*+ Continuous(V,X,W)* NoExitCavity(V,X,HPlace(U),Y)* -> Lt(V,skf1(V,Z,X1,X2))* P(Slice(X,W),Slice(X,HPlace(U)))*.
	Given clause: 216[0:SpL:12.0,72.0] || P(Rc1,Slice(Ta1,U))+ Continuous(Ta1,V,Hc1) NoExitCavity(Ta1,V,U,W)* -> P(Slice(V,Hc1),Slice(V,U))* O(Slice(skf1(Ta1,V,W,Hc1),Hc1),Slice(skf1(Ta1,V,W,Hc1),W))*.
	Given clause: 245[0:SpL:12.0,216.0] || P(Rc1,Rc1) Continuous(Ta1,U,Hc1) NoExitCavity(Ta1,U,Hc1,V) -> P(Slice(U,Hc1),Slice(U,Hc1)) O(Slice(skf1(Ta1,U,V,Hc1),Hc1),Slice(skf1(Ta1,U,V,Hc1),V))*.
	Given clause: 250[0:Res:245.4,132.0] || P(Rc1,Rc1) Continuous(Ta1,U,Hc1) NoExitCavity(Ta1,U,Hc1,V)+ -> P(Slice(U,Hc1),Slice(U,Hc1))* Region(Slice(skf1(Ta1,U,V,Hc1),Hc1))*.
	Given clause: 252[0:Res:25.0,250.2] || P(Rc1,Rc1) Continuous(Ta1,Tb1,Hc1) -> P(Slice(Tb1,Hc1),Slice(Tb1,Hc1)) Region(Slice(skf1(Ta1,Tb1,HPlace(Ob1),Hc1),Hc1))*.
	Given clause: 249[0:Res:245.4,133.0] || P(Rc1,Rc1) Continuous(Ta1,U,Hc1) NoExitCavity(Ta1,U,Hc1,V)+ -> P(Slice(U,Hc1),Slice(U,Hc1))* Region(Slice(skf1(Ta1,U,V,Hc1),V))*.
	Given clause: 214[0:SpL:12.0,72.0] || P(Slice(Ta1,U),Rc1) Continuous(Ta1,V,U) NoExitCavity(Ta1,V,Hc1,W) -> P(Slice(V,U),Slice(V,Hc1)) O(Slice(skf1(Ta1,V,W,U),U),Slice(skf1(Ta1,V,W,U),W))*.
	Given clause: 253[0:Res:25.0,249.2] || P(Rc1,Rc1) Continuous(Ta1,Tb1,Hc1) -> P(Slice(Tb1,Hc1),Slice(Tb1,Hc1)) Region(Slice(skf1(Ta1,Tb1,HPlace(Ob1),Hc1),HPlace(Ob1)))*.
	Given clause: 257[0:Res:214.4,132.0] || P(Slice(Ta1,U),Rc1)+ Continuous(Ta1,V,U) NoExitCavity(Ta1,V,Hc1,W) -> P(Slice(V,U),Slice(V,Hc1))* Region(Slice(skf1(Ta1,V,W,U),U))*.
	Given clause: 256[0:Res:214.4,133.0] || P(Slice(Ta1,U),Rc1)+ Continuous(Ta1,V,U) NoExitCavity(Ta1,V,Hc1,W) -> P(Slice(V,U),Slice(V,Hc1))* Region(Slice(skf1(Ta1,V,W,U),W))*.
	Given clause: 266[0:SSi:265.1,3.0] Object(U) || P(Place(Ta1,U),Rc1)+ Continuous(Ta1,V,HPlace(U)) NoExitCavity(Ta1,V,Hc1,W) -> P(Slice(V,HPlace(U)),Slice(V,Hc1))* Region(Slice(skf1(Ta1,V,W,HPlace(U)),W))*.
	Given clause: 218[0:MRR:215.1,155.1] Object(U) || P(Slice(V,W),Place(V,U))*+ Continuous(V,X,W) NoExitCavity(V,X,HPlace(U),Y)* -> P(Slice(X,W),Slice(X,HPlace(U)))* O(Slice(skf1(V,X,Y,W),W),Slice(skf1(V,X,Y,W),Y))*.
	Given clause: 268[0:SSi:267.0,2.0] || Continuous(Ta1,U,HPlace(Ox1))+ NoExitCavity(Ta1,U,Hc1,V) -> P(Slice(U,HPlace(Ox1)),Slice(U,Hc1))* Region(Slice(skf1(Ta1,U,V,HPlace(Ox1)),V))*.
	Given clause: 273[0:SSi:272.0,2.0] || Lt(Ta1,U) NoExitCavity(Ta1,U,Hc1,V)+ -> P(Slice(U,HPlace(Ox1)),Slice(U,Hc1))* Region(Slice(skf1(Ta1,U,V,HPlace(Ox1)),V))*.
	Given clause: 275[0:MRR:274.0,274.1,7.0,57.0] ||  -> Region(Slice(skf1(Ta1,Tb1,HPlace(Ob1),HPlace(Ox1)),HPlace(Ob1)))*.
	Given clause: 263[0:SSi:262.1,3.0] Object(U) || P(Place(Ta1,U),Rc1)+ Continuous(Ta1,V,HPlace(U)) NoExitCavity(Ta1,V,Hc1,W) -> P(Slice(V,HPlace(U)),Slice(V,Hc1))* Region(Slice(skf1(Ta1,V,W,HPlace(U)),HPlace(U)))*.
	Given clause: 219[0:MRR:217.1,155.1] Object(U) || P(Place(V,U),Slice(V,W))*+ Continuous(V,X,HPlace(U)) NoExitCavity(V,X,W,Y)* -> P(Slice(X,HPlace(U)),Slice(X,W))* O(Slice(skf1(V,X,Y,HPlace(U)),HPlace(U)),Slice(skf1(V,X,Y,HPlace(U)),Y))*.
	Given clause: 278[0:SSi:277.0,2.0] || Continuous(Ta1,U,HPlace(Ox1))+ NoExitCavity(Ta1,U,Hc1,V) -> P(Slice(U,HPlace(Ox1)),Slice(U,Hc1))* Region(Slice(skf1(Ta1,U,V,HPlace(Ox1)),HPlace(Ox1)))*.
	Given clause: 282[0:SSi:281.0,2.0] || Lt(Ta1,U) NoExitCavity(Ta1,U,Hc1,V)+ -> P(Slice(U,HPlace(Ox1)),Slice(U,Hc1))* Region(Slice(skf1(Ta1,U,V,HPlace(Ox1)),HPlace(Ox1)))*.
	Given clause: 284[0:MRR:283.0,283.1,7.0,57.0] ||  -> Region(Slice(skf1(Ta1,Tb1,HPlace(Ob1),HPlace(Ox1)),HPlace(Ox1)))*.
	Given clause: 251[0:SSi:248.1,221.0,24.1,5.0] Object(U) || P(Rc1,Rc1) Continuous(Ta1,V,Hc1) NoExitCavity(Ta1,V,Hc1,HPlace(U)) -> P(Slice(V,Hc1),Slice(V,Hc1)) O(Slice(skf1(Ta1,V,HPlace(U),Hc1),Hc1),Place(skf1(Ta1,V,HPlace(U),Hc1),U))*.
	Given clause: 236[0:MRR:235.1,155.1] Object(U) Object(V) || P(Place(W,V),Place(W,U))*+ Continuous(W,X,HPlace(V))* NoExitCavity(W,X,HPlace(U),Y)* -> P(Slice(X,HPlace(V)),Slice(X,HPlace(U)))* Lt(skf1(W,X,Z,X1),X)*.
	Given clause: 286[0:Res:251.5,133.0] Object(U) || P(Rc1,Rc1) Continuous(Ta1,V,Hc1) NoExitCavity(Ta1,V,Hc1,HPlace(U))+ -> P(Slice(V,Hc1),Slice(V,Hc1))* Region(Place(skf1(Ta1,V,HPlace(U),Hc1),U))*.
	Given clause: 289[0:SSi:288.0,1.0] || P(Rc1,Rc1) Continuous(Ta1,Tb1,Hc1) -> P(Slice(Tb1,Hc1),Slice(Tb1,Hc1)) Region(Place(skf1(Ta1,Tb1,HPlace(Ob1),Hc1),Ob1))*.
	Given clause: 290[1:Spt:289.2] ||  -> P(Slice(Tb1,Hc1),Slice(Tb1,Hc1))*.
	Given clause: 291[1:Res:290.0,137.0] ||  -> Region(Slice(Tb1,Hc1))*.
	Given clause: 294[1:Res:290.0,71.0] || Continuous(Tb1,U,Hc1) NoExitCavity(Tb1,U,Hc1,V)*+ -> Lt(Tb1,skf1(Tb1,W,X,Y))* P(Slice(U,Hc1),Slice(U,Hc1))*.
	Given clause: 296[2:Spt:294.0,294.1,294.3] || Continuous(Tb1,U,Hc1) NoExitCavity(Tb1,U,Hc1,V)*+ -> P(Slice(U,Hc1),Slice(U,Hc1))*.
	Given clause: 242[0:MRR:241.1,155.1] Object(U) Object(V) || P(Place(W,V),Place(W,U))*+ Continuous(W,X,HPlace(V))* NoExitCavity(W,X,HPlace(U),Y)* -> Lt(W,skf1(W,Z,X1,X2))* P(Slice(X,HPlace(V)),Slice(X,HPlace(U)))*.
	Given clause: 247[0:SSi:246.1,3.0] Object(U) || P(Rc1,Place(Ta1,U)) Continuous(Ta1,V,Hc1) NoExitCavity(Ta1,V,HPlace(U),W)*+ -> P(Slice(V,Hc1),Slice(V,HPlace(U)))* O(Slice(skf1(Ta1,V,W,Hc1),Hc1),Slice(skf1(Ta1,V,W,Hc1),W))*.
	Given clause: 258[0:SSi:254.1,221.1,24.0] Object(U) || P(Slice(Ta1,V),Rc1) Continuous(Ta1,W,V) NoExitCavity(Ta1,W,Hc1,HPlace(U)) -> P(Slice(W,V),Slice(W,Hc1)) O(Slice(skf1(Ta1,W,HPlace(U),V),V),Place(skf1(Ta1,W,HPlace(U),V),U))*.
	Given clause: 298[0:Res:258.5,133.0] Object(U) || P(Slice(Ta1,V),Rc1) Continuous(Ta1,W,V) NoExitCavity(Ta1,W,Hc1,HPlace(U))+ -> P(Slice(W,V),Slice(W,Hc1))* Region(Place(skf1(Ta1,W,HPlace(U),V),U))*.
	Given clause: 302[0:SSi:301.0,1.0] || P(Slice(Ta1,U),Rc1) Continuous(Ta1,Tb1,U) -> P(Slice(Tb1,U),Slice(Tb1,Hc1)) Region(Place(skf1(Ta1,Tb1,HPlace(Ob1),U),Ob1))*.
	Given clause: 259[0:SSi:255.1,221.1,24.0] Object(U) || P(Slice(Ta1,HPlace(U)),Rc1) Continuous(Ta1,V,HPlace(U)) NoExitCavity(Ta1,V,Hc1,W) -> P(Slice(V,HPlace(U)),Slice(V,Hc1)) O(Place(skf1(Ta1,V,W,HPlace(U)),U),Slice(skf1(Ta1,V,W,HPlace(U)),W))*.
	Given clause: 305[0:Res:259.5,132.0] Object(U) || P(Slice(Ta1,HPlace(U)),Rc1)+ Continuous(Ta1,V,HPlace(U)) NoExitCavity(Ta1,V,Hc1,W) -> P(Slice(V,HPlace(U)),Slice(V,Hc1))* Region(Place(skf1(Ta1,V,W,HPlace(U)),U))*.
	Given clause: 308[0:SSi:307.0,3.0] Object(U) || P(Place(Ta1,U),Rc1)+ Continuous(Ta1,V,HPlace(U)) NoExitCavity(Ta1,V,Hc1,W) -> P(Slice(V,HPlace(U)),Slice(V,Hc1))* Region(Place(skf1(Ta1,V,W,HPlace(U)),U))*.
	Given clause: 310[0:SSi:309.0,2.0] || Continuous(Ta1,U,HPlace(Ox1))+ NoExitCavity(Ta1,U,Hc1,V) -> P(Slice(U,HPlace(Ox1)),Slice(U,Hc1))* Region(Place(skf1(Ta1,U,V,HPlace(Ox1)),Ox1))*.
	Given clause: 312[0:SSi:311.0,2.0] || Lt(Ta1,U) NoExitCavity(Ta1,U,Hc1,V)+ -> P(Slice(U,HPlace(Ox1)),Slice(U,Hc1))* Region(Place(skf1(Ta1,U,V,HPlace(Ox1)),Ox1))*.
	Given clause: 279[0:SpL:12.0,219.1] Object(U) || P(Place(Ta1,U),Rc1) Continuous(Ta1,V,HPlace(U)) NoExitCavity(Ta1,V,Hc1,W) -> P(Slice(V,HPlace(U)),Slice(V,Hc1)) O(Slice(skf1(Ta1,V,W,HPlace(U)),HPlace(U)),Slice(skf1(Ta1,V,W,HPlace(U)),W))*.
	Given clause: 314[0:MRR:313.0,313.1,7.0,57.0] ||  -> Region(Place(skf1(Ta1,Tb1,HPlace(Ob1),HPlace(Ox1)),Ox1))*.
	Given clause: 320[0:SSi:319.0,221.1,24.0] Object(U) || P(Place(Ta1,U),Rc1) Continuous(Ta1,V,HPlace(U)) NoExitCavity(Ta1,V,Hc1,W) -> P(Slice(V,HPlace(U)),Slice(V,Hc1)) O(Place(skf1(Ta1,V,W,HPlace(U)),U),Slice(skf1(Ta1,V,W,HPlace(U)),W))*.
	Given clause: 322[0:SSi:321.1,221.1,24.1,24.0] Object(U) Object(V) || P(Place(Ta1,V),Rc1) Continuous(Ta1,W,HPlace(V)) NoExitCavity(Ta1,W,Hc1,HPlace(U)) -> P(Slice(W,HPlace(V)),Slice(W,Hc1)) O(Place(skf1(Ta1,W,HPlace(U),HPlace(V)),V),Place(skf1(Ta1,W,HPlace(U),HPlace(V)),U))*.
	Given clause: 330[0:SSi:329.0,221.1,24.1,24.0] Object(U) Object(V) || P(Place(Ta1,V),Rc1) Continuous(Ta1,W,HPlace(V)) NoExitCavity(Ta1,W,Hc1,HPlace(U))*+ -> P(Slice(W,HPlace(V)),Slice(W,Hc1))* equal(V,U)*.
	Given clause: 271[0:MRR:270.1,155.1] Object(U) Object(V) || P(Place(W,U),Place(W,V))*+ Continuous(W,X,HPlace(U)) NoExitCavity(W,X,HPlace(V),Y)* -> P(Slice(X,HPlace(U)),Slice(X,HPlace(V)))* O(Slice(skf1(W,X,Y,HPlace(U)),HPlace(U)),Slice(skf1(W,X,Y,HPlace(U)),Y))*.
	Given clause: 332[0:SSi:331.0,1.0] Object(U) || P(Place(Ta1,U),Rc1) Continuous(Ta1,Tb1,HPlace(U)) -> P(Slice(Tb1,HPlace(U)),Slice(Tb1,Hc1))* equal(U,Ob1).
	Given clause: 343[0:MRR:342.0,342.2,11.0,8.0] || Continuous(Ta1,Tb1,HPlace(Ox1))* -> .
SPASS V 3.7 
SPASS beiseite: Proof found.
Problem: C:\Users\ang\Documents\Courant\Case1-Piece3.dfg 
SPASS derived 168 clauses, backtracked 0 clauses, performed 2 splits and kept 186 clauses.
SPASS allocated 31838 KBytes.
SPASS spent	0:00:00.56 on the problem.
		0:00:00.00 for the input.
		0:00:00.01 for the FLOTTER CNF translation.
		0:00:00.01 for inferences.
		0:00:00.00 for the backtracking.
		0:00:00.01 for the reduction.


Here is a proof with depth 7, length 48 :
1[0:Inp] ||  -> Object(Ob1)*.
2[0:Inp] ||  -> Object(Ox1)*.
3[0:Inp] ||  -> Time(Ta1)*.
7[0:Inp] ||  -> Lt(Ta1,Tb1)*.
8[0:Inp] || equal(Ob1,Ox1)** -> .
11[0:Inp] ||  -> P(Place(Ta1,Ox1),Rc1)*.
12[0:Inp] ||  -> equal(Slice(Ta1,Hc1),Rc1)**.
14[0:Inp] || Lt(U,V)* -> Time(V).
24[0:Inp] Object(U) ||  -> History(HPlace(U))*.
25[0:Inp] ||  -> NoExitCavity(Ta1,Tb1,Hc1,HPlace(Ob1))*.
52[0:Inp] || SkP3(U,V,W,X)* -> Time(X).
56[0:Inp] || DR(U,V)* O(U,V) -> .
57[0:Inp] || P(Slice(Tb1,HPlace(Ox1)),Slice(Tb1,Hc1))* -> .
63[0:Inp] || NoExitCavity(U,V,W,X) -> SkP3(X,W,V,U)*.
66[0:Inp] Object(U) || Lt(V,W) -> Continuous(V,W,HPlace(U))*.
68[0:Inp] Object(U) Time(V) ||  -> equal(Slice(V,HPlace(U)),Place(V,U))**.
69[0:Inp] Time(U) Object(V) Object(W) ||  -> equal(W,V) DR(Place(U,W),Place(U,V))*.
71[0:Inp] || P(Slice(U,V),Slice(U,W))*+ Continuous(U,X,V)* NoExitCavity(U,X,W,Y)* -> Lt(U,skf1(U,Z,X1,X2))* P(Slice(X,V),Slice(X,W))*.
72[0:Inp] || P(Slice(U,V),Slice(U,W))*+ Continuous(U,X,V) NoExitCavity(U,X,W,Y)* -> P(Slice(X,V),Slice(X,W))* O(Slice(skf1(U,X,Y,V),V),Slice(skf1(U,X,Y,V),Y))*.
74[0:Res:71.4,57.0] || P(Slice(U,HPlace(Ox1)),Slice(U,Hc1))*+ Continuous(U,Tb1,HPlace(Ox1)) NoExitCavity(U,Tb1,Hc1,V)* -> Lt(U,skf1(U,W,X,Y))*.
155[0:Res:63.1,52.0] || NoExitCavity(U,V,W,X)* -> Time(U).
174[0:Res:69.4,56.0] Time(U) Object(V) Object(W) || O(Place(U,W),Place(U,V))* -> equal(W,V).
203[0:SpL:12.0,74.0] || P(Slice(Ta1,HPlace(Ox1)),Rc1)+ Continuous(Ta1,Tb1,HPlace(Ox1)) NoExitCavity(Ta1,Tb1,Hc1,U)* -> Lt(Ta1,skf1(Ta1,V,W,X))*.
207[0:SpL:68.2,203.0] Object(Ox1) Time(Ta1) || P(Place(Ta1,Ox1),Rc1) Continuous(Ta1,Tb1,HPlace(Ox1)) NoExitCavity(Ta1,Tb1,Hc1,U)* -> Lt(Ta1,skf1(Ta1,V,W,X))*.
208[0:SSi:207.1,207.0,3.0,2.0] || P(Place(Ta1,Ox1),Rc1) Continuous(Ta1,Tb1,HPlace(Ox1)) NoExitCavity(Ta1,Tb1,Hc1,U)* -> Lt(Ta1,skf1(Ta1,V,W,X))*.
209[0:MRR:208.0,11.0] || Continuous(Ta1,Tb1,HPlace(Ox1))+ NoExitCavity(Ta1,Tb1,Hc1,U)* -> Lt(Ta1,skf1(Ta1,V,W,X))*.
210[0:Res:66.2,209.0] Object(Ox1) || Lt(Ta1,Tb1) NoExitCavity(Ta1,Tb1,Hc1,U)* -> Lt(Ta1,skf1(Ta1,V,W,X))*.
211[0:SSi:210.0,2.0] || Lt(Ta1,Tb1) NoExitCavity(Ta1,Tb1,Hc1,U)* -> Lt(Ta1,skf1(Ta1,V,W,X))*.
212[0:MRR:211.0,7.0] || NoExitCavity(Ta1,Tb1,Hc1,U)*+ -> Lt(Ta1,skf1(Ta1,V,W,X))*.
213[0:Res:25.0,212.0] ||  -> Lt(Ta1,skf1(Ta1,U,V,W))*.
217[0:SpL:68.2,72.0] Object(U) Time(V) || P(Place(V,U),Slice(V,W))* Continuous(V,X,HPlace(U)) NoExitCavity(V,X,W,Y)* -> P(Slice(X,HPlace(U)),Slice(X,W))* O(Slice(skf1(V,X,Y,HPlace(U)),HPlace(U)),Slice(skf1(V,X,Y,HPlace(U)),Y))*.
219[0:MRR:217.1,155.1] Object(U) || P(Place(V,U),Slice(V,W))*+ Continuous(V,X,HPlace(U)) NoExitCavity(V,X,W,Y)* -> P(Slice(X,HPlace(U)),Slice(X,W))* O(Slice(skf1(V,X,Y,HPlace(U)),HPlace(U)),Slice(skf1(V,X,Y,HPlace(U)),Y))*.
221[0:Res:213.0,14.0] ||  -> Time(skf1(Ta1,U,V,W))*.
279[0:SpL:12.0,219.1] Object(U) || P(Place(Ta1,U),Rc1) Continuous(Ta1,V,HPlace(U)) NoExitCavity(Ta1,V,Hc1,W) -> P(Slice(V,HPlace(U)),Slice(V,Hc1)) O(Slice(skf1(Ta1,V,W,HPlace(U)),HPlace(U)),Slice(skf1(Ta1,V,W,HPlace(U)),W))*.
315[0:SpR:68.2,279.5] Object(U) Time(skf1(Ta1,V,HPlace(U),HPlace(W))) Object(W) || P(Place(Ta1,W),Rc1) Continuous(Ta1,V,HPlace(W)) NoExitCavity(Ta1,V,Hc1,HPlace(U)) -> P(Slice(V,HPlace(W)),Slice(V,Hc1)) O(Slice(skf1(Ta1,V,HPlace(U),HPlace(W)),HPlace(W)),Place(skf1(Ta1,V,HPlace(U),HPlace(W)),U))*.
321[0:Rew:68.2,315.7] Object(U) Time(skf1(Ta1,V,HPlace(U),HPlace(W))) Object(W) || P(Place(Ta1,W),Rc1) Continuous(Ta1,V,HPlace(W)) NoExitCavity(Ta1,V,Hc1,HPlace(U)) -> P(Slice(V,HPlace(W)),Slice(V,Hc1)) O(Place(skf1(Ta1,V,HPlace(U),HPlace(W)),W),Place(skf1(Ta1,V,HPlace(U),HPlace(W)),U))*.
322[0:SSi:321.1,221.1,24.1,24.0] Object(U) Object(V) || P(Place(Ta1,V),Rc1) Continuous(Ta1,W,HPlace(V)) NoExitCavity(Ta1,W,Hc1,HPlace(U)) -> P(Slice(W,HPlace(V)),Slice(W,Hc1)) O(Place(skf1(Ta1,W,HPlace(U),HPlace(V)),V),Place(skf1(Ta1,W,HPlace(U),HPlace(V)),U))*.
328[0:Res:322.6,174.3] Object(U) Object(V) Time(skf1(Ta1,W,HPlace(U),HPlace(V))) Object(U) Object(V) || P(Place(Ta1,V),Rc1) Continuous(Ta1,W,HPlace(V)) NoExitCavity(Ta1,W,Hc1,HPlace(U))* -> P(Slice(W,HPlace(V)),Slice(W,Hc1))* equal(V,U)*.
329[0:Obv:328.1] Time(skf1(Ta1,U,HPlace(V),HPlace(W))) Object(V) Object(W) || P(Place(Ta1,W),Rc1) Continuous(Ta1,U,HPlace(W)) NoExitCavity(Ta1,U,Hc1,HPlace(V))* -> P(Slice(U,HPlace(W)),Slice(U,Hc1))* equal(W,V)*.
330[0:SSi:329.0,221.1,24.1,24.0] Object(U) Object(V) || P(Place(Ta1,V),Rc1) Continuous(Ta1,W,HPlace(V)) NoExitCavity(Ta1,W,Hc1,HPlace(U))*+ -> P(Slice(W,HPlace(V)),Slice(W,Hc1))* equal(V,U)*.
331[0:Res:25.0,330.4] Object(Ob1) Object(U) || P(Place(Ta1,U),Rc1) Continuous(Ta1,Tb1,HPlace(U)) -> P(Slice(Tb1,HPlace(U)),Slice(Tb1,Hc1))* equal(U,Ob1).
332[0:SSi:331.0,1.0] Object(U) || P(Place(Ta1,U),Rc1) Continuous(Ta1,Tb1,HPlace(U)) -> P(Slice(Tb1,HPlace(U)),Slice(Tb1,Hc1))* equal(U,Ob1).
336[0:Res:332.3,57.0] Object(Ox1) || P(Place(Ta1,Ox1),Rc1) Continuous(Ta1,Tb1,HPlace(Ox1))* -> equal(Ob1,Ox1).
342[0:SSi:336.0,2.0] || P(Place(Ta1,Ox1),Rc1) Continuous(Ta1,Tb1,HPlace(Ox1))* -> equal(Ob1,Ox1).
343[0:MRR:342.0,342.2,11.0,8.0] || Continuous(Ta1,Tb1,HPlace(Ox1))* -> .
346[0:Res:66.2,343.0] Object(Ox1) || Lt(Ta1,Tb1)* -> .
347[0:SSi:346.0,2.0] || Lt(Ta1,Tb1)* -> .
348[0:MRR:347.0,7.0] ||  -> .
Formulae used in the proof : axiom19 axiom20 axiom21 axiom28 axiom29 axiom26 axiom27 axiom0 axiom14 axiom25 axiom16 axiom33 conjecture0 axiom30 axiom31 axiom32 axiom34

--------------------------SPASS-STOP------------------------------