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

TRS termination of:
[1] eq(0,0) -> true
[2] eq(0,s(x)) -> false
[3] eq(s(x),0) -> false
[4] eq(s(x),s(y)) -> eq(x,y)
[5] or(true,y) -> true
[6] or(false,y) -> y
[7] union(empty,h) -> h
[8] union(edge(x,y,i),h) -> edge(x,y,union(i,h))
[9] isEmpty(empty) -> true
[10] isEmpty(edge(x,y,i)) -> false
[11] from(edge(x,y,i)) -> x
[12] to(edge(x,y,i)) -> y
[13] rest(edge(x,y,i)) -> i
[14] rest(empty) -> empty
[15] reach(x,y,i,h) ->
 if1(eq(x,y),isEmpty(i),eq(x,from(i)),eq(y,to(i)),x,y,i,h)
[16] if1(true,b1,b2,b3,x,y,i,h) -> true
[17] if1(false,b1,b2,b3,x,y,i,h) -> if2(b1,b2,b3,x,y,i,h)
[18] if2(true,b2,b3,x,y,i,h) -> false
[19] if2(false,b2,b3,x,y,i,h) -> if3(b2,b3,x,y,i,h)
[20] if3(false,b3,x,y,i,h) -> reach(x,y,rest(i),edge(from(i),to(i),h))
[21] if3(true,b3,x,y,i,h) -> if4(b3,x,y,i,h)
[22] if4(true,x,y,i,h) -> true
[23] if4(false,x,y,i,h) ->
 or(reach(x,y,rest(i),h),reach(to(i),y,union(rest(i),h),empty))


Sub problem: 
guided: 

DP termination of:
<Marked_eq(s(x),s(y)) , Marked_eq(x,y)>
<Marked_union(edge(x,y,i),h) , Marked_union(i,h)>
<Marked_reach(x,y,i,h) , Marked_if1(eq(x,y),isEmpty(i),eq(x,from(i)),
                          eq(y,to(i)),x,y,i,h)>
<Marked_reach(x,y,i,h) , Marked_eq(x,y)>
<Marked_reach(x,y,i,h) , Marked_isEmpty(i)>
<Marked_reach(x,y,i,h) , Marked_eq(x,from(i))>
<Marked_reach(x,y,i,h) , Marked_from(i)>
<Marked_reach(x,y,i,h) , Marked_eq(y,to(i))>
<Marked_reach(x,y,i,h) , Marked_to(i)>
<Marked_if1(false,b1,b2,b3,x,y,i,h) , Marked_if2(b1,b2,b3,x,y,i,h)>
<Marked_if2(false,b2,b3,x,y,i,h) , Marked_if3(b2,b3,x,y,i,h)>
<Marked_if3(false,b3,x,y,i,h) , Marked_reach(x,y,rest(i),edge(from(i),to(i),h))>
<Marked_if3(false,b3,x,y,i,h) , Marked_rest(i)>
<Marked_if3(false,b3,x,y,i,h) , Marked_from(i)>
<Marked_if3(false,b3,x,y,i,h) , Marked_to(i)>
<Marked_if3(true,b3,x,y,i,h) , Marked_if4(b3,x,y,i,h)>
<Marked_if4(false,x,y,i,h) , Marked_or(reach(x,y,rest(i),h),
                              reach(to(i),y,union(rest(i),h),empty))>
<Marked_if4(false,x,y,i,h) , Marked_reach(x,y,rest(i),h)>
<Marked_if4(false,x,y,i,h) , Marked_rest(i)>
<Marked_if4(false,x,y,i,h) , Marked_reach(to(i),y,union(rest(i),h),empty)>
<Marked_if4(false,x,y,i,h) , Marked_to(i)>
<Marked_if4(false,x,y,i,h) , Marked_union(rest(i),h)>
<Marked_if4(false,x,y,i,h) , Marked_rest(i)>
 
END GUIDED
APPLY CRITERIA (Graph splitting)
Found 3 components:

