MAYBE 879.53/298.49 MAYBE 879.53/298.49 879.53/298.49 We are left with following problem, upon which TcT provides the 879.53/298.49 certificate MAYBE. 879.53/298.49 879.53/298.49 Strict Trs: 879.53/298.49 { a__f(X) -> a__if(mark(X), c(), f(true())) 879.53/298.49 , a__f(X) -> f(X) 879.53/298.49 , a__if(X1, X2, X3) -> if(X1, X2, X3) 879.53/298.49 , a__if(true(), X, Y) -> mark(X) 879.53/298.49 , a__if(false(), X, Y) -> mark(Y) 879.53/298.49 , mark(c()) -> c() 879.53/298.49 , mark(f(X)) -> a__f(mark(X)) 879.53/298.49 , mark(true()) -> true() 879.53/298.49 , mark(false()) -> false() 879.53/298.49 , mark(if(X1, X2, X3)) -> a__if(mark(X1), mark(X2), X3) } 879.53/298.49 Obligation: 879.53/298.49 innermost runtime complexity 879.53/298.49 Answer: 879.53/298.49 MAYBE 879.53/298.49 879.53/298.49 None of the processors succeeded. 879.53/298.49 879.53/298.49 Details of failed attempt(s): 879.53/298.49 ----------------------------- 879.53/298.49 1) 'empty' failed due to the following reason: 879.53/298.49 879.53/298.49 Empty strict component of the problem is NOT empty. 879.53/298.49 879.53/298.49 2) 'Best' failed due to the following reason: 879.53/298.49 879.53/298.49 None of the processors succeeded. 879.53/298.49 879.53/298.49 Details of failed attempt(s): 879.53/298.49 ----------------------------- 879.53/298.49 1) 'With Problem ... (timeout of 297 seconds)' failed due to the 879.53/298.49 following reason: 879.53/298.49 879.53/298.49 Computation stopped due to timeout after 297.0 seconds. 879.53/298.49 879.53/298.49 2) 'Best' failed due to the following reason: 879.53/298.49 879.53/298.49 None of the processors succeeded. 879.53/298.49 879.53/298.49 Details of failed attempt(s): 879.53/298.49 ----------------------------- 879.53/298.49 1) 'Fastest (timeout of 24 seconds) (timeout of 297 seconds)' 879.53/298.49 failed due to the following reason: 879.53/298.49 879.53/298.49 Computation stopped due to timeout after 24.0 seconds. 879.53/298.49 879.53/298.49 2) 'With Problem ... (timeout of 148 seconds) (timeout of 297 879.53/298.49 seconds)' failed due to the following reason: 879.53/298.49 879.53/298.49 The weightgap principle applies (using the following nonconstant 879.53/298.49 growth matrix-interpretation) 879.53/298.49 879.53/298.49 The following argument positions are usable: 879.53/298.49 Uargs(a__f) = {1}, Uargs(a__if) = {1, 2} 879.53/298.49 879.53/298.49 TcT has computed the following matrix interpretation satisfying 879.53/298.49 not(EDA) and not(IDA(1)). 879.53/298.49 879.53/298.49 [a__f](x1) = [1] x1 + [4] 879.53/298.49 879.53/298.49 [a__if](x1, x2, x3) = [1] x1 + [1] x2 + [0] 879.53/298.49 879.53/298.49 [mark](x1) = [0] 879.53/298.49 879.53/298.49 [c] = [0] 879.53/298.49 879.53/298.49 [f](x1) = [5] 879.53/298.49 879.53/298.49 [true] = [0] 879.53/298.49 879.53/298.49 [false] = [0] 879.53/298.49 879.53/298.49 [if](x1, x2, x3) = [1] x1 + [1] x2 + [7] 879.53/298.49 879.53/298.49 The order satisfies the following ordering constraints: 879.53/298.49 879.53/298.49 [a__f(X)] = [1] X + [4] 879.53/298.49 > [0] 879.53/298.49 = [a__if(mark(X), c(), f(true()))] 879.53/298.49 879.53/298.49 [a__f(X)] = [1] X + [4] 879.53/298.49 ? [5] 879.53/298.49 = [f(X)] 879.53/298.49 879.53/298.49 [a__if(X1, X2, X3)] = [1] X1 + [1] X2 + [0] 879.53/298.49 ? [1] X1 + [1] X2 + [7] 879.53/298.49 = [if(X1, X2, X3)] 879.53/298.49 879.53/298.49 [a__if(true(), X, Y)] = [1] X + [0] 879.53/298.49 >= [0] 879.53/298.49 = [mark(X)] 879.53/298.49 879.53/298.49 [a__if(false(), X, Y)] = [1] X + [0] 879.53/298.49 >= [0] 879.53/298.49 = [mark(Y)] 879.53/298.49 879.53/298.49 [mark(c())] = [0] 879.53/298.49 >= [0] 879.53/298.49 = [c()] 879.53/298.49 879.53/298.49 [mark(f(X))] = [0] 879.53/298.49 ? [4] 879.53/298.49 = [a__f(mark(X))] 879.53/298.49 879.53/298.49 [mark(true())] = [0] 879.53/298.49 >= [0] 879.53/298.49 = [true()] 879.53/298.49 879.53/298.49 [mark(false())] = [0] 879.53/298.49 >= [0] 879.53/298.49 = [false()] 879.53/298.49 879.53/298.49 [mark(if(X1, X2, X3))] = [0] 879.53/298.49 >= [0] 879.53/298.49 = [a__if(mark(X1), mark(X2), X3)] 879.53/298.49 879.53/298.49 879.53/298.49 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 879.53/298.49 879.53/298.49 We are left with following problem, upon which TcT provides the 879.53/298.49 certificate MAYBE. 879.53/298.49 879.53/298.49 Strict Trs: 879.53/298.49 { a__f(X) -> f(X) 879.53/298.49 , a__if(X1, X2, X3) -> if(X1, X2, X3) 879.53/298.49 , a__if(true(), X, Y) -> mark(X) 879.53/298.49 , a__if(false(), X, Y) -> mark(Y) 879.53/298.49 , mark(c()) -> c() 879.53/298.49 , mark(f(X)) -> a__f(mark(X)) 879.53/298.49 , mark(true()) -> true() 879.53/298.49 , mark(false()) -> false() 879.53/298.49 , mark(if(X1, X2, X3)) -> a__if(mark(X1), mark(X2), X3) } 879.53/298.49 Weak Trs: { a__f(X) -> a__if(mark(X), c(), f(true())) } 879.53/298.49 Obligation: 879.53/298.49 innermost runtime complexity 879.53/298.49 Answer: 879.53/298.49 MAYBE 879.53/298.49 879.53/298.49 The weightgap principle applies (using the following nonconstant 879.53/298.49 growth matrix-interpretation) 879.53/298.49 879.53/298.49 The following argument positions are usable: 879.53/298.49 Uargs(a__f) = {1}, Uargs(a__if) = {1, 2} 879.53/298.49 879.53/298.49 TcT has computed the following matrix interpretation satisfying 879.53/298.49 not(EDA) and not(IDA(1)). 879.53/298.49 879.53/298.49 [a__f](x1) = [1] x1 + [0] 879.53/298.49 879.53/298.49 [a__if](x1, x2, x3) = [1] x1 + [1] x2 + [0] 879.53/298.49 879.53/298.49 [mark](x1) = [0] 879.53/298.49 879.53/298.49 [c] = [0] 879.53/298.49 879.53/298.49 [f](x1) = [5] 879.53/298.49 879.53/298.49 [true] = [0] 879.53/298.49 879.53/298.49 [false] = [4] 879.53/298.49 879.53/298.49 [if](x1, x2, x3) = [1] x1 + [1] x2 + [7] 879.53/298.49 879.53/298.49 The order satisfies the following ordering constraints: 879.53/298.49 879.53/298.49 [a__f(X)] = [1] X + [0] 879.53/298.49 >= [0] 879.53/298.49 = [a__if(mark(X), c(), f(true()))] 879.53/298.49 879.53/298.49 [a__f(X)] = [1] X + [0] 879.53/298.49 ? [5] 879.53/298.49 = [f(X)] 879.53/298.49 879.53/298.49 [a__if(X1, X2, X3)] = [1] X1 + [1] X2 + [0] 879.53/298.49 ? [1] X1 + [1] X2 + [7] 879.53/298.49 = [if(X1, X2, X3)] 879.53/298.49 879.53/298.49 [a__if(true(), X, Y)] = [1] X + [0] 879.53/298.49 >= [0] 879.53/298.49 = [mark(X)] 879.53/298.49 879.53/298.49 [a__if(false(), X, Y)] = [1] X + [4] 879.53/298.49 > [0] 879.53/298.49 = [mark(Y)] 879.53/298.49 879.53/298.49 [mark(c())] = [0] 879.53/298.49 >= [0] 879.53/298.49 = [c()] 879.53/298.49 879.53/298.49 [mark(f(X))] = [0] 879.53/298.49 >= [0] 879.53/298.49 = [a__f(mark(X))] 879.53/298.49 879.53/298.49 [mark(true())] = [0] 879.53/298.49 >= [0] 879.53/298.49 = [true()] 879.53/298.49 879.53/298.49 [mark(false())] = [0] 879.53/298.49 ? [4] 879.53/298.49 = [false()] 879.53/298.49 879.53/298.49 [mark(if(X1, X2, X3))] = [0] 879.53/298.49 >= [0] 879.53/298.49 = [a__if(mark(X1), mark(X2), X3)] 879.53/298.49 879.53/298.49 879.53/298.49 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 879.53/298.49 879.53/298.49 We are left with following problem, upon which TcT provides the 879.53/298.49 certificate MAYBE. 879.53/298.49 879.53/298.49 Strict Trs: 879.53/298.49 { a__f(X) -> f(X) 879.53/298.49 , a__if(X1, X2, X3) -> if(X1, X2, X3) 879.53/298.49 , a__if(true(), X, Y) -> mark(X) 879.53/298.49 , mark(c()) -> c() 879.53/298.49 , mark(f(X)) -> a__f(mark(X)) 879.53/298.49 , mark(true()) -> true() 879.53/298.49 , mark(false()) -> false() 879.53/298.49 , mark(if(X1, X2, X3)) -> a__if(mark(X1), mark(X2), X3) } 879.53/298.49 Weak Trs: 879.53/298.49 { a__f(X) -> a__if(mark(X), c(), f(true())) 879.53/298.49 , a__if(false(), X, Y) -> mark(Y) } 879.53/298.49 Obligation: 879.53/298.49 innermost runtime complexity 879.53/298.49 Answer: 879.53/298.49 MAYBE 879.53/298.49 879.53/298.49 The weightgap principle applies (using the following nonconstant 879.53/298.49 growth matrix-interpretation) 879.53/298.49 879.53/298.49 The following argument positions are usable: 879.53/298.49 Uargs(a__f) = {1}, Uargs(a__if) = {1, 2} 879.53/298.49 879.53/298.49 TcT has computed the following matrix interpretation satisfying 879.53/298.49 not(EDA) and not(IDA(1)). 879.53/298.49 879.53/298.49 [a__f](x1) = [1] x1 + [0] 879.53/298.49 879.53/298.49 [a__if](x1, x2, x3) = [1] x1 + [1] x2 + [0] 879.53/298.49 879.53/298.49 [mark](x1) = [0] 879.53/298.49 879.53/298.49 [c] = [0] 879.53/298.49 879.53/298.49 [f](x1) = [5] 879.53/298.49 879.53/298.49 [true] = [4] 879.53/298.49 879.53/298.49 [false] = [0] 879.53/298.49 879.53/298.49 [if](x1, x2, x3) = [1] x1 + [1] x2 + [7] 879.53/298.49 879.53/298.49 The order satisfies the following ordering constraints: 879.53/298.49 879.53/298.49 [a__f(X)] = [1] X + [0] 879.53/298.49 >= [0] 879.53/298.49 = [a__if(mark(X), c(), f(true()))] 879.53/298.49 879.53/298.49 [a__f(X)] = [1] X + [0] 879.53/298.49 ? [5] 879.53/298.49 = [f(X)] 879.53/298.49 879.53/298.49 [a__if(X1, X2, X3)] = [1] X1 + [1] X2 + [0] 879.53/298.49 ? [1] X1 + [1] X2 + [7] 879.53/298.49 = [if(X1, X2, X3)] 879.53/298.49 879.53/298.49 [a__if(true(), X, Y)] = [1] X + [4] 879.53/298.49 > [0] 879.53/298.49 = [mark(X)] 879.53/298.49 879.53/298.49 [a__if(false(), X, Y)] = [1] X + [0] 879.53/298.49 >= [0] 879.53/298.49 = [mark(Y)] 879.53/298.49 879.53/298.49 [mark(c())] = [0] 879.53/298.49 >= [0] 879.53/298.49 = [c()] 879.53/298.49 879.53/298.49 [mark(f(X))] = [0] 879.53/298.49 >= [0] 879.53/298.49 = [a__f(mark(X))] 879.53/298.49 879.53/298.49 [mark(true())] = [0] 879.53/298.49 ? [4] 879.53/298.49 = [true()] 879.53/298.49 879.53/298.49 [mark(false())] = [0] 879.53/298.49 >= [0] 879.53/298.49 = [false()] 879.53/298.49 879.53/298.49 [mark(if(X1, X2, X3))] = [0] 879.53/298.49 >= [0] 879.53/298.49 = [a__if(mark(X1), mark(X2), X3)] 879.53/298.49 879.53/298.49 879.53/298.49 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 879.53/298.49 879.53/298.49 We are left with following problem, upon which TcT provides the 879.53/298.49 certificate MAYBE. 879.53/298.49 879.53/298.49 Strict Trs: 879.53/298.49 { a__f(X) -> f(X) 879.53/298.49 , a__if(X1, X2, X3) -> if(X1, X2, X3) 879.53/298.49 , mark(c()) -> c() 879.53/298.49 , mark(f(X)) -> a__f(mark(X)) 879.53/298.49 , mark(true()) -> true() 879.53/298.49 , mark(false()) -> false() 879.53/298.49 , mark(if(X1, X2, X3)) -> a__if(mark(X1), mark(X2), X3) } 879.53/298.49 Weak Trs: 879.53/298.49 { a__f(X) -> a__if(mark(X), c(), f(true())) 879.53/298.49 , a__if(true(), X, Y) -> mark(X) 879.53/298.49 , a__if(false(), X, Y) -> mark(Y) } 879.53/298.49 Obligation: 879.53/298.49 innermost runtime complexity 879.53/298.49 Answer: 879.53/298.49 MAYBE 879.53/298.49 879.53/298.49 The weightgap principle applies (using the following nonconstant 879.53/298.50 growth matrix-interpretation) 879.53/298.50 879.53/298.50 The following argument positions are usable: 879.53/298.50 Uargs(a__f) = {1}, Uargs(a__if) = {1, 2} 879.53/298.50 879.53/298.50 TcT has computed the following matrix interpretation satisfying 879.53/298.50 not(EDA) and not(IDA(1)). 879.53/298.50 879.53/298.50 [a__f](x1) = [1] x1 + [1] 879.53/298.50 879.53/298.50 [a__if](x1, x2, x3) = [1] x1 + [1] x2 + [0] 879.53/298.50 879.53/298.50 [mark](x1) = [0] 879.53/298.50 879.53/298.50 [c] = [0] 879.53/298.50 879.53/298.50 [f](x1) = [0] 879.53/298.50 879.53/298.50 [true] = [4] 879.53/298.50 879.53/298.50 [false] = [4] 879.53/298.50 879.53/298.50 [if](x1, x2, x3) = [1] x1 + [1] x2 + [7] 879.53/298.50 879.53/298.50 The order satisfies the following ordering constraints: 879.53/298.50 879.53/298.50 [a__f(X)] = [1] X + [1] 879.53/298.50 > [0] 879.53/298.50 = [a__if(mark(X), c(), f(true()))] 879.53/298.50 879.53/298.50 [a__f(X)] = [1] X + [1] 879.53/298.50 > [0] 879.53/298.50 = [f(X)] 879.53/298.50 879.53/298.50 [a__if(X1, X2, X3)] = [1] X1 + [1] X2 + [0] 879.53/298.50 ? [1] X1 + [1] X2 + [7] 879.53/298.50 = [if(X1, X2, X3)] 879.53/298.50 879.53/298.50 [a__if(true(), X, Y)] = [1] X + [4] 879.53/298.50 > [0] 879.53/298.50 = [mark(X)] 879.53/298.50 879.53/298.50 [a__if(false(), X, Y)] = [1] X + [4] 879.53/298.50 > [0] 879.53/298.50 = [mark(Y)] 879.53/298.50 879.53/298.50 [mark(c())] = [0] 879.53/298.50 >= [0] 879.53/298.50 = [c()] 879.53/298.50 879.53/298.50 [mark(f(X))] = [0] 879.53/298.50 ? [1] 879.53/298.50 = [a__f(mark(X))] 879.53/298.50 879.53/298.50 [mark(true())] = [0] 879.53/298.50 ? [4] 879.53/298.50 = [true()] 879.53/298.50 879.53/298.50 [mark(false())] = [0] 879.53/298.50 ? [4] 879.53/298.50 = [false()] 879.53/298.50 879.53/298.50 [mark(if(X1, X2, X3))] = [0] 879.53/298.50 >= [0] 879.53/298.50 = [a__if(mark(X1), mark(X2), X3)] 879.53/298.50 879.53/298.50 879.53/298.50 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 879.53/298.50 879.53/298.50 We are left with following problem, upon which TcT provides the 879.53/298.50 certificate MAYBE. 879.53/298.50 879.53/298.50 Strict Trs: 879.53/298.50 { a__if(X1, X2, X3) -> if(X1, X2, X3) 879.53/298.50 , mark(c()) -> c() 879.53/298.50 , mark(f(X)) -> a__f(mark(X)) 879.53/298.50 , mark(true()) -> true() 879.53/298.50 , mark(false()) -> false() 879.53/298.50 , mark(if(X1, X2, X3)) -> a__if(mark(X1), mark(X2), X3) } 879.53/298.50 Weak Trs: 879.53/298.50 { a__f(X) -> a__if(mark(X), c(), f(true())) 879.53/298.50 , a__f(X) -> f(X) 879.53/298.50 , a__if(true(), X, Y) -> mark(X) 879.53/298.50 , a__if(false(), X, Y) -> mark(Y) } 879.53/298.50 Obligation: 879.53/298.50 innermost runtime complexity 879.53/298.50 Answer: 879.53/298.50 MAYBE 879.53/298.50 879.53/298.50 The weightgap principle applies (using the following nonconstant 879.53/298.50 growth matrix-interpretation) 879.53/298.50 879.53/298.50 The following argument positions are usable: 879.53/298.50 Uargs(a__f) = {1}, Uargs(a__if) = {1, 2} 879.53/298.50 879.53/298.50 TcT has computed the following matrix interpretation satisfying 879.53/298.50 not(EDA) and not(IDA(1)). 879.53/298.50 879.53/298.50 [a__f](x1) = [1] x1 + [1] 879.53/298.50 879.53/298.50 [a__if](x1, x2, x3) = [1] x1 + [1] x2 + [1] 879.53/298.50 879.53/298.50 [mark](x1) = [0] 879.53/298.50 879.53/298.50 [c] = [0] 879.53/298.50 879.53/298.50 [f](x1) = [1] 879.53/298.50 879.53/298.50 [true] = [4] 879.53/298.50 879.53/298.50 [false] = [4] 879.53/298.50 879.53/298.50 [if](x1, x2, x3) = [1] x1 + [1] x2 + [0] 879.53/298.50 879.53/298.50 The order satisfies the following ordering constraints: 879.53/298.50 879.53/298.50 [a__f(X)] = [1] X + [1] 879.53/298.50 >= [1] 879.53/298.50 = [a__if(mark(X), c(), f(true()))] 879.53/298.50 879.53/298.50 [a__f(X)] = [1] X + [1] 879.53/298.50 >= [1] 879.53/298.50 = [f(X)] 879.53/298.50 879.53/298.50 [a__if(X1, X2, X3)] = [1] X1 + [1] X2 + [1] 879.53/298.50 > [1] X1 + [1] X2 + [0] 879.53/298.50 = [if(X1, X2, X3)] 879.53/298.50 879.53/298.50 [a__if(true(), X, Y)] = [1] X + [5] 879.53/298.50 > [0] 879.53/298.50 = [mark(X)] 879.53/298.50 879.53/298.50 [a__if(false(), X, Y)] = [1] X + [5] 879.53/298.50 > [0] 879.53/298.50 = [mark(Y)] 879.53/298.50 879.53/298.50 [mark(c())] = [0] 879.53/298.50 >= [0] 879.53/298.50 = [c()] 879.53/298.50 879.53/298.50 [mark(f(X))] = [0] 879.53/298.50 ? [1] 879.53/298.50 = [a__f(mark(X))] 879.53/298.50 879.91/298.50 [mark(true())] = [0] 879.91/298.50 ? [4] 879.91/298.50 = [true()] 879.91/298.50 879.91/298.50 [mark(false())] = [0] 879.91/298.50 ? [4] 879.91/298.50 = [false()] 879.91/298.50 879.91/298.50 [mark(if(X1, X2, X3))] = [0] 879.91/298.50 ? [1] 879.91/298.50 = [a__if(mark(X1), mark(X2), X3)] 879.91/298.50 879.91/298.50 879.91/298.50 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 879.91/298.50 879.91/298.50 We are left with following problem, upon which TcT provides the 879.91/298.50 certificate MAYBE. 879.91/298.50 879.91/298.50 Strict Trs: 879.91/298.50 { mark(c()) -> c() 879.91/298.50 , mark(f(X)) -> a__f(mark(X)) 879.91/298.50 , mark(true()) -> true() 879.91/298.50 , mark(false()) -> false() 879.91/298.50 , mark(if(X1, X2, X3)) -> a__if(mark(X1), mark(X2), X3) } 879.91/298.50 Weak Trs: 879.91/298.50 { a__f(X) -> a__if(mark(X), c(), f(true())) 879.91/298.50 , a__f(X) -> f(X) 879.91/298.50 , a__if(X1, X2, X3) -> if(X1, X2, X3) 879.91/298.50 , a__if(true(), X, Y) -> mark(X) 879.91/298.50 , a__if(false(), X, Y) -> mark(Y) } 879.91/298.50 Obligation: 879.91/298.50 innermost runtime complexity 879.91/298.50 Answer: 879.91/298.50 MAYBE 879.91/298.50 879.91/298.50 The weightgap principle applies (using the following nonconstant 879.91/298.50 growth matrix-interpretation) 879.91/298.50 879.91/298.50 The following argument positions are usable: 879.91/298.50 Uargs(a__f) = {1}, Uargs(a__if) = {1, 2} 879.91/298.50 879.91/298.50 TcT has computed the following matrix interpretation satisfying 879.91/298.50 not(EDA) and not(IDA(1)). 879.91/298.50 879.91/298.50 [a__f](x1) = [1] x1 + [4] 879.91/298.50 879.91/298.50 [a__if](x1, x2, x3) = [1] x1 + [1] x2 + [1] x3 + [1] 879.91/298.50 879.91/298.50 [mark](x1) = [1] x1 + [1] 879.91/298.50 879.91/298.50 [c] = [0] 879.91/298.50 879.91/298.50 [f](x1) = [1] x1 + [0] 879.91/298.50 879.91/298.50 [true] = [0] 879.91/298.50 879.91/298.50 [false] = [3] 879.91/298.50 879.91/298.50 [if](x1, x2, x3) = [1] x1 + [1] x2 + [1] x3 + [0] 879.91/298.50 879.91/298.50 The order satisfies the following ordering constraints: 879.91/298.50 879.91/298.50 [a__f(X)] = [1] X + [4] 879.91/298.50 > [1] X + [2] 879.91/298.50 = [a__if(mark(X), c(), f(true()))] 879.91/298.50 879.91/298.50 [a__f(X)] = [1] X + [4] 879.91/298.50 > [1] X + [0] 879.91/298.50 = [f(X)] 879.91/298.50 879.91/298.50 [a__if(X1, X2, X3)] = [1] X1 + [1] X2 + [1] X3 + [1] 879.91/298.50 > [1] X1 + [1] X2 + [1] X3 + [0] 879.91/298.50 = [if(X1, X2, X3)] 879.91/298.50 879.91/298.50 [a__if(true(), X, Y)] = [1] X + [1] Y + [1] 879.91/298.50 >= [1] X + [1] 879.91/298.50 = [mark(X)] 879.91/298.50 879.91/298.50 [a__if(false(), X, Y)] = [1] X + [1] Y + [4] 879.91/298.50 > [1] Y + [1] 879.91/298.50 = [mark(Y)] 879.91/298.50 879.91/298.50 [mark(c())] = [1] 879.91/298.50 > [0] 879.91/298.50 = [c()] 879.91/298.50 879.91/298.50 [mark(f(X))] = [1] X + [1] 879.91/298.50 ? [1] X + [5] 879.91/298.50 = [a__f(mark(X))] 879.91/298.50 879.91/298.50 [mark(true())] = [1] 879.91/298.50 > [0] 879.91/298.50 = [true()] 879.91/298.50 879.91/298.50 [mark(false())] = [4] 879.91/298.50 > [3] 879.91/298.50 = [false()] 879.91/298.50 879.91/298.50 [mark(if(X1, X2, X3))] = [1] X1 + [1] X2 + [1] X3 + [1] 879.91/298.50 ? [1] X1 + [1] X2 + [1] X3 + [3] 879.91/298.50 = [a__if(mark(X1), mark(X2), X3)] 879.91/298.50 879.91/298.50 879.91/298.50 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 879.91/298.50 879.91/298.50 We are left with following problem, upon which TcT provides the 879.91/298.50 certificate MAYBE. 879.91/298.50 879.91/298.50 Strict Trs: 879.91/298.50 { mark(f(X)) -> a__f(mark(X)) 879.91/298.50 , mark(if(X1, X2, X3)) -> a__if(mark(X1), mark(X2), X3) } 879.91/298.50 Weak Trs: 879.91/298.50 { a__f(X) -> a__if(mark(X), c(), f(true())) 879.91/298.50 , a__f(X) -> f(X) 879.91/298.50 , a__if(X1, X2, X3) -> if(X1, X2, X3) 879.91/298.50 , a__if(true(), X, Y) -> mark(X) 879.91/298.50 , a__if(false(), X, Y) -> mark(Y) 879.91/298.50 , mark(c()) -> c() 879.91/298.50 , mark(true()) -> true() 879.91/298.50 , mark(false()) -> false() } 879.91/298.50 Obligation: 879.91/298.50 innermost runtime complexity 879.91/298.50 Answer: 879.91/298.50 MAYBE 879.91/298.50 879.91/298.50 None of the processors succeeded. 879.91/298.50 879.91/298.50 Details of failed attempt(s): 879.91/298.50 ----------------------------- 879.91/298.50 1) 'empty' failed due to the following reason: 879.91/298.50 879.91/298.50 Empty strict component of the problem is NOT empty. 879.91/298.50 879.91/298.50 2) 'With Problem ...' failed due to the following reason: 879.91/298.50 879.91/298.50 None of the processors succeeded. 879.91/298.50 879.91/298.50 Details of failed attempt(s): 879.91/298.50 ----------------------------- 879.91/298.50 1) 'empty' failed due to the following reason: 879.91/298.50 879.91/298.50 Empty strict component of the problem is NOT empty. 879.91/298.50 879.91/298.50 2) 'Fastest' failed due to the following reason: 879.91/298.50 879.91/298.50 None of the processors succeeded. 879.91/298.50 879.91/298.50 Details of failed attempt(s): 879.91/298.50 ----------------------------- 879.91/298.50 1) 'With Problem ...' failed due to the following reason: 879.91/298.50 879.91/298.50 None of the processors succeeded. 879.91/298.50 879.91/298.50 Details of failed attempt(s): 879.91/298.50 ----------------------------- 879.91/298.50 1) 'empty' failed due to the following reason: 879.91/298.50 879.91/298.50 Empty strict component of the problem is NOT empty. 879.91/298.50 879.91/298.50 2) 'With Problem ...' failed due to the following reason: 879.91/298.50 879.91/298.50 None of the processors succeeded. 879.91/298.50 879.91/298.50 Details of failed attempt(s): 879.91/298.50 ----------------------------- 879.91/298.50 1) 'empty' failed due to the following reason: 879.91/298.50 879.91/298.50 Empty strict component of the problem is NOT empty. 879.91/298.50 879.91/298.50 2) 'With Problem ...' failed due to the following reason: 879.91/298.50 879.91/298.50 None of the processors succeeded. 879.91/298.50 879.91/298.50 Details of failed attempt(s): 879.91/298.50 ----------------------------- 879.91/298.50 1) 'empty' failed due to the following reason: 879.91/298.50 879.91/298.50 Empty strict component of the problem is NOT empty. 879.91/298.50 879.91/298.50 2) 'With Problem ...' failed due to the following reason: 879.91/298.50 879.91/298.50 Empty strict component of the problem is NOT empty. 879.91/298.50 879.91/298.50 879.91/298.50 879.91/298.50 879.91/298.50 2) 'With Problem ...' failed due to the following reason: 879.91/298.50 879.91/298.50 None of the processors succeeded. 879.91/298.50 879.91/298.50 Details of failed attempt(s): 879.91/298.50 ----------------------------- 879.91/298.50 1) 'empty' failed due to the following reason: 879.91/298.50 879.91/298.50 Empty strict component of the problem is NOT empty. 879.91/298.50 879.91/298.50 2) 'With Problem ...' failed due to the following reason: 879.91/298.50 879.91/298.50 Empty strict component of the problem is NOT empty. 879.91/298.50 879.91/298.50 879.91/298.50 879.91/298.50 879.91/298.50 879.91/298.50 3) 'Best' failed due to the following reason: 879.91/298.50 879.91/298.50 None of the processors succeeded. 879.91/298.50 879.91/298.50 Details of failed attempt(s): 879.91/298.50 ----------------------------- 879.91/298.50 1) 'Polynomial Path Order (PS) (timeout of 297 seconds)' failed due 879.91/298.50 to the following reason: 879.91/298.50 879.91/298.50 The input cannot be shown compatible 879.91/298.50 879.91/298.50 2) 'bsearch-popstar (timeout of 297 seconds)' failed due to the 879.91/298.50 following reason: 879.91/298.50 879.91/298.50 The input cannot be shown compatible 879.91/298.50 879.91/298.50 879.91/298.50 879.91/298.50 879.91/298.50 879.91/298.50 Arrrr.. 880.32/298.98 EOF