MAYBE
Time: 1.092

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:
 DP Processor:
  Equations#:
   
  DPs:
   +{C,#}(s(N),s(M)) -> +{C,#}(N,M)
   *{C,#}(s(N),s(M)) -> *{C,#}(N,M)
   *{C,#}(s(N),s(M)) -> +{C,#}(M,*C(N,M))
   *{C,#}(s(N),s(M)) -> +{C,#}(N,+C(M,*C(N,M)))
   gt#(NzN,0()) -> is_xNzNat#(NzN)
   gt#(NzN,0()) -> u_4#(is_xNzNat(NzN))
   gt#(s(N),s(M)) -> gt#(N,M)
   lt#(N,M) -> gt#(M,N)
   d{C,#}(s(N),s(M)) -> d{C,#}(N,M)
   quot#(N,NzM) -> is_xNzNat#(NzM)
   quot#(N,NzM) -> u_11#(is_xNzNat(NzM),N,NzM)
   u_11#(True(),N,NzM) -> gt#(N,NzM)
   u_11#(True(),N,NzM) -> u_1#(gt(N,NzM),N,NzM)
   u_1#(True(),N,NzM) -> d{C,#}(N,NzM)
   u_1#(True(),N,NzM) -> quot#(dC(N,NzM),NzM)
   quot#(NzM,NzM) -> is_xNzNat#(NzM)
   quot#(NzM,NzM) -> u_01#(is_xNzNat(NzM))
   quot#(N,NzM) -> u_21#(is_xNzNat(NzM),NzM,N)
   u_21#(True(),NzM,N) -> gt#(NzM,N)
   u_21#(True(),NzM,N) -> u_2#(gt(NzM,N))
   gcd{C,#}(NzM,NzM) -> is_xNzNat#(NzM)
   gcd{C,#}(NzM,NzM) -> u_02#(is_xNzNat(NzM),NzM)
   gcd{C,#}(NzN,NzM) -> is_xNzNat#(NzM)
   gcd{C,#}(NzN,NzM) -> is_xNzNat#(NzN)
   gcd{C,#}(NzN,NzM) -> u_31#(is_xNzNat(NzN),is_xNzNat(NzM),NzN,NzM)
   u_31#(True(),True(),NzN,NzM) -> gt#(NzN,NzM)
   u_31#(True(),True(),NzN,NzM) -> u_3#(gt(NzN,NzM),NzN,NzM)
   u_3#(True(),NzN,NzM) -> d{C,#}(NzN,NzM)
   u_3#(True(),NzN,NzM) -> gcd{C,#}(dC(NzN,NzM),NzM)
  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)
  S:
   
  AC-EDG Processor:
   Equations#:
    
   DPs:
    +{C,#}(s(N),s(M)) -> +{C,#}(N,M)
    *{C,#}(s(N),s(M)) -> *{C,#}(N,M)
    *{C,#}(s(N),s(M)) -> +{C,#}(M,*C(N,M))
    *{C,#}(s(N),s(M)) -> +{C,#}(N,+C(M,*C(N,M)))
    gt#(NzN,0()) -> is_xNzNat#(NzN)
    gt#(NzN,0()) -> u_4#(is_xNzNat(NzN))
    gt#(s(N),s(M)) -> gt#(N,M)
    lt#(N,M) -> gt#(M,N)
    d{C,#}(s(N),s(M)) -> d{C,#}(N,M)
    quot#(N,NzM) -> is_xNzNat#(NzM)
    quot#(N,NzM) -> u_11#(is_xNzNat(NzM),N,NzM)
    u_11#(True(),N,NzM) -> gt#(N,NzM)
    u_11#(True(),N,NzM) -> u_1#(gt(N,NzM),N,NzM)
    u_1#(True(),N,NzM) -> d{C,#}(N,NzM)
    u_1#(True(),N,NzM) -> quot#(dC(N,NzM),NzM)
    quot#(NzM,NzM) -> is_xNzNat#(NzM)
    quot#(NzM,NzM) -> u_01#(is_xNzNat(NzM))
    quot#(N,NzM) -> u_21#(is_xNzNat(NzM),NzM,N)
    u_21#(True(),NzM,N) -> gt#(NzM,N)
    u_21#(True(),NzM,N) -> u_2#(gt(NzM,N))
    gcd{C,#}(NzM,NzM) -> is_xNzNat#(NzM)
    gcd{C,#}(NzM,NzM) -> u_02#(is_xNzNat(NzM),NzM)
    gcd{C,#}(NzN,NzM) -> is_xNzNat#(NzM)
    gcd{C,#}(NzN,NzM) -> is_xNzNat#(NzN)
    gcd{C,#}(NzN,NzM) -> u_31#(is_xNzNat(NzN),is_xNzNat(NzM),NzN,NzM)
    u_31#(True(),True(),NzN,NzM) -> gt#(NzN,NzM)
    u_31#(True(),True(),NzN,NzM) -> u_3#(gt(NzN,NzM),NzN,NzM)
    u_3#(True(),NzN,NzM) -> d{C,#}(NzN,NzM)
    u_3#(True(),NzN,NzM) -> gcd{C,#}(dC(NzN,NzM),NzM)
   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)
   S:
    
   Open