Problem Transformed CSR 04 ExIntrod GM01 C

Tool CaT

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

stdout:

YES(?,O(n^1))

Problem:
active(incr(nil())) -> mark(nil())
active(incr(cons(X,L))) -> mark(cons(s(X),incr(L)))
active(adx(nil())) -> mark(nil())
active(adx(cons(X,L))) -> mark(incr(cons(X,adx(L))))
active(nats()) -> mark(adx(zeros()))
active(zeros()) -> mark(cons(0(),zeros()))
active(head(cons(X,L))) -> mark(X)
active(tail(cons(X,L))) -> mark(L)
active(incr(X)) -> incr(active(X))
active(cons(X1,X2)) -> cons(active(X1),X2)
active(s(X)) -> s(active(X))
active(adx(X)) -> adx(active(X))
active(head(X)) -> head(active(X))
active(tail(X)) -> tail(active(X))
incr(mark(X)) -> mark(incr(X))
cons(mark(X1),X2) -> mark(cons(X1,X2))
s(mark(X)) -> mark(s(X))
adx(mark(X)) -> mark(adx(X))
head(mark(X)) -> mark(head(X))
tail(mark(X)) -> mark(tail(X))
proper(incr(X)) -> incr(proper(X))
proper(nil()) -> ok(nil())
proper(cons(X1,X2)) -> cons(proper(X1),proper(X2))
proper(s(X)) -> s(proper(X))
proper(adx(X)) -> adx(proper(X))
proper(nats()) -> ok(nats())
proper(zeros()) -> ok(zeros())
proper(0()) -> ok(0())
proper(head(X)) -> head(proper(X))
proper(tail(X)) -> tail(proper(X))
incr(ok(X)) -> ok(incr(X))
cons(ok(X1),ok(X2)) -> ok(cons(X1,X2))
s(ok(X)) -> ok(s(X))
adx(ok(X)) -> ok(adx(X))
head(ok(X)) -> ok(head(X))
tail(ok(X)) -> ok(tail(X))
top(mark(X)) -> top(proper(X))
top(ok(X)) -> top(active(X))

