YES(?,O(n^1))

Problem:
 p(f(f(x))) -> q(f(g(x)))
 p(g(g(x))) -> q(g(f(x)))
 q(f(f(x))) -> p(f(g(x)))
 q(g(g(x))) -> p(g(f(x)))

Proof:
 RT Transformation Processor:
  strict:
   p(f(f(x))) -> q(f(g(x)))
   p(g(g(x))) -> q(g(f(x)))
   q(f(f(x))) -> p(f(g(x)))
   q(g(g(x))) -> p(g(f(x)))
  weak:
   
  Bounds Processor:
   bound: 1
   enrichment: match-rt
   automaton:
    final states: {5}
    transitions:
     q1(12) -> 13*
     f1(11) -> 12*
     g1(10) -> 11*
     p0(5) -> 5*
     f0(5) -> 5*
     q0(5) -> 5*
     g0(5) -> 5*
     5 -> 10*
     13 -> 5*
   problem:
    strict:
     p(g(g(x))) -> q(g(f(x)))
     q(f(f(x))) -> p(f(g(x)))
     q(g(g(x))) -> p(g(f(x)))
    weak:
     p(f(f(x))) -> q(f(g(x)))
   Bounds Processor:
    bound: 1
    enrichment: match-rt
    automaton:
     final states: {5}
     transitions:
      q1(12) -> 13*
      f1(10) -> 11*
      g1(11) -> 12*
      p0(5) -> 5*
      f0(5) -> 5*
      q0(5) -> 5*
      g0(5) -> 5*
      5 -> 10*
      13 -> 5*
    problem:
     strict:
      q(f(f(x))) -> p(f(g(x)))
      q(g(g(x))) -> p(g(f(x)))
     weak:
      p(g(g(x))) -> q(g(f(x)))
      p(f(f(x))) -> q(f(g(x)))
    Bounds Processor:
     bound: 1
     enrichment: match-rt
     automaton:
      final states: {5}
      transitions:
       f1(11) -> 12*
       g1(10) -> 11*
       p1(12) -> 13*
       p0(5) -> 5*
       f0(5) -> 5*
       q0(5) -> 5*
       g0(5) -> 5*
       5 -> 10*
       13 -> 5*
     problem:
      strict:
       q(g(g(x))) -> p(g(f(x)))
      weak:
       q(f(f(x))) -> p(f(g(x)))
       p(g(g(x))) -> q(g(f(x)))
       p(f(f(x))) -> q(f(g(x)))
     Bounds Processor:
      bound: 1
      enrichment: match-rt
      automaton:
       final states: {5}
       transitions:
        f1(10) -> 11*
        g1(11) -> 12*
        p1(12) -> 13*
        p0(5) -> 5*
        f0(5) -> 5*
        q0(5) -> 5*
        g0(5) -> 5*
        5 -> 10*
        13 -> 5*
      problem:
       strict:
        
       weak:
        q(g(g(x))) -> p(g(f(x)))
        q(f(f(x))) -> p(f(g(x)))
        p(g(g(x))) -> q(g(f(x)))
        p(f(f(x))) -> q(f(g(x)))
      Qed