MAYBE
Time: 0.115890
TRS:
 {         a__first(X1, X2) -> first(X1, X2),
           a__first(0(), X) -> nil(),
  a__first(s X, cons(Y, Z)) -> cons(mark Y, first(X, Z)),
                 mark nil() -> nil(),
                   mark 0() -> 0(),
          mark cons(X1, X2) -> cons(mark X1, X2),
         mark first(X1, X2) -> a__first(mark X1, mark X2),
                   mark s X -> s mark X,
                mark from X -> a__from mark X,
                  a__from X -> cons(mark X, from s X),
                  a__from X -> from X}
 DP:
  DP:
   {a__first#(s X, cons(Y, Z)) -> mark# Y,
            mark# cons(X1, X2) -> mark# X1,
           mark# first(X1, X2) -> a__first#(mark X1, mark X2),
           mark# first(X1, X2) -> mark# X1,
           mark# first(X1, X2) -> mark# X2,
                     mark# s X -> mark# X,
                  mark# from X -> mark# X,
                  mark# from X -> a__from# mark X,
                    a__from# X -> mark# X}
  TRS:
  {         a__first(X1, X2) -> first(X1, X2),
            a__first(0(), X) -> nil(),
   a__first(s X, cons(Y, Z)) -> cons(mark Y, first(X, Z)),
                  mark nil() -> nil(),
                    mark 0() -> 0(),
           mark cons(X1, X2) -> cons(mark X1, X2),
          mark first(X1, X2) -> a__first(mark X1, mark X2),
                    mark s X -> s mark X,
                 mark from X -> a__from mark X,
                   a__from X -> cons(mark X, from s X),
                   a__from X -> from X}
  UR:
   {         a__first(X1, X2) -> first(X1, X2),
             a__first(0(), X) -> nil(),
    a__first(s X, cons(Y, Z)) -> cons(mark Y, first(X, Z)),
                   mark nil() -> nil(),
                     mark 0() -> 0(),
            mark cons(X1, X2) -> cons(mark X1, X2),
           mark first(X1, X2) -> a__first(mark X1, mark X2),
                     mark s X -> s mark X,
                  mark from X -> a__from mark X,
                    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# from X -> a__from# mark X)
     (mark# from X -> mark# X, mark# from X -> mark# X)
     (mark# from X -> mark# X, mark# s X -> mark# X)
     (mark# from X -> mark# X, mark# first(X1, X2) -> mark# X2)
     (mark# from X -> mark# X, mark# first(X1, X2) -> mark# X1)
     (mark# from X -> mark# X, mark# first(X1, X2) -> a__first#(mark X1, mark X2))
     (mark# from X -> mark# X, mark# cons(X1, X2) -> mark# X1)
     (mark# first(X1, X2) -> mark# X2, mark# from X -> a__from# mark X)
     (mark# first(X1, X2) -> mark# X2, mark# from X -> mark# X)
     (mark# first(X1, X2) -> mark# X2, mark# s X -> mark# X)
     (mark# first(X1, X2) -> mark# X2, mark# first(X1, X2) -> mark# X2)
     (mark# first(X1, X2) -> mark# X2, mark# first(X1, X2) -> mark# X1)
     (mark# first(X1, X2) -> mark# X2, mark# first(X1, X2) -> a__first#(mark X1, mark X2))
     (mark# first(X1, X2) -> mark# X2, mark# cons(X1, X2) -> mark# X1)
     (a__first#(s X, cons(Y, Z)) -> mark# Y, mark# from X -> a__from# mark X)
     (a__first#(s X, cons(Y, Z)) -> mark# Y, mark# from X -> mark# X)
     (a__first#(s X, cons(Y, Z)) -> mark# Y, mark# s X -> mark# X)
     (a__first#(s X, cons(Y, Z)) -> mark# Y, mark# first(X1, X2) -> mark# X2)
     (a__first#(s X, cons(Y, Z)) -> mark# Y, mark# first(X1, X2) -> mark# X1)
     (a__first#(s X, cons(Y, Z)) -> mark# Y, mark# first(X1, X2) -> a__first#(mark X1, mark X2))
     (a__first#(s X, cons(Y, Z)) -> mark# Y, mark# cons(X1, X2) -> mark# X1)
     (mark# first(X1, X2) -> mark# X1, mark# from X -> a__from# mark X)
     (mark# first(X1, X2) -> mark# X1, mark# from X -> mark# X)
     (mark# first(X1, X2) -> mark# X1, mark# s X -> mark# X)
     (mark# first(X1, X2) -> mark# X1, mark# first(X1, X2) -> mark# X2)
     (mark# first(X1, X2) -> mark# X1, mark# first(X1, X2) -> mark# X1)
     (mark# first(X1, X2) -> mark# X1, mark# first(X1, X2) -> a__first#(mark X1, mark X2))
     (mark# first(X1, X2) -> mark# X1, mark# cons(X1, X2) -> mark# X1)
     (mark# first(X1, X2) -> a__first#(mark X1, mark X2), a__first#(s X, cons(Y, Z)) -> mark# Y)
     (mark# cons(X1, X2) -> mark# X1, mark# cons(X1, X2) -> mark# X1)
     (mark# cons(X1, X2) -> mark# X1, mark# first(X1, X2) -> a__first#(mark X1, mark X2))
     (mark# cons(X1, X2) -> mark# X1, mark# first(X1, X2) -> mark# X1)
     (mark# cons(X1, X2) -> mark# X1, mark# first(X1, X2) -> mark# X2)
     (mark# cons(X1, X2) -> mark# X1, mark# s X -> mark# X)
     (mark# cons(X1, X2) -> mark# X1, mark# from X -> mark# X)
     (mark# cons(X1, X2) -> mark# X1, mark# from X -> a__from# mark X)
     (mark# from X -> a__from# mark X, a__from# X -> mark# X)
     (a__from# X -> mark# X, mark# cons(X1, X2) -> mark# X1)
     (a__from# X -> mark# X, mark# first(X1, X2) -> a__first#(mark X1, mark X2))
     (a__from# X -> mark# X, mark# first(X1, X2) -> mark# X1)
     (a__from# X -> mark# X, mark# first(X1, X2) -> mark# X2)
     (a__from# X -> mark# X, mark# s X -> mark# X)
     (a__from# X -> mark# X, mark# from X -> mark# X)
     (a__from# X -> mark# X, mark# from X -> a__from# mark X)
     (mark# s X -> mark# X, mark# cons(X1, X2) -> mark# X1)
     (mark# s X -> mark# X, mark# first(X1, X2) -> a__first#(mark X1, mark X2))
     (mark# s X -> mark# X, mark# first(X1, X2) -> mark# X1)
     (mark# s X -> mark# X, mark# first(X1, X2) -> mark# X2)
     (mark# s X -> mark# X, mark# s X -> mark# X)
     (mark# s X -> mark# X, mark# from X -> mark# X)
     (mark# s X -> mark# X, mark# from X -> a__from# mark X)}
    STATUS:
     arrows: 0.370370
     SCCS (1):
      Scc:
       {a__first#(s X, cons(Y, Z)) -> mark# Y,
                mark# cons(X1, X2) -> mark# X1,
               mark# first(X1, X2) -> a__first#(mark X1, mark X2),
               mark# first(X1, X2) -> mark# X1,
               mark# first(X1, X2) -> mark# X2,
                         mark# s X -> mark# X,
                      mark# from X -> mark# X,
                      mark# from X -> a__from# mark X,
                        a__from# X -> mark# X}
      
      SCC (9):
       Strict:
        {a__first#(s X, cons(Y, Z)) -> mark# Y,
                 mark# cons(X1, X2) -> mark# X1,
                mark# first(X1, X2) -> a__first#(mark X1, mark X2),
                mark# first(X1, X2) -> mark# X1,
                mark# first(X1, X2) -> mark# X2,
                          mark# s X -> mark# X,
                       mark# from X -> mark# X,
                       mark# from X -> a__from# mark X,
                         a__from# X -> mark# X}
       Weak:
       {         a__first(X1, X2) -> first(X1, X2),
                 a__first(0(), X) -> nil(),
        a__first(s X, cons(Y, Z)) -> cons(mark Y, first(X, Z)),
                       mark nil() -> nil(),
                         mark 0() -> 0(),
                mark cons(X1, X2) -> cons(mark X1, X2),
               mark first(X1, X2) -> a__first(mark X1, mark X2),
                         mark s X -> s mark X,
                      mark from X -> a__from mark X,
                        a__from X -> cons(mark X, from s X),
                        a__from X -> from X}
       Open