YES
Time: 0.050674
TRS:
 {q f f x -> p f g x,
  q g g x -> p g f x,
  p f f x -> q f g x,
  p g g x -> q g f x}
 DP:
  DP:
   {q# f f x -> p# f g x,
    q# g g x -> p# g f x,
    p# f f x -> q# f g x,
    p# g g x -> q# g f x}
  TRS:
  {q f f x -> p f g x,
   q g g x -> p g f x,
   p f f x -> q f g x,
   p g g x -> q g f x}
  UR:
   {}
   EDG:
    {(q# g g x -> p# g f x, p# g g x -> q# g f x)
     (q# g g x -> p# g f x, p# f f x -> q# f g x)
     (p# g g x -> q# g f x, q# g g x -> p# g f x)
     (p# g g x -> q# g f x, q# f f x -> p# f g x)
     (p# f f x -> q# f g x, q# f f x -> p# f g x)
     (p# f f x -> q# f g x, q# g g x -> p# g f x)
     (q# f f x -> p# f g x, p# f f x -> q# f g x)
     (q# f f x -> p# f g x, p# g g x -> q# g f x)}
    STATUS:
     arrows: 0.500000
     SCCS (1):
      Scc:
       {q# f f x -> p# f g x,
        q# g g x -> p# g f x,
        p# f f x -> q# f g x,
        p# g g x -> q# g f x}
      
      SCC (4):
       Strict:
        {q# f f x -> p# f g x,
         q# g g x -> p# g f x,
         p# f f x -> q# f g x,
         p# g g x -> q# g f x}
       Weak:
       {q f f x -> p f g x,
        q g g x -> p g f x,
        p f f x -> q f g x,
        p g g x -> q g f x}
       POLY:
        Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
        Interpretation:
         [q](x0) = x0,
         
         [f](x0) = x0 + 1,
         
         [g](x0) = 0,
         
         [p](x0) = 0,
         
         [q#](x0) = x0,
         
         [p#](x0) = x0
        Strict:
         p# g g x -> q# g f x
         0 + 0x >= 0 + 0x
         p# f f x -> q# f g x
         2 + 1x >= 1 + 0x
         q# g g x -> p# g f x
         0 + 0x >= 0 + 0x
         q# f f x -> p# f g x
         2 + 1x >= 1 + 0x
        Weak:
         p g g x -> q g f x
         0 + 0x >= 0 + 0x
         p f f x -> q f g x
         0 + 0x >= 1 + 0x
         q g g x -> p g f x
         0 + 0x >= 0 + 0x
         q f f x -> p f g x
         2 + 1x >= 0 + 0x
       SCCS (1):
        Scc:
         {q# g g x -> p# g f x,
          p# g g x -> q# g f x}
        
        SCC (2):
         Strict:
          {q# g g x -> p# g f x,
           p# g g x -> q# g f x}
         Weak:
         {q f f x -> p f g x,
          q g g x -> p g f x,
          p f f x -> q f g x,
          p g g x -> q g f x}
         POLY:
          Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
          Interpretation:
           [q](x0) = 0,
           
           [f](x0) = 0,
           
           [g](x0) = x0 + 1,
           
           [p](x0) = 0,
           
           [q#](x0) = x0,
           
           [p#](x0) = x0
          Strict:
           p# g g x -> q# g f x
           2 + 1x >= 1 + 0x
           q# g g x -> p# g f x
           2 + 1x >= 1 + 0x
          Weak:
           p g g x -> q g f x
           0 + 0x >= 0 + 0x
           p f f x -> q f g x
           0 + 0x >= 0 + 0x
           q g g x -> p g f x
           0 + 0x >= 0 + 0x
           q f f x -> p f g x
           0 + 0x >= 0 + 0x
         Qed