%------------------------------------------------------------------------------ % File : SuperZenon---0.0.1 % Problem : SWV438+1 : TPTP v8.1.0. Released v4.0.0. % Transfm : none % Format : tptp:raw % Command : run_super_zenon -p0 -itptp -om -max-time %d %s % Computer : n019.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 21:51:33 EDT 2022 % Result : Theorem 0.18s 0.40s % Output : Proof 0.18s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.11 % Problem : SWV438+1 : TPTP v8.1.0. Released v4.0.0. % 0.03/0.12 % Command : run_super_zenon -p0 -itptp -om -max-time %d %s % 0.12/0.33 % Computer : n019.cluster.edu % 0.12/0.33 % Model : x86_64 x86_64 % 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.33 % Memory : 8042.1875MB % 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.33 % CPULimit : 300 % 0.12/0.33 % WCLimit : 600 % 0.12/0.33 % DateTime : Wed Jun 15 14:10:39 EDT 2022 % 0.12/0.33 % CPUTime : % 0.18/0.40 % SZS status Theorem % 0.18/0.40 (* PROOF-FOUND *) % 0.18/0.40 (* BEGIN-PROOF *) % 0.18/0.40 % SZS output start Proof % 0.18/0.40 1. (-. (admin_file_has_compartments_h (admin) (not_secretfile) (nil) (nil))) (admin_file_has_compartments_h (admin) (not_secretfile) (nil) (nil)) ### Axiom % 0.18/0.40 2. (All CL, (admin_file_has_compartments_h (admin) (not_secretfile) CL (nil))) (-. (admin_file_has_compartments_h (admin) (not_secretfile) (nil) (nil))) ### All 1 % 0.18/0.40 3. (All F, (All CL, (admin_file_has_compartments_h (admin) F CL (nil)))) (-. (admin_file_has_compartments_h (admin) (not_secretfile) (nil) (nil))) ### All 2 % 0.18/0.40 4. (state_file_is_not_working_paper (not_secretfile)) (-. (state_file_is_not_working_paper (not_secretfile))) ### Axiom % 0.18/0.40 5. (system_file_needs_citizenship (system) (not_secretfile) (anycountry)) (-. (system_file_needs_citizenship (system) (not_secretfile) (anycountry))) ### Axiom % 0.18/0.40 6. (admin_file_has_compartments (admin) (not_secretfile) (nil)) (-. (admin_file_has_compartments (admin) (not_secretfile) (nil))) ### Axiom % 0.18/0.40 7. (-. (admin_file_has_citizenship_h (admin) (not_secretfile) (anycountry) (nil))) (admin_file_has_citizenship_h (admin) (not_secretfile) (anycountry) (nil)) ### Axiom % 0.18/0.40 8. (All U, (admin_file_has_citizenship_h (admin) (not_secretfile) U (nil))) (-. (admin_file_has_citizenship_h (admin) (not_secretfile) (anycountry) (nil))) ### All 7 % 0.18/0.40 9. (All F, (All U, (admin_file_has_citizenship_h (admin) F U (nil)))) (-. (admin_file_has_citizenship_h (admin) (not_secretfile) (anycountry) (nil))) ### All 8 % 0.18/0.40 10. (-. (admin_file_has_citizenship (admin) (not_secretfile) (anycountry))) (admin_file_has_citizenship (admin) (not_secretfile) (anycountry)) ### Axiom % 0.18/0.40 11. ((system_file_needs_citizenship (system) (not_secretfile) (anycountry)) => ((admin_file_has_compartments (admin) (not_secretfile) (nil)) => ((admin_file_has_citizenship_h (admin) (not_secretfile) (anycountry) (nil)) => (admin_file_has_citizenship (admin) (not_secretfile) (anycountry))))) (-. (admin_file_has_citizenship (admin) (not_secretfile) (anycountry))) (All F, (All U, (admin_file_has_citizenship_h (admin) F U (nil)))) (admin_file_has_compartments (admin) (not_secretfile) (nil)) (system_file_needs_citizenship (system) (not_secretfile) (anycountry)) ### DisjTree 5 6 9 10 % 0.18/0.40 12. (All CL, ((system_file_needs_citizenship (system) (not_secretfile) (anycountry)) => ((admin_file_has_compartments (admin) (not_secretfile) CL) => ((admin_file_has_citizenship_h (admin) (not_secretfile) (anycountry) CL) => (admin_file_has_citizenship (admin) (not_secretfile) (anycountry)))))) (system_file_needs_citizenship (system) (not_secretfile) (anycountry)) (admin_file_has_compartments (admin) (not_secretfile) (nil)) (All F, (All U, (admin_file_has_citizenship_h (admin) F U (nil)))) (-. (admin_file_has_citizenship (admin) (not_secretfile) (anycountry))) ### All 11 % 0.18/0.40 13. (All U, (All CL, ((system_file_needs_citizenship (system) (not_secretfile) U) => ((admin_file_has_compartments (admin) (not_secretfile) CL) => ((admin_file_has_citizenship_h (admin) (not_secretfile) U CL) => (admin_file_has_citizenship (admin) (not_secretfile) U)))))) (-. (admin_file_has_citizenship (admin) (not_secretfile) (anycountry))) (All F, (All U, (admin_file_has_citizenship_h (admin) F U (nil)))) (admin_file_has_compartments (admin) (not_secretfile) (nil)) (system_file_needs_citizenship (system) (not_secretfile) (anycountry)) ### All 12 % 0.18/0.40 14. (All F, (All U, (All CL, ((system_file_needs_citizenship (system) F U) => ((admin_file_has_compartments (admin) F CL) => ((admin_file_has_citizenship_h (admin) F U CL) => (admin_file_has_citizenship (admin) F U))))))) (system_file_needs_citizenship (system) (not_secretfile) (anycountry)) (admin_file_has_compartments (admin) (not_secretfile) (nil)) (All F, (All U, (admin_file_has_citizenship_h (admin) F U (nil)))) (-. (admin_file_has_citizenship (admin) (not_secretfile) (anycountry))) ### All 13 % 0.18/0.40 15. (-. (admin_indi_has_citizenship (admin) (babu) (anycountry))) (admin_indi_has_citizenship (admin) (babu) (anycountry)) ### Axiom % 0.18/0.40 16. (All K, (admin_indi_has_citizenship (admin) K (anycountry))) (-. (admin_indi_has_citizenship (admin) (babu) (anycountry))) ### All 15 % 0.18/0.40 17. (-. (admin_indi_has_citizenship_for_file (admin) (babu) (not_secretfile))) (admin_indi_has_citizenship_for_file (admin) (babu) (not_secretfile)) ### Axiom % 0.18/0.40 18. ((admin_file_has_citizenship (admin) (not_secretfile) (anycountry)) => ((admin_indi_has_citizenship (admin) (babu) (anycountry)) => (admin_indi_has_citizenship_for_file (admin) (babu) (not_secretfile)))) (-. (admin_indi_has_citizenship_for_file (admin) (babu) (not_secretfile))) (All K, (admin_indi_has_citizenship (admin) K (anycountry))) (All F, (All U, (admin_file_has_citizenship_h (admin) F U (nil)))) (admin_file_has_compartments (admin) (not_secretfile) (nil)) (system_file_needs_citizenship (system) (not_secretfile) (anycountry)) (All F, (All U, (All CL, ((system_file_needs_citizenship (system) F U) => ((admin_file_has_compartments (admin) F CL) => ((admin_file_has_citizenship_h (admin) F U CL) => (admin_file_has_citizenship (admin) F U))))))) ### DisjTree 14 16 17 % 0.18/0.40 19. (All L, ((admin_file_has_citizenship (admin) (not_secretfile) L) => ((admin_indi_has_citizenship (admin) (babu) L) => (admin_indi_has_citizenship_for_file (admin) (babu) (not_secretfile))))) (All F, (All U, (All CL, ((system_file_needs_citizenship (system) F U) => ((admin_file_has_compartments (admin) F CL) => ((admin_file_has_citizenship_h (admin) F U CL) => (admin_file_has_citizenship (admin) F U))))))) (system_file_needs_citizenship (system) (not_secretfile) (anycountry)) (admin_file_has_compartments (admin) (not_secretfile) (nil)) (All F, (All U, (admin_file_has_citizenship_h (admin) F U (nil)))) (All K, (admin_indi_has_citizenship (admin) K (anycountry))) (-. (admin_indi_has_citizenship_for_file (admin) (babu) (not_secretfile))) ### All 18 % 0.18/0.40 20. (All F, (All L, ((admin_file_has_citizenship (admin) F L) => ((admin_indi_has_citizenship (admin) (babu) L) => (admin_indi_has_citizenship_for_file (admin) (babu) F))))) (-. (admin_indi_has_citizenship_for_file (admin) (babu) (not_secretfile))) (All K, (admin_indi_has_citizenship (admin) K (anycountry))) (All F, (All U, (admin_file_has_citizenship_h (admin) F U (nil)))) (admin_file_has_compartments (admin) (not_secretfile) (nil)) (system_file_needs_citizenship (system) (not_secretfile) (anycountry)) (All F, (All U, (All CL, ((system_file_needs_citizenship (system) F U) => ((admin_file_has_compartments (admin) F CL) => ((admin_file_has_citizenship_h (admin) F U CL) => (admin_file_has_citizenship (admin) F U))))))) ### All 19 % 0.18/0.40 21. (All K, (All F, (All L, ((admin_file_has_citizenship (admin) F L) => ((admin_indi_has_citizenship (admin) K L) => (admin_indi_has_citizenship_for_file (admin) K F)))))) (All F, (All U, (All CL, ((system_file_needs_citizenship (system) F U) => ((admin_file_has_compartments (admin) F CL) => ((admin_file_has_citizenship_h (admin) F U CL) => (admin_file_has_citizenship (admin) F U))))))) (system_file_needs_citizenship (system) (not_secretfile) (anycountry)) (admin_file_has_compartments (admin) (not_secretfile) (nil)) (All F, (All U, (admin_file_has_citizenship_h (admin) F U (nil)))) (All K, (admin_indi_has_citizenship (admin) K (anycountry))) (-. (admin_indi_has_citizenship_for_file (admin) (babu) (not_secretfile))) ### All 20 % 0.18/0.40 22. (state_file_has_owner (not_secretfile) (owner_not_secretfile)) (-. (state_file_has_owner (not_secretfile) (owner_not_secretfile))) ### Axiom % 0.18/0.40 23. (owner_indi_has_need_to_know (owner_not_secretfile) (babu) (not_secretfile)) (-. (owner_indi_has_need_to_know (owner_not_secretfile) (babu) (not_secretfile))) ### Axiom % 0.18/0.40 24. (-. (admin_indi_has_need_to_know_for_file (admin) (babu) (not_secretfile))) (admin_indi_has_need_to_know_for_file (admin) (babu) (not_secretfile)) ### Axiom % 0.18/0.40 25. ((state_file_has_owner (not_secretfile) (owner_not_secretfile)) => ((owner_indi_has_need_to_know (owner_not_secretfile) (babu) (not_secretfile)) => (admin_indi_has_need_to_know_for_file (admin) (babu) (not_secretfile)))) (-. (admin_indi_has_need_to_know_for_file (admin) (babu) (not_secretfile))) (owner_indi_has_need_to_know (owner_not_secretfile) (babu) (not_secretfile)) (state_file_has_owner (not_secretfile) (owner_not_secretfile)) ### DisjTree 22 23 24 % 0.18/0.40 26. (All OWR, ((state_file_has_owner (not_secretfile) OWR) => ((owner_indi_has_need_to_know OWR (babu) (not_secretfile)) => (admin_indi_has_need_to_know_for_file (admin) (babu) (not_secretfile))))) (state_file_has_owner (not_secretfile) (owner_not_secretfile)) (owner_indi_has_need_to_know (owner_not_secretfile) (babu) (not_secretfile)) (-. (admin_indi_has_need_to_know_for_file (admin) (babu) (not_secretfile))) ### All 25 % 0.18/0.40 27. (All F, (All OWR, ((state_file_has_owner F OWR) => ((owner_indi_has_need_to_know OWR (babu) F) => (admin_indi_has_need_to_know_for_file (admin) (babu) F))))) (-. (admin_indi_has_need_to_know_for_file (admin) (babu) (not_secretfile))) (owner_indi_has_need_to_know (owner_not_secretfile) (babu) (not_secretfile)) (state_file_has_owner (not_secretfile) (owner_not_secretfile)) ### All 26 % 0.18/0.40 28. (All K, (All F, (All OWR, ((state_file_has_owner F OWR) => ((owner_indi_has_need_to_know OWR K F) => (admin_indi_has_need_to_know_for_file (admin) K F)))))) (state_file_has_owner (not_secretfile) (owner_not_secretfile)) (owner_indi_has_need_to_know (owner_not_secretfile) (babu) (not_secretfile)) (-. (admin_indi_has_need_to_know_for_file (admin) (babu) (not_secretfile))) ### All 27 % 0.18/0.40 29. (system_file_needs_level (system) (not_secretfile) (unclassified)) (-. (system_file_needs_level (system) (not_secretfile) (unclassified))) ### Axiom % 0.18/0.40 30. (admin_file_has_compartments (admin) (not_secretfile) (nil)) (-. (admin_file_has_compartments (admin) (not_secretfile) (nil))) ### Axiom % 0.18/0.40 31. (-. (admin_file_has_level_h (admin) (not_secretfile) (unclassified) (nil))) (admin_file_has_level_h (admin) (not_secretfile) (unclassified) (nil)) ### Axiom % 0.18/0.40 32. (All L, (admin_file_has_level_h (admin) (not_secretfile) L (nil))) (-. (admin_file_has_level_h (admin) (not_secretfile) (unclassified) (nil))) ### All 31 % 0.18/0.40 33. (All F, (All L, (admin_file_has_level_h (admin) F L (nil)))) (-. (admin_file_has_level_h (admin) (not_secretfile) (unclassified) (nil))) ### All 32 % 0.18/0.40 34. (-. (admin_file_has_level (admin) (not_secretfile) (unclassified))) (admin_file_has_level (admin) (not_secretfile) (unclassified)) ### Axiom % 0.18/0.40 35. ((system_file_needs_level (system) (not_secretfile) (unclassified)) => ((admin_file_has_compartments (admin) (not_secretfile) (nil)) => ((admin_file_has_level_h (admin) (not_secretfile) (unclassified) (nil)) => (admin_file_has_level (admin) (not_secretfile) (unclassified))))) (-. (admin_file_has_level (admin) (not_secretfile) (unclassified))) (All F, (All L, (admin_file_has_level_h (admin) F L (nil)))) (admin_file_has_compartments (admin) (not_secretfile) (nil)) (system_file_needs_level (system) (not_secretfile) (unclassified)) ### DisjTree 29 30 33 34 % 0.18/0.40 36. (All CL, ((system_file_needs_level (system) (not_secretfile) (unclassified)) => ((admin_file_has_compartments (admin) (not_secretfile) CL) => ((admin_file_has_level_h (admin) (not_secretfile) (unclassified) CL) => (admin_file_has_level (admin) (not_secretfile) (unclassified)))))) (system_file_needs_level (system) (not_secretfile) (unclassified)) (admin_file_has_compartments (admin) (not_secretfile) (nil)) (All F, (All L, (admin_file_has_level_h (admin) F L (nil)))) (-. (admin_file_has_level (admin) (not_secretfile) (unclassified))) ### All 35 % 0.18/0.40 37. (All L, (All CL, ((system_file_needs_level (system) (not_secretfile) L) => ((admin_file_has_compartments (admin) (not_secretfile) CL) => ((admin_file_has_level_h (admin) (not_secretfile) L CL) => (admin_file_has_level (admin) (not_secretfile) L)))))) (-. (admin_file_has_level (admin) (not_secretfile) (unclassified))) (All F, (All L, (admin_file_has_level_h (admin) F L (nil)))) (admin_file_has_compartments (admin) (not_secretfile) (nil)) (system_file_needs_level (system) (not_secretfile) (unclassified)) ### All 36 % 0.18/0.40 38. (All F, (All L, (All CL, ((system_file_needs_level (system) F L) => ((admin_file_has_compartments (admin) F CL) => ((admin_file_has_level_h (admin) F L CL) => (admin_file_has_level (admin) F L))))))) (system_file_needs_level (system) (not_secretfile) (unclassified)) (admin_file_has_compartments (admin) (not_secretfile) (nil)) (All F, (All L, (admin_file_has_level_h (admin) F L (nil)))) (-. (admin_file_has_level (admin) (not_secretfile) (unclassified))) ### All 37 % 0.18/0.40 39. (-. (admin_indi_has_level (admin) (babu) (unclassified))) (admin_indi_has_level (admin) (babu) (unclassified)) ### Axiom % 0.18/0.40 40. (All K, (admin_indi_has_level (admin) K (unclassified))) (-. (admin_indi_has_level (admin) (babu) (unclassified))) ### All 39 % 0.18/0.40 41. (-. (admin_indi_has_level_for_file (admin) (babu) (not_secretfile))) (admin_indi_has_level_for_file (admin) (babu) (not_secretfile)) ### Axiom % 0.18/0.40 42. ((admin_file_has_level (admin) (not_secretfile) (unclassified)) => ((admin_indi_has_level (admin) (babu) (unclassified)) => (admin_indi_has_level_for_file (admin) (babu) (not_secretfile)))) (-. (admin_indi_has_level_for_file (admin) (babu) (not_secretfile))) (All K, (admin_indi_has_level (admin) K (unclassified))) (All F, (All L, (admin_file_has_level_h (admin) F L (nil)))) (admin_file_has_compartments (admin) (not_secretfile) (nil)) (system_file_needs_level (system) (not_secretfile) (unclassified)) (All F, (All L, (All CL, ((system_file_needs_level (system) F L) => ((admin_file_has_compartments (admin) F CL) => ((admin_file_has_level_h (admin) F L CL) => (admin_file_has_level (admin) F L))))))) ### DisjTree 38 40 41 % 0.18/0.40 43. (All L, ((admin_file_has_level (admin) (not_secretfile) L) => ((admin_indi_has_level (admin) (babu) L) => (admin_indi_has_level_for_file (admin) (babu) (not_secretfile))))) (All F, (All L, (All CL, ((system_file_needs_level (system) F L) => ((admin_file_has_compartments (admin) F CL) => ((admin_file_has_level_h (admin) F L CL) => (admin_file_has_level (admin) F L))))))) (system_file_needs_level (system) (not_secretfile) (unclassified)) (admin_file_has_compartments (admin) (not_secretfile) (nil)) (All F, (All L, (admin_file_has_level_h (admin) F L (nil)))) (All K, (admin_indi_has_level (admin) K (unclassified))) (-. (admin_indi_has_level_for_file (admin) (babu) (not_secretfile))) ### All 42 % 0.18/0.40 44. (All F, (All L, ((admin_file_has_level (admin) F L) => ((admin_indi_has_level (admin) (babu) L) => (admin_indi_has_level_for_file (admin) (babu) F))))) (-. (admin_indi_has_level_for_file (admin) (babu) (not_secretfile))) (All K, (admin_indi_has_level (admin) K (unclassified))) (All F, (All L, (admin_file_has_level_h (admin) F L (nil)))) (admin_file_has_compartments (admin) (not_secretfile) (nil)) (system_file_needs_level (system) (not_secretfile) (unclassified)) (All F, (All L, (All CL, ((system_file_needs_level (system) F L) => ((admin_file_has_compartments (admin) F CL) => ((admin_file_has_level_h (admin) F L CL) => (admin_file_has_level (admin) F L))))))) ### All 43 % 0.18/0.40 45. (All K, (All F, (All L, ((admin_file_has_level (admin) F L) => ((admin_indi_has_level (admin) K L) => (admin_indi_has_level_for_file (admin) K F)))))) (All F, (All L, (All CL, ((system_file_needs_level (system) F L) => ((admin_file_has_compartments (admin) F CL) => ((admin_file_has_level_h (admin) F L CL) => (admin_file_has_level (admin) F L))))))) (system_file_needs_level (system) (not_secretfile) (unclassified)) (admin_file_has_compartments (admin) (not_secretfile) (nil)) (All F, (All L, (admin_file_has_level_h (admin) F L (nil)))) (All K, (admin_indi_has_level (admin) K (unclassified))) (-. (admin_indi_has_level_for_file (admin) (babu) (not_secretfile))) ### All 44 % 0.18/0.40 46. (admin_file_has_compartments (admin) (not_secretfile) (nil)) (-. (admin_file_has_compartments (admin) (not_secretfile) (nil))) ### Axiom % 0.18/0.40 47. (-. (admin_indi_has_compartments (admin) (babu) (nil))) (admin_indi_has_compartments (admin) (babu) (nil)) ### Axiom % 0.18/0.40 48. (All K, (admin_indi_has_compartments (admin) K (nil))) (-. (admin_indi_has_compartments (admin) (babu) (nil))) ### All 47 % 0.18/0.40 49. (-. (admin_indi_has_compartments_for_file (admin) (babu) (not_secretfile))) (admin_indi_has_compartments_for_file (admin) (babu) (not_secretfile)) ### Axiom % 0.18/0.40 50. ((admin_file_has_compartments (admin) (not_secretfile) (nil)) => ((admin_indi_has_compartments (admin) (babu) (nil)) => (admin_indi_has_compartments_for_file (admin) (babu) (not_secretfile)))) (-. (admin_indi_has_compartments_for_file (admin) (babu) (not_secretfile))) (All K, (admin_indi_has_compartments (admin) K (nil))) (admin_file_has_compartments (admin) (not_secretfile) (nil)) ### DisjTree 46 48 49 % 0.18/0.40 51. (All CL, ((admin_file_has_compartments (admin) (not_secretfile) CL) => ((admin_indi_has_compartments (admin) (babu) CL) => (admin_indi_has_compartments_for_file (admin) (babu) (not_secretfile))))) (admin_file_has_compartments (admin) (not_secretfile) (nil)) (All K, (admin_indi_has_compartments (admin) K (nil))) (-. (admin_indi_has_compartments_for_file (admin) (babu) (not_secretfile))) ### All 50 % 0.18/0.40 52. (All F, (All CL, ((admin_file_has_compartments (admin) F CL) => ((admin_indi_has_compartments (admin) (babu) CL) => (admin_indi_has_compartments_for_file (admin) (babu) F))))) (-. (admin_indi_has_compartments_for_file (admin) (babu) (not_secretfile))) (All K, (admin_indi_has_compartments (admin) K (nil))) (admin_file_has_compartments (admin) (not_secretfile) (nil)) ### All 51 % 0.18/0.40 53. (All K, (All F, (All CL, ((admin_file_has_compartments (admin) F CL) => ((admin_indi_has_compartments (admin) K CL) => (admin_indi_has_compartments_for_file (admin) K F)))))) (admin_file_has_compartments (admin) (not_secretfile) (nil)) (All K, (admin_indi_has_compartments (admin) K (nil))) (-. (admin_indi_has_compartments_for_file (admin) (babu) (not_secretfile))) ### All 52 % 0.18/0.40 54. (-. (admin_indi_may_file (admin) (babu) (not_secretfile) (read))) (admin_indi_may_file (admin) (babu) (not_secretfile) (read)) ### Axiom % 0.18/0.40 55. ((state_file_is_not_working_paper (not_secretfile)) => ((admin_indi_has_citizenship_for_file (admin) (babu) (not_secretfile)) => ((admin_indi_has_need_to_know_for_file (admin) (babu) (not_secretfile)) => ((admin_indi_has_level_for_file (admin) (babu) (not_secretfile)) => ((admin_indi_has_compartments_for_file (admin) (babu) (not_secretfile)) => (admin_indi_may_file (admin) (babu) (not_secretfile) (read))))))) (-. (admin_indi_may_file (admin) (babu) (not_secretfile) (read))) (All K, (admin_indi_has_compartments (admin) K (nil))) (All K, (All F, (All CL, ((admin_file_has_compartments (admin) F CL) => ((admin_indi_has_compartments (admin) K CL) => (admin_indi_has_compartments_for_file (admin) K F)))))) (All K, (admin_indi_has_level (admin) K (unclassified))) (All F, (All L, (admin_file_has_level_h (admin) F L (nil)))) (system_file_needs_level (system) (not_secretfile) (unclassified)) (All F, (All L, (All CL, ((system_file_needs_level (system) F L) => ((admin_file_has_compartments (admin) F CL) => ((admin_file_has_level_h (admin) F L CL) => (admin_file_has_level (admin) F L))))))) (All K, (All F, (All L, ((admin_file_has_level (admin) F L) => ((admin_indi_has_level (admin) K L) => (admin_indi_has_level_for_file (admin) K F)))))) (owner_indi_has_need_to_know (owner_not_secretfile) (babu) (not_secretfile)) (state_file_has_owner (not_secretfile) (owner_not_secretfile)) (All K, (All F, (All OWR, ((state_file_has_owner F OWR) => ((owner_indi_has_need_to_know OWR K F) => (admin_indi_has_need_to_know_for_file (admin) K F)))))) (All K, (admin_indi_has_citizenship (admin) K (anycountry))) (All F, (All U, (admin_file_has_citizenship_h (admin) F U (nil)))) (admin_file_has_compartments (admin) (not_secretfile) (nil)) (system_file_needs_citizenship (system) (not_secretfile) (anycountry)) (All F, (All U, (All CL, ((system_file_needs_citizenship (system) F U) => ((admin_file_has_compartments (admin) F CL) => ((admin_file_has_citizenship_h (admin) F U CL) => (admin_file_has_citizenship (admin) F U))))))) (All K, (All F, (All L, ((admin_file_has_citizenship (admin) F L) => ((admin_indi_has_citizenship (admin) K L) => (admin_indi_has_citizenship_for_file (admin) K F)))))) (state_file_is_not_working_paper (not_secretfile)) ### DisjTree 4 21 28 45 53 54 % 0.18/0.40 56. (All F, ((state_file_is_not_working_paper F) => ((admin_indi_has_citizenship_for_file (admin) (babu) F) => ((admin_indi_has_need_to_know_for_file (admin) (babu) F) => ((admin_indi_has_level_for_file (admin) (babu) F) => ((admin_indi_has_compartments_for_file (admin) (babu) F) => (admin_indi_may_file (admin) (babu) F (read)))))))) (state_file_is_not_working_paper (not_secretfile)) (All K, (All F, (All L, ((admin_file_has_citizenship (admin) F L) => ((admin_indi_has_citizenship (admin) K L) => (admin_indi_has_citizenship_for_file (admin) K F)))))) (All F, (All U, (All CL, ((system_file_needs_citizenship (system) F U) => ((admin_file_has_compartments (admin) F CL) => ((admin_file_has_citizenship_h (admin) F U CL) => (admin_file_has_citizenship (admin) F U))))))) (system_file_needs_citizenship (system) (not_secretfile) (anycountry)) (admin_file_has_compartments (admin) (not_secretfile) (nil)) (All F, (All U, (admin_file_has_citizenship_h (admin) F U (nil)))) (All K, (admin_indi_has_citizenship (admin) K (anycountry))) (All K, (All F, (All OWR, ((state_file_has_owner F OWR) => ((owner_indi_has_need_to_know OWR K F) => (admin_indi_has_need_to_know_for_file (admin) K F)))))) (state_file_has_owner (not_secretfile) (owner_not_secretfile)) (owner_indi_has_need_to_know (owner_not_secretfile) (babu) (not_secretfile)) (All K, (All F, (All L, ((admin_file_has_level (admin) F L) => ((admin_indi_has_level (admin) K L) => (admin_indi_has_level_for_file (admin) K F)))))) (All F, (All L, (All CL, ((system_file_needs_level (system) F L) => ((admin_file_has_compartments (admin) F CL) => ((admin_file_has_level_h (admin) F L CL) => (admin_file_has_level (admin) F L))))))) (system_file_needs_level (system) (not_secretfile) (unclassified)) (All F, (All L, (admin_file_has_level_h (admin) F L (nil)))) (All K, (admin_indi_has_level (admin) K (unclassified))) (All K, (All F, (All CL, ((admin_file_has_compartments (admin) F CL) => ((admin_indi_has_compartments (admin) K CL) => (admin_indi_has_compartments_for_file (admin) K F)))))) (All K, (admin_indi_has_compartments (admin) K (nil))) (-. (admin_indi_may_file (admin) (babu) (not_secretfile) (read))) ### All 55 % 0.18/0.40 57. (All K, (All F, ((state_file_is_not_working_paper F) => ((admin_indi_has_citizenship_for_file (admin) K F) => ((admin_indi_has_need_to_know_for_file (admin) K F) => ((admin_indi_has_level_for_file (admin) K F) => ((admin_indi_has_compartments_for_file (admin) K F) => (admin_indi_may_file (admin) K F (read))))))))) (-. (admin_indi_may_file (admin) (babu) (not_secretfile) (read))) (All K, (admin_indi_has_compartments (admin) K (nil))) (All K, (All F, (All CL, ((admin_file_has_compartments (admin) F CL) => ((admin_indi_has_compartments (admin) K CL) => (admin_indi_has_compartments_for_file (admin) K F)))))) (All K, (admin_indi_has_level (admin) K (unclassified))) (All F, (All L, (admin_file_has_level_h (admin) F L (nil)))) (system_file_needs_level (system) (not_secretfile) (unclassified)) (All F, (All L, (All CL, ((system_file_needs_level (system) F L) => ((admin_file_has_compartments (admin) F CL) => ((admin_file_has_level_h (admin) F L CL) => (admin_file_has_level (admin) F L))))))) (All K, (All F, (All L, ((admin_file_has_level (admin) F L) => ((admin_indi_has_level (admin) K L) => (admin_indi_has_level_for_file (admin) K F)))))) (owner_indi_has_need_to_know (owner_not_secretfile) (babu) (not_secretfile)) (state_file_has_owner (not_secretfile) (owner_not_secretfile)) (All K, (All F, (All OWR, ((state_file_has_owner F OWR) => ((owner_indi_has_need_to_know OWR K F) => (admin_indi_has_need_to_know_for_file (admin) K F)))))) (All K, (admin_indi_has_citizenship (admin) K (anycountry))) (All F, (All U, (admin_file_has_citizenship_h (admin) F U (nil)))) (admin_file_has_compartments (admin) (not_secretfile) (nil)) (system_file_needs_citizenship (system) (not_secretfile) (anycountry)) (All F, (All U, (All CL, ((system_file_needs_citizenship (system) F U) => ((admin_file_has_compartments (admin) F CL) => ((admin_file_has_citizenship_h (admin) F U CL) => (admin_file_has_citizenship (admin) F U))))))) (All K, (All F, (All L, ((admin_file_has_citizenship (admin) F L) => ((admin_indi_has_citizenship (admin) K L) => (admin_indi_has_citizenship_for_file (admin) K F)))))) (state_file_is_not_working_paper (not_secretfile)) ### All 56 % 0.18/0.41 58. (system_file_needs_compartments (system) (not_secretfile) (nil)) (state_file_is_not_working_paper (not_secretfile)) (All K, (All F, (All L, ((admin_file_has_citizenship (admin) F L) => ((admin_indi_has_citizenship (admin) K L) => (admin_indi_has_citizenship_for_file (admin) K F)))))) (All F, (All U, (All CL, ((system_file_needs_citizenship (system) F U) => ((admin_file_has_compartments (admin) F CL) => ((admin_file_has_citizenship_h (admin) F U CL) => (admin_file_has_citizenship (admin) F U))))))) (system_file_needs_citizenship (system) (not_secretfile) (anycountry)) (All F, (All U, (admin_file_has_citizenship_h (admin) F U (nil)))) (All K, (admin_indi_has_citizenship (admin) K (anycountry))) (All K, (All F, (All OWR, ((state_file_has_owner F OWR) => ((owner_indi_has_need_to_know OWR K F) => (admin_indi_has_need_to_know_for_file (admin) K F)))))) (state_file_has_owner (not_secretfile) (owner_not_secretfile)) (owner_indi_has_need_to_know (owner_not_secretfile) (babu) (not_secretfile)) (All K, (All F, (All L, ((admin_file_has_level (admin) F L) => ((admin_indi_has_level (admin) K L) => (admin_indi_has_level_for_file (admin) K F)))))) (All F, (All L, (All CL, ((system_file_needs_level (system) F L) => ((admin_file_has_compartments (admin) F CL) => ((admin_file_has_level_h (admin) F L CL) => (admin_file_has_level (admin) F L))))))) (system_file_needs_level (system) (not_secretfile) (unclassified)) (All F, (All L, (admin_file_has_level_h (admin) F L (nil)))) (All K, (admin_indi_has_level (admin) K (unclassified))) (All K, (All F, (All CL, ((admin_file_has_compartments (admin) F CL) => ((admin_indi_has_compartments (admin) K CL) => (admin_indi_has_compartments_for_file (admin) K F)))))) (All K, (admin_indi_has_compartments (admin) K (nil))) (-. (admin_indi_may_file (admin) (babu) (not_secretfile) (read))) (All K, (All F, ((state_file_is_not_working_paper F) => ((admin_indi_has_citizenship_for_file (admin) K F) => ((admin_indi_has_need_to_know_for_file (admin) K F) => ((admin_indi_has_level_for_file (admin) K F) => ((admin_indi_has_compartments_for_file (admin) K F) => (admin_indi_may_file (admin) K F (read))))))))) (All F, (All CL, (admin_file_has_compartments_h (admin) F CL (nil)))) ### Extension/test/ax8 3 57 % 0.18/0.41 % SZS output end Proof % 0.18/0.41 (* END-PROOF *) %------------------------------------------------------------------------------