MAYBE 1179.22/297.05 MAYBE 1179.22/297.05 1179.22/297.05 We are left with following problem, upon which TcT provides the 1179.22/297.05 certificate MAYBE. 1179.22/297.05 1179.22/297.05 Strict Trs: 1179.22/297.05 { U11(tt(), V1, V2) -> U12(isNat(activate(V1)), activate(V2)) 1179.22/297.05 , U12(tt(), V2) -> U13(isNat(activate(V2))) 1179.22/297.05 , isNat(n__0()) -> tt() 1179.22/297.05 , isNat(n__plus(V1, V2)) -> 1179.22/297.05 U11(and(isNatKind(activate(V1)), n__isNatKind(activate(V2))), 1179.22/297.05 activate(V1), 1179.22/297.05 activate(V2)) 1179.22/297.05 , isNat(n__s(V1)) -> U21(isNatKind(activate(V1)), activate(V1)) 1179.22/297.05 , isNat(n__x(V1, V2)) -> 1179.22/297.05 U31(and(isNatKind(activate(V1)), n__isNatKind(activate(V2))), 1179.22/297.05 activate(V1), 1179.22/297.05 activate(V2)) 1179.22/297.05 , activate(X) -> X 1179.22/297.05 , activate(n__0()) -> 0() 1179.22/297.05 , activate(n__plus(X1, X2)) -> plus(X1, X2) 1179.22/297.05 , activate(n__isNatKind(X)) -> isNatKind(X) 1179.22/297.05 , activate(n__s(X)) -> s(X) 1179.22/297.05 , activate(n__x(X1, X2)) -> x(X1, X2) 1179.22/297.05 , activate(n__and(X1, X2)) -> and(X1, X2) 1179.22/297.05 , U13(tt()) -> tt() 1179.22/297.05 , U21(tt(), V1) -> U22(isNat(activate(V1))) 1179.22/297.05 , U22(tt()) -> tt() 1179.22/297.05 , U31(tt(), V1, V2) -> U32(isNat(activate(V1)), activate(V2)) 1179.22/297.05 , U32(tt(), V2) -> U33(isNat(activate(V2))) 1179.22/297.05 , U33(tt()) -> tt() 1179.22/297.05 , U41(tt(), N) -> activate(N) 1179.22/297.05 , U51(tt(), M, N) -> s(plus(activate(N), activate(M))) 1179.22/297.05 , s(X) -> n__s(X) 1179.22/297.05 , plus(X1, X2) -> n__plus(X1, X2) 1179.22/297.05 , plus(N, s(M)) -> 1179.22/297.05 U51(and(and(isNat(M), n__isNatKind(M)), 1179.22/297.05 n__and(isNat(N), n__isNatKind(N))), 1179.22/297.05 M, 1179.22/297.05 N) 1179.22/297.05 , plus(N, 0()) -> U41(and(isNat(N), n__isNatKind(N)), N) 1179.22/297.05 , U61(tt()) -> 0() 1179.22/297.05 , 0() -> n__0() 1179.22/297.05 , U71(tt(), M, N) -> plus(x(activate(N), activate(M)), activate(N)) 1179.22/297.05 , x(X1, X2) -> n__x(X1, X2) 1179.22/297.05 , x(N, s(M)) -> 1179.22/297.05 U71(and(and(isNat(M), n__isNatKind(M)), 1179.22/297.05 n__and(isNat(N), n__isNatKind(N))), 1179.22/297.05 M, 1179.22/297.05 N) 1179.22/297.05 , x(N, 0()) -> U61(and(isNat(N), n__isNatKind(N))) 1179.22/297.05 , and(X1, X2) -> n__and(X1, X2) 1179.22/297.05 , and(tt(), X) -> activate(X) 1179.22/297.05 , isNatKind(X) -> n__isNatKind(X) 1179.22/297.05 , isNatKind(n__0()) -> tt() 1179.22/297.05 , isNatKind(n__plus(V1, V2)) -> 1179.22/297.05 and(isNatKind(activate(V1)), n__isNatKind(activate(V2))) 1179.22/297.05 , isNatKind(n__s(V1)) -> isNatKind(activate(V1)) 1179.22/297.05 , isNatKind(n__x(V1, V2)) -> 1179.22/297.05 and(isNatKind(activate(V1)), n__isNatKind(activate(V2))) } 1179.22/297.05 Obligation: 1179.22/297.05 innermost runtime complexity 1179.22/297.05 Answer: 1179.22/297.05 MAYBE 1179.22/297.05 1179.22/297.05 Arguments of following rules are not normal-forms: 1179.22/297.05 1179.22/297.05 { plus(N, s(M)) -> 1179.22/297.05 U51(and(and(isNat(M), n__isNatKind(M)), 1179.22/297.05 n__and(isNat(N), n__isNatKind(N))), 1179.22/297.05 M, 1179.22/297.05 N) 1179.22/297.05 , plus(N, 0()) -> U41(and(isNat(N), n__isNatKind(N)), N) 1179.22/297.05 , x(N, s(M)) -> 1179.22/297.05 U71(and(and(isNat(M), n__isNatKind(M)), 1179.22/297.05 n__and(isNat(N), n__isNatKind(N))), 1179.22/297.05 M, 1179.22/297.05 N) 1179.22/297.05 , x(N, 0()) -> U61(and(isNat(N), n__isNatKind(N))) } 1179.22/297.05 1179.22/297.05 All above mentioned rules can be savely removed. 1179.22/297.05 1179.22/297.05 We are left with following problem, upon which TcT provides the 1179.22/297.05 certificate MAYBE. 1179.22/297.05 1179.22/297.05 Strict Trs: 1179.22/297.05 { U11(tt(), V1, V2) -> U12(isNat(activate(V1)), activate(V2)) 1179.22/297.05 , U12(tt(), V2) -> U13(isNat(activate(V2))) 1179.22/297.05 , isNat(n__0()) -> tt() 1179.22/297.05 , isNat(n__plus(V1, V2)) -> 1179.22/297.05 U11(and(isNatKind(activate(V1)), n__isNatKind(activate(V2))), 1179.22/297.05 activate(V1), 1179.22/297.05 activate(V2)) 1179.22/297.05 , isNat(n__s(V1)) -> U21(isNatKind(activate(V1)), activate(V1)) 1179.22/297.05 , isNat(n__x(V1, V2)) -> 1179.22/297.05 U31(and(isNatKind(activate(V1)), n__isNatKind(activate(V2))), 1179.22/297.05 activate(V1), 1179.22/297.05 activate(V2)) 1179.22/297.05 , activate(X) -> X 1179.22/297.05 , activate(n__0()) -> 0() 1179.22/297.05 , activate(n__plus(X1, X2)) -> plus(X1, X2) 1179.22/297.05 , activate(n__isNatKind(X)) -> isNatKind(X) 1179.22/297.05 , activate(n__s(X)) -> s(X) 1179.22/297.05 , activate(n__x(X1, X2)) -> x(X1, X2) 1179.22/297.05 , activate(n__and(X1, X2)) -> and(X1, X2) 1179.22/297.05 , U13(tt()) -> tt() 1179.22/297.05 , U21(tt(), V1) -> U22(isNat(activate(V1))) 1179.22/297.05 , U22(tt()) -> tt() 1179.22/297.05 , U31(tt(), V1, V2) -> U32(isNat(activate(V1)), activate(V2)) 1179.22/297.05 , U32(tt(), V2) -> U33(isNat(activate(V2))) 1179.22/297.05 , U33(tt()) -> tt() 1179.22/297.05 , U41(tt(), N) -> activate(N) 1179.22/297.05 , U51(tt(), M, N) -> s(plus(activate(N), activate(M))) 1179.22/297.05 , s(X) -> n__s(X) 1179.22/297.05 , plus(X1, X2) -> n__plus(X1, X2) 1179.22/297.05 , U61(tt()) -> 0() 1179.22/297.05 , 0() -> n__0() 1179.22/297.05 , U71(tt(), M, N) -> plus(x(activate(N), activate(M)), activate(N)) 1179.22/297.05 , x(X1, X2) -> n__x(X1, X2) 1179.22/297.05 , and(X1, X2) -> n__and(X1, X2) 1179.22/297.05 , and(tt(), X) -> activate(X) 1179.22/297.05 , isNatKind(X) -> n__isNatKind(X) 1179.22/297.05 , isNatKind(n__0()) -> tt() 1179.22/297.05 , isNatKind(n__plus(V1, V2)) -> 1179.22/297.05 and(isNatKind(activate(V1)), n__isNatKind(activate(V2))) 1179.22/297.05 , isNatKind(n__s(V1)) -> isNatKind(activate(V1)) 1179.22/297.05 , isNatKind(n__x(V1, V2)) -> 1179.22/297.05 and(isNatKind(activate(V1)), n__isNatKind(activate(V2))) } 1179.22/297.05 Obligation: 1179.22/297.05 innermost runtime complexity 1179.22/297.05 Answer: 1179.22/297.05 MAYBE 1179.22/297.05 1179.22/297.05 None of the processors succeeded. 1179.22/297.05 1179.22/297.05 Details of failed attempt(s): 1179.22/297.05 ----------------------------- 1179.22/297.05 1) 'empty' failed due to the following reason: 1179.22/297.05 1179.22/297.05 Empty strict component of the problem is NOT empty. 1179.22/297.05 1179.22/297.05 2) 'Best' failed due to the following reason: 1179.22/297.05 1179.22/297.05 None of the processors succeeded. 1179.22/297.05 1179.22/297.05 Details of failed attempt(s): 1179.22/297.05 ----------------------------- 1179.22/297.05 1) 'With Problem ... (timeout of 297 seconds)' failed due to the 1179.22/297.05 following reason: 1179.22/297.05 1179.22/297.05 Computation stopped due to timeout after 297.0 seconds. 1179.22/297.05 1179.22/297.05 2) 'Best' failed due to the following reason: 1179.22/297.05 1179.22/297.05 None of the processors succeeded. 1179.22/297.05 1179.22/297.05 Details of failed attempt(s): 1179.22/297.05 ----------------------------- 1179.22/297.05 1) 'With Problem ... (timeout of 148 seconds) (timeout of 297 1179.22/297.05 seconds)' failed due to the following reason: 1179.22/297.05 1179.22/297.05 Computation stopped due to timeout after 148.0 seconds. 1179.22/297.05 1179.22/297.05 2) 'Best' failed due to the following reason: 1179.22/297.05 1179.22/297.05 None of the processors succeeded. 1179.22/297.05 1179.22/297.05 Details of failed attempt(s): 1179.22/297.05 ----------------------------- 1179.22/297.05 1) 'bsearch-popstar (timeout of 297 seconds)' failed due to the 1179.22/297.05 following reason: 1179.22/297.05 1179.22/297.05 The input cannot be shown compatible 1179.22/297.05 1179.22/297.05 2) 'Polynomial Path Order (PS) (timeout of 297 seconds)' failed due 1179.22/297.05 to the following reason: 1179.22/297.05 1179.22/297.05 The input cannot be shown compatible 1179.22/297.05 1179.22/297.05 1179.22/297.05 3) 'Fastest (timeout of 24 seconds) (timeout of 297 seconds)' 1179.22/297.05 failed due to the following reason: 1179.22/297.05 1179.22/297.05 None of the processors succeeded. 1179.22/297.05 1179.22/297.05 Details of failed attempt(s): 1179.22/297.05 ----------------------------- 1179.22/297.05 1) 'Bounds with minimal-enrichment and initial automaton 'match'' 1179.22/297.05 failed due to the following reason: 1179.22/297.05 1179.22/297.05 match-boundness of the problem could not be verified. 1179.22/297.05 1179.22/297.05 2) 'Bounds with perSymbol-enrichment and initial automaton 'match'' 1179.22/297.05 failed due to the following reason: 1179.22/297.05 1179.22/297.05 match-boundness of the problem could not be verified. 1179.22/297.05 1179.22/297.05 1179.22/297.05 1179.22/297.05 1179.22/297.05 1179.22/297.05 Arrrr.. 1179.46/297.12 EOF