- : unit = ()
- : 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 (Subterm criterion)
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 (Subterm criterion)

ST: Marked_eq -> 2

APPLY CRITERIA (Graph splitting)
Found 1 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(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))>
}
APPLY CRITERIA (Subterm criterion)
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,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,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,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 (Graph splitting)
Found 1 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)>
}
APPLY CRITERIA (Subterm criterion)

ST: Marked_ren -> 3

APPLY CRITERIA (Graph splitting)
Found 0 components:
APPLY CRITERIA (Graph splitting)
Found 0 components:
SOLVED
{
 
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)))
 ,
 CRITERION: MDP
 [ {
      
     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)>
 ,
 CRITERION: SG
 [ {
      
     DP termination of:
     <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)>
 ,
 CRITERION: CG using polynomial interpretation = 
 [ and ] (X0,X1) = 1*X1; 
 [ lambda ] (X0,X1) = 1*X1; 
 [ nil ] () = 0; 
 [ false ] () = 0; 
 [ ren ] (X0,X1,X2) = 1*X2; 
 [ var ] (X0) = 0; 
 [ true ] () = 0; 
 [ if ] (X0,X1,X2) = 0; 
 [ cons ] (X0,X1) = 0; 
 [ eq ] (X0,X1) = 1; 
 [ Marked_ren ] (X0,X1,X2) = 2*X2; 
 [ apply ] (X0,X1) = 2*X1 + 2*X0 + 1; 
 removing <Marked_ren(x,y,apply(t,s)),Marked_ren(x,y,t)><Marked_ren(x,
                                                          y,apply(t,s)),
Marked_ren(x,y,s)>
 [ {
      
     DP termination of:
     <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)>
 ,
 CRITERION: SG
 [ {
      
     DP termination of:
     <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)>
 ,
 CRITERION: CG using polynomial interpretation = 
 [ and ] (X0,X1) = 1*X1; 
 [ lambda ] (X0,X1) = 1*X1 + 2; 
 [ nil ] () = 0; 
 [ false ] () = 0; 
 [ ren ] (X0,X1,X2) = 1*X2; 
 [ var ] (X0) = 2; 
 [ true ] () = 0; 
 [ if ] (X0,X1,X2) = 2; 
 [ cons ] (X0,X1) = 0; 
 [ eq ] (X0,X1) = 0; 
 [ Marked_ren ] (X0,X1,X2) = 2*X2 + 2*X1; 
 [ apply ] (X0,X1) = 0; 
 removing <Marked_ren(x,y,lambda(z,t)),Marked_ren(x,y,
                                        ren(z,
                                         var(cons(x,
                                              cons(y,cons(lambda(z,t),nil)))),
                                         t))>
 [ {
      
     DP termination of:
     <Marked_ren(x,y,lambda(z,t)) , Marked_ren(z,
                                     var(cons(x,cons(y,cons(lambda(z,t),nil)))),
                                     t)>
 ,
 CRITERION: SG
 [ {
      
     DP termination of:
     <Marked_ren(x,y,lambda(z,t)) , Marked_ren(z,
                                     var(cons(x,cons(y,cons(lambda(z,t),nil)))),
                                     t)>
 ,
 CRITERION: ST
 [ {
      
     DP termination of:
      ,
      CRITERION: SG
      [  ]} 
      ]} 
 ]} 
 ]} 
 ]} 
 ]} 
{
 
DP termination of:
<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_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(lambda(x,t),lambda(x',t')) , Marked_eq(t,t')>
 ,
 CRITERION: ST
 [ {
      
     DP termination of:
      ,
      CRITERION: SG
      [  ]} 
      ]} 
 ]} 
 ]} 

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