Problem Transformed CSR 04 LengthOfFiniteLists nosorts C

Tool CaT

Execution Time	Unknown
Answer	YES(?,O(n^1))
Input	Transformed CSR 04 LengthOfFiniteLists nosorts C

stdout:

YES(?,O(n^1))

Problem:
active(zeros()) -> mark(cons(0(),zeros()))
active(and(tt(),X)) -> mark(X)
active(length(nil())) -> mark(0())
active(length(cons(N,L))) -> mark(s(length(L)))
active(cons(X1,X2)) -> cons(active(X1),X2)
active(and(X1,X2)) -> and(active(X1),X2)
active(length(X)) -> length(active(X))
active(s(X)) -> s(active(X))
cons(mark(X1),X2) -> mark(cons(X1,X2))
and(mark(X1),X2) -> mark(and(X1,X2))
length(mark(X)) -> mark(length(X))
s(mark(X)) -> mark(s(X))
proper(zeros()) -> ok(zeros())
proper(cons(X1,X2)) -> cons(proper(X1),proper(X2))
proper(0()) -> ok(0())
proper(and(X1,X2)) -> and(proper(X1),proper(X2))
proper(tt()) -> ok(tt())
proper(length(X)) -> length(proper(X))
proper(nil()) -> ok(nil())
proper(s(X)) -> s(proper(X))
cons(ok(X1),ok(X2)) -> ok(cons(X1,X2))
and(ok(X1),ok(X2)) -> ok(and(X1,X2))
length(ok(X)) -> ok(length(X))
s(ok(X)) -> ok(s(X))
top(mark(X)) -> top(proper(X))
top(ok(X)) -> top(active(X))

