Input TRS:
    1: p(f(f(x))) -> q(f(g(x)))
    2: p(g(g(x))) -> q(g(f(x)))
    3: q(f(f(x))) -> p(f(g(x)))
    4: q(g(g(x))) -> p(g(f(x)))
Number of strict rules: 4
Direct Order(PosReal,>,Poly) ... failed.
Freezing p❆1_g q❆1_f p❆1_f q❆1_g q p
1: p❆1_f❆1_f(x) -> q❆1_f❆1_g(x)
2: p❆1_g❆1_g(x) -> q❆1_g❆1_f(x)
3: q❆1_f❆1_f(x) -> p❆1_f❆1_g(x)
4: q❆1_g❆1_g(x) -> p❆1_g❆1_f(x)
5: p(g(_1)) ->= p❆1_g(_1)
6: p(f(_1)) ->= p❆1_f(_1)
7: q(g(_1)) ->= q❆1_g(_1)
8: q(f(_1)) ->= q❆1_f(_1)
9: q❆1_g(g(_1)) ->= q❆1_g❆1_g(_1)
10: q❆1_g(f(_1)) ->= q❆1_g❆1_f(_1)
11: p❆1_f(g(_1)) ->= p❆1_f❆1_g(_1)
12: p❆1_f(f(_1)) ->= p❆1_f❆1_f(_1)
13: q❆1_f(g(_1)) ->= q❆1_f❆1_g(_1)
14: q❆1_f(f(_1)) ->= q❆1_f❆1_f(_1)
15: p❆1_g(g(_1)) ->= p❆1_g❆1_g(_1)
16: p❆1_g(f(_1)) ->= p❆1_g❆1_f(_1)
Number of strict rules: 4
Direct Order(PosReal,>,Poly) ... removes: 4 15 8 1 3 16 5 10 7 14 12 11 9 13 6 2
     q(x1)	weight: (/ 7 4) + 2 * x1
q❆1_g(x1)	weight: (/ 1 4) + x1
q❆1_g❆1_g(x1)	weight: (/ 1 4) + x1
p❆1_f❆1_g(x1)	weight: x1
q❆1_f(x1)	weight: 2 * x1
p❆1_f❆1_f(x1)	weight: (/ 1 4) + x1
     f(x1)	weight: (/ 1 4) + x1
q❆1_g❆1_f(x1)	weight: x1
p❆1_g❆1_g(x1)	weight: (/ 1 4) + x1
     p(x1)	weight: 2 * x1
q❆1_f❆1_g(x1)	weight: x1
p❆1_g❆1_f(x1)	weight: x1
p❆1_f(x1)	weight: 2 * x1
q❆1_f❆1_f(x1)	weight: (/ 1 4) + x1
     g(x1)	weight: (/ 1 4) + x1
p❆1_g(x1)	weight: 2 * x1
Number of strict rules: 0
YES