%------------------------------------------------------------------------------
% File : nanoCoP---2.0
% Problem : SWV437+1 : TPTP v8.1.2. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : nanocop.sh %s %d
% Computer : n010.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Fri May 19 12:20:43 EDT 2023
% Result : Theorem 2.71s 3.47s
% Output : Proof 2.71s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12 % Problem : SWV437+1 : TPTP v8.1.2. Released v4.0.0.
% 0.03/0.13 % Command : nanocop.sh %s %d
% 0.13/0.34 % Computer : n010.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 : Fri May 19 02:39:11 EDT 2023
% 0.13/0.35 % CPUTime :
% 2.71/3.47
% 2.71/3.47 /export/starexec/sandbox/benchmark/theBenchmark.p is a Theorem
% 2.71/3.47 Start of proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% 2.71/3.47 %-----------------------------------------------------
% 2.71/3.47 ncf(matrix, plain, [(528 ^ _143431) ^ [] : [admin_indi_may_file(admin, alice, secretfile, read)], (436 ^ _143431) ^ [] : [-(system_indi_is_oca(system, oca))], (438 ^ _143431) ^ [] : [-(oca_compartment_is_compartment(oca, compartmentb, confidential, topsecret, yes, yes))], (440 ^ _143431) ^ [] : [-(oca_compartment_is_compartment(oca, compartmenta, sbu, unclassified, no, no))], (442 ^ _143431) ^ [] : [-(system_compartment_has_sso(system, compartmentb, sso_compartmentb))], (444 ^ _143431) ^ [] : [-(oca_compartment_has_scg(oca, compartmentb, scg_compartmentb))], (446 ^ _143431) ^ [] : [-(sso_compartment_has_scg(sso_compartmentb, compartmentb, scg_compartmentb))], (448 ^ _143431) ^ [] : [-(system_compartment_has_sso(system, compartmenta, sso_compartmenta))], (450 ^ _143431) ^ [] : [-(oca_compartment_has_scg(oca, compartmenta, scg_compartmenta))], (452 ^ _143431) ^ [] : [-(sso_compartment_has_scg(sso_compartmenta, compartmenta, scg_compartmenta))], (454 ^ _143431) ^ [] : [-(state_file_is_not_working_paper(secretfile))], (456 ^ _143431) ^ [] : [-(system_file_needs_compartments(system, secretfile, cons(compartmentb, cons(compartmenta, nil))))], (458 ^ _143431) ^ [] : [-(sso_file_has_compartments(sso_compartmentb, secretfile, cons(compartmentb, cons(compartmenta, nil))))], (460 ^ _143431) ^ [] : [-(sso_file_has_compartments(sso_compartmenta, secretfile, cons(compartmentb, cons(compartmenta, nil))))], (462 ^ _143431) ^ [] : [-(system_file_needs_level(system, secretfile, secret))], (464 ^ _143431) ^ [] : [-(sso_file_has_level(sso_compartmentb, secretfile, secret, scg_compartmentb))], (466 ^ _143431) ^ [] : [-(sso_file_has_level(sso_compartmenta, secretfile, secret, scg_compartmenta))], (468 ^ _143431) ^ [] : [-(system_file_needs_citizenship(system, secretfile, usa))], (470 ^ _143431) ^ [] : [-(sso_file_has_citizenship(sso_compartmentb, secretfile, usa, scg_compartmentb))], (472 ^ _143431) ^ [] : [-(sso_file_has_citizenship(sso_compartmenta, secretfile, usa, scg_compartmenta))], (474 ^ _143431) ^ [] : [-(state_file_has_owner(secretfile, owner_secretfile))], (476 ^ _143431) ^ [] : [-(state_file_is_not_working_paper(not_secretfile))], (478 ^ _143431) ^ [] : [-(system_file_needs_compartments(system, not_secretfile, nil))], (480 ^ _143431) ^ [] : [-(system_file_needs_level(system, not_secretfile, unclassified))], (482 ^ _143431) ^ [] : [-(system_file_needs_citizenship(system, not_secretfile, anycountry))], (484 ^ _143431) ^ [] : [-(state_file_has_owner(not_secretfile, owner_not_secretfile))], (486 ^ _143431) ^ [] : [-(system_indi_is_polygraph_admin(system, polygraph_admin))], (488 ^ _143431) ^ [] : [-(system_indi_is_credit_admin(system, credit_admin))], (490 ^ _143431) ^ [] : [-(system_indi_is_background_admin(system, background_admin))], (492 ^ _143431) ^ [] : [-(system_indi_is_hr_admin(system, hr_admin))], (494 ^ _143431) ^ [] : [-(system_indi_is_level_admin(system, level_admin))], (496 ^ _143431) ^ [] : [-(system_indi_has_citizenship(system, alice, usa))], (498 ^ _143431) ^ [] : [-(polygraph_admin_indi_has_polygraph(polygraph_admin, alice))], (500 ^ _143431) ^ [] : [-(credit_admin_indi_has_credit(credit_admin, alice))], (502 ^ _143431) ^ [] : [-(background_admin_indi_has_background(background_admin, alice, topsecret))], (504 ^ _143431) ^ [] : [-(hr_admin_indi_has_employment(hr_admin, alice))], (506 ^ _143431) ^ [] : [-(system_indi_needs_level(system, alice, secret))], (508 ^ _143431) ^ [] : [-(level_admin_indi_has_level(level_admin, alice, topsecret))], (510 ^ _143431) ^ [] : [-(system_indi_needs_compartment(system, alice, compartmentb))], (512 ^ _143431) ^ [] : [-(system_indi_needs_compartment(system, alice, compartmenta))], (514 ^ _143431) ^ [] : [-(sso_indi_has_compartment(sso_compartmentb, alice, compartmentb))], (516 ^ _143431) ^ [] : [-(sso_indi_has_compartment(sso_compartmenta, alice, compartmenta))], (518 ^ _143431) ^ [] : [-(owner_indi_has_need_to_know(owner_secretfile, alice, secretfile))], (520 ^ _143431) ^ [] : [-(owner_indi_has_need_to_know(owner_secretfile, alice, not_secretfile))], (522 ^ _143431) ^ [] : [-(system_indi_has_citizenship(system, babu, india))], (524 ^ _143431) ^ [] : [-(owner_indi_has_need_to_know(owner_not_secretfile, babu, not_secretfile))], (526 ^ _143431) ^ [] : [-(system_indi_is_counterintelligence(system, ci, owner_secretfile))], (2 ^ _143431) ^ [_143535] : [-(loca_level_direct_below(_143535, unclassified, sbu))], (4 ^ _143431) ^ [_143614] : [-(loca_level_direct_below(_143614, sbu, confidential))], (6 ^ _143431) ^ [_143693] : [-(loca_level_direct_below(_143693, confidential, secret))], (8 ^ _143431) ^ [_143772] : [-(loca_level_direct_below(_143772, secret, topsecret))], (10 ^ _143431) ^ [_143865, _143867] : [-(loca_level_below(_143867, _143865, _143865))], (12 ^ _143431) ^ [_144003, _144005, _144007, _144009] : [loca_level_direct_below(_144009, _144005, _144003), loca_level_below(_144009, _144007, _144005), -(loca_level_below(_144009, _144007, _144003))], (22 ^ _143431) ^ [_144328, _144330] : [system_compartment_has_sso(system, _144330, _144328), -(admin_compartment_has_sso(admin, _144330, _144328))], (28 ^ _143431) ^ [_144570, _144572, _144574, _144576] : [system_indi_is_oca(system, _144576), oca_compartment_has_scg(_144576, _144574, _144570), admin_compartment_has_sso(admin, _144574, _144572), sso_compartment_has_scg(_144572, _144574, _144570), -(admin_compartment_has_scg(admin, _144574, _144570))], (46 ^ _143431) ^ [_145091, _145093] : [system_file_needs_compartments(system, _145093, _145091), admin_file_has_compartments_h(admin, _145093, _145091, _145091), -(admin_file_has_compartments(admin, _145093, _145091))], (56 ^ _143431) ^ [_145383, _145385] : [-(admin_file_has_compartments_h(admin, _145385, _145383, nil))], (58 ^ _143431) ^ [_145536, _145538, _145540, _145542, _145544] : [admin_compartment_has_sso(admin, _145540, _145536), sso_file_has_compartments(_145536, _145544, _145542), admin_file_has_compartments_h(admin, _145544, _145542, _145538), -(admin_file_has_compartments_h(admin, _145544, _145542, cons(_145540, _145538)))], (72 ^ _143431) ^ [_145998, _146000, _146002] : [system_file_needs_level(system, _146002, _146000), admin_file_has_compartments(admin, _146002, _145998), admin_file_has_level_h(admin, _146002, _146000, _145998), -(admin_file_has_level(admin, _146002, _146000))], (86 ^ _143431) ^ [_146395, _146397] : [-(admin_file_has_level_h(admin, _146397, _146395, nil))], (88 ^ _143431) ^ [_146562, _146564, _146566, _146568, _146570, _146572] : [admin_compartment_has_sso(admin, _146568, _146564), admin_compartment_has_scg(admin, _146568, _146562), sso_file_has_level(_146564, _146572, _146570, _146562), admin_file_has_level_h(admin, _146572, _146570, _146566), -(admin_file_has_level_h(admin, _146572, _146570, cons(_146568, _146566)))], (106 ^ _143431) ^ [_147147, _147149, _147151] : [system_file_needs_citizenship(system, _147151, _147149), admin_file_has_compartments(admin, _147151, _147147), admin_file_has_citizenship_h(admin, _147151, _147149, _147147), -(admin_file_has_citizenship(admin, _147151, _147149))], (120 ^ _143431) ^ [_147544, _147546] : [-(admin_file_has_citizenship_h(admin, _147546, _147544, nil))], (122 ^ _143431) ^ [_147711, _147713, _147715, _147717, _147719, _147721] : [admin_compartment_has_sso(admin, _147717, _147713), admin_compartment_has_scg(admin, _147717, _147711), sso_file_has_citizenship(_147713, _147721, _147719, _147711), admin_file_has_citizenship_h(admin, _147721, _147719, _147715), -(admin_file_has_citizenship_h(admin, _147721, _147719, cons(_147717, _147715)))], (140 ^ _143431) ^ [_148282, _148284] : [system_indi_is_polygraph_admin(system, _148282), polygraph_admin_indi_has_polygraph(_148282, _148284), -(admin_indi_has_polygraph(admin, _148284))], (150 ^ _143431) ^ [_148581, _148583] : [system_indi_is_credit_admin(system, _148581), credit_admin_indi_has_credit(_148581, _148583), -(admin_indi_has_credit(admin, _148583))], (160 ^ _143431) ^ [_148851] : [-(admin_indi_has_background(admin, _148851, unclassified))], (162 ^ _143431) ^ [_148987, _148989, _148991, _148993] : [system_indi_is_background_admin(system, _148989), background_admin_indi_has_background(_148989, _148993, _148987), loca_level_below(admin, _148991, _148987), -(admin_indi_has_background(admin, _148993, _148991))], (176 ^ _143431) ^ [_149409, _149411] : [system_indi_is_hr_admin(system, _149409), hr_admin_indi_has_employment(_149409, _149411), -(admin_indi_has_employment(admin, _149411))], (186 ^ _143431) ^ [_149679] : [-(admin_indi_has_citizenship(admin, _149679, anycountry))], (188 ^ _143431) ^ [_149787, _149789] : [system_indi_has_citizenship(system, _149789, _149787), -(admin_indi_has_citizenship(admin, _149789, _149787))], (194 ^ _143431) ^ [_149972] : [-(admin_indi_has_level(admin, _149972, unclassified))], (196 ^ _143431) ^ [_150122, _150124, _150126, _150128, _150130] : [system_indi_needs_level(system, _150130, _150126), admin_indi_has_citizenship(admin, _150130, usa), admin_indi_has_polygraph(admin, _150130), admin_indi_has_employment(admin, _150130), admin_indi_has_credit(admin, _150130), loca_level_below(admin, _150128, _150126), system_indi_is_level_admin(system, _150124), level_admin_indi_has_level(_150124, _150130, _150122), loca_level_below(admin, _150128, _150122), admin_indi_has_background(admin, _150130, _150128), -(admin_indi_has_level(admin, _150130, _150128))], (238 ^ _143431) ^ [_151244] : [-(admin_indi_has_compartments(admin, _151244, nil))], (240 ^ _143431) ^ [_151380, _151382, _151384, _151386] : [system_indi_needs_compartment(system, _151386, _151384), admin_indi_has_employment(admin, _151386), admin_indi_has_citizenship(admin, _151386, usa), admin_indi_has_polygraph_for_compartment(admin, _151386, _151384), admin_indi_has_credit_for_compartment(admin, _151386, _151384), admin_compartment_has_sso(admin, _151384, _151380), sso_indi_has_compartment(_151380, _151386, _151384), admin_indi_has_background_for_compartment(admin, _151386, _151384), admin_indi_has_level_for_compartment(admin, _151386, _151384), admin_indi_has_compartments(admin, _151386, _151382), -(admin_indi_has_compartments(admin, _151386, cons(_151384, _151382)))], (282 ^ _143431) ^ [_152571, _152573, _152575, _152577, _152579, _152581, _152583] : [system_indi_is_oca(system, _152579), oca_compartment_is_compartment(_152579, _152581, _152577, _152575, _152573, _152571), admin_indi_has_background(admin, _152583, _152575), -(admin_indi_has_background_for_compartment(admin, _152583, _152581))], (296 ^ _143431) ^ [_153111, _153113, _153115, _153117, _153119, _153121, _153123] : [system_indi_is_oca(system, _153119), oca_compartment_is_compartment(_153119, _153121, _153117, _153115, _153113, _153111), admin_indi_has_level(admin, _153123, _153117), -(admin_indi_has_level_for_compartment(admin, _153123, _153121))], (310 ^ _143431) ^ [_153637, _153639, _153641, _153643, _153645, _153647] : [system_indi_is_oca(system, _153643), oca_compartment_is_compartment(_153643, _153645, _153641, _153639, _153637, yes), admin_indi_has_polygraph(admin, _153647), -(admin_indi_has_polygraph_for_compartment(admin, _153647, _153645))], (324 ^ _143431) ^ [_154147, _154149, _154151, _154153, _154155, _154157] : [system_indi_is_oca(system, _154153), oca_compartment_is_compartment(_154153, _154155, _154151, _154149, _154147, no), -(admin_indi_has_polygraph_for_compartment(admin, _154157, _154155))], (334 ^ _143431) ^ [_154552, _154554, _154556, _154558, _154560, _154562] : [system_indi_is_oca(system, _154558), oca_compartment_is_compartment(_154558, _154560, _154556, _154554, yes, _154552), admin_indi_has_credit(admin, _154562), -(admin_indi_has_credit_for_compartment(admin, _154562, _154560))], (348 ^ _143431) ^ [_155062, _155064, _155066, _155068, _155070, _155072] : [system_indi_is_oca(system, _155068), oca_compartment_is_compartment(_155068, _155070, _155066, _155064, no, _155062), -(admin_indi_has_credit_for_compartment(admin, _155072, _155070))], (358 ^ _143431) ^ [_155425, _155427, _155429] : [admin_file_has_compartments(admin, _155427, _155425), admin_indi_has_compartments(admin, _155429, _155425), -(admin_indi_has_compartments_for_file(admin, _155429, _155427))], (368 ^ _143431) ^ [_155754, _155756, _155758] : [admin_file_has_level(admin, _155756, _155754), admin_indi_has_level(admin, _155758, _155754), -(admin_indi_has_level_for_file(admin, _155758, _155756))], (378 ^ _143431) ^ [_156083, _156085, _156087] : [state_file_has_owner(_156085, _156083), owner_indi_has_need_to_know(_156083, _156087, _156085), -(admin_indi_has_need_to_know_for_file(admin, _156087, _156085))], (388 ^ _143431) ^ [_156410, _156412, _156414] : [admin_file_has_citizenship(admin, _156412, _156410), admin_indi_has_citizenship(admin, _156414, _156410), -(admin_indi_has_citizenship_for_file(admin, _156414, _156412))], (398 ^ _143431) ^ [_156725, _156727] : [admin_indi_has_citizenship(admin, _156727, usa), -(admin_indi_has_citizenship_for_file(admin, _156727, _156725))], (426 ^ _143431) ^ [_157509, _157511, _157513] : [state_file_has_owner(_157511, _157509), system_indi_is_counterintelligence(system, _157513, _157509), -(admin_indi_may_file(admin, _157513, _157511, read))], (404 ^ _143431) ^ [_156939, _156941] : [state_file_is_not_working_paper(_156939), admin_indi_has_citizenship_for_file(admin, _156941, _156939), admin_indi_has_need_to_know_for_file(admin, _156941, _156939), admin_indi_has_level_for_file(admin, _156941, _156939), admin_indi_has_compartments_for_file(admin, _156941, _156939), -(admin_indi_may_file(admin, _156941, _156939, read))]], input).
% 2.71/3.47 ncf('1',plain,[admin_indi_may_file(admin, alice, secretfile, read)],start(528 ^ 0)).
% 2.71/3.47 ncf('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(404 ^ 1,bind([[_156939, _156941], [secretfile, alice]]))).
% 2.71/3.47 ncf('1.1.1',plain,[-(state_file_is_not_working_paper(secretfile))],extension(454 ^ 2)).
% 2.71/3.47 ncf('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(388 ^ 2,bind([[_156410, _156412, _156414], [usa, secretfile, alice]]))).
% 2.71/3.47 ncf('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(106 ^ 3,bind([[_147147, _147149, _147151], [cons(compartmentb, cons(compartmenta, nil)), usa, secretfile]]))).
% 2.71/3.47 ncf('1.1.2.1.1',plain,[-(system_file_needs_citizenship(system, secretfile, usa))],extension(468 ^ 4)).
% 2.71/3.47 ncf('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 ^ 4,bind([[_145091, _145093], [cons(compartmentb, cons(compartmenta, nil)), secretfile]]))).
% 2.71/3.47 ncf('1.1.2.1.2.1',plain,[-(system_file_needs_compartments(system, secretfile, cons(compartmentb, cons(compartmenta, nil))))],extension(456 ^ 5)).
% 2.71/3.47 ncf('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(58 ^ 5,bind([[_145536, _145538, _145540, _145542, _145544], [sso_compartmentb, cons(compartmenta, nil), compartmentb, cons(compartmentb, cons(compartmenta, nil)), secretfile]]))).
% 2.71/3.47 ncf('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(22 ^ 6,bind([[_144328, _144330], [sso_compartmentb, compartmentb]]))).
% 2.71/3.47 ncf('1.1.2.1.2.2.1.1',plain,[-(system_compartment_has_sso(system, compartmentb, sso_compartmentb))],extension(442 ^ 7)).
% 2.71/3.47 ncf('1.1.2.1.2.2.2',plain,[-(sso_file_has_compartments(sso_compartmentb, secretfile, cons(compartmentb, cons(compartmenta, nil))))],extension(458 ^ 6)).
% 2.71/3.47 ncf('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(58 ^ 6,bind([[_145536, _145538, _145540, _145542, _145544], [sso_compartmenta, nil, compartmenta, cons(compartmentb, cons(compartmenta, nil)), secretfile]]))).
% 2.71/3.47 ncf('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(22 ^ 7,bind([[_144328, _144330], [sso_compartmenta, compartmenta]]))).
% 2.71/3.47 ncf('1.1.2.1.2.2.3.1.1',plain,[-(system_compartment_has_sso(system, compartmenta, sso_compartmenta))],extension(448 ^ 8)).
% 2.71/3.47 ncf('1.1.2.1.2.2.3.2',plain,[-(sso_file_has_compartments(sso_compartmenta, secretfile, cons(compartmentb, cons(compartmenta, nil))))],extension(460 ^ 7)).
% 2.71/3.47 ncf('1.1.2.1.2.2.3.3',plain,[-(admin_file_has_compartments_h(admin, secretfile, cons(compartmentb, cons(compartmenta, nil)), nil))],extension(56 ^ 7,bind([[_145383, _145385], [cons(compartmentb, cons(compartmenta, nil)), secretfile]]))).
% 2.71/3.47 ncf('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(122 ^ 4,bind([[_147711, _147713, _147715, _147717, _147719, _147721], [scg_compartmentb, sso_compartmentb, cons(compartmenta, nil), compartmentb, usa, secretfile]]))).
% 2.71/3.47 ncf('1.1.2.1.3.1',plain,[-(admin_compartment_has_sso(admin, compartmentb, sso_compartmentb)), system_compartment_has_sso(system, compartmentb, sso_compartmentb)],extension(22 ^ 5,bind([[_144328, _144330], [sso_compartmentb, compartmentb]]))).
% 2.71/3.47 ncf('1.1.2.1.3.1.1',plain,[-(system_compartment_has_sso(system, compartmentb, sso_compartmentb))],extension(442 ^ 6)).
% 2.71/3.47 ncf('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(28 ^ 5,bind([[_144570, _144572, _144574, _144576], [scg_compartmentb, sso_compartmentb, compartmentb, oca]]))).
% 2.71/3.47 ncf('1.1.2.1.3.2.1',plain,[-(system_indi_is_oca(system, oca))],extension(436 ^ 6)).
% 2.71/3.47 ncf('1.1.2.1.3.2.2',plain,[-(oca_compartment_has_scg(oca, compartmentb, scg_compartmentb))],extension(444 ^ 6)).
% 2.71/3.47 ncf('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(22 ^ 6,bind([[_144328, _144330], [sso_compartmentb, compartmentb]]))).
% 2.71/3.47 ncf('1.1.2.1.3.2.3.1',plain,[-(system_compartment_has_sso(system, compartmentb, sso_compartmentb))],extension(442 ^ 7)).
% 2.71/3.47 ncf('1.1.2.1.3.2.4',plain,[-(sso_compartment_has_scg(sso_compartmentb, compartmentb, scg_compartmentb))],extension(446 ^ 6)).
% 2.71/3.47 ncf('1.1.2.1.3.3',plain,[-(sso_file_has_citizenship(sso_compartmentb, secretfile, usa, scg_compartmentb))],extension(470 ^ 5)).
% 2.71/3.47 ncf('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(122 ^ 5,bind([[_147711, _147713, _147715, _147717, _147719, _147721], [scg_compartmenta, sso_compartmenta, nil, compartmenta, usa, secretfile]]))).
% 2.71/3.47 ncf('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(22 ^ 6,bind([[_144328, _144330], [sso_compartmenta, compartmenta]]))).
% 2.71/3.47 ncf('1.1.2.1.3.4.1.1',plain,[-(system_compartment_has_sso(system, compartmenta, sso_compartmenta))],extension(448 ^ 7)).
% 2.71/3.47 ncf('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(28 ^ 6,bind([[_144570, _144572, _144574, _144576], [scg_compartmenta, sso_compartmenta, compartmenta, oca]]))).
% 2.71/3.47 ncf('1.1.2.1.3.4.2.1',plain,[-(system_indi_is_oca(system, oca))],extension(436 ^ 7)).
% 2.71/3.47 ncf('1.1.2.1.3.4.2.2',plain,[-(oca_compartment_has_scg(oca, compartmenta, scg_compartmenta))],extension(450 ^ 7)).
% 2.71/3.47 ncf('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(22 ^ 7,bind([[_144328, _144330], [sso_compartmenta, compartmenta]]))).
% 2.71/3.47 ncf('1.1.2.1.3.4.2.3.1',plain,[-(system_compartment_has_sso(system, compartmenta, sso_compartmenta))],extension(448 ^ 8)).
% 2.71/3.47 ncf('1.1.2.1.3.4.2.4',plain,[-(sso_compartment_has_scg(sso_compartmenta, compartmenta, scg_compartmenta))],extension(452 ^ 7)).
% 2.71/3.47 ncf('1.1.2.1.3.4.3',plain,[-(sso_file_has_citizenship(sso_compartmenta, secretfile, usa, scg_compartmenta))],extension(472 ^ 6)).
% 2.71/3.47 ncf('1.1.2.1.3.4.4',plain,[-(admin_file_has_citizenship_h(admin, secretfile, usa, nil))],extension(120 ^ 6,bind([[_147544, _147546], [usa, secretfile]]))).
% 2.71/3.47 ncf('1.1.2.2',plain,[-(admin_indi_has_citizenship(admin, alice, usa)), system_indi_has_citizenship(system, alice, usa)],extension(188 ^ 3,bind([[_149787, _149789], [usa, alice]]))).
% 2.71/3.47 ncf('1.1.2.2.1',plain,[-(system_indi_has_citizenship(system, alice, usa))],extension(496 ^ 4)).
% 2.71/3.47 ncf('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(378 ^ 2,bind([[_156083, _156085, _156087], [owner_secretfile, secretfile, alice]]))).
% 2.71/3.47 ncf('1.1.3.1',plain,[-(state_file_has_owner(secretfile, owner_secretfile))],extension(474 ^ 3)).
% 2.71/3.47 ncf('1.1.3.2',plain,[-(owner_indi_has_need_to_know(owner_secretfile, alice, secretfile))],extension(518 ^ 3)).
% 2.71/3.47 ncf('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(368 ^ 2,bind([[_155754, _155756, _155758], [secret, secretfile, alice]]))).
% 2.71/3.47 ncf('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(72 ^ 3,bind([[_145998, _146000, _146002], [cons(compartmentb, cons(compartmenta, nil)), secret, secretfile]]))).
% 2.71/3.47 ncf('1.1.4.1.1',plain,[-(system_file_needs_level(system, secretfile, secret))],extension(462 ^ 4)).
% 2.71/3.47 ncf('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 ^ 4,bind([[_145091, _145093], [cons(compartmentb, cons(compartmenta, nil)), secretfile]]))).
% 2.71/3.47 ncf('1.1.4.1.2.1',plain,[-(system_file_needs_compartments(system, secretfile, cons(compartmentb, cons(compartmenta, nil))))],extension(456 ^ 5)).
% 2.71/3.47 ncf('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(58 ^ 5,bind([[_145536, _145538, _145540, _145542, _145544], [sso_compartmentb, cons(compartmenta, nil), compartmentb, cons(compartmentb, cons(compartmenta, nil)), secretfile]]))).
% 2.71/3.47 ncf('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(22 ^ 6,bind([[_144328, _144330], [sso_compartmentb, compartmentb]]))).
% 2.71/3.47 ncf('1.1.4.1.2.2.1.1',plain,[-(system_compartment_has_sso(system, compartmentb, sso_compartmentb))],extension(442 ^ 7)).
% 2.71/3.47 ncf('1.1.4.1.2.2.2',plain,[-(sso_file_has_compartments(sso_compartmentb, secretfile, cons(compartmentb, cons(compartmenta, nil))))],extension(458 ^ 6)).
% 2.71/3.47 ncf('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(58 ^ 6,bind([[_145536, _145538, _145540, _145542, _145544], [sso_compartmenta, nil, compartmenta, cons(compartmentb, cons(compartmenta, nil)), secretfile]]))).
% 2.71/3.47 ncf('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(22 ^ 7,bind([[_144328, _144330], [sso_compartmenta, compartmenta]]))).
% 2.71/3.47 ncf('1.1.4.1.2.2.3.1.1',plain,[-(system_compartment_has_sso(system, compartmenta, sso_compartmenta))],extension(448 ^ 8)).
% 2.71/3.47 ncf('1.1.4.1.2.2.3.2',plain,[-(sso_file_has_compartments(sso_compartmenta, secretfile, cons(compartmentb, cons(compartmenta, nil))))],extension(460 ^ 7)).
% 2.71/3.47 ncf('1.1.4.1.2.2.3.3',plain,[-(admin_file_has_compartments_h(admin, secretfile, cons(compartmentb, cons(compartmenta, nil)), nil))],extension(56 ^ 7,bind([[_145383, _145385], [cons(compartmentb, cons(compartmenta, nil)), secretfile]]))).
% 2.71/3.47 ncf('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(88 ^ 4,bind([[_146562, _146564, _146566, _146568, _146570, _146572], [scg_compartmentb, sso_compartmentb, cons(compartmenta, nil), compartmentb, secret, secretfile]]))).
% 2.71/3.47 ncf('1.1.4.1.3.1',plain,[-(admin_compartment_has_sso(admin, compartmentb, sso_compartmentb)), system_compartment_has_sso(system, compartmentb, sso_compartmentb)],extension(22 ^ 5,bind([[_144328, _144330], [sso_compartmentb, compartmentb]]))).
% 2.71/3.47 ncf('1.1.4.1.3.1.1',plain,[-(system_compartment_has_sso(system, compartmentb, sso_compartmentb))],extension(442 ^ 6)).
% 2.71/3.47 ncf('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(28 ^ 5,bind([[_144570, _144572, _144574, _144576], [scg_compartmentb, sso_compartmentb, compartmentb, oca]]))).
% 2.71/3.47 ncf('1.1.4.1.3.2.1',plain,[-(system_indi_is_oca(system, oca))],extension(436 ^ 6)).
% 2.71/3.47 ncf('1.1.4.1.3.2.2',plain,[-(oca_compartment_has_scg(oca, compartmentb, scg_compartmentb))],extension(444 ^ 6)).
% 2.71/3.47 ncf('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(22 ^ 6,bind([[_144328, _144330], [sso_compartmentb, compartmentb]]))).
% 2.71/3.47 ncf('1.1.4.1.3.2.3.1',plain,[-(system_compartment_has_sso(system, compartmentb, sso_compartmentb))],extension(442 ^ 7)).
% 2.71/3.47 ncf('1.1.4.1.3.2.4',plain,[-(sso_compartment_has_scg(sso_compartmentb, compartmentb, scg_compartmentb))],extension(446 ^ 6)).
% 2.71/3.47 ncf('1.1.4.1.3.3',plain,[-(sso_file_has_level(sso_compartmentb, secretfile, secret, scg_compartmentb))],extension(464 ^ 5)).
% 2.71/3.47 ncf('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(88 ^ 5,bind([[_146562, _146564, _146566, _146568, _146570, _146572], [scg_compartmenta, sso_compartmenta, nil, compartmenta, secret, secretfile]]))).
% 2.71/3.47 ncf('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(22 ^ 6,bind([[_144328, _144330], [sso_compartmenta, compartmenta]]))).
% 2.71/3.47 ncf('1.1.4.1.3.4.1.1',plain,[-(system_compartment_has_sso(system, compartmenta, sso_compartmenta))],extension(448 ^ 7)).
% 2.71/3.47 ncf('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(28 ^ 6,bind([[_144570, _144572, _144574, _144576], [scg_compartmenta, sso_compartmenta, compartmenta, oca]]))).
% 2.71/3.47 ncf('1.1.4.1.3.4.2.1',plain,[-(system_indi_is_oca(system, oca))],extension(436 ^ 7)).
% 2.71/3.47 ncf('1.1.4.1.3.4.2.2',plain,[-(oca_compartment_has_scg(oca, compartmenta, scg_compartmenta))],extension(450 ^ 7)).
% 2.71/3.47 ncf('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(22 ^ 7,bind([[_144328, _144330], [sso_compartmenta, compartmenta]]))).
% 2.71/3.47 ncf('1.1.4.1.3.4.2.3.1',plain,[-(system_compartment_has_sso(system, compartmenta, sso_compartmenta))],extension(448 ^ 8)).
% 2.71/3.47 ncf('1.1.4.1.3.4.2.4',plain,[-(sso_compartment_has_scg(sso_compartmenta, compartmenta, scg_compartmenta))],extension(452 ^ 7)).
% 2.71/3.47 ncf('1.1.4.1.3.4.3',plain,[-(sso_file_has_level(sso_compartmenta, secretfile, secret, scg_compartmenta))],extension(466 ^ 6)).
% 2.71/3.47 ncf('1.1.4.1.3.4.4',plain,[-(admin_file_has_level_h(admin, secretfile, secret, nil))],extension(86 ^ 6,bind([[_146395, _146397], [secret, secretfile]]))).
% 2.71/3.47 ncf('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(196 ^ 3,bind([[_150122, _150124, _150126, _150128, _150130], [topsecret, level_admin, secret, secret, alice]]))).
% 2.71/3.47 ncf('1.1.4.2.1',plain,[-(system_indi_needs_level(system, alice, secret))],extension(506 ^ 4)).
% 2.71/3.47 ncf('1.1.4.2.2',plain,[-(admin_indi_has_citizenship(admin, alice, usa)), system_indi_has_citizenship(system, alice, usa)],extension(188 ^ 4,bind([[_149787, _149789], [usa, alice]]))).
% 2.71/3.47 ncf('1.1.4.2.2.1',plain,[-(system_indi_has_citizenship(system, alice, usa))],extension(496 ^ 5)).
% 2.71/3.47 ncf('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(140 ^ 4,bind([[_148282, _148284], [polygraph_admin, alice]]))).
% 2.71/3.47 ncf('1.1.4.2.3.1',plain,[-(system_indi_is_polygraph_admin(system, polygraph_admin))],extension(486 ^ 5)).
% 2.71/3.47 ncf('1.1.4.2.3.2',plain,[-(polygraph_admin_indi_has_polygraph(polygraph_admin, alice))],extension(498 ^ 5)).
% 2.71/3.47 ncf('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(176 ^ 4,bind([[_149409, _149411], [hr_admin, alice]]))).
% 2.71/3.47 ncf('1.1.4.2.4.1',plain,[-(system_indi_is_hr_admin(system, hr_admin))],extension(492 ^ 5)).
% 2.71/3.47 ncf('1.1.4.2.4.2',plain,[-(hr_admin_indi_has_employment(hr_admin, alice))],extension(504 ^ 5)).
% 2.71/3.47 ncf('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(150 ^ 4,bind([[_148581, _148583], [credit_admin, alice]]))).
% 2.71/3.47 ncf('1.1.4.2.5.1',plain,[-(system_indi_is_credit_admin(system, credit_admin))],extension(488 ^ 5)).
% 2.71/3.47 ncf('1.1.4.2.5.2',plain,[-(credit_admin_indi_has_credit(credit_admin, alice))],extension(500 ^ 5)).
% 2.71/3.47 ncf('1.1.4.2.6',plain,[-(loca_level_below(admin, secret, secret))],extension(10 ^ 4,bind([[_143865, _143867], [secret, admin]]))).
% 2.71/3.47 ncf('1.1.4.2.7',plain,[-(system_indi_is_level_admin(system, level_admin))],extension(494 ^ 4)).
% 2.71/3.47 ncf('1.1.4.2.8',plain,[-(level_admin_indi_has_level(level_admin, alice, topsecret))],extension(508 ^ 4)).
% 2.71/3.47 ncf('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(12 ^ 4,bind([[_144003, _144005, _144007, _144009], [topsecret, secret, secret, admin]]))).
% 2.71/3.47 ncf('1.1.4.2.9.1',plain,[-(loca_level_direct_below(admin, secret, topsecret))],extension(8 ^ 5,bind([[_143772], [admin]]))).
% 2.71/3.47 ncf('1.1.4.2.9.2',plain,[-(loca_level_below(admin, secret, secret))],lemmata('[4, 1, 1].x')).
% 2.71/3.47 ncf('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(162 ^ 4,bind([[_148987, _148989, _148991, _148993], [topsecret, background_admin, secret, alice]]))).
% 2.71/3.47 ncf('1.1.4.2.10.1',plain,[-(system_indi_is_background_admin(system, background_admin))],extension(490 ^ 5)).
% 2.71/3.47 ncf('1.1.4.2.10.2',plain,[-(background_admin_indi_has_background(background_admin, alice, topsecret))],extension(502 ^ 5)).
% 2.71/3.47 ncf('1.1.4.2.10.3',plain,[-(loca_level_below(admin, secret, topsecret))],lemmata('[4, 1, 1].x')).
% 2.71/3.47 ncf('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(358 ^ 2,bind([[_155425, _155427, _155429], [cons(compartmentb, cons(compartmenta, nil)), secretfile, alice]]))).
% 2.71/3.47 ncf('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 ^ 3,bind([[_145091, _145093], [cons(compartmentb, cons(compartmenta, nil)), secretfile]]))).
% 2.71/3.47 ncf('1.1.5.1.1',plain,[-(system_file_needs_compartments(system, secretfile, cons(compartmentb, cons(compartmenta, nil))))],extension(456 ^ 4)).
% 2.71/3.47 ncf('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(58 ^ 4,bind([[_145536, _145538, _145540, _145542, _145544], [sso_compartmentb, cons(compartmenta, nil), compartmentb, cons(compartmentb, cons(compartmenta, nil)), secretfile]]))).
% 2.71/3.47 ncf('1.1.5.1.2.1',plain,[-(admin_compartment_has_sso(admin, compartmentb, sso_compartmentb)), system_compartment_has_sso(system, compartmentb, sso_compartmentb)],extension(22 ^ 5,bind([[_144328, _144330], [sso_compartmentb, compartmentb]]))).
% 2.71/3.47 ncf('1.1.5.1.2.1.1',plain,[-(system_compartment_has_sso(system, compartmentb, sso_compartmentb))],extension(442 ^ 6)).
% 2.71/3.47 ncf('1.1.5.1.2.2',plain,[-(sso_file_has_compartments(sso_compartmentb, secretfile, cons(compartmentb, cons(compartmenta, nil))))],extension(458 ^ 5)).
% 2.71/3.47 ncf('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(58 ^ 5,bind([[_145536, _145538, _145540, _145542, _145544], [sso_compartmenta, nil, compartmenta, cons(compartmentb, cons(compartmenta, nil)), secretfile]]))).
% 2.71/3.47 ncf('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(22 ^ 6,bind([[_144328, _144330], [sso_compartmenta, compartmenta]]))).
% 2.71/3.47 ncf('1.1.5.1.2.3.1.1',plain,[-(system_compartment_has_sso(system, compartmenta, sso_compartmenta))],extension(448 ^ 7)).
% 2.71/3.47 ncf('1.1.5.1.2.3.2',plain,[-(sso_file_has_compartments(sso_compartmenta, secretfile, cons(compartmentb, cons(compartmenta, nil))))],extension(460 ^ 6)).
% 2.71/3.47 ncf('1.1.5.1.2.3.3',plain,[-(admin_file_has_compartments_h(admin, secretfile, cons(compartmentb, cons(compartmenta, nil)), nil))],extension(56 ^ 6,bind([[_145383, _145385], [cons(compartmentb, cons(compartmenta, nil)), secretfile]]))).
% 2.71/3.47 ncf('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(240 ^ 3,bind([[_151380, _151382, _151384, _151386], [sso_compartmentb, cons(compartmenta, nil), compartmentb, alice]]))).
% 2.71/3.47 ncf('1.1.5.2.1',plain,[-(system_indi_needs_compartment(system, alice, compartmentb))],extension(510 ^ 4)).
% 2.71/3.47 ncf('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(176 ^ 4,bind([[_149409, _149411], [hr_admin, alice]]))).
% 2.71/3.47 ncf('1.1.5.2.2.1',plain,[-(system_indi_is_hr_admin(system, hr_admin))],extension(492 ^ 5)).
% 2.71/3.47 ncf('1.1.5.2.2.2',plain,[-(hr_admin_indi_has_employment(hr_admin, alice))],extension(504 ^ 5)).
% 2.71/3.47 ncf('1.1.5.2.3',plain,[-(admin_indi_has_citizenship(admin, alice, usa)), system_indi_has_citizenship(system, alice, usa)],extension(188 ^ 4,bind([[_149787, _149789], [usa, alice]]))).
% 2.71/3.47 ncf('1.1.5.2.3.1',plain,[-(system_indi_has_citizenship(system, alice, usa))],extension(496 ^ 5)).
% 2.71/3.47 ncf('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(310 ^ 4,bind([[_153637, _153639, _153641, _153643, _153645, _153647], [yes, topsecret, confidential, oca, compartmentb, alice]]))).
% 2.71/3.47 ncf('1.1.5.2.4.1',plain,[-(system_indi_is_oca(system, oca))],extension(436 ^ 5)).
% 2.71/3.47 ncf('1.1.5.2.4.2',plain,[-(oca_compartment_is_compartment(oca, compartmentb, confidential, topsecret, yes, yes))],extension(438 ^ 5)).
% 2.71/3.47 ncf('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(140 ^ 5,bind([[_148282, _148284], [polygraph_admin, alice]]))).
% 2.71/3.47 ncf('1.1.5.2.4.3.1',plain,[-(system_indi_is_polygraph_admin(system, polygraph_admin))],extension(486 ^ 6)).
% 2.71/3.47 ncf('1.1.5.2.4.3.2',plain,[-(polygraph_admin_indi_has_polygraph(polygraph_admin, alice))],extension(498 ^ 6)).
% 2.71/3.47 ncf('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(334 ^ 4,bind([[_154552, _154554, _154556, _154558, _154560, _154562], [yes, topsecret, confidential, oca, compartmentb, alice]]))).
% 2.71/3.47 ncf('1.1.5.2.5.1',plain,[-(system_indi_is_oca(system, oca))],extension(436 ^ 5)).
% 2.71/3.47 ncf('1.1.5.2.5.2',plain,[-(oca_compartment_is_compartment(oca, compartmentb, confidential, topsecret, yes, yes))],extension(438 ^ 5)).
% 2.71/3.47 ncf('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(150 ^ 5,bind([[_148581, _148583], [credit_admin, alice]]))).
% 2.71/3.47 ncf('1.1.5.2.5.3.1',plain,[-(system_indi_is_credit_admin(system, credit_admin))],extension(488 ^ 6)).
% 2.71/3.47 ncf('1.1.5.2.5.3.2',plain,[-(credit_admin_indi_has_credit(credit_admin, alice))],extension(500 ^ 6)).
% 2.71/3.47 ncf('1.1.5.2.6',plain,[-(admin_compartment_has_sso(admin, compartmentb, sso_compartmentb)), system_compartment_has_sso(system, compartmentb, sso_compartmentb)],extension(22 ^ 4,bind([[_144328, _144330], [sso_compartmentb, compartmentb]]))).
% 2.71/3.47 ncf('1.1.5.2.6.1',plain,[-(system_compartment_has_sso(system, compartmentb, sso_compartmentb))],extension(442 ^ 5)).
% 2.71/3.47 ncf('1.1.5.2.7',plain,[-(sso_indi_has_compartment(sso_compartmentb, alice, compartmentb))],extension(514 ^ 4)).
% 2.71/3.47 ncf('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(282 ^ 4,bind([[_152571, _152573, _152575, _152577, _152579, _152581, _152583], [yes, yes, topsecret, confidential, oca, compartmentb, alice]]))).
% 2.71/3.47 ncf('1.1.5.2.8.1',plain,[-(system_indi_is_oca(system, oca))],extension(436 ^ 5)).
% 2.71/3.47 ncf('1.1.5.2.8.2',plain,[-(oca_compartment_is_compartment(oca, compartmentb, confidential, topsecret, yes, yes))],extension(438 ^ 5)).
% 2.71/3.47 ncf('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(162 ^ 5,bind([[_148987, _148989, _148991, _148993], [topsecret, background_admin, topsecret, alice]]))).
% 2.71/3.47 ncf('1.1.5.2.8.3.1',plain,[-(system_indi_is_background_admin(system, background_admin))],extension(490 ^ 6)).
% 2.71/3.47 ncf('1.1.5.2.8.3.2',plain,[-(background_admin_indi_has_background(background_admin, alice, topsecret))],extension(502 ^ 6)).
% 2.71/3.47 ncf('1.1.5.2.8.3.3',plain,[-(loca_level_below(admin, topsecret, topsecret))],extension(10 ^ 6,bind([[_143865, _143867], [topsecret, admin]]))).
% 2.71/3.47 ncf('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(296 ^ 4,bind([[_153111, _153113, _153115, _153117, _153119, _153121, _153123], [yes, yes, topsecret, confidential, oca, compartmentb, alice]]))).
% 2.71/3.47 ncf('1.1.5.2.9.1',plain,[-(system_indi_is_oca(system, oca))],extension(436 ^ 5)).
% 2.71/3.47 ncf('1.1.5.2.9.2',plain,[-(oca_compartment_is_compartment(oca, compartmentb, confidential, topsecret, yes, yes))],extension(438 ^ 5)).
% 2.71/3.47 ncf('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(196 ^ 5,bind([[_150122, _150124, _150126, _150128, _150130], [topsecret, level_admin, secret, confidential, alice]]))).
% 2.71/3.47 ncf('1.1.5.2.9.3.1',plain,[-(system_indi_needs_level(system, alice, secret))],extension(506 ^ 6)).
% 2.71/3.47 ncf('1.1.5.2.9.3.2',plain,[-(admin_indi_has_citizenship(admin, alice, usa))],lemmata('[5, 1, 1].x')).
% 2.71/3.47 ncf('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(140 ^ 6,bind([[_148282, _148284], [polygraph_admin, alice]]))).
% 2.71/3.47 ncf('1.1.5.2.9.3.3.1',plain,[-(system_indi_is_polygraph_admin(system, polygraph_admin))],extension(486 ^ 7)).
% 2.71/3.47 ncf('1.1.5.2.9.3.3.2',plain,[-(polygraph_admin_indi_has_polygraph(polygraph_admin, alice))],extension(498 ^ 7)).
% 2.71/3.47 ncf('1.1.5.2.9.3.4',plain,[-(admin_indi_has_employment(admin, alice))],lemmata('[5, 1, 1].x')).
% 2.71/3.47 ncf('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(150 ^ 6,bind([[_148581, _148583], [credit_admin, alice]]))).
% 2.71/3.47 ncf('1.1.5.2.9.3.5.1',plain,[-(system_indi_is_credit_admin(system, credit_admin))],extension(488 ^ 7)).
% 2.71/3.47 ncf('1.1.5.2.9.3.5.2',plain,[-(credit_admin_indi_has_credit(credit_admin, alice))],extension(500 ^ 7)).
% 2.71/3.47 ncf('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(12 ^ 6,bind([[_144003, _144005, _144007, _144009], [secret, confidential, confidential, admin]]))).
% 2.71/3.47 ncf('1.1.5.2.9.3.6.1',plain,[-(loca_level_direct_below(admin, confidential, secret))],extension(6 ^ 7,bind([[_143693], [admin]]))).
% 2.71/3.47 ncf('1.1.5.2.9.3.6.2',plain,[-(loca_level_below(admin, confidential, confidential))],extension(10 ^ 7,bind([[_143865, _143867], [confidential, admin]]))).
% 2.71/3.47 ncf('1.1.5.2.9.3.7',plain,[-(system_indi_is_level_admin(system, level_admin))],extension(494 ^ 6)).
% 2.71/3.47 ncf('1.1.5.2.9.3.8',plain,[-(level_admin_indi_has_level(level_admin, alice, topsecret))],extension(508 ^ 6)).
% 2.71/3.47 ncf('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(12 ^ 6,bind([[_144003, _144005, _144007, _144009], [topsecret, secret, confidential, admin]]))).
% 2.71/3.47 ncf('1.1.5.2.9.3.9.1',plain,[-(loca_level_direct_below(admin, secret, topsecret))],extension(8 ^ 7,bind([[_143772], [admin]]))).
% 2.71/3.47 ncf('1.1.5.2.9.3.9.2',plain,[-(loca_level_below(admin, confidential, secret))],lemmata('[9, 2, 5, 1, 1].x')).
% 2.71/3.47 ncf('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(162 ^ 6,bind([[_148987, _148989, _148991, _148993], [topsecret, background_admin, confidential, alice]]))).
% 2.71/3.47 ncf('1.1.5.2.9.3.10.1',plain,[-(system_indi_is_background_admin(system, background_admin))],extension(490 ^ 7)).
% 2.71/3.47 ncf('1.1.5.2.9.3.10.2',plain,[-(background_admin_indi_has_background(background_admin, alice, topsecret))],extension(502 ^ 7)).
% 2.71/3.47 ncf('1.1.5.2.9.3.10.3',plain,[-(loca_level_below(admin, confidential, topsecret))],lemmata('[9, 2, 5, 1, 1].x')).
% 2.71/3.47 ncf('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(240 ^ 4,bind([[_151380, _151382, _151384, _151386], [sso_compartmenta, nil, compartmenta, alice]]))).
% 2.71/3.47 ncf('1.1.5.2.10.1',plain,[-(system_indi_needs_compartment(system, alice, compartmenta))],extension(512 ^ 5)).
% 2.71/3.47 ncf('1.1.5.2.10.2',plain,[-(admin_indi_has_employment(admin, alice))],lemmata('[5, 1, 1].x')).
% 2.71/3.47 ncf('1.1.5.2.10.3',plain,[-(admin_indi_has_citizenship(admin, alice, usa))],lemmata('[5, 1, 1].x')).
% 2.71/3.47 ncf('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(324 ^ 5,bind([[_154147, _154149, _154151, _154153, _154155, _154157], [no, unclassified, sbu, oca, compartmenta, alice]]))).
% 2.71/3.47 ncf('1.1.5.2.10.4.1',plain,[-(system_indi_is_oca(system, oca))],extension(436 ^ 6)).
% 2.71/3.47 ncf('1.1.5.2.10.4.2',plain,[-(oca_compartment_is_compartment(oca, compartmenta, sbu, unclassified, no, no))],extension(440 ^ 6)).
% 2.71/3.47 ncf('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(348 ^ 5,bind([[_155062, _155064, _155066, _155068, _155070, _155072], [no, unclassified, sbu, oca, compartmenta, alice]]))).
% 2.71/3.47 ncf('1.1.5.2.10.5.1',plain,[-(system_indi_is_oca(system, oca))],extension(436 ^ 6)).
% 2.71/3.47 ncf('1.1.5.2.10.5.2',plain,[-(oca_compartment_is_compartment(oca, compartmenta, sbu, unclassified, no, no))],extension(440 ^ 6)).
% 2.71/3.47 ncf('1.1.5.2.10.6',plain,[-(admin_compartment_has_sso(admin, compartmenta, sso_compartmenta)), system_compartment_has_sso(system, compartmenta, sso_compartmenta)],extension(22 ^ 5,bind([[_144328, _144330], [sso_compartmenta, compartmenta]]))).
% 2.71/3.47 ncf('1.1.5.2.10.6.1',plain,[-(system_compartment_has_sso(system, compartmenta, sso_compartmenta))],extension(448 ^ 6)).
% 2.71/3.47 ncf('1.1.5.2.10.7',plain,[-(sso_indi_has_compartment(sso_compartmenta, alice, compartmenta))],extension(516 ^ 5)).
% 2.71/3.47 ncf('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(282 ^ 5,bind([[_152571, _152573, _152575, _152577, _152579, _152581, _152583], [no, no, unclassified, sbu, oca, compartmenta, alice]]))).
% 2.71/3.47 ncf('1.1.5.2.10.8.1',plain,[-(system_indi_is_oca(system, oca))],extension(436 ^ 6)).
% 2.71/3.47 ncf('1.1.5.2.10.8.2',plain,[-(oca_compartment_is_compartment(oca, compartmenta, sbu, unclassified, no, no))],extension(440 ^ 6)).
% 2.71/3.47 ncf('1.1.5.2.10.8.3',plain,[-(admin_indi_has_background(admin, alice, unclassified))],extension(160 ^ 6,bind([[_148851], [alice]]))).
% 2.71/3.47 ncf('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(296 ^ 5,bind([[_153111, _153113, _153115, _153117, _153119, _153121, _153123], [no, no, unclassified, sbu, oca, compartmenta, alice]]))).
% 2.71/3.47 ncf('1.1.5.2.10.9.1',plain,[-(system_indi_is_oca(system, oca))],extension(436 ^ 6)).
% 2.71/3.47 ncf('1.1.5.2.10.9.2',plain,[-(oca_compartment_is_compartment(oca, compartmenta, sbu, unclassified, no, no))],extension(440 ^ 6)).
% 2.71/3.47 ncf('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(196 ^ 6,bind([[_150122, _150124, _150126, _150128, _150130], [topsecret, level_admin, secret, sbu, alice]]))).
% 2.71/3.47 ncf('1.1.5.2.10.9.3.1',plain,[-(system_indi_needs_level(system, alice, secret))],extension(506 ^ 7)).
% 2.71/3.47 ncf('1.1.5.2.10.9.3.2',plain,[-(admin_indi_has_citizenship(admin, alice, usa))],lemmata('[2, 5, 1, 1].x')).
% 2.71/3.47 ncf('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(140 ^ 7,bind([[_148282, _148284], [polygraph_admin, alice]]))).
% 2.71/3.47 ncf('1.1.5.2.10.9.3.3.1',plain,[-(system_indi_is_polygraph_admin(system, polygraph_admin))],extension(486 ^ 8)).
% 2.71/3.47 ncf('1.1.5.2.10.9.3.3.2',plain,[-(polygraph_admin_indi_has_polygraph(polygraph_admin, alice))],extension(498 ^ 8)).
% 2.71/3.47 ncf('1.1.5.2.10.9.3.4',plain,[-(admin_indi_has_employment(admin, alice))],lemmata('[2, 5, 1, 1].x')).
% 2.71/3.47 ncf('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(150 ^ 7,bind([[_148581, _148583], [credit_admin, alice]]))).
% 2.71/3.47 ncf('1.1.5.2.10.9.3.5.1',plain,[-(system_indi_is_credit_admin(system, credit_admin))],extension(488 ^ 8)).
% 2.71/3.47 ncf('1.1.5.2.10.9.3.5.2',plain,[-(credit_admin_indi_has_credit(credit_admin, alice))],extension(500 ^ 8)).
% 2.71/3.47 ncf('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(12 ^ 7,bind([[_144003, _144005, _144007, _144009], [secret, confidential, sbu, admin]]))).
% 2.71/3.47 ncf('1.1.5.2.10.9.3.6.1',plain,[-(loca_level_direct_below(admin, confidential, secret))],extension(6 ^ 8,bind([[_143693], [admin]]))).
% 2.71/3.47 ncf('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(12 ^ 8,bind([[_144003, _144005, _144007, _144009], [confidential, sbu, sbu, admin]]))).
% 2.71/3.47 ncf('1.1.5.2.10.9.3.6.2.1',plain,[-(loca_level_direct_below(admin, sbu, confidential))],extension(4 ^ 9,bind([[_143614], [admin]]))).
% 2.71/3.47 ncf('1.1.5.2.10.9.3.6.2.2',plain,[-(loca_level_below(admin, sbu, sbu))],extension(10 ^ 9,bind([[_143865, _143867], [sbu, admin]]))).
% 2.71/3.47 ncf('1.1.5.2.10.9.3.7',plain,[-(system_indi_is_level_admin(system, level_admin))],extension(494 ^ 7)).
% 2.71/3.47 ncf('1.1.5.2.10.9.3.8',plain,[-(level_admin_indi_has_level(level_admin, alice, topsecret))],extension(508 ^ 7)).
% 2.71/3.47 ncf('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(12 ^ 7,bind([[_144003, _144005, _144007, _144009], [topsecret, secret, sbu, admin]]))).
% 2.71/3.47 ncf('1.1.5.2.10.9.3.9.1',plain,[-(loca_level_direct_below(admin, secret, topsecret))],extension(8 ^ 8,bind([[_143772], [admin]]))).
% 2.71/3.47 ncf('1.1.5.2.10.9.3.9.2',plain,[-(loca_level_below(admin, sbu, secret))],lemmata('[9, 10, 2, 5, 1, 1].x')).
% 2.71/3.47 ncf('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(162 ^ 7,bind([[_148987, _148989, _148991, _148993], [topsecret, background_admin, sbu, alice]]))).
% 2.71/3.47 ncf('1.1.5.2.10.9.3.10.1',plain,[-(system_indi_is_background_admin(system, background_admin))],extension(490 ^ 8)).
% 2.71/3.47 ncf('1.1.5.2.10.9.3.10.2',plain,[-(background_admin_indi_has_background(background_admin, alice, topsecret))],extension(502 ^ 8)).
% 2.71/3.47 ncf('1.1.5.2.10.9.3.10.3',plain,[-(loca_level_below(admin, sbu, topsecret))],lemmata('[9, 10, 2, 5, 1, 1].x')).
% 2.71/3.47 ncf('1.1.5.2.10.10',plain,[-(admin_indi_has_compartments(admin, alice, nil))],extension(238 ^ 5,bind([[_151244], [alice]]))).
% 2.71/3.47 %-----------------------------------------------------
% 2.71/3.47 End of proof for /export/starexec/sandbox/benchmark/theBenchmark.p
%------------------------------------------------------------------------------