%------------------------------------------------------------------------------ % File : Zenon---0.7.1 % Problem : CSR034+2 : TPTP v8.1.0. Released v3.4.0. % Transfm : none % Format : tptp:raw % Command : run_zenon %s %d % Computer : n025.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 : Sat Jul 16 00:01:55 EDT 2022 % Result : Theorem 0.99s 1.20s % Output : Proof 0.99s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.12 % Problem : CSR034+2 : TPTP v8.1.0. Released v3.4.0. % 0.03/0.13 % Command : run_zenon %s %d % 0.13/0.34 % Computer : n025.cluster.edu % 0.13/0.34 % Model : x86_64 x86_64 % 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.34 % Memory : 8042.1875MB % 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.34 % CPULimit : 300 % 0.13/0.34 % WCLimit : 600 % 0.13/0.34 % DateTime : Sat Jun 11 03:58:52 EDT 2022 % 0.13/0.35 % CPUTime : % 0.99/1.20 (* PROOF-FOUND *) % 0.99/1.20 % SZS status Theorem % 0.99/1.20 (* BEGIN-PROOF *) % 0.99/1.20 % SZS output start Proof % 0.99/1.20 Theorem query84 : (exists COL : zenon_U, ((mtvisible (c_tptp_member3515_mt))->(isa (c_wanica_districtsuriname) COL))). % 0.99/1.20 Proof. % 0.99/1.20 assert (zenon_L1_ : (~((c_worldgeographymt) = (c_worldgeographymt))) -> False). % 0.99/1.20 do 0 intro. intros zenon_H451. % 0.99/1.20 apply zenon_H451. apply refl_equal. % 0.99/1.20 (* end of lemma zenon_L1_ *) % 0.99/1.20 apply NNPP. intro zenon_G. % 0.99/1.20 elim (classic (forall x : zenon_U, (forall y : zenon_U, (forall z : zenon_U, ((genlmt x y)->((genlmt y z)->(genlmt x z))))))); [ zenon_intro zenon_H452 | zenon_intro zenon_H453 ]. % 0.99/1.20 apply (zenon_imply_s _ _ ax1_321); [ zenon_intro zenon_H455 | zenon_intro zenon_H454 ]. % 0.99/1.20 apply zenon_G. exists zenon_E. apply NNPP. zenon_intro zenon_H456. % 0.99/1.20 apply (zenon_notimply_s _ _ zenon_H456). zenon_intro zenon_H458. zenon_intro zenon_H457. % 0.99/1.20 generalize (ax1_1123 (c_tptp_member3515_mt)). zenon_intro zenon_H459. % 0.99/1.20 generalize (zenon_H459 (c_worldgeographymt)). zenon_intro zenon_H45a. % 0.99/1.20 apply (zenon_imply_s _ _ zenon_H45a); [ zenon_intro zenon_H45c | zenon_intro zenon_H45b ]. % 0.99/1.20 apply (zenon_notand_s _ _ zenon_H45c); [ zenon_intro zenon_H45e | zenon_intro zenon_H45d ]. % 0.99/1.20 exact (zenon_H45e zenon_H458). % 0.99/1.20 elim (classic ((~((c_tptp_member3515_mt) = (c_worldgeographydualistmt)))/\(~(genlmt (c_tptp_member3515_mt) (c_worldgeographydualistmt))))); [ zenon_intro zenon_H45f | zenon_intro zenon_H460 ]. % 0.99/1.20 apply (zenon_and_s _ _ zenon_H45f). zenon_intro zenon_H462. zenon_intro zenon_H461. % 0.99/1.20 elim (classic ((~((c_tptp_member3515_mt) = (c_unitedstatesgeographydualistmt)))/\(~(genlmt (c_tptp_member3515_mt) (c_unitedstatesgeographydualistmt))))); [ zenon_intro zenon_H463 | zenon_intro zenon_H464 ]. % 0.99/1.20 apply (zenon_and_s _ _ zenon_H463). zenon_intro zenon_H466. zenon_intro zenon_H465. % 0.99/1.20 elim (classic ((~((c_tptp_member3515_mt) = (c_worldcompletedualistgeographymt)))/\(~(genlmt (c_tptp_member3515_mt) (c_worldcompletedualistgeographymt))))); [ zenon_intro zenon_H467 | zenon_intro zenon_H468 ]. % 0.99/1.20 apply (zenon_and_s _ _ zenon_H467). zenon_intro zenon_H46a. zenon_intro zenon_H469. % 0.99/1.20 elim (classic ((~((c_tptp_member3515_mt) = (c_ethnicgroupsvocabularymt)))/\(~(genlmt (c_tptp_member3515_mt) (c_ethnicgroupsvocabularymt))))); [ zenon_intro zenon_H46b | zenon_intro zenon_H46c ]. % 0.99/1.20 apply (zenon_and_s _ _ zenon_H46b). zenon_intro zenon_H46e. zenon_intro zenon_H46d. % 0.99/1.20 elim (classic ((~((c_tptp_member3515_mt) = (c_ethnicgroupsmt)))/\(~(genlmt (c_tptp_member3515_mt) (c_ethnicgroupsmt))))); [ zenon_intro zenon_H46f | zenon_intro zenon_H470 ]. % 0.99/1.20 apply (zenon_and_s _ _ zenon_H46f). zenon_intro zenon_H472. zenon_intro zenon_H471. % 0.99/1.20 elim (classic ((~((c_tptp_member3515_mt) = (c_massmediadatamt)))/\(~(genlmt (c_tptp_member3515_mt) (c_massmediadatamt))))); [ zenon_intro zenon_H473 | zenon_intro zenon_H474 ]. % 0.99/1.20 apply (zenon_and_s _ _ zenon_H473). zenon_intro zenon_H476. zenon_intro zenon_H475. % 0.99/1.20 elim (classic ((~((c_tptp_member3515_mt) = (f_contextofpcwfn (c_ap_martha_stewart_omnimedia_names_chairman))))/\(~(genlmt (c_tptp_member3515_mt) (f_contextofpcwfn (c_ap_martha_stewart_omnimedia_names_chairman)))))); [ zenon_intro zenon_H477 | zenon_intro zenon_H478 ]. % 0.99/1.20 apply (zenon_and_s _ _ zenon_H477). zenon_intro zenon_H47a. zenon_intro zenon_H479. % 0.99/1.20 elim (classic ((~((c_tptp_member3515_mt) = (c_organizationdatamt)))/\(~(genlmt (c_tptp_member3515_mt) (c_organizationdatamt))))); [ zenon_intro zenon_H47b | zenon_intro zenon_H47c ]. % 0.99/1.20 apply (zenon_and_s _ _ zenon_H47b). zenon_intro zenon_H47e. zenon_intro zenon_H47d. % 0.99/1.20 elim (classic ((~((c_tptp_member3515_mt) = (c_nooescapearchitecturemt)))/\(~(genlmt (c_tptp_member3515_mt) (c_nooescapearchitecturemt))))); [ zenon_intro zenon_H47f | zenon_intro zenon_H480 ]. % 0.99/1.20 apply (zenon_and_s _ _ zenon_H47f). zenon_intro zenon_H482. zenon_intro zenon_H481. % 0.99/1.20 elim (classic ((~((c_tptp_member3515_mt) = (c_testvocabularymt)))/\(~(genlmt (c_tptp_member3515_mt) (c_testvocabularymt))))); [ zenon_intro zenon_H483 | zenon_intro zenon_H484 ]. % 0.99/1.20 apply (zenon_and_s _ _ zenon_H483). zenon_intro zenon_H486. zenon_intro zenon_H485. % 0.99/1.20 elim (classic ((~((c_tptp_member3515_mt) = (c_keinteractionresourcetestmt)))/\(~(genlmt (c_tptp_member3515_mt) (c_keinteractionresourcetestmt))))); [ zenon_intro zenon_H487 | zenon_intro zenon_H488 ]. % 0.99/1.20 apply (zenon_and_s _ _ zenon_H487). zenon_intro zenon_H48a. zenon_intro zenon_H489. % 0.99/1.20 elim (classic ((~((c_tptp_member3515_mt) = (c_cyclistsmt)))/\(~(genlmt (c_tptp_member3515_mt) (c_cyclistsmt))))); [ zenon_intro zenon_H48b | zenon_intro zenon_H48c ]. % 0.99/1.20 apply (zenon_and_s _ _ zenon_H48b). zenon_intro zenon_H48e. zenon_intro zenon_H48d. % 0.99/1.20 elim (classic ((~((c_tptp_member3515_mt) = (c_tptp_spindleheadmt)))/\(~(genlmt (c_tptp_member3515_mt) (c_tptp_spindleheadmt))))); [ zenon_intro zenon_H48f | zenon_intro zenon_H490 ]. % 0.99/1.20 apply (zenon_and_s _ _ zenon_H48f). zenon_intro zenon_H492. zenon_intro zenon_H491. % 0.99/1.20 exact (zenon_H491 ax1_147). % 0.99/1.20 cut ((genlmt (c_tptp_spindleheadmt) (c_cyclistsmt)) = (genlmt (c_tptp_member3515_mt) (c_cyclistsmt))). % 0.99/1.20 intro zenon_D_pnotp. % 0.99/1.20 apply zenon_H48d. % 0.99/1.20 rewrite <- zenon_D_pnotp. % 0.99/1.20 exact ax1_254. % 0.99/1.20 cut (((c_cyclistsmt) = (c_cyclistsmt))); [idtac | apply NNPP; zenon_intro zenon_H493]. % 0.99/1.20 cut (((c_tptp_spindleheadmt) = (c_tptp_member3515_mt))); [idtac | apply NNPP; zenon_intro zenon_H494]. % 0.99/1.20 congruence. % 0.99/1.20 apply (zenon_notand_s _ _ zenon_H490); [ zenon_intro zenon_H496 | zenon_intro zenon_H495 ]. % 0.99/1.20 apply zenon_H496. zenon_intro zenon_H497. % 0.99/1.20 elim (classic ((c_tptp_member3515_mt) = (c_tptp_member3515_mt))); [ zenon_intro zenon_H498 | zenon_intro zenon_H499 ]. % 0.99/1.20 cut (((c_tptp_member3515_mt) = (c_tptp_member3515_mt)) = ((c_tptp_spindleheadmt) = (c_tptp_member3515_mt))). % 0.99/1.20 intro zenon_D_pnotp. % 0.99/1.20 apply zenon_H494. % 0.99/1.20 rewrite <- zenon_D_pnotp. % 0.99/1.20 exact zenon_H498. % 0.99/1.20 cut (((c_tptp_member3515_mt) = (c_tptp_member3515_mt))); [idtac | apply NNPP; zenon_intro zenon_H499]. % 0.99/1.20 cut (((c_tptp_member3515_mt) = (c_tptp_spindleheadmt))); [idtac | apply NNPP; zenon_intro zenon_H492]. % 0.99/1.20 congruence. % 0.99/1.20 exact (zenon_H492 zenon_H497). % 0.99/1.20 apply zenon_H499. apply refl_equal. % 0.99/1.20 apply zenon_H499. apply refl_equal. % 0.99/1.20 apply zenon_H495. zenon_intro ax1_147. % 0.99/1.20 generalize (zenon_H452 (c_tptp_member3515_mt)). zenon_intro zenon_H49a. % 0.99/1.20 generalize (zenon_H49a (c_tptp_spindleheadmt)). zenon_intro zenon_H49b. % 0.99/1.20 generalize (zenon_H49b (c_cyclistsmt)). zenon_intro zenon_H49c. % 0.99/1.20 apply (zenon_imply_s _ _ zenon_H49c); [ zenon_intro zenon_H491 | zenon_intro zenon_H49d ]. % 0.99/1.20 exact (zenon_H491 ax1_147). % 0.99/1.20 apply (zenon_imply_s _ _ zenon_H49d); [ zenon_intro zenon_H49f | zenon_intro zenon_H49e ]. % 0.99/1.20 exact (zenon_H49f ax1_254). % 0.99/1.20 exact (zenon_H48d zenon_H49e). % 0.99/1.20 apply zenon_H493. apply refl_equal. % 0.99/1.20 cut ((genlmt (c_cyclistsmt) (c_keinteractionresourcetestmt)) = (genlmt (c_tptp_member3515_mt) (c_keinteractionresourcetestmt))). % 0.99/1.20 intro zenon_D_pnotp. % 0.99/1.20 apply zenon_H489. % 0.99/1.20 rewrite <- zenon_D_pnotp. % 0.99/1.20 exact ax1_310. % 0.99/1.20 cut (((c_keinteractionresourcetestmt) = (c_keinteractionresourcetestmt))); [idtac | apply NNPP; zenon_intro zenon_H4a0]. % 0.99/1.20 cut (((c_cyclistsmt) = (c_tptp_member3515_mt))); [idtac | apply NNPP; zenon_intro zenon_H4a1]. % 0.99/1.20 congruence. % 0.99/1.20 apply (zenon_notand_s _ _ zenon_H48c); [ zenon_intro zenon_H4a3 | zenon_intro zenon_H4a2 ]. % 0.99/1.20 apply zenon_H4a3. zenon_intro zenon_H4a4. % 0.99/1.20 elim (classic ((c_tptp_member3515_mt) = (c_tptp_member3515_mt))); [ zenon_intro zenon_H498 | zenon_intro zenon_H499 ]. % 0.99/1.20 cut (((c_tptp_member3515_mt) = (c_tptp_member3515_mt)) = ((c_cyclistsmt) = (c_tptp_member3515_mt))). % 0.99/1.20 intro zenon_D_pnotp. % 0.99/1.20 apply zenon_H4a1. % 0.99/1.20 rewrite <- zenon_D_pnotp. % 0.99/1.20 exact zenon_H498. % 0.99/1.20 cut (((c_tptp_member3515_mt) = (c_tptp_member3515_mt))); [idtac | apply NNPP; zenon_intro zenon_H499]. % 0.99/1.20 cut (((c_tptp_member3515_mt) = (c_cyclistsmt))); [idtac | apply NNPP; zenon_intro zenon_H48e]. % 0.99/1.20 congruence. % 0.99/1.20 exact (zenon_H48e zenon_H4a4). % 0.99/1.20 apply zenon_H499. apply refl_equal. % 0.99/1.20 apply zenon_H499. apply refl_equal. % 0.99/1.20 apply zenon_H4a2. zenon_intro zenon_H49e. % 0.99/1.20 generalize (zenon_H452 (c_tptp_member3515_mt)). zenon_intro zenon_H49a. % 0.99/1.20 generalize (zenon_H49a (c_cyclistsmt)). zenon_intro zenon_H4a5. % 0.99/1.20 generalize (zenon_H4a5 (c_keinteractionresourcetestmt)). zenon_intro zenon_H4a6. % 0.99/1.20 apply (zenon_imply_s _ _ zenon_H4a6); [ zenon_intro zenon_H48d | zenon_intro zenon_H4a7 ]. % 0.99/1.20 exact (zenon_H48d zenon_H49e). % 0.99/1.20 apply (zenon_imply_s _ _ zenon_H4a7); [ zenon_intro zenon_H4a9 | zenon_intro zenon_H4a8 ]. % 0.99/1.20 exact (zenon_H4a9 ax1_310). % 0.99/1.20 exact (zenon_H489 zenon_H4a8). % 0.99/1.20 apply zenon_H4a0. apply refl_equal. % 0.99/1.20 cut ((genlmt (c_keinteractionresourcetestmt) (c_testvocabularymt)) = (genlmt (c_tptp_member3515_mt) (c_testvocabularymt))). % 0.99/1.20 intro zenon_D_pnotp. % 0.99/1.20 apply zenon_H485. % 0.99/1.20 rewrite <- zenon_D_pnotp. % 0.99/1.20 exact ax1_257. % 0.99/1.20 cut (((c_testvocabularymt) = (c_testvocabularymt))); [idtac | apply NNPP; zenon_intro zenon_H4aa]. % 0.99/1.20 cut (((c_keinteractionresourcetestmt) = (c_tptp_member3515_mt))); [idtac | apply NNPP; zenon_intro zenon_H4ab]. % 0.99/1.20 congruence. % 0.99/1.20 apply (zenon_notand_s _ _ zenon_H488); [ zenon_intro zenon_H4ad | zenon_intro zenon_H4ac ]. % 0.99/1.20 apply zenon_H4ad. zenon_intro zenon_H4ae. % 0.99/1.20 elim (classic ((c_tptp_member3515_mt) = (c_tptp_member3515_mt))); [ zenon_intro zenon_H498 | zenon_intro zenon_H499 ]. % 0.99/1.20 cut (((c_tptp_member3515_mt) = (c_tptp_member3515_mt)) = ((c_keinteractionresourcetestmt) = (c_tptp_member3515_mt))). % 0.99/1.20 intro zenon_D_pnotp. % 0.99/1.20 apply zenon_H4ab. % 0.99/1.20 rewrite <- zenon_D_pnotp. % 0.99/1.20 exact zenon_H498. % 0.99/1.20 cut (((c_tptp_member3515_mt) = (c_tptp_member3515_mt))); [idtac | apply NNPP; zenon_intro zenon_H499]. % 0.99/1.20 cut (((c_tptp_member3515_mt) = (c_keinteractionresourcetestmt))); [idtac | apply NNPP; zenon_intro zenon_H48a]. % 0.99/1.20 congruence. % 0.99/1.20 exact (zenon_H48a zenon_H4ae). % 0.99/1.20 apply zenon_H499. apply refl_equal. % 0.99/1.20 apply zenon_H499. apply refl_equal. % 0.99/1.20 apply zenon_H4ac. zenon_intro zenon_H4a8. % 0.99/1.20 generalize (zenon_H452 (c_tptp_member3515_mt)). zenon_intro zenon_H49a. % 0.99/1.20 generalize (zenon_H49a (c_keinteractionresourcetestmt)). zenon_intro zenon_H4af. % 0.99/1.20 generalize (zenon_H4af (c_testvocabularymt)). zenon_intro zenon_H4b0. % 0.99/1.20 apply (zenon_imply_s _ _ zenon_H4b0); [ zenon_intro zenon_H489 | zenon_intro zenon_H4b1 ]. % 0.99/1.20 exact (zenon_H489 zenon_H4a8). % 0.99/1.20 apply (zenon_imply_s _ _ zenon_H4b1); [ zenon_intro zenon_H4b3 | zenon_intro zenon_H4b2 ]. % 0.99/1.20 exact (zenon_H4b3 ax1_257). % 0.99/1.20 exact (zenon_H485 zenon_H4b2). % 0.99/1.20 apply zenon_H4aa. apply refl_equal. % 0.99/1.20 cut ((genlmt (c_testvocabularymt) (c_nooescapearchitecturemt)) = (genlmt (c_tptp_member3515_mt) (c_nooescapearchitecturemt))). % 0.99/1.20 intro zenon_D_pnotp. % 0.99/1.20 apply zenon_H481. % 0.99/1.20 rewrite <- zenon_D_pnotp. % 0.99/1.20 exact ax1_275. % 0.99/1.20 cut (((c_nooescapearchitecturemt) = (c_nooescapearchitecturemt))); [idtac | apply NNPP; zenon_intro zenon_H4b4]. % 0.99/1.20 cut (((c_testvocabularymt) = (c_tptp_member3515_mt))); [idtac | apply NNPP; zenon_intro zenon_H4b5]. % 0.99/1.20 congruence. % 0.99/1.20 apply (zenon_notand_s _ _ zenon_H484); [ zenon_intro zenon_H4b7 | zenon_intro zenon_H4b6 ]. % 0.99/1.20 apply zenon_H4b7. zenon_intro zenon_H4b8. % 0.99/1.20 elim (classic ((c_tptp_member3515_mt) = (c_tptp_member3515_mt))); [ zenon_intro zenon_H498 | zenon_intro zenon_H499 ]. % 0.99/1.20 cut (((c_tptp_member3515_mt) = (c_tptp_member3515_mt)) = ((c_testvocabularymt) = (c_tptp_member3515_mt))). % 0.99/1.20 intro zenon_D_pnotp. % 0.99/1.20 apply zenon_H4b5. % 0.99/1.20 rewrite <- zenon_D_pnotp. % 0.99/1.20 exact zenon_H498. % 0.99/1.20 cut (((c_tptp_member3515_mt) = (c_tptp_member3515_mt))); [idtac | apply NNPP; zenon_intro zenon_H499]. % 0.99/1.20 cut (((c_tptp_member3515_mt) = (c_testvocabularymt))); [idtac | apply NNPP; zenon_intro zenon_H486]. % 0.99/1.20 congruence. % 0.99/1.20 exact (zenon_H486 zenon_H4b8). % 0.99/1.20 apply zenon_H499. apply refl_equal. % 0.99/1.20 apply zenon_H499. apply refl_equal. % 0.99/1.20 apply zenon_H4b6. zenon_intro zenon_H4b2. % 0.99/1.20 generalize (zenon_H452 (c_tptp_member3515_mt)). zenon_intro zenon_H49a. % 0.99/1.20 generalize (zenon_H49a (c_testvocabularymt)). zenon_intro zenon_H4b9. % 0.99/1.20 generalize (zenon_H4b9 (c_nooescapearchitecturemt)). zenon_intro zenon_H4ba. % 0.99/1.20 apply (zenon_imply_s _ _ zenon_H4ba); [ zenon_intro zenon_H485 | zenon_intro zenon_H4bb ]. % 0.99/1.20 exact (zenon_H485 zenon_H4b2). % 0.99/1.20 apply (zenon_imply_s _ _ zenon_H4bb); [ zenon_intro zenon_H4bd | zenon_intro zenon_H4bc ]. % 0.99/1.20 exact (zenon_H4bd ax1_275). % 0.99/1.20 exact (zenon_H481 zenon_H4bc). % 0.99/1.20 apply zenon_H4b4. apply refl_equal. % 0.99/1.20 cut ((genlmt (c_nooescapearchitecturemt) (c_organizationdatamt)) = (genlmt (c_tptp_member3515_mt) (c_organizationdatamt))). % 0.99/1.20 intro zenon_D_pnotp. % 0.99/1.20 apply zenon_H47d. % 0.99/1.20 rewrite <- zenon_D_pnotp. % 0.99/1.20 exact ax1_66. % 0.99/1.20 cut (((c_organizationdatamt) = (c_organizationdatamt))); [idtac | apply NNPP; zenon_intro zenon_H4be]. % 0.99/1.20 cut (((c_nooescapearchitecturemt) = (c_tptp_member3515_mt))); [idtac | apply NNPP; zenon_intro zenon_H4bf]. % 0.99/1.20 congruence. % 0.99/1.20 apply (zenon_notand_s _ _ zenon_H480); [ zenon_intro zenon_H4c1 | zenon_intro zenon_H4c0 ]. % 0.99/1.20 apply zenon_H4c1. zenon_intro zenon_H4c2. % 0.99/1.20 elim (classic ((c_tptp_member3515_mt) = (c_tptp_member3515_mt))); [ zenon_intro zenon_H498 | zenon_intro zenon_H499 ]. % 0.99/1.20 cut (((c_tptp_member3515_mt) = (c_tptp_member3515_mt)) = ((c_nooescapearchitecturemt) = (c_tptp_member3515_mt))). % 0.99/1.20 intro zenon_D_pnotp. % 0.99/1.20 apply zenon_H4bf. % 0.99/1.20 rewrite <- zenon_D_pnotp. % 0.99/1.20 exact zenon_H498. % 0.99/1.20 cut (((c_tptp_member3515_mt) = (c_tptp_member3515_mt))); [idtac | apply NNPP; zenon_intro zenon_H499]. % 0.99/1.20 cut (((c_tptp_member3515_mt) = (c_nooescapearchitecturemt))); [idtac | apply NNPP; zenon_intro zenon_H482]. % 0.99/1.20 congruence. % 0.99/1.20 exact (zenon_H482 zenon_H4c2). % 0.99/1.20 apply zenon_H499. apply refl_equal. % 0.99/1.20 apply zenon_H499. apply refl_equal. % 0.99/1.20 apply zenon_H4c0. zenon_intro zenon_H4bc. % 0.99/1.20 generalize (zenon_H452 (c_tptp_member3515_mt)). zenon_intro zenon_H49a. % 0.99/1.20 generalize (zenon_H49a (c_nooescapearchitecturemt)). zenon_intro zenon_H4c3. % 0.99/1.20 generalize (zenon_H4c3 (c_organizationdatamt)). zenon_intro zenon_H4c4. % 0.99/1.20 apply (zenon_imply_s _ _ zenon_H4c4); [ zenon_intro zenon_H481 | zenon_intro zenon_H4c5 ]. % 0.99/1.20 exact (zenon_H481 zenon_H4bc). % 0.99/1.20 apply (zenon_imply_s _ _ zenon_H4c5); [ zenon_intro zenon_H4c7 | zenon_intro zenon_H4c6 ]. % 0.99/1.20 exact (zenon_H4c7 ax1_66). % 0.99/1.20 exact (zenon_H47d zenon_H4c6). % 0.99/1.20 apply zenon_H4be. apply refl_equal. % 0.99/1.20 cut ((genlmt (c_organizationdatamt) (f_contextofpcwfn (c_ap_martha_stewart_omnimedia_names_chairman))) = (genlmt (c_tptp_member3515_mt) (f_contextofpcwfn (c_ap_martha_stewart_omnimedia_names_chairman)))). % 0.99/1.20 intro zenon_D_pnotp. % 0.99/1.20 apply zenon_H479. % 0.99/1.20 rewrite <- zenon_D_pnotp. % 0.99/1.20 exact ax1_486. % 0.99/1.20 cut (((f_contextofpcwfn (c_ap_martha_stewart_omnimedia_names_chairman)) = (f_contextofpcwfn (c_ap_martha_stewart_omnimedia_names_chairman)))); [idtac | apply NNPP; zenon_intro zenon_H4c8]. % 0.99/1.20 cut (((c_organizationdatamt) = (c_tptp_member3515_mt))); [idtac | apply NNPP; zenon_intro zenon_H4c9]. % 0.99/1.20 congruence. % 0.99/1.20 apply (zenon_notand_s _ _ zenon_H47c); [ zenon_intro zenon_H4cb | zenon_intro zenon_H4ca ]. % 0.99/1.20 apply zenon_H4cb. zenon_intro zenon_H4cc. % 0.99/1.20 elim (classic ((c_tptp_member3515_mt) = (c_tptp_member3515_mt))); [ zenon_intro zenon_H498 | zenon_intro zenon_H499 ]. % 0.99/1.20 cut (((c_tptp_member3515_mt) = (c_tptp_member3515_mt)) = ((c_organizationdatamt) = (c_tptp_member3515_mt))). % 0.99/1.20 intro zenon_D_pnotp. % 0.99/1.20 apply zenon_H4c9. % 0.99/1.20 rewrite <- zenon_D_pnotp. % 0.99/1.20 exact zenon_H498. % 0.99/1.20 cut (((c_tptp_member3515_mt) = (c_tptp_member3515_mt))); [idtac | apply NNPP; zenon_intro zenon_H499]. % 0.99/1.20 cut (((c_tptp_member3515_mt) = (c_organizationdatamt))); [idtac | apply NNPP; zenon_intro zenon_H47e]. % 0.99/1.20 congruence. % 0.99/1.20 exact (zenon_H47e zenon_H4cc). % 0.99/1.20 apply zenon_H499. apply refl_equal. % 0.99/1.20 apply zenon_H499. apply refl_equal. % 0.99/1.20 apply zenon_H4ca. zenon_intro zenon_H4c6. % 0.99/1.20 generalize (zenon_H452 (c_tptp_member3515_mt)). zenon_intro zenon_H49a. % 0.99/1.20 generalize (zenon_H49a (c_organizationdatamt)). zenon_intro zenon_H4cd. % 0.99/1.20 generalize (zenon_H4cd (f_contextofpcwfn (c_ap_martha_stewart_omnimedia_names_chairman))). zenon_intro zenon_H4ce. % 0.99/1.20 apply (zenon_imply_s _ _ zenon_H4ce); [ zenon_intro zenon_H47d | zenon_intro zenon_H4cf ]. % 0.99/1.20 exact (zenon_H47d zenon_H4c6). % 0.99/1.20 apply (zenon_imply_s _ _ zenon_H4cf); [ zenon_intro zenon_H4d1 | zenon_intro zenon_H4d0 ]. % 0.99/1.20 exact (zenon_H4d1 ax1_486). % 0.99/1.20 exact (zenon_H479 zenon_H4d0). % 0.99/1.20 apply zenon_H4c8. apply refl_equal. % 0.99/1.20 cut ((genlmt (f_contextofpcwfn (c_ap_martha_stewart_omnimedia_names_chairman)) (c_massmediadatamt)) = (genlmt (c_tptp_member3515_mt) (c_massmediadatamt))). % 0.99/1.20 intro zenon_D_pnotp. % 0.99/1.20 apply zenon_H475. % 0.99/1.20 rewrite <- zenon_D_pnotp. % 0.99/1.20 exact ax1_232. % 0.99/1.20 cut (((c_massmediadatamt) = (c_massmediadatamt))); [idtac | apply NNPP; zenon_intro zenon_H4d2]. % 0.99/1.20 cut (((f_contextofpcwfn (c_ap_martha_stewart_omnimedia_names_chairman)) = (c_tptp_member3515_mt))); [idtac | apply NNPP; zenon_intro zenon_H4d3]. % 0.99/1.20 congruence. % 0.99/1.20 apply (zenon_notand_s _ _ zenon_H478); [ zenon_intro zenon_H4d5 | zenon_intro zenon_H4d4 ]. % 0.99/1.20 apply zenon_H4d5. zenon_intro zenon_H4d6. % 0.99/1.20 elim (classic ((c_tptp_member3515_mt) = (c_tptp_member3515_mt))); [ zenon_intro zenon_H498 | zenon_intro zenon_H499 ]. % 0.99/1.20 cut (((c_tptp_member3515_mt) = (c_tptp_member3515_mt)) = ((f_contextofpcwfn (c_ap_martha_stewart_omnimedia_names_chairman)) = (c_tptp_member3515_mt))). % 0.99/1.20 intro zenon_D_pnotp. % 0.99/1.20 apply zenon_H4d3. % 0.99/1.20 rewrite <- zenon_D_pnotp. % 0.99/1.20 exact zenon_H498. % 0.99/1.20 cut (((c_tptp_member3515_mt) = (c_tptp_member3515_mt))); [idtac | apply NNPP; zenon_intro zenon_H499]. % 0.99/1.20 cut (((c_tptp_member3515_mt) = (f_contextofpcwfn (c_ap_martha_stewart_omnimedia_names_chairman)))); [idtac | apply NNPP; zenon_intro zenon_H47a]. % 0.99/1.20 congruence. % 0.99/1.20 exact (zenon_H47a zenon_H4d6). % 0.99/1.20 apply zenon_H499. apply refl_equal. % 0.99/1.20 apply zenon_H499. apply refl_equal. % 0.99/1.20 apply zenon_H4d4. zenon_intro zenon_H4d0. % 0.99/1.20 generalize (zenon_H452 (c_tptp_member3515_mt)). zenon_intro zenon_H49a. % 0.99/1.20 generalize (zenon_H49a (f_contextofpcwfn (c_ap_martha_stewart_omnimedia_names_chairman))). zenon_intro zenon_H4d7. % 0.99/1.20 generalize (zenon_H4d7 (c_massmediadatamt)). zenon_intro zenon_H4d8. % 0.99/1.20 apply (zenon_imply_s _ _ zenon_H4d8); [ zenon_intro zenon_H479 | zenon_intro zenon_H4d9 ]. % 0.99/1.20 exact (zenon_H479 zenon_H4d0). % 0.99/1.20 apply (zenon_imply_s _ _ zenon_H4d9); [ zenon_intro zenon_H4db | zenon_intro zenon_H4da ]. % 0.99/1.20 exact (zenon_H4db ax1_232). % 0.99/1.20 exact (zenon_H475 zenon_H4da). % 0.99/1.20 apply zenon_H4d2. apply refl_equal. % 0.99/1.20 cut ((genlmt (c_massmediadatamt) (c_ethnicgroupsmt)) = (genlmt (c_tptp_member3515_mt) (c_ethnicgroupsmt))). % 0.99/1.20 intro zenon_D_pnotp. % 0.99/1.20 apply zenon_H471. % 0.99/1.20 rewrite <- zenon_D_pnotp. % 0.99/1.20 exact ax1_329. % 0.99/1.20 cut (((c_ethnicgroupsmt) = (c_ethnicgroupsmt))); [idtac | apply NNPP; zenon_intro zenon_H4dc]. % 0.99/1.20 cut (((c_massmediadatamt) = (c_tptp_member3515_mt))); [idtac | apply NNPP; zenon_intro zenon_H4dd]. % 0.99/1.20 congruence. % 0.99/1.20 apply (zenon_notand_s _ _ zenon_H474); [ zenon_intro zenon_H4df | zenon_intro zenon_H4de ]. % 0.99/1.20 apply zenon_H4df. zenon_intro zenon_H4e0. % 0.99/1.20 elim (classic ((c_tptp_member3515_mt) = (c_tptp_member3515_mt))); [ zenon_intro zenon_H498 | zenon_intro zenon_H499 ]. % 0.99/1.20 cut (((c_tptp_member3515_mt) = (c_tptp_member3515_mt)) = ((c_massmediadatamt) = (c_tptp_member3515_mt))). % 0.99/1.20 intro zenon_D_pnotp. % 0.99/1.20 apply zenon_H4dd. % 0.99/1.20 rewrite <- zenon_D_pnotp. % 0.99/1.20 exact zenon_H498. % 0.99/1.20 cut (((c_tptp_member3515_mt) = (c_tptp_member3515_mt))); [idtac | apply NNPP; zenon_intro zenon_H499]. % 0.99/1.20 cut (((c_tptp_member3515_mt) = (c_massmediadatamt))); [idtac | apply NNPP; zenon_intro zenon_H476]. % 0.99/1.20 congruence. % 0.99/1.20 exact (zenon_H476 zenon_H4e0). % 0.99/1.20 apply zenon_H499. apply refl_equal. % 0.99/1.20 apply zenon_H499. apply refl_equal. % 0.99/1.20 apply zenon_H4de. zenon_intro zenon_H4da. % 0.99/1.20 generalize (zenon_H452 (c_tptp_member3515_mt)). zenon_intro zenon_H49a. % 0.99/1.20 generalize (zenon_H49a (c_massmediadatamt)). zenon_intro zenon_H4e1. % 0.99/1.20 generalize (zenon_H4e1 (c_ethnicgroupsmt)). zenon_intro zenon_H4e2. % 0.99/1.20 apply (zenon_imply_s _ _ zenon_H4e2); [ zenon_intro zenon_H475 | zenon_intro zenon_H4e3 ]. % 0.99/1.20 exact (zenon_H475 zenon_H4da). % 0.99/1.20 apply (zenon_imply_s _ _ zenon_H4e3); [ zenon_intro zenon_H4e5 | zenon_intro zenon_H4e4 ]. % 0.99/1.20 exact (zenon_H4e5 ax1_329). % 0.99/1.20 exact (zenon_H471 zenon_H4e4). % 0.99/1.20 apply zenon_H4dc. apply refl_equal. % 0.99/1.20 cut ((genlmt (c_ethnicgroupsmt) (c_ethnicgroupsvocabularymt)) = (genlmt (c_tptp_member3515_mt) (c_ethnicgroupsvocabularymt))). % 0.99/1.20 intro zenon_D_pnotp. % 0.99/1.20 apply zenon_H46d. % 0.99/1.20 rewrite <- zenon_D_pnotp. % 0.99/1.20 exact ax1_53. % 0.99/1.20 cut (((c_ethnicgroupsvocabularymt) = (c_ethnicgroupsvocabularymt))); [idtac | apply NNPP; zenon_intro zenon_H4e6]. % 0.99/1.20 cut (((c_ethnicgroupsmt) = (c_tptp_member3515_mt))); [idtac | apply NNPP; zenon_intro zenon_H4e7]. % 0.99/1.20 congruence. % 0.99/1.20 apply (zenon_notand_s _ _ zenon_H470); [ zenon_intro zenon_H4e9 | zenon_intro zenon_H4e8 ]. % 0.99/1.20 apply zenon_H4e9. zenon_intro zenon_H4ea. % 0.99/1.20 elim (classic ((c_tptp_member3515_mt) = (c_tptp_member3515_mt))); [ zenon_intro zenon_H498 | zenon_intro zenon_H499 ]. % 0.99/1.20 cut (((c_tptp_member3515_mt) = (c_tptp_member3515_mt)) = ((c_ethnicgroupsmt) = (c_tptp_member3515_mt))). % 0.99/1.20 intro zenon_D_pnotp. % 0.99/1.20 apply zenon_H4e7. % 0.99/1.20 rewrite <- zenon_D_pnotp. % 0.99/1.20 exact zenon_H498. % 0.99/1.20 cut (((c_tptp_member3515_mt) = (c_tptp_member3515_mt))); [idtac | apply NNPP; zenon_intro zenon_H499]. % 0.99/1.20 cut (((c_tptp_member3515_mt) = (c_ethnicgroupsmt))); [idtac | apply NNPP; zenon_intro zenon_H472]. % 0.99/1.20 congruence. % 0.99/1.20 exact (zenon_H472 zenon_H4ea). % 0.99/1.20 apply zenon_H499. apply refl_equal. % 0.99/1.20 apply zenon_H499. apply refl_equal. % 0.99/1.20 apply zenon_H4e8. zenon_intro zenon_H4e4. % 0.99/1.20 generalize (zenon_H452 (c_tptp_member3515_mt)). zenon_intro zenon_H49a. % 0.99/1.20 generalize (zenon_H49a (c_ethnicgroupsmt)). zenon_intro zenon_H4eb. % 0.99/1.20 generalize (zenon_H4eb (c_ethnicgroupsvocabularymt)). zenon_intro zenon_H4ec. % 0.99/1.20 apply (zenon_imply_s _ _ zenon_H4ec); [ zenon_intro zenon_H471 | zenon_intro zenon_H4ed ]. % 0.99/1.20 exact (zenon_H471 zenon_H4e4). % 0.99/1.20 apply (zenon_imply_s _ _ zenon_H4ed); [ zenon_intro zenon_H4ef | zenon_intro zenon_H4ee ]. % 0.99/1.20 exact (zenon_H4ef ax1_53). % 0.99/1.20 exact (zenon_H46d zenon_H4ee). % 0.99/1.20 apply zenon_H4e6. apply refl_equal. % 0.99/1.20 cut ((genlmt (c_ethnicgroupsvocabularymt) (c_worldcompletedualistgeographymt)) = (genlmt (c_tptp_member3515_mt) (c_worldcompletedualistgeographymt))). % 0.99/1.20 intro zenon_D_pnotp. % 0.99/1.20 apply zenon_H469. % 0.99/1.20 rewrite <- zenon_D_pnotp. % 0.99/1.20 exact ax1_367. % 0.99/1.20 cut (((c_worldcompletedualistgeographymt) = (c_worldcompletedualistgeographymt))); [idtac | apply NNPP; zenon_intro zenon_H4f0]. % 0.99/1.20 cut (((c_ethnicgroupsvocabularymt) = (c_tptp_member3515_mt))); [idtac | apply NNPP; zenon_intro zenon_H4f1]. % 0.99/1.20 congruence. % 0.99/1.20 apply (zenon_notand_s _ _ zenon_H46c); [ zenon_intro zenon_H4f3 | zenon_intro zenon_H4f2 ]. % 0.99/1.20 apply zenon_H4f3. zenon_intro zenon_H4f4. % 0.99/1.20 elim (classic ((c_tptp_member3515_mt) = (c_tptp_member3515_mt))); [ zenon_intro zenon_H498 | zenon_intro zenon_H499 ]. % 0.99/1.20 cut (((c_tptp_member3515_mt) = (c_tptp_member3515_mt)) = ((c_ethnicgroupsvocabularymt) = (c_tptp_member3515_mt))). % 0.99/1.20 intro zenon_D_pnotp. % 0.99/1.20 apply zenon_H4f1. % 0.99/1.20 rewrite <- zenon_D_pnotp. % 0.99/1.20 exact zenon_H498. % 0.99/1.20 cut (((c_tptp_member3515_mt) = (c_tptp_member3515_mt))); [idtac | apply NNPP; zenon_intro zenon_H499]. % 0.99/1.20 cut (((c_tptp_member3515_mt) = (c_ethnicgroupsvocabularymt))); [idtac | apply NNPP; zenon_intro zenon_H46e]. % 0.99/1.20 congruence. % 0.99/1.20 exact (zenon_H46e zenon_H4f4). % 0.99/1.20 apply zenon_H499. apply refl_equal. % 0.99/1.20 apply zenon_H499. apply refl_equal. % 0.99/1.20 apply zenon_H4f2. zenon_intro zenon_H4ee. % 0.99/1.20 generalize (zenon_H452 (c_tptp_member3515_mt)). zenon_intro zenon_H49a. % 0.99/1.20 generalize (zenon_H49a (c_ethnicgroupsvocabularymt)). zenon_intro zenon_H4f5. % 0.99/1.20 generalize (zenon_H4f5 (c_worldcompletedualistgeographymt)). zenon_intro zenon_H4f6. % 0.99/1.20 apply (zenon_imply_s _ _ zenon_H4f6); [ zenon_intro zenon_H46d | zenon_intro zenon_H4f7 ]. % 0.99/1.20 exact (zenon_H46d zenon_H4ee). % 0.99/1.20 apply (zenon_imply_s _ _ zenon_H4f7); [ zenon_intro zenon_H4f9 | zenon_intro zenon_H4f8 ]. % 0.99/1.20 exact (zenon_H4f9 ax1_367). % 0.99/1.20 exact (zenon_H469 zenon_H4f8). % 0.99/1.20 apply zenon_H4f0. apply refl_equal. % 0.99/1.20 cut ((genlmt (c_worldcompletedualistgeographymt) (c_unitedstatesgeographydualistmt)) = (genlmt (c_tptp_member3515_mt) (c_unitedstatesgeographydualistmt))). % 0.99/1.20 intro zenon_D_pnotp. % 0.99/1.20 apply zenon_H465. % 0.99/1.20 rewrite <- zenon_D_pnotp. % 0.99/1.20 exact ax1_339. % 0.99/1.20 cut (((c_unitedstatesgeographydualistmt) = (c_unitedstatesgeographydualistmt))); [idtac | apply NNPP; zenon_intro zenon_H4fa]. % 0.99/1.20 cut (((c_worldcompletedualistgeographymt) = (c_tptp_member3515_mt))); [idtac | apply NNPP; zenon_intro zenon_H4fb]. % 0.99/1.20 congruence. % 0.99/1.20 apply (zenon_notand_s _ _ zenon_H468); [ zenon_intro zenon_H4fd | zenon_intro zenon_H4fc ]. % 0.99/1.20 apply zenon_H4fd. zenon_intro zenon_H4fe. % 0.99/1.20 elim (classic ((c_tptp_member3515_mt) = (c_tptp_member3515_mt))); [ zenon_intro zenon_H498 | zenon_intro zenon_H499 ]. % 0.99/1.20 cut (((c_tptp_member3515_mt) = (c_tptp_member3515_mt)) = ((c_worldcompletedualistgeographymt) = (c_tptp_member3515_mt))). % 0.99/1.20 intro zenon_D_pnotp. % 0.99/1.20 apply zenon_H4fb. % 0.99/1.20 rewrite <- zenon_D_pnotp. % 0.99/1.20 exact zenon_H498. % 0.99/1.20 cut (((c_tptp_member3515_mt) = (c_tptp_member3515_mt))); [idtac | apply NNPP; zenon_intro zenon_H499]. % 0.99/1.20 cut (((c_tptp_member3515_mt) = (c_worldcompletedualistgeographymt))); [idtac | apply NNPP; zenon_intro zenon_H46a]. % 0.99/1.20 congruence. % 0.99/1.20 exact (zenon_H46a zenon_H4fe). % 0.99/1.20 apply zenon_H499. apply refl_equal. % 0.99/1.20 apply zenon_H499. apply refl_equal. % 0.99/1.20 apply zenon_H4fc. zenon_intro zenon_H4f8. % 0.99/1.20 generalize (zenon_H452 (c_tptp_member3515_mt)). zenon_intro zenon_H49a. % 0.99/1.20 generalize (zenon_H49a (c_worldcompletedualistgeographymt)). zenon_intro zenon_H4ff. % 0.99/1.20 generalize (zenon_H4ff (c_unitedstatesgeographydualistmt)). zenon_intro zenon_H500. % 0.99/1.20 apply (zenon_imply_s _ _ zenon_H500); [ zenon_intro zenon_H469 | zenon_intro zenon_H501 ]. % 0.99/1.20 exact (zenon_H469 zenon_H4f8). % 0.99/1.20 apply (zenon_imply_s _ _ zenon_H501); [ zenon_intro zenon_H503 | zenon_intro zenon_H502 ]. % 0.99/1.20 exact (zenon_H503 ax1_339). % 0.99/1.20 exact (zenon_H465 zenon_H502). % 0.99/1.20 apply zenon_H4fa. apply refl_equal. % 0.99/1.20 cut ((genlmt (c_unitedstatesgeographydualistmt) (c_worldgeographydualistmt)) = (genlmt (c_tptp_member3515_mt) (c_worldgeographydualistmt))). % 0.99/1.20 intro zenon_D_pnotp. % 0.99/1.20 apply zenon_H461. % 0.99/1.20 rewrite <- zenon_D_pnotp. % 0.99/1.20 exact ax1_454. % 0.99/1.20 cut (((c_worldgeographydualistmt) = (c_worldgeographydualistmt))); [idtac | apply NNPP; zenon_intro zenon_H504]. % 0.99/1.20 cut (((c_unitedstatesgeographydualistmt) = (c_tptp_member3515_mt))); [idtac | apply NNPP; zenon_intro zenon_H505]. % 0.99/1.20 congruence. % 0.99/1.20 apply (zenon_notand_s _ _ zenon_H464); [ zenon_intro zenon_H507 | zenon_intro zenon_H506 ]. % 0.99/1.20 apply zenon_H507. zenon_intro zenon_H508. % 0.99/1.20 elim (classic ((c_tptp_member3515_mt) = (c_tptp_member3515_mt))); [ zenon_intro zenon_H498 | zenon_intro zenon_H499 ]. % 0.99/1.20 cut (((c_tptp_member3515_mt) = (c_tptp_member3515_mt)) = ((c_unitedstatesgeographydualistmt) = (c_tptp_member3515_mt))). % 0.99/1.20 intro zenon_D_pnotp. % 0.99/1.20 apply zenon_H505. % 0.99/1.20 rewrite <- zenon_D_pnotp. % 0.99/1.20 exact zenon_H498. % 0.99/1.20 cut (((c_tptp_member3515_mt) = (c_tptp_member3515_mt))); [idtac | apply NNPP; zenon_intro zenon_H499]. % 0.99/1.20 cut (((c_tptp_member3515_mt) = (c_unitedstatesgeographydualistmt))); [idtac | apply NNPP; zenon_intro zenon_H466]. % 0.99/1.20 congruence. % 0.99/1.20 exact (zenon_H466 zenon_H508). % 0.99/1.20 apply zenon_H499. apply refl_equal. % 0.99/1.20 apply zenon_H499. apply refl_equal. % 0.99/1.20 apply zenon_H506. zenon_intro zenon_H502. % 0.99/1.20 generalize (zenon_H452 (c_tptp_member3515_mt)). zenon_intro zenon_H49a. % 0.99/1.20 generalize (zenon_H49a (c_unitedstatesgeographydualistmt)). zenon_intro zenon_H509. % 0.99/1.20 generalize (zenon_H509 (c_worldgeographydualistmt)). zenon_intro zenon_H50a. % 0.99/1.20 apply (zenon_imply_s _ _ zenon_H50a); [ zenon_intro zenon_H465 | zenon_intro zenon_H50b ]. % 0.99/1.20 exact (zenon_H465 zenon_H502). % 0.99/1.20 apply (zenon_imply_s _ _ zenon_H50b); [ zenon_intro zenon_H50d | zenon_intro zenon_H50c ]. % 0.99/1.20 exact (zenon_H50d ax1_454). % 0.99/1.20 exact (zenon_H461 zenon_H50c). % 0.99/1.20 apply zenon_H504. apply refl_equal. % 0.99/1.20 cut ((genlmt (c_worldgeographydualistmt) (c_worldgeographymt)) = (genlmt (c_tptp_member3515_mt) (c_worldgeographymt))). % 0.99/1.20 intro zenon_D_pnotp. % 0.99/1.20 apply zenon_H45d. % 0.99/1.20 rewrite <- zenon_D_pnotp. % 0.99/1.20 exact ax1_137. % 0.99/1.20 cut (((c_worldgeographymt) = (c_worldgeographymt))); [idtac | apply NNPP; zenon_intro zenon_H451]. % 0.99/1.20 cut (((c_worldgeographydualistmt) = (c_tptp_member3515_mt))); [idtac | apply NNPP; zenon_intro zenon_H50e]. % 0.99/1.20 congruence. % 0.99/1.20 apply (zenon_notand_s _ _ zenon_H460); [ zenon_intro zenon_H510 | zenon_intro zenon_H50f ]. % 0.99/1.20 apply zenon_H510. zenon_intro zenon_H511. % 0.99/1.20 elim (classic ((c_tptp_member3515_mt) = (c_tptp_member3515_mt))); [ zenon_intro zenon_H498 | zenon_intro zenon_H499 ]. % 0.99/1.20 cut (((c_tptp_member3515_mt) = (c_tptp_member3515_mt)) = ((c_worldgeographydualistmt) = (c_tptp_member3515_mt))). % 0.99/1.20 intro zenon_D_pnotp. % 0.99/1.20 apply zenon_H50e. % 0.99/1.20 rewrite <- zenon_D_pnotp. % 0.99/1.20 exact zenon_H498. % 0.99/1.20 cut (((c_tptp_member3515_mt) = (c_tptp_member3515_mt))); [idtac | apply NNPP; zenon_intro zenon_H499]. % 0.99/1.20 cut (((c_tptp_member3515_mt) = (c_worldgeographydualistmt))); [idtac | apply NNPP; zenon_intro zenon_H462]. % 0.99/1.20 congruence. % 0.99/1.20 exact (zenon_H462 zenon_H511). % 0.99/1.20 apply zenon_H499. apply refl_equal. % 0.99/1.20 apply zenon_H499. apply refl_equal. % 0.99/1.20 apply zenon_H50f. zenon_intro zenon_H50c. % 0.99/1.20 generalize (zenon_H452 (c_tptp_member3515_mt)). zenon_intro zenon_H49a. % 0.99/1.20 generalize (zenon_H49a (c_worldgeographydualistmt)). zenon_intro zenon_H512. % 0.99/1.20 generalize (zenon_H512 (c_worldgeographymt)). zenon_intro zenon_H513. % 0.99/1.20 apply (zenon_imply_s _ _ zenon_H513); [ zenon_intro zenon_H461 | zenon_intro zenon_H514 ]. % 0.99/1.20 exact (zenon_H461 zenon_H50c). % 0.99/1.20 apply (zenon_imply_s _ _ zenon_H514); [ zenon_intro zenon_H516 | zenon_intro zenon_H515 ]. % 0.99/1.20 exact (zenon_H516 ax1_137). % 0.99/1.20 exact (zenon_H45d zenon_H515). % 0.99/1.20 apply zenon_H451. apply refl_equal. % 0.99/1.20 exact (zenon_H455 zenon_H45b). % 0.99/1.20 apply zenon_G. exists (c_state_geopolitical). apply NNPP. zenon_intro zenon_H517. % 0.99/1.20 apply (zenon_notimply_s _ _ zenon_H517). zenon_intro zenon_H458. zenon_intro zenon_H518. % 0.99/1.20 generalize (ax1_629 (c_wanica_districtsuriname)). zenon_intro zenon_H519. % 0.99/1.20 apply (zenon_imply_s _ _ zenon_H519); [ zenon_intro zenon_H51b | zenon_intro zenon_H51a ]. % 0.99/1.20 exact (zenon_H51b zenon_H454). % 0.99/1.20 exact (zenon_H518 zenon_H51a). % 0.99/1.20 apply zenon_H453. zenon_intro zenon_Tx_byi. apply NNPP. zenon_intro zenon_H51d. % 0.99/1.20 apply zenon_H51d. zenon_intro zenon_Ty_byk. apply NNPP. zenon_intro zenon_H51f. % 0.99/1.20 apply zenon_H51f. zenon_intro zenon_Tz_bym. apply NNPP. zenon_intro zenon_H521. % 0.99/1.20 apply (zenon_notimply_s _ _ zenon_H521). zenon_intro zenon_H523. zenon_intro zenon_H522. % 0.99/1.20 apply (zenon_notimply_s _ _ zenon_H522). zenon_intro zenon_H525. zenon_intro zenon_H524. % 0.99/1.20 generalize (ax1_1128 zenon_Tx_byi). zenon_intro zenon_H526. % 0.99/1.20 generalize (zenon_H526 zenon_Ty_byk). zenon_intro zenon_H527. % 0.99/1.20 generalize (zenon_H527 zenon_Tz_bym). zenon_intro zenon_H528. % 0.99/1.20 apply (zenon_imply_s _ _ zenon_H528); [ zenon_intro zenon_H52a | zenon_intro zenon_H529 ]. % 0.99/1.20 apply (zenon_notand_s _ _ zenon_H52a); [ zenon_intro zenon_H52c | zenon_intro zenon_H52b ]. % 0.99/1.20 exact (zenon_H52c zenon_H523). % 0.99/1.20 exact (zenon_H52b zenon_H525). % 0.99/1.20 exact (zenon_H524 zenon_H529). % 0.99/1.20 Qed. % 0.99/1.20 % SZS output end Proof % 0.99/1.20 (* END-PROOF *) % 0.99/1.20 nodes searched: 12796 % 0.99/1.20 max branch formulas: 6786 % 0.99/1.20 proof nodes created: 837 % 0.99/1.20 formulas created: 140552 % 0.99/1.20 %------------------------------------------------------------------------------