YES

Problem:
 f(f(0(),x),1()) -> f(g(f(x,x)),x)
 f(g(x),y) -> g(f(x,y))

Proof:
 DP Processor:
  DPs:
   f#(f(0(),x),1()) -> f#(x,x)
   f#(f(0(),x),1()) -> f#(g(f(x,x)),x)
   f#(g(x),y) -> f#(x,y)
  TRS:
   f(f(0(),x),1()) -> f(g(f(x,x)),x)
   f(g(x),y) -> g(f(x,y))
  EDG Processor:
   DPs:
    f#(f(0(),x),1()) -> f#(x,x)
    f#(f(0(),x),1()) -> f#(g(f(x,x)),x)
    f#(g(x),y) -> f#(x,y)
   TRS:
    f(f(0(),x),1()) -> f(g(f(x,x)),x)
    f(g(x),y) -> g(f(x,y))
   graph:
    f#(g(x),y) -> f#(x,y) -> f#(f(0(),x),1()) -> f#(x,x)
    f#(g(x),y) -> f#(x,y) -> f#(f(0(),x),1()) -> f#(g(f(x,x)),x)
    f#(g(x),y) -> f#(x,y) -> f#(g(x),y) -> f#(x,y)
    f#(f(0(),x),1()) -> f#(g(f(x,x)),x) -> f#(g(x),y) -> f#(x,y)
    f#(f(0(),x),1()) -> f#(x,x) -> f#(g(x),y) -> f#(x,y)
   Bounds Processor:
    bound: 1
    enrichment: top-dp
    automaton:
     final states: {13}
     transitions:
      f{#,1}(13,13) -> 13*
      f{#,1}(9,12) -> 13*
      f{#,1}(11,12) -> 13*
      f{#,1}(13,12) -> 13*
      f{#,1}(9,9) -> 13*
      f{#,1}(10,10) -> 13*
      f{#,1}(10,12) -> 13*
      f{#,1}(11,11) -> 13*
      f{#,1}(12,12) -> 13*
      f{#,0}(13,9) -> 13*
      f{#,0}(13,11) -> 13*
      f{#,0}(13,13) -> 13*
      f{#,0}(9,10) -> 13*
      f{#,0}(9,12) -> 13*
      f{#,0}(10,9) -> 13*
      f{#,0}(10,11) -> 13*
      f{#,0}(10,13) -> 13*
      f{#,0}(11,10) -> 13*
      f{#,0}(11,12) -> 13*
      f{#,0}(12,9) -> 13*
      f{#,0}(12,11) -> 13*
      f{#,0}(12,13) -> 13*
      f{#,0}(13,10) -> 13*
      f{#,0}(13,12) -> 13*
      f{#,0}(9,9) -> 13*
      f{#,0}(9,11) -> 13*
      f{#,0}(9,13) -> 13*
      f{#,0}(10,10) -> 13*
      f{#,0}(10,12) -> 13*
      f{#,0}(11,9) -> 13*
      f{#,0}(11,11) -> 13*
      f{#,0}(11,13) -> 13*
      f{#,0}(12,10) -> 13*
      f{#,0}(12,12) -> 13*
      f0(13,9) -> 9*
      f0(13,11) -> 9*
      f0(13,13) -> 9*
      f0(9,10) -> 9*
      f0(9,12) -> 9*
      f0(10,9) -> 9*
      f0(10,11) -> 9*
      f0(10,13) -> 9*
      f0(11,10) -> 9*
      f0(11,12) -> 9*
      f0(12,9) -> 9*
      f0(12,11) -> 9*
      f0(12,13) -> 9*
      f0(13,10) -> 9*
      f0(13,12) -> 9*
      f0(9,9) -> 9*
      f0(9,11) -> 9*
      f0(9,13) -> 9*
      f0(10,10) -> 9*
      f0(10,12) -> 9*
      f0(11,9) -> 9*
      f0(11,11) -> 9*
      f0(11,13) -> 9*
      f0(12,10) -> 9*
      f0(12,12) -> 9*
      00() -> 10*
      10() -> 11*
      g0(10) -> 12*
      g0(12) -> 12*
      g0(9) -> 9,12
      g0(11) -> 12*
      g0(13) -> 12*
    problem:
     DPs:
      f#(f(0(),x),1()) -> f#(g(f(x,x)),x)
      f#(g(x),y) -> f#(x,y)
     TRS:
      f(f(0(),x),1()) -> f(g(f(x,x)),x)
      f(g(x),y) -> g(f(x,y))
    Bounds Processor:
     bound: 1
     enrichment: top-dp
     automaton:
      final states: {17}
      transitions:
       f{#,1}(38,15) -> 17,10
       f{#,1}(44,12) -> 17,10
       f{#,1}(34,16) -> 17,10
       f{#,1}(35,13) -> 17,10
       f{#,1}(40,17) -> 17,10
       f{#,1}(41,10) -> 17,10
       f{#,1}(46,14) -> 17,10
       f{#,1}(31,14) -> 17,10
       f{#,1}(37,15) -> 17,10
       f{#,1}(43,12) -> 17,10
       f{#,1}(33,16) -> 17,10
       f{#,1}(39,17) -> 17,10
       f{#,1}(45,16) -> 17,10
       f{#,1}(36,13) -> 17,10
       f{#,1}(42,10) -> 17,10
       f{#,1}(32,14) -> 17,10
       g1(45) -> 45,33
       g1(35) -> 36*
       g1(37) -> 37,38
       g1(39) -> 40*
       g1(46) -> 31*
       g1(41) -> 42*
       g1(31) -> 31,32
       g1(43) -> 44*
       g1(33) -> 34*
       f1(17,14) -> 46*
       f1(12,14) -> 46*
       f1(13,13) -> 35*
       f1(14,14) -> 31*
       f1(15,15) -> 37*
       f1(16,14) -> 31*
       f1(16,16) -> 33*
       f1(17,17) -> 39*
       f1(13,14) -> 31*
       f1(10,10) -> 41*
       f1(15,14) -> 31*
       f1(10,14) -> 46*
       f1(15,16) -> 45*
       f1(12,12) -> 43*
       f{#,0}(12,14) -> 10*
       f{#,0}(17,16) -> 10*
       f{#,0}(12,16) -> 10*
       f{#,0}(13,13) -> 10*
       f{#,0}(13,15) -> 10*
       f{#,0}(13,17) -> 10*
       f{#,0}(14,10) -> 10*
       f{#,0}(14,12) -> 10*
       f{#,0}(14,14) -> 10*
       f{#,0}(14,16) -> 10*
       f{#,0}(15,13) -> 17,10
       f{#,0}(10,13) -> 10*
       f{#,0}(15,15) -> 17,10
       f{#,0}(10,15) -> 10*
       f{#,0}(15,17) -> 17,10
       f{#,0}(10,17) -> 10*
       f{#,0}(16,10) -> 10,17
       f{#,0}(16,12) -> 10,17
       f{#,0}(16,14) -> 10,17
       f{#,0}(16,16) -> 10,17
       f{#,0}(17,13) -> 10*
       f{#,0}(12,13) -> 10*
       f{#,0}(17,15) -> 10*
       f{#,0}(12,15) -> 10*
       f{#,0}(17,17) -> 10*
       f{#,0}(12,17) -> 10*
       f{#,0}(13,10) -> 10*
       f{#,0}(13,12) -> 10*
       f{#,0}(13,14) -> 10*
       f{#,0}(13,16) -> 10*
       f{#,0}(14,13) -> 10*
       f{#,0}(14,15) -> 10*
       f{#,0}(14,17) -> 10*
       f{#,0}(15,10) -> 17,10
       f{#,0}(10,10) -> 10*
       f{#,0}(15,12) -> 17,10
       f{#,0}(10,12) -> 10*
       f{#,0}(15,14) -> 17,10
       f{#,0}(10,14) -> 10*
       f{#,0}(15,16) -> 17,10
       f{#,0}(10,16) -> 10*
       f{#,0}(16,13) -> 10,17
       f{#,0}(16,15) -> 10,17
       f{#,0}(16,17) -> 10,17
       f{#,0}(17,10) -> 10*
       f{#,0}(12,10) -> 10*
       f{#,0}(17,12) -> 10*
       f{#,0}(12,12) -> 10*
       f{#,0}(17,14) -> 10*
       f0(12,14) -> 15*
       f0(17,16) -> 15*
       f0(12,16) -> 15*
       f0(13,13) -> 15*
       f0(13,15) -> 15*
       f0(13,17) -> 15*
       f0(14,10) -> 15*
       f0(14,12) -> 15*
       f0(14,14) -> 15*
       f0(14,16) -> 15*
       f0(15,13) -> 15*
       f0(10,13) -> 15*
       f0(15,15) -> 15*
       f0(10,15) -> 15*
       f0(15,17) -> 15*
       f0(10,17) -> 15*
       f0(16,10) -> 15*
       f0(16,12) -> 15*
       f0(16,14) -> 15*
       f0(16,16) -> 15*
       f0(17,13) -> 15*
       f0(12,13) -> 15*
       f0(17,15) -> 15*
       f0(12,15) -> 15*
       f0(17,17) -> 15*
       f0(12,17) -> 15*
       f0(13,10) -> 15*
       f0(13,12) -> 15*
       f0(13,14) -> 15*
       f0(13,16) -> 15*
       f0(14,13) -> 15*
       f0(14,15) -> 15*
       f0(14,17) -> 15*
       f0(15,10) -> 15*
       f0(10,10) -> 15*
       f0(15,12) -> 15*
       f0(10,12) -> 15*
       f0(15,14) -> 15*
       f0(10,14) -> 15*
       f0(15,16) -> 15*
       f0(10,16) -> 15*
       f0(16,13) -> 15*
       f0(16,15) -> 15*
       f0(16,17) -> 15*
       f0(17,10) -> 15*
       f0(12,10) -> 15*
       f0(17,12) -> 15*
       f0(12,12) -> 15*
       f0(17,14) -> 15*
       00() -> 12*
       10() -> 13*
       g0(15) -> 15,16
       g0(10) -> 14*
       g0(17) -> 14*
       g0(12) -> 14*
       g0(14) -> 14*
       g0(16) -> 14*
       g0(13) -> 14*
     problem:
      DPs:
       f#(g(x),y) -> f#(x,y)
      TRS:
       f(f(0(),x),1()) -> f(g(f(x,x)),x)
       f(g(x),y) -> g(f(x,y))
     Subterm Criterion Processor:
      simple projection:
       pi(f#) = 0
      problem:
       DPs:
        
       TRS:
        f(f(0(),x),1()) -> f(g(f(x,x)),x)
        f(g(x),y) -> g(f(x,y))
      Qed