========================================== reduce in TEST : !(((P(x':S, f-y(x:S)) -> P(x':S, x':S)), (P(x':S, x':S) -> P( x':S, f-y(x:S))), (empty -> P(z:S, x:S), P(z:S, f-y'(x:S, x':S))), (P(z:S, x:S), P(z:S, f-y'(x:S, x':S)) -> empty))) . rewrites: 13965 in 58ms cpu (61ms real) (236731 rewrites/second) result State: [empty -> empty,8] Bye.