Tool CaT
stdout:
MAYBE
Problem:
thrice(0(x1)) -> p(s(p(p(p(s(s(s(0(p(s(p(s(x1)))))))))))))
thrice(s(x1)) -> p(p(s(s(half(p(p(s(s(p(s(sixtimes(p(s(p(p(s(s(x1))))))))))))))))))
half(0(x1)) -> p(p(s(s(p(s(0(p(s(s(s(s(x1))))))))))))
half(s(x1)) -> p(s(p(p(s(s(p(p(s(s(half(p(p(s(s(p(s(x1)))))))))))))))))
half(s(s(x1))) -> p(s(p(s(s(p(p(s(s(half(p(p(s(s(p(s(x1))))))))))))))))
sixtimes(0(x1)) -> p(s(p(s(0(s(s(s(s(s(p(s(p(s(x1))))))))))))))
sixtimes(s(x1)) ->
p(p(s(s(s(s(s(s(s(p(p(s(p(s(s(s(sixtimes(p(s(p(p(p(s(s(s(x1)))))))))))))))))))))))))
p(p(s(x1))) -> p(x1)
p(s(x1)) -> x1
p(0(x1)) -> 0(s(s(s(s(x1)))))
0(x1) -> x1
Proof:
Complexity Transformation Processor:
strict:
thrice(0(x1)) -> p(s(p(p(p(s(s(s(0(p(s(p(s(x1)))))))))))))
thrice(s(x1)) -> p(p(s(s(half(p(p(s(s(p(s(sixtimes(p(s(p(p(s(s(x1))))))))))))))))))
half(0(x1)) -> p(p(s(s(p(s(0(p(s(s(s(s(x1))))))))))))
half(s(x1)) -> p(s(p(p(s(s(p(p(s(s(half(p(p(s(s(p(s(x1)))))))))))))))))
half(s(s(x1))) -> p(s(p(s(s(p(p(s(s(half(p(p(s(s(p(s(x1))))))))))))))))
sixtimes(0(x1)) -> p(s(p(s(0(s(s(s(s(s(p(s(p(s(x1))))))))))))))
sixtimes(s(x1)) ->
p(p(s(s(s(s(s(s(s(p(p(s(p(s(s(s(sixtimes(p(s(p(p(p(s(s(s(x1)))))))))))))))))))))))))
p(p(s(x1))) -> p(x1)
p(s(x1)) -> x1
p(0(x1)) -> 0(s(s(s(s(x1)))))
0(x1) -> x1
weak:
Arctic Interpretation Processor:
dimension: 1
interpretation:
[half](x0) = x0,
[sixtimes](x0) = x0,
[p](x0) = x0,
[s](x0) = x0,
[thrice](x0) = x0,
[0](x0) = 1x0
orientation:
thrice(0(x1)) = 1x1 >= 1x1 = p(s(p(p(p(s(s(s(0(p(s(p(s(x1)))))))))))))
thrice(s(x1)) = x1 >= x1 = p(p(s(s(half(p(p(s(s(p(s(sixtimes(p(s(p(p(s(s(x1))))))))))))))))))
half(0(x1)) = 1x1 >= 1x1 = p(p(s(s(p(s(0(p(s(s(s(s(x1))))))))))))
half(s(x1)) = x1 >= x1 = p(s(p(p(s(s(p(p(s(s(half(p(p(s(s(p(s(x1)))))))))))))))))
half(s(s(x1))) = x1 >= x1 = p(s(p(s(s(p(p(s(s(half(p(p(s(s(p(s(x1))))))))))))))))
sixtimes(0(x1)) = 1x1 >= 1x1 = p(s(p(s(0(s(s(s(s(s(p(s(p(s(x1))))))))))))))
sixtimes(s(x1)) = x1 >= x1 = p(p(s(s(s(s(s(s(s(p(p(s(p(s(s(s(sixtimes(p(s(p(p(p(s(s(s(x1)))))))))))))))))))))))))
p(p(s(x1))) = x1 >= x1 = p(x1)
p(s(x1)) = x1 >= x1 = x1
p(0(x1)) = 1x1 >= 1x1 = 0(s(s(s(s(x1)))))
0(x1) = 1x1 >= x1 = x1
problem:
strict:
thrice(0(x1)) -> p(s(p(p(p(s(s(s(0(p(s(p(s(x1)))))))))))))
thrice(s(x1)) -> p(p(s(s(half(p(p(s(s(p(s(sixtimes(p(s(p(p(s(s(x1))))))))))))))))))
half(0(x1)) -> p(p(s(s(p(s(0(p(s(s(s(s(x1))))))))))))
half(s(x1)) -> p(s(p(p(s(s(p(p(s(s(half(p(p(s(s(p(s(x1)))))))))))))))))
half(s(s(x1))) -> p(s(p(s(s(p(p(s(s(half(p(p(s(s(p(s(x1))))))))))))))))
sixtimes(0(x1)) -> p(s(p(s(0(s(s(s(s(s(p(s(p(s(x1))))))))))))))
sixtimes(s(x1)) ->
p(p(s(s(s(s(s(s(s(p(p(s(p(s(s(s(sixtimes(p(s(p(p(p(s(s(s(x1)))))))))))))))))))))))))
p(p(s(x1))) -> p(x1)
p(s(x1)) -> x1
p(0(x1)) -> 0(s(s(s(s(x1)))))
weak:
0(x1) -> x1
Arctic Interpretation Processor:
dimension: 1
interpretation:
[half](x0) = 2x0,
[sixtimes](x0) = x0,
[p](x0) = x0,
[s](x0) = x0,
[thrice](x0) = 3x0,
[0](x0) = x0
orientation:
thrice(0(x1)) = 3x1 >= x1 = p(s(p(p(p(s(s(s(0(p(s(p(s(x1)))))))))))))
thrice(s(x1)) = 3x1 >= 2x1 = p(p(s(s(half(p(p(s(s(p(s(sixtimes(p(s(p(p(s(s(x1))))))))))))))))))
half(0(x1)) = 2x1 >= x1 = p(p(s(s(p(s(0(p(s(s(s(s(x1))))))))))))
half(s(x1)) = 2x1 >= 2x1 = p(s(p(p(s(s(p(p(s(s(half(p(p(s(s(p(s(x1)))))))))))))))))
half(s(s(x1))) = 2x1 >= 2x1 = p(s(p(s(s(p(p(s(s(half(p(p(s(s(p(s(x1))))))))))))))))
sixtimes(0(x1)) = x1 >= x1 = p(s(p(s(0(s(s(s(s(s(p(s(p(s(x1))))))))))))))
sixtimes(s(x1)) = x1 >= x1 = p(p(s(s(s(s(s(s(s(p(p(s(p(s(s(s(sixtimes(p(s(p(p(p(s(s(s(x1)))))))))))))))))))))))))
p(p(s(x1))) = x1 >= x1 = p(x1)
p(s(x1)) = x1 >= x1 = x1
p(0(x1)) = x1 >= x1 = 0(s(s(s(s(x1)))))
0(x1) = x1 >= x1 = x1
problem:
strict:
half(s(x1)) -> p(s(p(p(s(s(p(p(s(s(half(p(p(s(s(p(s(x1)))))))))))))))))
half(s(s(x1))) -> p(s(p(s(s(p(p(s(s(half(p(p(s(s(p(s(x1))))))))))))))))
sixtimes(0(x1)) -> p(s(p(s(0(s(s(s(s(s(p(s(p(s(x1))))))))))))))
sixtimes(s(x1)) ->
p(p(s(s(s(s(s(s(s(p(p(s(p(s(s(s(sixtimes(p(s(p(p(p(s(s(s(x1)))))))))))))))))))))))))
p(p(s(x1))) -> p(x1)
p(s(x1)) -> x1
p(0(x1)) -> 0(s(s(s(s(x1)))))
weak:
thrice(0(x1)) -> p(s(p(p(p(s(s(s(0(p(s(p(s(x1)))))))))))))
thrice(s(x1)) -> p(p(s(s(half(p(p(s(s(p(s(sixtimes(p(s(p(p(s(s(x1))))))))))))))))))
half(0(x1)) -> p(p(s(s(p(s(0(p(s(s(s(s(x1))))))))))))
0(x1) -> x1
Arctic Interpretation Processor:
dimension: 1
interpretation:
[half](x0) = 1x0,
[sixtimes](x0) = 2x0,
[p](x0) = x0,
[s](x0) = x0,
[thrice](x0) = 4x0,
[0](x0) = x0
orientation:
half(s(x1)) = 1x1 >= 1x1 = p(s(p(p(s(s(p(p(s(s(half(p(p(s(s(p(s(x1)))))))))))))))))
half(s(s(x1))) = 1x1 >= 1x1 = p(s(p(s(s(p(p(s(s(half(p(p(s(s(p(s(x1))))))))))))))))
sixtimes(0(x1)) = 2x1 >= x1 = p(s(p(s(0(s(s(s(s(s(p(s(p(s(x1))))))))))))))
sixtimes(s(x1)) = 2x1 >= 2x1 = p(p(s(s(s(s(s(s(s(p(p(s(p(s(s(s(sixtimes(p(s(p(p(p(s(s(s(x1)))))))))))))))))))))))))
p(p(s(x1))) = x1 >= x1 = p(x1)
p(s(x1)) = x1 >= x1 = x1
p(0(x1)) = x1 >= x1 = 0(s(s(s(s(x1)))))
thrice(0(x1)) = 4x1 >= x1 = p(s(p(p(p(s(s(s(0(p(s(p(s(x1)))))))))))))
thrice(s(x1)) = 4x1 >= 3x1 = p(p(s(s(half(p(p(s(s(p(s(sixtimes(p(s(p(p(s(s(x1))))))))))))))))))
half(0(x1)) = 1x1 >= x1 = p(p(s(s(p(s(0(p(s(s(s(s(x1))))))))))))
0(x1) = x1 >= x1 = x1
problem:
strict:
half(s(x1)) -> p(s(p(p(s(s(p(p(s(s(half(p(p(s(s(p(s(x1)))))))))))))))))
half(s(s(x1))) -> p(s(p(s(s(p(p(s(s(half(p(p(s(s(p(s(x1))))))))))))))))
sixtimes(s(x1)) ->
p(p(s(s(s(s(s(s(s(p(p(s(p(s(s(s(sixtimes(p(s(p(p(p(s(s(s(x1)))))))))))))))))))))))))
p(p(s(x1))) -> p(x1)
p(s(x1)) -> x1
p(0(x1)) -> 0(s(s(s(s(x1)))))
weak:
sixtimes(0(x1)) -> p(s(p(s(0(s(s(s(s(s(p(s(p(s(x1))))))))))))))
thrice(0(x1)) -> p(s(p(p(p(s(s(s(0(p(s(p(s(x1)))))))))))))
thrice(s(x1)) -> p(p(s(s(half(p(p(s(s(p(s(sixtimes(p(s(p(p(s(s(x1))))))))))))))))))
half(0(x1)) -> p(p(s(s(p(s(0(p(s(s(s(s(x1))))))))))))
0(x1) -> x1
Matrix Interpretation Processor:
dimension: 1
max_matrix:
1
interpretation:
[half](x0) = x0 + 8,
[sixtimes](x0) = x0 + 18,
[p](x0) = x0 + 1,
[s](x0) = x0,
[thrice](x0) = x0 + 44,
[0](x0) = x0
orientation:
half(s(x1)) = x1 + 8 >= x1 + 16 = p(s(p(p(s(s(p(p(s(s(half(p(p(s(s(p(s(x1)))))))))))))))))
half(s(s(x1))) = x1 + 8 >= x1 + 15 = p(s(p(s(s(p(p(s(s(half(p(p(s(s(p(s(x1))))))))))))))))
sixtimes(s(x1)) = x1 + 18 >= x1 + 27 = p(p(s(s(s(s(s(s(s(p(p(s(p(s(s(s(sixtimes(p(s(p(p(p(s(s(s(x1)))))))))))))))))))))))))
p(p(s(x1))) = x1 + 2 >= x1 + 1 = p(x1)
p(s(x1)) = x1 + 1 >= x1 = x1
p(0(x1)) = x1 + 1 >= x1 = 0(s(s(s(s(x1)))))
sixtimes(0(x1)) = x1 + 18 >= x1 + 4 = p(s(p(s(0(s(s(s(s(s(p(s(p(s(x1))))))))))))))
thrice(0(x1)) = x1 + 44 >= x1 + 6 = p(s(p(p(p(s(s(s(0(p(s(p(s(x1)))))))))))))
thrice(s(x1)) = x1 + 44 >= x1 + 34 = p(p(s(s(half(p(p(s(s(p(s(sixtimes(p(s(p(p(s(s(x1))))))))))))))))))
half(0(x1)) = x1 + 8 >= x1 + 4 = p(p(s(s(p(s(0(p(s(s(s(s(x1))))))))))))
0(x1) = x1 >= x1 = x1
problem:
strict:
half(s(x1)) -> p(s(p(p(s(s(p(p(s(s(half(p(p(s(s(p(s(x1)))))))))))))))))
half(s(s(x1))) -> p(s(p(s(s(p(p(s(s(half(p(p(s(s(p(s(x1))))))))))))))))
sixtimes(s(x1)) ->
p(p(s(s(s(s(s(s(s(p(p(s(p(s(s(s(sixtimes(p(s(p(p(p(s(s(s(x1)))))))))))))))))))))))))
weak:
p(p(s(x1))) -> p(x1)
p(s(x1)) -> x1
p(0(x1)) -> 0(s(s(s(s(x1)))))
sixtimes(0(x1)) -> p(s(p(s(0(s(s(s(s(s(p(s(p(s(x1))))))))))))))
thrice(0(x1)) -> p(s(p(p(p(s(s(s(0(p(s(p(s(x1)))))))))))))
thrice(s(x1)) -> p(p(s(s(half(p(p(s(s(p(s(sixtimes(p(s(p(p(s(s(x1))))))))))))))))))
half(0(x1)) -> p(p(s(s(p(s(0(p(s(s(s(s(x1))))))))))))
0(x1) -> x1
Open
Tool IRC1
stdout:
YES(?,O(n^1))
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:
{ thrice(0(x1)) -> p(s(p(p(p(s(s(s(0(p(s(p(s(x1)))))))))))))
, thrice(s(x1)) ->
p(p(s(s(half(p(p(s(s(p(s(sixtimes(p(s(p(p(s(s(x1))))))))))))))))))
, half(0(x1)) -> p(p(s(s(p(s(0(p(s(s(s(s(x1))))))))))))
, half(s(x1)) ->
p(s(p(p(s(s(p(p(s(s(half(p(p(s(s(p(s(x1)))))))))))))))))
, half(s(s(x1))) ->
p(s(p(s(s(p(p(s(s(half(p(p(s(s(p(s(x1))))))))))))))))
, sixtimes(0(x1)) -> p(s(p(s(0(s(s(s(s(s(p(s(p(s(x1))))))))))))))
, sixtimes(s(x1)) ->
p(p(s(s(s(s(s(s(s(p(p(s(p(s(s(s(sixtimes(p(s(p(p(p(s(s(s(x1)))))))))))))))))))))))))
, p(p(s(x1))) -> p(x1)
, p(s(x1)) -> x1
, p(0(x1)) -> 0(s(s(s(s(x1)))))
, 0(x1) -> x1}
Proof Output:
'Bounds with perSymbol-enrichment and initial automaton 'match'' proved the best result:
Details:
--------
'Bounds with perSymbol-enrichment and initial automaton 'match'' succeeded with the following output:
'Bounds with perSymbol-enrichment and initial automaton 'match''
----------------------------------------------------------------
Answer: YES(?,O(n^1))
Input Problem: innermost runtime-complexity with respect to
Rules:
{ thrice(0(x1)) -> p(s(p(p(p(s(s(s(0(p(s(p(s(x1)))))))))))))
, thrice(s(x1)) ->
p(p(s(s(half(p(p(s(s(p(s(sixtimes(p(s(p(p(s(s(x1))))))))))))))))))
, half(0(x1)) -> p(p(s(s(p(s(0(p(s(s(s(s(x1))))))))))))
, half(s(x1)) ->
p(s(p(p(s(s(p(p(s(s(half(p(p(s(s(p(s(x1)))))))))))))))))
, half(s(s(x1))) ->
p(s(p(s(s(p(p(s(s(half(p(p(s(s(p(s(x1))))))))))))))))
, sixtimes(0(x1)) -> p(s(p(s(0(s(s(s(s(s(p(s(p(s(x1))))))))))))))
, sixtimes(s(x1)) ->
p(p(s(s(s(s(s(s(s(p(p(s(p(s(s(s(sixtimes(p(s(p(p(p(s(s(s(x1)))))))))))))))))))))))))
, p(p(s(x1))) -> p(x1)
, p(s(x1)) -> x1
, p(0(x1)) -> 0(s(s(s(s(x1)))))
, 0(x1) -> x1}
Proof Output:
The problem is match-bounded by 3.
The enriched problem is compatible with the following automaton:
{ thrice_0(4) -> 1
, 0_0(4) -> 2
, p_0(4) -> 3
, p_1(7) -> 1
, p_1(8) -> 7
, p_1(12) -> 11
, p_1(13) -> 12
, p_1(16) -> 11
, p_1(16) -> 15
, p_1(19) -> 18
, p_1(21) -> 18
, p_1(21) -> 20
, p_1(22) -> 21
, p_1(23) -> 34
, p_1(23) -> 38
, p_1(24) -> 5
, p_1(24) -> 25
, p_1(24) -> 29
, p_1(24) -> 33
, p_1(26) -> 5
, p_1(26) -> 25
, p_1(26) -> 29
, p_1(26) -> 33
, p_1(27) -> 5
, p_1(27) -> 25
, p_1(27) -> 26
, p_1(27) -> 29
, p_1(27) -> 33
, p_1(30) -> 5
, p_1(30) -> 25
, p_1(30) -> 29
, p_1(30) -> 33
, p_1(31) -> 30
, p_1(35) -> 34
, p_1(36) -> 35
, p_1(39) -> 6
, p_1(39) -> 11
, p_1(39) -> 15
, p_1(39) -> 17
, p_1(39) -> 54
, p_1(39) -> 150
, p_1(39) -> 154
, p_1(40) -> 39
, p_1(48) -> 47
, p_1(48) -> 133
, p_1(48) -> 137
, p_1(49) -> 48
, p_1(51) -> 48
, p_1(51) -> 50
, p_1(56) -> 55
, p_1(58) -> 55
, p_1(58) -> 57
, p_1(59) -> 58
, p_1(60) -> 59
, p_2(9) -> 1
, p_2(9) -> 10
, p_2(14) -> 11
, p_2(22) -> 58
, p_2(23) -> 18
, p_2(23) -> 20
, p_2(23) -> 55
, p_2(23) -> 57
, p_2(28) -> 5
, p_2(28) -> 25
, p_2(28) -> 29
, p_2(28) -> 33
, p_2(32) -> 5
, p_2(32) -> 25
, p_2(32) -> 29
, p_2(32) -> 33
, p_2(37) -> 34
, p_2(41) -> 6
, p_2(41) -> 11
, p_2(41) -> 15
, p_2(41) -> 17
, p_2(41) -> 54
, p_2(41) -> 150
, p_2(41) -> 154
, p_2(50) -> 47
, p_2(50) -> 133
, p_2(50) -> 137
, p_2(52) -> 47
, p_2(52) -> 133
, p_2(52) -> 137
, p_2(61) -> 1
, p_2(61) -> 10
, p_2(61) -> 61
, p_2(61) -> 65
, p_2(61) -> 69
, p_2(61) -> 77
, p_2(61) -> 81
, p_2(61) -> 91
, p_2(61) -> 95
, p_2(61) -> 102
, p_2(61) -> 111
, p_2(61) -> 128
, p_2(61) -> 132
, p_2(61) -> 139
, p_2(61) -> 148
, p_2(62) -> 1
, p_2(62) -> 10
, p_2(62) -> 61
, p_2(63) -> 62
, p_2(66) -> 1
, p_2(66) -> 10
, p_2(66) -> 61
, p_2(66) -> 65
, p_2(66) -> 69
, p_2(66) -> 77
, p_2(66) -> 81
, p_2(66) -> 91
, p_2(66) -> 95
, p_2(66) -> 102
, p_2(66) -> 111
, p_2(66) -> 128
, p_2(66) -> 132
, p_2(66) -> 139
, p_2(66) -> 148
, p_2(67) -> 66
, p_2(68) -> 1
, p_2(68) -> 10
, p_2(68) -> 61
, p_2(68) -> 65
, p_2(68) -> 69
, p_2(68) -> 77
, p_2(68) -> 81
, p_2(68) -> 91
, p_2(68) -> 95
, p_2(68) -> 102
, p_2(68) -> 111
, p_2(68) -> 128
, p_2(68) -> 132
, p_2(68) -> 139
, p_2(68) -> 148
, p_2(71) -> 70
, p_2(72) -> 71
, p_2(75) -> 70
, p_2(75) -> 74
, p_2(78) -> 1
, p_2(78) -> 10
, p_2(78) -> 61
, p_2(78) -> 65
, p_2(78) -> 69
, p_2(78) -> 77
, p_2(78) -> 81
, p_2(78) -> 91
, p_2(78) -> 95
, p_2(78) -> 102
, p_2(78) -> 111
, p_2(78) -> 128
, p_2(78) -> 132
, p_2(78) -> 139
, p_2(78) -> 148
, p_2(79) -> 78
, p_2(80) -> 1
, p_2(80) -> 10
, p_2(80) -> 61
, p_2(80) -> 65
, p_2(80) -> 69
, p_2(80) -> 77
, p_2(80) -> 81
, p_2(80) -> 91
, p_2(80) -> 95
, p_2(80) -> 102
, p_2(80) -> 111
, p_2(80) -> 128
, p_2(80) -> 132
, p_2(80) -> 139
, p_2(80) -> 148
, p_2(83) -> 82
, p_2(84) -> 83
, p_2(87) -> 82
, p_2(87) -> 86
, p_2(88) -> 1
, p_2(88) -> 10
, p_2(88) -> 61
, p_2(88) -> 65
, p_2(88) -> 69
, p_2(88) -> 77
, p_2(88) -> 81
, p_2(88) -> 91
, p_2(88) -> 95
, p_2(88) -> 102
, p_2(88) -> 111
, p_2(88) -> 128
, p_2(88) -> 132
, p_2(88) -> 139
, p_2(88) -> 148
, p_2(89) -> 1
, p_2(89) -> 10
, p_2(89) -> 61
, p_2(89) -> 65
, p_2(89) -> 69
, p_2(89) -> 77
, p_2(89) -> 81
, p_2(89) -> 88
, p_2(89) -> 91
, p_2(89) -> 95
, p_2(89) -> 102
, p_2(89) -> 111
, p_2(89) -> 128
, p_2(89) -> 132
, p_2(89) -> 139
, p_2(89) -> 148
, p_2(92) -> 1
, p_2(92) -> 10
, p_2(92) -> 61
, p_2(92) -> 65
, p_2(92) -> 69
, p_2(92) -> 77
, p_2(92) -> 81
, p_2(92) -> 91
, p_2(92) -> 95
, p_2(92) -> 102
, p_2(92) -> 111
, p_2(92) -> 128
, p_2(92) -> 132
, p_2(92) -> 139
, p_2(92) -> 148
, p_2(93) -> 92
, p_2(94) -> 1
, p_2(94) -> 10
, p_2(94) -> 61
, p_2(94) -> 65
, p_2(94) -> 69
, p_2(94) -> 77
, p_2(94) -> 81
, p_2(94) -> 91
, p_2(94) -> 95
, p_2(94) -> 102
, p_2(94) -> 111
, p_2(94) -> 128
, p_2(94) -> 132
, p_2(94) -> 139
, p_2(94) -> 148
, p_2(97) -> 96
, p_2(98) -> 97
, p_2(101) -> 96
, p_2(101) -> 100
, p_2(103) -> 1
, p_2(103) -> 10
, p_2(103) -> 61
, p_2(103) -> 65
, p_2(103) -> 69
, p_2(103) -> 77
, p_2(103) -> 81
, p_2(103) -> 91
, p_2(103) -> 95
, p_2(103) -> 102
, p_2(103) -> 111
, p_2(103) -> 128
, p_2(103) -> 132
, p_2(103) -> 139
, p_2(103) -> 148
, p_2(104) -> 103
, p_2(109) -> 1
, p_2(109) -> 10
, p_2(109) -> 61
, p_2(109) -> 65
, p_2(109) -> 69
, p_2(109) -> 77
, p_2(109) -> 81
, p_2(109) -> 91
, p_2(109) -> 95
, p_2(109) -> 102
, p_2(109) -> 111
, p_2(109) -> 128
, p_2(109) -> 132
, p_2(109) -> 139
, p_2(109) -> 148
, p_2(114) -> 113
, p_2(115) -> 114
, p_2(118) -> 113
, p_2(118) -> 117
, p_2(125) -> 1
, p_2(125) -> 10
, p_2(125) -> 61
, p_2(125) -> 65
, p_2(125) -> 69
, p_2(125) -> 77
, p_2(125) -> 81
, p_2(125) -> 91
, p_2(125) -> 95
, p_2(125) -> 102
, p_2(125) -> 111
, p_2(125) -> 128
, p_2(125) -> 132
, p_2(125) -> 139
, p_2(125) -> 148
, p_2(126) -> 1
, p_2(126) -> 10
, p_2(126) -> 61
, p_2(126) -> 65
, p_2(126) -> 69
, p_2(126) -> 77
, p_2(126) -> 81
, p_2(126) -> 91
, p_2(126) -> 95
, p_2(126) -> 102
, p_2(126) -> 111
, p_2(126) -> 125
, p_2(126) -> 128
, p_2(126) -> 132
, p_2(126) -> 139
, p_2(126) -> 148
, p_2(129) -> 1
, p_2(129) -> 10
, p_2(129) -> 61
, p_2(129) -> 65
, p_2(129) -> 69
, p_2(129) -> 77
, p_2(129) -> 81
, p_2(129) -> 91
, p_2(129) -> 95
, p_2(129) -> 102
, p_2(129) -> 111
, p_2(129) -> 128
, p_2(129) -> 132
, p_2(129) -> 139
, p_2(129) -> 148
, p_2(130) -> 129
, p_2(134) -> 133
, p_2(135) -> 134
, p_2(138) -> 133
, p_2(138) -> 137
, p_2(140) -> 1
, p_2(140) -> 10
, p_2(140) -> 61
, p_2(140) -> 65
, p_2(140) -> 69
, p_2(140) -> 77
, p_2(140) -> 81
, p_2(140) -> 91
, p_2(140) -> 95
, p_2(140) -> 102
, p_2(140) -> 111
, p_2(140) -> 128
, p_2(140) -> 132
, p_2(140) -> 139
, p_2(140) -> 148
, p_2(141) -> 140
, p_2(151) -> 150
, p_2(152) -> 151
, p_2(155) -> 150
, p_2(155) -> 154
, p_3(64) -> 1
, p_3(64) -> 10
, p_3(64) -> 61
, p_3(65) -> 1
, p_3(65) -> 10
, p_3(65) -> 61
, p_3(65) -> 65
, p_3(65) -> 69
, p_3(65) -> 77
, p_3(65) -> 81
, p_3(65) -> 91
, p_3(65) -> 95
, p_3(65) -> 102
, p_3(65) -> 111
, p_3(65) -> 128
, p_3(65) -> 132
, p_3(65) -> 139
, p_3(65) -> 148
, p_3(68) -> 1
, p_3(68) -> 10
, p_3(68) -> 61
, p_3(68) -> 65
, p_3(68) -> 69
, p_3(68) -> 77
, p_3(68) -> 81
, p_3(68) -> 91
, p_3(68) -> 95
, p_3(68) -> 102
, p_3(68) -> 111
, p_3(68) -> 128
, p_3(68) -> 132
, p_3(68) -> 139
, p_3(68) -> 148
, p_3(69) -> 1
, p_3(69) -> 10
, p_3(69) -> 61
, p_3(69) -> 65
, p_3(69) -> 69
, p_3(69) -> 77
, p_3(69) -> 81
, p_3(69) -> 91
, p_3(69) -> 95
, p_3(69) -> 102
, p_3(69) -> 111
, p_3(69) -> 128
, p_3(69) -> 132
, p_3(69) -> 139
, p_3(69) -> 148
, p_3(73) -> 70
, p_3(76) -> 1
, p_3(76) -> 10
, p_3(76) -> 61
, p_3(76) -> 65
, p_3(76) -> 69
, p_3(76) -> 77
, p_3(76) -> 81
, p_3(76) -> 91
, p_3(76) -> 95
, p_3(76) -> 102
, p_3(76) -> 111
, p_3(76) -> 128
, p_3(76) -> 132
, p_3(76) -> 139
, p_3(76) -> 148
, p_3(77) -> 1
, p_3(77) -> 10
, p_3(77) -> 61
, p_3(77) -> 65
, p_3(77) -> 69
, p_3(77) -> 77
, p_3(77) -> 81
, p_3(77) -> 91
, p_3(77) -> 95
, p_3(77) -> 102
, p_3(77) -> 111
, p_3(77) -> 128
, p_3(77) -> 132
, p_3(77) -> 139
, p_3(77) -> 148
, p_3(80) -> 1
, p_3(80) -> 10
, p_3(80) -> 61
, p_3(80) -> 65
, p_3(80) -> 69
, p_3(80) -> 77
, p_3(80) -> 81
, p_3(80) -> 91
, p_3(80) -> 95
, p_3(80) -> 102
, p_3(80) -> 111
, p_3(80) -> 128
, p_3(80) -> 132
, p_3(80) -> 139
, p_3(80) -> 148
, p_3(81) -> 1
, p_3(81) -> 10
, p_3(81) -> 61
, p_3(81) -> 65
, p_3(81) -> 69
, p_3(81) -> 77
, p_3(81) -> 81
, p_3(81) -> 91
, p_3(81) -> 95
, p_3(81) -> 102
, p_3(81) -> 111
, p_3(81) -> 128
, p_3(81) -> 132
, p_3(81) -> 139
, p_3(81) -> 148
, p_3(85) -> 82
, p_3(88) -> 1
, p_3(88) -> 10
, p_3(88) -> 61
, p_3(88) -> 65
, p_3(88) -> 69
, p_3(88) -> 77
, p_3(88) -> 81
, p_3(88) -> 91
, p_3(88) -> 95
, p_3(88) -> 102
, p_3(88) -> 111
, p_3(88) -> 128
, p_3(88) -> 132
, p_3(88) -> 139
, p_3(88) -> 148
, p_3(90) -> 1
, p_3(90) -> 10
, p_3(90) -> 61
, p_3(90) -> 65
, p_3(90) -> 69
, p_3(90) -> 77
, p_3(90) -> 81
, p_3(90) -> 91
, p_3(90) -> 95
, p_3(90) -> 102
, p_3(90) -> 111
, p_3(90) -> 128
, p_3(90) -> 132
, p_3(90) -> 139
, p_3(90) -> 148
, p_3(91) -> 1
, p_3(91) -> 10
, p_3(91) -> 61
, p_3(91) -> 65
, p_3(91) -> 69
, p_3(91) -> 77
, p_3(91) -> 81
, p_3(91) -> 91
, p_3(91) -> 95
, p_3(91) -> 102
, p_3(91) -> 111
, p_3(91) -> 128
, p_3(91) -> 132
, p_3(91) -> 139
, p_3(91) -> 148
, p_3(94) -> 1
, p_3(94) -> 10
, p_3(94) -> 61
, p_3(94) -> 65
, p_3(94) -> 69
, p_3(94) -> 77
, p_3(94) -> 81
, p_3(94) -> 91
, p_3(94) -> 95
, p_3(94) -> 102
, p_3(94) -> 111
, p_3(94) -> 128
, p_3(94) -> 132
, p_3(94) -> 139
, p_3(94) -> 148
, p_3(95) -> 1
, p_3(95) -> 10
, p_3(95) -> 61
, p_3(95) -> 65
, p_3(95) -> 69
, p_3(95) -> 77
, p_3(95) -> 81
, p_3(95) -> 91
, p_3(95) -> 95
, p_3(95) -> 102
, p_3(95) -> 111
, p_3(95) -> 128
, p_3(95) -> 132
, p_3(95) -> 139
, p_3(95) -> 148
, p_3(99) -> 96
, p_3(102) -> 1
, p_3(102) -> 10
, p_3(102) -> 61
, p_3(102) -> 65
, p_3(102) -> 69
, p_3(102) -> 77
, p_3(102) -> 81
, p_3(102) -> 91
, p_3(102) -> 95
, p_3(102) -> 102
, p_3(102) -> 111
, p_3(102) -> 128
, p_3(102) -> 132
, p_3(102) -> 139
, p_3(102) -> 148
, p_3(109) -> 1
, p_3(109) -> 10
, p_3(109) -> 61
, p_3(109) -> 65
, p_3(109) -> 69
, p_3(109) -> 77
, p_3(109) -> 81
, p_3(109) -> 91
, p_3(109) -> 95
, p_3(109) -> 102
, p_3(109) -> 111
, p_3(109) -> 128
, p_3(109) -> 132
, p_3(109) -> 139
, p_3(109) -> 148
, p_3(111) -> 1
, p_3(111) -> 10
, p_3(111) -> 61
, p_3(111) -> 65
, p_3(111) -> 69
, p_3(111) -> 77
, p_3(111) -> 81
, p_3(111) -> 91
, p_3(111) -> 95
, p_3(111) -> 102
, p_3(111) -> 111
, p_3(111) -> 128
, p_3(111) -> 132
, p_3(111) -> 139
, p_3(111) -> 148
, p_3(116) -> 113
, p_3(125) -> 1
, p_3(125) -> 10
, p_3(125) -> 61
, p_3(125) -> 65
, p_3(125) -> 69
, p_3(125) -> 77
, p_3(125) -> 81
, p_3(125) -> 91
, p_3(125) -> 95
, p_3(125) -> 102
, p_3(125) -> 111
, p_3(125) -> 128
, p_3(125) -> 132
, p_3(125) -> 139
, p_3(125) -> 148
, p_3(127) -> 1
, p_3(127) -> 10
, p_3(127) -> 61
, p_3(127) -> 65
, p_3(127) -> 69
, p_3(127) -> 77
, p_3(127) -> 81
, p_3(127) -> 91
, p_3(127) -> 95
, p_3(127) -> 102
, p_3(127) -> 111
, p_3(127) -> 128
, p_3(127) -> 132
, p_3(127) -> 139
, p_3(127) -> 148
, p_3(128) -> 1
, p_3(128) -> 10
, p_3(128) -> 61
, p_3(128) -> 65
, p_3(128) -> 69
, p_3(128) -> 77
, p_3(128) -> 81
, p_3(128) -> 91
, p_3(128) -> 95
, p_3(128) -> 102
, p_3(128) -> 111
, p_3(128) -> 128
, p_3(128) -> 132
, p_3(128) -> 139
, p_3(128) -> 148
, p_3(131) -> 1
, p_3(131) -> 10
, p_3(131) -> 61
, p_3(131) -> 65
, p_3(131) -> 69
, p_3(131) -> 77
, p_3(131) -> 81
, p_3(131) -> 91
, p_3(131) -> 95
, p_3(131) -> 102
, p_3(131) -> 111
, p_3(131) -> 128
, p_3(131) -> 132
, p_3(131) -> 139
, p_3(131) -> 148
, p_3(132) -> 1
, p_3(132) -> 10
, p_3(132) -> 61
, p_3(132) -> 65
, p_3(132) -> 69
, p_3(132) -> 77
, p_3(132) -> 81
, p_3(132) -> 91
, p_3(132) -> 95
, p_3(132) -> 102
, p_3(132) -> 111
, p_3(132) -> 128
, p_3(132) -> 132
, p_3(132) -> 139
, p_3(132) -> 148
, p_3(136) -> 133
, p_3(139) -> 1
, p_3(139) -> 10
, p_3(139) -> 61
, p_3(139) -> 65
, p_3(139) -> 69
, p_3(139) -> 77
, p_3(139) -> 81
, p_3(139) -> 91
, p_3(139) -> 95
, p_3(139) -> 102
, p_3(139) -> 111
, p_3(139) -> 128
, p_3(139) -> 132
, p_3(139) -> 139
, p_3(139) -> 148
, p_3(146) -> 1
, p_3(146) -> 10
, p_3(146) -> 61
, p_3(146) -> 65
, p_3(146) -> 69
, p_3(146) -> 77
, p_3(146) -> 81
, p_3(146) -> 91
, p_3(146) -> 95
, p_3(146) -> 102
, p_3(146) -> 111
, p_3(146) -> 128
, p_3(146) -> 132
, p_3(146) -> 139
, p_3(146) -> 148
, p_3(148) -> 1
, p_3(148) -> 10
, p_3(148) -> 61
, p_3(148) -> 65
, p_3(148) -> 69
, p_3(148) -> 77
, p_3(148) -> 81
, p_3(148) -> 91
, p_3(148) -> 95
, p_3(148) -> 102
, p_3(148) -> 111
, p_3(148) -> 128
, p_3(148) -> 132
, p_3(148) -> 139
, p_3(148) -> 148
, p_3(153) -> 150
, s_0(4) -> 2
, s_0(4) -> 3
, s_0(4) -> 4
, s_0(4) -> 18
, s_0(4) -> 20
, s_0(4) -> 34
, s_0(4) -> 38
, s_0(4) -> 55
, s_0(4) -> 57
, s_1(4) -> 21
, s_1(4) -> 23
, s_1(4) -> 58
, s_1(9) -> 8
, s_1(10) -> 7
, s_1(10) -> 9
, s_1(14) -> 13
, s_1(15) -> 12
, s_1(15) -> 14
, s_1(17) -> 16
, s_1(20) -> 19
, s_1(22) -> 60
, s_1(23) -> 22
, s_1(23) -> 59
, s_1(25) -> 24
, s_1(26) -> 24
, s_1(28) -> 27
, s_1(29) -> 5
, s_1(29) -> 25
, s_1(29) -> 26
, s_1(29) -> 28
, s_1(29) -> 29
, s_1(29) -> 33
, s_1(32) -> 31
, s_1(33) -> 30
, s_1(33) -> 32
, s_1(37) -> 36
, s_1(38) -> 35
, s_1(38) -> 37
, s_1(41) -> 40
, s_1(42) -> 39
, s_1(42) -> 41
, s_1(43) -> 6
, s_1(43) -> 11
, s_1(43) -> 15
, s_1(43) -> 17
, s_1(43) -> 42
, s_1(43) -> 54
, s_1(43) -> 150
, s_1(43) -> 154
, s_1(44) -> 43
, s_1(44) -> 70
, s_1(44) -> 74
, s_1(45) -> 44
, s_1(45) -> 82
, s_1(45) -> 86
, s_1(46) -> 45
, s_1(46) -> 96
, s_1(46) -> 100
, s_1(47) -> 46
, s_1(47) -> 113
, s_1(47) -> 117
, s_1(50) -> 49
, s_1(52) -> 51
, s_1(53) -> 48
, s_1(53) -> 50
, s_1(53) -> 52
, s_1(54) -> 47
, s_1(54) -> 53
, s_1(54) -> 133
, s_1(54) -> 137
, s_1(57) -> 56
, s_2(43) -> 75
, s_2(44) -> 87
, s_2(45) -> 101
, s_2(46) -> 118
, s_2(47) -> 138
, s_2(54) -> 155
, s_2(61) -> 7
, s_2(61) -> 9
, s_2(64) -> 63
, s_2(65) -> 62
, s_2(65) -> 64
, s_2(68) -> 67
, s_2(69) -> 66
, s_2(69) -> 68
, s_2(73) -> 72
, s_2(74) -> 71
, s_2(74) -> 73
, s_2(76) -> 62
, s_2(77) -> 1
, s_2(77) -> 10
, s_2(77) -> 61
, s_2(77) -> 76
, s_2(80) -> 79
, s_2(81) -> 78
, s_2(81) -> 80
, s_2(85) -> 84
, s_2(86) -> 83
, s_2(86) -> 85
, s_2(88) -> 66
, s_2(90) -> 89
, s_2(91) -> 1
, s_2(91) -> 10
, s_2(91) -> 61
, s_2(91) -> 65
, s_2(91) -> 69
, s_2(91) -> 77
, s_2(91) -> 81
, s_2(91) -> 88
, s_2(91) -> 90
, s_2(91) -> 91
, s_2(91) -> 95
, s_2(91) -> 102
, s_2(91) -> 111
, s_2(91) -> 128
, s_2(91) -> 132
, s_2(91) -> 139
, s_2(91) -> 148
, s_2(94) -> 93
, s_2(95) -> 92
, s_2(95) -> 94
, s_2(99) -> 98
, s_2(100) -> 97
, s_2(100) -> 99
, s_2(102) -> 1
, s_2(102) -> 10
, s_2(102) -> 61
, s_2(102) -> 65
, s_2(102) -> 69
, s_2(102) -> 77
, s_2(102) -> 81
, s_2(102) -> 91
, s_2(102) -> 95
, s_2(102) -> 102
, s_2(102) -> 111
, s_2(102) -> 128
, s_2(102) -> 132
, s_2(102) -> 139
, s_2(102) -> 148
, s_2(109) -> 104
, s_2(111) -> 103
, s_2(111) -> 109
, s_2(116) -> 115
, s_2(117) -> 114
, s_2(117) -> 116
, s_2(125) -> 66
, s_2(125) -> 68
, s_2(127) -> 126
, s_2(128) -> 1
, s_2(128) -> 10
, s_2(128) -> 61
, s_2(128) -> 65
, s_2(128) -> 69
, s_2(128) -> 77
, s_2(128) -> 81
, s_2(128) -> 91
, s_2(128) -> 95
, s_2(128) -> 102
, s_2(128) -> 111
, s_2(128) -> 125
, s_2(128) -> 127
, s_2(128) -> 128
, s_2(128) -> 132
, s_2(128) -> 139
, s_2(128) -> 148
, s_2(131) -> 130
, s_2(132) -> 129
, s_2(132) -> 131
, s_2(136) -> 135
, s_2(137) -> 134
, s_2(137) -> 136
, s_2(139) -> 1
, s_2(139) -> 10
, s_2(139) -> 61
, s_2(139) -> 65
, s_2(139) -> 69
, s_2(139) -> 77
, s_2(139) -> 81
, s_2(139) -> 91
, s_2(139) -> 95
, s_2(139) -> 102
, s_2(139) -> 111
, s_2(139) -> 128
, s_2(139) -> 132
, s_2(139) -> 139
, s_2(139) -> 148
, s_2(146) -> 141
, s_2(148) -> 140
, s_2(148) -> 146
, s_2(153) -> 152
, s_2(154) -> 151
, s_2(154) -> 153
, half_0(4) -> 5
, half_1(11) -> 1
, half_1(11) -> 10
, half_1(34) -> 5
, half_1(34) -> 25
, half_1(34) -> 29
, half_1(34) -> 33
, half_2(70) -> 1
, half_2(70) -> 10
, half_2(70) -> 61
, half_2(70) -> 65
, half_2(70) -> 69
, half_2(70) -> 77
, half_2(70) -> 81
, half_2(70) -> 91
, half_2(70) -> 95
, half_2(70) -> 102
, half_2(70) -> 111
, half_2(70) -> 128
, half_2(70) -> 132
, half_2(70) -> 139
, half_2(70) -> 148
, half_2(82) -> 1
, half_2(82) -> 10
, half_2(82) -> 61
, half_2(82) -> 65
, half_2(82) -> 69
, half_2(82) -> 77
, half_2(82) -> 81
, half_2(82) -> 91
, half_2(82) -> 95
, half_2(82) -> 102
, half_2(82) -> 111
, half_2(82) -> 128
, half_2(82) -> 132
, half_2(82) -> 139
, half_2(82) -> 148
, half_2(96) -> 1
, half_2(96) -> 10
, half_2(96) -> 61
, half_2(96) -> 65
, half_2(96) -> 69
, half_2(96) -> 77
, half_2(96) -> 81
, half_2(96) -> 91
, half_2(96) -> 95
, half_2(96) -> 102
, half_2(96) -> 111
, half_2(96) -> 128
, half_2(96) -> 132
, half_2(96) -> 139
, half_2(96) -> 148
, half_2(113) -> 1
, half_2(113) -> 10
, half_2(113) -> 61
, half_2(113) -> 65
, half_2(113) -> 69
, half_2(113) -> 77
, half_2(113) -> 81
, half_2(113) -> 91
, half_2(113) -> 95
, half_2(113) -> 102
, half_2(113) -> 111
, half_2(113) -> 128
, half_2(113) -> 132
, half_2(113) -> 139
, half_2(113) -> 148
, half_2(133) -> 1
, half_2(133) -> 10
, half_2(133) -> 61
, half_2(133) -> 65
, half_2(133) -> 69
, half_2(133) -> 77
, half_2(133) -> 81
, half_2(133) -> 91
, half_2(133) -> 95
, half_2(133) -> 102
, half_2(133) -> 111
, half_2(133) -> 128
, half_2(133) -> 132
, half_2(133) -> 139
, half_2(133) -> 148
, half_2(150) -> 1
, half_2(150) -> 10
, half_2(150) -> 61
, half_2(150) -> 65
, half_2(150) -> 69
, half_2(150) -> 77
, half_2(150) -> 81
, half_2(150) -> 91
, half_2(150) -> 95
, half_2(150) -> 102
, half_2(150) -> 111
, half_2(150) -> 128
, half_2(150) -> 132
, half_2(150) -> 139
, half_2(150) -> 148
, sixtimes_0(4) -> 6
, sixtimes_1(18) -> 11
, sixtimes_1(18) -> 15
, sixtimes_1(18) -> 17
, sixtimes_1(55) -> 54
, sixtimes_1(55) -> 150
, sixtimes_1(55) -> 154}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:
{ thrice(0(x1)) -> p(s(p(p(p(s(s(s(0(p(s(p(s(x1)))))))))))))
, thrice(s(x1)) ->
p(p(s(s(half(p(p(s(s(p(s(sixtimes(p(s(p(p(s(s(x1))))))))))))))))))
, half(0(x1)) -> p(p(s(s(p(s(0(p(s(s(s(s(x1))))))))))))
, half(s(x1)) ->
p(s(p(p(s(s(p(p(s(s(half(p(p(s(s(p(s(x1)))))))))))))))))
, half(s(s(x1))) ->
p(s(p(s(s(p(p(s(s(half(p(p(s(s(p(s(x1))))))))))))))))
, sixtimes(0(x1)) -> p(s(p(s(0(s(s(s(s(s(p(s(p(s(x1))))))))))))))
, sixtimes(s(x1)) ->
p(p(s(s(s(s(s(s(s(p(p(s(p(s(s(s(sixtimes(p(s(p(p(p(s(s(s(x1)))))))))))))))))))))))))
, p(p(s(x1))) -> p(x1)
, p(s(x1)) -> x1
, p(0(x1)) -> 0(s(s(s(s(x1)))))
, 0(x1) -> x1}
Proof Output:
'Bounds with perSymbol-enrichment and initial automaton 'match'' proved the best result:
Details:
--------
'Bounds with perSymbol-enrichment and initial automaton 'match'' succeeded with the following output:
'Bounds with perSymbol-enrichment and initial automaton 'match''
----------------------------------------------------------------
Answer: YES(?,O(n^1))
Input Problem: runtime-complexity with respect to
Rules:
{ thrice(0(x1)) -> p(s(p(p(p(s(s(s(0(p(s(p(s(x1)))))))))))))
, thrice(s(x1)) ->
p(p(s(s(half(p(p(s(s(p(s(sixtimes(p(s(p(p(s(s(x1))))))))))))))))))
, half(0(x1)) -> p(p(s(s(p(s(0(p(s(s(s(s(x1))))))))))))
, half(s(x1)) ->
p(s(p(p(s(s(p(p(s(s(half(p(p(s(s(p(s(x1)))))))))))))))))
, half(s(s(x1))) ->
p(s(p(s(s(p(p(s(s(half(p(p(s(s(p(s(x1))))))))))))))))
, sixtimes(0(x1)) -> p(s(p(s(0(s(s(s(s(s(p(s(p(s(x1))))))))))))))
, sixtimes(s(x1)) ->
p(p(s(s(s(s(s(s(s(p(p(s(p(s(s(s(sixtimes(p(s(p(p(p(s(s(s(x1)))))))))))))))))))))))))
, p(p(s(x1))) -> p(x1)
, p(s(x1)) -> x1
, p(0(x1)) -> 0(s(s(s(s(x1)))))
, 0(x1) -> x1}
Proof Output:
The problem is match-bounded by 3.
The enriched problem is compatible with the following automaton:
{ thrice_0(4) -> 1
, 0_0(4) -> 2
, p_0(4) -> 3
, p_1(7) -> 1
, p_1(8) -> 7
, p_1(12) -> 11
, p_1(13) -> 12
, p_1(16) -> 11
, p_1(16) -> 15
, p_1(19) -> 18
, p_1(21) -> 18
, p_1(21) -> 20
, p_1(22) -> 21
, p_1(23) -> 34
, p_1(23) -> 38
, p_1(24) -> 5
, p_1(24) -> 25
, p_1(24) -> 29
, p_1(24) -> 33
, p_1(26) -> 5
, p_1(26) -> 25
, p_1(26) -> 29
, p_1(26) -> 33
, p_1(27) -> 5
, p_1(27) -> 25
, p_1(27) -> 26
, p_1(27) -> 29
, p_1(27) -> 33
, p_1(30) -> 5
, p_1(30) -> 25
, p_1(30) -> 29
, p_1(30) -> 33
, p_1(31) -> 30
, p_1(35) -> 34
, p_1(36) -> 35
, p_1(39) -> 6
, p_1(39) -> 11
, p_1(39) -> 15
, p_1(39) -> 17
, p_1(39) -> 54
, p_1(39) -> 150
, p_1(39) -> 154
, p_1(40) -> 39
, p_1(48) -> 47
, p_1(48) -> 133
, p_1(48) -> 137
, p_1(49) -> 48
, p_1(51) -> 48
, p_1(51) -> 50
, p_1(56) -> 55
, p_1(58) -> 55
, p_1(58) -> 57
, p_1(59) -> 58
, p_1(60) -> 59
, p_2(9) -> 1
, p_2(9) -> 10
, p_2(14) -> 11
, p_2(22) -> 58
, p_2(23) -> 18
, p_2(23) -> 20
, p_2(23) -> 55
, p_2(23) -> 57
, p_2(28) -> 5
, p_2(28) -> 25
, p_2(28) -> 29
, p_2(28) -> 33
, p_2(32) -> 5
, p_2(32) -> 25
, p_2(32) -> 29
, p_2(32) -> 33
, p_2(37) -> 34
, p_2(41) -> 6
, p_2(41) -> 11
, p_2(41) -> 15
, p_2(41) -> 17
, p_2(41) -> 54
, p_2(41) -> 150
, p_2(41) -> 154
, p_2(50) -> 47
, p_2(50) -> 133
, p_2(50) -> 137
, p_2(52) -> 47
, p_2(52) -> 133
, p_2(52) -> 137
, p_2(61) -> 1
, p_2(61) -> 10
, p_2(61) -> 61
, p_2(61) -> 65
, p_2(61) -> 69
, p_2(61) -> 77
, p_2(61) -> 81
, p_2(61) -> 91
, p_2(61) -> 95
, p_2(61) -> 102
, p_2(61) -> 111
, p_2(61) -> 128
, p_2(61) -> 132
, p_2(61) -> 139
, p_2(61) -> 148
, p_2(62) -> 1
, p_2(62) -> 10
, p_2(62) -> 61
, p_2(63) -> 62
, p_2(66) -> 1
, p_2(66) -> 10
, p_2(66) -> 61
, p_2(66) -> 65
, p_2(66) -> 69
, p_2(66) -> 77
, p_2(66) -> 81
, p_2(66) -> 91
, p_2(66) -> 95
, p_2(66) -> 102
, p_2(66) -> 111
, p_2(66) -> 128
, p_2(66) -> 132
, p_2(66) -> 139
, p_2(66) -> 148
, p_2(67) -> 66
, p_2(68) -> 1
, p_2(68) -> 10
, p_2(68) -> 61
, p_2(68) -> 65
, p_2(68) -> 69
, p_2(68) -> 77
, p_2(68) -> 81
, p_2(68) -> 91
, p_2(68) -> 95
, p_2(68) -> 102
, p_2(68) -> 111
, p_2(68) -> 128
, p_2(68) -> 132
, p_2(68) -> 139
, p_2(68) -> 148
, p_2(71) -> 70
, p_2(72) -> 71
, p_2(75) -> 70
, p_2(75) -> 74
, p_2(78) -> 1
, p_2(78) -> 10
, p_2(78) -> 61
, p_2(78) -> 65
, p_2(78) -> 69
, p_2(78) -> 77
, p_2(78) -> 81
, p_2(78) -> 91
, p_2(78) -> 95
, p_2(78) -> 102
, p_2(78) -> 111
, p_2(78) -> 128
, p_2(78) -> 132
, p_2(78) -> 139
, p_2(78) -> 148
, p_2(79) -> 78
, p_2(80) -> 1
, p_2(80) -> 10
, p_2(80) -> 61
, p_2(80) -> 65
, p_2(80) -> 69
, p_2(80) -> 77
, p_2(80) -> 81
, p_2(80) -> 91
, p_2(80) -> 95
, p_2(80) -> 102
, p_2(80) -> 111
, p_2(80) -> 128
, p_2(80) -> 132
, p_2(80) -> 139
, p_2(80) -> 148
, p_2(83) -> 82
, p_2(84) -> 83
, p_2(87) -> 82
, p_2(87) -> 86
, p_2(88) -> 1
, p_2(88) -> 10
, p_2(88) -> 61
, p_2(88) -> 65
, p_2(88) -> 69
, p_2(88) -> 77
, p_2(88) -> 81
, p_2(88) -> 91
, p_2(88) -> 95
, p_2(88) -> 102
, p_2(88) -> 111
, p_2(88) -> 128
, p_2(88) -> 132
, p_2(88) -> 139
, p_2(88) -> 148
, p_2(89) -> 1
, p_2(89) -> 10
, p_2(89) -> 61
, p_2(89) -> 65
, p_2(89) -> 69
, p_2(89) -> 77
, p_2(89) -> 81
, p_2(89) -> 88
, p_2(89) -> 91
, p_2(89) -> 95
, p_2(89) -> 102
, p_2(89) -> 111
, p_2(89) -> 128
, p_2(89) -> 132
, p_2(89) -> 139
, p_2(89) -> 148
, p_2(92) -> 1
, p_2(92) -> 10
, p_2(92) -> 61
, p_2(92) -> 65
, p_2(92) -> 69
, p_2(92) -> 77
, p_2(92) -> 81
, p_2(92) -> 91
, p_2(92) -> 95
, p_2(92) -> 102
, p_2(92) -> 111
, p_2(92) -> 128
, p_2(92) -> 132
, p_2(92) -> 139
, p_2(92) -> 148
, p_2(93) -> 92
, p_2(94) -> 1
, p_2(94) -> 10
, p_2(94) -> 61
, p_2(94) -> 65
, p_2(94) -> 69
, p_2(94) -> 77
, p_2(94) -> 81
, p_2(94) -> 91
, p_2(94) -> 95
, p_2(94) -> 102
, p_2(94) -> 111
, p_2(94) -> 128
, p_2(94) -> 132
, p_2(94) -> 139
, p_2(94) -> 148
, p_2(97) -> 96
, p_2(98) -> 97
, p_2(101) -> 96
, p_2(101) -> 100
, p_2(103) -> 1
, p_2(103) -> 10
, p_2(103) -> 61
, p_2(103) -> 65
, p_2(103) -> 69
, p_2(103) -> 77
, p_2(103) -> 81
, p_2(103) -> 91
, p_2(103) -> 95
, p_2(103) -> 102
, p_2(103) -> 111
, p_2(103) -> 128
, p_2(103) -> 132
, p_2(103) -> 139
, p_2(103) -> 148
, p_2(104) -> 103
, p_2(109) -> 1
, p_2(109) -> 10
, p_2(109) -> 61
, p_2(109) -> 65
, p_2(109) -> 69
, p_2(109) -> 77
, p_2(109) -> 81
, p_2(109) -> 91
, p_2(109) -> 95
, p_2(109) -> 102
, p_2(109) -> 111
, p_2(109) -> 128
, p_2(109) -> 132
, p_2(109) -> 139
, p_2(109) -> 148
, p_2(114) -> 113
, p_2(115) -> 114
, p_2(118) -> 113
, p_2(118) -> 117
, p_2(125) -> 1
, p_2(125) -> 10
, p_2(125) -> 61
, p_2(125) -> 65
, p_2(125) -> 69
, p_2(125) -> 77
, p_2(125) -> 81
, p_2(125) -> 91
, p_2(125) -> 95
, p_2(125) -> 102
, p_2(125) -> 111
, p_2(125) -> 128
, p_2(125) -> 132
, p_2(125) -> 139
, p_2(125) -> 148
, p_2(126) -> 1
, p_2(126) -> 10
, p_2(126) -> 61
, p_2(126) -> 65
, p_2(126) -> 69
, p_2(126) -> 77
, p_2(126) -> 81
, p_2(126) -> 91
, p_2(126) -> 95
, p_2(126) -> 102
, p_2(126) -> 111
, p_2(126) -> 125
, p_2(126) -> 128
, p_2(126) -> 132
, p_2(126) -> 139
, p_2(126) -> 148
, p_2(129) -> 1
, p_2(129) -> 10
, p_2(129) -> 61
, p_2(129) -> 65
, p_2(129) -> 69
, p_2(129) -> 77
, p_2(129) -> 81
, p_2(129) -> 91
, p_2(129) -> 95
, p_2(129) -> 102
, p_2(129) -> 111
, p_2(129) -> 128
, p_2(129) -> 132
, p_2(129) -> 139
, p_2(129) -> 148
, p_2(130) -> 129
, p_2(134) -> 133
, p_2(135) -> 134
, p_2(138) -> 133
, p_2(138) -> 137
, p_2(140) -> 1
, p_2(140) -> 10
, p_2(140) -> 61
, p_2(140) -> 65
, p_2(140) -> 69
, p_2(140) -> 77
, p_2(140) -> 81
, p_2(140) -> 91
, p_2(140) -> 95
, p_2(140) -> 102
, p_2(140) -> 111
, p_2(140) -> 128
, p_2(140) -> 132
, p_2(140) -> 139
, p_2(140) -> 148
, p_2(141) -> 140
, p_2(151) -> 150
, p_2(152) -> 151
, p_2(155) -> 150
, p_2(155) -> 154
, p_3(64) -> 1
, p_3(64) -> 10
, p_3(64) -> 61
, p_3(65) -> 1
, p_3(65) -> 10
, p_3(65) -> 61
, p_3(65) -> 65
, p_3(65) -> 69
, p_3(65) -> 77
, p_3(65) -> 81
, p_3(65) -> 91
, p_3(65) -> 95
, p_3(65) -> 102
, p_3(65) -> 111
, p_3(65) -> 128
, p_3(65) -> 132
, p_3(65) -> 139
, p_3(65) -> 148
, p_3(68) -> 1
, p_3(68) -> 10
, p_3(68) -> 61
, p_3(68) -> 65
, p_3(68) -> 69
, p_3(68) -> 77
, p_3(68) -> 81
, p_3(68) -> 91
, p_3(68) -> 95
, p_3(68) -> 102
, p_3(68) -> 111
, p_3(68) -> 128
, p_3(68) -> 132
, p_3(68) -> 139
, p_3(68) -> 148
, p_3(69) -> 1
, p_3(69) -> 10
, p_3(69) -> 61
, p_3(69) -> 65
, p_3(69) -> 69
, p_3(69) -> 77
, p_3(69) -> 81
, p_3(69) -> 91
, p_3(69) -> 95
, p_3(69) -> 102
, p_3(69) -> 111
, p_3(69) -> 128
, p_3(69) -> 132
, p_3(69) -> 139
, p_3(69) -> 148
, p_3(73) -> 70
, p_3(76) -> 1
, p_3(76) -> 10
, p_3(76) -> 61
, p_3(76) -> 65
, p_3(76) -> 69
, p_3(76) -> 77
, p_3(76) -> 81
, p_3(76) -> 91
, p_3(76) -> 95
, p_3(76) -> 102
, p_3(76) -> 111
, p_3(76) -> 128
, p_3(76) -> 132
, p_3(76) -> 139
, p_3(76) -> 148
, p_3(77) -> 1
, p_3(77) -> 10
, p_3(77) -> 61
, p_3(77) -> 65
, p_3(77) -> 69
, p_3(77) -> 77
, p_3(77) -> 81
, p_3(77) -> 91
, p_3(77) -> 95
, p_3(77) -> 102
, p_3(77) -> 111
, p_3(77) -> 128
, p_3(77) -> 132
, p_3(77) -> 139
, p_3(77) -> 148
, p_3(80) -> 1
, p_3(80) -> 10
, p_3(80) -> 61
, p_3(80) -> 65
, p_3(80) -> 69
, p_3(80) -> 77
, p_3(80) -> 81
, p_3(80) -> 91
, p_3(80) -> 95
, p_3(80) -> 102
, p_3(80) -> 111
, p_3(80) -> 128
, p_3(80) -> 132
, p_3(80) -> 139
, p_3(80) -> 148
, p_3(81) -> 1
, p_3(81) -> 10
, p_3(81) -> 61
, p_3(81) -> 65
, p_3(81) -> 69
, p_3(81) -> 77
, p_3(81) -> 81
, p_3(81) -> 91
, p_3(81) -> 95
, p_3(81) -> 102
, p_3(81) -> 111
, p_3(81) -> 128
, p_3(81) -> 132
, p_3(81) -> 139
, p_3(81) -> 148
, p_3(85) -> 82
, p_3(88) -> 1
, p_3(88) -> 10
, p_3(88) -> 61
, p_3(88) -> 65
, p_3(88) -> 69
, p_3(88) -> 77
, p_3(88) -> 81
, p_3(88) -> 91
, p_3(88) -> 95
, p_3(88) -> 102
, p_3(88) -> 111
, p_3(88) -> 128
, p_3(88) -> 132
, p_3(88) -> 139
, p_3(88) -> 148
, p_3(90) -> 1
, p_3(90) -> 10
, p_3(90) -> 61
, p_3(90) -> 65
, p_3(90) -> 69
, p_3(90) -> 77
, p_3(90) -> 81
, p_3(90) -> 91
, p_3(90) -> 95
, p_3(90) -> 102
, p_3(90) -> 111
, p_3(90) -> 128
, p_3(90) -> 132
, p_3(90) -> 139
, p_3(90) -> 148
, p_3(91) -> 1
, p_3(91) -> 10
, p_3(91) -> 61
, p_3(91) -> 65
, p_3(91) -> 69
, p_3(91) -> 77
, p_3(91) -> 81
, p_3(91) -> 91
, p_3(91) -> 95
, p_3(91) -> 102
, p_3(91) -> 111
, p_3(91) -> 128
, p_3(91) -> 132
, p_3(91) -> 139
, p_3(91) -> 148
, p_3(94) -> 1
, p_3(94) -> 10
, p_3(94) -> 61
, p_3(94) -> 65
, p_3(94) -> 69
, p_3(94) -> 77
, p_3(94) -> 81
, p_3(94) -> 91
, p_3(94) -> 95
, p_3(94) -> 102
, p_3(94) -> 111
, p_3(94) -> 128
, p_3(94) -> 132
, p_3(94) -> 139
, p_3(94) -> 148
, p_3(95) -> 1
, p_3(95) -> 10
, p_3(95) -> 61
, p_3(95) -> 65
, p_3(95) -> 69
, p_3(95) -> 77
, p_3(95) -> 81
, p_3(95) -> 91
, p_3(95) -> 95
, p_3(95) -> 102
, p_3(95) -> 111
, p_3(95) -> 128
, p_3(95) -> 132
, p_3(95) -> 139
, p_3(95) -> 148
, p_3(99) -> 96
, p_3(102) -> 1
, p_3(102) -> 10
, p_3(102) -> 61
, p_3(102) -> 65
, p_3(102) -> 69
, p_3(102) -> 77
, p_3(102) -> 81
, p_3(102) -> 91
, p_3(102) -> 95
, p_3(102) -> 102
, p_3(102) -> 111
, p_3(102) -> 128
, p_3(102) -> 132
, p_3(102) -> 139
, p_3(102) -> 148
, p_3(109) -> 1
, p_3(109) -> 10
, p_3(109) -> 61
, p_3(109) -> 65
, p_3(109) -> 69
, p_3(109) -> 77
, p_3(109) -> 81
, p_3(109) -> 91
, p_3(109) -> 95
, p_3(109) -> 102
, p_3(109) -> 111
, p_3(109) -> 128
, p_3(109) -> 132
, p_3(109) -> 139
, p_3(109) -> 148
, p_3(111) -> 1
, p_3(111) -> 10
, p_3(111) -> 61
, p_3(111) -> 65
, p_3(111) -> 69
, p_3(111) -> 77
, p_3(111) -> 81
, p_3(111) -> 91
, p_3(111) -> 95
, p_3(111) -> 102
, p_3(111) -> 111
, p_3(111) -> 128
, p_3(111) -> 132
, p_3(111) -> 139
, p_3(111) -> 148
, p_3(116) -> 113
, p_3(125) -> 1
, p_3(125) -> 10
, p_3(125) -> 61
, p_3(125) -> 65
, p_3(125) -> 69
, p_3(125) -> 77
, p_3(125) -> 81
, p_3(125) -> 91
, p_3(125) -> 95
, p_3(125) -> 102
, p_3(125) -> 111
, p_3(125) -> 128
, p_3(125) -> 132
, p_3(125) -> 139
, p_3(125) -> 148
, p_3(127) -> 1
, p_3(127) -> 10
, p_3(127) -> 61
, p_3(127) -> 65
, p_3(127) -> 69
, p_3(127) -> 77
, p_3(127) -> 81
, p_3(127) -> 91
, p_3(127) -> 95
, p_3(127) -> 102
, p_3(127) -> 111
, p_3(127) -> 128
, p_3(127) -> 132
, p_3(127) -> 139
, p_3(127) -> 148
, p_3(128) -> 1
, p_3(128) -> 10
, p_3(128) -> 61
, p_3(128) -> 65
, p_3(128) -> 69
, p_3(128) -> 77
, p_3(128) -> 81
, p_3(128) -> 91
, p_3(128) -> 95
, p_3(128) -> 102
, p_3(128) -> 111
, p_3(128) -> 128
, p_3(128) -> 132
, p_3(128) -> 139
, p_3(128) -> 148
, p_3(131) -> 1
, p_3(131) -> 10
, p_3(131) -> 61
, p_3(131) -> 65
, p_3(131) -> 69
, p_3(131) -> 77
, p_3(131) -> 81
, p_3(131) -> 91
, p_3(131) -> 95
, p_3(131) -> 102
, p_3(131) -> 111
, p_3(131) -> 128
, p_3(131) -> 132
, p_3(131) -> 139
, p_3(131) -> 148
, p_3(132) -> 1
, p_3(132) -> 10
, p_3(132) -> 61
, p_3(132) -> 65
, p_3(132) -> 69
, p_3(132) -> 77
, p_3(132) -> 81
, p_3(132) -> 91
, p_3(132) -> 95
, p_3(132) -> 102
, p_3(132) -> 111
, p_3(132) -> 128
, p_3(132) -> 132
, p_3(132) -> 139
, p_3(132) -> 148
, p_3(136) -> 133
, p_3(139) -> 1
, p_3(139) -> 10
, p_3(139) -> 61
, p_3(139) -> 65
, p_3(139) -> 69
, p_3(139) -> 77
, p_3(139) -> 81
, p_3(139) -> 91
, p_3(139) -> 95
, p_3(139) -> 102
, p_3(139) -> 111
, p_3(139) -> 128
, p_3(139) -> 132
, p_3(139) -> 139
, p_3(139) -> 148
, p_3(146) -> 1
, p_3(146) -> 10
, p_3(146) -> 61
, p_3(146) -> 65
, p_3(146) -> 69
, p_3(146) -> 77
, p_3(146) -> 81
, p_3(146) -> 91
, p_3(146) -> 95
, p_3(146) -> 102
, p_3(146) -> 111
, p_3(146) -> 128
, p_3(146) -> 132
, p_3(146) -> 139
, p_3(146) -> 148
, p_3(148) -> 1
, p_3(148) -> 10
, p_3(148) -> 61
, p_3(148) -> 65
, p_3(148) -> 69
, p_3(148) -> 77
, p_3(148) -> 81
, p_3(148) -> 91
, p_3(148) -> 95
, p_3(148) -> 102
, p_3(148) -> 111
, p_3(148) -> 128
, p_3(148) -> 132
, p_3(148) -> 139
, p_3(148) -> 148
, p_3(153) -> 150
, s_0(4) -> 2
, s_0(4) -> 3
, s_0(4) -> 4
, s_0(4) -> 18
, s_0(4) -> 20
, s_0(4) -> 34
, s_0(4) -> 38
, s_0(4) -> 55
, s_0(4) -> 57
, s_1(4) -> 21
, s_1(4) -> 23
, s_1(4) -> 58
, s_1(9) -> 8
, s_1(10) -> 7
, s_1(10) -> 9
, s_1(14) -> 13
, s_1(15) -> 12
, s_1(15) -> 14
, s_1(17) -> 16
, s_1(20) -> 19
, s_1(22) -> 60
, s_1(23) -> 22
, s_1(23) -> 59
, s_1(25) -> 24
, s_1(26) -> 24
, s_1(28) -> 27
, s_1(29) -> 5
, s_1(29) -> 25
, s_1(29) -> 26
, s_1(29) -> 28
, s_1(29) -> 29
, s_1(29) -> 33
, s_1(32) -> 31
, s_1(33) -> 30
, s_1(33) -> 32
, s_1(37) -> 36
, s_1(38) -> 35
, s_1(38) -> 37
, s_1(41) -> 40
, s_1(42) -> 39
, s_1(42) -> 41
, s_1(43) -> 6
, s_1(43) -> 11
, s_1(43) -> 15
, s_1(43) -> 17
, s_1(43) -> 42
, s_1(43) -> 54
, s_1(43) -> 150
, s_1(43) -> 154
, s_1(44) -> 43
, s_1(44) -> 70
, s_1(44) -> 74
, s_1(45) -> 44
, s_1(45) -> 82
, s_1(45) -> 86
, s_1(46) -> 45
, s_1(46) -> 96
, s_1(46) -> 100
, s_1(47) -> 46
, s_1(47) -> 113
, s_1(47) -> 117
, s_1(50) -> 49
, s_1(52) -> 51
, s_1(53) -> 48
, s_1(53) -> 50
, s_1(53) -> 52
, s_1(54) -> 47
, s_1(54) -> 53
, s_1(54) -> 133
, s_1(54) -> 137
, s_1(57) -> 56
, s_2(43) -> 75
, s_2(44) -> 87
, s_2(45) -> 101
, s_2(46) -> 118
, s_2(47) -> 138
, s_2(54) -> 155
, s_2(61) -> 7
, s_2(61) -> 9
, s_2(64) -> 63
, s_2(65) -> 62
, s_2(65) -> 64
, s_2(68) -> 67
, s_2(69) -> 66
, s_2(69) -> 68
, s_2(73) -> 72
, s_2(74) -> 71
, s_2(74) -> 73
, s_2(76) -> 62
, s_2(77) -> 1
, s_2(77) -> 10
, s_2(77) -> 61
, s_2(77) -> 76
, s_2(80) -> 79
, s_2(81) -> 78
, s_2(81) -> 80
, s_2(85) -> 84
, s_2(86) -> 83
, s_2(86) -> 85
, s_2(88) -> 66
, s_2(90) -> 89
, s_2(91) -> 1
, s_2(91) -> 10
, s_2(91) -> 61
, s_2(91) -> 65
, s_2(91) -> 69
, s_2(91) -> 77
, s_2(91) -> 81
, s_2(91) -> 88
, s_2(91) -> 90
, s_2(91) -> 91
, s_2(91) -> 95
, s_2(91) -> 102
, s_2(91) -> 111
, s_2(91) -> 128
, s_2(91) -> 132
, s_2(91) -> 139
, s_2(91) -> 148
, s_2(94) -> 93
, s_2(95) -> 92
, s_2(95) -> 94
, s_2(99) -> 98
, s_2(100) -> 97
, s_2(100) -> 99
, s_2(102) -> 1
, s_2(102) -> 10
, s_2(102) -> 61
, s_2(102) -> 65
, s_2(102) -> 69
, s_2(102) -> 77
, s_2(102) -> 81
, s_2(102) -> 91
, s_2(102) -> 95
, s_2(102) -> 102
, s_2(102) -> 111
, s_2(102) -> 128
, s_2(102) -> 132
, s_2(102) -> 139
, s_2(102) -> 148
, s_2(109) -> 104
, s_2(111) -> 103
, s_2(111) -> 109
, s_2(116) -> 115
, s_2(117) -> 114
, s_2(117) -> 116
, s_2(125) -> 66
, s_2(125) -> 68
, s_2(127) -> 126
, s_2(128) -> 1
, s_2(128) -> 10
, s_2(128) -> 61
, s_2(128) -> 65
, s_2(128) -> 69
, s_2(128) -> 77
, s_2(128) -> 81
, s_2(128) -> 91
, s_2(128) -> 95
, s_2(128) -> 102
, s_2(128) -> 111
, s_2(128) -> 125
, s_2(128) -> 127
, s_2(128) -> 128
, s_2(128) -> 132
, s_2(128) -> 139
, s_2(128) -> 148
, s_2(131) -> 130
, s_2(132) -> 129
, s_2(132) -> 131
, s_2(136) -> 135
, s_2(137) -> 134
, s_2(137) -> 136
, s_2(139) -> 1
, s_2(139) -> 10
, s_2(139) -> 61
, s_2(139) -> 65
, s_2(139) -> 69
, s_2(139) -> 77
, s_2(139) -> 81
, s_2(139) -> 91
, s_2(139) -> 95
, s_2(139) -> 102
, s_2(139) -> 111
, s_2(139) -> 128
, s_2(139) -> 132
, s_2(139) -> 139
, s_2(139) -> 148
, s_2(146) -> 141
, s_2(148) -> 140
, s_2(148) -> 146
, s_2(153) -> 152
, s_2(154) -> 151
, s_2(154) -> 153
, half_0(4) -> 5
, half_1(11) -> 1
, half_1(11) -> 10
, half_1(34) -> 5
, half_1(34) -> 25
, half_1(34) -> 29
, half_1(34) -> 33
, half_2(70) -> 1
, half_2(70) -> 10
, half_2(70) -> 61
, half_2(70) -> 65
, half_2(70) -> 69
, half_2(70) -> 77
, half_2(70) -> 81
, half_2(70) -> 91
, half_2(70) -> 95
, half_2(70) -> 102
, half_2(70) -> 111
, half_2(70) -> 128
, half_2(70) -> 132
, half_2(70) -> 139
, half_2(70) -> 148
, half_2(82) -> 1
, half_2(82) -> 10
, half_2(82) -> 61
, half_2(82) -> 65
, half_2(82) -> 69
, half_2(82) -> 77
, half_2(82) -> 81
, half_2(82) -> 91
, half_2(82) -> 95
, half_2(82) -> 102
, half_2(82) -> 111
, half_2(82) -> 128
, half_2(82) -> 132
, half_2(82) -> 139
, half_2(82) -> 148
, half_2(96) -> 1
, half_2(96) -> 10
, half_2(96) -> 61
, half_2(96) -> 65
, half_2(96) -> 69
, half_2(96) -> 77
, half_2(96) -> 81
, half_2(96) -> 91
, half_2(96) -> 95
, half_2(96) -> 102
, half_2(96) -> 111
, half_2(96) -> 128
, half_2(96) -> 132
, half_2(96) -> 139
, half_2(96) -> 148
, half_2(113) -> 1
, half_2(113) -> 10
, half_2(113) -> 61
, half_2(113) -> 65
, half_2(113) -> 69
, half_2(113) -> 77
, half_2(113) -> 81
, half_2(113) -> 91
, half_2(113) -> 95
, half_2(113) -> 102
, half_2(113) -> 111
, half_2(113) -> 128
, half_2(113) -> 132
, half_2(113) -> 139
, half_2(113) -> 148
, half_2(133) -> 1
, half_2(133) -> 10
, half_2(133) -> 61
, half_2(133) -> 65
, half_2(133) -> 69
, half_2(133) -> 77
, half_2(133) -> 81
, half_2(133) -> 91
, half_2(133) -> 95
, half_2(133) -> 102
, half_2(133) -> 111
, half_2(133) -> 128
, half_2(133) -> 132
, half_2(133) -> 139
, half_2(133) -> 148
, half_2(150) -> 1
, half_2(150) -> 10
, half_2(150) -> 61
, half_2(150) -> 65
, half_2(150) -> 69
, half_2(150) -> 77
, half_2(150) -> 81
, half_2(150) -> 91
, half_2(150) -> 95
, half_2(150) -> 102
, half_2(150) -> 111
, half_2(150) -> 128
, half_2(150) -> 132
, half_2(150) -> 139
, half_2(150) -> 148
, sixtimes_0(4) -> 6
, sixtimes_1(18) -> 11
, sixtimes_1(18) -> 15
, sixtimes_1(18) -> 17
, sixtimes_1(55) -> 54
, sixtimes_1(55) -> 150
, sixtimes_1(55) -> 154}