MAYBE
Time: 0.002923
TRS:
 {         mark cons1(X1, X2) -> cons1(mark X1, mark X2),
            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 cons1(X, cons(Y, Z)) -> mark Y,
           a__2nd cons(X, X1) -> a__2nd cons1(mark X, mark X1),
                    a__from X -> cons(mark X, from s X),
                    a__from X -> from X}
 DP:
  DP:
   {         mark# cons1(X1, X2) -> mark# X1,
             mark# cons1(X1, X2) -> mark# X2,
              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# cons1(X, cons(Y, Z)) -> mark# Y,
             a__2nd# cons(X, X1) -> mark# X,
             a__2nd# cons(X, X1) -> mark# X1,
             a__2nd# cons(X, X1) -> a__2nd# cons1(mark X, mark X1),
                      a__from# X -> mark# X}
  TRS:
  {         mark cons1(X1, X2) -> cons1(mark X1, mark X2),
             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 cons1(X, cons(Y, Z)) -> mark Y,
            a__2nd cons(X, X1) -> a__2nd cons1(mark X, mark X1),
                     a__from X -> cons(mark X, from s X),
                     a__from X -> from X}
  UR:
   {         mark cons1(X1, X2) -> cons1(mark X1, mark X2),
              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 cons1(X, cons(Y, Z)) -> mark Y,
             a__2nd cons(X, X1) -> a__2nd cons1(mark X, mark X1),
                      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 -> 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# from X -> mark# X, mark# cons1(X1, X2) -> mark# X2)
     (mark# from X -> mark# X, mark# cons1(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# 2nd X -> mark# X, mark# cons1(X1, X2) -> mark# X2)
     (mark# 2nd X -> mark# X, mark# cons1(X1, X2) -> mark# X1)
     (a__from# X -> mark# X, mark# 2nd X -> a__2nd# mark X)
     (a__from# X -> mark# X, mark# 2nd X -> mark# X)
     (a__from# X -> mark# X, mark# s X -> mark# X)
     (a__from# X -> mark# X, mark# from X -> a__from# mark X)
     (a__from# X -> mark# X, mark# from X -> mark# X)
     (a__from# X -> mark# X, mark# cons(X1, X2) -> mark# X1)
     (a__from# X -> mark# X, mark# cons1(X1, X2) -> mark# X2)
     (a__from# X -> mark# X, mark# cons1(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)
     (mark# cons(X1, X2) -> mark# X1, mark# cons1(X1, X2) -> mark# X2)
     (mark# cons(X1, X2) -> mark# X1, mark# cons1(X1, X2) -> mark# X1)
     (a__2nd# cons(X, X1) -> a__2nd# cons1(mark X, mark X1), a__2nd# cons(X, X1) -> a__2nd# cons1(mark X, mark X1))
     (a__2nd# cons(X, X1) -> a__2nd# cons1(mark X, mark X1), a__2nd# cons(X, X1) -> mark# X1)
     (a__2nd# cons(X, X1) -> a__2nd# cons1(mark X, mark X1), a__2nd# cons(X, X1) -> mark# X)
     (a__2nd# cons(X, X1) -> a__2nd# cons1(mark X, mark X1), a__2nd# cons1(X, cons(Y, Z)) -> mark# Y)
     (mark# from X -> a__from# mark X, a__from# X -> mark# X)
     (mark# 2nd X -> a__2nd# mark X, a__2nd# cons1(X, cons(Y, Z)) -> mark# Y)
     (mark# 2nd X -> a__2nd# mark X, a__2nd# cons(X, X1) -> mark# X)
     (mark# 2nd X -> a__2nd# mark X, a__2nd# cons(X, X1) -> mark# X1)
     (mark# 2nd X -> a__2nd# mark X, a__2nd# cons(X, X1) -> a__2nd# cons1(mark X, mark X1))
     (mark# cons1(X1, X2) -> mark# X2, mark# cons1(X1, X2) -> mark# X1)
     (mark# cons1(X1, X2) -> mark# X2, mark# cons1(X1, X2) -> mark# X2)
     (mark# cons1(X1, X2) -> mark# X2, mark# cons(X1, X2) -> mark# X1)
     (mark# cons1(X1, X2) -> mark# X2, mark# from X -> mark# X)
     (mark# cons1(X1, X2) -> mark# X2, mark# from X -> a__from# mark X)
     (mark# cons1(X1, X2) -> mark# X2, mark# s X -> mark# X)
     (mark# cons1(X1, X2) -> mark# X2, mark# 2nd X -> mark# X)
     (mark# cons1(X1, X2) -> mark# X2, mark# 2nd X -> a__2nd# mark X)
     (a__2nd# cons(X, X1) -> mark# X1, mark# cons1(X1, X2) -> mark# X1)
     (a__2nd# cons(X, X1) -> mark# X1, mark# cons1(X1, X2) -> mark# X2)
     (a__2nd# cons(X, X1) -> mark# X1, mark# cons(X1, X2) -> mark# X1)
     (a__2nd# cons(X, X1) -> mark# X1, mark# from X -> mark# X)
     (a__2nd# cons(X, X1) -> mark# X1, mark# from X -> a__from# mark X)
     (a__2nd# cons(X, X1) -> mark# X1, mark# s X -> mark# X)
     (a__2nd# cons(X, X1) -> mark# X1, mark# 2nd X -> mark# X)
     (a__2nd# cons(X, X1) -> mark# X1, mark# 2nd X -> a__2nd# mark X)
     (mark# cons1(X1, X2) -> mark# X1, mark# cons1(X1, X2) -> mark# X1)
     (mark# cons1(X1, X2) -> mark# X1, mark# cons1(X1, X2) -> mark# X2)
     (mark# cons1(X1, X2) -> mark# X1, mark# cons(X1, X2) -> mark# X1)
     (mark# cons1(X1, X2) -> mark# X1, mark# from X -> mark# X)
     (mark# cons1(X1, X2) -> mark# X1, mark# from X -> a__from# mark X)
     (mark# cons1(X1, X2) -> mark# X1, mark# s X -> mark# X)
     (mark# cons1(X1, X2) -> mark# X1, mark# 2nd X -> mark# X)
     (mark# cons1(X1, X2) -> mark# X1, mark# 2nd X -> a__2nd# mark X)
     (a__2nd# cons(X, X1) -> mark# X, mark# cons1(X1, X2) -> mark# X1)
     (a__2nd# cons(X, X1) -> mark# X, mark# cons1(X1, X2) -> mark# X2)
     (a__2nd# cons(X, X1) -> mark# X, mark# cons(X1, X2) -> mark# X1)
     (a__2nd# cons(X, X1) -> mark# X, mark# from X -> mark# X)
     (a__2nd# cons(X, X1) -> mark# X, mark# from X -> a__from# mark X)
     (a__2nd# cons(X, X1) -> mark# X, mark# s X -> mark# X)
     (a__2nd# cons(X, X1) -> mark# X, mark# 2nd X -> mark# X)
     (a__2nd# cons(X, X1) -> mark# X, mark# 2nd X -> a__2nd# mark X)
     (mark# s X -> mark# X, mark# cons1(X1, X2) -> mark# X1)
     (mark# s X -> mark# X, mark# cons1(X1, X2) -> mark# X2)
     (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)
     (a__2nd# cons1(X, cons(Y, Z)) -> mark# Y, mark# cons1(X1, X2) -> mark# X1)
     (a__2nd# cons1(X, cons(Y, Z)) -> mark# Y, mark# cons1(X1, X2) -> mark# X2)
     (a__2nd# cons1(X, cons(Y, Z)) -> mark# Y, mark# cons(X1, X2) -> mark# X1)
     (a__2nd# cons1(X, cons(Y, Z)) -> mark# Y, mark# from X -> mark# X)
     (a__2nd# cons1(X, cons(Y, Z)) -> mark# Y, mark# from X -> a__from# mark X)
     (a__2nd# cons1(X, cons(Y, Z)) -> mark# Y, mark# s X -> mark# X)
     (a__2nd# cons1(X, cons(Y, Z)) -> mark# Y, mark# 2nd X -> mark# X)
     (a__2nd# cons1(X, cons(Y, Z)) -> mark# Y, mark# 2nd X -> a__2nd# mark X)}
    STATUS:
     arrows: 0.473373
     SCCS (1):
      Scc:
       {         mark# cons1(X1, X2) -> mark# X1,
                 mark# cons1(X1, X2) -> mark# X2,
                  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# cons1(X, cons(Y, Z)) -> mark# Y,
                 a__2nd# cons(X, X1) -> mark# X,
                 a__2nd# cons(X, X1) -> mark# X1,
                 a__2nd# cons(X, X1) -> a__2nd# cons1(mark X, mark X1),
                          a__from# X -> mark# X}
      
      SCC (13):
       Strict:
        {         mark# cons1(X1, X2) -> mark# X1,
                  mark# cons1(X1, X2) -> mark# X2,
                   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# cons1(X, cons(Y, Z)) -> mark# Y,
                  a__2nd# cons(X, X1) -> mark# X,
                  a__2nd# cons(X, X1) -> mark# X1,
                  a__2nd# cons(X, X1) -> a__2nd# cons1(mark X, mark X1),
                           a__from# X -> mark# X}
       Weak:
       {         mark cons1(X1, X2) -> cons1(mark X1, mark X2),
                  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 cons1(X, cons(Y, Z)) -> mark Y,
                 a__2nd cons(X, X1) -> a__2nd cons1(mark X, mark X1),
                          a__from X -> cons(mark X, from s X),
                          a__from X -> from X}
       Open