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