YES

Problem:
 f(f(y,z),f(x,f(a(),x))) -> f(f(f(a(),z),f(x,a())),f(a(),y))

Proof:
 DP Processor:
  DPs:
   f#(f(y,z),f(x,f(a(),x))) -> f#(a(),y)
   f#(f(y,z),f(x,f(a(),x))) -> f#(x,a())
   f#(f(y,z),f(x,f(a(),x))) -> f#(a(),z)
   f#(f(y,z),f(x,f(a(),x))) -> f#(f(a(),z),f(x,a()))
   f#(f(y,z),f(x,f(a(),x))) -> f#(f(f(a(),z),f(x,a())),f(a(),y))
  TRS:
   f(f(y,z),f(x,f(a(),x))) -> f(f(f(a(),z),f(x,a())),f(a(),y))
  EDG Processor:
   DPs:
    f#(f(y,z),f(x,f(a(),x))) -> f#(a(),y)
    f#(f(y,z),f(x,f(a(),x))) -> f#(x,a())
    f#(f(y,z),f(x,f(a(),x))) -> f#(a(),z)
    f#(f(y,z),f(x,f(a(),x))) -> f#(f(a(),z),f(x,a()))
    f#(f(y,z),f(x,f(a(),x))) -> f#(f(f(a(),z),f(x,a())),f(a(),y))
   TRS:
    f(f(y,z),f(x,f(a(),x))) -> f(f(f(a(),z),f(x,a())),f(a(),y))
   graph:
    f#(f(y,z),f(x,f(a(),x))) -> f#(f(f(a(),z),f(x,a())),f(a(),y)) ->
    f#(f(y,z),f(x,f(a(),x))) -> f#(a(),y)
    f#(f(y,z),f(x,f(a(),x))) -> f#(f(f(a(),z),f(x,a())),f(a(),y)) ->
    f#(f(y,z),f(x,f(a(),x))) -> f#(x,a())
    f#(f(y,z),f(x,f(a(),x))) -> f#(f(f(a(),z),f(x,a())),f(a(),y)) ->
    f#(f(y,z),f(x,f(a(),x))) -> f#(a(),z)
    f#(f(y,z),f(x,f(a(),x))) -> f#(f(f(a(),z),f(x,a())),f(a(),y)) ->
    f#(f(y,z),f(x,f(a(),x))) -> f#(f(a(),z),f(x,a()))
    f#(f(y,z),f(x,f(a(),x))) -> f#(f(f(a(),z),f(x,a())),f(a(),y)) ->
    f#(f(y,z),f(x,f(a(),x))) -> f#(f(f(a(),z),f(x,a())),f(a(),y))
   SCC Processor:
    #sccs: 1
    #rules: 1
    #arcs: 5/25
    DPs:
     f#(f(y,z),f(x,f(a(),x))) -> f#(f(f(a(),z),f(x,a())),f(a(),y))
    TRS:
     f(f(y,z),f(x,f(a(),x))) -> f(f(f(a(),z),f(x,a())),f(a(),y))
    Bounds Processor:
     bound: 2
     enrichment: match-dp
     automaton:
      final states: {4}
      transitions:
       f{#,0}(22,20) -> 4*
       f{#,0}(8,5) -> 4*
       f{#,0}(42,38) -> 4*
       f{#,0}(42,40) -> 4*
       f{#,0}(22,38) -> 4*
       f{#,0}(8,17) -> 4*
       f{#,0}(22,40) -> 4*
       f{#,0}(8,21) -> 4*
       f{#,0}(64,20) -> 4*
       f{#,0}(42,60) -> 4*
       f{#,0}(42,62) -> 4*
       f{#,0}(8,37) -> 4*
       f{#,0}(22,60) -> 4*
       f{#,0}(8,39) -> 4*
       f{#,0}(22,62) -> 4*
       f{#,0}(8,41) -> 4*
       f{#,0}(64,38) -> 4*
       f{#,0}(64,40) -> 4*
       f{#,0}(8,61) -> 4*
       f{#,0}(8,63) -> 4*
       f{#,0}(64,60) -> 4*
       f{#,0}(64,62) -> 4*
       f{#,0}(42,5) -> 4*
       f{#,0}(22,5) -> 4*
       f{#,0}(42,17) -> 4*
       f{#,0}(42,21) -> 4*
       f{#,0}(22,17) -> 4*
       f{#,0}(22,21) -> 4*
       f{#,0}(42,37) -> 4*
       f{#,0}(42,39) -> 4*
       f{#,0}(64,5) -> 4*
       f{#,0}(42,41) -> 4*
       f{#,0}(22,37) -> 4*
       f{#,0}(22,39) -> 4*
       f{#,0}(22,41) -> 4*
       f{#,0}(8,20) -> 4*
       f{#,0}(64,17) -> 4*
       f{#,0}(64,21) -> 4*
       f{#,0}(42,61) -> 4*
       f{#,0}(42,63) -> 4*
       f{#,0}(8,38) -> 4*
       f{#,0}(22,61) -> 4*
       f{#,0}(8,40) -> 4*
       f{#,0}(22,63) -> 4*
       f{#,0}(64,37) -> 4*
       f{#,0}(64,39) -> 4*
       f{#,0}(64,41) -> 4*
       f{#,0}(8,60) -> 4*
       f{#,0}(8,62) -> 4*
       f{#,0}(64,61) -> 4*
       f{#,0}(64,63) -> 4*
       f{#,0}(42,20) -> 4*
       f0(16,35) -> 6,19*
       f0(60,64) -> 16*
       f0(40,60) -> 16*
       f0(43,1) -> 6,19*
       f0(37,20) -> 16*
       f0(21,37) -> 16*
       f0(41,41) -> 16*
       f0(35,60) -> 20*
       f0(38,1) -> 6,19*
       f0(42,22) -> 16*
       f0(22,18) -> 6,19*
       f0(16,37) -> 16*
       f0(40,62) -> 22*,8
       f0(37,22) -> 16*
       f0(1,35) -> 20*
       f0(41,43) -> 16*
       f0(21,39) -> 16*
       f0(35,62) -> 20*
       f0(2,16) -> 16*
       f0(22,20) -> 16*
       f0(16,39) -> 16*
       f0(40,64) -> 16*
       f0(20,60) -> 16*
       f0(21,41) -> 16*
       f0(1,37) -> 20*
       f0(35,64) -> 20*
       f0(18,1) -> 19*,6
       f0(2,18) -> 16*
       f0(22,22) -> 16*
       f0(16,41) -> 16*
       f0(20,62) -> 22*,8
       f0(21,43) -> 16*
       f0(1,39) -> 20*
       f0(18,3) -> 17*
       f0(2,20) -> 16*
       f0(16,43) -> 16*
       f0(20,64) -> 16*
       f0(3,1) -> 6*
       f0(1,41) -> 20*
       f0(2,22) -> 16*
       f0(1,43) -> 20*
       f0(62,38) -> 22*,8
       f0(63,19) -> 22*,8
       f0(61,59) -> 6,19*
       f0(62,40) -> 16*
       f0(63,21) -> 22*,8
       f0(61,61) -> 16*
       f0(64,2) -> 16*
       f0(42,38) -> 16*
       f0(62,42) -> 16*
       f0(59,2) -> 16*
       f0(43,19) -> 16*
       f0(37,38) -> 22*,8
       f0(41,59) -> 6,19*
       f0(61,63) -> 16*
       f0(38,19) -> 22*,8
       f0(42,40) -> 16*
       f0(43,21) -> 16*
       f0(37,40) -> 16*
       f0(41,61) -> 16*
       f0(38,21) -> 22*,8
       f0(42,42) -> 16*
       f0(22,38) -> 16*
       f0(39,2) -> 16*
       f0(37,42) -> 16*
       f0(17,38) -> 8*
       f0(21,59) -> 6,19*
       f0(41,63) -> 16*
       f0(18,19) -> 20*
       f0(22,40) -> 16*
       f0(16,59) -> 6,19*
       f0(7,38) -> 8*
       f0(21,61) -> 16*
       f0(18,21) -> 20*
       f0(22,42) -> 16*
       f0(2,38) -> 16*
       f0(16,61) -> 16*
       f0(19,2) -> 16*
       f0(39,6) -> 8*
       f0(1,59) -> 20*
       f0(21,63) -> 16*
       f0(2,40) -> 16*
       f0(16,63) -> 16*
       f0(1,61) -> 20*
       f0(2,42) -> 16*
       f0(63,35) -> 6,19*
       f0(1,63) -> 20*
       f0(64,16) -> 16*
       f0(59,16) -> 20*
       f0(63,37) -> 16*
       f0(64,18) -> 6,19*
       f0(59,18) -> 6,21*
       f0(43,35) -> 6,19*
       f0(63,39) -> 16*
       f0(64,20) -> 16*
       f0(38,35) -> 6,19*
       f0(62,60) -> 16*
       f0(59,20) -> 20*
       f0(39,16) -> 16*
       f0(43,37) -> 16*
       f0(63,41) -> 16*
       f0(60,1) -> 6,19*
       f0(64,22) -> 16*
       f0(38,37) -> 16*
       f0(62,62) -> 22*,8
       f0(59,22) -> 20*
       f0(39,18) -> 6,19*
       f0(43,39) -> 16*
       f0(63,43) -> 16*
       f0(18,35) -> 21*,6
       f0(38,39) -> 16*
       f0(62,64) -> 16*
       f0(42,60) -> 16*
       f0(19,16) -> 16*
       f0(39,20) -> 16*
       f0(43,41) -> 16*
       f0(37,60) -> 16*
       f0(40,1) -> 6,19*
       f0(38,41) -> 16*
       f0(18,37) -> 20*
       f0(42,62) -> 16*
       f0(35,1) -> 19*,6
       f0(19,18) -> 6,19*
       f0(39,22) -> 16*
       f0(43,43) -> 16*
       f0(3,35) -> 6*
       f0(37,62) -> 22*,8
       f0(38,43) -> 16*
       f0(18,39) -> 20*
       f0(42,64) -> 16*
       f0(22,60) -> 16*
       f0(35,3) -> 17*
       f0(19,20) -> 16*
       f0(37,64) -> 16*
       f0(20,1) -> 6,19*
       f0(18,41) -> 20*
       f0(22,62) -> 16*
       f0(19,22) -> 16*
       f0(17,62) -> 8*
       f0(18,43) -> 20*
       f0(22,64) -> 16*
       f0(2,60) -> 16*
       f0(7,62) -> 8*
       f0(2,62) -> 16*
       f0(2,64) -> 16*
       f0(64,38) -> 16*
       f0(59,38) -> 20*
       f0(63,59) -> 6,19*
       f0(60,19) -> 22*,8
       f0(64,40) -> 16*
       f0(59,40) -> 20*
       f0(63,61) -> 16*
       f0(60,21) -> 22*,8
       f0(64,42) -> 16*
       f0(61,2) -> 16*
       f0(39,38) -> 22*,8
       f0(59,42) -> 20*
       f0(43,59) -> 19*,6
       f0(63,63) -> 16*
       f0(40,19) -> 22*,8
       f0(38,59) -> 19*,6
       f0(35,19) -> 20*
       f0(39,40) -> 16*
       f0(43,61) -> 16*
       f0(40,21) -> 22*,8
       f0(38,61) -> 16*
       f0(41,2) -> 16*
       f0(61,6) -> 8*
       f0(35,21) -> 20*
       f0(39,42) -> 16*
       f0(19,38) -> 16*
       f0(43,63) -> 16*
       f0(20,19) -> 22*,8
       f0(18,59) -> 21*,6
       f0(38,63) -> 16*
       f0(19,40) -> 16*
       f0(20,21) -> 22*,8
       f0(18,61) -> 20*
       f0(21,2) -> 16*
       f0(41,6) -> 8*
       f0(19,42) -> 16*
       f0(3,59) -> 6*
       f0(16,2) -> 16*
       f0(18,63) -> 20*
       f0(1,2) -> 16*,3,2
       f0(21,6) -> 8*
       f0(60,35) -> 6,19*
       f0(61,16) -> 16*
       f0(60,37) -> 16*
       f0(61,18) -> 6,19*
       f0(40,35) -> 6,19*
       f0(60,39) -> 16*
       f0(64,60) -> 16*
       f0(41,16) -> 16*
       f0(61,20) -> 16*
       f0(35,35) -> 21*,6
       f0(59,60) -> 20*
       f0(62,1) -> 6,19*
       f0(40,37) -> 16*
       f0(60,41) -> 16*
       f0(64,62) -> 16*
       f0(41,18) -> 6,19*
       f0(61,22) -> 16*
       f0(35,37) -> 20*
       f0(59,62) -> 20*
       f0(20,35) -> 6,19*
       f0(40,39) -> 16*
       f0(60,43) -> 16*
       f0(64,64) -> 16*
       f0(21,16) -> 16*
       f0(41,20) -> 16*
       f0(35,39) -> 20*
       f0(59,64) -> 20*
       f0(39,60) -> 16*
       f0(42,1) -> 6,19*
       f0(16,16) -> 16*
       f0(20,37) -> 16*
       f0(40,41) -> 16*
       f0(37,1) -> 6,19*
       f0(21,18) -> 6,19*
       f0(41,22) -> 16*
       f0(35,41) -> 20*
       f0(39,62) -> 22*,8
       f0(16,18) -> 19*,6
       f0(40,43) -> 16*
       f0(20,39) -> 16*
       f0(1,16) -> 20*
       f0(21,20) -> 16*
       f0(35,43) -> 20*
       f0(39,64) -> 16*
       f0(19,60) -> 16*
       f0(22,1) -> 6,19*
       f0(16,20) -> 16*
       f0(20,41) -> 16*
       f0(1,18) -> 20*
       f0(21,22) -> 16*
       f0(19,62) -> 16*
       f0(16,22) -> 16*
       f0(20,43) -> 16*
       f0(1,20) -> 20*
       f0(19,64) -> 16*
       f0(2,1) -> 16*,3,2
       f0(1,22) -> 20*
       f0(61,38) -> 22*,8
       f0(62,19) -> 22*,8
       f0(60,59) -> 6,19*
       f0(61,40) -> 16*
       f0(62,21) -> 22*,8
       f0(60,61) -> 16*
       f0(63,2) -> 16*
       f0(41,38) -> 22*,8
       f0(61,42) -> 16*
       f0(42,19) -> 16*
       f0(40,59) -> 6,19*
       f0(60,63) -> 16*
       f0(37,19) -> 22*,8
       f0(41,40) -> 16*
       f0(35,59) -> 21*,6
       f0(42,21) -> 16*
       f0(40,61) -> 16*
       f0(43,2) -> 16*
       f0(63,6) -> 8*
       f0(37,21) -> 22*,8
       f0(41,42) -> 16*
       f0(21,38) -> 22*,8
       f0(35,61) -> 20*
       f0(38,2) -> 16*
       f0(22,19) -> 16*
       f0(16,38) -> 16*
       f0(20,59) -> 6,19*
       f0(40,63) -> 16*
       f0(17,19) -> 8*
       f0(21,40) -> 16*
       f0(35,63) -> 20*
       f0(22,21) -> 16*
       f0(16,40) -> 16*
       f0(20,61) -> 16*
       f0(7,19) -> 8*
       f0(17,21) -> 8*
       f0(21,42) -> 16*
       f0(1,38) -> 20*
       f0(18,2) -> 16*
       f0(38,6) -> 8*
       f0(2,19) -> 16*
       f0(16,42) -> 16*
       f0(20,63) -> 16*
       f0(7,21) -> 8*
       f0(1,40) -> 20*
       f0(2,21) -> 16*
       f0(1,42) -> 20*
       f0(62,35) -> 6,19*
       f0(63,16) -> 16*
       f0(62,37) -> 16*
       f0(63,18) -> 6,19*
       f0(42,35) -> 6,19*
       f0(62,39) -> 16*
       f0(43,16) -> 16*
       f0(63,20) -> 16*
       f0(37,35) -> 6,19*
       f0(61,60) -> 16*
       f0(64,1) -> 6,19*
       f0(38,16) -> 16*
       f0(42,37) -> 16*
       f0(62,41) -> 16*
       f0(59,1) -> 6,19*
       f0(43,18) -> 6,19*
       f0(63,22) -> 16*
       f0(37,37) -> 16*
       f0(61,62) -> 22*,8
       f0(38,18) -> 6,19*
       f0(42,39) -> 16*
       f0(22,35) -> 19*,6
       f0(62,43) -> 16*
       f0(59,3) -> 17*
       f0(43,20) -> 16*
       f0(37,39) -> 16*
       f0(61,64) -> 16*
       f0(41,60) -> 16*
       f0(18,16) -> 20*
       f0(38,20) -> 16*
       f0(42,41) -> 16*
       f0(22,37) -> 16*
       f0(39,1) -> 6,19*
       f0(43,22) -> 16*
       f0(37,41) -> 16*
       f0(41,62) -> 22*,8
       f0(18,18) -> 21*,6
       f0(38,22) -> 16*
       f0(42,43) -> 16*
       f0(2,35) -> 16*
       f0(22,39) -> 16*
       f0(37,43) -> 16*
       f0(41,64) -> 16*
       f0(21,60) -> 16*
       f0(18,20) -> 20*
       f0(2,37) -> 16*
       f0(22,41) -> 16*
       f0(16,60) -> 16*
       f0(19,1) -> 6,19*
       f0(3,18) -> 6*
       f0(21,62) -> 22*,8
       f0(18,22) -> 20*
       f0(22,43) -> 16*
       f0(2,39) -> 16*
       f0(16,62) -> 16*
       f0(21,64) -> 16*
       f0(1,60) -> 20*
       f0(2,41) -> 16*
       f0(16,64) -> 16*
       f0(1,62) -> 20*
       f0(2,43) -> 16*
       f0(1,64) -> 20*
       f0(63,38) -> 22*,8
       f0(64,19) -> 16*
       f0(62,59) -> 6,19*
       f0(59,19) -> 20*
       f0(63,40) -> 16*
       f0(64,21) -> 16*
       f0(62,61) -> 16*
       f0(59,21) -> 20*
       f0(43,38) -> 16*
       f0(63,42) -> 16*
       f0(60,2) -> 16*
       f0(38,38) -> 22*,8
       f0(42,59) -> 6,19*
       f0(62,63) -> 16*
       f0(39,19) -> 22*,8
       f0(43,40) -> 16*
       f0(37,59) -> 6,19*
       f0(38,40) -> 16*
       f0(42,61) -> 16*
       f0(39,21) -> 22*,8
       f0(43,42) -> 16*
       f0(37,61) -> 16*
       f0(40,2) -> 16*
       f0(60,6) -> 8*
       f0(38,42) -> 16*
       f0(18,38) -> 20*
       f0(22,59) -> 19*,6
       f0(42,63) -> 16*
       f0(35,2) -> 16*
       f0(19,19) -> 16*
       f0(37,63) -> 16*
       f0(18,40) -> 20*
       f0(22,61) -> 16*
       f0(19,21) -> 16*
       f0(20,2) -> 16*
       f0(40,6) -> 8*
       f0(18,42) -> 20*
       f0(2,59) -> 16*
       f0(22,63) -> 16*
       f0(2,61) -> 16*
       f0(20,6) -> 8*
       f0(64,35) -> 6,19*
       f0(2,63) -> 16*
       f0(59,35) -> 21*,6
       f0(60,16) -> 16*
       f0(64,37) -> 16*
       f0(59,37) -> 20*
       f0(60,18) -> 6,19*
       f0(64,39) -> 16*
       f0(59,39) -> 20*
       f0(39,35) -> 6,19*
       f0(63,60) -> 16*
       f0(40,16) -> 16*
       f0(60,20) -> 16*
       f0(64,41) -> 16*
       f0(61,1) -> 6,19*
       f0(35,16) -> 20*
       f0(59,41) -> 20*
       f0(39,37) -> 16*
       f0(63,62) -> 22*,8
       f0(40,18) -> 6,19*
       f0(60,22) -> 16*
       f0(64,43) -> 16*
       f0(35,18) -> 21*,6
       f0(59,43) -> 20*
       f0(19,35) -> 19*,6
       f0(39,39) -> 16*
       f0(63,64) -> 16*
       f0(43,60) -> 16*
       f0(20,16) -> 16*
       f0(40,20) -> 16*
       f0(38,60) -> 16*
       f0(41,1) -> 6,19*
       f0(35,20) -> 20*
       f0(19,37) -> 16*
       f0(39,41) -> 16*
       f0(43,62) -> 16*
       f0(20,18) -> 6,19*
       f0(40,22) -> 16*
       f0(38,62) -> 22*,8
       f0(35,22) -> 20*
       f0(39,43) -> 16*
       f0(19,39) -> 16*
       f0(43,64) -> 16*
       f0(20,20) -> 16*
       f0(38,64) -> 16*
       f0(18,60) -> 20*
       f0(21,1) -> 6,19*
       f0(19,41) -> 16*
       f0(16,1) -> 19*,6
       f0(20,22) -> 16*
       f0(18,62) -> 20*
       f0(19,43) -> 16*
       f0(18,64) -> 20*
       f0(1,1) -> 16*,3,2
       f0(1,3) -> 17*,7,5
       f0(60,38) -> 22*,8
       f0(64,59) -> 6,19*
       f0(61,19) -> 22*,8
       f0(59,59) -> 21*,6
       f0(60,40) -> 16*
       f0(64,61) -> 16*
       f0(61,21) -> 22*,8
       f0(59,61) -> 20*
       f0(62,2) -> 16*
       f0(40,38) -> 22*,8
       f0(60,42) -> 16*
       f0(64,63) -> 16*
       f0(41,19) -> 22*,8
       f0(35,38) -> 20*
       f0(59,63) -> 20*
       f0(39,59) -> 6,19*
       f0(40,40) -> 16*
       f0(41,21) -> 22*,8
       f0(35,40) -> 20*
       f0(39,61) -> 16*
       f0(42,2) -> 16*
       f0(62,6) -> 8*
       f0(40,42) -> 16*
       f0(20,38) -> 22*,8
       f0(37,2) -> 16*
       f0(21,19) -> 22*,8
       f0(35,42) -> 20*
       f0(19,59) -> 6,19*
       f0(39,63) -> 16*
       f0(16,19) -> 16*
       f0(20,40) -> 16*
       f0(21,21) -> 22*,8
       f0(19,61) -> 16*
       f0(22,2) -> 16*
       f0(16,21) -> 16*
       f0(20,42) -> 16*
       f0(37,6) -> 8*
       f0(1,19) -> 20*
       f0(19,63) -> 16*
       f0(1,21) -> 20*
       f0(2,2) -> 16*,3,2
       f0(17,6) -> 8*
       f0(61,35) -> 6,19*
       f0(62,16) -> 16*
       f0(7,6) -> 8*
       f0(61,37) -> 16*
       f0(62,18) -> 6,19*
       f0(41,35) -> 6,19*
       f0(61,39) -> 16*
       f0(42,16) -> 16*
       f0(62,20) -> 16*
       f0(60,60) -> 16*
       f0(63,1) -> 6,19*
       f0(37,16) -> 16*
       f0(41,37) -> 16*
       f0(61,41) -> 16*
       f0(42,18) -> 19*,6
       f0(62,22) -> 16*
       f0(60,62) -> 22*,8
       f0(37,18) -> 6,19*
       f0(21,35) -> 6,19*
       f0(41,39) -> 16*
       f0(61,43) -> 16*
       f0(42,20) -> 16*
       f0(22,16) -> 16*
       f{#,1}(42,24) -> 4*
       f{#,1}(27,24) -> 4*
       f{#,1}(42,36) -> 4*
       f{#,1}(27,36) -> 4*
       f{#,1}(42,40) -> 4*
       f{#,1}(27,40) -> 4*
       f{#,1}(64,24) -> 4*
       f{#,1}(42,60) -> 4*
       f{#,1}(43,41) -> 4*
       f{#,1}(27,60) -> 4*
       f{#,1}(64,36) -> 4*
       f{#,1}(64,40) -> 4*
       f{#,1}(43,61) -> 4*
       f{#,1}(43,63) -> 4*
       f{#,1}(64,60) -> 4*
       f{#,1}(42,41) -> 4*
       f{#,1}(43,24) -> 4*
       f{#,1}(27,41) -> 4*
       f{#,1}(43,36) -> 4*
       f{#,1}(43,40) -> 4*
       f{#,1}(42,61) -> 4*
       f{#,1}(42,63) -> 4*
       f{#,1}(27,61) -> 4*
       f{#,1}(27,63) -> 4*
       f{#,1}(64,41) -> 4*
       f{#,1}(43,60) -> 4*
       f{#,1}(64,61) -> 4*
       f{#,1}(64,63) -> 4*
       f1(26,37) -> 27*
       f1(35,60) -> 20,24,41*
       f1(40,62) -> 22,8,42*,27
       f1(1,35) -> 20,37*,25
       f1(35,62) -> 20,24,26,40*
       f1(23,7) -> 24*
       f1(23,17) -> 24*
       f1(63,25) -> 27*
       f1(59,6) -> 26*
       f1(23,19) -> 26*
       f1(23,21) -> 36*,26,24
       f1(1,59) -> 20,37*,25
       f1(18,23) -> 25*
       f1(63,37) -> 16,27,43*
       f1(59,20) -> 20,24,41*
       f1(18,35) -> 21,38*,6,25
       f1(23,37) -> 24*
       f1(23,39) -> 24*
       f1(23,41) -> 24*
       f1(35,7) -> 24*
       f1(59,38) -> 26,24,36*
       f1(59,40) -> 24*
       f1(35,17) -> 24*
       f1(39,38) -> 22,42*,8,27
       f1(35,19) -> 20,39*,26
       f1(60,25) -> 27*
       f1(24,38) -> 27*
       f1(35,21) -> 20,36,40*,24,26
       f1(18,59) -> 21,6,38*,25
       f1(35,23) -> 25*
       f1(23,61) -> 24*
       f1(40,25) -> 27*
       f1(23,63) -> 24*
       f1(60,37) -> 16,43*,27
       f1(35,35) -> 21,38*,6,25
       f1(59,60) -> 24*
       f1(40,37) -> 16,43*,27
       f1(35,37) -> 20,24,41*
       f1(59,62) -> 26,24,36*
       f1(35,39) -> 20,24,41*
       f1(35,41) -> 20,24,41*
       f1(39,62) -> 22,8,42*,27
       f1(24,62) -> 27*
       f1(61,38) -> 22,8,42*,27
       f1(41,38) -> 22,42*,8,27
       f1(36,38) -> 27*
       f1(35,59) -> 37*,25
       f1(26,38) -> 27*
       f1(35,61) -> 20,24,41*
       f1(35,63) -> 20,24,41*
       f1(23,6) -> 26*
       f1(61,62) -> 22,8,42*,27
       f1(41,62) -> 22,8,42*,27
       f1(36,62) -> 27*
       f1(59,7) -> 24*
       f1(23,20) -> 24*
       f1(26,62) -> 27*
       f1(59,17) -> 24*
       f1(63,38) -> 22,8,42*,27
       f1(59,19) -> 20,39*,26
       f1(59,21) -> 20,24,40*,26
       f1(59,23) -> 25*
       f1(23,38) -> 24,36*,26
       f1(23,40) -> 24*
       f1(39,25) -> 27*
       f1(35,6) -> 26*
       f1(24,25) -> 27*
       f1(59,35) -> 21,6,38*,25
       f1(59,37) -> 24*
       f1(59,39) -> 24*
       f1(59,41) -> 24*
       f1(39,37) -> 16,43*,27
       f1(63,62) -> 27*
       f1(24,37) -> 27*
       f1(35,20) -> 20,41*,24
       f1(23,60) -> 24*
       f1(23,62) -> 24,26,36*
       f1(60,38) -> 22,8,42*,27
       f1(59,59) -> 37*,25
       f1(59,61) -> 24*
       f1(40,38) -> 22,42*,8,27
       f1(35,38) -> 20,24,40*,26
       f1(59,63) -> 24*
       f1(61,25) -> 27*
       f1(35,40) -> 20,24,41*
       f1(41,25) -> 27*
       f1(36,25) -> 27*
       f1(26,25) -> 27*
       f1(1,23) -> 25*
       f1(61,37) -> 16,27,43*
       f1(41,37) -> 16,43*,27
       f1(36,37) -> 27*
       f1(60,62) -> 27*
       f{#,2}(48,45) -> 4*
       f{#,2}(48,61) -> 4*
       f{#,2}(64,45) -> 4*
       f{#,2}(64,61) -> 4*
       f2(47,46) -> 48*
       f2(59,24) -> 45*
       f2(47,62) -> 48*
       f2(59,26) -> 45*
       f2(44,24) -> 45*
       f2(44,26) -> 45*
       f2(59,36) -> 45*
       f2(59,38) -> 36,40,20,60*,26,24,47
       f2(44,36) -> 45*
       f2(59,40) -> 20,41,61*,24,45
       f2(44,38) -> 47*
       f2(44,40) -> 45*
       f2(59,44) -> 46*
       f2(59,60) -> 20,41,24,61*,45
       f2(59,62) -> 40,20,36,24,26,60*,47
       f2(44,60) -> 45*
       f2(44,62) -> 47*
       f2(35,59) -> 38,21,37,62*,25,6,46
       f2(59,25) -> 47*
       f2(63,46) -> 48*
       f2(44,25) -> 47*
       f2(59,37) -> 20,41,63*,24,47
       f2(59,39) -> 20,41,61*,24,45
       f2(44,37) -> 47*
       f2(59,41) -> 20,41,61*,24,45
       f2(63,62) -> 42,22,43,64*,27,8,48
       f2(44,39) -> 45*
       f2(44,41) -> 45*
       f2(59,59) -> 38,21,37,62*,25,6,46
       f2(59,61) -> 20,41,24,61*,45
       f2(59,63) -> 20,41,24,61*,45
       f2(44,61) -> 45*
       f2(60,46) -> 48*
       f2(44,63) -> 45*
       f2(35,44) -> 46*
       f2(60,62) -> 22,42,64*,27,8,48
       a2() -> 18,35,59*,23,3,1,44
       1 -> 3*
       2 -> 3*
     problem:
      DPs:
       
      TRS:
       f(f(y,z),f(x,f(a(),x))) -> f(f(f(a(),z),f(x,a())),f(a(),y))
     Qed