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

TRS termination of:
[1]  *(0,x) -> 0
[2]  *(1,x) -> x
[3]  *(2,2) -> .(1,0)
[4]  *(3,x) -> .(x, *(min,x))
[5]  *(min,min) -> 1
[6]  *(2,min) -> .(min,2)
[7]  *(.(x,y),z) -> .( *(x,z), *(y,z))
[8]  *(+(y,z),x) -> +( *(x,y), *(x,z))
[9] +(0,x) -> x
[10] +(x,x) ->  *(2,x)
[11] +(1,2) -> 3
[12] +(1,min) -> 0
[13] +(2,min) -> 1
[14] +(3,x) -> .(1,+(min,x))
[15] +(.(x,y),z) -> .(x,+(y,z))
[16] +( *(2,x),x) ->  *(3,x)
[17] +( *(min,x),x) -> 0
[18] +( *(2,v), *(min,v)) -> v
[19] .(min,3) -> min
[20] .(x,min) -> .(+(min,x),3)
[21] .(0,x) -> x
[22] .(x,.(y,z)) -> .(+(x,y),z)


Sub problem: 
guided: 

DP termination of:
<Marked_*(2,2) , Marked_.(1,0)>
<Marked_*(3,x) , Marked_.(x, *(min,x))>
<Marked_*(3,x) , Marked_*(min,x)>
<Marked_*(2,min) , Marked_.(min,2)>
<Marked_*(.(x,y),z) , Marked_.( *(x,z), *(y,z))>
<Marked_*(.(x,y),z) , Marked_*(x,z)>
<Marked_*(.(x,y),z) , Marked_*(y,z)>
<Marked_*(+(y,z),x) , Marked_+( *(x,y), *(x,z))>
<Marked_*(+(y,z),x) , Marked_*(x,y)>
<Marked_*(+(y,z),x) , Marked_*(x,z)>
<Marked_+(x,x) , Marked_*(2,x)>
<Marked_+(3,x) , Marked_.(1,+(min,x))>
<Marked_+(3,x) , Marked_+(min,x)>
<Marked_+(.(x,y),z) , Marked_.(x,+(y,z))>
<Marked_+(.(x,y),z) , Marked_+(y,z)>
<Marked_+( *(2,x),x) , Marked_*(3,x)>
<Marked_.(x,min) , Marked_.(+(min,x),3)>
<Marked_.(x,min) , Marked_+(min,x)>
<Marked_.(x,.(y,z)) , Marked_.(+(x,y),z)>
<Marked_.(x,.(y,z)) , Marked_+(x,y)>
 
END GUIDED
APPLY CRITERIA (Graph splitting)
Found 2 components:

{  <Marked_*(+(y,z),x) , Marked_*(x,z)> 
      --> <Marked_*(+(y,z),x) , Marked_*(x,z)>
  <Marked_*(+(y,z),x) , Marked_*(x,z)> --> <Marked_*(+(y,z),x) , Marked_*(x,y)>
  <Marked_*(+(y,z),x) , Marked_*(x,z)> --> <Marked_*(.(x,y),z) , Marked_*(y,z)>
  <Marked_*(+(y,z),x) , Marked_*(x,z)> --> <Marked_*(.(x,y),z) , Marked_*(x,z)>
  <Marked_*(+(y,z),x) , Marked_*(x,y)> --> <Marked_*(+(y,z),x) , Marked_*(x,z)>
  <Marked_*(+(y,z),x) , Marked_*(x,y)> --> <Marked_*(+(y,z),x) , Marked_*(x,y)>
  <Marked_*(+(y,z),x) , Marked_*(x,y)> --> <Marked_*(.(x,y),z) , Marked_*(y,z)>
  <Marked_*(+(y,z),x) , Marked_*(x,y)> --> <Marked_*(.(x,y),z) , Marked_*(x,z)>
  <Marked_*(.(x,y),z) , Marked_*(y,z)> --> <Marked_*(+(y,z),x) , Marked_*(x,z)>
  <Marked_*(.(x,y),z) , Marked_*(y,z)> --> <Marked_*(+(y,z),x) , Marked_*(x,y)>
  <Marked_*(.(x,y),z) , Marked_*(y,z)> --> <Marked_*(.(x,y),z) , Marked_*(y,z)>
  <Marked_*(.(x,y),z) , Marked_*(y,z)> --> <Marked_*(.(x,y),z) , Marked_*(x,z)>
  <Marked_*(.(x,y),z) , Marked_*(x,z)> --> <Marked_*(+(y,z),x) , Marked_*(x,z)>
  <Marked_*(.(x,y),z) , Marked_*(x,z)> --> <Marked_*(+(y,z),x) , Marked_*(x,y)>
  <Marked_*(.(x,y),z) , Marked_*(x,z)> --> <Marked_*(.(x,y),z) , Marked_*(y,z)>
  <Marked_*(.(x,y),z) , Marked_*(x,z)> --> <Marked_*(.(x,y),z) , Marked_*(x,z)>
}

