MAYBE
Time: 0.002086
TRS:
 {              0() -> n__0(),
              p 0() -> 0(),
              p s X -> X,
                s X -> n__s X,
        leq(0(), Y) -> true(),
      leq(s X, 0()) -> false(),
      leq(s X, s Y) -> leq(X, Y),
         activate X -> X,
    activate n__0() -> 0(),
    activate n__s X -> s X,
   if(true(), X, Y) -> activate X,
  if(false(), X, Y) -> activate Y,
         diff(X, Y) -> if(leq(X, Y), n__0(), n__s diff(p X, Y))}
 DP:
  DP:
   {    leq#(s X, s Y) -> leq#(X, Y),
      activate# n__0() -> 0#(),
      activate# n__s X -> s# X,
     if#(true(), X, Y) -> activate# X,
    if#(false(), X, Y) -> activate# Y,
           diff#(X, Y) -> p# X,
           diff#(X, Y) -> leq#(X, Y),
           diff#(X, Y) -> if#(leq(X, Y), n__0(), n__s diff(p X, Y)),
           diff#(X, Y) -> diff#(p X, Y)}
  TRS:
  {              0() -> n__0(),
               p 0() -> 0(),
               p s X -> X,
                 s X -> n__s X,
         leq(0(), Y) -> true(),
       leq(s X, 0()) -> false(),
       leq(s X, s Y) -> leq(X, Y),
          activate X -> X,
     activate n__0() -> 0(),
     activate n__s X -> s X,
    if(true(), X, Y) -> activate X,
   if(false(), X, Y) -> activate Y,
          diff(X, Y) -> if(leq(X, Y), n__0(), n__s diff(p X, Y))}
  EDG:
   {(if#(true(), X, Y) -> activate# X, activate# n__s X -> s# X)
    (if#(true(), X, Y) -> activate# X, activate# n__0() -> 0#())
    (diff#(X, Y) -> diff#(p X, Y), diff#(X, Y) -> diff#(p X, Y))
    (diff#(X, Y) -> diff#(p X, Y), diff#(X, Y) -> if#(leq(X, Y), n__0(), n__s diff(p X, Y)))
    (diff#(X, Y) -> diff#(p X, Y), diff#(X, Y) -> leq#(X, Y))
    (diff#(X, Y) -> diff#(p X, Y), diff#(X, Y) -> p# X)
    (diff#(X, Y) -> leq#(X, Y), leq#(s X, s Y) -> leq#(X, Y))
    (diff#(X, Y) -> if#(leq(X, Y), n__0(), n__s diff(p X, Y)), if#(false(), X, Y) -> activate# Y)
    (diff#(X, Y) -> if#(leq(X, Y), n__0(), n__s diff(p X, Y)), if#(true(), X, Y) -> activate# X)
    (if#(false(), X, Y) -> activate# Y, activate# n__0() -> 0#())
    (if#(false(), X, Y) -> activate# Y, activate# n__s X -> s# X)
    (leq#(s X, s Y) -> leq#(X, Y), leq#(s X, s Y) -> leq#(X, Y))}
   STATUS:
    arrows: 0.851852
    SCCS (2):
     Scc:
      {diff#(X, Y) -> diff#(p X, Y)}
     Scc:
      {leq#(s X, s Y) -> leq#(X, Y)}
     
     SCC (1):
      Strict:
       {diff#(X, Y) -> diff#(p X, Y)}
      Weak:
      {              0() -> n__0(),
                   p 0() -> 0(),
                   p s X -> X,
                     s X -> n__s X,
             leq(0(), Y) -> true(),
           leq(s X, 0()) -> false(),
           leq(s X, s Y) -> leq(X, Y),
              activate X -> X,
         activate n__0() -> 0(),
         activate n__s X -> s X,
        if(true(), X, Y) -> activate X,
       if(false(), X, Y) -> activate Y,
              diff(X, Y) -> if(leq(X, Y), n__0(), n__s diff(p X, Y))}
      Open
     
     
     
     SCC (1):
      Strict:
       {leq#(s X, s Y) -> leq#(X, Y)}
      Weak:
      {              0() -> n__0(),
                   p 0() -> 0(),
                   p s X -> X,
                     s X -> n__s X,
             leq(0(), Y) -> true(),
           leq(s X, 0()) -> false(),
           leq(s X, s Y) -> leq(X, Y),
              activate X -> X,
         activate n__0() -> 0(),
         activate n__s X -> s X,
        if(true(), X, Y) -> activate X,
       if(false(), X, Y) -> activate Y,
              diff(X, Y) -> if(leq(X, Y), n__0(), n__s diff(p X, Y))}
      Open