MAYBE 365.83/104.63 MAYBE 365.83/104.63 365.83/104.63 We are left with following problem, upon which TcT provides the 365.83/104.63 certificate MAYBE. 365.83/104.63 365.83/104.63 Strict Trs: 365.83/104.63 { log(s(x1)) -> s(log(half(s(x1)))) 365.83/104.63 , s(s(p(s(x1)))) -> s(s(x1)) 365.83/104.63 , half(s(s(x1))) -> s(half(p(s(s(x1))))) 365.83/104.63 , half(s(0(x1))) -> 0(x1) 365.83/104.63 , half(half(s(s(s(s(x1)))))) -> s(s(half(half(x1)))) 365.83/104.63 , half(0(x1)) -> 0(s(s(half(x1)))) 365.83/104.63 , 0(x1) -> x1 365.83/104.63 , p(s(s(s(x1)))) -> s(p(s(s(x1)))) } 365.83/104.63 Obligation: 365.83/104.63 derivational complexity 365.83/104.63 Answer: 365.83/104.63 MAYBE 365.83/104.63 365.83/104.63 None of the processors succeeded. 365.83/104.63 365.83/104.63 Details of failed attempt(s): 365.83/104.63 ----------------------------- 365.83/104.63 1) 'Inspecting Problem... (timeout of 297 seconds)' failed due to 365.83/104.63 the following reason: 365.83/104.63 365.83/104.63 The weightgap principle applies (using the following nonconstant 365.83/104.63 growth matrix-interpretation) 365.83/104.63 365.83/104.63 TcT has computed the following triangular matrix interpretation. 365.83/104.63 Note that the diagonal of the component-wise maxima of 365.83/104.63 interpretation-entries contains no more than 1 non-zero entries. 365.83/104.63 365.83/104.63 [log](x1) = [1] x1 + [0] 365.83/104.63 365.83/104.63 [s](x1) = [1] x1 + [0] 365.83/104.63 365.83/104.63 [half](x1) = [1] x1 + [0] 365.83/104.63 365.83/104.63 [0](x1) = [1] x1 + [1] 365.83/104.63 365.83/104.63 [p](x1) = [1] x1 + [0] 365.83/104.63 365.83/104.63 The order satisfies the following ordering constraints: 365.83/104.63 365.83/104.63 [log(s(x1))] = [1] x1 + [0] 365.83/104.63 >= [1] x1 + [0] 365.83/104.63 = [s(log(half(s(x1))))] 365.83/104.63 365.83/104.63 [s(s(p(s(x1))))] = [1] x1 + [0] 365.83/104.63 >= [1] x1 + [0] 365.83/104.63 = [s(s(x1))] 365.83/104.63 365.83/104.63 [half(s(s(x1)))] = [1] x1 + [0] 365.83/104.63 >= [1] x1 + [0] 365.83/104.63 = [s(half(p(s(s(x1)))))] 365.83/104.63 365.83/104.63 [half(s(0(x1)))] = [1] x1 + [1] 365.83/104.63 >= [1] x1 + [1] 365.83/104.63 = [0(x1)] 365.83/104.63 365.83/104.63 [half(half(s(s(s(s(x1))))))] = [1] x1 + [0] 365.83/104.63 >= [1] x1 + [0] 365.83/104.63 = [s(s(half(half(x1))))] 365.83/104.63 365.83/104.63 [half(0(x1))] = [1] x1 + [1] 365.83/104.63 >= [1] x1 + [1] 365.83/104.63 = [0(s(s(half(x1))))] 365.83/104.63 365.83/104.63 [0(x1)] = [1] x1 + [1] 365.83/104.63 > [1] x1 + [0] 365.83/104.63 = [x1] 365.83/104.63 365.83/104.63 [p(s(s(s(x1))))] = [1] x1 + [0] 365.83/104.63 >= [1] x1 + [0] 365.83/104.63 = [s(p(s(s(x1))))] 365.83/104.63 365.83/104.63 365.83/104.63 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 365.83/104.63 365.83/104.63 We are left with following problem, upon which TcT provides the 365.83/104.63 certificate MAYBE. 365.83/104.63 365.83/104.63 Strict Trs: 365.83/104.63 { log(s(x1)) -> s(log(half(s(x1)))) 365.83/104.63 , s(s(p(s(x1)))) -> s(s(x1)) 365.83/104.63 , half(s(s(x1))) -> s(half(p(s(s(x1))))) 365.83/104.63 , half(s(0(x1))) -> 0(x1) 365.83/104.63 , half(half(s(s(s(s(x1)))))) -> s(s(half(half(x1)))) 365.83/104.63 , half(0(x1)) -> 0(s(s(half(x1)))) 365.83/104.63 , p(s(s(s(x1)))) -> s(p(s(s(x1)))) } 365.83/104.63 Weak Trs: { 0(x1) -> x1 } 365.83/104.63 Obligation: 365.83/104.63 derivational complexity 365.83/104.63 Answer: 365.83/104.63 MAYBE 365.83/104.63 365.83/104.63 The weightgap principle applies (using the following nonconstant 365.83/104.63 growth matrix-interpretation) 365.83/104.63 365.83/104.63 TcT has computed the following triangular matrix interpretation. 365.83/104.63 Note that the diagonal of the component-wise maxima of 365.83/104.63 interpretation-entries contains no more than 1 non-zero entries. 365.83/104.63 365.83/104.63 [log](x1) = [1] x1 + [0] 365.83/104.63 365.83/104.63 [s](x1) = [1] x1 + [0] 365.83/104.63 365.83/104.63 [half](x1) = [1] x1 + [0] 365.83/104.63 365.83/104.63 [0](x1) = [1] x1 + [0] 365.83/104.63 365.83/104.63 [p](x1) = [1] x1 + [1] 365.83/104.63 365.83/104.63 The order satisfies the following ordering constraints: 365.83/104.63 365.83/104.63 [log(s(x1))] = [1] x1 + [0] 365.83/104.63 >= [1] x1 + [0] 365.83/104.63 = [s(log(half(s(x1))))] 365.83/104.63 365.83/104.63 [s(s(p(s(x1))))] = [1] x1 + [1] 365.83/104.63 > [1] x1 + [0] 365.83/104.63 = [s(s(x1))] 365.83/104.63 365.83/104.63 [half(s(s(x1)))] = [1] x1 + [0] 365.83/104.63 ? [1] x1 + [1] 365.83/104.63 = [s(half(p(s(s(x1)))))] 365.83/104.63 365.83/104.63 [half(s(0(x1)))] = [1] x1 + [0] 365.83/104.63 >= [1] x1 + [0] 365.83/104.63 = [0(x1)] 365.83/104.63 365.83/104.63 [half(half(s(s(s(s(x1))))))] = [1] x1 + [0] 365.83/104.63 >= [1] x1 + [0] 365.83/104.63 = [s(s(half(half(x1))))] 365.83/104.63 365.83/104.63 [half(0(x1))] = [1] x1 + [0] 365.83/104.63 >= [1] x1 + [0] 365.83/104.63 = [0(s(s(half(x1))))] 365.83/104.63 365.83/104.63 [0(x1)] = [1] x1 + [0] 365.83/104.63 >= [1] x1 + [0] 365.83/104.63 = [x1] 365.83/104.63 365.83/104.63 [p(s(s(s(x1))))] = [1] x1 + [1] 365.83/104.63 >= [1] x1 + [1] 365.83/104.63 = [s(p(s(s(x1))))] 365.83/104.63 365.83/104.63 365.83/104.63 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 365.83/104.63 365.83/104.63 We are left with following problem, upon which TcT provides the 365.83/104.63 certificate MAYBE. 365.83/104.63 365.83/104.63 Strict Trs: 365.83/104.63 { log(s(x1)) -> s(log(half(s(x1)))) 365.83/104.63 , half(s(s(x1))) -> s(half(p(s(s(x1))))) 365.83/104.63 , half(s(0(x1))) -> 0(x1) 365.83/104.63 , half(half(s(s(s(s(x1)))))) -> s(s(half(half(x1)))) 365.83/104.63 , half(0(x1)) -> 0(s(s(half(x1)))) 365.83/104.63 , p(s(s(s(x1)))) -> s(p(s(s(x1)))) } 365.83/104.63 Weak Trs: 365.83/104.63 { s(s(p(s(x1)))) -> s(s(x1)) 365.83/104.63 , 0(x1) -> x1 } 365.83/104.63 Obligation: 365.83/104.63 derivational complexity 365.83/104.63 Answer: 365.83/104.63 MAYBE 365.83/104.63 365.83/104.63 The weightgap principle applies (using the following nonconstant 365.83/104.63 growth matrix-interpretation) 365.83/104.63 365.83/104.63 TcT has computed the following triangular matrix interpretation. 365.83/104.63 Note that the diagonal of the component-wise maxima of 365.83/104.64 interpretation-entries contains no more than 1 non-zero entries. 365.83/104.64 365.83/104.64 [log](x1) = [1] x1 + [0] 365.83/104.64 365.83/104.64 [s](x1) = [1] x1 + [0] 365.83/104.64 365.83/104.64 [half](x1) = [1] x1 + [1] 365.83/104.64 365.83/104.64 [0](x1) = [1] x1 + [0] 365.83/104.64 365.83/104.64 [p](x1) = [1] x1 + [0] 365.83/104.64 365.83/104.64 The order satisfies the following ordering constraints: 365.83/104.64 365.83/104.64 [log(s(x1))] = [1] x1 + [0] 365.83/104.64 ? [1] x1 + [1] 365.83/104.64 = [s(log(half(s(x1))))] 365.83/104.64 365.83/104.64 [s(s(p(s(x1))))] = [1] x1 + [0] 365.83/104.64 >= [1] x1 + [0] 365.83/104.64 = [s(s(x1))] 365.83/104.64 365.83/104.64 [half(s(s(x1)))] = [1] x1 + [1] 365.83/104.64 >= [1] x1 + [1] 365.83/104.64 = [s(half(p(s(s(x1)))))] 365.83/104.64 365.83/104.64 [half(s(0(x1)))] = [1] x1 + [1] 365.83/104.64 > [1] x1 + [0] 365.83/104.64 = [0(x1)] 365.83/104.64 365.83/104.64 [half(half(s(s(s(s(x1))))))] = [1] x1 + [2] 365.83/104.64 >= [1] x1 + [2] 365.83/104.64 = [s(s(half(half(x1))))] 365.83/104.64 365.83/104.64 [half(0(x1))] = [1] x1 + [1] 365.83/104.64 >= [1] x1 + [1] 365.83/104.64 = [0(s(s(half(x1))))] 365.83/104.64 365.83/104.64 [0(x1)] = [1] x1 + [0] 365.83/104.64 >= [1] x1 + [0] 365.83/104.64 = [x1] 365.83/104.64 365.83/104.64 [p(s(s(s(x1))))] = [1] x1 + [0] 365.83/104.64 >= [1] x1 + [0] 365.83/104.64 = [s(p(s(s(x1))))] 365.83/104.64 365.83/104.64 365.83/104.64 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 365.83/104.64 365.83/104.64 We are left with following problem, upon which TcT provides the 365.83/104.64 certificate MAYBE. 365.83/104.64 365.83/104.64 Strict Trs: 365.83/104.64 { log(s(x1)) -> s(log(half(s(x1)))) 365.83/104.64 , half(s(s(x1))) -> s(half(p(s(s(x1))))) 365.83/104.64 , half(half(s(s(s(s(x1)))))) -> s(s(half(half(x1)))) 365.83/104.64 , half(0(x1)) -> 0(s(s(half(x1)))) 365.83/104.64 , p(s(s(s(x1)))) -> s(p(s(s(x1)))) } 365.83/104.64 Weak Trs: 365.83/104.64 { s(s(p(s(x1)))) -> s(s(x1)) 365.83/104.64 , half(s(0(x1))) -> 0(x1) 365.83/104.64 , 0(x1) -> x1 } 365.83/104.64 Obligation: 365.83/104.64 derivational complexity 365.83/104.64 Answer: 365.83/104.64 MAYBE 365.83/104.64 365.83/104.64 The weightgap principle applies (using the following nonconstant 365.83/104.64 growth matrix-interpretation) 365.83/104.64 365.83/104.64 TcT has computed the following triangular matrix interpretation. 365.83/104.64 Note that the diagonal of the component-wise maxima of 365.83/104.64 interpretation-entries contains no more than 1 non-zero entries. 365.83/104.64 365.83/104.64 [log](x1) = [1] x1 + [0] 365.83/104.64 365.83/104.64 [s](x1) = [1] x1 + [1] 365.83/104.64 365.83/104.64 [half](x1) = [1] x1 + [0] 365.83/104.64 365.83/104.64 [0](x1) = [1] x1 + [0] 365.83/104.64 365.83/104.64 [p](x1) = [1] x1 + [0] 365.83/104.64 365.83/104.64 The order satisfies the following ordering constraints: 365.83/104.64 365.83/104.64 [log(s(x1))] = [1] x1 + [1] 365.83/104.64 ? [1] x1 + [2] 365.83/104.64 = [s(log(half(s(x1))))] 365.83/104.64 365.83/104.64 [s(s(p(s(x1))))] = [1] x1 + [3] 365.83/104.64 > [1] x1 + [2] 365.83/104.64 = [s(s(x1))] 365.83/104.64 365.83/104.64 [half(s(s(x1)))] = [1] x1 + [2] 365.83/104.64 ? [1] x1 + [3] 365.83/104.64 = [s(half(p(s(s(x1)))))] 365.83/104.64 365.83/104.64 [half(s(0(x1)))] = [1] x1 + [1] 365.83/104.64 > [1] x1 + [0] 365.83/104.64 = [0(x1)] 365.83/104.64 365.83/104.64 [half(half(s(s(s(s(x1))))))] = [1] x1 + [4] 365.83/104.64 > [1] x1 + [2] 365.83/104.64 = [s(s(half(half(x1))))] 365.83/104.64 365.83/104.64 [half(0(x1))] = [1] x1 + [0] 365.83/104.64 ? [1] x1 + [2] 365.83/104.64 = [0(s(s(half(x1))))] 365.83/104.64 365.83/104.64 [0(x1)] = [1] x1 + [0] 365.83/104.64 >= [1] x1 + [0] 365.83/104.64 = [x1] 365.83/104.64 365.83/104.64 [p(s(s(s(x1))))] = [1] x1 + [3] 365.83/104.64 >= [1] x1 + [3] 365.83/104.64 = [s(p(s(s(x1))))] 365.83/104.64 365.83/104.64 365.83/104.64 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 365.83/104.64 365.83/104.64 We are left with following problem, upon which TcT provides the 365.83/104.64 certificate MAYBE. 365.83/104.64 365.83/104.64 Strict Trs: 365.83/104.64 { log(s(x1)) -> s(log(half(s(x1)))) 365.83/104.64 , half(s(s(x1))) -> s(half(p(s(s(x1))))) 365.83/104.64 , half(0(x1)) -> 0(s(s(half(x1)))) 365.83/104.64 , p(s(s(s(x1)))) -> s(p(s(s(x1)))) } 365.83/104.64 Weak Trs: 365.83/104.64 { s(s(p(s(x1)))) -> s(s(x1)) 365.83/104.64 , half(s(0(x1))) -> 0(x1) 365.83/104.64 , half(half(s(s(s(s(x1)))))) -> s(s(half(half(x1)))) 365.83/104.64 , 0(x1) -> x1 } 365.83/104.64 Obligation: 365.83/104.64 derivational complexity 365.83/104.64 Answer: 365.83/104.64 MAYBE 365.83/104.64 365.83/104.64 None of the processors succeeded. 365.83/104.64 365.83/104.64 Details of failed attempt(s): 365.83/104.64 ----------------------------- 365.83/104.64 1) 'empty' failed due to the following reason: 365.83/104.64 365.83/104.64 Empty strict component of the problem is NOT empty. 365.83/104.64 365.83/104.64 2) 'Fastest' failed due to the following reason: 365.83/104.64 365.83/104.64 None of the processors succeeded. 365.83/104.64 365.83/104.64 Details of failed attempt(s): 365.83/104.64 ----------------------------- 365.83/104.64 1) 'bsearch-matrix' failed due to the following reason: 365.83/104.64 365.83/104.64 Following exception was raised: 365.83/104.64 stack overflow 365.83/104.64 365.83/104.64 2) 'iteProgress' failed due to the following reason: 365.83/104.64 365.83/104.64 Fail 365.83/104.64 365.83/104.64 3) 'Fastest' failed due to the following reason: 365.83/104.64 365.83/104.64 None of the processors succeeded. 365.83/104.64 365.83/104.64 Details of failed attempt(s): 365.83/104.64 ----------------------------- 365.83/104.64 1) 'matrix interpretation of dimension 6' failed due to the 365.83/104.64 following reason: 365.83/104.64 365.83/104.64 Following exception was raised: 365.83/104.64 stack overflow 365.83/104.64 365.83/104.64 2) 'matrix interpretation of dimension 5' failed due to the 365.83/104.64 following reason: 365.83/104.64 365.83/104.64 The input cannot be shown compatible 365.83/104.64 365.83/104.64 3) 'matrix interpretation of dimension 4' failed due to the 365.83/104.64 following reason: 365.83/104.64 365.83/104.64 The input cannot be shown compatible 365.83/104.64 365.83/104.64 4) 'matrix interpretation of dimension 3' failed due to the 365.83/104.64 following reason: 365.83/104.64 365.83/104.64 The input cannot be shown compatible 365.83/104.64 365.83/104.64 5) 'matrix interpretation of dimension 2' failed due to the 365.83/104.64 following reason: 365.83/104.64 365.83/104.64 The input cannot be shown compatible 365.83/104.64 365.83/104.64 6) 'matrix interpretation of dimension 1' failed due to the 365.83/104.64 following reason: 365.83/104.64 365.83/104.64 The input cannot be shown compatible 365.83/104.64 365.83/104.64 365.83/104.64 4) 'Fastest (timeout of 30 seconds)' failed due to the following 365.83/104.64 reason: 365.83/104.64 365.83/104.64 Computation stopped due to timeout after 30.0 seconds. 365.83/104.64 365.83/104.64 365.83/104.64 365.83/104.64 2) 'iteProgress (timeout of 297 seconds)' failed due to the 365.83/104.64 following reason: 365.83/104.64 365.83/104.64 Fail 365.83/104.64 365.83/104.64 3) 'Fastest (timeout of 60 seconds)' failed due to the following 365.83/104.64 reason: 365.83/104.64 365.83/104.64 Computation stopped due to timeout after 60.0 seconds. 365.83/104.64 365.83/104.64 4) 'bsearch-matrix (timeout of 297 seconds)' failed due to the 365.83/104.64 following reason: 365.83/104.64 365.83/104.64 Following exception was raised: 365.83/104.64 stack overflow 365.83/104.64 365.83/104.64 365.83/104.64 Arrrr.. 365.83/104.68 EOF