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