%------------------------------------------------------------------------------ % File : SuperZenon---0.0.1 % Problem : COM003+2 : TPTP v8.1.0. Bugfixed v2.2.0. % Transfm : none % Format : tptp:raw % Command : run_super_zenon -p0 -itptp -om -max-time %d %s % Computer : n009.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 : Fri Jul 15 01:45:46 EDT 2022 % Result : Theorem 0.19s 0.43s % Output : Proof 0.19s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.12 % Problem : COM003+2 : TPTP v8.1.0. Bugfixed v2.2.0. % 0.03/0.12 % Command : run_super_zenon -p0 -itptp -om -max-time %d %s % 0.12/0.33 % Computer : n009.cluster.edu % 0.12/0.33 % Model : x86_64 x86_64 % 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.33 % Memory : 8042.1875MB % 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.33 % CPULimit : 300 % 0.12/0.33 % WCLimit : 600 % 0.12/0.33 % DateTime : Thu Jun 16 20:07:37 EDT 2022 % 0.12/0.34 % CPUTime : % 0.19/0.43 % SZS status Theorem % 0.19/0.43 (* PROOF-FOUND *) % 0.19/0.43 (* BEGIN-PROOF *) % 0.19/0.43 % SZS output start Proof % 0.19/0.43 1. (Ex X, (algorithm_program_decides X)) (-. (Ex X, (algorithm_program_decides X))) ### Axiom % 0.19/0.43 2. (program T_0) (-. (program T_0)) ### Axiom % 0.19/0.43 3. ((program T_0) /\ (program_decides T_0)) (-. ((program T_0) /\ (program_decides T_0))) ### Axiom % 0.19/0.43 4. (-. (program_program_decides T_0)) ((program T_0) /\ (program_decides T_0)) ### Definition-Pseudo(program_program_decides) 3 % 0.19/0.43 5. (-. ((program_halts2 T_1 T_1) => (halts3_outputs T_0 T_1 T_1 (good)))) ((program_halts2 T_1 T_1) => (halts3_outputs T_0 T_1 T_1 (good))) ### Axiom % 0.19/0.43 6. (program_halts2_halts3_outputs T_0 T_1 T_1 (good)) (-. ((program_halts2 T_1 T_1) => (halts3_outputs T_0 T_1 T_1 (good)))) ### Definition-Pseudo(program_halts2_halts3_outputs) 5 % 0.19/0.43 7. ((program_halts2_halts3_outputs T_0 T_1 T_1 (good)) /\ (program_not_halts2_halts3_outputs T_0 T_1 T_1 (bad))) (-. ((program_halts2 T_1 T_1) => (halts3_outputs T_0 T_1 T_1 (good)))) ### And 6 % 0.19/0.43 8. (All Z, ((program_halts2_halts3_outputs T_0 T_1 Z (good)) /\ (program_not_halts2_halts3_outputs T_0 T_1 Z (bad)))) (-. ((program_halts2 T_1 T_1) => (halts3_outputs T_0 T_1 T_1 (good)))) ### All 7 % 0.19/0.43 9. (All Y, (All Z, ((program_halts2_halts3_outputs T_0 Y Z (good)) /\ (program_not_halts2_halts3_outputs T_0 Y Z (bad))))) (-. ((program_halts2 T_1 T_1) => (halts3_outputs T_0 T_1 T_1 (good)))) ### All 8 % 0.19/0.43 10. ((program_program_decides T_0) => (All Y, (All Z, ((program_halts2_halts3_outputs T_0 Y Z (good)) /\ (program_not_halts2_halts3_outputs T_0 Y Z (bad)))))) (-. ((program_halts2 T_1 T_1) => (halts3_outputs T_0 T_1 T_1 (good)))) ((program T_0) /\ (program_decides T_0)) ### Imply 4 9 % 0.19/0.43 11. (All W, ((program_program_decides W) => (All Y, (All Z, ((program_halts2_halts3_outputs W Y Z (good)) /\ (program_not_halts2_halts3_outputs W Y Z (bad))))))) ((program T_0) /\ (program_decides T_0)) (-. ((program_halts2 T_1 T_1) => (halts3_outputs T_0 T_1 T_1 (good)))) ### All 10 % 0.19/0.43 12. (-. (program_halts2_halts3_outputs T_0 T_1 T_1 (good))) ((program T_0) /\ (program_decides T_0)) (All W, ((program_program_decides W) => (All Y, (All Z, ((program_halts2_halts3_outputs W Y Z (good)) /\ (program_not_halts2_halts3_outputs W Y Z (bad))))))) ### Definition-Pseudo(program_halts2_halts3_outputs) 11 % 0.19/0.43 13. (-. ((program_not_halts2 T_1 T_1) => (halts3_outputs T_0 T_1 T_1 (bad)))) ((program_not_halts2 T_1 T_1) => (halts3_outputs T_0 T_1 T_1 (bad))) ### Axiom % 0.19/0.43 14. (program_not_halts2_halts3_outputs T_0 T_1 T_1 (bad)) (-. ((program_not_halts2 T_1 T_1) => (halts3_outputs T_0 T_1 T_1 (bad)))) ### Definition-Pseudo(program_not_halts2_halts3_outputs) 13 % 0.19/0.43 15. ((program_halts2_halts3_outputs T_0 T_1 T_1 (good)) /\ (program_not_halts2_halts3_outputs T_0 T_1 T_1 (bad))) (-. ((program_not_halts2 T_1 T_1) => (halts3_outputs T_0 T_1 T_1 (bad)))) ### And 14 % 0.19/0.43 16. (All Z, ((program_halts2_halts3_outputs T_0 T_1 Z (good)) /\ (program_not_halts2_halts3_outputs T_0 T_1 Z (bad)))) (-. ((program_not_halts2 T_1 T_1) => (halts3_outputs T_0 T_1 T_1 (bad)))) ### All 15 % 0.19/0.43 17. (All Y, (All Z, ((program_halts2_halts3_outputs T_0 Y Z (good)) /\ (program_not_halts2_halts3_outputs T_0 Y Z (bad))))) (-. ((program_not_halts2 T_1 T_1) => (halts3_outputs T_0 T_1 T_1 (bad)))) ### All 16 % 0.19/0.43 18. ((program_program_decides T_0) => (All Y, (All Z, ((program_halts2_halts3_outputs T_0 Y Z (good)) /\ (program_not_halts2_halts3_outputs T_0 Y Z (bad)))))) (-. ((program_not_halts2 T_1 T_1) => (halts3_outputs T_0 T_1 T_1 (bad)))) ((program T_0) /\ (program_decides T_0)) ### Imply 4 17 % 0.19/0.43 19. (All W, ((program_program_decides W) => (All Y, (All Z, ((program_halts2_halts3_outputs W Y Z (good)) /\ (program_not_halts2_halts3_outputs W Y Z (bad))))))) ((program T_0) /\ (program_decides T_0)) (-. ((program_not_halts2 T_1 T_1) => (halts3_outputs T_0 T_1 T_1 (bad)))) ### All 18 % 0.19/0.43 20. (-. (program_not_halts2_halts3_outputs T_0 T_1 T_1 (bad))) ((program T_0) /\ (program_decides T_0)) (All W, ((program_program_decides W) => (All Y, (All Z, ((program_halts2_halts3_outputs W Y Z (good)) /\ (program_not_halts2_halts3_outputs W Y Z (bad))))))) ### Definition-Pseudo(program_not_halts2_halts3_outputs) 19 % 0.19/0.43 21. (-. ((program_halts2_halts3_outputs T_0 T_1 T_1 (good)) /\ (program_not_halts2_halts3_outputs T_0 T_1 T_1 (bad)))) (All W, ((program_program_decides W) => (All Y, (All Z, ((program_halts2_halts3_outputs W Y Z (good)) /\ (program_not_halts2_halts3_outputs W Y Z (bad))))))) ((program T_0) /\ (program_decides T_0)) ### NotAnd 12 20 % 0.19/0.43 22. (-. (All Y, ((program_halts2_halts3_outputs T_0 Y Y (good)) /\ (program_not_halts2_halts3_outputs T_0 Y Y (bad))))) ((program T_0) /\ (program_decides T_0)) (All W, ((program_program_decides W) => (All Y, (All Z, ((program_halts2_halts3_outputs W Y Z (good)) /\ (program_not_halts2_halts3_outputs W Y Z (bad))))))) ### NotAllEx 21 % 0.19/0.43 23. (-. ((program T_0) /\ (All Y, ((program_halts2_halts3_outputs T_0 Y Y (good)) /\ (program_not_halts2_halts3_outputs T_0 Y Y (bad)))))) (All W, ((program_program_decides W) => (All Y, (All Z, ((program_halts2_halts3_outputs W Y Z (good)) /\ (program_not_halts2_halts3_outputs W Y Z (bad))))))) ((program T_0) /\ (program_decides T_0)) (program T_0) ### NotAnd 2 22 % 0.19/0.43 24. (-. (Ex W, ((program W) /\ (All Y, ((program_halts2_halts3_outputs W Y Y (good)) /\ (program_not_halts2_halts3_outputs W Y Y (bad))))))) (program T_0) ((program T_0) /\ (program_decides T_0)) (All W, ((program_program_decides W) => (All Y, (All Z, ((program_halts2_halts3_outputs W Y Z (good)) /\ (program_not_halts2_halts3_outputs W Y Z (bad))))))) ### NotExists 23 % 0.19/0.43 25. (All W, ((program_program_decides W) => (All Y, (All Z, ((program_halts2_halts3_outputs W Y Z (good)) /\ (program_not_halts2_halts3_outputs W Y Z (bad))))))) ((program T_0) /\ (program_decides T_0)) (-. (Ex W, ((program W) /\ (All Y, ((program_halts2_halts3_outputs W Y Y (good)) /\ (program_not_halts2_halts3_outputs W Y Y (bad))))))) ### And 24 % 0.19/0.43 26. (program_program_decides T_0) (-. (Ex W, ((program W) /\ (All Y, ((program_halts2_halts3_outputs W Y Y (good)) /\ (program_not_halts2_halts3_outputs W Y Y (bad))))))) (All W, ((program_program_decides W) => (All Y, (All Z, ((program_halts2_halts3_outputs W Y Z (good)) /\ (program_not_halts2_halts3_outputs W Y Z (bad))))))) ### Definition-Pseudo(program_program_decides) 25 % 0.19/0.43 27. (Ex W, (program_program_decides W)) (All W, ((program_program_decides W) => (All Y, (All Z, ((program_halts2_halts3_outputs W Y Z (good)) /\ (program_not_halts2_halts3_outputs W Y Z (bad))))))) (-. (Ex W, ((program W) /\ (All Y, ((program_halts2_halts3_outputs W Y Y (good)) /\ (program_not_halts2_halts3_outputs W Y Y (bad))))))) ### Exists 26 % 0.19/0.43 28. ((Ex X, (algorithm_program_decides X)) => (Ex W, (program_program_decides W))) (-. (Ex W, ((program W) /\ (All Y, ((program_halts2_halts3_outputs W Y Y (good)) /\ (program_not_halts2_halts3_outputs W Y Y (bad))))))) (All W, ((program_program_decides W) => (All Y, (All Z, ((program_halts2_halts3_outputs W Y Z (good)) /\ (program_not_halts2_halts3_outputs W Y Z (bad))))))) (Ex X, (algorithm_program_decides X)) ### Imply 1 27 % 0.19/0.43 29. (-. (Ex V, ((program V) /\ (All Y, ((program_halts2_halts2_outputs V Y (good)) /\ (program_not_halts2_halts2_outputs V Y (bad))))))) (Ex V, ((program V) /\ (All Y, ((program_halts2_halts2_outputs V Y (good)) /\ (program_not_halts2_halts2_outputs V Y (bad)))))) ### Axiom % 0.19/0.43 30. ((Ex W, ((program W) /\ (All Y, ((program_halts2_halts3_outputs W Y Y (good)) /\ (program_not_halts2_halts3_outputs W Y Y (bad)))))) => (Ex V, ((program V) /\ (All Y, ((program_halts2_halts2_outputs V Y (good)) /\ (program_not_halts2_halts2_outputs V Y (bad))))))) (-. (Ex V, ((program V) /\ (All Y, ((program_halts2_halts2_outputs V Y (good)) /\ (program_not_halts2_halts2_outputs V Y (bad))))))) (Ex X, (algorithm_program_decides X)) (All W, ((program_program_decides W) => (All Y, (All Z, ((program_halts2_halts3_outputs W Y Z (good)) /\ (program_not_halts2_halts3_outputs W Y Z (bad))))))) ((Ex X, (algorithm_program_decides X)) => (Ex W, (program_program_decides W))) ### Imply 28 29 % 0.19/0.43 31. (program T_2) (-. (program T_2)) ### Axiom % 0.19/0.43 32. (program T_2) (-. (program T_2)) ### Axiom % 0.19/0.43 33. (halts2 T_2 T_2) (-. (halts2 T_2 T_2)) ### Axiom % 0.19/0.43 34. (-. ((program T_2) /\ (halts2 T_2 T_2))) (halts2 T_2 T_2) (program T_2) ### NotAnd 32 33 % 0.19/0.43 35. (-. (program_halts2 T_2 T_2)) (program T_2) (halts2 T_2 T_2) ### Definition-Pseudo(program_halts2) 34 % 0.19/0.43 36. (halts2 T_2 T_2) (-. (halts2 T_2 T_2)) ### Axiom % 0.19/0.43 37. ((program_halts2 T_2 T_2) => (-. (halts2 T_2 T_2))) (halts2 T_2 T_2) (program T_2) ### Imply 35 36 % 0.19/0.43 38. (-. (-. (halts2 T_2 T_2))) (program T_2) ((program_halts2 T_2 T_2) => (-. (halts2 T_2 T_2))) ### NotNot 37 % 0.19/0.43 39. (-. ((program T_2) /\ (-. (halts2 T_2 T_2)))) ((program_halts2 T_2 T_2) => (-. (halts2 T_2 T_2))) (program T_2) ### NotAnd 31 38 % 0.19/0.43 40. (-. (program_not_halts2 T_2 T_2)) (program T_2) ((program_halts2 T_2 T_2) => (-. (halts2 T_2 T_2))) ### Definition-Pseudo(program_not_halts2) 39 % 0.19/0.43 41. ((halts2 T_2 T_2) /\ (outputs T_2 (good))) (program T_2) ((program_halts2 T_2 T_2) => (-. (halts2 T_2 T_2))) ### And 37 % 0.19/0.43 42. (halts2_outputs T_2 T_2 (good)) ((program_halts2 T_2 T_2) => (-. (halts2 T_2 T_2))) (program T_2) ### Definition-Pseudo(halts2_outputs) 41 % 0.19/0.43 43. ((program_not_halts2 T_2 T_2) => (halts2_outputs T_2 T_2 (good))) ((program_halts2 T_2 T_2) => (-. (halts2 T_2 T_2))) (program T_2) ### Imply 40 42 % 0.19/0.43 44. (program_not_halts2_halts2_outputs T_2 T_2 (good)) (program T_2) ((program_halts2 T_2 T_2) => (-. (halts2 T_2 T_2))) ### Definition-Pseudo(program_not_halts2_halts2_outputs) 43 % 0.19/0.43 45. (((program_halts2 T_2 T_2) => (-. (halts2 T_2 T_2))) /\ (program_not_halts2_halts2_outputs T_2 T_2 (good))) (program T_2) ### And 44 % 0.19/0.43 46. (All Y, (((program_halts2 Y Y) => (-. (halts2 T_2 Y))) /\ (program_not_halts2_halts2_outputs T_2 Y (good)))) (program T_2) ### All 45 % 0.19/0.43 47. ((program T_2) /\ (All Y, (((program_halts2 Y Y) => (-. (halts2 T_2 Y))) /\ (program_not_halts2_halts2_outputs T_2 Y (good))))) ### And 46 % 0.19/0.43 48. (Ex U, ((program U) /\ (All Y, (((program_halts2 Y Y) => (-. (halts2 U Y))) /\ (program_not_halts2_halts2_outputs U Y (good)))))) ### Exists 47 % 0.19/0.43 49. ((Ex V, ((program V) /\ (All Y, ((program_halts2_halts2_outputs V Y (good)) /\ (program_not_halts2_halts2_outputs V Y (bad)))))) => (Ex U, ((program U) /\ (All Y, (((program_halts2 Y Y) => (-. (halts2 U Y))) /\ (program_not_halts2_halts2_outputs U Y (good))))))) ((Ex X, (algorithm_program_decides X)) => (Ex W, (program_program_decides W))) (All W, ((program_program_decides W) => (All Y, (All Z, ((program_halts2_halts3_outputs W Y Z (good)) /\ (program_not_halts2_halts3_outputs W Y Z (bad))))))) (Ex X, (algorithm_program_decides X)) ((Ex W, ((program W) /\ (All Y, ((program_halts2_halts3_outputs W Y Y (good)) /\ (program_not_halts2_halts3_outputs W Y Y (bad)))))) => (Ex V, ((program V) /\ (All Y, ((program_halts2_halts2_outputs V Y (good)) /\ (program_not_halts2_halts2_outputs V Y (bad))))))) ### Imply 30 48 % 0.19/0.43 50. (-. (-. (Ex X, (algorithm_program_decides X)))) ((Ex W, ((program W) /\ (All Y, ((program_halts2_halts3_outputs W Y Y (good)) /\ (program_not_halts2_halts3_outputs W Y Y (bad)))))) => (Ex V, ((program V) /\ (All Y, ((program_halts2_halts2_outputs V Y (good)) /\ (program_not_halts2_halts2_outputs V Y (bad))))))) (All W, ((program_program_decides W) => (All Y, (All Z, ((program_halts2_halts3_outputs W Y Z (good)) /\ (program_not_halts2_halts3_outputs W Y Z (bad))))))) ((Ex X, (algorithm_program_decides X)) => (Ex W, (program_program_decides W))) ((Ex V, ((program V) /\ (All Y, ((program_halts2_halts2_outputs V Y (good)) /\ (program_not_halts2_halts2_outputs V Y (bad)))))) => (Ex U, ((program U) /\ (All Y, (((program_halts2 Y Y) => (-. (halts2 U Y))) /\ (program_not_halts2_halts2_outputs U Y (good))))))) ### NotNot 49 % 0.19/0.43 % SZS output end Proof % 0.19/0.43 (* END-PROOF *) %------------------------------------------------------------------------------