Problem Transformed CSR 04 Ex1 Zan97 C

Tool CaT

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

stdout:

YES(?,O(n^1))

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

Proof:
 Bounds Processor:
  bound: 4
  enrichment: match
  automaton:
   final states: {9,8,7,6,5}
   transitions:
    ok3(124) -> 125*
    top1(62) -> 63*
    d3() -> 124*
    active1(80) -> 81*
    active1(86) -> 87*
    active1(88) -> 89*
    active1(78) -> 79*
    top4(132) -> 133*
    proper1(70) -> 71*
    proper1(72) -> 73*
    proper1(64) -> 65*
    proper1(61) -> 62*
    active4(131) -> 132*
    ok1(44) -> 45*
    ok1(26) -> 27*
    ok1(16) -> 17*
    ok1(18) -> 19*
    h1(52) -> 53*
    h1(54) -> 55*
    h1(46) -> 47*
    h1(43) -> 44*
    g1(25) -> 26*
    g1(34) -> 35*
    g1(36) -> 37*
    g1(28) -> 29*
    d1() -> 10*
    c1() -> 16*
    mark1(10) -> 11*
    top2(93) -> 94*
    active0(2) -> 5*
    active0(4) -> 5*
    active0(1) -> 5*
    active0(3) -> 5*
    active2(104) -> 105*
    active2(98) -> 99*
    g0(2) -> 7*
    g0(4) -> 7*
    g0(1) -> 7*
    g0(3) -> 7*
    proper2(92) -> 93*
    mark0(2) -> 1*
    mark0(4) -> 1*
    mark0(1) -> 1*
    mark0(3) -> 1*
    ok2(110) -> 111*
    h0(2) -> 8*
    h0(4) -> 8*
    h0(1) -> 8*
    h0(3) -> 8*
    d2() -> 106*
    c0() -> 2*
    mark2(106) -> 107*
    d0() -> 3*
    top3(118) -> 119*
    proper0(2) -> 6*
    proper0(4) -> 6*
    proper0(1) -> 6*
    proper0(3) -> 6*
    active3(122) -> 123*
    ok0(2) -> 4*
    ok0(4) -> 4*
    ok0(1) -> 4*
    ok0(3) -> 4*
    proper3(117) -> 118*
    top0(2) -> 9*
    top0(4) -> 9*
    top0(1) -> 9*
    top0(3) -> 9*
    1 -> 86,70,52,34
    2 -> 78,61,43,25
    3 -> 88,72,54,36
    4 -> 80,64,46,28
    10 -> 92,18
    11 -> 79,62,5
    16 -> 98*
    17 -> 62,6
    18 -> 104*
    19 -> 73,62,6
    27 -> 29,26,7
    29 -> 26*
    35 -> 26*
    37 -> 26*
    45 -> 47,44,8
    47 -> 44*
    53 -> 44*
    55 -> 44*
    63 -> 9*
    65 -> 62*
    71 -> 62*
    73 -> 62*
    79 -> 62*
    81 -> 62*
    87 -> 62*
    89 -> 62*
    94 -> 63,9
    99 -> 93*
    105 -> 93*
    106 -> 117,110
    107 -> 99,93
    110 -> 122*
    111 -> 93*
    119 -> 94,63
    123 -> 118*
    124 -> 131*
    125 -> 118*
    133 -> 119,94
  problem:
   
  Qed

Tool IRC1

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

stdout:

YES(?,O(n^1))

Tool IRC2

