%------------------------------------------------------------------------------ % File : Zenon---0.7.1 % Problem : AGT005+1 : TPTP v8.1.0. Bugfixed v3.1.0. % Transfm : none % Format : tptp:raw % Command : run_zenon %s %d % Computer : n020.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 : Thu Jul 14 12:05:58 EDT 2022 % Result : Theorem 52.16s 52.35s % Output : Proof 52.16s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.13 % Problem : AGT005+1 : TPTP v8.1.0. Bugfixed v3.1.0. % 0.13/0.13 % Command : run_zenon %s %d % 0.13/0.35 % Computer : n020.cluster.edu % 0.13/0.35 % Model : x86_64 x86_64 % 0.13/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.35 % Memory : 8042.1875MB % 0.13/0.35 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.35 % CPULimit : 300 % 0.13/0.35 % WCLimit : 600 % 0.13/0.35 % DateTime : Sat Jun 4 06:41:52 EDT 2022 % 0.20/0.35 % CPUTime : % 52.16/52.35 (* PROOF-FOUND *) % 52.16/52.35 % SZS status Theorem % 52.16/52.35 (* BEGIN-PROOF *) % 52.16/52.35 % SZS output start Proof % 52.16/52.35 Theorem query_5 : (accept_team (christiansufferterrahumanitarianorganization) (countryafirstaidorganization) (towna) (n3)). % 52.16/52.35 Proof. % 52.16/52.35 assert (zenon_L1_ : (~((christiansufferterrahumanitarianorganization) = (christiansufferterrahumanitarianorganization))) -> False). % 52.16/52.35 do 0 intro. intros zenon_H22c. % 52.16/52.35 apply zenon_H22c. apply refl_equal. % 52.16/52.35 (* end of lemma zenon_L1_ *) % 52.16/52.35 assert (zenon_L2_ : (~(~((n3) = (n5)))) -> (~((n5) = (n3))) -> False). % 52.16/52.35 do 0 intro. intros zenon_H22d zenon_H22e. % 52.16/52.35 apply zenon_H22d. zenon_intro zenon_H22f. % 52.16/52.35 apply zenon_H22e. apply sym_equal. exact zenon_H22f. % 52.16/52.35 (* end of lemma zenon_L2_ *) % 52.16/52.35 assert (zenon_L3_ : (forall M : zenon_U, (((accept_number (countryccivilorganization) (n3))/\(less M (n3)))->(accept_number (countryccivilorganization) M))) -> (less (n5) (n3)) -> (~(accept_number (countryccivilorganization) (n5))) -> False). % 52.16/52.35 do 0 intro. intros zenon_H230 zenon_H231 zenon_H232. % 52.16/52.35 generalize (zenon_H230 (n5)). zenon_intro zenon_H233. % 52.16/52.35 apply (zenon_imply_s _ _ zenon_H233); [ zenon_intro zenon_H235 | zenon_intro zenon_H234 ]. % 52.16/52.35 apply (zenon_notand_s _ _ zenon_H235); [ zenon_intro zenon_H237 | zenon_intro zenon_H236 ]. % 52.16/52.35 exact (zenon_H237 event_215). % 52.16/52.35 exact (zenon_H236 zenon_H231). % 52.16/52.35 exact (zenon_H232 zenon_H234). % 52.16/52.35 (* end of lemma zenon_L3_ *) % 52.16/52.35 assert (zenon_L4_ : (~(accept_number (countryccivilorganization) (n5))) -> (~(accept_number (christiansufferterrahumanitarianorganization) (n3))) -> (accept_number (christiansufferterrahumanitarianorganization) (n5)) -> (~((n5) = (n3))) -> False). % 52.16/52.35 do 0 intro. intros zenon_H232 zenon_H238 zenon_H239 zenon_H22e. % 52.16/52.35 generalize (a1_2 (countryccivilorganization)). zenon_intro zenon_H23a. % 52.16/52.35 generalize (a1_2 (christiansufferterrahumanitarianorganization)). zenon_intro zenon_H23b. % 52.16/52.35 generalize (zenon_H23a (n3)). zenon_intro zenon_H230. % 52.16/52.35 generalize (less_property (n5)). zenon_intro zenon_H23c. % 52.16/52.35 generalize (zenon_H23b (n5)). zenon_intro zenon_H23d. % 52.16/52.35 generalize (zenon_H23c (n3)). zenon_intro zenon_H23e. % 52.16/52.35 apply (zenon_equiv_s _ _ zenon_H23e); [ zenon_intro zenon_H236; zenon_intro zenon_H240 | zenon_intro zenon_H231; zenon_intro zenon_H23f ]. % 52.16/52.35 apply (zenon_notand_s _ _ zenon_H240); [ zenon_intro zenon_H241 | zenon_intro zenon_H22d ]. % 52.16/52.35 apply zenon_H241. zenon_intro zenon_H242. % 52.16/52.35 generalize (zenon_H23d (n3)). zenon_intro zenon_H243. % 52.16/52.35 apply (zenon_imply_s _ _ zenon_H243); [ zenon_intro zenon_H245 | zenon_intro zenon_H244 ]. % 52.16/52.35 apply (zenon_notand_s _ _ zenon_H245); [ zenon_intro zenon_H247 | zenon_intro zenon_H246 ]. % 52.16/52.35 exact (zenon_H247 zenon_H239). % 52.16/52.35 exact (zenon_H246 zenon_H242). % 52.16/52.35 exact (zenon_H238 zenon_H244). % 52.16/52.35 apply (zenon_L2_); trivial. % 52.16/52.35 apply (zenon_L3_); trivial. % 52.16/52.35 (* end of lemma zenon_L4_ *) % 52.16/52.35 apply NNPP. intro zenon_G. % 52.16/52.35 generalize (a1_1 (countryccivilorganization)). zenon_intro zenon_H248. % 52.16/52.35 generalize (zenon_H248 (cityb)). zenon_intro zenon_H249. % 52.16/52.35 generalize (zenon_H249 (n2)). zenon_intro zenon_H24a. % 52.16/52.35 generalize (zenon_H24a (countrybhumanitarianorganization)). zenon_intro zenon_H24b. % 52.16/52.35 apply (zenon_equiv_s _ _ zenon_H24b); [ zenon_intro zenon_H24e; zenon_intro zenon_H24d | zenon_intro event_7; zenon_intro zenon_H24c ]. % 52.16/52.35 exact (zenon_H24e event_7). % 52.16/52.35 apply (zenon_and_s _ _ zenon_H24c). zenon_intro zenon_H250. zenon_intro zenon_H24f. % 52.16/52.35 apply (zenon_and_s _ _ zenon_H24f). zenon_intro zenon_H251. zenon_intro event_214. % 52.16/52.35 generalize (a1_1 (christiansufferterrahumanitarianorganization)). zenon_intro zenon_H252. % 52.16/52.35 generalize (zenon_H252 (towna)). zenon_intro zenon_H253. % 52.16/52.35 generalize (zenon_H253 (n6)). zenon_intro zenon_H254. % 52.16/52.35 generalize (zenon_H254 (countryacivilorganization)). zenon_intro zenon_H255. % 52.16/52.35 apply (zenon_equiv_s _ _ zenon_H255); [ zenon_intro zenon_H258; zenon_intro zenon_H257 | zenon_intro event_26; zenon_intro zenon_H256 ]. % 52.16/52.35 exact (zenon_H258 event_26). % 52.16/52.35 apply (zenon_and_s _ _ zenon_H256). zenon_intro zenon_H25a. zenon_intro zenon_H259. % 52.16/52.35 generalize (a1_1 (christiansufferterrahumanitarianorganization)). zenon_intro zenon_H252. % 52.16/52.35 generalize (zenon_H252 (coastvillage)). zenon_intro zenon_H25b. % 52.16/52.35 generalize (zenon_H25b (n5)). zenon_intro zenon_H25c. % 52.16/52.35 generalize (zenon_H25c (countryahumanitarianorganization)). zenon_intro zenon_H25d. % 52.16/52.35 apply (zenon_equiv_s _ _ zenon_H25d); [ zenon_intro zenon_H260; zenon_intro zenon_H25f | zenon_intro event_90; zenon_intro zenon_H25e ]. % 52.16/52.35 exact (zenon_H260 event_90). % 52.16/52.35 apply (zenon_and_s _ _ zenon_H25e). zenon_intro zenon_H262. zenon_intro zenon_H261. % 52.16/52.35 apply (zenon_and_s _ _ zenon_H261). zenon_intro zenon_H263. zenon_intro zenon_H239. % 52.16/52.35 generalize (a1_1 (christiansufferterrahumanitarianorganization)). zenon_intro zenon_H252. % 52.16/52.35 generalize (zenon_H252 (coastvillage)). zenon_intro zenon_H25b. % 52.16/52.35 generalize (zenon_H25b (n6)). zenon_intro zenon_H264. % 52.16/52.35 generalize (zenon_H264 (countryafirstaidorganization)). zenon_intro zenon_H265. % 52.16/52.35 apply (zenon_equiv_s _ _ zenon_H265); [ zenon_intro zenon_H268; zenon_intro zenon_H267 | zenon_intro event_93; zenon_intro zenon_H266 ]. % 52.16/52.35 exact (zenon_H268 event_93). % 52.16/52.35 apply (zenon_and_s _ _ zenon_H266). zenon_intro zenon_H262. zenon_intro zenon_H269. % 52.16/52.35 apply (zenon_and_s _ _ zenon_H269). zenon_intro zenon_H26a. zenon_intro event_140. % 52.16/52.35 generalize (a1_1 (countryccivilorganization)). zenon_intro zenon_H248. % 52.16/52.35 generalize (zenon_H248 (cityb)). zenon_intro zenon_H249. % 52.16/52.35 generalize (zenon_H249 (n5)). zenon_intro zenon_H26b. % 52.16/52.35 generalize (zenon_H26b (countrybhumanitarianorganization)). zenon_intro zenon_H26c. % 52.16/52.35 apply (zenon_equiv_s _ _ zenon_H26c); [ zenon_intro event_143; zenon_intro zenon_H26f | zenon_intro zenon_H26e; zenon_intro zenon_H26d ]. % 52.16/52.35 generalize (a1_1 (christiansufferterrahumanitarianorganization)). zenon_intro zenon_H252. % 52.16/52.35 generalize (zenon_H252 (towna)). zenon_intro zenon_H253. % 52.16/52.35 generalize (zenon_H253 (n3)). zenon_intro zenon_H270. % 52.16/52.35 generalize (zenon_H270 (countryafirstaidorganization)). zenon_intro zenon_H271. % 52.16/52.35 apply (zenon_equiv_s _ _ zenon_H271); [ zenon_intro zenon_G; zenon_intro zenon_H274 | zenon_intro zenon_H273; zenon_intro zenon_H272 ]. % 52.16/52.35 apply (zenon_notand_s _ _ zenon_H274); [ zenon_intro zenon_H276 | zenon_intro zenon_H275 ]. % 52.16/52.35 exact (zenon_H276 zenon_H25a). % 52.16/52.35 apply (zenon_notand_s _ _ zenon_H275); [ zenon_intro zenon_H277 | zenon_intro zenon_H238 ]. % 52.16/52.35 exact (zenon_H277 zenon_H26a). % 52.16/52.35 apply (zenon_notand_s _ _ zenon_H26f); [ zenon_intro zenon_H279 | zenon_intro zenon_H278 ]. % 52.16/52.35 exact (zenon_H279 zenon_H250). % 52.16/52.35 apply (zenon_notand_s _ _ zenon_H278); [ zenon_intro zenon_H27a | zenon_intro zenon_H232 ]. % 52.16/52.35 exact (zenon_H27a zenon_H251). % 52.16/52.35 cut ((accept_number (christiansufferterrahumanitarianorganization) (n5)) = (accept_number (christiansufferterrahumanitarianorganization) (n3))). % 52.16/52.35 intro zenon_D_pnotp. % 52.16/52.35 apply zenon_H238. % 52.16/52.35 rewrite <- zenon_D_pnotp. % 52.16/52.35 exact zenon_H239. % 52.16/52.35 cut (((n5) = (n3))); [idtac | apply NNPP; zenon_intro zenon_H22e]. % 52.16/52.35 cut (((christiansufferterrahumanitarianorganization) = (christiansufferterrahumanitarianorganization))); [idtac | apply NNPP; zenon_intro zenon_H22c]. % 52.16/52.35 congruence. % 52.16/52.35 apply zenon_H22c. apply refl_equal. % 52.16/52.35 apply (zenon_L4_); trivial. % 52.16/52.35 exact (zenon_G zenon_H273). % 52.16/52.35 exact (event_143 zenon_H26e). % 52.16/52.35 Qed. % 52.16/52.35 % SZS output end Proof % 52.16/52.35 (* END-PROOF *) % 52.16/52.35 nodes searched: 1287574 % 52.16/52.35 max branch formulas: 23701 % 52.16/52.35 proof nodes created: 33709 % 52.16/52.35 formulas created: 2482841 % 52.16/52.35 %------------------------------------------------------------------------------