MAYBE
Time: 0.001239
TRS:
 {            p 0() -> 0(),
              p s x -> x,
         le(0(), y) -> true(),
       le(s x, 0()) -> false(),
       le(s x, s y) -> le(x, y),
   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:
   {     le#(s x, s y) -> le#(x, y),
    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 0() -> 0(),
               p s x -> x,
          le(0(), y) -> true(),
        le(s x, 0()) -> false(),
        le(s x, s y) -> le(x, y),
    if(true(), x, y) -> 0(),
   if(false(), x, y) -> s minus(p x, y),
         minus(x, y) -> if(le(x, y), x, y)}
  EDG:
   {(minus#(x, y) -> le#(x, y), le#(s x, s y) -> le#(x, y))
    (minus#(x, y) -> if#(le(x, y), x, y), if#(false(), x, y) -> minus#(p x, y))
    (minus#(x, y) -> if#(le(x, y), x, y), if#(false(), x, y) -> p# x)
    (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))
    (le#(s x, s y) -> le#(x, y), le#(s x, s y) -> le#(x, y))}
   STATUS:
    arrows: 0.760000
    SCCS (2):
     Scc:
      {if#(false(), x, y) -> minus#(p x, y),
             minus#(x, y) -> if#(le(x, y), x, y)}
     Scc:
      {le#(s x, s y) -> le#(x, y)}
     
     SCC (2):
      Strict:
       {if#(false(), x, y) -> minus#(p x, y),
              minus#(x, y) -> if#(le(x, y), x, y)}
      Weak:
      {            p 0() -> 0(),
                   p s x -> x,
              le(0(), y) -> true(),
            le(s x, 0()) -> false(),
            le(s x, s y) -> le(x, y),
        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:
       {le#(s x, s y) -> le#(x, y)}
      Weak:
      {            p 0() -> 0(),
                   p s x -> x,
              le(0(), y) -> true(),
            le(s x, 0()) -> false(),
            le(s x, s y) -> le(x, y),
        if(true(), x, y) -> 0(),
       if(false(), x, y) -> s minus(p x, y),
             minus(x, y) -> if(le(x, y), x, y)}
      Open