========================================== reduce in TEST : !(((empty -> F(x:S), F(f-y(x:S))), (G(f-y(x:S)) -> F(x:S)), ( empty -> F(f-y(x:S)), G(x:S)), (H(x:S) -> F(f-y(x:S)), H(f-y(x:S))), (H( f-y(x:S)) -> G(x:S)), (F(f-y(x:S)) -> G(f-y(x:S)), H(x:S)), (F(x:S), F(f-y( x:S)) -> G(f-y(x:S))), (H(f-y(x:S)) -> H(x:S)), (F(f-y(x:S)), G(x:S) -> H( f-y(x:S))), (F(f-z(x:S)), G(f-z(x:S)), H(f-z(x:S)) -> empty), (G(f-y(x:S)), H(x:S) -> H(f-y(x:S))))) . rewrites: 107565 in 542ms cpu (767ms real) (198123 rewrites/second) result State: [empty -> empty,44] Bye.