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(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) -> 17
, 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(19) -> 18
, 1_2(17) -> 23
, 1_2(22) -> 5
, 1_2(22) -> 8
, 1_2(22) -> 11
, 1_2(22) -> 14
, 1_2(22) -> 17
, 1_2(24) -> 23
, 1_2(25) -> 24
, 1_2(27) -> 26
, 1_2(28) -> 39
, 1_2(30) -> 29
, 1_2(31) -> 39
, 1_2(33) -> 32
, 1_2(36) -> 35
, 1_2(37) -> 5
, 1_2(37) -> 8
, 1_2(37) -> 11
, 1_2(37) -> 14
, 1_2(37) -> 17
, 1_2(39) -> 38
, 1_2(40) -> 5
, 1_2(40) -> 8
, 1_2(40) -> 11
, 1_2(40) -> 14
, 1_2(42) -> 41
, 1_2(43) -> 42
, 1_2(45) -> 44
, 1_2(46) -> 24
, 1_2(48) -> 47
, 1_2(144) -> 143
, 1_2(145) -> 5
, 1_2(145) -> 8
, 1_2(145) -> 11
, 1_2(147) -> 146
, 1_2(148) -> 147
, 1_2(150) -> 149
, 1_2(151) -> 147
, 1_2(153) -> 152
, 1_2(154) -> 39
, 1_2(156) -> 155
, 1_2(157) -> 39
, 1_2(159) -> 158
, 1_2(162) -> 161
, 1_2(181) -> 5
, 1_2(181) -> 8
, 1_2(183) -> 182
, 1_2(184) -> 183
, 1_2(186) -> 185
, 1_2(187) -> 183
, 1_2(189) -> 188
, 1_2(190) -> 42
, 1_2(192) -> 191
, 1_2(195) -> 194
, 1_3(163) -> 25
, 1_3(163) -> 28
, 1_3(163) -> 31
, 1_3(163) -> 34
, 1_3(165) -> 164
, 1_3(166) -> 165
, 1_3(168) -> 167
, 1_3(169) -> 198
, 1_3(171) -> 170
, 1_3(172) -> 198
, 1_3(174) -> 173
, 1_3(175) -> 198
, 1_3(177) -> 176
, 1_3(180) -> 179
, 1_3(196) -> 25
, 1_3(196) -> 28
, 1_3(196) -> 31
, 1_3(196) -> 34
, 1_3(198) -> 197
, 1_3(199) -> 198
, 1_3(201) -> 200
, 1_3(202) -> 198
, 1_3(204) -> 203
, 1_3(205) -> 198
, 1_3(207) -> 206
, 1_3(210) -> 209
, 1_3(211) -> 25
, 1_3(211) -> 28
, 1_3(211) -> 31
, 1_3(213) -> 212
, 1_3(214) -> 213
, 1_3(216) -> 215
, 1_3(217) -> 213
, 1_3(219) -> 218
, 1_3(220) -> 213
, 1_3(222) -> 221
, 1_3(225) -> 224
, 2_0(1) -> 1
, 2_1(1) -> 19
, 2_1(2) -> 16
, 2_1(3) -> 2
, 2_1(4) -> 16
, 2_1(5) -> 7
, 2_1(8) -> 7
, 2_1(11) -> 10
, 2_1(14) -> 13
, 2_1(17) -> 16
, 2_2(2) -> 36
, 2_2(5) -> 36
, 2_2(8) -> 36
, 2_2(11) -> 33
, 2_2(14) -> 27
, 2_2(22) -> 36
, 2_2(23) -> 22
, 2_2(25) -> 30
, 2_2(28) -> 27
, 2_2(31) -> 30
, 2_2(34) -> 33
, 2_2(37) -> 48
, 2_2(38) -> 37
, 2_2(40) -> 162
, 2_2(41) -> 40
, 2_2(43) -> 144
, 2_2(46) -> 45
, 2_2(145) -> 195
, 2_2(146) -> 145
, 2_2(151) -> 150
, 2_2(154) -> 153
, 2_2(157) -> 156
, 2_2(160) -> 159
, 2_2(181) -> 192
, 2_2(182) -> 181
, 2_2(184) -> 45
, 2_2(187) -> 186
, 2_2(190) -> 189
, 2_2(193) -> 192
, 2_3(22) -> 210
, 2_3(37) -> 210
, 2_3(40) -> 180
, 2_3(145) -> 177
, 2_3(163) -> 225
, 2_3(164) -> 163
, 2_3(166) -> 168
, 2_3(169) -> 168
, 2_3(172) -> 171
, 2_3(175) -> 174
, 2_3(178) -> 177
, 2_3(181) -> 174
, 2_3(196) -> 222
, 2_3(197) -> 196
, 2_3(199) -> 171
, 2_3(202) -> 201
, 2_3(205) -> 204
, 2_3(208) -> 207
, 2_3(211) -> 177
, 2_3(212) -> 211
, 2_3(214) -> 171
, 2_3(217) -> 216
, 2_3(220) -> 219
, 2_3(223) -> 222
, 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_2(26) -> 25
, 0_2(29) -> 28
, 0_2(32) -> 31
, 0_2(35) -> 34
, 0_2(44) -> 43
, 0_2(47) -> 46
, 0_2(143) -> 37
, 0_2(149) -> 148
, 0_2(152) -> 151
, 0_2(155) -> 154
, 0_2(158) -> 157
, 0_2(161) -> 160
, 0_2(185) -> 184
, 0_2(188) -> 187
, 0_2(191) -> 190
, 0_2(194) -> 193
, 0_3(167) -> 166
, 0_3(170) -> 169
, 0_3(173) -> 172
, 0_3(176) -> 175
, 0_3(179) -> 178
, 0_3(200) -> 199
, 0_3(203) -> 202
, 0_3(206) -> 205
, 0_3(209) -> 208
, 0_3(215) -> 214
, 0_3(218) -> 217
, 0_3(221) -> 220
, 0_3(224) -> 223}
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(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(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(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(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..