{  <Marked_if4(false,x,y,i,h) , Marked_reach(to(i),y,union(rest(i),h),empty)> 
      --> <Marked_reach(x,y,i,h) , Marked_if1(eq(x,y),isEmpty(i),eq(x,from(i)),
                                    eq(y,to(i)),x,y,i,h)>
  <Marked_if4(false,x,y,i,h) , Marked_reach(x,y,rest(i),h)> 
     --> <Marked_reach(x,y,i,h) , Marked_if1(eq(x,y),isEmpty(i),eq(x,from(i)),
                                   eq(y,to(i)),x,y,i,h)>
  <Marked_if3(true,b3,x,y,i,h) , Marked_if4(b3,x,y,i,h)> 
     --> <Marked_if4(false,x,y,i,h) , Marked_reach(to(i),y,union(rest(i),h),
                                       empty)>
  <Marked_if3(true,b3,x,y,i,h) , Marked_if4(b3,x,y,i,h)> 
     --> <Marked_if4(false,x,y,i,h) , Marked_reach(x,y,rest(i),h)>
  <Marked_if3(false,b3,x,y,i,h) , Marked_reach(x,y,rest(i),
                                   edge(from(i),to(i),h))> 
     --> <Marked_reach(x,y,i,h) , Marked_if1(eq(x,y),isEmpty(i),eq(x,from(i)),
                                   eq(y,to(i)),x,y,i,h)>
  <Marked_if2(false,b2,b3,x,y,i,h) , Marked_if3(b2,b3,x,y,i,h)> 
     --> <Marked_if3(true,b3,x,y,i,h) , Marked_if4(b3,x,y,i,h)>
  <Marked_if2(false,b2,b3,x,y,i,h) , Marked_if3(b2,b3,x,y,i,h)> 
     --> <Marked_if3(false,b3,x,y,i,h) , Marked_reach(x,y,rest(i),
                                          edge(from(i),to(i),h))>
  <Marked_if1(false,b1,b2,b3,x,y,i,h) , Marked_if2(b1,b2,b3,x,y,i,h)> 
     --> <Marked_if2(false,b2,b3,x,y,i,h) , Marked_if3(b2,b3,x,y,i,h)>
  <Marked_reach(x,y,i,h) , Marked_if1(eq(x,y),isEmpty(i),eq(x,from(i)),
                            eq(y,to(i)),x,y,i,h)> 
     --> <Marked_if1(false,b1,b2,b3,x,y,i,h) , Marked_if2(b1,b2,b3,x,y,i,h)>
}

{  <Marked_eq(s(x),s(y)) , Marked_eq(x,y)> 
      --> <Marked_eq(s(x),s(y)) , Marked_eq(x,y)>
}

