%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : SWV437+1 : TPTP v9.2.0. Released v4.0.0. % Transfm : none % Format : tptp:raw % Command : duper %s % 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 : 300s % DateTime : Fri Oct 3 08:05:06 PM UTC 2025 % Result : Theorem 11.27s 11.46s % Output : Proof 11.74s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.09 % Problem : SWV437+1 : TPTP v9.2.0. Released v4.0.0. % 0.09/0.10 % Command : duper %s % 0.09/0.31 % Computer : n025.cluster.edu % 0.09/0.31 % Model : x86_64 x86_64 % 0.09/0.31 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.09/0.31 % Memory : 8042.1875MB % 0.09/0.31 % OS : Linux 3.10.0-693.el7.x86_64 % 0.09/0.31 % CPULimit : 300 % 0.09/0.31 % WCLimit : 300 % 0.09/0.31 % DateTime : Thu Oct 2 13:19:08 EDT 2025 % 0.09/0.31 % CPUTime : % 11.27/11.46 SZS status Theorem for theBenchmark.p % 11.27/11.46 SZS output start Proof for theBenchmark.p % 11.27/11.46 Clause #1 (by assumption #[]): Eq (∀ (K : Iota), loca_level_direct_below K sbu confidential) True % 11.27/11.46 Clause #2 (by assumption #[]): Eq (∀ (K : Iota), loca_level_direct_below K confidential secret) True % 11.27/11.46 Clause #3 (by assumption #[]): Eq (∀ (K : Iota), loca_level_direct_below K secret topsecret) True % 11.27/11.46 Clause #4 (by assumption #[]): Eq (∀ (K L : Iota), loca_level_below K L L) True % 11.27/11.46 Clause #5 (by assumption #[]): Eq (∀ (K L L1 L11 : Iota), loca_level_direct_below K L1 L11 → loca_level_below K L L1 → loca_level_below K L L11) True % 11.27/11.46 Clause #6 (by assumption #[]): Eq (∀ (C SSO : Iota), system_compartment_has_sso system C SSO → admin_compartment_has_sso admin C SSO) True % 11.27/11.46 Clause #7 (by assumption #[]): Eq % 11.27/11.46 (∀ (OCA C SSO SCG : Iota), % 11.27/11.46 system_indi_is_oca system OCA → % 11.27/11.46 oca_compartment_has_scg OCA C SCG → % 11.27/11.46 admin_compartment_has_sso admin C SSO → % 11.27/11.46 sso_compartment_has_scg SSO C SCG → admin_compartment_has_scg admin C SCG) % 11.27/11.46 True % 11.27/11.46 Clause #8 (by assumption #[]): Eq % 11.27/11.46 (∀ (F CL : Iota), % 11.27/11.46 system_file_needs_compartments system F CL → % 11.27/11.46 admin_file_has_compartments_h admin F CL CL → admin_file_has_compartments admin F CL) % 11.27/11.46 True % 11.27/11.46 Clause #9 (by assumption #[]): Eq (∀ (F CL : Iota), admin_file_has_compartments_h admin F CL nil) True % 11.27/11.46 Clause #10 (by assumption #[]): Eq % 11.27/11.46 (∀ (F CL C1 CL1 SSO : Iota), % 11.27/11.46 admin_compartment_has_sso admin C1 SSO → % 11.27/11.46 sso_file_has_compartments SSO F CL → % 11.27/11.46 admin_file_has_compartments_h admin F CL CL1 → admin_file_has_compartments_h admin F CL (cons C1 CL1)) % 11.27/11.46 True % 11.27/11.46 Clause #11 (by assumption #[]): Eq % 11.27/11.46 (∀ (F L CL : Iota), % 11.27/11.46 system_file_needs_level system F L → % 11.27/11.46 admin_file_has_compartments admin F CL → admin_file_has_level_h admin F L CL → admin_file_has_level admin F L) % 11.27/11.46 True % 11.27/11.46 Clause #12 (by assumption #[]): Eq (∀ (F L : Iota), admin_file_has_level_h admin F L nil) True % 11.27/11.46 Clause #13 (by assumption #[]): Eq % 11.27/11.46 (∀ (F L C CL SSO SCG : Iota), % 11.27/11.46 admin_compartment_has_sso admin C SSO → % 11.27/11.46 admin_compartment_has_scg admin C SCG → % 11.27/11.46 sso_file_has_level SSO F L SCG → % 11.27/11.46 admin_file_has_level_h admin F L CL → admin_file_has_level_h admin F L (cons C CL)) % 11.27/11.46 True % 11.27/11.46 Clause #17 (by assumption #[]): Eq % 11.27/11.46 (∀ (K PA : Iota), % 11.27/11.46 system_indi_is_polygraph_admin system PA → % 11.27/11.46 polygraph_admin_indi_has_polygraph PA K → admin_indi_has_polygraph admin K) % 11.27/11.46 True % 11.27/11.46 Clause #18 (by assumption #[]): Eq % 11.27/11.46 (∀ (K CA : Iota), % 11.27/11.46 system_indi_is_credit_admin system CA → credit_admin_indi_has_credit CA K → admin_indi_has_credit admin K) % 11.27/11.46 True % 11.27/11.46 Clause #19 (by assumption #[]): Eq (∀ (K : Iota), admin_indi_has_background admin K unclassified) True % 11.27/11.46 Clause #20 (by assumption #[]): Eq % 11.27/11.46 (∀ (K L BA L1 : Iota), % 11.27/11.46 system_indi_is_background_admin system BA → % 11.27/11.46 background_admin_indi_has_background BA K L1 → loca_level_below admin L L1 → admin_indi_has_background admin K L) % 11.27/11.46 True % 11.27/11.46 Clause #21 (by assumption #[]): Eq % 11.27/11.46 (∀ (K HR : Iota), % 11.27/11.46 system_indi_is_hr_admin system HR → hr_admin_indi_has_employment HR K → admin_indi_has_employment admin K) % 11.27/11.46 True % 11.27/11.46 Clause #23 (by assumption #[]): Eq (∀ (K U : Iota), system_indi_has_citizenship system K U → admin_indi_has_citizenship admin K U) True % 11.27/11.46 Clause #25 (by assumption #[]): Eq % 11.27/11.46 (∀ (K L L1 LA L11 : Iota), % 11.27/11.46 system_indi_needs_level system K L1 → % 11.27/11.46 admin_indi_has_citizenship admin K usa → % 11.27/11.46 admin_indi_has_polygraph admin K → % 11.27/11.46 admin_indi_has_employment admin K → % 11.27/11.46 admin_indi_has_credit admin K → % 11.27/11.46 loca_level_below admin L L1 → % 11.27/11.46 system_indi_is_level_admin system LA → % 11.27/11.46 level_admin_indi_has_level LA K L11 → % 11.27/11.46 loca_level_below admin L L11 → admin_indi_has_background admin K L → admin_indi_has_level admin K L) % 11.27/11.46 True % 11.27/11.46 Clause #26 (by assumption #[]): Eq (∀ (K : Iota), admin_indi_has_compartments admin K nil) True % 11.27/11.46 Clause #27 (by assumption #[]): Eq % 11.27/11.46 (∀ (K C CL SSO : Iota), % 11.27/11.46 system_indi_needs_compartment system K C → % 11.27/11.47 admin_indi_has_employment admin K → % 11.27/11.47 admin_indi_has_citizenship admin K usa → % 11.27/11.47 admin_indi_has_polygraph_for_compartment admin K C → % 11.27/11.47 admin_indi_has_credit_for_compartment admin K C → % 11.27/11.47 admin_compartment_has_sso admin C SSO → % 11.27/11.47 sso_indi_has_compartment SSO K C → % 11.27/11.47 admin_indi_has_background_for_compartment admin K C → % 11.27/11.47 admin_indi_has_level_for_compartment admin K C → % 11.27/11.47 admin_indi_has_compartments admin K CL → admin_indi_has_compartments admin K (cons C CL)) % 11.27/11.47 True % 11.27/11.47 Clause #28 (by assumption #[]): Eq % 11.27/11.47 (∀ (K C OCA L1 L2 B1 B2 : Iota), % 11.27/11.47 system_indi_is_oca system OCA → % 11.27/11.47 oca_compartment_is_compartment OCA C L1 L2 B1 B2 → % 11.27/11.47 admin_indi_has_background admin K L2 → admin_indi_has_background_for_compartment admin K C) % 11.27/11.47 True % 11.27/11.47 Clause #29 (by assumption #[]): Eq % 11.27/11.47 (∀ (K C OCA L1 L2 B1 B2 : Iota), % 11.27/11.47 system_indi_is_oca system OCA → % 11.27/11.47 oca_compartment_is_compartment OCA C L1 L2 B1 B2 → % 11.27/11.47 admin_indi_has_level admin K L1 → admin_indi_has_level_for_compartment admin K C) % 11.27/11.47 True % 11.27/11.47 Clause #30 (by assumption #[]): Eq % 11.27/11.47 (∀ (K C OCA L1 L2 B1 : Iota), % 11.27/11.47 system_indi_is_oca system OCA → % 11.27/11.47 oca_compartment_is_compartment OCA C L1 L2 B1 yes → % 11.27/11.47 admin_indi_has_polygraph admin K → admin_indi_has_polygraph_for_compartment admin K C) % 11.27/11.47 True % 11.27/11.47 Clause #31 (by assumption #[]): Eq % 11.27/11.47 (∀ (K C OCA L1 L2 B1 : Iota), % 11.27/11.47 system_indi_is_oca system OCA → % 11.27/11.47 oca_compartment_is_compartment OCA C L1 L2 B1 no → admin_indi_has_polygraph_for_compartment admin K C) % 11.27/11.47 True % 11.27/11.47 Clause #32 (by assumption #[]): Eq % 11.27/11.47 (∀ (K C OCA L1 L2 B2 : Iota), % 11.27/11.47 system_indi_is_oca system OCA → % 11.27/11.47 oca_compartment_is_compartment OCA C L1 L2 yes B2 → % 11.27/11.47 admin_indi_has_credit admin K → admin_indi_has_credit_for_compartment admin K C) % 11.27/11.47 True % 11.27/11.47 Clause #33 (by assumption #[]): Eq % 11.27/11.47 (∀ (K C OCA L1 L2 B2 : Iota), % 11.27/11.47 system_indi_is_oca system OCA → % 11.27/11.47 oca_compartment_is_compartment OCA C L1 L2 no B2 → admin_indi_has_credit_for_compartment admin K C) % 11.27/11.47 True % 11.27/11.47 Clause #34 (by assumption #[]): Eq % 11.27/11.47 (∀ (K F CL : Iota), % 11.27/11.47 admin_file_has_compartments admin F CL → % 11.27/11.47 admin_indi_has_compartments admin K CL → admin_indi_has_compartments_for_file admin K F) % 11.27/11.47 True % 11.27/11.47 Clause #35 (by assumption #[]): Eq % 11.27/11.47 (∀ (K F L : Iota), % 11.27/11.47 admin_file_has_level admin F L → admin_indi_has_level admin K L → admin_indi_has_level_for_file admin K F) % 11.27/11.47 True % 11.27/11.47 Clause #36 (by assumption #[]): Eq % 11.27/11.47 (∀ (K F OWR : Iota), % 11.27/11.47 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) % 11.27/11.47 True % 11.27/11.47 Clause #38 (by assumption #[]): Eq (∀ (K F : Iota), admin_indi_has_citizenship admin K usa → admin_indi_has_citizenship_for_file admin K F) True % 11.27/11.47 Clause #39 (by assumption #[]): Eq % 11.27/11.47 (∀ (K F : Iota), % 11.27/11.47 state_file_is_not_working_paper F → % 11.27/11.47 admin_indi_has_citizenship_for_file admin K F → % 11.27/11.47 admin_indi_has_need_to_know_for_file admin K F → % 11.27/11.47 admin_indi_has_level_for_file admin K F → % 11.27/11.47 admin_indi_has_compartments_for_file admin K F → admin_indi_may_file admin K F read) % 11.27/11.47 True % 11.27/11.47 Clause #41 (by assumption #[]): Eq (system_indi_is_oca system oca) True % 11.27/11.47 Clause #42 (by assumption #[]): Eq (oca_compartment_is_compartment oca compartmentb confidential topsecret yes yes) True % 11.27/11.47 Clause #43 (by assumption #[]): Eq (oca_compartment_is_compartment oca compartmenta sbu unclassified no no) True % 11.27/11.47 Clause #44 (by assumption #[]): Eq (system_compartment_has_sso system compartmentb sso_compartmentb) True % 11.27/11.47 Clause #45 (by assumption #[]): Eq (oca_compartment_has_scg oca compartmentb scg_compartmentb) True % 11.27/11.47 Clause #46 (by assumption #[]): Eq (sso_compartment_has_scg sso_compartmentb compartmentb scg_compartmentb) True % 11.27/11.47 Clause #47 (by assumption #[]): Eq (system_compartment_has_sso system compartmenta sso_compartmenta) True % 11.27/11.47 Clause #48 (by assumption #[]): Eq (oca_compartment_has_scg oca compartmenta scg_compartmenta) True % 11.27/11.47 Clause #49 (by assumption #[]): Eq (sso_compartment_has_scg sso_compartmenta compartmenta scg_compartmenta) True % 11.27/11.49 Clause #50 (by assumption #[]): Eq (state_file_is_not_working_paper secretfile) True % 11.27/11.49 Clause #51 (by assumption #[]): Eq (system_file_needs_compartments system secretfile (cons compartmentb (cons compartmenta nil))) True % 11.27/11.49 Clause #52 (by assumption #[]): Eq (sso_file_has_compartments sso_compartmentb secretfile (cons compartmentb (cons compartmenta nil))) True % 11.27/11.49 Clause #53 (by assumption #[]): Eq (sso_file_has_compartments sso_compartmenta secretfile (cons compartmentb (cons compartmenta nil))) True % 11.27/11.49 Clause #54 (by assumption #[]): Eq (system_file_needs_level system secretfile secret) True % 11.27/11.49 Clause #55 (by assumption #[]): Eq (sso_file_has_level sso_compartmentb secretfile secret scg_compartmentb) True % 11.27/11.49 Clause #56 (by assumption #[]): Eq (sso_file_has_level sso_compartmenta secretfile secret scg_compartmenta) True % 11.27/11.49 Clause #60 (by assumption #[]): Eq (state_file_has_owner secretfile owner_secretfile) True % 11.27/11.49 Clause #66 (by assumption #[]): Eq (system_indi_is_polygraph_admin system polygraph_admin) True % 11.27/11.49 Clause #67 (by assumption #[]): Eq (system_indi_is_credit_admin system credit_admin) True % 11.27/11.49 Clause #68 (by assumption #[]): Eq (system_indi_is_background_admin system background_admin) True % 11.27/11.49 Clause #69 (by assumption #[]): Eq (system_indi_is_hr_admin system hr_admin) True % 11.27/11.49 Clause #70 (by assumption #[]): Eq (system_indi_is_level_admin system level_admin) True % 11.27/11.49 Clause #71 (by assumption #[]): Eq (system_indi_has_citizenship system alice usa) True % 11.27/11.49 Clause #72 (by assumption #[]): Eq (polygraph_admin_indi_has_polygraph polygraph_admin alice) True % 11.27/11.49 Clause #73 (by assumption #[]): Eq (credit_admin_indi_has_credit credit_admin alice) True % 11.27/11.49 Clause #74 (by assumption #[]): Eq (background_admin_indi_has_background background_admin alice topsecret) True % 11.27/11.49 Clause #75 (by assumption #[]): Eq (hr_admin_indi_has_employment hr_admin alice) True % 11.27/11.49 Clause #76 (by assumption #[]): Eq (system_indi_needs_level system alice secret) True % 11.27/11.49 Clause #77 (by assumption #[]): Eq (level_admin_indi_has_level level_admin alice topsecret) True % 11.27/11.49 Clause #78 (by assumption #[]): Eq (system_indi_needs_compartment system alice compartmentb) True % 11.27/11.49 Clause #79 (by assumption #[]): Eq (system_indi_needs_compartment system alice compartmenta) True % 11.27/11.49 Clause #80 (by assumption #[]): Eq (sso_indi_has_compartment sso_compartmentb alice compartmentb) True % 11.27/11.49 Clause #81 (by assumption #[]): Eq (sso_indi_has_compartment sso_compartmenta alice compartmenta) True % 11.27/11.49 Clause #82 (by assumption #[]): Eq (owner_indi_has_need_to_know owner_secretfile alice secretfile) True % 11.27/11.49 Clause #87 (by assumption #[]): Eq (Not (admin_indi_may_file admin alice secretfile read)) True % 11.27/11.49 Clause #89 (by clausification #[1]): ∀ (a : Iota), Eq (loca_level_direct_below a sbu confidential) True % 11.27/11.49 Clause #90 (by clausification #[2]): ∀ (a : Iota), Eq (loca_level_direct_below a confidential secret) True % 11.27/11.49 Clause #91 (by clausification #[3]): ∀ (a : Iota), Eq (loca_level_direct_below a secret topsecret) True % 11.27/11.49 Clause #92 (by clausification #[4]): ∀ (a : Iota), Eq (∀ (L : Iota), loca_level_below a L L) True % 11.27/11.49 Clause #93 (by clausification #[92]): ∀ (a a_1 : Iota), Eq (loca_level_below a a_1 a_1) True % 11.27/11.49 Clause #94 (by clausification #[5]): ∀ (a : Iota), % 11.27/11.49 Eq (∀ (L L1 L11 : Iota), loca_level_direct_below a L1 L11 → loca_level_below a L L1 → loca_level_below a L L11) True % 11.27/11.49 Clause #95 (by clausification #[94]): ∀ (a a_1 : Iota), % 11.27/11.49 Eq (∀ (L1 L11 : Iota), loca_level_direct_below a L1 L11 → loca_level_below a a_1 L1 → loca_level_below a a_1 L11) True % 11.27/11.49 Clause #96 (by clausification #[95]): ∀ (a a_1 a_2 : Iota), % 11.27/11.49 Eq (∀ (L11 : Iota), loca_level_direct_below a a_1 L11 → loca_level_below a a_2 a_1 → loca_level_below a a_2 L11) True % 11.27/11.49 Clause #97 (by clausification #[96]): ∀ (a a_1 a_2 a_3 : Iota), % 11.27/11.49 Eq (loca_level_direct_below a a_1 a_2 → loca_level_below a a_3 a_1 → loca_level_below a a_3 a_2) True % 11.27/11.49 Clause #98 (by clausification #[97]): ∀ (a a_1 a_2 a_3 : Iota), % 11.27/11.49 Or (Eq (loca_level_direct_below a a_1 a_2) False) (Eq (loca_level_below a a_3 a_1 → loca_level_below a a_3 a_2) True) % 11.27/11.50 Clause #99 (by clausification #[98]): ∀ (a a_1 a_2 a_3 : Iota), % 11.27/11.50 Or (Eq (loca_level_direct_below a a_1 a_2) False) % 11.27/11.50 (Or (Eq (loca_level_below a a_3 a_1) False) (Eq (loca_level_below a a_3 a_2) True)) % 11.27/11.50 Clause #101 (by superposition #[99, 89]): ∀ (a a_1 : Iota), % 11.27/11.50 Or (Eq (loca_level_below a a_1 sbu) False) (Or (Eq (loca_level_below a a_1 confidential) True) (Eq False True)) % 11.27/11.50 Clause #102 (by superposition #[99, 90]): ∀ (a a_1 : Iota), % 11.27/11.50 Or (Eq (loca_level_below a a_1 confidential) False) (Or (Eq (loca_level_below a a_1 secret) True) (Eq False True)) % 11.27/11.50 Clause #103 (by superposition #[99, 91]): ∀ (a a_1 : Iota), % 11.27/11.50 Or (Eq (loca_level_below a a_1 secret) False) (Or (Eq (loca_level_below a a_1 topsecret) True) (Eq False True)) % 11.27/11.50 Clause #104 (by clausification #[6]): ∀ (a : Iota), Eq (∀ (SSO : Iota), system_compartment_has_sso system a SSO → admin_compartment_has_sso admin a SSO) True % 11.27/11.50 Clause #105 (by clausification #[104]): ∀ (a a_1 : Iota), Eq (system_compartment_has_sso system a a_1 → admin_compartment_has_sso admin a a_1) True % 11.27/11.50 Clause #106 (by clausification #[105]): ∀ (a a_1 : Iota), % 11.27/11.50 Or (Eq (system_compartment_has_sso system a a_1) False) (Eq (admin_compartment_has_sso admin a a_1) True) % 11.27/11.50 Clause #107 (by superposition #[106, 47]): Or (Eq (admin_compartment_has_sso admin compartmenta sso_compartmenta) True) (Eq False True) % 11.27/11.50 Clause #108 (by superposition #[44, 106]): Or (Eq (admin_compartment_has_sso admin compartmentb sso_compartmentb) True) (Eq False True) % 11.27/11.50 Clause #109 (by clausification #[7]): ∀ (a : Iota), % 11.27/11.50 Eq % 11.27/11.50 (∀ (C SSO SCG : Iota), % 11.27/11.50 system_indi_is_oca system a → % 11.27/11.50 oca_compartment_has_scg a C SCG → % 11.27/11.50 admin_compartment_has_sso admin C SSO → % 11.27/11.50 sso_compartment_has_scg SSO C SCG → admin_compartment_has_scg admin C SCG) % 11.27/11.50 True % 11.27/11.50 Clause #110 (by clausification #[109]): ∀ (a a_1 : Iota), % 11.27/11.50 Eq % 11.27/11.50 (∀ (SSO SCG : Iota), % 11.27/11.50 system_indi_is_oca system a → % 11.27/11.50 oca_compartment_has_scg a a_1 SCG → % 11.27/11.50 admin_compartment_has_sso admin a_1 SSO → % 11.27/11.50 sso_compartment_has_scg SSO a_1 SCG → admin_compartment_has_scg admin a_1 SCG) % 11.27/11.50 True % 11.27/11.50 Clause #111 (by clausification #[110]): ∀ (a a_1 a_2 : Iota), % 11.27/11.50 Eq % 11.27/11.50 (∀ (SCG : Iota), % 11.27/11.50 system_indi_is_oca system a → % 11.27/11.50 oca_compartment_has_scg a a_1 SCG → % 11.27/11.50 admin_compartment_has_sso admin a_1 a_2 → % 11.27/11.50 sso_compartment_has_scg a_2 a_1 SCG → admin_compartment_has_scg admin a_1 SCG) % 11.27/11.50 True % 11.27/11.50 Clause #112 (by clausification #[111]): ∀ (a a_1 a_2 a_3 : Iota), % 11.27/11.50 Eq % 11.27/11.50 (system_indi_is_oca system a → % 11.27/11.50 oca_compartment_has_scg a a_1 a_2 → % 11.27/11.50 admin_compartment_has_sso admin a_1 a_3 → % 11.27/11.50 sso_compartment_has_scg a_3 a_1 a_2 → admin_compartment_has_scg admin a_1 a_2) % 11.27/11.50 True % 11.27/11.50 Clause #113 (by clausification #[112]): ∀ (a a_1 a_2 a_3 : Iota), % 11.27/11.50 Or (Eq (system_indi_is_oca system a) False) % 11.27/11.50 (Eq % 11.27/11.50 (oca_compartment_has_scg a a_1 a_2 → % 11.27/11.50 admin_compartment_has_sso admin a_1 a_3 → % 11.27/11.50 sso_compartment_has_scg a_3 a_1 a_2 → admin_compartment_has_scg admin a_1 a_2) % 11.27/11.50 True) % 11.27/11.50 Clause #114 (by clausification #[113]): ∀ (a a_1 a_2 a_3 : Iota), % 11.27/11.50 Or (Eq (system_indi_is_oca system a) False) % 11.27/11.50 (Or (Eq (oca_compartment_has_scg a a_1 a_2) False) % 11.27/11.50 (Eq % 11.27/11.50 (admin_compartment_has_sso admin a_1 a_3 → % 11.27/11.50 sso_compartment_has_scg a_3 a_1 a_2 → admin_compartment_has_scg admin a_1 a_2) % 11.27/11.50 True)) % 11.27/11.50 Clause #115 (by clausification #[114]): ∀ (a a_1 a_2 a_3 : Iota), % 11.27/11.50 Or (Eq (system_indi_is_oca system a) False) % 11.27/11.50 (Or (Eq (oca_compartment_has_scg a a_1 a_2) False) % 11.27/11.50 (Or (Eq (admin_compartment_has_sso admin a_1 a_3) False) % 11.27/11.50 (Eq (sso_compartment_has_scg a_3 a_1 a_2 → admin_compartment_has_scg admin a_1 a_2) True))) % 11.27/11.50 Clause #116 (by clausification #[115]): ∀ (a a_1 a_2 a_3 : Iota), % 11.27/11.50 Or (Eq (system_indi_is_oca system a) False) % 11.27/11.50 (Or (Eq (oca_compartment_has_scg a a_1 a_2) False) % 11.27/11.50 (Or (Eq (admin_compartment_has_sso admin a_1 a_3) False) % 11.27/11.50 (Or (Eq (sso_compartment_has_scg a_3 a_1 a_2) False) (Eq (admin_compartment_has_scg admin a_1 a_2) True)))) % 11.27/11.52 Clause #117 (by superposition #[116, 41]): ∀ (a a_1 a_2 : Iota), % 11.27/11.52 Or (Eq (oca_compartment_has_scg oca a a_1) False) % 11.27/11.52 (Or (Eq (admin_compartment_has_sso admin a a_2) False) % 11.27/11.52 (Or (Eq (sso_compartment_has_scg a_2 a a_1) False) % 11.27/11.52 (Or (Eq (admin_compartment_has_scg admin a a_1) True) (Eq False True)))) % 11.27/11.52 Clause #118 (by clausification #[26]): ∀ (a : Iota), Eq (admin_indi_has_compartments admin a nil) True % 11.27/11.52 Clause #121 (by clausification #[19]): ∀ (a : Iota), Eq (admin_indi_has_background admin a unclassified) True % 11.27/11.52 Clause #122 (by clausification #[8]): ∀ (a : Iota), % 11.27/11.52 Eq % 11.27/11.52 (∀ (CL : Iota), % 11.27/11.52 system_file_needs_compartments system a CL → % 11.27/11.52 admin_file_has_compartments_h admin a CL CL → admin_file_has_compartments admin a CL) % 11.27/11.52 True % 11.27/11.52 Clause #123 (by clausification #[122]): ∀ (a a_1 : Iota), % 11.27/11.52 Eq % 11.27/11.52 (system_file_needs_compartments system a a_1 → % 11.27/11.52 admin_file_has_compartments_h admin a a_1 a_1 → admin_file_has_compartments admin a a_1) % 11.27/11.52 True % 11.27/11.52 Clause #124 (by clausification #[123]): ∀ (a a_1 : Iota), % 11.27/11.52 Or (Eq (system_file_needs_compartments system a a_1) False) % 11.27/11.52 (Eq (admin_file_has_compartments_h admin a a_1 a_1 → admin_file_has_compartments admin a a_1) True) % 11.27/11.52 Clause #125 (by clausification #[124]): ∀ (a a_1 : Iota), % 11.27/11.52 Or (Eq (system_file_needs_compartments system a a_1) False) % 11.27/11.52 (Or (Eq (admin_file_has_compartments_h admin a a_1 a_1) False) (Eq (admin_file_has_compartments admin a a_1) True)) % 11.27/11.52 Clause #127 (by clausification #[87]): Eq (admin_indi_may_file admin alice secretfile read) False % 11.27/11.52 Clause #128 (by clausification #[107]): Eq (admin_compartment_has_sso admin compartmenta sso_compartmenta) True % 11.27/11.52 Clause #129 (by clausification #[108]): Eq (admin_compartment_has_sso admin compartmentb sso_compartmentb) True % 11.27/11.52 Clause #130 (by clausification #[18]): ∀ (a : Iota), % 11.27/11.52 Eq % 11.27/11.52 (∀ (CA : Iota), % 11.27/11.52 system_indi_is_credit_admin system CA → credit_admin_indi_has_credit CA a → admin_indi_has_credit admin a) % 11.27/11.52 True % 11.27/11.52 Clause #131 (by clausification #[130]): ∀ (a a_1 : Iota), % 11.27/11.52 Eq (system_indi_is_credit_admin system a → credit_admin_indi_has_credit a a_1 → admin_indi_has_credit admin a_1) True % 11.27/11.52 Clause #132 (by clausification #[131]): ∀ (a a_1 : Iota), % 11.27/11.52 Or (Eq (system_indi_is_credit_admin system a) False) % 11.27/11.52 (Eq (credit_admin_indi_has_credit a a_1 → admin_indi_has_credit admin a_1) True) % 11.27/11.52 Clause #133 (by clausification #[132]): ∀ (a a_1 : Iota), % 11.27/11.52 Or (Eq (system_indi_is_credit_admin system a) False) % 11.27/11.52 (Or (Eq (credit_admin_indi_has_credit a a_1) False) (Eq (admin_indi_has_credit admin a_1) True)) % 11.27/11.52 Clause #134 (by superposition #[133, 67]): ∀ (a : Iota), % 11.27/11.52 Or (Eq (credit_admin_indi_has_credit credit_admin a) False) % 11.27/11.52 (Or (Eq (admin_indi_has_credit admin a) True) (Eq False True)) % 11.27/11.52 Clause #135 (by clausification #[17]): ∀ (a : Iota), % 11.27/11.52 Eq % 11.27/11.52 (∀ (PA : Iota), % 11.27/11.52 system_indi_is_polygraph_admin system PA → % 11.27/11.52 polygraph_admin_indi_has_polygraph PA a → admin_indi_has_polygraph admin a) % 11.27/11.52 True % 11.27/11.52 Clause #136 (by clausification #[135]): ∀ (a a_1 : Iota), % 11.27/11.52 Eq % 11.27/11.52 (system_indi_is_polygraph_admin system a → % 11.27/11.52 polygraph_admin_indi_has_polygraph a a_1 → admin_indi_has_polygraph admin a_1) % 11.27/11.52 True % 11.27/11.52 Clause #137 (by clausification #[136]): ∀ (a a_1 : Iota), % 11.27/11.52 Or (Eq (system_indi_is_polygraph_admin system a) False) % 11.27/11.52 (Eq (polygraph_admin_indi_has_polygraph a a_1 → admin_indi_has_polygraph admin a_1) True) % 11.27/11.52 Clause #138 (by clausification #[137]): ∀ (a a_1 : Iota), % 11.27/11.52 Or (Eq (system_indi_is_polygraph_admin system a) False) % 11.27/11.52 (Or (Eq (polygraph_admin_indi_has_polygraph a a_1) False) (Eq (admin_indi_has_polygraph admin a_1) True)) % 11.27/11.52 Clause #139 (by superposition #[138, 66]): ∀ (a : Iota), % 11.27/11.52 Or (Eq (polygraph_admin_indi_has_polygraph polygraph_admin a) False) % 11.27/11.52 (Or (Eq (admin_indi_has_polygraph admin a) True) (Eq False True)) % 11.27/11.52 Clause #140 (by clausification #[9]): ∀ (a : Iota), Eq (∀ (CL : Iota), admin_file_has_compartments_h admin a CL nil) True % 11.27/11.52 Clause #141 (by clausification #[140]): ∀ (a a_1 : Iota), Eq (admin_file_has_compartments_h admin a a_1 nil) True % 11.37/11.53 Clause #142 (by clausification #[38]): ∀ (a : Iota), % 11.37/11.53 Eq (∀ (F : Iota), admin_indi_has_citizenship admin a usa → admin_indi_has_citizenship_for_file admin a F) True % 11.37/11.53 Clause #143 (by clausification #[142]): ∀ (a a_1 : Iota), Eq (admin_indi_has_citizenship admin a usa → admin_indi_has_citizenship_for_file admin a a_1) True % 11.37/11.53 Clause #144 (by clausification #[143]): ∀ (a a_1 : Iota), % 11.37/11.53 Or (Eq (admin_indi_has_citizenship admin a usa) False) (Eq (admin_indi_has_citizenship_for_file admin a a_1) True) % 11.37/11.53 Clause #145 (by clausification #[23]): ∀ (a : Iota), Eq (∀ (U : Iota), system_indi_has_citizenship system a U → admin_indi_has_citizenship admin a U) True % 11.37/11.53 Clause #146 (by clausification #[145]): ∀ (a a_1 : Iota), Eq (system_indi_has_citizenship system a a_1 → admin_indi_has_citizenship admin a a_1) True % 11.37/11.53 Clause #147 (by clausification #[146]): ∀ (a a_1 : Iota), % 11.37/11.53 Or (Eq (system_indi_has_citizenship system a a_1) False) (Eq (admin_indi_has_citizenship admin a a_1) True) % 11.37/11.53 Clause #148 (by superposition #[147, 71]): Or (Eq (admin_indi_has_citizenship admin alice usa) True) (Eq False True) % 11.37/11.53 Clause #151 (by clausification #[10]): ∀ (a : Iota), % 11.37/11.53 Eq % 11.37/11.53 (∀ (CL C1 CL1 SSO : Iota), % 11.37/11.53 admin_compartment_has_sso admin C1 SSO → % 11.37/11.53 sso_file_has_compartments SSO a CL → % 11.37/11.53 admin_file_has_compartments_h admin a CL CL1 → admin_file_has_compartments_h admin a CL (cons C1 CL1)) % 11.37/11.53 True % 11.37/11.53 Clause #152 (by clausification #[151]): ∀ (a a_1 : Iota), % 11.37/11.53 Eq % 11.37/11.53 (∀ (C1 CL1 SSO : Iota), % 11.37/11.53 admin_compartment_has_sso admin C1 SSO → % 11.37/11.53 sso_file_has_compartments SSO a a_1 → % 11.37/11.53 admin_file_has_compartments_h admin a a_1 CL1 → admin_file_has_compartments_h admin a a_1 (cons C1 CL1)) % 11.37/11.53 True % 11.37/11.53 Clause #153 (by clausification #[152]): ∀ (a a_1 a_2 : Iota), % 11.37/11.53 Eq % 11.37/11.53 (∀ (CL1 SSO : Iota), % 11.37/11.53 admin_compartment_has_sso admin a SSO → % 11.37/11.53 sso_file_has_compartments SSO a_1 a_2 → % 11.37/11.53 admin_file_has_compartments_h admin a_1 a_2 CL1 → admin_file_has_compartments_h admin a_1 a_2 (cons a CL1)) % 11.37/11.53 True % 11.37/11.53 Clause #154 (by clausification #[153]): ∀ (a a_1 a_2 a_3 : Iota), % 11.37/11.53 Eq % 11.37/11.53 (∀ (SSO : Iota), % 11.37/11.53 admin_compartment_has_sso admin a SSO → % 11.37/11.53 sso_file_has_compartments SSO a_1 a_2 → % 11.37/11.53 admin_file_has_compartments_h admin a_1 a_2 a_3 → admin_file_has_compartments_h admin a_1 a_2 (cons a a_3)) % 11.37/11.53 True % 11.37/11.53 Clause #155 (by clausification #[154]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 11.37/11.53 Eq % 11.37/11.53 (admin_compartment_has_sso admin a a_1 → % 11.37/11.53 sso_file_has_compartments a_1 a_2 a_3 → % 11.37/11.53 admin_file_has_compartments_h admin a_2 a_3 a_4 → admin_file_has_compartments_h admin a_2 a_3 (cons a a_4)) % 11.37/11.53 True % 11.37/11.53 Clause #156 (by clausification #[155]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 11.37/11.53 Or (Eq (admin_compartment_has_sso admin a a_1) False) % 11.37/11.53 (Eq % 11.37/11.53 (sso_file_has_compartments a_1 a_2 a_3 → % 11.37/11.53 admin_file_has_compartments_h admin a_2 a_3 a_4 → admin_file_has_compartments_h admin a_2 a_3 (cons a a_4)) % 11.37/11.53 True) % 11.37/11.53 Clause #157 (by clausification #[156]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 11.37/11.53 Or (Eq (admin_compartment_has_sso admin a a_1) False) % 11.37/11.53 (Or (Eq (sso_file_has_compartments a_1 a_2 a_3) False) % 11.37/11.53 (Eq (admin_file_has_compartments_h admin a_2 a_3 a_4 → admin_file_has_compartments_h admin a_2 a_3 (cons a a_4)) % 11.37/11.53 True)) % 11.37/11.53 Clause #158 (by clausification #[157]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 11.37/11.53 Or (Eq (admin_compartment_has_sso admin a a_1) False) % 11.37/11.53 (Or (Eq (sso_file_has_compartments a_1 a_2 a_3) False) % 11.37/11.53 (Or (Eq (admin_file_has_compartments_h admin a_2 a_3 a_4) False) % 11.37/11.53 (Eq (admin_file_has_compartments_h admin a_2 a_3 (cons a a_4)) True))) % 11.37/11.53 Clause #159 (by superposition #[158, 128]): ∀ (a a_1 a_2 : Iota), % 11.37/11.53 Or (Eq (sso_file_has_compartments sso_compartmenta a a_1) False) % 11.37/11.53 (Or (Eq (admin_file_has_compartments_h admin a a_1 a_2) False) % 11.37/11.53 (Or (Eq (admin_file_has_compartments_h admin a a_1 (cons compartmenta a_2)) True) (Eq False True))) % 11.37/11.53 Clause #160 (by superposition #[158, 129]): ∀ (a a_1 a_2 : Iota), % 11.37/11.55 Or (Eq (sso_file_has_compartments sso_compartmentb a a_1) False) % 11.37/11.55 (Or (Eq (admin_file_has_compartments_h admin a a_1 a_2) False) % 11.37/11.55 (Or (Eq (admin_file_has_compartments_h admin a a_1 (cons compartmentb a_2)) True) (Eq False True))) % 11.37/11.55 Clause #161 (by clausification #[148]): Eq (admin_indi_has_citizenship admin alice usa) True % 11.37/11.55 Clause #162 (by superposition #[161, 144]): ∀ (a : Iota), Or (Eq True False) (Eq (admin_indi_has_citizenship_for_file admin alice a) True) % 11.37/11.55 Clause #163 (by clausification #[162]): ∀ (a : Iota), Eq (admin_indi_has_citizenship_for_file admin alice a) True % 11.37/11.55 Clause #164 (by clausification #[21]): ∀ (a : Iota), % 11.37/11.55 Eq % 11.37/11.55 (∀ (HR : Iota), % 11.37/11.55 system_indi_is_hr_admin system HR → hr_admin_indi_has_employment HR a → admin_indi_has_employment admin a) % 11.37/11.55 True % 11.37/11.55 Clause #165 (by clausification #[164]): ∀ (a a_1 : Iota), % 11.37/11.55 Eq (system_indi_is_hr_admin system a → hr_admin_indi_has_employment a a_1 → admin_indi_has_employment admin a_1) True % 11.37/11.55 Clause #166 (by clausification #[165]): ∀ (a a_1 : Iota), % 11.37/11.55 Or (Eq (system_indi_is_hr_admin system a) False) % 11.37/11.55 (Eq (hr_admin_indi_has_employment a a_1 → admin_indi_has_employment admin a_1) True) % 11.37/11.55 Clause #167 (by clausification #[166]): ∀ (a a_1 : Iota), % 11.37/11.55 Or (Eq (system_indi_is_hr_admin system a) False) % 11.37/11.55 (Or (Eq (hr_admin_indi_has_employment a a_1) False) (Eq (admin_indi_has_employment admin a_1) True)) % 11.37/11.55 Clause #168 (by superposition #[167, 69]): ∀ (a : Iota), % 11.37/11.55 Or (Eq (hr_admin_indi_has_employment hr_admin a) False) % 11.37/11.55 (Or (Eq (admin_indi_has_employment admin a) True) (Eq False True)) % 11.37/11.55 Clause #171 (by clausification #[12]): ∀ (a : Iota), Eq (∀ (L : Iota), admin_file_has_level_h admin a L nil) True % 11.37/11.55 Clause #172 (by clausification #[171]): ∀ (a a_1 : Iota), Eq (admin_file_has_level_h admin a a_1 nil) True % 11.37/11.55 Clause #173 (by clausification #[11]): ∀ (a : Iota), % 11.37/11.55 Eq % 11.37/11.55 (∀ (L CL : Iota), % 11.37/11.55 system_file_needs_level system a L → % 11.37/11.55 admin_file_has_compartments admin a CL → admin_file_has_level_h admin a L CL → admin_file_has_level admin a L) % 11.37/11.55 True % 11.37/11.55 Clause #174 (by clausification #[173]): ∀ (a a_1 : Iota), % 11.37/11.55 Eq % 11.37/11.55 (∀ (CL : Iota), % 11.37/11.55 system_file_needs_level system a a_1 → % 11.37/11.55 admin_file_has_compartments admin a CL → % 11.37/11.55 admin_file_has_level_h admin a a_1 CL → admin_file_has_level admin a a_1) % 11.37/11.55 True % 11.37/11.55 Clause #175 (by clausification #[174]): ∀ (a a_1 a_2 : Iota), % 11.37/11.55 Eq % 11.37/11.55 (system_file_needs_level system a a_1 → % 11.37/11.55 admin_file_has_compartments admin a a_2 → % 11.37/11.55 admin_file_has_level_h admin a a_1 a_2 → admin_file_has_level admin a a_1) % 11.37/11.55 True % 11.37/11.55 Clause #176 (by clausification #[175]): ∀ (a a_1 a_2 : Iota), % 11.37/11.55 Or (Eq (system_file_needs_level system a a_1) False) % 11.37/11.55 (Eq % 11.37/11.55 (admin_file_has_compartments admin a a_2 → % 11.37/11.55 admin_file_has_level_h admin a a_1 a_2 → admin_file_has_level admin a a_1) % 11.37/11.55 True) % 11.37/11.55 Clause #177 (by clausification #[176]): ∀ (a a_1 a_2 : Iota), % 11.37/11.55 Or (Eq (system_file_needs_level system a a_1) False) % 11.37/11.55 (Or (Eq (admin_file_has_compartments admin a a_2) False) % 11.37/11.55 (Eq (admin_file_has_level_h admin a a_1 a_2 → admin_file_has_level admin a a_1) True)) % 11.37/11.55 Clause #178 (by clausification #[177]): ∀ (a a_1 a_2 : Iota), % 11.37/11.55 Or (Eq (system_file_needs_level system a a_1) False) % 11.37/11.55 (Or (Eq (admin_file_has_compartments admin a a_2) False) % 11.37/11.55 (Or (Eq (admin_file_has_level_h admin a a_1 a_2) False) (Eq (admin_file_has_level admin a a_1) True))) % 11.37/11.55 Clause #179 (by superposition #[178, 54]): ∀ (a : Iota), % 11.37/11.55 Or (Eq (admin_file_has_compartments admin secretfile a) False) % 11.37/11.55 (Or (Eq (admin_file_has_level_h admin secretfile secret a) False) % 11.37/11.55 (Or (Eq (admin_file_has_level admin secretfile secret) True) (Eq False True))) % 11.37/11.55 Clause #181 (by superposition #[51, 125]): Or % 11.37/11.55 (Eq % 11.37/11.55 (admin_file_has_compartments_h admin secretfile (cons compartmentb (cons compartmenta nil)) % 11.37/11.55 (cons compartmentb (cons compartmenta nil))) % 11.37/11.55 False) % 11.37/11.55 (Or (Eq (admin_file_has_compartments admin secretfile (cons compartmentb (cons compartmenta nil))) True) % 11.37/11.57 (Eq False True)) % 11.37/11.57 Clause #182 (by clausification #[134]): ∀ (a : Iota), Or (Eq (credit_admin_indi_has_credit credit_admin a) False) (Eq (admin_indi_has_credit admin a) True) % 11.37/11.57 Clause #183 (by superposition #[182, 73]): Or (Eq (admin_indi_has_credit admin alice) True) (Eq False True) % 11.37/11.57 Clause #184 (by clausification #[183]): Eq (admin_indi_has_credit admin alice) True % 11.37/11.57 Clause #185 (by clausification #[13]): ∀ (a : Iota), % 11.37/11.57 Eq % 11.37/11.57 (∀ (L C CL SSO SCG : Iota), % 11.37/11.57 admin_compartment_has_sso admin C SSO → % 11.37/11.57 admin_compartment_has_scg admin C SCG → % 11.37/11.57 sso_file_has_level SSO a L SCG → % 11.37/11.57 admin_file_has_level_h admin a L CL → admin_file_has_level_h admin a L (cons C CL)) % 11.37/11.57 True % 11.37/11.57 Clause #186 (by clausification #[185]): ∀ (a a_1 : Iota), % 11.37/11.57 Eq % 11.37/11.57 (∀ (C CL SSO SCG : Iota), % 11.37/11.57 admin_compartment_has_sso admin C SSO → % 11.37/11.57 admin_compartment_has_scg admin C SCG → % 11.37/11.57 sso_file_has_level SSO a a_1 SCG → % 11.37/11.57 admin_file_has_level_h admin a a_1 CL → admin_file_has_level_h admin a a_1 (cons C CL)) % 11.37/11.57 True % 11.37/11.57 Clause #187 (by clausification #[186]): ∀ (a a_1 a_2 : Iota), % 11.37/11.57 Eq % 11.37/11.57 (∀ (CL SSO SCG : Iota), % 11.37/11.57 admin_compartment_has_sso admin a SSO → % 11.37/11.57 admin_compartment_has_scg admin a SCG → % 11.37/11.57 sso_file_has_level SSO a_1 a_2 SCG → % 11.37/11.57 admin_file_has_level_h admin a_1 a_2 CL → admin_file_has_level_h admin a_1 a_2 (cons a CL)) % 11.37/11.57 True % 11.37/11.57 Clause #188 (by clausification #[187]): ∀ (a a_1 a_2 a_3 : Iota), % 11.37/11.57 Eq % 11.37/11.57 (∀ (SSO SCG : Iota), % 11.37/11.57 admin_compartment_has_sso admin a SSO → % 11.37/11.57 admin_compartment_has_scg admin a SCG → % 11.37/11.57 sso_file_has_level SSO a_1 a_2 SCG → % 11.37/11.57 admin_file_has_level_h admin a_1 a_2 a_3 → admin_file_has_level_h admin a_1 a_2 (cons a a_3)) % 11.37/11.57 True % 11.37/11.57 Clause #189 (by clausification #[188]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 11.37/11.57 Eq % 11.37/11.57 (∀ (SCG : Iota), % 11.37/11.57 admin_compartment_has_sso admin a a_1 → % 11.37/11.57 admin_compartment_has_scg admin a SCG → % 11.37/11.57 sso_file_has_level a_1 a_2 a_3 SCG → % 11.37/11.57 admin_file_has_level_h admin a_2 a_3 a_4 → admin_file_has_level_h admin a_2 a_3 (cons a a_4)) % 11.37/11.57 True % 11.37/11.57 Clause #190 (by clausification #[189]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 11.37/11.57 Eq % 11.37/11.57 (admin_compartment_has_sso admin a a_1 → % 11.37/11.57 admin_compartment_has_scg admin a a_2 → % 11.37/11.57 sso_file_has_level a_1 a_3 a_4 a_2 → % 11.37/11.57 admin_file_has_level_h admin a_3 a_4 a_5 → admin_file_has_level_h admin a_3 a_4 (cons a a_5)) % 11.37/11.57 True % 11.37/11.57 Clause #191 (by clausification #[190]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 11.37/11.57 Or (Eq (admin_compartment_has_sso admin a a_1) False) % 11.37/11.57 (Eq % 11.37/11.57 (admin_compartment_has_scg admin a a_2 → % 11.37/11.57 sso_file_has_level a_1 a_3 a_4 a_2 → % 11.37/11.57 admin_file_has_level_h admin a_3 a_4 a_5 → admin_file_has_level_h admin a_3 a_4 (cons a a_5)) % 11.37/11.57 True) % 11.37/11.57 Clause #192 (by clausification #[191]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 11.37/11.57 Or (Eq (admin_compartment_has_sso admin a a_1) False) % 11.37/11.57 (Or (Eq (admin_compartment_has_scg admin a a_2) False) % 11.37/11.57 (Eq % 11.37/11.57 (sso_file_has_level a_1 a_3 a_4 a_2 → % 11.37/11.57 admin_file_has_level_h admin a_3 a_4 a_5 → admin_file_has_level_h admin a_3 a_4 (cons a a_5)) % 11.37/11.57 True)) % 11.37/11.57 Clause #193 (by clausification #[192]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 11.37/11.57 Or (Eq (admin_compartment_has_sso admin a a_1) False) % 11.37/11.57 (Or (Eq (admin_compartment_has_scg admin a a_2) False) % 11.37/11.57 (Or (Eq (sso_file_has_level a_1 a_3 a_4 a_2) False) % 11.37/11.57 (Eq (admin_file_has_level_h admin a_3 a_4 a_5 → admin_file_has_level_h admin a_3 a_4 (cons a a_5)) True))) % 11.37/11.57 Clause #194 (by clausification #[193]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 11.37/11.57 Or (Eq (admin_compartment_has_sso admin a a_1) False) % 11.37/11.57 (Or (Eq (admin_compartment_has_scg admin a a_2) False) % 11.37/11.57 (Or (Eq (sso_file_has_level a_1 a_3 a_4 a_2) False) % 11.37/11.57 (Or (Eq (admin_file_has_level_h admin a_3 a_4 a_5) False) % 11.37/11.57 (Eq (admin_file_has_level_h admin a_3 a_4 (cons a a_5)) True)))) % 11.37/11.57 Clause #195 (by superposition #[194, 128]): ∀ (a a_1 a_2 a_3 : Iota), % 11.37/11.57 Or (Eq (admin_compartment_has_scg admin compartmenta a) False) % 11.37/11.58 (Or (Eq (sso_file_has_level sso_compartmenta a_1 a_2 a) False) % 11.37/11.58 (Or (Eq (admin_file_has_level_h admin a_1 a_2 a_3) False) % 11.37/11.58 (Or (Eq (admin_file_has_level_h admin a_1 a_2 (cons compartmenta a_3)) True) (Eq False True)))) % 11.37/11.58 Clause #196 (by superposition #[194, 129]): ∀ (a a_1 a_2 a_3 : Iota), % 11.37/11.58 Or (Eq (admin_compartment_has_scg admin compartmentb a) False) % 11.37/11.58 (Or (Eq (sso_file_has_level sso_compartmentb a_1 a_2 a) False) % 11.37/11.58 (Or (Eq (admin_file_has_level_h admin a_1 a_2 a_3) False) % 11.37/11.58 (Or (Eq (admin_file_has_level_h admin a_1 a_2 (cons compartmentb a_3)) True) (Eq False True)))) % 11.37/11.58 Clause #197 (by clausification #[168]): ∀ (a : Iota), Or (Eq (hr_admin_indi_has_employment hr_admin a) False) (Eq (admin_indi_has_employment admin a) True) % 11.37/11.58 Clause #198 (by superposition #[197, 75]): Or (Eq (admin_indi_has_employment admin alice) True) (Eq False True) % 11.37/11.58 Clause #199 (by clausification #[198]): Eq (admin_indi_has_employment admin alice) True % 11.37/11.58 Clause #200 (by clausification #[35]): ∀ (a : Iota), % 11.37/11.58 Eq % 11.37/11.58 (∀ (F L : Iota), % 11.37/11.58 admin_file_has_level admin F L → admin_indi_has_level admin a L → admin_indi_has_level_for_file admin a F) % 11.37/11.58 True % 11.37/11.58 Clause #201 (by clausification #[200]): ∀ (a a_1 : Iota), % 11.37/11.58 Eq % 11.37/11.58 (∀ (L : Iota), % 11.37/11.58 admin_file_has_level admin a L → admin_indi_has_level admin a_1 L → admin_indi_has_level_for_file admin a_1 a) % 11.37/11.58 True % 11.37/11.58 Clause #202 (by clausification #[201]): ∀ (a a_1 a_2 : Iota), % 11.37/11.58 Eq (admin_file_has_level admin a a_1 → admin_indi_has_level admin a_2 a_1 → admin_indi_has_level_for_file admin a_2 a) % 11.37/11.58 True % 11.37/11.58 Clause #203 (by clausification #[202]): ∀ (a a_1 a_2 : Iota), % 11.37/11.58 Or (Eq (admin_file_has_level admin a a_1) False) % 11.37/11.58 (Eq (admin_indi_has_level admin a_2 a_1 → admin_indi_has_level_for_file admin a_2 a) True) % 11.37/11.58 Clause #204 (by clausification #[203]): ∀ (a a_1 a_2 : Iota), % 11.37/11.58 Or (Eq (admin_file_has_level admin a a_1) False) % 11.37/11.58 (Or (Eq (admin_indi_has_level admin a_2 a_1) False) (Eq (admin_indi_has_level_for_file admin a_2 a) True)) % 11.37/11.58 Clause #205 (by clausification #[34]): ∀ (a : Iota), % 11.37/11.58 Eq % 11.37/11.58 (∀ (F CL : Iota), % 11.37/11.58 admin_file_has_compartments admin F CL → % 11.37/11.58 admin_indi_has_compartments admin a CL → admin_indi_has_compartments_for_file admin a F) % 11.37/11.58 True % 11.37/11.58 Clause #206 (by clausification #[205]): ∀ (a a_1 : Iota), % 11.37/11.58 Eq % 11.37/11.58 (∀ (CL : Iota), % 11.37/11.58 admin_file_has_compartments admin a CL → % 11.37/11.58 admin_indi_has_compartments admin a_1 CL → admin_indi_has_compartments_for_file admin a_1 a) % 11.37/11.58 True % 11.37/11.58 Clause #207 (by clausification #[206]): ∀ (a a_1 a_2 : Iota), % 11.37/11.58 Eq % 11.37/11.58 (admin_file_has_compartments admin a a_1 → % 11.37/11.58 admin_indi_has_compartments admin a_2 a_1 → admin_indi_has_compartments_for_file admin a_2 a) % 11.37/11.58 True % 11.37/11.58 Clause #208 (by clausification #[207]): ∀ (a a_1 a_2 : Iota), % 11.37/11.58 Or (Eq (admin_file_has_compartments admin a a_1) False) % 11.37/11.58 (Eq (admin_indi_has_compartments admin a_2 a_1 → admin_indi_has_compartments_for_file admin a_2 a) True) % 11.37/11.58 Clause #209 (by clausification #[208]): ∀ (a a_1 a_2 : Iota), % 11.37/11.58 Or (Eq (admin_file_has_compartments admin a a_1) False) % 11.37/11.58 (Or (Eq (admin_indi_has_compartments admin a_2 a_1) False) % 11.37/11.58 (Eq (admin_indi_has_compartments_for_file admin a_2 a) True)) % 11.37/11.58 Clause #210 (by clausification #[139]): ∀ (a : Iota), % 11.37/11.58 Or (Eq (polygraph_admin_indi_has_polygraph polygraph_admin a) False) (Eq (admin_indi_has_polygraph admin a) True) % 11.37/11.58 Clause #211 (by superposition #[210, 72]): Or (Eq (admin_indi_has_polygraph admin alice) True) (Eq False True) % 11.37/11.58 Clause #220 (by clausification #[211]): Eq (admin_indi_has_polygraph admin alice) True % 11.37/11.58 Clause #226 (by clausification #[36]): ∀ (a : Iota), % 11.37/11.58 Eq % 11.37/11.58 (∀ (F OWR : Iota), % 11.37/11.58 state_file_has_owner F OWR → owner_indi_has_need_to_know OWR a F → admin_indi_has_need_to_know_for_file admin a F) % 11.37/11.58 True % 11.37/11.58 Clause #227 (by clausification #[226]): ∀ (a a_1 : Iota), % 11.37/11.58 Eq % 11.37/11.58 (∀ (OWR : Iota), % 11.37/11.58 state_file_has_owner a OWR → % 11.37/11.58 owner_indi_has_need_to_know OWR a_1 a → admin_indi_has_need_to_know_for_file admin a_1 a) % 11.37/11.58 True % 11.37/11.58 Clause #228 (by clausification #[227]): ∀ (a a_1 a_2 : Iota), % 11.44/11.60 Eq % 11.44/11.60 (state_file_has_owner a a_1 → % 11.44/11.60 owner_indi_has_need_to_know a_1 a_2 a → admin_indi_has_need_to_know_for_file admin a_2 a) % 11.44/11.60 True % 11.44/11.60 Clause #229 (by clausification #[228]): ∀ (a a_1 a_2 : Iota), % 11.44/11.60 Or (Eq (state_file_has_owner a a_1) False) % 11.44/11.60 (Eq (owner_indi_has_need_to_know a_1 a_2 a → admin_indi_has_need_to_know_for_file admin a_2 a) True) % 11.44/11.60 Clause #230 (by clausification #[229]): ∀ (a a_1 a_2 : Iota), % 11.44/11.60 Or (Eq (state_file_has_owner a a_1) False) % 11.44/11.60 (Or (Eq (owner_indi_has_need_to_know a_1 a_2 a) False) (Eq (admin_indi_has_need_to_know_for_file admin a_2 a) True)) % 11.44/11.60 Clause #231 (by superposition #[230, 60]): ∀ (a : Iota), % 11.44/11.60 Or (Eq (owner_indi_has_need_to_know owner_secretfile a secretfile) False) % 11.44/11.60 (Or (Eq (admin_indi_has_need_to_know_for_file admin a secretfile) True) (Eq False True)) % 11.44/11.60 Clause #255 (by clausification #[103]): ∀ (a a_1 : Iota), Or (Eq (loca_level_below a a_1 secret) False) (Eq (loca_level_below a a_1 topsecret) True) % 11.44/11.60 Clause #256 (by superposition #[255, 93]): ∀ (a : Iota), Or (Eq (loca_level_below a secret topsecret) True) (Eq False True) % 11.44/11.60 Clause #257 (by clausification #[256]): ∀ (a : Iota), Eq (loca_level_below a secret topsecret) True % 11.44/11.60 Clause #258 (by clausification #[102]): ∀ (a a_1 : Iota), Or (Eq (loca_level_below a a_1 confidential) False) (Eq (loca_level_below a a_1 secret) True) % 11.44/11.60 Clause #259 (by superposition #[258, 93]): ∀ (a : Iota), Or (Eq (loca_level_below a confidential secret) True) (Eq False True) % 11.44/11.60 Clause #260 (by clausification #[259]): ∀ (a : Iota), Eq (loca_level_below a confidential secret) True % 11.44/11.60 Clause #261 (by superposition #[260, 255]): ∀ (a : Iota), Or (Eq True False) (Eq (loca_level_below a confidential topsecret) True) % 11.44/11.60 Clause #262 (by clausification #[20]): ∀ (a : Iota), % 11.44/11.60 Eq % 11.44/11.60 (∀ (L BA L1 : Iota), % 11.44/11.60 system_indi_is_background_admin system BA → % 11.44/11.60 background_admin_indi_has_background BA a L1 → % 11.44/11.60 loca_level_below admin L L1 → admin_indi_has_background admin a L) % 11.44/11.60 True % 11.44/11.60 Clause #263 (by clausification #[262]): ∀ (a a_1 : Iota), % 11.44/11.60 Eq % 11.44/11.60 (∀ (BA L1 : Iota), % 11.44/11.60 system_indi_is_background_admin system BA → % 11.44/11.60 background_admin_indi_has_background BA a L1 → % 11.44/11.60 loca_level_below admin a_1 L1 → admin_indi_has_background admin a a_1) % 11.44/11.60 True % 11.44/11.60 Clause #264 (by clausification #[263]): ∀ (a a_1 a_2 : Iota), % 11.44/11.60 Eq % 11.44/11.60 (∀ (L1 : Iota), % 11.44/11.60 system_indi_is_background_admin system a → % 11.44/11.60 background_admin_indi_has_background a a_1 L1 → % 11.44/11.60 loca_level_below admin a_2 L1 → admin_indi_has_background admin a_1 a_2) % 11.44/11.60 True % 11.44/11.60 Clause #265 (by clausification #[264]): ∀ (a a_1 a_2 a_3 : Iota), % 11.44/11.60 Eq % 11.44/11.60 (system_indi_is_background_admin system a → % 11.44/11.60 background_admin_indi_has_background a a_1 a_2 → % 11.44/11.60 loca_level_below admin a_3 a_2 → admin_indi_has_background admin a_1 a_3) % 11.44/11.60 True % 11.44/11.60 Clause #266 (by clausification #[265]): ∀ (a a_1 a_2 a_3 : Iota), % 11.44/11.60 Or (Eq (system_indi_is_background_admin system a) False) % 11.44/11.60 (Eq % 11.44/11.60 (background_admin_indi_has_background a a_1 a_2 → % 11.44/11.60 loca_level_below admin a_3 a_2 → admin_indi_has_background admin a_1 a_3) % 11.44/11.60 True) % 11.44/11.60 Clause #267 (by clausification #[266]): ∀ (a a_1 a_2 a_3 : Iota), % 11.44/11.60 Or (Eq (system_indi_is_background_admin system a) False) % 11.44/11.60 (Or (Eq (background_admin_indi_has_background a a_1 a_2) False) % 11.44/11.60 (Eq (loca_level_below admin a_3 a_2 → admin_indi_has_background admin a_1 a_3) True)) % 11.44/11.60 Clause #268 (by clausification #[267]): ∀ (a a_1 a_2 a_3 : Iota), % 11.44/11.60 Or (Eq (system_indi_is_background_admin system a) False) % 11.44/11.60 (Or (Eq (background_admin_indi_has_background a a_1 a_2) False) % 11.44/11.60 (Or (Eq (loca_level_below admin a_3 a_2) False) (Eq (admin_indi_has_background admin a_1 a_3) True))) % 11.44/11.60 Clause #269 (by superposition #[268, 68]): ∀ (a a_1 a_2 : Iota), % 11.44/11.60 Or (Eq (background_admin_indi_has_background background_admin a a_1) False) % 11.44/11.60 (Or (Eq (loca_level_below admin a_2 a_1) False) % 11.44/11.60 (Or (Eq (admin_indi_has_background admin a a_2) True) (Eq False True))) % 11.44/11.60 Clause #270 (by clausification #[261]): ∀ (a : Iota), Eq (loca_level_below a confidential topsecret) True % 11.44/11.61 Clause #271 (by clausification #[101]): ∀ (a a_1 : Iota), Or (Eq (loca_level_below a a_1 sbu) False) (Eq (loca_level_below a a_1 confidential) True) % 11.44/11.61 Clause #273 (by superposition #[271, 93]): ∀ (a : Iota), Or (Eq (loca_level_below a sbu confidential) True) (Eq False True) % 11.44/11.61 Clause #274 (by clausification #[273]): ∀ (a : Iota), Eq (loca_level_below a sbu confidential) True % 11.44/11.61 Clause #275 (by superposition #[274, 258]): ∀ (a : Iota), Or (Eq True False) (Eq (loca_level_below a sbu secret) True) % 11.44/11.61 Clause #276 (by clausification #[275]): ∀ (a : Iota), Eq (loca_level_below a sbu secret) True % 11.44/11.61 Clause #277 (by superposition #[276, 255]): ∀ (a : Iota), Or (Eq True False) (Eq (loca_level_below a sbu topsecret) True) % 11.44/11.61 Clause #278 (by clausification #[277]): ∀ (a : Iota), Eq (loca_level_below a sbu topsecret) True % 11.44/11.61 Clause #279 (by clausification #[25]): ∀ (a : Iota), % 11.44/11.61 Eq % 11.44/11.61 (∀ (L L1 LA L11 : Iota), % 11.44/11.61 system_indi_needs_level system a L1 → % 11.44/11.61 admin_indi_has_citizenship admin a usa → % 11.44/11.61 admin_indi_has_polygraph admin a → % 11.44/11.61 admin_indi_has_employment admin a → % 11.44/11.61 admin_indi_has_credit admin a → % 11.44/11.61 loca_level_below admin L L1 → % 11.44/11.61 system_indi_is_level_admin system LA → % 11.44/11.61 level_admin_indi_has_level LA a L11 → % 11.44/11.61 loca_level_below admin L L11 → % 11.44/11.61 admin_indi_has_background admin a L → admin_indi_has_level admin a L) % 11.44/11.61 True % 11.44/11.61 Clause #280 (by clausification #[279]): ∀ (a a_1 : Iota), % 11.44/11.61 Eq % 11.44/11.61 (∀ (L1 LA L11 : Iota), % 11.44/11.61 system_indi_needs_level system a L1 → % 11.44/11.61 admin_indi_has_citizenship admin a usa → % 11.44/11.61 admin_indi_has_polygraph admin a → % 11.44/11.61 admin_indi_has_employment admin a → % 11.44/11.61 admin_indi_has_credit admin a → % 11.44/11.61 loca_level_below admin a_1 L1 → % 11.44/11.61 system_indi_is_level_admin system LA → % 11.44/11.61 level_admin_indi_has_level LA a L11 → % 11.44/11.61 loca_level_below admin a_1 L11 → % 11.44/11.61 admin_indi_has_background admin a a_1 → admin_indi_has_level admin a a_1) % 11.44/11.61 True % 11.44/11.61 Clause #281 (by clausification #[280]): ∀ (a a_1 a_2 : Iota), % 11.44/11.61 Eq % 11.44/11.61 (∀ (LA L11 : Iota), % 11.44/11.61 system_indi_needs_level system a a_1 → % 11.44/11.61 admin_indi_has_citizenship admin a usa → % 11.44/11.61 admin_indi_has_polygraph admin a → % 11.44/11.61 admin_indi_has_employment admin a → % 11.44/11.61 admin_indi_has_credit admin a → % 11.44/11.61 loca_level_below admin a_2 a_1 → % 11.44/11.61 system_indi_is_level_admin system LA → % 11.44/11.61 level_admin_indi_has_level LA a L11 → % 11.44/11.61 loca_level_below admin a_2 L11 → % 11.44/11.61 admin_indi_has_background admin a a_2 → admin_indi_has_level admin a a_2) % 11.44/11.61 True % 11.44/11.61 Clause #282 (by clausification #[281]): ∀ (a a_1 a_2 a_3 : Iota), % 11.44/11.61 Eq % 11.44/11.61 (∀ (L11 : Iota), % 11.44/11.61 system_indi_needs_level system a a_1 → % 11.44/11.61 admin_indi_has_citizenship admin a usa → % 11.44/11.61 admin_indi_has_polygraph admin a → % 11.44/11.61 admin_indi_has_employment admin a → % 11.44/11.61 admin_indi_has_credit admin a → % 11.44/11.61 loca_level_below admin a_2 a_1 → % 11.44/11.61 system_indi_is_level_admin system a_3 → % 11.44/11.61 level_admin_indi_has_level a_3 a L11 → % 11.44/11.61 loca_level_below admin a_2 L11 → % 11.44/11.61 admin_indi_has_background admin a a_2 → admin_indi_has_level admin a a_2) % 11.44/11.61 True % 11.44/11.61 Clause #283 (by clausification #[282]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 11.44/11.61 Eq % 11.44/11.61 (system_indi_needs_level system a a_1 → % 11.44/11.61 admin_indi_has_citizenship admin a usa → % 11.44/11.61 admin_indi_has_polygraph admin a → % 11.44/11.61 admin_indi_has_employment admin a → % 11.44/11.61 admin_indi_has_credit admin a → % 11.44/11.61 loca_level_below admin a_2 a_1 → % 11.44/11.61 system_indi_is_level_admin system a_3 → % 11.44/11.61 level_admin_indi_has_level a_3 a a_4 → % 11.44/11.61 loca_level_below admin a_2 a_4 → % 11.44/11.62 admin_indi_has_background admin a a_2 → admin_indi_has_level admin a a_2) % 11.44/11.62 True % 11.44/11.62 Clause #284 (by clausification #[283]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 11.44/11.62 Or (Eq (system_indi_needs_level system a a_1) False) % 11.44/11.62 (Eq % 11.44/11.62 (admin_indi_has_citizenship admin a usa → % 11.44/11.62 admin_indi_has_polygraph admin a → % 11.44/11.62 admin_indi_has_employment admin a → % 11.44/11.62 admin_indi_has_credit admin a → % 11.44/11.62 loca_level_below admin a_2 a_1 → % 11.44/11.62 system_indi_is_level_admin system a_3 → % 11.44/11.62 level_admin_indi_has_level a_3 a a_4 → % 11.44/11.62 loca_level_below admin a_2 a_4 → % 11.44/11.62 admin_indi_has_background admin a a_2 → admin_indi_has_level admin a a_2) % 11.44/11.62 True) % 11.44/11.62 Clause #285 (by clausification #[284]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 11.44/11.62 Or (Eq (system_indi_needs_level system a a_1) False) % 11.44/11.62 (Or (Eq (admin_indi_has_citizenship admin a usa) False) % 11.44/11.62 (Eq % 11.44/11.62 (admin_indi_has_polygraph admin a → % 11.44/11.62 admin_indi_has_employment admin a → % 11.44/11.62 admin_indi_has_credit admin a → % 11.44/11.62 loca_level_below admin a_2 a_1 → % 11.44/11.62 system_indi_is_level_admin system a_3 → % 11.44/11.62 level_admin_indi_has_level a_3 a a_4 → % 11.44/11.62 loca_level_below admin a_2 a_4 → % 11.44/11.62 admin_indi_has_background admin a a_2 → admin_indi_has_level admin a a_2) % 11.44/11.62 True)) % 11.44/11.62 Clause #286 (by clausification #[285]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 11.44/11.62 Or (Eq (system_indi_needs_level system a a_1) False) % 11.44/11.62 (Or (Eq (admin_indi_has_citizenship admin a usa) False) % 11.44/11.62 (Or (Eq (admin_indi_has_polygraph admin a) False) % 11.44/11.62 (Eq % 11.44/11.62 (admin_indi_has_employment admin a → % 11.44/11.62 admin_indi_has_credit admin a → % 11.44/11.62 loca_level_below admin a_2 a_1 → % 11.44/11.62 system_indi_is_level_admin system a_3 → % 11.44/11.62 level_admin_indi_has_level a_3 a a_4 → % 11.44/11.62 loca_level_below admin a_2 a_4 → % 11.44/11.62 admin_indi_has_background admin a a_2 → admin_indi_has_level admin a a_2) % 11.44/11.62 True))) % 11.44/11.62 Clause #287 (by clausification #[286]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 11.44/11.62 Or (Eq (system_indi_needs_level system a a_1) False) % 11.44/11.62 (Or (Eq (admin_indi_has_citizenship admin a usa) False) % 11.44/11.62 (Or (Eq (admin_indi_has_polygraph admin a) False) % 11.44/11.62 (Or (Eq (admin_indi_has_employment admin a) False) % 11.44/11.62 (Eq % 11.44/11.62 (admin_indi_has_credit admin a → % 11.44/11.62 loca_level_below admin a_2 a_1 → % 11.44/11.62 system_indi_is_level_admin system a_3 → % 11.44/11.62 level_admin_indi_has_level a_3 a a_4 → % 11.44/11.62 loca_level_below admin a_2 a_4 → % 11.44/11.62 admin_indi_has_background admin a a_2 → admin_indi_has_level admin a a_2) % 11.44/11.62 True)))) % 11.44/11.62 Clause #288 (by clausification #[287]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 11.44/11.62 Or (Eq (system_indi_needs_level system a a_1) False) % 11.44/11.62 (Or (Eq (admin_indi_has_citizenship admin a usa) False) % 11.44/11.62 (Or (Eq (admin_indi_has_polygraph admin a) False) % 11.44/11.62 (Or (Eq (admin_indi_has_employment admin a) False) % 11.44/11.62 (Or (Eq (admin_indi_has_credit admin a) False) % 11.44/11.62 (Eq % 11.44/11.62 (loca_level_below admin a_2 a_1 → % 11.44/11.62 system_indi_is_level_admin system a_3 → % 11.44/11.62 level_admin_indi_has_level a_3 a a_4 → % 11.44/11.62 loca_level_below admin a_2 a_4 → % 11.44/11.62 admin_indi_has_background admin a a_2 → admin_indi_has_level admin a a_2) % 11.44/11.62 True))))) % 11.44/11.62 Clause #289 (by clausification #[288]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 11.44/11.62 Or (Eq (system_indi_needs_level system a a_1) False) % 11.44/11.62 (Or (Eq (admin_indi_has_citizenship admin a usa) False) % 11.44/11.62 (Or (Eq (admin_indi_has_polygraph admin a) False) % 11.44/11.62 (Or (Eq (admin_indi_has_employment admin a) False) % 11.44/11.62 (Or (Eq (admin_indi_has_credit admin a) False) % 11.44/11.62 (Or (Eq (loca_level_below admin a_2 a_1) False) % 11.44/11.62 (Eq % 11.44/11.62 (system_indi_is_level_admin system a_3 → % 11.44/11.62 level_admin_indi_has_level a_3 a a_4 → % 11.44/11.64 loca_level_below admin a_2 a_4 → % 11.44/11.64 admin_indi_has_background admin a a_2 → admin_indi_has_level admin a a_2) % 11.44/11.64 True)))))) % 11.44/11.64 Clause #290 (by clausification #[289]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 11.44/11.64 Or (Eq (system_indi_needs_level system a a_1) False) % 11.44/11.64 (Or (Eq (admin_indi_has_citizenship admin a usa) False) % 11.44/11.64 (Or (Eq (admin_indi_has_polygraph admin a) False) % 11.44/11.64 (Or (Eq (admin_indi_has_employment admin a) False) % 11.44/11.64 (Or (Eq (admin_indi_has_credit admin a) False) % 11.44/11.64 (Or (Eq (loca_level_below admin a_2 a_1) False) % 11.44/11.64 (Or (Eq (system_indi_is_level_admin system a_3) False) % 11.44/11.64 (Eq % 11.44/11.64 (level_admin_indi_has_level a_3 a a_4 → % 11.44/11.64 loca_level_below admin a_2 a_4 → % 11.44/11.64 admin_indi_has_background admin a a_2 → admin_indi_has_level admin a a_2) % 11.44/11.64 True))))))) % 11.44/11.64 Clause #291 (by clausification #[290]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 11.44/11.64 Or (Eq (system_indi_needs_level system a a_1) False) % 11.44/11.64 (Or (Eq (admin_indi_has_citizenship admin a usa) False) % 11.44/11.64 (Or (Eq (admin_indi_has_polygraph admin a) False) % 11.44/11.64 (Or (Eq (admin_indi_has_employment admin a) False) % 11.44/11.64 (Or (Eq (admin_indi_has_credit admin a) False) % 11.44/11.64 (Or (Eq (loca_level_below admin a_2 a_1) False) % 11.44/11.64 (Or (Eq (system_indi_is_level_admin system a_3) False) % 11.44/11.64 (Or (Eq (level_admin_indi_has_level a_3 a a_4) False) % 11.44/11.64 (Eq % 11.44/11.64 (loca_level_below admin a_2 a_4 → % 11.44/11.64 admin_indi_has_background admin a a_2 → admin_indi_has_level admin a a_2) % 11.44/11.64 True)))))))) % 11.44/11.64 Clause #292 (by clausification #[291]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 11.44/11.64 Or (Eq (system_indi_needs_level system a a_1) False) % 11.44/11.64 (Or (Eq (admin_indi_has_citizenship admin a usa) False) % 11.44/11.64 (Or (Eq (admin_indi_has_polygraph admin a) False) % 11.44/11.64 (Or (Eq (admin_indi_has_employment admin a) False) % 11.44/11.64 (Or (Eq (admin_indi_has_credit admin a) False) % 11.44/11.64 (Or (Eq (loca_level_below admin a_2 a_1) False) % 11.44/11.64 (Or (Eq (system_indi_is_level_admin system a_3) False) % 11.44/11.64 (Or (Eq (level_admin_indi_has_level a_3 a a_4) False) % 11.44/11.64 (Or (Eq (loca_level_below admin a_2 a_4) False) % 11.44/11.64 (Eq (admin_indi_has_background admin a a_2 → admin_indi_has_level admin a a_2) True))))))))) % 11.44/11.64 Clause #293 (by clausification #[292]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 11.44/11.64 Or (Eq (system_indi_needs_level system a a_1) False) % 11.44/11.64 (Or (Eq (admin_indi_has_citizenship admin a usa) False) % 11.44/11.64 (Or (Eq (admin_indi_has_polygraph admin a) False) % 11.44/11.64 (Or (Eq (admin_indi_has_employment admin a) False) % 11.44/11.64 (Or (Eq (admin_indi_has_credit admin a) False) % 11.44/11.64 (Or (Eq (loca_level_below admin a_2 a_1) False) % 11.44/11.64 (Or (Eq (system_indi_is_level_admin system a_3) False) % 11.44/11.64 (Or (Eq (level_admin_indi_has_level a_3 a a_4) False) % 11.44/11.64 (Or (Eq (loca_level_below admin a_2 a_4) False) % 11.44/11.64 (Or (Eq (admin_indi_has_background admin a a_2) False) % 11.44/11.64 (Eq (admin_indi_has_level admin a a_2) True)))))))))) % 11.44/11.64 Clause #294 (by superposition #[293, 76]): ∀ (a a_1 a_2 : Iota), % 11.44/11.64 Or (Eq (admin_indi_has_citizenship admin alice usa) False) % 11.44/11.64 (Or (Eq (admin_indi_has_polygraph admin alice) False) % 11.44/11.64 (Or (Eq (admin_indi_has_employment admin alice) False) % 11.44/11.64 (Or (Eq (admin_indi_has_credit admin alice) False) % 11.44/11.64 (Or (Eq (loca_level_below admin a secret) False) % 11.44/11.64 (Or (Eq (system_indi_is_level_admin system a_1) False) % 11.44/11.64 (Or (Eq (level_admin_indi_has_level a_1 alice a_2) False) % 11.44/11.64 (Or (Eq (loca_level_below admin a a_2) False) % 11.44/11.64 (Or (Eq (admin_indi_has_background admin alice a) False) % 11.44/11.64 (Or (Eq (admin_indi_has_level admin alice a) True) (Eq False True)))))))))) % 11.44/11.64 Clause #303 (by clausification #[27]): ∀ (a : Iota), % 11.44/11.64 Eq % 11.44/11.64 (∀ (C CL SSO : Iota), % 11.44/11.64 system_indi_needs_compartment system a C → % 11.44/11.65 admin_indi_has_employment admin a → % 11.44/11.65 admin_indi_has_citizenship admin a usa → % 11.44/11.65 admin_indi_has_polygraph_for_compartment admin a C → % 11.44/11.65 admin_indi_has_credit_for_compartment admin a C → % 11.44/11.65 admin_compartment_has_sso admin C SSO → % 11.44/11.65 sso_indi_has_compartment SSO a C → % 11.44/11.65 admin_indi_has_background_for_compartment admin a C → % 11.44/11.65 admin_indi_has_level_for_compartment admin a C → % 11.44/11.65 admin_indi_has_compartments admin a CL → admin_indi_has_compartments admin a (cons C CL)) % 11.44/11.65 True % 11.44/11.65 Clause #304 (by clausification #[303]): ∀ (a a_1 : Iota), % 11.44/11.65 Eq % 11.44/11.65 (∀ (CL SSO : Iota), % 11.44/11.65 system_indi_needs_compartment system a a_1 → % 11.44/11.65 admin_indi_has_employment admin a → % 11.44/11.65 admin_indi_has_citizenship admin a usa → % 11.44/11.65 admin_indi_has_polygraph_for_compartment admin a a_1 → % 11.44/11.65 admin_indi_has_credit_for_compartment admin a a_1 → % 11.44/11.65 admin_compartment_has_sso admin a_1 SSO → % 11.44/11.65 sso_indi_has_compartment SSO a a_1 → % 11.44/11.65 admin_indi_has_background_for_compartment admin a a_1 → % 11.44/11.65 admin_indi_has_level_for_compartment admin a a_1 → % 11.44/11.65 admin_indi_has_compartments admin a CL → admin_indi_has_compartments admin a (cons a_1 CL)) % 11.44/11.65 True % 11.44/11.65 Clause #305 (by clausification #[304]): ∀ (a a_1 a_2 : Iota), % 11.44/11.65 Eq % 11.44/11.65 (∀ (SSO : Iota), % 11.44/11.65 system_indi_needs_compartment system a a_1 → % 11.44/11.65 admin_indi_has_employment admin a → % 11.44/11.65 admin_indi_has_citizenship admin a usa → % 11.44/11.65 admin_indi_has_polygraph_for_compartment admin a a_1 → % 11.44/11.65 admin_indi_has_credit_for_compartment admin a a_1 → % 11.44/11.65 admin_compartment_has_sso admin a_1 SSO → % 11.44/11.65 sso_indi_has_compartment SSO a a_1 → % 11.44/11.65 admin_indi_has_background_for_compartment admin a a_1 → % 11.44/11.65 admin_indi_has_level_for_compartment admin a a_1 → % 11.44/11.65 admin_indi_has_compartments admin a a_2 → admin_indi_has_compartments admin a (cons a_1 a_2)) % 11.44/11.65 True % 11.44/11.65 Clause #306 (by clausification #[305]): ∀ (a a_1 a_2 a_3 : Iota), % 11.44/11.65 Eq % 11.44/11.65 (system_indi_needs_compartment system a a_1 → % 11.44/11.65 admin_indi_has_employment admin a → % 11.44/11.65 admin_indi_has_citizenship admin a usa → % 11.44/11.65 admin_indi_has_polygraph_for_compartment admin a a_1 → % 11.44/11.65 admin_indi_has_credit_for_compartment admin a a_1 → % 11.44/11.65 admin_compartment_has_sso admin a_1 a_2 → % 11.44/11.65 sso_indi_has_compartment a_2 a a_1 → % 11.44/11.65 admin_indi_has_background_for_compartment admin a a_1 → % 11.44/11.65 admin_indi_has_level_for_compartment admin a a_1 → % 11.44/11.65 admin_indi_has_compartments admin a a_3 → admin_indi_has_compartments admin a (cons a_1 a_3)) % 11.44/11.65 True % 11.44/11.65 Clause #307 (by clausification #[306]): ∀ (a a_1 a_2 a_3 : Iota), % 11.44/11.65 Or (Eq (system_indi_needs_compartment system a a_1) False) % 11.44/11.65 (Eq % 11.44/11.65 (admin_indi_has_employment admin a → % 11.44/11.65 admin_indi_has_citizenship admin a usa → % 11.44/11.65 admin_indi_has_polygraph_for_compartment admin a a_1 → % 11.44/11.65 admin_indi_has_credit_for_compartment admin a a_1 → % 11.44/11.65 admin_compartment_has_sso admin a_1 a_2 → % 11.44/11.65 sso_indi_has_compartment a_2 a a_1 → % 11.44/11.65 admin_indi_has_background_for_compartment admin a a_1 → % 11.44/11.65 admin_indi_has_level_for_compartment admin a a_1 → % 11.44/11.65 admin_indi_has_compartments admin a a_3 → admin_indi_has_compartments admin a (cons a_1 a_3)) % 11.44/11.65 True) % 11.44/11.65 Clause #308 (by clausification #[307]): ∀ (a a_1 a_2 a_3 : Iota), % 11.44/11.65 Or (Eq (system_indi_needs_compartment system a a_1) False) % 11.44/11.65 (Or (Eq (admin_indi_has_employment admin a) False) % 11.44/11.65 (Eq % 11.44/11.65 (admin_indi_has_citizenship admin a usa → % 11.44/11.65 admin_indi_has_polygraph_for_compartment admin a a_1 → % 11.44/11.65 admin_indi_has_credit_for_compartment admin a a_1 → % 11.44/11.65 admin_compartment_has_sso admin a_1 a_2 → % 11.50/11.66 sso_indi_has_compartment a_2 a a_1 → % 11.50/11.66 admin_indi_has_background_for_compartment admin a a_1 → % 11.50/11.66 admin_indi_has_level_for_compartment admin a a_1 → % 11.50/11.66 admin_indi_has_compartments admin a a_3 → admin_indi_has_compartments admin a (cons a_1 a_3)) % 11.50/11.66 True)) % 11.50/11.66 Clause #309 (by clausification #[308]): ∀ (a a_1 a_2 a_3 : Iota), % 11.50/11.66 Or (Eq (system_indi_needs_compartment system a a_1) False) % 11.50/11.66 (Or (Eq (admin_indi_has_employment admin a) False) % 11.50/11.66 (Or (Eq (admin_indi_has_citizenship admin a usa) False) % 11.50/11.66 (Eq % 11.50/11.66 (admin_indi_has_polygraph_for_compartment admin a a_1 → % 11.50/11.66 admin_indi_has_credit_for_compartment admin a a_1 → % 11.50/11.66 admin_compartment_has_sso admin a_1 a_2 → % 11.50/11.66 sso_indi_has_compartment a_2 a a_1 → % 11.50/11.66 admin_indi_has_background_for_compartment admin a a_1 → % 11.50/11.66 admin_indi_has_level_for_compartment admin a a_1 → % 11.50/11.66 admin_indi_has_compartments admin a a_3 → admin_indi_has_compartments admin a (cons a_1 a_3)) % 11.50/11.66 True))) % 11.50/11.66 Clause #310 (by clausification #[309]): ∀ (a a_1 a_2 a_3 : Iota), % 11.50/11.66 Or (Eq (system_indi_needs_compartment system a a_1) False) % 11.50/11.66 (Or (Eq (admin_indi_has_employment admin a) False) % 11.50/11.66 (Or (Eq (admin_indi_has_citizenship admin a usa) False) % 11.50/11.66 (Or (Eq (admin_indi_has_polygraph_for_compartment admin a a_1) False) % 11.50/11.66 (Eq % 11.50/11.66 (admin_indi_has_credit_for_compartment admin a a_1 → % 11.50/11.66 admin_compartment_has_sso admin a_1 a_2 → % 11.50/11.66 sso_indi_has_compartment a_2 a a_1 → % 11.50/11.66 admin_indi_has_background_for_compartment admin a a_1 → % 11.50/11.66 admin_indi_has_level_for_compartment admin a a_1 → % 11.50/11.66 admin_indi_has_compartments admin a a_3 → admin_indi_has_compartments admin a (cons a_1 a_3)) % 11.50/11.66 True)))) % 11.50/11.66 Clause #311 (by clausification #[310]): ∀ (a a_1 a_2 a_3 : Iota), % 11.50/11.66 Or (Eq (system_indi_needs_compartment system a a_1) False) % 11.50/11.66 (Or (Eq (admin_indi_has_employment admin a) False) % 11.50/11.66 (Or (Eq (admin_indi_has_citizenship admin a usa) False) % 11.50/11.66 (Or (Eq (admin_indi_has_polygraph_for_compartment admin a a_1) False) % 11.50/11.66 (Or (Eq (admin_indi_has_credit_for_compartment admin a a_1) False) % 11.50/11.66 (Eq % 11.50/11.66 (admin_compartment_has_sso admin a_1 a_2 → % 11.50/11.66 sso_indi_has_compartment a_2 a a_1 → % 11.50/11.66 admin_indi_has_background_for_compartment admin a a_1 → % 11.50/11.66 admin_indi_has_level_for_compartment admin a a_1 → % 11.50/11.66 admin_indi_has_compartments admin a a_3 → admin_indi_has_compartments admin a (cons a_1 a_3)) % 11.50/11.66 True))))) % 11.50/11.66 Clause #312 (by clausification #[311]): ∀ (a a_1 a_2 a_3 : Iota), % 11.50/11.66 Or (Eq (system_indi_needs_compartment system a a_1) False) % 11.50/11.66 (Or (Eq (admin_indi_has_employment admin a) False) % 11.50/11.66 (Or (Eq (admin_indi_has_citizenship admin a usa) False) % 11.50/11.66 (Or (Eq (admin_indi_has_polygraph_for_compartment admin a a_1) False) % 11.50/11.66 (Or (Eq (admin_indi_has_credit_for_compartment admin a a_1) False) % 11.50/11.66 (Or (Eq (admin_compartment_has_sso admin a_1 a_2) False) % 11.50/11.66 (Eq % 11.50/11.66 (sso_indi_has_compartment a_2 a a_1 → % 11.50/11.66 admin_indi_has_background_for_compartment admin a a_1 → % 11.50/11.66 admin_indi_has_level_for_compartment admin a a_1 → % 11.50/11.66 admin_indi_has_compartments admin a a_3 → admin_indi_has_compartments admin a (cons a_1 a_3)) % 11.50/11.66 True)))))) % 11.50/11.66 Clause #313 (by clausification #[312]): ∀ (a a_1 a_2 a_3 : Iota), % 11.50/11.66 Or (Eq (system_indi_needs_compartment system a a_1) False) % 11.50/11.66 (Or (Eq (admin_indi_has_employment admin a) False) % 11.50/11.66 (Or (Eq (admin_indi_has_citizenship admin a usa) False) % 11.50/11.66 (Or (Eq (admin_indi_has_polygraph_for_compartment admin a a_1) False) % 11.50/11.66 (Or (Eq (admin_indi_has_credit_for_compartment admin a a_1) False) % 11.50/11.66 (Or (Eq (admin_compartment_has_sso admin a_1 a_2) False) % 11.50/11.66 (Or (Eq (sso_indi_has_compartment a_2 a a_1) False) % 11.50/11.68 (Eq % 11.50/11.68 (admin_indi_has_background_for_compartment admin a a_1 → % 11.50/11.68 admin_indi_has_level_for_compartment admin a a_1 → % 11.50/11.68 admin_indi_has_compartments admin a a_3 → admin_indi_has_compartments admin a (cons a_1 a_3)) % 11.50/11.68 True))))))) % 11.50/11.68 Clause #314 (by clausification #[313]): ∀ (a a_1 a_2 a_3 : Iota), % 11.50/11.68 Or (Eq (system_indi_needs_compartment system a a_1) False) % 11.50/11.68 (Or (Eq (admin_indi_has_employment admin a) False) % 11.50/11.68 (Or (Eq (admin_indi_has_citizenship admin a usa) False) % 11.50/11.68 (Or (Eq (admin_indi_has_polygraph_for_compartment admin a a_1) False) % 11.50/11.68 (Or (Eq (admin_indi_has_credit_for_compartment admin a a_1) False) % 11.50/11.68 (Or (Eq (admin_compartment_has_sso admin a_1 a_2) False) % 11.50/11.68 (Or (Eq (sso_indi_has_compartment a_2 a a_1) False) % 11.50/11.68 (Or (Eq (admin_indi_has_background_for_compartment admin a a_1) False) % 11.50/11.68 (Eq % 11.50/11.68 (admin_indi_has_level_for_compartment admin a a_1 → % 11.50/11.68 admin_indi_has_compartments admin a a_3 → admin_indi_has_compartments admin a (cons a_1 a_3)) % 11.50/11.68 True)))))))) % 11.50/11.68 Clause #315 (by clausification #[314]): ∀ (a a_1 a_2 a_3 : Iota), % 11.50/11.68 Or (Eq (system_indi_needs_compartment system a a_1) False) % 11.50/11.68 (Or (Eq (admin_indi_has_employment admin a) False) % 11.50/11.68 (Or (Eq (admin_indi_has_citizenship admin a usa) False) % 11.50/11.68 (Or (Eq (admin_indi_has_polygraph_for_compartment admin a a_1) False) % 11.50/11.68 (Or (Eq (admin_indi_has_credit_for_compartment admin a a_1) False) % 11.50/11.68 (Or (Eq (admin_compartment_has_sso admin a_1 a_2) False) % 11.50/11.68 (Or (Eq (sso_indi_has_compartment a_2 a a_1) False) % 11.50/11.68 (Or (Eq (admin_indi_has_background_for_compartment admin a a_1) False) % 11.50/11.68 (Or (Eq (admin_indi_has_level_for_compartment admin a a_1) False) % 11.50/11.68 (Eq (admin_indi_has_compartments admin a a_3 → admin_indi_has_compartments admin a (cons a_1 a_3)) % 11.50/11.68 True))))))))) % 11.50/11.68 Clause #316 (by clausification #[315]): ∀ (a a_1 a_2 a_3 : Iota), % 11.50/11.68 Or (Eq (system_indi_needs_compartment system a a_1) False) % 11.50/11.68 (Or (Eq (admin_indi_has_employment admin a) False) % 11.50/11.68 (Or (Eq (admin_indi_has_citizenship admin a usa) False) % 11.50/11.68 (Or (Eq (admin_indi_has_polygraph_for_compartment admin a a_1) False) % 11.50/11.68 (Or (Eq (admin_indi_has_credit_for_compartment admin a a_1) False) % 11.50/11.68 (Or (Eq (admin_compartment_has_sso admin a_1 a_2) False) % 11.50/11.68 (Or (Eq (sso_indi_has_compartment a_2 a a_1) False) % 11.50/11.68 (Or (Eq (admin_indi_has_background_for_compartment admin a a_1) False) % 11.50/11.68 (Or (Eq (admin_indi_has_level_for_compartment admin a a_1) False) % 11.50/11.68 (Or (Eq (admin_indi_has_compartments admin a a_3) False) % 11.50/11.68 (Eq (admin_indi_has_compartments admin a (cons a_1 a_3)) True)))))))))) % 11.50/11.68 Clause #317 (by superposition #[316, 79]): ∀ (a a_1 : Iota), % 11.50/11.68 Or (Eq (admin_indi_has_employment admin alice) False) % 11.50/11.68 (Or (Eq (admin_indi_has_citizenship admin alice usa) False) % 11.50/11.68 (Or (Eq (admin_indi_has_polygraph_for_compartment admin alice compartmenta) False) % 11.50/11.68 (Or (Eq (admin_indi_has_credit_for_compartment admin alice compartmenta) False) % 11.50/11.68 (Or (Eq (admin_compartment_has_sso admin compartmenta a) False) % 11.50/11.68 (Or (Eq (sso_indi_has_compartment a alice compartmenta) False) % 11.50/11.68 (Or (Eq (admin_indi_has_background_for_compartment admin alice compartmenta) False) % 11.50/11.68 (Or (Eq (admin_indi_has_level_for_compartment admin alice compartmenta) False) % 11.50/11.68 (Or (Eq (admin_indi_has_compartments admin alice a_1) False) % 11.50/11.68 (Or (Eq (admin_indi_has_compartments admin alice (cons compartmenta a_1)) True) % 11.50/11.68 (Eq False True)))))))))) % 11.50/11.68 Clause #318 (by superposition #[316, 78]): ∀ (a a_1 : Iota), % 11.50/11.68 Or (Eq (admin_indi_has_employment admin alice) False) % 11.50/11.68 (Or (Eq (admin_indi_has_citizenship admin alice usa) False) % 11.50/11.68 (Or (Eq (admin_indi_has_polygraph_for_compartment admin alice compartmentb) False) % 11.50/11.69 (Or (Eq (admin_indi_has_credit_for_compartment admin alice compartmentb) False) % 11.50/11.69 (Or (Eq (admin_compartment_has_sso admin compartmentb a) False) % 11.50/11.69 (Or (Eq (sso_indi_has_compartment a alice compartmentb) False) % 11.50/11.69 (Or (Eq (admin_indi_has_background_for_compartment admin alice compartmentb) False) % 11.50/11.69 (Or (Eq (admin_indi_has_level_for_compartment admin alice compartmentb) False) % 11.50/11.69 (Or (Eq (admin_indi_has_compartments admin alice a_1) False) % 11.50/11.69 (Or (Eq (admin_indi_has_compartments admin alice (cons compartmentb a_1)) True) % 11.50/11.69 (Eq False True)))))))))) % 11.50/11.69 Clause #319 (by clausification #[231]): ∀ (a : Iota), % 11.50/11.69 Or (Eq (owner_indi_has_need_to_know owner_secretfile a secretfile) False) % 11.50/11.69 (Eq (admin_indi_has_need_to_know_for_file admin a secretfile) True) % 11.50/11.69 Clause #320 (by superposition #[319, 82]): Or (Eq (admin_indi_has_need_to_know_for_file admin alice secretfile) True) (Eq False True) % 11.50/11.69 Clause #321 (by clausification #[320]): Eq (admin_indi_has_need_to_know_for_file admin alice secretfile) True % 11.50/11.69 Clause #322 (by clausification #[33]): ∀ (a : Iota), % 11.50/11.69 Eq % 11.50/11.69 (∀ (C OCA L1 L2 B2 : Iota), % 11.50/11.69 system_indi_is_oca system OCA → % 11.50/11.69 oca_compartment_is_compartment OCA C L1 L2 no B2 → admin_indi_has_credit_for_compartment admin a C) % 11.50/11.69 True % 11.50/11.69 Clause #323 (by clausification #[322]): ∀ (a a_1 : Iota), % 11.50/11.69 Eq % 11.50/11.69 (∀ (OCA L1 L2 B2 : Iota), % 11.50/11.69 system_indi_is_oca system OCA → % 11.50/11.69 oca_compartment_is_compartment OCA a L1 L2 no B2 → admin_indi_has_credit_for_compartment admin a_1 a) % 11.50/11.69 True % 11.50/11.69 Clause #324 (by clausification #[323]): ∀ (a a_1 a_2 : Iota), % 11.50/11.69 Eq % 11.50/11.69 (∀ (L1 L2 B2 : Iota), % 11.50/11.69 system_indi_is_oca system a → % 11.50/11.69 oca_compartment_is_compartment a a_1 L1 L2 no B2 → admin_indi_has_credit_for_compartment admin a_2 a_1) % 11.50/11.69 True % 11.50/11.69 Clause #325 (by clausification #[324]): ∀ (a a_1 a_2 a_3 : Iota), % 11.50/11.69 Eq % 11.50/11.69 (∀ (L2 B2 : Iota), % 11.50/11.69 system_indi_is_oca system a → % 11.50/11.69 oca_compartment_is_compartment a a_1 a_2 L2 no B2 → admin_indi_has_credit_for_compartment admin a_3 a_1) % 11.50/11.69 True % 11.50/11.69 Clause #326 (by clausification #[325]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 11.50/11.69 Eq % 11.50/11.69 (∀ (B2 : Iota), % 11.50/11.69 system_indi_is_oca system a → % 11.50/11.69 oca_compartment_is_compartment a a_1 a_2 a_3 no B2 → admin_indi_has_credit_for_compartment admin a_4 a_1) % 11.50/11.69 True % 11.50/11.69 Clause #327 (by clausification #[326]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 11.50/11.69 Eq % 11.50/11.69 (system_indi_is_oca system a → % 11.50/11.69 oca_compartment_is_compartment a a_1 a_2 a_3 no a_4 → admin_indi_has_credit_for_compartment admin a_5 a_1) % 11.50/11.69 True % 11.50/11.69 Clause #328 (by clausification #[327]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 11.50/11.69 Or (Eq (system_indi_is_oca system a) False) % 11.50/11.69 (Eq (oca_compartment_is_compartment a a_1 a_2 a_3 no a_4 → admin_indi_has_credit_for_compartment admin a_5 a_1) % 11.50/11.69 True) % 11.50/11.69 Clause #329 (by clausification #[328]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 11.50/11.69 Or (Eq (system_indi_is_oca system a) False) % 11.50/11.69 (Or (Eq (oca_compartment_is_compartment a a_1 a_2 a_3 no a_4) False) % 11.50/11.69 (Eq (admin_indi_has_credit_for_compartment admin a_5 a_1) True)) % 11.50/11.69 Clause #330 (by superposition #[329, 41]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 11.50/11.69 Or (Eq (oca_compartment_is_compartment oca a a_1 a_2 no a_3) False) % 11.50/11.69 (Or (Eq (admin_indi_has_credit_for_compartment admin a_4 a) True) (Eq False True)) % 11.50/11.69 Clause #334 (by clausification #[28]): ∀ (a : Iota), % 11.50/11.69 Eq % 11.50/11.69 (∀ (C OCA L1 L2 B1 B2 : Iota), % 11.50/11.69 system_indi_is_oca system OCA → % 11.50/11.69 oca_compartment_is_compartment OCA C L1 L2 B1 B2 → % 11.50/11.69 admin_indi_has_background admin a L2 → admin_indi_has_background_for_compartment admin a C) % 11.50/11.69 True % 11.50/11.69 Clause #335 (by clausification #[334]): ∀ (a a_1 : Iota), % 11.50/11.69 Eq % 11.50/11.69 (∀ (OCA L1 L2 B1 B2 : Iota), % 11.50/11.69 system_indi_is_oca system OCA → % 11.50/11.69 oca_compartment_is_compartment OCA a L1 L2 B1 B2 → % 11.50/11.69 admin_indi_has_background admin a_1 L2 → admin_indi_has_background_for_compartment admin a_1 a) % 11.50/11.69 True % 11.54/11.70 Clause #336 (by clausification #[335]): ∀ (a a_1 a_2 : Iota), % 11.54/11.70 Eq % 11.54/11.70 (∀ (L1 L2 B1 B2 : Iota), % 11.54/11.70 system_indi_is_oca system a → % 11.54/11.70 oca_compartment_is_compartment a a_1 L1 L2 B1 B2 → % 11.54/11.70 admin_indi_has_background admin a_2 L2 → admin_indi_has_background_for_compartment admin a_2 a_1) % 11.54/11.70 True % 11.54/11.70 Clause #337 (by clausification #[336]): ∀ (a a_1 a_2 a_3 : Iota), % 11.54/11.70 Eq % 11.54/11.70 (∀ (L2 B1 B2 : Iota), % 11.54/11.70 system_indi_is_oca system a → % 11.54/11.70 oca_compartment_is_compartment a a_1 a_2 L2 B1 B2 → % 11.54/11.70 admin_indi_has_background admin a_3 L2 → admin_indi_has_background_for_compartment admin a_3 a_1) % 11.54/11.70 True % 11.54/11.70 Clause #338 (by clausification #[337]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 11.54/11.70 Eq % 11.54/11.70 (∀ (B1 B2 : Iota), % 11.54/11.70 system_indi_is_oca system a → % 11.54/11.70 oca_compartment_is_compartment a a_1 a_2 a_3 B1 B2 → % 11.54/11.70 admin_indi_has_background admin a_4 a_3 → admin_indi_has_background_for_compartment admin a_4 a_1) % 11.54/11.70 True % 11.54/11.70 Clause #339 (by clausification #[338]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 11.54/11.70 Eq % 11.54/11.70 (∀ (B2 : Iota), % 11.54/11.70 system_indi_is_oca system a → % 11.54/11.70 oca_compartment_is_compartment a a_1 a_2 a_3 a_4 B2 → % 11.54/11.70 admin_indi_has_background admin a_5 a_3 → admin_indi_has_background_for_compartment admin a_5 a_1) % 11.54/11.70 True % 11.54/11.70 Clause #340 (by clausification #[339]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 11.54/11.70 Eq % 11.54/11.70 (system_indi_is_oca system a → % 11.54/11.70 oca_compartment_is_compartment a a_1 a_2 a_3 a_4 a_5 → % 11.54/11.70 admin_indi_has_background admin a_6 a_3 → admin_indi_has_background_for_compartment admin a_6 a_1) % 11.54/11.70 True % 11.54/11.70 Clause #341 (by clausification #[340]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 11.54/11.70 Or (Eq (system_indi_is_oca system a) False) % 11.54/11.70 (Eq % 11.54/11.70 (oca_compartment_is_compartment a a_1 a_2 a_3 a_4 a_5 → % 11.54/11.70 admin_indi_has_background admin a_6 a_3 → admin_indi_has_background_for_compartment admin a_6 a_1) % 11.54/11.70 True) % 11.54/11.70 Clause #342 (by clausification #[341]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 11.54/11.70 Or (Eq (system_indi_is_oca system a) False) % 11.54/11.70 (Or (Eq (oca_compartment_is_compartment a a_1 a_2 a_3 a_4 a_5) False) % 11.54/11.70 (Eq (admin_indi_has_background admin a_6 a_3 → admin_indi_has_background_for_compartment admin a_6 a_1) True)) % 11.54/11.70 Clause #343 (by clausification #[342]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 11.54/11.70 Or (Eq (system_indi_is_oca system a) False) % 11.54/11.70 (Or (Eq (oca_compartment_is_compartment a a_1 a_2 a_3 a_4 a_5) False) % 11.54/11.70 (Or (Eq (admin_indi_has_background admin a_6 a_3) False) % 11.54/11.70 (Eq (admin_indi_has_background_for_compartment admin a_6 a_1) True))) % 11.54/11.70 Clause #344 (by superposition #[343, 41]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 11.54/11.70 Or (Eq (oca_compartment_is_compartment oca a a_1 a_2 a_3 a_4) False) % 11.54/11.70 (Or (Eq (admin_indi_has_background admin a_5 a_2) False) % 11.54/11.70 (Or (Eq (admin_indi_has_background_for_compartment admin a_5 a) True) (Eq False True))) % 11.54/11.70 Clause #346 (by clausification #[31]): ∀ (a : Iota), % 11.54/11.70 Eq % 11.54/11.70 (∀ (C OCA L1 L2 B1 : Iota), % 11.54/11.70 system_indi_is_oca system OCA → % 11.54/11.70 oca_compartment_is_compartment OCA C L1 L2 B1 no → admin_indi_has_polygraph_for_compartment admin a C) % 11.54/11.70 True % 11.54/11.70 Clause #347 (by clausification #[346]): ∀ (a a_1 : Iota), % 11.54/11.70 Eq % 11.54/11.70 (∀ (OCA L1 L2 B1 : Iota), % 11.54/11.70 system_indi_is_oca system OCA → % 11.54/11.70 oca_compartment_is_compartment OCA a L1 L2 B1 no → admin_indi_has_polygraph_for_compartment admin a_1 a) % 11.54/11.70 True % 11.54/11.70 Clause #348 (by clausification #[347]): ∀ (a a_1 a_2 : Iota), % 11.54/11.70 Eq % 11.54/11.70 (∀ (L1 L2 B1 : Iota), % 11.54/11.70 system_indi_is_oca system a → % 11.54/11.70 oca_compartment_is_compartment a a_1 L1 L2 B1 no → admin_indi_has_polygraph_for_compartment admin a_2 a_1) % 11.54/11.70 True % 11.54/11.70 Clause #349 (by clausification #[348]): ∀ (a a_1 a_2 a_3 : Iota), % 11.54/11.70 Eq % 11.54/11.70 (∀ (L2 B1 : Iota), % 11.54/11.70 system_indi_is_oca system a → % 11.54/11.70 oca_compartment_is_compartment a a_1 a_2 L2 B1 no → admin_indi_has_polygraph_for_compartment admin a_3 a_1) % 11.54/11.70 True % 11.54/11.70 Clause #350 (by clausification #[349]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 11.54/11.70 Eq % 11.54/11.70 (∀ (B1 : Iota), % 11.54/11.70 system_indi_is_oca system a → % 11.54/11.70 oca_compartment_is_compartment a a_1 a_2 a_3 B1 no → admin_indi_has_polygraph_for_compartment admin a_4 a_1) % 11.54/11.72 True % 11.54/11.72 Clause #351 (by clausification #[350]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 11.54/11.72 Eq % 11.54/11.72 (system_indi_is_oca system a → % 11.54/11.72 oca_compartment_is_compartment a a_1 a_2 a_3 a_4 no → admin_indi_has_polygraph_for_compartment admin a_5 a_1) % 11.54/11.72 True % 11.54/11.72 Clause #352 (by clausification #[351]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 11.54/11.72 Or (Eq (system_indi_is_oca system a) False) % 11.54/11.72 (Eq (oca_compartment_is_compartment a a_1 a_2 a_3 a_4 no → admin_indi_has_polygraph_for_compartment admin a_5 a_1) % 11.54/11.72 True) % 11.54/11.72 Clause #353 (by clausification #[352]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 11.54/11.72 Or (Eq (system_indi_is_oca system a) False) % 11.54/11.72 (Or (Eq (oca_compartment_is_compartment a a_1 a_2 a_3 a_4 no) False) % 11.54/11.72 (Eq (admin_indi_has_polygraph_for_compartment admin a_5 a_1) True)) % 11.54/11.72 Clause #354 (by superposition #[353, 41]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 11.54/11.72 Or (Eq (oca_compartment_is_compartment oca a a_1 a_2 a_3 no) False) % 11.54/11.72 (Or (Eq (admin_indi_has_polygraph_for_compartment admin a_4 a) True) (Eq False True)) % 11.54/11.72 Clause #360 (by clausification #[29]): ∀ (a : Iota), % 11.54/11.72 Eq % 11.54/11.72 (∀ (C OCA L1 L2 B1 B2 : Iota), % 11.54/11.72 system_indi_is_oca system OCA → % 11.54/11.72 oca_compartment_is_compartment OCA C L1 L2 B1 B2 → % 11.54/11.72 admin_indi_has_level admin a L1 → admin_indi_has_level_for_compartment admin a C) % 11.54/11.72 True % 11.54/11.72 Clause #361 (by clausification #[360]): ∀ (a a_1 : Iota), % 11.54/11.72 Eq % 11.54/11.72 (∀ (OCA L1 L2 B1 B2 : Iota), % 11.54/11.72 system_indi_is_oca system OCA → % 11.54/11.72 oca_compartment_is_compartment OCA a L1 L2 B1 B2 → % 11.54/11.72 admin_indi_has_level admin a_1 L1 → admin_indi_has_level_for_compartment admin a_1 a) % 11.54/11.72 True % 11.54/11.72 Clause #362 (by clausification #[361]): ∀ (a a_1 a_2 : Iota), % 11.54/11.72 Eq % 11.54/11.72 (∀ (L1 L2 B1 B2 : Iota), % 11.54/11.72 system_indi_is_oca system a → % 11.54/11.72 oca_compartment_is_compartment a a_1 L1 L2 B1 B2 → % 11.54/11.72 admin_indi_has_level admin a_2 L1 → admin_indi_has_level_for_compartment admin a_2 a_1) % 11.54/11.72 True % 11.54/11.72 Clause #363 (by clausification #[362]): ∀ (a a_1 a_2 a_3 : Iota), % 11.54/11.72 Eq % 11.54/11.72 (∀ (L2 B1 B2 : Iota), % 11.54/11.72 system_indi_is_oca system a → % 11.54/11.72 oca_compartment_is_compartment a a_1 a_2 L2 B1 B2 → % 11.54/11.72 admin_indi_has_level admin a_3 a_2 → admin_indi_has_level_for_compartment admin a_3 a_1) % 11.54/11.72 True % 11.54/11.72 Clause #364 (by clausification #[363]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 11.54/11.72 Eq % 11.54/11.72 (∀ (B1 B2 : Iota), % 11.54/11.72 system_indi_is_oca system a → % 11.54/11.72 oca_compartment_is_compartment a a_1 a_2 a_3 B1 B2 → % 11.54/11.72 admin_indi_has_level admin a_4 a_2 → admin_indi_has_level_for_compartment admin a_4 a_1) % 11.54/11.72 True % 11.54/11.72 Clause #365 (by clausification #[364]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 11.54/11.72 Eq % 11.54/11.72 (∀ (B2 : Iota), % 11.54/11.72 system_indi_is_oca system a → % 11.54/11.72 oca_compartment_is_compartment a a_1 a_2 a_3 a_4 B2 → % 11.54/11.72 admin_indi_has_level admin a_5 a_2 → admin_indi_has_level_for_compartment admin a_5 a_1) % 11.54/11.72 True % 11.54/11.72 Clause #366 (by clausification #[365]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 11.54/11.72 Eq % 11.54/11.72 (system_indi_is_oca system a → % 11.54/11.72 oca_compartment_is_compartment a a_1 a_2 a_3 a_4 a_5 → % 11.54/11.72 admin_indi_has_level admin a_6 a_2 → admin_indi_has_level_for_compartment admin a_6 a_1) % 11.54/11.72 True % 11.54/11.72 Clause #367 (by clausification #[366]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 11.54/11.72 Or (Eq (system_indi_is_oca system a) False) % 11.54/11.72 (Eq % 11.54/11.72 (oca_compartment_is_compartment a a_1 a_2 a_3 a_4 a_5 → % 11.54/11.72 admin_indi_has_level admin a_6 a_2 → admin_indi_has_level_for_compartment admin a_6 a_1) % 11.54/11.72 True) % 11.54/11.72 Clause #368 (by clausification #[367]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 11.54/11.72 Or (Eq (system_indi_is_oca system a) False) % 11.54/11.72 (Or (Eq (oca_compartment_is_compartment a a_1 a_2 a_3 a_4 a_5) False) % 11.54/11.72 (Eq (admin_indi_has_level admin a_6 a_2 → admin_indi_has_level_for_compartment admin a_6 a_1) True)) % 11.54/11.72 Clause #369 (by clausification #[368]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 11.54/11.72 Or (Eq (system_indi_is_oca system a) False) % 11.54/11.72 (Or (Eq (oca_compartment_is_compartment a a_1 a_2 a_3 a_4 a_5) False) % 11.54/11.72 (Or (Eq (admin_indi_has_level admin a_6 a_2) False) % 11.54/11.73 (Eq (admin_indi_has_level_for_compartment admin a_6 a_1) True))) % 11.54/11.73 Clause #370 (by superposition #[369, 41]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 11.54/11.73 Or (Eq (oca_compartment_is_compartment oca a a_1 a_2 a_3 a_4) False) % 11.54/11.73 (Or (Eq (admin_indi_has_level admin a_5 a_1) False) % 11.54/11.73 (Or (Eq (admin_indi_has_level_for_compartment admin a_5 a) True) (Eq False True))) % 11.54/11.73 Clause #374 (by clausification #[39]): ∀ (a : Iota), % 11.54/11.73 Eq % 11.54/11.73 (∀ (F : Iota), % 11.54/11.73 state_file_is_not_working_paper F → % 11.54/11.73 admin_indi_has_citizenship_for_file admin a F → % 11.54/11.73 admin_indi_has_need_to_know_for_file admin a F → % 11.54/11.73 admin_indi_has_level_for_file admin a F → % 11.54/11.73 admin_indi_has_compartments_for_file admin a F → admin_indi_may_file admin a F read) % 11.54/11.73 True % 11.54/11.73 Clause #375 (by clausification #[374]): ∀ (a a_1 : Iota), % 11.54/11.73 Eq % 11.54/11.73 (state_file_is_not_working_paper a → % 11.54/11.73 admin_indi_has_citizenship_for_file admin a_1 a → % 11.54/11.73 admin_indi_has_need_to_know_for_file admin a_1 a → % 11.54/11.73 admin_indi_has_level_for_file admin a_1 a → % 11.54/11.73 admin_indi_has_compartments_for_file admin a_1 a → admin_indi_may_file admin a_1 a read) % 11.54/11.73 True % 11.54/11.73 Clause #376 (by clausification #[375]): ∀ (a a_1 : Iota), % 11.54/11.73 Or (Eq (state_file_is_not_working_paper a) False) % 11.54/11.73 (Eq % 11.54/11.73 (admin_indi_has_citizenship_for_file admin a_1 a → % 11.54/11.73 admin_indi_has_need_to_know_for_file admin a_1 a → % 11.54/11.73 admin_indi_has_level_for_file admin a_1 a → % 11.54/11.73 admin_indi_has_compartments_for_file admin a_1 a → admin_indi_may_file admin a_1 a read) % 11.54/11.73 True) % 11.54/11.73 Clause #377 (by clausification #[376]): ∀ (a a_1 : Iota), % 11.54/11.73 Or (Eq (state_file_is_not_working_paper a) False) % 11.54/11.73 (Or (Eq (admin_indi_has_citizenship_for_file admin a_1 a) False) % 11.54/11.73 (Eq % 11.54/11.73 (admin_indi_has_need_to_know_for_file admin a_1 a → % 11.54/11.73 admin_indi_has_level_for_file admin a_1 a → % 11.54/11.73 admin_indi_has_compartments_for_file admin a_1 a → admin_indi_may_file admin a_1 a read) % 11.54/11.73 True)) % 11.54/11.73 Clause #378 (by clausification #[377]): ∀ (a a_1 : Iota), % 11.57/11.73 Or (Eq (state_file_is_not_working_paper a) False) % 11.57/11.73 (Or (Eq (admin_indi_has_citizenship_for_file admin a_1 a) False) % 11.57/11.73 (Or (Eq (admin_indi_has_need_to_know_for_file admin a_1 a) False) % 11.57/11.73 (Eq % 11.57/11.73 (admin_indi_has_level_for_file admin a_1 a → % 11.57/11.73 admin_indi_has_compartments_for_file admin a_1 a → admin_indi_may_file admin a_1 a read) % 11.57/11.73 True))) % 11.57/11.73 Clause #379 (by clausification #[378]): ∀ (a a_1 : Iota), % 11.57/11.73 Or (Eq (state_file_is_not_working_paper a) False) % 11.57/11.73 (Or (Eq (admin_indi_has_citizenship_for_file admin a_1 a) False) % 11.57/11.73 (Or (Eq (admin_indi_has_need_to_know_for_file admin a_1 a) False) % 11.57/11.73 (Or (Eq (admin_indi_has_level_for_file admin a_1 a) False) % 11.57/11.73 (Eq (admin_indi_has_compartments_for_file admin a_1 a → admin_indi_may_file admin a_1 a read) True)))) % 11.57/11.73 Clause #380 (by clausification #[379]): ∀ (a a_1 : Iota), % 11.57/11.73 Or (Eq (state_file_is_not_working_paper a) False) % 11.57/11.73 (Or (Eq (admin_indi_has_citizenship_for_file admin a_1 a) False) % 11.57/11.73 (Or (Eq (admin_indi_has_need_to_know_for_file admin a_1 a) False) % 11.57/11.73 (Or (Eq (admin_indi_has_level_for_file admin a_1 a) False) % 11.57/11.73 (Or (Eq (admin_indi_has_compartments_for_file admin a_1 a) False) % 11.57/11.73 (Eq (admin_indi_may_file admin a_1 a read) True))))) % 11.57/11.73 Clause #382 (by superposition #[380, 50]): ∀ (a : Iota), % 11.57/11.73 Or (Eq (admin_indi_has_citizenship_for_file admin a secretfile) False) % 11.57/11.73 (Or (Eq (admin_indi_has_need_to_know_for_file admin a secretfile) False) % 11.57/11.73 (Or (Eq (admin_indi_has_level_for_file admin a secretfile) False) % 11.57/11.73 (Or (Eq (admin_indi_has_compartments_for_file admin a secretfile) False) % 11.57/11.73 (Or (Eq (admin_indi_may_file admin a secretfile read) True) (Eq False True))))) % 11.57/11.73 Clause #383 (by clausification #[32]): ∀ (a : Iota), % 11.57/11.73 Eq % 11.57/11.73 (∀ (C OCA L1 L2 B2 : Iota), % 11.57/11.73 system_indi_is_oca system OCA → % 11.57/11.73 oca_compartment_is_compartment OCA C L1 L2 yes B2 → % 11.57/11.73 admin_indi_has_credit admin a → admin_indi_has_credit_for_compartment admin a C) % 11.57/11.75 True % 11.57/11.75 Clause #384 (by clausification #[383]): ∀ (a a_1 : Iota), % 11.57/11.75 Eq % 11.57/11.75 (∀ (OCA L1 L2 B2 : Iota), % 11.57/11.75 system_indi_is_oca system OCA → % 11.57/11.75 oca_compartment_is_compartment OCA a L1 L2 yes B2 → % 11.57/11.75 admin_indi_has_credit admin a_1 → admin_indi_has_credit_for_compartment admin a_1 a) % 11.57/11.75 True % 11.57/11.75 Clause #385 (by clausification #[384]): ∀ (a a_1 a_2 : Iota), % 11.57/11.75 Eq % 11.57/11.75 (∀ (L1 L2 B2 : Iota), % 11.57/11.75 system_indi_is_oca system a → % 11.57/11.75 oca_compartment_is_compartment a a_1 L1 L2 yes B2 → % 11.57/11.75 admin_indi_has_credit admin a_2 → admin_indi_has_credit_for_compartment admin a_2 a_1) % 11.57/11.75 True % 11.57/11.75 Clause #386 (by clausification #[385]): ∀ (a a_1 a_2 a_3 : Iota), % 11.57/11.75 Eq % 11.57/11.75 (∀ (L2 B2 : Iota), % 11.57/11.75 system_indi_is_oca system a → % 11.57/11.75 oca_compartment_is_compartment a a_1 a_2 L2 yes B2 → % 11.57/11.75 admin_indi_has_credit admin a_3 → admin_indi_has_credit_for_compartment admin a_3 a_1) % 11.57/11.75 True % 11.57/11.75 Clause #387 (by clausification #[386]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 11.57/11.75 Eq % 11.57/11.75 (∀ (B2 : Iota), % 11.57/11.75 system_indi_is_oca system a → % 11.57/11.75 oca_compartment_is_compartment a a_1 a_2 a_3 yes B2 → % 11.57/11.75 admin_indi_has_credit admin a_4 → admin_indi_has_credit_for_compartment admin a_4 a_1) % 11.57/11.75 True % 11.57/11.75 Clause #388 (by clausification #[387]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 11.57/11.75 Eq % 11.57/11.75 (system_indi_is_oca system a → % 11.57/11.75 oca_compartment_is_compartment a a_1 a_2 a_3 yes a_4 → % 11.57/11.75 admin_indi_has_credit admin a_5 → admin_indi_has_credit_for_compartment admin a_5 a_1) % 11.57/11.75 True % 11.57/11.75 Clause #389 (by clausification #[388]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 11.57/11.75 Or (Eq (system_indi_is_oca system a) False) % 11.57/11.75 (Eq % 11.57/11.75 (oca_compartment_is_compartment a a_1 a_2 a_3 yes a_4 → % 11.57/11.75 admin_indi_has_credit admin a_5 → admin_indi_has_credit_for_compartment admin a_5 a_1) % 11.57/11.75 True) % 11.57/11.75 Clause #390 (by clausification #[389]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 11.57/11.75 Or (Eq (system_indi_is_oca system a) False) % 11.57/11.75 (Or (Eq (oca_compartment_is_compartment a a_1 a_2 a_3 yes a_4) False) % 11.57/11.75 (Eq (admin_indi_has_credit admin a_5 → admin_indi_has_credit_for_compartment admin a_5 a_1) True)) % 11.57/11.75 Clause #391 (by clausification #[390]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 11.57/11.75 Or (Eq (system_indi_is_oca system a) False) % 11.57/11.75 (Or (Eq (oca_compartment_is_compartment a a_1 a_2 a_3 yes a_4) False) % 11.57/11.75 (Or (Eq (admin_indi_has_credit admin a_5) False) (Eq (admin_indi_has_credit_for_compartment admin a_5 a_1) True))) % 11.57/11.75 Clause #392 (by superposition #[391, 41]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 11.57/11.75 Or (Eq (oca_compartment_is_compartment oca a a_1 a_2 yes a_3) False) % 11.57/11.75 (Or (Eq (admin_indi_has_credit admin a_4) False) % 11.57/11.75 (Or (Eq (admin_indi_has_credit_for_compartment admin a_4 a) True) (Eq False True))) % 11.57/11.75 Clause #393 (by clausification #[30]): ∀ (a : Iota), % 11.57/11.75 Eq % 11.57/11.75 (∀ (C OCA L1 L2 B1 : Iota), % 11.57/11.75 system_indi_is_oca system OCA → % 11.57/11.75 oca_compartment_is_compartment OCA C L1 L2 B1 yes → % 11.57/11.75 admin_indi_has_polygraph admin a → admin_indi_has_polygraph_for_compartment admin a C) % 11.57/11.75 True % 11.57/11.75 Clause #394 (by clausification #[393]): ∀ (a a_1 : Iota), % 11.57/11.75 Eq % 11.57/11.75 (∀ (OCA L1 L2 B1 : Iota), % 11.57/11.75 system_indi_is_oca system OCA → % 11.57/11.75 oca_compartment_is_compartment OCA a L1 L2 B1 yes → % 11.57/11.75 admin_indi_has_polygraph admin a_1 → admin_indi_has_polygraph_for_compartment admin a_1 a) % 11.57/11.75 True % 11.57/11.75 Clause #395 (by clausification #[394]): ∀ (a a_1 a_2 : Iota), % 11.57/11.75 Eq % 11.57/11.75 (∀ (L1 L2 B1 : Iota), % 11.57/11.75 system_indi_is_oca system a → % 11.57/11.75 oca_compartment_is_compartment a a_1 L1 L2 B1 yes → % 11.57/11.75 admin_indi_has_polygraph admin a_2 → admin_indi_has_polygraph_for_compartment admin a_2 a_1) % 11.57/11.75 True % 11.57/11.75 Clause #396 (by clausification #[395]): ∀ (a a_1 a_2 a_3 : Iota), % 11.57/11.75 Eq % 11.57/11.75 (∀ (L2 B1 : Iota), % 11.57/11.75 system_indi_is_oca system a → % 11.57/11.75 oca_compartment_is_compartment a a_1 a_2 L2 B1 yes → % 11.57/11.75 admin_indi_has_polygraph admin a_3 → admin_indi_has_polygraph_for_compartment admin a_3 a_1) % 11.57/11.75 True % 11.57/11.75 Clause #397 (by clausification #[396]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 11.57/11.75 Eq % 11.57/11.75 (∀ (B1 : Iota), % 11.57/11.75 system_indi_is_oca system a → % 11.57/11.76 oca_compartment_is_compartment a a_1 a_2 a_3 B1 yes → % 11.57/11.76 admin_indi_has_polygraph admin a_4 → admin_indi_has_polygraph_for_compartment admin a_4 a_1) % 11.57/11.76 True % 11.57/11.76 Clause #398 (by clausification #[397]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 11.57/11.76 Eq % 11.57/11.76 (system_indi_is_oca system a → % 11.57/11.76 oca_compartment_is_compartment a a_1 a_2 a_3 a_4 yes → % 11.57/11.76 admin_indi_has_polygraph admin a_5 → admin_indi_has_polygraph_for_compartment admin a_5 a_1) % 11.57/11.76 True % 11.57/11.76 Clause #399 (by clausification #[398]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 11.57/11.76 Or (Eq (system_indi_is_oca system a) False) % 11.57/11.76 (Eq % 11.57/11.76 (oca_compartment_is_compartment a a_1 a_2 a_3 a_4 yes → % 11.57/11.76 admin_indi_has_polygraph admin a_5 → admin_indi_has_polygraph_for_compartment admin a_5 a_1) % 11.57/11.76 True) % 11.57/11.76 Clause #400 (by clausification #[399]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 11.57/11.76 Or (Eq (system_indi_is_oca system a) False) % 11.57/11.76 (Or (Eq (oca_compartment_is_compartment a a_1 a_2 a_3 a_4 yes) False) % 11.57/11.76 (Eq (admin_indi_has_polygraph admin a_5 → admin_indi_has_polygraph_for_compartment admin a_5 a_1) True)) % 11.57/11.76 Clause #401 (by clausification #[400]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 11.57/11.76 Or (Eq (system_indi_is_oca system a) False) % 11.57/11.76 (Or (Eq (oca_compartment_is_compartment a a_1 a_2 a_3 a_4 yes) False) % 11.57/11.76 (Or (Eq (admin_indi_has_polygraph admin a_5) False) % 11.57/11.76 (Eq (admin_indi_has_polygraph_for_compartment admin a_5 a_1) True))) % 11.57/11.76 Clause #402 (by superposition #[401, 41]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 11.57/11.76 Or (Eq (oca_compartment_is_compartment oca a a_1 a_2 a_3 yes) False) % 11.57/11.76 (Or (Eq (admin_indi_has_polygraph admin a_4) False) % 11.57/11.76 (Or (Eq (admin_indi_has_polygraph_for_compartment admin a_4 a) True) (Eq False True))) % 11.57/11.76 Clause #403 (by clausification #[354]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 11.57/11.76 Or (Eq (oca_compartment_is_compartment oca a a_1 a_2 a_3 no) False) % 11.57/11.76 (Eq (admin_indi_has_polygraph_for_compartment admin a_4 a) True) % 11.57/11.76 Clause #404 (by superposition #[403, 43]): ∀ (a : Iota), Or (Eq (admin_indi_has_polygraph_for_compartment admin a compartmenta) True) (Eq False True) % 11.57/11.76 Clause #405 (by clausification #[117]): ∀ (a a_1 a_2 : Iota), % 11.57/11.76 Or (Eq (oca_compartment_has_scg oca a a_1) False) % 11.57/11.76 (Or (Eq (admin_compartment_has_sso admin a a_2) False) % 11.57/11.76 (Or (Eq (sso_compartment_has_scg a_2 a a_1) False) (Eq (admin_compartment_has_scg admin a a_1) True))) % 11.57/11.76 Clause #406 (by superposition #[405, 48]): ∀ (a : Iota), % 11.57/11.76 Or (Eq (admin_compartment_has_sso admin compartmenta a) False) % 11.57/11.76 (Or (Eq (sso_compartment_has_scg a compartmenta scg_compartmenta) False) % 11.57/11.76 (Or (Eq (admin_compartment_has_scg admin compartmenta scg_compartmenta) True) (Eq False True))) % 11.57/11.76 Clause #407 (by superposition #[405, 45]): ∀ (a : Iota), % 11.57/11.76 Or (Eq (admin_compartment_has_sso admin compartmentb a) False) % 11.57/11.76 (Or (Eq (sso_compartment_has_scg a compartmentb scg_compartmentb) False) % 11.57/11.76 (Or (Eq (admin_compartment_has_scg admin compartmentb scg_compartmentb) True) (Eq False True))) % 11.57/11.76 Clause #408 (by clausification #[404]): ∀ (a : Iota), Eq (admin_indi_has_polygraph_for_compartment admin a compartmenta) True % 11.57/11.76 Clause #409 (by clausification #[330]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 11.57/11.76 Or (Eq (oca_compartment_is_compartment oca a a_1 a_2 no a_3) False) % 11.57/11.76 (Eq (admin_indi_has_credit_for_compartment admin a_4 a) True) % 11.57/11.76 Clause #410 (by superposition #[409, 43]): ∀ (a : Iota), Or (Eq (admin_indi_has_credit_for_compartment admin a compartmenta) True) (Eq False True) % 11.57/11.76 Clause #411 (by clausification #[410]): ∀ (a : Iota), Eq (admin_indi_has_credit_for_compartment admin a compartmenta) True % 11.57/11.76 Clause #412 (by clausification #[269]): ∀ (a a_1 a_2 : Iota), % 11.57/11.76 Or (Eq (background_admin_indi_has_background background_admin a a_1) False) % 11.57/11.76 (Or (Eq (loca_level_below admin a_2 a_1) False) (Eq (admin_indi_has_background admin a a_2) True)) % 11.57/11.76 Clause #413 (by superposition #[412, 74]): ∀ (a : Iota), % 11.57/11.76 Or (Eq (loca_level_below admin a topsecret) False) % 11.57/11.76 (Or (Eq (admin_indi_has_background admin alice a) True) (Eq False True)) % 11.57/11.76 Clause #414 (by clausification #[413]): ∀ (a : Iota), Or (Eq (loca_level_below admin a topsecret) False) (Eq (admin_indi_has_background admin alice a) True) % 11.57/11.78 Clause #415 (by superposition #[414, 257]): Or (Eq (admin_indi_has_background admin alice secret) True) (Eq False True) % 11.57/11.78 Clause #416 (by superposition #[414, 270]): Or (Eq (admin_indi_has_background admin alice confidential) True) (Eq False True) % 11.57/11.78 Clause #417 (by superposition #[414, 278]): Or (Eq (admin_indi_has_background admin alice sbu) True) (Eq False True) % 11.57/11.78 Clause #419 (by superposition #[414, 93]): Or (Eq (admin_indi_has_background admin alice topsecret) True) (Eq False True) % 11.57/11.78 Clause #420 (by clausification #[159]): ∀ (a a_1 a_2 : Iota), % 11.57/11.78 Or (Eq (sso_file_has_compartments sso_compartmenta a a_1) False) % 11.57/11.78 (Or (Eq (admin_file_has_compartments_h admin a a_1 a_2) False) % 11.57/11.78 (Eq (admin_file_has_compartments_h admin a a_1 (cons compartmenta a_2)) True)) % 11.57/11.78 Clause #421 (by superposition #[420, 53]): ∀ (a : Iota), % 11.57/11.78 Or (Eq (admin_file_has_compartments_h admin secretfile (cons compartmentb (cons compartmenta nil)) a) False) % 11.57/11.78 (Or % 11.57/11.78 (Eq % 11.57/11.78 (admin_file_has_compartments_h admin secretfile (cons compartmentb (cons compartmenta nil)) % 11.57/11.78 (cons compartmenta a)) % 11.57/11.78 True) % 11.57/11.78 (Eq False True)) % 11.57/11.78 Clause #422 (by clausification #[419]): Eq (admin_indi_has_background admin alice topsecret) True % 11.57/11.78 Clause #424 (by clausification #[417]): Eq (admin_indi_has_background admin alice sbu) True % 11.57/11.78 Clause #425 (by clausification #[415]): Eq (admin_indi_has_background admin alice secret) True % 11.57/11.78 Clause #426 (by clausification #[416]): Eq (admin_indi_has_background admin alice confidential) True % 11.57/11.78 Clause #427 (by clausification #[160]): ∀ (a a_1 a_2 : Iota), % 11.57/11.78 Or (Eq (sso_file_has_compartments sso_compartmentb a a_1) False) % 11.57/11.78 (Or (Eq (admin_file_has_compartments_h admin a a_1 a_2) False) % 11.57/11.78 (Eq (admin_file_has_compartments_h admin a a_1 (cons compartmentb a_2)) True)) % 11.57/11.78 Clause #428 (by superposition #[427, 52]): ∀ (a : Iota), % 11.57/11.78 Or (Eq (admin_file_has_compartments_h admin secretfile (cons compartmentb (cons compartmenta nil)) a) False) % 11.57/11.78 (Or % 11.57/11.78 (Eq % 11.57/11.78 (admin_file_has_compartments_h admin secretfile (cons compartmentb (cons compartmenta nil)) % 11.57/11.78 (cons compartmentb a)) % 11.57/11.78 True) % 11.57/11.78 (Eq False True)) % 11.57/11.78 Clause #429 (by clausification #[407]): ∀ (a : Iota), % 11.57/11.78 Or (Eq (admin_compartment_has_sso admin compartmentb a) False) % 11.57/11.78 (Or (Eq (sso_compartment_has_scg a compartmentb scg_compartmentb) False) % 11.57/11.78 (Eq (admin_compartment_has_scg admin compartmentb scg_compartmentb) True)) % 11.57/11.78 Clause #430 (by superposition #[429, 129]): Or (Eq (sso_compartment_has_scg sso_compartmentb compartmentb scg_compartmentb) False) % 11.57/11.78 (Or (Eq (admin_compartment_has_scg admin compartmentb scg_compartmentb) True) (Eq False True)) % 11.57/11.78 Clause #431 (by clausification #[430]): Or (Eq (sso_compartment_has_scg sso_compartmentb compartmentb scg_compartmentb) False) % 11.57/11.78 (Eq (admin_compartment_has_scg admin compartmentb scg_compartmentb) True) % 11.57/11.78 Clause #432 (by forward demodulation #[431, 46]): Or (Eq True False) (Eq (admin_compartment_has_scg admin compartmentb scg_compartmentb) True) % 11.57/11.78 Clause #433 (by clausification #[432]): Eq (admin_compartment_has_scg admin compartmentb scg_compartmentb) True % 11.57/11.78 Clause #434 (by clausification #[406]): ∀ (a : Iota), % 11.57/11.78 Or (Eq (admin_compartment_has_sso admin compartmenta a) False) % 11.57/11.78 (Or (Eq (sso_compartment_has_scg a compartmenta scg_compartmenta) False) % 11.57/11.78 (Eq (admin_compartment_has_scg admin compartmenta scg_compartmenta) True)) % 11.57/11.78 Clause #435 (by superposition #[434, 128]): Or (Eq (sso_compartment_has_scg sso_compartmenta compartmenta scg_compartmenta) False) % 11.57/11.78 (Or (Eq (admin_compartment_has_scg admin compartmenta scg_compartmenta) True) (Eq False True)) % 11.57/11.78 Clause #436 (by clausification #[435]): Or (Eq (sso_compartment_has_scg sso_compartmenta compartmenta scg_compartmenta) False) % 11.57/11.78 (Eq (admin_compartment_has_scg admin compartmenta scg_compartmenta) True) % 11.57/11.78 Clause #437 (by forward demodulation #[436, 49]): Or (Eq True False) (Eq (admin_compartment_has_scg admin compartmenta scg_compartmenta) True) % 11.57/11.78 Clause #438 (by clausification #[437]): Eq (admin_compartment_has_scg admin compartmenta scg_compartmenta) True % 11.57/11.79 Clause #441 (by clausification #[179]): ∀ (a : Iota), % 11.57/11.79 Or (Eq (admin_file_has_compartments admin secretfile a) False) % 11.57/11.79 (Or (Eq (admin_file_has_level_h admin secretfile secret a) False) % 11.57/11.79 (Eq (admin_file_has_level admin secretfile secret) True)) % 11.57/11.79 Clause #462 (by clausification #[181]): Or % 11.57/11.79 (Eq % 11.57/11.79 (admin_file_has_compartments_h admin secretfile (cons compartmentb (cons compartmenta nil)) % 11.57/11.79 (cons compartmentb (cons compartmenta nil))) % 11.57/11.79 False) % 11.57/11.79 (Eq (admin_file_has_compartments admin secretfile (cons compartmentb (cons compartmenta nil))) True) % 11.57/11.79 Clause #464 (by clausification #[402]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 11.57/11.79 Or (Eq (oca_compartment_is_compartment oca a a_1 a_2 a_3 yes) False) % 11.57/11.79 (Or (Eq (admin_indi_has_polygraph admin a_4) False) % 11.57/11.79 (Eq (admin_indi_has_polygraph_for_compartment admin a_4 a) True)) % 11.57/11.79 Clause #465 (by superposition #[464, 42]): ∀ (a : Iota), % 11.57/11.79 Or (Eq (admin_indi_has_polygraph admin a) False) % 11.57/11.79 (Or (Eq (admin_indi_has_polygraph_for_compartment admin a compartmentb) True) (Eq False True)) % 11.57/11.79 Clause #466 (by clausification #[465]): ∀ (a : Iota), % 11.57/11.79 Or (Eq (admin_indi_has_polygraph admin a) False) % 11.57/11.79 (Eq (admin_indi_has_polygraph_for_compartment admin a compartmentb) True) % 11.57/11.79 Clause #467 (by superposition #[466, 220]): Or (Eq (admin_indi_has_polygraph_for_compartment admin alice compartmentb) True) (Eq False True) % 11.57/11.79 Clause #468 (by clausification #[467]): Eq (admin_indi_has_polygraph_for_compartment admin alice compartmentb) True % 11.57/11.79 Clause #469 (by clausification #[392]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 11.57/11.79 Or (Eq (oca_compartment_is_compartment oca a a_1 a_2 yes a_3) False) % 11.57/11.79 (Or (Eq (admin_indi_has_credit admin a_4) False) (Eq (admin_indi_has_credit_for_compartment admin a_4 a) True)) % 11.57/11.79 Clause #470 (by superposition #[469, 42]): ∀ (a : Iota), % 11.57/11.79 Or (Eq (admin_indi_has_credit admin a) False) % 11.57/11.79 (Or (Eq (admin_indi_has_credit_for_compartment admin a compartmentb) True) (Eq False True)) % 11.57/11.79 Clause #471 (by clausification #[195]): ∀ (a a_1 a_2 a_3 : Iota), % 11.57/11.79 Or (Eq (admin_compartment_has_scg admin compartmenta a) False) % 11.57/11.79 (Or (Eq (sso_file_has_level sso_compartmenta a_1 a_2 a) False) % 11.57/11.79 (Or (Eq (admin_file_has_level_h admin a_1 a_2 a_3) False) % 11.57/11.79 (Eq (admin_file_has_level_h admin a_1 a_2 (cons compartmenta a_3)) True))) % 11.57/11.79 Clause #472 (by superposition #[471, 438]): ∀ (a a_1 a_2 : Iota), % 11.57/11.79 Or (Eq (sso_file_has_level sso_compartmenta a a_1 scg_compartmenta) False) % 11.57/11.79 (Or (Eq (admin_file_has_level_h admin a a_1 a_2) False) % 11.57/11.79 (Or (Eq (admin_file_has_level_h admin a a_1 (cons compartmenta a_2)) True) (Eq False True))) % 11.57/11.79 Clause #473 (by clausification #[470]): ∀ (a : Iota), % 11.57/11.79 Or (Eq (admin_indi_has_credit admin a) False) (Eq (admin_indi_has_credit_for_compartment admin a compartmentb) True) % 11.57/11.79 Clause #474 (by superposition #[473, 184]): Or (Eq (admin_indi_has_credit_for_compartment admin alice compartmentb) True) (Eq False True) % 11.57/11.79 Clause #475 (by clausification #[474]): Eq (admin_indi_has_credit_for_compartment admin alice compartmentb) True % 11.57/11.79 Clause #476 (by clausification #[370]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 11.57/11.79 Or (Eq (oca_compartment_is_compartment oca a a_1 a_2 a_3 a_4) False) % 11.57/11.79 (Or (Eq (admin_indi_has_level admin a_5 a_1) False) (Eq (admin_indi_has_level_for_compartment admin a_5 a) True)) % 11.57/11.79 Clause #477 (by superposition #[476, 43]): ∀ (a : Iota), % 11.57/11.79 Or (Eq (admin_indi_has_level admin a sbu) False) % 11.57/11.79 (Or (Eq (admin_indi_has_level_for_compartment admin a compartmenta) True) (Eq False True)) % 11.57/11.79 Clause #478 (by superposition #[476, 42]): ∀ (a : Iota), % 11.57/11.79 Or (Eq (admin_indi_has_level admin a confidential) False) % 11.57/11.79 (Or (Eq (admin_indi_has_level_for_compartment admin a compartmentb) True) (Eq False True)) % 11.57/11.79 Clause #479 (by clausification #[478]): ∀ (a : Iota), % 11.57/11.79 Or (Eq (admin_indi_has_level admin a confidential) False) % 11.57/11.79 (Eq (admin_indi_has_level_for_compartment admin a compartmentb) True) % 11.57/11.79 Clause #480 (by clausification #[477]): ∀ (a : Iota), % 11.57/11.79 Or (Eq (admin_indi_has_level admin a sbu) False) (Eq (admin_indi_has_level_for_compartment admin a compartmenta) True) % 11.57/11.81 Clause #481 (by clausification #[196]): ∀ (a a_1 a_2 a_3 : Iota), % 11.57/11.81 Or (Eq (admin_compartment_has_scg admin compartmentb a) False) % 11.57/11.81 (Or (Eq (sso_file_has_level sso_compartmentb a_1 a_2 a) False) % 11.57/11.81 (Or (Eq (admin_file_has_level_h admin a_1 a_2 a_3) False) % 11.57/11.81 (Eq (admin_file_has_level_h admin a_1 a_2 (cons compartmentb a_3)) True))) % 11.57/11.81 Clause #482 (by superposition #[481, 433]): ∀ (a a_1 a_2 : Iota), % 11.57/11.81 Or (Eq (sso_file_has_level sso_compartmentb a a_1 scg_compartmentb) False) % 11.57/11.81 (Or (Eq (admin_file_has_level_h admin a a_1 a_2) False) % 11.57/11.81 (Or (Eq (admin_file_has_level_h admin a a_1 (cons compartmentb a_2)) True) (Eq False True))) % 11.57/11.81 Clause #483 (by clausification #[344]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 11.57/11.81 Or (Eq (oca_compartment_is_compartment oca a a_1 a_2 a_3 a_4) False) % 11.57/11.81 (Or (Eq (admin_indi_has_background admin a_5 a_2) False) % 11.57/11.81 (Eq (admin_indi_has_background_for_compartment admin a_5 a) True)) % 11.57/11.81 Clause #484 (by superposition #[483, 43]): ∀ (a : Iota), % 11.57/11.81 Or (Eq (admin_indi_has_background admin a unclassified) False) % 11.57/11.81 (Or (Eq (admin_indi_has_background_for_compartment admin a compartmenta) True) (Eq False True)) % 11.57/11.81 Clause #485 (by superposition #[483, 42]): ∀ (a : Iota), % 11.57/11.81 Or (Eq (admin_indi_has_background admin a topsecret) False) % 11.57/11.81 (Or (Eq (admin_indi_has_background_for_compartment admin a compartmentb) True) (Eq False True)) % 11.57/11.81 Clause #486 (by clausification #[485]): ∀ (a : Iota), % 11.57/11.81 Or (Eq (admin_indi_has_background admin a topsecret) False) % 11.57/11.81 (Eq (admin_indi_has_background_for_compartment admin a compartmentb) True) % 11.57/11.81 Clause #487 (by superposition #[486, 422]): Or (Eq (admin_indi_has_background_for_compartment admin alice compartmentb) True) (Eq False True) % 11.57/11.81 Clause #488 (by clausification #[487]): Eq (admin_indi_has_background_for_compartment admin alice compartmentb) True % 11.57/11.81 Clause #489 (by clausification #[484]): ∀ (a : Iota), % 11.57/11.81 Or (Eq (admin_indi_has_background admin a unclassified) False) % 11.57/11.81 (Eq (admin_indi_has_background_for_compartment admin a compartmenta) True) % 11.57/11.81 Clause #490 (by forward demodulation #[489, 121]): ∀ (a : Iota), Or (Eq True False) (Eq (admin_indi_has_background_for_compartment admin a compartmenta) True) % 11.57/11.81 Clause #491 (by clausification #[490]): ∀ (a : Iota), Eq (admin_indi_has_background_for_compartment admin a compartmenta) True % 11.57/11.81 Clause #492 (by clausification #[482]): ∀ (a a_1 a_2 : Iota), % 11.57/11.81 Or (Eq (sso_file_has_level sso_compartmentb a a_1 scg_compartmentb) False) % 11.57/11.81 (Or (Eq (admin_file_has_level_h admin a a_1 a_2) False) % 11.57/11.81 (Eq (admin_file_has_level_h admin a a_1 (cons compartmentb a_2)) True)) % 11.57/11.81 Clause #493 (by superposition #[492, 55]): ∀ (a : Iota), % 11.57/11.81 Or (Eq (admin_file_has_level_h admin secretfile secret a) False) % 11.57/11.81 (Or (Eq (admin_file_has_level_h admin secretfile secret (cons compartmentb a)) True) (Eq False True)) % 11.57/11.81 Clause #496 (by clausification #[493]): ∀ (a : Iota), % 11.57/11.81 Or (Eq (admin_file_has_level_h admin secretfile secret a) False) % 11.57/11.81 (Eq (admin_file_has_level_h admin secretfile secret (cons compartmentb a)) True) % 11.57/11.81 Clause #518 (by clausification #[294]): ∀ (a a_1 a_2 : Iota), % 11.57/11.81 Or (Eq (admin_indi_has_citizenship admin alice usa) False) % 11.57/11.81 (Or (Eq (admin_indi_has_polygraph admin alice) False) % 11.57/11.81 (Or (Eq (admin_indi_has_employment admin alice) False) % 11.57/11.81 (Or (Eq (admin_indi_has_credit admin alice) False) % 11.57/11.81 (Or (Eq (loca_level_below admin a secret) False) % 11.57/11.81 (Or (Eq (system_indi_is_level_admin system a_1) False) % 11.57/11.81 (Or (Eq (level_admin_indi_has_level a_1 alice a_2) False) % 11.57/11.81 (Or (Eq (loca_level_below admin a a_2) False) % 11.57/11.81 (Or (Eq (admin_indi_has_background admin alice a) False) % 11.57/11.81 (Eq (admin_indi_has_level admin alice a) True))))))))) % 11.57/11.81 Clause #519 (by forward demodulation #[518, 161]): ∀ (a a_1 a_2 : Iota), % 11.57/11.81 Or (Eq True False) % 11.57/11.81 (Or (Eq (admin_indi_has_polygraph admin alice) False) % 11.57/11.81 (Or (Eq (admin_indi_has_employment admin alice) False) % 11.57/11.81 (Or (Eq (admin_indi_has_credit admin alice) False) % 11.57/11.83 (Or (Eq (loca_level_below admin a secret) False) % 11.57/11.83 (Or (Eq (system_indi_is_level_admin system a_1) False) % 11.57/11.83 (Or (Eq (level_admin_indi_has_level a_1 alice a_2) False) % 11.57/11.83 (Or (Eq (loca_level_below admin a a_2) False) % 11.57/11.83 (Or (Eq (admin_indi_has_background admin alice a) False) % 11.57/11.83 (Eq (admin_indi_has_level admin alice a) True))))))))) % 11.57/11.83 Clause #520 (by clausification #[519]): ∀ (a a_1 a_2 : Iota), % 11.57/11.83 Or (Eq (admin_indi_has_polygraph admin alice) False) % 11.57/11.83 (Or (Eq (admin_indi_has_employment admin alice) False) % 11.57/11.83 (Or (Eq (admin_indi_has_credit admin alice) False) % 11.57/11.83 (Or (Eq (loca_level_below admin a secret) False) % 11.57/11.83 (Or (Eq (system_indi_is_level_admin system a_1) False) % 11.57/11.83 (Or (Eq (level_admin_indi_has_level a_1 alice a_2) False) % 11.57/11.83 (Or (Eq (loca_level_below admin a a_2) False) % 11.57/11.83 (Or (Eq (admin_indi_has_background admin alice a) False) % 11.57/11.83 (Eq (admin_indi_has_level admin alice a) True)))))))) % 11.57/11.83 Clause #521 (by forward demodulation #[520, 220]): ∀ (a a_1 a_2 : Iota), % 11.57/11.83 Or (Eq True False) % 11.57/11.83 (Or (Eq (admin_indi_has_employment admin alice) False) % 11.57/11.83 (Or (Eq (admin_indi_has_credit admin alice) False) % 11.57/11.83 (Or (Eq (loca_level_below admin a secret) False) % 11.57/11.83 (Or (Eq (system_indi_is_level_admin system a_1) False) % 11.57/11.83 (Or (Eq (level_admin_indi_has_level a_1 alice a_2) False) % 11.57/11.83 (Or (Eq (loca_level_below admin a a_2) False) % 11.57/11.83 (Or (Eq (admin_indi_has_background admin alice a) False) % 11.57/11.83 (Eq (admin_indi_has_level admin alice a) True)))))))) % 11.57/11.83 Clause #522 (by clausification #[521]): ∀ (a a_1 a_2 : Iota), % 11.57/11.83 Or (Eq (admin_indi_has_employment admin alice) False) % 11.57/11.83 (Or (Eq (admin_indi_has_credit admin alice) False) % 11.57/11.83 (Or (Eq (loca_level_below admin a secret) False) % 11.57/11.83 (Or (Eq (system_indi_is_level_admin system a_1) False) % 11.57/11.83 (Or (Eq (level_admin_indi_has_level a_1 alice a_2) False) % 11.57/11.83 (Or (Eq (loca_level_below admin a a_2) False) % 11.57/11.83 (Or (Eq (admin_indi_has_background admin alice a) False) % 11.57/11.83 (Eq (admin_indi_has_level admin alice a) True))))))) % 11.57/11.83 Clause #523 (by forward demodulation #[522, 199]): ∀ (a a_1 a_2 : Iota), % 11.57/11.83 Or (Eq True False) % 11.57/11.83 (Or (Eq (admin_indi_has_credit admin alice) False) % 11.57/11.83 (Or (Eq (loca_level_below admin a secret) False) % 11.57/11.83 (Or (Eq (system_indi_is_level_admin system a_1) False) % 11.57/11.83 (Or (Eq (level_admin_indi_has_level a_1 alice a_2) False) % 11.57/11.83 (Or (Eq (loca_level_below admin a a_2) False) % 11.57/11.83 (Or (Eq (admin_indi_has_background admin alice a) False) % 11.57/11.83 (Eq (admin_indi_has_level admin alice a) True))))))) % 11.57/11.83 Clause #524 (by clausification #[523]): ∀ (a a_1 a_2 : Iota), % 11.57/11.83 Or (Eq (admin_indi_has_credit admin alice) False) % 11.57/11.83 (Or (Eq (loca_level_below admin a secret) False) % 11.57/11.83 (Or (Eq (system_indi_is_level_admin system a_1) False) % 11.57/11.83 (Or (Eq (level_admin_indi_has_level a_1 alice a_2) False) % 11.57/11.83 (Or (Eq (loca_level_below admin a a_2) False) % 11.57/11.83 (Or (Eq (admin_indi_has_background admin alice a) False) (Eq (admin_indi_has_level admin alice a) True)))))) % 11.57/11.83 Clause #525 (by forward demodulation #[524, 184]): ∀ (a a_1 a_2 : Iota), % 11.57/11.83 Or (Eq True False) % 11.57/11.83 (Or (Eq (loca_level_below admin a secret) False) % 11.57/11.83 (Or (Eq (system_indi_is_level_admin system a_1) False) % 11.57/11.83 (Or (Eq (level_admin_indi_has_level a_1 alice a_2) False) % 11.57/11.83 (Or (Eq (loca_level_below admin a a_2) False) % 11.57/11.83 (Or (Eq (admin_indi_has_background admin alice a) False) (Eq (admin_indi_has_level admin alice a) True)))))) % 11.57/11.83 Clause #526 (by clausification #[525]): ∀ (a a_1 a_2 : Iota), % 11.57/11.83 Or (Eq (loca_level_below admin a secret) False) % 11.57/11.83 (Or (Eq (system_indi_is_level_admin system a_1) False) % 11.57/11.83 (Or (Eq (level_admin_indi_has_level a_1 alice a_2) False) % 11.57/11.83 (Or (Eq (loca_level_below admin a a_2) False) % 11.57/11.83 (Or (Eq (admin_indi_has_background admin alice a) False) (Eq (admin_indi_has_level admin alice a) True))))) % 11.57/11.83 Clause #527 (by superposition #[526, 260]): ∀ (a a_1 : Iota), % 11.67/11.84 Or (Eq (system_indi_is_level_admin system a) False) % 11.67/11.84 (Or (Eq (level_admin_indi_has_level a alice a_1) False) % 11.67/11.84 (Or (Eq (loca_level_below admin confidential a_1) False) % 11.67/11.84 (Or (Eq (admin_indi_has_background admin alice confidential) False) % 11.67/11.84 (Or (Eq (admin_indi_has_level admin alice confidential) True) (Eq False True))))) % 11.67/11.84 Clause #528 (by superposition #[526, 276]): ∀ (a a_1 : Iota), % 11.67/11.84 Or (Eq (system_indi_is_level_admin system a) False) % 11.67/11.84 (Or (Eq (level_admin_indi_has_level a alice a_1) False) % 11.67/11.84 (Or (Eq (loca_level_below admin sbu a_1) False) % 11.67/11.84 (Or (Eq (admin_indi_has_background admin alice sbu) False) % 11.67/11.84 (Or (Eq (admin_indi_has_level admin alice sbu) True) (Eq False True))))) % 11.67/11.84 Clause #530 (by superposition #[526, 93]): ∀ (a a_1 : Iota), % 11.67/11.84 Or (Eq (system_indi_is_level_admin system a) False) % 11.67/11.84 (Or (Eq (level_admin_indi_has_level a alice a_1) False) % 11.67/11.84 (Or (Eq (loca_level_below admin secret a_1) False) % 11.67/11.84 (Or (Eq (admin_indi_has_background admin alice secret) False) % 11.67/11.84 (Or (Eq (admin_indi_has_level admin alice secret) True) (Eq False True))))) % 11.67/11.84 Clause #541 (by clausification #[317]): ∀ (a a_1 : Iota), % 11.67/11.84 Or (Eq (admin_indi_has_employment admin alice) False) % 11.67/11.84 (Or (Eq (admin_indi_has_citizenship admin alice usa) False) % 11.67/11.84 (Or (Eq (admin_indi_has_polygraph_for_compartment admin alice compartmenta) False) % 11.67/11.84 (Or (Eq (admin_indi_has_credit_for_compartment admin alice compartmenta) False) % 11.67/11.84 (Or (Eq (admin_compartment_has_sso admin compartmenta a) False) % 11.67/11.84 (Or (Eq (sso_indi_has_compartment a alice compartmenta) False) % 11.67/11.84 (Or (Eq (admin_indi_has_background_for_compartment admin alice compartmenta) False) % 11.67/11.84 (Or (Eq (admin_indi_has_level_for_compartment admin alice compartmenta) False) % 11.67/11.84 (Or (Eq (admin_indi_has_compartments admin alice a_1) False) % 11.67/11.84 (Eq (admin_indi_has_compartments admin alice (cons compartmenta a_1)) True))))))))) % 11.67/11.84 Clause #542 (by forward demodulation #[541, 199]): ∀ (a a_1 : Iota), % 11.67/11.84 Or (Eq True False) % 11.67/11.84 (Or (Eq (admin_indi_has_citizenship admin alice usa) False) % 11.67/11.84 (Or (Eq (admin_indi_has_polygraph_for_compartment admin alice compartmenta) False) % 11.67/11.84 (Or (Eq (admin_indi_has_credit_for_compartment admin alice compartmenta) False) % 11.67/11.84 (Or (Eq (admin_compartment_has_sso admin compartmenta a) False) % 11.67/11.84 (Or (Eq (sso_indi_has_compartment a alice compartmenta) False) % 11.67/11.84 (Or (Eq (admin_indi_has_background_for_compartment admin alice compartmenta) False) % 11.67/11.84 (Or (Eq (admin_indi_has_level_for_compartment admin alice compartmenta) False) % 11.67/11.84 (Or (Eq (admin_indi_has_compartments admin alice a_1) False) % 11.67/11.84 (Eq (admin_indi_has_compartments admin alice (cons compartmenta a_1)) True))))))))) % 11.67/11.84 Clause #543 (by clausification #[542]): ∀ (a a_1 : Iota), % 11.67/11.84 Or (Eq (admin_indi_has_citizenship admin alice usa) False) % 11.67/11.84 (Or (Eq (admin_indi_has_polygraph_for_compartment admin alice compartmenta) False) % 11.67/11.84 (Or (Eq (admin_indi_has_credit_for_compartment admin alice compartmenta) False) % 11.67/11.84 (Or (Eq (admin_compartment_has_sso admin compartmenta a) False) % 11.67/11.84 (Or (Eq (sso_indi_has_compartment a alice compartmenta) False) % 11.67/11.84 (Or (Eq (admin_indi_has_background_for_compartment admin alice compartmenta) False) % 11.67/11.84 (Or (Eq (admin_indi_has_level_for_compartment admin alice compartmenta) False) % 11.67/11.84 (Or (Eq (admin_indi_has_compartments admin alice a_1) False) % 11.67/11.84 (Eq (admin_indi_has_compartments admin alice (cons compartmenta a_1)) True)))))))) % 11.67/11.84 Clause #544 (by forward demodulation #[543, 161]): ∀ (a a_1 : Iota), % 11.67/11.84 Or (Eq True False) % 11.67/11.84 (Or (Eq (admin_indi_has_polygraph_for_compartment admin alice compartmenta) False) % 11.67/11.84 (Or (Eq (admin_indi_has_credit_for_compartment admin alice compartmenta) False) % 11.67/11.84 (Or (Eq (admin_compartment_has_sso admin compartmenta a) False) % 11.67/11.84 (Or (Eq (sso_indi_has_compartment a alice compartmenta) False) % 11.67/11.86 (Or (Eq (admin_indi_has_background_for_compartment admin alice compartmenta) False) % 11.67/11.86 (Or (Eq (admin_indi_has_level_for_compartment admin alice compartmenta) False) % 11.67/11.86 (Or (Eq (admin_indi_has_compartments admin alice a_1) False) % 11.67/11.86 (Eq (admin_indi_has_compartments admin alice (cons compartmenta a_1)) True)))))))) % 11.67/11.86 Clause #545 (by clausification #[544]): ∀ (a a_1 : Iota), % 11.67/11.86 Or (Eq (admin_indi_has_polygraph_for_compartment admin alice compartmenta) False) % 11.67/11.86 (Or (Eq (admin_indi_has_credit_for_compartment admin alice compartmenta) False) % 11.67/11.86 (Or (Eq (admin_compartment_has_sso admin compartmenta a) False) % 11.67/11.86 (Or (Eq (sso_indi_has_compartment a alice compartmenta) False) % 11.67/11.86 (Or (Eq (admin_indi_has_background_for_compartment admin alice compartmenta) False) % 11.67/11.86 (Or (Eq (admin_indi_has_level_for_compartment admin alice compartmenta) False) % 11.67/11.86 (Or (Eq (admin_indi_has_compartments admin alice a_1) False) % 11.67/11.86 (Eq (admin_indi_has_compartments admin alice (cons compartmenta a_1)) True))))))) % 11.67/11.86 Clause #546 (by forward demodulation #[545, 408]): ∀ (a a_1 : Iota), % 11.67/11.86 Or (Eq True False) % 11.67/11.86 (Or (Eq (admin_indi_has_credit_for_compartment admin alice compartmenta) False) % 11.67/11.86 (Or (Eq (admin_compartment_has_sso admin compartmenta a) False) % 11.67/11.86 (Or (Eq (sso_indi_has_compartment a alice compartmenta) False) % 11.67/11.86 (Or (Eq (admin_indi_has_background_for_compartment admin alice compartmenta) False) % 11.67/11.86 (Or (Eq (admin_indi_has_level_for_compartment admin alice compartmenta) False) % 11.67/11.86 (Or (Eq (admin_indi_has_compartments admin alice a_1) False) % 11.67/11.86 (Eq (admin_indi_has_compartments admin alice (cons compartmenta a_1)) True))))))) % 11.67/11.86 Clause #547 (by clausification #[546]): ∀ (a a_1 : Iota), % 11.67/11.86 Or (Eq (admin_indi_has_credit_for_compartment admin alice compartmenta) False) % 11.67/11.86 (Or (Eq (admin_compartment_has_sso admin compartmenta a) False) % 11.67/11.86 (Or (Eq (sso_indi_has_compartment a alice compartmenta) False) % 11.67/11.86 (Or (Eq (admin_indi_has_background_for_compartment admin alice compartmenta) False) % 11.67/11.86 (Or (Eq (admin_indi_has_level_for_compartment admin alice compartmenta) False) % 11.67/11.86 (Or (Eq (admin_indi_has_compartments admin alice a_1) False) % 11.67/11.86 (Eq (admin_indi_has_compartments admin alice (cons compartmenta a_1)) True)))))) % 11.67/11.86 Clause #548 (by forward demodulation #[547, 411]): ∀ (a a_1 : Iota), % 11.67/11.86 Or (Eq True False) % 11.67/11.86 (Or (Eq (admin_compartment_has_sso admin compartmenta a) False) % 11.67/11.86 (Or (Eq (sso_indi_has_compartment a alice compartmenta) False) % 11.67/11.86 (Or (Eq (admin_indi_has_background_for_compartment admin alice compartmenta) False) % 11.67/11.86 (Or (Eq (admin_indi_has_level_for_compartment admin alice compartmenta) False) % 11.67/11.86 (Or (Eq (admin_indi_has_compartments admin alice a_1) False) % 11.67/11.86 (Eq (admin_indi_has_compartments admin alice (cons compartmenta a_1)) True)))))) % 11.67/11.86 Clause #549 (by clausification #[548]): ∀ (a a_1 : Iota), % 11.67/11.86 Or (Eq (admin_compartment_has_sso admin compartmenta a) False) % 11.67/11.86 (Or (Eq (sso_indi_has_compartment a alice compartmenta) False) % 11.67/11.86 (Or (Eq (admin_indi_has_background_for_compartment admin alice compartmenta) False) % 11.67/11.86 (Or (Eq (admin_indi_has_level_for_compartment admin alice compartmenta) False) % 11.67/11.86 (Or (Eq (admin_indi_has_compartments admin alice a_1) False) % 11.67/11.86 (Eq (admin_indi_has_compartments admin alice (cons compartmenta a_1)) True))))) % 11.67/11.86 Clause #550 (by forward demodulation #[549, 491]): ∀ (a a_1 : Iota), % 11.67/11.86 Or (Eq (admin_compartment_has_sso admin compartmenta a) False) % 11.67/11.86 (Or (Eq (sso_indi_has_compartment a alice compartmenta) False) % 11.67/11.86 (Or (Eq True False) % 11.67/11.86 (Or (Eq (admin_indi_has_level_for_compartment admin alice compartmenta) False) % 11.67/11.86 (Or (Eq (admin_indi_has_compartments admin alice a_1) False) % 11.67/11.86 (Eq (admin_indi_has_compartments admin alice (cons compartmenta a_1)) True))))) % 11.67/11.86 Clause #551 (by clausification #[550]): ∀ (a a_1 : Iota), % 11.67/11.86 Or (Eq (admin_compartment_has_sso admin compartmenta a) False) % 11.67/11.87 (Or (Eq (sso_indi_has_compartment a alice compartmenta) False) % 11.67/11.87 (Or (Eq (admin_indi_has_level_for_compartment admin alice compartmenta) False) % 11.67/11.87 (Or (Eq (admin_indi_has_compartments admin alice a_1) False) % 11.67/11.87 (Eq (admin_indi_has_compartments admin alice (cons compartmenta a_1)) True)))) % 11.67/11.87 Clause #552 (by superposition #[551, 128]): ∀ (a : Iota), % 11.67/11.87 Or (Eq (sso_indi_has_compartment sso_compartmenta alice compartmenta) False) % 11.67/11.87 (Or (Eq (admin_indi_has_level_for_compartment admin alice compartmenta) False) % 11.67/11.87 (Or (Eq (admin_indi_has_compartments admin alice a) False) % 11.67/11.87 (Or (Eq (admin_indi_has_compartments admin alice (cons compartmenta a)) True) (Eq False True)))) % 11.67/11.87 Clause #557 (by clausification #[472]): ∀ (a a_1 a_2 : Iota), % 11.67/11.87 Or (Eq (sso_file_has_level sso_compartmenta a a_1 scg_compartmenta) False) % 11.67/11.87 (Or (Eq (admin_file_has_level_h admin a a_1 a_2) False) % 11.67/11.87 (Eq (admin_file_has_level_h admin a a_1 (cons compartmenta a_2)) True)) % 11.67/11.87 Clause #558 (by superposition #[557, 56]): ∀ (a : Iota), % 11.67/11.87 Or (Eq (admin_file_has_level_h admin secretfile secret a) False) % 11.67/11.87 (Or (Eq (admin_file_has_level_h admin secretfile secret (cons compartmenta a)) True) (Eq False True)) % 11.67/11.87 Clause #559 (by clausification #[558]): ∀ (a : Iota), % 11.67/11.87 Or (Eq (admin_file_has_level_h admin secretfile secret a) False) % 11.67/11.87 (Eq (admin_file_has_level_h admin secretfile secret (cons compartmenta a)) True) % 11.67/11.87 Clause #567 (by superposition #[559, 172]): Or (Eq (admin_file_has_level_h admin secretfile secret (cons compartmenta nil)) True) (Eq False True) % 11.67/11.87 Clause #568 (by clausification #[567]): Eq (admin_file_has_level_h admin secretfile secret (cons compartmenta nil)) True % 11.67/11.87 Clause #569 (by superposition #[568, 496]): Or (Eq True False) % 11.67/11.87 (Eq (admin_file_has_level_h admin secretfile secret (cons compartmentb (cons compartmenta nil))) True) % 11.67/11.87 Clause #571 (by clausification #[318]): ∀ (a a_1 : Iota), % 11.67/11.87 Or (Eq (admin_indi_has_employment admin alice) False) % 11.67/11.87 (Or (Eq (admin_indi_has_citizenship admin alice usa) False) % 11.67/11.87 (Or (Eq (admin_indi_has_polygraph_for_compartment admin alice compartmentb) False) % 11.67/11.87 (Or (Eq (admin_indi_has_credit_for_compartment admin alice compartmentb) False) % 11.67/11.87 (Or (Eq (admin_compartment_has_sso admin compartmentb a) False) % 11.67/11.87 (Or (Eq (sso_indi_has_compartment a alice compartmentb) False) % 11.67/11.87 (Or (Eq (admin_indi_has_background_for_compartment admin alice compartmentb) False) % 11.67/11.87 (Or (Eq (admin_indi_has_level_for_compartment admin alice compartmentb) False) % 11.67/11.87 (Or (Eq (admin_indi_has_compartments admin alice a_1) False) % 11.67/11.87 (Eq (admin_indi_has_compartments admin alice (cons compartmentb a_1)) True))))))))) % 11.67/11.87 Clause #572 (by forward demodulation #[571, 199]): ∀ (a a_1 : Iota), % 11.67/11.87 Or (Eq True False) % 11.67/11.87 (Or (Eq (admin_indi_has_citizenship admin alice usa) False) % 11.67/11.87 (Or (Eq (admin_indi_has_polygraph_for_compartment admin alice compartmentb) False) % 11.67/11.87 (Or (Eq (admin_indi_has_credit_for_compartment admin alice compartmentb) False) % 11.67/11.87 (Or (Eq (admin_compartment_has_sso admin compartmentb a) False) % 11.67/11.87 (Or (Eq (sso_indi_has_compartment a alice compartmentb) False) % 11.67/11.87 (Or (Eq (admin_indi_has_background_for_compartment admin alice compartmentb) False) % 11.67/11.87 (Or (Eq (admin_indi_has_level_for_compartment admin alice compartmentb) False) % 11.67/11.87 (Or (Eq (admin_indi_has_compartments admin alice a_1) False) % 11.67/11.87 (Eq (admin_indi_has_compartments admin alice (cons compartmentb a_1)) True))))))))) % 11.67/11.87 Clause #573 (by clausification #[572]): ∀ (a a_1 : Iota), % 11.67/11.87 Or (Eq (admin_indi_has_citizenship admin alice usa) False) % 11.67/11.87 (Or (Eq (admin_indi_has_polygraph_for_compartment admin alice compartmentb) False) % 11.67/11.87 (Or (Eq (admin_indi_has_credit_for_compartment admin alice compartmentb) False) % 11.67/11.87 (Or (Eq (admin_compartment_has_sso admin compartmentb a) False) % 11.67/11.87 (Or (Eq (sso_indi_has_compartment a alice compartmentb) False) % 11.67/11.87 (Or (Eq (admin_indi_has_background_for_compartment admin alice compartmentb) False) % 11.67/11.88 (Or (Eq (admin_indi_has_level_for_compartment admin alice compartmentb) False) % 11.67/11.88 (Or (Eq (admin_indi_has_compartments admin alice a_1) False) % 11.67/11.88 (Eq (admin_indi_has_compartments admin alice (cons compartmentb a_1)) True)))))))) % 11.67/11.88 Clause #574 (by forward demodulation #[573, 161]): ∀ (a a_1 : Iota), % 11.67/11.88 Or (Eq True False) % 11.67/11.88 (Or (Eq (admin_indi_has_polygraph_for_compartment admin alice compartmentb) False) % 11.67/11.88 (Or (Eq (admin_indi_has_credit_for_compartment admin alice compartmentb) False) % 11.67/11.88 (Or (Eq (admin_compartment_has_sso admin compartmentb a) False) % 11.67/11.88 (Or (Eq (sso_indi_has_compartment a alice compartmentb) False) % 11.67/11.88 (Or (Eq (admin_indi_has_background_for_compartment admin alice compartmentb) False) % 11.67/11.88 (Or (Eq (admin_indi_has_level_for_compartment admin alice compartmentb) False) % 11.67/11.88 (Or (Eq (admin_indi_has_compartments admin alice a_1) False) % 11.67/11.88 (Eq (admin_indi_has_compartments admin alice (cons compartmentb a_1)) True)))))))) % 11.67/11.88 Clause #575 (by clausification #[574]): ∀ (a a_1 : Iota), % 11.67/11.88 Or (Eq (admin_indi_has_polygraph_for_compartment admin alice compartmentb) False) % 11.67/11.88 (Or (Eq (admin_indi_has_credit_for_compartment admin alice compartmentb) False) % 11.67/11.88 (Or (Eq (admin_compartment_has_sso admin compartmentb a) False) % 11.67/11.88 (Or (Eq (sso_indi_has_compartment a alice compartmentb) False) % 11.67/11.88 (Or (Eq (admin_indi_has_background_for_compartment admin alice compartmentb) False) % 11.67/11.88 (Or (Eq (admin_indi_has_level_for_compartment admin alice compartmentb) False) % 11.67/11.88 (Or (Eq (admin_indi_has_compartments admin alice a_1) False) % 11.67/11.88 (Eq (admin_indi_has_compartments admin alice (cons compartmentb a_1)) True))))))) % 11.67/11.88 Clause #576 (by forward demodulation #[575, 468]): ∀ (a a_1 : Iota), % 11.67/11.88 Or (Eq True False) % 11.67/11.88 (Or (Eq (admin_indi_has_credit_for_compartment admin alice compartmentb) False) % 11.67/11.88 (Or (Eq (admin_compartment_has_sso admin compartmentb a) False) % 11.67/11.88 (Or (Eq (sso_indi_has_compartment a alice compartmentb) False) % 11.67/11.88 (Or (Eq (admin_indi_has_background_for_compartment admin alice compartmentb) False) % 11.67/11.88 (Or (Eq (admin_indi_has_level_for_compartment admin alice compartmentb) False) % 11.67/11.88 (Or (Eq (admin_indi_has_compartments admin alice a_1) False) % 11.67/11.88 (Eq (admin_indi_has_compartments admin alice (cons compartmentb a_1)) True))))))) % 11.67/11.88 Clause #577 (by clausification #[576]): ∀ (a a_1 : Iota), % 11.67/11.88 Or (Eq (admin_indi_has_credit_for_compartment admin alice compartmentb) False) % 11.67/11.88 (Or (Eq (admin_compartment_has_sso admin compartmentb a) False) % 11.67/11.88 (Or (Eq (sso_indi_has_compartment a alice compartmentb) False) % 11.67/11.88 (Or (Eq (admin_indi_has_background_for_compartment admin alice compartmentb) False) % 11.67/11.88 (Or (Eq (admin_indi_has_level_for_compartment admin alice compartmentb) False) % 11.67/11.88 (Or (Eq (admin_indi_has_compartments admin alice a_1) False) % 11.67/11.88 (Eq (admin_indi_has_compartments admin alice (cons compartmentb a_1)) True)))))) % 11.67/11.88 Clause #578 (by forward demodulation #[577, 475]): ∀ (a a_1 : Iota), % 11.67/11.88 Or (Eq True False) % 11.67/11.88 (Or (Eq (admin_compartment_has_sso admin compartmentb a) False) % 11.67/11.88 (Or (Eq (sso_indi_has_compartment a alice compartmentb) False) % 11.67/11.88 (Or (Eq (admin_indi_has_background_for_compartment admin alice compartmentb) False) % 11.67/11.88 (Or (Eq (admin_indi_has_level_for_compartment admin alice compartmentb) False) % 11.67/11.88 (Or (Eq (admin_indi_has_compartments admin alice a_1) False) % 11.67/11.88 (Eq (admin_indi_has_compartments admin alice (cons compartmentb a_1)) True)))))) % 11.67/11.88 Clause #579 (by clausification #[578]): ∀ (a a_1 : Iota), % 11.67/11.88 Or (Eq (admin_compartment_has_sso admin compartmentb a) False) % 11.67/11.88 (Or (Eq (sso_indi_has_compartment a alice compartmentb) False) % 11.67/11.88 (Or (Eq (admin_indi_has_background_for_compartment admin alice compartmentb) False) % 11.67/11.88 (Or (Eq (admin_indi_has_level_for_compartment admin alice compartmentb) False) % 11.74/11.90 (Or (Eq (admin_indi_has_compartments admin alice a_1) False) % 11.74/11.90 (Eq (admin_indi_has_compartments admin alice (cons compartmentb a_1)) True))))) % 11.74/11.90 Clause #580 (by forward demodulation #[579, 488]): ∀ (a a_1 : Iota), % 11.74/11.90 Or (Eq (admin_compartment_has_sso admin compartmentb a) False) % 11.74/11.90 (Or (Eq (sso_indi_has_compartment a alice compartmentb) False) % 11.74/11.90 (Or (Eq True False) % 11.74/11.90 (Or (Eq (admin_indi_has_level_for_compartment admin alice compartmentb) False) % 11.74/11.90 (Or (Eq (admin_indi_has_compartments admin alice a_1) False) % 11.74/11.90 (Eq (admin_indi_has_compartments admin alice (cons compartmentb a_1)) True))))) % 11.74/11.90 Clause #581 (by clausification #[580]): ∀ (a a_1 : Iota), % 11.74/11.90 Or (Eq (admin_compartment_has_sso admin compartmentb a) False) % 11.74/11.90 (Or (Eq (sso_indi_has_compartment a alice compartmentb) False) % 11.74/11.90 (Or (Eq (admin_indi_has_level_for_compartment admin alice compartmentb) False) % 11.74/11.90 (Or (Eq (admin_indi_has_compartments admin alice a_1) False) % 11.74/11.90 (Eq (admin_indi_has_compartments admin alice (cons compartmentb a_1)) True)))) % 11.74/11.90 Clause #582 (by superposition #[581, 129]): ∀ (a : Iota), % 11.74/11.90 Or (Eq (sso_indi_has_compartment sso_compartmentb alice compartmentb) False) % 11.74/11.90 (Or (Eq (admin_indi_has_level_for_compartment admin alice compartmentb) False) % 11.74/11.90 (Or (Eq (admin_indi_has_compartments admin alice a) False) % 11.74/11.90 (Or (Eq (admin_indi_has_compartments admin alice (cons compartmentb a)) True) (Eq False True)))) % 11.74/11.90 Clause #583 (by clausification #[569]): Eq (admin_file_has_level_h admin secretfile secret (cons compartmentb (cons compartmenta nil))) True % 11.74/11.90 Clause #619 (by clausification #[382]): ∀ (a : Iota), % 11.74/11.90 Or (Eq (admin_indi_has_citizenship_for_file admin a secretfile) False) % 11.74/11.90 (Or (Eq (admin_indi_has_need_to_know_for_file admin a secretfile) False) % 11.74/11.90 (Or (Eq (admin_indi_has_level_for_file admin a secretfile) False) % 11.74/11.90 (Or (Eq (admin_indi_has_compartments_for_file admin a secretfile) False) % 11.74/11.90 (Eq (admin_indi_may_file admin a secretfile read) True)))) % 11.74/11.90 Clause #620 (by superposition #[619, 163]): Or (Eq (admin_indi_has_need_to_know_for_file admin alice secretfile) False) % 11.74/11.90 (Or (Eq (admin_indi_has_level_for_file admin alice secretfile) False) % 11.74/11.90 (Or (Eq (admin_indi_has_compartments_for_file admin alice secretfile) False) % 11.74/11.90 (Or (Eq (admin_indi_may_file admin alice secretfile read) True) (Eq False True)))) % 11.74/11.90 Clause #636 (by clausification #[421]): ∀ (a : Iota), % 11.74/11.90 Or (Eq (admin_file_has_compartments_h admin secretfile (cons compartmentb (cons compartmenta nil)) a) False) % 11.74/11.90 (Eq % 11.74/11.90 (admin_file_has_compartments_h admin secretfile (cons compartmentb (cons compartmenta nil)) (cons compartmenta a)) % 11.74/11.90 True) % 11.74/11.90 Clause #637 (by superposition #[636, 141]): Or % 11.74/11.90 (Eq % 11.74/11.90 (admin_file_has_compartments_h admin secretfile (cons compartmentb (cons compartmenta nil)) (cons compartmenta nil)) % 11.74/11.90 True) % 11.74/11.90 (Eq False True) % 11.74/11.90 Clause #638 (by clausification #[637]): Eq (admin_file_has_compartments_h admin secretfile (cons compartmentb (cons compartmenta nil)) (cons compartmenta nil)) % 11.74/11.90 True % 11.74/11.90 Clause #651 (by clausification #[428]): ∀ (a : Iota), % 11.74/11.90 Or (Eq (admin_file_has_compartments_h admin secretfile (cons compartmentb (cons compartmenta nil)) a) False) % 11.74/11.90 (Eq % 11.74/11.90 (admin_file_has_compartments_h admin secretfile (cons compartmentb (cons compartmenta nil)) (cons compartmentb a)) % 11.74/11.90 True) % 11.74/11.90 Clause #652 (by superposition #[651, 638]): Or % 11.74/11.90 (Eq % 11.74/11.90 (admin_file_has_compartments_h admin secretfile (cons compartmentb (cons compartmenta nil)) % 11.74/11.90 (cons compartmentb (cons compartmenta nil))) % 11.74/11.90 True) % 11.74/11.90 (Eq False True) % 11.74/11.90 Clause #658 (by clausification #[652]): Eq % 11.74/11.90 (admin_file_has_compartments_h admin secretfile (cons compartmentb (cons compartmenta nil)) % 11.74/11.90 (cons compartmentb (cons compartmenta nil))) % 11.74/11.90 True % 11.74/11.90 Clause #659 (by superposition #[658, 462]): Or (Eq True False) (Eq (admin_file_has_compartments admin secretfile (cons compartmentb (cons compartmenta nil))) True) % 11.74/11.90 Clause #662 (by clausification #[659]): Eq (admin_file_has_compartments admin secretfile (cons compartmentb (cons compartmenta nil))) True % 11.74/11.92 Clause #664 (by superposition #[662, 441]): Or (Eq True False) % 11.74/11.92 (Or (Eq (admin_file_has_level_h admin secretfile secret (cons compartmentb (cons compartmenta nil))) False) % 11.74/11.92 (Eq (admin_file_has_level admin secretfile secret) True)) % 11.74/11.92 Clause #666 (by superposition #[662, 209]): ∀ (a : Iota), % 11.74/11.92 Or (Eq True False) % 11.74/11.92 (Or (Eq (admin_indi_has_compartments admin a (cons compartmentb (cons compartmenta nil))) False) % 11.74/11.92 (Eq (admin_indi_has_compartments_for_file admin a secretfile) True)) % 11.74/11.92 Clause #667 (by clausification #[666]): ∀ (a : Iota), % 11.74/11.92 Or (Eq (admin_indi_has_compartments admin a (cons compartmentb (cons compartmenta nil))) False) % 11.74/11.92 (Eq (admin_indi_has_compartments_for_file admin a secretfile) True) % 11.74/11.92 Clause #691 (by clausification #[527]): ∀ (a a_1 : Iota), % 11.74/11.92 Or (Eq (system_indi_is_level_admin system a) False) % 11.74/11.92 (Or (Eq (level_admin_indi_has_level a alice a_1) False) % 11.74/11.92 (Or (Eq (loca_level_below admin confidential a_1) False) % 11.74/11.92 (Or (Eq (admin_indi_has_background admin alice confidential) False) % 11.74/11.92 (Eq (admin_indi_has_level admin alice confidential) True)))) % 11.74/11.92 Clause #692 (by forward demodulation #[691, 426]): ∀ (a a_1 : Iota), % 11.74/11.92 Or (Eq (system_indi_is_level_admin system a) False) % 11.74/11.92 (Or (Eq (level_admin_indi_has_level a alice a_1) False) % 11.74/11.92 (Or (Eq (loca_level_below admin confidential a_1) False) % 11.74/11.92 (Or (Eq True False) (Eq (admin_indi_has_level admin alice confidential) True)))) % 11.74/11.92 Clause #693 (by clausification #[692]): ∀ (a a_1 : Iota), % 11.74/11.92 Or (Eq (system_indi_is_level_admin system a) False) % 11.74/11.92 (Or (Eq (level_admin_indi_has_level a alice a_1) False) % 11.74/11.92 (Or (Eq (loca_level_below admin confidential a_1) False) % 11.74/11.92 (Eq (admin_indi_has_level admin alice confidential) True))) % 11.74/11.92 Clause #694 (by superposition #[693, 70]): ∀ (a : Iota), % 11.74/11.92 Or (Eq (level_admin_indi_has_level level_admin alice a) False) % 11.74/11.92 (Or (Eq (loca_level_below admin confidential a) False) % 11.74/11.92 (Or (Eq (admin_indi_has_level admin alice confidential) True) (Eq False True))) % 11.74/11.92 Clause #710 (by clausification #[528]): ∀ (a a_1 : Iota), % 11.74/11.92 Or (Eq (system_indi_is_level_admin system a) False) % 11.74/11.92 (Or (Eq (level_admin_indi_has_level a alice a_1) False) % 11.74/11.92 (Or (Eq (loca_level_below admin sbu a_1) False) % 11.74/11.92 (Or (Eq (admin_indi_has_background admin alice sbu) False) (Eq (admin_indi_has_level admin alice sbu) True)))) % 11.74/11.92 Clause #711 (by forward demodulation #[710, 424]): ∀ (a a_1 : Iota), % 11.74/11.92 Or (Eq (system_indi_is_level_admin system a) False) % 11.74/11.92 (Or (Eq (level_admin_indi_has_level a alice a_1) False) % 11.74/11.92 (Or (Eq (loca_level_below admin sbu a_1) False) % 11.74/11.92 (Or (Eq True False) (Eq (admin_indi_has_level admin alice sbu) True)))) % 11.74/11.92 Clause #712 (by clausification #[711]): ∀ (a a_1 : Iota), % 11.74/11.92 Or (Eq (system_indi_is_level_admin system a) False) % 11.74/11.92 (Or (Eq (level_admin_indi_has_level a alice a_1) False) % 11.74/11.92 (Or (Eq (loca_level_below admin sbu a_1) False) (Eq (admin_indi_has_level admin alice sbu) True))) % 11.74/11.92 Clause #713 (by superposition #[712, 70]): ∀ (a : Iota), % 11.74/11.92 Or (Eq (level_admin_indi_has_level level_admin alice a) False) % 11.74/11.92 (Or (Eq (loca_level_below admin sbu a) False) (Or (Eq (admin_indi_has_level admin alice sbu) True) (Eq False True))) % 11.74/11.92 Clause #748 (by clausification #[530]): ∀ (a a_1 : Iota), % 11.74/11.92 Or (Eq (system_indi_is_level_admin system a) False) % 11.74/11.92 (Or (Eq (level_admin_indi_has_level a alice a_1) False) % 11.74/11.92 (Or (Eq (loca_level_below admin secret a_1) False) % 11.74/11.92 (Or (Eq (admin_indi_has_background admin alice secret) False) % 11.74/11.92 (Eq (admin_indi_has_level admin alice secret) True)))) % 11.74/11.92 Clause #749 (by forward demodulation #[748, 425]): ∀ (a a_1 : Iota), % 11.74/11.92 Or (Eq (system_indi_is_level_admin system a) False) % 11.74/11.92 (Or (Eq (level_admin_indi_has_level a alice a_1) False) % 11.74/11.92 (Or (Eq (loca_level_below admin secret a_1) False) % 11.74/11.92 (Or (Eq True False) (Eq (admin_indi_has_level admin alice secret) True)))) % 11.74/11.92 Clause #750 (by clausification #[749]): ∀ (a a_1 : Iota), % 11.74/11.92 Or (Eq (system_indi_is_level_admin system a) False) % 11.74/11.92 (Or (Eq (level_admin_indi_has_level a alice a_1) False) % 11.74/11.92 (Or (Eq (loca_level_below admin secret a_1) False) (Eq (admin_indi_has_level admin alice secret) True))) % 11.74/11.93 Clause #751 (by superposition #[750, 70]): ∀ (a : Iota), % 11.74/11.93 Or (Eq (level_admin_indi_has_level level_admin alice a) False) % 11.74/11.93 (Or (Eq (loca_level_below admin secret a) False) % 11.74/11.93 (Or (Eq (admin_indi_has_level admin alice secret) True) (Eq False True))) % 11.74/11.93 Clause #767 (by clausification #[552]): ∀ (a : Iota), % 11.74/11.93 Or (Eq (sso_indi_has_compartment sso_compartmenta alice compartmenta) False) % 11.74/11.93 (Or (Eq (admin_indi_has_level_for_compartment admin alice compartmenta) False) % 11.74/11.93 (Or (Eq (admin_indi_has_compartments admin alice a) False) % 11.74/11.93 (Eq (admin_indi_has_compartments admin alice (cons compartmenta a)) True))) % 11.74/11.93 Clause #768 (by forward demodulation #[767, 81]): ∀ (a : Iota), % 11.74/11.93 Or (Eq True False) % 11.74/11.93 (Or (Eq (admin_indi_has_level_for_compartment admin alice compartmenta) False) % 11.74/11.93 (Or (Eq (admin_indi_has_compartments admin alice a) False) % 11.74/11.93 (Eq (admin_indi_has_compartments admin alice (cons compartmenta a)) True))) % 11.74/11.93 Clause #769 (by clausification #[768]): ∀ (a : Iota), % 11.74/11.93 Or (Eq (admin_indi_has_level_for_compartment admin alice compartmenta) False) % 11.74/11.93 (Or (Eq (admin_indi_has_compartments admin alice a) False) % 11.74/11.93 (Eq (admin_indi_has_compartments admin alice (cons compartmenta a)) True)) % 11.74/11.93 Clause #812 (by clausification #[694]): ∀ (a : Iota), % 11.74/11.93 Or (Eq (level_admin_indi_has_level level_admin alice a) False) % 11.74/11.93 (Or (Eq (loca_level_below admin confidential a) False) (Eq (admin_indi_has_level admin alice confidential) True)) % 11.74/11.93 Clause #813 (by superposition #[812, 77]): Or (Eq (loca_level_below admin confidential topsecret) False) % 11.74/11.93 (Or (Eq (admin_indi_has_level admin alice confidential) True) (Eq False True)) % 11.74/11.93 Clause #814 (by clausification #[813]): Or (Eq (loca_level_below admin confidential topsecret) False) (Eq (admin_indi_has_level admin alice confidential) True) % 11.74/11.93 Clause #815 (by forward demodulation #[814, 270]): Or (Eq True False) (Eq (admin_indi_has_level admin alice confidential) True) % 11.74/11.93 Clause #816 (by clausification #[815]): Eq (admin_indi_has_level admin alice confidential) True % 11.74/11.93 Clause #819 (by superposition #[816, 479]): Or (Eq True False) (Eq (admin_indi_has_level_for_compartment admin alice compartmentb) True) % 11.74/11.93 Clause #820 (by clausification #[819]): Eq (admin_indi_has_level_for_compartment admin alice compartmentb) True % 11.74/11.93 Clause #835 (by clausification #[664]): Or (Eq (admin_file_has_level_h admin secretfile secret (cons compartmentb (cons compartmenta nil))) False) % 11.74/11.93 (Eq (admin_file_has_level admin secretfile secret) True) % 11.74/11.93 Clause #836 (by superposition #[835, 583]): Or (Eq (admin_file_has_level admin secretfile secret) True) (Eq False True) % 11.74/11.93 Clause #837 (by clausification #[836]): Eq (admin_file_has_level admin secretfile secret) True % 11.74/11.93 Clause #840 (by superposition #[837, 204]): ∀ (a : Iota), % 11.74/11.93 Or (Eq True False) % 11.74/11.93 (Or (Eq (admin_indi_has_level admin a secret) False) (Eq (admin_indi_has_level_for_file admin a secretfile) True)) % 11.74/11.93 Clause #841 (by clausification #[840]): ∀ (a : Iota), % 11.74/11.93 Or (Eq (admin_indi_has_level admin a secret) False) (Eq (admin_indi_has_level_for_file admin a secretfile) True) % 11.74/11.93 Clause #845 (by clausification #[751]): ∀ (a : Iota), % 11.74/11.93 Or (Eq (level_admin_indi_has_level level_admin alice a) False) % 11.74/11.93 (Or (Eq (loca_level_below admin secret a) False) (Eq (admin_indi_has_level admin alice secret) True)) % 11.74/11.93 Clause #846 (by superposition #[845, 77]): Or (Eq (loca_level_below admin secret topsecret) False) % 11.74/11.93 (Or (Eq (admin_indi_has_level admin alice secret) True) (Eq False True)) % 11.74/11.93 Clause #847 (by clausification #[846]): Or (Eq (loca_level_below admin secret topsecret) False) (Eq (admin_indi_has_level admin alice secret) True) % 11.74/11.93 Clause #848 (by forward demodulation #[847, 257]): Or (Eq True False) (Eq (admin_indi_has_level admin alice secret) True) % 11.74/11.93 Clause #849 (by clausification #[848]): Eq (admin_indi_has_level admin alice secret) True % 11.74/11.93 Clause #852 (by superposition #[849, 841]): Or (Eq True False) (Eq (admin_indi_has_level_for_file admin alice secretfile) True) % 11.74/11.93 Clause #853 (by clausification #[852]): Eq (admin_indi_has_level_for_file admin alice secretfile) True % 11.74/11.95 Clause #857 (by clausification #[713]): ∀ (a : Iota), % 11.74/11.95 Or (Eq (level_admin_indi_has_level level_admin alice a) False) % 11.74/11.95 (Or (Eq (loca_level_below admin sbu a) False) (Eq (admin_indi_has_level admin alice sbu) True)) % 11.74/11.95 Clause #858 (by superposition #[857, 77]): Or (Eq (loca_level_below admin sbu topsecret) False) % 11.74/11.95 (Or (Eq (admin_indi_has_level admin alice sbu) True) (Eq False True)) % 11.74/11.95 Clause #859 (by clausification #[858]): Or (Eq (loca_level_below admin sbu topsecret) False) (Eq (admin_indi_has_level admin alice sbu) True) % 11.74/11.95 Clause #860 (by forward demodulation #[859, 278]): Or (Eq True False) (Eq (admin_indi_has_level admin alice sbu) True) % 11.74/11.95 Clause #861 (by clausification #[860]): Eq (admin_indi_has_level admin alice sbu) True % 11.74/11.95 Clause #864 (by superposition #[861, 480]): Or (Eq True False) (Eq (admin_indi_has_level_for_compartment admin alice compartmenta) True) % 11.74/11.95 Clause #865 (by clausification #[864]): Eq (admin_indi_has_level_for_compartment admin alice compartmenta) True % 11.74/11.95 Clause #866 (by backward demodulation #[865, 769]): ∀ (a : Iota), % 11.74/11.95 Or (Eq True False) % 11.74/11.95 (Or (Eq (admin_indi_has_compartments admin alice a) False) % 11.74/11.95 (Eq (admin_indi_has_compartments admin alice (cons compartmenta a)) True)) % 11.74/11.95 Clause #867 (by clausification #[582]): ∀ (a : Iota), % 11.74/11.95 Or (Eq (sso_indi_has_compartment sso_compartmentb alice compartmentb) False) % 11.74/11.95 (Or (Eq (admin_indi_has_level_for_compartment admin alice compartmentb) False) % 11.74/11.95 (Or (Eq (admin_indi_has_compartments admin alice a) False) % 11.74/11.95 (Eq (admin_indi_has_compartments admin alice (cons compartmentb a)) True))) % 11.74/11.95 Clause #868 (by forward demodulation #[867, 80]): ∀ (a : Iota), % 11.74/11.95 Or (Eq True False) % 11.74/11.95 (Or (Eq (admin_indi_has_level_for_compartment admin alice compartmentb) False) % 11.74/11.95 (Or (Eq (admin_indi_has_compartments admin alice a) False) % 11.74/11.95 (Eq (admin_indi_has_compartments admin alice (cons compartmentb a)) True))) % 11.74/11.95 Clause #869 (by clausification #[868]): ∀ (a : Iota), % 11.74/11.95 Or (Eq (admin_indi_has_level_for_compartment admin alice compartmentb) False) % 11.74/11.95 (Or (Eq (admin_indi_has_compartments admin alice a) False) % 11.74/11.95 (Eq (admin_indi_has_compartments admin alice (cons compartmentb a)) True)) % 11.74/11.95 Clause #870 (by forward demodulation #[869, 820]): ∀ (a : Iota), % 11.74/11.95 Or (Eq True False) % 11.74/11.95 (Or (Eq (admin_indi_has_compartments admin alice a) False) % 11.74/11.95 (Eq (admin_indi_has_compartments admin alice (cons compartmentb a)) True)) % 11.74/11.95 Clause #871 (by clausification #[870]): ∀ (a : Iota), % 11.74/11.95 Or (Eq (admin_indi_has_compartments admin alice a) False) % 11.74/11.95 (Eq (admin_indi_has_compartments admin alice (cons compartmentb a)) True) % 11.74/11.95 Clause #879 (by clausification #[866]): ∀ (a : Iota), % 11.74/11.95 Or (Eq (admin_indi_has_compartments admin alice a) False) % 11.74/11.95 (Eq (admin_indi_has_compartments admin alice (cons compartmenta a)) True) % 11.74/11.95 Clause #883 (by superposition #[879, 118]): Or (Eq (admin_indi_has_compartments admin alice (cons compartmenta nil)) True) (Eq False True) % 11.74/11.95 Clause #884 (by clausification #[620]): Or (Eq (admin_indi_has_need_to_know_for_file admin alice secretfile) False) % 11.74/11.95 (Or (Eq (admin_indi_has_level_for_file admin alice secretfile) False) % 11.74/11.95 (Or (Eq (admin_indi_has_compartments_for_file admin alice secretfile) False) % 11.74/11.95 (Eq (admin_indi_may_file admin alice secretfile read) True))) % 11.74/11.95 Clause #885 (by forward demodulation #[884, 321]): Or (Eq True False) % 11.74/11.95 (Or (Eq (admin_indi_has_level_for_file admin alice secretfile) False) % 11.74/11.95 (Or (Eq (admin_indi_has_compartments_for_file admin alice secretfile) False) % 11.74/11.95 (Eq (admin_indi_may_file admin alice secretfile read) True))) % 11.74/11.95 Clause #886 (by clausification #[885]): Or (Eq (admin_indi_has_level_for_file admin alice secretfile) False) % 11.74/11.95 (Or (Eq (admin_indi_has_compartments_for_file admin alice secretfile) False) % 11.74/11.95 (Eq (admin_indi_may_file admin alice secretfile read) True)) % 11.74/11.95 Clause #887 (by forward demodulation #[886, 853]): Or (Eq True False) % 11.74/11.95 (Or (Eq (admin_indi_has_compartments_for_file admin alice secretfile) False) % 11.74/11.95 (Eq (admin_indi_may_file admin alice secretfile read) True)) % 11.74/11.95 Clause #888 (by clausification #[887]): Or (Eq (admin_indi_has_compartments_for_file admin alice secretfile) False) % 11.74/11.95 (Eq (admin_indi_may_file admin alice secretfile read) True) % 11.74/11.95 Clause #889 (by clausification #[883]): Eq (admin_indi_has_compartments admin alice (cons compartmenta nil)) True % 11.74/11.95 Clause #890 (by superposition #[889, 871]): Or (Eq True False) (Eq (admin_indi_has_compartments admin alice (cons compartmentb (cons compartmenta nil))) True) % 11.74/11.95 Clause #892 (by clausification #[890]): Eq (admin_indi_has_compartments admin alice (cons compartmentb (cons compartmenta nil))) True % 11.74/11.95 Clause #893 (by superposition #[892, 667]): Or (Eq True False) (Eq (admin_indi_has_compartments_for_file admin alice secretfile) True) % 11.74/11.95 Clause #896 (by clausification #[893]): Eq (admin_indi_has_compartments_for_file admin alice secretfile) True % 11.74/11.95 Clause #897 (by backward demodulation #[896, 888]): Or (Eq True False) (Eq (admin_indi_may_file admin alice secretfile read) True) % 11.74/11.95 Clause #898 (by clausification #[897]): Eq (admin_indi_may_file admin alice secretfile read) True % 11.74/11.95 Clause #899 (by superposition #[898, 127]): Eq True False % 11.74/11.95 Clause #900 (by clausification #[899]): False % 11.74/11.95 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------