一阶逻辑和自动定理证明

如何解决一阶逻辑和自动定理证明

我想问一下 Melvin Fitting 的“一阶逻辑和自动定理证明”一书中的练习是否有任何解决方案。