YES
Time: 0.000673
TRS:
 { 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)),
           f(x, y, z) -> g(<=(x, y), x, y, z),
                p 0() -> 0(),
                p s x -> x}
 DP:
  DP:
   {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) -> f#(p x, y, z),
    g#(false(), x, y, z) -> f#(p y, z, x),
    g#(false(), x, y, z) -> f#(p z, x, y),
    g#(false(), x, y, z) -> p# x,
    g#(false(), x, y, z) -> p# y,
    g#(false(), x, y, z) -> p# z,
             f#(x, y, z) -> g#(<=(x, y), x, y, z)}
  TRS:
  { 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)),
            f(x, y, z) -> g(<=(x, y), x, y, z),
                 p 0() -> 0(),
                 p s x -> x}
  EDG:
   {(g#(false(), x, y, z) -> f#(p x, y, z), f#(x, y, z) -> g#(<=(x, y), x, y, z))
    (g#(false(), x, y, z) -> f#(f(p x, y, z), f(p y, z, x), f(p z, x, y)), f#(x, y, z) -> g#(<=(x, y), x, y, z))
    (g#(false(), x, y, z) -> f#(p y, z, x), f#(x, y, z) -> g#(<=(x, y), x, y, z))
    (g#(false(), x, y, z) -> f#(p z, x, y), f#(x, y, z) -> g#(<=(x, y), x, y, z))}
   SCCS (0):
    
    Qed