MAYBE
Time: 25.162

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(isNat(N),M,N)
  U102(tt(),M,N) -> dC(N,M)
  U11(tt()) -> 0()
  U111(tt()) -> 0()
  U121(tt(),M',N') -> U122(isNzNat(N'),M',N')
  U122(tt(),M',N') -> U123(equal(_>_(N',M'),true()),M',N')
  U123(tt(),M',N') -> gcdC(dC(N',M'),M')
  U131(tt(),N') -> N'
  U141(tt(),V2) -> U142(isNat(V2))
  U142(tt()) -> tt()
  U151(tt(),V2) -> U152(isNat(V2))
  U152(tt()) -> tt()
  U161(tt()) -> tt()
  U171(tt(),V2) -> U172(isNat(V2))
  U172(tt()) -> tt()
  U181(tt(),V2) -> U182(isNat(V2))
  U182(tt()) -> tt()
  U191(tt(),V2) -> U192(isNat(V2))
  U192(tt()) -> tt()
  U201(tt(),V2) -> U202(isNat(V2))
  U202(tt()) -> tt()
  U21(tt(),M,N) -> U22(isNat(N),M,N)
  U211(tt()) -> tt()
  U22(tt(),M,N) -> s_(_+_C(N,_+_C(M,_*_C(N,M))))
  U221(tt(),V2) -> U222(isNzNat(V2))
  U222(tt()) -> tt()
  U231(tt(),V2) -> U232(isNzNat(V2))
  U232(tt()) -> tt()
  U241(tt(),V2) -> U242(isNzNat(V2))
  U242(tt()) -> tt()
  U251(tt()) -> tt()
  U261(tt(),N) -> N
  U271(tt()) -> s_(0())
  U281(tt(),M',N) -> U282(isNat(N),M',N)
  U282(tt(),M',N) -> U283(equal(_>_(M',N),true()))
  U283(tt()) -> 0()
  U291(tt(),M',N) -> U292(isNat(N),M',N)
  U292(tt(),M',N) -> U293(equal(_>_(N,M'),true()),M',N)
  U293(tt(),M',N) -> s_(quot(dC(N,M'),M'))
  U31(tt(),N) -> N
  U41(tt(),M,N) -> U42(isNat(N),M,N)
  U42(tt(),M,N) -> s_(s_(_+_C(N,M)))
  U51(tt(),M,N) -> U52(isNat(N),M,N)
  U52(tt(),M,N) -> _>_(M,N)
  U61(tt()) -> false()
  U71(tt()) -> true()
  U81(tt(),M,N) -> U82(isNat(N),M,N)
  U82(tt(),M,N) -> _>_(N,M)
  U91(tt(),N) -> N
  _*_C(N,0()) -> U11(isNat(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))
  _>_(N',0()) -> U71(isNzNat(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))
  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(isNat(V1),V2)
  isBoolean(_>_(V1,V2)) -> U151(isNat(V1),V2)
  isNat(0()) -> tt()
  isNat(V) -> U161(isNzNat(V))
  isNat(_*_C(V1,V2)) -> U171(isNat(V1),V2)
  isNat(_+_C(V1,V2)) -> U181(isNat(V1),V2)
  isNat(dC(V1,V2)) -> U191(isNat(V1),V2)
  isNat(gcdC(V1,V2)) -> U201(isNat(V1),V2)
  isNat(p_(V1)) -> U211(isNzNat(V1))
  isNat(quot(V1,V2)) -> U221(isNat(V1),V2)
  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)) -> U231(isNzNat(V1),V2)
  isNzNat(gcdC(V1,V2)) -> U241(isNzNat(V1),V2)
  isNzNat(s_(V1)) -> U251(isNat(V1))
  p_(s_(N)) -> U261(isNat(N),N)
  quot(M',M') -> U271(isNzNat(M'))
  quot(N,M') -> U281(isNzNat(M'),M',N)
  quot(N,M') -> U291(isNzNat(M'),M',N)

Proof:
 DP Processor:
  Equations#:
   
  DPs:
   U101#(tt(),M,N) -> isNat#(N)
   U101#(tt(),M,N) -> U102#(isNat(N),M,N)
   U102#(tt(),M,N) -> d{C,#}(N,M)
   U121#(tt(),M',N') -> isNzNat#(N')
   U121#(tt(),M',N') -> U122#(isNzNat(N'),M',N')
   U122#(tt(),M',N') -> _>_#(N',M')
   U122#(tt(),M',N') -> equal#(_>_(N',M'),true())
   U122#(tt(),M',N') -> U123#(equal(_>_(N',M'),true()),M',N')
   U123#(tt(),M',N') -> d{C,#}(N',M')
   U123#(tt(),M',N') -> gcd{C,#}(dC(N',M'),M')
   U141#(tt(),V2) -> isNat#(V2)
   U141#(tt(),V2) -> U142#(isNat(V2))
   U151#(tt(),V2) -> isNat#(V2)
   U151#(tt(),V2) -> U152#(isNat(V2))
   U171#(tt(),V2) -> isNat#(V2)
   U171#(tt(),V2) -> U172#(isNat(V2))
   U181#(tt(),V2) -> isNat#(V2)
   U181#(tt(),V2) -> U182#(isNat(V2))
   U191#(tt(),V2) -> isNat#(V2)
   U191#(tt(),V2) -> U192#(isNat(V2))
   U201#(tt(),V2) -> isNat#(V2)
   U201#(tt(),V2) -> U202#(isNat(V2))
   U21#(tt(),M,N) -> isNat#(N)
   U21#(tt(),M,N) -> U22#(isNat(N),M,N)
   U22#(tt(),M,N) -> _*_{C,#}(N,M)
   U22#(tt(),M,N) -> _+_{C,#}(M,_*_C(N,M))
   U22#(tt(),M,N) -> _+_{C,#}(N,_+_C(M,_*_C(N,M)))
   U221#(tt(),V2) -> isNzNat#(V2)
   U221#(tt(),V2) -> U222#(isNzNat(V2))
   U231#(tt(),V2) -> isNzNat#(V2)
   U231#(tt(),V2) -> U232#(isNzNat(V2))
   U241#(tt(),V2) -> isNzNat#(V2)
   U241#(tt(),V2) -> U242#(isNzNat(V2))
   U281#(tt(),M',N) -> isNat#(N)
   U281#(tt(),M',N) -> U282#(isNat(N),M',N)
   U282#(tt(),M',N) -> _>_#(M',N)
   U282#(tt(),M',N) -> equal#(_>_(M',N),true())
   U282#(tt(),M',N) -> U283#(equal(_>_(M',N),true()))
   U291#(tt(),M',N) -> isNat#(N)
   U291#(tt(),M',N) -> U292#(isNat(N),M',N)
   U292#(tt(),M',N) -> _>_#(N,M')
   U292#(tt(),M',N) -> equal#(_>_(N,M'),true())
   U292#(tt(),M',N) -> U293#(equal(_>_(N,M'),true()),M',N)
   U293#(tt(),M',N) -> d{C,#}(N,M')
   U293#(tt(),M',N) -> quot#(dC(N,M'),M')
   U41#(tt(),M,N) -> isNat#(N)
   U41#(tt(),M,N) -> U42#(isNat(N),M,N)
   U42#(tt(),M,N) -> _+_{C,#}(N,M)
   U51#(tt(),M,N) -> isNat#(N)
   U51#(tt(),M,N) -> U52#(isNat(N),M,N)
   U52#(tt(),M,N) -> _>_#(M,N)
   U81#(tt(),M,N) -> isNat#(N)
   U81#(tt(),M,N) -> U82#(isNat(N),M,N)
   U82#(tt(),M,N) -> _>_#(N,M)
   _*_{C,#}(N,0()) -> isNat#(N)
   _*_{C,#}(N,0()) -> U11#(isNat(N))
   _*_{C,#}(s_(N),s_(M)) -> isNat#(M)
   _*_{C,#}(s_(N),s_(M)) -> U21#(isNat(M),M,N)
   _+_{C,#}(N,0()) -> isNat#(N)
   _+_{C,#}(N,0()) -> U31#(isNat(N),N)
   _+_{C,#}(s_(N),s_(M)) -> isNat#(M)
   _+_{C,#}(s_(N),s_(M)) -> U41#(isNat(M),M,N)
   _<_#(N,M) -> isNat#(M)
   _<_#(N,M) -> U51#(isNat(M),M,N)
   _>_#(0(),M) -> isNat#(M)
   _>_#(0(),M) -> U61#(isNat(M))
   _>_#(N',0()) -> isNzNat#(N')
   _>_#(N',0()) -> U71#(isNzNat(N'))
   _>_#(s_(N),s_(M)) -> isNat#(M)
   _>_#(s_(N),s_(M)) -> U81#(isNat(M),M,N)
   d{C,#}(0(),N) -> isNat#(N)
   d{C,#}(0(),N) -> U91#(isNat(N),N)
   d{C,#}(s_(N),s_(M)) -> isNat#(M)
   d{C,#}(s_(N),s_(M)) -> U101#(isNat(M),M,N)
   gcd{C,#}(0(),N) -> isNat#(N)
   gcd{C,#}(0(),N) -> U111#(isNat(N))
   gcd{C,#}(N',M') -> isNzNat#(M')
   gcd{C,#}(N',M') -> U121#(isNzNat(M'),M',N')
   gcd{C,#}(N',N') -> isNzNat#(N')
   gcd{C,#}(N',N') -> U131#(isNzNat(N'),N')
   isBoolean#(_<_(V1,V2)) -> isNat#(V1)
   isBoolean#(_<_(V1,V2)) -> U141#(isNat(V1),V2)
   isBoolean#(_>_(V1,V2)) -> isNat#(V1)
   isBoolean#(_>_(V1,V2)) -> U151#(isNat(V1),V2)
   isNat#(V) -> isNzNat#(V)
   isNat#(V) -> U161#(isNzNat(V))
   isNat#(_*_C(V1,V2)) -> isNat#(V1)
   isNat#(_*_C(V1,V2)) -> U171#(isNat(V1),V2)
   isNat#(_+_C(V1,V2)) -> isNat#(V1)
   isNat#(_+_C(V1,V2)) -> U181#(isNat(V1),V2)
   isNat#(dC(V1,V2)) -> isNat#(V1)
   isNat#(dC(V1,V2)) -> U191#(isNat(V1),V2)
   isNat#(gcdC(V1,V2)) -> isNat#(V1)
   isNat#(gcdC(V1,V2)) -> U201#(isNat(V1),V2)
   isNat#(p_(V1)) -> isNzNat#(V1)
   isNat#(p_(V1)) -> U211#(isNzNat(V1))
   isNat#(quot(V1,V2)) -> isNat#(V1)
   isNat#(quot(V1,V2)) -> U221#(isNat(V1),V2)
   isNzNat#(_*_C(V1,V2)) -> isNzNat#(V1)
   isNzNat#(_*_C(V1,V2)) -> U231#(isNzNat(V1),V2)
   isNzNat#(gcdC(V1,V2)) -> isNzNat#(V1)
   isNzNat#(gcdC(V1,V2)) -> U241#(isNzNat(V1),V2)
   isNzNat#(s_(V1)) -> isNat#(V1)
   isNzNat#(s_(V1)) -> U251#(isNat(V1))
   p_#(s_(N)) -> isNat#(N)
   p_#(s_(N)) -> U261#(isNat(N),N)
   quot#(M',M') -> isNzNat#(M')
   quot#(M',M') -> U271#(isNzNat(M'))
   quot#(N,M') -> isNzNat#(M')
   quot#(N,M') -> U281#(isNzNat(M'),M',N)
   quot#(N,M') -> U291#(isNzNat(M'),M',N)
  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(isNat(N),M,N)
   U102(tt(),M,N) -> dC(N,M)
   U11(tt()) -> 0()
   U111(tt()) -> 0()
   U121(tt(),M',N') -> U122(isNzNat(N'),M',N')
   U122(tt(),M',N') -> U123(equal(_>_(N',M'),true()),M',N')
   U123(tt(),M',N') -> gcdC(dC(N',M'),M')
   U131(tt(),N') -> N'
   U141(tt(),V2) -> U142(isNat(V2))
   U142(tt()) -> tt()
   U151(tt(),V2) -> U152(isNat(V2))
   U152(tt()) -> tt()
   U161(tt()) -> tt()
   U171(tt(),V2) -> U172(isNat(V2))
   U172(tt()) -> tt()
   U181(tt(),V2) -> U182(isNat(V2))
   U182(tt()) -> tt()
   U191(tt(),V2) -> U192(isNat(V2))
   U192(tt()) -> tt()
   U201(tt(),V2) -> U202(isNat(V2))
   U202(tt()) -> tt()
   U21(tt(),M,N) -> U22(isNat(N),M,N)
   U211(tt()) -> tt()
   U22(tt(),M,N) -> s_(_+_C(N,_+_C(M,_*_C(N,M))))
   U221(tt(),V2) -> U222(isNzNat(V2))
   U222(tt()) -> tt()
   U231(tt(),V2) -> U232(isNzNat(V2))
   U232(tt()) -> tt()
   U241(tt(),V2) -> U242(isNzNat(V2))
   U242(tt()) -> tt()
   U251(tt()) -> tt()
   U261(tt(),N) -> N
   U271(tt()) -> s_(0())
   U281(tt(),M',N) -> U282(isNat(N),M',N)
   U282(tt(),M',N) -> U283(equal(_>_(M',N),true()))
   U283(tt()) -> 0()
   U291(tt(),M',N) -> U292(isNat(N),M',N)
   U292(tt(),M',N) -> U293(equal(_>_(N,M'),true()),M',N)
   U293(tt(),M',N) -> s_(quot(dC(N,M'),M'))
   U31(tt(),N) -> N
   U41(tt(),M,N) -> U42(isNat(N),M,N)
   U42(tt(),M,N) -> s_(s_(_+_C(N,M)))
   U51(tt(),M,N) -> U52(isNat(N),M,N)
   U52(tt(),M,N) -> _>_(M,N)
   U61(tt()) -> false()
   U71(tt()) -> true()
   U81(tt(),M,N) -> U82(isNat(N),M,N)
   U82(tt(),M,N) -> _>_(N,M)
   U91(tt(),N) -> N
   _*_C(N,0()) -> U11(isNat(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))
   _>_(N',0()) -> U71(isNzNat(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))
   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(isNat(V1),V2)
   isBoolean(_>_(V1,V2)) -> U151(isNat(V1),V2)
   isNat(0()) -> tt()
   isNat(V) -> U161(isNzNat(V))
   isNat(_*_C(V1,V2)) -> U171(isNat(V1),V2)
   isNat(_+_C(V1,V2)) -> U181(isNat(V1),V2)
   isNat(dC(V1,V2)) -> U191(isNat(V1),V2)
   isNat(gcdC(V1,V2)) -> U201(isNat(V1),V2)
   isNat(p_(V1)) -> U211(isNzNat(V1))
   isNat(quot(V1,V2)) -> U221(isNat(V1),V2)
   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)) -> U231(isNzNat(V1),V2)
   isNzNat(gcdC(V1,V2)) -> U241(isNzNat(V1),V2)
   isNzNat(s_(V1)) -> U251(isNat(V1))
   p_(s_(N)) -> U261(isNat(N),N)
   quot(M',M') -> U271(isNzNat(M'))
   quot(N,M') -> U281(isNzNat(M'),M',N)
   quot(N,M') -> U291(isNzNat(M'),M',N)
  S:
   
  AC-EDG Processor:
   Equations#:
    
   DPs:
    U101#(tt(),M,N) -> isNat#(N)
    U101#(tt(),M,N) -> U102#(isNat(N),M,N)
    U102#(tt(),M,N) -> d{C,#}(N,M)
    U121#(tt(),M',N') -> isNzNat#(N')
    U121#(tt(),M',N') -> U122#(isNzNat(N'),M',N')
    U122#(tt(),M',N') -> _>_#(N',M')
    U122#(tt(),M',N') -> equal#(_>_(N',M'),true())
    U122#(tt(),M',N') -> U123#(equal(_>_(N',M'),true()),M',N')
    U123#(tt(),M',N') -> d{C,#}(N',M')
    U123#(tt(),M',N') -> gcd{C,#}(dC(N',M'),M')
    U141#(tt(),V2) -> isNat#(V2)
    U141#(tt(),V2) -> U142#(isNat(V2))
    U151#(tt(),V2) -> isNat#(V2)
    U151#(tt(),V2) -> U152#(isNat(V2))
    U171#(tt(),V2) -> isNat#(V2)
    U171#(tt(),V2) -> U172#(isNat(V2))
    U181#(tt(),V2) -> isNat#(V2)
    U181#(tt(),V2) -> U182#(isNat(V2))
    U191#(tt(),V2) -> isNat#(V2)
    U191#(tt(),V2) -> U192#(isNat(V2))
    U201#(tt(),V2) -> isNat#(V2)
    U201#(tt(),V2) -> U202#(isNat(V2))
    U21#(tt(),M,N) -> isNat#(N)
    U21#(tt(),M,N) -> U22#(isNat(N),M,N)
    U22#(tt(),M,N) -> _*_{C,#}(N,M)
    U22#(tt(),M,N) -> _+_{C,#}(M,_*_C(N,M))
    U22#(tt(),M,N) -> _+_{C,#}(N,_+_C(M,_*_C(N,M)))
    U221#(tt(),V2) -> isNzNat#(V2)
    U221#(tt(),V2) -> U222#(isNzNat(V2))
    U231#(tt(),V2) -> isNzNat#(V2)
    U231#(tt(),V2) -> U232#(isNzNat(V2))
    U241#(tt(),V2) -> isNzNat#(V2)
    U241#(tt(),V2) -> U242#(isNzNat(V2))
    U281#(tt(),M',N) -> isNat#(N)
    U281#(tt(),M',N) -> U282#(isNat(N),M',N)
    U282#(tt(),M',N) -> _>_#(M',N)
    U282#(tt(),M',N) -> equal#(_>_(M',N),true())
    U282#(tt(),M',N) -> U283#(equal(_>_(M',N),true()))
    U291#(tt(),M',N) -> isNat#(N)
    U291#(tt(),M',N) -> U292#(isNat(N),M',N)
    U292#(tt(),M',N) -> _>_#(N,M')
    U292#(tt(),M',N) -> equal#(_>_(N,M'),true())
    U292#(tt(),M',N) -> U293#(equal(_>_(N,M'),true()),M',N)
    U293#(tt(),M',N) -> d{C,#}(N,M')
    U293#(tt(),M',N) -> quot#(dC(N,M'),M')
    U41#(tt(),M,N) -> isNat#(N)
    U41#(tt(),M,N) -> U42#(isNat(N),M,N)
    U42#(tt(),M,N) -> _+_{C,#}(N,M)
    U51#(tt(),M,N) -> isNat#(N)
    U51#(tt(),M,N) -> U52#(isNat(N),M,N)
    U52#(tt(),M,N) -> _>_#(M,N)
    U81#(tt(),M,N) -> isNat#(N)
    U81#(tt(),M,N) -> U82#(isNat(N),M,N)
    U82#(tt(),M,N) -> _>_#(N,M)
    _*_{C,#}(N,0()) -> isNat#(N)
    _*_{C,#}(N,0()) -> U11#(isNat(N))
    _*_{C,#}(s_(N),s_(M)) -> isNat#(M)
    _*_{C,#}(s_(N),s_(M)) -> U21#(isNat(M),M,N)
    _+_{C,#}(N,0()) -> isNat#(N)
    _+_{C,#}(N,0()) -> U31#(isNat(N),N)
    _+_{C,#}(s_(N),s_(M)) -> isNat#(M)
    _+_{C,#}(s_(N),s_(M)) -> U41#(isNat(M),M,N)
    _<_#(N,M) -> isNat#(M)
    _<_#(N,M) -> U51#(isNat(M),M,N)
    _>_#(0(),M) -> isNat#(M)
    _>_#(0(),M) -> U61#(isNat(M))
    _>_#(N',0()) -> isNzNat#(N')
    _>_#(N',0()) -> U71#(isNzNat(N'))
    _>_#(s_(N),s_(M)) -> isNat#(M)
    _>_#(s_(N),s_(M)) -> U81#(isNat(M),M,N)
    d{C,#}(0(),N) -> isNat#(N)
    d{C,#}(0(),N) -> U91#(isNat(N),N)
    d{C,#}(s_(N),s_(M)) -> isNat#(M)
    d{C,#}(s_(N),s_(M)) -> U101#(isNat(M),M,N)
    gcd{C,#}(0(),N) -> isNat#(N)
    gcd{C,#}(0(),N) -> U111#(isNat(N))
    gcd{C,#}(N',M') -> isNzNat#(M')
    gcd{C,#}(N',M') -> U121#(isNzNat(M'),M',N')
    gcd{C,#}(N',N') -> isNzNat#(N')
    gcd{C,#}(N',N') -> U131#(isNzNat(N'),N')
    isBoolean#(_<_(V1,V2)) -> isNat#(V1)
    isBoolean#(_<_(V1,V2)) -> U141#(isNat(V1),V2)
    isBoolean#(_>_(V1,V2)) -> isNat#(V1)
    isBoolean#(_>_(V1,V2)) -> U151#(isNat(V1),V2)
    isNat#(V) -> isNzNat#(V)
    isNat#(V) -> U161#(isNzNat(V))
    isNat#(_*_C(V1,V2)) -> isNat#(V1)
    isNat#(_*_C(V1,V2)) -> U171#(isNat(V1),V2)
    isNat#(_+_C(V1,V2)) -> isNat#(V1)
    isNat#(_+_C(V1,V2)) -> U181#(isNat(V1),V2)
    isNat#(dC(V1,V2)) -> isNat#(V1)
    isNat#(dC(V1,V2)) -> U191#(isNat(V1),V2)
    isNat#(gcdC(V1,V2)) -> isNat#(V1)
    isNat#(gcdC(V1,V2)) -> U201#(isNat(V1),V2)
    isNat#(p_(V1)) -> isNzNat#(V1)
    isNat#(p_(V1)) -> U211#(isNzNat(V1))
    isNat#(quot(V1,V2)) -> isNat#(V1)
    isNat#(quot(V1,V2)) -> U221#(isNat(V1),V2)
    isNzNat#(_*_C(V1,V2)) -> isNzNat#(V1)
    isNzNat#(_*_C(V1,V2)) -> U231#(isNzNat(V1),V2)
    isNzNat#(gcdC(V1,V2)) -> isNzNat#(V1)
    isNzNat#(gcdC(V1,V2)) -> U241#(isNzNat(V1),V2)
    isNzNat#(s_(V1)) -> isNat#(V1)
    isNzNat#(s_(V1)) -> U251#(isNat(V1))
    p_#(s_(N)) -> isNat#(N)
    p_#(s_(N)) -> U261#(isNat(N),N)
    quot#(M',M') -> isNzNat#(M')
    quot#(M',M') -> U271#(isNzNat(M'))
    quot#(N,M') -> isNzNat#(M')
    quot#(N,M') -> U281#(isNzNat(M'),M',N)
    quot#(N,M') -> U291#(isNzNat(M'),M',N)
   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(isNat(N),M,N)
    U102(tt(),M,N) -> dC(N,M)
    U11(tt()) -> 0()
    U111(tt()) -> 0()
    U121(tt(),M',N') -> U122(isNzNat(N'),M',N')
    U122(tt(),M',N') -> U123(equal(_>_(N',M'),true()),M',N')
    U123(tt(),M',N') -> gcdC(dC(N',M'),M')
    U131(tt(),N') -> N'
    U141(tt(),V2) -> U142(isNat(V2))
    U142(tt()) -> tt()
    U151(tt(),V2) -> U152(isNat(V2))
    U152(tt()) -> tt()
    U161(tt()) -> tt()
    U171(tt(),V2) -> U172(isNat(V2))
    U172(tt()) -> tt()
    U181(tt(),V2) -> U182(isNat(V2))
    U182(tt()) -> tt()
    U191(tt(),V2) -> U192(isNat(V2))
    U192(tt()) -> tt()
    U201(tt(),V2) -> U202(isNat(V2))
    U202(tt()) -> tt()
    U21(tt(),M,N) -> U22(isNat(N),M,N)
    U211(tt()) -> tt()
    U22(tt(),M,N) -> s_(_+_C(N,_+_C(M,_*_C(N,M))))
    U221(tt(),V2) -> U222(isNzNat(V2))
    U222(tt()) -> tt()
    U231(tt(),V2) -> U232(isNzNat(V2))
    U232(tt()) -> tt()
    U241(tt(),V2) -> U242(isNzNat(V2))
    U242(tt()) -> tt()
    U251(tt()) -> tt()
    U261(tt(),N) -> N
    U271(tt()) -> s_(0())
    U281(tt(),M',N) -> U282(isNat(N),M',N)
    U282(tt(),M',N) -> U283(equal(_>_(M',N),true()))
    U283(tt()) -> 0()
    U291(tt(),M',N) -> U292(isNat(N),M',N)
    U292(tt(),M',N) -> U293(equal(_>_(N,M'),true()),M',N)
    U293(tt(),M',N) -> s_(quot(dC(N,M'),M'))
    U31(tt(),N) -> N
    U41(tt(),M,N) -> U42(isNat(N),M,N)
    U42(tt(),M,N) -> s_(s_(_+_C(N,M)))
    U51(tt(),M,N) -> U52(isNat(N),M,N)
    U52(tt(),M,N) -> _>_(M,N)
    U61(tt()) -> false()
    U71(tt()) -> true()
    U81(tt(),M,N) -> U82(isNat(N),M,N)
    U82(tt(),M,N) -> _>_(N,M)
    U91(tt(),N) -> N
    _*_C(N,0()) -> U11(isNat(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))
    _>_(N',0()) -> U71(isNzNat(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))
    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(isNat(V1),V2)
    isBoolean(_>_(V1,V2)) -> U151(isNat(V1),V2)
    isNat(0()) -> tt()
    isNat(V) -> U161(isNzNat(V))
    isNat(_*_C(V1,V2)) -> U171(isNat(V1),V2)
    isNat(_+_C(V1,V2)) -> U181(isNat(V1),V2)
    isNat(dC(V1,V2)) -> U191(isNat(V1),V2)
    isNat(gcdC(V1,V2)) -> U201(isNat(V1),V2)
    isNat(p_(V1)) -> U211(isNzNat(V1))
    isNat(quot(V1,V2)) -> U221(isNat(V1),V2)
    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)) -> U231(isNzNat(V1),V2)
    isNzNat(gcdC(V1,V2)) -> U241(isNzNat(V1),V2)
    isNzNat(s_(V1)) -> U251(isNat(V1))
    p_(s_(N)) -> U261(isNat(N),N)
    quot(M',M') -> U271(isNzNat(M'))
    quot(N,M') -> U281(isNzNat(M'),M',N)
    quot(N,M') -> U291(isNzNat(M'),M',N)
   S:
    
   Open