YES

The TRS could be proven terminating. The proof took 29 ms.

The following DP Processors were used

Problem 1 was processed with processor DependencyGraph (19ms).

Problem 1: DependencyGraph

Dependency Pair Problem

Dependency Pairs

g^#(false, x, y, z)	→	p^#(y)		g^#(false, x, y, z)	→	p^#(x)
g^#(false, x, y, z)	→	f^#(p(z), x, y)		g^#(false, x, y, z)	→	f^#(p(y), z, x)
g^#(false, x, y, z)	→	f^#(f(p(x), y, z), f(p(y), z, x), f(p(z), x, y))		g^#(false, x, y, z)	→	p^#(z)
f^#(x, y, z)	→	g^#(<=(x, y), x, y, z)		g^#(false, x, y, z)	→	f^#(p(x), y, z)

Rewrite Rules

f(x, y, z)	→	g(<=(x, y), x, y, z)		g(true, x, y, z)	→	z
g(false, x, y, z)	→	f(f(p(x), y, z), f(p(y), z, x), f(p(z), x, y))		p(0)	→	0
p(s(x))	→	x

Original Signature

Termination of terms over the following signature is verified: f, g, 0, s, <=, p, true, false

Strategy

There are no SCCs!