Problem Transformed CSR 04 LengthOfFiniteLists nosorts noand C

Tool CaT

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

stdout:

YES(?,O(n^1))

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

Proof:
Bounds Processor:
  bound: 5
  enrichment: match
  automaton:
   final states: {14,13,12,11,10,9,8,7}
   transitions:
    active3(52) -> 46*
    top1(32) -> 14*
    nil3() -> 53*
    active1(5) -> 32*
    active1(2) -> 32*
    active1(4) -> 32*
    active1(6) -> 32*
    active1(1) -> 32*
    active1(3) -> 32*
    tt3() -> 53*
    proper1(5) -> 32*
    proper1(2) -> 32*
    proper1(4) -> 32*
    proper1(6) -> 32*
    proper1(1) -> 32*
    proper1(3) -> 32*
    03() -> 56*
    ok1(25) -> 25,10
    ok1(27) -> 27,11
    ok1(29) -> 29,12
    ok1(19) -> 32,13
    ok1(21) -> 21,8
    ok1(23) -> 23,9
    ok1(18) -> 32,13
    zeros3() -> 53*
    length1(5) -> 29*
    length1(2) -> 29*
    length1(4) -> 29*
    length1(6) -> 29*
    length1(1) -> 29*
    length1(3) -> 29*
    ok4(59) -> 46*
    s1(5) -> 27*
    s1(2) -> 27*
    s1(4) -> 27*
    s1(6) -> 27*
    s1(1) -> 27*
    s1(3) -> 27*
    cons4(56,53) -> 59*
    cons4(58,38) -> 46*
    U121(3,1) -> 25*
    U121(3,3) -> 25*
    U121(3,5) -> 25*
    U121(4,2) -> 25*
    U121(4,4) -> 25*
    U121(4,6) -> 25*
    U121(5,1) -> 25*
    U121(5,3) -> 25*
    U121(5,5) -> 25*
    U121(6,2) -> 25*
    U121(1,2) -> 25*
    U121(6,4) -> 25*
    U121(1,4) -> 25*
    U121(6,6) -> 25*
    U121(1,6) -> 25*
    U121(2,1) -> 25*
    U121(2,3) -> 25*
    U121(2,5) -> 25*
    U121(3,2) -> 25*
    U121(3,4) -> 25*
    U121(3,6) -> 25*
    U121(4,1) -> 25*
    U121(4,3) -> 25*
    U121(4,5) -> 25*
    U121(5,2) -> 25*
    U121(5,4) -> 25*
    U121(5,6) -> 25*
    U121(6,1) -> 25*
    U121(1,1) -> 25*
    U121(6,3) -> 25*
    U121(1,3) -> 25*
    U121(6,5) -> 25*
    U121(1,5) -> 25*
    U121(2,2) -> 25*
    U121(2,4) -> 25*
    U121(2,6) -> 25*
    active4(59) -> 62*
    active4(39) -> 58*
    U111(2,6) -> 23*
    U111(3,1) -> 23*
    U111(3,3) -> 23*
    U111(3,5) -> 23*
    U111(4,2) -> 23*
    U111(4,4) -> 23*
    U111(4,6) -> 23*
    U111(5,1) -> 23*
    U111(5,3) -> 23*
    U111(5,5) -> 23*
    U111(6,2) -> 23*
    U111(1,2) -> 23*
    U111(6,4) -> 23*
    U111(1,4) -> 23*
    U111(6,6) -> 23*
    U111(1,6) -> 23*
    U111(2,1) -> 23*
    U111(2,3) -> 23*
    U111(2,5) -> 23*
    U111(3,2) -> 23*
    U111(3,4) -> 23*
    U111(3,6) -> 23*
    U111(4,1) -> 23*
    U111(4,3) -> 23*
    U111(4,5) -> 23*
    U111(5,2) -> 23*
    U111(5,4) -> 23*
    U111(5,6) -> 23*
    U111(6,1) -> 23*
    U111(1,1) -> 23*
    U111(6,3) -> 23*
    U111(1,3) -> 23*
    U111(6,5) -> 23*
    U111(1,5) -> 23*
    U111(2,2) -> 23*
    U111(2,4) -> 23*
    top4(62) -> 14*
    cons1(2,6) -> 21*
    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(19,18) -> 20*
    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(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*
    cons5(63,53) -> 62*
    nil1() -> 18*
    active5(56) -> 63*
    tt1() -> 18*
    01() -> 19*
    zeros1() -> 18*
    mark1(25) -> 25,10
    mark1(20) -> 32,7
    mark1(27) -> 27,11
    mark1(29) -> 29,12
    mark1(21) -> 21,8
    mark1(23) -> 23,9
    top2(33) -> 14*
    active0(5) -> 7*
    active0(2) -> 7*
    active0(4) -> 7*
    active0(6) -> 7*
    active0(1) -> 7*
    active0(3) -> 7*
    active2(19) -> 33*
    active2(18) -> 33*
    zeros0() -> 1*
    proper2(20) -> 33*
    proper2(19) -> 42*
    proper2(18) -> 41*
    mark0(5) -> 2*
    mark0(2) -> 2*
    mark0(4) -> 2*
    mark0(6) -> 2*
    mark0(1) -> 2*
    mark0(3) -> 2*
    cons2(39,38) -> 40*
    cons2(42,41) -> 33*
    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(40) -> 33*
    00() -> 3*
    02() -> 39*
    U110(3,1) -> 9*
    U110(3,3) -> 9*
    U110(3,5) -> 9*
    U110(4,2) -> 9*
    U110(4,4) -> 9*
    U110(4,6) -> 9*
    U110(5,1) -> 9*
    U110(5,3) -> 9*
    U110(5,5) -> 9*
    U110(6,2) -> 9*
    U110(1,2) -> 9*
    U110(6,4) -> 9*
    U110(1,4) -> 9*
    U110(6,6) -> 9*
    U110(1,6) -> 9*
    U110(2,1) -> 9*
    U110(2,3) -> 9*
    U110(2,5) -> 9*
    U110(3,2) -> 9*
    U110(3,4) -> 9*
    U110(3,6) -> 9*
    U110(4,1) -> 9*
    U110(4,3) -> 9*
    U110(4,5) -> 9*
    U110(5,2) -> 9*
    U110(5,4) -> 9*
    U110(5,6) -> 9*
    U110(6,1) -> 9*
    U110(1,1) -> 9*
    U110(6,3) -> 9*
    U110(1,3) -> 9*
    U110(6,5) -> 9*
    U110(1,5) -> 9*
    U110(2,2) -> 9*
    U110(2,4) -> 9*
    U110(2,6) -> 9*
    zeros2() -> 38*
    tt0() -> 4*
    top3(46) -> 14*
    U120(3,1) -> 10*
    U120(3,3) -> 10*
    U120(3,5) -> 10*
    U120(4,2) -> 10*
    U120(4,4) -> 10*
    U120(4,6) -> 10*
    U120(5,1) -> 10*
    U120(5,3) -> 10*
    U120(5,5) -> 10*
    U120(6,2) -> 10*
    U120(1,2) -> 10*
    U120(6,4) -> 10*
    U120(1,4) -> 10*
    U120(6,6) -> 10*
    U120(1,6) -> 10*
    U120(2,1) -> 10*
    U120(2,3) -> 10*
    U120(2,5) -> 10*
    U120(3,2) -> 10*
    U120(3,4) -> 10*
    U120(3,6) -> 10*
    U120(4,1) -> 10*
    U120(4,3) -> 10*
    U120(4,5) -> 10*
    U120(5,2) -> 10*
    U120(5,4) -> 10*
    U120(5,6) -> 10*
    U120(6,1) -> 10*
    U120(1,1) -> 10*
    U120(6,3) -> 10*
    U120(1,3) -> 10*
    U120(6,5) -> 10*
    U120(1,5) -> 10*
    U120(2,2) -> 10*
    U120(2,4) -> 10*
    U120(2,6) -> 10*
    proper3(40) -> 46*
    proper3(39) -> 48*
    proper3(38) -> 47*
    s0(5) -> 11*
    s0(2) -> 11*
    s0(4) -> 11*
    s0(6) -> 11*
    s0(1) -> 11*
    s0(3) -> 11*
    ok2(39) -> 42*
    ok2(38) -> 41*
    length0(5) -> 12*
    length0(2) -> 12*
    length0(4) -> 12*
    length0(6) -> 12*
    length0(1) -> 12*
    length0(3) -> 12*
    nil2() -> 38*
    nil0() -> 5*
    tt2() -> 38*
    proper0(5) -> 13*
    proper0(2) -> 13*
    proper0(4) -> 13*
    proper0(6) -> 13*
    proper0(1) -> 13*
    proper0(3) -> 13*
    ok3(52) -> 33*
    ok3(56) -> 48*
    ok3(53) -> 47*
    ok0(5) -> 6*
    ok0(2) -> 6*
    ok0(4) -> 6*
    ok0(6) -> 6*
    ok0(1) -> 6*
    ok0(3) -> 6*
    cons3(48,47) -> 46*
    cons3(39,38) -> 52*
    top0(5) -> 14*
    top0(2) -> 14*
    top0(4) -> 14*
    top0(6) -> 14*
    top0(1) -> 14*
    top0(3) -> 14*
  problem:

  Qed

Tool IRC1

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

stdout:

YES(?,O(n^1))

Tool IRC2

Execution Time	Unknown
Answer	YES(?,O(n^1))
Input	Transformed CSR 04 LengthOfFiniteLists nosorts noand 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(U11(tt(), L)) -> mark(U12(tt(), L))
     , active(U12(tt(), L)) -> mark(s(length(L)))
     , active(length(nil())) -> mark(0())
     , active(length(cons(N, L))) -> mark(U11(tt(), L))
     , active(cons(X1, X2)) -> cons(active(X1), X2)
     , active(U11(X1, X2)) -> U11(active(X1), X2)
     , active(U12(X1, X2)) -> U12(active(X1), X2)
     , active(s(X)) -> s(active(X))
     , active(length(X)) -> length(active(X))
     , cons(mark(X1), X2) -> mark(cons(X1, X2))
     , U11(mark(X1), X2) -> mark(U11(X1, X2))
     , U12(mark(X1), X2) -> mark(U12(X1, X2))
     , s(mark(X)) -> mark(s(X))
     , length(mark(X)) -> mark(length(X))
     , proper(zeros()) -> ok(zeros())
     , proper(cons(X1, X2)) -> cons(proper(X1), proper(X2))
     , proper(0()) -> ok(0())
     , proper(U11(X1, X2)) -> U11(proper(X1), proper(X2))
     , proper(tt()) -> ok(tt())
     , proper(U12(X1, X2)) -> U12(proper(X1), proper(X2))
     , proper(s(X)) -> s(proper(X))
     , proper(length(X)) -> length(proper(X))
     , proper(nil()) -> ok(nil())
     , cons(ok(X1), ok(X2)) -> ok(cons(X1, X2))
     , U11(ok(X1), ok(X2)) -> ok(U11(X1, X2))
     , U12(ok(X1), ok(X2)) -> ok(U12(X1, X2))
     , s(ok(X)) -> ok(s(X))
     , length(ok(X)) -> ok(length(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(U11(tt(), L)) -> mark(U12(tt(), L))
          , active(U12(tt(), L)) -> mark(s(length(L)))
          , active(length(nil())) -> mark(0())
          , active(length(cons(N, L))) -> mark(U11(tt(), L))
          , active(cons(X1, X2)) -> cons(active(X1), X2)
          , active(U11(X1, X2)) -> U11(active(X1), X2)
          , active(U12(X1, X2)) -> U12(active(X1), X2)
          , active(s(X)) -> s(active(X))
          , active(length(X)) -> length(active(X))
          , cons(mark(X1), X2) -> mark(cons(X1, X2))
          , U11(mark(X1), X2) -> mark(U11(X1, X2))
          , U12(mark(X1), X2) -> mark(U12(X1, X2))
          , s(mark(X)) -> mark(s(X))
          , length(mark(X)) -> mark(length(X))
          , proper(zeros()) -> ok(zeros())
          , proper(cons(X1, X2)) -> cons(proper(X1), proper(X2))
          , proper(0()) -> ok(0())
          , proper(U11(X1, X2)) -> U11(proper(X1), proper(X2))
          , proper(tt()) -> ok(tt())
          , proper(U12(X1, X2)) -> U12(proper(X1), proper(X2))
          , proper(s(X)) -> s(proper(X))
          , proper(length(X)) -> length(proper(X))
          , proper(nil()) -> ok(nil())
          , cons(ok(X1), ok(X2)) -> ok(cons(X1, X2))
          , U11(ok(X1), ok(X2)) -> ok(U11(X1, X2))
          , U12(ok(X1), ok(X2)) -> ok(U12(X1, X2))
          , s(ok(X)) -> ok(s(X))
          , length(ok(X)) -> ok(length(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(11) -> 1
        , active_0(13) -> 1
        , active_1(2) -> 23
        , active_1(3) -> 23
        , active_1(5) -> 23
        , active_1(7) -> 23
        , active_1(11) -> 23
        , active_1(13) -> 23
        , active_2(16) -> 24
        , active_2(17) -> 24
        , active_3(34) -> 30
        , active_4(26) -> 35
        , active_4(37) -> 38
        , active_5(33) -> 39
        , zeros_0() -> 2
        , zeros_1() -> 17
        , zeros_2() -> 27
        , zeros_3() -> 36
        , mark_0(2) -> 3
        , mark_0(3) -> 3
        , mark_0(5) -> 3
        , mark_0(7) -> 3
        , mark_0(11) -> 3
        , mark_0(13) -> 3
        , mark_1(15) -> 1
        , mark_1(15) -> 23
        , mark_1(18) -> 4
        , mark_1(18) -> 18
        , mark_1(19) -> 6
        , mark_1(19) -> 19
        , mark_1(20) -> 8
        , mark_1(20) -> 20
        , mark_1(21) -> 9
        , mark_1(21) -> 21
        , mark_1(22) -> 10
        , mark_1(22) -> 22
        , mark_2(25) -> 24
        , cons_0(2, 2) -> 4
        , cons_0(2, 3) -> 4
        , cons_0(2, 5) -> 4
        , cons_0(2, 7) -> 4
        , cons_0(2, 11) -> 4
        , cons_0(2, 13) -> 4
        , cons_0(3, 2) -> 4
        , cons_0(3, 3) -> 4
        , cons_0(3, 5) -> 4
        , cons_0(3, 7) -> 4
        , cons_0(3, 11) -> 4
        , cons_0(3, 13) -> 4
        , cons_0(5, 2) -> 4
        , cons_0(5, 3) -> 4
        , cons_0(5, 5) -> 4
        , cons_0(5, 7) -> 4
        , cons_0(5, 11) -> 4
        , cons_0(5, 13) -> 4
        , cons_0(7, 2) -> 4
        , cons_0(7, 3) -> 4
        , cons_0(7, 5) -> 4
        , cons_0(7, 7) -> 4
        , cons_0(7, 11) -> 4
        , cons_0(7, 13) -> 4
        , cons_0(11, 2) -> 4
        , cons_0(11, 3) -> 4
        , cons_0(11, 5) -> 4
        , cons_0(11, 7) -> 4
        , cons_0(11, 11) -> 4
        , cons_0(11, 13) -> 4
        , cons_0(13, 2) -> 4
        , cons_0(13, 3) -> 4
        , cons_0(13, 5) -> 4
        , cons_0(13, 7) -> 4
        , cons_0(13, 11) -> 4
        , cons_0(13, 13) -> 4
        , cons_1(2, 2) -> 18
        , cons_1(2, 3) -> 18
        , cons_1(2, 5) -> 18
        , cons_1(2, 7) -> 18
        , cons_1(2, 11) -> 18
        , cons_1(2, 13) -> 18
        , cons_1(3, 2) -> 18
        , cons_1(3, 3) -> 18
        , cons_1(3, 5) -> 18
        , cons_1(3, 7) -> 18
        , cons_1(3, 11) -> 18
        , cons_1(3, 13) -> 18
        , cons_1(5, 2) -> 18
        , cons_1(5, 3) -> 18
        , cons_1(5, 5) -> 18
        , cons_1(5, 7) -> 18
        , cons_1(5, 11) -> 18
        , cons_1(5, 13) -> 18
        , cons_1(7, 2) -> 18
        , cons_1(7, 3) -> 18
        , cons_1(7, 5) -> 18
        , cons_1(7, 7) -> 18
        , cons_1(7, 11) -> 18
        , cons_1(7, 13) -> 18
        , cons_1(11, 2) -> 18
        , cons_1(11, 3) -> 18
        , cons_1(11, 5) -> 18
        , cons_1(11, 7) -> 18
        , cons_1(11, 11) -> 18
        , cons_1(11, 13) -> 18
        , cons_1(13, 2) -> 18
        , cons_1(13, 3) -> 18
        , cons_1(13, 5) -> 18
        , cons_1(13, 7) -> 18
        , cons_1(13, 11) -> 18
        , cons_1(13, 13) -> 18
        , cons_1(16, 17) -> 15
        , cons_2(26, 27) -> 25
        , cons_2(28, 29) -> 24
        , cons_3(26, 27) -> 34
        , cons_3(31, 32) -> 30
        , cons_4(33, 36) -> 37
        , cons_4(35, 27) -> 30
        , cons_5(39, 36) -> 38
        , 0_0() -> 5
        , 0_1() -> 16
        , 0_2() -> 26
        , 0_3() -> 33
        , U11_0(2, 2) -> 6
        , U11_0(2, 3) -> 6
        , U11_0(2, 5) -> 6
        , U11_0(2, 7) -> 6
        , U11_0(2, 11) -> 6
        , U11_0(2, 13) -> 6
        , U11_0(3, 2) -> 6
        , U11_0(3, 3) -> 6
        , U11_0(3, 5) -> 6
        , U11_0(3, 7) -> 6
        , U11_0(3, 11) -> 6
        , U11_0(3, 13) -> 6
        , U11_0(5, 2) -> 6
        , U11_0(5, 3) -> 6
        , U11_0(5, 5) -> 6
        , U11_0(5, 7) -> 6
        , U11_0(5, 11) -> 6
        , U11_0(5, 13) -> 6
        , U11_0(7, 2) -> 6
        , U11_0(7, 3) -> 6
        , U11_0(7, 5) -> 6
        , U11_0(7, 7) -> 6
        , U11_0(7, 11) -> 6
        , U11_0(7, 13) -> 6
        , U11_0(11, 2) -> 6
        , U11_0(11, 3) -> 6
        , U11_0(11, 5) -> 6
        , U11_0(11, 7) -> 6
        , U11_0(11, 11) -> 6
        , U11_0(11, 13) -> 6
        , U11_0(13, 2) -> 6
        , U11_0(13, 3) -> 6
        , U11_0(13, 5) -> 6
        , U11_0(13, 7) -> 6
        , U11_0(13, 11) -> 6
        , U11_0(13, 13) -> 6
        , U11_1(2, 2) -> 19
        , U11_1(2, 3) -> 19
        , U11_1(2, 5) -> 19
        , U11_1(2, 7) -> 19
        , U11_1(2, 11) -> 19
        , U11_1(2, 13) -> 19
        , U11_1(3, 2) -> 19
        , U11_1(3, 3) -> 19
        , U11_1(3, 5) -> 19
        , U11_1(3, 7) -> 19
        , U11_1(3, 11) -> 19
        , U11_1(3, 13) -> 19
        , U11_1(5, 2) -> 19
        , U11_1(5, 3) -> 19
        , U11_1(5, 5) -> 19
        , U11_1(5, 7) -> 19
        , U11_1(5, 11) -> 19
        , U11_1(5, 13) -> 19
        , U11_1(7, 2) -> 19
        , U11_1(7, 3) -> 19
        , U11_1(7, 5) -> 19
        , U11_1(7, 7) -> 19
        , U11_1(7, 11) -> 19
        , U11_1(7, 13) -> 19
        , U11_1(11, 2) -> 19
        , U11_1(11, 3) -> 19
        , U11_1(11, 5) -> 19
        , U11_1(11, 7) -> 19
        , U11_1(11, 11) -> 19
        , U11_1(11, 13) -> 19
        , U11_1(13, 2) -> 19
        , U11_1(13, 3) -> 19
        , U11_1(13, 5) -> 19
        , U11_1(13, 7) -> 19
        , U11_1(13, 11) -> 19
        , U11_1(13, 13) -> 19
        , tt_0() -> 7
        , tt_1() -> 16
        , tt_2() -> 26
        , tt_3() -> 33
        , U12_0(2, 2) -> 8
        , U12_0(2, 3) -> 8
        , U12_0(2, 5) -> 8
        , U12_0(2, 7) -> 8
        , U12_0(2, 11) -> 8
        , U12_0(2, 13) -> 8
        , U12_0(3, 2) -> 8
        , U12_0(3, 3) -> 8
        , U12_0(3, 5) -> 8
        , U12_0(3, 7) -> 8
        , U12_0(3, 11) -> 8
        , U12_0(3, 13) -> 8
        , U12_0(5, 2) -> 8
        , U12_0(5, 3) -> 8
        , U12_0(5, 5) -> 8
        , U12_0(5, 7) -> 8
        , U12_0(5, 11) -> 8
        , U12_0(5, 13) -> 8
        , U12_0(7, 2) -> 8
        , U12_0(7, 3) -> 8
        , U12_0(7, 5) -> 8
        , U12_0(7, 7) -> 8
        , U12_0(7, 11) -> 8
        , U12_0(7, 13) -> 8
        , U12_0(11, 2) -> 8
        , U12_0(11, 3) -> 8
        , U12_0(11, 5) -> 8
        , U12_0(11, 7) -> 8
        , U12_0(11, 11) -> 8
        , U12_0(11, 13) -> 8
        , U12_0(13, 2) -> 8
        , U12_0(13, 3) -> 8
        , U12_0(13, 5) -> 8
        , U12_0(13, 7) -> 8
        , U12_0(13, 11) -> 8
        , U12_0(13, 13) -> 8
        , U12_1(2, 2) -> 20
        , U12_1(2, 3) -> 20
        , U12_1(2, 5) -> 20
        , U12_1(2, 7) -> 20
        , U12_1(2, 11) -> 20
        , U12_1(2, 13) -> 20
        , U12_1(3, 2) -> 20
        , U12_1(3, 3) -> 20
        , U12_1(3, 5) -> 20
        , U12_1(3, 7) -> 20
        , U12_1(3, 11) -> 20
        , U12_1(3, 13) -> 20
        , U12_1(5, 2) -> 20
        , U12_1(5, 3) -> 20
        , U12_1(5, 5) -> 20
        , U12_1(5, 7) -> 20
        , U12_1(5, 11) -> 20
        , U12_1(5, 13) -> 20
        , U12_1(7, 2) -> 20
        , U12_1(7, 3) -> 20
        , U12_1(7, 5) -> 20
        , U12_1(7, 7) -> 20
        , U12_1(7, 11) -> 20
        , U12_1(7, 13) -> 20
        , U12_1(11, 2) -> 20
        , U12_1(11, 3) -> 20
        , U12_1(11, 5) -> 20
        , U12_1(11, 7) -> 20
        , U12_1(11, 11) -> 20
        , U12_1(11, 13) -> 20
        , U12_1(13, 2) -> 20
        , U12_1(13, 3) -> 20
        , U12_1(13, 5) -> 20
        , U12_1(13, 7) -> 20
        , U12_1(13, 11) -> 20
        , U12_1(13, 13) -> 20
        , s_0(2) -> 9
        , s_0(3) -> 9
        , s_0(5) -> 9
        , s_0(7) -> 9
        , s_0(11) -> 9
        , s_0(13) -> 9
        , s_1(2) -> 21
        , s_1(3) -> 21
        , s_1(5) -> 21
        , s_1(7) -> 21
        , s_1(11) -> 21
        , s_1(13) -> 21
        , length_0(2) -> 10
        , length_0(3) -> 10
        , length_0(5) -> 10
        , length_0(7) -> 10
        , length_0(11) -> 10
        , length_0(13) -> 10
        , length_1(2) -> 22
        , length_1(3) -> 22
        , length_1(5) -> 22
        , length_1(7) -> 22
        , length_1(11) -> 22
        , length_1(13) -> 22
        , nil_0() -> 11
        , nil_1() -> 16
        , nil_2() -> 26
        , nil_3() -> 33
        , proper_0(2) -> 12
        , proper_0(3) -> 12
        , proper_0(5) -> 12
        , proper_0(7) -> 12
        , proper_0(11) -> 12
        , proper_0(13) -> 12
        , proper_1(2) -> 23
        , proper_1(3) -> 23
        , proper_1(5) -> 23
        , proper_1(7) -> 23
        , proper_1(11) -> 23
        , proper_1(13) -> 23
        , proper_2(15) -> 24
        , proper_2(16) -> 28
        , proper_2(17) -> 29
        , proper_3(25) -> 30
        , proper_3(26) -> 31
        , proper_3(27) -> 32
        , ok_0(2) -> 13
        , ok_0(3) -> 13
        , ok_0(5) -> 13
        , ok_0(7) -> 13
        , ok_0(11) -> 13
        , ok_0(13) -> 13
        , ok_1(16) -> 12
        , ok_1(16) -> 23
        , ok_1(17) -> 12
        , ok_1(17) -> 23
        , ok_1(18) -> 4
        , ok_1(18) -> 18
        , ok_1(19) -> 6
        , ok_1(19) -> 19
        , ok_1(20) -> 8
        , ok_1(20) -> 20
        , ok_1(21) -> 9
        , ok_1(21) -> 21
        , ok_1(22) -> 10
        , ok_1(22) -> 22
        , ok_2(26) -> 28
        , ok_2(27) -> 29
        , ok_3(33) -> 31
        , ok_3(34) -> 24
        , ok_3(36) -> 32
        , ok_4(37) -> 30
        , top_0(2) -> 14
        , top_0(3) -> 14
        , top_0(5) -> 14
        , top_0(7) -> 14
        , top_0(11) -> 14
        , top_0(13) -> 14
        , top_1(23) -> 14
        , top_2(24) -> 14
        , top_3(30) -> 14
        , top_4(38) -> 14}

Tool RC1

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

stdout:

YES(?,O(n^1))

Tool RC2

Execution Time	Unknown
Answer	YES(?,O(n^1))
Input	Transformed CSR 04 LengthOfFiniteLists nosorts noand 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(U11(tt(), L)) -> mark(U12(tt(), L))
     , active(U12(tt(), L)) -> mark(s(length(L)))
     , active(length(nil())) -> mark(0())
     , active(length(cons(N, L))) -> mark(U11(tt(), L))
     , active(cons(X1, X2)) -> cons(active(X1), X2)
     , active(U11(X1, X2)) -> U11(active(X1), X2)
     , active(U12(X1, X2)) -> U12(active(X1), X2)
     , active(s(X)) -> s(active(X))
     , active(length(X)) -> length(active(X))
     , cons(mark(X1), X2) -> mark(cons(X1, X2))
     , U11(mark(X1), X2) -> mark(U11(X1, X2))
     , U12(mark(X1), X2) -> mark(U12(X1, X2))
     , s(mark(X)) -> mark(s(X))
     , length(mark(X)) -> mark(length(X))
     , proper(zeros()) -> ok(zeros())
     , proper(cons(X1, X2)) -> cons(proper(X1), proper(X2))
     , proper(0()) -> ok(0())
     , proper(U11(X1, X2)) -> U11(proper(X1), proper(X2))
     , proper(tt()) -> ok(tt())
     , proper(U12(X1, X2)) -> U12(proper(X1), proper(X2))
     , proper(s(X)) -> s(proper(X))
     , proper(length(X)) -> length(proper(X))
     , proper(nil()) -> ok(nil())
     , cons(ok(X1), ok(X2)) -> ok(cons(X1, X2))
     , U11(ok(X1), ok(X2)) -> ok(U11(X1, X2))
     , U12(ok(X1), ok(X2)) -> ok(U12(X1, X2))
     , s(ok(X)) -> ok(s(X))
     , length(ok(X)) -> ok(length(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(U11(tt(), L)) -> mark(U12(tt(), L))
          , active(U12(tt(), L)) -> mark(s(length(L)))
          , active(length(nil())) -> mark(0())
          , active(length(cons(N, L))) -> mark(U11(tt(), L))
          , active(cons(X1, X2)) -> cons(active(X1), X2)
          , active(U11(X1, X2)) -> U11(active(X1), X2)
          , active(U12(X1, X2)) -> U12(active(X1), X2)
          , active(s(X)) -> s(active(X))
          , active(length(X)) -> length(active(X))
          , cons(mark(X1), X2) -> mark(cons(X1, X2))
          , U11(mark(X1), X2) -> mark(U11(X1, X2))
          , U12(mark(X1), X2) -> mark(U12(X1, X2))
          , s(mark(X)) -> mark(s(X))
          , length(mark(X)) -> mark(length(X))
          , proper(zeros()) -> ok(zeros())
          , proper(cons(X1, X2)) -> cons(proper(X1), proper(X2))
          , proper(0()) -> ok(0())
          , proper(U11(X1, X2)) -> U11(proper(X1), proper(X2))
          , proper(tt()) -> ok(tt())
          , proper(U12(X1, X2)) -> U12(proper(X1), proper(X2))
          , proper(s(X)) -> s(proper(X))
          , proper(length(X)) -> length(proper(X))
          , proper(nil()) -> ok(nil())
          , cons(ok(X1), ok(X2)) -> ok(cons(X1, X2))
          , U11(ok(X1), ok(X2)) -> ok(U11(X1, X2))
          , U12(ok(X1), ok(X2)) -> ok(U12(X1, X2))
          , s(ok(X)) -> ok(s(X))
          , length(ok(X)) -> ok(length(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(11) -> 1
        , active_0(13) -> 1
        , active_1(2) -> 23
        , active_1(3) -> 23
        , active_1(5) -> 23
        , active_1(7) -> 23
        , active_1(11) -> 23
        , active_1(13) -> 23
        , active_2(16) -> 24
        , active_2(17) -> 24
        , active_3(34) -> 30
        , active_4(26) -> 35
        , active_4(37) -> 38
        , active_5(33) -> 39
        , zeros_0() -> 2
        , zeros_1() -> 17
        , zeros_2() -> 27
        , zeros_3() -> 36
        , mark_0(2) -> 3
        , mark_0(3) -> 3
        , mark_0(5) -> 3
        , mark_0(7) -> 3
        , mark_0(11) -> 3
        , mark_0(13) -> 3
        , mark_1(15) -> 1
        , mark_1(15) -> 23
        , mark_1(18) -> 4
        , mark_1(18) -> 18
        , mark_1(19) -> 6
        , mark_1(19) -> 19
        , mark_1(20) -> 8
        , mark_1(20) -> 20
        , mark_1(21) -> 9
        , mark_1(21) -> 21
        , mark_1(22) -> 10
        , mark_1(22) -> 22
        , mark_2(25) -> 24
        , cons_0(2, 2) -> 4
        , cons_0(2, 3) -> 4
        , cons_0(2, 5) -> 4
        , cons_0(2, 7) -> 4
        , cons_0(2, 11) -> 4
        , cons_0(2, 13) -> 4
        , cons_0(3, 2) -> 4
        , cons_0(3, 3) -> 4
        , cons_0(3, 5) -> 4
        , cons_0(3, 7) -> 4
        , cons_0(3, 11) -> 4
        , cons_0(3, 13) -> 4
        , cons_0(5, 2) -> 4
        , cons_0(5, 3) -> 4
        , cons_0(5, 5) -> 4
        , cons_0(5, 7) -> 4
        , cons_0(5, 11) -> 4
        , cons_0(5, 13) -> 4
        , cons_0(7, 2) -> 4
        , cons_0(7, 3) -> 4
        , cons_0(7, 5) -> 4
        , cons_0(7, 7) -> 4
        , cons_0(7, 11) -> 4
        , cons_0(7, 13) -> 4
        , cons_0(11, 2) -> 4
        , cons_0(11, 3) -> 4
        , cons_0(11, 5) -> 4
        , cons_0(11, 7) -> 4
        , cons_0(11, 11) -> 4
        , cons_0(11, 13) -> 4
        , cons_0(13, 2) -> 4
        , cons_0(13, 3) -> 4
        , cons_0(13, 5) -> 4
        , cons_0(13, 7) -> 4
        , cons_0(13, 11) -> 4
        , cons_0(13, 13) -> 4
        , cons_1(2, 2) -> 18
        , cons_1(2, 3) -> 18
        , cons_1(2, 5) -> 18
        , cons_1(2, 7) -> 18
        , cons_1(2, 11) -> 18
        , cons_1(2, 13) -> 18
        , cons_1(3, 2) -> 18
        , cons_1(3, 3) -> 18
        , cons_1(3, 5) -> 18
        , cons_1(3, 7) -> 18
        , cons_1(3, 11) -> 18
        , cons_1(3, 13) -> 18
        , cons_1(5, 2) -> 18
        , cons_1(5, 3) -> 18
        , cons_1(5, 5) -> 18
        , cons_1(5, 7) -> 18
        , cons_1(5, 11) -> 18
        , cons_1(5, 13) -> 18
        , cons_1(7, 2) -> 18
        , cons_1(7, 3) -> 18
        , cons_1(7, 5) -> 18
        , cons_1(7, 7) -> 18
        , cons_1(7, 11) -> 18
        , cons_1(7, 13) -> 18
        , cons_1(11, 2) -> 18
        , cons_1(11, 3) -> 18
        , cons_1(11, 5) -> 18
        , cons_1(11, 7) -> 18
        , cons_1(11, 11) -> 18
        , cons_1(11, 13) -> 18
        , cons_1(13, 2) -> 18
        , cons_1(13, 3) -> 18
        , cons_1(13, 5) -> 18
        , cons_1(13, 7) -> 18
        , cons_1(13, 11) -> 18
        , cons_1(13, 13) -> 18
        , cons_1(16, 17) -> 15
        , cons_2(26, 27) -> 25
        , cons_2(28, 29) -> 24
        , cons_3(26, 27) -> 34
        , cons_3(31, 32) -> 30
        , cons_4(33, 36) -> 37
        , cons_4(35, 27) -> 30
        , cons_5(39, 36) -> 38
        , 0_0() -> 5
        , 0_1() -> 16
        , 0_2() -> 26
        , 0_3() -> 33
        , U11_0(2, 2) -> 6
        , U11_0(2, 3) -> 6
        , U11_0(2, 5) -> 6
        , U11_0(2, 7) -> 6
        , U11_0(2, 11) -> 6
        , U11_0(2, 13) -> 6
        , U11_0(3, 2) -> 6
        , U11_0(3, 3) -> 6
        , U11_0(3, 5) -> 6
        , U11_0(3, 7) -> 6
        , U11_0(3, 11) -> 6
        , U11_0(3, 13) -> 6
        , U11_0(5, 2) -> 6
        , U11_0(5, 3) -> 6
        , U11_0(5, 5) -> 6
        , U11_0(5, 7) -> 6
        , U11_0(5, 11) -> 6
        , U11_0(5, 13) -> 6
        , U11_0(7, 2) -> 6
        , U11_0(7, 3) -> 6
        , U11_0(7, 5) -> 6
        , U11_0(7, 7) -> 6
        , U11_0(7, 11) -> 6
        , U11_0(7, 13) -> 6
        , U11_0(11, 2) -> 6
        , U11_0(11, 3) -> 6
        , U11_0(11, 5) -> 6
        , U11_0(11, 7) -> 6
        , U11_0(11, 11) -> 6
        , U11_0(11, 13) -> 6
        , U11_0(13, 2) -> 6
        , U11_0(13, 3) -> 6
        , U11_0(13, 5) -> 6
        , U11_0(13, 7) -> 6
        , U11_0(13, 11) -> 6
        , U11_0(13, 13) -> 6
        , U11_1(2, 2) -> 19
        , U11_1(2, 3) -> 19
        , U11_1(2, 5) -> 19
        , U11_1(2, 7) -> 19
        , U11_1(2, 11) -> 19
        , U11_1(2, 13) -> 19
        , U11_1(3, 2) -> 19
        , U11_1(3, 3) -> 19
        , U11_1(3, 5) -> 19
        , U11_1(3, 7) -> 19
        , U11_1(3, 11) -> 19
        , U11_1(3, 13) -> 19
        , U11_1(5, 2) -> 19
        , U11_1(5, 3) -> 19
        , U11_1(5, 5) -> 19
        , U11_1(5, 7) -> 19
        , U11_1(5, 11) -> 19
        , U11_1(5, 13) -> 19
        , U11_1(7, 2) -> 19
        , U11_1(7, 3) -> 19
        , U11_1(7, 5) -> 19
        , U11_1(7, 7) -> 19
        , U11_1(7, 11) -> 19
        , U11_1(7, 13) -> 19
        , U11_1(11, 2) -> 19
        , U11_1(11, 3) -> 19
        , U11_1(11, 5) -> 19
        , U11_1(11, 7) -> 19
        , U11_1(11, 11) -> 19
        , U11_1(11, 13) -> 19
        , U11_1(13, 2) -> 19
        , U11_1(13, 3) -> 19
        , U11_1(13, 5) -> 19
        , U11_1(13, 7) -> 19
        , U11_1(13, 11) -> 19
        , U11_1(13, 13) -> 19
        , tt_0() -> 7
        , tt_1() -> 16
        , tt_2() -> 26
        , tt_3() -> 33
        , U12_0(2, 2) -> 8
        , U12_0(2, 3) -> 8
        , U12_0(2, 5) -> 8
        , U12_0(2, 7) -> 8
        , U12_0(2, 11) -> 8
        , U12_0(2, 13) -> 8
        , U12_0(3, 2) -> 8
        , U12_0(3, 3) -> 8
        , U12_0(3, 5) -> 8
        , U12_0(3, 7) -> 8
        , U12_0(3, 11) -> 8
        , U12_0(3, 13) -> 8
        , U12_0(5, 2) -> 8
        , U12_0(5, 3) -> 8
        , U12_0(5, 5) -> 8
        , U12_0(5, 7) -> 8
        , U12_0(5, 11) -> 8
        , U12_0(5, 13) -> 8
        , U12_0(7, 2) -> 8
        , U12_0(7, 3) -> 8
        , U12_0(7, 5) -> 8
        , U12_0(7, 7) -> 8
        , U12_0(7, 11) -> 8
        , U12_0(7, 13) -> 8
        , U12_0(11, 2) -> 8
        , U12_0(11, 3) -> 8
        , U12_0(11, 5) -> 8
        , U12_0(11, 7) -> 8
        , U12_0(11, 11) -> 8
        , U12_0(11, 13) -> 8
        , U12_0(13, 2) -> 8
        , U12_0(13, 3) -> 8
        , U12_0(13, 5) -> 8
        , U12_0(13, 7) -> 8
        , U12_0(13, 11) -> 8
        , U12_0(13, 13) -> 8
        , U12_1(2, 2) -> 20
        , U12_1(2, 3) -> 20
        , U12_1(2, 5) -> 20
        , U12_1(2, 7) -> 20
        , U12_1(2, 11) -> 20
        , U12_1(2, 13) -> 20
        , U12_1(3, 2) -> 20
        , U12_1(3, 3) -> 20
        , U12_1(3, 5) -> 20
        , U12_1(3, 7) -> 20
        , U12_1(3, 11) -> 20
        , U12_1(3, 13) -> 20
        , U12_1(5, 2) -> 20
        , U12_1(5, 3) -> 20
        , U12_1(5, 5) -> 20
        , U12_1(5, 7) -> 20
        , U12_1(5, 11) -> 20
        , U12_1(5, 13) -> 20
        , U12_1(7, 2) -> 20
        , U12_1(7, 3) -> 20
        , U12_1(7, 5) -> 20
        , U12_1(7, 7) -> 20
        , U12_1(7, 11) -> 20
        , U12_1(7, 13) -> 20
        , U12_1(11, 2) -> 20
        , U12_1(11, 3) -> 20
        , U12_1(11, 5) -> 20
        , U12_1(11, 7) -> 20
        , U12_1(11, 11) -> 20
        , U12_1(11, 13) -> 20
        , U12_1(13, 2) -> 20
        , U12_1(13, 3) -> 20
        , U12_1(13, 5) -> 20
        , U12_1(13, 7) -> 20
        , U12_1(13, 11) -> 20
        , U12_1(13, 13) -> 20
        , s_0(2) -> 9
        , s_0(3) -> 9
        , s_0(5) -> 9
        , s_0(7) -> 9
        , s_0(11) -> 9
        , s_0(13) -> 9
        , s_1(2) -> 21
        , s_1(3) -> 21
        , s_1(5) -> 21
        , s_1(7) -> 21
        , s_1(11) -> 21
        , s_1(13) -> 21
        , length_0(2) -> 10
        , length_0(3) -> 10
        , length_0(5) -> 10
        , length_0(7) -> 10
        , length_0(11) -> 10
        , length_0(13) -> 10
        , length_1(2) -> 22
        , length_1(3) -> 22
        , length_1(5) -> 22
        , length_1(7) -> 22
        , length_1(11) -> 22
        , length_1(13) -> 22
        , nil_0() -> 11
        , nil_1() -> 16
        , nil_2() -> 26
        , nil_3() -> 33
        , proper_0(2) -> 12
        , proper_0(3) -> 12
        , proper_0(5) -> 12
        , proper_0(7) -> 12
        , proper_0(11) -> 12
        , proper_0(13) -> 12
        , proper_1(2) -> 23
        , proper_1(3) -> 23
        , proper_1(5) -> 23
        , proper_1(7) -> 23
        , proper_1(11) -> 23
        , proper_1(13) -> 23
        , proper_2(15) -> 24
        , proper_2(16) -> 28
        , proper_2(17) -> 29
        , proper_3(25) -> 30
        , proper_3(26) -> 31
        , proper_3(27) -> 32
        , ok_0(2) -> 13
        , ok_0(3) -> 13
        , ok_0(5) -> 13
        , ok_0(7) -> 13
        , ok_0(11) -> 13
        , ok_0(13) -> 13
        , ok_1(16) -> 12
        , ok_1(16) -> 23
        , ok_1(17) -> 12
        , ok_1(17) -> 23
        , ok_1(18) -> 4
        , ok_1(18) -> 18
        , ok_1(19) -> 6
        , ok_1(19) -> 19
        , ok_1(20) -> 8
        , ok_1(20) -> 20
        , ok_1(21) -> 9
        , ok_1(21) -> 21
        , ok_1(22) -> 10
        , ok_1(22) -> 22
        , ok_2(26) -> 28
        , ok_2(27) -> 29
        , ok_3(33) -> 31
        , ok_3(34) -> 24
        , ok_3(36) -> 32
        , ok_4(37) -> 30
        , top_0(2) -> 14
        , top_0(3) -> 14
        , top_0(5) -> 14
        , top_0(7) -> 14
        , top_0(11) -> 14
        , top_0(13) -> 14
        , top_1(23) -> 14
        , top_2(24) -> 14
        , top_3(30) -> 14
        , top_4(38) -> 14}