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

TRS termination of:
[1] isEmpty(cons(x,xs)) -> false
[2] isEmpty(nil) -> true
[3] isZero(0) -> true
[4] isZero(s(x)) -> false
[5] head(cons(x,xs)) -> x
[6] tail(cons(x,xs)) -> xs
[7] tail(nil) -> nil
[8] append(nil,x) -> cons(x,nil)
[9] append(cons(y,ys),x) -> cons(y,append(ys,x))
[10] p(s(s(x))) -> s(p(s(x)))
[11] p(s(0)) -> 0
[12] p(0) -> 0
[13] inc(s(x)) -> s(inc(x))
[14] inc(0) -> s(0)
[15] addLists(xs,ys,zs) ->
 if(isEmpty(xs),isEmpty(ys),isZero(head(xs)),tail(xs),tail(ys),
  cons(p(head(xs)),tail(xs)),cons(inc(head(ys)),tail(ys)),zs,
  append(zs,head(ys)))
[16] if(true,true,b,xs,ys,xs2,ys2,zs,zs2) -> zs
[17] if(true,false,b,xs,ys,xs2,ys2,zs,zs2) -> differentLengthError
[18] if(false,true,b,xs,ys,xs2,ys2,zs,zs2) -> differentLengthError
[19] if(false,false,false,xs,ys,xs2,ys2,zs,zs2) -> addLists(xs2,ys2,zs)
[20] if(false,false,true,xs,ys,xs2,ys2,zs,zs2) -> addLists(xs,ys,zs2)
[21] addList(xs,ys) -> addLists(xs,ys,nil)


Sub problem: 
guided: 

DP termination of:
<Marked_append(cons(y,ys),x) , Marked_append(ys,x)>
<Marked_p(s(s(x))) , Marked_p(s(x))>
<Marked_inc(s(x)) , Marked_inc(x)>
<Marked_addLists(xs,ys,zs) , Marked_if(isEmpty(xs),isEmpty(ys),
                              isZero(head(xs)),tail(xs),tail(ys),
                              cons(p(head(xs)),tail(xs)),
                              cons(inc(head(ys)),tail(ys)),zs,
                              append(zs,head(ys)))>
<Marked_addLists(xs,ys,zs) , Marked_isEmpty(xs)>
<Marked_addLists(xs,ys,zs) , Marked_isEmpty(ys)>
<Marked_addLists(xs,ys,zs) , Marked_isZero(head(xs))>
<Marked_addLists(xs,ys,zs) , Marked_head(xs)>
<Marked_addLists(xs,ys,zs) , Marked_tail(xs)>
<Marked_addLists(xs,ys,zs) , Marked_tail(ys)>
<Marked_addLists(xs,ys,zs) , Marked_p(head(xs))>
<Marked_addLists(xs,ys,zs) , Marked_head(xs)>
<Marked_addLists(xs,ys,zs) , Marked_tail(xs)>
<Marked_addLists(xs,ys,zs) , Marked_inc(head(ys))>
<Marked_addLists(xs,ys,zs) , Marked_head(ys)>
<Marked_addLists(xs,ys,zs) , Marked_tail(ys)>
<Marked_addLists(xs,ys,zs) , Marked_append(zs,head(ys))>
<Marked_addLists(xs,ys,zs) , Marked_head(ys)>
<Marked_if(false,false,false,xs,ys,xs2,ys2,zs,zs2) , Marked_addLists(
                                                      xs2,ys2,zs)>
<Marked_if(false,false,true,xs,ys,xs2,ys2,zs,zs2) , Marked_addLists(xs,ys,zs2)>
<Marked_addList(xs,ys) , Marked_addLists(xs,ys,nil)>
 
END GUIDED
APPLY CRITERIA (Graph splitting)
Found 4 components:

