DONT KNOW Welcome to CiME version 2.02 - Built on 14/04/2004 13:29:51 - : unit = () - : unit = () X : variable_set = F : signature = R : HTRS = { 1 -> s_(0), 2 -> s_(s_(0)), 3 -> s_(s_(s_(0))), 4 -> s_(s_(s_(s_(0)))), 5 -> s_(s_(s_(s_(s_(0))))), 6 -> s_(s_(s_(s_(s_(s_(0)))))), 7 -> s_(s_(s_(s_(s_(s_(s_(0))))))), U101(tt,M,N) -> U102(isNatKind(M),M,N), U102(tt,M,N) -> U103(isNat(N),M,N), U103(tt,M,N) -> U104(isNatKind(N),M,N), U104(tt,M,N) -> d(M,N), U11(tt,N) -> U12(isNatKind(N)), U111(tt,N) -> U112(isNatKind(N)), U112(tt) -> 0, U12(tt) -> 0, U121(tt,M',N') -> U122(isNatKind(M'),M',N'), U122(tt,M',N') -> U123(isNzNat(N'),M',N'), U123(tt,M',N') -> U124(isNatKind(N'),M',N'), U124(tt,M',N') -> U125(equal(_gt_(N',M'),true),M',N'), U125(tt,M',N') -> gcd(d(M',N'),M'), U131(tt,N') -> U132(isNatKind(N'),N'), U132(tt,N') -> N', U141(tt,V1,V2) -> U142(isNatKind(V1),V1,V2), U142(tt,V1,V2) -> U143(isNatKind(V2),V1,V2), U143(tt,V1,V2) -> U144(isNatKind(V2),V1,V2), U144(tt,V1,V2) -> U145(isNat(V1),V2), U145(tt,V2) -> U146(isNat(V2)), U146(tt) -> tt, U151(tt,V1,V2) -> U152(isNatKind(V1),V1,V2), U152(tt,V1,V2) -> U153(isNatKind(V2),V1,V2), U153(tt,V1,V2) -> U154(isNatKind(V2),V1,V2), U154(tt,V1,V2) -> U155(isNat(V1),V2), U155(tt,V2) -> U156(isNat(V2)), U156(tt) -> tt, U161(tt,V2) -> U162(isNatKind(V2)), U162(tt) -> tt, U171(tt,V2) -> U172(isNatKind(V2)), U172(tt) -> tt, U181(tt,V) -> U182(isNatKind(V),V), U182(tt,V) -> U183(isNzNat(V)), U183(tt) -> tt, U191(tt,V1,V2) -> U192(isNatKind(V1),V1,V2), U192(tt,V1,V2) -> U193(isNatKind(V2),V1,V2), U193(tt,V1,V2) -> U194(isNatKind(V2),V1,V2), U194(tt,V1,V2) -> U195(isNat(V1),V2), U195(tt,V2) -> U196(isNat(V2)), U196(tt) -> tt, U201(tt,V1,V2) -> U202(isNatKind(V1),V1,V2), U202(tt,V1,V2) -> U203(isNatKind(V2),V1,V2), U203(tt,V1,V2) -> U204(isNatKind(V2),V1,V2), U204(tt,V1,V2) -> U205(isNat(V1),V2), U205(tt,V2) -> U206(isNat(V2)), U206(tt) -> tt, U21(tt,M,N) -> U22(isNatKind(M),M,N), U211(tt,V1,V2) -> U212(isNatKind(V1),V1,V2), U212(tt,V1,V2) -> U213(isNatKind(V2),V1,V2), U213(tt,V1,V2) -> U214(isNatKind(V2),V1,V2), U214(tt,V1,V2) -> U215(isNat(V1),V2), U215(tt,V2) -> U216(isNat(V2)), U216(tt) -> tt, U22(tt,M,N) -> U23(isNat(N),M,N), U221(tt,V1,V2) -> U222(isNatKind(V1),V1,V2), U222(tt,V1,V2) -> U223(isNatKind(V2),V1,V2), U223(tt,V1,V2) -> U224(isNatKind(V2),V1,V2), U224(tt,V1,V2) -> U225(isNat(V1),V2), U225(tt,V2) -> U226(isNat(V2)), U226(tt) -> tt, U23(tt,M,N) -> U24(isNatKind(N),M,N), U231(tt,V1) -> U232(isNatKind(V1),V1), U232(tt,V1) -> U233(isNzNat(V1)), U233(tt) -> tt, U24(tt,M,N) -> s_(+(+(*(M,N),M),N)), U241(tt,V1,V2) -> U242(isNatKind(V1),V1,V2), U242(tt,V1,V2) -> U243(isNatKind(V2),V1,V2), U243(tt,V1,V2) -> U244(isNatKind(V2),V1,V2), U244(tt,V1,V2) -> U245(isNat(V1),V2), U245(tt,V2) -> U246(isNzNat(V2)), U246(tt) -> tt, U251(tt,V2) -> U252(isNatKind(V2)), U252(tt) -> tt, U261(tt,V2) -> U262(isNatKind(V2)), U262(tt) -> tt, U271(tt,V2) -> U272(isNatKind(V2)), U272(tt) -> tt, U281(tt,V2) -> U282(isNatKind(V2)), U282(tt) -> tt, U291(tt) -> tt, U301(tt,V2) -> U302(isNatKind(V2)), U302(tt) -> tt, U31(tt,N) -> U32(isNatKind(N),N), U311(tt) -> tt, U32(tt,N) -> N, U321(tt,V1,V2) -> U322(isNatKind(V1),V1,V2), U322(tt,V1,V2) -> U323(isNatKind(V2),V1,V2), U323(tt,V1,V2) -> U324(isNatKind(V2),V1,V2), U324(tt,V1,V2) -> U325(isNzNat(V1),V2), U325(tt,V2) -> U326(isNzNat(V2)), U326(tt) -> tt, U331(tt,V1,V2) -> U332(isNatKind(V1),V1,V2), U332(tt,V1,V2) -> U333(isNatKind(V2),V1,V2), U333(tt,V1,V2) -> U334(isNatKind(V2),V1,V2), U334(tt,V1,V2) -> U335(isNzNat(V1),V2), U335(tt,V2) -> U336(isNzNat(V2)), U336(tt) -> tt, U341(tt,V1) -> U342(isNatKind(V1),V1), U342(tt,V1) -> U343(isNat(V1)), U343(tt) -> tt, U351(tt,N) -> U352(isNatKind(N),N), U352(tt,N) -> N, U361(tt,M') -> U362(isNatKind(M')), U362(tt) -> s_(0), U371(tt,M',N) -> U372(isNatKind(M'),M',N), U372(tt,M',N) -> U373(isNat(N),M',N), U373(tt,M',N) -> U374(isNatKind(N),M',N), U374(tt,M',N) -> U375(equal(_gt_(M',N),true)), U375(tt) -> 0, U381(tt,M',N) -> U382(isNatKind(M'),M',N), U382(tt,M',N) -> U383(isNat(N),M',N), U383(tt,M',N) -> U384(isNatKind(N),M',N), U384(tt,M',N) -> U385(equal(_gt_(N,M'),true),M',N), U385(tt,M',N) -> s_(quot(d(M',N),M')), U41(tt,M,N) -> U42(isNatKind(M),M,N), U42(tt,M,N) -> U43(isNat(N),M,N), U43(tt,M,N) -> U44(isNatKind(N),M,N), U44(tt,M,N) -> s_(s_(+(M,N))), U51(tt,M,N) -> U52(isNatKind(M),M,N), U52(tt,M,N) -> U53(isNat(N),M,N), U53(tt,M,N) -> U54(isNatKind(N),M,N), U54(tt,M,N) -> _gt_(M,N), U61(tt,M) -> U62(isNatKind(M)), U62(tt) -> false, U71(tt,N') -> U72(isNatKind(N')), U72(tt) -> true, U81(tt,M,N) -> U82(isNatKind(M),M,N), U82(tt,M,N) -> U83(isNat(N),M,N), U83(tt,M,N) -> U84(isNatKind(N),M,N), U84(tt,M,N) -> _gt_(N,M), U91(tt,N) -> U92(isNatKind(N),N), U92(tt,N) -> N, *(0,N) -> U11(isNat(N),N), *(s_(M),s_(N)) -> U21(isNat(M),M,N), +(0,N) -> U31(isNat(N),N), +(s_(M),s_(N)) -> U41(isNat(M),M,N), _lt_(N,M) -> U51(isNat(M),M,N), _gt_(0,M) -> U61(isNat(M),M), _gt_(N',0) -> U71(isNzNat(N'),N'), _gt_(s_(N),s_(M)) -> U81(isNat(M),M,N), d(0,N) -> U91(isNat(N),N), d(s_(M),s_(N)) -> U101(isNat(M),M,N), equal(X,X) -> tt, gcd(0,N) -> U111(isNat(N),N), gcd(M',N') -> U121(isNzNat(M'),M',N'), gcd(N',N') -> U131(isNzNat(N'),N'), isBoolean(false) -> tt, isBoolean(true) -> tt, isBoolean(_lt_(V1,V2)) -> U141(isNatKind(V1),V1,V2), isBoolean(_gt_(V1,V2)) -> U151(isNatKind(V1),V1,V2), isBooleanKind(false) -> tt, isBooleanKind(true) -> tt, isBooleanKind(_lt_(V1,V2)) -> U161(isNatKind(V1),V2), isBooleanKind(_gt_(V1,V2)) -> U171(isNatKind(V1),V2), isNat(0) -> tt, isNat(V) -> U181(isNatKind(V),V), isNat(*(V1,V2)) -> U191(isNatKind(V1),V1,V2), isNat(+(V1,V2)) -> U201(isNatKind(V1),V1,V2), isNat(d(V1,V2)) -> U211(isNatKind(V1),V1,V2), isNat(gcd(V1,V2)) -> U221(isNatKind(V1),V1,V2), isNat(p_(V1)) -> U231(isNatKind(V1),V1), isNat(quot(V1,V2)) -> U241(isNatKind(V1),V1,V2), isNatKind(0) -> tt, isNatKind(1) -> tt, isNatKind(2) -> tt, isNatKind(3) -> tt, isNatKind(4) -> tt, isNatKind(5) -> tt, isNatKind(6) -> tt, isNatKind(7) -> tt, isNatKind(*(V1,V2)) -> U251(isNatKind(V1),V2), isNatKind(+(V1,V2)) -> U261(isNatKind(V1),V2), isNatKind(d(V1,V2)) -> U271(isNatKind(V1),V2), isNatKind(gcd(V1,V2)) -> U281(isNatKind(V1),V2), isNatKind(p_(V1)) -> U291(isNatKind(V1)), isNatKind(quot(V1,V2)) -> U301(isNatKind(V1),V2), isNatKind(s_(V1)) -> U311(isNatKind(V1)), isNzNat(1) -> tt, isNzNat(2) -> tt, isNzNat(3) -> tt, isNzNat(4) -> tt, isNzNat(5) -> tt, isNzNat(6) -> tt, isNzNat(7) -> tt, isNzNat(*(V1,V2)) -> U321(isNatKind(V1),V1,V2), isNzNat(gcd(V1,V2)) -> U331(isNatKind(V1),V1,V2), isNzNat(s_(V1)) -> U341(isNatKind(V1),V1), p_(s_(N)) -> U351(isNat(N),N), quot(M',M') -> U361(isNzNat(M'),M'), quot(N,M') -> U371(isNzNat(M'),M',N), quot(N,M') -> U381(isNzNat(M'),M',N) } (198 rules) Termination now uses minimal decomposition - : unit = () Entering the termination expert for modules. Verbose level = 0 Checking module: {} The dependency graph is (0 nodes) Checking each of the 0 strongly connected components : Checking module: { U352(tt,V_3) -> V_3 } (1 rules) The dependency graph is (0 nodes) Checking each of the 0 strongly connected components : Checking module: {} The dependency graph is (0 nodes) Checking each of the 0 strongly connected components : Checking module: { U92(tt,V_3) -> V_3 } (1 rules) The dependency graph is (0 nodes) Checking each of the 0 strongly connected components : Checking module: { U246(tt) -> tt } (1 rules) The dependency graph is (0 nodes) Checking each of the 0 strongly connected components : Checking module: { U343(tt) -> tt } (1 rules) The dependency graph is (0 nodes) Checking each of the 0 strongly connected components : Checking module: { U336(tt) -> tt } (1 rules) The dependency graph is (0 nodes) Checking each of the 0 strongly connected components : Checking module: { U326(tt) -> tt } (1 rules) The dependency graph is (0 nodes) Checking each of the 0 strongly connected components : Checking module: {} The dependency graph is (0 nodes) Checking each of the 0 strongly connected components : Checking module: { 7 -> s_(s_(s_(s_(s_(s_(s_(0))))))) } (1 rules) The dependency graph is (0 nodes) Checking each of the 0 strongly connected components : Checking module: { 6 -> s_(s_(s_(s_(s_(s_(0)))))) } (1 rules) The dependency graph is (0 nodes) Checking each of the 0 strongly connected components : Checking module: { 5 -> s_(s_(s_(s_(s_(0))))) } (1 rules) The dependency graph is (0 nodes) Checking each of the 0 strongly connected components : Checking module: { 4 -> s_(s_(s_(s_(0)))) } (1 rules) The dependency graph is (0 nodes) Checking each of the 0 strongly connected components : Checking module: { 3 -> s_(s_(s_(0))) } (1 rules) The dependency graph is (0 nodes) Checking each of the 0 strongly connected components : Checking module: { 2 -> s_(s_(0)) } (1 rules) The dependency graph is (0 nodes) Checking each of the 0 strongly connected components : Checking module: { 1 -> s_(0) } (1 rules) The dependency graph is (0 nodes) Checking each of the 0 strongly connected components : Checking module: { U32(tt,V_3) -> V_3 } (1 rules) The dependency graph is (0 nodes) Checking each of the 0 strongly connected components : Checking module: { U12(tt) -> 0 } (1 rules) The dependency graph is (0 nodes) Checking each of the 0 strongly connected components : Checking module: { U132(tt,V_2) -> V_2 } (1 rules) The dependency graph is (0 nodes) Checking each of the 0 strongly connected components : Checking module: { equal(V_7,V_7) -> tt } (1 rules) The dependency graph is (0 nodes) Checking each of the 0 strongly connected components : Checking module: {} The dependency graph is (0 nodes) Checking each of the 0 strongly connected components : Checking module: { U72(tt) -> true } (1 rules) The dependency graph is (0 nodes) Checking each of the 0 strongly connected components : Checking module: {} The dependency graph is (0 nodes) Checking each of the 0 strongly connected components : Checking module: { U62(tt) -> false } (1 rules) The dependency graph is (0 nodes) Checking each of the 0 strongly connected components : Checking module: { U112(tt) -> 0 } (1 rules) The dependency graph is (0 nodes) Checking each of the 0 strongly connected components : Checking module: { U233(tt) -> tt } (1 rules) The dependency graph is (0 nodes) Checking each of the 0 strongly connected components : Checking module: { U226(tt) -> tt } (1 rules) The dependency graph is (0 nodes) Checking each of the 0 strongly connected components : Checking module: { U216(tt) -> tt } (1 rules) The dependency graph is (0 nodes) Checking each of the 0 strongly connected components : Checking module: { U206(tt) -> tt } (1 rules) The dependency graph is (0 nodes) Checking each of the 0 strongly connected components : Checking module: { U196(tt) -> tt } (1 rules) The dependency graph is (0 nodes) Checking each of the 0 strongly connected components : Checking module: { U183(tt) -> tt } (1 rules) The dependency graph is (0 nodes) Checking each of the 0 strongly connected components : Checking module: { U375(tt) -> 0 } (1 rules) The dependency graph is (0 nodes) Checking each of the 0 strongly connected components : Checking module: { U362(tt) -> s_(0) } (1 rules) The dependency graph is (0 nodes) Checking each of the 0 strongly connected components : Checking module: { U311(tt) -> tt } (1 rules) The dependency graph is (0 nodes) Checking each of the 0 strongly connected components : Checking module: { U302(tt) -> tt } (1 rules) The dependency graph is (0 nodes) Checking each of the 0 strongly connected components : Checking module: { U291(tt) -> tt } (1 rules) The dependency graph is (0 nodes) Checking each of the 0 strongly connected components : Checking module: { U282(tt) -> tt } (1 rules) The dependency graph is (0 nodes) Checking each of the 0 strongly connected components : Checking module: { U272(tt) -> tt } (1 rules) The dependency graph is (0 nodes) Checking each of the 0 strongly connected components : Checking module: { U262(tt) -> tt } (1 rules) The dependency graph is (0 nodes) Checking each of the 0 strongly connected components : Checking module: { U252(tt) -> tt } (1 rules) The dependency graph is (0 nodes) Checking each of the 0 strongly connected components : Checking module: { p_(s_(V_3)) -> U351(isNat(V_3),V_3), isNat(quot(V_4,V_5)) -> U241(isNatKind(V_4),V_4,V_5), isNat(p_(V_4)) -> U231(isNatKind(V_4),V_4), isNat(gcd(V_4,V_5)) -> U221(isNatKind(V_4),V_4,V_5), isNat(d(V_4,V_5)) -> U211(isNatKind(V_4),V_4,V_5), isNat(+(V_4,V_5)) -> U201(isNatKind(V_4),V_4,V_5), isNat(*(V_4,V_5)) -> U191(isNatKind(V_4),V_4,V_5), isNat(V_6) -> U181(isNatKind(V_6),V_6), isNat(0) -> tt, U195(tt,V_5) -> U196(isNat(V_5)), U194(tt,V_4,V_5) -> U195(isNat(V_4),V_5), U205(tt,V_5) -> U206(isNat(V_5)), U204(tt,V_4,V_5) -> U205(isNat(V_4),V_5), U215(tt,V_5) -> U216(isNat(V_5)), U214(tt,V_4,V_5) -> U215(isNat(V_4),V_5), U225(tt,V_5) -> U226(isNat(V_5)), U224(tt,V_4,V_5) -> U225(isNat(V_4),V_5), U342(tt,V_4) -> U343(isNat(V_4)), U82(tt,V_1,V_3) -> U83(isNat(V_3),V_1,V_3), U81(tt,V_1,V_3) -> U82(isNatKind(V_1),V_1,V_3), _gt_(s_(V_3),s_(V_1)) -> U81(isNat(V_1),V_1,V_3), _gt_(V_2,0) -> U71(isNzNat(V_2),V_2), _gt_(0,V_1) -> U61(isNat(V_1),V_1), U374(tt,V_0,V_3) -> U375(equal(_gt_(V_0,V_3),true)), U384(tt,V_0,V_3) -> U385(equal(_gt_(V_3,V_0),true),V_0,V_3), U383(tt,V_0,V_3) -> U384(isNatKind(V_3),V_0,V_3), U382(tt,V_0,V_3) -> U383(isNat(V_3),V_0,V_3), U381(tt,V_0,V_3) -> U382(isNatKind(V_0),V_0,V_3), quot(V_3,V_0) -> U381(isNzNat(V_0),V_0,V_3), quot(V_3,V_0) -> U371(isNzNat(V_0),V_0,V_3), quot(V_0,V_0) -> U361(isNzNat(V_0),V_0), isNatKind(0) -> tt, isNatKind(1) -> tt, isNatKind(2) -> tt, isNatKind(3) -> tt, isNatKind(4) -> tt, isNatKind(5) -> tt, isNatKind(6) -> tt, isNatKind(7) -> tt, isNatKind(*(V_4,V_5)) -> U251(isNatKind(V_4),V_5), isNatKind(+(V_4,V_5)) -> U261(isNatKind(V_4),V_5), isNatKind(d(V_4,V_5)) -> U271(isNatKind(V_4),V_5), isNatKind(gcd(V_4,V_5)) -> U281(isNatKind(V_4),V_5), isNatKind(p_(V_4)) -> U291(isNatKind(V_4)), isNatKind(quot(V_4,V_5)) -> U301(isNatKind(V_4),V_5), isNatKind(s_(V_4)) -> U311(isNatKind(V_4)), U11(tt,V_3) -> U12(isNatKind(V_3)), U111(tt,V_3) -> U112(isNatKind(V_3)), U131(tt,V_2) -> U132(isNatKind(V_2),V_2), U193(tt,V_4,V_5) -> U194(isNatKind(V_5),V_4,V_5), U192(tt,V_4,V_5) -> U193(isNatKind(V_5),V_4,V_5), U191(tt,V_4,V_5) -> U192(isNatKind(V_4),V_4,V_5), U203(tt,V_4,V_5) -> U204(isNatKind(V_5),V_4,V_5), U202(tt,V_4,V_5) -> U203(isNatKind(V_5),V_4,V_5), U201(tt,V_4,V_5) -> U202(isNatKind(V_4),V_4,V_5), U213(tt,V_4,V_5) -> U214(isNatKind(V_5),V_4,V_5), U212(tt,V_4,V_5) -> U213(isNatKind(V_5),V_4,V_5), U211(tt,V_4,V_5) -> U212(isNatKind(V_4),V_4,V_5), U223(tt,V_4,V_5) -> U224(isNatKind(V_5),V_4,V_5), U222(tt,V_4,V_5) -> U223(isNatKind(V_5),V_4,V_5), U221(tt,V_4,V_5) -> U222(isNatKind(V_4),V_4,V_5), U251(tt,V_5) -> U252(isNatKind(V_5)), U261(tt,V_5) -> U262(isNatKind(V_5)), U271(tt,V_5) -> U272(isNatKind(V_5)), U281(tt,V_5) -> U282(isNatKind(V_5)), U301(tt,V_5) -> U302(isNatKind(V_5)), U31(tt,V_3) -> U32(isNatKind(V_3),V_3), U341(tt,V_4) -> U342(isNatKind(V_4),V_4), U351(tt,V_3) -> U352(isNatKind(V_3),V_3), U361(tt,V_0) -> U362(isNatKind(V_0)), U373(tt,V_0,V_3) -> U374(isNatKind(V_3),V_0,V_3), U372(tt,V_0,V_3) -> U373(isNat(V_3),V_0,V_3), U371(tt,V_0,V_3) -> U372(isNatKind(V_0),V_0,V_3), U43(tt,V_1,V_3) -> U44(isNatKind(V_3),V_1,V_3), U42(tt,V_1,V_3) -> U43(isNat(V_3),V_1,V_3), U41(tt,V_1,V_3) -> U42(isNatKind(V_1),V_1,V_3), +(s_(V_1),s_(V_3)) -> U41(isNat(V_1),V_1,V_3), +(0,V_3) -> U31(isNat(V_3),V_3), U24(tt,V_1,V_3) -> s_(+(+(*(V_1,V_3),V_1),V_3)), U23(tt,V_1,V_3) -> U24(isNatKind(V_3),V_1,V_3), U22(tt,V_1,V_3) -> U23(isNat(V_3),V_1,V_3), U21(tt,V_1,V_3) -> U22(isNatKind(V_1),V_1,V_3), *(0,V_3) -> U11(isNat(V_3),V_3), *(s_(V_1),s_(V_3)) -> U21(isNat(V_1),V_1,V_3), U44(tt,V_1,V_3) -> s_(s_(+(V_1,V_3))), U61(tt,V_1) -> U62(isNatKind(V_1)), U71(tt,V_2) -> U72(isNatKind(V_2)), U91(tt,V_3) -> U92(isNatKind(V_3),V_3), d(s_(V_1),s_(V_3)) -> U101(isNat(V_1),V_1,V_3), d(0,V_3) -> U91(isNat(V_3),V_3), U104(tt,V_1,V_3) -> d(V_1,V_3), U103(tt,V_1,V_3) -> U104(isNatKind(V_3),V_1,V_3), U102(tt,V_1,V_3) -> U103(isNat(V_3),V_1,V_3), U101(tt,V_1,V_3) -> U102(isNatKind(V_1),V_1,V_3), U125(tt,V_0,V_2) -> gcd(d(V_0,V_2),V_0), U124(tt,V_0,V_2) -> U125(equal(_gt_(V_2,V_0),true),V_0,V_2), U123(tt,V_0,V_2) -> U124(isNatKind(V_2),V_0,V_2), U122(tt,V_0,V_2) -> U123(isNzNat(V_2),V_0,V_2), U121(tt,V_0,V_2) -> U122(isNatKind(V_0),V_0,V_2), gcd(V_2,V_2) -> U131(isNzNat(V_2),V_2), gcd(V_0,V_2) -> U121(isNzNat(V_0),V_0,V_2), gcd(0,V_3) -> U111(isNat(V_3),V_3), isNzNat(1) -> tt, isNzNat(2) -> tt, isNzNat(3) -> tt, isNzNat(4) -> tt, isNzNat(5) -> tt, isNzNat(6) -> tt, isNzNat(7) -> tt, isNzNat(*(V_4,V_5)) -> U321(isNatKind(V_4),V_4,V_5), isNzNat(gcd(V_4,V_5)) -> U331(isNatKind(V_4),V_4,V_5), isNzNat(s_(V_4)) -> U341(isNatKind(V_4),V_4), U182(tt,V_6) -> U183(isNzNat(V_6)), U181(tt,V_6) -> U182(isNatKind(V_6),V_6), U232(tt,V_4) -> U233(isNzNat(V_4)), U231(tt,V_4) -> U232(isNatKind(V_4),V_4), U245(tt,V_5) -> U246(isNzNat(V_5)), U244(tt,V_4,V_5) -> U245(isNat(V_4),V_5), U243(tt,V_4,V_5) -> U244(isNatKind(V_5),V_4,V_5), U242(tt,V_4,V_5) -> U243(isNatKind(V_5),V_4,V_5), U241(tt,V_4,V_5) -> U242(isNatKind(V_4),V_4,V_5), U325(tt,V_5) -> U326(isNzNat(V_5)), U324(tt,V_4,V_5) -> U325(isNzNat(V_4),V_5), U323(tt,V_4,V_5) -> U324(isNatKind(V_5),V_4,V_5), U322(tt,V_4,V_5) -> U323(isNatKind(V_5),V_4,V_5), U321(tt,V_4,V_5) -> U322(isNatKind(V_4),V_4,V_5), U335(tt,V_5) -> U336(isNzNat(V_5)), U334(tt,V_4,V_5) -> U335(isNzNat(V_4),V_5), U333(tt,V_4,V_5) -> U334(isNatKind(V_5),V_4,V_5), U332(tt,V_4,V_5) -> U333(isNatKind(V_5),V_4,V_5), U331(tt,V_4,V_5) -> U332(isNatKind(V_4),V_4,V_5), U385(tt,V_0,V_3) -> s_(quot(d(V_0,V_3),V_0)), U84(tt,V_1,V_3) -> _gt_(V_3,V_1), U83(tt,V_1,V_3) -> U84(isNatKind(V_3),V_1,V_3) } (134 rules) The dependency graph is (1 nodes) Checking each of the 8 strongly connected components : Checking component 1 Trying simple graph criterion. Trying to solve the following constraints: (174 termination constraints) Search parameters: linear polynomials, coefficient bound is 2. No solution found for these parameters. Search parameters: simple polynomials, coefficient bound is 3. Time out for these parameters. No solution found for these constraints. Trying strongly connected part criterion. Trying to solve the following constraints: (174 termination constraints) Search parameters: linear polynomials, coefficient bound is 2. No solution found for these parameters. Search parameters: simple polynomials, coefficient bound is 3. Time out for these parameters. No solution found for these constraints. Trying to solve the following constraints: (174 termination constraints) Search parameters: linear polynomials, coefficient bound is 2. No solution found for these parameters. Search parameters: simple polynomials, coefficient bound is 3. Time out for these parameters. No solution found for these constraints. Trying to solve the following constraints: (174 termination constraints) Search parameters: linear polynomials, coefficient bound is 2. No solution found for these parameters. Search parameters: simple polynomials, coefficient bound is 3. Time out for these parameters. No solution found for these constraints. Trying to solve the following constraints: (174 termination constraints) Search parameters: linear polynomials, coefficient bound is 2. No solution found for these parameters. Search parameters: simple polynomials, coefficient bound is 3. Time out for these parameters. No solution found for these constraints. Trying to solve the following constraints: (174 termination constraints) Search parameters: linear polynomials, coefficient bound is 2. No solution found for these parameters. Search parameters: simple polynomials, coefficient bound is 3. Time out for these parameters. No solution found for these constraints. No modular termination proof found. - : unit = () The last proof attempt failed. - : unit = () Quitting. Standard error: