YES
LCTRS
  Theories
    Core
  Sorts
    Unit
  Signature
    f: (Unit, Unit) -> Unit
  Rules
    f(?10, ?11) -> f(?11, ?10)
    f(f(?12, ?13), ?14) -> f(?12, f(?13, ?14))
Confluent by Strongly Closedness with proof:
    * Critical Pair
      Inner Rule
        f(f(?12', ?13'), ?14') -> f(?12', f(?13', ?14'))
      Outer Rule
        f(?10", ?11") -> f(?11", ?10")
      Pair
        f(?12', f(?13', ?11")) ≈ f(?11", f(?12', ?13'))
    which reaches the trivial constrained equation
      f(?12', f(?13', ?11")) ≈ f(?11", f(?12', ?13')) 
        -> f(f(?13', ?11"), ?12') ≈ f(?11", f(?12', ?13')) 
        -> f(f(?11", ?13'), ?12') ≈ f(?11", f(?12', ?13')) 
        -> f(?11", f(?13', ?12')) ≈ f(?11", f(?12', ?13')) 
        -> f(?11", f(?13', ?12')) ≈ f(?11", f(?13', ?12')) 
    and the trivial constrained equation
      f(?12', f(?13', ?11")) ≈ f(?11", f(?12', ?13')) 
        -> f(?12', f(?13', ?11")) ≈ f(f(?12', ?13'), ?11") 
        -> f(?12', f(?13', ?11")) ≈ f(?12', f(?13', ?11")) 
    * Critical Pair
      Inner Rule
        f(?10', ?11') -> f(?11', ?10')
      Outer Rule
        f(f(?12", ?13"), ?14") -> f(?12", f(?13", ?14"))
      Pair
        f(?14", f(?12", ?13")) ≈ f(?12", f(?13", ?14"))
    which reaches the trivial constrained equation
      f(?14", f(?12", ?13")) ≈ f(?12", f(?13", ?14")) 
        -> f(f(?12", ?13"), ?14") ≈ f(?12", f(?13", ?14")) 
        -> f(?12", f(?13", ?14")) ≈ f(?12", f(?13", ?14")) 
    and the trivial constrained equation
      f(?14", f(?12", ?13")) ≈ f(?12", f(?13", ?14")) 
        -> f(?14", f(?12", ?13")) ≈ f(f(?13", ?14"), ?12") 
        -> f(?14", f(?12", ?13")) ≈ f(f(?14", ?13"), ?12") 
        -> f(?14", f(?12", ?13")) ≈ f(?14", f(?13", ?12")) 
        -> f(?14", f(?13", ?12")) ≈ f(?14", f(?13", ?12")) 
    * Critical Pair
      Inner Rule
        f(?10', ?11') -> f(?11', ?10')
      Outer Rule
        f(f(?12", ?13"), ?14") -> f(?12", f(?13", ?14"))
      Pair
        f(f(?13", ?12"), ?14") ≈ f(?12", f(?13", ?14"))
    which reaches the trivial constrained equation
      f(f(?13", ?12"), ?14") ≈ f(?12", f(?13", ?14")) 
        -> f(f(?12", ?13"), ?14") ≈ f(?12", f(?13", ?14")) 
        -> f(?12", f(?13", ?14")) ≈ f(?12", f(?13", ?14")) 
    and the trivial constrained equation
      f(f(?13", ?12"), ?14") ≈ f(?12", f(?13", ?14")) 
        -> f(f(?13", ?12"), ?14") ≈ f(f(?13", ?14"), ?12") 
        -> f(f(?13", ?12"), ?14") ≈ f(f(?14", ?13"), ?12") 
        -> f(f(?13", ?12"), ?14") ≈ f(?14", f(?13", ?12")) 
        -> f(?14", f(?13", ?12")) ≈ f(?14", f(?13", ?12")) 
    * Critical Pair
      Inner Rule
        f(f(?12', ?13'), ?14') -> f(?12', f(?13', ?14'))
      Outer Rule
        f(f(?12", ?13"), ?14") -> f(?12", f(?13", ?14"))
      Pair
        f(f(?12', f(?13', ?13")), ?14") ≈ f(f(?12', ?13'), f(?13", ?14"))
    which reaches the trivial constrained equation
      f(f(?12', f(?13', ?13")), ?14") ≈ f(f(?12', ?13'), f(?13", ?14")) 
        -> f(?12', f(f(?13', ?13"), ?14")) ≈ f(f(?12', ?13'), f(?13", ?14")) 
        -> f(?12', f(?13', f(?13", ?14"))) ≈ f(f(?12', ?13'), f(?13", ?14")) 
        -> f(?12', f(?13', f(?13", ?14"))) ≈ f(?12', f(?13', f(?13", ?14"))) 
    and the trivial constrained equation
      f(f(?12', f(?13', ?13")), ?14") ≈ f(f(?12', ?13'), f(?13", ?14")) 
        -> f(f(?12', f(?13', ?13")), ?14") ≈ f(f(?13", ?14"), f(?12', ?13')) 
        -> f(f(?12', f(?13', ?13")), ?14") ≈ f(f(?14", ?13"), f(?12', ?13')) 
        -> f(f(?12', f(?13', ?13")), ?14") ≈ f(?14", f(?13", f(?12', ?13'))) 
        -> f(f(?12', f(?13', ?13")), ?14") ≈ f(?14", f(f(?12', ?13'), ?13")) 
        -> f(f(?12', f(?13', ?13")), ?14") ≈ f(?14", f(?12', f(?13', ?13"))) 
        -> f(?14", f(?12', f(?13', ?13"))) ≈ f(?14", f(?12', f(?13', ?13"))) 

Elapsed Time: 3892.14 ms