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