MAYBE
Time: 0.727

Problem:
 Equations:
  
 TRS:
  p(s(N)) -> N
  +C(N,0()) -> N
  +C(s(N),s(M)) -> s(s(+C(N,M)))
  *C(N,0()) -> 0()
  *C(s(N),s(M)) -> s(+C(N,+C(M,*C(N,M))))
  gt(0(),M) -> False()
  gt(NzN,0()) -> u_4(is_xNzNat(NzN))
  u_4(True()) -> True()
  is_xNzNat(0()) -> False()
  is_xNzNat(s(N)) -> True()
  gt(s(N),s(M)) -> gt(N,M)
  lt(N,M) -> gt(M,N)
  dC(0(),N) -> N
  dC(s(N),s(M)) -> dC(N,M)
  quot(N,NzM) -> u_11(is_xNzNat(NzM),N,NzM)
  u_11(True(),N,NzM) -> u_1(gt(N,NzM),N,NzM)
  u_1(True(),N,NzM) -> s(quot(dC(N,NzM),NzM))
  quot(NzM,NzM) -> u_01(is_xNzNat(NzM))
  u_01(True()) -> s(0())
  quot(N,NzM) -> u_21(is_xNzNat(NzM),NzM,N)
  u_21(True(),NzM,N) -> u_2(gt(NzM,N))
  u_2(True()) -> 0()
  gcdC(0(),N) -> 0()
  gcdC(NzM,NzM) -> u_02(is_xNzNat(NzM),NzM)
  u_02(True(),NzM) -> NzM
  gcdC(NzN,NzM) -> u_31(is_xNzNat(NzN),is_xNzNat(NzM),NzN,NzM)
  u_31(True(),True(),NzN,NzM) -> u_3(gt(NzN,NzM),NzN,NzM)
  u_3(True(),NzN,NzM) -> gcdC(dC(NzN,NzM),NzM)

Proof:
 Open