NO
(ignored inputs)COMMENT TPDB SRS_Standard/Secret_05_SRS/matchbox1
input TRS:
   [ r(e(?x)) -> w(r(?x)),
     i(t(?x)) -> e(r(?x)),
     e(w(?x)) -> r(i(?x)),
     t(e(?x)) -> r(e(?x)),
     w(r(?x)) -> i(t(?x)),
     e(r(?x)) -> e(w(?x)),
     r(i(t(e(r(?x))))) -> e(w(r(i(t(e(?x)))))) ]
TRS:
   [ r(e(?x)) -> w(r(?x)),
     i(t(?x)) -> e(r(?x)),
     e(w(?x)) -> r(i(?x)),
     t(e(?x)) -> r(e(?x)),
     w(r(?x)) -> i(t(?x)),
     e(r(?x)) -> e(w(?x)),
     r(i(t(e(r(?x))))) -> e(w(r(i(t(e(?x)))))) ]
constructed TRS:
   [ r(e(?x)) -> w(r(?x)),
     i(t(?x)) -> e(r(?x)),
     e(w(?x)) -> r(i(?x)),
     t(e(?x)) -> r(e(?x)),
     w(r(?x)) -> i(t(?x)),
     e(r(?x)) -> e(w(?x)),
     r(i(t(e(r(?x))))) -> e(w(r(i(t(e(?x)))))) ]
convertible distinct normal forms: r(i(r(?x))) = r(i(e(?x)))
UNC Completion (Development Closed)
problems/956.trs: Success(not UNC)
(4 msec.)