Proof:
Bounds Processor:
  bound: 5
  enrichment: match
  automaton:
   final states: {13,12,11,10,9,8,7}
   transitions:
    cons3(36,35) -> 49*
    cons3(45,44) -> 43*
    top1(29) -> 13*
    active3(49) -> 43*
    active1(5) -> 29*
    active1(2) -> 29*
    active1(4) -> 29*
    active1(6) -> 29*
    active1(1) -> 29*
    active1(3) -> 29*
    nil3() -> 50*
    proper1(5) -> 29*
    proper1(2) -> 29*
    proper1(4) -> 29*
    proper1(6) -> 29*
    proper1(1) -> 29*
    proper1(3) -> 29*
    tt3() -> 50*
    ok1(25) -> 25,10
    ok1(15) -> 29,12
    ok1(27) -> 27,11
    ok1(14) -> 29,12
    ok1(21) -> 21,8
    ok1(23) -> 23,9
    03() -> 53*
    s1(5) -> 27*
    s1(2) -> 27*
    s1(4) -> 27*
    s1(6) -> 27*
    s1(1) -> 27*
    s1(3) -> 27*
    zeros3() -> 50*
    length1(5) -> 25*
    length1(2) -> 25*
    length1(4) -> 25*
    length1(6) -> 25*
    length1(1) -> 25*
    length1(3) -> 25*
    ok4(56) -> 43*
    and1(3,1) -> 23*
    and1(3,3) -> 23*
    and1(3,5) -> 23*
    and1(4,2) -> 23*
    and1(4,4) -> 23*
    and1(4,6) -> 23*
    and1(5,1) -> 23*
    and1(5,3) -> 23*
    and1(5,5) -> 23*
    and1(6,2) -> 23*
    and1(1,2) -> 23*
    and1(6,4) -> 23*
    and1(1,4) -> 23*
    and1(6,6) -> 23*
    and1(1,6) -> 23*
    and1(2,1) -> 23*
    and1(2,3) -> 23*
    and1(2,5) -> 23*
    and1(3,2) -> 23*
    and1(3,4) -> 23*
    and1(3,6) -> 23*
    and1(4,1) -> 23*
    and1(4,3) -> 23*
    and1(4,5) -> 23*
    and1(5,2) -> 23*
    and1(5,4) -> 23*
    and1(5,6) -> 23*
    and1(6,1) -> 23*
    and1(1,1) -> 23*
    and1(6,3) -> 23*
    and1(1,3) -> 23*
    and1(6,5) -> 23*
    and1(1,5) -> 23*
    and1(2,2) -> 23*
    and1(2,4) -> 23*
    and1(2,6) -> 23*
    cons4(55,35) -> 43*
    cons4(53,50) -> 56*
    cons1(3,1) -> 21*
    cons1(3,3) -> 21*
    cons1(3,5) -> 21*
    cons1(4,2) -> 21*
    cons1(4,4) -> 21*
    cons1(4,6) -> 21*
    cons1(5,1) -> 21*
    cons1(5,3) -> 21*
    cons1(5,5) -> 21*
    cons1(6,2) -> 21*
    cons1(1,2) -> 21*
    cons1(6,4) -> 21*
    cons1(1,4) -> 21*
    cons1(6,6) -> 21*
    cons1(1,6) -> 21*
    cons1(2,1) -> 21*
    cons1(2,3) -> 21*
    cons1(2,5) -> 21*
    cons1(3,2) -> 21*
    cons1(3,4) -> 21*
    cons1(3,6) -> 21*
    cons1(4,1) -> 21*
    cons1(4,3) -> 21*
    cons1(4,5) -> 21*
    cons1(5,2) -> 21*
    cons1(5,4) -> 21*
    cons1(5,6) -> 21*
    cons1(15,14) -> 16*
    cons1(6,1) -> 21*
    cons1(1,1) -> 21*
    cons1(6,3) -> 21*
    cons1(1,3) -> 21*
    cons1(6,5) -> 21*
    cons1(1,5) -> 21*
    cons1(2,2) -> 21*
    cons1(2,4) -> 21*
    cons1(2,6) -> 21*
    active4(56) -> 59*
    active4(36) -> 55*
    nil1() -> 14*
    top4(59) -> 13*
    tt1() -> 14*
    cons5(60,50) -> 59*
    01() -> 15*
    active5(53) -> 60*
    zeros1() -> 14*
    mark1(25) -> 25,10
    mark1(27) -> 27,11
    mark1(21) -> 21,8
    mark1(16) -> 29,7
    mark1(23) -> 23,9
    top2(30) -> 13*
    active0(5) -> 7*
    active0(2) -> 7*
    active0(4) -> 7*
    active0(6) -> 7*
    active0(1) -> 7*
    active0(3) -> 7*
    active2(15) -> 30*
    active2(14) -> 30*
    zeros0() -> 1*
    proper2(15) -> 39*
    proper2(14) -> 38*
    proper2(16) -> 30*
    mark0(5) -> 2*
    mark0(2) -> 2*
    mark0(4) -> 2*
    mark0(6) -> 2*
    mark0(1) -> 2*
    mark0(3) -> 2*
    cons2(36,35) -> 37*
    cons2(39,38) -> 30*
    cons0(3,1) -> 8*
    cons0(3,3) -> 8*
    cons0(3,5) -> 8*
    cons0(4,2) -> 8*
    cons0(4,4) -> 8*
    cons0(4,6) -> 8*
    cons0(5,1) -> 8*
    cons0(5,3) -> 8*
    cons0(5,5) -> 8*
    cons0(6,2) -> 8*
    cons0(1,2) -> 8*
    cons0(6,4) -> 8*
    cons0(1,4) -> 8*
    cons0(6,6) -> 8*
    cons0(1,6) -> 8*
    cons0(2,1) -> 8*
    cons0(2,3) -> 8*
    cons0(2,5) -> 8*
    cons0(3,2) -> 8*
    cons0(3,4) -> 8*
    cons0(3,6) -> 8*
    cons0(4,1) -> 8*
    cons0(4,3) -> 8*
    cons0(4,5) -> 8*
    cons0(5,2) -> 8*
    cons0(5,4) -> 8*
    cons0(5,6) -> 8*
    cons0(6,1) -> 8*
    cons0(1,1) -> 8*
    cons0(6,3) -> 8*
    cons0(1,3) -> 8*
    cons0(6,5) -> 8*
    cons0(1,5) -> 8*
    cons0(2,2) -> 8*
    cons0(2,4) -> 8*
    cons0(2,6) -> 8*
    mark2(37) -> 30*
    00() -> 3*
    02() -> 36*
    and0(3,1) -> 9*
    and0(3,3) -> 9*
    and0(3,5) -> 9*
    and0(4,2) -> 9*
    and0(4,4) -> 9*
    and0(4,6) -> 9*
    and0(5,1) -> 9*
    and0(5,3) -> 9*
    and0(5,5) -> 9*
    and0(6,2) -> 9*
    and0(1,2) -> 9*
    and0(6,4) -> 9*
    and0(1,4) -> 9*
    and0(6,6) -> 9*
    and0(1,6) -> 9*
    and0(2,1) -> 9*
    and0(2,3) -> 9*
    and0(2,5) -> 9*
    and0(3,2) -> 9*
    and0(3,4) -> 9*
    and0(3,6) -> 9*
    and0(4,1) -> 9*
    and0(4,3) -> 9*
    and0(4,5) -> 9*
    and0(5,2) -> 9*
    and0(5,4) -> 9*
    and0(5,6) -> 9*
    and0(6,1) -> 9*
    and0(1,1) -> 9*
    and0(6,3) -> 9*
    and0(1,3) -> 9*
    and0(6,5) -> 9*
    and0(1,5) -> 9*
    and0(2,2) -> 9*
    and0(2,4) -> 9*
    and0(2,6) -> 9*
    zeros2() -> 35*
    tt0() -> 4*
    top3(43) -> 13*
    length0(5) -> 10*
    length0(2) -> 10*
    length0(4) -> 10*
    length0(6) -> 10*
    length0(1) -> 10*
    length0(3) -> 10*
    proper3(35) -> 44*
    proper3(37) -> 43*
    proper3(36) -> 45*
    nil0() -> 5*
    ok2(35) -> 38*
    ok2(36) -> 39*
    s0(5) -> 11*
    s0(2) -> 11*
    s0(4) -> 11*
    s0(6) -> 11*
    s0(1) -> 11*
    s0(3) -> 11*
    nil2() -> 35*
    proper0(5) -> 12*
    proper0(2) -> 12*
    proper0(4) -> 12*
    proper0(6) -> 12*
    proper0(1) -> 12*
    proper0(3) -> 12*
    tt2() -> 35*
    ok0(5) -> 6*
    ok0(2) -> 6*
    ok0(4) -> 6*
    ok0(6) -> 6*
    ok0(1) -> 6*
    ok0(3) -> 6*
    ok3(50) -> 44*
    ok3(49) -> 30*
    ok3(53) -> 45*
    top0(5) -> 13*
    top0(2) -> 13*
    top0(4) -> 13*
    top0(6) -> 13*
    top0(1) -> 13*
    top0(3) -> 13*
  problem:

  Qed

