MAYBE
LCTRS
  Theories
    Core, Ints
  Sorts
    List, Tree
  Signature
    @: (List, List) -> List
    L: Int -> Tree
    N: (Tree, Tree) -> Tree
    Nil: List
    add: (Int, List) -> List
    cons: (Int, List) -> List
    flatten: Tree -> List
    singleton: Int -> List
    sorting: List -> List
    toTree: List -> Tree
    tsorting: Tree -> Tree
  Rules
    @(Nil, !xs) -> !xs
    add(!x, Nil) -> singleton(!x)
    add(!x, cons(!y, !ys)) -> cons(!y, add(!x, !ys)) [>=(!x, !y)]
    sorting(cons(!x, !xs)) -> add(!x, sorting(!xs))
    flatten(N(!x, !y)) -> @(flatten(!x), flatten(!y))
    tsorting(!t) -> toTree(sorting(flatten(!t)))
    @(cons(!x, !xs), !ys) -> cons(!x, @(!xs, !ys))
    add(!x, cons(!y, !ys)) -> cons(!x, cons(!y, !ys)) [<(!x, !y)]
    sorting(Nil) -> Nil
    flatten(L(!x)) -> singleton(!x)
    N(!x, !y) -> N(!y, !x)
No termination info given.

Elapsed Time:  89.93 ms