DONT KNOW
Welcome to CiME version 2.02 - Built on 14/04/2004 13:29:51

- : unit = ()
- : unit = ()
X : variable_set = <variable set>

F : signature = <signature>
R : HTRS = { U101(tt,V1,V2) -> U102(isNaturalKind(V1),V1,V2),
             U102(tt,V1,V2) -> U103(isLNatKind(V2),V1,V2),
             U103(tt,V1,V2) -> U104(isLNatKind(V2),V1,V2),
             U104(tt,V1,V2) -> U105(isNatural(V1),V2),
             U105(tt,V2) -> U106(isLNat(V2)),
             U106(tt) -> tt,
             U11(tt,N,XS) -> U12(isNaturalKind(N),N,XS),
             U111(tt,V2) -> U112(isLNatKind(V2)),
             U112(tt) -> tt,
             U12(tt,N,XS) -> U13(isLNat(XS),N,XS),
             U121(tt,V2) -> U122(isLNatKind(V2)),
             U122(tt) -> tt,
             U13(tt,N,XS) -> U14(isLNatKind(XS),N,XS),
             U131(tt) -> tt,
             U14(tt,N,XS) -> snd(splitAt(N,XS)),
             U141(tt) -> tt,
             U151(tt) -> tt,
             U161(tt) -> tt,
             U171(tt,V2) -> U172(isLNatKind(V2)),
             U172(tt) -> tt,
             U181(tt,V1) -> U182(isLNatKind(V1),V1),
             U182(tt,V1) -> U183(isLNat(V1)),
             U183(tt) -> tt,
             U191(tt,V1) -> U192(isNaturalKind(V1),V1),
             U192(tt,V1) -> U193(isNatural(V1)),
             U193(tt) -> tt,
             U201(tt,V1,V2) -> U202(isNaturalKind(V1),V1,V2),
             U202(tt,V1,V2) -> U203(isLNatKind(V2),V1,V2),
             U203(tt,V1,V2) -> U204(isLNatKind(V2),V1,V2),
             U204(tt,V1,V2) -> U205(isNatural(V1),V2),
             U205(tt,V2) -> U206(isLNat(V2)),
             U206(tt) -> tt,
             U21(tt,X,Y) -> U22(isLNatKind(X),X,Y),
             U211(tt) -> tt,
             U22(tt,X,Y) -> U23(isLNat(Y),X,Y),
             U221(tt) -> tt,
             U23(tt,X,Y) -> U24(isLNatKind(Y),X),
             U231(tt,V2) -> U232(isLNatKind(V2)),
             U232(tt) -> tt,
             U24(tt,X) -> X,
             U241(tt,V1,V2) -> U242(isLNatKind(V1),V1,V2),
             U242(tt,V1,V2) -> U243(isLNatKind(V2),V1,V2),
             U243(tt,V1,V2) -> U244(isLNatKind(V2),V1,V2),
             U244(tt,V1,V2) -> U245(isLNat(V1),V2),
             U245(tt,V2) -> U246(isLNat(V2)),
             U246(tt) -> tt,
             U251(tt,V1,V2) -> U252(isNaturalKind(V1),V1,V2),
             U252(tt,V1,V2) -> U253(isLNatKind(V2),V1,V2),
             U253(tt,V1,V2) -> U254(isLNatKind(V2),V1,V2),
             U254(tt,V1,V2) -> U255(isNatural(V1),V2),
             U255(tt,V2) -> U256(isLNat(V2)),
             U256(tt) -> tt,
             U261(tt,V2) -> U262(isLNatKind(V2)),
             U262(tt) -> tt,
             U271(tt,V2) -> U272(isLNatKind(V2)),
             U272(tt) -> tt,
             U281(tt,N) -> U282(isNaturalKind(N),N),
             U282(tt,N) -> cons(N,natsFrom(s(N))),
             U291(tt,N,XS) -> U292(isNaturalKind(N),N,XS),
             U292(tt,N,XS) -> U293(isLNat(XS),N,XS),
             U293(tt,N,XS) -> U294(isLNatKind(XS),N,XS),
             U294(tt,N,XS) -> head(afterNth(N,XS)),
             U301(tt,X,Y) -> U302(isLNatKind(X),Y),
             U302(tt,Y) -> U303(isLNat(Y),Y),
             U303(tt,Y) -> U304(isLNatKind(Y),Y),
             U304(tt,Y) -> Y,
             U31(tt,N,XS) -> U32(isNaturalKind(N),N,XS),
             U311(tt,XS) -> U312(isLNatKind(XS),XS),
             U312(tt,XS) -> pair(nil,XS),
             U32(tt,N,XS) -> U33(isLNat(XS),N,XS),
             U321(tt,N,X,XS) -> U322(isNaturalKind(N),N,X,XS),
             U322(tt,N,X,XS) -> U323(isNatural(X),N,X,XS),
             U323(tt,N,X,XS) -> U324(isNaturalKind(X),N,X,XS),
             U324(tt,N,X,XS) -> U325(isLNat(XS),N,X,XS),
             U325(tt,N,X,XS) -> U326(isLNatKind(XS),N,X,XS),
             U326(tt,N,X,XS) -> U327(splitAt(N,XS),X),
             U327(pair(YS,ZS),X) -> pair(cons(X,YS),ZS),
             U33(tt,N,XS) -> U34(isLNatKind(XS),N),
             U331(tt,N,XS) -> U332(isNaturalKind(N),XS),
             U332(tt,XS) -> U333(isLNat(XS),XS),
             U333(tt,XS) -> U334(isLNatKind(XS),XS),
             U334(tt,XS) -> XS,
             U34(tt,N) -> N,
             U341(tt,N,XS) -> U342(isNaturalKind(N),N,XS),
             U342(tt,N,XS) -> U343(isLNat(XS),N,XS),
             U343(tt,N,XS) -> U344(isLNatKind(XS),N,XS),
             U344(tt,N,XS) -> fst(splitAt(N,XS)),
             U41(tt,V1,V2) -> U42(isNaturalKind(V1),V1,V2),
             U42(tt,V1,V2) -> U43(isLNatKind(V2),V1,V2),
             U43(tt,V1,V2) -> U44(isLNatKind(V2),V1,V2),
             U44(tt,V1,V2) -> U45(isNatural(V1),V2),
             U45(tt,V2) -> U46(isLNat(V2)),
             U46(tt) -> tt,
             U51(tt,V1,V2) -> U52(isNaturalKind(V1),V1,V2),
             U52(tt,V1,V2) -> U53(isLNatKind(V2),V1,V2),
             U53(tt,V1,V2) -> U54(isLNatKind(V2),V1,V2),
             U54(tt,V1,V2) -> U55(isNatural(V1),V2),
             U55(tt,V2) -> U56(isLNat(V2)),
             U56(tt) -> tt,
             U61(tt,V1) -> U62(isPLNatKind(V1),V1),
             U62(tt,V1) -> U63(isPLNat(V1)),
             U63(tt) -> tt,
             U71(tt,V1) -> U72(isNaturalKind(V1),V1),
             U72(tt,V1) -> U73(isNatural(V1)),
             U73(tt) -> tt,
             U81(tt,V1) -> U82(isPLNatKind(V1),V1),
             U82(tt,V1) -> U83(isPLNat(V1)),
             U83(tt) -> tt,
             U91(tt,V1) -> U92(isLNatKind(V1),V1),
             U92(tt,V1) -> U93(isLNat(V1)),
             U93(tt) -> tt,
             afterNth(N,XS) -> U11(isNatural(N),N,XS),
             fst(pair(X,Y)) -> U21(isLNat(X),X,Y),
             head(cons(N,XS)) -> U31(isNatural(N),N,XS),
             isLNat(nil) -> tt,
             isLNat(afterNth(V1,V2)) -> U41(isNaturalKind(V1),V1,V2),
             isLNat(cons(V1,V2)) -> U51(isNaturalKind(V1),V1,V2),
             isLNat(fst(V1)) -> U61(isPLNatKind(V1),V1),
             isLNat(natsFrom(V1)) -> U71(isNaturalKind(V1),V1),
             isLNat(snd(V1)) -> U81(isPLNatKind(V1),V1),
             isLNat(tail(V1)) -> U91(isLNatKind(V1),V1),
             isLNat(take(V1,V2)) -> U101(isNaturalKind(V1),V1,V2),
             isLNatKind(nil) -> tt,
             isLNatKind(afterNth(V1,V2)) -> U111(isNaturalKind(V1),V2),
             isLNatKind(cons(V1,V2)) -> U121(isNaturalKind(V1),V2),
             isLNatKind(fst(V1)) -> U131(isPLNatKind(V1)),
             isLNatKind(natsFrom(V1)) -> U141(isNaturalKind(V1)),
             isLNatKind(snd(V1)) -> U151(isPLNatKind(V1)),
             isLNatKind(tail(V1)) -> U161(isLNatKind(V1)),
             isLNatKind(take(V1,V2)) -> U171(isNaturalKind(V1),V2),
             isNatural(0) -> tt,
             isNatural(head(V1)) -> U181(isLNatKind(V1),V1),
             isNatural(s(V1)) -> U191(isNaturalKind(V1),V1),
             isNatural(sel(V1,V2)) -> U201(isNaturalKind(V1),V1,V2),
             isNaturalKind(0) -> tt,
             isNaturalKind(head(V1)) -> U211(isLNatKind(V1)),
             isNaturalKind(s(V1)) -> U221(isNaturalKind(V1)),
             isNaturalKind(sel(V1,V2)) -> U231(isNaturalKind(V1),V2),
             isPLNat(pair(V1,V2)) -> U241(isLNatKind(V1),V1,V2),
             isPLNat(splitAt(V1,V2)) -> U251(isNaturalKind(V1),V1,V2),
             isPLNatKind(pair(V1,V2)) -> U261(isLNatKind(V1),V2),
             isPLNatKind(splitAt(V1,V2)) -> U271(isNaturalKind(V1),V2),
             natsFrom(N) -> U281(isNatural(N),N),
             sel(N,XS) -> U291(isNatural(N),N,XS),
             snd(pair(X,Y)) -> U301(isLNat(X),X,Y),
             splitAt(0,XS) -> U311(isLNat(XS),XS),
             splitAt(s(N),cons(X,XS)) -> U321(isNatural(N),N,X,XS),
             tail(cons(N,XS)) -> U331(isNatural(N),N,XS),
             take(N,XS) -> U341(isNatural(N),N,XS) } (149 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:
{ U34(tt,V_0) -> V_0 } (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:
{ U24(tt,V_3) -> V_3 } (1 rules)

The dependency graph is
(0 nodes)
Checking each of the 0 strongly connected components :

Checking module:
{ U334(tt,V_4) -> V_4 } (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:
{}

The dependency graph is
(0 nodes)
Checking each of the 0 strongly connected components :

Checking module:
{ U232(tt) -> tt } (1 rules)

The dependency graph is
(0 nodes)
Checking each of the 0 strongly connected components :

Checking module:
{ U221(tt) -> tt } (1 rules)

The dependency graph is
(0 nodes)
Checking each of the 0 strongly connected components :

Checking module:
{ U211(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:
{ U206(tt) -> tt } (1 rules)

The dependency graph is
(0 nodes)
Checking each of the 0 strongly connected components :

Checking module:
{ U193(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:
{ U93(tt) -> tt } (1 rules)

The dependency graph is
(0 nodes)
Checking each of the 0 strongly connected components :

Checking module:
{ U83(tt) -> tt } (1 rules)

The dependency graph is
(0 nodes)
Checking each of the 0 strongly connected components :

Checking module:
{ U256(tt) -> tt } (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:
{ U327(pair(V_6,V_7),V_3) -> pair(cons(V_3,V_6),V_7) } (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:
{ U312(tt,V_4) -> pair(nil,V_4) } (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:
{ U73(tt) -> tt } (1 rules)

The dependency graph is
(0 nodes)
Checking each of the 0 strongly connected components :

Checking module:
{ U63(tt) -> tt } (1 rules)

The dependency graph is
(0 nodes)
Checking each of the 0 strongly connected components :

Checking module:
{ U56(tt) -> tt } (1 rules)

The dependency graph is
(0 nodes)
Checking each of the 0 strongly connected components :

Checking module:
{ U46(tt) -> tt } (1 rules)

The dependency graph is
(0 nodes)
Checking each of the 0 strongly connected components :

Checking module:
{ U304(tt,V_5) -> V_5 } (1 rules)

The dependency graph is
(0 nodes)
Checking each of the 0 strongly connected components :

Checking module:
{ U106(tt) -> tt } (1 rules)

The dependency graph is
(0 nodes)
Checking each of the 0 strongly connected components :

Checking module:
{ U172(tt) -> tt } (1 rules)

The dependency graph is
(0 nodes)
Checking each of the 0 strongly connected components :

Checking module:
{ U161(tt) -> tt } (1 rules)

The dependency graph is
(0 nodes)
Checking each of the 0 strongly connected components :

Checking module:
{ U151(tt) -> tt } (1 rules)

The dependency graph is
(0 nodes)
Checking each of the 0 strongly connected components :

Checking module:
{ U141(tt) -> tt } (1 rules)

The dependency graph is
(0 nodes)
Checking each of the 0 strongly connected components :

Checking module:
{ U131(tt) -> tt } (1 rules)

The dependency graph is
(0 nodes)
Checking each of the 0 strongly connected components :

Checking module:
{ U122(tt) -> tt } (1 rules)

The dependency graph is
(0 nodes)
Checking each of the 0 strongly connected components :

Checking module:
{ U112(tt) -> tt } (1 rules)

The dependency graph is
(0 nodes)
Checking each of the 0 strongly connected components :

Checking module:
{ sel(V_0,V_4) -> U291(isNatural(V_0),V_0,V_4),
  isNatural(sel(V_1,V_2)) -> U201(isNaturalKind(V_1),V_1,V_2),
  isNatural(s(V_1)) -> U191(isNaturalKind(V_1),V_1),
  isNatural(head(V_1)) -> U181(isLNatKind(V_1),V_1),
  isNatural(0) -> tt,
  U192(tt,V_1) -> U193(isNatural(V_1)),
  U72(tt,V_1) -> U73(isNatural(V_1)),
  take(V_0,V_4) -> U341(isNatural(V_0),V_0,V_4),
  isLNat(take(V_1,V_2)) -> U101(isNaturalKind(V_1),V_1,V_2),
  isLNat(tail(V_1)) -> U91(isLNatKind(V_1),V_1),
  isLNat(snd(V_1)) -> U81(isPLNatKind(V_1),V_1),
  isLNat(natsFrom(V_1)) -> U71(isNaturalKind(V_1),V_1),
  isLNat(fst(V_1)) -> U61(isPLNatKind(V_1),V_1),
  isLNat(cons(V_1,V_2)) -> U51(isNaturalKind(V_1),V_1,V_2),
  isLNat(afterNth(V_1,V_2)) -> U41(isNaturalKind(V_1),V_1,V_2),
  isLNat(nil) -> tt,
  U105(tt,V_2) -> U106(isLNat(V_2)),
  U104(tt,V_1,V_2) -> U105(isNatural(V_1),V_2),
  U182(tt,V_1) -> U183(isLNat(V_1)),
  U205(tt,V_2) -> U206(isLNat(V_2)),
  U204(tt,V_1,V_2) -> U205(isNatural(V_1),V_2),
  U245(tt,V_2) -> U246(isLNat(V_2)),
  U244(tt,V_1,V_2) -> U245(isLNat(V_1),V_2),
  U255(tt,V_2) -> U256(isLNat(V_2)),
  U254(tt,V_1,V_2) -> U255(isNatural(V_1),V_2),
  fst(pair(V_3,V_5)) -> U21(isLNat(V_3),V_3,V_5),
  isLNatKind(nil) -> tt,
  isLNatKind(afterNth(V_1,V_2)) -> U111(isNaturalKind(V_1),V_2),
  isLNatKind(cons(V_1,V_2)) -> U121(isNaturalKind(V_1),V_2),
  isLNatKind(fst(V_1)) -> U131(isPLNatKind(V_1)),
  isLNatKind(natsFrom(V_1)) -> U141(isNaturalKind(V_1)),
  isLNatKind(snd(V_1)) -> U151(isPLNatKind(V_1)),
  isLNatKind(tail(V_1)) -> U161(isLNatKind(V_1)),
  isLNatKind(take(V_1,V_2)) -> U171(isNaturalKind(V_1),V_2),
  U103(tt,V_1,V_2) -> U104(isLNatKind(V_2),V_1,V_2),
  U102(tt,V_1,V_2) -> U103(isLNatKind(V_2),V_1,V_2),
  U111(tt,V_2) -> U112(isLNatKind(V_2)),
  U121(tt,V_2) -> U122(isLNatKind(V_2)),
  U171(tt,V_2) -> U172(isLNatKind(V_2)),
  U181(tt,V_1) -> U182(isLNatKind(V_1),V_1),
  U203(tt,V_1,V_2) -> U204(isLNatKind(V_2),V_1,V_2),
  U202(tt,V_1,V_2) -> U203(isLNatKind(V_2),V_1,V_2),
  U23(tt,V_3,V_5) -> U24(isLNatKind(V_5),V_3),
  U22(tt,V_3,V_5) -> U23(isLNat(V_5),V_3,V_5),
  U21(tt,V_3,V_5) -> U22(isLNatKind(V_3),V_3,V_5),
  U231(tt,V_2) -> U232(isLNatKind(V_2)),
  U243(tt,V_1,V_2) -> U244(isLNatKind(V_2),V_1,V_2),
  U242(tt,V_1,V_2) -> U243(isLNatKind(V_2),V_1,V_2),
  U241(tt,V_1,V_2) -> U242(isLNatKind(V_1),V_1,V_2),
  U253(tt,V_1,V_2) -> U254(isLNatKind(V_2),V_1,V_2),
  U252(tt,V_1,V_2) -> U253(isLNatKind(V_2),V_1,V_2),
  U261(tt,V_2) -> U262(isLNatKind(V_2)),
  U271(tt,V_2) -> U272(isLNatKind(V_2)),
  U303(tt,V_5) -> U304(isLNatKind(V_5),V_5),
  U302(tt,V_5) -> U303(isLNat(V_5),V_5),
  U301(tt,V_3,V_5) -> U302(isLNatKind(V_3),V_5),
  snd(pair(V_3,V_5)) -> U301(isLNat(V_3),V_3,V_5),
  U311(tt,V_4) -> U312(isLNatKind(V_4),V_4),
  U33(tt,V_0,V_4) -> U34(isLNatKind(V_4),V_0),
  U32(tt,V_0,V_4) -> U33(isLNat(V_4),V_0,V_4),
  U31(tt,V_0,V_4) -> U32(isNaturalKind(V_0),V_0,V_4),
  head(cons(V_0,V_4)) -> U31(isNatural(V_0),V_0,V_4),
  isNaturalKind(sel(V_1,V_2)) -> U231(isNaturalKind(V_1),V_2),
  isNaturalKind(s(V_1)) -> U221(isNaturalKind(V_1)),
  isNaturalKind(head(V_1)) -> U211(isLNatKind(V_1)),
  isNaturalKind(0) -> tt,
  U101(tt,V_1,V_2) -> U102(isNaturalKind(V_1),V_1,V_2),
  U191(tt,V_1) -> U192(isNaturalKind(V_1),V_1),
  U201(tt,V_1,V_2) -> U202(isNaturalKind(V_1),V_1,V_2),
  U251(tt,V_1,V_2) -> U252(isNaturalKind(V_1),V_1,V_2),
  U281(tt,V_0) -> U282(isNaturalKind(V_0),V_0),
  natsFrom(V_0) -> U281(isNatural(V_0),V_0),
  U282(tt,V_0) -> cons(V_0,natsFrom(s(V_0))),
  U71(tt,V_1) -> U72(isNaturalKind(V_1),V_1),
  U325(tt,V_0,V_3,V_4) -> U326(isLNatKind(V_4),V_0,V_3,V_4),
  U324(tt,V_0,V_3,V_4) -> U325(isLNat(V_4),V_0,V_3,V_4),
  U323(tt,V_0,V_3,V_4) -> U324(isNaturalKind(V_3),V_0,V_3,V_4),
  U322(tt,V_0,V_3,V_4) -> U323(isNatural(V_3),V_0,V_3,V_4),
  U321(tt,V_0,V_3,V_4) -> U322(isNaturalKind(V_0),V_0,V_3,V_4),
  splitAt(s(V_0),cons(V_3,V_4)) -> U321(isNatural(V_0),V_0,V_3,V_4),
  splitAt(0,V_4) -> U311(isLNat(V_4),V_4),
  U14(tt,V_0,V_4) -> snd(splitAt(V_0,V_4)),
  U13(tt,V_0,V_4) -> U14(isLNatKind(V_4),V_0,V_4),
  U12(tt,V_0,V_4) -> U13(isLNat(V_4),V_0,V_4),
  U11(tt,V_0,V_4) -> U12(isNaturalKind(V_0),V_0,V_4),
  afterNth(V_0,V_4) -> U11(isNatural(V_0),V_0,V_4),
  U294(tt,V_0,V_4) -> head(afterNth(V_0,V_4)),
  U293(tt,V_0,V_4) -> U294(isLNatKind(V_4),V_0,V_4),
  U292(tt,V_0,V_4) -> U293(isLNat(V_4),V_0,V_4),
  U291(tt,V_0,V_4) -> U292(isNaturalKind(V_0),V_0,V_4),
  U326(tt,V_0,V_3,V_4) -> U327(splitAt(V_0,V_4),V_3),
  U333(tt,V_4) -> U334(isLNatKind(V_4),V_4),
  U332(tt,V_4) -> U333(isLNat(V_4),V_4),
  U331(tt,V_0,V_4) -> U332(isNaturalKind(V_0),V_4),
  tail(cons(V_0,V_4)) -> U331(isNatural(V_0),V_0,V_4),
  isPLNatKind(pair(V_1,V_2)) -> U261(isLNatKind(V_1),V_2),
  isPLNatKind(splitAt(V_1,V_2)) -> U271(isNaturalKind(V_1),V_2),
  isPLNat(splitAt(V_1,V_2)) -> U251(isNaturalKind(V_1),V_1,V_2),
  isPLNat(pair(V_1,V_2)) -> U241(isLNatKind(V_1),V_1,V_2),
  U62(tt,V_1) -> U63(isPLNat(V_1)),
  U61(tt,V_1) -> U62(isPLNatKind(V_1),V_1),
  U82(tt,V_1) -> U83(isPLNat(V_1)),
  U81(tt,V_1) -> U82(isPLNatKind(V_1),V_1),
  U344(tt,V_0,V_4) -> fst(splitAt(V_0,V_4)),
  U343(tt,V_0,V_4) -> U344(isLNatKind(V_4),V_0,V_4),
  U342(tt,V_0,V_4) -> U343(isLNat(V_4),V_0,V_4),
  U341(tt,V_0,V_4) -> U342(isNaturalKind(V_0),V_0,V_4),
  U45(tt,V_2) -> U46(isLNat(V_2)),
  U44(tt,V_1,V_2) -> U45(isNatural(V_1),V_2),
  U43(tt,V_1,V_2) -> U44(isLNatKind(V_2),V_1,V_2),
  U42(tt,V_1,V_2) -> U43(isLNatKind(V_2),V_1,V_2),
  U41(tt,V_1,V_2) -> U42(isNaturalKind(V_1),V_1,V_2),
  U55(tt,V_2) -> U56(isLNat(V_2)),
  U54(tt,V_1,V_2) -> U55(isNatural(V_1),V_2),
  U53(tt,V_1,V_2) -> U54(isLNatKind(V_2),V_1,V_2),
  U52(tt,V_1,V_2) -> U53(isLNatKind(V_2),V_1,V_2),
  U51(tt,V_1,V_2) -> U52(isNaturalKind(V_1),V_1,V_2),
  U92(tt,V_1) -> U93(isLNat(V_1)),
  U91(tt,V_1) -> U92(isLNatKind(V_1),V_1) } (119 rules)

The dependency graph is
(1 nodes)
Checking each of the 4 strongly connected components :
Checking component 1
Trying simple graph criterion.
Trying to solve the following constraints:
(152 termination constraints)
Search parameters: linear polynomials, coefficient bound is 2.
Time out 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:
(152 termination constraints)
Search parameters: linear polynomials, coefficient bound is 2.
Time out 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:
(152 termination constraints)
Search parameters: linear polynomials, coefficient bound is 2.
Time out 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:
(152 termination constraints)
Search parameters: linear polynomials, coefficient bound is 2.
Time out 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: