MAYBE
* Step 1: Failure MAYBE
  + Considered Problem:
      - Strict TRS:
          *(N,0()) -> 0()
          *(s(N),s(M)) -> s(+(N,+(M,*(N,M))))
          +(N,0()) -> N
          +(s(N),s(M)) -> s(s(+(N,M)))
          d(0(),N) -> N
          d(s(N),s(M)) -> d(N,M)
          gcd(NzM,NzM) -> u_02(is_NzNat(NzM),NzM)
          gcd(NzN,NzM) -> u_31(is_NzNat(NzN),is_NzNat(NzM),NzN,NzM)
          gcd(0(),N) -> 0()
          gt(NzN,0()) -> u_4(is_NzNat(NzN))
          gt(0(),M) -> False()
          gt(s(N),s(M)) -> gt(N,M)
          is_NzNat(0()) -> False()
          is_NzNat(s(N)) -> True()
          lt(N,M) -> gt(M,N)
          p(s(N)) -> N
          quot(N,NzM) -> u_11(is_NzNat(NzM),N,NzM)
          quot(N,NzM) -> u_21(is_NzNat(NzM),NzM,N)
          quot(NzM,NzM) -> u_01(is_NzNat(NzM))
          u_01(True()) -> s(0())
          u_02(True(),NzM) -> NzM
          u_1(True(),N,NzM) -> s(quot(d(N,NzM),NzM))
          u_11(True(),N,NzM) -> u_1(gt(N,NzM),N,NzM)
          u_2(True()) -> 0()
          u_21(True(),NzM,N) -> u_2(gt(NzM,N))
          u_3(True(),NzN,NzM) -> gcd(d(NzN,NzM),NzM)
          u_31(True(),True(),NzN,NzM) -> u_3(gt(NzN,NzM),NzN,NzM)
          u_4(True()) -> True()
      - Signature:
          {*/2,+/2,d/2,gcd/2,gt/2,is_NzNat/1,lt/2,p/1,quot/2,u_01/1,u_02/2,u_1/3,u_11/3,u_2/1,u_21/3,u_3/3,u_31/4
          ,u_4/1} / {0/0,False/0,True/0,s/1}
      - Obligation:
          innermost runtime complexity wrt. defined symbols {*,+,d,gcd,gt,is_NzNat,lt,p,quot,u_01,u_02,u_1,u_11,u_2
          ,u_21,u_3,u_31,u_4} and constructors {0,False,True,s}
  + Applied Processor:
      Ara {heuristics_ = NoHeuristics, minDegree = 1, maxDegree = 3, araTimeout = 60, araFindStrictRules = Nothing, araSmtSolver = MiniSMT}
  + Details:
      The input can not be schown compatible.
MAYBE