MAYBE
Time: 0.019315
TRS:
 {       mark cons(X1, X2) -> active cons(mark X1, X2),
               mark from X -> active from mark X,
                  mark s X -> active s mark X,
                  mark 0() -> active 0(),
             mark length X -> active length X,
                mark nil() -> active nil(),
            mark length1 X -> active length1 X,
         cons(X1, mark X2) -> cons(X1, X2),
       cons(X1, active X2) -> cons(X1, X2),
         cons(mark X1, X2) -> cons(X1, X2),
       cons(active X1, X2) -> cons(X1, X2),
               from mark X -> from X,
             from active X -> from X,
                  s mark X -> s X,
                s active X -> s X,
             active from X -> mark cons(X, from s X),
  active length cons(X, Y) -> mark s length1 Y,
       active length nil() -> mark 0(),
          active length1 X -> mark length X,
             length mark X -> length X,
           length active X -> length X,
            length1 mark X -> length1 X,
          length1 active X -> length1 X}
 DP:
  DP:
   {       mark# cons(X1, X2) -> mark# X1,
           mark# cons(X1, X2) -> cons#(mark X1, X2),
           mark# cons(X1, X2) -> active# cons(mark X1, X2),
                 mark# from X -> mark# X,
                 mark# from X -> from# mark X,
                 mark# from X -> active# from mark X,
                    mark# s X -> mark# X,
                    mark# s X -> s# mark X,
                    mark# s X -> active# s mark X,
                    mark# 0() -> active# 0(),
               mark# length X -> active# length X,
                  mark# nil() -> active# nil(),
              mark# length1 X -> active# length1 X,
           cons#(X1, mark X2) -> cons#(X1, X2),
         cons#(X1, active X2) -> cons#(X1, X2),
           cons#(mark X1, X2) -> cons#(X1, X2),
         cons#(active X1, X2) -> cons#(X1, X2),
                 from# mark X -> from# X,
               from# active X -> from# X,
                    s# mark X -> s# X,
                  s# active X -> s# X,
               active# from X -> mark# cons(X, from s X),
               active# from X -> cons#(X, from s X),
               active# from X -> from# s X,
               active# from X -> s# X,
    active# length cons(X, Y) -> mark# s length1 Y,
    active# length cons(X, Y) -> s# length1 Y,
    active# length cons(X, Y) -> length1# Y,
         active# length nil() -> mark# 0(),
            active# length1 X -> mark# length X,
            active# length1 X -> length# X,
               length# mark X -> length# X,
             length# active X -> length# X,
              length1# mark X -> length1# X,
            length1# active X -> length1# X}
  TRS:
  {       mark cons(X1, X2) -> active cons(mark X1, X2),
                mark from X -> active from mark X,
                   mark s X -> active s mark X,
                   mark 0() -> active 0(),
              mark length X -> active length X,
                 mark nil() -> active nil(),
             mark length1 X -> active length1 X,
          cons(X1, mark X2) -> cons(X1, X2),
        cons(X1, active X2) -> cons(X1, X2),
          cons(mark X1, X2) -> cons(X1, X2),
        cons(active X1, X2) -> cons(X1, X2),
                from mark X -> from X,
              from active X -> from X,
                   s mark X -> s X,
                 s active X -> s X,
              active from X -> mark cons(X, from s X),
   active length cons(X, Y) -> mark s length1 Y,
        active length nil() -> mark 0(),
           active length1 X -> mark length X,
              length mark X -> length X,
            length active X -> length X,
             length1 mark X -> length1 X,
           length1 active X -> length1 X}
  EDG:
   {(active# from X -> cons#(X, from s X), cons#(active X1, X2) -> cons#(X1, X2))
    (active# from X -> cons#(X, from s X), cons#(mark X1, X2) -> cons#(X1, X2))
    (mark# from X -> mark# X, mark# length1 X -> active# length1 X)
    (mark# from X -> mark# X, mark# nil() -> active# nil())
    (mark# from X -> mark# X, mark# length X -> active# length X)
    (mark# from X -> mark# X, mark# 0() -> active# 0())
    (mark# from X -> mark# X, mark# s X -> active# s mark X)
    (mark# from X -> mark# X, mark# s X -> s# mark X)
    (mark# from X -> mark# X, mark# s X -> mark# X)
    (mark# from X -> mark# X, mark# from X -> active# from mark X)
    (mark# from X -> mark# X, mark# from X -> from# mark X)
    (mark# from X -> mark# X, mark# from X -> mark# X)
    (mark# from X -> mark# X, mark# cons(X1, X2) -> active# cons(mark X1, X2))
    (mark# from X -> mark# X, mark# cons(X1, X2) -> cons#(mark X1, X2))
    (mark# from X -> mark# X, mark# cons(X1, X2) -> mark# X1)
    (from# mark X -> from# X, from# active X -> from# X)
    (from# mark X -> from# X, from# mark X -> from# X)
    (s# mark X -> s# X, s# active X -> s# X)
    (s# mark X -> s# X, s# mark X -> s# X)
    (active# from X -> s# X, s# active X -> s# X)
    (active# from X -> s# X, s# mark X -> s# X)
    (length# mark X -> length# X, length# active X -> length# X)
    (length# mark X -> length# X, length# mark X -> length# X)
    (length1# mark X -> length1# X, length1# active X -> length1# X)
    (length1# mark X -> length1# X, length1# mark X -> length1# X)
    (mark# cons(X1, X2) -> mark# X1, mark# length1 X -> active# length1 X)
    (mark# cons(X1, X2) -> mark# X1, mark# nil() -> active# nil())
    (mark# cons(X1, X2) -> mark# X1, mark# length X -> active# length X)
    (mark# cons(X1, X2) -> mark# X1, mark# 0() -> active# 0())
    (mark# cons(X1, X2) -> mark# X1, mark# s X -> active# s mark X)
    (mark# cons(X1, X2) -> mark# X1, mark# s X -> s# mark X)
    (mark# cons(X1, X2) -> mark# X1, mark# s X -> mark# X)
    (mark# cons(X1, X2) -> mark# X1, mark# from X -> active# from mark X)
    (mark# cons(X1, X2) -> mark# X1, mark# from X -> from# mark X)
    (mark# cons(X1, X2) -> mark# X1, mark# from X -> mark# X)
    (mark# cons(X1, X2) -> mark# X1, mark# cons(X1, X2) -> active# cons(mark X1, X2))
    (mark# cons(X1, X2) -> mark# X1, mark# cons(X1, X2) -> cons#(mark X1, X2))
    (mark# cons(X1, X2) -> mark# X1, mark# cons(X1, X2) -> mark# X1)
    (active# from X -> mark# cons(X, from s X), mark# cons(X1, X2) -> active# cons(mark X1, X2))
    (active# from X -> mark# cons(X, from s X), mark# cons(X1, X2) -> cons#(mark X1, X2))
    (active# from X -> mark# cons(X, from s X), mark# cons(X1, X2) -> mark# X1)
    (active# length cons(X, Y) -> length1# Y, length1# active X -> length1# X)
    (active# length cons(X, Y) -> length1# Y, length1# mark X -> length1# X)
    (mark# from X -> from# mark X, from# active X -> from# X)
    (mark# from X -> from# mark X, from# mark X -> from# X)
    (mark# length X -> active# length X, active# length nil() -> mark# 0())
    (mark# length X -> active# length X, active# length cons(X, Y) -> length1# Y)
    (mark# length X -> active# length X, active# length cons(X, Y) -> s# length1 Y)
    (mark# length X -> active# length X, active# length cons(X, Y) -> mark# s length1 Y)
    (cons#(X1, mark X2) -> cons#(X1, X2), cons#(active X1, X2) -> cons#(X1, X2))
    (cons#(X1, mark X2) -> cons#(X1, X2), cons#(mark X1, X2) -> cons#(X1, X2))
    (cons#(X1, mark X2) -> cons#(X1, X2), cons#(X1, active X2) -> cons#(X1, X2))
    (cons#(X1, mark X2) -> cons#(X1, X2), cons#(X1, mark X2) -> cons#(X1, X2))
    (cons#(mark X1, X2) -> cons#(X1, X2), cons#(active X1, X2) -> cons#(X1, X2))
    (cons#(mark X1, X2) -> cons#(X1, X2), cons#(mark X1, X2) -> cons#(X1, X2))
    (cons#(mark X1, X2) -> cons#(X1, X2), cons#(X1, active X2) -> cons#(X1, X2))
    (cons#(mark X1, X2) -> cons#(X1, X2), cons#(X1, mark X2) -> cons#(X1, X2))
    (cons#(active X1, X2) -> cons#(X1, X2), cons#(X1, mark X2) -> cons#(X1, X2))
    (cons#(active X1, X2) -> cons#(X1, X2), cons#(X1, active X2) -> cons#(X1, X2))
    (cons#(active X1, X2) -> cons#(X1, X2), cons#(mark X1, X2) -> cons#(X1, X2))
    (cons#(active X1, X2) -> cons#(X1, X2), cons#(active X1, X2) -> cons#(X1, X2))
    (cons#(X1, active X2) -> cons#(X1, X2), cons#(X1, mark X2) -> cons#(X1, X2))
    (cons#(X1, active X2) -> cons#(X1, X2), cons#(X1, active X2) -> cons#(X1, X2))
    (cons#(X1, active X2) -> cons#(X1, X2), cons#(mark X1, X2) -> cons#(X1, X2))
    (cons#(X1, active X2) -> cons#(X1, X2), cons#(active X1, X2) -> cons#(X1, X2))
    (active# length1 X -> mark# length X, mark# length X -> active# length X)
    (mark# length1 X -> active# length1 X, active# length1 X -> mark# length X)
    (mark# length1 X -> active# length1 X, active# length1 X -> length# X)
    (mark# s X -> s# mark X, s# mark X -> s# X)
    (mark# s X -> s# mark X, s# active X -> s# X)
    (active# length cons(X, Y) -> mark# s length1 Y, mark# s X -> mark# X)
    (active# length cons(X, Y) -> mark# s length1 Y, mark# s X -> s# mark X)
    (active# length cons(X, Y) -> mark# s length1 Y, mark# s X -> active# s mark X)
    (mark# from X -> active# from mark X, active# from X -> mark# cons(X, from s X))
    (mark# from X -> active# from mark X, active# from X -> cons#(X, from s X))
    (mark# from X -> active# from mark X, active# from X -> from# s X)
    (mark# from X -> active# from mark X, active# from X -> s# X)
    (mark# cons(X1, X2) -> cons#(mark X1, X2), cons#(X1, mark X2) -> cons#(X1, X2))
    (mark# cons(X1, X2) -> cons#(mark X1, X2), cons#(X1, active X2) -> cons#(X1, X2))
    (mark# cons(X1, X2) -> cons#(mark X1, X2), cons#(mark X1, X2) -> cons#(X1, X2))
    (mark# cons(X1, X2) -> cons#(mark X1, X2), cons#(active X1, X2) -> cons#(X1, X2))
    (length1# active X -> length1# X, length1# mark X -> length1# X)
    (length1# active X -> length1# X, length1# active X -> length1# X)
    (length# active X -> length# X, length# mark X -> length# X)
    (length# active X -> length# X, length# active X -> length# X)
    (active# length1 X -> length# X, length# mark X -> length# X)
    (active# length1 X -> length# X, length# active X -> length# X)
    (s# active X -> s# X, s# mark X -> s# X)
    (s# active X -> s# X, s# active X -> s# X)
    (from# active X -> from# X, from# mark X -> from# X)
    (from# active X -> from# X, from# active X -> from# X)
    (mark# s X -> mark# X, mark# cons(X1, X2) -> mark# X1)
    (mark# s X -> mark# X, mark# cons(X1, X2) -> cons#(mark X1, X2))
    (mark# s X -> mark# X, mark# cons(X1, X2) -> active# cons(mark X1, X2))
    (mark# s X -> mark# X, mark# from X -> mark# X)
    (mark# s X -> mark# X, mark# from X -> from# mark X)
    (mark# s X -> mark# X, mark# from X -> active# from mark X)
    (mark# s X -> mark# X, mark# s X -> mark# X)
    (mark# s X -> mark# X, mark# s X -> s# mark X)
    (mark# s X -> mark# X, mark# s X -> active# s mark X)
    (mark# s X -> mark# X, mark# 0() -> active# 0())
    (mark# s X -> mark# X, mark# length X -> active# length X)
    (mark# s X -> mark# X, mark# nil() -> active# nil())
    (mark# s X -> mark# X, mark# length1 X -> active# length1 X)
    (active# length nil() -> mark# 0(), mark# 0() -> active# 0())}
   STATUS:
    arrows: 0.914286
    SCCS (6):
     Scc:
      {       mark# cons(X1, X2) -> mark# X1,
                    mark# from X -> mark# X,
                    mark# from X -> active# from mark X,
                       mark# s X -> mark# X,
                  mark# length X -> active# length X,
                 mark# length1 X -> active# length1 X,
                  active# from X -> mark# cons(X, from s X),
       active# length cons(X, Y) -> mark# s length1 Y,
               active# length1 X -> mark# length X}
     Scc:
      {  length# mark X -> length# X,
       length# active X -> length# X}
     Scc:
      {  length1# mark X -> length1# X,
       length1# active X -> length1# X}
     Scc:
      {  s# mark X -> s# X,
       s# active X -> s# X}
     Scc:
      {  from# mark X -> from# X,
       from# active X -> from# X}
     Scc:
      {  cons#(X1, mark X2) -> cons#(X1, X2),
       cons#(X1, active X2) -> cons#(X1, X2),
         cons#(mark X1, X2) -> cons#(X1, X2),
       cons#(active X1, X2) -> cons#(X1, X2)}
     
     SCC (9):
      Strict:
       {       mark# cons(X1, X2) -> mark# X1,
                     mark# from X -> mark# X,
                     mark# from X -> active# from mark X,
                        mark# s X -> mark# X,
                   mark# length X -> active# length X,
                  mark# length1 X -> active# length1 X,
                   active# from X -> mark# cons(X, from s X),
        active# length cons(X, Y) -> mark# s length1 Y,
                active# length1 X -> mark# length X}
      Weak:
      {       mark cons(X1, X2) -> active cons(mark X1, X2),
                    mark from X -> active from mark X,
                       mark s X -> active s mark X,
                       mark 0() -> active 0(),
                  mark length X -> active length X,
                     mark nil() -> active nil(),
                 mark length1 X -> active length1 X,
              cons(X1, mark X2) -> cons(X1, X2),
            cons(X1, active X2) -> cons(X1, X2),
              cons(mark X1, X2) -> cons(X1, X2),
            cons(active X1, X2) -> cons(X1, X2),
                    from mark X -> from X,
                  from active X -> from X,
                       s mark X -> s X,
                     s active X -> s X,
                  active from X -> mark cons(X, from s X),
       active length cons(X, Y) -> mark s length1 Y,
            active length nil() -> mark 0(),
               active length1 X -> mark length X,
                  length mark X -> length X,
                length active X -> length X,
                 length1 mark X -> length1 X,
               length1 active X -> length1 X}
      Open
     
     SCC (2):
      Strict:
       {  length# mark X -> length# X,
        length# active X -> length# X}
      Weak:
      {       mark cons(X1, X2) -> active cons(mark X1, X2),
                    mark from X -> active from mark X,
                       mark s X -> active s mark X,
                       mark 0() -> active 0(),
                  mark length X -> active length X,
                     mark nil() -> active nil(),
                 mark length1 X -> active length1 X,
              cons(X1, mark X2) -> cons(X1, X2),
            cons(X1, active X2) -> cons(X1, X2),
              cons(mark X1, X2) -> cons(X1, X2),
            cons(active X1, X2) -> cons(X1, X2),
                    from mark X -> from X,
                  from active X -> from X,
                       s mark X -> s X,
                     s active X -> s X,
                  active from X -> mark cons(X, from s X),
       active length cons(X, Y) -> mark s length1 Y,
            active length nil() -> mark 0(),
               active length1 X -> mark length X,
                  length mark X -> length X,
                length active X -> length X,
                 length1 mark X -> length1 X,
               length1 active X -> length1 X}
      Open
     
     SCC (2):
      Strict:
       {  length1# mark X -> length1# X,
        length1# active X -> length1# X}
      Weak:
      {       mark cons(X1, X2) -> active cons(mark X1, X2),
                    mark from X -> active from mark X,
                       mark s X -> active s mark X,
                       mark 0() -> active 0(),
                  mark length X -> active length X,
                     mark nil() -> active nil(),
                 mark length1 X -> active length1 X,
              cons(X1, mark X2) -> cons(X1, X2),
            cons(X1, active X2) -> cons(X1, X2),
              cons(mark X1, X2) -> cons(X1, X2),
            cons(active X1, X2) -> cons(X1, X2),
                    from mark X -> from X,
                  from active X -> from X,
                       s mark X -> s X,
                     s active X -> s X,
                  active from X -> mark cons(X, from s X),
       active length cons(X, Y) -> mark s length1 Y,
            active length nil() -> mark 0(),
               active length1 X -> mark length X,
                  length mark X -> length X,
                length active X -> length X,
                 length1 mark X -> length1 X,
               length1 active X -> length1 X}
      Open
     
     
     
     
     SCC (2):
      Strict:
       {  s# mark X -> s# X,
        s# active X -> s# X}
      Weak:
      {       mark cons(X1, X2) -> active cons(mark X1, X2),
                    mark from X -> active from mark X,
                       mark s X -> active s mark X,
                       mark 0() -> active 0(),
                  mark length X -> active length X,
                     mark nil() -> active nil(),
                 mark length1 X -> active length1 X,
              cons(X1, mark X2) -> cons(X1, X2),
            cons(X1, active X2) -> cons(X1, X2),
              cons(mark X1, X2) -> cons(X1, X2),
            cons(active X1, X2) -> cons(X1, X2),
                    from mark X -> from X,
                  from active X -> from X,
                       s mark X -> s X,
                     s active X -> s X,
                  active from X -> mark cons(X, from s X),
       active length cons(X, Y) -> mark s length1 Y,
            active length nil() -> mark 0(),
               active length1 X -> mark length X,
                  length mark X -> length X,
                length active X -> length X,
                 length1 mark X -> length1 X,
               length1 active X -> length1 X}
      Open
     
     
     SCC (2):
      Strict:
       {  from# mark X -> from# X,
        from# active X -> from# X}
      Weak:
      {       mark cons(X1, X2) -> active cons(mark X1, X2),
                    mark from X -> active from mark X,
                       mark s X -> active s mark X,
                       mark 0() -> active 0(),
                  mark length X -> active length X,
                     mark nil() -> active nil(),
                 mark length1 X -> active length1 X,
              cons(X1, mark X2) -> cons(X1, X2),
            cons(X1, active X2) -> cons(X1, X2),
              cons(mark X1, X2) -> cons(X1, X2),
            cons(active X1, X2) -> cons(X1, X2),
                    from mark X -> from X,
                  from active X -> from X,
                       s mark X -> s X,
                     s active X -> s X,
                  active from X -> mark cons(X, from s X),
       active length cons(X, Y) -> mark s length1 Y,
            active length nil() -> mark 0(),
               active length1 X -> mark length X,
                  length mark X -> length X,
                length active X -> length X,
                 length1 mark X -> length1 X,
               length1 active X -> length1 X}
      Open
     
     
     
     SCC (4):
      Strict:
       {  cons#(X1, mark X2) -> cons#(X1, X2),
        cons#(X1, active X2) -> cons#(X1, X2),
          cons#(mark X1, X2) -> cons#(X1, X2),
        cons#(active X1, X2) -> cons#(X1, X2)}
      Weak:
      {       mark cons(X1, X2) -> active cons(mark X1, X2),
                    mark from X -> active from mark X,
                       mark s X -> active s mark X,
                       mark 0() -> active 0(),
                  mark length X -> active length X,
                     mark nil() -> active nil(),
                 mark length1 X -> active length1 X,
              cons(X1, mark X2) -> cons(X1, X2),
            cons(X1, active X2) -> cons(X1, X2),
              cons(mark X1, X2) -> cons(X1, X2),
            cons(active X1, X2) -> cons(X1, X2),
                    from mark X -> from X,
                  from active X -> from X,
                       s mark X -> s X,
                     s active X -> s X,
                  active from X -> mark cons(X, from s X),
       active length cons(X, Y) -> mark s length1 Y,
            active length nil() -> mark 0(),
               active length1 X -> mark length X,
                  length mark X -> length X,
                length active X -> length X,
                 length1 mark X -> length1 X,
               length1 active X -> length1 X}
      Open