MAYBE
Time: 0.007743
TRS:
 {                               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()))}
 DP:
  DP:
   {                               eq#(s x, s y) -> eq#(x, y),
                        union#(edge(x, y, i), h) -> union#(i, h),
                  reach#(x, y, edge(u, v, i), h) -> eq#(x, u),
                  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) -> eq#(y, v),
     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#(false(), x, y, edge(u, v, i), h) -> or#(reach(x, y, i, h), reach(v, y, union(i, h), empty())),
    if_reach_2#(false(), x, y, edge(u, v, i), h) -> union#(i, h),
    if_reach_2#(false(), x, y, edge(u, v, i), h) -> reach#(x, y, i, h),
    if_reach_2#(false(), x, y, edge(u, v, i), h) -> reach#(v, y, union(i, h), empty())}
  TRS:
  {                               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()))}
  UR:
   {                               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())),
                                        a(z, w) -> z,
                                        a(z, w) -> w}
   EDG:
    {(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_2#(false(), x, y, edge(u, v, i), h) -> reach#(v, y, union(i, h), empty()))
     (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_2#(false(), x, y, edge(u, v, i), h) -> reach#(x, y, 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_2#(false(), x, y, edge(u, v, i), h) -> union#(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_2#(false(), x, y, edge(u, v, i), h) -> or#(reach(x, y, i, h), reach(v, y, union(i, h), empty())))
     (if_reach_2#(false(), x, y, edge(u, v, i), h) -> reach#(v, y, union(i, h), empty()), reach#(x, y, edge(u, v, i), h) -> if_reach_1#(eq(x, u), x, y, edge(u, v, i), h))
     (if_reach_2#(false(), x, y, edge(u, v, i), h) -> reach#(v, y, union(i, h), empty()), reach#(x, y, edge(u, v, i), h) -> eq#(x, u))
     (union#(edge(x, y, i), h) -> union#(i, h), union#(edge(x, y, i), h) -> union#(i, h))
     (if_reach_2#(false(), x, y, edge(u, v, i), h) -> reach#(x, y, i, h), reach#(x, y, edge(u, v, i), h) -> if_reach_1#(eq(x, u), x, y, edge(u, v, i), h))
     (if_reach_2#(false(), x, y, edge(u, v, i), h) -> reach#(x, y, i, h), reach#(x, y, edge(u, v, i), h) -> eq#(x, u))
     (reach#(x, y, edge(u, v, i), h) -> eq#(x, u), eq#(s x, s y) -> eq#(x, y))
     (if_reach_2#(false(), x, y, edge(u, v, i), h) -> union#(i, h), union#(edge(x, y, i), h) -> union#(i, h))
     (if_reach_1#(true(), x, y, edge(u, v, i), h) -> eq#(y, v), eq#(s x, s y) -> eq#(x, y))
     (if_reach_1#(false(), x, y, edge(u, v, i), h) -> reach#(x, y, i, edge(u, v, h)), reach#(x, y, edge(u, v, i), h) -> eq#(x, u))
     (if_reach_1#(false(), x, y, edge(u, v, i), h) -> reach#(x, y, i, edge(u, v, h)), reach#(x, y, edge(u, v, i), h) -> if_reach_1#(eq(x, u), x, y, edge(u, v, i), h))
     (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) -> eq#(y, v))
     (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))
     (reach#(x, y, edge(u, v, i), h) -> if_reach_1#(eq(x, u), 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)))
     (eq#(s x, s y) -> eq#(x, y), eq#(s x, s y) -> eq#(x, y))}
    STATUS:
     arrows: 0.851240
     SCCS (3):
      Scc:
       {              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#(false(), x, y, edge(u, v, i), h) -> reach#(x, y, i, h),
        if_reach_2#(false(), x, y, edge(u, v, i), h) -> reach#(v, y, union(i, h), empty())}
      Scc:
       {union#(edge(x, y, i), h) -> union#(i, h)}
      Scc:
       {eq#(s x, s y) -> eq#(x, y)}
      
      SCC (5):
       Strict:
        {              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#(false(), x, y, edge(u, v, i), h) -> reach#(x, y, i, h),
         if_reach_2#(false(), x, y, edge(u, v, i), h) -> reach#(v, y, union(i, h), empty())}
       Weak:
       {                               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()))}
       Open
      
      
      SCC (1):
       Strict:
        {union#(edge(x, y, i), h) -> union#(i, h)}
       Weak:
       {                               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()))}
       Open
      
      
      SCC (1):
       Strict:
        {eq#(s x, s y) -> eq#(x, y)}
       Weak:
       {                               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()))}
       Open