- : unit = ()
h : heuristic = <heuristic>
- : unit = ()
APPLY CRITERIA (Marked dependency pairs)

TRS termination of:
[1] p(s(N)) -> N
[2] +(N,0) -> N
[3] +(s(N),s(M)) -> s(s(+(N,M)))
[4]  *(N,0) -> 0
[5]  *(s(N),s(M)) -> s(+(N,+(M, *(N,M))))
[6] gt(0,M) -> False
[7] gt(NzN,0) -> u_4(is_NzNat(NzN))
[8] u_4(True) -> True
[9] is_NzNat(0) -> False
[10] is_NzNat(s(N)) -> True
[11] gt(s(N),s(M)) -> gt(N,M)
[12] lt(N,M) -> gt(M,N)
[13] d(0,N) -> N
[14] d(s(N),s(M)) -> d(N,M)
[15] quot(N,NzM) -> u_11(is_NzNat(NzM),N,NzM)
[16] u_11(True,N,NzM) -> u_1(gt(N,NzM),N,NzM)
[17] u_1(True,N,NzM) -> s(quot(d(N,NzM),NzM))
[18] quot(NzM,NzM) -> u_01(is_NzNat(NzM))
[19] u_01(True) -> s(0)
[20] quot(N,NzM) -> u_21(is_NzNat(NzM),NzM,N)
[21] u_21(True,NzM,N) -> u_2(gt(NzM,N))
[22] u_2(True) -> 0
[23] gcd(0,N) -> 0
[24] gcd(NzM,NzM) -> u_02(is_NzNat(NzM),NzM)
[25] u_02(True,NzM) -> NzM
[26] gcd(NzN,NzM) -> u_31(is_NzNat(NzN),is_NzNat(NzM),NzN,NzM)
[27] u_31(True,True,NzN,NzM) -> u_3(gt(NzN,NzM),NzN,NzM)
[28] u_3(True,NzN,NzM) -> gcd(d(NzN,NzM),NzM)


Sub problem: 
guided: 

DP termination of:
<Marked_+(s(N),s(M)) , Marked_+(N,M)>
<Marked_*(s(N),s(M)) , Marked_+(N,+(M, *(N,M)))>
<Marked_*(s(N),s(M)) , Marked_+(M, *(N,M))>
<Marked_*(s(N),s(M)) , Marked_*(N,M)>
<Marked_gt(NzN,0) , Marked_u_4(is_NzNat(NzN))>
<Marked_gt(NzN,0) , Marked_is_NzNat(NzN)>
<Marked_gt(s(N),s(M)) , Marked_gt(N,M)>
<Marked_lt(N,M) , Marked_gt(M,N)>
<Marked_d(s(N),s(M)) , Marked_d(N,M)>
<Marked_quot(N,NzM) , Marked_u_11(is_NzNat(NzM),N,NzM)>
<Marked_quot(N,NzM) , Marked_is_NzNat(NzM)>
<Marked_u_11(True,N,NzM) , Marked_u_1(gt(N,NzM),N,NzM)>
<Marked_u_11(True,N,NzM) , Marked_gt(N,NzM)>
<Marked_u_1(True,N,NzM) , Marked_quot(d(N,NzM),NzM)>
<Marked_u_1(True,N,NzM) , Marked_d(N,NzM)>
<Marked_quot(NzM,NzM) , Marked_u_01(is_NzNat(NzM))>
<Marked_quot(NzM,NzM) , Marked_is_NzNat(NzM)>
<Marked_quot(N,NzM) , Marked_u_21(is_NzNat(NzM),NzM,N)>
<Marked_quot(N,NzM) , Marked_is_NzNat(NzM)>
<Marked_u_21(True,NzM,N) , Marked_u_2(gt(NzM,N))>
<Marked_u_21(True,NzM,N) , Marked_gt(NzM,N)>
<Marked_gcd(NzM,NzM) , Marked_u_02(is_NzNat(NzM),NzM)>
<Marked_gcd(NzM,NzM) , Marked_is_NzNat(NzM)>
<Marked_gcd(NzN,NzM) , Marked_u_31(is_NzNat(NzN),is_NzNat(NzM),NzN,NzM)>
<Marked_gcd(NzN,NzM) , Marked_is_NzNat(NzN)>
<Marked_gcd(NzN,NzM) , Marked_is_NzNat(NzM)>
<Marked_u_31(True,True,NzN,NzM) , Marked_u_3(gt(NzN,NzM),NzN,NzM)>
<Marked_u_31(True,True,NzN,NzM) , Marked_gt(NzN,NzM)>
<Marked_u_3(True,NzN,NzM) , Marked_gcd(d(NzN,NzM),NzM)>
<Marked_u_3(True,NzN,NzM) , Marked_d(NzN,NzM)>
 
END GUIDED
APPLY CRITERIA (Graph splitting)
Found 6 components:

{  <Marked_*(s(N),s(M)) , Marked_*(N,M)> 
      --> <Marked_*(s(N),s(M)) , Marked_*(N,M)>
}

{  <Marked_+(s(N),s(M)) , Marked_+(N,M)> 
      --> <Marked_+(s(N),s(M)) , Marked_+(N,M)>
}

