Problem ICFP 2010 212094

Tool CaT

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

stdout:

YES(?,O(n^1))

Problem:
0(1(1(2(x1)))) -> 1(3(0(1(2(x1)))))
0(1(1(2(x1)))) -> 1(3(1(0(2(x1)))))
0(1(1(2(x1)))) -> 2(3(1(3(0(1(x1))))))
0(1(2(0(x1)))) -> 1(0(0(2(2(x1)))))
0(1(2(4(x1)))) -> 0(2(3(4(1(x1)))))
0(1(2(4(x1)))) -> 1(0(4(2(3(x1)))))
0(1(2(4(x1)))) -> 1(2(3(0(4(x1)))))
0(1(2(4(x1)))) -> 2(1(4(0(3(x1)))))
0(1(2(4(x1)))) -> 1(2(3(4(0(5(x1))))))
0(1(2(4(x1)))) -> 2(1(1(0(3(4(x1))))))
0(1(2(4(x1)))) -> 4(1(2(2(3(0(x1))))))
0(1(2(4(x1)))) -> 4(5(0(2(3(1(x1))))))
0(4(2(0(x1)))) -> 0(4(2(3(0(x1)))))
0(4(2(0(x1)))) -> 2(3(0(4(0(0(x1))))))
0(4(2(0(x1)))) -> 3(4(0(2(3(0(x1))))))
0(4(2(0(x1)))) -> 4(2(3(0(4(0(x1))))))
0(4(2(0(x1)))) -> 4(3(0(0(5(2(x1))))))
0(4(2(4(x1)))) -> 4(0(2(3(1(4(x1))))))
0(4(2(4(x1)))) -> 4(0(4(2(0(3(x1))))))
5(1(2(0(x1)))) -> 2(1(3(5(0(x1)))))
5(1(2(0(x1)))) -> 3(1(0(2(5(x1)))))
5(1(2(0(x1)))) -> 2(3(0(0(1(5(x1))))))
5(1(2(4(x1)))) -> 3(2(5(1(4(x1)))))
5(1(2(4(x1)))) -> 5(2(1(3(4(x1)))))
5(1(2(4(x1)))) -> 5(5(2(1(4(x1)))))
5(1(2(4(x1)))) -> 0(3(4(5(2(1(x1))))))
5(1(4(2(x1)))) -> 3(4(5(2(1(x1)))))
5(1(4(2(x1)))) -> 2(1(3(4(5(4(x1))))))
5(1(4(2(x1)))) -> 3(3(4(2(1(5(x1))))))
5(4(1(4(x1)))) -> 3(4(4(1(5(4(x1))))))
5(4(1(4(x1)))) -> 4(1(3(5(0(4(x1))))))
5(4(1(4(x1)))) -> 5(1(3(4(5(4(x1))))))
5(4(1(4(x1)))) -> 5(1(5(3(4(4(x1))))))
5(4(2(0(x1)))) -> 5(4(2(3(0(x1)))))
5(4(2(0(x1)))) -> 0(1(2(3(4(5(x1))))))
5(4(2(0(x1)))) -> 4(5(3(3(0(2(x1))))))
0(1(2(0(4(x1))))) -> 0(2(4(1(3(0(x1))))))
0(1(2(0(4(x1))))) -> 2(0(3(4(0(1(x1))))))
0(1(2(0(4(x1))))) -> 4(0(2(3(1(0(x1))))))
0(1(4(2(2(x1))))) -> 1(2(3(4(0(2(x1))))))
5(0(1(2(4(x1))))) -> 3(0(2(1(4(5(x1))))))
5(1(2(2(4(x1))))) -> 5(2(2(1(4(5(x1))))))
5(1(2(4(0(x1))))) -> 5(0(2(1(3(4(x1))))))
5(1(2(4(0(x1))))) -> 5(0(3(2(1(4(x1))))))
5(1(3(1(4(x1))))) -> 1(5(1(3(4(0(x1))))))
5(1(4(1(2(x1))))) -> 2(1(5(3(4(1(x1))))))
5(4(1(1(4(x1))))) -> 1(1(3(4(5(4(x1))))))
5(4(1(4(0(x1))))) -> 3(4(0(4(5(1(x1))))))
5(4(3(2(0(x1))))) -> 5(4(0(3(2(3(x1))))))
5(4(5(2(0(x1))))) -> 5(0(5(4(4(2(x1))))))

