Problem ICFP 2010 26186

Tool CaT

Execution Time	Unknown
Answer	YES(?,O(n^1))
Input	ICFP 2010 26186

stdout:

YES(?,O(n^1))

Problem:
0(1(2(1(x1)))) -> 1(2(1(1(0(1(2(0(1(2(x1))))))))))
0(1(2(1(x1)))) -> 1(2(1(1(0(1(2(0(1(2(0(1(2(x1)))))))))))))
0(1(2(1(x1)))) -> 1(2(1(1(0(1(2(0(1(2(0(1(2(0(1(2(x1))))))))))))))))
0(1(2(1(x1)))) -> 1(2(1(1(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(x1)))))))))))))))))))
0(1(2(1(x1)))) -> 1(2(1(1(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(x1))))))))))))))))))))))
0(1(2(1(x1)))) -> 1(2(1(1(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(x1)))))))))))))))))))))))))
0(1(2(1(x1)))) ->
1(2(1(1(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(x1))))))))))))))))))))))))))))
0(1(2(1(x1)))) ->
1(2(1(1(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(x1)))))))))))))))))))))))))))))))

Proof:
Bounds Processor:
  bound: 2
  enrichment: match
  automaton:
   final states: {3}
   transitions:
    11(22) -> 23*
    11(24) -> 25*
    11(19) -> 20*
    11(21) -> 22*
    11(16) -> 17*
    21(15) -> 16*
    21(32) -> 33*
    21(26) -> 27*
    21(23) -> 24*
    21(18) -> 19*
    01(20) -> 21*
    01(17) -> 18*
    12(52) -> 53*
    12(54) -> 55*
    12(49) -> 50*
    12(51) -> 52*
    12(46) -> 47*
    00(2) -> 3*
    00(1) -> 3*
    22(60) -> 61*
    22(45) -> 46*
    22(58) -> 59*
    22(53) -> 54*
    22(48) -> 49*
    10(2) -> 1*
    10(1) -> 1*
    02(50) -> 51*
    02(47) -> 48*
    20(2) -> 2*
    20(1) -> 2*
    1 -> 26*
    2 -> 15*
    21 -> 32*
    24 -> 45*
    25 -> 18,3
    27 -> 16*
    33 -> 19*
    51 -> 58*
    54 -> 60*
    55 -> 21,32
    59 -> 49*
    61 -> 46*
  problem:

  Qed

Tool IRC1

Execution Time	Unknown
Answer	YES(?,O(n^1))
Input	ICFP 2010 26186

stdout:

YES(?,O(n^1))

Tool IRC2

Execution Time	Unknown
Answer	YES(?,O(n^1))
Input	ICFP 2010 26186

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:
    {  0(1(2(1(x1)))) -> 1(2(1(1(0(1(2(0(1(2(x1))))))))))
     , 0(1(2(1(x1)))) -> 1(2(1(1(0(1(2(0(1(2(0(1(2(x1)))))))))))))
     , 0(1(2(1(x1)))) ->
       1(2(1(1(0(1(2(0(1(2(0(1(2(0(1(2(x1))))))))))))))))
     , 0(1(2(1(x1)))) ->
       1(2(1(1(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(x1)))))))))))))))))))
     , 0(1(2(1(x1)))) ->
       1(2(1(1(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(x1))))))))))))))))))))))
     , 0(1(2(1(x1)))) ->
       1(2(1(1(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(x1)))))))))))))))))))))))))
     , 0(1(2(1(x1)))) ->
       1(2(1(1(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(x1))))))))))))))))))))))))))))
     , 0(1(2(1(x1)))) ->
       1(2(1(1(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(x1)))))))))))))))))))))))))))))))}

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:
         {  0(1(2(1(x1)))) -> 1(2(1(1(0(1(2(0(1(2(x1))))))))))
          , 0(1(2(1(x1)))) -> 1(2(1(1(0(1(2(0(1(2(0(1(2(x1)))))))))))))
          , 0(1(2(1(x1)))) ->
            1(2(1(1(0(1(2(0(1(2(0(1(2(0(1(2(x1))))))))))))))))
          , 0(1(2(1(x1)))) ->
            1(2(1(1(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(x1)))))))))))))))))))
          , 0(1(2(1(x1)))) ->
            1(2(1(1(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(x1))))))))))))))))))))))
          , 0(1(2(1(x1)))) ->
            1(2(1(1(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(x1)))))))))))))))))))))))))
          , 0(1(2(1(x1)))) ->
            1(2(1(1(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(x1))))))))))))))))))))))))))))
          , 0(1(2(1(x1)))) ->
            1(2(1(1(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(x1)))))))))))))))))))))))))))))))}

     Proof Output:
       The problem is match-bounded by 2.
       The enriched problem is compatible with the following automaton:
       {  0_0(2) -> 1
        , 0_1(7) -> 6
        , 0_1(10) -> 9
        , 0_2(16) -> 15
        , 0_2(19) -> 18
        , 0_2(22) -> 21
        , 0_2(25) -> 24
        , 1_0(2) -> 2
        , 1_1(3) -> 1
        , 1_1(3) -> 9
        , 1_1(5) -> 4
        , 1_1(6) -> 5
        , 1_1(8) -> 7
        , 1_1(11) -> 10
        , 1_2(12) -> 6
        , 1_2(14) -> 13
        , 1_2(15) -> 14
        , 1_2(17) -> 16
        , 1_2(18) -> 14
        , 1_2(20) -> 19
        , 1_2(21) -> 14
        , 1_2(23) -> 22
        , 1_2(26) -> 25
        , 2_0(2) -> 2
        , 2_1(2) -> 11
        , 2_1(4) -> 3
        , 2_1(6) -> 8
        , 2_1(9) -> 8
        , 2_2(3) -> 26
        , 2_2(12) -> 17
        , 2_2(13) -> 12
        , 2_2(15) -> 17
        , 2_2(18) -> 17
        , 2_2(21) -> 20
        , 2_2(24) -> 23}

