MAYBE Time: 0.001564 TRS: { f(X1, X2) -> n__f(X1, X2), f(g X, Y) -> f(X, n__f(g X, activate Y)), activate X -> X, activate n__f(X1, X2) -> f(X1, X2)} DP: DP: { f#(g X, Y) -> f#(X, n__f(g X, activate Y)), f#(g X, Y) -> activate# Y, activate# n__f(X1, X2) -> f#(X1, X2)} TRS: { f(X1, X2) -> n__f(X1, X2), f(g X, Y) -> f(X, n__f(g X, activate Y)), activate X -> X, activate n__f(X1, X2) -> f(X1, X2)} UR: { f(X1, X2) -> n__f(X1, X2), f(g X, Y) -> f(X, n__f(g X, activate Y)), activate X -> X, activate n__f(X1, X2) -> f(X1, X2), a(x, y) -> x, a(x, y) -> y} EDG: {(f#(g X, Y) -> activate# Y, activate# n__f(X1, X2) -> f#(X1, X2)) (activate# n__f(X1, X2) -> f#(X1, X2), f#(g X, Y) -> f#(X, n__f(g X, activate Y))) (activate# n__f(X1, X2) -> f#(X1, X2), f#(g X, Y) -> activate# Y) (f#(g X, Y) -> f#(X, n__f(g X, activate Y)), f#(g X, Y) -> f#(X, n__f(g X, activate Y))) (f#(g X, Y) -> f#(X, n__f(g X, activate Y)), f#(g X, Y) -> activate# Y)} EDG: {(f#(g X, Y) -> activate# Y, activate# n__f(X1, X2) -> f#(X1, X2)) (activate# n__f(X1, X2) -> f#(X1, X2), f#(g X, Y) -> f#(X, n__f(g X, activate Y))) (activate# n__f(X1, X2) -> f#(X1, X2), f#(g X, Y) -> activate# Y) (f#(g X, Y) -> f#(X, n__f(g X, activate Y)), f#(g X, Y) -> f#(X, n__f(g X, activate Y))) (f#(g X, Y) -> f#(X, n__f(g X, activate Y)), f#(g X, Y) -> activate# Y)} EDG: {(f#(g X, Y) -> activate# Y, activate# n__f(X1, X2) -> f#(X1, X2)) (activate# n__f(X1, X2) -> f#(X1, X2), f#(g X, Y) -> f#(X, n__f(g X, activate Y))) (activate# n__f(X1, X2) -> f#(X1, X2), f#(g X, Y) -> activate# Y) (f#(g X, Y) -> f#(X, n__f(g X, activate Y)), f#(g X, Y) -> f#(X, n__f(g X, activate Y))) (f#(g X, Y) -> f#(X, n__f(g X, activate Y)), f#(g X, Y) -> activate# Y)} EDG: {(f#(g X, Y) -> activate# Y, activate# n__f(X1, X2) -> f#(X1, X2)) (activate# n__f(X1, X2) -> f#(X1, X2), f#(g X, Y) -> f#(X, n__f(g X, activate Y))) (activate# n__f(X1, X2) -> f#(X1, X2), f#(g X, Y) -> activate# Y) (f#(g X, Y) -> f#(X, n__f(g X, activate Y)), f#(g X, Y) -> f#(X, n__f(g X, activate Y))) (f#(g X, Y) -> f#(X, n__f(g X, activate Y)), f#(g X, Y) -> activate# Y)} STATUS: arrows: 0.444444 SCCS (1): Scc: { f#(g X, Y) -> f#(X, n__f(g X, activate Y)), f#(g X, Y) -> activate# Y, activate# n__f(X1, X2) -> f#(X1, X2)} SCC (3): Strict: { f#(g X, Y) -> f#(X, n__f(g X, activate Y)), f#(g X, Y) -> activate# Y, activate# n__f(X1, X2) -> f#(X1, X2)} Weak: { f(X1, X2) -> n__f(X1, X2), f(g X, Y) -> f(X, n__f(g X, activate Y)), activate X -> X, activate n__f(X1, X2) -> f(X1, X2)} Open