MAYBE 230.40/96.32 MAYBE 230.40/96.32 230.40/96.32 We are left with following problem, upon which TcT provides the 230.40/96.32 certificate MAYBE. 230.40/96.32 230.40/96.32 Strict Trs: 230.40/96.32 { plus(0(), Y) -> Y 230.40/96.32 , plus(s(X), Y) -> s(plus(X, Y)) 230.40/96.32 , min(X, 0()) -> X 230.40/96.32 , min(s(X), s(Y)) -> min(X, Y) 230.40/96.32 , min(min(X, Y), Z()) -> min(X, plus(Y, Z())) 230.40/96.32 , quot(0(), s(Y)) -> 0() 230.40/96.32 , quot(s(X), s(Y)) -> s(quot(min(X, Y), s(Y))) } 230.40/96.32 Obligation: 230.40/96.32 innermost runtime complexity 230.40/96.32 Answer: 230.40/96.32 MAYBE 230.40/96.32 230.40/96.32 None of the processors succeeded. 230.40/96.32 230.40/96.32 Details of failed attempt(s): 230.40/96.32 ----------------------------- 230.40/96.32 1) 'empty' failed due to the following reason: 230.40/96.32 230.40/96.32 Empty strict component of the problem is NOT empty. 230.40/96.32 230.40/96.32 2) 'Best' failed due to the following reason: 230.40/96.32 230.40/96.32 None of the processors succeeded. 230.40/96.32 230.40/96.32 Details of failed attempt(s): 230.40/96.32 ----------------------------- 230.40/96.32 1) 'With Problem ... (timeout of 297 seconds)' failed due to the 230.40/96.32 following reason: 230.40/96.32 230.40/96.32 We add the following dependency tuples: 230.40/96.32 230.40/96.32 Strict DPs: 230.40/96.32 { plus^#(0(), Y) -> c_1() 230.40/96.32 , plus^#(s(X), Y) -> c_2(plus^#(X, Y)) 230.40/96.32 , min^#(X, 0()) -> c_3() 230.40/96.32 , min^#(s(X), s(Y)) -> c_4(min^#(X, Y)) 230.40/96.32 , min^#(min(X, Y), Z()) -> 230.40/96.32 c_5(min^#(X, plus(Y, Z())), plus^#(Y, Z())) 230.40/96.32 , quot^#(0(), s(Y)) -> c_6() 230.40/96.32 , quot^#(s(X), s(Y)) -> c_7(quot^#(min(X, Y), s(Y)), min^#(X, Y)) } 230.40/96.32 230.40/96.32 and mark the set of starting terms. 230.40/96.32 230.40/96.32 We are left with following problem, upon which TcT provides the 230.40/96.32 certificate MAYBE. 230.40/96.32 230.40/96.32 Strict DPs: 230.40/96.32 { plus^#(0(), Y) -> c_1() 230.40/96.32 , plus^#(s(X), Y) -> c_2(plus^#(X, Y)) 230.40/96.32 , min^#(X, 0()) -> c_3() 230.40/96.32 , min^#(s(X), s(Y)) -> c_4(min^#(X, Y)) 230.40/96.32 , min^#(min(X, Y), Z()) -> 230.40/96.32 c_5(min^#(X, plus(Y, Z())), plus^#(Y, Z())) 230.40/96.32 , quot^#(0(), s(Y)) -> c_6() 230.40/96.32 , quot^#(s(X), s(Y)) -> c_7(quot^#(min(X, Y), s(Y)), min^#(X, Y)) } 230.40/96.32 Weak Trs: 230.40/96.32 { plus(0(), Y) -> Y 230.40/96.32 , plus(s(X), Y) -> s(plus(X, Y)) 230.40/96.32 , min(X, 0()) -> X 230.40/96.32 , min(s(X), s(Y)) -> min(X, Y) 230.40/96.32 , min(min(X, Y), Z()) -> min(X, plus(Y, Z())) 230.40/96.32 , quot(0(), s(Y)) -> 0() 230.40/96.32 , quot(s(X), s(Y)) -> s(quot(min(X, Y), s(Y))) } 230.40/96.32 Obligation: 230.40/96.32 innermost runtime complexity 230.40/96.32 Answer: 230.40/96.32 MAYBE 230.40/96.32 230.40/96.32 We estimate the number of application of {1,3,6} by applications of 230.40/96.32 Pre({1,3,6}) = {2,4,5,7}. Here rules are labeled as follows: 230.40/96.32 230.40/96.32 DPs: 230.40/96.32 { 1: plus^#(0(), Y) -> c_1() 230.40/96.32 , 2: plus^#(s(X), Y) -> c_2(plus^#(X, Y)) 230.40/96.32 , 3: min^#(X, 0()) -> c_3() 230.40/96.32 , 4: min^#(s(X), s(Y)) -> c_4(min^#(X, Y)) 230.40/96.32 , 5: min^#(min(X, Y), Z()) -> 230.40/96.32 c_5(min^#(X, plus(Y, Z())), plus^#(Y, Z())) 230.40/96.32 , 6: quot^#(0(), s(Y)) -> c_6() 230.40/96.32 , 7: quot^#(s(X), s(Y)) -> 230.40/96.32 c_7(quot^#(min(X, Y), s(Y)), min^#(X, Y)) } 230.40/96.32 230.40/96.32 We are left with following problem, upon which TcT provides the 230.40/96.32 certificate MAYBE. 230.40/96.32 230.40/96.32 Strict DPs: 230.40/96.32 { plus^#(s(X), Y) -> c_2(plus^#(X, Y)) 230.40/96.32 , min^#(s(X), s(Y)) -> c_4(min^#(X, Y)) 230.40/96.32 , min^#(min(X, Y), Z()) -> 230.40/96.32 c_5(min^#(X, plus(Y, Z())), plus^#(Y, Z())) 230.40/96.32 , quot^#(s(X), s(Y)) -> c_7(quot^#(min(X, Y), s(Y)), min^#(X, Y)) } 230.40/96.32 Weak DPs: 230.40/96.32 { plus^#(0(), Y) -> c_1() 230.40/96.32 , min^#(X, 0()) -> c_3() 230.40/96.32 , quot^#(0(), s(Y)) -> c_6() } 230.40/96.32 Weak Trs: 230.40/96.32 { plus(0(), Y) -> Y 230.40/96.32 , plus(s(X), Y) -> s(plus(X, Y)) 230.40/96.32 , min(X, 0()) -> X 230.40/96.32 , min(s(X), s(Y)) -> min(X, Y) 230.40/96.32 , min(min(X, Y), Z()) -> min(X, plus(Y, Z())) 230.40/96.32 , quot(0(), s(Y)) -> 0() 230.40/96.32 , quot(s(X), s(Y)) -> s(quot(min(X, Y), s(Y))) } 230.40/96.32 Obligation: 230.40/96.32 innermost runtime complexity 230.40/96.32 Answer: 230.40/96.32 MAYBE 230.40/96.32 230.40/96.32 The following weak DPs constitute a sub-graph of the DG that is 230.40/96.32 closed under successors. The DPs are removed. 230.40/96.32 230.40/96.32 { plus^#(0(), Y) -> c_1() 230.40/96.32 , min^#(X, 0()) -> c_3() 230.40/96.32 , quot^#(0(), s(Y)) -> c_6() } 230.40/96.32 230.40/96.32 We are left with following problem, upon which TcT provides the 230.40/96.32 certificate MAYBE. 230.40/96.32 230.40/96.32 Strict DPs: 230.40/96.32 { plus^#(s(X), Y) -> c_2(plus^#(X, Y)) 230.40/96.32 , min^#(s(X), s(Y)) -> c_4(min^#(X, Y)) 230.40/96.32 , min^#(min(X, Y), Z()) -> 230.40/96.32 c_5(min^#(X, plus(Y, Z())), plus^#(Y, Z())) 230.40/96.32 , quot^#(s(X), s(Y)) -> c_7(quot^#(min(X, Y), s(Y)), min^#(X, Y)) } 230.40/96.32 Weak Trs: 230.40/96.32 { plus(0(), Y) -> Y 230.40/96.32 , plus(s(X), Y) -> s(plus(X, Y)) 230.40/96.32 , min(X, 0()) -> X 230.40/96.32 , min(s(X), s(Y)) -> min(X, Y) 230.40/96.32 , min(min(X, Y), Z()) -> min(X, plus(Y, Z())) 230.40/96.32 , quot(0(), s(Y)) -> 0() 230.40/96.32 , quot(s(X), s(Y)) -> s(quot(min(X, Y), s(Y))) } 230.40/96.32 Obligation: 230.40/96.32 innermost runtime complexity 230.40/96.32 Answer: 230.40/96.32 MAYBE 230.40/96.32 230.40/96.32 We replace rewrite rules by usable rules: 230.40/96.32 230.40/96.32 Weak Usable Rules: 230.40/96.32 { plus(0(), Y) -> Y 230.40/96.32 , plus(s(X), Y) -> s(plus(X, Y)) 230.40/96.32 , min(X, 0()) -> X 230.40/96.32 , min(s(X), s(Y)) -> min(X, Y) 230.40/96.32 , min(min(X, Y), Z()) -> min(X, plus(Y, Z())) } 230.40/96.32 230.40/96.32 We are left with following problem, upon which TcT provides the 230.40/96.32 certificate MAYBE. 230.40/96.32 230.40/96.32 Strict DPs: 230.40/96.32 { plus^#(s(X), Y) -> c_2(plus^#(X, Y)) 230.40/96.32 , min^#(s(X), s(Y)) -> c_4(min^#(X, Y)) 230.40/96.32 , min^#(min(X, Y), Z()) -> 230.40/96.32 c_5(min^#(X, plus(Y, Z())), plus^#(Y, Z())) 230.40/96.32 , quot^#(s(X), s(Y)) -> c_7(quot^#(min(X, Y), s(Y)), min^#(X, Y)) } 230.40/96.32 Weak Trs: 230.40/96.32 { plus(0(), Y) -> Y 230.40/96.32 , plus(s(X), Y) -> s(plus(X, Y)) 230.40/96.32 , min(X, 0()) -> X 230.40/96.32 , min(s(X), s(Y)) -> min(X, Y) 230.40/96.32 , min(min(X, Y), Z()) -> min(X, plus(Y, Z())) } 230.40/96.32 Obligation: 230.40/96.32 innermost runtime complexity 230.40/96.32 Answer: 230.40/96.32 MAYBE 230.40/96.32 230.40/96.32 None of the processors succeeded. 230.40/96.32 230.40/96.32 Details of failed attempt(s): 230.40/96.32 ----------------------------- 230.40/96.32 1) 'empty' failed due to the following reason: 230.40/96.32 230.40/96.32 Empty strict component of the problem is NOT empty. 230.40/96.32 230.40/96.32 2) 'With Problem ...' failed due to the following reason: 230.40/96.32 230.40/96.32 We decompose the input problem according to the dependency graph 230.40/96.32 into the upper component 230.40/96.32 230.40/96.32 { quot^#(s(X), s(Y)) -> c_7(quot^#(min(X, Y), s(Y)), min^#(X, Y)) } 230.40/96.32 230.40/96.32 and lower component 230.40/96.32 230.40/96.32 { plus^#(s(X), Y) -> c_2(plus^#(X, Y)) 230.40/96.32 , min^#(s(X), s(Y)) -> c_4(min^#(X, Y)) 230.40/96.32 , min^#(min(X, Y), Z()) -> 230.40/96.32 c_5(min^#(X, plus(Y, Z())), plus^#(Y, Z())) } 230.40/96.32 230.40/96.32 Further, following extension rules are added to the lower 230.40/96.32 component. 230.40/96.32 230.40/96.32 { quot^#(s(X), s(Y)) -> min^#(X, Y) 230.40/96.32 , quot^#(s(X), s(Y)) -> quot^#(min(X, Y), s(Y)) } 230.40/96.32 230.40/96.32 TcT solves the upper component with certificate YES(O(1),O(n^1)). 230.40/96.32 230.40/96.32 Sub-proof: 230.40/96.32 ---------- 230.40/96.32 We are left with following problem, upon which TcT provides the 230.40/96.32 certificate YES(O(1),O(n^1)). 230.40/96.32 230.40/96.32 Strict DPs: 230.40/96.32 { quot^#(s(X), s(Y)) -> c_7(quot^#(min(X, Y), s(Y)), min^#(X, Y)) } 230.40/96.32 Weak Trs: 230.40/96.32 { plus(0(), Y) -> Y 230.40/96.32 , plus(s(X), Y) -> s(plus(X, Y)) 230.40/96.32 , min(X, 0()) -> X 230.40/96.32 , min(s(X), s(Y)) -> min(X, Y) 230.40/96.32 , min(min(X, Y), Z()) -> min(X, plus(Y, Z())) } 230.40/96.32 Obligation: 230.40/96.32 innermost runtime complexity 230.40/96.32 Answer: 230.40/96.32 YES(O(1),O(n^1)) 230.40/96.32 230.40/96.32 We use the processor 'Small Polynomial Path Order (PS,1-bounded)' 230.40/96.32 to orient following rules strictly. 230.40/96.32 230.40/96.32 DPs: 230.40/96.32 { 1: quot^#(s(X), s(Y)) -> 230.40/96.32 c_7(quot^#(min(X, Y), s(Y)), min^#(X, Y)) } 230.40/96.32 Trs: { min(s(X), s(Y)) -> min(X, Y) } 230.40/96.32 230.40/96.32 Sub-proof: 230.40/96.32 ---------- 230.40/96.32 The input was oriented with the instance of 'Small Polynomial Path 230.40/96.32 Order (PS,1-bounded)' as induced by the safe mapping 230.40/96.32 230.40/96.32 safe(plus) = {1}, safe(0) = {}, safe(s) = {1}, safe(min) = {1, 2}, 230.40/96.32 safe(Z) = {}, safe(min^#) = {}, safe(quot^#) = {}, safe(c_7) = {} 230.40/96.32 230.40/96.32 and precedence 230.40/96.32 230.40/96.33 empty . 230.40/96.33 230.40/96.33 Following symbols are considered recursive: 230.40/96.33 230.40/96.33 {plus, quot^#} 230.40/96.33 230.40/96.33 The recursion depth is 1. 230.40/96.33 230.40/96.33 Further, following argument filtering is employed: 230.40/96.33 230.40/96.33 pi(plus) = 2, pi(0) = [], pi(s) = [1], pi(min) = 1, pi(Z) = [], 230.40/96.33 pi(min^#) = [], pi(quot^#) = [1, 2], pi(c_7) = [1, 2] 230.40/96.33 230.40/96.33 Usable defined function symbols are a subset of: 230.40/96.33 230.40/96.33 {min, min^#, quot^#} 230.40/96.33 230.40/96.33 For your convenience, here are the satisfied ordering constraints: 230.40/96.33 230.40/96.33 pi(quot^#(s(X), s(Y))) = quot^#(s(; X), s(; Y);) 230.40/96.33 > c_7(quot^#(X, s(; Y);), min^#();) 230.40/96.33 = pi(c_7(quot^#(min(X, Y), s(Y)), min^#(X, Y))) 230.40/96.33 230.40/96.33 pi(min(X, 0())) = X 230.40/96.33 >= X 230.40/96.33 = pi(X) 230.40/96.33 230.40/96.33 pi(min(s(X), s(Y))) = s(; X) 230.40/96.33 > X 230.40/96.33 = pi(min(X, Y)) 230.40/96.33 230.40/96.33 pi(min(min(X, Y), Z())) = X 230.40/96.33 >= X 230.40/96.33 = pi(min(X, plus(Y, Z()))) 230.40/96.33 230.40/96.33 230.40/96.33 The strictly oriented rules are moved into the weak component. 230.40/96.33 230.40/96.33 We are left with following problem, upon which TcT provides the 230.40/96.33 certificate YES(O(1),O(1)). 230.40/96.33 230.40/96.33 Weak DPs: 230.40/96.33 { quot^#(s(X), s(Y)) -> c_7(quot^#(min(X, Y), s(Y)), min^#(X, Y)) } 230.40/96.33 Weak Trs: 230.40/96.33 { plus(0(), Y) -> Y 230.40/96.33 , plus(s(X), Y) -> s(plus(X, Y)) 230.40/96.33 , min(X, 0()) -> X 230.40/96.33 , min(s(X), s(Y)) -> min(X, Y) 230.40/96.33 , min(min(X, Y), Z()) -> min(X, plus(Y, Z())) } 230.40/96.33 Obligation: 230.40/96.33 innermost runtime complexity 230.40/96.33 Answer: 230.40/96.33 YES(O(1),O(1)) 230.40/96.33 230.40/96.33 The following weak DPs constitute a sub-graph of the DG that is 230.40/96.33 closed under successors. The DPs are removed. 230.40/96.33 230.40/96.33 { quot^#(s(X), s(Y)) -> c_7(quot^#(min(X, Y), s(Y)), min^#(X, Y)) } 230.40/96.33 230.40/96.33 We are left with following problem, upon which TcT provides the 230.40/96.33 certificate YES(O(1),O(1)). 230.40/96.33 230.40/96.33 Weak Trs: 230.40/96.33 { plus(0(), Y) -> Y 230.40/96.33 , plus(s(X), Y) -> s(plus(X, Y)) 230.40/96.33 , min(X, 0()) -> X 230.40/96.33 , min(s(X), s(Y)) -> min(X, Y) 230.40/96.33 , min(min(X, Y), Z()) -> min(X, plus(Y, Z())) } 230.40/96.33 Obligation: 230.40/96.33 innermost runtime complexity 230.40/96.33 Answer: 230.40/96.33 YES(O(1),O(1)) 230.40/96.33 230.40/96.33 No rule is usable, rules are removed from the input problem. 230.40/96.33 230.40/96.33 We are left with following problem, upon which TcT provides the 230.40/96.33 certificate YES(O(1),O(1)). 230.40/96.33 230.40/96.33 Rules: Empty 230.40/96.33 Obligation: 230.40/96.33 innermost runtime complexity 230.40/96.33 Answer: 230.40/96.33 YES(O(1),O(1)) 230.40/96.33 230.40/96.33 Empty rules are trivially bounded 230.40/96.33 230.40/96.33 We return to the main proof. 230.40/96.33 230.40/96.33 We are left with following problem, upon which TcT provides the 230.40/96.33 certificate MAYBE. 230.40/96.33 230.40/96.33 Strict DPs: 230.40/96.33 { plus^#(s(X), Y) -> c_2(plus^#(X, Y)) 230.40/96.33 , min^#(s(X), s(Y)) -> c_4(min^#(X, Y)) 230.40/96.33 , min^#(min(X, Y), Z()) -> 230.40/96.33 c_5(min^#(X, plus(Y, Z())), plus^#(Y, Z())) } 230.40/96.33 Weak DPs: 230.40/96.33 { quot^#(s(X), s(Y)) -> min^#(X, Y) 230.40/96.33 , quot^#(s(X), s(Y)) -> quot^#(min(X, Y), s(Y)) } 230.40/96.33 Weak Trs: 230.40/96.33 { plus(0(), Y) -> Y 230.40/96.33 , plus(s(X), Y) -> s(plus(X, Y)) 230.40/96.33 , min(X, 0()) -> X 230.40/96.33 , min(s(X), s(Y)) -> min(X, Y) 230.40/96.33 , min(min(X, Y), Z()) -> min(X, plus(Y, Z())) } 230.40/96.33 Obligation: 230.40/96.33 innermost runtime complexity 230.40/96.33 Answer: 230.40/96.33 MAYBE 230.40/96.33 230.40/96.33 We decompose the input problem according to the dependency graph 230.40/96.33 into the upper component 230.40/96.33 230.40/96.33 { min^#(s(X), s(Y)) -> c_4(min^#(X, Y)) 230.40/96.33 , min^#(min(X, Y), Z()) -> 230.40/96.33 c_5(min^#(X, plus(Y, Z())), plus^#(Y, Z())) 230.40/96.33 , quot^#(s(X), s(Y)) -> min^#(X, Y) 230.40/96.33 , quot^#(s(X), s(Y)) -> quot^#(min(X, Y), s(Y)) } 230.40/96.33 230.40/96.33 and lower component 230.40/96.33 230.40/96.33 { plus^#(s(X), Y) -> c_2(plus^#(X, Y)) } 230.40/96.33 230.40/96.33 Further, following extension rules are added to the lower 230.40/96.33 component. 230.40/96.33 230.40/96.33 { min^#(s(X), s(Y)) -> min^#(X, Y) 230.40/96.33 , min^#(min(X, Y), Z()) -> plus^#(Y, Z()) 230.40/96.33 , min^#(min(X, Y), Z()) -> min^#(X, plus(Y, Z())) 230.40/96.33 , quot^#(s(X), s(Y)) -> min^#(X, Y) 230.40/96.33 , quot^#(s(X), s(Y)) -> quot^#(min(X, Y), s(Y)) } 230.40/96.33 230.40/96.33 TcT solves the upper component with certificate YES(O(1),O(n^1)). 230.40/96.33 230.40/96.33 Sub-proof: 230.40/96.33 ---------- 230.40/96.33 We are left with following problem, upon which TcT provides the 230.40/96.33 certificate YES(O(1),O(n^1)). 230.40/96.33 230.40/96.33 Strict DPs: 230.40/96.33 { min^#(s(X), s(Y)) -> c_4(min^#(X, Y)) 230.40/96.33 , min^#(min(X, Y), Z()) -> 230.40/96.33 c_5(min^#(X, plus(Y, Z())), plus^#(Y, Z())) } 230.40/96.33 Weak DPs: 230.40/96.33 { quot^#(s(X), s(Y)) -> min^#(X, Y) 230.40/96.33 , quot^#(s(X), s(Y)) -> quot^#(min(X, Y), s(Y)) } 230.40/96.33 Weak Trs: 230.40/96.33 { plus(0(), Y) -> Y 230.40/96.33 , plus(s(X), Y) -> s(plus(X, Y)) 230.40/96.33 , min(X, 0()) -> X 230.40/96.33 , min(s(X), s(Y)) -> min(X, Y) 230.40/96.33 , min(min(X, Y), Z()) -> min(X, plus(Y, Z())) } 230.40/96.33 Obligation: 230.40/96.33 innermost runtime complexity 230.40/96.33 Answer: 230.40/96.33 YES(O(1),O(n^1)) 230.40/96.33 230.40/96.33 We use the processor 'Small Polynomial Path Order (PS,1-bounded)' 230.40/96.33 to orient following rules strictly. 230.40/96.33 230.40/96.33 DPs: 230.40/96.33 { 1: min^#(s(X), s(Y)) -> c_4(min^#(X, Y)) 230.40/96.33 , 2: min^#(min(X, Y), Z()) -> 230.40/96.33 c_5(min^#(X, plus(Y, Z())), plus^#(Y, Z())) 230.40/96.33 , 3: quot^#(s(X), s(Y)) -> min^#(X, Y) } 230.40/96.33 Trs: 230.40/96.33 { min(X, 0()) -> X 230.40/96.33 , min(s(X), s(Y)) -> min(X, Y) 230.40/96.33 , min(min(X, Y), Z()) -> min(X, plus(Y, Z())) } 230.40/96.33 230.40/96.33 Sub-proof: 230.40/96.33 ---------- 230.40/96.33 The input was oriented with the instance of 'Small Polynomial Path 230.40/96.33 Order (PS,1-bounded)' as induced by the safe mapping 230.40/96.33 230.40/96.33 safe(plus) = {}, safe(0) = {}, safe(s) = {1}, safe(min) = {1, 2}, 230.40/96.33 safe(Z) = {}, safe(plus^#) = {}, safe(min^#) = {2}, safe(c_4) = {}, 230.40/96.33 safe(c_5) = {}, safe(quot^#) = {} 230.40/96.33 230.40/96.33 and precedence 230.40/96.33 230.40/96.33 quot^# > plus, quot^# > min^#, plus ~ min^# . 230.40/96.33 230.40/96.33 Following symbols are considered recursive: 230.40/96.33 230.40/96.33 {min^#} 230.40/96.33 230.40/96.33 The recursion depth is 1. 230.40/96.33 230.40/96.33 Further, following argument filtering is employed: 230.40/96.33 230.40/96.33 pi(plus) = [], pi(0) = [], pi(s) = [1], pi(min) = [1], pi(Z) = [], 230.40/96.33 pi(plus^#) = [2], pi(min^#) = [1], pi(c_4) = [1], pi(c_5) = [1, 2], 230.40/96.33 pi(quot^#) = [1] 230.40/96.33 230.40/96.33 Usable defined function symbols are a subset of: 230.40/96.33 230.40/96.33 {min, plus^#, min^#, quot^#} 230.40/96.33 230.40/96.33 For your convenience, here are the satisfied ordering constraints: 230.40/96.33 230.40/96.33 pi(min^#(s(X), s(Y))) = min^#(s(; X);) 230.40/96.33 > c_4(min^#(X;);) 230.40/96.33 = pi(c_4(min^#(X, Y))) 230.40/96.33 230.40/96.33 pi(min^#(min(X, Y), Z())) = min^#(min(; X);) 230.40/96.33 > c_5(min^#(X;), plus^#(Z(););) 230.40/96.33 = pi(c_5(min^#(X, plus(Y, Z())), plus^#(Y, Z()))) 230.40/96.33 230.40/96.33 pi(quot^#(s(X), s(Y))) = quot^#(s(; X);) 230.40/96.33 > min^#(X;) 230.40/96.33 = pi(min^#(X, Y)) 230.40/96.33 230.40/96.33 pi(quot^#(s(X), s(Y))) = quot^#(s(; X);) 230.40/96.33 >= quot^#(min(; X);) 230.40/96.33 = pi(quot^#(min(X, Y), s(Y))) 230.40/96.33 230.40/96.33 pi(min(X, 0())) = min(; X) 230.40/96.33 > X 230.40/96.33 = pi(X) 230.40/96.33 230.40/96.33 pi(min(s(X), s(Y))) = min(; s(; X)) 230.40/96.33 > min(; X) 230.40/96.33 = pi(min(X, Y)) 230.40/96.33 230.40/96.33 pi(min(min(X, Y), Z())) = min(; min(; X)) 230.40/96.33 > min(; X) 230.40/96.33 = pi(min(X, plus(Y, Z()))) 230.40/96.33 230.40/96.33 230.40/96.33 The strictly oriented rules are moved into the weak component. 230.40/96.33 230.40/96.33 We are left with following problem, upon which TcT provides the 230.40/96.33 certificate YES(O(1),O(1)). 230.40/96.33 230.40/96.33 Weak DPs: 230.40/96.33 { min^#(s(X), s(Y)) -> c_4(min^#(X, Y)) 230.40/96.33 , min^#(min(X, Y), Z()) -> 230.40/96.33 c_5(min^#(X, plus(Y, Z())), plus^#(Y, Z())) 230.40/96.33 , quot^#(s(X), s(Y)) -> min^#(X, Y) 230.40/96.33 , quot^#(s(X), s(Y)) -> quot^#(min(X, Y), s(Y)) } 230.40/96.33 Weak Trs: 230.40/96.33 { plus(0(), Y) -> Y 230.40/96.33 , plus(s(X), Y) -> s(plus(X, Y)) 230.40/96.33 , min(X, 0()) -> X 230.40/96.33 , min(s(X), s(Y)) -> min(X, Y) 230.40/96.33 , min(min(X, Y), Z()) -> min(X, plus(Y, Z())) } 230.40/96.33 Obligation: 230.40/96.33 innermost runtime complexity 230.40/96.33 Answer: 230.40/96.33 YES(O(1),O(1)) 230.40/96.33 230.40/96.33 The following weak DPs constitute a sub-graph of the DG that is 230.40/96.33 closed under successors. The DPs are removed. 230.40/96.33 230.40/96.33 { min^#(s(X), s(Y)) -> c_4(min^#(X, Y)) 230.40/96.33 , min^#(min(X, Y), Z()) -> 230.40/96.33 c_5(min^#(X, plus(Y, Z())), plus^#(Y, Z())) 230.40/96.33 , quot^#(s(X), s(Y)) -> min^#(X, Y) 230.40/96.33 , quot^#(s(X), s(Y)) -> quot^#(min(X, Y), s(Y)) } 230.40/96.33 230.40/96.33 We are left with following problem, upon which TcT provides the 230.40/96.33 certificate YES(O(1),O(1)). 230.40/96.33 230.40/96.33 Weak Trs: 230.40/96.33 { plus(0(), Y) -> Y 230.40/96.33 , plus(s(X), Y) -> s(plus(X, Y)) 230.40/96.33 , min(X, 0()) -> X 230.40/96.33 , min(s(X), s(Y)) -> min(X, Y) 230.40/96.33 , min(min(X, Y), Z()) -> min(X, plus(Y, Z())) } 230.40/96.33 Obligation: 230.40/96.33 innermost runtime complexity 230.40/96.33 Answer: 230.40/96.33 YES(O(1),O(1)) 230.40/96.33 230.40/96.33 No rule is usable, rules are removed from the input problem. 230.40/96.33 230.40/96.33 We are left with following problem, upon which TcT provides the 230.40/96.33 certificate YES(O(1),O(1)). 230.40/96.33 230.40/96.33 Rules: Empty 230.40/96.33 Obligation: 230.40/96.33 innermost runtime complexity 230.40/96.33 Answer: 230.40/96.33 YES(O(1),O(1)) 230.40/96.33 230.40/96.33 Empty rules are trivially bounded 230.40/96.33 230.40/96.33 We return to the main proof. 230.40/96.33 230.40/96.33 We are left with following problem, upon which TcT provides the 230.40/96.33 certificate MAYBE. 230.40/96.33 230.40/96.33 Strict DPs: { plus^#(s(X), Y) -> c_2(plus^#(X, Y)) } 230.40/96.33 Weak DPs: 230.40/96.33 { min^#(s(X), s(Y)) -> min^#(X, Y) 230.40/96.33 , min^#(min(X, Y), Z()) -> plus^#(Y, Z()) 230.40/96.33 , min^#(min(X, Y), Z()) -> min^#(X, plus(Y, Z())) 230.40/96.33 , quot^#(s(X), s(Y)) -> min^#(X, Y) 230.40/96.33 , quot^#(s(X), s(Y)) -> quot^#(min(X, Y), s(Y)) } 230.40/96.33 Weak Trs: 230.40/96.33 { plus(0(), Y) -> Y 230.40/96.33 , plus(s(X), Y) -> s(plus(X, Y)) 230.40/96.33 , min(X, 0()) -> X 230.40/96.33 , min(s(X), s(Y)) -> min(X, Y) 230.40/96.33 , min(min(X, Y), Z()) -> min(X, plus(Y, Z())) } 230.40/96.33 Obligation: 230.40/96.33 innermost runtime complexity 230.40/96.33 Answer: 230.40/96.33 MAYBE 230.40/96.33 230.40/96.33 None of the processors succeeded. 230.40/96.33 230.40/96.33 Details of failed attempt(s): 230.40/96.33 ----------------------------- 230.40/96.33 1) 'empty' failed due to the following reason: 230.40/96.33 230.40/96.33 Empty strict component of the problem is NOT empty. 230.40/96.33 230.40/96.33 2) 'Fastest' failed due to the following reason: 230.40/96.33 230.40/96.33 None of the processors succeeded. 230.40/96.33 230.40/96.33 Details of failed attempt(s): 230.40/96.33 ----------------------------- 230.40/96.33 1) 'With Problem ...' failed due to the following reason: 230.40/96.33 230.40/96.33 None of the processors succeeded. 230.40/96.33 230.40/96.33 Details of failed attempt(s): 230.40/96.33 ----------------------------- 230.40/96.33 1) 'empty' failed due to the following reason: 230.40/96.33 230.40/96.33 Empty strict component of the problem is NOT empty. 230.40/96.33 230.40/96.33 2) 'Polynomial Path Order (PS)' failed due to the following reason: 230.40/96.33 230.40/96.33 The input cannot be shown compatible 230.40/96.33 230.40/96.33 230.40/96.33 2) 'Polynomial Path Order (PS)' failed due to the following reason: 230.40/96.33 230.40/96.33 The input cannot be shown compatible 230.40/96.33 230.40/96.33 3) 'Fastest (timeout of 24 seconds)' failed due to the following 230.40/96.33 reason: 230.40/96.33 230.40/96.33 None of the processors succeeded. 230.40/96.33 230.40/96.33 Details of failed attempt(s): 230.40/96.33 ----------------------------- 230.40/96.33 1) 'Bounds with minimal-enrichment and initial automaton 'match'' 230.40/96.33 failed due to the following reason: 230.40/96.33 230.40/96.33 match-boundness of the problem could not be verified. 230.40/96.33 230.40/96.33 2) 'Bounds with perSymbol-enrichment and initial automaton 'match'' 230.40/96.33 failed due to the following reason: 230.40/96.33 230.40/96.33 match-boundness of the problem could not be verified. 230.40/96.33 230.40/96.33 230.40/96.33 230.40/96.33 230.40/96.33 230.40/96.33 2) 'Best' failed due to the following reason: 230.40/96.33 230.40/96.33 None of the processors succeeded. 230.40/96.33 230.40/96.33 Details of failed attempt(s): 230.40/96.33 ----------------------------- 230.40/96.33 1) 'With Problem ... (timeout of 148 seconds) (timeout of 297 230.40/96.33 seconds)' failed due to the following reason: 230.40/96.33 230.40/96.33 None of the processors succeeded. 230.40/96.33 230.40/96.33 Details of failed attempt(s): 230.40/96.33 ----------------------------- 230.40/96.33 1) 'empty' failed due to the following reason: 230.40/96.33 230.40/96.33 Empty strict component of the problem is NOT empty. 230.40/96.33 230.40/96.33 2) 'With Problem ...' failed due to the following reason: 230.40/96.33 230.40/96.33 None of the processors succeeded. 230.40/96.33 230.40/96.33 Details of failed attempt(s): 230.40/96.33 ----------------------------- 230.40/96.33 1) 'empty' failed due to the following reason: 230.40/96.33 230.40/96.33 Empty strict component of the problem is NOT empty. 230.40/96.33 230.40/96.33 2) 'Fastest' failed due to the following reason: 230.40/96.33 230.40/96.33 None of the processors succeeded. 230.40/96.33 230.40/96.33 Details of failed attempt(s): 230.40/96.33 ----------------------------- 230.40/96.33 1) 'With Problem ...' failed due to the following reason: 230.40/96.33 230.40/96.33 None of the processors succeeded. 230.40/96.33 230.40/96.33 Details of failed attempt(s): 230.40/96.33 ----------------------------- 230.40/96.33 1) 'empty' failed due to the following reason: 230.40/96.33 230.40/96.33 Empty strict component of the problem is NOT empty. 230.40/96.33 230.40/96.33 2) 'With Problem ...' failed due to the following reason: 230.40/96.33 230.40/96.33 Empty strict component of the problem is NOT empty. 230.40/96.33 230.40/96.33 230.40/96.33 2) 'With Problem ...' failed due to the following reason: 230.40/96.33 230.40/96.33 None of the processors succeeded. 230.40/96.33 230.40/96.33 Details of failed attempt(s): 230.40/96.33 ----------------------------- 230.40/96.33 1) 'empty' failed due to the following reason: 230.40/96.33 230.40/96.33 Empty strict component of the problem is NOT empty. 230.40/96.33 230.40/96.33 2) 'With Problem ...' failed due to the following reason: 230.40/96.33 230.40/96.33 None of the processors succeeded. 230.40/96.33 230.40/96.33 Details of failed attempt(s): 230.40/96.33 ----------------------------- 230.40/96.33 1) 'empty' failed due to the following reason: 230.40/96.33 230.40/96.33 Empty strict component of the problem is NOT empty. 230.40/96.33 230.40/96.33 2) 'With Problem ...' failed due to the following reason: 230.40/96.33 230.40/96.33 None of the processors succeeded. 230.40/96.33 230.40/96.33 Details of failed attempt(s): 230.40/96.33 ----------------------------- 230.40/96.33 1) 'empty' failed due to the following reason: 230.40/96.33 230.40/96.33 Empty strict component of the problem is NOT empty. 230.40/96.33 230.40/96.33 2) 'With Problem ...' failed due to the following reason: 230.40/96.33 230.40/96.33 Empty strict component of the problem is NOT empty. 230.40/96.33 230.40/96.33 230.40/96.33 230.40/96.33 230.40/96.33 230.40/96.33 230.40/96.33 230.40/96.33 2) 'Best' failed due to the following reason: 230.40/96.33 230.40/96.33 None of the processors succeeded. 230.40/96.33 230.40/96.33 Details of failed attempt(s): 230.40/96.33 ----------------------------- 230.40/96.33 1) 'Polynomial Path Order (PS) (timeout of 297 seconds)' failed due 230.40/96.33 to the following reason: 230.40/96.33 230.40/96.33 The input cannot be shown compatible 230.40/96.33 230.40/96.33 2) 'bsearch-popstar (timeout of 297 seconds)' failed due to the 230.40/96.33 following reason: 230.40/96.33 230.40/96.33 The input cannot be shown compatible 230.40/96.33 230.40/96.33 230.40/96.33 3) 'Fastest (timeout of 24 seconds) (timeout of 297 seconds)' 230.40/96.33 failed due to the following reason: 230.40/96.33 230.40/96.33 None of the processors succeeded. 230.40/96.33 230.40/96.33 Details of failed attempt(s): 230.40/96.33 ----------------------------- 230.40/96.33 1) 'Bounds with minimal-enrichment and initial automaton 'match'' 230.40/96.33 failed due to the following reason: 230.40/96.33 230.40/96.33 match-boundness of the problem could not be verified. 230.40/96.33 230.40/96.33 2) 'Bounds with perSymbol-enrichment and initial automaton 'match'' 230.40/96.33 failed due to the following reason: 230.40/96.33 230.40/96.33 match-boundness of the problem could not be verified. 230.40/96.33 230.40/96.33 230.40/96.33 230.40/96.33 230.40/96.33 230.40/96.33 Arrrr.. 230.52/96.43 EOF