MAYBE
Time: 0.001604
TRS:
 {         mark cons(X1, X2) -> cons(mark X1, X2),
                 mark from X -> a__from mark X,
                    mark s X -> s mark X,
                  mark 2nd X -> a__2nd mark X,
                    a__2nd X -> 2nd X,
  a__2nd cons(X, cons(Y, Z)) -> mark Y,
                   a__from X -> cons(mark X, from s X),
                   a__from X -> from X}
 DP:
  DP:
   {         mark# cons(X1, X2) -> mark# X1,
                   mark# from X -> mark# X,
                   mark# from X -> a__from# mark X,
                      mark# s X -> mark# X,
                    mark# 2nd X -> mark# X,
                    mark# 2nd X -> a__2nd# mark X,
    a__2nd# cons(X, cons(Y, Z)) -> mark# Y,
                     a__from# X -> mark# X}
  TRS:
  {         mark cons(X1, X2) -> cons(mark X1, X2),
                  mark from X -> a__from mark X,
                     mark s X -> s mark X,
                   mark 2nd X -> a__2nd mark X,
                     a__2nd X -> 2nd X,
   a__2nd cons(X, cons(Y, Z)) -> mark Y,
                    a__from X -> cons(mark X, from s X),
                    a__from X -> from X}
  UR:
   {         mark cons(X1, X2) -> cons(mark X1, X2),
                   mark from X -> a__from mark X,
                      mark s X -> s mark X,
                    mark 2nd X -> a__2nd mark X,
                      a__2nd X -> 2nd X,
    a__2nd cons(X, cons(Y, Z)) -> mark Y,
                     a__from X -> cons(mark X, from s X),
                     a__from X -> from X,
                       a(x, y) -> x,
                       a(x, y) -> y}
   EDG:
    {(mark# from X -> a__from# mark X, a__from# X -> mark# X)
     (mark# from X -> mark# X, mark# 2nd X -> a__2nd# mark X)
     (mark# from X -> mark# X, mark# 2nd X -> mark# X)
     (mark# from X -> mark# X, mark# s X -> mark# X)
     (mark# from X -> mark# X, mark# from X -> a__from# mark X)
     (mark# from X -> mark# X, mark# from X -> mark# X)
     (mark# from X -> mark# X, mark# cons(X1, X2) -> mark# X1)
     (mark# 2nd X -> mark# X, mark# 2nd X -> a__2nd# mark X)
     (mark# 2nd X -> mark# X, mark# 2nd X -> mark# X)
     (mark# 2nd X -> mark# X, mark# s X -> mark# X)
     (mark# 2nd X -> mark# X, mark# from X -> a__from# mark X)
     (mark# 2nd X -> mark# X, mark# from X -> mark# X)
     (mark# 2nd X -> mark# X, mark# cons(X1, X2) -> mark# X1)
     (mark# cons(X1, X2) -> mark# X1, mark# 2nd X -> a__2nd# mark X)
     (mark# cons(X1, X2) -> mark# X1, mark# 2nd X -> mark# X)
     (mark# cons(X1, X2) -> mark# X1, mark# s X -> mark# X)
     (mark# cons(X1, X2) -> mark# X1, mark# from X -> a__from# mark X)
     (mark# cons(X1, X2) -> mark# X1, mark# from X -> mark# X)
     (mark# cons(X1, X2) -> mark# X1, mark# cons(X1, X2) -> mark# X1)
     (a__from# X -> mark# X, mark# cons(X1, X2) -> mark# X1)
     (a__from# X -> mark# X, mark# from X -> mark# X)
     (a__from# X -> mark# X, mark# from X -> a__from# mark X)
     (a__from# X -> mark# X, mark# s X -> mark# X)
     (a__from# X -> mark# X, mark# 2nd X -> mark# X)
     (a__from# X -> mark# X, mark# 2nd X -> a__2nd# mark X)
     (mark# s X -> mark# X, mark# cons(X1, X2) -> mark# X1)
     (mark# s X -> mark# X, mark# from X -> mark# X)
     (mark# s X -> mark# X, mark# from X -> a__from# mark X)
     (mark# s X -> mark# X, mark# s X -> mark# X)
     (mark# s X -> mark# X, mark# 2nd X -> mark# X)
     (mark# s X -> mark# X, mark# 2nd X -> a__2nd# mark X)
     (mark# 2nd X -> a__2nd# mark X, a__2nd# cons(X, cons(Y, Z)) -> mark# Y)
     (a__2nd# cons(X, cons(Y, Z)) -> mark# Y, mark# cons(X1, X2) -> mark# X1)
     (a__2nd# cons(X, cons(Y, Z)) -> mark# Y, mark# from X -> mark# X)
     (a__2nd# cons(X, cons(Y, Z)) -> mark# Y, mark# from X -> a__from# mark X)
     (a__2nd# cons(X, cons(Y, Z)) -> mark# Y, mark# s X -> mark# X)
     (a__2nd# cons(X, cons(Y, Z)) -> mark# Y, mark# 2nd X -> mark# X)
     (a__2nd# cons(X, cons(Y, Z)) -> mark# Y, mark# 2nd X -> a__2nd# mark X)}
    STATUS:
     arrows: 0.406250
     SCCS (1):
      Scc:
       {         mark# cons(X1, X2) -> mark# X1,
                       mark# from X -> mark# X,
                       mark# from X -> a__from# mark X,
                          mark# s X -> mark# X,
                        mark# 2nd X -> mark# X,
                        mark# 2nd X -> a__2nd# mark X,
        a__2nd# cons(X, cons(Y, Z)) -> mark# Y,
                         a__from# X -> mark# X}
      
      SCC (8):
       Strict:
        {         mark# cons(X1, X2) -> mark# X1,
                        mark# from X -> mark# X,
                        mark# from X -> a__from# mark X,
                           mark# s X -> mark# X,
                         mark# 2nd X -> mark# X,
                         mark# 2nd X -> a__2nd# mark X,
         a__2nd# cons(X, cons(Y, Z)) -> mark# Y,
                          a__from# X -> mark# X}
       Weak:
       {         mark cons(X1, X2) -> cons(mark X1, X2),
                       mark from X -> a__from mark X,
                          mark s X -> s mark X,
                        mark 2nd X -> a__2nd mark X,
                          a__2nd X -> 2nd X,
        a__2nd cons(X, cons(Y, Z)) -> mark Y,
                         a__from X -> cons(mark X, from s X),
                         a__from X -> from X}
       Open