Problem Transformed CSR 04 Ex25 Luc06 FR

Tool CaT

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

stdout:

YES(?,O(n^1))

Problem:
f(f(X)) -> c(n__f(n__g(n__f(X))))
c(X) -> d(activate(X))
h(X) -> c(n__d(X))
f(X) -> n__f(X)
g(X) -> n__g(X)
d(X) -> n__d(X)
activate(n__f(X)) -> f(activate(X))
activate(n__g(X)) -> g(X)
activate(n__d(X)) -> d(X)
activate(X) -> X

Proof:
Bounds Processor:
  bound: 4
  enrichment: match
  automaton:
   final states: {9,8,7,6,5,4}
   transitions:
    n__d4(194) -> 195*
    d1(96) -> 97*
    d1(11) -> 12*
    d1(88) -> 89*
    d1(90) -> 91*
    g3(216) -> 217*
    g3(208) -> 209*
    g3(210) -> 211*
    g1(80) -> 81*
    g1(82) -> 83*
    g1(74) -> 75*
    n__f4(204) -> 205*
    f1(72) -> 73*
    f1(64) -> 65*
    f1(66) -> 67*
    n__g4(222) -> 223*
    n__g4(228) -> 229*
    n__g4(220) -> 221*
    activate1(20) -> 21*
    activate1(10) -> 11*
    activate1(18) -> 19*
    n__d1(30) -> 31*
    n__d1(27) -> 28*
    n__d1(36) -> 37*
    n__g1(60) -> 61*
    n__g1(52) -> 53*
    n__g1(54) -> 55*
    n__f1(44) -> 45*
    n__f1(46) -> 47*
    n__f1(38) -> 39*
    c1(28) -> 29*
    n__d2(132) -> 133*
    n__d2(138) -> 139*
    n__d2(140) -> 141*
    n__d2(130) -> 131*
    n__g2(122) -> 123*
    n__g2(144) -> 145*
    n__g2(124) -> 125*
    n__g2(156) -> 157*
    n__g2(116) -> 117*
    n__g2(148) -> 149*
    f0(2) -> 4*
    f0(1) -> 4*
    f0(3) -> 4*
    n__f2(114) -> 115*
    n__f2(106) -> 107*
    n__f2(108) -> 109*
    n__f2(145) -> 146*
    c0(2) -> 5*
    c0(1) -> 5*
    c0(3) -> 5*
    d2(172) -> 173*
    d2(102) -> 103*
    d2(164) -> 165*
    d2(166) -> 167*
    n__f0(2) -> 1*
    n__f0(1) -> 1*
    n__f0(3) -> 1*
    activate2(101) -> 102*
    n__g0(2) -> 2*
    n__g0(1) -> 2*
    n__g0(3) -> 2*
    n__d3(182) -> 183*
    n__d3(186) -> 187*
    n__d3(188) -> 189*
    n__d3(160) -> 161*
    d0(2) -> 8*
    d0(1) -> 8*
    d0(3) -> 8*
    c2(146) -> 147*
    activate0(2) -> 9*
    activate0(1) -> 9*
    activate0(3) -> 9*
    d3(177) -> 178*
    h0(2) -> 6*
    h0(1) -> 6*
    h0(3) -> 6*
    activate3(176) -> 177*
    activate3(198) -> 199*
    n__d0(2) -> 3*
    n__d0(1) -> 3*
    n__d0(3) -> 3*
    f3(199) -> 200*
    g0(2) -> 7*
    g0(1) -> 7*
    g0(3) -> 7*
    1 -> 9,90,80,54,44,30,18
    2 -> 9,88,74,60,46,36,20
    3 -> 9,96,82,52,38,27,10
    10 -> 11,72
    11 -> 130,72
    12 -> 5*
    18 -> 19,66,11,72
    19 -> 66,11
    20 -> 21,11,72,64
    21 -> 64,11
    27 -> 166*
    28 -> 101,8
    29 -> 6*
    30 -> 164*
    31 -> 28*
    36 -> 172*
    37 -> 28*
    39 -> 4*
    45 -> 4*
    47 -> 4*
    53 -> 7*
    55 -> 7*
    61 -> 7*
    64 -> 106*
    65 -> 19,66,11,72,9
    66 -> 108*
    67 -> 19,66,11,72,9
    72 -> 114*
    73 -> 19,66,11,72,9
    74 -> 122*
    75 -> 21,64,11,72,9
    80 -> 124*
    81 -> 21,64,11,72,9
    82 -> 116*
    83 -> 21,64,11,72,9
    88 -> 132*
    89 -> 11,72,9
    90 -> 138*
    91 -> 11,72,9
    96 -> 140*
    97 -> 11,72,9
    101 -> 102*
    102 -> 160*
    103 -> 29,6
    107 -> 148,65
    109 -> 156,67,9
    115 -> 144,73,9
    117 -> 83*
    123 -> 75,9
    125 -> 81,9
    131 -> 12*
    133 -> 89*
    139 -> 91,9
    141 -> 97,9
    144 -> 208*
    145 -> 198*
    146 -> 176*
    147 -> 73,67
    148 -> 216*
    149 -> 145*
    156 -> 210*
    157 -> 145*
    161 -> 103,29
    164 -> 182*
    165 -> 102*
    166 -> 186*
    167 -> 102*
    172 -> 188*
    173 -> 102*
    176 -> 177*
    177 -> 194*
    178 -> 147,67,73,72,66,108,114
    183 -> 165*
    187 -> 167,102,160
    189 -> 173,102,160
    195 -> 178,147,73,67,19
    198 -> 199*
    199 -> 204*
    200 -> 177*
    205 -> 200,177,194
    208 -> 220*
    209 -> 199*
    210 -> 222*
    211 -> 199*
    216 -> 228*
    217 -> 199*
    221 -> 209*
    223 -> 211,199,204
    229 -> 217,199,204
  problem:

  Qed

