MAYBE
Time: 0.012553
TRS:
 {        mark tt() -> tt(),
           mark 0() -> 0(),
           mark s X -> s mark X,
   mark and(X1, X2) -> a__and(mark X1, X2),
  mark plus(X1, X2) -> a__plus(mark X1, mark X2),
     a__and(X1, X2) -> and(X1, X2),
    a__and(tt(), X) -> mark X,
    a__plus(N, 0()) -> mark N,
    a__plus(N, s M) -> s a__plus(mark N, mark M),
    a__plus(X1, X2) -> plus(X1, X2)}
 DP:
  DP:
   {         mark# s X -> mark# X,
     mark# and(X1, X2) -> mark# X1,
     mark# and(X1, X2) -> a__and#(mark X1, X2),
    mark# plus(X1, X2) -> mark# X1,
    mark# plus(X1, X2) -> mark# X2,
    mark# plus(X1, X2) -> a__plus#(mark X1, mark X2),
      a__and#(tt(), X) -> mark# X,
      a__plus#(N, 0()) -> mark# N,
      a__plus#(N, s M) -> mark# N,
      a__plus#(N, s M) -> mark# M,
      a__plus#(N, s M) -> a__plus#(mark N, mark M)}
  TRS:
  {        mark tt() -> tt(),
            mark 0() -> 0(),
            mark s X -> s mark X,
    mark and(X1, X2) -> a__and(mark X1, X2),
   mark plus(X1, X2) -> a__plus(mark X1, mark X2),
      a__and(X1, X2) -> and(X1, X2),
     a__and(tt(), X) -> mark X,
     a__plus(N, 0()) -> mark N,
     a__plus(N, s M) -> s a__plus(mark N, mark M),
     a__plus(X1, X2) -> plus(X1, X2)}
  UR:
   {        mark tt() -> tt(),
             mark 0() -> 0(),
             mark s X -> s mark X,
     mark and(X1, X2) -> a__and(mark X1, X2),
    mark plus(X1, X2) -> a__plus(mark X1, mark X2),
       a__and(X1, X2) -> and(X1, X2),
      a__and(tt(), X) -> mark X,
      a__plus(N, 0()) -> mark N,
      a__plus(N, s M) -> s a__plus(mark N, mark M),
      a__plus(X1, X2) -> plus(X1, X2)}
   EDG:
    {(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# X2)
     (mark# s X -> mark# X, mark# plus(X1, X2) -> mark# X1)
     (mark# s X -> mark# X, mark# and(X1, X2) -> a__and#(mark X1, X2))
     (mark# s X -> mark# X, mark# and(X1, X2) -> mark# X1)
     (mark# s X -> mark# X, mark# s X -> mark# X)
     (a__and#(tt(), X) -> mark# X, mark# plus(X1, X2) -> a__plus#(mark X1, mark X2))
     (a__and#(tt(), X) -> mark# X, mark# plus(X1, X2) -> mark# X2)
     (a__and#(tt(), X) -> mark# X, mark# plus(X1, X2) -> mark# X1)
     (a__and#(tt(), X) -> mark# X, mark# and(X1, X2) -> a__and#(mark X1, X2))
     (a__and#(tt(), X) -> mark# X, mark# and(X1, X2) -> mark# X1)
     (a__and#(tt(), X) -> mark# X, mark# s X -> mark# X)
     (a__plus#(N, 0()) -> mark# N, mark# plus(X1, X2) -> a__plus#(mark X1, mark X2))
     (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# and(X1, X2) -> a__and#(mark X1, X2))
     (a__plus#(N, 0()) -> mark# N, mark# and(X1, X2) -> mark# X1)
     (a__plus#(N, 0()) -> mark# N, mark# s X -> mark# X)
     (a__plus#(N, s M) -> mark# M, mark# plus(X1, X2) -> a__plus#(mark X1, mark X2))
     (a__plus#(N, s M) -> mark# M, mark# plus(X1, X2) -> mark# X2)
     (a__plus#(N, s M) -> mark# M, mark# plus(X1, X2) -> mark# X1)
     (a__plus#(N, s M) -> mark# M, mark# and(X1, X2) -> a__and#(mark X1, X2))
     (a__plus#(N, s M) -> mark# M, mark# and(X1, X2) -> mark# X1)
     (a__plus#(N, s M) -> mark# M, mark# s X -> mark# X)
     (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# X2)
     (mark# plus(X1, X2) -> mark# X1, mark# plus(X1, X2) -> mark# X1)
     (mark# plus(X1, X2) -> mark# X1, mark# and(X1, X2) -> a__and#(mark X1, X2))
     (mark# plus(X1, X2) -> mark# X1, mark# and(X1, X2) -> mark# X1)
     (mark# plus(X1, X2) -> mark# X1, mark# s X -> mark# X)
     (mark# plus(X1, X2) -> mark# X2, mark# s X -> mark# X)
     (mark# plus(X1, X2) -> mark# X2, mark# and(X1, X2) -> mark# X1)
     (mark# plus(X1, X2) -> mark# X2, mark# and(X1, X2) -> a__and#(mark X1, X2))
     (mark# plus(X1, X2) -> mark# X2, mark# plus(X1, X2) -> mark# X1)
     (mark# plus(X1, X2) -> mark# X2, mark# plus(X1, X2) -> mark# X2)
     (mark# plus(X1, X2) -> mark# X2, mark# plus(X1, X2) -> a__plus#(mark X1, mark X2))
     (mark# and(X1, X2) -> mark# X1, mark# s X -> mark# X)
     (mark# and(X1, X2) -> mark# X1, mark# and(X1, X2) -> mark# X1)
     (mark# and(X1, X2) -> mark# X1, mark# and(X1, X2) -> a__and#(mark X1, X2))
     (mark# and(X1, X2) -> mark# X1, mark# plus(X1, X2) -> mark# X1)
     (mark# and(X1, X2) -> mark# X1, mark# plus(X1, X2) -> mark# X2)
     (mark# and(X1, X2) -> mark# X1, mark# plus(X1, X2) -> a__plus#(mark X1, mark X2))
     (a__plus#(N, s M) -> mark# N, mark# s X -> mark# X)
     (a__plus#(N, s M) -> mark# N, mark# and(X1, X2) -> mark# X1)
     (a__plus#(N, s M) -> mark# N, mark# and(X1, X2) -> a__and#(mark X1, X2))
     (a__plus#(N, s M) -> mark# N, mark# plus(X1, X2) -> mark# X1)
     (a__plus#(N, s M) -> mark# N, mark# plus(X1, X2) -> mark# X2)
     (a__plus#(N, s M) -> mark# N, mark# plus(X1, X2) -> a__plus#(mark X1, mark X2))
     (a__plus#(N, s M) -> a__plus#(mark N, mark M), a__plus#(N, 0()) -> mark# N)
     (a__plus#(N, s M) -> a__plus#(mark N, mark M), a__plus#(N, s M) -> mark# N)
     (a__plus#(N, s M) -> a__plus#(mark N, mark M), a__plus#(N, s M) -> mark# M)
     (a__plus#(N, s M) -> a__plus#(mark N, mark M), a__plus#(N, s M) -> 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) -> mark# N)
     (mark# plus(X1, X2) -> a__plus#(mark X1, mark X2), a__plus#(N, s M) -> mark# M)
     (mark# plus(X1, X2) -> a__plus#(mark X1, mark X2), a__plus#(N, s M) -> a__plus#(mark N, mark M))
     (mark# and(X1, X2) -> a__and#(mark X1, X2), a__and#(tt(), X) -> mark# X)}
    STATUS:
     arrows: 0.528926
     SCCS (1):
      Scc:
       {         mark# s X -> mark# X,
         mark# and(X1, X2) -> mark# X1,
         mark# and(X1, X2) -> a__and#(mark X1, X2),
        mark# plus(X1, X2) -> mark# X1,
        mark# plus(X1, X2) -> mark# X2,
        mark# plus(X1, X2) -> a__plus#(mark X1, mark X2),
          a__and#(tt(), X) -> mark# X,
          a__plus#(N, 0()) -> mark# N,
          a__plus#(N, s M) -> mark# N,
          a__plus#(N, s M) -> mark# M,
          a__plus#(N, s M) -> a__plus#(mark N, mark M)}
      
      SCC (11):
       Strict:
        {         mark# s X -> mark# X,
          mark# and(X1, X2) -> mark# X1,
          mark# and(X1, X2) -> a__and#(mark X1, X2),
         mark# plus(X1, X2) -> mark# X1,
         mark# plus(X1, X2) -> mark# X2,
         mark# plus(X1, X2) -> a__plus#(mark X1, mark X2),
           a__and#(tt(), X) -> mark# X,
           a__plus#(N, 0()) -> mark# N,
           a__plus#(N, s M) -> mark# N,
           a__plus#(N, s M) -> mark# M,
           a__plus#(N, s M) -> a__plus#(mark N, mark M)}
       Weak:
       {        mark tt() -> tt(),
                 mark 0() -> 0(),
                 mark s X -> s mark X,
         mark and(X1, X2) -> a__and(mark X1, X2),
        mark plus(X1, X2) -> a__plus(mark X1, mark X2),
           a__and(X1, X2) -> and(X1, X2),
          a__and(tt(), X) -> mark X,
          a__plus(N, 0()) -> mark N,
          a__plus(N, s M) -> s a__plus(mark N, mark M),
          a__plus(X1, X2) -> plus(X1, X2)}
       Open