Proof:
Bounds Processor:
  bound: 10
  enrichment: match
  automaton:
   final states: {15,14,13,12,11,10,9,8,7}
   transitions:
    zeros3() -> 58*
    ok4(67) -> 51*
    ok4(79) -> 87*
    ok4(78) -> 86*
    adx4(69) -> 77*
    adx4(64) -> 51*
    adx4(58) -> 67*
    cons4(87,86) -> 74*
    cons4(79,78) -> 80*
    cons4(61,58) -> 67*
    cons4(63,42) -> 51*
    active4(67) -> 70*
    active4(42) -> 64*
    active4(44) -> 63*
    top4(70) -> 15*
    mark3(69) -> 64*
    mark4(80) -> 74*
    mark4(77) -> 51*
    adx5(80) -> 84*
    adx5(74) -> 70*
    active5(105) -> 91*
    active5(61) -> 73*
    active5(58) -> 74*
    cons5(97,96) -> 92*
    cons5(79,78) -> 98*
    cons5(73,58) -> 70*
    proper4(77) -> 70*
    proper4(61) -> 87*
    proper4(58) -> 86*
    04() -> 79*
    zeros4() -> 78*
    proper5(84) -> 91*
    proper5(79) -> 97*
    proper5(69) -> 74*
    proper5(78) -> 96*
    mark5(84) -> 70*
    active0(5) -> 7*
    active0(2) -> 7*
    active0(4) -> 7*
    active0(6) -> 7*
    active0(1) -> 7*
    active0(3) -> 7*
    top5(91) -> 15*
    incr0(5) -> 8*
    incr0(2) -> 8*
    incr0(4) -> 8*
    incr0(6) -> 8*
    incr0(1) -> 8*
    incr0(3) -> 8*
    adx6(92) -> 91*
    adx6(101) -> 151*
    adx6(98) -> 105*
    adx6(78) -> 108*
    nil0() -> 1*
    proper6(110) -> 118*
    proper6(80) -> 92*
    mark0(5) -> 2*
    mark0(2) -> 2*
    mark0(4) -> 2*
    mark0(6) -> 2*
    mark0(1) -> 2*
    mark0(3) -> 2*
    ok5(102) -> 133,97
    ok5(101) -> 141,96
    ok5(98) -> 74*
    cons0(3,1) -> 9*
    cons0(3,3) -> 9*
    cons0(3,5) -> 9*
    cons0(4,2) -> 9*
    cons0(4,4) -> 9*
    cons0(4,6) -> 9*
    cons0(5,1) -> 9*
    cons0(5,3) -> 9*
    cons0(5,5) -> 9*
    cons0(6,2) -> 9*
    cons0(1,2) -> 9*
    cons0(6,4) -> 9*
    cons0(1,4) -> 9*
    cons0(6,6) -> 9*
    cons0(1,6) -> 9*
    cons0(2,1) -> 9*
    cons0(2,3) -> 9*
    cons0(2,5) -> 9*
    cons0(3,2) -> 9*
    cons0(3,4) -> 9*
    cons0(3,6) -> 9*
    cons0(4,1) -> 9*
    cons0(4,3) -> 9*
    cons0(4,5) -> 9*
    cons0(5,2) -> 9*
    cons0(5,4) -> 9*
    cons0(5,6) -> 9*
    cons0(6,1) -> 9*
    cons0(1,1) -> 9*
    cons0(6,3) -> 9*
    cons0(1,3) -> 9*
    cons0(6,5) -> 9*
    cons0(1,5) -> 9*
    cons0(2,2) -> 9*
    cons0(2,4) -> 9*
    cons0(2,6) -> 9*
    ok6(105) -> 70*
    ok6(152) -> 194,147
    ok6(151) -> 132*
    ok6(106) -> 92*
    ok6(148) -> 145*
    ok6(155) -> 128*
    s0(5) -> 10*
    s0(2) -> 10*
    s0(4) -> 10*
    s0(6) -> 10*
    s0(1) -> 10*
    s0(3) -> 10*
    05() -> 102*
    adx0(5) -> 11*
    adx0(2) -> 11*
    adx0(4) -> 11*
    adx0(6) -> 11*
    adx0(1) -> 11*
    adx0(3) -> 11*
    zeros5() -> 101*
    nats0() -> 3*
    cons6(117,78) -> 92*
    cons6(102,151) -> 155*
    cons6(79,108) -> 109*
    cons6(102,101) -> 106*
    zeros0() -> 4*
    ok7(197) -> 181*
    ok7(204) -> 201*
    ok7(159) -> 186,144
    ok7(114) -> 91*
    ok7(206) -> 203*
    ok7(156) -> 118*
    ok7(160) -> 138*
    00() -> 5*
    adx7(152) -> 159*
    adx7(127) -> 118*
    adx7(194) -> 186*
    adx7(141) -> 132*
    adx7(106) -> 114*
    adx7(101) -> 120*
    head0(5) -> 12*
    head0(2) -> 12*
    head0(4) -> 12*
    head0(6) -> 12*
    head0(1) -> 12*
    head0(3) -> 12*
    active6(114) -> 118*
    active6(79) -> 117*
    active6(98) -> 92*
    tail0(5) -> 13*
    tail0(2) -> 13*
    tail0(4) -> 13*
    tail0(6) -> 13*
    tail0(1) -> 13*
    tail0(3) -> 13*
    mark6(110) -> 91*
    proper0(5) -> 14*
    proper0(2) -> 14*
    proper0(4) -> 14*
    proper0(6) -> 14*
    proper0(1) -> 14*
    proper0(3) -> 14*
    incr6(109) -> 110*
    ok0(5) -> 6*
    ok0(2) -> 6*
    ok0(4) -> 6*
    ok0(6) -> 6*
    ok0(1) -> 6*
    ok0(3) -> 6*
    top6(118) -> 15*
    top0(5) -> 15*
    top0(2) -> 15*
    top0(4) -> 15*
    top0(6) -> 15*
    top0(1) -> 15*
    top0(3) -> 15*
    incr7(155) -> 156*
    incr7(151) -> 162*
    incr7(121) -> 122*
    incr7(128) -> 118*
    top1(37) -> 15*
    proper7(122) -> 137*
    proper7(109) -> 128*
    proper7(79) -> 133*
    proper7(101) -> 194*
    proper7(108) -> 132*
    proper7(78) -> 141*
    active1(5) -> 37*
    active1(2) -> 37*
    active1(4) -> 37*
    active1(6) -> 37*
    active1(1) -> 37*
    active1(3) -> 37*
    active7(102) -> 131*
    active7(156) -> 137*
    active7(106) -> 127*
    proper1(5) -> 37*
    proper1(2) -> 37*
    proper1(4) -> 37*
    proper1(6) -> 37*
    proper1(1) -> 37*
    proper1(3) -> 37*
    mark7(122) -> 118*
    mark7(164) -> 137*
    ok1(35) -> 37,14
    ok1(25) -> 25,9
    ok1(20) -> 37,14
    ok1(27) -> 27,10
    ok1(29) -> 29,11
    ok1(31) -> 31,12
    ok1(33) -> 33,13
    ok1(23) -> 23,8
    ok1(18) -> 37,14
    cons7(131,101) -> 127*
    cons7(133,132) -> 128*
    cons7(163,162) -> 164*
    cons7(102,120) -> 121*
    cons7(131,151) -> 138*
    cons7(148,159) -> 160*
    tail1(5) -> 33*
    tail1(2) -> 33*
    tail1(4) -> 33*
    tail1(6) -> 33*
    tail1(1) -> 33*
    tail1(3) -> 33*
    top7(137) -> 15*
    head1(5) -> 31*
    head1(2) -> 31*
    head1(4) -> 31*
    head1(6) -> 31*
    head1(1) -> 31*
    head1(3) -> 31*
    incr8(160) -> 168*
    incr8(159) -> 172*
    incr8(186) -> 180*
    incr8(138) -> 137*
    adx1(5) -> 29*
    adx1(2) -> 29*
    adx1(4) -> 29*
    adx1(6) -> 29*
    adx1(1) -> 29*
    adx1(18) -> 19*
    adx1(3) -> 29*
    proper8(120) -> 144*
    proper8(162) -> 180*
    proper8(152) -> 203*
    proper8(102) -> 145*
    proper8(164) -> 170*
    proper8(151) -> 186*
    proper8(121) -> 138*
    proper8(101) -> 147*
    proper8(163) -> 181*
    s1(5) -> 27*
    s1(2) -> 27*
    s1(4) -> 27*
    s1(6) -> 27*
    s1(1) -> 27*
    s1(3) -> 27*
    cons8(185,159) -> 179*
    cons8(181,180) -> 170*
    cons8(173,172) -> 174*
    cons8(145,144) -> 138*
    cons8(197,172) -> 211*
    cons1(2,6) -> 25*
    cons1(3,1) -> 25*
    cons1(3,3) -> 25*
    cons1(3,5) -> 25*
    cons1(4,2) -> 25*
    cons1(4,4) -> 25*
    cons1(4,6) -> 25*
    cons1(5,1) -> 25*
    cons1(5,3) -> 25*
    cons1(5,5) -> 25*
    cons1(6,2) -> 25*
    cons1(1,2) -> 25*
    cons1(6,4) -> 25*
    cons1(1,4) -> 25*
    cons1(6,6) -> 25*
    cons1(1,6) -> 25*
    cons1(2,1) -> 25*
    cons1(2,3) -> 25*
    cons1(2,5) -> 25*
    cons1(3,2) -> 25*
    cons1(3,4) -> 25*
    cons1(3,6) -> 25*
    cons1(4,1) -> 25*
    cons1(4,3) -> 25*
    cons1(4,5) -> 25*
    cons1(5,2) -> 25*
    cons1(5,4) -> 25*
    cons1(5,6) -> 25*
    cons1(20,18) -> 19*
    cons1(6,1) -> 25*
    cons1(1,1) -> 25*
    cons1(6,3) -> 25*
    cons1(1,3) -> 25*
    cons1(6,5) -> 25*
    cons1(1,5) -> 25*
    cons1(2,2) -> 25*
    cons1(2,4) -> 25*
    06() -> 148*
    incr1(5) -> 23*
    incr1(2) -> 23*
    incr1(4) -> 23*
    incr1(6) -> 23*
    incr1(1) -> 23*
    incr1(3) -> 23*
    adx8(147) -> 144*
    adx8(206) -> 212*
    adx8(203) -> 198*
    01() -> 20*
    zeros6() -> 152*
    zeros1() -> 18*
    ok8(212) -> 198*
    ok8(172) -> 180*
    ok8(211) -> 170*
    ok8(208) -> 193*
    ok8(168) -> 137*
    nats1() -> 35*
    active8(155) -> 138*
    active8(168) -> 170*
    active8(148) -> 185*
    nil1() -> 35*
    s7(102) -> 163*
    s7(148) -> 197*
    mark1(25) -> 25,9
    mark1(27) -> 27,10
    mark1(29) -> 29,11
    mark1(19) -> 37,7
    mark1(31) -> 31,12
    mark1(33) -> 33,13
    mark1(23) -> 23,8
    top8(170) -> 15*
    top2(39) -> 15*
    incr9(212) -> 215*
    incr9(179) -> 170*
    incr9(198) -> 192*
    active2(35) -> 39*
    active2(20) -> 39*
    active2(18) -> 39*
    active9(160) -> 179*
    active9(197) -> 217*
    active9(204) -> 224*
    active9(211) -> 188*
    proper2(20) -> 49*
    proper2(19) -> 39*
    proper2(18) -> 48*
    mark8(174) -> 170*
    adx2(42) -> 43*
    adx2(48) -> 39*
    s8(145) -> 181*
    s8(204) -> 208*
    s8(148) -> 173*
    s8(185) -> 217*
    cons2(44,42) -> 43*
    cons2(49,48) -> 39*
    top9(188) -> 15*
    mark2(43) -> 39*
    proper9(172) -> 192*
    proper9(174) -> 188*
    proper9(159) -> 198*
    proper9(173) -> 193*
    proper9(148) -> 201*
    02() -> 44*
    cons9(208,215) -> 218*
    cons9(193,192) -> 188*
    cons9(217,172) -> 188*
    zeros2() -> 42*
    s9(224) -> 223*
    s9(201) -> 193*
    top3(51) -> 15*
    07() -> 204*
    proper3(42) -> 52*
    proper3(44) -> 53*
    proper3(43) -> 51*
    zeros7() -> 206*
    ok2(42) -> 48*
    ok2(44) -> 49*
    ok9(218) -> 188*
    ok9(215) -> 192*
    ok3(61) -> 53*
    ok3(56) -> 39*
    ok3(58) -> 52*
    top10(220) -> 15*
    adx3(52) -> 51*
    adx3(42) -> 56*
    active10(218) -> 220*
    active10(208) -> 223*
    cons3(44,42) -> 56*
    cons3(61,58) -> 69*
    cons3(53,52) -> 51*
    cons10(223,215) -> 220*
    active3(56) -> 51*
    03() -> 61*
  problem:

  Qed

