Problem Transformed CSR 04 Ex6 GM04 C

Tool CaT

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

stdout:

YES(?,O(n^1))

Problem:
active(c()) -> mark(f(g(c())))
active(f(g(X))) -> mark(g(X))
proper(c()) -> ok(c())
proper(f(X)) -> f(proper(X))
proper(g(X)) -> g(proper(X))
f(ok(X)) -> ok(f(X))
g(ok(X)) -> ok(g(X))
top(mark(X)) -> top(proper(X))
top(ok(X)) -> top(active(X))

Proof:
Bounds Processor:
  bound: 6
  enrichment: match
  automaton:
   final states: {8,7,6,5,4}
   transitions:
    f3(137) -> 138*
    f3(119) -> 120*
    ok2(111) -> 112*
    ok3(131) -> 132*
    ok3(138) -> 139*
    ok3(135) -> 136*
    g3(122) -> 123*
    g3(130) -> 131*
    c3() -> 135*
    active3(149) -> 150*
    ok4(144) -> 145*
    ok4(201) -> 202*
    ok4(163) -> 164*
    g4(156) -> 157*
    g4(143) -> 144*
    f4(162) -> 163*
    active0(2) -> 4*
    active0(1) -> 4*
    active0(3) -> 4*
    mark4(157) -> 158*
    c0() -> 1*
    top4(169) -> 170*
    mark0(2) -> 2*
    mark0(1) -> 2*
    mark0(3) -> 2*
    active4(173) -> 174*
    f0(2) -> 6*
    f0(1) -> 6*
    f0(3) -> 6*
    proper4(168) -> 169*
    g0(2) -> 7*
    g0(1) -> 7*
    g0(3) -> 7*
    g5(182) -> 183*
    g5(210) -> 211*
    g5(175) -> 176*
    proper0(2) -> 5*
    proper0(1) -> 5*
    proper0(3) -> 5*
    proper5(187) -> 188*
    proper5(181) -> 182*
    ok0(2) -> 3*
    ok0(1) -> 3*
    ok0(3) -> 3*
    mark5(176) -> 177*
    top0(2) -> 8*
    top0(1) -> 8*
    top0(3) -> 8*
    top5(188) -> 189*
    top1(53) -> 54*
    g6(194) -> 195*
    active1(69) -> 70*
    active1(71) -> 72*
    active1(63) -> 64*
    proper6(193) -> 194*
    proper1(55) -> 56*
    proper1(52) -> 53*
    proper1(61) -> 62*
    active5(203) -> 204*
    ok1(25) -> 26*
    ok1(17) -> 18*
    ok1(36) -> 37*
    c4() -> 201*
    g1(45) -> 46*
    g1(35) -> 36*
    g1(43) -> 44*
    g1(13) -> 14*
    ok5(211) -> 212*
    f1(27) -> 28*
    f1(24) -> 25*
    f1(14) -> 15*
    f1(33) -> 34*
    top6(217) -> 218*
    c1() -> 13*
    active6(216) -> 217*
    mark1(15) -> 16*
    top2(79) -> 80*
    active2(83) -> 84*
    proper2(102) -> 103*
    proper2(93) -> 94*
    proper2(78) -> 79*
    f2(94) -> 95*
    f2(86) -> 87*
    mark2(87) -> 88*
    g2(85) -> 86*
    g2(103) -> 104*
    c2() -> 85*
    top3(106) -> 107*
    proper3(121) -> 122*
    proper3(118) -> 119*
    proper3(105) -> 106*
    1 -> 69,55,43,27
    2 -> 63,52,35,24
    3 -> 71,61,45,33
    13 -> 102,17
    14 -> 93*
    15 -> 78*
    16 -> 70,53,4
    17 -> 83*
    18 -> 56,53,5
    26 -> 34,25,6
    28 -> 25*
    34 -> 25*
    37 -> 46,36,7
    44 -> 36*
    46 -> 36*
    54 -> 8*
    56 -> 53*
    62 -> 53*
    64 -> 53*
    70 -> 53*
    72 -> 53*
    80 -> 54,8
    84 -> 79*
    85 -> 121,111
    86 -> 118*
    87 -> 105*
    88 -> 84,79
    95 -> 79*
    104 -> 94*
    107 -> 80,54
    111 -> 130*
    112 -> 103*
    120 -> 106*
    123 -> 119*
    130 -> 156*
    131 -> 137*
    132 -> 104,94
    135 -> 143*
    136 -> 182,122
    138 -> 149*
    139 -> 95,79
    143 -> 175*
    144 -> 203,162
    145 -> 183,169,123,119
    150 -> 106*
    156 -> 181*
    157 -> 168*
    158 -> 150,106
    163 -> 173*
    164 -> 120,106
    170 -> 107,80
    174 -> 169*
    175 -> 193*
    176 -> 187*
    177 -> 174,169
    183 -> 169*
    189 -> 170,107
    195 -> 188*
    201 -> 210*
    202 -> 194*
    204 -> 188*
    211 -> 216*
    212 -> 195,188
    218 -> 189,170
  problem:

  Qed

