Problem Transformed CSR 04 Ex1 Luc04b C

Tool CaT

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

stdout:

YES(?,O(n^1))

Problem:
active(nats()) -> mark(cons(0(),incr(nats())))
active(pairs()) -> mark(cons(0(),incr(odds())))
active(odds()) -> mark(incr(pairs()))
active(incr(cons(X,XS))) -> mark(cons(s(X),incr(XS)))
active(head(cons(X,XS))) -> mark(X)
active(tail(cons(X,XS))) -> mark(XS)
active(cons(X1,X2)) -> cons(active(X1),X2)
active(incr(X)) -> incr(active(X))
active(s(X)) -> s(active(X))
active(head(X)) -> head(active(X))
active(tail(X)) -> tail(active(X))
cons(mark(X1),X2) -> mark(cons(X1,X2))
incr(mark(X)) -> mark(incr(X))
s(mark(X)) -> mark(s(X))
head(mark(X)) -> mark(head(X))
tail(mark(X)) -> mark(tail(X))
proper(nats()) -> ok(nats())
proper(cons(X1,X2)) -> cons(proper(X1),proper(X2))
proper(0()) -> ok(0())
proper(incr(X)) -> incr(proper(X))
proper(pairs()) -> ok(pairs())
proper(odds()) -> ok(odds())
proper(s(X)) -> s(proper(X))
proper(head(X)) -> head(proper(X))
proper(tail(X)) -> tail(proper(X))
cons(ok(X1),ok(X2)) -> ok(cons(X1,X2))
incr(ok(X)) -> ok(incr(X))
s(ok(X)) -> ok(s(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: 9
  enrichment: match
  automaton:
   final states: {14,13,12,11,10,9,8,7}
   transitions:
    cons3(45,74) -> 66*
    cons3(62,61) -> 58*
    cons3(67,81) -> 82*
    active3(66) -> 58*
    pairs3() -> 71*
    03() -> 67*
    ok4(80) -> 58*
    ok4(87) -> 61*
    ok4(99) -> 114*
    ok4(101) -> 108*
    ok4(118) -> 114*
    incr4(82) -> 94*
    incr4(77) -> 87*
    incr4(114) -> 107*
    incr4(99) -> 100*
    incr4(76) -> 58*
    incr4(71) -> 80*
    odds3() -> 77*
    nats3() -> 77*
    active4(80) -> 90*
    active4(45) -> 86*
    active4(48) -> 76*
    top4(90) -> 14*
    cons4(108,107) -> 91*
    cons4(86,74) -> 58*
    cons4(101,100) -> 102*
    cons4(67,87) -> 80*
    mark3(82) -> 76*
    mark4(102) -> 91*
    mark4(94) -> 58*
    incr5(102) -> 105*
    incr5(99) -> 127*
    incr5(126) -> 119*
    incr5(91) -> 90*
    incr5(118) -> 127*
    active5(67) -> 103*
    active5(71) -> 91*
    active5(133) -> 112*
    active0(5) -> 7*
    active0(2) -> 7*
    active0(4) -> 7*
    active0(6) -> 7*
    active0(1) -> 7*
    active0(3) -> 7*
    proper4(77) -> 114*
    proper4(67) -> 108*
    proper4(94) -> 90*
    proper4(81) -> 107*
    nats0() -> 1*
    cons5(103,87) -> 90*
    cons5(101,127) -> 132*
    cons5(120,119) -> 115*
    mark0(5) -> 2*
    mark0(2) -> 2*
    mark0(4) -> 2*
    mark0(6) -> 2*
    mark0(1) -> 2*
    mark0(3) -> 2*
    04() -> 101*
    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*
    odds4() -> 99*
    00() -> 3*
    proper5(105) -> 112*
    proper5(100) -> 119*
    proper5(82) -> 91*
    proper5(99) -> 126*
    proper5(101) -> 120*
    incr0(5) -> 9*
    incr0(2) -> 9*
    incr0(4) -> 9*
    incr0(6) -> 9*
    incr0(1) -> 9*
    incr0(3) -> 9*
    mark5(105) -> 90*
    pairs0() -> 4*
    top5(112) -> 14*
    odds0() -> 5*
    incr6(115) -> 112*
    incr6(132) -> 133*
    incr6(127) -> 139*
    incr6(129) -> 136*
    incr6(176) -> 165*
    incr6(178) -> 136*
    s0(5) -> 10*
    s0(2) -> 10*
    s0(4) -> 10*
    s0(6) -> 10*
    s0(1) -> 10*
    s0(3) -> 10*
    proper6(102) -> 115*
    proper6(99) -> 176*
    proper6(141) -> 149*
    proper6(118) -> 176*
    head0(5) -> 11*
    head0(2) -> 11*
    head0(4) -> 11*
    head0(6) -> 11*
    head0(1) -> 11*
    head0(3) -> 11*
    nats4() -> 118*
    tail0(5) -> 12*
    tail0(2) -> 12*
    tail0(4) -> 12*
    tail0(6) -> 12*
    tail0(1) -> 12*
    tail0(3) -> 12*
    ok5(132) -> 91*
    ok5(127) -> 107*
    ok5(129) -> 176,126
    ok5(178) -> 176*
    ok5(123) -> 168,120
    proper0(5) -> 13*
    proper0(2) -> 13*
    proper0(4) -> 13*
    proper0(6) -> 13*
    proper0(1) -> 13*
    proper0(3) -> 13*
    05() -> 123*
    ok0(5) -> 6*
    ok0(2) -> 6*
    ok0(4) -> 6*
    ok0(6) -> 6*
    ok0(1) -> 6*
    ok0(3) -> 6*
    odds5() -> 129*
    top0(5) -> 14*
    top0(2) -> 14*
    top0(4) -> 14*
    top0(6) -> 14*
    top0(1) -> 14*
    top0(3) -> 14*
    ok6(152) -> 160*
    ok6(137) -> 115*
    ok6(136) -> 165,119
    ok6(188) -> 186*
    ok6(183) -> 181*
    ok6(133) -> 90*
    top1(36) -> 14*
    cons6(140,139) -> 141*
    cons6(123,136) -> 137*
    cons6(148,127) -> 115*
    active1(5) -> 36*
    active1(2) -> 36*
    active1(4) -> 36*
    active1(6) -> 36*
    active1(1) -> 36*
    active1(3) -> 36*
    ok7(145) -> 112*
    ok7(191) -> 179*
    ok7(151) -> 159*
    ok7(153) -> 149*
    ok7(190) -> 174*
    proper1(5) -> 36*
    proper1(2) -> 36*
    proper1(4) -> 36*
    proper1(6) -> 36*
    proper1(1) -> 36*
    proper1(3) -> 36*
    incr7(137) -> 145*
    incr7(186) -> 179*
    incr7(136) -> 151*
    incr7(188) -> 191*
    incr7(158) -> 149*
    incr7(165) -> 159*
    ok1(30) -> 30,10
    ok1(15) -> 36,13
    ok1(32) -> 32,11
    ok1(17) -> 36,13
    ok1(34) -> 34,12
    ok1(26) -> 26,8
    ok1(28) -> 28,9
    ok1(23) -> 36,13
    active6(145) -> 149*
    active6(132) -> 115*
    active6(101) -> 148*
    tail1(5) -> 34*
    tail1(2) -> 34*
    tail1(4) -> 34*
    tail1(6) -> 34*
    tail1(1) -> 34*
    tail1(3) -> 34*
    mark6(141) -> 112*
    head1(5) -> 32*
    head1(2) -> 32*
    head1(4) -> 32*
    head1(6) -> 32*
    head1(1) -> 32*
    head1(3) -> 32*
    s6(101) -> 140*
    s1(5) -> 30*
    s1(2) -> 30*
    s1(4) -> 30*
    s1(6) -> 30*
    s1(1) -> 30*
    s1(3) -> 30*
    top6(149) -> 14*
    incr1(15) -> 16*
    incr1(5) -> 28*
    incr1(2) -> 28*
    incr1(4) -> 28*
    incr1(6) -> 28*
    incr1(1) -> 28*
    incr1(23) -> 18*
    incr1(3) -> 28*
    cons7(160,159) -> 149*
    cons7(152,151) -> 153*
    cons7(164,136) -> 158*
    cons1(2,6) -> 26*
    cons1(17,16) -> 18*
    cons1(3,1) -> 26*
    cons1(3,3) -> 26*
    cons1(3,5) -> 26*
    cons1(4,2) -> 26*
    cons1(4,4) -> 26*
    cons1(4,6) -> 26*
    cons1(5,1) -> 26*
    cons1(5,3) -> 26*
    cons1(5,5) -> 26*
    cons1(6,2) -> 26*
    cons1(1,2) -> 26*
    cons1(6,4) -> 26*
    cons1(1,4) -> 26*
    cons1(6,6) -> 26*
    cons1(1,6) -> 26*
    cons1(2,1) -> 26*
    cons1(2,3) -> 26*
    cons1(2,5) -> 26*
    cons1(3,2) -> 26*
    cons1(3,4) -> 26*
    cons1(3,6) -> 26*
    cons1(4,1) -> 26*
    cons1(4,3) -> 26*
    cons1(4,5) -> 26*
    cons1(5,2) -> 26*
    cons1(5,4) -> 26*
    cons1(5,6) -> 26*
    cons1(6,1) -> 26*
    cons1(1,1) -> 26*
    cons1(6,3) -> 26*
    cons1(1,3) -> 26*
    cons1(6,5) -> 26*
    cons1(1,5) -> 26*
    cons1(2,2) -> 26*
    cons1(2,4) -> 26*
    proper7(140) -> 160*
    proper7(127) -> 165*
    proper7(139) -> 159*
    proper7(129) -> 186*
    proper7(101) -> 168*
    proper7(178) -> 186*
    proper7(153) -> 169*
    odds1() -> 15*
    active7(137) -> 158*
    active7(153) -> 169*
    active7(123) -> 164*
    pairs1() -> 23*
    mark7(153) -> 149*
    01() -> 17*
    s7(183) -> 190*
    s7(168) -> 160*
    s7(123) -> 152*
    nats1() -> 15*
    top7(169) -> 14*
    mark1(30) -> 30,10
    mark1(32) -> 32,11
    mark1(34) -> 34,12
    mark1(26) -> 26,8
    mark1(28) -> 28,9
    mark1(18) -> 36,7
    cons8(174,173) -> 169*
    cons8(196,151) -> 169*
    cons8(190,194) -> 197*
    top2(38) -> 14*
    proper8(152) -> 174*
    proper8(151) -> 173*
    proper8(136) -> 179*
    proper8(123) -> 181*
    active2(15) -> 38*
    active2(17) -> 38*
    active2(23) -> 38*
    s8(181) -> 174*
    s8(205) -> 204*
    s8(200) -> 196*
    proper2(15) -> 56*
    proper2(17) -> 50*
    proper2(16) -> 49*
    proper2(23) -> 54*
    proper2(18) -> 38*
    incr8(179) -> 173*
    incr8(191) -> 194*
    incr2(54) -> 38*
    incr2(56) -> 49*
    incr2(48) -> 46*
    incr2(43) -> 44*
    nats5() -> 178*
    cons2(50,49) -> 38*
    cons2(45,44) -> 46*
    06() -> 183*
    mark2(46) -> 38*
    odds6() -> 188*
    pairs2() -> 48*
    nats6() -> 188*
    02() -> 45*
    ok8(197) -> 169*
    ok8(194) -> 173*
    odds2() -> 43*
    active8(197) -> 201*
    active8(152) -> 196*
    active8(183) -> 205*
    active8(123) -> 200*
    nats2() -> 43*
    top8(201) -> 14*
    top3(58) -> 14*
    cons9(204,194) -> 201*
    proper3(45) -> 62*
    proper3(44) -> 61*
    proper3(46) -> 58*
    proper3(48) -> 63*
    proper3(43) -> 70*
    active9(190) -> 204*
    ok2(45) -> 50*
    ok2(48) -> 54*
    ok2(43) -> 56*
    ok3(77) -> 70*
    ok3(67) -> 62*
    ok3(74) -> 49*
    ok3(71) -> 63*
    ok3(66) -> 38*
    incr3(70) -> 61*
    incr3(77) -> 81*
    incr3(63) -> 58*
    incr3(48) -> 66*
    incr3(43) -> 74*
  problem:

  Qed

Tool IRC1

Execution Time	Unknown
Answer	MAYBE
Input	Transformed CSR 04 Ex1 Luc04b C

stdout:

MAYBE

Tool IRC2

Execution Time	Unknown
Answer	YES(?,O(n^1))
Input	Transformed CSR 04 Ex1 Luc04b 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(nats()) -> mark(cons(0(), incr(nats())))
     , active(pairs()) -> mark(cons(0(), incr(odds())))
     , active(odds()) -> mark(incr(pairs()))
     , active(incr(cons(X, XS))) -> mark(cons(s(X), incr(XS)))
     , active(head(cons(X, XS))) -> mark(X)
     , active(tail(cons(X, XS))) -> mark(XS)
     , active(cons(X1, X2)) -> cons(active(X1), X2)
     , active(incr(X)) -> incr(active(X))
     , active(s(X)) -> s(active(X))
     , active(head(X)) -> head(active(X))
     , active(tail(X)) -> tail(active(X))
     , cons(mark(X1), X2) -> mark(cons(X1, X2))
     , incr(mark(X)) -> mark(incr(X))
     , s(mark(X)) -> mark(s(X))
     , head(mark(X)) -> mark(head(X))
     , tail(mark(X)) -> mark(tail(X))
     , proper(nats()) -> ok(nats())
     , proper(cons(X1, X2)) -> cons(proper(X1), proper(X2))
     , proper(0()) -> ok(0())
     , proper(incr(X)) -> incr(proper(X))
     , proper(pairs()) -> ok(pairs())
     , proper(odds()) -> ok(odds())
     , proper(s(X)) -> s(proper(X))
     , proper(head(X)) -> head(proper(X))
     , proper(tail(X)) -> tail(proper(X))
     , cons(ok(X1), ok(X2)) -> ok(cons(X1, X2))
     , incr(ok(X)) -> ok(incr(X))
     , s(ok(X)) -> ok(s(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(nats()) -> mark(cons(0(), incr(nats())))
          , active(pairs()) -> mark(cons(0(), incr(odds())))
          , active(odds()) -> mark(incr(pairs()))
          , active(incr(cons(X, XS))) -> mark(cons(s(X), incr(XS)))
          , active(head(cons(X, XS))) -> mark(X)
          , active(tail(cons(X, XS))) -> mark(XS)
          , active(cons(X1, X2)) -> cons(active(X1), X2)
          , active(incr(X)) -> incr(active(X))
          , active(s(X)) -> s(active(X))
          , active(head(X)) -> head(active(X))
          , active(tail(X)) -> tail(active(X))
          , cons(mark(X1), X2) -> mark(cons(X1, X2))
          , incr(mark(X)) -> mark(incr(X))
          , s(mark(X)) -> mark(s(X))
          , head(mark(X)) -> mark(head(X))
          , tail(mark(X)) -> mark(tail(X))
          , proper(nats()) -> ok(nats())
          , proper(cons(X1, X2)) -> cons(proper(X1), proper(X2))
          , proper(0()) -> ok(0())
          , proper(incr(X)) -> incr(proper(X))
          , proper(pairs()) -> ok(pairs())
          , proper(odds()) -> ok(odds())
          , proper(s(X)) -> s(proper(X))
          , proper(head(X)) -> head(proper(X))
          , proper(tail(X)) -> tail(proper(X))
          , cons(ok(X1), ok(X2)) -> ok(cons(X1, X2))
          , incr(ok(X)) -> ok(incr(X))
          , s(ok(X)) -> ok(s(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 9.
       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(8) -> 1
        , active_0(13) -> 1
        , active_1(2) -> 25
        , active_1(3) -> 25
        , active_1(5) -> 25
        , active_1(7) -> 25
        , active_1(8) -> 25
        , active_1(13) -> 25
        , active_2(16) -> 26
        , active_2(18) -> 26
        , active_2(19) -> 26
        , active_3(37) -> 38
        , active_4(28) -> 52
        , active_4(31) -> 39
        , active_4(47) -> 49
        , active_5(42) -> 59
        , active_5(45) -> 53
        , active_5(74) -> 61
        , active_6(56) -> 84
        , active_6(72) -> 65
        , active_6(79) -> 80
        , active_7(69) -> 91
        , active_7(78) -> 85
        , active_7(103) -> 90
        , active_8(97) -> 105
        , active_8(98) -> 109
        , active_8(106) -> 107
        , active_9(102) -> 108
        , nats_0() -> 2
        , nats_1() -> 18
        , nats_2() -> 30
        , nats_3() -> 46
        , nats_4() -> 58
        , nats_5() -> 71
        , nats_6() -> 100
        , mark_0(2) -> 3
        , mark_0(3) -> 3
        , mark_0(5) -> 3
        , mark_0(7) -> 3
        , mark_0(8) -> 3
        , mark_0(13) -> 3
        , mark_1(15) -> 1
        , mark_1(15) -> 25
        , mark_1(20) -> 4
        , mark_1(20) -> 20
        , mark_1(21) -> 6
        , mark_1(21) -> 21
        , mark_1(22) -> 9
        , mark_1(22) -> 22
        , mark_1(23) -> 10
        , mark_1(23) -> 23
        , mark_1(24) -> 11
        , mark_1(24) -> 24
        , mark_2(27) -> 26
        , mark_3(50) -> 39
        , mark_4(54) -> 38
        , mark_4(55) -> 53
        , mark_5(60) -> 49
        , mark_6(75) -> 61
        , mark_7(81) -> 80
        , cons_0(2, 2) -> 4
        , cons_0(2, 3) -> 4
        , cons_0(2, 5) -> 4
        , cons_0(2, 7) -> 4
        , cons_0(2, 8) -> 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, 8) -> 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, 8) -> 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, 8) -> 4
        , cons_0(7, 13) -> 4
        , cons_0(8, 2) -> 4
        , cons_0(8, 3) -> 4
        , cons_0(8, 5) -> 4
        , cons_0(8, 7) -> 4
        , cons_0(8, 8) -> 4
        , cons_0(8, 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, 8) -> 4
        , cons_0(13, 13) -> 4
        , cons_1(2, 2) -> 20
        , cons_1(2, 3) -> 20
        , cons_1(2, 5) -> 20
        , cons_1(2, 7) -> 20
        , cons_1(2, 8) -> 20
        , cons_1(2, 13) -> 20
        , cons_1(3, 2) -> 20
        , cons_1(3, 3) -> 20
        , cons_1(3, 5) -> 20
        , cons_1(3, 7) -> 20
        , cons_1(3, 8) -> 20
        , cons_1(3, 13) -> 20
        , cons_1(5, 2) -> 20
        , cons_1(5, 3) -> 20
        , cons_1(5, 5) -> 20
        , cons_1(5, 7) -> 20
        , cons_1(5, 8) -> 20
        , cons_1(5, 13) -> 20
        , cons_1(7, 2) -> 20
        , cons_1(7, 3) -> 20
        , cons_1(7, 5) -> 20
        , cons_1(7, 7) -> 20
        , cons_1(7, 8) -> 20
        , cons_1(7, 13) -> 20
        , cons_1(8, 2) -> 20
        , cons_1(8, 3) -> 20
        , cons_1(8, 5) -> 20
        , cons_1(8, 7) -> 20
        , cons_1(8, 8) -> 20
        , cons_1(8, 13) -> 20
        , cons_1(13, 2) -> 20
        , cons_1(13, 3) -> 20
        , cons_1(13, 5) -> 20
        , cons_1(13, 7) -> 20
        , cons_1(13, 8) -> 20
        , cons_1(13, 13) -> 20
        , cons_1(16, 17) -> 15
        , cons_2(28, 29) -> 27
        , cons_2(32, 33) -> 26
        , cons_3(28, 36) -> 37
        , cons_3(40, 41) -> 38
        , cons_3(42, 51) -> 50
        , cons_4(42, 48) -> 47
        , cons_4(52, 36) -> 38
        , cons_4(56, 57) -> 55
        , cons_4(62, 63) -> 53
        , cons_5(56, 66) -> 72
        , cons_5(59, 48) -> 49
        , cons_5(67, 68) -> 65
        , cons_6(69, 73) -> 78
        , cons_6(76, 77) -> 75
        , cons_6(84, 66) -> 65
        , cons_7(82, 83) -> 81
        , cons_7(86, 87) -> 80
        , cons_7(91, 73) -> 85
        , cons_7(97, 83) -> 103
        , cons_8(92, 93) -> 90
        , cons_8(102, 104) -> 106
        , cons_8(105, 83) -> 90
        , cons_9(108, 104) -> 107
        , 0_0() -> 5
        , 0_1() -> 16
        , 0_2() -> 28
        , 0_3() -> 42
        , 0_4() -> 56
        , 0_5() -> 69
        , 0_6() -> 98
        , incr_0(2) -> 6
        , incr_0(3) -> 6
        , incr_0(5) -> 6
        , incr_0(7) -> 6
        , incr_0(8) -> 6
        , incr_0(13) -> 6
        , incr_1(2) -> 21
        , incr_1(3) -> 21
        , incr_1(5) -> 21
        , incr_1(7) -> 21
        , incr_1(8) -> 21
        , incr_1(13) -> 21
        , incr_1(18) -> 17
        , incr_1(19) -> 15
        , incr_2(30) -> 29
        , incr_2(31) -> 27
        , incr_2(34) -> 33
        , incr_2(35) -> 26
        , incr_3(30) -> 36
        , incr_3(31) -> 37
        , incr_3(43) -> 41
        , incr_3(44) -> 38
        , incr_3(46) -> 51
        , incr_4(39) -> 38
        , incr_4(45) -> 47
        , incr_4(46) -> 48
        , incr_4(50) -> 54
        , incr_4(58) -> 57
        , incr_4(64) -> 63
        , incr_5(53) -> 49
        , incr_5(55) -> 60
        , incr_5(58) -> 66
        , incr_5(70) -> 68
        , incr_6(65) -> 61
        , incr_6(66) -> 77
        , incr_6(71) -> 73
        , incr_6(72) -> 74
        , incr_6(94) -> 88
        , incr_7(73) -> 83
        , incr_7(78) -> 79
        , incr_7(85) -> 80
        , incr_7(88) -> 87
        , incr_7(99) -> 95
        , incr_7(100) -> 101
        , incr_8(95) -> 93
        , incr_8(101) -> 104
        , pairs_0() -> 7
        , pairs_1() -> 19
        , pairs_2() -> 31
        , pairs_3() -> 45
        , odds_0() -> 8
        , odds_1() -> 18
        , odds_2() -> 30
        , odds_3() -> 46
        , odds_4() -> 58
        , odds_5() -> 71
        , odds_6() -> 100
        , s_0(2) -> 9
        , s_0(3) -> 9
        , s_0(5) -> 9
        , s_0(7) -> 9
        , s_0(8) -> 9
        , s_0(13) -> 9
        , s_1(2) -> 22
        , s_1(3) -> 22
        , s_1(5) -> 22
        , s_1(7) -> 22
        , s_1(8) -> 22
        , s_1(13) -> 22
        , s_6(56) -> 76
        , s_6(69) -> 97
        , s_7(69) -> 82
        , s_7(89) -> 86
        , s_7(91) -> 105
        , s_7(98) -> 102
        , s_8(96) -> 92
        , s_8(109) -> 108
        , head_0(2) -> 10
        , head_0(3) -> 10
        , head_0(5) -> 10
        , head_0(7) -> 10
        , head_0(8) -> 10
        , head_0(13) -> 10
        , head_1(2) -> 23
        , head_1(3) -> 23
        , head_1(5) -> 23
        , head_1(7) -> 23
        , head_1(8) -> 23
        , head_1(13) -> 23
        , tail_0(2) -> 11
        , tail_0(3) -> 11
        , tail_0(5) -> 11
        , tail_0(7) -> 11
        , tail_0(8) -> 11
        , tail_0(13) -> 11
        , tail_1(2) -> 24
        , tail_1(3) -> 24
        , tail_1(5) -> 24
        , tail_1(7) -> 24
        , tail_1(8) -> 24
        , tail_1(13) -> 24
        , proper_0(2) -> 12
        , proper_0(3) -> 12
        , proper_0(5) -> 12
        , proper_0(7) -> 12
        , proper_0(8) -> 12
        , proper_0(13) -> 12
        , proper_1(2) -> 25
        , proper_1(3) -> 25
        , proper_1(5) -> 25
        , proper_1(7) -> 25
        , proper_1(8) -> 25
        , proper_1(13) -> 25
        , proper_2(15) -> 26
        , proper_2(16) -> 32
        , proper_2(17) -> 33
        , proper_2(18) -> 34
        , proper_2(19) -> 35
        , proper_3(27) -> 38
        , proper_3(28) -> 40
        , proper_3(29) -> 41
        , proper_3(30) -> 43
        , proper_3(31) -> 44
        , proper_4(42) -> 62
        , proper_4(46) -> 64
        , proper_4(51) -> 63
        , proper_4(54) -> 49
        , proper_5(50) -> 53
        , proper_5(56) -> 67
        , proper_5(57) -> 68
        , proper_5(58) -> 70
        , proper_5(60) -> 61
        , proper_6(55) -> 65
        , proper_6(58) -> 94
        , proper_6(75) -> 80
        , proper_7(56) -> 89
        , proper_7(66) -> 88
        , proper_7(71) -> 99
        , proper_7(76) -> 86
        , proper_7(77) -> 87
        , proper_7(81) -> 90
        , proper_8(69) -> 96
        , proper_8(73) -> 95
        , proper_8(82) -> 92
        , proper_8(83) -> 93
        , ok_0(2) -> 13
        , ok_0(3) -> 13
        , ok_0(5) -> 13
        , ok_0(7) -> 13
        , ok_0(8) -> 13
        , ok_0(13) -> 13
        , ok_1(16) -> 12
        , ok_1(16) -> 25
        , ok_1(18) -> 12
        , ok_1(18) -> 25
        , ok_1(19) -> 12
        , ok_1(19) -> 25
        , ok_1(20) -> 4
        , ok_1(20) -> 20
        , ok_1(21) -> 6
        , ok_1(21) -> 21
        , ok_1(22) -> 9
        , ok_1(22) -> 22
        , ok_1(23) -> 10
        , ok_1(23) -> 23
        , ok_1(24) -> 11
        , ok_1(24) -> 24
        , ok_2(28) -> 32
        , ok_2(30) -> 34
        , ok_2(31) -> 35
        , ok_3(36) -> 33
        , ok_3(37) -> 26
        , ok_3(42) -> 40
        , ok_3(45) -> 44
        , ok_3(46) -> 43
        , ok_4(47) -> 38
        , ok_4(48) -> 41
        , ok_4(56) -> 62
        , ok_4(58) -> 64
        , ok_5(66) -> 63
        , ok_5(69) -> 67
        , ok_5(69) -> 89
        , ok_5(71) -> 70
        , ok_5(71) -> 94
        , ok_5(72) -> 53
        , ok_6(73) -> 68
        , ok_6(73) -> 88
        , ok_6(74) -> 49
        , ok_6(78) -> 65
        , ok_6(97) -> 86
        , ok_6(98) -> 96
        , ok_6(100) -> 99
        , ok_7(79) -> 61
        , ok_7(83) -> 87
        , ok_7(101) -> 95
        , ok_7(102) -> 92
        , ok_7(103) -> 80
        , ok_8(104) -> 93
        , ok_8(106) -> 90
        , top_0(2) -> 14
        , top_0(3) -> 14
        , top_0(5) -> 14
        , top_0(7) -> 14
        , top_0(8) -> 14
        , top_0(13) -> 14
        , top_1(25) -> 14
        , top_2(26) -> 14
        , top_3(38) -> 14
        , top_4(49) -> 14
        , top_5(61) -> 14
        , top_6(80) -> 14
        , top_7(90) -> 14
        , top_8(107) -> 14}

Tool RC1

Execution Time	Unknown
Answer	MAYBE
Input	Transformed CSR 04 Ex1 Luc04b C

stdout:

MAYBE

Tool RC2

Execution Time	Unknown
Answer	YES(?,O(n^1))
Input	Transformed CSR 04 Ex1 Luc04b 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(nats()) -> mark(cons(0(), incr(nats())))
     , active(pairs()) -> mark(cons(0(), incr(odds())))
     , active(odds()) -> mark(incr(pairs()))
     , active(incr(cons(X, XS))) -> mark(cons(s(X), incr(XS)))
     , active(head(cons(X, XS))) -> mark(X)
     , active(tail(cons(X, XS))) -> mark(XS)
     , active(cons(X1, X2)) -> cons(active(X1), X2)
     , active(incr(X)) -> incr(active(X))
     , active(s(X)) -> s(active(X))
     , active(head(X)) -> head(active(X))
     , active(tail(X)) -> tail(active(X))
     , cons(mark(X1), X2) -> mark(cons(X1, X2))
     , incr(mark(X)) -> mark(incr(X))
     , s(mark(X)) -> mark(s(X))
     , head(mark(X)) -> mark(head(X))
     , tail(mark(X)) -> mark(tail(X))
     , proper(nats()) -> ok(nats())
     , proper(cons(X1, X2)) -> cons(proper(X1), proper(X2))
     , proper(0()) -> ok(0())
     , proper(incr(X)) -> incr(proper(X))
     , proper(pairs()) -> ok(pairs())
     , proper(odds()) -> ok(odds())
     , proper(s(X)) -> s(proper(X))
     , proper(head(X)) -> head(proper(X))
     , proper(tail(X)) -> tail(proper(X))
     , cons(ok(X1), ok(X2)) -> ok(cons(X1, X2))
     , incr(ok(X)) -> ok(incr(X))
     , s(ok(X)) -> ok(s(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(nats()) -> mark(cons(0(), incr(nats())))
          , active(pairs()) -> mark(cons(0(), incr(odds())))
          , active(odds()) -> mark(incr(pairs()))
          , active(incr(cons(X, XS))) -> mark(cons(s(X), incr(XS)))
          , active(head(cons(X, XS))) -> mark(X)
          , active(tail(cons(X, XS))) -> mark(XS)
          , active(cons(X1, X2)) -> cons(active(X1), X2)
          , active(incr(X)) -> incr(active(X))
          , active(s(X)) -> s(active(X))
          , active(head(X)) -> head(active(X))
          , active(tail(X)) -> tail(active(X))
          , cons(mark(X1), X2) -> mark(cons(X1, X2))
          , incr(mark(X)) -> mark(incr(X))
          , s(mark(X)) -> mark(s(X))
          , head(mark(X)) -> mark(head(X))
          , tail(mark(X)) -> mark(tail(X))
          , proper(nats()) -> ok(nats())
          , proper(cons(X1, X2)) -> cons(proper(X1), proper(X2))
          , proper(0()) -> ok(0())
          , proper(incr(X)) -> incr(proper(X))
          , proper(pairs()) -> ok(pairs())
          , proper(odds()) -> ok(odds())
          , proper(s(X)) -> s(proper(X))
          , proper(head(X)) -> head(proper(X))
          , proper(tail(X)) -> tail(proper(X))
          , cons(ok(X1), ok(X2)) -> ok(cons(X1, X2))
          , incr(ok(X)) -> ok(incr(X))
          , s(ok(X)) -> ok(s(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 9.
       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(8) -> 1
        , active_0(13) -> 1
        , active_1(2) -> 25
        , active_1(3) -> 25
        , active_1(5) -> 25
        , active_1(7) -> 25
        , active_1(8) -> 25
        , active_1(13) -> 25
        , active_2(16) -> 26
        , active_2(18) -> 26
        , active_2(19) -> 26
        , active_3(37) -> 38
        , active_4(28) -> 52
        , active_4(31) -> 39
        , active_4(47) -> 49
        , active_5(42) -> 59
        , active_5(45) -> 53
        , active_5(74) -> 61
        , active_6(56) -> 84
        , active_6(72) -> 65
        , active_6(79) -> 80
        , active_7(69) -> 91
        , active_7(78) -> 85
        , active_7(103) -> 90
        , active_8(97) -> 105
        , active_8(98) -> 109
        , active_8(106) -> 107
        , active_9(102) -> 108
        , nats_0() -> 2
        , nats_1() -> 18
        , nats_2() -> 30
        , nats_3() -> 46
        , nats_4() -> 58
        , nats_5() -> 71
        , nats_6() -> 100
        , mark_0(2) -> 3
        , mark_0(3) -> 3
        , mark_0(5) -> 3
        , mark_0(7) -> 3
        , mark_0(8) -> 3
        , mark_0(13) -> 3
        , mark_1(15) -> 1
        , mark_1(15) -> 25
        , mark_1(20) -> 4
        , mark_1(20) -> 20
        , mark_1(21) -> 6
        , mark_1(21) -> 21
        , mark_1(22) -> 9
        , mark_1(22) -> 22
        , mark_1(23) -> 10
        , mark_1(23) -> 23
        , mark_1(24) -> 11
        , mark_1(24) -> 24
        , mark_2(27) -> 26
        , mark_3(50) -> 39
        , mark_4(54) -> 38
        , mark_4(55) -> 53
        , mark_5(60) -> 49
        , mark_6(75) -> 61
        , mark_7(81) -> 80
        , cons_0(2, 2) -> 4
        , cons_0(2, 3) -> 4
        , cons_0(2, 5) -> 4
        , cons_0(2, 7) -> 4
        , cons_0(2, 8) -> 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, 8) -> 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, 8) -> 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, 8) -> 4
        , cons_0(7, 13) -> 4
        , cons_0(8, 2) -> 4
        , cons_0(8, 3) -> 4
        , cons_0(8, 5) -> 4
        , cons_0(8, 7) -> 4
        , cons_0(8, 8) -> 4
        , cons_0(8, 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, 8) -> 4
        , cons_0(13, 13) -> 4
        , cons_1(2, 2) -> 20
        , cons_1(2, 3) -> 20
        , cons_1(2, 5) -> 20
        , cons_1(2, 7) -> 20
        , cons_1(2, 8) -> 20
        , cons_1(2, 13) -> 20
        , cons_1(3, 2) -> 20
        , cons_1(3, 3) -> 20
        , cons_1(3, 5) -> 20
        , cons_1(3, 7) -> 20
        , cons_1(3, 8) -> 20
        , cons_1(3, 13) -> 20
        , cons_1(5, 2) -> 20
        , cons_1(5, 3) -> 20
        , cons_1(5, 5) -> 20
        , cons_1(5, 7) -> 20
        , cons_1(5, 8) -> 20
        , cons_1(5, 13) -> 20
        , cons_1(7, 2) -> 20
        , cons_1(7, 3) -> 20
        , cons_1(7, 5) -> 20
        , cons_1(7, 7) -> 20
        , cons_1(7, 8) -> 20
        , cons_1(7, 13) -> 20
        , cons_1(8, 2) -> 20
        , cons_1(8, 3) -> 20
        , cons_1(8, 5) -> 20
        , cons_1(8, 7) -> 20
        , cons_1(8, 8) -> 20
        , cons_1(8, 13) -> 20
        , cons_1(13, 2) -> 20
        , cons_1(13, 3) -> 20
        , cons_1(13, 5) -> 20
        , cons_1(13, 7) -> 20
        , cons_1(13, 8) -> 20
        , cons_1(13, 13) -> 20
        , cons_1(16, 17) -> 15
        , cons_2(28, 29) -> 27
        , cons_2(32, 33) -> 26
        , cons_3(28, 36) -> 37
        , cons_3(40, 41) -> 38
        , cons_3(42, 51) -> 50
        , cons_4(42, 48) -> 47
        , cons_4(52, 36) -> 38
        , cons_4(56, 57) -> 55
        , cons_4(62, 63) -> 53
        , cons_5(56, 66) -> 72
        , cons_5(59, 48) -> 49
        , cons_5(67, 68) -> 65
        , cons_6(69, 73) -> 78
        , cons_6(76, 77) -> 75
        , cons_6(84, 66) -> 65
        , cons_7(82, 83) -> 81
        , cons_7(86, 87) -> 80
        , cons_7(91, 73) -> 85
        , cons_7(97, 83) -> 103
        , cons_8(92, 93) -> 90
        , cons_8(102, 104) -> 106
        , cons_8(105, 83) -> 90
        , cons_9(108, 104) -> 107
        , 0_0() -> 5
        , 0_1() -> 16
        , 0_2() -> 28
        , 0_3() -> 42
        , 0_4() -> 56
        , 0_5() -> 69
        , 0_6() -> 98
        , incr_0(2) -> 6
        , incr_0(3) -> 6
        , incr_0(5) -> 6
        , incr_0(7) -> 6
        , incr_0(8) -> 6
        , incr_0(13) -> 6
        , incr_1(2) -> 21
        , incr_1(3) -> 21
        , incr_1(5) -> 21
        , incr_1(7) -> 21
        , incr_1(8) -> 21
        , incr_1(13) -> 21
        , incr_1(18) -> 17
        , incr_1(19) -> 15
        , incr_2(30) -> 29
        , incr_2(31) -> 27
        , incr_2(34) -> 33
        , incr_2(35) -> 26
        , incr_3(30) -> 36
        , incr_3(31) -> 37
        , incr_3(43) -> 41
        , incr_3(44) -> 38
        , incr_3(46) -> 51
        , incr_4(39) -> 38
        , incr_4(45) -> 47
        , incr_4(46) -> 48
        , incr_4(50) -> 54
        , incr_4(58) -> 57
        , incr_4(64) -> 63
        , incr_5(53) -> 49
        , incr_5(55) -> 60
        , incr_5(58) -> 66
        , incr_5(70) -> 68
        , incr_6(65) -> 61
        , incr_6(66) -> 77
        , incr_6(71) -> 73
        , incr_6(72) -> 74
        , incr_6(94) -> 88
        , incr_7(73) -> 83
        , incr_7(78) -> 79
        , incr_7(85) -> 80
        , incr_7(88) -> 87
        , incr_7(99) -> 95
        , incr_7(100) -> 101
        , incr_8(95) -> 93
        , incr_8(101) -> 104
        , pairs_0() -> 7
        , pairs_1() -> 19
        , pairs_2() -> 31
        , pairs_3() -> 45
        , odds_0() -> 8
        , odds_1() -> 18
        , odds_2() -> 30
        , odds_3() -> 46
        , odds_4() -> 58
        , odds_5() -> 71
        , odds_6() -> 100
        , s_0(2) -> 9
        , s_0(3) -> 9
        , s_0(5) -> 9
        , s_0(7) -> 9
        , s_0(8) -> 9
        , s_0(13) -> 9
        , s_1(2) -> 22
        , s_1(3) -> 22
        , s_1(5) -> 22
        , s_1(7) -> 22
        , s_1(8) -> 22
        , s_1(13) -> 22
        , s_6(56) -> 76
        , s_6(69) -> 97
        , s_7(69) -> 82
        , s_7(89) -> 86
        , s_7(91) -> 105
        , s_7(98) -> 102
        , s_8(96) -> 92
        , s_8(109) -> 108
        , head_0(2) -> 10
        , head_0(3) -> 10
        , head_0(5) -> 10
        , head_0(7) -> 10
        , head_0(8) -> 10
        , head_0(13) -> 10
        , head_1(2) -> 23
        , head_1(3) -> 23
        , head_1(5) -> 23
        , head_1(7) -> 23
        , head_1(8) -> 23
        , head_1(13) -> 23
        , tail_0(2) -> 11
        , tail_0(3) -> 11
        , tail_0(5) -> 11
        , tail_0(7) -> 11
        , tail_0(8) -> 11
        , tail_0(13) -> 11
        , tail_1(2) -> 24
        , tail_1(3) -> 24
        , tail_1(5) -> 24
        , tail_1(7) -> 24
        , tail_1(8) -> 24
        , tail_1(13) -> 24
        , proper_0(2) -> 12
        , proper_0(3) -> 12
        , proper_0(5) -> 12
        , proper_0(7) -> 12
        , proper_0(8) -> 12
        , proper_0(13) -> 12
        , proper_1(2) -> 25
        , proper_1(3) -> 25
        , proper_1(5) -> 25
        , proper_1(7) -> 25
        , proper_1(8) -> 25
        , proper_1(13) -> 25
        , proper_2(15) -> 26
        , proper_2(16) -> 32
        , proper_2(17) -> 33
        , proper_2(18) -> 34
        , proper_2(19) -> 35
        , proper_3(27) -> 38
        , proper_3(28) -> 40
        , proper_3(29) -> 41
        , proper_3(30) -> 43
        , proper_3(31) -> 44
        , proper_4(42) -> 62
        , proper_4(46) -> 64
        , proper_4(51) -> 63
        , proper_4(54) -> 49
        , proper_5(50) -> 53
        , proper_5(56) -> 67
        , proper_5(57) -> 68
        , proper_5(58) -> 70
        , proper_5(60) -> 61
        , proper_6(55) -> 65
        , proper_6(58) -> 94
        , proper_6(75) -> 80
        , proper_7(56) -> 89
        , proper_7(66) -> 88
        , proper_7(71) -> 99
        , proper_7(76) -> 86
        , proper_7(77) -> 87
        , proper_7(81) -> 90
        , proper_8(69) -> 96
        , proper_8(73) -> 95
        , proper_8(82) -> 92
        , proper_8(83) -> 93
        , ok_0(2) -> 13
        , ok_0(3) -> 13
        , ok_0(5) -> 13
        , ok_0(7) -> 13
        , ok_0(8) -> 13
        , ok_0(13) -> 13
        , ok_1(16) -> 12
        , ok_1(16) -> 25
        , ok_1(18) -> 12
        , ok_1(18) -> 25
        , ok_1(19) -> 12
        , ok_1(19) -> 25
        , ok_1(20) -> 4
        , ok_1(20) -> 20
        , ok_1(21) -> 6
        , ok_1(21) -> 21
        , ok_1(22) -> 9
        , ok_1(22) -> 22
        , ok_1(23) -> 10
        , ok_1(23) -> 23
        , ok_1(24) -> 11
        , ok_1(24) -> 24
        , ok_2(28) -> 32
        , ok_2(30) -> 34
        , ok_2(31) -> 35
        , ok_3(36) -> 33
        , ok_3(37) -> 26
        , ok_3(42) -> 40
        , ok_3(45) -> 44
        , ok_3(46) -> 43
        , ok_4(47) -> 38
        , ok_4(48) -> 41
        , ok_4(56) -> 62
        , ok_4(58) -> 64
        , ok_5(66) -> 63
        , ok_5(69) -> 67
        , ok_5(69) -> 89
        , ok_5(71) -> 70
        , ok_5(71) -> 94
        , ok_5(72) -> 53
        , ok_6(73) -> 68
        , ok_6(73) -> 88
        , ok_6(74) -> 49
        , ok_6(78) -> 65
        , ok_6(97) -> 86
        , ok_6(98) -> 96
        , ok_6(100) -> 99
        , ok_7(79) -> 61
        , ok_7(83) -> 87
        , ok_7(101) -> 95
        , ok_7(102) -> 92
        , ok_7(103) -> 80
        , ok_8(104) -> 93
        , ok_8(106) -> 90
        , top_0(2) -> 14
        , top_0(3) -> 14
        , top_0(5) -> 14
        , top_0(7) -> 14
        , top_0(8) -> 14
        , top_0(13) -> 14
        , top_1(25) -> 14
        , top_2(26) -> 14
        , top_3(38) -> 14
        , top_4(49) -> 14
        , top_5(61) -> 14
        , top_6(80) -> 14
        , top_7(90) -> 14
        , top_8(107) -> 14}