%------------------------------------------------------------------------------ % File : Zenon---0.7.1 % Problem : RNG106+1 : TPTP v8.1.0. Released v4.0.0. % Transfm : none % Format : tptp:raw % Command : run_zenon %s %d % Computer : n032.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 : Mon Jul 18 20:48:28 EDT 2022 % Result : Theorem 0.15s 0.49s % Output : Proof 0.15s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.06/0.11 % Problem : RNG106+1 : TPTP v8.1.0. Released v4.0.0. % 0.06/0.11 % Command : run_zenon %s %d % 0.11/0.30 % Computer : n032.cluster.edu % 0.11/0.30 % Model : x86_64 x86_64 % 0.11/0.30 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.11/0.30 % Memory : 8042.1875MB % 0.11/0.30 % OS : Linux 3.10.0-693.el7.x86_64 % 0.11/0.30 % CPULimit : 300 % 0.11/0.30 % WCLimit : 600 % 0.11/0.30 % DateTime : Mon May 30 11:43:42 EDT 2022 % 0.11/0.31 % CPUTime : % 0.15/0.49 (* PROOF-FOUND *) % 0.15/0.49 % SZS status Theorem % 0.15/0.49 (* BEGIN-PROOF *) % 0.15/0.49 % SZS output start Proof % 0.15/0.49 Theorem m__ : ((forall W0 : zenon_U, (forall W1 : zenon_U, (forall W2 : zenon_U, (((aElementOf0 W0 (slsdtgt0 (xc)))/\((aElementOf0 W1 (slsdtgt0 (xc)))/\(aElement0 W2)))->(exists W3 : zenon_U, ((aElement0 W3)/\(((sdtasdt0 (xc) W3) = W0)/\(exists W4 : zenon_U, ((aElement0 W4)/\(((sdtasdt0 (xc) W4) = W1)/\(((sdtpldt0 W0 W1) = (sdtasdt0 (xc) (sdtpldt0 W3 W4)))/\(((sdtasdt0 W2 W0) = (sdtasdt0 (xc) (sdtasdt0 W3 W2)))/\((aElementOf0 (sdtpldt0 W0 W1) (slsdtgt0 (xc)))/\(aElementOf0 (sdtasdt0 W2 W0) (slsdtgt0 (xc))))))))))))))))->(aIdeal0 (slsdtgt0 (xc)))). % 0.15/0.49 Proof. % 0.15/0.49 apply NNPP. intro zenon_G. % 0.15/0.49 apply (zenon_notimply_s _ _ zenon_G). zenon_intro zenon_H28. zenon_intro zenon_H27. % 0.15/0.49 generalize (mDefIdeal (slsdtgt0 (xc))). zenon_intro zenon_H29. % 0.15/0.49 apply (zenon_equiv_s _ _ zenon_H29); [ zenon_intro zenon_H27; zenon_intro zenon_H2c | zenon_intro zenon_H2b; zenon_intro zenon_H2a ]. % 0.15/0.49 apply (zenon_notand_s _ _ zenon_H2c); [ zenon_intro zenon_H2e | zenon_intro zenon_H2d ]. % 0.15/0.49 generalize (mDefPrIdeal (xc)). zenon_intro zenon_H2f. % 0.15/0.49 apply (zenon_imply_s _ _ zenon_H2f); [ zenon_intro zenon_H31 | zenon_intro zenon_H30 ]. % 0.15/0.49 exact (zenon_H31 m__1905). % 0.15/0.49 generalize (zenon_H30 (slsdtgt0 (xc))). zenon_intro zenon_H32. % 0.15/0.49 apply (zenon_equiv_s _ _ zenon_H32); [ zenon_intro zenon_H36; zenon_intro zenon_H35 | zenon_intro zenon_H34; zenon_intro zenon_H33 ]. % 0.15/0.49 apply zenon_H36. apply refl_equal. % 0.15/0.49 apply (zenon_and_s _ _ zenon_H33). zenon_intro zenon_H38. zenon_intro zenon_H37. % 0.15/0.49 exact (zenon_H2e zenon_H38). % 0.15/0.49 apply (zenon_notallex_s (fun W1 : zenon_U => ((aElementOf0 W1 (slsdtgt0 (xc)))->((forall W2 : zenon_U, ((aElementOf0 W2 (slsdtgt0 (xc)))->(aElementOf0 (sdtpldt0 W1 W2) (slsdtgt0 (xc)))))/\(forall W2 : zenon_U, ((aElement0 W2)->(aElementOf0 (sdtasdt0 W2 W1) (slsdtgt0 (xc)))))))) zenon_H2d); [ zenon_intro zenon_H39; idtac ]. % 0.15/0.49 elim zenon_H39. zenon_intro zenon_TW1_cg. zenon_intro zenon_H3b. % 0.15/0.49 apply (zenon_notimply_s _ _ zenon_H3b). zenon_intro zenon_H3d. zenon_intro zenon_H3c. % 0.15/0.49 apply (zenon_notand_s _ _ zenon_H3c); [ zenon_intro zenon_H3f | zenon_intro zenon_H3e ]. % 0.15/0.49 apply (zenon_notallex_s (fun W2 : zenon_U => ((aElementOf0 W2 (slsdtgt0 (xc)))->(aElementOf0 (sdtpldt0 zenon_TW1_cg W2) (slsdtgt0 (xc))))) zenon_H3f); [ zenon_intro zenon_H40; idtac ]. % 0.15/0.49 elim zenon_H40. zenon_intro zenon_TW2_cn. zenon_intro zenon_H42. % 0.15/0.49 apply (zenon_notimply_s _ _ zenon_H42). zenon_intro zenon_H44. zenon_intro zenon_H43. % 0.15/0.49 generalize (zenon_H28 zenon_TW1_cg). zenon_intro zenon_H45. % 0.15/0.49 generalize (zenon_H45 zenon_TW2_cn). zenon_intro zenon_H46. % 0.15/0.49 generalize (zenon_H46 (xc)). zenon_intro zenon_H47. % 0.15/0.49 apply (zenon_imply_s _ _ zenon_H47); [ zenon_intro zenon_H49 | zenon_intro zenon_H48 ]. % 0.15/0.49 apply (zenon_notand_s _ _ zenon_H49); [ zenon_intro zenon_H4b | zenon_intro zenon_H4a ]. % 0.15/0.49 exact (zenon_H4b zenon_H3d). % 0.15/0.49 apply (zenon_notand_s _ _ zenon_H4a); [ zenon_intro zenon_H4c | zenon_intro zenon_H31 ]. % 0.15/0.49 exact (zenon_H4c zenon_H44). % 0.15/0.49 exact (zenon_H31 m__1905). % 0.15/0.49 elim zenon_H48. zenon_intro zenon_TW3_cz. zenon_intro zenon_H4e. % 0.15/0.49 apply (zenon_and_s _ _ zenon_H4e). zenon_intro zenon_H50. zenon_intro zenon_H4f. % 0.15/0.49 apply (zenon_and_s _ _ zenon_H4f). zenon_intro zenon_H52. zenon_intro zenon_H51. % 0.15/0.49 elim zenon_H51. zenon_intro zenon_TW4_df. zenon_intro zenon_H54. % 0.15/0.49 apply (zenon_and_s _ _ zenon_H54). zenon_intro zenon_H56. zenon_intro zenon_H55. % 0.15/0.49 apply (zenon_and_s _ _ zenon_H55). zenon_intro zenon_H58. zenon_intro zenon_H57. % 0.15/0.49 apply (zenon_and_s _ _ zenon_H57). zenon_intro zenon_H5a. zenon_intro zenon_H59. % 0.15/0.49 apply (zenon_and_s _ _ zenon_H59). zenon_intro zenon_H5c. zenon_intro zenon_H5b. % 0.15/0.49 apply (zenon_and_s _ _ zenon_H5b). zenon_intro zenon_H5e. zenon_intro zenon_H5d. % 0.15/0.49 exact (zenon_H43 zenon_H5e). % 0.15/0.49 apply (zenon_notallex_s (fun W2 : zenon_U => ((aElement0 W2)->(aElementOf0 (sdtasdt0 W2 zenon_TW1_cg) (slsdtgt0 (xc))))) zenon_H3e); [ zenon_intro zenon_H5f; idtac ]. % 0.15/0.49 elim zenon_H5f. zenon_intro zenon_TW2_ds. zenon_intro zenon_H61. % 0.15/0.49 apply (zenon_notimply_s _ _ zenon_H61). zenon_intro zenon_H63. zenon_intro zenon_H62. % 0.15/0.49 generalize (zenon_H28 zenon_TW1_cg). zenon_intro zenon_H45. % 0.15/0.49 generalize (zenon_H45 zenon_TW1_cg). zenon_intro zenon_H64. % 0.15/0.49 generalize (zenon_H64 zenon_TW2_ds). zenon_intro zenon_H65. % 0.15/0.49 apply (zenon_imply_s _ _ zenon_H65); [ zenon_intro zenon_H67 | zenon_intro zenon_H66 ]. % 0.15/0.49 apply (zenon_notand_s _ _ zenon_H67); [ zenon_intro zenon_H4b | zenon_intro zenon_H68 ]. % 0.15/0.49 exact (zenon_H4b zenon_H3d). % 0.15/0.49 apply (zenon_notand_s _ _ zenon_H68); [ zenon_intro zenon_H4b | zenon_intro zenon_H69 ]. % 0.15/0.49 exact (zenon_H4b zenon_H3d). % 0.15/0.49 exact (zenon_H69 zenon_H63). % 0.15/0.49 elim zenon_H66. zenon_intro zenon_TW3_ec. zenon_intro zenon_H6b. % 0.15/0.49 apply (zenon_and_s _ _ zenon_H6b). zenon_intro zenon_H6d. zenon_intro zenon_H6c. % 0.15/0.49 apply (zenon_and_s _ _ zenon_H6c). zenon_intro zenon_H6f. zenon_intro zenon_H6e. % 0.15/0.49 elim zenon_H6e. zenon_intro zenon_TW4_ei. zenon_intro zenon_H71. % 0.15/0.49 apply (zenon_and_s _ _ zenon_H71). zenon_intro zenon_H73. zenon_intro zenon_H72. % 0.15/0.49 apply (zenon_and_s _ _ zenon_H72). zenon_intro zenon_H75. zenon_intro zenon_H74. % 0.15/0.49 apply (zenon_and_s _ _ zenon_H74). zenon_intro zenon_H77. zenon_intro zenon_H76. % 0.15/0.49 apply (zenon_and_s _ _ zenon_H76). zenon_intro zenon_H79. zenon_intro zenon_H78. % 0.15/0.49 apply (zenon_and_s _ _ zenon_H78). zenon_intro zenon_H7b. zenon_intro zenon_H7a. % 0.15/0.49 exact (zenon_H62 zenon_H7a). % 0.15/0.49 exact (zenon_H27 zenon_H2b). % 0.15/0.49 Qed. % 0.15/0.49 % SZS output end Proof % 0.15/0.49 (* END-PROOF *) % 0.15/0.49 nodes searched: 1286 % 0.15/0.49 max branch formulas: 519 % 0.15/0.49 proof nodes created: 82 % 0.15/0.49 formulas created: 11691 % 0.15/0.49 %------------------------------------------------------------------------------