Tool CaT
stdout:
YES(?,O(n^1))
Problem:
p(0(x1)) -> 0(s(s(p(x1))))
p(s(x1)) -> x1
p(p(s(x1))) -> p(x1)
f(s(x1)) -> p(s(g(p(s(s(x1))))))
g(s(x1)) -> p(p(s(s(s(j(s(p(s(p(s(x1)))))))))))
j(s(x1)) -> p(s(s(p(s(f(p(s(p(p(s(x1)))))))))))
half(0(x1)) -> 0(s(s(half(p(s(p(s(x1))))))))
half(s(s(x1))) -> s(half(p(p(s(s(x1))))))
rd(0(x1)) -> 0(s(0(0(0(0(s(0(rd(x1)))))))))
Proof:
Bounds Processor:
bound: 4
enrichment: match
automaton:
final states: {8,7,6,5,4,3}
transitions:
01(107) -> 108*
01(102) -> 103*
01(12) -> 13*
01(109) -> 110*
01(104) -> 105*
01(106) -> 107*
01(86) -> 87*
01(105) -> 106*
s1(85) -> 86*
s1(80) -> 81*
s1(10) -> 11*
s1(77) -> 78*
s1(47) -> 48*
s1(42) -> 43*
s1(27) -> 28*
s1(99) -> 100*
s1(84) -> 85*
s1(79) -> 80*
s1(74) -> 75*
s1(44) -> 45*
s1(39) -> 40*
s1(24) -> 25*
s1(46) -> 47*
s1(11) -> 12*
s1(108) -> 109*
s1(103) -> 104*
s1(48) -> 49*
s1(23) -> 24*
rd1(101) -> 102*
rd1(123) -> 124*
half1(98) -> 99*
half1(83) -> 84*
p1(75) -> 76*
p1(50) -> 51*
p1(25) -> 26*
p1(97) -> 98*
p1(49) -> 50*
p1(9) -> 10*
p1(81) -> 82*
p1(41) -> 42*
p1(21) -> 22*
p1(78) -> 79*
p1(73) -> 74*
p1(43) -> 44*
p1(28) -> 29*
f1(76) -> 77*
j1(45) -> 46*
g1(26) -> 27*
p2(187) -> 188*
p2(157) -> 158*
p2(154) -> 155*
p2(149) -> 150*
p2(186) -> 187*
p2(151) -> 152*
p2(163) -> 164*
p2(133) -> 134*
p2(180) -> 181*
p2(160) -> 161*
p2(155) -> 156*
p2(135) -> 136*
p0(2) -> 3*
p0(1) -> 3*
s2(162) -> 163*
s2(184) -> 185*
s2(179) -> 180*
s2(159) -> 160*
s2(181) -> 182*
s2(161) -> 162*
s2(156) -> 157*
s2(183) -> 184*
s2(153) -> 154*
s2(185) -> 186*
00(2) -> 1*
00(1) -> 1*
f2(158) -> 159*
s0(2) -> 2*
s0(1) -> 2*
j2(182) -> 183*
f0(2) -> 4*
f0(1) -> 4*
p3(212) -> 213*
p3(207) -> 208*
p3(177) -> 178*
p3(209) -> 210*
p3(206) -> 207*
p3(191) -> 192*
p3(215) -> 216*
g0(2) -> 5*
g0(1) -> 5*
s3(214) -> 215*
s3(211) -> 212*
s3(213) -> 214*
s3(208) -> 209*
s3(205) -> 206*
j0(2) -> 6*
j0(1) -> 6*
f3(210) -> 211*
half0(2) -> 7*
half0(1) -> 7*
p4(217) -> 218*
rd0(2) -> 8*
rd0(1) -> 8*
1 -> 218,208,178,156,150,74,10,123,39,3,21
2 -> 218,208,178,156,150,74,10,101,23,3,9
13 -> 218,208,178,156,136,74,22,10,3
22 -> 10*
23 -> 152,149,42,73
24 -> 151,26,97,41
26 -> 97*
27 -> 29*
29 -> 211,213,159,161,77,79,4
39 -> 152,135,42,73
40 -> 24*
42 -> 44,73
44 -> 153,83
47 -> 134,51,5
48 -> 133,50
51 -> 5*
74 -> 76*
77 -> 79*
80 -> 82,6
82 -> 6*
87 -> 99,84,7
100 -> 99,84,7
110 -> 124,102,8
124 -> 102*
134 -> 51,5
136 -> 74*
150 -> 74*
152 -> 98*
153 -> 177,155
155 -> 179*
156 -> 158*
159 -> 161*
162 -> 164*
164 -> 46*
178 -> 156*
179 -> 181*
181 -> 205*
184 -> 192,188
185 -> 191,187
188 -> 27,29,4
192 -> 188*
205 -> 217,207
208 -> 210*
211 -> 213*
214 -> 216,183
216 -> 183*
218 -> 208*
problem:
QedTool 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:
{ p(0(x1)) -> 0(s(s(p(x1))))
, p(s(x1)) -> x1
, p(p(s(x1))) -> p(x1)
, f(s(x1)) -> p(s(g(p(s(s(x1))))))
, g(s(x1)) -> p(p(s(s(s(j(s(p(s(p(s(x1)))))))))))
, j(s(x1)) -> p(s(s(p(s(f(p(s(p(p(s(x1)))))))))))
, half(0(x1)) -> 0(s(s(half(p(s(p(s(x1))))))))
, half(s(s(x1))) -> s(half(p(p(s(s(x1))))))
, rd(0(x1)) -> 0(s(0(0(0(0(s(0(rd(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:
{ p(0(x1)) -> 0(s(s(p(x1))))
, p(s(x1)) -> x1
, p(p(s(x1))) -> p(x1)
, f(s(x1)) -> p(s(g(p(s(s(x1))))))
, g(s(x1)) -> p(p(s(s(s(j(s(p(s(p(s(x1)))))))))))
, j(s(x1)) -> p(s(s(p(s(f(p(s(p(p(s(x1)))))))))))
, half(0(x1)) -> 0(s(s(half(p(s(p(s(x1))))))))
, half(s(s(x1))) -> s(half(p(p(s(s(x1))))))
, rd(0(x1)) -> 0(s(0(0(0(0(s(0(rd(x1)))))))))}
Proof Output:
The problem is match-bounded by 4.
The enriched problem is compatible with the following automaton:
{ p_0(2) -> 1
, p_0(3) -> 1
, p_1(2) -> 11
, p_1(3) -> 11
, p_1(12) -> 4
, p_1(12) -> 28
, p_1(12) -> 30
, p_1(12) -> 36
, p_1(12) -> 38
, p_1(12) -> 69
, p_1(12) -> 71
, p_1(14) -> 48
, p_1(15) -> 14
, p_1(16) -> 23
, p_1(16) -> 25
, p_1(16) -> 42
, p_1(17) -> 5
, p_1(18) -> 17
, p_1(24) -> 23
, p_1(24) -> 42
, p_1(25) -> 31
, p_1(25) -> 33
, p_1(26) -> 6
, p_1(29) -> 28
, p_1(29) -> 69
, p_1(29) -> 71
, p_1(32) -> 31
, p_2(2) -> 31
, p_2(2) -> 33
, p_2(2) -> 39
, p_2(2) -> 41
, p_2(3) -> 31
, p_2(3) -> 33
, p_2(3) -> 39
, p_2(3) -> 41
, p_2(16) -> 48
, p_2(19) -> 5
, p_2(25) -> 39
, p_2(25) -> 41
, p_2(34) -> 21
, p_2(37) -> 36
, p_2(40) -> 39
, p_2(42) -> 39
, p_2(42) -> 41
, p_2(43) -> 42
, p_2(57) -> 4
, p_2(57) -> 13
, p_2(57) -> 28
, p_2(57) -> 30
, p_2(57) -> 36
, p_2(57) -> 38
, p_2(57) -> 69
, p_2(57) -> 71
, p_2(58) -> 57
, p_2(64) -> 63
, p_2(64) -> 75
, p_2(66) -> 63
, p_2(66) -> 65
, p_2(66) -> 75
, p_3(2) -> 72
, p_3(2) -> 74
, p_3(3) -> 72
, p_3(3) -> 74
, p_3(23) -> 39
, p_3(23) -> 41
, p_3(59) -> 4
, p_3(59) -> 13
, p_3(59) -> 28
, p_3(59) -> 30
, p_3(59) -> 36
, p_3(59) -> 38
, p_3(59) -> 69
, p_3(59) -> 71
, p_3(65) -> 72
, p_3(65) -> 74
, p_3(67) -> 61
, p_3(70) -> 69
, p_3(73) -> 72
, p_3(75) -> 72
, p_3(75) -> 74
, p_3(76) -> 75
, p_4(63) -> 72
, p_4(63) -> 74
, 0_0(2) -> 1
, 0_0(2) -> 2
, 0_0(2) -> 11
, 0_0(2) -> 23
, 0_0(2) -> 25
, 0_0(2) -> 31
, 0_0(2) -> 33
, 0_0(2) -> 39
, 0_0(2) -> 41
, 0_0(2) -> 42
, 0_0(2) -> 48
, 0_0(2) -> 63
, 0_0(2) -> 65
, 0_0(2) -> 72
, 0_0(2) -> 74
, 0_0(2) -> 75
, 0_0(3) -> 1
, 0_0(3) -> 2
, 0_0(3) -> 11
, 0_0(3) -> 23
, 0_0(3) -> 25
, 0_0(3) -> 31
, 0_0(3) -> 33
, 0_0(3) -> 39
, 0_0(3) -> 41
, 0_0(3) -> 42
, 0_0(3) -> 48
, 0_0(3) -> 63
, 0_0(3) -> 65
, 0_0(3) -> 72
, 0_0(3) -> 74
, 0_0(3) -> 75
, 0_1(9) -> 1
, 0_1(9) -> 11
, 0_1(9) -> 31
, 0_1(9) -> 33
, 0_1(9) -> 39
, 0_1(9) -> 41
, 0_1(9) -> 72
, 0_1(9) -> 74
, 0_1(44) -> 7
, 0_1(44) -> 46
, 0_1(44) -> 47
, 0_1(49) -> 8
, 0_1(49) -> 56
, 0_1(51) -> 50
, 0_1(52) -> 51
, 0_1(53) -> 52
, 0_1(54) -> 53
, 0_1(56) -> 55
, s_0(2) -> 1
, s_0(2) -> 3
, s_0(2) -> 11
, s_0(2) -> 23
, s_0(2) -> 25
, s_0(2) -> 31
, s_0(2) -> 33
, s_0(2) -> 39
, s_0(2) -> 41
, s_0(2) -> 42
, s_0(2) -> 48
, s_0(2) -> 63
, s_0(2) -> 65
, s_0(2) -> 72
, s_0(2) -> 74
, s_0(2) -> 75
, s_0(3) -> 1
, s_0(3) -> 3
, s_0(3) -> 11
, s_0(3) -> 23
, s_0(3) -> 25
, s_0(3) -> 31
, s_0(3) -> 33
, s_0(3) -> 39
, s_0(3) -> 41
, s_0(3) -> 42
, s_0(3) -> 48
, s_0(3) -> 63
, s_0(3) -> 65
, s_0(3) -> 72
, s_0(3) -> 74
, s_0(3) -> 75
, s_1(2) -> 14
, s_1(2) -> 16
, s_1(3) -> 14
, s_1(3) -> 16
, s_1(10) -> 9
, s_1(11) -> 10
, s_1(13) -> 12
, s_1(16) -> 15
, s_1(19) -> 18
, s_1(20) -> 17
, s_1(20) -> 19
, s_1(21) -> 5
, s_1(21) -> 20
, s_1(23) -> 22
, s_1(25) -> 24
, s_1(27) -> 26
, s_1(28) -> 6
, s_1(28) -> 27
, s_1(30) -> 29
, s_1(33) -> 32
, s_1(45) -> 44
, s_1(46) -> 45
, s_1(47) -> 7
, s_1(47) -> 46
, s_1(47) -> 47
, s_1(50) -> 49
, s_1(55) -> 54
, s_2(2) -> 66
, s_2(3) -> 66
, s_2(23) -> 43
, s_2(35) -> 34
, s_2(36) -> 21
, s_2(36) -> 35
, s_2(38) -> 37
, s_2(41) -> 40
, s_2(59) -> 58
, s_2(60) -> 57
, s_2(60) -> 59
, s_2(61) -> 4
, s_2(61) -> 13
, s_2(61) -> 28
, s_2(61) -> 30
, s_2(61) -> 36
, s_2(61) -> 38
, s_2(61) -> 60
, s_2(61) -> 69
, s_2(61) -> 71
, s_2(63) -> 62
, s_2(65) -> 64
, s_3(63) -> 76
, s_3(68) -> 67
, s_3(69) -> 61
, s_3(69) -> 68
, s_3(71) -> 70
, s_3(74) -> 73
, f_0(2) -> 4
, f_0(3) -> 4
, f_1(31) -> 28
, f_1(31) -> 30
, f_1(31) -> 69
, f_1(31) -> 71
, f_2(39) -> 36
, f_2(39) -> 38
, f_3(72) -> 69
, f_3(72) -> 71
, g_0(2) -> 5
, g_0(3) -> 5
, g_1(14) -> 4
, g_1(14) -> 13
, g_1(14) -> 28
, g_1(14) -> 30
, g_1(14) -> 36
, g_1(14) -> 38
, g_1(14) -> 69
, g_1(14) -> 71
, j_0(2) -> 6
, j_0(3) -> 6
, j_1(22) -> 21
, j_2(62) -> 61
, half_0(2) -> 7
, half_0(3) -> 7
, half_1(23) -> 46
, half_1(48) -> 47
, rd_0(2) -> 8
, rd_0(3) -> 8
, rd_1(2) -> 56
, rd_1(3) -> 56}Tool RC1
stdout:
YES(?,O(n^1))
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:
{ p(0(x1)) -> 0(s(s(p(x1))))
, p(s(x1)) -> x1
, p(p(s(x1))) -> p(x1)
, f(s(x1)) -> p(s(g(p(s(s(x1))))))
, g(s(x1)) -> p(p(s(s(s(j(s(p(s(p(s(x1)))))))))))
, j(s(x1)) -> p(s(s(p(s(f(p(s(p(p(s(x1)))))))))))
, half(0(x1)) -> 0(s(s(half(p(s(p(s(x1))))))))
, half(s(s(x1))) -> s(half(p(p(s(s(x1))))))
, rd(0(x1)) -> 0(s(0(0(0(0(s(0(rd(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:
{ p(0(x1)) -> 0(s(s(p(x1))))
, p(s(x1)) -> x1
, p(p(s(x1))) -> p(x1)
, f(s(x1)) -> p(s(g(p(s(s(x1))))))
, g(s(x1)) -> p(p(s(s(s(j(s(p(s(p(s(x1)))))))))))
, j(s(x1)) -> p(s(s(p(s(f(p(s(p(p(s(x1)))))))))))
, half(0(x1)) -> 0(s(s(half(p(s(p(s(x1))))))))
, half(s(s(x1))) -> s(half(p(p(s(s(x1))))))
, rd(0(x1)) -> 0(s(0(0(0(0(s(0(rd(x1)))))))))}
Proof Output:
The problem is match-bounded by 4.
The enriched problem is compatible with the following automaton:
{ p_0(2) -> 1
, p_0(3) -> 1
, p_1(2) -> 11
, p_1(3) -> 11
, p_1(12) -> 4
, p_1(12) -> 28
, p_1(12) -> 30
, p_1(12) -> 36
, p_1(12) -> 38
, p_1(12) -> 69
, p_1(12) -> 71
, p_1(14) -> 48
, p_1(15) -> 14
, p_1(16) -> 23
, p_1(16) -> 25
, p_1(16) -> 42
, p_1(17) -> 5
, p_1(18) -> 17
, p_1(24) -> 23
, p_1(24) -> 42
, p_1(25) -> 31
, p_1(25) -> 33
, p_1(26) -> 6
, p_1(29) -> 28
, p_1(29) -> 69
, p_1(29) -> 71
, p_1(32) -> 31
, p_2(2) -> 31
, p_2(2) -> 33
, p_2(2) -> 39
, p_2(2) -> 41
, p_2(3) -> 31
, p_2(3) -> 33
, p_2(3) -> 39
, p_2(3) -> 41
, p_2(16) -> 48
, p_2(19) -> 5
, p_2(25) -> 39
, p_2(25) -> 41
, p_2(34) -> 21
, p_2(37) -> 36
, p_2(40) -> 39
, p_2(42) -> 39
, p_2(42) -> 41
, p_2(43) -> 42
, p_2(57) -> 4
, p_2(57) -> 13
, p_2(57) -> 28
, p_2(57) -> 30
, p_2(57) -> 36
, p_2(57) -> 38
, p_2(57) -> 69
, p_2(57) -> 71
, p_2(58) -> 57
, p_2(64) -> 63
, p_2(64) -> 75
, p_2(66) -> 63
, p_2(66) -> 65
, p_2(66) -> 75
, p_3(2) -> 72
, p_3(2) -> 74
, p_3(3) -> 72
, p_3(3) -> 74
, p_3(23) -> 39
, p_3(23) -> 41
, p_3(59) -> 4
, p_3(59) -> 13
, p_3(59) -> 28
, p_3(59) -> 30
, p_3(59) -> 36
, p_3(59) -> 38
, p_3(59) -> 69
, p_3(59) -> 71
, p_3(65) -> 72
, p_3(65) -> 74
, p_3(67) -> 61
, p_3(70) -> 69
, p_3(73) -> 72
, p_3(75) -> 72
, p_3(75) -> 74
, p_3(76) -> 75
, p_4(63) -> 72
, p_4(63) -> 74
, 0_0(2) -> 1
, 0_0(2) -> 2
, 0_0(2) -> 11
, 0_0(2) -> 23
, 0_0(2) -> 25
, 0_0(2) -> 31
, 0_0(2) -> 33
, 0_0(2) -> 39
, 0_0(2) -> 41
, 0_0(2) -> 42
, 0_0(2) -> 48
, 0_0(2) -> 63
, 0_0(2) -> 65
, 0_0(2) -> 72
, 0_0(2) -> 74
, 0_0(2) -> 75
, 0_0(3) -> 1
, 0_0(3) -> 2
, 0_0(3) -> 11
, 0_0(3) -> 23
, 0_0(3) -> 25
, 0_0(3) -> 31
, 0_0(3) -> 33
, 0_0(3) -> 39
, 0_0(3) -> 41
, 0_0(3) -> 42
, 0_0(3) -> 48
, 0_0(3) -> 63
, 0_0(3) -> 65
, 0_0(3) -> 72
, 0_0(3) -> 74
, 0_0(3) -> 75
, 0_1(9) -> 1
, 0_1(9) -> 11
, 0_1(9) -> 31
, 0_1(9) -> 33
, 0_1(9) -> 39
, 0_1(9) -> 41
, 0_1(9) -> 72
, 0_1(9) -> 74
, 0_1(44) -> 7
, 0_1(44) -> 46
, 0_1(44) -> 47
, 0_1(49) -> 8
, 0_1(49) -> 56
, 0_1(51) -> 50
, 0_1(52) -> 51
, 0_1(53) -> 52
, 0_1(54) -> 53
, 0_1(56) -> 55
, s_0(2) -> 1
, s_0(2) -> 3
, s_0(2) -> 11
, s_0(2) -> 23
, s_0(2) -> 25
, s_0(2) -> 31
, s_0(2) -> 33
, s_0(2) -> 39
, s_0(2) -> 41
, s_0(2) -> 42
, s_0(2) -> 48
, s_0(2) -> 63
, s_0(2) -> 65
, s_0(2) -> 72
, s_0(2) -> 74
, s_0(2) -> 75
, s_0(3) -> 1
, s_0(3) -> 3
, s_0(3) -> 11
, s_0(3) -> 23
, s_0(3) -> 25
, s_0(3) -> 31
, s_0(3) -> 33
, s_0(3) -> 39
, s_0(3) -> 41
, s_0(3) -> 42
, s_0(3) -> 48
, s_0(3) -> 63
, s_0(3) -> 65
, s_0(3) -> 72
, s_0(3) -> 74
, s_0(3) -> 75
, s_1(2) -> 14
, s_1(2) -> 16
, s_1(3) -> 14
, s_1(3) -> 16
, s_1(10) -> 9
, s_1(11) -> 10
, s_1(13) -> 12
, s_1(16) -> 15
, s_1(19) -> 18
, s_1(20) -> 17
, s_1(20) -> 19
, s_1(21) -> 5
, s_1(21) -> 20
, s_1(23) -> 22
, s_1(25) -> 24
, s_1(27) -> 26
, s_1(28) -> 6
, s_1(28) -> 27
, s_1(30) -> 29
, s_1(33) -> 32
, s_1(45) -> 44
, s_1(46) -> 45
, s_1(47) -> 7
, s_1(47) -> 46
, s_1(47) -> 47
, s_1(50) -> 49
, s_1(55) -> 54
, s_2(2) -> 66
, s_2(3) -> 66
, s_2(23) -> 43
, s_2(35) -> 34
, s_2(36) -> 21
, s_2(36) -> 35
, s_2(38) -> 37
, s_2(41) -> 40
, s_2(59) -> 58
, s_2(60) -> 57
, s_2(60) -> 59
, s_2(61) -> 4
, s_2(61) -> 13
, s_2(61) -> 28
, s_2(61) -> 30
, s_2(61) -> 36
, s_2(61) -> 38
, s_2(61) -> 60
, s_2(61) -> 69
, s_2(61) -> 71
, s_2(63) -> 62
, s_2(65) -> 64
, s_3(63) -> 76
, s_3(68) -> 67
, s_3(69) -> 61
, s_3(69) -> 68
, s_3(71) -> 70
, s_3(74) -> 73
, f_0(2) -> 4
, f_0(3) -> 4
, f_1(31) -> 28
, f_1(31) -> 30
, f_1(31) -> 69
, f_1(31) -> 71
, f_2(39) -> 36
, f_2(39) -> 38
, f_3(72) -> 69
, f_3(72) -> 71
, g_0(2) -> 5
, g_0(3) -> 5
, g_1(14) -> 4
, g_1(14) -> 13
, g_1(14) -> 28
, g_1(14) -> 30
, g_1(14) -> 36
, g_1(14) -> 38
, g_1(14) -> 69
, g_1(14) -> 71
, j_0(2) -> 6
, j_0(3) -> 6
, j_1(22) -> 21
, j_2(62) -> 61
, half_0(2) -> 7
, half_0(3) -> 7
, half_1(23) -> 46
, half_1(48) -> 47
, rd_0(2) -> 8
, rd_0(3) -> 8
, rd_1(2) -> 56
, rd_1(3) -> 56}