Proof:
Bounds Processor:
  bound: 2
  enrichment: match
  automaton:
   final states: {6,5}
   transitions:
    11(242) -> 243*
    11(157) -> 158*
    11(274) -> 275*
    11(57) -> 58*
    11(47) -> 48*
    11(32) -> 33*
    11(194) -> 195*
    11(119) -> 120*
    11(261) -> 262*
    11(59) -> 60*
    11(256) -> 257*
    11(44) -> 45*
    11(151) -> 152*
    11(303) -> 304*
    11(298) -> 299*
    11(51) -> 52*
    11(213) -> 214*
    11(11) -> 12*
    11(305) -> 306*
    11(8) -> 9*
    11(317) -> 318*
    31(10) -> 11*
    31(97) -> 98*
    31(87) -> 88*
    31(259) -> 260*
    31(179) -> 180*
    31(154) -> 155*
    31(149) -> 150*
    31(286) -> 287*
    31(69) -> 70*
    31(241) -> 242*
    31(211) -> 212*
    31(273) -> 274*
    31(46) -> 47*
    31(93) -> 94*
    31(73) -> 74*
    31(48) -> 49*
    31(230) -> 231*
    31(195) -> 196*
    31(302) -> 303*
    31(85) -> 86*
    41(75) -> 76*
    41(262) -> 263*
    41(107) -> 108*
    41(289) -> 290*
    41(229) -> 230*
    41(109) -> 110*
    41(301) -> 302*
    41(131) -> 132*
    41(258) -> 259*
    41(158) -> 159*
    41(118) -> 119*
    41(285) -> 286*
    41(275) -> 276*
    41(68) -> 69*
    41(240) -> 241*
    41(200) -> 201*
    41(115) -> 116*
    41(297) -> 298*
    41(95) -> 96*
    51(277) -> 278*
    51(272) -> 273*
    51(182) -> 183*
    51(304) -> 305*
    51(239) -> 240*
    51(209) -> 210*
    51(139) -> 140*
    51(129) -> 130*
    51(141) -> 142*
    51(228) -> 229*
    51(133) -> 134*
    51(315) -> 316*
    51(225) -> 226*
    51(215) -> 216*
    51(287) -> 288*
    21(70) -> 71*
    21(257) -> 258*
    21(227) -> 228*
    21(299) -> 300*
    21(224) -> 225*
    21(214) -> 215*
    21(7) -> 8*
    21(199) -> 200*
    21(74) -> 75*
    21(49) -> 50*
    21(29) -> 30*
    21(196) -> 197*
    21(156) -> 157*
    21(243) -> 244*
    21(21) -> 22*
    21(98) -> 99*
    21(23) -> 24*
    21(210) -> 211*
    21(180) -> 181*
    21(155) -> 156*
    01(45) -> 46*
    01(197) -> 198*
    01(177) -> 178*
    01(117) -> 118*
    01(169) -> 170*
    01(231) -> 232*
    01(9) -> 10*
    01(181) -> 182*
    01(171) -> 172*
    01(96) -> 97*
    01(76) -> 77*
    01(71) -> 72*
    01(31) -> 32*
    01(153) -> 154*
    01(150) -> 151*
    01(130) -> 131*
    42(349) -> 350*
    42(324) -> 325*
    42(353) -> 354*
    42(328) -> 329*
    42(340) -> 341*
    00(2) -> 5*
    00(4) -> 5*
    00(1) -> 5*
    00(3) -> 5*
    32(351) -> 352*
    32(341) -> 342*
    32(363) -> 364*
    32(330) -> 331*
    32(322) -> 323*
    10(2) -> 1*
    10(4) -> 1*
    10(1) -> 1*
    10(3) -> 1*
    02(339) -> 340*
    02(329) -> 330*
    02(361) -> 362*
    02(321) -> 322*
    02(350) -> 351*
    02(325) -> 326*
    02(362) -> 363*
    02(327) -> 328*
    20(2) -> 2*
    20(4) -> 2*
    20(1) -> 2*
    20(3) -> 2*
    52(360) -> 361*
    30(2) -> 3*
    30(4) -> 3*
    30(1) -> 3*
    30(3) -> 3*
    22(359) -> 360*
    22(331) -> 332*
    22(323) -> 324*
    22(352) -> 353*
    40(2) -> 4*
    40(4) -> 4*
    40(1) -> 4*
    40(3) -> 4*
    50(2) -> 6*
    50(4) -> 6*
    50(1) -> 6*
    50(3) -> 6*
    1 -> 171,139,109,87,57,23
    2 -> 153,129,95,73,44,7
    3 -> 177,141,115,93,59,29
    4 -> 169,133,107,85,51,21
    8 -> 31*
    12 -> 10,46,172,5
    22 -> 8*
    24 -> 8*
    30 -> 8*
    32 -> 289*
    33 -> 10*
    45 -> 227,179,68
    50 -> 10,46,172,5
    52 -> 45*
    58 -> 45*
    60 -> 45*
    70 -> 315*
    72 -> 46,172,301,10,5
    74 -> 117*
    77 -> 11*
    86 -> 74*
    88 -> 74*
    94 -> 74*
    96 -> 285,239,194,149
    97 -> 272*
    99 -> 11*
    108 -> 96*
    110 -> 96*
    116 -> 96*
    117 -> 359,321
    118 -> 199*
    120 -> 49*
    130 -> 297,256
    132 -> 97*
    134 -> 130*
    140 -> 130*
    142 -> 130*
    150 -> 213*
    152 -> 119*
    154 -> 301*
    159 -> 170,97,46,172,301,10,5
    170 -> 154*
    172 -> 154*
    178 -> 154*
    183 -> 158*
    195 -> 224,209
    198 -> 158*
    201 -> 197*
    212 -> 210,140,130,297,6
    216 -> 140,130,297,6
    226 -> 215*
    231 -> 240,134,261,210,140,6
    232 -> 140,130,297,6
    240 -> 261*
    243 -> 317,277
    244 -> 210,140,6
    260 -> 211*
    263 -> 229*
    276 -> 240,134,130,297,261,6
    278 -> 240,134,130,297,261,6
    288 -> 242*
    290 -> 97*
    300 -> 214*
    306 -> 140,130,297,6
    316 -> 242*
    318 -> 240,134,130,297,261,6
    322 -> 349,327
    324 -> 339*
    326 -> 198,158
    332 -> 198,158
    342 -> 198,158
    354 -> 198,158
    364 -> 353*
  problem:

  Qed

