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