Problem Transformed CSR 04 Ex6 GM04 GM

Tool CaT

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

stdout:

YES(?,O(n^1))

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

Proof:
Bounds Processor:
  bound: 3
  enrichment: match
  automaton:
   final states: {6,5,4}
   transitions:
    f1(45) -> 46*
    f1(47) -> 48*
    f1(39) -> 40*
    c1() -> 7*
    g1(15) -> 16*
    g1(17) -> 18*
    g1(7) -> 8*
    g1(23) -> 24*
    a__f1(37) -> 38*
    a__f1(29) -> 30*
    a__f1(31) -> 32*
    a__f1(8) -> 9*
    a__c1() -> 25*
    f2(75) -> 76*
    f2(67) -> 68*
    f2(69) -> 70*
    f2(61) -> 62*
    c2() -> 54*
    a__c0() -> 4*
    g2(59) -> 60*
    g2(54) -> 55*
    a__f0(2) -> 5*
    a__f0(1) -> 5*
    a__f0(3) -> 5*
    a__f2(55) -> 56*
    g0(2) -> 1*
    g0(1) -> 1*
    g0(3) -> 1*
    f3(83) -> 84*
    c0() -> 2*
    g3(79) -> 80*
    mark0(2) -> 6*
    mark0(1) -> 6*
    mark0(3) -> 6*
    f0(2) -> 3*
    f0(1) -> 3*
    f0(3) -> 3*
    1 -> 45,31,17
    2 -> 47,29,15
    3 -> 39,37,23
    7 -> 59,4
    8 -> 75*
    9 -> 4*
    16 -> 32,6,5
    18 -> 32,6,5
    24 -> 32,6,5
    25 -> 6*
    29 -> 61*
    30 -> 6*
    31 -> 67*
    32 -> 6*
    37 -> 69*
    38 -> 6*
    40 -> 5*
    46 -> 5*
    48 -> 5*
    54 -> 79,25,6
    55 -> 83*
    56 -> 25,6
    60 -> 9,4
    62 -> 30*
    68 -> 32,6
    70 -> 38,6
    76 -> 9,4
    80 -> 56,25
    84 -> 56,25
  problem:

  Qed

Tool IRC1

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

stdout:

YES(?,O(n^1))

Tool IRC2

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

     Proof Output:
       The problem is match-bounded by 3.
       The enriched problem is compatible with the following automaton:
       {  a__c_0() -> 1
        , a__c_1() -> 1
        , a__f_0(2) -> 1
        , a__f_1(2) -> 1
        , a__f_1(3) -> 1
        , a__f_2(5) -> 1
        , g_0(2) -> 2
        , g_1(2) -> 1
        , g_1(4) -> 3
        , g_2(1) -> 5
        , g_2(4) -> 1
        , g_3(1) -> 1
        , c_0() -> 2
        , c_1() -> 1
        , c_1() -> 4
        , c_2() -> 1
        , mark_0(2) -> 1
        , f_0(2) -> 2
        , f_1(2) -> 1
        , f_2(2) -> 1
        , f_2(3) -> 1
        , f_3(5) -> 1}

Tool RC1

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

stdout:

YES(?,O(n^1))

Tool RC2

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

     Proof Output:
       The problem is match-bounded by 3.
       The enriched problem is compatible with the following automaton:
       {  a__c_0() -> 1
        , a__c_1() -> 1
        , a__f_0(2) -> 1
        , a__f_1(2) -> 1
        , a__f_1(3) -> 1
        , a__f_2(5) -> 1
        , g_0(2) -> 2
        , g_1(2) -> 1
        , g_1(4) -> 3
        , g_2(1) -> 5
        , g_2(4) -> 1
        , g_3(1) -> 1
        , c_0() -> 2
        , c_1() -> 1
        , c_1() -> 4
        , c_2() -> 1
        , mark_0(2) -> 1
        , f_0(2) -> 2
        , f_1(2) -> 1
        , f_2(2) -> 1
        , f_2(3) -> 1
        , f_3(5) -> 1}