Tool IRC1

Execution Time	Unknown
Answer	MAYBE
Input	ICFP 2010 212094

stdout:

MAYBE

Tool IRC2

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

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(1(2(x1)))) -> 1(3(0(1(2(x1)))))
     , 0(1(1(2(x1)))) -> 1(3(1(0(2(x1)))))
     , 0(1(1(2(x1)))) -> 2(3(1(3(0(1(x1))))))
     , 0(1(2(0(x1)))) -> 1(0(0(2(2(x1)))))
     , 0(1(2(4(x1)))) -> 0(2(3(4(1(x1)))))
     , 0(1(2(4(x1)))) -> 1(0(4(2(3(x1)))))
     , 0(1(2(4(x1)))) -> 1(2(3(0(4(x1)))))
     , 0(1(2(4(x1)))) -> 2(1(4(0(3(x1)))))
     , 0(1(2(4(x1)))) -> 1(2(3(4(0(5(x1))))))
     , 0(1(2(4(x1)))) -> 2(1(1(0(3(4(x1))))))
     , 0(1(2(4(x1)))) -> 4(1(2(2(3(0(x1))))))
     , 0(1(2(4(x1)))) -> 4(5(0(2(3(1(x1))))))
     , 0(4(2(0(x1)))) -> 0(4(2(3(0(x1)))))
     , 0(4(2(0(x1)))) -> 2(3(0(4(0(0(x1))))))
     , 0(4(2(0(x1)))) -> 3(4(0(2(3(0(x1))))))
     , 0(4(2(0(x1)))) -> 4(2(3(0(4(0(x1))))))
     , 0(4(2(0(x1)))) -> 4(3(0(0(5(2(x1))))))
     , 0(4(2(4(x1)))) -> 4(0(2(3(1(4(x1))))))
     , 0(4(2(4(x1)))) -> 4(0(4(2(0(3(x1))))))
     , 5(1(2(0(x1)))) -> 2(1(3(5(0(x1)))))
     , 5(1(2(0(x1)))) -> 3(1(0(2(5(x1)))))
     , 5(1(2(0(x1)))) -> 2(3(0(0(1(5(x1))))))
     , 5(1(2(4(x1)))) -> 3(2(5(1(4(x1)))))
     , 5(1(2(4(x1)))) -> 5(2(1(3(4(x1)))))
     , 5(1(2(4(x1)))) -> 5(5(2(1(4(x1)))))
     , 5(1(2(4(x1)))) -> 0(3(4(5(2(1(x1))))))
     , 5(1(4(2(x1)))) -> 3(4(5(2(1(x1)))))
     , 5(1(4(2(x1)))) -> 2(1(3(4(5(4(x1))))))
     , 5(1(4(2(x1)))) -> 3(3(4(2(1(5(x1))))))
     , 5(4(1(4(x1)))) -> 3(4(4(1(5(4(x1))))))
     , 5(4(1(4(x1)))) -> 4(1(3(5(0(4(x1))))))
     , 5(4(1(4(x1)))) -> 5(1(3(4(5(4(x1))))))
     , 5(4(1(4(x1)))) -> 5(1(5(3(4(4(x1))))))
     , 5(4(2(0(x1)))) -> 5(4(2(3(0(x1)))))
     , 5(4(2(0(x1)))) -> 0(1(2(3(4(5(x1))))))
     , 5(4(2(0(x1)))) -> 4(5(3(3(0(2(x1))))))
     , 0(1(2(0(4(x1))))) -> 0(2(4(1(3(0(x1))))))
     , 0(1(2(0(4(x1))))) -> 2(0(3(4(0(1(x1))))))
     , 0(1(2(0(4(x1))))) -> 4(0(2(3(1(0(x1))))))
     , 0(1(4(2(2(x1))))) -> 1(2(3(4(0(2(x1))))))
     , 5(0(1(2(4(x1))))) -> 3(0(2(1(4(5(x1))))))
     , 5(1(2(2(4(x1))))) -> 5(2(2(1(4(5(x1))))))
     , 5(1(2(4(0(x1))))) -> 5(0(2(1(3(4(x1))))))
     , 5(1(2(4(0(x1))))) -> 5(0(3(2(1(4(x1))))))
     , 5(1(3(1(4(x1))))) -> 1(5(1(3(4(0(x1))))))
     , 5(1(4(1(2(x1))))) -> 2(1(5(3(4(1(x1))))))
     , 5(4(1(1(4(x1))))) -> 1(1(3(4(5(4(x1))))))
     , 5(4(1(4(0(x1))))) -> 3(4(0(4(5(1(x1))))))
     , 5(4(3(2(0(x1))))) -> 5(4(0(3(2(3(x1))))))
     , 5(4(5(2(0(x1))))) -> 5(0(5(4(4(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(1(2(x1)))) -> 1(3(0(1(2(x1)))))
          , 0(1(1(2(x1)))) -> 1(3(1(0(2(x1)))))
          , 0(1(1(2(x1)))) -> 2(3(1(3(0(1(x1))))))
          , 0(1(2(0(x1)))) -> 1(0(0(2(2(x1)))))
          , 0(1(2(4(x1)))) -> 0(2(3(4(1(x1)))))
          , 0(1(2(4(x1)))) -> 1(0(4(2(3(x1)))))
          , 0(1(2(4(x1)))) -> 1(2(3(0(4(x1)))))
          , 0(1(2(4(x1)))) -> 2(1(4(0(3(x1)))))
          , 0(1(2(4(x1)))) -> 1(2(3(4(0(5(x1))))))
          , 0(1(2(4(x1)))) -> 2(1(1(0(3(4(x1))))))
          , 0(1(2(4(x1)))) -> 4(1(2(2(3(0(x1))))))
          , 0(1(2(4(x1)))) -> 4(5(0(2(3(1(x1))))))
          , 0(4(2(0(x1)))) -> 0(4(2(3(0(x1)))))
          , 0(4(2(0(x1)))) -> 2(3(0(4(0(0(x1))))))
          , 0(4(2(0(x1)))) -> 3(4(0(2(3(0(x1))))))
          , 0(4(2(0(x1)))) -> 4(2(3(0(4(0(x1))))))
          , 0(4(2(0(x1)))) -> 4(3(0(0(5(2(x1))))))
          , 0(4(2(4(x1)))) -> 4(0(2(3(1(4(x1))))))
          , 0(4(2(4(x1)))) -> 4(0(4(2(0(3(x1))))))
          , 5(1(2(0(x1)))) -> 2(1(3(5(0(x1)))))
          , 5(1(2(0(x1)))) -> 3(1(0(2(5(x1)))))
          , 5(1(2(0(x1)))) -> 2(3(0(0(1(5(x1))))))
          , 5(1(2(4(x1)))) -> 3(2(5(1(4(x1)))))
          , 5(1(2(4(x1)))) -> 5(2(1(3(4(x1)))))
          , 5(1(2(4(x1)))) -> 5(5(2(1(4(x1)))))
          , 5(1(2(4(x1)))) -> 0(3(4(5(2(1(x1))))))
          , 5(1(4(2(x1)))) -> 3(4(5(2(1(x1)))))
          , 5(1(4(2(x1)))) -> 2(1(3(4(5(4(x1))))))
          , 5(1(4(2(x1)))) -> 3(3(4(2(1(5(x1))))))
          , 5(4(1(4(x1)))) -> 3(4(4(1(5(4(x1))))))
          , 5(4(1(4(x1)))) -> 4(1(3(5(0(4(x1))))))
          , 5(4(1(4(x1)))) -> 5(1(3(4(5(4(x1))))))
          , 5(4(1(4(x1)))) -> 5(1(5(3(4(4(x1))))))
          , 5(4(2(0(x1)))) -> 5(4(2(3(0(x1)))))
          , 5(4(2(0(x1)))) -> 0(1(2(3(4(5(x1))))))
          , 5(4(2(0(x1)))) -> 4(5(3(3(0(2(x1))))))
          , 0(1(2(0(4(x1))))) -> 0(2(4(1(3(0(x1))))))
          , 0(1(2(0(4(x1))))) -> 2(0(3(4(0(1(x1))))))
          , 0(1(2(0(4(x1))))) -> 4(0(2(3(1(0(x1))))))
          , 0(1(4(2(2(x1))))) -> 1(2(3(4(0(2(x1))))))
          , 5(0(1(2(4(x1))))) -> 3(0(2(1(4(5(x1))))))
          , 5(1(2(2(4(x1))))) -> 5(2(2(1(4(5(x1))))))
          , 5(1(2(4(0(x1))))) -> 5(0(2(1(3(4(x1))))))
          , 5(1(2(4(0(x1))))) -> 5(0(3(2(1(4(x1))))))
          , 5(1(3(1(4(x1))))) -> 1(5(1(3(4(0(x1))))))
          , 5(1(4(1(2(x1))))) -> 2(1(5(3(4(1(x1))))))
          , 5(4(1(1(4(x1))))) -> 1(1(3(4(5(4(x1))))))
          , 5(4(1(4(0(x1))))) -> 3(4(0(4(5(1(x1))))))
          , 5(4(3(2(0(x1))))) -> 5(4(0(3(2(3(x1))))))
          , 5(4(5(2(0(x1))))) -> 5(0(5(4(4(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(2) -> 32
        , 0_1(5) -> 4
        , 0_1(6) -> 7
        , 0_1(12) -> 11
        , 0_1(13) -> 1
        , 0_1(13) -> 4
        , 0_1(13) -> 11
        , 0_1(13) -> 25
        , 0_1(13) -> 32
        , 0_1(16) -> 3
        , 0_1(18) -> 23
        , 0_1(21) -> 20
        , 0_1(25) -> 24
        , 0_1(27) -> 26
        , 0_1(34) -> 33
        , 0_1(36) -> 28
        , 0_2(18) -> 76
        , 0_2(73) -> 28
        , 0_2(74) -> 82
        , 0_2(76) -> 80
        , 0_2(79) -> 78
        , 0_2(86) -> 85
        , 0_2(88) -> 87
        , 0_2(89) -> 88
        , 1_0(2) -> 2
        , 1_1(2) -> 12
        , 1_1(3) -> 1
        , 1_1(3) -> 4
        , 1_1(3) -> 11
        , 1_1(3) -> 25
        , 1_1(3) -> 32
        , 1_1(6) -> 5
        , 1_1(7) -> 4
        , 1_1(8) -> 1
        , 1_1(8) -> 25
        , 1_1(8) -> 49
        , 1_1(10) -> 9
        , 1_1(21) -> 38
        , 1_1(22) -> 8
        , 1_1(25) -> 53
        , 1_1(26) -> 22
        , 1_1(27) -> 43
        , 1_1(29) -> 28
        , 1_1(49) -> 58
        , 1_1(69) -> 68
        , 1_1(71) -> 70
        , 2_0(2) -> 2
        , 2_1(2) -> 6
        , 2_1(8) -> 1
        , 2_1(8) -> 4
        , 2_1(8) -> 11
        , 2_1(8) -> 25
        , 2_1(8) -> 32
        , 2_1(8) -> 41
        , 2_1(12) -> 47
        , 2_1(14) -> 13
        , 2_1(18) -> 17
        , 2_1(19) -> 3
        , 2_1(23) -> 39
        , 2_1(30) -> 29
        , 2_1(31) -> 30
        , 2_1(35) -> 34
        , 2_1(37) -> 36
        , 2_1(38) -> 44
        , 2_1(41) -> 40
        , 2_1(43) -> 42
        , 2_1(53) -> 52
        , 2_1(68) -> 43
        , 2_2(18) -> 90
        , 2_2(75) -> 74
        , 2_2(77) -> 28
        , 2_2(84) -> 83
        , 3_0(2) -> 2
        , 3_1(2) -> 18
        , 3_1(4) -> 3
        , 3_1(9) -> 8
        , 3_1(11) -> 10
        , 3_1(12) -> 35
        , 3_1(15) -> 14
        , 3_1(20) -> 19
        , 3_1(21) -> 27
        , 3_1(32) -> 31
        , 3_1(38) -> 37
        , 3_1(40) -> 1
        , 3_1(40) -> 25
        , 3_1(40) -> 41
        , 3_1(45) -> 1
        , 3_1(45) -> 13
        , 3_1(45) -> 25
        , 3_1(45) -> 41
        , 3_1(45) -> 49
        , 3_1(48) -> 22
        , 3_1(50) -> 40
        , 3_1(59) -> 29
        , 3_1(62) -> 61
        , 3_1(72) -> 71
        , 3_2(76) -> 75
        , 3_2(78) -> 77
        , 3_2(81) -> 28
        , 3_2(85) -> 84
        , 3_2(87) -> 83
        , 4_0(2) -> 2
        , 4_1(2) -> 21
        , 4_1(7) -> 20
        , 4_1(12) -> 15
        , 4_1(17) -> 16
        , 4_1(21) -> 62
        , 4_1(23) -> 22
        , 4_1(24) -> 20
        , 4_1(25) -> 69
        , 4_1(28) -> 1
        , 4_1(28) -> 4
        , 4_1(28) -> 11
        , 4_1(28) -> 20
        , 4_1(28) -> 25
        , 4_1(28) -> 32
        , 4_1(28) -> 49
        , 4_1(32) -> 72
        , 4_1(39) -> 36
        , 4_1(46) -> 45
        , 4_1(49) -> 48
        , 4_1(52) -> 50
        , 4_1(58) -> 46
        , 4_2(74) -> 73
        , 4_2(76) -> 86
        , 4_2(80) -> 79
        , 4_2(82) -> 81
        , 4_2(83) -> 28
        , 5_0(2) -> 1
        , 5_1(2) -> 25
        , 5_1(8) -> 1
        , 5_1(8) -> 25
        , 5_1(8) -> 49
        , 5_1(14) -> 22
        , 5_1(20) -> 59
        , 5_1(21) -> 49
        , 5_1(33) -> 28
        , 5_1(38) -> 41
        , 5_1(42) -> 1
        , 5_1(42) -> 25
        , 5_1(44) -> 42
        , 5_1(47) -> 46
        , 5_1(61) -> 22
        , 5_1(70) -> 3
        , 5_2(90) -> 89}

Tool RC1

Execution Time	Unknown
Answer	MAYBE
Input	ICFP 2010 212094

stdout:

MAYBE

Tool RC2

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

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(1(2(x1)))) -> 1(3(0(1(2(x1)))))
     , 0(1(1(2(x1)))) -> 1(3(1(0(2(x1)))))
     , 0(1(1(2(x1)))) -> 2(3(1(3(0(1(x1))))))
     , 0(1(2(0(x1)))) -> 1(0(0(2(2(x1)))))
     , 0(1(2(4(x1)))) -> 0(2(3(4(1(x1)))))
     , 0(1(2(4(x1)))) -> 1(0(4(2(3(x1)))))
     , 0(1(2(4(x1)))) -> 1(2(3(0(4(x1)))))
     , 0(1(2(4(x1)))) -> 2(1(4(0(3(x1)))))
     , 0(1(2(4(x1)))) -> 1(2(3(4(0(5(x1))))))
     , 0(1(2(4(x1)))) -> 2(1(1(0(3(4(x1))))))
     , 0(1(2(4(x1)))) -> 4(1(2(2(3(0(x1))))))
     , 0(1(2(4(x1)))) -> 4(5(0(2(3(1(x1))))))
     , 0(4(2(0(x1)))) -> 0(4(2(3(0(x1)))))
     , 0(4(2(0(x1)))) -> 2(3(0(4(0(0(x1))))))
     , 0(4(2(0(x1)))) -> 3(4(0(2(3(0(x1))))))
     , 0(4(2(0(x1)))) -> 4(2(3(0(4(0(x1))))))
     , 0(4(2(0(x1)))) -> 4(3(0(0(5(2(x1))))))
     , 0(4(2(4(x1)))) -> 4(0(2(3(1(4(x1))))))
     , 0(4(2(4(x1)))) -> 4(0(4(2(0(3(x1))))))
     , 5(1(2(0(x1)))) -> 2(1(3(5(0(x1)))))
     , 5(1(2(0(x1)))) -> 3(1(0(2(5(x1)))))
     , 5(1(2(0(x1)))) -> 2(3(0(0(1(5(x1))))))
     , 5(1(2(4(x1)))) -> 3(2(5(1(4(x1)))))
     , 5(1(2(4(x1)))) -> 5(2(1(3(4(x1)))))
     , 5(1(2(4(x1)))) -> 5(5(2(1(4(x1)))))
     , 5(1(2(4(x1)))) -> 0(3(4(5(2(1(x1))))))
     , 5(1(4(2(x1)))) -> 3(4(5(2(1(x1)))))
     , 5(1(4(2(x1)))) -> 2(1(3(4(5(4(x1))))))
     , 5(1(4(2(x1)))) -> 3(3(4(2(1(5(x1))))))
     , 5(4(1(4(x1)))) -> 3(4(4(1(5(4(x1))))))
     , 5(4(1(4(x1)))) -> 4(1(3(5(0(4(x1))))))
     , 5(4(1(4(x1)))) -> 5(1(3(4(5(4(x1))))))
     , 5(4(1(4(x1)))) -> 5(1(5(3(4(4(x1))))))
     , 5(4(2(0(x1)))) -> 5(4(2(3(0(x1)))))
     , 5(4(2(0(x1)))) -> 0(1(2(3(4(5(x1))))))
     , 5(4(2(0(x1)))) -> 4(5(3(3(0(2(x1))))))
     , 0(1(2(0(4(x1))))) -> 0(2(4(1(3(0(x1))))))
     , 0(1(2(0(4(x1))))) -> 2(0(3(4(0(1(x1))))))
     , 0(1(2(0(4(x1))))) -> 4(0(2(3(1(0(x1))))))
     , 0(1(4(2(2(x1))))) -> 1(2(3(4(0(2(x1))))))
     , 5(0(1(2(4(x1))))) -> 3(0(2(1(4(5(x1))))))
     , 5(1(2(2(4(x1))))) -> 5(2(2(1(4(5(x1))))))
     , 5(1(2(4(0(x1))))) -> 5(0(2(1(3(4(x1))))))
     , 5(1(2(4(0(x1))))) -> 5(0(3(2(1(4(x1))))))
     , 5(1(3(1(4(x1))))) -> 1(5(1(3(4(0(x1))))))
     , 5(1(4(1(2(x1))))) -> 2(1(5(3(4(1(x1))))))
     , 5(4(1(1(4(x1))))) -> 1(1(3(4(5(4(x1))))))
     , 5(4(1(4(0(x1))))) -> 3(4(0(4(5(1(x1))))))
     , 5(4(3(2(0(x1))))) -> 5(4(0(3(2(3(x1))))))
     , 5(4(5(2(0(x1))))) -> 5(0(5(4(4(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(1(2(x1)))) -> 1(3(0(1(2(x1)))))
          , 0(1(1(2(x1)))) -> 1(3(1(0(2(x1)))))
          , 0(1(1(2(x1)))) -> 2(3(1(3(0(1(x1))))))
          , 0(1(2(0(x1)))) -> 1(0(0(2(2(x1)))))
          , 0(1(2(4(x1)))) -> 0(2(3(4(1(x1)))))
          , 0(1(2(4(x1)))) -> 1(0(4(2(3(x1)))))
          , 0(1(2(4(x1)))) -> 1(2(3(0(4(x1)))))
          , 0(1(2(4(x1)))) -> 2(1(4(0(3(x1)))))
          , 0(1(2(4(x1)))) -> 1(2(3(4(0(5(x1))))))
          , 0(1(2(4(x1)))) -> 2(1(1(0(3(4(x1))))))
          , 0(1(2(4(x1)))) -> 4(1(2(2(3(0(x1))))))
          , 0(1(2(4(x1)))) -> 4(5(0(2(3(1(x1))))))
          , 0(4(2(0(x1)))) -> 0(4(2(3(0(x1)))))
          , 0(4(2(0(x1)))) -> 2(3(0(4(0(0(x1))))))
          , 0(4(2(0(x1)))) -> 3(4(0(2(3(0(x1))))))
          , 0(4(2(0(x1)))) -> 4(2(3(0(4(0(x1))))))
          , 0(4(2(0(x1)))) -> 4(3(0(0(5(2(x1))))))
          , 0(4(2(4(x1)))) -> 4(0(2(3(1(4(x1))))))
          , 0(4(2(4(x1)))) -> 4(0(4(2(0(3(x1))))))
          , 5(1(2(0(x1)))) -> 2(1(3(5(0(x1)))))
          , 5(1(2(0(x1)))) -> 3(1(0(2(5(x1)))))
          , 5(1(2(0(x1)))) -> 2(3(0(0(1(5(x1))))))
          , 5(1(2(4(x1)))) -> 3(2(5(1(4(x1)))))
          , 5(1(2(4(x1)))) -> 5(2(1(3(4(x1)))))
          , 5(1(2(4(x1)))) -> 5(5(2(1(4(x1)))))
          , 5(1(2(4(x1)))) -> 0(3(4(5(2(1(x1))))))
          , 5(1(4(2(x1)))) -> 3(4(5(2(1(x1)))))
          , 5(1(4(2(x1)))) -> 2(1(3(4(5(4(x1))))))
          , 5(1(4(2(x1)))) -> 3(3(4(2(1(5(x1))))))
          , 5(4(1(4(x1)))) -> 3(4(4(1(5(4(x1))))))
          , 5(4(1(4(x1)))) -> 4(1(3(5(0(4(x1))))))
          , 5(4(1(4(x1)))) -> 5(1(3(4(5(4(x1))))))
          , 5(4(1(4(x1)))) -> 5(1(5(3(4(4(x1))))))
          , 5(4(2(0(x1)))) -> 5(4(2(3(0(x1)))))
          , 5(4(2(0(x1)))) -> 0(1(2(3(4(5(x1))))))
          , 5(4(2(0(x1)))) -> 4(5(3(3(0(2(x1))))))
          , 0(1(2(0(4(x1))))) -> 0(2(4(1(3(0(x1))))))
          , 0(1(2(0(4(x1))))) -> 2(0(3(4(0(1(x1))))))
          , 0(1(2(0(4(x1))))) -> 4(0(2(3(1(0(x1))))))
          , 0(1(4(2(2(x1))))) -> 1(2(3(4(0(2(x1))))))
          , 5(0(1(2(4(x1))))) -> 3(0(2(1(4(5(x1))))))
          , 5(1(2(2(4(x1))))) -> 5(2(2(1(4(5(x1))))))
          , 5(1(2(4(0(x1))))) -> 5(0(2(1(3(4(x1))))))
          , 5(1(2(4(0(x1))))) -> 5(0(3(2(1(4(x1))))))
          , 5(1(3(1(4(x1))))) -> 1(5(1(3(4(0(x1))))))
          , 5(1(4(1(2(x1))))) -> 2(1(5(3(4(1(x1))))))
          , 5(4(1(1(4(x1))))) -> 1(1(3(4(5(4(x1))))))
          , 5(4(1(4(0(x1))))) -> 3(4(0(4(5(1(x1))))))
          , 5(4(3(2(0(x1))))) -> 5(4(0(3(2(3(x1))))))
          , 5(4(5(2(0(x1))))) -> 5(0(5(4(4(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(2) -> 32
        , 0_1(5) -> 4
        , 0_1(6) -> 7
        , 0_1(12) -> 11
        , 0_1(13) -> 1
        , 0_1(13) -> 4
        , 0_1(13) -> 11
        , 0_1(13) -> 25
        , 0_1(13) -> 32
        , 0_1(16) -> 3
        , 0_1(18) -> 23
        , 0_1(21) -> 20
        , 0_1(25) -> 24
        , 0_1(27) -> 26
        , 0_1(34) -> 33
        , 0_1(36) -> 28
        , 0_2(18) -> 76
        , 0_2(73) -> 28
        , 0_2(74) -> 82
        , 0_2(76) -> 80
        , 0_2(79) -> 78
        , 0_2(86) -> 85
        , 0_2(88) -> 87
        , 0_2(89) -> 88
        , 1_0(2) -> 2
        , 1_1(2) -> 12
        , 1_1(3) -> 1
        , 1_1(3) -> 4
        , 1_1(3) -> 11
        , 1_1(3) -> 25
        , 1_1(3) -> 32
        , 1_1(6) -> 5
        , 1_1(7) -> 4
        , 1_1(8) -> 1
        , 1_1(8) -> 25
        , 1_1(8) -> 49
        , 1_1(10) -> 9
        , 1_1(21) -> 38
        , 1_1(22) -> 8
        , 1_1(25) -> 53
        , 1_1(26) -> 22
        , 1_1(27) -> 43
        , 1_1(29) -> 28
        , 1_1(49) -> 58
        , 1_1(69) -> 68
        , 1_1(71) -> 70
        , 2_0(2) -> 2
        , 2_1(2) -> 6
        , 2_1(8) -> 1
        , 2_1(8) -> 4
        , 2_1(8) -> 11
        , 2_1(8) -> 25
        , 2_1(8) -> 32
        , 2_1(8) -> 41
        , 2_1(12) -> 47
        , 2_1(14) -> 13
        , 2_1(18) -> 17
        , 2_1(19) -> 3
        , 2_1(23) -> 39
        , 2_1(30) -> 29
        , 2_1(31) -> 30
        , 2_1(35) -> 34
        , 2_1(37) -> 36
        , 2_1(38) -> 44
        , 2_1(41) -> 40
        , 2_1(43) -> 42
        , 2_1(53) -> 52
        , 2_1(68) -> 43
        , 2_2(18) -> 90
        , 2_2(75) -> 74
        , 2_2(77) -> 28
        , 2_2(84) -> 83
        , 3_0(2) -> 2
        , 3_1(2) -> 18
        , 3_1(4) -> 3
        , 3_1(9) -> 8
        , 3_1(11) -> 10
        , 3_1(12) -> 35
        , 3_1(15) -> 14
        , 3_1(20) -> 19
        , 3_1(21) -> 27
        , 3_1(32) -> 31
        , 3_1(38) -> 37
        , 3_1(40) -> 1
        , 3_1(40) -> 25
        , 3_1(40) -> 41
        , 3_1(45) -> 1
        , 3_1(45) -> 13
        , 3_1(45) -> 25
        , 3_1(45) -> 41
        , 3_1(45) -> 49
        , 3_1(48) -> 22
        , 3_1(50) -> 40
        , 3_1(59) -> 29
        , 3_1(62) -> 61
        , 3_1(72) -> 71
        , 3_2(76) -> 75
        , 3_2(78) -> 77
        , 3_2(81) -> 28
        , 3_2(85) -> 84
        , 3_2(87) -> 83
        , 4_0(2) -> 2
        , 4_1(2) -> 21
        , 4_1(7) -> 20
        , 4_1(12) -> 15
        , 4_1(17) -> 16
        , 4_1(21) -> 62
        , 4_1(23) -> 22
        , 4_1(24) -> 20
        , 4_1(25) -> 69
        , 4_1(28) -> 1
        , 4_1(28) -> 4
        , 4_1(28) -> 11
        , 4_1(28) -> 20
        , 4_1(28) -> 25
        , 4_1(28) -> 32
        , 4_1(28) -> 49
        , 4_1(32) -> 72
        , 4_1(39) -> 36
        , 4_1(46) -> 45
        , 4_1(49) -> 48
        , 4_1(52) -> 50
        , 4_1(58) -> 46
        , 4_2(74) -> 73
        , 4_2(76) -> 86
        , 4_2(80) -> 79
        , 4_2(82) -> 81
        , 4_2(83) -> 28
        , 5_0(2) -> 1
        , 5_1(2) -> 25
        , 5_1(8) -> 1
        , 5_1(8) -> 25
        , 5_1(8) -> 49
        , 5_1(14) -> 22
        , 5_1(20) -> 59
        , 5_1(21) -> 49
        , 5_1(33) -> 28
        , 5_1(38) -> 41
        , 5_1(42) -> 1
        , 5_1(42) -> 25
        , 5_1(44) -> 42
        , 5_1(47) -> 46
        , 5_1(61) -> 22
        , 5_1(70) -> 3
        , 5_2(90) -> 89}