Tool IRC1

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

stdout:

YES(?,O(n^1))

Tool IRC2

Execution Time	Unknown
Answer	YES(?,O(n^1))
Input	Transformed CSR 04 Ex6 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(c()) -> mark(f(g(c())))
     , active(f(g(X))) -> mark(g(X))
     , proper(c()) -> ok(c())
     , proper(f(X)) -> f(proper(X))
     , proper(g(X)) -> g(proper(X))
     , f(ok(X)) -> ok(f(X))
     , g(ok(X)) -> ok(g(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(c()) -> mark(f(g(c())))
          , active(f(g(X))) -> mark(g(X))
          , proper(c()) -> ok(c())
          , proper(f(X)) -> f(proper(X))
          , proper(g(X)) -> g(proper(X))
          , f(ok(X)) -> ok(f(X))
          , g(ok(X)) -> ok(g(X))
          , top(mark(X)) -> top(proper(X))
          , top(ok(X)) -> top(active(X))}

     Proof Output:
       The problem is match-bounded by 6.
       The enriched problem is compatible with the following automaton:
       {  active_0(2) -> 1
        , active_0(3) -> 1
        , active_0(7) -> 1
        , active_1(2) -> 14
        , active_1(3) -> 14
        , active_1(7) -> 14
        , active_2(11) -> 15
        , active_3(26) -> 21
        , active_4(29) -> 30
        , active_5(27) -> 33
        , active_6(36) -> 37
        , c_0() -> 2
        , c_1() -> 11
        , c_2() -> 18
        , c_3() -> 25
        , c_4() -> 35
        , mark_0(2) -> 3
        , mark_0(3) -> 3
        , mark_0(7) -> 3
        , mark_1(9) -> 1
        , mark_1(9) -> 14
        , mark_2(16) -> 15
        , mark_4(28) -> 21
        , mark_5(31) -> 30
        , f_0(2) -> 4
        , f_0(3) -> 4
        , f_0(7) -> 4
        , f_1(2) -> 12
        , f_1(3) -> 12
        , f_1(7) -> 12
        , f_1(10) -> 9
        , f_2(17) -> 16
        , f_2(19) -> 15
        , f_3(22) -> 21
        , f_3(24) -> 26
        , f_4(27) -> 29
        , g_0(2) -> 5
        , g_0(3) -> 5
        , g_0(7) -> 5
        , g_1(2) -> 13
        , g_1(3) -> 13
        , g_1(7) -> 13
        , g_1(11) -> 10
        , g_2(18) -> 17
        , g_2(20) -> 19
        , g_3(18) -> 24
        , g_3(23) -> 22
        , g_4(18) -> 28
        , g_4(25) -> 27
        , g_5(25) -> 31
        , g_5(32) -> 30
        , g_5(35) -> 36
        , g_6(34) -> 33
        , proper_0(2) -> 6
        , proper_0(3) -> 6
        , proper_0(7) -> 6
        , proper_1(2) -> 14
        , proper_1(3) -> 14
        , proper_1(7) -> 14
        , proper_2(9) -> 15
        , proper_2(10) -> 19
        , proper_2(11) -> 20
        , proper_3(16) -> 21
        , proper_3(17) -> 22
        , proper_3(18) -> 23
        , proper_4(28) -> 30
        , proper_5(18) -> 32
        , proper_5(31) -> 33
        , proper_6(25) -> 34
        , ok_0(2) -> 7
        , ok_0(3) -> 7
        , ok_0(7) -> 7
        , ok_1(11) -> 6
        , ok_1(11) -> 14
        , ok_1(12) -> 4
        , ok_1(12) -> 12
        , ok_1(13) -> 5
        , ok_1(13) -> 13
        , ok_2(18) -> 20
        , ok_3(24) -> 19
        , ok_3(25) -> 23
        , ok_3(25) -> 32
        , ok_3(26) -> 15
        , ok_4(27) -> 22
        , ok_4(27) -> 30
        , ok_4(29) -> 21
        , ok_4(35) -> 34
        , ok_5(36) -> 33
        , top_0(2) -> 8
        , top_0(3) -> 8
        , top_0(7) -> 8
        , top_1(14) -> 8
        , top_2(15) -> 8
        , top_3(21) -> 8
        , top_4(30) -> 8
        , top_5(33) -> 8
        , top_6(37) -> 8}

Tool RC1

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

stdout:

YES(?,O(n^1))

Tool RC2

Execution Time	Unknown
Answer	YES(?,O(n^1))
Input	Transformed CSR 04 Ex6 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(c()) -> mark(f(g(c())))
     , active(f(g(X))) -> mark(g(X))
     , proper(c()) -> ok(c())
     , proper(f(X)) -> f(proper(X))
     , proper(g(X)) -> g(proper(X))
     , f(ok(X)) -> ok(f(X))
     , g(ok(X)) -> ok(g(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(c()) -> mark(f(g(c())))
          , active(f(g(X))) -> mark(g(X))
          , proper(c()) -> ok(c())
          , proper(f(X)) -> f(proper(X))
          , proper(g(X)) -> g(proper(X))
          , f(ok(X)) -> ok(f(X))
          , g(ok(X)) -> ok(g(X))
          , top(mark(X)) -> top(proper(X))
          , top(ok(X)) -> top(active(X))}

     Proof Output:
       The problem is match-bounded by 6.
       The enriched problem is compatible with the following automaton:
       {  active_0(2) -> 1
        , active_0(3) -> 1
        , active_0(7) -> 1
        , active_1(2) -> 14
        , active_1(3) -> 14
        , active_1(7) -> 14
        , active_2(11) -> 15
        , active_3(26) -> 21
        , active_4(29) -> 30
        , active_5(27) -> 33
        , active_6(36) -> 37
        , c_0() -> 2
        , c_1() -> 11
        , c_2() -> 18
        , c_3() -> 25
        , c_4() -> 35
        , mark_0(2) -> 3
        , mark_0(3) -> 3
        , mark_0(7) -> 3
        , mark_1(9) -> 1
        , mark_1(9) -> 14
        , mark_2(16) -> 15
        , mark_4(28) -> 21
        , mark_5(31) -> 30
        , f_0(2) -> 4
        , f_0(3) -> 4
        , f_0(7) -> 4
        , f_1(2) -> 12
        , f_1(3) -> 12
        , f_1(7) -> 12
        , f_1(10) -> 9
        , f_2(17) -> 16
        , f_2(19) -> 15
        , f_3(22) -> 21
        , f_3(24) -> 26
        , f_4(27) -> 29
        , g_0(2) -> 5
        , g_0(3) -> 5
        , g_0(7) -> 5
        , g_1(2) -> 13
        , g_1(3) -> 13
        , g_1(7) -> 13
        , g_1(11) -> 10
        , g_2(18) -> 17
        , g_2(20) -> 19
        , g_3(18) -> 24
        , g_3(23) -> 22
        , g_4(18) -> 28
        , g_4(25) -> 27
        , g_5(25) -> 31
        , g_5(32) -> 30
        , g_5(35) -> 36
        , g_6(34) -> 33
        , proper_0(2) -> 6
        , proper_0(3) -> 6
        , proper_0(7) -> 6
        , proper_1(2) -> 14
        , proper_1(3) -> 14
        , proper_1(7) -> 14
        , proper_2(9) -> 15
        , proper_2(10) -> 19
        , proper_2(11) -> 20
        , proper_3(16) -> 21
        , proper_3(17) -> 22
        , proper_3(18) -> 23
        , proper_4(28) -> 30
        , proper_5(18) -> 32
        , proper_5(31) -> 33
        , proper_6(25) -> 34
        , ok_0(2) -> 7
        , ok_0(3) -> 7
        , ok_0(7) -> 7
        , ok_1(11) -> 6
        , ok_1(11) -> 14
        , ok_1(12) -> 4
        , ok_1(12) -> 12
        , ok_1(13) -> 5
        , ok_1(13) -> 13
        , ok_2(18) -> 20
        , ok_3(24) -> 19
        , ok_3(25) -> 23
        , ok_3(25) -> 32
        , ok_3(26) -> 15
        , ok_4(27) -> 22
        , ok_4(27) -> 30
        , ok_4(29) -> 21
        , ok_4(35) -> 34
        , ok_5(36) -> 33
        , top_0(2) -> 8
        , top_0(3) -> 8
        , top_0(7) -> 8
        , top_1(14) -> 8
        , top_2(15) -> 8
        , top_3(21) -> 8
        , top_4(30) -> 8
        , top_5(33) -> 8
        , top_6(37) -> 8}