- : 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] reach(x,y,empty,h) -> false
[10] reach(x,y,edge(u,v,i),h) -> if_reach_1(eq(x,u),x,y,edge(u,v,i),h)
[11] if_reach_1(true,x,y,edge(u,v,i),h) ->
 if_reach_2(eq(y,v),x,y,edge(u,v,i),h)
[12] if_reach_2(true,x,y,edge(u,v,i),h) -> true
[13] if_reach_2(false,x,y,edge(u,v,i),h) ->
 or(reach(x,y,i,h),reach(v,y,union(i,h),empty))
[14] if_reach_1(false,x,y,edge(u,v,i),h) -> reach(x,y,i,edge(u,v,h))


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,edge(u,v,i),h) , Marked_if_reach_1(eq(x,u),x,y,edge(u,v,i),h)>
<Marked_reach(x,y,edge(u,v,i),h) , Marked_eq(x,u)>
<Marked_if_reach_1(true,x,y,edge(u,v,i),h) , Marked_if_reach_2(eq(y,v),
                                              x,y,edge(u,v,i),h)>
<Marked_if_reach_1(true,x,y,edge(u,v,i),h) , Marked_eq(y,v)>
<Marked_if_reach_2(false,x,y,edge(u,v,i),h) , Marked_or(reach(x,y,i,h),
                                               reach(v,y,union(i,h),empty))>
<Marked_if_reach_2(false,x,y,edge(u,v,i),h) , Marked_reach(x,y,i,h)>
<Marked_if_reach_2(false,x,y,edge(u,v,i),h) , Marked_reach(v,y,union(i,h),
                                               empty)>
<Marked_if_reach_2(false,x,y,edge(u,v,i),h) , Marked_union(i,h)>
<Marked_if_reach_1(false,x,y,edge(u,v,i),h) , Marked_reach(x,y,i,edge(u,v,h))>
 
END GUIDED
APPLY CRITERIA (Graph splitting)
Found 3 components:

{  <Marked_if_reach_1(false,x,y,edge(u,v,i),h) , Marked_reach(x,y,i,
                                                  edge(u,v,h))> 
      --> <Marked_reach(x,y,edge(u,v,i),h) , Marked_if_reach_1(eq(x,u),
                                              x,y,edge(u,v,i),h)>
  <Marked_if_reach_2(false,x,y,edge(u,v,i),h) , Marked_reach(v,y,union(i,h),
                                                 empty)> 
     --> <Marked_reach(x,y,edge(u,v,i),h) , Marked_if_reach_1(eq(x,u),
                                             x,y,edge(u,v,i),h)>
  <Marked_if_reach_2(false,x,y,edge(u,v,i),h) , Marked_reach(x,y,i,h)> 
     --> <Marked_reach(x,y,edge(u,v,i),h) , Marked_if_reach_1(eq(x,u),
                                             x,y,edge(u,v,i),h)>
  <Marked_if_reach_1(true,x,y,edge(u,v,i),h) , Marked_if_reach_2(eq(y,v),
                                                x,y,edge(u,v,i),h)> 
     --> <Marked_if_reach_2(false,x,y,edge(u,v,i),h) , Marked_reach(v,
                                                        y,union(i,h),
                                                        empty)>
  <Marked_if_reach_1(true,x,y,edge(u,v,i),h) , Marked_if_reach_2(eq(y,v),
                                                x,y,edge(u,v,i),h)> 
     --> <Marked_if_reach_2(false,x,y,edge(u,v,i),h) , Marked_reach(x,y,i,h)>
  <Marked_reach(x,y,edge(u,v,i),h) , Marked_if_reach_1(eq(x,u),x,y,edge(u,v,i),
                                      h)> 
     --> <Marked_if_reach_1(false,x,y,edge(u,v,i),h) , Marked_reach(x,
                                                        y,i,edge(u,v,h))>
  <Marked_reach(x,y,edge(u,v,i),h) , Marked_if_reach_1(eq(x,u),x,y,edge(u,v,i),
                                      h)> 
     --> <Marked_if_reach_1(true,x,y,edge(u,v,i),h) , Marked_if_reach_2(
                                                       eq(y,v),x,y,edge(u,v,i),
                                                       h)>
}

