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

Elapsed Time: 4005.50 ms