Term Rewriting System R:
[x, y]
f(x, a(b(y))) -> f(c(d(x)), y)
f(c(x), y) -> f(x, a(y))
f(d(x), y) -> f(x, b(y))

Termination of R to be shown. 



   R
     ↳Dependency Pair Analysis



R contains the following Dependency Pairs:

F(x, a(b(y))) -> F(c(d(x)), y)
F(c(x), y) -> F(x, a(y))
F(d(x), y) -> F(x, b(y))

Furthermore, R contains one SCC. 


   R
     ↳DPs
       →DP Problem 1
         ↳Modular Removal of Rules


Dependency Pairs:

F(d(x), y) -> F(x, b(y))
F(c(x), y) -> F(x, a(y))
F(x, a(b(y))) -> F(c(d(x)), y)


Rules:


f(x, a(b(y))) -> f(c(d(x)), y)
f(c(x), y) -> f(x, a(y))
f(d(x), y) -> f(x, b(y))





We have the following set of usable rules: none
To remove rules and DPs from this DP problem we used the following monotonic and CE-compatible order: Polynomial ordering.
Polynomial interpretation:
  POL(c(x1))=  x1  
  POL(b(x1))=  x1  
  POL(d(x1))=  x1  
  POL(a(x1))=  x1  
  POL(F(x1, x2))=  1 + x1 + x2  

We have the following set D of usable symbols: {c, b, d, a, F}
No Dependency Pairs can be deleted.
3 non usable rules have been deleted.

The result of this processor delivers one new DP problem.



   R
     ↳DPs
       →DP Problem 1
         ↳MRR
           →DP Problem 2
             ↳Non-Overlappingness Check


Dependency Pairs:

F(d(x), y) -> F(x, b(y))
F(c(x), y) -> F(x, a(y))
F(x, a(b(y))) -> F(c(d(x)), y)


Rule:

none





R does not overlap into P. Moreover, R is locally confluent (all critical pairs are trivially joinable).Hence we can switch to innermost.
The transformation is resulting in one subcycle: 


   R
     ↳DPs
       →DP Problem 1
         ↳MRR
           →DP Problem 2
             ↳NOC
             ...
               →DP Problem 3
                 ↳Instantiation Transformation


Dependency Pairs:

F(d(x), y) -> F(x, b(y))
F(c(x), y) -> F(x, a(y))
F(x, a(b(y))) -> F(c(d(x)), y)


Rule:

none


Strategy:

innermost




On this DP problem, an Instantiation SCC transformation can be performed.
As a result of transforming the rule

F(d(x), y) -> F(x, b(y))
two new Dependency Pairs are created:

F(d(x''), b(y'')) -> F(x'', b(b(y'')))
F(d(x''), a(y'')) -> F(x'', b(a(y'')))

The transformation is resulting in one new DP problem: 



   R
     ↳DPs
       →DP Problem 1
         ↳MRR
           →DP Problem 2
             ↳NOC
             ...
               →DP Problem 4
                 ↳Instantiation Transformation


Dependency Pairs:

F(d(x''), b(y'')) -> F(x'', b(b(y'')))
F(d(x''), a(y'')) -> F(x'', b(a(y'')))
F(x, a(b(y))) -> F(c(d(x)), y)
F(c(x), y) -> F(x, a(y))


Rule:

none


Strategy:

innermost




On this DP problem, an Instantiation SCC transformation can be performed.
As a result of transforming the rule

F(c(x), y) -> F(x, a(y))
four new Dependency Pairs are created:

