WYCS: working on the ad-hoc axiom instantiation transform.