MAYBE
Time: 0.015294
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,
                          and(true(), y) -> y,
                         and(false(), y) -> false(),
                            size empty() -> 0(),
                      size edge(x, y, i) -> s size i,
                              le(0(), y) -> true(),
                            le(s x, 0()) -> false(),
                            le(s x, s y) -> le(x, y),
                    reach(x, y, c, i, j) -> if1(eq(x, y), x, y, c, i, j),
                      reachable(x, y, i) -> reach(x, y, 0(), i, i),
              if1(true(), x, y, c, i, j) -> true(),
             if1(false(), x, y, c, i, j) -> if2(le(c, size j), x, y, c, i, j),
        if2(true(), x, y, c, empty(), j) -> false(),
  if2(true(), x, y, c, edge(u, v, i), j) -> or(if2(true(), x, y, c, i, j), and(eq(x, u), reach(v, y, s c, j, j))),
             if2(false(), x, y, c, i, j) -> false()}
 DP:
  DP:
   {                          eq#(s x, s y) -> eq#(x, y),
                        size# edge(x, y, i) -> size# i,
                              le#(s x, s y) -> le#(x, y),
                      reach#(x, y, c, i, j) -> eq#(x, y),
                      reach#(x, y, c, i, j) -> if1#(eq(x, y), x, y, c, i, j),
                        reachable#(x, y, i) -> reach#(x, y, 0(), i, i),
               if1#(false(), x, y, c, i, j) -> size# j,
               if1#(false(), x, y, c, i, j) -> le#(c, size j),
               if1#(false(), x, y, c, i, j) -> if2#(le(c, size j), x, y, c, i, j),
    if2#(true(), x, y, c, edge(u, v, i), j) -> eq#(x, u),
    if2#(true(), x, y, c, edge(u, v, i), j) -> or#(if2(true(), x, y, c, i, j), and(eq(x, u), reach(v, y, s c, j, j))),
    if2#(true(), x, y, c, edge(u, v, i), j) -> and#(eq(x, u), reach(v, y, s c, j, j)),
    if2#(true(), x, y, c, edge(u, v, i), j) -> reach#(v, y, s c, j, j),
    if2#(true(), x, y, c, edge(u, v, i), j) -> if2#(true(), x, y, c, i, j)}
  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,
                           and(true(), y) -> y,
                          and(false(), y) -> false(),
                             size empty() -> 0(),
                       size edge(x, y, i) -> s size i,
                               le(0(), y) -> true(),
                             le(s x, 0()) -> false(),
                             le(s x, s y) -> le(x, y),
                     reach(x, y, c, i, j) -> if1(eq(x, y), x, y, c, i, j),
                       reachable(x, y, i) -> reach(x, y, 0(), i, i),
               if1(true(), x, y, c, i, j) -> true(),
              if1(false(), x, y, c, i, j) -> if2(le(c, size j), x, y, c, i, j),
         if2(true(), x, y, c, empty(), j) -> false(),
   if2(true(), x, y, c, edge(u, v, i), j) -> or(if2(true(), x, y, c, i, j), and(eq(x, u), reach(v, y, s c, j, j))),
              if2(false(), x, y, c, i, j) -> false()}
  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,
                            and(true(), y) -> y,
                           and(false(), y) -> false(),
                              size empty() -> 0(),
                        size edge(x, y, i) -> s size i,
                                le(0(), y) -> true(),
                              le(s x, 0()) -> false(),
                              le(s x, s y) -> le(x, y),
                      reach(x, y, c, i, j) -> if1(eq(x, y), x, y, c, i, j),
                if1(true(), x, y, c, i, j) -> true(),
               if1(false(), x, y, c, i, j) -> if2(le(c, size j), x, y, c, i, j),
          if2(true(), x, y, c, empty(), j) -> false(),
    if2(true(), x, y, c, edge(u, v, i), j) -> or(if2(true(), x, y, c, i, j), and(eq(x, u), reach(v, y, s c, j, j))),
               if2(false(), x, y, c, i, j) -> false(),
                                   a(z, w) -> z,
                                   a(z, w) -> w}
   EDG:
    {(if2#(true(), x, y, c, edge(u, v, i), j) -> reach#(v, y, s c, j, j), reach#(x, y, c, i, j) -> if1#(eq(x, y), x, y, c, i, j))
     (if2#(true(), x, y, c, edge(u, v, i), j) -> reach#(v, y, s c, j, j), reach#(x, y, c, i, j) -> eq#(x, y))
     (le#(s x, s y) -> le#(x, y), le#(s x, s y) -> le#(x, y))
     (size# edge(x, y, i) -> size# i, size# edge(x, y, i) -> size# i)
     (reach#(x, y, c, i, j) -> if1#(eq(x, y), x, y, c, i, j), if1#(false(), x, y, c, i, j) -> if2#(le(c, size j), x, y, c, i, j))
     (reach#(x, y, c, i, j) -> if1#(eq(x, y), x, y, c, i, j), if1#(false(), x, y, c, i, j) -> le#(c, size j))
     (reach#(x, y, c, i, j) -> if1#(eq(x, y), x, y, c, i, j), if1#(false(), x, y, c, i, j) -> size# j)
     (if2#(true(), x, y, c, edge(u, v, i), j) -> if2#(true(), x, y, c, i, j), if2#(true(), x, y, c, edge(u, v, i), j) -> if2#(true(), x, y, c, i, j))
     (if2#(true(), x, y, c, edge(u, v, i), j) -> if2#(true(), x, y, c, i, j), if2#(true(), x, y, c, edge(u, v, i), j) -> reach#(v, y, s c, j, j))
     (if2#(true(), x, y, c, edge(u, v, i), j) -> if2#(true(), x, y, c, i, j), if2#(true(), x, y, c, edge(u, v, i), j) -> and#(eq(x, u), reach(v, y, s c, j, j)))
     (if2#(true(), x, y, c, edge(u, v, i), j) -> if2#(true(), x, y, c, i, j), if2#(true(), x, y, c, edge(u, v, i), j) -> or#(if2(true(), x, y, c, i, j), and(eq(x, u), reach(v, y, s c, j, j))))
     (if2#(true(), x, y, c, edge(u, v, i), j) -> if2#(true(), x, y, c, i, j), if2#(true(), x, y, c, edge(u, v, i), j) -> eq#(x, u))
     (if1#(false(), x, y, c, i, j) -> if2#(le(c, size j), x, y, c, i, j), if2#(true(), x, y, c, edge(u, v, i), j) -> eq#(x, u))
     (if1#(false(), x, y, c, i, j) -> if2#(le(c, size j), x, y, c, i, j), if2#(true(), x, y, c, edge(u, v, i), j) -> or#(if2(true(), x, y, c, i, j), and(eq(x, u), reach(v, y, s c, j, j))))
     (if1#(false(), x, y, c, i, j) -> if2#(le(c, size j), x, y, c, i, j), if2#(true(), x, y, c, edge(u, v, i), j) -> and#(eq(x, u), reach(v, y, s c, j, j)))
     (if1#(false(), x, y, c, i, j) -> if2#(le(c, size j), x, y, c, i, j), if2#(true(), x, y, c, edge(u, v, i), j) -> reach#(v, y, s c, j, j))
     (if1#(false(), x, y, c, i, j) -> if2#(le(c, size j), x, y, c, i, j), if2#(true(), x, y, c, edge(u, v, i), j) -> if2#(true(), x, y, c, i, j))
     (if2#(true(), x, y, c, edge(u, v, i), j) -> eq#(x, u), eq#(s x, s y) -> eq#(x, y))
     (if1#(false(), x, y, c, i, j) -> le#(c, size j), le#(s x, s y) -> le#(x, y))
     (if1#(false(), x, y, c, i, j) -> size# j, size# edge(x, y, i) -> size# i)
     (reach#(x, y, c, i, j) -> eq#(x, y), eq#(s x, s y) -> eq#(x, y))
     (eq#(s x, s y) -> eq#(x, y), eq#(s x, s y) -> eq#(x, y))
     (reachable#(x, y, i) -> reach#(x, y, 0(), i, i), reach#(x, y, c, i, j) -> eq#(x, y))
     (reachable#(x, y, i) -> reach#(x, y, 0(), i, i), reach#(x, y, c, i, j) -> if1#(eq(x, y), x, y, c, i, j))}
    EDG:
     {(if2#(true(), x, y, c, edge(u, v, i), j) -> reach#(v, y, s c, j, j), reach#(x, y, c, i, j) -> if1#(eq(x, y), x, y, c, i, j))
      (if2#(true(), x, y, c, edge(u, v, i), j) -> reach#(v, y, s c, j, j), reach#(x, y, c, i, j) -> eq#(x, y))
      (le#(s x, s y) -> le#(x, y), le#(s x, s y) -> le#(x, y))
      (size# edge(x, y, i) -> size# i, size# edge(x, y, i) -> size# i)
      (reach#(x, y, c, i, j) -> if1#(eq(x, y), x, y, c, i, j), if1#(false(), x, y, c, i, j) -> if2#(le(c, size j), x, y, c, i, j))
      (reach#(x, y, c, i, j) -> if1#(eq(x, y), x, y, c, i, j), if1#(false(), x, y, c, i, j) -> le#(c, size j))
      (reach#(x, y, c, i, j) -> if1#(eq(x, y), x, y, c, i, j), if1#(false(), x, y, c, i, j) -> size# j)
      (if2#(true(), x, y, c, edge(u, v, i), j) -> if2#(true(), x, y, c, i, j), if2#(true(), x, y, c, edge(u, v, i), j) -> if2#(true(), x, y, c, i, j))
      (if2#(true(), x, y, c, edge(u, v, i), j) -> if2#(true(), x, y, c, i, j), if2#(true(), x, y, c, edge(u, v, i), j) -> reach#(v, y, s c, j, j))
      (if2#(true(), x, y, c, edge(u, v, i), j) -> if2#(true(), x, y, c, i, j), if2#(true(), x, y, c, edge(u, v, i), j) -> and#(eq(x, u), reach(v, y, s c, j, j)))
      (if2#(true(), x, y, c, edge(u, v, i), j) -> if2#(true(), x, y, c, i, j), if2#(true(), x, y, c, edge(u, v, i), j) -> or#(if2(true(), x, y, c, i, j), and(eq(x, u), reach(v, y, s c, j, j))))
      (if2#(true(), x, y, c, edge(u, v, i), j) -> if2#(true(), x, y, c, i, j), if2#(true(), x, y, c, edge(u, v, i), j) -> eq#(x, u))
      (if1#(false(), x, y, c, i, j) -> if2#(le(c, size j), x, y, c, i, j), if2#(true(), x, y, c, edge(u, v, i), j) -> eq#(x, u))
      (if1#(false(), x, y, c, i, j) -> if2#(le(c, size j), x, y, c, i, j), if2#(true(), x, y, c, edge(u, v, i), j) -> or#(if2(true(), x, y, c, i, j), and(eq(x, u), reach(v, y, s c, j, j))))
      (if1#(false(), x, y, c, i, j) -> if2#(le(c, size j), x, y, c, i, j), if2#(true(), x, y, c, edge(u, v, i), j) -> and#(eq(x, u), reach(v, y, s c, j, j)))
      (if1#(false(), x, y, c, i, j) -> if2#(le(c, size j), x, y, c, i, j), if2#(true(), x, y, c, edge(u, v, i), j) -> reach#(v, y, s c, j, j))
      (if1#(false(), x, y, c, i, j) -> if2#(le(c, size j), x, y, c, i, j), if2#(true(), x, y, c, edge(u, v, i), j) -> if2#(true(), x, y, c, i, j))
      (if2#(true(), x, y, c, edge(u, v, i), j) -> eq#(x, u), eq#(s x, s y) -> eq#(x, y))
      (if1#(false(), x, y, c, i, j) -> le#(c, size j), le#(s x, s y) -> le#(x, y))
      (if1#(false(), x, y, c, i, j) -> size# j, size# edge(x, y, i) -> size# i)
      (reach#(x, y, c, i, j) -> eq#(x, y), eq#(s x, s y) -> eq#(x, y))
      (eq#(s x, s y) -> eq#(x, y), eq#(s x, s y) -> eq#(x, y))
      (reachable#(x, y, i) -> reach#(x, y, 0(), i, i), reach#(x, y, c, i, j) -> eq#(x, y))
      (reachable#(x, y, i) -> reach#(x, y, 0(), i, i), reach#(x, y, c, i, j) -> if1#(eq(x, y), x, y, c, i, j))}
     EDG:
      {(if2#(true(), x, y, c, edge(u, v, i), j) -> reach#(v, y, s c, j, j), reach#(x, y, c, i, j) -> if1#(eq(x, y), x, y, c, i, j))
       (if2#(true(), x, y, c, edge(u, v, i), j) -> reach#(v, y, s c, j, j), reach#(x, y, c, i, j) -> eq#(x, y))
       (le#(s x, s y) -> le#(x, y), le#(s x, s y) -> le#(x, y))
       (size# edge(x, y, i) -> size# i, size# edge(x, y, i) -> size# i)
       (reach#(x, y, c, i, j) -> if1#(eq(x, y), x, y, c, i, j), if1#(false(), x, y, c, i, j) -> if2#(le(c, size j), x, y, c, i, j))
       (reach#(x, y, c, i, j) -> if1#(eq(x, y), x, y, c, i, j), if1#(false(), x, y, c, i, j) -> le#(c, size j))
       (reach#(x, y, c, i, j) -> if1#(eq(x, y), x, y, c, i, j), if1#(false(), x, y, c, i, j) -> size# j)
       (if2#(true(), x, y, c, edge(u, v, i), j) -> if2#(true(), x, y, c, i, j), if2#(true(), x, y, c, edge(u, v, i), j) -> if2#(true(), x, y, c, i, j))
       (if2#(true(), x, y, c, edge(u, v, i), j) -> if2#(true(), x, y, c, i, j), if2#(true(), x, y, c, edge(u, v, i), j) -> reach#(v, y, s c, j, j))
       (if2#(true(), x, y, c, edge(u, v, i), j) -> if2#(true(), x, y, c, i, j), if2#(true(), x, y, c, edge(u, v, i), j) -> and#(eq(x, u), reach(v, y, s c, j, j)))
       (if2#(true(), x, y, c, edge(u, v, i), j) -> if2#(true(), x, y, c, i, j), if2#(true(), x, y, c, edge(u, v, i), j) -> or#(if2(true(), x, y, c, i, j), and(eq(x, u), reach(v, y, s c, j, j))))
       (if2#(true(), x, y, c, edge(u, v, i), j) -> if2#(true(), x, y, c, i, j), if2#(true(), x, y, c, edge(u, v, i), j) -> eq#(x, u))
       (if1#(false(), x, y, c, i, j) -> if2#(le(c, size j), x, y, c, i, j), if2#(true(), x, y, c, edge(u, v, i), j) -> eq#(x, u))
       (if1#(false(), x, y, c, i, j) -> if2#(le(c, size j), x, y, c, i, j), if2#(true(), x, y, c, edge(u, v, i), j) -> or#(if2(true(), x, y, c, i, j), and(eq(x, u), reach(v, y, s c, j, j))))
       (if1#(false(), x, y, c, i, j) -> if2#(le(c, size j), x, y, c, i, j), if2#(true(), x, y, c, edge(u, v, i), j) -> and#(eq(x, u), reach(v, y, s c, j, j)))
       (if1#(false(), x, y, c, i, j) -> if2#(le(c, size j), x, y, c, i, j), if2#(true(), x, y, c, edge(u, v, i), j) -> reach#(v, y, s c, j, j))
       (if1#(false(), x, y, c, i, j) -> if2#(le(c, size j), x, y, c, i, j), if2#(true(), x, y, c, edge(u, v, i), j) -> if2#(true(), x, y, c, i, j))
       (if2#(true(), x, y, c, edge(u, v, i), j) -> eq#(x, u), eq#(s x, s y) -> eq#(x, y))
       (if1#(false(), x, y, c, i, j) -> le#(c, size j), le#(s x, s y) -> le#(x, y))
       (if1#(false(), x, y, c, i, j) -> size# j, size# edge(x, y, i) -> size# i)
       (reach#(x, y, c, i, j) -> eq#(x, y), eq#(s x, s y) -> eq#(x, y))
       (eq#(s x, s y) -> eq#(x, y), eq#(s x, s y) -> eq#(x, y))
       (reachable#(x, y, i) -> reach#(x, y, 0(), i, i), reach#(x, y, c, i, j) -> eq#(x, y))
       (reachable#(x, y, i) -> reach#(x, y, 0(), i, i), reach#(x, y, c, i, j) -> if1#(eq(x, y), x, y, c, i, j))}
      EDG:
       {(if2#(true(), x, y, c, edge(u, v, i), j) -> reach#(v, y, s c, j, j), reach#(x, y, c, i, j) -> if1#(eq(x, y), x, y, c, i, j))
        (if2#(true(), x, y, c, edge(u, v, i), j) -> reach#(v, y, s c, j, j), reach#(x, y, c, i, j) -> eq#(x, y))
        (le#(s x, s y) -> le#(x, y), le#(s x, s y) -> le#(x, y))
        (size# edge(x, y, i) -> size# i, size# edge(x, y, i) -> size# i)
        (reach#(x, y, c, i, j) -> if1#(eq(x, y), x, y, c, i, j), if1#(false(), x, y, c, i, j) -> if2#(le(c, size j), x, y, c, i, j))
        (reach#(x, y, c, i, j) -> if1#(eq(x, y), x, y, c, i, j), if1#(false(), x, y, c, i, j) -> le#(c, size j))
        (reach#(x, y, c, i, j) -> if1#(eq(x, y), x, y, c, i, j), if1#(false(), x, y, c, i, j) -> size# j)
        (if2#(true(), x, y, c, edge(u, v, i), j) -> if2#(true(), x, y, c, i, j), if2#(true(), x, y, c, edge(u, v, i), j) -> if2#(true(), x, y, c, i, j))
        (if2#(true(), x, y, c, edge(u, v, i), j) -> if2#(true(), x, y, c, i, j), if2#(true(), x, y, c, edge(u, v, i), j) -> reach#(v, y, s c, j, j))
        (if2#(true(), x, y, c, edge(u, v, i), j) -> if2#(true(), x, y, c, i, j), if2#(true(), x, y, c, edge(u, v, i), j) -> and#(eq(x, u), reach(v, y, s c, j, j)))
        (if2#(true(), x, y, c, edge(u, v, i), j) -> if2#(true(), x, y, c, i, j), if2#(true(), x, y, c, edge(u, v, i), j) -> or#(if2(true(), x, y, c, i, j), and(eq(x, u), reach(v, y, s c, j, j))))
        (if2#(true(), x, y, c, edge(u, v, i), j) -> if2#(true(), x, y, c, i, j), if2#(true(), x, y, c, edge(u, v, i), j) -> eq#(x, u))
        (if1#(false(), x, y, c, i, j) -> if2#(le(c, size j), x, y, c, i, j), if2#(true(), x, y, c, edge(u, v, i), j) -> eq#(x, u))
        (if1#(false(), x, y, c, i, j) -> if2#(le(c, size j), x, y, c, i, j), if2#(true(), x, y, c, edge(u, v, i), j) -> or#(if2(true(), x, y, c, i, j), and(eq(x, u), reach(v, y, s c, j, j))))
        (if1#(false(), x, y, c, i, j) -> if2#(le(c, size j), x, y, c, i, j), if2#(true(), x, y, c, edge(u, v, i), j) -> and#(eq(x, u), reach(v, y, s c, j, j)))
        (if1#(false(), x, y, c, i, j) -> if2#(le(c, size j), x, y, c, i, j), if2#(true(), x, y, c, edge(u, v, i), j) -> reach#(v, y, s c, j, j))
        (if1#(false(), x, y, c, i, j) -> if2#(le(c, size j), x, y, c, i, j), if2#(true(), x, y, c, edge(u, v, i), j) -> if2#(true(), x, y, c, i, j))
        (if2#(true(), x, y, c, edge(u, v, i), j) -> eq#(x, u), eq#(s x, s y) -> eq#(x, y))
        (if1#(false(), x, y, c, i, j) -> le#(c, size j), le#(s x, s y) -> le#(x, y))
        (if1#(false(), x, y, c, i, j) -> size# j, size# edge(x, y, i) -> size# i)
        (reach#(x, y, c, i, j) -> eq#(x, y), eq#(s x, s y) -> eq#(x, y))
        (eq#(s x, s y) -> eq#(x, y), eq#(s x, s y) -> eq#(x, y))
        (reachable#(x, y, i) -> reach#(x, y, 0(), i, i), reach#(x, y, c, i, j) -> eq#(x, y))
        (reachable#(x, y, i) -> reach#(x, y, 0(), i, i), reach#(x, y, c, i, j) -> if1#(eq(x, y), x, y, c, i, j))}
       STATUS:
        arrows: 0.877551
        SCCS (4):
         Scc:
          {                  reach#(x, y, c, i, j) -> if1#(eq(x, y), x, y, c, i, j),
                      if1#(false(), x, y, c, i, j) -> if2#(le(c, size j), x, y, c, i, j),
           if2#(true(), x, y, c, edge(u, v, i), j) -> reach#(v, y, s c, j, j),
           if2#(true(), x, y, c, edge(u, v, i), j) -> if2#(true(), x, y, c, i, j)}
         Scc:
          {le#(s x, s y) -> le#(x, y)}
         Scc:
          {size# edge(x, y, i) -> size# i}
         Scc:
          {eq#(s x, s y) -> eq#(x, y)}
         
         
         SCC (4):
          Strict:
           {                  reach#(x, y, c, i, j) -> if1#(eq(x, y), x, y, c, i, j),
                       if1#(false(), x, y, c, i, j) -> if2#(le(c, size j), x, y, c, i, j),
            if2#(true(), x, y, c, edge(u, v, i), j) -> reach#(v, y, s c, j, j),
            if2#(true(), x, y, c, edge(u, v, i), j) -> if2#(true(), x, y, c, i, j)}
          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,
                                   and(true(), y) -> y,
                                  and(false(), y) -> false(),
                                     size empty() -> 0(),
                               size edge(x, y, i) -> s size i,
                                       le(0(), y) -> true(),
                                     le(s x, 0()) -> false(),
                                     le(s x, s y) -> le(x, y),
                             reach(x, y, c, i, j) -> if1(eq(x, y), x, y, c, i, j),
                               reachable(x, y, i) -> reach(x, y, 0(), i, i),
                       if1(true(), x, y, c, i, j) -> true(),
                      if1(false(), x, y, c, i, j) -> if2(le(c, size j), x, y, c, i, j),
                 if2(true(), x, y, c, empty(), j) -> false(),
           if2(true(), x, y, c, edge(u, v, i), j) -> or(if2(true(), x, y, c, i, j), and(eq(x, u), reach(v, y, s c, j, j))),
                      if2(false(), x, y, c, i, j) -> false()}
          Open
         
         
         
         
         SCC (1):
          Strict:
           {le#(s x, s y) -> le#(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,
                                   and(true(), y) -> y,
                                  and(false(), y) -> false(),
                                     size empty() -> 0(),
                               size edge(x, y, i) -> s size i,
                                       le(0(), y) -> true(),
                                     le(s x, 0()) -> false(),
                                     le(s x, s y) -> le(x, y),
                             reach(x, y, c, i, j) -> if1(eq(x, y), x, y, c, i, j),
                               reachable(x, y, i) -> reach(x, y, 0(), i, i),
                       if1(true(), x, y, c, i, j) -> true(),
                      if1(false(), x, y, c, i, j) -> if2(le(c, size j), x, y, c, i, j),
                 if2(true(), x, y, c, empty(), j) -> false(),
           if2(true(), x, y, c, edge(u, v, i), j) -> or(if2(true(), x, y, c, i, j), and(eq(x, u), reach(v, y, s c, j, j))),
                      if2(false(), x, y, c, i, j) -> false()}
          Open
         
         SCC (1):
          Strict:
           {size# edge(x, y, i) -> size# i}
          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,
                                   and(true(), y) -> y,
                                  and(false(), y) -> false(),
                                     size empty() -> 0(),
                               size edge(x, y, i) -> s size i,
                                       le(0(), y) -> true(),
                                     le(s x, 0()) -> false(),
                                     le(s x, s y) -> le(x, y),
                             reach(x, y, c, i, j) -> if1(eq(x, y), x, y, c, i, j),
                               reachable(x, y, i) -> reach(x, y, 0(), i, i),
                       if1(true(), x, y, c, i, j) -> true(),
                      if1(false(), x, y, c, i, j) -> if2(le(c, size j), x, y, c, i, j),
                 if2(true(), x, y, c, empty(), j) -> false(),
           if2(true(), x, y, c, edge(u, v, i), j) -> or(if2(true(), x, y, c, i, j), and(eq(x, u), reach(v, y, s c, j, j))),
                      if2(false(), x, y, c, i, j) -> false()}
          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,
                                   and(true(), y) -> y,
                                  and(false(), y) -> false(),
                                     size empty() -> 0(),
                               size edge(x, y, i) -> s size i,
                                       le(0(), y) -> true(),
                                     le(s x, 0()) -> false(),
                                     le(s x, s y) -> le(x, y),
                             reach(x, y, c, i, j) -> if1(eq(x, y), x, y, c, i, j),
                               reachable(x, y, i) -> reach(x, y, 0(), i, i),
                       if1(true(), x, y, c, i, j) -> true(),
                      if1(false(), x, y, c, i, j) -> if2(le(c, size j), x, y, c, i, j),
                 if2(true(), x, y, c, empty(), j) -> false(),
           if2(true(), x, y, c, edge(u, v, i), j) -> or(if2(true(), x, y, c, i, j), and(eq(x, u), reach(v, y, s c, j, j))),
                      if2(false(), x, y, c, i, j) -> false()}
          Open