========================================== reduce in TEST : !(((empty -> P(c-x)), (empty -> Q(f-y(v:S, w:S))), (P(v:S) -> R(f-z(v:S, w:S))), (R(w:S) -> R(f-z(v:S, w:S))), (P(v:S), Q(v:S) -> empty), (Q(v:S), R(w:S) -> empty))) . rewrites: 3659 in 35ms cpu (35ms real) (101653 rewrites/second) result State: [empty -> empty,8] Bye.