%------------------------------------------------------------------------------ % File : Zenon---0.7.1 % Problem : CSR033+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:53 EDT 2022 % Result : Theorem 8.01s 8.19s % Output : Proof 8.01s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.12 % Problem : CSR033+2 : TPTP v8.1.0. Released v3.4.0. % 0.07/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 07:41:07 EDT 2022 % 0.13/0.34 % CPUTime : % 8.01/8.19 (* PROOF-FOUND *) % 8.01/8.19 % SZS status Theorem % 8.01/8.19 (* BEGIN-PROOF *) % 8.01/8.19 % SZS output start Proof % 8.01/8.19 Theorem query83 : ((mtvisible (c_tptpgeo_spindlecollectormt))->((inregion (c_geolocation_x76_y23) (c_georegion_l1_x2_y0))/\(geolevel_1 (c_georegion_l1_x2_y0)))). % 8.01/8.19 Proof. % 8.01/8.19 assert (zenon_L1_ : (~(mtvisible (c_tptpgeo_member2_mt))) -> (mtvisible (c_tptpgeo_spindlecollectormt)) -> False). % 8.01/8.19 do 0 intro. intros zenon_H450 zenon_H451. % 8.01/8.19 generalize (ax1_1123 (c_tptpgeo_spindlecollectormt)). zenon_intro zenon_H452. % 8.01/8.19 generalize (zenon_H452 (c_tptpgeo_member2_mt)). zenon_intro zenon_H453. % 8.01/8.19 apply (zenon_imply_s _ _ zenon_H453); [ zenon_intro zenon_H455 | zenon_intro zenon_H454 ]. % 8.01/8.19 apply (zenon_notand_s _ _ zenon_H455); [ zenon_intro zenon_H457 | zenon_intro zenon_H456 ]. % 8.01/8.19 exact (zenon_H457 zenon_H451). % 8.01/8.19 exact (zenon_H456 ax1_273). % 8.01/8.19 exact (zenon_H450 zenon_H454). % 8.01/8.19 (* end of lemma zenon_L1_ *) % 8.01/8.19 assert (zenon_L2_ : (~((c_georegion_l3_x25_y7) = (c_georegion_l3_x25_y7))) -> False). % 8.01/8.19 do 0 intro. intros zenon_H458. % 8.01/8.19 apply zenon_H458. apply refl_equal. % 8.01/8.19 (* end of lemma zenon_L2_ *) % 8.01/8.19 assert (zenon_L3_ : (~((c_georegion_l4_x76_y23) = (c_georegion_l4_x76_y23))) -> False). % 8.01/8.19 do 0 intro. intros zenon_H459. % 8.01/8.19 apply zenon_H459. apply refl_equal. % 8.01/8.19 (* end of lemma zenon_L3_ *) % 8.01/8.19 assert (zenon_L4_ : (~((c_tptpgeo_spindleheadmt) = (c_tptpgeo_spindleheadmt))) -> False). % 8.01/8.19 do 0 intro. intros zenon_H45a. % 8.01/8.19 apply zenon_H45a. apply refl_equal. % 8.01/8.19 (* end of lemma zenon_L4_ *) % 8.01/8.19 apply NNPP. intro zenon_G. % 8.01/8.19 elim (classic (forall x : zenon_U, (forall y : zenon_U, (forall z : zenon_U, ((geographicalsubregions x y)->((geographicalsubregions y z)->(geographicalsubregions x z))))))); [ zenon_intro zenon_H45b | zenon_intro zenon_H45c ]. % 8.01/8.19 elim (classic (forall x : zenon_U, (forall y : zenon_U, (forall z : zenon_U, ((inregion x y)->((inregion y z)->(inregion x z))))))); [ zenon_intro zenon_H45d | zenon_intro zenon_H45e ]. % 8.01/8.19 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_H45f | zenon_intro zenon_H460 ]. % 8.01/8.19 apply (zenon_notimply_s _ _ zenon_G). zenon_intro zenon_H451. zenon_intro zenon_H461. % 8.01/8.19 apply (zenon_notand_s _ _ zenon_H461); [ zenon_intro zenon_H463 | zenon_intro zenon_H462 ]. % 8.01/8.19 apply (zenon_imply_s _ _ ax1_18); [ zenon_intro zenon_H450 | zenon_intro zenon_H464 ]. % 8.01/8.19 apply (zenon_L1_); trivial. % 8.01/8.19 apply (zenon_imply_s _ _ ax1_291); [ zenon_intro zenon_H450 | zenon_intro zenon_H465 ]. % 8.01/8.19 apply (zenon_L1_); trivial. % 8.01/8.19 apply (zenon_imply_s _ _ ax1_300); [ zenon_intro zenon_H450 | zenon_intro zenon_H466 ]. % 8.01/8.19 apply (zenon_L1_); trivial. % 8.01/8.19 apply (zenon_imply_s _ _ ax1_355); [ zenon_intro zenon_H450 | zenon_intro zenon_H467 ]. % 8.01/8.19 apply (zenon_L1_); trivial. % 8.01/8.19 elim (classic (inregion (c_georegion_l4_x76_y23) (c_georegion_l1_x2_y0))); [ zenon_intro zenon_H468 | zenon_intro zenon_H469 ]. % 8.01/8.19 generalize (zenon_H45d (c_geolocation_x76_y23)). zenon_intro zenon_H46a. % 8.01/8.19 generalize (zenon_H46a (c_georegion_l4_x76_y23)). zenon_intro zenon_H46b. % 8.01/8.19 generalize (zenon_H46b (c_georegion_l1_x2_y0)). zenon_intro zenon_H46c. % 8.01/8.19 apply (zenon_imply_s _ _ zenon_H46c); [ zenon_intro zenon_H46e | zenon_intro zenon_H46d ]. % 8.01/8.19 exact (zenon_H46e zenon_H467). % 8.01/8.19 apply (zenon_imply_s _ _ zenon_H46d); [ zenon_intro zenon_H469 | zenon_intro zenon_H46f ]. % 8.01/8.19 exact (zenon_H469 zenon_H468). % 8.01/8.19 exact (zenon_H463 zenon_H46f). % 8.01/8.19 generalize (ax1_128 (c_georegion_l1_x2_y0)). zenon_intro zenon_H470. % 8.01/8.19 generalize (zenon_H470 (c_georegion_l4_x76_y23)). zenon_intro zenon_H471. % 8.01/8.19 apply (zenon_imply_s _ _ zenon_H471); [ zenon_intro zenon_H472 | zenon_intro zenon_H468 ]. % 8.01/8.19 elim (classic ((~((c_georegion_l1_x2_y0) = (c_georegion_l3_x25_y7)))/\(~(geographicalsubregions (c_georegion_l1_x2_y0) (c_georegion_l3_x25_y7))))); [ zenon_intro zenon_H473 | zenon_intro zenon_H474 ]. % 8.01/8.19 apply (zenon_and_s _ _ zenon_H473). zenon_intro zenon_H476. zenon_intro zenon_H475. % 8.01/8.19 elim (classic ((~((c_georegion_l1_x2_y0) = (c_georegion_l2_x8_y2)))/\(~(geographicalsubregions (c_georegion_l1_x2_y0) (c_georegion_l2_x8_y2))))); [ zenon_intro zenon_H477 | zenon_intro zenon_H478 ]. % 8.01/8.19 apply (zenon_and_s _ _ zenon_H477). zenon_intro zenon_H47a. zenon_intro zenon_H479. % 8.01/8.19 exact (zenon_H479 zenon_H464). % 8.01/8.19 cut ((geographicalsubregions (c_georegion_l2_x8_y2) (c_georegion_l3_x25_y7)) = (geographicalsubregions (c_georegion_l1_x2_y0) (c_georegion_l3_x25_y7))). % 8.01/8.19 intro zenon_D_pnotp. % 8.01/8.19 apply zenon_H475. % 8.01/8.19 rewrite <- zenon_D_pnotp. % 8.01/8.19 exact zenon_H465. % 8.01/8.19 cut (((c_georegion_l3_x25_y7) = (c_georegion_l3_x25_y7))); [idtac | apply NNPP; zenon_intro zenon_H458]. % 8.01/8.19 cut (((c_georegion_l2_x8_y2) = (c_georegion_l1_x2_y0))); [idtac | apply NNPP; zenon_intro zenon_H47b]. % 8.01/8.19 congruence. % 8.01/8.19 apply (zenon_notand_s _ _ zenon_H478); [ zenon_intro zenon_H47d | zenon_intro zenon_H47c ]. % 8.01/8.19 apply zenon_H47d. zenon_intro zenon_H47e. % 8.01/8.19 elim (classic ((c_georegion_l1_x2_y0) = (c_georegion_l1_x2_y0))); [ zenon_intro zenon_H47f | zenon_intro zenon_H480 ]. % 8.01/8.19 cut (((c_georegion_l1_x2_y0) = (c_georegion_l1_x2_y0)) = ((c_georegion_l2_x8_y2) = (c_georegion_l1_x2_y0))). % 8.01/8.19 intro zenon_D_pnotp. % 8.01/8.19 apply zenon_H47b. % 8.01/8.19 rewrite <- zenon_D_pnotp. % 8.01/8.19 exact zenon_H47f. % 8.01/8.19 cut (((c_georegion_l1_x2_y0) = (c_georegion_l1_x2_y0))); [idtac | apply NNPP; zenon_intro zenon_H480]. % 8.01/8.19 cut (((c_georegion_l1_x2_y0) = (c_georegion_l2_x8_y2))); [idtac | apply NNPP; zenon_intro zenon_H47a]. % 8.01/8.19 congruence. % 8.01/8.19 exact (zenon_H47a zenon_H47e). % 8.01/8.19 apply zenon_H480. apply refl_equal. % 8.01/8.19 apply zenon_H480. apply refl_equal. % 8.01/8.19 apply zenon_H47c. zenon_intro zenon_H464. % 8.01/8.19 generalize (zenon_H45b (c_georegion_l1_x2_y0)). zenon_intro zenon_H481. % 8.01/8.19 generalize (zenon_H481 (c_georegion_l2_x8_y2)). zenon_intro zenon_H482. % 8.01/8.19 generalize (zenon_H482 (c_georegion_l3_x25_y7)). zenon_intro zenon_H483. % 8.01/8.19 apply (zenon_imply_s _ _ zenon_H483); [ zenon_intro zenon_H479 | zenon_intro zenon_H484 ]. % 8.01/8.19 exact (zenon_H479 zenon_H464). % 8.01/8.19 apply (zenon_imply_s _ _ zenon_H484); [ zenon_intro zenon_H486 | zenon_intro zenon_H485 ]. % 8.01/8.19 exact (zenon_H486 zenon_H465). % 8.01/8.19 exact (zenon_H475 zenon_H485). % 8.01/8.19 apply zenon_H458. apply refl_equal. % 8.01/8.19 cut ((geographicalsubregions (c_georegion_l3_x25_y7) (c_georegion_l4_x76_y23)) = (geographicalsubregions (c_georegion_l1_x2_y0) (c_georegion_l4_x76_y23))). % 8.01/8.19 intro zenon_D_pnotp. % 8.01/8.19 apply zenon_H472. % 8.01/8.19 rewrite <- zenon_D_pnotp. % 8.01/8.19 exact zenon_H466. % 8.01/8.19 cut (((c_georegion_l4_x76_y23) = (c_georegion_l4_x76_y23))); [idtac | apply NNPP; zenon_intro zenon_H459]. % 8.01/8.19 cut (((c_georegion_l3_x25_y7) = (c_georegion_l1_x2_y0))); [idtac | apply NNPP; zenon_intro zenon_H487]. % 8.01/8.19 congruence. % 8.01/8.19 apply (zenon_notand_s _ _ zenon_H474); [ zenon_intro zenon_H489 | zenon_intro zenon_H488 ]. % 8.01/8.19 apply zenon_H489. zenon_intro zenon_H48a. % 8.01/8.19 elim (classic ((c_georegion_l1_x2_y0) = (c_georegion_l1_x2_y0))); [ zenon_intro zenon_H47f | zenon_intro zenon_H480 ]. % 8.01/8.19 cut (((c_georegion_l1_x2_y0) = (c_georegion_l1_x2_y0)) = ((c_georegion_l3_x25_y7) = (c_georegion_l1_x2_y0))). % 8.01/8.19 intro zenon_D_pnotp. % 8.01/8.19 apply zenon_H487. % 8.01/8.19 rewrite <- zenon_D_pnotp. % 8.01/8.19 exact zenon_H47f. % 8.01/8.19 cut (((c_georegion_l1_x2_y0) = (c_georegion_l1_x2_y0))); [idtac | apply NNPP; zenon_intro zenon_H480]. % 8.01/8.19 cut (((c_georegion_l1_x2_y0) = (c_georegion_l3_x25_y7))); [idtac | apply NNPP; zenon_intro zenon_H476]. % 8.01/8.19 congruence. % 8.01/8.19 exact (zenon_H476 zenon_H48a). % 8.01/8.19 apply zenon_H480. apply refl_equal. % 8.01/8.19 apply zenon_H480. apply refl_equal. % 8.01/8.19 apply zenon_H488. zenon_intro zenon_H485. % 8.01/8.19 generalize (zenon_H45b (c_georegion_l1_x2_y0)). zenon_intro zenon_H481. % 8.01/8.19 generalize (zenon_H481 (c_georegion_l3_x25_y7)). zenon_intro zenon_H48b. % 8.01/8.19 generalize (zenon_H48b (c_georegion_l4_x76_y23)). zenon_intro zenon_H48c. % 8.01/8.19 apply (zenon_imply_s _ _ zenon_H48c); [ zenon_intro zenon_H475 | zenon_intro zenon_H48d ]. % 8.01/8.19 exact (zenon_H475 zenon_H485). % 8.01/8.19 apply (zenon_imply_s _ _ zenon_H48d); [ zenon_intro zenon_H48f | zenon_intro zenon_H48e ]. % 8.01/8.19 exact (zenon_H48f zenon_H466). % 8.01/8.19 exact (zenon_H472 zenon_H48e). % 8.01/8.19 apply zenon_H459. apply refl_equal. % 8.01/8.19 exact (zenon_H469 zenon_H468). % 8.01/8.19 apply (zenon_imply_s _ _ ax1_292); [ zenon_intro zenon_H491 | zenon_intro zenon_H490 ]. % 8.01/8.19 generalize (ax1_1123 (c_tptpgeo_spindlecollectormt)). zenon_intro zenon_H452. % 8.01/8.19 generalize (zenon_H452 (c_worldgeographymt)). zenon_intro zenon_H492. % 8.01/8.19 apply (zenon_imply_s _ _ zenon_H492); [ zenon_intro zenon_H494 | zenon_intro zenon_H493 ]. % 8.01/8.19 apply (zenon_notand_s _ _ zenon_H494); [ zenon_intro zenon_H457 | zenon_intro zenon_H495 ]. % 8.01/8.19 exact (zenon_H457 zenon_H451). % 8.01/8.19 elim (classic ((~((c_tptpgeo_spindlecollectormt) = (c_tptpgeo_spindleheadmt)))/\(~(genlmt (c_tptpgeo_spindlecollectormt) (c_tptpgeo_spindleheadmt))))); [ zenon_intro zenon_H496 | zenon_intro zenon_H497 ]. % 8.01/8.19 apply (zenon_and_s _ _ zenon_H496). zenon_intro zenon_H499. zenon_intro zenon_H498. % 8.01/8.19 elim (classic ((~((c_tptpgeo_spindlecollectormt) = (c_tptpgeo_member8_mt)))/\(~(genlmt (c_tptpgeo_spindlecollectormt) (c_tptpgeo_member8_mt))))); [ zenon_intro zenon_H49a | zenon_intro zenon_H49b ]. % 8.01/8.19 apply (zenon_and_s _ _ zenon_H49a). zenon_intro zenon_H49d. zenon_intro zenon_H49c. % 8.01/8.19 exact (zenon_H49c ax1_369). % 8.01/8.19 cut ((genlmt (c_tptpgeo_member8_mt) (c_tptpgeo_spindleheadmt)) = (genlmt (c_tptpgeo_spindlecollectormt) (c_tptpgeo_spindleheadmt))). % 8.01/8.19 intro zenon_D_pnotp. % 8.01/8.19 apply zenon_H498. % 8.01/8.19 rewrite <- zenon_D_pnotp. % 8.01/8.19 exact ax1_1. % 8.01/8.19 cut (((c_tptpgeo_spindleheadmt) = (c_tptpgeo_spindleheadmt))); [idtac | apply NNPP; zenon_intro zenon_H45a]. % 8.01/8.19 cut (((c_tptpgeo_member8_mt) = (c_tptpgeo_spindlecollectormt))); [idtac | apply NNPP; zenon_intro zenon_H49e]. % 8.01/8.19 congruence. % 8.01/8.19 apply (zenon_notand_s _ _ zenon_H49b); [ zenon_intro zenon_H4a0 | zenon_intro zenon_H49f ]. % 8.01/8.19 apply zenon_H4a0. zenon_intro zenon_H4a1. % 8.01/8.19 elim (classic ((c_tptpgeo_spindlecollectormt) = (c_tptpgeo_spindlecollectormt))); [ zenon_intro zenon_H4a2 | zenon_intro zenon_H4a3 ]. % 8.01/8.19 cut (((c_tptpgeo_spindlecollectormt) = (c_tptpgeo_spindlecollectormt)) = ((c_tptpgeo_member8_mt) = (c_tptpgeo_spindlecollectormt))). % 8.01/8.19 intro zenon_D_pnotp. % 8.01/8.19 apply zenon_H49e. % 8.01/8.19 rewrite <- zenon_D_pnotp. % 8.01/8.19 exact zenon_H4a2. % 8.01/8.19 cut (((c_tptpgeo_spindlecollectormt) = (c_tptpgeo_spindlecollectormt))); [idtac | apply NNPP; zenon_intro zenon_H4a3]. % 8.01/8.19 cut (((c_tptpgeo_spindlecollectormt) = (c_tptpgeo_member8_mt))); [idtac | apply NNPP; zenon_intro zenon_H49d]. % 8.01/8.19 congruence. % 8.01/8.19 exact (zenon_H49d zenon_H4a1). % 8.01/8.19 apply zenon_H4a3. apply refl_equal. % 8.01/8.19 apply zenon_H4a3. apply refl_equal. % 8.01/8.19 apply zenon_H49f. zenon_intro ax1_369. % 8.01/8.19 generalize (zenon_H45f (c_tptpgeo_spindlecollectormt)). zenon_intro zenon_H4a4. % 8.01/8.19 generalize (zenon_H4a4 (c_tptpgeo_member8_mt)). zenon_intro zenon_H4a5. % 8.01/8.19 generalize (zenon_H4a5 (c_tptpgeo_spindleheadmt)). zenon_intro zenon_H4a6. % 8.01/8.19 apply (zenon_imply_s _ _ zenon_H4a6); [ zenon_intro zenon_H49c | zenon_intro zenon_H4a7 ]. % 8.01/8.19 exact (zenon_H49c ax1_369). % 8.01/8.19 apply (zenon_imply_s _ _ zenon_H4a7); [ zenon_intro zenon_H4a9 | zenon_intro zenon_H4a8 ]. % 8.01/8.19 exact (zenon_H4a9 ax1_1). % 8.01/8.19 exact (zenon_H498 zenon_H4a8). % 8.01/8.19 apply zenon_H45a. apply refl_equal. % 8.01/8.19 cut ((genlmt (c_tptpgeo_spindleheadmt) (c_worldgeographymt)) = (genlmt (c_tptpgeo_spindlecollectormt) (c_worldgeographymt))). % 8.01/8.19 intro zenon_D_pnotp. % 8.01/8.19 apply zenon_H495. % 8.01/8.19 rewrite <- zenon_D_pnotp. % 8.01/8.19 exact ax1_326. % 8.01/8.19 cut (((c_worldgeographymt) = (c_worldgeographymt))); [idtac | apply NNPP; zenon_intro zenon_H4aa]. % 8.01/8.19 cut (((c_tptpgeo_spindleheadmt) = (c_tptpgeo_spindlecollectormt))); [idtac | apply NNPP; zenon_intro zenon_H4ab]. % 8.01/8.19 congruence. % 8.01/8.19 apply (zenon_notand_s _ _ zenon_H497); [ zenon_intro zenon_H4ad | zenon_intro zenon_H4ac ]. % 8.01/8.19 apply zenon_H4ad. zenon_intro zenon_H4ae. % 8.01/8.19 elim (classic ((c_tptpgeo_spindlecollectormt) = (c_tptpgeo_spindlecollectormt))); [ zenon_intro zenon_H4a2 | zenon_intro zenon_H4a3 ]. % 8.01/8.19 cut (((c_tptpgeo_spindlecollectormt) = (c_tptpgeo_spindlecollectormt)) = ((c_tptpgeo_spindleheadmt) = (c_tptpgeo_spindlecollectormt))). % 8.01/8.19 intro zenon_D_pnotp. % 8.01/8.19 apply zenon_H4ab. % 8.01/8.19 rewrite <- zenon_D_pnotp. % 8.01/8.19 exact zenon_H4a2. % 8.01/8.19 cut (((c_tptpgeo_spindlecollectormt) = (c_tptpgeo_spindlecollectormt))); [idtac | apply NNPP; zenon_intro zenon_H4a3]. % 8.01/8.19 cut (((c_tptpgeo_spindlecollectormt) = (c_tptpgeo_spindleheadmt))); [idtac | apply NNPP; zenon_intro zenon_H499]. % 8.01/8.19 congruence. % 8.01/8.19 exact (zenon_H499 zenon_H4ae). % 8.01/8.19 apply zenon_H4a3. apply refl_equal. % 8.01/8.19 apply zenon_H4a3. apply refl_equal. % 8.01/8.19 apply zenon_H4ac. zenon_intro zenon_H4a8. % 8.01/8.19 generalize (zenon_H45f (c_tptpgeo_spindlecollectormt)). zenon_intro zenon_H4a4. % 8.01/8.19 generalize (zenon_H4a4 (c_tptpgeo_spindleheadmt)). zenon_intro zenon_H4af. % 8.01/8.19 generalize (zenon_H4af (c_worldgeographymt)). zenon_intro zenon_H4b0. % 8.01/8.19 apply (zenon_imply_s _ _ zenon_H4b0); [ zenon_intro zenon_H498 | zenon_intro zenon_H4b1 ]. % 8.01/8.19 exact (zenon_H498 zenon_H4a8). % 8.01/8.20 apply (zenon_imply_s _ _ zenon_H4b1); [ zenon_intro zenon_H4b3 | zenon_intro zenon_H4b2 ]. % 8.01/8.20 exact (zenon_H4b3 ax1_326). % 8.01/8.20 exact (zenon_H495 zenon_H4b2). % 8.01/8.20 apply zenon_H4aa. apply refl_equal. % 8.01/8.20 exact (zenon_H491 zenon_H493). % 8.01/8.20 exact (zenon_H462 zenon_H490). % 8.01/8.20 apply zenon_H460. zenon_intro zenon_Tx_bui. apply NNPP. zenon_intro zenon_H4b5. % 8.01/8.20 apply zenon_H4b5. zenon_intro zenon_Ty_buk. apply NNPP. zenon_intro zenon_H4b7. % 8.01/8.20 apply zenon_H4b7. zenon_intro zenon_Tz_bum. apply NNPP. zenon_intro zenon_H4b9. % 8.01/8.20 apply (zenon_notimply_s _ _ zenon_H4b9). zenon_intro zenon_H4bb. zenon_intro zenon_H4ba. % 8.01/8.20 apply (zenon_notimply_s _ _ zenon_H4ba). zenon_intro zenon_H4bd. zenon_intro zenon_H4bc. % 8.01/8.20 generalize (ax1_1128 zenon_Tx_bui). zenon_intro zenon_H4be. % 8.01/8.20 generalize (zenon_H4be zenon_Ty_buk). zenon_intro zenon_H4bf. % 8.01/8.20 generalize (zenon_H4bf zenon_Tz_bum). zenon_intro zenon_H4c0. % 8.01/8.20 apply (zenon_imply_s _ _ zenon_H4c0); [ zenon_intro zenon_H4c2 | zenon_intro zenon_H4c1 ]. % 8.01/8.20 apply (zenon_notand_s _ _ zenon_H4c2); [ zenon_intro zenon_H4c4 | zenon_intro zenon_H4c3 ]. % 8.01/8.20 exact (zenon_H4c4 zenon_H4bb). % 8.01/8.20 exact (zenon_H4c3 zenon_H4bd). % 8.01/8.20 exact (zenon_H4bc zenon_H4c1). % 8.01/8.20 apply zenon_H45e. zenon_intro zenon_Tx_buz. apply NNPP. zenon_intro zenon_H4c6. % 8.01/8.20 apply zenon_H4c6. zenon_intro zenon_Ty_bvb. apply NNPP. zenon_intro zenon_H4c8. % 8.01/8.20 apply zenon_H4c8. zenon_intro zenon_Tz_bvd. apply NNPP. zenon_intro zenon_H4ca. % 8.01/8.20 apply (zenon_notimply_s _ _ zenon_H4ca). zenon_intro zenon_H4cc. zenon_intro zenon_H4cb. % 8.01/8.20 apply (zenon_notimply_s _ _ zenon_H4cb). zenon_intro zenon_H4ce. zenon_intro zenon_H4cd. % 8.01/8.20 generalize (ax1_933 zenon_Tx_buz). zenon_intro zenon_H4cf. % 8.01/8.20 generalize (zenon_H4cf zenon_Ty_bvb). zenon_intro zenon_H4d0. % 8.01/8.20 generalize (zenon_H4d0 zenon_Tz_bvd). zenon_intro zenon_H4d1. % 8.01/8.20 apply (zenon_imply_s _ _ zenon_H4d1); [ zenon_intro zenon_H4d3 | zenon_intro zenon_H4d2 ]. % 8.01/8.20 apply (zenon_notand_s _ _ zenon_H4d3); [ zenon_intro zenon_H4d5 | zenon_intro zenon_H4d4 ]. % 8.01/8.20 exact (zenon_H4d5 zenon_H4cc). % 8.01/8.20 exact (zenon_H4d4 zenon_H4ce). % 8.01/8.20 exact (zenon_H4cd zenon_H4d2). % 8.01/8.20 apply zenon_H45c. zenon_intro zenon_Tx_bvq. apply NNPP. zenon_intro zenon_H4d7. % 8.01/8.20 apply zenon_H4d7. zenon_intro zenon_Ty_bvs. apply NNPP. zenon_intro zenon_H4d9. % 8.01/8.20 apply zenon_H4d9. zenon_intro zenon_Tz_bvu. apply NNPP. zenon_intro zenon_H4db. % 8.01/8.20 apply (zenon_notimply_s _ _ zenon_H4db). zenon_intro zenon_H4dd. zenon_intro zenon_H4dc. % 8.01/8.20 apply (zenon_notimply_s _ _ zenon_H4dc). zenon_intro zenon_H4df. zenon_intro zenon_H4de. % 8.01/8.20 generalize (ax1_1041 zenon_Tx_bvq). zenon_intro zenon_H4e0. % 8.01/8.20 generalize (zenon_H4e0 zenon_Ty_bvs). zenon_intro zenon_H4e1. % 8.01/8.20 generalize (zenon_H4e1 zenon_Tz_bvu). zenon_intro zenon_H4e2. % 8.01/8.20 apply (zenon_imply_s _ _ zenon_H4e2); [ zenon_intro zenon_H4e4 | zenon_intro zenon_H4e3 ]. % 8.01/8.20 apply (zenon_notand_s _ _ zenon_H4e4); [ zenon_intro zenon_H4e6 | zenon_intro zenon_H4e5 ]. % 8.01/8.20 exact (zenon_H4e6 zenon_H4dd). % 8.01/8.20 exact (zenon_H4e5 zenon_H4df). % 8.01/8.20 exact (zenon_H4de zenon_H4e3). % 8.01/8.20 Qed. % 8.01/8.20 % SZS output end Proof % 8.01/8.20 (* END-PROOF *) % 8.01/8.20 nodes searched: 302714 % 8.01/8.20 max branch formulas: 155209 % 8.01/8.20 proof nodes created: 333 % 8.01/8.20 formulas created: 2250975 % 8.01/8.20 %------------------------------------------------------------------------------