Tool CaT
stdout:
YES(?,O(n^1))
Problem:
v(s(x1)) -> s(p(p(s(s(s(s(s(s(s(s(w(p(p(s(s(p(s(p(s(x1))))))))))))))))))))
v(0(x1)) -> p(p(s(s(0(p(p(s(s(s(s(s(x1))))))))))))
w(s(x1)) -> s(s(s(s(s(s(p(p(s(s(v(p(p(s(s(s(p(p(s(s(x1))))))))))))))))))))
w(0(x1)) -> p(s(p(p(p(p(p(p(p(p(s(s(0(s(s(s(s(s(s(x1)))))))))))))))))))
p(p(s(x1))) -> p(x1)
p(s(x1)) -> x1
p(0(x1)) -> 0(s(s(s(s(s(s(s(p(s(x1))))))))))
Proof:
Bounds Processor:
bound: 3
enrichment: match
automaton:
final states: {5,4,3}
transitions:
01(70) -> 71*
01(150) -> 151*
01(130) -> 131*
s1(80) -> 81*
s1(65) -> 66*
s1(40) -> 41*
s1(147) -> 148*
s1(132) -> 133*
s1(92) -> 93*
s1(72) -> 73*
s1(67) -> 68*
s1(42) -> 43*
s1(37) -> 38*
s1(32) -> 33*
s1(27) -> 28*
s1(149) -> 150*
s1(144) -> 145*
s1(129) -> 130*
s1(89) -> 90*
s1(84) -> 85*
s1(79) -> 80*
s1(64) -> 65*
s1(39) -> 40*
s1(29) -> 30*
s1(146) -> 147*
s1(141) -> 142*
s1(131) -> 132*
s1(91) -> 92*
s1(71) -> 72*
s1(66) -> 67*
s1(46) -> 47*
s1(41) -> 42*
s1(36) -> 37*
s1(31) -> 32*
s1(148) -> 149*
s1(93) -> 94*
s1(88) -> 89*
s1(78) -> 79*
s1(48) -> 49*
s1(43) -> 44*
s1(38) -> 39*
s1(145) -> 146*
s1(90) -> 91*
s1(85) -> 86*
p1(45) -> 46*
p1(30) -> 31*
p1(142) -> 143*
p1(137) -> 138*
p1(87) -> 88*
p1(82) -> 83*
p1(77) -> 78*
p1(139) -> 140*
p1(134) -> 135*
p1(74) -> 75*
p1(69) -> 70*
p1(44) -> 45*
p1(34) -> 35*
p1(136) -> 137*
p1(86) -> 87*
p1(81) -> 82*
p1(76) -> 77*
p1(138) -> 139*
p1(133) -> 134*
p1(73) -> 74*
p1(68) -> 69*
p1(33) -> 34*
p1(28) -> 29*
p1(140) -> 141*
p1(135) -> 136*
v1(83) -> 84*
w1(35) -> 36*
p2(202) -> 203*
p2(197) -> 198*
p2(192) -> 193*
p2(172) -> 173*
p2(162) -> 163*
p2(269) -> 270*
p2(239) -> 240*
p2(214) -> 215*
p2(199) -> 200*
p2(164) -> 165*
p2(291) -> 292*
p2(186) -> 187*
p2(313) -> 314*
p2(213) -> 214*
p2(203) -> 204*
p2(188) -> 189*
p2(178) -> 179*
p2(335) -> 336*
p2(180) -> 181*
p2(170) -> 171*
p2(357) -> 358*
v0(2) -> 3*
v0(1) -> 3*
02(277) -> 278*
02(247) -> 248*
02(299) -> 300*
02(321) -> 322*
02(343) -> 344*
02(365) -> 366*
s0(2) -> 1*
s0(1) -> 1*
s2(272) -> 273*
s2(242) -> 243*
s2(212) -> 213*
s2(207) -> 208*
s2(364) -> 365*
s2(359) -> 360*
s2(339) -> 340*
s2(334) -> 335*
s2(319) -> 320*
s2(314) -> 315*
s2(294) -> 295*
s2(274) -> 275*
s2(244) -> 245*
s2(209) -> 210*
s2(361) -> 362*
s2(356) -> 357*
s2(341) -> 342*
s2(336) -> 337*
s2(316) -> 317*
s2(296) -> 297*
s2(276) -> 277*
s2(271) -> 272*
s2(246) -> 247*
s2(241) -> 242*
s2(211) -> 212*
s2(206) -> 207*
s2(201) -> 202*
s2(196) -> 197*
s2(363) -> 364*
s2(358) -> 359*
s2(338) -> 339*
s2(318) -> 319*
s2(298) -> 299*
s2(293) -> 294*
s2(273) -> 274*
s2(268) -> 269*
s2(243) -> 244*
s2(238) -> 239*
s2(208) -> 209*
s2(198) -> 199*
s2(360) -> 361*
s2(340) -> 341*
s2(320) -> 321*
s2(315) -> 316*
s2(295) -> 296*
s2(290) -> 291*
s2(275) -> 276*
s2(270) -> 271*
s2(245) -> 246*
s2(240) -> 241*
s2(215) -> 216*
s2(210) -> 211*
s2(205) -> 206*
s2(200) -> 201*
s2(362) -> 363*
s2(342) -> 343*
s2(337) -> 338*
s2(317) -> 318*
s2(312) -> 313*
s2(297) -> 298*
s2(292) -> 293*
p0(2) -> 5*
p0(1) -> 5*
w2(204) -> 205*
w0(2) -> 4*
w0(1) -> 4*
p3(262) -> 263*
p3(260) -> 261*
00(2) -> 2*
00(1) -> 2*
1 -> 5,48
2 -> 5,27
27 -> 165,78,29
28 -> 64*
29 -> 31*
30 -> 144*
31 -> 179*
32 -> 34,178
42 -> 189,46
43 -> 45,188
47 -> 3*
48 -> 165,78,29
49 -> 28*
64 -> 77,164
65 -> 76*
66 -> 173,70
67 -> 69,172
68 -> 129*
71 -> 171*
72 -> 74,170
75 -> 3*
78 -> 196*
79 -> 187*
80 -> 82,186
84 -> 163*
85 -> 87,162
94 -> 205,36,4
130 -> 238*
131 -> 181,135,192
132 -> 134,180
141 -> 143*
143 -> 205,36,4
151 -> 5*
163 -> 88*
165 -> 78*
171 -> 75*
173 -> 70*
179 -> 35*
181 -> 135*
187 -> 83*
189 -> 46*
193 -> 136*
196 -> 198*
198 -> 200*
200 -> 261*
201 -> 203,260
211 -> 263,215
212 -> 214,262
216 -> 84,163,88
238 -> 240*
247 -> 268*
248 -> 193,136
261 -> 204*
263 -> 215*
268 -> 270*
277 -> 290*
278 -> 137*
290 -> 292*
299 -> 312*
300 -> 138*
312 -> 314*
321 -> 334*
322 -> 139*
334 -> 336*
343 -> 356*
344 -> 140*
356 -> 358*
366 -> 141*
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:
{ v(s(x1)) ->
s(p(p(s(s(s(s(s(s(s(s(w(p(p(s(s(p(s(p(s(x1))))))))))))))))))))
, v(0(x1)) -> p(p(s(s(0(p(p(s(s(s(s(s(x1))))))))))))
, w(s(x1)) ->
s(s(s(s(s(s(p(p(s(s(v(p(p(s(s(s(p(p(s(s(x1))))))))))))))))))))
, w(0(x1)) ->
p(s(p(p(p(p(p(p(p(p(s(s(0(s(s(s(s(s(s(x1)))))))))))))))))))
, p(p(s(x1))) -> p(x1)
, p(s(x1)) -> x1
, p(0(x1)) -> 0(s(s(s(s(s(s(s(p(s(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:
{ v(s(x1)) ->
s(p(p(s(s(s(s(s(s(s(s(w(p(p(s(s(p(s(p(s(x1))))))))))))))))))))
, v(0(x1)) -> p(p(s(s(0(p(p(s(s(s(s(s(x1))))))))))))
, w(s(x1)) ->
s(s(s(s(s(s(p(p(s(s(v(p(p(s(s(s(p(p(s(s(x1))))))))))))))))))))
, w(0(x1)) ->
p(s(p(p(p(p(p(p(p(p(s(s(0(s(s(s(s(s(s(x1)))))))))))))))))))
, p(p(s(x1))) -> p(x1)
, p(s(x1)) -> x1
, p(0(x1)) -> 0(s(s(s(s(s(s(s(p(s(x1))))))))))}
Proof Output:
The problem is match-bounded by 3.
The enriched problem is compatible with the following automaton:
{ v_0(2) -> 1
, v_0(5) -> 1
, v_1(45) -> 40
, v_1(45) -> 44
, s_0(2) -> 2
, s_0(2) -> 3
, s_0(2) -> 17
, s_0(2) -> 21
, s_0(2) -> 23
, s_0(2) -> 50
, s_0(2) -> 89
, s_0(2) -> 93
, s_0(2) -> 95
, s_0(5) -> 2
, s_0(5) -> 3
, s_0(5) -> 17
, s_0(5) -> 21
, s_0(5) -> 23
, s_0(5) -> 50
, s_0(5) -> 89
, s_0(5) -> 93
, s_0(5) -> 95
, s_1(2) -> 24
, s_1(2) -> 51
, s_1(5) -> 24
, s_1(5) -> 51
, s_1(6) -> 1
, s_1(9) -> 8
, s_1(10) -> 7
, s_1(10) -> 9
, s_1(11) -> 6
, s_1(11) -> 10
, s_1(12) -> 11
, s_1(13) -> 12
, s_1(14) -> 13
, s_1(15) -> 14
, s_1(16) -> 15
, s_1(20) -> 19
, s_1(21) -> 18
, s_1(21) -> 20
, s_1(23) -> 22
, s_1(24) -> 34
, s_1(27) -> 26
, s_1(28) -> 25
, s_1(28) -> 27
, s_1(31) -> 64
, s_1(31) -> 76
, s_1(32) -> 31
, s_1(33) -> 30
, s_1(33) -> 32
, s_1(34) -> 29
, s_1(34) -> 33
, s_1(35) -> 4
, s_1(35) -> 16
, s_1(35) -> 88
, s_1(36) -> 35
, s_1(37) -> 36
, s_1(38) -> 37
, s_1(39) -> 38
, s_1(40) -> 39
, s_1(43) -> 42
, s_1(44) -> 41
, s_1(44) -> 43
, s_1(47) -> 68
, s_1(48) -> 47
, s_1(49) -> 46
, s_1(49) -> 48
, s_1(50) -> 45
, s_1(50) -> 49
, s_1(53) -> 52
, s_1(62) -> 61
, s_1(63) -> 60
, s_1(63) -> 62
, s_1(66) -> 65
, s_1(67) -> 66
, s_1(68) -> 67
, s_2(50) -> 96
, s_2(64) -> 77
, s_2(69) -> 105
, s_2(70) -> 69
, s_2(70) -> 104
, s_2(71) -> 70
, s_2(72) -> 71
, s_2(73) -> 72
, s_2(74) -> 73
, s_2(75) -> 74
, s_2(76) -> 75
, s_2(78) -> 40
, s_2(78) -> 44
, s_2(81) -> 80
, s_2(82) -> 79
, s_2(82) -> 81
, s_2(83) -> 78
, s_2(83) -> 82
, s_2(84) -> 83
, s_2(85) -> 84
, s_2(86) -> 85
, s_2(87) -> 86
, s_2(88) -> 87
, s_2(92) -> 91
, s_2(93) -> 90
, s_2(93) -> 92
, s_2(95) -> 94
, s_2(97) -> 114
, s_2(98) -> 97
, s_2(98) -> 113
, s_2(99) -> 98
, s_2(100) -> 99
, s_2(101) -> 100
, s_2(102) -> 101
, s_2(103) -> 102
, s_2(104) -> 103
, s_2(106) -> 123
, s_2(107) -> 106
, s_2(107) -> 122
, s_2(108) -> 107
, s_2(109) -> 108
, s_2(110) -> 109
, s_2(111) -> 110
, s_2(112) -> 111
, s_2(113) -> 112
, s_2(115) -> 132
, s_2(116) -> 115
, s_2(116) -> 131
, s_2(117) -> 116
, s_2(118) -> 117
, s_2(119) -> 118
, s_2(120) -> 119
, s_2(121) -> 120
, s_2(122) -> 121
, s_2(124) -> 141
, s_2(125) -> 124
, s_2(125) -> 140
, s_2(126) -> 125
, s_2(127) -> 126
, s_2(128) -> 127
, s_2(129) -> 128
, s_2(130) -> 129
, s_2(131) -> 130
, s_2(134) -> 133
, s_2(135) -> 134
, s_2(136) -> 135
, s_2(137) -> 136
, s_2(138) -> 137
, s_2(139) -> 138
, s_2(140) -> 139
, p_0(2) -> 3
, p_0(5) -> 3
, p_1(7) -> 6
, p_1(8) -> 7
, p_1(18) -> 17
, p_1(19) -> 18
, p_1(22) -> 17
, p_1(22) -> 21
, p_1(24) -> 17
, p_1(24) -> 21
, p_1(24) -> 23
, p_1(25) -> 1
, p_1(26) -> 25
, p_1(30) -> 29
, p_1(31) -> 30
, p_1(34) -> 51
, p_1(41) -> 40
, p_1(42) -> 41
, p_1(46) -> 45
, p_1(47) -> 46
, p_1(51) -> 50
, p_1(51) -> 89
, p_1(51) -> 93
, p_1(51) -> 95
, p_1(52) -> 4
, p_1(52) -> 16
, p_1(52) -> 88
, p_1(54) -> 4
, p_1(54) -> 16
, p_1(54) -> 53
, p_1(54) -> 88
, p_1(55) -> 54
, p_1(56) -> 55
, p_1(57) -> 56
, p_1(58) -> 57
, p_1(59) -> 58
, p_1(60) -> 59
, p_1(61) -> 60
, p_2(9) -> 6
, p_2(20) -> 17
, p_2(24) -> 50
, p_2(24) -> 89
, p_2(24) -> 93
, p_2(24) -> 95
, p_2(27) -> 1
, p_2(32) -> 29
, p_2(43) -> 40
, p_2(48) -> 45
, p_2(62) -> 59
, p_2(63) -> 58
, p_2(77) -> 76
, p_2(79) -> 78
, p_2(80) -> 79
, p_2(90) -> 89
, p_2(91) -> 90
, p_2(94) -> 89
, p_2(94) -> 93
, p_2(96) -> 89
, p_2(96) -> 93
, p_2(96) -> 95
, p_2(105) -> 104
, p_2(114) -> 113
, p_2(123) -> 122
, p_2(132) -> 131
, p_2(141) -> 140
, p_3(81) -> 78
, p_3(92) -> 89
, w_0(2) -> 4
, w_0(5) -> 4
, w_1(17) -> 16
, w_2(89) -> 88
, 0_0(2) -> 3
, 0_0(2) -> 5
, 0_0(2) -> 17
, 0_0(2) -> 21
, 0_0(2) -> 23
, 0_0(2) -> 50
, 0_0(2) -> 89
, 0_0(2) -> 93
, 0_0(2) -> 95
, 0_0(5) -> 3
, 0_0(5) -> 5
, 0_0(5) -> 17
, 0_0(5) -> 21
, 0_0(5) -> 23
, 0_0(5) -> 50
, 0_0(5) -> 89
, 0_0(5) -> 93
, 0_0(5) -> 95
, 0_1(29) -> 1
, 0_1(29) -> 28
, 0_1(64) -> 59
, 0_1(64) -> 63
, 0_1(65) -> 3
, 0_2(69) -> 58
, 0_2(97) -> 57
, 0_2(106) -> 56
, 0_2(115) -> 55
, 0_2(124) -> 54
, 0_2(133) -> 4
, 0_2(133) -> 16
, 0_2(133) -> 53
, 0_2(133) -> 88}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:
{ v(s(x1)) ->
s(p(p(s(s(s(s(s(s(s(s(w(p(p(s(s(p(s(p(s(x1))))))))))))))))))))
, v(0(x1)) -> p(p(s(s(0(p(p(s(s(s(s(s(x1))))))))))))
, w(s(x1)) ->
s(s(s(s(s(s(p(p(s(s(v(p(p(s(s(s(p(p(s(s(x1))))))))))))))))))))
, w(0(x1)) ->
p(s(p(p(p(p(p(p(p(p(s(s(0(s(s(s(s(s(s(x1)))))))))))))))))))
, p(p(s(x1))) -> p(x1)
, p(s(x1)) -> x1
, p(0(x1)) -> 0(s(s(s(s(s(s(s(p(s(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:
{ v(s(x1)) ->
s(p(p(s(s(s(s(s(s(s(s(w(p(p(s(s(p(s(p(s(x1))))))))))))))))))))
, v(0(x1)) -> p(p(s(s(0(p(p(s(s(s(s(s(x1))))))))))))
, w(s(x1)) ->
s(s(s(s(s(s(p(p(s(s(v(p(p(s(s(s(p(p(s(s(x1))))))))))))))))))))
, w(0(x1)) ->
p(s(p(p(p(p(p(p(p(p(s(s(0(s(s(s(s(s(s(x1)))))))))))))))))))
, p(p(s(x1))) -> p(x1)
, p(s(x1)) -> x1
, p(0(x1)) -> 0(s(s(s(s(s(s(s(p(s(x1))))))))))}
Proof Output:
The problem is match-bounded by 3.
The enriched problem is compatible with the following automaton:
{ v_0(2) -> 1
, v_0(5) -> 1
, v_1(45) -> 40
, v_1(45) -> 44
, s_0(2) -> 2
, s_0(2) -> 3
, s_0(2) -> 17
, s_0(2) -> 21
, s_0(2) -> 23
, s_0(2) -> 50
, s_0(2) -> 89
, s_0(2) -> 93
, s_0(2) -> 95
, s_0(5) -> 2
, s_0(5) -> 3
, s_0(5) -> 17
, s_0(5) -> 21
, s_0(5) -> 23
, s_0(5) -> 50
, s_0(5) -> 89
, s_0(5) -> 93
, s_0(5) -> 95
, s_1(2) -> 24
, s_1(2) -> 51
, s_1(5) -> 24
, s_1(5) -> 51
, s_1(6) -> 1
, s_1(9) -> 8
, s_1(10) -> 7
, s_1(10) -> 9
, s_1(11) -> 6
, s_1(11) -> 10
, s_1(12) -> 11
, s_1(13) -> 12
, s_1(14) -> 13
, s_1(15) -> 14
, s_1(16) -> 15
, s_1(20) -> 19
, s_1(21) -> 18
, s_1(21) -> 20
, s_1(23) -> 22
, s_1(24) -> 34
, s_1(27) -> 26
, s_1(28) -> 25
, s_1(28) -> 27
, s_1(31) -> 64
, s_1(31) -> 76
, s_1(32) -> 31
, s_1(33) -> 30
, s_1(33) -> 32
, s_1(34) -> 29
, s_1(34) -> 33
, s_1(35) -> 4
, s_1(35) -> 16
, s_1(35) -> 88
, s_1(36) -> 35
, s_1(37) -> 36
, s_1(38) -> 37
, s_1(39) -> 38
, s_1(40) -> 39
, s_1(43) -> 42
, s_1(44) -> 41
, s_1(44) -> 43
, s_1(47) -> 68
, s_1(48) -> 47
, s_1(49) -> 46
, s_1(49) -> 48
, s_1(50) -> 45
, s_1(50) -> 49
, s_1(53) -> 52
, s_1(62) -> 61
, s_1(63) -> 60
, s_1(63) -> 62
, s_1(66) -> 65
, s_1(67) -> 66
, s_1(68) -> 67
, s_2(50) -> 96
, s_2(64) -> 77
, s_2(69) -> 105
, s_2(70) -> 69
, s_2(70) -> 104
, s_2(71) -> 70
, s_2(72) -> 71
, s_2(73) -> 72
, s_2(74) -> 73
, s_2(75) -> 74
, s_2(76) -> 75
, s_2(78) -> 40
, s_2(78) -> 44
, s_2(81) -> 80
, s_2(82) -> 79
, s_2(82) -> 81
, s_2(83) -> 78
, s_2(83) -> 82
, s_2(84) -> 83
, s_2(85) -> 84
, s_2(86) -> 85
, s_2(87) -> 86
, s_2(88) -> 87
, s_2(92) -> 91
, s_2(93) -> 90
, s_2(93) -> 92
, s_2(95) -> 94
, s_2(97) -> 114
, s_2(98) -> 97
, s_2(98) -> 113
, s_2(99) -> 98
, s_2(100) -> 99
, s_2(101) -> 100
, s_2(102) -> 101
, s_2(103) -> 102
, s_2(104) -> 103
, s_2(106) -> 123
, s_2(107) -> 106
, s_2(107) -> 122
, s_2(108) -> 107
, s_2(109) -> 108
, s_2(110) -> 109
, s_2(111) -> 110
, s_2(112) -> 111
, s_2(113) -> 112
, s_2(115) -> 132
, s_2(116) -> 115
, s_2(116) -> 131
, s_2(117) -> 116
, s_2(118) -> 117
, s_2(119) -> 118
, s_2(120) -> 119
, s_2(121) -> 120
, s_2(122) -> 121
, s_2(124) -> 141
, s_2(125) -> 124
, s_2(125) -> 140
, s_2(126) -> 125
, s_2(127) -> 126
, s_2(128) -> 127
, s_2(129) -> 128
, s_2(130) -> 129
, s_2(131) -> 130
, s_2(134) -> 133
, s_2(135) -> 134
, s_2(136) -> 135
, s_2(137) -> 136
, s_2(138) -> 137
, s_2(139) -> 138
, s_2(140) -> 139
, p_0(2) -> 3
, p_0(5) -> 3
, p_1(7) -> 6
, p_1(8) -> 7
, p_1(18) -> 17
, p_1(19) -> 18
, p_1(22) -> 17
, p_1(22) -> 21
, p_1(24) -> 17
, p_1(24) -> 21
, p_1(24) -> 23
, p_1(25) -> 1
, p_1(26) -> 25
, p_1(30) -> 29
, p_1(31) -> 30
, p_1(34) -> 51
, p_1(41) -> 40
, p_1(42) -> 41
, p_1(46) -> 45
, p_1(47) -> 46
, p_1(51) -> 50
, p_1(51) -> 89
, p_1(51) -> 93
, p_1(51) -> 95
, p_1(52) -> 4
, p_1(52) -> 16
, p_1(52) -> 88
, p_1(54) -> 4
, p_1(54) -> 16
, p_1(54) -> 53
, p_1(54) -> 88
, p_1(55) -> 54
, p_1(56) -> 55
, p_1(57) -> 56
, p_1(58) -> 57
, p_1(59) -> 58
, p_1(60) -> 59
, p_1(61) -> 60
, p_2(9) -> 6
, p_2(20) -> 17
, p_2(24) -> 50
, p_2(24) -> 89
, p_2(24) -> 93
, p_2(24) -> 95
, p_2(27) -> 1
, p_2(32) -> 29
, p_2(43) -> 40
, p_2(48) -> 45
, p_2(62) -> 59
, p_2(63) -> 58
, p_2(77) -> 76
, p_2(79) -> 78
, p_2(80) -> 79
, p_2(90) -> 89
, p_2(91) -> 90
, p_2(94) -> 89
, p_2(94) -> 93
, p_2(96) -> 89
, p_2(96) -> 93
, p_2(96) -> 95
, p_2(105) -> 104
, p_2(114) -> 113
, p_2(123) -> 122
, p_2(132) -> 131
, p_2(141) -> 140
, p_3(81) -> 78
, p_3(92) -> 89
, w_0(2) -> 4
, w_0(5) -> 4
, w_1(17) -> 16
, w_2(89) -> 88
, 0_0(2) -> 3
, 0_0(2) -> 5
, 0_0(2) -> 17
, 0_0(2) -> 21
, 0_0(2) -> 23
, 0_0(2) -> 50
, 0_0(2) -> 89
, 0_0(2) -> 93
, 0_0(2) -> 95
, 0_0(5) -> 3
, 0_0(5) -> 5
, 0_0(5) -> 17
, 0_0(5) -> 21
, 0_0(5) -> 23
, 0_0(5) -> 50
, 0_0(5) -> 89
, 0_0(5) -> 93
, 0_0(5) -> 95
, 0_1(29) -> 1
, 0_1(29) -> 28
, 0_1(64) -> 59
, 0_1(64) -> 63
, 0_1(65) -> 3
, 0_2(69) -> 58
, 0_2(97) -> 57
, 0_2(106) -> 56
, 0_2(115) -> 55
, 0_2(124) -> 54
, 0_2(133) -> 4
, 0_2(133) -> 16
, 0_2(133) -> 53
, 0_2(133) -> 88}