%------------------------------------------------------------------------------
% File : ConnectPP---0.7.2
% Problem : SWV437+1 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : /export/starexec/sandbox2/solver/bin/connect++ --verbosity 1 --no-colour --tptp-proof --schedule default --timeout 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n008.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Thu Sep 24 09:03:43 AM UTC 2026
% Result : Theorem 2.15s 2.43s
% Output : Proof 2.15s
% Verified :
% SZS Type : Refutation
% Derivation depth : 8
% Number of leaves : 68
% Syntax : Number of formulae : 680 ( 487 unt; 0 def)
% Number of atoms : 1251 ( 0 equ)
% Maximal formula atoms : 11 ( 1 avg)
% Number of connectives : 1069 ( 498 ~; 494 |; 0 &)
% ( 0 <=>; 77 =>; 0 <=; 0 <~>)
% Maximal formula depth : 17 ( 3 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 51 ( 50 usr; 1 prp; 0-6 aty)
% Number of functors : 28 ( 28 usr; 27 con; 0-2 aty)
% Number of variables : 502 ( 31 sgn 393 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(ax0,axiom,
! [K] : loca_level_direct_below(K,unclassified,sbu),
file('SWV009+0.ax',ax0) ).
fof(ax1,axiom,
! [K] : loca_level_direct_below(K,sbu,confidential),
file('SWV009+0.ax',ax1) ).
fof(ax2,axiom,
! [K] : loca_level_direct_below(K,confidential,secret),
file('SWV009+0.ax',ax2) ).
fof(ax3,axiom,
! [K] : loca_level_direct_below(K,secret,topsecret),
file('SWV009+0.ax',ax3) ).
fof(ax4,axiom,
! [K,L] : loca_level_below(K,L,L),
file('SWV009+0.ax',ax4) ).
fof(ax5,axiom,
! [K,L,L1,L11] :
( loca_level_direct_below(K,L1,L11)
=> ( loca_level_below(K,L,L1)
=> loca_level_below(K,L,L11) ) ),
file('SWV009+0.ax',ax5) ).
fof(ax6,axiom,
! [C,SSO] :
( system_compartment_has_sso(system,C,SSO)
=> admin_compartment_has_sso(admin,C,SSO) ),
file('SWV009+0.ax',ax6) ).
fof(ax7,axiom,
! [OCA,C,SSO,SCG] :
( system_indi_is_oca(system,OCA)
=> ( oca_compartment_has_scg(OCA,C,SCG)
=> ( admin_compartment_has_sso(admin,C,SSO)
=> ( sso_compartment_has_scg(SSO,C,SCG)
=> admin_compartment_has_scg(admin,C,SCG) ) ) ) ),
file('SWV009+0.ax',ax7) ).
fof(ax8,axiom,
! [F,CL] :
( system_file_needs_compartments(system,F,CL)
=> ( admin_file_has_compartments_h(admin,F,CL,CL)
=> admin_file_has_compartments(admin,F,CL) ) ),
file('SWV009+0.ax',ax8) ).
fof(ax9,axiom,
! [F,CL] : admin_file_has_compartments_h(admin,F,CL,nil),
file('SWV009+0.ax',ax9) ).
fof(ax10,axiom,
! [F,CL,C1,CL1,SSO] :
( admin_compartment_has_sso(admin,C1,SSO)
=> ( sso_file_has_compartments(SSO,F,CL)
=> ( admin_file_has_compartments_h(admin,F,CL,CL1)
=> admin_file_has_compartments_h(admin,F,CL,cons(C1,CL1)) ) ) ),
file('SWV009+0.ax',ax10) ).
fof(ax11,axiom,
! [F,L,CL] :
( system_file_needs_level(system,F,L)
=> ( admin_file_has_compartments(admin,F,CL)
=> ( admin_file_has_level_h(admin,F,L,CL)
=> admin_file_has_level(admin,F,L) ) ) ),
file('SWV009+0.ax',ax11) ).
fof(ax12,axiom,
! [F,L] : admin_file_has_level_h(admin,F,L,nil),
file('SWV009+0.ax',ax12) ).
fof(ax13,axiom,
! [F,L,C,CL,SSO,SCG] :
( admin_compartment_has_sso(admin,C,SSO)
=> ( admin_compartment_has_scg(admin,C,SCG)
=> ( sso_file_has_level(SSO,F,L,SCG)
=> ( admin_file_has_level_h(admin,F,L,CL)
=> admin_file_has_level_h(admin,F,L,cons(C,CL)) ) ) ) ),
file('SWV009+0.ax',ax13) ).
fof(ax17,axiom,
! [K,PA] :
( system_indi_is_polygraph_admin(system,PA)
=> ( polygraph_admin_indi_has_polygraph(PA,K)
=> admin_indi_has_polygraph(admin,K) ) ),
file('SWV009+0.ax',ax17) ).
fof(ax18,axiom,
! [K,CA] :
( system_indi_is_credit_admin(system,CA)
=> ( credit_admin_indi_has_credit(CA,K)
=> admin_indi_has_credit(admin,K) ) ),
file('SWV009+0.ax',ax18) ).
fof(ax20,axiom,
! [K,L,BA,L1] :
( system_indi_is_background_admin(system,BA)
=> ( background_admin_indi_has_background(BA,K,L1)
=> ( loca_level_below(admin,L,L1)
=> admin_indi_has_background(admin,K,L) ) ) ),
file('SWV009+0.ax',ax20) ).
fof(ax21,axiom,
! [K,HR] :
( system_indi_is_hr_admin(system,HR)
=> ( hr_admin_indi_has_employment(HR,K)
=> admin_indi_has_employment(admin,K) ) ),
file('SWV009+0.ax',ax21) ).
fof(ax23,axiom,
! [K,U] :
( system_indi_has_citizenship(system,K,U)
=> admin_indi_has_citizenship(admin,K,U) ),
file('SWV009+0.ax',ax23) ).
fof(ax25,axiom,
! [K,L,L1,LA,L11] :
( system_indi_needs_level(system,K,L1)
=> ( admin_indi_has_citizenship(admin,K,usa)
=> ( admin_indi_has_polygraph(admin,K)
=> ( admin_indi_has_employment(admin,K)
=> ( admin_indi_has_credit(admin,K)
=> ( loca_level_below(admin,L,L1)
=> ( system_indi_is_level_admin(system,LA)
=> ( level_admin_indi_has_level(LA,K,L11)
=> ( loca_level_below(admin,L,L11)
=> ( admin_indi_has_background(admin,K,L)
=> admin_indi_has_level(admin,K,L) ) ) ) ) ) ) ) ) ) ),
file('SWV009+0.ax',ax25) ).
fof(ax26,axiom,
! [K] : admin_indi_has_compartments(admin,K,nil),
file('SWV009+0.ax',ax26) ).
fof(ax27,axiom,
! [K,C,CL,SSO] :
( system_indi_needs_compartment(system,K,C)
=> ( admin_indi_has_employment(admin,K)
=> ( admin_indi_has_citizenship(admin,K,usa)
=> ( admin_indi_has_polygraph_for_compartment(admin,K,C)
=> ( admin_indi_has_credit_for_compartment(admin,K,C)
=> ( admin_compartment_has_sso(admin,C,SSO)
=> ( sso_indi_has_compartment(SSO,K,C)
=> ( admin_indi_has_background_for_compartment(admin,K,C)
=> ( admin_indi_has_level_for_compartment(admin,K,C)
=> ( admin_indi_has_compartments(admin,K,CL)
=> admin_indi_has_compartments(admin,K,cons(C,CL)) ) ) ) ) ) ) ) ) ) ),
file('SWV009+0.ax',ax27) ).
fof(ax28,axiom,
! [K,C,OCA,L1,L2,B1,B2] :
( system_indi_is_oca(system,OCA)
=> ( oca_compartment_is_compartment(OCA,C,L1,L2,B1,B2)
=> ( admin_indi_has_background(admin,K,L2)
=> admin_indi_has_background_for_compartment(admin,K,C) ) ) ),
file('SWV009+0.ax',ax28) ).
fof(ax29,axiom,
! [K,C,OCA,L1,L2,B1,B2] :
( system_indi_is_oca(system,OCA)
=> ( oca_compartment_is_compartment(OCA,C,L1,L2,B1,B2)
=> ( admin_indi_has_level(admin,K,L1)
=> admin_indi_has_level_for_compartment(admin,K,C) ) ) ),
file('SWV009+0.ax',ax29) ).
fof(ax30,axiom,
! [K,C,OCA,L1,L2,B1] :
( system_indi_is_oca(system,OCA)
=> ( oca_compartment_is_compartment(OCA,C,L1,L2,B1,yes)
=> ( admin_indi_has_polygraph(admin,K)
=> admin_indi_has_polygraph_for_compartment(admin,K,C) ) ) ),
file('SWV009+0.ax',ax30) ).
fof(ax31,axiom,
! [K,C,OCA,L1,L2,B1] :
( system_indi_is_oca(system,OCA)
=> ( oca_compartment_is_compartment(OCA,C,L1,L2,B1,no)
=> admin_indi_has_polygraph_for_compartment(admin,K,C) ) ),
file('SWV009+0.ax',ax31) ).
fof(ax32,axiom,
! [K,C,OCA,L1,L2,B2] :
( system_indi_is_oca(system,OCA)
=> ( oca_compartment_is_compartment(OCA,C,L1,L2,yes,B2)
=> ( admin_indi_has_credit(admin,K)
=> admin_indi_has_credit_for_compartment(admin,K,C) ) ) ),
file('SWV009+0.ax',ax32) ).
fof(ax33,axiom,
! [K,C,OCA,L1,L2,B2] :
( system_indi_is_oca(system,OCA)
=> ( oca_compartment_is_compartment(OCA,C,L1,L2,no,B2)
=> admin_indi_has_credit_for_compartment(admin,K,C) ) ),
file('SWV009+0.ax',ax33) ).
fof(ax34,axiom,
! [K,F,CL] :
( admin_file_has_compartments(admin,F,CL)
=> ( admin_indi_has_compartments(admin,K,CL)
=> admin_indi_has_compartments_for_file(admin,K,F) ) ),
file('SWV009+0.ax',ax34) ).
fof(ax35,axiom,
! [K,F,L] :
( admin_file_has_level(admin,F,L)
=> ( admin_indi_has_level(admin,K,L)
=> admin_indi_has_level_for_file(admin,K,F) ) ),
file('SWV009+0.ax',ax35) ).
fof(ax36,axiom,
! [K,F,OWR] :
( state_file_has_owner(F,OWR)
=> ( owner_indi_has_need_to_know(OWR,K,F)
=> admin_indi_has_need_to_know_for_file(admin,K,F) ) ),
file('SWV009+0.ax',ax36) ).
fof(ax38,axiom,
! [K,F] :
( admin_indi_has_citizenship(admin,K,usa)
=> admin_indi_has_citizenship_for_file(admin,K,F) ),
file('SWV009+0.ax',ax38) ).
fof(ax39,axiom,
! [K,F] :
( state_file_is_not_working_paper(F)
=> ( admin_indi_has_citizenship_for_file(admin,K,F)
=> ( admin_indi_has_need_to_know_for_file(admin,K,F)
=> ( admin_indi_has_level_for_file(admin,K,F)
=> ( admin_indi_has_compartments_for_file(admin,K,F)
=> admin_indi_may_file(admin,K,F,read) ) ) ) ) ),
file('SWV009+0.ax',ax39) ).
fof(ax41,hypothesis,
system_indi_is_oca(system,oca),
file('theBenchmark.p',ax41) ).
fof(ax42,hypothesis,
oca_compartment_is_compartment(oca,compartmentb,confidential,topsecret,yes,yes),
file('theBenchmark.p',ax42) ).
fof(ax43,hypothesis,
oca_compartment_is_compartment(oca,compartmenta,sbu,unclassified,no,no),
file('theBenchmark.p',ax43) ).
fof(ax44,hypothesis,
system_compartment_has_sso(system,compartmentb,sso_compartmentb),
file('theBenchmark.p',ax44) ).
fof(ax45,hypothesis,
oca_compartment_has_scg(oca,compartmentb,scg_compartmentb),
file('theBenchmark.p',ax45) ).
fof(ax46,hypothesis,
sso_compartment_has_scg(sso_compartmentb,compartmentb,scg_compartmentb),
file('theBenchmark.p',ax46) ).
fof(ax47,hypothesis,
system_compartment_has_sso(system,compartmenta,sso_compartmenta),
file('theBenchmark.p',ax47) ).
fof(ax48,hypothesis,
oca_compartment_has_scg(oca,compartmenta,scg_compartmenta),
file('theBenchmark.p',ax48) ).
fof(ax49,hypothesis,
sso_compartment_has_scg(sso_compartmenta,compartmenta,scg_compartmenta),
file('theBenchmark.p',ax49) ).
fof(ax50,hypothesis,
state_file_is_not_working_paper(secretfile),
file('theBenchmark.p',ax50) ).
fof(ax51,hypothesis,
system_file_needs_compartments(system,secretfile,cons(compartmentb,cons(compartmenta,nil))),
file('theBenchmark.p',ax51) ).
fof(ax52,hypothesis,
sso_file_has_compartments(sso_compartmentb,secretfile,cons(compartmentb,cons(compartmenta,nil))),
file('theBenchmark.p',ax52) ).
fof(ax53,hypothesis,
sso_file_has_compartments(sso_compartmenta,secretfile,cons(compartmentb,cons(compartmenta,nil))),
file('theBenchmark.p',ax53) ).
fof(ax54,hypothesis,
system_file_needs_level(system,secretfile,secret),
file('theBenchmark.p',ax54) ).
fof(ax55,hypothesis,
sso_file_has_level(sso_compartmentb,secretfile,secret,scg_compartmentb),
file('theBenchmark.p',ax55) ).
fof(ax56,hypothesis,
sso_file_has_level(sso_compartmenta,secretfile,secret,scg_compartmenta),
file('theBenchmark.p',ax56) ).
fof(ax60,hypothesis,
state_file_has_owner(secretfile,owner_secretfile),
file('theBenchmark.p',ax60) ).
fof(ax66,hypothesis,
system_indi_is_polygraph_admin(system,polygraph_admin),
file('theBenchmark.p',ax66) ).
fof(ax67,hypothesis,
system_indi_is_credit_admin(system,credit_admin),
file('theBenchmark.p',ax67) ).
fof(ax68,hypothesis,
system_indi_is_background_admin(system,background_admin),
file('theBenchmark.p',ax68) ).
fof(ax69,hypothesis,
system_indi_is_hr_admin(system,hr_admin),
file('theBenchmark.p',ax69) ).
fof(ax70,hypothesis,
system_indi_is_level_admin(system,level_admin),
file('theBenchmark.p',ax70) ).
fof(ax71,hypothesis,
system_indi_has_citizenship(system,alice,usa),
file('theBenchmark.p',ax71) ).
fof(ax72,hypothesis,
polygraph_admin_indi_has_polygraph(polygraph_admin,alice),
file('theBenchmark.p',ax72) ).
fof(ax73,hypothesis,
credit_admin_indi_has_credit(credit_admin,alice),
file('theBenchmark.p',ax73) ).
fof(ax74,hypothesis,
background_admin_indi_has_background(background_admin,alice,topsecret),
file('theBenchmark.p',ax74) ).
fof(ax75,hypothesis,
hr_admin_indi_has_employment(hr_admin,alice),
file('theBenchmark.p',ax75) ).
fof(ax76,hypothesis,
system_indi_needs_level(system,alice,secret),
file('theBenchmark.p',ax76) ).
fof(ax77,hypothesis,
level_admin_indi_has_level(level_admin,alice,topsecret),
file('theBenchmark.p',ax77) ).
fof(ax78,hypothesis,
system_indi_needs_compartment(system,alice,compartmentb),
file('theBenchmark.p',ax78) ).
fof(ax79,hypothesis,
system_indi_needs_compartment(system,alice,compartmenta),
file('theBenchmark.p',ax79) ).
fof(ax80,hypothesis,
sso_indi_has_compartment(sso_compartmentb,alice,compartmentb),
file('theBenchmark.p',ax80) ).
fof(ax81,hypothesis,
sso_indi_has_compartment(sso_compartmenta,alice,compartmenta),
file('theBenchmark.p',ax81) ).
fof(ax82,hypothesis,
owner_indi_has_need_to_know(owner_secretfile,alice,secretfile),
file('theBenchmark.p',ax82) ).
fof(alicereadsecret,conjecture,
admin_indi_may_file(admin,alice,secretfile,read),
file('theBenchmark.p',alicereadsecret) ).
fof(f_1_1,plain,
! [K] : loca_level_direct_below(K,unclassified,sbu),
inference(fof_nnf,[status(thm)],[ax0]) ).
fof(f_1_2,plain,
! [U_0] : loca_level_direct_below(U_0,unclassified,sbu),
inference(variable_rename,[status(thm)],[f_1_1]) ).
cnf(f_1_3,plain,
loca_level_direct_below(U_0,unclassified,sbu),
inference(clausify,[status(thm)],[f_1_2]) ).
fof(f_2_1,plain,
! [K] : loca_level_direct_below(K,sbu,confidential),
inference(fof_nnf,[status(thm)],[ax1]) ).
fof(f_2_2,plain,
! [U_1] : loca_level_direct_below(U_1,sbu,confidential),
inference(variable_rename,[status(thm)],[f_2_1]) ).
cnf(f_2_3,plain,
loca_level_direct_below(U_1,sbu,confidential),
inference(clausify,[status(thm)],[f_2_2]) ).
fof(f_3_1,plain,
! [K] : loca_level_direct_below(K,confidential,secret),
inference(fof_nnf,[status(thm)],[ax2]) ).
fof(f_3_2,plain,
! [U_2] : loca_level_direct_below(U_2,confidential,secret),
inference(variable_rename,[status(thm)],[f_3_1]) ).
cnf(f_3_3,plain,
loca_level_direct_below(U_2,confidential,secret),
inference(clausify,[status(thm)],[f_3_2]) ).
fof(f_4_1,plain,
! [K] : loca_level_direct_below(K,secret,topsecret),
inference(fof_nnf,[status(thm)],[ax3]) ).
fof(f_4_2,plain,
! [U_3] : loca_level_direct_below(U_3,secret,topsecret),
inference(variable_rename,[status(thm)],[f_4_1]) ).
cnf(f_4_3,plain,
loca_level_direct_below(U_3,secret,topsecret),
inference(clausify,[status(thm)],[f_4_2]) ).
fof(f_5_1,plain,
! [K,L] : loca_level_below(K,L,L),
inference(fof_nnf,[status(thm)],[ax4]) ).
fof(f_5_2,plain,
! [U_5,U_4] : loca_level_below(U_5,U_4,U_4),
inference(variable_rename,[status(thm)],[f_5_1]) ).
cnf(f_5_3,plain,
loca_level_below(U_5,U_4,U_4),
inference(clausify,[status(thm)],[f_5_2]) ).
fof(f_6_1,plain,
! [K,L,L1,L11] :
( loca_level_below(K,L,L11)
| ~ loca_level_below(K,L,L1)
| ~ loca_level_direct_below(K,L1,L11) ),
inference(fof_nnf,[status(thm)],[ax5]) ).
fof(f_6_2,plain,
! [U_9,U_8,U_7,U_6] :
( loca_level_below(U_9,U_8,U_6)
| ~ loca_level_below(U_9,U_8,U_7)
| ~ loca_level_direct_below(U_9,U_7,U_6) ),
inference(variable_rename,[status(thm)],[f_6_1]) ).
cnf(f_6_3,plain,
( loca_level_below(U_9,U_8,U_6)
| ~ loca_level_below(U_9,U_8,U_7)
| ~ loca_level_direct_below(U_9,U_7,U_6) ),
inference(clausify,[status(thm)],[f_6_2]) ).
fof(f_7_1,plain,
! [C,SSO] :
( admin_compartment_has_sso(admin,C,SSO)
| ~ system_compartment_has_sso(system,C,SSO) ),
inference(fof_nnf,[status(thm)],[ax6]) ).
fof(f_7_2,plain,
! [U_11,U_10] :
( admin_compartment_has_sso(admin,U_11,U_10)
| ~ system_compartment_has_sso(system,U_11,U_10) ),
inference(variable_rename,[status(thm)],[f_7_1]) ).
cnf(f_7_3,plain,
( admin_compartment_has_sso(admin,U_11,U_10)
| ~ system_compartment_has_sso(system,U_11,U_10) ),
inference(clausify,[status(thm)],[f_7_2]) ).
fof(f_8_1,plain,
! [OCA,C,SSO,SCG] :
( admin_compartment_has_scg(admin,C,SCG)
| ~ sso_compartment_has_scg(SSO,C,SCG)
| ~ admin_compartment_has_sso(admin,C,SSO)
| ~ oca_compartment_has_scg(OCA,C,SCG)
| ~ system_indi_is_oca(system,OCA) ),
inference(fof_nnf,[status(thm)],[ax7]) ).
fof(f_8_2,plain,
! [U_15,U_14,U_13,U_12] :
( admin_compartment_has_scg(admin,U_14,U_12)
| ~ sso_compartment_has_scg(U_13,U_14,U_12)
| ~ admin_compartment_has_sso(admin,U_14,U_13)
| ~ oca_compartment_has_scg(U_15,U_14,U_12)
| ~ system_indi_is_oca(system,U_15) ),
inference(variable_rename,[status(thm)],[f_8_1]) ).
fof(f_8_3,plain,
! [U_15] :
( ! [U_14,U_13,U_12] :
( admin_compartment_has_scg(admin,U_14,U_12)
| ~ sso_compartment_has_scg(U_13,U_14,U_12)
| ~ admin_compartment_has_sso(admin,U_14,U_13)
| ~ oca_compartment_has_scg(U_15,U_14,U_12) )
| ~ system_indi_is_oca(system,U_15) ),
inference(miniscope,[status(thm)],[f_8_2]) ).
cnf(f_8_4,plain,
( admin_compartment_has_scg(admin,U_14,U_12)
| ~ sso_compartment_has_scg(U_13,U_14,U_12)
| ~ admin_compartment_has_sso(admin,U_14,U_13)
| ~ oca_compartment_has_scg(U_15,U_14,U_12)
| ~ system_indi_is_oca(system,U_15) ),
inference(clausify,[status(thm)],[f_8_3]) ).
fof(f_9_1,plain,
! [F,CL] :
( admin_file_has_compartments(admin,F,CL)
| ~ admin_file_has_compartments_h(admin,F,CL,CL)
| ~ system_file_needs_compartments(system,F,CL) ),
inference(fof_nnf,[status(thm)],[ax8]) ).
fof(f_9_2,plain,
! [U_17,U_16] :
( admin_file_has_compartments(admin,U_17,U_16)
| ~ admin_file_has_compartments_h(admin,U_17,U_16,U_16)
| ~ system_file_needs_compartments(system,U_17,U_16) ),
inference(variable_rename,[status(thm)],[f_9_1]) ).
cnf(f_9_3,plain,
( admin_file_has_compartments(admin,U_17,U_16)
| ~ admin_file_has_compartments_h(admin,U_17,U_16,U_16)
| ~ system_file_needs_compartments(system,U_17,U_16) ),
inference(clausify,[status(thm)],[f_9_2]) ).
fof(f_10_1,plain,
! [F,CL] : admin_file_has_compartments_h(admin,F,CL,nil),
inference(fof_nnf,[status(thm)],[ax9]) ).
fof(f_10_2,plain,
! [U_19,U_18] : admin_file_has_compartments_h(admin,U_19,U_18,nil),
inference(variable_rename,[status(thm)],[f_10_1]) ).
cnf(f_10_3,plain,
admin_file_has_compartments_h(admin,U_19,U_18,nil),
inference(clausify,[status(thm)],[f_10_2]) ).
fof(f_11_1,plain,
! [F,CL,C1,CL1,SSO] :
( admin_file_has_compartments_h(admin,F,CL,cons(C1,CL1))
| ~ admin_file_has_compartments_h(admin,F,CL,CL1)
| ~ sso_file_has_compartments(SSO,F,CL)
| ~ admin_compartment_has_sso(admin,C1,SSO) ),
inference(fof_nnf,[status(thm)],[ax10]) ).
fof(f_11_2,plain,
! [U_24,U_23,U_22,U_21,U_20] :
( admin_file_has_compartments_h(admin,U_24,U_23,cons(U_22,U_21))
| ~ admin_file_has_compartments_h(admin,U_24,U_23,U_21)
| ~ sso_file_has_compartments(U_20,U_24,U_23)
| ~ admin_compartment_has_sso(admin,U_22,U_20) ),
inference(variable_rename,[status(thm)],[f_11_1]) ).
cnf(f_11_3,plain,
( admin_file_has_compartments_h(admin,U_24,U_23,cons(U_22,U_21))
| ~ admin_file_has_compartments_h(admin,U_24,U_23,U_21)
| ~ sso_file_has_compartments(U_20,U_24,U_23)
| ~ admin_compartment_has_sso(admin,U_22,U_20) ),
inference(clausify,[status(thm)],[f_11_2]) ).
fof(f_12_1,plain,
! [F,L,CL] :
( admin_file_has_level(admin,F,L)
| ~ admin_file_has_level_h(admin,F,L,CL)
| ~ admin_file_has_compartments(admin,F,CL)
| ~ system_file_needs_level(system,F,L) ),
inference(fof_nnf,[status(thm)],[ax11]) ).
fof(f_12_2,plain,
! [U_27,U_26,U_25] :
( admin_file_has_level(admin,U_27,U_26)
| ~ admin_file_has_level_h(admin,U_27,U_26,U_25)
| ~ admin_file_has_compartments(admin,U_27,U_25)
| ~ system_file_needs_level(system,U_27,U_26) ),
inference(variable_rename,[status(thm)],[f_12_1]) ).
fof(f_12_3,plain,
! [U_27,U_26] :
( ! [U_25] :
( admin_file_has_level(admin,U_27,U_26)
| ~ admin_file_has_level_h(admin,U_27,U_26,U_25)
| ~ admin_file_has_compartments(admin,U_27,U_25) )
| ~ system_file_needs_level(system,U_27,U_26) ),
inference(miniscope,[status(thm)],[f_12_2]) ).
cnf(f_12_4,plain,
( admin_file_has_level(admin,U_27,U_26)
| ~ admin_file_has_level_h(admin,U_27,U_26,U_25)
| ~ admin_file_has_compartments(admin,U_27,U_25)
| ~ system_file_needs_level(system,U_27,U_26) ),
inference(clausify,[status(thm)],[f_12_3]) ).
fof(f_13_1,plain,
! [F,L] : admin_file_has_level_h(admin,F,L,nil),
inference(fof_nnf,[status(thm)],[ax12]) ).
fof(f_13_2,plain,
! [U_29,U_28] : admin_file_has_level_h(admin,U_29,U_28,nil),
inference(variable_rename,[status(thm)],[f_13_1]) ).
cnf(f_13_3,plain,
admin_file_has_level_h(admin,U_29,U_28,nil),
inference(clausify,[status(thm)],[f_13_2]) ).
fof(f_14_1,plain,
! [F,L,C,CL,SSO,SCG] :
( admin_file_has_level_h(admin,F,L,cons(C,CL))
| ~ admin_file_has_level_h(admin,F,L,CL)
| ~ sso_file_has_level(SSO,F,L,SCG)
| ~ admin_compartment_has_scg(admin,C,SCG)
| ~ admin_compartment_has_sso(admin,C,SSO) ),
inference(fof_nnf,[status(thm)],[ax13]) ).
fof(f_14_2,plain,
! [U_35,U_34,U_33,U_32,U_31,U_30] :
( admin_file_has_level_h(admin,U_35,U_34,cons(U_33,U_32))
| ~ admin_file_has_level_h(admin,U_35,U_34,U_32)
| ~ sso_file_has_level(U_31,U_35,U_34,U_30)
| ~ admin_compartment_has_scg(admin,U_33,U_30)
| ~ admin_compartment_has_sso(admin,U_33,U_31) ),
inference(variable_rename,[status(thm)],[f_14_1]) ).
fof(f_14_3,plain,
! [U_35,U_34,U_33,U_32,U_31] :
( ! [U_30] :
( admin_file_has_level_h(admin,U_35,U_34,cons(U_33,U_32))
| ~ admin_file_has_level_h(admin,U_35,U_34,U_32)
| ~ sso_file_has_level(U_31,U_35,U_34,U_30)
| ~ admin_compartment_has_scg(admin,U_33,U_30) )
| ~ admin_compartment_has_sso(admin,U_33,U_31) ),
inference(miniscope,[status(thm)],[f_14_2]) ).
cnf(f_14_4,plain,
( admin_file_has_level_h(admin,U_35,U_34,cons(U_33,U_32))
| ~ admin_file_has_level_h(admin,U_35,U_34,U_32)
| ~ sso_file_has_level(U_31,U_35,U_34,U_30)
| ~ admin_compartment_has_scg(admin,U_33,U_30)
| ~ admin_compartment_has_sso(admin,U_33,U_31) ),
inference(clausify,[status(thm)],[f_14_3]) ).
fof(f_18_1,plain,
! [K,PA] :
( admin_indi_has_polygraph(admin,K)
| ~ polygraph_admin_indi_has_polygraph(PA,K)
| ~ system_indi_is_polygraph_admin(system,PA) ),
inference(fof_nnf,[status(thm)],[ax17]) ).
fof(f_18_2,plain,
! [U_48,U_47] :
( admin_indi_has_polygraph(admin,U_48)
| ~ polygraph_admin_indi_has_polygraph(U_47,U_48)
| ~ system_indi_is_polygraph_admin(system,U_47) ),
inference(variable_rename,[status(thm)],[f_18_1]) ).
cnf(f_18_3,plain,
( admin_indi_has_polygraph(admin,U_48)
| ~ polygraph_admin_indi_has_polygraph(U_47,U_48)
| ~ system_indi_is_polygraph_admin(system,U_47) ),
inference(clausify,[status(thm)],[f_18_2]) ).
fof(f_19_1,plain,
! [K,CA] :
( admin_indi_has_credit(admin,K)
| ~ credit_admin_indi_has_credit(CA,K)
| ~ system_indi_is_credit_admin(system,CA) ),
inference(fof_nnf,[status(thm)],[ax18]) ).
fof(f_19_2,plain,
! [U_50,U_49] :
( admin_indi_has_credit(admin,U_50)
| ~ credit_admin_indi_has_credit(U_49,U_50)
| ~ system_indi_is_credit_admin(system,U_49) ),
inference(variable_rename,[status(thm)],[f_19_1]) ).
cnf(f_19_3,plain,
( admin_indi_has_credit(admin,U_50)
| ~ credit_admin_indi_has_credit(U_49,U_50)
| ~ system_indi_is_credit_admin(system,U_49) ),
inference(clausify,[status(thm)],[f_19_2]) ).
fof(f_21_1,plain,
! [K,L,BA,L1] :
( admin_indi_has_background(admin,K,L)
| ~ loca_level_below(admin,L,L1)
| ~ background_admin_indi_has_background(BA,K,L1)
| ~ system_indi_is_background_admin(system,BA) ),
inference(fof_nnf,[status(thm)],[ax20]) ).
fof(f_21_2,plain,
! [U_55,U_54,U_53,U_52] :
( admin_indi_has_background(admin,U_55,U_54)
| ~ loca_level_below(admin,U_54,U_52)
| ~ background_admin_indi_has_background(U_53,U_55,U_52)
| ~ system_indi_is_background_admin(system,U_53) ),
inference(variable_rename,[status(thm)],[f_21_1]) ).
fof(f_21_3,plain,
! [U_55,U_54,U_53] :
( ! [U_52] :
( admin_indi_has_background(admin,U_55,U_54)
| ~ loca_level_below(admin,U_54,U_52)
| ~ background_admin_indi_has_background(U_53,U_55,U_52) )
| ~ system_indi_is_background_admin(system,U_53) ),
inference(miniscope,[status(thm)],[f_21_2]) ).
cnf(f_21_4,plain,
( admin_indi_has_background(admin,U_55,U_54)
| ~ loca_level_below(admin,U_54,U_52)
| ~ background_admin_indi_has_background(U_53,U_55,U_52)
| ~ system_indi_is_background_admin(system,U_53) ),
inference(clausify,[status(thm)],[f_21_3]) ).
fof(f_22_1,plain,
! [K,HR] :
( admin_indi_has_employment(admin,K)
| ~ hr_admin_indi_has_employment(HR,K)
| ~ system_indi_is_hr_admin(system,HR) ),
inference(fof_nnf,[status(thm)],[ax21]) ).
fof(f_22_2,plain,
! [U_57,U_56] :
( admin_indi_has_employment(admin,U_57)
| ~ hr_admin_indi_has_employment(U_56,U_57)
| ~ system_indi_is_hr_admin(system,U_56) ),
inference(variable_rename,[status(thm)],[f_22_1]) ).
cnf(f_22_3,plain,
( admin_indi_has_employment(admin,U_57)
| ~ hr_admin_indi_has_employment(U_56,U_57)
| ~ system_indi_is_hr_admin(system,U_56) ),
inference(clausify,[status(thm)],[f_22_2]) ).
fof(f_24_1,plain,
! [K,U] :
( admin_indi_has_citizenship(admin,K,U)
| ~ system_indi_has_citizenship(system,K,U) ),
inference(fof_nnf,[status(thm)],[ax23]) ).
fof(f_24_2,plain,
! [U_60,U_59] :
( admin_indi_has_citizenship(admin,U_60,U_59)
| ~ system_indi_has_citizenship(system,U_60,U_59) ),
inference(variable_rename,[status(thm)],[f_24_1]) ).
cnf(f_24_3,plain,
( admin_indi_has_citizenship(admin,U_60,U_59)
| ~ system_indi_has_citizenship(system,U_60,U_59) ),
inference(clausify,[status(thm)],[f_24_2]) ).
fof(f_26_1,plain,
! [K,L,L1,LA,L11] :
( admin_indi_has_level(admin,K,L)
| ~ admin_indi_has_background(admin,K,L)
| ~ loca_level_below(admin,L,L11)
| ~ level_admin_indi_has_level(LA,K,L11)
| ~ system_indi_is_level_admin(system,LA)
| ~ loca_level_below(admin,L,L1)
| ~ admin_indi_has_credit(admin,K)
| ~ admin_indi_has_employment(admin,K)
| ~ admin_indi_has_polygraph(admin,K)
| ~ admin_indi_has_citizenship(admin,K,usa)
| ~ system_indi_needs_level(system,K,L1) ),
inference(fof_nnf,[status(thm)],[ax25]) ).
fof(f_26_2,plain,
! [U_66,U_65,U_64,U_63,U_62] :
( admin_indi_has_level(admin,U_66,U_65)
| ~ admin_indi_has_background(admin,U_66,U_65)
| ~ loca_level_below(admin,U_65,U_62)
| ~ level_admin_indi_has_level(U_63,U_66,U_62)
| ~ system_indi_is_level_admin(system,U_63)
| ~ loca_level_below(admin,U_65,U_64)
| ~ admin_indi_has_credit(admin,U_66)
| ~ admin_indi_has_employment(admin,U_66)
| ~ admin_indi_has_polygraph(admin,U_66)
| ~ admin_indi_has_citizenship(admin,U_66,usa)
| ~ system_indi_needs_level(system,U_66,U_64) ),
inference(variable_rename,[status(thm)],[f_26_1]) ).
fof(f_26_3,plain,
! [U_66,U_65,U_64] :
( ! [U_63] :
( ! [U_62] :
( admin_indi_has_level(admin,U_66,U_65)
| ~ admin_indi_has_background(admin,U_66,U_65)
| ~ loca_level_below(admin,U_65,U_62)
| ~ level_admin_indi_has_level(U_63,U_66,U_62) )
| ~ system_indi_is_level_admin(system,U_63) )
| ~ loca_level_below(admin,U_65,U_64)
| ~ admin_indi_has_credit(admin,U_66)
| ~ admin_indi_has_employment(admin,U_66)
| ~ admin_indi_has_polygraph(admin,U_66)
| ~ admin_indi_has_citizenship(admin,U_66,usa)
| ~ system_indi_needs_level(system,U_66,U_64) ),
inference(miniscope,[status(thm)],[f_26_2]) ).
cnf(f_26_4,plain,
( admin_indi_has_level(admin,U_66,U_65)
| ~ admin_indi_has_background(admin,U_66,U_65)
| ~ loca_level_below(admin,U_65,U_62)
| ~ level_admin_indi_has_level(U_63,U_66,U_62)
| ~ system_indi_is_level_admin(system,U_63)
| ~ loca_level_below(admin,U_65,U_64)
| ~ admin_indi_has_credit(admin,U_66)
| ~ admin_indi_has_employment(admin,U_66)
| ~ admin_indi_has_polygraph(admin,U_66)
| ~ admin_indi_has_citizenship(admin,U_66,usa)
| ~ system_indi_needs_level(system,U_66,U_64) ),
inference(clausify,[status(thm)],[f_26_3]) ).
fof(f_27_1,plain,
! [K] : admin_indi_has_compartments(admin,K,nil),
inference(fof_nnf,[status(thm)],[ax26]) ).
fof(f_27_2,plain,
! [U_67] : admin_indi_has_compartments(admin,U_67,nil),
inference(variable_rename,[status(thm)],[f_27_1]) ).
cnf(f_27_3,plain,
admin_indi_has_compartments(admin,U_67,nil),
inference(clausify,[status(thm)],[f_27_2]) ).
fof(f_28_1,plain,
! [K,C,CL,SSO] :
( admin_indi_has_compartments(admin,K,cons(C,CL))
| ~ admin_indi_has_compartments(admin,K,CL)
| ~ admin_indi_has_level_for_compartment(admin,K,C)
| ~ admin_indi_has_background_for_compartment(admin,K,C)
| ~ sso_indi_has_compartment(SSO,K,C)
| ~ admin_compartment_has_sso(admin,C,SSO)
| ~ admin_indi_has_credit_for_compartment(admin,K,C)
| ~ admin_indi_has_polygraph_for_compartment(admin,K,C)
| ~ admin_indi_has_citizenship(admin,K,usa)
| ~ admin_indi_has_employment(admin,K)
| ~ system_indi_needs_compartment(system,K,C) ),
inference(fof_nnf,[status(thm)],[ax27]) ).
fof(f_28_2,plain,
! [U_71,U_70,U_69,U_68] :
( admin_indi_has_compartments(admin,U_71,cons(U_70,U_69))
| ~ admin_indi_has_compartments(admin,U_71,U_69)
| ~ admin_indi_has_level_for_compartment(admin,U_71,U_70)
| ~ admin_indi_has_background_for_compartment(admin,U_71,U_70)
| ~ sso_indi_has_compartment(U_68,U_71,U_70)
| ~ admin_compartment_has_sso(admin,U_70,U_68)
| ~ admin_indi_has_credit_for_compartment(admin,U_71,U_70)
| ~ admin_indi_has_polygraph_for_compartment(admin,U_71,U_70)
| ~ admin_indi_has_citizenship(admin,U_71,usa)
| ~ admin_indi_has_employment(admin,U_71)
| ~ system_indi_needs_compartment(system,U_71,U_70) ),
inference(variable_rename,[status(thm)],[f_28_1]) ).
fof(f_28_3,plain,
! [U_71,U_70] :
( ! [U_69,U_68] :
( admin_indi_has_compartments(admin,U_71,cons(U_70,U_69))
| ~ admin_indi_has_compartments(admin,U_71,U_69)
| ~ admin_indi_has_level_for_compartment(admin,U_71,U_70)
| ~ admin_indi_has_background_for_compartment(admin,U_71,U_70)
| ~ sso_indi_has_compartment(U_68,U_71,U_70)
| ~ admin_compartment_has_sso(admin,U_70,U_68) )
| ~ admin_indi_has_credit_for_compartment(admin,U_71,U_70)
| ~ admin_indi_has_polygraph_for_compartment(admin,U_71,U_70)
| ~ admin_indi_has_citizenship(admin,U_71,usa)
| ~ admin_indi_has_employment(admin,U_71)
| ~ system_indi_needs_compartment(system,U_71,U_70) ),
inference(miniscope,[status(thm)],[f_28_2]) ).
cnf(f_28_4,plain,
( admin_indi_has_compartments(admin,U_71,cons(U_70,U_69))
| ~ admin_indi_has_compartments(admin,U_71,U_69)
| ~ admin_indi_has_level_for_compartment(admin,U_71,U_70)
| ~ admin_indi_has_background_for_compartment(admin,U_71,U_70)
| ~ sso_indi_has_compartment(U_68,U_71,U_70)
| ~ admin_compartment_has_sso(admin,U_70,U_68)
| ~ admin_indi_has_credit_for_compartment(admin,U_71,U_70)
| ~ admin_indi_has_polygraph_for_compartment(admin,U_71,U_70)
| ~ admin_indi_has_citizenship(admin,U_71,usa)
| ~ admin_indi_has_employment(admin,U_71)
| ~ system_indi_needs_compartment(system,U_71,U_70) ),
inference(clausify,[status(thm)],[f_28_3]) ).
fof(f_29_1,plain,
! [K,C,OCA,L1,L2,B1,B2] :
( admin_indi_has_background_for_compartment(admin,K,C)
| ~ admin_indi_has_background(admin,K,L2)
| ~ oca_compartment_is_compartment(OCA,C,L1,L2,B1,B2)
| ~ system_indi_is_oca(system,OCA) ),
inference(fof_nnf,[status(thm)],[ax28]) ).
fof(f_29_2,plain,
! [U_78,U_77,U_76,U_75,U_74,U_73,U_72] :
( admin_indi_has_background_for_compartment(admin,U_78,U_77)
| ~ admin_indi_has_background(admin,U_78,U_74)
| ~ oca_compartment_is_compartment(U_76,U_77,U_75,U_74,U_73,U_72)
| ~ system_indi_is_oca(system,U_76) ),
inference(variable_rename,[status(thm)],[f_29_1]) ).
fof(f_29_3,plain,
! [U_78,U_77,U_76] :
( ! [U_75,U_74] :
( ! [U_73,U_72] : ~ oca_compartment_is_compartment(U_76,U_77,U_75,U_74,U_73,U_72)
| admin_indi_has_background_for_compartment(admin,U_78,U_77)
| ~ admin_indi_has_background(admin,U_78,U_74) )
| ~ system_indi_is_oca(system,U_76) ),
inference(miniscope,[status(thm)],[f_29_2]) ).
cnf(f_29_4,plain,
( ~ oca_compartment_is_compartment(U_76,U_77,U_75,U_74,U_73,U_72)
| admin_indi_has_background_for_compartment(admin,U_78,U_77)
| ~ admin_indi_has_background(admin,U_78,U_74)
| ~ system_indi_is_oca(system,U_76) ),
inference(clausify,[status(thm)],[f_29_3]) ).
fof(f_30_1,plain,
! [K,C,OCA,L1,L2,B1,B2] :
( admin_indi_has_level_for_compartment(admin,K,C)
| ~ admin_indi_has_level(admin,K,L1)
| ~ oca_compartment_is_compartment(OCA,C,L1,L2,B1,B2)
| ~ system_indi_is_oca(system,OCA) ),
inference(fof_nnf,[status(thm)],[ax29]) ).
fof(f_30_2,plain,
! [U_85,U_84,U_83,U_82,U_81,U_80,U_79] :
( admin_indi_has_level_for_compartment(admin,U_85,U_84)
| ~ admin_indi_has_level(admin,U_85,U_82)
| ~ oca_compartment_is_compartment(U_83,U_84,U_82,U_81,U_80,U_79)
| ~ system_indi_is_oca(system,U_83) ),
inference(variable_rename,[status(thm)],[f_30_1]) ).
fof(f_30_3,plain,
! [U_85,U_84,U_83] :
( ! [U_82] :
( ! [U_81,U_80,U_79] : ~ oca_compartment_is_compartment(U_83,U_84,U_82,U_81,U_80,U_79)
| admin_indi_has_level_for_compartment(admin,U_85,U_84)
| ~ admin_indi_has_level(admin,U_85,U_82) )
| ~ system_indi_is_oca(system,U_83) ),
inference(miniscope,[status(thm)],[f_30_2]) ).
cnf(f_30_4,plain,
( ~ oca_compartment_is_compartment(U_83,U_84,U_82,U_81,U_80,U_79)
| admin_indi_has_level_for_compartment(admin,U_85,U_84)
| ~ admin_indi_has_level(admin,U_85,U_82)
| ~ system_indi_is_oca(system,U_83) ),
inference(clausify,[status(thm)],[f_30_3]) ).
fof(f_31_1,plain,
! [K,C,OCA,L1,L2,B1] :
( admin_indi_has_polygraph_for_compartment(admin,K,C)
| ~ admin_indi_has_polygraph(admin,K)
| ~ oca_compartment_is_compartment(OCA,C,L1,L2,B1,yes)
| ~ system_indi_is_oca(system,OCA) ),
inference(fof_nnf,[status(thm)],[ax30]) ).
fof(f_31_2,plain,
! [U_91,U_90,U_89,U_88,U_87,U_86] :
( admin_indi_has_polygraph_for_compartment(admin,U_91,U_90)
| ~ admin_indi_has_polygraph(admin,U_91)
| ~ oca_compartment_is_compartment(U_89,U_90,U_88,U_87,U_86,yes)
| ~ system_indi_is_oca(system,U_89) ),
inference(variable_rename,[status(thm)],[f_31_1]) ).
fof(f_31_3,plain,
! [U_91,U_90,U_89] :
( ! [U_88,U_87,U_86] : ~ oca_compartment_is_compartment(U_89,U_90,U_88,U_87,U_86,yes)
| admin_indi_has_polygraph_for_compartment(admin,U_91,U_90)
| ~ admin_indi_has_polygraph(admin,U_91)
| ~ system_indi_is_oca(system,U_89) ),
inference(miniscope,[status(thm)],[f_31_2]) ).
cnf(f_31_4,plain,
( ~ oca_compartment_is_compartment(U_89,U_90,U_88,U_87,U_86,yes)
| admin_indi_has_polygraph_for_compartment(admin,U_91,U_90)
| ~ admin_indi_has_polygraph(admin,U_91)
| ~ system_indi_is_oca(system,U_89) ),
inference(clausify,[status(thm)],[f_31_3]) ).
fof(f_32_1,plain,
! [K,C,OCA,L1,L2,B1] :
( admin_indi_has_polygraph_for_compartment(admin,K,C)
| ~ oca_compartment_is_compartment(OCA,C,L1,L2,B1,no)
| ~ system_indi_is_oca(system,OCA) ),
inference(fof_nnf,[status(thm)],[ax31]) ).
fof(f_32_2,plain,
! [U_97,U_96,U_95,U_94,U_93,U_92] :
( admin_indi_has_polygraph_for_compartment(admin,U_97,U_96)
| ~ oca_compartment_is_compartment(U_95,U_96,U_94,U_93,U_92,no)
| ~ system_indi_is_oca(system,U_95) ),
inference(variable_rename,[status(thm)],[f_32_1]) ).
fof(f_32_3,plain,
! [U_97,U_96,U_95] :
( ! [U_94,U_93,U_92] : ~ oca_compartment_is_compartment(U_95,U_96,U_94,U_93,U_92,no)
| admin_indi_has_polygraph_for_compartment(admin,U_97,U_96)
| ~ system_indi_is_oca(system,U_95) ),
inference(miniscope,[status(thm)],[f_32_2]) ).
cnf(f_32_4,plain,
( ~ oca_compartment_is_compartment(U_95,U_96,U_94,U_93,U_92,no)
| admin_indi_has_polygraph_for_compartment(admin,U_97,U_96)
| ~ system_indi_is_oca(system,U_95) ),
inference(clausify,[status(thm)],[f_32_3]) ).
fof(f_33_1,plain,
! [K,C,OCA,L1,L2,B2] :
( admin_indi_has_credit_for_compartment(admin,K,C)
| ~ admin_indi_has_credit(admin,K)
| ~ oca_compartment_is_compartment(OCA,C,L1,L2,yes,B2)
| ~ system_indi_is_oca(system,OCA) ),
inference(fof_nnf,[status(thm)],[ax32]) ).
fof(f_33_2,plain,
! [U_103,U_102,U_101,U_100,U_99,U_98] :
( admin_indi_has_credit_for_compartment(admin,U_103,U_102)
| ~ admin_indi_has_credit(admin,U_103)
| ~ oca_compartment_is_compartment(U_101,U_102,U_100,U_99,yes,U_98)
| ~ system_indi_is_oca(system,U_101) ),
inference(variable_rename,[status(thm)],[f_33_1]) ).
fof(f_33_3,plain,
! [U_103,U_102,U_101] :
( ! [U_100,U_99,U_98] : ~ oca_compartment_is_compartment(U_101,U_102,U_100,U_99,yes,U_98)
| admin_indi_has_credit_for_compartment(admin,U_103,U_102)
| ~ admin_indi_has_credit(admin,U_103)
| ~ system_indi_is_oca(system,U_101) ),
inference(miniscope,[status(thm)],[f_33_2]) ).
cnf(f_33_4,plain,
( ~ oca_compartment_is_compartment(U_101,U_102,U_100,U_99,yes,U_98)
| admin_indi_has_credit_for_compartment(admin,U_103,U_102)
| ~ admin_indi_has_credit(admin,U_103)
| ~ system_indi_is_oca(system,U_101) ),
inference(clausify,[status(thm)],[f_33_3]) ).
fof(f_34_1,plain,
! [K,C,OCA,L1,L2,B2] :
( admin_indi_has_credit_for_compartment(admin,K,C)
| ~ oca_compartment_is_compartment(OCA,C,L1,L2,no,B2)
| ~ system_indi_is_oca(system,OCA) ),
inference(fof_nnf,[status(thm)],[ax33]) ).
fof(f_34_2,plain,
! [U_109,U_108,U_107,U_106,U_105,U_104] :
( admin_indi_has_credit_for_compartment(admin,U_109,U_108)
| ~ oca_compartment_is_compartment(U_107,U_108,U_106,U_105,no,U_104)
| ~ system_indi_is_oca(system,U_107) ),
inference(variable_rename,[status(thm)],[f_34_1]) ).
fof(f_34_3,plain,
! [U_109,U_108,U_107] :
( ! [U_106,U_105,U_104] : ~ oca_compartment_is_compartment(U_107,U_108,U_106,U_105,no,U_104)
| admin_indi_has_credit_for_compartment(admin,U_109,U_108)
| ~ system_indi_is_oca(system,U_107) ),
inference(miniscope,[status(thm)],[f_34_2]) ).
cnf(f_34_4,plain,
( ~ oca_compartment_is_compartment(U_107,U_108,U_106,U_105,no,U_104)
| admin_indi_has_credit_for_compartment(admin,U_109,U_108)
| ~ system_indi_is_oca(system,U_107) ),
inference(clausify,[status(thm)],[f_34_3]) ).
fof(f_35_1,plain,
! [K,F,CL] :
( admin_indi_has_compartments_for_file(admin,K,F)
| ~ admin_indi_has_compartments(admin,K,CL)
| ~ admin_file_has_compartments(admin,F,CL) ),
inference(fof_nnf,[status(thm)],[ax34]) ).
fof(f_35_2,plain,
! [U_112,U_111,U_110] :
( admin_indi_has_compartments_for_file(admin,U_112,U_111)
| ~ admin_indi_has_compartments(admin,U_112,U_110)
| ~ admin_file_has_compartments(admin,U_111,U_110) ),
inference(variable_rename,[status(thm)],[f_35_1]) ).
cnf(f_35_3,plain,
( admin_indi_has_compartments_for_file(admin,U_112,U_111)
| ~ admin_indi_has_compartments(admin,U_112,U_110)
| ~ admin_file_has_compartments(admin,U_111,U_110) ),
inference(clausify,[status(thm)],[f_35_2]) ).
fof(f_36_1,plain,
! [K,F,L] :
( admin_indi_has_level_for_file(admin,K,F)
| ~ admin_indi_has_level(admin,K,L)
| ~ admin_file_has_level(admin,F,L) ),
inference(fof_nnf,[status(thm)],[ax35]) ).
fof(f_36_2,plain,
! [U_115,U_114,U_113] :
( admin_indi_has_level_for_file(admin,U_115,U_114)
| ~ admin_indi_has_level(admin,U_115,U_113)
| ~ admin_file_has_level(admin,U_114,U_113) ),
inference(variable_rename,[status(thm)],[f_36_1]) ).
cnf(f_36_3,plain,
( admin_indi_has_level_for_file(admin,U_115,U_114)
| ~ admin_indi_has_level(admin,U_115,U_113)
| ~ admin_file_has_level(admin,U_114,U_113) ),
inference(clausify,[status(thm)],[f_36_2]) ).
fof(f_37_1,plain,
! [K,F,OWR] :
( admin_indi_has_need_to_know_for_file(admin,K,F)
| ~ owner_indi_has_need_to_know(OWR,K,F)
| ~ state_file_has_owner(F,OWR) ),
inference(fof_nnf,[status(thm)],[ax36]) ).
fof(f_37_2,plain,
! [U_118,U_117,U_116] :
( admin_indi_has_need_to_know_for_file(admin,U_118,U_117)
| ~ owner_indi_has_need_to_know(U_116,U_118,U_117)
| ~ state_file_has_owner(U_117,U_116) ),
inference(variable_rename,[status(thm)],[f_37_1]) ).
cnf(f_37_3,plain,
( admin_indi_has_need_to_know_for_file(admin,U_118,U_117)
| ~ owner_indi_has_need_to_know(U_116,U_118,U_117)
| ~ state_file_has_owner(U_117,U_116) ),
inference(clausify,[status(thm)],[f_37_2]) ).
fof(f_39_1,plain,
! [K,F] :
( admin_indi_has_citizenship_for_file(admin,K,F)
| ~ admin_indi_has_citizenship(admin,K,usa) ),
inference(fof_nnf,[status(thm)],[ax38]) ).
fof(f_39_2,plain,
! [U_123,U_122] :
( admin_indi_has_citizenship_for_file(admin,U_123,U_122)
| ~ admin_indi_has_citizenship(admin,U_123,usa) ),
inference(variable_rename,[status(thm)],[f_39_1]) ).
fof(f_39_3,plain,
! [U_123] :
( ! [U_122] : admin_indi_has_citizenship_for_file(admin,U_123,U_122)
| ~ admin_indi_has_citizenship(admin,U_123,usa) ),
inference(miniscope,[status(thm)],[f_39_2]) ).
cnf(f_39_4,plain,
( admin_indi_has_citizenship_for_file(admin,U_123,U_122)
| ~ admin_indi_has_citizenship(admin,U_123,usa) ),
inference(clausify,[status(thm)],[f_39_3]) ).
fof(f_40_1,plain,
! [K,F] :
( admin_indi_may_file(admin,K,F,read)
| ~ admin_indi_has_compartments_for_file(admin,K,F)
| ~ admin_indi_has_level_for_file(admin,K,F)
| ~ admin_indi_has_need_to_know_for_file(admin,K,F)
| ~ admin_indi_has_citizenship_for_file(admin,K,F)
| ~ state_file_is_not_working_paper(F) ),
inference(fof_nnf,[status(thm)],[ax39]) ).
fof(f_40_2,plain,
! [U_125,U_124] :
( admin_indi_may_file(admin,U_125,U_124,read)
| ~ admin_indi_has_compartments_for_file(admin,U_125,U_124)
| ~ admin_indi_has_level_for_file(admin,U_125,U_124)
| ~ admin_indi_has_need_to_know_for_file(admin,U_125,U_124)
| ~ admin_indi_has_citizenship_for_file(admin,U_125,U_124)
| ~ state_file_is_not_working_paper(U_124) ),
inference(variable_rename,[status(thm)],[f_40_1]) ).
cnf(f_40_3,plain,
( admin_indi_may_file(admin,U_125,U_124,read)
| ~ admin_indi_has_compartments_for_file(admin,U_125,U_124)
| ~ admin_indi_has_level_for_file(admin,U_125,U_124)
| ~ admin_indi_has_need_to_know_for_file(admin,U_125,U_124)
| ~ admin_indi_has_citizenship_for_file(admin,U_125,U_124)
| ~ state_file_is_not_working_paper(U_124) ),
inference(clausify,[status(thm)],[f_40_2]) ).
fof(f_42_1,plain,
system_indi_is_oca(system,oca),
inference(fof_nnf,[status(thm)],[ax41]) ).
cnf(f_42_2,plain,
system_indi_is_oca(system,oca),
inference(clausify,[status(thm)],[f_42_1]) ).
fof(f_43_1,plain,
oca_compartment_is_compartment(oca,compartmentb,confidential,topsecret,yes,yes),
inference(fof_nnf,[status(thm)],[ax42]) ).
cnf(f_43_2,plain,
oca_compartment_is_compartment(oca,compartmentb,confidential,topsecret,yes,yes),
inference(clausify,[status(thm)],[f_43_1]) ).
fof(f_44_1,plain,
oca_compartment_is_compartment(oca,compartmenta,sbu,unclassified,no,no),
inference(fof_nnf,[status(thm)],[ax43]) ).
cnf(f_44_2,plain,
oca_compartment_is_compartment(oca,compartmenta,sbu,unclassified,no,no),
inference(clausify,[status(thm)],[f_44_1]) ).
fof(f_45_1,plain,
system_compartment_has_sso(system,compartmentb,sso_compartmentb),
inference(fof_nnf,[status(thm)],[ax44]) ).
cnf(f_45_2,plain,
system_compartment_has_sso(system,compartmentb,sso_compartmentb),
inference(clausify,[status(thm)],[f_45_1]) ).
fof(f_46_1,plain,
oca_compartment_has_scg(oca,compartmentb,scg_compartmentb),
inference(fof_nnf,[status(thm)],[ax45]) ).
cnf(f_46_2,plain,
oca_compartment_has_scg(oca,compartmentb,scg_compartmentb),
inference(clausify,[status(thm)],[f_46_1]) ).
fof(f_47_1,plain,
sso_compartment_has_scg(sso_compartmentb,compartmentb,scg_compartmentb),
inference(fof_nnf,[status(thm)],[ax46]) ).
cnf(f_47_2,plain,
sso_compartment_has_scg(sso_compartmentb,compartmentb,scg_compartmentb),
inference(clausify,[status(thm)],[f_47_1]) ).
fof(f_48_1,plain,
system_compartment_has_sso(system,compartmenta,sso_compartmenta),
inference(fof_nnf,[status(thm)],[ax47]) ).
cnf(f_48_2,plain,
system_compartment_has_sso(system,compartmenta,sso_compartmenta),
inference(clausify,[status(thm)],[f_48_1]) ).
fof(f_49_1,plain,
oca_compartment_has_scg(oca,compartmenta,scg_compartmenta),
inference(fof_nnf,[status(thm)],[ax48]) ).
cnf(f_49_2,plain,
oca_compartment_has_scg(oca,compartmenta,scg_compartmenta),
inference(clausify,[status(thm)],[f_49_1]) ).
fof(f_50_1,plain,
sso_compartment_has_scg(sso_compartmenta,compartmenta,scg_compartmenta),
inference(fof_nnf,[status(thm)],[ax49]) ).
cnf(f_50_2,plain,
sso_compartment_has_scg(sso_compartmenta,compartmenta,scg_compartmenta),
inference(clausify,[status(thm)],[f_50_1]) ).
fof(f_51_1,plain,
state_file_is_not_working_paper(secretfile),
inference(fof_nnf,[status(thm)],[ax50]) ).
cnf(f_51_2,plain,
state_file_is_not_working_paper(secretfile),
inference(clausify,[status(thm)],[f_51_1]) ).
fof(f_52_1,plain,
system_file_needs_compartments(system,secretfile,cons(compartmentb,cons(compartmenta,nil))),
inference(fof_nnf,[status(thm)],[ax51]) ).
cnf(f_52_2,plain,
system_file_needs_compartments(system,secretfile,cons(compartmentb,cons(compartmenta,nil))),
inference(clausify,[status(thm)],[f_52_1]) ).
fof(f_53_1,plain,
sso_file_has_compartments(sso_compartmentb,secretfile,cons(compartmentb,cons(compartmenta,nil))),
inference(fof_nnf,[status(thm)],[ax52]) ).
cnf(f_53_2,plain,
sso_file_has_compartments(sso_compartmentb,secretfile,cons(compartmentb,cons(compartmenta,nil))),
inference(clausify,[status(thm)],[f_53_1]) ).
fof(f_54_1,plain,
sso_file_has_compartments(sso_compartmenta,secretfile,cons(compartmentb,cons(compartmenta,nil))),
inference(fof_nnf,[status(thm)],[ax53]) ).
cnf(f_54_2,plain,
sso_file_has_compartments(sso_compartmenta,secretfile,cons(compartmentb,cons(compartmenta,nil))),
inference(clausify,[status(thm)],[f_54_1]) ).
fof(f_55_1,plain,
system_file_needs_level(system,secretfile,secret),
inference(fof_nnf,[status(thm)],[ax54]) ).
cnf(f_55_2,plain,
system_file_needs_level(system,secretfile,secret),
inference(clausify,[status(thm)],[f_55_1]) ).
fof(f_56_1,plain,
sso_file_has_level(sso_compartmentb,secretfile,secret,scg_compartmentb),
inference(fof_nnf,[status(thm)],[ax55]) ).
cnf(f_56_2,plain,
sso_file_has_level(sso_compartmentb,secretfile,secret,scg_compartmentb),
inference(clausify,[status(thm)],[f_56_1]) ).
fof(f_57_1,plain,
sso_file_has_level(sso_compartmenta,secretfile,secret,scg_compartmenta),
inference(fof_nnf,[status(thm)],[ax56]) ).
cnf(f_57_2,plain,
sso_file_has_level(sso_compartmenta,secretfile,secret,scg_compartmenta),
inference(clausify,[status(thm)],[f_57_1]) ).
fof(f_61_1,plain,
state_file_has_owner(secretfile,owner_secretfile),
inference(fof_nnf,[status(thm)],[ax60]) ).
cnf(f_61_2,plain,
state_file_has_owner(secretfile,owner_secretfile),
inference(clausify,[status(thm)],[f_61_1]) ).
fof(f_67_1,plain,
system_indi_is_polygraph_admin(system,polygraph_admin),
inference(fof_nnf,[status(thm)],[ax66]) ).
cnf(f_67_2,plain,
system_indi_is_polygraph_admin(system,polygraph_admin),
inference(clausify,[status(thm)],[f_67_1]) ).
fof(f_68_1,plain,
system_indi_is_credit_admin(system,credit_admin),
inference(fof_nnf,[status(thm)],[ax67]) ).
cnf(f_68_2,plain,
system_indi_is_credit_admin(system,credit_admin),
inference(clausify,[status(thm)],[f_68_1]) ).
fof(f_69_1,plain,
system_indi_is_background_admin(system,background_admin),
inference(fof_nnf,[status(thm)],[ax68]) ).
cnf(f_69_2,plain,
system_indi_is_background_admin(system,background_admin),
inference(clausify,[status(thm)],[f_69_1]) ).
fof(f_70_1,plain,
system_indi_is_hr_admin(system,hr_admin),
inference(fof_nnf,[status(thm)],[ax69]) ).
cnf(f_70_2,plain,
system_indi_is_hr_admin(system,hr_admin),
inference(clausify,[status(thm)],[f_70_1]) ).
fof(f_71_1,plain,
system_indi_is_level_admin(system,level_admin),
inference(fof_nnf,[status(thm)],[ax70]) ).
cnf(f_71_2,plain,
system_indi_is_level_admin(system,level_admin),
inference(clausify,[status(thm)],[f_71_1]) ).
fof(f_72_1,plain,
system_indi_has_citizenship(system,alice,usa),
inference(fof_nnf,[status(thm)],[ax71]) ).
cnf(f_72_2,plain,
system_indi_has_citizenship(system,alice,usa),
inference(clausify,[status(thm)],[f_72_1]) ).
fof(f_73_1,plain,
polygraph_admin_indi_has_polygraph(polygraph_admin,alice),
inference(fof_nnf,[status(thm)],[ax72]) ).
cnf(f_73_2,plain,
polygraph_admin_indi_has_polygraph(polygraph_admin,alice),
inference(clausify,[status(thm)],[f_73_1]) ).
fof(f_74_1,plain,
credit_admin_indi_has_credit(credit_admin,alice),
inference(fof_nnf,[status(thm)],[ax73]) ).
cnf(f_74_2,plain,
credit_admin_indi_has_credit(credit_admin,alice),
inference(clausify,[status(thm)],[f_74_1]) ).
fof(f_75_1,plain,
background_admin_indi_has_background(background_admin,alice,topsecret),
inference(fof_nnf,[status(thm)],[ax74]) ).
cnf(f_75_2,plain,
background_admin_indi_has_background(background_admin,alice,topsecret),
inference(clausify,[status(thm)],[f_75_1]) ).
fof(f_76_1,plain,
hr_admin_indi_has_employment(hr_admin,alice),
inference(fof_nnf,[status(thm)],[ax75]) ).
cnf(f_76_2,plain,
hr_admin_indi_has_employment(hr_admin,alice),
inference(clausify,[status(thm)],[f_76_1]) ).
fof(f_77_1,plain,
system_indi_needs_level(system,alice,secret),
inference(fof_nnf,[status(thm)],[ax76]) ).
cnf(f_77_2,plain,
system_indi_needs_level(system,alice,secret),
inference(clausify,[status(thm)],[f_77_1]) ).
fof(f_78_1,plain,
level_admin_indi_has_level(level_admin,alice,topsecret),
inference(fof_nnf,[status(thm)],[ax77]) ).
cnf(f_78_2,plain,
level_admin_indi_has_level(level_admin,alice,topsecret),
inference(clausify,[status(thm)],[f_78_1]) ).
fof(f_79_1,plain,
system_indi_needs_compartment(system,alice,compartmentb),
inference(fof_nnf,[status(thm)],[ax78]) ).
cnf(f_79_2,plain,
system_indi_needs_compartment(system,alice,compartmentb),
inference(clausify,[status(thm)],[f_79_1]) ).
fof(f_80_1,plain,
system_indi_needs_compartment(system,alice,compartmenta),
inference(fof_nnf,[status(thm)],[ax79]) ).
cnf(f_80_2,plain,
system_indi_needs_compartment(system,alice,compartmenta),
inference(clausify,[status(thm)],[f_80_1]) ).
fof(f_81_1,plain,
sso_indi_has_compartment(sso_compartmentb,alice,compartmentb),
inference(fof_nnf,[status(thm)],[ax80]) ).
cnf(f_81_2,plain,
sso_indi_has_compartment(sso_compartmentb,alice,compartmentb),
inference(clausify,[status(thm)],[f_81_1]) ).
fof(f_82_1,plain,
sso_indi_has_compartment(sso_compartmenta,alice,compartmenta),
inference(fof_nnf,[status(thm)],[ax81]) ).
cnf(f_82_2,plain,
sso_indi_has_compartment(sso_compartmenta,alice,compartmenta),
inference(clausify,[status(thm)],[f_82_1]) ).
fof(f_83_1,plain,
owner_indi_has_need_to_know(owner_secretfile,alice,secretfile),
inference(fof_nnf,[status(thm)],[ax82]) ).
cnf(f_83_2,plain,
owner_indi_has_need_to_know(owner_secretfile,alice,secretfile),
inference(clausify,[status(thm)],[f_83_1]) ).
fof(f_88_1,negated_conjecture,
~ admin_indi_may_file(admin,alice,secretfile,read),
inference(negate,[status(cth)],[alicereadsecret]) ).
fof(f_88_2,negated_conjecture,
~ admin_indi_may_file(admin,alice,secretfile,read),
inference(definitional_conversion,[status(esa)],[f_88_1]) ).
cnf(f_88_3,negated_conjecture,
~ admin_indi_may_file(admin,alice,secretfile,read),
inference(clausify,[status(thm)],[f_88_2]) ).
cnf(t1,plain,
~ admin_indi_may_file(admin,alice,secretfile,read),
inference(start,[status(thm),parent(0:0)],[f_88_3]) ).
cnf(t2,plain,
( ~ 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)
| ~ state_file_is_not_working_paper(secretfile)
| admin_indi_may_file(admin,alice,secretfile,read) ),
inference(extension,[status(thm),parent(t1:1)],[f_40_3]) ).
cnf(t3,plain,
$false,
inference(connection,[status(thm),parent(t2:1)],[t2:1,t1:1]) ).
cnf(t4,plain,
state_file_is_not_working_paper(secretfile),
inference(extension,[status(thm),parent(t2:2)],[f_51_2]) ).
cnf(t5,plain,
$false,
inference(connection,[status(thm),parent(t4:1)],[t4:1,t2:2]) ).
cnf(t6,plain,
( ~ admin_indi_has_compartments(admin,alice,cons(compartmentb,cons(compartmenta,nil)))
| ~ admin_file_has_compartments(admin,secretfile,cons(compartmentb,cons(compartmenta,nil)))
| admin_indi_has_compartments_for_file(admin,alice,secretfile) ),
inference(extension,[status(thm),parent(t2:3)],[f_35_3]) ).
cnf(t7,plain,
$false,
inference(connection,[status(thm),parent(t6:1)],[t6:1,t2:3]) ).
cnf(t8,plain,
( ~ admin_file_has_compartments_h(admin,secretfile,cons(compartmentb,cons(compartmenta,nil)),cons(compartmentb,cons(compartmenta,nil)))
| ~ system_file_needs_compartments(system,secretfile,cons(compartmentb,cons(compartmenta,nil)))
| admin_file_has_compartments(admin,secretfile,cons(compartmentb,cons(compartmenta,nil))) ),
inference(extension,[status(thm),parent(t6:2)],[f_9_3]) ).
cnf(t9,plain,
$false,
inference(connection,[status(thm),parent(t8:1)],[t8:1,t6:2]) ).
cnf(t10,plain,
system_file_needs_compartments(system,secretfile,cons(compartmentb,cons(compartmenta,nil))),
inference(extension,[status(thm),parent(t8:2)],[f_52_2]) ).
cnf(t11,plain,
$false,
inference(connection,[status(thm),parent(t10:1)],[t10:1,t8:2]) ).
cnf(t12,plain,
( ~ 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))
| ~ admin_compartment_has_sso(admin,compartmentb,sso_compartmentb)
| admin_file_has_compartments_h(admin,secretfile,cons(compartmentb,cons(compartmenta,nil)),cons(compartmentb,cons(compartmenta,nil))) ),
inference(extension,[status(thm),parent(t8:3)],[f_11_3]) ).
cnf(t13,plain,
$false,
inference(connection,[status(thm),parent(t12:1)],[t12:1,t8:3]) ).
cnf(t14,plain,
( ~ system_compartment_has_sso(system,compartmentb,sso_compartmentb)
| admin_compartment_has_sso(admin,compartmentb,sso_compartmentb) ),
inference(extension,[status(thm),parent(t12:2)],[f_7_3]) ).
cnf(t15,plain,
$false,
inference(connection,[status(thm),parent(t14:1)],[t14:1,t12:2]) ).
cnf(t16,plain,
system_compartment_has_sso(system,compartmentb,sso_compartmentb),
inference(extension,[status(thm),parent(t14:2)],[f_45_2]) ).
cnf(t17,plain,
$false,
inference(connection,[status(thm),parent(t16:1)],[t16:1,t14:2]) ).
cnf(t18,plain,
( ~ 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)
| ~ admin_compartment_has_sso(admin,compartmenta,sso_compartmenta)
| admin_file_has_compartments_h(admin,secretfile,cons(compartmentb,cons(compartmenta,nil)),cons(compartmenta,nil)) ),
inference(extension,[status(thm),parent(t12:3)],[f_11_3]) ).
cnf(t19,plain,
$false,
inference(connection,[status(thm),parent(t18:1)],[t18:1,t12:3]) ).
cnf(t20,plain,
( ~ system_compartment_has_sso(system,compartmenta,sso_compartmenta)
| admin_compartment_has_sso(admin,compartmenta,sso_compartmenta) ),
inference(extension,[status(thm),parent(t18:2)],[f_7_3]) ).
cnf(t21,plain,
$false,
inference(connection,[status(thm),parent(t20:1)],[t20:1,t18:2]) ).
cnf(t22,plain,
system_compartment_has_sso(system,compartmenta,sso_compartmenta),
inference(extension,[status(thm),parent(t20:2)],[f_48_2]) ).
cnf(t23,plain,
$false,
inference(connection,[status(thm),parent(t22:1)],[t22:1,t20:2]) ).
cnf(t24,plain,
admin_file_has_compartments_h(admin,secretfile,cons(compartmentb,cons(compartmenta,nil)),nil),
inference(extension,[status(thm),parent(t18:3)],[f_10_3]) ).
cnf(t25,plain,
$false,
inference(connection,[status(thm),parent(t24:1)],[t24:1,t18:3]) ).
cnf(t26,plain,
sso_file_has_compartments(sso_compartmenta,secretfile,cons(compartmentb,cons(compartmenta,nil))),
inference(extension,[status(thm),parent(t18:4)],[f_54_2]) ).
cnf(t27,plain,
$false,
inference(connection,[status(thm),parent(t26:1)],[t26:1,t18:4]) ).
cnf(t28,plain,
sso_file_has_compartments(sso_compartmentb,secretfile,cons(compartmentb,cons(compartmenta,nil))),
inference(extension,[status(thm),parent(t12:4)],[f_53_2]) ).
cnf(t29,plain,
$false,
inference(connection,[status(thm),parent(t28:1)],[t28:1,t12:4]) ).
cnf(t30,plain,
( ~ 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))
| ~ system_indi_needs_compartment(system,alice,compartmentb)
| admin_indi_has_compartments(admin,alice,cons(compartmentb,cons(compartmenta,nil))) ),
inference(extension,[status(thm),parent(t6:3)],[f_28_4]) ).
cnf(t31,plain,
$false,
inference(connection,[status(thm),parent(t30:1)],[t30:1,t6:3]) ).
cnf(t32,plain,
system_indi_needs_compartment(system,alice,compartmentb),
inference(extension,[status(thm),parent(t30:2)],[f_79_2]) ).
cnf(t33,plain,
$false,
inference(connection,[status(thm),parent(t32:1)],[t32:1,t30:2]) ).
cnf(t34,plain,
( ~ 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)
| ~ system_indi_needs_compartment(system,alice,compartmenta)
| admin_indi_has_compartments(admin,alice,cons(compartmenta,nil)) ),
inference(extension,[status(thm),parent(t30:3)],[f_28_4]) ).
cnf(t35,plain,
$false,
inference(connection,[status(thm),parent(t34:1)],[t34:1,t30:3]) ).
cnf(t36,plain,
system_indi_needs_compartment(system,alice,compartmenta),
inference(extension,[status(thm),parent(t34:2)],[f_80_2]) ).
cnf(t37,plain,
$false,
inference(connection,[status(thm),parent(t36:1)],[t36:1,t34:2]) ).
cnf(t38,plain,
admin_indi_has_compartments(admin,alice,nil),
inference(extension,[status(thm),parent(t34:3)],[f_27_3]) ).
cnf(t39,plain,
$false,
inference(connection,[status(thm),parent(t38:1)],[t38:1,t34:3]) ).
cnf(t40,plain,
( ~ admin_indi_has_level(admin,alice,sbu)
| ~ oca_compartment_is_compartment(oca,compartmenta,sbu,unclassified,no,no)
| ~ system_indi_is_oca(system,oca)
| admin_indi_has_level_for_compartment(admin,alice,compartmenta) ),
inference(extension,[status(thm),parent(t34:4)],[f_30_4]) ).
cnf(t41,plain,
$false,
inference(connection,[status(thm),parent(t40:1)],[t40:1,t34:4]) ).
cnf(t42,plain,
system_indi_is_oca(system,oca),
inference(extension,[status(thm),parent(t40:2)],[f_42_2]) ).
cnf(t43,plain,
$false,
inference(connection,[status(thm),parent(t42:1)],[t42:1,t40:2]) ).
cnf(t44,plain,
oca_compartment_is_compartment(oca,compartmenta,sbu,unclassified,no,no),
inference(extension,[status(thm),parent(t40:3)],[f_44_2]) ).
cnf(t45,plain,
$false,
inference(connection,[status(thm),parent(t44:1)],[t44:1,t40:3]) ).
cnf(t46,plain,
( ~ 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)
| ~ system_indi_needs_level(system,alice,secret)
| admin_indi_has_level(admin,alice,sbu) ),
inference(extension,[status(thm),parent(t40:4)],[f_26_4]) ).
cnf(t47,plain,
$false,
inference(connection,[status(thm),parent(t46:1)],[t46:1,t40:4]) ).
cnf(t48,plain,
system_indi_needs_level(system,alice,secret),
inference(extension,[status(thm),parent(t46:2)],[f_77_2]) ).
cnf(t49,plain,
$false,
inference(connection,[status(thm),parent(t48:1)],[t48:1,t46:2]) ).
cnf(t50,plain,
( ~ background_admin_indi_has_background(background_admin,alice,topsecret)
| ~ loca_level_below(admin,sbu,topsecret)
| ~ system_indi_is_background_admin(system,background_admin)
| admin_indi_has_background(admin,alice,sbu) ),
inference(extension,[status(thm),parent(t46:3)],[f_21_4]) ).
cnf(t51,plain,
$false,
inference(connection,[status(thm),parent(t50:1)],[t50:1,t46:3]) ).
cnf(t52,plain,
system_indi_is_background_admin(system,background_admin),
inference(extension,[status(thm),parent(t50:2)],[f_69_2]) ).
cnf(t53,plain,
$false,
inference(connection,[status(thm),parent(t52:1)],[t52:1,t50:2]) ).
cnf(t54,plain,
( ~ loca_level_below(admin,sbu,secret)
| ~ loca_level_direct_below(admin,secret,topsecret)
| loca_level_below(admin,sbu,topsecret) ),
inference(extension,[status(thm),parent(t50:3)],[f_6_3]) ).
cnf(t55,plain,
$false,
inference(connection,[status(thm),parent(t54:1)],[t54:1,t50:3]) ).
cnf(t56,plain,
loca_level_direct_below(admin,secret,topsecret),
inference(extension,[status(thm),parent(t54:2)],[f_4_3]) ).
cnf(t57,plain,
$false,
inference(connection,[status(thm),parent(t56:1)],[t56:1,t54:2]) ).
cnf(t58,plain,
( ~ loca_level_below(admin,sbu,confidential)
| ~ loca_level_direct_below(admin,confidential,secret)
| loca_level_below(admin,sbu,secret) ),
inference(extension,[status(thm),parent(t54:3)],[f_6_3]) ).
cnf(t59,plain,
$false,
inference(connection,[status(thm),parent(t58:1)],[t58:1,t54:3]) ).
cnf(t60,plain,
loca_level_direct_below(admin,confidential,secret),
inference(extension,[status(thm),parent(t58:2)],[f_3_3]) ).
cnf(t61,plain,
$false,
inference(connection,[status(thm),parent(t60:1)],[t60:1,t58:2]) ).
cnf(t62,plain,
( ~ loca_level_below(admin,sbu,sbu)
| ~ loca_level_direct_below(admin,sbu,confidential)
| loca_level_below(admin,sbu,confidential) ),
inference(extension,[status(thm),parent(t58:3)],[f_6_3]) ).
cnf(t63,plain,
$false,
inference(connection,[status(thm),parent(t62:1)],[t62:1,t58:3]) ).
cnf(t64,plain,
loca_level_direct_below(admin,sbu,confidential),
inference(extension,[status(thm),parent(t62:2)],[f_2_3]) ).
cnf(t65,plain,
$false,
inference(connection,[status(thm),parent(t64:1)],[t64:1,t62:2]) ).
cnf(t66,plain,
loca_level_below(admin,sbu,sbu),
inference(extension,[status(thm),parent(t62:3)],[f_5_3]) ).
cnf(t67,plain,
$false,
inference(connection,[status(thm),parent(t66:1)],[t66:1,t62:3]) ).
cnf(t68,plain,
background_admin_indi_has_background(background_admin,alice,topsecret),
inference(extension,[status(thm),parent(t50:4)],[f_75_2]) ).
cnf(t69,plain,
$false,
inference(connection,[status(thm),parent(t68:1)],[t68:1,t50:4]) ).
cnf(t70,plain,
( ~ loca_level_below(admin,sbu,secret)
| ~ loca_level_direct_below(admin,secret,topsecret)
| loca_level_below(admin,sbu,topsecret) ),
inference(extension,[status(thm),parent(t46:4)],[f_6_3]) ).
cnf(t71,plain,
$false,
inference(connection,[status(thm),parent(t70:1)],[t70:1,t46:4]) ).
cnf(t72,plain,
loca_level_direct_below(admin,secret,topsecret),
inference(extension,[status(thm),parent(t70:2)],[f_4_3]) ).
cnf(t73,plain,
$false,
inference(connection,[status(thm),parent(t72:1)],[t72:1,t70:2]) ).
cnf(t74,plain,
( ~ loca_level_below(admin,sbu,confidential)
| ~ loca_level_direct_below(admin,confidential,secret)
| loca_level_below(admin,sbu,secret) ),
inference(extension,[status(thm),parent(t70:3)],[f_6_3]) ).
cnf(t75,plain,
$false,
inference(connection,[status(thm),parent(t74:1)],[t74:1,t70:3]) ).
cnf(t76,plain,
loca_level_direct_below(admin,confidential,secret),
inference(extension,[status(thm),parent(t74:2)],[f_3_3]) ).
cnf(t77,plain,
$false,
inference(connection,[status(thm),parent(t76:1)],[t76:1,t74:2]) ).
cnf(t78,plain,
( ~ loca_level_below(admin,sbu,sbu)
| ~ loca_level_direct_below(admin,sbu,confidential)
| loca_level_below(admin,sbu,confidential) ),
inference(extension,[status(thm),parent(t74:3)],[f_6_3]) ).
cnf(t79,plain,
$false,
inference(connection,[status(thm),parent(t78:1)],[t78:1,t74:3]) ).
cnf(t80,plain,
loca_level_direct_below(admin,sbu,confidential),
inference(extension,[status(thm),parent(t78:2)],[f_2_3]) ).
cnf(t81,plain,
$false,
inference(connection,[status(thm),parent(t80:1)],[t80:1,t78:2]) ).
cnf(t82,plain,
loca_level_below(admin,sbu,sbu),
inference(extension,[status(thm),parent(t78:3)],[f_5_3]) ).
cnf(t83,plain,
$false,
inference(connection,[status(thm),parent(t82:1)],[t82:1,t78:3]) ).
cnf(t84,plain,
level_admin_indi_has_level(level_admin,alice,topsecret),
inference(extension,[status(thm),parent(t46:5)],[f_78_2]) ).
cnf(t85,plain,
$false,
inference(connection,[status(thm),parent(t84:1)],[t84:1,t46:5]) ).
cnf(t86,plain,
system_indi_is_level_admin(system,level_admin),
inference(extension,[status(thm),parent(t46:6)],[f_71_2]) ).
cnf(t87,plain,
$false,
inference(connection,[status(thm),parent(t86:1)],[t86:1,t46:6]) ).
cnf(t88,plain,
( ~ loca_level_below(admin,sbu,confidential)
| ~ loca_level_direct_below(admin,confidential,secret)
| loca_level_below(admin,sbu,secret) ),
inference(extension,[status(thm),parent(t46:7)],[f_6_3]) ).
cnf(t89,plain,
$false,
inference(connection,[status(thm),parent(t88:1)],[t88:1,t46:7]) ).
cnf(t90,plain,
loca_level_direct_below(admin,confidential,secret),
inference(extension,[status(thm),parent(t88:2)],[f_3_3]) ).
cnf(t91,plain,
$false,
inference(connection,[status(thm),parent(t90:1)],[t90:1,t88:2]) ).
cnf(t92,plain,
( ~ loca_level_below(admin,sbu,sbu)
| ~ loca_level_direct_below(admin,sbu,confidential)
| loca_level_below(admin,sbu,confidential) ),
inference(extension,[status(thm),parent(t88:3)],[f_6_3]) ).
cnf(t93,plain,
$false,
inference(connection,[status(thm),parent(t92:1)],[t92:1,t88:3]) ).
cnf(t94,plain,
loca_level_direct_below(admin,sbu,confidential),
inference(extension,[status(thm),parent(t92:2)],[f_2_3]) ).
cnf(t95,plain,
$false,
inference(connection,[status(thm),parent(t94:1)],[t94:1,t92:2]) ).
cnf(t96,plain,
loca_level_below(admin,sbu,sbu),
inference(extension,[status(thm),parent(t92:3)],[f_5_3]) ).
cnf(t97,plain,
$false,
inference(connection,[status(thm),parent(t96:1)],[t96:1,t92:3]) ).
cnf(t98,plain,
( ~ credit_admin_indi_has_credit(credit_admin,alice)
| ~ system_indi_is_credit_admin(system,credit_admin)
| admin_indi_has_credit(admin,alice) ),
inference(extension,[status(thm),parent(t46:8)],[f_19_3]) ).
cnf(t99,plain,
$false,
inference(connection,[status(thm),parent(t98:1)],[t98:1,t46:8]) ).
cnf(t100,plain,
system_indi_is_credit_admin(system,credit_admin),
inference(extension,[status(thm),parent(t98:2)],[f_68_2]) ).
cnf(t101,plain,
$false,
inference(connection,[status(thm),parent(t100:1)],[t100:1,t98:2]) ).
cnf(t102,plain,
credit_admin_indi_has_credit(credit_admin,alice),
inference(extension,[status(thm),parent(t98:3)],[f_74_2]) ).
cnf(t103,plain,
$false,
inference(connection,[status(thm),parent(t102:1)],[t102:1,t98:3]) ).
cnf(t104,plain,
( ~ hr_admin_indi_has_employment(hr_admin,alice)
| ~ system_indi_is_hr_admin(system,hr_admin)
| admin_indi_has_employment(admin,alice) ),
inference(extension,[status(thm),parent(t46:9)],[f_22_3]) ).
cnf(t105,plain,
$false,
inference(connection,[status(thm),parent(t104:1)],[t104:1,t46:9]) ).
cnf(t106,plain,
system_indi_is_hr_admin(system,hr_admin),
inference(extension,[status(thm),parent(t104:2)],[f_70_2]) ).
cnf(t107,plain,
$false,
inference(connection,[status(thm),parent(t106:1)],[t106:1,t104:2]) ).
cnf(t108,plain,
hr_admin_indi_has_employment(hr_admin,alice),
inference(extension,[status(thm),parent(t104:3)],[f_76_2]) ).
cnf(t109,plain,
$false,
inference(connection,[status(thm),parent(t108:1)],[t108:1,t104:3]) ).
cnf(t110,plain,
( ~ polygraph_admin_indi_has_polygraph(polygraph_admin,alice)
| ~ system_indi_is_polygraph_admin(system,polygraph_admin)
| admin_indi_has_polygraph(admin,alice) ),
inference(extension,[status(thm),parent(t46:10)],[f_18_3]) ).
cnf(t111,plain,
$false,
inference(connection,[status(thm),parent(t110:1)],[t110:1,t46:10]) ).
cnf(t112,plain,
system_indi_is_polygraph_admin(system,polygraph_admin),
inference(extension,[status(thm),parent(t110:2)],[f_67_2]) ).
cnf(t113,plain,
$false,
inference(connection,[status(thm),parent(t112:1)],[t112:1,t110:2]) ).
cnf(t114,plain,
polygraph_admin_indi_has_polygraph(polygraph_admin,alice),
inference(extension,[status(thm),parent(t110:3)],[f_73_2]) ).
cnf(t115,plain,
$false,
inference(connection,[status(thm),parent(t114:1)],[t114:1,t110:3]) ).
cnf(t116,plain,
( ~ system_indi_has_citizenship(system,alice,usa)
| admin_indi_has_citizenship(admin,alice,usa) ),
inference(extension,[status(thm),parent(t46:11)],[f_24_3]) ).
cnf(t117,plain,
$false,
inference(connection,[status(thm),parent(t116:1)],[t116:1,t46:11]) ).
cnf(t118,plain,
system_indi_has_citizenship(system,alice,usa),
inference(extension,[status(thm),parent(t116:2)],[f_72_2]) ).
cnf(t119,plain,
$false,
inference(connection,[status(thm),parent(t118:1)],[t118:1,t116:2]) ).
cnf(t120,plain,
( ~ admin_indi_has_background(admin,alice,unclassified)
| ~ oca_compartment_is_compartment(oca,compartmenta,sbu,unclassified,no,no)
| ~ system_indi_is_oca(system,oca)
| admin_indi_has_background_for_compartment(admin,alice,compartmenta) ),
inference(extension,[status(thm),parent(t34:5)],[f_29_4]) ).
cnf(t121,plain,
$false,
inference(connection,[status(thm),parent(t120:1)],[t120:1,t34:5]) ).
cnf(t122,plain,
system_indi_is_oca(system,oca),
inference(extension,[status(thm),parent(t120:2)],[f_42_2]) ).
cnf(t123,plain,
$false,
inference(connection,[status(thm),parent(t122:1)],[t122:1,t120:2]) ).
cnf(t124,plain,
oca_compartment_is_compartment(oca,compartmenta,sbu,unclassified,no,no),
inference(extension,[status(thm),parent(t120:3)],[f_44_2]) ).
cnf(t125,plain,
$false,
inference(connection,[status(thm),parent(t124:1)],[t124:1,t120:3]) ).
cnf(t126,plain,
( ~ background_admin_indi_has_background(background_admin,alice,topsecret)
| ~ loca_level_below(admin,unclassified,topsecret)
| ~ system_indi_is_background_admin(system,background_admin)
| admin_indi_has_background(admin,alice,unclassified) ),
inference(extension,[status(thm),parent(t120:4)],[f_21_4]) ).
cnf(t127,plain,
$false,
inference(connection,[status(thm),parent(t126:1)],[t126:1,t120:4]) ).
cnf(t128,plain,
system_indi_is_background_admin(system,background_admin),
inference(extension,[status(thm),parent(t126:2)],[f_69_2]) ).
cnf(t129,plain,
$false,
inference(connection,[status(thm),parent(t128:1)],[t128:1,t126:2]) ).
cnf(t130,plain,
( ~ loca_level_below(admin,unclassified,secret)
| ~ loca_level_direct_below(admin,secret,topsecret)
| loca_level_below(admin,unclassified,topsecret) ),
inference(extension,[status(thm),parent(t126:3)],[f_6_3]) ).
cnf(t131,plain,
$false,
inference(connection,[status(thm),parent(t130:1)],[t130:1,t126:3]) ).
cnf(t132,plain,
loca_level_direct_below(admin,secret,topsecret),
inference(extension,[status(thm),parent(t130:2)],[f_4_3]) ).
cnf(t133,plain,
$false,
inference(connection,[status(thm),parent(t132:1)],[t132:1,t130:2]) ).
cnf(t134,plain,
( ~ loca_level_below(admin,unclassified,confidential)
| ~ loca_level_direct_below(admin,confidential,secret)
| loca_level_below(admin,unclassified,secret) ),
inference(extension,[status(thm),parent(t130:3)],[f_6_3]) ).
cnf(t135,plain,
$false,
inference(connection,[status(thm),parent(t134:1)],[t134:1,t130:3]) ).
cnf(t136,plain,
loca_level_direct_below(admin,confidential,secret),
inference(extension,[status(thm),parent(t134:2)],[f_3_3]) ).
cnf(t137,plain,
$false,
inference(connection,[status(thm),parent(t136:1)],[t136:1,t134:2]) ).
cnf(t138,plain,
( ~ loca_level_below(admin,unclassified,sbu)
| ~ loca_level_direct_below(admin,sbu,confidential)
| loca_level_below(admin,unclassified,confidential) ),
inference(extension,[status(thm),parent(t134:3)],[f_6_3]) ).
cnf(t139,plain,
$false,
inference(connection,[status(thm),parent(t138:1)],[t138:1,t134:3]) ).
cnf(t140,plain,
loca_level_direct_below(admin,sbu,confidential),
inference(extension,[status(thm),parent(t138:2)],[f_2_3]) ).
cnf(t141,plain,
$false,
inference(connection,[status(thm),parent(t140:1)],[t140:1,t138:2]) ).
cnf(t142,plain,
( ~ loca_level_below(admin,unclassified,unclassified)
| ~ loca_level_direct_below(admin,unclassified,sbu)
| loca_level_below(admin,unclassified,sbu) ),
inference(extension,[status(thm),parent(t138:3)],[f_6_3]) ).
cnf(t143,plain,
$false,
inference(connection,[status(thm),parent(t142:1)],[t142:1,t138:3]) ).
cnf(t144,plain,
loca_level_direct_below(admin,unclassified,sbu),
inference(extension,[status(thm),parent(t142:2)],[f_1_3]) ).
cnf(t145,plain,
$false,
inference(connection,[status(thm),parent(t144:1)],[t144:1,t142:2]) ).
cnf(t146,plain,
loca_level_below(admin,unclassified,unclassified),
inference(extension,[status(thm),parent(t142:3)],[f_5_3]) ).
cnf(t147,plain,
$false,
inference(connection,[status(thm),parent(t146:1)],[t146:1,t142:3]) ).
cnf(t148,plain,
background_admin_indi_has_background(background_admin,alice,topsecret),
inference(extension,[status(thm),parent(t126:4)],[f_75_2]) ).
cnf(t149,plain,
$false,
inference(connection,[status(thm),parent(t148:1)],[t148:1,t126:4]) ).
cnf(t150,plain,
sso_indi_has_compartment(sso_compartmenta,alice,compartmenta),
inference(extension,[status(thm),parent(t34:6)],[f_82_2]) ).
cnf(t151,plain,
$false,
inference(connection,[status(thm),parent(t150:1)],[t150:1,t34:6]) ).
cnf(t152,plain,
( ~ system_compartment_has_sso(system,compartmenta,sso_compartmenta)
| admin_compartment_has_sso(admin,compartmenta,sso_compartmenta) ),
inference(extension,[status(thm),parent(t34:7)],[f_7_3]) ).
cnf(t153,plain,
$false,
inference(connection,[status(thm),parent(t152:1)],[t152:1,t34:7]) ).
cnf(t154,plain,
system_compartment_has_sso(system,compartmenta,sso_compartmenta),
inference(extension,[status(thm),parent(t152:2)],[f_48_2]) ).
cnf(t155,plain,
$false,
inference(connection,[status(thm),parent(t154:1)],[t154:1,t152:2]) ).
cnf(t156,plain,
( ~ oca_compartment_is_compartment(oca,compartmenta,sbu,unclassified,no,no)
| ~ system_indi_is_oca(system,oca)
| admin_indi_has_credit_for_compartment(admin,alice,compartmenta) ),
inference(extension,[status(thm),parent(t34:8)],[f_34_4]) ).
cnf(t157,plain,
$false,
inference(connection,[status(thm),parent(t156:1)],[t156:1,t34:8]) ).
cnf(t158,plain,
system_indi_is_oca(system,oca),
inference(extension,[status(thm),parent(t156:2)],[f_42_2]) ).
cnf(t159,plain,
$false,
inference(connection,[status(thm),parent(t158:1)],[t158:1,t156:2]) ).
cnf(t160,plain,
oca_compartment_is_compartment(oca,compartmenta,sbu,unclassified,no,no),
inference(extension,[status(thm),parent(t156:3)],[f_44_2]) ).
cnf(t161,plain,
$false,
inference(connection,[status(thm),parent(t160:1)],[t160:1,t156:3]) ).
cnf(t162,plain,
( ~ oca_compartment_is_compartment(oca,compartmenta,sbu,unclassified,no,no)
| ~ system_indi_is_oca(system,oca)
| admin_indi_has_polygraph_for_compartment(admin,alice,compartmenta) ),
inference(extension,[status(thm),parent(t34:9)],[f_32_4]) ).
cnf(t163,plain,
$false,
inference(connection,[status(thm),parent(t162:1)],[t162:1,t34:9]) ).
cnf(t164,plain,
system_indi_is_oca(system,oca),
inference(extension,[status(thm),parent(t162:2)],[f_42_2]) ).
cnf(t165,plain,
$false,
inference(connection,[status(thm),parent(t164:1)],[t164:1,t162:2]) ).
cnf(t166,plain,
oca_compartment_is_compartment(oca,compartmenta,sbu,unclassified,no,no),
inference(extension,[status(thm),parent(t162:3)],[f_44_2]) ).
cnf(t167,plain,
$false,
inference(connection,[status(thm),parent(t166:1)],[t166:1,t162:3]) ).
cnf(t168,plain,
( ~ system_indi_has_citizenship(system,alice,usa)
| admin_indi_has_citizenship(admin,alice,usa) ),
inference(extension,[status(thm),parent(t34:10)],[f_24_3]) ).
cnf(t169,plain,
$false,
inference(connection,[status(thm),parent(t168:1)],[t168:1,t34:10]) ).
cnf(t170,plain,
system_indi_has_citizenship(system,alice,usa),
inference(extension,[status(thm),parent(t168:2)],[f_72_2]) ).
cnf(t171,plain,
$false,
inference(connection,[status(thm),parent(t170:1)],[t170:1,t168:2]) ).
cnf(t172,plain,
( ~ hr_admin_indi_has_employment(hr_admin,alice)
| ~ system_indi_is_hr_admin(system,hr_admin)
| admin_indi_has_employment(admin,alice) ),
inference(extension,[status(thm),parent(t34:11)],[f_22_3]) ).
cnf(t173,plain,
$false,
inference(connection,[status(thm),parent(t172:1)],[t172:1,t34:11]) ).
cnf(t174,plain,
system_indi_is_hr_admin(system,hr_admin),
inference(extension,[status(thm),parent(t172:2)],[f_70_2]) ).
cnf(t175,plain,
$false,
inference(connection,[status(thm),parent(t174:1)],[t174:1,t172:2]) ).
cnf(t176,plain,
hr_admin_indi_has_employment(hr_admin,alice),
inference(extension,[status(thm),parent(t172:3)],[f_76_2]) ).
cnf(t177,plain,
$false,
inference(connection,[status(thm),parent(t176:1)],[t176:1,t172:3]) ).
cnf(t178,plain,
( ~ admin_indi_has_level(admin,alice,confidential)
| ~ oca_compartment_is_compartment(oca,compartmentb,confidential,topsecret,yes,yes)
| ~ system_indi_is_oca(system,oca)
| admin_indi_has_level_for_compartment(admin,alice,compartmentb) ),
inference(extension,[status(thm),parent(t30:4)],[f_30_4]) ).
cnf(t179,plain,
$false,
inference(connection,[status(thm),parent(t178:1)],[t178:1,t30:4]) ).
cnf(t180,plain,
system_indi_is_oca(system,oca),
inference(extension,[status(thm),parent(t178:2)],[f_42_2]) ).
cnf(t181,plain,
$false,
inference(connection,[status(thm),parent(t180:1)],[t180:1,t178:2]) ).
cnf(t182,plain,
oca_compartment_is_compartment(oca,compartmentb,confidential,topsecret,yes,yes),
inference(extension,[status(thm),parent(t178:3)],[f_43_2]) ).
cnf(t183,plain,
$false,
inference(connection,[status(thm),parent(t182:1)],[t182:1,t178:3]) ).
cnf(t184,plain,
( ~ 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)
| ~ system_indi_needs_level(system,alice,secret)
| admin_indi_has_level(admin,alice,confidential) ),
inference(extension,[status(thm),parent(t178:4)],[f_26_4]) ).
cnf(t185,plain,
$false,
inference(connection,[status(thm),parent(t184:1)],[t184:1,t178:4]) ).
cnf(t186,plain,
system_indi_needs_level(system,alice,secret),
inference(extension,[status(thm),parent(t184:2)],[f_77_2]) ).
cnf(t187,plain,
$false,
inference(connection,[status(thm),parent(t186:1)],[t186:1,t184:2]) ).
cnf(t188,plain,
( ~ background_admin_indi_has_background(background_admin,alice,topsecret)
| ~ loca_level_below(admin,confidential,topsecret)
| ~ system_indi_is_background_admin(system,background_admin)
| admin_indi_has_background(admin,alice,confidential) ),
inference(extension,[status(thm),parent(t184:3)],[f_21_4]) ).
cnf(t189,plain,
$false,
inference(connection,[status(thm),parent(t188:1)],[t188:1,t184:3]) ).
cnf(t190,plain,
system_indi_is_background_admin(system,background_admin),
inference(extension,[status(thm),parent(t188:2)],[f_69_2]) ).
cnf(t191,plain,
$false,
inference(connection,[status(thm),parent(t190:1)],[t190:1,t188:2]) ).
cnf(t192,plain,
( ~ loca_level_below(admin,confidential,secret)
| ~ loca_level_direct_below(admin,secret,topsecret)
| loca_level_below(admin,confidential,topsecret) ),
inference(extension,[status(thm),parent(t188:3)],[f_6_3]) ).
cnf(t193,plain,
$false,
inference(connection,[status(thm),parent(t192:1)],[t192:1,t188:3]) ).
cnf(t194,plain,
loca_level_direct_below(admin,secret,topsecret),
inference(extension,[status(thm),parent(t192:2)],[f_4_3]) ).
cnf(t195,plain,
$false,
inference(connection,[status(thm),parent(t194:1)],[t194:1,t192:2]) ).
cnf(t196,plain,
( ~ loca_level_below(admin,confidential,confidential)
| ~ loca_level_direct_below(admin,confidential,secret)
| loca_level_below(admin,confidential,secret) ),
inference(extension,[status(thm),parent(t192:3)],[f_6_3]) ).
cnf(t197,plain,
$false,
inference(connection,[status(thm),parent(t196:1)],[t196:1,t192:3]) ).
cnf(t198,plain,
loca_level_direct_below(admin,confidential,secret),
inference(extension,[status(thm),parent(t196:2)],[f_3_3]) ).
cnf(t199,plain,
$false,
inference(connection,[status(thm),parent(t198:1)],[t198:1,t196:2]) ).
cnf(t200,plain,
loca_level_below(admin,confidential,confidential),
inference(extension,[status(thm),parent(t196:3)],[f_5_3]) ).
cnf(t201,plain,
$false,
inference(connection,[status(thm),parent(t200:1)],[t200:1,t196:3]) ).
cnf(t202,plain,
background_admin_indi_has_background(background_admin,alice,topsecret),
inference(extension,[status(thm),parent(t188:4)],[f_75_2]) ).
cnf(t203,plain,
$false,
inference(connection,[status(thm),parent(t202:1)],[t202:1,t188:4]) ).
cnf(t204,plain,
( ~ loca_level_below(admin,confidential,secret)
| ~ loca_level_direct_below(admin,secret,topsecret)
| loca_level_below(admin,confidential,topsecret) ),
inference(extension,[status(thm),parent(t184:4)],[f_6_3]) ).
cnf(t205,plain,
$false,
inference(connection,[status(thm),parent(t204:1)],[t204:1,t184:4]) ).
cnf(t206,plain,
loca_level_direct_below(admin,secret,topsecret),
inference(extension,[status(thm),parent(t204:2)],[f_4_3]) ).
cnf(t207,plain,
$false,
inference(connection,[status(thm),parent(t206:1)],[t206:1,t204:2]) ).
cnf(t208,plain,
( ~ loca_level_below(admin,confidential,confidential)
| ~ loca_level_direct_below(admin,confidential,secret)
| loca_level_below(admin,confidential,secret) ),
inference(extension,[status(thm),parent(t204:3)],[f_6_3]) ).
cnf(t209,plain,
$false,
inference(connection,[status(thm),parent(t208:1)],[t208:1,t204:3]) ).
cnf(t210,plain,
loca_level_direct_below(admin,confidential,secret),
inference(extension,[status(thm),parent(t208:2)],[f_3_3]) ).
cnf(t211,plain,
$false,
inference(connection,[status(thm),parent(t210:1)],[t210:1,t208:2]) ).
cnf(t212,plain,
loca_level_below(admin,confidential,confidential),
inference(extension,[status(thm),parent(t208:3)],[f_5_3]) ).
cnf(t213,plain,
$false,
inference(connection,[status(thm),parent(t212:1)],[t212:1,t208:3]) ).
cnf(t214,plain,
level_admin_indi_has_level(level_admin,alice,topsecret),
inference(extension,[status(thm),parent(t184:5)],[f_78_2]) ).
cnf(t215,plain,
$false,
inference(connection,[status(thm),parent(t214:1)],[t214:1,t184:5]) ).
cnf(t216,plain,
system_indi_is_level_admin(system,level_admin),
inference(extension,[status(thm),parent(t184:6)],[f_71_2]) ).
cnf(t217,plain,
$false,
inference(connection,[status(thm),parent(t216:1)],[t216:1,t184:6]) ).
cnf(t218,plain,
( ~ loca_level_below(admin,confidential,confidential)
| ~ loca_level_direct_below(admin,confidential,secret)
| loca_level_below(admin,confidential,secret) ),
inference(extension,[status(thm),parent(t184:7)],[f_6_3]) ).
cnf(t219,plain,
$false,
inference(connection,[status(thm),parent(t218:1)],[t218:1,t184:7]) ).
cnf(t220,plain,
loca_level_direct_below(admin,confidential,secret),
inference(extension,[status(thm),parent(t218:2)],[f_3_3]) ).
cnf(t221,plain,
$false,
inference(connection,[status(thm),parent(t220:1)],[t220:1,t218:2]) ).
cnf(t222,plain,
loca_level_below(admin,confidential,confidential),
inference(extension,[status(thm),parent(t218:3)],[f_5_3]) ).
cnf(t223,plain,
$false,
inference(connection,[status(thm),parent(t222:1)],[t222:1,t218:3]) ).
cnf(t224,plain,
( ~ credit_admin_indi_has_credit(credit_admin,alice)
| ~ system_indi_is_credit_admin(system,credit_admin)
| admin_indi_has_credit(admin,alice) ),
inference(extension,[status(thm),parent(t184:8)],[f_19_3]) ).
cnf(t225,plain,
$false,
inference(connection,[status(thm),parent(t224:1)],[t224:1,t184:8]) ).
cnf(t226,plain,
system_indi_is_credit_admin(system,credit_admin),
inference(extension,[status(thm),parent(t224:2)],[f_68_2]) ).
cnf(t227,plain,
$false,
inference(connection,[status(thm),parent(t226:1)],[t226:1,t224:2]) ).
cnf(t228,plain,
credit_admin_indi_has_credit(credit_admin,alice),
inference(extension,[status(thm),parent(t224:3)],[f_74_2]) ).
cnf(t229,plain,
$false,
inference(connection,[status(thm),parent(t228:1)],[t228:1,t224:3]) ).
cnf(t230,plain,
( ~ hr_admin_indi_has_employment(hr_admin,alice)
| ~ system_indi_is_hr_admin(system,hr_admin)
| admin_indi_has_employment(admin,alice) ),
inference(extension,[status(thm),parent(t184:9)],[f_22_3]) ).
cnf(t231,plain,
$false,
inference(connection,[status(thm),parent(t230:1)],[t230:1,t184:9]) ).
cnf(t232,plain,
system_indi_is_hr_admin(system,hr_admin),
inference(extension,[status(thm),parent(t230:2)],[f_70_2]) ).
cnf(t233,plain,
$false,
inference(connection,[status(thm),parent(t232:1)],[t232:1,t230:2]) ).
cnf(t234,plain,
hr_admin_indi_has_employment(hr_admin,alice),
inference(extension,[status(thm),parent(t230:3)],[f_76_2]) ).
cnf(t235,plain,
$false,
inference(connection,[status(thm),parent(t234:1)],[t234:1,t230:3]) ).
cnf(t236,plain,
( ~ polygraph_admin_indi_has_polygraph(polygraph_admin,alice)
| ~ system_indi_is_polygraph_admin(system,polygraph_admin)
| admin_indi_has_polygraph(admin,alice) ),
inference(extension,[status(thm),parent(t184:10)],[f_18_3]) ).
cnf(t237,plain,
$false,
inference(connection,[status(thm),parent(t236:1)],[t236:1,t184:10]) ).
cnf(t238,plain,
system_indi_is_polygraph_admin(system,polygraph_admin),
inference(extension,[status(thm),parent(t236:2)],[f_67_2]) ).
cnf(t239,plain,
$false,
inference(connection,[status(thm),parent(t238:1)],[t238:1,t236:2]) ).
cnf(t240,plain,
polygraph_admin_indi_has_polygraph(polygraph_admin,alice),
inference(extension,[status(thm),parent(t236:3)],[f_73_2]) ).
cnf(t241,plain,
$false,
inference(connection,[status(thm),parent(t240:1)],[t240:1,t236:3]) ).
cnf(t242,plain,
( ~ system_indi_has_citizenship(system,alice,usa)
| admin_indi_has_citizenship(admin,alice,usa) ),
inference(extension,[status(thm),parent(t184:11)],[f_24_3]) ).
cnf(t243,plain,
$false,
inference(connection,[status(thm),parent(t242:1)],[t242:1,t184:11]) ).
cnf(t244,plain,
system_indi_has_citizenship(system,alice,usa),
inference(extension,[status(thm),parent(t242:2)],[f_72_2]) ).
cnf(t245,plain,
$false,
inference(connection,[status(thm),parent(t244:1)],[t244:1,t242:2]) ).
cnf(t246,plain,
( ~ admin_indi_has_background(admin,alice,topsecret)
| ~ oca_compartment_is_compartment(oca,compartmentb,confidential,topsecret,yes,yes)
| ~ system_indi_is_oca(system,oca)
| admin_indi_has_background_for_compartment(admin,alice,compartmentb) ),
inference(extension,[status(thm),parent(t30:5)],[f_29_4]) ).
cnf(t247,plain,
$false,
inference(connection,[status(thm),parent(t246:1)],[t246:1,t30:5]) ).
cnf(t248,plain,
system_indi_is_oca(system,oca),
inference(extension,[status(thm),parent(t246:2)],[f_42_2]) ).
cnf(t249,plain,
$false,
inference(connection,[status(thm),parent(t248:1)],[t248:1,t246:2]) ).
cnf(t250,plain,
oca_compartment_is_compartment(oca,compartmentb,confidential,topsecret,yes,yes),
inference(extension,[status(thm),parent(t246:3)],[f_43_2]) ).
cnf(t251,plain,
$false,
inference(connection,[status(thm),parent(t250:1)],[t250:1,t246:3]) ).
cnf(t252,plain,
( ~ background_admin_indi_has_background(background_admin,alice,topsecret)
| ~ loca_level_below(admin,topsecret,topsecret)
| ~ system_indi_is_background_admin(system,background_admin)
| admin_indi_has_background(admin,alice,topsecret) ),
inference(extension,[status(thm),parent(t246:4)],[f_21_4]) ).
cnf(t253,plain,
$false,
inference(connection,[status(thm),parent(t252:1)],[t252:1,t246:4]) ).
cnf(t254,plain,
system_indi_is_background_admin(system,background_admin),
inference(extension,[status(thm),parent(t252:2)],[f_69_2]) ).
cnf(t255,plain,
$false,
inference(connection,[status(thm),parent(t254:1)],[t254:1,t252:2]) ).
cnf(t256,plain,
loca_level_below(admin,topsecret,topsecret),
inference(extension,[status(thm),parent(t252:3)],[f_5_3]) ).
cnf(t257,plain,
$false,
inference(connection,[status(thm),parent(t256:1)],[t256:1,t252:3]) ).
cnf(t258,plain,
background_admin_indi_has_background(background_admin,alice,topsecret),
inference(extension,[status(thm),parent(t252:4)],[f_75_2]) ).
cnf(t259,plain,
$false,
inference(connection,[status(thm),parent(t258:1)],[t258:1,t252:4]) ).
cnf(t260,plain,
sso_indi_has_compartment(sso_compartmentb,alice,compartmentb),
inference(extension,[status(thm),parent(t30:6)],[f_81_2]) ).
cnf(t261,plain,
$false,
inference(connection,[status(thm),parent(t260:1)],[t260:1,t30:6]) ).
cnf(t262,plain,
( ~ system_compartment_has_sso(system,compartmentb,sso_compartmentb)
| admin_compartment_has_sso(admin,compartmentb,sso_compartmentb) ),
inference(extension,[status(thm),parent(t30:7)],[f_7_3]) ).
cnf(t263,plain,
$false,
inference(connection,[status(thm),parent(t262:1)],[t262:1,t30:7]) ).
cnf(t264,plain,
system_compartment_has_sso(system,compartmentb,sso_compartmentb),
inference(extension,[status(thm),parent(t262:2)],[f_45_2]) ).
cnf(t265,plain,
$false,
inference(connection,[status(thm),parent(t264:1)],[t264:1,t262:2]) ).
cnf(t266,plain,
( ~ admin_indi_has_credit(admin,alice)
| ~ oca_compartment_is_compartment(oca,compartmentb,confidential,topsecret,yes,yes)
| ~ system_indi_is_oca(system,oca)
| admin_indi_has_credit_for_compartment(admin,alice,compartmentb) ),
inference(extension,[status(thm),parent(t30:8)],[f_33_4]) ).
cnf(t267,plain,
$false,
inference(connection,[status(thm),parent(t266:1)],[t266:1,t30:8]) ).
cnf(t268,plain,
system_indi_is_oca(system,oca),
inference(extension,[status(thm),parent(t266:2)],[f_42_2]) ).
cnf(t269,plain,
$false,
inference(connection,[status(thm),parent(t268:1)],[t268:1,t266:2]) ).
cnf(t270,plain,
oca_compartment_is_compartment(oca,compartmentb,confidential,topsecret,yes,yes),
inference(extension,[status(thm),parent(t266:3)],[f_43_2]) ).
cnf(t271,plain,
$false,
inference(connection,[status(thm),parent(t270:1)],[t270:1,t266:3]) ).
cnf(t272,plain,
( ~ credit_admin_indi_has_credit(credit_admin,alice)
| ~ system_indi_is_credit_admin(system,credit_admin)
| admin_indi_has_credit(admin,alice) ),
inference(extension,[status(thm),parent(t266:4)],[f_19_3]) ).
cnf(t273,plain,
$false,
inference(connection,[status(thm),parent(t272:1)],[t272:1,t266:4]) ).
cnf(t274,plain,
system_indi_is_credit_admin(system,credit_admin),
inference(extension,[status(thm),parent(t272:2)],[f_68_2]) ).
cnf(t275,plain,
$false,
inference(connection,[status(thm),parent(t274:1)],[t274:1,t272:2]) ).
cnf(t276,plain,
credit_admin_indi_has_credit(credit_admin,alice),
inference(extension,[status(thm),parent(t272:3)],[f_74_2]) ).
cnf(t277,plain,
$false,
inference(connection,[status(thm),parent(t276:1)],[t276:1,t272:3]) ).
cnf(t278,plain,
( ~ admin_indi_has_polygraph(admin,alice)
| ~ oca_compartment_is_compartment(oca,compartmentb,confidential,topsecret,yes,yes)
| ~ system_indi_is_oca(system,oca)
| admin_indi_has_polygraph_for_compartment(admin,alice,compartmentb) ),
inference(extension,[status(thm),parent(t30:9)],[f_31_4]) ).
cnf(t279,plain,
$false,
inference(connection,[status(thm),parent(t278:1)],[t278:1,t30:9]) ).
cnf(t280,plain,
system_indi_is_oca(system,oca),
inference(extension,[status(thm),parent(t278:2)],[f_42_2]) ).
cnf(t281,plain,
$false,
inference(connection,[status(thm),parent(t280:1)],[t280:1,t278:2]) ).
cnf(t282,plain,
oca_compartment_is_compartment(oca,compartmentb,confidential,topsecret,yes,yes),
inference(extension,[status(thm),parent(t278:3)],[f_43_2]) ).
cnf(t283,plain,
$false,
inference(connection,[status(thm),parent(t282:1)],[t282:1,t278:3]) ).
cnf(t284,plain,
( ~ polygraph_admin_indi_has_polygraph(polygraph_admin,alice)
| ~ system_indi_is_polygraph_admin(system,polygraph_admin)
| admin_indi_has_polygraph(admin,alice) ),
inference(extension,[status(thm),parent(t278:4)],[f_18_3]) ).
cnf(t285,plain,
$false,
inference(connection,[status(thm),parent(t284:1)],[t284:1,t278:4]) ).
cnf(t286,plain,
system_indi_is_polygraph_admin(system,polygraph_admin),
inference(extension,[status(thm),parent(t284:2)],[f_67_2]) ).
cnf(t287,plain,
$false,
inference(connection,[status(thm),parent(t286:1)],[t286:1,t284:2]) ).
cnf(t288,plain,
polygraph_admin_indi_has_polygraph(polygraph_admin,alice),
inference(extension,[status(thm),parent(t284:3)],[f_73_2]) ).
cnf(t289,plain,
$false,
inference(connection,[status(thm),parent(t288:1)],[t288:1,t284:3]) ).
cnf(t290,plain,
( ~ system_indi_has_citizenship(system,alice,usa)
| admin_indi_has_citizenship(admin,alice,usa) ),
inference(extension,[status(thm),parent(t30:10)],[f_24_3]) ).
cnf(t291,plain,
$false,
inference(connection,[status(thm),parent(t290:1)],[t290:1,t30:10]) ).
cnf(t292,plain,
system_indi_has_citizenship(system,alice,usa),
inference(extension,[status(thm),parent(t290:2)],[f_72_2]) ).
cnf(t293,plain,
$false,
inference(connection,[status(thm),parent(t292:1)],[t292:1,t290:2]) ).
cnf(t294,plain,
( ~ hr_admin_indi_has_employment(hr_admin,alice)
| ~ system_indi_is_hr_admin(system,hr_admin)
| admin_indi_has_employment(admin,alice) ),
inference(extension,[status(thm),parent(t30:11)],[f_22_3]) ).
cnf(t295,plain,
$false,
inference(connection,[status(thm),parent(t294:1)],[t294:1,t30:11]) ).
cnf(t296,plain,
system_indi_is_hr_admin(system,hr_admin),
inference(extension,[status(thm),parent(t294:2)],[f_70_2]) ).
cnf(t297,plain,
$false,
inference(connection,[status(thm),parent(t296:1)],[t296:1,t294:2]) ).
cnf(t298,plain,
hr_admin_indi_has_employment(hr_admin,alice),
inference(extension,[status(thm),parent(t294:3)],[f_76_2]) ).
cnf(t299,plain,
$false,
inference(connection,[status(thm),parent(t298:1)],[t298:1,t294:3]) ).
cnf(t300,plain,
( ~ admin_indi_has_level(admin,alice,secret)
| ~ admin_file_has_level(admin,secretfile,secret)
| admin_indi_has_level_for_file(admin,alice,secretfile) ),
inference(extension,[status(thm),parent(t2:4)],[f_36_3]) ).
cnf(t301,plain,
$false,
inference(connection,[status(thm),parent(t300:1)],[t300:1,t2:4]) ).
cnf(t302,plain,
( ~ admin_file_has_compartments(admin,secretfile,cons(compartmentb,cons(compartmenta,nil)))
| ~ admin_file_has_level_h(admin,secretfile,secret,cons(compartmentb,cons(compartmenta,nil)))
| ~ system_file_needs_level(system,secretfile,secret)
| admin_file_has_level(admin,secretfile,secret) ),
inference(extension,[status(thm),parent(t300:2)],[f_12_4]) ).
cnf(t303,plain,
$false,
inference(connection,[status(thm),parent(t302:1)],[t302:1,t300:2]) ).
cnf(t304,plain,
system_file_needs_level(system,secretfile,secret),
inference(extension,[status(thm),parent(t302:2)],[f_55_2]) ).
cnf(t305,plain,
$false,
inference(connection,[status(thm),parent(t304:1)],[t304:1,t302:2]) ).
cnf(t306,plain,
( ~ 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))
| ~ admin_compartment_has_sso(admin,compartmentb,sso_compartmentb)
| admin_file_has_level_h(admin,secretfile,secret,cons(compartmentb,cons(compartmenta,nil))) ),
inference(extension,[status(thm),parent(t302:3)],[f_14_4]) ).
cnf(t307,plain,
$false,
inference(connection,[status(thm),parent(t306:1)],[t306:1,t302:3]) ).
cnf(t308,plain,
( ~ system_compartment_has_sso(system,compartmentb,sso_compartmentb)
| admin_compartment_has_sso(admin,compartmentb,sso_compartmentb) ),
inference(extension,[status(thm),parent(t306:2)],[f_7_3]) ).
cnf(t309,plain,
$false,
inference(connection,[status(thm),parent(t308:1)],[t308:1,t306:2]) ).
cnf(t310,plain,
system_compartment_has_sso(system,compartmentb,sso_compartmentb),
inference(extension,[status(thm),parent(t308:2)],[f_45_2]) ).
cnf(t311,plain,
$false,
inference(connection,[status(thm),parent(t310:1)],[t310:1,t308:2]) ).
cnf(l154,lemma,
admin_compartment_has_sso(admin,compartmentb,sso_compartmentb),
inference(lemma,[status(cth),parent(t306:2),below(t302:3)],[t306:2]) ).
cnf(t312,plain,
( ~ 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)
| ~ admin_compartment_has_sso(admin,compartmenta,sso_compartmenta)
| admin_file_has_level_h(admin,secretfile,secret,cons(compartmenta,nil)) ),
inference(extension,[status(thm),parent(t306:3)],[f_14_4]) ).
cnf(t313,plain,
$false,
inference(connection,[status(thm),parent(t312:1)],[t312:1,t306:3]) ).
cnf(t314,plain,
( ~ system_compartment_has_sso(system,compartmenta,sso_compartmenta)
| admin_compartment_has_sso(admin,compartmenta,sso_compartmenta) ),
inference(extension,[status(thm),parent(t312:2)],[f_7_3]) ).
cnf(t315,plain,
$false,
inference(connection,[status(thm),parent(t314:1)],[t314:1,t312:2]) ).
cnf(t316,plain,
system_compartment_has_sso(system,compartmenta,sso_compartmenta),
inference(extension,[status(thm),parent(t314:2)],[f_48_2]) ).
cnf(t317,plain,
$false,
inference(connection,[status(thm),parent(t316:1)],[t316:1,t314:2]) ).
cnf(l157,lemma,
admin_compartment_has_sso(admin,compartmenta,sso_compartmenta),
inference(lemma,[status(cth),parent(t312:2),below(t306:3)],[t312:2]) ).
cnf(t318,plain,
admin_file_has_level_h(admin,secretfile,secret,nil),
inference(extension,[status(thm),parent(t312:3)],[f_13_3]) ).
cnf(t319,plain,
$false,
inference(connection,[status(thm),parent(t318:1)],[t318:1,t312:3]) ).
cnf(t320,plain,
sso_file_has_level(sso_compartmenta,secretfile,secret,scg_compartmenta),
inference(extension,[status(thm),parent(t312:4)],[f_57_2]) ).
cnf(t321,plain,
$false,
inference(connection,[status(thm),parent(t320:1)],[t320:1,t312:4]) ).
cnf(t322,plain,
( ~ 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)
| ~ system_indi_is_oca(system,oca)
| admin_compartment_has_scg(admin,compartmenta,scg_compartmenta) ),
inference(extension,[status(thm),parent(t312:5)],[f_8_4]) ).
cnf(t323,plain,
$false,
inference(connection,[status(thm),parent(t322:1)],[t322:1,t312:5]) ).
cnf(t324,plain,
system_indi_is_oca(system,oca),
inference(extension,[status(thm),parent(t322:2)],[f_42_2]) ).
cnf(t325,plain,
$false,
inference(connection,[status(thm),parent(t324:1)],[t324:1,t322:2]) ).
cnf(t326,plain,
sso_compartment_has_scg(sso_compartmenta,compartmenta,scg_compartmenta),
inference(extension,[status(thm),parent(t322:3)],[f_50_2]) ).
cnf(t327,plain,
$false,
inference(connection,[status(thm),parent(t326:1)],[t326:1,t322:3]) ).
cnf(t328,plain,
admin_compartment_has_sso(admin,compartmenta,sso_compartmenta),
inference(lemma_extension,[status(thm),parent(t322:4)],[l157:1]) ).
cnf(t329,plain,
$false,
inference(connection,[status(thm),parent(t328:1)],[t328:1,t322:4]) ).
cnf(t330,plain,
oca_compartment_has_scg(oca,compartmenta,scg_compartmenta),
inference(extension,[status(thm),parent(t322:5)],[f_49_2]) ).
cnf(t331,plain,
$false,
inference(connection,[status(thm),parent(t330:1)],[t330:1,t322:5]) ).
cnf(t332,plain,
sso_file_has_level(sso_compartmentb,secretfile,secret,scg_compartmentb),
inference(extension,[status(thm),parent(t306:4)],[f_56_2]) ).
cnf(t333,plain,
$false,
inference(connection,[status(thm),parent(t332:1)],[t332:1,t306:4]) ).
cnf(t334,plain,
( ~ 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)
| ~ system_indi_is_oca(system,oca)
| admin_compartment_has_scg(admin,compartmentb,scg_compartmentb) ),
inference(extension,[status(thm),parent(t306:5)],[f_8_4]) ).
cnf(t335,plain,
$false,
inference(connection,[status(thm),parent(t334:1)],[t334:1,t306:5]) ).
cnf(t336,plain,
system_indi_is_oca(system,oca),
inference(extension,[status(thm),parent(t334:2)],[f_42_2]) ).
cnf(t337,plain,
$false,
inference(connection,[status(thm),parent(t336:1)],[t336:1,t334:2]) ).
cnf(t338,plain,
sso_compartment_has_scg(sso_compartmentb,compartmentb,scg_compartmentb),
inference(extension,[status(thm),parent(t334:3)],[f_47_2]) ).
cnf(t339,plain,
$false,
inference(connection,[status(thm),parent(t338:1)],[t338:1,t334:3]) ).
cnf(t340,plain,
admin_compartment_has_sso(admin,compartmentb,sso_compartmentb),
inference(lemma_extension,[status(thm),parent(t334:4)],[l154:1]) ).
cnf(t341,plain,
$false,
inference(connection,[status(thm),parent(t340:1)],[t340:1,t334:4]) ).
cnf(t342,plain,
oca_compartment_has_scg(oca,compartmentb,scg_compartmentb),
inference(extension,[status(thm),parent(t334:5)],[f_46_2]) ).
cnf(t343,plain,
$false,
inference(connection,[status(thm),parent(t342:1)],[t342:1,t334:5]) ).
cnf(t344,plain,
( ~ admin_file_has_compartments_h(admin,secretfile,cons(compartmentb,cons(compartmenta,nil)),cons(compartmentb,cons(compartmenta,nil)))
| ~ system_file_needs_compartments(system,secretfile,cons(compartmentb,cons(compartmenta,nil)))
| admin_file_has_compartments(admin,secretfile,cons(compartmentb,cons(compartmenta,nil))) ),
inference(extension,[status(thm),parent(t302:4)],[f_9_3]) ).
cnf(t345,plain,
$false,
inference(connection,[status(thm),parent(t344:1)],[t344:1,t302:4]) ).
cnf(t346,plain,
system_file_needs_compartments(system,secretfile,cons(compartmentb,cons(compartmenta,nil))),
inference(extension,[status(thm),parent(t344:2)],[f_52_2]) ).
cnf(t347,plain,
$false,
inference(connection,[status(thm),parent(t346:1)],[t346:1,t344:2]) ).
cnf(t348,plain,
( ~ 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))
| ~ admin_compartment_has_sso(admin,compartmentb,sso_compartmentb)
| admin_file_has_compartments_h(admin,secretfile,cons(compartmentb,cons(compartmenta,nil)),cons(compartmentb,cons(compartmenta,nil))) ),
inference(extension,[status(thm),parent(t344:3)],[f_11_3]) ).
cnf(t349,plain,
$false,
inference(connection,[status(thm),parent(t348:1)],[t348:1,t344:3]) ).
cnf(t350,plain,
( ~ system_compartment_has_sso(system,compartmentb,sso_compartmentb)
| admin_compartment_has_sso(admin,compartmentb,sso_compartmentb) ),
inference(extension,[status(thm),parent(t348:2)],[f_7_3]) ).
cnf(t351,plain,
$false,
inference(connection,[status(thm),parent(t350:1)],[t350:1,t348:2]) ).
cnf(t352,plain,
system_compartment_has_sso(system,compartmentb,sso_compartmentb),
inference(extension,[status(thm),parent(t350:2)],[f_45_2]) ).
cnf(t353,plain,
$false,
inference(connection,[status(thm),parent(t352:1)],[t352:1,t350:2]) ).
cnf(t354,plain,
( ~ 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)
| ~ admin_compartment_has_sso(admin,compartmenta,sso_compartmenta)
| admin_file_has_compartments_h(admin,secretfile,cons(compartmentb,cons(compartmenta,nil)),cons(compartmenta,nil)) ),
inference(extension,[status(thm),parent(t348:3)],[f_11_3]) ).
cnf(t355,plain,
$false,
inference(connection,[status(thm),parent(t354:1)],[t354:1,t348:3]) ).
cnf(t356,plain,
( ~ system_compartment_has_sso(system,compartmenta,sso_compartmenta)
| admin_compartment_has_sso(admin,compartmenta,sso_compartmenta) ),
inference(extension,[status(thm),parent(t354:2)],[f_7_3]) ).
cnf(t357,plain,
$false,
inference(connection,[status(thm),parent(t356:1)],[t356:1,t354:2]) ).
cnf(t358,plain,
system_compartment_has_sso(system,compartmenta,sso_compartmenta),
inference(extension,[status(thm),parent(t356:2)],[f_48_2]) ).
cnf(t359,plain,
$false,
inference(connection,[status(thm),parent(t358:1)],[t358:1,t356:2]) ).
cnf(t360,plain,
admin_file_has_compartments_h(admin,secretfile,cons(compartmentb,cons(compartmenta,nil)),nil),
inference(extension,[status(thm),parent(t354:3)],[f_10_3]) ).
cnf(t361,plain,
$false,
inference(connection,[status(thm),parent(t360:1)],[t360:1,t354:3]) ).
cnf(t362,plain,
sso_file_has_compartments(sso_compartmenta,secretfile,cons(compartmentb,cons(compartmenta,nil))),
inference(extension,[status(thm),parent(t354:4)],[f_54_2]) ).
cnf(t363,plain,
$false,
inference(connection,[status(thm),parent(t362:1)],[t362:1,t354:4]) ).
cnf(t364,plain,
sso_file_has_compartments(sso_compartmentb,secretfile,cons(compartmentb,cons(compartmenta,nil))),
inference(extension,[status(thm),parent(t348:4)],[f_53_2]) ).
cnf(t365,plain,
$false,
inference(connection,[status(thm),parent(t364:1)],[t364:1,t348:4]) ).
cnf(t366,plain,
( ~ 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)
| ~ system_indi_needs_level(system,alice,secret)
| admin_indi_has_level(admin,alice,secret) ),
inference(extension,[status(thm),parent(t300:3)],[f_26_4]) ).
cnf(t367,plain,
$false,
inference(connection,[status(thm),parent(t366:1)],[t366:1,t300:3]) ).
cnf(t368,plain,
system_indi_needs_level(system,alice,secret),
inference(extension,[status(thm),parent(t366:2)],[f_77_2]) ).
cnf(t369,plain,
$false,
inference(connection,[status(thm),parent(t368:1)],[t368:1,t366:2]) ).
cnf(t370,plain,
( ~ background_admin_indi_has_background(background_admin,alice,topsecret)
| ~ loca_level_below(admin,secret,topsecret)
| ~ system_indi_is_background_admin(system,background_admin)
| admin_indi_has_background(admin,alice,secret) ),
inference(extension,[status(thm),parent(t366:3)],[f_21_4]) ).
cnf(t371,plain,
$false,
inference(connection,[status(thm),parent(t370:1)],[t370:1,t366:3]) ).
cnf(t372,plain,
system_indi_is_background_admin(system,background_admin),
inference(extension,[status(thm),parent(t370:2)],[f_69_2]) ).
cnf(t373,plain,
$false,
inference(connection,[status(thm),parent(t372:1)],[t372:1,t370:2]) ).
cnf(t374,plain,
( ~ loca_level_below(admin,secret,secret)
| ~ loca_level_direct_below(admin,secret,topsecret)
| loca_level_below(admin,secret,topsecret) ),
inference(extension,[status(thm),parent(t370:3)],[f_6_3]) ).
cnf(t375,plain,
$false,
inference(connection,[status(thm),parent(t374:1)],[t374:1,t370:3]) ).
cnf(t376,plain,
loca_level_direct_below(admin,secret,topsecret),
inference(extension,[status(thm),parent(t374:2)],[f_4_3]) ).
cnf(t377,plain,
$false,
inference(connection,[status(thm),parent(t376:1)],[t376:1,t374:2]) ).
cnf(t378,plain,
loca_level_below(admin,secret,secret),
inference(extension,[status(thm),parent(t374:3)],[f_5_3]) ).
cnf(t379,plain,
$false,
inference(connection,[status(thm),parent(t378:1)],[t378:1,t374:3]) ).
cnf(t380,plain,
background_admin_indi_has_background(background_admin,alice,topsecret),
inference(extension,[status(thm),parent(t370:4)],[f_75_2]) ).
cnf(t381,plain,
$false,
inference(connection,[status(thm),parent(t380:1)],[t380:1,t370:4]) ).
cnf(t382,plain,
( ~ loca_level_below(admin,secret,secret)
| ~ loca_level_direct_below(admin,secret,topsecret)
| loca_level_below(admin,secret,topsecret) ),
inference(extension,[status(thm),parent(t366:4)],[f_6_3]) ).
cnf(t383,plain,
$false,
inference(connection,[status(thm),parent(t382:1)],[t382:1,t366:4]) ).
cnf(t384,plain,
loca_level_direct_below(admin,secret,topsecret),
inference(extension,[status(thm),parent(t382:2)],[f_4_3]) ).
cnf(t385,plain,
$false,
inference(connection,[status(thm),parent(t384:1)],[t384:1,t382:2]) ).
cnf(t386,plain,
loca_level_below(admin,secret,secret),
inference(extension,[status(thm),parent(t382:3)],[f_5_3]) ).
cnf(t387,plain,
$false,
inference(connection,[status(thm),parent(t386:1)],[t386:1,t382:3]) ).
cnf(t388,plain,
level_admin_indi_has_level(level_admin,alice,topsecret),
inference(extension,[status(thm),parent(t366:5)],[f_78_2]) ).
cnf(t389,plain,
$false,
inference(connection,[status(thm),parent(t388:1)],[t388:1,t366:5]) ).
cnf(t390,plain,
system_indi_is_level_admin(system,level_admin),
inference(extension,[status(thm),parent(t366:6)],[f_71_2]) ).
cnf(t391,plain,
$false,
inference(connection,[status(thm),parent(t390:1)],[t390:1,t366:6]) ).
cnf(t392,plain,
loca_level_below(admin,secret,secret),
inference(extension,[status(thm),parent(t366:7)],[f_5_3]) ).
cnf(t393,plain,
$false,
inference(connection,[status(thm),parent(t392:1)],[t392:1,t366:7]) ).
cnf(t394,plain,
( ~ credit_admin_indi_has_credit(credit_admin,alice)
| ~ system_indi_is_credit_admin(system,credit_admin)
| admin_indi_has_credit(admin,alice) ),
inference(extension,[status(thm),parent(t366:8)],[f_19_3]) ).
cnf(t395,plain,
$false,
inference(connection,[status(thm),parent(t394:1)],[t394:1,t366:8]) ).
cnf(t396,plain,
system_indi_is_credit_admin(system,credit_admin),
inference(extension,[status(thm),parent(t394:2)],[f_68_2]) ).
cnf(t397,plain,
$false,
inference(connection,[status(thm),parent(t396:1)],[t396:1,t394:2]) ).
cnf(t398,plain,
credit_admin_indi_has_credit(credit_admin,alice),
inference(extension,[status(thm),parent(t394:3)],[f_74_2]) ).
cnf(t399,plain,
$false,
inference(connection,[status(thm),parent(t398:1)],[t398:1,t394:3]) ).
cnf(t400,plain,
( ~ hr_admin_indi_has_employment(hr_admin,alice)
| ~ system_indi_is_hr_admin(system,hr_admin)
| admin_indi_has_employment(admin,alice) ),
inference(extension,[status(thm),parent(t366:9)],[f_22_3]) ).
cnf(t401,plain,
$false,
inference(connection,[status(thm),parent(t400:1)],[t400:1,t366:9]) ).
cnf(t402,plain,
system_indi_is_hr_admin(system,hr_admin),
inference(extension,[status(thm),parent(t400:2)],[f_70_2]) ).
cnf(t403,plain,
$false,
inference(connection,[status(thm),parent(t402:1)],[t402:1,t400:2]) ).
cnf(t404,plain,
hr_admin_indi_has_employment(hr_admin,alice),
inference(extension,[status(thm),parent(t400:3)],[f_76_2]) ).
cnf(t405,plain,
$false,
inference(connection,[status(thm),parent(t404:1)],[t404:1,t400:3]) ).
cnf(t406,plain,
( ~ polygraph_admin_indi_has_polygraph(polygraph_admin,alice)
| ~ system_indi_is_polygraph_admin(system,polygraph_admin)
| admin_indi_has_polygraph(admin,alice) ),
inference(extension,[status(thm),parent(t366:10)],[f_18_3]) ).
cnf(t407,plain,
$false,
inference(connection,[status(thm),parent(t406:1)],[t406:1,t366:10]) ).
cnf(t408,plain,
system_indi_is_polygraph_admin(system,polygraph_admin),
inference(extension,[status(thm),parent(t406:2)],[f_67_2]) ).
cnf(t409,plain,
$false,
inference(connection,[status(thm),parent(t408:1)],[t408:1,t406:2]) ).
cnf(t410,plain,
polygraph_admin_indi_has_polygraph(polygraph_admin,alice),
inference(extension,[status(thm),parent(t406:3)],[f_73_2]) ).
cnf(t411,plain,
$false,
inference(connection,[status(thm),parent(t410:1)],[t410:1,t406:3]) ).
cnf(t412,plain,
( ~ system_indi_has_citizenship(system,alice,usa)
| admin_indi_has_citizenship(admin,alice,usa) ),
inference(extension,[status(thm),parent(t366:11)],[f_24_3]) ).
cnf(t413,plain,
$false,
inference(connection,[status(thm),parent(t412:1)],[t412:1,t366:11]) ).
cnf(t414,plain,
system_indi_has_citizenship(system,alice,usa),
inference(extension,[status(thm),parent(t412:2)],[f_72_2]) ).
cnf(t415,plain,
$false,
inference(connection,[status(thm),parent(t414:1)],[t414:1,t412:2]) ).
cnf(t416,plain,
( ~ owner_indi_has_need_to_know(owner_secretfile,alice,secretfile)
| ~ state_file_has_owner(secretfile,owner_secretfile)
| admin_indi_has_need_to_know_for_file(admin,alice,secretfile) ),
inference(extension,[status(thm),parent(t2:5)],[f_37_3]) ).
cnf(t417,plain,
$false,
inference(connection,[status(thm),parent(t416:1)],[t416:1,t2:5]) ).
cnf(t418,plain,
state_file_has_owner(secretfile,owner_secretfile),
inference(extension,[status(thm),parent(t416:2)],[f_61_2]) ).
cnf(t419,plain,
$false,
inference(connection,[status(thm),parent(t418:1)],[t418:1,t416:2]) ).
cnf(t420,plain,
owner_indi_has_need_to_know(owner_secretfile,alice,secretfile),
inference(extension,[status(thm),parent(t416:3)],[f_83_2]) ).
cnf(t421,plain,
$false,
inference(connection,[status(thm),parent(t420:1)],[t420:1,t416:3]) ).
cnf(t422,plain,
( ~ admin_indi_has_citizenship(admin,alice,usa)
| admin_indi_has_citizenship_for_file(admin,alice,secretfile) ),
inference(extension,[status(thm),parent(t2:6)],[f_39_4]) ).
cnf(t423,plain,
$false,
inference(connection,[status(thm),parent(t422:1)],[t422:1,t2:6]) ).
cnf(t424,plain,
( ~ system_indi_has_citizenship(system,alice,usa)
| admin_indi_has_citizenship(admin,alice,usa) ),
inference(extension,[status(thm),parent(t422:2)],[f_24_3]) ).
cnf(t425,plain,
$false,
inference(connection,[status(thm),parent(t424:1)],[t424:1,t422:2]) ).
cnf(t426,plain,
system_indi_has_citizenship(system,alice,usa),
inference(extension,[status(thm),parent(t424:2)],[f_72_2]) ).
cnf(t427,plain,
$false,
inference(connection,[status(thm),parent(t426:1)],[t426:1,t424:2]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SWV437+1 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.03 This is a FOF_THM_RFO_NEQ problem
% 0.00/0.04 % Command : /export/starexec/sandbox2/solver/bin/connect++ --verbosity 1 --no-colour --tptp-proof --schedule default --timeout 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.09/0.36 % Computer : n008.cluster.edu
% 0.09/0.36 % Model : x86_64 x86_64
% 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.36 % Memory : 8046.5625MB
% 0.09/0.36 % OS : Linux 6.8.0-71-generic
% 0.12/0.36 % CPULimit : 300
% 0.12/0.36 % WCLimit : 300
% 0.12/0.36 % DateTime : Sun Sep 20 03:42:25 UTC 2026
% 0.12/0.36 % CPUTime :
% 2.15/2.43 % SZS status Theorem for theBenchmark
% 2.15/2.43 % SZS output start Proof for theBenchmark
% See solution above
%------------------------------------------------------------------------------