--------------------------SPASS-START-----------------------------
Input Problem:
1[0:Inp] ||  -> Lt(Ta1,Tb1)*.
2[0:Inp] || equal(Ob1,Ox1)** -> .
3[0:Inp] || IntConn(U)* -> Region(U).
4[0:Inp] || RigidObject(U) -> Object(U)*.
5[0:Inp] || RigidHistory(U) -> History(U)*.
6[0:Inp] ||  -> P(Place(Ta1,Ox1),Rc1)*.
7[0:Inp] ||  -> equal(Slice(Ta1,Hc1),Rc1)**.
8[0:Inp] || Lt(U,V)* -> Time(U).
9[0:Inp] || Lt(U,V)* -> Time(V).
10[0:Inp] || Leq(U,V)* -> Time(U).
11[0:Inp] || Leq(U,V)* -> Time(V).
12[0:Inp] || Ordered(U,V)* -> Time(U).
13[0:Inp] || Ordered(U,V)* -> Time(V).
14[0:Inp] || SkP0(U,V)* -> Region(V).
15[0:Inp] || SkP0(U,V)* -> Region(U).
16[0:Inp] || SkP1(U,V)* -> Region(V).
17[0:Inp] || SkP1(U,V)* -> Region(U).
18[0:Inp] || Object(U) -> ObjectSet(Singleton(U))*.
19[0:Inp] || Object(U) -> History(HPlace(U))*.
20[0:Inp] ||  -> NoExitCavity(Ta1,Tb1,Hc1,HPlace(Ob1))*.
21[0:Inp] || DR(U,V)* -> Region(U).
22[0:Inp] || DR(U,V)* -> Region(V).
23[0:Inp] || Cavity(U,V)* -> IntConn(U).
24[0:Inp] || Leq3(U,V,W)* -> Time(U).
25[0:Inp] || Leq3(U,V,W)* -> Time(V).
26[0:Inp] || Leq3(U,V,W)* -> Time(W).
27[0:Inp] || P(U,V) -> SkP0(V,U)*.
28[0:Inp] || O(U,V) -> SkP0(V,U)*.
29[0:Inp] || EC(U,V) -> SkP0(V,U)*.
30[0:Inp] || DR(U,V) -> SkP0(V,U)*.
31[0:Inp] || Cavity(U,V) -> SkP1(V,U)*.
32[0:Inp] || Outside(U,V) -> SkP1(V,U)*.
33[0:Inp] || OSPlace(U,V,W)* -> Time(U).
34[0:Inp] || OSPlace(U,V,W)* -> ObjectSet(V).
35[0:Inp] || OSPlace(U,V,W)* -> Region(W).
36[0:Inp] || ClosedContainer(U,V,W)* -> Time(U).
37[0:Inp] || ClosedContainer(U,V,W)* -> ObjectSet(V).
38[0:Inp] || ClosedContainer(U,V,W)* -> Region(W).
39[0:Inp] || CContained(U,V,W)* -> Time(U).
40[0:Inp] || CContained(U,V,W)* -> Object(V).
41[0:Inp] || CContained(U,V,W)* -> ObjectSet(W).
42[0:Inp] || SkP2(U,V,W)* -> Time(W).
43[0:Inp] || SkP2(U,V,W)* -> Time(V).
44[0:Inp] || SkP2(U,V,W)* -> History(U).
45[0:Inp] || Constant(U,V,W)* -> Time(U).
46[0:Inp] || Constant(U,V,W)* -> Time(V).
47[0:Inp] || Constant(U,V,W)* -> History(W).
48[0:Inp] || AlwaysIntConn(U,V,W)* -> Time(U).
49[0:Inp] || AlwaysIntConn(U,V,W)* -> Time(V).
50[0:Inp] || AlwaysIntConn(U,V,W)* -> History(W).
51[0:Inp] || Cavity(U,V) -> DR(U,V)*.
52[0:Inp] || AlwaysIntConn(U,V,W)* -> History(W).
53[0:Inp] || SkP3(U,V,W,X)* -> Time(X).
54[0:Inp] || SkP3(U,V,W,X)* -> Time(W).
55[0:Inp] || SkP3(U,V,W,X)* -> History(V).
56[0:Inp] || SkP3(U,V,W,X)* -> History(U).
57[0:Inp] || O(U,V) DR(U,V)* -> .
58[0:Inp] || AlwaysIntConn(U,V,W)* -> Lt(U,V).
59[0:Inp] || P(Slice(Tb1,HPlace(Ox1)),Slice(Tb1,Hc1))* -> .
60[0:Inp] || Continuous(U,V,W) -> SkP2(W,V,U)*.
61[0:Inp] || WeaklyContinuous(U,V,W) -> SkP2(W,V,U)*.
62[0:Inp] || Region(U) Region(V) -> Region(RUnion(U,V))*.
63[0:Inp] || Time(U) Object(V) -> Region(Place(U,V))*.
64[0:Inp] || Time(U) History(V) -> Region(Slice(U,V))*.
65[0:Inp] || NoExitCavity(U,V,W,X) -> SkP3(X,W,V,U)*.
66[0:Inp] || NoEntranceCavity(U,V,W,X) -> SkP3(X,W,V,U)*.
67[0:Inp] || PersistentCavity(U,V,W,X) -> SkP3(X,W,V,U)*.
68[0:Inp] || Lt(U,V) Object(W) -> Continuous(U,V,HPlace(W))*.
69[0:Inp] || Region(U) Region(V) -> O(V,U) DR(V,U)*.
70[0:Inp] || Time(U) Object(V) -> equal(Slice(U,HPlace(V)),Place(U,V))**.
71[0:Inp] || DR(U,V)* IntConn(U) -> IntConn(skf3(W,X))* Cavity(U,V).
72[0:Inp] || Leq3(U,V,W)* AlwaysIntConn(U,W,X)* -> IntConn(Slice(V,X))*.
73[0:Inp] || DR(U,V) IntConn(U) -> O(skf3(V,U),U)* Cavity(U,V).
74[0:Inp] || DR(U,V)* IntConn(U) -> DR(skf3(V,W),V)* Cavity(U,V).
75[0:Inp] || P(skf3(U,V),V)* DR(V,U) IntConn(V) -> Cavity(V,U).
76[0:Inp] || IntConn(U) O(U,V)* DR(U,W)* Cavity(V,W)* -> P(U,V).
77[0:Inp] || Lt(U,V) History(W) -> Leq3(U,skf4(W,V,U),V)* AlwaysIntConn(U,V,W).
78[0:Inp] || Object(U) Object(V) Time(W) -> equal(U,V) DR(Place(W,U),Place(W,V))*.
79[0:Inp] || IntConn(Slice(skf4(U,V,W),U))* Lt(X,Y) History(U) -> AlwaysIntConn(X,Y,U)*.
80[0:Inp] || NoExitCavity(U,V,W,X)* P(Slice(U,Y),Slice(U,W))* AlwaysIntConn(U,V,Y)* Continuous(U,V,Y) -> Lt(skf5(U,V,Z,X1),V)* P(Slice(V,Y),Slice(V,W))*.
81[0:Inp] || NoExitCavity(U,V,W,X)* P(Slice(U,Y),Slice(U,W))* AlwaysIntConn(U,V,Y)* Continuous(U,V,Y) -> Lt(U,skf5(U,Z,X1,X2))* P(Slice(V,Y),Slice(V,W))*.
82[0:Inp] || NoExitCavity(U,V,W,X)* P(Slice(U,Y),Slice(U,W))* AlwaysIntConn(U,V,Y) Continuous(U,V,Y) -> O(Slice(skf5(U,V,X,Y),Y),Slice(skf5(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.
 The conjecture is ground.
 Axiom clauses: 81 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 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: skf5 > skf2 > skf4 > skf1 > skf3 > skf0 > Slice > Place > RUnion > HPlace > Singleton > SkP2 > SkP1 > SkP0 > IntConn > AlwaysIntConn > Continuous > DR > O > Cavity > P > Leq3 > Lt > History > Region > Time > Ordered > ObjectSet > Object > Leq > OSPlace > ClosedContainer > CContained > RigidObject > RigidHistory > EC > Outside > SkP3 > NoExitCavity > PersistentCavity > NoEntranceCavity > WeaklyContinuous > Constant > skc9 > skc8 > skc7 > skc6 > skc5 > skc4 > skc3 > skc2 > skc1 > skc0 > Hc1 > Rc1 > Tb1 > Ta1 > Ob1 > Ox1
 Ordering  : KBO
Processed Problem:

Worked Off Clauses:

Usable Clauses:
1[0:Inp] ||  -> Lt(Ta1,Tb1)*.
2[0:Inp] || equal(Ob1,Ox1)** -> .
7[0:Inp] ||  -> equal(Slice(Ta1,Hc1),Rc1)**.
6[0:Inp] ||  -> P(Place(Ta1,Ox1),Rc1)*.
4[0:Inp] RigidObject(U) ||  -> Object(U)*.
5[0:Inp] RigidHistory(U) ||  -> History(U)*.
3[0:Inp] IntConn(U) ||  -> Region(U)*.
20[0:Inp] ||  -> NoExitCavity(Ta1,Tb1,Hc1,HPlace(Ob1))*.
18[0:Inp] Object(U) ||  -> ObjectSet(Singleton(U))*.
19[0:Inp] Object(U) ||  -> History(HPlace(U))*.
23[0:Inp] || Cavity(U,V)* -> IntConn(U).
17[0:Inp] || SkP1(U,V)* -> Region(U).
16[0:Inp] || SkP1(U,V)* -> Region(V).
15[0:Inp] || SkP0(U,V)* -> Region(U).
14[0:Inp] || SkP0(U,V)* -> Region(V).
22[0:Inp] || DR(U,V)* -> Region(V).
21[0:Inp] || DR(U,V)* -> Region(U).
13[0:Inp] || Ordered(U,V)* -> Time(V).
12[0:Inp] || Ordered(U,V)* -> Time(U).
11[0:Inp] || Leq(U,V)* -> Time(V).
10[0:Inp] || Leq(U,V)* -> Time(U).
9[0:Inp] || Lt(U,V)* -> Time(V).
8[0:Inp] || Lt(U,V)* -> Time(U).
32[0:Inp] || Outside(U,V) -> SkP1(V,U)*.
31[0:Inp] || Cavity(U,V) -> SkP1(V,U)*.
29[0:Inp] || EC(U,V) -> SkP0(V,U)*.
28[0:Inp] || O(U,V) -> SkP0(V,U)*.
27[0:Inp] || P(U,V) -> SkP0(V,U)*.
30[0:Inp] || DR(U,V) -> SkP0(V,U)*.
51[0:Inp] || Cavity(U,V) -> DR(U,V)*.
41[0:Inp] || CContained(U,V,W)* -> ObjectSet(W).
37[0:Inp] || ClosedContainer(U,V,W)* -> ObjectSet(V).
34[0:Inp] || OSPlace(U,V,W)* -> ObjectSet(V).
40[0:Inp] || CContained(U,V,W)* -> Object(V).
47[0:Inp] || Constant(U,V,W)* -> History(W).
44[0:Inp] || SkP2(U,V,W)* -> History(U).
52[0:Inp] || AlwaysIntConn(U,V,W)* -> History(W).
38[0:Inp] || ClosedContainer(U,V,W)* -> Region(W).
35[0:Inp] || OSPlace(U,V,W)* -> Region(W).
46[0:Inp] || Constant(U,V,W)* -> Time(V).
45[0:Inp] || Constant(U,V,W)* -> Time(U).
39[0:Inp] || CContained(U,V,W)* -> Time(U).
36[0:Inp] || ClosedContainer(U,V,W)* -> Time(U).
33[0:Inp] || OSPlace(U,V,W)* -> Time(U).
43[0:Inp] || SkP2(U,V,W)* -> Time(V).
42[0:Inp] || SkP2(U,V,W)* -> Time(W).
26[0:Inp] || Leq3(U,V,W)* -> Time(W).
25[0:Inp] || Leq3(U,V,W)* -> Time(V).
24[0:Inp] || Leq3(U,V,W)* -> Time(U).
49[0:Inp] || AlwaysIntConn(U,V,W)* -> Time(V).
48[0:Inp] || AlwaysIntConn(U,V,W)* -> Time(U).
57[0:Inp] || DR(U,V)* O(U,V) -> .
58[0:Inp] || AlwaysIntConn(U,V,W)* -> Lt(U,V).
56[0:Inp] || SkP3(U,V,W,X)* -> History(U).
55[0:Inp] || SkP3(U,V,W,X)* -> History(V).
54[0:Inp] || SkP3(U,V,W,X)* -> Time(W).
53[0:Inp] || SkP3(U,V,W,X)* -> Time(X).
59[0:Inp] || P(Slice(Tb1,HPlace(Ox1)),Slice(Tb1,Hc1))* -> .
61[0:Inp] || WeaklyContinuous(U,V,W) -> SkP2(W,V,U)*.
60[0:Inp] || Continuous(U,V,W) -> SkP2(W,V,U)*.
62[0:Inp] Region(U) Region(V) ||  -> Region(RUnion(V,U))*.
63[0:Inp] Object(U) Time(V) ||  -> Region(Place(V,U))*.
64[0:Inp] History(U) Time(V) ||  -> Region(Slice(V,U))*.
67[0:Inp] || PersistentCavity(U,V,W,X) -> SkP3(X,W,V,U)*.
66[0:Inp] || NoEntranceCavity(U,V,W,X) -> SkP3(X,W,V,U)*.
65[0:Inp] || NoExitCavity(U,V,W,X) -> SkP3(X,W,V,U)*.
69[0:Inp] Region(U) Region(V) ||  -> DR(U,V)* O(U,V).
68[0:Inp] Object(U) || Lt(V,W) -> Continuous(V,W,HPlace(U))*.
70[0:Inp] Object(U) Time(V) ||  -> equal(Slice(V,HPlace(U)),Place(V,U))**.
71[0:Inp] IntConn(U) || DR(U,V)* -> IntConn(skf3(W,X))* Cavity(U,V).
72[0:Inp] || AlwaysIntConn(U,V,W)* Leq3(U,X,V)* -> IntConn(Slice(X,W))*.
73[0:Inp] IntConn(U) || DR(U,V) -> Cavity(U,V) O(skf3(V,U),U)*.
74[0:Inp] IntConn(U) || DR(U,V)* -> Cavity(U,V) DR(skf3(V,W),V)*.
75[0:Inp] IntConn(U) || DR(U,V) P(skf3(V,U),U)* -> Cavity(U,V).
77[0:Inp] History(U) || Lt(V,W) -> AlwaysIntConn(V,W,U) Leq3(V,skf4(U,W,V),W)*.
76[0:Inp] IntConn(U) || Cavity(V,W)* DR(U,W)* O(U,V)* -> P(U,V).
78[0:Inp] Time(U) Object(V) Object(W) ||  -> equal(W,V) DR(Place(U,W),Place(U,V))*.
79[0:Inp] History(U) || IntConn(Slice(skf4(U,V,W),U))* Lt(X,Y) -> AlwaysIntConn(X,Y,U)*.
83[0:Res:76.4,59.0] IntConn(Slice(Tb1,HPlace(Ox1))) || Cavity(Slice(Tb1,Hc1),U) DR(Slice(Tb1,HPlace(Ox1)),U)* O(Slice(Tb1,HPlace(Ox1)),Slice(Tb1,Hc1))* -> .
86[0:Res:80.5,59.0] || P(Slice(U,HPlace(Ox1)),Slice(U,Hc1))* Continuous(U,Tb1,HPlace(Ox1)) AlwaysIntConn(U,Tb1,HPlace(Ox1)) NoExitCavity(U,Tb1,Hc1,V)* -> Lt(skf5(U,Tb1,W,X),Tb1)*.
85[0:Res:81.5,59.0] || P(Slice(U,HPlace(Ox1)),Slice(U,Hc1))* Continuous(U,Tb1,HPlace(Ox1)) AlwaysIntConn(U,Tb1,HPlace(Ox1)) NoExitCavity(U,Tb1,Hc1,V)* -> Lt(U,skf5(U,W,X,Y))*.
80[0:Inp] || P(Slice(U,V),Slice(U,W))* Continuous(U,X,V) AlwaysIntConn(U,X,V)* NoExitCavity(U,X,W,Y)* -> P(Slice(X,V),Slice(X,W))* Lt(skf5(U,X,Z,X1),X)*.
81[0:Inp] || P(Slice(U,V),Slice(U,W))* Continuous(U,X,V) AlwaysIntConn(U,X,V)* NoExitCavity(U,X,W,Y)* -> Lt(U,skf5(U,Z,X1,X2))* P(Slice(X,V),Slice(X,W))*.
82[0:Inp] || P(Slice(U,V),Slice(U,W))* Continuous(U,X,V) AlwaysIntConn(U,X,V) NoExitCavity(U,X,W,Y)* -> P(Slice(X,V),Slice(X,W))* O(Slice(skf5(U,X,Y,V),V),Slice(skf5(U,X,Y,V),Y))*.
	Given clause: 71[0:Inp] IntConn(U) || DR(U,V)*+ -> IntConn(skf3(W,X))* Cavity(U,V).
	Given clause: 87[1:Spt:71.0,71.1,71.3] IntConn(U) || DR(U,V)* -> Cavity(U,V).
	Given clause: 1[0:Inp] ||  -> Lt(Ta1,Tb1)*.
	Given clause: 2[0:Inp] || equal(Ob1,Ox1)** -> .
	Given clause: 7[0:Inp] ||  -> equal(Slice(Ta1,Hc1),Rc1)**.
	Given clause: 6[0:Inp] ||  -> P(Place(Ta1,Ox1),Rc1)*.
	Given clause: 4[0:Inp] RigidObject(U) ||  -> Object(U)*.
	Given clause: 5[0:Inp] RigidHistory(U) ||  -> History(U)*.
	Given clause: 3[0:Inp] IntConn(U) ||  -> Region(U)*.
	Given clause: 20[0:Inp] ||  -> NoExitCavity(Ta1,Tb1,Hc1,HPlace(Ob1))*.
	Given clause: 18[0:Inp] Object(U) ||  -> ObjectSet(Singleton(U))*.
	Given clause: 19[0:Inp] Object(U) ||  -> History(HPlace(U))*.
	Given clause: 23[0:Inp] || Cavity(U,V)* -> IntConn(U).
	Given clause: 17[0:Inp] || SkP1(U,V)* -> Region(U).
	Given clause: 16[0:Inp] || SkP1(U,V)* -> Region(V).
	Given clause: 15[0:Inp] || SkP0(U,V)* -> Region(U).
	Given clause: 14[0:Inp] || SkP0(U,V)* -> Region(V).
	Given clause: 22[0:Inp] || DR(U,V)* -> Region(V).
	Given clause: 21[0:Inp] || DR(U,V)* -> Region(U).
	Given clause: 13[0:Inp] || Ordered(U,V)* -> Time(V).
	Given clause: 12[0:Inp] || Ordered(U,V)* -> Time(U).
	Given clause: 11[0:Inp] || Leq(U,V)* -> Time(V).
	Given clause: 10[0:Inp] || Leq(U,V)* -> Time(U).
	Given clause: 9[0:Inp] || Lt(U,V)* -> Time(V).
	Given clause: 89[0:Res:1.0,9.0] ||  -> Time(Tb1)*.
	Given clause: 8[0:Inp] || Lt(U,V)* -> Time(U).
	Given clause: 32[0:Inp] || Outside(U,V) -> SkP1(V,U)*.
	Given clause: 90[0:Res:1.0,8.0] ||  -> Time(Ta1)*.
	Given clause: 91[0:Res:32.1,16.0] || Outside(U,V)* -> Region(U).
	Given clause: 92[0:Res:32.1,17.0] || Outside(U,V)* -> Region(V).
	Given clause: 31[0:Inp] || Cavity(U,V) -> SkP1(V,U)*.
	Given clause: 29[0:Inp] || EC(U,V) -> SkP0(V,U)*.
	Given clause: 93[0:Res:31.1,16.0] || Cavity(U,V)* -> Region(U).
	Given clause: 94[0:Res:31.1,17.0] || Cavity(U,V)* -> Region(V).
	Given clause: 95[0:Res:29.1,14.0] || EC(U,V)* -> Region(U).
	Given clause: 96[0:Res:29.1,15.0] || EC(U,V)* -> Region(V).
	Given clause: 28[0:Inp] || O(U,V) -> SkP0(V,U)*.
	Given clause: 97[0:Res:28.1,14.0] || O(U,V)* -> Region(U).
	Given clause: 98[0:Res:28.1,15.0] || O(U,V)* -> Region(V).
	Given clause: 27[0:Inp] || P(U,V) -> SkP0(V,U)*.
	Given clause: 99[0:Res:27.1,14.0] || P(U,V)* -> Region(U).
	Given clause: 30[0:Inp] || DR(U,V) -> SkP0(V,U)*.
	Given clause: 101[0:Res:6.0,99.0] ||  -> Region(Place(Ta1,Ox1))*.
	Given clause: 100[0:Res:27.1,15.0] || P(U,V)* -> Region(V).
	Given clause: 104[0:Res:6.0,100.0] ||  -> Region(Rc1)*.
	Given clause: 51[0:Inp] || Cavity(U,V) -> DR(U,V)*.
	Given clause: 41[0:Inp] || CContained(U,V,W)* -> ObjectSet(W).
	Given clause: 37[0:Inp] || ClosedContainer(U,V,W)* -> ObjectSet(V).
	Given clause: 34[0:Inp] || OSPlace(U,V,W)* -> ObjectSet(V).
	Given clause: 40[0:Inp] || CContained(U,V,W)* -> Object(V).
	Given clause: 47[0:Inp] || Constant(U,V,W)* -> History(W).
	Given clause: 44[0:Inp] || SkP2(U,V,W)* -> History(U).
	Given clause: 52[0:Inp] || AlwaysIntConn(U,V,W)* -> History(W).
	Given clause: 38[0:Inp] || ClosedContainer(U,V,W)* -> Region(W).
	Given clause: 35[0:Inp] || OSPlace(U,V,W)* -> Region(W).
	Given clause: 46[0:Inp] || Constant(U,V,W)* -> Time(V).
	Given clause: 45[0:Inp] || Constant(U,V,W)* -> Time(U).
	Given clause: 39[0:Inp] || CContained(U,V,W)* -> Time(U).
	Given clause: 36[0:Inp] || ClosedContainer(U,V,W)* -> Time(U).
	Given clause: 33[0:Inp] || OSPlace(U,V,W)* -> Time(U).
	Given clause: 43[0:Inp] || SkP2(U,V,W)* -> Time(V).
	Given clause: 42[0:Inp] || SkP2(U,V,W)* -> Time(W).
	Given clause: 26[0:Inp] || Leq3(U,V,W)* -> Time(W).
	Given clause: 25[0:Inp] || Leq3(U,V,W)* -> Time(V).
	Given clause: 24[0:Inp] || Leq3(U,V,W)* -> Time(U).
	Given clause: 49[0:Inp] || AlwaysIntConn(U,V,W)* -> Time(V).
	Given clause: 48[0:Inp] || AlwaysIntConn(U,V,W)* -> Time(U).
	Given clause: 57[0:Inp] || DR(U,V)* O(U,V) -> .
	Given clause: 108[0:Res:51.1,57.0] || Cavity(U,V) O(U,V)* -> .
	Given clause: 58[0:Inp] || AlwaysIntConn(U,V,W)* -> Lt(U,V).
	Given clause: 56[0:Inp] || SkP3(U,V,W,X)* -> History(U).
	Given clause: 55[0:Inp] || SkP3(U,V,W,X)* -> History(V).
	Given clause: 54[0:Inp] || SkP3(U,V,W,X)* -> Time(W).
	Given clause: 53[0:Inp] || SkP3(U,V,W,X)* -> Time(X).
	Given clause: 59[0:Inp] || P(Slice(Tb1,HPlace(Ox1)),Slice(Tb1,Hc1))* -> .
	Given clause: 61[0:Inp] || WeaklyContinuous(U,V,W) -> SkP2(W,V,U)*.
	Given clause: 60[0:Inp] || Continuous(U,V,W) -> SkP2(W,V,U)*.
	Given clause: 109[0:Res:61.1,42.0] || WeaklyContinuous(U,V,W)* -> Time(U).
	Given clause: 110[0:Res:61.1,43.0] || WeaklyContinuous(U,V,W)* -> Time(V).
	Given clause: 111[0:Res:61.1,44.0] || WeaklyContinuous(U,V,W)* -> History(W).
	Given clause: 112[0:Res:60.1,42.0] || Continuous(U,V,W)* -> Time(U).
	Given clause: 62[0:Inp] Region(U) Region(V) ||  -> Region(RUnion(V,U))*.
	Given clause: 113[0:Res:60.1,43.0] || Continuous(U,V,W)* -> Time(V).
	Given clause: 114[0:Res:60.1,44.0] || Continuous(U,V,W)* -> History(W).
	Given clause: 63[0:Inp] Object(U) Time(V) ||  -> Region(Place(V,U))*.
	Given clause: 64[0:Inp] History(U) Time(V) ||  -> Region(Slice(V,U))*.
	Given clause: 67[0:Inp] || PersistentCavity(U,V,W,X) -> SkP3(X,W,V,U)*.
	Given clause: 116[0:Res:67.1,53.0] || PersistentCavity(U,V,W,X)* -> Time(U).
	Given clause: 117[0:Res:67.1,54.0] || PersistentCavity(U,V,W,X)* -> Time(V).
	Given clause: 118[0:Res:67.1,55.0] || PersistentCavity(U,V,W,X)* -> History(W).
	Given clause: 119[0:Res:67.1,56.0] || PersistentCavity(U,V,W,X)* -> History(X).
	Given clause: 66[0:Inp] || NoEntranceCavity(U,V,W,X) -> SkP3(X,W,V,U)*.
	Given clause: 120[0:Res:66.1,53.0] || NoEntranceCavity(U,V,W,X)* -> Time(U).
	Given clause: 121[0:Res:66.1,54.0] || NoEntranceCavity(U,V,W,X)* -> Time(V).
	Given clause: 122[0:Res:66.1,55.0] || NoEntranceCavity(U,V,W,X)* -> History(W).
	Given clause: 123[0:Res:66.1,56.0] || NoEntranceCavity(U,V,W,X)* -> History(X).
	Given clause: 65[0:Inp] || NoExitCavity(U,V,W,X) -> SkP3(X,W,V,U)*.
	Given clause: 124[0:Res:65.1,53.0] || NoExitCavity(U,V,W,X)* -> Time(U).
	Given clause: 125[0:Res:65.1,54.0] || NoExitCavity(U,V,W,X)* -> Time(V).
	Given clause: 126[0:Res:65.1,55.0] || NoExitCavity(U,V,W,X)* -> History(W).
	Given clause: 130[0:Res:20.0,126.0] ||  -> History(Hc1)*.
	Given clause: 69[0:Inp] Region(U) Region(V) ||  -> DR(U,V)* O(U,V).
	Given clause: 127[0:Res:65.1,56.0] || NoExitCavity(U,V,W,X)* -> History(X).
	Given clause: 136[0:Res:20.0,127.0] ||  -> History(HPlace(Ob1))*.
	Given clause: 68[0:Inp] Object(U) || Lt(V,W) -> Continuous(V,W,HPlace(U))*.
	Given clause: 135[1:SSi:134.0,3.1] Region(U) IntConn(V) ||  -> O(V,U)* Cavity(V,U).
	Given clause: 70[0:Inp] Object(U) Time(V) ||  -> equal(Slice(V,HPlace(U)),Place(V,U))**.
	Given clause: 146[0:SSi:145.1,89.0] Object(Ox1) || P(Place(Tb1,Ox1),Slice(Tb1,Hc1))* -> .
	Given clause: 148[0:SoR:146.0,4.1] RigidObject(Ox1) || P(Place(Tb1,Ox1),Slice(Tb1,Hc1))* -> .
	Given clause: 72[0:Inp] || AlwaysIntConn(U,V,W)*+ Leq3(U,X,V)* -> IntConn(Slice(X,W))*.
	Given clause: 76[0:Inp] IntConn(U) || Cavity(V,W)*+ DR(U,W)* O(U,V)* -> P(U,V).
	Given clause: 77[0:Inp] History(U) || Lt(V,W) -> AlwaysIntConn(V,W,U) Leq3(V,skf4(U,W,V),W)*.
	Given clause: 150[0:Res:77.3,25.0] History(U) || Lt(V,W) -> AlwaysIntConn(V,W,U) Time(skf4(U,W,V))*.
	Given clause: 78[0:Inp] Time(U) Object(V) Object(W) ||  -> equal(W,V) DR(Place(U,W),Place(U,V))*.
	Given clause: 79[0:Inp] History(U) || IntConn(Slice(skf4(U,V,W),U))*+ Lt(X,Y) -> AlwaysIntConn(X,Y,U)*.
	Given clause: 152[0:Res:78.4,57.0] Time(U) Object(V) Object(W) || O(Place(U,W),Place(U,V))* -> equal(W,V).
	Given clause: 80[0:Inp] || P(Slice(U,V),Slice(U,W))*+ Continuous(U,X,V) AlwaysIntConn(U,X,V)* NoExitCavity(U,X,W,Y)* -> P(Slice(X,V),Slice(X,W))* Lt(skf5(U,X,Z,X1),X)*.
	Given clause: 155[1:Res:78.4,87.1] Time(U) Object(V) Object(W) IntConn(Place(U,W)) ||  -> equal(W,V) Cavity(Place(U,W),Place(U,V))*.
	Given clause: 83[0:Res:76.4,59.0] IntConn(Slice(Tb1,HPlace(Ox1))) || Cavity(Slice(Tb1,Hc1),U) DR(Slice(Tb1,HPlace(Ox1)),U)* O(Slice(Tb1,HPlace(Ox1)),Slice(Tb1,Hc1))* -> .
	Given clause: 157[0:SSi:156.2,19.1] Object(U) Time(skf4(HPlace(U),V,W)) || IntConn(Place(skf4(HPlace(U),V,W),U))* Lt(X,Y) -> AlwaysIntConn(X,Y,HPlace(U))*.
	Given clause: 168[0:SSi:167.1,19.1] Object(U) || IntConn(Place(skf4(HPlace(U),V,W),U))* Lt(W,V) -> AlwaysIntConn(W,V,HPlace(U)).
	Given clause: 81[0:Inp] || P(Slice(U,V),Slice(U,W))*+ Continuous(U,X,V) AlwaysIntConn(U,X,V)* NoExitCavity(U,X,W,Y)* -> Lt(U,skf5(U,Z,X1,X2))* P(Slice(X,V),Slice(X,W))*.
	Given clause: 165[0:SoR:83.0,72.2] || Cavity(Slice(Tb1,Hc1),U) DR(Slice(Tb1,HPlace(Ox1)),U)* O(Slice(Tb1,HPlace(Ox1)),Slice(Tb1,Hc1))*+ Leq3(V,Tb1,W) AlwaysIntConn(V,W,HPlace(Ox1))* -> .
	Given clause: 180[1:MRR:179.0,72.2] || Cavity(Slice(Tb1,Hc1),U) DR(Slice(Tb1,HPlace(Ox1)),U)*+ Leq3(V,Tb1,W) AlwaysIntConn(V,W,HPlace(Ox1))* -> Cavity(Slice(Tb1,HPlace(Ox1)),Slice(Tb1,Hc1))*.
	Given clause: 183[1:Res:51.1,180.1] || Cavity(Slice(Tb1,HPlace(Ox1)),U)*+ Cavity(Slice(Tb1,Hc1),U) Leq3(V,Tb1,W) AlwaysIntConn(V,W,HPlace(Ox1))* -> Cavity(Slice(Tb1,HPlace(Ox1)),Slice(Tb1,Hc1))*.
	Given clause: 185[1:SSi:184.1,89.0] Object(Ox1) || Cavity(Slice(Tb1,Hc1),U) DR(Place(Tb1,Ox1),U)* Leq3(V,Tb1,W) AlwaysIntConn(V,W,HPlace(Ox1))* -> Cavity(Place(Tb1,Ox1),Slice(Tb1,Hc1))*.
	Given clause: 82[0:Inp] || P(Slice(U,V),Slice(U,W))*+ Continuous(U,X,V) AlwaysIntConn(U,X,V) NoExitCavity(U,X,W,Y)* -> P(Slice(X,V),Slice(X,W))* O(Slice(skf5(U,X,Y,V),V),Slice(skf5(U,X,Y,V),Y))*.
	Given clause: 189[1:SSi:188.1,89.0] Object(Ox1) || Cavity(Place(Tb1,Ox1),U) Cavity(Slice(Tb1,Hc1),U)* Leq3(V,Tb1,W) AlwaysIntConn(V,W,HPlace(Ox1))* -> Cavity(Place(Tb1,Ox1),Slice(Tb1,Hc1))*.
	Given clause: 190[1:SoR:185.0,4.1] RigidObject(Ox1) || Cavity(Slice(Tb1,Hc1),U) DR(Place(Tb1,Ox1),U)* Leq3(V,Tb1,W) AlwaysIntConn(V,W,HPlace(Ox1))* -> Cavity(Place(Tb1,Ox1),Slice(Tb1,Hc1))*.
	Given clause: 197[1:SoR:189.0,4.1] RigidObject(Ox1) || Cavity(Place(Tb1,Ox1),U) Cavity(Slice(Tb1,Hc1),U)* Leq3(V,Tb1,W) AlwaysIntConn(V,W,HPlace(Ox1))* -> Cavity(Place(Tb1,Ox1),Slice(Tb1,Hc1))*.
	Given clause: 178[0:SSi:177.1,89.0] Object(Ox1) || Cavity(Slice(Tb1,Hc1),U) DR(Place(Tb1,Ox1),U)* O(Place(Tb1,Ox1),Slice(Tb1,Hc1))* Leq3(V,Tb1,W) AlwaysIntConn(V,W,HPlace(Ox1))* -> .
	Given clause: 86[0:Res:80.5,59.0] || P(Slice(U,HPlace(Ox1)),Slice(U,Hc1))*+ Continuous(U,Tb1,HPlace(Ox1)) AlwaysIntConn(U,Tb1,HPlace(Ox1)) NoExitCavity(U,Tb1,Hc1,V)* -> Lt(skf5(U,Tb1,W,X),Tb1)*.
	Given clause: 199[0:SpL:7.0,86.0] || P(Slice(Ta1,HPlace(Ox1)),Rc1)+ Continuous(Ta1,Tb1,HPlace(Ox1)) AlwaysIntConn(Ta1,Tb1,HPlace(Ox1)) NoExitCavity(Ta1,Tb1,Hc1,U)* -> Lt(skf5(Ta1,Tb1,V,W),Tb1)*.
	Given clause: 204[0:MRR:203.1,6.0] Object(Ox1) || Continuous(Ta1,Tb1,HPlace(Ox1)) AlwaysIntConn(Ta1,Tb1,HPlace(Ox1)) NoExitCavity(Ta1,Tb1,Hc1,U)* -> Lt(skf5(Ta1,Tb1,V,W),Tb1)*.
	Given clause: 205[0:SoR:204.0,4.1] RigidObject(Ox1) || Continuous(Ta1,Tb1,HPlace(Ox1)) AlwaysIntConn(Ta1,Tb1,HPlace(Ox1)) NoExitCavity(Ta1,Tb1,Hc1,U)* -> Lt(skf5(Ta1,Tb1,V,W),Tb1)*.
	Given clause: 198[0:SoR:178.0,4.1] RigidObject(Ox1) || Cavity(Slice(Tb1,Hc1),U) DR(Place(Tb1,Ox1),U)* O(Place(Tb1,Ox1),Slice(Tb1,Hc1))* Leq3(V,Tb1,W) AlwaysIntConn(V,W,HPlace(Ox1))* -> .
	Given clause: 85[0:Res:81.5,59.0] || P(Slice(U,HPlace(Ox1)),Slice(U,Hc1))*+ Continuous(U,Tb1,HPlace(Ox1)) AlwaysIntConn(U,Tb1,HPlace(Ox1)) NoExitCavity(U,Tb1,Hc1,V)* -> Lt(U,skf5(U,W,X,Y))*.
	Given clause: 206[0:SpL:7.0,85.0] || P(Slice(Ta1,HPlace(Ox1)),Rc1)+ Continuous(Ta1,Tb1,HPlace(Ox1)) AlwaysIntConn(Ta1,Tb1,HPlace(Ox1)) NoExitCavity(Ta1,Tb1,Hc1,U)* -> Lt(Ta1,skf5(Ta1,V,W,X))*.
	Given clause: 211[0:MRR:210.1,6.0] Object(Ox1) || Continuous(Ta1,Tb1,HPlace(Ox1)) AlwaysIntConn(Ta1,Tb1,HPlace(Ox1)) NoExitCavity(Ta1,Tb1,Hc1,U)* -> Lt(Ta1,skf5(Ta1,V,W,X))*.
	Given clause: 212[0:SoR:211.0,4.1] RigidObject(Ox1) || Continuous(Ta1,Tb1,HPlace(Ox1)) AlwaysIntConn(Ta1,Tb1,HPlace(Ox1)) NoExitCavity(Ta1,Tb1,Hc1,U)* -> Lt(Ta1,skf5(Ta1,V,W,X))*.
	Given clause: 201[0:MRR:200.1,124.1] Object(Ox1) || P(Place(U,Ox1),Slice(U,Hc1))* Continuous(U,Tb1,HPlace(Ox1)) AlwaysIntConn(U,Tb1,HPlace(Ox1)) NoExitCavity(U,Tb1,Hc1,V)* -> Lt(skf5(U,Tb1,W,X),Tb1)*.
	Given clause: 171[0:SpL:7.0,81.0] || P(Rc1,Slice(Ta1,U))+ Continuous(Ta1,V,Hc1) AlwaysIntConn(Ta1,V,Hc1) NoExitCavity(Ta1,V,U,W)* -> Lt(Ta1,skf5(Ta1,X,Y,Z))* P(Slice(V,Hc1),Slice(V,U))*.
	Given clause: 214[2:Spt:171.4] ||  -> Lt(Ta1,skf5(Ta1,U,V,W))*.
	Given clause: 216[2:Res:214.0,9.0] ||  -> Time(skf5(Ta1,U,V,W))*.
	Given clause: 213[0:SoR:201.0,4.1] RigidObject(Ox1) || P(Place(U,Ox1),Slice(U,Hc1))* Continuous(U,Tb1,HPlace(Ox1)) AlwaysIntConn(U,Tb1,HPlace(Ox1)) NoExitCavity(U,Tb1,Hc1,V)* -> Lt(skf5(U,Tb1,W,X),Tb1)*.
	Given clause: 208[0:MRR:207.1,124.1] Object(Ox1) || P(Place(U,Ox1),Slice(U,Hc1))* Continuous(U,Tb1,HPlace(Ox1)) AlwaysIntConn(U,Tb1,HPlace(Ox1)) NoExitCavity(U,Tb1,Hc1,V)* -> Lt(U,skf5(U,W,X,Y))*.
	Given clause: 217[0:SoR:208.0,4.1] RigidObject(Ox1) || P(Place(U,Ox1),Slice(U,Hc1))* Continuous(U,Tb1,HPlace(Ox1)) AlwaysIntConn(U,Tb1,HPlace(Ox1)) NoExitCavity(U,Tb1,Hc1,V)* -> Lt(U,skf5(U,W,X,Y))*.
	Given clause: 161[0:SpL:7.0,80.0] || P(Rc1,Slice(Ta1,U))+ Continuous(Ta1,V,Hc1) AlwaysIntConn(Ta1,V,Hc1) NoExitCavity(Ta1,V,U,W)* -> P(Slice(V,Hc1),Slice(V,U))* Lt(skf5(Ta1,V,X,Y),V)*.
	Given clause: 218[0:SpL:7.0,161.0] || P(Rc1,Rc1) Continuous(Ta1,U,Hc1) AlwaysIntConn(Ta1,U,Hc1) NoExitCavity(Ta1,U,Hc1,V)*+ -> P(Slice(U,Hc1),Slice(U,Hc1))* Lt(skf5(Ta1,U,W,X),U)*.
	Given clause: 221[0:Res:20.0,218.3] || P(Rc1,Rc1) Continuous(Ta1,Tb1,Hc1)+ AlwaysIntConn(Ta1,Tb1,Hc1) -> P(Slice(Tb1,Hc1),Slice(Tb1,Hc1))* Lt(skf5(Ta1,Tb1,U,V),Tb1)*.
	Given clause: 222[3:Spt:221.4] ||  -> Lt(skf5(Ta1,Tb1,U,V),Tb1)*.
	Given clause: 159[0:SpL:7.0,80.0] || P(Slice(Ta1,U),Rc1)+ Continuous(Ta1,V,U) AlwaysIntConn(Ta1,V,U) NoExitCavity(Ta1,V,Hc1,W)* -> P(Slice(V,U),Slice(V,Hc1))* Lt(skf5(Ta1,V,X,Y),V)*.
	Given clause: 186[1:MRR:182.1,94.1] Region(Slice(Tb1,HPlace(Ox1))) || Cavity(Slice(Tb1,Hc1),U) Leq3(V,Tb1,W) AlwaysIntConn(V,W,HPlace(Ox1))* -> O(Slice(Tb1,HPlace(Ox1)),U)* Cavity(Slice(Tb1,HPlace(Ox1)),Slice(Tb1,Hc1))*.
	Given clause: 163[0:MRR:160.1,124.1] Object(U) || P(Slice(V,W),Place(V,U))*+ Continuous(V,X,W) AlwaysIntConn(V,X,W)* NoExitCavity(V,X,HPlace(U),Y)* -> P(Slice(X,W),Slice(X,HPlace(U)))* Lt(skf5(V,X,Z,X1),X)*.
	Given clause: 230[1:MRR:229.0,72.2] || Cavity(Slice(Tb1,Hc1),U)+ Leq3(V,Tb1,W) AlwaysIntConn(V,W,HPlace(Ox1))* -> O(Slice(Tb1,HPlace(Ox1)),U)* Cavity(Slice(Tb1,HPlace(Ox1)),Slice(Tb1,Hc1))*.
	Given clause: 234[4:Spt:230.0,230.3] || Cavity(Slice(Tb1,Hc1),U) -> O(Slice(Tb1,HPlace(Ox1)),U)*.
	Given clause: 238[4:Res:234.1,97.0] || Cavity(Slice(Tb1,Hc1),U)* -> Region(Slice(Tb1,HPlace(Ox1))).
	Given clause: 236[4:Res:234.1,108.1] || Cavity(Slice(Tb1,Hc1),U) Cavity(Slice(Tb1,HPlace(Ox1)),U)* -> .
	Given clause: 240[4:SSi:235.1,89.0] Object(Ox1) || Cavity(Slice(Tb1,Hc1),U) -> O(Place(Tb1,Ox1),U)*.
	Given clause: 173[0:MRR:170.1,124.1] Object(U) || P(Slice(V,W),Place(V,U))*+ Continuous(V,X,W) AlwaysIntConn(V,X,W)* NoExitCavity(V,X,HPlace(U),Y)* -> Lt(V,skf5(V,Z,X1,X2))* P(Slice(X,W),Slice(X,HPlace(U)))*.
	Given clause: 243[4:SoR:240.0,4.1] RigidObject(Ox1) || Cavity(Slice(Tb1,Hc1),U) -> O(Place(Tb1,Ox1),U)*.
	Given clause: 242[4:SSi:241.1,89.0] Object(Ox1) || Cavity(Slice(Tb1,Hc1),U)* Cavity(Place(Tb1,Ox1),U) -> .
	Given clause: 247[4:SoR:242.0,4.1] RigidObject(Ox1) || Cavity(Slice(Tb1,Hc1),U)* Cavity(Place(Tb1,Ox1),U) -> .
	Given clause: 239[4:Res:234.1,165.2] || Cavity(Slice(Tb1,Hc1),Slice(Tb1,Hc1))*+ Cavity(Slice(Tb1,Hc1),U) DR(Slice(Tb1,HPlace(Ox1)),U)* Leq3(V,Tb1,W) AlwaysIntConn(V,W,HPlace(Ox1))* -> .
	Given clause: 193[0:SpL:7.0,82.0] || P(Rc1,Slice(Ta1,U))+ Continuous(Ta1,V,Hc1) AlwaysIntConn(Ta1,V,Hc1) NoExitCavity(Ta1,V,U,W)* -> P(Slice(V,Hc1),Slice(V,U))* O(Slice(skf5(Ta1,V,W,Hc1),Hc1),Slice(skf5(Ta1,V,W,Hc1),W))*.
	Given clause: 220[0:SSi:219.1,90.0] Object(U) || P(Rc1,Place(Ta1,U)) Continuous(Ta1,V,Hc1) AlwaysIntConn(Ta1,V,Hc1) NoExitCavity(Ta1,V,HPlace(U),W)*+ -> P(Slice(V,Hc1),Slice(V,HPlace(U)))* Lt(skf5(Ta1,V,X,Y),V)*.
	Given clause: 248[0:SpL:7.0,193.0] || P(Rc1,Rc1) Continuous(Ta1,U,Hc1) AlwaysIntConn(Ta1,U,Hc1) NoExitCavity(Ta1,U,Hc1,V) -> P(Slice(U,Hc1),Slice(U,Hc1)) O(Slice(skf5(Ta1,U,V,Hc1),Hc1),Slice(skf5(Ta1,U,V,Hc1),V))*.
	Given clause: 254[0:Res:248.5,97.0] || P(Rc1,Rc1) Continuous(Ta1,U,Hc1) AlwaysIntConn(Ta1,U,Hc1) NoExitCavity(Ta1,U,Hc1,V)+ -> P(Slice(U,Hc1),Slice(U,Hc1))* Region(Slice(skf5(Ta1,U,V,Hc1),Hc1))*.
	Given clause: 256[0:Res:20.0,254.3] || P(Rc1,Rc1) Continuous(Ta1,Tb1,Hc1) AlwaysIntConn(Ta1,Tb1,Hc1) -> P(Slice(Tb1,Hc1),Slice(Tb1,Hc1)) Region(Slice(skf5(Ta1,Tb1,HPlace(Ob1),Hc1),Hc1))*.
	Given clause: 191[0:SpL:7.0,82.0] || P(Slice(Ta1,U),Rc1) Continuous(Ta1,V,U) AlwaysIntConn(Ta1,V,U) NoExitCavity(Ta1,V,Hc1,W) -> P(Slice(V,U),Slice(V,Hc1)) O(Slice(skf5(Ta1,V,W,U),U),Slice(skf5(Ta1,V,W,U),W))*.
	Given clause: 253[0:Res:248.5,98.0] || P(Rc1,Rc1) Continuous(Ta1,U,Hc1) AlwaysIntConn(Ta1,U,Hc1) NoExitCavity(Ta1,U,Hc1,V)+ -> P(Slice(U,Hc1),Slice(U,Hc1))* Region(Slice(skf5(Ta1,U,V,Hc1),V))*.
	Given clause: 264[0:Res:20.0,253.3] || P(Rc1,Rc1) Continuous(Ta1,Tb1,Hc1) AlwaysIntConn(Ta1,Tb1,Hc1) -> P(Slice(Tb1,Hc1),Slice(Tb1,Hc1)) Region(Slice(skf5(Ta1,Tb1,HPlace(Ob1),Hc1),HPlace(Ob1)))*.
	Given clause: 261[0:Res:191.5,97.0] || P(Slice(Ta1,U),Rc1)+ Continuous(Ta1,V,U) AlwaysIntConn(Ta1,V,U) NoExitCavity(Ta1,V,Hc1,W) -> P(Slice(V,U),Slice(V,Hc1))* Region(Slice(skf5(Ta1,V,W,U),U))*.
	Given clause: 260[0:Res:191.5,98.0] || P(Slice(Ta1,U),Rc1)+ Continuous(Ta1,V,U) AlwaysIntConn(Ta1,V,U) NoExitCavity(Ta1,V,Hc1,W) -> P(Slice(V,U),Slice(V,Hc1))* Region(Slice(skf5(Ta1,V,W,U),W))*.
	Given clause: 164[0:MRR:162.1,124.1] Object(U) || P(Place(V,U),Slice(V,W))*+ Continuous(V,X,HPlace(U)) AlwaysIntConn(V,X,HPlace(U))* NoExitCavity(V,X,W,Y)* -> P(Slice(X,HPlace(U)),Slice(X,W))* Lt(skf5(V,X,Z,X1),X)*.
	Given clause: 227[0:SSi:226.1,90.0] Object(U) || P(Place(Ta1,U),Rc1)+ Continuous(Ta1,V,HPlace(U)) AlwaysIntConn(Ta1,V,HPlace(U)) NoExitCavity(Ta1,V,Hc1,W)* -> P(Slice(V,HPlace(U)),Slice(V,Hc1))* Lt(skf5(Ta1,V,X,Y),V)*.
	Given clause: 274[0:Res:6.0,227.1] Object(Ox1) || Continuous(Ta1,U,HPlace(Ox1)) AlwaysIntConn(Ta1,U,HPlace(Ox1)) NoExitCavity(Ta1,U,Hc1,V)* -> P(Slice(U,HPlace(Ox1)),Slice(U,Hc1))* Lt(skf5(Ta1,U,W,X),U)*.
	Given clause: 275[0:SoR:274.0,4.1] RigidObject(Ox1) || Continuous(Ta1,U,HPlace(Ox1)) AlwaysIntConn(Ta1,U,HPlace(Ox1)) NoExitCavity(Ta1,U,Hc1,V)* -> P(Slice(U,HPlace(Ox1)),Slice(U,Hc1))* Lt(skf5(Ta1,U,W,X),U)*.
	Given clause: 252[0:Res:248.5,108.1] || P(Rc1,Rc1) Continuous(Ta1,U,Hc1) AlwaysIntConn(Ta1,U,Hc1) NoExitCavity(Ta1,U,Hc1,V) Cavity(Slice(skf5(Ta1,U,V,Hc1),Hc1),Slice(skf5(Ta1,U,V,Hc1),V))* -> P(Slice(U,Hc1),Slice(U,Hc1)).
	Given clause: 174[0:MRR:172.1,124.1] Object(U) || P(Place(V,U),Slice(V,W))*+ Continuous(V,X,HPlace(U)) AlwaysIntConn(V,X,HPlace(U))* NoExitCavity(V,X,W,Y)* -> Lt(V,skf5(V,Z,X1,X2))* P(Slice(X,HPlace(U)),Slice(X,W))*.
	Given clause: 271[0:SSi:270.1,90.0] Object(U) || P(Place(Ta1,U),Rc1)+ Continuous(Ta1,V,HPlace(U)) AlwaysIntConn(Ta1,V,HPlace(U)) NoExitCavity(Ta1,V,Hc1,W) -> P(Slice(V,HPlace(U)),Slice(V,Hc1))* Region(Slice(skf5(Ta1,V,W,HPlace(U)),W))*.
	Given clause: 280[0:Res:6.0,271.1] Object(Ox1) || Continuous(Ta1,U,HPlace(Ox1)) AlwaysIntConn(Ta1,U,HPlace(Ox1)) NoExitCavity(Ta1,U,Hc1,V) -> P(Slice(U,HPlace(Ox1)),Slice(U,Hc1))* Region(Slice(skf5(Ta1,U,V,HPlace(Ox1)),V))*.
	Given clause: 281[0:SoR:280.0,4.1] RigidObject(Ox1) || Continuous(Ta1,U,HPlace(Ox1)) AlwaysIntConn(Ta1,U,HPlace(Ox1)) NoExitCavity(Ta1,U,Hc1,V) -> P(Slice(U,HPlace(Ox1)),Slice(U,Hc1))* Region(Slice(skf5(Ta1,U,V,HPlace(Ox1)),V))*.
	Given clause: 268[0:SSi:267.1,90.0] Object(U) || P(Place(Ta1,U),Rc1)+ Continuous(Ta1,V,HPlace(U)) AlwaysIntConn(Ta1,V,HPlace(U)) NoExitCavity(Ta1,V,Hc1,W) -> P(Slice(V,HPlace(U)),Slice(V,Hc1))* Region(Slice(skf5(Ta1,V,W,HPlace(U)),HPlace(U)))*.
	Given clause: 195[0:MRR:192.1,124.1] Object(U) || P(Slice(V,W),Place(V,U))*+ Continuous(V,X,W) AlwaysIntConn(V,X,W) NoExitCavity(V,X,HPlace(U),Y)* -> P(Slice(X,W),Slice(X,HPlace(U)))* O(Slice(skf5(V,X,Y,W),W),Slice(skf5(V,X,Y,W),Y))*.
	Given clause: 282[0:Res:6.0,268.1] Object(Ox1) || Continuous(Ta1,U,HPlace(Ox1)) AlwaysIntConn(Ta1,U,HPlace(Ox1)) NoExitCavity(Ta1,U,Hc1,V) -> P(Slice(U,HPlace(Ox1)),Slice(U,Hc1))* Region(Slice(skf5(Ta1,U,V,HPlace(Ox1)),HPlace(Ox1)))*.
	Given clause: 286[0:SoR:282.0,4.1] RigidObject(Ox1) || Continuous(Ta1,U,HPlace(Ox1)) AlwaysIntConn(Ta1,U,HPlace(Ox1)) NoExitCavity(Ta1,U,Hc1,V) -> P(Slice(U,HPlace(Ox1)),Slice(U,Hc1))* Region(Slice(skf5(Ta1,U,V,HPlace(Ox1)),HPlace(Ox1)))*.
	Given clause: 259[0:Res:191.5,108.1] || P(Slice(Ta1,U),Rc1) Continuous(Ta1,V,U) AlwaysIntConn(Ta1,V,U) NoExitCavity(Ta1,V,Hc1,W) Cavity(Slice(skf5(Ta1,V,W,U),U),Slice(skf5(Ta1,V,W,U),W))* -> P(Slice(V,U),Slice(V,Hc1)).
	Given clause: 255[2:SSi:251.1,216.0,19.1,130.0] Object(U) || P(Rc1,Rc1) Continuous(Ta1,V,Hc1) AlwaysIntConn(Ta1,V,Hc1) NoExitCavity(Ta1,V,Hc1,HPlace(U)) -> P(Slice(V,Hc1),Slice(V,Hc1)) O(Slice(skf5(Ta1,V,HPlace(U),Hc1),Hc1),Place(skf5(Ta1,V,HPlace(U),Hc1),U))*.
	Given clause: 196[0:MRR:194.1,124.1] Object(U) || P(Place(V,U),Slice(V,W))*+ Continuous(V,X,HPlace(U)) AlwaysIntConn(V,X,HPlace(U)) NoExitCavity(V,X,W,Y)* -> P(Slice(X,HPlace(U)),Slice(X,W))* O(Slice(skf5(V,X,Y,HPlace(U)),HPlace(U)),Slice(skf5(V,X,Y,HPlace(U)),Y))*.
	Given clause: 292[2:Res:255.6,98.0] Object(U) || P(Rc1,Rc1) Continuous(Ta1,V,Hc1) AlwaysIntConn(Ta1,V,Hc1) NoExitCavity(Ta1,V,Hc1,HPlace(U))+ -> P(Slice(V,Hc1),Slice(V,Hc1))* Region(Place(skf5(Ta1,V,HPlace(U),Hc1),U))*.
	Given clause: 296[2:Res:20.0,292.4] Object(Ob1) || P(Rc1,Rc1) Continuous(Ta1,Tb1,Hc1) AlwaysIntConn(Ta1,Tb1,Hc1) -> P(Slice(Tb1,Hc1),Slice(Tb1,Hc1)) Region(Place(skf5(Ta1,Tb1,HPlace(Ob1),Hc1),Ob1))*.
	Given clause: 297[2:SoR:296.0,4.1] RigidObject(Ob1) || P(Rc1,Rc1) Continuous(Ta1,Tb1,Hc1) AlwaysIntConn(Ta1,Tb1,Hc1) -> P(Slice(Tb1,Hc1),Slice(Tb1,Hc1)) Region(Place(skf5(Ta1,Tb1,HPlace(Ob1),Hc1),Ob1))*.
	Given clause: 277[2:SSi:276.1,216.0,19.1,130.0] Object(U) || P(Rc1,Rc1) Continuous(Ta1,V,Hc1) AlwaysIntConn(Ta1,V,Hc1) NoExitCavity(Ta1,V,Hc1,HPlace(U)) Cavity(Slice(skf5(Ta1,V,HPlace(U),Hc1),Hc1),Place(skf5(Ta1,V,HPlace(U),Hc1),U))* -> P(Slice(V,Hc1),Slice(V,Hc1)).
	Given clause: 250[0:SSi:249.1,90.0] Object(U) || P(Rc1,Place(Ta1,U)) Continuous(Ta1,V,Hc1) AlwaysIntConn(Ta1,V,Hc1) NoExitCavity(Ta1,V,HPlace(U),W)*+ -> P(Slice(V,Hc1),Slice(V,HPlace(U)))* O(Slice(skf5(Ta1,V,W,Hc1),Hc1),Slice(skf5(Ta1,V,W,Hc1),W))*.
	Given clause: 233[0:MRR:232.1,124.1] Object(U) Object(V) || P(Place(W,U),Place(W,V))*+ Continuous(W,X,HPlace(U)) AlwaysIntConn(W,X,HPlace(U))* NoExitCavity(W,X,HPlace(V),Y)* -> P(Slice(X,HPlace(U)),Slice(X,HPlace(V)))* Lt(skf5(W,X,Z,X1),X)*.
	Given clause: 246[0:MRR:245.1,124.1] Object(U) Object(V) || P(Place(W,U),Place(W,V))*+ Continuous(W,X,HPlace(U)) AlwaysIntConn(W,X,HPlace(U))* NoExitCavity(W,X,HPlace(V),Y)* -> Lt(W,skf5(W,Z,X1,X2))* P(Slice(X,HPlace(U)),Slice(X,HPlace(V)))*.
	Given clause: 262[2:SSi:257.1,216.1,19.0] Object(U) || P(Slice(Ta1,V),Rc1) Continuous(Ta1,W,V) AlwaysIntConn(Ta1,W,V) NoExitCavity(Ta1,W,Hc1,HPlace(U)) -> P(Slice(W,V),Slice(W,Hc1)) O(Slice(skf5(Ta1,W,HPlace(U),V),V),Place(skf5(Ta1,W,HPlace(U),V),U))*.
	Given clause: 300[2:Res:262.6,98.0] Object(U) || P(Slice(Ta1,V),Rc1) Continuous(Ta1,W,V) AlwaysIntConn(Ta1,W,V) NoExitCavity(Ta1,W,Hc1,HPlace(U))+ -> P(Slice(W,V),Slice(W,Hc1))* Region(Place(skf5(Ta1,W,HPlace(U),V),U))*.
	Given clause: 263[2:SSi:258.1,216.1,19.0] Object(U) || P(Slice(Ta1,HPlace(U)),Rc1) Continuous(Ta1,V,HPlace(U)) AlwaysIntConn(Ta1,V,HPlace(U)) NoExitCavity(Ta1,V,Hc1,W) -> P(Slice(V,HPlace(U)),Slice(V,Hc1)) O(Place(skf5(Ta1,V,W,HPlace(U)),U),Slice(skf5(Ta1,V,W,HPlace(U)),W))*.
	Given clause: 303[2:Res:20.0,300.4] Object(Ob1) || P(Slice(Ta1,U),Rc1) Continuous(Ta1,Tb1,U) AlwaysIntConn(Ta1,Tb1,U) -> P(Slice(Tb1,U),Slice(Tb1,Hc1)) Region(Place(skf5(Ta1,Tb1,HPlace(Ob1),U),Ob1))*.
	Given clause: 308[2:SoR:303.0,4.1] RigidObject(Ob1) || P(Slice(Ta1,U),Rc1) Continuous(Ta1,Tb1,U) AlwaysIntConn(Ta1,Tb1,U) -> P(Slice(Tb1,U),Slice(Tb1,Hc1)) Region(Place(skf5(Ta1,Tb1,HPlace(Ob1),U),Ob1))*.
	Given clause: 307[2:Res:263.6,97.0] Object(U) || P(Slice(Ta1,HPlace(U)),Rc1)+ Continuous(Ta1,V,HPlace(U)) AlwaysIntConn(Ta1,V,HPlace(U)) NoExitCavity(Ta1,V,Hc1,W) -> P(Slice(V,HPlace(U)),Slice(V,Hc1))* Region(Place(skf5(Ta1,V,W,HPlace(U)),U))*.
	Given clause: 311[2:SSi:310.0,90.0] Object(U) || P(Place(Ta1,U),Rc1)+ Continuous(Ta1,V,HPlace(U)) AlwaysIntConn(Ta1,V,HPlace(U)) NoExitCavity(Ta1,V,Hc1,W) -> P(Slice(V,HPlace(U)),Slice(V,Hc1))* Region(Place(skf5(Ta1,V,W,HPlace(U)),U))*.
	Given clause: 294[0:SpL:7.0,196.1] Object(U) || P(Place(Ta1,U),Rc1) Continuous(Ta1,V,HPlace(U)) AlwaysIntConn(Ta1,V,HPlace(U)) NoExitCavity(Ta1,V,Hc1,W) -> P(Slice(V,HPlace(U)),Slice(V,Hc1)) O(Slice(skf5(Ta1,V,W,HPlace(U)),HPlace(U)),Slice(skf5(Ta1,V,W,HPlace(U)),W))*.
	Given clause: 312[2:Res:6.0,311.1] Object(Ox1) || Continuous(Ta1,U,HPlace(Ox1)) AlwaysIntConn(Ta1,U,HPlace(Ox1)) NoExitCavity(Ta1,U,Hc1,V) -> P(Slice(U,HPlace(Ox1)),Slice(U,Hc1))* Region(Place(skf5(Ta1,U,V,HPlace(Ox1)),Ox1))*.
	Given clause: 322[2:SoR:312.0,4.1] RigidObject(Ox1) || Continuous(Ta1,U,HPlace(Ox1)) AlwaysIntConn(Ta1,U,HPlace(Ox1)) NoExitCavity(Ta1,U,Hc1,V) -> P(Slice(U,HPlace(Ox1)),Slice(U,Hc1))* Region(Place(skf5(Ta1,U,V,HPlace(Ox1)),Ox1))*.
	Given clause: 289[2:SSi:287.1,216.1,19.0] Object(U) || P(Slice(Ta1,V),Rc1) Continuous(Ta1,W,V) AlwaysIntConn(Ta1,W,V) NoExitCavity(Ta1,W,Hc1,HPlace(U)) Cavity(Slice(skf5(Ta1,W,HPlace(U),V),V),Place(skf5(Ta1,W,HPlace(U),V),U))* -> P(Slice(W,V),Slice(W,Hc1)).
	Given clause: 319[2:SSi:318.0,216.1,19.0] Object(U) || P(Place(Ta1,U),Rc1) Continuous(Ta1,V,HPlace(U)) AlwaysIntConn(Ta1,V,HPlace(U)) NoExitCavity(Ta1,V,Hc1,W) -> P(Slice(V,HPlace(U)),Slice(V,Hc1)) O(Place(skf5(Ta1,V,W,HPlace(U)),U),Slice(skf5(Ta1,V,W,HPlace(U)),W))*.
	Given clause: 285[0:MRR:284.1,124.1] Object(U) Object(V) || P(Place(W,U),Place(W,V))*+ Continuous(W,X,HPlace(U)) AlwaysIntConn(W,X,HPlace(U)) NoExitCavity(W,X,HPlace(V),Y)* -> P(Slice(X,HPlace(U)),Slice(X,HPlace(V)))* O(Slice(skf5(W,X,Y,HPlace(U)),HPlace(U)),Slice(skf5(W,X,Y,HPlace(U)),Y))*.
	Given clause: 326[2:Res:319.6,108.1] Object(U) || P(Place(Ta1,U),Rc1) Continuous(Ta1,V,HPlace(U)) AlwaysIntConn(Ta1,V,HPlace(U)) NoExitCavity(Ta1,V,Hc1,W) Cavity(Place(skf5(Ta1,V,W,HPlace(U)),U),Slice(skf5(Ta1,V,W,HPlace(U)),W))* -> P(Slice(V,HPlace(U)),Slice(V,Hc1)).
	Given clause: 290[2:SSi:288.1,216.1,19.0] Object(U) || P(Slice(Ta1,HPlace(U)),Rc1) Continuous(Ta1,V,HPlace(U)) AlwaysIntConn(Ta1,V,HPlace(U)) NoExitCavity(Ta1,V,Hc1,W) Cavity(Place(skf5(Ta1,V,W,HPlace(U)),U),Slice(skf5(Ta1,V,W,HPlace(U)),W))* -> P(Slice(V,HPlace(U)),Slice(V,Hc1)).
	Given clause: 315[0:Res:294.6,108.1] Object(U) || P(Place(Ta1,U),Rc1) Continuous(Ta1,V,HPlace(U)) AlwaysIntConn(Ta1,V,HPlace(U)) NoExitCavity(Ta1,V,Hc1,W) Cavity(Slice(skf5(Ta1,V,W,HPlace(U)),HPlace(U)),Slice(skf5(Ta1,V,W,HPlace(U)),W))* -> P(Slice(V,HPlace(U)),Slice(V,Hc1)).
	Given clause: 321[2:SSi:320.1,216.1,19.1,19.0] Object(U) Object(V) || P(Place(Ta1,V),Rc1) Continuous(Ta1,W,HPlace(V)) AlwaysIntConn(Ta1,W,HPlace(V)) NoExitCavity(Ta1,W,Hc1,HPlace(U)) -> P(Slice(W,HPlace(V)),Slice(W,Hc1)) O(Place(skf5(Ta1,W,HPlace(U),HPlace(V)),V),Place(skf5(Ta1,W,HPlace(U),HPlace(V)),U))*.
	Given clause: 302[2:SSi:298.1,216.1,19.1,19.0] Object(U) Object(V) || P(Slice(Ta1,HPlace(U)),Rc1) Continuous(Ta1,W,HPlace(U)) AlwaysIntConn(Ta1,W,HPlace(U)) NoExitCavity(Ta1,W,Hc1,HPlace(V)) -> P(Slice(W,HPlace(U)),Slice(W,Hc1)) O(Place(skf5(Ta1,W,HPlace(V),HPlace(U)),U),Place(skf5(Ta1,W,HPlace(V),HPlace(U)),V))*.
	Given clause: 341[2:SSi:340.0,216.1,19.1,19.0] Object(U) Object(V) || P(Place(Ta1,V),Rc1) Continuous(Ta1,W,HPlace(V)) AlwaysIntConn(Ta1,W,HPlace(V)) NoExitCavity(Ta1,W,Hc1,HPlace(U))*+ -> P(Slice(W,HPlace(V)),Slice(W,Hc1))* equal(V,U)*.
	Given clause: 348[2:Res:20.0,341.5] Object(Ob1) Object(U) || P(Place(Ta1,U),Rc1) Continuous(Ta1,Tb1,HPlace(U)) AlwaysIntConn(Ta1,Tb1,HPlace(U)) -> P(Slice(Tb1,HPlace(U)),Slice(Tb1,Hc1))* equal(U,Ob1).
	Given clause: 349[2:SoR:348.0,4.1] Object(U) RigidObject(Ob1) || P(Place(Ta1,U),Rc1) Continuous(Ta1,Tb1,HPlace(U)) AlwaysIntConn(Ta1,Tb1,HPlace(U)) -> P(Slice(Tb1,HPlace(U)),Slice(Tb1,Hc1))* equal(U,Ob1).
	Given clause: 347[2:SSi:346.0,216.1,19.1,19.0] Object(U) Object(V) || P(Slice(Ta1,HPlace(V)),Rc1)+ Continuous(Ta1,W,HPlace(V)) AlwaysIntConn(Ta1,W,HPlace(V)) NoExitCavity(Ta1,W,Hc1,HPlace(U))* -> P(Slice(W,HPlace(V)),Slice(W,Hc1))* equal(V,U)*.
	Given clause: 337[2:Res:321.7,98.0] Object(U) Object(V) || P(Place(Ta1,V),Rc1) Continuous(Ta1,W,HPlace(V)) AlwaysIntConn(Ta1,W,HPlace(V)) NoExitCavity(Ta1,W,Hc1,HPlace(U))+ -> P(Slice(W,HPlace(V)),Slice(W,Hc1))* Region(Place(skf5(Ta1,W,HPlace(U),HPlace(V)),U))*.
	Given clause: 352[2:Res:20.0,337.5] Object(Ob1) Object(U) || P(Place(Ta1,U),Rc1) Continuous(Ta1,Tb1,HPlace(U)) AlwaysIntConn(Ta1,Tb1,HPlace(U)) -> P(Slice(Tb1,HPlace(U)),Slice(Tb1,Hc1)) Region(Place(skf5(Ta1,Tb1,HPlace(Ob1),HPlace(U)),Ob1))*.
	Given clause: 353[2:SoR:352.0,4.1] Object(U) RigidObject(Ob1) || P(Place(Ta1,U),Rc1) Continuous(Ta1,Tb1,HPlace(U)) AlwaysIntConn(Ta1,Tb1,HPlace(U)) -> P(Slice(Tb1,HPlace(U)),Slice(Tb1,Hc1)) Region(Place(skf5(Ta1,Tb1,HPlace(Ob1),HPlace(U)),Ob1))*.
	Given clause: 330[2:SSi:329.1,216.1,19.1,19.0] Object(U) Object(V) || P(Place(Ta1,V),Rc1) Continuous(Ta1,W,HPlace(V)) AlwaysIntConn(Ta1,W,HPlace(V)) NoExitCavity(Ta1,W,Hc1,HPlace(U)) Cavity(Place(skf5(Ta1,W,HPlace(U),HPlace(V)),V),Place(skf5(Ta1,W,HPlace(U),HPlace(V)),U))* -> P(Slice(W,HPlace(V)),Slice(W,Hc1)).
	Given clause: 324[2:SSi:323.1,216.1,19.1,19.0] Object(U) Object(V) || P(Slice(Ta1,HPlace(U)),Rc1) Continuous(Ta1,W,HPlace(U)) AlwaysIntConn(Ta1,W,HPlace(U)) NoExitCavity(Ta1,W,Hc1,HPlace(V)) Cavity(Place(skf5(Ta1,W,HPlace(V),HPlace(U)),U),Place(skf5(Ta1,W,HPlace(V),HPlace(U)),V))* -> P(Slice(W,HPlace(U)),Slice(W,Hc1)).
SPASS V 3.7 
SPASS beiseite: Completion found.
Problem: Scenario1_Part3.txt 
SPASS derived 210 clauses, backtracked 0 clauses, performed 4 splits and kept 228 clauses.
SPASS allocated 52727 KBytes.
SPASS spent	0:00:00.06 on the problem.
		0:00:00.01 for the input.
		0:00:00.01 for the FLOTTER CNF translation.
		0:00:00.00 for inferences.
		0:00:00.00 for the backtracking.
		0:00:00.01 for the reduction.


 The saturated set of worked-off clauses is :
324[2:SSi:323.1,216.1,19.1,19.0] Object(U) Object(V) || P(Slice(Ta1,HPlace(U)),Rc1) Continuous(Ta1,W,HPlace(U)) AlwaysIntConn(Ta1,W,HPlace(U)) NoExitCavity(Ta1,W,Hc1,HPlace(V)) Cavity(Place(skf5(Ta1,W,HPlace(V),HPlace(U)),U),Place(skf5(Ta1,W,HPlace(V),HPlace(U)),V))* -> P(Slice(W,HPlace(U)),Slice(W,Hc1)).
330[2:SSi:329.1,216.1,19.1,19.0] Object(U) Object(V) || P(Place(Ta1,V),Rc1) Continuous(Ta1,W,HPlace(V)) AlwaysIntConn(Ta1,W,HPlace(V)) NoExitCavity(Ta1,W,Hc1,HPlace(U)) Cavity(Place(skf5(Ta1,W,HPlace(U),HPlace(V)),V),Place(skf5(Ta1,W,HPlace(U),HPlace(V)),U))* -> P(Slice(W,HPlace(V)),Slice(W,Hc1)).
353[2:SoR:352.0,4.1] Object(U) RigidObject(Ob1) || P(Place(Ta1,U),Rc1) Continuous(Ta1,Tb1,HPlace(U)) AlwaysIntConn(Ta1,Tb1,HPlace(U)) -> P(Slice(Tb1,HPlace(U)),Slice(Tb1,Hc1)) Region(Place(skf5(Ta1,Tb1,HPlace(Ob1),HPlace(U)),Ob1))*.
352[2:Res:20.0,337.5] Object(Ob1) Object(U) || P(Place(Ta1,U),Rc1) Continuous(Ta1,Tb1,HPlace(U)) AlwaysIntConn(Ta1,Tb1,HPlace(U)) -> P(Slice(Tb1,HPlace(U)),Slice(Tb1,Hc1)) Region(Place(skf5(Ta1,Tb1,HPlace(Ob1),HPlace(U)),Ob1))*.
337[2:Res:321.7,98.0] Object(U) Object(V) || P(Place(Ta1,V),Rc1) Continuous(Ta1,W,HPlace(V)) AlwaysIntConn(Ta1,W,HPlace(V)) NoExitCavity(Ta1,W,Hc1,HPlace(U))+ -> P(Slice(W,HPlace(V)),Slice(W,Hc1))* Region(Place(skf5(Ta1,W,HPlace(U),HPlace(V)),U))*.
347[2:SSi:346.0,216.1,19.1,19.0] Object(U) Object(V) || P(Slice(Ta1,HPlace(V)),Rc1)+ Continuous(Ta1,W,HPlace(V)) AlwaysIntConn(Ta1,W,HPlace(V)) NoExitCavity(Ta1,W,Hc1,HPlace(U))* -> P(Slice(W,HPlace(V)),Slice(W,Hc1))* equal(V,U)*.
349[2:SoR:348.0,4.1] Object(U) RigidObject(Ob1) || P(Place(Ta1,U),Rc1) Continuous(Ta1,Tb1,HPlace(U)) AlwaysIntConn(Ta1,Tb1,HPlace(U)) -> P(Slice(Tb1,HPlace(U)),Slice(Tb1,Hc1))* equal(U,Ob1).
348[2:Res:20.0,341.5] Object(Ob1) Object(U) || P(Place(Ta1,U),Rc1) Continuous(Ta1,Tb1,HPlace(U)) AlwaysIntConn(Ta1,Tb1,HPlace(U)) -> P(Slice(Tb1,HPlace(U)),Slice(Tb1,Hc1))* equal(U,Ob1).
341[2:SSi:340.0,216.1,19.1,19.0] Object(U) Object(V) || P(Place(Ta1,V),Rc1) Continuous(Ta1,W,HPlace(V)) AlwaysIntConn(Ta1,W,HPlace(V)) NoExitCavity(Ta1,W,Hc1,HPlace(U))*+ -> P(Slice(W,HPlace(V)),Slice(W,Hc1))* equal(V,U)*.
302[2:SSi:298.1,216.1,19.1,19.0] Object(U) Object(V) || P(Slice(Ta1,HPlace(U)),Rc1) Continuous(Ta1,W,HPlace(U)) AlwaysIntConn(Ta1,W,HPlace(U)) NoExitCavity(Ta1,W,Hc1,HPlace(V)) -> P(Slice(W,HPlace(U)),Slice(W,Hc1)) O(Place(skf5(Ta1,W,HPlace(V),HPlace(U)),U),Place(skf5(Ta1,W,HPlace(V),HPlace(U)),V))*.
321[2:SSi:320.1,216.1,19.1,19.0] Object(U) Object(V) || P(Place(Ta1,V),Rc1) Continuous(Ta1,W,HPlace(V)) AlwaysIntConn(Ta1,W,HPlace(V)) NoExitCavity(Ta1,W,Hc1,HPlace(U)) -> P(Slice(W,HPlace(V)),Slice(W,Hc1)) O(Place(skf5(Ta1,W,HPlace(U),HPlace(V)),V),Place(skf5(Ta1,W,HPlace(U),HPlace(V)),U))*.
315[0:Res:294.6,108.1] Object(U) || P(Place(Ta1,U),Rc1) Continuous(Ta1,V,HPlace(U)) AlwaysIntConn(Ta1,V,HPlace(U)) NoExitCavity(Ta1,V,Hc1,W) Cavity(Slice(skf5(Ta1,V,W,HPlace(U)),HPlace(U)),Slice(skf5(Ta1,V,W,HPlace(U)),W))* -> P(Slice(V,HPlace(U)),Slice(V,Hc1)).
290[2:SSi:288.1,216.1,19.0] Object(U) || P(Slice(Ta1,HPlace(U)),Rc1) Continuous(Ta1,V,HPlace(U)) AlwaysIntConn(Ta1,V,HPlace(U)) NoExitCavity(Ta1,V,Hc1,W) Cavity(Place(skf5(Ta1,V,W,HPlace(U)),U),Slice(skf5(Ta1,V,W,HPlace(U)),W))* -> P(Slice(V,HPlace(U)),Slice(V,Hc1)).
326[2:Res:319.6,108.1] Object(U) || P(Place(Ta1,U),Rc1) Continuous(Ta1,V,HPlace(U)) AlwaysIntConn(Ta1,V,HPlace(U)) NoExitCavity(Ta1,V,Hc1,W) Cavity(Place(skf5(Ta1,V,W,HPlace(U)),U),Slice(skf5(Ta1,V,W,HPlace(U)),W))* -> P(Slice(V,HPlace(U)),Slice(V,Hc1)).
285[0:MRR:284.1,124.1] Object(U) Object(V) || P(Place(W,U),Place(W,V))*+ Continuous(W,X,HPlace(U)) AlwaysIntConn(W,X,HPlace(U)) NoExitCavity(W,X,HPlace(V),Y)* -> P(Slice(X,HPlace(U)),Slice(X,HPlace(V)))* O(Slice(skf5(W,X,Y,HPlace(U)),HPlace(U)),Slice(skf5(W,X,Y,HPlace(U)),Y))*.
319[2:SSi:318.0,216.1,19.0] Object(U) || P(Place(Ta1,U),Rc1) Continuous(Ta1,V,HPlace(U)) AlwaysIntConn(Ta1,V,HPlace(U)) NoExitCavity(Ta1,V,Hc1,W) -> P(Slice(V,HPlace(U)),Slice(V,Hc1)) O(Place(skf5(Ta1,V,W,HPlace(U)),U),Slice(skf5(Ta1,V,W,HPlace(U)),W))*.
289[2:SSi:287.1,216.1,19.0] Object(U) || P(Slice(Ta1,V),Rc1) Continuous(Ta1,W,V) AlwaysIntConn(Ta1,W,V) NoExitCavity(Ta1,W,Hc1,HPlace(U)) Cavity(Slice(skf5(Ta1,W,HPlace(U),V),V),Place(skf5(Ta1,W,HPlace(U),V),U))* -> P(Slice(W,V),Slice(W,Hc1)).
322[2:SoR:312.0,4.1] RigidObject(Ox1) || Continuous(Ta1,U,HPlace(Ox1)) AlwaysIntConn(Ta1,U,HPlace(Ox1)) NoExitCavity(Ta1,U,Hc1,V) -> P(Slice(U,HPlace(Ox1)),Slice(U,Hc1))* Region(Place(skf5(Ta1,U,V,HPlace(Ox1)),Ox1))*.
312[2:Res:6.0,311.1] Object(Ox1) || Continuous(Ta1,U,HPlace(Ox1)) AlwaysIntConn(Ta1,U,HPlace(Ox1)) NoExitCavity(Ta1,U,Hc1,V) -> P(Slice(U,HPlace(Ox1)),Slice(U,Hc1))* Region(Place(skf5(Ta1,U,V,HPlace(Ox1)),Ox1))*.
294[0:SpL:7.0,196.1] Object(U) || P(Place(Ta1,U),Rc1) Continuous(Ta1,V,HPlace(U)) AlwaysIntConn(Ta1,V,HPlace(U)) NoExitCavity(Ta1,V,Hc1,W) -> P(Slice(V,HPlace(U)),Slice(V,Hc1)) O(Slice(skf5(Ta1,V,W,HPlace(U)),HPlace(U)),Slice(skf5(Ta1,V,W,HPlace(U)),W))*.
311[2:SSi:310.0,90.0] Object(U) || P(Place(Ta1,U),Rc1)+ Continuous(Ta1,V,HPlace(U)) AlwaysIntConn(Ta1,V,HPlace(U)) NoExitCavity(Ta1,V,Hc1,W) -> P(Slice(V,HPlace(U)),Slice(V,Hc1))* Region(Place(skf5(Ta1,V,W,HPlace(U)),U))*.
307[2:Res:263.6,97.0] Object(U) || P(Slice(Ta1,HPlace(U)),Rc1)+ Continuous(Ta1,V,HPlace(U)) AlwaysIntConn(Ta1,V,HPlace(U)) NoExitCavity(Ta1,V,Hc1,W) -> P(Slice(V,HPlace(U)),Slice(V,Hc1))* Region(Place(skf5(Ta1,V,W,HPlace(U)),U))*.
308[2:SoR:303.0,4.1] RigidObject(Ob1) || P(Slice(Ta1,U),Rc1) Continuous(Ta1,Tb1,U) AlwaysIntConn(Ta1,Tb1,U) -> P(Slice(Tb1,U),Slice(Tb1,Hc1)) Region(Place(skf5(Ta1,Tb1,HPlace(Ob1),U),Ob1))*.
303[2:Res:20.0,300.4] Object(Ob1) || P(Slice(Ta1,U),Rc1) Continuous(Ta1,Tb1,U) AlwaysIntConn(Ta1,Tb1,U) -> P(Slice(Tb1,U),Slice(Tb1,Hc1)) Region(Place(skf5(Ta1,Tb1,HPlace(Ob1),U),Ob1))*.
263[2:SSi:258.1,216.1,19.0] Object(U) || P(Slice(Ta1,HPlace(U)),Rc1) Continuous(Ta1,V,HPlace(U)) AlwaysIntConn(Ta1,V,HPlace(U)) NoExitCavity(Ta1,V,Hc1,W) -> P(Slice(V,HPlace(U)),Slice(V,Hc1)) O(Place(skf5(Ta1,V,W,HPlace(U)),U),Slice(skf5(Ta1,V,W,HPlace(U)),W))*.
300[2:Res:262.6,98.0] Object(U) || P(Slice(Ta1,V),Rc1) Continuous(Ta1,W,V) AlwaysIntConn(Ta1,W,V) NoExitCavity(Ta1,W,Hc1,HPlace(U))+ -> P(Slice(W,V),Slice(W,Hc1))* Region(Place(skf5(Ta1,W,HPlace(U),V),U))*.
262[2:SSi:257.1,216.1,19.0] Object(U) || P(Slice(Ta1,V),Rc1) Continuous(Ta1,W,V) AlwaysIntConn(Ta1,W,V) NoExitCavity(Ta1,W,Hc1,HPlace(U)) -> P(Slice(W,V),Slice(W,Hc1)) O(Slice(skf5(Ta1,W,HPlace(U),V),V),Place(skf5(Ta1,W,HPlace(U),V),U))*.
246[0:MRR:245.1,124.1] Object(U) Object(V) || P(Place(W,U),Place(W,V))*+ Continuous(W,X,HPlace(U)) AlwaysIntConn(W,X,HPlace(U))* NoExitCavity(W,X,HPlace(V),Y)* -> Lt(W,skf5(W,Z,X1,X2))* P(Slice(X,HPlace(U)),Slice(X,HPlace(V)))*.
233[0:MRR:232.1,124.1] Object(U) Object(V) || P(Place(W,U),Place(W,V))*+ Continuous(W,X,HPlace(U)) AlwaysIntConn(W,X,HPlace(U))* NoExitCavity(W,X,HPlace(V),Y)* -> P(Slice(X,HPlace(U)),Slice(X,HPlace(V)))* Lt(skf5(W,X,Z,X1),X)*.
250[0:SSi:249.1,90.0] Object(U) || P(Rc1,Place(Ta1,U)) Continuous(Ta1,V,Hc1) AlwaysIntConn(Ta1,V,Hc1) NoExitCavity(Ta1,V,HPlace(U),W)*+ -> P(Slice(V,Hc1),Slice(V,HPlace(U)))* O(Slice(skf5(Ta1,V,W,Hc1),Hc1),Slice(skf5(Ta1,V,W,Hc1),W))*.
277[2:SSi:276.1,216.0,19.1,130.0] Object(U) || P(Rc1,Rc1) Continuous(Ta1,V,Hc1) AlwaysIntConn(Ta1,V,Hc1) NoExitCavity(Ta1,V,Hc1,HPlace(U)) Cavity(Slice(skf5(Ta1,V,HPlace(U),Hc1),Hc1),Place(skf5(Ta1,V,HPlace(U),Hc1),U))* -> P(Slice(V,Hc1),Slice(V,Hc1)).
297[2:SoR:296.0,4.1] RigidObject(Ob1) || P(Rc1,Rc1) Continuous(Ta1,Tb1,Hc1) AlwaysIntConn(Ta1,Tb1,Hc1) -> P(Slice(Tb1,Hc1),Slice(Tb1,Hc1)) Region(Place(skf5(Ta1,Tb1,HPlace(Ob1),Hc1),Ob1))*.
296[2:Res:20.0,292.4] Object(Ob1) || P(Rc1,Rc1) Continuous(Ta1,Tb1,Hc1) AlwaysIntConn(Ta1,Tb1,Hc1) -> P(Slice(Tb1,Hc1),Slice(Tb1,Hc1)) Region(Place(skf5(Ta1,Tb1,HPlace(Ob1),Hc1),Ob1))*.
292[2:Res:255.6,98.0] Object(U) || P(Rc1,Rc1) Continuous(Ta1,V,Hc1) AlwaysIntConn(Ta1,V,Hc1) NoExitCavity(Ta1,V,Hc1,HPlace(U))+ -> P(Slice(V,Hc1),Slice(V,Hc1))* Region(Place(skf5(Ta1,V,HPlace(U),Hc1),U))*.
196[0:MRR:194.1,124.1] Object(U) || P(Place(V,U),Slice(V,W))*+ Continuous(V,X,HPlace(U)) AlwaysIntConn(V,X,HPlace(U)) NoExitCavity(V,X,W,Y)* -> P(Slice(X,HPlace(U)),Slice(X,W))* O(Slice(skf5(V,X,Y,HPlace(U)),HPlace(U)),Slice(skf5(V,X,Y,HPlace(U)),Y))*.
255[2:SSi:251.1,216.0,19.1,130.0] Object(U) || P(Rc1,Rc1) Continuous(Ta1,V,Hc1) AlwaysIntConn(Ta1,V,Hc1) NoExitCavity(Ta1,V,Hc1,HPlace(U)) -> P(Slice(V,Hc1),Slice(V,Hc1)) O(Slice(skf5(Ta1,V,HPlace(U),Hc1),Hc1),Place(skf5(Ta1,V,HPlace(U),Hc1),U))*.
259[0:Res:191.5,108.1] || P(Slice(Ta1,U),Rc1) Continuous(Ta1,V,U) AlwaysIntConn(Ta1,V,U) NoExitCavity(Ta1,V,Hc1,W) Cavity(Slice(skf5(Ta1,V,W,U),U),Slice(skf5(Ta1,V,W,U),W))* -> P(Slice(V,U),Slice(V,Hc1)).
286[0:SoR:282.0,4.1] RigidObject(Ox1) || Continuous(Ta1,U,HPlace(Ox1)) AlwaysIntConn(Ta1,U,HPlace(Ox1)) NoExitCavity(Ta1,U,Hc1,V) -> P(Slice(U,HPlace(Ox1)),Slice(U,Hc1))* Region(Slice(skf5(Ta1,U,V,HPlace(Ox1)),HPlace(Ox1)))*.
282[0:Res:6.0,268.1] Object(Ox1) || Continuous(Ta1,U,HPlace(Ox1)) AlwaysIntConn(Ta1,U,HPlace(Ox1)) NoExitCavity(Ta1,U,Hc1,V) -> P(Slice(U,HPlace(Ox1)),Slice(U,Hc1))* Region(Slice(skf5(Ta1,U,V,HPlace(Ox1)),HPlace(Ox1)))*.
195[0:MRR:192.1,124.1] Object(U) || P(Slice(V,W),Place(V,U))*+ Continuous(V,X,W) AlwaysIntConn(V,X,W) NoExitCavity(V,X,HPlace(U),Y)* -> P(Slice(X,W),Slice(X,HPlace(U)))* O(Slice(skf5(V,X,Y,W),W),Slice(skf5(V,X,Y,W),Y))*.
268[0:SSi:267.1,90.0] Object(U) || P(Place(Ta1,U),Rc1)+ Continuous(Ta1,V,HPlace(U)) AlwaysIntConn(Ta1,V,HPlace(U)) NoExitCavity(Ta1,V,Hc1,W) -> P(Slice(V,HPlace(U)),Slice(V,Hc1))* Region(Slice(skf5(Ta1,V,W,HPlace(U)),HPlace(U)))*.
281[0:SoR:280.0,4.1] RigidObject(Ox1) || Continuous(Ta1,U,HPlace(Ox1)) AlwaysIntConn(Ta1,U,HPlace(Ox1)) NoExitCavity(Ta1,U,Hc1,V) -> P(Slice(U,HPlace(Ox1)),Slice(U,Hc1))* Region(Slice(skf5(Ta1,U,V,HPlace(Ox1)),V))*.
280[0:Res:6.0,271.1] Object(Ox1) || Continuous(Ta1,U,HPlace(Ox1)) AlwaysIntConn(Ta1,U,HPlace(Ox1)) NoExitCavity(Ta1,U,Hc1,V) -> P(Slice(U,HPlace(Ox1)),Slice(U,Hc1))* Region(Slice(skf5(Ta1,U,V,HPlace(Ox1)),V))*.
271[0:SSi:270.1,90.0] Object(U) || P(Place(Ta1,U),Rc1)+ Continuous(Ta1,V,HPlace(U)) AlwaysIntConn(Ta1,V,HPlace(U)) NoExitCavity(Ta1,V,Hc1,W) -> P(Slice(V,HPlace(U)),Slice(V,Hc1))* Region(Slice(skf5(Ta1,V,W,HPlace(U)),W))*.
174[0:MRR:172.1,124.1] Object(U) || P(Place(V,U),Slice(V,W))*+ Continuous(V,X,HPlace(U)) AlwaysIntConn(V,X,HPlace(U))* NoExitCavity(V,X,W,Y)* -> Lt(V,skf5(V,Z,X1,X2))* P(Slice(X,HPlace(U)),Slice(X,W))*.
252[0:Res:248.5,108.1] || P(Rc1,Rc1) Continuous(Ta1,U,Hc1) AlwaysIntConn(Ta1,U,Hc1) NoExitCavity(Ta1,U,Hc1,V) Cavity(Slice(skf5(Ta1,U,V,Hc1),Hc1),Slice(skf5(Ta1,U,V,Hc1),V))* -> P(Slice(U,Hc1),Slice(U,Hc1)).
275[0:SoR:274.0,4.1] RigidObject(Ox1) || Continuous(Ta1,U,HPlace(Ox1)) AlwaysIntConn(Ta1,U,HPlace(Ox1)) NoExitCavity(Ta1,U,Hc1,V)* -> P(Slice(U,HPlace(Ox1)),Slice(U,Hc1))* Lt(skf5(Ta1,U,W,X),U)*.
274[0:Res:6.0,227.1] Object(Ox1) || Continuous(Ta1,U,HPlace(Ox1)) AlwaysIntConn(Ta1,U,HPlace(Ox1)) NoExitCavity(Ta1,U,Hc1,V)* -> P(Slice(U,HPlace(Ox1)),Slice(U,Hc1))* Lt(skf5(Ta1,U,W,X),U)*.
227[0:SSi:226.1,90.0] Object(U) || P(Place(Ta1,U),Rc1)+ Continuous(Ta1,V,HPlace(U)) AlwaysIntConn(Ta1,V,HPlace(U)) NoExitCavity(Ta1,V,Hc1,W)* -> P(Slice(V,HPlace(U)),Slice(V,Hc1))* Lt(skf5(Ta1,V,X,Y),V)*.
164[0:MRR:162.1,124.1] Object(U) || P(Place(V,U),Slice(V,W))*+ Continuous(V,X,HPlace(U)) AlwaysIntConn(V,X,HPlace(U))* NoExitCavity(V,X,W,Y)* -> P(Slice(X,HPlace(U)),Slice(X,W))* Lt(skf5(V,X,Z,X1),X)*.
260[0:Res:191.5,98.0] || P(Slice(Ta1,U),Rc1)+ Continuous(Ta1,V,U) AlwaysIntConn(Ta1,V,U) NoExitCavity(Ta1,V,Hc1,W) -> P(Slice(V,U),Slice(V,Hc1))* Region(Slice(skf5(Ta1,V,W,U),W))*.
261[0:Res:191.5,97.0] || P(Slice(Ta1,U),Rc1)+ Continuous(Ta1,V,U) AlwaysIntConn(Ta1,V,U) NoExitCavity(Ta1,V,Hc1,W) -> P(Slice(V,U),Slice(V,Hc1))* Region(Slice(skf5(Ta1,V,W,U),U))*.
264[0:Res:20.0,253.3] || P(Rc1,Rc1) Continuous(Ta1,Tb1,Hc1) AlwaysIntConn(Ta1,Tb1,Hc1) -> P(Slice(Tb1,Hc1),Slice(Tb1,Hc1)) Region(Slice(skf5(Ta1,Tb1,HPlace(Ob1),Hc1),HPlace(Ob1)))*.
253[0:Res:248.5,98.0] || P(Rc1,Rc1) Continuous(Ta1,U,Hc1) AlwaysIntConn(Ta1,U,Hc1) NoExitCavity(Ta1,U,Hc1,V)+ -> P(Slice(U,Hc1),Slice(U,Hc1))* Region(Slice(skf5(Ta1,U,V,Hc1),V))*.
191[0:SpL:7.0,82.0] || P(Slice(Ta1,U),Rc1) Continuous(Ta1,V,U) AlwaysIntConn(Ta1,V,U) NoExitCavity(Ta1,V,Hc1,W) -> P(Slice(V,U),Slice(V,Hc1)) O(Slice(skf5(Ta1,V,W,U),U),Slice(skf5(Ta1,V,W,U),W))*.
256[0:Res:20.0,254.3] || P(Rc1,Rc1) Continuous(Ta1,Tb1,Hc1) AlwaysIntConn(Ta1,Tb1,Hc1) -> P(Slice(Tb1,Hc1),Slice(Tb1,Hc1)) Region(Slice(skf5(Ta1,Tb1,HPlace(Ob1),Hc1),Hc1))*.
254[0:Res:248.5,97.0] || P(Rc1,Rc1) Continuous(Ta1,U,Hc1) AlwaysIntConn(Ta1,U,Hc1) NoExitCavity(Ta1,U,Hc1,V)+ -> P(Slice(U,Hc1),Slice(U,Hc1))* Region(Slice(skf5(Ta1,U,V,Hc1),Hc1))*.
248[0:SpL:7.0,193.0] || P(Rc1,Rc1) Continuous(Ta1,U,Hc1) AlwaysIntConn(Ta1,U,Hc1) NoExitCavity(Ta1,U,Hc1,V) -> P(Slice(U,Hc1),Slice(U,Hc1)) O(Slice(skf5(Ta1,U,V,Hc1),Hc1),Slice(skf5(Ta1,U,V,Hc1),V))*.
220[0:SSi:219.1,90.0] Object(U) || P(Rc1,Place(Ta1,U)) Continuous(Ta1,V,Hc1) AlwaysIntConn(Ta1,V,Hc1) NoExitCavity(Ta1,V,HPlace(U),W)*+ -> P(Slice(V,Hc1),Slice(V,HPlace(U)))* Lt(skf5(Ta1,V,X,Y),V)*.
193[0:SpL:7.0,82.0] || P(Rc1,Slice(Ta1,U))+ Continuous(Ta1,V,Hc1) AlwaysIntConn(Ta1,V,Hc1) NoExitCavity(Ta1,V,U,W)* -> P(Slice(V,Hc1),Slice(V,U))* O(Slice(skf5(Ta1,V,W,Hc1),Hc1),Slice(skf5(Ta1,V,W,Hc1),W))*.
239[4:Res:234.1,165.2] || Cavity(Slice(Tb1,Hc1),Slice(Tb1,Hc1))*+ Cavity(Slice(Tb1,Hc1),U) DR(Slice(Tb1,HPlace(Ox1)),U)* Leq3(V,Tb1,W) AlwaysIntConn(V,W,HPlace(Ox1))* -> .
247[4:SoR:242.0,4.1] RigidObject(Ox1) || Cavity(Slice(Tb1,Hc1),U)* Cavity(Place(Tb1,Ox1),U) -> .
242[4:SSi:241.1,89.0] Object(Ox1) || Cavity(Slice(Tb1,Hc1),U)* Cavity(Place(Tb1,Ox1),U) -> .
243[4:SoR:240.0,4.1] RigidObject(Ox1) || Cavity(Slice(Tb1,Hc1),U) -> O(Place(Tb1,Ox1),U)*.
173[0:MRR:170.1,124.1] Object(U) || P(Slice(V,W),Place(V,U))*+ Continuous(V,X,W) AlwaysIntConn(V,X,W)* NoExitCavity(V,X,HPlace(U),Y)* -> Lt(V,skf5(V,Z,X1,X2))* P(Slice(X,W),Slice(X,HPlace(U)))*.
240[4:SSi:235.1,89.0] Object(Ox1) || Cavity(Slice(Tb1,Hc1),U) -> O(Place(Tb1,Ox1),U)*.
236[4:Res:234.1,108.1] || Cavity(Slice(Tb1,Hc1),U) Cavity(Slice(Tb1,HPlace(Ox1)),U)* -> .
238[4:Res:234.1,97.0] || Cavity(Slice(Tb1,Hc1),U)* -> Region(Slice(Tb1,HPlace(Ox1))).
234[4:Spt:230.0,230.3] || Cavity(Slice(Tb1,Hc1),U) -> O(Slice(Tb1,HPlace(Ox1)),U)*.
163[0:MRR:160.1,124.1] Object(U) || P(Slice(V,W),Place(V,U))*+ Continuous(V,X,W) AlwaysIntConn(V,X,W)* NoExitCavity(V,X,HPlace(U),Y)* -> P(Slice(X,W),Slice(X,HPlace(U)))* Lt(skf5(V,X,Z,X1),X)*.
159[0:SpL:7.0,80.0] || P(Slice(Ta1,U),Rc1)+ Continuous(Ta1,V,U) AlwaysIntConn(Ta1,V,U) NoExitCavity(Ta1,V,Hc1,W)* -> P(Slice(V,U),Slice(V,Hc1))* Lt(skf5(Ta1,V,X,Y),V)*.
222[3:Spt:221.4] ||  -> Lt(skf5(Ta1,Tb1,U,V),Tb1)*.
218[0:SpL:7.0,161.0] || P(Rc1,Rc1) Continuous(Ta1,U,Hc1) AlwaysIntConn(Ta1,U,Hc1) NoExitCavity(Ta1,U,Hc1,V)*+ -> P(Slice(U,Hc1),Slice(U,Hc1))* Lt(skf5(Ta1,U,W,X),U)*.
161[0:SpL:7.0,80.0] || P(Rc1,Slice(Ta1,U))+ Continuous(Ta1,V,Hc1) AlwaysIntConn(Ta1,V,Hc1) NoExitCavity(Ta1,V,U,W)* -> P(Slice(V,Hc1),Slice(V,U))* Lt(skf5(Ta1,V,X,Y),V)*.
217[0:SoR:208.0,4.1] RigidObject(Ox1) || P(Place(U,Ox1),Slice(U,Hc1))* Continuous(U,Tb1,HPlace(Ox1)) AlwaysIntConn(U,Tb1,HPlace(Ox1)) NoExitCavity(U,Tb1,Hc1,V)* -> Lt(U,skf5(U,W,X,Y))*.
208[0:MRR:207.1,124.1] Object(Ox1) || P(Place(U,Ox1),Slice(U,Hc1))* Continuous(U,Tb1,HPlace(Ox1)) AlwaysIntConn(U,Tb1,HPlace(Ox1)) NoExitCavity(U,Tb1,Hc1,V)* -> Lt(U,skf5(U,W,X,Y))*.
213[0:SoR:201.0,4.1] RigidObject(Ox1) || P(Place(U,Ox1),Slice(U,Hc1))* Continuous(U,Tb1,HPlace(Ox1)) AlwaysIntConn(U,Tb1,HPlace(Ox1)) NoExitCavity(U,Tb1,Hc1,V)* -> Lt(skf5(U,Tb1,W,X),Tb1)*.
216[2:Res:214.0,9.0] ||  -> Time(skf5(Ta1,U,V,W))*.
214[2:Spt:171.4] ||  -> Lt(Ta1,skf5(Ta1,U,V,W))*.
201[0:MRR:200.1,124.1] Object(Ox1) || P(Place(U,Ox1),Slice(U,Hc1))* Continuous(U,Tb1,HPlace(Ox1)) AlwaysIntConn(U,Tb1,HPlace(Ox1)) NoExitCavity(U,Tb1,Hc1,V)* -> Lt(skf5(U,Tb1,W,X),Tb1)*.
85[0:Res:81.5,59.0] || P(Slice(U,HPlace(Ox1)),Slice(U,Hc1))*+ Continuous(U,Tb1,HPlace(Ox1)) AlwaysIntConn(U,Tb1,HPlace(Ox1)) NoExitCavity(U,Tb1,Hc1,V)* -> Lt(U,skf5(U,W,X,Y))*.
198[0:SoR:178.0,4.1] RigidObject(Ox1) || Cavity(Slice(Tb1,Hc1),U) DR(Place(Tb1,Ox1),U)* O(Place(Tb1,Ox1),Slice(Tb1,Hc1))* Leq3(V,Tb1,W) AlwaysIntConn(V,W,HPlace(Ox1))* -> .
86[0:Res:80.5,59.0] || P(Slice(U,HPlace(Ox1)),Slice(U,Hc1))*+ Continuous(U,Tb1,HPlace(Ox1)) AlwaysIntConn(U,Tb1,HPlace(Ox1)) NoExitCavity(U,Tb1,Hc1,V)* -> Lt(skf5(U,Tb1,W,X),Tb1)*.
178[0:SSi:177.1,89.0] Object(Ox1) || Cavity(Slice(Tb1,Hc1),U) DR(Place(Tb1,Ox1),U)* O(Place(Tb1,Ox1),Slice(Tb1,Hc1))* Leq3(V,Tb1,W) AlwaysIntConn(V,W,HPlace(Ox1))* -> .
190[1:SoR:185.0,4.1] RigidObject(Ox1) || Cavity(Slice(Tb1,Hc1),U) DR(Place(Tb1,Ox1),U)* Leq3(V,Tb1,W) AlwaysIntConn(V,W,HPlace(Ox1))* -> Cavity(Place(Tb1,Ox1),Slice(Tb1,Hc1))*.
82[0:Inp] || P(Slice(U,V),Slice(U,W))*+ Continuous(U,X,V) AlwaysIntConn(U,X,V) NoExitCavity(U,X,W,Y)* -> P(Slice(X,V),Slice(X,W))* O(Slice(skf5(U,X,Y,V),V),Slice(skf5(U,X,Y,V),Y))*.
185[1:SSi:184.1,89.0] Object(Ox1) || Cavity(Slice(Tb1,Hc1),U) DR(Place(Tb1,Ox1),U)* Leq3(V,Tb1,W) AlwaysIntConn(V,W,HPlace(Ox1))* -> Cavity(Place(Tb1,Ox1),Slice(Tb1,Hc1))*.
180[1:MRR:179.0,72.2] || Cavity(Slice(Tb1,Hc1),U) DR(Slice(Tb1,HPlace(Ox1)),U)*+ Leq3(V,Tb1,W) AlwaysIntConn(V,W,HPlace(Ox1))* -> Cavity(Slice(Tb1,HPlace(Ox1)),Slice(Tb1,Hc1))*.
165[0:SoR:83.0,72.2] || Cavity(Slice(Tb1,Hc1),U) DR(Slice(Tb1,HPlace(Ox1)),U)* O(Slice(Tb1,HPlace(Ox1)),Slice(Tb1,Hc1))*+ Leq3(V,Tb1,W) AlwaysIntConn(V,W,HPlace(Ox1))* -> .
81[0:Inp] || P(Slice(U,V),Slice(U,W))*+ Continuous(U,X,V) AlwaysIntConn(U,X,V)* NoExitCavity(U,X,W,Y)* -> Lt(U,skf5(U,Z,X1,X2))* P(Slice(X,V),Slice(X,W))*.
168[0:SSi:167.1,19.1] Object(U) || IntConn(Place(skf4(HPlace(U),V,W),U))* Lt(W,V) -> AlwaysIntConn(W,V,HPlace(U)).
157[0:SSi:156.2,19.1] Object(U) Time(skf4(HPlace(U),V,W)) || IntConn(Place(skf4(HPlace(U),V,W),U))* Lt(X,Y) -> AlwaysIntConn(X,Y,HPlace(U))*.
83[0:Res:76.4,59.0] IntConn(Slice(Tb1,HPlace(Ox1))) || Cavity(Slice(Tb1,Hc1),U) DR(Slice(Tb1,HPlace(Ox1)),U)* O(Slice(Tb1,HPlace(Ox1)),Slice(Tb1,Hc1))* -> .
155[1:Res:78.4,87.1] Time(U) Object(V) Object(W) IntConn(Place(U,W)) ||  -> equal(W,V) Cavity(Place(U,W),Place(U,V))*.
80[0:Inp] || P(Slice(U,V),Slice(U,W))*+ Continuous(U,X,V) AlwaysIntConn(U,X,V)* NoExitCavity(U,X,W,Y)* -> P(Slice(X,V),Slice(X,W))* Lt(skf5(U,X,Z,X1),X)*.
152[0:Res:78.4,57.0] Time(U) Object(V) Object(W) || O(Place(U,W),Place(U,V))* -> equal(W,V).
79[0:Inp] History(U) || IntConn(Slice(skf4(U,V,W),U))*+ Lt(X,Y) -> AlwaysIntConn(X,Y,U)*.
78[0:Inp] Time(U) Object(V) Object(W) ||  -> equal(W,V) DR(Place(U,W),Place(U,V))*.
150[0:Res:77.3,25.0] History(U) || Lt(V,W) -> AlwaysIntConn(V,W,U) Time(skf4(U,W,V))*.
77[0:Inp] History(U) || Lt(V,W) -> AlwaysIntConn(V,W,U) Leq3(V,skf4(U,W,V),W)*.
76[0:Inp] IntConn(U) || Cavity(V,W)*+ DR(U,W)* O(U,V)* -> P(U,V).
72[0:Inp] || AlwaysIntConn(U,V,W)*+ Leq3(U,X,V)* -> IntConn(Slice(X,W))*.
148[0:SoR:146.0,4.1] RigidObject(Ox1) || P(Place(Tb1,Ox1),Slice(Tb1,Hc1))* -> .
146[0:SSi:145.1,89.0] Object(Ox1) || P(Place(Tb1,Ox1),Slice(Tb1,Hc1))* -> .
70[0:Inp] Object(U) Time(V) ||  -> equal(Slice(V,HPlace(U)),Place(V,U))**.
135[1:SSi:134.0,3.1] Region(U) IntConn(V) ||  -> O(V,U)* Cavity(V,U).
68[0:Inp] Object(U) || Lt(V,W) -> Continuous(V,W,HPlace(U))*.
136[0:Res:20.0,127.0] ||  -> History(HPlace(Ob1))*.
127[0:Res:65.1,56.0] || NoExitCavity(U,V,W,X)* -> History(X).
69[0:Inp] Region(U) Region(V) ||  -> DR(U,V)* O(U,V).
130[0:Res:20.0,126.0] ||  -> History(Hc1)*.
126[0:Res:65.1,55.0] || NoExitCavity(U,V,W,X)* -> History(W).
125[0:Res:65.1,54.0] || NoExitCavity(U,V,W,X)* -> Time(V).
124[0:Res:65.1,53.0] || NoExitCavity(U,V,W,X)* -> Time(U).
65[0:Inp] || NoExitCavity(U,V,W,X) -> SkP3(X,W,V,U)*.
123[0:Res:66.1,56.0] || NoEntranceCavity(U,V,W,X)* -> History(X).
122[0:Res:66.1,55.0] || NoEntranceCavity(U,V,W,X)* -> History(W).
121[0:Res:66.1,54.0] || NoEntranceCavity(U,V,W,X)* -> Time(V).
120[0:Res:66.1,53.0] || NoEntranceCavity(U,V,W,X)* -> Time(U).
66[0:Inp] || NoEntranceCavity(U,V,W,X) -> SkP3(X,W,V,U)*.
119[0:Res:67.1,56.0] || PersistentCavity(U,V,W,X)* -> History(X).
118[0:Res:67.1,55.0] || PersistentCavity(U,V,W,X)* -> History(W).
117[0:Res:67.1,54.0] || PersistentCavity(U,V,W,X)* -> Time(V).
116[0:Res:67.1,53.0] || PersistentCavity(U,V,W,X)* -> Time(U).
67[0:Inp] || PersistentCavity(U,V,W,X) -> SkP3(X,W,V,U)*.
64[0:Inp] History(U) Time(V) ||  -> Region(Slice(V,U))*.
63[0:Inp] Object(U) Time(V) ||  -> Region(Place(V,U))*.
114[0:Res:60.1,44.0] || Continuous(U,V,W)* -> History(W).
113[0:Res:60.1,43.0] || Continuous(U,V,W)* -> Time(V).
62[0:Inp] Region(U) Region(V) ||  -> Region(RUnion(V,U))*.
112[0:Res:60.1,42.0] || Continuous(U,V,W)* -> Time(U).
111[0:Res:61.1,44.0] || WeaklyContinuous(U,V,W)* -> History(W).
110[0:Res:61.1,43.0] || WeaklyContinuous(U,V,W)* -> Time(V).
109[0:Res:61.1,42.0] || WeaklyContinuous(U,V,W)* -> Time(U).
60[0:Inp] || Continuous(U,V,W) -> SkP2(W,V,U)*.
61[0:Inp] || WeaklyContinuous(U,V,W) -> SkP2(W,V,U)*.
59[0:Inp] || P(Slice(Tb1,HPlace(Ox1)),Slice(Tb1,Hc1))* -> .
53[0:Inp] || SkP3(U,V,W,X)* -> Time(X).
54[0:Inp] || SkP3(U,V,W,X)* -> Time(W).
55[0:Inp] || SkP3(U,V,W,X)* -> History(V).
56[0:Inp] || SkP3(U,V,W,X)* -> History(U).
58[0:Inp] || AlwaysIntConn(U,V,W)* -> Lt(U,V).
108[0:Res:51.1,57.0] || Cavity(U,V) O(U,V)* -> .
57[0:Inp] || DR(U,V)* O(U,V) -> .
48[0:Inp] || AlwaysIntConn(U,V,W)* -> Time(U).
49[0:Inp] || AlwaysIntConn(U,V,W)* -> Time(V).
24[0:Inp] || Leq3(U,V,W)* -> Time(U).
25[0:Inp] || Leq3(U,V,W)* -> Time(V).
26[0:Inp] || Leq3(U,V,W)* -> Time(W).
42[0:Inp] || SkP2(U,V,W)* -> Time(W).
43[0:Inp] || SkP2(U,V,W)* -> Time(V).
33[0:Inp] || OSPlace(U,V,W)* -> Time(U).
36[0:Inp] || ClosedContainer(U,V,W)* -> Time(U).
39[0:Inp] || CContained(U,V,W)* -> Time(U).
45[0:Inp] || Constant(U,V,W)* -> Time(U).
46[0:Inp] || Constant(U,V,W)* -> Time(V).
35[0:Inp] || OSPlace(U,V,W)* -> Region(W).
38[0:Inp] || ClosedContainer(U,V,W)* -> Region(W).
52[0:Inp] || AlwaysIntConn(U,V,W)* -> History(W).
44[0:Inp] || SkP2(U,V,W)* -> History(U).
47[0:Inp] || Constant(U,V,W)* -> History(W).
40[0:Inp] || CContained(U,V,W)* -> Object(V).
34[0:Inp] || OSPlace(U,V,W)* -> ObjectSet(V).
37[0:Inp] || ClosedContainer(U,V,W)* -> ObjectSet(V).
41[0:Inp] || CContained(U,V,W)* -> ObjectSet(W).
51[0:Inp] || Cavity(U,V) -> DR(U,V)*.
104[0:Res:6.0,100.0] ||  -> Region(Rc1)*.
100[0:Res:27.1,15.0] || P(U,V)* -> Region(V).
101[0:Res:6.0,99.0] ||  -> Region(Place(Ta1,Ox1))*.
30[0:Inp] || DR(U,V) -> SkP0(V,U)*.
99[0:Res:27.1,14.0] || P(U,V)* -> Region(U).
27[0:Inp] || P(U,V) -> SkP0(V,U)*.
98[0:Res:28.1,15.0] || O(U,V)* -> Region(V).
97[0:Res:28.1,14.0] || O(U,V)* -> Region(U).
28[0:Inp] || O(U,V) -> SkP0(V,U)*.
96[0:Res:29.1,15.0] || EC(U,V)* -> Region(V).
95[0:Res:29.1,14.0] || EC(U,V)* -> Region(U).
94[0:Res:31.1,17.0] || Cavity(U,V)* -> Region(V).
93[0:Res:31.1,16.0] || Cavity(U,V)* -> Region(U).
29[0:Inp] || EC(U,V) -> SkP0(V,U)*.
31[0:Inp] || Cavity(U,V) -> SkP1(V,U)*.
92[0:Res:32.1,17.0] || Outside(U,V)* -> Region(V).
91[0:Res:32.1,16.0] || Outside(U,V)* -> Region(U).
90[0:Res:1.0,8.0] ||  -> Time(Ta1)*.
32[0:Inp] || Outside(U,V) -> SkP1(V,U)*.
8[0:Inp] || Lt(U,V)* -> Time(U).
89[0:Res:1.0,9.0] ||  -> Time(Tb1)*.
9[0:Inp] || Lt(U,V)* -> Time(V).
10[0:Inp] || Leq(U,V)* -> Time(U).
11[0:Inp] || Leq(U,V)* -> Time(V).
12[0:Inp] || Ordered(U,V)* -> Time(U).
13[0:Inp] || Ordered(U,V)* -> Time(V).
21[0:Inp] || DR(U,V)* -> Region(U).
22[0:Inp] || DR(U,V)* -> Region(V).
14[0:Inp] || SkP0(U,V)* -> Region(V).
15[0:Inp] || SkP0(U,V)* -> Region(U).
16[0:Inp] || SkP1(U,V)* -> Region(V).
17[0:Inp] || SkP1(U,V)* -> Region(U).
23[0:Inp] || Cavity(U,V)* -> IntConn(U).
19[0:Inp] Object(U) ||  -> History(HPlace(U))*.
18[0:Inp] Object(U) ||  -> ObjectSet(Singleton(U))*.
20[0:Inp] ||  -> NoExitCavity(Ta1,Tb1,Hc1,HPlace(Ob1))*.
3[0:Inp] IntConn(U) ||  -> Region(U)*.
5[0:Inp] RigidHistory(U) ||  -> History(U)*.
4[0:Inp] RigidObject(U) ||  -> Object(U)*.
6[0:Inp] ||  -> P(Place(Ta1,Ox1),Rc1)*.
7[0:Inp] ||  -> equal(Slice(Ta1,Hc1),Rc1)**.
2[0:Inp] || equal(Ob1,Ox1)** -> .
1[0:Inp] ||  -> Lt(Ta1,Tb1)*.
87[1:Spt:71.0,71.1,71.3] IntConn(U) || DR(U,V)* -> Cavity(U,V).
--------------------------SPASS-STOP------------------------------