YES
(VAR x y)
(RULES 
f(g(x),g(y)) -> f(p(f(g(x),s(y))),g(s(p(x))))
p(0) -> g(0)
g(s(p(x))) -> p(x)
)

Proving termination of rewriting for tricky1:

-> Dependency pairs:
nF_f(g(x),g(y)) -> nF_f(p(f(g(x),s(y))),g(s(p(x))))
nF_f(g(x),g(y)) -> nF_p(f(g(x),s(y)))
nF_f(g(x),g(y)) -> nF_f(g(x),s(y))
nF_f(g(x),g(y)) -> nF_g(x)
nF_f(g(x),g(y)) -> nF_g(s(p(x)))
nF_f(g(x),g(y)) -> nF_p(x)
nF_p(0) -> nF_g(0)
nF_g(s(p(x))) -> nF_p(x)

-> Proof of termination for tricky1_1:
-> -> Dependency pairs in cycle:
nF_f(g(x),g(y)) -> nF_f(p(f(g(x),s(y))),g(s(p(x))))

UsableRules:
f(g(x),g(y)) -> f(p(f(g(x),s(y))),g(s(p(x))))
p(0) -> g(0)
g(s(p(x))) -> p(x)

Polynomial Interpretation:

[f](X1,X2) = 0
[g](X) = X + 1
[p](X) = 2.X
[s](X) = X
[0] = 1
[nF_f](X1,X2) = X1

TIME: 4.51e-4


SETTINGS:
Base ordering: Polynomial ordering
Proof mode: SCCs in DG + base ordering
Upper bound for coeffs: 2
Rationals below 1 for all non-replacing args: No
Polynomial interpretation: Linear
Coeffs in polynomials: No rationals
Delta: automatic



Termination was proved succesfully.