MAYBE We are left with following problem, upon which TcT provides the certificate MAYBE. Strict Trs: { a__f(X1, X2, X3) -> f(X1, X2, X3) , a__f(a(), b(), X) -> a__f(X, X, mark(X)) , mark(a()) -> a() , mark(b()) -> b() , mark(f(X1, X2, X3)) -> a__f(X1, X2, mark(X3)) , mark(c()) -> a__c() , a__c() -> a() , a__c() -> b() , a__c() -> c() } 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: The weightgap principle applies (using the following nonconstant growth matrix-interpretation) The following argument positions are usable: Uargs(a__f) = {3} TcT has computed the following matrix interpretation satisfying not(EDA) and not(IDA(1)). [a__f](x1, x2, x3) = [1] x3 + [7] [a] = [7] [b] = [7] [mark](x1) = [1] x1 + [7] [a__c] = [3] [f](x1, x2, x3) = [1] x3 + [7] [c] = [7] The following symbols are considered usable {a__f, mark, a__c} The order satisfies the following ordering constraints: [a__f(X1, X2, X3)] = [1] X3 + [7] >= [1] X3 + [7] = [f(X1, X2, X3)] [a__f(a(), b(), X)] = [1] X + [7] ? [1] X + [14] = [a__f(X, X, mark(X))] [mark(a())] = [14] > [7] = [a()] [mark(b())] = [14] > [7] = [b()] [mark(f(X1, X2, X3))] = [1] X3 + [14] >= [1] X3 + [14] = [a__f(X1, X2, mark(X3))] [mark(c())] = [14] > [3] = [a__c()] [a__c()] = [3] ? [7] = [a()] [a__c()] = [3] ? [7] = [b()] [a__c()] = [3] ? [7] = [c()] Further, it can be verified that all rules not oriented are covered by the weightgap condition. We are left with following problem, upon which TcT provides the certificate MAYBE. Strict Trs: { a__f(X1, X2, X3) -> f(X1, X2, X3) , a__f(a(), b(), X) -> a__f(X, X, mark(X)) , mark(f(X1, X2, X3)) -> a__f(X1, X2, mark(X3)) , a__c() -> a() , a__c() -> b() , a__c() -> c() } Weak Trs: { mark(a()) -> a() , mark(b()) -> b() , mark(c()) -> a__c() } Obligation: innermost runtime complexity Answer: MAYBE The weightgap principle applies (using the following nonconstant growth matrix-interpretation) The following argument positions are usable: Uargs(a__f) = {3} TcT has computed the following matrix interpretation satisfying not(EDA) and not(IDA(1)). [a__f](x1, x2, x3) = [1] x3 + [7] [a] = [5] [b] = [5] [mark](x1) = [1] x1 + [7] [a__c] = [6] [f](x1, x2, x3) = [1] x3 + [7] [c] = [3] The following symbols are considered usable {a__f, mark, a__c} The order satisfies the following ordering constraints: [a__f(X1, X2, X3)] = [1] X3 + [7] >= [1] X3 + [7] = [f(X1, X2, X3)] [a__f(a(), b(), X)] = [1] X + [7] ? [1] X + [14] = [a__f(X, X, mark(X))] [mark(a())] = [12] > [5] = [a()] [mark(b())] = [12] > [5] = [b()] [mark(f(X1, X2, X3))] = [1] X3 + [14] >= [1] X3 + [14] = [a__f(X1, X2, mark(X3))] [mark(c())] = [10] > [6] = [a__c()] [a__c()] = [6] > [5] = [a()] [a__c()] = [6] > [5] = [b()] [a__c()] = [6] > [3] = [c()] Further, it can be verified that all rules not oriented are covered by the weightgap condition. We are left with following problem, upon which TcT provides the certificate MAYBE. Strict Trs: { a__f(X1, X2, X3) -> f(X1, X2, X3) , a__f(a(), b(), X) -> a__f(X, X, mark(X)) , mark(f(X1, X2, X3)) -> a__f(X1, X2, mark(X3)) } Weak Trs: { mark(a()) -> a() , mark(b()) -> b() , mark(c()) -> a__c() , a__c() -> a() , a__c() -> b() , a__c() -> c() } Obligation: innermost runtime complexity Answer: MAYBE The weightgap principle applies (using the following nonconstant growth matrix-interpretation) The following argument positions are usable: Uargs(a__f) = {3} TcT has computed the following matrix interpretation satisfying not(EDA) and not(IDA(1)). [a__f](x1, x2, x3) = [1] x3 + [4] [a] = [7] [b] = [7] [mark](x1) = [1] x1 + [0] [a__c] = [7] [f](x1, x2, x3) = [1] x3 + [1] [c] = [7] The following symbols are considered usable {a__f, mark, a__c} The order satisfies the following ordering constraints: [a__f(X1, X2, X3)] = [1] X3 + [4] > [1] X3 + [1] = [f(X1, X2, X3)] [a__f(a(), b(), X)] = [1] X + [4] >= [1] X + [4] = [a__f(X, X, mark(X))] [mark(a())] = [7] >= [7] = [a()] [mark(b())] = [7] >= [7] = [b()] [mark(f(X1, X2, X3))] = [1] X3 + [1] ? [1] X3 + [4] = [a__f(X1, X2, mark(X3))] [mark(c())] = [7] >= [7] = [a__c()] [a__c()] = [7] >= [7] = [a()] [a__c()] = [7] >= [7] = [b()] [a__c()] = [7] >= [7] = [c()] Further, it can be verified that all rules not oriented are covered by the weightgap condition. We are left with following problem, upon which TcT provides the certificate MAYBE. Strict Trs: { a__f(a(), b(), X) -> a__f(X, X, mark(X)) , mark(f(X1, X2, X3)) -> a__f(X1, X2, mark(X3)) } Weak Trs: { a__f(X1, X2, X3) -> f(X1, X2, X3) , mark(a()) -> a() , mark(b()) -> b() , mark(c()) -> a__c() , a__c() -> a() , a__c() -> b() , a__c() -> c() } 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: 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: 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) '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) 'bsearch-popstar (timeout of 60 seconds)' failed due to the following reason: The input cannot be shown compatible 2) 'Polynomial Path Order (PS) (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..