AND fears(x,z1) =  y1 = z1 FORALL x:T4 U T5. FORALL y1. FORALL z1. craves(x,y1)
AND craves(x,z1) =  y1 = z1 FORALL x:T4 U T5. (Exists y1:T0. craves(x,y1)
OR Exists y1:T4. fears(x,y1))
FORALL x:T4 U T5. NOT (Exists y1:T0. craves(x,y1)
AND Exists y1:T4. fears(x,y1))

## Tim :  Domain  Invariants:

(x0,x1): attacks(x0,x1)   = 5 (x0,x1): eats(x0,x1)
= 36 x0: food(x0)
= 13
(x0,x1): harmony(x0,x1)
= 2
(x0,x1): locale(x0,x1)
= 13
(x0,x1): orbits(x0,x1)
= 2 x0: pain(x0)
= 8 x0: planet(x0)   = 3 x0: pleasure(x0)
= 2 x0: province(x0)   = 6

## Tim: Attribute Spaces:

Objects, x, in T1 U T2 U T3 can have property: Exists y1:T4. harmony(y1,x); Objects, x, in T6 U T7 U T8 can have property: Exists y1:T0. locale(y1,x); Objects, x, in T4 can have property:
Exists y1:T4. fears(y1,x);
Objects, x, in TO can have property: Exists y1:T4 U T5. craves(y1,x);
Objects, x, in T6 U T7 all have property:
Exists y1:T6 U T8. attacks(x,y1);
Objects, x, in T6 U T8 all have property:
Exists y1:T6 U T7. attacks(y1,x);
Objects, x, in TO all have property: Exists y1:T0. eats(x,y1); Objects, x, in TO all have property: Exists y1:T0. eats(y1,x); Objects, x, in TO all have property: food(x); Objects, x, in T2 U T3 all have property:
Exists y1:T1 U T2. orbits(x,y1);