{  <Marked_.(x,.(y,z)) , Marked_+(x,y)> 
      --> <Marked_+( *(2,x),x) , Marked_*(3,x)>
  <Marked_.(x,.(y,z)) , Marked_+(x,y)> --> <Marked_+(.(x,y),z) , Marked_+(y,z)>
  <Marked_.(x,.(y,z)) , Marked_+(x,y)> 
     --> <Marked_+(.(x,y),z) , Marked_.(x,+(y,z))>
  <Marked_.(x,.(y,z)) , Marked_+(x,y)> 
     --> <Marked_+(3,x) , Marked_.(1,+(min,x))>
  <Marked_.(x,.(y,z)) , Marked_.(+(x,y),z)> 
     --> <Marked_.(x,.(y,z)) , Marked_+(x,y)>
  <Marked_.(x,.(y,z)) , Marked_.(+(x,y),z)> 
     --> <Marked_.(x,.(y,z)) , Marked_.(+(x,y),z)>
  <Marked_+( *(2,x),x) , Marked_*(3,x)> 
     --> <Marked_*(3,x) , Marked_.(x, *(min,x))>
  <Marked_+(.(x,y),z) , Marked_+(y,z)> 
     --> <Marked_+( *(2,x),x) , Marked_*(3,x)>
  <Marked_+(.(x,y),z) , Marked_+(y,z)> --> <Marked_+(.(x,y),z) , Marked_+(y,z)>
  <Marked_+(.(x,y),z) , Marked_+(y,z)> 
     --> <Marked_+(.(x,y),z) , Marked_.(x,+(y,z))>
  <Marked_+(.(x,y),z) , Marked_+(y,z)> 
     --> <Marked_+(3,x) , Marked_.(1,+(min,x))>
  <Marked_+(.(x,y),z) , Marked_.(x,+(y,z))> 
     --> <Marked_.(x,.(y,z)) , Marked_+(x,y)>
  <Marked_+(.(x,y),z) , Marked_.(x,+(y,z))> 
     --> <Marked_.(x,.(y,z)) , Marked_.(+(x,y),z)>
  <Marked_+(3,x) , Marked_.(1,+(min,x))> 
     --> <Marked_.(x,.(y,z)) , Marked_+(x,y)>
  <Marked_+(3,x) , Marked_.(1,+(min,x))> 
     --> <Marked_.(x,.(y,z)) , Marked_.(+(x,y),z)>
  <Marked_*(3,x) , Marked_.(x, *(min,x))> 
     --> <Marked_.(x,.(y,z)) , Marked_+(x,y)>
  <Marked_*(3,x) , Marked_.(x, *(min,x))> 
     --> <Marked_.(x,.(y,z)) , Marked_.(+(x,y),z)>
}
APPLY CRITERIA (Subterm criterion)
APPLY CRITERIA (Choosing graph)
Trying to solve the following constraints:
{
   *(0,x) >= 0 ;
   *(1,x) >= x ;
   *(.(x,y),z) >= .( *(x,z), *(y,z)) ;
   *(2,2) >= .(1,0) ;
   *(2,min) >= .(min,2) ;
   *(min,min) >= 1 ;
   *(3,x) >= .(x, *(min,x)) ;
   *(+(y,z),x) >= +( *(x,y), *(x,z)) ;
  .(0,x) >= x ;
  .(min,3) >= min ;
  .(x,.(y,z)) >= .(+(x,y),z) ;
  .(x,min) >= .(+(min,x),3) ;
  +(0,x) >= x ;
  +( *(2,v), *(min,v)) >= v ;
  +( *(2,x),x) >=  *(3,x) ;
  +( *(min,x),x) >= 0 ;
  +(1,2) >= 3 ;
  +(1,min) >= 0 ;
  +(.(x,y),z) >= .(x,+(y,z)) ;
  +(2,min) >= 1 ;
  +(3,x) >= .(1,+(min,x)) ;
  +(x,x) >=  *(2,x) ;
  Marked_*(.(x,y),z) >= Marked_*(x,z) ;
  Marked_*(.(x,y),z) >= Marked_*(y,z) ;
  Marked_*(+(y,z),x) >= Marked_*(x,y) ;
  Marked_*(+(y,z),x) >= Marked_*(x,z) ;
 }
 + Disjunctions:{ 
{
  Marked_*(.(x,y),z) > Marked_*(x,z) ;
 }
{
  Marked_*(.(x,y),z) > Marked_*(y,z) ;
 }
{
  Marked_*(+(y,z),x) > Marked_*(x,y) ;
 }
{
  Marked_*(+(y,z),x) > Marked_*(x,z) ;
 }
 } 
