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

TRS termination of:
[1] and(true,y) -> y
[2] and(false,y) -> false
[3] eq(nil,nil) -> true
[4] eq(cons(t,l),nil) -> false
[5] eq(nil,cons(t,l)) -> false
[6] eq(cons(t,l),cons(t',l')) -> and(eq(t,t'),eq(l,l'))
[7] eq(var(l),var(l')) -> eq(l,l')
[8] eq(var(l),apply(t,s)) -> false
[9] eq(var(l),lambda(x,t)) -> false
[10] eq(apply(t,s),var(l)) -> false
[11] eq(apply(t,s),apply(t',s')) -> and(eq(t,t'),eq(s,s'))
[12] eq(apply(t,s),lambda(x,t)) -> false
[13] eq(lambda(x,t),var(l)) -> false
[14] eq(lambda(x,t),apply(t,s)) -> false
[15] eq(lambda(x,t),lambda(x',t')) -> and(eq(x,x'),eq(t,t'))
[16] if(true,var(k),var(l')) -> var(k)
[17] if(false,var(k),var(l')) -> var(l')
[18] ren(var(l),var(k),var(l')) -> if(eq(l,l'),var(k),var(l'))
[19] ren(x,y,apply(t,s)) -> apply(ren(x,y,t),ren(x,y,s))
[20] ren(x,y,lambda(z,t)) ->
 lambda(var(cons(x,cons(y,cons(lambda(z,t),nil)))),
  ren(x,y,ren(z,var(cons(x,cons(y,cons(lambda(z,t),nil)))),t)))


Sub problem: 
guided: 

DP termination of:
<Marked_eq(cons(t,l),cons(t',l')) , Marked_and(eq(t,t'),eq(l,l'))>
<Marked_eq(cons(t,l),cons(t',l')) , Marked_eq(t,t')>
<Marked_eq(cons(t,l),cons(t',l')) , Marked_eq(l,l')>
<Marked_eq(var(l),var(l')) , Marked_eq(l,l')>
<Marked_eq(apply(t,s),apply(t',s')) , Marked_and(eq(t,t'),eq(s,s'))>
<Marked_eq(apply(t,s),apply(t',s')) , Marked_eq(t,t')>
<Marked_eq(apply(t,s),apply(t',s')) , Marked_eq(s,s')>
<Marked_eq(lambda(x,t),lambda(x',t')) , Marked_and(eq(x,x'),eq(t,t'))>
<Marked_eq(lambda(x,t),lambda(x',t')) , Marked_eq(x,x')>
<Marked_eq(lambda(x,t),lambda(x',t')) , Marked_eq(t,t')>
<Marked_ren(var(l),var(k),var(l')) , Marked_if(eq(l,l'),var(k),var(l'))>
<Marked_ren(var(l),var(k),var(l')) , Marked_eq(l,l')>
<Marked_ren(x,y,apply(t,s)) , Marked_ren(x,y,t)>
<Marked_ren(x,y,apply(t,s)) , Marked_ren(x,y,s)>
<Marked_ren(x,y,lambda(z,t)) , Marked_ren(x,y,
                                ren(z,
                                 var(cons(x,cons(y,cons(lambda(z,t),nil)))),
                                 t))>
<Marked_ren(x,y,lambda(z,t)) , Marked_ren(z,
                                var(cons(x,cons(y,cons(lambda(z,t),nil)))),
                                t)>
 
END GUIDED
APPLY CRITERIA (Graph splitting)
Found 2 components:

{  <Marked_ren(x,y,lambda(z,t)) , Marked_ren(z,
                                   var(cons(x,cons(y,cons(lambda(z,t),nil)))),
                                   t)> 
      --> <Marked_ren(x,y,lambda(z,t)) , Marked_ren(z,
                                          var(cons(x,
                                               cons(y,cons(lambda(z,t),nil)))),
                                          t)>
  <Marked_ren(x,y,lambda(z,t)) , Marked_ren(z,
                                  var(cons(x,cons(y,cons(lambda(z,t),nil)))),
                                  t)> 
     --> <Marked_ren(x,y,lambda(z,t)) , Marked_ren(x,y,
                                         ren(z,
                                          var(cons(x,
                                               cons(y,cons(lambda(z,t),nil)))),
                                          t))>
  <Marked_ren(x,y,lambda(z,t)) , Marked_ren(z,
                                  var(cons(x,cons(y,cons(lambda(z,t),nil)))),
                                  t)> 
     --> <Marked_ren(x,y,apply(t,s)) , Marked_ren(x,y,s)>
  <Marked_ren(x,y,lambda(z,t)) , Marked_ren(z,
                                  var(cons(x,cons(y,cons(lambda(z,t),nil)))),
                                  t)> 
     --> <Marked_ren(x,y,apply(t,s)) , Marked_ren(x,y,t)>
  <Marked_ren(x,y,lambda(z,t)) , Marked_ren(x,y,
                                  ren(z,
                                   var(cons(x,cons(y,cons(lambda(z,t),nil)))),
                                   t))> 
     --> <Marked_ren(x,y,lambda(z,t)) , Marked_ren(z,
                                         var(cons(x,
                                              cons(y,cons(lambda(z,t),nil)))),
                                         t)>
  <Marked_ren(x,y,lambda(z,t)) , Marked_ren(x,y,
                                  ren(z,
                                   var(cons(x,cons(y,cons(lambda(z,t),nil)))),
                                   t))> 
     --> <Marked_ren(x,y,lambda(z,t)) , Marked_ren(x,y,
                                         ren(z,
                                          var(cons(x,
                                               cons(y,cons(lambda(z,t),nil)))),
                                          t))>
  <Marked_ren(x,y,lambda(z,t)) , Marked_ren(x,y,
                                  ren(z,
                                   var(cons(x,cons(y,cons(lambda(z,t),nil)))),
                                   t))> 
     --> <Marked_ren(x,y,apply(t,s)) , Marked_ren(x,y,s)>
  <Marked_ren(x,y,lambda(z,t)) , Marked_ren(x,y,
                                  ren(z,
                                   var(cons(x,cons(y,cons(lambda(z,t),nil)))),
                                   t))> 
     --> <Marked_ren(x,y,apply(t,s)) , Marked_ren(x,y,t)>
  <Marked_ren(x,y,apply(t,s)) , Marked_ren(x,y,s)> 
     --> <Marked_ren(x,y,lambda(z,t)) , Marked_ren(z,
                                         var(cons(x,
                                              cons(y,cons(lambda(z,t),nil)))),
                                         t)>
  <Marked_ren(x,y,apply(t,s)) , Marked_ren(x,y,s)> 
     --> <Marked_ren(x,y,lambda(z,t)) , Marked_ren(x,y,
                                         ren(z,
                                          var(cons(x,
                                               cons(y,cons(lambda(z,t),nil)))),
                                          t))>
  <Marked_ren(x,y,apply(t,s)) , Marked_ren(x,y,s)> 
     --> <Marked_ren(x,y,apply(t,s)) , Marked_ren(x,y,s)>
  <Marked_ren(x,y,apply(t,s)) , Marked_ren(x,y,s)> 
     --> <Marked_ren(x,y,apply(t,s)) , Marked_ren(x,y,t)>
  <Marked_ren(x,y,apply(t,s)) , Marked_ren(x,y,t)> 
     --> <Marked_ren(x,y,lambda(z,t)) , Marked_ren(z,
                                         var(cons(x,
                                              cons(y,cons(lambda(z,t),nil)))),
                                         t)>
  <Marked_ren(x,y,apply(t,s)) , Marked_ren(x,y,t)> 
     --> <Marked_ren(x,y,lambda(z,t)) , Marked_ren(x,y,
                                         ren(z,
                                          var(cons(x,
                                               cons(y,cons(lambda(z,t),nil)))),
                                          t))>
  <Marked_ren(x,y,apply(t,s)) , Marked_ren(x,y,t)> 
     --> <Marked_ren(x,y,apply(t,s)) , Marked_ren(x,y,s)>
  <Marked_ren(x,y,apply(t,s)) , Marked_ren(x,y,t)> 
     --> <Marked_ren(x,y,apply(t,s)) , Marked_ren(x,y,t)>
}

{  <Marked_eq(lambda(x,t),lambda(x',t')) , Marked_eq(t,t')> 
      --> <Marked_eq(lambda(x,t),lambda(x',t')) , Marked_eq(t,t')>
  <Marked_eq(lambda(x,t),lambda(x',t')) , Marked_eq(t,t')> 
     --> <Marked_eq(lambda(x,t),lambda(x',t')) , Marked_eq(x,x')>
  <Marked_eq(lambda(x,t),lambda(x',t')) , Marked_eq(t,t')> 
     --> <Marked_eq(apply(t,s),apply(t',s')) , Marked_eq(s,s')>
  <Marked_eq(lambda(x,t),lambda(x',t')) , Marked_eq(t,t')> 
     --> <Marked_eq(apply(t,s),apply(t',s')) , Marked_eq(t,t')>
  <Marked_eq(lambda(x,t),lambda(x',t')) , Marked_eq(t,t')> 
     --> <Marked_eq(var(l),var(l')) , Marked_eq(l,l')>
  <Marked_eq(lambda(x,t),lambda(x',t')) , Marked_eq(t,t')> 
     --> <Marked_eq(cons(t,l),cons(t',l')) , Marked_eq(l,l')>
  <Marked_eq(lambda(x,t),lambda(x',t')) , Marked_eq(t,t')> 
     --> <Marked_eq(cons(t,l),cons(t',l')) , Marked_eq(t,t')>
  <Marked_eq(lambda(x,t),lambda(x',t')) , Marked_eq(x,x')> 
     --> <Marked_eq(lambda(x,t),lambda(x',t')) , Marked_eq(t,t')>
  <Marked_eq(lambda(x,t),lambda(x',t')) , Marked_eq(x,x')> 
     --> <Marked_eq(lambda(x,t),lambda(x',t')) , Marked_eq(x,x')>
  <Marked_eq(lambda(x,t),lambda(x',t')) , Marked_eq(x,x')> 
     --> <Marked_eq(apply(t,s),apply(t',s')) , Marked_eq(s,s')>
  <Marked_eq(lambda(x,t),lambda(x',t')) , Marked_eq(x,x')> 
     --> <Marked_eq(apply(t,s),apply(t',s')) , Marked_eq(t,t')>
  <Marked_eq(lambda(x,t),lambda(x',t')) , Marked_eq(x,x')> 
     --> <Marked_eq(var(l),var(l')) , Marked_eq(l,l')>
  <Marked_eq(lambda(x,t),lambda(x',t')) , Marked_eq(x,x')> 
     --> <Marked_eq(cons(t,l),cons(t',l')) , Marked_eq(l,l')>
  <Marked_eq(lambda(x,t),lambda(x',t')) , Marked_eq(x,x')> 
     --> <Marked_eq(cons(t,l),cons(t',l')) , Marked_eq(t,t')>
  <Marked_eq(apply(t,s),apply(t',s')) , Marked_eq(s,s')> 
     --> <Marked_eq(lambda(x,t),lambda(x',t')) , Marked_eq(t,t')>
  <Marked_eq(apply(t,s),apply(t',s')) , Marked_eq(s,s')> 
     --> <Marked_eq(lambda(x,t),lambda(x',t')) , Marked_eq(x,x')>
  <Marked_eq(apply(t,s),apply(t',s')) , Marked_eq(s,s')> 
     --> <Marked_eq(apply(t,s),apply(t',s')) , Marked_eq(s,s')>
  <Marked_eq(apply(t,s),apply(t',s')) , Marked_eq(s,s')> 
     --> <Marked_eq(apply(t,s),apply(t',s')) , Marked_eq(t,t')>
  <Marked_eq(apply(t,s),apply(t',s')) , Marked_eq(s,s')> 
     --> <Marked_eq(var(l),var(l')) , Marked_eq(l,l')>
  <Marked_eq(apply(t,s),apply(t',s')) , Marked_eq(s,s')> 
     --> <Marked_eq(cons(t,l),cons(t',l')) , Marked_eq(l,l')>
  <Marked_eq(apply(t,s),apply(t',s')) , Marked_eq(s,s')> 
     --> <Marked_eq(cons(t,l),cons(t',l')) , Marked_eq(t,t')>
  <Marked_eq(apply(t,s),apply(t',s')) , Marked_eq(t,t')> 
     --> <Marked_eq(lambda(x,t),lambda(x',t')) , Marked_eq(t,t')>
  <Marked_eq(apply(t,s),apply(t',s')) , Marked_eq(t,t')> 
     --> <Marked_eq(lambda(x,t),lambda(x',t')) , Marked_eq(x,x')>
  <Marked_eq(apply(t,s),apply(t',s')) , Marked_eq(t,t')> 
     --> <Marked_eq(apply(t,s),apply(t',s')) , Marked_eq(s,s')>
  <Marked_eq(apply(t,s),apply(t',s')) , Marked_eq(t,t')> 
     --> <Marked_eq(apply(t,s),apply(t',s')) , Marked_eq(t,t')>
  <Marked_eq(apply(t,s),apply(t',s')) , Marked_eq(t,t')> 
     --> <Marked_eq(var(l),var(l')) , Marked_eq(l,l')>
  <Marked_eq(apply(t,s),apply(t',s')) , Marked_eq(t,t')> 
     --> <Marked_eq(cons(t,l),cons(t',l')) , Marked_eq(l,l')>
  <Marked_eq(apply(t,s),apply(t',s')) , Marked_eq(t,t')> 
     --> <Marked_eq(cons(t,l),cons(t',l')) , Marked_eq(t,t')>
  <Marked_eq(var(l),var(l')) , Marked_eq(l,l')> 
     --> <Marked_eq(lambda(x,t),lambda(x',t')) , Marked_eq(t,t')>
  <Marked_eq(var(l),var(l')) , Marked_eq(l,l')> 
     --> <Marked_eq(lambda(x,t),lambda(x',t')) , Marked_eq(x,x')>
  <Marked_eq(var(l),var(l')) , Marked_eq(l,l')> 
     --> <Marked_eq(apply(t,s),apply(t',s')) , Marked_eq(s,s')>
  <Marked_eq(var(l),var(l')) , Marked_eq(l,l')> 
     --> <Marked_eq(apply(t,s),apply(t',s')) , Marked_eq(t,t')>
  <Marked_eq(var(l),var(l')) , Marked_eq(l,l')> 
     --> <Marked_eq(var(l),var(l')) , Marked_eq(l,l')>
  <Marked_eq(var(l),var(l')) , Marked_eq(l,l')> 
     --> <Marked_eq(cons(t,l),cons(t',l')) , Marked_eq(l,l')>
  <Marked_eq(var(l),var(l')) , Marked_eq(l,l')> 
     --> <Marked_eq(cons(t,l),cons(t',l')) , Marked_eq(t,t')>
  <Marked_eq(cons(t,l),cons(t',l')) , Marked_eq(l,l')> 
     --> <Marked_eq(lambda(x,t),lambda(x',t')) , Marked_eq(t,t')>
  <Marked_eq(cons(t,l),cons(t',l')) , Marked_eq(l,l')> 
     --> <Marked_eq(lambda(x,t),lambda(x',t')) , Marked_eq(x,x')>
  <Marked_eq(cons(t,l),cons(t',l')) , Marked_eq(l,l')> 
     --> <Marked_eq(apply(t,s),apply(t',s')) , Marked_eq(s,s')>
  <Marked_eq(cons(t,l),cons(t',l')) , Marked_eq(l,l')> 
     --> <Marked_eq(apply(t,s),apply(t',s')) , Marked_eq(t,t')>
  <Marked_eq(cons(t,l),cons(t',l')) , Marked_eq(l,l')> 
     --> <Marked_eq(var(l),var(l')) , Marked_eq(l,l')>
  <Marked_eq(cons(t,l),cons(t',l')) , Marked_eq(l,l')> 
     --> <Marked_eq(cons(t,l),cons(t',l')) , Marked_eq(l,l')>
  <Marked_eq(cons(t,l),cons(t',l')) , Marked_eq(l,l')> 
     --> <Marked_eq(cons(t,l),cons(t',l')) , Marked_eq(t,t')>
  <Marked_eq(cons(t,l),cons(t',l')) , Marked_eq(t,t')> 
     --> <Marked_eq(lambda(x,t),lambda(x',t')) , Marked_eq(t,t')>
  <Marked_eq(cons(t,l),cons(t',l')) , Marked_eq(t,t')> 
     --> <Marked_eq(lambda(x,t),lambda(x',t')) , Marked_eq(x,x')>
  <Marked_eq(cons(t,l),cons(t',l')) , Marked_eq(t,t')> 
     --> <Marked_eq(apply(t,s),apply(t',s')) , Marked_eq(s,s')>
  <Marked_eq(cons(t,l),cons(t',l')) , Marked_eq(t,t')> 
     --> <Marked_eq(apply(t,s),apply(t',s')) , Marked_eq(t,t')>
  <Marked_eq(cons(t,l),cons(t',l')) , Marked_eq(t,t')> 
     --> <Marked_eq(var(l),var(l')) , Marked_eq(l,l')>
  <Marked_eq(cons(t,l),cons(t',l')) , Marked_eq(t,t')> 
     --> <Marked_eq(cons(t,l),cons(t',l')) , Marked_eq(l,l')>
  <Marked_eq(cons(t,l),cons(t',l')) , Marked_eq(t,t')> 
     --> <Marked_eq(cons(t,l),cons(t',l')) , Marked_eq(t,t')>
}
APPLY CRITERIA (Choosing graph)
Trying to solve the following constraints:
{
  and(true,y) >= y ;
  and(false,y) >= false ;
  eq(nil,nil) >= true ;
  eq(nil,cons(t,l)) >= false ;
  eq(cons(t,l),nil) >= false ;
  eq(cons(t,l),cons(t',l')) >= and(eq(t,t'),eq(l,l')) ;
  eq(var(l),var(l')) >= eq(l,l') ;
  eq(var(l),apply(t,s)) >= false ;
  eq(var(l),lambda(x,t)) >= false ;
  eq(apply(t,s),var(l)) >= false ;
  eq(apply(t,s),apply(t',s')) >= and(eq(t,t'),eq(s,s')) ;
  eq(apply(t,s),lambda(x,t)) >= false ;
  eq(lambda(x,t),var(l)) >= false ;
  eq(lambda(x,t),apply(t,s)) >= false ;
  eq(lambda(x,t),lambda(x',t')) >= and(eq(x,x'),eq(t,t')) ;
  if(true,var(k),var(l')) >= var(k) ;
  if(false,var(k),var(l')) >= var(l') ;
  ren(var(l),var(k),var(l')) >= if(eq(l,l'),var(k),var(l')) ;
  ren(x,y,apply(t,s)) >= apply(ren(x,y,t),ren(x,y,s)) ;
  ren(x,y,lambda(z,t)) >= lambda(var(cons(x,cons(y,cons(lambda(z,t),nil)))),
                           ren(x,y,
                            ren(z,var(cons(x,cons(y,cons(lambda(z,t),nil)))),t)))
                            ;
  Marked_ren(x,y,apply(t,s)) >= Marked_ren(x,y,s) ;
  Marked_ren(x,y,apply(t,s)) >= Marked_ren(x,y,t) ;
  Marked_ren(x,y,lambda(z,t)) >= Marked_ren(x,y,
                                  ren(z,
                                   var(cons(x,cons(y,cons(lambda(z,t),nil)))),
                                   t)) ;
  Marked_ren(x,y,lambda(z,t)) >= Marked_ren(z,
                                  var(cons(x,cons(y,cons(lambda(z,t),nil)))),
                                  t) ;
 }
 + Disjunctions:{ 
{
  Marked_ren(x,y,apply(t,s)) > Marked_ren(x,y,s) ;
 }
{
  Marked_ren(x,y,apply(t,s)) > Marked_ren(x,y,t) ;
 }
{
  Marked_ren(x,y,lambda(z,t)) > Marked_ren(x,y,
                                 ren(z,
                                  var(cons(x,cons(y,cons(lambda(z,t),nil)))),
                                  t)) ;
 }
{
  Marked_ren(x,y,lambda(z,t)) > Marked_ren(z,
                                 var(cons(x,cons(y,cons(lambda(z,t),nil)))),
                                 t) ;
 }
 } 
=== 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: and(true,y) >= y
constraint: and(false,y) >= false
constraint: eq(nil,nil) >= true
constraint: eq(nil,cons(t,l)) >= false
constraint: eq(cons(t,l),nil) >= false
constraint: eq(cons(t,l),cons(t',l')) >= and(eq(t,t'),eq(l,l'))
constraint: eq(var(l),var(l')) >= eq(l,l')
constraint: eq(var(l),apply(t,s)) >= false
constraint: eq(var(l),lambda(x,t)) >= false
constraint: eq(apply(t,s),var(l)) >= false
constraint: eq(apply(t,s),apply(t',s')) >= and(eq(t,t'),eq(s,s'))
constraint: eq(apply(t,s),lambda(x,t)) >= false
constraint: eq(lambda(x,t),var(l)) >= false
constraint: eq(lambda(x,t),apply(t,s)) >= false
constraint: eq(lambda(x,t),lambda(x',t')) >= and(eq(x,x'),eq(t,t'))
constraint: if(true,var(k),var(l')) >= var(k)
constraint: if(false,var(k),var(l')) >= var(l')
constraint: ren(var(l),var(k),var(l')) >= if(eq(l,l'),var(k),var(l'))
constraint: ren(x,y,apply(t,s)) >= apply(ren(x,y,t),ren(x,y,s))
constraint: ren(x,y,lambda(z,t)) >= lambda(var(cons(x,
                                                cons(y,cons(lambda(z,t),nil)))),
                                     ren(x,y,
                                      ren(z,
                                       var(cons(x,
                                            cons(y,cons(lambda(z,t),nil)))),
                                       t)))
constraint: Marked_ren(x,y,apply(t,s)) >= Marked_ren(x,y,s)
constraint: Marked_ren(x,y,apply(t,s)) >= Marked_ren(x,y,t)
constraint: Marked_ren(x,y,lambda(z,t)) >= Marked_ren(x,y,
                                            ren(z,
                                             var(cons(x,
                                                  cons(y,cons(lambda(z,t),nil))))
                                              ,t))
constraint: Marked_ren(x,y,lambda(z,t)) >= Marked_ren(z,
                                            var(cons(x,
                                                 cons(y,cons(lambda(z,t),nil)))),
                                            t)
APPLY CRITERIA (Choosing graph)
Trying to solve the following constraints:
{
  and(true,y) >= y ;
  and(false,y) >= false ;
  eq(nil,nil) >= true ;
  eq(nil,cons(t,l)) >= false ;
  eq(cons(t,l),nil) >= false ;
  eq(cons(t,l),cons(t',l')) >= and(eq(t,t'),eq(l,l')) ;
  eq(var(l),var(l')) >= eq(l,l') ;
  eq(var(l),apply(t,s)) >= false ;
  eq(var(l),lambda(x,t)) >= false ;
  eq(apply(t,s),var(l)) >= false ;
  eq(apply(t,s),apply(t',s')) >= and(eq(t,t'),eq(s,s')) ;
  eq(apply(t,s),lambda(x,t)) >= false ;
  eq(lambda(x,t),var(l)) >= false ;
  eq(lambda(x,t),apply(t,s)) >= false ;
  eq(lambda(x,t),lambda(x',t')) >= and(eq(x,x'),eq(t,t')) ;
  if(true,var(k),var(l')) >= var(k) ;
  if(false,var(k),var(l')) >= var(l') ;
  ren(var(l),var(k),var(l')) >= if(eq(l,l'),var(k),var(l')) ;
  ren(x,y,apply(t,s)) >= apply(ren(x,y,t),ren(x,y,s)) ;
  ren(x,y,lambda(z,t)) >= lambda(var(cons(x,cons(y,cons(lambda(z,t),nil)))),
                           ren(x,y,
                            ren(z,var(cons(x,cons(y,cons(lambda(z,t),nil)))),t)))
                            ;
  Marked_eq(cons(t,l),cons(t',l')) >= Marked_eq(l,l') ;
  Marked_eq(cons(t,l),cons(t',l')) >= Marked_eq(t,t') ;
  Marked_eq(var(l),var(l')) >= Marked_eq(l,l') ;
  Marked_eq(apply(t,s),apply(t',s')) >= Marked_eq(s,s') ;
  Marked_eq(apply(t,s),apply(t',s')) >= Marked_eq(t,t') ;
  Marked_eq(lambda(x,t),lambda(x',t')) >= Marked_eq(t,t') ;
  Marked_eq(lambda(x,t),lambda(x',t')) >= Marked_eq(x,x') ;
 }
 + Disjunctions:{ 
{
  Marked_eq(cons(t,l),cons(t',l')) > Marked_eq(l,l') ;
 }
{
  Marked_eq(cons(t,l),cons(t',l')) > Marked_eq(t,t') ;
 }
{
  Marked_eq(var(l),var(l')) > Marked_eq(l,l') ;
 }
{
  Marked_eq(apply(t,s),apply(t',s')) > Marked_eq(s,s') ;
 }
{
  Marked_eq(apply(t,s),apply(t',s')) > Marked_eq(t,t') ;
 }
{
  Marked_eq(lambda(x,t),lambda(x',t')) > Marked_eq(t,t') ;
 }
{
  Marked_eq(lambda(x,t),lambda(x',t')) > Marked_eq(x,x') ;
 }
 } 
=== 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 ===
=== TIMER virtual : 25.000000 ===
Search parameters: AFS type: 2 ; time limit: 25.. 
=== STOPING TIMER virtual ===
=== TIMER virtual : 25.000000 ===
Search parameters: AFS type: 2 ; time limit: 25.. 
=== STOPING TIMER virtual ===
=== TIMER virtual : 25.000000 ===
Search parameters: AFS type: 2 ; time limit: 25.. 
=== STOPING TIMER virtual ===
=== TIMER virtual : 25.000000 ===
Search parameters: AFS type: 2 ; time limit: 25.. 
=== STOPING TIMER virtual ===
=== TIMER virtual : 25.000000 ===
Search parameters: AFS type: 2 ; time limit: 25.. 
=== STOPING TIMER virtual ===
=== TIMER virtual : 25.000000 ===
Search parameters: AFS type: 2 ; time limit: 25.. 
=== STOPING TIMER virtual ===
=== 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
=== 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 67.241180 seconds (real time)
Cime Exit Status: 0