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