Problem Transformed CSR 04 ExIntrod GM04 C

Tool CaT

Execution TimeUnknown
Answer
YES(?,O(n^1))
InputTransformed CSR 04 ExIntrod GM04 C

stdout:

YES(?,O(n^1))

Problem:
 active(nats()) -> mark(adx(zeros()))
 active(zeros()) -> mark(cons(0(),zeros()))
 active(incr(cons(X,Y))) -> mark(cons(s(X),incr(Y)))
 active(adx(cons(X,Y))) -> mark(incr(cons(X,adx(Y))))
 active(hd(cons(X,Y))) -> mark(X)
 active(tl(cons(X,Y))) -> mark(Y)
 active(adx(X)) -> adx(active(X))
 active(incr(X)) -> incr(active(X))
 active(hd(X)) -> hd(active(X))
 active(tl(X)) -> tl(active(X))
 adx(mark(X)) -> mark(adx(X))
 incr(mark(X)) -> mark(incr(X))
 hd(mark(X)) -> mark(hd(X))
 tl(mark(X)) -> mark(tl(X))
 proper(nats()) -> ok(nats())
 proper(adx(X)) -> adx(proper(X))
 proper(zeros()) -> ok(zeros())
 proper(cons(X1,X2)) -> cons(proper(X1),proper(X2))
 proper(0()) -> ok(0())
 proper(incr(X)) -> incr(proper(X))
 proper(s(X)) -> s(proper(X))
 proper(hd(X)) -> hd(proper(X))
 proper(tl(X)) -> tl(proper(X))
 adx(ok(X)) -> ok(adx(X))
 cons(ok(X1),ok(X2)) -> ok(cons(X1,X2))
 incr(ok(X)) -> ok(incr(X))
 s(ok(X)) -> ok(s(X))
 hd(ok(X)) -> ok(hd(X))
 tl(ok(X)) -> ok(tl(X))
 top(mark(X)) -> top(proper(X))
 top(ok(X)) -> top(active(X))

