YES

We show the termination of the TRS R:

  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

-- SCC decomposition.

Consider the dependency pair problem (P, R), where P consists of

p1: f#(x,y,z) -> g#(<=(x,y),x,y,z)
p2: g#(false(),x,y,z) -> f#(f(p(x),y,z),f(p(y),z,x),f(p(z),x,y))
p3: g#(false(),x,y,z) -> f#(p(x),y,z)
p4: g#(false(),x,y,z) -> p#(x)
p5: g#(false(),x,y,z) -> f#(p(y),z,x)
p6: g#(false(),x,y,z) -> p#(y)
p7: g#(false(),x,y,z) -> f#(p(z),x,y)
p8: g#(false(),x,y,z) -> p#(z)

and R consists of:

r1: f(x,y,z) -> g(<=(x,y),x,y,z)
r2: g(true(),x,y,z) -> z
r3: g(false(),x,y,z) -> f(f(p(x),y,z),f(p(y),z,x),f(p(z),x,y))
r4: p(|0|()) -> |0|()
r5: p(s(x)) -> x

The estimated dependency graph contains the following SCCs:

  (no SCCs)