YES
LCTRS
  Theories
    Core, Ints
  Signature
    quad: Int -> Int
    twice: Int -> Int
    u: (Int, Int, Int) -> Int
  Rules
    quad(?16) -> +(twice(?16), twice(?16))
    twice(?17) -> u(?17, 0, 0)
    u(?18, ?19, ?20) -> ?20 [not(<(?19, ?18))]
    u(?21, ?22, ?23) -> u(?21, +(?22, 1), +(?23, 2)) [<(?22, ?21)]
Confluent by Weak Orthogonality with proof:
  no critical pairs

Elapsed Time:  52.00 ms