%------------------------------------------------------------------------------ % File : Zenon---0.7.1 % Problem : SWV438+1 : TPTP v8.1.0. Released v4.0.0. % Transfm : none % Format : tptp:raw % Command : run_zenon %s %d % Computer : n011.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 : Wed Jul 20 23:04:32 EDT 2022 % Result : Theorem 0.35s 0.53s % Output : Proof 0.35s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.13 % Problem : SWV438+1 : TPTP v8.1.0. Released v4.0.0. % 0.07/0.13 % Command : run_zenon %s %d % 0.12/0.35 % Computer : n011.cluster.edu % 0.12/0.35 % Model : x86_64 x86_64 % 0.12/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.35 % Memory : 8042.1875MB % 0.12/0.35 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.35 % CPULimit : 300 % 0.12/0.35 % WCLimit : 600 % 0.12/0.35 % DateTime : Wed Jun 15 14:03:50 EDT 2022 % 0.12/0.35 % CPUTime : % 0.35/0.53 (* PROOF-FOUND *) % 0.35/0.53 % SZS status Theorem % 0.35/0.53 (* BEGIN-PROOF *) % 0.35/0.53 % SZS output start Proof % 0.35/0.53 Theorem babureadnotsecret : (admin_indi_may_file (admin) (babu) (not_secretfile) (read)). % 0.35/0.53 Proof. % 0.35/0.53 assert (zenon_L1_ : (forall CL : zenon_U, ((system_file_needs_compartments (system) (not_secretfile) CL)->((admin_file_has_compartments_h (admin) (not_secretfile) CL CL)->(admin_file_has_compartments (admin) (not_secretfile) CL)))) -> (~(admin_file_has_compartments (admin) (not_secretfile) (nil))) -> False). % 0.35/0.53 do 0 intro. intros zenon_H58 zenon_H59. % 0.35/0.53 generalize (zenon_H58 (nil)). zenon_intro zenon_H5a. % 0.35/0.53 apply (zenon_imply_s _ _ zenon_H5a); [ zenon_intro zenon_H5c | zenon_intro zenon_H5b ]. % 0.35/0.53 exact (zenon_H5c ax62). % 0.35/0.53 apply (zenon_imply_s _ _ zenon_H5b); [ zenon_intro zenon_H5e | zenon_intro zenon_H5d ]. % 0.35/0.53 generalize (ax9 (not_secretfile)). zenon_intro zenon_H5f. % 0.35/0.53 generalize (zenon_H5f (nil)). zenon_intro zenon_H60. % 0.35/0.53 exact (zenon_H5e zenon_H60). % 0.35/0.53 exact (zenon_H59 zenon_H5d). % 0.35/0.53 (* end of lemma zenon_L1_ *) % 0.35/0.53 assert (zenon_L2_ : (~(admin_file_has_compartments (admin) (not_secretfile) (nil))) -> False). % 0.35/0.53 do 0 intro. intros zenon_H59. % 0.35/0.53 generalize (ax8 (not_secretfile)). zenon_intro zenon_H58. % 0.35/0.53 apply (zenon_L1_); trivial. % 0.35/0.53 (* end of lemma zenon_L2_ *) % 0.35/0.53 apply NNPP. intro zenon_G. % 0.35/0.53 generalize (ax39 (babu)). zenon_intro zenon_H61. % 0.35/0.53 generalize (zenon_H61 (not_secretfile)). zenon_intro zenon_H62. % 0.35/0.53 apply (zenon_imply_s _ _ zenon_H62); [ zenon_intro zenon_H64 | zenon_intro zenon_H63 ]. % 0.35/0.53 exact (zenon_H64 ax61). % 0.35/0.53 apply (zenon_imply_s _ _ zenon_H63); [ zenon_intro zenon_H66 | zenon_intro zenon_H65 ]. % 0.35/0.53 generalize (ax37 (babu)). zenon_intro zenon_H67. % 0.35/0.53 generalize (zenon_H67 (not_secretfile)). zenon_intro zenon_H68. % 0.35/0.53 generalize (zenon_H68 (anycountry)). zenon_intro zenon_H69. % 0.35/0.53 apply (zenon_imply_s _ _ zenon_H69); [ zenon_intro zenon_H6b | zenon_intro zenon_H6a ]. % 0.35/0.53 generalize (ax14 (not_secretfile)). zenon_intro zenon_H6c. % 0.35/0.53 generalize (zenon_H6c (anycountry)). zenon_intro zenon_H6d. % 0.35/0.53 generalize (ax8 (not_secretfile)). zenon_intro zenon_H58. % 0.35/0.53 generalize (zenon_H6d (nil)). zenon_intro zenon_H6e. % 0.35/0.53 apply (zenon_imply_s _ _ zenon_H6e); [ zenon_intro zenon_H70 | zenon_intro zenon_H6f ]. % 0.35/0.53 exact (zenon_H70 ax64). % 0.35/0.53 apply (zenon_imply_s _ _ zenon_H6f); [ zenon_intro zenon_H59 | zenon_intro zenon_H71 ]. % 0.35/0.53 apply (zenon_L1_); trivial. % 0.35/0.53 apply (zenon_imply_s _ _ zenon_H71); [ zenon_intro zenon_H73 | zenon_intro zenon_H72 ]. % 0.35/0.53 generalize (ax15 (not_secretfile)). zenon_intro zenon_H74. % 0.35/0.53 generalize (zenon_H74 (anycountry)). zenon_intro zenon_H75. % 0.35/0.53 exact (zenon_H73 zenon_H75). % 0.35/0.53 exact (zenon_H6b zenon_H72). % 0.35/0.53 apply (zenon_imply_s _ _ zenon_H6a); [ zenon_intro zenon_H77 | zenon_intro zenon_H76 ]. % 0.35/0.53 generalize (ax22 (babu)). zenon_intro zenon_H78. % 0.35/0.53 exact (zenon_H77 zenon_H78). % 0.35/0.53 exact (zenon_H66 zenon_H76). % 0.35/0.53 apply (zenon_imply_s _ _ zenon_H65); [ zenon_intro zenon_H7a | zenon_intro zenon_H79 ]. % 0.35/0.53 generalize (ax36 (babu)). zenon_intro zenon_H7b. % 0.35/0.53 generalize (zenon_H7b (not_secretfile)). zenon_intro zenon_H7c. % 0.35/0.53 generalize (zenon_H7c (owner_not_secretfile)). zenon_intro zenon_H7d. % 0.35/0.53 apply (zenon_imply_s _ _ zenon_H7d); [ zenon_intro zenon_H7f | zenon_intro zenon_H7e ]. % 0.35/0.53 exact (zenon_H7f ax65). % 0.35/0.53 apply (zenon_imply_s _ _ zenon_H7e); [ zenon_intro zenon_H81 | zenon_intro zenon_H80 ]. % 0.35/0.53 exact (zenon_H81 ax85). % 0.35/0.53 exact (zenon_H7a zenon_H80). % 0.35/0.53 apply (zenon_imply_s _ _ zenon_H79); [ zenon_intro zenon_H83 | zenon_intro zenon_H82 ]. % 0.35/0.53 generalize (ax35 (babu)). zenon_intro zenon_H84. % 0.35/0.53 generalize (zenon_H84 (not_secretfile)). zenon_intro zenon_H85. % 0.35/0.53 generalize (zenon_H85 (unclassified)). zenon_intro zenon_H86. % 0.35/0.53 apply (zenon_imply_s _ _ zenon_H86); [ zenon_intro zenon_H88 | zenon_intro zenon_H87 ]. % 0.35/0.53 generalize (ax11 (not_secretfile)). zenon_intro zenon_H89. % 0.35/0.53 generalize (zenon_H89 (unclassified)). zenon_intro zenon_H8a. % 0.35/0.53 generalize (ax8 (not_secretfile)). zenon_intro zenon_H58. % 0.35/0.53 generalize (zenon_H8a (nil)). zenon_intro zenon_H8b. % 0.35/0.53 apply (zenon_imply_s _ _ zenon_H8b); [ zenon_intro zenon_H8d | zenon_intro zenon_H8c ]. % 0.35/0.53 exact (zenon_H8d ax63). % 0.35/0.53 apply (zenon_imply_s _ _ zenon_H8c); [ zenon_intro zenon_H59 | zenon_intro zenon_H8e ]. % 0.35/0.53 apply (zenon_L1_); trivial. % 0.35/0.53 apply (zenon_imply_s _ _ zenon_H8e); [ zenon_intro zenon_H90 | zenon_intro zenon_H8f ]. % 0.35/0.53 generalize (ax12 (not_secretfile)). zenon_intro zenon_H91. % 0.35/0.53 generalize (zenon_H91 (unclassified)). zenon_intro zenon_H92. % 0.35/0.53 exact (zenon_H90 zenon_H92). % 0.35/0.53 exact (zenon_H88 zenon_H8f). % 0.35/0.53 apply (zenon_imply_s _ _ zenon_H87); [ zenon_intro zenon_H94 | zenon_intro zenon_H93 ]. % 0.35/0.53 generalize (ax24 (babu)). zenon_intro zenon_H95. % 0.35/0.53 exact (zenon_H94 zenon_H95). % 0.35/0.53 exact (zenon_H83 zenon_H93). % 0.35/0.53 apply (zenon_imply_s _ _ zenon_H82); [ zenon_intro zenon_H97 | zenon_intro zenon_H96 ]. % 0.35/0.53 generalize (ax34 (babu)). zenon_intro zenon_H98. % 0.35/0.53 generalize (zenon_H98 (not_secretfile)). zenon_intro zenon_H99. % 0.35/0.53 generalize (zenon_H99 (nil)). zenon_intro zenon_H9a. % 0.35/0.53 apply (zenon_imply_s _ _ zenon_H9a); [ zenon_intro zenon_H59 | zenon_intro zenon_H9b ]. % 0.35/0.53 apply (zenon_L2_); trivial. % 0.35/0.53 apply (zenon_imply_s _ _ zenon_H9b); [ zenon_intro zenon_H9d | zenon_intro zenon_H9c ]. % 0.35/0.53 generalize (ax26 (babu)). zenon_intro zenon_H9e. % 0.35/0.53 exact (zenon_H9d zenon_H9e). % 0.35/0.53 exact (zenon_H97 zenon_H9c). % 0.35/0.53 exact (zenon_G zenon_H96). % 0.35/0.53 Qed. % 0.35/0.53 % SZS output end Proof % 0.35/0.53 (* END-PROOF *) % 0.35/0.53 nodes searched: 591 % 0.35/0.53 max branch formulas: 396 % 0.35/0.53 proof nodes created: 111 % 0.35/0.53 formulas created: 3616 % 0.35/0.53 %------------------------------------------------------------------------------