MAYBE We are left with following problem, upon which TcT provides the certificate MAYBE. Strict Trs: { +(0(), y) -> y , +(s(x), y) -> s(+(x, y)) , +(p(x), y) -> p(+(x, y)) , minus(0()) -> 0() , minus(s(x)) -> p(minus(x)) , minus(p(x)) -> s(minus(x)) , *(0(), y) -> 0() , *(s(x), y) -> +(*(x, y), y) , *(p(x), y) -> +(*(x, y), minus(y)) } Obligation: innermost runtime complexity Answer: MAYBE None of the processors succeeded. Details of failed attempt(s): ----------------------------- 1) 'empty' failed due to the following reason: Empty strict component of the problem is NOT empty. 2) 'Best' failed due to the following reason: None of the processors succeeded. Details of failed attempt(s): ----------------------------- 1) 'WithProblem (timeout of 60 seconds)' failed due to the following reason: Computation stopped due to timeout after 60.0 seconds. 2) 'Best' failed due to the following reason: None of the processors succeeded. Details of failed attempt(s): ----------------------------- 1) 'WithProblem (timeout of 30 seconds) (timeout of 60 seconds)' failed due to the following reason: None of the processors succeeded. Details of failed attempt(s): ----------------------------- 1) 'empty' failed due to the following reason: Empty strict component of the problem is NOT empty. 2) 'WithProblem' failed due to the following reason: None of the processors succeeded. Details of failed attempt(s): ----------------------------- 1) 'empty' failed due to the following reason: Empty strict component of the problem is NOT empty. 2) 'Fastest' failed due to the following reason: None of the processors succeeded. Details of failed attempt(s): ----------------------------- 1) 'WithProblem' failed due to the following reason: We use the processor 'polynomial interpretation' to orient following rules strictly. Trs: { *(s(x), y) -> +(*(x, y), y) , *(p(x), y) -> +(*(x, y), minus(y)) } The induced complexity on above rules (modulo remaining rules) is YES(?,O(n^2)) . These rules are moved into the corresponding weak component(s). Sub-proof: ---------- The following argument positions are considered usable: Uargs(+) = {1, 2}, Uargs(s) = {1}, Uargs(p) = {1} TcT has computed the following constructor-restricted polynomial interpretation. [+](x1, x2) = x1 + x2 [0]() = 0 [s](x1) = 1 + x1 [p](x1) = 1 + x1 [minus](x1) = x1 [*](x1, x2) = x1*x2 + x1^2 The following symbols are considered usable {+, minus, *} This order satisfies the following ordering constraints. [+(0(), y)] = y >= y = [y] [+(s(x), y)] = 1 + x + y >= 1 + x + y = [s(+(x, y))] [+(p(x), y)] = 1 + x + y >= 1 + x + y = [p(+(x, y))] [minus(0())] = >= = [0()] [minus(s(x))] = 1 + x >= 1 + x = [p(minus(x))] [minus(p(x))] = 1 + x >= 1 + x = [s(minus(x))] [*(0(), y)] = >= = [0()] [*(s(x), y)] = y + x*y + 1 + 2*x + x^2 > x*y + x^2 + y = [+(*(x, y), y)] [*(p(x), y)] = y + x*y + 1 + 2*x + x^2 > x*y + x^2 + y = [+(*(x, y), minus(y))] We return to the main proof. We are left with following problem, upon which TcT provides the certificate MAYBE. Strict Trs: { +(0(), y) -> y , +(s(x), y) -> s(+(x, y)) , +(p(x), y) -> p(+(x, y)) , minus(0()) -> 0() , minus(s(x)) -> p(minus(x)) , minus(p(x)) -> s(minus(x)) , *(0(), y) -> 0() } Weak Trs: { *(s(x), y) -> +(*(x, y), y) , *(p(x), y) -> +(*(x, y), minus(y)) } Obligation: innermost runtime complexity Answer: MAYBE We use the processor 'polynomial interpretation' to orient following rules strictly. Trs: { *(0(), y) -> 0() } The induced complexity on above rules (modulo remaining rules) is YES(?,O(n^2)) . These rules are moved into the corresponding weak component(s). Sub-proof: ---------- The following argument positions are considered usable: Uargs(+) = {1, 2}, Uargs(s) = {1}, Uargs(p) = {1} TcT has computed the following constructor-restricted polynomial interpretation. [+](x1, x2) = x1 + x2 [0]() = 0 [s](x1) = 1 + x1 [p](x1) = 1 + x1 [minus](x1) = x1 [*](x1, x2) = 1 + x1*x2 The following symbols are considered usable {+, minus, *} This order satisfies the following ordering constraints. [+(0(), y)] = y >= y = [y] [+(s(x), y)] = 1 + x + y >= 1 + x + y = [s(+(x, y))] [+(p(x), y)] = 1 + x + y >= 1 + x + y = [p(+(x, y))] [minus(0())] = >= = [0()] [minus(s(x))] = 1 + x >= 1 + x = [p(minus(x))] [minus(p(x))] = 1 + x >= 1 + x = [s(minus(x))] [*(0(), y)] = 1 > = [0()] [*(s(x), y)] = 1 + y + x*y >= 1 + x*y + y = [+(*(x, y), y)] [*(p(x), y)] = 1 + y + x*y >= 1 + x*y + y = [+(*(x, y), minus(y))] We return to the main proof. We are left with following problem, upon which TcT provides the certificate MAYBE. Strict Trs: { +(0(), y) -> y , +(s(x), y) -> s(+(x, y)) , +(p(x), y) -> p(+(x, y)) , minus(0()) -> 0() , minus(s(x)) -> p(minus(x)) , minus(p(x)) -> s(minus(x)) } Weak Trs: { *(0(), y) -> 0() , *(s(x), y) -> +(*(x, y), y) , *(p(x), y) -> +(*(x, y), minus(y)) } Obligation: innermost runtime complexity Answer: MAYBE We use the processor 'polynomial interpretation' to orient following rules strictly. Trs: { +(0(), y) -> y } The induced complexity on above rules (modulo remaining rules) is YES(?,O(n^2)) . These rules are moved into the corresponding weak component(s). Sub-proof: ---------- The following argument positions are considered usable: Uargs(+) = {1, 2}, Uargs(s) = {1}, Uargs(p) = {1} TcT has computed the following constructor-restricted polynomial interpretation. [+](x1, x2) = 3 + x1 + x2 [0]() = 0 [s](x1) = 1 + x1 [p](x1) = 1 + x1 [minus](x1) = x1 [*](x1, x2) = 2*x1 + x1*x2 + 2*x1^2 The following symbols are considered usable {+, minus, *} This order satisfies the following ordering constraints. [+(0(), y)] = 3 + y > y = [y] [+(s(x), y)] = 4 + x + y >= 4 + x + y = [s(+(x, y))] [+(p(x), y)] = 4 + x + y >= 4 + x + y = [p(+(x, y))] [minus(0())] = >= = [0()] [minus(s(x))] = 1 + x >= 1 + x = [p(minus(x))] [minus(p(x))] = 1 + x >= 1 + x = [s(minus(x))] [*(0(), y)] = >= = [0()] [*(s(x), y)] = 4 + 6*x + y + x*y + 2*x^2 > 3 + 2*x + x*y + 2*x^2 + y = [+(*(x, y), y)] [*(p(x), y)] = 4 + 6*x + y + x*y + 2*x^2 > 3 + 2*x + x*y + 2*x^2 + y = [+(*(x, y), minus(y))] We return to the main proof. We are left with following problem, upon which TcT provides the certificate MAYBE. Strict Trs: { +(s(x), y) -> s(+(x, y)) , +(p(x), y) -> p(+(x, y)) , minus(0()) -> 0() , minus(s(x)) -> p(minus(x)) , minus(p(x)) -> s(minus(x)) } Weak Trs: { +(0(), y) -> y , *(0(), y) -> 0() , *(s(x), y) -> +(*(x, y), y) , *(p(x), y) -> +(*(x, y), minus(y)) } Obligation: innermost runtime complexity Answer: MAYBE We use the processor 'polynomial interpretation' to orient following rules strictly. Trs: { minus(0()) -> 0() , minus(p(x)) -> s(minus(x)) } The induced complexity on above rules (modulo remaining rules) is YES(?,O(n^2)) . These rules are moved into the corresponding weak component(s). Sub-proof: ---------- The following argument positions are considered usable: Uargs(+) = {1, 2}, Uargs(s) = {1}, Uargs(p) = {1} TcT has computed the following constructor-restricted polynomial interpretation. [+](x1, x2) = x1 + 2*x2 [0]() = 2 [s](x1) = 1 + x1 [p](x1) = 2 + x1 [minus](x1) = 2*x1 [*](x1, x2) = 2*x1 + 2*x1*x2 + 2*x2 The following symbols are considered usable {+, minus, *} This order satisfies the following ordering constraints. [+(0(), y)] = 2 + 2*y > y = [y] [+(s(x), y)] = 1 + x + 2*y >= 1 + x + 2*y = [s(+(x, y))] [+(p(x), y)] = 2 + x + 2*y >= 2 + x + 2*y = [p(+(x, y))] [minus(0())] = 4 > 2 = [0()] [minus(s(x))] = 2 + 2*x >= 2 + 2*x = [p(minus(x))] [minus(p(x))] = 4 + 2*x > 1 + 2*x = [s(minus(x))] [*(0(), y)] = 4 + 6*y > 2 = [0()] [*(s(x), y)] = 2 + 2*x + 4*y + 2*x*y > 2*x + 2*x*y + 4*y = [+(*(x, y), y)] [*(p(x), y)] = 4 + 2*x + 6*y + 2*x*y > 2*x + 2*x*y + 6*y = [+(*(x, y), minus(y))] We return to the main proof. We are left with following problem, upon which TcT provides the certificate MAYBE. Strict Trs: { +(s(x), y) -> s(+(x, y)) , +(p(x), y) -> p(+(x, y)) , minus(s(x)) -> p(minus(x)) } Weak Trs: { +(0(), y) -> y , minus(0()) -> 0() , minus(p(x)) -> s(minus(x)) , *(0(), y) -> 0() , *(s(x), y) -> +(*(x, y), y) , *(p(x), y) -> +(*(x, y), minus(y)) } Obligation: innermost runtime complexity Answer: MAYBE We use the processor 'polynomial interpretation' to orient following rules strictly. Trs: { minus(s(x)) -> p(minus(x)) } The induced complexity on above rules (modulo remaining rules) is YES(?,O(n^2)) . These rules are moved into the corresponding weak component(s). Sub-proof: ---------- The following argument positions are considered usable: Uargs(+) = {1, 2}, Uargs(s) = {1}, Uargs(p) = {1} TcT has computed the following constructor-restricted polynomial interpretation. [+](x1, x2) = 2 + x1 + x2 [0]() = 0 [s](x1) = 2 + x1 [p](x1) = 2 + x1 [minus](x1) = 2*x1 [*](x1, x2) = x1 + 2*x1*x2 The following symbols are considered usable {+, minus, *} This order satisfies the following ordering constraints. [+(0(), y)] = 2 + y > y = [y] [+(s(x), y)] = 4 + x + y >= 4 + x + y = [s(+(x, y))] [+(p(x), y)] = 4 + x + y >= 4 + x + y = [p(+(x, y))] [minus(0())] = >= = [0()] [minus(s(x))] = 4 + 2*x > 2 + 2*x = [p(minus(x))] [minus(p(x))] = 4 + 2*x > 2 + 2*x = [s(minus(x))] [*(0(), y)] = >= = [0()] [*(s(x), y)] = 2 + x + 4*y + 2*x*y >= 2 + x + 2*x*y + y = [+(*(x, y), y)] [*(p(x), y)] = 2 + x + 4*y + 2*x*y >= 2 + x + 2*x*y + 2*y = [+(*(x, y), minus(y))] We return to the main proof. We are left with following problem, upon which TcT provides the certificate MAYBE. Strict Trs: { +(s(x), y) -> s(+(x, y)) , +(p(x), y) -> p(+(x, y)) } Weak Trs: { +(0(), y) -> y , minus(0()) -> 0() , minus(s(x)) -> p(minus(x)) , minus(p(x)) -> s(minus(x)) , *(0(), y) -> 0() , *(s(x), y) -> +(*(x, y), y) , *(p(x), y) -> +(*(x, y), minus(y)) } Obligation: innermost runtime complexity Answer: MAYBE None of the processors succeeded. Details of failed attempt(s): ----------------------------- 1) 'empty' failed due to the following reason: Empty strict component of the problem is NOT empty. 2) 'WithProblem' failed due to the following reason: Empty strict component of the problem is NOT empty. 2) 'WithProblem' failed due to the following reason: None of the processors succeeded. Details of failed attempt(s): ----------------------------- 1) 'empty' failed due to the following reason: Empty strict component of the problem is NOT empty. 2) 'WithProblem' failed due to the following reason: None of the processors succeeded. Details of failed attempt(s): ----------------------------- 1) 'empty' failed due to the following reason: Empty strict component of the problem is NOT empty. 2) 'WithProblem' failed due to the following reason: None of the processors succeeded. Details of failed attempt(s): ----------------------------- 1) 'empty' failed due to the following reason: Empty strict component of the problem is NOT empty. 2) 'WithProblem' failed due to the following reason: Empty strict component of the problem is NOT empty. 2) 'Best' failed due to the following reason: None of the processors succeeded. Details of failed attempt(s): ----------------------------- 1) 'Polynomial Path Order (PS) (timeout of 60 seconds)' failed due to the following reason: The input cannot be shown compatible 2) 'bsearch-popstar (timeout of 60 seconds)' failed due to the following reason: The input cannot be shown compatible 3) 'Fastest (timeout of 5 seconds) (timeout of 60 seconds)' failed due to the following reason: None of the processors succeeded. Details of failed attempt(s): ----------------------------- 1) 'Bounds with minimal-enrichment and initial automaton 'match'' failed due to the following reason: match-boundness of the problem could not be verified. 2) 'Bounds with perSymbol-enrichment and initial automaton 'match'' failed due to the following reason: match-boundness of the problem could not be verified. Arrrr..