Execution TimeUnknown
Answer
YES(?,O(n^1))
InputTransformed CSR 04 Ex1 Zan97 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(g(X)) -> mark(h(X))
     , active(c()) -> mark(d())
     , active(h(d())) -> mark(g(c()))
     , proper(g(X)) -> g(proper(X))
     , proper(h(X)) -> h(proper(X))
     , proper(c()) -> ok(c())
     , proper(d()) -> ok(d())
     , g(ok(X)) -> ok(g(X))
     , h(ok(X)) -> ok(h(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(g(X)) -> mark(h(X))
          , active(c()) -> mark(d())
          , active(h(d())) -> mark(g(c()))
          , proper(g(X)) -> g(proper(X))
          , proper(h(X)) -> h(proper(X))
          , proper(c()) -> ok(c())
          , proper(d()) -> ok(d())
          , g(ok(X)) -> ok(g(X))
          , h(ok(X)) -> ok(h(X))
          , top(mark(X)) -> top(proper(X))
          , top(ok(X)) -> top(active(X))}
     
     Proof Output:    
       The problem is match-bounded by 4.
       The enriched problem is compatible with the following automaton:
       {  active_0(3) -> 1
        , active_0(5) -> 1
        , active_0(6) -> 1
        , active_0(8) -> 1
        , active_1(3) -> 14
        , active_1(5) -> 14
        , active_1(6) -> 14
        , active_1(8) -> 14
        , active_2(10) -> 15
        , active_2(11) -> 15
        , active_3(16) -> 17
        , active_4(18) -> 19
        , g_0(3) -> 2
        , g_0(5) -> 2
        , g_0(6) -> 2
        , g_0(8) -> 2
        , g_1(3) -> 12
        , g_1(5) -> 12
        , g_1(6) -> 12
        , g_1(8) -> 12
        , mark_0(3) -> 3
        , mark_0(5) -> 3
        , mark_0(6) -> 3
        , mark_0(8) -> 3
        , mark_1(10) -> 1
        , mark_1(10) -> 14
        , mark_2(16) -> 15
        , h_0(3) -> 4
        , h_0(5) -> 4
        , h_0(6) -> 4
        , h_0(8) -> 4
        , h_1(3) -> 13
        , h_1(5) -> 13
        , h_1(6) -> 13
        , h_1(8) -> 13
        , c_0() -> 5
        , c_1() -> 11
        , d_0() -> 6
        , d_1() -> 10
        , d_2() -> 16
        , d_3() -> 18
        , proper_0(3) -> 7
        , proper_0(5) -> 7
        , proper_0(6) -> 7
        , proper_0(8) -> 7
        , proper_1(3) -> 14
        , proper_1(5) -> 14
        , proper_1(6) -> 14
        , proper_1(8) -> 14
        , proper_2(10) -> 15
        , proper_3(16) -> 17
        , ok_0(3) -> 8
        , ok_0(5) -> 8
        , ok_0(6) -> 8
        , ok_0(8) -> 8
        , ok_1(10) -> 7
        , ok_1(10) -> 14
        , ok_1(11) -> 7
        , ok_1(11) -> 14
        , ok_1(12) -> 2
        , ok_1(12) -> 12
        , ok_1(13) -> 4
        , ok_1(13) -> 13
        , ok_2(16) -> 15
        , ok_3(18) -> 17
        , top_0(3) -> 9
        , top_0(5) -> 9
        , top_0(6) -> 9
        , top_0(8) -> 9
        , top_1(14) -> 9
        , top_2(15) -> 9
        , top_3(17) -> 9
        , top_4(19) -> 9}

Tool RC1

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

stdout:

YES(?,O(n^1))

Tool RC2

Execution TimeUnknown
Answer
YES(?,O(n^1))
InputTransformed CSR 04 Ex1 Zan97 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(g(X)) -> mark(h(X))
     , active(c()) -> mark(d())
     , active(h(d())) -> mark(g(c()))
     , proper(g(X)) -> g(proper(X))
     , proper(h(X)) -> h(proper(X))
     , proper(c()) -> ok(c())
     , proper(d()) -> ok(d())
     , g(ok(X)) -> ok(g(X))
     , h(ok(X)) -> ok(h(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(g(X)) -> mark(h(X))
          , active(c()) -> mark(d())
          , active(h(d())) -> mark(g(c()))
          , proper(g(X)) -> g(proper(X))
          , proper(h(X)) -> h(proper(X))
          , proper(c()) -> ok(c())
          , proper(d()) -> ok(d())
          , g(ok(X)) -> ok(g(X))
          , h(ok(X)) -> ok(h(X))
          , top(mark(X)) -> top(proper(X))
          , top(ok(X)) -> top(active(X))}
     
     Proof Output:    
       The problem is match-bounded by 4.
       The enriched problem is compatible with the following automaton:
       {  active_0(3) -> 1
        , active_0(5) -> 1
        , active_0(6) -> 1
        , active_0(8) -> 1
        , active_1(3) -> 14
        , active_1(5) -> 14
        , active_1(6) -> 14
        , active_1(8) -> 14
        , active_2(10) -> 15
        , active_2(11) -> 15
        , active_3(16) -> 17
        , active_4(18) -> 19
        , g_0(3) -> 2
        , g_0(5) -> 2
        , g_0(6) -> 2
        , g_0(8) -> 2
        , g_1(3) -> 12
        , g_1(5) -> 12
        , g_1(6) -> 12
        , g_1(8) -> 12
        , mark_0(3) -> 3
        , mark_0(5) -> 3
        , mark_0(6) -> 3
        , mark_0(8) -> 3
        , mark_1(10) -> 1
        , mark_1(10) -> 14
        , mark_2(16) -> 15
        , h_0(3) -> 4
        , h_0(5) -> 4
        , h_0(6) -> 4
        , h_0(8) -> 4
        , h_1(3) -> 13
        , h_1(5) -> 13
        , h_1(6) -> 13
        , h_1(8) -> 13
        , c_0() -> 5
        , c_1() -> 11
        , d_0() -> 6
        , d_1() -> 10
        , d_2() -> 16
        , d_3() -> 18
        , proper_0(3) -> 7
        , proper_0(5) -> 7
        , proper_0(6) -> 7
        , proper_0(8) -> 7
        , proper_1(3) -> 14
        , proper_1(5) -> 14
        , proper_1(6) -> 14
        , proper_1(8) -> 14
        , proper_2(10) -> 15
        , proper_3(16) -> 17
        , ok_0(3) -> 8
        , ok_0(5) -> 8
        , ok_0(6) -> 8
        , ok_0(8) -> 8
        , ok_1(10) -> 7
        , ok_1(10) -> 14
        , ok_1(11) -> 7
        , ok_1(11) -> 14
        , ok_1(12) -> 2
        , ok_1(12) -> 12
        , ok_1(13) -> 4
        , ok_1(13) -> 13
        , ok_2(16) -> 15
        , ok_3(18) -> 17
        , top_0(3) -> 9
        , top_0(5) -> 9
        , top_0(6) -> 9
        , top_0(8) -> 9
        , top_1(14) -> 9
        , top_2(15) -> 9
        , top_3(17) -> 9
        , top_4(19) -> 9}