MAYBE
Time: 0.009716
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)),
                       isEmpty empty() -> true(),
                 isEmpty edge(x, y, i) -> false(),
                    from edge(x, y, i) -> x,
                      to edge(x, y, i) -> y,
                          rest empty() -> empty(),
                    rest edge(x, y, i) -> i,
   if1(true(), b1, b2, b3, x, y, i, h) -> true(),
  if1(false(), b1, b2, b3, x, y, i, h) -> if2(b1, b2, b3, x, y, i, h),
                     reach(x, y, i, h) -> if1(eq(x, y), isEmpty i, eq(x, from i), eq(y, to i), x, y, i, h),
       if2(true(), b2, b3, x, y, i, h) -> false(),
      if2(false(), b2, b3, x, y, i, h) -> if3(b2, b3, x, y, i, h),
           if3(true(), b3, x, y, i, h) -> if4(b3, x, y, i, h),
          if3(false(), b3, x, y, i, h) -> reach(x, y, rest i, edge(from i, to i, h)),
               if4(true(), x, y, i, h) -> true(),
              if4(false(), x, y, i, h) -> or(reach(x, y, rest i, h), reach(to i, y, union(rest i, h), empty()))}
 DP:
  DP:
   {                        eq#(s x, s y) -> eq#(x, y),
                 union#(edge(x, y, i), h) -> union#(i, h),
    if1#(false(), b1, b2, b3, x, y, i, h) -> if2#(b1, b2, b3, x, y, i, h),
                       reach#(x, y, i, h) -> eq#(x, y),
                       reach#(x, y, i, h) -> eq#(x, from i),
                       reach#(x, y, i, h) -> eq#(y, to i),
                       reach#(x, y, i, h) -> isEmpty# i,
                       reach#(x, y, i, h) -> from# i,
                       reach#(x, y, i, h) -> to# i,
                       reach#(x, y, i, h) -> if1#(eq(x, y), isEmpty i, eq(x, from i), eq(y, to i), x, y, i, h),
        if2#(false(), b2, b3, x, y, i, h) -> if3#(b2, b3, x, y, i, h),
             if3#(true(), b3, x, y, i, h) -> if4#(b3, x, y, i, h),
            if3#(false(), b3, x, y, i, h) -> from# i,
            if3#(false(), b3, x, y, i, h) -> to# i,
            if3#(false(), b3, x, y, i, h) -> rest# i,
            if3#(false(), b3, x, y, i, h) -> reach#(x, y, rest i, edge(from i, to i, h)),
                if4#(false(), x, y, i, h) -> or#(reach(x, y, rest i, h), reach(to i, y, union(rest i, h), empty())),
                if4#(false(), x, y, i, h) -> union#(rest i, h),
                if4#(false(), x, y, i, h) -> to# i,
                if4#(false(), x, y, i, h) -> rest# i,
                if4#(false(), x, y, i, h) -> reach#(x, y, rest i, h),
                if4#(false(), x, y, i, h) -> reach#(to i, y, union(rest 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)),
                        isEmpty empty() -> true(),
                  isEmpty edge(x, y, i) -> false(),
                     from edge(x, y, i) -> x,
                       to edge(x, y, i) -> y,
                           rest empty() -> empty(),
                     rest edge(x, y, i) -> i,
    if1(true(), b1, b2, b3, x, y, i, h) -> true(),
   if1(false(), b1, b2, b3, x, y, i, h) -> if2(b1, b2, b3, x, y, i, h),
                      reach(x, y, i, h) -> if1(eq(x, y), isEmpty i, eq(x, from i), eq(y, to i), x, y, i, h),
        if2(true(), b2, b3, x, y, i, h) -> false(),
       if2(false(), b2, b3, x, y, i, h) -> if3(b2, b3, x, y, i, h),
            if3(true(), b3, x, y, i, h) -> if4(b3, x, y, i, h),
           if3(false(), b3, x, y, i, h) -> reach(x, y, rest i, edge(from i, to i, h)),
                if4(true(), x, y, i, h) -> true(),
               if4(false(), x, y, i, h) -> or(reach(x, y, rest i, h), reach(to i, y, union(rest i, h), empty()))}
  EDG:
   {(union#(edge(x, y, i), h) -> union#(i, h), union#(edge(x, y, i), h) -> union#(i, h))
    (reach#(x, y, i, h) -> eq#(y, to i), eq#(s x, s y) -> eq#(x, y))
    (reach#(x, y, i, h) -> eq#(x, y), eq#(s x, s y) -> eq#(x, y))
    (reach#(x, y, i, h) -> if1#(eq(x, y), isEmpty i, eq(x, from i), eq(y, to i), x, y, i, h), if1#(false(), b1, b2, b3, x, y, i, h) -> if2#(b1, b2, b3, x, y, i, h))
    (if3#(true(), b3, x, y, i, h) -> if4#(b3, x, y, i, h), if4#(false(), x, y, i, h) -> reach#(to i, y, union(rest i, h), empty()))
    (if3#(true(), b3, x, y, i, h) -> if4#(b3, x, y, i, h), if4#(false(), x, y, i, h) -> reach#(x, y, rest i, h))
    (if3#(true(), b3, x, y, i, h) -> if4#(b3, x, y, i, h), if4#(false(), x, y, i, h) -> rest# i)
    (if3#(true(), b3, x, y, i, h) -> if4#(b3, x, y, i, h), if4#(false(), x, y, i, h) -> to# i)
    (if3#(true(), b3, x, y, i, h) -> if4#(b3, x, y, i, h), if4#(false(), x, y, i, h) -> union#(rest i, h))
    (if3#(true(), b3, x, y, i, h) -> if4#(b3, x, y, i, h), if4#(false(), x, y, i, h) -> or#(reach(x, y, rest i, h), reach(to i, y, union(rest i, h), empty())))
    (if4#(false(), x, y, i, h) -> reach#(to i, y, union(rest i, h), empty()), reach#(x, y, i, h) -> if1#(eq(x, y), isEmpty i, eq(x, from i), eq(y, to i), x, y, i, h))
    (if4#(false(), x, y, i, h) -> reach#(to i, y, union(rest i, h), empty()), reach#(x, y, i, h) -> to# i)
    (if4#(false(), x, y, i, h) -> reach#(to i, y, union(rest i, h), empty()), reach#(x, y, i, h) -> from# i)
    (if4#(false(), x, y, i, h) -> reach#(to i, y, union(rest i, h), empty()), reach#(x, y, i, h) -> isEmpty# i)
    (if4#(false(), x, y, i, h) -> reach#(to i, y, union(rest i, h), empty()), reach#(x, y, i, h) -> eq#(y, to i))
    (if4#(false(), x, y, i, h) -> reach#(to i, y, union(rest i, h), empty()), reach#(x, y, i, h) -> eq#(x, from i))
    (if4#(false(), x, y, i, h) -> reach#(to i, y, union(rest i, h), empty()), reach#(x, y, i, h) -> eq#(x, y))
    (if4#(false(), x, y, i, h) -> union#(rest i, h), union#(edge(x, y, i), h) -> union#(i, h))
    (if4#(false(), x, y, i, h) -> reach#(x, y, rest i, h), reach#(x, y, i, h) -> eq#(x, y))
    (if4#(false(), x, y, i, h) -> reach#(x, y, rest i, h), reach#(x, y, i, h) -> eq#(x, from i))
    (if4#(false(), x, y, i, h) -> reach#(x, y, rest i, h), reach#(x, y, i, h) -> eq#(y, to i))
    (if4#(false(), x, y, i, h) -> reach#(x, y, rest i, h), reach#(x, y, i, h) -> isEmpty# i)
    (if4#(false(), x, y, i, h) -> reach#(x, y, rest i, h), reach#(x, y, i, h) -> from# i)
    (if4#(false(), x, y, i, h) -> reach#(x, y, rest i, h), reach#(x, y, i, h) -> to# i)
    (if4#(false(), x, y, i, h) -> reach#(x, y, rest i, h), reach#(x, y, i, h) -> if1#(eq(x, y), isEmpty i, eq(x, from i), eq(y, to i), x, y, i, h))
    (if3#(false(), b3, x, y, i, h) -> reach#(x, y, rest i, edge(from i, to i, h)), reach#(x, y, i, h) -> eq#(x, y))
    (if3#(false(), b3, x, y, i, h) -> reach#(x, y, rest i, edge(from i, to i, h)), reach#(x, y, i, h) -> eq#(x, from i))
    (if3#(false(), b3, x, y, i, h) -> reach#(x, y, rest i, edge(from i, to i, h)), reach#(x, y, i, h) -> eq#(y, to i))
    (if3#(false(), b3, x, y, i, h) -> reach#(x, y, rest i, edge(from i, to i, h)), reach#(x, y, i, h) -> isEmpty# i)
    (if3#(false(), b3, x, y, i, h) -> reach#(x, y, rest i, edge(from i, to i, h)), reach#(x, y, i, h) -> from# i)
    (if3#(false(), b3, x, y, i, h) -> reach#(x, y, rest i, edge(from i, to i, h)), reach#(x, y, i, h) -> to# i)
    (if3#(false(), b3, x, y, i, h) -> reach#(x, y, rest i, edge(from i, to i, h)), reach#(x, y, i, h) -> if1#(eq(x, y), isEmpty i, eq(x, from i), eq(y, to i), x, y, i, h))
    (if2#(false(), b2, b3, x, y, i, h) -> if3#(b2, b3, x, y, i, h), if3#(true(), b3, x, y, i, h) -> if4#(b3, x, y, i, h))
    (if2#(false(), b2, b3, x, y, i, h) -> if3#(b2, b3, x, y, i, h), if3#(false(), b3, x, y, i, h) -> from# i)
    (if2#(false(), b2, b3, x, y, i, h) -> if3#(b2, b3, x, y, i, h), if3#(false(), b3, x, y, i, h) -> to# i)
    (if2#(false(), b2, b3, x, y, i, h) -> if3#(b2, b3, x, y, i, h), if3#(false(), b3, x, y, i, h) -> rest# i)
    (if2#(false(), b2, b3, x, y, i, h) -> if3#(b2, b3, x, y, i, h), if3#(false(), b3, x, y, i, h) -> reach#(x, y, rest i, edge(from i, to i, h)))
    (if1#(false(), b1, b2, b3, x, y, i, h) -> if2#(b1, b2, b3, x, y, i, h), if2#(false(), b2, b3, x, y, i, h) -> if3#(b2, b3, x, y, i, h))
    (eq#(s x, s y) -> eq#(x, y), eq#(s x, s y) -> eq#(x, y))
    (reach#(x, y, i, h) -> eq#(x, from i), eq#(s x, s y) -> eq#(x, y))}
   STATUS:
    arrows: 0.917355
    SCCS (3):
     Scc:
      {if1#(false(), b1, b2, b3, x, y, i, h) -> if2#(b1, b2, b3, x, y, i, h),
                          reach#(x, y, i, h) -> if1#(eq(x, y), isEmpty i, eq(x, from i), eq(y, to i), x, y, i, h),
           if2#(false(), b2, b3, x, y, i, h) -> if3#(b2, b3, x, y, i, h),
                if3#(true(), b3, x, y, i, h) -> if4#(b3, x, y, i, h),
               if3#(false(), b3, x, y, i, h) -> reach#(x, y, rest i, edge(from i, to i, h)),
                   if4#(false(), x, y, i, h) -> reach#(x, y, rest i, h),
                   if4#(false(), x, y, i, h) -> reach#(to i, y, union(rest i, h), empty())}
     Scc:
      {eq#(s x, s y) -> eq#(x, y)}
     Scc:
      {union#(edge(x, y, i), h) -> union#(i, h)}
     
     SCC (7):
      Strict:
       {if1#(false(), b1, b2, b3, x, y, i, h) -> if2#(b1, b2, b3, x, y, i, h),
                           reach#(x, y, i, h) -> if1#(eq(x, y), isEmpty i, eq(x, from i), eq(y, to i), x, y, i, h),
            if2#(false(), b2, b3, x, y, i, h) -> if3#(b2, b3, x, y, i, h),
                 if3#(true(), b3, x, y, i, h) -> if4#(b3, x, y, i, h),
                if3#(false(), b3, x, y, i, h) -> reach#(x, y, rest i, edge(from i, to i, h)),
                    if4#(false(), x, y, i, h) -> reach#(x, y, rest i, h),
                    if4#(false(), x, y, i, h) -> reach#(to i, y, union(rest 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)),
                            isEmpty empty() -> true(),
                      isEmpty edge(x, y, i) -> false(),
                         from edge(x, y, i) -> x,
                           to edge(x, y, i) -> y,
                               rest empty() -> empty(),
                         rest edge(x, y, i) -> i,
        if1(true(), b1, b2, b3, x, y, i, h) -> true(),
       if1(false(), b1, b2, b3, x, y, i, h) -> if2(b1, b2, b3, x, y, i, h),
                          reach(x, y, i, h) -> if1(eq(x, y), isEmpty i, eq(x, from i), eq(y, to i), x, y, i, h),
            if2(true(), b2, b3, x, y, i, h) -> false(),
           if2(false(), b2, b3, x, y, i, h) -> if3(b2, b3, x, y, i, h),
                if3(true(), b3, x, y, i, h) -> if4(b3, x, y, i, h),
               if3(false(), b3, x, y, i, h) -> reach(x, y, rest i, edge(from i, to i, h)),
                    if4(true(), x, y, i, h) -> true(),
                   if4(false(), x, y, i, h) -> or(reach(x, y, rest i, h), reach(to i, y, union(rest 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)),
                            isEmpty empty() -> true(),
                      isEmpty edge(x, y, i) -> false(),
                         from edge(x, y, i) -> x,
                           to edge(x, y, i) -> y,
                               rest empty() -> empty(),
                         rest edge(x, y, i) -> i,
        if1(true(), b1, b2, b3, x, y, i, h) -> true(),
       if1(false(), b1, b2, b3, x, y, i, h) -> if2(b1, b2, b3, x, y, i, h),
                          reach(x, y, i, h) -> if1(eq(x, y), isEmpty i, eq(x, from i), eq(y, to i), x, y, i, h),
            if2(true(), b2, b3, x, y, i, h) -> false(),
           if2(false(), b2, b3, x, y, i, h) -> if3(b2, b3, x, y, i, h),
                if3(true(), b3, x, y, i, h) -> if4(b3, x, y, i, h),
               if3(false(), b3, x, y, i, h) -> reach(x, y, rest i, edge(from i, to i, h)),
                    if4(true(), x, y, i, h) -> true(),
                   if4(false(), x, y, i, h) -> or(reach(x, y, rest i, h), reach(to i, y, union(rest 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)),
                            isEmpty empty() -> true(),
                      isEmpty edge(x, y, i) -> false(),
                         from edge(x, y, i) -> x,
                           to edge(x, y, i) -> y,
                               rest empty() -> empty(),
                         rest edge(x, y, i) -> i,
        if1(true(), b1, b2, b3, x, y, i, h) -> true(),
       if1(false(), b1, b2, b3, x, y, i, h) -> if2(b1, b2, b3, x, y, i, h),
                          reach(x, y, i, h) -> if1(eq(x, y), isEmpty i, eq(x, from i), eq(y, to i), x, y, i, h),
            if2(true(), b2, b3, x, y, i, h) -> false(),
           if2(false(), b2, b3, x, y, i, h) -> if3(b2, b3, x, y, i, h),
                if3(true(), b3, x, y, i, h) -> if4(b3, x, y, i, h),
               if3(false(), b3, x, y, i, h) -> reach(x, y, rest i, edge(from i, to i, h)),
                    if4(true(), x, y, i, h) -> true(),
                   if4(false(), x, y, i, h) -> or(reach(x, y, rest i, h), reach(to i, y, union(rest i, h), empty()))}
      Open