S contains the constraints od( v, w ) ≪ od( z, y ) od( w, x ) ≪ od( z, y ).

od( x, y ) ≪ od( z, y ).

od( z, y ) ≪ od( v, z ).

The algorithm proceeds as follows:
Initialization:
The tree is initializes to a single node with n 1.

n1.symbols := { v, w, x, y, z }.

First iteration:
The shorts of S are { vw, wx, xy, zy, vz }.

H is set to its connected components, which is the complete graph over v, w, x, y, z. The algorithm exits returning false Table 2: Example of determining inconsistency axiom A.7 and has only finitely many different orders of magnitude. If the algorithm returns T and T has no more different labels than the number of different orders of magnitude in the space, then the constraints are satisfiable. If T uses more labels than the space has orders of magnitude, then the constraints are unsatisfiable.

The proof is easier to present if we rewrite algorithm solve constraints in the following form, which returns only the number of different non-zero labels used, but does not actually construct the cluster tree. 1 function num_labels( S );
if S is empty then return(0)
else return(1 + num labels(reduce constraints( S )))
function reduce constraints( S )
H := connected components of the shorts of S ; if H contains all the edges in S then return(false) to top-level else return(the set of constraints in S whose long is in H )
It is easily verified that the sequence of values of S in successive recursive calls to num labels is the same as the sequence of values of S in the main loop of solve constraints. Therefore num labels returns the number of different non-zero labels in the tree constructed by solve constraints.