NO
LCTRS
  Theories
    Core, Ints
  Sorts
    List
  Signature
    app: (List, List) -> List
    cons: (Int, List) -> List
    flatten: List -> List
    insert: (Int, List) -> List
    leaf: Int -> List
    nil: List
    node: (List, List) -> List
    rev: List -> List
    sorting: List -> List
    tsorting: List -> List
  Rules
    app(cons(?36, ?37), ?38) -> cons(?36, app(?37, ?38))
    app(nil, ?39) -> ?39
    flatten(leaf(?40)) -> cons(?40, nil)
    flatten(node(?41, ?42)) -> app(flatten(?41), flatten(?42))
    insert(?43, nil) -> cons(?43, nil)
    insert(?44, cons(?45, ?46)) -> cons(?45, insert(?44, ?46)) [>=(?44, ?45)]
    insert(?47, cons(?48, nil)) -> cons(?47, cons(?48, nil)) [<(?47, ?48)]
    node(?49, ?50) -> node(?50, ?49)
    sorting(cons(?51, ?52)) -> insert(?51, sorting(?52))
    sorting(nil) -> nil
    tsorting(?53) -> sorting(flatten(?53))
Not confluent by "two different NFs found" with proof:
  * Critical Pair
    Inner Rule
      node(?49', ?50') -> node(?50', ?49')
    Outer Rule
      flatten(node(?41", ?42")) -> app(flatten(?41"), flatten(?42"))
    Pair
      flatten(node(?42", ?41")) ≈ app(flatten(?41"), flatten(?42"))
  reaches the non-trivial normal form
    flatten(node(?42", ?41")) ≈ app(flatten(?41"), flatten(?42")) 
      ->^* app(flatten(?42"), flatten(?41")) ≈ app(flatten(?41"), flatten(?42")) 

Elapsed Time: 123.00 ms