%------------------------------------------------------------------------------ % File : Zenon---0.7.1 % Problem : MGT013+1 : TPTP v9.3.0. Released v2.0.0. % Transfm : none % Format : tptp:raw % Command : run_zenon %s %d % Computer : n009.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8046.5625MB % OS : Linux 6.8.0-71-generic % CPULimit : 300s % WCLimit : 300s % DateTime : Tue Sep 8 06:24:17 AM UTC 2026 % Result : Theorem 3.04s 3.39s % Output : Proof 0.13s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.02 % Problem : MGT013+1 : TPTP v9.3.0. Released v2.0.0. % 0.00/0.03 % Command : run_zenon %s %d % 0.09/0.35 % Computer : n009.cluster.edu % 0.09/0.35 % Model : x86_64 x86_64 % 0.09/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.09/0.35 % Memory : 8046.5625MB % 0.09/0.35 % OS : Linux 6.8.0-71-generic % 0.09/0.35 % CPULimit : 300 % 0.09/0.35 % WCLimit : 300 % 0.09/0.35 % DateTime : Mon Sep 7 11:51:07 UTC 2026 % 0.09/0.35 % CPUTime : % 3.04/3.39 (* PROOF-FOUND *) % 3.04/3.39 % SZS status Theorem % 3.04/3.39 (* BEGIN-PROOF *) % 3.04/3.39 % SZS output start Proof % 3.04/3.39 Theorem t13_FOL : (forall X : zenon_U, (forall C1 : zenon_U, (forall C2 : zenon_U, (forall S1 : zenon_U, (forall S2 : zenon_U, (forall T1 : zenon_U, (forall T2 : zenon_U, (((organization X T1)/\((organization X T2)/\((reorganization_free X T1 T2)/\((complexity X C1 T1)/\((complexity X C2 T2)/\((size X S1 T1)/\((size X S2 T2)/\(greater C2 C1))))))))->(~(greater S1 S2)))))))))). % 3.04/3.39 Proof. % 3.04/3.39 assert (zenon_L1_ : forall (zenon_TX_l : zenon_U) (zenon_TT2_m : zenon_U), (~(time zenon_TT2_m)) -> (organization zenon_TX_l zenon_TT2_m) -> False). % 3.04/3.39 do 2 intro. intros zenon_H9 zenon_Ha. % 3.04/3.39 generalize (mp15 zenon_TX_l). zenon_intro zenon_Hd. % 3.04/3.39 generalize (zenon_Hd zenon_TT2_m). zenon_intro zenon_He. % 3.04/3.39 apply (zenon_imply_s _ _ zenon_He); [ zenon_intro zenon_H10 | zenon_intro zenon_Hf ]. % 3.04/3.39 exact (zenon_H10 zenon_Ha). % 3.04/3.39 exact (zenon_H9 zenon_Hf). % 3.04/3.39 (* end of lemma zenon_L1_ *) % 3.04/3.39 assert (zenon_L2_ : forall (zenon_TX_l : zenon_U) (zenon_TT1_t : zenon_U), (~(time zenon_TT1_t)) -> (organization zenon_TX_l zenon_TT1_t) -> False). % 3.04/3.39 do 2 intro. intros zenon_H11 zenon_H12. % 3.04/3.39 generalize (mp15 zenon_TX_l). zenon_intro zenon_Hd. % 3.04/3.39 generalize (zenon_Hd zenon_TT1_t). zenon_intro zenon_H14. % 3.04/3.39 apply (zenon_imply_s _ _ zenon_H14); [ zenon_intro zenon_H16 | zenon_intro zenon_H15 ]. % 3.04/3.39 exact (zenon_H16 zenon_H12). % 3.04/3.39 exact (zenon_H11 zenon_H15). % 3.04/3.39 (* end of lemma zenon_L2_ *) % 3.04/3.39 assert (zenon_L3_ : forall (zenon_TT1_t : zenon_U) (zenon_TT2_m : zenon_U) (zenon_TS2_bd : zenon_U) (zenon_TS1_be : zenon_U) (zenon_TX_l : zenon_U), (forall T1 : zenon_U, (forall T2 : zenon_U, (((organization zenon_TX_l T1)/\((organization zenon_TX_l T2)/\((reorganization_free zenon_TX_l T1 T2)/\((size zenon_TX_l zenon_TS1_be T1)/\((size zenon_TX_l zenon_TS2_bd T2)/\(greater T2 T1))))))->(~(greater zenon_TS1_be zenon_TS2_bd))))) -> (greater zenon_TS1_be zenon_TS2_bd) -> (greater zenon_TT2_m zenon_TT1_t) -> (size zenon_TX_l zenon_TS2_bd zenon_TT2_m) -> (size zenon_TX_l zenon_TS1_be zenon_TT1_t) -> (reorganization_free zenon_TX_l zenon_TT1_t zenon_TT2_m) -> (organization zenon_TX_l zenon_TT2_m) -> (organization zenon_TX_l zenon_TT1_t) -> False). % 3.04/3.39 do 5 intro. intros zenon_H17 zenon_H18 zenon_H19 zenon_H1a zenon_H1b zenon_H1c zenon_Ha zenon_H12. % 3.04/3.39 generalize (zenon_H17 zenon_TT1_t). zenon_intro zenon_H1f. % 3.04/3.39 generalize (zenon_H1f zenon_TT2_m). zenon_intro zenon_H20. % 3.04/3.39 apply (zenon_imply_s _ _ zenon_H20); [ zenon_intro zenon_H22 | zenon_intro zenon_H21 ]. % 3.04/3.39 apply (zenon_notand_s _ _ zenon_H22); [ zenon_intro zenon_H16 | zenon_intro zenon_H23 ]. % 3.04/3.39 exact (zenon_H16 zenon_H12). % 3.04/3.39 apply (zenon_notand_s _ _ zenon_H23); [ zenon_intro zenon_H10 | zenon_intro zenon_H24 ]. % 3.04/3.39 exact (zenon_H10 zenon_Ha). % 3.04/3.39 apply (zenon_notand_s _ _ zenon_H24); [ zenon_intro zenon_H26 | zenon_intro zenon_H25 ]. % 3.04/3.39 exact (zenon_H26 zenon_H1c). % 3.04/3.39 apply (zenon_notand_s _ _ zenon_H25); [ zenon_intro zenon_H28 | zenon_intro zenon_H27 ]. % 3.04/3.39 exact (zenon_H28 zenon_H1b). % 3.04/3.39 apply (zenon_notand_s _ _ zenon_H27); [ zenon_intro zenon_H2a | zenon_intro zenon_H29 ]. % 3.04/3.39 exact (zenon_H2a zenon_H1a). % 3.04/3.39 exact (zenon_H29 zenon_H19). % 3.04/3.39 exact (zenon_H21 zenon_H18). % 3.04/3.39 (* end of lemma zenon_L3_ *) % 3.04/3.39 assert (zenon_L4_ : forall (zenon_TS2_bd : zenon_U) (zenon_TT2_m : zenon_U) (zenon_TT1_t : zenon_U) (zenon_TS1_be : zenon_U) (zenon_TX_l : zenon_U), (forall S2 : zenon_U, (forall T1 : zenon_U, (forall T2 : zenon_U, (((organization zenon_TX_l T1)/\((organization zenon_TX_l T2)/\((reorganization_free zenon_TX_l T1 T2)/\((size zenon_TX_l zenon_TS1_be T1)/\((size zenon_TX_l S2 T2)/\(greater T2 T1))))))->(~(greater zenon_TS1_be S2)))))) -> (organization zenon_TX_l zenon_TT1_t) -> (organization zenon_TX_l zenon_TT2_m) -> (reorganization_free zenon_TX_l zenon_TT1_t zenon_TT2_m) -> (size zenon_TX_l zenon_TS1_be zenon_TT1_t) -> (size zenon_TX_l zenon_TS2_bd zenon_TT2_m) -> (greater zenon_TT2_m zenon_TT1_t) -> (greater zenon_TS1_be zenon_TS2_bd) -> False). % 3.04/3.39 do 5 intro. intros zenon_H2b zenon_H12 zenon_Ha zenon_H1c zenon_H1b zenon_H1a zenon_H19 zenon_H18. % 3.04/3.39 generalize (zenon_H2b zenon_TS2_bd). zenon_intro zenon_H17. % 3.04/3.39 apply (zenon_L3_ zenon_TT1_t zenon_TT2_m zenon_TS2_bd zenon_TS1_be zenon_TX_l); trivial. % 3.04/3.39 (* end of lemma zenon_L4_ *) % 3.04/3.39 assert (zenon_L5_ : forall (zenon_TT1_t : zenon_U) (zenon_TC1_bx : zenon_U) (zenon_TC2_by : zenon_U) (zenon_TT2_m : zenon_U) (zenon_TX_l : zenon_U), (forall T2 : zenon_U, (((organization zenon_TX_l zenon_TT2_m)/\((organization zenon_TX_l T2)/\((reorganization_free zenon_TX_l zenon_TT2_m T2)/\((complexity zenon_TX_l zenon_TC2_by zenon_TT2_m)/\((complexity zenon_TX_l zenon_TC1_bx T2)/\(greater T2 zenon_TT2_m))))))->(~(greater zenon_TC2_by zenon_TC1_bx)))) -> (organization zenon_TX_l zenon_TT2_m) -> (organization zenon_TX_l zenon_TT1_t) -> (reorganization_free zenon_TX_l zenon_TT1_t zenon_TT2_m) -> (complexity zenon_TX_l zenon_TC2_by zenon_TT2_m) -> (complexity zenon_TX_l zenon_TC1_bx zenon_TT1_t) -> (greater zenon_TT1_t zenon_TT2_m) -> (greater zenon_TC2_by zenon_TC1_bx) -> False). % 3.04/3.39 do 5 intro. intros zenon_H2c zenon_Ha zenon_H12 zenon_H1c zenon_H2d zenon_H2e zenon_H2f zenon_H30. % 3.04/3.39 generalize (zenon_H2c zenon_TT1_t). zenon_intro zenon_H33. % 3.04/3.39 apply (zenon_imply_s _ _ zenon_H33); [ zenon_intro zenon_H35 | zenon_intro zenon_H34 ]. % 3.04/3.39 apply (zenon_notand_s _ _ zenon_H35); [ zenon_intro zenon_H10 | zenon_intro zenon_H36 ]. % 3.04/3.39 exact (zenon_H10 zenon_Ha). % 3.04/3.39 apply (zenon_notand_s _ _ zenon_H36); [ zenon_intro zenon_H16 | zenon_intro zenon_H37 ]. % 3.04/3.39 exact (zenon_H16 zenon_H12). % 3.04/3.39 apply (zenon_notand_s _ _ zenon_H37); [ zenon_intro zenon_H39 | zenon_intro zenon_H38 ]. % 3.04/3.39 generalize (mp17 zenon_TX_l). zenon_intro zenon_H3a. % 3.04/3.39 generalize (zenon_H3a zenon_TT1_t). zenon_intro zenon_H3b. % 3.04/3.39 generalize (zenon_H3b zenon_TT2_m). zenon_intro zenon_H3c. % 3.04/3.39 apply (zenon_imply_s _ _ zenon_H3c); [ zenon_intro zenon_H26 | zenon_intro zenon_H3d ]. % 3.04/3.39 exact (zenon_H26 zenon_H1c). % 3.04/3.39 exact (zenon_H39 zenon_H3d). % 3.04/3.39 apply (zenon_notand_s _ _ zenon_H38); [ zenon_intro zenon_H3f | zenon_intro zenon_H3e ]. % 3.04/3.39 exact (zenon_H3f zenon_H2d). % 3.04/3.39 apply (zenon_notand_s _ _ zenon_H3e); [ zenon_intro zenon_H41 | zenon_intro zenon_H40 ]. % 3.04/3.39 exact (zenon_H41 zenon_H2e). % 3.04/3.39 exact (zenon_H40 zenon_H2f). % 3.04/3.39 exact (zenon_H34 zenon_H30). % 3.04/3.39 (* end of lemma zenon_L5_ *) % 3.04/3.39 assert (zenon_L6_ : forall (zenon_TC2_by : zenon_U) (zenon_TC1_bx : zenon_U), (~(greater zenon_TC1_bx zenon_TC2_by)) -> (greater zenon_TC2_by zenon_TC1_bx) -> (zenon_TC2_by = zenon_TC1_bx) -> False). % 3.04/3.39 do 2 intro. intros zenon_H42 zenon_H30 zenon_H43. % 3.04/3.39 cut ((greater zenon_TC2_by zenon_TC1_bx) = (greater zenon_TC1_bx zenon_TC2_by)). % 3.04/3.39 intro zenon_D_pnotp. % 3.04/3.39 apply zenon_H42. % 3.04/3.39 rewrite <- zenon_D_pnotp. % 3.04/3.39 exact zenon_H30. % 3.04/3.39 cut ((zenon_TC1_bx = zenon_TC2_by)); [idtac | apply NNPP; zenon_intro zenon_H44]. % 3.04/3.39 cut ((zenon_TC2_by = zenon_TC1_bx)); [idtac | apply NNPP; zenon_intro zenon_H45]. % 3.04/3.39 congruence. % 3.04/3.39 exact (zenon_H45 zenon_H43). % 3.04/3.39 apply zenon_H44. apply sym_equal. exact zenon_H43. % 3.04/3.39 (* end of lemma zenon_L6_ *) % 3.04/3.39 apply NNPP. intro zenon_G. % 3.04/3.39 apply (zenon_notallex_s (fun X : zenon_U => (forall C1 : zenon_U, (forall C2 : zenon_U, (forall S1 : zenon_U, (forall S2 : zenon_U, (forall T1 : zenon_U, (forall T2 : zenon_U, (((organization X T1)/\((organization X T2)/\((reorganization_free X T1 T2)/\((complexity X C1 T1)/\((complexity X C2 T2)/\((size X S1 T1)/\((size X S2 T2)/\(greater C2 C1))))))))->(~(greater S1 S2)))))))))) zenon_G); [ zenon_intro zenon_H46; idtac ]. % 3.04/3.39 elim zenon_H46. zenon_intro zenon_TX_l. zenon_intro zenon_H47. % 3.04/3.39 apply (zenon_notallex_s (fun C1 : zenon_U => (forall C2 : zenon_U, (forall S1 : zenon_U, (forall S2 : zenon_U, (forall T1 : zenon_U, (forall T2 : zenon_U, (((organization zenon_TX_l T1)/\((organization zenon_TX_l T2)/\((reorganization_free zenon_TX_l T1 T2)/\((complexity zenon_TX_l C1 T1)/\((complexity zenon_TX_l C2 T2)/\((size zenon_TX_l S1 T1)/\((size zenon_TX_l S2 T2)/\(greater C2 C1))))))))->(~(greater S1 S2))))))))) zenon_H47); [ zenon_intro zenon_H48; idtac ]. % 3.04/3.39 elim zenon_H48. zenon_intro zenon_TC1_bx. zenon_intro zenon_H49. % 3.04/3.39 apply (zenon_notallex_s (fun C2 : zenon_U => (forall S1 : zenon_U, (forall S2 : zenon_U, (forall T1 : zenon_U, (forall T2 : zenon_U, (((organization zenon_TX_l T1)/\((organization zenon_TX_l T2)/\((reorganization_free zenon_TX_l T1 T2)/\((complexity zenon_TX_l zenon_TC1_bx T1)/\((complexity zenon_TX_l C2 T2)/\((size zenon_TX_l S1 T1)/\((size zenon_TX_l S2 T2)/\(greater C2 zenon_TC1_bx))))))))->(~(greater S1 S2)))))))) zenon_H49); [ zenon_intro zenon_H4a; idtac ]. % 3.04/3.39 elim zenon_H4a. zenon_intro zenon_TC2_by. zenon_intro zenon_H4b. % 3.04/3.39 apply (zenon_notallex_s (fun S1 : zenon_U => (forall S2 : zenon_U, (forall T1 : zenon_U, (forall T2 : zenon_U, (((organization zenon_TX_l T1)/\((organization zenon_TX_l T2)/\((reorganization_free zenon_TX_l T1 T2)/\((complexity zenon_TX_l zenon_TC1_bx T1)/\((complexity zenon_TX_l zenon_TC2_by T2)/\((size zenon_TX_l S1 T1)/\((size zenon_TX_l S2 T2)/\(greater zenon_TC2_by zenon_TC1_bx))))))))->(~(greater S1 S2))))))) zenon_H4b); [ zenon_intro zenon_H4c; idtac ]. % 3.04/3.39 elim zenon_H4c. zenon_intro zenon_TS1_be. zenon_intro zenon_H4d. % 3.04/3.39 apply (zenon_notallex_s (fun S2 : zenon_U => (forall T1 : zenon_U, (forall T2 : zenon_U, (((organization zenon_TX_l T1)/\((organization zenon_TX_l T2)/\((reorganization_free zenon_TX_l T1 T2)/\((complexity zenon_TX_l zenon_TC1_bx T1)/\((complexity zenon_TX_l zenon_TC2_by T2)/\((size zenon_TX_l zenon_TS1_be T1)/\((size zenon_TX_l S2 T2)/\(greater zenon_TC2_by zenon_TC1_bx))))))))->(~(greater zenon_TS1_be S2)))))) zenon_H4d); [ zenon_intro zenon_H4e; idtac ]. % 3.04/3.39 elim zenon_H4e. zenon_intro zenon_TS2_bd. zenon_intro zenon_H4f. % 3.04/3.39 apply (zenon_notallex_s (fun T1 : zenon_U => (forall T2 : zenon_U, (((organization zenon_TX_l T1)/\((organization zenon_TX_l T2)/\((reorganization_free zenon_TX_l T1 T2)/\((complexity zenon_TX_l zenon_TC1_bx T1)/\((complexity zenon_TX_l zenon_TC2_by T2)/\((size zenon_TX_l zenon_TS1_be T1)/\((size zenon_TX_l zenon_TS2_bd T2)/\(greater zenon_TC2_by zenon_TC1_bx))))))))->(~(greater zenon_TS1_be zenon_TS2_bd))))) zenon_H4f); [ zenon_intro zenon_H50; idtac ]. % 3.04/3.39 elim zenon_H50. zenon_intro zenon_TT1_t. zenon_intro zenon_H51. % 3.04/3.39 apply (zenon_notallex_s (fun T2 : zenon_U => (((organization zenon_TX_l zenon_TT1_t)/\((organization zenon_TX_l T2)/\((reorganization_free zenon_TX_l zenon_TT1_t T2)/\((complexity zenon_TX_l zenon_TC1_bx zenon_TT1_t)/\((complexity zenon_TX_l zenon_TC2_by T2)/\((size zenon_TX_l zenon_TS1_be zenon_TT1_t)/\((size zenon_TX_l zenon_TS2_bd T2)/\(greater zenon_TC2_by zenon_TC1_bx))))))))->(~(greater zenon_TS1_be zenon_TS2_bd)))) zenon_H51); [ zenon_intro zenon_H52; idtac ]. % 3.04/3.39 elim zenon_H52. zenon_intro zenon_TT2_m. zenon_intro zenon_H53. % 3.04/3.39 apply (zenon_notimply_s _ _ zenon_H53). zenon_intro zenon_H55. zenon_intro zenon_H54. % 3.04/3.39 apply zenon_H54. zenon_intro zenon_H18. % 3.04/3.39 apply (zenon_and_s _ _ zenon_H55). zenon_intro zenon_H12. zenon_intro zenon_H56. % 3.04/3.39 apply (zenon_and_s _ _ zenon_H56). zenon_intro zenon_Ha. zenon_intro zenon_H57. % 3.04/3.39 apply (zenon_and_s _ _ zenon_H57). zenon_intro zenon_H1c. zenon_intro zenon_H58. % 3.04/3.39 apply (zenon_and_s _ _ zenon_H58). zenon_intro zenon_H2e. zenon_intro zenon_H59. % 3.04/3.39 apply (zenon_and_s _ _ zenon_H59). zenon_intro zenon_H2d. zenon_intro zenon_H5a. % 3.04/3.39 apply (zenon_and_s _ _ zenon_H5a). zenon_intro zenon_H1b. zenon_intro zenon_H5b. % 3.04/3.39 apply (zenon_and_s _ _ zenon_H5b). zenon_intro zenon_H1a. zenon_intro zenon_H30. % 3.04/3.39 generalize (mp6_2 zenon_TC1_bx). zenon_intro zenon_H5c. % 3.04/3.39 generalize (zenon_H5c zenon_TC2_by). zenon_intro zenon_H5d. % 3.04/3.39 apply (zenon_notand_s _ _ zenon_H5d); [ zenon_intro zenon_H42 | zenon_intro zenon_H34 ]. % 3.04/3.39 generalize (mp18 zenon_TX_l). zenon_intro zenon_H5e. % 3.04/3.39 generalize (zenon_H5e zenon_TC2_by). zenon_intro zenon_H5f. % 3.04/3.39 generalize (t12_FOL zenon_TX_l). zenon_intro zenon_H60. % 3.04/3.39 generalize (t11_FOL zenon_TX_l). zenon_intro zenon_H61. % 3.04/3.39 generalize (zenon_H60 zenon_TC2_by). zenon_intro zenon_H62. % 3.04/3.39 generalize (mp16 zenon_TT2_m). zenon_intro zenon_H63. % 3.04/3.39 generalize (zenon_H62 zenon_TC1_bx). zenon_intro zenon_H64. % 3.04/3.39 generalize (zenon_H5f zenon_TC1_bx). zenon_intro zenon_H65. % 3.04/3.39 generalize (zenon_H65 zenon_TT2_m). zenon_intro zenon_H66. % 3.04/3.39 generalize (zenon_H61 zenon_TS1_be). zenon_intro zenon_H2b. % 3.04/3.39 generalize (zenon_H64 zenon_TT2_m). zenon_intro zenon_H2c. % 3.04/3.39 generalize (zenon_H66 zenon_TT1_t). zenon_intro zenon_H67. % 3.04/3.39 apply (zenon_imply_s _ _ zenon_H67); [ zenon_intro zenon_H68 | zenon_intro zenon_H43 ]. % 3.04/3.39 apply (zenon_notand_s _ _ zenon_H68); [ zenon_intro zenon_H10 | zenon_intro zenon_H69 ]. % 0.13/3.40 exact (zenon_H10 zenon_Ha). % 0.13/3.40 apply (zenon_notand_s _ _ zenon_H69); [ zenon_intro zenon_H16 | zenon_intro zenon_H6a ]. % 0.13/3.40 exact (zenon_H16 zenon_H12). % 0.13/3.40 apply (zenon_notand_s _ _ zenon_H6a); [ zenon_intro zenon_H3f | zenon_intro zenon_H6b ]. % 0.13/3.40 exact (zenon_H3f zenon_H2d). % 0.13/3.40 apply (zenon_notand_s _ _ zenon_H6b); [ zenon_intro zenon_H41 | zenon_intro zenon_H6c ]. % 0.13/3.40 exact (zenon_H41 zenon_H2e). % 0.13/3.40 generalize (zenon_H63 zenon_TT1_t). zenon_intro zenon_H6d. % 0.13/3.40 apply (zenon_imply_s _ _ zenon_H6d); [ zenon_intro zenon_H6f | zenon_intro zenon_H6e ]. % 0.13/3.40 apply (zenon_notand_s _ _ zenon_H6f); [ zenon_intro zenon_H9 | zenon_intro zenon_H11 ]. % 0.13/3.40 apply (zenon_L1_ zenon_TX_l zenon_TT2_m); trivial. % 0.13/3.40 apply (zenon_L2_ zenon_TX_l zenon_TT1_t); trivial. % 0.13/3.40 apply (zenon_or_s _ _ zenon_H6e); [ zenon_intro zenon_H19 | zenon_intro zenon_H70 ]. % 0.13/3.40 apply (zenon_L4_ zenon_TS2_bd zenon_TT2_m zenon_TT1_t zenon_TS1_be zenon_TX_l); trivial. % 0.13/3.40 apply (zenon_or_s _ _ zenon_H70); [ zenon_intro zenon_H71 | zenon_intro zenon_H2f ]. % 0.13/3.40 exact (zenon_H6c zenon_H71). % 0.13/3.40 apply (zenon_L5_ zenon_TT1_t zenon_TC1_bx zenon_TC2_by zenon_TT2_m zenon_TX_l); trivial. % 0.13/3.40 apply (zenon_L6_ zenon_TC2_by zenon_TC1_bx); trivial. % 0.13/3.40 exact (zenon_H34 zenon_H30). % 0.13/3.40 Qed. % 0.13/3.40 % SZS output end Proof % 0.13/3.40 (* END-PROOF *) % 0.13/3.40 nodes searched: 27266 % 0.13/3.40 max branch formulas: 2978 % 0.13/3.40 proof nodes created: 3403 % 0.13/3.40 formulas created: 55366 % 0.13/3.40 %------------------------------------------------------------------------------