========================================== reduce in TEST : !(((empty -> P, Q(x:S)), (Q(f-x''(x:S)) -> P), (P -> Q(f-x'( x:S))), (P, Q(x:S) -> empty))) . rewrites: 1623 in 20ms cpu (20ms real) (77296 rewrites/second) result State: [empty -> empty,6] Bye.