MAYBE
MAYBE
TRS:
 {
    mark(U12(X1, X2, X3)) -> active(U12(mark(X1), X2, X3)),
               mark(tt()) -> active(tt()),
    mark(U11(X1, X2, X3)) -> active(U11(mark(X1), X2, X3)),
               mark(s(X)) -> active(s(mark(X))),
       mark(plus(X1, X2)) -> active(plus(mark(X1), mark(X2))),
                mark(0()) -> active(0()),
    U12(X1, X2, mark(X3)) -> U12(X1, X2, X3),
  U12(X1, X2, active(X3)) -> U12(X1, X2, X3),
    U12(X1, mark(X2), X3) -> U12(X1, X2, X3),
  U12(X1, active(X2), X3) -> U12(X1, X2, X3),
    U12(mark(X1), X2, X3) -> U12(X1, X2, X3),
  U12(active(X1), X2, X3) -> U12(X1, X2, X3),
  active(U12(tt(), M, N)) -> mark(s(plus(N, M))),
  active(U11(tt(), M, N)) -> mark(U12(tt(), M, N)),
    active(plus(N, s(M))) -> mark(U11(tt(), M, N)),
     active(plus(N, 0())) -> mark(N),
    U11(X1, X2, mark(X3)) -> U11(X1, X2, X3),
  U11(X1, X2, active(X3)) -> U11(X1, X2, X3),
    U11(X1, mark(X2), X3) -> U11(X1, X2, X3),
  U11(X1, active(X2), X3) -> U11(X1, X2, X3),
    U11(mark(X1), X2, X3) -> U11(X1, X2, X3),
  U11(active(X1), X2, X3) -> U11(X1, X2, X3),
               s(mark(X)) -> s(X),
             s(active(X)) -> s(X),
       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)
 }
 DUP: We consider a non-duplicating system.
  Trs:
   {
      mark(U12(X1, X2, X3)) -> active(U12(mark(X1), X2, X3)),
                 mark(tt()) -> active(tt()),
      mark(U11(X1, X2, X3)) -> active(U11(mark(X1), X2, X3)),
                 mark(s(X)) -> active(s(mark(X))),
         mark(plus(X1, X2)) -> active(plus(mark(X1), mark(X2))),
                  mark(0()) -> active(0()),
      U12(X1, X2, mark(X3)) -> U12(X1, X2, X3),
    U12(X1, X2, active(X3)) -> U12(X1, X2, X3),
      U12(X1, mark(X2), X3) -> U12(X1, X2, X3),
    U12(X1, active(X2), X3) -> U12(X1, X2, X3),
      U12(mark(X1), X2, X3) -> U12(X1, X2, X3),
    U12(active(X1), X2, X3) -> U12(X1, X2, X3),
    active(U12(tt(), M, N)) -> mark(s(plus(N, M))),
    active(U11(tt(), M, N)) -> mark(U12(tt(), M, N)),
      active(plus(N, s(M))) -> mark(U11(tt(), M, N)),
       active(plus(N, 0())) -> mark(N),
      U11(X1, X2, mark(X3)) -> U11(X1, X2, X3),
    U11(X1, X2, active(X3)) -> U11(X1, X2, X3),
      U11(X1, mark(X2), X3) -> U11(X1, X2, X3),
    U11(X1, active(X2), X3) -> U11(X1, X2, X3),
      U11(mark(X1), X2, X3) -> U11(X1, X2, X3),
    U11(active(X1), X2, X3) -> U11(X1, X2, X3),
                 s(mark(X)) -> s(X),
               s(active(X)) -> s(X),
         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)
   }
  Fail