MAYBE 1061.44/297.17 MAYBE 1061.44/297.17 1061.44/297.17 We are left with following problem, upon which TcT provides the 1061.44/297.17 certificate MAYBE. 1061.44/297.17 1061.44/297.17 Strict Trs: 1061.44/297.17 { a__U101(X1, X2, X3) -> U101(X1, X2, X3) 1061.44/297.17 , a__U101(tt(), M, N) -> a__U102(a__isNatKind(M), M, N) 1061.44/297.17 , a__U102(X1, X2, X3) -> U102(X1, X2, X3) 1061.44/297.17 , a__U102(tt(), M, N) -> a__U103(a__isNat(N), M, N) 1061.44/297.17 , a__isNatKind(X) -> isNatKind(X) 1061.44/297.17 , a__isNatKind(s(V1)) -> a__U51(a__isNatKind(V1)) 1061.44/297.17 , a__isNatKind(0()) -> tt() 1061.44/297.17 , a__isNatKind(plus(V1, V2)) -> a__U41(a__isNatKind(V1), V2) 1061.44/297.17 , a__isNatKind(x(V1, V2)) -> a__U61(a__isNatKind(V1), V2) 1061.44/297.17 , a__U103(X1, X2, X3) -> U103(X1, X2, X3) 1061.44/297.17 , a__U103(tt(), M, N) -> a__U104(a__isNatKind(N), M, N) 1061.44/297.17 , a__isNat(X) -> isNat(X) 1061.44/297.17 , a__isNat(s(V1)) -> a__U21(a__isNatKind(V1), V1) 1061.44/297.17 , a__isNat(0()) -> tt() 1061.44/297.17 , a__isNat(plus(V1, V2)) -> a__U11(a__isNatKind(V1), V1, V2) 1061.44/297.17 , a__isNat(x(V1, V2)) -> a__U31(a__isNatKind(V1), V1, V2) 1061.44/297.17 , a__U104(X1, X2, X3) -> U104(X1, X2, X3) 1061.44/297.17 , a__U104(tt(), M, N) -> a__plus(a__x(mark(N), mark(M)), mark(N)) 1061.44/297.17 , a__plus(X1, X2) -> plus(X1, X2) 1061.44/297.17 , a__plus(N, s(M)) -> a__U81(a__isNat(M), M, N) 1061.44/297.17 , a__plus(N, 0()) -> a__U71(a__isNat(N), N) 1061.44/297.17 , a__x(X1, X2) -> x(X1, X2) 1061.44/297.17 , a__x(N, s(M)) -> a__U101(a__isNat(M), M, N) 1061.44/297.17 , a__x(N, 0()) -> a__U91(a__isNat(N), N) 1061.44/297.17 , mark(tt()) -> tt() 1061.44/297.17 , mark(s(X)) -> s(mark(X)) 1061.44/297.17 , mark(0()) -> 0() 1061.44/297.17 , mark(plus(X1, X2)) -> a__plus(mark(X1), mark(X2)) 1061.44/297.17 , mark(x(X1, X2)) -> a__x(mark(X1), mark(X2)) 1061.44/297.17 , mark(U101(X1, X2, X3)) -> a__U101(mark(X1), X2, X3) 1061.44/297.17 , mark(U102(X1, X2, X3)) -> a__U102(mark(X1), X2, X3) 1061.44/297.17 , mark(isNatKind(X)) -> a__isNatKind(X) 1061.44/297.17 , mark(U103(X1, X2, X3)) -> a__U103(mark(X1), X2, X3) 1061.44/297.17 , mark(isNat(X)) -> a__isNat(X) 1061.44/297.17 , mark(U104(X1, X2, X3)) -> a__U104(mark(X1), X2, X3) 1061.44/297.17 , mark(U11(X1, X2, X3)) -> a__U11(mark(X1), X2, X3) 1061.44/297.17 , mark(U12(X1, X2, X3)) -> a__U12(mark(X1), X2, X3) 1061.44/297.17 , mark(U13(X1, X2, X3)) -> a__U13(mark(X1), X2, X3) 1061.44/297.17 , mark(U14(X1, X2, X3)) -> a__U14(mark(X1), X2, X3) 1061.44/297.17 , mark(U15(X1, X2)) -> a__U15(mark(X1), X2) 1061.44/297.17 , mark(U16(X)) -> a__U16(mark(X)) 1061.44/297.17 , mark(U21(X1, X2)) -> a__U21(mark(X1), X2) 1061.44/297.17 , mark(U22(X1, X2)) -> a__U22(mark(X1), X2) 1061.44/297.17 , mark(U23(X)) -> a__U23(mark(X)) 1061.44/297.17 , mark(U31(X1, X2, X3)) -> a__U31(mark(X1), X2, X3) 1061.44/297.17 , mark(U32(X1, X2, X3)) -> a__U32(mark(X1), X2, X3) 1061.44/297.17 , mark(U33(X1, X2, X3)) -> a__U33(mark(X1), X2, X3) 1061.44/297.17 , mark(U34(X1, X2, X3)) -> a__U34(mark(X1), X2, X3) 1061.44/297.17 , mark(U35(X1, X2)) -> a__U35(mark(X1), X2) 1061.44/297.17 , mark(U36(X)) -> a__U36(mark(X)) 1061.44/297.17 , mark(U41(X1, X2)) -> a__U41(mark(X1), X2) 1061.44/297.17 , mark(U42(X)) -> a__U42(mark(X)) 1061.44/297.17 , mark(U51(X)) -> a__U51(mark(X)) 1061.44/297.17 , mark(U61(X1, X2)) -> a__U61(mark(X1), X2) 1061.44/297.17 , mark(U62(X)) -> a__U62(mark(X)) 1061.44/297.17 , mark(U71(X1, X2)) -> a__U71(mark(X1), X2) 1061.44/297.17 , mark(U72(X1, X2)) -> a__U72(mark(X1), X2) 1061.44/297.17 , mark(U81(X1, X2, X3)) -> a__U81(mark(X1), X2, X3) 1061.44/297.17 , mark(U82(X1, X2, X3)) -> a__U82(mark(X1), X2, X3) 1061.44/297.17 , mark(U83(X1, X2, X3)) -> a__U83(mark(X1), X2, X3) 1061.44/297.17 , mark(U84(X1, X2, X3)) -> a__U84(mark(X1), X2, X3) 1061.44/297.17 , mark(U91(X1, X2)) -> a__U91(mark(X1), X2) 1061.44/297.17 , mark(U92(X)) -> a__U92(mark(X)) 1061.44/297.17 , a__U11(X1, X2, X3) -> U11(X1, X2, X3) 1061.44/297.17 , a__U11(tt(), V1, V2) -> a__U12(a__isNatKind(V1), V1, V2) 1061.44/297.17 , a__U12(X1, X2, X3) -> U12(X1, X2, X3) 1061.44/297.17 , a__U12(tt(), V1, V2) -> a__U13(a__isNatKind(V2), V1, V2) 1061.44/297.17 , a__U13(X1, X2, X3) -> U13(X1, X2, X3) 1061.44/297.17 , a__U13(tt(), V1, V2) -> a__U14(a__isNatKind(V2), V1, V2) 1061.44/297.17 , a__U14(X1, X2, X3) -> U14(X1, X2, X3) 1061.44/297.17 , a__U14(tt(), V1, V2) -> a__U15(a__isNat(V1), V2) 1061.44/297.17 , a__U15(X1, X2) -> U15(X1, X2) 1061.44/297.17 , a__U15(tt(), V2) -> a__U16(a__isNat(V2)) 1061.44/297.17 , a__U16(X) -> U16(X) 1061.44/297.17 , a__U16(tt()) -> tt() 1061.44/297.17 , a__U21(X1, X2) -> U21(X1, X2) 1061.44/297.17 , a__U21(tt(), V1) -> a__U22(a__isNatKind(V1), V1) 1061.44/297.17 , a__U22(X1, X2) -> U22(X1, X2) 1061.44/297.17 , a__U22(tt(), V1) -> a__U23(a__isNat(V1)) 1061.44/297.17 , a__U23(X) -> U23(X) 1061.44/297.17 , a__U23(tt()) -> tt() 1061.44/297.17 , a__U31(X1, X2, X3) -> U31(X1, X2, X3) 1061.44/297.17 , a__U31(tt(), V1, V2) -> a__U32(a__isNatKind(V1), V1, V2) 1061.44/297.17 , a__U32(X1, X2, X3) -> U32(X1, X2, X3) 1061.44/297.17 , a__U32(tt(), V1, V2) -> a__U33(a__isNatKind(V2), V1, V2) 1061.44/297.17 , a__U33(X1, X2, X3) -> U33(X1, X2, X3) 1061.44/297.17 , a__U33(tt(), V1, V2) -> a__U34(a__isNatKind(V2), V1, V2) 1061.44/297.17 , a__U34(X1, X2, X3) -> U34(X1, X2, X3) 1061.44/297.17 , a__U34(tt(), V1, V2) -> a__U35(a__isNat(V1), V2) 1061.44/297.17 , a__U35(X1, X2) -> U35(X1, X2) 1061.44/297.17 , a__U35(tt(), V2) -> a__U36(a__isNat(V2)) 1061.44/297.17 , a__U36(X) -> U36(X) 1061.44/297.17 , a__U36(tt()) -> tt() 1061.44/297.17 , a__U41(X1, X2) -> U41(X1, X2) 1061.44/297.17 , a__U41(tt(), V2) -> a__U42(a__isNatKind(V2)) 1061.44/297.17 , a__U42(X) -> U42(X) 1061.44/297.17 , a__U42(tt()) -> tt() 1061.44/297.17 , a__U51(X) -> U51(X) 1061.44/297.17 , a__U51(tt()) -> tt() 1061.44/297.17 , a__U61(X1, X2) -> U61(X1, X2) 1061.44/297.17 , a__U61(tt(), V2) -> a__U62(a__isNatKind(V2)) 1061.44/297.17 , a__U62(X) -> U62(X) 1061.44/297.17 , a__U62(tt()) -> tt() 1061.44/297.17 , a__U71(X1, X2) -> U71(X1, X2) 1061.44/297.17 , a__U71(tt(), N) -> a__U72(a__isNatKind(N), N) 1061.44/297.17 , a__U72(X1, X2) -> U72(X1, X2) 1061.44/297.17 , a__U72(tt(), N) -> mark(N) 1061.44/297.17 , a__U81(X1, X2, X3) -> U81(X1, X2, X3) 1061.44/297.17 , a__U81(tt(), M, N) -> a__U82(a__isNatKind(M), M, N) 1061.44/297.17 , a__U82(X1, X2, X3) -> U82(X1, X2, X3) 1061.44/297.17 , a__U82(tt(), M, N) -> a__U83(a__isNat(N), M, N) 1061.44/297.17 , a__U83(X1, X2, X3) -> U83(X1, X2, X3) 1061.44/297.17 , a__U83(tt(), M, N) -> a__U84(a__isNatKind(N), M, N) 1061.44/297.17 , a__U84(X1, X2, X3) -> U84(X1, X2, X3) 1061.44/297.17 , a__U84(tt(), M, N) -> s(a__plus(mark(N), mark(M))) 1061.44/297.17 , a__U91(X1, X2) -> U91(X1, X2) 1061.44/297.17 , a__U91(tt(), N) -> a__U92(a__isNatKind(N)) 1061.44/297.17 , a__U92(X) -> U92(X) 1061.44/297.17 , a__U92(tt()) -> 0() } 1061.44/297.17 Obligation: 1061.44/297.17 runtime complexity 1061.44/297.17 Answer: 1061.44/297.17 MAYBE 1061.44/297.17 1061.44/297.17 None of the processors succeeded. 1061.44/297.17 1061.44/297.17 Details of failed attempt(s): 1061.44/297.17 ----------------------------- 1061.44/297.17 1) 'With Problem ... (timeout of 297 seconds)' failed due to the 1061.44/297.17 following reason: 1061.44/297.17 1061.44/297.17 Computation stopped due to timeout after 297.0 seconds. 1061.44/297.17 1061.44/297.17 2) 'Weak Dependency Pairs (timeout of 297 seconds)' failed due to 1061.44/297.17 the following reason: 1061.44/297.17 1061.44/297.17 We add the following weak dependency pairs: 1061.44/297.17 1061.44/297.17 Strict DPs: 1061.44/297.17 { a__U101^#(X1, X2, X3) -> c_1(X1, X2, X3) 1061.44/297.17 , a__U101^#(tt(), M, N) -> c_2(a__U102^#(a__isNatKind(M), M, N)) 1061.44/297.17 , a__U102^#(X1, X2, X3) -> c_3(X1, X2, X3) 1061.44/297.17 , a__U102^#(tt(), M, N) -> c_4(a__U103^#(a__isNat(N), M, N)) 1061.44/297.17 , a__U103^#(X1, X2, X3) -> c_10(X1, X2, X3) 1061.44/297.17 , a__U103^#(tt(), M, N) -> c_11(a__U104^#(a__isNatKind(N), M, N)) 1061.44/297.17 , a__isNatKind^#(X) -> c_5(X) 1061.44/297.17 , a__isNatKind^#(s(V1)) -> c_6(a__U51^#(a__isNatKind(V1))) 1061.44/297.17 , a__isNatKind^#(0()) -> c_7() 1061.44/297.17 , a__isNatKind^#(plus(V1, V2)) -> 1061.44/297.17 c_8(a__U41^#(a__isNatKind(V1), V2)) 1061.44/297.17 , a__isNatKind^#(x(V1, V2)) -> c_9(a__U61^#(a__isNatKind(V1), V2)) 1061.44/297.17 , a__U51^#(X) -> c_98(X) 1061.44/297.17 , a__U51^#(tt()) -> c_99() 1061.44/297.17 , a__U41^#(X1, X2) -> c_94(X1, X2) 1061.44/297.17 , a__U41^#(tt(), V2) -> c_95(a__U42^#(a__isNatKind(V2))) 1061.44/297.17 , a__U61^#(X1, X2) -> c_100(X1, X2) 1061.44/297.17 , a__U61^#(tt(), V2) -> c_101(a__U62^#(a__isNatKind(V2))) 1061.44/297.17 , a__U104^#(X1, X2, X3) -> c_17(X1, X2, X3) 1061.44/297.17 , a__U104^#(tt(), M, N) -> 1061.44/297.17 c_18(a__plus^#(a__x(mark(N), mark(M)), mark(N))) 1061.44/297.17 , a__isNat^#(X) -> c_12(X) 1061.44/297.17 , a__isNat^#(s(V1)) -> c_13(a__U21^#(a__isNatKind(V1), V1)) 1061.44/297.17 , a__isNat^#(0()) -> c_14() 1061.44/297.17 , a__isNat^#(plus(V1, V2)) -> 1061.44/297.17 c_15(a__U11^#(a__isNatKind(V1), V1, V2)) 1061.44/297.17 , a__isNat^#(x(V1, V2)) -> c_16(a__U31^#(a__isNatKind(V1), V1, V2)) 1061.44/297.17 , a__U21^#(X1, X2) -> c_76(X1, X2) 1061.44/297.17 , a__U21^#(tt(), V1) -> c_77(a__U22^#(a__isNatKind(V1), V1)) 1061.44/297.17 , a__U11^#(X1, X2, X3) -> c_64(X1, X2, X3) 1061.44/297.17 , a__U11^#(tt(), V1, V2) -> 1061.44/297.17 c_65(a__U12^#(a__isNatKind(V1), V1, V2)) 1061.44/297.17 , a__U31^#(X1, X2, X3) -> c_82(X1, X2, X3) 1061.44/297.17 , a__U31^#(tt(), V1, V2) -> 1061.44/297.17 c_83(a__U32^#(a__isNatKind(V1), V1, V2)) 1061.44/297.17 , a__plus^#(X1, X2) -> c_19(X1, X2) 1061.44/297.17 , a__plus^#(N, s(M)) -> c_20(a__U81^#(a__isNat(M), M, N)) 1061.44/297.17 , a__plus^#(N, 0()) -> c_21(a__U71^#(a__isNat(N), N)) 1061.44/297.17 , a__U81^#(X1, X2, X3) -> c_108(X1, X2, X3) 1061.44/297.17 , a__U81^#(tt(), M, N) -> c_109(a__U82^#(a__isNatKind(M), M, N)) 1061.44/297.17 , a__U71^#(X1, X2) -> c_104(X1, X2) 1061.44/297.17 , a__U71^#(tt(), N) -> c_105(a__U72^#(a__isNatKind(N), N)) 1061.44/297.17 , a__x^#(X1, X2) -> c_22(X1, X2) 1061.44/297.17 , a__x^#(N, s(M)) -> c_23(a__U101^#(a__isNat(M), M, N)) 1061.44/297.17 , a__x^#(N, 0()) -> c_24(a__U91^#(a__isNat(N), N)) 1061.44/297.17 , a__U91^#(X1, X2) -> c_116(X1, X2) 1061.44/297.17 , a__U91^#(tt(), N) -> c_117(a__U92^#(a__isNatKind(N))) 1061.44/297.17 , mark^#(tt()) -> c_25() 1061.44/297.17 , mark^#(s(X)) -> c_26(mark^#(X)) 1061.44/297.17 , mark^#(0()) -> c_27() 1061.44/297.17 , mark^#(plus(X1, X2)) -> c_28(a__plus^#(mark(X1), mark(X2))) 1061.44/297.17 , mark^#(x(X1, X2)) -> c_29(a__x^#(mark(X1), mark(X2))) 1061.44/297.17 , mark^#(U101(X1, X2, X3)) -> c_30(a__U101^#(mark(X1), X2, X3)) 1061.44/297.17 , mark^#(U102(X1, X2, X3)) -> c_31(a__U102^#(mark(X1), X2, X3)) 1061.44/297.17 , mark^#(isNatKind(X)) -> c_32(a__isNatKind^#(X)) 1061.44/297.17 , mark^#(U103(X1, X2, X3)) -> c_33(a__U103^#(mark(X1), X2, X3)) 1061.44/297.17 , mark^#(isNat(X)) -> c_34(a__isNat^#(X)) 1061.44/297.17 , mark^#(U104(X1, X2, X3)) -> c_35(a__U104^#(mark(X1), X2, X3)) 1061.44/297.17 , mark^#(U11(X1, X2, X3)) -> c_36(a__U11^#(mark(X1), X2, X3)) 1061.44/297.17 , mark^#(U12(X1, X2, X3)) -> c_37(a__U12^#(mark(X1), X2, X3)) 1061.44/297.17 , mark^#(U13(X1, X2, X3)) -> c_38(a__U13^#(mark(X1), X2, X3)) 1061.44/297.17 , mark^#(U14(X1, X2, X3)) -> c_39(a__U14^#(mark(X1), X2, X3)) 1061.44/297.17 , mark^#(U15(X1, X2)) -> c_40(a__U15^#(mark(X1), X2)) 1061.44/297.17 , mark^#(U16(X)) -> c_41(a__U16^#(mark(X))) 1061.44/297.17 , mark^#(U21(X1, X2)) -> c_42(a__U21^#(mark(X1), X2)) 1061.44/297.17 , mark^#(U22(X1, X2)) -> c_43(a__U22^#(mark(X1), X2)) 1061.44/297.17 , mark^#(U23(X)) -> c_44(a__U23^#(mark(X))) 1061.44/297.17 , mark^#(U31(X1, X2, X3)) -> c_45(a__U31^#(mark(X1), X2, X3)) 1061.44/297.17 , mark^#(U32(X1, X2, X3)) -> c_46(a__U32^#(mark(X1), X2, X3)) 1061.44/297.17 , mark^#(U33(X1, X2, X3)) -> c_47(a__U33^#(mark(X1), X2, X3)) 1061.44/297.17 , mark^#(U34(X1, X2, X3)) -> c_48(a__U34^#(mark(X1), X2, X3)) 1061.44/297.17 , mark^#(U35(X1, X2)) -> c_49(a__U35^#(mark(X1), X2)) 1061.44/297.17 , mark^#(U36(X)) -> c_50(a__U36^#(mark(X))) 1061.44/297.17 , mark^#(U41(X1, X2)) -> c_51(a__U41^#(mark(X1), X2)) 1061.44/297.17 , mark^#(U42(X)) -> c_52(a__U42^#(mark(X))) 1061.44/297.17 , mark^#(U51(X)) -> c_53(a__U51^#(mark(X))) 1061.44/297.17 , mark^#(U61(X1, X2)) -> c_54(a__U61^#(mark(X1), X2)) 1061.44/297.17 , mark^#(U62(X)) -> c_55(a__U62^#(mark(X))) 1061.44/297.17 , mark^#(U71(X1, X2)) -> c_56(a__U71^#(mark(X1), X2)) 1061.44/297.17 , mark^#(U72(X1, X2)) -> c_57(a__U72^#(mark(X1), X2)) 1061.44/297.17 , mark^#(U81(X1, X2, X3)) -> c_58(a__U81^#(mark(X1), X2, X3)) 1061.44/297.17 , mark^#(U82(X1, X2, X3)) -> c_59(a__U82^#(mark(X1), X2, X3)) 1061.44/297.17 , mark^#(U83(X1, X2, X3)) -> c_60(a__U83^#(mark(X1), X2, X3)) 1061.44/297.17 , mark^#(U84(X1, X2, X3)) -> c_61(a__U84^#(mark(X1), X2, X3)) 1061.44/297.17 , mark^#(U91(X1, X2)) -> c_62(a__U91^#(mark(X1), X2)) 1061.44/297.17 , mark^#(U92(X)) -> c_63(a__U92^#(mark(X))) 1061.44/297.17 , a__U12^#(X1, X2, X3) -> c_66(X1, X2, X3) 1061.44/297.17 , a__U12^#(tt(), V1, V2) -> 1061.44/297.17 c_67(a__U13^#(a__isNatKind(V2), V1, V2)) 1061.44/297.17 , a__U13^#(X1, X2, X3) -> c_68(X1, X2, X3) 1061.44/297.17 , a__U13^#(tt(), V1, V2) -> 1061.44/297.17 c_69(a__U14^#(a__isNatKind(V2), V1, V2)) 1061.44/297.17 , a__U14^#(X1, X2, X3) -> c_70(X1, X2, X3) 1061.44/297.17 , a__U14^#(tt(), V1, V2) -> c_71(a__U15^#(a__isNat(V1), V2)) 1061.44/297.17 , a__U15^#(X1, X2) -> c_72(X1, X2) 1061.44/297.17 , a__U15^#(tt(), V2) -> c_73(a__U16^#(a__isNat(V2))) 1061.44/297.17 , a__U16^#(X) -> c_74(X) 1061.44/297.17 , a__U16^#(tt()) -> c_75() 1061.44/297.17 , a__U22^#(X1, X2) -> c_78(X1, X2) 1061.44/297.17 , a__U22^#(tt(), V1) -> c_79(a__U23^#(a__isNat(V1))) 1061.44/297.17 , a__U23^#(X) -> c_80(X) 1061.44/297.17 , a__U23^#(tt()) -> c_81() 1061.44/297.17 , a__U32^#(X1, X2, X3) -> c_84(X1, X2, X3) 1061.44/297.17 , a__U32^#(tt(), V1, V2) -> 1061.44/297.17 c_85(a__U33^#(a__isNatKind(V2), V1, V2)) 1061.44/297.17 , a__U33^#(X1, X2, X3) -> c_86(X1, X2, X3) 1061.44/297.17 , a__U33^#(tt(), V1, V2) -> 1061.44/297.17 c_87(a__U34^#(a__isNatKind(V2), V1, V2)) 1061.44/297.17 , a__U34^#(X1, X2, X3) -> c_88(X1, X2, X3) 1061.44/297.17 , a__U34^#(tt(), V1, V2) -> c_89(a__U35^#(a__isNat(V1), V2)) 1061.44/297.17 , a__U35^#(X1, X2) -> c_90(X1, X2) 1061.44/297.17 , a__U35^#(tt(), V2) -> c_91(a__U36^#(a__isNat(V2))) 1061.44/297.17 , a__U36^#(X) -> c_92(X) 1061.44/297.17 , a__U36^#(tt()) -> c_93() 1061.44/297.17 , a__U42^#(X) -> c_96(X) 1061.44/297.17 , a__U42^#(tt()) -> c_97() 1061.44/297.17 , a__U62^#(X) -> c_102(X) 1061.44/297.17 , a__U62^#(tt()) -> c_103() 1061.44/297.17 , a__U72^#(X1, X2) -> c_106(X1, X2) 1061.44/297.17 , a__U72^#(tt(), N) -> c_107(mark^#(N)) 1061.44/297.17 , a__U82^#(X1, X2, X3) -> c_110(X1, X2, X3) 1061.44/297.17 , a__U82^#(tt(), M, N) -> c_111(a__U83^#(a__isNat(N), M, N)) 1061.44/297.17 , a__U83^#(X1, X2, X3) -> c_112(X1, X2, X3) 1061.44/297.17 , a__U83^#(tt(), M, N) -> c_113(a__U84^#(a__isNatKind(N), M, N)) 1061.44/297.17 , a__U84^#(X1, X2, X3) -> c_114(X1, X2, X3) 1061.44/297.17 , a__U84^#(tt(), M, N) -> c_115(a__plus^#(mark(N), mark(M))) 1061.44/297.17 , a__U92^#(X) -> c_118(X) 1061.44/297.17 , a__U92^#(tt()) -> c_119() } 1061.44/297.17 1061.44/297.17 and mark the set of starting terms. 1061.44/297.17 1061.44/297.17 We are left with following problem, upon which TcT provides the 1061.44/297.17 certificate MAYBE. 1061.44/297.17 1061.44/297.17 Strict DPs: 1061.44/297.17 { a__U101^#(X1, X2, X3) -> c_1(X1, X2, X3) 1061.44/297.17 , a__U101^#(tt(), M, N) -> c_2(a__U102^#(a__isNatKind(M), M, N)) 1061.44/297.17 , a__U102^#(X1, X2, X3) -> c_3(X1, X2, X3) 1061.44/297.17 , a__U102^#(tt(), M, N) -> c_4(a__U103^#(a__isNat(N), M, N)) 1061.44/297.17 , a__U103^#(X1, X2, X3) -> c_10(X1, X2, X3) 1061.44/297.17 , a__U103^#(tt(), M, N) -> c_11(a__U104^#(a__isNatKind(N), M, N)) 1061.44/297.17 , a__isNatKind^#(X) -> c_5(X) 1061.44/297.17 , a__isNatKind^#(s(V1)) -> c_6(a__U51^#(a__isNatKind(V1))) 1061.44/297.17 , a__isNatKind^#(0()) -> c_7() 1061.44/297.17 , a__isNatKind^#(plus(V1, V2)) -> 1061.44/297.17 c_8(a__U41^#(a__isNatKind(V1), V2)) 1061.44/297.17 , a__isNatKind^#(x(V1, V2)) -> c_9(a__U61^#(a__isNatKind(V1), V2)) 1061.44/297.17 , a__U51^#(X) -> c_98(X) 1061.44/297.17 , a__U51^#(tt()) -> c_99() 1061.44/297.17 , a__U41^#(X1, X2) -> c_94(X1, X2) 1061.44/297.17 , a__U41^#(tt(), V2) -> c_95(a__U42^#(a__isNatKind(V2))) 1061.44/297.17 , a__U61^#(X1, X2) -> c_100(X1, X2) 1061.44/297.17 , a__U61^#(tt(), V2) -> c_101(a__U62^#(a__isNatKind(V2))) 1061.44/297.17 , a__U104^#(X1, X2, X3) -> c_17(X1, X2, X3) 1061.44/297.17 , a__U104^#(tt(), M, N) -> 1061.44/297.17 c_18(a__plus^#(a__x(mark(N), mark(M)), mark(N))) 1061.44/297.17 , a__isNat^#(X) -> c_12(X) 1061.44/297.17 , a__isNat^#(s(V1)) -> c_13(a__U21^#(a__isNatKind(V1), V1)) 1061.44/297.17 , a__isNat^#(0()) -> c_14() 1061.44/297.17 , a__isNat^#(plus(V1, V2)) -> 1061.44/297.17 c_15(a__U11^#(a__isNatKind(V1), V1, V2)) 1061.44/297.17 , a__isNat^#(x(V1, V2)) -> c_16(a__U31^#(a__isNatKind(V1), V1, V2)) 1061.44/297.17 , a__U21^#(X1, X2) -> c_76(X1, X2) 1061.44/297.17 , a__U21^#(tt(), V1) -> c_77(a__U22^#(a__isNatKind(V1), V1)) 1061.44/297.17 , a__U11^#(X1, X2, X3) -> c_64(X1, X2, X3) 1061.44/297.17 , a__U11^#(tt(), V1, V2) -> 1061.44/297.17 c_65(a__U12^#(a__isNatKind(V1), V1, V2)) 1061.44/297.17 , a__U31^#(X1, X2, X3) -> c_82(X1, X2, X3) 1061.44/297.17 , a__U31^#(tt(), V1, V2) -> 1061.44/297.17 c_83(a__U32^#(a__isNatKind(V1), V1, V2)) 1061.44/297.17 , a__plus^#(X1, X2) -> c_19(X1, X2) 1061.44/297.17 , a__plus^#(N, s(M)) -> c_20(a__U81^#(a__isNat(M), M, N)) 1061.44/297.17 , a__plus^#(N, 0()) -> c_21(a__U71^#(a__isNat(N), N)) 1061.44/297.17 , a__U81^#(X1, X2, X3) -> c_108(X1, X2, X3) 1061.44/297.17 , a__U81^#(tt(), M, N) -> c_109(a__U82^#(a__isNatKind(M), M, N)) 1061.44/297.17 , a__U71^#(X1, X2) -> c_104(X1, X2) 1061.44/297.17 , a__U71^#(tt(), N) -> c_105(a__U72^#(a__isNatKind(N), N)) 1061.44/297.17 , a__x^#(X1, X2) -> c_22(X1, X2) 1061.44/297.17 , a__x^#(N, s(M)) -> c_23(a__U101^#(a__isNat(M), M, N)) 1061.44/297.17 , a__x^#(N, 0()) -> c_24(a__U91^#(a__isNat(N), N)) 1061.44/297.17 , a__U91^#(X1, X2) -> c_116(X1, X2) 1061.44/297.17 , a__U91^#(tt(), N) -> c_117(a__U92^#(a__isNatKind(N))) 1061.44/297.17 , mark^#(tt()) -> c_25() 1061.44/297.17 , mark^#(s(X)) -> c_26(mark^#(X)) 1061.44/297.17 , mark^#(0()) -> c_27() 1061.44/297.17 , mark^#(plus(X1, X2)) -> c_28(a__plus^#(mark(X1), mark(X2))) 1061.44/297.17 , mark^#(x(X1, X2)) -> c_29(a__x^#(mark(X1), mark(X2))) 1061.44/297.17 , mark^#(U101(X1, X2, X3)) -> c_30(a__U101^#(mark(X1), X2, X3)) 1061.44/297.17 , mark^#(U102(X1, X2, X3)) -> c_31(a__U102^#(mark(X1), X2, X3)) 1061.44/297.17 , mark^#(isNatKind(X)) -> c_32(a__isNatKind^#(X)) 1061.44/297.17 , mark^#(U103(X1, X2, X3)) -> c_33(a__U103^#(mark(X1), X2, X3)) 1061.44/297.17 , mark^#(isNat(X)) -> c_34(a__isNat^#(X)) 1061.44/297.17 , mark^#(U104(X1, X2, X3)) -> c_35(a__U104^#(mark(X1), X2, X3)) 1061.44/297.17 , mark^#(U11(X1, X2, X3)) -> c_36(a__U11^#(mark(X1), X2, X3)) 1061.44/297.17 , mark^#(U12(X1, X2, X3)) -> c_37(a__U12^#(mark(X1), X2, X3)) 1061.44/297.17 , mark^#(U13(X1, X2, X3)) -> c_38(a__U13^#(mark(X1), X2, X3)) 1061.44/297.17 , mark^#(U14(X1, X2, X3)) -> c_39(a__U14^#(mark(X1), X2, X3)) 1061.44/297.17 , mark^#(U15(X1, X2)) -> c_40(a__U15^#(mark(X1), X2)) 1061.44/297.17 , mark^#(U16(X)) -> c_41(a__U16^#(mark(X))) 1061.44/297.17 , mark^#(U21(X1, X2)) -> c_42(a__U21^#(mark(X1), X2)) 1061.44/297.17 , mark^#(U22(X1, X2)) -> c_43(a__U22^#(mark(X1), X2)) 1061.44/297.17 , mark^#(U23(X)) -> c_44(a__U23^#(mark(X))) 1061.44/297.17 , mark^#(U31(X1, X2, X3)) -> c_45(a__U31^#(mark(X1), X2, X3)) 1061.44/297.17 , mark^#(U32(X1, X2, X3)) -> c_46(a__U32^#(mark(X1), X2, X3)) 1061.44/297.17 , mark^#(U33(X1, X2, X3)) -> c_47(a__U33^#(mark(X1), X2, X3)) 1061.44/297.17 , mark^#(U34(X1, X2, X3)) -> c_48(a__U34^#(mark(X1), X2, X3)) 1061.44/297.17 , mark^#(U35(X1, X2)) -> c_49(a__U35^#(mark(X1), X2)) 1061.44/297.17 , mark^#(U36(X)) -> c_50(a__U36^#(mark(X))) 1061.44/297.18 , mark^#(U41(X1, X2)) -> c_51(a__U41^#(mark(X1), X2)) 1061.44/297.18 , mark^#(U42(X)) -> c_52(a__U42^#(mark(X))) 1061.44/297.18 , mark^#(U51(X)) -> c_53(a__U51^#(mark(X))) 1061.44/297.18 , mark^#(U61(X1, X2)) -> c_54(a__U61^#(mark(X1), X2)) 1061.44/297.18 , mark^#(U62(X)) -> c_55(a__U62^#(mark(X))) 1061.44/297.18 , mark^#(U71(X1, X2)) -> c_56(a__U71^#(mark(X1), X2)) 1061.44/297.18 , mark^#(U72(X1, X2)) -> c_57(a__U72^#(mark(X1), X2)) 1061.44/297.18 , mark^#(U81(X1, X2, X3)) -> c_58(a__U81^#(mark(X1), X2, X3)) 1061.44/297.18 , mark^#(U82(X1, X2, X3)) -> c_59(a__U82^#(mark(X1), X2, X3)) 1061.44/297.18 , mark^#(U83(X1, X2, X3)) -> c_60(a__U83^#(mark(X1), X2, X3)) 1061.44/297.18 , mark^#(U84(X1, X2, X3)) -> c_61(a__U84^#(mark(X1), X2, X3)) 1061.44/297.18 , mark^#(U91(X1, X2)) -> c_62(a__U91^#(mark(X1), X2)) 1061.44/297.18 , mark^#(U92(X)) -> c_63(a__U92^#(mark(X))) 1061.44/297.18 , a__U12^#(X1, X2, X3) -> c_66(X1, X2, X3) 1061.44/297.18 , a__U12^#(tt(), V1, V2) -> 1061.44/297.18 c_67(a__U13^#(a__isNatKind(V2), V1, V2)) 1061.44/297.18 , a__U13^#(X1, X2, X3) -> c_68(X1, X2, X3) 1061.44/297.18 , a__U13^#(tt(), V1, V2) -> 1061.44/297.18 c_69(a__U14^#(a__isNatKind(V2), V1, V2)) 1061.44/297.18 , a__U14^#(X1, X2, X3) -> c_70(X1, X2, X3) 1061.44/297.18 , a__U14^#(tt(), V1, V2) -> c_71(a__U15^#(a__isNat(V1), V2)) 1061.44/297.18 , a__U15^#(X1, X2) -> c_72(X1, X2) 1061.44/297.18 , a__U15^#(tt(), V2) -> c_73(a__U16^#(a__isNat(V2))) 1061.44/297.18 , a__U16^#(X) -> c_74(X) 1061.44/297.18 , a__U16^#(tt()) -> c_75() 1061.44/297.18 , a__U22^#(X1, X2) -> c_78(X1, X2) 1061.44/297.18 , a__U22^#(tt(), V1) -> c_79(a__U23^#(a__isNat(V1))) 1061.44/297.18 , a__U23^#(X) -> c_80(X) 1061.44/297.18 , a__U23^#(tt()) -> c_81() 1061.44/297.18 , a__U32^#(X1, X2, X3) -> c_84(X1, X2, X3) 1061.44/297.18 , a__U32^#(tt(), V1, V2) -> 1061.44/297.18 c_85(a__U33^#(a__isNatKind(V2), V1, V2)) 1061.44/297.18 , a__U33^#(X1, X2, X3) -> c_86(X1, X2, X3) 1061.44/297.18 , a__U33^#(tt(), V1, V2) -> 1061.44/297.18 c_87(a__U34^#(a__isNatKind(V2), V1, V2)) 1061.44/297.18 , a__U34^#(X1, X2, X3) -> c_88(X1, X2, X3) 1061.44/297.18 , a__U34^#(tt(), V1, V2) -> c_89(a__U35^#(a__isNat(V1), V2)) 1061.44/297.18 , a__U35^#(X1, X2) -> c_90(X1, X2) 1061.44/297.18 , a__U35^#(tt(), V2) -> c_91(a__U36^#(a__isNat(V2))) 1061.44/297.18 , a__U36^#(X) -> c_92(X) 1061.44/297.18 , a__U36^#(tt()) -> c_93() 1061.44/297.18 , a__U42^#(X) -> c_96(X) 1061.44/297.18 , a__U42^#(tt()) -> c_97() 1061.44/297.18 , a__U62^#(X) -> c_102(X) 1061.44/297.18 , a__U62^#(tt()) -> c_103() 1061.44/297.18 , a__U72^#(X1, X2) -> c_106(X1, X2) 1061.44/297.18 , a__U72^#(tt(), N) -> c_107(mark^#(N)) 1061.44/297.18 , a__U82^#(X1, X2, X3) -> c_110(X1, X2, X3) 1061.44/297.18 , a__U82^#(tt(), M, N) -> c_111(a__U83^#(a__isNat(N), M, N)) 1061.44/297.18 , a__U83^#(X1, X2, X3) -> c_112(X1, X2, X3) 1061.44/297.18 , a__U83^#(tt(), M, N) -> c_113(a__U84^#(a__isNatKind(N), M, N)) 1061.44/297.18 , a__U84^#(X1, X2, X3) -> c_114(X1, X2, X3) 1061.44/297.18 , a__U84^#(tt(), M, N) -> c_115(a__plus^#(mark(N), mark(M))) 1061.44/297.18 , a__U92^#(X) -> c_118(X) 1061.44/297.18 , a__U92^#(tt()) -> c_119() } 1061.44/297.18 Strict Trs: 1061.44/297.18 { a__U101(X1, X2, X3) -> U101(X1, X2, X3) 1061.44/297.18 , a__U101(tt(), M, N) -> a__U102(a__isNatKind(M), M, N) 1061.44/297.18 , a__U102(X1, X2, X3) -> U102(X1, X2, X3) 1061.44/297.18 , a__U102(tt(), M, N) -> a__U103(a__isNat(N), M, N) 1061.44/297.18 , a__isNatKind(X) -> isNatKind(X) 1061.44/297.18 , a__isNatKind(s(V1)) -> a__U51(a__isNatKind(V1)) 1061.44/297.18 , a__isNatKind(0()) -> tt() 1061.44/297.18 , a__isNatKind(plus(V1, V2)) -> a__U41(a__isNatKind(V1), V2) 1061.44/297.18 , a__isNatKind(x(V1, V2)) -> a__U61(a__isNatKind(V1), V2) 1061.44/297.18 , a__U103(X1, X2, X3) -> U103(X1, X2, X3) 1061.44/297.18 , a__U103(tt(), M, N) -> a__U104(a__isNatKind(N), M, N) 1061.44/297.18 , a__isNat(X) -> isNat(X) 1061.44/297.18 , a__isNat(s(V1)) -> a__U21(a__isNatKind(V1), V1) 1061.44/297.18 , a__isNat(0()) -> tt() 1061.44/297.18 , a__isNat(plus(V1, V2)) -> a__U11(a__isNatKind(V1), V1, V2) 1061.44/297.18 , a__isNat(x(V1, V2)) -> a__U31(a__isNatKind(V1), V1, V2) 1061.44/297.18 , a__U104(X1, X2, X3) -> U104(X1, X2, X3) 1061.44/297.18 , a__U104(tt(), M, N) -> a__plus(a__x(mark(N), mark(M)), mark(N)) 1061.44/297.18 , a__plus(X1, X2) -> plus(X1, X2) 1061.44/297.18 , a__plus(N, s(M)) -> a__U81(a__isNat(M), M, N) 1061.44/297.18 , a__plus(N, 0()) -> a__U71(a__isNat(N), N) 1061.44/297.18 , a__x(X1, X2) -> x(X1, X2) 1061.44/297.18 , a__x(N, s(M)) -> a__U101(a__isNat(M), M, N) 1061.44/297.18 , a__x(N, 0()) -> a__U91(a__isNat(N), N) 1061.44/297.18 , mark(tt()) -> tt() 1061.44/297.18 , mark(s(X)) -> s(mark(X)) 1061.44/297.18 , mark(0()) -> 0() 1061.44/297.18 , mark(plus(X1, X2)) -> a__plus(mark(X1), mark(X2)) 1061.44/297.18 , mark(x(X1, X2)) -> a__x(mark(X1), mark(X2)) 1061.44/297.18 , mark(U101(X1, X2, X3)) -> a__U101(mark(X1), X2, X3) 1061.44/297.18 , mark(U102(X1, X2, X3)) -> a__U102(mark(X1), X2, X3) 1061.44/297.18 , mark(isNatKind(X)) -> a__isNatKind(X) 1061.44/297.18 , mark(U103(X1, X2, X3)) -> a__U103(mark(X1), X2, X3) 1061.44/297.18 , mark(isNat(X)) -> a__isNat(X) 1061.44/297.18 , mark(U104(X1, X2, X3)) -> a__U104(mark(X1), X2, X3) 1061.44/297.18 , mark(U11(X1, X2, X3)) -> a__U11(mark(X1), X2, X3) 1061.44/297.18 , mark(U12(X1, X2, X3)) -> a__U12(mark(X1), X2, X3) 1061.44/297.18 , mark(U13(X1, X2, X3)) -> a__U13(mark(X1), X2, X3) 1061.44/297.18 , mark(U14(X1, X2, X3)) -> a__U14(mark(X1), X2, X3) 1061.44/297.18 , mark(U15(X1, X2)) -> a__U15(mark(X1), X2) 1061.44/297.18 , mark(U16(X)) -> a__U16(mark(X)) 1061.44/297.18 , mark(U21(X1, X2)) -> a__U21(mark(X1), X2) 1061.44/297.18 , mark(U22(X1, X2)) -> a__U22(mark(X1), X2) 1061.44/297.18 , mark(U23(X)) -> a__U23(mark(X)) 1061.44/297.18 , mark(U31(X1, X2, X3)) -> a__U31(mark(X1), X2, X3) 1061.44/297.18 , mark(U32(X1, X2, X3)) -> a__U32(mark(X1), X2, X3) 1061.44/297.18 , mark(U33(X1, X2, X3)) -> a__U33(mark(X1), X2, X3) 1061.44/297.18 , mark(U34(X1, X2, X3)) -> a__U34(mark(X1), X2, X3) 1061.44/297.18 , mark(U35(X1, X2)) -> a__U35(mark(X1), X2) 1061.44/297.18 , mark(U36(X)) -> a__U36(mark(X)) 1061.44/297.18 , mark(U41(X1, X2)) -> a__U41(mark(X1), X2) 1061.44/297.18 , mark(U42(X)) -> a__U42(mark(X)) 1061.44/297.18 , mark(U51(X)) -> a__U51(mark(X)) 1061.44/297.18 , mark(U61(X1, X2)) -> a__U61(mark(X1), X2) 1061.44/297.18 , mark(U62(X)) -> a__U62(mark(X)) 1061.44/297.18 , mark(U71(X1, X2)) -> a__U71(mark(X1), X2) 1061.44/297.18 , mark(U72(X1, X2)) -> a__U72(mark(X1), X2) 1061.44/297.18 , mark(U81(X1, X2, X3)) -> a__U81(mark(X1), X2, X3) 1061.44/297.18 , mark(U82(X1, X2, X3)) -> a__U82(mark(X1), X2, X3) 1061.44/297.18 , mark(U83(X1, X2, X3)) -> a__U83(mark(X1), X2, X3) 1061.44/297.18 , mark(U84(X1, X2, X3)) -> a__U84(mark(X1), X2, X3) 1061.44/297.18 , mark(U91(X1, X2)) -> a__U91(mark(X1), X2) 1061.44/297.18 , mark(U92(X)) -> a__U92(mark(X)) 1061.44/297.18 , a__U11(X1, X2, X3) -> U11(X1, X2, X3) 1061.44/297.18 , a__U11(tt(), V1, V2) -> a__U12(a__isNatKind(V1), V1, V2) 1061.44/297.18 , a__U12(X1, X2, X3) -> U12(X1, X2, X3) 1061.44/297.18 , a__U12(tt(), V1, V2) -> a__U13(a__isNatKind(V2), V1, V2) 1061.44/297.18 , a__U13(X1, X2, X3) -> U13(X1, X2, X3) 1061.44/297.18 , a__U13(tt(), V1, V2) -> a__U14(a__isNatKind(V2), V1, V2) 1061.44/297.18 , a__U14(X1, X2, X3) -> U14(X1, X2, X3) 1061.44/297.18 , a__U14(tt(), V1, V2) -> a__U15(a__isNat(V1), V2) 1061.44/297.18 , a__U15(X1, X2) -> U15(X1, X2) 1061.44/297.18 , a__U15(tt(), V2) -> a__U16(a__isNat(V2)) 1061.44/297.18 , a__U16(X) -> U16(X) 1061.44/297.18 , a__U16(tt()) -> tt() 1061.44/297.18 , a__U21(X1, X2) -> U21(X1, X2) 1061.44/297.18 , a__U21(tt(), V1) -> a__U22(a__isNatKind(V1), V1) 1061.44/297.18 , a__U22(X1, X2) -> U22(X1, X2) 1061.44/297.18 , a__U22(tt(), V1) -> a__U23(a__isNat(V1)) 1061.44/297.18 , a__U23(X) -> U23(X) 1061.44/297.18 , a__U23(tt()) -> tt() 1061.44/297.18 , a__U31(X1, X2, X3) -> U31(X1, X2, X3) 1061.44/297.18 , a__U31(tt(), V1, V2) -> a__U32(a__isNatKind(V1), V1, V2) 1061.44/297.18 , a__U32(X1, X2, X3) -> U32(X1, X2, X3) 1061.44/297.18 , a__U32(tt(), V1, V2) -> a__U33(a__isNatKind(V2), V1, V2) 1061.44/297.18 , a__U33(X1, X2, X3) -> U33(X1, X2, X3) 1061.44/297.18 , a__U33(tt(), V1, V2) -> a__U34(a__isNatKind(V2), V1, V2) 1061.44/297.18 , a__U34(X1, X2, X3) -> U34(X1, X2, X3) 1061.44/297.18 , a__U34(tt(), V1, V2) -> a__U35(a__isNat(V1), V2) 1061.44/297.18 , a__U35(X1, X2) -> U35(X1, X2) 1061.44/297.18 , a__U35(tt(), V2) -> a__U36(a__isNat(V2)) 1061.44/297.18 , a__U36(X) -> U36(X) 1061.44/297.18 , a__U36(tt()) -> tt() 1061.44/297.18 , a__U41(X1, X2) -> U41(X1, X2) 1061.44/297.18 , a__U41(tt(), V2) -> a__U42(a__isNatKind(V2)) 1061.44/297.18 , a__U42(X) -> U42(X) 1061.44/297.18 , a__U42(tt()) -> tt() 1061.44/297.18 , a__U51(X) -> U51(X) 1061.44/297.18 , a__U51(tt()) -> tt() 1061.44/297.18 , a__U61(X1, X2) -> U61(X1, X2) 1061.44/297.18 , a__U61(tt(), V2) -> a__U62(a__isNatKind(V2)) 1061.44/297.18 , a__U62(X) -> U62(X) 1061.44/297.18 , a__U62(tt()) -> tt() 1061.44/297.18 , a__U71(X1, X2) -> U71(X1, X2) 1061.44/297.18 , a__U71(tt(), N) -> a__U72(a__isNatKind(N), N) 1061.44/297.18 , a__U72(X1, X2) -> U72(X1, X2) 1061.44/297.18 , a__U72(tt(), N) -> mark(N) 1061.44/297.18 , a__U81(X1, X2, X3) -> U81(X1, X2, X3) 1061.44/297.18 , a__U81(tt(), M, N) -> a__U82(a__isNatKind(M), M, N) 1061.44/297.18 , a__U82(X1, X2, X3) -> U82(X1, X2, X3) 1061.44/297.18 , a__U82(tt(), M, N) -> a__U83(a__isNat(N), M, N) 1061.44/297.18 , a__U83(X1, X2, X3) -> U83(X1, X2, X3) 1061.44/297.18 , a__U83(tt(), M, N) -> a__U84(a__isNatKind(N), M, N) 1061.44/297.18 , a__U84(X1, X2, X3) -> U84(X1, X2, X3) 1061.44/297.18 , a__U84(tt(), M, N) -> s(a__plus(mark(N), mark(M))) 1061.44/297.18 , a__U91(X1, X2) -> U91(X1, X2) 1061.44/297.18 , a__U91(tt(), N) -> a__U92(a__isNatKind(N)) 1061.44/297.18 , a__U92(X) -> U92(X) 1061.44/297.18 , a__U92(tt()) -> 0() } 1061.44/297.18 Obligation: 1061.44/297.18 runtime complexity 1061.44/297.18 Answer: 1061.44/297.18 MAYBE 1061.44/297.18 1061.44/297.18 We estimate the number of application of 1061.44/297.18 {9,13,22,43,45,91,95,105,107,109,119} by applications of 1061.44/297.18 Pre({9,13,22,43,45,91,95,105,107,109,119}) = 1061.44/297.18 {1,3,5,7,8,12,14,15,16,17,18,20,25,27,29,31,34,36,38,41,42,44,50,52,59,62,68,70,71,73,81,82,84,86,88,89,90,92,93,94,96,98,100,102,103,104,106,108,110,111,112,114,116,118}. 1061.44/297.18 Here rules are labeled as follows: 1061.44/297.18 1061.44/297.18 DPs: 1061.44/297.18 { 1: a__U101^#(X1, X2, X3) -> c_1(X1, X2, X3) 1061.44/297.18 , 2: a__U101^#(tt(), M, N) -> c_2(a__U102^#(a__isNatKind(M), M, N)) 1061.44/297.18 , 3: a__U102^#(X1, X2, X3) -> c_3(X1, X2, X3) 1061.44/297.18 , 4: a__U102^#(tt(), M, N) -> c_4(a__U103^#(a__isNat(N), M, N)) 1061.44/297.18 , 5: a__U103^#(X1, X2, X3) -> c_10(X1, X2, X3) 1061.44/297.18 , 6: a__U103^#(tt(), M, N) -> 1061.44/297.18 c_11(a__U104^#(a__isNatKind(N), M, N)) 1061.44/297.18 , 7: a__isNatKind^#(X) -> c_5(X) 1061.44/297.18 , 8: a__isNatKind^#(s(V1)) -> c_6(a__U51^#(a__isNatKind(V1))) 1061.44/297.18 , 9: a__isNatKind^#(0()) -> c_7() 1061.44/297.18 , 10: a__isNatKind^#(plus(V1, V2)) -> 1061.44/297.18 c_8(a__U41^#(a__isNatKind(V1), V2)) 1061.44/297.18 , 11: a__isNatKind^#(x(V1, V2)) -> 1061.44/297.18 c_9(a__U61^#(a__isNatKind(V1), V2)) 1061.44/297.18 , 12: a__U51^#(X) -> c_98(X) 1061.44/297.18 , 13: a__U51^#(tt()) -> c_99() 1061.44/297.18 , 14: a__U41^#(X1, X2) -> c_94(X1, X2) 1061.44/297.18 , 15: a__U41^#(tt(), V2) -> c_95(a__U42^#(a__isNatKind(V2))) 1061.44/297.18 , 16: a__U61^#(X1, X2) -> c_100(X1, X2) 1061.44/297.18 , 17: a__U61^#(tt(), V2) -> c_101(a__U62^#(a__isNatKind(V2))) 1061.44/297.18 , 18: a__U104^#(X1, X2, X3) -> c_17(X1, X2, X3) 1061.44/297.18 , 19: a__U104^#(tt(), M, N) -> 1061.44/297.18 c_18(a__plus^#(a__x(mark(N), mark(M)), mark(N))) 1061.44/297.18 , 20: a__isNat^#(X) -> c_12(X) 1061.44/297.18 , 21: a__isNat^#(s(V1)) -> c_13(a__U21^#(a__isNatKind(V1), V1)) 1061.44/297.18 , 22: a__isNat^#(0()) -> c_14() 1061.44/297.18 , 23: a__isNat^#(plus(V1, V2)) -> 1061.44/297.18 c_15(a__U11^#(a__isNatKind(V1), V1, V2)) 1061.44/297.18 , 24: a__isNat^#(x(V1, V2)) -> 1061.44/297.18 c_16(a__U31^#(a__isNatKind(V1), V1, V2)) 1061.44/297.18 , 25: a__U21^#(X1, X2) -> c_76(X1, X2) 1061.44/297.18 , 26: a__U21^#(tt(), V1) -> c_77(a__U22^#(a__isNatKind(V1), V1)) 1061.44/297.18 , 27: a__U11^#(X1, X2, X3) -> c_64(X1, X2, X3) 1061.44/297.18 , 28: a__U11^#(tt(), V1, V2) -> 1061.44/297.18 c_65(a__U12^#(a__isNatKind(V1), V1, V2)) 1061.44/297.18 , 29: a__U31^#(X1, X2, X3) -> c_82(X1, X2, X3) 1061.44/297.18 , 30: a__U31^#(tt(), V1, V2) -> 1061.44/297.18 c_83(a__U32^#(a__isNatKind(V1), V1, V2)) 1061.44/297.18 , 31: a__plus^#(X1, X2) -> c_19(X1, X2) 1061.44/297.18 , 32: a__plus^#(N, s(M)) -> c_20(a__U81^#(a__isNat(M), M, N)) 1061.44/297.18 , 33: a__plus^#(N, 0()) -> c_21(a__U71^#(a__isNat(N), N)) 1061.44/297.18 , 34: a__U81^#(X1, X2, X3) -> c_108(X1, X2, X3) 1061.44/297.18 , 35: a__U81^#(tt(), M, N) -> 1061.44/297.18 c_109(a__U82^#(a__isNatKind(M), M, N)) 1061.44/297.18 , 36: a__U71^#(X1, X2) -> c_104(X1, X2) 1061.44/297.18 , 37: a__U71^#(tt(), N) -> c_105(a__U72^#(a__isNatKind(N), N)) 1061.44/297.18 , 38: a__x^#(X1, X2) -> c_22(X1, X2) 1061.44/297.18 , 39: a__x^#(N, s(M)) -> c_23(a__U101^#(a__isNat(M), M, N)) 1061.44/297.18 , 40: a__x^#(N, 0()) -> c_24(a__U91^#(a__isNat(N), N)) 1061.44/297.18 , 41: a__U91^#(X1, X2) -> c_116(X1, X2) 1061.44/297.18 , 42: a__U91^#(tt(), N) -> c_117(a__U92^#(a__isNatKind(N))) 1061.44/297.18 , 43: mark^#(tt()) -> c_25() 1061.44/297.18 , 44: mark^#(s(X)) -> c_26(mark^#(X)) 1061.44/297.18 , 45: mark^#(0()) -> c_27() 1061.44/297.18 , 46: mark^#(plus(X1, X2)) -> c_28(a__plus^#(mark(X1), mark(X2))) 1061.44/297.18 , 47: mark^#(x(X1, X2)) -> c_29(a__x^#(mark(X1), mark(X2))) 1061.44/297.18 , 48: mark^#(U101(X1, X2, X3)) -> c_30(a__U101^#(mark(X1), X2, X3)) 1061.44/297.18 , 49: mark^#(U102(X1, X2, X3)) -> c_31(a__U102^#(mark(X1), X2, X3)) 1061.44/297.18 , 50: mark^#(isNatKind(X)) -> c_32(a__isNatKind^#(X)) 1061.44/297.18 , 51: mark^#(U103(X1, X2, X3)) -> c_33(a__U103^#(mark(X1), X2, X3)) 1061.44/297.18 , 52: mark^#(isNat(X)) -> c_34(a__isNat^#(X)) 1061.44/297.18 , 53: mark^#(U104(X1, X2, X3)) -> c_35(a__U104^#(mark(X1), X2, X3)) 1061.44/297.18 , 54: mark^#(U11(X1, X2, X3)) -> c_36(a__U11^#(mark(X1), X2, X3)) 1061.44/297.18 , 55: mark^#(U12(X1, X2, X3)) -> c_37(a__U12^#(mark(X1), X2, X3)) 1061.44/297.18 , 56: mark^#(U13(X1, X2, X3)) -> c_38(a__U13^#(mark(X1), X2, X3)) 1061.44/297.18 , 57: mark^#(U14(X1, X2, X3)) -> c_39(a__U14^#(mark(X1), X2, X3)) 1061.44/297.18 , 58: mark^#(U15(X1, X2)) -> c_40(a__U15^#(mark(X1), X2)) 1061.44/297.18 , 59: mark^#(U16(X)) -> c_41(a__U16^#(mark(X))) 1061.44/297.18 , 60: mark^#(U21(X1, X2)) -> c_42(a__U21^#(mark(X1), X2)) 1061.44/297.18 , 61: mark^#(U22(X1, X2)) -> c_43(a__U22^#(mark(X1), X2)) 1061.44/297.18 , 62: mark^#(U23(X)) -> c_44(a__U23^#(mark(X))) 1061.44/297.18 , 63: mark^#(U31(X1, X2, X3)) -> c_45(a__U31^#(mark(X1), X2, X3)) 1061.44/297.18 , 64: mark^#(U32(X1, X2, X3)) -> c_46(a__U32^#(mark(X1), X2, X3)) 1061.44/297.18 , 65: mark^#(U33(X1, X2, X3)) -> c_47(a__U33^#(mark(X1), X2, X3)) 1061.44/297.18 , 66: mark^#(U34(X1, X2, X3)) -> c_48(a__U34^#(mark(X1), X2, X3)) 1061.44/297.18 , 67: mark^#(U35(X1, X2)) -> c_49(a__U35^#(mark(X1), X2)) 1061.44/297.18 , 68: mark^#(U36(X)) -> c_50(a__U36^#(mark(X))) 1061.44/297.18 , 69: mark^#(U41(X1, X2)) -> c_51(a__U41^#(mark(X1), X2)) 1061.44/297.18 , 70: mark^#(U42(X)) -> c_52(a__U42^#(mark(X))) 1061.44/297.18 , 71: mark^#(U51(X)) -> c_53(a__U51^#(mark(X))) 1061.44/297.18 , 72: mark^#(U61(X1, X2)) -> c_54(a__U61^#(mark(X1), X2)) 1061.44/297.18 , 73: mark^#(U62(X)) -> c_55(a__U62^#(mark(X))) 1061.44/297.18 , 74: mark^#(U71(X1, X2)) -> c_56(a__U71^#(mark(X1), X2)) 1061.44/297.18 , 75: mark^#(U72(X1, X2)) -> c_57(a__U72^#(mark(X1), X2)) 1061.44/297.18 , 76: mark^#(U81(X1, X2, X3)) -> c_58(a__U81^#(mark(X1), X2, X3)) 1061.44/297.18 , 77: mark^#(U82(X1, X2, X3)) -> c_59(a__U82^#(mark(X1), X2, X3)) 1061.44/297.18 , 78: mark^#(U83(X1, X2, X3)) -> c_60(a__U83^#(mark(X1), X2, X3)) 1061.44/297.18 , 79: mark^#(U84(X1, X2, X3)) -> c_61(a__U84^#(mark(X1), X2, X3)) 1061.44/297.18 , 80: mark^#(U91(X1, X2)) -> c_62(a__U91^#(mark(X1), X2)) 1061.44/297.18 , 81: mark^#(U92(X)) -> c_63(a__U92^#(mark(X))) 1061.44/297.18 , 82: a__U12^#(X1, X2, X3) -> c_66(X1, X2, X3) 1061.44/297.18 , 83: a__U12^#(tt(), V1, V2) -> 1061.44/297.18 c_67(a__U13^#(a__isNatKind(V2), V1, V2)) 1061.44/297.18 , 84: a__U13^#(X1, X2, X3) -> c_68(X1, X2, X3) 1061.44/297.18 , 85: a__U13^#(tt(), V1, V2) -> 1061.44/297.18 c_69(a__U14^#(a__isNatKind(V2), V1, V2)) 1061.44/297.18 , 86: a__U14^#(X1, X2, X3) -> c_70(X1, X2, X3) 1061.44/297.18 , 87: a__U14^#(tt(), V1, V2) -> c_71(a__U15^#(a__isNat(V1), V2)) 1061.44/297.18 , 88: a__U15^#(X1, X2) -> c_72(X1, X2) 1061.44/297.18 , 89: a__U15^#(tt(), V2) -> c_73(a__U16^#(a__isNat(V2))) 1061.44/297.18 , 90: a__U16^#(X) -> c_74(X) 1061.44/297.18 , 91: a__U16^#(tt()) -> c_75() 1061.44/297.18 , 92: a__U22^#(X1, X2) -> c_78(X1, X2) 1061.44/297.18 , 93: a__U22^#(tt(), V1) -> c_79(a__U23^#(a__isNat(V1))) 1061.44/297.18 , 94: a__U23^#(X) -> c_80(X) 1061.44/297.18 , 95: a__U23^#(tt()) -> c_81() 1061.44/297.18 , 96: a__U32^#(X1, X2, X3) -> c_84(X1, X2, X3) 1061.44/297.18 , 97: a__U32^#(tt(), V1, V2) -> 1061.44/297.18 c_85(a__U33^#(a__isNatKind(V2), V1, V2)) 1061.44/297.18 , 98: a__U33^#(X1, X2, X3) -> c_86(X1, X2, X3) 1061.44/297.18 , 99: a__U33^#(tt(), V1, V2) -> 1061.44/297.18 c_87(a__U34^#(a__isNatKind(V2), V1, V2)) 1061.44/297.18 , 100: a__U34^#(X1, X2, X3) -> c_88(X1, X2, X3) 1061.44/297.18 , 101: a__U34^#(tt(), V1, V2) -> c_89(a__U35^#(a__isNat(V1), V2)) 1061.44/297.18 , 102: a__U35^#(X1, X2) -> c_90(X1, X2) 1061.44/297.18 , 103: a__U35^#(tt(), V2) -> c_91(a__U36^#(a__isNat(V2))) 1061.44/297.18 , 104: a__U36^#(X) -> c_92(X) 1061.44/297.18 , 105: a__U36^#(tt()) -> c_93() 1061.44/297.18 , 106: a__U42^#(X) -> c_96(X) 1061.44/297.18 , 107: a__U42^#(tt()) -> c_97() 1061.44/297.18 , 108: a__U62^#(X) -> c_102(X) 1061.44/297.18 , 109: a__U62^#(tt()) -> c_103() 1061.44/297.18 , 110: a__U72^#(X1, X2) -> c_106(X1, X2) 1061.44/297.18 , 111: a__U72^#(tt(), N) -> c_107(mark^#(N)) 1061.44/297.18 , 112: a__U82^#(X1, X2, X3) -> c_110(X1, X2, X3) 1061.44/297.18 , 113: a__U82^#(tt(), M, N) -> c_111(a__U83^#(a__isNat(N), M, N)) 1061.44/297.18 , 114: a__U83^#(X1, X2, X3) -> c_112(X1, X2, X3) 1061.44/297.18 , 115: a__U83^#(tt(), M, N) -> 1061.44/297.18 c_113(a__U84^#(a__isNatKind(N), M, N)) 1061.44/297.18 , 116: a__U84^#(X1, X2, X3) -> c_114(X1, X2, X3) 1061.44/297.18 , 117: a__U84^#(tt(), M, N) -> c_115(a__plus^#(mark(N), mark(M))) 1061.44/297.18 , 118: a__U92^#(X) -> c_118(X) 1061.44/297.18 , 119: a__U92^#(tt()) -> c_119() } 1061.44/297.18 1061.44/297.18 We are left with following problem, upon which TcT provides the 1061.44/297.18 certificate MAYBE. 1061.44/297.18 1061.44/297.18 Strict DPs: 1061.44/297.18 { a__U101^#(X1, X2, X3) -> c_1(X1, X2, X3) 1061.44/297.18 , a__U101^#(tt(), M, N) -> c_2(a__U102^#(a__isNatKind(M), M, N)) 1061.44/297.18 , a__U102^#(X1, X2, X3) -> c_3(X1, X2, X3) 1061.44/297.18 , a__U102^#(tt(), M, N) -> c_4(a__U103^#(a__isNat(N), M, N)) 1061.44/297.18 , a__U103^#(X1, X2, X3) -> c_10(X1, X2, X3) 1061.44/297.18 , a__U103^#(tt(), M, N) -> c_11(a__U104^#(a__isNatKind(N), M, N)) 1061.44/297.18 , a__isNatKind^#(X) -> c_5(X) 1061.44/297.18 , a__isNatKind^#(s(V1)) -> c_6(a__U51^#(a__isNatKind(V1))) 1061.44/297.18 , a__isNatKind^#(plus(V1, V2)) -> 1061.44/297.18 c_8(a__U41^#(a__isNatKind(V1), V2)) 1061.44/297.18 , a__isNatKind^#(x(V1, V2)) -> c_9(a__U61^#(a__isNatKind(V1), V2)) 1061.44/297.18 , a__U51^#(X) -> c_98(X) 1061.44/297.18 , a__U41^#(X1, X2) -> c_94(X1, X2) 1061.44/297.18 , a__U41^#(tt(), V2) -> c_95(a__U42^#(a__isNatKind(V2))) 1061.44/297.18 , a__U61^#(X1, X2) -> c_100(X1, X2) 1061.44/297.18 , a__U61^#(tt(), V2) -> c_101(a__U62^#(a__isNatKind(V2))) 1061.44/297.18 , a__U104^#(X1, X2, X3) -> c_17(X1, X2, X3) 1061.44/297.18 , a__U104^#(tt(), M, N) -> 1061.44/297.18 c_18(a__plus^#(a__x(mark(N), mark(M)), mark(N))) 1061.44/297.18 , a__isNat^#(X) -> c_12(X) 1061.44/297.18 , a__isNat^#(s(V1)) -> c_13(a__U21^#(a__isNatKind(V1), V1)) 1061.44/297.18 , a__isNat^#(plus(V1, V2)) -> 1061.44/297.18 c_15(a__U11^#(a__isNatKind(V1), V1, V2)) 1061.44/297.18 , a__isNat^#(x(V1, V2)) -> c_16(a__U31^#(a__isNatKind(V1), V1, V2)) 1061.44/297.18 , a__U21^#(X1, X2) -> c_76(X1, X2) 1061.44/297.18 , a__U21^#(tt(), V1) -> c_77(a__U22^#(a__isNatKind(V1), V1)) 1061.44/297.18 , a__U11^#(X1, X2, X3) -> c_64(X1, X2, X3) 1061.44/297.18 , a__U11^#(tt(), V1, V2) -> 1061.44/297.18 c_65(a__U12^#(a__isNatKind(V1), V1, V2)) 1061.44/297.18 , a__U31^#(X1, X2, X3) -> c_82(X1, X2, X3) 1061.44/297.18 , a__U31^#(tt(), V1, V2) -> 1061.44/297.18 c_83(a__U32^#(a__isNatKind(V1), V1, V2)) 1061.44/297.18 , a__plus^#(X1, X2) -> c_19(X1, X2) 1061.44/297.18 , a__plus^#(N, s(M)) -> c_20(a__U81^#(a__isNat(M), M, N)) 1061.44/297.18 , a__plus^#(N, 0()) -> c_21(a__U71^#(a__isNat(N), N)) 1061.44/297.18 , a__U81^#(X1, X2, X3) -> c_108(X1, X2, X3) 1061.44/297.18 , a__U81^#(tt(), M, N) -> c_109(a__U82^#(a__isNatKind(M), M, N)) 1061.44/297.18 , a__U71^#(X1, X2) -> c_104(X1, X2) 1061.44/297.18 , a__U71^#(tt(), N) -> c_105(a__U72^#(a__isNatKind(N), N)) 1061.44/297.18 , a__x^#(X1, X2) -> c_22(X1, X2) 1061.44/297.18 , a__x^#(N, s(M)) -> c_23(a__U101^#(a__isNat(M), M, N)) 1061.44/297.18 , a__x^#(N, 0()) -> c_24(a__U91^#(a__isNat(N), N)) 1061.44/297.18 , a__U91^#(X1, X2) -> c_116(X1, X2) 1061.44/297.18 , a__U91^#(tt(), N) -> c_117(a__U92^#(a__isNatKind(N))) 1061.44/297.18 , mark^#(s(X)) -> c_26(mark^#(X)) 1061.44/297.18 , mark^#(plus(X1, X2)) -> c_28(a__plus^#(mark(X1), mark(X2))) 1061.44/297.18 , mark^#(x(X1, X2)) -> c_29(a__x^#(mark(X1), mark(X2))) 1061.44/297.18 , mark^#(U101(X1, X2, X3)) -> c_30(a__U101^#(mark(X1), X2, X3)) 1061.44/297.18 , mark^#(U102(X1, X2, X3)) -> c_31(a__U102^#(mark(X1), X2, X3)) 1061.44/297.18 , mark^#(isNatKind(X)) -> c_32(a__isNatKind^#(X)) 1061.44/297.18 , mark^#(U103(X1, X2, X3)) -> c_33(a__U103^#(mark(X1), X2, X3)) 1061.44/297.18 , mark^#(isNat(X)) -> c_34(a__isNat^#(X)) 1061.44/297.18 , mark^#(U104(X1, X2, X3)) -> c_35(a__U104^#(mark(X1), X2, X3)) 1061.44/297.18 , mark^#(U11(X1, X2, X3)) -> c_36(a__U11^#(mark(X1), X2, X3)) 1061.44/297.18 , mark^#(U12(X1, X2, X3)) -> c_37(a__U12^#(mark(X1), X2, X3)) 1061.44/297.18 , mark^#(U13(X1, X2, X3)) -> c_38(a__U13^#(mark(X1), X2, X3)) 1061.44/297.18 , mark^#(U14(X1, X2, X3)) -> c_39(a__U14^#(mark(X1), X2, X3)) 1061.44/297.18 , mark^#(U15(X1, X2)) -> c_40(a__U15^#(mark(X1), X2)) 1061.44/297.18 , mark^#(U16(X)) -> c_41(a__U16^#(mark(X))) 1061.44/297.18 , mark^#(U21(X1, X2)) -> c_42(a__U21^#(mark(X1), X2)) 1061.44/297.18 , mark^#(U22(X1, X2)) -> c_43(a__U22^#(mark(X1), X2)) 1061.44/297.18 , mark^#(U23(X)) -> c_44(a__U23^#(mark(X))) 1061.44/297.18 , mark^#(U31(X1, X2, X3)) -> c_45(a__U31^#(mark(X1), X2, X3)) 1061.44/297.18 , mark^#(U32(X1, X2, X3)) -> c_46(a__U32^#(mark(X1), X2, X3)) 1061.44/297.18 , mark^#(U33(X1, X2, X3)) -> c_47(a__U33^#(mark(X1), X2, X3)) 1061.44/297.18 , mark^#(U34(X1, X2, X3)) -> c_48(a__U34^#(mark(X1), X2, X3)) 1061.44/297.18 , mark^#(U35(X1, X2)) -> c_49(a__U35^#(mark(X1), X2)) 1061.44/297.18 , mark^#(U36(X)) -> c_50(a__U36^#(mark(X))) 1061.44/297.18 , mark^#(U41(X1, X2)) -> c_51(a__U41^#(mark(X1), X2)) 1061.44/297.18 , mark^#(U42(X)) -> c_52(a__U42^#(mark(X))) 1061.44/297.18 , mark^#(U51(X)) -> c_53(a__U51^#(mark(X))) 1061.44/297.18 , mark^#(U61(X1, X2)) -> c_54(a__U61^#(mark(X1), X2)) 1061.44/297.18 , mark^#(U62(X)) -> c_55(a__U62^#(mark(X))) 1061.44/297.18 , mark^#(U71(X1, X2)) -> c_56(a__U71^#(mark(X1), X2)) 1061.44/297.18 , mark^#(U72(X1, X2)) -> c_57(a__U72^#(mark(X1), X2)) 1061.44/297.18 , mark^#(U81(X1, X2, X3)) -> c_58(a__U81^#(mark(X1), X2, X3)) 1061.44/297.18 , mark^#(U82(X1, X2, X3)) -> c_59(a__U82^#(mark(X1), X2, X3)) 1061.44/297.18 , mark^#(U83(X1, X2, X3)) -> c_60(a__U83^#(mark(X1), X2, X3)) 1061.44/297.18 , mark^#(U84(X1, X2, X3)) -> c_61(a__U84^#(mark(X1), X2, X3)) 1061.44/297.18 , mark^#(U91(X1, X2)) -> c_62(a__U91^#(mark(X1), X2)) 1061.44/297.18 , mark^#(U92(X)) -> c_63(a__U92^#(mark(X))) 1061.44/297.18 , a__U12^#(X1, X2, X3) -> c_66(X1, X2, X3) 1061.44/297.18 , a__U12^#(tt(), V1, V2) -> 1061.44/297.18 c_67(a__U13^#(a__isNatKind(V2), V1, V2)) 1061.44/297.18 , a__U13^#(X1, X2, X3) -> c_68(X1, X2, X3) 1061.44/297.18 , a__U13^#(tt(), V1, V2) -> 1061.44/297.18 c_69(a__U14^#(a__isNatKind(V2), V1, V2)) 1061.44/297.18 , a__U14^#(X1, X2, X3) -> c_70(X1, X2, X3) 1061.44/297.18 , a__U14^#(tt(), V1, V2) -> c_71(a__U15^#(a__isNat(V1), V2)) 1061.44/297.18 , a__U15^#(X1, X2) -> c_72(X1, X2) 1061.44/297.18 , a__U15^#(tt(), V2) -> c_73(a__U16^#(a__isNat(V2))) 1061.44/297.18 , a__U16^#(X) -> c_74(X) 1061.44/297.18 , a__U22^#(X1, X2) -> c_78(X1, X2) 1061.44/297.18 , a__U22^#(tt(), V1) -> c_79(a__U23^#(a__isNat(V1))) 1061.44/297.18 , a__U23^#(X) -> c_80(X) 1061.44/297.18 , a__U32^#(X1, X2, X3) -> c_84(X1, X2, X3) 1061.44/297.18 , a__U32^#(tt(), V1, V2) -> 1061.44/297.18 c_85(a__U33^#(a__isNatKind(V2), V1, V2)) 1061.44/297.18 , a__U33^#(X1, X2, X3) -> c_86(X1, X2, X3) 1061.44/297.19 , a__U33^#(tt(), V1, V2) -> 1061.44/297.19 c_87(a__U34^#(a__isNatKind(V2), V1, V2)) 1061.44/297.19 , a__U34^#(X1, X2, X3) -> c_88(X1, X2, X3) 1061.44/297.19 , a__U34^#(tt(), V1, V2) -> c_89(a__U35^#(a__isNat(V1), V2)) 1061.44/297.19 , a__U35^#(X1, X2) -> c_90(X1, X2) 1061.44/297.19 , a__U35^#(tt(), V2) -> c_91(a__U36^#(a__isNat(V2))) 1061.44/297.19 , a__U36^#(X) -> c_92(X) 1061.44/297.19 , a__U42^#(X) -> c_96(X) 1061.44/297.19 , a__U62^#(X) -> c_102(X) 1061.44/297.19 , a__U72^#(X1, X2) -> c_106(X1, X2) 1061.44/297.19 , a__U72^#(tt(), N) -> c_107(mark^#(N)) 1061.44/297.19 , a__U82^#(X1, X2, X3) -> c_110(X1, X2, X3) 1061.44/297.19 , a__U82^#(tt(), M, N) -> c_111(a__U83^#(a__isNat(N), M, N)) 1061.44/297.19 , a__U83^#(X1, X2, X3) -> c_112(X1, X2, X3) 1061.44/297.19 , a__U83^#(tt(), M, N) -> c_113(a__U84^#(a__isNatKind(N), M, N)) 1061.44/297.19 , a__U84^#(X1, X2, X3) -> c_114(X1, X2, X3) 1061.44/297.19 , a__U84^#(tt(), M, N) -> c_115(a__plus^#(mark(N), mark(M))) 1061.44/297.19 , a__U92^#(X) -> c_118(X) } 1061.44/297.19 Strict Trs: 1061.44/297.19 { a__U101(X1, X2, X3) -> U101(X1, X2, X3) 1061.44/297.19 , a__U101(tt(), M, N) -> a__U102(a__isNatKind(M), M, N) 1061.44/297.19 , a__U102(X1, X2, X3) -> U102(X1, X2, X3) 1061.44/297.19 , a__U102(tt(), M, N) -> a__U103(a__isNat(N), M, N) 1061.44/297.19 , a__isNatKind(X) -> isNatKind(X) 1061.44/297.19 , a__isNatKind(s(V1)) -> a__U51(a__isNatKind(V1)) 1061.44/297.19 , a__isNatKind(0()) -> tt() 1061.44/297.19 , a__isNatKind(plus(V1, V2)) -> a__U41(a__isNatKind(V1), V2) 1061.44/297.19 , a__isNatKind(x(V1, V2)) -> a__U61(a__isNatKind(V1), V2) 1061.44/297.19 , a__U103(X1, X2, X3) -> U103(X1, X2, X3) 1061.44/297.19 , a__U103(tt(), M, N) -> a__U104(a__isNatKind(N), M, N) 1061.44/297.19 , a__isNat(X) -> isNat(X) 1061.44/297.19 , a__isNat(s(V1)) -> a__U21(a__isNatKind(V1), V1) 1061.44/297.19 , a__isNat(0()) -> tt() 1061.44/297.19 , a__isNat(plus(V1, V2)) -> a__U11(a__isNatKind(V1), V1, V2) 1061.44/297.19 , a__isNat(x(V1, V2)) -> a__U31(a__isNatKind(V1), V1, V2) 1061.44/297.19 , a__U104(X1, X2, X3) -> U104(X1, X2, X3) 1061.44/297.19 , a__U104(tt(), M, N) -> a__plus(a__x(mark(N), mark(M)), mark(N)) 1061.44/297.19 , a__plus(X1, X2) -> plus(X1, X2) 1061.44/297.19 , a__plus(N, s(M)) -> a__U81(a__isNat(M), M, N) 1061.44/297.19 , a__plus(N, 0()) -> a__U71(a__isNat(N), N) 1061.44/297.19 , a__x(X1, X2) -> x(X1, X2) 1061.44/297.19 , a__x(N, s(M)) -> a__U101(a__isNat(M), M, N) 1061.44/297.19 , a__x(N, 0()) -> a__U91(a__isNat(N), N) 1061.44/297.19 , mark(tt()) -> tt() 1061.44/297.19 , mark(s(X)) -> s(mark(X)) 1061.44/297.19 , mark(0()) -> 0() 1061.44/297.19 , mark(plus(X1, X2)) -> a__plus(mark(X1), mark(X2)) 1061.44/297.19 , mark(x(X1, X2)) -> a__x(mark(X1), mark(X2)) 1061.44/297.19 , mark(U101(X1, X2, X3)) -> a__U101(mark(X1), X2, X3) 1061.44/297.19 , mark(U102(X1, X2, X3)) -> a__U102(mark(X1), X2, X3) 1061.44/297.19 , mark(isNatKind(X)) -> a__isNatKind(X) 1061.44/297.19 , mark(U103(X1, X2, X3)) -> a__U103(mark(X1), X2, X3) 1061.44/297.19 , mark(isNat(X)) -> a__isNat(X) 1061.44/297.19 , mark(U104(X1, X2, X3)) -> a__U104(mark(X1), X2, X3) 1061.44/297.19 , mark(U11(X1, X2, X3)) -> a__U11(mark(X1), X2, X3) 1061.44/297.19 , mark(U12(X1, X2, X3)) -> a__U12(mark(X1), X2, X3) 1061.44/297.19 , mark(U13(X1, X2, X3)) -> a__U13(mark(X1), X2, X3) 1061.44/297.19 , mark(U14(X1, X2, X3)) -> a__U14(mark(X1), X2, X3) 1061.44/297.19 , mark(U15(X1, X2)) -> a__U15(mark(X1), X2) 1061.44/297.19 , mark(U16(X)) -> a__U16(mark(X)) 1061.44/297.19 , mark(U21(X1, X2)) -> a__U21(mark(X1), X2) 1061.44/297.19 , mark(U22(X1, X2)) -> a__U22(mark(X1), X2) 1061.44/297.19 , mark(U23(X)) -> a__U23(mark(X)) 1061.44/297.19 , mark(U31(X1, X2, X3)) -> a__U31(mark(X1), X2, X3) 1061.44/297.19 , mark(U32(X1, X2, X3)) -> a__U32(mark(X1), X2, X3) 1061.44/297.19 , mark(U33(X1, X2, X3)) -> a__U33(mark(X1), X2, X3) 1061.44/297.19 , mark(U34(X1, X2, X3)) -> a__U34(mark(X1), X2, X3) 1061.44/297.19 , mark(U35(X1, X2)) -> a__U35(mark(X1), X2) 1061.44/297.19 , mark(U36(X)) -> a__U36(mark(X)) 1061.44/297.19 , mark(U41(X1, X2)) -> a__U41(mark(X1), X2) 1061.44/297.19 , mark(U42(X)) -> a__U42(mark(X)) 1061.44/297.19 , mark(U51(X)) -> a__U51(mark(X)) 1061.44/297.19 , mark(U61(X1, X2)) -> a__U61(mark(X1), X2) 1061.44/297.19 , mark(U62(X)) -> a__U62(mark(X)) 1061.44/297.19 , mark(U71(X1, X2)) -> a__U71(mark(X1), X2) 1061.44/297.19 , mark(U72(X1, X2)) -> a__U72(mark(X1), X2) 1061.44/297.19 , mark(U81(X1, X2, X3)) -> a__U81(mark(X1), X2, X3) 1061.44/297.19 , mark(U82(X1, X2, X3)) -> a__U82(mark(X1), X2, X3) 1061.44/297.19 , mark(U83(X1, X2, X3)) -> a__U83(mark(X1), X2, X3) 1061.44/297.19 , mark(U84(X1, X2, X3)) -> a__U84(mark(X1), X2, X3) 1061.44/297.19 , mark(U91(X1, X2)) -> a__U91(mark(X1), X2) 1061.44/297.19 , mark(U92(X)) -> a__U92(mark(X)) 1061.44/297.19 , a__U11(X1, X2, X3) -> U11(X1, X2, X3) 1061.44/297.19 , a__U11(tt(), V1, V2) -> a__U12(a__isNatKind(V1), V1, V2) 1061.44/297.19 , a__U12(X1, X2, X3) -> U12(X1, X2, X3) 1061.44/297.19 , a__U12(tt(), V1, V2) -> a__U13(a__isNatKind(V2), V1, V2) 1061.44/297.19 , a__U13(X1, X2, X3) -> U13(X1, X2, X3) 1061.44/297.19 , a__U13(tt(), V1, V2) -> a__U14(a__isNatKind(V2), V1, V2) 1061.44/297.19 , a__U14(X1, X2, X3) -> U14(X1, X2, X3) 1061.44/297.19 , a__U14(tt(), V1, V2) -> a__U15(a__isNat(V1), V2) 1061.44/297.19 , a__U15(X1, X2) -> U15(X1, X2) 1061.44/297.19 , a__U15(tt(), V2) -> a__U16(a__isNat(V2)) 1061.44/297.19 , a__U16(X) -> U16(X) 1061.44/297.19 , a__U16(tt()) -> tt() 1061.44/297.19 , a__U21(X1, X2) -> U21(X1, X2) 1061.44/297.19 , a__U21(tt(), V1) -> a__U22(a__isNatKind(V1), V1) 1061.44/297.19 , a__U22(X1, X2) -> U22(X1, X2) 1061.44/297.19 , a__U22(tt(), V1) -> a__U23(a__isNat(V1)) 1061.44/297.19 , a__U23(X) -> U23(X) 1061.44/297.19 , a__U23(tt()) -> tt() 1061.44/297.19 , a__U31(X1, X2, X3) -> U31(X1, X2, X3) 1061.44/297.19 , a__U31(tt(), V1, V2) -> a__U32(a__isNatKind(V1), V1, V2) 1061.44/297.19 , a__U32(X1, X2, X3) -> U32(X1, X2, X3) 1061.44/297.19 , a__U32(tt(), V1, V2) -> a__U33(a__isNatKind(V2), V1, V2) 1061.44/297.19 , a__U33(X1, X2, X3) -> U33(X1, X2, X3) 1061.44/297.19 , a__U33(tt(), V1, V2) -> a__U34(a__isNatKind(V2), V1, V2) 1061.44/297.19 , a__U34(X1, X2, X3) -> U34(X1, X2, X3) 1061.44/297.19 , a__U34(tt(), V1, V2) -> a__U35(a__isNat(V1), V2) 1061.44/297.19 , a__U35(X1, X2) -> U35(X1, X2) 1061.44/297.19 , a__U35(tt(), V2) -> a__U36(a__isNat(V2)) 1061.44/297.19 , a__U36(X) -> U36(X) 1061.44/297.19 , a__U36(tt()) -> tt() 1061.44/297.19 , a__U41(X1, X2) -> U41(X1, X2) 1061.44/297.19 , a__U41(tt(), V2) -> a__U42(a__isNatKind(V2)) 1061.44/297.19 , a__U42(X) -> U42(X) 1061.44/297.19 , a__U42(tt()) -> tt() 1061.44/297.19 , a__U51(X) -> U51(X) 1061.44/297.19 , a__U51(tt()) -> tt() 1061.44/297.19 , a__U61(X1, X2) -> U61(X1, X2) 1061.44/297.19 , a__U61(tt(), V2) -> a__U62(a__isNatKind(V2)) 1061.44/297.19 , a__U62(X) -> U62(X) 1061.44/297.19 , a__U62(tt()) -> tt() 1061.44/297.19 , a__U71(X1, X2) -> U71(X1, X2) 1061.44/297.19 , a__U71(tt(), N) -> a__U72(a__isNatKind(N), N) 1061.44/297.19 , a__U72(X1, X2) -> U72(X1, X2) 1061.44/297.19 , a__U72(tt(), N) -> mark(N) 1061.44/297.19 , a__U81(X1, X2, X3) -> U81(X1, X2, X3) 1061.44/297.19 , a__U81(tt(), M, N) -> a__U82(a__isNatKind(M), M, N) 1061.44/297.19 , a__U82(X1, X2, X3) -> U82(X1, X2, X3) 1061.44/297.19 , a__U82(tt(), M, N) -> a__U83(a__isNat(N), M, N) 1061.44/297.19 , a__U83(X1, X2, X3) -> U83(X1, X2, X3) 1061.44/297.19 , a__U83(tt(), M, N) -> a__U84(a__isNatKind(N), M, N) 1061.44/297.19 , a__U84(X1, X2, X3) -> U84(X1, X2, X3) 1061.44/297.19 , a__U84(tt(), M, N) -> s(a__plus(mark(N), mark(M))) 1061.44/297.19 , a__U91(X1, X2) -> U91(X1, X2) 1061.44/297.19 , a__U91(tt(), N) -> a__U92(a__isNatKind(N)) 1061.44/297.19 , a__U92(X) -> U92(X) 1061.44/297.19 , a__U92(tt()) -> 0() } 1061.44/297.19 Weak DPs: 1061.44/297.19 { a__isNatKind^#(0()) -> c_7() 1061.44/297.19 , a__U51^#(tt()) -> c_99() 1061.44/297.19 , a__isNat^#(0()) -> c_14() 1061.44/297.19 , mark^#(tt()) -> c_25() 1061.44/297.19 , mark^#(0()) -> c_27() 1061.44/297.19 , a__U16^#(tt()) -> c_75() 1061.44/297.19 , a__U23^#(tt()) -> c_81() 1061.44/297.19 , a__U36^#(tt()) -> c_93() 1061.44/297.19 , a__U42^#(tt()) -> c_97() 1061.44/297.19 , a__U62^#(tt()) -> c_103() 1061.44/297.19 , a__U92^#(tt()) -> c_119() } 1061.44/297.19 Obligation: 1061.44/297.19 runtime complexity 1061.44/297.19 Answer: 1061.44/297.19 MAYBE 1061.44/297.19 1061.44/297.19 Empty strict component of the problem is NOT empty. 1061.44/297.19 1061.44/297.19 3) 'Best' failed due to the following reason: 1061.44/297.19 1061.44/297.19 None of the processors succeeded. 1061.44/297.19 1061.44/297.19 Details of failed attempt(s): 1061.44/297.19 ----------------------------- 1061.44/297.19 1) 'With Problem ... (timeout of 148 seconds) (timeout of 297 1061.44/297.19 seconds)' failed due to the following reason: 1061.44/297.19 1061.44/297.19 Computation stopped due to timeout after 148.0 seconds. 1061.44/297.19 1061.44/297.19 2) 'Best' failed due to the following reason: 1061.44/297.19 1061.44/297.19 None of the processors succeeded. 1061.44/297.19 1061.44/297.19 Details of failed attempt(s): 1061.44/297.19 ----------------------------- 1061.44/297.19 1) 'bsearch-popstar (timeout of 297 seconds)' failed due to the 1061.44/297.19 following reason: 1061.44/297.19 1061.44/297.19 The processor is inapplicable, reason: 1061.44/297.19 Processor only applicable for innermost runtime complexity analysis 1061.44/297.19 1061.44/297.19 2) 'Polynomial Path Order (PS) (timeout of 297 seconds)' failed due 1061.44/297.19 to the following reason: 1061.44/297.19 1061.44/297.19 The processor is inapplicable, reason: 1061.44/297.19 Processor only applicable for innermost runtime complexity analysis 1061.44/297.19 1061.44/297.19 1061.44/297.19 3) 'Fastest (timeout of 24 seconds) (timeout of 297 seconds)' 1061.44/297.19 failed due to the following reason: 1061.44/297.19 1061.44/297.19 None of the processors succeeded. 1061.44/297.19 1061.44/297.19 Details of failed attempt(s): 1061.44/297.19 ----------------------------- 1061.44/297.19 1) 'Bounds with perSymbol-enrichment and initial automaton 'match'' 1061.44/297.19 failed due to the following reason: 1061.44/297.19 1061.44/297.19 match-boundness of the problem could not be verified. 1061.44/297.19 1061.44/297.19 2) 'Bounds with minimal-enrichment and initial automaton 'match'' 1061.44/297.19 failed due to the following reason: 1061.44/297.19 1061.44/297.19 match-boundness of the problem could not be verified. 1061.44/297.19 1061.44/297.19 1061.44/297.19 1061.44/297.19 1061.44/297.19 Arrrr.. 1061.70/297.22 EOF