%------------------------------------------------------------------------------ % File : Beagle---0.9.52 % Problem : SWV439+1 : TPTP v9.0.0. Released v4.0.0. % Transfm : none % Format : tptp:raw % Command : java -Dfile.encoding=UTF-8 -Xms512M -Xmx4G -Xss10M -jar /export/starexec/sandbox2/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox2/solver/bin/cvc4-1.4-x86_64-linux-opt -liasolver cooper -t %d %s % Computer : n028.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 : Wed Apr 9 09:30:35 PM UTC 2025 % Result : CounterSatisfiable 7.49s 2.74s % Output : Assurance 0s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.11/0.12 % Problem : SWV439+1 : TPTP v9.0.0. Released v4.0.0. % 0.11/0.13 % Command : java -Dfile.encoding=UTF-8 -Xms512M -Xmx4G -Xss10M -jar /export/starexec/sandbox2/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox2/solver/bin/cvc4-1.4-x86_64-linux-opt -liasolver cooper -t %d %s % 0.13/0.34 % Computer : n028.cluster.edu % 0.13/0.34 % Model : x86_64 x86_64 % 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.34 % Memory : 8042.1875MB % 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.34 % CPULimit : 300 % 0.13/0.34 % WCLimit : 300 % 0.13/0.34 % DateTime : Wed Apr 9 03:27:04 EDT 2025 % 0.13/0.34 % CPUTime : % 7.49/2.74 % 7.49/2.74 % SZS status CounterSatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p % 7.49/2.74 % 7.49/2.74 % SZS output start Saturation for /export/starexec/sandbox2/benchmark/theBenchmark.p % 7.49/2.75 %$ oca_compartment_is_compartment > sso_file_has_level > sso_file_has_citizenship > admin_indi_may_file > admin_file_has_level_h > admin_file_has_compartments_h > admin_file_has_citizenship_h > system_indi_needs_level > system_indi_needs_compartment > system_indi_is_counterintelligence > system_indi_has_citizenship > system_file_needs_level > system_file_needs_compartments > system_file_needs_citizenship > system_compartment_has_sso > sso_indi_has_compartment > sso_file_has_compartments > sso_compartment_has_scg > owner_indi_has_need_to_know > oca_compartment_has_scg > loca_level_direct_below > loca_level_below > level_admin_indi_has_level > background_admin_indi_has_background > admin_indi_has_polygraph_for_compartment > admin_indi_has_need_to_know_for_file > admin_indi_has_level_for_file > admin_indi_has_level_for_compartment > admin_indi_has_level > admin_indi_has_credit_for_compartment > admin_indi_has_compartments_for_file > admin_indi_has_compartments > admin_indi_has_citizenship_for_file > admin_indi_has_citizenship > admin_indi_has_background_for_compartment > admin_indi_has_background > admin_file_has_level > admin_file_has_compartments > admin_file_has_citizenship > admin_compartment_has_sso > admin_compartment_has_scg > system_indi_is_polygraph_admin > system_indi_is_oca > system_indi_is_level_admin > system_indi_is_hr_admin > system_indi_is_credit_admin > system_indi_is_background_admin > state_file_has_owner > polygraph_admin_indi_has_polygraph > hr_admin_indi_has_employment > credit_admin_indi_has_credit > admin_indi_has_polygraph > admin_indi_has_employment > admin_indi_has_credit > state_file_is_not_working_paper > cons > #nlpp > yes > usa > unclassified > topsecret > system > sso_compartmentb > sso_compartmenta > secretfile > secret > scg_compartmentb > scg_compartmenta > sbu > read > polygraph_admin > owner_secretfile > owner_not_secretfile > oca > not_secretfile > no > nil > level_admin > india > hr_admin > credit_admin > confidential > compartmentb > compartmenta > ci > background_admin > babu > anycountry > alice > admin % 7.49/2.75 % 7.49/2.75 %Foreground sorts: % 7.49/2.75 % 7.49/2.75 % 7.49/2.75 %Background operators: % 7.49/2.75 % 7.49/2.75 % 7.49/2.75 %Foreground operators: % 7.49/2.75 tff(secretfile, type, secretfile: $i). % 7.49/2.75 tff(admin_indi_has_employment, type, admin_indi_has_employment: ($i * $i) > $o). % 7.49/2.75 tff(admin_indi_may_file, type, admin_indi_may_file: ($i * $i * $i * $i) > $o). % 7.49/2.75 tff(system_file_needs_level, type, system_file_needs_level: ($i * $i * $i) > $o). % 7.49/2.75 tff(background_admin, type, background_admin: $i). % 7.49/2.75 tff(polygraph_admin_indi_has_polygraph, type, polygraph_admin_indi_has_polygraph: ($i * $i) > $o). % 7.49/2.75 tff(admin_indi_has_level_for_file, type, admin_indi_has_level_for_file: ($i * $i * $i) > $o). % 7.49/2.75 tff(admin_indi_has_citizenship, type, admin_indi_has_citizenship: ($i * $i * $i) > $o). % 7.49/2.75 tff(admin_indi_has_level_for_compartment, type, admin_indi_has_level_for_compartment: ($i * $i * $i) > $o). % 7.49/2.75 tff(system_file_needs_citizenship, type, system_file_needs_citizenship: ($i * $i * $i) > $o). % 7.49/2.75 tff(hr_admin, type, hr_admin: $i). % 7.49/2.75 tff(babu, type, babu: $i). % 7.49/2.75 tff(confidential, type, confidential: $i). % 7.49/2.75 tff(scg_compartmenta, type, scg_compartmenta: $i). % 7.49/2.75 tff(not_secretfile, type, not_secretfile: $i). % 7.49/2.75 tff(india, type, india: $i). % 7.49/2.75 tff(sso_compartmenta, type, sso_compartmenta: $i). % 7.49/2.75 tff(admin_indi_has_credit, type, admin_indi_has_credit: ($i * $i) > $o). % 7.49/2.75 tff(system_compartment_has_sso, type, system_compartment_has_sso: ($i * $i * $i) > $o). % 7.49/2.75 tff(topsecret, type, topsecret: $i). % 7.49/2.75 tff(owner_not_secretfile, type, owner_not_secretfile: $i). % 7.49/2.75 tff(admin_indi_has_citizenship_for_file, type, admin_indi_has_citizenship_for_file: ($i * $i * $i) > $o). % 7.49/2.75 tff(unclassified, type, unclassified: $i). % 7.49/2.75 tff(compartmenta, type, compartmenta: $i). % 7.49/2.75 tff(yes, type, yes: $i). % 7.49/2.75 tff(system_indi_is_level_admin, type, system_indi_is_level_admin: ($i * $i) > $o). % 7.49/2.75 tff(no, type, no: $i). % 7.49/2.75 tff(read, type, read: $i). % 7.49/2.75 tff(credit_admin, type, credit_admin: $i). % 7.49/2.75 tff(system_file_needs_compartments, type, system_file_needs_compartments: ($i * $i * $i) > $o). % 7.49/2.75 tff(admin_indi_has_compartments_for_file, type, admin_indi_has_compartments_for_file: ($i * $i * $i) > $o). % 7.49/2.75 tff(sbu, type, sbu: $i). % 7.49/2.75 tff(secret, type, secret: $i). % 7.49/2.75 tff(admin_compartment_has_scg, type, admin_compartment_has_scg: ($i * $i * $i) > $o). % 7.49/2.75 tff(usa, type, usa: $i). % 7.49/2.75 tff(background_admin_indi_has_background, type, background_admin_indi_has_background: ($i * $i * $i) > $o). % 7.49/2.75 tff(admin_file_has_level, type, admin_file_has_level: ($i * $i * $i) > $o). % 7.49/2.75 tff(system_indi_is_oca, type, system_indi_is_oca: ($i * $i) > $o). % 7.49/2.75 tff(system_indi_is_counterintelligence, type, system_indi_is_counterintelligence: ($i * $i * $i) > $o). % 7.49/2.75 tff(admin_indi_has_need_to_know_for_file, type, admin_indi_has_need_to_know_for_file: ($i * $i * $i) > $o). % 7.49/2.75 tff(system_indi_has_citizenship, type, system_indi_has_citizenship: ($i * $i * $i) > $o). % 7.49/2.75 tff(admin, type, admin: $i). % 7.49/2.75 tff(system_indi_needs_compartment, type, system_indi_needs_compartment: ($i * $i * $i) > $o). % 7.49/2.75 tff(sso_file_has_level, type, sso_file_has_level: ($i * $i * $i * $i) > $o). % 7.49/2.75 tff(system_indi_is_polygraph_admin, type, system_indi_is_polygraph_admin: ($i * $i) > $o). % 7.49/2.75 tff(sso_compartmentb, type, sso_compartmentb: $i). % 7.49/2.75 tff(scg_compartmentb, type, scg_compartmentb: $i). % 7.49/2.75 tff(compartmentb, type, compartmentb: $i). % 7.49/2.75 tff(sso_file_has_citizenship, type, sso_file_has_citizenship: ($i * $i * $i * $i) > $o). % 7.49/2.75 tff(sso_file_has_compartments, type, sso_file_has_compartments: ($i * $i * $i) > $o). % 7.49/2.75 tff(admin_indi_has_credit_for_compartment, type, admin_indi_has_credit_for_compartment: ($i * $i * $i) > $o). % 7.49/2.75 tff(admin_file_has_compartments, type, admin_file_has_compartments: ($i * $i * $i) > $o). % 7.49/2.75 tff(credit_admin_indi_has_credit, type, credit_admin_indi_has_credit: ($i * $i) > $o). % 7.49/2.75 tff(admin_indi_has_polygraph, type, admin_indi_has_polygraph: ($i * $i) > $o). % 7.49/2.75 tff(admin_file_has_citizenship, type, admin_file_has_citizenship: ($i * $i * $i) > $o). % 7.49/2.75 tff(oca, type, oca: $i). % 7.49/2.75 tff(state_file_has_owner, type, state_file_has_owner: ($i * $i) > $o). % 7.49/2.75 tff(anycountry, type, anycountry: $i). % 7.49/2.75 tff(system_indi_is_background_admin, type, system_indi_is_background_admin: ($i * $i) > $o). % 7.49/2.75 tff(admin_indi_has_background, type, admin_indi_has_background: ($i * $i * $i) > $o). % 7.49/2.75 tff(admin_file_has_citizenship_h, type, admin_file_has_citizenship_h: ($i * $i * $i * $i) > $o). % 7.49/2.75 tff(sso_compartment_has_scg, type, sso_compartment_has_scg: ($i * $i * $i) > $o). % 7.49/2.75 tff(admin_file_has_compartments_h, type, admin_file_has_compartments_h: ($i * $i * $i * $i) > $o). % 7.49/2.75 tff(admin_indi_has_compartments, type, admin_indi_has_compartments: ($i * $i * $i) > $o). % 7.49/2.75 tff(admin_file_has_level_h, type, admin_file_has_level_h: ($i * $i * $i * $i) > $o). % 7.49/2.75 tff(hr_admin_indi_has_employment, type, hr_admin_indi_has_employment: ($i * $i) > $o). % 7.49/2.75 tff(polygraph_admin, type, polygraph_admin: $i). % 7.49/2.75 tff(cons, type, cons: ($i * $i) > $i). % 7.49/2.75 tff(oca_compartment_has_scg, type, oca_compartment_has_scg: ($i * $i * $i) > $o). % 7.49/2.75 tff(system, type, system: $i). % 7.49/2.75 tff(loca_level_below, type, loca_level_below: ($i * $i * $i) > $o). % 7.49/2.75 tff(admin_indi_has_polygraph_for_compartment, type, admin_indi_has_polygraph_for_compartment: ($i * $i * $i) > $o). % 7.49/2.75 tff(state_file_is_not_working_paper, type, state_file_is_not_working_paper: $i > $o). % 7.49/2.75 tff(level_admin, type, level_admin: $i). % 7.49/2.75 tff(system_indi_is_hr_admin, type, system_indi_is_hr_admin: ($i * $i) > $o). % 7.49/2.75 tff(admin_compartment_has_sso, type, admin_compartment_has_sso: ($i * $i * $i) > $o). % 7.49/2.75 tff(system_indi_is_credit_admin, type, system_indi_is_credit_admin: ($i * $i) > $o). % 7.49/2.75 tff(system_indi_needs_level, type, system_indi_needs_level: ($i * $i * $i) > $o). % 7.49/2.75 tff(loca_level_direct_below, type, loca_level_direct_below: ($i * $i * $i) > $o). % 7.49/2.75 tff(oca_compartment_is_compartment, type, oca_compartment_is_compartment: ($i * $i * $i * $i * $i * $i) > $o). % 7.49/2.75 tff(admin_indi_has_background_for_compartment, type, admin_indi_has_background_for_compartment: ($i * $i * $i) > $o). % 7.49/2.75 tff(owner_secretfile, type, owner_secretfile: $i). % 7.49/2.75 tff(sso_indi_has_compartment, type, sso_indi_has_compartment: ($i * $i * $i) > $o). % 7.49/2.75 tff(nil, type, nil: $i). % 7.49/2.75 tff(level_admin_indi_has_level, type, level_admin_indi_has_level: ($i * $i * $i) > $o). % 7.49/2.75 tff(alice, type, alice: $i). % 7.49/2.75 tff(admin_indi_has_level, type, admin_indi_has_level: ($i * $i * $i) > $o). % 7.49/2.75 tff(ci, type, ci: $i). % 7.49/2.75 tff(owner_indi_has_need_to_know, type, owner_indi_has_need_to_know: ($i * $i * $i) > $o). % 7.49/2.75 % 7.49/2.75 %Saturated clause set: % 7.49/2.76 tff(c_1448, plain, (![C_81, B1_85, B2_86, L2_84, OCA_82]: (admin_indi_has_level_for_compartment(admin, alice, C_81) | ~oca_compartment_is_compartment(OCA_82, C_81, sbu, L2_84, B1_85, B2_86) | ~system_indi_is_oca(system, OCA_82)))). % 7.49/2.76 tff(c_1449, plain, (![F_115]: (admin_indi_has_level_for_file(admin, alice, F_115) | ~admin_file_has_level(admin, F_115, sbu)))). % 7.49/2.76 tff(c_1443, plain, (admin_indi_has_level(admin, alice, sbu))). % 7.49/2.76 tff(c_873, plain, (![K_397, LA_394, L1_393]: (admin_indi_has_level(admin, K_397, sbu) | ~admin_indi_has_background(admin, K_397, sbu) | ~level_admin_indi_has_level(LA_394, K_397, topsecret) | ~system_indi_is_level_admin(system, LA_394) | ~loca_level_below(admin, sbu, L1_393) | ~admin_indi_has_credit(admin, K_397) | ~admin_indi_has_employment(admin, K_397) | ~admin_indi_has_polygraph(admin, K_397) | ~admin_indi_has_citizenship(admin, K_397, usa) | ~system_indi_needs_level(system, K_397, L1_393)))). % 7.49/2.76 tff(c_1418, plain, (![C_81, B1_85, B2_86, L2_84, OCA_82]: (admin_indi_has_level_for_compartment(admin, alice, C_81) | ~oca_compartment_is_compartment(OCA_82, C_81, confidential, L2_84, B1_85, B2_86) | ~system_indi_is_oca(system, OCA_82)))). % 7.49/2.76 tff(c_1419, plain, (![F_115]: (admin_indi_has_level_for_file(admin, alice, F_115) | ~admin_file_has_level(admin, F_115, confidential)))). % 7.49/2.76 tff(c_1413, plain, (admin_indi_has_level(admin, alice, confidential))). % 7.49/2.76 tff(c_875, plain, (![K_397, LA_394, L1_393]: (admin_indi_has_level(admin, K_397, confidential) | ~admin_indi_has_background(admin, K_397, confidential) | ~level_admin_indi_has_level(LA_394, K_397, topsecret) | ~system_indi_is_level_admin(system, LA_394) | ~loca_level_below(admin, confidential, L1_393) | ~admin_indi_has_credit(admin, K_397) | ~admin_indi_has_employment(admin, K_397) | ~admin_indi_has_polygraph(admin, K_397) | ~admin_indi_has_citizenship(admin, K_397, usa) | ~system_indi_needs_level(system, K_397, L1_393)))). % 7.49/2.76 tff(c_874, plain, (![K_397, LA_394, L1_393]: (admin_indi_has_level(admin, K_397, sbu) | ~admin_indi_has_background(admin, K_397, sbu) | ~level_admin_indi_has_level(LA_394, K_397, secret) | ~system_indi_is_level_admin(system, LA_394) | ~loca_level_below(admin, sbu, L1_393) | ~admin_indi_has_credit(admin, K_397) | ~admin_indi_has_employment(admin, K_397) | ~admin_indi_has_polygraph(admin, K_397) | ~admin_indi_has_citizenship(admin, K_397, usa) | ~system_indi_needs_level(system, K_397, L1_393)))). % 7.49/2.76 tff(c_1393, plain, (![C_81, B1_85, B2_86, L2_84, OCA_82]: (admin_indi_has_level_for_compartment(admin, alice, C_81) | ~oca_compartment_is_compartment(OCA_82, C_81, secret, L2_84, B1_85, B2_86) | ~system_indi_is_oca(system, OCA_82)))). % 7.49/2.76 tff(c_1394, plain, (![F_115]: (admin_indi_has_level_for_file(admin, alice, F_115) | ~admin_file_has_level(admin, F_115, secret)))). % 7.49/2.76 tff(c_1387, plain, (admin_indi_has_level(admin, alice, secret))). % 7.49/2.76 tff(c_883, plain, (![K_397, LA_394, L1_393]: (admin_indi_has_level(admin, K_397, confidential) | ~admin_indi_has_background(admin, K_397, confidential) | ~level_admin_indi_has_level(LA_394, K_397, secret) | ~system_indi_is_level_admin(system, LA_394) | ~loca_level_below(admin, confidential, L1_393) | ~admin_indi_has_credit(admin, K_397) | ~admin_indi_has_employment(admin, K_397) | ~admin_indi_has_polygraph(admin, K_397) | ~admin_indi_has_citizenship(admin, K_397, usa) | ~system_indi_needs_level(system, K_397, L1_393)))). % 7.49/2.76 tff(c_884, plain, (![K_397, LA_394, L1_393]: (admin_indi_has_level(admin, K_397, secret) | ~admin_indi_has_background(admin, K_397, secret) | ~level_admin_indi_has_level(LA_394, K_397, topsecret) | ~system_indi_is_level_admin(system, LA_394) | ~loca_level_below(admin, secret, L1_393) | ~admin_indi_has_credit(admin, K_397) | ~admin_indi_has_employment(admin, K_397) | ~admin_indi_has_polygraph(admin, K_397) | ~admin_indi_has_citizenship(admin, K_397, usa) | ~system_indi_needs_level(system, K_397, L1_393)))). % 7.49/2.76 tff(c_882, plain, (![K_397, LA_394, L1_393]: (admin_indi_has_level(admin, K_397, sbu) | ~admin_indi_has_background(admin, K_397, sbu) | ~level_admin_indi_has_level(LA_394, K_397, confidential) | ~system_indi_is_level_admin(system, LA_394) | ~loca_level_below(admin, sbu, L1_393) | ~admin_indi_has_credit(admin, K_397) | ~admin_indi_has_employment(admin, K_397) | ~admin_indi_has_polygraph(admin, K_397) | ~admin_indi_has_citizenship(admin, K_397, usa) | ~system_indi_needs_level(system, K_397, L1_393)))). % 7.49/2.76 tff(c_1369, plain, (![F_112]: (admin_indi_has_compartments_for_file(admin, alice, F_112) | ~admin_file_has_compartments(admin, F_112, cons(compartmenta, nil))))). % 7.49/2.76 tff(c_1366, plain, (admin_indi_has_compartments(admin, alice, cons(compartmenta, nil)))). % 7.49/2.76 tff(c_1365, plain, (admin_indi_has_compartments_for_file(admin, alice, secretfile))). % 7.49/2.76 tff(c_1351, plain, (![F_112, CL_550]: (admin_indi_has_compartments_for_file(admin, alice, F_112) | ~admin_file_has_compartments(admin, F_112, cons(compartmentb, CL_550)) | ~admin_indi_has_compartments(admin, alice, CL_550)))). % 7.49/2.76 tff(c_1346, plain, (![CL_416]: (admin_indi_has_compartments(admin, alice, cons(compartmentb, CL_416)) | ~admin_indi_has_compartments(admin, alice, CL_416)))). % 7.49/2.76 tff(c_1347, plain, (admin_indi_has_credit_for_compartment(admin, alice, compartmentb))). % 7.49/2.76 tff(c_1331, plain, (~loca_level_below(admin, topsecret, secret))). % 7.49/2.76 tff(c_1326, plain, (![L1_545]: (~loca_level_below(admin, topsecret, L1_545) | ~system_indi_needs_level(system, alice, L1_545)))). % 7.49/2.76 tff(c_1319, plain, (admin_indi_has_level_for_compartment(admin, alice, compartmentb))). % 7.49/2.76 tff(c_885, plain, (![K_397, L_6, LA_394, L1_393]: (admin_indi_has_level(admin, K_397, L_6) | ~admin_indi_has_background(admin, K_397, L_6) | ~level_admin_indi_has_level(LA_394, K_397, L_6) | ~system_indi_is_level_admin(system, LA_394) | ~loca_level_below(admin, L_6, L1_393) | ~admin_indi_has_credit(admin, K_397) | ~admin_indi_has_employment(admin, K_397) | ~admin_indi_has_polygraph(admin, K_397) | ~admin_indi_has_citizenship(admin, K_397, usa) | ~system_indi_needs_level(system, K_397, L1_393)))). % 7.49/2.76 tff(c_1245, plain, (admin_indi_has_polygraph_for_compartment(admin, alice, compartmentb))). % 7.49/2.76 tff(c_1225, plain, (admin_file_has_compartments_h(admin, secretfile, cons(compartmentb, cons(compartmenta, nil)), cons(compartmenta, nil)))). % 7.49/2.76 tff(c_1224, plain, (admin_file_has_compartments(admin, secretfile, cons(compartmentb, cons(compartmenta, nil))))). % 7.49/2.76 tff(c_1208, plain, (![F_112, CL_501]: (admin_indi_has_compartments_for_file(admin, alice, F_112) | ~admin_file_has_compartments(admin, F_112, cons(compartmenta, CL_501)) | ~admin_indi_has_compartments(admin, alice, CL_501)))). % 7.49/2.76 tff(c_1203, plain, (![CL_416]: (admin_indi_has_compartments(admin, alice, cons(compartmenta, CL_416)) | ~admin_indi_has_compartments(admin, alice, CL_416)))). % 7.49/2.76 tff(c_1204, plain, (admin_indi_has_level_for_compartment(admin, alice, compartmenta))). % 7.49/2.76 tff(c_56, plain, (![K_69, C_70, CL_71, SSO_72]: (admin_indi_has_compartments(admin, K_69, cons(C_70, CL_71)) | ~admin_indi_has_compartments(admin, K_69, CL_71) | ~admin_indi_has_level_for_compartment(admin, K_69, C_70) | ~admin_indi_has_background_for_compartment(admin, K_69, C_70) | ~sso_indi_has_compartment(SSO_72, K_69, C_70) | ~admin_compartment_has_sso(admin, C_70, SSO_72) | ~admin_indi_has_credit_for_compartment(admin, K_69, C_70) | ~admin_indi_has_polygraph_for_compartment(admin, K_69, C_70) | ~admin_indi_has_citizenship(admin, K_69, usa) | ~admin_indi_has_employment(admin, K_69) | ~system_indi_needs_compartment(system, K_69, C_70)))). % 7.49/2.76 tff(c_574, plain, (![C1_311, CL1_314]: (admin_file_has_compartments_h(admin, secretfile, cons(compartmentb, cons(compartmenta, nil)), cons(C1_311, CL1_314)) | ~admin_file_has_compartments_h(admin, secretfile, cons(compartmentb, cons(compartmenta, nil)), CL1_314) | ~admin_compartment_has_sso(admin, C1_311, sso_compartmentb)))). % 7.49/2.76 tff(c_962, plain, (admin_file_has_citizenship(admin, secretfile, usa))). % 7.49/2.76 tff(c_832, plain, (![C_391, CL_392]: (~admin_file_has_compartments(admin, secretfile, cons(C_391, CL_392)) | ~admin_file_has_citizenship_h(admin, secretfile, usa, CL_392) | ~admin_compartment_has_scg(admin, C_391, scg_compartmenta) | ~admin_compartment_has_sso(admin, C_391, sso_compartmenta)))). % 7.49/2.76 tff(c_52, plain, (![L1_65, K_63, LA_66, L_64, L11_67]: (admin_indi_has_level(admin, K_63, L_64) | ~admin_indi_has_background(admin, K_63, L_64) | ~loca_level_below(admin, L_64, L11_67) | ~level_admin_indi_has_level(LA_66, K_63, L11_67) | ~system_indi_is_level_admin(system, LA_66) | ~loca_level_below(admin, L_64, L1_65) | ~admin_indi_has_credit(admin, K_63) | ~admin_indi_has_employment(admin, K_63) | ~admin_indi_has_polygraph(admin, K_63) | ~admin_indi_has_citizenship(admin, K_63, usa) | ~system_indi_needs_level(system, K_63, L1_65)))). % 7.49/2.76 tff(c_815, plain, (![C_388, CL_384]: (admin_file_has_citizenship_h(admin, secretfile, usa, cons(C_388, CL_384)) | ~admin_file_has_citizenship_h(admin, secretfile, usa, CL_384) | ~admin_compartment_has_scg(admin, C_388, scg_compartmenta) | ~admin_compartment_has_sso(admin, C_388, sso_compartmenta)))). % 7.49/2.77 tff(c_816, plain, (![C_388, CL_384]: (admin_file_has_citizenship_h(admin, secretfile, usa, cons(C_388, CL_384)) | ~admin_file_has_citizenship_h(admin, secretfile, usa, CL_384) | ~admin_compartment_has_scg(admin, C_388, scg_compartmentb) | ~admin_compartment_has_sso(admin, C_388, sso_compartmentb)))). % 7.49/2.77 tff(c_809, plain, (~admin_compartment_has_sso(admin, compartmentb, sso_compartmenta))). % 7.49/2.77 tff(c_34, plain, (![F_42, SCG_47, U_43, C_44, CL_45, SSO_46]: (admin_file_has_citizenship_h(admin, F_42, U_43, cons(C_44, CL_45)) | ~admin_file_has_citizenship_h(admin, F_42, U_43, CL_45) | ~sso_file_has_citizenship(SSO_46, F_42, U_43, SCG_47) | ~admin_compartment_has_scg(admin, C_44, SCG_47) | ~admin_compartment_has_sso(admin, C_44, SSO_46)))). % 7.49/2.77 tff(c_808, plain, (admin_file_has_level(admin, secretfile, secret))). % 7.49/2.77 tff(c_629, plain, (![C_343, CL_346]: (admin_file_has_level_h(admin, secretfile, secret, cons(C_343, CL_346)) | ~admin_file_has_level_h(admin, secretfile, secret, CL_346) | ~admin_compartment_has_scg(admin, C_343, scg_compartmenta) | ~admin_compartment_has_sso(admin, C_343, sso_compartmenta)))). % 7.49/2.77 tff(c_628, plain, (![C_343, CL_346]: (admin_file_has_level_h(admin, secretfile, secret, cons(C_343, CL_346)) | ~admin_file_has_level_h(admin, secretfile, secret, CL_346) | ~admin_compartment_has_scg(admin, C_343, scg_compartmentb) | ~admin_compartment_has_sso(admin, C_343, sso_compartmentb)))). % 7.49/2.77 tff(c_28, plain, (![CL_34, C_33, SCG_36, F_31, L_32, SSO_35]: (admin_file_has_level_h(admin, F_31, L_32, cons(C_33, CL_34)) | ~admin_file_has_level_h(admin, F_31, L_32, CL_34) | ~sso_file_has_level(SSO_35, F_31, L_32, SCG_36) | ~admin_compartment_has_scg(admin, C_33, SCG_36) | ~admin_compartment_has_sso(admin, C_33, SSO_35)))). % 7.49/2.77 tff(c_573, plain, (![C1_311, CL1_314]: (admin_file_has_compartments_h(admin, secretfile, cons(compartmentb, cons(compartmenta, nil)), cons(C1_311, CL1_314)) | ~admin_file_has_compartments_h(admin, secretfile, cons(compartmentb, cons(compartmenta, nil)), CL1_314) | ~admin_compartment_has_sso(admin, C1_311, sso_compartmenta)))). % 7.49/2.77 tff(c_612, plain, (~admin_file_has_citizenship(admin, secretfile, india))). % 7.49/2.77 tff(c_614, plain, (~admin_indi_has_citizenship(admin, babu, usa))). % 7.49/2.77 tff(c_613, plain, (~admin_file_has_citizenship(admin, secretfile, anycountry))). % 7.49/2.77 tff(c_602, plain, (~admin_indi_has_citizenship_for_file(admin, babu, secretfile))). % 7.49/2.77 tff(c_523, plain, (![B1_287, C_285, B2_290, L1_289, OCA_288]: (admin_indi_has_background_for_compartment(admin, alice, C_285) | ~oca_compartment_is_compartment(OCA_288, C_285, L1_289, sbu, B1_287, B2_290) | ~system_indi_is_oca(system, OCA_288)))). % 7.49/2.77 tff(c_524, plain, (![B1_287, C_285, B2_290, L1_289, OCA_288]: (admin_indi_has_background_for_compartment(admin, alice, C_285) | ~oca_compartment_is_compartment(OCA_288, C_285, L1_289, confidential, B1_287, B2_290) | ~system_indi_is_oca(system, OCA_288)))). % 7.49/2.77 tff(c_525, plain, (![B1_287, C_285, B2_290, L1_289, OCA_288]: (admin_indi_has_background_for_compartment(admin, alice, C_285) | ~oca_compartment_is_compartment(OCA_288, C_285, L1_289, secret, B1_287, B2_290) | ~system_indi_is_oca(system, OCA_288)))). % 7.49/2.77 tff(c_80, plain, (![K_125, F_126]: (admin_indi_may_file(admin, K_125, F_126, read) | ~admin_indi_has_compartments_for_file(admin, K_125, F_126) | ~admin_indi_has_level_for_file(admin, K_125, F_126) | ~admin_indi_has_need_to_know_for_file(admin, K_125, F_126) | ~admin_indi_has_citizenship_for_file(admin, K_125, F_126) | ~state_file_is_not_working_paper(F_126)))). % 7.49/2.77 tff(c_591, plain, (admin_indi_has_background_for_compartment(admin, alice, compartmentb))). % 7.49/2.77 tff(c_526, plain, (![B1_287, C_285, B2_290, L1_289, OCA_288]: (admin_indi_has_background_for_compartment(admin, alice, C_285) | ~oca_compartment_is_compartment(OCA_288, C_285, L1_289, topsecret, B1_287, B2_290) | ~system_indi_is_oca(system, OCA_288)))). % 7.49/2.77 tff(c_584, plain, (admin_compartment_has_scg(admin, compartmenta, scg_compartmenta))). % 7.49/2.77 tff(c_22, plain, (![C1_23, CL_22, CL1_24, SSO_25, F_21]: (admin_file_has_compartments_h(admin, F_21, CL_22, cons(C1_23, CL1_24)) | ~admin_file_has_compartments_h(admin, F_21, CL_22, CL1_24) | ~sso_file_has_compartments(SSO_25, F_21, CL_22) | ~admin_compartment_has_sso(admin, C1_23, SSO_25)))). % 7.49/2.77 tff(c_567, plain, (admin_compartment_has_scg(admin, compartmentb, scg_compartmentb))). % 7.49/2.77 tff(c_16, plain, (![C_14, SCG_16, SSO_15, OCA_13]: (admin_compartment_has_scg(admin, C_14, SCG_16) | ~sso_compartment_has_scg(SSO_15, C_14, SCG_16) | ~admin_compartment_has_sso(admin, C_14, SSO_15) | ~oca_compartment_has_scg(OCA_13, C_14, SCG_16) | ~system_indi_is_oca(system, OCA_13)))). % 7.49/2.77 tff(c_545, plain, (![K_303]: (admin_indi_has_background_for_compartment(admin, K_303, compartmenta)))). % 7.49/2.77 tff(c_527, plain, (![K_52, B1_287, C_285, B2_290, L1_289, OCA_288]: (admin_indi_has_background_for_compartment(admin, K_52, C_285) | ~oca_compartment_is_compartment(OCA_288, C_285, L1_289, unclassified, B1_287, B2_290) | ~system_indi_is_oca(system, OCA_288)))). % 7.49/2.77 tff(c_510, plain, (![B2_282, K_62, B1_278, OCA_279, L2_281, C_280]: (admin_indi_has_level_for_compartment(admin, K_62, C_280) | ~oca_compartment_is_compartment(OCA_279, C_280, unclassified, L2_281, B1_278, B2_282) | ~system_indi_is_oca(system, OCA_279)))). % 7.49/2.77 tff(c_537, plain, (admin_file_has_level(admin, not_secretfile, unclassified))). % 7.49/2.77 tff(c_452, plain, (![F_29, L_30]: (admin_file_has_level(admin, F_29, L_30) | ~admin_file_has_compartments(admin, F_29, nil) | ~system_file_needs_level(system, F_29, L_30)))). % 7.49/2.77 tff(c_58, plain, (![OCA_75, K_73, L1_76, B2_79, C_74, L2_77, B1_78]: (admin_indi_has_background_for_compartment(admin, K_73, C_74) | ~admin_indi_has_background(admin, K_73, L2_77) | ~oca_compartment_is_compartment(OCA_75, C_74, L1_76, L2_77, B1_78, B2_79) | ~system_indi_is_oca(system, OCA_75)))). % 7.49/2.77 tff(c_511, plain, (~admin_file_has_compartments(admin, secretfile, nil))). % 7.49/2.77 tff(c_505, plain, (admin_file_has_citizenship(admin, not_secretfile, anycountry))). % 7.49/2.77 tff(c_60, plain, (![C_81, B1_85, L1_83, B2_86, K_80, L2_84, OCA_82]: (admin_indi_has_level_for_compartment(admin, K_80, C_81) | ~admin_indi_has_level(admin, K_80, L1_83) | ~oca_compartment_is_compartment(OCA_82, C_81, L1_83, L2_84, B1_85, B2_86) | ~system_indi_is_oca(system, OCA_82)))). % 7.49/2.77 tff(c_473, plain, (![F_40, U_41]: (admin_file_has_citizenship(admin, F_40, U_41) | ~admin_file_has_compartments(admin, F_40, nil) | ~system_file_needs_citizenship(system, F_40, U_41)))). % 7.49/2.77 tff(c_495, plain, (admin_indi_has_background(admin, alice, sbu))). % 7.49/2.77 tff(c_399, plain, (![K_224, BA_227]: (admin_indi_has_background(admin, K_224, sbu) | ~background_admin_indi_has_background(BA_227, K_224, topsecret) | ~system_indi_is_background_admin(system, BA_227)))). % 7.49/2.77 tff(c_400, plain, (![K_224, BA_227]: (admin_indi_has_background(admin, K_224, sbu) | ~background_admin_indi_has_background(BA_227, K_224, secret) | ~system_indi_is_background_admin(system, BA_227)))). % 7.49/2.77 tff(c_486, plain, (![K_266]: (admin_indi_has_credit_for_compartment(admin, K_266, compartmentb) | ~admin_indi_has_credit(admin, K_266)))). % 7.49/2.77 tff(c_66, plain, (![OCA_101, L2_103, K_99, B2_104, C_100, L1_102]: (admin_indi_has_credit_for_compartment(admin, K_99, C_100) | ~admin_indi_has_credit(admin, K_99) | ~oca_compartment_is_compartment(OCA_101, C_100, L1_102, L2_103, yes, B2_104) | ~system_indi_is_oca(system, OCA_101)))). % 7.49/2.77 tff(c_480, plain, (admin_indi_has_background(admin, alice, confidential))). % 7.49/2.77 tff(c_401, plain, (![K_224, BA_227]: (admin_indi_has_background(admin, K_224, confidential) | ~background_admin_indi_has_background(BA_227, K_224, topsecret) | ~system_indi_is_background_admin(system, BA_227)))). % 7.49/2.77 tff(c_468, plain, (admin_indi_has_background(admin, alice, secret))). % 7.49/2.77 tff(c_30, plain, (![F_37, U_38, CL_39]: (admin_file_has_citizenship(admin, F_37, U_38) | ~admin_file_has_citizenship_h(admin, F_37, U_38, CL_39) | ~admin_file_has_compartments(admin, F_37, CL_39) | ~system_file_needs_citizenship(system, F_37, U_38)))). % 7.49/2.77 tff(c_408, plain, (![K_224, BA_227]: (admin_indi_has_background(admin, K_224, secret) | ~background_admin_indi_has_background(BA_227, K_224, topsecret) | ~system_indi_is_background_admin(system, BA_227)))). % 7.49/2.77 tff(c_407, plain, (![K_224, BA_227]: (admin_indi_has_background(admin, K_224, confidential) | ~background_admin_indi_has_background(BA_227, K_224, secret) | ~system_indi_is_background_admin(system, BA_227)))). % 7.49/2.77 tff(c_406, plain, (![K_224, BA_227]: (admin_indi_has_background(admin, K_224, sbu) | ~background_admin_indi_has_background(BA_227, K_224, confidential) | ~system_indi_is_background_admin(system, BA_227)))). % 7.49/2.77 tff(c_459, plain, (admin_indi_has_background(admin, alice, topsecret))). % 7.49/2.77 tff(c_409, plain, (![K_224, L_6, BA_227]: (admin_indi_has_background(admin, K_224, L_6) | ~background_admin_indi_has_background(BA_227, K_224, L_6) | ~system_indi_is_background_admin(system, BA_227)))). % 7.49/2.77 tff(c_24, plain, (![F_26, L_27, CL_28]: (admin_file_has_level(admin, F_26, L_27) | ~admin_file_has_level_h(admin, F_26, L_27, CL_28) | ~admin_file_has_compartments(admin, F_26, CL_28) | ~system_file_needs_level(system, F_26, L_27)))). % 7.49/2.77 tff(c_438, plain, (![K_235, L11_10]: (loca_level_below(K_235, unclassified, L11_10) | ~loca_level_direct_below(K_235, topsecret, L11_10)))). % 7.49/2.78 tff(c_370, plain, (![K_223, L11_10]: (loca_level_below(K_223, sbu, L11_10) | ~loca_level_direct_below(K_223, topsecret, L11_10)))). % 7.49/2.78 tff(c_444, plain, (![K_238]: (admin_indi_has_polygraph_for_compartment(admin, K_238, compartmentb) | ~admin_indi_has_polygraph(admin, K_238)))). % 7.49/2.78 tff(c_62, plain, (![K_87, B1_92, L1_90, L2_91, OCA_89, C_88]: (admin_indi_has_polygraph_for_compartment(admin, K_87, C_88) | ~admin_indi_has_polygraph(admin, K_87) | ~oca_compartment_is_compartment(OCA_89, C_88, L1_90, L2_91, B1_92, yes) | ~system_indi_is_oca(system, OCA_89)))). % 7.49/2.78 tff(c_429, plain, (![K_4]: (loca_level_below(K_4, unclassified, topsecret)))). % 7.49/2.78 tff(c_423, plain, (![K_230, L11_10]: (loca_level_below(K_230, unclassified, L11_10) | ~loca_level_direct_below(K_230, secret, L11_10)))). % 7.49/2.78 tff(c_344, plain, (![K_208, L11_10]: (loca_level_below(K_208, confidential, L11_10) | ~loca_level_direct_below(K_208, topsecret, L11_10)))). % 7.49/2.78 tff(c_414, plain, (![K_3]: (loca_level_below(K_3, unclassified, secret)))). % 7.49/2.78 tff(c_317, plain, (![K_195, L11_10]: (loca_level_below(K_195, unclassified, L11_10) | ~loca_level_direct_below(K_195, confidential, L11_10)))). % 7.49/2.78 tff(c_42, plain, (![K_53, L_54, L1_56, BA_55]: (admin_indi_has_background(admin, K_53, L_54) | ~loca_level_below(admin, L_54, L1_56) | ~background_admin_indi_has_background(BA_55, K_53, L1_56) | ~system_indi_is_background_admin(system, BA_55)))). % 7.49/2.78 tff(c_366, plain, (![K_4]: (loca_level_below(K_4, sbu, topsecret)))). % 7.49/2.78 tff(c_353, plain, (![K_211, L11_10]: (loca_level_below(K_211, sbu, L11_10) | ~loca_level_direct_below(K_211, secret, L11_10)))). % 7.49/2.78 tff(c_360, plain, (![K_217]: (admin_indi_has_credit_for_compartment(admin, K_217, compartmenta)))). % 7.49/2.78 tff(c_68, plain, (![K_105, L2_109, OCA_107, C_106, L1_108, B2_110]: (admin_indi_has_credit_for_compartment(admin, K_105, C_106) | ~oca_compartment_is_compartment(OCA_107, C_106, L1_108, L2_109, no, B2_110) | ~system_indi_is_oca(system, OCA_107)))). % 7.49/2.78 tff(c_291, plain, (![K_185, L11_10]: (loca_level_below(K_185, secret, L11_10) | ~loca_level_direct_below(K_185, topsecret, L11_10)))). % 7.49/2.78 tff(c_349, plain, (![K_3]: (loca_level_below(K_3, sbu, secret)))). % 7.49/2.78 tff(c_303, plain, (![K_190, L11_10]: (loca_level_below(K_190, sbu, L11_10) | ~loca_level_direct_below(K_190, confidential, L11_10)))). % 7.49/2.78 tff(c_333, plain, (![K_4]: (loca_level_below(K_4, confidential, topsecret)))). % 7.49/2.78 tff(c_339, plain, (![K_204]: (admin_indi_has_polygraph_for_compartment(admin, K_204, compartmenta)))). % 7.49/2.78 tff(c_64, plain, (![L1_96, L2_97, OCA_95, K_93, C_94, B1_98]: (admin_indi_has_polygraph_for_compartment(admin, K_93, C_94) | ~oca_compartment_is_compartment(OCA_95, C_94, L1_96, L2_97, B1_98, no) | ~system_indi_is_oca(system, OCA_95)))). % 7.49/2.78 tff(c_295, plain, (![K_186, L11_10]: (loca_level_below(K_186, confidential, L11_10) | ~loca_level_direct_below(K_186, secret, L11_10)))). % 7.49/2.78 tff(c_328, plain, (admin_file_has_compartments(admin, not_secretfile, nil))). % 7.49/2.78 tff(c_323, plain, (![F_19]: (admin_file_has_compartments(admin, F_19, nil) | ~system_file_needs_compartments(system, F_19, nil)))). % 7.49/2.78 tff(c_18, plain, (![F_17, CL_18]: (admin_file_has_compartments(admin, F_17, CL_18) | ~admin_file_has_compartments_h(admin, F_17, CL_18, CL_18) | ~system_file_needs_compartments(system, F_17, CL_18)))). % 7.49/2.78 tff(c_313, plain, (![K_2]: (loca_level_below(K_2, unclassified, confidential)))). % 7.49/2.78 tff(c_307, plain, (![K_191, L11_10]: (loca_level_below(K_191, unclassified, L11_10) | ~loca_level_direct_below(K_191, sbu, L11_10)))). % 7.49/2.78 tff(c_299, plain, (![F_188]: (admin_indi_may_file(admin, ci, F_188, read) | ~state_file_has_owner(F_188, owner_secretfile)))). % 7.49/2.78 tff(c_287, plain, (![K_1]: (loca_level_below(K_1, unclassified, sbu)))). % 7.49/2.78 tff(c_286, plain, (![K_2]: (loca_level_below(K_2, sbu, confidential)))). % 7.49/2.78 tff(c_82, plain, (![K_127, F_128, K1_129]: (admin_indi_may_file(admin, K_127, F_128, read) | ~system_indi_is_counterintelligence(system, K_127, K1_129) | ~state_file_has_owner(F_128, K1_129)))). % 7.49/2.78 tff(c_285, plain, (![K_3]: (loca_level_below(K_3, confidential, secret)))). % 7.49/2.78 tff(c_284, plain, (![K_4]: (loca_level_below(K_4, secret, topsecret)))). % 7.49/2.78 tff(c_270, plain, (![K_5, L_6, L11_180]: (loca_level_below(K_5, L_6, L11_180) | ~loca_level_direct_below(K_5, L_6, L11_180)))). % 7.49/2.78 tff(c_12, plain, (![K_7, L_8, L11_10, L1_9]: (loca_level_below(K_7, L_8, L11_10) | ~loca_level_below(K_7, L_8, L1_9) | ~loca_level_direct_below(K_7, L1_9, L11_10)))). % 7.49/2.78 tff(c_262, plain, (![F_172]: (admin_indi_has_citizenship_for_file(admin, alice, F_172) | ~admin_file_has_citizenship(admin, F_172, usa)))). % 7.49/2.78 tff(c_261, plain, (![F_172]: (admin_indi_has_citizenship_for_file(admin, babu, F_172) | ~admin_file_has_citizenship(admin, F_172, india)))). % 7.49/2.78 tff(c_263, plain, (![K_59, F_172]: (admin_indi_has_citizenship_for_file(admin, K_59, F_172) | ~admin_file_has_citizenship(admin, F_172, anycountry)))). % 7.49/2.78 tff(c_76, plain, (![K_120, F_121, L_122]: (admin_indi_has_citizenship_for_file(admin, K_120, F_121) | ~admin_indi_has_citizenship(admin, K_120, L_122) | ~admin_file_has_citizenship(admin, F_121, L_122)))). % 7.49/2.78 tff(c_252, plain, (![K_62, F_167]: (admin_indi_has_level_for_file(admin, K_62, F_167) | ~admin_file_has_level(admin, F_167, unclassified)))). % 7.49/2.78 tff(c_72, plain, (![K_114, F_115, L_116]: (admin_indi_has_level_for_file(admin, K_114, F_115) | ~admin_indi_has_level(admin, K_114, L_116) | ~admin_file_has_level(admin, F_115, L_116)))). % 7.49/2.78 tff(c_246, plain, (![K_68, F_162]: (admin_indi_has_compartments_for_file(admin, K_68, F_162) | ~admin_file_has_compartments(admin, F_162, nil)))). % 7.49/2.78 tff(c_247, plain, (~state_file_has_owner(not_secretfile, owner_secretfile))). % 7.49/2.78 tff(c_70, plain, (![K_111, F_112, CL_113]: (admin_indi_has_compartments_for_file(admin, K_111, F_112) | ~admin_indi_has_compartments(admin, K_111, CL_113) | ~admin_file_has_compartments(admin, F_112, CL_113)))). % 7.49/2.78 tff(c_241, plain, (admin_indi_has_need_to_know_for_file(admin, alice, secretfile))). % 7.49/2.78 tff(c_238, plain, (admin_indi_has_need_to_know_for_file(admin, babu, not_secretfile))). % 7.49/2.78 tff(c_74, plain, (![K_117, F_118, OWR_119]: (admin_indi_has_need_to_know_for_file(admin, K_117, F_118) | ~owner_indi_has_need_to_know(OWR_119, K_117, F_118) | ~state_file_has_owner(F_118, OWR_119)))). % 7.49/2.78 tff(c_225, plain, (admin_indi_has_polygraph(admin, alice))). % 7.49/2.78 tff(c_219, plain, (admin_indi_has_credit(admin, alice))). % 7.49/2.78 tff(c_36, plain, (![K_48, PA_49]: (admin_indi_has_polygraph(admin, K_48) | ~polygraph_admin_indi_has_polygraph(PA_49, K_48) | ~system_indi_is_polygraph_admin(system, PA_49)))). % 7.49/2.78 tff(c_38, plain, (![K_50, CA_51]: (admin_indi_has_credit(admin, K_50) | ~credit_admin_indi_has_credit(CA_51, K_50) | ~system_indi_is_credit_admin(system, CA_51)))). % 7.49/2.78 tff(c_213, plain, (admin_indi_has_employment(admin, alice))). % 7.49/2.78 tff(c_44, plain, (![K_57, HR_58]: (admin_indi_has_employment(admin, K_57) | ~hr_admin_indi_has_employment(HR_58, K_57) | ~system_indi_is_hr_admin(system, HR_58)))). % 7.49/2.78 tff(c_108, plain, (sso_file_has_compartments(sso_compartmenta, secretfile, cons(compartmentb, cons(compartmenta, nil))))). % 7.49/2.78 tff(c_78, plain, (![K_123, F_124]: (admin_indi_has_citizenship_for_file(admin, K_123, F_124) | ~admin_indi_has_citizenship(admin, K_123, usa)))). % 7.49/2.78 tff(c_205, plain, (admin_compartment_has_sso(admin, compartmentb, sso_compartmentb))). % 7.49/2.78 tff(c_197, plain, (admin_indi_has_citizenship(admin, babu, india))). % 7.49/2.78 tff(c_206, plain, (admin_compartment_has_sso(admin, compartmenta, sso_compartmenta))). % 7.49/2.78 tff(c_196, plain, (admin_indi_has_citizenship(admin, alice, usa))). % 7.49/2.78 tff(c_14, plain, (![C_11, SSO_12]: (admin_compartment_has_sso(admin, C_11, SSO_12) | ~system_compartment_has_sso(system, C_11, SSO_12)))). % 7.49/2.78 tff(c_48, plain, (![K_60, U_61]: (admin_indi_has_citizenship(admin, K_60, U_61) | ~system_indi_has_citizenship(system, K_60, U_61)))). % 7.49/2.78 tff(c_106, plain, (sso_file_has_compartments(sso_compartmentb, secretfile, cons(compartmentb, cons(compartmenta, nil))))). % 7.49/2.78 tff(c_104, plain, (system_file_needs_compartments(system, secretfile, cons(compartmentb, cons(compartmenta, nil))))). % 7.49/2.78 tff(c_86, plain, (oca_compartment_is_compartment(oca, compartmentb, confidential, topsecret, yes, yes))). % 7.49/2.78 tff(c_88, plain, (oca_compartment_is_compartment(oca, compartmenta, sbu, unclassified, no, no))). % 7.49/2.78 tff(c_32, plain, (![F_40, U_41]: (admin_file_has_citizenship_h(admin, F_40, U_41, nil)))). % 7.49/2.78 tff(c_112, plain, (sso_file_has_level(sso_compartmentb, secretfile, secret, scg_compartmentb))). % 7.49/2.78 tff(c_26, plain, (![F_29, L_30]: (admin_file_has_level_h(admin, F_29, L_30, nil)))). % 7.49/2.78 tff(c_114, plain, (sso_file_has_level(sso_compartmenta, secretfile, secret, scg_compartmenta))). % 7.49/2.78 tff(c_120, plain, (sso_file_has_citizenship(sso_compartmenta, secretfile, usa, scg_compartmenta))). % 7.49/2.78 tff(c_118, plain, (sso_file_has_citizenship(sso_compartmentb, secretfile, usa, scg_compartmentb))). % 7.49/2.78 tff(c_20, plain, (![F_19, CL_20]: (admin_file_has_compartments_h(admin, F_19, CL_20, nil)))). % 7.49/2.78 tff(c_128, plain, (system_file_needs_level(system, not_secretfile, unclassified))). % 7.49/2.78 tff(c_130, plain, (system_file_needs_citizenship(system, not_secretfile, anycountry))). % 7.49/2.79 tff(c_154, plain, (system_indi_needs_level(system, alice, secret))). % 7.49/2.79 tff(c_10, plain, (![K_5, L_6]: (loca_level_below(K_5, L_6, L_6)))). % 7.49/2.79 tff(c_90, plain, (system_compartment_has_sso(system, compartmentb, sso_compartmentb))). % 7.49/2.79 tff(c_156, plain, (level_admin_indi_has_level(level_admin, alice, topsecret))). % 7.49/2.79 tff(c_94, plain, (sso_compartment_has_scg(sso_compartmentb, compartmentb, scg_compartmentb))). % 7.49/2.79 tff(c_172, plain, (owner_indi_has_need_to_know(owner_not_secretfile, babu, not_secretfile))). % 7.49/2.79 tff(c_126, plain, (system_file_needs_compartments(system, not_secretfile, nil))). % 7.49/2.79 tff(c_166, plain, (owner_indi_has_need_to_know(owner_secretfile, alice, secretfile))). % 7.49/2.79 tff(c_174, plain, (system_indi_is_counterintelligence(system, ci, owner_secretfile))). % 7.49/2.79 tff(c_168, plain, (owner_indi_has_need_to_know(owner_secretfile, alice, not_secretfile))). % 7.49/2.79 tff(c_92, plain, (oca_compartment_has_scg(oca, compartmentb, scg_compartmentb))). % 7.49/2.79 tff(c_96, plain, (system_compartment_has_sso(system, compartmenta, sso_compartmenta))). % 7.49/2.79 tff(c_54, plain, (![K_68]: (admin_indi_has_compartments(admin, K_68, nil)))). % 7.49/2.79 tff(c_158, plain, (system_indi_needs_compartment(system, alice, compartmentb))). % 7.49/2.79 tff(c_8, plain, (![K_4]: (loca_level_direct_below(K_4, secret, topsecret)))). % 7.49/2.79 tff(c_98, plain, (oca_compartment_has_scg(oca, compartmenta, scg_compartmenta))). % 7.49/2.79 tff(c_150, plain, (background_admin_indi_has_background(background_admin, alice, topsecret))). % 7.49/2.79 tff(c_164, plain, (sso_indi_has_compartment(sso_compartmenta, alice, compartmenta))). % 7.49/2.79 tff(c_6, plain, (![K_3]: (loca_level_direct_below(K_3, confidential, secret)))). % 7.49/2.79 tff(c_116, plain, (system_file_needs_citizenship(system, secretfile, usa))). % 7.49/2.79 tff(c_4, plain, (![K_2]: (loca_level_direct_below(K_2, sbu, confidential)))). % 7.49/2.79 tff(c_40, plain, (![K_52]: (admin_indi_has_background(admin, K_52, unclassified)))). % 7.49/2.79 tff(c_110, plain, (system_file_needs_level(system, secretfile, secret))). % 7.49/2.79 tff(c_144, plain, (system_indi_has_citizenship(system, alice, usa))). % 7.49/2.79 tff(c_50, plain, (![K_62]: (admin_indi_has_level(admin, K_62, unclassified)))). % 7.49/2.79 tff(c_160, plain, (system_indi_needs_compartment(system, alice, compartmenta))). % 7.49/2.79 tff(c_46, plain, (![K_59]: (admin_indi_has_citizenship(admin, K_59, anycountry)))). % 7.49/2.79 tff(c_2, plain, (![K_1]: (loca_level_direct_below(K_1, unclassified, sbu)))). % 7.49/2.79 tff(c_170, plain, (system_indi_has_citizenship(system, babu, india))). % 7.49/2.79 tff(c_162, plain, (sso_indi_has_compartment(sso_compartmentb, alice, compartmentb))). % 7.49/2.79 tff(c_100, plain, (sso_compartment_has_scg(sso_compartmenta, compartmenta, scg_compartmenta))). % 7.49/2.79 tff(c_132, plain, (state_file_has_owner(not_secretfile, owner_not_secretfile))). % 7.49/2.79 tff(c_134, plain, (system_indi_is_polygraph_admin(system, polygraph_admin))). % 7.49/2.79 tff(c_136, plain, (system_indi_is_credit_admin(system, credit_admin))). % 7.49/2.79 tff(c_84, plain, (system_indi_is_oca(system, oca))). % 7.49/2.79 tff(c_176, plain, (~admin_indi_may_file(admin, babu, secretfile, read))). % 7.49/2.79 tff(c_152, plain, (hr_admin_indi_has_employment(hr_admin, alice))). % 7.49/2.79 tff(c_148, plain, (credit_admin_indi_has_credit(credit_admin, alice))). % 7.49/2.79 tff(c_122, plain, (state_file_has_owner(secretfile, owner_secretfile))). % 7.49/2.79 tff(c_138, plain, (system_indi_is_background_admin(system, background_admin))). % 7.49/2.79 tff(c_140, plain, (system_indi_is_hr_admin(system, hr_admin))). % 7.49/2.79 tff(c_142, plain, (system_indi_is_level_admin(system, level_admin))). % 7.49/2.79 tff(c_146, plain, (polygraph_admin_indi_has_polygraph(polygraph_admin, alice))). % 7.49/2.79 tff(c_102, plain, (state_file_is_not_working_paper(secretfile))). % 7.49/2.79 tff(c_124, plain, (state_file_is_not_working_paper(not_secretfile))). % 7.49/2.79 % SZS output end Saturation for /export/starexec/sandbox2/benchmark/theBenchmark.p % 7.49/2.79 %------------------------------------------------------------------------------