expected_output.txt

(p(x)) \/ (~(p(x))) is valid.
(forall x.(p(x))) -> (p(x)) is valid.
(forall x.(p(x))) -> (exists x.(p(x))) is valid.
(forall x.(p(x))) -> (forall y.(p(y))) is valid.
(forall x.((p(x)) \/ (q(x)))) -> ((exists x.(p(x))) \/ (forall x.(q(x)))) is valid.
(forall x.((p(x)) /\ (q(x)))) -> ((forall x.(p(x))) /\ (forall x.(q(x)))) is valid.
(forall x.((p(x)) -> (q(x)))) -> ((forall x.(p(x))) -> (forall x.(q(x)))) is valid.
(exists x.((p(x)) /\ (q(x)))) -> ((exists x.(p(x))) /\ (exists x.(q(x)))) is valid.
((exists x.(p(x))) /\ (forall x.((p(x)) -> (q(x))))) -> (exists x.(q(x))) is valid.
~(exists y.(forall z.((p(z, y)) <-> (~(exists x.((p(z, x)) /\ (p(x, z)))))))) is valid.
(exists x.(p(x))) -> (forall x.(p(x))) is invalid.
~(forall x.(forall y.(((p(x)) \/ (~(q(x)))) /\ ((~(p(y))) \/ (q(y)))))) may be valid or invalid. Since first order logic is undecidable, the program may run forever, so it can't tell us.