Странный вопрос.
1. На него должна ответить документация по тем системам.
2. Если всё плохо, то, разумеется, преобразуйте к виду с переменными одного сорта, а лучше просто найдите такое представление — оно уже очень давно где-нибудь должно быть выписано.
Хотя, конечно, на форуме могут оказаться люди, которые лучше вас знают Vampire, E и Spass.
-- Вт ноя 17, 2015 20:44:11 --(А что стало с ZFC?)