FORALL x:T2. (deflated(x))
The first attribute space, which contains all objects except the trunk and the hub, is now subjected to sub-space analysis yielding a rich new collection of invariants.

FORALL x:TO. FORALL y1. FORALL z1. in(x,y1) AND in(x,z1) =  y1 = z1 FORALL x:TO. (Exists y1:T3. in(x,y1) OR have(x))
FORALL x:TO. NOT (Exists y1:T3, in(x,y1) AND have(x))
FORALL x:T1. FORALL y1. FORALL z1. in(x,y1) AND in(x,z1) =  y1 = z1 FORALL x:T1. FORALL y1. FORALL z1. on(x,y1) AND on(x,z1) =  y1 = z1 FORALL x:T1. (Exists y1:T3. in(x,y1) OR have(x)
OR Exists y1:T4. on(x,y1))
FORALL x:T1. NOT (Exists y1:T3. in(x,y1) AND have(x))
FORALL x:T1. NOT (Exists y1:T3, in(x,y1) AND Exists y1:T4. on(x,y1))
FORALL x:T1. NOT (have(x) AND Exists y1:T4. on(x,y1))
FORALL x:T2. FORALL y1. FORALL z1. in(x,y1) AND in(x,z1) =  y1 = z1 FORALL x:T2. FORALL y1. FORALL z1. on(x,y1) AND on(x,z1) =  y1 = z1 FORALL x:T2. (Exists y1:T4. on(x,y1) OR have(x)
OR Exists y1:T3. in(x,y1))
FORALL x:T2. NOT (Exists y1:T4. on(x,y1) AND have(x))
FORALL x:T2. NOT (Exists y1:T4. on(x,y1) AND Exists y1:T3. in(x,y1))
FORALL x:T2. NOT (have(x) AND Exists y1:T3. in(x,y1)) FORALL x:T5. FORALL y1. FORALL z1. in(x,y1) AND in(x,z1) =  y1 = z1 FORALL x:T5. (Exists y1:T3. in(x,y1) OR have(x)) FORALL x:T5. NOT (Exists y1:T3. in(x,y1) AND have(x)) FORALL x:T6. FORALL y1. FORALL z1. in(x,y1) AND in(x,z1) =  y1 = z1 FORALL x:T6. FORALL y1. FORALL z1. tight(x,y1)
AND tight(x,z1) =  y1 = z1 FORALL x:T6. FORALL y1. FORALL z1. loose(x,y1)
AND loose(x,z1) =  y1 = z1 FORALL x:T6. (Exists y1:T4. tight(x,y1)
OR Exists y1:T4. loose(x,y1)
OR have(x) OR Exists y1:T3. in(x,y1))
FORALL x:T6. NOT (Exists y1:T4. tight(x,y1)
AND Exists y1:T4. loose(x,y1))
FORALL x:T6. NOT (Exists y1:T4. tight(x,y1) AND have(x))
FORALL x:T6. NOT (Exists y1:T4. tight(x,y1)
AND Exists y1:T3. in(x,y1))
FORALL x:T6. NOT (Exists y1:T4. loose(x,y1) AND have(x)) FORALL x:T6. NOT (Exists y1:T4. loose(x,y1)
AND Exists y1:T3. in(x,y1))
FORALL x:T6. NOT (have(x) AND Exists y1:T3. in(x,y1))