Some further possibilities of the theorem prover of the system GRAPH [2]--[5] are described. Instead of skolemization of a formula, we transform the subgoal into an equivalent form or into a stronger subgoal with less quantifiers, in a human like manner. A heuristic is proposed how to choose, among several possibilities, a stronger subgoal which would be proved more easily. Although an incomplete method, it is suitable for interactive work since human behavior is imitated. If machine's choice is not suitable, the user can appropriately modify the transformation.