MAYBE
Time: 0.008641
TRS:
 {            p s x -> x,
              p 0() -> s s 0(),
            p p s x -> p x,
       le(s x, s y) -> le(x, y),
       le(s x, 0()) -> false(),
         le(0(), y) -> true(),
       le(p s x, x) -> le(x, x),
   if(true(), x, y) -> 0(),
  if(false(), x, y) -> s minus(p x, y),
        minus(x, y) -> if(le(x, y), x, y)}
 DP:
  DP:
   {          p# p s x -> p# x,
         le#(s x, s y) -> le#(x, y),
         le#(p s x, x) -> le#(x, x),
    if#(false(), x, y) -> p# x,
    if#(false(), x, y) -> minus#(p x, y),
          minus#(x, y) -> le#(x, y),
          minus#(x, y) -> if#(le(x, y), x, y)}
  TRS:
  {            p s x -> x,
               p 0() -> s s 0(),
             p p s x -> p x,
        le(s x, s y) -> le(x, y),
        le(s x, 0()) -> false(),
          le(0(), y) -> true(),
        le(p s x, x) -> le(x, x),
    if(true(), x, y) -> 0(),
   if(false(), x, y) -> s minus(p x, y),
         minus(x, y) -> if(le(x, y), x, y)}
  UR:
   {       p s x -> x,
           p 0() -> s s 0(),
         p p s x -> p x,
    le(s x, s y) -> le(x, y),
    le(s x, 0()) -> false(),
      le(0(), y) -> true(),
    le(p s x, x) -> le(x, x),
         a(z, w) -> z,
         a(z, w) -> w}
   EDG:
    {(le#(p s x, x) -> le#(x, x), le#(p s x, x) -> le#(x, x))
     (le#(p s x, x) -> le#(x, x), le#(s x, s y) -> le#(x, y))
     (p# p s x -> p# x, p# p s x -> p# x)
     (le#(s x, s y) -> le#(x, y), le#(p s x, x) -> le#(x, x))
     (le#(s x, s y) -> le#(x, y), le#(s x, s y) -> le#(x, y))
     (minus#(x, y) -> le#(x, y), le#(s x, s y) -> le#(x, y))
     (minus#(x, y) -> le#(x, y), le#(p s x, x) -> le#(x, x))
     (if#(false(), x, y) -> p# x, p# p s x -> p# x)
     (minus#(x, y) -> if#(le(x, y), x, y), if#(false(), x, y) -> p# x)
     (minus#(x, y) -> if#(le(x, y), x, y), if#(false(), x, y) -> minus#(p x, y))
     (if#(false(), x, y) -> minus#(p x, y), minus#(x, y) -> le#(x, y))
     (if#(false(), x, y) -> minus#(p x, y), minus#(x, y) -> if#(le(x, y), x, y))}
    STATUS:
     arrows: 0.755102
     SCCS (3):
      Scc:
       {if#(false(), x, y) -> minus#(p x, y),
              minus#(x, y) -> if#(le(x, y), x, y)}
      Scc:
       {p# p s x -> p# x}
      Scc:
       {le#(s x, s y) -> le#(x, y),
        le#(p s x, x) -> le#(x, x)}
      
      SCC (2):
       Strict:
        {if#(false(), x, y) -> minus#(p x, y),
               minus#(x, y) -> if#(le(x, y), x, y)}
       Weak:
       {            p s x -> x,
                    p 0() -> s s 0(),
                  p p s x -> p x,
             le(s x, s y) -> le(x, y),
             le(s x, 0()) -> false(),
               le(0(), y) -> true(),
             le(p s x, x) -> le(x, x),
         if(true(), x, y) -> 0(),
        if(false(), x, y) -> s minus(p x, y),
              minus(x, y) -> if(le(x, y), x, y)}
       Open
      
      SCC (1):
       Strict:
        {p# p s x -> p# x}
       Weak:
       {            p s x -> x,
                    p 0() -> s s 0(),
                  p p s x -> p x,
             le(s x, s y) -> le(x, y),
             le(s x, 0()) -> false(),
               le(0(), y) -> true(),
             le(p s x, x) -> le(x, x),
         if(true(), x, y) -> 0(),
        if(false(), x, y) -> s minus(p x, y),
              minus(x, y) -> if(le(x, y), x, y)}
       Open
      
      SCC (2):
       Strict:
        {le#(s x, s y) -> le#(x, y),
         le#(p s x, x) -> le#(x, x)}
       Weak:
       {            p s x -> x,
                    p 0() -> s s 0(),
                  p p s x -> p x,
             le(s x, s y) -> le(x, y),
             le(s x, 0()) -> false(),
               le(0(), y) -> true(),
             le(p s x, x) -> le(x, x),
         if(true(), x, y) -> 0(),
        if(false(), x, y) -> s minus(p x, y),
              minus(x, y) -> if(le(x, y), x, y)}
       Open