Tool CaT
stdout:
MAYBE
Problem:
r1(a(x1)) -> a(a(a(r1(x1))))
r2(a(x1)) -> a(a(a(r2(x1))))
a(l1(x1)) -> l1(a(a(a(x1))))
a(a(l2(x1))) -> l2(a(a(x1)))
r1(b(x1)) -> l1(b(x1))
r2(b(x1)) -> l2(a(b(x1)))
b(l1(x1)) -> b(r2(x1))
b(l2(x1)) -> b(r1(x1))
a(a(x1)) -> x1
Proof:
Complexity Transformation Processor:
strict:
r1(a(x1)) -> a(a(a(r1(x1))))
r2(a(x1)) -> a(a(a(r2(x1))))
a(l1(x1)) -> l1(a(a(a(x1))))
a(a(l2(x1))) -> l2(a(a(x1)))
r1(b(x1)) -> l1(b(x1))
r2(b(x1)) -> l2(a(b(x1)))
b(l1(x1)) -> b(r2(x1))
b(l2(x1)) -> b(r1(x1))
a(a(x1)) -> x1
weak:
Bounds Processor:
bound: 0
enrichment: match
automaton:
final states: {6,5,4,3}
transitions:
r10(2) -> 3*
r10(1) -> 3*
a0(82) -> 83*
a0(2) -> 5*
a0(199) -> 200*
a0(29) -> 30*
a0(81) -> 82*
a0(1) -> 5*
a0(163) -> 164*
a0(28) -> 29*
a0(80) -> 81*
r20(2) -> 4*
r20(1) -> 4*
l10(30) -> 31*
l10(2) -> 1*
l10(1) -> 1*
l10(83) -> 84*
l20(2) -> 2*
l20(1) -> 2*
l20(118) -> 119*
b0(42) -> 43*
b0(2) -> 6*
b0(64) -> 65*
b0(1) -> 6*
1 -> 29*
2 -> 81,29
3 -> 64*
4 -> 42*
5 -> 28*
28 -> 200,30
29 -> 81,118
30 -> 80*
31 -> 164,200,5
43 -> 6*
65 -> 6*
80 -> 82*
81 -> 83*
82 -> 164*
83 -> 163*
84 -> 81,29
118 -> 199*
119 -> 81,29
163 -> 29*
164 -> 28*
199 -> 29*
200 -> 28*
problem:
strict:
r1(a(x1)) -> a(a(a(r1(x1))))
r2(a(x1)) -> a(a(a(r2(x1))))
a(l1(x1)) -> l1(a(a(a(x1))))
a(a(l2(x1))) -> l2(a(a(x1)))
r1(b(x1)) -> l1(b(x1))
b(l1(x1)) -> b(r2(x1))
b(l2(x1)) -> b(r1(x1))
a(a(x1)) -> x1
weak:
r2(b(x1)) -> l2(a(b(x1)))
Bounds Processor:
bound: 0
enrichment: match
automaton:
final states: {6,5,4,3}
transitions:
r10(2) -> 3*
r10(1) -> 3*
a0(82) -> 83*
a0(12) -> 13*
a0(2) -> 5*
a0(84) -> 85*
a0(191) -> 192*
a0(141) -> 142*
a0(11) -> 12*
a0(1) -> 5*
a0(83) -> 84*
r20(2) -> 4*
r20(1) -> 4*
l10(2) -> 1*
l10(1) -> 1*
l10(13) -> 14*
l10(85) -> 86*
l20(2) -> 2*
l20(94) -> 95*
l20(1) -> 2*
b0(52) -> 53*
b0(2) -> 6*
b0(46) -> 47*
b0(1) -> 6*
1 -> 12*
2 -> 12*
3 -> 52*
4 -> 46*
5 -> 11*
11 -> 192,13
12 -> 83,94
13 -> 82*
14 -> 142,192,5
47 -> 6*
53 -> 6*
82 -> 142,84
83 -> 85*
84 -> 142*
85 -> 141*
86 -> 83,12
94 -> 191*
95 -> 83,12
141 -> 12*
142 -> 11*
191 -> 12*
192 -> 11*
problem:
strict:
r1(a(x1)) -> a(a(a(r1(x1))))
a(l1(x1)) -> l1(a(a(a(x1))))
a(a(l2(x1))) -> l2(a(a(x1)))
r1(b(x1)) -> l1(b(x1))
b(l1(x1)) -> b(r2(x1))
b(l2(x1)) -> b(r1(x1))
a(a(x1)) -> x1
weak:
r2(a(x1)) -> a(a(a(r2(x1))))
r2(b(x1)) -> l2(a(b(x1)))
Bounds Processor:
bound: 0
enrichment: match
automaton:
final states: {6,5,4,3}
transitions:
r10(2) -> 3*
r10(1) -> 3*
a0(65) -> 66*
a0(20) -> 21*
a0(2) -> 4*
a0(64) -> 65*
a0(66) -> 67*
a0(21) -> 22*
a0(1) -> 4*
a0(133) -> 134*
a0(165) -> 166*
r20(2) -> 6*
r20(1) -> 6*
l10(67) -> 68*
l10(22) -> 23*
l10(2) -> 1*
l10(1) -> 1*
l20(2) -> 2*
l20(1) -> 2*
l20(88) -> 89*
b0(2) -> 5*
b0(34) -> 35*
b0(1) -> 5*
b0(48) -> 49*
1 -> 21*
2 -> 65,21
3 -> 48*
4 -> 20*
6 -> 34*
20 -> 166,134,22
21 -> 65,88
22 -> 64*
23 -> 134,166,4
35 -> 5*
49 -> 5*
64 -> 134,66
65 -> 67*
66 -> 134*
67 -> 133*
68 -> 65,21
88 -> 165*
89 -> 65,21
133 -> 21*
134 -> 20*
165 -> 21*
166 -> 20*
problem:
strict:
r1(a(x1)) -> a(a(a(r1(x1))))
a(l1(x1)) -> l1(a(a(a(x1))))
a(a(l2(x1))) -> l2(a(a(x1)))
b(l1(x1)) -> b(r2(x1))
b(l2(x1)) -> b(r1(x1))
a(a(x1)) -> x1
weak:
r1(b(x1)) -> l1(b(x1))
r2(a(x1)) -> a(a(a(r2(x1))))
r2(b(x1)) -> l2(a(b(x1)))
Bounds Processor:
bound: 0
enrichment: match
automaton:
final states: {6,5,4,3}
transitions:
r10(2) -> 3*
r10(1) -> 3*
a0(157) -> 158*
a0(127) -> 128*
a0(62) -> 63*
a0(7) -> 8*
a0(2) -> 4*
a0(61) -> 62*
a0(1) -> 4*
a0(63) -> 64*
a0(8) -> 9*
r20(2) -> 6*
r20(1) -> 6*
l10(2) -> 1*
l10(64) -> 65*
l10(9) -> 10*
l10(1) -> 1*
l20(2) -> 2*
l20(66) -> 67*
l20(1) -> 2*
b0(2) -> 5*
b0(36) -> 37*
b0(1) -> 5*
b0(38) -> 39*
1 -> 62,8
2 -> 62,8
3 -> 38*
4 -> 7*
6 -> 36*
7 -> 158,128,9
8 -> 62,66
9 -> 61*
10 -> 158,128,4
37 -> 5*
39 -> 5*
61 -> 128,63
62 -> 64*
63 -> 128*
64 -> 127*
65 -> 62,8
66 -> 157*
67 -> 62,8
127 -> 8*
128 -> 7*
157 -> 8*
158 -> 7*
problem:
strict:
a(l1(x1)) -> l1(a(a(a(x1))))
a(a(l2(x1))) -> l2(a(a(x1)))
b(l1(x1)) -> b(r2(x1))
b(l2(x1)) -> b(r1(x1))
a(a(x1)) -> x1
weak:
r1(a(x1)) -> a(a(a(r1(x1))))
r1(b(x1)) -> l1(b(x1))
r2(a(x1)) -> a(a(a(r2(x1))))
r2(b(x1)) -> l2(a(b(x1)))
Bounds Processor:
bound: 1
enrichment: match
automaton:
final states: {6,5,4,3}
transitions:
l11(42) -> 43*
l11(125) -> 126*
a1(40) -> 41*
a1(122) -> 123*
a1(159) -> 160*
a1(124) -> 125*
a1(44) -> 45*
a1(39) -> 40*
a1(41) -> 42*
a1(143) -> 144*
a1(123) -> 124*
b1(20) -> 21*
r11(22) -> 23*
r11(19) -> 20*
l21(83) -> 84*
r10(2) -> 5*
r10(1) -> 5*
a0(2) -> 3*
a0(1) -> 3*
r20(2) -> 6*
r20(1) -> 6*
l10(2) -> 1*
l10(1) -> 1*
l20(2) -> 2*
l20(1) -> 2*
b0(62) -> 63*
b0(2) -> 4*
b0(1) -> 4*
1 -> 44,22
2 -> 39,19
6 -> 62*
21 -> 4*
23 -> 20*
39 -> 123,41
40 -> 160,144,42
41 -> 123,83
42 -> 122*
43 -> 160,144,45,3
44 -> 123,41
45 -> 40*
63 -> 4*
83 -> 159*
84 -> 123,41
122 -> 144,124
123 -> 125*
124 -> 144*
125 -> 143*
126 -> 123,41
143 -> 41,123
144 -> 40*
159 -> 41,123
160 -> 40*
problem:
strict:
a(l1(x1)) -> l1(a(a(a(x1))))
a(a(l2(x1))) -> l2(a(a(x1)))
b(l1(x1)) -> b(r2(x1))
a(a(x1)) -> x1
weak:
b(l2(x1)) -> b(r1(x1))
r1(a(x1)) -> a(a(a(r1(x1))))
r1(b(x1)) -> l1(b(x1))
r2(a(x1)) -> a(a(a(r2(x1))))
r2(b(x1)) -> l2(a(b(x1)))
Bounds Processor:
bound: 1
enrichment: match
automaton:
final states: {6,5,4,3}
transitions:
l11(32) -> 33*
l11(104) -> 105*
a1(30) -> 31*
a1(102) -> 103*
a1(134) -> 135*
a1(34) -> 35*
a1(29) -> 30*
a1(106) -> 107*
a1(101) -> 102*
a1(31) -> 32*
a1(103) -> 104*
b1(17) -> 18*
r21(19) -> 20*
r21(16) -> 17*
l21(67) -> 68*
r10(2) -> 5*
r10(1) -> 5*
a0(2) -> 3*
a0(1) -> 3*
r20(2) -> 6*
r20(1) -> 6*
l10(2) -> 1*
l10(1) -> 1*
l20(2) -> 2*
l20(1) -> 2*
b0(2) -> 4*
b0(1) -> 4*
b0(48) -> 49*
1 -> 34,19
2 -> 29,16
5 -> 48*
18 -> 4*
20 -> 17*
29 -> 102,31
30 -> 135,107,32
31 -> 102,67
32 -> 101*
33 -> 135,107,35,3
34 -> 102,31
35 -> 30*
49 -> 4*
67 -> 134*
68 -> 102,31
101 -> 107,103
102 -> 104*
103 -> 107*
104 -> 106*
105 -> 102,31
106 -> 31,102,104
107 -> 30*
134 -> 31,102,104
135 -> 30*
problem:
strict:
a(l1(x1)) -> l1(a(a(a(x1))))
a(a(l2(x1))) -> l2(a(a(x1)))
a(a(x1)) -> x1
weak:
b(l1(x1)) -> b(r2(x1))
b(l2(x1)) -> b(r1(x1))
r1(a(x1)) -> a(a(a(r1(x1))))
r1(b(x1)) -> l1(b(x1))
r2(a(x1)) -> a(a(a(r2(x1))))
r2(b(x1)) -> l2(a(b(x1)))
OpenTool IRC1
stdout:
MAYBE
Tool IRC2
stdout:
TIMEOUT
'Fastest (timeout of 60.0 seconds)'
-----------------------------------
Answer: TIMEOUT
Input Problem: innermost runtime-complexity with respect to
Rules:
{ r1(a(x1)) -> a(a(a(r1(x1))))
, r2(a(x1)) -> a(a(a(r2(x1))))
, a(l1(x1)) -> l1(a(a(a(x1))))
, a(a(l2(x1))) -> l2(a(a(x1)))
, r1(b(x1)) -> l1(b(x1))
, r2(b(x1)) -> l2(a(b(x1)))
, b(l1(x1)) -> b(r2(x1))
, b(l2(x1)) -> b(r1(x1))
, a(a(x1)) -> x1}
Proof Output:
Computation stopped due to timeout after 60.0 secondsTool RC1
stdout:
MAYBE
Tool RC2
stdout:
TIMEOUT
'Fastest (timeout of 60.0 seconds)'
-----------------------------------
Answer: TIMEOUT
Input Problem: runtime-complexity with respect to
Rules:
{ r1(a(x1)) -> a(a(a(r1(x1))))
, r2(a(x1)) -> a(a(a(r2(x1))))
, a(l1(x1)) -> l1(a(a(a(x1))))
, a(a(l2(x1))) -> l2(a(a(x1)))
, r1(b(x1)) -> l1(b(x1))
, r2(b(x1)) -> l2(a(b(x1)))
, b(l1(x1)) -> b(r2(x1))
, b(l2(x1)) -> b(r1(x1))
, a(a(x1)) -> x1}
Proof Output:
Computation stopped due to timeout after 60.0 seconds