%------------------------------------------------------------------------------ % File : SuperZenon---0.0.1 % Problem : SYN067+1 : TPTP v8.1.0. Released v2.0.0. % Transfm : none % Format : tptp:raw % Command : run_super_zenon -p0 -itptp -om -max-time %d %s % Computer : n029.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8042.1875MB % OS : Linux 3.10.0-693.el7.x86_64 % CPULimit : 300s % WCLimit : 600s % DateTime : Thu Jul 21 12:40:49 EDT 2022 % Result : Theorem 0.13s 0.35s % Output : Proof 0.13s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.02/0.09 % Problem : SYN067+1 : TPTP v8.1.0. Released v2.0.0. % 0.02/0.10 % Command : run_super_zenon -p0 -itptp -om -max-time %d %s % 0.08/0.30 % Computer : n029.cluster.edu % 0.08/0.30 % Model : x86_64 x86_64 % 0.08/0.30 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.08/0.30 % Memory : 8042.1875MB % 0.08/0.30 % OS : Linux 3.10.0-693.el7.x86_64 % 0.08/0.30 % CPULimit : 300 % 0.08/0.30 % WCLimit : 600 % 0.08/0.30 % DateTime : Mon Jul 11 14:58:17 EDT 2022 % 0.08/0.30 % CPUTime : % 0.13/0.35 % SZS status Theorem % 0.13/0.35 (* PROOF-FOUND *) % 0.13/0.35 (* BEGIN-PROOF *) % 0.13/0.35 % SZS output start Proof % 0.13/0.35 1. (big_p (a)) (-. (big_p (a))) ### Axiom % 0.13/0.35 2. (-. (big_p T_0)) (big_p T_0) ### Axiom % 0.13/0.35 3. (-. (Ex Z, (Ex W, ((big_p Z) /\ ((big_r T_0 W) /\ (big_r W Z)))))) (Ex Z, (Ex W, ((big_p Z) /\ ((big_r T_0 W) /\ (big_r W Z))))) ### Axiom % 0.13/0.35 4. ((-. (big_p (a))) \/ ((big_p T_0) \/ (Ex Z, (Ex W, ((big_p Z) /\ ((big_r T_0 W) /\ (big_r W Z))))))) (-. (Ex Z, (Ex W, ((big_p Z) /\ ((big_r T_0 W) /\ (big_r W Z)))))) (-. (big_p T_0)) (big_p (a)) ### DisjTree 1 2 3 % 0.13/0.35 5. (((-. (big_p (a))) \/ ((big_p T_0) \/ (Ex Z, (Ex W, ((big_p Z) /\ ((big_r T_0 W) /\ (big_r W Z))))))) /\ ((-. (big_p (a))) \/ ((-. (Ex Y, ((big_p Y) /\ (big_r T_0 Y)))) \/ (Ex Z, (Ex W, ((big_p Z) /\ ((big_r T_0 W) /\ (big_r W Z)))))))) (big_p (a)) (-. (big_p T_0)) (-. (Ex Z, (Ex W, ((big_p Z) /\ ((big_r T_0 W) /\ (big_r W Z)))))) ### And 4 % 0.13/0.35 6. (All X1, (((-. (big_p (a))) \/ ((big_p X1) \/ (Ex Z1, (Ex W1, ((big_p Z1) /\ ((big_r X1 W1) /\ (big_r W1 Z1))))))) /\ ((-. (big_p (a))) \/ ((-. (Ex Y1, ((big_p Y1) /\ (big_r X1 Y1)))) \/ (Ex Z1, (Ex W1, ((big_p Z1) /\ ((big_r X1 W1) /\ (big_r W1 Z1))))))))) (-. (Ex Z, (Ex W, ((big_p Z) /\ ((big_r T_0 W) /\ (big_r W Z)))))) (-. (big_p T_0)) (big_p (a)) ### All 5 % 0.13/0.35 7. (big_p (a)) (-. (big_p (a))) ### Axiom % 0.13/0.35 8. (Ex Y, ((big_p Y) /\ (big_r T_0 Y))) (-. (Ex Y, ((big_p Y) /\ (big_r T_0 Y)))) ### Axiom % 0.13/0.35 9. (-. (Ex Z, (Ex W, ((big_p Z) /\ ((big_r T_0 W) /\ (big_r W Z)))))) (Ex Z, (Ex W, ((big_p Z) /\ ((big_r T_0 W) /\ (big_r W Z))))) ### Axiom % 0.13/0.35 10. ((-. (big_p (a))) \/ ((-. (Ex Y, ((big_p Y) /\ (big_r T_0 Y)))) \/ (Ex Z, (Ex W, ((big_p Z) /\ ((big_r T_0 W) /\ (big_r W Z))))))) (-. (Ex Z, (Ex W, ((big_p Z) /\ ((big_r T_0 W) /\ (big_r W Z)))))) (Ex Y, ((big_p Y) /\ (big_r T_0 Y))) (big_p (a)) ### DisjTree 7 8 9 % 0.13/0.35 11. (((-. (big_p (a))) \/ ((big_p T_0) \/ (Ex Z, (Ex W, ((big_p Z) /\ ((big_r T_0 W) /\ (big_r W Z))))))) /\ ((-. (big_p (a))) \/ ((-. (Ex Y, ((big_p Y) /\ (big_r T_0 Y)))) \/ (Ex Z, (Ex W, ((big_p Z) /\ ((big_r T_0 W) /\ (big_r W Z)))))))) (big_p (a)) (Ex Y, ((big_p Y) /\ (big_r T_0 Y))) (-. (Ex Z, (Ex W, ((big_p Z) /\ ((big_r T_0 W) /\ (big_r W Z)))))) ### And 10 % 0.13/0.35 12. (All X1, (((-. (big_p (a))) \/ ((big_p X1) \/ (Ex Z1, (Ex W1, ((big_p Z1) /\ ((big_r X1 W1) /\ (big_r W1 Z1))))))) /\ ((-. (big_p (a))) \/ ((-. (Ex Y1, ((big_p Y1) /\ (big_r X1 Y1)))) \/ (Ex Z1, (Ex W1, ((big_p Z1) /\ ((big_r X1 W1) /\ (big_r W1 Z1))))))))) (-. (Ex Z, (Ex W, ((big_p Z) /\ ((big_r T_0 W) /\ (big_r W Z)))))) (Ex Y, ((big_p Y) /\ (big_r T_0 Y))) (big_p (a)) ### All 11 % 0.13/0.35 13. ((big_p T_0) => (Ex Y, ((big_p Y) /\ (big_r T_0 Y)))) (big_p (a)) (-. (Ex Z, (Ex W, ((big_p Z) /\ ((big_r T_0 W) /\ (big_r W Z)))))) (All X1, (((-. (big_p (a))) \/ ((big_p X1) \/ (Ex Z1, (Ex W1, ((big_p Z1) /\ ((big_r X1 W1) /\ (big_r W1 Z1))))))) /\ ((-. (big_p (a))) \/ ((-. (Ex Y1, ((big_p Y1) /\ (big_r X1 Y1)))) \/ (Ex Z1, (Ex W1, ((big_p Z1) /\ ((big_r X1 W1) /\ (big_r W1 Z1))))))))) ### Imply 6 12 % 0.13/0.35 14. (-. (((big_p (a)) /\ ((big_p T_0) => (Ex Y, ((big_p Y) /\ (big_r T_0 Y))))) => (Ex Z, (Ex W, ((big_p Z) /\ ((big_r T_0 W) /\ (big_r W Z))))))) (All X1, (((-. (big_p (a))) \/ ((big_p X1) \/ (Ex Z1, (Ex W1, ((big_p Z1) /\ ((big_r X1 W1) /\ (big_r W1 Z1))))))) /\ ((-. (big_p (a))) \/ ((-. (Ex Y1, ((big_p Y1) /\ (big_r X1 Y1)))) \/ (Ex Z1, (Ex W1, ((big_p Z1) /\ ((big_r X1 W1) /\ (big_r W1 Z1))))))))) ### ConjTree 13 % 0.13/0.35 15. (-. (All X, (((big_p (a)) /\ ((big_p X) => (Ex Y, ((big_p Y) /\ (big_r X Y))))) => (Ex Z, (Ex W, ((big_p Z) /\ ((big_r X W) /\ (big_r W Z)))))))) (All X1, (((-. (big_p (a))) \/ ((big_p X1) \/ (Ex Z1, (Ex W1, ((big_p Z1) /\ ((big_r X1 W1) /\ (big_r W1 Z1))))))) /\ ((-. (big_p (a))) \/ ((-. (Ex Y1, ((big_p Y1) /\ (big_r X1 Y1)))) \/ (Ex Z1, (Ex W1, ((big_p Z1) /\ ((big_r X1 W1) /\ (big_r W1 Z1))))))))) ### NotAllEx 14 % 0.13/0.35 16. (big_p (a)) (-. (big_p (a))) ### Axiom % 0.13/0.35 17. (-. (big_p T_1)) (big_p T_1) ### Axiom % 0.13/0.35 18. (-. ((big_p T_1) => (Ex Y1, ((big_p Y1) /\ (big_r T_1 Y1))))) (-. (big_p T_1)) ### NotImply 17 % 0.13/0.35 19. (-. (Ex Z1, (Ex W1, ((big_p Z1) /\ ((big_r T_1 W1) /\ (big_r W1 Z1)))))) (Ex Z1, (Ex W1, ((big_p Z1) /\ ((big_r T_1 W1) /\ (big_r W1 Z1))))) ### Axiom % 0.13/0.35 20. (((big_p (a)) /\ ((big_p T_1) => (Ex Y1, ((big_p Y1) /\ (big_r T_1 Y1))))) => (Ex Z1, (Ex W1, ((big_p Z1) /\ ((big_r T_1 W1) /\ (big_r W1 Z1)))))) (-. (Ex Z1, (Ex W1, ((big_p Z1) /\ ((big_r T_1 W1) /\ (big_r W1 Z1)))))) (-. (big_p T_1)) (big_p (a)) ### DisjTree 16 18 19 % 0.13/0.35 21. (All X, (((big_p (a)) /\ ((big_p X) => (Ex Y, ((big_p Y) /\ (big_r X Y))))) => (Ex Z, (Ex W, ((big_p Z) /\ ((big_r X W) /\ (big_r W Z))))))) (big_p (a)) (-. (big_p T_1)) (-. (Ex Z1, (Ex W1, ((big_p Z1) /\ ((big_r T_1 W1) /\ (big_r W1 Z1)))))) ### All 20 % 0.13/0.35 22. (-. ((-. (big_p (a))) \/ ((big_p T_1) \/ (Ex Z1, (Ex W1, ((big_p Z1) /\ ((big_r T_1 W1) /\ (big_r W1 Z1)))))))) (All X, (((big_p (a)) /\ ((big_p X) => (Ex Y, ((big_p Y) /\ (big_r X Y))))) => (Ex Z, (Ex W, ((big_p Z) /\ ((big_r X W) /\ (big_r W Z))))))) ### ConjTree 21 % 0.13/0.35 23. (big_p (a)) (-. (big_p (a))) ### Axiom % 0.13/0.35 24. (Ex Y1, ((big_p Y1) /\ (big_r T_1 Y1))) (-. (Ex Y1, ((big_p Y1) /\ (big_r T_1 Y1)))) ### Axiom % 0.13/0.35 25. (-. ((big_p T_1) => (Ex Y1, ((big_p Y1) /\ (big_r T_1 Y1))))) (Ex Y1, ((big_p Y1) /\ (big_r T_1 Y1))) ### NotImply 24 % 0.13/0.35 26. (-. (Ex Z1, (Ex W1, ((big_p Z1) /\ ((big_r T_1 W1) /\ (big_r W1 Z1)))))) (Ex Z1, (Ex W1, ((big_p Z1) /\ ((big_r T_1 W1) /\ (big_r W1 Z1))))) ### Axiom % 0.13/0.35 27. (((big_p (a)) /\ ((big_p T_1) => (Ex Y1, ((big_p Y1) /\ (big_r T_1 Y1))))) => (Ex Z1, (Ex W1, ((big_p Z1) /\ ((big_r T_1 W1) /\ (big_r W1 Z1)))))) (-. (Ex Z1, (Ex W1, ((big_p Z1) /\ ((big_r T_1 W1) /\ (big_r W1 Z1)))))) (Ex Y1, ((big_p Y1) /\ (big_r T_1 Y1))) (big_p (a)) ### DisjTree 23 25 26 % 0.13/0.35 28. (All X, (((big_p (a)) /\ ((big_p X) => (Ex Y, ((big_p Y) /\ (big_r X Y))))) => (Ex Z, (Ex W, ((big_p Z) /\ ((big_r X W) /\ (big_r W Z))))))) (big_p (a)) (Ex Y1, ((big_p Y1) /\ (big_r T_1 Y1))) (-. (Ex Z1, (Ex W1, ((big_p Z1) /\ ((big_r T_1 W1) /\ (big_r W1 Z1)))))) ### All 27 % 0.13/0.35 29. (-. ((-. (big_p (a))) \/ ((-. (Ex Y1, ((big_p Y1) /\ (big_r T_1 Y1)))) \/ (Ex Z1, (Ex W1, ((big_p Z1) /\ ((big_r T_1 W1) /\ (big_r W1 Z1)))))))) (All X, (((big_p (a)) /\ ((big_p X) => (Ex Y, ((big_p Y) /\ (big_r X Y))))) => (Ex Z, (Ex W, ((big_p Z) /\ ((big_r X W) /\ (big_r W Z))))))) ### ConjTree 28 % 0.13/0.35 30. (-. (((-. (big_p (a))) \/ ((big_p T_1) \/ (Ex Z1, (Ex W1, ((big_p Z1) /\ ((big_r T_1 W1) /\ (big_r W1 Z1))))))) /\ ((-. (big_p (a))) \/ ((-. (Ex Y1, ((big_p Y1) /\ (big_r T_1 Y1)))) \/ (Ex Z1, (Ex W1, ((big_p Z1) /\ ((big_r T_1 W1) /\ (big_r W1 Z1))))))))) (All X, (((big_p (a)) /\ ((big_p X) => (Ex Y, ((big_p Y) /\ (big_r X Y))))) => (Ex Z, (Ex W, ((big_p Z) /\ ((big_r X W) /\ (big_r W Z))))))) ### NotAnd 22 29 % 0.13/0.35 31. (-. (All X1, (((-. (big_p (a))) \/ ((big_p X1) \/ (Ex Z1, (Ex W1, ((big_p Z1) /\ ((big_r X1 W1) /\ (big_r W1 Z1))))))) /\ ((-. (big_p (a))) \/ ((-. (Ex Y1, ((big_p Y1) /\ (big_r X1 Y1)))) \/ (Ex Z1, (Ex W1, ((big_p Z1) /\ ((big_r X1 W1) /\ (big_r W1 Z1)))))))))) (All X, (((big_p (a)) /\ ((big_p X) => (Ex Y, ((big_p Y) /\ (big_r X Y))))) => (Ex Z, (Ex W, ((big_p Z) /\ ((big_r X W) /\ (big_r W Z))))))) ### NotAllEx 30 % 0.13/0.35 32. (-. ((All X, (((big_p (a)) /\ ((big_p X) => (Ex Y, ((big_p Y) /\ (big_r X Y))))) => (Ex Z, (Ex W, ((big_p Z) /\ ((big_r X W) /\ (big_r W Z))))))) <=> (All X1, (((-. (big_p (a))) \/ ((big_p X1) \/ (Ex Z1, (Ex W1, ((big_p Z1) /\ ((big_r X1 W1) /\ (big_r W1 Z1))))))) /\ ((-. (big_p (a))) \/ ((-. (Ex Y1, ((big_p Y1) /\ (big_r X1 Y1)))) \/ (Ex Z1, (Ex W1, ((big_p Z1) /\ ((big_r X1 W1) /\ (big_r W1 Z1))))))))))) ### NotEquiv 15 31 % 0.13/0.35 % SZS output end Proof % 0.13/0.35 (* END-PROOF *) %------------------------------------------------------------------------------