{  <Marked_union(edge(x,y,i),h) , Marked_union(i,h)> 
      --> <Marked_union(edge(x,y,i),h) , Marked_union(i,h)>
}
APPLY CRITERIA (Subterm criterion)
APPLY CRITERIA (Choosing graph)
Trying to solve the following constraints:
{
  eq(0,0) >= true ;
  eq(0,s(x)) >= false ;
  eq(s(x),0) >= false ;
  eq(s(x),s(y)) >= eq(x,y) ;
  or(true,y) >= true ;
  or(false,y) >= y ;
  union(empty,h) >= h ;
  union(edge(x,y,i),h) >= edge(x,y,union(i,h)) ;
  isEmpty(empty) >= true ;
  isEmpty(edge(x,y,i)) >= false ;
  from(edge(x,y,i)) >= x ;
  to(edge(x,y,i)) >= y ;
  rest(empty) >= empty ;
  rest(edge(x,y,i)) >= i ;
  if1(true,b1,b2,b3,x,y,i,h) >= true ;
  if1(false,b1,b2,b3,x,y,i,h) >= if2(b1,b2,b3,x,y,i,h) ;
  reach(x,y,i,h) >= if1(eq(x,y),isEmpty(i),eq(x,from(i)),eq(y,to(i)),x,y,i,h) ;
  if2(true,b2,b3,x,y,i,h) >= false ;
  if2(false,b2,b3,x,y,i,h) >= if3(b2,b3,x,y,i,h) ;
  if3(true,b3,x,y,i,h) >= if4(b3,x,y,i,h) ;
  if3(false,b3,x,y,i,h) >= reach(x,y,rest(i),edge(from(i),to(i),h)) ;
  if4(true,x,y,i,h) >= true ;
  if4(false,x,y,i,h) >= or(reach(x,y,rest(i),h),
                         reach(to(i),y,union(rest(i),h),empty)) ;
  Marked_if4(false,x,y,i,h) >= Marked_reach(to(i),y,union(rest(i),h),empty) ;
  Marked_if4(false,x,y,i,h) >= Marked_reach(x,y,rest(i),h) ;
  Marked_reach(x,y,i,h) >= Marked_if1(eq(x,y),isEmpty(i),eq(x,from(i)),
                            eq(y,to(i)),x,y,i,h) ;
  Marked_if3(true,b3,x,y,i,h) >= Marked_if4(b3,x,y,i,h) ;
  Marked_if3(false,b3,x,y,i,h) >= Marked_reach(x,y,rest(i),
                                   edge(from(i),to(i),h)) ;
  Marked_if2(false,b2,b3,x,y,i,h) >= Marked_if3(b2,b3,x,y,i,h) ;
  Marked_if1(false,b1,b2,b3,x,y,i,h) >= Marked_if2(b1,b2,b3,x,y,i,h) ;
 }
 + Disjunctions:{ 
{
  Marked_if4(false,x,y,i,h) > Marked_reach(to(i),y,union(rest(i),h),empty) ;
 }
{
  Marked_if4(false,x,y,i,h) > Marked_reach(x,y,rest(i),h) ;
 }
{
  Marked_reach(x,y,i,h) > Marked_if1(eq(x,y),isEmpty(i),eq(x,from(i)),
                           eq(y,to(i)),x,y,i,h) ;
 }
{
  Marked_if3(true,b3,x,y,i,h) > Marked_if4(b3,x,y,i,h) ;
 }
{
  Marked_if3(false,b3,x,y,i,h) > Marked_reach(x,y,rest(i),
                                  edge(from(i),to(i),h)) ;
 }
{
  Marked_if2(false,b2,b3,x,y,i,h) > Marked_if3(b2,b3,x,y,i,h) ;
 }
{
  Marked_if1(false,b1,b2,b3,x,y,i,h) > Marked_if2(b1,b2,b3,x,y,i,h) ;
 }
 } 
=== 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
=== 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 (Simple graph)
Found the following constraints:
{
  eq(0,0) >= true ;
  eq(0,s(x)) >= false ;
  eq(s(x),0) >= false ;
  eq(s(x),s(y)) >= eq(x,y) ;
  or(true,y) >= true ;
  or(false,y) >= y ;
  union(empty,h) >= h ;
  union(edge(x,y,i),h) >= edge(x,y,union(i,h)) ;
  isEmpty(empty) >= true ;
  isEmpty(edge(x,y,i)) >= false ;
  from(edge(x,y,i)) >= x ;
  to(edge(x,y,i)) >= y ;
  rest(empty) >= empty ;
  rest(edge(x,y,i)) >= i ;
  if1(true,b1,b2,b3,x,y,i,h) >= true ;
  if1(false,b1,b2,b3,x,y,i,h) >= if2(b1,b2,b3,x,y,i,h) ;
  reach(x,y,i,h) >= if1(eq(x,y),isEmpty(i),eq(x,from(i)),eq(y,to(i)),x,y,i,h) ;
  if2(true,b2,b3,x,y,i,h) >= false ;
  if2(false,b2,b3,x,y,i,h) >= if3(b2,b3,x,y,i,h) ;
  if3(true,b3,x,y,i,h) >= if4(b3,x,y,i,h) ;
  if3(false,b3,x,y,i,h) >= reach(x,y,rest(i),edge(from(i),to(i),h)) ;
  if4(true,x,y,i,h) >= true ;
  if4(false,x,y,i,h) >= or(reach(x,y,rest(i),h),
                         reach(to(i),y,union(rest(i),h),empty)) ;
  Marked_if4(false,x,y,i,h) >= Marked_reach(to(i),y,union(rest(i),h),empty) ;
  Marked_if4(false,x,y,i,h) > Marked_reach(x,y,rest(i),h) ;
  Marked_reach(x,y,i,h) >= Marked_if1(eq(x,y),isEmpty(i),eq(x,from(i)),
                            eq(y,to(i)),x,y,i,h) ;
  Marked_if3(true,b3,x,y,i,h) > Marked_if4(b3,x,y,i,h) ;
  Marked_if3(false,b3,x,y,i,h) > Marked_reach(x,y,rest(i),
                                  edge(from(i),to(i),h)) ;
  Marked_if2(false,b2,b3,x,y,i,h) >= Marked_if3(b2,b3,x,y,i,h) ;
  Marked_if1(false,b1,b2,b3,x,y,i,h) >= Marked_if2(b1,b2,b3,x,y,i,h) ;
 }

