MAYBE 945.67/297.03 MAYBE 945.67/297.03 945.67/297.03 We are left with following problem, upon which TcT provides the 945.67/297.03 certificate MAYBE. 945.67/297.03 945.67/297.03 Strict Trs: 945.67/297.03 { f(x, y, g(z)) -> g(f(x, y, z)) 945.67/297.03 , f(x, g(y), z) -> g(f(x, y, z)) 945.67/297.03 , f(0(), 1(), x) -> f(g(x), g(x), x) 945.67/297.03 , f(g(x), y, z) -> g(f(x, y, z)) } 945.67/297.03 Obligation: 945.67/297.03 innermost runtime complexity 945.67/297.03 Answer: 945.67/297.03 MAYBE 945.67/297.03 945.67/297.03 None of the processors succeeded. 945.67/297.03 945.67/297.03 Details of failed attempt(s): 945.67/297.03 ----------------------------- 945.67/297.03 1) 'empty' failed due to the following reason: 945.67/297.03 945.67/297.03 Empty strict component of the problem is NOT empty. 945.67/297.03 945.67/297.03 2) 'Best' failed due to the following reason: 945.67/297.03 945.67/297.03 None of the processors succeeded. 945.67/297.03 945.67/297.03 Details of failed attempt(s): 945.67/297.03 ----------------------------- 945.67/297.03 1) 'With Problem ... (timeout of 297 seconds)' failed due to the 945.67/297.03 following reason: 945.67/297.03 945.67/297.03 Computation stopped due to timeout after 297.0 seconds. 945.67/297.03 945.67/297.03 2) 'Best' failed due to the following reason: 945.67/297.03 945.67/297.03 None of the processors succeeded. 945.67/297.03 945.67/297.03 Details of failed attempt(s): 945.67/297.03 ----------------------------- 945.67/297.03 1) 'With Problem ... (timeout of 148 seconds) (timeout of 297 945.67/297.03 seconds)' failed due to the following reason: 945.67/297.03 945.67/297.03 None of the processors succeeded. 945.67/297.03 945.67/297.03 Details of failed attempt(s): 945.67/297.03 ----------------------------- 945.67/297.03 1) 'empty' failed due to the following reason: 945.67/297.03 945.67/297.03 Empty strict component of the problem is NOT empty. 945.67/297.03 945.67/297.03 2) 'With Problem ...' failed due to the following reason: 945.67/297.03 945.67/297.03 None of the processors succeeded. 945.67/297.03 945.67/297.03 Details of failed attempt(s): 945.67/297.03 ----------------------------- 945.67/297.03 1) 'empty' failed due to the following reason: 945.67/297.03 945.67/297.03 Empty strict component of the problem is NOT empty. 945.67/297.03 945.67/297.03 2) 'Fastest' failed due to the following reason: 945.67/297.03 945.67/297.03 None of the processors succeeded. 945.67/297.03 945.67/297.03 Details of failed attempt(s): 945.67/297.03 ----------------------------- 945.67/297.03 1) 'With Problem ...' failed due to the following reason: 945.67/297.03 945.67/297.03 None of the processors succeeded. 945.67/297.03 945.67/297.03 Details of failed attempt(s): 945.67/297.03 ----------------------------- 945.67/297.03 1) 'empty' failed due to the following reason: 945.67/297.03 945.67/297.03 Empty strict component of the problem is NOT empty. 945.67/297.03 945.67/297.03 2) 'With Problem ...' failed due to the following reason: 945.67/297.03 945.67/297.03 The weightgap principle applies (using the following nonconstant 945.67/297.03 growth matrix-interpretation) 945.67/297.03 945.67/297.03 The following argument positions are usable: 945.67/297.03 Uargs(g) = {1} 945.67/297.03 945.67/297.03 TcT has computed the following matrix interpretation satisfying 945.67/297.03 not(EDA) and not(IDA(1)). 945.67/297.03 945.67/297.03 [f](x1, x2, x3) = [0 4] x3 + [0] 945.67/297.03 [0 1] [0] 945.67/297.03 945.67/297.03 [0] = [7] 945.67/297.03 [0] 945.67/297.03 945.67/297.03 [1] = [7] 945.67/297.03 [0] 945.67/297.03 945.67/297.03 [g](x1) = [1 0] x1 + [0] 945.67/297.03 [0 1] [2] 945.67/297.03 945.67/297.03 The order satisfies the following ordering constraints: 945.67/297.03 945.67/297.03 [f(x, y, g(z))] = [0 4] z + [8] 945.67/297.03 [0 1] [2] 945.67/297.03 > [0 4] z + [0] 945.67/297.03 [0 1] [2] 945.67/297.03 = [g(f(x, y, z))] 945.67/297.03 945.67/297.03 [f(x, g(y), z)] = [0 4] z + [0] 945.67/297.03 [0 1] [0] 945.67/297.03 ? [0 4] z + [0] 945.67/297.03 [0 1] [2] 945.67/297.03 = [g(f(x, y, z))] 945.67/297.03 945.67/297.03 [f(0(), 1(), x)] = [0 4] x + [0] 945.67/297.03 [0 1] [0] 945.67/297.03 >= [0 4] x + [0] 945.67/297.03 [0 1] [0] 945.67/297.03 = [f(g(x), g(x), x)] 945.67/297.03 945.67/297.03 [f(g(x), y, z)] = [0 4] z + [0] 945.67/297.03 [0 1] [0] 945.67/297.03 ? [0 4] z + [0] 945.67/297.03 [0 1] [2] 945.67/297.03 = [g(f(x, y, z))] 945.67/297.03 945.67/297.03 945.67/297.03 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 945.67/297.03 945.67/297.03 We are left with following problem, upon which TcT provides the 945.67/297.03 certificate MAYBE. 945.67/297.03 945.67/297.03 Strict Trs: 945.67/297.03 { f(x, g(y), z) -> g(f(x, y, z)) 945.67/297.03 , f(0(), 1(), x) -> f(g(x), g(x), x) 945.67/297.03 , f(g(x), y, z) -> g(f(x, y, z)) } 945.67/297.03 Weak Trs: { f(x, y, g(z)) -> g(f(x, y, z)) } 945.67/297.03 Obligation: 945.67/297.03 innermost runtime complexity 945.67/297.03 Answer: 945.67/297.03 MAYBE 945.67/297.03 945.67/297.03 None of the processors succeeded. 945.67/297.03 945.67/297.03 Details of failed attempt(s): 945.67/297.03 ----------------------------- 945.67/297.03 1) 'empty' failed due to the following reason: 945.67/297.03 945.67/297.03 Empty strict component of the problem is NOT empty. 945.67/297.03 945.67/297.03 2) 'With Problem ...' failed due to the following reason: 945.67/297.03 945.67/297.03 None of the processors succeeded. 945.67/297.03 945.67/297.03 Details of failed attempt(s): 945.67/297.03 ----------------------------- 945.67/297.03 1) 'empty' failed due to the following reason: 945.67/297.03 945.67/297.03 Empty strict component of the problem is NOT empty. 945.67/297.03 945.67/297.03 2) 'With Problem ...' failed due to the following reason: 945.67/297.03 945.67/297.03 Empty strict component of the problem is NOT empty. 945.67/297.03 945.67/297.03 945.67/297.03 945.67/297.03 945.67/297.03 2) 'With Problem ...' failed due to the following reason: 945.67/297.03 945.67/297.03 None of the processors succeeded. 945.67/297.03 945.67/297.03 Details of failed attempt(s): 945.67/297.03 ----------------------------- 945.67/297.03 1) 'empty' failed due to the following reason: 945.67/297.03 945.67/297.03 Empty strict component of the problem is NOT empty. 945.67/297.03 945.67/297.03 2) 'With Problem ...' failed due to the following reason: 945.67/297.03 945.67/297.03 Empty strict component of the problem is NOT empty. 945.67/297.03 945.67/297.03 945.67/297.03 945.67/297.03 945.67/297.03 945.67/297.03 2) 'Best' failed due to the following reason: 945.67/297.03 945.67/297.03 None of the processors succeeded. 945.67/297.03 945.67/297.03 Details of failed attempt(s): 945.67/297.03 ----------------------------- 945.67/297.03 1) 'bsearch-popstar (timeout of 297 seconds)' failed due to the 945.67/297.03 following reason: 945.67/297.03 945.67/297.03 The input cannot be shown compatible 945.67/297.03 945.67/297.03 2) 'Polynomial Path Order (PS) (timeout of 297 seconds)' failed due 945.67/297.03 to the following reason: 945.67/297.03 945.67/297.03 The input cannot be shown compatible 945.67/297.03 945.67/297.03 945.67/297.03 3) 'Fastest (timeout of 24 seconds) (timeout of 297 seconds)' 945.67/297.03 failed due to the following reason: 945.67/297.03 945.67/297.03 None of the processors succeeded. 945.67/297.03 945.67/297.03 Details of failed attempt(s): 945.67/297.03 ----------------------------- 945.67/297.03 1) 'Bounds with perSymbol-enrichment and initial automaton 'match'' 945.67/297.03 failed due to the following reason: 945.67/297.03 945.67/297.03 match-boundness of the problem could not be verified. 945.67/297.03 945.67/297.03 2) 'Bounds with minimal-enrichment and initial automaton 'match'' 945.67/297.03 failed due to the following reason: 945.67/297.03 945.67/297.03 match-boundness of the problem could not be verified. 945.67/297.03 945.67/297.03 945.67/297.03 945.67/297.03 945.67/297.03 945.67/297.03 Arrrr.. 946.52/297.81 EOF