\sorts { U; } \functions { U c; } \predicates { p(U); q(U); } \problem { (\exists U x; p(x) -> \exists U x; q(x)) -> \exists U x; (p(x) -> q(x)) }