APPLY CRITERIA (SOLVE_ORD)
Trying to solve the following constraints:
{
  eq(0,0) >= true ;
  eq(0,s(x)) >= false ;
  eq(s(x),0) >= false ;
  eq(s(x),s(y)) >= eq(x,y) ;
  or(true,y) >= true ;
  or(false,y) >= y ;
  union(empty,h) >= h ;
  union(edge(x,y,i),h) >= edge(x,y,union(i,h)) ;
  isEmpty(empty) >= true ;
  isEmpty(edge(x,y,i)) >= false ;
  from(edge(x,y,i)) >= x ;
  to(edge(x,y,i)) >= y ;
  rest(empty) >= empty ;
  rest(edge(x,y,i)) >= i ;
  if1(true,b1,b2,b3,x,y,i,h) >= true ;
  if1(false,b1,b2,b3,x,y,i,h) >= if2(b1,b2,b3,x,y,i,h) ;
  reach(x,y,i,h) >= if1(eq(x,y),isEmpty(i),eq(x,from(i)),eq(y,to(i)),x,y,i,h) ;
  if2(true,b2,b3,x,y,i,h) >= false ;
  if2(false,b2,b3,x,y,i,h) >= if3(b2,b3,x,y,i,h) ;
  if3(true,b3,x,y,i,h) >= if4(b3,x,y,i,h) ;
  if3(false,b3,x,y,i,h) >= reach(x,y,rest(i),edge(from(i),to(i),h)) ;
  if4(true,x,y,i,h) >= true ;
  if4(false,x,y,i,h) >= or(reach(x,y,rest(i),h),
                         reach(to(i),y,union(rest(i),h),empty)) ;
  Marked_if4(false,x,y,i,h) >= Marked_reach(to(i),y,union(rest(i),h),empty) ;
  Marked_if4(false,x,y,i,h) > Marked_reach(x,y,rest(i),h) ;
  Marked_reach(x,y,i,h) >= Marked_if1(eq(x,y),isEmpty(i),eq(x,from(i)),
                            eq(y,to(i)),x,y,i,h) ;
  Marked_if3(true,b3,x,y,i,h) > Marked_if4(b3,x,y,i,h) ;
  Marked_if3(false,b3,x,y,i,h) > Marked_reach(x,y,rest(i),
                                  edge(from(i),to(i),h)) ;
  Marked_if2(false,b2,b3,x,y,i,h) >= Marked_if3(b2,b3,x,y,i,h) ;
  Marked_if1(false,b1,b2,b3,x,y,i,h) >= Marked_if2(b1,b2,b3,x,y,i,h) ;
 }
 + 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 ===
Time out for these parameters.
=== TIMER virtual : 15.000000 ===
Entering poly_solver
Starting Sat solver initialization
=== 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 87.606194 seconds (real time)
Cime Exit Status: 0