%------------------------------------------------------------------------------ % File : SuperZenon---0.0.1 % Problem : SYN722+1 : TPTP v8.1.0. Released v2.5.0. % Transfm : none % Format : tptp:raw % Command : run_super_zenon -p0 -itptp -om -max-time %d %s % Computer : n014.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:46:06 EDT 2022 % Result : Theorem 0.11s 0.38s % Output : Proof 0.11s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.12 % Problem : SYN722+1 : TPTP v8.1.0. Released v2.5.0. % 0.07/0.12 % Command : run_super_zenon -p0 -itptp -om -max-time %d %s % 0.11/0.32 % Computer : n014.cluster.edu % 0.11/0.32 % Model : x86_64 x86_64 % 0.11/0.32 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.11/0.32 % Memory : 8042.1875MB % 0.11/0.32 % OS : Linux 3.10.0-693.el7.x86_64 % 0.11/0.32 % CPULimit : 300 % 0.11/0.32 % WCLimit : 600 % 0.11/0.32 % DateTime : Mon Jul 11 14:24:34 EDT 2022 % 0.11/0.32 % CPUTime : % 0.11/0.38 % SZS status Theorem % 0.11/0.38 (* PROOF-FOUND *) % 0.11/0.38 (* BEGIN-PROOF *) % 0.11/0.38 % SZS output start Proof % 0.11/0.38 1. (-. (p (a))) (p (a)) ### Axiom % 0.11/0.38 2. (-. (q (a))) (q (a)) ### Axiom % 0.11/0.38 3. (((p (a)) \/ (r (a))) /\ (q (a))) (-. (q (a))) ### And 2 % 0.11/0.38 4. (All Z, (((p Z) \/ (r Z)) /\ (q Z))) (-. (q (a))) ### All 3 % 0.11/0.38 5. (-. (q T_0)) (q T_0) ### Axiom % 0.11/0.38 6. (((p T_0) \/ (r T_0)) /\ (q T_0)) (-. (q T_0)) ### And 5 % 0.11/0.38 7. (All Z, (((p Z) \/ (r Z)) /\ (q Z))) (-. (q T_0)) ### All 6 % 0.11/0.38 8. (-. (q (c))) (q (c)) ### Axiom % 0.11/0.38 9. (((p (c)) \/ (r (c))) /\ (q (c))) (-. (q (c))) ### And 8 % 0.11/0.38 10. (All Z, (((p Z) \/ (r Z)) /\ (q Z))) (-. (q (c))) ### All 9 % 0.11/0.38 11. (-. (q (d))) (q (d)) ### Axiom % 0.11/0.38 12. (((p (d)) \/ (r (d))) /\ (q (d))) (-. (q (d))) ### And 11 % 0.11/0.38 13. (All Z, (((p Z) \/ (r Z)) /\ (q Z))) (-. (q (d))) ### All 12 % 0.11/0.38 14. ((p (a)) \/ ((-. (q (a))) \/ ((-. (q T_0)) \/ ((-. (q (c))) \/ (-. (q (d))))))) (All Z, (((p Z) \/ (r Z)) /\ (q Z))) (-. (p (a))) ### DisjTree 1 4 7 10 13 % 0.11/0.38 15. (Ex Y, ((p (a)) \/ ((-. (q (a))) \/ ((-. (q Y)) \/ ((-. (q (c))) \/ (-. (q (d)))))))) (-. (p (a))) (All Z, (((p Z) \/ (r Z)) /\ (q Z))) ### Exists 14 % 0.11/0.38 16. (All X, (Ex Y, ((p X) \/ ((-. (q X)) \/ ((-. (q Y)) \/ ((-. (q (c))) \/ (-. (q (d))))))))) (All Z, (((p Z) \/ (r Z)) /\ (q Z))) (-. (p (a))) ### All 15 % 0.11/0.38 17. (-. (p (b))) (p (b)) ### Axiom % 0.11/0.38 18. (-. (q (b))) (q (b)) ### Axiom % 0.11/0.38 19. (((p (b)) \/ (r (b))) /\ (q (b))) (-. (q (b))) ### And 18 % 0.11/0.38 20. (All Z, (((p Z) \/ (r Z)) /\ (q Z))) (-. (q (b))) ### All 19 % 0.11/0.38 21. (-. (q T_1)) (q T_1) ### Axiom % 0.11/0.38 22. (((p T_1) \/ (r T_1)) /\ (q T_1)) (-. (q T_1)) ### And 21 % 0.11/0.38 23. (All Z, (((p Z) \/ (r Z)) /\ (q Z))) (-. (q T_1)) ### All 22 % 0.11/0.38 24. ((p (b)) \/ ((-. (q (b))) \/ ((-. (q T_1)) \/ ((-. (q (c))) \/ (-. (q (d))))))) (All Z, (((p Z) \/ (r Z)) /\ (q Z))) (-. (p (b))) ### DisjTree 17 20 23 10 13 % 0.11/0.38 25. (Ex Y, ((p (b)) \/ ((-. (q (b))) \/ ((-. (q Y)) \/ ((-. (q (c))) \/ (-. (q (d)))))))) (-. (p (b))) (All Z, (((p Z) \/ (r Z)) /\ (q Z))) ### Exists 24 % 0.11/0.38 26. (All X, (Ex Y, ((p X) \/ ((-. (q X)) \/ ((-. (q Y)) \/ ((-. (q (c))) \/ (-. (q (d))))))))) (All Z, (((p Z) \/ (r Z)) /\ (q Z))) (-. (p (b))) ### All 25 % 0.11/0.38 27. ((-. (p (a))) \/ (-. (p (b)))) (All Z, (((p Z) \/ (r Z)) /\ (q Z))) (All X, (Ex Y, ((p X) \/ ((-. (q X)) \/ ((-. (q Y)) \/ ((-. (q (c))) \/ (-. (q (d))))))))) ### Or 16 26 % 0.11/0.38 28. ((All Z, (((p Z) \/ (r Z)) /\ (q Z))) /\ ((All X, (Ex Y, ((p X) \/ ((-. (q X)) \/ ((-. (q Y)) \/ ((-. (q (c))) \/ (-. (q (d))))))))) /\ ((-. (p (a))) \/ (-. (p (b)))))) ### ConjTree 27 % 0.11/0.38 29. (-. (-. ((All Z, (((p Z) \/ (r Z)) /\ (q Z))) /\ ((All X, (Ex Y, ((p X) \/ ((-. (q X)) \/ ((-. (q Y)) \/ ((-. (q (c))) \/ (-. (q (d))))))))) /\ ((-. (p (a))) \/ (-. (p (b)))))))) ### NotNot 28 % 0.11/0.38 % SZS output end Proof % 0.11/0.38 (* END-PROOF *) %------------------------------------------------------------------------------