MAYBE MAYBE TRS: { if(true(), X, Y) -> activate(X), if(false(), X, Y) -> activate(Y), zero(0()) -> true(), zero(s(X)) -> false(), fact(X) -> if(zero(X), n__s(n__0()), n__prod(X, n__fact(n__p(X)))), fact(X) -> n__fact(X), add(0(), X) -> X, add(s(X), Y) -> s(add(X, Y)), 0() -> n__0(), s(X) -> n__s(X), prod(X1, X2) -> n__prod(X1, X2), prod(0(), X) -> 0(), prod(s(X), Y) -> add(Y, prod(X, Y)), activate(X) -> X, activate(n__s(X)) -> s(activate(X)), activate(n__0()) -> 0(), activate(n__prod(X1, X2)) -> prod(activate(X1), activate(X2)), activate(n__fact(X)) -> fact(activate(X)), activate(n__p(X)) -> p(activate(X)), p(X) -> n__p(X), p(s(X)) -> X } DUP: We consider a duplicating system. Trs: { if(true(), X, Y) -> activate(X), if(false(), X, Y) -> activate(Y), zero(0()) -> true(), zero(s(X)) -> false(), fact(X) -> if(zero(X), n__s(n__0()), n__prod(X, n__fact(n__p(X)))), fact(X) -> n__fact(X), add(0(), X) -> X, add(s(X), Y) -> s(add(X, Y)), 0() -> n__0(), s(X) -> n__s(X), prod(X1, X2) -> n__prod(X1, X2), prod(0(), X) -> 0(), prod(s(X), Y) -> add(Y, prod(X, Y)), activate(X) -> X, activate(n__s(X)) -> s(activate(X)), activate(n__0()) -> 0(), activate(n__prod(X1, X2)) -> prod(activate(X1), activate(X2)), activate(n__fact(X)) -> fact(activate(X)), activate(n__p(X)) -> p(activate(X)), p(X) -> n__p(X), p(s(X)) -> X } Fail