Tool IRC1

Execution Time	Unknown
Answer	YES(?,O(n^1))
Input	Transformed CSR 04 LengthOfFiniteLists nosorts C

stdout:

YES(?,O(n^1))

Tool IRC2

Execution Time	Unknown
Answer	YES(?,O(n^1))
Input	Transformed CSR 04 LengthOfFiniteLists nosorts C

stdout:

YES(?,O(n^1))

'Fastest (timeout of 60.0 seconds)'
-----------------------------------
Answer:           YES(?,O(n^1))
Input Problem:    innermost runtime-complexity with respect to
  Rules:
    {  active(zeros()) -> mark(cons(0(), zeros()))
     , active(and(tt(), X)) -> mark(X)
     , active(length(nil())) -> mark(0())
     , active(length(cons(N, L))) -> mark(s(length(L)))
     , active(cons(X1, X2)) -> cons(active(X1), X2)
     , active(and(X1, X2)) -> and(active(X1), X2)
     , active(length(X)) -> length(active(X))
     , active(s(X)) -> s(active(X))
     , cons(mark(X1), X2) -> mark(cons(X1, X2))
     , and(mark(X1), X2) -> mark(and(X1, X2))
     , length(mark(X)) -> mark(length(X))
     , s(mark(X)) -> mark(s(X))
     , proper(zeros()) -> ok(zeros())
     , proper(cons(X1, X2)) -> cons(proper(X1), proper(X2))
     , proper(0()) -> ok(0())
     , proper(and(X1, X2)) -> and(proper(X1), proper(X2))
     , proper(tt()) -> ok(tt())
     , proper(length(X)) -> length(proper(X))
     , proper(nil()) -> ok(nil())
     , proper(s(X)) -> s(proper(X))
     , cons(ok(X1), ok(X2)) -> ok(cons(X1, X2))
     , and(ok(X1), ok(X2)) -> ok(and(X1, X2))
     , length(ok(X)) -> ok(length(X))
     , s(ok(X)) -> ok(s(X))
     , top(mark(X)) -> top(proper(X))
     , top(ok(X)) -> top(active(X))}

