Tool Bounds
stdout:
YES(?,O(n^1))
We consider the following Problem:
Strict Trs:
{ 5(5(5(2(2(3(0(1(0(0(5(3(x1)))))))))))) ->
3(5(4(0(1(1(4(1(1(1(3(5(1(3(x1))))))))))))))
, 5(5(5(1(1(1(2(0(5(0(2(5(x1)))))))))))) ->
1(4(1(4(3(4(0(4(3(3(4(4(0(4(0(4(4(0(x1))))))))))))))))))
, 5(5(4(5(3(3(5(2(5(5(2(2(x1)))))))))))) ->
1(3(2(1(2(5(2(4(1(1(0(4(1(4(x1))))))))))))))
, 5(5(3(5(1(2(3(4(2(5(5(3(x1)))))))))))) ->
4(1(3(1(5(4(1(3(1(4(3(2(2(4(4(0(4(4(x1))))))))))))))))))
, 5(5(1(5(5(4(1(5(2(5(1(1(x1)))))))))))) ->
4(0(4(1(1(0(0(4(4(1(1(5(4(4(5(4(4(4(x1))))))))))))))))))
, 5(5(1(2(3(2(5(3(5(5(0(4(x1)))))))))))) ->
0(1(1(0(3(4(0(3(3(4(4(1(0(5(1(1(4(x1)))))))))))))))))
, 5(5(0(2(3(5(2(1(5(0(5(5(x1)))))))))))) ->
1(1(0(2(4(4(4(2(0(4(5(0(2(4(1(5(4(4(x1))))))))))))))))))
, 5(4(0(2(5(5(3(1(2(3(1(0(x1)))))))))))) ->
1(4(4(2(4(1(4(1(3(3(1(3(1(3(1(4(4(3(x1))))))))))))))))))
, 5(3(3(2(3(1(2(2(1(5(5(0(x1)))))))))))) ->
5(5(4(4(1(1(1(4(1(3(0(1(4(2(1(4(4(x1)))))))))))))))))
, 5(3(2(5(1(5(2(5(0(0(0(5(x1)))))))))))) ->
5(3(2(2(0(4(2(5(4(1(5(2(0(4(x1))))))))))))))
, 5(3(1(5(1(2(2(2(2(5(2(5(x1)))))))))))) ->
1(1(4(4(4(4(5(3(4(1(2(0(1(0(0(x1)))))))))))))))
, 5(3(0(5(5(2(5(3(4(5(2(2(x1)))))))))))) ->
1(1(3(3(2(4(2(4(4(2(2(1(0(1(3(4(x1))))))))))))))))
, 5(3(0(2(3(3(2(5(1(1(4(5(x1)))))))))))) ->
4(3(4(1(0(1(3(3(5(4(1(2(1(4(4(x1)))))))))))))))
, 5(2(5(3(4(0(2(3(3(2(0(3(x1)))))))))))) ->
4(0(5(4(0(3(5(0(1(4(4(1(3(4(1(x1)))))))))))))))
, 5(2(5(0(5(4(2(5(2(2(3(5(x1)))))))))))) ->
1(4(4(1(1(4(1(2(1(0(3(3(3(4(0(2(4(2(x1))))))))))))))))))
, 5(2(3(2(3(0(5(2(4(0(5(5(x1)))))))))))) ->
4(4(2(4(2(4(1(4(4(4(5(4(4(1(x1))))))))))))))
, 5(2(1(2(3(2(1(5(0(3(3(4(x1)))))))))))) ->
1(4(4(0(1(2(1(4(3(0(4(5(2(5(x1))))))))))))))
, 5(2(1(0(3(5(5(1(0(5(0(2(x1)))))))))))) ->
4(4(2(3(1(3(3(4(5(4(1(3(1(4(4(3(4(x1)))))))))))))))))
, 5(1(5(5(2(3(1(3(1(1(0(3(x1)))))))))))) ->
0(0(1(5(4(3(1(5(4(4(1(1(4(0(x1))))))))))))))
, 5(1(3(0(5(2(2(1(4(5(3(1(x1)))))))))))) ->
4(4(1(4(1(4(1(3(4(3(1(0(3(4(x1))))))))))))))
, 5(0(5(3(0(1(1(3(4(0(2(5(x1)))))))))))) ->
3(2(4(3(2(4(4(4(4(1(4(4(0(3(x1))))))))))))))
, 5(0(3(4(4(3(0(3(2(5(0(0(x1)))))))))))) ->
3(3(4(3(4(4(0(2(1(4(1(1(4(4(4(x1)))))))))))))))
, 4(5(5(3(3(5(2(3(2(2(0(5(x1)))))))))))) ->
0(1(4(2(4(4(5(4(4(4(5(5(4(5(4(4(5(x1)))))))))))))))))
, 4(5(5(2(3(1(1(5(5(2(0(5(x1)))))))))))) ->
4(0(4(1(4(4(0(1(4(4(5(1(2(3(2(4(x1))))))))))))))))
, 4(5(3(5(2(1(2(3(3(3(2(5(x1)))))))))))) ->
4(4(5(4(5(4(5(1(4(4(3(4(4(4(1(5(x1))))))))))))))))
, 4(3(5(2(2(1(2(0(2(5(0(0(x1)))))))))))) ->
1(4(4(3(5(5(0(4(4(4(4(3(4(0(x1))))))))))))))
, 4(3(0(3(3(0(2(3(0(5(1(3(x1)))))))))))) ->
0(1(2(2(3(4(5(4(4(3(3(4(4(1(x1))))))))))))))
, 4(3(0(0(1(5(3(2(1(0(1(0(x1)))))))))))) ->
0(1(2(4(5(4(4(4(2(4(3(0(1(4(x1))))))))))))))
, 4(1(2(0(0(0(0(0(1(5(3(1(x1)))))))))))) ->
4(1(4(4(2(5(1(4(3(1(1(5(5(3(x1))))))))))))))
, 4(0(5(0(5(4(3(5(2(2(5(0(x1)))))))))))) ->
0(4(5(2(4(4(0(4(2(0(4(4(5(1(0(x1)))))))))))))))
, 3(5(5(5(2(0(1(2(2(4(2(3(x1)))))))))))) ->
0(2(0(4(4(1(0(4(5(4(1(4(4(4(4(1(4(2(x1))))))))))))))))))
, 3(5(5(2(3(0(0(1(3(2(5(3(x1)))))))))))) ->
0(1(4(0(0(1(1(3(3(1(1(0(0(2(4(x1)))))))))))))))
, 3(5(5(0(0(5(2(2(2(5(5(4(x1)))))))))))) ->
4(3(4(2(4(1(4(4(3(3(2(2(4(3(4(3(x1))))))))))))))))
, 3(5(1(0(3(5(2(1(1(3(5(0(x1)))))))))))) ->
1(1(1(5(4(4(4(3(4(0(5(1(4(4(0(0(x1))))))))))))))))
, 3(5(0(2(5(3(3(2(0(2(2(4(x1)))))))))))) ->
4(3(3(3(1(3(4(1(3(4(4(4(5(4(1(3(1(4(x1))))))))))))))))))
, 3(4(0(3(0(3(5(0(2(3(2(1(x1)))))))))))) ->
3(1(3(4(1(4(4(4(4(0(1(1(3(2(0(x1)))))))))))))))
, 3(3(5(4(3(5(0(0(3(5(2(1(x1)))))))))))) ->
0(2(4(4(0(4(4(4(5(2(1(1(3(3(5(1(4(x1)))))))))))))))))
, 3(3(5(3(3(0(1(2(2(1(1(5(x1)))))))))))) ->
4(2(3(4(1(1(3(1(5(2(4(4(1(1(1(x1)))))))))))))))
, 3(3(5(2(0(2(3(1(1(1(0(5(x1)))))))))))) ->
1(1(4(0(1(2(4(5(4(0(1(4(1(3(4(4(x1))))))))))))))))
, 3(3(5(1(1(5(0(3(5(1(1(1(x1)))))))))))) ->
4(4(3(3(1(4(4(1(1(3(4(4(1(0(1(5(4(4(x1))))))))))))))))))
, 3(3(2(1(5(2(0(4(5(1(0(5(x1)))))))))))) ->
3(1(4(3(4(1(0(5(0(4(0(4(3(1(4(4(x1))))))))))))))))
, 3(2(5(2(2(1(2(5(5(5(0(0(x1)))))))))))) ->
1(3(0(2(0(5(1(4(4(1(3(1(4(5(4(0(4(x1)))))))))))))))))
, 3(2(2(5(2(5(5(1(5(5(1(5(x1)))))))))))) ->
4(4(5(3(3(3(5(3(1(4(4(1(4(3(1(1(0(1(x1))))))))))))))))))
, 3(2(2(1(3(5(5(5(5(3(3(1(x1)))))))))))) ->
1(1(1(3(4(1(2(4(5(2(2(0(4(1(x1))))))))))))))
, 3(2(0(2(1(0(5(0(0(0(1(2(x1)))))))))))) ->
4(5(4(4(1(3(1(5(4(2(4(0(1(4(4(1(x1))))))))))))))))
, 3(2(0(0(5(0(5(5(5(3(5(2(x1)))))))))))) ->
4(0(1(4(2(4(4(0(5(0(4(4(3(1(0(1(0(0(x1))))))))))))))))))
, 3(1(3(3(0(5(5(1(3(0(1(3(x1)))))))))))) ->
1(5(3(2(4(4(4(4(0(2(2(1(4(4(x1))))))))))))))
, 3(0(3(5(5(2(1(4(0(1(3(5(x1)))))))))))) ->
1(4(4(1(3(2(4(4(1(0(0(1(5(3(x1))))))))))))))
, 3(0(2(5(3(1(2(5(0(2(3(1(x1)))))))))))) ->
3(4(4(4(1(5(0(1(4(1(5(0(1(4(5(4(x1))))))))))))))))
, 2(5(2(2(0(0(0(1(1(3(2(2(x1)))))))))))) ->
0(4(5(4(2(4(4(4(4(4(4(3(1(4(1(1(4(2(x1))))))))))))))))))
, 2(5(1(2(5(4(4(3(0(0(5(5(x1)))))))))))) ->
4(4(4(2(4(5(5(4(1(2(1(4(0(3(4(x1)))))))))))))))
, 2(5(0(5(1(2(2(3(3(2(0(3(x1)))))))))))) ->
2(4(1(3(2(0(1(5(4(4(5(3(0(4(4(4(x1))))))))))))))))
, 2(3(5(5(4(0(2(0(0(0(2(0(x1)))))))))))) ->
4(3(1(3(4(1(5(4(4(0(1(4(5(4(4(2(x1))))))))))))))))
, 2(3(2(5(1(0(3(5(0(5(2(3(x1)))))))))))) ->
2(1(3(3(2(4(2(4(0(4(4(1(2(4(4(0(x1))))))))))))))))
, 2(3(2(5(1(0(0(4(3(3(5(3(x1)))))))))))) ->
4(1(1(4(1(4(4(4(0(4(4(3(4(3(4(1(4(3(x1))))))))))))))))))
, 2(2(5(5(3(0(1(2(3(0(2(5(x1)))))))))))) ->
2(0(1(4(4(5(0(1(3(0(2(2(4(3(x1))))))))))))))
, 2(1(5(5(5(2(1(5(1(4(4(1(x1)))))))))))) ->
4(3(0(4(1(0(4(0(4(4(1(2(5(4(4(x1)))))))))))))))
, 2(1(5(2(0(5(0(3(4(5(2(5(x1)))))))))))) ->
1(3(2(1(2(5(4(4(3(0(4(4(4(4(4(1(1(x1)))))))))))))))))
, 2(1(2(5(2(5(0(5(1(2(0(1(x1)))))))))))) ->
2(4(1(4(1(4(1(1(1(4(4(4(4(1(4(0(3(2(x1))))))))))))))))))
, 2(0(3(0(5(0(5(0(5(3(2(2(x1)))))))))))) ->
4(5(4(5(4(4(4(2(4(3(1(0(2(3(4(3(x1))))))))))))))))
, 1(5(5(5(0(4(3(4(3(2(5(3(x1)))))))))))) ->
4(4(3(4(5(3(1(0(4(2(0(0(4(0(1(4(x1))))))))))))))))
, 1(5(4(3(2(3(4(0(0(3(1(3(x1)))))))))))) ->
1(4(3(2(4(2(4(4(5(3(3(5(1(0(x1))))))))))))))
, 1(5(4(0(5(2(5(4(3(5(2(1(x1)))))))))))) ->
4(1(4(3(1(4(4(4(0(5(3(3(4(4(2(1(x1))))))))))))))))
, 1(5(3(5(5(5(2(2(3(5(5(3(x1)))))))))))) ->
4(4(5(3(3(0(2(4(3(3(4(2(2(4(0(1(x1))))))))))))))))
, 1(5(2(5(5(5(3(5(0(2(3(0(x1)))))))))))) ->
1(3(3(4(3(1(4(3(0(1(0(2(2(4(4(0(1(x1)))))))))))))))))
, 1(5(2(3(2(0(5(2(2(5(1(3(x1)))))))))))) ->
0(1(4(1(1(5(1(3(5(4(0(3(1(4(2(x1)))))))))))))))
, 1(5(2(1(1(5(4(0(0(2(2(2(x1)))))))))))) ->
1(2(4(1(1(4(1(1(3(4(5(1(4(1(x1))))))))))))))
, 1(5(0(2(4(3(2(5(5(3(1(3(x1)))))))))))) ->
4(3(2(0(2(2(2(4(1(4(4(1(2(3(x1))))))))))))))
, 1(2(3(5(2(0(0(1(2(0(2(2(x1)))))))))))) ->
2(1(4(4(1(4(4(1(1(2(0(3(3(0(0(4(1(4(x1))))))))))))))))))
, 1(2(3(2(0(5(5(2(0(0(1(2(x1)))))))))))) ->
5(1(4(1(4(2(2(2(1(4(0(4(4(5(x1))))))))))))))
, 1(2(1(3(5(2(2(2(2(1(3(4(x1)))))))))))) ->
4(4(1(0(5(4(3(1(5(5(4(0(4(4(x1))))))))))))))
, 1(2(0(5(5(5(5(3(2(3(2(1(x1)))))))))))) ->
5(1(5(5(0(4(0(0(4(1(4(4(4(1(1(3(3(3(x1))))))))))))))))))
, 1(2(0(5(4(1(5(5(1(3(5(2(x1)))))))))))) ->
0(4(1(3(4(4(1(4(4(0(4(4(3(2(4(4(5(x1)))))))))))))))))
, 1(2(0(5(0(4(1(1(2(5(1(1(x1)))))))))))) ->
2(2(4(3(3(0(3(4(0(1(5(4(4(4(4(x1)))))))))))))))
, 1(2(0(0(5(5(0(5(0(0(0(3(x1)))))))))))) ->
0(2(3(0(4(4(4(0(1(3(3(5(3(3(3(1(4(x1)))))))))))))))))
, 1(1(2(3(3(4(0(5(0(0(0(1(x1)))))))))))) ->
2(2(4(4(5(2(1(1(3(4(3(4(4(1(3(x1)))))))))))))))
, 1(1(2(1(3(5(4(4(0(0(3(2(x1)))))))))))) ->
4(0(1(1(0(4(3(4(3(1(0(0(4(5(x1))))))))))))))
, 1(1(2(1(3(0(3(2(5(3(3(5(x1)))))))))))) ->
3(3(5(3(4(4(5(1(4(4(4(1(3(4(4(1(4(3(x1))))))))))))))))))
, 1(1(0(5(0(5(2(4(2(3(5(2(x1)))))))))))) ->
1(1(3(4(4(4(4(4(4(5(4(3(1(4(3(1(4(3(x1))))))))))))))))))
, 1(0(5(1(3(3(5(5(0(0(2(3(x1)))))))))))) ->
1(0(3(5(3(4(4(4(4(1(4(1(2(4(0(x1)))))))))))))))
, 1(0(5(1(1(5(3(5(2(3(5(3(x1)))))))))))) ->
0(0(4(5(1(2(4(2(4(5(1(4(1(1(x1))))))))))))))
, 1(0(3(5(1(5(1(2(3(0(3(1(x1)))))))))))) ->
1(4(1(1(1(1(4(3(1(1(0(1(3(4(3(4(4(x1)))))))))))))))))
, 0(5(2(1(2(5(0(5(5(3(2(1(x1)))))))))))) ->
2(1(4(5(4(2(3(4(0(2(1(4(4(0(x1))))))))))))))
, 0(5(1(0(5(0(5(3(4(0(5(5(x1)))))))))))) ->
4(1(2(2(4(5(1(3(4(1(0(4(4(2(0(x1)))))))))))))))
, 0(5(0(1(2(5(1(1(2(1(4(2(x1)))))))))))) ->
3(4(4(1(3(0(4(3(3(1(0(1(3(4(4(x1)))))))))))))))
, 0(3(2(5(3(4(0(0(5(5(3(4(x1)))))))))))) ->
4(4(1(2(4(4(0(4(2(0(4(5(4(5(2(4(4(x1)))))))))))))))))
, 0(3(2(0(3(2(0(3(5(2(4(1(x1)))))))))))) ->
0(3(4(1(1(3(3(4(4(4(4(0(1(1(1(3(4(4(x1))))))))))))))))))
, 0(3(0(0(1(5(5(2(4(5(5(5(x1)))))))))))) ->
1(4(2(4(5(0(4(4(4(4(2(4(0(1(4(4(3(x1)))))))))))))))))
, 0(2(1(0(0(1(3(2(0(2(1(5(x1)))))))))))) ->
2(2(4(3(3(4(5(4(4(0(0(1(4(4(x1))))))))))))))
, 0(2(0(3(5(0(5(5(3(1(3(5(x1)))))))))))) ->
4(3(1(4(3(0(4(3(4(4(1(0(4(2(x1))))))))))))))
, 0(1(5(3(0(5(3(2(5(5(1(1(x1)))))))))))) ->
3(4(0(1(4(4(4(2(4(1(4(2(3(0(1(5(1(x1)))))))))))))))))
, 0(0(3(4(2(3(0(0(5(5(2(3(x1)))))))))))) ->
4(4(2(4(0(1(1(0(4(0(2(0(5(5(4(x1)))))))))))))))
, 0(0(3(2(0(3(4(2(2(3(0(5(x1)))))))))))) ->
4(1(5(5(0(0(1(4(4(4(1(1(3(0(x1))))))))))))))
, 0(0(3(0(5(5(0(0(3(3(0(5(x1)))))))))))) ->
0(1(0(5(4(2(3(3(5(4(5(4(4(0(x1))))))))))))))
, 0(0(2(3(1(5(5(0(5(2(4(1(x1)))))))))))) ->
3(4(1(4(4(4(4(1(0(0(4(5(4(4(3(0(4(3(x1))))))))))))))))))
, 0(0(0(0(0(0(3(5(3(0(0(2(x1)))))))))))) ->
1(4(4(1(4(4(0(1(1(3(3(1(4(4(1(1(0(x1)))))))))))))))))}
StartTerms: all
Strategy: none
Certificate: YES(?,O(n^1))
Proof:
The problem is match-bounded by 1.
The enriched problem is compatible with the following automaton:
{ 2_0(1) -> 1
, 2_0(2) -> 1
, 2_0(3) -> 1
, 2_0(4) -> 1
, 2_0(5) -> 1
, 2_0(6) -> 1
, 2_1(1) -> 203
, 2_1(2) -> 203
, 2_1(3) -> 203
, 2_1(4) -> 203
, 2_1(5) -> 203
, 2_1(6) -> 203
, 2_1(7) -> 203
, 2_1(8) -> 203
, 2_1(19) -> 2142
, 2_1(20) -> 203
, 2_1(34) -> 953
, 2_1(35) -> 2277
, 2_1(36) -> 444
, 2_1(37) -> 203
, 2_1(38) -> 37
, 2_1(40) -> 39
, 2_1(42) -> 41
, 2_1(45) -> 535
, 2_1(46) -> 303
, 2_1(47) -> 2081
, 2_1(48) -> 303
, 2_1(60) -> 59
, 2_1(61) -> 60
, 2_1(64) -> 2341
, 2_1(79) -> 203
, 2_1(80) -> 203
, 2_1(95) -> 94
, 2_1(99) -> 98
, 2_1(104) -> 103
, 2_1(106) -> 1084
, 2_1(108) -> 107
, 2_1(120) -> 1049
, 2_1(121) -> 203
, 2_1(133) -> 567
, 2_1(134) -> 133
, 2_1(136) -> 135
, 2_1(137) -> 136
, 2_1(140) -> 139
, 2_1(144) -> 534
, 2_1(145) -> 144
, 2_1(154) -> 153
, 2_1(159) -> 158
, 2_1(161) -> 160
, 2_1(164) -> 163
, 2_1(165) -> 164
, 2_1(189) -> 2081
, 2_1(194) -> 193
, 2_1(202) -> 201
, 2_1(205) -> 204
, 2_1(207) -> 206
, 2_1(216) -> 215
, 2_1(223) -> 222
, 2_1(254) -> 7
, 2_1(257) -> 256
, 2_1(271) -> 270
, 2_1(275) -> 203
, 2_1(276) -> 203
, 2_1(278) -> 277
, 2_1(288) -> 2199
, 2_1(302) -> 301
, 2_1(317) -> 203
, 2_1(328) -> 276
, 2_1(329) -> 328
, 2_1(341) -> 340
, 2_1(347) -> 346
, 2_1(357) -> 356
, 2_1(362) -> 361
, 2_1(367) -> 203
, 2_1(368) -> 367
, 2_1(369) -> 203
, 2_1(382) -> 203
, 2_1(396) -> 395
, 2_1(403) -> 402
, 2_1(404) -> 403
, 2_1(405) -> 1686
, 2_1(406) -> 203
, 2_1(416) -> 2306
, 2_1(432) -> 203
, 2_1(433) -> 203
, 2_1(452) -> 451
, 2_1(457) -> 393
, 2_1(458) -> 203
, 2_1(465) -> 464
, 2_1(472) -> 471
, 2_1(502) -> 203
, 2_1(504) -> 503
, 2_1(532) -> 531
, 2_1(535) -> 534
, 2_1(536) -> 535
, 2_1(545) -> 544
, 2_1(547) -> 133
, 2_1(551) -> 550
, 2_1(562) -> 561
, 2_1(572) -> 571
, 2_1(590) -> 203
, 2_1(594) -> 593
, 2_1(615) -> 614
, 2_1(621) -> 620
, 2_1(680) -> 1
, 2_1(680) -> 203
, 2_1(680) -> 222
, 2_1(680) -> 2081
, 2_1(680) -> 2142
, 2_1(684) -> 683
, 2_1(946) -> 945
, 2_1(948) -> 947
, 2_1(1040) -> 203
, 2_1(1041) -> 203
, 2_1(1049) -> 1048
, 2_1(1621) -> 203
, 2_1(1622) -> 203
, 2_1(1623) -> 1622
, 2_1(1625) -> 1624
, 2_1(1682) -> 1681
, 2_1(2056) -> 2055
, 2_1(2058) -> 2091
, 2_1(2059) -> 203
, 2_1(2062) -> 2061
, 2_1(2064) -> 2063
, 2_1(2086) -> 2085
, 2_1(2091) -> 2090
, 2_1(2092) -> 2091
, 2_1(2093) -> 203
, 2_1(2103) -> 2102
, 2_1(2104) -> 2103
, 2_1(2105) -> 203
, 2_1(2106) -> 203
, 2_1(2116) -> 2059
, 2_1(2133) -> 2132
, 2_1(2135) -> 2134
, 2_1(2136) -> 2135
, 2_1(2137) -> 2136
, 2_1(2143) -> 5
, 2_1(2143) -> 47
, 2_1(2143) -> 189
, 2_1(2143) -> 468
, 2_1(2143) -> 2141
, 2_1(2152) -> 2151
, 2_1(2157) -> 203
, 2_1(2162) -> 2161
, 2_1(2163) -> 2162
, 2_1(2164) -> 2163
, 2_1(2200) -> 2143
, 2_1(2210) -> 2105
, 2_1(2211) -> 203
, 2_1(2224) -> 2223
, 2_1(2241) -> 203
, 2_1(2242) -> 222
, 2_1(2282) -> 2281
, 2_1(2284) -> 2283
, 2_1(2298) -> 2
, 2_1(2298) -> 36
, 2_1(2303) -> 2302
, 2_1(2309) -> 2308
, 2_1(2310) -> 2309
, 2_1(2319) -> 203
, 2_1(2331) -> 2330
, 2_1(2336) -> 2335
, 2_1(2342) -> 203
, 2_1(2355) -> 1
, 2_1(2357) -> 2356
, 2_1(2365) -> 2364
, 2_1(2367) -> 2298
, 2_1(2391) -> 2390
, 2_1(2395) -> 2394
, 2_1(2399) -> 2329
, 2_1(2407) -> 2406
, 2_1(2419) -> 1
, 2_1(2420) -> 203
, 2_1(2423) -> 2422
, 0_0(1) -> 2
, 0_0(2) -> 2
, 0_0(3) -> 2
, 0_0(4) -> 2
, 0_0(5) -> 2
, 0_0(6) -> 2
, 0_1(1) -> 36
, 0_1(2) -> 36
, 0_1(3) -> 36
, 0_1(4) -> 36
, 0_1(5) -> 36
, 0_1(6) -> 36
, 0_1(7) -> 36
, 0_1(10) -> 9
, 0_1(18) -> 166
, 0_1(19) -> 264
, 0_1(20) -> 36
, 0_1(26) -> 25
, 0_1(32) -> 31
, 0_1(34) -> 33
, 0_1(36) -> 156
, 0_1(37) -> 35
, 0_1(45) -> 2155
, 0_1(46) -> 45
, 0_1(47) -> 343
, 0_1(48) -> 145
, 0_1(64) -> 63
, 0_1(65) -> 49
, 0_1(69) -> 68
, 0_1(70) -> 69
, 0_1(78) -> 691
, 0_1(79) -> 4
, 0_1(79) -> 223
, 0_1(79) -> 365
, 0_1(79) -> 456
, 0_1(82) -> 81
, 0_1(85) -> 84
, 0_1(91) -> 90
, 0_1(94) -> 93
, 0_1(100) -> 99
, 0_1(103) -> 102
, 0_1(105) -> 491
, 0_1(118) -> 2366
, 0_1(120) -> 2440
, 0_1(121) -> 36
, 0_1(122) -> 36
, 0_1(131) -> 130
, 0_1(134) -> 2375
, 0_1(138) -> 137
, 0_1(155) -> 154
, 0_1(167) -> 166
, 0_1(168) -> 253
, 0_1(172) -> 171
, 0_1(180) -> 179
, 0_1(183) -> 182
, 0_1(188) -> 536
, 0_1(189) -> 528
, 0_1(196) -> 195
, 0_1(201) -> 200
, 0_1(202) -> 2385
, 0_1(213) -> 63
, 0_1(214) -> 107
, 0_1(220) -> 219
, 0_1(235) -> 79
, 0_1(270) -> 269
, 0_1(275) -> 6
, 0_1(275) -> 35
, 0_1(275) -> 48
, 0_1(275) -> 120
, 0_1(275) -> 289
, 0_1(288) -> 2166
, 0_1(289) -> 2240
, 0_1(291) -> 290
, 0_1(296) -> 295
, 0_1(303) -> 392
, 0_1(313) -> 691
, 0_1(316) -> 2396
, 0_1(317) -> 36
, 0_1(323) -> 322
, 0_1(360) -> 359
, 0_1(363) -> 362
, 0_1(367) -> 3
, 0_1(367) -> 19
, 0_1(367) -> 2187
, 0_1(368) -> 36
, 0_1(369) -> 368
, 0_1(373) -> 372
, 0_1(384) -> 383
, 0_1(385) -> 384
, 0_1(392) -> 391
, 0_1(406) -> 36
, 0_1(415) -> 414
, 0_1(432) -> 36
, 0_1(434) -> 35
, 0_1(441) -> 440
, 0_1(447) -> 446
, 0_1(470) -> 469
, 0_1(476) -> 475
, 0_1(478) -> 2328
, 0_1(496) -> 495
, 0_1(498) -> 497
, 0_1(500) -> 499
, 0_1(502) -> 35
, 0_1(503) -> 502
, 0_1(505) -> 504
, 0_1(536) -> 2155
, 0_1(547) -> 546
, 0_1(548) -> 393
, 0_1(554) -> 553
, 0_1(556) -> 555
, 0_1(567) -> 566
, 0_1(576) -> 575
, 0_1(577) -> 576
, 0_1(583) -> 582
, 0_1(588) -> 587
, 0_1(590) -> 1
, 0_1(590) -> 203
, 0_1(590) -> 222
, 0_1(680) -> 36
, 0_1(685) -> 684
, 0_1(716) -> 715
, 0_1(943) -> 36
, 0_1(950) -> 949
, 0_1(971) -> 970
, 0_1(1040) -> 680
, 0_1(1045) -> 1044
, 0_1(1048) -> 1047
, 0_1(1054) -> 529
, 0_1(1068) -> 1067
, 0_1(1070) -> 1069
, 0_1(1621) -> 36
, 0_1(1622) -> 35
, 0_1(1630) -> 1629
, 0_1(1647) -> 1646
, 0_1(1686) -> 1685
, 0_1(2054) -> 2053
, 0_1(2057) -> 2056
, 0_1(2058) -> 2057
, 0_1(2059) -> 36
, 0_1(2076) -> 2075
, 0_1(2085) -> 2084
, 0_1(2093) -> 35
, 0_1(2100) -> 2099
, 0_1(2102) -> 2101
, 0_1(2105) -> 5
, 0_1(2105) -> 47
, 0_1(2105) -> 89
, 0_1(2105) -> 189
, 0_1(2105) -> 316
, 0_1(2105) -> 366
, 0_1(2105) -> 2141
, 0_1(2115) -> 2114
, 0_1(2116) -> 36
, 0_1(2134) -> 2133
, 0_1(2143) -> 36
, 0_1(2144) -> 36
, 0_1(2153) -> 2152
, 0_1(2157) -> 36
, 0_1(2168) -> 2167
, 0_1(2176) -> 2175
, 0_1(2178) -> 2177
, 0_1(2179) -> 2178
, 0_1(2196) -> 2195
, 0_1(2200) -> 36
, 0_1(2204) -> 2203
, 0_1(2207) -> 2206
, 0_1(2210) -> 36
, 0_1(2211) -> 36
, 0_1(2212) -> 2211
, 0_1(2216) -> 2215
, 0_1(2231) -> 2047
, 0_1(2234) -> 2233
, 0_1(2240) -> 2239
, 0_1(2241) -> 36
, 0_1(2267) -> 2059
, 0_1(2268) -> 36
, 0_1(2278) -> 2105
, 0_1(2295) -> 2294
, 0_1(2298) -> 36
, 0_1(2299) -> 36
, 0_1(2306) -> 2305
, 0_1(2317) -> 2316
, 0_1(2319) -> 36
, 0_1(2324) -> 2323
, 0_1(2334) -> 2333
, 0_1(2337) -> 2336
, 0_1(2342) -> 2
, 0_1(2342) -> 36
, 0_1(2342) -> 156
, 0_1(2342) -> 264
, 0_1(2342) -> 1646
, 0_1(2343) -> 36
, 0_1(2353) -> 2352
, 0_1(2355) -> 36
, 0_1(2360) -> 2359
, 0_1(2367) -> 36
, 0_1(2375) -> 2374
, 0_1(2380) -> 2379
, 0_1(2386) -> 2320
, 0_1(2397) -> 2396
, 0_1(2401) -> 2400
, 0_1(2404) -> 2403
, 0_1(2406) -> 2405
, 0_1(2408) -> 2407
, 0_1(2411) -> 2410
, 0_1(2412) -> 2411
, 0_1(2419) -> 36
, 0_1(2420) -> 2419
, 0_1(2434) -> 2433
, 0_1(2435) -> 2434
, 0_1(2445) -> 2444
, 3_0(1) -> 3
, 3_0(2) -> 3
, 3_0(3) -> 3
, 3_0(4) -> 3
, 3_0(5) -> 3
, 3_0(6) -> 3
, 3_1(1) -> 19
, 3_1(2) -> 19
, 3_1(3) -> 19
, 3_1(4) -> 19
, 3_1(5) -> 19
, 3_1(6) -> 19
, 3_1(7) -> 4
, 3_1(7) -> 223
, 3_1(8) -> 19
, 3_1(17) -> 16
, 3_1(19) -> 2187
, 3_1(20) -> 19
, 3_1(24) -> 23
, 3_1(28) -> 27
, 3_1(29) -> 28
, 3_1(35) -> 327
, 3_1(36) -> 2418
, 3_1(37) -> 20
, 3_1(46) -> 187
, 3_1(47) -> 431
, 3_1(48) -> 168
, 3_1(49) -> 19
, 3_1(50) -> 19
, 3_1(51) -> 50
, 3_1(56) -> 55
, 3_1(59) -> 58
, 3_1(64) -> 479
, 3_1(79) -> 19
, 3_1(80) -> 19
, 3_1(83) -> 82
, 3_1(86) -> 85
, 3_1(87) -> 86
, 3_1(113) -> 112
, 3_1(114) -> 113
, 3_1(116) -> 115
, 3_1(118) -> 117
, 3_1(120) -> 405
, 3_1(121) -> 19
, 3_1(122) -> 19
, 3_1(123) -> 19
, 3_1(130) -> 129
, 3_1(134) -> 501
, 3_1(135) -> 121
, 3_1(137) -> 19
, 3_1(151) -> 150
, 3_1(157) -> 93
, 3_1(158) -> 157
, 3_1(165) -> 2326
, 3_1(169) -> 49
, 3_1(174) -> 173
, 3_1(175) -> 174
, 3_1(181) -> 180
, 3_1(188) -> 187
, 3_1(189) -> 431
, 3_1(190) -> 19
, 3_1(191) -> 19
, 3_1(193) -> 19
, 3_1(194) -> 19
, 3_1(195) -> 19
, 3_1(197) -> 196
, 3_1(198) -> 197
, 3_1(199) -> 198
, 3_1(203) -> 1647
, 3_1(213) -> 335
, 3_1(219) -> 218
, 3_1(224) -> 205
, 3_1(226) -> 225
, 3_1(227) -> 226
, 3_1(232) -> 231
, 3_1(234) -> 2296
, 3_1(236) -> 19
, 3_1(239) -> 238
, 3_1(245) -> 19
, 3_1(247) -> 19
, 3_1(249) -> 19
, 3_1(250) -> 249
, 3_1(252) -> 251
, 3_1(256) -> 255
, 3_1(265) -> 7
, 3_1(267) -> 266
, 3_1(275) -> 19
, 3_1(276) -> 19
, 3_1(290) -> 19
, 3_1(303) -> 302
, 3_1(313) -> 312
, 3_1(317) -> 19
, 3_1(320) -> 319
, 3_1(330) -> 329
, 3_1(335) -> 334
, 3_1(343) -> 342
, 3_1(344) -> 19
, 3_1(351) -> 350
, 3_1(364) -> 2122
, 3_1(365) -> 2068
, 3_1(367) -> 19
, 3_1(381) -> 2115
, 3_1(382) -> 19
, 3_1(388) -> 387
, 3_1(389) -> 388
, 3_1(393) -> 19
, 3_1(394) -> 393
, 3_1(401) -> 400
, 3_1(402) -> 401
, 3_1(406) -> 19
, 3_1(407) -> 19
, 3_1(408) -> 19
, 3_1(413) -> 412
, 3_1(419) -> 394
, 3_1(420) -> 419
, 3_1(422) -> 421
, 3_1(425) -> 424
, 3_1(431) -> 2221
, 3_1(432) -> 3
, 3_1(432) -> 19
, 3_1(432) -> 168
, 3_1(432) -> 327
, 3_1(432) -> 2187
, 3_1(432) -> 2418
, 3_1(433) -> 19
, 3_1(434) -> 433
, 3_1(444) -> 443
, 3_1(455) -> 454
, 3_1(456) -> 455
, 3_1(458) -> 457
, 3_1(462) -> 461
, 3_1(479) -> 334
, 3_1(481) -> 480
, 3_1(482) -> 481
, 3_1(488) -> 487
, 3_1(493) -> 492
, 3_1(502) -> 406
, 3_1(511) -> 510
, 3_1(516) -> 515
, 3_1(517) -> 516
, 3_1(518) -> 517
, 3_1(520) -> 519
, 3_1(526) -> 525
, 3_1(528) -> 342
, 3_1(529) -> 408
, 3_1(541) -> 540
, 3_1(559) -> 558
, 3_1(561) -> 560
, 3_1(570) -> 19
, 3_1(571) -> 570
, 3_1(590) -> 19
, 3_1(601) -> 600
, 3_1(680) -> 19
, 3_1(682) -> 19
, 3_1(683) -> 682
, 3_1(691) -> 690
, 3_1(695) -> 694
, 3_1(719) -> 2078
, 3_1(943) -> 19
, 3_1(944) -> 943
, 3_1(945) -> 944
, 3_1(956) -> 19
, 3_1(961) -> 19
, 3_1(974) -> 973
, 3_1(976) -> 975
, 3_1(977) -> 2266
, 3_1(1040) -> 19
, 3_1(1041) -> 19
, 3_1(1047) -> 1046
, 3_1(1621) -> 19
, 3_1(1622) -> 1621
, 3_1(1629) -> 1628
, 3_1(1636) -> 19
, 3_1(1638) -> 19
, 3_1(1639) -> 19
, 3_1(1640) -> 19
, 3_1(1684) -> 1683
, 3_1(2047) -> 19
, 3_1(2049) -> 2048
, 3_1(2052) -> 2051
, 3_1(2059) -> 19
, 3_1(2061) -> 2060
, 3_1(2068) -> 2067
, 3_1(2069) -> 19
, 3_1(2071) -> 2070
, 3_1(2078) -> 2077
, 3_1(2079) -> 2078
, 3_1(2083) -> 2082
, 3_1(2084) -> 2083
, 3_1(2088) -> 2087
, 3_1(2089) -> 2088
, 3_1(2093) -> 2059
, 3_1(2094) -> 2093
, 3_1(2096) -> 2095
, 3_1(2099) -> 2098
, 3_1(2105) -> 19
, 3_1(2106) -> 19
, 3_1(2108) -> 19
, 3_1(2109) -> 19
, 3_1(2112) -> 2111
, 3_1(2116) -> 19
, 3_1(2118) -> 19
, 3_1(2119) -> 19
, 3_1(2121) -> 19
, 3_1(2122) -> 19
, 3_1(2123) -> 2122
, 3_1(2132) -> 2047
, 3_1(2143) -> 19
, 3_1(2144) -> 19
, 3_1(2154) -> 2153
, 3_1(2155) -> 2154
, 3_1(2157) -> 19
, 3_1(2167) -> 19
, 3_1(2171) -> 2170
, 3_1(2187) -> 2186
, 3_1(2189) -> 19
, 3_1(2190) -> 2189
, 3_1(2199) -> 2198
, 3_1(2200) -> 19
, 3_1(2202) -> 2201
, 3_1(2203) -> 2202
, 3_1(2205) -> 2204
, 3_1(2210) -> 19
, 3_1(2211) -> 2210
, 3_1(2218) -> 2217
, 3_1(2219) -> 2218
, 3_1(2221) -> 2220
, 3_1(2227) -> 2226
, 3_1(2229) -> 2228
, 3_1(2236) -> 2235
, 3_1(2238) -> 2237
, 3_1(2241) -> 5
, 3_1(2241) -> 47
, 3_1(2241) -> 468
, 3_1(2242) -> 2241
, 3_1(2243) -> 19
, 3_1(2244) -> 2243
, 3_1(2253) -> 2252
, 3_1(2254) -> 19
, 3_1(2255) -> 2254
, 3_1(2264) -> 2263
, 3_1(2267) -> 19
, 3_1(2268) -> 2267
, 3_1(2270) -> 2269
, 3_1(2278) -> 19
, 3_1(2286) -> 600
, 3_1(2287) -> 19
, 3_1(2288) -> 19
, 3_1(2289) -> 19
, 3_1(2290) -> 19
, 3_1(2292) -> 2291
, 3_1(2297) -> 2296
, 3_1(2298) -> 19
, 3_1(2299) -> 19
, 3_1(2304) -> 2303
, 3_1(2307) -> 19
, 3_1(2308) -> 19
, 3_1(2309) -> 19
, 3_1(2310) -> 19
, 3_1(2314) -> 2313
, 3_1(2319) -> 2
, 3_1(2319) -> 36
, 3_1(2319) -> 156
, 3_1(2319) -> 343
, 3_1(2319) -> 576
, 3_1(2319) -> 2396
, 3_1(2323) -> 2322
, 3_1(2326) -> 2325
, 3_1(2327) -> 2326
, 3_1(2330) -> 19
, 3_1(2331) -> 19
, 3_1(2342) -> 19
, 3_1(2343) -> 2342
, 3_1(2347) -> 2346
, 3_1(2348) -> 2347
, 3_1(2355) -> 19
, 3_1(2357) -> 19
, 3_1(2367) -> 19
, 3_1(2369) -> 2368
, 3_1(2370) -> 2369
, 3_1(2376) -> 2307
, 3_1(2379) -> 2378
, 3_1(2382) -> 2381
, 3_1(2396) -> 2395
, 3_1(2398) -> 455
, 3_1(2419) -> 19
, 3_1(2420) -> 19
, 3_1(2424) -> 2423
, 3_1(2425) -> 2424
, 3_1(2440) -> 2439
, 3_1(2442) -> 19
, 3_1(2448) -> 2447
, 3_1(2449) -> 2448
, 5_0(1) -> 4
, 5_0(2) -> 4
, 5_0(3) -> 4
, 5_0(4) -> 4
, 5_0(5) -> 4
, 5_0(6) -> 4
, 5_1(1) -> 223
, 5_1(2) -> 223
, 5_1(3) -> 223
, 5_1(4) -> 223
, 5_1(5) -> 223
, 5_1(6) -> 223
, 5_1(8) -> 7
, 5_1(18) -> 17
, 5_1(19) -> 354
, 5_1(20) -> 223
, 5_1(34) -> 2427
, 5_1(35) -> 513
, 5_1(41) -> 40
, 5_1(46) -> 106
, 5_1(47) -> 456
, 5_1(48) -> 106
, 5_1(49) -> 223
, 5_1(50) -> 223
, 5_1(53) -> 52
, 5_1(62) -> 2173
, 5_1(64) -> 106
, 5_1(75) -> 74
, 5_1(78) -> 77
, 5_1(92) -> 91
, 5_1(102) -> 101
, 5_1(106) -> 2408
, 5_1(121) -> 4
, 5_1(121) -> 223
, 5_1(121) -> 354
, 5_1(122) -> 121
, 5_1(141) -> 140
, 5_1(144) -> 143
, 5_1(150) -> 149
, 5_1(176) -> 175
, 5_1(178) -> 65
, 5_1(182) -> 181
, 5_1(189) -> 2398
, 5_1(190) -> 223
, 5_1(191) -> 223
, 5_1(193) -> 223
, 5_1(194) -> 223
, 5_1(195) -> 223
, 5_1(213) -> 212
, 5_1(222) -> 221
, 5_1(229) -> 228
, 5_1(237) -> 236
, 5_1(241) -> 240
, 5_1(244) -> 365
, 5_1(245) -> 223
, 5_1(247) -> 223
, 5_1(249) -> 223
, 5_1(254) -> 223
, 5_1(266) -> 223
, 5_1(275) -> 223
, 5_1(276) -> 223
, 5_1(281) -> 280
, 5_1(285) -> 284
, 5_1(286) -> 285
, 5_1(288) -> 287
, 5_1(290) -> 223
, 5_1(300) -> 299
, 5_1(303) -> 2340
, 5_1(305) -> 304
, 5_1(307) -> 306
, 5_1(309) -> 308
, 5_1(316) -> 365
, 5_1(317) -> 223
, 5_1(321) -> 320
, 5_1(322) -> 321
, 5_1(328) -> 223
, 5_1(332) -> 331
, 5_1(334) -> 2076
, 5_1(337) -> 336
, 5_1(344) -> 223
, 5_1(348) -> 347
, 5_1(354) -> 353
, 5_1(356) -> 355
, 5_1(366) -> 365
, 5_1(367) -> 223
, 5_1(375) -> 374
, 5_1(382) -> 223
, 5_1(393) -> 223
, 5_1(406) -> 223
, 5_1(407) -> 223
, 5_1(408) -> 223
, 5_1(409) -> 408
, 5_1(416) -> 415
, 5_1(429) -> 428
, 5_1(433) -> 223
, 5_1(451) -> 450
, 5_1(464) -> 463
, 5_1(468) -> 91
, 5_1(474) -> 473
, 5_1(497) -> 496
, 5_1(506) -> 505
, 5_1(513) -> 2172
, 5_1(514) -> 513
, 5_1(515) -> 480
, 5_1(519) -> 518
, 5_1(534) -> 533
, 5_1(537) -> 393
, 5_1(543) -> 542
, 5_1(555) -> 554
, 5_1(560) -> 406
, 5_1(570) -> 223
, 5_1(578) -> 223
, 5_1(582) -> 581
, 5_1(587) -> 586
, 5_1(590) -> 223
, 5_1(592) -> 591
, 5_1(617) -> 616
, 5_1(618) -> 617
, 5_1(680) -> 223
, 5_1(682) -> 223
, 5_1(687) -> 686
, 5_1(690) -> 689
, 5_1(704) -> 703
, 5_1(719) -> 718
, 5_1(943) -> 223
, 5_1(956) -> 223
, 5_1(961) -> 223
, 5_1(1040) -> 223
, 5_1(1041) -> 223
, 5_1(1044) -> 1043
, 5_1(1621) -> 223
, 5_1(1626) -> 1625
, 5_1(1636) -> 223
, 5_1(1638) -> 223
, 5_1(1639) -> 223
, 5_1(1640) -> 223
, 5_1(1658) -> 410
, 5_1(2047) -> 223
, 5_1(2051) -> 2050
, 5_1(2059) -> 223
, 5_1(2067) -> 2066
, 5_1(2069) -> 223
, 5_1(2077) -> 2076
, 5_1(2082) -> 2048
, 5_1(2105) -> 223
, 5_1(2106) -> 223
, 5_1(2108) -> 223
, 5_1(2109) -> 223
, 5_1(2110) -> 2109
, 5_1(2113) -> 2112
, 5_1(2116) -> 223
, 5_1(2118) -> 223
, 5_1(2119) -> 223
, 5_1(2121) -> 223
, 5_1(2122) -> 223
, 5_1(2125) -> 2124
, 5_1(2143) -> 223
, 5_1(2144) -> 223
, 5_1(2157) -> 5
, 5_1(2157) -> 189
, 5_1(2157) -> 2141
, 5_1(2167) -> 223
, 5_1(2169) -> 2168
, 5_1(2173) -> 2172
, 5_1(2174) -> 2158
, 5_1(2175) -> 2174
, 5_1(2189) -> 223
, 5_1(2200) -> 223
, 5_1(2209) -> 2208
, 5_1(2210) -> 223
, 5_1(2220) -> 2219
, 5_1(2223) -> 2222
, 5_1(2230) -> 428
, 5_1(2243) -> 2242
, 5_1(2247) -> 2246
, 5_1(2254) -> 223
, 5_1(2262) -> 2261
, 5_1(2267) -> 223
, 5_1(2269) -> 2268
, 5_1(2278) -> 223
, 5_1(2280) -> 2279
, 5_1(2286) -> 2285
, 5_1(2287) -> 223
, 5_1(2288) -> 223
, 5_1(2289) -> 223
, 5_1(2290) -> 223
, 5_1(2298) -> 223
, 5_1(2299) -> 223
, 5_1(2301) -> 2300
, 5_1(2307) -> 223
, 5_1(2308) -> 223
, 5_1(2309) -> 223
, 5_1(2310) -> 223
, 5_1(2312) -> 2311
, 5_1(2320) -> 223
, 5_1(2330) -> 223
, 5_1(2331) -> 223
, 5_1(2339) -> 2338
, 5_1(2341) -> 2340
, 5_1(2342) -> 223
, 5_1(2355) -> 223
, 5_1(2357) -> 223
, 5_1(2359) -> 2358
, 5_1(2367) -> 223
, 5_1(2372) -> 2371
, 5_1(2409) -> 2308
, 5_1(2410) -> 2409
, 5_1(2419) -> 223
, 5_1(2420) -> 223
, 5_1(2421) -> 2420
, 5_1(2426) -> 2425
, 5_1(2437) -> 2436
, 5_1(2442) -> 223
, 1_0(1) -> 5
, 1_0(2) -> 5
, 1_0(3) -> 5
, 1_0(4) -> 5
, 1_0(5) -> 5
, 1_0(6) -> 5
, 1_1(1) -> 189
, 1_1(2) -> 189
, 1_1(3) -> 189
, 1_1(4) -> 47
, 1_1(5) -> 47
, 1_1(6) -> 47
, 1_1(7) -> 47
, 1_1(11) -> 10
, 1_1(12) -> 11
, 1_1(14) -> 13
, 1_1(15) -> 14
, 1_1(16) -> 15
, 1_1(19) -> 18
, 1_1(20) -> 4
, 1_1(20) -> 106
, 1_1(20) -> 221
, 1_1(20) -> 223
, 1_1(20) -> 354
, 1_1(20) -> 513
, 1_1(20) -> 2408
, 1_1(22) -> 21
, 1_1(34) -> 416
, 1_1(35) -> 244
, 1_1(36) -> 366
, 1_1(37) -> 47
, 1_1(39) -> 38
, 1_1(44) -> 43
, 1_1(45) -> 44
, 1_1(46) -> 47
, 1_1(47) -> 92
, 1_1(48) -> 47
, 1_1(50) -> 49
, 1_1(52) -> 51
, 1_1(55) -> 54
, 1_1(57) -> 56
, 1_1(64) -> 134
, 1_1(67) -> 66
, 1_1(68) -> 67
, 1_1(73) -> 72
, 1_1(74) -> 73
, 1_1(77) -> 2207
, 1_1(78) -> 274
, 1_1(79) -> 47
, 1_1(80) -> 79
, 1_1(81) -> 80
, 1_1(90) -> 89
, 1_1(92) -> 467
, 1_1(93) -> 20
, 1_1(106) -> 105
, 1_1(110) -> 109
, 1_1(112) -> 111
, 1_1(115) -> 114
, 1_1(117) -> 116
, 1_1(119) -> 118
, 1_1(120) -> 977
, 1_1(121) -> 47
, 1_1(122) -> 47
, 1_1(125) -> 124
, 1_1(126) -> 125
, 1_1(127) -> 126
, 1_1(129) -> 128
, 1_1(132) -> 131
, 1_1(133) -> 177
, 1_1(134) -> 273
, 1_1(135) -> 47
, 1_1(143) -> 142
, 1_1(153) -> 152
, 1_1(154) -> 559
, 1_1(156) -> 155
, 1_1(166) -> 165
, 1_1(167) -> 2354
, 1_1(168) -> 167
, 1_1(171) -> 170
, 1_1(173) -> 172
, 1_1(184) -> 183
, 1_1(187) -> 186
, 1_1(188) -> 2125
, 1_1(189) -> 468
, 1_1(190) -> 107
, 1_1(191) -> 190
, 1_1(193) -> 192
, 1_1(195) -> 194
, 1_1(202) -> 381
, 1_1(203) -> 2141
, 1_1(209) -> 208
, 1_1(213) -> 547
, 1_1(215) -> 214
, 1_1(217) -> 216
, 1_1(222) -> 2141
, 1_1(223) -> 316
, 1_1(225) -> 224
, 1_1(231) -> 230
, 1_1(233) -> 232
, 1_1(236) -> 235
, 1_1(240) -> 239
, 1_1(244) -> 243
, 1_1(245) -> 204
, 1_1(247) -> 246
, 1_1(249) -> 248
, 1_1(253) -> 252
, 1_1(262) -> 261
, 1_1(263) -> 1644
, 1_1(264) -> 252
, 1_1(272) -> 271
, 1_1(274) -> 273
, 1_1(275) -> 47
, 1_1(276) -> 275
, 1_1(286) -> 588
, 1_1(289) -> 588
, 1_1(293) -> 292
, 1_1(297) -> 296
, 1_1(301) -> 300
, 1_1(310) -> 309
, 1_1(317) -> 6
, 1_1(317) -> 48
, 1_1(317) -> 120
, 1_1(328) -> 47
, 1_1(343) -> 527
, 1_1(344) -> 290
, 1_1(349) -> 348
, 1_1(352) -> 351
, 1_1(353) -> 352
, 1_1(354) -> 577
, 1_1(366) -> 2452
, 1_1(367) -> 47
, 1_1(372) -> 371
, 1_1(377) -> 376
, 1_1(381) -> 603
, 1_1(382) -> 367
, 1_1(386) -> 385
, 1_1(387) -> 386
, 1_1(390) -> 389
, 1_1(391) -> 390
, 1_1(398) -> 397
, 1_1(406) -> 3
, 1_1(406) -> 19
, 1_1(406) -> 431
, 1_1(406) -> 455
, 1_1(406) -> 1647
, 1_1(406) -> 2068
, 1_1(406) -> 2187
, 1_1(406) -> 2418
, 1_1(407) -> 406
, 1_1(408) -> 407
, 1_1(417) -> 416
, 1_1(421) -> 420
, 1_1(424) -> 423
, 1_1(431) -> 430
, 1_1(432) -> 47
, 1_1(433) -> 432
, 1_1(436) -> 435
, 1_1(442) -> 441
, 1_1(443) -> 442
, 1_1(453) -> 452
, 1_1(454) -> 453
, 1_1(455) -> 15
, 1_1(456) -> 2397
, 1_1(460) -> 459
, 1_1(461) -> 460
, 1_1(463) -> 462
, 1_1(468) -> 467
, 1_1(471) -> 470
, 1_1(477) -> 476
, 1_1(478) -> 2354
, 1_1(479) -> 478
, 1_1(483) -> 482
, 1_1(486) -> 485
, 1_1(487) -> 486
, 1_1(491) -> 490
, 1_1(495) -> 494
, 1_1(502) -> 47
, 1_1(507) -> 506
, 1_1(510) -> 509
, 1_1(512) -> 511
, 1_1(521) -> 520
, 1_1(524) -> 523
, 1_1(527) -> 526
, 1_1(528) -> 527
, 1_1(531) -> 530
, 1_1(536) -> 44
, 1_1(540) -> 539
, 1_1(542) -> 541
, 1_1(549) -> 548
, 1_1(560) -> 47
, 1_1(570) -> 569
, 1_1(575) -> 574
, 1_1(581) -> 580
, 1_1(584) -> 583
, 1_1(586) -> 585
, 1_1(590) -> 47
, 1_1(602) -> 601
, 1_1(620) -> 619
, 1_1(622) -> 621
, 1_1(680) -> 1
, 1_1(682) -> 681
, 1_1(686) -> 685
, 1_1(694) -> 434
, 1_1(703) -> 702
, 1_1(717) -> 716
, 1_1(943) -> 680
, 1_1(953) -> 952
, 1_1(956) -> 382
, 1_1(961) -> 960
, 1_1(1041) -> 1040
, 1_1(1046) -> 1045
, 1_1(1067) -> 1066
, 1_1(1084) -> 1083
, 1_1(1621) -> 1
, 1_1(1621) -> 203
, 1_1(1621) -> 2081
, 1_1(1622) -> 47
, 1_1(1624) -> 1623
, 1_1(1634) -> 2286
, 1_1(1636) -> 1635
, 1_1(1638) -> 1637
, 1_1(1639) -> 1638
, 1_1(1640) -> 1639
, 1_1(1645) -> 1644
, 1_1(1685) -> 1684
, 1_1(2053) -> 2052
, 1_1(2059) -> 5
, 1_1(2059) -> 47
, 1_1(2059) -> 105
, 1_1(2059) -> 189
, 1_1(2059) -> 252
, 1_1(2059) -> 316
, 1_1(2059) -> 366
, 1_1(2059) -> 468
, 1_1(2059) -> 2452
, 1_1(2068) -> 15
, 1_1(2069) -> 2047
, 1_1(2072) -> 2071
, 1_1(2080) -> 131
, 1_1(2093) -> 47
, 1_1(2097) -> 2096
, 1_1(2101) -> 2100
, 1_1(2105) -> 47
, 1_1(2106) -> 2105
, 1_1(2108) -> 2107
, 1_1(2109) -> 2108
, 1_1(2111) -> 2110
, 1_1(2116) -> 1
, 1_1(2118) -> 2117
, 1_1(2119) -> 2118
, 1_1(2121) -> 2120
, 1_1(2122) -> 2121
, 1_1(2139) -> 2138
, 1_1(2142) -> 2141
, 1_1(2143) -> 1
, 1_1(2144) -> 2143
, 1_1(2147) -> 2146
, 1_1(2150) -> 2149
, 1_1(2151) -> 2150
, 1_1(2157) -> 47
, 1_1(2158) -> 2157
, 1_1(2160) -> 2159
, 1_1(2165) -> 2164
, 1_1(2167) -> 2048
, 1_1(2172) -> 2171
, 1_1(2174) -> 47
, 1_1(2181) -> 2180
, 1_1(2185) -> 2184
, 1_1(2186) -> 2185
, 1_1(2189) -> 2188
, 1_1(2193) -> 2192
, 1_1(2200) -> 1
, 1_1(2208) -> 2207
, 1_1(2212) -> 47
, 1_1(2217) -> 2216
, 1_1(2225) -> 2224
, 1_1(2226) -> 2225
, 1_1(2232) -> 2231
, 1_1(2233) -> 2232
, 1_1(2239) -> 2238
, 1_1(2241) -> 47
, 1_1(2248) -> 2247
, 1_1(2252) -> 2251
, 1_1(2254) -> 2059
, 1_1(2265) -> 2264
, 1_1(2275) -> 2274
, 1_1(2277) -> 2276
, 1_1(2281) -> 2280
, 1_1(2287) -> 2060
, 1_1(2288) -> 2287
, 1_1(2289) -> 2288
, 1_1(2290) -> 2289
, 1_1(2293) -> 2292
, 1_1(2294) -> 2293
, 1_1(2296) -> 2295
, 1_1(2298) -> 1
, 1_1(2299) -> 2298
, 1_1(2308) -> 2307
, 1_1(2313) -> 2312
, 1_1(2316) -> 2315
, 1_1(2319) -> 47
, 1_1(2322) -> 2321
, 1_1(2328) -> 2327
, 1_1(2330) -> 2329
, 1_1(2342) -> 47
, 1_1(2343) -> 47
, 1_1(2345) -> 2344
, 1_1(2346) -> 2345
, 1_1(2354) -> 2353
, 1_1(2355) -> 2
, 1_1(2355) -> 36
, 1_1(2355) -> 156
, 1_1(2355) -> 264
, 1_1(2367) -> 1
, 1_1(2377) -> 2376
, 1_1(2385) -> 2384
, 1_1(2387) -> 2386
, 1_1(2393) -> 2392
, 1_1(2398) -> 2397
, 1_1(2402) -> 2401
, 1_1(2403) -> 2402
, 1_1(2413) -> 2412
, 1_1(2417) -> 2416
, 1_1(2418) -> 2417
, 1_1(2419) -> 2342
, 1_1(2428) -> 2320
, 1_1(2433) -> 2432
, 1_1(2442) -> 2441
, 1_1(2446) -> 2445
, 1_1(2447) -> 2446
, 1_1(2450) -> 2449
, 4_0(1) -> 6
, 4_0(2) -> 6
, 4_0(3) -> 6
, 4_0(4) -> 6
, 4_0(5) -> 6
, 4_0(6) -> 6
, 4_1(1) -> 48
, 4_1(2) -> 48
, 4_1(3) -> 48
, 4_1(4) -> 48
, 4_1(5) -> 48
, 4_1(6) -> 48
, 4_1(7) -> 48
, 4_1(9) -> 8
, 4_1(13) -> 12
, 4_1(18) -> 2230
, 4_1(19) -> 120
, 4_1(20) -> 48
, 4_1(21) -> 20
, 4_1(23) -> 22
, 4_1(25) -> 24
, 4_1(27) -> 26
, 4_1(30) -> 29
, 4_1(31) -> 30
, 4_1(33) -> 32
, 4_1(35) -> 34
, 4_1(36) -> 35
, 4_1(37) -> 48
, 4_1(43) -> 42
, 4_1(45) -> 35
, 4_1(46) -> 213
, 4_1(47) -> 46
, 4_1(48) -> 64
, 4_1(49) -> 4
, 4_1(49) -> 17
, 4_1(49) -> 221
, 4_1(49) -> 223
, 4_1(49) -> 353
, 4_1(49) -> 354
, 4_1(49) -> 2398
, 4_1(50) -> 1
, 4_1(54) -> 53
, 4_1(58) -> 57
, 4_1(62) -> 61
, 4_1(63) -> 62
, 4_1(64) -> 78
, 4_1(66) -> 65
, 4_1(71) -> 70
, 4_1(72) -> 71
, 4_1(76) -> 75
, 4_1(77) -> 76
, 4_1(78) -> 2209
, 4_1(79) -> 48
, 4_1(84) -> 83
, 4_1(88) -> 87
, 4_1(89) -> 88
, 4_1(92) -> 1634
, 4_1(93) -> 48
, 4_1(96) -> 95
, 4_1(97) -> 96
, 4_1(98) -> 97
, 4_1(101) -> 100
, 4_1(105) -> 104
, 4_1(106) -> 286
, 4_1(107) -> 21
, 4_1(109) -> 108
, 4_1(111) -> 110
, 4_1(116) -> 229
, 4_1(119) -> 324
, 4_1(120) -> 119
, 4_1(121) -> 48
, 4_1(122) -> 48
, 4_1(123) -> 122
, 4_1(124) -> 123
, 4_1(128) -> 127
, 4_1(133) -> 132
, 4_1(135) -> 48
, 4_1(139) -> 138
, 4_1(142) -> 141
, 4_1(145) -> 514
, 4_1(146) -> 93
, 4_1(147) -> 146
, 4_1(148) -> 147
, 4_1(149) -> 148
, 4_1(152) -> 151
, 4_1(156) -> 418
, 4_1(160) -> 159
, 4_1(162) -> 161
, 4_1(163) -> 162
, 4_1(168) -> 234
, 4_1(170) -> 169
, 4_1(177) -> 176
, 4_1(179) -> 178
, 4_1(185) -> 184
, 4_1(186) -> 185
, 4_1(187) -> 974
, 4_1(188) -> 213
, 4_1(189) -> 188
, 4_1(190) -> 1
, 4_1(191) -> 1
, 4_1(192) -> 191
, 4_1(193) -> 1
, 4_1(194) -> 1
, 4_1(195) -> 1
, 4_1(200) -> 199
, 4_1(202) -> 719
, 4_1(203) -> 202
, 4_1(204) -> 49
, 4_1(206) -> 205
, 4_1(208) -> 207
, 4_1(210) -> 209
, 4_1(211) -> 210
, 4_1(212) -> 211
, 4_1(213) -> 313
, 4_1(218) -> 217
, 4_1(221) -> 220
, 4_1(223) -> 289
, 4_1(228) -> 227
, 4_1(230) -> 229
, 4_1(233) -> 324
, 4_1(234) -> 233
, 4_1(235) -> 48
, 4_1(238) -> 237
, 4_1(242) -> 241
, 4_1(243) -> 242
, 4_1(245) -> 1
, 4_1(246) -> 245
, 4_1(247) -> 1
, 4_1(248) -> 247
, 4_1(249) -> 1
, 4_1(251) -> 250
, 4_1(253) -> 622
, 4_1(255) -> 254
, 4_1(258) -> 257
, 4_1(259) -> 258
, 4_1(260) -> 259
, 4_1(261) -> 260
, 4_1(263) -> 262
, 4_1(264) -> 263
, 4_1(266) -> 265
, 4_1(268) -> 267
, 4_1(269) -> 268
, 4_1(273) -> 272
, 4_1(275) -> 4
, 4_1(276) -> 1
, 4_1(277) -> 276
, 4_1(279) -> 278
, 4_1(280) -> 279
, 4_1(282) -> 281
, 4_1(283) -> 282
, 4_1(284) -> 283
, 4_1(286) -> 75
, 4_1(287) -> 286
, 4_1(289) -> 288
, 4_1(290) -> 6
, 4_1(290) -> 48
, 4_1(290) -> 188
, 4_1(290) -> 289
, 4_1(290) -> 2140
, 4_1(292) -> 291
, 4_1(294) -> 293
, 4_1(295) -> 294
, 4_1(298) -> 297
, 4_1(299) -> 298
, 4_1(304) -> 290
, 4_1(306) -> 305
, 4_1(308) -> 307
, 4_1(311) -> 310
, 4_1(312) -> 311
, 4_1(314) -> 313
, 4_1(315) -> 314
, 4_1(316) -> 315
, 4_1(317) -> 4
, 4_1(318) -> 317
, 4_1(319) -> 318
, 4_1(324) -> 323
, 4_1(325) -> 324
, 4_1(326) -> 325
, 4_1(327) -> 326
, 4_1(328) -> 48
, 4_1(331) -> 330
, 4_1(333) -> 332
, 4_1(334) -> 333
, 4_1(336) -> 328
, 4_1(338) -> 337
, 4_1(339) -> 338
, 4_1(340) -> 339
, 4_1(342) -> 341
, 4_1(343) -> 2058
, 4_1(344) -> 1
, 4_1(345) -> 344
, 4_1(346) -> 345
, 4_1(350) -> 349
, 4_1(355) -> 275
, 4_1(358) -> 357
, 4_1(359) -> 358
, 4_1(361) -> 360
, 4_1(364) -> 363
, 4_1(365) -> 364
, 4_1(367) -> 1
, 4_1(367) -> 203
, 4_1(367) -> 2142
, 4_1(368) -> 48
, 4_1(370) -> 369
, 4_1(371) -> 370
, 4_1(374) -> 373
, 4_1(376) -> 375
, 4_1(378) -> 377
, 4_1(379) -> 378
, 4_1(380) -> 379
, 4_1(381) -> 380
, 4_1(382) -> 1
, 4_1(383) -> 382
, 4_1(393) -> 3
, 4_1(393) -> 19
, 4_1(393) -> 443
, 4_1(393) -> 454
, 4_1(393) -> 1647
, 4_1(393) -> 2187
, 4_1(395) -> 394
, 4_1(397) -> 396
, 4_1(399) -> 398
, 4_1(400) -> 399
, 4_1(405) -> 404
, 4_1(406) -> 4
, 4_1(407) -> 1
, 4_1(407) -> 203
, 4_1(407) -> 222
, 4_1(408) -> 1
, 4_1(408) -> 203
, 4_1(408) -> 444
, 4_1(408) -> 2081
, 4_1(409) -> 46
, 4_1(410) -> 409
, 4_1(411) -> 410
, 4_1(412) -> 411
, 4_1(414) -> 413
, 4_1(418) -> 417
, 4_1(423) -> 422
, 4_1(426) -> 425
, 4_1(427) -> 426
, 4_1(428) -> 427
, 4_1(430) -> 429
, 4_1(432) -> 46
, 4_1(433) -> 1
, 4_1(433) -> 203
, 4_1(433) -> 2142
, 4_1(435) -> 434
, 4_1(437) -> 436
, 4_1(438) -> 437
, 4_1(439) -> 438
, 4_1(440) -> 439
, 4_1(444) -> 2318
, 4_1(445) -> 368
, 4_1(446) -> 445
, 4_1(448) -> 447
, 4_1(449) -> 448
, 4_1(450) -> 449
, 4_1(456) -> 2123
, 4_1(457) -> 48
, 4_1(459) -> 458
, 4_1(466) -> 465
, 4_1(467) -> 466
, 4_1(468) -> 1634
, 4_1(469) -> 407
, 4_1(473) -> 472
, 4_1(475) -> 474
, 4_1(478) -> 477
, 4_1(479) -> 2297
, 4_1(480) -> 393
, 4_1(484) -> 483
, 4_1(485) -> 484
, 4_1(489) -> 488
, 4_1(490) -> 489
, 4_1(492) -> 433
, 4_1(494) -> 493
, 4_1(499) -> 498
, 4_1(501) -> 500
, 4_1(502) -> 46
, 4_1(508) -> 507
, 4_1(509) -> 508
, 4_1(513) -> 512
, 4_1(522) -> 521
, 4_1(523) -> 522
, 4_1(525) -> 524
, 4_1(528) -> 2092
, 4_1(530) -> 529
, 4_1(533) -> 532
, 4_1(537) -> 46
, 4_1(538) -> 537
, 4_1(539) -> 538
, 4_1(544) -> 543
, 4_1(546) -> 545
, 4_1(550) -> 549
, 4_1(552) -> 551
, 4_1(553) -> 552
, 4_1(557) -> 556
, 4_1(558) -> 557
, 4_1(560) -> 48
, 4_1(563) -> 562
, 4_1(564) -> 563
, 4_1(565) -> 564
, 4_1(566) -> 565
, 4_1(568) -> 406
, 4_1(569) -> 568
, 4_1(570) -> 1
, 4_1(573) -> 572
, 4_1(574) -> 573
, 4_1(578) -> 432
, 4_1(579) -> 578
, 4_1(580) -> 579
, 4_1(585) -> 584
, 4_1(590) -> 1
, 4_1(591) -> 590
, 4_1(593) -> 592
, 4_1(595) -> 594
, 4_1(596) -> 595
, 4_1(597) -> 596
, 4_1(598) -> 597
, 4_1(599) -> 598
, 4_1(600) -> 599
, 4_1(603) -> 602
, 4_1(614) -> 469
, 4_1(616) -> 615
, 4_1(619) -> 618
, 4_1(680) -> 4
, 4_1(681) -> 680
, 4_1(682) -> 1
, 4_1(688) -> 687
, 4_1(689) -> 688
, 4_1(702) -> 695
, 4_1(714) -> 704
, 4_1(715) -> 714
, 4_1(718) -> 717
, 4_1(943) -> 1
, 4_1(947) -> 946
, 4_1(949) -> 948
, 4_1(951) -> 950
, 4_1(952) -> 951
, 4_1(956) -> 1
, 4_1(960) -> 956
, 4_1(961) -> 1
, 4_1(968) -> 961
, 4_1(969) -> 968
, 4_1(970) -> 969
, 4_1(972) -> 971
, 4_1(973) -> 972
, 4_1(975) -> 974
, 4_1(976) -> 2253
, 4_1(977) -> 976
, 4_1(1040) -> 1
, 4_1(1041) -> 1
, 4_1(1042) -> 1041
, 4_1(1043) -> 1042
, 4_1(1066) -> 1054
, 4_1(1069) -> 1068
, 4_1(1082) -> 1070
, 4_1(1083) -> 1082
, 4_1(1621) -> 1
, 4_1(1622) -> 46
, 4_1(1627) -> 1626
, 4_1(1628) -> 1627
, 4_1(1631) -> 1630
, 4_1(1632) -> 1631
, 4_1(1633) -> 1632
, 4_1(1634) -> 1633
, 4_1(1635) -> 682
, 4_1(1636) -> 1
, 4_1(1637) -> 1636
, 4_1(1638) -> 1
, 4_1(1639) -> 1
, 4_1(1640) -> 1
, 4_1(1641) -> 1640
, 4_1(1642) -> 1641
, 4_1(1643) -> 1642
, 4_1(1644) -> 1643
, 4_1(1646) -> 1645
, 4_1(1679) -> 1658
, 4_1(1680) -> 1679
, 4_1(1681) -> 1680
, 4_1(1683) -> 1682
, 4_1(2047) -> 5
, 4_1(2047) -> 47
, 4_1(2047) -> 105
, 4_1(2047) -> 189
, 4_1(2047) -> 316
, 4_1(2047) -> 468
, 4_1(2047) -> 577
, 4_1(2047) -> 2141
, 4_1(2048) -> 2047
, 4_1(2050) -> 2049
, 4_1(2055) -> 2054
, 4_1(2058) -> 2104
, 4_1(2059) -> 1
, 4_1(2060) -> 2059
, 4_1(2063) -> 2062
, 4_1(2065) -> 2064
, 4_1(2066) -> 2065
, 4_1(2069) -> 1
, 4_1(2070) -> 2069
, 4_1(2073) -> 2072
, 4_1(2074) -> 2073
, 4_1(2075) -> 2074
, 4_1(2080) -> 2079
, 4_1(2081) -> 2080
, 4_1(2087) -> 2086
, 4_1(2090) -> 2089
, 4_1(2091) -> 543
, 4_1(2092) -> 2104
, 4_1(2093) -> 46
, 4_1(2095) -> 2094
, 4_1(2098) -> 2097
, 4_1(2105) -> 1
, 4_1(2106) -> 1
, 4_1(2107) -> 2106
, 4_1(2108) -> 1
, 4_1(2109) -> 1
, 4_1(2110) -> 46
, 4_1(2114) -> 2113
, 4_1(2116) -> 1
, 4_1(2117) -> 2116
, 4_1(2118) -> 1
, 4_1(2119) -> 1
, 4_1(2120) -> 2119
, 4_1(2121) -> 1
, 4_1(2122) -> 1
, 4_1(2123) -> 363
, 4_1(2124) -> 2123
, 4_1(2138) -> 2137
, 4_1(2140) -> 2139
, 4_1(2141) -> 2140
, 4_1(2143) -> 1
, 4_1(2144) -> 1
, 4_1(2145) -> 2144
, 4_1(2146) -> 2145
, 4_1(2148) -> 2147
, 4_1(2149) -> 2148
, 4_1(2157) -> 48
, 4_1(2159) -> 2158
, 4_1(2161) -> 2160
, 4_1(2166) -> 2165
, 4_1(2167) -> 1
, 4_1(2170) -> 2169
, 4_1(2177) -> 2176
, 4_1(2180) -> 2179
, 4_1(2182) -> 2181
, 4_1(2183) -> 2182
, 4_1(2184) -> 2183
, 4_1(2188) -> 2105
, 4_1(2189) -> 1
, 4_1(2191) -> 2190
, 4_1(2192) -> 2191
, 4_1(2194) -> 2193
, 4_1(2195) -> 2194
, 4_1(2197) -> 2196
, 4_1(2198) -> 2197
, 4_1(2200) -> 1
, 4_1(2201) -> 2200
, 4_1(2206) -> 2205
, 4_1(2210) -> 1
, 4_1(2213) -> 2212
, 4_1(2214) -> 2213
, 4_1(2215) -> 2214
, 4_1(2222) -> 2201
, 4_1(2228) -> 2227
, 4_1(2230) -> 2229
, 4_1(2235) -> 2234
, 4_1(2237) -> 2236
, 4_1(2241) -> 46
, 4_1(2243) -> 1
, 4_1(2245) -> 2244
, 4_1(2246) -> 2245
, 4_1(2249) -> 2248
, 4_1(2250) -> 2249
, 4_1(2251) -> 2250
, 4_1(2254) -> 1
, 4_1(2256) -> 2255
, 4_1(2257) -> 2256
, 4_1(2258) -> 2257
, 4_1(2259) -> 2258
, 4_1(2260) -> 2259
, 4_1(2261) -> 2260
, 4_1(2263) -> 2262
, 4_1(2266) -> 2265
, 4_1(2267) -> 1
, 4_1(2271) -> 2270
, 4_1(2272) -> 2271
, 4_1(2273) -> 2272
, 4_1(2274) -> 2273
, 4_1(2276) -> 2275
, 4_1(2278) -> 1
, 4_1(2279) -> 2278
, 4_1(2283) -> 2282
, 4_1(2285) -> 2284
, 4_1(2287) -> 1
, 4_1(2288) -> 1
, 4_1(2289) -> 1
, 4_1(2290) -> 1
, 4_1(2291) -> 2290
, 4_1(2298) -> 1
, 4_1(2299) -> 1
, 4_1(2300) -> 2299
, 4_1(2301) -> 46
, 4_1(2302) -> 2301
, 4_1(2305) -> 2304
, 4_1(2307) -> 2
, 4_1(2307) -> 36
, 4_1(2307) -> 156
, 4_1(2307) -> 264
, 4_1(2307) -> 1646
, 4_1(2308) -> 1
, 4_1(2309) -> 1
, 4_1(2310) -> 1
, 4_1(2311) -> 2310
, 4_1(2315) -> 2314
, 4_1(2318) -> 2317
, 4_1(2319) -> 46
, 4_1(2320) -> 2319
, 4_1(2321) -> 2320
, 4_1(2325) -> 2324
, 4_1(2329) -> 2307
, 4_1(2330) -> 1
, 4_1(2331) -> 1
, 4_1(2332) -> 2331
, 4_1(2333) -> 2332
, 4_1(2335) -> 2334
, 4_1(2338) -> 2337
, 4_1(2340) -> 2339
, 4_1(2342) -> 1
, 4_1(2343) -> 46
, 4_1(2344) -> 2343
, 4_1(2349) -> 2348
, 4_1(2350) -> 2349
, 4_1(2351) -> 2350
, 4_1(2352) -> 2351
, 4_1(2355) -> 1
, 4_1(2356) -> 2355
, 4_1(2357) -> 1
, 4_1(2358) -> 2357
, 4_1(2361) -> 2360
, 4_1(2362) -> 2361
, 4_1(2363) -> 2362
, 4_1(2364) -> 2363
, 4_1(2366) -> 2365
, 4_1(2367) -> 1
, 4_1(2368) -> 2367
, 4_1(2371) -> 2370
, 4_1(2373) -> 2372
, 4_1(2374) -> 2373
, 4_1(2375) -> 545
, 4_1(2378) -> 2377
, 4_1(2381) -> 2380
, 4_1(2383) -> 2382
, 4_1(2384) -> 2383
, 4_1(2388) -> 2387
, 4_1(2389) -> 2388
, 4_1(2390) -> 2389
, 4_1(2392) -> 2391
, 4_1(2394) -> 2393
, 4_1(2398) -> 364
, 4_1(2400) -> 2399
, 4_1(2405) -> 2404
, 4_1(2409) -> 46
, 4_1(2414) -> 2413
, 4_1(2415) -> 2414
, 4_1(2416) -> 2415
, 4_1(2419) -> 1
, 4_1(2420) -> 1
, 4_1(2421) -> 46
, 4_1(2422) -> 2421
, 4_1(2427) -> 2426
, 4_1(2429) -> 2428
, 4_1(2430) -> 2429
, 4_1(2431) -> 2430
, 4_1(2432) -> 2431
, 4_1(2436) -> 2435
, 4_1(2438) -> 2437
, 4_1(2439) -> 2438
, 4_1(2441) -> 2356
, 4_1(2442) -> 1
, 4_1(2443) -> 2442
, 4_1(2444) -> 2443
, 4_1(2451) -> 2450
, 4_1(2452) -> 2451}
Hurray, we answered YES(?,O(n^1))Tool CDI
stdout:
TIMEOUT
Statistics:
Number of monomials: 0
Last formula building started for bound 0
Last SAT solving started for bound 0Tool EDA
stdout:
TIMEOUT
We consider the following Problem:
Strict Trs:
{ 5(5(5(2(2(3(0(1(0(0(5(3(x1)))))))))))) ->
3(5(4(0(1(1(4(1(1(1(3(5(1(3(x1))))))))))))))
, 5(5(5(1(1(1(2(0(5(0(2(5(x1)))))))))))) ->
1(4(1(4(3(4(0(4(3(3(4(4(0(4(0(4(4(0(x1))))))))))))))))))
, 5(5(4(5(3(3(5(2(5(5(2(2(x1)))))))))))) ->
1(3(2(1(2(5(2(4(1(1(0(4(1(4(x1))))))))))))))
, 5(5(3(5(1(2(3(4(2(5(5(3(x1)))))))))))) ->
4(1(3(1(5(4(1(3(1(4(3(2(2(4(4(0(4(4(x1))))))))))))))))))
, 5(5(1(5(5(4(1(5(2(5(1(1(x1)))))))))))) ->
4(0(4(1(1(0(0(4(4(1(1(5(4(4(5(4(4(4(x1))))))))))))))))))
, 5(5(1(2(3(2(5(3(5(5(0(4(x1)))))))))))) ->
0(1(1(0(3(4(0(3(3(4(4(1(0(5(1(1(4(x1)))))))))))))))))
, 5(5(0(2(3(5(2(1(5(0(5(5(x1)))))))))))) ->
1(1(0(2(4(4(4(2(0(4(5(0(2(4(1(5(4(4(x1))))))))))))))))))
, 5(4(0(2(5(5(3(1(2(3(1(0(x1)))))))))))) ->
1(4(4(2(4(1(4(1(3(3(1(3(1(3(1(4(4(3(x1))))))))))))))))))
, 5(3(3(2(3(1(2(2(1(5(5(0(x1)))))))))))) ->
5(5(4(4(1(1(1(4(1(3(0(1(4(2(1(4(4(x1)))))))))))))))))
, 5(3(2(5(1(5(2(5(0(0(0(5(x1)))))))))))) ->
5(3(2(2(0(4(2(5(4(1(5(2(0(4(x1))))))))))))))
, 5(3(1(5(1(2(2(2(2(5(2(5(x1)))))))))))) ->
1(1(4(4(4(4(5(3(4(1(2(0(1(0(0(x1)))))))))))))))
, 5(3(0(5(5(2(5(3(4(5(2(2(x1)))))))))))) ->
1(1(3(3(2(4(2(4(4(2(2(1(0(1(3(4(x1))))))))))))))))
, 5(3(0(2(3(3(2(5(1(1(4(5(x1)))))))))))) ->
4(3(4(1(0(1(3(3(5(4(1(2(1(4(4(x1)))))))))))))))
, 5(2(5(3(4(0(2(3(3(2(0(3(x1)))))))))))) ->
4(0(5(4(0(3(5(0(1(4(4(1(3(4(1(x1)))))))))))))))
, 5(2(5(0(5(4(2(5(2(2(3(5(x1)))))))))))) ->
1(4(4(1(1(4(1(2(1(0(3(3(3(4(0(2(4(2(x1))))))))))))))))))
, 5(2(3(2(3(0(5(2(4(0(5(5(x1)))))))))))) ->
4(4(2(4(2(4(1(4(4(4(5(4(4(1(x1))))))))))))))
, 5(2(1(2(3(2(1(5(0(3(3(4(x1)))))))))))) ->
1(4(4(0(1(2(1(4(3(0(4(5(2(5(x1))))))))))))))
, 5(2(1(0(3(5(5(1(0(5(0(2(x1)))))))))))) ->
4(4(2(3(1(3(3(4(5(4(1(3(1(4(4(3(4(x1)))))))))))))))))
, 5(1(5(5(2(3(1(3(1(1(0(3(x1)))))))))))) ->
0(0(1(5(4(3(1(5(4(4(1(1(4(0(x1))))))))))))))
, 5(1(3(0(5(2(2(1(4(5(3(1(x1)))))))))))) ->
4(4(1(4(1(4(1(3(4(3(1(0(3(4(x1))))))))))))))
, 5(0(5(3(0(1(1(3(4(0(2(5(x1)))))))))))) ->
3(2(4(3(2(4(4(4(4(1(4(4(0(3(x1))))))))))))))
, 5(0(3(4(4(3(0(3(2(5(0(0(x1)))))))))))) ->
3(3(4(3(4(4(0(2(1(4(1(1(4(4(4(x1)))))))))))))))
, 4(5(5(3(3(5(2(3(2(2(0(5(x1)))))))))))) ->
0(1(4(2(4(4(5(4(4(4(5(5(4(5(4(4(5(x1)))))))))))))))))
, 4(5(5(2(3(1(1(5(5(2(0(5(x1)))))))))))) ->
4(0(4(1(4(4(0(1(4(4(5(1(2(3(2(4(x1))))))))))))))))
, 4(5(3(5(2(1(2(3(3(3(2(5(x1)))))))))))) ->
4(4(5(4(5(4(5(1(4(4(3(4(4(4(1(5(x1))))))))))))))))
, 4(3(5(2(2(1(2(0(2(5(0(0(x1)))))))))))) ->
1(4(4(3(5(5(0(4(4(4(4(3(4(0(x1))))))))))))))
, 4(3(0(3(3(0(2(3(0(5(1(3(x1)))))))))))) ->
0(1(2(2(3(4(5(4(4(3(3(4(4(1(x1))))))))))))))
, 4(3(0(0(1(5(3(2(1(0(1(0(x1)))))))))))) ->
0(1(2(4(5(4(4(4(2(4(3(0(1(4(x1))))))))))))))
, 4(1(2(0(0(0(0(0(1(5(3(1(x1)))))))))))) ->
4(1(4(4(2(5(1(4(3(1(1(5(5(3(x1))))))))))))))
, 4(0(5(0(5(4(3(5(2(2(5(0(x1)))))))))))) ->
0(4(5(2(4(4(0(4(2(0(4(4(5(1(0(x1)))))))))))))))
, 3(5(5(5(2(0(1(2(2(4(2(3(x1)))))))))))) ->
0(2(0(4(4(1(0(4(5(4(1(4(4(4(4(1(4(2(x1))))))))))))))))))
, 3(5(5(2(3(0(0(1(3(2(5(3(x1)))))))))))) ->
0(1(4(0(0(1(1(3(3(1(1(0(0(2(4(x1)))))))))))))))
, 3(5(5(0(0(5(2(2(2(5(5(4(x1)))))))))))) ->
4(3(4(2(4(1(4(4(3(3(2(2(4(3(4(3(x1))))))))))))))))
, 3(5(1(0(3(5(2(1(1(3(5(0(x1)))))))))))) ->
1(1(1(5(4(4(4(3(4(0(5(1(4(4(0(0(x1))))))))))))))))
, 3(5(0(2(5(3(3(2(0(2(2(4(x1)))))))))))) ->
4(3(3(3(1(3(4(1(3(4(4(4(5(4(1(3(1(4(x1))))))))))))))))))
, 3(4(0(3(0(3(5(0(2(3(2(1(x1)))))))))))) ->
3(1(3(4(1(4(4(4(4(0(1(1(3(2(0(x1)))))))))))))))
, 3(3(5(4(3(5(0(0(3(5(2(1(x1)))))))))))) ->
0(2(4(4(0(4(4(4(5(2(1(1(3(3(5(1(4(x1)))))))))))))))))
, 3(3(5(3(3(0(1(2(2(1(1(5(x1)))))))))))) ->
4(2(3(4(1(1(3(1(5(2(4(4(1(1(1(x1)))))))))))))))
, 3(3(5(2(0(2(3(1(1(1(0(5(x1)))))))))))) ->
1(1(4(0(1(2(4(5(4(0(1(4(1(3(4(4(x1))))))))))))))))
, 3(3(5(1(1(5(0(3(5(1(1(1(x1)))))))))))) ->
4(4(3(3(1(4(4(1(1(3(4(4(1(0(1(5(4(4(x1))))))))))))))))))
, 3(3(2(1(5(2(0(4(5(1(0(5(x1)))))))))))) ->
3(1(4(3(4(1(0(5(0(4(0(4(3(1(4(4(x1))))))))))))))))
, 3(2(5(2(2(1(2(5(5(5(0(0(x1)))))))))))) ->
1(3(0(2(0(5(1(4(4(1(3(1(4(5(4(0(4(x1)))))))))))))))))
, 3(2(2(5(2(5(5(1(5(5(1(5(x1)))))))))))) ->
4(4(5(3(3(3(5(3(1(4(4(1(4(3(1(1(0(1(x1))))))))))))))))))
, 3(2(2(1(3(5(5(5(5(3(3(1(x1)))))))))))) ->
1(1(1(3(4(1(2(4(5(2(2(0(4(1(x1))))))))))))))
, 3(2(0(2(1(0(5(0(0(0(1(2(x1)))))))))))) ->
4(5(4(4(1(3(1(5(4(2(4(0(1(4(4(1(x1))))))))))))))))
, 3(2(0(0(5(0(5(5(5(3(5(2(x1)))))))))))) ->
4(0(1(4(2(4(4(0(5(0(4(4(3(1(0(1(0(0(x1))))))))))))))))))
, 3(1(3(3(0(5(5(1(3(0(1(3(x1)))))))))))) ->
1(5(3(2(4(4(4(4(0(2(2(1(4(4(x1))))))))))))))
, 3(0(3(5(5(2(1(4(0(1(3(5(x1)))))))))))) ->
1(4(4(1(3(2(4(4(1(0(0(1(5(3(x1))))))))))))))
, 3(0(2(5(3(1(2(5(0(2(3(1(x1)))))))))))) ->
3(4(4(4(1(5(0(1(4(1(5(0(1(4(5(4(x1))))))))))))))))
, 2(5(2(2(0(0(0(1(1(3(2(2(x1)))))))))))) ->
0(4(5(4(2(4(4(4(4(4(4(3(1(4(1(1(4(2(x1))))))))))))))))))
, 2(5(1(2(5(4(4(3(0(0(5(5(x1)))))))))))) ->
4(4(4(2(4(5(5(4(1(2(1(4(0(3(4(x1)))))))))))))))
, 2(5(0(5(1(2(2(3(3(2(0(3(x1)))))))))))) ->
2(4(1(3(2(0(1(5(4(4(5(3(0(4(4(4(x1))))))))))))))))
, 2(3(5(5(4(0(2(0(0(0(2(0(x1)))))))))))) ->
4(3(1(3(4(1(5(4(4(0(1(4(5(4(4(2(x1))))))))))))))))
, 2(3(2(5(1(0(3(5(0(5(2(3(x1)))))))))))) ->
2(1(3(3(2(4(2(4(0(4(4(1(2(4(4(0(x1))))))))))))))))
, 2(3(2(5(1(0(0(4(3(3(5(3(x1)))))))))))) ->
4(1(1(4(1(4(4(4(0(4(4(3(4(3(4(1(4(3(x1))))))))))))))))))
, 2(2(5(5(3(0(1(2(3(0(2(5(x1)))))))))))) ->
2(0(1(4(4(5(0(1(3(0(2(2(4(3(x1))))))))))))))
, 2(1(5(5(5(2(1(5(1(4(4(1(x1)))))))))))) ->
4(3(0(4(1(0(4(0(4(4(1(2(5(4(4(x1)))))))))))))))
, 2(1(5(2(0(5(0(3(4(5(2(5(x1)))))))))))) ->
1(3(2(1(2(5(4(4(3(0(4(4(4(4(4(1(1(x1)))))))))))))))))
, 2(1(2(5(2(5(0(5(1(2(0(1(x1)))))))))))) ->
2(4(1(4(1(4(1(1(1(4(4(4(4(1(4(0(3(2(x1))))))))))))))))))
, 2(0(3(0(5(0(5(0(5(3(2(2(x1)))))))))))) ->
4(5(4(5(4(4(4(2(4(3(1(0(2(3(4(3(x1))))))))))))))))
, 1(5(5(5(0(4(3(4(3(2(5(3(x1)))))))))))) ->
4(4(3(4(5(3(1(0(4(2(0(0(4(0(1(4(x1))))))))))))))))
, 1(5(4(3(2(3(4(0(0(3(1(3(x1)))))))))))) ->
1(4(3(2(4(2(4(4(5(3(3(5(1(0(x1))))))))))))))
, 1(5(4(0(5(2(5(4(3(5(2(1(x1)))))))))))) ->
4(1(4(3(1(4(4(4(0(5(3(3(4(4(2(1(x1))))))))))))))))
, 1(5(3(5(5(5(2(2(3(5(5(3(x1)))))))))))) ->
4(4(5(3(3(0(2(4(3(3(4(2(2(4(0(1(x1))))))))))))))))
, 1(5(2(5(5(5(3(5(0(2(3(0(x1)))))))))))) ->
1(3(3(4(3(1(4(3(0(1(0(2(2(4(4(0(1(x1)))))))))))))))))
, 1(5(2(3(2(0(5(2(2(5(1(3(x1)))))))))))) ->
0(1(4(1(1(5(1(3(5(4(0(3(1(4(2(x1)))))))))))))))
, 1(5(2(1(1(5(4(0(0(2(2(2(x1)))))))))))) ->
1(2(4(1(1(4(1(1(3(4(5(1(4(1(x1))))))))))))))
, 1(5(0(2(4(3(2(5(5(3(1(3(x1)))))))))))) ->
4(3(2(0(2(2(2(4(1(4(4(1(2(3(x1))))))))))))))
, 1(2(3(5(2(0(0(1(2(0(2(2(x1)))))))))))) ->
2(1(4(4(1(4(4(1(1(2(0(3(3(0(0(4(1(4(x1))))))))))))))))))
, 1(2(3(2(0(5(5(2(0(0(1(2(x1)))))))))))) ->
5(1(4(1(4(2(2(2(1(4(0(4(4(5(x1))))))))))))))
, 1(2(1(3(5(2(2(2(2(1(3(4(x1)))))))))))) ->
4(4(1(0(5(4(3(1(5(5(4(0(4(4(x1))))))))))))))
, 1(2(0(5(5(5(5(3(2(3(2(1(x1)))))))))))) ->
5(1(5(5(0(4(0(0(4(1(4(4(4(1(1(3(3(3(x1))))))))))))))))))
, 1(2(0(5(4(1(5(5(1(3(5(2(x1)))))))))))) ->
0(4(1(3(4(4(1(4(4(0(4(4(3(2(4(4(5(x1)))))))))))))))))
, 1(2(0(5(0(4(1(1(2(5(1(1(x1)))))))))))) ->
2(2(4(3(3(0(3(4(0(1(5(4(4(4(4(x1)))))))))))))))
, 1(2(0(0(5(5(0(5(0(0(0(3(x1)))))))))))) ->
0(2(3(0(4(4(4(0(1(3(3(5(3(3(3(1(4(x1)))))))))))))))))
, 1(1(2(3(3(4(0(5(0(0(0(1(x1)))))))))))) ->
2(2(4(4(5(2(1(1(3(4(3(4(4(1(3(x1)))))))))))))))
, 1(1(2(1(3(5(4(4(0(0(3(2(x1)))))))))))) ->
4(0(1(1(0(4(3(4(3(1(0(0(4(5(x1))))))))))))))
, 1(1(2(1(3(0(3(2(5(3(3(5(x1)))))))))))) ->
3(3(5(3(4(4(5(1(4(4(4(1(3(4(4(1(4(3(x1))))))))))))))))))
, 1(1(0(5(0(5(2(4(2(3(5(2(x1)))))))))))) ->
1(1(3(4(4(4(4(4(4(5(4(3(1(4(3(1(4(3(x1))))))))))))))))))
, 1(0(5(1(3(3(5(5(0(0(2(3(x1)))))))))))) ->
1(0(3(5(3(4(4(4(4(1(4(1(2(4(0(x1)))))))))))))))
, 1(0(5(1(1(5(3(5(2(3(5(3(x1)))))))))))) ->
0(0(4(5(1(2(4(2(4(5(1(4(1(1(x1))))))))))))))
, 1(0(3(5(1(5(1(2(3(0(3(1(x1)))))))))))) ->
1(4(1(1(1(1(4(3(1(1(0(1(3(4(3(4(4(x1)))))))))))))))))
, 0(5(2(1(2(5(0(5(5(3(2(1(x1)))))))))))) ->
2(1(4(5(4(2(3(4(0(2(1(4(4(0(x1))))))))))))))
, 0(5(1(0(5(0(5(3(4(0(5(5(x1)))))))))))) ->
4(1(2(2(4(5(1(3(4(1(0(4(4(2(0(x1)))))))))))))))
, 0(5(0(1(2(5(1(1(2(1(4(2(x1)))))))))))) ->
3(4(4(1(3(0(4(3(3(1(0(1(3(4(4(x1)))))))))))))))
, 0(3(2(5(3(4(0(0(5(5(3(4(x1)))))))))))) ->
4(4(1(2(4(4(0(4(2(0(4(5(4(5(2(4(4(x1)))))))))))))))))
, 0(3(2(0(3(2(0(3(5(2(4(1(x1)))))))))))) ->
0(3(4(1(1(3(3(4(4(4(4(0(1(1(1(3(4(4(x1))))))))))))))))))
, 0(3(0(0(1(5(5(2(4(5(5(5(x1)))))))))))) ->
1(4(2(4(5(0(4(4(4(4(2(4(0(1(4(4(3(x1)))))))))))))))))
, 0(2(1(0(0(1(3(2(0(2(1(5(x1)))))))))))) ->
2(2(4(3(3(4(5(4(4(0(0(1(4(4(x1))))))))))))))
, 0(2(0(3(5(0(5(5(3(1(3(5(x1)))))))))))) ->
4(3(1(4(3(0(4(3(4(4(1(0(4(2(x1))))))))))))))
, 0(1(5(3(0(5(3(2(5(5(1(1(x1)))))))))))) ->
3(4(0(1(4(4(4(2(4(1(4(2(3(0(1(5(1(x1)))))))))))))))))
, 0(0(3(4(2(3(0(0(5(5(2(3(x1)))))))))))) ->
4(4(2(4(0(1(1(0(4(0(2(0(5(5(4(x1)))))))))))))))
, 0(0(3(2(0(3(4(2(2(3(0(5(x1)))))))))))) ->
4(1(5(5(0(0(1(4(4(4(1(1(3(0(x1))))))))))))))
, 0(0(3(0(5(5(0(0(3(3(0(5(x1)))))))))))) ->
0(1(0(5(4(2(3(3(5(4(5(4(4(0(x1))))))))))))))
, 0(0(2(3(1(5(5(0(5(2(4(1(x1)))))))))))) ->
3(4(1(4(4(4(4(1(0(0(4(5(4(4(3(0(4(3(x1))))))))))))))))))
, 0(0(0(0(0(0(3(5(3(0(0(2(x1)))))))))))) ->
1(4(4(1(4(4(0(1(1(3(3(1(4(4(1(1(0(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:
{ 5(5(5(2(2(3(0(1(0(0(5(3(x1)))))))))))) ->
3(5(4(0(1(1(4(1(1(1(3(5(1(3(x1))))))))))))))
, 5(5(5(1(1(1(2(0(5(0(2(5(x1)))))))))))) ->
1(4(1(4(3(4(0(4(3(3(4(4(0(4(0(4(4(0(x1))))))))))))))))))
, 5(5(4(5(3(3(5(2(5(5(2(2(x1)))))))))))) ->
1(3(2(1(2(5(2(4(1(1(0(4(1(4(x1))))))))))))))
, 5(5(3(5(1(2(3(4(2(5(5(3(x1)))))))))))) ->
4(1(3(1(5(4(1(3(1(4(3(2(2(4(4(0(4(4(x1))))))))))))))))))
, 5(5(1(5(5(4(1(5(2(5(1(1(x1)))))))))))) ->
4(0(4(1(1(0(0(4(4(1(1(5(4(4(5(4(4(4(x1))))))))))))))))))
, 5(5(1(2(3(2(5(3(5(5(0(4(x1)))))))))))) ->
0(1(1(0(3(4(0(3(3(4(4(1(0(5(1(1(4(x1)))))))))))))))))
, 5(5(0(2(3(5(2(1(5(0(5(5(x1)))))))))))) ->
1(1(0(2(4(4(4(2(0(4(5(0(2(4(1(5(4(4(x1))))))))))))))))))
, 5(4(0(2(5(5(3(1(2(3(1(0(x1)))))))))))) ->
1(4(4(2(4(1(4(1(3(3(1(3(1(3(1(4(4(3(x1))))))))))))))))))
, 5(3(3(2(3(1(2(2(1(5(5(0(x1)))))))))))) ->
5(5(4(4(1(1(1(4(1(3(0(1(4(2(1(4(4(x1)))))))))))))))))
, 5(3(2(5(1(5(2(5(0(0(0(5(x1)))))))))))) ->
5(3(2(2(0(4(2(5(4(1(5(2(0(4(x1))))))))))))))
, 5(3(1(5(1(2(2(2(2(5(2(5(x1)))))))))))) ->
1(1(4(4(4(4(5(3(4(1(2(0(1(0(0(x1)))))))))))))))
, 5(3(0(5(5(2(5(3(4(5(2(2(x1)))))))))))) ->
1(1(3(3(2(4(2(4(4(2(2(1(0(1(3(4(x1))))))))))))))))
, 5(3(0(2(3(3(2(5(1(1(4(5(x1)))))))))))) ->
4(3(4(1(0(1(3(3(5(4(1(2(1(4(4(x1)))))))))))))))
, 5(2(5(3(4(0(2(3(3(2(0(3(x1)))))))))))) ->
4(0(5(4(0(3(5(0(1(4(4(1(3(4(1(x1)))))))))))))))
, 5(2(5(0(5(4(2(5(2(2(3(5(x1)))))))))))) ->
1(4(4(1(1(4(1(2(1(0(3(3(3(4(0(2(4(2(x1))))))))))))))))))
, 5(2(3(2(3(0(5(2(4(0(5(5(x1)))))))))))) ->
4(4(2(4(2(4(1(4(4(4(5(4(4(1(x1))))))))))))))
, 5(2(1(2(3(2(1(5(0(3(3(4(x1)))))))))))) ->
1(4(4(0(1(2(1(4(3(0(4(5(2(5(x1))))))))))))))
, 5(2(1(0(3(5(5(1(0(5(0(2(x1)))))))))))) ->
4(4(2(3(1(3(3(4(5(4(1(3(1(4(4(3(4(x1)))))))))))))))))
, 5(1(5(5(2(3(1(3(1(1(0(3(x1)))))))))))) ->
0(0(1(5(4(3(1(5(4(4(1(1(4(0(x1))))))))))))))
, 5(1(3(0(5(2(2(1(4(5(3(1(x1)))))))))))) ->
4(4(1(4(1(4(1(3(4(3(1(0(3(4(x1))))))))))))))
, 5(0(5(3(0(1(1(3(4(0(2(5(x1)))))))))))) ->
3(2(4(3(2(4(4(4(4(1(4(4(0(3(x1))))))))))))))
, 5(0(3(4(4(3(0(3(2(5(0(0(x1)))))))))))) ->
3(3(4(3(4(4(0(2(1(4(1(1(4(4(4(x1)))))))))))))))
, 4(5(5(3(3(5(2(3(2(2(0(5(x1)))))))))))) ->
0(1(4(2(4(4(5(4(4(4(5(5(4(5(4(4(5(x1)))))))))))))))))
, 4(5(5(2(3(1(1(5(5(2(0(5(x1)))))))))))) ->
4(0(4(1(4(4(0(1(4(4(5(1(2(3(2(4(x1))))))))))))))))
, 4(5(3(5(2(1(2(3(3(3(2(5(x1)))))))))))) ->
4(4(5(4(5(4(5(1(4(4(3(4(4(4(1(5(x1))))))))))))))))
, 4(3(5(2(2(1(2(0(2(5(0(0(x1)))))))))))) ->
1(4(4(3(5(5(0(4(4(4(4(3(4(0(x1))))))))))))))
, 4(3(0(3(3(0(2(3(0(5(1(3(x1)))))))))))) ->
0(1(2(2(3(4(5(4(4(3(3(4(4(1(x1))))))))))))))
, 4(3(0(0(1(5(3(2(1(0(1(0(x1)))))))))))) ->
0(1(2(4(5(4(4(4(2(4(3(0(1(4(x1))))))))))))))
, 4(1(2(0(0(0(0(0(1(5(3(1(x1)))))))))))) ->
4(1(4(4(2(5(1(4(3(1(1(5(5(3(x1))))))))))))))
, 4(0(5(0(5(4(3(5(2(2(5(0(x1)))))))))))) ->
0(4(5(2(4(4(0(4(2(0(4(4(5(1(0(x1)))))))))))))))
, 3(5(5(5(2(0(1(2(2(4(2(3(x1)))))))))))) ->
0(2(0(4(4(1(0(4(5(4(1(4(4(4(4(1(4(2(x1))))))))))))))))))
, 3(5(5(2(3(0(0(1(3(2(5(3(x1)))))))))))) ->
0(1(4(0(0(1(1(3(3(1(1(0(0(2(4(x1)))))))))))))))
, 3(5(5(0(0(5(2(2(2(5(5(4(x1)))))))))))) ->
4(3(4(2(4(1(4(4(3(3(2(2(4(3(4(3(x1))))))))))))))))
, 3(5(1(0(3(5(2(1(1(3(5(0(x1)))))))))))) ->
1(1(1(5(4(4(4(3(4(0(5(1(4(4(0(0(x1))))))))))))))))
, 3(5(0(2(5(3(3(2(0(2(2(4(x1)))))))))))) ->
4(3(3(3(1(3(4(1(3(4(4(4(5(4(1(3(1(4(x1))))))))))))))))))
, 3(4(0(3(0(3(5(0(2(3(2(1(x1)))))))))))) ->
3(1(3(4(1(4(4(4(4(0(1(1(3(2(0(x1)))))))))))))))
, 3(3(5(4(3(5(0(0(3(5(2(1(x1)))))))))))) ->
0(2(4(4(0(4(4(4(5(2(1(1(3(3(5(1(4(x1)))))))))))))))))
, 3(3(5(3(3(0(1(2(2(1(1(5(x1)))))))))))) ->
4(2(3(4(1(1(3(1(5(2(4(4(1(1(1(x1)))))))))))))))
, 3(3(5(2(0(2(3(1(1(1(0(5(x1)))))))))))) ->
1(1(4(0(1(2(4(5(4(0(1(4(1(3(4(4(x1))))))))))))))))
, 3(3(5(1(1(5(0(3(5(1(1(1(x1)))))))))))) ->
4(4(3(3(1(4(4(1(1(3(4(4(1(0(1(5(4(4(x1))))))))))))))))))
, 3(3(2(1(5(2(0(4(5(1(0(5(x1)))))))))))) ->
3(1(4(3(4(1(0(5(0(4(0(4(3(1(4(4(x1))))))))))))))))
, 3(2(5(2(2(1(2(5(5(5(0(0(x1)))))))))))) ->
1(3(0(2(0(5(1(4(4(1(3(1(4(5(4(0(4(x1)))))))))))))))))
, 3(2(2(5(2(5(5(1(5(5(1(5(x1)))))))))))) ->
4(4(5(3(3(3(5(3(1(4(4(1(4(3(1(1(0(1(x1))))))))))))))))))
, 3(2(2(1(3(5(5(5(5(3(3(1(x1)))))))))))) ->
1(1(1(3(4(1(2(4(5(2(2(0(4(1(x1))))))))))))))
, 3(2(0(2(1(0(5(0(0(0(1(2(x1)))))))))))) ->
4(5(4(4(1(3(1(5(4(2(4(0(1(4(4(1(x1))))))))))))))))
, 3(2(0(0(5(0(5(5(5(3(5(2(x1)))))))))))) ->
4(0(1(4(2(4(4(0(5(0(4(4(3(1(0(1(0(0(x1))))))))))))))))))
, 3(1(3(3(0(5(5(1(3(0(1(3(x1)))))))))))) ->
1(5(3(2(4(4(4(4(0(2(2(1(4(4(x1))))))))))))))
, 3(0(3(5(5(2(1(4(0(1(3(5(x1)))))))))))) ->
1(4(4(1(3(2(4(4(1(0(0(1(5(3(x1))))))))))))))
, 3(0(2(5(3(1(2(5(0(2(3(1(x1)))))))))))) ->
3(4(4(4(1(5(0(1(4(1(5(0(1(4(5(4(x1))))))))))))))))
, 2(5(2(2(0(0(0(1(1(3(2(2(x1)))))))))))) ->
0(4(5(4(2(4(4(4(4(4(4(3(1(4(1(1(4(2(x1))))))))))))))))))
, 2(5(1(2(5(4(4(3(0(0(5(5(x1)))))))))))) ->
4(4(4(2(4(5(5(4(1(2(1(4(0(3(4(x1)))))))))))))))
, 2(5(0(5(1(2(2(3(3(2(0(3(x1)))))))))))) ->
2(4(1(3(2(0(1(5(4(4(5(3(0(4(4(4(x1))))))))))))))))
, 2(3(5(5(4(0(2(0(0(0(2(0(x1)))))))))))) ->
4(3(1(3(4(1(5(4(4(0(1(4(5(4(4(2(x1))))))))))))))))
, 2(3(2(5(1(0(3(5(0(5(2(3(x1)))))))))))) ->
2(1(3(3(2(4(2(4(0(4(4(1(2(4(4(0(x1))))))))))))))))
, 2(3(2(5(1(0(0(4(3(3(5(3(x1)))))))))))) ->
4(1(1(4(1(4(4(4(0(4(4(3(4(3(4(1(4(3(x1))))))))))))))))))
, 2(2(5(5(3(0(1(2(3(0(2(5(x1)))))))))))) ->
2(0(1(4(4(5(0(1(3(0(2(2(4(3(x1))))))))))))))
, 2(1(5(5(5(2(1(5(1(4(4(1(x1)))))))))))) ->
4(3(0(4(1(0(4(0(4(4(1(2(5(4(4(x1)))))))))))))))
, 2(1(5(2(0(5(0(3(4(5(2(5(x1)))))))))))) ->
1(3(2(1(2(5(4(4(3(0(4(4(4(4(4(1(1(x1)))))))))))))))))
, 2(1(2(5(2(5(0(5(1(2(0(1(x1)))))))))))) ->
2(4(1(4(1(4(1(1(1(4(4(4(4(1(4(0(3(2(x1))))))))))))))))))
, 2(0(3(0(5(0(5(0(5(3(2(2(x1)))))))))))) ->
4(5(4(5(4(4(4(2(4(3(1(0(2(3(4(3(x1))))))))))))))))
, 1(5(5(5(0(4(3(4(3(2(5(3(x1)))))))))))) ->
4(4(3(4(5(3(1(0(4(2(0(0(4(0(1(4(x1))))))))))))))))
, 1(5(4(3(2(3(4(0(0(3(1(3(x1)))))))))))) ->
1(4(3(2(4(2(4(4(5(3(3(5(1(0(x1))))))))))))))
, 1(5(4(0(5(2(5(4(3(5(2(1(x1)))))))))))) ->
4(1(4(3(1(4(4(4(0(5(3(3(4(4(2(1(x1))))))))))))))))
, 1(5(3(5(5(5(2(2(3(5(5(3(x1)))))))))))) ->
4(4(5(3(3(0(2(4(3(3(4(2(2(4(0(1(x1))))))))))))))))
, 1(5(2(5(5(5(3(5(0(2(3(0(x1)))))))))))) ->
1(3(3(4(3(1(4(3(0(1(0(2(2(4(4(0(1(x1)))))))))))))))))
, 1(5(2(3(2(0(5(2(2(5(1(3(x1)))))))))))) ->
0(1(4(1(1(5(1(3(5(4(0(3(1(4(2(x1)))))))))))))))
, 1(5(2(1(1(5(4(0(0(2(2(2(x1)))))))))))) ->
1(2(4(1(1(4(1(1(3(4(5(1(4(1(x1))))))))))))))
, 1(5(0(2(4(3(2(5(5(3(1(3(x1)))))))))))) ->
4(3(2(0(2(2(2(4(1(4(4(1(2(3(x1))))))))))))))
, 1(2(3(5(2(0(0(1(2(0(2(2(x1)))))))))))) ->
2(1(4(4(1(4(4(1(1(2(0(3(3(0(0(4(1(4(x1))))))))))))))))))
, 1(2(3(2(0(5(5(2(0(0(1(2(x1)))))))))))) ->
5(1(4(1(4(2(2(2(1(4(0(4(4(5(x1))))))))))))))
, 1(2(1(3(5(2(2(2(2(1(3(4(x1)))))))))))) ->
4(4(1(0(5(4(3(1(5(5(4(0(4(4(x1))))))))))))))
, 1(2(0(5(5(5(5(3(2(3(2(1(x1)))))))))))) ->
5(1(5(5(0(4(0(0(4(1(4(4(4(1(1(3(3(3(x1))))))))))))))))))
, 1(2(0(5(4(1(5(5(1(3(5(2(x1)))))))))))) ->
0(4(1(3(4(4(1(4(4(0(4(4(3(2(4(4(5(x1)))))))))))))))))
, 1(2(0(5(0(4(1(1(2(5(1(1(x1)))))))))))) ->
2(2(4(3(3(0(3(4(0(1(5(4(4(4(4(x1)))))))))))))))
, 1(2(0(0(5(5(0(5(0(0(0(3(x1)))))))))))) ->
0(2(3(0(4(4(4(0(1(3(3(5(3(3(3(1(4(x1)))))))))))))))))
, 1(1(2(3(3(4(0(5(0(0(0(1(x1)))))))))))) ->
2(2(4(4(5(2(1(1(3(4(3(4(4(1(3(x1)))))))))))))))
, 1(1(2(1(3(5(4(4(0(0(3(2(x1)))))))))))) ->
4(0(1(1(0(4(3(4(3(1(0(0(4(5(x1))))))))))))))
, 1(1(2(1(3(0(3(2(5(3(3(5(x1)))))))))))) ->
3(3(5(3(4(4(5(1(4(4(4(1(3(4(4(1(4(3(x1))))))))))))))))))
, 1(1(0(5(0(5(2(4(2(3(5(2(x1)))))))))))) ->
1(1(3(4(4(4(4(4(4(5(4(3(1(4(3(1(4(3(x1))))))))))))))))))
, 1(0(5(1(3(3(5(5(0(0(2(3(x1)))))))))))) ->
1(0(3(5(3(4(4(4(4(1(4(1(2(4(0(x1)))))))))))))))
, 1(0(5(1(1(5(3(5(2(3(5(3(x1)))))))))))) ->
0(0(4(5(1(2(4(2(4(5(1(4(1(1(x1))))))))))))))
, 1(0(3(5(1(5(1(2(3(0(3(1(x1)))))))))))) ->
1(4(1(1(1(1(4(3(1(1(0(1(3(4(3(4(4(x1)))))))))))))))))
, 0(5(2(1(2(5(0(5(5(3(2(1(x1)))))))))))) ->
2(1(4(5(4(2(3(4(0(2(1(4(4(0(x1))))))))))))))
, 0(5(1(0(5(0(5(3(4(0(5(5(x1)))))))))))) ->
4(1(2(2(4(5(1(3(4(1(0(4(4(2(0(x1)))))))))))))))
, 0(5(0(1(2(5(1(1(2(1(4(2(x1)))))))))))) ->
3(4(4(1(3(0(4(3(3(1(0(1(3(4(4(x1)))))))))))))))
, 0(3(2(5(3(4(0(0(5(5(3(4(x1)))))))))))) ->
4(4(1(2(4(4(0(4(2(0(4(5(4(5(2(4(4(x1)))))))))))))))))
, 0(3(2(0(3(2(0(3(5(2(4(1(x1)))))))))))) ->
0(3(4(1(1(3(3(4(4(4(4(0(1(1(1(3(4(4(x1))))))))))))))))))
, 0(3(0(0(1(5(5(2(4(5(5(5(x1)))))))))))) ->
1(4(2(4(5(0(4(4(4(4(2(4(0(1(4(4(3(x1)))))))))))))))))
, 0(2(1(0(0(1(3(2(0(2(1(5(x1)))))))))))) ->
2(2(4(3(3(4(5(4(4(0(0(1(4(4(x1))))))))))))))
, 0(2(0(3(5(0(5(5(3(1(3(5(x1)))))))))))) ->
4(3(1(4(3(0(4(3(4(4(1(0(4(2(x1))))))))))))))
, 0(1(5(3(0(5(3(2(5(5(1(1(x1)))))))))))) ->
3(4(0(1(4(4(4(2(4(1(4(2(3(0(1(5(1(x1)))))))))))))))))
, 0(0(3(4(2(3(0(0(5(5(2(3(x1)))))))))))) ->
4(4(2(4(0(1(1(0(4(0(2(0(5(5(4(x1)))))))))))))))
, 0(0(3(2(0(3(4(2(2(3(0(5(x1)))))))))))) ->
4(1(5(5(0(0(1(4(4(4(1(1(3(0(x1))))))))))))))
, 0(0(3(0(5(5(0(0(3(3(0(5(x1)))))))))))) ->
0(1(0(5(4(2(3(3(5(4(5(4(4(0(x1))))))))))))))
, 0(0(2(3(1(5(5(0(5(2(4(1(x1)))))))))))) ->
3(4(1(4(4(4(4(1(0(0(4(5(4(4(3(0(4(3(x1))))))))))))))))))
, 0(0(0(0(0(0(3(5(3(0(0(2(x1)))))))))))) ->
1(4(4(1(4(4(0(1(1(3(3(1(4(4(1(1(0(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:
{ 5(5(5(2(2(3(0(1(0(0(5(3(x1)))))))))))) ->
3(5(4(0(1(1(4(1(1(1(3(5(1(3(x1))))))))))))))
, 5(5(5(1(1(1(2(0(5(0(2(5(x1)))))))))))) ->
1(4(1(4(3(4(0(4(3(3(4(4(0(4(0(4(4(0(x1))))))))))))))))))
, 5(5(4(5(3(3(5(2(5(5(2(2(x1)))))))))))) ->
1(3(2(1(2(5(2(4(1(1(0(4(1(4(x1))))))))))))))
, 5(5(3(5(1(2(3(4(2(5(5(3(x1)))))))))))) ->
4(1(3(1(5(4(1(3(1(4(3(2(2(4(4(0(4(4(x1))))))))))))))))))
, 5(5(1(5(5(4(1(5(2(5(1(1(x1)))))))))))) ->
4(0(4(1(1(0(0(4(4(1(1(5(4(4(5(4(4(4(x1))))))))))))))))))
, 5(5(1(2(3(2(5(3(5(5(0(4(x1)))))))))))) ->
0(1(1(0(3(4(0(3(3(4(4(1(0(5(1(1(4(x1)))))))))))))))))
, 5(5(0(2(3(5(2(1(5(0(5(5(x1)))))))))))) ->
1(1(0(2(4(4(4(2(0(4(5(0(2(4(1(5(4(4(x1))))))))))))))))))
, 5(4(0(2(5(5(3(1(2(3(1(0(x1)))))))))))) ->
1(4(4(2(4(1(4(1(3(3(1(3(1(3(1(4(4(3(x1))))))))))))))))))
, 5(3(3(2(3(1(2(2(1(5(5(0(x1)))))))))))) ->
5(5(4(4(1(1(1(4(1(3(0(1(4(2(1(4(4(x1)))))))))))))))))
, 5(3(2(5(1(5(2(5(0(0(0(5(x1)))))))))))) ->
5(3(2(2(0(4(2(5(4(1(5(2(0(4(x1))))))))))))))
, 5(3(1(5(1(2(2(2(2(5(2(5(x1)))))))))))) ->
1(1(4(4(4(4(5(3(4(1(2(0(1(0(0(x1)))))))))))))))
, 5(3(0(5(5(2(5(3(4(5(2(2(x1)))))))))))) ->
1(1(3(3(2(4(2(4(4(2(2(1(0(1(3(4(x1))))))))))))))))
, 5(3(0(2(3(3(2(5(1(1(4(5(x1)))))))))))) ->
4(3(4(1(0(1(3(3(5(4(1(2(1(4(4(x1)))))))))))))))
, 5(2(5(3(4(0(2(3(3(2(0(3(x1)))))))))))) ->
4(0(5(4(0(3(5(0(1(4(4(1(3(4(1(x1)))))))))))))))
, 5(2(5(0(5(4(2(5(2(2(3(5(x1)))))))))))) ->
1(4(4(1(1(4(1(2(1(0(3(3(3(4(0(2(4(2(x1))))))))))))))))))
, 5(2(3(2(3(0(5(2(4(0(5(5(x1)))))))))))) ->
4(4(2(4(2(4(1(4(4(4(5(4(4(1(x1))))))))))))))
, 5(2(1(2(3(2(1(5(0(3(3(4(x1)))))))))))) ->
1(4(4(0(1(2(1(4(3(0(4(5(2(5(x1))))))))))))))
, 5(2(1(0(3(5(5(1(0(5(0(2(x1)))))))))))) ->
4(4(2(3(1(3(3(4(5(4(1(3(1(4(4(3(4(x1)))))))))))))))))
, 5(1(5(5(2(3(1(3(1(1(0(3(x1)))))))))))) ->
0(0(1(5(4(3(1(5(4(4(1(1(4(0(x1))))))))))))))
, 5(1(3(0(5(2(2(1(4(5(3(1(x1)))))))))))) ->
4(4(1(4(1(4(1(3(4(3(1(0(3(4(x1))))))))))))))
, 5(0(5(3(0(1(1(3(4(0(2(5(x1)))))))))))) ->
3(2(4(3(2(4(4(4(4(1(4(4(0(3(x1))))))))))))))
, 5(0(3(4(4(3(0(3(2(5(0(0(x1)))))))))))) ->
3(3(4(3(4(4(0(2(1(4(1(1(4(4(4(x1)))))))))))))))
, 4(5(5(3(3(5(2(3(2(2(0(5(x1)))))))))))) ->
0(1(4(2(4(4(5(4(4(4(5(5(4(5(4(4(5(x1)))))))))))))))))
, 4(5(5(2(3(1(1(5(5(2(0(5(x1)))))))))))) ->
4(0(4(1(4(4(0(1(4(4(5(1(2(3(2(4(x1))))))))))))))))
, 4(5(3(5(2(1(2(3(3(3(2(5(x1)))))))))))) ->
4(4(5(4(5(4(5(1(4(4(3(4(4(4(1(5(x1))))))))))))))))
, 4(3(5(2(2(1(2(0(2(5(0(0(x1)))))))))))) ->
1(4(4(3(5(5(0(4(4(4(4(3(4(0(x1))))))))))))))
, 4(3(0(3(3(0(2(3(0(5(1(3(x1)))))))))))) ->
0(1(2(2(3(4(5(4(4(3(3(4(4(1(x1))))))))))))))
, 4(3(0(0(1(5(3(2(1(0(1(0(x1)))))))))))) ->
0(1(2(4(5(4(4(4(2(4(3(0(1(4(x1))))))))))))))
, 4(1(2(0(0(0(0(0(1(5(3(1(x1)))))))))))) ->
4(1(4(4(2(5(1(4(3(1(1(5(5(3(x1))))))))))))))
, 4(0(5(0(5(4(3(5(2(2(5(0(x1)))))))))))) ->
0(4(5(2(4(4(0(4(2(0(4(4(5(1(0(x1)))))))))))))))
, 3(5(5(5(2(0(1(2(2(4(2(3(x1)))))))))))) ->
0(2(0(4(4(1(0(4(5(4(1(4(4(4(4(1(4(2(x1))))))))))))))))))
, 3(5(5(2(3(0(0(1(3(2(5(3(x1)))))))))))) ->
0(1(4(0(0(1(1(3(3(1(1(0(0(2(4(x1)))))))))))))))
, 3(5(5(0(0(5(2(2(2(5(5(4(x1)))))))))))) ->
4(3(4(2(4(1(4(4(3(3(2(2(4(3(4(3(x1))))))))))))))))
, 3(5(1(0(3(5(2(1(1(3(5(0(x1)))))))))))) ->
1(1(1(5(4(4(4(3(4(0(5(1(4(4(0(0(x1))))))))))))))))
, 3(5(0(2(5(3(3(2(0(2(2(4(x1)))))))))))) ->
4(3(3(3(1(3(4(1(3(4(4(4(5(4(1(3(1(4(x1))))))))))))))))))
, 3(4(0(3(0(3(5(0(2(3(2(1(x1)))))))))))) ->
3(1(3(4(1(4(4(4(4(0(1(1(3(2(0(x1)))))))))))))))
, 3(3(5(4(3(5(0(0(3(5(2(1(x1)))))))))))) ->
0(2(4(4(0(4(4(4(5(2(1(1(3(3(5(1(4(x1)))))))))))))))))
, 3(3(5(3(3(0(1(2(2(1(1(5(x1)))))))))))) ->
4(2(3(4(1(1(3(1(5(2(4(4(1(1(1(x1)))))))))))))))
, 3(3(5(2(0(2(3(1(1(1(0(5(x1)))))))))))) ->
1(1(4(0(1(2(4(5(4(0(1(4(1(3(4(4(x1))))))))))))))))
, 3(3(5(1(1(5(0(3(5(1(1(1(x1)))))))))))) ->
4(4(3(3(1(4(4(1(1(3(4(4(1(0(1(5(4(4(x1))))))))))))))))))
, 3(3(2(1(5(2(0(4(5(1(0(5(x1)))))))))))) ->
3(1(4(3(4(1(0(5(0(4(0(4(3(1(4(4(x1))))))))))))))))
, 3(2(5(2(2(1(2(5(5(5(0(0(x1)))))))))))) ->
1(3(0(2(0(5(1(4(4(1(3(1(4(5(4(0(4(x1)))))))))))))))))
, 3(2(2(5(2(5(5(1(5(5(1(5(x1)))))))))))) ->
4(4(5(3(3(3(5(3(1(4(4(1(4(3(1(1(0(1(x1))))))))))))))))))
, 3(2(2(1(3(5(5(5(5(3(3(1(x1)))))))))))) ->
1(1(1(3(4(1(2(4(5(2(2(0(4(1(x1))))))))))))))
, 3(2(0(2(1(0(5(0(0(0(1(2(x1)))))))))))) ->
4(5(4(4(1(3(1(5(4(2(4(0(1(4(4(1(x1))))))))))))))))
, 3(2(0(0(5(0(5(5(5(3(5(2(x1)))))))))))) ->
4(0(1(4(2(4(4(0(5(0(4(4(3(1(0(1(0(0(x1))))))))))))))))))
, 3(1(3(3(0(5(5(1(3(0(1(3(x1)))))))))))) ->
1(5(3(2(4(4(4(4(0(2(2(1(4(4(x1))))))))))))))
, 3(0(3(5(5(2(1(4(0(1(3(5(x1)))))))))))) ->
1(4(4(1(3(2(4(4(1(0(0(1(5(3(x1))))))))))))))
, 3(0(2(5(3(1(2(5(0(2(3(1(x1)))))))))))) ->
3(4(4(4(1(5(0(1(4(1(5(0(1(4(5(4(x1))))))))))))))))
, 2(5(2(2(0(0(0(1(1(3(2(2(x1)))))))))))) ->
0(4(5(4(2(4(4(4(4(4(4(3(1(4(1(1(4(2(x1))))))))))))))))))
, 2(5(1(2(5(4(4(3(0(0(5(5(x1)))))))))))) ->
4(4(4(2(4(5(5(4(1(2(1(4(0(3(4(x1)))))))))))))))
, 2(5(0(5(1(2(2(3(3(2(0(3(x1)))))))))))) ->
2(4(1(3(2(0(1(5(4(4(5(3(0(4(4(4(x1))))))))))))))))
, 2(3(5(5(4(0(2(0(0(0(2(0(x1)))))))))))) ->
4(3(1(3(4(1(5(4(4(0(1(4(5(4(4(2(x1))))))))))))))))
, 2(3(2(5(1(0(3(5(0(5(2(3(x1)))))))))))) ->
2(1(3(3(2(4(2(4(0(4(4(1(2(4(4(0(x1))))))))))))))))
, 2(3(2(5(1(0(0(4(3(3(5(3(x1)))))))))))) ->
4(1(1(4(1(4(4(4(0(4(4(3(4(3(4(1(4(3(x1))))))))))))))))))
, 2(2(5(5(3(0(1(2(3(0(2(5(x1)))))))))))) ->
2(0(1(4(4(5(0(1(3(0(2(2(4(3(x1))))))))))))))
, 2(1(5(5(5(2(1(5(1(4(4(1(x1)))))))))))) ->
4(3(0(4(1(0(4(0(4(4(1(2(5(4(4(x1)))))))))))))))
, 2(1(5(2(0(5(0(3(4(5(2(5(x1)))))))))))) ->
1(3(2(1(2(5(4(4(3(0(4(4(4(4(4(1(1(x1)))))))))))))))))
, 2(1(2(5(2(5(0(5(1(2(0(1(x1)))))))))))) ->
2(4(1(4(1(4(1(1(1(4(4(4(4(1(4(0(3(2(x1))))))))))))))))))
, 2(0(3(0(5(0(5(0(5(3(2(2(x1)))))))))))) ->
4(5(4(5(4(4(4(2(4(3(1(0(2(3(4(3(x1))))))))))))))))
, 1(5(5(5(0(4(3(4(3(2(5(3(x1)))))))))))) ->
4(4(3(4(5(3(1(0(4(2(0(0(4(0(1(4(x1))))))))))))))))
, 1(5(4(3(2(3(4(0(0(3(1(3(x1)))))))))))) ->
1(4(3(2(4(2(4(4(5(3(3(5(1(0(x1))))))))))))))
, 1(5(4(0(5(2(5(4(3(5(2(1(x1)))))))))))) ->
4(1(4(3(1(4(4(4(0(5(3(3(4(4(2(1(x1))))))))))))))))
, 1(5(3(5(5(5(2(2(3(5(5(3(x1)))))))))))) ->
4(4(5(3(3(0(2(4(3(3(4(2(2(4(0(1(x1))))))))))))))))
, 1(5(2(5(5(5(3(5(0(2(3(0(x1)))))))))))) ->
1(3(3(4(3(1(4(3(0(1(0(2(2(4(4(0(1(x1)))))))))))))))))
, 1(5(2(3(2(0(5(2(2(5(1(3(x1)))))))))))) ->
0(1(4(1(1(5(1(3(5(4(0(3(1(4(2(x1)))))))))))))))
, 1(5(2(1(1(5(4(0(0(2(2(2(x1)))))))))))) ->
1(2(4(1(1(4(1(1(3(4(5(1(4(1(x1))))))))))))))
, 1(5(0(2(4(3(2(5(5(3(1(3(x1)))))))))))) ->
4(3(2(0(2(2(2(4(1(4(4(1(2(3(x1))))))))))))))
, 1(2(3(5(2(0(0(1(2(0(2(2(x1)))))))))))) ->
2(1(4(4(1(4(4(1(1(2(0(3(3(0(0(4(1(4(x1))))))))))))))))))
, 1(2(3(2(0(5(5(2(0(0(1(2(x1)))))))))))) ->
5(1(4(1(4(2(2(2(1(4(0(4(4(5(x1))))))))))))))
, 1(2(1(3(5(2(2(2(2(1(3(4(x1)))))))))))) ->
4(4(1(0(5(4(3(1(5(5(4(0(4(4(x1))))))))))))))
, 1(2(0(5(5(5(5(3(2(3(2(1(x1)))))))))))) ->
5(1(5(5(0(4(0(0(4(1(4(4(4(1(1(3(3(3(x1))))))))))))))))))
, 1(2(0(5(4(1(5(5(1(3(5(2(x1)))))))))))) ->
0(4(1(3(4(4(1(4(4(0(4(4(3(2(4(4(5(x1)))))))))))))))))
, 1(2(0(5(0(4(1(1(2(5(1(1(x1)))))))))))) ->
2(2(4(3(3(0(3(4(0(1(5(4(4(4(4(x1)))))))))))))))
, 1(2(0(0(5(5(0(5(0(0(0(3(x1)))))))))))) ->
0(2(3(0(4(4(4(0(1(3(3(5(3(3(3(1(4(x1)))))))))))))))))
, 1(1(2(3(3(4(0(5(0(0(0(1(x1)))))))))))) ->
2(2(4(4(5(2(1(1(3(4(3(4(4(1(3(x1)))))))))))))))
, 1(1(2(1(3(5(4(4(0(0(3(2(x1)))))))))))) ->
4(0(1(1(0(4(3(4(3(1(0(0(4(5(x1))))))))))))))
, 1(1(2(1(3(0(3(2(5(3(3(5(x1)))))))))))) ->
3(3(5(3(4(4(5(1(4(4(4(1(3(4(4(1(4(3(x1))))))))))))))))))
, 1(1(0(5(0(5(2(4(2(3(5(2(x1)))))))))))) ->
1(1(3(4(4(4(4(4(4(5(4(3(1(4(3(1(4(3(x1))))))))))))))))))
, 1(0(5(1(3(3(5(5(0(0(2(3(x1)))))))))))) ->
1(0(3(5(3(4(4(4(4(1(4(1(2(4(0(x1)))))))))))))))
, 1(0(5(1(1(5(3(5(2(3(5(3(x1)))))))))))) ->
0(0(4(5(1(2(4(2(4(5(1(4(1(1(x1))))))))))))))
, 1(0(3(5(1(5(1(2(3(0(3(1(x1)))))))))))) ->
1(4(1(1(1(1(4(3(1(1(0(1(3(4(3(4(4(x1)))))))))))))))))
, 0(5(2(1(2(5(0(5(5(3(2(1(x1)))))))))))) ->
2(1(4(5(4(2(3(4(0(2(1(4(4(0(x1))))))))))))))
, 0(5(1(0(5(0(5(3(4(0(5(5(x1)))))))))))) ->
4(1(2(2(4(5(1(3(4(1(0(4(4(2(0(x1)))))))))))))))
, 0(5(0(1(2(5(1(1(2(1(4(2(x1)))))))))))) ->
3(4(4(1(3(0(4(3(3(1(0(1(3(4(4(x1)))))))))))))))
, 0(3(2(5(3(4(0(0(5(5(3(4(x1)))))))))))) ->
4(4(1(2(4(4(0(4(2(0(4(5(4(5(2(4(4(x1)))))))))))))))))
, 0(3(2(0(3(2(0(3(5(2(4(1(x1)))))))))))) ->
0(3(4(1(1(3(3(4(4(4(4(0(1(1(1(3(4(4(x1))))))))))))))))))
, 0(3(0(0(1(5(5(2(4(5(5(5(x1)))))))))))) ->
1(4(2(4(5(0(4(4(4(4(2(4(0(1(4(4(3(x1)))))))))))))))))
, 0(2(1(0(0(1(3(2(0(2(1(5(x1)))))))))))) ->
2(2(4(3(3(4(5(4(4(0(0(1(4(4(x1))))))))))))))
, 0(2(0(3(5(0(5(5(3(1(3(5(x1)))))))))))) ->
4(3(1(4(3(0(4(3(4(4(1(0(4(2(x1))))))))))))))
, 0(1(5(3(0(5(3(2(5(5(1(1(x1)))))))))))) ->
3(4(0(1(4(4(4(2(4(1(4(2(3(0(1(5(1(x1)))))))))))))))))
, 0(0(3(4(2(3(0(0(5(5(2(3(x1)))))))))))) ->
4(4(2(4(0(1(1(0(4(0(2(0(5(5(4(x1)))))))))))))))
, 0(0(3(2(0(3(4(2(2(3(0(5(x1)))))))))))) ->
4(1(5(5(0(0(1(4(4(4(1(1(3(0(x1))))))))))))))
, 0(0(3(0(5(5(0(0(3(3(0(5(x1)))))))))))) ->
0(1(0(5(4(2(3(3(5(4(5(4(4(0(x1))))))))))))))
, 0(0(2(3(1(5(5(0(5(2(4(1(x1)))))))))))) ->
3(4(1(4(4(4(4(1(0(0(4(5(4(4(3(0(4(3(x1))))))))))))))))))
, 0(0(0(0(0(0(3(5(3(0(0(2(x1)))))))))))) ->
1(4(4(1(4(4(0(1(1(3(3(1(4(4(1(1(0(x1)))))))))))))))))}
StartTerms: all
Strategy: none
Certificate: TIMEOUT
Proof:
Computation stopped due to timeout after 60.0 seconds.
Arrrr..