NO (ignored inputs)COMMENT TPDB SRS_Standard/Zantema_04/z101 input TRS: [ a(a(?x)) -> b(b(b(?x))), b(b(b(b(?x)))) -> a(a(a(?x))) ] TRS: [ a(a(?x)) -> b(b(b(?x))), b(b(b(b(?x)))) -> a(a(a(?x))) ] constructed TRS: [ a(a(?x)) -> b(b(b(?x))), b(b(b(b(?x)))) -> a(a(a(?x))) ] convertible distinct normal forms: b(b(a(b(b(b(?x)))))) = b(b(b(a(b(b(?x)))))) UNC Completion (Strongly Closed) problems/946.trs: Success(not UNC) (0 msec.)