YES

Problem:
 f(x,x) -> f(a(),b())
 b() -> c()

Proof:
 DP Processor:
  DPs:
   f#(x,x) -> b#()
   f#(x,x) -> f#(a(),b())
  TRS:
   f(x,x) -> f(a(),b())
   b() -> c()
  EDG Processor:
   DPs:
    f#(x,x) -> b#()
    f#(x,x) -> f#(a(),b())
   TRS:
    f(x,x) -> f(a(),b())
    b() -> c()
   graph:
    f#(x,x) -> f#(a(),b()) -> f#(x,x) -> b#()
    f#(x,x) -> f#(a(),b()) -> f#(x,x) -> f#(a(),b())
   SCC Processor:
    #sccs: 1
    #rules: 1
    #arcs: 2/4
    DPs:
     f#(x,x) -> f#(a(),b())
    TRS:
     f(x,x) -> f(a(),b())
     b() -> c()
    Bounds Processor:
     bound: 2
     enrichment: match
     automaton:
      final states: {7}
      transitions:
       c2() -> 6,11*
       f{#,0}(10,11) -> 7*
       f{#,0}(11,6) -> 7*
       f{#,0}(6,6) -> 7*
       f{#,0}(11,10) -> 7*
       f{#,0}(6,10) -> 7*
       f{#,0}(10,6) -> 7*
       f{#,0}(10,10) -> 7*
       f{#,0}(11,11) -> 7*
       f{#,0}(6,11) -> 7*
       f0(10,11) -> 6*
       f0(11,6) -> 6*
       f0(6,6) -> 6*
       f0(11,10) -> 6*
       f0(6,10) -> 6*
       f0(10,6) -> 6*
       f0(10,10) -> 6*
       f0(11,11) -> 6*
       f0(6,11) -> 6*
       f1(9,8) -> 6*
       f1(10,11) -> 6*
       f1(9,11) -> 6*
       f1(10,8) -> 6*
       a1() -> 10*,6,9
       b1() -> 11*,6,8
       f{#,1}(9,8) -> 7*
       f{#,1}(10,11) -> 7*
       f{#,1}(9,11) -> 7*
       f{#,1}(10,8) -> 7*
     problem:
      DPs:
       
      TRS:
       f(x,x) -> f(a(),b())
       b() -> c()
     Qed