MAYBE
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(nil, !xs) -> !xs
    app(cons(!x, !xs), !ys) -> cons(!x, app(!xs, !ys))
    insert(!x, nil) -> cons(!x, nil)
    insert(!x, cons(!y, nil)) -> cons(!x, cons(!y, nil)) [<(!x, !y)]
    insert(!x, cons(!y, !ys)) -> cons(!y, insert(!x, !ys)) [>=(!x, !y)]
    sorting(nil) -> nil
    sorting(cons(!x, !xs)) -> insert(!x, sorting(!xs))
    flatten(leaf(!x)) -> cons(!x, nil)
    flatten(node(!x, !y)) -> app(flatten(!x), flatten(!y))
    node(!x, !y) -> node(!y, !x)
    tsorting(!x) -> sorting(flatten(!x))
No termination info given.

Elapsed Time: 108.95 ms