(VAR x y h i u v)
(THEORY (AC or))
(THEORY (C eq))
(RULES
  eq(0, 0) -> true
  eq(0, s(x)) -> false
  eq(s(x), 0) -> false
  eq(s(x), s(y)) -> eq(x, y)
  or(true, y) -> true
  or(false, y) -> y
  union(empty, h) -> h
  union(edge(x, y, i), h) -> edge(x, y, union(i, h))
  reach(x, y, empty, h) -> false
  reach(x, y, edge(u, v, i), h) -> if_reach_1(eq(x, u), x, y, edge(u, v, i), h)
  if_reach_1(true, x, y, edge(u, v, i), h) -> if_reach_2(eq(y, v), x, y, edge(u, v, i), h)
  if_reach_1(false, x, y, edge(u, v, i), h) -> reach(x, y, i, edge(u, v, h))
  if_reach_2(true, x, y, edge(u, v, i), h) -> true
  if_reach_2(false, x, y, edge(u, v, i), h) -> or(reach(x, y, i, h), reach(v, y, union(i, h), empty))
)