========================================== reduce in TEST : !(((empty -> P(x:S), P(f(x:S))), (P(x:S) -> P(f(x:S))), (P( x:S), P(f(x:S)) -> empty))) . rewrites: 5513 in 38ms cpu (39ms real) (141380 rewrites/second) result State: [empty -> empty,6] Bye.