MAYBE
Time: 0.009498
TRS:
 {                     0() -> n__0(),
                       p X -> n__p X,
                     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 activate X,
  activate n__diff(X1, X2) -> diff(activate X1, activate X2),
           activate n__p X -> p activate X,
          if(true(), X, Y) -> activate X,
         if(false(), X, Y) -> activate Y,
                diff(X, Y) -> if(leq(X, Y), n__0(), n__s n__diff(n__p X, Y)),
              diff(X1, X2) -> n__diff(X1, X2)}
 DP:
  DP:
   {           leq#(s X, s Y) -> leq#(X, Y),
             activate# n__0() -> 0#(),
             activate# n__s X -> s# activate X,
             activate# n__s X -> activate# X,
    activate# n__diff(X1, X2) -> activate# X1,
    activate# n__diff(X1, X2) -> activate# X2,
    activate# n__diff(X1, X2) -> diff#(activate X1, activate X2),
             activate# n__p X -> p# activate X,
             activate# n__p X -> activate# X,
            if#(true(), X, Y) -> activate# X,
           if#(false(), X, Y) -> activate# Y,
                  diff#(X, Y) -> leq#(X, Y),
                  diff#(X, Y) -> if#(leq(X, Y), n__0(), n__s n__diff(n__p X, Y))}
  TRS:
  {                     0() -> n__0(),
                        p X -> n__p X,
                      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 activate X,
   activate n__diff(X1, X2) -> diff(activate X1, activate X2),
            activate n__p X -> p activate X,
           if(true(), X, Y) -> activate X,
          if(false(), X, Y) -> activate Y,
                 diff(X, Y) -> if(leq(X, Y), n__0(), n__s n__diff(n__p X, Y)),
               diff(X1, X2) -> n__diff(X1, X2)}
  EDG:
   {(diff#(X, Y) -> leq#(X, Y), leq#(s X, s Y) -> leq#(X, Y))
    (activate# n__p X -> activate# X, activate# n__p X -> activate# X)
    (activate# n__p X -> activate# X, activate# n__p X -> p# activate X)
    (activate# n__p X -> activate# X, activate# n__diff(X1, X2) -> diff#(activate X1, activate X2))
    (activate# n__p X -> activate# X, activate# n__diff(X1, X2) -> activate# X2)
    (activate# n__p X -> activate# X, activate# n__diff(X1, X2) -> activate# X1)
    (activate# n__p X -> activate# X, activate# n__s X -> activate# X)
    (activate# n__p X -> activate# X, activate# n__s X -> s# activate X)
    (activate# n__p X -> activate# X, activate# n__0() -> 0#())
    (diff#(X, Y) -> if#(leq(X, Y), n__0(), n__s n__diff(n__p X, Y)), if#(false(), X, Y) -> activate# Y)
    (diff#(X, Y) -> if#(leq(X, Y), n__0(), n__s n__diff(n__p X, Y)), if#(true(), X, Y) -> activate# X)
    (activate# n__diff(X1, X2) -> activate# X1, activate# n__p X -> activate# X)
    (activate# n__diff(X1, X2) -> activate# X1, activate# n__p X -> p# activate X)
    (activate# n__diff(X1, X2) -> activate# X1, activate# n__diff(X1, X2) -> diff#(activate X1, activate X2))
    (activate# n__diff(X1, X2) -> activate# X1, activate# n__diff(X1, X2) -> activate# X2)
    (activate# n__diff(X1, X2) -> activate# X1, activate# n__diff(X1, X2) -> activate# X1)
    (activate# n__diff(X1, X2) -> activate# X1, activate# n__s X -> activate# X)
    (activate# n__diff(X1, X2) -> activate# X1, activate# n__s X -> s# activate X)
    (activate# n__diff(X1, X2) -> activate# X1, activate# n__0() -> 0#())
    (activate# n__diff(X1, X2) -> activate# X2, activate# n__p X -> activate# X)
    (activate# n__diff(X1, X2) -> activate# X2, activate# n__p X -> p# activate X)
    (activate# n__diff(X1, X2) -> activate# X2, activate# n__diff(X1, X2) -> diff#(activate X1, activate X2))
    (activate# n__diff(X1, X2) -> activate# X2, activate# n__diff(X1, X2) -> activate# X2)
    (activate# n__diff(X1, X2) -> activate# X2, activate# n__diff(X1, X2) -> activate# X1)
    (activate# n__diff(X1, X2) -> activate# X2, activate# n__s X -> activate# X)
    (activate# n__diff(X1, X2) -> activate# X2, activate# n__s X -> s# activate X)
    (activate# n__diff(X1, X2) -> activate# X2, activate# n__0() -> 0#())
    (activate# n__diff(X1, X2) -> diff#(activate X1, activate X2), diff#(X, Y) -> leq#(X, Y))
    (activate# n__diff(X1, X2) -> diff#(activate X1, activate X2), diff#(X, Y) -> if#(leq(X, Y), n__0(), n__s n__diff(n__p X, Y)))
    (if#(false(), X, Y) -> activate# Y, activate# n__0() -> 0#())
    (if#(false(), X, Y) -> activate# Y, activate# n__s X -> s# activate X)
    (if#(false(), X, Y) -> activate# Y, activate# n__s X -> activate# X)
    (if#(false(), X, Y) -> activate# Y, activate# n__diff(X1, X2) -> activate# X1)
    (if#(false(), X, Y) -> activate# Y, activate# n__diff(X1, X2) -> activate# X2)
    (if#(false(), X, Y) -> activate# Y, activate# n__diff(X1, X2) -> diff#(activate X1, activate X2))
    (if#(false(), X, Y) -> activate# Y, activate# n__p X -> p# activate X)
    (if#(false(), X, Y) -> activate# Y, activate# n__p X -> activate# X)
    (if#(true(), X, Y) -> activate# X, activate# n__0() -> 0#())
    (if#(true(), X, Y) -> activate# X, activate# n__s X -> s# activate X)
    (if#(true(), X, Y) -> activate# X, activate# n__s X -> activate# X)
    (if#(true(), X, Y) -> activate# X, activate# n__diff(X1, X2) -> activate# X1)
    (if#(true(), X, Y) -> activate# X, activate# n__diff(X1, X2) -> activate# X2)
    (if#(true(), X, Y) -> activate# X, activate# n__diff(X1, X2) -> diff#(activate X1, activate X2))
    (if#(true(), X, Y) -> activate# X, activate# n__p X -> p# activate X)
    (if#(true(), X, Y) -> activate# X, activate# n__p X -> activate# X)
    (activate# n__s X -> activate# X, activate# n__0() -> 0#())
    (activate# n__s X -> activate# X, activate# n__s X -> s# activate X)
    (activate# n__s X -> activate# X, activate# n__s X -> activate# X)
    (activate# n__s X -> activate# X, activate# n__diff(X1, X2) -> activate# X1)
    (activate# n__s X -> activate# X, activate# n__diff(X1, X2) -> activate# X2)
    (activate# n__s X -> activate# X, activate# n__diff(X1, X2) -> diff#(activate X1, activate X2))
    (activate# n__s X -> activate# X, activate# n__p X -> p# activate X)
    (activate# n__s X -> activate# X, activate# n__p X -> activate# X)
    (leq#(s X, s Y) -> leq#(X, Y), leq#(s X, s Y) -> leq#(X, Y))}
   STATUS:
    arrows: 0.680473
    SCCS (2):
     Scc:
      {         activate# n__s X -> activate# X,
       activate# n__diff(X1, X2) -> activate# X1,
       activate# n__diff(X1, X2) -> activate# X2,
       activate# n__diff(X1, X2) -> diff#(activate X1, activate X2),
                activate# n__p X -> activate# X,
               if#(true(), X, Y) -> activate# X,
              if#(false(), X, Y) -> activate# Y,
                     diff#(X, Y) -> if#(leq(X, Y), n__0(), n__s n__diff(n__p X, Y))}
     Scc:
      {leq#(s X, s Y) -> leq#(X, Y)}
     
     SCC (8):
      Strict:
       {         activate# n__s X -> activate# X,
        activate# n__diff(X1, X2) -> activate# X1,
        activate# n__diff(X1, X2) -> activate# X2,
        activate# n__diff(X1, X2) -> diff#(activate X1, activate X2),
                 activate# n__p X -> activate# X,
                if#(true(), X, Y) -> activate# X,
               if#(false(), X, Y) -> activate# Y,
                      diff#(X, Y) -> if#(leq(X, Y), n__0(), n__s n__diff(n__p X, Y))}
      Weak:
      {                     0() -> n__0(),
                            p X -> n__p X,
                          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 activate X,
       activate n__diff(X1, X2) -> diff(activate X1, activate X2),
                activate n__p X -> p activate X,
               if(true(), X, Y) -> activate X,
              if(false(), X, Y) -> activate Y,
                     diff(X, Y) -> if(leq(X, Y), n__0(), n__s n__diff(n__p X, Y)),
                   diff(X1, X2) -> n__diff(X1, X2)}
      Open
     
     
     
     
     SCC (1):
      Strict:
       {leq#(s X, s Y) -> leq#(X, Y)}
      Weak:
      {                     0() -> n__0(),
                            p X -> n__p X,
                          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 activate X,
       activate n__diff(X1, X2) -> diff(activate X1, activate X2),
                activate n__p X -> p activate X,
               if(true(), X, Y) -> activate X,
              if(false(), X, Y) -> activate Y,
                     diff(X, Y) -> if(leq(X, Y), n__0(), n__s n__diff(n__p X, Y)),
                   diff(X1, X2) -> n__diff(X1, X2)}
      Open