Tool RC1

Execution Time	Unknown
Answer	YES(?,O(n^1))
Input	ICFP 2010 26186

stdout:

YES(?,O(n^1))

Tool RC2

Execution Time	Unknown
Answer	YES(?,O(n^1))
Input	ICFP 2010 26186

stdout:

YES(?,O(n^1))

'Fastest (timeout of 60.0 seconds)'
-----------------------------------
Answer:           YES(?,O(n^1))
Input Problem:    runtime-complexity with respect to
  Rules:
    {  0(1(2(1(x1)))) -> 1(2(1(1(0(1(2(0(1(2(x1))))))))))
     , 0(1(2(1(x1)))) -> 1(2(1(1(0(1(2(0(1(2(0(1(2(x1)))))))))))))
     , 0(1(2(1(x1)))) ->
       1(2(1(1(0(1(2(0(1(2(0(1(2(0(1(2(x1))))))))))))))))
     , 0(1(2(1(x1)))) ->
       1(2(1(1(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(x1)))))))))))))))))))
     , 0(1(2(1(x1)))) ->
       1(2(1(1(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(x1))))))))))))))))))))))
     , 0(1(2(1(x1)))) ->
       1(2(1(1(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(x1)))))))))))))))))))))))))
     , 0(1(2(1(x1)))) ->
       1(2(1(1(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(x1))))))))))))))))))))))))))))
     , 0(1(2(1(x1)))) ->
       1(2(1(1(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(x1)))))))))))))))))))))))))))))))}

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:
         {  0(1(2(1(x1)))) -> 1(2(1(1(0(1(2(0(1(2(x1))))))))))
          , 0(1(2(1(x1)))) -> 1(2(1(1(0(1(2(0(1(2(0(1(2(x1)))))))))))))
          , 0(1(2(1(x1)))) ->
            1(2(1(1(0(1(2(0(1(2(0(1(2(0(1(2(x1))))))))))))))))
          , 0(1(2(1(x1)))) ->
            1(2(1(1(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(x1)))))))))))))))))))
          , 0(1(2(1(x1)))) ->
            1(2(1(1(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(x1))))))))))))))))))))))
          , 0(1(2(1(x1)))) ->
            1(2(1(1(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(x1)))))))))))))))))))))))))
          , 0(1(2(1(x1)))) ->
            1(2(1(1(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(x1))))))))))))))))))))))))))))
          , 0(1(2(1(x1)))) ->
            1(2(1(1(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(x1)))))))))))))))))))))))))))))))}

     Proof Output:
       The problem is match-bounded by 2.
       The enriched problem is compatible with the following automaton:
       {  0_0(2) -> 1
        , 0_1(7) -> 6
        , 0_1(10) -> 9
        , 0_2(16) -> 15
        , 0_2(19) -> 18
        , 0_2(22) -> 21
        , 0_2(25) -> 24
        , 1_0(2) -> 2
        , 1_1(3) -> 1
        , 1_1(3) -> 9
        , 1_1(5) -> 4
        , 1_1(6) -> 5
        , 1_1(8) -> 7
        , 1_1(11) -> 10
        , 1_2(12) -> 6
        , 1_2(14) -> 13
        , 1_2(15) -> 14
        , 1_2(17) -> 16
        , 1_2(18) -> 14
        , 1_2(20) -> 19
        , 1_2(21) -> 14
        , 1_2(23) -> 22
        , 1_2(26) -> 25
        , 2_0(2) -> 2
        , 2_1(2) -> 11
        , 2_1(4) -> 3
        , 2_1(6) -> 8
        , 2_1(9) -> 8
        , 2_2(3) -> 26
        , 2_2(12) -> 17
        , 2_2(13) -> 12
        , 2_2(15) -> 17
        , 2_2(18) -> 17
        , 2_2(21) -> 20
        , 2_2(24) -> 23}