Proof Output:
  'Bounds with perSymbol-enrichment and initial automaton 'match'' proved the best result:

  Details:
  --------
    'Bounds with perSymbol-enrichment and initial automaton 'match'' succeeded with the following output:
     'Bounds with perSymbol-enrichment and initial automaton 'match''
     ----------------------------------------------------------------
     Answer:           YES(?,O(n^1))
     Input Problem:    innermost runtime-complexity with respect to
       Rules:
         {  active(zeros()) -> mark(cons(0(), zeros()))
          , active(and(tt(), X)) -> mark(X)
          , active(length(nil())) -> mark(0())
          , active(length(cons(N, L))) -> mark(s(length(L)))
          , active(cons(X1, X2)) -> cons(active(X1), X2)
          , active(and(X1, X2)) -> and(active(X1), X2)
          , active(length(X)) -> length(active(X))
          , active(s(X)) -> s(active(X))
          , cons(mark(X1), X2) -> mark(cons(X1, X2))
          , and(mark(X1), X2) -> mark(and(X1, X2))
          , length(mark(X)) -> mark(length(X))
          , s(mark(X)) -> mark(s(X))
          , proper(zeros()) -> ok(zeros())
          , proper(cons(X1, X2)) -> cons(proper(X1), proper(X2))
          , proper(0()) -> ok(0())
          , proper(and(X1, X2)) -> and(proper(X1), proper(X2))
          , proper(tt()) -> ok(tt())
          , proper(length(X)) -> length(proper(X))
          , proper(nil()) -> ok(nil())
          , proper(s(X)) -> s(proper(X))
          , cons(ok(X1), ok(X2)) -> ok(cons(X1, X2))
          , and(ok(X1), ok(X2)) -> ok(and(X1, X2))
          , length(ok(X)) -> ok(length(X))
          , s(ok(X)) -> ok(s(X))
          , top(mark(X)) -> top(proper(X))
          , top(ok(X)) -> top(active(X))}

     Proof Output:
       The problem is match-bounded by 5.
       The enriched problem is compatible with the following automaton:
       {  active_0(2) -> 1
        , active_0(3) -> 1
        , active_0(5) -> 1
        , active_0(7) -> 1
        , active_0(9) -> 1
        , active_0(12) -> 1
        , active_1(2) -> 21
        , active_1(3) -> 21
        , active_1(5) -> 21
        , active_1(7) -> 21
        , active_1(9) -> 21
        , active_1(12) -> 21
        , active_2(15) -> 22
        , active_2(16) -> 22
        , active_3(32) -> 28
        , active_4(24) -> 33
        , active_4(35) -> 36
        , active_5(31) -> 37
        , zeros_0() -> 2
        , zeros_1() -> 16
        , zeros_2() -> 25
        , zeros_3() -> 34
        , mark_0(2) -> 3
        , mark_0(3) -> 3
        , mark_0(5) -> 3
        , mark_0(7) -> 3
        , mark_0(9) -> 3
        , mark_0(12) -> 3
        , mark_1(14) -> 1
        , mark_1(14) -> 21
        , mark_1(17) -> 4
        , mark_1(17) -> 17
        , mark_1(18) -> 6
        , mark_1(18) -> 18
        , mark_1(19) -> 8
        , mark_1(19) -> 19
        , mark_1(20) -> 10
        , mark_1(20) -> 20
        , mark_2(23) -> 22
        , cons_0(2, 2) -> 4
        , cons_0(2, 3) -> 4
        , cons_0(2, 5) -> 4
        , cons_0(2, 7) -> 4
        , cons_0(2, 9) -> 4
        , cons_0(2, 12) -> 4
        , cons_0(3, 2) -> 4
        , cons_0(3, 3) -> 4
        , cons_0(3, 5) -> 4
        , cons_0(3, 7) -> 4
        , cons_0(3, 9) -> 4
        , cons_0(3, 12) -> 4
        , cons_0(5, 2) -> 4
        , cons_0(5, 3) -> 4
        , cons_0(5, 5) -> 4
        , cons_0(5, 7) -> 4
        , cons_0(5, 9) -> 4
        , cons_0(5, 12) -> 4
        , cons_0(7, 2) -> 4
        , cons_0(7, 3) -> 4
        , cons_0(7, 5) -> 4
        , cons_0(7, 7) -> 4
        , cons_0(7, 9) -> 4
        , cons_0(7, 12) -> 4
        , cons_0(9, 2) -> 4
        , cons_0(9, 3) -> 4
        , cons_0(9, 5) -> 4
        , cons_0(9, 7) -> 4
        , cons_0(9, 9) -> 4
        , cons_0(9, 12) -> 4
        , cons_0(12, 2) -> 4
        , cons_0(12, 3) -> 4
        , cons_0(12, 5) -> 4
        , cons_0(12, 7) -> 4
        , cons_0(12, 9) -> 4
        , cons_0(12, 12) -> 4
        , cons_1(2, 2) -> 17
        , cons_1(2, 3) -> 17
        , cons_1(2, 5) -> 17
        , cons_1(2, 7) -> 17
        , cons_1(2, 9) -> 17
        , cons_1(2, 12) -> 17
        , cons_1(3, 2) -> 17
        , cons_1(3, 3) -> 17
        , cons_1(3, 5) -> 17
        , cons_1(3, 7) -> 17
        , cons_1(3, 9) -> 17
        , cons_1(3, 12) -> 17
        , cons_1(5, 2) -> 17
        , cons_1(5, 3) -> 17
        , cons_1(5, 5) -> 17
        , cons_1(5, 7) -> 17
        , cons_1(5, 9) -> 17
        , cons_1(5, 12) -> 17
        , cons_1(7, 2) -> 17
        , cons_1(7, 3) -> 17
        , cons_1(7, 5) -> 17
        , cons_1(7, 7) -> 17
        , cons_1(7, 9) -> 17
        , cons_1(7, 12) -> 17
        , cons_1(9, 2) -> 17
        , cons_1(9, 3) -> 17
        , cons_1(9, 5) -> 17
        , cons_1(9, 7) -> 17
        , cons_1(9, 9) -> 17
        , cons_1(9, 12) -> 17
        , cons_1(12, 2) -> 17
        , cons_1(12, 3) -> 17
        , cons_1(12, 5) -> 17
        , cons_1(12, 7) -> 17
        , cons_1(12, 9) -> 17
        , cons_1(12, 12) -> 17
        , cons_1(15, 16) -> 14
        , cons_2(24, 25) -> 23
        , cons_2(26, 27) -> 22
        , cons_3(24, 25) -> 32
        , cons_3(29, 30) -> 28
        , cons_4(31, 34) -> 35
        , cons_4(33, 25) -> 28
        , cons_5(37, 34) -> 36
        , 0_0() -> 5
        , 0_1() -> 15
        , 0_2() -> 24
        , 0_3() -> 31
        , and_0(2, 2) -> 6
        , and_0(2, 3) -> 6
        , and_0(2, 5) -> 6
        , and_0(2, 7) -> 6
        , and_0(2, 9) -> 6
        , and_0(2, 12) -> 6
        , and_0(3, 2) -> 6
        , and_0(3, 3) -> 6
        , and_0(3, 5) -> 6
        , and_0(3, 7) -> 6
        , and_0(3, 9) -> 6
        , and_0(3, 12) -> 6
        , and_0(5, 2) -> 6
        , and_0(5, 3) -> 6
        , and_0(5, 5) -> 6
        , and_0(5, 7) -> 6
        , and_0(5, 9) -> 6
        , and_0(5, 12) -> 6
        , and_0(7, 2) -> 6
        , and_0(7, 3) -> 6
        , and_0(7, 5) -> 6
        , and_0(7, 7) -> 6
        , and_0(7, 9) -> 6
        , and_0(7, 12) -> 6
        , and_0(9, 2) -> 6
        , and_0(9, 3) -> 6
        , and_0(9, 5) -> 6
        , and_0(9, 7) -> 6
        , and_0(9, 9) -> 6
        , and_0(9, 12) -> 6
        , and_0(12, 2) -> 6
        , and_0(12, 3) -> 6
        , and_0(12, 5) -> 6
        , and_0(12, 7) -> 6
        , and_0(12, 9) -> 6
        , and_0(12, 12) -> 6
        , and_1(2, 2) -> 18
        , and_1(2, 3) -> 18
        , and_1(2, 5) -> 18
        , and_1(2, 7) -> 18
        , and_1(2, 9) -> 18
        , and_1(2, 12) -> 18
        , and_1(3, 2) -> 18
        , and_1(3, 3) -> 18
        , and_1(3, 5) -> 18
        , and_1(3, 7) -> 18
        , and_1(3, 9) -> 18
        , and_1(3, 12) -> 18
        , and_1(5, 2) -> 18
        , and_1(5, 3) -> 18
        , and_1(5, 5) -> 18
        , and_1(5, 7) -> 18
        , and_1(5, 9) -> 18
        , and_1(5, 12) -> 18
        , and_1(7, 2) -> 18
        , and_1(7, 3) -> 18
        , and_1(7, 5) -> 18
        , and_1(7, 7) -> 18
        , and_1(7, 9) -> 18
        , and_1(7, 12) -> 18
        , and_1(9, 2) -> 18
        , and_1(9, 3) -> 18
        , and_1(9, 5) -> 18
        , and_1(9, 7) -> 18
        , and_1(9, 9) -> 18
        , and_1(9, 12) -> 18
        , and_1(12, 2) -> 18
        , and_1(12, 3) -> 18
        , and_1(12, 5) -> 18
        , and_1(12, 7) -> 18
        , and_1(12, 9) -> 18
        , and_1(12, 12) -> 18
        , tt_0() -> 7
        , tt_1() -> 15
        , tt_2() -> 24
        , tt_3() -> 31
        , length_0(2) -> 8
        , length_0(3) -> 8
        , length_0(5) -> 8
        , length_0(7) -> 8
        , length_0(9) -> 8
        , length_0(12) -> 8
        , length_1(2) -> 19
        , length_1(3) -> 19
        , length_1(5) -> 19
        , length_1(7) -> 19
        , length_1(9) -> 19
        , length_1(12) -> 19
        , nil_0() -> 9
        , nil_1() -> 15
        , nil_2() -> 24
        , nil_3() -> 31
        , s_0(2) -> 10
        , s_0(3) -> 10
        , s_0(5) -> 10
        , s_0(7) -> 10
        , s_0(9) -> 10
        , s_0(12) -> 10
        , s_1(2) -> 20
        , s_1(3) -> 20
        , s_1(5) -> 20
        , s_1(7) -> 20
        , s_1(9) -> 20
        , s_1(12) -> 20
        , proper_0(2) -> 11
        , proper_0(3) -> 11
        , proper_0(5) -> 11
        , proper_0(7) -> 11
        , proper_0(9) -> 11
        , proper_0(12) -> 11
        , proper_1(2) -> 21
        , proper_1(3) -> 21
        , proper_1(5) -> 21
        , proper_1(7) -> 21
        , proper_1(9) -> 21
        , proper_1(12) -> 21
        , proper_2(14) -> 22
        , proper_2(15) -> 26
        , proper_2(16) -> 27
        , proper_3(23) -> 28
        , proper_3(24) -> 29
        , proper_3(25) -> 30
        , ok_0(2) -> 12
        , ok_0(3) -> 12
        , ok_0(5) -> 12
        , ok_0(7) -> 12
        , ok_0(9) -> 12
        , ok_0(12) -> 12
        , ok_1(15) -> 11
        , ok_1(15) -> 21
        , ok_1(16) -> 11
        , ok_1(16) -> 21
        , ok_1(17) -> 4
        , ok_1(17) -> 17
        , ok_1(18) -> 6
        , ok_1(18) -> 18
        , ok_1(19) -> 8
        , ok_1(19) -> 19
        , ok_1(20) -> 10
        , ok_1(20) -> 20
        , ok_2(24) -> 26
        , ok_2(25) -> 27
        , ok_3(31) -> 29
        , ok_3(32) -> 22
        , ok_3(34) -> 30
        , ok_4(35) -> 28
        , top_0(2) -> 13
        , top_0(3) -> 13
        , top_0(5) -> 13
        , top_0(7) -> 13
        , top_0(9) -> 13
        , top_0(12) -> 13
        , top_1(21) -> 13
        , top_2(22) -> 13
        , top_3(28) -> 13
        , top_4(36) -> 13}

