construct node M as a new child of N in T ;
M symbols:= the vertices of I ;
endfor endif endfor S := the subset of constraints in S whose long is in H ; m := m  - 1; until S is empty; for each leaf N of T
N label := 0; if N symbols has more than one symbol then create a leaf of N for each symbol in N symbols; label each such leaf 0; endif endfor end solve constraints.

Tables 3 and 4 give two examples of the working of procedure solve constraints. Table 3 shows how the procedure can be used to establish that the following constraints are cnsistent :
The Empire State Building ( x ) is mu closer to the Washington Monument ( w )
than to Notre Dame Cathedral (v).

Bunker Hill (y) is much closer to the Empire State Building than to the Eiffel Tower ( z ). The distance from the Eiffel Tower to Notre Dame is much less than the distance from the Washington Monument to Bunker Hill.

Table 4 shows that the following inference can be justified:
Given: The distances from the Statue of Liberty (v) to the World Trade Center ( w ), from the World Trade Center to the Empire State Building ( x ), and from the Empire State Building to the Chrysler Building ( y ) are all much less than the distance from the Chrysler Building to the Washington Monument ( z ).

Infer: The Washington Monument is not much nearer to the Chrysler Building than to the Statue of Liberty.

This inference is carried out by asserting the negation of the consequent, "The Washington Monument is much nearer to the Chrysler Building than to the Statue of Liberty," and showing that that collection of constraints is inconsistent. Note that if we change "much less" and "much nearer" in this example to "less" and "nearer", then the inference no longer valid.

Theorem 1 states the correctness of algorithm solve constraints. The proof is given in the appendix.

Theorem 1: The algorithm solve_constraints( S ) returns a cluster tree satisfying S if S is consistent, and returns false if S is inconsistent.

There may be many cluster trees that satisfy a given set of constraints. Among these, the cluster tree returned by the algorithm solve constraints has an important property: it has the fewest possible labels consistent with the constraints. In other words, it uses the minimum number of different orders of magnitude of any solution.  Therefore, the algorithm can be used to check the satisfiability of a set of constraints in an om-space that violates