Tool IRC1

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

stdout:

YES(?,O(n^1))

Tool IRC2

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

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:
    {  f(f(X)) -> c(n__f(n__g(n__f(X))))
     , c(X) -> d(activate(X))
     , h(X) -> c(n__d(X))
     , f(X) -> n__f(X)
     , g(X) -> n__g(X)
     , d(X) -> n__d(X)
     , activate(n__f(X)) -> f(activate(X))
     , activate(n__g(X)) -> g(X)
     , activate(n__d(X)) -> d(X)
     , activate(X) -> 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:
         {  f(f(X)) -> c(n__f(n__g(n__f(X))))
          , c(X) -> d(activate(X))
          , h(X) -> c(n__d(X))
          , f(X) -> n__f(X)
          , g(X) -> n__g(X)
          , d(X) -> n__d(X)
          , activate(n__f(X)) -> f(activate(X))
          , activate(n__g(X)) -> g(X)
          , activate(n__d(X)) -> d(X)
          , activate(X) -> X}

     Proof Output:
       The problem is match-bounded by 4.
       The enriched problem is compatible with the following automaton:
       {  f_0(2) -> 1
        , f_1(3) -> 1
        , f_1(3) -> 3
        , f_3(10) -> 9
        , c_0(2) -> 1
        , c_1(4) -> 1
        , c_2(5) -> 1
        , c_2(5) -> 3
        , n__f_0(2) -> 1
        , n__f_0(2) -> 2
        , n__f_0(2) -> 3
        , n__f_1(2) -> 1
        , n__f_2(3) -> 1
        , n__f_2(3) -> 3
        , n__f_2(3) -> 7
        , n__f_2(6) -> 5
        , n__f_2(6) -> 9
        , n__f_4(10) -> 9
        , n__g_0(2) -> 1
        , n__g_0(2) -> 2
        , n__g_0(2) -> 3
        , n__g_1(2) -> 1
        , n__g_2(2) -> 1
        , n__g_2(2) -> 3
        , n__g_2(7) -> 6
        , n__g_2(7) -> 10
        , n__g_4(7) -> 10
        , d_0(2) -> 1
        , d_1(2) -> 1
        , d_1(2) -> 3
        , d_1(3) -> 1
        , d_2(2) -> 8
        , d_2(8) -> 1
        , d_3(9) -> 1
        , d_3(9) -> 3
        , activate_0(2) -> 1
        , activate_1(2) -> 3
        , activate_2(4) -> 8
        , activate_3(5) -> 9
        , activate_3(6) -> 10
        , h_0(2) -> 1
        , n__d_0(2) -> 1
        , n__d_0(2) -> 2
        , n__d_0(2) -> 3
        , n__d_1(2) -> 1
        , n__d_1(2) -> 4
        , n__d_1(2) -> 8
        , n__d_2(2) -> 1
        , n__d_2(2) -> 3
        , n__d_2(3) -> 1
        , n__d_3(2) -> 8
        , n__d_3(8) -> 1
        , n__d_4(9) -> 1
        , n__d_4(9) -> 3
        , g_0(2) -> 1
        , g_1(2) -> 1
        , g_1(2) -> 3
        , g_3(7) -> 10}

Tool RC1

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

stdout:

YES(?,O(n^1))

Tool RC2

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

stdout:

YES(?,O(n^1))

'Fastest (timeout of 60.0 seconds)'
-----------------------------------
Answer:           YES(?,O(n^1))
Input Problem:    runtime-complexity with respect to
  Rules:
    {  f(f(X)) -> c(n__f(n__g(n__f(X))))
     , c(X) -> d(activate(X))
     , h(X) -> c(n__d(X))
     , f(X) -> n__f(X)
     , g(X) -> n__g(X)
     , d(X) -> n__d(X)
     , activate(n__f(X)) -> f(activate(X))
     , activate(n__g(X)) -> g(X)
     , activate(n__d(X)) -> d(X)
     , activate(X) -> 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:
         {  f(f(X)) -> c(n__f(n__g(n__f(X))))
          , c(X) -> d(activate(X))
          , h(X) -> c(n__d(X))
          , f(X) -> n__f(X)
          , g(X) -> n__g(X)
          , d(X) -> n__d(X)
          , activate(n__f(X)) -> f(activate(X))
          , activate(n__g(X)) -> g(X)
          , activate(n__d(X)) -> d(X)
          , activate(X) -> X}

     Proof Output:
       The problem is match-bounded by 4.
       The enriched problem is compatible with the following automaton:
       {  f_0(2) -> 1
        , f_1(3) -> 1
        , f_1(3) -> 3
        , f_3(10) -> 9
        , c_0(2) -> 1
        , c_1(4) -> 1
        , c_2(5) -> 1
        , c_2(5) -> 3
        , n__f_0(2) -> 1
        , n__f_0(2) -> 2
        , n__f_0(2) -> 3
        , n__f_1(2) -> 1
        , n__f_2(3) -> 1
        , n__f_2(3) -> 3
        , n__f_2(3) -> 7
        , n__f_2(6) -> 5
        , n__f_2(6) -> 9
        , n__f_4(10) -> 9
        , n__g_0(2) -> 1
        , n__g_0(2) -> 2
        , n__g_0(2) -> 3
        , n__g_1(2) -> 1
        , n__g_2(2) -> 1
        , n__g_2(2) -> 3
        , n__g_2(7) -> 6
        , n__g_2(7) -> 10
        , n__g_4(7) -> 10
        , d_0(2) -> 1
        , d_1(2) -> 1
        , d_1(2) -> 3
        , d_1(3) -> 1
        , d_2(2) -> 8
        , d_2(8) -> 1
        , d_3(9) -> 1
        , d_3(9) -> 3
        , activate_0(2) -> 1
        , activate_1(2) -> 3
        , activate_2(4) -> 8
        , activate_3(5) -> 9
        , activate_3(6) -> 10
        , h_0(2) -> 1
        , n__d_0(2) -> 1
        , n__d_0(2) -> 2
        , n__d_0(2) -> 3
        , n__d_1(2) -> 1
        , n__d_1(2) -> 4
        , n__d_1(2) -> 8
        , n__d_2(2) -> 1
        , n__d_2(2) -> 3
        , n__d_2(3) -> 1
        , n__d_3(2) -> 8
        , n__d_3(8) -> 1
        , n__d_4(9) -> 1
        , n__d_4(9) -> 3
        , g_0(2) -> 1
        , g_1(2) -> 1
        , g_1(2) -> 3
        , g_3(7) -> 10}