MAYBE
Time: 0.006923
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}
  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