{  <Marked_u_1(True,N,NzM) , Marked_quot(d(N,NzM),NzM)> 
      --> <Marked_quot(N,NzM) , Marked_u_11(is_NzNat(NzM),N,NzM)>
  <Marked_u_11(True,N,NzM) , Marked_u_1(gt(N,NzM),N,NzM)> 
     --> <Marked_u_1(True,N,NzM) , Marked_quot(d(N,NzM),NzM)>
  <Marked_quot(N,NzM) , Marked_u_11(is_NzNat(NzM),N,NzM)> 
     --> <Marked_u_11(True,N,NzM) , Marked_u_1(gt(N,NzM),N,NzM)>
}

{  <Marked_u_3(True,NzN,NzM) , Marked_gcd(d(NzN,NzM),NzM)> 
      --> <Marked_gcd(NzN,NzM) , Marked_u_31(is_NzNat(NzN),is_NzNat(NzM),
                                  NzN,NzM)>
  <Marked_u_31(True,True,NzN,NzM) , Marked_u_3(gt(NzN,NzM),NzN,NzM)> 
     --> <Marked_u_3(True,NzN,NzM) , Marked_gcd(d(NzN,NzM),NzM)>
  <Marked_gcd(NzN,NzM) , Marked_u_31(is_NzNat(NzN),is_NzNat(NzM),NzN,NzM)> 
     --> <Marked_u_31(True,True,NzN,NzM) , Marked_u_3(gt(NzN,NzM),NzN,NzM)>
}

{  <Marked_gt(s(N),s(M)) , Marked_gt(N,M)> 
      --> <Marked_gt(s(N),s(M)) , Marked_gt(N,M)>
}

{  <Marked_d(s(N),s(M)) , Marked_d(N,M)> 
      --> <Marked_d(s(N),s(M)) , Marked_d(N,M)>
}
APPLY CRITERIA (Choosing graph)
Trying to solve the following constraints:
{
  p(s(N)) >= N ;
  +(s(N),s(M)) >= s(s(+(N,M))) ;
  +(N,0) >= N ;
   *(s(N),s(M)) >= s(+(N,+(M, *(N,M)))) ;
   *(N,0) >= 0 ;
  gt(s(N),s(M)) >= gt(N,M) ;
  gt(0,M) >= False ;
  gt(NzN,0) >= u_4(is_NzNat(NzN)) ;
  u_4(True) >= True ;
  is_NzNat(s(N)) >= True ;
  is_NzNat(0) >= False ;
  lt(N,M) >= gt(M,N) ;
  d(s(N),s(M)) >= d(N,M) ;
  d(0,N) >= N ;
  u_11(True,N,NzM) >= u_1(gt(N,NzM),N,NzM) ;
  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_1(True,N,NzM) >= s(quot(d(N,NzM),NzM)) ;
  u_01(True) >= s(0) ;
  u_21(True,NzM,N) >= u_2(gt(NzM,N)) ;
  u_2(True) >= 0 ;
  gcd(0,N) >= 0 ;
  gcd(NzN,NzM) >= u_31(is_NzNat(NzN),is_NzNat(NzM),NzN,NzM) ;
  gcd(NzM,NzM) >= u_02(is_NzNat(NzM),NzM) ;
  u_02(True,NzM) >= NzM ;
  u_31(True,True,NzN,NzM) >= u_3(gt(NzN,NzM),NzN,NzM) ;
  u_3(True,NzN,NzM) >= gcd(d(NzN,NzM),NzM) ;
  Marked_*(s(N),s(M)) >= Marked_*(N,M) ;
 }
 + Disjunctions:{ 
{
  Marked_*(s(N),s(M)) > Marked_*(N,M) ;
 }
 } 
=== TIMER virtual : 10.000000 ===
Entering poly_solver
Starting Sat solver initialization
Calling Sat solver...
=== STOPING TIMER virtual ===
=== TIMER real : 10.000000 ===
=== STOPING TIMER real ===
Sat solver returned
=== STOPING TIMER real ===
=== STOPING TIMER virtual ===
No solution found for these parameters.
Entering rpo_solver
=== TIMER virtual : 25.000000 ===
Search parameters: AFS type: 2 ; time limit: 25.. 
=== STOPING TIMER virtual ===
Time out for these parameters.
=== TIMER virtual : 15.000000 ===
Entering poly_solver
Starting Sat solver initialization
Calling Sat solver...
=== STOPING TIMER virtual ===
=== TIMER real : 15.000000 ===
=== STOPING TIMER real ===
Sat solver returned
=== STOPING TIMER real ===
=== STOPING TIMER virtual ===
No solution found for these parameters.
=== TIMER virtual : 50.000000 ===
trying sub matrices of size: 1
Matrix interpretation constraints generated.
Search parameters: LINEAR MATRIX 3x3 (strict=1x1) ; time limit: 50.. 
Termination constraints generated.
Starting Sat solver initialization
Calling Sat solver...
=== STOPING TIMER virtual ===
=== TIMER real : 50.000000 ===
=== STOPING TIMER real ===
Sat solver returned
=== STOPING TIMER real ===
=== STOPING TIMER virtual ===
No solution found for these parameters.
No solution found for these constraints.
APPLY CRITERIA (ID_CRIT)
NOT SOLVED
No proof found
Cime worked for 31.024868 seconds (real time)
Cime Exit Status: 0