%------------------------------------------------------------------------------ % File : Zenon---0.7.1 % Problem : KRS103+1 : TPTP v8.1.0. Released v3.1.0. % Transfm : none % Format : tptp:raw % Command : run_zenon %s %d % Computer : n024.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 : Sun Jul 17 03:39:27 EDT 2022 % Result : Unsatisfiable 0.50s 0.69s % Output : Proof 0.50s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.12 % Problem : KRS103+1 : TPTP v8.1.0. Released v3.1.0. % 0.03/0.12 % Command : run_zenon %s %d % 0.12/0.34 % Computer : n024.cluster.edu % 0.12/0.34 % Model : x86_64 x86_64 % 0.12/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.34 % Memory : 8042.1875MB % 0.12/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.34 % CPULimit : 300 % 0.12/0.34 % WCLimit : 600 % 0.12/0.34 % DateTime : Tue Jun 7 16:49:49 EDT 2022 % 0.12/0.34 % CPUTime : % 0.50/0.69 (* PROOF-FOUND *) % 0.50/0.69 % SZS status Unsatisfiable % 0.50/0.69 (* BEGIN-PROOF *) % 0.50/0.69 % SZS output start Proof % 0.50/0.69 Theorem zenon_thm : False. % 0.50/0.69 Proof. % 0.50/0.69 assert (zenon_L1_ : (~(cminus8 (i2003_11_14_17_20_46476))) -> (~(cplus9 (i2003_11_14_17_20_46476))) -> (cminus3 (i2003_11_14_17_20_46476)) -> False). % 0.50/0.69 do 0 intro. intros zenon_H39 zenon_H3a zenon_H3b. % 0.50/0.69 generalize (axiom_52 (i2003_11_14_17_20_46476)). zenon_intro zenon_H3c. % 0.50/0.69 apply (zenon_notand_s _ _ zenon_H3c); [ zenon_intro zenon_H3e | zenon_intro zenon_H3d ]. % 0.50/0.69 generalize (axiom_32 (i2003_11_14_17_20_46476)). zenon_intro zenon_H3f. % 0.50/0.69 apply (zenon_imply_s _ _ zenon_H3f); [ zenon_intro zenon_H41 | zenon_intro zenon_H40 ]. % 0.50/0.69 exact (zenon_H41 axiom_47). % 0.50/0.69 apply (zenon_or_s _ _ zenon_H40); [ zenon_intro zenon_H43 | zenon_intro zenon_H42 ]. % 0.50/0.69 exact (zenon_H3e zenon_H43). % 0.50/0.69 apply (zenon_or_s _ _ zenon_H42); [ zenon_intro zenon_H45 | zenon_intro zenon_H44 ]. % 0.50/0.69 exact (zenon_H39 zenon_H45). % 0.50/0.69 exact (zenon_H3a zenon_H44). % 0.50/0.69 exact (zenon_H3d zenon_H3b). % 0.50/0.69 (* end of lemma zenon_L1_ *) % 0.50/0.69 assert (zenon_L2_ : (cminus9 (i2003_11_14_17_20_46476)) -> (~(cminus8 (i2003_11_14_17_20_46476))) -> (cminus3 (i2003_11_14_17_20_46476)) -> False). % 0.50/0.70 do 0 intro. intros zenon_H46 zenon_H39 zenon_H3b. % 0.50/0.70 generalize (axiom_49 (i2003_11_14_17_20_46476)). zenon_intro zenon_H47. % 0.50/0.70 apply (zenon_notand_s _ _ zenon_H47); [ zenon_intro zenon_H48 | zenon_intro zenon_H3a ]. % 0.50/0.70 exact (zenon_H48 zenon_H46). % 0.50/0.70 apply (zenon_L1_); trivial. % 0.50/0.70 (* end of lemma zenon_L2_ *) % 0.50/0.70 assert (zenon_L3_ : (~((cplus4 (i2003_11_14_17_20_46476))/\(cminus4 (i2003_11_14_17_20_46476)))) -> (cminus4 (i2003_11_14_17_20_46476)) -> (cminus3 (i2003_11_14_17_20_46476)) -> (~(cminus9 (i2003_11_14_17_20_46476))) -> False). % 0.50/0.70 do 0 intro. intros zenon_H49 zenon_H4a zenon_H3b zenon_H48. % 0.50/0.70 apply (zenon_notand_s _ _ zenon_H49); [ zenon_intro zenon_H4c | zenon_intro zenon_H4b ]. % 0.50/0.70 generalize (axiom_52 (i2003_11_14_17_20_46476)). zenon_intro zenon_H3c. % 0.50/0.70 apply (zenon_notand_s _ _ zenon_H3c); [ zenon_intro zenon_H3e | zenon_intro zenon_H3d ]. % 0.50/0.70 generalize (axiom_28 (i2003_11_14_17_20_46476)). zenon_intro zenon_H4d. % 0.50/0.70 apply (zenon_imply_s _ _ zenon_H4d); [ zenon_intro zenon_H41 | zenon_intro zenon_H4e ]. % 0.50/0.70 exact (zenon_H41 axiom_47). % 0.50/0.70 apply (zenon_or_s _ _ zenon_H4e); [ zenon_intro zenon_H46 | zenon_intro zenon_H4f ]. % 0.50/0.70 exact (zenon_H48 zenon_H46). % 0.50/0.70 apply (zenon_or_s _ _ zenon_H4f); [ zenon_intro zenon_H43 | zenon_intro zenon_H50 ]. % 0.50/0.70 exact (zenon_H3e zenon_H43). % 0.50/0.70 exact (zenon_H4c zenon_H50). % 0.50/0.70 exact (zenon_H3d zenon_H3b). % 0.50/0.70 exact (zenon_H4b zenon_H4a). % 0.50/0.70 (* end of lemma zenon_L3_ *) % 0.50/0.70 assert (zenon_L4_ : (~(cminus9 (i2003_11_14_17_20_46476))) -> (cminus3 (i2003_11_14_17_20_46476)) -> (cminus4 (i2003_11_14_17_20_46476)) -> False). % 0.50/0.70 do 0 intro. intros zenon_H48 zenon_H3b zenon_H4a. % 0.50/0.70 generalize (axiom_50 (i2003_11_14_17_20_46476)). zenon_intro zenon_H49. % 0.50/0.70 apply (zenon_L3_); trivial. % 0.50/0.70 (* end of lemma zenon_L4_ *) % 0.50/0.70 assert (zenon_L5_ : (~(cminus8 (i2003_11_14_17_20_46476))) -> (cminus3 (i2003_11_14_17_20_46476)) -> False). % 0.50/0.70 do 0 intro. intros zenon_H39 zenon_H3b. % 0.50/0.70 generalize (axiom_9 (i2003_11_14_17_20_46476)). zenon_intro zenon_H51. % 0.50/0.70 apply (zenon_imply_s _ _ zenon_H51); [ zenon_intro zenon_H41 | zenon_intro zenon_H52 ]. % 0.50/0.70 exact (zenon_H41 axiom_47). % 0.50/0.70 apply (zenon_or_s _ _ zenon_H52); [ zenon_intro zenon_H46 | zenon_intro zenon_H53 ]. % 0.50/0.70 apply (zenon_L2_); trivial. % 0.50/0.70 apply (zenon_or_s _ _ zenon_H53); [ zenon_intro zenon_H4a | zenon_intro zenon_H45 ]. % 0.50/0.70 generalize (axiom_49 (i2003_11_14_17_20_46476)). zenon_intro zenon_H47. % 0.50/0.70 apply (zenon_notand_s _ _ zenon_H47); [ zenon_intro zenon_H48 | zenon_intro zenon_H3a ]. % 0.50/0.70 apply (zenon_L4_); trivial. % 0.50/0.70 apply (zenon_L1_); trivial. % 0.50/0.70 exact (zenon_H39 zenon_H45). % 0.50/0.70 (* end of lemma zenon_L5_ *) % 0.50/0.70 assert (zenon_L6_ : (cplus5 (i2003_11_14_17_20_46476)) -> (cminus5 (i2003_11_14_17_20_46476)) -> False). % 0.50/0.70 do 0 intro. intros zenon_H54 zenon_H55. % 0.50/0.70 generalize (axiom_53 (i2003_11_14_17_20_46476)). zenon_intro zenon_H56. % 0.50/0.70 apply (zenon_notand_s _ _ zenon_H56); [ zenon_intro zenon_H58 | zenon_intro zenon_H57 ]. % 0.50/0.70 exact (zenon_H58 zenon_H54). % 0.50/0.70 exact (zenon_H57 zenon_H55). % 0.50/0.70 (* end of lemma zenon_L6_ *) % 0.50/0.70 assert (zenon_L7_ : (~(cminus8 (i2003_11_14_17_20_46476))) -> (cminus5 (i2003_11_14_17_20_46476)) -> False). % 0.50/0.70 do 0 intro. intros zenon_H39 zenon_H55. % 0.50/0.70 generalize (axiom_15 (i2003_11_14_17_20_46476)). zenon_intro zenon_H59. % 0.50/0.70 apply (zenon_imply_s _ _ zenon_H59); [ zenon_intro zenon_H41 | zenon_intro zenon_H5a ]. % 0.50/0.70 exact (zenon_H41 axiom_47). % 0.50/0.70 apply (zenon_or_s _ _ zenon_H5a); [ zenon_intro zenon_H3b | zenon_intro zenon_H5b ]. % 0.50/0.70 apply (zenon_L5_); trivial. % 0.50/0.70 apply (zenon_or_s _ _ zenon_H5b); [ zenon_intro zenon_H54 | zenon_intro zenon_H45 ]. % 0.50/0.70 apply (zenon_L6_); trivial. % 0.50/0.70 exact (zenon_H39 zenon_H45). % 0.50/0.70 (* end of lemma zenon_L7_ *) % 0.50/0.70 assert (zenon_L8_ : (~(cminus8 (i2003_11_14_17_20_46476))) -> False). % 0.50/0.70 do 0 intro. intros zenon_H39. % 0.50/0.70 generalize (axiom_3 (i2003_11_14_17_20_46476)). zenon_intro zenon_H5c. % 0.50/0.70 apply (zenon_imply_s _ _ zenon_H5c); [ zenon_intro zenon_H41 | zenon_intro zenon_H5d ]. % 0.50/0.70 exact (zenon_H41 axiom_47). % 0.50/0.70 apply (zenon_or_s _ _ zenon_H5d); [ zenon_intro zenon_H3b | zenon_intro zenon_H5e ]. % 0.50/0.70 apply (zenon_L5_); trivial. % 0.50/0.70 apply (zenon_or_s _ _ zenon_H5e); [ zenon_intro zenon_H55 | zenon_intro zenon_H45 ]. % 0.50/0.70 apply (zenon_L7_); trivial. % 0.50/0.70 exact (zenon_H39 zenon_H45). % 0.50/0.70 (* end of lemma zenon_L8_ *) % 0.50/0.70 assert (zenon_L9_ : (cminus2 (i2003_11_14_17_20_46476)) -> (cplus2 (i2003_11_14_17_20_46476)) -> False). % 0.50/0.70 do 0 intro. intros zenon_H5f zenon_H60. % 0.50/0.70 generalize (axiom_54 (i2003_11_14_17_20_46476)). zenon_intro zenon_H61. % 0.50/0.70 apply (zenon_notand_s _ _ zenon_H61); [ zenon_intro zenon_H63 | zenon_intro zenon_H62 ]. % 0.50/0.70 exact (zenon_H63 zenon_H5f). % 0.50/0.70 exact (zenon_H62 zenon_H60). % 0.50/0.70 (* end of lemma zenon_L9_ *) % 0.50/0.70 assert (zenon_L10_ : (~(cminus9 (i2003_11_14_17_20_46476))) -> (cminus3 (i2003_11_14_17_20_46476)) -> False). % 0.50/0.70 do 0 intro. intros zenon_H48 zenon_H3b. % 0.50/0.70 generalize (axiom_52 (i2003_11_14_17_20_46476)). zenon_intro zenon_H3c. % 0.50/0.70 apply (zenon_notand_s _ _ zenon_H3c); [ zenon_intro zenon_H3e | zenon_intro zenon_H3d ]. % 0.50/0.70 generalize (axiom_35 (i2003_11_14_17_20_46476)). zenon_intro zenon_H64. % 0.50/0.70 apply (zenon_imply_s _ _ zenon_H64); [ zenon_intro zenon_H41 | zenon_intro zenon_H65 ]. % 0.50/0.70 exact (zenon_H41 axiom_47). % 0.50/0.70 apply (zenon_or_s _ _ zenon_H65); [ zenon_intro zenon_H46 | zenon_intro zenon_H66 ]. % 0.50/0.70 exact (zenon_H48 zenon_H46). % 0.50/0.70 apply (zenon_or_s _ _ zenon_H66); [ zenon_intro zenon_H5f | zenon_intro zenon_H43 ]. % 0.50/0.70 generalize (axiom_48 (i2003_11_14_17_20_46476)). zenon_intro zenon_H67. % 0.50/0.70 apply (zenon_notand_s _ _ zenon_H67); [ zenon_intro zenon_H39 | zenon_intro zenon_H68 ]. % 0.50/0.70 apply (zenon_L8_); trivial. % 0.50/0.70 generalize (axiom_45 (i2003_11_14_17_20_46476)). zenon_intro zenon_H69. % 0.50/0.70 apply (zenon_imply_s _ _ zenon_H69); [ zenon_intro zenon_H41 | zenon_intro zenon_H6a ]. % 0.50/0.70 exact (zenon_H41 axiom_47). % 0.50/0.70 apply (zenon_or_s _ _ zenon_H6a); [ zenon_intro zenon_H4a | zenon_intro zenon_H6b ]. % 0.50/0.70 apply (zenon_L4_); trivial. % 0.50/0.70 apply (zenon_or_s _ _ zenon_H6b); [ zenon_intro zenon_H60 | zenon_intro zenon_H6c ]. % 0.50/0.70 apply (zenon_L9_); trivial. % 0.50/0.70 exact (zenon_H68 zenon_H6c). % 0.50/0.70 exact (zenon_H3e zenon_H43). % 0.50/0.70 exact (zenon_H3d zenon_H3b). % 0.50/0.70 (* end of lemma zenon_L10_ *) % 0.50/0.70 assert (zenon_L11_ : (cplus8 (i2003_11_14_17_20_46476)) -> False). % 0.50/0.70 do 0 intro. intros zenon_H6c. % 0.50/0.70 generalize (axiom_48 (i2003_11_14_17_20_46476)). zenon_intro zenon_H67. % 0.50/0.70 apply (zenon_notand_s _ _ zenon_H67); [ zenon_intro zenon_H39 | zenon_intro zenon_H68 ]. % 0.50/0.70 apply (zenon_L8_); trivial. % 0.50/0.70 exact (zenon_H68 zenon_H6c). % 0.50/0.70 (* end of lemma zenon_L11_ *) % 0.50/0.70 assert (zenon_L12_ : (~(cplus2 (i2003_11_14_17_20_46476))) -> (cminus5 (i2003_11_14_17_20_46476)) -> (~(cplus9 (i2003_11_14_17_20_46476))) -> False). % 0.50/0.70 do 0 intro. intros zenon_H62 zenon_H55 zenon_H3a. % 0.50/0.70 generalize (axiom_13 (i2003_11_14_17_20_46476)). zenon_intro zenon_H6d. % 0.50/0.70 apply (zenon_imply_s _ _ zenon_H6d); [ zenon_intro zenon_H41 | zenon_intro zenon_H6e ]. % 0.50/0.70 exact (zenon_H41 axiom_47). % 0.50/0.70 apply (zenon_or_s _ _ zenon_H6e); [ zenon_intro zenon_H60 | zenon_intro zenon_H6f ]. % 0.50/0.70 exact (zenon_H62 zenon_H60). % 0.50/0.70 apply (zenon_or_s _ _ zenon_H6f); [ zenon_intro zenon_H54 | zenon_intro zenon_H44 ]. % 0.50/0.70 apply (zenon_L6_); trivial. % 0.50/0.70 exact (zenon_H3a zenon_H44). % 0.50/0.70 (* end of lemma zenon_L12_ *) % 0.50/0.70 assert (zenon_L13_ : (cminus3 (i2003_11_14_17_20_46476)) -> (cminus4 (i2003_11_14_17_20_46476)) -> (~(cplus2 (i2003_11_14_17_20_46476))) -> (cminus5 (i2003_11_14_17_20_46476)) -> False). % 0.50/0.70 do 0 intro. intros zenon_H3b zenon_H4a zenon_H62 zenon_H55. % 0.50/0.70 generalize (axiom_49 (i2003_11_14_17_20_46476)). zenon_intro zenon_H47. % 0.50/0.70 apply (zenon_notand_s _ _ zenon_H47); [ zenon_intro zenon_H48 | zenon_intro zenon_H3a ]. % 0.50/0.70 apply (zenon_L4_); trivial. % 0.50/0.70 apply (zenon_L12_); trivial. % 0.50/0.70 (* end of lemma zenon_L13_ *) % 0.50/0.70 assert (zenon_L14_ : (cplus4 (i2003_11_14_17_20_46476)) -> (cminus4 (i2003_11_14_17_20_46476)) -> False). % 0.50/0.70 do 0 intro. intros zenon_H50 zenon_H4a. % 0.50/0.70 generalize (axiom_50 (i2003_11_14_17_20_46476)). zenon_intro zenon_H49. % 0.50/0.70 apply (zenon_notand_s _ _ zenon_H49); [ zenon_intro zenon_H4c | zenon_intro zenon_H4b ]. % 0.50/0.70 exact (zenon_H4c zenon_H50). % 0.50/0.70 exact (zenon_H4b zenon_H4a). % 0.50/0.70 (* end of lemma zenon_L14_ *) % 0.50/0.70 assert (zenon_L15_ : (cminus3 (i2003_11_14_17_20_46476)) -> (cplus9 (i2003_11_14_17_20_46476)) -> False). % 0.50/0.70 do 0 intro. intros zenon_H3b zenon_H44. % 0.50/0.70 generalize (axiom_49 (i2003_11_14_17_20_46476)). zenon_intro zenon_H47. % 0.50/0.70 apply (zenon_notand_s _ _ zenon_H47); [ zenon_intro zenon_H48 | zenon_intro zenon_H3a ]. % 0.50/0.70 apply (zenon_L10_); trivial. % 0.50/0.70 exact (zenon_H3a zenon_H44). % 0.50/0.70 (* end of lemma zenon_L15_ *) % 0.50/0.70 assert (zenon_L16_ : (cplus3 (i2003_11_14_17_20_46476)) -> (cminus3 (i2003_11_14_17_20_46476)) -> False). % 0.50/0.70 do 0 intro. intros zenon_H43 zenon_H3b. % 0.50/0.70 generalize (axiom_52 (i2003_11_14_17_20_46476)). zenon_intro zenon_H3c. % 0.50/0.70 apply (zenon_notand_s _ _ zenon_H3c); [ zenon_intro zenon_H3e | zenon_intro zenon_H3d ]. % 0.50/0.70 exact (zenon_H3e zenon_H43). % 0.50/0.70 exact (zenon_H3d zenon_H3b). % 0.50/0.70 (* end of lemma zenon_L16_ *) % 0.50/0.70 assert (zenon_L17_ : (cplus4 (i2003_11_14_17_20_46476)) -> (cplus7 (i2003_11_14_17_20_46476)) -> False). % 0.50/0.70 do 0 intro. intros zenon_H50 zenon_H70. % 0.50/0.70 generalize (axiom_51 (i2003_11_14_17_20_46476)). zenon_intro zenon_H71. % 0.50/0.70 apply (zenon_notand_s _ _ zenon_H71); [ zenon_intro zenon_H73 | zenon_intro zenon_H72 ]. % 0.50/0.70 generalize (axiom_29 (i2003_11_14_17_20_46476)). zenon_intro zenon_H74. % 0.50/0.70 apply (zenon_imply_s _ _ zenon_H74); [ zenon_intro zenon_H41 | zenon_intro zenon_H75 ]. % 0.50/0.70 exact (zenon_H41 axiom_47). % 0.50/0.70 apply (zenon_or_s _ _ zenon_H75); [ zenon_intro zenon_H4a | zenon_intro zenon_H76 ]. % 0.50/0.70 apply (zenon_L14_); trivial. % 0.50/0.70 apply (zenon_or_s _ _ zenon_H76); [ zenon_intro zenon_H3b | zenon_intro zenon_H77 ]. % 0.50/0.70 generalize (axiom_6 (i2003_11_14_17_20_46476)). zenon_intro zenon_H78. % 0.50/0.70 apply (zenon_imply_s _ _ zenon_H78); [ zenon_intro zenon_H41 | zenon_intro zenon_H79 ]. % 0.50/0.70 exact (zenon_H41 axiom_47). % 0.50/0.70 apply (zenon_or_s _ _ zenon_H79); [ zenon_intro zenon_H43 | zenon_intro zenon_H7a ]. % 0.50/0.70 apply (zenon_L16_); trivial. % 0.50/0.70 apply (zenon_or_s _ _ zenon_H7a); [ zenon_intro zenon_H77 | zenon_intro zenon_H6c ]. % 0.50/0.70 exact (zenon_H73 zenon_H77). % 0.50/0.70 apply (zenon_L11_); trivial. % 0.50/0.70 exact (zenon_H73 zenon_H77). % 0.50/0.70 exact (zenon_H72 zenon_H70). % 0.50/0.70 (* end of lemma zenon_L17_ *) % 0.50/0.70 assert (zenon_L18_ : (cplus9 (i2003_11_14_17_20_46476)) -> (cplus4 (i2003_11_14_17_20_46476)) -> False). % 0.50/0.70 do 0 intro. intros zenon_H44 zenon_H50. % 0.50/0.70 generalize (axiom_4 (i2003_11_14_17_20_46476)). zenon_intro zenon_H7b. % 0.50/0.70 apply (zenon_imply_s _ _ zenon_H7b); [ zenon_intro zenon_H41 | zenon_intro zenon_H7c ]. % 0.50/0.70 exact (zenon_H41 axiom_47). % 0.50/0.70 apply (zenon_or_s _ _ zenon_H7c); [ zenon_intro zenon_H3b | zenon_intro zenon_H7d ]. % 0.50/0.70 apply (zenon_L15_); trivial. % 0.50/0.70 apply (zenon_or_s _ _ zenon_H7d); [ zenon_intro zenon_H70 | zenon_intro zenon_H6c ]. % 0.50/0.70 apply (zenon_L17_); trivial. % 0.50/0.70 apply (zenon_L11_); trivial. % 0.50/0.70 (* end of lemma zenon_L18_ *) % 0.50/0.70 assert (zenon_L19_ : (cplus4 (i2003_11_14_17_20_46476)) -> False). % 0.50/0.70 do 0 intro. intros zenon_H50. % 0.50/0.70 generalize (axiom_34 (i2003_11_14_17_20_46476)). zenon_intro zenon_H7e. % 0.50/0.70 apply (zenon_imply_s _ _ zenon_H7e); [ zenon_intro zenon_H41 | zenon_intro zenon_H7f ]. % 0.50/0.70 exact (zenon_H41 axiom_47). % 0.50/0.70 apply (zenon_or_s _ _ zenon_H7f); [ zenon_intro zenon_H4a | zenon_intro zenon_H80 ]. % 0.50/0.70 apply (zenon_L14_); trivial. % 0.50/0.70 apply (zenon_or_s _ _ zenon_H80); [ zenon_intro zenon_H44 | zenon_intro zenon_H70 ]. % 0.50/0.70 apply (zenon_L18_); trivial. % 0.50/0.70 apply (zenon_L17_); trivial. % 0.50/0.70 (* end of lemma zenon_L19_ *) % 0.50/0.70 assert (zenon_L20_ : (~(cminus1 (i2003_11_14_17_20_46476))) -> (cminus2 (i2003_11_14_17_20_46476)) -> False). % 0.50/0.70 do 0 intro. intros zenon_H81 zenon_H5f. % 0.50/0.70 generalize (axiom_36 (i2003_11_14_17_20_46476)). zenon_intro zenon_H82. % 0.50/0.70 apply (zenon_imply_s _ _ zenon_H82); [ zenon_intro zenon_H41 | zenon_intro zenon_H83 ]. % 0.50/0.70 exact (zenon_H41 axiom_47). % 0.50/0.70 apply (zenon_or_s _ _ zenon_H83); [ zenon_intro zenon_H85 | zenon_intro zenon_H84 ]. % 0.50/0.70 exact (zenon_H81 zenon_H85). % 0.50/0.70 apply (zenon_or_s _ _ zenon_H84); [ zenon_intro zenon_H50 | zenon_intro zenon_H60 ]. % 0.50/0.70 apply (zenon_L19_); trivial. % 0.50/0.70 apply (zenon_L9_); trivial. % 0.50/0.70 (* end of lemma zenon_L20_ *) % 0.50/0.70 assert (zenon_L21_ : (cminus2 (i2003_11_14_17_20_46476)) -> (cplus1 (i2003_11_14_17_20_46476)) -> False). % 0.50/0.70 do 0 intro. intros zenon_H5f zenon_H86. % 0.50/0.70 generalize (axiom_55 (i2003_11_14_17_20_46476)). zenon_intro zenon_H87. % 0.50/0.70 apply (zenon_notand_s _ _ zenon_H87); [ zenon_intro zenon_H81 | zenon_intro zenon_H88 ]. % 0.50/0.70 apply (zenon_L20_); trivial. % 0.50/0.70 exact (zenon_H88 zenon_H86). % 0.50/0.70 (* end of lemma zenon_L21_ *) % 0.50/0.70 assert (zenon_L22_ : (cplus6 (i2003_11_14_17_20_46476)) -> (cminus6 (i2003_11_14_17_20_46476)) -> False). % 0.50/0.70 do 0 intro. intros zenon_H89 zenon_H8a. % 0.50/0.70 generalize (axiom_56 (i2003_11_14_17_20_46476)). zenon_intro zenon_H8b. % 0.50/0.70 apply (zenon_notand_s _ _ zenon_H8b); [ zenon_intro zenon_H8d | zenon_intro zenon_H8c ]. % 0.50/0.70 exact (zenon_H8d zenon_H89). % 0.50/0.70 exact (zenon_H8c zenon_H8a). % 0.50/0.70 (* end of lemma zenon_L22_ *) % 0.50/0.70 assert (zenon_L23_ : (cplus1 (i2003_11_14_17_20_46476)) -> (cplus6 (i2003_11_14_17_20_46476)) -> False). % 0.50/0.70 do 0 intro. intros zenon_H86 zenon_H89. % 0.50/0.70 generalize (axiom_21 (i2003_11_14_17_20_46476)). zenon_intro zenon_H8e. % 0.50/0.70 apply (zenon_imply_s _ _ zenon_H8e); [ zenon_intro zenon_H41 | zenon_intro zenon_H8f ]. % 0.50/0.70 exact (zenon_H41 axiom_47). % 0.50/0.70 apply (zenon_or_s _ _ zenon_H8f); [ zenon_intro zenon_H5f | zenon_intro zenon_H90 ]. % 0.50/0.70 apply (zenon_L21_); trivial. % 0.50/0.70 apply (zenon_or_s _ _ zenon_H90); [ zenon_intro zenon_H50 | zenon_intro zenon_H8a ]. % 0.50/0.70 apply (zenon_L19_); trivial. % 0.50/0.70 apply (zenon_L22_); trivial. % 0.50/0.70 (* end of lemma zenon_L23_ *) % 0.50/0.70 assert (zenon_L24_ : (cplus9 (i2003_11_14_17_20_46476)) -> (cminus2 (i2003_11_14_17_20_46476)) -> False). % 0.50/0.70 do 0 intro. intros zenon_H44 zenon_H5f. % 0.50/0.70 generalize (axiom_48 (i2003_11_14_17_20_46476)). zenon_intro zenon_H67. % 0.50/0.70 apply (zenon_notand_s _ _ zenon_H67); [ zenon_intro zenon_H39 | zenon_intro zenon_H68 ]. % 0.50/0.70 apply (zenon_L8_); trivial. % 0.50/0.70 generalize (axiom_20 (i2003_11_14_17_20_46476)). zenon_intro zenon_H91. % 0.50/0.70 apply (zenon_imply_s _ _ zenon_H91); [ zenon_intro zenon_H41 | zenon_intro zenon_H92 ]. % 0.50/0.70 exact (zenon_H41 axiom_47). % 0.50/0.70 apply (zenon_or_s _ _ zenon_H92); [ zenon_intro zenon_H3b | zenon_intro zenon_H6b ]. % 0.50/0.70 apply (zenon_L15_); trivial. % 0.50/0.70 apply (zenon_or_s _ _ zenon_H6b); [ zenon_intro zenon_H60 | zenon_intro zenon_H6c ]. % 0.50/0.70 apply (zenon_L9_); trivial. % 0.50/0.70 exact (zenon_H68 zenon_H6c). % 0.50/0.70 (* end of lemma zenon_L24_ *) % 0.50/0.70 assert (zenon_L25_ : (cplus6 (i2003_11_14_17_20_46476)) -> False). % 0.50/0.70 do 0 intro. intros zenon_H89. % 0.50/0.70 generalize (axiom_21 (i2003_11_14_17_20_46476)). zenon_intro zenon_H8e. % 0.50/0.70 apply (zenon_imply_s _ _ zenon_H8e); [ zenon_intro zenon_H41 | zenon_intro zenon_H8f ]. % 0.50/0.70 exact (zenon_H41 axiom_47). % 0.50/0.70 apply (zenon_or_s _ _ zenon_H8f); [ zenon_intro zenon_H5f | zenon_intro zenon_H90 ]. % 0.50/0.70 generalize (axiom_2 (i2003_11_14_17_20_46476)). zenon_intro zenon_H93. % 0.50/0.70 apply (zenon_imply_s _ _ zenon_H93); [ zenon_intro zenon_H41 | zenon_intro zenon_H94 ]. % 0.50/0.70 exact (zenon_H41 axiom_47). % 0.50/0.70 apply (zenon_or_s _ _ zenon_H94); [ zenon_intro zenon_H86 | zenon_intro zenon_H95 ]. % 0.50/0.70 apply (zenon_L23_); trivial. % 0.50/0.70 apply (zenon_or_s _ _ zenon_H95); [ zenon_intro zenon_H44 | zenon_intro zenon_H8a ]. % 0.50/0.70 apply (zenon_L24_); trivial. % 0.50/0.70 apply (zenon_L22_); trivial. % 0.50/0.70 apply (zenon_or_s _ _ zenon_H90); [ zenon_intro zenon_H50 | zenon_intro zenon_H8a ]. % 0.50/0.70 apply (zenon_L19_); trivial. % 0.50/0.70 apply (zenon_L22_); trivial. % 0.50/0.70 (* end of lemma zenon_L25_ *) % 0.50/0.70 assert (zenon_L26_ : (~(cminus2 (i2003_11_14_17_20_46476))) -> (~(cplus9 (i2003_11_14_17_20_46476))) -> False). % 0.50/0.70 do 0 intro. intros zenon_H63 zenon_H3a. % 0.50/0.70 generalize (axiom_18 (i2003_11_14_17_20_46476)). zenon_intro zenon_H96. % 0.50/0.70 apply (zenon_imply_s _ _ zenon_H96); [ zenon_intro zenon_H41 | zenon_intro zenon_H97 ]. % 0.50/0.70 exact (zenon_H41 axiom_47). % 0.50/0.70 apply (zenon_or_s _ _ zenon_H97); [ zenon_intro zenon_H5f | zenon_intro zenon_H98 ]. % 0.50/0.70 exact (zenon_H63 zenon_H5f). % 0.50/0.70 apply (zenon_or_s _ _ zenon_H98); [ zenon_intro zenon_H89 | zenon_intro zenon_H44 ]. % 0.50/0.70 apply (zenon_L25_); trivial. % 0.50/0.70 exact (zenon_H3a zenon_H44). % 0.50/0.70 (* end of lemma zenon_L26_ *) % 0.50/0.70 generalize (axiom_5 (i2003_11_14_17_20_46476)). zenon_intro zenon_H99. % 0.50/0.70 apply (zenon_imply_s _ _ zenon_H99); [ zenon_intro zenon_H41 | zenon_intro zenon_H9a ]. % 0.50/0.70 exact (zenon_H41 axiom_47). % 0.50/0.70 apply (zenon_or_s _ _ zenon_H9a); [ zenon_intro zenon_H4a | zenon_intro zenon_H9b ]. % 0.50/0.70 generalize (axiom_50 (i2003_11_14_17_20_46476)). zenon_intro zenon_H49. % 0.50/0.70 apply (zenon_notand_s _ _ zenon_H49); [ zenon_intro zenon_H4c | zenon_intro zenon_H4b ]. % 0.50/0.70 generalize (axiom_49 (i2003_11_14_17_20_46476)). zenon_intro zenon_H47. % 0.50/0.70 apply (zenon_notand_s _ _ zenon_H47); [ zenon_intro zenon_H48 | zenon_intro zenon_H3a ]. % 0.50/0.70 generalize (axiom_56 (i2003_11_14_17_20_46476)). zenon_intro zenon_H8b. % 0.50/0.70 apply (zenon_notand_s _ _ zenon_H8b); [ zenon_intro zenon_H8d | zenon_intro zenon_H8c ]. % 0.50/0.70 generalize (axiom_54 (i2003_11_14_17_20_46476)). zenon_intro zenon_H61. % 0.50/0.70 apply (zenon_notand_s _ _ zenon_H61); [ zenon_intro zenon_H63 | zenon_intro zenon_H62 ]. % 0.50/0.70 generalize (axiom_4 (i2003_11_14_17_20_46476)). zenon_intro zenon_H7b. % 0.50/0.70 apply (zenon_imply_s _ _ zenon_H7b); [ zenon_intro zenon_H41 | zenon_intro zenon_H7c ]. % 0.50/0.70 exact (zenon_H41 axiom_47). % 0.50/0.70 apply (zenon_or_s _ _ zenon_H7c); [ zenon_intro zenon_H3b | zenon_intro zenon_H7d ]. % 0.50/0.70 apply (zenon_L10_); trivial. % 0.50/0.70 apply (zenon_or_s _ _ zenon_H7d); [ zenon_intro zenon_H70 | zenon_intro zenon_H6c ]. % 0.50/0.70 generalize (axiom_51 (i2003_11_14_17_20_46476)). zenon_intro zenon_H71. % 0.50/0.70 apply (zenon_notand_s _ _ zenon_H71); [ zenon_intro zenon_H73 | zenon_intro zenon_H72 ]. % 0.50/0.70 generalize (axiom_22 (i2003_11_14_17_20_46476)). zenon_intro zenon_H9c. % 0.50/0.70 apply (zenon_imply_s _ _ zenon_H9c); [ zenon_intro zenon_H41 | zenon_intro zenon_H9d ]. % 0.50/0.70 exact (zenon_H41 axiom_47). % 0.50/0.70 apply (zenon_or_s _ _ zenon_H9d); [ zenon_intro zenon_H5f | zenon_intro zenon_H9e ]. % 0.50/0.70 exact (zenon_H63 zenon_H5f). % 0.50/0.70 apply (zenon_or_s _ _ zenon_H9e); [ zenon_intro zenon_H89 | zenon_intro zenon_H77 ]. % 0.50/0.70 exact (zenon_H8d zenon_H89). % 0.50/0.70 exact (zenon_H73 zenon_H77). % 0.50/0.70 exact (zenon_H72 zenon_H70). % 0.50/0.70 apply (zenon_L11_); trivial. % 0.50/0.70 generalize (axiom_27 (i2003_11_14_17_20_46476)). zenon_intro zenon_H9f. % 0.50/0.70 apply (zenon_imply_s _ _ zenon_H9f); [ zenon_intro zenon_H41 | zenon_intro zenon_Ha0 ]. % 0.50/0.70 exact (zenon_H41 axiom_47). % 0.50/0.70 apply (zenon_or_s _ _ zenon_Ha0); [ zenon_intro zenon_H50 | zenon_intro zenon_Ha1 ]. % 0.50/0.70 exact (zenon_H4c zenon_H50). % 0.50/0.70 apply (zenon_or_s _ _ zenon_Ha1); [ zenon_intro zenon_H55 | zenon_intro zenon_H89 ]. % 0.50/0.70 generalize (axiom_48 (i2003_11_14_17_20_46476)). zenon_intro zenon_H67. % 0.50/0.70 apply (zenon_notand_s _ _ zenon_H67); [ zenon_intro zenon_H39 | zenon_intro zenon_H68 ]. % 0.50/0.70 apply (zenon_L7_); trivial. % 0.50/0.70 generalize (axiom_20 (i2003_11_14_17_20_46476)). zenon_intro zenon_H91. % 0.50/0.70 apply (zenon_imply_s _ _ zenon_H91); [ zenon_intro zenon_H41 | zenon_intro zenon_H92 ]. % 0.50/0.70 exact (zenon_H41 axiom_47). % 0.50/0.70 apply (zenon_or_s _ _ zenon_H92); [ zenon_intro zenon_H3b | zenon_intro zenon_H6b ]. % 0.50/0.70 apply (zenon_L13_); trivial. % 0.50/0.70 apply (zenon_or_s _ _ zenon_H6b); [ zenon_intro zenon_H60 | zenon_intro zenon_H6c ]. % 0.50/0.70 exact (zenon_H62 zenon_H60). % 0.50/0.70 exact (zenon_H68 zenon_H6c). % 0.50/0.70 exact (zenon_H8d zenon_H89). % 0.50/0.70 generalize (axiom_43 (i2003_11_14_17_20_46476)). zenon_intro zenon_Ha2. % 0.50/0.70 apply (zenon_imply_s _ _ zenon_Ha2); [ zenon_intro zenon_H41 | zenon_intro zenon_Ha3 ]. % 0.50/0.70 exact (zenon_H41 axiom_47). % 0.50/0.70 apply (zenon_or_s _ _ zenon_Ha3); [ zenon_intro zenon_H46 | zenon_intro zenon_Ha4 ]. % 0.50/0.70 exact (zenon_H48 zenon_H46). % 0.50/0.70 apply (zenon_or_s _ _ zenon_Ha4); [ zenon_intro zenon_H86 | zenon_intro zenon_H8a ]. % 0.50/0.70 generalize (axiom_55 (i2003_11_14_17_20_46476)). zenon_intro zenon_H87. % 0.50/0.70 apply (zenon_notand_s _ _ zenon_H87); [ zenon_intro zenon_H81 | zenon_intro zenon_H88 ]. % 0.50/0.70 generalize (axiom_21 (i2003_11_14_17_20_46476)). zenon_intro zenon_H8e. % 0.50/0.70 apply (zenon_imply_s _ _ zenon_H8e); [ zenon_intro zenon_H41 | zenon_intro zenon_H8f ]. % 0.50/0.70 exact (zenon_H41 axiom_47). % 0.50/0.70 apply (zenon_or_s _ _ zenon_H8f); [ zenon_intro zenon_H5f | zenon_intro zenon_H90 ]. % 0.50/0.70 apply (zenon_L20_); trivial. % 0.50/0.70 apply (zenon_or_s _ _ zenon_H90); [ zenon_intro zenon_H50 | zenon_intro zenon_H8a ]. % 0.50/0.70 exact (zenon_H4c zenon_H50). % 0.50/0.70 exact (zenon_H8c zenon_H8a). % 0.50/0.70 exact (zenon_H88 zenon_H86). % 0.50/0.70 exact (zenon_H8c zenon_H8a). % 0.50/0.70 generalize (axiom_56 (i2003_11_14_17_20_46476)). zenon_intro zenon_H8b. % 0.50/0.70 apply (zenon_notand_s _ _ zenon_H8b); [ zenon_intro zenon_H8d | zenon_intro zenon_H8c ]. % 0.50/0.70 generalize (axiom_54 (i2003_11_14_17_20_46476)). zenon_intro zenon_H61. % 0.50/0.70 apply (zenon_notand_s _ _ zenon_H61); [ zenon_intro zenon_H63 | zenon_intro zenon_H62 ]. % 0.50/0.70 apply (zenon_L26_); trivial. % 0.50/0.70 generalize (axiom_13 (i2003_11_14_17_20_46476)). zenon_intro zenon_H6d. % 0.50/0.70 apply (zenon_imply_s _ _ zenon_H6d); [ zenon_intro zenon_H41 | zenon_intro zenon_H6e ]. % 0.50/0.70 exact (zenon_H41 axiom_47). % 0.50/0.70 apply (zenon_or_s _ _ zenon_H6e); [ zenon_intro zenon_H60 | zenon_intro zenon_H6f ]. % 0.50/0.70 exact (zenon_H62 zenon_H60). % 0.50/0.70 apply (zenon_or_s _ _ zenon_H6f); [ zenon_intro zenon_H54 | zenon_intro zenon_H44 ]. % 0.50/0.70 generalize (axiom_27 (i2003_11_14_17_20_46476)). zenon_intro zenon_H9f. % 0.50/0.70 apply (zenon_imply_s _ _ zenon_H9f); [ zenon_intro zenon_H41 | zenon_intro zenon_Ha0 ]. % 0.50/0.70 exact (zenon_H41 axiom_47). % 0.50/0.70 apply (zenon_or_s _ _ zenon_Ha0); [ zenon_intro zenon_H50 | zenon_intro zenon_Ha1 ]. % 0.50/0.70 exact (zenon_H4c zenon_H50). % 0.50/0.70 apply (zenon_or_s _ _ zenon_Ha1); [ zenon_intro zenon_H55 | zenon_intro zenon_H89 ]. % 0.50/0.70 apply (zenon_L6_); trivial. % 0.50/0.70 exact (zenon_H8d zenon_H89). % 0.50/0.70 exact (zenon_H3a zenon_H44). % 0.50/0.70 generalize (axiom_54 (i2003_11_14_17_20_46476)). zenon_intro zenon_H61. % 0.50/0.70 apply (zenon_notand_s _ _ zenon_H61); [ zenon_intro zenon_H63 | zenon_intro zenon_H62 ]. % 0.50/0.70 apply (zenon_L26_); trivial. % 0.50/0.70 generalize (axiom_55 (i2003_11_14_17_20_46476)). zenon_intro zenon_H87. % 0.50/0.70 apply (zenon_notand_s _ _ zenon_H87); [ zenon_intro zenon_H81 | zenon_intro zenon_H88 ]. % 0.50/0.70 generalize (axiom_18 (i2003_11_14_17_20_46476)). zenon_intro zenon_H96. % 0.50/0.70 apply (zenon_imply_s _ _ zenon_H96); [ zenon_intro zenon_H41 | zenon_intro zenon_H97 ]. % 0.50/0.70 exact (zenon_H41 axiom_47). % 0.50/0.70 apply (zenon_or_s _ _ zenon_H97); [ zenon_intro zenon_H5f | zenon_intro zenon_H98 ]. % 0.50/0.70 apply (zenon_L20_); trivial. % 0.50/0.70 apply (zenon_or_s _ _ zenon_H98); [ zenon_intro zenon_H89 | zenon_intro zenon_H44 ]. % 0.50/0.70 apply (zenon_L25_); trivial. % 0.50/0.70 exact (zenon_H3a zenon_H44). % 0.50/0.70 generalize (axiom_19 (i2003_11_14_17_20_46476)). zenon_intro zenon_Ha5. % 0.50/0.70 apply (zenon_imply_s _ _ zenon_Ha5); [ zenon_intro zenon_H41 | zenon_intro zenon_Ha6 ]. % 0.50/0.70 exact (zenon_H41 axiom_47). % 0.50/0.70 apply (zenon_or_s _ _ zenon_Ha6); [ zenon_intro zenon_H60 | zenon_intro zenon_Ha4 ]. % 0.50/0.70 exact (zenon_H62 zenon_H60). % 0.50/0.70 apply (zenon_or_s _ _ zenon_Ha4); [ zenon_intro zenon_H86 | zenon_intro zenon_H8a ]. % 0.50/0.70 exact (zenon_H88 zenon_H86). % 0.50/0.70 exact (zenon_H8c zenon_H8a). % 0.50/0.70 exact (zenon_H4b zenon_H4a). % 0.50/0.70 apply (zenon_or_s _ _ zenon_H9b); [ zenon_intro zenon_H89 | zenon_intro zenon_H6c ]. % 0.50/0.70 apply (zenon_L25_); trivial. % 0.50/0.70 apply (zenon_L11_); trivial. % 0.50/0.70 Qed. % 0.50/0.70 % SZS output end Proof % 0.50/0.70 (* END-PROOF *) % 0.50/0.70 nodes searched: 15901 % 0.50/0.70 max branch formulas: 1453 % 0.50/0.70 proof nodes created: 1273 % 0.50/0.70 formulas created: 31815 % 0.50/0.70 %------------------------------------------------------------------------------