{  <Marked_union(edge(x,y,i),h) , Marked_union(i,h)> 
      --> <Marked_union(edge(x,y,i),h) , Marked_union(i,h)>
}

{  <Marked_eq(s(x),s(y)) , Marked_eq(x,y)> 
      --> <Marked_eq(s(x),s(y)) , Marked_eq(x,y)>
}
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)) ;
  reach(x,y,empty,h) >= false ;
  reach(x,y,edge(u,v,i),h) >= if_reach_1(eq(x,u),x,y,edge(u,v,i),h) ;
  if_reach_1(true,x,y,edge(u,v,i),h) >= if_reach_2(eq(y,v),x,y,edge(u,v,i),h) ;
  if_reach_1(false,x,y,edge(u,v,i),h) >= reach(x,y,i,edge(u,v,h)) ;
  if_reach_2(true,x,y,edge(u,v,i),h) >= true ;
  if_reach_2(false,x,y,edge(u,v,i),h) >= or(reach(x,y,i,h),
                                          reach(v,y,union(i,h),empty)) ;
  Marked_if_reach_1(true,x,y,edge(u,v,i),h) >= Marked_if_reach_2(eq(y,v),
                                                x,y,edge(u,v,i),h) ;
  Marked_if_reach_1(false,x,y,edge(u,v,i),h) >= Marked_reach(x,y,i,edge(u,v,h)) ;
  Marked_reach(x,y,edge(u,v,i),h) >= Marked_if_reach_1(eq(x,u),x,y,edge(u,v,i),
                                      h) ;
  Marked_if_reach_2(false,x,y,edge(u,v,i),h) >= Marked_reach(v,y,union(i,h),
                                                 empty) ;
  Marked_if_reach_2(false,x,y,edge(u,v,i),h) >= Marked_reach(x,y,i,h) ;
 }
 + Disjunctions:{ 
{
  Marked_if_reach_1(true,x,y,edge(u,v,i),h) > Marked_if_reach_2(eq(y,v),
                                               x,y,edge(u,v,i),h) ;
 }
{
  Marked_if_reach_1(false,x,y,edge(u,v,i),h) > Marked_reach(x,y,i,edge(u,v,h)) ;
 }
{
  Marked_reach(x,y,edge(u,v,i),h) > Marked_if_reach_1(eq(x,u),x,y,edge(u,v,i),
                                     h) ;
 }
{
  Marked_if_reach_2(false,x,y,edge(u,v,i),h) > Marked_reach(v,y,union(i,h),
                                                empty) ;
 }
{
  Marked_if_reach_2(false,x,y,edge(u,v,i),h) > Marked_reach(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
Sat solver result read
=== STOPING TIMER real ===
=== STOPING TIMER virtual ===
constraint: eq(0,0) >= true
constraint: eq(0,s(x)) >= false
constraint: eq(s(x),0) >= false
constraint: eq(s(x),s(y)) >= eq(x,y)
constraint: or(true,y) >= true
constraint: or(false,y) >= y
constraint: union(empty,h) >= h
constraint: union(edge(x,y,i),h) >= edge(x,y,union(i,h))
constraint: reach(x,y,empty,h) >= false
constraint: reach(x,y,edge(u,v,i),h) >= if_reach_1(eq(x,u),x,y,edge(u,v,i),h)
constraint: if_reach_1(true,x,y,edge(u,v,i),h) >= if_reach_2(eq(y,v),
                                                   x,y,edge(u,v,i),h)
constraint: if_reach_1(false,x,y,edge(u,v,i),h) >= reach(x,y,i,edge(u,v,h))
constraint: if_reach_2(true,x,y,edge(u,v,i),h) >= true
constraint: if_reach_2(false,x,y,edge(u,v,i),h) >= or(reach(x,y,i,h),
                                                    reach(v,y,union(i,h),empty))
constraint: Marked_if_reach_1(true,x,y,edge(u,v,i),h) >= Marked_if_reach_2(
                                                          eq(y,v),x,y,
                                                          edge(u,v,i),
                                                          h)
constraint: Marked_if_reach_1(false,x,y,edge(u,v,i),h) >= Marked_reach(
                                                           x,y,i,edge(u,v,h))
constraint: Marked_reach(x,y,edge(u,v,i),h) >= Marked_if_reach_1(eq(x,u),
                                                x,y,edge(u,v,i),h)
constraint: Marked_if_reach_2(false,x,y,edge(u,v,i),h) >= Marked_reach(
                                                           v,y,union(i,h),
                                                           empty)
constraint: Marked_if_reach_2(false,x,y,edge(u,v,i),h) >= Marked_reach(x,y,i,h)
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)) ;
  reach(x,y,empty,h) >= false ;
  reach(x,y,edge(u,v,i),h) >= if_reach_1(eq(x,u),x,y,edge(u,v,i),h) ;
  if_reach_1(true,x,y,edge(u,v,i),h) >= if_reach_2(eq(y,v),x,y,edge(u,v,i),h) ;
  if_reach_1(false,x,y,edge(u,v,i),h) >= reach(x,y,i,edge(u,v,h)) ;
  if_reach_2(true,x,y,edge(u,v,i),h) >= true ;
  if_reach_2(false,x,y,edge(u,v,i),h) >= or(reach(x,y,i,h),
                                          reach(v,y,union(i,h),empty)) ;
  Marked_union(edge(x,y,i),h) >= Marked_union(i,h) ;
 }
 + Disjunctions:{ 
{
  Marked_union(edge(x,y,i),h) > Marked_union(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
Sat solver result read
=== STOPING TIMER real ===
=== STOPING TIMER virtual ===
constraint: eq(0,0) >= true
constraint: eq(0,s(x)) >= false
constraint: eq(s(x),0) >= false
constraint: eq(s(x),s(y)) >= eq(x,y)
constraint: or(true,y) >= true
constraint: or(false,y) >= y
constraint: union(empty,h) >= h
constraint: union(edge(x,y,i),h) >= edge(x,y,union(i,h))
constraint: reach(x,y,empty,h) >= false
constraint: reach(x,y,edge(u,v,i),h) >= if_reach_1(eq(x,u),x,y,edge(u,v,i),h)
constraint: if_reach_1(true,x,y,edge(u,v,i),h) >= if_reach_2(eq(y,v),
                                                   x,y,edge(u,v,i),h)
constraint: if_reach_1(false,x,y,edge(u,v,i),h) >= reach(x,y,i,edge(u,v,h))
constraint: if_reach_2(true,x,y,edge(u,v,i),h) >= true
constraint: if_reach_2(false,x,y,edge(u,v,i),h) >= or(reach(x,y,i,h),
                                                    reach(v,y,union(i,h),empty))
constraint: Marked_union(edge(x,y,i),h) >= Marked_union(i,h)
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)) ;
  reach(x,y,empty,h) >= false ;
  reach(x,y,edge(u,v,i),h) >= if_reach_1(eq(x,u),x,y,edge(u,v,i),h) ;
  if_reach_1(true,x,y,edge(u,v,i),h) >= if_reach_2(eq(y,v),x,y,edge(u,v,i),h) ;
  if_reach_1(false,x,y,edge(u,v,i),h) >= reach(x,y,i,edge(u,v,h)) ;
  if_reach_2(true,x,y,edge(u,v,i),h) >= true ;
  if_reach_2(false,x,y,edge(u,v,i),h) >= or(reach(x,y,i,h),
                                          reach(v,y,union(i,h),empty)) ;
  Marked_eq(s(x),s(y)) >= Marked_eq(x,y) ;
 }
 + Disjunctions:{ 
{
  Marked_eq(s(x),s(y)) > Marked_eq(x,y) ;
 }
 } 
