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

TRS termination of:
[1] car(cons(x,l)) -> x
[2] cddr(nil) -> nil
[3] cddr(cons(x,nil)) -> nil
[4] cddr(cons(x,cons(y,l))) -> l
[5] cadr(cons(x,cons(y,l))) -> y
[6] isZero(0) -> true
[7] isZero(s(x)) -> false
[8] plus(x,y) -> ifplus(isZero(x),x,y)
[9] ifplus(true,x,y) -> y
[10] ifplus(false,x,y) -> s(plus(p(x),y))
[11] times(x,y) -> iftimes(isZero(x),x,y)
[12] iftimes(true,x,y) -> 0
[13] iftimes(false,x,y) -> plus(y,times(p(x),y))
[14] p(s(x)) -> x
[15] p(0) -> 0
[16] shorter(nil,y) -> true
[17] shorter(cons(x,l),0) -> false
[18] shorter(cons(x,l),s(y)) -> shorter(l,y)
[19] prod(l) -> if(shorter(l,0),shorter(l,s(0)),l)
[20] if(true,b,l) -> s(0)
[21] if(false,b,l) -> if2(b,l)
[22] if2(true,l) -> car(l)
[23] if2(false,l) -> prod(cons(times(car(l),cadr(l)),cddr(l)))


Sub problem: 
guided: 

DP termination of:
<Marked_plus(x,y) , Marked_ifplus(isZero(x),x,y)>
<Marked_plus(x,y) , Marked_isZero(x)>
<Marked_ifplus(false,x,y) , Marked_plus(p(x),y)>
<Marked_ifplus(false,x,y) , Marked_p(x)>
<Marked_times(x,y) , Marked_iftimes(isZero(x),x,y)>
<Marked_times(x,y) , Marked_isZero(x)>
<Marked_iftimes(false,x,y) , Marked_plus(y,times(p(x),y))>
<Marked_iftimes(false,x,y) , Marked_times(p(x),y)>
<Marked_iftimes(false,x,y) , Marked_p(x)>
<Marked_shorter(cons(x,l),s(y)) , Marked_shorter(l,y)>
<Marked_prod(l) , Marked_if(shorter(l,0),shorter(l,s(0)),l)>
<Marked_prod(l) , Marked_shorter(l,0)>
<Marked_prod(l) , Marked_shorter(l,s(0))>
<Marked_if(false,b,l) , Marked_if2(b,l)>
<Marked_if2(true,l) , Marked_car(l)>
<Marked_if2(false,l) , Marked_prod(cons(times(car(l),cadr(l)),cddr(l)))>
<Marked_if2(false,l) , Marked_times(car(l),cadr(l))>
<Marked_if2(false,l) , Marked_car(l)>
<Marked_if2(false,l) , Marked_cadr(l)>
<Marked_if2(false,l) , Marked_cddr(l)>
 
END GUIDED
APPLY CRITERIA (Graph splitting)
Found 4 components:

{  <Marked_if2(false,l) , Marked_prod(cons(times(car(l),cadr(l)),cddr(l)))> 
      --> <Marked_prod(l) , Marked_if(shorter(l,0),shorter(l,s(0)),l)>
  <Marked_if(false,b,l) , Marked_if2(b,l)> 
     --> <Marked_if2(false,l) , Marked_prod(cons(times(car(l),cadr(l)),cddr(l)))>
  <Marked_prod(l) , Marked_if(shorter(l,0),shorter(l,s(0)),l)> 
     --> <Marked_if(false,b,l) , Marked_if2(b,l)>
}

{  <Marked_shorter(cons(x,l),s(y)) , Marked_shorter(l,y)> 
      --> <Marked_shorter(cons(x,l),s(y)) , Marked_shorter(l,y)>
}

{  <Marked_iftimes(false,x,y) , Marked_times(p(x),y)> 
      --> <Marked_times(x,y) , Marked_iftimes(isZero(x),x,y)>
  <Marked_times(x,y) , Marked_iftimes(isZero(x),x,y)> 
     --> <Marked_iftimes(false,x,y) , Marked_times(p(x),y)>
}

{  <Marked_ifplus(false,x,y) , Marked_plus(p(x),y)> 
      --> <Marked_plus(x,y) , Marked_ifplus(isZero(x),x,y)>
  <Marked_plus(x,y) , Marked_ifplus(isZero(x),x,y)> 
     --> <Marked_ifplus(false,x,y) , Marked_plus(p(x),y)>
}
APPLY CRITERIA (Choosing graph)
Trying to solve the following constraints:
{
  car(cons(x,l)) >= x ;
  cddr(cons(x,cons(y,l))) >= l ;
  cddr(cons(x,nil)) >= nil ;
  cddr(nil) >= nil ;
  cadr(cons(x,cons(y,l))) >= y ;
  isZero(0) >= true ;
  isZero(s(x)) >= false ;
  ifplus(true,x,y) >= y ;
  ifplus(false,x,y) >= s(plus(p(x),y)) ;
  plus(x,y) >= ifplus(isZero(x),x,y) ;
  p(0) >= 0 ;
  p(s(x)) >= x ;
  iftimes(true,x,y) >= 0 ;
  iftimes(false,x,y) >= plus(y,times(p(x),y)) ;
  times(x,y) >= iftimes(isZero(x),x,y) ;
  shorter(cons(x,l),0) >= false ;
  shorter(cons(x,l),s(y)) >= shorter(l,y) ;
  shorter(nil,y) >= true ;
  if(true,b,l) >= s(0) ;
  if(false,b,l) >= if2(b,l) ;
  prod(l) >= if(shorter(l,0),shorter(l,s(0)),l) ;
  if2(true,l) >= car(l) ;
  if2(false,l) >= prod(cons(times(car(l),cadr(l)),cddr(l))) ;
  Marked_if2(false,l) >= Marked_prod(cons(times(car(l),cadr(l)),cddr(l))) ;
  Marked_prod(l) >= Marked_if(shorter(l,0),shorter(l,s(0)),l) ;
  Marked_if(false,b,l) >= Marked_if2(b,l) ;
 }
 + Disjunctions:{ 
{
  Marked_if2(false,l) > Marked_prod(cons(times(car(l),cadr(l)),cddr(l))) ;
 }
{
  Marked_prod(l) > Marked_if(shorter(l,0),shorter(l,s(0)),l) ;
 }
{
  Marked_if(false,b,l) > Marked_if2(b,l) ;
 }
 } 
=== 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 32.431568 seconds (real time)
Cime Exit Status: 0