Problem ICFP 2010 26103

Tool Bounds

Execution Time0.58957195ms
Answer
YES(?,O(n^1))
InputICFP 2010 26103

stdout:

YES(?,O(n^1))

We consider the following Problem:

  Strict Trs:
    {  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(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(x1)))))))))))))
     , 0(1(2(1(x1)))) -> 1(2(1(1(0(1(2(0(1(2(x1))))))))))}
  StartTerms: all
  Strategy: none

Certificate: YES(?,O(n^1))

Proof:
  The problem is match-bounded by 3.
  The enriched problem is compatible with the following automaton:
  {  1_0(1) -> 1
   , 1_1(2) -> 1
   , 1_1(2) -> 20
   , 1_1(4) -> 3
   , 1_1(5) -> 4
   , 1_1(7) -> 6
   , 1_1(8) -> 4
   , 1_1(10) -> 9
   , 1_1(11) -> 4
   , 1_1(13) -> 12
   , 1_1(14) -> 4
   , 1_1(16) -> 15
   , 1_1(17) -> 4
   , 1_1(19) -> 18
   , 1_1(22) -> 21
   , 1_2(17) -> 44
   , 1_2(25) -> 5
   , 1_2(25) -> 8
   , 1_2(25) -> 11
   , 1_2(25) -> 14
   , 1_2(25) -> 17
   , 1_2(25) -> 20
   , 1_2(27) -> 26
   , 1_2(28) -> 27
   , 1_2(30) -> 29
   , 1_2(31) -> 45
   , 1_2(33) -> 32
   , 1_2(34) -> 45
   , 1_2(36) -> 35
   , 1_2(37) -> 45
   , 1_2(39) -> 38
   , 1_2(42) -> 41
   , 1_2(43) -> 5
   , 1_2(43) -> 8
   , 1_2(43) -> 11
   , 1_2(43) -> 14
   , 1_2(43) -> 17
   , 1_2(43) -> 20
   , 1_2(45) -> 44
   , 1_2(46) -> 5
   , 1_2(46) -> 8
   , 1_2(46) -> 11
   , 1_2(46) -> 14
   , 1_2(46) -> 17
   , 1_2(48) -> 47
   , 1_2(49) -> 48
   , 1_2(51) -> 50
   , 1_2(52) -> 48
   , 1_2(54) -> 53
   , 1_2(55) -> 27
   , 1_2(57) -> 56
   , 1_2(60) -> 5
   , 1_2(60) -> 8
   , 1_2(60) -> 11
   , 1_2(60) -> 14
   , 1_2(62) -> 61
   , 1_2(63) -> 62
   , 1_2(65) -> 64
   , 1_2(66) -> 62
   , 1_2(68) -> 67
   , 1_2(277) -> 276
   , 1_2(278) -> 17
   , 1_2(280) -> 279
   , 1_2(281) -> 5
   , 1_2(281) -> 8
   , 1_2(281) -> 11
   , 1_2(283) -> 282
   , 1_2(284) -> 283
   , 1_2(286) -> 285
   , 1_2(287) -> 283
   , 1_2(289) -> 288
   , 1_2(290) -> 283
   , 1_2(292) -> 291
   , 1_2(293) -> 48
   , 1_2(295) -> 294
   , 1_2(296) -> 48
   , 1_2(298) -> 297
   , 1_2(301) -> 300
   , 1_2(323) -> 5
   , 1_2(323) -> 8
   , 1_2(325) -> 324
   , 1_2(326) -> 325
   , 1_2(328) -> 327
   , 1_2(329) -> 325
   , 1_2(331) -> 330
   , 1_2(332) -> 325
   , 1_2(334) -> 333
   , 1_2(335) -> 62
   , 1_2(337) -> 336
   , 1_2(340) -> 339
   , 1_3(302) -> 28
   , 1_3(302) -> 31
   , 1_3(302) -> 34
   , 1_3(302) -> 37
   , 1_3(302) -> 40
   , 1_3(304) -> 303
   , 1_3(305) -> 304
   , 1_3(307) -> 306
   , 1_3(308) -> 343
   , 1_3(310) -> 309
   , 1_3(311) -> 343
   , 1_3(313) -> 312
   , 1_3(314) -> 343
   , 1_3(316) -> 315
   , 1_3(317) -> 343
   , 1_3(319) -> 318
   , 1_3(322) -> 321
   , 1_3(341) -> 28
   , 1_3(341) -> 31
   , 1_3(341) -> 34
   , 1_3(341) -> 37
   , 1_3(341) -> 40
   , 1_3(343) -> 342
   , 1_3(344) -> 343
   , 1_3(346) -> 345
   , 1_3(347) -> 343
   , 1_3(349) -> 348
   , 1_3(350) -> 343
   , 1_3(352) -> 351
   , 1_3(353) -> 343
   , 1_3(355) -> 354
   , 1_3(358) -> 357
   , 1_3(359) -> 28
   , 1_3(359) -> 31
   , 1_3(359) -> 34
   , 1_3(359) -> 37
   , 1_3(361) -> 360
   , 1_3(362) -> 361
   , 1_3(364) -> 363
   , 1_3(365) -> 361
   , 1_3(367) -> 366
   , 1_3(368) -> 343
   , 1_3(370) -> 369
   , 1_3(371) -> 343
   , 1_3(373) -> 372
   , 1_3(376) -> 375
   , 2_0(1) -> 1
   , 2_1(1) -> 22
   , 2_1(2) -> 19
   , 2_1(3) -> 2
   , 2_1(4) -> 19
   , 2_1(5) -> 7
   , 2_1(8) -> 7
   , 2_1(11) -> 10
   , 2_1(14) -> 13
   , 2_1(17) -> 16
   , 2_1(20) -> 19
   , 2_2(2) -> 42
   , 2_2(5) -> 42
   , 2_2(8) -> 42
   , 2_2(11) -> 39
   , 2_2(14) -> 36
   , 2_2(17) -> 30
   , 2_2(25) -> 42
   , 2_2(26) -> 25
   , 2_2(28) -> 33
   , 2_2(31) -> 30
   , 2_2(34) -> 33
   , 2_2(37) -> 36
   , 2_2(40) -> 39
   , 2_2(43) -> 57
   , 2_2(44) -> 43
   , 2_2(46) -> 68
   , 2_2(47) -> 46
   , 2_2(49) -> 57
   , 2_2(52) -> 51
   , 2_2(55) -> 54
   , 2_2(60) -> 301
   , 2_2(61) -> 60
   , 2_2(63) -> 280
   , 2_2(66) -> 65
   , 2_2(278) -> 277
   , 2_2(281) -> 340
   , 2_2(282) -> 281
   , 2_2(287) -> 286
   , 2_2(290) -> 289
   , 2_2(293) -> 292
   , 2_2(296) -> 295
   , 2_2(299) -> 298
   , 2_2(323) -> 337
   , 2_2(324) -> 323
   , 2_2(326) -> 65
   , 2_2(329) -> 328
   , 2_2(332) -> 331
   , 2_2(335) -> 334
   , 2_2(338) -> 337
   , 2_3(25) -> 358
   , 2_3(43) -> 358
   , 2_3(46) -> 322
   , 2_3(60) -> 322
   , 2_3(278) -> 313
   , 2_3(281) -> 319
   , 2_3(302) -> 376
   , 2_3(303) -> 302
   , 2_3(305) -> 313
   , 2_3(308) -> 307
   , 2_3(311) -> 310
   , 2_3(314) -> 313
   , 2_3(317) -> 316
   , 2_3(320) -> 319
   , 2_3(323) -> 316
   , 2_3(341) -> 373
   , 2_3(342) -> 341
   , 2_3(344) -> 310
   , 2_3(347) -> 346
   , 2_3(350) -> 349
   , 2_3(353) -> 352
   , 2_3(356) -> 355
   , 2_3(359) -> 319
   , 2_3(360) -> 359
   , 2_3(362) -> 310
   , 2_3(365) -> 364
   , 2_3(368) -> 367
   , 2_3(371) -> 370
   , 2_3(374) -> 373
   , 0_0(1) -> 1
   , 0_1(6) -> 5
   , 0_1(9) -> 8
   , 0_1(12) -> 11
   , 0_1(15) -> 14
   , 0_1(18) -> 17
   , 0_1(21) -> 20
   , 0_2(29) -> 28
   , 0_2(32) -> 31
   , 0_2(35) -> 34
   , 0_2(38) -> 37
   , 0_2(41) -> 40
   , 0_2(50) -> 49
   , 0_2(53) -> 52
   , 0_2(56) -> 55
   , 0_2(64) -> 63
   , 0_2(67) -> 66
   , 0_2(276) -> 46
   , 0_2(279) -> 278
   , 0_2(285) -> 284
   , 0_2(288) -> 287
   , 0_2(291) -> 290
   , 0_2(294) -> 293
   , 0_2(297) -> 296
   , 0_2(300) -> 299
   , 0_2(327) -> 326
   , 0_2(330) -> 329
   , 0_2(333) -> 332
   , 0_2(336) -> 335
   , 0_2(339) -> 338
   , 0_3(306) -> 305
   , 0_3(309) -> 308
   , 0_3(312) -> 311
   , 0_3(315) -> 314
   , 0_3(318) -> 317
   , 0_3(321) -> 320
   , 0_3(345) -> 344
   , 0_3(348) -> 347
   , 0_3(351) -> 350
   , 0_3(354) -> 353
   , 0_3(357) -> 356
   , 0_3(363) -> 362
   , 0_3(366) -> 365
   , 0_3(369) -> 368
   , 0_3(372) -> 371
   , 0_3(375) -> 374}

