MAYBE
Time: 0.007725
TRS:
 {              mark true() -> true(),
               mark false() -> false(),
                   mark 0() -> 0(),
                   mark s X -> s X,
           mark add(X1, X2) -> a__add(mark X1, X2),
                 mark nil() -> nil(),
          mark cons(X1, X2) -> cons(X1, X2),
         mark first(X1, X2) -> a__first(mark X1, mark X2),
                mark from X -> a__from X,
           mark and(X1, X2) -> a__and(mark X1, X2),
        mark if(X1, X2, X3) -> a__if(mark X1, X2, X3),
             a__and(X1, X2) -> and(X1, X2),
          a__and(true(), X) -> mark X,
         a__and(false(), Y) -> false(),
          a__if(X1, X2, X3) -> if(X1, X2, X3),
        a__if(true(), X, Y) -> mark X,
       a__if(false(), X, Y) -> mark Y,
             a__add(X1, X2) -> add(X1, X2),
             a__add(0(), X) -> mark X,
             a__add(s X, Y) -> s add(X, Y),
           a__first(X1, X2) -> first(X1, X2),
           a__first(0(), X) -> nil(),
  a__first(s X, cons(Y, Z)) -> cons(Y, first(X, Z)),
                  a__from X -> cons(X, from s X),
                  a__from X -> from X}
 DP:
  DP:
   {    mark# add(X1, X2) -> mark# X1,
        mark# add(X1, X2) -> a__add#(mark X1, X2),
      mark# first(X1, X2) -> mark# X1,
      mark# first(X1, X2) -> mark# X2,
      mark# first(X1, X2) -> a__first#(mark X1, mark X2),
             mark# from X -> a__from# X,
        mark# and(X1, X2) -> mark# X1,
        mark# and(X1, X2) -> a__and#(mark X1, X2),
     mark# if(X1, X2, X3) -> mark# X1,
     mark# if(X1, X2, X3) -> a__if#(mark X1, X2, X3),
       a__and#(true(), X) -> mark# X,
     a__if#(true(), X, Y) -> mark# X,
    a__if#(false(), X, Y) -> mark# Y,
          a__add#(0(), X) -> mark# X}
  TRS:
  {              mark true() -> true(),
                mark false() -> false(),
                    mark 0() -> 0(),
                    mark s X -> s X,
            mark add(X1, X2) -> a__add(mark X1, X2),
                  mark nil() -> nil(),
           mark cons(X1, X2) -> cons(X1, X2),
          mark first(X1, X2) -> a__first(mark X1, mark X2),
                 mark from X -> a__from X,
            mark and(X1, X2) -> a__and(mark X1, X2),
         mark if(X1, X2, X3) -> a__if(mark X1, X2, X3),
              a__and(X1, X2) -> and(X1, X2),
           a__and(true(), X) -> mark X,
          a__and(false(), Y) -> false(),
           a__if(X1, X2, X3) -> if(X1, X2, X3),
         a__if(true(), X, Y) -> mark X,
        a__if(false(), X, Y) -> mark Y,
              a__add(X1, X2) -> add(X1, X2),
              a__add(0(), X) -> mark X,
              a__add(s X, Y) -> s add(X, Y),
            a__first(X1, X2) -> first(X1, X2),
            a__first(0(), X) -> nil(),
   a__first(s X, cons(Y, Z)) -> cons(Y, first(X, Z)),
                   a__from X -> cons(X, from s X),
                   a__from X -> from X}
  EDG:
   {(mark# first(X1, X2) -> mark# X1, mark# if(X1, X2, X3) -> a__if#(mark X1, X2, X3))
    (mark# first(X1, X2) -> mark# X1, mark# if(X1, X2, X3) -> mark# X1)
    (mark# first(X1, X2) -> mark# X1, mark# and(X1, X2) -> a__and#(mark X1, X2))
    (mark# first(X1, X2) -> mark# X1, mark# and(X1, X2) -> mark# X1)
    (mark# first(X1, X2) -> mark# X1, mark# from X -> a__from# X)
    (mark# first(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# first(X1, X2) -> mark# X1, mark# first(X1, X2) -> mark# X1)
    (mark# first(X1, X2) -> mark# X1, mark# add(X1, X2) -> a__add#(mark X1, X2))
    (mark# first(X1, X2) -> mark# X1, mark# add(X1, X2) -> mark# X1)
    (mark# if(X1, X2, X3) -> mark# X1, mark# if(X1, X2, X3) -> a__if#(mark X1, X2, X3))
    (mark# if(X1, X2, X3) -> mark# X1, mark# if(X1, X2, X3) -> mark# X1)
    (mark# if(X1, X2, X3) -> mark# X1, mark# and(X1, X2) -> a__and#(mark X1, X2))
    (mark# if(X1, X2, X3) -> mark# X1, mark# and(X1, X2) -> mark# X1)
    (mark# if(X1, X2, X3) -> mark# X1, mark# from X -> a__from# X)
    (mark# if(X1, X2, X3) -> mark# X1, mark# first(X1, X2) -> a__first#(mark X1, mark X2))
    (mark# if(X1, X2, X3) -> mark# X1, mark# first(X1, X2) -> mark# X2)
    (mark# if(X1, X2, X3) -> mark# X1, mark# first(X1, X2) -> mark# X1)
    (mark# if(X1, X2, X3) -> mark# X1, mark# add(X1, X2) -> a__add#(mark X1, X2))
    (mark# if(X1, X2, X3) -> mark# X1, mark# add(X1, X2) -> mark# X1)
    (mark# first(X1, X2) -> mark# X2, mark# if(X1, X2, X3) -> a__if#(mark X1, X2, X3))
    (mark# first(X1, X2) -> mark# X2, mark# if(X1, X2, X3) -> mark# X1)
    (mark# first(X1, X2) -> mark# X2, mark# and(X1, X2) -> a__and#(mark X1, X2))
    (mark# first(X1, X2) -> mark# X2, mark# and(X1, X2) -> mark# X1)
    (mark# first(X1, X2) -> mark# X2, mark# from X -> a__from# X)
    (mark# first(X1, X2) -> mark# X2, mark# first(X1, X2) -> a__first#(mark X1, mark X2))
    (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# add(X1, X2) -> a__add#(mark X1, X2))
    (mark# first(X1, X2) -> mark# X2, mark# add(X1, X2) -> mark# X1)
    (a__if#(true(), X, Y) -> mark# X, mark# if(X1, X2, X3) -> a__if#(mark X1, X2, X3))
    (a__if#(true(), X, Y) -> mark# X, mark# if(X1, X2, X3) -> mark# X1)
    (a__if#(true(), X, Y) -> mark# X, mark# and(X1, X2) -> a__and#(mark X1, X2))
    (a__if#(true(), X, Y) -> mark# X, mark# and(X1, X2) -> mark# X1)
    (a__if#(true(), X, Y) -> mark# X, mark# from X -> a__from# X)
    (a__if#(true(), X, Y) -> mark# X, mark# first(X1, X2) -> a__first#(mark X1, mark X2))
    (a__if#(true(), X, Y) -> mark# X, mark# first(X1, X2) -> mark# X2)
    (a__if#(true(), X, Y) -> mark# X, mark# first(X1, X2) -> mark# X1)
    (a__if#(true(), X, Y) -> mark# X, mark# add(X1, X2) -> a__add#(mark X1, X2))
    (a__if#(true(), X, Y) -> mark# X, mark# add(X1, X2) -> mark# X1)
    (mark# add(X1, X2) -> a__add#(mark X1, X2), a__add#(0(), X) -> mark# X)
    (mark# if(X1, X2, X3) -> a__if#(mark X1, X2, X3), a__if#(false(), X, Y) -> mark# Y)
    (mark# if(X1, X2, X3) -> a__if#(mark X1, X2, X3), a__if#(true(), X, Y) -> mark# X)
    (mark# and(X1, X2) -> a__and#(mark X1, X2), a__and#(true(), X) -> mark# X)
    (a__add#(0(), X) -> mark# X, mark# add(X1, X2) -> mark# X1)
    (a__add#(0(), X) -> mark# X, mark# add(X1, X2) -> a__add#(mark X1, X2))
    (a__add#(0(), X) -> mark# X, mark# first(X1, X2) -> mark# X1)
    (a__add#(0(), X) -> mark# X, mark# first(X1, X2) -> mark# X2)
    (a__add#(0(), X) -> mark# X, mark# first(X1, X2) -> a__first#(mark X1, mark X2))
    (a__add#(0(), X) -> mark# X, mark# from X -> a__from# X)
    (a__add#(0(), X) -> mark# X, mark# and(X1, X2) -> mark# X1)
    (a__add#(0(), X) -> mark# X, mark# and(X1, X2) -> a__and#(mark X1, X2))
    (a__add#(0(), X) -> mark# X, mark# if(X1, X2, X3) -> mark# X1)
    (a__add#(0(), X) -> mark# X, mark# if(X1, X2, X3) -> a__if#(mark X1, X2, X3))
    (a__and#(true(), X) -> mark# X, mark# add(X1, X2) -> mark# X1)
    (a__and#(true(), X) -> mark# X, mark# add(X1, X2) -> a__add#(mark X1, X2))
    (a__and#(true(), X) -> mark# X, mark# first(X1, X2) -> mark# X1)
    (a__and#(true(), X) -> mark# X, mark# first(X1, X2) -> mark# X2)
    (a__and#(true(), X) -> mark# X, mark# first(X1, X2) -> a__first#(mark X1, mark X2))
    (a__and#(true(), X) -> mark# X, mark# from X -> a__from# X)
    (a__and#(true(), X) -> mark# X, mark# and(X1, X2) -> mark# X1)
    (a__and#(true(), X) -> mark# X, mark# and(X1, X2) -> a__and#(mark X1, X2))
    (a__and#(true(), X) -> mark# X, mark# if(X1, X2, X3) -> mark# X1)
    (a__and#(true(), X) -> mark# X, mark# if(X1, X2, X3) -> a__if#(mark X1, X2, X3))
    (a__if#(false(), X, Y) -> mark# Y, mark# add(X1, X2) -> mark# X1)
    (a__if#(false(), X, Y) -> mark# Y, mark# add(X1, X2) -> a__add#(mark X1, X2))
    (a__if#(false(), X, Y) -> mark# Y, mark# first(X1, X2) -> mark# X1)
    (a__if#(false(), X, Y) -> mark# Y, mark# first(X1, X2) -> mark# X2)
    (a__if#(false(), X, Y) -> mark# Y, mark# first(X1, X2) -> a__first#(mark X1, mark X2))
    (a__if#(false(), X, Y) -> mark# Y, mark# from X -> a__from# X)
    (a__if#(false(), X, Y) -> mark# Y, mark# and(X1, X2) -> mark# X1)
    (a__if#(false(), X, Y) -> mark# Y, mark# and(X1, X2) -> a__and#(mark X1, X2))
    (a__if#(false(), X, Y) -> mark# Y, mark# if(X1, X2, X3) -> mark# X1)
    (a__if#(false(), X, Y) -> mark# Y, mark# if(X1, X2, X3) -> a__if#(mark X1, X2, X3))
    (mark# and(X1, X2) -> mark# X1, mark# add(X1, X2) -> mark# X1)
    (mark# and(X1, X2) -> mark# X1, mark# add(X1, X2) -> a__add#(mark X1, X2))
    (mark# and(X1, X2) -> mark# X1, mark# first(X1, X2) -> mark# X1)
    (mark# and(X1, X2) -> mark# X1, mark# first(X1, X2) -> mark# X2)
    (mark# and(X1, X2) -> mark# X1, mark# first(X1, X2) -> a__first#(mark X1, mark X2))
    (mark# and(X1, X2) -> mark# X1, mark# from X -> a__from# X)
    (mark# and(X1, X2) -> mark# X1, mark# and(X1, X2) -> mark# X1)
    (mark# and(X1, X2) -> mark# X1, mark# and(X1, X2) -> a__and#(mark X1, X2))
    (mark# and(X1, X2) -> mark# X1, mark# if(X1, X2, X3) -> mark# X1)
    (mark# and(X1, X2) -> mark# X1, mark# if(X1, X2, X3) -> a__if#(mark X1, X2, X3))
    (mark# add(X1, X2) -> mark# X1, mark# add(X1, X2) -> mark# X1)
    (mark# add(X1, X2) -> mark# X1, mark# add(X1, X2) -> a__add#(mark X1, X2))
    (mark# add(X1, X2) -> mark# X1, mark# first(X1, X2) -> mark# X1)
    (mark# add(X1, X2) -> mark# X1, mark# first(X1, X2) -> mark# X2)
    (mark# add(X1, X2) -> mark# X1, mark# first(X1, X2) -> a__first#(mark X1, mark X2))
    (mark# add(X1, X2) -> mark# X1, mark# from X -> a__from# X)
    (mark# add(X1, X2) -> mark# X1, mark# and(X1, X2) -> mark# X1)
    (mark# add(X1, X2) -> mark# X1, mark# and(X1, X2) -> a__and#(mark X1, X2))
    (mark# add(X1, X2) -> mark# X1, mark# if(X1, X2, X3) -> mark# X1)
    (mark# add(X1, X2) -> mark# X1, mark# if(X1, X2, X3) -> a__if#(mark X1, X2, X3))}
   STATUS:
    arrows: 0.520408
    SCCS (1):
     Scc:
      {    mark# add(X1, X2) -> mark# X1,
           mark# add(X1, X2) -> a__add#(mark X1, X2),
         mark# first(X1, X2) -> mark# X1,
         mark# first(X1, X2) -> mark# X2,
           mark# and(X1, X2) -> mark# X1,
           mark# and(X1, X2) -> a__and#(mark X1, X2),
        mark# if(X1, X2, X3) -> mark# X1,
        mark# if(X1, X2, X3) -> a__if#(mark X1, X2, X3),
          a__and#(true(), X) -> mark# X,
        a__if#(true(), X, Y) -> mark# X,
       a__if#(false(), X, Y) -> mark# Y,
             a__add#(0(), X) -> mark# X}
     
     SCC (12):
      Strict:
       {    mark# add(X1, X2) -> mark# X1,
            mark# add(X1, X2) -> a__add#(mark X1, X2),
          mark# first(X1, X2) -> mark# X1,
          mark# first(X1, X2) -> mark# X2,
            mark# and(X1, X2) -> mark# X1,
            mark# and(X1, X2) -> a__and#(mark X1, X2),
         mark# if(X1, X2, X3) -> mark# X1,
         mark# if(X1, X2, X3) -> a__if#(mark X1, X2, X3),
           a__and#(true(), X) -> mark# X,
         a__if#(true(), X, Y) -> mark# X,
        a__if#(false(), X, Y) -> mark# Y,
              a__add#(0(), X) -> mark# X}
      Weak:
      {              mark true() -> true(),
                    mark false() -> false(),
                        mark 0() -> 0(),
                        mark s X -> s X,
                mark add(X1, X2) -> a__add(mark X1, X2),
                      mark nil() -> nil(),
               mark cons(X1, X2) -> cons(X1, X2),
              mark first(X1, X2) -> a__first(mark X1, mark X2),
                     mark from X -> a__from X,
                mark and(X1, X2) -> a__and(mark X1, X2),
             mark if(X1, X2, X3) -> a__if(mark X1, X2, X3),
                  a__and(X1, X2) -> and(X1, X2),
               a__and(true(), X) -> mark X,
              a__and(false(), Y) -> false(),
               a__if(X1, X2, X3) -> if(X1, X2, X3),
             a__if(true(), X, Y) -> mark X,
            a__if(false(), X, Y) -> mark Y,
                  a__add(X1, X2) -> add(X1, X2),
                  a__add(0(), X) -> mark X,
                  a__add(s X, Y) -> s add(X, Y),
                a__first(X1, X2) -> first(X1, X2),
                a__first(0(), X) -> nil(),
       a__first(s X, cons(Y, Z)) -> cons(Y, first(X, Z)),
                       a__from X -> cons(X, from s X),
                       a__from X -> from X}
      Open