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

TRS termination of:
[1] din(der(plus(X,Y))) -> u21(din(der(X)),X,Y)
[2] u21(dout(DX),X,Y) -> u22(din(der(Y)),X,Y,DX)
[3] u22(dout(DY),X,Y,DX) -> dout(plus(DX,DY))
[4] din(der(times(X,Y))) -> u31(din(der(X)),X,Y)
[5] u31(dout(DX),X,Y) -> u32(din(der(Y)),X,Y,DX)
[6] u32(dout(DY),X,Y,DX) -> dout(plus(times(X,DY),times(Y,DX)))
[7] din(der(der(X))) -> u41(din(der(X)),X)
[8] u41(dout(DX),X) -> u42(din(der(DX)),X,DX)
[9] u42(dout(DDX),X,DX) -> dout(DDX)


Sub problem: 
guided: 

DP termination of:
<Marked_din(der(plus(X,Y))) , Marked_u21(din(der(X)),X,Y)>
<Marked_din(der(plus(X,Y))) , Marked_din(der(X))>
<Marked_u21(dout(DX),X,Y) , Marked_u22(din(der(Y)),X,Y,DX)>
<Marked_u21(dout(DX),X,Y) , Marked_din(der(Y))>
<Marked_din(der(times(X,Y))) , Marked_u31(din(der(X)),X,Y)>
<Marked_din(der(times(X,Y))) , Marked_din(der(X))>
<Marked_u31(dout(DX),X,Y) , Marked_u32(din(der(Y)),X,Y,DX)>
<Marked_u31(dout(DX),X,Y) , Marked_din(der(Y))>
<Marked_din(der(der(X))) , Marked_u41(din(der(X)),X)>
<Marked_din(der(der(X))) , Marked_din(der(X))>
<Marked_u41(dout(DX),X) , Marked_u42(din(der(DX)),X,DX)>
<Marked_u41(dout(DX),X) , Marked_din(der(DX))>
 
END GUIDED
APPLY CRITERIA (Graph splitting)
Found 1 components:

