MAYBE 478.30/297.17 MAYBE 478.30/297.17 478.30/297.17 We are left with following problem, upon which TcT provides the 478.30/297.17 certificate MAYBE. 478.30/297.17 478.30/297.17 Strict Trs: 478.30/297.17 { from(X) -> cons(X, n__from(s(X))) 478.30/297.17 , from(X) -> n__from(X) 478.30/297.17 , sel(s(N), cons(X, XS)) -> sel(N, activate(XS)) 478.30/297.17 , sel(0(), cons(X, XS)) -> X 478.30/297.17 , activate(X) -> X 478.30/297.17 , activate(n__from(X)) -> from(X) 478.30/297.17 , activate(n__zWquot(X1, X2)) -> zWquot(X1, X2) 478.30/297.17 , minus(X, 0()) -> 0() 478.30/297.17 , minus(s(X), s(Y)) -> minus(X, Y) 478.30/297.17 , quot(s(X), s(Y)) -> s(quot(minus(X, Y), s(Y))) 478.30/297.17 , quot(0(), s(Y)) -> 0() 478.30/297.17 , zWquot(X1, X2) -> n__zWquot(X1, X2) 478.30/297.17 , zWquot(XS, nil()) -> nil() 478.30/297.17 , zWquot(cons(X, XS), cons(Y, YS)) -> 478.30/297.17 cons(quot(X, Y), n__zWquot(activate(XS), activate(YS))) 478.30/297.17 , zWquot(nil(), XS) -> nil() } 478.30/297.17 Obligation: 478.30/297.17 innermost runtime complexity 478.30/297.17 Answer: 478.30/297.17 MAYBE 478.30/297.17 478.30/297.17 None of the processors succeeded. 478.30/297.17 478.30/297.17 Details of failed attempt(s): 478.30/297.17 ----------------------------- 478.30/297.17 1) 'empty' failed due to the following reason: 478.30/297.17 478.30/297.17 Empty strict component of the problem is NOT empty. 478.30/297.17 478.30/297.17 2) 'Best' failed due to the following reason: 478.30/297.17 478.30/297.17 None of the processors succeeded. 478.30/297.17 478.30/297.17 Details of failed attempt(s): 478.30/297.17 ----------------------------- 478.30/297.17 1) 'With Problem ... (timeout of 297 seconds)' failed due to the 478.30/297.17 following reason: 478.30/297.17 478.30/297.17 Computation stopped due to timeout after 297.0 seconds. 478.30/297.17 478.30/297.17 2) 'Best' failed due to the following reason: 478.30/297.17 478.30/297.17 None of the processors succeeded. 478.30/297.17 478.30/297.17 Details of failed attempt(s): 478.30/297.17 ----------------------------- 478.30/297.17 1) 'With Problem ... (timeout of 148 seconds) (timeout of 297 478.30/297.17 seconds)' failed due to the following reason: 478.30/297.17 478.30/297.17 None of the processors succeeded. 478.30/297.17 478.30/297.17 Details of failed attempt(s): 478.30/297.17 ----------------------------- 478.30/297.17 1) 'empty' failed due to the following reason: 478.30/297.17 478.30/297.17 Empty strict component of the problem is NOT empty. 478.30/297.17 478.30/297.17 2) 'With Problem ...' failed due to the following reason: 478.30/297.17 478.30/297.17 None of the processors succeeded. 478.30/297.17 478.30/297.17 Details of failed attempt(s): 478.30/297.17 ----------------------------- 478.30/297.17 1) 'empty' failed due to the following reason: 478.30/297.17 478.30/297.17 Empty strict component of the problem is NOT empty. 478.30/297.17 478.30/297.17 2) 'Fastest' failed due to the following reason: 478.30/297.17 478.30/297.17 None of the processors succeeded. 478.30/297.17 478.30/297.17 Details of failed attempt(s): 478.30/297.17 ----------------------------- 478.30/297.17 1) 'With Problem ...' failed due to the following reason: 478.30/297.17 478.30/297.17 None of the processors succeeded. 478.30/297.17 478.30/297.17 Details of failed attempt(s): 478.30/297.17 ----------------------------- 478.30/297.17 1) 'empty' failed due to the following reason: 478.30/297.17 478.30/297.17 Empty strict component of the problem is NOT empty. 478.30/297.17 478.30/297.17 2) 'With Problem ...' failed due to the following reason: 478.30/297.17 478.30/297.17 The weightgap principle applies (using the following nonconstant 478.30/297.17 growth matrix-interpretation) 478.30/297.17 478.30/297.17 The following argument positions are usable: 478.30/297.17 Uargs(cons) = {1, 2}, Uargs(s) = {1}, Uargs(sel) = {2}, 478.30/297.17 Uargs(quot) = {1}, Uargs(n__zWquot) = {1, 2} 478.30/297.17 478.30/297.17 TcT has computed the following matrix interpretation satisfying 478.30/297.17 not(EDA) and not(IDA(1)). 478.30/297.17 478.30/297.17 [from](x1) = [1 0] x1 + [0] 478.30/297.17 [0 0] [0] 478.30/297.17 478.30/297.17 [cons](x1, x2) = [1 0] x1 + [1 0] x2 + [0] 478.30/297.17 [0 0] [0 1] [0] 478.30/297.17 478.30/297.17 [n__from](x1) = [0 0] x1 + [0] 478.30/297.17 [1 0] [1] 478.30/297.17 478.30/297.17 [s](x1) = [1 0] x1 + [0] 478.30/297.17 [0 0] [0] 478.30/297.17 478.30/297.17 [sel](x1, x2) = [0 0] x1 + [1 1] x2 + [0] 478.30/297.17 [1 1] [0 0] [7] 478.30/297.17 478.30/297.17 [0] = [0] 478.30/297.17 [0] 478.30/297.17 478.30/297.17 [activate](x1) = [1 1] x1 + [0] 478.30/297.17 [0 0] [0] 478.30/297.17 478.30/297.17 [minus](x1, x2) = [0] 478.30/297.17 [0] 478.30/297.17 478.30/297.17 [quot](x1, x2) = [1 0] x1 + [0] 478.30/297.17 [0 0] [0] 478.30/297.17 478.30/297.17 [zWquot](x1, x2) = [1 1] x1 + [1 1] x2 + [0] 478.30/297.17 [0 0] [0 0] [0] 478.30/297.17 478.30/297.17 [nil] = [0] 478.30/297.17 [0] 478.30/297.17 478.30/297.17 [n__zWquot](x1, x2) = [1 1] x1 + [1 1] x2 + [0] 478.30/297.17 [0 0] [0 0] [0] 478.30/297.17 478.30/297.17 The order satisfies the following ordering constraints: 478.30/297.17 478.30/297.17 [from(X)] = [1 0] X + [0] 478.30/297.17 [0 0] [0] 478.30/297.17 ? [1 0] X + [0] 478.30/297.17 [1 0] [1] 478.30/297.17 = [cons(X, n__from(s(X)))] 478.30/297.17 478.30/297.17 [from(X)] = [1 0] X + [0] 478.30/297.17 [0 0] [0] 478.30/297.17 ? [0 0] X + [0] 478.30/297.17 [1 0] [1] 478.30/297.17 = [n__from(X)] 478.30/297.17 478.30/297.17 [sel(s(N), cons(X, XS))] = [1 0] X + [1 1] XS + [0 0] N + [0] 478.30/297.17 [0 0] [0 0] [1 0] [7] 478.30/297.17 ? [1 1] XS + [0 0] N + [0] 478.30/297.17 [0 0] [1 1] [7] 478.30/297.17 = [sel(N, activate(XS))] 478.30/297.17 478.30/297.17 [sel(0(), cons(X, XS))] = [1 0] X + [1 1] XS + [0] 478.30/297.17 [0 0] [0 0] [7] 478.30/297.17 ? [1 0] X + [0] 478.30/297.17 [0 1] [0] 478.30/297.17 = [X] 478.30/297.17 478.30/297.17 [activate(X)] = [1 1] X + [0] 478.30/297.17 [0 0] [0] 478.30/297.17 ? [1 0] X + [0] 478.30/297.17 [0 1] [0] 478.30/297.17 = [X] 478.30/297.17 478.30/297.17 [activate(n__from(X))] = [1 0] X + [1] 478.30/297.17 [0 0] [0] 478.30/297.17 > [1 0] X + [0] 478.30/297.17 [0 0] [0] 478.30/297.17 = [from(X)] 478.30/297.17 478.30/297.17 [activate(n__zWquot(X1, X2))] = [1 1] X1 + [1 1] X2 + [0] 478.30/297.17 [0 0] [0 0] [0] 478.30/297.17 >= [1 1] X1 + [1 1] X2 + [0] 478.30/297.17 [0 0] [0 0] [0] 478.30/297.17 = [zWquot(X1, X2)] 478.30/297.17 478.30/297.17 [minus(X, 0())] = [0] 478.30/297.17 [0] 478.30/297.17 >= [0] 478.30/297.17 [0] 478.30/297.17 = [0()] 478.30/297.17 478.30/297.17 [minus(s(X), s(Y))] = [0] 478.30/297.17 [0] 478.30/297.17 >= [0] 478.30/297.17 [0] 478.30/297.17 = [minus(X, Y)] 478.30/297.17 478.30/297.17 [quot(s(X), s(Y))] = [1 0] X + [0] 478.30/297.17 [0 0] [0] 478.30/297.17 >= [0] 478.30/297.17 [0] 478.30/297.17 = [s(quot(minus(X, Y), s(Y)))] 478.30/297.17 478.30/297.17 [quot(0(), s(Y))] = [0] 478.30/297.17 [0] 478.30/297.17 >= [0] 478.30/297.17 [0] 478.30/297.17 = [0()] 478.30/297.17 478.30/297.17 [zWquot(X1, X2)] = [1 1] X1 + [1 1] X2 + [0] 478.30/297.17 [0 0] [0 0] [0] 478.30/297.17 >= [1 1] X1 + [1 1] X2 + [0] 478.30/297.17 [0 0] [0 0] [0] 478.30/297.17 = [n__zWquot(X1, X2)] 478.30/297.17 478.30/297.17 [zWquot(XS, nil())] = [1 1] XS + [0] 478.30/297.17 [0 0] [0] 478.30/297.17 >= [0] 478.30/297.17 [0] 478.30/297.17 = [nil()] 478.30/297.17 478.30/297.17 [zWquot(cons(X, XS), cons(Y, YS))] = [1 0] X + [1 1] XS + [1 0] Y + [1 1] YS + [0] 478.30/297.17 [0 0] [0 0] [0 0] [0 0] [0] 478.30/297.17 >= [1 0] X + [1 1] XS + [1 1] YS + [0] 478.30/297.17 [0 0] [0 0] [0 0] [0] 478.30/297.17 = [cons(quot(X, Y), n__zWquot(activate(XS), activate(YS)))] 478.30/297.17 478.30/297.17 [zWquot(nil(), XS)] = [1 1] XS + [0] 478.30/297.17 [0 0] [0] 478.30/297.17 >= [0] 478.30/297.17 [0] 478.30/297.17 = [nil()] 478.30/297.17 478.30/297.17 478.30/297.17 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 478.30/297.17 478.30/297.17 We are left with following problem, upon which TcT provides the 478.30/297.17 certificate MAYBE. 478.30/297.17 478.30/297.17 Strict Trs: 478.30/297.17 { from(X) -> cons(X, n__from(s(X))) 478.30/297.17 , from(X) -> n__from(X) 478.30/297.17 , sel(s(N), cons(X, XS)) -> sel(N, activate(XS)) 478.30/297.17 , sel(0(), cons(X, XS)) -> X 478.30/297.17 , activate(X) -> X 478.30/297.17 , activate(n__zWquot(X1, X2)) -> zWquot(X1, X2) 478.30/297.17 , minus(X, 0()) -> 0() 478.30/297.17 , minus(s(X), s(Y)) -> minus(X, Y) 478.30/297.17 , quot(s(X), s(Y)) -> s(quot(minus(X, Y), s(Y))) 478.30/297.17 , quot(0(), s(Y)) -> 0() 478.30/297.17 , zWquot(X1, X2) -> n__zWquot(X1, X2) 478.30/297.17 , zWquot(XS, nil()) -> nil() 478.30/297.17 , zWquot(cons(X, XS), cons(Y, YS)) -> 478.30/297.17 cons(quot(X, Y), n__zWquot(activate(XS), activate(YS))) 478.30/297.17 , zWquot(nil(), XS) -> nil() } 478.30/297.17 Weak Trs: { activate(n__from(X)) -> from(X) } 478.30/297.17 Obligation: 478.30/297.17 innermost runtime complexity 478.30/297.17 Answer: 478.30/297.17 MAYBE 478.30/297.17 478.30/297.17 The weightgap principle applies (using the following nonconstant 478.30/297.17 growth matrix-interpretation) 478.30/297.17 478.30/297.17 The following argument positions are usable: 478.30/297.17 Uargs(cons) = {1, 2}, Uargs(s) = {1}, Uargs(sel) = {2}, 478.30/297.17 Uargs(quot) = {1}, Uargs(n__zWquot) = {1, 2} 478.30/297.17 478.30/297.17 TcT has computed the following matrix interpretation satisfying 478.30/297.17 not(EDA) and not(IDA(1)). 478.30/297.17 478.30/297.17 [from](x1) = [1 0] x1 + [0] 478.30/297.17 [0 0] [0] 478.30/297.17 478.30/297.17 [cons](x1, x2) = [1 0] x1 + [1 0] x2 + [0] 478.30/297.17 [0 0] [0 1] [0] 478.30/297.17 478.30/297.17 [n__from](x1) = [0 0] x1 + [0] 478.30/297.17 [1 0] [0] 478.30/297.17 478.30/297.17 [s](x1) = [1 0] x1 + [0] 478.30/297.17 [0 0] [0] 478.30/297.17 478.30/297.17 [sel](x1, x2) = [0 0] x1 + [1 1] x2 + [0] 478.30/297.17 [1 1] [0 0] [7] 478.30/297.17 478.30/297.17 [0] = [0] 478.30/297.17 [0] 478.30/297.17 478.30/297.17 [activate](x1) = [1 1] x1 + [0] 478.30/297.17 [0 0] [0] 478.30/297.17 478.30/297.17 [minus](x1, x2) = [0] 478.30/297.17 [0] 478.30/297.17 478.30/297.17 [quot](x1, x2) = [1 0] x1 + [0] 478.30/297.17 [0 0] [0] 478.30/297.17 478.30/297.17 [zWquot](x1, x2) = [1 1] x1 + [1 1] x2 + [4] 478.30/297.17 [0 0] [0 0] [4] 478.30/297.17 478.30/297.17 [nil] = [0] 478.30/297.17 [0] 478.30/297.17 478.30/297.17 [n__zWquot](x1, x2) = [1 1] x1 + [1 1] x2 + [0] 478.30/297.17 [0 0] [0 0] [0] 478.30/297.18 478.30/297.18 The order satisfies the following ordering constraints: 478.30/297.18 478.30/297.18 [from(X)] = [1 0] X + [0] 478.30/297.18 [0 0] [0] 478.30/297.18 ? [1 0] X + [0] 478.30/297.18 [1 0] [0] 478.30/297.18 = [cons(X, n__from(s(X)))] 478.30/297.18 478.30/297.18 [from(X)] = [1 0] X + [0] 478.30/297.18 [0 0] [0] 478.30/297.18 ? [0 0] X + [0] 478.30/297.18 [1 0] [0] 478.30/297.18 = [n__from(X)] 478.30/297.18 478.30/297.18 [sel(s(N), cons(X, XS))] = [1 0] X + [1 1] XS + [0 0] N + [0] 478.30/297.18 [0 0] [0 0] [1 0] [7] 478.30/297.18 ? [1 1] XS + [0 0] N + [0] 478.30/297.18 [0 0] [1 1] [7] 478.30/297.18 = [sel(N, activate(XS))] 478.30/297.18 478.30/297.18 [sel(0(), cons(X, XS))] = [1 0] X + [1 1] XS + [0] 478.30/297.18 [0 0] [0 0] [7] 478.30/297.18 ? [1 0] X + [0] 478.30/297.18 [0 1] [0] 478.30/297.18 = [X] 478.30/297.18 478.30/297.18 [activate(X)] = [1 1] X + [0] 478.30/297.18 [0 0] [0] 478.30/297.18 ? [1 0] X + [0] 478.30/297.18 [0 1] [0] 478.30/297.18 = [X] 478.30/297.18 478.30/297.18 [activate(n__from(X))] = [1 0] X + [0] 478.30/297.18 [0 0] [0] 478.30/297.18 >= [1 0] X + [0] 478.30/297.18 [0 0] [0] 478.30/297.18 = [from(X)] 478.30/297.18 478.30/297.18 [activate(n__zWquot(X1, X2))] = [1 1] X1 + [1 1] X2 + [0] 478.30/297.18 [0 0] [0 0] [0] 478.30/297.18 ? [1 1] X1 + [1 1] X2 + [4] 478.30/297.18 [0 0] [0 0] [4] 478.30/297.18 = [zWquot(X1, X2)] 478.30/297.18 478.30/297.18 [minus(X, 0())] = [0] 478.30/297.18 [0] 478.30/297.18 >= [0] 478.30/297.18 [0] 478.30/297.18 = [0()] 478.30/297.18 478.30/297.18 [minus(s(X), s(Y))] = [0] 478.30/297.18 [0] 478.30/297.18 >= [0] 478.30/297.18 [0] 478.30/297.18 = [minus(X, Y)] 478.30/297.18 478.30/297.18 [quot(s(X), s(Y))] = [1 0] X + [0] 478.30/297.18 [0 0] [0] 478.30/297.18 >= [0] 478.30/297.18 [0] 478.30/297.18 = [s(quot(minus(X, Y), s(Y)))] 478.30/297.18 478.30/297.18 [quot(0(), s(Y))] = [0] 478.30/297.18 [0] 478.30/297.18 >= [0] 478.30/297.18 [0] 478.30/297.18 = [0()] 478.30/297.18 478.30/297.18 [zWquot(X1, X2)] = [1 1] X1 + [1 1] X2 + [4] 478.30/297.18 [0 0] [0 0] [4] 478.30/297.18 > [1 1] X1 + [1 1] X2 + [0] 478.30/297.18 [0 0] [0 0] [0] 478.30/297.18 = [n__zWquot(X1, X2)] 478.30/297.18 478.30/297.18 [zWquot(XS, nil())] = [1 1] XS + [4] 478.30/297.18 [0 0] [4] 478.30/297.18 > [0] 478.30/297.18 [0] 478.30/297.18 = [nil()] 478.30/297.18 478.30/297.18 [zWquot(cons(X, XS), cons(Y, YS))] = [1 0] X + [1 1] XS + [1 0] Y + [1 1] YS + [4] 478.30/297.18 [0 0] [0 0] [0 0] [0 0] [4] 478.30/297.18 > [1 0] X + [1 1] XS + [1 1] YS + [0] 478.30/297.18 [0 0] [0 0] [0 0] [0] 478.30/297.18 = [cons(quot(X, Y), n__zWquot(activate(XS), activate(YS)))] 478.30/297.18 478.30/297.18 [zWquot(nil(), XS)] = [1 1] XS + [4] 478.30/297.18 [0 0] [4] 478.30/297.18 > [0] 478.30/297.18 [0] 478.30/297.18 = [nil()] 478.30/297.18 478.30/297.18 478.30/297.18 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 478.30/297.18 478.30/297.18 We are left with following problem, upon which TcT provides the 478.30/297.18 certificate MAYBE. 478.30/297.18 478.30/297.18 Strict Trs: 478.30/297.18 { from(X) -> cons(X, n__from(s(X))) 478.30/297.18 , from(X) -> n__from(X) 478.30/297.18 , sel(s(N), cons(X, XS)) -> sel(N, activate(XS)) 478.30/297.18 , sel(0(), cons(X, XS)) -> X 478.30/297.18 , activate(X) -> X 478.30/297.18 , activate(n__zWquot(X1, X2)) -> zWquot(X1, X2) 478.30/297.18 , minus(X, 0()) -> 0() 478.30/297.18 , minus(s(X), s(Y)) -> minus(X, Y) 478.30/297.18 , quot(s(X), s(Y)) -> s(quot(minus(X, Y), s(Y))) 478.30/297.18 , quot(0(), s(Y)) -> 0() } 478.30/297.18 Weak Trs: 478.30/297.18 { activate(n__from(X)) -> from(X) 478.30/297.18 , zWquot(X1, X2) -> n__zWquot(X1, X2) 478.30/297.18 , zWquot(XS, nil()) -> nil() 478.30/297.18 , zWquot(cons(X, XS), cons(Y, YS)) -> 478.30/297.18 cons(quot(X, Y), n__zWquot(activate(XS), activate(YS))) 478.30/297.18 , zWquot(nil(), XS) -> nil() } 478.30/297.18 Obligation: 478.30/297.18 innermost runtime complexity 478.30/297.18 Answer: 478.30/297.18 MAYBE 478.30/297.18 478.30/297.18 The weightgap principle applies (using the following nonconstant 478.30/297.18 growth matrix-interpretation) 478.30/297.18 478.30/297.18 The following argument positions are usable: 478.30/297.18 Uargs(cons) = {1, 2}, Uargs(s) = {1}, Uargs(sel) = {2}, 478.30/297.18 Uargs(quot) = {1}, Uargs(n__zWquot) = {1, 2} 478.30/297.18 478.30/297.18 TcT has computed the following matrix interpretation satisfying 478.30/297.18 not(EDA) and not(IDA(1)). 478.30/297.18 478.30/297.18 [from](x1) = [1 0] x1 + [0] 478.30/297.18 [0 0] [0] 478.30/297.18 478.30/297.18 [cons](x1, x2) = [1 0] x1 + [1 0] x2 + [0] 478.30/297.18 [0 0] [0 1] [0] 478.30/297.18 478.30/297.18 [n__from](x1) = [0 0] x1 + [0] 478.30/297.18 [1 0] [0] 478.30/297.18 478.30/297.18 [s](x1) = [1 0] x1 + [0] 478.30/297.18 [0 0] [0] 478.30/297.18 478.30/297.18 [sel](x1, x2) = [0 0] x1 + [1 1] x2 + [0] 478.30/297.18 [1 1] [0 0] [7] 478.30/297.18 478.30/297.18 [0] = [0] 478.30/297.18 [0] 478.30/297.18 478.30/297.18 [activate](x1) = [1 1] x1 + [0] 478.30/297.18 [0 0] [0] 478.30/297.18 478.30/297.18 [minus](x1, x2) = [1] 478.30/297.18 [0] 478.30/297.18 478.30/297.18 [quot](x1, x2) = [1 0] x1 + [0] 478.30/297.18 [0 0] [0] 478.30/297.18 478.30/297.18 [zWquot](x1, x2) = [1 1] x1 + [1 1] x2 + [1] 478.30/297.18 [0 0] [0 0] [4] 478.30/297.18 478.30/297.18 [nil] = [3] 478.30/297.18 [0] 478.30/297.18 478.30/297.18 [n__zWquot](x1, x2) = [1 1] x1 + [1 1] x2 + [0] 478.30/297.18 [0 0] [0 0] [0] 478.30/297.18 478.30/297.18 The order satisfies the following ordering constraints: 478.30/297.18 478.30/297.18 [from(X)] = [1 0] X + [0] 478.30/297.18 [0 0] [0] 478.30/297.18 ? [1 0] X + [0] 478.30/297.18 [1 0] [0] 478.30/297.18 = [cons(X, n__from(s(X)))] 478.30/297.18 478.30/297.18 [from(X)] = [1 0] X + [0] 478.30/297.18 [0 0] [0] 478.30/297.18 ? [0 0] X + [0] 478.30/297.18 [1 0] [0] 478.30/297.18 = [n__from(X)] 478.30/297.18 478.30/297.18 [sel(s(N), cons(X, XS))] = [1 0] X + [1 1] XS + [0 0] N + [0] 478.30/297.18 [0 0] [0 0] [1 0] [7] 478.30/297.18 ? [1 1] XS + [0 0] N + [0] 478.30/297.18 [0 0] [1 1] [7] 478.30/297.18 = [sel(N, activate(XS))] 478.30/297.18 478.30/297.18 [sel(0(), cons(X, XS))] = [1 0] X + [1 1] XS + [0] 478.30/297.18 [0 0] [0 0] [7] 478.30/297.18 ? [1 0] X + [0] 478.30/297.18 [0 1] [0] 478.30/297.18 = [X] 478.30/297.18 478.30/297.18 [activate(X)] = [1 1] X + [0] 478.30/297.18 [0 0] [0] 478.30/297.18 ? [1 0] X + [0] 478.30/297.18 [0 1] [0] 478.30/297.18 = [X] 478.30/297.18 478.30/297.18 [activate(n__from(X))] = [1 0] X + [0] 478.30/297.18 [0 0] [0] 478.30/297.18 >= [1 0] X + [0] 478.30/297.18 [0 0] [0] 478.30/297.18 = [from(X)] 478.30/297.18 478.30/297.18 [activate(n__zWquot(X1, X2))] = [1 1] X1 + [1 1] X2 + [0] 478.30/297.18 [0 0] [0 0] [0] 478.30/297.18 ? [1 1] X1 + [1 1] X2 + [1] 478.30/297.18 [0 0] [0 0] [4] 478.30/297.18 = [zWquot(X1, X2)] 478.30/297.18 478.30/297.18 [minus(X, 0())] = [1] 478.30/297.18 [0] 478.30/297.18 > [0] 478.30/297.18 [0] 478.30/297.18 = [0()] 478.30/297.18 478.30/297.18 [minus(s(X), s(Y))] = [1] 478.30/297.18 [0] 478.30/297.18 >= [1] 478.30/297.18 [0] 478.30/297.18 = [minus(X, Y)] 478.30/297.18 478.30/297.18 [quot(s(X), s(Y))] = [1 0] X + [0] 478.30/297.18 [0 0] [0] 478.30/297.18 ? [1] 478.30/297.18 [0] 478.30/297.18 = [s(quot(minus(X, Y), s(Y)))] 478.30/297.18 478.30/297.18 [quot(0(), s(Y))] = [0] 478.30/297.18 [0] 478.30/297.18 >= [0] 478.30/297.18 [0] 478.30/297.18 = [0()] 478.30/297.18 478.30/297.18 [zWquot(X1, X2)] = [1 1] X1 + [1 1] X2 + [1] 478.30/297.18 [0 0] [0 0] [4] 478.30/297.18 > [1 1] X1 + [1 1] X2 + [0] 478.30/297.18 [0 0] [0 0] [0] 478.30/297.18 = [n__zWquot(X1, X2)] 478.30/297.18 478.30/297.18 [zWquot(XS, nil())] = [1 1] XS + [4] 478.30/297.18 [0 0] [4] 478.30/297.18 > [3] 478.30/297.18 [0] 478.30/297.18 = [nil()] 478.30/297.18 478.30/297.18 [zWquot(cons(X, XS), cons(Y, YS))] = [1 0] X + [1 1] XS + [1 0] Y + [1 1] YS + [1] 478.30/297.18 [0 0] [0 0] [0 0] [0 0] [4] 478.30/297.18 > [1 0] X + [1 1] XS + [1 1] YS + [0] 478.30/297.18 [0 0] [0 0] [0 0] [0] 478.30/297.18 = [cons(quot(X, Y), n__zWquot(activate(XS), activate(YS)))] 478.30/297.18 478.30/297.18 [zWquot(nil(), XS)] = [1 1] XS + [4] 478.30/297.18 [0 0] [4] 478.30/297.18 > [3] 478.30/297.18 [0] 478.30/297.18 = [nil()] 478.30/297.18 478.30/297.18 478.30/297.18 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 478.30/297.18 478.30/297.18 We are left with following problem, upon which TcT provides the 478.30/297.18 certificate MAYBE. 478.30/297.18 478.30/297.18 Strict Trs: 478.30/297.18 { from(X) -> cons(X, n__from(s(X))) 478.30/297.18 , from(X) -> n__from(X) 478.30/297.18 , sel(s(N), cons(X, XS)) -> sel(N, activate(XS)) 478.30/297.18 , sel(0(), cons(X, XS)) -> X 478.30/297.18 , activate(X) -> X 478.30/297.18 , activate(n__zWquot(X1, X2)) -> zWquot(X1, X2) 478.30/297.18 , minus(s(X), s(Y)) -> minus(X, Y) 478.30/297.18 , quot(s(X), s(Y)) -> s(quot(minus(X, Y), s(Y))) 478.30/297.18 , quot(0(), s(Y)) -> 0() } 478.30/297.18 Weak Trs: 478.30/297.18 { activate(n__from(X)) -> from(X) 478.30/297.18 , minus(X, 0()) -> 0() 478.30/297.18 , zWquot(X1, X2) -> n__zWquot(X1, X2) 478.30/297.18 , zWquot(XS, nil()) -> nil() 478.30/297.18 , zWquot(cons(X, XS), cons(Y, YS)) -> 478.30/297.18 cons(quot(X, Y), n__zWquot(activate(XS), activate(YS))) 478.30/297.18 , zWquot(nil(), XS) -> nil() } 478.30/297.18 Obligation: 478.30/297.18 innermost runtime complexity 478.30/297.18 Answer: 478.30/297.18 MAYBE 478.30/297.18 478.30/297.18 The weightgap principle applies (using the following nonconstant 478.30/297.18 growth matrix-interpretation) 478.30/297.18 478.30/297.18 The following argument positions are usable: 478.30/297.18 Uargs(cons) = {1, 2}, Uargs(s) = {1}, Uargs(sel) = {2}, 478.30/297.18 Uargs(quot) = {1}, Uargs(n__zWquot) = {1, 2} 478.30/297.18 478.30/297.18 TcT has computed the following matrix interpretation satisfying 478.30/297.18 not(EDA) and not(IDA(1)). 478.30/297.18 478.30/297.18 [from](x1) = [1 0] x1 + [0] 478.30/297.18 [0 0] [0] 478.30/297.18 478.30/297.18 [cons](x1, x2) = [1 0] x1 + [1 0] x2 + [0] 478.30/297.18 [0 0] [0 1] [4] 478.30/297.18 478.30/297.18 [n__from](x1) = [0 0] x1 + [0] 478.30/297.18 [1 0] [0] 478.30/297.18 478.30/297.18 [s](x1) = [1 0] x1 + [0] 478.30/297.18 [0 0] [0] 478.30/297.18 478.30/297.18 [sel](x1, x2) = [0 0] x1 + [1 1] x2 + [0] 478.30/297.18 [1 0] [0 0] [7] 478.30/297.18 478.30/297.18 [0] = [0] 478.30/297.18 [0] 478.30/297.18 478.30/297.18 [activate](x1) = [1 1] x1 + [0] 478.30/297.18 [0 0] [0] 478.30/297.18 478.30/297.18 [minus](x1, x2) = [0] 478.30/297.18 [0] 478.30/297.18 478.30/297.18 [quot](x1, x2) = [1 0] x1 + [0] 478.30/297.18 [0 0] [0] 478.30/297.18 478.30/297.18 [zWquot](x1, x2) = [1 1] x1 + [1 1] x2 + [0] 478.30/297.18 [0 0] [0 0] [4] 478.30/297.18 478.30/297.18 [nil] = [0] 478.30/297.18 [0] 478.30/297.18 478.30/297.18 [n__zWquot](x1, x2) = [1 1] x1 + [1 1] x2 + [0] 478.30/297.18 [0 0] [0 0] [0] 478.30/297.18 478.30/297.18 The order satisfies the following ordering constraints: 478.30/297.18 478.30/297.18 [from(X)] = [1 0] X + [0] 478.30/297.18 [0 0] [0] 478.30/297.18 ? [1 0] X + [0] 478.30/297.18 [1 0] [4] 478.30/297.18 = [cons(X, n__from(s(X)))] 478.30/297.18 478.30/297.18 [from(X)] = [1 0] X + [0] 478.30/297.18 [0 0] [0] 478.30/297.18 ? [0 0] X + [0] 478.30/297.18 [1 0] [0] 478.30/297.18 = [n__from(X)] 478.30/297.18 478.30/297.18 [sel(s(N), cons(X, XS))] = [1 0] X + [1 1] XS + [0 0] N + [4] 478.30/297.18 [0 0] [0 0] [1 0] [7] 478.30/297.18 > [1 1] XS + [0 0] N + [0] 478.30/297.18 [0 0] [1 0] [7] 478.30/297.18 = [sel(N, activate(XS))] 478.30/297.18 478.30/297.18 [sel(0(), cons(X, XS))] = [1 0] X + [1 1] XS + [4] 478.30/297.18 [0 0] [0 0] [7] 478.30/297.18 ? [1 0] X + [0] 478.30/297.18 [0 1] [0] 478.30/297.18 = [X] 478.30/297.18 478.30/297.18 [activate(X)] = [1 1] X + [0] 478.30/297.18 [0 0] [0] 478.30/297.18 ? [1 0] X + [0] 478.30/297.18 [0 1] [0] 478.30/297.18 = [X] 478.30/297.18 478.30/297.18 [activate(n__from(X))] = [1 0] X + [0] 478.30/297.18 [0 0] [0] 478.30/297.18 >= [1 0] X + [0] 478.30/297.18 [0 0] [0] 478.30/297.18 = [from(X)] 478.30/297.18 478.30/297.18 [activate(n__zWquot(X1, X2))] = [1 1] X1 + [1 1] X2 + [0] 478.30/297.18 [0 0] [0 0] [0] 478.30/297.18 ? [1 1] X1 + [1 1] X2 + [0] 478.30/297.18 [0 0] [0 0] [4] 478.30/297.18 = [zWquot(X1, X2)] 478.30/297.18 478.30/297.18 [minus(X, 0())] = [0] 478.30/297.18 [0] 478.30/297.18 >= [0] 478.30/297.18 [0] 478.30/297.18 = [0()] 478.30/297.18 478.30/297.18 [minus(s(X), s(Y))] = [0] 478.30/297.18 [0] 478.30/297.18 >= [0] 478.30/297.18 [0] 478.30/297.18 = [minus(X, Y)] 478.30/297.18 478.30/297.18 [quot(s(X), s(Y))] = [1 0] X + [0] 478.30/297.18 [0 0] [0] 478.30/297.18 >= [0] 478.30/297.18 [0] 478.30/297.18 = [s(quot(minus(X, Y), s(Y)))] 478.30/297.18 478.30/297.18 [quot(0(), s(Y))] = [0] 478.30/297.18 [0] 478.30/297.18 >= [0] 478.30/297.18 [0] 478.30/297.18 = [0()] 478.30/297.18 478.30/297.18 [zWquot(X1, X2)] = [1 1] X1 + [1 1] X2 + [0] 478.30/297.18 [0 0] [0 0] [4] 478.30/297.18 >= [1 1] X1 + [1 1] X2 + [0] 478.30/297.18 [0 0] [0 0] [0] 478.30/297.18 = [n__zWquot(X1, X2)] 478.30/297.18 478.30/297.18 [zWquot(XS, nil())] = [1 1] XS + [0] 478.30/297.18 [0 0] [4] 478.30/297.18 >= [0] 478.30/297.18 [0] 478.30/297.18 = [nil()] 478.30/297.18 478.30/297.18 [zWquot(cons(X, XS), cons(Y, YS))] = [1 0] X + [1 1] XS + [1 0] Y + [1 1] YS + [8] 478.30/297.18 [0 0] [0 0] [0 0] [0 0] [4] 478.30/297.18 > [1 0] X + [1 1] XS + [1 1] YS + [0] 478.30/297.18 [0 0] [0 0] [0 0] [4] 478.30/297.18 = [cons(quot(X, Y), n__zWquot(activate(XS), activate(YS)))] 478.30/297.18 478.30/297.18 [zWquot(nil(), XS)] = [1 1] XS + [0] 478.30/297.18 [0 0] [4] 478.30/297.18 >= [0] 478.30/297.18 [0] 478.30/297.18 = [nil()] 478.30/297.18 478.30/297.18 478.30/297.18 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 478.30/297.18 478.30/297.18 We are left with following problem, upon which TcT provides the 478.30/297.18 certificate MAYBE. 478.30/297.18 478.30/297.18 Strict Trs: 478.30/297.18 { from(X) -> cons(X, n__from(s(X))) 478.30/297.18 , from(X) -> n__from(X) 478.30/297.18 , sel(0(), cons(X, XS)) -> X 478.30/297.18 , activate(X) -> X 478.30/297.18 , activate(n__zWquot(X1, X2)) -> zWquot(X1, X2) 478.30/297.18 , minus(s(X), s(Y)) -> minus(X, Y) 478.30/297.18 , quot(s(X), s(Y)) -> s(quot(minus(X, Y), s(Y))) 478.30/297.18 , quot(0(), s(Y)) -> 0() } 478.30/297.18 Weak Trs: 478.30/297.18 { sel(s(N), cons(X, XS)) -> sel(N, activate(XS)) 478.30/297.18 , activate(n__from(X)) -> from(X) 478.30/297.18 , minus(X, 0()) -> 0() 478.30/297.18 , zWquot(X1, X2) -> n__zWquot(X1, X2) 478.30/297.18 , zWquot(XS, nil()) -> nil() 478.30/297.18 , zWquot(cons(X, XS), cons(Y, YS)) -> 478.30/297.18 cons(quot(X, Y), n__zWquot(activate(XS), activate(YS))) 478.30/297.18 , zWquot(nil(), XS) -> nil() } 478.30/297.18 Obligation: 478.30/297.18 innermost runtime complexity 478.30/297.18 Answer: 478.30/297.18 MAYBE 478.30/297.18 478.30/297.18 The weightgap principle applies (using the following nonconstant 478.30/297.18 growth matrix-interpretation) 478.30/297.18 478.30/297.18 The following argument positions are usable: 478.30/297.18 Uargs(cons) = {1, 2}, Uargs(s) = {1}, Uargs(sel) = {2}, 478.30/297.18 Uargs(quot) = {1}, Uargs(n__zWquot) = {1, 2} 478.30/297.18 478.30/297.18 TcT has computed the following matrix interpretation satisfying 478.30/297.18 not(EDA) and not(IDA(1)). 478.30/297.18 478.30/297.18 [from](x1) = [1 1] x1 + [5] 478.30/297.18 [0 0] [0] 478.30/297.18 478.30/297.18 [cons](x1, x2) = [1 1] x1 + [1 0] x2 + [0] 478.30/297.18 [0 0] [0 1] [5] 478.30/297.18 478.30/297.18 [n__from](x1) = [0 0] x1 + [4] 478.30/297.18 [1 1] [0] 478.30/297.18 478.30/297.18 [s](x1) = [1 0] x1 + [0] 478.30/297.18 [0 0] [0] 478.30/297.18 478.30/297.18 [sel](x1, x2) = [0 0] x1 + [1 1] x2 + [0] 478.30/297.18 [1 0] [0 0] [7] 478.30/297.18 478.30/297.18 [0] = [2] 478.30/297.18 [2] 478.30/297.18 478.30/297.18 [activate](x1) = [1 1] x1 + [1] 478.30/297.18 [0 0] [0] 478.30/297.18 478.30/297.18 [minus](x1, x2) = [4] 478.30/297.18 [4] 478.30/297.18 478.30/297.18 [quot](x1, x2) = [1 1] x1 + [0] 478.30/297.18 [0 0] [4] 478.30/297.18 478.30/297.18 [zWquot](x1, x2) = [1 1] x1 + [1 1] x2 + [3] 478.30/297.18 [0 0] [0 0] [5] 478.30/297.18 478.30/297.18 [nil] = [1] 478.30/297.18 [0] 478.30/297.18 478.30/297.18 [n__zWquot](x1, x2) = [1 1] x1 + [1 1] x2 + [3] 478.30/297.18 [0 0] [0 0] [0] 478.30/297.18 478.30/297.18 The order satisfies the following ordering constraints: 478.30/297.18 478.30/297.18 [from(X)] = [1 1] X + [5] 478.30/297.18 [0 0] [0] 478.30/297.18 ? [1 1] X + [4] 478.30/297.18 [1 0] [5] 478.30/297.18 = [cons(X, n__from(s(X)))] 478.30/297.18 478.30/297.18 [from(X)] = [1 1] X + [5] 478.30/297.18 [0 0] [0] 478.30/297.18 ? [0 0] X + [4] 478.30/297.18 [1 1] [0] 478.30/297.18 = [n__from(X)] 478.30/297.18 478.30/297.18 [sel(s(N), cons(X, XS))] = [1 1] X + [1 1] XS + [0 0] N + [5] 478.30/297.18 [0 0] [0 0] [1 0] [7] 478.30/297.18 > [1 1] XS + [0 0] N + [1] 478.30/297.18 [0 0] [1 0] [7] 478.30/297.18 = [sel(N, activate(XS))] 478.30/297.18 478.30/297.18 [sel(0(), cons(X, XS))] = [1 1] X + [1 1] XS + [5] 478.30/297.18 [0 0] [0 0] [9] 478.30/297.18 ? [1 0] X + [0] 478.30/297.18 [0 1] [0] 478.30/297.18 = [X] 478.30/297.18 478.30/297.18 [activate(X)] = [1 1] X + [1] 478.30/297.18 [0 0] [0] 478.30/297.18 ? [1 0] X + [0] 478.30/297.18 [0 1] [0] 478.30/297.18 = [X] 478.30/297.18 478.30/297.18 [activate(n__from(X))] = [1 1] X + [5] 478.30/297.18 [0 0] [0] 478.30/297.18 >= [1 1] X + [5] 478.30/297.18 [0 0] [0] 478.30/297.18 = [from(X)] 478.30/297.18 478.30/297.18 [activate(n__zWquot(X1, X2))] = [1 1] X1 + [1 1] X2 + [4] 478.30/297.18 [0 0] [0 0] [0] 478.30/297.18 ? [1 1] X1 + [1 1] X2 + [3] 478.30/297.18 [0 0] [0 0] [5] 478.30/297.18 = [zWquot(X1, X2)] 478.30/297.18 478.30/297.18 [minus(X, 0())] = [4] 478.30/297.18 [4] 478.30/297.18 > [2] 478.30/297.18 [2] 478.30/297.19 = [0()] 478.30/297.19 478.30/297.19 [minus(s(X), s(Y))] = [4] 478.30/297.19 [4] 478.30/297.19 >= [4] 478.30/297.19 [4] 478.30/297.19 = [minus(X, Y)] 478.30/297.19 478.30/297.19 [quot(s(X), s(Y))] = [1 0] X + [0] 478.30/297.19 [0 0] [4] 478.30/297.19 ? [8] 478.30/297.19 [0] 478.30/297.19 = [s(quot(minus(X, Y), s(Y)))] 478.30/297.19 478.30/297.19 [quot(0(), s(Y))] = [4] 478.30/297.19 [4] 478.30/297.19 > [2] 478.30/297.19 [2] 478.30/297.19 = [0()] 478.30/297.19 478.30/297.19 [zWquot(X1, X2)] = [1 1] X1 + [1 1] X2 + [3] 478.30/297.19 [0 0] [0 0] [5] 478.30/297.19 >= [1 1] X1 + [1 1] X2 + [3] 478.30/297.19 [0 0] [0 0] [0] 478.30/297.19 = [n__zWquot(X1, X2)] 478.30/297.19 478.30/297.19 [zWquot(XS, nil())] = [1 1] XS + [4] 478.30/297.19 [0 0] [5] 478.30/297.19 > [1] 478.30/297.19 [0] 478.30/297.19 = [nil()] 478.30/297.19 478.30/297.19 [zWquot(cons(X, XS), cons(Y, YS))] = [1 1] X + [1 1] XS + [1 1] Y + [1 1] YS + [13] 478.30/297.19 [0 0] [0 0] [0 0] [0 0] [5] 478.30/297.19 > [1 1] X + [1 1] XS + [1 1] YS + [9] 478.30/297.19 [0 0] [0 0] [0 0] [5] 478.30/297.19 = [cons(quot(X, Y), n__zWquot(activate(XS), activate(YS)))] 478.30/297.19 478.30/297.19 [zWquot(nil(), XS)] = [1 1] XS + [4] 478.30/297.19 [0 0] [5] 478.30/297.19 > [1] 478.30/297.19 [0] 478.30/297.19 = [nil()] 478.30/297.19 478.30/297.19 478.30/297.19 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 478.30/297.19 478.30/297.19 We are left with following problem, upon which TcT provides the 478.30/297.19 certificate MAYBE. 478.30/297.19 478.30/297.19 Strict Trs: 478.30/297.19 { from(X) -> cons(X, n__from(s(X))) 478.30/297.19 , from(X) -> n__from(X) 478.30/297.19 , sel(0(), cons(X, XS)) -> X 478.30/297.19 , activate(X) -> X 478.30/297.19 , activate(n__zWquot(X1, X2)) -> zWquot(X1, X2) 478.30/297.19 , minus(s(X), s(Y)) -> minus(X, Y) 478.30/297.19 , quot(s(X), s(Y)) -> s(quot(minus(X, Y), s(Y))) } 478.30/297.19 Weak Trs: 478.30/297.19 { sel(s(N), cons(X, XS)) -> sel(N, activate(XS)) 478.30/297.19 , activate(n__from(X)) -> from(X) 478.30/297.19 , minus(X, 0()) -> 0() 478.30/297.19 , quot(0(), s(Y)) -> 0() 478.30/297.19 , zWquot(X1, X2) -> n__zWquot(X1, X2) 478.30/297.19 , zWquot(XS, nil()) -> nil() 478.30/297.19 , zWquot(cons(X, XS), cons(Y, YS)) -> 478.30/297.19 cons(quot(X, Y), n__zWquot(activate(XS), activate(YS))) 478.30/297.19 , zWquot(nil(), XS) -> nil() } 478.30/297.19 Obligation: 478.30/297.19 innermost runtime complexity 478.30/297.19 Answer: 478.30/297.19 MAYBE 478.30/297.19 478.30/297.19 The weightgap principle applies (using the following nonconstant 478.30/297.19 growth matrix-interpretation) 478.30/297.19 478.30/297.19 The following argument positions are usable: 478.30/297.19 Uargs(cons) = {1, 2}, Uargs(s) = {1}, Uargs(sel) = {2}, 478.30/297.19 Uargs(quot) = {1}, Uargs(n__zWquot) = {1, 2} 478.30/297.19 478.30/297.19 TcT has computed the following matrix interpretation satisfying 478.30/297.19 not(EDA) and not(IDA(1)). 478.30/297.19 478.30/297.19 [from](x1) = [1 1] x1 + [1] 478.30/297.19 [0 0] [0] 478.30/297.19 478.30/297.19 [cons](x1, x2) = [1 1] x1 + [1 0] x2 + [4] 478.30/297.19 [0 0] [0 1] [0] 478.30/297.19 478.30/297.19 [n__from](x1) = [0 0] x1 + [0] 478.30/297.19 [1 1] [0] 478.30/297.19 478.30/297.19 [s](x1) = [1 0] x1 + [0] 478.30/297.19 [0 0] [0] 478.30/297.19 478.30/297.19 [sel](x1, x2) = [0 0] x1 + [1 1] x2 + [0] 478.30/297.19 [1 0] [0 0] [7] 478.30/297.19 478.30/297.19 [0] = [0] 478.30/297.19 [0] 478.30/297.19 478.30/297.19 [activate](x1) = [1 1] x1 + [1] 478.30/297.19 [0 0] [0] 478.30/297.19 478.30/297.19 [minus](x1, x2) = [0] 478.30/297.19 [4] 478.30/297.19 478.30/297.19 [quot](x1, x2) = [1 0] x1 + [1] 478.30/297.19 [0 0] [1] 478.30/297.19 478.30/297.19 [zWquot](x1, x2) = [1 1] x1 + [1 1] x2 + [0] 478.30/297.19 [0 0] [0 0] [0] 478.30/297.19 478.30/297.19 [nil] = [0] 478.30/297.19 [0] 478.30/297.19 478.30/297.19 [n__zWquot](x1, x2) = [1 1] x1 + [1 1] x2 + [0] 478.30/297.19 [0 0] [0 0] [0] 478.30/297.19 478.30/297.19 The order satisfies the following ordering constraints: 478.30/297.19 478.30/297.19 [from(X)] = [1 1] X + [1] 478.30/297.19 [0 0] [0] 478.30/297.19 ? [1 1] X + [4] 478.30/297.19 [1 0] [0] 478.30/297.19 = [cons(X, n__from(s(X)))] 478.30/297.19 478.30/297.19 [from(X)] = [1 1] X + [1] 478.30/297.19 [0 0] [0] 478.30/297.19 ? [0 0] X + [0] 478.30/297.19 [1 1] [0] 478.30/297.19 = [n__from(X)] 478.30/297.19 478.30/297.19 [sel(s(N), cons(X, XS))] = [1 1] X + [1 1] XS + [0 0] N + [4] 478.30/297.19 [0 0] [0 0] [1 0] [7] 478.30/297.19 > [1 1] XS + [0 0] N + [1] 478.30/297.19 [0 0] [1 0] [7] 478.30/297.19 = [sel(N, activate(XS))] 478.30/297.19 478.30/297.19 [sel(0(), cons(X, XS))] = [1 1] X + [1 1] XS + [4] 478.30/297.19 [0 0] [0 0] [7] 478.30/297.19 ? [1 0] X + [0] 478.30/297.19 [0 1] [0] 478.30/297.19 = [X] 478.30/297.19 478.30/297.19 [activate(X)] = [1 1] X + [1] 478.30/297.19 [0 0] [0] 478.30/297.19 ? [1 0] X + [0] 478.30/297.19 [0 1] [0] 478.30/297.19 = [X] 478.30/297.19 478.30/297.19 [activate(n__from(X))] = [1 1] X + [1] 478.30/297.19 [0 0] [0] 478.30/297.19 >= [1 1] X + [1] 478.30/297.19 [0 0] [0] 478.30/297.19 = [from(X)] 478.30/297.19 478.30/297.19 [activate(n__zWquot(X1, X2))] = [1 1] X1 + [1 1] X2 + [1] 478.30/297.19 [0 0] [0 0] [0] 478.30/297.19 > [1 1] X1 + [1 1] X2 + [0] 478.30/297.19 [0 0] [0 0] [0] 478.30/297.19 = [zWquot(X1, X2)] 478.30/297.19 478.30/297.19 [minus(X, 0())] = [0] 478.30/297.19 [4] 478.30/297.19 >= [0] 478.30/297.19 [0] 478.30/297.19 = [0()] 478.30/297.19 478.30/297.19 [minus(s(X), s(Y))] = [0] 478.30/297.19 [4] 478.30/297.19 >= [0] 478.30/297.19 [4] 478.30/297.19 = [minus(X, Y)] 478.30/297.19 478.30/297.19 [quot(s(X), s(Y))] = [1 0] X + [1] 478.30/297.19 [0 0] [1] 478.30/297.19 >= [1] 478.30/297.19 [0] 478.30/297.19 = [s(quot(minus(X, Y), s(Y)))] 478.30/297.19 478.30/297.19 [quot(0(), s(Y))] = [1] 478.30/297.19 [1] 478.30/297.19 > [0] 478.30/297.19 [0] 478.30/297.19 = [0()] 478.30/297.19 478.30/297.19 [zWquot(X1, X2)] = [1 1] X1 + [1 1] X2 + [0] 478.30/297.19 [0 0] [0 0] [0] 478.30/297.19 >= [1 1] X1 + [1 1] X2 + [0] 478.30/297.19 [0 0] [0 0] [0] 478.30/297.19 = [n__zWquot(X1, X2)] 478.30/297.19 478.30/297.19 [zWquot(XS, nil())] = [1 1] XS + [0] 478.30/297.19 [0 0] [0] 478.30/297.19 >= [0] 478.30/297.19 [0] 478.30/297.19 = [nil()] 478.30/297.19 478.30/297.19 [zWquot(cons(X, XS), cons(Y, YS))] = [1 1] X + [1 1] XS + [1 1] Y + [1 1] YS + [8] 478.30/297.19 [0 0] [0 0] [0 0] [0 0] [0] 478.30/297.19 >= [1 0] X + [1 1] XS + [1 1] YS + [8] 478.30/297.19 [0 0] [0 0] [0 0] [0] 478.30/297.19 = [cons(quot(X, Y), n__zWquot(activate(XS), activate(YS)))] 478.30/297.19 478.30/297.19 [zWquot(nil(), XS)] = [1 1] XS + [0] 478.30/297.19 [0 0] [0] 478.30/297.19 >= [0] 478.30/297.19 [0] 478.30/297.19 = [nil()] 478.30/297.19 478.30/297.19 478.30/297.19 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 478.30/297.19 478.30/297.19 We are left with following problem, upon which TcT provides the 478.30/297.19 certificate MAYBE. 478.30/297.19 478.30/297.19 Strict Trs: 478.30/297.19 { from(X) -> cons(X, n__from(s(X))) 478.30/297.19 , from(X) -> n__from(X) 478.30/297.19 , sel(0(), cons(X, XS)) -> X 478.30/297.19 , activate(X) -> X 478.30/297.19 , minus(s(X), s(Y)) -> minus(X, Y) 478.30/297.19 , quot(s(X), s(Y)) -> s(quot(minus(X, Y), s(Y))) } 478.30/297.19 Weak Trs: 478.30/297.19 { sel(s(N), cons(X, XS)) -> sel(N, activate(XS)) 478.30/297.19 , activate(n__from(X)) -> from(X) 478.30/297.19 , activate(n__zWquot(X1, X2)) -> zWquot(X1, X2) 478.30/297.19 , minus(X, 0()) -> 0() 478.30/297.19 , quot(0(), s(Y)) -> 0() 478.30/297.19 , zWquot(X1, X2) -> n__zWquot(X1, X2) 478.30/297.19 , zWquot(XS, nil()) -> nil() 478.30/297.19 , zWquot(cons(X, XS), cons(Y, YS)) -> 478.30/297.19 cons(quot(X, Y), n__zWquot(activate(XS), activate(YS))) 478.30/297.19 , zWquot(nil(), XS) -> nil() } 478.30/297.19 Obligation: 478.30/297.19 innermost runtime complexity 478.30/297.19 Answer: 478.30/297.19 MAYBE 478.30/297.19 478.30/297.19 The weightgap principle applies (using the following nonconstant 478.30/297.19 growth matrix-interpretation) 478.30/297.19 478.30/297.19 The following argument positions are usable: 478.30/297.19 Uargs(cons) = {1, 2}, Uargs(s) = {1}, Uargs(sel) = {2}, 478.30/297.19 Uargs(quot) = {1}, Uargs(n__zWquot) = {1, 2} 478.30/297.19 478.30/297.19 TcT has computed the following matrix interpretation satisfying 478.30/297.19 not(EDA) and not(IDA(1)). 478.30/297.19 478.30/297.19 [from](x1) = [1 1] x1 + [4] 478.30/297.19 [0 0] [0] 478.30/297.19 478.30/297.19 [cons](x1, x2) = [1 1] x1 + [1 0] x2 + [4] 478.30/297.19 [0 0] [0 1] [0] 478.30/297.19 478.30/297.19 [n__from](x1) = [0 0] x1 + [4] 478.30/297.19 [1 1] [4] 478.30/297.19 478.30/297.19 [s](x1) = [1 0] x1 + [0] 478.30/297.19 [0 1] [4] 478.30/297.19 478.30/297.19 [sel](x1, x2) = [0 1] x1 + [1 1] x2 + [0] 478.30/297.19 [1 0] [0 0] [7] 478.30/297.19 478.30/297.19 [0] = [0] 478.30/297.19 [0] 478.30/297.19 478.30/297.19 [activate](x1) = [1 1] x1 + [0] 478.30/297.19 [0 0] [0] 478.30/297.19 478.30/297.19 [minus](x1, x2) = [0 1] x1 + [0] 478.30/297.19 [0 0] [0] 478.30/297.19 478.30/297.19 [quot](x1, x2) = [1 1] x1 + [0 0] x2 + [4] 478.30/297.19 [0 0] [0 1] [0] 478.30/297.19 478.30/297.19 [zWquot](x1, x2) = [1 1] x1 + [1 1] x2 + [4] 478.30/297.19 [0 0] [0 0] [0] 478.30/297.19 478.30/297.19 [nil] = [0] 478.30/297.19 [0] 478.30/297.19 478.30/297.19 [n__zWquot](x1, x2) = [1 1] x1 + [1 1] x2 + [4] 478.30/297.19 [0 0] [0 0] [0] 478.30/297.19 478.30/297.19 The order satisfies the following ordering constraints: 478.30/297.19 478.30/297.19 [from(X)] = [1 1] X + [4] 478.30/297.19 [0 0] [0] 478.30/297.19 ? [1 1] X + [8] 478.30/297.19 [1 1] [8] 478.30/297.19 = [cons(X, n__from(s(X)))] 478.30/297.19 478.30/297.19 [from(X)] = [1 1] X + [4] 478.30/297.19 [0 0] [0] 478.30/297.19 ? [0 0] X + [4] 478.30/297.19 [1 1] [4] 478.30/297.19 = [n__from(X)] 478.30/297.19 478.30/297.19 [sel(s(N), cons(X, XS))] = [1 1] X + [1 1] XS + [0 1] N + [8] 478.30/297.19 [0 0] [0 0] [1 0] [7] 478.30/297.19 > [1 1] XS + [0 1] N + [0] 478.30/297.19 [0 0] [1 0] [7] 478.30/297.19 = [sel(N, activate(XS))] 478.30/297.19 478.30/297.19 [sel(0(), cons(X, XS))] = [1 1] X + [1 1] XS + [4] 478.30/297.19 [0 0] [0 0] [7] 478.30/297.19 ? [1 0] X + [0] 478.30/297.19 [0 1] [0] 478.30/297.19 = [X] 478.30/297.19 478.30/297.19 [activate(X)] = [1 1] X + [0] 478.30/297.19 [0 0] [0] 478.30/297.19 ? [1 0] X + [0] 478.30/297.19 [0 1] [0] 478.30/297.19 = [X] 478.30/297.19 478.30/297.19 [activate(n__from(X))] = [1 1] X + [8] 478.30/297.19 [0 0] [0] 478.30/297.19 > [1 1] X + [4] 478.30/297.19 [0 0] [0] 478.30/297.19 = [from(X)] 478.30/297.19 478.30/297.19 [activate(n__zWquot(X1, X2))] = [1 1] X1 + [1 1] X2 + [4] 478.30/297.19 [0 0] [0 0] [0] 478.30/297.19 >= [1 1] X1 + [1 1] X2 + [4] 478.30/297.19 [0 0] [0 0] [0] 478.30/297.19 = [zWquot(X1, X2)] 478.30/297.19 478.30/297.19 [minus(X, 0())] = [0 1] X + [0] 478.30/297.19 [0 0] [0] 478.30/297.19 >= [0] 478.30/297.19 [0] 478.30/297.19 = [0()] 478.30/297.19 478.30/297.19 [minus(s(X), s(Y))] = [0 1] X + [4] 478.30/297.19 [0 0] [0] 478.30/297.19 > [0 1] X + [0] 478.30/297.19 [0 0] [0] 478.30/297.19 = [minus(X, Y)] 478.30/297.19 478.30/297.19 [quot(s(X), s(Y))] = [1 1] X + [0 0] Y + [8] 478.30/297.19 [0 0] [0 1] [4] 478.30/297.19 ? [0 1] X + [0 0] Y + [4] 478.30/297.19 [0 0] [0 1] [8] 478.30/297.19 = [s(quot(minus(X, Y), s(Y)))] 478.30/297.19 478.30/297.19 [quot(0(), s(Y))] = [0 0] Y + [4] 478.30/297.19 [0 1] [4] 478.30/297.19 > [0] 478.30/297.19 [0] 478.30/297.19 = [0()] 478.30/297.19 478.30/297.19 [zWquot(X1, X2)] = [1 1] X1 + [1 1] X2 + [4] 478.30/297.19 [0 0] [0 0] [0] 478.30/297.19 >= [1 1] X1 + [1 1] X2 + [4] 478.30/297.19 [0 0] [0 0] [0] 478.30/297.19 = [n__zWquot(X1, X2)] 478.30/297.19 478.30/297.19 [zWquot(XS, nil())] = [1 1] XS + [4] 478.30/297.19 [0 0] [0] 478.30/297.19 > [0] 478.30/297.19 [0] 478.30/297.19 = [nil()] 478.30/297.19 478.30/297.19 [zWquot(cons(X, XS), cons(Y, YS))] = [1 1] X + [1 1] XS + [1 1] Y + [1 1] YS + [12] 478.30/297.19 [0 0] [0 0] [0 0] [0 0] [0] 478.30/297.19 >= [1 1] X + [1 1] XS + [0 1] Y + [1 1] YS + [12] 478.30/297.19 [0 0] [0 0] [0 0] [0 0] [0] 478.30/297.19 = [cons(quot(X, Y), n__zWquot(activate(XS), activate(YS)))] 478.30/297.19 478.30/297.19 [zWquot(nil(), XS)] = [1 1] XS + [4] 478.30/297.19 [0 0] [0] 478.30/297.19 > [0] 478.30/297.19 [0] 478.30/297.19 = [nil()] 478.30/297.19 478.30/297.19 478.30/297.19 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 478.30/297.19 478.30/297.19 We are left with following problem, upon which TcT provides the 478.30/297.19 certificate MAYBE. 478.30/297.19 478.30/297.19 Strict Trs: 478.30/297.19 { from(X) -> cons(X, n__from(s(X))) 478.30/297.19 , from(X) -> n__from(X) 478.30/297.19 , sel(0(), cons(X, XS)) -> X 478.30/297.19 , activate(X) -> X 478.30/297.19 , quot(s(X), s(Y)) -> s(quot(minus(X, Y), s(Y))) } 478.30/297.19 Weak Trs: 478.30/297.19 { sel(s(N), cons(X, XS)) -> sel(N, activate(XS)) 478.30/297.19 , activate(n__from(X)) -> from(X) 478.30/297.19 , activate(n__zWquot(X1, X2)) -> zWquot(X1, X2) 478.30/297.19 , minus(X, 0()) -> 0() 478.30/297.19 , minus(s(X), s(Y)) -> minus(X, Y) 478.30/297.19 , quot(0(), s(Y)) -> 0() 478.30/297.19 , zWquot(X1, X2) -> n__zWquot(X1, X2) 478.30/297.19 , zWquot(XS, nil()) -> nil() 478.30/297.19 , zWquot(cons(X, XS), cons(Y, YS)) -> 478.30/297.19 cons(quot(X, Y), n__zWquot(activate(XS), activate(YS))) 478.30/297.19 , zWquot(nil(), XS) -> nil() } 478.30/297.19 Obligation: 478.30/297.19 innermost runtime complexity 478.30/297.19 Answer: 478.30/297.19 MAYBE 478.30/297.19 478.30/297.19 The weightgap principle applies (using the following nonconstant 478.30/297.19 growth matrix-interpretation) 478.30/297.19 478.30/297.19 The following argument positions are usable: 478.30/297.19 Uargs(cons) = {1, 2}, Uargs(s) = {1}, Uargs(sel) = {2}, 478.30/297.19 Uargs(quot) = {1}, Uargs(n__zWquot) = {1, 2} 478.30/297.19 478.30/297.19 TcT has computed the following matrix interpretation satisfying 478.30/297.19 not(EDA) and not(IDA(1)). 478.30/297.19 478.30/297.19 [from](x1) = [1 1] x1 + [4] 478.30/297.19 [0 0] [0] 478.30/297.19 478.30/297.19 [cons](x1, x2) = [1 1] x1 + [1 0] x2 + [4] 478.30/297.19 [0 0] [0 1] [0] 478.30/297.19 478.30/297.19 [n__from](x1) = [0 1] x1 + [4] 478.30/297.19 [1 0] [0] 478.30/297.19 478.30/297.19 [s](x1) = [1 0] x1 + [1] 478.30/297.19 [0 0] [7] 478.30/297.19 478.30/297.19 [sel](x1, x2) = [0 0] x1 + [1 1] x2 + [0] 478.30/297.19 [1 0] [0 0] [7] 478.30/297.19 478.30/297.19 [0] = [0] 478.30/297.19 [0] 478.30/297.19 478.30/297.19 [activate](x1) = [1 1] x1 + [0] 478.30/297.19 [0 0] [0] 478.30/297.19 478.30/297.19 [minus](x1, x2) = [0] 478.30/297.19 [0] 478.30/297.19 478.30/297.19 [quot](x1, x2) = [1 1] x1 + [1 0] x2 + [0] 478.30/297.19 [0 0] [0 1] [0] 478.30/297.19 478.30/297.19 [zWquot](x1, x2) = [1 1] x1 + [1 1] x2 + [0] 478.30/297.19 [0 0] [0 0] [0] 478.30/297.19 478.30/297.19 [nil] = [0] 478.30/297.19 [0] 478.30/297.19 478.30/297.19 [n__zWquot](x1, x2) = [1 1] x1 + [1 1] x2 + [0] 478.30/297.19 [0 0] [0 0] [0] 478.30/297.19 478.30/297.19 The order satisfies the following ordering constraints: 478.30/297.19 478.30/297.19 [from(X)] = [1 1] X + [4] 478.30/297.19 [0 0] [0] 478.30/297.19 ? [1 1] X + [15] 478.30/297.19 [1 0] [1] 478.30/297.19 = [cons(X, n__from(s(X)))] 478.30/297.19 478.30/297.19 [from(X)] = [1 1] X + [4] 478.30/297.19 [0 0] [0] 478.30/297.19 ? [0 1] X + [4] 478.30/297.19 [1 0] [0] 478.30/297.19 = [n__from(X)] 478.30/297.19 478.30/297.19 [sel(s(N), cons(X, XS))] = [1 1] X + [1 1] XS + [0 0] N + [4] 478.30/297.19 [0 0] [0 0] [1 0] [8] 478.30/297.19 > [1 1] XS + [0 0] N + [0] 478.30/297.19 [0 0] [1 0] [7] 478.30/297.19 = [sel(N, activate(XS))] 478.30/297.19 478.30/297.19 [sel(0(), cons(X, XS))] = [1 1] X + [1 1] XS + [4] 478.30/297.19 [0 0] [0 0] [7] 478.30/297.19 ? [1 0] X + [0] 478.30/297.19 [0 1] [0] 478.30/297.19 = [X] 478.30/297.19 478.30/297.19 [activate(X)] = [1 1] X + [0] 478.30/297.19 [0 0] [0] 478.30/297.19 ? [1 0] X + [0] 478.30/297.19 [0 1] [0] 478.30/297.19 = [X] 478.30/297.19 478.30/297.19 [activate(n__from(X))] = [1 1] X + [4] 478.30/297.19 [0 0] [0] 478.30/297.19 >= [1 1] X + [4] 478.30/297.19 [0 0] [0] 478.30/297.19 = [from(X)] 478.30/297.19 478.30/297.19 [activate(n__zWquot(X1, X2))] = [1 1] X1 + [1 1] X2 + [0] 478.30/297.19 [0 0] [0 0] [0] 478.30/297.19 >= [1 1] X1 + [1 1] X2 + [0] 478.30/297.19 [0 0] [0 0] [0] 478.30/297.19 = [zWquot(X1, X2)] 478.30/297.19 478.30/297.19 [minus(X, 0())] = [0] 478.30/297.19 [0] 478.30/297.19 >= [0] 478.30/297.19 [0] 478.30/297.19 = [0()] 478.30/297.19 478.30/297.19 [minus(s(X), s(Y))] = [0] 478.30/297.19 [0] 478.30/297.19 >= [0] 478.30/297.19 [0] 478.30/297.19 = [minus(X, Y)] 478.30/297.19 478.30/297.19 [quot(s(X), s(Y))] = [1 0] X + [1 0] Y + [9] 478.30/297.19 [0 0] [0 0] [7] 478.30/297.19 > [1 0] Y + [2] 478.30/297.19 [0 0] [7] 478.30/297.19 = [s(quot(minus(X, Y), s(Y)))] 478.30/297.19 478.30/297.19 [quot(0(), s(Y))] = [1 0] Y + [1] 478.30/297.19 [0 0] [7] 478.30/297.19 > [0] 478.30/297.19 [0] 478.30/297.19 = [0()] 478.30/297.19 478.30/297.19 [zWquot(X1, X2)] = [1 1] X1 + [1 1] X2 + [0] 478.30/297.19 [0 0] [0 0] [0] 478.30/297.19 >= [1 1] X1 + [1 1] X2 + [0] 478.30/297.19 [0 0] [0 0] [0] 478.30/297.19 = [n__zWquot(X1, X2)] 478.30/297.19 478.30/297.19 [zWquot(XS, nil())] = [1 1] XS + [0] 478.30/297.19 [0 0] [0] 478.30/297.19 >= [0] 478.30/297.19 [0] 478.30/297.19 = [nil()] 478.30/297.19 478.30/297.19 [zWquot(cons(X, XS), cons(Y, YS))] = [1 1] X + [1 1] XS + [1 1] Y + [1 1] YS + [8] 478.30/297.19 [0 0] [0 0] [0 0] [0 0] [0] 478.30/297.19 > [1 1] X + [1 1] XS + [1 1] Y + [1 1] YS + [4] 478.30/297.19 [0 0] [0 0] [0 0] [0 0] [0] 478.30/297.19 = [cons(quot(X, Y), n__zWquot(activate(XS), activate(YS)))] 478.30/297.19 478.30/297.19 [zWquot(nil(), XS)] = [1 1] XS + [0] 478.30/297.19 [0 0] [0] 478.30/297.19 >= [0] 478.30/297.19 [0] 478.30/297.19 = [nil()] 478.30/297.19 478.30/297.19 478.30/297.19 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 478.30/297.19 478.30/297.19 We are left with following problem, upon which TcT provides the 478.30/297.19 certificate MAYBE. 478.30/297.19 478.30/297.19 Strict Trs: 478.30/297.19 { from(X) -> cons(X, n__from(s(X))) 478.30/297.19 , from(X) -> n__from(X) 478.30/297.19 , sel(0(), cons(X, XS)) -> X 478.30/297.19 , activate(X) -> X } 478.30/297.19 Weak Trs: 478.30/297.19 { sel(s(N), cons(X, XS)) -> sel(N, activate(XS)) 478.30/297.19 , activate(n__from(X)) -> from(X) 478.30/297.19 , activate(n__zWquot(X1, X2)) -> zWquot(X1, X2) 478.30/297.19 , minus(X, 0()) -> 0() 478.30/297.19 , minus(s(X), s(Y)) -> minus(X, Y) 478.30/297.19 , quot(s(X), s(Y)) -> s(quot(minus(X, Y), s(Y))) 478.30/297.19 , quot(0(), s(Y)) -> 0() 478.30/297.19 , zWquot(X1, X2) -> n__zWquot(X1, X2) 478.30/297.19 , zWquot(XS, nil()) -> nil() 478.30/297.19 , zWquot(cons(X, XS), cons(Y, YS)) -> 478.30/297.19 cons(quot(X, Y), n__zWquot(activate(XS), activate(YS))) 478.30/297.19 , zWquot(nil(), XS) -> nil() } 478.30/297.19 Obligation: 478.30/297.19 innermost runtime complexity 478.30/297.19 Answer: 478.30/297.19 MAYBE 478.30/297.19 478.30/297.19 None of the processors succeeded. 478.30/297.19 478.30/297.19 Details of failed attempt(s): 478.30/297.19 ----------------------------- 478.30/297.19 1) 'empty' failed due to the following reason: 478.30/297.19 478.30/297.19 Empty strict component of the problem is NOT empty. 478.30/297.19 478.30/297.19 2) 'With Problem ...' failed due to the following reason: 478.30/297.19 478.30/297.19 None of the processors succeeded. 478.30/297.19 478.30/297.19 Details of failed attempt(s): 478.30/297.19 ----------------------------- 478.30/297.19 1) 'empty' failed due to the following reason: 478.30/297.19 478.30/297.19 Empty strict component of the problem is NOT empty. 478.30/297.19 478.30/297.19 2) 'With Problem ...' failed due to the following reason: 478.30/297.19 478.30/297.19 Empty strict component of the problem is NOT empty. 478.30/297.19 478.30/297.19 478.30/297.19 478.30/297.19 478.30/297.19 2) 'With Problem ...' failed due to the following reason: 478.30/297.19 478.30/297.19 None of the processors succeeded. 478.30/297.19 478.30/297.19 Details of failed attempt(s): 478.30/297.19 ----------------------------- 478.30/297.19 1) 'empty' failed due to the following reason: 478.30/297.19 478.30/297.19 Empty strict component of the problem is NOT empty. 478.30/297.19 478.30/297.19 2) 'With Problem ...' failed due to the following reason: 478.30/297.19 478.30/297.19 Empty strict component of the problem is NOT empty. 478.30/297.19 478.30/297.19 478.30/297.19 478.30/297.19 478.30/297.19 478.30/297.19 2) 'Best' failed due to the following reason: 478.30/297.19 478.30/297.19 None of the processors succeeded. 478.30/297.19 478.30/297.19 Details of failed attempt(s): 478.30/297.19 ----------------------------- 478.30/297.19 1) 'Polynomial Path Order (PS) (timeout of 297 seconds)' failed due 478.30/297.19 to the following reason: 478.30/297.19 478.30/297.19 The input cannot be shown compatible 478.30/297.19 478.30/297.19 2) 'bsearch-popstar (timeout of 297 seconds)' failed due to the 478.30/297.19 following reason: 478.30/297.19 478.30/297.19 The input cannot be shown compatible 478.30/297.19 478.30/297.19 478.30/297.19 3) 'Fastest (timeout of 24 seconds) (timeout of 297 seconds)' 478.30/297.19 failed due to the following reason: 478.30/297.19 478.30/297.19 None of the processors succeeded. 478.30/297.19 478.30/297.19 Details of failed attempt(s): 478.30/297.19 ----------------------------- 478.30/297.19 1) 'Bounds with minimal-enrichment and initial automaton 'match'' 478.30/297.19 failed due to the following reason: 478.30/297.19 478.30/297.19 match-boundness of the problem could not be verified. 478.30/297.19 478.30/297.19 2) 'Bounds with perSymbol-enrichment and initial automaton 'match'' 478.30/297.19 failed due to the following reason: 478.30/297.19 478.30/297.19 match-boundness of the problem could not be verified. 478.30/297.19 478.30/297.19 478.30/297.19 478.30/297.19 478.30/297.19 478.30/297.19 Arrrr.. 478.64/297.23 EOF