Problem Transformed CSR 04 Ex25 Luc06 GM

Tool CaT

Execution Time	Unknown
Answer	YES(?,O(n^1))
Input	Transformed CSR 04 Ex25 Luc06 GM

stdout:

YES(?,O(n^1))

Problem:
a__f(f(X)) -> a__c(f(g(f(X))))
a__c(X) -> d(X)
a__h(X) -> a__c(d(X))
mark(f(X)) -> a__f(mark(X))
mark(c(X)) -> a__c(X)
mark(h(X)) -> a__h(mark(X))
mark(g(X)) -> g(X)
mark(d(X)) -> d(X)
a__f(X) -> f(X)
a__c(X) -> c(X)
a__h(X) -> h(X)

Proof:
Bounds Processor:
  bound: 3
  enrichment: match
  automaton:
   final states: {9,8,7,6}
   transitions:
    h1(172) -> 173*
    h1(174) -> 175*
    h1(164) -> 165*
    h1(166) -> 167*
    h1(180) -> 181*
    c1(142) -> 143*
    c1(156) -> 157*
    c1(158) -> 159*
    c1(148) -> 149*
    c1(150) -> 151*
    f1(20) -> 21*
    f1(15) -> 16*
    f1(17) -> 18*
    f1(34) -> 35*
    f1(26) -> 27*
    f1(28) -> 29*
    d1(50) -> 51*
    d1(52) -> 53*
    d1(42) -> 43*
    d1(44) -> 45*
    d1(36) -> 37*
    g1(132) -> 133*
    g1(134) -> 135*
    g1(124) -> 125*
    g1(126) -> 127*
    g1(16) -> 17*
    g1(140) -> 141*
    a__h1(118) -> 119*
    mark1(92) -> 93*
    mark1(94) -> 95*
    mark1(84) -> 85*
    mark1(86) -> 87*
    mark1(76) -> 77*
    a__c1(60) -> 61*
    a__c1(102) -> 103*
    a__c1(74) -> 75*
    a__c1(116) -> 117*
    a__c1(66) -> 67*
    a__c1(108) -> 109*
    a__c1(68) -> 69*
    a__c1(58) -> 59*
    a__c1(18) -> 19*
    a__c1(110) -> 111*
    a__c1(100) -> 101*
    a__f1(77) -> 78*
    h2(280) -> 281*
    a__f0(5) -> 6*
    a__f0(2) -> 6*
    a__f0(4) -> 6*
    a__f0(1) -> 6*
    a__f0(3) -> 6*
    c2(262) -> 263*
    c2(254) -> 255*
    c2(234) -> 235*
    c2(276) -> 277*
    c2(256) -> 257*
    c2(246) -> 247*
    c2(268) -> 269*
    c2(248) -> 249*
    c2(238) -> 239*
    c2(270) -> 271*
    c2(240) -> 241*
    f0(5) -> 1*
    f0(2) -> 1*
    f0(4) -> 1*
    f0(1) -> 1*
    f0(3) -> 1*
    f2(232) -> 233*
    f2(283) -> 284*
    a__c0(5) -> 7*
    a__c0(2) -> 7*
    a__c0(4) -> 7*
    a__c0(1) -> 7*
    a__c0(3) -> 7*
    a__c2(227) -> 228*
    g0(5) -> 2*
    g0(2) -> 2*
    g0(4) -> 2*
    g0(1) -> 2*
    g0(3) -> 2*
    d2(212) -> 213*
    d2(182) -> 183*
    d2(224) -> 225*
    d2(204) -> 205*
    d2(226) -> 227*
    d2(206) -> 207*
    d2(196) -> 197*
    d2(218) -> 219*
    d2(198) -> 199*
    d2(188) -> 189*
    d2(220) -> 221*
    d2(190) -> 191*
    d0(5) -> 3*
    d0(2) -> 3*
    d0(4) -> 3*
    d0(1) -> 3*
    d0(3) -> 3*
    c3(292) -> 293*
    a__h0(5) -> 8*
    a__h0(2) -> 8*
    a__h0(4) -> 8*
    a__h0(1) -> 8*
    a__h0(3) -> 8*
    d3(287) -> 288*
    mark0(5) -> 9*
    mark0(2) -> 9*
    mark0(4) -> 9*
    mark0(1) -> 9*
    mark0(3) -> 9*
    g2(282) -> 283*
    c0(5) -> 4*
    c0(2) -> 4*
    c0(4) -> 4*
    c0(1) -> 4*
    c0(3) -> 4*
    h0(5) -> 5*
    h0(2) -> 5*
    h0(4) -> 5*
    h0(1) -> 5*
    h0(3) -> 5*
    1 -> 166,148,134,110,92,42,28
    2 -> 174,156,126,102,84,50,20
    3 -> 164,142,140,116,94,36,34
    4 -> 172,150,132,108,86,44,26
    5 -> 180,158,124,100,76,52,15
    16 -> 6*
    18 -> 248,198
    19 -> 6*
    21 -> 6,16
    27 -> 6,16
    29 -> 6,16
    35 -> 6,16
    37 -> 95,77,118,9,58,7
    43 -> 95,77,118,9,60,7
    45 -> 95,77,118,9,66,7
    51 -> 95,77,118,9,68,7
    53 -> 95,77,118,9,74,7
    58 -> 246,196
    59 -> 8*
    60 -> 276,224
    61 -> 8*
    66 -> 268,218
    67 -> 8*
    68 -> 262,212
    69 -> 8*
    74 -> 270,220
    75 -> 8*
    77 -> 232,118
    78 -> 93,77,118,9
    85 -> 77*
    87 -> 77*
    93 -> 77*
    95 -> 77*
    100 -> 256,206
    101 -> 87,77,118,9
    102 -> 234,182
    103 -> 87,77,118,9
    108 -> 240,190
    109 -> 87,77,118,9
    110 -> 254,204
    111 -> 87,77,118,9
    116 -> 238,188
    117 -> 87,77,118,9
    118 -> 280,226
    119 -> 77,118,9
    125 -> 85,77,118,9
    127 -> 85,77,118,9
    133 -> 85,77,118,9
    135 -> 85,77,118,9
    141 -> 85,77,118,9
    143 -> 7*
    149 -> 7*
    151 -> 7*
    157 -> 7*
    159 -> 7*
    165 -> 8*
    167 -> 8*
    173 -> 8*
    175 -> 8*
    181 -> 8*
    183 -> 103*
    189 -> 117*
    191 -> 109*
    197 -> 59*
    199 -> 19*
    205 -> 111*
    207 -> 101,9
    213 -> 69,8
    219 -> 67,8
    221 -> 75,8
    225 -> 61,8
    227 -> 292,287
    228 -> 78,93,119,9
    233 -> 282,78,9
    235 -> 103*
    239 -> 117*
    241 -> 109*
    247 -> 59*
    249 -> 19*
    255 -> 111*
    257 -> 101,9
    263 -> 69,8
    269 -> 67,8
    271 -> 75,8
    277 -> 61,8
    281 -> 119,9
    284 -> 227*
    288 -> 228,119
    293 -> 228,119
  problem:

  Qed

