%------------------------------------------------------------------------------ % File : Zenon---0.7.1 % Problem : SEU374+1 : TPTP v8.1.0. Released v3.3.0. % Transfm : none % Format : tptp:raw % Command : run_zenon %s %d % Computer : n017.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 : Tue Jul 19 16:01:37 EDT 2022 % Result : Theorem 0.37s 0.56s % Output : Proof 0.37s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.06/0.11 % Problem : SEU374+1 : TPTP v8.1.0. Released v3.3.0. % 0.06/0.12 % Command : run_zenon %s %d % 0.12/0.33 % Computer : n017.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 : Sat Jun 18 23:48:43 EDT 2022 % 0.12/0.33 % CPUTime : % 0.37/0.56 Zenon warning: unused variable (B : zenon_U) in reflexivity_r1_tarski % 0.37/0.56 (* PROOF-FOUND *) % 0.37/0.56 % SZS status Theorem % 0.37/0.56 (* BEGIN-PROOF *) % 0.37/0.56 % SZS output start Proof % 0.37/0.56 Theorem t20_yellow_6 : (forall A : zenon_U, ((one_sorted_str A)->(forall B : zenon_U, ((net_str B A)->(forall C : zenon_U, ((subnetstr C A B)->(forall D : zenon_U, ((element D (the_carrier B))->(forall E : zenon_U, ((element E (the_carrier B))->(forall F : zenon_U, ((element F (the_carrier C))->(forall G : zenon_U, ((element G (the_carrier C))->(((D = F)/\((E = G)/\(related C F G)))->(related B D E)))))))))))))))). % 0.37/0.56 Proof. % 0.37/0.56 assert (zenon_L1_ : forall (zenon_TG_ci : zenon_U) (zenon_TF_cj : zenon_U) (zenon_TE_ck : zenon_U) (zenon_TD_cl : zenon_U) (zenon_TC_cm : zenon_U) (zenon_TB_cn : zenon_U), (forall C : zenon_U, ((element C (the_carrier zenon_TB_cn))->(forall D : zenon_U, ((element D (the_carrier zenon_TB_cn))->(forall E : zenon_U, ((element E (the_carrier zenon_TC_cm))->(forall F : zenon_U, ((element F (the_carrier zenon_TC_cm))->(((E = C)/\((F = D)/\(related zenon_TC_cm E F)))->(related zenon_TB_cn C D)))))))))) -> (element zenon_TD_cl (the_carrier zenon_TB_cn)) -> (element zenon_TE_ck (the_carrier zenon_TB_cn)) -> (element zenon_TF_cj (the_carrier zenon_TC_cm)) -> (element zenon_TG_ci (the_carrier zenon_TC_cm)) -> (zenon_TD_cl = zenon_TF_cj) -> (zenon_TE_ck = zenon_TG_ci) -> (related zenon_TC_cm zenon_TF_cj zenon_TG_ci) -> (~(related zenon_TB_cn zenon_TD_cl zenon_TE_ck)) -> False). % 0.37/0.56 do 6 intro. intros zenon_H33 zenon_H34 zenon_H35 zenon_H36 zenon_H37 zenon_H38 zenon_H39 zenon_H3a zenon_H3b. % 0.37/0.56 generalize (zenon_H33 zenon_TD_cl). zenon_intro zenon_H42. % 0.37/0.56 apply (zenon_imply_s _ _ zenon_H42); [ zenon_intro zenon_H44 | zenon_intro zenon_H43 ]. % 0.37/0.56 exact (zenon_H44 zenon_H34). % 0.37/0.56 generalize (zenon_H43 zenon_TE_ck). zenon_intro zenon_H45. % 0.37/0.56 apply (zenon_imply_s _ _ zenon_H45); [ zenon_intro zenon_H47 | zenon_intro zenon_H46 ]. % 0.37/0.56 exact (zenon_H47 zenon_H35). % 0.37/0.56 generalize (zenon_H46 zenon_TF_cj). zenon_intro zenon_H48. % 0.37/0.56 apply (zenon_imply_s _ _ zenon_H48); [ zenon_intro zenon_H4a | zenon_intro zenon_H49 ]. % 0.37/0.56 exact (zenon_H4a zenon_H36). % 0.37/0.56 generalize (zenon_H49 zenon_TG_ci). zenon_intro zenon_H4b. % 0.37/0.56 apply (zenon_imply_s _ _ zenon_H4b); [ zenon_intro zenon_H4d | zenon_intro zenon_H4c ]. % 0.37/0.56 exact (zenon_H4d zenon_H37). % 0.37/0.56 apply (zenon_imply_s _ _ zenon_H4c); [ zenon_intro zenon_H4f | zenon_intro zenon_H4e ]. % 0.37/0.56 apply (zenon_notand_s _ _ zenon_H4f); [ zenon_intro zenon_H51 | zenon_intro zenon_H50 ]. % 0.37/0.56 apply zenon_H51. apply sym_equal. exact zenon_H38. % 0.37/0.56 apply (zenon_notand_s _ _ zenon_H50); [ zenon_intro zenon_H53 | zenon_intro zenon_H52 ]. % 0.37/0.56 apply zenon_H53. apply sym_equal. exact zenon_H39. % 0.37/0.56 exact (zenon_H52 zenon_H3a). % 0.37/0.56 exact (zenon_H3b zenon_H4e). % 0.37/0.56 (* end of lemma zenon_L1_ *) % 0.37/0.56 apply NNPP. intro zenon_G. % 0.37/0.56 apply (zenon_notallex_s (fun A : zenon_U => ((one_sorted_str A)->(forall B : zenon_U, ((net_str B A)->(forall C : zenon_U, ((subnetstr C A B)->(forall D : zenon_U, ((element D (the_carrier B))->(forall E : zenon_U, ((element E (the_carrier B))->(forall F : zenon_U, ((element F (the_carrier C))->(forall G : zenon_U, ((element G (the_carrier C))->(((D = F)/\((E = G)/\(related C F G)))->(related B D E)))))))))))))))) zenon_G); [ zenon_intro zenon_H54; idtac ]. % 0.37/0.56 elim zenon_H54. zenon_intro zenon_TA_dh. zenon_intro zenon_H56. % 0.37/0.56 apply (zenon_notimply_s _ _ zenon_H56). zenon_intro zenon_H58. zenon_intro zenon_H57. % 0.37/0.56 apply (zenon_notallex_s (fun B : zenon_U => ((net_str B zenon_TA_dh)->(forall C : zenon_U, ((subnetstr C zenon_TA_dh B)->(forall D : zenon_U, ((element D (the_carrier B))->(forall E : zenon_U, ((element E (the_carrier B))->(forall F : zenon_U, ((element F (the_carrier C))->(forall G : zenon_U, ((element G (the_carrier C))->(((D = F)/\((E = G)/\(related C F G)))->(related B D E)))))))))))))) zenon_H57); [ zenon_intro zenon_H59; idtac ]. % 0.37/0.56 elim zenon_H59. zenon_intro zenon_TB_cn. zenon_intro zenon_H5a. % 0.37/0.56 apply (zenon_notimply_s _ _ zenon_H5a). zenon_intro zenon_H5c. zenon_intro zenon_H5b. % 0.37/0.56 apply (zenon_notallex_s (fun C : zenon_U => ((subnetstr C zenon_TA_dh zenon_TB_cn)->(forall D : zenon_U, ((element D (the_carrier zenon_TB_cn))->(forall E : zenon_U, ((element E (the_carrier zenon_TB_cn))->(forall F : zenon_U, ((element F (the_carrier C))->(forall G : zenon_U, ((element G (the_carrier C))->(((D = F)/\((E = G)/\(related C F G)))->(related zenon_TB_cn D E)))))))))))) zenon_H5b); [ zenon_intro zenon_H5d; idtac ]. % 0.37/0.56 elim zenon_H5d. zenon_intro zenon_TC_cm. zenon_intro zenon_H5e. % 0.37/0.56 apply (zenon_notimply_s _ _ zenon_H5e). zenon_intro zenon_H60. zenon_intro zenon_H5f. % 0.37/0.56 apply (zenon_notallex_s (fun D : zenon_U => ((element D (the_carrier zenon_TB_cn))->(forall E : zenon_U, ((element E (the_carrier zenon_TB_cn))->(forall F : zenon_U, ((element F (the_carrier zenon_TC_cm))->(forall G : zenon_U, ((element G (the_carrier zenon_TC_cm))->(((D = F)/\((E = G)/\(related zenon_TC_cm F G)))->(related zenon_TB_cn D E)))))))))) zenon_H5f); [ zenon_intro zenon_H61; idtac ]. % 0.37/0.56 elim zenon_H61. zenon_intro zenon_TD_cl. zenon_intro zenon_H62. % 0.37/0.56 apply (zenon_notimply_s _ _ zenon_H62). zenon_intro zenon_H34. zenon_intro zenon_H63. % 0.37/0.56 apply (zenon_notallex_s (fun E : zenon_U => ((element E (the_carrier zenon_TB_cn))->(forall F : zenon_U, ((element F (the_carrier zenon_TC_cm))->(forall G : zenon_U, ((element G (the_carrier zenon_TC_cm))->(((zenon_TD_cl = F)/\((E = G)/\(related zenon_TC_cm F G)))->(related zenon_TB_cn zenon_TD_cl E)))))))) zenon_H63); [ zenon_intro zenon_H64; idtac ]. % 0.37/0.56 elim zenon_H64. zenon_intro zenon_TE_ck. zenon_intro zenon_H65. % 0.37/0.56 apply (zenon_notimply_s _ _ zenon_H65). zenon_intro zenon_H35. zenon_intro zenon_H66. % 0.37/0.56 apply (zenon_notallex_s (fun F : zenon_U => ((element F (the_carrier zenon_TC_cm))->(forall G : zenon_U, ((element G (the_carrier zenon_TC_cm))->(((zenon_TD_cl = F)/\((zenon_TE_ck = G)/\(related zenon_TC_cm F G)))->(related zenon_TB_cn zenon_TD_cl zenon_TE_ck)))))) zenon_H66); [ zenon_intro zenon_H67; idtac ]. % 0.37/0.56 elim zenon_H67. zenon_intro zenon_TF_cj. zenon_intro zenon_H68. % 0.37/0.56 apply (zenon_notimply_s _ _ zenon_H68). zenon_intro zenon_H36. zenon_intro zenon_H69. % 0.37/0.56 apply (zenon_notallex_s (fun G : zenon_U => ((element G (the_carrier zenon_TC_cm))->(((zenon_TD_cl = zenon_TF_cj)/\((zenon_TE_ck = G)/\(related zenon_TC_cm zenon_TF_cj G)))->(related zenon_TB_cn zenon_TD_cl zenon_TE_ck)))) zenon_H69); [ zenon_intro zenon_H6a; idtac ]. % 0.37/0.56 elim zenon_H6a. zenon_intro zenon_TG_ci. zenon_intro zenon_H6b. % 0.37/0.56 apply (zenon_notimply_s _ _ zenon_H6b). zenon_intro zenon_H37. zenon_intro zenon_H6c. % 0.37/0.56 apply (zenon_notimply_s _ _ zenon_H6c). zenon_intro zenon_H6d. zenon_intro zenon_H3b. % 0.37/0.56 apply (zenon_and_s _ _ zenon_H6d). zenon_intro zenon_H38. zenon_intro zenon_H6e. % 0.37/0.56 apply (zenon_and_s _ _ zenon_H6e). zenon_intro zenon_H39. zenon_intro zenon_H3a. % 0.37/0.56 generalize (t60_yellow_0 zenon_TB_cn). zenon_intro zenon_H6f. % 0.37/0.56 apply (zenon_imply_s _ _ zenon_H6f); [ zenon_intro zenon_H71 | zenon_intro zenon_H70 ]. % 0.37/0.56 generalize (dt_l1_waybel_0 zenon_TA_dh). zenon_intro zenon_H72. % 0.37/0.56 apply (zenon_imply_s _ _ zenon_H72); [ zenon_intro zenon_H74 | zenon_intro zenon_H73 ]. % 0.37/0.56 exact (zenon_H74 zenon_H58). % 0.37/0.56 generalize (zenon_H73 zenon_TB_cn). zenon_intro zenon_H75. % 0.37/0.56 apply (zenon_imply_s _ _ zenon_H75); [ zenon_intro zenon_H77 | zenon_intro zenon_H76 ]. % 0.37/0.56 exact (zenon_H77 zenon_H5c). % 0.37/0.56 exact (zenon_H71 zenon_H76). % 0.37/0.56 generalize (dt_m1_yellow_6 zenon_TA_dh). zenon_intro zenon_H78. % 0.37/0.56 generalize (d8_yellow_6 zenon_TA_dh). zenon_intro zenon_H79. % 0.37/0.56 apply (zenon_imply_s _ _ zenon_H79); [ zenon_intro zenon_H74 | zenon_intro zenon_H7a ]. % 0.37/0.56 exact (zenon_H74 zenon_H58). % 0.37/0.56 generalize (zenon_H70 zenon_TC_cm). zenon_intro zenon_H7b. % 0.37/0.56 apply (zenon_imply_s _ _ zenon_H7b); [ zenon_intro zenon_H7c | zenon_intro zenon_H33 ]. % 0.37/0.56 generalize (zenon_H7a zenon_TB_cn). zenon_intro zenon_H7d. % 0.37/0.56 apply (zenon_imply_s _ _ zenon_H7d); [ zenon_intro zenon_H77 | zenon_intro zenon_H7e ]. % 0.37/0.56 exact (zenon_H77 zenon_H5c). % 0.37/0.56 generalize (zenon_H7e zenon_TC_cm). zenon_intro zenon_H7f. % 0.37/0.56 apply (zenon_imply_s _ _ zenon_H7f); [ zenon_intro zenon_H81 | zenon_intro zenon_H80 ]. % 0.37/0.56 generalize (zenon_H78 zenon_TB_cn). zenon_intro zenon_H82. % 0.37/0.56 apply (zenon_imply_s _ _ zenon_H82); [ zenon_intro zenon_H84 | zenon_intro zenon_H83 ]. % 0.37/0.56 apply (zenon_notand_s _ _ zenon_H84); [ zenon_intro zenon_H74 | zenon_intro zenon_H77 ]. % 0.37/0.56 exact (zenon_H74 zenon_H58). % 0.37/0.56 exact (zenon_H77 zenon_H5c). % 0.37/0.56 generalize (zenon_H83 zenon_TC_cm). zenon_intro zenon_H85. % 0.37/0.56 apply (zenon_imply_s _ _ zenon_H85); [ zenon_intro zenon_H87 | zenon_intro zenon_H86 ]. % 0.37/0.56 exact (zenon_H87 zenon_H60). % 0.37/0.56 exact (zenon_H81 zenon_H86). % 0.37/0.56 apply (zenon_equiv_s _ _ zenon_H80); [ zenon_intro zenon_H87; zenon_intro zenon_H89 | zenon_intro zenon_H60; zenon_intro zenon_H88 ]. % 0.37/0.56 exact (zenon_H87 zenon_H60). % 0.37/0.56 apply (zenon_and_s _ _ zenon_H88). zenon_intro zenon_H8b. zenon_intro zenon_H8a. % 0.37/0.56 exact (zenon_H7c zenon_H8b). % 0.37/0.56 apply (zenon_L1_ zenon_TG_ci zenon_TF_cj zenon_TE_ck zenon_TD_cl zenon_TC_cm zenon_TB_cn); trivial. % 0.37/0.56 Qed. % 0.37/0.56 % SZS output end Proof % 0.37/0.56 (* END-PROOF *) % 0.37/0.56 nodes searched: 1624 % 0.37/0.56 max branch formulas: 664 % 0.37/0.56 proof nodes created: 205 % 0.37/0.56 formulas created: 6874 % 0.37/0.56 %------------------------------------------------------------------------------