MAYBE
Time: 0.010718
TRS:
 {             empty nil() -> true(),
          empty cons(x, y) -> false(),
                tail nil() -> nil(),
           tail cons(x, y) -> y,
           head cons(x, y) -> x,
                  zero 0() -> true(),
                  zero s x -> false(),
                     p 0() -> 0(),
                   p s 0() -> 0(),
                   p s s x -> s p s x,
     if_intlist(true(), x) -> nil(),
    if_intlist(false(), x) -> cons(s head x, intlist tail x),
                 intlist x -> if_intlist(empty x, x),
   if_int(true(), b, x, y) -> if1(b, x, y),
  if_int(false(), b, x, y) -> if2(b, x, y),
                 int(x, y) -> if_int(zero x, zero y, x, y),
         if1(true(), x, y) -> cons(0(), nil()),
        if1(false(), x, y) -> cons(0(), int(s 0(), y)),
         if2(true(), x, y) -> nil(),
        if2(false(), x, y) -> intlist int(p x, p y)}
 DP:
  DP:
   {                 p# s s x -> p# s x,
      if_intlist#(false(), x) -> tail# x,
      if_intlist#(false(), x) -> head# x,
      if_intlist#(false(), x) -> intlist# tail x,
                   intlist# x -> empty# x,
                   intlist# x -> if_intlist#(empty x, x),
     if_int#(true(), b, x, y) -> if1#(b, x, y),
    if_int#(false(), b, x, y) -> if2#(b, x, y),
                   int#(x, y) -> zero# x,
                   int#(x, y) -> zero# y,
                   int#(x, y) -> if_int#(zero x, zero y, x, y),
          if1#(false(), x, y) -> int#(s 0(), y),
          if2#(false(), x, y) -> p# x,
          if2#(false(), x, y) -> p# y,
          if2#(false(), x, y) -> intlist# int(p x, p y),
          if2#(false(), x, y) -> int#(p x, p y)}
  TRS:
  {             empty nil() -> true(),
           empty cons(x, y) -> false(),
                 tail nil() -> nil(),
            tail cons(x, y) -> y,
            head cons(x, y) -> x,
                   zero 0() -> true(),
                   zero s x -> false(),
                      p 0() -> 0(),
                    p s 0() -> 0(),
                    p s s x -> s p s x,
      if_intlist(true(), x) -> nil(),
     if_intlist(false(), x) -> cons(s head x, intlist tail x),
                  intlist x -> if_intlist(empty x, x),
    if_int(true(), b, x, y) -> if1(b, x, y),
   if_int(false(), b, x, y) -> if2(b, x, y),
                  int(x, y) -> if_int(zero x, zero y, x, y),
          if1(true(), x, y) -> cons(0(), nil()),
         if1(false(), x, y) -> cons(0(), int(s 0(), y)),
          if2(true(), x, y) -> nil(),
         if2(false(), x, y) -> intlist int(p x, p y)}
  EDG:
   {(p# s s x -> p# s x, p# s s x -> p# s x)
    (if2#(false(), x, y) -> int#(p x, p y), int#(x, y) -> if_int#(zero x, zero y, x, y))
    (if2#(false(), x, y) -> int#(p x, p y), int#(x, y) -> zero# y)
    (if2#(false(), x, y) -> int#(p x, p y), int#(x, y) -> zero# x)
    (if_int#(false(), b, x, y) -> if2#(b, x, y), if2#(false(), x, y) -> int#(p x, p y))
    (if_int#(false(), b, x, y) -> if2#(b, x, y), if2#(false(), x, y) -> intlist# int(p x, p y))
    (if_int#(false(), b, x, y) -> if2#(b, x, y), if2#(false(), x, y) -> p# y)
    (if_int#(false(), b, x, y) -> if2#(b, x, y), if2#(false(), x, y) -> p# x)
    (int#(x, y) -> if_int#(zero x, zero y, x, y), if_int#(false(), b, x, y) -> if2#(b, x, y))
    (int#(x, y) -> if_int#(zero x, zero y, x, y), if_int#(true(), b, x, y) -> if1#(b, x, y))
    (intlist# x -> if_intlist#(empty x, x), if_intlist#(false(), x) -> intlist# tail x)
    (intlist# x -> if_intlist#(empty x, x), if_intlist#(false(), x) -> head# x)
    (intlist# x -> if_intlist#(empty x, x), if_intlist#(false(), x) -> tail# x)
    (if2#(false(), x, y) -> intlist# int(p x, p y), intlist# x -> empty# x)
    (if2#(false(), x, y) -> intlist# int(p x, p y), intlist# x -> if_intlist#(empty x, x))
    (if1#(false(), x, y) -> int#(s 0(), y), int#(x, y) -> zero# x)
    (if1#(false(), x, y) -> int#(s 0(), y), int#(x, y) -> zero# y)
    (if1#(false(), x, y) -> int#(s 0(), y), int#(x, y) -> if_int#(zero x, zero y, x, y))
    (if_int#(true(), b, x, y) -> if1#(b, x, y), if1#(false(), x, y) -> int#(s 0(), y))
    (if2#(false(), x, y) -> p# y, p# s s x -> p# s x)
    (if_intlist#(false(), x) -> intlist# tail x, intlist# x -> empty# x)
    (if_intlist#(false(), x) -> intlist# tail x, intlist# x -> if_intlist#(empty x, x))
    (if2#(false(), x, y) -> p# x, p# s s x -> p# s x)}
   STATUS:
    arrows: 0.910156
    SCCS (3):
     Scc:
      { if_int#(true(), b, x, y) -> if1#(b, x, y),
       if_int#(false(), b, x, y) -> if2#(b, x, y),
                      int#(x, y) -> if_int#(zero x, zero y, x, y),
             if1#(false(), x, y) -> int#(s 0(), y),
             if2#(false(), x, y) -> int#(p x, p y)}
     Scc:
      {if_intlist#(false(), x) -> intlist# tail x,
                    intlist# x -> if_intlist#(empty x, x)}
     Scc:
      {p# s s x -> p# s x}
     
     SCC (5):
      Strict:
       { if_int#(true(), b, x, y) -> if1#(b, x, y),
        if_int#(false(), b, x, y) -> if2#(b, x, y),
                       int#(x, y) -> if_int#(zero x, zero y, x, y),
              if1#(false(), x, y) -> int#(s 0(), y),
              if2#(false(), x, y) -> int#(p x, p y)}
      Weak:
      {             empty nil() -> true(),
               empty cons(x, y) -> false(),
                     tail nil() -> nil(),
                tail cons(x, y) -> y,
                head cons(x, y) -> x,
                       zero 0() -> true(),
                       zero s x -> false(),
                          p 0() -> 0(),
                        p s 0() -> 0(),
                        p s s x -> s p s x,
          if_intlist(true(), x) -> nil(),
         if_intlist(false(), x) -> cons(s head x, intlist tail x),
                      intlist x -> if_intlist(empty x, x),
        if_int(true(), b, x, y) -> if1(b, x, y),
       if_int(false(), b, x, y) -> if2(b, x, y),
                      int(x, y) -> if_int(zero x, zero y, x, y),
              if1(true(), x, y) -> cons(0(), nil()),
             if1(false(), x, y) -> cons(0(), int(s 0(), y)),
              if2(true(), x, y) -> nil(),
             if2(false(), x, y) -> intlist int(p x, p y)}
      Open
     
     
     
     SCC (2):
      Strict:
       {if_intlist#(false(), x) -> intlist# tail x,
                     intlist# x -> if_intlist#(empty x, x)}
      Weak:
      {             empty nil() -> true(),
               empty cons(x, y) -> false(),
                     tail nil() -> nil(),
                tail cons(x, y) -> y,
                head cons(x, y) -> x,
                       zero 0() -> true(),
                       zero s x -> false(),
                          p 0() -> 0(),
                        p s 0() -> 0(),
                        p s s x -> s p s x,
          if_intlist(true(), x) -> nil(),
         if_intlist(false(), x) -> cons(s head x, intlist tail x),
                      intlist x -> if_intlist(empty x, x),
        if_int(true(), b, x, y) -> if1(b, x, y),
       if_int(false(), b, x, y) -> if2(b, x, y),
                      int(x, y) -> if_int(zero x, zero y, x, y),
              if1(true(), x, y) -> cons(0(), nil()),
             if1(false(), x, y) -> cons(0(), int(s 0(), y)),
              if2(true(), x, y) -> nil(),
             if2(false(), x, y) -> intlist int(p x, p y)}
      Open
     
     SCC (1):
      Strict:
       {p# s s x -> p# s x}
      Weak:
      {             empty nil() -> true(),
               empty cons(x, y) -> false(),
                     tail nil() -> nil(),
                tail cons(x, y) -> y,
                head cons(x, y) -> x,
                       zero 0() -> true(),
                       zero s x -> false(),
                          p 0() -> 0(),
                        p s 0() -> 0(),
                        p s s x -> s p s x,
          if_intlist(true(), x) -> nil(),
         if_intlist(false(), x) -> cons(s head x, intlist tail x),
                      intlist x -> if_intlist(empty x, x),
        if_int(true(), b, x, y) -> if1(b, x, y),
       if_int(false(), b, x, y) -> if2(b, x, y),
                      int(x, y) -> if_int(zero x, zero y, x, y),
              if1(true(), x, y) -> cons(0(), nil()),
             if1(false(), x, y) -> cons(0(), int(s 0(), y)),
              if2(true(), x, y) -> nil(),
             if2(false(), x, y) -> intlist int(p x, p y)}
      Open