MAYBE
LCTRS
  Theories
    Core, Ints
  Sorts
    Sigma, trm
  Signature
    cod: trm -> Int
    def: trm -> Int
    dom: trm -> Int
    gen: (Sigma, Int, Int) -> trm
    id: Int -> trm
    layer: (Int, Int, Sigma, Int, Int) -> trm
    par: (trm, trm) -> trm
    seq: (trm, trm) -> trm
  Rules
    layer(!k, !l, !g, !ni, !no) -> par(id(!k), par(gen(!g, !ni, !no), id(!l)))
    dom(gen(!g, !ni, !no)) -> !ni
    dom(id(!n)) -> !n
    dom(seq(!u, !v)) -> dom(!u)
    dom(par(!u, !v)) -> +(dom(!u), dom(!v))
    dom(layer(!k, !l, !g, !ni, !no)) -> +(!k, +(!ni, !l))
    cod(gen(!g, !ni, !no)) -> !no
    cod(id(!n)) -> !n
    cod(seq(!u, !v)) -> cod(!v)
    cod(par(!u, !v)) -> +(cod(!u), cod(!v))
    cod(layer(!k, !l, !g, !ni, !no)) -> +(!k, +(!no, !l))
    def(!t) -> -(dom(!t), cod(!t))
    seq(seq(!t, !u), !v) -> seq(!t, seq(!u, !v))
    par(par(!t, !u), !v) -> par(!t, par(!u, !v))
    seq(id(!n), !t) -> !t
    seq(!t, id(!n)) -> !t
    par(id(!n), id(!m)) -> id(+(!n, !m))
    par(id(!n), par(id(!m), !t)) -> par(id(+(!n, !m)), !t)
    par(gen(!g, !ni, !no), gen(!h, !mi, !mo)) -> seq(par(gen(!g, !ni, !no), id(dom(gen(!h, !mi, !mo)))), par(id(cod(gen(!g, !ni, !no))), gen(!h, !mi, !mo)))
    par(gen(!g, !ni, !no), par(!u, !v)) -> seq(par(gen(!g, !ni, !no), id(dom(par(!u, !v)))), par(id(cod(gen(!g, !ni, !no))), par(!u, !v)))
    par(gen(!g, !ni, !no), seq(!u, !v)) -> seq(par(gen(!g, !ni, !no), id(dom(seq(!u, !v)))), par(id(cod(gen(!g, !ni, !no))), seq(!u, !v)))
    par(par(!s, !t), gen(!h, !mi, !mo)) -> seq(par(par(!s, !t), id(dom(gen(!h, !mi, !mo)))), par(id(cod(par(!s, !t))), gen(!h, !mi, !mo)))
    par(par(!s, !t), par(!u, !v)) -> seq(par(par(!s, !t), id(dom(par(!u, !v)))), par(id(cod(par(!s, !t))), par(!u, !v)))
    par(par(!s, !t), seq(!u, !v)) -> seq(par(par(!s, !t), id(dom(seq(!u, !v)))), par(id(cod(par(!s, !t))), seq(!u, !v)))
    par(seq(!s, !t), gen(!h, !mi, !mo)) -> seq(par(seq(!s, !t), id(dom(gen(!h, !mi, !mo)))), par(id(cod(seq(!s, !t))), gen(!h, !mi, !mo)))
    par(seq(!s, !t), par(!u, !v)) -> seq(par(seq(!s, !t), id(dom(par(!u, !v)))), par(id(cod(seq(!s, !t))), par(!u, !v)))
    par(seq(!s, !t), seq(!u, !v)) -> seq(par(seq(!s, !t), id(dom(seq(!u, !v)))), par(id(cod(seq(!s, !t))), seq(!u, !v)))
    par(id(!n), seq(!u, !v)) -> seq(par(id(!n), !u), par(id(!n), !v))
    par(seq(!u, !v), id(!n)) -> seq(par(!u, id(!n)), par(!v, id(!n)))
    seq(par(id(!k1), par(gen(!g1, !ni1, !no1), id(!l1))), par(id(!k2), par(gen(!g2, !ni2, !no2), id(!l2)))) -> seq(layer(!k2, +(!l2, def(gen(!g1, !ni1, !no1))), !g2, !ni2, !no2), layer(-(!k1, def(gen(!g2, !ni2, !no2))), !l1, !g1, !ni1, !no1)) [>=(!k1, +(!k2, !ni2))]
    seq(par(id(!k1), par(gen(!g1, !ni1, !no1), id(!l1))), seq(par(id(!k2), par(gen(!g2, !ni2, !no2), id(!l2))), !t)) -> seq(layer(!k2, +(!l2, def(gen(!g1, !ni1, !no1))), !g2, !ni2, !no2), seq(layer(-(!k1, def(gen(!g2, !ni2, !no2))), !l1, !g1, !ni1, !no1), !t)) [>=(!k1, +(!k2, !ni2))]
* No termination info given.

Elapsed Time: 2296.59 ms