YES
Time: 0.014861
TRS:
 {  average(x, s s s y) -> s average(s x, y),
        average(s x, y) -> average(x, s y),
  average(0(), s s 0()) -> s 0(),
    average(0(), s 0()) -> 0(),
      average(0(), 0()) -> 0()}
 DP:
  DP:
   {average#(x, s s s y) -> average#(s x, y),
        average#(s x, y) -> average#(x, s y)}
  TRS:
  {  average(x, s s s y) -> s average(s x, y),
         average(s x, y) -> average(x, s y),
   average(0(), s s 0()) -> s 0(),
     average(0(), s 0()) -> 0(),
       average(0(), 0()) -> 0()}
  UR:
   {}
   EDG:
    {(average#(x, s s s y) -> average#(s x, y), average#(s x, y) -> average#(x, s y))
     (average#(x, s s s y) -> average#(s x, y), average#(x, s s s y) -> average#(s x, y))
     (average#(s x, y) -> average#(x, s y), average#(x, s s s y) -> average#(s x, y))
     (average#(s x, y) -> average#(x, s y), average#(s x, y) -> average#(x, s y))}
    STATUS:
     arrows: 0.000000
     SCCS (1):
      Scc:
       {average#(x, s s s y) -> average#(s x, y),
            average#(s x, y) -> average#(x, s y)}
      
      SCC (2):
       Strict:
        {average#(x, s s s y) -> average#(s x, y),
             average#(s x, y) -> average#(x, s y)}
       Weak:
       {  average(x, s s s y) -> s average(s x, y),
              average(s x, y) -> average(x, s y),
        average(0(), s s 0()) -> s 0(),
          average(0(), s 0()) -> 0(),
            average(0(), 0()) -> 0()}
       POLY:
        Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
        Interpretation:
         [average](x0, x1) = x0 + 1,
         
         [s](x0) = x0 + 1,
         
         [0] = 1,
         
         [average#](x0, x1) = x0 + x1 + 1
        Strict:
         average#(s x, y) -> average#(x, s y)
         2 + 1x + 1y >= 2 + 1x + 1y
         average#(x, s s s y) -> average#(s x, y)
         4 + 1x + 1y >= 2 + 1x + 1y
        Weak:
         average(0(), 0()) -> 0()
         2 >= 1
         average(0(), s 0()) -> 0()
         2 >= 1
         average(0(), s s 0()) -> s 0()
         2 >= 2
         average(s x, y) -> average(x, s y)
         2 + 1x + 0y >= 1 + 1x + 0y
         average(x, s s s y) -> s average(s x, y)
         1 + 1x + 0y >= 3 + 1x + 0y
       SCCS (1):
        Scc:
         {average#(s x, y) -> average#(x, s y)}
        
        SCC (1):
         Strict:
          {average#(s x, y) -> average#(x, s y)}
         Weak:
         {  average(x, s s s y) -> s average(s x, y),
                average(s x, y) -> average(x, s y),
          average(0(), s s 0()) -> s 0(),
            average(0(), s 0()) -> 0(),
              average(0(), 0()) -> 0()}
         POLY:
          Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
          Interpretation:
           [average](x0, x1) = x0 + 1,
           
           [s](x0) = x0 + 1,
           
           [0] = 1,
           
           [average#](x0, x1) = x0
          Strict:
           average#(s x, y) -> average#(x, s y)
           1 + 1x + 0y >= 0 + 1x + 0y
          Weak:
           average(0(), 0()) -> 0()
           2 >= 1
           average(0(), s 0()) -> 0()
           2 >= 1
           average(0(), s s 0()) -> s 0()
           2 >= 2
           average(s x, y) -> average(x, s y)
           2 + 1x + 0y >= 1 + 1x + 0y
           average(x, s s s y) -> s average(s x, y)
           1 + 1x + 0y >= 3 + 1x + 0y
         Qed