=== 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
Sat solver result read
=== STOPING TIMER real ===
=== STOPING TIMER virtual ===
constraint: eq(0,0) >= true
constraint: eq(0,s(x)) >= false
constraint: eq(s(x),0) >= false
constraint: eq(s(x),s(y)) >= eq(x,y)
constraint: or(true,y) >= true
constraint: or(false,y) >= y
constraint: union(empty,h) >= h
constraint: union(edge(x,y,i),h) >= edge(x,y,union(i,h))
constraint: reach(x,y,empty,h) >= false
constraint: reach(x,y,edge(u,v,i),h) >= if_reach_1(eq(x,u),x,y,edge(u,v,i),h)
constraint: if_reach_1(true,x,y,edge(u,v,i),h) >= if_reach_2(eq(y,v),
                                                   x,y,edge(u,v,i),h)
constraint: if_reach_1(false,x,y,edge(u,v,i),h) >= reach(x,y,i,edge(u,v,h))
constraint: if_reach_2(true,x,y,edge(u,v,i),h) >= true
constraint: if_reach_2(false,x,y,edge(u,v,i),h) >= or(reach(x,y,i,h),
                                                    reach(v,y,union(i,h),empty))
constraint: Marked_eq(s(x),s(y)) >= Marked_eq(x,y)
APPLY CRITERIA (Graph splitting)
Found 1 components:

