The following invariants add the constraints that trucks and airplanes must always be at a location and never loaded into one another.

FORALL x:TO. FORALL y1. FORALL z1. at(x,y1) AND at(x,z1) =  y1 = z1 FORALL x:TO. (Exists y1:T1 U T2. at(x,y1)) FORALL x:T5. FORALL y1. FORALL z1. at(x,y1) AND at(x,z1) =  y1 = z1 FORALL x:T5. (Exists y1:T1 U T2. at(x,y1))

## Appendix D. The Rocket Domain

The Rocket domain used in the construction of Figure 6 is as follows:
(define (domain rocket)
( : p r e d i c a t e s
(at x y)
(in x y) (fuelled x)
(unfuelled x)
(loc x)
(obj x) (container x))
(:action fly
:parameters ( x  y  z)
:precondition (and (at x y) (loc z) (fuelled x))
:effect (and (not (at x y)) (at x z) (unfuelled x)
(not (fuelled  x))))
(:action load
:parameters ( x  y  z)
:precondition (and (obj  x) (container  y) (at  x  z)
z))
(at y
:effect (and (in x y) (not (at x z))))
(:action unload
:parameters ( x  y  z) :precondition (and (at  y  z) (in  x  y))
:effect (and (at x z) (not (in x y))))

## Appendix E. Operator Test Domain

This domain is an artificial domain used to test the effects of increasing operators and literals in the domain encoding on the performance of TIM. This example is the third instance - the variation was achieved by adding more operator schemas in the pattern of those included here.