MAYBE
Time: 5.946

Problem:
 Equations:
  
 TRS:
  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) -> dC(N,M)
  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(_>_(N',M'),true()),M',N')
  U125(tt(),M',N') -> gcdC(dC(N',M'),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_(_+_C(N,_+_C(M,_*_C(N,M))))
  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(_>_(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(_>_(N,M'),true()),M',N)
  U385(tt(),M',N) -> s_(quot(dC(N,M'),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_(_+_C(N,M)))
  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) -> _>_(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) -> _>_(N,M)
  U91(tt(),N) -> U92(isNatKind(N),N)
  U92(tt(),N) -> N
  _*_C(N,0()) -> U11(isNat(N),N)
  _*_C(s_(N),s_(M)) -> U21(isNat(M),M,N)
  _+_C(N,0()) -> U31(isNat(N),N)
  _+_C(s_(N),s_(M)) -> U41(isNat(M),M,N)
  _<_(N,M) -> U51(isNat(M),M,N)
  _>_(0(),M) -> U61(isNat(M),M)
  _>_(N',0()) -> U71(isNzNat(N'),N')
  _>_(s_(N),s_(M)) -> U81(isNat(M),M,N)
  dC(0(),N) -> U91(isNat(N),N)
  dC(s_(N),s_(M)) -> U101(isNat(M),M,N)
  equal(X,X) -> tt()
  gcdC(0(),N) -> U111(isNat(N),N)
  gcdC(N',M') -> U121(isNzNat(M'),M',N')
  gcdC(N',N') -> U131(isNzNat(N'),N')
  isBoolean(false()) -> tt()
  isBoolean(true()) -> tt()
  isBoolean(_<_(V1,V2)) -> U141(isNatKind(V1),V1,V2)
  isBoolean(_>_(V1,V2)) -> U151(isNatKind(V1),V1,V2)
  isBooleanKind(false()) -> tt()
  isBooleanKind(true()) -> tt()
  isBooleanKind(_<_(V1,V2)) -> U161(isNatKind(V1),V2)
  isBooleanKind(_>_(V1,V2)) -> U171(isNatKind(V1),V2)
  isNat(0()) -> tt()
  isNat(V) -> U181(isNatKind(V),V)
  isNat(_*_C(V1,V2)) -> U191(isNatKind(V1),V1,V2)
  isNat(_+_C(V1,V2)) -> U201(isNatKind(V1),V1,V2)
  isNat(dC(V1,V2)) -> U211(isNatKind(V1),V1,V2)
  isNat(gcdC(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(_*_C(V1,V2)) -> U251(isNatKind(V1),V2)
  isNatKind(_+_C(V1,V2)) -> U261(isNatKind(V1),V2)
  isNatKind(dC(V1,V2)) -> U271(isNatKind(V1),V2)
  isNatKind(gcdC(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(_*_C(V1,V2)) -> U321(isNatKind(V1),V1,V2)
  isNzNat(gcdC(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)

Proof:
 Open