Proof:
 Bounds Processor:
  bound: 10
  enrichment: match
  automaton:
   final states: {14,13,12,11,10,9,8,7,6}
   transitions:
    ok9(204) -> 181*
    ok9(206) -> 177*
    03() -> 60*
    top10(207) -> 14*
    zeros3() -> 57*
    active10(206) -> 207*
    ok4(74) -> 82*
    ok4(73) -> 81*
    ok4(63) -> 50*
    cons4(60,57) -> 63*
    cons4(82,81) -> 69*
    cons4(74,73) -> 75*
    adx4(65) -> 72*
    adx4(62) -> 50*
    adx4(57) -> 63*
    active4(41) -> 62*
    active4(63) -> 68*
    top4(68) -> 14*
    mark3(65) -> 62*
    mark4(75) -> 69*
    mark4(72) -> 50*
    adx5(75) -> 79*
    adx5(69) -> 68*
    active5(100) -> 86*
    active5(57) -> 69*
    proper4(60) -> 82*
    proper4(72) -> 68*
    proper4(57) -> 81*
    04() -> 74*
    zeros4() -> 73*
    proper5(65) -> 69*
    proper5(79) -> 86*
    proper5(74) -> 92*
    proper5(73) -> 91*
    active0(5) -> 6*
    active0(2) -> 6*
    active0(4) -> 6*
    active0(1) -> 6*
    active0(3) -> 6*
    mark5(79) -> 68*
    nats0() -> 1*
    top5(86) -> 14*
    mark0(5) -> 2*
    mark0(2) -> 2*
    mark0(4) -> 2*
    mark0(1) -> 2*
    mark0(3) -> 2*
    adx6(87) -> 86*
    adx6(96) -> 142*
    adx6(93) -> 100*
    adx6(73) -> 103*
    adx0(5) -> 7*
    adx0(2) -> 7*
    adx0(4) -> 7*
    adx0(1) -> 7*
    adx0(3) -> 7*
    proper6(105) -> 112*
    proper6(75) -> 87*
    zeros0() -> 3*
    ok5(97) -> 124,92
    ok5(96) -> 129,91
    ok5(93) -> 69*
    cons0(3,1) -> 12*
    cons0(3,3) -> 12*
    cons0(3,5) -> 12*
    cons0(4,2) -> 12*
    cons0(4,4) -> 12*
    cons0(5,1) -> 12*
    cons0(5,3) -> 12*
    cons0(5,5) -> 12*
    cons0(1,2) -> 12*
    cons0(1,4) -> 12*
    cons0(2,1) -> 12*
    cons0(2,3) -> 12*
    cons0(2,5) -> 12*
    cons0(3,2) -> 12*
    cons0(3,4) -> 12*
    cons0(4,1) -> 12*
    cons0(4,3) -> 12*
    cons0(4,5) -> 12*
    cons0(5,2) -> 12*
    cons0(5,4) -> 12*
    cons0(1,1) -> 12*
    cons0(1,3) -> 12*
    cons0(1,5) -> 12*
    cons0(2,2) -> 12*
    cons0(2,4) -> 12*
    cons5(74,73) -> 93*
    cons5(92,91) -> 87*
    00() -> 4*
    ok6(100) -> 68*
    ok6(142) -> 123*
    ok6(139) -> 134*
    ok6(146) -> 122*
    ok6(101) -> 87*
    ok6(143) -> 180,138
    incr0(5) -> 8*
    incr0(2) -> 8*
    incr0(4) -> 8*
    incr0(1) -> 8*
    incr0(3) -> 8*
    05() -> 97*
    s0(5) -> 13*
    s0(2) -> 13*
    s0(4) -> 13*
    s0(1) -> 13*
    s0(3) -> 13*
    zeros5() -> 96*
    hd0(5) -> 9*
    hd0(2) -> 9*
    hd0(4) -> 9*
    hd0(1) -> 9*
    hd0(3) -> 9*
    cons6(74,103) -> 104*
    cons6(97,96) -> 101*
    cons6(97,142) -> 146*
    tl0(5) -> 10*
    tl0(2) -> 10*
    tl0(4) -> 10*
    tl0(1) -> 10*
    tl0(3) -> 10*
    ok7(150) -> 112*
    ok7(147) -> 175,133
    ok7(109) -> 86*
    ok7(186) -> 174*
    ok7(151) -> 131*
    ok7(193) -> 189*
    ok7(195) -> 192*
    proper0(5) -> 11*
    proper0(2) -> 11*
    proper0(4) -> 11*
    proper0(1) -> 11*
    proper0(3) -> 11*
    adx7(129) -> 123*
    adx7(119) -> 112*
    adx7(101) -> 109*
    adx7(96) -> 116*
    adx7(143) -> 147*
    adx7(180) -> 175*
    ok0(5) -> 5*
    ok0(2) -> 5*
    ok0(4) -> 5*
    ok0(1) -> 5*
    ok0(3) -> 5*
    active6(109) -> 112*
    active6(93) -> 87*
    top0(5) -> 14*
    top0(2) -> 14*
    top0(4) -> 14*
    top0(1) -> 14*
    top0(3) -> 14*
    mark6(105) -> 86*
    top1(36) -> 14*
    incr6(104) -> 105*
    active1(5) -> 36*
    active1(2) -> 36*
    active1(4) -> 36*
    active1(1) -> 36*
    active1(3) -> 36*
    top6(112) -> 14*
    proper1(5) -> 36*
    proper1(2) -> 36*
    proper1(4) -> 36*
    proper1(1) -> 36*
    proper1(3) -> 36*
    incr7(142) -> 153*
    incr7(122) -> 112*
    incr7(117) -> 118*
    incr7(146) -> 150*
    ok1(25) -> 25,9
    ok1(20) -> 36,11
    ok1(15) -> 36,11
    ok1(29) -> 36,11
    ok1(24) -> 24,8
    ok1(31) -> 31,12
    ok1(21) -> 21,7
    ok1(33) -> 33,13
    ok1(28) -> 28,10
    proper7(104) -> 122*
    proper7(74) -> 124*
    proper7(96) -> 180*
    proper7(118) -> 128*
    proper7(103) -> 123*
    proper7(73) -> 129*
    tl1(5) -> 28*
    tl1(2) -> 28*
    tl1(4) -> 28*
    tl1(1) -> 28*
    tl1(3) -> 28*
    active7(150) -> 128*
    active7(101) -> 119*
    hd1(5) -> 25*
    hd1(2) -> 25*
    hd1(4) -> 25*
    hd1(1) -> 25*
    hd1(3) -> 25*
    mark7(155) -> 128*
    mark7(118) -> 112*
    s1(5) -> 33*
    s1(2) -> 33*
    s1(4) -> 33*
    s1(1) -> 33*
    s1(3) -> 33*
    cons7(124,123) -> 122*
    cons7(139,147) -> 151*
    cons7(154,153) -> 155*
    cons7(97,116) -> 117*
    incr1(5) -> 24*
    incr1(2) -> 24*
    incr1(4) -> 24*
    incr1(1) -> 24*
    incr1(3) -> 24*
    top7(128) -> 14*
    cons1(3,1) -> 31*
    cons1(3,3) -> 31*
    cons1(3,5) -> 31*
    cons1(4,2) -> 31*
    cons1(4,4) -> 31*
    cons1(5,1) -> 31*
    cons1(5,3) -> 31*
    cons1(5,5) -> 31*
    cons1(20,15) -> 16*
    cons1(1,2) -> 31*
    cons1(1,4) -> 31*
    cons1(2,1) -> 31*
    cons1(2,3) -> 31*
    cons1(2,5) -> 31*
    cons1(3,2) -> 31*
    cons1(3,4) -> 31*
    cons1(4,1) -> 31*
    cons1(4,3) -> 31*
    cons1(4,5) -> 31*
    cons1(5,2) -> 31*
    cons1(5,4) -> 31*
    cons1(1,1) -> 31*
    cons1(1,3) -> 31*
    cons1(1,5) -> 31*
    cons1(2,2) -> 31*
    cons1(2,4) -> 31*
    incr8(147) -> 166*
    incr8(151) -> 159*
    incr8(131) -> 128*
    incr8(175) -> 173*
    adx1(15) -> 16*
    adx1(5) -> 21*
    adx1(2) -> 21*
    adx1(4) -> 21*
    adx1(1) -> 21*
    adx1(3) -> 21*
    proper8(155) -> 162*
    proper8(142) -> 175*
    proper8(117) -> 131*
    proper8(97) -> 134*
    proper8(154) -> 174*
    proper8(116) -> 133*
    proper8(96) -> 138*
    proper8(153) -> 173*
    proper8(143) -> 192*
    01() -> 20*
    cons8(186,166) -> 201*
    cons8(134,133) -> 131*
    cons8(174,173) -> 162*
    cons8(167,166) -> 168*
    zeros1() -> 15*
    06() -> 139*
    nats1() -> 29*
    adx8(192) -> 188*
    adx8(138) -> 133*
    adx8(195) -> 200*
    mark1(25) -> 25,9
    mark1(24) -> 24,8
    mark1(21) -> 21,7
    mark1(16) -> 36,6
    mark1(28) -> 28,10
    zeros6() -> 143*
    top2(38) -> 14*
    ok8(197) -> 182*
    ok8(159) -> 128*
    ok8(201) -> 162*
    ok8(166) -> 173*
    ok8(200) -> 188*
    active2(20) -> 38*
    active2(15) -> 38*
    active2(29) -> 38*
    active8(159) -> 162*
    active8(146) -> 131*
    proper2(20) -> 47*
    proper2(15) -> 46*
    proper2(16) -> 38*
    s7(97) -> 154*
    s7(139) -> 186*
    cons2(47,46) -> 38*
    cons2(43,41) -> 42*
    top8(162) -> 14*
    adx2(46) -> 38*
    adx2(41) -> 42*
    incr9(169) -> 162*
    incr9(188) -> 181*
    incr9(200) -> 204*
    mark2(42) -> 38*
    active9(201) -> 177*
    active9(151) -> 169*
    02() -> 43*
    mark8(168) -> 162*
    zeros2() -> 41*
    s8(139) -> 167*
    s8(134) -> 174*
    s8(193) -> 197*
    top3(50) -> 14*
    top9(177) -> 14*
    proper3(42) -> 50*
    proper3(41) -> 51*
    proper3(43) -> 54*
    proper9(167) -> 182*
    proper9(147) -> 188*
    proper9(139) -> 189*
    proper9(166) -> 181*
    proper9(168) -> 177*
    ok2(41) -> 46*
    ok2(43) -> 47*
    cons9(197,204) -> 206*
    cons9(182,181) -> 177*
    ok3(60) -> 54*
    ok3(55) -> 38*
    ok3(57) -> 51*
    s9(189) -> 182*
    cons3(43,41) -> 55*
    cons3(60,57) -> 65*
    cons3(54,51) -> 50*
    07() -> 193*
    adx3(51) -> 50*
    adx3(41) -> 55*
    zeros7() -> 195*
    active3(55) -> 50*
  problem:
   
  Qed

Tool IRC1

Execution TimeUnknown
Answer
MAYBE
InputTransformed CSR 04 ExIntrod GM04 C

stdout:

MAYBE

Tool IRC2

Execution TimeUnknown
Answer
YES(?,O(n^1))
InputTransformed CSR 04 ExIntrod GM04 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(adx(zeros()))
     , active(zeros()) -> mark(cons(0(), zeros()))
     , active(incr(cons(X, Y))) -> mark(cons(s(X), incr(Y)))
     , active(adx(cons(X, Y))) -> mark(incr(cons(X, adx(Y))))
     , active(hd(cons(X, Y))) -> mark(X)
     , active(tl(cons(X, Y))) -> mark(Y)
     , active(adx(X)) -> adx(active(X))
     , active(incr(X)) -> incr(active(X))
     , active(hd(X)) -> hd(active(X))
     , active(tl(X)) -> tl(active(X))
     , adx(mark(X)) -> mark(adx(X))
     , incr(mark(X)) -> mark(incr(X))
     , hd(mark(X)) -> mark(hd(X))
     , tl(mark(X)) -> mark(tl(X))
     , proper(nats()) -> ok(nats())
     , proper(adx(X)) -> adx(proper(X))
     , proper(zeros()) -> ok(zeros())
     , proper(cons(X1, X2)) -> cons(proper(X1), proper(X2))
     , proper(0()) -> ok(0())
     , proper(incr(X)) -> incr(proper(X))
     , proper(s(X)) -> s(proper(X))
     , proper(hd(X)) -> hd(proper(X))
     , proper(tl(X)) -> tl(proper(X))
     , adx(ok(X)) -> ok(adx(X))
     , cons(ok(X1), ok(X2)) -> ok(cons(X1, X2))
     , incr(ok(X)) -> ok(incr(X))
     , s(ok(X)) -> ok(s(X))
     , hd(ok(X)) -> ok(hd(X))
     , tl(ok(X)) -> ok(tl(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(adx(zeros()))
          , active(zeros()) -> mark(cons(0(), zeros()))
          , active(incr(cons(X, Y))) -> mark(cons(s(X), incr(Y)))
          , active(adx(cons(X, Y))) -> mark(incr(cons(X, adx(Y))))
          , active(hd(cons(X, Y))) -> mark(X)
          , active(tl(cons(X, Y))) -> mark(Y)
          , active(adx(X)) -> adx(active(X))
          , active(incr(X)) -> incr(active(X))
          , active(hd(X)) -> hd(active(X))
          , active(tl(X)) -> tl(active(X))
          , adx(mark(X)) -> mark(adx(X))
          , incr(mark(X)) -> mark(incr(X))
          , hd(mark(X)) -> mark(hd(X))
          , tl(mark(X)) -> mark(tl(X))
          , proper(nats()) -> ok(nats())
          , proper(adx(X)) -> adx(proper(X))
          , proper(zeros()) -> ok(zeros())
          , proper(cons(X1, X2)) -> cons(proper(X1), proper(X2))
          , proper(0()) -> ok(0())
          , proper(incr(X)) -> incr(proper(X))
          , proper(s(X)) -> s(proper(X))
          , proper(hd(X)) -> hd(proper(X))
          , proper(tl(X)) -> tl(proper(X))
          , adx(ok(X)) -> ok(adx(X))
          , cons(ok(X1), ok(X2)) -> ok(cons(X1, X2))
          , incr(ok(X)) -> ok(incr(X))
          , s(ok(X)) -> ok(s(X))
          , hd(ok(X)) -> ok(hd(X))
          , tl(ok(X)) -> ok(tl(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(2) -> 1
        , active_0(3) -> 1
        , active_0(5) -> 1
        , active_0(7) -> 1
        , active_0(13) -> 1
        , active_1(2) -> 25
        , active_1(3) -> 25
        , active_1(5) -> 25
        , active_1(7) -> 25
        , active_1(13) -> 25
        , active_2(16) -> 26
        , active_2(17) -> 26
        , active_2(22) -> 26
        , active_3(32) -> 33
        , active_4(28) -> 34
        , active_4(39) -> 40
        , active_5(36) -> 42
        , active_5(57) -> 50
        , active_6(55) -> 51
        , active_6(62) -> 63
        , active_7(58) -> 67
        , active_7(79) -> 69
        , active_8(78) -> 72
        , active_8(87) -> 88
        , active_9(86) -> 92
        , active_9(107) -> 97
        , active_10(110) -> 111
        , nats_0() -> 2
        , nats_1() -> 22
        , mark_0(2) -> 3
        , mark_0(3) -> 3
        , mark_0(5) -> 3
        , mark_0(7) -> 3
        , mark_0(13) -> 3
        , mark_1(15) -> 1
        , mark_1(15) -> 25
        , mark_1(18) -> 4
        , mark_1(18) -> 18
        , mark_1(19) -> 8
        , mark_1(19) -> 19
        , mark_1(20) -> 10
        , mark_1(20) -> 20
        , mark_1(21) -> 11
        , mark_1(21) -> 21
        , mark_2(27) -> 26
        , mark_3(41) -> 34
        , mark_4(43) -> 33
        , mark_4(44) -> 42
        , mark_5(47) -> 40
        , mark_6(59) -> 50
        , mark_7(64) -> 63
        , mark_7(80) -> 69
        , mark_8(89) -> 88
        , adx_0(2) -> 4
        , adx_0(3) -> 4
        , adx_0(5) -> 4
        , adx_0(7) -> 4
        , adx_0(13) -> 4
        , adx_1(2) -> 18
        , adx_1(3) -> 18
        , adx_1(5) -> 18
        , adx_1(7) -> 18
        , adx_1(13) -> 18
        , adx_1(16) -> 15
        , adx_2(28) -> 27
        , adx_2(30) -> 26
        , adx_3(28) -> 32
        , adx_3(35) -> 33
        , adx_4(34) -> 33
        , adx_4(36) -> 39
        , adx_4(41) -> 43
        , adx_5(42) -> 40
        , adx_5(44) -> 47
        , adx_6(46) -> 61
        , adx_6(51) -> 50
        , adx_6(55) -> 57
        , adx_6(56) -> 77
        , adx_7(56) -> 66
        , adx_7(58) -> 62
        , adx_7(67) -> 63
        , adx_7(73) -> 71
        , adx_7(84) -> 85
        , adx_7(98) -> 95
        , adx_8(83) -> 75
        , adx_8(103) -> 101
        , adx_8(104) -> 106
        , zeros_0() -> 5
        , zeros_1() -> 16
        , zeros_2() -> 28
        , zeros_3() -> 36
        , zeros_4() -> 46
        , zeros_5() -> 56
        , zeros_6() -> 84
        , zeros_7() -> 104
        , cons_0(2, 2) -> 6
        , cons_0(2, 3) -> 6
        , cons_0(2, 5) -> 6
        , cons_0(2, 7) -> 6
        , cons_0(2, 13) -> 6
        , cons_0(3, 2) -> 6
        , cons_0(3, 3) -> 6
        , cons_0(3, 5) -> 6
        , cons_0(3, 7) -> 6
        , cons_0(3, 13) -> 6
        , cons_0(5, 2) -> 6
        , cons_0(5, 3) -> 6
        , cons_0(5, 5) -> 6
        , cons_0(5, 7) -> 6
        , cons_0(5, 13) -> 6
        , cons_0(7, 2) -> 6
        , cons_0(7, 3) -> 6
        , cons_0(7, 5) -> 6
        , cons_0(7, 7) -> 6
        , cons_0(7, 13) -> 6
        , cons_0(13, 2) -> 6
        , cons_0(13, 3) -> 6
        , cons_0(13, 5) -> 6
        , cons_0(13, 7) -> 6
        , cons_0(13, 13) -> 6
        , cons_1(2, 2) -> 23
        , cons_1(2, 3) -> 23
        , cons_1(2, 5) -> 23
        , cons_1(2, 7) -> 23
        , cons_1(2, 13) -> 23
        , cons_1(3, 2) -> 23
        , cons_1(3, 3) -> 23
        , cons_1(3, 5) -> 23
        , cons_1(3, 7) -> 23
        , cons_1(3, 13) -> 23
        , cons_1(5, 2) -> 23
        , cons_1(5, 3) -> 23
        , cons_1(5, 5) -> 23
        , cons_1(5, 7) -> 23
        , cons_1(5, 13) -> 23
        , cons_1(7, 2) -> 23
        , cons_1(7, 3) -> 23
        , cons_1(7, 5) -> 23
        , cons_1(7, 7) -> 23
        , cons_1(7, 13) -> 23
        , cons_1(13, 2) -> 23
        , cons_1(13, 3) -> 23
        , cons_1(13, 5) -> 23
        , cons_1(13, 7) -> 23
        , cons_1(13, 13) -> 23
        , cons_1(17, 16) -> 15
        , cons_2(29, 28) -> 27
        , cons_2(31, 30) -> 26
        , cons_3(29, 28) -> 32
        , cons_3(37, 35) -> 33
        , cons_3(38, 36) -> 41
        , cons_4(38, 36) -> 39
        , cons_4(45, 46) -> 44
        , cons_4(48, 49) -> 42
        , cons_5(45, 46) -> 55
        , cons_5(52, 53) -> 51
        , cons_6(45, 61) -> 60
        , cons_6(54, 56) -> 58
        , cons_6(54, 77) -> 78
        , cons_7(54, 66) -> 65
        , cons_7(70, 71) -> 68
        , cons_7(76, 85) -> 86
        , cons_7(81, 82) -> 80
        , cons_8(74, 75) -> 72
        , cons_8(90, 91) -> 89
        , cons_8(93, 94) -> 88
        , cons_8(96, 91) -> 107
        , cons_9(99, 100) -> 97
        , cons_9(109, 108) -> 110
        , 0_0() -> 7
        , 0_1() -> 17
        , 0_2() -> 29
        , 0_3() -> 38
        , 0_4() -> 45
        , 0_5() -> 54
        , 0_6() -> 76
        , 0_7() -> 105
        , incr_0(2) -> 8
        , incr_0(3) -> 8
        , incr_0(5) -> 8
        , incr_0(7) -> 8
        , incr_0(13) -> 8
        , incr_1(2) -> 19
        , incr_1(3) -> 19
        , incr_1(5) -> 19
        , incr_1(7) -> 19
        , incr_1(13) -> 19
        , incr_6(60) -> 59
        , incr_7(65) -> 64
        , incr_7(68) -> 63
        , incr_7(77) -> 82
        , incr_7(78) -> 79
        , incr_8(72) -> 69
        , incr_8(85) -> 91
        , incr_8(86) -> 87
        , incr_8(95) -> 94
        , incr_9(92) -> 88
        , incr_9(101) -> 100
        , incr_9(106) -> 108
        , s_0(2) -> 9
        , s_0(3) -> 9
        , s_0(5) -> 9
        , s_0(7) -> 9
        , s_0(13) -> 9
        , s_1(2) -> 24
        , s_1(3) -> 24
        , s_1(5) -> 24
        , s_1(7) -> 24
        , s_1(13) -> 24
        , s_7(54) -> 81
        , s_7(76) -> 96
        , s_8(74) -> 93
        , s_8(76) -> 90
        , s_8(105) -> 109
        , s_9(102) -> 99
        , hd_0(2) -> 10
        , hd_0(3) -> 10
        , hd_0(5) -> 10
        , hd_0(7) -> 10
        , hd_0(13) -> 10
        , hd_1(2) -> 20
        , hd_1(3) -> 20
        , hd_1(5) -> 20
        , hd_1(7) -> 20
        , hd_1(13) -> 20
        , tl_0(2) -> 11
        , tl_0(3) -> 11
        , tl_0(5) -> 11
        , tl_0(7) -> 11
        , tl_0(13) -> 11
        , tl_1(2) -> 21
        , tl_1(3) -> 21
        , tl_1(5) -> 21
        , tl_1(7) -> 21
        , tl_1(13) -> 21
        , proper_0(2) -> 12
        , proper_0(3) -> 12
        , proper_0(5) -> 12
        , proper_0(7) -> 12
        , proper_0(13) -> 12
        , proper_1(2) -> 25
        , proper_1(3) -> 25
        , proper_1(5) -> 25
        , proper_1(7) -> 25
        , proper_1(13) -> 25
        , proper_2(15) -> 26
        , proper_2(16) -> 30
        , proper_2(17) -> 31
        , proper_3(27) -> 33
        , proper_3(28) -> 35
        , proper_3(29) -> 37
        , proper_4(36) -> 49
        , proper_4(38) -> 48
        , proper_4(43) -> 40
        , proper_5(41) -> 42
        , proper_5(45) -> 52
        , proper_5(46) -> 53
        , proper_5(47) -> 50
        , proper_6(44) -> 51
        , proper_6(59) -> 63
        , proper_7(45) -> 70
        , proper_7(46) -> 73
        , proper_7(56) -> 98
        , proper_7(60) -> 68
        , proper_7(61) -> 71
        , proper_7(64) -> 69
        , proper_8(54) -> 74
        , proper_8(56) -> 83
        , proper_8(65) -> 72
        , proper_8(66) -> 75
        , proper_8(77) -> 95
        , proper_8(80) -> 88
        , proper_8(81) -> 93
        , proper_8(82) -> 94
        , proper_8(84) -> 103
        , proper_9(76) -> 102
        , proper_9(85) -> 101
        , proper_9(89) -> 97
        , proper_9(90) -> 99
        , proper_9(91) -> 100
        , ok_0(2) -> 13
        , ok_0(3) -> 13
        , ok_0(5) -> 13
        , ok_0(7) -> 13
        , ok_0(13) -> 13
        , ok_1(16) -> 12
        , ok_1(16) -> 25
        , ok_1(17) -> 12
        , ok_1(17) -> 25
        , ok_1(18) -> 4
        , ok_1(18) -> 18
        , ok_1(19) -> 8
        , ok_1(19) -> 19
        , ok_1(20) -> 10
        , ok_1(20) -> 20
        , ok_1(21) -> 11
        , ok_1(21) -> 21
        , ok_1(22) -> 12
        , ok_1(22) -> 25
        , ok_1(23) -> 6
        , ok_1(23) -> 23
        , ok_1(24) -> 9
        , ok_1(24) -> 24
        , ok_2(28) -> 30
        , ok_2(29) -> 31
        , ok_3(32) -> 26
        , ok_3(36) -> 35
        , ok_3(38) -> 37
        , ok_4(39) -> 33
        , ok_4(45) -> 48
        , ok_4(46) -> 49
        , ok_5(54) -> 52
        , ok_5(54) -> 70
        , ok_5(55) -> 42
        , ok_5(56) -> 53
        , ok_5(56) -> 73
        , ok_6(57) -> 40
        , ok_6(58) -> 51
        , ok_6(76) -> 74
        , ok_6(77) -> 71
        , ok_6(78) -> 68
        , ok_6(84) -> 83
        , ok_6(84) -> 98
        , ok_7(62) -> 50
        , ok_7(79) -> 63
        , ok_7(85) -> 75
        , ok_7(85) -> 95
        , ok_7(86) -> 72
        , ok_7(96) -> 93
        , ok_7(104) -> 103
        , ok_7(105) -> 102
        , ok_8(87) -> 69
        , ok_8(91) -> 94
        , ok_8(106) -> 101
        , ok_8(107) -> 88
        , ok_8(109) -> 99
        , ok_9(108) -> 100
        , ok_9(110) -> 97
        , top_0(2) -> 14
        , top_0(3) -> 14
        , top_0(5) -> 14
        , top_0(7) -> 14
        , top_0(13) -> 14
        , top_1(25) -> 14
        , top_2(26) -> 14
        , top_3(33) -> 14
        , top_4(40) -> 14
        , top_5(50) -> 14
        , top_6(63) -> 14
        , top_7(69) -> 14
        , top_8(88) -> 14
        , top_9(97) -> 14
        , top_10(111) -> 14}

Tool RC1

Execution TimeUnknown
Answer
MAYBE
InputTransformed CSR 04 ExIntrod GM04 C

stdout:

MAYBE

Tool RC2

Execution TimeUnknown
Answer
YES(?,O(n^1))
InputTransformed CSR 04 ExIntrod GM04 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(adx(zeros()))
     , active(zeros()) -> mark(cons(0(), zeros()))
     , active(incr(cons(X, Y))) -> mark(cons(s(X), incr(Y)))
     , active(adx(cons(X, Y))) -> mark(incr(cons(X, adx(Y))))
     , active(hd(cons(X, Y))) -> mark(X)
     , active(tl(cons(X, Y))) -> mark(Y)
     , active(adx(X)) -> adx(active(X))
     , active(incr(X)) -> incr(active(X))
     , active(hd(X)) -> hd(active(X))
     , active(tl(X)) -> tl(active(X))
     , adx(mark(X)) -> mark(adx(X))
     , incr(mark(X)) -> mark(incr(X))
     , hd(mark(X)) -> mark(hd(X))
     , tl(mark(X)) -> mark(tl(X))
     , proper(nats()) -> ok(nats())
     , proper(adx(X)) -> adx(proper(X))
     , proper(zeros()) -> ok(zeros())
     , proper(cons(X1, X2)) -> cons(proper(X1), proper(X2))
     , proper(0()) -> ok(0())
     , proper(incr(X)) -> incr(proper(X))
     , proper(s(X)) -> s(proper(X))
     , proper(hd(X)) -> hd(proper(X))
     , proper(tl(X)) -> tl(proper(X))
     , adx(ok(X)) -> ok(adx(X))
     , cons(ok(X1), ok(X2)) -> ok(cons(X1, X2))
     , incr(ok(X)) -> ok(incr(X))
     , s(ok(X)) -> ok(s(X))
     , hd(ok(X)) -> ok(hd(X))
     , tl(ok(X)) -> ok(tl(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(adx(zeros()))
          , active(zeros()) -> mark(cons(0(), zeros()))
          , active(incr(cons(X, Y))) -> mark(cons(s(X), incr(Y)))
          , active(adx(cons(X, Y))) -> mark(incr(cons(X, adx(Y))))
          , active(hd(cons(X, Y))) -> mark(X)
          , active(tl(cons(X, Y))) -> mark(Y)
          , active(adx(X)) -> adx(active(X))
          , active(incr(X)) -> incr(active(X))
          , active(hd(X)) -> hd(active(X))
          , active(tl(X)) -> tl(active(X))
          , adx(mark(X)) -> mark(adx(X))
          , incr(mark(X)) -> mark(incr(X))
          , hd(mark(X)) -> mark(hd(X))
          , tl(mark(X)) -> mark(tl(X))
          , proper(nats()) -> ok(nats())
          , proper(adx(X)) -> adx(proper(X))
          , proper(zeros()) -> ok(zeros())
          , proper(cons(X1, X2)) -> cons(proper(X1), proper(X2))
          , proper(0()) -> ok(0())
          , proper(incr(X)) -> incr(proper(X))
          , proper(s(X)) -> s(proper(X))
          , proper(hd(X)) -> hd(proper(X))
          , proper(tl(X)) -> tl(proper(X))
          , adx(ok(X)) -> ok(adx(X))
          , cons(ok(X1), ok(X2)) -> ok(cons(X1, X2))
          , incr(ok(X)) -> ok(incr(X))
          , s(ok(X)) -> ok(s(X))
          , hd(ok(X)) -> ok(hd(X))
          , tl(ok(X)) -> ok(tl(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(2) -> 1
        , active_0(3) -> 1
        , active_0(5) -> 1
        , active_0(7) -> 1
        , active_0(13) -> 1
        , active_1(2) -> 25
        , active_1(3) -> 25
        , active_1(5) -> 25
        , active_1(7) -> 25
        , active_1(13) -> 25
        , active_2(16) -> 26
        , active_2(17) -> 26
        , active_2(22) -> 26
        , active_3(32) -> 33
        , active_4(28) -> 34
        , active_4(39) -> 40
        , active_5(36) -> 42
        , active_5(57) -> 50
        , active_6(55) -> 51
        , active_6(62) -> 63
        , active_7(58) -> 67
        , active_7(79) -> 69
        , active_8(78) -> 72
        , active_8(87) -> 88
        , active_9(86) -> 92
        , active_9(107) -> 97
        , active_10(110) -> 111
        , nats_0() -> 2
        , nats_1() -> 22
        , mark_0(2) -> 3
        , mark_0(3) -> 3
        , mark_0(5) -> 3
        , mark_0(7) -> 3
        , mark_0(13) -> 3
        , mark_1(15) -> 1
        , mark_1(15) -> 25
        , mark_1(18) -> 4
        , mark_1(18) -> 18
        , mark_1(19) -> 8
        , mark_1(19) -> 19
        , mark_1(20) -> 10
        , mark_1(20) -> 20
        , mark_1(21) -> 11
        , mark_1(21) -> 21
        , mark_2(27) -> 26
        , mark_3(41) -> 34
        , mark_4(43) -> 33
        , mark_4(44) -> 42
        , mark_5(47) -> 40
        , mark_6(59) -> 50
        , mark_7(64) -> 63
        , mark_7(80) -> 69
        , mark_8(89) -> 88
        , adx_0(2) -> 4
        , adx_0(3) -> 4
        , adx_0(5) -> 4
        , adx_0(7) -> 4
        , adx_0(13) -> 4
        , adx_1(2) -> 18
        , adx_1(3) -> 18
        , adx_1(5) -> 18
        , adx_1(7) -> 18
        , adx_1(13) -> 18
        , adx_1(16) -> 15
        , adx_2(28) -> 27
        , adx_2(30) -> 26
        , adx_3(28) -> 32
        , adx_3(35) -> 33
        , adx_4(34) -> 33
        , adx_4(36) -> 39
        , adx_4(41) -> 43
        , adx_5(42) -> 40
        , adx_5(44) -> 47
        , adx_6(46) -> 61
        , adx_6(51) -> 50
        , adx_6(55) -> 57
        , adx_6(56) -> 77
        , adx_7(56) -> 66
        , adx_7(58) -> 62
        , adx_7(67) -> 63
        , adx_7(73) -> 71
        , adx_7(84) -> 85
        , adx_7(98) -> 95
        , adx_8(83) -> 75
        , adx_8(103) -> 101
        , adx_8(104) -> 106
        , zeros_0() -> 5
        , zeros_1() -> 16
        , zeros_2() -> 28
        , zeros_3() -> 36
        , zeros_4() -> 46
        , zeros_5() -> 56
        , zeros_6() -> 84
        , zeros_7() -> 104
        , cons_0(2, 2) -> 6
        , cons_0(2, 3) -> 6
        , cons_0(2, 5) -> 6
        , cons_0(2, 7) -> 6
        , cons_0(2, 13) -> 6
        , cons_0(3, 2) -> 6
        , cons_0(3, 3) -> 6
        , cons_0(3, 5) -> 6
        , cons_0(3, 7) -> 6
        , cons_0(3, 13) -> 6
        , cons_0(5, 2) -> 6
        , cons_0(5, 3) -> 6
        , cons_0(5, 5) -> 6
        , cons_0(5, 7) -> 6
        , cons_0(5, 13) -> 6
        , cons_0(7, 2) -> 6
        , cons_0(7, 3) -> 6
        , cons_0(7, 5) -> 6
        , cons_0(7, 7) -> 6
        , cons_0(7, 13) -> 6
        , cons_0(13, 2) -> 6
        , cons_0(13, 3) -> 6
        , cons_0(13, 5) -> 6
        , cons_0(13, 7) -> 6
        , cons_0(13, 13) -> 6
        , cons_1(2, 2) -> 23
        , cons_1(2, 3) -> 23
        , cons_1(2, 5) -> 23
        , cons_1(2, 7) -> 23
        , cons_1(2, 13) -> 23
        , cons_1(3, 2) -> 23
        , cons_1(3, 3) -> 23
        , cons_1(3, 5) -> 23
        , cons_1(3, 7) -> 23
        , cons_1(3, 13) -> 23
        , cons_1(5, 2) -> 23
        , cons_1(5, 3) -> 23
        , cons_1(5, 5) -> 23
        , cons_1(5, 7) -> 23
        , cons_1(5, 13) -> 23
        , cons_1(7, 2) -> 23
        , cons_1(7, 3) -> 23
        , cons_1(7, 5) -> 23
        , cons_1(7, 7) -> 23
        , cons_1(7, 13) -> 23
        , cons_1(13, 2) -> 23
        , cons_1(13, 3) -> 23
        , cons_1(13, 5) -> 23
        , cons_1(13, 7) -> 23
        , cons_1(13, 13) -> 23
        , cons_1(17, 16) -> 15
        , cons_2(29, 28) -> 27
        , cons_2(31, 30) -> 26
        , cons_3(29, 28) -> 32
        , cons_3(37, 35) -> 33
        , cons_3(38, 36) -> 41
        , cons_4(38, 36) -> 39
        , cons_4(45, 46) -> 44
        , cons_4(48, 49) -> 42
        , cons_5(45, 46) -> 55
        , cons_5(52, 53) -> 51
        , cons_6(45, 61) -> 60
        , cons_6(54, 56) -> 58
        , cons_6(54, 77) -> 78
        , cons_7(54, 66) -> 65
        , cons_7(70, 71) -> 68
        , cons_7(76, 85) -> 86
        , cons_7(81, 82) -> 80
        , cons_8(74, 75) -> 72
        , cons_8(90, 91) -> 89
        , cons_8(93, 94) -> 88
        , cons_8(96, 91) -> 107
        , cons_9(99, 100) -> 97
        , cons_9(109, 108) -> 110
        , 0_0() -> 7
        , 0_1() -> 17
        , 0_2() -> 29
        , 0_3() -> 38
        , 0_4() -> 45
        , 0_5() -> 54
        , 0_6() -> 76
        , 0_7() -> 105
        , incr_0(2) -> 8
        , incr_0(3) -> 8
        , incr_0(5) -> 8
        , incr_0(7) -> 8
        , incr_0(13) -> 8
        , incr_1(2) -> 19
        , incr_1(3) -> 19
        , incr_1(5) -> 19
        , incr_1(7) -> 19
        , incr_1(13) -> 19
        , incr_6(60) -> 59
        , incr_7(65) -> 64
        , incr_7(68) -> 63
        , incr_7(77) -> 82
        , incr_7(78) -> 79
        , incr_8(72) -> 69
        , incr_8(85) -> 91
        , incr_8(86) -> 87
        , incr_8(95) -> 94
        , incr_9(92) -> 88
        , incr_9(101) -> 100
        , incr_9(106) -> 108
        , s_0(2) -> 9
        , s_0(3) -> 9
        , s_0(5) -> 9
        , s_0(7) -> 9
        , s_0(13) -> 9
        , s_1(2) -> 24
        , s_1(3) -> 24
        , s_1(5) -> 24
        , s_1(7) -> 24
        , s_1(13) -> 24
        , s_7(54) -> 81
        , s_7(76) -> 96
        , s_8(74) -> 93
        , s_8(76) -> 90
        , s_8(105) -> 109
        , s_9(102) -> 99
        , hd_0(2) -> 10
        , hd_0(3) -> 10
        , hd_0(5) -> 10
        , hd_0(7) -> 10
        , hd_0(13) -> 10
        , hd_1(2) -> 20
        , hd_1(3) -> 20
        , hd_1(5) -> 20
        , hd_1(7) -> 20
        , hd_1(13) -> 20
        , tl_0(2) -> 11
        , tl_0(3) -> 11
        , tl_0(5) -> 11
        , tl_0(7) -> 11
        , tl_0(13) -> 11
        , tl_1(2) -> 21
        , tl_1(3) -> 21
        , tl_1(5) -> 21
        , tl_1(7) -> 21
        , tl_1(13) -> 21
        , proper_0(2) -> 12
        , proper_0(3) -> 12
        , proper_0(5) -> 12
        , proper_0(7) -> 12
        , proper_0(13) -> 12
        , proper_1(2) -> 25
        , proper_1(3) -> 25
        , proper_1(5) -> 25
        , proper_1(7) -> 25
        , proper_1(13) -> 25
        , proper_2(15) -> 26
        , proper_2(16) -> 30
        , proper_2(17) -> 31
        , proper_3(27) -> 33
        , proper_3(28) -> 35
        , proper_3(29) -> 37
        , proper_4(36) -> 49
        , proper_4(38) -> 48
        , proper_4(43) -> 40
        , proper_5(41) -> 42
        , proper_5(45) -> 52
        , proper_5(46) -> 53
        , proper_5(47) -> 50
        , proper_6(44) -> 51
        , proper_6(59) -> 63
        , proper_7(45) -> 70
        , proper_7(46) -> 73
        , proper_7(56) -> 98
        , proper_7(60) -> 68
        , proper_7(61) -> 71
        , proper_7(64) -> 69
        , proper_8(54) -> 74
        , proper_8(56) -> 83
        , proper_8(65) -> 72
        , proper_8(66) -> 75
        , proper_8(77) -> 95
        , proper_8(80) -> 88
        , proper_8(81) -> 93
        , proper_8(82) -> 94
        , proper_8(84) -> 103
        , proper_9(76) -> 102
        , proper_9(85) -> 101
        , proper_9(89) -> 97
        , proper_9(90) -> 99
        , proper_9(91) -> 100
        , ok_0(2) -> 13
        , ok_0(3) -> 13
        , ok_0(5) -> 13
        , ok_0(7) -> 13
        , ok_0(13) -> 13
        , ok_1(16) -> 12
        , ok_1(16) -> 25
        , ok_1(17) -> 12
        , ok_1(17) -> 25
        , ok_1(18) -> 4
        , ok_1(18) -> 18
        , ok_1(19) -> 8
        , ok_1(19) -> 19
        , ok_1(20) -> 10
        , ok_1(20) -> 20
        , ok_1(21) -> 11
        , ok_1(21) -> 21
        , ok_1(22) -> 12
        , ok_1(22) -> 25
        , ok_1(23) -> 6
        , ok_1(23) -> 23
        , ok_1(24) -> 9
        , ok_1(24) -> 24
        , ok_2(28) -> 30
        , ok_2(29) -> 31
        , ok_3(32) -> 26
        , ok_3(36) -> 35
        , ok_3(38) -> 37
        , ok_4(39) -> 33
        , ok_4(45) -> 48
        , ok_4(46) -> 49
        , ok_5(54) -> 52
        , ok_5(54) -> 70
        , ok_5(55) -> 42
        , ok_5(56) -> 53
        , ok_5(56) -> 73
        , ok_6(57) -> 40
        , ok_6(58) -> 51
        , ok_6(76) -> 74
        , ok_6(77) -> 71
        , ok_6(78) -> 68
        , ok_6(84) -> 83
        , ok_6(84) -> 98
        , ok_7(62) -> 50
        , ok_7(79) -> 63
        , ok_7(85) -> 75
        , ok_7(85) -> 95
        , ok_7(86) -> 72
        , ok_7(96) -> 93
        , ok_7(104) -> 103
        , ok_7(105) -> 102
        , ok_8(87) -> 69
        , ok_8(91) -> 94
        , ok_8(106) -> 101
        , ok_8(107) -> 88
        , ok_8(109) -> 99
        , ok_9(108) -> 100
        , ok_9(110) -> 97
        , top_0(2) -> 14
        , top_0(3) -> 14
        , top_0(5) -> 14
        , top_0(7) -> 14
        , top_0(13) -> 14
        , top_1(25) -> 14
        , top_2(26) -> 14
        , top_3(33) -> 14
        , top_4(40) -> 14
        , top_5(50) -> 14
        , top_6(63) -> 14
        , top_7(69) -> 14
        , top_8(88) -> 14
        , top_9(97) -> 14
        , top_10(111) -> 14}