%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : SWV437+1 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n017.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 : Sun Sep 27 09:07:57 AM UTC 2026
% Result : Theorem 0.10s 0.45s
% Output : CNFRefutation 0.10s
% Verified :
% SZS Type : Refutation
% Derivation depth : 30
% Number of leaves : 68
% Syntax : Number of formulae : 263 ( 109 unt; 0 def)
% Number of atoms : 864 ( 0 equ)
% Maximal formula atoms : 11 ( 3 avg)
% Number of connectives : 1137 ( 536 ~; 524 |; 0 &)
% ( 0 <=>; 77 =>; 0 <=; 0 <~>)
% Maximal formula depth : 16 ( 4 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 : 617 ( 258 sgn 109 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(ax1,axiom,
! [K] : loca_level_direct_below(K,sbu,confidential),
file('theBenchmark.p',ax1) ).
fof(ax2,axiom,
! [K] : loca_level_direct_below(K,confidential,secret),
file('theBenchmark.p',ax2) ).
fof(ax3,axiom,
! [K] : loca_level_direct_below(K,secret,topsecret),
file('theBenchmark.p',ax3) ).
fof(ax4,axiom,
! [K,L] : loca_level_below(K,L,L),
file('theBenchmark.p',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('theBenchmark.p',ax5) ).
fof(ax6,axiom,
! [C,SSO] :
( system_compartment_has_sso(system,C,SSO)
=> admin_compartment_has_sso(admin,C,SSO) ),
file('theBenchmark.p',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('theBenchmark.p',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('theBenchmark.p',ax8) ).
fof(ax9,axiom,
! [F,CL] : admin_file_has_compartments_h(admin,F,CL,nil),
file('theBenchmark.p',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('theBenchmark.p',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('theBenchmark.p',ax11) ).
fof(ax12,axiom,
! [F,L] : admin_file_has_level_h(admin,F,L,nil),
file('theBenchmark.p',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('theBenchmark.p',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('theBenchmark.p',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('theBenchmark.p',ax18) ).
fof(ax19,axiom,
! [K] : admin_indi_has_background(admin,K,unclassified),
file('theBenchmark.p',ax19) ).
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('theBenchmark.p',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('theBenchmark.p',ax21) ).
fof(ax23,axiom,
! [K,U] :
( system_indi_has_citizenship(system,K,U)
=> admin_indi_has_citizenship(admin,K,U) ),
file('theBenchmark.p',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('theBenchmark.p',ax25) ).
fof(ax26,axiom,
! [K] : admin_indi_has_compartments(admin,K,nil),
file('theBenchmark.p',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('theBenchmark.p',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('theBenchmark.p',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('theBenchmark.p',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('theBenchmark.p',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('theBenchmark.p',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('theBenchmark.p',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('theBenchmark.p',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('theBenchmark.p',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('theBenchmark.p',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('theBenchmark.p',ax36) ).
fof(ax38,axiom,
! [K,F] :
( admin_indi_has_citizenship(admin,K,usa)
=> admin_indi_has_citizenship_for_file(admin,K,F) ),
file('theBenchmark.p',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('theBenchmark.p',ax39) ).
fof(alicereadsecret,conjecture,
admin_indi_may_file(admin,alice,secretfile,read),
file('theBenchmark.p',alicereadsecret) ).
fof(alicereadsecret_neg,negated_conjecture,
~ admin_indi_may_file(admin,alice,secretfile,read),
inference(assume_negation,[status(cth)],[alicereadsecret]) ).
cnf(c_43,plain,
( loca_level_below(A,D,C)
| ~ loca_level_below(A,D,B)
| ~ loca_level_direct_below(A,B,C) ),
inference(clausify,[status(thm)],[ax5]) ).
cnf(c_44,plain,
loca_level_direct_below(A,secret,topsecret),
inference(clausify,[status(thm)],[ax3]) ).
cnf(c_45,plain,
loca_level_direct_below(A,confidential,secret),
inference(clausify,[status(thm)],[ax2]) ).
cnf(c_46,plain,
loca_level_direct_below(A,sbu,confidential),
inference(clausify,[status(thm)],[ax1]) ).
cnf(c_48,plain,
( admin_compartment_has_sso(admin,A,B)
| ~ system_compartment_has_sso(system,A,B) ),
inference(clausify,[status(thm)],[ax6]) ).
fof(ax44,axiom,
system_compartment_has_sso(system,compartmentb,sso_compartmentb),
file('theBenchmark.p',ax44) ).
cnf(c_49,plain,
system_compartment_has_sso(system,compartmentb,sso_compartmentb),
inference(clausify,[status(thm)],[ax44]) ).
fof(ax47,axiom,
system_compartment_has_sso(system,compartmenta,sso_compartmenta),
file('theBenchmark.p',ax47) ).
cnf(c_50,plain,
system_compartment_has_sso(system,compartmenta,sso_compartmenta),
inference(clausify,[status(thm)],[ax47]) ).
cnf(c_51,plain,
( admin_compartment_has_scg(admin,B,C)
| ~ sso_compartment_has_scg(D,B,C)
| ~ admin_compartment_has_sso(admin,B,D)
| ~ oca_compartment_has_scg(A,B,C)
| ~ system_indi_is_oca(system,A) ),
inference(clausify,[status(thm)],[ax7]) ).
cnf(c_52,plain,
admin_compartment_has_sso(admin,compartmentb,sso_compartmentb),
inference(resolve,[status(thm)],[c_48,c_49]) ).
cnf(c_53,plain,
admin_compartment_has_sso(admin,compartmenta,sso_compartmenta),
inference(resolve,[status(thm)],[c_48,c_50]) ).
cnf(c_54,plain,
( admin_file_has_compartments_h(admin,C,D,cons(A,E))
| ~ admin_file_has_compartments_h(admin,C,D,E)
| ~ sso_file_has_compartments(B,C,D)
| ~ admin_compartment_has_sso(admin,A,B) ),
inference(clausify,[status(thm)],[ax10]) ).
cnf(c_55,plain,
( admin_file_has_level_h(admin,D,E,cons(A,F))
| ~ admin_file_has_level_h(admin,D,E,F)
| ~ sso_file_has_level(B,D,E,C)
| ~ admin_compartment_has_scg(admin,A,C)
| ~ admin_compartment_has_sso(admin,A,B) ),
inference(clausify,[status(thm)],[ax13]) ).
cnf(c_57,plain,
( admin_indi_has_compartments(admin,A,cons(B,D))
| ~ admin_indi_has_compartments(admin,A,D)
| ~ admin_indi_has_level_for_compartment(admin,A,B)
| ~ admin_indi_has_background_for_compartment(admin,A,B)
| ~ sso_indi_has_compartment(C,A,B)
| ~ admin_compartment_has_sso(admin,B,C)
| ~ admin_indi_has_credit_for_compartment(admin,A,B)
| ~ admin_indi_has_polygraph_for_compartment(admin,A,B)
| ~ admin_indi_has_citizenship(admin,A,usa)
| ~ admin_indi_has_employment(admin,A)
| ~ system_indi_needs_compartment(system,A,B) ),
inference(clausify,[status(thm)],[ax27]) ).
fof(ax41,axiom,
system_indi_is_oca(system,oca),
file('theBenchmark.p',ax41) ).
cnf(c_58,plain,
system_indi_is_oca(system,oca),
inference(clausify,[status(thm)],[ax41]) ).
cnf(c_59,plain,
( admin_compartment_has_scg(admin,compartmentb,B)
| ~ sso_compartment_has_scg(sso_compartmentb,compartmentb,B)
| ~ oca_compartment_has_scg(A,compartmentb,B)
| ~ system_indi_is_oca(system,A) ),
inference(resolve,[status(thm)],[c_51,c_52]) ).
cnf(c_60,plain,
( admin_compartment_has_scg(admin,compartmenta,B)
| ~ sso_compartment_has_scg(sso_compartmenta,compartmenta,B)
| ~ oca_compartment_has_scg(A,compartmenta,B)
| ~ system_indi_is_oca(system,A) ),
inference(resolve,[status(thm)],[c_51,c_53]) ).
cnf(c_61,plain,
( admin_indi_has_credit_for_compartment(admin,F,B)
| ~ oca_compartment_is_compartment(A,B,C,D,no,E)
| ~ system_indi_is_oca(system,A) ),
inference(clausify,[status(thm)],[ax33]) ).
cnf(c_62,plain,
( admin_indi_has_credit_for_compartment(admin,F,B)
| ~ admin_indi_has_credit(admin,F)
| ~ oca_compartment_is_compartment(A,B,C,D,yes,E)
| ~ system_indi_is_oca(system,A) ),
inference(clausify,[status(thm)],[ax32]) ).
cnf(c_63,plain,
( admin_indi_has_polygraph_for_compartment(admin,F,B)
| ~ oca_compartment_is_compartment(A,B,C,D,E,no)
| ~ system_indi_is_oca(system,A) ),
inference(clausify,[status(thm)],[ax31]) ).
cnf(c_64,plain,
( admin_indi_has_polygraph_for_compartment(admin,F,B)
| ~ admin_indi_has_polygraph(admin,F)
| ~ oca_compartment_is_compartment(A,B,C,D,E,yes)
| ~ system_indi_is_oca(system,A) ),
inference(clausify,[status(thm)],[ax30]) ).
cnf(c_65,plain,
( admin_indi_has_level_for_compartment(admin,V6,B)
| ~ admin_indi_has_level(admin,V6,C)
| ~ oca_compartment_is_compartment(A,B,C,D,E,F)
| ~ system_indi_is_oca(system,A) ),
inference(clausify,[status(thm)],[ax29]) ).
cnf(c_66,plain,
( admin_indi_has_background_for_compartment(admin,V6,B)
| ~ admin_indi_has_background(admin,V6,D)
| ~ oca_compartment_is_compartment(A,B,C,D,E,F)
| ~ system_indi_is_oca(system,A) ),
inference(clausify,[status(thm)],[ax28]) ).
fof(ax45,axiom,
oca_compartment_has_scg(oca,compartmentb,scg_compartmentb),
file('theBenchmark.p',ax45) ).
cnf(c_67,plain,
oca_compartment_has_scg(oca,compartmentb,scg_compartmentb),
inference(clausify,[status(thm)],[ax45]) ).
cnf(c_68,plain,
( admin_compartment_has_scg(admin,compartmentb,A)
| ~ sso_compartment_has_scg(sso_compartmentb,compartmentb,A)
| ~ oca_compartment_has_scg(oca,compartmentb,A) ),
inference(resolve,[status(thm)],[c_58,c_59]) ).
cnf(c_69,plain,
( admin_compartment_has_scg(admin,compartmenta,A)
| ~ sso_compartment_has_scg(sso_compartmenta,compartmenta,A)
| ~ oca_compartment_has_scg(oca,compartmenta,A) ),
inference(resolve,[status(thm)],[c_58,c_60]) ).
fof(ax48,axiom,
oca_compartment_has_scg(oca,compartmenta,scg_compartmenta),
file('theBenchmark.p',ax48) ).
cnf(c_70,plain,
oca_compartment_has_scg(oca,compartmenta,scg_compartmenta),
inference(clausify,[status(thm)],[ax48]) ).
fof(ax49,axiom,
sso_compartment_has_scg(sso_compartmenta,compartmenta,scg_compartmenta),
file('theBenchmark.p',ax49) ).
cnf(c_71,plain,
sso_compartment_has_scg(sso_compartmenta,compartmenta,scg_compartmenta),
inference(clausify,[status(thm)],[ax49]) ).
cnf(c_72,plain,
( admin_compartment_has_scg(admin,compartmentb,scg_compartmentb)
| ~ sso_compartment_has_scg(sso_compartmentb,compartmentb,scg_compartmentb) ),
inference(resolve,[status(thm)],[c_67,c_68]) ).
cnf(c_73,plain,
( admin_compartment_has_scg(admin,compartmenta,scg_compartmenta)
| ~ sso_compartment_has_scg(sso_compartmenta,compartmenta,scg_compartmenta) ),
inference(resolve,[status(thm)],[c_70,c_69]) ).
fof(ax46,axiom,
sso_compartment_has_scg(sso_compartmentb,compartmentb,scg_compartmentb),
file('theBenchmark.p',ax46) ).
cnf(c_74,plain,
sso_compartment_has_scg(sso_compartmentb,compartmentb,scg_compartmentb),
inference(clausify,[status(thm)],[ax46]) ).
cnf(c_75,plain,
( admin_file_has_level_h(admin,B,C,cons(compartmentb,D))
| ~ admin_file_has_level_h(admin,B,C,D)
| ~ sso_file_has_level(sso_compartmentb,B,C,A)
| ~ admin_compartment_has_scg(admin,compartmentb,A) ),
inference(resolve,[status(thm)],[c_55,c_52]) ).
cnf(c_76,plain,
admin_compartment_has_scg(admin,compartmenta,scg_compartmenta),
inference(resolve,[status(thm)],[c_71,c_73]) ).
cnf(c_77,plain,
admin_compartment_has_scg(admin,compartmentb,scg_compartmentb),
inference(resolve,[status(thm)],[c_74,c_72]) ).
cnf(c_78,plain,
( admin_file_has_level_h(admin,B,C,cons(compartmenta,D))
| ~ admin_file_has_level_h(admin,B,C,D)
| ~ sso_file_has_level(sso_compartmenta,B,C,A)
| ~ admin_compartment_has_scg(admin,compartmenta,A) ),
inference(resolve,[status(thm)],[c_55,c_53]) ).
cnf(c_81,plain,
( admin_file_has_compartments(admin,A,B)
| ~ admin_file_has_compartments_h(admin,A,B,B)
| ~ system_file_needs_compartments(system,A,B) ),
inference(clausify,[status(thm)],[ax8]) ).
fof(ax51,axiom,
system_file_needs_compartments(system,secretfile,cons(compartmentb,cons(compartmenta,nil))),
file('theBenchmark.p',ax51) ).
cnf(c_82,plain,
system_file_needs_compartments(system,secretfile,cons(compartmentb,cons(compartmenta,nil))),
inference(clausify,[status(thm)],[ax51]) ).
cnf(c_84,plain,
( admin_file_has_level(admin,A,B)
| ~ admin_file_has_level_h(admin,A,B,C)
| ~ admin_file_has_compartments(admin,A,C)
| ~ system_file_needs_level(system,A,B) ),
inference(clausify,[status(thm)],[ax11]) ).
cnf(c_85,plain,
( admin_file_has_compartments(admin,secretfile,cons(compartmentb,cons(compartmenta,nil)))
| ~ admin_file_has_compartments_h(admin,secretfile,cons(compartmentb,cons(compartmenta,nil)),cons(compartmentb,cons(compartmenta,nil))) ),
inference(resolve,[status(thm)],[c_81,c_82]) ).
cnf(c_88,plain,
( admin_indi_has_compartments_for_file(admin,C,A)
| ~ admin_indi_has_compartments(admin,C,B)
| ~ admin_file_has_compartments(admin,A,B) ),
inference(clausify,[status(thm)],[ax34]) ).
fof(ax53,axiom,
sso_file_has_compartments(sso_compartmenta,secretfile,cons(compartmentb,cons(compartmenta,nil))),
file('theBenchmark.p',ax53) ).
cnf(c_89,plain,
sso_file_has_compartments(sso_compartmenta,secretfile,cons(compartmentb,cons(compartmenta,nil))),
inference(clausify,[status(thm)],[ax53]) ).
cnf(c_90,plain,
( admin_file_has_compartments_h(admin,A,B,cons(compartmentb,C))
| ~ admin_file_has_compartments_h(admin,A,B,C)
| ~ sso_file_has_compartments(sso_compartmentb,A,B) ),
inference(resolve,[status(thm)],[c_54,c_52]) ).
cnf(c_91,plain,
( admin_file_has_compartments_h(admin,A,B,cons(compartmenta,C))
| ~ admin_file_has_compartments_h(admin,A,B,C)
| ~ sso_file_has_compartments(sso_compartmenta,A,B) ),
inference(resolve,[status(thm)],[c_54,c_53]) ).
fof(ax52,axiom,
sso_file_has_compartments(sso_compartmentb,secretfile,cons(compartmentb,cons(compartmenta,nil))),
file('theBenchmark.p',ax52) ).
cnf(c_92,plain,
sso_file_has_compartments(sso_compartmentb,secretfile,cons(compartmentb,cons(compartmenta,nil))),
inference(clausify,[status(thm)],[ax52]) ).
cnf(c_93,plain,
( ~ admin_file_has_compartments_h(admin,secretfile,cons(compartmentb,cons(compartmenta,nil)),cons(compartmentb,cons(compartmenta,nil)))
| admin_file_has_level(admin,secretfile,A)
| ~ admin_file_has_level_h(admin,secretfile,A,cons(compartmentb,cons(compartmenta,nil)))
| ~ system_file_needs_level(system,secretfile,A) ),
inference(resolve,[status(thm)],[c_84,c_85]) ).
fof(ax54,axiom,
system_file_needs_level(system,secretfile,secret),
file('theBenchmark.p',ax54) ).
cnf(c_95,plain,
system_file_needs_level(system,secretfile,secret),
inference(clausify,[status(thm)],[ax54]) ).
cnf(c_97,plain,
( admin_indi_has_level_for_file(admin,C,A)
| ~ admin_indi_has_level(admin,C,B)
| ~ admin_file_has_level(admin,A,B) ),
inference(clausify,[status(thm)],[ax35]) ).
cnf(c_98,plain,
( ~ admin_file_has_compartments_h(admin,secretfile,cons(compartmentb,cons(compartmenta,nil)),cons(compartmentb,cons(compartmenta,nil)))
| admin_file_has_level(admin,secretfile,secret)
| ~ admin_file_has_level_h(admin,secretfile,secret,cons(compartmentb,cons(compartmenta,nil))) ),
inference(resolve,[status(thm)],[c_93,c_95]) ).
cnf(c_100,plain,
( admin_file_has_level_h(admin,A,B,cons(compartmentb,C))
| ~ admin_file_has_level_h(admin,A,B,C)
| ~ sso_file_has_level(sso_compartmentb,A,B,scg_compartmentb) ),
inference(resolve,[status(thm)],[c_75,c_77]) ).
fof(ax56,axiom,
sso_file_has_level(sso_compartmenta,secretfile,secret,scg_compartmenta),
file('theBenchmark.p',ax56) ).
cnf(c_101,plain,
sso_file_has_level(sso_compartmenta,secretfile,secret,scg_compartmenta),
inference(clausify,[status(thm)],[ax56]) ).
fof(ax55,axiom,
sso_file_has_level(sso_compartmentb,secretfile,secret,scg_compartmentb),
file('theBenchmark.p',ax55) ).
cnf(c_102,plain,
sso_file_has_level(sso_compartmentb,secretfile,secret,scg_compartmentb),
inference(clausify,[status(thm)],[ax55]) ).
cnf(c_103,plain,
( admin_file_has_level_h(admin,A,B,cons(compartmenta,C))
| ~ admin_file_has_level_h(admin,A,B,C)
| ~ sso_file_has_level(sso_compartmenta,A,B,scg_compartmenta) ),
inference(resolve,[status(thm)],[c_78,c_76]) ).
fof(ax66,axiom,
system_indi_is_polygraph_admin(system,polygraph_admin),
file('theBenchmark.p',ax66) ).
cnf(c_115,plain,
system_indi_is_polygraph_admin(system,polygraph_admin),
inference(clausify,[status(thm)],[ax66]) ).
cnf(c_116,plain,
( admin_indi_has_polygraph(admin,B)
| ~ polygraph_admin_indi_has_polygraph(A,B)
| ~ system_indi_is_polygraph_admin(system,A) ),
inference(clausify,[status(thm)],[ax17]) ).
fof(ax72,axiom,
polygraph_admin_indi_has_polygraph(polygraph_admin,alice),
file('theBenchmark.p',ax72) ).
cnf(c_117,plain,
polygraph_admin_indi_has_polygraph(polygraph_admin,alice),
inference(clausify,[status(thm)],[ax72]) ).
cnf(c_118,plain,
( admin_indi_has_polygraph(admin,A)
| ~ polygraph_admin_indi_has_polygraph(polygraph_admin,A) ),
inference(resolve,[status(thm)],[c_115,c_116]) ).
cnf(c_119,plain,
( admin_indi_has_polygraph_for_compartment(admin,E,A)
| ~ admin_indi_has_polygraph(admin,E)
| ~ oca_compartment_is_compartment(oca,A,B,C,D,yes) ),
inference(resolve,[status(thm)],[c_64,c_58]) ).
cnf(c_120,plain,
admin_indi_has_polygraph(admin,alice),
inference(resolve,[status(thm)],[c_117,c_118]) ).
cnf(c_121,plain,
( admin_indi_has_level(admin,A,C)
| ~ admin_indi_has_background(admin,A,C)
| ~ loca_level_below(admin,C,E)
| ~ level_admin_indi_has_level(D,A,E)
| ~ system_indi_is_level_admin(system,D)
| ~ loca_level_below(admin,C,B)
| ~ admin_indi_has_credit(admin,A)
| ~ admin_indi_has_employment(admin,A)
| ~ admin_indi_has_polygraph(admin,A)
| ~ admin_indi_has_citizenship(admin,A,usa)
| ~ system_indi_needs_level(system,A,B) ),
inference(clausify,[status(thm)],[ax25]) ).
cnf(c_122,plain,
( admin_indi_has_credit(admin,B)
| ~ credit_admin_indi_has_credit(A,B)
| ~ system_indi_is_credit_admin(system,A) ),
inference(clausify,[status(thm)],[ax18]) ).
fof(ax67,axiom,
system_indi_is_credit_admin(system,credit_admin),
file('theBenchmark.p',ax67) ).
cnf(c_123,plain,
system_indi_is_credit_admin(system,credit_admin),
inference(clausify,[status(thm)],[ax67]) ).
fof(ax73,axiom,
credit_admin_indi_has_credit(credit_admin,alice),
file('theBenchmark.p',ax73) ).
cnf(c_124,plain,
credit_admin_indi_has_credit(credit_admin,alice),
inference(clausify,[status(thm)],[ax73]) ).
cnf(c_125,plain,
( admin_indi_has_credit(admin,A)
| ~ credit_admin_indi_has_credit(credit_admin,A) ),
inference(resolve,[status(thm)],[c_122,c_123]) ).
cnf(c_126,plain,
( admin_indi_has_level(admin,alice,B)
| ~ admin_indi_has_background(admin,alice,B)
| ~ loca_level_below(admin,B,D)
| ~ level_admin_indi_has_level(C,alice,D)
| ~ system_indi_is_level_admin(system,C)
| ~ loca_level_below(admin,B,A)
| ~ admin_indi_has_credit(admin,alice)
| ~ admin_indi_has_employment(admin,alice)
| ~ admin_indi_has_citizenship(admin,alice,usa)
| ~ system_indi_needs_level(system,alice,A) ),
inference(resolve,[status(thm)],[c_121,c_120]) ).
cnf(c_127,plain,
admin_indi_has_credit(admin,alice),
inference(resolve,[status(thm)],[c_124,c_125]) ).
cnf(c_128,plain,
( admin_indi_has_credit_for_compartment(admin,E,A)
| ~ admin_indi_has_credit(admin,E)
| ~ oca_compartment_is_compartment(oca,A,B,C,yes,D) ),
inference(resolve,[status(thm)],[c_62,c_58]) ).
cnf(c_129,plain,
admin_indi_has_background(admin,A,unclassified),
inference(clausify,[status(thm)],[ax19]) ).
cnf(c_130,plain,
( admin_indi_has_background_for_compartment(admin,F,A)
| ~ admin_indi_has_background(admin,F,C)
| ~ oca_compartment_is_compartment(oca,A,B,C,D,E) ),
inference(resolve,[status(thm)],[c_66,c_58]) ).
cnf(c_131,plain,
( admin_indi_has_level(admin,alice,B)
| ~ admin_indi_has_background(admin,alice,B)
| ~ loca_level_below(admin,B,D)
| ~ level_admin_indi_has_level(C,alice,D)
| ~ system_indi_is_level_admin(system,C)
| ~ loca_level_below(admin,B,A)
| ~ admin_indi_has_employment(admin,alice)
| ~ admin_indi_has_citizenship(admin,alice,usa)
| ~ system_indi_needs_level(system,alice,A) ),
inference(resolve,[status(thm)],[c_126,c_127]) ).
cnf(c_132,plain,
( admin_indi_has_background(admin,B,D)
| ~ loca_level_below(admin,D,C)
| ~ background_admin_indi_has_background(A,B,C)
| ~ system_indi_is_background_admin(system,A) ),
inference(clausify,[status(thm)],[ax20]) ).
fof(ax68,axiom,
system_indi_is_background_admin(system,background_admin),
file('theBenchmark.p',ax68) ).
cnf(c_133,plain,
system_indi_is_background_admin(system,background_admin),
inference(clausify,[status(thm)],[ax68]) ).
cnf(c_134,plain,
( admin_indi_has_background_for_compartment(admin,B,E)
| ~ oca_compartment_is_compartment(oca,E,F,D,V6,V7)
| ~ loca_level_below(admin,D,C)
| ~ background_admin_indi_has_background(A,B,C)
| ~ system_indi_is_background_admin(system,A) ),
inference(resolve,[status(thm)],[c_132,c_130]) ).
cnf(c_135,plain,
( admin_indi_has_level(admin,alice,C)
| ~ loca_level_below(admin,C,F)
| ~ level_admin_indi_has_level(E,alice,F)
| ~ system_indi_is_level_admin(system,E)
| ~ loca_level_below(admin,C,D)
| ~ admin_indi_has_employment(admin,alice)
| ~ admin_indi_has_citizenship(admin,alice,usa)
| ~ system_indi_needs_level(system,alice,D)
| ~ loca_level_below(admin,C,B)
| ~ background_admin_indi_has_background(A,alice,B)
| ~ system_indi_is_background_admin(system,A) ),
inference(resolve,[status(thm)],[c_132,c_131]) ).
fof(ax74,axiom,
background_admin_indi_has_background(background_admin,alice,topsecret),
file('theBenchmark.p',ax74) ).
cnf(c_136,plain,
background_admin_indi_has_background(background_admin,alice,topsecret),
inference(clausify,[status(thm)],[ax74]) ).
cnf(c_137,plain,
( admin_indi_has_background_for_compartment(admin,A,D)
| ~ oca_compartment_is_compartment(oca,D,E,C,F,V6)
| ~ loca_level_below(admin,C,B)
| ~ background_admin_indi_has_background(background_admin,A,B) ),
inference(resolve,[status(thm)],[c_133,c_134]) ).
cnf(c_138,plain,
( admin_indi_has_level(admin,alice,B)
| ~ loca_level_below(admin,B,E)
| ~ level_admin_indi_has_level(D,alice,E)
| ~ system_indi_is_level_admin(system,D)
| ~ loca_level_below(admin,B,C)
| ~ admin_indi_has_employment(admin,alice)
| ~ admin_indi_has_citizenship(admin,alice,usa)
| ~ system_indi_needs_level(system,alice,C)
| ~ loca_level_below(admin,B,A)
| ~ background_admin_indi_has_background(background_admin,alice,A) ),
inference(resolve,[status(thm)],[c_133,c_135]) ).
cnf(c_139,plain,
( admin_indi_has_employment(admin,B)
| ~ hr_admin_indi_has_employment(A,B)
| ~ system_indi_is_hr_admin(system,A) ),
inference(clausify,[status(thm)],[ax21]) ).
fof(ax69,axiom,
system_indi_is_hr_admin(system,hr_admin),
file('theBenchmark.p',ax69) ).
cnf(c_140,plain,
system_indi_is_hr_admin(system,hr_admin),
inference(clausify,[status(thm)],[ax69]) ).
fof(ax75,axiom,
hr_admin_indi_has_employment(hr_admin,alice),
file('theBenchmark.p',ax75) ).
cnf(c_141,plain,
hr_admin_indi_has_employment(hr_admin,alice),
inference(clausify,[status(thm)],[ax75]) ).
cnf(c_142,plain,
( admin_indi_has_employment(admin,A)
| ~ hr_admin_indi_has_employment(hr_admin,A) ),
inference(resolve,[status(thm)],[c_139,c_140]) ).
cnf(c_143,plain,
( admin_indi_has_level(admin,alice,A)
| ~ loca_level_below(admin,A,D)
| ~ level_admin_indi_has_level(C,alice,D)
| ~ system_indi_is_level_admin(system,C)
| ~ loca_level_below(admin,A,B)
| ~ admin_indi_has_employment(admin,alice)
| ~ admin_indi_has_citizenship(admin,alice,usa)
| ~ system_indi_needs_level(system,alice,B)
| ~ loca_level_below(admin,A,topsecret) ),
inference(resolve,[status(thm)],[c_136,c_138]) ).
cnf(c_144,plain,
admin_indi_has_employment(admin,alice),
inference(resolve,[status(thm)],[c_141,c_142]) ).
cnf(c_145,plain,
( admin_indi_has_compartments(admin,A,cons(compartmenta,B))
| ~ admin_indi_has_compartments(admin,A,B)
| ~ admin_indi_has_level_for_compartment(admin,A,compartmenta)
| ~ admin_indi_has_background_for_compartment(admin,A,compartmenta)
| ~ sso_indi_has_compartment(sso_compartmenta,A,compartmenta)
| ~ admin_indi_has_credit_for_compartment(admin,A,compartmenta)
| ~ admin_indi_has_polygraph_for_compartment(admin,A,compartmenta)
| ~ admin_indi_has_citizenship(admin,A,usa)
| ~ admin_indi_has_employment(admin,A)
| ~ system_indi_needs_compartment(system,A,compartmenta) ),
inference(resolve,[status(thm)],[c_57,c_53]) ).
cnf(c_146,plain,
( admin_indi_has_compartments(admin,A,cons(compartmentb,B))
| ~ admin_indi_has_compartments(admin,A,B)
| ~ admin_indi_has_level_for_compartment(admin,A,compartmentb)
| ~ admin_indi_has_background_for_compartment(admin,A,compartmentb)
| ~ sso_indi_has_compartment(sso_compartmentb,A,compartmentb)
| ~ admin_indi_has_credit_for_compartment(admin,A,compartmentb)
| ~ admin_indi_has_polygraph_for_compartment(admin,A,compartmentb)
| ~ admin_indi_has_citizenship(admin,A,usa)
| ~ admin_indi_has_employment(admin,A)
| ~ system_indi_needs_compartment(system,A,compartmentb) ),
inference(resolve,[status(thm)],[c_57,c_52]) ).
cnf(c_148,plain,
( admin_indi_has_level(admin,alice,A)
| ~ loca_level_below(admin,A,D)
| ~ level_admin_indi_has_level(C,alice,D)
| ~ system_indi_is_level_admin(system,C)
| ~ loca_level_below(admin,A,B)
| ~ admin_indi_has_citizenship(admin,alice,usa)
| ~ system_indi_needs_level(system,alice,B)
| ~ loca_level_below(admin,A,topsecret) ),
inference(resolve,[status(thm)],[c_143,c_144]) ).
cnf(c_149,plain,
( admin_indi_has_compartments(admin,alice,cons(compartmenta,A))
| ~ admin_indi_has_compartments(admin,alice,A)
| ~ admin_indi_has_level_for_compartment(admin,alice,compartmenta)
| ~ admin_indi_has_background_for_compartment(admin,alice,compartmenta)
| ~ sso_indi_has_compartment(sso_compartmenta,alice,compartmenta)
| ~ admin_indi_has_credit_for_compartment(admin,alice,compartmenta)
| ~ admin_indi_has_polygraph_for_compartment(admin,alice,compartmenta)
| ~ admin_indi_has_citizenship(admin,alice,usa)
| ~ system_indi_needs_compartment(system,alice,compartmenta) ),
inference(resolve,[status(thm)],[c_145,c_144]) ).
cnf(c_150,plain,
( admin_indi_has_compartments(admin,alice,cons(compartmentb,A))
| ~ admin_indi_has_compartments(admin,alice,A)
| ~ admin_indi_has_level_for_compartment(admin,alice,compartmentb)
| ~ admin_indi_has_background_for_compartment(admin,alice,compartmentb)
| ~ sso_indi_has_compartment(sso_compartmentb,alice,compartmentb)
| ~ admin_indi_has_credit_for_compartment(admin,alice,compartmentb)
| ~ admin_indi_has_polygraph_for_compartment(admin,alice,compartmentb)
| ~ admin_indi_has_citizenship(admin,alice,usa)
| ~ system_indi_needs_compartment(system,alice,compartmentb) ),
inference(resolve,[status(thm)],[c_146,c_144]) ).
cnf(c_151,plain,
( admin_indi_has_citizenship(admin,A,B)
| ~ system_indi_has_citizenship(system,A,B) ),
inference(clausify,[status(thm)],[ax23]) ).
cnf(c_152,plain,
( admin_indi_has_citizenship_for_file(admin,A,B)
| ~ admin_indi_has_citizenship(admin,A,usa) ),
inference(clausify,[status(thm)],[ax38]) ).
cnf(c_155,plain,
( admin_indi_has_level(admin,alice,A)
| ~ loca_level_below(admin,A,D)
| ~ level_admin_indi_has_level(C,alice,D)
| ~ system_indi_is_level_admin(system,C)
| ~ loca_level_below(admin,A,B)
| ~ system_indi_needs_level(system,alice,B)
| ~ loca_level_below(admin,A,topsecret)
| ~ system_indi_has_citizenship(system,alice,usa) ),
inference(resolve,[status(thm)],[c_151,c_148]) ).
cnf(c_156,plain,
( admin_indi_has_compartments(admin,alice,cons(compartmenta,A))
| ~ admin_indi_has_compartments(admin,alice,A)
| ~ admin_indi_has_level_for_compartment(admin,alice,compartmenta)
| ~ admin_indi_has_background_for_compartment(admin,alice,compartmenta)
| ~ sso_indi_has_compartment(sso_compartmenta,alice,compartmenta)
| ~ admin_indi_has_credit_for_compartment(admin,alice,compartmenta)
| ~ admin_indi_has_polygraph_for_compartment(admin,alice,compartmenta)
| ~ system_indi_needs_compartment(system,alice,compartmenta)
| ~ system_indi_has_citizenship(system,alice,usa) ),
inference(resolve,[status(thm)],[c_151,c_149]) ).
cnf(c_157,plain,
( admin_indi_has_compartments(admin,alice,cons(compartmentb,A))
| ~ admin_indi_has_compartments(admin,alice,A)
| ~ admin_indi_has_level_for_compartment(admin,alice,compartmentb)
| ~ admin_indi_has_background_for_compartment(admin,alice,compartmentb)
| ~ sso_indi_has_compartment(sso_compartmentb,alice,compartmentb)
| ~ admin_indi_has_credit_for_compartment(admin,alice,compartmentb)
| ~ admin_indi_has_polygraph_for_compartment(admin,alice,compartmentb)
| ~ system_indi_needs_compartment(system,alice,compartmentb)
| ~ system_indi_has_citizenship(system,alice,usa) ),
inference(resolve,[status(thm)],[c_151,c_150]) ).
cnf(c_158,plain,
( ~ system_indi_has_citizenship(system,A,usa)
| admin_indi_has_citizenship_for_file(admin,A,B) ),
inference(resolve,[status(thm)],[c_152,c_151]) ).
fof(ax71,axiom,
system_indi_has_citizenship(system,alice,usa),
file('theBenchmark.p',ax71) ).
cnf(c_160,plain,
system_indi_has_citizenship(system,alice,usa),
inference(clausify,[status(thm)],[ax71]) ).
cnf(c_162,plain,
( admin_indi_has_level(admin,alice,A)
| ~ loca_level_below(admin,A,D)
| ~ level_admin_indi_has_level(C,alice,D)
| ~ system_indi_is_level_admin(system,C)
| ~ loca_level_below(admin,A,B)
| ~ system_indi_needs_level(system,alice,B)
| ~ loca_level_below(admin,A,topsecret) ),
inference(resolve,[status(thm)],[c_160,c_155]) ).
cnf(c_163,plain,
( ~ admin_file_has_compartments_h(admin,secretfile,cons(compartmentb,cons(compartmenta,nil)),cons(compartmentb,cons(compartmenta,nil)))
| ~ admin_file_has_level_h(admin,secretfile,secret,cons(compartmentb,cons(compartmenta,nil)))
| admin_indi_has_level_for_file(admin,A,secretfile)
| ~ admin_indi_has_level(admin,A,secret) ),
inference(resolve,[status(thm)],[c_97,c_98]) ).
cnf(c_164,plain,
( admin_indi_has_level_for_compartment(admin,F,A)
| ~ admin_indi_has_level(admin,F,B)
| ~ oca_compartment_is_compartment(oca,A,B,C,D,E) ),
inference(resolve,[status(thm)],[c_65,c_58]) ).
fof(ax76,axiom,
system_indi_needs_level(system,alice,secret),
file('theBenchmark.p',ax76) ).
cnf(c_166,plain,
system_indi_needs_level(system,alice,secret),
inference(clausify,[status(thm)],[ax76]) ).
cnf(c_168,plain,
( ~ loca_level_below(admin,secret,C)
| ~ level_admin_indi_has_level(B,alice,C)
| ~ system_indi_is_level_admin(system,B)
| ~ loca_level_below(admin,secret,A)
| ~ system_indi_needs_level(system,alice,A)
| ~ loca_level_below(admin,secret,topsecret)
| ~ admin_file_has_compartments_h(admin,secretfile,cons(compartmentb,cons(compartmenta,nil)),cons(compartmentb,cons(compartmenta,nil)))
| ~ admin_file_has_level_h(admin,secretfile,secret,cons(compartmentb,cons(compartmenta,nil)))
| admin_indi_has_level_for_file(admin,alice,secretfile) ),
inference(resolve,[status(thm)],[c_163,c_162]) ).
cnf(c_169,plain,
( ~ loca_level_below(admin,B,V7)
| ~ level_admin_indi_has_level(V6,alice,V7)
| ~ system_indi_is_level_admin(system,V6)
| ~ loca_level_below(admin,B,F)
| ~ system_indi_needs_level(system,alice,F)
| ~ loca_level_below(admin,B,topsecret)
| admin_indi_has_level_for_compartment(admin,alice,A)
| ~ oca_compartment_is_compartment(oca,A,B,C,D,E) ),
inference(resolve,[status(thm)],[c_164,c_162]) ).
fof(ax70,axiom,
system_indi_is_level_admin(system,level_admin),
file('theBenchmark.p',ax70) ).
cnf(c_170,plain,
system_indi_is_level_admin(system,level_admin),
inference(clausify,[status(thm)],[ax70]) ).
cnf(c_172,plain,
( ~ loca_level_below(admin,secret,B)
| ~ level_admin_indi_has_level(A,alice,B)
| ~ system_indi_is_level_admin(system,A)
| ~ loca_level_below(admin,secret,secret)
| ~ loca_level_below(admin,secret,topsecret)
| ~ admin_file_has_compartments_h(admin,secretfile,cons(compartmentb,cons(compartmenta,nil)),cons(compartmentb,cons(compartmenta,nil)))
| ~ admin_file_has_level_h(admin,secretfile,secret,cons(compartmentb,cons(compartmenta,nil)))
| admin_indi_has_level_for_file(admin,alice,secretfile) ),
inference(resolve,[status(thm)],[c_166,c_168]) ).
cnf(c_173,plain,
( ~ loca_level_below(admin,B,V6)
| ~ level_admin_indi_has_level(F,alice,V6)
| ~ system_indi_is_level_admin(system,F)
| ~ loca_level_below(admin,B,secret)
| ~ loca_level_below(admin,B,topsecret)
| admin_indi_has_level_for_compartment(admin,alice,A)
| ~ oca_compartment_is_compartment(oca,A,B,C,D,E) ),
inference(resolve,[status(thm)],[c_166,c_169]) ).
fof(ax77,axiom,
level_admin_indi_has_level(level_admin,alice,topsecret),
file('theBenchmark.p',ax77) ).
cnf(c_174,plain,
level_admin_indi_has_level(level_admin,alice,topsecret),
inference(clausify,[status(thm)],[ax77]) ).
cnf(c_175,plain,
( ~ loca_level_below(admin,secret,A)
| ~ level_admin_indi_has_level(level_admin,alice,A)
| ~ loca_level_below(admin,secret,secret)
| ~ loca_level_below(admin,secret,topsecret)
| ~ admin_file_has_compartments_h(admin,secretfile,cons(compartmentb,cons(compartmenta,nil)),cons(compartmentb,cons(compartmenta,nil)))
| ~ admin_file_has_level_h(admin,secretfile,secret,cons(compartmentb,cons(compartmenta,nil)))
| admin_indi_has_level_for_file(admin,alice,secretfile) ),
inference(resolve,[status(thm)],[c_170,c_172]) ).
cnf(c_176,plain,
( ~ loca_level_below(admin,B,F)
| ~ level_admin_indi_has_level(level_admin,alice,F)
| ~ loca_level_below(admin,B,secret)
| ~ loca_level_below(admin,B,topsecret)
| admin_indi_has_level_for_compartment(admin,alice,A)
| ~ oca_compartment_is_compartment(oca,A,B,C,D,E) ),
inference(resolve,[status(thm)],[c_170,c_173]) ).
fof(ax78,axiom,
system_indi_needs_compartment(system,alice,compartmentb),
file('theBenchmark.p',ax78) ).
cnf(c_177,plain,
system_indi_needs_compartment(system,alice,compartmentb),
inference(clausify,[status(thm)],[ax78]) ).
cnf(c_178,plain,
( admin_indi_has_compartments(admin,alice,cons(compartmenta,A))
| ~ admin_indi_has_compartments(admin,alice,A)
| ~ admin_indi_has_level_for_compartment(admin,alice,compartmenta)
| ~ admin_indi_has_background_for_compartment(admin,alice,compartmenta)
| ~ sso_indi_has_compartment(sso_compartmenta,alice,compartmenta)
| ~ admin_indi_has_credit_for_compartment(admin,alice,compartmenta)
| ~ admin_indi_has_polygraph_for_compartment(admin,alice,compartmenta)
| ~ system_indi_needs_compartment(system,alice,compartmenta) ),
inference(resolve,[status(thm)],[c_160,c_156]) ).
cnf(c_179,plain,
( admin_indi_has_compartments(admin,alice,cons(compartmentb,A))
| ~ admin_indi_has_compartments(admin,alice,A)
| ~ admin_indi_has_level_for_compartment(admin,alice,compartmentb)
| ~ admin_indi_has_background_for_compartment(admin,alice,compartmentb)
| ~ sso_indi_has_compartment(sso_compartmentb,alice,compartmentb)
| ~ admin_indi_has_credit_for_compartment(admin,alice,compartmentb)
| ~ admin_indi_has_polygraph_for_compartment(admin,alice,compartmentb)
| ~ system_indi_needs_compartment(system,alice,compartmentb) ),
inference(resolve,[status(thm)],[c_160,c_157]) ).
fof(ax79,axiom,
system_indi_needs_compartment(system,alice,compartmenta),
file('theBenchmark.p',ax79) ).
cnf(c_180,plain,
system_indi_needs_compartment(system,alice,compartmenta),
inference(clausify,[status(thm)],[ax79]) ).
cnf(c_181,plain,
( admin_indi_has_polygraph_for_compartment(admin,alice,A)
| ~ oca_compartment_is_compartment(oca,A,B,C,D,yes) ),
inference(resolve,[status(thm)],[c_119,c_120]) ).
cnf(c_182,plain,
( admin_indi_has_compartments(admin,alice,cons(compartmentb,A))
| ~ admin_indi_has_compartments(admin,alice,A)
| ~ admin_indi_has_level_for_compartment(admin,alice,compartmentb)
| ~ admin_indi_has_background_for_compartment(admin,alice,compartmentb)
| ~ sso_indi_has_compartment(sso_compartmentb,alice,compartmentb)
| ~ admin_indi_has_credit_for_compartment(admin,alice,compartmentb)
| ~ admin_indi_has_polygraph_for_compartment(admin,alice,compartmentb) ),
inference(resolve,[status(thm)],[c_177,c_179]) ).
cnf(c_183,plain,
( admin_indi_has_compartments(admin,alice,cons(compartmenta,A))
| ~ admin_indi_has_compartments(admin,alice,A)
| ~ admin_indi_has_level_for_compartment(admin,alice,compartmenta)
| ~ admin_indi_has_background_for_compartment(admin,alice,compartmenta)
| ~ sso_indi_has_compartment(sso_compartmenta,alice,compartmenta)
| ~ admin_indi_has_credit_for_compartment(admin,alice,compartmenta)
| ~ admin_indi_has_polygraph_for_compartment(admin,alice,compartmenta) ),
inference(resolve,[status(thm)],[c_180,c_178]) ).
cnf(c_184,plain,
( admin_indi_has_polygraph_for_compartment(admin,E,A)
| ~ oca_compartment_is_compartment(oca,A,B,C,D,no) ),
inference(resolve,[status(thm)],[c_63,c_58]) ).
cnf(c_185,plain,
( admin_indi_has_credit_for_compartment(admin,alice,A)
| ~ oca_compartment_is_compartment(oca,A,B,C,yes,D) ),
inference(resolve,[status(thm)],[c_128,c_127]) ).
cnf(c_186,plain,
( admin_indi_has_compartments(admin,alice,cons(compartmentb,D))
| ~ admin_indi_has_compartments(admin,alice,D)
| ~ admin_indi_has_level_for_compartment(admin,alice,compartmentb)
| ~ admin_indi_has_background_for_compartment(admin,alice,compartmentb)
| ~ sso_indi_has_compartment(sso_compartmentb,alice,compartmentb)
| ~ admin_indi_has_credit_for_compartment(admin,alice,compartmentb)
| ~ oca_compartment_is_compartment(oca,compartmentb,A,B,C,yes) ),
inference(resolve,[status(thm)],[c_181,c_182]) ).
cnf(c_189,plain,
( admin_indi_has_compartments(admin,alice,cons(compartmenta,D))
| ~ admin_indi_has_compartments(admin,alice,D)
| ~ admin_indi_has_level_for_compartment(admin,alice,compartmenta)
| ~ admin_indi_has_background_for_compartment(admin,alice,compartmenta)
| ~ sso_indi_has_compartment(sso_compartmenta,alice,compartmenta)
| ~ admin_indi_has_credit_for_compartment(admin,alice,compartmenta)
| ~ oca_compartment_is_compartment(oca,compartmenta,A,B,C,no) ),
inference(resolve,[status(thm)],[c_184,c_183]) ).
cnf(c_190,plain,
( admin_indi_has_credit_for_compartment(admin,E,A)
| ~ oca_compartment_is_compartment(oca,A,B,C,no,D) ),
inference(resolve,[status(thm)],[c_61,c_58]) ).
fof(ax81,axiom,
sso_indi_has_compartment(sso_compartmenta,alice,compartmenta),
file('theBenchmark.p',ax81) ).
cnf(c_191,plain,
sso_indi_has_compartment(sso_compartmenta,alice,compartmenta),
inference(clausify,[status(thm)],[ax81]) ).
cnf(c_192,plain,
( admin_indi_has_compartments(admin,alice,cons(compartmentb,V6))
| ~ admin_indi_has_compartments(admin,alice,V6)
| ~ admin_indi_has_level_for_compartment(admin,alice,compartmentb)
| ~ admin_indi_has_background_for_compartment(admin,alice,compartmentb)
| ~ sso_indi_has_compartment(sso_compartmentb,alice,compartmentb)
| ~ oca_compartment_is_compartment(oca,compartmentb,D,E,F,yes)
| ~ oca_compartment_is_compartment(oca,compartmentb,A,B,yes,C) ),
inference(resolve,[status(thm)],[c_185,c_186]) ).
cnf(c_199,plain,
( admin_indi_has_compartments(admin,alice,cons(compartmenta,V6))
| ~ admin_indi_has_compartments(admin,alice,V6)
| ~ admin_indi_has_level_for_compartment(admin,alice,compartmenta)
| ~ admin_indi_has_background_for_compartment(admin,alice,compartmenta)
| ~ sso_indi_has_compartment(sso_compartmenta,alice,compartmenta)
| ~ oca_compartment_is_compartment(oca,compartmenta,D,E,F,no)
| ~ oca_compartment_is_compartment(oca,compartmenta,A,B,no,C) ),
inference(resolve,[status(thm)],[c_190,c_189]) ).
fof(ax80,axiom,
sso_indi_has_compartment(sso_compartmentb,alice,compartmentb),
file('theBenchmark.p',ax80) ).
cnf(c_200,plain,
sso_indi_has_compartment(sso_compartmentb,alice,compartmentb),
inference(clausify,[status(thm)],[ax80]) ).
cnf(c_201,plain,
( admin_indi_has_background_for_compartment(admin,E,A)
| ~ oca_compartment_is_compartment(oca,A,B,unclassified,C,D) ),
inference(resolve,[status(thm)],[c_129,c_130]) ).
cnf(c_205,plain,
( admin_indi_has_compartments(admin,alice,cons(compartmenta,V6))
| ~ admin_indi_has_compartments(admin,alice,V6)
| ~ admin_indi_has_level_for_compartment(admin,alice,compartmenta)
| ~ admin_indi_has_background_for_compartment(admin,alice,compartmenta)
| ~ oca_compartment_is_compartment(oca,compartmenta,D,E,F,no)
| ~ oca_compartment_is_compartment(oca,compartmenta,A,B,no,C) ),
inference(resolve,[status(thm)],[c_191,c_199]) ).
cnf(c_206,plain,
( admin_indi_has_compartments(admin,alice,cons(compartmentb,V6))
| ~ admin_indi_has_compartments(admin,alice,V6)
| ~ admin_indi_has_level_for_compartment(admin,alice,compartmentb)
| ~ admin_indi_has_background_for_compartment(admin,alice,compartmentb)
| ~ oca_compartment_is_compartment(oca,compartmentb,D,E,F,yes)
| ~ oca_compartment_is_compartment(oca,compartmentb,A,B,yes,C) ),
inference(resolve,[status(thm)],[c_200,c_192]) ).
cnf(c_210,plain,
( admin_indi_has_background_for_compartment(admin,alice,B)
| ~ oca_compartment_is_compartment(oca,B,C,A,D,E)
| ~ loca_level_below(admin,A,topsecret) ),
inference(resolve,[status(thm)],[c_136,c_137]) ).
cnf(c_215,plain,
( admin_indi_has_compartments(admin,alice,cons(compartmenta,V9))
| ~ admin_indi_has_compartments(admin,alice,V9)
| ~ admin_indi_has_level_for_compartment(admin,alice,compartmenta)
| ~ oca_compartment_is_compartment(oca,compartmenta,V6,V7,V8,no)
| ~ oca_compartment_is_compartment(oca,compartmenta,D,E,no,F)
| ~ oca_compartment_is_compartment(oca,compartmenta,A,unclassified,B,C) ),
inference(resolve,[status(thm)],[c_201,c_205]) ).
cnf(c_224,plain,
( admin_indi_has_compartments(admin,alice,cons(compartmentb,V10))
| ~ admin_indi_has_compartments(admin,alice,V10)
| ~ admin_indi_has_level_for_compartment(admin,alice,compartmentb)
| ~ oca_compartment_is_compartment(oca,compartmentb,V7,V8,V9,yes)
| ~ oca_compartment_is_compartment(oca,compartmentb,E,F,yes,V6)
| ~ oca_compartment_is_compartment(oca,compartmentb,B,A,C,D)
| ~ loca_level_below(admin,A,topsecret) ),
inference(resolve,[status(thm)],[c_210,c_206]) ).
cnf(c_228,plain,
( ~ loca_level_below(admin,B,topsecret)
| ~ loca_level_below(admin,B,secret)
| ~ loca_level_below(admin,B,topsecret)
| admin_indi_has_level_for_compartment(admin,alice,A)
| ~ oca_compartment_is_compartment(oca,A,B,C,D,E) ),
inference(resolve,[status(thm)],[c_174,c_176]) ).
cnf(c_229,plain,
( ~ admin_file_has_compartments_h(admin,secretfile,cons(compartmentb,cons(compartmenta,nil)),cons(compartmentb,cons(compartmenta,nil)))
| admin_indi_has_compartments_for_file(admin,A,secretfile)
| ~ admin_indi_has_compartments(admin,A,cons(compartmentb,cons(compartmenta,nil))) ),
inference(resolve,[status(thm)],[c_88,c_85]) ).
cnf(c_230,plain,
( admin_indi_may_file(admin,B,A,read)
| ~ admin_indi_has_compartments_for_file(admin,B,A)
| ~ admin_indi_has_level_for_file(admin,B,A)
| ~ admin_indi_has_need_to_know_for_file(admin,B,A)
| ~ admin_indi_has_citizenship_for_file(admin,B,A)
| ~ state_file_is_not_working_paper(A) ),
inference(clausify,[status(thm)],[ax39]) ).
cnf(c_233,plain,
( admin_indi_may_file(admin,A,secretfile,read)
| ~ admin_indi_has_level_for_file(admin,A,secretfile)
| ~ admin_indi_has_need_to_know_for_file(admin,A,secretfile)
| ~ admin_indi_has_citizenship_for_file(admin,A,secretfile)
| ~ state_file_is_not_working_paper(secretfile)
| ~ admin_file_has_compartments_h(admin,secretfile,cons(compartmentb,cons(compartmenta,nil)),cons(compartmentb,cons(compartmenta,nil)))
| ~ admin_indi_has_compartments(admin,A,cons(compartmentb,cons(compartmenta,nil))) ),
inference(resolve,[status(thm)],[c_229,c_230]) ).
cnf(c_235,plain,
( ~ loca_level_below(admin,secret,topsecret)
| ~ loca_level_below(admin,secret,secret)
| ~ loca_level_below(admin,secret,topsecret)
| ~ admin_file_has_compartments_h(admin,secretfile,cons(compartmentb,cons(compartmenta,nil)),cons(compartmentb,cons(compartmenta,nil)))
| ~ admin_file_has_level_h(admin,secretfile,secret,cons(compartmentb,cons(compartmenta,nil)))
| admin_indi_has_level_for_file(admin,alice,secretfile) ),
inference(resolve,[status(thm)],[c_174,c_175]) ).
fof(ax60,axiom,
state_file_has_owner(secretfile,owner_secretfile),
file('theBenchmark.p',ax60) ).
cnf(c_236,plain,
state_file_has_owner(secretfile,owner_secretfile),
inference(clausify,[status(thm)],[ax60]) ).
cnf(c_238,plain,
( admin_indi_has_need_to_know_for_file(admin,C,A)
| ~ owner_indi_has_need_to_know(B,C,A)
| ~ state_file_has_owner(A,B) ),
inference(clausify,[status(thm)],[ax36]) ).
cnf(c_241,plain,
( admin_indi_has_need_to_know_for_file(admin,A,secretfile)
| ~ owner_indi_has_need_to_know(owner_secretfile,A,secretfile) ),
inference(resolve,[status(thm)],[c_236,c_238]) ).
fof(ax82,axiom,
owner_indi_has_need_to_know(owner_secretfile,alice,secretfile),
file('theBenchmark.p',ax82) ).
cnf(c_244,plain,
owner_indi_has_need_to_know(owner_secretfile,alice,secretfile),
inference(clausify,[status(thm)],[ax82]) ).
cnf(c_245,plain,
( admin_indi_may_file(admin,alice,secretfile,read)
| ~ admin_indi_has_need_to_know_for_file(admin,alice,secretfile)
| ~ admin_indi_has_citizenship_for_file(admin,alice,secretfile)
| ~ state_file_is_not_working_paper(secretfile)
| ~ admin_file_has_compartments_h(admin,secretfile,cons(compartmentb,cons(compartmenta,nil)),cons(compartmentb,cons(compartmenta,nil)))
| ~ admin_indi_has_compartments(admin,alice,cons(compartmentb,cons(compartmenta,nil)))
| ~ loca_level_below(admin,secret,topsecret)
| ~ loca_level_below(admin,secret,secret)
| ~ loca_level_below(admin,secret,topsecret)
| ~ admin_file_has_compartments_h(admin,secretfile,cons(compartmentb,cons(compartmenta,nil)),cons(compartmentb,cons(compartmenta,nil)))
| ~ admin_file_has_level_h(admin,secretfile,secret,cons(compartmentb,cons(compartmenta,nil))) ),
inference(resolve,[status(thm)],[c_235,c_233]) ).
cnf(c_247,plain,
admin_indi_has_need_to_know_for_file(admin,alice,secretfile),
inference(resolve,[status(thm)],[c_244,c_241]) ).
cnf(c_250,plain,
( admin_indi_may_file(admin,alice,secretfile,read)
| ~ admin_indi_has_citizenship_for_file(admin,alice,secretfile)
| ~ state_file_is_not_working_paper(secretfile)
| ~ admin_file_has_compartments_h(admin,secretfile,cons(compartmentb,cons(compartmenta,nil)),cons(compartmentb,cons(compartmenta,nil)))
| ~ admin_indi_has_compartments(admin,alice,cons(compartmentb,cons(compartmenta,nil)))
| ~ loca_level_below(admin,secret,topsecret)
| ~ loca_level_below(admin,secret,secret)
| ~ loca_level_below(admin,secret,topsecret)
| ~ admin_file_has_compartments_h(admin,secretfile,cons(compartmentb,cons(compartmenta,nil)),cons(compartmentb,cons(compartmenta,nil)))
| ~ admin_file_has_level_h(admin,secretfile,secret,cons(compartmentb,cons(compartmenta,nil))) ),
inference(resolve,[status(thm)],[c_245,c_247]) ).
cnf(c_252,plain,
admin_indi_has_citizenship_for_file(admin,alice,A),
inference(resolve,[status(thm)],[c_160,c_158]) ).
fof(ax50,axiom,
state_file_is_not_working_paper(secretfile),
file('theBenchmark.p',ax50) ).
cnf(c_253,plain,
state_file_is_not_working_paper(secretfile),
inference(clausify,[status(thm)],[ax50]) ).
cnf(c_255,plain,
( admin_indi_may_file(admin,alice,secretfile,read)
| ~ state_file_is_not_working_paper(secretfile)
| ~ admin_file_has_compartments_h(admin,secretfile,cons(compartmentb,cons(compartmenta,nil)),cons(compartmentb,cons(compartmenta,nil)))
| ~ admin_indi_has_compartments(admin,alice,cons(compartmentb,cons(compartmenta,nil)))
| ~ loca_level_below(admin,secret,topsecret)
| ~ loca_level_below(admin,secret,secret)
| ~ loca_level_below(admin,secret,topsecret)
| ~ admin_file_has_compartments_h(admin,secretfile,cons(compartmentb,cons(compartmenta,nil)),cons(compartmentb,cons(compartmenta,nil)))
| ~ admin_file_has_level_h(admin,secretfile,secret,cons(compartmentb,cons(compartmenta,nil))) ),
inference(resolve,[status(thm)],[c_252,c_250]) ).
cnf(c_257,negated_conjecture,
~ admin_indi_may_file(admin,alice,secretfile,read),
inference(clausify,[status(thm)],[alicereadsecret_neg]) ).
cnf(c_260,plain,
( admin_indi_may_file(admin,alice,secretfile,read)
| ~ admin_file_has_compartments_h(admin,secretfile,cons(compartmentb,cons(compartmenta,nil)),cons(compartmentb,cons(compartmenta,nil)))
| ~ admin_indi_has_compartments(admin,alice,cons(compartmentb,cons(compartmenta,nil)))
| ~ loca_level_below(admin,secret,topsecret)
| ~ loca_level_below(admin,secret,secret)
| ~ loca_level_below(admin,secret,topsecret)
| ~ admin_file_has_compartments_h(admin,secretfile,cons(compartmentb,cons(compartmenta,nil)),cons(compartmentb,cons(compartmenta,nil)))
| ~ admin_file_has_level_h(admin,secretfile,secret,cons(compartmentb,cons(compartmenta,nil))) ),
inference(resolve,[status(thm)],[c_253,c_255]) ).
cnf(c_264,plain,
( admin_file_has_level_h(admin,secretfile,secret,cons(compartmenta,A))
| ~ admin_file_has_level_h(admin,secretfile,secret,A) ),
inference(resolve,[status(thm)],[c_103,c_101]) ).
cnf(c_265,plain,
( admin_file_has_level_h(admin,secretfile,secret,cons(compartmentb,A))
| ~ admin_file_has_level_h(admin,secretfile,secret,A) ),
inference(resolve,[status(thm)],[c_100,c_102]) ).
cnf(c_267,plain,
( loca_level_below(A,B,confidential)
| ~ loca_level_below(A,B,sbu) ),
inference(resolve,[status(thm)],[c_43,c_46]) ).
cnf(c_268,plain,
( loca_level_below(A,B,secret)
| ~ loca_level_below(A,B,confidential) ),
inference(resolve,[status(thm)],[c_43,c_45]) ).
cnf(c_269,plain,
( loca_level_below(A,B,topsecret)
| ~ loca_level_below(A,B,secret) ),
inference(resolve,[status(thm)],[c_43,c_44]) ).
fof(ax43,axiom,
oca_compartment_is_compartment(oca,compartmenta,sbu,unclassified,no,no),
file('theBenchmark.p',ax43) ).
cnf(c_270,plain,
oca_compartment_is_compartment(oca,compartmenta,sbu,unclassified,no,no),
inference(clausify,[status(thm)],[ax43]) ).
fof(ax42,axiom,
oca_compartment_is_compartment(oca,compartmentb,confidential,topsecret,yes,yes),
file('theBenchmark.p',ax42) ).
cnf(c_271,plain,
oca_compartment_is_compartment(oca,compartmentb,confidential,topsecret,yes,yes),
inference(clausify,[status(thm)],[ax42]) ).
cnf(c_272,plain,
admin_indi_has_compartments(admin,A,nil),
inference(clausify,[status(thm)],[ax26]) ).
cnf(c_274,plain,
admin_file_has_level_h(admin,A,B,nil),
inference(clausify,[status(thm)],[ax12]) ).
cnf(c_275,plain,
admin_file_has_compartments_h(admin,A,B,nil),
inference(clausify,[status(thm)],[ax9]) ).
cnf(c_276,plain,
loca_level_below(A,B,B),
inference(clausify,[status(thm)],[ax4]) ).
cnf(c_277,plain,
( admin_file_has_compartments_h(admin,secretfile,cons(compartmentb,cons(compartmenta,nil)),cons(compartmenta,A))
| ~ admin_file_has_compartments_h(admin,secretfile,cons(compartmentb,cons(compartmenta,nil)),A) ),
inference(resolve,[status(thm)],[c_89,c_91]) ).
cnf(c_278,plain,
( admin_file_has_compartments_h(admin,secretfile,cons(compartmentb,cons(compartmenta,nil)),cons(compartmentb,A))
| ~ admin_file_has_compartments_h(admin,secretfile,cons(compartmentb,cons(compartmenta,nil)),A) ),
inference(resolve,[status(thm)],[c_92,c_90]) ).
cnf(c_303,plain,
( admin_indi_has_compartments(admin,alice,cons(compartmenta,V13))
| ~ admin_indi_has_compartments(admin,alice,V13)
| ~ oca_compartment_is_compartment(oca,compartmenta,V10,V11,V12,no)
| ~ oca_compartment_is_compartment(oca,compartmenta,V7,V8,no,V9)
| ~ oca_compartment_is_compartment(oca,compartmenta,E,unclassified,F,V6)
| ~ loca_level_below(admin,A,topsecret)
| ~ loca_level_below(admin,A,secret)
| ~ loca_level_below(admin,A,topsecret)
| ~ oca_compartment_is_compartment(oca,compartmenta,A,B,C,D) ),
inference(resolve,[status(thm)],[c_228,c_215]) ).
cnf(c_304,plain,
( admin_indi_has_compartments(admin,alice,cons(compartmenta,V13))
| ~ admin_indi_has_compartments(admin,alice,V13)
| ~ oca_compartment_is_compartment(oca,compartmenta,V10,V11,V12,no)
| ~ oca_compartment_is_compartment(oca,compartmenta,V7,V8,no,V9)
| ~ oca_compartment_is_compartment(oca,compartmenta,E,unclassified,F,V6)
| ~ loca_level_below(admin,A,secret)
| ~ loca_level_below(admin,A,topsecret)
| ~ oca_compartment_is_compartment(oca,compartmenta,A,B,C,D) ),
inference(copy,[status(thm)],[c_303]) ).
cnf(c_321,plain,
( admin_indi_has_compartments(admin,alice,cons(compartmentb,V14))
| ~ admin_indi_has_compartments(admin,alice,V14)
| ~ oca_compartment_is_compartment(oca,compartmentb,V11,V12,V13,yes)
| ~ oca_compartment_is_compartment(oca,compartmentb,V8,V9,yes,V10)
| ~ oca_compartment_is_compartment(oca,compartmentb,F,E,V6,V7)
| ~ loca_level_below(admin,E,topsecret)
| ~ loca_level_below(admin,A,topsecret)
| ~ loca_level_below(admin,A,secret)
| ~ loca_level_below(admin,A,topsecret)
| ~ oca_compartment_is_compartment(oca,compartmentb,A,B,C,D) ),
inference(resolve,[status(thm)],[c_228,c_224]) ).
cnf(c_322,plain,
( admin_indi_has_compartments(admin,alice,cons(compartmentb,V14))
| ~ admin_indi_has_compartments(admin,alice,V14)
| ~ oca_compartment_is_compartment(oca,compartmentb,V11,V12,V13,yes)
| ~ oca_compartment_is_compartment(oca,compartmentb,V8,V9,yes,V10)
| ~ oca_compartment_is_compartment(oca,compartmentb,F,E,V6,V7)
| ~ loca_level_below(admin,E,topsecret)
| ~ loca_level_below(admin,A,secret)
| ~ loca_level_below(admin,A,topsecret)
| ~ oca_compartment_is_compartment(oca,compartmentb,A,B,C,D) ),
inference(copy,[status(thm)],[c_321]) ).
cnf(c_329,negated_conjecture,
( ~ admin_file_has_compartments_h(admin,secretfile,cons(compartmentb,cons(compartmenta,nil)),cons(compartmentb,cons(compartmenta,nil)))
| ~ admin_indi_has_compartments(admin,alice,cons(compartmentb,cons(compartmenta,nil)))
| ~ loca_level_below(admin,secret,topsecret)
| ~ loca_level_below(admin,secret,secret)
| ~ loca_level_below(admin,secret,topsecret)
| ~ admin_file_has_compartments_h(admin,secretfile,cons(compartmentb,cons(compartmenta,nil)),cons(compartmentb,cons(compartmenta,nil)))
| ~ admin_file_has_level_h(admin,secretfile,secret,cons(compartmentb,cons(compartmenta,nil))) ),
inference(resolve,[status(thm)],[c_257,c_260]) ).
cnf(c_445,negated_conjecture,
( ~ admin_file_has_compartments_h(admin,secretfile,cons(compartmentb,cons(compartmenta,nil)),cons(compartmentb,cons(compartmenta,nil)))
| ~ admin_indi_has_compartments(admin,alice,cons(compartmentb,cons(compartmenta,nil)))
| ~ loca_level_below(admin,secret,secret)
| ~ loca_level_below(admin,secret,topsecret)
| ~ admin_file_has_compartments_h(admin,secretfile,cons(compartmentb,cons(compartmenta,nil)),cons(compartmentb,cons(compartmenta,nil)))
| ~ admin_file_has_level_h(admin,secretfile,secret,cons(compartmentb,cons(compartmenta,nil))) ),
inference(copy,[status(thm)],[c_329]) ).
cnf(c_446,negated_conjecture,
( ~ admin_indi_has_compartments(admin,alice,cons(compartmentb,cons(compartmenta,nil)))
| ~ loca_level_below(admin,secret,secret)
| ~ loca_level_below(admin,secret,topsecret)
| ~ admin_file_has_compartments_h(admin,secretfile,cons(compartmentb,cons(compartmenta,nil)),cons(compartmentb,cons(compartmenta,nil)))
| ~ admin_file_has_level_h(admin,secretfile,secret,cons(compartmentb,cons(compartmenta,nil))) ),
inference(copy,[status(thm)],[c_445]) ).
cnf(c_330,negated_conjecture,
( ~ admin_indi_has_compartments(admin,alice,cons(compartmentb,cons(compartmenta,nil)))
| ~ loca_level_below(admin,secret,topsecret)
| ~ admin_file_has_compartments_h(admin,secretfile,cons(compartmentb,cons(compartmenta,nil)),cons(compartmentb,cons(compartmenta,nil)))
| ~ admin_file_has_level_h(admin,secretfile,secret,cons(compartmentb,cons(compartmenta,nil))) ),
inference(resolve,[status(thm)],[c_276,c_446]) ).
cnf(c_332,plain,
admin_file_has_level_h(admin,secretfile,secret,cons(compartmenta,nil)),
inference(resolve,[status(thm)],[c_264,c_274]) ).
cnf(c_333,plain,
loca_level_below(A,secret,topsecret),
inference(resolve,[status(thm)],[c_269,c_276]) ).
cnf(c_334,plain,
loca_level_below(A,confidential,secret),
inference(resolve,[status(thm)],[c_268,c_276]) ).
cnf(c_335,plain,
loca_level_below(A,sbu,confidential),
inference(resolve,[status(thm)],[c_267,c_276]) ).
cnf(c_337,negated_conjecture,
( ~ admin_indi_has_compartments(admin,alice,cons(compartmentb,cons(compartmenta,nil)))
| ~ admin_file_has_compartments_h(admin,secretfile,cons(compartmentb,cons(compartmenta,nil)),cons(compartmentb,cons(compartmenta,nil)))
| ~ admin_file_has_level_h(admin,secretfile,secret,cons(compartmentb,cons(compartmenta,nil))) ),
inference(resolve,[status(thm)],[c_333,c_330]) ).
cnf(c_338,plain,
admin_file_has_compartments_h(admin,secretfile,cons(compartmentb,cons(compartmenta,nil)),cons(compartmenta,nil)),
inference(resolve,[status(thm)],[c_277,c_275]) ).
cnf(c_344,plain,
admin_file_has_level_h(admin,secretfile,secret,cons(compartmentb,cons(compartmenta,nil))),
inference(resolve,[status(thm)],[c_265,c_332]) ).
cnf(c_346,negated_conjecture,
( ~ admin_indi_has_compartments(admin,alice,cons(compartmentb,cons(compartmenta,nil)))
| ~ admin_file_has_compartments_h(admin,secretfile,cons(compartmentb,cons(compartmenta,nil)),cons(compartmentb,cons(compartmenta,nil))) ),
inference(resolve,[status(thm)],[c_344,c_337]) ).
cnf(c_447,negated_conjecture,
( ~ admin_file_has_compartments_h(admin,secretfile,cons(compartmentb,cons(compartmenta,nil)),cons(compartmenta,nil))
| ~ admin_indi_has_compartments(admin,alice,cons(compartmentb,cons(compartmenta,nil))) ),
inference(resolve,[status(thm)],[c_346,c_278]) ).
cnf(c_347,negated_conjecture,
~ admin_indi_has_compartments(admin,alice,cons(compartmentb,cons(compartmenta,nil))),
inference(resolve,[status(thm)],[c_338,c_447]) ).
cnf(c_413,plain,
loca_level_below(A,confidential,topsecret),
inference(resolve,[status(thm)],[c_269,c_334]) ).
cnf(c_414,plain,
loca_level_below(A,sbu,secret),
inference(resolve,[status(thm)],[c_268,c_335]) ).
cnf(c_448,plain,
( admin_indi_has_compartments(admin,alice,cons(compartmentb,V10))
| ~ admin_indi_has_compartments(admin,alice,V10)
| ~ oca_compartment_is_compartment(oca,compartmentb,V7,V8,V9,yes)
| ~ oca_compartment_is_compartment(oca,compartmentb,E,F,yes,V6)
| ~ oca_compartment_is_compartment(oca,compartmentb,B,A,C,D)
| ~ loca_level_below(admin,A,topsecret)
| ~ loca_level_below(admin,confidential,secret)
| ~ loca_level_below(admin,confidential,topsecret) ),
inference(resolve,[status(thm)],[c_322,c_271]) ).
cnf(c_449,plain,
( admin_indi_has_compartments(admin,alice,cons(compartmentb,V10))
| ~ admin_indi_has_compartments(admin,alice,V10)
| ~ oca_compartment_is_compartment(oca,compartmentb,V7,V8,V9,yes)
| ~ oca_compartment_is_compartment(oca,compartmentb,E,F,yes,V6)
| ~ oca_compartment_is_compartment(oca,compartmentb,B,A,C,D)
| ~ loca_level_below(admin,A,topsecret)
| ~ loca_level_below(admin,confidential,secret) ),
inference(resolve,[status(thm)],[c_448,c_413]) ).
cnf(c_450,plain,
( admin_indi_has_compartments(admin,alice,cons(compartmentb,V10))
| ~ admin_indi_has_compartments(admin,alice,V10)
| ~ oca_compartment_is_compartment(oca,compartmentb,V7,V8,V9,yes)
| ~ oca_compartment_is_compartment(oca,compartmentb,E,F,yes,V6)
| ~ oca_compartment_is_compartment(oca,compartmentb,B,A,C,D)
| ~ loca_level_below(admin,A,topsecret) ),
inference(resolve,[status(thm)],[c_449,c_334]) ).
cnf(c_451,plain,
( admin_indi_has_compartments(admin,alice,cons(compartmentb,V9))
| ~ admin_indi_has_compartments(admin,alice,V9)
| ~ oca_compartment_is_compartment(oca,compartmentb,V6,V7,V8,yes)
| ~ oca_compartment_is_compartment(oca,compartmentb,D,E,yes,F)
| ~ oca_compartment_is_compartment(oca,compartmentb,A,topsecret,B,C) ),
inference(resolve,[status(thm)],[c_450,c_276]) ).
cnf(c_452,plain,
( admin_indi_has_compartments(admin,alice,cons(compartmentb,V6))
| ~ admin_indi_has_compartments(admin,alice,V6)
| ~ oca_compartment_is_compartment(oca,compartmentb,D,E,F,yes)
| ~ oca_compartment_is_compartment(oca,compartmentb,A,B,yes,C) ),
inference(resolve,[status(thm)],[c_451,c_271]) ).
cnf(c_453,plain,
( admin_indi_has_compartments(admin,alice,cons(compartmentb,D))
| ~ admin_indi_has_compartments(admin,alice,D)
| ~ oca_compartment_is_compartment(oca,compartmentb,A,B,C,yes) ),
inference(resolve,[status(thm)],[c_452,c_271]) ).
cnf(c_454,plain,
( admin_indi_has_compartments(admin,alice,cons(compartmentb,A))
| ~ admin_indi_has_compartments(admin,alice,A) ),
inference(resolve,[status(thm)],[c_453,c_271]) ).
cnf(c_417,plain,
~ admin_indi_has_compartments(admin,alice,cons(compartmenta,nil)),
inference(resolve,[status(thm)],[c_454,c_347]) ).
cnf(c_418,plain,
loca_level_below(A,sbu,topsecret),
inference(resolve,[status(thm)],[c_269,c_414]) ).
cnf(c_455,plain,
( admin_indi_has_compartments(admin,alice,cons(compartmenta,V9))
| ~ admin_indi_has_compartments(admin,alice,V9)
| ~ oca_compartment_is_compartment(oca,compartmenta,V6,V7,V8,no)
| ~ oca_compartment_is_compartment(oca,compartmenta,D,E,no,F)
| ~ oca_compartment_is_compartment(oca,compartmenta,A,unclassified,B,C)
| ~ loca_level_below(admin,sbu,secret)
| ~ loca_level_below(admin,sbu,topsecret) ),
inference(resolve,[status(thm)],[c_304,c_270]) ).
cnf(c_456,plain,
( admin_indi_has_compartments(admin,alice,cons(compartmenta,V9))
| ~ admin_indi_has_compartments(admin,alice,V9)
| ~ oca_compartment_is_compartment(oca,compartmenta,V6,V7,V8,no)
| ~ oca_compartment_is_compartment(oca,compartmenta,D,E,no,F)
| ~ oca_compartment_is_compartment(oca,compartmenta,A,unclassified,B,C)
| ~ loca_level_below(admin,sbu,topsecret) ),
inference(resolve,[status(thm)],[c_455,c_414]) ).
cnf(c_457,plain,
( admin_indi_has_compartments(admin,alice,cons(compartmenta,V6))
| ~ admin_indi_has_compartments(admin,alice,V6)
| ~ oca_compartment_is_compartment(oca,compartmenta,D,E,F,no)
| ~ oca_compartment_is_compartment(oca,compartmenta,A,B,no,C)
| ~ loca_level_below(admin,sbu,topsecret) ),
inference(resolve,[status(thm)],[c_456,c_270]) ).
cnf(c_458,plain,
( admin_indi_has_compartments(admin,alice,cons(compartmenta,D))
| ~ admin_indi_has_compartments(admin,alice,D)
| ~ oca_compartment_is_compartment(oca,compartmenta,A,B,C,no)
| ~ loca_level_below(admin,sbu,topsecret) ),
inference(resolve,[status(thm)],[c_457,c_270]) ).
cnf(c_459,plain,
( admin_indi_has_compartments(admin,alice,cons(compartmenta,A))
| ~ admin_indi_has_compartments(admin,alice,A)
| ~ loca_level_below(admin,sbu,topsecret) ),
inference(resolve,[status(thm)],[c_458,c_270]) ).
cnf(c_460,plain,
( admin_indi_has_compartments(admin,alice,cons(compartmenta,nil))
| ~ loca_level_below(admin,sbu,topsecret) ),
inference(resolve,[status(thm)],[c_459,c_272]) ).
cnf(c_461,plain,
~ loca_level_below(admin,sbu,topsecret),
inference(resolve,[status(thm)],[c_460,c_417]) ).
cnf(c_444,plain,
$false,
inference(resolve,[status(thm)],[c_418,c_461]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWV437+1 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.10/0.36 % Computer : n017.cluster.edu
% 0.10/0.36 % Model : x86_64 x86_64
% 0.10/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.36 % Memory : 8046.5625MB
% 0.10/0.36 % OS : Linux 6.8.0-71-generic
% 0.10/0.36 % CPULimit : 300
% 0.10/0.36 % WCLimit : 300
% 0.10/0.36 % DateTime : Sat Sep 26 13:48:34 UTC 2026
% 0.10/0.36 % CPUTime :
% 0.10/0.36 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.10/0.36 % Process 865225 was started by sandbox2 on n017,
% 0.10/0.36 % Sat Sep 26 13:48:34 2026
% 0.10/0.36 % The command was "/export/starexec/sandbox2/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p".
% 0.10/0.38
% 0.10/0.38 % From the command line: assign(max_seconds, 300).
% 0.10/0.45
% 0.10/0.45 % SZS status Theorem for theBenchmark
% 0.10/0.45
% 0.10/0.45 % Proof 1 at 0.04 (+ 0.01) seconds.
% 0.10/0.45 % Length of proof is 211.
% 0.10/0.45 % Level of proof is 26.
% 0.10/0.45 % Maximum clause weight is 69.000.
% 0.10/0.45 % Given clauses 66.
% 0.10/0.45
% 0.10/0.45 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------