{  <Marked_u41(dout(DX),X) , Marked_din(der(DX))> 
      --> <Marked_din(der(der(X))) , Marked_din(der(X))>
  <Marked_u41(dout(DX),X) , Marked_din(der(DX))> 
     --> <Marked_din(der(der(X))) , Marked_u41(din(der(X)),X)>
  <Marked_u41(dout(DX),X) , Marked_din(der(DX))> 
     --> <Marked_din(der(times(X,Y))) , Marked_din(der(X))>
  <Marked_u41(dout(DX),X) , Marked_din(der(DX))> 
     --> <Marked_din(der(times(X,Y))) , Marked_u31(din(der(X)),X,Y)>
  <Marked_u41(dout(DX),X) , Marked_din(der(DX))> 
     --> <Marked_din(der(plus(X,Y))) , Marked_din(der(X))>
  <Marked_u41(dout(DX),X) , Marked_din(der(DX))> 
     --> <Marked_din(der(plus(X,Y))) , Marked_u21(din(der(X)),X,Y)>
  <Marked_din(der(der(X))) , Marked_din(der(X))> 
     --> <Marked_din(der(der(X))) , Marked_din(der(X))>
  <Marked_din(der(der(X))) , Marked_din(der(X))> 
     --> <Marked_din(der(der(X))) , Marked_u41(din(der(X)),X)>
  <Marked_din(der(der(X))) , Marked_din(der(X))> 
     --> <Marked_din(der(times(X,Y))) , Marked_din(der(X))>
  <Marked_din(der(der(X))) , Marked_din(der(X))> 
     --> <Marked_din(der(times(X,Y))) , Marked_u31(din(der(X)),X,Y)>
  <Marked_din(der(der(X))) , Marked_din(der(X))> 
     --> <Marked_din(der(plus(X,Y))) , Marked_din(der(X))>
  <Marked_din(der(der(X))) , Marked_din(der(X))> 
     --> <Marked_din(der(plus(X,Y))) , Marked_u21(din(der(X)),X,Y)>
  <Marked_din(der(der(X))) , Marked_u41(din(der(X)),X)> 
     --> <Marked_u41(dout(DX),X) , Marked_din(der(DX))>
  <Marked_u31(dout(DX),X,Y) , Marked_din(der(Y))> 
     --> <Marked_din(der(der(X))) , Marked_din(der(X))>
  <Marked_u31(dout(DX),X,Y) , Marked_din(der(Y))> 
     --> <Marked_din(der(der(X))) , Marked_u41(din(der(X)),X)>
  <Marked_u31(dout(DX),X,Y) , Marked_din(der(Y))> 
     --> <Marked_din(der(times(X,Y))) , Marked_din(der(X))>
  <Marked_u31(dout(DX),X,Y) , Marked_din(der(Y))> 
     --> <Marked_din(der(times(X,Y))) , Marked_u31(din(der(X)),X,Y)>
  <Marked_u31(dout(DX),X,Y) , Marked_din(der(Y))> 
     --> <Marked_din(der(plus(X,Y))) , Marked_din(der(X))>
  <Marked_u31(dout(DX),X,Y) , Marked_din(der(Y))> 
     --> <Marked_din(der(plus(X,Y))) , Marked_u21(din(der(X)),X,Y)>
  <Marked_din(der(times(X,Y))) , Marked_din(der(X))> 
     --> <Marked_din(der(der(X))) , Marked_din(der(X))>
  <Marked_din(der(times(X,Y))) , Marked_din(der(X))> 
     --> <Marked_din(der(der(X))) , Marked_u41(din(der(X)),X)>
  <Marked_din(der(times(X,Y))) , Marked_din(der(X))> 
     --> <Marked_din(der(times(X,Y))) , Marked_din(der(X))>
  <Marked_din(der(times(X,Y))) , Marked_din(der(X))> 
     --> <Marked_din(der(times(X,Y))) , Marked_u31(din(der(X)),X,Y)>
  <Marked_din(der(times(X,Y))) , Marked_din(der(X))> 
     --> <Marked_din(der(plus(X,Y))) , Marked_din(der(X))>
  <Marked_din(der(times(X,Y))) , Marked_din(der(X))> 
     --> <Marked_din(der(plus(X,Y))) , Marked_u21(din(der(X)),X,Y)>
  <Marked_din(der(times(X,Y))) , Marked_u31(din(der(X)),X,Y)> 
     --> <Marked_u31(dout(DX),X,Y) , Marked_din(der(Y))>
  <Marked_u21(dout(DX),X,Y) , Marked_din(der(Y))> 
     --> <Marked_din(der(der(X))) , Marked_din(der(X))>
  <Marked_u21(dout(DX),X,Y) , Marked_din(der(Y))> 
     --> <Marked_din(der(der(X))) , Marked_u41(din(der(X)),X)>
  <Marked_u21(dout(DX),X,Y) , Marked_din(der(Y))> 
     --> <Marked_din(der(times(X,Y))) , Marked_din(der(X))>
  <Marked_u21(dout(DX),X,Y) , Marked_din(der(Y))> 
     --> <Marked_din(der(times(X,Y))) , Marked_u31(din(der(X)),X,Y)>
  <Marked_u21(dout(DX),X,Y) , Marked_din(der(Y))> 
     --> <Marked_din(der(plus(X,Y))) , Marked_din(der(X))>
  <Marked_u21(dout(DX),X,Y) , Marked_din(der(Y))> 
     --> <Marked_din(der(plus(X,Y))) , Marked_u21(din(der(X)),X,Y)>
  <Marked_din(der(plus(X,Y))) , Marked_din(der(X))> 
     --> <Marked_din(der(der(X))) , Marked_din(der(X))>
  <Marked_din(der(plus(X,Y))) , Marked_din(der(X))> 
     --> <Marked_din(der(der(X))) , Marked_u41(din(der(X)),X)>
  <Marked_din(der(plus(X,Y))) , Marked_din(der(X))> 
     --> <Marked_din(der(times(X,Y))) , Marked_din(der(X))>
  <Marked_din(der(plus(X,Y))) , Marked_din(der(X))> 
     --> <Marked_din(der(times(X,Y))) , Marked_u31(din(der(X)),X,Y)>
  <Marked_din(der(plus(X,Y))) , Marked_din(der(X))> 
     --> <Marked_din(der(plus(X,Y))) , Marked_din(der(X))>
  <Marked_din(der(plus(X,Y))) , Marked_din(der(X))> 
     --> <Marked_din(der(plus(X,Y))) , Marked_u21(din(der(X)),X,Y)>
  <Marked_din(der(plus(X,Y))) , Marked_u21(din(der(X)),X,Y)> 
     --> <Marked_u21(dout(DX),X,Y) , Marked_din(der(Y))>
}
APPLY CRITERIA (Choosing graph)
Trying to solve the following constraints:
{
  u21(dout(DX),X,Y) >= u22(din(der(Y)),X,Y,DX) ;
  din(der(der(X))) >= u41(din(der(X)),X) ;
  din(der(plus(X,Y))) >= u21(din(der(X)),X,Y) ;
  din(der(times(X,Y))) >= u31(din(der(X)),X,Y) ;
  u22(dout(DY),X,Y,DX) >= dout(plus(DX,DY)) ;
  u31(dout(DX),X,Y) >= u32(din(der(Y)),X,Y,DX) ;
  u32(dout(DY),X,Y,DX) >= dout(plus(times(X,DY),times(Y,DX))) ;
  u41(dout(DX),X) >= u42(din(der(DX)),X,DX) ;
  u42(dout(DDX),X,DX) >= dout(DDX) ;
  Marked_u41(dout(DX),X) >= Marked_din(der(DX)) ;
  Marked_din(der(der(X))) >= Marked_u41(din(der(X)),X) ;
  Marked_din(der(der(X))) >= Marked_din(der(X)) ;
  Marked_din(der(plus(X,Y))) >= Marked_din(der(X)) ;
  Marked_din(der(plus(X,Y))) >= Marked_u21(din(der(X)),X,Y) ;
  Marked_din(der(times(X,Y))) >= Marked_din(der(X)) ;
  Marked_din(der(times(X,Y))) >= Marked_u31(din(der(X)),X,Y) ;
  Marked_u31(dout(DX),X,Y) >= Marked_din(der(Y)) ;
  Marked_u21(dout(DX),X,Y) >= Marked_din(der(Y)) ;
 }
 + Disjunctions:{ 
{
  Marked_u41(dout(DX),X) > Marked_din(der(DX)) ;
 }
{
  Marked_din(der(der(X))) > Marked_u41(din(der(X)),X) ;
 }
{
  Marked_din(der(der(X))) > Marked_din(der(X)) ;
 }
{
  Marked_din(der(plus(X,Y))) > Marked_din(der(X)) ;
 }
{
  Marked_din(der(plus(X,Y))) > Marked_u21(din(der(X)),X,Y) ;
 }
{
  Marked_din(der(times(X,Y))) > Marked_din(der(X)) ;
 }
{
  Marked_din(der(times(X,Y))) > Marked_u31(din(der(X)),X,Y) ;
 }
{
  Marked_u31(dout(DX),X,Y) > Marked_din(der(Y)) ;
 }
{
  Marked_u21(dout(DX),X,Y) > Marked_din(der(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: u21(dout(DX),X,Y) >= u22(din(der(Y)),X,Y,DX)
constraint: din(der(der(X))) >= u41(din(der(X)),X)
constraint: din(der(plus(X,Y))) >= u21(din(der(X)),X,Y)
constraint: din(der(times(X,Y))) >= u31(din(der(X)),X,Y)
constraint: u22(dout(DY),X,Y,DX) >= dout(plus(DX,DY))
constraint: u31(dout(DX),X,Y) >= u32(din(der(Y)),X,Y,DX)
constraint: u32(dout(DY),X,Y,DX) >= dout(plus(times(X,DY),times(Y,DX)))
constraint: u41(dout(DX),X) >= u42(din(der(DX)),X,DX)
constraint: u42(dout(DDX),X,DX) >= dout(DDX)
constraint: Marked_u41(dout(DX),X) >= Marked_din(der(DX))
constraint: Marked_din(der(der(X))) >= Marked_u41(din(der(X)),X)
constraint: Marked_din(der(der(X))) >= Marked_din(der(X))
constraint: Marked_din(der(plus(X,Y))) >= Marked_din(der(X))
constraint: Marked_din(der(plus(X,Y))) >= Marked_u21(din(der(X)),X,Y)
constraint: Marked_din(der(times(X,Y))) >= Marked_din(der(X))
constraint: Marked_din(der(times(X,Y))) >= Marked_u31(din(der(X)),X,Y)
constraint: Marked_u31(dout(DX),X,Y) >= Marked_din(der(Y))
constraint: Marked_u21(dout(DX),X,Y) >= Marked_din(der(Y))
APPLY CRITERIA (Graph splitting)
Found 1 components:

{  <Marked_u41(dout(DX),X) , Marked_din(der(DX))> 
      --> <Marked_din(der(der(X))) , Marked_din(der(X))>
  <Marked_u41(dout(DX),X) , Marked_din(der(DX))> 
     --> <Marked_din(der(der(X))) , Marked_u41(din(der(X)),X)>
  <Marked_u41(dout(DX),X) , Marked_din(der(DX))> 
     --> <Marked_din(der(times(X,Y))) , Marked_din(der(X))>
  <Marked_u41(dout(DX),X) , Marked_din(der(DX))> 
     --> <Marked_din(der(plus(X,Y))) , Marked_din(der(X))>
  <Marked_din(der(der(X))) , Marked_din(der(X))> 
     --> <Marked_din(der(der(X))) , Marked_din(der(X))>
  <Marked_din(der(der(X))) , Marked_din(der(X))> 
     --> <Marked_din(der(der(X))) , Marked_u41(din(der(X)),X)>
  <Marked_din(der(der(X))) , Marked_din(der(X))> 
     --> <Marked_din(der(times(X,Y))) , Marked_din(der(X))>
  <Marked_din(der(der(X))) , Marked_din(der(X))> 
     --> <Marked_din(der(plus(X,Y))) , Marked_din(der(X))>
  <Marked_din(der(der(X))) , Marked_u41(din(der(X)),X)> 
     --> <Marked_u41(dout(DX),X) , Marked_din(der(DX))>
  <Marked_din(der(times(X,Y))) , Marked_din(der(X))> 
     --> <Marked_din(der(der(X))) , Marked_din(der(X))>
  <Marked_din(der(times(X,Y))) , Marked_din(der(X))> 
     --> <Marked_din(der(der(X))) , Marked_u41(din(der(X)),X)>
  <Marked_din(der(times(X,Y))) , Marked_din(der(X))> 
     --> <Marked_din(der(times(X,Y))) , Marked_din(der(X))>
  <Marked_din(der(times(X,Y))) , Marked_din(der(X))> 
     --> <Marked_din(der(plus(X,Y))) , Marked_din(der(X))>
  <Marked_din(der(plus(X,Y))) , Marked_din(der(X))> 
     --> <Marked_din(der(der(X))) , Marked_din(der(X))>
  <Marked_din(der(plus(X,Y))) , Marked_din(der(X))> 
     --> <Marked_din(der(der(X))) , Marked_u41(din(der(X)),X)>
  <Marked_din(der(plus(X,Y))) , Marked_din(der(X))> 
     --> <Marked_din(der(times(X,Y))) , Marked_din(der(X))>
  <Marked_din(der(plus(X,Y))) , Marked_din(der(X))> 
     --> <Marked_din(der(plus(X,Y))) , Marked_din(der(X))>
}
APPLY CRITERIA (Choosing graph)
Trying to solve the following constraints:
{
  u21(dout(DX),X,Y) >= u22(din(der(Y)),X,Y,DX) ;
  din(der(der(X))) >= u41(din(der(X)),X) ;
  din(der(plus(X,Y))) >= u21(din(der(X)),X,Y) ;
  din(der(times(X,Y))) >= u31(din(der(X)),X,Y) ;
  u22(dout(DY),X,Y,DX) >= dout(plus(DX,DY)) ;
  u31(dout(DX),X,Y) >= u32(din(der(Y)),X,Y,DX) ;
  u32(dout(DY),X,Y,DX) >= dout(plus(times(X,DY),times(Y,DX))) ;
  u41(dout(DX),X) >= u42(din(der(DX)),X,DX) ;
  u42(dout(DDX),X,DX) >= dout(DDX) ;
  Marked_u41(dout(DX),X) >= Marked_din(der(DX)) ;
  Marked_din(der(der(X))) >= Marked_u41(din(der(X)),X) ;
  Marked_din(der(der(X))) >= Marked_din(der(X)) ;
  Marked_din(der(plus(X,Y))) >= Marked_din(der(X)) ;
  Marked_din(der(times(X,Y))) >= Marked_din(der(X)) ;
 }
 + Disjunctions:{ 
{
  Marked_u41(dout(DX),X) > Marked_din(der(DX)) ;
 }
{
  Marked_din(der(der(X))) > Marked_u41(din(der(X)),X) ;
 }
{
  Marked_din(der(der(X))) > Marked_din(der(X)) ;
 }
{
  Marked_din(der(plus(X,Y))) > Marked_din(der(X)) ;
 }
{
  Marked_din(der(times(X,Y))) > Marked_din(der(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
Sat solver result read
=== STOPING TIMER real ===
=== STOPING TIMER virtual ===
constraint: u21(dout(DX),X,Y) >= u22(din(der(Y)),X,Y,DX)
constraint: din(der(der(X))) >= u41(din(der(X)),X)
constraint: din(der(plus(X,Y))) >= u21(din(der(X)),X,Y)
constraint: din(der(times(X,Y))) >= u31(din(der(X)),X,Y)
constraint: u22(dout(DY),X,Y,DX) >= dout(plus(DX,DY))
constraint: u31(dout(DX),X,Y) >= u32(din(der(Y)),X,Y,DX)
constraint: u32(dout(DY),X,Y,DX) >= dout(plus(times(X,DY),times(Y,DX)))
constraint: u41(dout(DX),X) >= u42(din(der(DX)),X,DX)
constraint: u42(dout(DDX),X,DX) >= dout(DDX)
constraint: Marked_u41(dout(DX),X) >= Marked_din(der(DX))
constraint: Marked_din(der(der(X))) >= Marked_u41(din(der(X)),X)
constraint: Marked_din(der(der(X))) >= Marked_din(der(X))
constraint: Marked_din(der(plus(X,Y))) >= Marked_din(der(X))
constraint: Marked_din(der(times(X,Y))) >= Marked_din(der(X))
APPLY CRITERIA (Graph splitting)
Found 1 components:

{  <Marked_din(der(times(X,Y))) , Marked_din(der(X))> 
      --> <Marked_din(der(times(X,Y))) , Marked_din(der(X))>
  <Marked_din(der(times(X,Y))) , Marked_din(der(X))> 
     --> <Marked_din(der(plus(X,Y))) , Marked_din(der(X))>
  <Marked_din(der(plus(X,Y))) , Marked_din(der(X))> 
     --> <Marked_din(der(times(X,Y))) , Marked_din(der(X))>
  <Marked_din(der(plus(X,Y))) , Marked_din(der(X))> 
     --> <Marked_din(der(plus(X,Y))) , Marked_din(der(X))>
}
APPLY CRITERIA (Choosing graph)
Trying to solve the following constraints:
{
  u21(dout(DX),X,Y) >= u22(din(der(Y)),X,Y,DX) ;
  din(der(der(X))) >= u41(din(der(X)),X) ;
  din(der(plus(X,Y))) >= u21(din(der(X)),X,Y) ;
  din(der(times(X,Y))) >= u31(din(der(X)),X,Y) ;
  u22(dout(DY),X,Y,DX) >= dout(plus(DX,DY)) ;
  u31(dout(DX),X,Y) >= u32(din(der(Y)),X,Y,DX) ;
  u32(dout(DY),X,Y,DX) >= dout(plus(times(X,DY),times(Y,DX))) ;
  u41(dout(DX),X) >= u42(din(der(DX)),X,DX) ;
  u42(dout(DDX),X,DX) >= dout(DDX) ;
  Marked_din(der(plus(X,Y))) >= Marked_din(der(X)) ;
  Marked_din(der(times(X,Y))) >= Marked_din(der(X)) ;
 }
 + Disjunctions:{ 
{
  Marked_din(der(plus(X,Y))) > Marked_din(der(X)) ;
 }
{
  Marked_din(der(times(X,Y))) > Marked_din(der(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
Sat solver result read
=== STOPING TIMER real ===
=== STOPING TIMER virtual ===
constraint: u21(dout(DX),X,Y) >= u22(din(der(Y)),X,Y,DX)
constraint: din(der(der(X))) >= u41(din(der(X)),X)
constraint: din(der(plus(X,Y))) >= u21(din(der(X)),X,Y)
constraint: din(der(times(X,Y))) >= u31(din(der(X)),X,Y)
constraint: u22(dout(DY),X,Y,DX) >= dout(plus(DX,DY))
constraint: u31(dout(DX),X,Y) >= u32(din(der(Y)),X,Y,DX)
constraint: u32(dout(DY),X,Y,DX) >= dout(plus(times(X,DY),times(Y,DX)))
constraint: u41(dout(DX),X) >= u42(din(der(DX)),X,DX)
constraint: u42(dout(DDX),X,DX) >= dout(DDX)
constraint: Marked_din(der(plus(X,Y))) >= Marked_din(der(X))
constraint: Marked_din(der(times(X,Y))) >= Marked_din(der(X))
APPLY CRITERIA (Graph splitting)
Found 1 components:

{  <Marked_din(der(times(X,Y))) , Marked_din(der(X))> 
      --> <Marked_din(der(times(X,Y))) , Marked_din(der(X))>
}
APPLY CRITERIA (Choosing graph)
Trying to solve the following constraints:
{
  u21(dout(DX),X,Y) >= u22(din(der(Y)),X,Y,DX) ;
  din(der(der(X))) >= u41(din(der(X)),X) ;
  din(der(plus(X,Y))) >= u21(din(der(X)),X,Y) ;
  din(der(times(X,Y))) >= u31(din(der(X)),X,Y) ;
  u22(dout(DY),X,Y,DX) >= dout(plus(DX,DY)) ;
  u31(dout(DX),X,Y) >= u32(din(der(Y)),X,Y,DX) ;
  u32(dout(DY),X,Y,DX) >= dout(plus(times(X,DY),times(Y,DX))) ;
  u41(dout(DX),X) >= u42(din(der(DX)),X,DX) ;
  u42(dout(DDX),X,DX) >= dout(DDX) ;
  Marked_din(der(times(X,Y))) >= Marked_din(der(X)) ;
 }
 + Disjunctions:{ 
{
  Marked_din(der(times(X,Y))) > Marked_din(der(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
Sat solver result read
=== STOPING TIMER real ===
=== STOPING TIMER virtual ===
constraint: u21(dout(DX),X,Y) >= u22(din(der(Y)),X,Y,DX)
constraint: din(der(der(X))) >= u41(din(der(X)),X)
constraint: din(der(plus(X,Y))) >= u21(din(der(X)),X,Y)
constraint: din(der(times(X,Y))) >= u31(din(der(X)),X,Y)
constraint: u22(dout(DY),X,Y,DX) >= dout(plus(DX,DY))
constraint: u31(dout(DX),X,Y) >= u32(din(der(Y)),X,Y,DX)
constraint: u32(dout(DY),X,Y,DX) >= dout(plus(times(X,DY),times(Y,DX)))
constraint: u41(dout(DX),X) >= u42(din(der(DX)),X,DX)
constraint: u42(dout(DDX),X,DX) >= dout(DDX)
constraint: Marked_din(der(times(X,Y))) >= Marked_din(der(X))
APPLY CRITERIA (Graph splitting)
Found 0 components:
SOLVED
{
 
TRS termination of:
[1] din(der(plus(X,Y))) -> u21(din(der(X)),X,Y)
[2] u21(dout(DX),X,Y) -> u22(din(der(Y)),X,Y,DX)
[3] u22(dout(DY),X,Y,DX) -> dout(plus(DX,DY))
[4] din(der(times(X,Y))) -> u31(din(der(X)),X,Y)
[5] u31(dout(DX),X,Y) -> u32(din(der(Y)),X,Y,DX)
[6] u32(dout(DY),X,Y,DX) -> dout(plus(times(X,DY),times(Y,DX)))
[7] din(der(der(X))) -> u41(din(der(X)),X)
[8] u41(dout(DX),X) -> u42(din(der(DX)),X,DX)
[9] u42(dout(DDX),X,DX) -> dout(DDX)
 ,
 CRITERION: MDP
 [ {
      
     DP termination of:
     <Marked_din(der(plus(X,Y))) , Marked_u21(din(der(X)),X,Y)>
<Marked_din(der(plus(X,Y))) , Marked_din(der(X))>
<Marked_u21(dout(DX),X,Y) , Marked_u22(din(der(Y)),X,Y,DX)>
<Marked_u21(dout(DX),X,Y) , Marked_din(der(Y))>
<Marked_din(der(times(X,Y))) , Marked_u31(din(der(X)),X,Y)>
<Marked_din(der(times(X,Y))) , Marked_din(der(X))>
<Marked_u31(dout(DX),X,Y) , Marked_u32(din(der(Y)),X,Y,DX)>
<Marked_u31(dout(DX),X,Y) , Marked_din(der(Y))>
<Marked_din(der(der(X))) , Marked_u41(din(der(X)),X)>
<Marked_din(der(der(X))) , Marked_din(der(X))>
<Marked_u41(dout(DX),X) , Marked_u42(din(der(DX)),X,DX)>
<Marked_u41(dout(DX),X) , Marked_din(der(DX))>
 ,
 CRITERION: SG
 [ {
      
     DP termination of:
     <Marked_din(der(plus(X,Y))) , Marked_u21(din(der(X)),X,Y)>
<Marked_din(der(plus(X,Y))) , Marked_din(der(X))>
<Marked_u21(dout(DX),X,Y) , Marked_din(der(Y))>
<Marked_din(der(times(X,Y))) , Marked_u31(din(der(X)),X,Y)>
<Marked_din(der(times(X,Y))) , Marked_din(der(X))>
<Marked_u31(dout(DX),X,Y) , Marked_din(der(Y))>
<Marked_din(der(der(X))) , Marked_u41(din(der(X)),X)>
<Marked_din(der(der(X))) , Marked_din(der(X))>
<Marked_u41(dout(DX),X) , Marked_din(der(DX))>
 ,
 CRITERION: CG using polynomial interpretation = 
 [ u21 ] (X0,X1,X2) = 0; 
 [ u32 ] (X0,X1,X2,X3) = 2; 
 [ u22 ] (X0,X1,X2,X3) = 2*X0; 
 [ Marked_u41 ] (X0,X1) = 2; 
 [ der ] (X0) = 0; 
 [ u42 ] (X0,X1,X2) = 2; 
 [ u31 ] (X0,X1,X2) = 2*X0; 
 [ din ] (X0) = 0; 
 [ Marked_u21 ] (X0,X1,X2) = 1*X0 + 2; 
 [ u41 ] (X0,X1) = 1*X0; 
 [ dout ] (X0) = 2; 
 [ Marked_din ] (X0) = 2; 
 [ plus ] (X0,X1) = 0; 
 [ times ] (X0,X1) = 0; 
 [ Marked_u31 ] (X0,X1,X2) = 3*X0 + 2; 
 removing <Marked_u21(dout(DX),X,Y),Marked_din(der(Y))><Marked_u31(dout(DX),
                                                         X,Y),Marked_din(
                                                               der(Y))>
 [ {
      
     DP termination of:
     <Marked_din(der(plus(X,Y))) , Marked_u21(din(der(X)),X,Y)>
<Marked_din(der(plus(X,Y))) , Marked_din(der(X))>
<Marked_din(der(times(X,Y))) , Marked_u31(din(der(X)),X,Y)>
<Marked_din(der(times(X,Y))) , Marked_din(der(X))>
<Marked_din(der(der(X))) , Marked_u41(din(der(X)),X)>
<Marked_din(der(der(X))) , Marked_din(der(X))>
<Marked_u41(dout(DX),X) , Marked_din(der(DX))>
 ,
 CRITERION: SG
 [ {
      
     DP termination of:
     <Marked_din(der(plus(X,Y))) , Marked_din(der(X))>
<Marked_din(der(times(X,Y))) , Marked_din(der(X))>
<Marked_din(der(der(X))) , Marked_u41(din(der(X)),X)>
<Marked_din(der(der(X))) , Marked_din(der(X))>
<Marked_u41(dout(DX),X) , Marked_din(der(DX))>
 ,
 CRITERION: CG using polynomial interpretation = 
 [ u21 ] (X0,X1,X2) = 1*X0; 
 [ u32 ] (X0,X1,X2,X3) = 1*X1 + 3; 
 [ u22 ] (X0,X1,X2,X3) = 1*X3 + 3; 
 [ Marked_u41 ] (X0,X1) = 3*X0 + 3; 
 [ der ] (X0) = 1*X0 + 3; 
 [ u42 ] (X0,X1,X2) = 1*X0; 
 [ u31 ] (X0,X1,X2) = 1*X1 + 3; 
 [ din ] (X0) = 1*X0; 
 [ u41 ] (X0,X1) = 1*X0 + 3; 
 [ dout ] (X0) = 1*X0 + 3; 
 [ Marked_din ] (X0) = 3*X0 + 1; 
 [ plus ] (X0,X1) = 1*X0; 
 [ times ] (X0,X1) = 1*X0; 
 removing <Marked_din(der(der(X))),Marked_u41(din(der(X)),X)><Marked_din(
                                                               der(der(X))),
Marked_din(der(X))><Marked_u41(dout(DX),X),Marked_din(der(DX))>
 [ {
      
     DP termination of:
     <Marked_din(der(plus(X,Y))) , Marked_din(der(X))>
<Marked_din(der(times(X,Y))) , Marked_din(der(X))>
 ,
 CRITERION: SG
 [ {
      
     DP termination of:
     <Marked_din(der(plus(X,Y))) , Marked_din(der(X))>
<Marked_din(der(times(X,Y))) , Marked_din(der(X))>
 ,
 CRITERION: CG using polynomial interpretation = 
 [ u21 ] (X0,X1,X2) = 0; 
 [ u32 ] (X0,X1,X2,X3) = 0; 
 [ u22 ] (X0,X1,X2,X3) = 0; 
 [ der ] (X0) = 2*X0; 
 [ u42 ] (X0,X1,X2) = 0; 
 [ u31 ] (X0,X1,X2) = 0; 
 [ din ] (X0) = 0; 
 [ u41 ] (X0,X1) = 0; 
 [ dout ] (X0) = 0; 
 [ Marked_din ] (X0) = 2*X0; 
 [ plus ] (X0,X1) = 2*X0 + 2; 
 [ times ] (X0,X1) = 2*X0; 
 removing <Marked_din(der(plus(X,Y))),Marked_din(der(X))>
 [ {
      
     DP termination of:
     <Marked_din(der(times(X,Y))) , Marked_din(der(X))>
 ,
 CRITERION: SG
 [ {
      
     DP termination of:
     <Marked_din(der(times(X,Y))) , Marked_din(der(X))>
 ,
 CRITERION: ORD
 [ 
     Solution found:
     polynomial interpretation = 
      [ u21 ] (X0,X1,X2) = 2*X0 + 0; 
 [ u32 ] (X0,X1,X2,X3) = 1*X0 + 0; 
 [ u22 ] (X0,X1,X2,X3) = 1*X0 + 0; 
 [ der ] (X0) = 1*X0 + 0; 
 [ u42 ] (X0,X1,X2) = 2*X0 + 0; 
 [ u31 ] (X0,X1,X2) = 0; 
 [ din ] (X0) = 0; 
 [ u41 ] (X0,X1) = 0; 
 [ dout ] (X0) = 3 + 0; 
 [ Marked_din ] (X0) = 1*X0 + 0; 
 [ plus ] (X0,X1) = 0; 
 [ times ] (X0,X1) = 2 + 1*X0 + 0; 
 ]} 
 ]} 
 ]} 
 ]} 
 ]} 
 ]} 
 ]} 
 ]} 
 ]} 

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