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(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(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) -> 29
, 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(26) -> 4
, 1_1(28) -> 27
, 1_1(31) -> 30
, 1_2(17) -> 178
, 1_2(34) -> 5
, 1_2(34) -> 8
, 1_2(34) -> 11
, 1_2(34) -> 14
, 1_2(34) -> 17
, 1_2(34) -> 20
, 1_2(34) -> 23
, 1_2(34) -> 26
, 1_2(34) -> 29
, 1_2(36) -> 35
, 1_2(37) -> 36
, 1_2(39) -> 38
, 1_2(40) -> 63
, 1_2(42) -> 41
, 1_2(43) -> 63
, 1_2(45) -> 44
, 1_2(46) -> 63
, 1_2(48) -> 47
, 1_2(49) -> 63
, 1_2(51) -> 50
, 1_2(52) -> 63
, 1_2(54) -> 53
, 1_2(55) -> 63
, 1_2(57) -> 56
, 1_2(60) -> 59
, 1_2(61) -> 5
, 1_2(61) -> 8
, 1_2(61) -> 11
, 1_2(61) -> 14
, 1_2(61) -> 17
, 1_2(61) -> 20
, 1_2(61) -> 23
, 1_2(61) -> 26
, 1_2(61) -> 29
, 1_2(63) -> 62
, 1_2(64) -> 5
, 1_2(64) -> 8
, 1_2(64) -> 11
, 1_2(64) -> 14
, 1_2(64) -> 17
, 1_2(64) -> 20
, 1_2(64) -> 23
, 1_2(64) -> 26
, 1_2(66) -> 65
, 1_2(67) -> 66
, 1_2(69) -> 68
, 1_2(70) -> 66
, 1_2(72) -> 71
, 1_2(73) -> 66
, 1_2(75) -> 74
, 1_2(76) -> 66
, 1_2(78) -> 77
, 1_2(79) -> 66
, 1_2(81) -> 80
, 1_2(84) -> 83
, 1_2(87) -> 5
, 1_2(87) -> 8
, 1_2(87) -> 11
, 1_2(87) -> 14
, 1_2(87) -> 17
, 1_2(87) -> 20
, 1_2(87) -> 23
, 1_2(89) -> 88
, 1_2(90) -> 89
, 1_2(92) -> 91
, 1_2(93) -> 89
, 1_2(95) -> 94
, 1_2(96) -> 89
, 1_2(98) -> 97
, 1_2(99) -> 89
, 1_2(101) -> 100
, 1_2(104) -> 103
, 1_2(114) -> 5
, 1_2(114) -> 8
, 1_2(114) -> 11
, 1_2(114) -> 14
, 1_2(114) -> 17
, 1_2(114) -> 20
, 1_2(116) -> 115
, 1_2(117) -> 116
, 1_2(119) -> 118
, 1_2(120) -> 116
, 1_2(122) -> 121
, 1_2(123) -> 116
, 1_2(125) -> 124
, 1_2(126) -> 66
, 1_2(128) -> 127
, 1_2(145) -> 5
, 1_2(145) -> 8
, 1_2(145) -> 11
, 1_2(145) -> 14
, 1_2(145) -> 17
, 1_2(147) -> 146
, 1_2(148) -> 147
, 1_2(150) -> 149
, 1_2(151) -> 147
, 1_2(153) -> 152
, 1_2(154) -> 147
, 1_2(156) -> 155
, 1_2(177) -> 5
, 1_2(177) -> 8
, 1_2(177) -> 11
, 1_2(177) -> 14
, 1_2(177) -> 17
, 1_2(177) -> 20
, 1_2(179) -> 178
, 1_2(180) -> 179
, 1_2(182) -> 181
, 1_2(183) -> 179
, 1_2(185) -> 184
, 1_2(1112) -> 1111
, 1_2(1128) -> 1127
, 1_2(1129) -> 17
, 1_2(1137) -> 1136
, 1_2(1138) -> 17
, 1_2(1146) -> 1145
, 1_2(1152) -> 1151
, 1_2(1153) -> 17
, 1_2(1155) -> 1154
, 1_2(1156) -> 17
, 1_2(1158) -> 1157
, 1_2(1159) -> 17
, 1_2(1161) -> 1160
, 1_2(1162) -> 17
, 1_2(1164) -> 1163
, 1_2(1165) -> 5
, 1_2(1165) -> 8
, 1_2(1165) -> 11
, 1_2(1165) -> 14
, 1_2(1165) -> 17
, 1_2(1167) -> 1166
, 1_2(1168) -> 1167
, 1_2(1170) -> 1169
, 1_2(1171) -> 1167
, 1_2(1173) -> 1172
, 1_2(1174) -> 1167
, 1_2(1176) -> 1175
, 1_2(1177) -> 1167
, 1_2(1179) -> 1178
, 1_2(1180) -> 1167
, 1_2(1182) -> 1181
, 1_2(1183) -> 1167
, 1_2(1185) -> 1184
, 1_2(1186) -> 147
, 1_2(1188) -> 1187
, 1_2(1189) -> 17
, 1_2(1191) -> 1190
, 1_2(1194) -> 1193
, 1_2(1330) -> 5
, 1_2(1330) -> 8
, 1_2(1330) -> 11
, 1_2(1330) -> 14
, 1_2(1332) -> 1331
, 1_2(1333) -> 1332
, 1_2(1335) -> 1334
, 1_2(1336) -> 1332
, 1_2(1338) -> 1337
, 1_2(1339) -> 1332
, 1_2(1341) -> 1340
, 1_2(1342) -> 1332
, 1_2(1344) -> 1343
, 1_2(1345) -> 1332
, 1_2(1347) -> 1346
, 1_2(1348) -> 1332
, 1_2(1350) -> 1349
, 1_2(1351) -> 17
, 1_2(1353) -> 1352
, 1_2(1356) -> 1355
, 1_3(157) -> 37
, 1_3(157) -> 40
, 1_3(157) -> 43
, 1_3(157) -> 46
, 1_3(157) -> 49
, 1_3(157) -> 52
, 1_3(157) -> 55
, 1_3(157) -> 58
, 1_3(159) -> 158
, 1_3(160) -> 159
, 1_3(162) -> 161
, 1_3(163) -> 188
, 1_3(165) -> 164
, 1_3(168) -> 167
, 1_3(186) -> 37
, 1_3(186) -> 40
, 1_3(186) -> 43
, 1_3(186) -> 46
, 1_3(186) -> 49
, 1_3(186) -> 52
, 1_3(186) -> 55
, 1_3(186) -> 58
, 1_3(188) -> 187
, 1_3(189) -> 188
, 1_3(191) -> 190
, 1_3(194) -> 193
, 1_3(1195) -> 37
, 1_3(1195) -> 40
, 1_3(1195) -> 43
, 1_3(1195) -> 46
, 1_3(1195) -> 49
, 1_3(1195) -> 52
, 1_3(1195) -> 55
, 1_3(1195) -> 58
, 1_3(1197) -> 1196
, 1_3(1198) -> 1197
, 1_3(1200) -> 1199
, 1_3(1201) -> 1359
, 1_3(1203) -> 1202
, 1_3(1204) -> 1359
, 1_3(1206) -> 1205
, 1_3(1207) -> 1359
, 1_3(1209) -> 1208
, 1_3(1210) -> 1359
, 1_3(1212) -> 1211
, 1_3(1213) -> 1359
, 1_3(1215) -> 1214
, 1_3(1216) -> 1359
, 1_3(1218) -> 1217
, 1_3(1219) -> 1359
, 1_3(1221) -> 1220
, 1_3(1224) -> 1223
, 1_3(1357) -> 37
, 1_3(1357) -> 40
, 1_3(1357) -> 43
, 1_3(1357) -> 46
, 1_3(1357) -> 49
, 1_3(1357) -> 52
, 1_3(1357) -> 55
, 1_3(1357) -> 58
, 1_3(1359) -> 1358
, 1_3(1360) -> 1359
, 1_3(1362) -> 1361
, 1_3(1363) -> 1359
, 1_3(1365) -> 1364
, 1_3(1366) -> 1359
, 1_3(1368) -> 1367
, 1_3(1369) -> 1359
, 1_3(1371) -> 1370
, 1_3(1372) -> 1359
, 1_3(1374) -> 1373
, 1_3(1375) -> 1359
, 1_3(1377) -> 1376
, 1_3(1378) -> 1359
, 1_3(1380) -> 1379
, 1_3(1383) -> 1382
, 1_3(1460) -> 37
, 1_3(1460) -> 40
, 1_3(1460) -> 43
, 1_3(1460) -> 46
, 1_3(1460) -> 49
, 1_3(1460) -> 52
, 1_3(1460) -> 55
, 1_3(1462) -> 1461
, 1_3(1463) -> 1462
, 1_3(1465) -> 1464
, 1_3(1466) -> 1462
, 1_3(1468) -> 1467
, 1_3(1469) -> 1359
, 1_3(1471) -> 1470
, 1_3(1472) -> 1359
, 1_3(1474) -> 1473
, 1_3(1475) -> 1359
, 1_3(1477) -> 1476
, 1_3(1478) -> 1359
, 1_3(1480) -> 1479
, 1_3(1481) -> 188
, 1_3(1483) -> 1482
, 1_3(1486) -> 1485
, 2_0(1) -> 1
, 2_1(1) -> 31
, 2_1(2) -> 28
, 2_1(3) -> 2
, 2_1(4) -> 28
, 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_1(29) -> 28
, 2_2(2) -> 60
, 2_2(5) -> 60
, 2_2(8) -> 60
, 2_2(11) -> 57
, 2_2(14) -> 54
, 2_2(17) -> 51
, 2_2(20) -> 48
, 2_2(23) -> 45
, 2_2(26) -> 39
, 2_2(34) -> 60
, 2_2(35) -> 34
, 2_2(37) -> 42
, 2_2(40) -> 39
, 2_2(43) -> 42
, 2_2(46) -> 45
, 2_2(49) -> 48
, 2_2(52) -> 51
, 2_2(55) -> 54
, 2_2(58) -> 57
, 2_2(61) -> 84
, 2_2(62) -> 61
, 2_2(64) -> 104
, 2_2(65) -> 64
, 2_2(67) -> 75
, 2_2(70) -> 69
, 2_2(73) -> 72
, 2_2(76) -> 75
, 2_2(79) -> 78
, 2_2(82) -> 81
, 2_2(87) -> 128
, 2_2(88) -> 87
, 2_2(90) -> 101
, 2_2(93) -> 92
, 2_2(96) -> 95
, 2_2(99) -> 98
, 2_2(102) -> 101
, 2_2(114) -> 156
, 2_2(115) -> 114
, 2_2(117) -> 1112
, 2_2(120) -> 119
, 2_2(123) -> 122
, 2_2(126) -> 125
, 2_2(145) -> 185
, 2_2(146) -> 145
, 2_2(148) -> 1146
, 2_2(151) -> 150
, 2_2(154) -> 153
, 2_2(177) -> 1194
, 2_2(178) -> 177
, 2_2(180) -> 1164
, 2_2(183) -> 182
, 2_2(1129) -> 1128
, 2_2(1138) -> 1137
, 2_2(1153) -> 1152
, 2_2(1156) -> 1155
, 2_2(1159) -> 1158
, 2_2(1162) -> 1161
, 2_2(1165) -> 1356
, 2_2(1166) -> 1165
, 2_2(1168) -> 92
, 2_2(1171) -> 1170
, 2_2(1174) -> 1173
, 2_2(1177) -> 1176
, 2_2(1180) -> 1179
, 2_2(1183) -> 1182
, 2_2(1186) -> 1185
, 2_2(1189) -> 1188
, 2_2(1192) -> 1191
, 2_2(1330) -> 1353
, 2_2(1331) -> 1330
, 2_2(1333) -> 182
, 2_2(1336) -> 1335
, 2_2(1339) -> 1338
, 2_2(1342) -> 1341
, 2_2(1345) -> 1344
, 2_2(1348) -> 1347
, 2_2(1351) -> 1350
, 2_2(1354) -> 1353
, 2_3(34) -> 1383
, 2_3(61) -> 1383
, 2_3(64) -> 1224
, 2_3(87) -> 194
, 2_3(114) -> 168
, 2_3(145) -> 165
, 2_3(157) -> 168
, 2_3(158) -> 157
, 2_3(160) -> 1215
, 2_3(163) -> 162
, 2_3(166) -> 165
, 2_3(177) -> 165
, 2_3(186) -> 168
, 2_3(187) -> 186
, 2_3(189) -> 1218
, 2_3(192) -> 191
, 2_3(1129) -> 162
, 2_3(1138) -> 162
, 2_3(1153) -> 162
, 2_3(1156) -> 162
, 2_3(1159) -> 162
, 2_3(1162) -> 162
, 2_3(1165) -> 162
, 2_3(1189) -> 162
, 2_3(1195) -> 1486
, 2_3(1196) -> 1195
, 2_3(1198) -> 162
, 2_3(1201) -> 1200
, 2_3(1204) -> 1203
, 2_3(1207) -> 1206
, 2_3(1210) -> 1209
, 2_3(1213) -> 1212
, 2_3(1216) -> 1215
, 2_3(1219) -> 1218
, 2_3(1222) -> 1221
, 2_3(1330) -> 162
, 2_3(1351) -> 162
, 2_3(1357) -> 1483
, 2_3(1358) -> 1357
, 2_3(1360) -> 162
, 2_3(1363) -> 1362
, 2_3(1366) -> 1365
, 2_3(1369) -> 1368
, 2_3(1372) -> 1371
, 2_3(1375) -> 1374
, 2_3(1378) -> 1377
, 2_3(1381) -> 1380
, 2_3(1460) -> 165
, 2_3(1461) -> 1460
, 2_3(1463) -> 162
, 2_3(1466) -> 1465
, 2_3(1469) -> 1468
, 2_3(1472) -> 1471
, 2_3(1475) -> 1474
, 2_3(1478) -> 1477
, 2_3(1481) -> 1480
, 2_3(1484) -> 1483
, 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_1(30) -> 29
, 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(56) -> 55
, 0_2(59) -> 58
, 0_2(68) -> 67
, 0_2(71) -> 70
, 0_2(74) -> 73
, 0_2(77) -> 76
, 0_2(80) -> 79
, 0_2(83) -> 82
, 0_2(91) -> 90
, 0_2(94) -> 93
, 0_2(97) -> 96
, 0_2(100) -> 99
, 0_2(103) -> 102
, 0_2(118) -> 117
, 0_2(121) -> 120
, 0_2(124) -> 123
, 0_2(127) -> 126
, 0_2(149) -> 148
, 0_2(152) -> 151
, 0_2(155) -> 154
, 0_2(181) -> 180
, 0_2(184) -> 183
, 0_2(1111) -> 87
, 0_2(1127) -> 114
, 0_2(1136) -> 1129
, 0_2(1145) -> 1138
, 0_2(1151) -> 145
, 0_2(1154) -> 1153
, 0_2(1157) -> 1156
, 0_2(1160) -> 1159
, 0_2(1163) -> 1162
, 0_2(1169) -> 1168
, 0_2(1172) -> 1171
, 0_2(1175) -> 1174
, 0_2(1178) -> 1177
, 0_2(1181) -> 1180
, 0_2(1184) -> 1183
, 0_2(1187) -> 1186
, 0_2(1190) -> 1189
, 0_2(1193) -> 1192
, 0_2(1334) -> 1333
, 0_2(1337) -> 1336
, 0_2(1340) -> 1339
, 0_2(1343) -> 1342
, 0_2(1346) -> 1345
, 0_2(1349) -> 1348
, 0_2(1352) -> 1351
, 0_2(1355) -> 1354
, 0_3(161) -> 160
, 0_3(164) -> 163
, 0_3(167) -> 166
, 0_3(190) -> 189
, 0_3(193) -> 192
, 0_3(1199) -> 1198
, 0_3(1202) -> 1201
, 0_3(1205) -> 1204
, 0_3(1208) -> 1207
, 0_3(1211) -> 1210
, 0_3(1214) -> 1213
, 0_3(1217) -> 1216
, 0_3(1220) -> 1219
, 0_3(1223) -> 1222
, 0_3(1361) -> 1360
, 0_3(1364) -> 1363
, 0_3(1367) -> 1366
, 0_3(1370) -> 1369
, 0_3(1373) -> 1372
, 0_3(1376) -> 1375
, 0_3(1379) -> 1378
, 0_3(1382) -> 1381
, 0_3(1464) -> 1463
, 0_3(1467) -> 1466
, 0_3(1470) -> 1469
, 0_3(1473) -> 1472
, 0_3(1476) -> 1475
, 0_3(1479) -> 1478
, 0_3(1482) -> 1481
, 0_3(1485) -> 1484}
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(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(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(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(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(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(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..