F(c(x''), a(y'')) -> F(x'', a(a(y'')))
F(c(d(x'')), y'') -> F(d(x''), a(y''))
F(c(x'), b(b(y''''))) -> F(x', a(b(b(y''''))))
F(c(x'), b(a(y''''))) -> F(x', a(b(a(y''''))))

The transformation is resulting in one new DP problem: 



   R
     ↳DPs
       →DP Problem 1
         ↳MRR
           →DP Problem 2
             ↳NOC
             ...
               →DP Problem 5
                 ↳Instantiation Transformation


Dependency Pairs:

F(c(x'), b(b(y''''))) -> F(x', a(b(b(y''''))))
F(c(x'), b(a(y''''))) -> F(x', a(b(a(y''''))))
F(d(x''), a(y'')) -> F(x'', b(a(y'')))
F(c(x''), a(y'')) -> F(x'', a(a(y'')))
F(x, a(b(y))) -> F(c(d(x)), y)
F(c(d(x'')), y'') -> F(d(x''), a(y''))
F(d(x''), b(y'')) -> F(x'', b(b(y'')))


Rule:

none


Strategy:

innermost




On this DP problem, an Instantiation SCC transformation can be performed.
As a result of transforming the rule

F(x, a(b(y))) -> F(c(d(x)), y)
four new Dependency Pairs are created:

F(c(d(x'')), a(b(y''))) -> F(c(d(c(d(x'')))), y'')
F(d(x''''), a(b(y'))) -> F(c(d(d(x''''))), y')
F(x', a(b(b(y'''''')))) -> F(c(d(x')), b(y''''''))
F(x', a(b(a(y'''''')))) -> F(c(d(x')), a(y''''''))

The transformation is resulting in one new DP problem: 



   R
     ↳DPs
       →DP Problem 1
         ↳MRR
           →DP Problem 2
             ↳NOC
             ...
               →DP Problem 6
                 ↳Semantic Labelling


Dependency Pairs:

F(x', a(b(a(y'''''')))) -> F(c(d(x')), a(y''''''))
F(x', a(b(b(y'''''')))) -> F(c(d(x')), b(y''''''))
F(c(d(x'')), a(b(y''))) -> F(c(d(c(d(x'')))), y'')
F(c(x'), b(a(y''''))) -> F(x', a(b(a(y''''))))
F(c(x''), a(y'')) -> F(x'', a(a(y'')))
F(d(x''''), a(b(y'))) -> F(c(d(d(x''''))), y')
F(c(d(x'')), y'') -> F(d(x''), a(y''))
F(d(x''), b(y'')) -> F(x'', b(b(y'')))
F(d(x''), a(y'')) -> F(x'', b(a(y'')))
F(c(x'), b(b(y''''))) -> F(x', a(b(b(y''''))))


Rule:

none


Strategy:

innermost




Using Semantic Labelling, the DP problem could be transformed. The following model was found:
F(x0, x1)=  1
c(x0)=  x0
d(x0)=  0
a(x0)=  1
b(x0)=  0

From the dependency graph we obtain 2 (labeled) SCCs which each result in correspondingDP problem.


   R
     ↳DPs
       →DP Problem 1
         ↳MRR
           →DP Problem 2
             ↳NOC
             ...
               →DP Problem 7
                 ↳Modular Removal of Rules


Dependency Pairs:

F01(d0(x''''), a0(b1(y'))) -> F01(c0(d0(d0(x''''))), y')
F11(x', a0(b0(b1(y'''''')))) -> F00(c0(d1(x')), b1(y''''''))
F10(c1(x'), b0(b1(y''''))) -> F11(x', a0(b0(b1(y''''))))
F00(d1(x''), b1(y'')) -> F10(x'', b0(b1(y'')))
F11(x', a0(b0(b0(y'''''')))) -> F00(c0(d1(x')), b0(y''''''))
F10(c1(x'), b0(b0(y''''))) -> F11(x', a0(b0(b0(y''''))))
F00(d1(x''), b0(y'')) -> F10(x'', b0(b0(y'')))
F00(d0(x''), b0(y'')) -> F00(x'', b0(b0(y'')))
F00(d0(x''), b1(y'')) -> F00(x'', b0(b1(y'')))
F11(x', a0(b1(a0(y'''''')))) -> F01(c0(d1(x')), a0(y''''''))
F10(c1(x'), b1(a0(y''''))) -> F11(x', a0(b1(a0(y''''))))
F01(d1(x''), a0(y'')) -> F10(x'', b1(a0(y'')))
F01(d1(x''''), a0(b1(y'))) -> F01(c0(d0(d1(x''''))), y')
F00(c0(d1(x'')), y'') -> F01(d1(x''), a0(y''))
F01(d0(x''), a0(y'')) -> F00(x'', b1(a0(y'')))
F01(d1(x''''), a0(b0(y'))) -> F00(c0(d0(d1(x''''))), y')
F01(d0(x''''), a0(b0(y'))) -> F00(c0(d0(d0(x''''))), y')
F11(x', a0(b1(a1(y'''''')))) -> F01(c0(d1(x')), a1(y''''''))
F10(c1(x'), b1(a1(y''''))) -> F11(x', a0(b1(a1(y''''))))
F01(d1(x''), a1(y'')) -> F10(x'', b1(a1(y'')))
F01(c0(d1(x'')), y'') -> F01(d1(x''), a1(y''))
F01(c0(x''), a0(y'')) -> F01(x'', a1(a0(y'')))
F00(c0(x'), b0(b1(y''''))) -> F01(x', a0(b0(b1(y''''))))
F01(c0(d1(x'')), a0(b0(y''))) -> F00(c0(d0(c0(d1(x'')))), y'')
F00(c0(x'), b0(b0(y''''))) -> F01(x', a0(b0(b0(y''''))))
F01(c0(d0(x'')), a0(b0(y''))) -> F00(c0(d0(c0(d0(x'')))), y'')
F01(c0(d1(x'')), a0(b1(y''))) -> F01(c0(d0(c0(d1(x'')))), y'')
F00(c0(x'), b1(a0(y''''))) -> F01(x', a0(b1(a0(y''''))))
F01(x', a0(b0(b1(y'''''')))) -> F00(c0(d0(x')), b1(y''''''))
F00(c0(d0(x'')), y'') -> F01(d0(x''), a0(y''))
F01(x', a0(b0(b0(y'''''')))) -> F00(c0(d0(x')), b0(y''''''))
F01(c0(d0(x'')), a0(b1(y''))) -> F01(c0(d0(c0(d0(x'')))), y'')
F00(c0(x'), b1(a1(y''''))) -> F01(x', a0(b1(a1(y''''))))
F01(d0(x''), a1(y'')) -> F00(x'', b1(a1(y'')))
F01(c0(d0(x'')), y'') -> F01(d0(x''), a1(y''))
F01(c0(x''), a1(y'')) -> F01(x'', a1(a1(y'')))
F01(x', a0(b1(a1(y'''''')))) -> F01(c0(d0(x')), a1(y''''''))
F01(x', a0(b1(a0(y'''''')))) -> F01(c0(d0(x')), a0(y''''''))


Rule:

none


Strategy:

innermost




We have the following set of usable rules: none
To remove rules and DPs from this DP problem we used the following monotonic and CE-compatible order: Polynomial ordering.
Polynomial interpretation:
  POL(F_00(x1, x2))=  x1 + x2  
  POL(a_1(x1))=  x1  
  POL(b_0(x1))=  x1  
  POL(c_1(x1))=  x1  
  POL(d_0(x1))=  x1  
  POL(a_0(x1))=  x1  
  POL(F_11(x1, x2))=  x1 + x2  
  POL(F_01(x1, x2))=  x1 + x2  
  POL(b_1(x1))=  x1  
  POL(c_0(x1))=  x1  
  POL(d_1(x1))=  x1  
  POL(F_10(x1, x2))=  x1 + x2  

We have the following set D of usable symbols: {F00, a1, b0, d0, a0, F11, F01, c0, d1, b1, F10}
The following Dependency Pairs can be deleted as they contain symbols in their lhs which do not occur in D:

F10(c1(x'), b0(b1(y''''))) -> F11(x', a0(b0(b1(y''''))))
F10(c1(x'), b0(b0(y''''))) -> F11(x', a0(b0(b0(y''''))))
F10(c1(x'), b1(a0(y''''))) -> F11(x', a0(b1(a0(y''''))))
F10(c1(x'), b1(a1(y''''))) -> F11(x', a0(b1(a1(y''''))))

No Rules can be deleted.

The result of this processor delivers one new DP problem.



   R
     ↳DPs
       →DP Problem 1
         ↳MRR
           →DP Problem 2
             ↳NOC
             ...
               →DP Problem 9
                 ↳Modular Removal of Rules


Dependency Pairs:

F00(d0(x''), b0(y'')) -> F00(x'', b0(b0(y'')))
F00(d0(x''), b1(y'')) -> F00(x'', b0(b1(y'')))
F01(d1(x''''), a0(b1(y'))) -> F01(c0(d0(d1(x''''))), y')
F00(c0(d1(x'')), y'') -> F01(d1(x''), a0(y''))
F01(d0(x''), a0(y'')) -> F00(x'', b1(a0(y'')))
F01(d1(x''''), a0(b0(y'))) -> F00(c0(d0(d1(x''''))), y')
F01(d0(x''''), a0(b0(y'))) -> F00(c0(d0(d0(x''''))), y')
F01(c0(x''), a0(y'')) -> F01(x'', a1(a0(y'')))
F00(c0(x'), b0(b1(y''''))) -> F01(x', a0(b0(b1(y''''))))
F01(c0(d1(x'')), a0(b0(y''))) -> F00(c0(d0(c0(d1(x'')))), y'')
F00(c0(x'), b0(b0(y''''))) -> F01(x', a0(b0(b0(y''''))))
F01(c0(d0(x'')), a0(b0(y''))) -> F00(c0(d0(c0(d0(x'')))), y'')
F01(c0(d1(x'')), a0(b1(y''))) -> F01(c0(d0(c0(d1(x'')))), y'')
F00(c0(x'), b1(a0(y''''))) -> F01(x', a0(b1(a0(y''''))))
F01(x', a0(b0(b1(y'''''')))) -> F00(c0(d0(x')), b1(y''''''))
F00(c0(d0(x'')), y'') -> F01(d0(x''), a0(y''))
F01(x', a0(b0(b0(y'''''')))) -> F00(c0(d0(x')), b0(y''''''))
F01(c0(d0(x'')), a0(b1(y''))) -> F01(c0(d0(c0(d0(x'')))), y'')
F00(c0(x'), b1(a1(y''''))) -> F01(x', a0(b1(a1(y''''))))
F01(d0(x''), a1(y'')) -> F00(x'', b1(a1(y'')))
F01(c0(d0(x'')), y'') -> F01(d0(x''), a1(y''))
F01(c0(x''), a1(y'')) -> F01(x'', a1(a1(y'')))
F01(x', a0(b1(a1(y'''''')))) -> F01(c0(d0(x')), a1(y''''''))
F01(x', a0(b1(a0(y'''''')))) -> F01(c0(d0(x')), a0(y''''''))
F01(d0(x''''), a0(b1(y'))) -> F01(c0(d0(d0(x''''))), y')


Rule:

none


Strategy:

innermost




We have the following set of usable rules: none
To remove rules and DPs from this DP problem we used the following monotonic and CE-compatible order: Polynomial ordering.
Polynomial interpretation:
  POL(F_00(x1, x2))=  x1 + x2  
  POL(a_1(x1))=  x1  
  POL(b_0(x1))=  x1  
  POL(d_0(x1))=  x1  
  POL(a_0(x1))=  x1  
  POL(F_01(x1, x2))=  1 + x1 + x2  
  POL(b_1(x1))=  1 + x1  
  POL(d_1(x1))=  x1  
  POL(c_0(x1))=  1 + x1  

We have the following set D of usable symbols: {F00, a1, b0, d0, a0, F01, b1, c0, d1}
The following Dependency Pairs can be deleted as the lhs is strictly greater than the corresponding rhs:

F01(c0(x''), a0(y'')) -> F01(x'', a1(a0(y'')))
F01(c0(d0(x'')), y'') -> F01(d0(x''), a1(y''))
F01(c0(x''), a1(y'')) -> F01(x'', a1(a1(y'')))

No Rules can be deleted.

The result of this processor delivers one new DP problem.



   R
     ↳DPs
       →DP Problem 1
         ↳MRR
           →DP Problem 2
             ↳NOC
             ...
               →DP Problem 10
                 ↳Unlabel


Dependency Pairs:

F00(d0(x''), b1(y'')) -> F00(x'', b0(b1(y'')))
F01(d0(x''''), a0(b0(y'))) -> F00(c0(d0(d0(x''''))), y')
F01(c0(d1(x'')), a0(b0(y''))) -> F00(c0(d0(c0(d1(x'')))), y'')
F00(c0(x'), b0(b1(y''''))) -> F01(x', a0(b0(b1(y''''))))
F01(d1(x''''), a0(b0(y'))) -> F00(c0(d0(d1(x''''))), y')
F00(c0(d1(x'')), y'') -> F01(d1(x''), a0(y''))
F01(d0(x''), a0(y'')) -> F00(x'', b1(a0(y'')))
F01(d1(x''''), a0(b1(y'))) -> F01(c0(d0(d1(x''''))), y')
F01(d0(x''''), a0(b1(y'))) -> F01(c0(d0(d0(x''''))), y')
F01(c0(d1(x'')), a0(b1(y''))) -> F01(c0(d0(c0(d1(x'')))), y'')
F00(c0(x'), b1(a1(y''''))) -> F01(x', a0(b1(a1(y''''))))
F01(x', a0(b0(b1(y'''''')))) -> F00(c0(d0(x')), b1(y''''''))
F01(c0(d0(x'')), a0(b1(y''))) -> F01(c0(d0(c0(d0(x'')))), y'')
F00(c0(x'), b1(a0(y''''))) -> F01(x', a0(b1(a0(y''''))))
F01(c0(d0(x'')), a0(b0(y''))) -> F00(c0(d0(c0(d0(x'')))), y'')
F00(c0(x'), b0(b0(y''''))) -> F01(x', a0(b0(b0(y''''))))
F01(x', a0(b0(b0(y'''''')))) -> F00(c0(d0(x')), b0(y''''''))
F01(x', a0(b1(a0(y'''''')))) -> F01(c0(d0(x')), a0(y''''''))
F00(c0(d0(x'')), y'') -> F01(d0(x''), a0(y''))
F00(d0(x''), b0(y'')) -> F00(x'', b0(b0(y'')))


Rule:

none


Strategy:

innermost




Removed all semantic labels.

   R
     ↳DPs
       →DP Problem 1
         ↳MRR
           →DP Problem 2
             ↳NOC
             ...
               →DP Problem 11
                 ↳Instantiation Transformation


Dependency Pairs:

F(c(d(x'')), a(b(y''))) -> F(c(d(c(d(x'')))), y'')
F(x', a(b(a(y'''''')))) -> F(c(d(x')), a(y''''''))
F(c(x'), b(b(y''''))) -> F(x', a(b(b(y''''))))
F(d(x''), a(y'')) -> F(x'', b(a(y'')))
F(c(d(x'')), y'') -> F(d(x''), a(y''))
F(d(x''''), a(b(y'))) -> F(c(d(d(x''''))), y')
F(d(x''), b(y'')) -> F(x'', b(b(y'')))
F(x', a(b(b(y'''''')))) -> F(c(d(x')), b(y''''''))
F(c(x'), b(a(y''''))) -> F(x', a(b(a(y''''))))


Rule:

none


Strategy:

innermost




On this DP problem, an Instantiation SCC transformation can be performed.
As a result of transforming the rule

F(c(d(x'')), y'') -> F(d(x''), a(y''))
eight new Dependency Pairs are created:

F(c(d(c(d(x'''')))), y'''') -> F(d(c(d(x''''))), a(y''''))
F(c(d(x'''')), a(y'''''''')) -> F(d(x''''), a(a(y'''''''')))
F(c(d(x'''')), a(b(b(y'''''')))) -> F(d(x''''), a(a(b(b(y'''''')))))
F(c(d(x'''')), b(a(y''''))) -> F(d(x''''), a(b(a(y''''))))
F(c(d(d(x''''''))), y'''') -> F(d(d(x'''''')), a(y''''))
F(c(d(x'''')), b(b(y''''))) -> F(d(x''''), a(b(b(y''''))))
F(c(d(x'''')), b(y'''''''')) -> F(d(x''''), a(b(y'''''''')))
F(c(d(x'''')), a(b(a(y'''''')))) -> F(d(x''''), a(a(b(a(y'''''')))))

The transformation is resulting in one new DP problem: 



   R
     ↳DPs
       →DP Problem 1
         ↳MRR
           →DP Problem 2
             ↳NOC
             ...
               →DP Problem 12
                 ↳Instantiation Transformation


Dependency Pairs:

F(c(d(x'''')), b(y'''''''')) -> F(d(x''''), a(b(y'''''''')))
F(c(d(x'''')), b(b(y''''))) -> F(d(x''''), a(b(b(y''''))))
F(c(d(x'''')), b(a(y''''))) -> F(d(x''''), a(b(a(y''''))))
F(c(d(x'''')), a(b(b(y'''''')))) -> F(d(x''''), a(a(b(b(y'''''')))))
F(c(d(x'''')), a(b(a(y'''''')))) -> F(d(x''''), a(a(b(a(y'''''')))))
F(c(d(d(x''''''))), y'''') -> F(d(d(x'''''')), a(y''''))
F(c(d(x'''')), a(y'''''''')) -> F(d(x''''), a(a(y'''''''')))
F(c(x'), b(a(y''''))) -> F(x', a(b(a(y''''))))
F(d(x''''), a(b(y'))) -> F(c(d(d(x''''))), y')
F(c(d(c(d(x'''')))), y'''') -> F(d(c(d(x''''))), a(y''''))
F(d(x''), b(y'')) -> F(x'', b(b(y'')))
F(d(x''), a(y'')) -> F(x'', b(a(y'')))
F(c(x'), b(b(y''''))) -> F(x', a(b(b(y''''))))
F(x', a(b(b(y'''''')))) -> F(c(d(x')), b(y''''''))
F(x', a(b(a(y'''''')))) -> F(c(d(x')), a(y''''''))
F(c(d(x'')), a(b(y''))) -> F(c(d(c(d(x'')))), y'')


Rule:

none


Strategy:

innermost




On this DP problem, an Instantiation SCC transformation can be performed.
As a result of transforming the rule

F(d(x''), a(y'')) -> F(x'', b(a(y'')))
10 new Dependency Pairs are created:

F(d(x''''), a(b(b(y'''''')))) -> F(x'''', b(a(b(b(y'''''')))))
F(d(x''''), a(b(a(y'''''')))) -> F(x'''', b(a(b(a(y'''''')))))
F(d(c(d(x''''''))), a(y''')) -> F(c(d(x'''''')), b(a(y''')))
F(d(x'''), a(a(y''''''''''))) -> F(x''', b(a(a(y''''''''''))))
F(d(x'''), a(a(b(b(y''''''''))))) -> F(x''', b(a(a(b(b(y''''''''))))))
F(d(x'''), a(b(a(y'''''')))) -> F(x''', b(a(b(a(y'''''')))))
F(d(d(x'''''''')), a(y''')) -> F(d(x''''''''), b(a(y''')))
F(d(x'''), a(b(b(y'''''')))) -> F(x''', b(a(b(b(y'''''')))))
F(d(x'''), a(b(y''''''''''))) -> F(x''', b(a(b(y''''''''''))))
F(d(x'''), a(a(b(a(y''''''''))))) -> F(x''', b(a(a(b(a(y''''''''))))))

The transformation is resulting in one new DP problem: 



   R
     ↳DPs
       →DP Problem 1
         ↳MRR
           →DP Problem 2
             ↳NOC
             ...
               →DP Problem 13
                 ↳Instantiation Transformation


Dependency Pairs:

F(c(d(x'''')), a(b(b(y'''''')))) -> F(d(x''''), a(a(b(b(y'''''')))))
F(c(d(x'''')), a(b(a(y'''''')))) -> F(d(x''''), a(a(b(a(y'''''')))))
F(c(d(x'''')), a(y'''''''')) -> F(d(x''''), a(a(y'''''''')))
F(c(d(x'''')), b(b(y''''))) -> F(d(x''''), a(b(b(y''''))))
F(d(x'''), a(a(b(a(y''''''''))))) -> F(x''', b(a(a(b(a(y''''''''))))))
F(d(x'''), a(b(b(y'''''')))) -> F(x''', b(a(b(b(y'''''')))))
F(d(x'''), a(a(b(b(y''''''''))))) -> F(x''', b(a(a(b(b(y''''''''))))))
F(d(x'''), a(a(y''''''''''))) -> F(x''', b(a(a(y''''''''''))))
F(d(x'''), a(b(y''''''''''))) -> F(x''', b(a(b(y''''''''''))))
F(d(d(x'''''''')), a(y''')) -> F(d(x''''''''), b(a(y''')))
F(d(x'''), a(b(a(y'''''')))) -> F(x''', b(a(b(a(y'''''')))))
F(d(c(d(x''''''))), a(y''')) -> F(c(d(x'''''')), b(a(y''')))
F(c(d(x'''')), b(a(y''''))) -> F(d(x''''), a(b(a(y''''))))
F(d(x''''), a(b(a(y'''''')))) -> F(x'''', b(a(b(a(y'''''')))))
F(c(d(d(x''''''))), y'''') -> F(d(d(x'''''')), a(y''''))
F(d(x''), b(y'')) -> F(x'', b(b(y'')))
F(d(x''''), a(b(b(y'''''')))) -> F(x'''', b(a(b(b(y'''''')))))
F(c(d(c(d(x'''')))), y'''') -> F(d(c(d(x''''))), a(y''''))
F(c(x'), b(a(y''''))) -> F(x', a(b(a(y''''))))
F(x', a(b(b(y'''''')))) -> F(c(d(x')), b(y''''''))
F(d(x''''), a(b(y'))) -> F(c(d(d(x''''))), y')
F(c(x'), b(b(y''''))) -> F(x', a(b(b(y''''))))
F(c(d(x'')), a(b(y''))) -> F(c(d(c(d(x'')))), y'')
F(x', a(b(a(y'''''')))) -> F(c(d(x')), a(y''''''))
F(c(d(x'''')), b(y'''''''')) -> F(d(x''''), a(b(y'''''''')))


Rule:

none


Strategy:

innermost




On this DP problem, an Instantiation SCC transformation can be performed.
As a result of transforming the rule

F(d(x''), b(y'')) -> F(x'', b(b(y'')))
eight new Dependency Pairs are created:

F(d(x''''), b(b(y''''))) -> F(x'''', b(b(b(y''''))))
F(d(x'''), b(a(b(b(y''''''''))))) -> F(x''', b(b(a(b(b(y''''''''))))))
F(d(x'''), b(a(b(a(y''''''''))))) -> F(x''', b(b(a(b(a(y''''''''))))))
F(d(x'''), b(a(a(y'''''''''''')))) -> F(x''', b(b(a(a(y'''''''''''')))))
F(d(x'''), b(a(a(b(b(y'''''''''')))))) -> F(x''', b(b(a(a(b(b(y'''''''''')))))))
F(d(x'''), b(a(y'''''))) -> F(x''', b(b(a(y'''''))))
F(d(x'''), b(a(b(y'''''''''''')))) -> F(x''', b(b(a(b(y'''''''''''')))))
F(d(x'''), b(a(a(b(a(y'''''''''')))))) -> F(x''', b(b(a(a(b(a(y'''''''''')))))))

The transformation is resulting in one new DP problem: 



   R
     ↳DPs
       →DP Problem 1
         ↳MRR
           →DP Problem 2
             ↳NOC
             ...
               →DP Problem 14
                 ↳Instantiation Transformation


Dependency Pairs:

F(c(d(x'''')), a(b(a(y'''''')))) -> F(d(x''''), a(a(b(a(y'''''')))))
F(d(x'''), a(a(b(a(y''''''''))))) -> F(x''', b(a(a(b(a(y''''''''))))))
F(d(x'''), a(b(y''''''''''))) -> F(x''', b(a(b(y''''''''''))))
F(d(x'''), a(b(b(y'''''')))) -> F(x''', b(a(b(b(y'''''')))))
F(d(x'''), b(a(a(b(a(y'''''''''')))))) -> F(x''', b(b(a(a(b(a(y'''''''''')))))))
F(d(x'''), b(a(b(y'''''''''''')))) -> F(x''', b(b(a(b(y'''''''''''')))))
F(d(x'''), b(a(y'''''))) -> F(x''', b(b(a(y'''''))))
F(d(x'''), b(a(a(b(b(y'''''''''')))))) -> F(x''', b(b(a(a(b(b(y'''''''''')))))))
F(d(x'''), b(a(a(y'''''''''''')))) -> F(x''', b(b(a(a(y'''''''''''')))))
F(d(x''''), b(b(y''''))) -> F(x'''', b(b(b(y''''))))
F(d(x'''), b(a(b(b(y''''''''))))) -> F(x''', b(b(a(b(b(y''''''''))))))
F(d(d(x'''''''')), a(y''')) -> F(d(x''''''''), b(a(y''')))
F(c(d(x'''')), b(b(y''''))) -> F(d(x''''), a(b(b(y''''))))
F(d(x'''), b(a(b(a(y''''''''))))) -> F(x''', b(b(a(b(a(y''''''''))))))
F(d(x'''), a(b(a(y'''''')))) -> F(x''', b(a(b(a(y'''''')))))
F(c(d(x'''')), b(y'''''''')) -> F(d(x''''), a(b(y'''''''')))
F(d(x'''), a(a(b(b(y''''''''))))) -> F(x''', b(a(a(b(b(y''''''''))))))
F(c(d(d(x''''''))), y'''') -> F(d(d(x'''''')), a(y''''))
F(d(x''''), a(b(a(y'''''')))) -> F(x'''', b(a(b(a(y'''''')))))
F(c(d(x'''')), b(a(y''''))) -> F(d(x''''), a(b(a(y''''))))
F(d(x''''), a(b(b(y'''''')))) -> F(x'''', b(a(b(b(y'''''')))))
F(c(d(c(d(x'''')))), y'''') -> F(d(c(d(x''''))), a(y''''))
F(d(x'''), a(a(y''''''''''))) -> F(x''', b(a(a(y''''''''''))))
F(c(d(x'''')), a(y'''''''')) -> F(d(x''''), a(a(y'''''''')))
F(d(x''''), a(b(y'))) -> F(c(d(d(x''''))), y')
F(c(x'), b(b(y''''))) -> F(x', a(b(b(y''''))))
F(x', a(b(b(y'''''')))) -> F(c(d(x')), b(y''''''))
F(x', a(b(a(y'''''')))) -> F(c(d(x')), a(y''''''))
F(c(d(x'')), a(b(y''))) -> F(c(d(c(d(x'')))), y'')
F(c(x'), b(a(y''''))) -> F(x', a(b(a(y''''))))
F(d(c(d(x''''''))), a(y''')) -> F(c(d(x'''''')), b(a(y''')))
F(c(d(x'''')), a(b(b(y'''''')))) -> F(d(x''''), a(a(b(b(y'''''')))))


Rule:

none


Strategy:

innermost




On this DP problem, an Instantiation SCC transformation can be performed.
As a result of transforming the rule

F(c(x'), b(b(y''''))) -> F(x', a(b(b(y''''))))
11 new Dependency Pairs are created:

F(c(d(c(d(x'''')))), b(b(y'''''))) -> F(d(c(d(x''''))), a(b(b(y'''''))))
F(c(d(d(x''''''))), b(b(y'''''))) -> F(d(d(x'''''')), a(b(b(y'''''))))
F(c(d(x''')), b(b(y'''''))) -> F(d(x'''), a(b(b(y'''''))))
F(c(x''), b(b(b(y'''''')))) -> F(x'', a(b(b(b(y'''''')))))
F(c(x''), b(b(a(b(b(y'''''''''')))))) -> F(x'', a(b(b(a(b(b(y'''''''''')))))))
F(c(x''), b(b(a(b(a(y'''''''''')))))) -> F(x'', a(b(b(a(b(a(y'''''''''')))))))
F(c(x''), b(b(a(a(y''''''''''''''))))) -> F(x'', a(b(b(a(a(y''''''''''''''))))))
F(c(x''), b(b(a(a(b(b(y''''''''''''))))))) -> F(x'', a(b(b(a(a(b(b(y''''''''''''))))))))
F(c(x''), b(b(a(y''''''')))) -> F(x'', a(b(b(a(y''''''')))))
F(c(x''), b(b(a(b(y''''''''''''''))))) -> F(x'', a(b(b(a(b(y''''''''''''''))))))
F(c(x''), b(b(a(a(b(a(y''''''''''''))))))) -> F(x'', a(b(b(a(a(b(a(y''''''''''''))))))))

The transformation is resulting in one new DP problem: 



   R
     ↳DPs
       →DP Problem 1
         ↳MRR
           →DP Problem 2
             ↳NOC
             ...
               →DP Problem 15
                 ↳Instantiation Transformation


Dependency Pairs:

F(d(x'''), a(a(b(a(y''''''''))))) -> F(x''', b(a(a(b(a(y''''''''))))))
F(d(x'''), b(a(a(b(a(y'''''''''')))))) -> F(x''', b(b(a(a(b(a(y'''''''''')))))))
F(c(x''), b(b(b(y'''''')))) -> F(x'', a(b(b(b(y'''''')))))
F(c(x''), b(b(a(b(y''''''''''''''))))) -> F(x'', a(b(b(a(b(y''''''''''''''))))))
F(c(x''), b(b(a(b(a(y'''''''''')))))) -> F(x'', a(b(b(a(b(a(y'''''''''')))))))
F(d(x'''), b(a(a(b(b(y'''''''''')))))) -> F(x''', b(b(a(a(b(b(y'''''''''')))))))
F(c(x''), b(b(a(a(b(a(y''''''''''''))))))) -> F(x'', a(b(b(a(a(b(a(y''''''''''''))))))))
F(c(x''), b(b(a(y''''''')))) -> F(x'', a(b(b(a(y''''''')))))
F(c(x''), b(b(a(a(b(b(y''''''''''''))))))) -> F(x'', a(b(b(a(a(b(b(y''''''''''''))))))))
F(c(x''), b(b(a(a(y''''''''''''''))))) -> F(x'', a(b(b(a(a(y''''''''''''''))))))
F(d(x'''), b(a(a(y'''''''''''')))) -> F(x''', b(b(a(a(y'''''''''''')))))
F(d(x'''), a(a(b(b(y''''''''))))) -> F(x''', b(a(a(b(b(y''''''''))))))
F(c(d(x'''')), a(b(b(y'''''')))) -> F(d(x''''), a(a(b(b(y'''''')))))
F(c(x''), b(b(a(b(b(y'''''''''')))))) -> F(x'', a(b(b(a(b(b(y'''''''''')))))))
F(c(d(x''')), b(b(y'''''))) -> F(d(x'''), a(b(b(y'''''))))
F(d(x'''), b(a(b(y'''''''''''')))) -> F(x''', b(b(a(b(y'''''''''''')))))
F(d(x'''), a(b(y''''''''''))) -> F(x''', b(a(b(y''''''''''))))
F(c(d(d(x''''''))), b(b(y'''''))) -> F(d(d(x'''''')), a(b(b(y'''''))))
F(d(x'''), b(a(y'''''))) -> F(x''', b(b(a(y'''''))))
F(d(x'''), a(b(b(y'''''')))) -> F(x''', b(a(b(b(y'''''')))))
F(c(d(c(d(x'''')))), b(b(y'''''))) -> F(d(c(d(x''''))), a(b(b(y'''''))))
F(d(x''''), b(b(y''''))) -> F(x'''', b(b(b(y''''))))
F(d(x'''), b(a(b(b(y''''''''))))) -> F(x''', b(b(a(b(b(y''''''''))))))
F(d(d(x'''''''')), a(y''')) -> F(d(x''''''''), b(a(y''')))
F(c(d(x'''')), b(b(y''''))) -> F(d(x''''), a(b(b(y''''))))
F(d(x'''), b(a(b(a(y''''''''))))) -> F(x''', b(b(a(b(a(y''''''''))))))
F(d(x'''), a(b(a(y'''''')))) -> F(x''', b(a(b(a(y'''''')))))
F(c(d(x'''')), b(y'''''''')) -> F(d(x''''), a(b(y'''''''')))
F(d(x''''), a(b(b(y'''''')))) -> F(x'''', b(a(b(b(y'''''')))))
F(c(d(d(x''''''))), y'''') -> F(d(d(x'''''')), a(y''''))
F(d(x''''), a(b(a(y'''''')))) -> F(x'''', b(a(b(a(y'''''')))))
F(c(d(x'''')), b(a(y''''))) -> F(d(x''''), a(b(a(y''''))))
F(d(x'''), a(a(y''''''''''))) -> F(x''', b(a(a(y''''''''''))))
F(c(d(x'''')), a(y'''''''')) -> F(d(x''''), a(a(y'''''''')))
F(d(x''''), a(b(y'))) -> F(c(d(d(x''''))), y')
F(c(d(c(d(x'''')))), y'''') -> F(d(c(d(x''''))), a(y''''))
F(x', a(b(b(y'''''')))) -> F(c(d(x')), b(y''''''))
F(x', a(b(a(y'''''')))) -> F(c(d(x')), a(y''''''))
F(c(d(x'')), a(b(y''))) -> F(c(d(c(d(x'')))), y'')
F(c(x'), b(a(y''''))) -> F(x', a(b(a(y''''))))
F(d(c(d(x''''''))), a(y''')) -> F(c(d(x'''''')), b(a(y''')))
F(c(d(x'''')), a(b(a(y'''''')))) -> F(d(x''''), a(a(b(a(y'''''')))))


Rule:

none


Strategy:

innermost




On this DP problem, an Instantiation SCC transformation can be performed.
As a result of transforming the rule

F(x', a(b(b(y'''''')))) -> F(c(d(x')), b(y''''''))
17 new Dependency Pairs are created:

F(c(d(c(d(x'''')))), a(b(b(y''''''')))) -> F(c(d(c(d(c(d(x'''')))))), b(y'''''''))
F(c(d(x''')), a(b(b(y'''''''')))) -> F(c(d(c(d(x''')))), b(y''''''''))
F(c(d(d(x''''''))), a(b(b(y''''''')))) -> F(c(d(c(d(d(x''''''))))), b(y'''''''))
F(d(c(d(x''''''))), a(b(b(y''''''')))) -> F(c(d(d(c(d(x''''''))))), b(y'''''''))
F(d(d(x'''''''')), a(b(b(y''''''')))) -> F(c(d(d(d(x'''''''')))), b(y'''''''))
F(d(x''''''), a(b(b(y''''''')))) -> F(c(d(d(x''''''))), b(y'''''''))
F(d(c(d(x''''''))), a(b(b(y'''''''')))) -> F(c(d(d(c(d(x''''''))))), b(y''''''''))
F(d(d(x'''''''')), a(b(b(y'''''''')))) -> F(c(d(d(d(x'''''''')))), b(y''''''''))
F(d(x'''''), a(b(b(y'''''''')))) -> F(c(d(d(x'''''))), b(y''''''''))
F(x'', a(b(b(b(y''''''''))))) -> F(c(d(x'')), b(b(y'''''''')))
F(x'', a(b(b(a(b(b(y''''''''''''))))))) -> F(c(d(x'')), b(a(b(b(y'''''''''''')))))
F(x'', a(b(b(a(b(a(y''''''''''''))))))) -> F(c(d(x'')), b(a(b(a(y'''''''''''')))))
F(x'', a(b(b(a(a(y'''''''''''''''')))))) -> F(c(d(x'')), b(a(a(y''''''''''''''''))))
F(x'', a(b(b(a(a(b(b(y'''''''''''''')))))))) -> F(c(d(x'')), b(a(a(b(b(y''''''''''''''))))))
F(x'', a(b(b(a(y'''''''''))))) -> F(c(d(x'')), b(a(y''''''''')))
F(x'', a(b(b(a(b(y'''''''''''''''')))))) -> F(c(d(x'')), b(a(b(y''''''''''''''''))))
F(x'', a(b(b(a(a(b(a(y'''''''''''''')))))))) -> F(c(d(x'')), b(a(a(b(a(y''''''''''''''))))))

The transformation is resulting in one new DP problem: 



   R
     ↳DPs
       →DP Problem 1
         ↳MRR
           →DP Problem 2
             ↳NOC
             ...
               →DP Problem 16
                 ↳Instantiation Transformation


Dependency Pairs:

F(c(d(x'''')), a(b(a(y'''''')))) -> F(d(x''''), a(a(b(a(y'''''')))))
F(x'', a(b(b(b(y''''''''))))) -> F(c(d(x'')), b(b(y'''''''')))
F(d(x'''), a(a(b(b(y''''''''))))) -> F(x''', b(a(a(b(b(y''''''''))))))
F(d(x'''), b(a(a(b(a(y'''''''''')))))) -> F(x''', b(b(a(a(b(a(y'''''''''')))))))
F(d(x'''), b(a(a(b(b(y'''''''''')))))) -> F(x''', b(b(a(a(b(b(y'''''''''')))))))
F(x'', a(b(b(a(a(b(b(y'''''''''''''')))))))) -> F(c(d(x'')), b(a(a(b(b(y''''''''''''''))))))
F(x'', a(b(b(a(b(y'''''''''''''''')))))) -> F(c(d(x'')), b(a(b(y''''''''''''''''))))
F(x'', a(b(b(a(b(a(y''''''''''''))))))) -> F(c(d(x'')), b(a(b(a(y'''''''''''')))))
F(x'', a(b(b(a(b(b(y''''''''''''))))))) -> F(c(d(x'')), b(a(b(b(y'''''''''''')))))
F(x'', a(b(b(a(a(b(a(y'''''''''''''')))))))) -> F(c(d(x'')), b(a(a(b(a(y''''''''''''''))))))
F(x'', a(b(b(a(y'''''''''))))) -> F(c(d(x'')), b(a(y''''''''')))
F(x'', a(b(b(a(a(y'''''''''''''''')))))) -> F(c(d(x'')), b(a(a(y''''''''''''''''))))
F(d(x'''''), a(b(b(y'''''''')))) -> F(c(d(d(x'''''))), b(y''''''''))
F(d(d(x'''''''')), a(b(b(y'''''''')))) -> F(c(d(d(d(x'''''''')))), b(y''''''''))
F(c(x''), b(b(a(a(b(a(y''''''''''''))))))) -> F(x'', a(b(b(a(a(b(a(y''''''''''''))))))))
F(d(c(d(x''''''))), a(b(b(y'''''''')))) -> F(c(d(d(c(d(x''''''))))), b(y''''''''))
F(c(x''), b(b(a(b(y''''''''''''''))))) -> F(x'', a(b(b(a(b(y''''''''''''''))))))
F(d(x''''''), a(b(b(y''''''')))) -> F(c(d(d(x''''''))), b(y'''''''))
F(c(x''), b(b(a(y''''''')))) -> F(x'', a(b(b(a(y''''''')))))
F(d(d(x'''''''')), a(b(b(y''''''')))) -> F(c(d(d(d(x'''''''')))), b(y'''''''))
F(c(x''), b(b(a(a(b(b(y''''''''''''))))))) -> F(x'', a(b(b(a(a(b(b(y''''''''''''))))))))
F(c(d(d(x''''''))), a(b(b(y''''''')))) -> F(c(d(c(d(d(x''''''))))), b(y'''''''))
F(c(x''), b(b(a(b(a(y'''''''''')))))) -> F(x'', a(b(b(a(b(a(y'''''''''')))))))
F(c(d(x''')), a(b(b(y'''''''')))) -> F(c(d(c(d(x''')))), b(y''''''''))
F(c(x''), b(b(a(b(b(y'''''''''')))))) -> F(x'', a(b(b(a(b(b(y'''''''''')))))))
F(c(d(c(d(x'''')))), a(b(b(y''''''')))) -> F(c(d(c(d(c(d(x'''')))))), b(y'''''''))
F(c(x''), b(b(a(a(y''''''''''''''))))) -> F(x'', a(b(b(a(a(y''''''''''''''))))))
F(d(x'''), b(a(a(y'''''''''''')))) -> F(x''', b(b(a(a(y'''''''''''')))))
F(d(x'''), a(a(y''''''''''))) -> F(x''', b(a(a(y''''''''''))))
F(c(d(x'''')), a(b(b(y'''''')))) -> F(d(x''''), a(a(b(b(y'''''')))))
F(c(x''), b(b(b(y'''''')))) -> F(x'', a(b(b(b(y'''''')))))
F(d(c(d(x''''''))), a(b(b(y''''''')))) -> F(c(d(d(c(d(x''''''))))), b(y'''''''))
F(c(d(x''')), b(b(y'''''))) -> F(d(x'''), a(b(b(y'''''))))
F(d(x'''), b(a(b(y'''''''''''')))) -> F(x''', b(b(a(b(y'''''''''''')))))
F(d(x'''), a(b(y''''''''''))) -> F(x''', b(a(b(y''''''''''))))
F(c(d(d(x''''''))), b(b(y'''''))) -> F(d(d(x'''''')), a(b(b(y'''''))))
F(d(x'''), b(a(y'''''))) -> F(x''', b(b(a(y'''''))))
F(d(x'''), a(b(b(y'''''')))) -> F(x''', b(a(b(b(y'''''')))))
F(c(d(c(d(x'''')))), b(b(y'''''))) -> F(d(c(d(x''''))), a(b(b(y'''''))))
F(d(x''''), b(b(y''''))) -> F(x'''', b(b(b(y''''))))
F(d(x'''), b(a(b(b(y''''''''))))) -> F(x''', b(b(a(b(b(y''''''''))))))
F(d(d(x'''''''')), a(y''')) -> F(d(x''''''''), b(a(y''')))
F(c(d(x'''')), b(b(y''''))) -> F(d(x''''), a(b(b(y''''))))
F(d(x'''), b(a(b(a(y''''''''))))) -> F(x''', b(b(a(b(a(y''''''''))))))
F(d(x'''), a(b(a(y'''''')))) -> F(x''', b(a(b(a(y'''''')))))
F(c(d(x'''')), b(y'''''''')) -> F(d(x''''), a(b(y'''''''')))
F(d(x''''), a(b(b(y'''''')))) -> F(x'''', b(a(b(b(y'''''')))))
F(c(d(d(x''''''))), y'''') -> F(d(d(x'''''')), a(y''''))
F(d(x''''), a(b(a(y'''''')))) -> F(x'''', b(a(b(a(y'''''')))))
F(c(d(x'''')), b(a(y''''))) -> F(d(x''''), a(b(a(y''''))))
F(d(c(d(x''''''))), a(y''')) -> F(c(d(x'''''')), b(a(y''')))
F(c(d(x'''')), a(y'''''''')) -> F(d(x''''), a(a(y'''''''')))
F(d(x''''), a(b(y'))) -> F(c(d(d(x''''))), y')
F(c(d(c(d(x'''')))), y'''') -> F(d(c(d(x''''))), a(y''''))
F(x', a(b(a(y'''''')))) -> F(c(d(x')), a(y''''''))
F(c(d(x'')), a(b(y''))) -> F(c(d(c(d(x'')))), y'')
F(c(x'), b(a(y''''))) -> F(x', a(b(a(y''''))))
F(d(x'''), a(a(b(a(y''''''''))))) -> F(x''', b(a(a(b(a(y''''''''))))))


Rule:

none


Strategy:

innermost




On this DP problem, an Instantiation SCC transformation can be performed.
As a result of transforming the rule

F(c(x'), b(a(y''''))) -> F(x', a(b(a(y''''))))
23 new Dependency Pairs are created:

F(c(d(c(d(x'''')))), b(a(y'''''))) -> F(d(c(d(x''''))), a(b(a(y'''''))))
F(c(d(d(x''''''))), b(a(y'''''))) -> F(d(d(x'''''')), a(b(a(y'''''))))
F(c(x''), b(a(b(b(y''''''''))))) -> F(x'', a(b(a(b(b(y''''''''))))))
F(c(x''), b(a(b(a(y''''''''))))) -> F(x'', a(b(a(b(a(y''''''''))))))
F(c(d(x'''''''')), b(a(y''''''))) -> F(d(x''''''''), a(b(a(y''''''))))
F(c(x''), b(a(a(y'''''''''''')))) -> F(x'', a(b(a(a(y'''''''''''')))))
F(c(x''), b(a(a(b(b(y'''''''''')))))) -> F(x'', a(b(a(a(b(b(y'''''''''')))))))
F(c(x''), b(a(b(y'''''''''''')))) -> F(x'', a(b(a(b(y'''''''''''')))))
F(c(x''), b(a(a(b(a(y'''''''''')))))) -> F(x'', a(b(a(a(b(a(y'''''''''')))))))
F(c(d(c(d(c(d(x'''''')))))), b(a(y'''''))) -> F(d(c(d(c(d(x''''''))))), a(b(a(y'''''))))
F(c(d(c(d(x''''')))), b(a(y'''''))) -> F(d(c(d(x'''''))), a(b(a(y'''''))))
F(c(d(c(d(d(x''''''''))))), b(a(y'''''))) -> F(d(c(d(d(x'''''''')))), a(b(a(y'''''))))
F(c(d(d(c(d(x''''''''))))), b(a(y'''''))) -> F(d(d(c(d(x'''''''')))), a(b(a(y'''''))))
F(c(d(d(d(x'''''''''')))), b(a(y'''''))) -> F(d(d(d(x''''''''''))), a(b(a(y'''''))))
F(c(d(d(x''''''''))), b(a(y'''''))) -> F(d(d(x'''''''')), a(b(a(y'''''))))
F(c(d(d(x'''''''))), b(a(y'''''))) -> F(d(d(x''''''')), a(b(a(y'''''))))
F(c(d(x'''')), b(a(b(b(y''''''''''''''))))) -> F(d(x''''), a(b(a(b(b(y''''''''''''''))))))
F(c(d(x'''')), b(a(b(a(y''''''''''''''))))) -> F(d(x''''), a(b(a(b(a(y''''''''''''''))))))
F(c(d(x'''')), b(a(a(y'''''''''''''''''')))) -> F(d(x''''), a(b(a(a(y'''''''''''''''''')))))
F(c(d(x'''')), b(a(a(b(b(y'''''''''''''''')))))) -> F(d(x''''), a(b(a(a(b(b(y'''''''''''''''')))))))
F(c(d(x'''')), b(a(y'''''))) -> F(d(x''''), a(b(a(y'''''))))
F(c(d(x'''')), b(a(b(y'''''''''''''''''')))) -> F(d(x''''), a(b(a(b(y'''''''''''''''''')))))
F(c(d(x'''')), b(a(a(b(a(y'''''''''''''''')))))) -> F(d(x''''), a(b(a(a(b(a(y'''''''''''''''')))))))

The transformation is resulting in one new DP problem: 



   R
     ↳DPs
       →DP Problem 1
         ↳MRR
           →DP Problem 2
             ↳NOC
             ...
               →DP Problem 17
                 ↳Instantiation Transformation


Dependency Pairs:

F(d(x'''), a(a(b(a(y''''''''))))) -> F(x''', b(a(a(b(a(y''''''''))))))
F(d(x'''), b(a(a(b(a(y'''''''''')))))) -> F(x''', b(b(a(a(b(a(y'''''''''')))))))
F(d(x'''), b(a(a(b(b(y'''''''''')))))) -> F(x''', b(b(a(a(b(b(y'''''''''')))))))
F(d(x'''), b(a(a(y'''''''''''')))) -> F(x''', b(b(a(a(y'''''''''''')))))
F(x'', a(b(b(b(y''''''''))))) -> F(c(d(x'')), b(b(y'''''''')))
F(x'', a(b(b(a(a(b(b(y'''''''''''''')))))))) -> F(c(d(x'')), b(a(a(b(b(y''''''''''''''))))))
F(x'', a(b(b(a(b(y'''''''''''''''')))))) -> F(c(d(x'')), b(a(b(y''''''''''''''''))))
F(x'', a(b(b(a(b(a(y''''''''''''))))))) -> F(c(d(x'')), b(a(b(a(y'''''''''''')))))
F(x'', a(b(b(a(b(b(y''''''''''''))))))) -> F(c(d(x'')), b(a(b(b(y'''''''''''')))))
F(x'', a(b(b(a(a(b(a(y'''''''''''''')))))))) -> F(c(d(x'')), b(a(a(b(a(y''''''''''''''))))))
F(x'', a(b(b(a(y'''''''''))))) -> F(c(d(x'')), b(a(y''''''''')))
F(x'', a(b(b(a(a(y'''''''''''''''')))))) -> F(c(d(x'')), b(a(a(y''''''''''''''''))))
F(c(d(x'''')), b(a(a(b(a(y'''''''''''''''')))))) -> F(d(x''''), a(b(a(a(b(a(y'''''''''''''''')))))))
F(c(d(x'''')), b(a(a(b(b(y'''''''''''''''')))))) -> F(d(x''''), a(b(a(a(b(b(y'''''''''''''''')))))))
F(c(d(x'''')), b(a(a(y'''''''''''''''''')))) -> F(d(x''''), a(b(a(a(y'''''''''''''''''')))))
F(c(d(x'''')), b(a(b(b(y''''''''''''''))))) -> F(d(x''''), a(b(a(b(b(y''''''''''''''))))))
F(c(x''), b(a(a(b(a(y'''''''''')))))) -> F(x'', a(b(a(a(b(a(y'''''''''')))))))
F(c(x''), b(a(a(b(b(y'''''''''')))))) -> F(x'', a(b(a(a(b(b(y'''''''''')))))))
F(c(x''), b(a(a(y'''''''''''')))) -> F(x'', a(b(a(a(y'''''''''''')))))
F(c(x''), b(a(b(b(y''''''''))))) -> F(x'', a(b(a(b(b(y''''''''))))))
F(c(d(x'''')), b(a(b(y'''''''''''''''''')))) -> F(d(x''''), a(b(a(b(y'''''''''''''''''')))))
F(c(d(x'''')), b(a(y'''''))) -> F(d(x''''), a(b(a(y'''''))))
F(c(d(x'''')), b(a(b(a(y''''''''''''''))))) -> F(d(x''''), a(b(a(b(a(y''''''''''''''))))))
F(c(d(d(x'''''''))), b(a(y'''''))) -> F(d(d(x''''''')), a(b(a(y'''''))))
F(c(d(d(x''''''''))), b(a(y'''''))) -> F(d(d(x'''''''')), a(b(a(y'''''))))
F(c(d(d(d(x'''''''''')))), b(a(y'''''))) -> F(d(d(d(x''''''''''))), a(b(a(y'''''))))
F(c(d(d(c(d(x''''''''))))), b(a(y'''''))) -> F(d(d(c(d(x'''''''')))), a(b(a(y'''''))))
F(c(d(c(d(d(x''''''''))))), b(a(y'''''))) -> F(d(c(d(d(x'''''''')))), a(b(a(y'''''))))
F(c(d(c(d(x''''')))), b(a(y'''''))) -> F(d(c(d(x'''''))), a(b(a(y'''''))))
F(c(d(c(d(c(d(x'''''')))))), b(a(y'''''))) -> F(d(c(d(c(d(x''''''))))), a(b(a(y'''''))))
F(c(x''), b(a(b(y'''''''''''')))) -> F(x'', a(b(a(b(y'''''''''''')))))
F(c(d(x'''''''')), b(a(y''''''))) -> F(d(x''''''''), a(b(a(y''''''))))
F(c(x''), b(a(b(a(y''''''''))))) -> F(x'', a(b(a(b(a(y''''''''))))))
F(c(d(c(d(x'''')))), b(a(y'''''))) -> F(d(c(d(x''''))), a(b(a(y'''''))))
F(d(x'''), a(b(a(y'''''')))) -> F(x''', b(a(b(a(y'''''')))))
F(c(d(d(x''''''))), b(a(y'''''))) -> F(d(d(x'''''')), a(b(a(y'''''))))
F(d(x'''''), a(b(b(y'''''''')))) -> F(c(d(d(x'''''))), b(y''''''''))
F(c(x''), b(b(a(a(b(a(y''''''''''''))))))) -> F(x'', a(b(b(a(a(b(a(y''''''''''''))))))))
F(d(d(x'''''''')), a(b(b(y'''''''')))) -> F(c(d(d(d(x'''''''')))), b(y''''''''))
F(c(x''), b(b(a(b(y''''''''''''''))))) -> F(x'', a(b(b(a(b(y''''''''''''''))))))
F(d(c(d(x''''''))), a(b(b(y'''''''')))) -> F(c(d(d(c(d(x''''''))))), b(y''''''''))
F(c(x''), b(b(a(y''''''')))) -> F(x'', a(b(b(a(y''''''')))))
F(d(x''''''), a(b(b(y''''''')))) -> F(c(d(d(x''''''))), b(y'''''''))
F(c(x''), b(b(a(a(b(b(y''''''''''''))))))) -> F(x'', a(b(b(a(a(b(b(y''''''''''''))))))))
F(d(d(x'''''''')), a(b(b(y''''''')))) -> F(c(d(d(d(x'''''''')))), b(y'''''''))
F(c(x''), b(b(a(a(y''''''''''''''))))) -> F(x'', a(b(b(a(a(y''''''''''''''))))))
F(c(d(d(x''''''))), a(b(b(y''''''')))) -> F(c(d(c(d(d(x''''''))))), b(y'''''''))
F(c(x''), b(b(a(b(a(y'''''''''')))))) -> F(x'', a(b(b(a(b(a(y'''''''''')))))))
F(c(d(x''')), a(b(b(y'''''''')))) -> F(c(d(c(d(x''')))), b(y''''''''))
F(c(x''), b(b(a(b(b(y'''''''''')))))) -> F(x'', a(b(b(a(b(b(y'''''''''')))))))
F(c(d(c(d(x'''')))), a(b(b(y''''''')))) -> F(c(d(c(d(c(d(x'''')))))), b(y'''''''))
F(c(x''), b(b(b(y'''''')))) -> F(x'', a(b(b(b(y'''''')))))
F(d(c(d(x''''''))), a(b(b(y''''''')))) -> F(c(d(d(c(d(x''''''))))), b(y'''''''))
F(c(d(x''')), b(b(y'''''))) -> F(d(x'''), a(b(b(y'''''))))
F(d(x'''), b(a(b(y'''''''''''')))) -> F(x''', b(b(a(b(y'''''''''''')))))
F(d(x'''), a(b(y''''''''''))) -> F(x''', b(a(b(y''''''''''))))
F(c(d(d(x''''''))), b(b(y'''''))) -> F(d(d(x'''''')), a(b(b(y'''''))))
F(d(x'''), b(a(y'''''))) -> F(x''', b(b(a(y'''''))))
F(d(x'''), a(b(b(y'''''')))) -> F(x''', b(a(b(b(y'''''')))))
F(c(d(c(d(x'''')))), b(b(y'''''))) -> F(d(c(d(x''''))), a(b(b(y'''''))))
F(d(x''''), b(b(y''''))) -> F(x'''', b(b(b(y''''))))
F(d(x'''), b(a(b(b(y''''''''))))) -> F(x''', b(b(a(b(b(y''''''''))))))
F(d(d(x'''''''')), a(y''')) -> F(d(x''''''''), b(a(y''')))
F(c(d(x'''')), b(b(y''''))) -> F(d(x''''), a(b(b(y''''))))
F(d(x'''), b(a(b(a(y''''''''))))) -> F(x''', b(b(a(b(a(y''''''''))))))
F(d(x''''), a(b(a(y'''''')))) -> F(x'''', b(a(b(a(y'''''')))))
F(c(d(x'''')), b(y'''''''')) -> F(d(x''''), a(b(y'''''''')))
F(d(x''''), a(b(b(y'''''')))) -> F(x'''', b(a(b(b(y'''''')))))
F(c(d(d(x''''''))), y'''') -> F(d(d(x'''''')), a(y''''))
F(d(x'''), a(a(b(b(y''''''''))))) -> F(x''', b(a(a(b(b(y''''''''))))))
F(c(d(x'''')), a(b(b(y'''''')))) -> F(d(x''''), a(a(b(b(y'''''')))))
F(d(x''''), a(b(y'))) -> F(c(d(d(x''''))), y')
F(c(d(x'''')), b(a(y''''))) -> F(d(x''''), a(b(a(y''''))))
F(d(x'''), a(a(y''''''''''))) -> F(x''', b(a(a(y''''''''''))))
F(c(d(x'''')), a(y'''''''')) -> F(d(x''''), a(a(y'''''''')))
F(c(d(x'')), a(b(y''))) -> F(c(d(c(d(x'')))), y'')
F(x', a(b(a(y'''''')))) -> F(c(d(x')), a(y''''''))
F(c(d(c(d(x'''')))), y'''') -> F(d(c(d(x''''))), a(y''''))
F(d(c(d(x''''''))), a(y''')) -> F(c(d(x'''''')), b(a(y''')))
F(c(d(x'''')), a(b(a(y'''''')))) -> F(d(x''''), a(a(b(a(y'''''')))))


Rule:

none


Strategy:

innermost




On this DP problem, an Instantiation SCC transformation can be performed.
As a result of transforming the rule

F(x', a(b(a(y'''''')))) -> F(c(d(x')), a(y''''''))
29 new Dependency Pairs are created:

F(c(d(x''')), a(b(a(y'''''''')))) -> F(c(d(c(d(x''')))), a(y''''''''))
F(c(d(c(d(x'''')))), a(b(a(y''''''')))) -> F(c(d(c(d(c(d(x'''')))))), a(y'''''''))
F(c(d(d(x''''''))), a(b(a(y''''''')))) -> F(c(d(c(d(d(x''''''))))), a(y'''''''))
F(d(c(d(x''''''))), a(b(a(y''''''')))) -> F(c(d(d(c(d(x''''''))))), a(y'''''''))
F(d(x''''''), a(b(a(y''''''')))) -> F(c(d(d(x''''''))), a(y'''''''))
F(d(d(x'''''''')), a(b(a(y''''''')))) -> F(c(d(d(d(x'''''''')))), a(y'''''''))
F(d(c(d(x''''''))), a(b(a(y'''''''')))) -> F(c(d(d(c(d(x''''''))))), a(y''''''''))
F(d(d(x'''''''')), a(b(a(y'''''''')))) -> F(c(d(d(d(x'''''''')))), a(y''''''''))
F(x'', a(b(a(b(b(y'''''''''')))))) -> F(c(d(x'')), a(b(b(y''''''''''))))
F(x'', a(b(a(b(a(y'''''''''')))))) -> F(c(d(x'')), a(b(a(y''''''''''))))
F(d(x''''''''''), a(b(a(y'''''''')))) -> F(c(d(d(x''''''''''))), a(y''''''''))
F(x'', a(b(a(a(y''''''''''''''))))) -> F(c(d(x'')), a(a(y'''''''''''''')))
F(x'', a(b(a(a(b(b(y''''''''''''))))))) -> F(c(d(x'')), a(a(b(b(y'''''''''''')))))
F(x'', a(b(a(b(y''''''''''''''))))) -> F(c(d(x'')), a(b(y'''''''''''''')))
F(x'', a(b(a(a(b(a(y''''''''''''))))))) -> F(c(d(x'')), a(a(b(a(y'''''''''''')))))
F(d(c(d(c(d(x''''''''))))), a(b(a(y'''''''')))) -> F(c(d(d(c(d(c(d(x''''''''))))))), a(y''''''''))
F(d(c(d(x'''''''))), a(b(a(y'''''''')))) -> F(c(d(d(c(d(x'''''''))))), a(y''''''''))
F(d(c(d(d(x'''''''''')))), a(b(a(y'''''''')))) -> F(c(d(d(c(d(d(x'''''''''')))))), a(y''''''''))
F(d(d(c(d(x'''''''''')))), a(b(a(y'''''''')))) -> F(c(d(d(d(c(d(x'''''''''')))))), a(y''''''''))
F(d(d(d(x''''''''''''))), a(b(a(y'''''''')))) -> F(c(d(d(d(d(x''''''''''''))))), a(y''''''''))
F(d(d(x'''''''''')), a(b(a(y'''''''')))) -> F(c(d(d(d(x'''''''''')))), a(y''''''''))
F(d(d(x''''''''')), a(b(a(y'''''''')))) -> F(c(d(d(d(x''''''''')))), a(y''''''''))
F(d(x''''''), a(b(a(b(b(y'''''''''''''''')))))) -> F(c(d(d(x''''''))), a(b(b(y''''''''''''''''))))
F(d(x''''''), a(b(a(b(a(y'''''''''''''''')))))) -> F(c(d(d(x''''''))), a(b(a(y''''''''''''''''))))
F(d(x''''''), a(b(a(a(y''''''''''''''''''''))))) -> F(c(d(d(x''''''))), a(a(y'''''''''''''''''''')))
F(d(x''''''), a(b(a(a(b(b(y''''''''''''''''''))))))) -> F(c(d(d(x''''''))), a(a(b(b(y'''''''''''''''''')))))
F(d(x''''''), a(b(a(y'''''''')))) -> F(c(d(d(x''''''))), a(y''''''''))
F(d(x''''''), a(b(a(b(y''''''''''''''''''''))))) -> F(c(d(d(x''''''))), a(b(y'''''''''''''''''''')))
F(d(x''''''), a(b(a(a(b(a(y''''''''''''''''''))))))) -> F(c(d(d(x''''''))), a(a(b(a(y'''''''''''''''''')))))

The transformation is resulting in one new DP problem: 



   R
     ↳DPs
       →DP Problem 1
         ↳MRR
           →DP Problem 2
             ↳NOC
             ...
               →DP Problem 18
                 ↳Remaining Obligation(s)




The following remains to be proven:
Dependency Pairs:

F(d(x'''), a(a(b(b(y''''''''))))) -> F(x''', b(a(a(b(b(y''''''''))))))
F(d(x'''), b(a(a(b(a(y'''''''''')))))) -> F(x''', b(b(a(a(b(a(y'''''''''')))))))
F(d(x'''), b(a(a(b(b(y'''''''''')))))) -> F(x''', b(b(a(a(b(b(y'''''''''')))))))
F(d(x'''''), a(b(b(y'''''''')))) -> F(c(d(d(x'''''))), b(y''''''''))
F(c(d(x'''')), b(a(a(b(b(y'''''''''''''''')))))) -> F(d(x''''), a(b(a(a(b(b(y'''''''''''''''')))))))
F(c(x''), b(a(a(b(b(y'''''''''')))))) -> F(x'', a(b(a(a(b(b(y'''''''''')))))))
F(c(d(x'''')), b(a(b(y'''''''''''''''''')))) -> F(d(x''''), a(b(a(b(y'''''''''''''''''')))))
F(c(d(x'''')), b(a(b(a(y''''''''''''''))))) -> F(d(x''''), a(b(a(b(a(y''''''''''''''))))))
F(c(d(x'''')), b(a(b(b(y''''''''''''''))))) -> F(d(x''''), a(b(a(b(b(y''''''''''''''))))))
F(c(d(x'''')), b(a(a(b(a(y'''''''''''''''')))))) -> F(d(x''''), a(b(a(a(b(a(y'''''''''''''''')))))))
F(c(d(x'''')), b(a(y'''''))) -> F(d(x''''), a(b(a(y'''''))))
F(c(d(x'''')), b(a(a(y'''''''''''''''''')))) -> F(d(x''''), a(b(a(a(y'''''''''''''''''')))))
F(c(d(d(x'''''''))), b(a(y'''''))) -> F(d(d(x''''''')), a(b(a(y'''''))))
F(c(d(d(x''''''''))), b(a(y'''''))) -> F(d(d(x'''''''')), a(b(a(y'''''))))
F(c(d(d(d(x'''''''''')))), b(a(y'''''))) -> F(d(d(d(x''''''''''))), a(b(a(y'''''))))
F(c(d(d(c(d(x''''''''))))), b(a(y'''''))) -> F(d(d(c(d(x'''''''')))), a(b(a(y'''''))))
F(c(d(c(d(d(x''''''''))))), b(a(y'''''))) -> F(d(c(d(d(x'''''''')))), a(b(a(y'''''))))
F(c(d(c(d(x''''')))), b(a(y'''''))) -> F(d(c(d(x'''''))), a(b(a(y'''''))))
F(d(x''''''), a(b(a(b(y''''''''''''''''''''))))) -> F(c(d(d(x''''''))), a(b(y'''''''''''''''''''')))
F(d(x''''''), a(b(a(a(b(b(y''''''''''''''''''))))))) -> F(c(d(d(x''''''))), a(a(b(b(y'''''''''''''''''')))))
F(d(x''''''), a(b(a(b(a(y'''''''''''''''')))))) -> F(c(d(d(x''''''))), a(b(a(y''''''''''''''''))))
F(d(x''''''), a(b(a(b(b(y'''''''''''''''')))))) -> F(c(d(d(x''''''))), a(b(b(y''''''''''''''''))))
F(c(d(c(d(c(d(x'''''')))))), b(a(y'''''))) -> F(d(c(d(c(d(x''''''))))), a(b(a(y'''''))))
F(d(x''''''), a(b(a(a(b(a(y''''''''''''''''''))))))) -> F(c(d(d(x''''''))), a(a(b(a(y'''''''''''''''''')))))
F(d(x''''''), a(b(a(y'''''''')))) -> F(c(d(d(x''''''))), a(y''''''''))
F(d(x''''''), a(b(a(a(y''''''''''''''''''''))))) -> F(c(d(d(x''''''))), a(a(y'''''''''''''''''''')))
F(d(d(x''''''''')), a(b(a(y'''''''')))) -> F(c(d(d(d(x''''''''')))), a(y''''''''))
F(d(d(x'''''''''')), a(b(a(y'''''''')))) -> F(c(d(d(d(x'''''''''')))), a(y''''''''))
F(d(d(d(x''''''''''''))), a(b(a(y'''''''')))) -> F(c(d(d(d(d(x''''''''''''))))), a(y''''''''))
F(d(d(c(d(x'''''''''')))), a(b(a(y'''''''')))) -> F(c(d(d(d(c(d(x'''''''''')))))), a(y''''''''))
F(d(c(d(d(x'''''''''')))), a(b(a(y'''''''')))) -> F(c(d(d(c(d(d(x'''''''''')))))), a(y''''''''))
F(d(c(d(x'''''''))), a(b(a(y'''''''')))) -> F(c(d(d(c(d(x'''''''))))), a(y''''''''))
F(d(c(d(c(d(x''''''''))))), a(b(a(y'''''''')))) -> F(c(d(d(c(d(c(d(x''''''''))))))), a(y''''''''))
F(d(x''''''''''), a(b(a(y'''''''')))) -> F(c(d(d(x''''''''''))), a(y''''''''))
F(x'', a(b(a(a(b(a(y''''''''''''))))))) -> F(c(d(x'')), a(a(b(a(y'''''''''''')))))
F(x'', a(b(a(b(y''''''''''''''))))) -> F(c(d(x'')), a(b(y'''''''''''''')))
F(x'', a(b(a(a(b(b(y''''''''''''))))))) -> F(c(d(x'')), a(a(b(b(y'''''''''''')))))
F(x'', a(b(a(a(y''''''''''''''))))) -> F(c(d(x'')), a(a(y'''''''''''''')))
F(x'', a(b(a(b(a(y'''''''''')))))) -> F(c(d(x'')), a(b(a(y''''''''''))))
F(x'', a(b(a(b(b(y'''''''''')))))) -> F(c(d(x'')), a(b(b(y''''''''''))))
F(d(d(x'''''''')), a(b(a(y'''''''')))) -> F(c(d(d(d(x'''''''')))), a(y''''''''))
F(c(x''), b(a(a(b(a(y'''''''''')))))) -> F(x'', a(b(a(a(b(a(y'''''''''')))))))
F(x'', a(b(b(a(a(b(a(y'''''''''''''')))))))) -> F(c(d(x'')), b(a(a(b(a(y''''''''''''''))))))
F(d(c(d(x''''''))), a(b(a(y'''''''')))) -> F(c(d(d(c(d(x''''''))))), a(y''''''''))
F(c(x''), b(a(b(y'''''''''''')))) -> F(x'', a(b(a(b(y'''''''''''')))))
F(x'', a(b(b(a(b(y'''''''''''''''')))))) -> F(c(d(x'')), b(a(b(y''''''''''''''''))))
F(c(d(d(x''''''))), a(b(a(y''''''')))) -> F(c(d(c(d(d(x''''''))))), a(y'''''''))
F(c(x''), b(a(b(b(y''''''''))))) -> F(x'', a(b(a(b(b(y''''''''))))))
F(x'', a(b(b(a(y'''''''''))))) -> F(c(d(x'')), b(a(y''''''''')))
F(c(d(c(d(x'''')))), a(b(a(y''''''')))) -> F(c(d(c(d(c(d(x'''')))))), a(y'''''''))
F(c(x''), b(a(a(y'''''''''''')))) -> F(x'', a(b(a(a(y'''''''''''')))))
F(x'', a(b(b(a(a(b(b(y'''''''''''''')))))))) -> F(c(d(x'')), b(a(a(b(b(y''''''''''''''))))))
F(d(d(x'''''''')), a(b(a(y''''''')))) -> F(c(d(d(d(x'''''''')))), a(y'''''''))
F(c(d(x'''''''')), b(a(y''''''))) -> F(d(x''''''''), a(b(a(y''''''))))
F(x'', a(b(b(a(a(y'''''''''''''''')))))) -> F(c(d(x'')), b(a(a(y''''''''''''''''))))
F(c(d(x''')), a(b(a(y'''''''')))) -> F(c(d(c(d(x''')))), a(y''''''''))
F(c(x''), b(a(b(a(y''''''''))))) -> F(x'', a(b(a(b(a(y''''''''))))))
F(x'', a(b(b(a(b(a(y''''''''''''))))))) -> F(c(d(x'')), b(a(b(a(y'''''''''''')))))
F(d(c(d(x''''''))), a(b(a(y''''''')))) -> F(c(d(d(c(d(x''''''))))), a(y'''''''))
F(c(d(c(d(x'''')))), b(a(y'''''))) -> F(d(c(d(x''''))), a(b(a(y'''''))))
F(x'', a(b(b(a(b(b(y''''''''''''))))))) -> F(c(d(x'')), b(a(b(b(y'''''''''''')))))
F(x'', a(b(b(b(y''''''''))))) -> F(c(d(x'')), b(b(y'''''''')))
F(c(d(x'''')), a(b(a(y'''''')))) -> F(d(x''''), a(a(b(a(y'''''')))))
F(d(x''''''), a(b(a(y''''''')))) -> F(c(d(d(x''''''))), a(y'''''''))
F(c(d(d(x''''''))), b(a(y'''''))) -> F(d(d(x'''''')), a(b(a(y'''''))))
F(d(d(x'''''''')), a(b(b(y'''''''')))) -> F(c(d(d(d(x'''''''')))), b(y''''''''))
F(c(x''), b(b(a(a(b(a(y''''''''''''))))))) -> F(x'', a(b(b(a(a(b(a(y''''''''''''))))))))
F(d(c(d(x''''''))), a(b(b(y'''''''')))) -> F(c(d(d(c(d(x''''''))))), b(y''''''''))
F(c(x''), b(b(a(b(y''''''''''''''))))) -> F(x'', a(b(b(a(b(y''''''''''''''))))))
F(d(x''''''), a(b(b(y''''''')))) -> F(c(d(d(x''''''))), b(y'''''''))
F(c(x''), b(b(a(y''''''')))) -> F(x'', a(b(b(a(y''''''')))))
F(d(d(x'''''''')), a(b(b(y''''''')))) -> F(c(d(d(d(x'''''''')))), b(y'''''''))
F(c(x''), b(b(a(a(b(b(y''''''''''''))))))) -> F(x'', a(b(b(a(a(b(b(y''''''''''''))))))))
F(c(d(d(x''''''))), a(b(b(y''''''')))) -> F(c(d(c(d(d(x''''''))))), b(y'''''''))
F(c(x''), b(b(a(b(a(y'''''''''')))))) -> F(x'', a(b(b(a(b(a(y'''''''''')))))))
F(c(d(x''')), a(b(b(y'''''''')))) -> F(c(d(c(d(x''')))), b(y''''''''))
F(c(x''), b(b(a(b(b(y'''''''''')))))) -> F(x'', a(b(b(a(b(b(y'''''''''')))))))
F(c(d(c(d(x'''')))), a(b(b(y''''''')))) -> F(c(d(c(d(c(d(x'''')))))), b(y'''''''))
F(c(x''), b(b(a(a(y''''''''''''''))))) -> F(x'', a(b(b(a(a(y''''''''''''''))))))
F(d(x'''), b(a(a(y'''''''''''')))) -> F(x''', b(b(a(a(y'''''''''''')))))
F(d(x'''), a(a(y''''''''''))) -> F(x''', b(a(a(y''''''''''))))
F(c(d(x'''')), a(b(b(y'''''')))) -> F(d(x''''), a(a(b(b(y'''''')))))
F(c(x''), b(b(b(y'''''')))) -> F(x'', a(b(b(b(y'''''')))))
F(d(c(d(x''''''))), a(b(b(y''''''')))) -> F(c(d(d(c(d(x''''''))))), b(y'''''''))
F(c(d(x''')), b(b(y'''''))) -> F(d(x'''), a(b(b(y'''''))))
F(d(x'''), b(a(b(y'''''''''''')))) -> F(x''', b(b(a(b(y'''''''''''')))))
F(d(x'''), a(b(y''''''''''))) -> F(x''', b(a(b(y''''''''''))))
F(c(d(d(x''''''))), b(b(y'''''))) -> F(d(d(x'''''')), a(b(b(y'''''))))
F(d(x'''), b(a(y'''''))) -> F(x''', b(b(a(y'''''))))
F(d(x'''), a(b(b(y'''''')))) -> F(x''', b(a(b(b(y'''''')))))
F(c(d(c(d(x'''')))), b(b(y'''''))) -> F(d(c(d(x''''))), a(b(b(y'''''))))
F(d(x''''), b(b(y''''))) -> F(x'''', b(b(b(y''''))))
F(d(x'''), b(a(b(b(y''''''''))))) -> F(x''', b(b(a(b(b(y''''''''))))))
F(d(d(x'''''''')), a(y''')) -> F(d(x''''''''), b(a(y''')))
F(c(d(x'''')), b(b(y''''))) -> F(d(x''''), a(b(b(y''''))))
F(d(x'''), b(a(b(a(y''''''''))))) -> F(x''', b(b(a(b(a(y''''''''))))))
F(d(x'''), a(b(a(y'''''')))) -> F(x''', b(a(b(a(y'''''')))))
F(c(d(x'''')), b(y'''''''')) -> F(d(x''''), a(b(y'''''''')))
F(d(x''''), a(b(b(y'''''')))) -> F(x'''', b(a(b(b(y'''''')))))
F(c(d(d(x''''''))), y'''') -> F(d(d(x'''''')), a(y''''))
F(d(x''''), a(b(a(y'''''')))) -> F(x'''', b(a(b(a(y'''''')))))
F(c(d(x'''')), b(a(y''''))) -> F(d(x''''), a(b(a(y''''))))
F(d(c(d(x''''''))), a(y''')) -> F(c(d(x'''''')), b(a(y''')))
F(c(d(x'''')), a(y'''''''')) -> F(d(x''''), a(a(y'''''''')))
F(c(d(x'')), a(b(y''))) -> F(c(d(c(d(x'')))), y'')
F(d(x''''), a(b(y'))) -> F(c(d(d(x''''))), y')
F(c(d(c(d(x'''')))), y'''') -> F(d(c(d(x''''))), a(y''''))
F(d(x'''), a(a(b(a(y''''''''))))) -> F(x''', b(a(a(b(a(y''''''''))))))


Rule:

none


Strategy:

innermost




   R
     ↳DPs
       →DP Problem 1
         ↳MRR
           →DP Problem 2
             ↳NOC
             ...
               →DP Problem 8
                 ↳Modular Removal of Rules


Dependency Pair:

F11(c1(x''), a1(y'')) -> F11(x'', a1(a1(y'')))


Rule:

none


Strategy:

innermost




We have the following set of usable rules: none
To remove rules and DPs from this DP problem we used the following monotonic and CE-compatible order: Polynomial ordering.
Polynomial interpretation:
  POL(a_1(x1))=  x1  
  POL(c_1(x1))=  x1  
  POL(F_11(x1, x2))=  1 + x1 + x2  

We have the following set D of usable symbols: {a1, F11}
The following Dependency Pairs can be deleted as they contain symbols in their lhs which do not occur in D:

F11(c1(x''), a1(y'')) -> F11(x'', a1(a1(y'')))

No Rules can be deleted.

After the removal, there are no SCCs in the dependency graph which results in no DP problems which have to be solved.


The Proof could not be continued due to a Timeout.
Termination of R could not be shown.
Duration:
1:02 minutes