{  <Marked_if(false,false,true,xs,ys,xs2,ys2,zs,zs2) , Marked_addLists(
                                                        xs,ys,zs2)> 
      --> <Marked_addLists(xs,ys,zs) , Marked_if(isEmpty(xs),isEmpty(ys),
                                        isZero(head(xs)),tail(xs),tail(ys),
                                        cons(p(head(xs)),tail(xs)),
                                        cons(inc(head(ys)),tail(ys)),
                                        zs,append(zs,head(ys)))>
  <Marked_if(false,false,false,xs,ys,xs2,ys2,zs,zs2) , Marked_addLists(
                                                        xs2,ys2,zs)> 
     --> <Marked_addLists(xs,ys,zs) , Marked_if(isEmpty(xs),isEmpty(ys),
                                       isZero(head(xs)),tail(xs),tail(ys),
                                       cons(p(head(xs)),tail(xs)),
                                       cons(inc(head(ys)),tail(ys)),zs,
                                       append(zs,head(ys)))>
  <Marked_addLists(xs,ys,zs) , Marked_if(isEmpty(xs),isEmpty(ys),
                                isZero(head(xs)),tail(xs),tail(ys),
                                cons(p(head(xs)),tail(xs)),
                                cons(inc(head(ys)),tail(ys)),zs,
                                append(zs,head(ys)))> 
     --> <Marked_if(false,false,true,xs,ys,xs2,ys2,zs,zs2) , Marked_addLists(
                                                              xs,ys,zs2)>
  <Marked_addLists(xs,ys,zs) , Marked_if(isEmpty(xs),isEmpty(ys),
                                isZero(head(xs)),tail(xs),tail(ys),
                                cons(p(head(xs)),tail(xs)),
                                cons(inc(head(ys)),tail(ys)),zs,
                                append(zs,head(ys)))> 
     --> <Marked_if(false,false,false,xs,ys,xs2,ys2,zs,zs2) , Marked_addLists(
                                                               xs2,ys2,
                                                               zs)>
}

{  <Marked_p(s(s(x))) , Marked_p(s(x))> 
      --> <Marked_p(s(s(x))) , Marked_p(s(x))>
}

{  <Marked_inc(s(x)) , Marked_inc(x)> --> <Marked_inc(s(x)) , Marked_inc(x)>
}

{  <Marked_append(cons(y,ys),x) , Marked_append(ys,x)> 
      --> <Marked_append(cons(y,ys),x) , Marked_append(ys,x)>
}
APPLY CRITERIA (Choosing graph)
Trying to solve the following constraints:
{
  isEmpty(cons(x,xs)) >= false ;
  isEmpty(nil) >= true ;
  isZero(0) >= true ;
  isZero(s(x)) >= false ;
  head(cons(x,xs)) >= x ;
  tail(cons(x,xs)) >= xs ;
  tail(nil) >= nil ;
  append(cons(y,ys),x) >= cons(y,append(ys,x)) ;
  append(nil,x) >= cons(x,nil) ;
  p(0) >= 0 ;
  p(s(0)) >= 0 ;
  p(s(s(x))) >= s(p(s(x))) ;
  inc(0) >= s(0) ;
  inc(s(x)) >= s(inc(x)) ;
  if(false,false,false,xs,ys,xs2,ys2,zs,zs2) >= addLists(xs2,ys2,zs) ;
  if(false,false,true,xs,ys,xs2,ys2,zs,zs2) >= addLists(xs,ys,zs2) ;
  if(false,true,b,xs,ys,xs2,ys2,zs,zs2) >= differentLengthError ;
  if(true,false,b,xs,ys,xs2,ys2,zs,zs2) >= differentLengthError ;
  if(true,true,b,xs,ys,xs2,ys2,zs,zs2) >= zs ;
  addLists(xs,ys,zs) >= if(isEmpty(xs),isEmpty(ys),isZero(head(xs)),tail(xs),
                         tail(ys),cons(p(head(xs)),tail(xs)),
                         cons(inc(head(ys)),tail(ys)),zs,append(zs,head(ys))) ;
  addList(xs,ys) >= addLists(xs,ys,nil) ;
  Marked_addLists(xs,ys,zs) >= Marked_if(isEmpty(xs),isEmpty(ys),
                                isZero(head(xs)),tail(xs),tail(ys),
                                cons(p(head(xs)),tail(xs)),
                                cons(inc(head(ys)),tail(ys)),zs,
                                append(zs,head(ys))) ;
  Marked_if(false,false,false,xs,ys,xs2,ys2,zs,zs2) >= Marked_addLists(
                                                        xs2,ys2,zs) ;
  Marked_if(false,false,true,xs,ys,xs2,ys2,zs,zs2) >= Marked_addLists(
                                                       xs,ys,zs2) ;
 }
 + Disjunctions:{ 
{
  Marked_addLists(xs,ys,zs) > Marked_if(isEmpty(xs),isEmpty(ys),
                               isZero(head(xs)),tail(xs),tail(ys),
                               cons(p(head(xs)),tail(xs)),
                               cons(inc(head(ys)),tail(ys)),zs,
                               append(zs,head(ys))) ;
 }
{
  Marked_if(false,false,false,xs,ys,xs2,ys2,zs,zs2) > Marked_addLists(
                                                       xs2,ys2,zs) ;
 }
{
  Marked_if(false,false,true,xs,ys,xs2,ys2,zs,zs2) > Marked_addLists(xs,ys,zs2) ;
 }
 } 
=== 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
=== STOPING TIMER virtual ===
Time out 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 43.551407 seconds (real time)
Cime Exit Status: 0