MAYBE

Problem:
 p(s(N)) -> N
 +(N,0()) -> N
 +(s(N),s(M)) -> s(s(+(N,M)))
 *(N,0()) -> 0()
 *(s(N),s(M)) -> s(+(N,+(M,*(N,M))))
 gt(0(),M) -> False()
 gt(NzN,0()) -> u_4(is_NzNat(NzN))
 u_4(True()) -> True()
 is_NzNat(0()) -> False()
 is_NzNat(s(N)) -> True()
 gt(s(N),s(M)) -> gt(N,M)
 lt(N,M) -> gt(M,N)
 d(0(),N) -> N
 d(s(N),s(M)) -> d(N,M)
 quot(N,NzM) -> u_11(is_NzNat(NzM),N,NzM)
 u_11(True(),N,NzM) -> u_1(gt(N,NzM),N,NzM)
 u_1(True(),N,NzM) -> s(quot(d(N,NzM),NzM))
 quot(NzM,NzM) -> u_01(is_NzNat(NzM))
 u_01(True()) -> s(0())
 quot(N,NzM) -> u_21(is_NzNat(NzM),NzM,N)
 u_21(True(),NzM,N) -> u_2(gt(NzM,N))
 u_2(True()) -> 0()
 gcd(0(),N) -> 0()
 gcd(NzM,NzM) -> u_02(is_NzNat(NzM),NzM)
 u_02(True(),NzM) -> NzM
 gcd(NzN,NzM) -> u_31(is_NzNat(NzN),is_NzNat(NzM),NzN,NzM)
 u_31(True(),True(),NzN,NzM) -> u_3(gt(NzN,NzM),NzN,NzM)
 u_3(True(),NzN,NzM) -> gcd(d(NzN,NzM),NzM)

Proof:
 DP Processor:
  DPs:
   +#(s(N),s(M)) -> +#(N,M)
   *#(s(N),s(M)) -> *#(N,M)
   *#(s(N),s(M)) -> +#(M,*(N,M))
   *#(s(N),s(M)) -> +#(N,+(M,*(N,M)))
   gt#(NzN,0()) -> is_NzNat#(NzN)
   gt#(NzN,0()) -> u_4#(is_NzNat(NzN))
   gt#(s(N),s(M)) -> gt#(N,M)
   lt#(N,M) -> gt#(M,N)
   d#(s(N),s(M)) -> d#(N,M)
   quot#(N,NzM) -> is_NzNat#(NzM)
   quot#(N,NzM) -> u_11#(is_NzNat(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#(N,NzM)
   u_1#(True(),N,NzM) -> quot#(d(N,NzM),NzM)
   quot#(NzM,NzM) -> is_NzNat#(NzM)
   quot#(NzM,NzM) -> u_01#(is_NzNat(NzM))
   quot#(N,NzM) -> u_21#(is_NzNat(NzM),NzM,N)
   u_21#(True(),NzM,N) -> gt#(NzM,N)
   u_21#(True(),NzM,N) -> u_2#(gt(NzM,N))
   gcd#(NzM,NzM) -> is_NzNat#(NzM)
   gcd#(NzM,NzM) -> u_02#(is_NzNat(NzM),NzM)
   gcd#(NzN,NzM) -> is_NzNat#(NzM)
   gcd#(NzN,NzM) -> is_NzNat#(NzN)
   gcd#(NzN,NzM) -> u_31#(is_NzNat(NzN),is_NzNat(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#(NzN,NzM)
   u_3#(True(),NzN,NzM) -> gcd#(d(NzN,NzM),NzM)
  TRS:
   p(s(N)) -> N
   +(N,0()) -> N
   +(s(N),s(M)) -> s(s(+(N,M)))
   *(N,0()) -> 0()
   *(s(N),s(M)) -> s(+(N,+(M,*(N,M))))
   gt(0(),M) -> False()
   gt(NzN,0()) -> u_4(is_NzNat(NzN))
   u_4(True()) -> True()
   is_NzNat(0()) -> False()
   is_NzNat(s(N)) -> True()
   gt(s(N),s(M)) -> gt(N,M)
   lt(N,M) -> gt(M,N)
   d(0(),N) -> N
   d(s(N),s(M)) -> d(N,M)
   quot(N,NzM) -> u_11(is_NzNat(NzM),N,NzM)
   u_11(True(),N,NzM) -> u_1(gt(N,NzM),N,NzM)
   u_1(True(),N,NzM) -> s(quot(d(N,NzM),NzM))
   quot(NzM,NzM) -> u_01(is_NzNat(NzM))
   u_01(True()) -> s(0())
   quot(N,NzM) -> u_21(is_NzNat(NzM),NzM,N)
   u_21(True(),NzM,N) -> u_2(gt(NzM,N))
   u_2(True()) -> 0()
   gcd(0(),N) -> 0()
   gcd(NzM,NzM) -> u_02(is_NzNat(NzM),NzM)
   u_02(True(),NzM) -> NzM
   gcd(NzN,NzM) -> u_31(is_NzNat(NzN),is_NzNat(NzM),NzN,NzM)
   u_31(True(),True(),NzN,NzM) -> u_3(gt(NzN,NzM),NzN,NzM)
   u_3(True(),NzN,NzM) -> gcd(d(NzN,NzM),NzM)
  Usable Rule Processor:
   DPs:
    +#(s(N),s(M)) -> +#(N,M)
    *#(s(N),s(M)) -> *#(N,M)
    *#(s(N),s(M)) -> +#(M,*(N,M))
    *#(s(N),s(M)) -> +#(N,+(M,*(N,M)))
    gt#(NzN,0()) -> is_NzNat#(NzN)
    gt#(NzN,0()) -> u_4#(is_NzNat(NzN))
    gt#(s(N),s(M)) -> gt#(N,M)
    lt#(N,M) -> gt#(M,N)
    d#(s(N),s(M)) -> d#(N,M)
    quot#(N,NzM) -> is_NzNat#(NzM)
    quot#(N,NzM) -> u_11#(is_NzNat(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#(N,NzM)
    u_1#(True(),N,NzM) -> quot#(d(N,NzM),NzM)
    quot#(NzM,NzM) -> is_NzNat#(NzM)
    quot#(NzM,NzM) -> u_01#(is_NzNat(NzM))
    quot#(N,NzM) -> u_21#(is_NzNat(NzM),NzM,N)
    u_21#(True(),NzM,N) -> gt#(NzM,N)
    u_21#(True(),NzM,N) -> u_2#(gt(NzM,N))
    gcd#(NzM,NzM) -> is_NzNat#(NzM)
    gcd#(NzM,NzM) -> u_02#(is_NzNat(NzM),NzM)
    gcd#(NzN,NzM) -> is_NzNat#(NzM)
    gcd#(NzN,NzM) -> is_NzNat#(NzN)
    gcd#(NzN,NzM) -> u_31#(is_NzNat(NzN),is_NzNat(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#(NzN,NzM)
    u_3#(True(),NzN,NzM) -> gcd#(d(NzN,NzM),NzM)
   TRS:
    *(N,0()) -> 0()
    *(s(N),s(M)) -> s(+(N,+(M,*(N,M))))
    +(N,0()) -> N
    +(s(N),s(M)) -> s(s(+(N,M)))
    is_NzNat(0()) -> False()
    is_NzNat(s(N)) -> True()
    gt(0(),M) -> False()
    gt(NzN,0()) -> u_4(is_NzNat(NzN))
    gt(s(N),s(M)) -> gt(N,M)
    u_4(True()) -> True()
    d(0(),N) -> N
    d(s(N),s(M)) -> d(N,M)
   Open