%------------------------------------------------------------------------------ % File : SuperZenon---0.0.1 % Problem : COM003+3 : 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 : n027.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+3 : TPTP v8.1.0. Released v2.0.0. % 0.03/0.12 % Command : run_super_zenon -p0 -itptp -om -max-time %d %s % 0.12/0.33 % Computer : n027.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 17:01:35 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 X) /\ (All Y, ((program Y) => (All Z, (decides X Y Z)))))) (-. (Ex X, ((algorithm X) /\ (All Y, ((program Y) => (All Z, (decides X Y Z))))))) ### Axiom % 0.19/0.43 2. (program T_0) (-. (program T_0)) ### Axiom % 0.19/0.43 3. (All Y, ((program Y) => (All Z, (decides T_0 Y Z)))) (-. (All Y, ((program Y) => (All Z, (decides T_0 Y Z))))) ### Axiom % 0.19/0.43 4. (program T_0) (-. (program T_0)) ### Axiom % 0.19/0.43 5. (program T_0) (-. (program T_0)) ### Axiom % 0.19/0.43 6. (-. (halts2 T_0 zenon_X1)) (halts2 T_0 zenon_X1) ### Axiom % 0.19/0.43 7. (program T_0) (-. (program T_0)) ### Axiom % 0.19/0.43 8. (All Y, (All Z, ((((program Y) /\ (halts2 Y Z)) => ((halts3 T_0 Y Z) /\ (outputs T_0 (good)))) /\ (((program Y) /\ (-. (halts2 Y Z))) => ((halts3 T_0 Y Z) /\ (outputs T_0 (bad))))))) (-. (All Y, (All Z, ((((program Y) /\ (halts2 Y Z)) => ((halts3 T_0 Y Z) /\ (outputs T_0 (good)))) /\ (((program Y) /\ (-. (halts2 Y Z))) => ((halts3 T_0 Y Z) /\ (outputs T_0 (bad)))))))) ### Axiom % 0.19/0.43 9. (program T_0) (-. (program T_0)) ### Axiom % 0.19/0.43 10. (program T_0) (-. (program T_0)) ### Axiom % 0.19/0.43 11. (program T_0) (-. (program T_0)) ### Axiom % 0.19/0.43 12. (-. (halts2 T_0 T_0)) (halts2 T_0 T_0) ### Axiom % 0.19/0.43 13. (-. (halts3 T_0 T_0 T_0)) (halts3 T_0 T_0 T_0) ### Axiom % 0.19/0.43 14. ((halts3 T_0 T_0 T_0) /\ (outputs T_0 (bad))) (-. (halts3 T_0 T_0 T_0)) ### And 13 % 0.19/0.43 15. (((program T_0) /\ (-. (halts2 T_0 T_0))) => ((halts3 T_0 T_0 T_0) /\ (outputs T_0 (bad)))) (-. (halts3 T_0 T_0 T_0)) (-. (halts2 T_0 T_0)) (program T_0) ### DisjTree 11 12 14 % 0.19/0.43 16. (-. (halts3 T_0 T_0 T_0)) (halts3 T_0 T_0 T_0) ### Axiom % 0.19/0.43 17. ((halts3 T_0 T_0 T_0) /\ (outputs T_0 (good))) (-. (halts3 T_0 T_0 T_0)) ### And 16 % 0.19/0.43 18. (((program T_0) /\ (halts2 T_0 T_0)) => ((halts3 T_0 T_0 T_0) /\ (outputs T_0 (good)))) (-. (halts3 T_0 T_0 T_0)) (((program T_0) /\ (-. (halts2 T_0 T_0))) => ((halts3 T_0 T_0 T_0) /\ (outputs T_0 (bad)))) (program T_0) ### DisjTree 10 15 17 % 0.19/0.43 19. ((((program T_0) /\ (halts2 T_0 T_0)) => ((halts3 T_0 T_0 T_0) /\ (outputs T_0 (good)))) /\ (((program T_0) /\ (-. (halts2 T_0 T_0))) => ((halts3 T_0 T_0 T_0) /\ (outputs T_0 (bad))))) (program T_0) (-. (halts3 T_0 T_0 T_0)) ### And 18 % 0.19/0.43 20. (All Z, ((((program T_0) /\ (halts2 T_0 Z)) => ((halts3 T_0 T_0 Z) /\ (outputs T_0 (good)))) /\ (((program T_0) /\ (-. (halts2 T_0 Z))) => ((halts3 T_0 T_0 Z) /\ (outputs T_0 (bad)))))) (-. (halts3 T_0 T_0 T_0)) (program T_0) ### All 19 % 0.19/0.43 21. (program T_0) (-. (program T_0)) ### Axiom % 0.19/0.43 22. (outputs T_0 (bad)) (-. (outputs T_0 (bad))) ### Axiom % 0.19/0.43 23. (program T_2) (-. (program T_2)) ### Axiom % 0.19/0.43 24. (halts2 T_2 T_0) (-. (halts2 T_2 T_0)) ### Axiom % 0.19/0.43 25. (-. (outputs T_0 (good))) (outputs T_0 (good)) ### Axiom % 0.19/0.43 26. ((halts3 T_0 T_2 T_0) /\ (outputs T_0 (good))) (-. (outputs T_0 (good))) ### And 25 % 0.19/0.43 27. (((program T_2) /\ (halts2 T_2 T_0)) => ((halts3 T_0 T_2 T_0) /\ (outputs T_0 (good)))) (-. (outputs T_0 (good))) (halts2 T_2 T_0) (program T_2) ### DisjTree 23 24 26 % 0.19/0.43 28. ((((program T_2) /\ (halts2 T_2 T_0)) => ((halts3 T_0 T_2 T_0) /\ (outputs T_0 (good)))) /\ (((program T_2) /\ (-. (halts2 T_2 T_0))) => ((halts3 T_0 T_2 T_0) /\ (outputs T_0 (bad))))) (program T_2) (halts2 T_2 T_0) (-. (outputs T_0 (good))) ### And 27 % 0.19/0.43 29. (All Z, ((((program T_2) /\ (halts2 T_2 Z)) => ((halts3 T_0 T_2 Z) /\ (outputs T_0 (good)))) /\ (((program T_2) /\ (-. (halts2 T_2 Z))) => ((halts3 T_0 T_2 Z) /\ (outputs T_0 (bad)))))) (-. (outputs T_0 (good))) (halts2 T_2 T_0) (program T_2) ### All 28 % 0.19/0.43 30. (All Y, (All Z, ((((program Y) /\ (halts2 Y Z)) => ((halts3 T_0 Y Z) /\ (outputs T_0 (good)))) /\ (((program Y) /\ (-. (halts2 Y Z))) => ((halts3 T_0 Y Z) /\ (outputs T_0 (bad))))))) (program T_2) (halts2 T_2 T_0) (-. (outputs T_0 (good))) ### All 29 % 0.19/0.43 31. ((halts2 T_2 T_0) /\ (outputs T_2 (bad))) (-. (outputs T_0 (good))) (program T_2) (All Y, (All Z, ((((program Y) /\ (halts2 Y Z)) => ((halts3 T_0 Y Z) /\ (outputs T_0 (good)))) /\ (((program Y) /\ (-. (halts2 Y Z))) => ((halts3 T_0 Y Z) /\ (outputs T_0 (bad))))))) ### And 30 % 0.19/0.43 32. (((program T_0) /\ ((halts3 T_0 T_0 T_0) /\ (outputs T_0 (bad)))) => ((halts2 T_2 T_0) /\ (outputs T_2 (bad)))) (All Y, (All Z, ((((program Y) /\ (halts2 Y Z)) => ((halts3 T_0 Y Z) /\ (outputs T_0 (good)))) /\ (((program Y) /\ (-. (halts2 Y Z))) => ((halts3 T_0 Y Z) /\ (outputs T_0 (bad))))))) (program T_2) (-. (outputs T_0 (good))) (outputs T_0 (bad)) (All Z, ((((program T_0) /\ (halts2 T_0 Z)) => ((halts3 T_0 T_0 Z) /\ (outputs T_0 (good)))) /\ (((program T_0) /\ (-. (halts2 T_0 Z))) => ((halts3 T_0 T_0 Z) /\ (outputs T_0 (bad)))))) (program T_0) ### DisjTree 21 20 22 31 % 0.19/0.43 33. (program T_0) (-. (program T_0)) ### Axiom % 0.19/0.43 34. (outputs T_0 (bad)) (-. (outputs T_0 (bad))) ### Axiom % 0.19/0.43 35. (-. (halts2 T_2 T_0)) (halts2 T_2 T_0) ### Axiom % 0.19/0.43 36. ((halts2 T_2 T_0) /\ (outputs T_2 (bad))) (-. (halts2 T_2 T_0)) ### And 35 % 0.19/0.43 37. (((program T_0) /\ ((halts3 T_0 T_0 T_0) /\ (outputs T_0 (bad)))) => ((halts2 T_2 T_0) /\ (outputs T_2 (bad)))) (-. (halts2 T_2 T_0)) (outputs T_0 (bad)) (All Z, ((((program T_0) /\ (halts2 T_0 Z)) => ((halts3 T_0 T_0 Z) /\ (outputs T_0 (good)))) /\ (((program T_0) /\ (-. (halts2 T_0 Z))) => ((halts3 T_0 T_0 Z) /\ (outputs T_0 (bad)))))) (program T_0) ### DisjTree 33 20 34 36 % 0.19/0.43 38. (((program T_0) /\ ((halts3 T_0 T_0 T_0) /\ (outputs T_0 (good)))) => (-. (halts2 T_2 T_0))) (outputs T_0 (bad)) (program T_2) (All Y, (All Z, ((((program Y) /\ (halts2 Y Z)) => ((halts3 T_0 Y Z) /\ (outputs T_0 (good)))) /\ (((program Y) /\ (-. (halts2 Y Z))) => ((halts3 T_0 Y Z) /\ (outputs T_0 (bad))))))) (((program T_0) /\ ((halts3 T_0 T_0 T_0) /\ (outputs T_0 (bad)))) => ((halts2 T_2 T_0) /\ (outputs T_2 (bad)))) (All Z, ((((program T_0) /\ (halts2 T_0 Z)) => ((halts3 T_0 T_0 Z) /\ (outputs T_0 (good)))) /\ (((program T_0) /\ (-. (halts2 T_0 Z))) => ((halts3 T_0 T_0 Z) /\ (outputs T_0 (bad)))))) (program T_0) ### DisjTree 9 20 32 37 % 0.19/0.43 39. ((((program T_0) /\ ((halts3 T_0 T_0 T_0) /\ (outputs T_0 (good)))) => (-. (halts2 T_2 T_0))) /\ (((program T_0) /\ ((halts3 T_0 T_0 T_0) /\ (outputs T_0 (bad)))) => ((halts2 T_2 T_0) /\ (outputs T_2 (bad))))) (program T_0) (All Z, ((((program T_0) /\ (halts2 T_0 Z)) => ((halts3 T_0 T_0 Z) /\ (outputs T_0 (good)))) /\ (((program T_0) /\ (-. (halts2 T_0 Z))) => ((halts3 T_0 T_0 Z) /\ (outputs T_0 (bad)))))) (All Y, (All Z, ((((program Y) /\ (halts2 Y Z)) => ((halts3 T_0 Y Z) /\ (outputs T_0 (good)))) /\ (((program Y) /\ (-. (halts2 Y Z))) => ((halts3 T_0 Y Z) /\ (outputs T_0 (bad))))))) (program T_2) (outputs T_0 (bad)) ### And 38 % 0.19/0.43 40. (All Y, ((((program Y) /\ ((halts3 T_0 Y Y) /\ (outputs T_0 (good)))) => (-. (halts2 T_2 Y))) /\ (((program Y) /\ ((halts3 T_0 Y Y) /\ (outputs T_0 (bad)))) => ((halts2 T_2 Y) /\ (outputs T_2 (bad)))))) (outputs T_0 (bad)) (program T_2) (All Y, (All Z, ((((program Y) /\ (halts2 Y Z)) => ((halts3 T_0 Y Z) /\ (outputs T_0 (good)))) /\ (((program Y) /\ (-. (halts2 Y Z))) => ((halts3 T_0 Y Z) /\ (outputs T_0 (bad))))))) (All Z, ((((program T_0) /\ (halts2 T_0 Z)) => ((halts3 T_0 T_0 Z) /\ (outputs T_0 (good)))) /\ (((program T_0) /\ (-. (halts2 T_0 Z))) => ((halts3 T_0 T_0 Z) /\ (outputs T_0 (bad)))))) (program T_0) ### All 39 % 0.19/0.43 41. ((program T_2) /\ (All Y, ((((program Y) /\ ((halts3 T_0 Y Y) /\ (outputs T_0 (good)))) => (-. (halts2 T_2 Y))) /\ (((program Y) /\ ((halts3 T_0 Y Y) /\ (outputs T_0 (bad)))) => ((halts2 T_2 Y) /\ (outputs T_2 (bad))))))) (program T_0) (All Z, ((((program T_0) /\ (halts2 T_0 Z)) => ((halts3 T_0 T_0 Z) /\ (outputs T_0 (good)))) /\ (((program T_0) /\ (-. (halts2 T_0 Z))) => ((halts3 T_0 T_0 Z) /\ (outputs T_0 (bad)))))) (All Y, (All Z, ((((program Y) /\ (halts2 Y Z)) => ((halts3 T_0 Y Z) /\ (outputs T_0 (good)))) /\ (((program Y) /\ (-. (halts2 Y Z))) => ((halts3 T_0 Y Z) /\ (outputs T_0 (bad))))))) (outputs T_0 (bad)) ### And 40 % 0.19/0.43 42. (Ex V, ((program V) /\ (All Y, ((((program Y) /\ ((halts3 T_0 Y Y) /\ (outputs T_0 (good)))) => (-. (halts2 V Y))) /\ (((program Y) /\ ((halts3 T_0 Y Y) /\ (outputs T_0 (bad)))) => ((halts2 V Y) /\ (outputs V (bad)))))))) (outputs T_0 (bad)) (All Y, (All Z, ((((program Y) /\ (halts2 Y Z)) => ((halts3 T_0 Y Z) /\ (outputs T_0 (good)))) /\ (((program Y) /\ (-. (halts2 Y Z))) => ((halts3 T_0 Y Z) /\ (outputs T_0 (bad))))))) (All Z, ((((program T_0) /\ (halts2 T_0 Z)) => ((halts3 T_0 T_0 Z) /\ (outputs T_0 (good)))) /\ (((program T_0) /\ (-. (halts2 T_0 Z))) => ((halts3 T_0 T_0 Z) /\ (outputs T_0 (bad)))))) (program T_0) ### Exists 41 % 0.19/0.44 43. (((program T_0) /\ (All Y, (All Z, ((((program Y) /\ (halts2 Y Z)) => ((halts3 T_0 Y Z) /\ (outputs T_0 (good)))) /\ (((program Y) /\ (-. (halts2 Y Z))) => ((halts3 T_0 Y Z) /\ (outputs T_0 (bad)))))))) => (Ex V, ((program V) /\ (All Y, ((((program Y) /\ ((halts3 T_0 Y Y) /\ (outputs T_0 (good)))) => (-. (halts2 V Y))) /\ (((program Y) /\ ((halts3 T_0 Y Y) /\ (outputs T_0 (bad)))) => ((halts2 V Y) /\ (outputs V (bad))))))))) (All Z, ((((program T_0) /\ (halts2 T_0 Z)) => ((halts3 T_0 T_0 Z) /\ (outputs T_0 (good)))) /\ (((program T_0) /\ (-. (halts2 T_0 Z))) => ((halts3 T_0 T_0 Z) /\ (outputs T_0 (bad)))))) (outputs T_0 (bad)) (All Y, (All Z, ((((program Y) /\ (halts2 Y Z)) => ((halts3 T_0 Y Z) /\ (outputs T_0 (good)))) /\ (((program Y) /\ (-. (halts2 Y Z))) => ((halts3 T_0 Y Z) /\ (outputs T_0 (bad))))))) (program T_0) ### DisjTree 7 8 42 % 0.19/0.44 44. (All W, (((program W) /\ (All Y, (All Z, ((((program Y) /\ (halts2 Y Z)) => ((halts3 W Y Z) /\ (outputs W (good)))) /\ (((program Y) /\ (-. (halts2 Y Z))) => ((halts3 W Y Z) /\ (outputs W (bad)))))))) => (Ex V, ((program V) /\ (All Y, ((((program Y) /\ ((halts3 W Y Y) /\ (outputs W (good)))) => (-. (halts2 V Y))) /\ (((program Y) /\ ((halts3 W Y Y) /\ (outputs W (bad)))) => ((halts2 V Y) /\ (outputs V (bad)))))))))) (program T_0) (All Y, (All Z, ((((program Y) /\ (halts2 Y Z)) => ((halts3 T_0 Y Z) /\ (outputs T_0 (good)))) /\ (((program Y) /\ (-. (halts2 Y Z))) => ((halts3 T_0 Y Z) /\ (outputs T_0 (bad))))))) (outputs T_0 (bad)) (All Z, ((((program T_0) /\ (halts2 T_0 Z)) => ((halts3 T_0 T_0 Z) /\ (outputs T_0 (good)))) /\ (((program T_0) /\ (-. (halts2 T_0 Z))) => ((halts3 T_0 T_0 Z) /\ (outputs T_0 (bad)))))) ### All 43 % 0.19/0.44 45. ((halts3 T_0 T_0 zenon_X1) /\ (outputs T_0 (bad))) (All Z, ((((program T_0) /\ (halts2 T_0 Z)) => ((halts3 T_0 T_0 Z) /\ (outputs T_0 (good)))) /\ (((program T_0) /\ (-. (halts2 T_0 Z))) => ((halts3 T_0 T_0 Z) /\ (outputs T_0 (bad)))))) (All Y, (All Z, ((((program Y) /\ (halts2 Y Z)) => ((halts3 T_0 Y Z) /\ (outputs T_0 (good)))) /\ (((program Y) /\ (-. (halts2 Y Z))) => ((halts3 T_0 Y Z) /\ (outputs T_0 (bad))))))) (program T_0) (All W, (((program W) /\ (All Y, (All Z, ((((program Y) /\ (halts2 Y Z)) => ((halts3 W Y Z) /\ (outputs W (good)))) /\ (((program Y) /\ (-. (halts2 Y Z))) => ((halts3 W Y Z) /\ (outputs W (bad)))))))) => (Ex V, ((program V) /\ (All Y, ((((program Y) /\ ((halts3 W Y Y) /\ (outputs W (good)))) => (-. (halts2 V Y))) /\ (((program Y) /\ ((halts3 W Y Y) /\ (outputs W (bad)))) => ((halts2 V Y) /\ (outputs V (bad)))))))))) ### And 44 % 0.19/0.44 46. (((program T_0) /\ (-. (halts2 T_0 zenon_X1))) => ((halts3 T_0 T_0 zenon_X1) /\ (outputs T_0 (bad)))) (All W, (((program W) /\ (All Y, (All Z, ((((program Y) /\ (halts2 Y Z)) => ((halts3 W Y Z) /\ (outputs W (good)))) /\ (((program Y) /\ (-. (halts2 Y Z))) => ((halts3 W Y Z) /\ (outputs W (bad)))))))) => (Ex V, ((program V) /\ (All Y, ((((program Y) /\ ((halts3 W Y Y) /\ (outputs W (good)))) => (-. (halts2 V Y))) /\ (((program Y) /\ ((halts3 W Y Y) /\ (outputs W (bad)))) => ((halts2 V Y) /\ (outputs V (bad)))))))))) (All Y, (All Z, ((((program Y) /\ (halts2 Y Z)) => ((halts3 T_0 Y Z) /\ (outputs T_0 (good)))) /\ (((program Y) /\ (-. (halts2 Y Z))) => ((halts3 T_0 Y Z) /\ (outputs T_0 (bad))))))) (All Z, ((((program T_0) /\ (halts2 T_0 Z)) => ((halts3 T_0 T_0 Z) /\ (outputs T_0 (good)))) /\ (((program T_0) /\ (-. (halts2 T_0 Z))) => ((halts3 T_0 T_0 Z) /\ (outputs T_0 (bad)))))) (-. (halts2 T_0 zenon_X1)) (program T_0) ### DisjTree 5 6 45 % 0.19/0.44 47. (program T_0) (-. (program T_0)) ### Axiom % 0.19/0.44 48. (All Y, (All Z, ((((program Y) /\ (halts2 Y Z)) => ((halts3 T_0 Y Z) /\ (outputs T_0 (good)))) /\ (((program Y) /\ (-. (halts2 Y Z))) => ((halts3 T_0 Y Z) /\ (outputs T_0 (bad))))))) (-. (All Y, (All Z, ((((program Y) /\ (halts2 Y Z)) => ((halts3 T_0 Y Z) /\ (outputs T_0 (good)))) /\ (((program Y) /\ (-. (halts2 Y Z))) => ((halts3 T_0 Y Z) /\ (outputs T_0 (bad)))))))) ### Axiom % 0.19/0.44 49. (program T_0) (-. (program T_0)) ### Axiom % 0.19/0.44 50. (outputs T_0 (good)) (-. (outputs T_0 (good))) ### Axiom % 0.19/0.44 51. (program T_0) (-. (program T_0)) ### Axiom % 0.19/0.44 52. (program T_2) (-. (program T_2)) ### Axiom % 0.19/0.44 53. (-. (halts2 T_2 T_0)) (halts2 T_2 T_0) ### Axiom % 0.19/0.44 54. (-. (outputs T_0 (bad))) (outputs T_0 (bad)) ### Axiom % 0.19/0.44 55. ((halts3 T_0 T_2 T_0) /\ (outputs T_0 (bad))) (-. (outputs T_0 (bad))) ### And 54 % 0.19/0.44 56. (((program T_2) /\ (-. (halts2 T_2 T_0))) => ((halts3 T_0 T_2 T_0) /\ (outputs T_0 (bad)))) (-. (outputs T_0 (bad))) (-. (halts2 T_2 T_0)) (program T_2) ### DisjTree 52 53 55 % 0.19/0.44 57. ((((program T_2) /\ (halts2 T_2 T_0)) => ((halts3 T_0 T_2 T_0) /\ (outputs T_0 (good)))) /\ (((program T_2) /\ (-. (halts2 T_2 T_0))) => ((halts3 T_0 T_2 T_0) /\ (outputs T_0 (bad))))) (program T_2) (-. (halts2 T_2 T_0)) (-. (outputs T_0 (bad))) ### And 56 % 0.19/0.44 58. (All Z, ((((program T_2) /\ (halts2 T_2 Z)) => ((halts3 T_0 T_2 Z) /\ (outputs T_0 (good)))) /\ (((program T_2) /\ (-. (halts2 T_2 Z))) => ((halts3 T_0 T_2 Z) /\ (outputs T_0 (bad)))))) (-. (outputs T_0 (bad))) (-. (halts2 T_2 T_0)) (program T_2) ### All 57 % 0.19/0.44 59. (All Y, (All Z, ((((program Y) /\ (halts2 Y Z)) => ((halts3 T_0 Y Z) /\ (outputs T_0 (good)))) /\ (((program Y) /\ (-. (halts2 Y Z))) => ((halts3 T_0 Y Z) /\ (outputs T_0 (bad))))))) (program T_2) (-. (halts2 T_2 T_0)) (-. (outputs T_0 (bad))) ### All 58 % 0.19/0.44 60. (((program T_0) /\ ((halts3 T_0 T_0 T_0) /\ (outputs T_0 (bad)))) => ((halts2 T_2 T_0) /\ (outputs T_2 (bad)))) (-. (halts2 T_2 T_0)) (program T_2) (All Y, (All Z, ((((program Y) /\ (halts2 Y Z)) => ((halts3 T_0 Y Z) /\ (outputs T_0 (good)))) /\ (((program Y) /\ (-. (halts2 Y Z))) => ((halts3 T_0 Y Z) /\ (outputs T_0 (bad))))))) (All Z, ((((program T_0) /\ (halts2 T_0 Z)) => ((halts3 T_0 T_0 Z) /\ (outputs T_0 (good)))) /\ (((program T_0) /\ (-. (halts2 T_0 Z))) => ((halts3 T_0 T_0 Z) /\ (outputs T_0 (bad)))))) (program T_0) ### DisjTree 51 20 59 36 % 0.19/0.44 61. (((program T_0) /\ ((halts3 T_0 T_0 T_0) /\ (outputs T_0 (good)))) => (-. (halts2 T_2 T_0))) (All Y, (All Z, ((((program Y) /\ (halts2 Y Z)) => ((halts3 T_0 Y Z) /\ (outputs T_0 (good)))) /\ (((program Y) /\ (-. (halts2 Y Z))) => ((halts3 T_0 Y Z) /\ (outputs T_0 (bad))))))) (program T_2) (((program T_0) /\ ((halts3 T_0 T_0 T_0) /\ (outputs T_0 (bad)))) => ((halts2 T_2 T_0) /\ (outputs T_2 (bad)))) (outputs T_0 (good)) (All Z, ((((program T_0) /\ (halts2 T_0 Z)) => ((halts3 T_0 T_0 Z) /\ (outputs T_0 (good)))) /\ (((program T_0) /\ (-. (halts2 T_0 Z))) => ((halts3 T_0 T_0 Z) /\ (outputs T_0 (bad)))))) (program T_0) ### DisjTree 49 20 50 60 % 0.19/0.44 62. ((((program T_0) /\ ((halts3 T_0 T_0 T_0) /\ (outputs T_0 (good)))) => (-. (halts2 T_2 T_0))) /\ (((program T_0) /\ ((halts3 T_0 T_0 T_0) /\ (outputs T_0 (bad)))) => ((halts2 T_2 T_0) /\ (outputs T_2 (bad))))) (program T_0) (All Z, ((((program T_0) /\ (halts2 T_0 Z)) => ((halts3 T_0 T_0 Z) /\ (outputs T_0 (good)))) /\ (((program T_0) /\ (-. (halts2 T_0 Z))) => ((halts3 T_0 T_0 Z) /\ (outputs T_0 (bad)))))) (outputs T_0 (good)) (program T_2) (All Y, (All Z, ((((program Y) /\ (halts2 Y Z)) => ((halts3 T_0 Y Z) /\ (outputs T_0 (good)))) /\ (((program Y) /\ (-. (halts2 Y Z))) => ((halts3 T_0 Y Z) /\ (outputs T_0 (bad))))))) ### And 61 % 0.19/0.44 63. (All Y, ((((program Y) /\ ((halts3 T_0 Y Y) /\ (outputs T_0 (good)))) => (-. (halts2 T_2 Y))) /\ (((program Y) /\ ((halts3 T_0 Y Y) /\ (outputs T_0 (bad)))) => ((halts2 T_2 Y) /\ (outputs T_2 (bad)))))) (All Y, (All Z, ((((program Y) /\ (halts2 Y Z)) => ((halts3 T_0 Y Z) /\ (outputs T_0 (good)))) /\ (((program Y) /\ (-. (halts2 Y Z))) => ((halts3 T_0 Y Z) /\ (outputs T_0 (bad))))))) (program T_2) (outputs T_0 (good)) (All Z, ((((program T_0) /\ (halts2 T_0 Z)) => ((halts3 T_0 T_0 Z) /\ (outputs T_0 (good)))) /\ (((program T_0) /\ (-. (halts2 T_0 Z))) => ((halts3 T_0 T_0 Z) /\ (outputs T_0 (bad)))))) (program T_0) ### All 62 % 0.19/0.44 64. ((program T_2) /\ (All Y, ((((program Y) /\ ((halts3 T_0 Y Y) /\ (outputs T_0 (good)))) => (-. (halts2 T_2 Y))) /\ (((program Y) /\ ((halts3 T_0 Y Y) /\ (outputs T_0 (bad)))) => ((halts2 T_2 Y) /\ (outputs T_2 (bad))))))) (program T_0) (All Z, ((((program T_0) /\ (halts2 T_0 Z)) => ((halts3 T_0 T_0 Z) /\ (outputs T_0 (good)))) /\ (((program T_0) /\ (-. (halts2 T_0 Z))) => ((halts3 T_0 T_0 Z) /\ (outputs T_0 (bad)))))) (outputs T_0 (good)) (All Y, (All Z, ((((program Y) /\ (halts2 Y Z)) => ((halts3 T_0 Y Z) /\ (outputs T_0 (good)))) /\ (((program Y) /\ (-. (halts2 Y Z))) => ((halts3 T_0 Y Z) /\ (outputs T_0 (bad))))))) ### And 63 % 0.19/0.44 65. (Ex V, ((program V) /\ (All Y, ((((program Y) /\ ((halts3 T_0 Y Y) /\ (outputs T_0 (good)))) => (-. (halts2 V Y))) /\ (((program Y) /\ ((halts3 T_0 Y Y) /\ (outputs T_0 (bad)))) => ((halts2 V Y) /\ (outputs V (bad)))))))) (All Y, (All Z, ((((program Y) /\ (halts2 Y Z)) => ((halts3 T_0 Y Z) /\ (outputs T_0 (good)))) /\ (((program Y) /\ (-. (halts2 Y Z))) => ((halts3 T_0 Y Z) /\ (outputs T_0 (bad))))))) (outputs T_0 (good)) (All Z, ((((program T_0) /\ (halts2 T_0 Z)) => ((halts3 T_0 T_0 Z) /\ (outputs T_0 (good)))) /\ (((program T_0) /\ (-. (halts2 T_0 Z))) => ((halts3 T_0 T_0 Z) /\ (outputs T_0 (bad)))))) (program T_0) ### Exists 64 % 0.19/0.44 66. (((program T_0) /\ (All Y, (All Z, ((((program Y) /\ (halts2 Y Z)) => ((halts3 T_0 Y Z) /\ (outputs T_0 (good)))) /\ (((program Y) /\ (-. (halts2 Y Z))) => ((halts3 T_0 Y Z) /\ (outputs T_0 (bad)))))))) => (Ex V, ((program V) /\ (All Y, ((((program Y) /\ ((halts3 T_0 Y Y) /\ (outputs T_0 (good)))) => (-. (halts2 V Y))) /\ (((program Y) /\ ((halts3 T_0 Y Y) /\ (outputs T_0 (bad)))) => ((halts2 V Y) /\ (outputs V (bad))))))))) (All Z, ((((program T_0) /\ (halts2 T_0 Z)) => ((halts3 T_0 T_0 Z) /\ (outputs T_0 (good)))) /\ (((program T_0) /\ (-. (halts2 T_0 Z))) => ((halts3 T_0 T_0 Z) /\ (outputs T_0 (bad)))))) (outputs T_0 (good)) (All Y, (All Z, ((((program Y) /\ (halts2 Y Z)) => ((halts3 T_0 Y Z) /\ (outputs T_0 (good)))) /\ (((program Y) /\ (-. (halts2 Y Z))) => ((halts3 T_0 Y Z) /\ (outputs T_0 (bad))))))) (program T_0) ### DisjTree 47 48 65 % 0.19/0.44 67. (All W, (((program W) /\ (All Y, (All Z, ((((program Y) /\ (halts2 Y Z)) => ((halts3 W Y Z) /\ (outputs W (good)))) /\ (((program Y) /\ (-. (halts2 Y Z))) => ((halts3 W Y Z) /\ (outputs W (bad)))))))) => (Ex V, ((program V) /\ (All Y, ((((program Y) /\ ((halts3 W Y Y) /\ (outputs W (good)))) => (-. (halts2 V Y))) /\ (((program Y) /\ ((halts3 W Y Y) /\ (outputs W (bad)))) => ((halts2 V Y) /\ (outputs V (bad)))))))))) (program T_0) (All Y, (All Z, ((((program Y) /\ (halts2 Y Z)) => ((halts3 T_0 Y Z) /\ (outputs T_0 (good)))) /\ (((program Y) /\ (-. (halts2 Y Z))) => ((halts3 T_0 Y Z) /\ (outputs T_0 (bad))))))) (outputs T_0 (good)) (All Z, ((((program T_0) /\ (halts2 T_0 Z)) => ((halts3 T_0 T_0 Z) /\ (outputs T_0 (good)))) /\ (((program T_0) /\ (-. (halts2 T_0 Z))) => ((halts3 T_0 T_0 Z) /\ (outputs T_0 (bad)))))) ### All 66 % 0.19/0.44 68. ((halts3 T_0 T_0 zenon_X1) /\ (outputs T_0 (good))) (All Z, ((((program T_0) /\ (halts2 T_0 Z)) => ((halts3 T_0 T_0 Z) /\ (outputs T_0 (good)))) /\ (((program T_0) /\ (-. (halts2 T_0 Z))) => ((halts3 T_0 T_0 Z) /\ (outputs T_0 (bad)))))) (All Y, (All Z, ((((program Y) /\ (halts2 Y Z)) => ((halts3 T_0 Y Z) /\ (outputs T_0 (good)))) /\ (((program Y) /\ (-. (halts2 Y Z))) => ((halts3 T_0 Y Z) /\ (outputs T_0 (bad))))))) (program T_0) (All W, (((program W) /\ (All Y, (All Z, ((((program Y) /\ (halts2 Y Z)) => ((halts3 W Y Z) /\ (outputs W (good)))) /\ (((program Y) /\ (-. (halts2 Y Z))) => ((halts3 W Y Z) /\ (outputs W (bad)))))))) => (Ex V, ((program V) /\ (All Y, ((((program Y) /\ ((halts3 W Y Y) /\ (outputs W (good)))) => (-. (halts2 V Y))) /\ (((program Y) /\ ((halts3 W Y Y) /\ (outputs W (bad)))) => ((halts2 V Y) /\ (outputs V (bad)))))))))) ### And 67 % 0.19/0.44 69. (((program T_0) /\ (halts2 T_0 zenon_X1)) => ((halts3 T_0 T_0 zenon_X1) /\ (outputs T_0 (good)))) (All Z, ((((program T_0) /\ (halts2 T_0 Z)) => ((halts3 T_0 T_0 Z) /\ (outputs T_0 (good)))) /\ (((program T_0) /\ (-. (halts2 T_0 Z))) => ((halts3 T_0 T_0 Z) /\ (outputs T_0 (bad)))))) (All Y, (All Z, ((((program Y) /\ (halts2 Y Z)) => ((halts3 T_0 Y Z) /\ (outputs T_0 (good)))) /\ (((program Y) /\ (-. (halts2 Y Z))) => ((halts3 T_0 Y Z) /\ (outputs T_0 (bad))))))) (All W, (((program W) /\ (All Y, (All Z, ((((program Y) /\ (halts2 Y Z)) => ((halts3 W Y Z) /\ (outputs W (good)))) /\ (((program Y) /\ (-. (halts2 Y Z))) => ((halts3 W Y Z) /\ (outputs W (bad)))))))) => (Ex V, ((program V) /\ (All Y, ((((program Y) /\ ((halts3 W Y Y) /\ (outputs W (good)))) => (-. (halts2 V Y))) /\ (((program Y) /\ ((halts3 W Y Y) /\ (outputs W (bad)))) => ((halts2 V Y) /\ (outputs V (bad)))))))))) (((program T_0) /\ (-. (halts2 T_0 zenon_X1))) => ((halts3 T_0 T_0 zenon_X1) /\ (outputs T_0 (bad)))) (program T_0) ### DisjTree 4 46 68 % 0.19/0.44 70. ((((program T_0) /\ (halts2 T_0 zenon_X1)) => ((halts3 T_0 T_0 zenon_X1) /\ (outputs T_0 (good)))) /\ (((program T_0) /\ (-. (halts2 T_0 zenon_X1))) => ((halts3 T_0 T_0 zenon_X1) /\ (outputs T_0 (bad))))) (program T_0) (All W, (((program W) /\ (All Y, (All Z, ((((program Y) /\ (halts2 Y Z)) => ((halts3 W Y Z) /\ (outputs W (good)))) /\ (((program Y) /\ (-. (halts2 Y Z))) => ((halts3 W Y Z) /\ (outputs W (bad)))))))) => (Ex V, ((program V) /\ (All Y, ((((program Y) /\ ((halts3 W Y Y) /\ (outputs W (good)))) => (-. (halts2 V Y))) /\ (((program Y) /\ ((halts3 W Y Y) /\ (outputs W (bad)))) => ((halts2 V Y) /\ (outputs V (bad)))))))))) (All Y, (All Z, ((((program Y) /\ (halts2 Y Z)) => ((halts3 T_0 Y Z) /\ (outputs T_0 (good)))) /\ (((program Y) /\ (-. (halts2 Y Z))) => ((halts3 T_0 Y Z) /\ (outputs T_0 (bad))))))) (All Z, ((((program T_0) /\ (halts2 T_0 Z)) => ((halts3 T_0 T_0 Z) /\ (outputs T_0 (good)))) /\ (((program T_0) /\ (-. (halts2 T_0 Z))) => ((halts3 T_0 T_0 Z) /\ (outputs T_0 (bad)))))) ### And 69 % 0.19/0.44 71. (All Z, ((((program T_0) /\ (halts2 T_0 Z)) => ((halts3 T_0 T_0 Z) /\ (outputs T_0 (good)))) /\ (((program T_0) /\ (-. (halts2 T_0 Z))) => ((halts3 T_0 T_0 Z) /\ (outputs T_0 (bad)))))) (All Y, (All Z, ((((program Y) /\ (halts2 Y Z)) => ((halts3 T_0 Y Z) /\ (outputs T_0 (good)))) /\ (((program Y) /\ (-. (halts2 Y Z))) => ((halts3 T_0 Y Z) /\ (outputs T_0 (bad))))))) (All W, (((program W) /\ (All Y, (All Z, ((((program Y) /\ (halts2 Y Z)) => ((halts3 W Y Z) /\ (outputs W (good)))) /\ (((program Y) /\ (-. (halts2 Y Z))) => ((halts3 W Y Z) /\ (outputs W (bad)))))))) => (Ex V, ((program V) /\ (All Y, ((((program Y) /\ ((halts3 W Y Y) /\ (outputs W (good)))) => (-. (halts2 V Y))) /\ (((program Y) /\ ((halts3 W Y Y) /\ (outputs W (bad)))) => ((halts2 V Y) /\ (outputs V (bad)))))))))) (program T_0) ### All 70 % 0.19/0.44 72. (program T_0) (All W, (((program W) /\ (All Y, (All Z, ((((program Y) /\ (halts2 Y Z)) => ((halts3 W Y Z) /\ (outputs W (good)))) /\ (((program Y) /\ (-. (halts2 Y Z))) => ((halts3 W Y Z) /\ (outputs W (bad)))))))) => (Ex V, ((program V) /\ (All Y, ((((program Y) /\ ((halts3 W Y Y) /\ (outputs W (good)))) => (-. (halts2 V Y))) /\ (((program Y) /\ ((halts3 W Y Y) /\ (outputs W (bad)))) => ((halts2 V Y) /\ (outputs V (bad)))))))))) (All Y, (All Z, ((((program Y) /\ (halts2 Y Z)) => ((halts3 T_0 Y Z) /\ (outputs T_0 (good)))) /\ (((program Y) /\ (-. (halts2 Y Z))) => ((halts3 T_0 Y Z) /\ (outputs T_0 (bad))))))) ### All 71 % 0.19/0.44 73. (((program T_0) /\ (All Y, ((program Y) => (All Z, (decides T_0 Y Z))))) => (All Y, (All Z, ((((program Y) /\ (halts2 Y Z)) => ((halts3 T_0 Y Z) /\ (outputs T_0 (good)))) /\ (((program Y) /\ (-. (halts2 Y Z))) => ((halts3 T_0 Y Z) /\ (outputs T_0 (bad)))))))) (All W, (((program W) /\ (All Y, (All Z, ((((program Y) /\ (halts2 Y Z)) => ((halts3 W Y Z) /\ (outputs W (good)))) /\ (((program Y) /\ (-. (halts2 Y Z))) => ((halts3 W Y Z) /\ (outputs W (bad)))))))) => (Ex V, ((program V) /\ (All Y, ((((program Y) /\ ((halts3 W Y Y) /\ (outputs W (good)))) => (-. (halts2 V Y))) /\ (((program Y) /\ ((halts3 W Y Y) /\ (outputs W (bad)))) => ((halts2 V Y) /\ (outputs V (bad)))))))))) (All Y, ((program Y) => (All Z, (decides T_0 Y Z)))) (program T_0) ### DisjTree 2 3 72 % 0.19/0.44 74. (All W, (((program W) /\ (All Y, ((program Y) => (All Z, (decides W Y Z))))) => (All Y, (All Z, ((((program Y) /\ (halts2 Y Z)) => ((halts3 W Y Z) /\ (outputs W (good)))) /\ (((program Y) /\ (-. (halts2 Y Z))) => ((halts3 W Y Z) /\ (outputs W (bad))))))))) (program T_0) (All Y, ((program Y) => (All Z, (decides T_0 Y Z)))) (All W, (((program W) /\ (All Y, (All Z, ((((program Y) /\ (halts2 Y Z)) => ((halts3 W Y Z) /\ (outputs W (good)))) /\ (((program Y) /\ (-. (halts2 Y Z))) => ((halts3 W Y Z) /\ (outputs W (bad)))))))) => (Ex V, ((program V) /\ (All Y, ((((program Y) /\ ((halts3 W Y Y) /\ (outputs W (good)))) => (-. (halts2 V Y))) /\ (((program Y) /\ ((halts3 W Y Y) /\ (outputs W (bad)))) => ((halts2 V Y) /\ (outputs V (bad)))))))))) ### All 73 % 0.19/0.45 75. ((program T_0) /\ (All Y, ((program Y) => (All Z, (decides T_0 Y Z))))) (All W, (((program W) /\ (All Y, (All Z, ((((program Y) /\ (halts2 Y Z)) => ((halts3 W Y Z) /\ (outputs W (good)))) /\ (((program Y) /\ (-. (halts2 Y Z))) => ((halts3 W Y Z) /\ (outputs W (bad)))))))) => (Ex V, ((program V) /\ (All Y, ((((program Y) /\ ((halts3 W Y Y) /\ (outputs W (good)))) => (-. (halts2 V Y))) /\ (((program Y) /\ ((halts3 W Y Y) /\ (outputs W (bad)))) => ((halts2 V Y) /\ (outputs V (bad)))))))))) (All W, (((program W) /\ (All Y, ((program Y) => (All Z, (decides W Y Z))))) => (All Y, (All Z, ((((program Y) /\ (halts2 Y Z)) => ((halts3 W Y Z) /\ (outputs W (good)))) /\ (((program Y) /\ (-. (halts2 Y Z))) => ((halts3 W Y Z) /\ (outputs W (bad))))))))) ### And 74 % 0.19/0.45 76. (Ex W, ((program W) /\ (All Y, ((program Y) => (All Z, (decides W Y Z)))))) (All W, (((program W) /\ (All Y, ((program Y) => (All Z, (decides W Y Z))))) => (All Y, (All Z, ((((program Y) /\ (halts2 Y Z)) => ((halts3 W Y Z) /\ (outputs W (good)))) /\ (((program Y) /\ (-. (halts2 Y Z))) => ((halts3 W Y Z) /\ (outputs W (bad))))))))) (All W, (((program W) /\ (All Y, (All Z, ((((program Y) /\ (halts2 Y Z)) => ((halts3 W Y Z) /\ (outputs W (good)))) /\ (((program Y) /\ (-. (halts2 Y Z))) => ((halts3 W Y Z) /\ (outputs W (bad)))))))) => (Ex V, ((program V) /\ (All Y, ((((program Y) /\ ((halts3 W Y Y) /\ (outputs W (good)))) => (-. (halts2 V Y))) /\ (((program Y) /\ ((halts3 W Y Y) /\ (outputs W (bad)))) => ((halts2 V Y) /\ (outputs V (bad)))))))))) ### Exists 75 % 0.19/0.45 77. ((Ex X, ((algorithm X) /\ (All Y, ((program Y) => (All Z, (decides X Y Z)))))) => (Ex W, ((program W) /\ (All Y, ((program Y) => (All Z, (decides W Y Z))))))) (All W, (((program W) /\ (All Y, (All Z, ((((program Y) /\ (halts2 Y Z)) => ((halts3 W Y Z) /\ (outputs W (good)))) /\ (((program Y) /\ (-. (halts2 Y Z))) => ((halts3 W Y Z) /\ (outputs W (bad)))))))) => (Ex V, ((program V) /\ (All Y, ((((program Y) /\ ((halts3 W Y Y) /\ (outputs W (good)))) => (-. (halts2 V Y))) /\ (((program Y) /\ ((halts3 W Y Y) /\ (outputs W (bad)))) => ((halts2 V Y) /\ (outputs V (bad)))))))))) (All W, (((program W) /\ (All Y, ((program Y) => (All Z, (decides W Y Z))))) => (All Y, (All Z, ((((program Y) /\ (halts2 Y Z)) => ((halts3 W Y Z) /\ (outputs W (good)))) /\ (((program Y) /\ (-. (halts2 Y Z))) => ((halts3 W Y Z) /\ (outputs W (bad))))))))) (Ex X, ((algorithm X) /\ (All Y, ((program Y) => (All Z, (decides X Y Z)))))) ### Imply 1 76 % 0.19/0.45 78. (-. (-. (Ex X, ((algorithm X) /\ (All Y, ((program Y) => (All Z, (decides X Y Z)))))))) (All W, (((program W) /\ (All Y, ((program Y) => (All Z, (decides W Y Z))))) => (All Y, (All Z, ((((program Y) /\ (halts2 Y Z)) => ((halts3 W Y Z) /\ (outputs W (good)))) /\ (((program Y) /\ (-. (halts2 Y Z))) => ((halts3 W Y Z) /\ (outputs W (bad))))))))) (All W, (((program W) /\ (All Y, (All Z, ((((program Y) /\ (halts2 Y Z)) => ((halts3 W Y Z) /\ (outputs W (good)))) /\ (((program Y) /\ (-. (halts2 Y Z))) => ((halts3 W Y Z) /\ (outputs W (bad)))))))) => (Ex V, ((program V) /\ (All Y, ((((program Y) /\ ((halts3 W Y Y) /\ (outputs W (good)))) => (-. (halts2 V Y))) /\ (((program Y) /\ ((halts3 W Y Y) /\ (outputs W (bad)))) => ((halts2 V Y) /\ (outputs V (bad)))))))))) ((Ex X, ((algorithm X) /\ (All Y, ((program Y) => (All Z, (decides X Y Z)))))) => (Ex W, ((program W) /\ (All Y, ((program Y) => (All Z, (decides W Y Z))))))) ### NotNot 77 % 0.19/0.45 % SZS output end Proof % 0.19/0.45 (* END-PROOF *) %------------------------------------------------------------------------------