Twelf 1.5R3, Aug 30, 2005 (%trustme)
%% OK %%
[Opening file /home/www/twelf/hcode/fd12fb061fb3d16a8c2c4fde75258ad2]
node : type.
a : node.
b : node.
c : node.
d : node.
connect : node -> node -> type.
reaches : node -> node -> type.
connect/a-b : connect a b.
connect/a-c : connect a c.
connect/c-b : connect c b.
connect/c-d : connect c d.
reach/refl : {X:node} reaches X X.
reach/trans :
   {X:node} {Y:node} {Z:node} reaches Y Z -> connect X Y -> reaches X Z.
%query 1 *

reaches a d.
---------- Solution 1 ----------
Empty Substitution.
____________________________________________

%query 0 *

reaches b a.
____________________________________________

%query 5 *

reaches a Z.
---------- Solution 1 ----------
Z = a.
---------- Solution 2 ----------
Z = b.
---------- Solution 3 ----------
Z = c.
---------- Solution 4 ----------
Z = b.
---------- Solution 5 ----------
Z = d.
____________________________________________

[Closing file /home/www/twelf/hcode/fd12fb061fb3d16a8c2c4fde75258ad2]
%% OK %%