========================================== reduce in TEST : !(((R(x:S) -> H(x:S)), (H(x:S), Q(x:S) -> J(x:S)), (empty -> P(f-x'(x:S))), (P(x:S), G(x:S) -> Q(x:S)), (H(x:S), P(x:S) -> Q(x:S)), ( empty -> R(f-x'(x:S))), (J(f-x'(x:S)) -> empty))) . rewrites: 3598 in 36ms cpu (36ms real) (97256 rewrites/second) result State: [empty -> empty,10] Bye.