Tool Bounds
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(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(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) -> 23
, 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(20) -> 4
, 1_1(22) -> 21
, 1_1(25) -> 24
, 1_2(17) -> 86
, 1_2(28) -> 5
, 1_2(28) -> 8
, 1_2(28) -> 11
, 1_2(28) -> 14
, 1_2(28) -> 17
, 1_2(28) -> 20
, 1_2(28) -> 23
, 1_2(30) -> 29
, 1_2(31) -> 30
, 1_2(33) -> 32
, 1_2(34) -> 51
, 1_2(36) -> 35
, 1_2(37) -> 51
, 1_2(39) -> 38
, 1_2(40) -> 51
, 1_2(42) -> 41
, 1_2(43) -> 51
, 1_2(45) -> 44
, 1_2(48) -> 47
, 1_2(49) -> 5
, 1_2(49) -> 8
, 1_2(49) -> 11
, 1_2(49) -> 14
, 1_2(49) -> 17
, 1_2(49) -> 20
, 1_2(49) -> 23
, 1_2(51) -> 50
, 1_2(52) -> 5
, 1_2(52) -> 8
, 1_2(52) -> 11
, 1_2(52) -> 14
, 1_2(52) -> 17
, 1_2(52) -> 20
, 1_2(54) -> 53
, 1_2(55) -> 54
, 1_2(57) -> 56
, 1_2(58) -> 54
, 1_2(60) -> 59
, 1_2(61) -> 54
, 1_2(63) -> 62
, 1_2(66) -> 65
, 1_2(69) -> 5
, 1_2(69) -> 8
, 1_2(69) -> 11
, 1_2(69) -> 14
, 1_2(69) -> 17
, 1_2(71) -> 70
, 1_2(72) -> 71
, 1_2(74) -> 73
, 1_2(75) -> 71
, 1_2(77) -> 76
, 1_2(78) -> 51
, 1_2(80) -> 79
, 1_2(85) -> 5
, 1_2(85) -> 8
, 1_2(85) -> 11
, 1_2(85) -> 14
, 1_2(85) -> 17
, 1_2(87) -> 86
, 1_2(88) -> 87
, 1_2(90) -> 89
, 1_2(91) -> 87
, 1_2(93) -> 92
, 1_2(478) -> 477
, 1_2(484) -> 483
, 1_2(485) -> 17
, 1_2(487) -> 486
, 1_2(488) -> 17
, 1_2(490) -> 489
, 1_2(491) -> 5
, 1_2(491) -> 8
, 1_2(491) -> 11
, 1_2(491) -> 14
, 1_2(493) -> 492
, 1_2(494) -> 493
, 1_2(496) -> 495
, 1_2(497) -> 493
, 1_2(499) -> 498
, 1_2(500) -> 493
, 1_2(502) -> 501
, 1_2(503) -> 493
, 1_2(505) -> 504
, 1_2(506) -> 71
, 1_2(508) -> 507
, 1_2(509) -> 17
, 1_2(511) -> 510
, 1_2(514) -> 513
, 1_2(553) -> 5
, 1_2(553) -> 8
, 1_2(553) -> 11
, 1_2(553) -> 14
, 1_2(555) -> 554
, 1_2(556) -> 555
, 1_2(558) -> 557
, 1_2(559) -> 555
, 1_2(561) -> 560
, 1_2(562) -> 555
, 1_2(564) -> 563
, 1_2(565) -> 555
, 1_2(567) -> 566
, 1_2(568) -> 17
, 1_2(570) -> 569
, 1_2(573) -> 572
, 1_3(94) -> 31
, 1_3(94) -> 34
, 1_3(94) -> 37
, 1_3(94) -> 40
, 1_3(94) -> 43
, 1_3(94) -> 46
, 1_3(96) -> 95
, 1_3(97) -> 96
, 1_3(99) -> 98
, 1_3(102) -> 101
, 1_3(515) -> 31
, 1_3(515) -> 34
, 1_3(515) -> 37
, 1_3(515) -> 40
, 1_3(515) -> 43
, 1_3(515) -> 46
, 1_3(517) -> 516
, 1_3(518) -> 517
, 1_3(520) -> 519
, 1_3(521) -> 576
, 1_3(523) -> 522
, 1_3(524) -> 576
, 1_3(526) -> 525
, 1_3(527) -> 576
, 1_3(529) -> 528
, 1_3(530) -> 576
, 1_3(532) -> 531
, 1_3(533) -> 576
, 1_3(535) -> 534
, 1_3(538) -> 537
, 1_3(574) -> 31
, 1_3(574) -> 34
, 1_3(574) -> 37
, 1_3(574) -> 40
, 1_3(574) -> 43
, 1_3(574) -> 46
, 1_3(576) -> 575
, 1_3(577) -> 576
, 1_3(579) -> 578
, 1_3(580) -> 576
, 1_3(582) -> 581
, 1_3(583) -> 576
, 1_3(585) -> 584
, 1_3(586) -> 576
, 1_3(588) -> 587
, 1_3(589) -> 576
, 1_3(591) -> 590
, 1_3(594) -> 593
, 1_3(595) -> 31
, 1_3(595) -> 34
, 1_3(595) -> 37
, 1_3(595) -> 40
, 1_3(595) -> 43
, 1_3(597) -> 596
, 1_3(598) -> 597
, 1_3(600) -> 599
, 1_3(601) -> 597
, 1_3(603) -> 602
, 1_3(604) -> 576
, 1_3(606) -> 605
, 1_3(607) -> 576
, 1_3(609) -> 608
, 1_3(610) -> 576
, 1_3(612) -> 611
, 1_3(615) -> 614
, 2_0(1) -> 1
, 2_1(1) -> 25
, 2_1(2) -> 22
, 2_1(3) -> 2
, 2_1(4) -> 22
, 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_1(23) -> 22
, 2_2(2) -> 48
, 2_2(5) -> 48
, 2_2(8) -> 48
, 2_2(11) -> 45
, 2_2(14) -> 42
, 2_2(17) -> 39
, 2_2(20) -> 33
, 2_2(28) -> 48
, 2_2(29) -> 28
, 2_2(31) -> 36
, 2_2(34) -> 33
, 2_2(37) -> 36
, 2_2(40) -> 39
, 2_2(43) -> 42
, 2_2(46) -> 45
, 2_2(49) -> 66
, 2_2(50) -> 49
, 2_2(52) -> 80
, 2_2(53) -> 52
, 2_2(55) -> 63
, 2_2(58) -> 57
, 2_2(61) -> 60
, 2_2(64) -> 63
, 2_2(69) -> 93
, 2_2(70) -> 69
, 2_2(72) -> 478
, 2_2(75) -> 74
, 2_2(78) -> 77
, 2_2(85) -> 514
, 2_2(86) -> 85
, 2_2(88) -> 490
, 2_2(91) -> 90
, 2_2(485) -> 484
, 2_2(488) -> 487
, 2_2(491) -> 573
, 2_2(492) -> 491
, 2_2(494) -> 33
, 2_2(497) -> 496
, 2_2(500) -> 499
, 2_2(503) -> 502
, 2_2(506) -> 505
, 2_2(509) -> 508
, 2_2(512) -> 511
, 2_2(553) -> 570
, 2_2(554) -> 553
, 2_2(556) -> 90
, 2_2(559) -> 558
, 2_2(562) -> 561
, 2_2(565) -> 564
, 2_2(568) -> 567
, 2_2(571) -> 570
, 2_3(28) -> 594
, 2_3(49) -> 594
, 2_3(52) -> 538
, 2_3(69) -> 102
, 2_3(85) -> 102
, 2_3(94) -> 102
, 2_3(95) -> 94
, 2_3(97) -> 532
, 2_3(100) -> 99
, 2_3(485) -> 99
, 2_3(488) -> 99
, 2_3(491) -> 99
, 2_3(509) -> 99
, 2_3(515) -> 615
, 2_3(516) -> 515
, 2_3(518) -> 99
, 2_3(521) -> 520
, 2_3(524) -> 523
, 2_3(527) -> 526
, 2_3(530) -> 529
, 2_3(533) -> 532
, 2_3(536) -> 535
, 2_3(553) -> 99
, 2_3(568) -> 99
, 2_3(574) -> 612
, 2_3(575) -> 574
, 2_3(577) -> 523
, 2_3(580) -> 579
, 2_3(583) -> 582
, 2_3(586) -> 585
, 2_3(589) -> 588
, 2_3(592) -> 591
, 2_3(595) -> 99
, 2_3(596) -> 595
, 2_3(598) -> 520
, 2_3(601) -> 600
, 2_3(604) -> 603
, 2_3(607) -> 606
, 2_3(610) -> 609
, 2_3(613) -> 612
, 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_1(24) -> 23
, 0_2(32) -> 31
, 0_2(35) -> 34
, 0_2(38) -> 37
, 0_2(41) -> 40
, 0_2(44) -> 43
, 0_2(47) -> 46
, 0_2(56) -> 55
, 0_2(59) -> 58
, 0_2(62) -> 61
, 0_2(65) -> 64
, 0_2(73) -> 72
, 0_2(76) -> 75
, 0_2(79) -> 78
, 0_2(89) -> 88
, 0_2(92) -> 91
, 0_2(477) -> 52
, 0_2(483) -> 69
, 0_2(486) -> 485
, 0_2(489) -> 488
, 0_2(495) -> 494
, 0_2(498) -> 497
, 0_2(501) -> 500
, 0_2(504) -> 503
, 0_2(507) -> 506
, 0_2(510) -> 509
, 0_2(513) -> 512
, 0_2(557) -> 556
, 0_2(560) -> 559
, 0_2(563) -> 562
, 0_2(566) -> 565
, 0_2(569) -> 568
, 0_2(572) -> 571
, 0_3(98) -> 97
, 0_3(101) -> 100
, 0_3(519) -> 518
, 0_3(522) -> 521
, 0_3(525) -> 524
, 0_3(528) -> 527
, 0_3(531) -> 530
, 0_3(534) -> 533
, 0_3(537) -> 536
, 0_3(578) -> 577
, 0_3(581) -> 580
, 0_3(584) -> 583
, 0_3(587) -> 586
, 0_3(590) -> 589
, 0_3(593) -> 592
, 0_3(599) -> 598
, 0_3(602) -> 601
, 0_3(605) -> 604
, 0_3(608) -> 607
, 0_3(611) -> 610
, 0_3(614) -> 613}
Hurray, we answered YES(?,O(n^1))Tool EDA
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(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(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
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(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(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
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(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(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
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(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(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..