Tool RC1

Execution Time	Unknown
Answer	YES(?,O(n^1))
Input	Transformed CSR 04 LengthOfFiniteLists nosorts C

stdout:

YES(?,O(n^1))

Tool RC2

Execution Time	Unknown
Answer	YES(?,O(n^1))
Input	Transformed CSR 04 LengthOfFiniteLists nosorts C

stdout:

YES(?,O(n^1))

'Fastest (timeout of 60.0 seconds)'
-----------------------------------
Answer:           YES(?,O(n^1))
Input Problem:    runtime-complexity with respect to
  Rules:
    {  active(zeros()) -> mark(cons(0(), zeros()))
     , active(and(tt(), X)) -> mark(X)
     , active(length(nil())) -> mark(0())
     , active(length(cons(N, L))) -> mark(s(length(L)))
     , active(cons(X1, X2)) -> cons(active(X1), X2)
     , active(and(X1, X2)) -> and(active(X1), X2)
     , active(length(X)) -> length(active(X))
     , active(s(X)) -> s(active(X))
     , cons(mark(X1), X2) -> mark(cons(X1, X2))
     , and(mark(X1), X2) -> mark(and(X1, X2))
     , length(mark(X)) -> mark(length(X))
     , s(mark(X)) -> mark(s(X))
     , proper(zeros()) -> ok(zeros())
     , proper(cons(X1, X2)) -> cons(proper(X1), proper(X2))
     , proper(0()) -> ok(0())
     , proper(and(X1, X2)) -> and(proper(X1), proper(X2))
     , proper(tt()) -> ok(tt())
     , proper(length(X)) -> length(proper(X))
     , proper(nil()) -> ok(nil())
     , proper(s(X)) -> s(proper(X))
     , cons(ok(X1), ok(X2)) -> ok(cons(X1, X2))
     , and(ok(X1), ok(X2)) -> ok(and(X1, X2))
     , length(ok(X)) -> ok(length(X))
     , s(ok(X)) -> ok(s(X))
     , top(mark(X)) -> top(proper(X))
     , top(ok(X)) -> top(active(X))}

