MAYBE
Time: 0.018842
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))}
  UR:
   {              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)),
              a(x, y) -> x,
              a(x, y) -> 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))}
    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))}
     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))}
      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))}
          Fail
         
         
         
         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))}
          POLY:
           Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
           Interpretation:
            [if](x0, x1, x2) = 0,
            
            [leq](x0, x1) = x0 + 1,
            
            [diff](x0, x1) = x0 + 1,
            
            [p](x0) = x0 + 1,
            
            [s](x0) = x0 + 1,
            
            [activate](x0) = 0,
            
            [n__s](x0) = 0,
            
            [0] = 1,
            
            [true] = 0,
            
            [false] = 0,
            
            [n__0] = 0,
            
            [leq#](x0, x1) = x0
           Strict:
            leq#(s X, s Y) -> leq#(X, Y)
            1 + 0X + 1Y >= 0 + 0X + 1Y
           Weak:
            diff(X, Y) -> if(leq(X, Y), n__0(), n__s diff(p X, Y))
            1 + 1X + 0Y >= 0 + 0X + 0Y
            if(false(), X, Y) -> activate Y
            0 + 0X + 0Y >= 0 + 0Y
            if(true(), X, Y) -> activate X
            0 + 0X + 0Y >= 0 + 0X
            activate n__s X -> s X
            0 + 0X >= 1 + 1X
            activate n__0() -> 0()
            0 >= 1
            activate X -> X
            0 + 0X >= 1X
            leq(s X, s Y) -> leq(X, Y)
            2 + 1X + 0Y >= 1 + 1X + 0Y
            leq(s X, 0()) -> false()
            2 + 1X >= 0
            leq(0(), Y) -> true()
            2 + 0Y >= 0
            s X -> n__s X
            1 + 1X >= 0 + 0X
            p s X -> X
            2 + 1X >= 1X
            p 0() -> 0()
            2 >= 1
            0() -> n__0()
            1 >= 0
          Qed