Tool CaT
stdout:
YES(?,O(n^1))
Problem:
0(0(1(x1))) -> 0(1(2(0(x1))))
0(0(1(x1))) -> 0(3(1(0(x1))))
0(0(1(x1))) -> 1(0(4(0(x1))))
0(0(1(x1))) -> 0(1(3(0(2(x1)))))
0(0(1(x1))) -> 0(1(3(0(4(x1)))))
0(0(1(x1))) -> 0(2(0(1(2(x1)))))
0(0(1(x1))) -> 0(3(0(1(2(x1)))))
0(0(1(x1))) -> 0(3(0(3(1(x1)))))
0(0(1(x1))) -> 0(4(0(4(1(x1)))))
0(0(1(x1))) -> 1(2(0(2(0(x1)))))
0(0(1(x1))) -> 1(2(2(0(0(x1)))))
0(0(1(x1))) -> 0(0(2(2(1(2(x1))))))
0(0(1(x1))) -> 0(1(2(4(2(0(x1))))))
0(0(1(x1))) -> 1(2(0(3(0(4(x1))))))
0(1(1(x1))) -> 0(2(1(1(x1))))
0(1(1(x1))) -> 0(3(1(1(x1))))
0(1(1(x1))) -> 1(1(3(0(4(x1)))))
0(1(1(x1))) -> 1(2(0(2(1(x1)))))
0(1(1(x1))) -> 1(0(3(1(2(4(x1))))))
0(1(1(x1))) -> 1(0(4(2(1(2(x1))))))
0(1(1(x1))) -> 1(1(2(4(3(0(x1))))))
0(1(1(x1))) -> 1(2(1(0(4(4(x1))))))
0(1(1(x1))) -> 1(2(2(1(3(0(x1))))))
0(5(1(x1))) -> 0(3(1(5(x1))))
0(5(1(x1))) -> 0(4(5(1(x1))))
0(5(1(x1))) -> 0(2(3(1(5(x1)))))
0(5(1(x1))) -> 0(3(1(5(2(x1)))))
0(5(1(x1))) -> 0(3(1(2(5(2(x1))))))
5(0(1(x1))) -> 5(1(2(4(0(x1)))))
5(0(1(x1))) -> 5(0(2(1(2(4(x1))))))
5(0(1(x1))) -> 5(1(2(3(0(4(x1))))))
0(0(1(5(x1)))) -> 0(4(1(0(5(x1)))))
0(0(2(1(x1)))) -> 2(0(3(0(2(1(x1))))))
0(0(2(1(x1)))) -> 2(3(0(2(0(1(x1))))))
0(1(0(1(x1)))) -> 1(0(2(0(1(x1)))))
0(1(1(1(x1)))) -> 1(1(3(1(0(x1)))))
5(0(1(1(x1)))) -> 1(5(1(2(0(x1)))))
5(3(0(1(x1)))) -> 5(1(2(3(0(x1)))))
5(3(1(5(x1)))) -> 5(3(1(2(5(x1)))))
5(3(2(1(x1)))) -> 1(2(3(5(2(x1)))))
5(4(0(1(x1)))) -> 1(2(5(0(4(x1)))))
0(0(5(1(5(x1))))) -> 1(2(5(5(0(0(x1))))))
0(5(3(0(1(x1))))) -> 1(0(5(3(0(4(x1))))))
0(5(3(4(1(x1))))) -> 1(0(3(5(4(5(x1))))))
0(5(4(0(1(x1))))) -> 0(1(3(0(4(5(x1))))))
5(4(2(1(1(x1))))) -> 5(4(1(2(1(2(x1))))))
Proof:
Bounds Processor:
bound: 1
enrichment: match
automaton:
final states: {6,5}
transitions:
51(142) -> 143*
51(149) -> 150*
41(55) -> 56*
41(47) -> 48*
41(119) -> 120*
41(99) -> 100*
41(49) -> 50*
41(148) -> 149*
41(78) -> 79*
41(33) -> 34*
11(25) -> 26*
11(147) -> 148*
11(37) -> 38*
11(17) -> 18*
11(12) -> 13*
11(121) -> 122*
11(76) -> 77*
11(71) -> 72*
11(36) -> 37*
11(133) -> 134*
11(23) -> 24*
11(13) -> 14*
11(145) -> 146*
11(130) -> 131*
21(75) -> 76*
21(70) -> 71*
21(87) -> 88*
21(77) -> 78*
21(57) -> 58*
21(144) -> 145*
21(89) -> 90*
21(59) -> 60*
21(14) -> 15*
21(131) -> 132*
21(100) -> 101*
21(95) -> 96*
31(35) -> 36*
31(72) -> 73*
31(31) -> 32*
31(143) -> 144*
31(98) -> 99*
01(15) -> 16*
01(117) -> 118*
01(97) -> 98*
01(109) -> 110*
01(34) -> 35*
01(111) -> 112*
01(73) -> 74*
01(58) -> 59*
01(120) -> 121*
00(2) -> 5*
00(4) -> 5*
00(1) -> 5*
00(3) -> 5*
10(2) -> 1*
10(4) -> 1*
10(1) -> 1*
10(3) -> 1*
20(2) -> 2*
20(4) -> 2*
20(1) -> 2*
20(3) -> 2*
30(2) -> 3*
30(4) -> 3*
30(1) -> 3*
30(3) -> 3*
40(2) -> 4*
40(4) -> 4*
40(1) -> 4*
40(3) -> 4*
50(2) -> 6*
50(4) -> 6*
50(1) -> 6*
50(3) -> 6*
1 -> 111,89,49,23
2 -> 97,75,33,12
3 -> 117,95,55,25
4 -> 109,87,47,17
13 -> 57*
14 -> 31*
16 -> 112,133,5
18 -> 13*
24 -> 13*
26 -> 13*
32 -> 15*
34 -> 119,70
38 -> 112,133,5
48 -> 34*
50 -> 34*
56 -> 34*
60 -> 37*
74 -> 37*
76 -> 142*
78 -> 147*
79 -> 73*
88 -> 76*
90 -> 76*
96 -> 76*
98 -> 133*
99 -> 130*
101 -> 36*
110 -> 98*
112 -> 98*
118 -> 98*
122 -> 59*
132 -> 59*
134 -> 35*
146 -> 6*
150 -> 6*
problem:
QedTool IRC1
stdout:
MAYBE
Tool IRC2
stdout:
YES(?,O(n^1))
'Fastest (timeout of 60.0 seconds)'
-----------------------------------
Answer: YES(?,O(n^1))
Input Problem: innermost runtime-complexity with respect to
Rules:
{ 0(0(1(x1))) -> 0(1(2(0(x1))))
, 0(0(1(x1))) -> 0(3(1(0(x1))))
, 0(0(1(x1))) -> 1(0(4(0(x1))))
, 0(0(1(x1))) -> 0(1(3(0(2(x1)))))
, 0(0(1(x1))) -> 0(1(3(0(4(x1)))))
, 0(0(1(x1))) -> 0(2(0(1(2(x1)))))
, 0(0(1(x1))) -> 0(3(0(1(2(x1)))))
, 0(0(1(x1))) -> 0(3(0(3(1(x1)))))
, 0(0(1(x1))) -> 0(4(0(4(1(x1)))))
, 0(0(1(x1))) -> 1(2(0(2(0(x1)))))
, 0(0(1(x1))) -> 1(2(2(0(0(x1)))))
, 0(0(1(x1))) -> 0(0(2(2(1(2(x1))))))
, 0(0(1(x1))) -> 0(1(2(4(2(0(x1))))))
, 0(0(1(x1))) -> 1(2(0(3(0(4(x1))))))
, 0(1(1(x1))) -> 0(2(1(1(x1))))
, 0(1(1(x1))) -> 0(3(1(1(x1))))
, 0(1(1(x1))) -> 1(1(3(0(4(x1)))))
, 0(1(1(x1))) -> 1(2(0(2(1(x1)))))
, 0(1(1(x1))) -> 1(0(3(1(2(4(x1))))))
, 0(1(1(x1))) -> 1(0(4(2(1(2(x1))))))
, 0(1(1(x1))) -> 1(1(2(4(3(0(x1))))))
, 0(1(1(x1))) -> 1(2(1(0(4(4(x1))))))
, 0(1(1(x1))) -> 1(2(2(1(3(0(x1))))))
, 0(5(1(x1))) -> 0(3(1(5(x1))))
, 0(5(1(x1))) -> 0(4(5(1(x1))))
, 0(5(1(x1))) -> 0(2(3(1(5(x1)))))
, 0(5(1(x1))) -> 0(3(1(5(2(x1)))))
, 0(5(1(x1))) -> 0(3(1(2(5(2(x1))))))
, 5(0(1(x1))) -> 5(1(2(4(0(x1)))))
, 5(0(1(x1))) -> 5(0(2(1(2(4(x1))))))
, 5(0(1(x1))) -> 5(1(2(3(0(4(x1))))))
, 0(0(1(5(x1)))) -> 0(4(1(0(5(x1)))))
, 0(0(2(1(x1)))) -> 2(0(3(0(2(1(x1))))))
, 0(0(2(1(x1)))) -> 2(3(0(2(0(1(x1))))))
, 0(1(0(1(x1)))) -> 1(0(2(0(1(x1)))))
, 0(1(1(1(x1)))) -> 1(1(3(1(0(x1)))))
, 5(0(1(1(x1)))) -> 1(5(1(2(0(x1)))))
, 5(3(0(1(x1)))) -> 5(1(2(3(0(x1)))))
, 5(3(1(5(x1)))) -> 5(3(1(2(5(x1)))))
, 5(3(2(1(x1)))) -> 1(2(3(5(2(x1)))))
, 5(4(0(1(x1)))) -> 1(2(5(0(4(x1)))))
, 0(0(5(1(5(x1))))) -> 1(2(5(5(0(0(x1))))))
, 0(5(3(0(1(x1))))) -> 1(0(5(3(0(4(x1))))))
, 0(5(3(4(1(x1))))) -> 1(0(3(5(4(5(x1))))))
, 0(5(4(0(1(x1))))) -> 0(1(3(0(4(5(x1))))))
, 5(4(2(1(1(x1))))) -> 5(4(1(2(1(2(x1))))))}
Proof Output:
'Bounds with minimal-enrichment and initial automaton 'match'' proved the best result:
Details:
--------
'Bounds with minimal-enrichment and initial automaton 'match'' succeeded with the following output:
'Bounds with minimal-enrichment and initial automaton 'match''
--------------------------------------------------------------
Answer: YES(?,O(n^1))
Input Problem: innermost runtime-complexity with respect to
Rules:
{ 0(0(1(x1))) -> 0(1(2(0(x1))))
, 0(0(1(x1))) -> 0(3(1(0(x1))))
, 0(0(1(x1))) -> 1(0(4(0(x1))))
, 0(0(1(x1))) -> 0(1(3(0(2(x1)))))
, 0(0(1(x1))) -> 0(1(3(0(4(x1)))))
, 0(0(1(x1))) -> 0(2(0(1(2(x1)))))
, 0(0(1(x1))) -> 0(3(0(1(2(x1)))))
, 0(0(1(x1))) -> 0(3(0(3(1(x1)))))
, 0(0(1(x1))) -> 0(4(0(4(1(x1)))))
, 0(0(1(x1))) -> 1(2(0(2(0(x1)))))
, 0(0(1(x1))) -> 1(2(2(0(0(x1)))))
, 0(0(1(x1))) -> 0(0(2(2(1(2(x1))))))
, 0(0(1(x1))) -> 0(1(2(4(2(0(x1))))))
, 0(0(1(x1))) -> 1(2(0(3(0(4(x1))))))
, 0(1(1(x1))) -> 0(2(1(1(x1))))
, 0(1(1(x1))) -> 0(3(1(1(x1))))
, 0(1(1(x1))) -> 1(1(3(0(4(x1)))))
, 0(1(1(x1))) -> 1(2(0(2(1(x1)))))
, 0(1(1(x1))) -> 1(0(3(1(2(4(x1))))))
, 0(1(1(x1))) -> 1(0(4(2(1(2(x1))))))
, 0(1(1(x1))) -> 1(1(2(4(3(0(x1))))))
, 0(1(1(x1))) -> 1(2(1(0(4(4(x1))))))
, 0(1(1(x1))) -> 1(2(2(1(3(0(x1))))))
, 0(5(1(x1))) -> 0(3(1(5(x1))))
, 0(5(1(x1))) -> 0(4(5(1(x1))))
, 0(5(1(x1))) -> 0(2(3(1(5(x1)))))
, 0(5(1(x1))) -> 0(3(1(5(2(x1)))))
, 0(5(1(x1))) -> 0(3(1(2(5(2(x1))))))
, 5(0(1(x1))) -> 5(1(2(4(0(x1)))))
, 5(0(1(x1))) -> 5(0(2(1(2(4(x1))))))
, 5(0(1(x1))) -> 5(1(2(3(0(4(x1))))))
, 0(0(1(5(x1)))) -> 0(4(1(0(5(x1)))))
, 0(0(2(1(x1)))) -> 2(0(3(0(2(1(x1))))))
, 0(0(2(1(x1)))) -> 2(3(0(2(0(1(x1))))))
, 0(1(0(1(x1)))) -> 1(0(2(0(1(x1)))))
, 0(1(1(1(x1)))) -> 1(1(3(1(0(x1)))))
, 5(0(1(1(x1)))) -> 1(5(1(2(0(x1)))))
, 5(3(0(1(x1)))) -> 5(1(2(3(0(x1)))))
, 5(3(1(5(x1)))) -> 5(3(1(2(5(x1)))))
, 5(3(2(1(x1)))) -> 1(2(3(5(2(x1)))))
, 5(4(0(1(x1)))) -> 1(2(5(0(4(x1)))))
, 0(0(5(1(5(x1))))) -> 1(2(5(5(0(0(x1))))))
, 0(5(3(0(1(x1))))) -> 1(0(5(3(0(4(x1))))))
, 0(5(3(4(1(x1))))) -> 1(0(3(5(4(5(x1))))))
, 0(5(4(0(1(x1))))) -> 0(1(3(0(4(5(x1))))))
, 5(4(2(1(1(x1))))) -> 5(4(1(2(1(2(x1))))))}
Proof Output:
The problem is match-bounded by 1.
The enriched problem is compatible with the following automaton:
{ 0_0(2) -> 1
, 0_1(2) -> 20
, 0_1(3) -> 1
, 0_1(3) -> 20
, 0_1(9) -> 8
, 0_1(11) -> 10
, 0_1(12) -> 6
, 0_1(22) -> 21
, 1_0(2) -> 2
, 1_1(2) -> 5
, 1_1(5) -> 4
, 1_1(6) -> 1
, 1_1(6) -> 20
, 1_1(7) -> 6
, 1_1(14) -> 13
, 1_1(15) -> 26
, 1_1(17) -> 16
, 1_1(19) -> 23
, 1_1(20) -> 8
, 1_1(21) -> 10
, 2_0(2) -> 2
, 2_1(2) -> 17
, 2_1(4) -> 3
, 2_1(5) -> 11
, 2_1(9) -> 14
, 2_1(10) -> 6
, 2_1(16) -> 15
, 2_1(18) -> 7
, 2_1(23) -> 10
, 3_0(2) -> 2
, 3_1(4) -> 3
, 3_1(8) -> 7
, 3_1(13) -> 12
, 3_1(20) -> 19
, 3_1(24) -> 10
, 4_0(2) -> 2
, 4_1(2) -> 9
, 4_1(9) -> 22
, 4_1(15) -> 12
, 4_1(19) -> 18
, 4_1(26) -> 25
, 5_0(2) -> 1
, 5_1(17) -> 24
, 5_1(25) -> 1}Tool RC1
stdout:
MAYBE
Tool RC2
stdout:
YES(?,O(n^1))
'Fastest (timeout of 60.0 seconds)'
-----------------------------------
Answer: YES(?,O(n^1))
Input Problem: runtime-complexity with respect to
Rules:
{ 0(0(1(x1))) -> 0(1(2(0(x1))))
, 0(0(1(x1))) -> 0(3(1(0(x1))))
, 0(0(1(x1))) -> 1(0(4(0(x1))))
, 0(0(1(x1))) -> 0(1(3(0(2(x1)))))
, 0(0(1(x1))) -> 0(1(3(0(4(x1)))))
, 0(0(1(x1))) -> 0(2(0(1(2(x1)))))
, 0(0(1(x1))) -> 0(3(0(1(2(x1)))))
, 0(0(1(x1))) -> 0(3(0(3(1(x1)))))
, 0(0(1(x1))) -> 0(4(0(4(1(x1)))))
, 0(0(1(x1))) -> 1(2(0(2(0(x1)))))
, 0(0(1(x1))) -> 1(2(2(0(0(x1)))))
, 0(0(1(x1))) -> 0(0(2(2(1(2(x1))))))
, 0(0(1(x1))) -> 0(1(2(4(2(0(x1))))))
, 0(0(1(x1))) -> 1(2(0(3(0(4(x1))))))
, 0(1(1(x1))) -> 0(2(1(1(x1))))
, 0(1(1(x1))) -> 0(3(1(1(x1))))
, 0(1(1(x1))) -> 1(1(3(0(4(x1)))))
, 0(1(1(x1))) -> 1(2(0(2(1(x1)))))
, 0(1(1(x1))) -> 1(0(3(1(2(4(x1))))))
, 0(1(1(x1))) -> 1(0(4(2(1(2(x1))))))
, 0(1(1(x1))) -> 1(1(2(4(3(0(x1))))))
, 0(1(1(x1))) -> 1(2(1(0(4(4(x1))))))
, 0(1(1(x1))) -> 1(2(2(1(3(0(x1))))))
, 0(5(1(x1))) -> 0(3(1(5(x1))))
, 0(5(1(x1))) -> 0(4(5(1(x1))))
, 0(5(1(x1))) -> 0(2(3(1(5(x1)))))
, 0(5(1(x1))) -> 0(3(1(5(2(x1)))))
, 0(5(1(x1))) -> 0(3(1(2(5(2(x1))))))
, 5(0(1(x1))) -> 5(1(2(4(0(x1)))))
, 5(0(1(x1))) -> 5(0(2(1(2(4(x1))))))
, 5(0(1(x1))) -> 5(1(2(3(0(4(x1))))))
, 0(0(1(5(x1)))) -> 0(4(1(0(5(x1)))))
, 0(0(2(1(x1)))) -> 2(0(3(0(2(1(x1))))))
, 0(0(2(1(x1)))) -> 2(3(0(2(0(1(x1))))))
, 0(1(0(1(x1)))) -> 1(0(2(0(1(x1)))))
, 0(1(1(1(x1)))) -> 1(1(3(1(0(x1)))))
, 5(0(1(1(x1)))) -> 1(5(1(2(0(x1)))))
, 5(3(0(1(x1)))) -> 5(1(2(3(0(x1)))))
, 5(3(1(5(x1)))) -> 5(3(1(2(5(x1)))))
, 5(3(2(1(x1)))) -> 1(2(3(5(2(x1)))))
, 5(4(0(1(x1)))) -> 1(2(5(0(4(x1)))))
, 0(0(5(1(5(x1))))) -> 1(2(5(5(0(0(x1))))))
, 0(5(3(0(1(x1))))) -> 1(0(5(3(0(4(x1))))))
, 0(5(3(4(1(x1))))) -> 1(0(3(5(4(5(x1))))))
, 0(5(4(0(1(x1))))) -> 0(1(3(0(4(5(x1))))))
, 5(4(2(1(1(x1))))) -> 5(4(1(2(1(2(x1))))))}
Proof Output:
'Bounds with minimal-enrichment and initial automaton 'match'' proved the best result:
Details:
--------
'Bounds with minimal-enrichment and initial automaton 'match'' succeeded with the following output:
'Bounds with minimal-enrichment and initial automaton 'match''
--------------------------------------------------------------
Answer: YES(?,O(n^1))
Input Problem: runtime-complexity with respect to
Rules:
{ 0(0(1(x1))) -> 0(1(2(0(x1))))
, 0(0(1(x1))) -> 0(3(1(0(x1))))
, 0(0(1(x1))) -> 1(0(4(0(x1))))
, 0(0(1(x1))) -> 0(1(3(0(2(x1)))))
, 0(0(1(x1))) -> 0(1(3(0(4(x1)))))
, 0(0(1(x1))) -> 0(2(0(1(2(x1)))))
, 0(0(1(x1))) -> 0(3(0(1(2(x1)))))
, 0(0(1(x1))) -> 0(3(0(3(1(x1)))))
, 0(0(1(x1))) -> 0(4(0(4(1(x1)))))
, 0(0(1(x1))) -> 1(2(0(2(0(x1)))))
, 0(0(1(x1))) -> 1(2(2(0(0(x1)))))
, 0(0(1(x1))) -> 0(0(2(2(1(2(x1))))))
, 0(0(1(x1))) -> 0(1(2(4(2(0(x1))))))
, 0(0(1(x1))) -> 1(2(0(3(0(4(x1))))))
, 0(1(1(x1))) -> 0(2(1(1(x1))))
, 0(1(1(x1))) -> 0(3(1(1(x1))))
, 0(1(1(x1))) -> 1(1(3(0(4(x1)))))
, 0(1(1(x1))) -> 1(2(0(2(1(x1)))))
, 0(1(1(x1))) -> 1(0(3(1(2(4(x1))))))
, 0(1(1(x1))) -> 1(0(4(2(1(2(x1))))))
, 0(1(1(x1))) -> 1(1(2(4(3(0(x1))))))
, 0(1(1(x1))) -> 1(2(1(0(4(4(x1))))))
, 0(1(1(x1))) -> 1(2(2(1(3(0(x1))))))
, 0(5(1(x1))) -> 0(3(1(5(x1))))
, 0(5(1(x1))) -> 0(4(5(1(x1))))
, 0(5(1(x1))) -> 0(2(3(1(5(x1)))))
, 0(5(1(x1))) -> 0(3(1(5(2(x1)))))
, 0(5(1(x1))) -> 0(3(1(2(5(2(x1))))))
, 5(0(1(x1))) -> 5(1(2(4(0(x1)))))
, 5(0(1(x1))) -> 5(0(2(1(2(4(x1))))))
, 5(0(1(x1))) -> 5(1(2(3(0(4(x1))))))
, 0(0(1(5(x1)))) -> 0(4(1(0(5(x1)))))
, 0(0(2(1(x1)))) -> 2(0(3(0(2(1(x1))))))
, 0(0(2(1(x1)))) -> 2(3(0(2(0(1(x1))))))
, 0(1(0(1(x1)))) -> 1(0(2(0(1(x1)))))
, 0(1(1(1(x1)))) -> 1(1(3(1(0(x1)))))
, 5(0(1(1(x1)))) -> 1(5(1(2(0(x1)))))
, 5(3(0(1(x1)))) -> 5(1(2(3(0(x1)))))
, 5(3(1(5(x1)))) -> 5(3(1(2(5(x1)))))
, 5(3(2(1(x1)))) -> 1(2(3(5(2(x1)))))
, 5(4(0(1(x1)))) -> 1(2(5(0(4(x1)))))
, 0(0(5(1(5(x1))))) -> 1(2(5(5(0(0(x1))))))
, 0(5(3(0(1(x1))))) -> 1(0(5(3(0(4(x1))))))
, 0(5(3(4(1(x1))))) -> 1(0(3(5(4(5(x1))))))
, 0(5(4(0(1(x1))))) -> 0(1(3(0(4(5(x1))))))
, 5(4(2(1(1(x1))))) -> 5(4(1(2(1(2(x1))))))}
Proof Output:
The problem is match-bounded by 1.
The enriched problem is compatible with the following automaton:
{ 0_0(2) -> 1
, 0_1(2) -> 20
, 0_1(3) -> 1
, 0_1(3) -> 20
, 0_1(9) -> 8
, 0_1(11) -> 10
, 0_1(12) -> 6
, 0_1(22) -> 21
, 1_0(2) -> 2
, 1_1(2) -> 5
, 1_1(5) -> 4
, 1_1(6) -> 1
, 1_1(6) -> 20
, 1_1(7) -> 6
, 1_1(14) -> 13
, 1_1(15) -> 26
, 1_1(17) -> 16
, 1_1(19) -> 23
, 1_1(20) -> 8
, 1_1(21) -> 10
, 2_0(2) -> 2
, 2_1(2) -> 17
, 2_1(4) -> 3
, 2_1(5) -> 11
, 2_1(9) -> 14
, 2_1(10) -> 6
, 2_1(16) -> 15
, 2_1(18) -> 7
, 2_1(23) -> 10
, 3_0(2) -> 2
, 3_1(4) -> 3
, 3_1(8) -> 7
, 3_1(13) -> 12
, 3_1(20) -> 19
, 3_1(24) -> 10
, 4_0(2) -> 2
, 4_1(2) -> 9
, 4_1(9) -> 22
, 4_1(15) -> 12
, 4_1(19) -> 18
, 4_1(26) -> 25
, 5_0(2) -> 1
, 5_1(17) -> 24
, 5_1(25) -> 1}