Proof Output:
  'Bounds with perSymbol-enrichment and initial automaton 'match'' proved the best result:

  Details:
  --------
    'Bounds with perSymbol-enrichment and initial automaton 'match'' succeeded with the following output:
     'Bounds with perSymbol-enrichment and initial automaton 'match''
     ----------------------------------------------------------------
     Answer:           YES(?,O(n^1))
     Input Problem:    runtime-complexity with respect to
       Rules:
         {  active(zeros()) -> mark(cons(0(), zeros()))
          , active(and(tt(), X)) -> mark(X)
          , active(length(nil())) -> mark(0())
          , active(length(cons(N, L))) -> mark(s(length(L)))
          , active(cons(X1, X2)) -> cons(active(X1), X2)
          , active(and(X1, X2)) -> and(active(X1), X2)
          , active(length(X)) -> length(active(X))
          , active(s(X)) -> s(active(X))
          , cons(mark(X1), X2) -> mark(cons(X1, X2))
          , and(mark(X1), X2) -> mark(and(X1, X2))
          , length(mark(X)) -> mark(length(X))
          , s(mark(X)) -> mark(s(X))
          , proper(zeros()) -> ok(zeros())
          , proper(cons(X1, X2)) -> cons(proper(X1), proper(X2))
          , proper(0()) -> ok(0())
          , proper(and(X1, X2)) -> and(proper(X1), proper(X2))
          , proper(tt()) -> ok(tt())
          , proper(length(X)) -> length(proper(X))
          , proper(nil()) -> ok(nil())
          , proper(s(X)) -> s(proper(X))
          , cons(ok(X1), ok(X2)) -> ok(cons(X1, X2))
          , and(ok(X1), ok(X2)) -> ok(and(X1, X2))
          , length(ok(X)) -> ok(length(X))
          , s(ok(X)) -> ok(s(X))
          , top(mark(X)) -> top(proper(X))
          , top(ok(X)) -> top(active(X))}

     Proof Output:
       The problem is match-bounded by 5.
       The enriched problem is compatible with the following automaton:
       {  active_0(2) -> 1
        , active_0(3) -> 1
        , active_0(5) -> 1
        , active_0(7) -> 1
        , active_0(9) -> 1
        , active_0(12) -> 1
        , active_1(2) -> 21
        , active_1(3) -> 21
        , active_1(5) -> 21
        , active_1(7) -> 21
        , active_1(9) -> 21
        , active_1(12) -> 21
        , active_2(15) -> 22
        , active_2(16) -> 22
        , active_3(32) -> 28
        , active_4(24) -> 33
        , active_4(35) -> 36
        , active_5(31) -> 37
        , zeros_0() -> 2
        , zeros_1() -> 16
        , zeros_2() -> 25
        , zeros_3() -> 34
        , mark_0(2) -> 3
        , mark_0(3) -> 3
        , mark_0(5) -> 3
        , mark_0(7) -> 3
        , mark_0(9) -> 3
        , mark_0(12) -> 3
        , mark_1(14) -> 1
        , mark_1(14) -> 21
        , mark_1(17) -> 4
        , mark_1(17) -> 17
        , mark_1(18) -> 6
        , mark_1(18) -> 18
        , mark_1(19) -> 8
        , mark_1(19) -> 19
        , mark_1(20) -> 10
        , mark_1(20) -> 20
        , mark_2(23) -> 22
        , cons_0(2, 2) -> 4
        , cons_0(2, 3) -> 4
        , cons_0(2, 5) -> 4
        , cons_0(2, 7) -> 4
        , cons_0(2, 9) -> 4
        , cons_0(2, 12) -> 4
        , cons_0(3, 2) -> 4
        , cons_0(3, 3) -> 4
        , cons_0(3, 5) -> 4
        , cons_0(3, 7) -> 4
        , cons_0(3, 9) -> 4
        , cons_0(3, 12) -> 4
        , cons_0(5, 2) -> 4
        , cons_0(5, 3) -> 4
        , cons_0(5, 5) -> 4
        , cons_0(5, 7) -> 4
        , cons_0(5, 9) -> 4
        , cons_0(5, 12) -> 4
        , cons_0(7, 2) -> 4
        , cons_0(7, 3) -> 4
        , cons_0(7, 5) -> 4
        , cons_0(7, 7) -> 4
        , cons_0(7, 9) -> 4
        , cons_0(7, 12) -> 4
        , cons_0(9, 2) -> 4
        , cons_0(9, 3) -> 4
        , cons_0(9, 5) -> 4
        , cons_0(9, 7) -> 4
        , cons_0(9, 9) -> 4
        , cons_0(9, 12) -> 4
        , cons_0(12, 2) -> 4
        , cons_0(12, 3) -> 4
        , cons_0(12, 5) -> 4
        , cons_0(12, 7) -> 4
        , cons_0(12, 9) -> 4
        , cons_0(12, 12) -> 4
        , cons_1(2, 2) -> 17
        , cons_1(2, 3) -> 17
        , cons_1(2, 5) -> 17
        , cons_1(2, 7) -> 17
        , cons_1(2, 9) -> 17
        , cons_1(2, 12) -> 17
        , cons_1(3, 2) -> 17
        , cons_1(3, 3) -> 17
        , cons_1(3, 5) -> 17
        , cons_1(3, 7) -> 17
        , cons_1(3, 9) -> 17
        , cons_1(3, 12) -> 17
        , cons_1(5, 2) -> 17
        , cons_1(5, 3) -> 17
        , cons_1(5, 5) -> 17
        , cons_1(5, 7) -> 17
        , cons_1(5, 9) -> 17
        , cons_1(5, 12) -> 17
        , cons_1(7, 2) -> 17
        , cons_1(7, 3) -> 17
        , cons_1(7, 5) -> 17
        , cons_1(7, 7) -> 17
        , cons_1(7, 9) -> 17
        , cons_1(7, 12) -> 17
        , cons_1(9, 2) -> 17
        , cons_1(9, 3) -> 17
        , cons_1(9, 5) -> 17
        , cons_1(9, 7) -> 17
        , cons_1(9, 9) -> 17
        , cons_1(9, 12) -> 17
        , cons_1(12, 2) -> 17
        , cons_1(12, 3) -> 17
        , cons_1(12, 5) -> 17
        , cons_1(12, 7) -> 17
        , cons_1(12, 9) -> 17
        , cons_1(12, 12) -> 17
        , cons_1(15, 16) -> 14
        , cons_2(24, 25) -> 23
        , cons_2(26, 27) -> 22
        , cons_3(24, 25) -> 32
        , cons_3(29, 30) -> 28
        , cons_4(31, 34) -> 35
        , cons_4(33, 25) -> 28
        , cons_5(37, 34) -> 36
        , 0_0() -> 5
        , 0_1() -> 15
        , 0_2() -> 24
        , 0_3() -> 31
        , and_0(2, 2) -> 6
        , and_0(2, 3) -> 6
        , and_0(2, 5) -> 6
        , and_0(2, 7) -> 6
        , and_0(2, 9) -> 6
        , and_0(2, 12) -> 6
        , and_0(3, 2) -> 6
        , and_0(3, 3) -> 6
        , and_0(3, 5) -> 6
        , and_0(3, 7) -> 6
        , and_0(3, 9) -> 6
        , and_0(3, 12) -> 6
        , and_0(5, 2) -> 6
        , and_0(5, 3) -> 6
        , and_0(5, 5) -> 6
        , and_0(5, 7) -> 6
        , and_0(5, 9) -> 6
        , and_0(5, 12) -> 6
        , and_0(7, 2) -> 6
        , and_0(7, 3) -> 6
        , and_0(7, 5) -> 6
        , and_0(7, 7) -> 6
        , and_0(7, 9) -> 6
        , and_0(7, 12) -> 6
        , and_0(9, 2) -> 6
        , and_0(9, 3) -> 6
        , and_0(9, 5) -> 6
        , and_0(9, 7) -> 6
        , and_0(9, 9) -> 6
        , and_0(9, 12) -> 6
        , and_0(12, 2) -> 6
        , and_0(12, 3) -> 6
        , and_0(12, 5) -> 6
        , and_0(12, 7) -> 6
        , and_0(12, 9) -> 6
        , and_0(12, 12) -> 6
        , and_1(2, 2) -> 18
        , and_1(2, 3) -> 18
        , and_1(2, 5) -> 18
        , and_1(2, 7) -> 18
        , and_1(2, 9) -> 18
        , and_1(2, 12) -> 18
        , and_1(3, 2) -> 18
        , and_1(3, 3) -> 18
        , and_1(3, 5) -> 18
        , and_1(3, 7) -> 18
        , and_1(3, 9) -> 18
        , and_1(3, 12) -> 18
        , and_1(5, 2) -> 18
        , and_1(5, 3) -> 18
        , and_1(5, 5) -> 18
        , and_1(5, 7) -> 18
        , and_1(5, 9) -> 18
        , and_1(5, 12) -> 18
        , and_1(7, 2) -> 18
        , and_1(7, 3) -> 18
        , and_1(7, 5) -> 18
        , and_1(7, 7) -> 18
        , and_1(7, 9) -> 18
        , and_1(7, 12) -> 18
        , and_1(9, 2) -> 18
        , and_1(9, 3) -> 18
        , and_1(9, 5) -> 18
        , and_1(9, 7) -> 18
        , and_1(9, 9) -> 18
        , and_1(9, 12) -> 18
        , and_1(12, 2) -> 18
        , and_1(12, 3) -> 18
        , and_1(12, 5) -> 18
        , and_1(12, 7) -> 18
        , and_1(12, 9) -> 18
        , and_1(12, 12) -> 18
        , tt_0() -> 7
        , tt_1() -> 15
        , tt_2() -> 24
        , tt_3() -> 31
        , length_0(2) -> 8
        , length_0(3) -> 8
        , length_0(5) -> 8
        , length_0(7) -> 8
        , length_0(9) -> 8
        , length_0(12) -> 8
        , length_1(2) -> 19
        , length_1(3) -> 19
        , length_1(5) -> 19
        , length_1(7) -> 19
        , length_1(9) -> 19
        , length_1(12) -> 19
        , nil_0() -> 9
        , nil_1() -> 15
        , nil_2() -> 24
        , nil_3() -> 31
        , s_0(2) -> 10
        , s_0(3) -> 10
        , s_0(5) -> 10
        , s_0(7) -> 10
        , s_0(9) -> 10
        , s_0(12) -> 10
        , s_1(2) -> 20
        , s_1(3) -> 20
        , s_1(5) -> 20
        , s_1(7) -> 20
        , s_1(9) -> 20
        , s_1(12) -> 20
        , proper_0(2) -> 11
        , proper_0(3) -> 11
        , proper_0(5) -> 11
        , proper_0(7) -> 11
        , proper_0(9) -> 11
        , proper_0(12) -> 11
        , proper_1(2) -> 21
        , proper_1(3) -> 21
        , proper_1(5) -> 21
        , proper_1(7) -> 21
        , proper_1(9) -> 21
        , proper_1(12) -> 21
        , proper_2(14) -> 22
        , proper_2(15) -> 26
        , proper_2(16) -> 27
        , proper_3(23) -> 28
        , proper_3(24) -> 29
        , proper_3(25) -> 30
        , ok_0(2) -> 12
        , ok_0(3) -> 12
        , ok_0(5) -> 12
        , ok_0(7) -> 12
        , ok_0(9) -> 12
        , ok_0(12) -> 12
        , ok_1(15) -> 11
        , ok_1(15) -> 21
        , ok_1(16) -> 11
        , ok_1(16) -> 21
        , ok_1(17) -> 4
        , ok_1(17) -> 17
        , ok_1(18) -> 6
        , ok_1(18) -> 18
        , ok_1(19) -> 8
        , ok_1(19) -> 19
        , ok_1(20) -> 10
        , ok_1(20) -> 20
        , ok_2(24) -> 26
        , ok_2(25) -> 27
        , ok_3(31) -> 29
        , ok_3(32) -> 22
        , ok_3(34) -> 30
        , ok_4(35) -> 28
        , top_0(2) -> 13
        , top_0(3) -> 13
        , top_0(5) -> 13
        , top_0(7) -> 13
        , top_0(9) -> 13
        , top_0(12) -> 13
        , top_1(21) -> 13
        , top_2(22) -> 13
        , top_3(28) -> 13
        , top_4(36) -> 13}