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

TRS termination of:
[1] f1(a,x) -> g1(x,x)
[2] f1(x,a) -> g2(x,x)
[3] f2(a,x) -> g1(x,x)
[4] f2(x,a) -> g2(x,x)
[5] g1(a,x) -> h1(x)
[6] g1(x,a) -> h2(x)
[7] g2(a,x) -> h1(x)
[8] g2(x,a) -> h2(x)
[9] h1(a) -> i
[10] h2(a) -> i
[11] e1(h1(w),h2(w),x,y,z,w) -> e2(x,x,y,z,z,w)
[12] e1(x1,x1,x,y,z,a) -> e5(x1,x,y,z)
[13] e2(f1(w,w),x,y,z,f2(w,w),w) -> e3(x,y,x,y,y,z,y,z,x,y,z,w)
[14] e2(x,x,y,z,z,a) -> e6(x,y,z)
[15] e2(i,x,y,z,i,a) -> e6(x,y,z)
[16] e3(x1,x1,x2,x2,x3,x3,x4,x4,x,y,z,w) -> e4(x1,x1,x2,x2,x3,x3,x4,x4,x,y,z,w)
[17] e3(x,y,x,y,y,z,y,z,x,y,z,a) -> e6(x,y,z)
[18] e4(g1(w,w),x1,g2(w,w),x1,g1(w,w),x1,g2(w,w),x1,x,y,z,w) ->
 e1(x1,x1,x,y,z,w)
[19] e4(i,x1,i,x1,i,x1,i,x1,x,y,z,a) -> e5(x1,x,y,z)
[20] e4(x,x,x,x,x,x,x,x,x,x,x,a) -> e6(x,x,x)
[21] e5(i,x,y,z) -> e6(x,y,z)


Sub problem: 
guided: 

DP termination of:
<Marked_f1(a,x) , Marked_g1(x,x)>
<Marked_f1(x,a) , Marked_g2(x,x)>
<Marked_f2(a,x) , Marked_g1(x,x)>
<Marked_f2(x,a) , Marked_g2(x,x)>
<Marked_g1(a,x) , Marked_h1(x)>
<Marked_g1(x,a) , Marked_h2(x)>
<Marked_g2(a,x) , Marked_h1(x)>
<Marked_g2(x,a) , Marked_h2(x)>
<Marked_e1(h1(w),h2(w),x,y,z,w) , Marked_e2(x,x,y,z,z,w)>
<Marked_e1(x1,x1,x,y,z,a) , Marked_e5(x1,x,y,z)>
<Marked_e2(f1(w,w),x,y,z,f2(w,w),w) , Marked_e3(x,y,x,y,y,z,y,z,x,y,z,w)>
<Marked_e3(x1,x1,x2,x2,x3,x3,x4,x4,x,y,z,w) , Marked_e4(x1,x1,x2,x2,x3,
                                               x3,x4,x4,x,y,z,w)>
<Marked_e4(g1(w,w),x1,g2(w,w),x1,g1(w,w),x1,g2(w,w),x1,x,y,z,w) , Marked_e1(
                                                                   x1,
                                                                   x1,
                                                                   x,
                                                                   y,
                                                                   z,
                                                                   w)>
<Marked_e4(i,x1,i,x1,i,x1,i,x1,x,y,z,a) , Marked_e5(x1,x,y,z)>
 
END GUIDED
APPLY CRITERIA (Graph splitting)
Found 1 components:

