%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : SWV438+1 : TPTP v9.2.0. Released v4.0.0. % Transfm : none % Format : tptp:raw % Command : duper %s % Computer : n005.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:07 PM UTC 2025 % Result : Theorem 5.60s 5.79s % Output : Proof 5.69s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.12 % Problem : SWV438+1 : TPTP v9.2.0. Released v4.0.0. % 0.07/0.13 % Command : duper %s % 0.13/0.35 % Computer : n005.cluster.edu % 0.13/0.35 % Model : x86_64 x86_64 % 0.13/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.35 % Memory : 8042.1875MB % 0.13/0.35 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.35 % CPULimit : 300 % 0.13/0.35 % WCLimit : 300 % 0.13/0.35 % DateTime : Thu Oct 2 12:21:53 EDT 2025 % 0.13/0.35 % CPUTime : % 5.60/5.79 SZS status Theorem for theBenchmark.p % 5.60/5.79 SZS output start Proof for theBenchmark.p % 5.60/5.79 Clause #8 (by assumption #[]): Eq % 5.60/5.79 (∀ (F CL : Iota), % 5.60/5.79 system_file_needs_compartments system F CL → % 5.60/5.79 admin_file_has_compartments_h admin F CL CL → admin_file_has_compartments admin F CL) % 5.60/5.79 True % 5.60/5.79 Clause #9 (by assumption #[]): Eq (∀ (F CL : Iota), admin_file_has_compartments_h admin F CL nil) True % 5.60/5.79 Clause #11 (by assumption #[]): Eq % 5.60/5.79 (∀ (F L CL : Iota), % 5.60/5.79 system_file_needs_level system F L → % 5.60/5.79 admin_file_has_compartments admin F CL → admin_file_has_level_h admin F L CL → admin_file_has_level admin F L) % 5.60/5.79 True % 5.60/5.79 Clause #12 (by assumption #[]): Eq (∀ (F L : Iota), admin_file_has_level_h admin F L nil) True % 5.60/5.79 Clause #14 (by assumption #[]): Eq % 5.60/5.79 (∀ (F U CL : Iota), % 5.60/5.79 system_file_needs_citizenship system F U → % 5.60/5.79 admin_file_has_compartments admin F CL → % 5.60/5.79 admin_file_has_citizenship_h admin F U CL → admin_file_has_citizenship admin F U) % 5.60/5.79 True % 5.60/5.79 Clause #15 (by assumption #[]): Eq (∀ (F U : Iota), admin_file_has_citizenship_h admin F U nil) True % 5.60/5.79 Clause #22 (by assumption #[]): Eq (∀ (K : Iota), admin_indi_has_citizenship admin K anycountry) True % 5.60/5.79 Clause #24 (by assumption #[]): Eq (∀ (K : Iota), admin_indi_has_level admin K unclassified) True % 5.60/5.79 Clause #26 (by assumption #[]): Eq (∀ (K : Iota), admin_indi_has_compartments admin K nil) True % 5.60/5.79 Clause #34 (by assumption #[]): Eq % 5.60/5.79 (∀ (K F CL : Iota), % 5.60/5.79 admin_file_has_compartments admin F CL → % 5.60/5.79 admin_indi_has_compartments admin K CL → admin_indi_has_compartments_for_file admin K F) % 5.60/5.79 True % 5.60/5.79 Clause #35 (by assumption #[]): Eq % 5.60/5.79 (∀ (K F L : Iota), % 5.60/5.79 admin_file_has_level admin F L → admin_indi_has_level admin K L → admin_indi_has_level_for_file admin K F) % 5.60/5.79 True % 5.60/5.79 Clause #36 (by assumption #[]): Eq % 5.60/5.79 (∀ (K F OWR : Iota), % 5.60/5.79 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) % 5.60/5.79 True % 5.60/5.79 Clause #37 (by assumption #[]): Eq % 5.60/5.79 (∀ (K F L : Iota), % 5.60/5.79 admin_file_has_citizenship admin F L → % 5.60/5.79 admin_indi_has_citizenship admin K L → admin_indi_has_citizenship_for_file admin K F) % 5.60/5.79 True % 5.60/5.79 Clause #39 (by assumption #[]): Eq % 5.60/5.79 (∀ (K F : Iota), % 5.60/5.79 state_file_is_not_working_paper F → % 5.60/5.79 admin_indi_has_citizenship_for_file admin K F → % 5.60/5.79 admin_indi_has_need_to_know_for_file admin K F → % 5.60/5.79 admin_indi_has_level_for_file admin K F → % 5.60/5.79 admin_indi_has_compartments_for_file admin K F → admin_indi_may_file admin K F read) % 5.60/5.79 True % 5.60/5.79 Clause #61 (by assumption #[]): Eq (state_file_is_not_working_paper not_secretfile) True % 5.60/5.79 Clause #62 (by assumption #[]): Eq (system_file_needs_compartments system not_secretfile nil) True % 5.60/5.79 Clause #63 (by assumption #[]): Eq (system_file_needs_level system not_secretfile unclassified) True % 5.60/5.79 Clause #64 (by assumption #[]): Eq (system_file_needs_citizenship system not_secretfile anycountry) True % 5.60/5.79 Clause #65 (by assumption #[]): Eq (state_file_has_owner not_secretfile owner_not_secretfile) True % 5.60/5.79 Clause #85 (by assumption #[]): Eq (owner_indi_has_need_to_know owner_not_secretfile babu not_secretfile) True % 5.60/5.79 Clause #87 (by assumption #[]): Eq (Not (admin_indi_may_file admin babu not_secretfile read)) True % 5.60/5.79 Clause #118 (by clausification #[26]): ∀ (a : Iota), Eq (admin_indi_has_compartments admin a nil) True % 5.60/5.79 Clause #119 (by clausification #[24]): ∀ (a : Iota), Eq (admin_indi_has_level admin a unclassified) True % 5.60/5.79 Clause #120 (by clausification #[22]): ∀ (a : Iota), Eq (admin_indi_has_citizenship admin a anycountry) True % 5.60/5.79 Clause #122 (by clausification #[8]): ∀ (a : Iota), % 5.60/5.79 Eq % 5.60/5.79 (∀ (CL : Iota), % 5.60/5.79 system_file_needs_compartments system a CL → % 5.60/5.79 admin_file_has_compartments_h admin a CL CL → admin_file_has_compartments admin a CL) % 5.60/5.79 True % 5.60/5.79 Clause #123 (by clausification #[122]): ∀ (a a_1 : Iota), % 5.60/5.79 Eq % 5.60/5.79 (system_file_needs_compartments system a a_1 → % 5.60/5.79 admin_file_has_compartments_h admin a a_1 a_1 → admin_file_has_compartments admin a a_1) % 5.60/5.79 True % 5.60/5.79 Clause #124 (by clausification #[123]): ∀ (a a_1 : Iota), % 5.60/5.79 Or (Eq (system_file_needs_compartments system a a_1) False) % 5.60/5.81 (Eq (admin_file_has_compartments_h admin a a_1 a_1 → admin_file_has_compartments admin a a_1) True) % 5.60/5.81 Clause #125 (by clausification #[124]): ∀ (a a_1 : Iota), % 5.60/5.81 Or (Eq (system_file_needs_compartments system a a_1) False) % 5.60/5.81 (Or (Eq (admin_file_has_compartments_h admin a a_1 a_1) False) (Eq (admin_file_has_compartments admin a a_1) True)) % 5.60/5.81 Clause #126 (by superposition #[125, 62]): Or (Eq (admin_file_has_compartments_h admin not_secretfile nil nil) False) % 5.60/5.81 (Or (Eq (admin_file_has_compartments admin not_secretfile nil) True) (Eq False True)) % 5.60/5.81 Clause #127 (by clausification #[87]): Eq (admin_indi_may_file admin babu not_secretfile read) False % 5.60/5.81 Clause #140 (by clausification #[9]): ∀ (a : Iota), Eq (∀ (CL : Iota), admin_file_has_compartments_h admin a CL nil) True % 5.60/5.81 Clause #141 (by clausification #[140]): ∀ (a a_1 : Iota), Eq (admin_file_has_compartments_h admin a a_1 nil) True % 5.60/5.81 Clause #169 (by clausification #[15]): ∀ (a : Iota), Eq (∀ (U : Iota), admin_file_has_citizenship_h admin a U nil) True % 5.60/5.81 Clause #170 (by clausification #[169]): ∀ (a a_1 : Iota), Eq (admin_file_has_citizenship_h admin a a_1 nil) True % 5.60/5.81 Clause #171 (by clausification #[12]): ∀ (a : Iota), Eq (∀ (L : Iota), admin_file_has_level_h admin a L nil) True % 5.60/5.81 Clause #172 (by clausification #[171]): ∀ (a a_1 : Iota), Eq (admin_file_has_level_h admin a a_1 nil) True % 5.60/5.81 Clause #173 (by clausification #[11]): ∀ (a : Iota), % 5.60/5.81 Eq % 5.60/5.81 (∀ (L CL : Iota), % 5.60/5.81 system_file_needs_level system a L → % 5.60/5.81 admin_file_has_compartments admin a CL → admin_file_has_level_h admin a L CL → admin_file_has_level admin a L) % 5.60/5.81 True % 5.60/5.81 Clause #174 (by clausification #[173]): ∀ (a a_1 : Iota), % 5.60/5.81 Eq % 5.60/5.81 (∀ (CL : Iota), % 5.60/5.81 system_file_needs_level system a a_1 → % 5.60/5.81 admin_file_has_compartments admin a CL → % 5.60/5.81 admin_file_has_level_h admin a a_1 CL → admin_file_has_level admin a a_1) % 5.60/5.81 True % 5.60/5.81 Clause #175 (by clausification #[174]): ∀ (a a_1 a_2 : Iota), % 5.60/5.81 Eq % 5.60/5.81 (system_file_needs_level system a a_1 → % 5.60/5.81 admin_file_has_compartments admin a a_2 → % 5.60/5.81 admin_file_has_level_h admin a a_1 a_2 → admin_file_has_level admin a a_1) % 5.60/5.81 True % 5.60/5.81 Clause #176 (by clausification #[175]): ∀ (a a_1 a_2 : Iota), % 5.60/5.81 Or (Eq (system_file_needs_level system a a_1) False) % 5.60/5.81 (Eq % 5.60/5.81 (admin_file_has_compartments admin a a_2 → % 5.60/5.81 admin_file_has_level_h admin a a_1 a_2 → admin_file_has_level admin a a_1) % 5.60/5.81 True) % 5.60/5.81 Clause #177 (by clausification #[176]): ∀ (a a_1 a_2 : Iota), % 5.60/5.81 Or (Eq (system_file_needs_level system a a_1) False) % 5.60/5.81 (Or (Eq (admin_file_has_compartments admin a a_2) False) % 5.60/5.81 (Eq (admin_file_has_level_h admin a a_1 a_2 → admin_file_has_level admin a a_1) True)) % 5.60/5.81 Clause #178 (by clausification #[177]): ∀ (a a_1 a_2 : Iota), % 5.60/5.81 Or (Eq (system_file_needs_level system a a_1) False) % 5.60/5.81 (Or (Eq (admin_file_has_compartments admin a a_2) False) % 5.60/5.81 (Or (Eq (admin_file_has_level_h admin a a_1 a_2) False) (Eq (admin_file_has_level admin a a_1) True))) % 5.60/5.81 Clause #180 (by superposition #[178, 63]): ∀ (a : Iota), % 5.60/5.81 Or (Eq (admin_file_has_compartments admin not_secretfile a) False) % 5.60/5.81 (Or (Eq (admin_file_has_level_h admin not_secretfile unclassified a) False) % 5.60/5.81 (Or (Eq (admin_file_has_level admin not_secretfile unclassified) True) (Eq False True))) % 5.60/5.81 Clause #200 (by clausification #[35]): ∀ (a : Iota), % 5.60/5.81 Eq % 5.60/5.81 (∀ (F L : Iota), % 5.60/5.81 admin_file_has_level admin F L → admin_indi_has_level admin a L → admin_indi_has_level_for_file admin a F) % 5.60/5.81 True % 5.60/5.81 Clause #201 (by clausification #[200]): ∀ (a a_1 : Iota), % 5.60/5.81 Eq % 5.60/5.81 (∀ (L : Iota), % 5.60/5.81 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) % 5.60/5.81 True % 5.60/5.81 Clause #202 (by clausification #[201]): ∀ (a a_1 a_2 : Iota), % 5.60/5.81 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) % 5.60/5.81 True % 5.60/5.81 Clause #203 (by clausification #[202]): ∀ (a a_1 a_2 : Iota), % 5.60/5.81 Or (Eq (admin_file_has_level admin a a_1) False) % 5.60/5.82 (Eq (admin_indi_has_level admin a_2 a_1 → admin_indi_has_level_for_file admin a_2 a) True) % 5.60/5.82 Clause #204 (by clausification #[203]): ∀ (a a_1 a_2 : Iota), % 5.60/5.82 Or (Eq (admin_file_has_level admin a a_1) False) % 5.60/5.82 (Or (Eq (admin_indi_has_level admin a_2 a_1) False) (Eq (admin_indi_has_level_for_file admin a_2 a) True)) % 5.60/5.82 Clause #205 (by clausification #[34]): ∀ (a : Iota), % 5.60/5.82 Eq % 5.60/5.82 (∀ (F CL : Iota), % 5.60/5.82 admin_file_has_compartments admin F CL → % 5.60/5.82 admin_indi_has_compartments admin a CL → admin_indi_has_compartments_for_file admin a F) % 5.60/5.82 True % 5.60/5.82 Clause #206 (by clausification #[205]): ∀ (a a_1 : Iota), % 5.60/5.82 Eq % 5.60/5.82 (∀ (CL : Iota), % 5.60/5.82 admin_file_has_compartments admin a CL → % 5.60/5.82 admin_indi_has_compartments admin a_1 CL → admin_indi_has_compartments_for_file admin a_1 a) % 5.60/5.82 True % 5.60/5.82 Clause #207 (by clausification #[206]): ∀ (a a_1 a_2 : Iota), % 5.60/5.82 Eq % 5.60/5.82 (admin_file_has_compartments admin a a_1 → % 5.60/5.82 admin_indi_has_compartments admin a_2 a_1 → admin_indi_has_compartments_for_file admin a_2 a) % 5.60/5.82 True % 5.60/5.82 Clause #208 (by clausification #[207]): ∀ (a a_1 a_2 : Iota), % 5.60/5.82 Or (Eq (admin_file_has_compartments admin a a_1) False) % 5.60/5.82 (Eq (admin_indi_has_compartments admin a_2 a_1 → admin_indi_has_compartments_for_file admin a_2 a) True) % 5.60/5.82 Clause #209 (by clausification #[208]): ∀ (a a_1 a_2 : Iota), % 5.60/5.82 Or (Eq (admin_file_has_compartments admin a a_1) False) % 5.60/5.82 (Or (Eq (admin_indi_has_compartments admin a_2 a_1) False) % 5.60/5.82 (Eq (admin_indi_has_compartments_for_file admin a_2 a) True)) % 5.60/5.82 Clause #212 (by clausification #[14]): ∀ (a : Iota), % 5.60/5.82 Eq % 5.60/5.82 (∀ (U CL : Iota), % 5.60/5.82 system_file_needs_citizenship system a U → % 5.60/5.82 admin_file_has_compartments admin a CL → % 5.60/5.82 admin_file_has_citizenship_h admin a U CL → admin_file_has_citizenship admin a U) % 5.60/5.82 True % 5.60/5.82 Clause #213 (by clausification #[212]): ∀ (a a_1 : Iota), % 5.60/5.82 Eq % 5.60/5.82 (∀ (CL : Iota), % 5.60/5.82 system_file_needs_citizenship system a a_1 → % 5.60/5.82 admin_file_has_compartments admin a CL → % 5.60/5.82 admin_file_has_citizenship_h admin a a_1 CL → admin_file_has_citizenship admin a a_1) % 5.60/5.82 True % 5.60/5.82 Clause #214 (by clausification #[213]): ∀ (a a_1 a_2 : Iota), % 5.60/5.82 Eq % 5.60/5.82 (system_file_needs_citizenship system a a_1 → % 5.60/5.82 admin_file_has_compartments admin a a_2 → % 5.60/5.82 admin_file_has_citizenship_h admin a a_1 a_2 → admin_file_has_citizenship admin a a_1) % 5.60/5.82 True % 5.60/5.82 Clause #215 (by clausification #[214]): ∀ (a a_1 a_2 : Iota), % 5.60/5.82 Or (Eq (system_file_needs_citizenship system a a_1) False) % 5.60/5.82 (Eq % 5.60/5.82 (admin_file_has_compartments admin a a_2 → % 5.60/5.82 admin_file_has_citizenship_h admin a a_1 a_2 → admin_file_has_citizenship admin a a_1) % 5.60/5.82 True) % 5.60/5.82 Clause #216 (by clausification #[215]): ∀ (a a_1 a_2 : Iota), % 5.60/5.82 Or (Eq (system_file_needs_citizenship system a a_1) False) % 5.60/5.82 (Or (Eq (admin_file_has_compartments admin a a_2) False) % 5.60/5.82 (Eq (admin_file_has_citizenship_h admin a a_1 a_2 → admin_file_has_citizenship admin a a_1) True)) % 5.60/5.82 Clause #217 (by clausification #[216]): ∀ (a a_1 a_2 : Iota), % 5.60/5.82 Or (Eq (system_file_needs_citizenship system a a_1) False) % 5.60/5.82 (Or (Eq (admin_file_has_compartments admin a a_2) False) % 5.60/5.82 (Or (Eq (admin_file_has_citizenship_h admin a a_1 a_2) False) (Eq (admin_file_has_citizenship admin a a_1) True))) % 5.60/5.82 Clause #218 (by superposition #[217, 64]): ∀ (a : Iota), % 5.60/5.82 Or (Eq (admin_file_has_compartments admin not_secretfile a) False) % 5.60/5.82 (Or (Eq (admin_file_has_citizenship_h admin not_secretfile anycountry a) False) % 5.60/5.82 (Or (Eq (admin_file_has_citizenship admin not_secretfile anycountry) True) (Eq False True))) % 5.60/5.82 Clause #221 (by clausification #[37]): ∀ (a : Iota), % 5.60/5.82 Eq % 5.60/5.82 (∀ (F L : Iota), % 5.60/5.82 admin_file_has_citizenship admin F L → % 5.60/5.82 admin_indi_has_citizenship admin a L → admin_indi_has_citizenship_for_file admin a F) % 5.60/5.82 True % 5.60/5.82 Clause #222 (by clausification #[221]): ∀ (a a_1 : Iota), % 5.60/5.82 Eq % 5.60/5.82 (∀ (L : Iota), % 5.60/5.82 admin_file_has_citizenship admin a L → % 5.60/5.82 admin_indi_has_citizenship admin a_1 L → admin_indi_has_citizenship_for_file admin a_1 a) % 5.60/5.82 True % 5.60/5.82 Clause #223 (by clausification #[222]): ∀ (a a_1 a_2 : Iota), % 5.60/5.84 Eq % 5.60/5.84 (admin_file_has_citizenship admin a a_1 → % 5.60/5.84 admin_indi_has_citizenship admin a_2 a_1 → admin_indi_has_citizenship_for_file admin a_2 a) % 5.60/5.84 True % 5.60/5.84 Clause #224 (by clausification #[223]): ∀ (a a_1 a_2 : Iota), % 5.60/5.84 Or (Eq (admin_file_has_citizenship admin a a_1) False) % 5.60/5.84 (Eq (admin_indi_has_citizenship admin a_2 a_1 → admin_indi_has_citizenship_for_file admin a_2 a) True) % 5.60/5.84 Clause #225 (by clausification #[224]): ∀ (a a_1 a_2 : Iota), % 5.60/5.84 Or (Eq (admin_file_has_citizenship admin a a_1) False) % 5.60/5.84 (Or (Eq (admin_indi_has_citizenship admin a_2 a_1) False) % 5.60/5.84 (Eq (admin_indi_has_citizenship_for_file admin a_2 a) True)) % 5.60/5.84 Clause #226 (by clausification #[36]): ∀ (a : Iota), % 5.60/5.84 Eq % 5.60/5.84 (∀ (F OWR : Iota), % 5.60/5.84 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) % 5.60/5.84 True % 5.60/5.84 Clause #227 (by clausification #[226]): ∀ (a a_1 : Iota), % 5.60/5.84 Eq % 5.60/5.84 (∀ (OWR : Iota), % 5.60/5.84 state_file_has_owner a OWR → % 5.60/5.84 owner_indi_has_need_to_know OWR a_1 a → admin_indi_has_need_to_know_for_file admin a_1 a) % 5.60/5.84 True % 5.60/5.84 Clause #228 (by clausification #[227]): ∀ (a a_1 a_2 : Iota), % 5.60/5.84 Eq % 5.60/5.84 (state_file_has_owner a a_1 → % 5.60/5.84 owner_indi_has_need_to_know a_1 a_2 a → admin_indi_has_need_to_know_for_file admin a_2 a) % 5.60/5.84 True % 5.60/5.84 Clause #229 (by clausification #[228]): ∀ (a a_1 a_2 : Iota), % 5.60/5.84 Or (Eq (state_file_has_owner a a_1) False) % 5.60/5.84 (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) % 5.60/5.84 Clause #230 (by clausification #[229]): ∀ (a a_1 a_2 : Iota), % 5.60/5.84 Or (Eq (state_file_has_owner a a_1) False) % 5.60/5.84 (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)) % 5.60/5.84 Clause #232 (by superposition #[230, 65]): ∀ (a : Iota), % 5.60/5.84 Or (Eq (owner_indi_has_need_to_know owner_not_secretfile a not_secretfile) False) % 5.60/5.84 (Or (Eq (admin_indi_has_need_to_know_for_file admin a not_secretfile) True) (Eq False True)) % 5.60/5.84 Clause #300 (by clausification #[232]): ∀ (a : Iota), % 5.60/5.84 Or (Eq (owner_indi_has_need_to_know owner_not_secretfile a not_secretfile) False) % 5.60/5.84 (Eq (admin_indi_has_need_to_know_for_file admin a not_secretfile) True) % 5.60/5.84 Clause #301 (by superposition #[300, 85]): Or (Eq (admin_indi_has_need_to_know_for_file admin babu not_secretfile) True) (Eq False True) % 5.60/5.84 Clause #302 (by clausification #[301]): Eq (admin_indi_has_need_to_know_for_file admin babu not_secretfile) True % 5.60/5.84 Clause #355 (by clausification #[126]): Or (Eq (admin_file_has_compartments_h admin not_secretfile nil nil) False) % 5.60/5.84 (Eq (admin_file_has_compartments admin not_secretfile nil) True) % 5.60/5.84 Clause #356 (by superposition #[355, 141]): Or (Eq (admin_file_has_compartments admin not_secretfile nil) True) (Eq False True) % 5.60/5.84 Clause #357 (by clausification #[356]): Eq (admin_file_has_compartments admin not_secretfile nil) True % 5.60/5.84 Clause #359 (by superposition #[357, 209]): ∀ (a : Iota), % 5.60/5.84 Or (Eq True False) % 5.60/5.84 (Or (Eq (admin_indi_has_compartments admin a nil) False) % 5.60/5.84 (Eq (admin_indi_has_compartments_for_file admin a not_secretfile) True)) % 5.60/5.84 Clause #371 (by clausification #[359]): ∀ (a : Iota), % 5.60/5.84 Or (Eq (admin_indi_has_compartments admin a nil) False) % 5.60/5.84 (Eq (admin_indi_has_compartments_for_file admin a not_secretfile) True) % 5.60/5.84 Clause #372 (by forward demodulation #[371, 118]): ∀ (a : Iota), Or (Eq True False) (Eq (admin_indi_has_compartments_for_file admin a not_secretfile) True) % 5.60/5.84 Clause #373 (by clausification #[372]): ∀ (a : Iota), Eq (admin_indi_has_compartments_for_file admin a not_secretfile) True % 5.60/5.84 Clause #374 (by clausification #[39]): ∀ (a : Iota), % 5.60/5.84 Eq % 5.60/5.84 (∀ (F : Iota), % 5.60/5.84 state_file_is_not_working_paper F → % 5.60/5.84 admin_indi_has_citizenship_for_file admin a F → % 5.60/5.84 admin_indi_has_need_to_know_for_file admin a F → % 5.60/5.84 admin_indi_has_level_for_file admin a F → % 5.60/5.84 admin_indi_has_compartments_for_file admin a F → admin_indi_may_file admin a F read) % 5.60/5.84 True % 5.60/5.84 Clause #375 (by clausification #[374]): ∀ (a a_1 : Iota), % 5.60/5.84 Eq % 5.60/5.84 (state_file_is_not_working_paper a → % 5.69/5.85 admin_indi_has_citizenship_for_file admin a_1 a → % 5.69/5.85 admin_indi_has_need_to_know_for_file admin a_1 a → % 5.69/5.85 admin_indi_has_level_for_file admin a_1 a → % 5.69/5.85 admin_indi_has_compartments_for_file admin a_1 a → admin_indi_may_file admin a_1 a read) % 5.69/5.85 True % 5.69/5.85 Clause #376 (by clausification #[375]): ∀ (a a_1 : Iota), % 5.69/5.85 Or (Eq (state_file_is_not_working_paper a) False) % 5.69/5.85 (Eq % 5.69/5.85 (admin_indi_has_citizenship_for_file admin a_1 a → % 5.69/5.85 admin_indi_has_need_to_know_for_file admin a_1 a → % 5.69/5.85 admin_indi_has_level_for_file admin a_1 a → % 5.69/5.85 admin_indi_has_compartments_for_file admin a_1 a → admin_indi_may_file admin a_1 a read) % 5.69/5.85 True) % 5.69/5.85 Clause #377 (by clausification #[376]): ∀ (a a_1 : Iota), % 5.69/5.85 Or (Eq (state_file_is_not_working_paper a) False) % 5.69/5.85 (Or (Eq (admin_indi_has_citizenship_for_file admin a_1 a) False) % 5.69/5.85 (Eq % 5.69/5.85 (admin_indi_has_need_to_know_for_file admin a_1 a → % 5.69/5.85 admin_indi_has_level_for_file admin a_1 a → % 5.69/5.85 admin_indi_has_compartments_for_file admin a_1 a → admin_indi_may_file admin a_1 a read) % 5.69/5.85 True)) % 5.69/5.85 Clause #378 (by clausification #[377]): ∀ (a a_1 : Iota), % 5.69/5.85 Or (Eq (state_file_is_not_working_paper a) False) % 5.69/5.85 (Or (Eq (admin_indi_has_citizenship_for_file admin a_1 a) False) % 5.69/5.85 (Or (Eq (admin_indi_has_need_to_know_for_file admin a_1 a) False) % 5.69/5.85 (Eq % 5.69/5.85 (admin_indi_has_level_for_file admin a_1 a → % 5.69/5.85 admin_indi_has_compartments_for_file admin a_1 a → admin_indi_may_file admin a_1 a read) % 5.69/5.85 True))) % 5.69/5.85 Clause #379 (by clausification #[378]): ∀ (a a_1 : Iota), % 5.69/5.85 Or (Eq (state_file_is_not_working_paper a) False) % 5.69/5.85 (Or (Eq (admin_indi_has_citizenship_for_file admin a_1 a) False) % 5.69/5.85 (Or (Eq (admin_indi_has_need_to_know_for_file admin a_1 a) False) % 5.69/5.85 (Or (Eq (admin_indi_has_level_for_file admin a_1 a) False) % 5.69/5.85 (Eq (admin_indi_has_compartments_for_file admin a_1 a → admin_indi_may_file admin a_1 a read) True)))) % 5.69/5.85 Clause #380 (by clausification #[379]): ∀ (a a_1 : Iota), % 5.69/5.85 Or (Eq (state_file_is_not_working_paper a) False) % 5.69/5.85 (Or (Eq (admin_indi_has_citizenship_for_file admin a_1 a) False) % 5.69/5.85 (Or (Eq (admin_indi_has_need_to_know_for_file admin a_1 a) False) % 5.69/5.85 (Or (Eq (admin_indi_has_level_for_file admin a_1 a) False) % 5.69/5.85 (Or (Eq (admin_indi_has_compartments_for_file admin a_1 a) False) % 5.69/5.85 (Eq (admin_indi_may_file admin a_1 a read) True))))) % 5.69/5.85 Clause #381 (by superposition #[380, 61]): ∀ (a : Iota), % 5.69/5.85 Or (Eq (admin_indi_has_citizenship_for_file admin a not_secretfile) False) % 5.69/5.85 (Or (Eq (admin_indi_has_need_to_know_for_file admin a not_secretfile) False) % 5.69/5.85 (Or (Eq (admin_indi_has_level_for_file admin a not_secretfile) False) % 5.69/5.85 (Or (Eq (admin_indi_has_compartments_for_file admin a not_secretfile) False) % 5.69/5.85 (Or (Eq (admin_indi_may_file admin a not_secretfile read) True) (Eq False True))))) % 5.69/5.85 Clause #439 (by clausification #[218]): ∀ (a : Iota), % 5.69/5.85 Or (Eq (admin_file_has_compartments admin not_secretfile a) False) % 5.69/5.85 (Or (Eq (admin_file_has_citizenship_h admin not_secretfile anycountry a) False) % 5.69/5.85 (Eq (admin_file_has_citizenship admin not_secretfile anycountry) True)) % 5.69/5.85 Clause #440 (by superposition #[439, 357]): Or (Eq (admin_file_has_citizenship_h admin not_secretfile anycountry nil) False) % 5.69/5.85 (Or (Eq (admin_file_has_citizenship admin not_secretfile anycountry) True) (Eq False True)) % 5.69/5.85 Clause #442 (by clausification #[440]): Or (Eq (admin_file_has_citizenship_h admin not_secretfile anycountry nil) False) % 5.69/5.85 (Eq (admin_file_has_citizenship admin not_secretfile anycountry) True) % 5.69/5.85 Clause #443 (by superposition #[442, 170]): Or (Eq (admin_file_has_citizenship admin not_secretfile anycountry) True) (Eq False True) % 5.69/5.85 Clause #444 (by clausification #[443]): Eq (admin_file_has_citizenship admin not_secretfile anycountry) True % 5.69/5.85 Clause #447 (by superposition #[444, 225]): ∀ (a : Iota), % 5.69/5.85 Or (Eq True False) % 5.69/5.85 (Or (Eq (admin_indi_has_citizenship admin a anycountry) False) % 5.69/5.85 (Eq (admin_indi_has_citizenship_for_file admin a not_secretfile) True)) % 5.69/5.87 Clause #448 (by clausification #[447]): ∀ (a : Iota), % 5.69/5.87 Or (Eq (admin_indi_has_citizenship admin a anycountry) False) % 5.69/5.87 (Eq (admin_indi_has_citizenship_for_file admin a not_secretfile) True) % 5.69/5.87 Clause #449 (by forward demodulation #[448, 120]): ∀ (a : Iota), Or (Eq True False) (Eq (admin_indi_has_citizenship_for_file admin a not_secretfile) True) % 5.69/5.87 Clause #450 (by clausification #[449]): ∀ (a : Iota), Eq (admin_indi_has_citizenship_for_file admin a not_secretfile) True % 5.69/5.87 Clause #451 (by clausification #[180]): ∀ (a : Iota), % 5.69/5.87 Or (Eq (admin_file_has_compartments admin not_secretfile a) False) % 5.69/5.87 (Or (Eq (admin_file_has_level_h admin not_secretfile unclassified a) False) % 5.69/5.87 (Eq (admin_file_has_level admin not_secretfile unclassified) True)) % 5.69/5.87 Clause #452 (by superposition #[451, 357]): Or (Eq (admin_file_has_level_h admin not_secretfile unclassified nil) False) % 5.69/5.87 (Or (Eq (admin_file_has_level admin not_secretfile unclassified) True) (Eq False True)) % 5.69/5.87 Clause #453 (by clausification #[452]): Or (Eq (admin_file_has_level_h admin not_secretfile unclassified nil) False) % 5.69/5.87 (Eq (admin_file_has_level admin not_secretfile unclassified) True) % 5.69/5.87 Clause #454 (by superposition #[453, 172]): Or (Eq (admin_file_has_level admin not_secretfile unclassified) True) (Eq False True) % 5.69/5.87 Clause #455 (by clausification #[454]): Eq (admin_file_has_level admin not_secretfile unclassified) True % 5.69/5.87 Clause #458 (by superposition #[455, 204]): ∀ (a : Iota), % 5.69/5.87 Or (Eq True False) % 5.69/5.87 (Or (Eq (admin_indi_has_level admin a unclassified) False) % 5.69/5.87 (Eq (admin_indi_has_level_for_file admin a not_secretfile) True)) % 5.69/5.87 Clause #459 (by clausification #[458]): ∀ (a : Iota), % 5.69/5.87 Or (Eq (admin_indi_has_level admin a unclassified) False) % 5.69/5.87 (Eq (admin_indi_has_level_for_file admin a not_secretfile) True) % 5.69/5.87 Clause #460 (by forward demodulation #[459, 119]): ∀ (a : Iota), Or (Eq True False) (Eq (admin_indi_has_level_for_file admin a not_secretfile) True) % 5.69/5.87 Clause #461 (by clausification #[460]): ∀ (a : Iota), Eq (admin_indi_has_level_for_file admin a not_secretfile) True % 5.69/5.87 Clause #598 (by clausification #[381]): ∀ (a : Iota), % 5.69/5.87 Or (Eq (admin_indi_has_citizenship_for_file admin a not_secretfile) False) % 5.69/5.87 (Or (Eq (admin_indi_has_need_to_know_for_file admin a not_secretfile) False) % 5.69/5.87 (Or (Eq (admin_indi_has_level_for_file admin a not_secretfile) False) % 5.69/5.87 (Or (Eq (admin_indi_has_compartments_for_file admin a not_secretfile) False) % 5.69/5.87 (Eq (admin_indi_may_file admin a not_secretfile read) True)))) % 5.69/5.87 Clause #599 (by forward demodulation #[598, 450]): ∀ (a : Iota), % 5.69/5.87 Or (Eq True False) % 5.69/5.87 (Or (Eq (admin_indi_has_need_to_know_for_file admin a not_secretfile) False) % 5.69/5.87 (Or (Eq (admin_indi_has_level_for_file admin a not_secretfile) False) % 5.69/5.87 (Or (Eq (admin_indi_has_compartments_for_file admin a not_secretfile) False) % 5.69/5.87 (Eq (admin_indi_may_file admin a not_secretfile read) True)))) % 5.69/5.87 Clause #600 (by clausification #[599]): ∀ (a : Iota), % 5.69/5.87 Or (Eq (admin_indi_has_need_to_know_for_file admin a not_secretfile) False) % 5.69/5.87 (Or (Eq (admin_indi_has_level_for_file admin a not_secretfile) False) % 5.69/5.87 (Or (Eq (admin_indi_has_compartments_for_file admin a not_secretfile) False) % 5.69/5.87 (Eq (admin_indi_may_file admin a not_secretfile read) True))) % 5.69/5.87 Clause #601 (by forward demodulation #[600, 461]): ∀ (a : Iota), % 5.69/5.87 Or (Eq (admin_indi_has_need_to_know_for_file admin a not_secretfile) False) % 5.69/5.87 (Or (Eq True False) % 5.69/5.87 (Or (Eq (admin_indi_has_compartments_for_file admin a not_secretfile) False) % 5.69/5.87 (Eq (admin_indi_may_file admin a not_secretfile read) True))) % 5.69/5.87 Clause #602 (by clausification #[601]): ∀ (a : Iota), % 5.69/5.87 Or (Eq (admin_indi_has_need_to_know_for_file admin a not_secretfile) False) % 5.69/5.87 (Or (Eq (admin_indi_has_compartments_for_file admin a not_secretfile) False) % 5.69/5.87 (Eq (admin_indi_may_file admin a not_secretfile read) True)) % 5.69/5.87 Clause #603 (by forward demodulation #[602, 373]): ∀ (a : Iota), % 5.69/5.87 Or (Eq (admin_indi_has_need_to_know_for_file admin a not_secretfile) False) % 5.69/5.87 (Or (Eq True False) (Eq (admin_indi_may_file admin a not_secretfile read) True)) % 5.69/5.87 Clause #604 (by clausification #[603]): ∀ (a : Iota), % 5.69/5.87 Or (Eq (admin_indi_has_need_to_know_for_file admin a not_secretfile) False) % 5.69/5.87 (Eq (admin_indi_may_file admin a not_secretfile read) True) % 5.69/5.87 Clause #605 (by superposition #[604, 302]): Or (Eq (admin_indi_may_file admin babu not_secretfile read) True) (Eq False True) % 5.69/5.87 Clause #606 (by clausification #[605]): Eq (admin_indi_may_file admin babu not_secretfile read) True % 5.69/5.87 Clause #607 (by superposition #[606, 127]): Eq True False % 5.69/5.87 Clause #608 (by clausification #[607]): False % 5.69/5.87 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------