MAYBE
Time: 0.011441
TRS:
 {  a__U12(X1, X2, X3) -> U12(X1, X2, X3),
    a__U12(tt(), M, N) -> s a__plus(mark N, mark M),
    a__U11(X1, X2, X3) -> U11(X1, X2, X3),
    a__U11(tt(), M, N) -> a__U12(tt(), M, N),
       a__plus(N, s M) -> a__U11(tt(), M, N),
       a__plus(N, 0()) -> mark N,
       a__plus(X1, X2) -> plus(X1, X2),
             mark tt() -> tt(),
              mark s X -> s mark X,
              mark 0() -> 0(),
  mark U11(X1, X2, X3) -> a__U11(mark X1, X2, X3),
  mark U12(X1, X2, X3) -> a__U12(mark X1, X2, X3),
     mark plus(X1, X2) -> a__plus(mark X1, mark X2)}
 DP:
  DP:
   {  a__U12#(tt(), M, N) -> a__plus#(mark N, mark M),
      a__U12#(tt(), M, N) -> mark# M,
      a__U12#(tt(), M, N) -> mark# N,
      a__U11#(tt(), M, N) -> a__U12#(tt(), M, N),
         a__plus#(N, s M) -> a__U11#(tt(), M, N),
         a__plus#(N, 0()) -> mark# N,
                mark# s X -> mark# X,
    mark# U11(X1, X2, X3) -> a__U11#(mark X1, X2, X3),
    mark# U11(X1, X2, X3) -> mark# X1,
    mark# U12(X1, X2, X3) -> a__U12#(mark X1, X2, X3),
    mark# U12(X1, X2, X3) -> mark# X1,
       mark# plus(X1, X2) -> a__plus#(mark X1, mark X2),
       mark# plus(X1, X2) -> mark# X1,
       mark# plus(X1, X2) -> mark# X2}
  TRS:
  {  a__U12(X1, X2, X3) -> U12(X1, X2, X3),
     a__U12(tt(), M, N) -> s a__plus(mark N, mark M),
     a__U11(X1, X2, X3) -> U11(X1, X2, X3),
     a__U11(tt(), M, N) -> a__U12(tt(), M, N),
        a__plus(N, s M) -> a__U11(tt(), M, N),
        a__plus(N, 0()) -> mark N,
        a__plus(X1, X2) -> plus(X1, X2),
              mark tt() -> tt(),
               mark s X -> s mark X,
               mark 0() -> 0(),
   mark U11(X1, X2, X3) -> a__U11(mark X1, X2, X3),
   mark U12(X1, X2, X3) -> a__U12(mark X1, X2, X3),
      mark plus(X1, X2) -> a__plus(mark X1, mark X2)}
  UR:
   {  a__U12(X1, X2, X3) -> U12(X1, X2, X3),
      a__U12(tt(), M, N) -> s a__plus(mark N, mark M),
      a__U11(X1, X2, X3) -> U11(X1, X2, X3),
      a__U11(tt(), M, N) -> a__U12(tt(), M, N),
         a__plus(N, s M) -> a__U11(tt(), M, N),
         a__plus(N, 0()) -> mark N,
         a__plus(X1, X2) -> plus(X1, X2),
               mark tt() -> tt(),
                mark s X -> s mark X,
                mark 0() -> 0(),
    mark U11(X1, X2, X3) -> a__U11(mark X1, X2, X3),
    mark U12(X1, X2, X3) -> a__U12(mark X1, X2, X3),
       mark plus(X1, X2) -> a__plus(mark X1, mark X2)}
   EDG:
    {(mark# plus(X1, X2) -> mark# X2, mark# plus(X1, X2) -> mark# X2)
     (mark# plus(X1, X2) -> mark# X2, mark# plus(X1, X2) -> mark# X1)
     (mark# plus(X1, X2) -> mark# X2, mark# plus(X1, X2) -> a__plus#(mark X1, mark X2))
     (mark# plus(X1, X2) -> mark# X2, mark# U12(X1, X2, X3) -> mark# X1)
     (mark# plus(X1, X2) -> mark# X2, mark# U12(X1, X2, X3) -> a__U12#(mark X1, X2, X3))
     (mark# plus(X1, X2) -> mark# X2, mark# U11(X1, X2, X3) -> mark# X1)
     (mark# plus(X1, X2) -> mark# X2, mark# U11(X1, X2, X3) -> a__U11#(mark X1, X2, X3))
     (mark# plus(X1, X2) -> mark# X2, mark# s X -> mark# X)
     (a__plus#(N, 0()) -> mark# N, mark# plus(X1, X2) -> mark# X2)
     (a__plus#(N, 0()) -> mark# N, mark# plus(X1, X2) -> mark# X1)
     (a__plus#(N, 0()) -> mark# N, mark# plus(X1, X2) -> a__plus#(mark X1, mark X2))
     (a__plus#(N, 0()) -> mark# N, mark# U12(X1, X2, X3) -> mark# X1)
     (a__plus#(N, 0()) -> mark# N, mark# U12(X1, X2, X3) -> a__U12#(mark X1, X2, X3))
     (a__plus#(N, 0()) -> mark# N, mark# U11(X1, X2, X3) -> mark# X1)
     (a__plus#(N, 0()) -> mark# N, mark# U11(X1, X2, X3) -> a__U11#(mark X1, X2, X3))
     (a__plus#(N, 0()) -> mark# N, mark# s X -> mark# X)
     (mark# U11(X1, X2, X3) -> a__U11#(mark X1, X2, X3), a__U11#(tt(), M, N) -> a__U12#(tt(), M, N))
     (mark# U12(X1, X2, X3) -> a__U12#(mark X1, X2, X3), a__U12#(tt(), M, N) -> mark# N)
     (mark# U12(X1, X2, X3) -> a__U12#(mark X1, X2, X3), a__U12#(tt(), M, N) -> mark# M)
     (mark# U12(X1, X2, X3) -> a__U12#(mark X1, X2, X3), a__U12#(tt(), M, N) -> a__plus#(mark N, mark M))
     (mark# plus(X1, X2) -> a__plus#(mark X1, mark X2), a__plus#(N, 0()) -> mark# N)
     (mark# plus(X1, X2) -> a__plus#(mark X1, mark X2), a__plus#(N, s M) -> a__U11#(tt(), M, N))
     (a__U11#(tt(), M, N) -> a__U12#(tt(), M, N), a__U12#(tt(), M, N) -> mark# N)
     (a__U11#(tt(), M, N) -> a__U12#(tt(), M, N), a__U12#(tt(), M, N) -> mark# M)
     (a__U11#(tt(), M, N) -> a__U12#(tt(), M, N), a__U12#(tt(), M, N) -> a__plus#(mark N, mark M))
     (a__U12#(tt(), M, N) -> mark# M, mark# plus(X1, X2) -> mark# X2)
     (a__U12#(tt(), M, N) -> mark# M, mark# plus(X1, X2) -> mark# X1)
     (a__U12#(tt(), M, N) -> mark# M, mark# plus(X1, X2) -> a__plus#(mark X1, mark X2))
     (a__U12#(tt(), M, N) -> mark# M, mark# U12(X1, X2, X3) -> mark# X1)
     (a__U12#(tt(), M, N) -> mark# M, mark# U12(X1, X2, X3) -> a__U12#(mark X1, X2, X3))
     (a__U12#(tt(), M, N) -> mark# M, mark# U11(X1, X2, X3) -> mark# X1)
     (a__U12#(tt(), M, N) -> mark# M, mark# U11(X1, X2, X3) -> a__U11#(mark X1, X2, X3))
     (a__U12#(tt(), M, N) -> mark# M, mark# s X -> mark# X)
     (a__plus#(N, s M) -> a__U11#(tt(), M, N), a__U11#(tt(), M, N) -> a__U12#(tt(), M, N))
     (mark# plus(X1, X2) -> mark# X1, mark# s X -> mark# X)
     (mark# plus(X1, X2) -> mark# X1, mark# U11(X1, X2, X3) -> a__U11#(mark X1, X2, X3))
     (mark# plus(X1, X2) -> mark# X1, mark# U11(X1, X2, X3) -> mark# X1)
     (mark# plus(X1, X2) -> mark# X1, mark# U12(X1, X2, X3) -> a__U12#(mark X1, X2, X3))
     (mark# plus(X1, X2) -> mark# X1, mark# U12(X1, X2, X3) -> mark# X1)
     (mark# plus(X1, X2) -> mark# X1, mark# plus(X1, X2) -> a__plus#(mark X1, mark X2))
     (mark# plus(X1, X2) -> mark# X1, mark# plus(X1, X2) -> mark# X1)
     (mark# plus(X1, X2) -> mark# X1, mark# plus(X1, X2) -> mark# X2)
     (mark# U12(X1, X2, X3) -> mark# X1, mark# s X -> mark# X)
     (mark# U12(X1, X2, X3) -> mark# X1, mark# U11(X1, X2, X3) -> a__U11#(mark X1, X2, X3))
     (mark# U12(X1, X2, X3) -> mark# X1, mark# U11(X1, X2, X3) -> mark# X1)
     (mark# U12(X1, X2, X3) -> mark# X1, mark# U12(X1, X2, X3) -> a__U12#(mark X1, X2, X3))
     (mark# U12(X1, X2, X3) -> mark# X1, mark# U12(X1, X2, X3) -> mark# X1)
     (mark# U12(X1, X2, X3) -> mark# X1, mark# plus(X1, X2) -> a__plus#(mark X1, mark X2))
     (mark# U12(X1, X2, X3) -> mark# X1, mark# plus(X1, X2) -> mark# X1)
     (mark# U12(X1, X2, X3) -> mark# X1, mark# plus(X1, X2) -> mark# X2)
     (mark# U11(X1, X2, X3) -> mark# X1, mark# s X -> mark# X)
     (mark# U11(X1, X2, X3) -> mark# X1, mark# U11(X1, X2, X3) -> a__U11#(mark X1, X2, X3))
     (mark# U11(X1, X2, X3) -> mark# X1, mark# U11(X1, X2, X3) -> mark# X1)
     (mark# U11(X1, X2, X3) -> mark# X1, mark# U12(X1, X2, X3) -> a__U12#(mark X1, X2, X3))
     (mark# U11(X1, X2, X3) -> mark# X1, mark# U12(X1, X2, X3) -> mark# X1)
     (mark# U11(X1, X2, X3) -> mark# X1, mark# plus(X1, X2) -> a__plus#(mark X1, mark X2))
     (mark# U11(X1, X2, X3) -> mark# X1, mark# plus(X1, X2) -> mark# X1)
     (mark# U11(X1, X2, X3) -> mark# X1, mark# plus(X1, X2) -> mark# X2)
     (a__U12#(tt(), M, N) -> a__plus#(mark N, mark M), a__plus#(N, s M) -> a__U11#(tt(), M, N))
     (a__U12#(tt(), M, N) -> a__plus#(mark N, mark M), a__plus#(N, 0()) -> mark# N)
     (a__U12#(tt(), M, N) -> mark# N, mark# s X -> mark# X)
     (a__U12#(tt(), M, N) -> mark# N, mark# U11(X1, X2, X3) -> a__U11#(mark X1, X2, X3))
     (a__U12#(tt(), M, N) -> mark# N, mark# U11(X1, X2, X3) -> mark# X1)
     (a__U12#(tt(), M, N) -> mark# N, mark# U12(X1, X2, X3) -> a__U12#(mark X1, X2, X3))
     (a__U12#(tt(), M, N) -> mark# N, mark# U12(X1, X2, X3) -> mark# X1)
     (a__U12#(tt(), M, N) -> mark# N, mark# plus(X1, X2) -> a__plus#(mark X1, mark X2))
     (a__U12#(tt(), M, N) -> mark# N, mark# plus(X1, X2) -> mark# X1)
     (a__U12#(tt(), M, N) -> mark# N, mark# plus(X1, X2) -> mark# X2)
     (mark# s X -> mark# X, mark# s X -> mark# X)
     (mark# s X -> mark# X, mark# U11(X1, X2, X3) -> a__U11#(mark X1, X2, X3))
     (mark# s X -> mark# X, mark# U11(X1, X2, X3) -> mark# X1)
     (mark# s X -> mark# X, mark# U12(X1, X2, X3) -> a__U12#(mark X1, X2, X3))
     (mark# s X -> mark# X, mark# U12(X1, X2, X3) -> mark# X1)
     (mark# s X -> mark# X, mark# plus(X1, X2) -> a__plus#(mark X1, mark X2))
     (mark# s X -> mark# X, mark# plus(X1, X2) -> mark# X1)
     (mark# s X -> mark# X, mark# plus(X1, X2) -> mark# X2)}
    STATUS:
     arrows: 0.612245
     SCCS (1):
      Scc:
       {  a__U12#(tt(), M, N) -> a__plus#(mark N, mark M),
          a__U12#(tt(), M, N) -> mark# M,
          a__U12#(tt(), M, N) -> mark# N,
          a__U11#(tt(), M, N) -> a__U12#(tt(), M, N),
             a__plus#(N, s M) -> a__U11#(tt(), M, N),
             a__plus#(N, 0()) -> mark# N,
                    mark# s X -> mark# X,
        mark# U11(X1, X2, X3) -> a__U11#(mark X1, X2, X3),
        mark# U11(X1, X2, X3) -> mark# X1,
        mark# U12(X1, X2, X3) -> a__U12#(mark X1, X2, X3),
        mark# U12(X1, X2, X3) -> mark# X1,
           mark# plus(X1, X2) -> a__plus#(mark X1, mark X2),
           mark# plus(X1, X2) -> mark# X1,
           mark# plus(X1, X2) -> mark# X2}
      
      SCC (14):
       Strict:
        {  a__U12#(tt(), M, N) -> a__plus#(mark N, mark M),
           a__U12#(tt(), M, N) -> mark# M,
           a__U12#(tt(), M, N) -> mark# N,
           a__U11#(tt(), M, N) -> a__U12#(tt(), M, N),
              a__plus#(N, s M) -> a__U11#(tt(), M, N),
              a__plus#(N, 0()) -> mark# N,
                     mark# s X -> mark# X,
         mark# U11(X1, X2, X3) -> a__U11#(mark X1, X2, X3),
         mark# U11(X1, X2, X3) -> mark# X1,
         mark# U12(X1, X2, X3) -> a__U12#(mark X1, X2, X3),
         mark# U12(X1, X2, X3) -> mark# X1,
            mark# plus(X1, X2) -> a__plus#(mark X1, mark X2),
            mark# plus(X1, X2) -> mark# X1,
            mark# plus(X1, X2) -> mark# X2}
       Weak:
       {  a__U12(X1, X2, X3) -> U12(X1, X2, X3),
          a__U12(tt(), M, N) -> s a__plus(mark N, mark M),
          a__U11(X1, X2, X3) -> U11(X1, X2, X3),
          a__U11(tt(), M, N) -> a__U12(tt(), M, N),
             a__plus(N, s M) -> a__U11(tt(), M, N),
             a__plus(N, 0()) -> mark N,
             a__plus(X1, X2) -> plus(X1, X2),
                   mark tt() -> tt(),
                    mark s X -> s mark X,
                    mark 0() -> 0(),
        mark U11(X1, X2, X3) -> a__U11(mark X1, X2, X3),
        mark U12(X1, X2, X3) -> a__U12(mark X1, X2, X3),
           mark plus(X1, X2) -> a__plus(mark X1, mark X2)}
       Open