Tool IRC1

Execution Time	Unknown
Answer	MAYBE
Input	Transformed CSR 04 ExIntrod GM01 C

stdout:

MAYBE

Tool IRC2

Execution Time	Unknown
Answer	YES(?,O(n^1))
Input	Transformed CSR 04 ExIntrod GM01 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(incr(nil())) -> mark(nil())
     , active(incr(cons(X, L))) -> mark(cons(s(X), incr(L)))
     , active(adx(nil())) -> mark(nil())
     , active(adx(cons(X, L))) -> mark(incr(cons(X, adx(L))))
     , active(nats()) -> mark(adx(zeros()))
     , active(zeros()) -> mark(cons(0(), zeros()))
     , active(head(cons(X, L))) -> mark(X)
     , active(tail(cons(X, L))) -> mark(L)
     , active(incr(X)) -> incr(active(X))
     , active(cons(X1, X2)) -> cons(active(X1), X2)
     , active(s(X)) -> s(active(X))
     , active(adx(X)) -> adx(active(X))
     , active(head(X)) -> head(active(X))
     , active(tail(X)) -> tail(active(X))
     , incr(mark(X)) -> mark(incr(X))
     , cons(mark(X1), X2) -> mark(cons(X1, X2))
     , s(mark(X)) -> mark(s(X))
     , adx(mark(X)) -> mark(adx(X))
     , head(mark(X)) -> mark(head(X))
     , tail(mark(X)) -> mark(tail(X))
     , proper(incr(X)) -> incr(proper(X))
     , proper(nil()) -> ok(nil())
     , proper(cons(X1, X2)) -> cons(proper(X1), proper(X2))
     , proper(s(X)) -> s(proper(X))
     , proper(adx(X)) -> adx(proper(X))
     , proper(nats()) -> ok(nats())
     , proper(zeros()) -> ok(zeros())
     , proper(0()) -> ok(0())
     , proper(head(X)) -> head(proper(X))
     , proper(tail(X)) -> tail(proper(X))
     , incr(ok(X)) -> ok(incr(X))
     , cons(ok(X1), ok(X2)) -> ok(cons(X1, X2))
     , s(ok(X)) -> ok(s(X))
     , adx(ok(X)) -> ok(adx(X))
     , head(ok(X)) -> ok(head(X))
     , tail(ok(X)) -> ok(tail(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(incr(nil())) -> mark(nil())
          , active(incr(cons(X, L))) -> mark(cons(s(X), incr(L)))
          , active(adx(nil())) -> mark(nil())
          , active(adx(cons(X, L))) -> mark(incr(cons(X, adx(L))))
          , active(nats()) -> mark(adx(zeros()))
          , active(zeros()) -> mark(cons(0(), zeros()))
          , active(head(cons(X, L))) -> mark(X)
          , active(tail(cons(X, L))) -> mark(L)
          , active(incr(X)) -> incr(active(X))
          , active(cons(X1, X2)) -> cons(active(X1), X2)
          , active(s(X)) -> s(active(X))
          , active(adx(X)) -> adx(active(X))
          , active(head(X)) -> head(active(X))
          , active(tail(X)) -> tail(active(X))
          , incr(mark(X)) -> mark(incr(X))
          , cons(mark(X1), X2) -> mark(cons(X1, X2))
          , s(mark(X)) -> mark(s(X))
          , adx(mark(X)) -> mark(adx(X))
          , head(mark(X)) -> mark(head(X))
          , tail(mark(X)) -> mark(tail(X))
          , proper(incr(X)) -> incr(proper(X))
          , proper(nil()) -> ok(nil())
          , proper(cons(X1, X2)) -> cons(proper(X1), proper(X2))
          , proper(s(X)) -> s(proper(X))
          , proper(adx(X)) -> adx(proper(X))
          , proper(nats()) -> ok(nats())
          , proper(zeros()) -> ok(zeros())
          , proper(0()) -> ok(0())
          , proper(head(X)) -> head(proper(X))
          , proper(tail(X)) -> tail(proper(X))
          , incr(ok(X)) -> ok(incr(X))
          , cons(ok(X1), ok(X2)) -> ok(cons(X1, X2))
          , s(ok(X)) -> ok(s(X))
          , adx(ok(X)) -> ok(adx(X))
          , head(ok(X)) -> ok(head(X))
          , tail(ok(X)) -> ok(tail(X))
          , top(mark(X)) -> top(proper(X))
          , top(ok(X)) -> top(active(X))}

     Proof Output:
       The problem is match-bounded by 10.
       The enriched problem is compatible with the following automaton:
       {  active_0(3) -> 1
        , active_0(4) -> 1
        , active_0(8) -> 1
        , active_0(9) -> 1
        , active_0(10) -> 1
        , active_0(14) -> 1
        , active_1(3) -> 26
        , active_1(4) -> 26
        , active_1(8) -> 26
        , active_1(9) -> 26
        , active_1(10) -> 26
        , active_1(14) -> 26
        , active_2(17) -> 27
        , active_2(18) -> 27
        , active_2(25) -> 27
        , active_3(33) -> 34
        , active_4(29) -> 36
        , active_4(30) -> 35
        , active_4(41) -> 42
        , active_5(39) -> 45
        , active_5(40) -> 44
        , active_5(56) -> 51
        , active_6(48) -> 70
        , active_6(55) -> 54
        , active_6(65) -> 66
        , active_7(63) -> 78
        , active_7(64) -> 71
        , active_7(87) -> 77
        , active_8(84) -> 98
        , active_8(85) -> 79
        , active_8(92) -> 93
        , active_9(88) -> 97
        , active_9(101) -> 115
        , active_9(108) -> 120
        , active_9(113) -> 102
        , active_10(109) -> 119
        , active_10(117) -> 118
        , incr_0(3) -> 2
        , incr_0(4) -> 2
        , incr_0(8) -> 2
        , incr_0(9) -> 2
        , incr_0(10) -> 2
        , incr_0(14) -> 2
        , incr_1(3) -> 19
        , incr_1(4) -> 19
        , incr_1(8) -> 19
        , incr_1(9) -> 19
        , incr_1(10) -> 19
        , incr_1(14) -> 19
        , incr_6(58) -> 57
        , incr_7(68) -> 67
        , incr_7(72) -> 66
        , incr_7(76) -> 91
        , incr_7(85) -> 87
        , incr_8(79) -> 77
        , incr_8(86) -> 96
        , incr_8(88) -> 92
        , incr_8(103) -> 100
        , incr_9(97) -> 93
        , incr_9(110) -> 105
        , incr_9(114) -> 116
        , nil_0() -> 3
        , nil_1() -> 25
        , mark_0(3) -> 4
        , mark_0(4) -> 4
        , mark_0(8) -> 4
        , mark_0(9) -> 4
        , mark_0(10) -> 4
        , mark_0(14) -> 4
        , mark_1(16) -> 1
        , mark_1(16) -> 26
        , mark_1(19) -> 2
        , mark_1(19) -> 19
        , mark_1(20) -> 5
        , mark_1(20) -> 20
        , mark_1(21) -> 6
        , mark_1(21) -> 21
        , mark_1(22) -> 7
        , mark_1(22) -> 22
        , mark_1(23) -> 11
        , mark_1(23) -> 23
        , mark_1(24) -> 12
        , mark_1(24) -> 24
        , mark_2(28) -> 27
        , mark_3(43) -> 36
        , mark_4(46) -> 34
        , mark_4(47) -> 45
        , mark_5(50) -> 42
        , mark_6(57) -> 51
        , mark_7(67) -> 66
        , mark_7(89) -> 77
        , mark_8(94) -> 93
        , cons_0(3, 3) -> 5
        , cons_0(3, 4) -> 5
        , cons_0(3, 8) -> 5
        , cons_0(3, 9) -> 5
        , cons_0(3, 10) -> 5
        , cons_0(3, 14) -> 5
        , cons_0(4, 3) -> 5
        , cons_0(4, 4) -> 5
        , cons_0(4, 8) -> 5
        , cons_0(4, 9) -> 5
        , cons_0(4, 10) -> 5
        , cons_0(4, 14) -> 5
        , cons_0(8, 3) -> 5
        , cons_0(8, 4) -> 5
        , cons_0(8, 8) -> 5
        , cons_0(8, 9) -> 5
        , cons_0(8, 10) -> 5
        , cons_0(8, 14) -> 5
        , cons_0(9, 3) -> 5
        , cons_0(9, 4) -> 5
        , cons_0(9, 8) -> 5
        , cons_0(9, 9) -> 5
        , cons_0(9, 10) -> 5
        , cons_0(9, 14) -> 5
        , cons_0(10, 3) -> 5
        , cons_0(10, 4) -> 5
        , cons_0(10, 8) -> 5
        , cons_0(10, 9) -> 5
        , cons_0(10, 10) -> 5
        , cons_0(10, 14) -> 5
        , cons_0(14, 3) -> 5
        , cons_0(14, 4) -> 5
        , cons_0(14, 8) -> 5
        , cons_0(14, 9) -> 5
        , cons_0(14, 10) -> 5
        , cons_0(14, 14) -> 5
        , cons_1(3, 3) -> 20
        , cons_1(3, 4) -> 20
        , cons_1(3, 8) -> 20
        , cons_1(3, 9) -> 20
        , cons_1(3, 10) -> 20
        , cons_1(3, 14) -> 20
        , cons_1(4, 3) -> 20
        , cons_1(4, 4) -> 20
        , cons_1(4, 8) -> 20
        , cons_1(4, 9) -> 20
        , cons_1(4, 10) -> 20
        , cons_1(4, 14) -> 20
        , cons_1(8, 3) -> 20
        , cons_1(8, 4) -> 20
        , cons_1(8, 8) -> 20
        , cons_1(8, 9) -> 20
        , cons_1(8, 10) -> 20
        , cons_1(8, 14) -> 20
        , cons_1(9, 3) -> 20
        , cons_1(9, 4) -> 20
        , cons_1(9, 8) -> 20
        , cons_1(9, 9) -> 20
        , cons_1(9, 10) -> 20
        , cons_1(9, 14) -> 20
        , cons_1(10, 3) -> 20
        , cons_1(10, 4) -> 20
        , cons_1(10, 8) -> 20
        , cons_1(10, 9) -> 20
        , cons_1(10, 10) -> 20
        , cons_1(10, 14) -> 20
        , cons_1(14, 3) -> 20
        , cons_1(14, 4) -> 20
        , cons_1(14, 8) -> 20
        , cons_1(14, 9) -> 20
        , cons_1(14, 10) -> 20
        , cons_1(14, 14) -> 20
        , cons_1(18, 17) -> 16
        , cons_2(30, 29) -> 28
        , cons_2(31, 32) -> 27
        , cons_3(30, 29) -> 33
        , cons_3(37, 38) -> 34
        , cons_3(40, 39) -> 43
        , cons_4(35, 29) -> 34
        , cons_4(40, 39) -> 41
        , cons_4(48, 49) -> 47
        , cons_4(52, 53) -> 45
        , cons_5(44, 39) -> 42
        , cons_5(48, 49) -> 55
        , cons_5(60, 61) -> 54
        , cons_6(48, 59) -> 58
        , cons_6(63, 62) -> 64
        , cons_6(63, 76) -> 85
        , cons_6(70, 49) -> 54
        , cons_7(63, 69) -> 68
        , cons_7(73, 74) -> 72
        , cons_7(78, 62) -> 71
        , cons_7(78, 76) -> 79
        , cons_7(84, 86) -> 88
        , cons_7(90, 91) -> 89
        , cons_8(80, 81) -> 79
        , cons_8(95, 96) -> 94
        , cons_8(98, 86) -> 97
        , cons_8(99, 100) -> 93
        , cons_8(101, 96) -> 113
        , cons_9(104, 105) -> 102
        , cons_9(109, 116) -> 117
        , cons_9(115, 96) -> 102
        , cons_10(119, 116) -> 118
        , s_0(3) -> 6
        , s_0(4) -> 6
        , s_0(8) -> 6
        , s_0(9) -> 6
        , s_0(10) -> 6
        , s_0(14) -> 6
        , s_1(3) -> 21
        , s_1(4) -> 21
        , s_1(8) -> 21
        , s_1(9) -> 21
        , s_1(10) -> 21
        , s_1(14) -> 21
        , s_7(63) -> 90
        , s_7(84) -> 101
        , s_8(80) -> 99
        , s_8(84) -> 95
        , s_8(98) -> 115
        , s_8(108) -> 109
        , s_9(106) -> 104
        , s_9(120) -> 119
        , adx_0(3) -> 7
        , adx_0(4) -> 7
        , adx_0(8) -> 7
        , adx_0(9) -> 7
        , adx_0(10) -> 7
        , adx_0(14) -> 7
        , adx_1(3) -> 22
        , adx_1(4) -> 22
        , adx_1(8) -> 22
        , adx_1(9) -> 22
        , adx_1(10) -> 22
        , adx_1(14) -> 22
        , adx_1(17) -> 16
        , adx_2(29) -> 28
        , adx_2(32) -> 27
        , adx_3(29) -> 33
        , adx_3(38) -> 34
        , adx_4(36) -> 34
        , adx_4(39) -> 41
        , adx_4(43) -> 46
        , adx_5(45) -> 42
        , adx_5(47) -> 50
        , adx_6(49) -> 59
        , adx_6(54) -> 51
        , adx_6(55) -> 56
        , adx_6(62) -> 76
        , adx_7(62) -> 69
        , adx_7(64) -> 65
        , adx_7(71) -> 66
        , adx_7(75) -> 74
        , adx_7(83) -> 86
        , adx_7(107) -> 103
        , adx_8(82) -> 81
        , adx_8(111) -> 110
        , adx_8(112) -> 114
        , nats_0() -> 8
        , nats_1() -> 25
        , zeros_0() -> 9
        , zeros_1() -> 17
        , zeros_2() -> 29
        , zeros_3() -> 39
        , zeros_4() -> 49
        , zeros_5() -> 62
        , zeros_6() -> 83
        , zeros_7() -> 112
        , 0_0() -> 10
        , 0_1() -> 18
        , 0_2() -> 30
        , 0_3() -> 40
        , 0_4() -> 48
        , 0_5() -> 63
        , 0_6() -> 84
        , 0_7() -> 108
        , head_0(3) -> 11
        , head_0(4) -> 11
        , head_0(8) -> 11
        , head_0(9) -> 11
        , head_0(10) -> 11
        , head_0(14) -> 11
        , head_1(3) -> 23
        , head_1(4) -> 23
        , head_1(8) -> 23
        , head_1(9) -> 23
        , head_1(10) -> 23
        , head_1(14) -> 23
        , tail_0(3) -> 12
        , tail_0(4) -> 12
        , tail_0(8) -> 12
        , tail_0(9) -> 12
        , tail_0(10) -> 12
        , tail_0(14) -> 12
        , tail_1(3) -> 24
        , tail_1(4) -> 24
        , tail_1(8) -> 24
        , tail_1(9) -> 24
        , tail_1(10) -> 24
        , tail_1(14) -> 24
        , proper_0(3) -> 13
        , proper_0(4) -> 13
        , proper_0(8) -> 13
        , proper_0(9) -> 13
        , proper_0(10) -> 13
        , proper_0(14) -> 13
        , proper_1(3) -> 26
        , proper_1(4) -> 26
        , proper_1(8) -> 26
        , proper_1(9) -> 26
        , proper_1(10) -> 26
        , proper_1(14) -> 26
        , proper_2(16) -> 27
        , proper_2(17) -> 32
        , proper_2(18) -> 31
        , proper_3(28) -> 34
        , proper_3(29) -> 38
        , proper_3(30) -> 37
        , proper_4(39) -> 53
        , proper_4(40) -> 52
        , proper_4(46) -> 42
        , proper_5(43) -> 45
        , proper_5(48) -> 60
        , proper_5(49) -> 61
        , proper_5(50) -> 51
        , proper_6(47) -> 54
        , proper_6(57) -> 66
        , proper_7(48) -> 73
        , proper_7(49) -> 75
        , proper_7(58) -> 72
        , proper_7(59) -> 74
        , proper_7(62) -> 107
        , proper_7(67) -> 77
        , proper_8(62) -> 82
        , proper_8(63) -> 80
        , proper_8(68) -> 79
        , proper_8(69) -> 81
        , proper_8(76) -> 103
        , proper_8(83) -> 111
        , proper_8(89) -> 93
        , proper_8(90) -> 99
        , proper_8(91) -> 100
        , proper_9(84) -> 106
        , proper_9(86) -> 110
        , proper_9(94) -> 102
        , proper_9(95) -> 104
        , proper_9(96) -> 105
        , ok_0(3) -> 14
        , ok_0(4) -> 14
        , ok_0(8) -> 14
        , ok_0(9) -> 14
        , ok_0(10) -> 14
        , ok_0(14) -> 14
        , ok_1(17) -> 13
        , ok_1(17) -> 26
        , ok_1(18) -> 13
        , ok_1(18) -> 26
        , ok_1(19) -> 2
        , ok_1(19) -> 19
        , ok_1(20) -> 5
        , ok_1(20) -> 20
        , ok_1(21) -> 6
        , ok_1(21) -> 21
        , ok_1(22) -> 7
        , ok_1(22) -> 22
        , ok_1(23) -> 11
        , ok_1(23) -> 23
        , ok_1(24) -> 12
        , ok_1(24) -> 24
        , ok_1(25) -> 13
        , ok_1(25) -> 26
        , ok_2(29) -> 32
        , ok_2(30) -> 31
        , ok_3(33) -> 27
        , ok_3(39) -> 38
        , ok_3(40) -> 37
        , ok_4(41) -> 34
        , ok_4(48) -> 52
        , ok_4(49) -> 53
        , ok_5(55) -> 45
        , ok_5(62) -> 61
        , ok_5(62) -> 75
        , ok_5(63) -> 60
        , ok_5(63) -> 73
        , ok_6(56) -> 42
        , ok_6(64) -> 54
        , ok_6(76) -> 74
        , ok_6(83) -> 82
        , ok_6(83) -> 107
        , ok_6(84) -> 80
        , ok_6(85) -> 72
        , ok_7(65) -> 51
        , ok_7(86) -> 81
        , ok_7(86) -> 103
        , ok_7(87) -> 66
        , ok_7(88) -> 79
        , ok_7(101) -> 99
        , ok_7(108) -> 106
        , ok_7(112) -> 111
        , ok_8(92) -> 77
        , ok_8(96) -> 100
        , ok_8(109) -> 104
        , ok_8(113) -> 93
        , ok_8(114) -> 110
        , ok_9(116) -> 105
        , ok_9(117) -> 102
        , top_0(3) -> 15
        , top_0(4) -> 15
        , top_0(8) -> 15
        , top_0(9) -> 15
        , top_0(10) -> 15
        , top_0(14) -> 15
        , top_1(26) -> 15
        , top_2(27) -> 15
        , top_3(34) -> 15
        , top_4(42) -> 15
        , top_5(51) -> 15
        , top_6(66) -> 15
        , top_7(77) -> 15
        , top_8(93) -> 15
        , top_9(102) -> 15
        , top_10(118) -> 15}

Tool RC1

Execution Time	Unknown
Answer	MAYBE
Input	Transformed CSR 04 ExIntrod GM01 C

stdout:

MAYBE

Tool RC2

Execution Time	Unknown
Answer	YES(?,O(n^1))
Input	Transformed CSR 04 ExIntrod GM01 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(incr(nil())) -> mark(nil())
     , active(incr(cons(X, L))) -> mark(cons(s(X), incr(L)))
     , active(adx(nil())) -> mark(nil())
     , active(adx(cons(X, L))) -> mark(incr(cons(X, adx(L))))
     , active(nats()) -> mark(adx(zeros()))
     , active(zeros()) -> mark(cons(0(), zeros()))
     , active(head(cons(X, L))) -> mark(X)
     , active(tail(cons(X, L))) -> mark(L)
     , active(incr(X)) -> incr(active(X))
     , active(cons(X1, X2)) -> cons(active(X1), X2)
     , active(s(X)) -> s(active(X))
     , active(adx(X)) -> adx(active(X))
     , active(head(X)) -> head(active(X))
     , active(tail(X)) -> tail(active(X))
     , incr(mark(X)) -> mark(incr(X))
     , cons(mark(X1), X2) -> mark(cons(X1, X2))
     , s(mark(X)) -> mark(s(X))
     , adx(mark(X)) -> mark(adx(X))
     , head(mark(X)) -> mark(head(X))
     , tail(mark(X)) -> mark(tail(X))
     , proper(incr(X)) -> incr(proper(X))
     , proper(nil()) -> ok(nil())
     , proper(cons(X1, X2)) -> cons(proper(X1), proper(X2))
     , proper(s(X)) -> s(proper(X))
     , proper(adx(X)) -> adx(proper(X))
     , proper(nats()) -> ok(nats())
     , proper(zeros()) -> ok(zeros())
     , proper(0()) -> ok(0())
     , proper(head(X)) -> head(proper(X))
     , proper(tail(X)) -> tail(proper(X))
     , incr(ok(X)) -> ok(incr(X))
     , cons(ok(X1), ok(X2)) -> ok(cons(X1, X2))
     , s(ok(X)) -> ok(s(X))
     , adx(ok(X)) -> ok(adx(X))
     , head(ok(X)) -> ok(head(X))
     , tail(ok(X)) -> ok(tail(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(incr(nil())) -> mark(nil())
          , active(incr(cons(X, L))) -> mark(cons(s(X), incr(L)))
          , active(adx(nil())) -> mark(nil())
          , active(adx(cons(X, L))) -> mark(incr(cons(X, adx(L))))
          , active(nats()) -> mark(adx(zeros()))
          , active(zeros()) -> mark(cons(0(), zeros()))
          , active(head(cons(X, L))) -> mark(X)
          , active(tail(cons(X, L))) -> mark(L)
          , active(incr(X)) -> incr(active(X))
          , active(cons(X1, X2)) -> cons(active(X1), X2)
          , active(s(X)) -> s(active(X))
          , active(adx(X)) -> adx(active(X))
          , active(head(X)) -> head(active(X))
          , active(tail(X)) -> tail(active(X))
          , incr(mark(X)) -> mark(incr(X))
          , cons(mark(X1), X2) -> mark(cons(X1, X2))
          , s(mark(X)) -> mark(s(X))
          , adx(mark(X)) -> mark(adx(X))
          , head(mark(X)) -> mark(head(X))
          , tail(mark(X)) -> mark(tail(X))
          , proper(incr(X)) -> incr(proper(X))
          , proper(nil()) -> ok(nil())
          , proper(cons(X1, X2)) -> cons(proper(X1), proper(X2))
          , proper(s(X)) -> s(proper(X))
          , proper(adx(X)) -> adx(proper(X))
          , proper(nats()) -> ok(nats())
          , proper(zeros()) -> ok(zeros())
          , proper(0()) -> ok(0())
          , proper(head(X)) -> head(proper(X))
          , proper(tail(X)) -> tail(proper(X))
          , incr(ok(X)) -> ok(incr(X))
          , cons(ok(X1), ok(X2)) -> ok(cons(X1, X2))
          , s(ok(X)) -> ok(s(X))
          , adx(ok(X)) -> ok(adx(X))
          , head(ok(X)) -> ok(head(X))
          , tail(ok(X)) -> ok(tail(X))
          , top(mark(X)) -> top(proper(X))
          , top(ok(X)) -> top(active(X))}

     Proof Output:
       The problem is match-bounded by 10.
       The enriched problem is compatible with the following automaton:
       {  active_0(3) -> 1
        , active_0(4) -> 1
        , active_0(8) -> 1
        , active_0(9) -> 1
        , active_0(10) -> 1
        , active_0(14) -> 1
        , active_1(3) -> 26
        , active_1(4) -> 26
        , active_1(8) -> 26
        , active_1(9) -> 26
        , active_1(10) -> 26
        , active_1(14) -> 26
        , active_2(17) -> 27
        , active_2(18) -> 27
        , active_2(25) -> 27
        , active_3(33) -> 34
        , active_4(29) -> 36
        , active_4(30) -> 35
        , active_4(41) -> 42
        , active_5(39) -> 45
        , active_5(40) -> 44
        , active_5(56) -> 51
        , active_6(48) -> 70
        , active_6(55) -> 54
        , active_6(65) -> 66
        , active_7(63) -> 78
        , active_7(64) -> 71
        , active_7(87) -> 77
        , active_8(84) -> 98
        , active_8(85) -> 79
        , active_8(92) -> 93
        , active_9(88) -> 97
        , active_9(101) -> 115
        , active_9(108) -> 120
        , active_9(113) -> 102
        , active_10(109) -> 119
        , active_10(117) -> 118
        , incr_0(3) -> 2
        , incr_0(4) -> 2
        , incr_0(8) -> 2
        , incr_0(9) -> 2
        , incr_0(10) -> 2
        , incr_0(14) -> 2
        , incr_1(3) -> 19
        , incr_1(4) -> 19
        , incr_1(8) -> 19
        , incr_1(9) -> 19
        , incr_1(10) -> 19
        , incr_1(14) -> 19
        , incr_6(58) -> 57
        , incr_7(68) -> 67
        , incr_7(72) -> 66
        , incr_7(76) -> 91
        , incr_7(85) -> 87
        , incr_8(79) -> 77
        , incr_8(86) -> 96
        , incr_8(88) -> 92
        , incr_8(103) -> 100
        , incr_9(97) -> 93
        , incr_9(110) -> 105
        , incr_9(114) -> 116
        , nil_0() -> 3
        , nil_1() -> 25
        , mark_0(3) -> 4
        , mark_0(4) -> 4
        , mark_0(8) -> 4
        , mark_0(9) -> 4
        , mark_0(10) -> 4
        , mark_0(14) -> 4
        , mark_1(16) -> 1
        , mark_1(16) -> 26
        , mark_1(19) -> 2
        , mark_1(19) -> 19
        , mark_1(20) -> 5
        , mark_1(20) -> 20
        , mark_1(21) -> 6
        , mark_1(21) -> 21
        , mark_1(22) -> 7
        , mark_1(22) -> 22
        , mark_1(23) -> 11
        , mark_1(23) -> 23
        , mark_1(24) -> 12
        , mark_1(24) -> 24
        , mark_2(28) -> 27
        , mark_3(43) -> 36
        , mark_4(46) -> 34
        , mark_4(47) -> 45
        , mark_5(50) -> 42
        , mark_6(57) -> 51
        , mark_7(67) -> 66
        , mark_7(89) -> 77
        , mark_8(94) -> 93
        , cons_0(3, 3) -> 5
        , cons_0(3, 4) -> 5
        , cons_0(3, 8) -> 5
        , cons_0(3, 9) -> 5
        , cons_0(3, 10) -> 5
        , cons_0(3, 14) -> 5
        , cons_0(4, 3) -> 5
        , cons_0(4, 4) -> 5
        , cons_0(4, 8) -> 5
        , cons_0(4, 9) -> 5
        , cons_0(4, 10) -> 5
        , cons_0(4, 14) -> 5
        , cons_0(8, 3) -> 5
        , cons_0(8, 4) -> 5
        , cons_0(8, 8) -> 5
        , cons_0(8, 9) -> 5
        , cons_0(8, 10) -> 5
        , cons_0(8, 14) -> 5
        , cons_0(9, 3) -> 5
        , cons_0(9, 4) -> 5
        , cons_0(9, 8) -> 5
        , cons_0(9, 9) -> 5
        , cons_0(9, 10) -> 5
        , cons_0(9, 14) -> 5
        , cons_0(10, 3) -> 5
        , cons_0(10, 4) -> 5
        , cons_0(10, 8) -> 5
        , cons_0(10, 9) -> 5
        , cons_0(10, 10) -> 5
        , cons_0(10, 14) -> 5
        , cons_0(14, 3) -> 5
        , cons_0(14, 4) -> 5
        , cons_0(14, 8) -> 5
        , cons_0(14, 9) -> 5
        , cons_0(14, 10) -> 5
        , cons_0(14, 14) -> 5
        , cons_1(3, 3) -> 20
        , cons_1(3, 4) -> 20
        , cons_1(3, 8) -> 20
        , cons_1(3, 9) -> 20
        , cons_1(3, 10) -> 20
        , cons_1(3, 14) -> 20
        , cons_1(4, 3) -> 20
        , cons_1(4, 4) -> 20
        , cons_1(4, 8) -> 20
        , cons_1(4, 9) -> 20
        , cons_1(4, 10) -> 20
        , cons_1(4, 14) -> 20
        , cons_1(8, 3) -> 20
        , cons_1(8, 4) -> 20
        , cons_1(8, 8) -> 20
        , cons_1(8, 9) -> 20
        , cons_1(8, 10) -> 20
        , cons_1(8, 14) -> 20
        , cons_1(9, 3) -> 20
        , cons_1(9, 4) -> 20
        , cons_1(9, 8) -> 20
        , cons_1(9, 9) -> 20
        , cons_1(9, 10) -> 20
        , cons_1(9, 14) -> 20
        , cons_1(10, 3) -> 20
        , cons_1(10, 4) -> 20
        , cons_1(10, 8) -> 20
        , cons_1(10, 9) -> 20
        , cons_1(10, 10) -> 20
        , cons_1(10, 14) -> 20
        , cons_1(14, 3) -> 20
        , cons_1(14, 4) -> 20
        , cons_1(14, 8) -> 20
        , cons_1(14, 9) -> 20
        , cons_1(14, 10) -> 20
        , cons_1(14, 14) -> 20
        , cons_1(18, 17) -> 16
        , cons_2(30, 29) -> 28
        , cons_2(31, 32) -> 27
        , cons_3(30, 29) -> 33
        , cons_3(37, 38) -> 34
        , cons_3(40, 39) -> 43
        , cons_4(35, 29) -> 34
        , cons_4(40, 39) -> 41
        , cons_4(48, 49) -> 47
        , cons_4(52, 53) -> 45
        , cons_5(44, 39) -> 42
        , cons_5(48, 49) -> 55
        , cons_5(60, 61) -> 54
        , cons_6(48, 59) -> 58
        , cons_6(63, 62) -> 64
        , cons_6(63, 76) -> 85
        , cons_6(70, 49) -> 54
        , cons_7(63, 69) -> 68
        , cons_7(73, 74) -> 72
        , cons_7(78, 62) -> 71
        , cons_7(78, 76) -> 79
        , cons_7(84, 86) -> 88
        , cons_7(90, 91) -> 89
        , cons_8(80, 81) -> 79
        , cons_8(95, 96) -> 94
        , cons_8(98, 86) -> 97
        , cons_8(99, 100) -> 93
        , cons_8(101, 96) -> 113
        , cons_9(104, 105) -> 102
        , cons_9(109, 116) -> 117
        , cons_9(115, 96) -> 102
        , cons_10(119, 116) -> 118
        , s_0(3) -> 6
        , s_0(4) -> 6
        , s_0(8) -> 6
        , s_0(9) -> 6
        , s_0(10) -> 6
        , s_0(14) -> 6
        , s_1(3) -> 21
        , s_1(4) -> 21
        , s_1(8) -> 21
        , s_1(9) -> 21
        , s_1(10) -> 21
        , s_1(14) -> 21
        , s_7(63) -> 90
        , s_7(84) -> 101
        , s_8(80) -> 99
        , s_8(84) -> 95
        , s_8(98) -> 115
        , s_8(108) -> 109
        , s_9(106) -> 104
        , s_9(120) -> 119
        , adx_0(3) -> 7
        , adx_0(4) -> 7
        , adx_0(8) -> 7
        , adx_0(9) -> 7
        , adx_0(10) -> 7
        , adx_0(14) -> 7
        , adx_1(3) -> 22
        , adx_1(4) -> 22
        , adx_1(8) -> 22
        , adx_1(9) -> 22
        , adx_1(10) -> 22
        , adx_1(14) -> 22
        , adx_1(17) -> 16
        , adx_2(29) -> 28
        , adx_2(32) -> 27
        , adx_3(29) -> 33
        , adx_3(38) -> 34
        , adx_4(36) -> 34
        , adx_4(39) -> 41
        , adx_4(43) -> 46
        , adx_5(45) -> 42
        , adx_5(47) -> 50
        , adx_6(49) -> 59
        , adx_6(54) -> 51
        , adx_6(55) -> 56
        , adx_6(62) -> 76
        , adx_7(62) -> 69
        , adx_7(64) -> 65
        , adx_7(71) -> 66
        , adx_7(75) -> 74
        , adx_7(83) -> 86
        , adx_7(107) -> 103
        , adx_8(82) -> 81
        , adx_8(111) -> 110
        , adx_8(112) -> 114
        , nats_0() -> 8
        , nats_1() -> 25
        , zeros_0() -> 9
        , zeros_1() -> 17
        , zeros_2() -> 29
        , zeros_3() -> 39
        , zeros_4() -> 49
        , zeros_5() -> 62
        , zeros_6() -> 83
        , zeros_7() -> 112
        , 0_0() -> 10
        , 0_1() -> 18
        , 0_2() -> 30
        , 0_3() -> 40
        , 0_4() -> 48
        , 0_5() -> 63
        , 0_6() -> 84
        , 0_7() -> 108
        , head_0(3) -> 11
        , head_0(4) -> 11
        , head_0(8) -> 11
        , head_0(9) -> 11
        , head_0(10) -> 11
        , head_0(14) -> 11
        , head_1(3) -> 23
        , head_1(4) -> 23
        , head_1(8) -> 23
        , head_1(9) -> 23
        , head_1(10) -> 23
        , head_1(14) -> 23
        , tail_0(3) -> 12
        , tail_0(4) -> 12
        , tail_0(8) -> 12
        , tail_0(9) -> 12
        , tail_0(10) -> 12
        , tail_0(14) -> 12
        , tail_1(3) -> 24
        , tail_1(4) -> 24
        , tail_1(8) -> 24
        , tail_1(9) -> 24
        , tail_1(10) -> 24
        , tail_1(14) -> 24
        , proper_0(3) -> 13
        , proper_0(4) -> 13
        , proper_0(8) -> 13
        , proper_0(9) -> 13
        , proper_0(10) -> 13
        , proper_0(14) -> 13
        , proper_1(3) -> 26
        , proper_1(4) -> 26
        , proper_1(8) -> 26
        , proper_1(9) -> 26
        , proper_1(10) -> 26
        , proper_1(14) -> 26
        , proper_2(16) -> 27
        , proper_2(17) -> 32
        , proper_2(18) -> 31
        , proper_3(28) -> 34
        , proper_3(29) -> 38
        , proper_3(30) -> 37
        , proper_4(39) -> 53
        , proper_4(40) -> 52
        , proper_4(46) -> 42
        , proper_5(43) -> 45
        , proper_5(48) -> 60
        , proper_5(49) -> 61
        , proper_5(50) -> 51
        , proper_6(47) -> 54
        , proper_6(57) -> 66
        , proper_7(48) -> 73
        , proper_7(49) -> 75
        , proper_7(58) -> 72
        , proper_7(59) -> 74
        , proper_7(62) -> 107
        , proper_7(67) -> 77
        , proper_8(62) -> 82
        , proper_8(63) -> 80
        , proper_8(68) -> 79
        , proper_8(69) -> 81
        , proper_8(76) -> 103
        , proper_8(83) -> 111
        , proper_8(89) -> 93
        , proper_8(90) -> 99
        , proper_8(91) -> 100
        , proper_9(84) -> 106
        , proper_9(86) -> 110
        , proper_9(94) -> 102
        , proper_9(95) -> 104
        , proper_9(96) -> 105
        , ok_0(3) -> 14
        , ok_0(4) -> 14
        , ok_0(8) -> 14
        , ok_0(9) -> 14
        , ok_0(10) -> 14
        , ok_0(14) -> 14
        , ok_1(17) -> 13
        , ok_1(17) -> 26
        , ok_1(18) -> 13
        , ok_1(18) -> 26
        , ok_1(19) -> 2
        , ok_1(19) -> 19
        , ok_1(20) -> 5
        , ok_1(20) -> 20
        , ok_1(21) -> 6
        , ok_1(21) -> 21
        , ok_1(22) -> 7
        , ok_1(22) -> 22
        , ok_1(23) -> 11
        , ok_1(23) -> 23
        , ok_1(24) -> 12
        , ok_1(24) -> 24
        , ok_1(25) -> 13
        , ok_1(25) -> 26
        , ok_2(29) -> 32
        , ok_2(30) -> 31
        , ok_3(33) -> 27
        , ok_3(39) -> 38
        , ok_3(40) -> 37
        , ok_4(41) -> 34
        , ok_4(48) -> 52
        , ok_4(49) -> 53
        , ok_5(55) -> 45
        , ok_5(62) -> 61
        , ok_5(62) -> 75
        , ok_5(63) -> 60
        , ok_5(63) -> 73
        , ok_6(56) -> 42
        , ok_6(64) -> 54
        , ok_6(76) -> 74
        , ok_6(83) -> 82
        , ok_6(83) -> 107
        , ok_6(84) -> 80
        , ok_6(85) -> 72
        , ok_7(65) -> 51
        , ok_7(86) -> 81
        , ok_7(86) -> 103
        , ok_7(87) -> 66
        , ok_7(88) -> 79
        , ok_7(101) -> 99
        , ok_7(108) -> 106
        , ok_7(112) -> 111
        , ok_8(92) -> 77
        , ok_8(96) -> 100
        , ok_8(109) -> 104
        , ok_8(113) -> 93
        , ok_8(114) -> 110
        , ok_9(116) -> 105
        , ok_9(117) -> 102
        , top_0(3) -> 15
        , top_0(4) -> 15
        , top_0(8) -> 15
        , top_0(9) -> 15
        , top_0(10) -> 15
        , top_0(14) -> 15
        , top_1(26) -> 15
        , top_2(27) -> 15
        , top_3(34) -> 15
        , top_4(42) -> 15
        , top_5(51) -> 15
        , top_6(66) -> 15
        , top_7(77) -> 15
        , top_8(93) -> 15
        , top_9(102) -> 15
        , top_10(118) -> 15}