MAYBE 229.29/124.37 MAYBE 229.29/124.37 229.29/124.37 We are left with following problem, upon which TcT provides the 229.29/124.37 certificate MAYBE. 229.29/124.37 229.29/124.37 Strict Trs: 229.29/124.37 { minus(x, 0()) -> x 229.29/124.37 , minus(s(x), s(y)) -> minus(x, y) 229.29/124.37 , double(0()) -> 0() 229.29/124.37 , double(s(x)) -> s(s(double(x))) 229.29/124.37 , plus(0(), y) -> y 229.29/124.37 , plus(s(x), y) -> s(plus(x, y)) 229.29/124.37 , plus(s(x), y) -> s(plus(minus(x, y), double(y))) 229.29/124.37 , plus(s(x), y) -> plus(x, s(y)) } 229.29/124.37 Obligation: 229.29/124.37 innermost runtime complexity 229.29/124.37 Answer: 229.29/124.37 MAYBE 229.29/124.37 229.29/124.37 None of the processors succeeded. 229.29/124.37 229.29/124.37 Details of failed attempt(s): 229.29/124.37 ----------------------------- 229.29/124.37 1) 'empty' failed due to the following reason: 229.29/124.37 229.29/124.37 Empty strict component of the problem is NOT empty. 229.29/124.37 229.29/124.37 2) 'Best' failed due to the following reason: 229.29/124.37 229.29/124.37 None of the processors succeeded. 229.29/124.37 229.29/124.37 Details of failed attempt(s): 229.29/124.37 ----------------------------- 229.29/124.37 1) 'With Problem ... (timeout of 297 seconds)' failed due to the 229.29/124.37 following reason: 229.29/124.37 229.29/124.37 We add the following dependency tuples: 229.29/124.37 229.29/124.37 Strict DPs: 229.29/124.37 { minus^#(x, 0()) -> c_1() 229.29/124.37 , minus^#(s(x), s(y)) -> c_2(minus^#(x, y)) 229.29/124.37 , double^#(0()) -> c_3() 229.29/124.37 , double^#(s(x)) -> c_4(double^#(x)) 229.29/124.37 , plus^#(0(), y) -> c_5() 229.29/124.37 , plus^#(s(x), y) -> c_6(plus^#(x, y)) 229.29/124.37 , plus^#(s(x), y) -> 229.29/124.37 c_7(plus^#(minus(x, y), double(y)), minus^#(x, y), double^#(y)) 229.29/124.37 , plus^#(s(x), y) -> c_8(plus^#(x, s(y))) } 229.29/124.37 229.29/124.37 and mark the set of starting terms. 229.29/124.37 229.29/124.37 We are left with following problem, upon which TcT provides the 229.29/124.37 certificate MAYBE. 229.29/124.37 229.29/124.37 Strict DPs: 229.29/124.37 { minus^#(x, 0()) -> c_1() 229.29/124.37 , minus^#(s(x), s(y)) -> c_2(minus^#(x, y)) 229.29/124.37 , double^#(0()) -> c_3() 229.29/124.37 , double^#(s(x)) -> c_4(double^#(x)) 229.29/124.37 , plus^#(0(), y) -> c_5() 229.29/124.37 , plus^#(s(x), y) -> c_6(plus^#(x, y)) 229.29/124.37 , plus^#(s(x), y) -> 229.29/124.37 c_7(plus^#(minus(x, y), double(y)), minus^#(x, y), double^#(y)) 229.29/124.37 , plus^#(s(x), y) -> c_8(plus^#(x, s(y))) } 229.29/124.37 Weak Trs: 229.29/124.37 { minus(x, 0()) -> x 229.29/124.37 , minus(s(x), s(y)) -> minus(x, y) 229.29/124.37 , double(0()) -> 0() 229.29/124.37 , double(s(x)) -> s(s(double(x))) 229.29/124.37 , plus(0(), y) -> y 229.29/124.37 , plus(s(x), y) -> s(plus(x, y)) 229.29/124.37 , plus(s(x), y) -> s(plus(minus(x, y), double(y))) 229.29/124.37 , plus(s(x), y) -> plus(x, s(y)) } 229.29/124.37 Obligation: 229.29/124.37 innermost runtime complexity 229.29/124.37 Answer: 229.29/124.37 MAYBE 229.29/124.37 229.29/124.37 We estimate the number of application of {1,3,5} by applications of 229.29/124.37 Pre({1,3,5}) = {2,4,6,7,8}. Here rules are labeled as follows: 229.29/124.37 229.29/124.37 DPs: 229.29/124.37 { 1: minus^#(x, 0()) -> c_1() 229.29/124.37 , 2: minus^#(s(x), s(y)) -> c_2(minus^#(x, y)) 229.29/124.37 , 3: double^#(0()) -> c_3() 229.29/124.37 , 4: double^#(s(x)) -> c_4(double^#(x)) 229.29/124.37 , 5: plus^#(0(), y) -> c_5() 229.29/124.37 , 6: plus^#(s(x), y) -> c_6(plus^#(x, y)) 229.29/124.37 , 7: plus^#(s(x), y) -> 229.29/124.37 c_7(plus^#(minus(x, y), double(y)), minus^#(x, y), double^#(y)) 229.29/124.37 , 8: plus^#(s(x), y) -> c_8(plus^#(x, s(y))) } 229.29/124.37 229.29/124.37 We are left with following problem, upon which TcT provides the 229.29/124.37 certificate MAYBE. 229.29/124.37 229.29/124.37 Strict DPs: 229.29/124.37 { minus^#(s(x), s(y)) -> c_2(minus^#(x, y)) 229.29/124.37 , double^#(s(x)) -> c_4(double^#(x)) 229.29/124.37 , plus^#(s(x), y) -> c_6(plus^#(x, y)) 229.29/124.37 , plus^#(s(x), y) -> 229.29/124.37 c_7(plus^#(minus(x, y), double(y)), minus^#(x, y), double^#(y)) 229.29/124.37 , plus^#(s(x), y) -> c_8(plus^#(x, s(y))) } 229.29/124.37 Weak DPs: 229.29/124.37 { minus^#(x, 0()) -> c_1() 229.29/124.37 , double^#(0()) -> c_3() 229.29/124.37 , plus^#(0(), y) -> c_5() } 229.29/124.37 Weak Trs: 229.29/124.37 { minus(x, 0()) -> x 229.29/124.37 , minus(s(x), s(y)) -> minus(x, y) 229.29/124.37 , double(0()) -> 0() 229.29/124.37 , double(s(x)) -> s(s(double(x))) 229.29/124.37 , plus(0(), y) -> y 229.29/124.37 , plus(s(x), y) -> s(plus(x, y)) 229.29/124.37 , plus(s(x), y) -> s(plus(minus(x, y), double(y))) 229.29/124.37 , plus(s(x), y) -> plus(x, s(y)) } 229.29/124.37 Obligation: 229.29/124.37 innermost runtime complexity 229.29/124.37 Answer: 229.29/124.37 MAYBE 229.29/124.37 229.29/124.37 The following weak DPs constitute a sub-graph of the DG that is 229.29/124.37 closed under successors. The DPs are removed. 229.29/124.37 229.29/124.37 { minus^#(x, 0()) -> c_1() 229.29/124.37 , double^#(0()) -> c_3() 229.29/124.37 , plus^#(0(), y) -> c_5() } 229.29/124.37 229.29/124.37 We are left with following problem, upon which TcT provides the 229.29/124.37 certificate MAYBE. 229.29/124.37 229.29/124.37 Strict DPs: 229.29/124.37 { minus^#(s(x), s(y)) -> c_2(minus^#(x, y)) 229.29/124.37 , double^#(s(x)) -> c_4(double^#(x)) 229.29/124.37 , plus^#(s(x), y) -> c_6(plus^#(x, y)) 229.29/124.37 , plus^#(s(x), y) -> 229.29/124.37 c_7(plus^#(minus(x, y), double(y)), minus^#(x, y), double^#(y)) 229.29/124.37 , plus^#(s(x), y) -> c_8(plus^#(x, s(y))) } 229.29/124.37 Weak Trs: 229.29/124.37 { minus(x, 0()) -> x 229.29/124.37 , minus(s(x), s(y)) -> minus(x, y) 229.29/124.37 , double(0()) -> 0() 229.29/124.37 , double(s(x)) -> s(s(double(x))) 229.29/124.37 , plus(0(), y) -> y 229.29/124.37 , plus(s(x), y) -> s(plus(x, y)) 229.29/124.37 , plus(s(x), y) -> s(plus(minus(x, y), double(y))) 229.29/124.37 , plus(s(x), y) -> plus(x, s(y)) } 229.29/124.37 Obligation: 229.29/124.37 innermost runtime complexity 229.29/124.37 Answer: 229.29/124.37 MAYBE 229.29/124.37 229.29/124.37 We replace rewrite rules by usable rules: 229.29/124.37 229.29/124.37 Weak Usable Rules: 229.29/124.37 { minus(x, 0()) -> x 229.29/124.37 , minus(s(x), s(y)) -> minus(x, y) 229.29/124.37 , double(0()) -> 0() 229.29/124.37 , double(s(x)) -> s(s(double(x))) } 229.29/124.37 229.29/124.37 We are left with following problem, upon which TcT provides the 229.29/124.37 certificate MAYBE. 229.29/124.37 229.29/124.37 Strict DPs: 229.29/124.37 { minus^#(s(x), s(y)) -> c_2(minus^#(x, y)) 229.29/124.37 , double^#(s(x)) -> c_4(double^#(x)) 229.29/124.37 , plus^#(s(x), y) -> c_6(plus^#(x, y)) 229.29/124.37 , plus^#(s(x), y) -> 229.29/124.37 c_7(plus^#(minus(x, y), double(y)), minus^#(x, y), double^#(y)) 229.29/124.37 , plus^#(s(x), y) -> c_8(plus^#(x, s(y))) } 229.29/124.37 Weak Trs: 229.29/124.37 { minus(x, 0()) -> x 229.29/124.37 , minus(s(x), s(y)) -> minus(x, y) 229.29/124.37 , double(0()) -> 0() 229.29/124.37 , double(s(x)) -> s(s(double(x))) } 229.29/124.37 Obligation: 229.29/124.37 innermost runtime complexity 229.29/124.37 Answer: 229.29/124.37 MAYBE 229.29/124.37 229.29/124.37 None of the processors succeeded. 229.29/124.37 229.29/124.37 Details of failed attempt(s): 229.29/124.37 ----------------------------- 229.29/124.37 1) 'empty' failed due to the following reason: 229.29/124.37 229.29/124.37 Empty strict component of the problem is NOT empty. 229.29/124.37 229.29/124.37 2) 'With Problem ...' failed due to the following reason: 229.29/124.37 229.29/124.37 We use the processor 'matrix interpretation of dimension 2' to 229.29/124.37 orient following rules strictly. 229.29/124.37 229.29/124.37 DPs: 229.29/124.37 { 1: minus^#(s(x), s(y)) -> c_2(minus^#(x, y)) } 229.29/124.37 229.29/124.37 Sub-proof: 229.29/124.37 ---------- 229.29/124.37 The following argument positions are usable: 229.29/124.37 Uargs(c_2) = {1}, Uargs(c_4) = {1}, Uargs(c_6) = {1}, 229.29/124.37 Uargs(c_7) = {1, 2, 3}, Uargs(c_8) = {1} 229.29/124.37 229.29/124.37 TcT has computed the following constructor-based matrix 229.29/124.37 interpretation satisfying not(EDA). 229.29/124.37 229.29/124.37 [minus](x1, x2) = [1 0] x1 + [0] 229.29/124.37 [0 1] [0] 229.29/124.37 229.29/124.37 [0] = [0] 229.29/124.37 [0] 229.29/124.37 229.29/124.37 [s](x1) = [1 3] x1 + [0] 229.29/124.37 [0 1] [4] 229.29/124.37 229.29/124.37 [double](x1) = [0] 229.29/124.37 [0] 229.29/124.37 229.29/124.37 [minus^#](x1, x2) = [0 2] x1 + [0 0] x2 + [0] 229.29/124.37 [1 1] [2 1] [0] 229.29/124.37 229.29/124.37 [c_2](x1) = [1 0] x1 + [5] 229.29/124.37 [0 0] [3] 229.29/124.37 229.29/124.37 [double^#](x1) = [0 0] x1 + [0] 229.29/124.37 [3 0] [4] 229.29/124.37 229.29/124.37 [c_4](x1) = [4 0] x1 + [0] 229.29/124.37 [0 0] [3] 229.29/124.37 229.29/124.37 [plus^#](x1, x2) = [3 0] x1 + [0] 229.29/124.37 [0 0] [4] 229.29/124.37 229.29/124.37 [c_6](x1) = [1 0] x1 + [0] 229.29/124.37 [0 0] [3] 229.29/124.37 229.29/124.37 [c_7](x1, x2, x3) = [1 0] x1 + [4 0] x2 + [2 0] x3 + [0] 229.29/124.37 [0 0] [0 0] [0 0] [3] 229.29/124.37 229.29/124.37 [c_8](x1) = [1 0] x1 + [0] 229.29/124.37 [0 0] [3] 229.29/124.37 229.29/124.37 The order satisfies the following ordering constraints: 229.29/124.37 229.29/124.37 [minus(x, 0())] = [1 0] x + [0] 229.29/124.37 [0 1] [0] 229.29/124.37 >= [1 0] x + [0] 229.29/124.37 [0 1] [0] 229.29/124.37 = [x] 229.29/124.37 229.29/124.37 [minus(s(x), s(y))] = [1 3] x + [0] 229.29/124.37 [0 1] [4] 229.29/124.37 >= [1 0] x + [0] 229.29/124.37 [0 1] [0] 229.29/124.37 = [minus(x, y)] 229.29/124.37 229.29/124.37 [double(0())] = [0] 229.29/124.37 [0] 229.29/124.37 >= [0] 229.29/124.37 [0] 229.29/124.37 = [0()] 229.29/124.37 229.29/124.37 [double(s(x))] = [0] 229.29/124.37 [0] 229.29/124.37 ? [12] 229.29/124.37 [8] 229.29/124.37 = [s(s(double(x)))] 229.29/124.37 229.29/124.37 [minus^#(s(x), s(y))] = [0 2] x + [0 0] y + [8] 229.29/124.37 [1 4] [2 7] [8] 229.29/124.37 > [0 2] x + [5] 229.29/124.37 [0 0] [3] 229.29/124.37 = [c_2(minus^#(x, y))] 229.29/124.37 229.29/124.37 [double^#(s(x))] = [0 0] x + [0] 229.29/124.37 [3 9] [4] 229.29/124.37 >= [0] 229.29/124.37 [3] 229.29/124.37 = [c_4(double^#(x))] 229.29/124.37 229.29/124.37 [plus^#(s(x), y)] = [3 9] x + [0] 229.29/124.37 [0 0] [4] 229.29/124.37 >= [3 0] x + [0] 229.29/124.37 [0 0] [3] 229.29/124.37 = [c_6(plus^#(x, y))] 229.29/124.37 229.29/124.37 [plus^#(s(x), y)] = [3 9] x + [0] 229.29/124.37 [0 0] [4] 229.29/124.37 >= [3 8] x + [0] 229.29/124.37 [0 0] [3] 229.29/124.37 = [c_7(plus^#(minus(x, y), double(y)), minus^#(x, y), double^#(y))] 229.29/124.37 229.29/124.37 [plus^#(s(x), y)] = [3 9] x + [0] 229.29/124.37 [0 0] [4] 229.29/124.37 >= [3 0] x + [0] 229.29/124.37 [0 0] [3] 229.29/124.37 = [c_8(plus^#(x, s(y)))] 229.29/124.37 229.29/124.37 229.29/124.37 The strictly oriented rules are moved into the weak component. 229.29/124.37 229.29/124.37 We are left with following problem, upon which TcT provides the 229.29/124.37 certificate MAYBE. 229.29/124.37 229.29/124.37 Strict DPs: 229.29/124.37 { double^#(s(x)) -> c_4(double^#(x)) 229.29/124.37 , plus^#(s(x), y) -> c_6(plus^#(x, y)) 229.29/124.37 , plus^#(s(x), y) -> 229.29/124.37 c_7(plus^#(minus(x, y), double(y)), minus^#(x, y), double^#(y)) 229.29/124.37 , plus^#(s(x), y) -> c_8(plus^#(x, s(y))) } 229.29/124.37 Weak DPs: { minus^#(s(x), s(y)) -> c_2(minus^#(x, y)) } 229.29/124.37 Weak Trs: 229.29/124.37 { minus(x, 0()) -> x 229.29/124.37 , minus(s(x), s(y)) -> minus(x, y) 229.29/124.37 , double(0()) -> 0() 229.29/124.37 , double(s(x)) -> s(s(double(x))) } 229.29/124.37 Obligation: 229.29/124.37 innermost runtime complexity 229.29/124.37 Answer: 229.29/124.37 MAYBE 229.29/124.37 229.29/124.37 The following weak DPs constitute a sub-graph of the DG that is 229.29/124.37 closed under successors. The DPs are removed. 229.29/124.37 229.29/124.37 { minus^#(s(x), s(y)) -> c_2(minus^#(x, y)) } 229.29/124.37 229.29/124.37 We are left with following problem, upon which TcT provides the 229.29/124.37 certificate MAYBE. 229.29/124.37 229.29/124.37 Strict DPs: 229.29/124.37 { double^#(s(x)) -> c_4(double^#(x)) 229.29/124.37 , plus^#(s(x), y) -> c_6(plus^#(x, y)) 229.29/124.37 , plus^#(s(x), y) -> 229.29/124.37 c_7(plus^#(minus(x, y), double(y)), minus^#(x, y), double^#(y)) 229.29/124.37 , plus^#(s(x), y) -> c_8(plus^#(x, s(y))) } 229.29/124.37 Weak Trs: 229.29/124.37 { minus(x, 0()) -> x 229.29/124.37 , minus(s(x), s(y)) -> minus(x, y) 229.29/124.37 , double(0()) -> 0() 229.29/124.37 , double(s(x)) -> s(s(double(x))) } 229.29/124.37 Obligation: 229.29/124.37 innermost runtime complexity 229.29/124.37 Answer: 229.29/124.37 MAYBE 229.29/124.37 229.29/124.37 Due to missing edges in the dependency-graph, the right-hand sides 229.29/124.37 of following rules could be simplified: 229.29/124.37 229.29/124.37 { plus^#(s(x), y) -> 229.29/124.37 c_7(plus^#(minus(x, y), double(y)), minus^#(x, y), double^#(y)) } 229.29/124.37 229.29/124.37 We are left with following problem, upon which TcT provides the 229.29/124.37 certificate MAYBE. 229.29/124.37 229.29/124.37 Strict DPs: 229.29/124.37 { double^#(s(x)) -> c_1(double^#(x)) 229.29/124.37 , plus^#(s(x), y) -> c_2(plus^#(x, y)) 229.29/124.37 , plus^#(s(x), y) -> c_3(plus^#(x, s(y))) 229.29/124.37 , plus^#(s(x), y) -> 229.29/124.37 c_4(plus^#(minus(x, y), double(y)), double^#(y)) } 229.29/124.37 Weak Trs: 229.29/124.37 { minus(x, 0()) -> x 229.29/124.37 , minus(s(x), s(y)) -> minus(x, y) 229.29/124.37 , double(0()) -> 0() 229.29/124.37 , double(s(x)) -> s(s(double(x))) } 229.29/124.37 Obligation: 229.29/124.37 innermost runtime complexity 229.29/124.37 Answer: 229.29/124.37 MAYBE 229.29/124.37 229.29/124.37 We decompose the input problem according to the dependency graph 229.29/124.37 into the upper component 229.29/124.37 229.29/124.37 { plus^#(s(x), y) -> c_2(plus^#(x, y)) 229.29/124.37 , plus^#(s(x), y) -> c_3(plus^#(x, s(y))) 229.29/124.37 , plus^#(s(x), y) -> 229.29/124.37 c_4(plus^#(minus(x, y), double(y)), double^#(y)) } 229.29/124.37 229.29/124.37 and lower component 229.29/124.37 229.29/124.37 { double^#(s(x)) -> c_1(double^#(x)) } 229.29/124.37 229.29/124.37 Further, following extension rules are added to the lower 229.29/124.37 component. 229.29/124.37 229.29/124.37 { plus^#(s(x), y) -> double^#(y) 229.29/124.37 , plus^#(s(x), y) -> plus^#(x, y) 229.29/124.37 , plus^#(s(x), y) -> plus^#(x, s(y)) 229.29/124.37 , plus^#(s(x), y) -> plus^#(minus(x, y), double(y)) } 229.29/124.37 229.29/124.37 TcT solves the upper component with certificate YES(O(1),O(n^1)). 229.29/124.37 229.29/124.37 Sub-proof: 229.29/124.37 ---------- 229.29/124.37 We are left with following problem, upon which TcT provides the 229.29/124.37 certificate YES(O(1),O(n^1)). 229.29/124.37 229.29/124.37 Strict DPs: 229.29/124.37 { plus^#(s(x), y) -> c_2(plus^#(x, y)) 229.29/124.37 , plus^#(s(x), y) -> c_3(plus^#(x, s(y))) 229.29/124.37 , plus^#(s(x), y) -> 229.29/124.37 c_4(plus^#(minus(x, y), double(y)), double^#(y)) } 229.29/124.37 Weak Trs: 229.29/124.37 { minus(x, 0()) -> x 229.29/124.37 , minus(s(x), s(y)) -> minus(x, y) 229.29/124.37 , double(0()) -> 0() 229.29/124.37 , double(s(x)) -> s(s(double(x))) } 229.29/124.37 Obligation: 229.29/124.37 innermost runtime complexity 229.29/124.37 Answer: 229.29/124.37 YES(O(1),O(n^1)) 229.29/124.37 229.29/124.37 We use the processor 'Small Polynomial Path Order (PS,1-bounded)' 229.29/124.37 to orient following rules strictly. 229.29/124.37 229.29/124.37 DPs: 229.29/124.37 { 1: plus^#(s(x), y) -> c_2(plus^#(x, y)) 229.29/124.37 , 2: plus^#(s(x), y) -> c_3(plus^#(x, s(y))) 229.29/124.37 , 3: plus^#(s(x), y) -> 229.29/124.37 c_4(plus^#(minus(x, y), double(y)), double^#(y)) } 229.29/124.37 Trs: 229.29/124.37 { minus(s(x), s(y)) -> minus(x, y) 229.29/124.37 , double(0()) -> 0() } 229.29/124.37 229.29/124.37 Sub-proof: 229.29/124.37 ---------- 229.29/124.37 The input was oriented with the instance of 'Small Polynomial Path 229.29/124.37 Order (PS,1-bounded)' as induced by the safe mapping 229.29/124.37 229.29/124.37 safe(minus) = {}, safe(0) = {}, safe(s) = {1}, safe(double) = {}, 229.29/124.37 safe(double^#) = {}, safe(plus^#) = {2}, safe(c_2) = {}, 229.29/124.37 safe(c_3) = {}, safe(c_4) = {} 229.29/124.37 229.29/124.37 and precedence 229.29/124.37 229.29/124.37 minus ~ double, minus ~ plus^#, double ~ plus^# . 229.29/124.37 229.29/124.37 Following symbols are considered recursive: 229.29/124.37 229.29/124.37 {double, plus^#} 229.29/124.37 229.29/124.37 The recursion depth is 1. 229.29/124.37 229.29/124.37 Further, following argument filtering is employed: 229.29/124.37 229.29/124.37 pi(minus) = 1, pi(0) = [], pi(s) = [1], pi(double) = [], 229.29/124.37 pi(double^#) = [], pi(plus^#) = [1], pi(c_2) = [1], pi(c_3) = [1], 229.29/124.37 pi(c_4) = [1, 2] 229.29/124.37 229.29/124.37 Usable defined function symbols are a subset of: 229.29/124.37 229.29/124.37 {minus, double^#, plus^#} 229.29/124.37 229.29/124.37 For your convenience, here are the satisfied ordering constraints: 229.29/124.37 229.29/124.37 pi(plus^#(s(x), y)) = plus^#(s(; x);) 229.29/124.37 > c_2(plus^#(x;);) 229.29/124.37 = pi(c_2(plus^#(x, y))) 229.29/124.37 229.29/124.37 pi(plus^#(s(x), y)) = plus^#(s(; x);) 229.29/124.37 > c_3(plus^#(x;);) 229.29/124.37 = pi(c_3(plus^#(x, s(y)))) 229.29/124.37 229.29/124.37 pi(plus^#(s(x), y)) = plus^#(s(; x);) 229.29/124.37 > c_4(plus^#(x;), double^#();) 229.29/124.37 = pi(c_4(plus^#(minus(x, y), double(y)), double^#(y))) 229.29/124.37 229.29/124.37 pi(minus(x, 0())) = x 229.29/124.37 >= x 229.29/124.37 = pi(x) 229.29/124.37 229.29/124.37 pi(minus(s(x), s(y))) = s(; x) 229.29/124.37 > x 229.29/124.37 = pi(minus(x, y)) 229.29/124.37 229.29/124.37 229.29/124.37 The strictly oriented rules are moved into the weak component. 229.29/124.37 229.29/124.37 We are left with following problem, upon which TcT provides the 229.29/124.37 certificate YES(O(1),O(1)). 229.29/124.37 229.29/124.37 Weak DPs: 229.29/124.37 { plus^#(s(x), y) -> c_2(plus^#(x, y)) 229.29/124.37 , plus^#(s(x), y) -> c_3(plus^#(x, s(y))) 229.29/124.37 , plus^#(s(x), y) -> 229.29/124.37 c_4(plus^#(minus(x, y), double(y)), double^#(y)) } 229.29/124.37 Weak Trs: 229.29/124.37 { minus(x, 0()) -> x 229.29/124.37 , minus(s(x), s(y)) -> minus(x, y) 229.29/124.37 , double(0()) -> 0() 229.29/124.37 , double(s(x)) -> s(s(double(x))) } 229.29/124.37 Obligation: 229.29/124.37 innermost runtime complexity 229.29/124.37 Answer: 229.29/124.37 YES(O(1),O(1)) 229.29/124.37 229.29/124.37 The following weak DPs constitute a sub-graph of the DG that is 229.29/124.37 closed under successors. The DPs are removed. 229.29/124.37 229.29/124.37 { plus^#(s(x), y) -> c_2(plus^#(x, y)) 229.29/124.37 , plus^#(s(x), y) -> c_3(plus^#(x, s(y))) 229.29/124.37 , plus^#(s(x), y) -> 229.29/124.37 c_4(plus^#(minus(x, y), double(y)), double^#(y)) } 229.29/124.37 229.29/124.37 We are left with following problem, upon which TcT provides the 229.29/124.37 certificate YES(O(1),O(1)). 229.29/124.37 229.29/124.37 Weak Trs: 229.29/124.37 { minus(x, 0()) -> x 229.29/124.37 , minus(s(x), s(y)) -> minus(x, y) 229.29/124.37 , double(0()) -> 0() 229.29/124.37 , double(s(x)) -> s(s(double(x))) } 229.29/124.37 Obligation: 229.29/124.37 innermost runtime complexity 229.29/124.37 Answer: 229.29/124.37 YES(O(1),O(1)) 229.29/124.37 229.29/124.37 No rule is usable, rules are removed from the input problem. 229.29/124.37 229.29/124.37 We are left with following problem, upon which TcT provides the 229.29/124.37 certificate YES(O(1),O(1)). 229.29/124.37 229.29/124.37 Rules: Empty 229.29/124.37 Obligation: 229.29/124.37 innermost runtime complexity 229.29/124.37 Answer: 229.29/124.37 YES(O(1),O(1)) 229.29/124.37 229.29/124.37 Empty rules are trivially bounded 229.29/124.37 229.29/124.37 We return to the main proof. 229.29/124.37 229.29/124.37 We are left with following problem, upon which TcT provides the 229.29/124.37 certificate MAYBE. 229.29/124.37 229.29/124.37 Strict DPs: { double^#(s(x)) -> c_1(double^#(x)) } 229.29/124.37 Weak DPs: 229.29/124.37 { plus^#(s(x), y) -> double^#(y) 229.29/124.37 , plus^#(s(x), y) -> plus^#(x, y) 229.29/124.37 , plus^#(s(x), y) -> plus^#(x, s(y)) 229.29/124.37 , plus^#(s(x), y) -> plus^#(minus(x, y), double(y)) } 229.29/124.37 Weak Trs: 229.29/124.37 { minus(x, 0()) -> x 229.29/124.37 , minus(s(x), s(y)) -> minus(x, y) 229.29/124.37 , double(0()) -> 0() 229.29/124.37 , double(s(x)) -> s(s(double(x))) } 229.29/124.37 Obligation: 229.29/124.37 innermost runtime complexity 229.29/124.37 Answer: 229.29/124.37 MAYBE 229.29/124.37 229.29/124.37 None of the processors succeeded. 229.29/124.37 229.29/124.37 Details of failed attempt(s): 229.29/124.37 ----------------------------- 229.29/124.37 1) 'empty' failed due to the following reason: 229.29/124.37 229.29/124.37 Empty strict component of the problem is NOT empty. 229.29/124.37 229.29/124.37 2) 'Fastest' failed due to the following reason: 229.29/124.37 229.29/124.37 None of the processors succeeded. 229.29/124.37 229.29/124.37 Details of failed attempt(s): 229.29/124.37 ----------------------------- 229.29/124.37 1) 'With Problem ...' failed due to the following reason: 229.29/124.37 229.29/124.37 None of the processors succeeded. 229.29/124.37 229.29/124.37 Details of failed attempt(s): 229.29/124.37 ----------------------------- 229.29/124.37 1) 'empty' failed due to the following reason: 229.29/124.37 229.29/124.37 Empty strict component of the problem is NOT empty. 229.29/124.37 229.29/124.37 2) 'Polynomial Path Order (PS)' failed due to the following reason: 229.29/124.37 229.29/124.37 The input cannot be shown compatible 229.29/124.37 229.29/124.37 229.29/124.37 2) 'Polynomial Path Order (PS)' failed due to the following reason: 229.29/124.37 229.29/124.37 The input cannot be shown compatible 229.29/124.37 229.29/124.37 3) 'Fastest (timeout of 24 seconds)' failed due to the following 229.29/124.37 reason: 229.29/124.37 229.29/124.37 None of the processors succeeded. 229.29/124.37 229.29/124.37 Details of failed attempt(s): 229.29/124.37 ----------------------------- 229.29/124.37 1) 'Bounds with minimal-enrichment and initial automaton 'match'' 229.29/124.37 failed due to the following reason: 229.29/124.37 229.29/124.37 match-boundness of the problem could not be verified. 229.29/124.37 229.29/124.37 2) 'Bounds with perSymbol-enrichment and initial automaton 'match'' 229.29/124.37 failed due to the following reason: 229.29/124.37 229.29/124.37 match-boundness of the problem could not be verified. 229.29/124.37 229.29/124.37 229.29/124.37 229.29/124.37 229.29/124.37 229.29/124.37 2) 'Best' failed due to the following reason: 229.29/124.37 229.29/124.37 None of the processors succeeded. 229.29/124.37 229.29/124.37 Details of failed attempt(s): 229.29/124.37 ----------------------------- 229.29/124.37 1) 'With Problem ... (timeout of 148 seconds) (timeout of 297 229.29/124.37 seconds)' failed due to the following reason: 229.29/124.37 229.29/124.37 The weightgap principle applies (using the following nonconstant 229.29/124.37 growth matrix-interpretation) 229.29/124.37 229.29/124.37 The following argument positions are usable: 229.29/124.37 Uargs(s) = {1}, Uargs(plus) = {1, 2} 229.29/124.37 229.29/124.37 TcT has computed the following matrix interpretation satisfying 229.29/124.37 not(EDA) and not(IDA(1)). 229.29/124.37 229.29/124.37 [minus](x1, x2) = [1] x1 + [0] 229.29/124.37 229.29/124.37 [0] = [1] 229.29/124.37 229.29/124.37 [s](x1) = [1] x1 + [0] 229.29/124.37 229.29/124.37 [double](x1) = [0] 229.29/124.37 229.29/124.37 [plus](x1, x2) = [1] x1 + [1] x2 + [0] 229.29/124.37 229.29/124.37 The order satisfies the following ordering constraints: 229.29/124.37 229.29/124.37 [minus(x, 0())] = [1] x + [0] 229.29/124.37 >= [1] x + [0] 229.29/124.37 = [x] 229.29/124.37 229.29/124.37 [minus(s(x), s(y))] = [1] x + [0] 229.29/124.37 >= [1] x + [0] 229.29/124.37 = [minus(x, y)] 229.29/124.37 229.29/124.37 [double(0())] = [0] 229.29/124.37 ? [1] 229.29/124.37 = [0()] 229.29/124.37 229.29/124.37 [double(s(x))] = [0] 229.29/124.37 >= [0] 229.29/124.37 = [s(s(double(x)))] 229.29/124.37 229.29/124.37 [plus(0(), y)] = [1] y + [1] 229.29/124.37 > [1] y + [0] 229.29/124.37 = [y] 229.29/124.37 229.29/124.37 [plus(s(x), y)] = [1] x + [1] y + [0] 229.29/124.37 >= [1] x + [1] y + [0] 229.29/124.37 = [s(plus(x, y))] 229.29/124.37 229.29/124.37 [plus(s(x), y)] = [1] x + [1] y + [0] 229.29/124.37 >= [1] x + [0] 229.29/124.37 = [s(plus(minus(x, y), double(y)))] 229.29/124.37 229.29/124.37 [plus(s(x), y)] = [1] x + [1] y + [0] 229.29/124.37 >= [1] x + [1] y + [0] 229.29/124.37 = [plus(x, s(y))] 229.29/124.37 229.29/124.37 229.29/124.37 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 229.29/124.37 229.29/124.37 We are left with following problem, upon which TcT provides the 229.29/124.37 certificate MAYBE. 229.29/124.37 229.29/124.37 Strict Trs: 229.29/124.37 { minus(x, 0()) -> x 229.29/124.37 , minus(s(x), s(y)) -> minus(x, y) 229.29/124.37 , double(0()) -> 0() 229.29/124.37 , double(s(x)) -> s(s(double(x))) 229.29/124.37 , plus(s(x), y) -> s(plus(x, y)) 229.29/124.37 , plus(s(x), y) -> s(plus(minus(x, y), double(y))) 229.29/124.37 , plus(s(x), y) -> plus(x, s(y)) } 229.29/124.37 Weak Trs: { plus(0(), y) -> y } 229.29/124.37 Obligation: 229.29/124.37 innermost runtime complexity 229.29/124.37 Answer: 229.29/124.37 MAYBE 229.29/124.37 229.29/124.37 The weightgap principle applies (using the following nonconstant 229.29/124.37 growth matrix-interpretation) 229.29/124.37 229.29/124.37 The following argument positions are usable: 229.29/124.37 Uargs(s) = {1}, Uargs(plus) = {1, 2} 229.29/124.37 229.29/124.37 TcT has computed the following matrix interpretation satisfying 229.29/124.37 not(EDA) and not(IDA(1)). 229.29/124.37 229.29/124.37 [minus](x1, x2) = [1] x1 + [1] 229.29/124.37 229.29/124.37 [0] = [5] 229.29/124.37 229.29/124.37 [s](x1) = [1] x1 + [0] 229.29/124.37 229.29/124.37 [double](x1) = [0] 229.29/124.37 229.29/124.37 [plus](x1, x2) = [1] x1 + [1] x2 + [0] 229.29/124.37 229.29/124.37 The order satisfies the following ordering constraints: 229.29/124.37 229.29/124.37 [minus(x, 0())] = [1] x + [1] 229.29/124.37 > [1] x + [0] 229.29/124.37 = [x] 229.29/124.37 229.29/124.37 [minus(s(x), s(y))] = [1] x + [1] 229.29/124.37 >= [1] x + [1] 229.29/124.37 = [minus(x, y)] 229.29/124.37 229.29/124.37 [double(0())] = [0] 229.29/124.37 ? [5] 229.29/124.37 = [0()] 229.29/124.37 229.29/124.37 [double(s(x))] = [0] 229.29/124.37 >= [0] 229.29/124.37 = [s(s(double(x)))] 229.29/124.37 229.29/124.37 [plus(0(), y)] = [1] y + [5] 229.29/124.37 > [1] y + [0] 229.29/124.37 = [y] 229.29/124.37 229.29/124.37 [plus(s(x), y)] = [1] x + [1] y + [0] 229.29/124.37 >= [1] x + [1] y + [0] 229.29/124.37 = [s(plus(x, y))] 229.29/124.37 229.29/124.37 [plus(s(x), y)] = [1] x + [1] y + [0] 229.29/124.37 ? [1] x + [1] 229.29/124.37 = [s(plus(minus(x, y), double(y)))] 229.29/124.37 229.29/124.37 [plus(s(x), y)] = [1] x + [1] y + [0] 229.29/124.37 >= [1] x + [1] y + [0] 229.29/124.37 = [plus(x, s(y))] 229.29/124.37 229.29/124.37 229.29/124.37 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 229.29/124.37 229.29/124.37 We are left with following problem, upon which TcT provides the 229.29/124.37 certificate MAYBE. 229.29/124.37 229.29/124.37 Strict Trs: 229.29/124.37 { minus(s(x), s(y)) -> minus(x, y) 229.29/124.37 , double(0()) -> 0() 229.29/124.37 , double(s(x)) -> s(s(double(x))) 229.29/124.37 , plus(s(x), y) -> s(plus(x, y)) 229.29/124.37 , plus(s(x), y) -> s(plus(minus(x, y), double(y))) 229.29/124.37 , plus(s(x), y) -> plus(x, s(y)) } 229.29/124.37 Weak Trs: 229.29/124.37 { minus(x, 0()) -> x 229.29/124.37 , plus(0(), y) -> y } 229.29/124.37 Obligation: 229.29/124.37 innermost runtime complexity 229.29/124.37 Answer: 229.29/124.37 MAYBE 229.29/124.37 229.29/124.37 The weightgap principle applies (using the following nonconstant 229.29/124.37 growth matrix-interpretation) 229.29/124.37 229.29/124.37 The following argument positions are usable: 229.29/124.37 Uargs(s) = {1}, Uargs(plus) = {1, 2} 229.29/124.37 229.29/124.37 TcT has computed the following matrix interpretation satisfying 229.29/124.37 not(EDA) and not(IDA(1)). 229.29/124.37 229.29/124.37 [minus](x1, x2) = [1] x1 + [1] x2 + [0] 229.29/124.37 229.29/124.37 [0] = [7] 229.29/124.37 229.29/124.37 [s](x1) = [1] x1 + [4] 229.29/124.37 229.29/124.37 [double](x1) = [0] 229.29/124.37 229.29/124.37 [plus](x1, x2) = [1] x1 + [1] x2 + [0] 229.29/124.37 229.29/124.37 The order satisfies the following ordering constraints: 229.29/124.37 229.29/124.37 [minus(x, 0())] = [1] x + [7] 229.29/124.37 > [1] x + [0] 229.29/124.37 = [x] 229.29/124.37 229.29/124.37 [minus(s(x), s(y))] = [1] x + [1] y + [8] 229.29/124.37 > [1] x + [1] y + [0] 229.29/124.37 = [minus(x, y)] 229.29/124.37 229.29/124.37 [double(0())] = [0] 229.29/124.37 ? [7] 229.29/124.37 = [0()] 229.29/124.37 229.29/124.37 [double(s(x))] = [0] 229.29/124.37 ? [8] 229.29/124.37 = [s(s(double(x)))] 229.29/124.37 229.29/124.37 [plus(0(), y)] = [1] y + [7] 229.29/124.37 > [1] y + [0] 229.29/124.37 = [y] 229.29/124.37 229.29/124.37 [plus(s(x), y)] = [1] x + [1] y + [4] 229.29/124.37 >= [1] x + [1] y + [4] 229.29/124.37 = [s(plus(x, y))] 229.29/124.37 229.29/124.37 [plus(s(x), y)] = [1] x + [1] y + [4] 229.29/124.37 >= [1] x + [1] y + [4] 229.29/124.37 = [s(plus(minus(x, y), double(y)))] 229.29/124.37 229.29/124.37 [plus(s(x), y)] = [1] x + [1] y + [4] 229.29/124.37 >= [1] x + [1] y + [4] 229.29/124.37 = [plus(x, s(y))] 229.29/124.37 229.29/124.37 229.29/124.37 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 229.29/124.37 229.29/124.37 We are left with following problem, upon which TcT provides the 229.29/124.37 certificate MAYBE. 229.29/124.37 229.29/124.37 Strict Trs: 229.29/124.37 { double(0()) -> 0() 229.29/124.37 , double(s(x)) -> s(s(double(x))) 229.29/124.37 , plus(s(x), y) -> s(plus(x, y)) 229.29/124.37 , plus(s(x), y) -> s(plus(minus(x, y), double(y))) 229.29/124.37 , plus(s(x), y) -> plus(x, s(y)) } 229.29/124.37 Weak Trs: 229.29/124.37 { minus(x, 0()) -> x 229.29/124.37 , minus(s(x), s(y)) -> minus(x, y) 229.29/124.37 , plus(0(), y) -> y } 229.29/124.37 Obligation: 229.29/124.37 innermost runtime complexity 229.29/124.37 Answer: 229.29/124.37 MAYBE 229.29/124.37 229.29/124.37 The weightgap principle applies (using the following nonconstant 229.29/124.37 growth matrix-interpretation) 229.29/124.37 229.29/124.37 The following argument positions are usable: 229.29/124.37 Uargs(s) = {1}, Uargs(plus) = {1, 2} 229.29/124.37 229.29/124.37 TcT has computed the following matrix interpretation satisfying 229.29/124.37 not(EDA) and not(IDA(1)). 229.29/124.37 229.29/124.37 [minus](x1, x2) = [1] x1 + [1] x2 + [2] 229.29/124.37 229.29/124.37 [0] = [3] 229.29/124.37 229.29/124.37 [s](x1) = [1] x1 + [2] 229.29/124.37 229.29/124.37 [double](x1) = [4] 229.29/124.37 229.29/124.37 [plus](x1, x2) = [1] x1 + [1] x2 + [2] 229.29/124.37 229.29/124.37 The order satisfies the following ordering constraints: 229.29/124.37 229.29/124.37 [minus(x, 0())] = [1] x + [5] 229.29/124.37 > [1] x + [0] 229.29/124.37 = [x] 229.29/124.37 229.29/124.37 [minus(s(x), s(y))] = [1] x + [1] y + [6] 229.29/124.37 > [1] x + [1] y + [2] 229.29/124.37 = [minus(x, y)] 229.29/124.37 229.29/124.38 [double(0())] = [4] 229.29/124.38 > [3] 229.29/124.38 = [0()] 229.29/124.38 229.29/124.38 [double(s(x))] = [4] 229.29/124.38 ? [8] 229.29/124.38 = [s(s(double(x)))] 229.29/124.38 229.29/124.38 [plus(0(), y)] = [1] y + [5] 229.29/124.38 > [1] y + [0] 229.29/124.38 = [y] 229.29/124.38 229.29/124.38 [plus(s(x), y)] = [1] x + [1] y + [4] 229.29/124.38 >= [1] x + [1] y + [4] 229.29/124.38 = [s(plus(x, y))] 229.29/124.38 229.29/124.38 [plus(s(x), y)] = [1] x + [1] y + [4] 229.29/124.38 ? [1] x + [1] y + [10] 229.29/124.38 = [s(plus(minus(x, y), double(y)))] 229.29/124.38 229.29/124.38 [plus(s(x), y)] = [1] x + [1] y + [4] 229.29/124.38 >= [1] x + [1] y + [4] 229.29/124.38 = [plus(x, s(y))] 229.29/124.38 229.29/124.38 229.29/124.38 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 229.29/124.38 229.29/124.38 We are left with following problem, upon which TcT provides the 229.29/124.38 certificate MAYBE. 229.29/124.38 229.29/124.38 Strict Trs: 229.29/124.38 { double(s(x)) -> s(s(double(x))) 229.29/124.38 , plus(s(x), y) -> s(plus(x, y)) 229.29/124.38 , plus(s(x), y) -> s(plus(minus(x, y), double(y))) 229.29/124.38 , plus(s(x), y) -> plus(x, s(y)) } 229.29/124.38 Weak Trs: 229.29/124.38 { minus(x, 0()) -> x 229.29/124.38 , minus(s(x), s(y)) -> minus(x, y) 229.29/124.38 , double(0()) -> 0() 229.29/124.38 , plus(0(), y) -> y } 229.29/124.38 Obligation: 229.29/124.38 innermost runtime complexity 229.29/124.38 Answer: 229.29/124.38 MAYBE 229.29/124.38 229.29/124.38 None of the processors succeeded. 229.29/124.38 229.29/124.38 Details of failed attempt(s): 229.29/124.38 ----------------------------- 229.29/124.38 1) 'empty' failed due to the following reason: 229.29/124.38 229.29/124.38 Empty strict component of the problem is NOT empty. 229.29/124.38 229.29/124.38 2) 'With Problem ...' failed due to the following reason: 229.29/124.38 229.29/124.38 None of the processors succeeded. 229.29/124.38 229.29/124.38 Details of failed attempt(s): 229.29/124.38 ----------------------------- 229.29/124.38 1) 'empty' failed due to the following reason: 229.29/124.38 229.29/124.38 Empty strict component of the problem is NOT empty. 229.29/124.38 229.29/124.38 2) 'Fastest' failed due to the following reason: 229.29/124.38 229.29/124.38 None of the processors succeeded. 229.29/124.38 229.29/124.38 Details of failed attempt(s): 229.29/124.38 ----------------------------- 229.29/124.38 1) 'With Problem ...' failed due to the following reason: 229.29/124.38 229.29/124.38 None of the processors succeeded. 229.29/124.38 229.29/124.38 Details of failed attempt(s): 229.29/124.38 ----------------------------- 229.29/124.38 1) 'empty' failed due to the following reason: 229.29/124.38 229.29/124.38 Empty strict component of the problem is NOT empty. 229.29/124.38 229.29/124.38 2) 'With Problem ...' failed due to the following reason: 229.29/124.38 229.29/124.38 None of the processors succeeded. 229.29/124.38 229.29/124.38 Details of failed attempt(s): 229.29/124.38 ----------------------------- 229.29/124.38 1) 'empty' failed due to the following reason: 229.29/124.38 229.29/124.38 Empty strict component of the problem is NOT empty. 229.29/124.38 229.29/124.38 2) 'With Problem ...' failed due to the following reason: 229.29/124.38 229.29/124.38 None of the processors succeeded. 229.29/124.38 229.29/124.38 Details of failed attempt(s): 229.29/124.38 ----------------------------- 229.29/124.38 1) 'empty' failed due to the following reason: 229.29/124.38 229.29/124.38 Empty strict component of the problem is NOT empty. 229.29/124.38 229.29/124.38 2) 'With Problem ...' failed due to the following reason: 229.29/124.38 229.29/124.38 Empty strict component of the problem is NOT empty. 229.29/124.38 229.29/124.38 229.29/124.38 229.29/124.38 229.29/124.38 2) 'With Problem ...' failed due to the following reason: 229.29/124.38 229.29/124.38 None of the processors succeeded. 229.29/124.38 229.29/124.38 Details of failed attempt(s): 229.29/124.38 ----------------------------- 229.29/124.38 1) 'empty' failed due to the following reason: 229.29/124.38 229.29/124.38 Empty strict component of the problem is NOT empty. 229.29/124.38 229.29/124.38 2) 'With Problem ...' failed due to the following reason: 229.29/124.38 229.29/124.38 Empty strict component of the problem is NOT empty. 229.29/124.38 229.29/124.38 229.29/124.38 229.29/124.38 229.29/124.38 229.29/124.38 2) 'Best' failed due to the following reason: 229.29/124.38 229.29/124.38 None of the processors succeeded. 229.29/124.38 229.29/124.38 Details of failed attempt(s): 229.29/124.38 ----------------------------- 229.29/124.38 1) 'bsearch-popstar (timeout of 297 seconds)' failed due to the 229.29/124.38 following reason: 229.29/124.38 229.29/124.38 The input cannot be shown compatible 229.29/124.38 229.29/124.38 2) 'Polynomial Path Order (PS) (timeout of 297 seconds)' failed due 229.29/124.38 to the following reason: 229.29/124.38 229.29/124.38 The input cannot be shown compatible 229.29/124.38 229.29/124.38 229.29/124.38 3) 'Fastest (timeout of 24 seconds) (timeout of 297 seconds)' 229.29/124.38 failed due to the following reason: 229.29/124.38 229.29/124.38 None of the processors succeeded. 229.29/124.38 229.29/124.38 Details of failed attempt(s): 229.29/124.38 ----------------------------- 229.29/124.38 1) 'Bounds with minimal-enrichment and initial automaton 'match'' 229.29/124.38 failed due to the following reason: 229.29/124.38 229.29/124.38 match-boundness of the problem could not be verified. 229.29/124.38 229.29/124.38 2) 'Bounds with perSymbol-enrichment and initial automaton 'match'' 229.29/124.38 failed due to the following reason: 229.29/124.38 229.29/124.38 match-boundness of the problem could not be verified. 229.29/124.38 229.29/124.38 229.29/124.38 229.29/124.38 229.29/124.38 229.29/124.38 Arrrr.. 229.29/124.39 EOF