%------------------------------------------------------------------------------
% File : leanCoP---2.2
% Problem : SWV437+1 : TPTP v8.1.0. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : leancop_casc.sh %s %d
% Computer : n020.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 600s
% DateTime : Wed Jul 20 19:51:04 EDT 2022
% Result : Theorem 1.43s 2.44s
% Output : Proof 1.43s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : SWV437+1 : TPTP v8.1.0. Released v4.0.0.
% 0.07/0.12 % Command : leancop_casc.sh %s %d
% 0.12/0.33 % Computer : n020.cluster.edu
% 0.12/0.33 % Model : x86_64 x86_64
% 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.33 % Memory : 8042.1875MB
% 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.33 % CPULimit : 300
% 0.12/0.33 % WCLimit : 600
% 0.12/0.33 % DateTime : Thu Jun 16 02:22:19 EDT 2022
% 0.12/0.33 % CPUTime :
% 1.43/2.44 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 1.43/2.44 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 1.43/2.45
% 1.43/2.45 %-----------------------------------------------------
% 1.43/2.45 fof(alicereadsecret, conjecture, admin_indi_may_file(admin, alice, secretfile, read), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', alicereadsecret)).
% 1.43/2.45 fof(ax41, hypothesis, system_indi_is_oca(system, oca), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax41)).
% 1.43/2.45 fof(ax42, hypothesis, oca_compartment_is_compartment(oca, compartmentb, confidential, topsecret, yes, yes), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax42)).
% 1.43/2.45 fof(ax43, hypothesis, oca_compartment_is_compartment(oca, compartmenta, sbu, unclassified, no, no), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax43)).
% 1.43/2.45 fof(ax44, hypothesis, system_compartment_has_sso(system, compartmentb, sso_compartmentb), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax44)).
% 1.43/2.45 fof(ax45, hypothesis, oca_compartment_has_scg(oca, compartmentb, scg_compartmentb), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax45)).
% 1.43/2.45 fof(ax46, hypothesis, sso_compartment_has_scg(sso_compartmentb, compartmentb, scg_compartmentb), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax46)).
% 1.43/2.45 fof(ax47, hypothesis, system_compartment_has_sso(system, compartmenta, sso_compartmenta), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax47)).
% 1.43/2.45 fof(ax48, hypothesis, oca_compartment_has_scg(oca, compartmenta, scg_compartmenta), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax48)).
% 1.43/2.45 fof(ax49, hypothesis, sso_compartment_has_scg(sso_compartmenta, compartmenta, scg_compartmenta), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax49)).
% 1.43/2.45 fof(ax50, hypothesis, state_file_is_not_working_paper(secretfile), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax50)).
% 1.43/2.45 fof(ax51, hypothesis, system_file_needs_compartments(system, secretfile, cons(compartmentb, cons(compartmenta, nil))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax51)).
% 1.43/2.45 fof(ax52, hypothesis, sso_file_has_compartments(sso_compartmentb, secretfile, cons(compartmentb, cons(compartmenta, nil))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax52)).
% 1.43/2.45 fof(ax53, hypothesis, sso_file_has_compartments(sso_compartmenta, secretfile, cons(compartmentb, cons(compartmenta, nil))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax53)).
% 1.43/2.45 fof(ax54, hypothesis, system_file_needs_level(system, secretfile, secret), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax54)).
% 1.43/2.45 fof(ax55, hypothesis, sso_file_has_level(sso_compartmentb, secretfile, secret, scg_compartmentb), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax55)).
% 1.43/2.45 fof(ax56, hypothesis, sso_file_has_level(sso_compartmenta, secretfile, secret, scg_compartmenta), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax56)).
% 1.43/2.45 fof(ax57, hypothesis, system_file_needs_citizenship(system, secretfile, usa), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax57)).
% 1.43/2.45 fof(ax58, hypothesis, sso_file_has_citizenship(sso_compartmentb, secretfile, usa, scg_compartmentb), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax58)).
% 1.43/2.45 fof(ax59, hypothesis, sso_file_has_citizenship(sso_compartmenta, secretfile, usa, scg_compartmenta), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax59)).
% 1.43/2.45 fof(ax60, hypothesis, state_file_has_owner(secretfile, owner_secretfile), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax60)).
% 1.43/2.45 fof(ax66, hypothesis, system_indi_is_polygraph_admin(system, polygraph_admin), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax66)).
% 1.43/2.45 fof(ax67, hypothesis, system_indi_is_credit_admin(system, credit_admin), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax67)).
% 1.43/2.45 fof(ax68, hypothesis, system_indi_is_background_admin(system, background_admin), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax68)).
% 1.43/2.45 fof(ax69, hypothesis, system_indi_is_hr_admin(system, hr_admin), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax69)).
% 1.43/2.45 fof(ax70, hypothesis, system_indi_is_level_admin(system, level_admin), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax70)).
% 1.43/2.45 fof(ax71, hypothesis, system_indi_has_citizenship(system, alice, usa), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax71)).
% 1.43/2.45 fof(ax72, hypothesis, polygraph_admin_indi_has_polygraph(polygraph_admin, alice), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax72)).
% 1.43/2.45 fof(ax73, hypothesis, credit_admin_indi_has_credit(credit_admin, alice), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax73)).
% 1.43/2.45 fof(ax74, hypothesis, background_admin_indi_has_background(background_admin, alice, topsecret), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax74)).
% 1.43/2.45 fof(ax75, hypothesis, hr_admin_indi_has_employment(hr_admin, alice), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax75)).
% 1.43/2.45 fof(ax76, hypothesis, system_indi_needs_level(system, alice, secret), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax76)).
% 1.43/2.45 fof(ax77, hypothesis, level_admin_indi_has_level(level_admin, alice, topsecret), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax77)).
% 1.43/2.45 fof(ax78, hypothesis, system_indi_needs_compartment(system, alice, compartmentb), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax78)).
% 1.43/2.45 fof(ax79, hypothesis, system_indi_needs_compartment(system, alice, compartmenta), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax79)).
% 1.43/2.45 fof(ax80, hypothesis, sso_indi_has_compartment(sso_compartmentb, alice, compartmentb), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax80)).
% 1.43/2.45 fof(ax81, hypothesis, sso_indi_has_compartment(sso_compartmenta, alice, compartmenta), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax81)).
% 1.43/2.45 fof(ax82, hypothesis, owner_indi_has_need_to_know(owner_secretfile, alice, secretfile), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax82)).
% 1.43/2.45 fof(ax1, axiom, ! [_141316] : loca_level_direct_below(_141316, sbu, confidential), file('/export/starexec/sandbox2/benchmark/Axioms/SWV009+0.ax', ax1)).
% 1.43/2.45 fof(ax2, axiom, ! [_141430] : loca_level_direct_below(_141430, confidential, secret), file('/export/starexec/sandbox2/benchmark/Axioms/SWV009+0.ax', ax2)).
% 1.43/2.45 fof(ax3, axiom, ! [_141544] : loca_level_direct_below(_141544, secret, topsecret), file('/export/starexec/sandbox2/benchmark/Axioms/SWV009+0.ax', ax3)).
% 1.43/2.45 fof(ax4, axiom, ! [_141658, _141661] : loca_level_below(_141658, _141661, _141661), file('/export/starexec/sandbox2/benchmark/Axioms/SWV009+0.ax', ax4)).
% 1.43/2.45 fof(ax5, axiom, ! [_141783, _141786, _141789, _141792] : (loca_level_direct_below(_141783, _141789, _141792) => loca_level_below(_141783, _141786, _141789) => loca_level_below(_141783, _141786, _141792)), file('/export/starexec/sandbox2/benchmark/Axioms/SWV009+0.ax', ax5)).
% 1.43/2.45 fof(ax6, axiom, ! [_142000, _142003] : (system_compartment_has_sso(system, _142000, _142003) => admin_compartment_has_sso(admin, _142000, _142003)), file('/export/starexec/sandbox2/benchmark/Axioms/SWV009+0.ax', ax6)).
% 1.43/2.45 fof(ax7, axiom, ! [_142160, _142163, _142166, _142169] : (system_indi_is_oca(system, _142160) => oca_compartment_has_scg(_142160, _142163, _142169) => admin_compartment_has_sso(admin, _142163, _142166) => sso_compartment_has_scg(_142166, _142163, _142169) => admin_compartment_has_scg(admin, _142163, _142169)), file('/export/starexec/sandbox2/benchmark/Axioms/SWV009+0.ax', ax7)).
% 1.43/2.45 fof(ax8, axiom, ! [_142440, _142443] : (system_file_needs_compartments(system, _142440, _142443) => admin_file_has_compartments_h(admin, _142440, _142443, _142443) => admin_file_has_compartments(admin, _142440, _142443)), file('/export/starexec/sandbox2/benchmark/Axioms/SWV009+0.ax', ax8)).
% 1.43/2.45 fof(ax9, axiom, ! [_142642, _142645] : admin_file_has_compartments_h(admin, _142642, _142645, nil), file('/export/starexec/sandbox2/benchmark/Axioms/SWV009+0.ax', ax9)).
% 1.43/2.45 fof(ax10, axiom, ! [_142774, _142777, _142780, _142783, _142786] : (admin_compartment_has_sso(admin, _142780, _142786) => sso_file_has_compartments(_142786, _142774, _142777) => admin_file_has_compartments_h(admin, _142774, _142777, _142783) => admin_file_has_compartments_h(admin, _142774, _142777, cons(_142780, _142783))), file('/export/starexec/sandbox2/benchmark/Axioms/SWV009+0.ax', ax10)).
% 1.43/2.45 fof(ax11, axiom, ! [_143067, _143070, _143073] : (system_file_needs_level(system, _143067, _143070) => admin_file_has_compartments(admin, _143067, _143073) => admin_file_has_level_h(admin, _143067, _143070, _143073) => admin_file_has_level(admin, _143067, _143070)), file('/export/starexec/sandbox2/benchmark/Axioms/SWV009+0.ax', ax11)).
% 1.43/2.45 fof(ax12, axiom, ! [_143315, _143318] : admin_file_has_level_h(admin, _143315, _143318, nil), file('/export/starexec/sandbox2/benchmark/Axioms/SWV009+0.ax', ax12)).
% 1.43/2.45 fof(ax13, axiom, ! [_143447, _143450, _143453, _143456, _143459, _143462] : (admin_compartment_has_sso(admin, _143453, _143459) => admin_compartment_has_scg(admin, _143453, _143462) => sso_file_has_level(_143459, _143447, _143450, _143462) => admin_file_has_level_h(admin, _143447, _143450, _143456) => admin_file_has_level_h(admin, _143447, _143450, cons(_143453, _143456))), file('/export/starexec/sandbox2/benchmark/Axioms/SWV009+0.ax', ax13)).
% 1.43/2.45 fof(ax14, axiom, ! [_143793, _143796, _143799] : (system_file_needs_citizenship(system, _143793, _143796) => admin_file_has_compartments(admin, _143793, _143799) => admin_file_has_citizenship_h(admin, _143793, _143796, _143799) => admin_file_has_citizenship(admin, _143793, _143796)), file('/export/starexec/sandbox2/benchmark/Axioms/SWV009+0.ax', ax14)).
% 1.43/2.45 fof(ax15, axiom, ! [_144041, _144044] : admin_file_has_citizenship_h(admin, _144041, _144044, nil), file('/export/starexec/sandbox2/benchmark/Axioms/SWV009+0.ax', ax15)).
% 1.43/2.45 fof(ax16, axiom, ! [_144173, _144176, _144179, _144182, _144185, _144188] : (admin_compartment_has_sso(admin, _144179, _144185) => admin_compartment_has_scg(admin, _144179, _144188) => sso_file_has_citizenship(_144185, _144173, _144176, _144188) => admin_file_has_citizenship_h(admin, _144173, _144176, _144182) => admin_file_has_citizenship_h(admin, _144173, _144176, cons(_144179, _144182))), file('/export/starexec/sandbox2/benchmark/Axioms/SWV009+0.ax', ax16)).
% 1.43/2.45 fof(ax17, axiom, ! [_144519, _144522] : (system_indi_is_polygraph_admin(system, _144522) => polygraph_admin_indi_has_polygraph(_144522, _144519) => admin_indi_has_polygraph(admin, _144519)), file('/export/starexec/sandbox2/benchmark/Axioms/SWV009+0.ax', ax17)).
% 1.43/2.45 fof(ax18, axiom, ! [_144693, _144696] : (system_indi_is_credit_admin(system, _144696) => credit_admin_indi_has_credit(_144696, _144693) => admin_indi_has_credit(admin, _144693)), file('/export/starexec/sandbox2/benchmark/Axioms/SWV009+0.ax', ax18)).
% 1.43/2.45 fof(ax19, axiom, ! [_144867] : admin_indi_has_background(admin, _144867, unclassified), file('/export/starexec/sandbox2/benchmark/Axioms/SWV009+0.ax', ax19)).
% 1.43/2.45 fof(ax20, axiom, ! [_144981, _144984, _144987, _144990] : (system_indi_is_background_admin(system, _144987) => background_admin_indi_has_background(_144987, _144981, _144990) => loca_level_below(admin, _144984, _144990) => admin_indi_has_background(admin, _144981, _144984)), file('/export/starexec/sandbox2/benchmark/Axioms/SWV009+0.ax', ax20)).
% 1.43/2.45 fof(ax21, axiom, ! [_145226, _145229] : (system_indi_is_hr_admin(system, _145229) => hr_admin_indi_has_employment(_145229, _145226) => admin_indi_has_employment(admin, _145226)), file('/export/starexec/sandbox2/benchmark/Axioms/SWV009+0.ax', ax21)).
% 1.43/2.45 fof(ax23, axiom, ! [_145401, _145404] : (system_indi_has_citizenship(system, _145401, _145404) => admin_indi_has_citizenship(admin, _145401, _145404)), file('/export/starexec/sandbox2/benchmark/Axioms/SWV009+0.ax', ax23)).
% 1.43/2.45 fof(ax25, axiom, ! [_145562, _145565, _145568, _145571, _145574] : (system_indi_needs_level(system, _145562, _145568) => admin_indi_has_citizenship(admin, _145562, usa) => admin_indi_has_polygraph(admin, _145562) => admin_indi_has_employment(admin, _145562) => admin_indi_has_credit(admin, _145562) => loca_level_below(admin, _145565, _145568) => system_indi_is_level_admin(system, _145571) => level_admin_indi_has_level(_145571, _145562, _145574) => loca_level_below(admin, _145565, _145574) => admin_indi_has_background(admin, _145562, _145565) => admin_indi_has_level(admin, _145562, _145565)), file('/export/starexec/sandbox2/benchmark/Axioms/SWV009+0.ax', ax25)).
% 1.43/2.45 fof(ax26, axiom, ! [_146042] : admin_indi_has_compartments(admin, _146042, nil), file('/export/starexec/sandbox2/benchmark/Axioms/SWV009+0.ax', ax26)).
% 1.43/2.45 fof(ax27, axiom, ! [_146156, _146159, _146162, _146165] : (system_indi_needs_compartment(system, _146156, _146159) => admin_indi_has_employment(admin, _146156) => admin_indi_has_citizenship(admin, _146156, usa) => admin_indi_has_polygraph_for_compartment(admin, _146156, _146159) => admin_indi_has_credit_for_compartment(admin, _146156, _146159) => admin_compartment_has_sso(admin, _146159, _146165) => sso_indi_has_compartment(_146165, _146156, _146159) => admin_indi_has_background_for_compartment(admin, _146156, _146159) => admin_indi_has_level_for_compartment(admin, _146156, _146159) => admin_indi_has_compartments(admin, _146156, _146162) => admin_indi_has_compartments(admin, _146156, cons(_146159, _146162))), file('/export/starexec/sandbox2/benchmark/Axioms/SWV009+0.ax', ax27)).
% 1.43/2.45 fof(ax28, axiom, ! [_146662, _146665, _146668, _146671, _146674, _146677, _146680] : (system_indi_is_oca(system, _146668) => oca_compartment_is_compartment(_146668, _146665, _146671, _146674, _146677, _146680) => admin_indi_has_background(admin, _146662, _146674) => admin_indi_has_background_for_compartment(admin, _146662, _146665)), file('/export/starexec/sandbox2/benchmark/Axioms/SWV009+0.ax', ax28)).
% 1.43/2.45 fof(ax29, axiom, ! [_146961, _146964, _146967, _146970, _146973, _146976, _146979] : (system_indi_is_oca(system, _146967) => oca_compartment_is_compartment(_146967, _146964, _146970, _146973, _146976, _146979) => admin_indi_has_level(admin, _146961, _146970) => admin_indi_has_level_for_compartment(admin, _146961, _146964)), file('/export/starexec/sandbox2/benchmark/Axioms/SWV009+0.ax', ax29)).
% 1.43/2.45 fof(ax30, axiom, ! [_147260, _147263, _147266, _147269, _147272, _147275] : (system_indi_is_oca(system, _147266) => oca_compartment_is_compartment(_147266, _147263, _147269, _147272, _147275, yes) => admin_indi_has_polygraph(admin, _147260) => admin_indi_has_polygraph_for_compartment(admin, _147260, _147263)), file('/export/starexec/sandbox2/benchmark/Axioms/SWV009+0.ax', ax30)).
% 1.43/2.45 fof(ax31, axiom, ! [_147541, _147544, _147547, _147550, _147553, _147556] : (system_indi_is_oca(system, _147547) => oca_compartment_is_compartment(_147547, _147544, _147550, _147553, _147556, no) => admin_indi_has_polygraph_for_compartment(admin, _147541, _147544)), file('/export/starexec/sandbox2/benchmark/Axioms/SWV009+0.ax', ax31)).
% 1.43/2.45 fof(ax32, axiom, ! [_147794, _147797, _147800, _147803, _147806, _147809] : (system_indi_is_oca(system, _147800) => oca_compartment_is_compartment(_147800, _147797, _147803, _147806, yes, _147809) => admin_indi_has_credit(admin, _147794) => admin_indi_has_credit_for_compartment(admin, _147794, _147797)), file('/export/starexec/sandbox2/benchmark/Axioms/SWV009+0.ax', ax32)).
% 1.43/2.45 fof(ax33, axiom, ! [_148075, _148078, _148081, _148084, _148087, _148090] : (system_indi_is_oca(system, _148081) => oca_compartment_is_compartment(_148081, _148078, _148084, _148087, no, _148090) => admin_indi_has_credit_for_compartment(admin, _148075, _148078)), file('/export/starexec/sandbox2/benchmark/Axioms/SWV009+0.ax', ax33)).
% 1.43/2.45 fof(ax34, axiom, ! [_148328, _148331, _148334] : (admin_file_has_compartments(admin, _148331, _148334) => admin_indi_has_compartments(admin, _148328, _148334) => admin_indi_has_compartments_for_file(admin, _148328, _148331)), file('/export/starexec/sandbox2/benchmark/Axioms/SWV009+0.ax', ax34)).
% 1.43/2.45 fof(ax35, axiom, ! [_148534, _148537, _148540] : (admin_file_has_level(admin, _148537, _148540) => admin_indi_has_level(admin, _148534, _148540) => admin_indi_has_level_for_file(admin, _148534, _148537)), file('/export/starexec/sandbox2/benchmark/Axioms/SWV009+0.ax', ax35)).
% 1.43/2.45 fof(ax36, axiom, ! [_148740, _148743, _148746] : (state_file_has_owner(_148743, _148746) => owner_indi_has_need_to_know(_148746, _148740, _148743) => admin_indi_has_need_to_know_for_file(admin, _148740, _148743)), file('/export/starexec/sandbox2/benchmark/Axioms/SWV009+0.ax', ax36)).
% 1.43/2.45 fof(ax37, axiom, ! [_148939, _148942, _148945] : (admin_file_has_citizenship(admin, _148942, _148945) => admin_indi_has_citizenship(admin, _148939, _148945) => admin_indi_has_citizenship_for_file(admin, _148939, _148942)), file('/export/starexec/sandbox2/benchmark/Axioms/SWV009+0.ax', ax37)).
% 1.43/2.45 fof(ax39, axiom, ! [_149147, _149150] : (state_file_is_not_working_paper(_149150) => admin_indi_has_citizenship_for_file(admin, _149147, _149150) => admin_indi_has_need_to_know_for_file(admin, _149147, _149150) => admin_indi_has_level_for_file(admin, _149147, _149150) => admin_indi_has_compartments_for_file(admin, _149147, _149150) => admin_indi_may_file(admin, _149147, _149150, read)), file('/export/starexec/sandbox2/benchmark/Axioms/SWV009+0.ax', ax39)).
% 1.43/2.45
% 1.43/2.45 cnf(1, plain, [admin_indi_may_file(admin, alice, secretfile, read)], clausify(alicereadsecret)).
% 1.43/2.45 cnf(2, plain, [-(system_indi_is_oca(system, oca))], clausify(ax41)).
% 1.43/2.45 cnf(3, plain, [-(oca_compartment_is_compartment(oca, compartmentb, confidential, topsecret, yes, yes))], clausify(ax42)).
% 1.43/2.45 cnf(4, plain, [-(oca_compartment_is_compartment(oca, compartmenta, sbu, unclassified, no, no))], clausify(ax43)).
% 1.43/2.45 cnf(5, plain, [-(system_compartment_has_sso(system, compartmentb, sso_compartmentb))], clausify(ax44)).
% 1.43/2.45 cnf(6, plain, [-(oca_compartment_has_scg(oca, compartmentb, scg_compartmentb))], clausify(ax45)).
% 1.43/2.45 cnf(7, plain, [-(sso_compartment_has_scg(sso_compartmentb, compartmentb, scg_compartmentb))], clausify(ax46)).
% 1.43/2.45 cnf(8, plain, [-(system_compartment_has_sso(system, compartmenta, sso_compartmenta))], clausify(ax47)).
% 1.43/2.45 cnf(9, plain, [-(oca_compartment_has_scg(oca, compartmenta, scg_compartmenta))], clausify(ax48)).
% 1.43/2.45 cnf(10, plain, [-(sso_compartment_has_scg(sso_compartmenta, compartmenta, scg_compartmenta))], clausify(ax49)).
% 1.43/2.45 cnf(11, plain, [-(state_file_is_not_working_paper(secretfile))], clausify(ax50)).
% 1.43/2.45 cnf(12, plain, [-(system_file_needs_compartments(system, secretfile, cons(compartmentb, cons(compartmenta, nil))))], clausify(ax51)).
% 1.43/2.45 cnf(13, plain, [-(sso_file_has_compartments(sso_compartmentb, secretfile, cons(compartmentb, cons(compartmenta, nil))))], clausify(ax52)).
% 1.43/2.45 cnf(14, plain, [-(sso_file_has_compartments(sso_compartmenta, secretfile, cons(compartmentb, cons(compartmenta, nil))))], clausify(ax53)).
% 1.43/2.45 cnf(15, plain, [-(system_file_needs_level(system, secretfile, secret))], clausify(ax54)).
% 1.43/2.45 cnf(16, plain, [-(sso_file_has_level(sso_compartmentb, secretfile, secret, scg_compartmentb))], clausify(ax55)).
% 1.43/2.45 cnf(17, plain, [-(sso_file_has_level(sso_compartmenta, secretfile, secret, scg_compartmenta))], clausify(ax56)).
% 1.43/2.45 cnf(18, plain, [-(system_file_needs_citizenship(system, secretfile, usa))], clausify(ax57)).
% 1.43/2.45 cnf(19, plain, [-(sso_file_has_citizenship(sso_compartmentb, secretfile, usa, scg_compartmentb))], clausify(ax58)).
% 1.43/2.45 cnf(20, plain, [-(sso_file_has_citizenship(sso_compartmenta, secretfile, usa, scg_compartmenta))], clausify(ax59)).
% 1.43/2.45 cnf(21, plain, [-(state_file_has_owner(secretfile, owner_secretfile))], clausify(ax60)).
% 1.43/2.45 cnf(22, plain, [-(system_indi_is_polygraph_admin(system, polygraph_admin))], clausify(ax66)).
% 1.43/2.45 cnf(23, plain, [-(system_indi_is_credit_admin(system, credit_admin))], clausify(ax67)).
% 1.43/2.45 cnf(24, plain, [-(system_indi_is_background_admin(system, background_admin))], clausify(ax68)).
% 1.43/2.45 cnf(25, plain, [-(system_indi_is_hr_admin(system, hr_admin))], clausify(ax69)).
% 1.43/2.45 cnf(26, plain, [-(system_indi_is_level_admin(system, level_admin))], clausify(ax70)).
% 1.43/2.45 cnf(27, plain, [-(system_indi_has_citizenship(system, alice, usa))], clausify(ax71)).
% 1.43/2.45 cnf(28, plain, [-(polygraph_admin_indi_has_polygraph(polygraph_admin, alice))], clausify(ax72)).
% 1.43/2.45 cnf(29, plain, [-(credit_admin_indi_has_credit(credit_admin, alice))], clausify(ax73)).
% 1.43/2.45 cnf(30, plain, [-(background_admin_indi_has_background(background_admin, alice, topsecret))], clausify(ax74)).
% 1.43/2.45 cnf(31, plain, [-(hr_admin_indi_has_employment(hr_admin, alice))], clausify(ax75)).
% 1.43/2.45 cnf(32, plain, [-(system_indi_needs_level(system, alice, secret))], clausify(ax76)).
% 1.43/2.45 cnf(33, plain, [-(level_admin_indi_has_level(level_admin, alice, topsecret))], clausify(ax77)).
% 1.43/2.45 cnf(34, plain, [-(system_indi_needs_compartment(system, alice, compartmentb))], clausify(ax78)).
% 1.43/2.45 cnf(35, plain, [-(system_indi_needs_compartment(system, alice, compartmenta))], clausify(ax79)).
% 1.43/2.45 cnf(36, plain, [-(sso_indi_has_compartment(sso_compartmentb, alice, compartmentb))], clausify(ax80)).
% 1.43/2.45 cnf(37, plain, [-(sso_indi_has_compartment(sso_compartmenta, alice, compartmenta))], clausify(ax81)).
% 1.43/2.45 cnf(38, plain, [-(owner_indi_has_need_to_know(owner_secretfile, alice, secretfile))], clausify(ax82)).
% 1.43/2.45 cnf(39, plain, [-(loca_level_direct_below(_16897, sbu, confidential))], clausify(ax1)).
% 1.43/2.45 cnf(40, plain, [-(loca_level_direct_below(_17112, confidential, secret))], clausify(ax2)).
% 1.43/2.45 cnf(41, plain, [-(loca_level_direct_below(_17327, secret, topsecret))], clausify(ax3)).
% 1.43/2.45 cnf(42, plain, [-(loca_level_below(_17542, _17582, _17582))], clausify(ax4)).
% 1.43/2.45 cnf(43, plain, [loca_level_direct_below(_17808, _17935, _17997), loca_level_below(_17808, _17872, _17935), -(loca_level_below(_17808, _17872, _17997))], clausify(ax5)).
% 1.43/2.45 cnf(44, plain, [system_compartment_has_sso(system, _18487, _18534), -(admin_compartment_has_sso(admin, _18487, _18534))], clausify(ax6)).
% 1.43/2.45 cnf(45, plain, [system_indi_is_oca(system, _18881), oca_compartment_has_scg(_18881, _18958, _19109), admin_compartment_has_sso(admin, _18958, _19034), sso_compartment_has_scg(_19034, _18958, _19109), -(admin_compartment_has_scg(admin, _18958, _19109))], clausify(ax7)).
% 1.43/2.45 cnf(46, plain, [system_file_needs_compartments(system, _19800, _19855), admin_file_has_compartments_h(admin, _19800, _19855, _19855), -(admin_file_has_compartments(admin, _19800, _19855))], clausify(ax8)).
% 1.43/2.45 cnf(47, plain, [-(admin_file_has_compartments_h(admin, _20364, _20405, nil))], clausify(ax9)).
% 1.43/2.45 cnf(48, plain, [admin_compartment_has_sso(admin, _20833, _20990), sso_file_has_compartments(_20990, _20672, _20753), admin_file_has_compartments_h(admin, _20672, _20753, _20912), -(admin_file_has_compartments_h(admin, _20672, _20753, cons(_20833, _20912)))], clausify(ax10)).
% 1.43/2.45 cnf(49, plain, [system_file_needs_level(system, _21734, _21801), admin_file_has_compartments(admin, _21734, _21867), admin_file_has_level_h(admin, _21734, _21801, _21867), -(admin_file_has_level(admin, _21734, _21801))], clausify(ax11)).
% 1.43/2.45 cnf(50, plain, [-(admin_file_has_level_h(admin, _22508, _22549, nil))], clausify(ax12)).
% 1.43/2.45 cnf(51, plain, [admin_compartment_has_sso(admin, _23003, _23186), admin_compartment_has_scg(admin, _23003, _23276), sso_file_has_level(_23186, _22816, _22910, _23276), admin_file_has_level_h(admin, _22816, _22910, _23095), -(admin_file_has_level_h(admin, _22816, _22910, cons(_23003, _23095)))], clausify(ax13)).
% 1.43/2.45 cnf(52, plain, [system_file_needs_citizenship(system, _24193, _24260), admin_file_has_compartments(admin, _24193, _24326), admin_file_has_citizenship_h(admin, _24193, _24260, _24326), -(admin_file_has_citizenship(admin, _24193, _24260))], clausify(ax14)).
% 1.43/2.45 cnf(53, plain, [-(admin_file_has_citizenship_h(admin, _24967, _25008, nil))], clausify(ax15)).
% 1.43/2.45 cnf(54, plain, [admin_compartment_has_sso(admin, _25462, _25645), admin_compartment_has_scg(admin, _25462, _25735), sso_file_has_citizenship(_25645, _25275, _25369, _25735), admin_file_has_citizenship_h(admin, _25275, _25369, _25554), -(admin_file_has_citizenship_h(admin, _25275, _25369, cons(_25462, _25554)))], clausify(ax16)).
% 1.43/2.45 cnf(55, plain, [system_indi_is_polygraph_admin(system, _26703), polygraph_admin_indi_has_polygraph(_26703, _26652), -(admin_indi_has_polygraph(admin, _26652))], clausify(ax17)).
% 1.43/2.45 cnf(56, plain, [system_indi_is_credit_admin(system, _27099), credit_admin_indi_has_credit(_27099, _27048), -(admin_indi_has_credit(admin, _27048))], clausify(ax18)).
% 1.43/2.45 cnf(57, plain, [-(admin_indi_has_background(admin, _27444, unclassified))], clausify(ax19)).
% 1.43/2.45 cnf(58, plain, [system_indi_is_background_admin(system, _27798), background_admin_indi_has_background(_27798, _27659, _27866), loca_level_below(admin, _27729, _27866), -(admin_indi_has_background(admin, _27659, _27729))], clausify(ax20)).
% 1.43/2.45 cnf(59, plain, [system_indi_is_hr_admin(system, _28487), hr_admin_indi_has_employment(_28487, _28436), -(admin_indi_has_employment(admin, _28436))], clausify(ax21)).
% 1.43/2.45 cnf(60, plain, [system_indi_has_citizenship(system, _29047, _29094), -(admin_indi_has_citizenship(admin, _29047, _29094))], clausify(ax23)).
% 1.43/2.45 cnf(61, plain, [system_indi_needs_level(system, _29656, _29897), admin_indi_has_citizenship(admin, _29656, usa), admin_indi_has_polygraph(admin, _29656), admin_indi_has_employment(admin, _29656), admin_indi_has_credit(admin, _29656), loca_level_below(admin, _29777, _29897), system_indi_is_level_admin(system, _30016), level_admin_indi_has_level(_30016, _29656, _30134), loca_level_below(admin, _29777, _30134), admin_indi_has_background(admin, _29656, _29777), -(admin_indi_has_level(admin, _29656, _29777))], clausify(ax25)).
% 1.43/2.45 cnf(62, plain, [-(admin_indi_has_compartments(admin, _31439, nil))], clausify(ax26)).
% 1.43/2.45 cnf(63, plain, [system_indi_needs_compartment(system, _31654, _31776), admin_indi_has_employment(admin, _31654), admin_indi_has_citizenship(admin, _31654, usa), admin_indi_has_polygraph_for_compartment(admin, _31654, _31776), admin_indi_has_credit_for_compartment(admin, _31654, _31776), admin_compartment_has_sso(admin, _31776, _32017), sso_indi_has_compartment(_32017, _31654, _31776), admin_indi_has_background_for_compartment(admin, _31654, _31776), admin_indi_has_level_for_compartment(admin, _31654, _31776), admin_indi_has_compartments(admin, _31654, _31897), -(admin_indi_has_compartments(admin, _31654, cons(_31776, _31897)))], clausify(ax27)).
% 1.43/2.45 cnf(64, plain, [system_indi_is_oca(system, _33649), oca_compartment_is_compartment(_33649, _33562, _33735, _33820, _33904, _33987), admin_indi_has_background(admin, _33474, _33820), -(admin_indi_has_background_for_compartment(admin, _33474, _33562))], clausify(ax28)).
% 1.43/2.45 cnf(65, plain, [system_indi_is_oca(system, _34888), oca_compartment_is_compartment(_34888, _34801, _34974, _35059, _35143, _35226), admin_indi_has_level(admin, _34713, _34974), -(admin_indi_has_level_for_compartment(admin, _34713, _34801))], clausify(ax29)).
% 1.43/2.45 cnf(66, plain, [system_indi_is_oca(system, _36115), oca_compartment_is_compartment(_36115, _36034, _36195, _36274, _36352, yes), admin_indi_has_polygraph(admin, _35952), -(admin_indi_has_polygraph_for_compartment(admin, _35952, _36034))], clausify(ax30)).
% 1.43/2.45 cnf(67, plain, [system_indi_is_oca(system, _37177), oca_compartment_is_compartment(_37177, _37102, _37251, _37324, _37396, no), -(admin_indi_has_polygraph_for_compartment(admin, _37026, _37102))], clausify(ax31)).
% 1.43/2.45 cnf(68, plain, [system_indi_is_oca(system, _38153), oca_compartment_is_compartment(_38153, _38072, _38233, _38312, yes, _38390), admin_indi_has_credit(admin, _37990), -(admin_indi_has_credit_for_compartment(admin, _37990, _38072))], clausify(ax32)).
% 1.43/2.45 cnf(69, plain, [system_indi_is_oca(system, _39215), oca_compartment_is_compartment(_39215, _39140, _39289, _39362, no, _39434), -(admin_indi_has_credit_for_compartment(admin, _39064, _39140))], clausify(ax33)).
% 1.43/2.45 cnf(70, plain, [admin_file_has_compartments(admin, _40087, _40145), admin_indi_has_compartments(admin, _40028, _40145), -(admin_indi_has_compartments_for_file(admin, _40028, _40087))], clausify(ax34)).
% 1.43/2.45 cnf(71, plain, [admin_file_has_level(admin, _40683, _40741), admin_indi_has_level(admin, _40624, _40741), -(admin_indi_has_level_for_file(admin, _40624, _40683))], clausify(ax35)).
% 1.43/2.45 cnf(72, plain, [state_file_has_owner(_41278, _41335), owner_indi_has_need_to_know(_41335, _41220, _41278), -(admin_indi_has_need_to_know_for_file(admin, _41220, _41278))], clausify(ax36)).
% 1.43/2.45 cnf(73, plain, [admin_file_has_citizenship(admin, _41832, _41890), admin_indi_has_citizenship(admin, _41773, _41890), -(admin_indi_has_citizenship_for_file(admin, _41773, _41832))], clausify(ax37)).
% 1.43/2.45 cnf(74, plain, [state_file_is_not_working_paper(_42837), admin_indi_has_citizenship_for_file(admin, _42763, _42837), admin_indi_has_need_to_know_for_file(admin, _42763, _42837), admin_indi_has_level_for_file(admin, _42763, _42837), admin_indi_has_compartments_for_file(admin, _42763, _42837), -(admin_indi_may_file(admin, _42763, _42837, read))], clausify(ax39)).
% 1.43/2.45
% 1.43/2.45 cnf('1',plain,[admin_indi_may_file(admin, alice, secretfile, read)],start(1)).
% 1.43/2.45 cnf('1.1',plain,[-(admin_indi_may_file(admin, alice, secretfile, read)), state_file_is_not_working_paper(secretfile), admin_indi_has_citizenship_for_file(admin, alice, secretfile), admin_indi_has_need_to_know_for_file(admin, alice, secretfile), admin_indi_has_level_for_file(admin, alice, secretfile), admin_indi_has_compartments_for_file(admin, alice, secretfile)],extension(74,bind([[_42763, _42837], [alice, secretfile]]))).
% 1.43/2.45 cnf('1.1.1',plain,[-(state_file_is_not_working_paper(secretfile))],extension(11)).
% 1.43/2.45 cnf('1.1.2',plain,[-(admin_indi_has_citizenship_for_file(admin, alice, secretfile)), admin_file_has_citizenship(admin, secretfile, usa), admin_indi_has_citizenship(admin, alice, usa)],extension(73,bind([[_41832, _41773, _41890], [secretfile, alice, usa]]))).
% 1.43/2.45 cnf('1.1.2.1',plain,[-(admin_file_has_citizenship(admin, secretfile, usa)), system_file_needs_citizenship(system, secretfile, usa), admin_file_has_compartments(admin, secretfile, cons(compartmentb, cons(compartmenta, nil))), admin_file_has_citizenship_h(admin, secretfile, usa, cons(compartmentb, cons(compartmenta, nil)))],extension(52,bind([[_24193, _24260, _24326], [secretfile, usa, cons(compartmentb, cons(compartmenta, nil))]]))).
% 1.43/2.45 cnf('1.1.2.1.1',plain,[-(system_file_needs_citizenship(system, secretfile, usa))],extension(18)).
% 1.43/2.45 cnf('1.1.2.1.2',plain,[-(admin_file_has_compartments(admin, secretfile, cons(compartmentb, cons(compartmenta, nil)))), system_file_needs_compartments(system, secretfile, cons(compartmentb, cons(compartmenta, nil))), admin_file_has_compartments_h(admin, secretfile, cons(compartmentb, cons(compartmenta, nil)), cons(compartmentb, cons(compartmenta, nil)))],extension(46,bind([[_19800, _19855], [secretfile, cons(compartmentb, cons(compartmenta, nil))]]))).
% 1.43/2.45 cnf('1.1.2.1.2.1',plain,[-(system_file_needs_compartments(system, secretfile, cons(compartmentb, cons(compartmenta, nil))))],extension(12)).
% 1.43/2.45 cnf('1.1.2.1.2.2',plain,[-(admin_file_has_compartments_h(admin, secretfile, cons(compartmentb, cons(compartmenta, nil)), cons(compartmentb, cons(compartmenta, nil)))), admin_compartment_has_sso(admin, compartmentb, sso_compartmentb), sso_file_has_compartments(sso_compartmentb, secretfile, cons(compartmentb, cons(compartmenta, nil))), admin_file_has_compartments_h(admin, secretfile, cons(compartmentb, cons(compartmenta, nil)), cons(compartmenta, nil))],extension(48,bind([[_20833, _20990, _20672, _20753, _20912], [compartmentb, sso_compartmentb, secretfile, cons(compartmentb, cons(compartmenta, nil)), cons(compartmenta, nil)]]))).
% 1.43/2.45 cnf('1.1.2.1.2.2.1',plain,[-(admin_compartment_has_sso(admin, compartmentb, sso_compartmentb)), system_compartment_has_sso(system, compartmentb, sso_compartmentb)],extension(44,bind([[_18487, _18534], [compartmentb, sso_compartmentb]]))).
% 1.43/2.45 cnf('1.1.2.1.2.2.1.1',plain,[-(system_compartment_has_sso(system, compartmentb, sso_compartmentb))],extension(5)).
% 1.43/2.45 cnf('1.1.2.1.2.2.2',plain,[-(sso_file_has_compartments(sso_compartmentb, secretfile, cons(compartmentb, cons(compartmenta, nil))))],extension(13)).
% 1.43/2.45 cnf('1.1.2.1.2.2.3',plain,[-(admin_file_has_compartments_h(admin, secretfile, cons(compartmentb, cons(compartmenta, nil)), cons(compartmenta, nil))), admin_compartment_has_sso(admin, compartmenta, sso_compartmenta), sso_file_has_compartments(sso_compartmenta, secretfile, cons(compartmentb, cons(compartmenta, nil))), admin_file_has_compartments_h(admin, secretfile, cons(compartmentb, cons(compartmenta, nil)), nil)],extension(48,bind([[_20833, _20990, _20672, _20753, _20912], [compartmenta, sso_compartmenta, secretfile, cons(compartmentb, cons(compartmenta, nil)), nil]]))).
% 1.43/2.45 cnf('1.1.2.1.2.2.3.1',plain,[-(admin_compartment_has_sso(admin, compartmenta, sso_compartmenta)), system_compartment_has_sso(system, compartmenta, sso_compartmenta)],extension(44,bind([[_18487, _18534], [compartmenta, sso_compartmenta]]))).
% 1.43/2.45 cnf('1.1.2.1.2.2.3.1.1',plain,[-(system_compartment_has_sso(system, compartmenta, sso_compartmenta))],extension(8)).
% 1.43/2.45 cnf('1.1.2.1.2.2.3.2',plain,[-(sso_file_has_compartments(sso_compartmenta, secretfile, cons(compartmentb, cons(compartmenta, nil))))],extension(14)).
% 1.43/2.45 cnf('1.1.2.1.2.2.3.3',plain,[-(admin_file_has_compartments_h(admin, secretfile, cons(compartmentb, cons(compartmenta, nil)), nil))],extension(47,bind([[_20364, _20405], [secretfile, cons(compartmentb, cons(compartmenta, nil))]]))).
% 1.43/2.45 cnf('1.1.2.1.3',plain,[-(admin_file_has_citizenship_h(admin, secretfile, usa, cons(compartmentb, cons(compartmenta, nil)))), admin_compartment_has_sso(admin, compartmentb, sso_compartmentb), admin_compartment_has_scg(admin, compartmentb, scg_compartmentb), sso_file_has_citizenship(sso_compartmentb, secretfile, usa, scg_compartmentb), admin_file_has_citizenship_h(admin, secretfile, usa, cons(compartmenta, nil))],extension(54,bind([[_25462, _25645, _25735, _25275, _25369, _25554], [compartmentb, sso_compartmentb, scg_compartmentb, secretfile, usa, cons(compartmenta, nil)]]))).
% 1.43/2.45 cnf('1.1.2.1.3.1',plain,[-(admin_compartment_has_sso(admin, compartmentb, sso_compartmentb)), system_compartment_has_sso(system, compartmentb, sso_compartmentb)],extension(44,bind([[_18487, _18534], [compartmentb, sso_compartmentb]]))).
% 1.43/2.45 cnf('1.1.2.1.3.1.1',plain,[-(system_compartment_has_sso(system, compartmentb, sso_compartmentb))],extension(5)).
% 1.43/2.45 cnf('1.1.2.1.3.2',plain,[-(admin_compartment_has_scg(admin, compartmentb, scg_compartmentb)), system_indi_is_oca(system, oca), oca_compartment_has_scg(oca, compartmentb, scg_compartmentb), admin_compartment_has_sso(admin, compartmentb, sso_compartmentb), sso_compartment_has_scg(sso_compartmentb, compartmentb, scg_compartmentb)],extension(45,bind([[_18881, _19034, _18958, _19109], [oca, sso_compartmentb, compartmentb, scg_compartmentb]]))).
% 1.43/2.45 cnf('1.1.2.1.3.2.1',plain,[-(system_indi_is_oca(system, oca))],extension(2)).
% 1.43/2.45 cnf('1.1.2.1.3.2.2',plain,[-(oca_compartment_has_scg(oca, compartmentb, scg_compartmentb))],extension(6)).
% 1.43/2.45 cnf('1.1.2.1.3.2.3',plain,[-(admin_compartment_has_sso(admin, compartmentb, sso_compartmentb)), system_compartment_has_sso(system, compartmentb, sso_compartmentb)],extension(44,bind([[_18487, _18534], [compartmentb, sso_compartmentb]]))).
% 1.43/2.45 cnf('1.1.2.1.3.2.3.1',plain,[-(system_compartment_has_sso(system, compartmentb, sso_compartmentb))],extension(5)).
% 1.43/2.45 cnf('1.1.2.1.3.2.4',plain,[-(sso_compartment_has_scg(sso_compartmentb, compartmentb, scg_compartmentb))],extension(7)).
% 1.43/2.45 cnf('1.1.2.1.3.3',plain,[-(sso_file_has_citizenship(sso_compartmentb, secretfile, usa, scg_compartmentb))],extension(19)).
% 1.43/2.45 cnf('1.1.2.1.3.4',plain,[-(admin_file_has_citizenship_h(admin, secretfile, usa, cons(compartmenta, nil))), admin_compartment_has_sso(admin, compartmenta, sso_compartmenta), admin_compartment_has_scg(admin, compartmenta, scg_compartmenta), sso_file_has_citizenship(sso_compartmenta, secretfile, usa, scg_compartmenta), admin_file_has_citizenship_h(admin, secretfile, usa, nil)],extension(54,bind([[_25462, _25645, _25735, _25275, _25369, _25554], [compartmenta, sso_compartmenta, scg_compartmenta, secretfile, usa, nil]]))).
% 1.43/2.45 cnf('1.1.2.1.3.4.1',plain,[-(admin_compartment_has_sso(admin, compartmenta, sso_compartmenta)), system_compartment_has_sso(system, compartmenta, sso_compartmenta)],extension(44,bind([[_18487, _18534], [compartmenta, sso_compartmenta]]))).
% 1.43/2.45 cnf('1.1.2.1.3.4.1.1',plain,[-(system_compartment_has_sso(system, compartmenta, sso_compartmenta))],extension(8)).
% 1.43/2.45 cnf('1.1.2.1.3.4.2',plain,[-(admin_compartment_has_scg(admin, compartmenta, scg_compartmenta)), system_indi_is_oca(system, oca), oca_compartment_has_scg(oca, compartmenta, scg_compartmenta), admin_compartment_has_sso(admin, compartmenta, sso_compartmenta), sso_compartment_has_scg(sso_compartmenta, compartmenta, scg_compartmenta)],extension(45,bind([[_18881, _19034, _18958, _19109], [oca, sso_compartmenta, compartmenta, scg_compartmenta]]))).
% 1.43/2.45 cnf('1.1.2.1.3.4.2.1',plain,[-(system_indi_is_oca(system, oca))],extension(2)).
% 1.43/2.45 cnf('1.1.2.1.3.4.2.2',plain,[-(oca_compartment_has_scg(oca, compartmenta, scg_compartmenta))],extension(9)).
% 1.43/2.45 cnf('1.1.2.1.3.4.2.3',plain,[-(admin_compartment_has_sso(admin, compartmenta, sso_compartmenta)), system_compartment_has_sso(system, compartmenta, sso_compartmenta)],extension(44,bind([[_18487, _18534], [compartmenta, sso_compartmenta]]))).
% 1.43/2.45 cnf('1.1.2.1.3.4.2.3.1',plain,[-(system_compartment_has_sso(system, compartmenta, sso_compartmenta))],extension(8)).
% 1.43/2.45 cnf('1.1.2.1.3.4.2.4',plain,[-(sso_compartment_has_scg(sso_compartmenta, compartmenta, scg_compartmenta))],extension(10)).
% 1.43/2.45 cnf('1.1.2.1.3.4.3',plain,[-(sso_file_has_citizenship(sso_compartmenta, secretfile, usa, scg_compartmenta))],extension(20)).
% 1.43/2.45 cnf('1.1.2.1.3.4.4',plain,[-(admin_file_has_citizenship_h(admin, secretfile, usa, nil))],extension(53,bind([[_24967, _25008], [secretfile, usa]]))).
% 1.43/2.45 cnf('1.1.2.2',plain,[-(admin_indi_has_citizenship(admin, alice, usa)), system_indi_has_citizenship(system, alice, usa)],extension(60,bind([[_29047, _29094], [alice, usa]]))).
% 1.43/2.45 cnf('1.1.2.2.1',plain,[-(system_indi_has_citizenship(system, alice, usa))],extension(27)).
% 1.43/2.45 cnf('1.1.3',plain,[-(admin_indi_has_need_to_know_for_file(admin, alice, secretfile)), state_file_has_owner(secretfile, owner_secretfile), owner_indi_has_need_to_know(owner_secretfile, alice, secretfile)],extension(72,bind([[_41335, _41220, _41278], [owner_secretfile, alice, secretfile]]))).
% 1.43/2.45 cnf('1.1.3.1',plain,[-(state_file_has_owner(secretfile, owner_secretfile))],extension(21)).
% 1.43/2.45 cnf('1.1.3.2',plain,[-(owner_indi_has_need_to_know(owner_secretfile, alice, secretfile))],extension(38)).
% 1.43/2.45 cnf('1.1.4',plain,[-(admin_indi_has_level_for_file(admin, alice, secretfile)), admin_file_has_level(admin, secretfile, secret), admin_indi_has_level(admin, alice, secret)],extension(71,bind([[_40683, _40624, _40741], [secretfile, alice, secret]]))).
% 1.43/2.45 cnf('1.1.4.1',plain,[-(admin_file_has_level(admin, secretfile, secret)), system_file_needs_level(system, secretfile, secret), admin_file_has_compartments(admin, secretfile, cons(compartmentb, cons(compartmenta, nil))), admin_file_has_level_h(admin, secretfile, secret, cons(compartmentb, cons(compartmenta, nil)))],extension(49,bind([[_21734, _21801, _21867], [secretfile, secret, cons(compartmentb, cons(compartmenta, nil))]]))).
% 1.43/2.45 cnf('1.1.4.1.1',plain,[-(system_file_needs_level(system, secretfile, secret))],extension(15)).
% 1.43/2.45 cnf('1.1.4.1.2',plain,[-(admin_file_has_compartments(admin, secretfile, cons(compartmentb, cons(compartmenta, nil)))), system_file_needs_compartments(system, secretfile, cons(compartmentb, cons(compartmenta, nil))), admin_file_has_compartments_h(admin, secretfile, cons(compartmentb, cons(compartmenta, nil)), cons(compartmentb, cons(compartmenta, nil)))],extension(46,bind([[_19800, _19855], [secretfile, cons(compartmentb, cons(compartmenta, nil))]]))).
% 1.43/2.45 cnf('1.1.4.1.2.1',plain,[-(system_file_needs_compartments(system, secretfile, cons(compartmentb, cons(compartmenta, nil))))],extension(12)).
% 1.43/2.45 cnf('1.1.4.1.2.2',plain,[-(admin_file_has_compartments_h(admin, secretfile, cons(compartmentb, cons(compartmenta, nil)), cons(compartmentb, cons(compartmenta, nil)))), admin_compartment_has_sso(admin, compartmentb, sso_compartmentb), sso_file_has_compartments(sso_compartmentb, secretfile, cons(compartmentb, cons(compartmenta, nil))), admin_file_has_compartments_h(admin, secretfile, cons(compartmentb, cons(compartmenta, nil)), cons(compartmenta, nil))],extension(48,bind([[_20833, _20990, _20672, _20753, _20912], [compartmentb, sso_compartmentb, secretfile, cons(compartmentb, cons(compartmenta, nil)), cons(compartmenta, nil)]]))).
% 1.43/2.45 cnf('1.1.4.1.2.2.1',plain,[-(admin_compartment_has_sso(admin, compartmentb, sso_compartmentb)), system_compartment_has_sso(system, compartmentb, sso_compartmentb)],extension(44,bind([[_18487, _18534], [compartmentb, sso_compartmentb]]))).
% 1.43/2.45 cnf('1.1.4.1.2.2.1.1',plain,[-(system_compartment_has_sso(system, compartmentb, sso_compartmentb))],extension(5)).
% 1.43/2.45 cnf('1.1.4.1.2.2.2',plain,[-(sso_file_has_compartments(sso_compartmentb, secretfile, cons(compartmentb, cons(compartmenta, nil))))],extension(13)).
% 1.43/2.45 cnf('1.1.4.1.2.2.3',plain,[-(admin_file_has_compartments_h(admin, secretfile, cons(compartmentb, cons(compartmenta, nil)), cons(compartmenta, nil))), admin_compartment_has_sso(admin, compartmenta, sso_compartmenta), sso_file_has_compartments(sso_compartmenta, secretfile, cons(compartmentb, cons(compartmenta, nil))), admin_file_has_compartments_h(admin, secretfile, cons(compartmentb, cons(compartmenta, nil)), nil)],extension(48,bind([[_20833, _20990, _20672, _20753, _20912], [compartmenta, sso_compartmenta, secretfile, cons(compartmentb, cons(compartmenta, nil)), nil]]))).
% 1.43/2.45 cnf('1.1.4.1.2.2.3.1',plain,[-(admin_compartment_has_sso(admin, compartmenta, sso_compartmenta)), system_compartment_has_sso(system, compartmenta, sso_compartmenta)],extension(44,bind([[_18487, _18534], [compartmenta, sso_compartmenta]]))).
% 1.43/2.45 cnf('1.1.4.1.2.2.3.1.1',plain,[-(system_compartment_has_sso(system, compartmenta, sso_compartmenta))],extension(8)).
% 1.43/2.45 cnf('1.1.4.1.2.2.3.2',plain,[-(sso_file_has_compartments(sso_compartmenta, secretfile, cons(compartmentb, cons(compartmenta, nil))))],extension(14)).
% 1.43/2.45 cnf('1.1.4.1.2.2.3.3',plain,[-(admin_file_has_compartments_h(admin, secretfile, cons(compartmentb, cons(compartmenta, nil)), nil))],extension(47,bind([[_20364, _20405], [secretfile, cons(compartmentb, cons(compartmenta, nil))]]))).
% 1.43/2.45 cnf('1.1.4.1.3',plain,[-(admin_file_has_level_h(admin, secretfile, secret, cons(compartmentb, cons(compartmenta, nil)))), admin_compartment_has_sso(admin, compartmentb, sso_compartmentb), admin_compartment_has_scg(admin, compartmentb, scg_compartmentb), sso_file_has_level(sso_compartmentb, secretfile, secret, scg_compartmentb), admin_file_has_level_h(admin, secretfile, secret, cons(compartmenta, nil))],extension(51,bind([[_23003, _23186, _23276, _22816, _22910, _23095], [compartmentb, sso_compartmentb, scg_compartmentb, secretfile, secret, cons(compartmenta, nil)]]))).
% 1.43/2.45 cnf('1.1.4.1.3.1',plain,[-(admin_compartment_has_sso(admin, compartmentb, sso_compartmentb)), system_compartment_has_sso(system, compartmentb, sso_compartmentb)],extension(44,bind([[_18487, _18534], [compartmentb, sso_compartmentb]]))).
% 1.43/2.45 cnf('1.1.4.1.3.1.1',plain,[-(system_compartment_has_sso(system, compartmentb, sso_compartmentb))],extension(5)).
% 1.43/2.45 cnf('1.1.4.1.3.2',plain,[-(admin_compartment_has_scg(admin, compartmentb, scg_compartmentb)), system_indi_is_oca(system, oca), oca_compartment_has_scg(oca, compartmentb, scg_compartmentb), admin_compartment_has_sso(admin, compartmentb, sso_compartmentb), sso_compartment_has_scg(sso_compartmentb, compartmentb, scg_compartmentb)],extension(45,bind([[_18881, _19034, _18958, _19109], [oca, sso_compartmentb, compartmentb, scg_compartmentb]]))).
% 1.43/2.45 cnf('1.1.4.1.3.2.1',plain,[-(system_indi_is_oca(system, oca))],extension(2)).
% 1.43/2.45 cnf('1.1.4.1.3.2.2',plain,[-(oca_compartment_has_scg(oca, compartmentb, scg_compartmentb))],extension(6)).
% 1.43/2.45 cnf('1.1.4.1.3.2.3',plain,[-(admin_compartment_has_sso(admin, compartmentb, sso_compartmentb)), system_compartment_has_sso(system, compartmentb, sso_compartmentb)],extension(44,bind([[_18487, _18534], [compartmentb, sso_compartmentb]]))).
% 1.43/2.45 cnf('1.1.4.1.3.2.3.1',plain,[-(system_compartment_has_sso(system, compartmentb, sso_compartmentb))],extension(5)).
% 1.43/2.45 cnf('1.1.4.1.3.2.4',plain,[-(sso_compartment_has_scg(sso_compartmentb, compartmentb, scg_compartmentb))],extension(7)).
% 1.43/2.45 cnf('1.1.4.1.3.3',plain,[-(sso_file_has_level(sso_compartmentb, secretfile, secret, scg_compartmentb))],extension(16)).
% 1.43/2.45 cnf('1.1.4.1.3.4',plain,[-(admin_file_has_level_h(admin, secretfile, secret, cons(compartmenta, nil))), admin_compartment_has_sso(admin, compartmenta, sso_compartmenta), admin_compartment_has_scg(admin, compartmenta, scg_compartmenta), sso_file_has_level(sso_compartmenta, secretfile, secret, scg_compartmenta), admin_file_has_level_h(admin, secretfile, secret, nil)],extension(51,bind([[_23003, _23186, _23276, _22816, _22910, _23095], [compartmenta, sso_compartmenta, scg_compartmenta, secretfile, secret, nil]]))).
% 1.43/2.45 cnf('1.1.4.1.3.4.1',plain,[-(admin_compartment_has_sso(admin, compartmenta, sso_compartmenta)), system_compartment_has_sso(system, compartmenta, sso_compartmenta)],extension(44,bind([[_18487, _18534], [compartmenta, sso_compartmenta]]))).
% 1.43/2.45 cnf('1.1.4.1.3.4.1.1',plain,[-(system_compartment_has_sso(system, compartmenta, sso_compartmenta))],extension(8)).
% 1.43/2.45 cnf('1.1.4.1.3.4.2',plain,[-(admin_compartment_has_scg(admin, compartmenta, scg_compartmenta)), system_indi_is_oca(system, oca), oca_compartment_has_scg(oca, compartmenta, scg_compartmenta), admin_compartment_has_sso(admin, compartmenta, sso_compartmenta), sso_compartment_has_scg(sso_compartmenta, compartmenta, scg_compartmenta)],extension(45,bind([[_18881, _19034, _18958, _19109], [oca, sso_compartmenta, compartmenta, scg_compartmenta]]))).
% 1.43/2.45 cnf('1.1.4.1.3.4.2.1',plain,[-(system_indi_is_oca(system, oca))],extension(2)).
% 1.43/2.45 cnf('1.1.4.1.3.4.2.2',plain,[-(oca_compartment_has_scg(oca, compartmenta, scg_compartmenta))],extension(9)).
% 1.43/2.45 cnf('1.1.4.1.3.4.2.3',plain,[-(admin_compartment_has_sso(admin, compartmenta, sso_compartmenta)), system_compartment_has_sso(system, compartmenta, sso_compartmenta)],extension(44,bind([[_18487, _18534], [compartmenta, sso_compartmenta]]))).
% 1.43/2.45 cnf('1.1.4.1.3.4.2.3.1',plain,[-(system_compartment_has_sso(system, compartmenta, sso_compartmenta))],extension(8)).
% 1.43/2.45 cnf('1.1.4.1.3.4.2.4',plain,[-(sso_compartment_has_scg(sso_compartmenta, compartmenta, scg_compartmenta))],extension(10)).
% 1.43/2.45 cnf('1.1.4.1.3.4.3',plain,[-(sso_file_has_level(sso_compartmenta, secretfile, secret, scg_compartmenta))],extension(17)).
% 1.43/2.45 cnf('1.1.4.1.3.4.4',plain,[-(admin_file_has_level_h(admin, secretfile, secret, nil))],extension(50,bind([[_22508, _22549], [secretfile, secret]]))).
% 1.43/2.45 cnf('1.1.4.2',plain,[-(admin_indi_has_level(admin, alice, secret)), system_indi_needs_level(system, alice, secret), admin_indi_has_citizenship(admin, alice, usa), admin_indi_has_polygraph(admin, alice), admin_indi_has_employment(admin, alice), admin_indi_has_credit(admin, alice), loca_level_below(admin, secret, secret), system_indi_is_level_admin(system, level_admin), level_admin_indi_has_level(level_admin, alice, topsecret), loca_level_below(admin, secret, topsecret), admin_indi_has_background(admin, alice, secret)],extension(61,bind([[_29897, _30016, _30134, _29656, _29777], [secret, level_admin, topsecret, alice, secret]]))).
% 1.43/2.45 cnf('1.1.4.2.1',plain,[-(system_indi_needs_level(system, alice, secret))],extension(32)).
% 1.43/2.45 cnf('1.1.4.2.2',plain,[-(admin_indi_has_citizenship(admin, alice, usa)), system_indi_has_citizenship(system, alice, usa)],extension(60,bind([[_29047, _29094], [alice, usa]]))).
% 1.43/2.45 cnf('1.1.4.2.2.1',plain,[-(system_indi_has_citizenship(system, alice, usa))],extension(27)).
% 1.43/2.45 cnf('1.1.4.2.3',plain,[-(admin_indi_has_polygraph(admin, alice)), system_indi_is_polygraph_admin(system, polygraph_admin), polygraph_admin_indi_has_polygraph(polygraph_admin, alice)],extension(55,bind([[_26703, _26652], [polygraph_admin, alice]]))).
% 1.43/2.45 cnf('1.1.4.2.3.1',plain,[-(system_indi_is_polygraph_admin(system, polygraph_admin))],extension(22)).
% 1.43/2.45 cnf('1.1.4.2.3.2',plain,[-(polygraph_admin_indi_has_polygraph(polygraph_admin, alice))],extension(28)).
% 1.43/2.45 cnf('1.1.4.2.4',plain,[-(admin_indi_has_employment(admin, alice)), system_indi_is_hr_admin(system, hr_admin), hr_admin_indi_has_employment(hr_admin, alice)],extension(59,bind([[_28487, _28436], [hr_admin, alice]]))).
% 1.43/2.45 cnf('1.1.4.2.4.1',plain,[-(system_indi_is_hr_admin(system, hr_admin))],extension(25)).
% 1.43/2.45 cnf('1.1.4.2.4.2',plain,[-(hr_admin_indi_has_employment(hr_admin, alice))],extension(31)).
% 1.43/2.45 cnf('1.1.4.2.5',plain,[-(admin_indi_has_credit(admin, alice)), system_indi_is_credit_admin(system, credit_admin), credit_admin_indi_has_credit(credit_admin, alice)],extension(56,bind([[_27099, _27048], [credit_admin, alice]]))).
% 1.43/2.45 cnf('1.1.4.2.5.1',plain,[-(system_indi_is_credit_admin(system, credit_admin))],extension(23)).
% 1.43/2.45 cnf('1.1.4.2.5.2',plain,[-(credit_admin_indi_has_credit(credit_admin, alice))],extension(29)).
% 1.43/2.45 cnf('1.1.4.2.6',plain,[-(loca_level_below(admin, secret, secret))],extension(42,bind([[_17542, _17582], [admin, secret]]))).
% 1.43/2.45 cnf('1.1.4.2.7',plain,[-(system_indi_is_level_admin(system, level_admin))],extension(26)).
% 1.43/2.45 cnf('1.1.4.2.8',plain,[-(level_admin_indi_has_level(level_admin, alice, topsecret))],extension(33)).
% 1.43/2.45 cnf('1.1.4.2.9',plain,[-(loca_level_below(admin, secret, topsecret)), loca_level_direct_below(admin, secret, topsecret), loca_level_below(admin, secret, secret)],extension(43,bind([[_17997, _17808, _17872, _17935], [topsecret, admin, secret, secret]]))).
% 1.43/2.45 cnf('1.1.4.2.9.1',plain,[-(loca_level_direct_below(admin, secret, topsecret))],extension(41,bind([[_17327], [admin]]))).
% 1.43/2.45 cnf('1.1.4.2.9.2',plain,[-(loca_level_below(admin, secret, secret))],extension(42,bind([[_17542, _17582], [admin, secret]]))).
% 1.43/2.45 cnf('1.1.4.2.10',plain,[-(admin_indi_has_background(admin, alice, secret)), system_indi_is_background_admin(system, background_admin), background_admin_indi_has_background(background_admin, alice, topsecret), loca_level_below(admin, secret, topsecret)],extension(58,bind([[_27798, _27659, _27729, _27866], [background_admin, alice, secret, topsecret]]))).
% 1.43/2.45 cnf('1.1.4.2.10.1',plain,[-(system_indi_is_background_admin(system, background_admin))],extension(24)).
% 1.43/2.45 cnf('1.1.4.2.10.2',plain,[-(background_admin_indi_has_background(background_admin, alice, topsecret))],extension(30)).
% 1.43/2.45 cnf('1.1.4.2.10.3',plain,[-(loca_level_below(admin, secret, topsecret))],lemmata('1.1.4.2')).
% 1.43/2.45 cnf('1.1.5',plain,[-(admin_indi_has_compartments_for_file(admin, alice, secretfile)), admin_file_has_compartments(admin, secretfile, cons(compartmentb, cons(compartmenta, nil))), admin_indi_has_compartments(admin, alice, cons(compartmentb, cons(compartmenta, nil)))],extension(70,bind([[_40087, _40028, _40145], [secretfile, alice, cons(compartmentb, cons(compartmenta, nil))]]))).
% 1.43/2.45 cnf('1.1.5.1',plain,[-(admin_file_has_compartments(admin, secretfile, cons(compartmentb, cons(compartmenta, nil)))), system_file_needs_compartments(system, secretfile, cons(compartmentb, cons(compartmenta, nil))), admin_file_has_compartments_h(admin, secretfile, cons(compartmentb, cons(compartmenta, nil)), cons(compartmentb, cons(compartmenta, nil)))],extension(46,bind([[_19800, _19855], [secretfile, cons(compartmentb, cons(compartmenta, nil))]]))).
% 1.43/2.45 cnf('1.1.5.1.1',plain,[-(system_file_needs_compartments(system, secretfile, cons(compartmentb, cons(compartmenta, nil))))],extension(12)).
% 1.43/2.45 cnf('1.1.5.1.2',plain,[-(admin_file_has_compartments_h(admin, secretfile, cons(compartmentb, cons(compartmenta, nil)), cons(compartmentb, cons(compartmenta, nil)))), admin_compartment_has_sso(admin, compartmentb, sso_compartmentb), sso_file_has_compartments(sso_compartmentb, secretfile, cons(compartmentb, cons(compartmenta, nil))), admin_file_has_compartments_h(admin, secretfile, cons(compartmentb, cons(compartmenta, nil)), cons(compartmenta, nil))],extension(48,bind([[_20833, _20990, _20672, _20753, _20912], [compartmentb, sso_compartmentb, secretfile, cons(compartmentb, cons(compartmenta, nil)), cons(compartmenta, nil)]]))).
% 1.43/2.45 cnf('1.1.5.1.2.1',plain,[-(admin_compartment_has_sso(admin, compartmentb, sso_compartmentb)), system_compartment_has_sso(system, compartmentb, sso_compartmentb)],extension(44,bind([[_18487, _18534], [compartmentb, sso_compartmentb]]))).
% 1.43/2.45 cnf('1.1.5.1.2.1.1',plain,[-(system_compartment_has_sso(system, compartmentb, sso_compartmentb))],extension(5)).
% 1.43/2.45 cnf('1.1.5.1.2.2',plain,[-(sso_file_has_compartments(sso_compartmentb, secretfile, cons(compartmentb, cons(compartmenta, nil))))],extension(13)).
% 1.43/2.45 cnf('1.1.5.1.2.3',plain,[-(admin_file_has_compartments_h(admin, secretfile, cons(compartmentb, cons(compartmenta, nil)), cons(compartmenta, nil))), admin_compartment_has_sso(admin, compartmenta, sso_compartmenta), sso_file_has_compartments(sso_compartmenta, secretfile, cons(compartmentb, cons(compartmenta, nil))), admin_file_has_compartments_h(admin, secretfile, cons(compartmentb, cons(compartmenta, nil)), nil)],extension(48,bind([[_20833, _20990, _20672, _20753, _20912], [compartmenta, sso_compartmenta, secretfile, cons(compartmentb, cons(compartmenta, nil)), nil]]))).
% 1.43/2.45 cnf('1.1.5.1.2.3.1',plain,[-(admin_compartment_has_sso(admin, compartmenta, sso_compartmenta)), system_compartment_has_sso(system, compartmenta, sso_compartmenta)],extension(44,bind([[_18487, _18534], [compartmenta, sso_compartmenta]]))).
% 1.43/2.45 cnf('1.1.5.1.2.3.1.1',plain,[-(system_compartment_has_sso(system, compartmenta, sso_compartmenta))],extension(8)).
% 1.43/2.45 cnf('1.1.5.1.2.3.2',plain,[-(sso_file_has_compartments(sso_compartmenta, secretfile, cons(compartmentb, cons(compartmenta, nil))))],extension(14)).
% 1.43/2.45 cnf('1.1.5.1.2.3.3',plain,[-(admin_file_has_compartments_h(admin, secretfile, cons(compartmentb, cons(compartmenta, nil)), nil))],extension(47,bind([[_20364, _20405], [secretfile, cons(compartmentb, cons(compartmenta, nil))]]))).
% 1.43/2.45 cnf('1.1.5.2',plain,[-(admin_indi_has_compartments(admin, alice, cons(compartmentb, cons(compartmenta, nil)))), system_indi_needs_compartment(system, alice, compartmentb), admin_indi_has_employment(admin, alice), admin_indi_has_citizenship(admin, alice, usa), admin_indi_has_polygraph_for_compartment(admin, alice, compartmentb), admin_indi_has_credit_for_compartment(admin, alice, compartmentb), admin_compartment_has_sso(admin, compartmentb, sso_compartmentb), sso_indi_has_compartment(sso_compartmentb, alice, compartmentb), admin_indi_has_background_for_compartment(admin, alice, compartmentb), admin_indi_has_level_for_compartment(admin, alice, compartmentb), admin_indi_has_compartments(admin, alice, cons(compartmenta, nil))],extension(63,bind([[_32017, _31776, _31654, _31897], [sso_compartmentb, compartmentb, alice, cons(compartmenta, nil)]]))).
% 1.43/2.45 cnf('1.1.5.2.1',plain,[-(system_indi_needs_compartment(system, alice, compartmentb))],extension(34)).
% 1.43/2.45 cnf('1.1.5.2.2',plain,[-(admin_indi_has_employment(admin, alice)), system_indi_is_hr_admin(system, hr_admin), hr_admin_indi_has_employment(hr_admin, alice)],extension(59,bind([[_28487, _28436], [hr_admin, alice]]))).
% 1.43/2.45 cnf('1.1.5.2.2.1',plain,[-(system_indi_is_hr_admin(system, hr_admin))],extension(25)).
% 1.43/2.45 cnf('1.1.5.2.2.2',plain,[-(hr_admin_indi_has_employment(hr_admin, alice))],extension(31)).
% 1.43/2.45 cnf('1.1.5.2.3',plain,[-(admin_indi_has_citizenship(admin, alice, usa)), system_indi_has_citizenship(system, alice, usa)],extension(60,bind([[_29047, _29094], [alice, usa]]))).
% 1.43/2.45 cnf('1.1.5.2.3.1',plain,[-(system_indi_has_citizenship(system, alice, usa))],extension(27)).
% 1.43/2.45 cnf('1.1.5.2.4',plain,[-(admin_indi_has_polygraph_for_compartment(admin, alice, compartmentb)), system_indi_is_oca(system, oca), oca_compartment_is_compartment(oca, compartmentb, confidential, topsecret, yes, yes), admin_indi_has_polygraph(admin, alice)],extension(66,bind([[_36115, _36034, _36195, _36274, _36352, _35952], [oca, compartmentb, confidential, topsecret, yes, alice]]))).
% 1.43/2.45 cnf('1.1.5.2.4.1',plain,[-(system_indi_is_oca(system, oca))],extension(2)).
% 1.43/2.45 cnf('1.1.5.2.4.2',plain,[-(oca_compartment_is_compartment(oca, compartmentb, confidential, topsecret, yes, yes))],extension(3)).
% 1.43/2.45 cnf('1.1.5.2.4.3',plain,[-(admin_indi_has_polygraph(admin, alice)), system_indi_is_polygraph_admin(system, polygraph_admin), polygraph_admin_indi_has_polygraph(polygraph_admin, alice)],extension(55,bind([[_26703, _26652], [polygraph_admin, alice]]))).
% 1.43/2.45 cnf('1.1.5.2.4.3.1',plain,[-(system_indi_is_polygraph_admin(system, polygraph_admin))],extension(22)).
% 1.43/2.45 cnf('1.1.5.2.4.3.2',plain,[-(polygraph_admin_indi_has_polygraph(polygraph_admin, alice))],extension(28)).
% 1.43/2.45 cnf('1.1.5.2.5',plain,[-(admin_indi_has_credit_for_compartment(admin, alice, compartmentb)), system_indi_is_oca(system, oca), oca_compartment_is_compartment(oca, compartmentb, confidential, topsecret, yes, yes), admin_indi_has_credit(admin, alice)],extension(68,bind([[_38153, _38072, _38233, _38312, _38390, _37990], [oca, compartmentb, confidential, topsecret, yes, alice]]))).
% 1.43/2.45 cnf('1.1.5.2.5.1',plain,[-(system_indi_is_oca(system, oca))],extension(2)).
% 1.43/2.45 cnf('1.1.5.2.5.2',plain,[-(oca_compartment_is_compartment(oca, compartmentb, confidential, topsecret, yes, yes))],extension(3)).
% 1.43/2.45 cnf('1.1.5.2.5.3',plain,[-(admin_indi_has_credit(admin, alice)), system_indi_is_credit_admin(system, credit_admin), credit_admin_indi_has_credit(credit_admin, alice)],extension(56,bind([[_27099, _27048], [credit_admin, alice]]))).
% 1.43/2.45 cnf('1.1.5.2.5.3.1',plain,[-(system_indi_is_credit_admin(system, credit_admin))],extension(23)).
% 1.43/2.45 cnf('1.1.5.2.5.3.2',plain,[-(credit_admin_indi_has_credit(credit_admin, alice))],extension(29)).
% 1.43/2.45 cnf('1.1.5.2.6',plain,[-(admin_compartment_has_sso(admin, compartmentb, sso_compartmentb)), system_compartment_has_sso(system, compartmentb, sso_compartmentb)],extension(44,bind([[_18487, _18534], [compartmentb, sso_compartmentb]]))).
% 1.43/2.45 cnf('1.1.5.2.6.1',plain,[-(system_compartment_has_sso(system, compartmentb, sso_compartmentb))],extension(5)).
% 1.43/2.45 cnf('1.1.5.2.7',plain,[-(sso_indi_has_compartment(sso_compartmentb, alice, compartmentb))],extension(36)).
% 1.43/2.45 cnf('1.1.5.2.8',plain,[-(admin_indi_has_background_for_compartment(admin, alice, compartmentb)), system_indi_is_oca(system, oca), oca_compartment_is_compartment(oca, compartmentb, confidential, topsecret, yes, yes), admin_indi_has_background(admin, alice, topsecret)],extension(64,bind([[_33649, _33562, _33735, _33904, _33987, _33474, _33820], [oca, compartmentb, confidential, yes, yes, alice, topsecret]]))).
% 1.43/2.45 cnf('1.1.5.2.8.1',plain,[-(system_indi_is_oca(system, oca))],extension(2)).
% 1.43/2.45 cnf('1.1.5.2.8.2',plain,[-(oca_compartment_is_compartment(oca, compartmentb, confidential, topsecret, yes, yes))],extension(3)).
% 1.43/2.45 cnf('1.1.5.2.8.3',plain,[-(admin_indi_has_background(admin, alice, topsecret)), system_indi_is_background_admin(system, background_admin), background_admin_indi_has_background(background_admin, alice, topsecret), loca_level_below(admin, topsecret, topsecret)],extension(58,bind([[_27798, _27659, _27729, _27866], [background_admin, alice, topsecret, topsecret]]))).
% 1.43/2.45 cnf('1.1.5.2.8.3.1',plain,[-(system_indi_is_background_admin(system, background_admin))],extension(24)).
% 1.43/2.45 cnf('1.1.5.2.8.3.2',plain,[-(background_admin_indi_has_background(background_admin, alice, topsecret))],extension(30)).
% 1.43/2.45 cnf('1.1.5.2.8.3.3',plain,[-(loca_level_below(admin, topsecret, topsecret))],extension(42,bind([[_17542, _17582], [admin, topsecret]]))).
% 1.43/2.45 cnf('1.1.5.2.9',plain,[-(admin_indi_has_level_for_compartment(admin, alice, compartmentb)), system_indi_is_oca(system, oca), oca_compartment_is_compartment(oca, compartmentb, confidential, topsecret, yes, yes), admin_indi_has_level(admin, alice, confidential)],extension(65,bind([[_34888, _34801, _35059, _35143, _35226, _34713, _34974], [oca, compartmentb, topsecret, yes, yes, alice, confidential]]))).
% 1.43/2.45 cnf('1.1.5.2.9.1',plain,[-(system_indi_is_oca(system, oca))],extension(2)).
% 1.43/2.45 cnf('1.1.5.2.9.2',plain,[-(oca_compartment_is_compartment(oca, compartmentb, confidential, topsecret, yes, yes))],extension(3)).
% 1.43/2.45 cnf('1.1.5.2.9.3',plain,[-(admin_indi_has_level(admin, alice, confidential)), system_indi_needs_level(system, alice, secret), admin_indi_has_citizenship(admin, alice, usa), admin_indi_has_polygraph(admin, alice), admin_indi_has_employment(admin, alice), admin_indi_has_credit(admin, alice), loca_level_below(admin, confidential, secret), system_indi_is_level_admin(system, level_admin), level_admin_indi_has_level(level_admin, alice, topsecret), loca_level_below(admin, confidential, topsecret), admin_indi_has_background(admin, alice, confidential)],extension(61,bind([[_29897, _30016, _30134, _29656, _29777], [secret, level_admin, topsecret, alice, confidential]]))).
% 1.43/2.45 cnf('1.1.5.2.9.3.1',plain,[-(system_indi_needs_level(system, alice, secret))],extension(32)).
% 1.43/2.45 cnf('1.1.5.2.9.3.2',plain,[-(admin_indi_has_citizenship(admin, alice, usa))],lemmata('1.1.5.2')).
% 1.43/2.45 cnf('1.1.5.2.9.3.3',plain,[-(admin_indi_has_polygraph(admin, alice)), system_indi_is_polygraph_admin(system, polygraph_admin), polygraph_admin_indi_has_polygraph(polygraph_admin, alice)],extension(55,bind([[_26703, _26652], [polygraph_admin, alice]]))).
% 1.43/2.45 cnf('1.1.5.2.9.3.3.1',plain,[-(system_indi_is_polygraph_admin(system, polygraph_admin))],extension(22)).
% 1.43/2.45 cnf('1.1.5.2.9.3.3.2',plain,[-(polygraph_admin_indi_has_polygraph(polygraph_admin, alice))],extension(28)).
% 1.43/2.45 cnf('1.1.5.2.9.3.4',plain,[-(admin_indi_has_employment(admin, alice))],lemmata('1.1.5.2')).
% 1.43/2.45 cnf('1.1.5.2.9.3.5',plain,[-(admin_indi_has_credit(admin, alice)), system_indi_is_credit_admin(system, credit_admin), credit_admin_indi_has_credit(credit_admin, alice)],extension(56,bind([[_27099, _27048], [credit_admin, alice]]))).
% 1.43/2.45 cnf('1.1.5.2.9.3.5.1',plain,[-(system_indi_is_credit_admin(system, credit_admin))],extension(23)).
% 1.43/2.45 cnf('1.1.5.2.9.3.5.2',plain,[-(credit_admin_indi_has_credit(credit_admin, alice))],extension(29)).
% 1.43/2.45 cnf('1.1.5.2.9.3.6',plain,[-(loca_level_below(admin, confidential, secret)), loca_level_direct_below(admin, confidential, secret), loca_level_below(admin, confidential, confidential)],extension(43,bind([[_17997, _17808, _17872, _17935], [secret, admin, confidential, confidential]]))).
% 1.43/2.45 cnf('1.1.5.2.9.3.6.1',plain,[-(loca_level_direct_below(admin, confidential, secret))],extension(40,bind([[_17112], [admin]]))).
% 1.43/2.45 cnf('1.1.5.2.9.3.6.2',plain,[-(loca_level_below(admin, confidential, confidential))],extension(42,bind([[_17542, _17582], [admin, confidential]]))).
% 1.43/2.45 cnf('1.1.5.2.9.3.7',plain,[-(system_indi_is_level_admin(system, level_admin))],extension(26)).
% 1.43/2.45 cnf('1.1.5.2.9.3.8',plain,[-(level_admin_indi_has_level(level_admin, alice, topsecret))],extension(33)).
% 1.43/2.45 cnf('1.1.5.2.9.3.9',plain,[-(loca_level_below(admin, confidential, topsecret)), loca_level_direct_below(admin, secret, topsecret), loca_level_below(admin, confidential, secret)],extension(43,bind([[_17997, _17808, _17872, _17935], [topsecret, admin, confidential, secret]]))).
% 1.43/2.45 cnf('1.1.5.2.9.3.9.1',plain,[-(loca_level_direct_below(admin, secret, topsecret))],extension(41,bind([[_17327], [admin]]))).
% 1.43/2.45 cnf('1.1.5.2.9.3.9.2',plain,[-(loca_level_below(admin, confidential, secret))],lemmata('1.1.5.2.9.3')).
% 1.43/2.45 cnf('1.1.5.2.9.3.10',plain,[-(admin_indi_has_background(admin, alice, confidential)), system_indi_is_background_admin(system, background_admin), background_admin_indi_has_background(background_admin, alice, topsecret), loca_level_below(admin, confidential, topsecret)],extension(58,bind([[_27798, _27659, _27729, _27866], [background_admin, alice, confidential, topsecret]]))).
% 1.43/2.45 cnf('1.1.5.2.9.3.10.1',plain,[-(system_indi_is_background_admin(system, background_admin))],extension(24)).
% 1.43/2.45 cnf('1.1.5.2.9.3.10.2',plain,[-(background_admin_indi_has_background(background_admin, alice, topsecret))],extension(30)).
% 1.43/2.45 cnf('1.1.5.2.9.3.10.3',plain,[-(loca_level_below(admin, confidential, topsecret))],lemmata('1.1.5.2.9.3')).
% 1.43/2.45 cnf('1.1.5.2.10',plain,[-(admin_indi_has_compartments(admin, alice, cons(compartmenta, nil))), system_indi_needs_compartment(system, alice, compartmenta), admin_indi_has_employment(admin, alice), admin_indi_has_citizenship(admin, alice, usa), admin_indi_has_polygraph_for_compartment(admin, alice, compartmenta), admin_indi_has_credit_for_compartment(admin, alice, compartmenta), admin_compartment_has_sso(admin, compartmenta, sso_compartmenta), sso_indi_has_compartment(sso_compartmenta, alice, compartmenta), admin_indi_has_background_for_compartment(admin, alice, compartmenta), admin_indi_has_level_for_compartment(admin, alice, compartmenta), admin_indi_has_compartments(admin, alice, nil)],extension(63,bind([[_32017, _31776, _31654, _31897], [sso_compartmenta, compartmenta, alice, nil]]))).
% 1.43/2.45 cnf('1.1.5.2.10.1',plain,[-(system_indi_needs_compartment(system, alice, compartmenta))],extension(35)).
% 1.43/2.45 cnf('1.1.5.2.10.2',plain,[-(admin_indi_has_employment(admin, alice))],lemmata('1.1.5.2')).
% 1.43/2.45 cnf('1.1.5.2.10.3',plain,[-(admin_indi_has_citizenship(admin, alice, usa))],lemmata('1.1.5.2')).
% 1.43/2.45 cnf('1.1.5.2.10.4',plain,[-(admin_indi_has_polygraph_for_compartment(admin, alice, compartmenta)), system_indi_is_oca(system, oca), oca_compartment_is_compartment(oca, compartmenta, sbu, unclassified, no, no)],extension(67,bind([[_37026, _37177, _37102, _37251, _37324, _37396], [alice, oca, compartmenta, sbu, unclassified, no]]))).
% 1.43/2.45 cnf('1.1.5.2.10.4.1',plain,[-(system_indi_is_oca(system, oca))],extension(2)).
% 1.43/2.45 cnf('1.1.5.2.10.4.2',plain,[-(oca_compartment_is_compartment(oca, compartmenta, sbu, unclassified, no, no))],extension(4)).
% 1.43/2.45 cnf('1.1.5.2.10.5',plain,[-(admin_indi_has_credit_for_compartment(admin, alice, compartmenta)), system_indi_is_oca(system, oca), oca_compartment_is_compartment(oca, compartmenta, sbu, unclassified, no, no)],extension(69,bind([[_39064, _39215, _39140, _39289, _39362, _39434], [alice, oca, compartmenta, sbu, unclassified, no]]))).
% 1.43/2.45 cnf('1.1.5.2.10.5.1',plain,[-(system_indi_is_oca(system, oca))],extension(2)).
% 1.43/2.45 cnf('1.1.5.2.10.5.2',plain,[-(oca_compartment_is_compartment(oca, compartmenta, sbu, unclassified, no, no))],extension(4)).
% 1.43/2.45 cnf('1.1.5.2.10.6',plain,[-(admin_compartment_has_sso(admin, compartmenta, sso_compartmenta)), system_compartment_has_sso(system, compartmenta, sso_compartmenta)],extension(44,bind([[_18487, _18534], [compartmenta, sso_compartmenta]]))).
% 1.43/2.45 cnf('1.1.5.2.10.6.1',plain,[-(system_compartment_has_sso(system, compartmenta, sso_compartmenta))],extension(8)).
% 1.43/2.45 cnf('1.1.5.2.10.7',plain,[-(sso_indi_has_compartment(sso_compartmenta, alice, compartmenta))],extension(37)).
% 1.43/2.45 cnf('1.1.5.2.10.8',plain,[-(admin_indi_has_background_for_compartment(admin, alice, compartmenta)), system_indi_is_oca(system, oca), oca_compartment_is_compartment(oca, compartmenta, sbu, unclassified, no, no), admin_indi_has_background(admin, alice, unclassified)],extension(64,bind([[_33649, _33562, _33735, _33904, _33987, _33474, _33820], [oca, compartmenta, sbu, no, no, alice, unclassified]]))).
% 1.43/2.45 cnf('1.1.5.2.10.8.1',plain,[-(system_indi_is_oca(system, oca))],extension(2)).
% 1.43/2.45 cnf('1.1.5.2.10.8.2',plain,[-(oca_compartment_is_compartment(oca, compartmenta, sbu, unclassified, no, no))],extension(4)).
% 1.43/2.45 cnf('1.1.5.2.10.8.3',plain,[-(admin_indi_has_background(admin, alice, unclassified))],extension(57,bind([[_27444], [alice]]))).
% 1.43/2.45 cnf('1.1.5.2.10.9',plain,[-(admin_indi_has_level_for_compartment(admin, alice, compartmenta)), system_indi_is_oca(system, oca), oca_compartment_is_compartment(oca, compartmenta, sbu, unclassified, no, no), admin_indi_has_level(admin, alice, sbu)],extension(65,bind([[_34888, _34801, _35059, _35143, _35226, _34713, _34974], [oca, compartmenta, unclassified, no, no, alice, sbu]]))).
% 1.43/2.45 cnf('1.1.5.2.10.9.1',plain,[-(system_indi_is_oca(system, oca))],extension(2)).
% 1.43/2.45 cnf('1.1.5.2.10.9.2',plain,[-(oca_compartment_is_compartment(oca, compartmenta, sbu, unclassified, no, no))],extension(4)).
% 1.43/2.45 cnf('1.1.5.2.10.9.3',plain,[-(admin_indi_has_level(admin, alice, sbu)), system_indi_needs_level(system, alice, secret), admin_indi_has_citizenship(admin, alice, usa), admin_indi_has_polygraph(admin, alice), admin_indi_has_employment(admin, alice), admin_indi_has_credit(admin, alice), loca_level_below(admin, sbu, secret), system_indi_is_level_admin(system, level_admin), level_admin_indi_has_level(level_admin, alice, topsecret), loca_level_below(admin, sbu, topsecret), admin_indi_has_background(admin, alice, sbu)],extension(61,bind([[_29897, _30016, _30134, _29656, _29777], [secret, level_admin, topsecret, alice, sbu]]))).
% 1.43/2.45 cnf('1.1.5.2.10.9.3.1',plain,[-(system_indi_needs_level(system, alice, secret))],extension(32)).
% 1.43/2.45 cnf('1.1.5.2.10.9.3.2',plain,[-(admin_indi_has_citizenship(admin, alice, usa))],lemmata('1.1.5.2.10')).
% 1.43/2.45 cnf('1.1.5.2.10.9.3.3',plain,[-(admin_indi_has_polygraph(admin, alice)), system_indi_is_polygraph_admin(system, polygraph_admin), polygraph_admin_indi_has_polygraph(polygraph_admin, alice)],extension(55,bind([[_26703, _26652], [polygraph_admin, alice]]))).
% 1.43/2.45 cnf('1.1.5.2.10.9.3.3.1',plain,[-(system_indi_is_polygraph_admin(system, polygraph_admin))],extension(22)).
% 1.43/2.45 cnf('1.1.5.2.10.9.3.3.2',plain,[-(polygraph_admin_indi_has_polygraph(polygraph_admin, alice))],extension(28)).
% 1.43/2.45 cnf('1.1.5.2.10.9.3.4',plain,[-(admin_indi_has_employment(admin, alice))],lemmata('1.1.5.2.10')).
% 1.43/2.45 cnf('1.1.5.2.10.9.3.5',plain,[-(admin_indi_has_credit(admin, alice)), system_indi_is_credit_admin(system, credit_admin), credit_admin_indi_has_credit(credit_admin, alice)],extension(56,bind([[_27099, _27048], [credit_admin, alice]]))).
% 1.43/2.45 cnf('1.1.5.2.10.9.3.5.1',plain,[-(system_indi_is_credit_admin(system, credit_admin))],extension(23)).
% 1.43/2.45 cnf('1.1.5.2.10.9.3.5.2',plain,[-(credit_admin_indi_has_credit(credit_admin, alice))],extension(29)).
% 1.43/2.45 cnf('1.1.5.2.10.9.3.6',plain,[-(loca_level_below(admin, sbu, secret)), loca_level_direct_below(admin, confidential, secret), loca_level_below(admin, sbu, confidential)],extension(43,bind([[_17997, _17808, _17872, _17935], [secret, admin, sbu, confidential]]))).
% 1.43/2.45 cnf('1.1.5.2.10.9.3.6.1',plain,[-(loca_level_direct_below(admin, confidential, secret))],extension(40,bind([[_17112], [admin]]))).
% 1.43/2.45 cnf('1.1.5.2.10.9.3.6.2',plain,[-(loca_level_below(admin, sbu, confidential)), loca_level_direct_below(admin, sbu, confidential), loca_level_below(admin, sbu, sbu)],extension(43,bind([[_17997, _17808, _17872, _17935], [confidential, admin, sbu, sbu]]))).
% 1.43/2.45 cnf('1.1.5.2.10.9.3.6.2.1',plain,[-(loca_level_direct_below(admin, sbu, confidential))],extension(39,bind([[_16897], [admin]]))).
% 1.43/2.45 cnf('1.1.5.2.10.9.3.6.2.2',plain,[-(loca_level_below(admin, sbu, sbu))],extension(42,bind([[_17542, _17582], [admin, sbu]]))).
% 1.43/2.45 cnf('1.1.5.2.10.9.3.7',plain,[-(system_indi_is_level_admin(system, level_admin))],extension(26)).
% 1.43/2.45 cnf('1.1.5.2.10.9.3.8',plain,[-(level_admin_indi_has_level(level_admin, alice, topsecret))],extension(33)).
% 1.43/2.45 cnf('1.1.5.2.10.9.3.9',plain,[-(loca_level_below(admin, sbu, topsecret)), loca_level_direct_below(admin, secret, topsecret), loca_level_below(admin, sbu, secret)],extension(43,bind([[_17997, _17808, _17872, _17935], [topsecret, admin, sbu, secret]]))).
% 1.43/2.45 cnf('1.1.5.2.10.9.3.9.1',plain,[-(loca_level_direct_below(admin, secret, topsecret))],extension(41,bind([[_17327], [admin]]))).
% 1.43/2.45 cnf('1.1.5.2.10.9.3.9.2',plain,[-(loca_level_below(admin, sbu, secret))],lemmata('1.1.5.2.10.9.3')).
% 1.43/2.45 cnf('1.1.5.2.10.9.3.10',plain,[-(admin_indi_has_background(admin, alice, sbu)), system_indi_is_background_admin(system, background_admin), background_admin_indi_has_background(background_admin, alice, topsecret), loca_level_below(admin, sbu, topsecret)],extension(58,bind([[_27798, _27659, _27729, _27866], [background_admin, alice, sbu, topsecret]]))).
% 1.43/2.45 cnf('1.1.5.2.10.9.3.10.1',plain,[-(system_indi_is_background_admin(system, background_admin))],extension(24)).
% 1.43/2.45 cnf('1.1.5.2.10.9.3.10.2',plain,[-(background_admin_indi_has_background(background_admin, alice, topsecret))],extension(30)).
% 1.43/2.45 cnf('1.1.5.2.10.9.3.10.3',plain,[-(loca_level_below(admin, sbu, topsecret))],lemmata('1.1.5.2.10.9.3')).
% 1.43/2.45 cnf('1.1.5.2.10.10',plain,[-(admin_indi_has_compartments(admin, alice, nil))],extension(62,bind([[_31439], [alice]]))).
% 1.43/2.45 %-----------------------------------------------------
% 1.43/2.46
% 1.43/2.46 % SZS output end Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
%------------------------------------------------------------------------------