Hurray, we answered YES(?,O(n^1))

Tool EDA

Execution Time60.056007ms
Answer
TIMEOUT
InputICFP 2010 26103

stdout:

TIMEOUT

We consider the following Problem:

  Strict Trs:
    {  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(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(x1)))))))))))))
     , 0(1(2(1(x1)))) -> 1(2(1(1(0(1(2(0(1(2(x1))))))))))}
  StartTerms: all
  Strategy: none

Certificate: TIMEOUT

Proof:
  Computation stopped due to timeout after 60.0 seconds.

Arrrr..

Tool IDA

Execution Time60.302017ms
Answer
TIMEOUT
InputICFP 2010 26103

stdout:

TIMEOUT

We consider the following Problem:

  Strict Trs:
    {  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(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(x1)))))))))))))
     , 0(1(2(1(x1)))) -> 1(2(1(1(0(1(2(0(1(2(x1))))))))))}
  StartTerms: all
  Strategy: none

Certificate: TIMEOUT

Proof:
  Computation stopped due to timeout after 60.0 seconds.

Arrrr..

Tool TRI

Execution Time60.040077ms
Answer
TIMEOUT
InputICFP 2010 26103

stdout:

TIMEOUT

We consider the following Problem:

  Strict Trs:
    {  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(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(x1)))))))))))))
     , 0(1(2(1(x1)))) -> 1(2(1(1(0(1(2(0(1(2(x1))))))))))}
  StartTerms: all
  Strategy: none

Certificate: TIMEOUT

Proof:
  Computation stopped due to timeout after 60.0 seconds.

Arrrr..

Tool TRI2

Execution Time13.1724615ms
Answer
MAYBE
InputICFP 2010 26103

stdout:

MAYBE

We consider the following Problem:

  Strict Trs:
    {  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(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(x1)))))))))))))
     , 0(1(2(1(x1)))) -> 1(2(1(1(0(1(2(0(1(2(x1))))))))))}
  StartTerms: all
  Strategy: none

Certificate: MAYBE

Proof:
  The input cannot be shown compatible

Arrrr..