Tool IRC1

Execution Time	Unknown
Answer	YES(?,O(n^1))
Input	Transformed CSR 04 Ex25 Luc06 GM

stdout:

YES(?,O(n^1))

Tool IRC2

Execution Time	Unknown
Answer	YES(?,O(n^1))
Input	Transformed CSR 04 Ex25 Luc06 GM

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:
    {  a__f(f(X)) -> a__c(f(g(f(X))))
     , a__c(X) -> d(X)
     , a__h(X) -> a__c(d(X))
     , mark(f(X)) -> a__f(mark(X))
     , mark(c(X)) -> a__c(X)
     , mark(h(X)) -> a__h(mark(X))
     , mark(g(X)) -> g(X)
     , mark(d(X)) -> d(X)
     , a__f(X) -> f(X)
     , a__c(X) -> c(X)
     , a__h(X) -> h(X)}

Proof Output:
  'Bounds with minimal-enrichment and initial automaton 'match'' proved the best result:

  Details:
  --------
    'Bounds with minimal-enrichment and initial automaton 'match'' succeeded with the following output:
     'Bounds with minimal-enrichment and initial automaton 'match''
     --------------------------------------------------------------
     Answer:           YES(?,O(n^1))
     Input Problem:    innermost runtime-complexity with respect to
       Rules:
         {  a__f(f(X)) -> a__c(f(g(f(X))))
          , a__c(X) -> d(X)
          , a__h(X) -> a__c(d(X))
          , mark(f(X)) -> a__f(mark(X))
          , mark(c(X)) -> a__c(X)
          , mark(h(X)) -> a__h(mark(X))
          , mark(g(X)) -> g(X)
          , mark(d(X)) -> d(X)
          , a__f(X) -> f(X)
          , a__c(X) -> c(X)
          , a__h(X) -> h(X)}

     Proof Output:
       The problem is match-bounded by 3.
       The enriched problem is compatible with the following automaton:
       {  a__f_0(2) -> 1
        , a__f_1(6) -> 1
        , a__f_1(6) -> 6
        , f_0(2) -> 2
        , f_1(2) -> 1
        , f_1(2) -> 5
        , f_1(4) -> 3
        , f_2(6) -> 1
        , f_2(6) -> 6
        , f_2(8) -> 7
        , a__c_0(2) -> 1
        , a__c_1(1) -> 1
        , a__c_1(2) -> 1
        , a__c_1(2) -> 6
        , a__c_1(3) -> 1
        , a__c_2(7) -> 1
        , a__c_2(7) -> 6
        , g_0(2) -> 2
        , g_1(2) -> 1
        , g_1(2) -> 6
        , g_1(5) -> 4
        , g_2(6) -> 8
        , d_0(2) -> 2
        , d_1(2) -> 1
        , d_1(2) -> 6
        , d_2(1) -> 1
        , d_2(2) -> 1
        , d_2(2) -> 6
        , d_2(3) -> 1
        , d_2(6) -> 7
        , d_3(7) -> 1
        , d_3(7) -> 6
        , a__h_0(2) -> 1
        , a__h_1(6) -> 1
        , a__h_1(6) -> 6
        , mark_0(2) -> 1
        , mark_1(2) -> 6
        , c_0(2) -> 2
        , c_1(2) -> 1
        , c_2(1) -> 1
        , c_2(2) -> 1
        , c_2(2) -> 6
        , c_2(3) -> 1
        , c_3(7) -> 1
        , c_3(7) -> 6
        , h_0(2) -> 2
        , h_1(2) -> 1
        , h_2(6) -> 1
        , h_2(6) -> 6}