=== 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 ===
=== TIMER virtual : 25.000000 ===
Search parameters: AFS type: 2 ; time limit: 25.. 
=== STOPING TIMER virtual ===
=== TIMER virtual : 25.000000 ===
Search parameters: AFS type: 2 ; time limit: 25.. 
=== STOPING TIMER virtual ===
=== TIMER virtual : 25.000000 ===
Search parameters: AFS type: 2 ; time limit: 25.. 
=== STOPING TIMER virtual ===
=== 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 (Simple graph)
Found the following constraints:
{
   *(0,x) >= 0 ;
   *(1,x) >= x ;
   *(.(x,y),z) >= .( *(x,z), *(y,z)) ;
   *(2,2) >= .(1,0) ;
   *(2,min) >= .(min,2) ;
   *(min,min) >= 1 ;
   *(3,x) >= .(x, *(min,x)) ;
   *(+(y,z),x) >= +( *(x,y), *(x,z)) ;
  .(0,x) >= x ;
  .(min,3) >= min ;
  .(x,.(y,z)) >= .(+(x,y),z) ;
  .(x,min) >= .(+(min,x),3) ;
  +(0,x) >= x ;
  +( *(2,v), *(min,v)) >= v ;
  +( *(2,x),x) >=  *(3,x) ;
  +( *(min,x),x) >= 0 ;
  +(1,2) >= 3 ;
  +(1,min) >= 0 ;
  +(.(x,y),z) >= .(x,+(y,z)) ;
  +(2,min) >= 1 ;
  +(3,x) >= .(1,+(min,x)) ;
  +(x,x) >=  *(2,x) ;
  Marked_*(.(x,y),z) > Marked_*(x,z) ;
  Marked_*(.(x,y),z) > Marked_*(y,z) ;
  Marked_*(+(y,z),x) > Marked_*(x,y) ;
  Marked_*(+(y,z),x) > Marked_*(x,z) ;
 }

APPLY CRITERIA (SOLVE_ORD)
Trying to solve the following constraints:
{
   *(0,x) >= 0 ;
   *(1,x) >= x ;
   *(.(x,y),z) >= .( *(x,z), *(y,z)) ;
   *(2,2) >= .(1,0) ;
   *(2,min) >= .(min,2) ;
   *(min,min) >= 1 ;
   *(3,x) >= .(x, *(min,x)) ;
   *(+(y,z),x) >= +( *(x,y), *(x,z)) ;
  .(0,x) >= x ;
  .(min,3) >= min ;
  .(x,.(y,z)) >= .(+(x,y),z) ;
  .(x,min) >= .(+(min,x),3) ;
  +(0,x) >= x ;
  +( *(2,v), *(min,v)) >= v ;
  +( *(2,x),x) >=  *(3,x) ;
  +( *(min,x),x) >= 0 ;
  +(1,2) >= 3 ;
  +(1,min) >= 0 ;
  +(.(x,y),z) >= .(x,+(y,z)) ;
  +(2,min) >= 1 ;
  +(3,x) >= .(1,+(min,x)) ;
  +(x,x) >=  *(2,x) ;
  Marked_*(.(x,y),z) > Marked_*(x,z) ;
  Marked_*(.(x,y),z) > Marked_*(y,z) ;
  Marked_*(+(y,z),x) > Marked_*(x,y) ;
  Marked_*(+(y,z),x) > Marked_*(x,z) ;
 }
 + Disjunctions:{ 
 } 
=== 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 ===
No solution found for these parameters.(30 bt (26) [14])
=== 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 1.865372 seconds (real time)
Cime Exit Status: 0