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(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(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) -> 26
, 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(23) -> 4
, 1_1(25) -> 24
, 1_1(28) -> 27
, 1_2(17) -> 121
, 1_2(31) -> 5
, 1_2(31) -> 8
, 1_2(31) -> 11
, 1_2(31) -> 14
, 1_2(31) -> 17
, 1_2(31) -> 20
, 1_2(31) -> 23
, 1_2(31) -> 26
, 1_2(33) -> 32
, 1_2(34) -> 33
, 1_2(36) -> 35
, 1_2(37) -> 57
, 1_2(39) -> 38
, 1_2(40) -> 57
, 1_2(42) -> 41
, 1_2(43) -> 57
, 1_2(45) -> 44
, 1_2(46) -> 57
, 1_2(48) -> 47
, 1_2(49) -> 57
, 1_2(51) -> 50
, 1_2(54) -> 53
, 1_2(55) -> 5
, 1_2(55) -> 8
, 1_2(55) -> 11
, 1_2(55) -> 14
, 1_2(55) -> 17
, 1_2(55) -> 20
, 1_2(55) -> 23
, 1_2(55) -> 26
, 1_2(57) -> 56
, 1_2(58) -> 5
, 1_2(58) -> 8
, 1_2(58) -> 11
, 1_2(58) -> 14
, 1_2(58) -> 17
, 1_2(58) -> 20
, 1_2(58) -> 23
, 1_2(60) -> 59
, 1_2(61) -> 60
, 1_2(63) -> 62
, 1_2(64) -> 60
, 1_2(66) -> 65
, 1_2(67) -> 60
, 1_2(69) -> 68
, 1_2(70) -> 60
, 1_2(72) -> 71
, 1_2(75) -> 74
, 1_2(78) -> 5
, 1_2(78) -> 8
, 1_2(78) -> 11
, 1_2(78) -> 14
, 1_2(78) -> 17
, 1_2(78) -> 20
, 1_2(80) -> 79
, 1_2(81) -> 80
, 1_2(83) -> 82
, 1_2(84) -> 80
, 1_2(86) -> 85
, 1_2(87) -> 80
, 1_2(89) -> 88
, 1_2(90) -> 57
, 1_2(92) -> 91
, 1_2(102) -> 5
, 1_2(102) -> 8
, 1_2(102) -> 11
, 1_2(102) -> 14
, 1_2(102) -> 17
, 1_2(104) -> 103
, 1_2(105) -> 104
, 1_2(107) -> 106
, 1_2(108) -> 104
, 1_2(110) -> 109
, 1_2(111) -> 104
, 1_2(113) -> 112
, 1_2(120) -> 5
, 1_2(120) -> 8
, 1_2(120) -> 11
, 1_2(120) -> 14
, 1_2(120) -> 17
, 1_2(122) -> 121
, 1_2(123) -> 122
, 1_2(125) -> 124
, 1_2(126) -> 122
, 1_2(128) -> 127
, 1_2(749) -> 748
, 1_2(750) -> 17
, 1_2(758) -> 757
, 1_2(764) -> 763
, 1_2(765) -> 17
, 1_2(767) -> 766
, 1_2(768) -> 17
, 1_2(770) -> 769
, 1_2(771) -> 17
, 1_2(773) -> 772
, 1_2(774) -> 5
, 1_2(774) -> 8
, 1_2(774) -> 11
, 1_2(774) -> 14
, 1_2(776) -> 775
, 1_2(777) -> 776
, 1_2(779) -> 778
, 1_2(780) -> 776
, 1_2(782) -> 781
, 1_2(783) -> 776
, 1_2(785) -> 784
, 1_2(786) -> 776
, 1_2(788) -> 787
, 1_2(789) -> 776
, 1_2(791) -> 790
, 1_2(792) -> 104
, 1_2(794) -> 793
, 1_2(795) -> 17
, 1_2(797) -> 796
, 1_2(800) -> 799
, 1_2(862) -> 5
, 1_2(862) -> 8
, 1_2(862) -> 11
, 1_2(862) -> 14
, 1_2(864) -> 863
, 1_2(865) -> 864
, 1_2(867) -> 866
, 1_2(868) -> 864
, 1_2(870) -> 869
, 1_2(871) -> 864
, 1_2(873) -> 872
, 1_2(874) -> 864
, 1_2(876) -> 875
, 1_2(877) -> 864
, 1_2(879) -> 878
, 1_2(880) -> 17
, 1_2(882) -> 881
, 1_2(885) -> 884
, 1_3(129) -> 34
, 1_3(129) -> 37
, 1_3(129) -> 40
, 1_3(129) -> 43
, 1_3(129) -> 46
, 1_3(129) -> 49
, 1_3(129) -> 52
, 1_3(131) -> 130
, 1_3(132) -> 131
, 1_3(134) -> 133
, 1_3(137) -> 136
, 1_3(801) -> 34
, 1_3(801) -> 37
, 1_3(801) -> 40
, 1_3(801) -> 43
, 1_3(801) -> 46
, 1_3(801) -> 49
, 1_3(801) -> 52
, 1_3(803) -> 802
, 1_3(804) -> 803
, 1_3(806) -> 805
, 1_3(807) -> 888
, 1_3(809) -> 808
, 1_3(810) -> 888
, 1_3(812) -> 811
, 1_3(813) -> 888
, 1_3(815) -> 814
, 1_3(816) -> 888
, 1_3(818) -> 817
, 1_3(819) -> 888
, 1_3(821) -> 820
, 1_3(822) -> 888
, 1_3(824) -> 823
, 1_3(827) -> 826
, 1_3(886) -> 34
, 1_3(886) -> 37
, 1_3(886) -> 40
, 1_3(886) -> 43
, 1_3(886) -> 46
, 1_3(886) -> 49
, 1_3(886) -> 52
, 1_3(888) -> 887
, 1_3(889) -> 888
, 1_3(891) -> 890
, 1_3(892) -> 888
, 1_3(894) -> 893
, 1_3(895) -> 888
, 1_3(897) -> 896
, 1_3(898) -> 888
, 1_3(900) -> 899
, 1_3(901) -> 888
, 1_3(903) -> 902
, 1_3(904) -> 888
, 1_3(906) -> 905
, 1_3(909) -> 908
, 1_3(910) -> 34
, 1_3(910) -> 37
, 1_3(910) -> 40
, 1_3(910) -> 43
, 1_3(910) -> 46
, 1_3(910) -> 49
, 1_3(912) -> 911
, 1_3(913) -> 912
, 1_3(915) -> 914
, 1_3(916) -> 912
, 1_3(918) -> 917
, 1_3(919) -> 888
, 1_3(921) -> 920
, 1_3(922) -> 888
, 1_3(924) -> 923
, 1_3(925) -> 888
, 1_3(927) -> 926
, 1_3(928) -> 888
, 1_3(930) -> 929
, 1_3(933) -> 932
, 2_0(1) -> 1
, 2_1(1) -> 28
, 2_1(2) -> 25
, 2_1(3) -> 2
, 2_1(4) -> 25
, 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_1(26) -> 25
, 2_2(2) -> 54
, 2_2(5) -> 54
, 2_2(8) -> 54
, 2_2(11) -> 51
, 2_2(14) -> 48
, 2_2(17) -> 45
, 2_2(20) -> 42
, 2_2(23) -> 36
, 2_2(31) -> 54
, 2_2(32) -> 31
, 2_2(34) -> 39
, 2_2(37) -> 36
, 2_2(40) -> 39
, 2_2(43) -> 42
, 2_2(46) -> 45
, 2_2(49) -> 48
, 2_2(52) -> 51
, 2_2(55) -> 75
, 2_2(56) -> 55
, 2_2(58) -> 92
, 2_2(59) -> 58
, 2_2(61) -> 69
, 2_2(64) -> 63
, 2_2(67) -> 66
, 2_2(70) -> 69
, 2_2(73) -> 72
, 2_2(78) -> 113
, 2_2(79) -> 78
, 2_2(81) -> 92
, 2_2(84) -> 83
, 2_2(87) -> 86
, 2_2(90) -> 89
, 2_2(102) -> 128
, 2_2(103) -> 102
, 2_2(105) -> 758
, 2_2(108) -> 107
, 2_2(111) -> 110
, 2_2(120) -> 800
, 2_2(121) -> 120
, 2_2(123) -> 773
, 2_2(126) -> 125
, 2_2(750) -> 749
, 2_2(765) -> 764
, 2_2(768) -> 767
, 2_2(771) -> 770
, 2_2(774) -> 885
, 2_2(775) -> 774
, 2_2(777) -> 63
, 2_2(780) -> 779
, 2_2(783) -> 782
, 2_2(786) -> 785
, 2_2(789) -> 788
, 2_2(792) -> 791
, 2_2(795) -> 794
, 2_2(798) -> 797
, 2_2(862) -> 882
, 2_2(863) -> 862
, 2_2(865) -> 125
, 2_2(868) -> 867
, 2_2(871) -> 870
, 2_2(874) -> 873
, 2_2(877) -> 876
, 2_2(880) -> 879
, 2_2(883) -> 882
, 2_3(31) -> 909
, 2_3(55) -> 909
, 2_3(58) -> 827
, 2_3(78) -> 137
, 2_3(102) -> 137
, 2_3(120) -> 137
, 2_3(129) -> 137
, 2_3(130) -> 129
, 2_3(132) -> 821
, 2_3(135) -> 134
, 2_3(750) -> 134
, 2_3(765) -> 134
, 2_3(768) -> 134
, 2_3(771) -> 134
, 2_3(774) -> 134
, 2_3(795) -> 134
, 2_3(801) -> 933
, 2_3(802) -> 801
, 2_3(804) -> 134
, 2_3(807) -> 806
, 2_3(810) -> 809
, 2_3(813) -> 812
, 2_3(816) -> 815
, 2_3(819) -> 818
, 2_3(822) -> 821
, 2_3(825) -> 824
, 2_3(862) -> 134
, 2_3(880) -> 134
, 2_3(886) -> 930
, 2_3(887) -> 886
, 2_3(889) -> 809
, 2_3(892) -> 891
, 2_3(895) -> 894
, 2_3(898) -> 897
, 2_3(901) -> 900
, 2_3(904) -> 903
, 2_3(907) -> 906
, 2_3(910) -> 134
, 2_3(911) -> 910
, 2_3(913) -> 806
, 2_3(916) -> 915
, 2_3(919) -> 918
, 2_3(922) -> 921
, 2_3(925) -> 924
, 2_3(928) -> 927
, 2_3(931) -> 930
, 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_1(27) -> 26
, 0_2(35) -> 34
, 0_2(38) -> 37
, 0_2(41) -> 40
, 0_2(44) -> 43
, 0_2(47) -> 46
, 0_2(50) -> 49
, 0_2(53) -> 52
, 0_2(62) -> 61
, 0_2(65) -> 64
, 0_2(68) -> 67
, 0_2(71) -> 70
, 0_2(74) -> 73
, 0_2(82) -> 81
, 0_2(85) -> 84
, 0_2(88) -> 87
, 0_2(91) -> 90
, 0_2(106) -> 105
, 0_2(109) -> 108
, 0_2(112) -> 111
, 0_2(124) -> 123
, 0_2(127) -> 126
, 0_2(748) -> 78
, 0_2(757) -> 750
, 0_2(763) -> 102
, 0_2(766) -> 765
, 0_2(769) -> 768
, 0_2(772) -> 771
, 0_2(778) -> 777
, 0_2(781) -> 780
, 0_2(784) -> 783
, 0_2(787) -> 786
, 0_2(790) -> 789
, 0_2(793) -> 792
, 0_2(796) -> 795
, 0_2(799) -> 798
, 0_2(866) -> 865
, 0_2(869) -> 868
, 0_2(872) -> 871
, 0_2(875) -> 874
, 0_2(878) -> 877
, 0_2(881) -> 880
, 0_2(884) -> 883
, 0_3(133) -> 132
, 0_3(136) -> 135
, 0_3(805) -> 804
, 0_3(808) -> 807
, 0_3(811) -> 810
, 0_3(814) -> 813
, 0_3(817) -> 816
, 0_3(820) -> 819
, 0_3(823) -> 822
, 0_3(826) -> 825
, 0_3(890) -> 889
, 0_3(893) -> 892
, 0_3(896) -> 895
, 0_3(899) -> 898
, 0_3(902) -> 901
, 0_3(905) -> 904
, 0_3(908) -> 907
, 0_3(914) -> 913
, 0_3(917) -> 916
, 0_3(920) -> 919
, 0_3(923) -> 922
, 0_3(926) -> 925
, 0_3(929) -> 928
, 0_3(932) -> 931}
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(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(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(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(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(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(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(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(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..