{  <Marked_if_reach_1(false,x,y,edge(u,v,i),h) , Marked_reach(x,y,i,
                                                  edge(u,v,h))> 
      --> <Marked_reach(x,y,edge(u,v,i),h) , Marked_if_reach_1(eq(x,u),
                                              x,y,edge(u,v,i),h)>
  <Marked_if_reach_2(false,x,y,edge(u,v,i),h) , Marked_reach(v,y,union(i,h),
                                                 empty)> 
     --> <Marked_reach(x,y,edge(u,v,i),h) , Marked_if_reach_1(eq(x,u),
                                             x,y,edge(u,v,i),h)>
  <Marked_if_reach_1(true,x,y,edge(u,v,i),h) , Marked_if_reach_2(eq(y,v),
                                                x,y,edge(u,v,i),h)> 
     --> <Marked_if_reach_2(false,x,y,edge(u,v,i),h) , Marked_reach(v,
                                                        y,union(i,h),
                                                        empty)>
  <Marked_reach(x,y,edge(u,v,i),h) , Marked_if_reach_1(eq(x,u),x,y,edge(u,v,i),
                                      h)> 
     --> <Marked_if_reach_1(false,x,y,edge(u,v,i),h) , Marked_reach(x,
                                                        y,i,edge(u,v,h))>
  <Marked_reach(x,y,edge(u,v,i),h) , Marked_if_reach_1(eq(x,u),x,y,edge(u,v,i),
                                      h)> 
     --> <Marked_if_reach_1(true,x,y,edge(u,v,i),h) , Marked_if_reach_2(
                                                       eq(y,v),x,y,edge(u,v,i),
                                                       h)>
}
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)) ;
  reach(x,y,empty,h) >= false ;
  reach(x,y,edge(u,v,i),h) >= if_reach_1(eq(x,u),x,y,edge(u,v,i),h) ;
  if_reach_1(true,x,y,edge(u,v,i),h) >= if_reach_2(eq(y,v),x,y,edge(u,v,i),h) ;
  if_reach_1(false,x,y,edge(u,v,i),h) >= reach(x,y,i,edge(u,v,h)) ;
  if_reach_2(true,x,y,edge(u,v,i),h) >= true ;
  if_reach_2(false,x,y,edge(u,v,i),h) >= or(reach(x,y,i,h),
                                          reach(v,y,union(i,h),empty)) ;
  Marked_if_reach_1(true,x,y,edge(u,v,i),h) >= Marked_if_reach_2(eq(y,v),
                                                x,y,edge(u,v,i),h) ;
  Marked_if_reach_1(false,x,y,edge(u,v,i),h) >= Marked_reach(x,y,i,edge(u,v,h)) ;
  Marked_reach(x,y,edge(u,v,i),h) >= Marked_if_reach_1(eq(x,u),x,y,edge(u,v,i),
                                      h) ;
  Marked_if_reach_2(false,x,y,edge(u,v,i),h) >= Marked_reach(v,y,union(i,h),
                                                 empty) ;
 }
 + Disjunctions:{ 
{
  Marked_if_reach_1(true,x,y,edge(u,v,i),h) > Marked_if_reach_2(eq(y,v),
                                               x,y,edge(u,v,i),h) ;
 }
{
  Marked_if_reach_1(false,x,y,edge(u,v,i),h) > Marked_reach(x,y,i,edge(u,v,h)) ;
 }
{
  Marked_reach(x,y,edge(u,v,i),h) > Marked_if_reach_1(eq(x,u),x,y,edge(u,v,i),
                                     h) ;
 }
{
  Marked_if_reach_2(false,x,y,edge(u,v,i),h) > Marked_reach(v,y,union(i,h),
                                                empty) ;
 }
 } 
