MAYBE
Time: 0.470

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())))))))
  U11(tt(),M,N) -> U12(tt(),M,N)
  U12(tt(),M,N) -> s_(_+_C(N,_+_C(M,_*_C(N,M))))
  U21(tt(),M,N) -> U22(tt(),M,N)
  U22(tt(),M,N) -> s_(s_(_+_C(N,M)))
  U31(tt(),M,N) -> U32(tt(),M,N)
  U32(tt(),M,N) -> _>_(M,N)
  U41(tt(),M,N) -> U42(tt(),M,N)
  U42(tt(),M,N) -> _>_(N,M)
  U51(tt(),M,N) -> U52(tt(),M,N)
  U52(tt(),M,N) -> dC(N,M)
  U61(tt(),M',N') -> U62(tt(),M',N')
  U62(tt(),M',N') -> U63(equal(_>_(N',M'),true()),M',N')
  U63(tt(),M',N') -> gcdC(dC(N',M'),M')
  U71(tt(),M',N) -> U72(tt(),M',N)
  U72(tt(),M',N) -> U73(equal(_>_(M',N),true()))
  U73(tt()) -> 0()
  U81(tt(),M',N) -> U82(tt(),M',N)
  U82(tt(),M',N) -> U83(equal(_>_(N,M'),true()),M',N)
  U83(tt(),M',N) -> s_(quot(dC(N,M'),M'))
  _*_C(N,0()) -> 0()
  _*_C(s_(N),s_(M)) -> U11(tt(),M,N)
  _+_C(N,0()) -> N
  _+_C(s_(N),s_(M)) -> U21(tt(),M,N)
  _<_(N,M) -> U31(tt(),M,N)
  _>_(0(),M) -> false()
  _>_(N',0()) -> true()
  _>_(s_(N),s_(M)) -> U41(tt(),M,N)
  dC(0(),N) -> N
  dC(s_(N),s_(M)) -> U51(tt(),M,N)
  equal(X,X) -> tt()
  gcdC(0(),N) -> 0()
  gcdC(N',M') -> U61(tt(),M',N')
  gcdC(N',N') -> N'
  p_(s_(N)) -> N
  quot(M',M') -> s_(0())
  quot(N,M') -> U71(tt(),M',N)
  quot(N,M') -> U81(tt(),M',N)

Proof:
 DP Processor:
  Equations#:
   
  DPs:
   U11#(tt(),M,N) -> U12#(tt(),M,N)
   U12#(tt(),M,N) -> _*_{C,#}(N,M)
   U12#(tt(),M,N) -> _+_{C,#}(M,_*_C(N,M))
   U12#(tt(),M,N) -> _+_{C,#}(N,_+_C(M,_*_C(N,M)))
   U21#(tt(),M,N) -> U22#(tt(),M,N)
   U22#(tt(),M,N) -> _+_{C,#}(N,M)
   U31#(tt(),M,N) -> U32#(tt(),M,N)
   U32#(tt(),M,N) -> _>_#(M,N)
   U41#(tt(),M,N) -> U42#(tt(),M,N)
   U42#(tt(),M,N) -> _>_#(N,M)
   U51#(tt(),M,N) -> U52#(tt(),M,N)
   U52#(tt(),M,N) -> d{C,#}(N,M)
   U61#(tt(),M',N') -> U62#(tt(),M',N')
   U62#(tt(),M',N') -> _>_#(N',M')
   U62#(tt(),M',N') -> equal#(_>_(N',M'),true())
   U62#(tt(),M',N') -> U63#(equal(_>_(N',M'),true()),M',N')
   U63#(tt(),M',N') -> d{C,#}(N',M')
   U63#(tt(),M',N') -> gcd{C,#}(dC(N',M'),M')
   U71#(tt(),M',N) -> U72#(tt(),M',N)
   U72#(tt(),M',N) -> _>_#(M',N)
   U72#(tt(),M',N) -> equal#(_>_(M',N),true())
   U72#(tt(),M',N) -> U73#(equal(_>_(M',N),true()))
   U81#(tt(),M',N) -> U82#(tt(),M',N)
   U82#(tt(),M',N) -> _>_#(N,M')
   U82#(tt(),M',N) -> equal#(_>_(N,M'),true())
   U82#(tt(),M',N) -> U83#(equal(_>_(N,M'),true()),M',N)
   U83#(tt(),M',N) -> d{C,#}(N,M')
   U83#(tt(),M',N) -> quot#(dC(N,M'),M')
   _*_{C,#}(s_(N),s_(M)) -> U11#(tt(),M,N)
   _+_{C,#}(s_(N),s_(M)) -> U21#(tt(),M,N)
   _<_#(N,M) -> U31#(tt(),M,N)
   _>_#(s_(N),s_(M)) -> U41#(tt(),M,N)
   d{C,#}(s_(N),s_(M)) -> U51#(tt(),M,N)
   gcd{C,#}(N',M') -> U61#(tt(),M',N')
   quot#(N,M') -> U71#(tt(),M',N)
   quot#(N,M') -> U81#(tt(),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())))))))
   U11(tt(),M,N) -> U12(tt(),M,N)
   U12(tt(),M,N) -> s_(_+_C(N,_+_C(M,_*_C(N,M))))
   U21(tt(),M,N) -> U22(tt(),M,N)
   U22(tt(),M,N) -> s_(s_(_+_C(N,M)))
   U31(tt(),M,N) -> U32(tt(),M,N)
   U32(tt(),M,N) -> _>_(M,N)
   U41(tt(),M,N) -> U42(tt(),M,N)
   U42(tt(),M,N) -> _>_(N,M)
   U51(tt(),M,N) -> U52(tt(),M,N)
   U52(tt(),M,N) -> dC(N,M)
   U61(tt(),M',N') -> U62(tt(),M',N')
   U62(tt(),M',N') -> U63(equal(_>_(N',M'),true()),M',N')
   U63(tt(),M',N') -> gcdC(dC(N',M'),M')
   U71(tt(),M',N) -> U72(tt(),M',N)
   U72(tt(),M',N) -> U73(equal(_>_(M',N),true()))
   U73(tt()) -> 0()
   U81(tt(),M',N) -> U82(tt(),M',N)
   U82(tt(),M',N) -> U83(equal(_>_(N,M'),true()),M',N)
   U83(tt(),M',N) -> s_(quot(dC(N,M'),M'))
   _*_C(N,0()) -> 0()
   _*_C(s_(N),s_(M)) -> U11(tt(),M,N)
   _+_C(N,0()) -> N
   _+_C(s_(N),s_(M)) -> U21(tt(),M,N)
   _<_(N,M) -> U31(tt(),M,N)
   _>_(0(),M) -> false()
   _>_(N',0()) -> true()
   _>_(s_(N),s_(M)) -> U41(tt(),M,N)
   dC(0(),N) -> N
   dC(s_(N),s_(M)) -> U51(tt(),M,N)
   equal(X,X) -> tt()
   gcdC(0(),N) -> 0()
   gcdC(N',M') -> U61(tt(),M',N')
   gcdC(N',N') -> N'
   p_(s_(N)) -> N
   quot(M',M') -> s_(0())
   quot(N,M') -> U71(tt(),M',N)
   quot(N,M') -> U81(tt(),M',N)
  S:
   
  AC-EDG Processor:
   Equations#:
    
   DPs:
    U11#(tt(),M,N) -> U12#(tt(),M,N)
    U12#(tt(),M,N) -> _*_{C,#}(N,M)
    U12#(tt(),M,N) -> _+_{C,#}(M,_*_C(N,M))
    U12#(tt(),M,N) -> _+_{C,#}(N,_+_C(M,_*_C(N,M)))
    U21#(tt(),M,N) -> U22#(tt(),M,N)
    U22#(tt(),M,N) -> _+_{C,#}(N,M)
    U31#(tt(),M,N) -> U32#(tt(),M,N)
    U32#(tt(),M,N) -> _>_#(M,N)
    U41#(tt(),M,N) -> U42#(tt(),M,N)
    U42#(tt(),M,N) -> _>_#(N,M)
    U51#(tt(),M,N) -> U52#(tt(),M,N)
    U52#(tt(),M,N) -> d{C,#}(N,M)
    U61#(tt(),M',N') -> U62#(tt(),M',N')
    U62#(tt(),M',N') -> _>_#(N',M')
    U62#(tt(),M',N') -> equal#(_>_(N',M'),true())
    U62#(tt(),M',N') -> U63#(equal(_>_(N',M'),true()),M',N')
    U63#(tt(),M',N') -> d{C,#}(N',M')
    U63#(tt(),M',N') -> gcd{C,#}(dC(N',M'),M')
    U71#(tt(),M',N) -> U72#(tt(),M',N)
    U72#(tt(),M',N) -> _>_#(M',N)
    U72#(tt(),M',N) -> equal#(_>_(M',N),true())
    U72#(tt(),M',N) -> U73#(equal(_>_(M',N),true()))
    U81#(tt(),M',N) -> U82#(tt(),M',N)
    U82#(tt(),M',N) -> _>_#(N,M')
    U82#(tt(),M',N) -> equal#(_>_(N,M'),true())
    U82#(tt(),M',N) -> U83#(equal(_>_(N,M'),true()),M',N)
    U83#(tt(),M',N) -> d{C,#}(N,M')
    U83#(tt(),M',N) -> quot#(dC(N,M'),M')
    _*_{C,#}(s_(N),s_(M)) -> U11#(tt(),M,N)
    _+_{C,#}(s_(N),s_(M)) -> U21#(tt(),M,N)
    _<_#(N,M) -> U31#(tt(),M,N)
    _>_#(s_(N),s_(M)) -> U41#(tt(),M,N)
    d{C,#}(s_(N),s_(M)) -> U51#(tt(),M,N)
    gcd{C,#}(N',M') -> U61#(tt(),M',N')
    quot#(N,M') -> U71#(tt(),M',N)
    quot#(N,M') -> U81#(tt(),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())))))))
    U11(tt(),M,N) -> U12(tt(),M,N)
    U12(tt(),M,N) -> s_(_+_C(N,_+_C(M,_*_C(N,M))))
    U21(tt(),M,N) -> U22(tt(),M,N)
    U22(tt(),M,N) -> s_(s_(_+_C(N,M)))
    U31(tt(),M,N) -> U32(tt(),M,N)
    U32(tt(),M,N) -> _>_(M,N)
    U41(tt(),M,N) -> U42(tt(),M,N)
    U42(tt(),M,N) -> _>_(N,M)
    U51(tt(),M,N) -> U52(tt(),M,N)
    U52(tt(),M,N) -> dC(N,M)
    U61(tt(),M',N') -> U62(tt(),M',N')
    U62(tt(),M',N') -> U63(equal(_>_(N',M'),true()),M',N')
    U63(tt(),M',N') -> gcdC(dC(N',M'),M')
    U71(tt(),M',N) -> U72(tt(),M',N)
    U72(tt(),M',N) -> U73(equal(_>_(M',N),true()))
    U73(tt()) -> 0()
    U81(tt(),M',N) -> U82(tt(),M',N)
    U82(tt(),M',N) -> U83(equal(_>_(N,M'),true()),M',N)
    U83(tt(),M',N) -> s_(quot(dC(N,M'),M'))
    _*_C(N,0()) -> 0()
    _*_C(s_(N),s_(M)) -> U11(tt(),M,N)
    _+_C(N,0()) -> N
    _+_C(s_(N),s_(M)) -> U21(tt(),M,N)
    _<_(N,M) -> U31(tt(),M,N)
    _>_(0(),M) -> false()
    _>_(N',0()) -> true()
    _>_(s_(N),s_(M)) -> U41(tt(),M,N)
    dC(0(),N) -> N
    dC(s_(N),s_(M)) -> U51(tt(),M,N)
    equal(X,X) -> tt()
    gcdC(0(),N) -> 0()
    gcdC(N',M') -> U61(tt(),M',N')
    gcdC(N',N') -> N'
    p_(s_(N)) -> N
    quot(M',M') -> s_(0())
    quot(N,M') -> U71(tt(),M',N)
    quot(N,M') -> U81(tt(),M',N)
   S:
    
   Open