Tool CaT
stdout:
YES(?,O(n^1))
Problem:
foo(0(x1)) -> 0(s(p(p(p(s(s(s(p(s(x1))))))))))
foo(s(x1)) -> p(s(p(p(p(s(s(p(s(s(p(s(foo(p(p(s(s(p(s(bar(p(p(s(s(p(s(x1))))))))))))))))))))))))))
bar(0(x1)) -> 0(p(s(s(s(x1)))))
bar(s(x1)) -> p(s(p(p(s(s(foo(s(p(p(s(s(x1))))))))))))
p(p(s(x1))) -> p(x1)
p(s(x1)) -> x1
p(0(x1)) -> 0(s(s(s(s(x1)))))
Proof:
Bounds Processor:
bound: 4
enrichment: match
automaton:
final states: {5,4,3}
transitions:
02(223) -> 224*
01(15) -> 16*
01(114) -> 115*
01(86) -> 87*
03(247) -> 248*
s1(45) -> 46*
s1(35) -> 36*
s1(30) -> 31*
s1(10) -> 11*
s1(92) -> 93*
s1(52) -> 53*
s1(47) -> 48*
s1(42) -> 43*
s1(37) -> 38*
s1(84) -> 85*
s1(44) -> 45*
s1(14) -> 15*
s1(9) -> 10*
s1(96) -> 97*
s1(6) -> 7*
s1(113) -> 114*
s1(93) -> 94*
s1(83) -> 84*
s1(48) -> 49*
s1(38) -> 39*
s1(8) -> 9*
s1(90) -> 91*
s3(242) -> 243*
s3(264) -> 265*
s3(246) -> 247*
s3(241) -> 242*
s3(238) -> 239*
s3(240) -> 241*
p1(50) -> 51*
p1(40) -> 41*
p1(97) -> 98*
p1(32) -> 33*
p1(12) -> 13*
p1(7) -> 8*
p1(94) -> 95*
p1(89) -> 90*
p1(49) -> 50*
p1(39) -> 40*
p1(51) -> 52*
p1(46) -> 47*
p1(36) -> 37*
p1(11) -> 12*
p1(88) -> 89*
p1(53) -> 54*
p1(43) -> 44*
p1(33) -> 34*
p1(13) -> 14*
p1(95) -> 96*
p1(85) -> 86*
p4(266) -> 267*
p4(270) -> 271*
foo1(91) -> 92*
foo1(41) -> 42*
bar1(34) -> 35*
p2(182) -> 183*
p2(172) -> 173*
p2(137) -> 138*
p2(127) -> 128*
p2(117) -> 118*
p2(219) -> 220*
p2(174) -> 175*
p2(139) -> 140*
p2(134) -> 135*
p2(124) -> 125*
p2(221) -> 222*
p2(141) -> 142*
p2(131) -> 132*
p2(121) -> 122*
p2(188) -> 189*
p2(138) -> 139*
p2(128) -> 129*
p2(220) -> 221*
p2(215) -> 216*
p2(200) -> 201*
p2(190) -> 191*
p2(180) -> 181*
p2(120) -> 121*
foo0(2) -> 3*
foo0(1) -> 3*
s2(222) -> 223*
s2(217) -> 218*
s2(132) -> 133*
s2(214) -> 215*
s2(119) -> 120*
s2(216) -> 217*
s2(136) -> 137*
s2(126) -> 127*
s2(116) -> 117*
s2(218) -> 219*
s2(133) -> 134*
s2(123) -> 124*
s2(118) -> 119*
s2(140) -> 141*
s2(135) -> 136*
s2(130) -> 131*
s2(125) -> 126*
00(2) -> 1*
00(1) -> 1*
foo2(129) -> 130*
s0(2) -> 2*
s0(1) -> 2*
bar2(122) -> 123*
p0(2) -> 5*
p0(1) -> 5*
p3(262) -> 263*
p3(244) -> 245*
p3(239) -> 240*
p3(204) -> 205*
p3(194) -> 195*
p3(236) -> 237*
p3(206) -> 207*
p3(243) -> 244*
p3(245) -> 246*
p3(210) -> 211*
bar0(2) -> 4*
bar0(1) -> 4*
1 -> 5,30
2 -> 5,6
6 -> 175,8
7 -> 83*
8 -> 183,34
9 -> 189,33,182
10 -> 12,188,32
16 -> 3*
30 -> 175,8
31 -> 7*
35 -> 37*
37 -> 123,125,205,173
38 -> 40,172
41 -> 35*
42 -> 44*
44 -> 201*
45 -> 47*
47 -> 191,51,200
48 -> 50,190
52 -> 54*
54 -> 3*
83 -> 89,174
84 -> 86,88
85 -> 113*
86 -> 214*
87 -> 123,125,205,35,37,41,4
90 -> 116*
92 -> 181*
93 -> 95,180
96 -> 98,4
98 -> 37,41,4
115 -> 5*
116 -> 118*
118 -> 207,122
119 -> 121,206
123 -> 125*
125 -> 205,129
126 -> 128,204
130 -> 132*
132 -> 211,140,142
133 -> 135*
135 -> 195,210
136 -> 138,194
140 -> 142,92
142 -> 92*
173 -> 41*
175 -> 90*
181 -> 96*
183 -> 14,34
189 -> 13*
191 -> 51*
195 -> 139*
201 -> 52*
205 -> 129*
207 -> 122*
211 -> 140,142,96
214 -> 216*
216 -> 263,222
217 -> 237,221,262
218 -> 220,236
223 -> 238*
224 -> 130,132,140,181,98,37,123,129,42,44,52,3
237 -> 221*
238 -> 240*
240 -> 271*
241 -> 267,245,270
242 -> 244,266
247 -> 264*
248 -> 130,42,44,52,3,132,140,181,98,37,123,129
263 -> 222*
264 -> 240*
265 -> 239*
267 -> 245*
271 -> 246*
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:
{ foo(0(x1)) -> 0(s(p(p(p(s(s(s(p(s(x1))))))))))
, foo(s(x1)) ->
p(s(p(p(p(s(s(p(s(s(p(s(foo(p(p(s(s(p(s(bar(p(p(s(s(p(s(x1))))))))))))))))))))))))))
, bar(0(x1)) -> 0(p(s(s(s(x1)))))
, bar(s(x1)) -> p(s(p(p(s(s(foo(s(p(p(s(s(x1))))))))))))
, p(p(s(x1))) -> p(x1)
, p(s(x1)) -> x1
, p(0(x1)) -> 0(s(s(s(s(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:
{ foo(0(x1)) -> 0(s(p(p(p(s(s(s(p(s(x1))))))))))
, foo(s(x1)) ->
p(s(p(p(p(s(s(p(s(s(p(s(foo(p(p(s(s(p(s(bar(p(p(s(s(p(s(x1))))))))))))))))))))))))))
, bar(0(x1)) -> 0(p(s(s(s(x1)))))
, bar(s(x1)) -> p(s(p(p(s(s(foo(s(p(p(s(s(x1))))))))))))
, p(p(s(x1))) -> p(x1)
, p(s(x1)) -> x1
, p(0(x1)) -> 0(s(s(s(s(x1)))))}
Proof Output:
The problem is match-bounded by 4.
The enriched problem is compatible with the following automaton:
{ foo_0(2) -> 1
, foo_1(24) -> 1
, foo_1(24) -> 13
, foo_1(24) -> 21
, foo_1(24) -> 23
, foo_1(24) -> 24
, foo_1(24) -> 28
, foo_1(24) -> 30
, foo_1(24) -> 51
, foo_1(24) -> 55
, foo_1(24) -> 57
, foo_1(37) -> 1
, foo_1(37) -> 13
, foo_1(37) -> 24
, foo_1(37) -> 28
, foo_1(37) -> 30
, foo_1(37) -> 36
, foo_1(37) -> 51
, foo_1(37) -> 55
, foo_1(37) -> 57
, foo_2(51) -> 1
, foo_2(51) -> 13
, foo_2(51) -> 24
, foo_2(51) -> 28
, foo_2(51) -> 30
, foo_2(51) -> 36
, foo_2(51) -> 40
, foo_2(51) -> 48
, foo_2(51) -> 50
, foo_2(51) -> 51
, foo_2(51) -> 55
, foo_2(51) -> 57
, 0_0(2) -> 1
, 0_0(2) -> 2
, 0_0(2) -> 4
, 0_0(2) -> 10
, 0_0(2) -> 31
, 0_0(2) -> 38
, 0_0(2) -> 58
, 0_0(2) -> 62
, 0_1(3) -> 1
, 0_1(3) -> 24
, 0_1(3) -> 28
, 0_1(3) -> 30
, 0_1(3) -> 51
, 0_1(3) -> 55
, 0_1(3) -> 57
, 0_2(64) -> 1
, 0_2(64) -> 13
, 0_2(64) -> 21
, 0_2(64) -> 23
, 0_2(64) -> 24
, 0_2(64) -> 28
, 0_2(64) -> 30
, 0_2(64) -> 36
, 0_2(64) -> 40
, 0_2(64) -> 48
, 0_2(64) -> 50
, 0_2(64) -> 51
, 0_2(64) -> 55
, 0_2(64) -> 57
, 0_3(73) -> 1
, 0_3(73) -> 13
, 0_3(73) -> 24
, 0_3(73) -> 28
, 0_3(73) -> 30
, 0_3(73) -> 36
, 0_3(73) -> 40
, 0_3(73) -> 48
, 0_3(73) -> 50
, 0_3(73) -> 51
, 0_3(73) -> 55
, 0_3(73) -> 57
, s_0(2) -> 1
, s_0(2) -> 2
, s_0(2) -> 4
, s_0(2) -> 10
, s_0(2) -> 31
, s_0(2) -> 38
, s_0(2) -> 58
, s_0(2) -> 62
, s_1(2) -> 11
, s_1(2) -> 39
, s_1(4) -> 3
, s_1(4) -> 65
, s_1(4) -> 71
, s_1(8) -> 7
, s_1(9) -> 6
, s_1(9) -> 8
, s_1(10) -> 5
, s_1(10) -> 9
, s_1(10) -> 32
, s_1(11) -> 3
, s_1(11) -> 34
, s_1(11) -> 65
, s_1(11) -> 71
, s_1(13) -> 12
, s_1(17) -> 16
, s_1(18) -> 15
, s_1(18) -> 17
, s_1(20) -> 19
, s_1(21) -> 14
, s_1(21) -> 18
, s_1(21) -> 20
, s_1(23) -> 22
, s_1(27) -> 26
, s_1(28) -> 25
, s_1(28) -> 27
, s_1(30) -> 29
, s_1(33) -> 3
, s_1(33) -> 65
, s_1(33) -> 71
, s_1(34) -> 33
, s_1(35) -> 15
, s_1(36) -> 14
, s_1(36) -> 35
, s_1(38) -> 37
, s_2(3) -> 72
, s_2(38) -> 63
, s_2(40) -> 14
, s_2(40) -> 35
, s_2(44) -> 43
, s_2(45) -> 42
, s_2(45) -> 44
, s_2(47) -> 46
, s_2(48) -> 41
, s_2(48) -> 45
, s_2(48) -> 47
, s_2(50) -> 49
, s_2(54) -> 53
, s_2(55) -> 52
, s_2(55) -> 54
, s_2(57) -> 56
, s_2(61) -> 60
, s_2(62) -> 59
, s_2(62) -> 61
, s_2(64) -> 72
, s_2(65) -> 64
, s_2(65) -> 65
, s_2(65) -> 71
, s_2(65) -> 74
, s_2(65) -> 80
, s_2(69) -> 68
, s_2(70) -> 67
, s_2(70) -> 69
, s_2(71) -> 66
, s_2(71) -> 70
, s_2(73) -> 72
, s_3(64) -> 81
, s_3(73) -> 81
, s_3(74) -> 65
, s_3(74) -> 71
, s_3(74) -> 73
, s_3(74) -> 74
, s_3(74) -> 80
, s_3(78) -> 77
, s_3(79) -> 76
, s_3(79) -> 78
, s_3(80) -> 75
, s_3(80) -> 79
, p_0(2) -> 1
, p_1(5) -> 4
, p_1(6) -> 5
, p_1(7) -> 6
, p_1(8) -> 32
, p_1(11) -> 4
, p_1(11) -> 10
, p_1(11) -> 31
, p_1(12) -> 1
, p_1(12) -> 24
, p_1(12) -> 28
, p_1(12) -> 30
, p_1(12) -> 51
, p_1(12) -> 55
, p_1(12) -> 57
, p_1(14) -> 1
, p_1(14) -> 13
, p_1(14) -> 24
, p_1(14) -> 28
, p_1(14) -> 30
, p_1(14) -> 51
, p_1(14) -> 55
, p_1(14) -> 57
, p_1(15) -> 14
, p_1(16) -> 15
, p_1(19) -> 14
, p_1(19) -> 18
, p_1(22) -> 1
, p_1(22) -> 13
, p_1(22) -> 21
, p_1(22) -> 24
, p_1(22) -> 28
, p_1(22) -> 30
, p_1(22) -> 51
, p_1(22) -> 55
, p_1(22) -> 57
, p_1(25) -> 24
, p_1(26) -> 25
, p_1(29) -> 24
, p_1(29) -> 28
, p_1(29) -> 51
, p_1(29) -> 55
, p_1(29) -> 57
, p_1(32) -> 31
, p_1(33) -> 3
, p_1(33) -> 65
, p_1(33) -> 71
, p_1(34) -> 39
, p_1(39) -> 38
, p_1(39) -> 58
, p_1(39) -> 62
, p_2(8) -> 5
, p_2(9) -> 4
, p_2(9) -> 31
, p_2(11) -> 38
, p_2(11) -> 58
, p_2(11) -> 62
, p_2(17) -> 14
, p_2(18) -> 1
, p_2(18) -> 13
, p_2(18) -> 24
, p_2(18) -> 28
, p_2(18) -> 30
, p_2(18) -> 51
, p_2(18) -> 55
, p_2(18) -> 57
, p_2(20) -> 1
, p_2(20) -> 13
, p_2(20) -> 24
, p_2(20) -> 28
, p_2(20) -> 30
, p_2(20) -> 51
, p_2(20) -> 55
, p_2(20) -> 57
, p_2(27) -> 24
, p_2(35) -> 1
, p_2(35) -> 13
, p_2(35) -> 24
, p_2(35) -> 28
, p_2(35) -> 30
, p_2(35) -> 36
, p_2(35) -> 51
, p_2(35) -> 55
, p_2(35) -> 57
, p_2(41) -> 1
, p_2(41) -> 13
, p_2(41) -> 24
, p_2(41) -> 28
, p_2(41) -> 30
, p_2(41) -> 36
, p_2(41) -> 40
, p_2(41) -> 51
, p_2(41) -> 55
, p_2(41) -> 57
, p_2(42) -> 41
, p_2(43) -> 42
, p_2(46) -> 41
, p_2(46) -> 45
, p_2(49) -> 1
, p_2(49) -> 13
, p_2(49) -> 24
, p_2(49) -> 28
, p_2(49) -> 30
, p_2(49) -> 36
, p_2(49) -> 40
, p_2(49) -> 48
, p_2(49) -> 51
, p_2(49) -> 55
, p_2(49) -> 57
, p_2(52) -> 51
, p_2(53) -> 52
, p_2(56) -> 51
, p_2(56) -> 55
, p_2(59) -> 58
, p_2(60) -> 59
, p_2(63) -> 58
, p_2(63) -> 62
, p_2(66) -> 65
, p_2(67) -> 66
, p_2(68) -> 67
, p_2(72) -> 65
, p_2(72) -> 71
, p_3(44) -> 41
, p_3(45) -> 1
, p_3(45) -> 13
, p_3(45) -> 24
, p_3(45) -> 28
, p_3(45) -> 30
, p_3(45) -> 36
, p_3(45) -> 40
, p_3(45) -> 51
, p_3(45) -> 55
, p_3(45) -> 57
, p_3(47) -> 1
, p_3(47) -> 13
, p_3(47) -> 24
, p_3(47) -> 28
, p_3(47) -> 30
, p_3(47) -> 36
, p_3(47) -> 40
, p_3(47) -> 51
, p_3(47) -> 55
, p_3(47) -> 57
, p_3(54) -> 51
, p_3(61) -> 58
, p_3(69) -> 66
, p_3(70) -> 65
, p_3(75) -> 74
, p_3(76) -> 75
, p_3(77) -> 76
, p_3(81) -> 74
, p_3(81) -> 80
, p_4(78) -> 75
, p_4(79) -> 74
, bar_0(2) -> 1
, bar_1(31) -> 24
, bar_1(31) -> 28
, bar_1(31) -> 30
, bar_1(31) -> 51
, bar_1(31) -> 55
, bar_1(31) -> 57
, bar_2(58) -> 51
, bar_2(58) -> 55
, bar_2(58) -> 57}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:
{ foo(0(x1)) -> 0(s(p(p(p(s(s(s(p(s(x1))))))))))
, foo(s(x1)) ->
p(s(p(p(p(s(s(p(s(s(p(s(foo(p(p(s(s(p(s(bar(p(p(s(s(p(s(x1))))))))))))))))))))))))))
, bar(0(x1)) -> 0(p(s(s(s(x1)))))
, bar(s(x1)) -> p(s(p(p(s(s(foo(s(p(p(s(s(x1))))))))))))
, p(p(s(x1))) -> p(x1)
, p(s(x1)) -> x1
, p(0(x1)) -> 0(s(s(s(s(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:
{ foo(0(x1)) -> 0(s(p(p(p(s(s(s(p(s(x1))))))))))
, foo(s(x1)) ->
p(s(p(p(p(s(s(p(s(s(p(s(foo(p(p(s(s(p(s(bar(p(p(s(s(p(s(x1))))))))))))))))))))))))))
, bar(0(x1)) -> 0(p(s(s(s(x1)))))
, bar(s(x1)) -> p(s(p(p(s(s(foo(s(p(p(s(s(x1))))))))))))
, p(p(s(x1))) -> p(x1)
, p(s(x1)) -> x1
, p(0(x1)) -> 0(s(s(s(s(x1)))))}
Proof Output:
The problem is match-bounded by 4.
The enriched problem is compatible with the following automaton:
{ foo_0(2) -> 1
, foo_1(24) -> 1
, foo_1(24) -> 13
, foo_1(24) -> 21
, foo_1(24) -> 23
, foo_1(24) -> 24
, foo_1(24) -> 28
, foo_1(24) -> 30
, foo_1(24) -> 51
, foo_1(24) -> 55
, foo_1(24) -> 57
, foo_1(37) -> 1
, foo_1(37) -> 13
, foo_1(37) -> 24
, foo_1(37) -> 28
, foo_1(37) -> 30
, foo_1(37) -> 36
, foo_1(37) -> 51
, foo_1(37) -> 55
, foo_1(37) -> 57
, foo_2(51) -> 1
, foo_2(51) -> 13
, foo_2(51) -> 24
, foo_2(51) -> 28
, foo_2(51) -> 30
, foo_2(51) -> 36
, foo_2(51) -> 40
, foo_2(51) -> 48
, foo_2(51) -> 50
, foo_2(51) -> 51
, foo_2(51) -> 55
, foo_2(51) -> 57
, 0_0(2) -> 1
, 0_0(2) -> 2
, 0_0(2) -> 4
, 0_0(2) -> 10
, 0_0(2) -> 31
, 0_0(2) -> 38
, 0_0(2) -> 58
, 0_0(2) -> 62
, 0_1(3) -> 1
, 0_1(3) -> 24
, 0_1(3) -> 28
, 0_1(3) -> 30
, 0_1(3) -> 51
, 0_1(3) -> 55
, 0_1(3) -> 57
, 0_2(64) -> 1
, 0_2(64) -> 13
, 0_2(64) -> 21
, 0_2(64) -> 23
, 0_2(64) -> 24
, 0_2(64) -> 28
, 0_2(64) -> 30
, 0_2(64) -> 36
, 0_2(64) -> 40
, 0_2(64) -> 48
, 0_2(64) -> 50
, 0_2(64) -> 51
, 0_2(64) -> 55
, 0_2(64) -> 57
, 0_3(73) -> 1
, 0_3(73) -> 13
, 0_3(73) -> 24
, 0_3(73) -> 28
, 0_3(73) -> 30
, 0_3(73) -> 36
, 0_3(73) -> 40
, 0_3(73) -> 48
, 0_3(73) -> 50
, 0_3(73) -> 51
, 0_3(73) -> 55
, 0_3(73) -> 57
, s_0(2) -> 1
, s_0(2) -> 2
, s_0(2) -> 4
, s_0(2) -> 10
, s_0(2) -> 31
, s_0(2) -> 38
, s_0(2) -> 58
, s_0(2) -> 62
, s_1(2) -> 11
, s_1(2) -> 39
, s_1(4) -> 3
, s_1(4) -> 65
, s_1(4) -> 71
, s_1(8) -> 7
, s_1(9) -> 6
, s_1(9) -> 8
, s_1(10) -> 5
, s_1(10) -> 9
, s_1(10) -> 32
, s_1(11) -> 3
, s_1(11) -> 34
, s_1(11) -> 65
, s_1(11) -> 71
, s_1(13) -> 12
, s_1(17) -> 16
, s_1(18) -> 15
, s_1(18) -> 17
, s_1(20) -> 19
, s_1(21) -> 14
, s_1(21) -> 18
, s_1(21) -> 20
, s_1(23) -> 22
, s_1(27) -> 26
, s_1(28) -> 25
, s_1(28) -> 27
, s_1(30) -> 29
, s_1(33) -> 3
, s_1(33) -> 65
, s_1(33) -> 71
, s_1(34) -> 33
, s_1(35) -> 15
, s_1(36) -> 14
, s_1(36) -> 35
, s_1(38) -> 37
, s_2(3) -> 72
, s_2(38) -> 63
, s_2(40) -> 14
, s_2(40) -> 35
, s_2(44) -> 43
, s_2(45) -> 42
, s_2(45) -> 44
, s_2(47) -> 46
, s_2(48) -> 41
, s_2(48) -> 45
, s_2(48) -> 47
, s_2(50) -> 49
, s_2(54) -> 53
, s_2(55) -> 52
, s_2(55) -> 54
, s_2(57) -> 56
, s_2(61) -> 60
, s_2(62) -> 59
, s_2(62) -> 61
, s_2(64) -> 72
, s_2(65) -> 64
, s_2(65) -> 65
, s_2(65) -> 71
, s_2(65) -> 74
, s_2(65) -> 80
, s_2(69) -> 68
, s_2(70) -> 67
, s_2(70) -> 69
, s_2(71) -> 66
, s_2(71) -> 70
, s_2(73) -> 72
, s_3(64) -> 81
, s_3(73) -> 81
, s_3(74) -> 65
, s_3(74) -> 71
, s_3(74) -> 73
, s_3(74) -> 74
, s_3(74) -> 80
, s_3(78) -> 77
, s_3(79) -> 76
, s_3(79) -> 78
, s_3(80) -> 75
, s_3(80) -> 79
, p_0(2) -> 1
, p_1(5) -> 4
, p_1(6) -> 5
, p_1(7) -> 6
, p_1(8) -> 32
, p_1(11) -> 4
, p_1(11) -> 10
, p_1(11) -> 31
, p_1(12) -> 1
, p_1(12) -> 24
, p_1(12) -> 28
, p_1(12) -> 30
, p_1(12) -> 51
, p_1(12) -> 55
, p_1(12) -> 57
, p_1(14) -> 1
, p_1(14) -> 13
, p_1(14) -> 24
, p_1(14) -> 28
, p_1(14) -> 30
, p_1(14) -> 51
, p_1(14) -> 55
, p_1(14) -> 57
, p_1(15) -> 14
, p_1(16) -> 15
, p_1(19) -> 14
, p_1(19) -> 18
, p_1(22) -> 1
, p_1(22) -> 13
, p_1(22) -> 21
, p_1(22) -> 24
, p_1(22) -> 28
, p_1(22) -> 30
, p_1(22) -> 51
, p_1(22) -> 55
, p_1(22) -> 57
, p_1(25) -> 24
, p_1(26) -> 25
, p_1(29) -> 24
, p_1(29) -> 28
, p_1(29) -> 51
, p_1(29) -> 55
, p_1(29) -> 57
, p_1(32) -> 31
, p_1(33) -> 3
, p_1(33) -> 65
, p_1(33) -> 71
, p_1(34) -> 39
, p_1(39) -> 38
, p_1(39) -> 58
, p_1(39) -> 62
, p_2(8) -> 5
, p_2(9) -> 4
, p_2(9) -> 31
, p_2(11) -> 38
, p_2(11) -> 58
, p_2(11) -> 62
, p_2(17) -> 14
, p_2(18) -> 1
, p_2(18) -> 13
, p_2(18) -> 24
, p_2(18) -> 28
, p_2(18) -> 30
, p_2(18) -> 51
, p_2(18) -> 55
, p_2(18) -> 57
, p_2(20) -> 1
, p_2(20) -> 13
, p_2(20) -> 24
, p_2(20) -> 28
, p_2(20) -> 30
, p_2(20) -> 51
, p_2(20) -> 55
, p_2(20) -> 57
, p_2(27) -> 24
, p_2(35) -> 1
, p_2(35) -> 13
, p_2(35) -> 24
, p_2(35) -> 28
, p_2(35) -> 30
, p_2(35) -> 36
, p_2(35) -> 51
, p_2(35) -> 55
, p_2(35) -> 57
, p_2(41) -> 1
, p_2(41) -> 13
, p_2(41) -> 24
, p_2(41) -> 28
, p_2(41) -> 30
, p_2(41) -> 36
, p_2(41) -> 40
, p_2(41) -> 51
, p_2(41) -> 55
, p_2(41) -> 57
, p_2(42) -> 41
, p_2(43) -> 42
, p_2(46) -> 41
, p_2(46) -> 45
, p_2(49) -> 1
, p_2(49) -> 13
, p_2(49) -> 24
, p_2(49) -> 28
, p_2(49) -> 30
, p_2(49) -> 36
, p_2(49) -> 40
, p_2(49) -> 48
, p_2(49) -> 51
, p_2(49) -> 55
, p_2(49) -> 57
, p_2(52) -> 51
, p_2(53) -> 52
, p_2(56) -> 51
, p_2(56) -> 55
, p_2(59) -> 58
, p_2(60) -> 59
, p_2(63) -> 58
, p_2(63) -> 62
, p_2(66) -> 65
, p_2(67) -> 66
, p_2(68) -> 67
, p_2(72) -> 65
, p_2(72) -> 71
, p_3(44) -> 41
, p_3(45) -> 1
, p_3(45) -> 13
, p_3(45) -> 24
, p_3(45) -> 28
, p_3(45) -> 30
, p_3(45) -> 36
, p_3(45) -> 40
, p_3(45) -> 51
, p_3(45) -> 55
, p_3(45) -> 57
, p_3(47) -> 1
, p_3(47) -> 13
, p_3(47) -> 24
, p_3(47) -> 28
, p_3(47) -> 30
, p_3(47) -> 36
, p_3(47) -> 40
, p_3(47) -> 51
, p_3(47) -> 55
, p_3(47) -> 57
, p_3(54) -> 51
, p_3(61) -> 58
, p_3(69) -> 66
, p_3(70) -> 65
, p_3(75) -> 74
, p_3(76) -> 75
, p_3(77) -> 76
, p_3(81) -> 74
, p_3(81) -> 80
, p_4(78) -> 75
, p_4(79) -> 74
, bar_0(2) -> 1
, bar_1(31) -> 24
, bar_1(31) -> 28
, bar_1(31) -> 30
, bar_1(31) -> 51
, bar_1(31) -> 55
, bar_1(31) -> 57
, bar_2(58) -> 51
, bar_2(58) -> 55
, bar_2(58) -> 57}