MAYBE
Time: 3.687

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:
 Open