=== 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
Sat solver result read
=== STOPING TIMER real ===
=== STOPING TIMER virtual ===
constraint: eq(0,0) >= true
constraint: eq(0,s(x)) >= false
constraint: eq(s(x),0) >= false
constraint: eq(s(x),s(y)) >= eq(x,y)
constraint: or(true,y) >= true
constraint: or(false,y) >= y
constraint: union(empty,h) >= h
constraint: union(edge(x,y,i),h) >= edge(x,y,union(i,h))
constraint: reach(x,y,empty,h) >= false
constraint: reach(x,y,edge(u,v,i),h) >= if_reach_1(eq(x,u),x,y,edge(u,v,i),h)
constraint: if_reach_1(true,x,y,edge(u,v,i),h) >= if_reach_2(eq(y,v),
                                                   x,y,edge(u,v,i),h)
constraint: if_reach_1(false,x,y,edge(u,v,i),h) >= reach(x,y,i,edge(u,v,h))
constraint: if_reach_2(true,x,y,edge(u,v,i),h) >= true
constraint: if_reach_2(false,x,y,edge(u,v,i),h) >= or(reach(x,y,i,h),
                                                    reach(v,y,union(i,h),empty))
constraint: Marked_if_reach_1(true,x,y,edge(u,v,i),h) >= Marked_if_reach_2(
                                                          eq(y,v),x,y,
                                                          edge(u,v,i),
                                                          h)
constraint: Marked_if_reach_1(false,x,y,edge(u,v,i),h) >= Marked_reach(
                                                           x,y,i,edge(u,v,h))
constraint: Marked_reach(x,y,edge(u,v,i),h) >= Marked_if_reach_1(eq(x,u),
                                                x,y,edge(u,v,i),h)
constraint: Marked_if_reach_2(false,x,y,edge(u,v,i),h) >= Marked_reach(
                                                           v,y,union(i,h),
                                                           empty)
APPLY CRITERIA (Graph splitting)
Found 1 components:

{  <Marked_if_reach_1(false,x,y,edge(u,v,i),h) , Marked_reach(x,y,i,
                                                  edge(u,v,h))> 
      --> <Marked_reach(x,y,edge(u,v,i),h) , Marked_if_reach_1(eq(x,u),
                                              x,y,edge(u,v,i),h)>
  <Marked_reach(x,y,edge(u,v,i),h) , Marked_if_reach_1(eq(x,u),x,y,edge(u,v,i),
                                      h)> 
     --> <Marked_if_reach_1(false,x,y,edge(u,v,i),h) , Marked_reach(x,
                                                        y,i,edge(u,v,h))>
}
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)) ;
  reach(x,y,empty,h) >= false ;
  reach(x,y,edge(u,v,i),h) >= if_reach_1(eq(x,u),x,y,edge(u,v,i),h) ;
  if_reach_1(true,x,y,edge(u,v,i),h) >= if_reach_2(eq(y,v),x,y,edge(u,v,i),h) ;
  if_reach_1(false,x,y,edge(u,v,i),h) >= reach(x,y,i,edge(u,v,h)) ;
  if_reach_2(true,x,y,edge(u,v,i),h) >= true ;
  if_reach_2(false,x,y,edge(u,v,i),h) >= or(reach(x,y,i,h),
                                          reach(v,y,union(i,h),empty)) ;
  Marked_if_reach_1(false,x,y,edge(u,v,i),h) >= Marked_reach(x,y,i,edge(u,v,h)) ;
  Marked_reach(x,y,edge(u,v,i),h) >= Marked_if_reach_1(eq(x,u),x,y,edge(u,v,i),
                                      h) ;
 }
 + Disjunctions:{ 
{
  Marked_if_reach_1(false,x,y,edge(u,v,i),h) > Marked_reach(x,y,i,edge(u,v,h)) ;
 }
{
  Marked_reach(x,y,edge(u,v,i),h) > Marked_if_reach_1(eq(x,u),x,y,edge(u,v,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
Sat solver result read
=== STOPING TIMER real ===
=== STOPING TIMER virtual ===
constraint: eq(0,0) >= true
constraint: eq(0,s(x)) >= false
constraint: eq(s(x),0) >= false
constraint: eq(s(x),s(y)) >= eq(x,y)
constraint: or(true,y) >= true
constraint: or(false,y) >= y
constraint: union(empty,h) >= h
constraint: union(edge(x,y,i),h) >= edge(x,y,union(i,h))
constraint: reach(x,y,empty,h) >= false
constraint: reach(x,y,edge(u,v,i),h) >= if_reach_1(eq(x,u),x,y,edge(u,v,i),h)
constraint: if_reach_1(true,x,y,edge(u,v,i),h) >= if_reach_2(eq(y,v),
                                                   x,y,edge(u,v,i),h)
constraint: if_reach_1(false,x,y,edge(u,v,i),h) >= reach(x,y,i,edge(u,v,h))
constraint: if_reach_2(true,x,y,edge(u,v,i),h) >= true
constraint: if_reach_2(false,x,y,edge(u,v,i),h) >= or(reach(x,y,i,h),
                                                    reach(v,y,union(i,h),empty))
constraint: Marked_if_reach_1(false,x,y,edge(u,v,i),h) >= Marked_reach(
                                                           x,y,i,edge(u,v,h))
constraint: Marked_reach(x,y,edge(u,v,i),h) >= Marked_if_reach_1(eq(x,u),
                                                x,y,edge(u,v,i),h)
APPLY CRITERIA (Graph splitting)
Found 0 components:
APPLY CRITERIA (Graph splitting)
Found 0 components:
APPLY CRITERIA (Graph splitting)
Found 0 components:
SOLVED
{
 
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] reach(x,y,empty,h) -> false
[10] reach(x,y,edge(u,v,i),h) -> if_reach_1(eq(x,u),x,y,edge(u,v,i),h)
[11] if_reach_1(true,x,y,edge(u,v,i),h) ->
 if_reach_2(eq(y,v),x,y,edge(u,v,i),h)
[12] if_reach_2(true,x,y,edge(u,v,i),h) -> true
[13] if_reach_2(false,x,y,edge(u,v,i),h) ->
 or(reach(x,y,i,h),reach(v,y,union(i,h),empty))
[14] if_reach_1(false,x,y,edge(u,v,i),h) -> reach(x,y,i,edge(u,v,h))
 ,
 CRITERION: MDP
 [ {
      
     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,edge(u,v,i),h) , Marked_if_reach_1(eq(x,u),x,y,edge(u,v,i),h)>
<Marked_reach(x,y,edge(u,v,i),h) , Marked_eq(x,u)>
<Marked_if_reach_1(true,x,y,edge(u,v,i),h) , Marked_if_reach_2(eq(y,v),
                                              x,y,edge(u,v,i),h)>
<Marked_if_reach_1(true,x,y,edge(u,v,i),h) , Marked_eq(y,v)>
<Marked_if_reach_2(false,x,y,edge(u,v,i),h) , Marked_or(reach(x,y,i,h),
                                               reach(v,y,union(i,h),empty))>
<Marked_if_reach_2(false,x,y,edge(u,v,i),h) , Marked_reach(x,y,i,h)>
<Marked_if_reach_2(false,x,y,edge(u,v,i),h) , Marked_reach(v,y,union(i,h),
                                               empty)>
<Marked_if_reach_2(false,x,y,edge(u,v,i),h) , Marked_union(i,h)>
<Marked_if_reach_1(false,x,y,edge(u,v,i),h) , Marked_reach(x,y,i,edge(u,v,h))>
 ,
 CRITERION: SG
 [ {
      
     DP termination of:
     <Marked_reach(x,y,edge(u,v,i),h) , Marked_if_reach_1(eq(x,u),x,y,
                                         edge(u,v,i),h)>
<Marked_if_reach_1(true,x,y,edge(u,v,i),h) , Marked_if_reach_2(eq(y,v),
                                              x,y,edge(u,v,i),h)>
<Marked_if_reach_2(false,x,y,edge(u,v,i),h) , Marked_reach(x,y,i,h)>
<Marked_if_reach_2(false,x,y,edge(u,v,i),h) , Marked_reach(v,y,union(i,h),
                                               empty)>
<Marked_if_reach_1(false,x,y,edge(u,v,i),h) , Marked_reach(x,y,i,edge(u,v,h))>
 ,
 CRITERION: CG using polynomial interpretation = 
 [ true ] () = 0; 
 [ edge ] (X0,X1,X2) = 1*X2 + 2; 
 [ s ] (X0) = 3*X0; 
 [ Marked_if_reach_1 ] (X0,X1,X2,X3,X4) = 2*X4 + 2*X3 + 3*X2; 
 [ 0 ] () = 0; 
 [ if_reach_1 ] (X0,X1,X2,X3,X4) = 0; 
 [ union ] (X0,X1) = 1*X1 + 1*X0; 
 [ Marked_if_reach_2 ] (X0,X1,X2,X3,X4) = 2*X4 + 2*X3 + 3*X2; 
 [ eq ] (X0,X1) = 0; 
 [ reach ] (X0,X1,X2,X3) = 0; 
 [ or ] (X0,X1) = 2*X1; 
 [ Marked_reach ] (X0,X1,X2,X3) = 2*X3 + 2*X2 + 3*X1; 
 [ false ] () = 0; 
 [ if_reach_2 ] (X0,X1,X2,X3,X4) = 0; 
 [ empty ] () = 2; 
 removing <Marked_if_reach_2(false,x,y,edge(u,v,i),h),Marked_reach(x,y,i,h)>
 [ {
      
     DP termination of:
     <Marked_reach(x,y,edge(u,v,i),h) , Marked_if_reach_1(eq(x,u),x,y,
                                         edge(u,v,i),h)>
<Marked_if_reach_1(true,x,y,edge(u,v,i),h) , Marked_if_reach_2(eq(y,v),
                                              x,y,edge(u,v,i),h)>
<Marked_if_reach_2(false,x,y,edge(u,v,i),h) , Marked_reach(v,y,union(i,h),
                                               empty)>
<Marked_if_reach_1(false,x,y,edge(u,v,i),h) , Marked_reach(x,y,i,edge(u,v,h))>
 ,
 CRITERION: SG
 [ {
      
     DP termination of:
     <Marked_reach(x,y,edge(u,v,i),h) , Marked_if_reach_1(eq(x,u),x,y,
                                         edge(u,v,i),h)>
<Marked_if_reach_1(true,x,y,edge(u,v,i),h) , Marked_if_reach_2(eq(y,v),
                                              x,y,edge(u,v,i),h)>
<Marked_if_reach_2(false,x,y,edge(u,v,i),h) , Marked_reach(v,y,union(i,h),
                                               empty)>
<Marked_if_reach_1(false,x,y,edge(u,v,i),h) , Marked_reach(x,y,i,edge(u,v,h))>
 ,
 CRITERION: CG using polynomial interpretation = 
 [ true ] () = 0; 
 [ edge ] (X0,X1,X2) = 1*X2 + 1; 
 [ s ] (X0) = 3*X0; 
 [ Marked_if_reach_1 ] (X0,X1,X2,X3,X4) = 2*X4 + 2*X3 + 3*X2 + 2; 
 [ 0 ] () = 0; 
 [ if_reach_1 ] (X0,X1,X2,X3,X4) = 0; 
 [ union ] (X0,X1) = 1*X1 + 1*X0; 
 [ Marked_if_reach_2 ] (X0,X1,X2,X3,X4) = 2*X4 + 2*X3 + 3*X2; 
 [ eq ] (X0,X1) = 0; 
 [ reach ] (X0,X1,X2,X3) = 0; 
 [ or ] (X0,X1) = 2*X1; 
 [ Marked_reach ] (X0,X1,X2,X3) = 2*X3 + 2*X2 + 3*X1 + 2; 
 [ false ] () = 0; 
 [ if_reach_2 ] (X0,X1,X2,X3,X4) = 0; 
 [ empty ] () = 0; 
 removing <Marked_if_reach_1(true,x,y,edge(u,v,i),h),Marked_if_reach_2(
                                                      eq(y,v),x,y,edge(u,v,i),
                                                      h)>
 [ {
      
     DP termination of:
     <Marked_reach(x,y,edge(u,v,i),h) , Marked_if_reach_1(eq(x,u),x,y,
                                         edge(u,v,i),h)>
<Marked_if_reach_2(false,x,y,edge(u,v,i),h) , Marked_reach(v,y,union(i,h),
                                               empty)>
<Marked_if_reach_1(false,x,y,edge(u,v,i),h) , Marked_reach(x,y,i,edge(u,v,h))>
 ,
 CRITERION: SG
 [ {
      
     DP termination of:
     <Marked_reach(x,y,edge(u,v,i),h) , Marked_if_reach_1(eq(x,u),x,y,
                                         edge(u,v,i),h)>
<Marked_if_reach_1(false,x,y,edge(u,v,i),h) , Marked_reach(x,y,i,edge(u,v,h))>
 ,
 CRITERION: CG using polynomial interpretation = 
 [ true ] () = 0; 
 [ edge ] (X0,X1,X2) = 1*X2 + 2; 
 [ s ] (X0) = 3*X0; 
 [ Marked_if_reach_1 ] (X0,X1,X2,X3,X4) = 1*X3 + 3*X2 + 3*X1 + 1; 
 [ 0 ] () = 0; 
 [ if_reach_1 ] (X0,X1,X2,X3,X4) = 0; 
 [ union ] (X0,X1) = 2*X1 + 2*X0; 
 [ eq ] (X0,X1) = 0; 
 [ reach ] (X0,X1,X2,X3) = 0; 
 [ or ] (X0,X1) = 2*X1; 
 [ Marked_reach ] (X0,X1,X2,X3) = 1*X2 + 3*X1 + 3*X0 + 3; 
 [ false ] () = 0; 
 [ if_reach_2 ] (X0,X1,X2,X3,X4) = 0; 
 [ empty ] () = 0; 
 removing <Marked_reach(x,y,edge(u,v,i),h),Marked_if_reach_1(eq(x,u),
                                            x,y,edge(u,v,i),h)>
 [ {
      
     DP termination of:
     <Marked_if_reach_1(false,x,y,edge(u,v,i),h) , Marked_reach(x,y,i,
                                                    edge(u,v,h))>
 ,
 CRITERION: SG
 [  ]} 
 ]} 
 ]} 
 ]} 
 ]} 
 ]} 
{
 
DP termination of:
<Marked_union(edge(x,y,i),h) , Marked_union(i,h)>
 ,
 CRITERION: ORD
 [ 
     Solution found:
     polynomial interpretation = 
      [ true ] () = 0; 
 [ Marked_union ] (X0,X1) = 3*X0 + 0; 
 [ edge ] (X0,X1,X2) = 1 + 1*X2 + 0; 
 [ s ] (X0) = 3*X0 + 0; 
 [ 0 ] () = 0; 
 [ if_reach_1 ] (X0,X1,X2,X3,X4) = 0; 
 [ union ] (X0,X1) = 1*X0 + 2*X1 + 0; 
 [ eq ] (X0,X1) = 0; 
 [ reach ] (X0,X1,X2,X3) = 0; 
 [ or ] (X0,X1) = 2*X1 + 0; 
 [ false ] () = 0; 
 [ if_reach_2 ] (X0,X1,X2,X3,X4) = 0; 
 [ empty ] () = 0; 
 ]} 
{
 
DP termination of:
<Marked_eq(s(x),s(y)) , Marked_eq(x,y)>
 ,
 CRITERION: ORD
 [ 
     Solution found:
     polynomial interpretation = 
      [ true ] () = 0; 
 [ edge ] (X0,X1,X2) = 2 + 0; 
 [ s ] (X0) = 1 + 3*X0 + 0; 
 [ 0 ] () = 0; 
 [ if_reach_1 ] (X0,X1,X2,X3,X4) = 0; 
 [ union ] (X0,X1) = 2*X0 + 1*X1 + 0; 
 [ eq ] (X0,X1) = 0; 
 [ Marked_eq ] (X0,X1) = 1*X0 + 0; 
 [ reach ] (X0,X1,X2,X3) = 0; 
 [ or ] (X0,X1) = 1*X1 + 0; 
 [ false ] () = 0; 
 [ if_reach_2 ] (X0,X1,X2,X3,X4) = 0; 
 [ empty ] () = 0; 
 ]} 
 ]} 
 ]} 

Cime worked for 0.489260 seconds (real time)
Cime Exit Status: 0