Tool RC1

Execution Time	Unknown
Answer	YES(?,O(n^1))
Input	Transformed CSR 04 Ex25 Luc06 GM

stdout:

YES(?,O(n^1))

Tool RC2

Execution Time	Unknown
Answer	YES(?,O(n^1))
Input	Transformed CSR 04 Ex25 Luc06 GM

stdout:

YES(?,O(n^1))

'Fastest (timeout of 60.0 seconds)'
-----------------------------------
Answer:           YES(?,O(n^1))
Input Problem:    runtime-complexity with respect to
  Rules:
    {  a__f(f(X)) -> a__c(f(g(f(X))))
     , a__c(X) -> d(X)
     , a__h(X) -> a__c(d(X))
     , mark(f(X)) -> a__f(mark(X))
     , mark(c(X)) -> a__c(X)
     , mark(h(X)) -> a__h(mark(X))
     , mark(g(X)) -> g(X)
     , mark(d(X)) -> d(X)
     , a__f(X) -> f(X)
     , a__c(X) -> c(X)
     , a__h(X) -> h(X)}

Proof Output:
  'Bounds with minimal-enrichment and initial automaton 'match'' proved the best result:

  Details:
  --------
    'Bounds with minimal-enrichment and initial automaton 'match'' succeeded with the following output:
     'Bounds with minimal-enrichment and initial automaton 'match''
     --------------------------------------------------------------
     Answer:           YES(?,O(n^1))
     Input Problem:    runtime-complexity with respect to
       Rules:
         {  a__f(f(X)) -> a__c(f(g(f(X))))
          , a__c(X) -> d(X)
          , a__h(X) -> a__c(d(X))
          , mark(f(X)) -> a__f(mark(X))
          , mark(c(X)) -> a__c(X)
          , mark(h(X)) -> a__h(mark(X))
          , mark(g(X)) -> g(X)
          , mark(d(X)) -> d(X)
          , a__f(X) -> f(X)
          , a__c(X) -> c(X)
          , a__h(X) -> h(X)}

     Proof Output:
       The problem is match-bounded by 3.
       The enriched problem is compatible with the following automaton:
       {  a__f_0(2) -> 1
        , a__f_1(6) -> 1
        , a__f_1(6) -> 6
        , f_0(2) -> 2
        , f_1(2) -> 1
        , f_1(2) -> 5
        , f_1(4) -> 3
        , f_2(6) -> 1
        , f_2(6) -> 6
        , f_2(8) -> 7
        , a__c_0(2) -> 1
        , a__c_1(1) -> 1
        , a__c_1(2) -> 1
        , a__c_1(2) -> 6
        , a__c_1(3) -> 1
        , a__c_2(7) -> 1
        , a__c_2(7) -> 6
        , g_0(2) -> 2
        , g_1(2) -> 1
        , g_1(2) -> 6
        , g_1(5) -> 4
        , g_2(6) -> 8
        , d_0(2) -> 2
        , d_1(2) -> 1
        , d_1(2) -> 6
        , d_2(1) -> 1
        , d_2(2) -> 1
        , d_2(2) -> 6
        , d_2(3) -> 1
        , d_2(6) -> 7
        , d_3(7) -> 1
        , d_3(7) -> 6
        , a__h_0(2) -> 1
        , a__h_1(6) -> 1
        , a__h_1(6) -> 6
        , mark_0(2) -> 1
        , mark_1(2) -> 6
        , c_0(2) -> 2
        , c_1(2) -> 1
        , c_2(1) -> 1
        , c_2(2) -> 1
        , c_2(2) -> 6
        , c_2(3) -> 1
        , c_3(7) -> 1
        , c_3(7) -> 6
        , h_0(2) -> 2
        , h_1(2) -> 1
        , h_2(6) -> 1
        , h_2(6) -> 6}