{  <Marked_e4(g1(w,w),x1,g2(w,w),x1,g1(w,w),x1,g2(w,w),x1,x,y,z,w) , Marked_e1(
                                                                    x1,
                                                                    x1,
                                                                    x,y,
                                                                    z,w)> 
      --> <Marked_e1(h1(w),h2(w),x,y,z,w) , Marked_e2(x,x,y,z,z,w)>
  <Marked_e3(x1,x1,x2,x2,x3,x3,x4,x4,x,y,z,w) , Marked_e4(x1,x1,x2,x2,
                                                 x3,x3,x4,x4,x,y,z,w)> 
     --> <Marked_e4(g1(w,w),x1,g2(w,w),x1,g1(w,w),x1,g2(w,w),x1,x,y,z,w) , Marked_e1(
                                                                    x1,x1,x,y,
                                                                    z,w)>
  <Marked_e2(f1(w,w),x,y,z,f2(w,w),w) , Marked_e3(x,y,x,y,y,z,y,z,x,y,z,w)> 
     --> <Marked_e3(x1,x1,x2,x2,x3,x3,x4,x4,x,y,z,w) , Marked_e4(x1,x1,
                                                        x2,x2,x3,x3,x4,
                                                        x4,x,y,z,w)>
  <Marked_e1(h1(w),h2(w),x,y,z,w) , Marked_e2(x,x,y,z,z,w)> 
     --> <Marked_e2(f1(w,w),x,y,z,f2(w,w),w) , Marked_e3(x,y,x,y,y,z,
                                                y,z,x,y,z,w)>
}
APPLY CRITERIA (Choosing graph)
Trying to solve the following constraints:
{
  g1(a,x) >= h1(x) ;
  g1(x,a) >= h2(x) ;
  f1(a,x) >= g1(x,x) ;
  f1(x,a) >= g2(x,x) ;
  g2(a,x) >= h1(x) ;
  g2(x,a) >= h2(x) ;
  f2(a,x) >= g1(x,x) ;
  f2(x,a) >= g2(x,x) ;
  h1(a) >= i ;
  h2(a) >= i ;
  e2(f1(w,w),x,y,z,f2(w,w),w) >= e3(x,y,x,y,y,z,y,z,x,y,z,w) ;
  e2(i,x,y,z,i,a) >= e6(x,y,z) ;
  e2(x,x,y,z,z,a) >= e6(x,y,z) ;
  e1(h1(w),h2(w),x,y,z,w) >= e2(x,x,y,z,z,w) ;
  e1(x1,x1,x,y,z,a) >= e5(x1,x,y,z) ;
  e5(i,x,y,z) >= e6(x,y,z) ;
  e3(x,y,x,y,y,z,y,z,x,y,z,a) >= e6(x,y,z) ;
  e3(x1,x1,x2,x2,x3,x3,x4,x4,x,y,z,w) >= e4(x1,x1,x2,x2,x3,x3,x4,x4,x,y,z,w) ;
  e4(g1(w,w),x1,g2(w,w),x1,g1(w,w),x1,g2(w,w),x1,x,y,z,w) >= e1(x1,x1,x,y,z,w) ;
  e4(i,x1,i,x1,i,x1,i,x1,x,y,z,a) >= e5(x1,x,y,z) ;
  e4(x,x,x,x,x,x,x,x,x,x,x,a) >= e6(x,x,x) ;
  Marked_e4(g1(w,w),x1,g2(w,w),x1,g1(w,w),x1,g2(w,w),x1,x,y,z,w) >= Marked_e1(
                                                                    x1,
                                                                    x1,
                                                                    x,
                                                                    y,
                                                                    z,
                                                                    w) ;
  Marked_e1(h1(w),h2(w),x,y,z,w) >= Marked_e2(x,x,y,z,z,w) ;
  Marked_e3(x1,x1,x2,x2,x3,x3,x4,x4,x,y,z,w) >= Marked_e4(x1,x1,x2,x2,
                                                 x3,x3,x4,x4,x,y,z,w) ;
  Marked_e2(f1(w,w),x,y,z,f2(w,w),w) >= Marked_e3(x,y,x,y,y,z,y,z,x,y,z,w) ;
 }
 + Disjunctions:{ 
{
  Marked_e4(g1(w,w),x1,g2(w,w),x1,g1(w,w),x1,g2(w,w),x1,x,y,z,w) > Marked_e1(
                                                                    x1,
                                                                    x1,
                                                                    x,
                                                                    y,
                                                                    z,
                                                                    w) ;
 }
{
  Marked_e1(h1(w),h2(w),x,y,z,w) > Marked_e2(x,x,y,z,z,w) ;
 }
{
  Marked_e3(x1,x1,x2,x2,x3,x3,x4,x4,x,y,z,w) > Marked_e4(x1,x1,x2,x2,
                                                x3,x3,x4,x4,x,y,z,w) ;
 }
{
  Marked_e2(f1(w,w),x,y,z,f2(w,w),w) > Marked_e3(x,y,x,y,y,z,y,z,x,y,z,w) ;
 }
 } 
=== 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 41.058134 seconds (real time)
Cime Exit Status: 0