%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : SWV437+1 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n026.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 02:47:56 PM UTC 2026
% Result : Theorem 0.10s 0.40s
% Output : CNFRefutation 0.10s
% Verified :
% SZS Type : Refutation
% Derivation depth : 41
% Number of leaves : 68
% Syntax : Number of formulae : 307 ( 123 unt; 0 def)
% Number of atoms : 987 ( 0 equ)
% Maximal formula atoms : 20 ( 3 avg)
% Number of connectives : 1306 ( 626 ~; 603 |; 0 &)
% ( 0 <=>; 77 =>; 0 <=; 0 <~>)
% Maximal formula depth : 24 ( 5 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 : 537 ( 537 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f2,axiom,
! [K] : loca_level_direct_below(K,sbu,confidential),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f3,axiom,
! [K] : loca_level_direct_below(K,confidential,secret),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f4,axiom,
! [K] : loca_level_direct_below(K,secret,topsecret),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f5,axiom,
! [K,L] : loca_level_below(K,L,L),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f6,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('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f7,axiom,
! [C,SSO] :
( system_compartment_has_sso(system,C,SSO)
=> admin_compartment_has_sso(admin,C,SSO) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f8,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('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f9,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('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f10,axiom,
! [F,CL] : admin_file_has_compartments_h(admin,F,CL,nil),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f11,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('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f12,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('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f13,axiom,
! [F,L] : admin_file_has_level_h(admin,F,L,nil),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f14,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('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f18,axiom,
! [K,PA] :
( system_indi_is_polygraph_admin(system,PA)
=> ( polygraph_admin_indi_has_polygraph(PA,K)
=> admin_indi_has_polygraph(admin,K) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f19,axiom,
! [K,CA] :
( system_indi_is_credit_admin(system,CA)
=> ( credit_admin_indi_has_credit(CA,K)
=> admin_indi_has_credit(admin,K) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f20,axiom,
! [K] : admin_indi_has_background(admin,K,unclassified),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f21,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('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f22,axiom,
! [K,HR] :
( system_indi_is_hr_admin(system,HR)
=> ( hr_admin_indi_has_employment(HR,K)
=> admin_indi_has_employment(admin,K) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f24,axiom,
! [K,U] :
( system_indi_has_citizenship(system,K,U)
=> admin_indi_has_citizenship(admin,K,U) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f26,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('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f27,axiom,
! [K] : admin_indi_has_compartments(admin,K,nil),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f28,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('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f29,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('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f30,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('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f31,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('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f32,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('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f33,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('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f34,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('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f35,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('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f36,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('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f37,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('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f39,axiom,
! [K,F] :
( admin_indi_has_citizenship(admin,K,usa)
=> admin_indi_has_citizenship_for_file(admin,K,F) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f40,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('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f42,hypothesis,
system_indi_is_oca(system,oca),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f43,hypothesis,
oca_compartment_is_compartment(oca,compartmentb,confidential,topsecret,yes,yes),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f44,hypothesis,
oca_compartment_is_compartment(oca,compartmenta,sbu,unclassified,no,no),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f45,hypothesis,
system_compartment_has_sso(system,compartmentb,sso_compartmentb),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f46,hypothesis,
oca_compartment_has_scg(oca,compartmentb,scg_compartmentb),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f47,hypothesis,
sso_compartment_has_scg(sso_compartmentb,compartmentb,scg_compartmentb),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f48,hypothesis,
system_compartment_has_sso(system,compartmenta,sso_compartmenta),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f49,hypothesis,
oca_compartment_has_scg(oca,compartmenta,scg_compartmenta),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f50,hypothesis,
sso_compartment_has_scg(sso_compartmenta,compartmenta,scg_compartmenta),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f51,hypothesis,
state_file_is_not_working_paper(secretfile),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f52,hypothesis,
system_file_needs_compartments(system,secretfile,cons(compartmentb,cons(compartmenta,nil))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f53,hypothesis,
sso_file_has_compartments(sso_compartmentb,secretfile,cons(compartmentb,cons(compartmenta,nil))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f54,hypothesis,
sso_file_has_compartments(sso_compartmenta,secretfile,cons(compartmentb,cons(compartmenta,nil))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f55,hypothesis,
system_file_needs_level(system,secretfile,secret),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f56,hypothesis,
sso_file_has_level(sso_compartmentb,secretfile,secret,scg_compartmentb),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f57,hypothesis,
sso_file_has_level(sso_compartmenta,secretfile,secret,scg_compartmenta),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f61,hypothesis,
state_file_has_owner(secretfile,owner_secretfile),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f67,hypothesis,
system_indi_is_polygraph_admin(system,polygraph_admin),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f68,hypothesis,
system_indi_is_credit_admin(system,credit_admin),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f69,hypothesis,
system_indi_is_background_admin(system,background_admin),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f70,hypothesis,
system_indi_is_hr_admin(system,hr_admin),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f71,hypothesis,
system_indi_is_level_admin(system,level_admin),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f72,hypothesis,
system_indi_has_citizenship(system,alice,usa),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f73,hypothesis,
polygraph_admin_indi_has_polygraph(polygraph_admin,alice),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f74,hypothesis,
credit_admin_indi_has_credit(credit_admin,alice),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f75,hypothesis,
background_admin_indi_has_background(background_admin,alice,topsecret),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f76,hypothesis,
hr_admin_indi_has_employment(hr_admin,alice),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f77,hypothesis,
system_indi_needs_level(system,alice,secret),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f78,hypothesis,
level_admin_indi_has_level(level_admin,alice,topsecret),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f79,hypothesis,
system_indi_needs_compartment(system,alice,compartmentb),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f80,hypothesis,
system_indi_needs_compartment(system,alice,compartmenta),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f81,hypothesis,
sso_indi_has_compartment(sso_compartmentb,alice,compartmentb),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f82,hypothesis,
sso_indi_has_compartment(sso_compartmenta,alice,compartmenta),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f83,hypothesis,
owner_indi_has_need_to_know(owner_secretfile,alice,secretfile),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f88,conjecture,
admin_indi_may_file(admin,alice,secretfile,read),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f89,negated_conjecture,
~ admin_indi_may_file(admin,alice,secretfile,read),
inference(negated_conjecture,[status(cth)],[f88]) ).
fof(f91,plain,
! [X0] : loca_level_direct_below(X0,sbu,confidential),
inference(cnf_transformation,[status(thm)],[f2]) ).
fof(f92,plain,
! [X0] : loca_level_direct_below(X0,confidential,secret),
inference(cnf_transformation,[status(thm)],[f3]) ).
fof(f93,plain,
! [X0] : loca_level_direct_below(X0,secret,topsecret),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f94,plain,
! [X0,X1] : loca_level_below(X0,X1,X1),
inference(cnf_transformation,[status(thm)],[f5]) ).
fof(f95,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(pre_NNF_transformation,[status(thm)],[f6]) ).
fof(f96,plain,
! [K,L1,L11] :
( ! [L] :
( loca_level_below(K,L,L11)
| ~ loca_level_below(K,L,L1) )
| ~ loca_level_direct_below(K,L1,L11) ),
inference(miniscoping,[status(thm)],[f95]) ).
fof(f97,plain,
! [X0,X1,X2,X3] :
( loca_level_below(X0,X3,X2)
| ~ loca_level_below(X0,X3,X1)
| ~ loca_level_direct_below(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f96]) ).
fof(f98,plain,
! [C,SSO] :
( admin_compartment_has_sso(admin,C,SSO)
| ~ system_compartment_has_sso(system,C,SSO) ),
inference(pre_NNF_transformation,[status(thm)],[f7]) ).
fof(f99,plain,
! [X0,X1] :
( admin_compartment_has_sso(admin,X0,X1)
| ~ system_compartment_has_sso(system,X0,X1) ),
inference(cnf_transformation,[status(thm)],[f98]) ).
fof(f100,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(pre_NNF_transformation,[status(thm)],[f8]) ).
fof(f101,plain,
! [OCA] :
( ! [C,SCG] :
( ! [SSO] :
( 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(miniscoping,[status(thm)],[f100]) ).
fof(f102,plain,
! [X0,X1,X2,X3] :
( admin_compartment_has_scg(admin,X1,X2)
| ~ sso_compartment_has_scg(X3,X1,X2)
| ~ admin_compartment_has_sso(admin,X1,X3)
| ~ oca_compartment_has_scg(X0,X1,X2)
| ~ system_indi_is_oca(system,X0) ),
inference(cnf_transformation,[status(thm)],[f101]) ).
fof(f103,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(pre_NNF_transformation,[status(thm)],[f9]) ).
fof(f104,plain,
! [X0,X1] :
( admin_file_has_compartments(admin,X0,X1)
| ~ admin_file_has_compartments_h(admin,X0,X1,X1)
| ~ system_file_needs_compartments(system,X0,X1) ),
inference(cnf_transformation,[status(thm)],[f103]) ).
fof(f105,plain,
! [X0,X1] : admin_file_has_compartments_h(admin,X0,X1,nil),
inference(cnf_transformation,[status(thm)],[f10]) ).
fof(f106,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(pre_NNF_transformation,[status(thm)],[f11]) ).
fof(f107,plain,
! [C1,SSO] :
( ! [F,CL] :
( ! [CL1] :
( 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(miniscoping,[status(thm)],[f106]) ).
fof(f108,plain,
! [X0,X1,X2,X3,X4] :
( admin_file_has_compartments_h(admin,X2,X3,cons(X0,X4))
| ~ admin_file_has_compartments_h(admin,X2,X3,X4)
| ~ sso_file_has_compartments(X1,X2,X3)
| ~ admin_compartment_has_sso(admin,X0,X1) ),
inference(cnf_transformation,[status(thm)],[f107]) ).
fof(f109,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(pre_NNF_transformation,[status(thm)],[f12]) ).
fof(f110,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(miniscoping,[status(thm)],[f109]) ).
fof(f111,plain,
! [X0,X1,X2] :
( admin_file_has_level(admin,X0,X1)
| ~ admin_file_has_level_h(admin,X0,X1,X2)
| ~ admin_file_has_compartments(admin,X0,X2)
| ~ system_file_needs_level(system,X0,X1) ),
inference(cnf_transformation,[status(thm)],[f110]) ).
fof(f112,plain,
! [X0,X1] : admin_file_has_level_h(admin,X0,X1,nil),
inference(cnf_transformation,[status(thm)],[f13]) ).
fof(f113,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(pre_NNF_transformation,[status(thm)],[f14]) ).
fof(f114,plain,
! [C,SSO] :
( ! [SCG] :
( ! [F,L] :
( ! [CL] :
( 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(miniscoping,[status(thm)],[f113]) ).
fof(f115,plain,
! [X0,X1,X2,X3,X4,X5] :
( admin_file_has_level_h(admin,X3,X4,cons(X0,X5))
| ~ admin_file_has_level_h(admin,X3,X4,X5)
| ~ sso_file_has_level(X1,X3,X4,X2)
| ~ admin_compartment_has_scg(admin,X0,X2)
| ~ admin_compartment_has_sso(admin,X0,X1) ),
inference(cnf_transformation,[status(thm)],[f114]) ).
fof(f123,plain,
! [K,PA] :
( admin_indi_has_polygraph(admin,K)
| ~ polygraph_admin_indi_has_polygraph(PA,K)
| ~ system_indi_is_polygraph_admin(system,PA) ),
inference(pre_NNF_transformation,[status(thm)],[f18]) ).
fof(f124,plain,
! [PA] :
( ! [K] :
( admin_indi_has_polygraph(admin,K)
| ~ polygraph_admin_indi_has_polygraph(PA,K) )
| ~ system_indi_is_polygraph_admin(system,PA) ),
inference(miniscoping,[status(thm)],[f123]) ).
fof(f125,plain,
! [X0,X1] :
( admin_indi_has_polygraph(admin,X1)
| ~ polygraph_admin_indi_has_polygraph(X0,X1)
| ~ system_indi_is_polygraph_admin(system,X0) ),
inference(cnf_transformation,[status(thm)],[f124]) ).
fof(f126,plain,
! [K,CA] :
( admin_indi_has_credit(admin,K)
| ~ credit_admin_indi_has_credit(CA,K)
| ~ system_indi_is_credit_admin(system,CA) ),
inference(pre_NNF_transformation,[status(thm)],[f19]) ).
fof(f127,plain,
! [CA] :
( ! [K] :
( admin_indi_has_credit(admin,K)
| ~ credit_admin_indi_has_credit(CA,K) )
| ~ system_indi_is_credit_admin(system,CA) ),
inference(miniscoping,[status(thm)],[f126]) ).
fof(f128,plain,
! [X0,X1] :
( admin_indi_has_credit(admin,X1)
| ~ credit_admin_indi_has_credit(X0,X1)
| ~ system_indi_is_credit_admin(system,X0) ),
inference(cnf_transformation,[status(thm)],[f127]) ).
fof(f129,plain,
! [X0] : admin_indi_has_background(admin,X0,unclassified),
inference(cnf_transformation,[status(thm)],[f20]) ).
fof(f130,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(pre_NNF_transformation,[status(thm)],[f21]) ).
fof(f131,plain,
! [BA] :
( ! [K,L1] :
( ! [L] :
( 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(miniscoping,[status(thm)],[f130]) ).
fof(f132,plain,
! [X0,X1,X2,X3] :
( admin_indi_has_background(admin,X1,X3)
| ~ loca_level_below(admin,X3,X2)
| ~ background_admin_indi_has_background(X0,X1,X2)
| ~ system_indi_is_background_admin(system,X0) ),
inference(cnf_transformation,[status(thm)],[f131]) ).
fof(f133,plain,
! [K,HR] :
( admin_indi_has_employment(admin,K)
| ~ hr_admin_indi_has_employment(HR,K)
| ~ system_indi_is_hr_admin(system,HR) ),
inference(pre_NNF_transformation,[status(thm)],[f22]) ).
fof(f134,plain,
! [HR] :
( ! [K] :
( admin_indi_has_employment(admin,K)
| ~ hr_admin_indi_has_employment(HR,K) )
| ~ system_indi_is_hr_admin(system,HR) ),
inference(miniscoping,[status(thm)],[f133]) ).
fof(f135,plain,
! [X0,X1] :
( admin_indi_has_employment(admin,X1)
| ~ hr_admin_indi_has_employment(X0,X1)
| ~ system_indi_is_hr_admin(system,X0) ),
inference(cnf_transformation,[status(thm)],[f134]) ).
fof(f137,plain,
! [K,U] :
( admin_indi_has_citizenship(admin,K,U)
| ~ system_indi_has_citizenship(system,K,U) ),
inference(pre_NNF_transformation,[status(thm)],[f24]) ).
fof(f138,plain,
! [X0,X1] :
( admin_indi_has_citizenship(admin,X0,X1)
| ~ system_indi_has_citizenship(system,X0,X1) ),
inference(cnf_transformation,[status(thm)],[f137]) ).
fof(f140,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(pre_NNF_transformation,[status(thm)],[f26]) ).
fof(f141,plain,
! [K,L1] :
( ! [L] :
( ! [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(miniscoping,[status(thm)],[f140]) ).
fof(f142,plain,
! [X0,X1,X2,X3,X4] :
( admin_indi_has_level(admin,X0,X2)
| ~ admin_indi_has_background(admin,X0,X2)
| ~ loca_level_below(admin,X2,X4)
| ~ level_admin_indi_has_level(X3,X0,X4)
| ~ system_indi_is_level_admin(system,X3)
| ~ loca_level_below(admin,X2,X1)
| ~ admin_indi_has_credit(admin,X0)
| ~ admin_indi_has_employment(admin,X0)
| ~ admin_indi_has_polygraph(admin,X0)
| ~ admin_indi_has_citizenship(admin,X0,usa)
| ~ system_indi_needs_level(system,X0,X1) ),
inference(cnf_transformation,[status(thm)],[f141]) ).
fof(f143,plain,
! [X0] : admin_indi_has_compartments(admin,X0,nil),
inference(cnf_transformation,[status(thm)],[f27]) ).
fof(f144,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(pre_NNF_transformation,[status(thm)],[f28]) ).
fof(f145,plain,
! [K,C] :
( ! [SSO] :
( ! [CL] :
( 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(miniscoping,[status(thm)],[f144]) ).
fof(f146,plain,
! [X0,X1,X2,X3] :
( admin_indi_has_compartments(admin,X0,cons(X1,X3))
| ~ admin_indi_has_compartments(admin,X0,X3)
| ~ admin_indi_has_level_for_compartment(admin,X0,X1)
| ~ admin_indi_has_background_for_compartment(admin,X0,X1)
| ~ sso_indi_has_compartment(X2,X0,X1)
| ~ admin_compartment_has_sso(admin,X1,X2)
| ~ admin_indi_has_credit_for_compartment(admin,X0,X1)
| ~ admin_indi_has_polygraph_for_compartment(admin,X0,X1)
| ~ admin_indi_has_citizenship(admin,X0,usa)
| ~ admin_indi_has_employment(admin,X0)
| ~ system_indi_needs_compartment(system,X0,X1) ),
inference(cnf_transformation,[status(thm)],[f145]) ).
fof(f147,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(pre_NNF_transformation,[status(thm)],[f29]) ).
fof(f148,plain,
! [OCA] :
( ! [C,L2] :
( ! [K] :
( admin_indi_has_background_for_compartment(admin,K,C)
| ~ admin_indi_has_background(admin,K,L2) )
| ! [L1,B1,B2] : ~ oca_compartment_is_compartment(OCA,C,L1,L2,B1,B2) )
| ~ system_indi_is_oca(system,OCA) ),
inference(miniscoping,[status(thm)],[f147]) ).
fof(f149,plain,
! [X0,X1,X2,X3,X4,X5,X6] :
( admin_indi_has_background_for_compartment(admin,X6,X1)
| ~ admin_indi_has_background(admin,X6,X3)
| ~ oca_compartment_is_compartment(X0,X1,X2,X3,X4,X5)
| ~ system_indi_is_oca(system,X0) ),
inference(cnf_transformation,[status(thm)],[f148]) ).
fof(f150,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(pre_NNF_transformation,[status(thm)],[f30]) ).
fof(f151,plain,
! [OCA] :
( ! [C,L1] :
( ! [K] :
( admin_indi_has_level_for_compartment(admin,K,C)
| ~ admin_indi_has_level(admin,K,L1) )
| ! [L2,B1,B2] : ~ oca_compartment_is_compartment(OCA,C,L1,L2,B1,B2) )
| ~ system_indi_is_oca(system,OCA) ),
inference(miniscoping,[status(thm)],[f150]) ).
fof(f152,plain,
! [X0,X1,X2,X3,X4,X5,X6] :
( admin_indi_has_level_for_compartment(admin,X6,X1)
| ~ admin_indi_has_level(admin,X6,X2)
| ~ oca_compartment_is_compartment(X0,X1,X2,X3,X4,X5)
| ~ system_indi_is_oca(system,X0) ),
inference(cnf_transformation,[status(thm)],[f151]) ).
fof(f153,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(pre_NNF_transformation,[status(thm)],[f31]) ).
fof(f154,plain,
! [OCA] :
( ! [C] :
( ! [K] :
( admin_indi_has_polygraph_for_compartment(admin,K,C)
| ~ admin_indi_has_polygraph(admin,K) )
| ! [L1,L2,B1] : ~ oca_compartment_is_compartment(OCA,C,L1,L2,B1,yes) )
| ~ system_indi_is_oca(system,OCA) ),
inference(miniscoping,[status(thm)],[f153]) ).
fof(f155,plain,
! [X0,X1,X2,X3,X4,X5] :
( admin_indi_has_polygraph_for_compartment(admin,X5,X1)
| ~ admin_indi_has_polygraph(admin,X5)
| ~ oca_compartment_is_compartment(X0,X1,X2,X3,X4,yes)
| ~ system_indi_is_oca(system,X0) ),
inference(cnf_transformation,[status(thm)],[f154]) ).
fof(f156,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(pre_NNF_transformation,[status(thm)],[f32]) ).
fof(f157,plain,
! [OCA] :
( ! [C] :
( ! [K] : admin_indi_has_polygraph_for_compartment(admin,K,C)
| ! [L1,L2,B1] : ~ oca_compartment_is_compartment(OCA,C,L1,L2,B1,no) )
| ~ system_indi_is_oca(system,OCA) ),
inference(miniscoping,[status(thm)],[f156]) ).
fof(f158,plain,
! [X0,X1,X2,X3,X4,X5] :
( admin_indi_has_polygraph_for_compartment(admin,X5,X1)
| ~ oca_compartment_is_compartment(X0,X1,X2,X3,X4,no)
| ~ system_indi_is_oca(system,X0) ),
inference(cnf_transformation,[status(thm)],[f157]) ).
fof(f159,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(pre_NNF_transformation,[status(thm)],[f33]) ).
fof(f160,plain,
! [OCA] :
( ! [C] :
( ! [K] :
( admin_indi_has_credit_for_compartment(admin,K,C)
| ~ admin_indi_has_credit(admin,K) )
| ! [L1,L2,B2] : ~ oca_compartment_is_compartment(OCA,C,L1,L2,yes,B2) )
| ~ system_indi_is_oca(system,OCA) ),
inference(miniscoping,[status(thm)],[f159]) ).
fof(f161,plain,
! [X0,X1,X2,X3,X4,X5] :
( admin_indi_has_credit_for_compartment(admin,X5,X1)
| ~ admin_indi_has_credit(admin,X5)
| ~ oca_compartment_is_compartment(X0,X1,X2,X3,yes,X4)
| ~ system_indi_is_oca(system,X0) ),
inference(cnf_transformation,[status(thm)],[f160]) ).
fof(f162,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(pre_NNF_transformation,[status(thm)],[f34]) ).
fof(f163,plain,
! [OCA] :
( ! [C] :
( ! [K] : admin_indi_has_credit_for_compartment(admin,K,C)
| ! [L1,L2,B2] : ~ oca_compartment_is_compartment(OCA,C,L1,L2,no,B2) )
| ~ system_indi_is_oca(system,OCA) ),
inference(miniscoping,[status(thm)],[f162]) ).
fof(f164,plain,
! [X0,X1,X2,X3,X4,X5] :
( admin_indi_has_credit_for_compartment(admin,X5,X1)
| ~ oca_compartment_is_compartment(X0,X1,X2,X3,no,X4)
| ~ system_indi_is_oca(system,X0) ),
inference(cnf_transformation,[status(thm)],[f163]) ).
fof(f165,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(pre_NNF_transformation,[status(thm)],[f35]) ).
fof(f166,plain,
! [F,CL] :
( ! [K] :
( admin_indi_has_compartments_for_file(admin,K,F)
| ~ admin_indi_has_compartments(admin,K,CL) )
| ~ admin_file_has_compartments(admin,F,CL) ),
inference(miniscoping,[status(thm)],[f165]) ).
fof(f167,plain,
! [X0,X1,X2] :
( admin_indi_has_compartments_for_file(admin,X2,X0)
| ~ admin_indi_has_compartments(admin,X2,X1)
| ~ admin_file_has_compartments(admin,X0,X1) ),
inference(cnf_transformation,[status(thm)],[f166]) ).
fof(f168,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(pre_NNF_transformation,[status(thm)],[f36]) ).
fof(f169,plain,
! [F,L] :
( ! [K] :
( admin_indi_has_level_for_file(admin,K,F)
| ~ admin_indi_has_level(admin,K,L) )
| ~ admin_file_has_level(admin,F,L) ),
inference(miniscoping,[status(thm)],[f168]) ).
fof(f170,plain,
! [X0,X1,X2] :
( admin_indi_has_level_for_file(admin,X2,X0)
| ~ admin_indi_has_level(admin,X2,X1)
| ~ admin_file_has_level(admin,X0,X1) ),
inference(cnf_transformation,[status(thm)],[f169]) ).
fof(f171,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(pre_NNF_transformation,[status(thm)],[f37]) ).
fof(f172,plain,
! [F,OWR] :
( ! [K] :
( 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(miniscoping,[status(thm)],[f171]) ).
fof(f173,plain,
! [X0,X1,X2] :
( admin_indi_has_need_to_know_for_file(admin,X2,X0)
| ~ owner_indi_has_need_to_know(X1,X2,X0)
| ~ state_file_has_owner(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f172]) ).
fof(f177,plain,
! [K,F] :
( admin_indi_has_citizenship_for_file(admin,K,F)
| ~ admin_indi_has_citizenship(admin,K,usa) ),
inference(pre_NNF_transformation,[status(thm)],[f39]) ).
fof(f178,plain,
! [K] :
( ! [F] : admin_indi_has_citizenship_for_file(admin,K,F)
| ~ admin_indi_has_citizenship(admin,K,usa) ),
inference(miniscoping,[status(thm)],[f177]) ).
fof(f179,plain,
! [X0,X1] :
( admin_indi_has_citizenship_for_file(admin,X0,X1)
| ~ admin_indi_has_citizenship(admin,X0,usa) ),
inference(cnf_transformation,[status(thm)],[f178]) ).
fof(f180,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(pre_NNF_transformation,[status(thm)],[f40]) ).
fof(f181,plain,
! [F] :
( ! [K] :
( 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(miniscoping,[status(thm)],[f180]) ).
fof(f182,plain,
! [X0,X1] :
( admin_indi_may_file(admin,X1,X0,read)
| ~ admin_indi_has_compartments_for_file(admin,X1,X0)
| ~ admin_indi_has_level_for_file(admin,X1,X0)
| ~ admin_indi_has_need_to_know_for_file(admin,X1,X0)
| ~ admin_indi_has_citizenship_for_file(admin,X1,X0)
| ~ state_file_is_not_working_paper(X0) ),
inference(cnf_transformation,[status(thm)],[f181]) ).
fof(f186,plain,
system_indi_is_oca(system,oca),
inference(cnf_transformation,[status(thm)],[f42]) ).
fof(f187,plain,
oca_compartment_is_compartment(oca,compartmentb,confidential,topsecret,yes,yes),
inference(cnf_transformation,[status(thm)],[f43]) ).
fof(f188,plain,
oca_compartment_is_compartment(oca,compartmenta,sbu,unclassified,no,no),
inference(cnf_transformation,[status(thm)],[f44]) ).
fof(f189,plain,
system_compartment_has_sso(system,compartmentb,sso_compartmentb),
inference(cnf_transformation,[status(thm)],[f45]) ).
fof(f190,plain,
oca_compartment_has_scg(oca,compartmentb,scg_compartmentb),
inference(cnf_transformation,[status(thm)],[f46]) ).
fof(f191,plain,
sso_compartment_has_scg(sso_compartmentb,compartmentb,scg_compartmentb),
inference(cnf_transformation,[status(thm)],[f47]) ).
fof(f192,plain,
system_compartment_has_sso(system,compartmenta,sso_compartmenta),
inference(cnf_transformation,[status(thm)],[f48]) ).
fof(f193,plain,
oca_compartment_has_scg(oca,compartmenta,scg_compartmenta),
inference(cnf_transformation,[status(thm)],[f49]) ).
fof(f194,plain,
sso_compartment_has_scg(sso_compartmenta,compartmenta,scg_compartmenta),
inference(cnf_transformation,[status(thm)],[f50]) ).
fof(f195,plain,
state_file_is_not_working_paper(secretfile),
inference(cnf_transformation,[status(thm)],[f51]) ).
fof(f196,plain,
system_file_needs_compartments(system,secretfile,cons(compartmentb,cons(compartmenta,nil))),
inference(cnf_transformation,[status(thm)],[f52]) ).
fof(f197,plain,
sso_file_has_compartments(sso_compartmentb,secretfile,cons(compartmentb,cons(compartmenta,nil))),
inference(cnf_transformation,[status(thm)],[f53]) ).
fof(f198,plain,
sso_file_has_compartments(sso_compartmenta,secretfile,cons(compartmentb,cons(compartmenta,nil))),
inference(cnf_transformation,[status(thm)],[f54]) ).
fof(f199,plain,
system_file_needs_level(system,secretfile,secret),
inference(cnf_transformation,[status(thm)],[f55]) ).
fof(f200,plain,
sso_file_has_level(sso_compartmentb,secretfile,secret,scg_compartmentb),
inference(cnf_transformation,[status(thm)],[f56]) ).
fof(f201,plain,
sso_file_has_level(sso_compartmenta,secretfile,secret,scg_compartmenta),
inference(cnf_transformation,[status(thm)],[f57]) ).
fof(f205,plain,
state_file_has_owner(secretfile,owner_secretfile),
inference(cnf_transformation,[status(thm)],[f61]) ).
fof(f211,plain,
system_indi_is_polygraph_admin(system,polygraph_admin),
inference(cnf_transformation,[status(thm)],[f67]) ).
fof(f212,plain,
system_indi_is_credit_admin(system,credit_admin),
inference(cnf_transformation,[status(thm)],[f68]) ).
fof(f213,plain,
system_indi_is_background_admin(system,background_admin),
inference(cnf_transformation,[status(thm)],[f69]) ).
fof(f214,plain,
system_indi_is_hr_admin(system,hr_admin),
inference(cnf_transformation,[status(thm)],[f70]) ).
fof(f215,plain,
system_indi_is_level_admin(system,level_admin),
inference(cnf_transformation,[status(thm)],[f71]) ).
fof(f216,plain,
system_indi_has_citizenship(system,alice,usa),
inference(cnf_transformation,[status(thm)],[f72]) ).
fof(f217,plain,
polygraph_admin_indi_has_polygraph(polygraph_admin,alice),
inference(cnf_transformation,[status(thm)],[f73]) ).
fof(f218,plain,
credit_admin_indi_has_credit(credit_admin,alice),
inference(cnf_transformation,[status(thm)],[f74]) ).
fof(f219,plain,
background_admin_indi_has_background(background_admin,alice,topsecret),
inference(cnf_transformation,[status(thm)],[f75]) ).
fof(f220,plain,
hr_admin_indi_has_employment(hr_admin,alice),
inference(cnf_transformation,[status(thm)],[f76]) ).
fof(f221,plain,
system_indi_needs_level(system,alice,secret),
inference(cnf_transformation,[status(thm)],[f77]) ).
fof(f222,plain,
level_admin_indi_has_level(level_admin,alice,topsecret),
inference(cnf_transformation,[status(thm)],[f78]) ).
fof(f223,plain,
system_indi_needs_compartment(system,alice,compartmentb),
inference(cnf_transformation,[status(thm)],[f79]) ).
fof(f224,plain,
system_indi_needs_compartment(system,alice,compartmenta),
inference(cnf_transformation,[status(thm)],[f80]) ).
fof(f225,plain,
sso_indi_has_compartment(sso_compartmentb,alice,compartmentb),
inference(cnf_transformation,[status(thm)],[f81]) ).
fof(f226,plain,
sso_indi_has_compartment(sso_compartmenta,alice,compartmenta),
inference(cnf_transformation,[status(thm)],[f82]) ).
fof(f227,plain,
owner_indi_has_need_to_know(owner_secretfile,alice,secretfile),
inference(cnf_transformation,[status(thm)],[f83]) ).
fof(f232,plain,
~ admin_indi_may_file(admin,alice,secretfile,read),
inference(cnf_transformation,[status(thm)],[f89]) ).
fof(f233,plain,
! [X0,X1] :
( loca_level_below(X0,X1,topsecret)
| ~ loca_level_below(X0,X1,secret) ),
inference(resolution,[status(thm)],[f97,f93]) ).
fof(f234,plain,
! [X0,X1] :
( loca_level_below(X0,X1,secret)
| ~ loca_level_below(X0,X1,confidential) ),
inference(resolution,[status(thm)],[f97,f92]) ).
fof(f235,plain,
! [X0,X1] :
( loca_level_below(X0,X1,confidential)
| ~ loca_level_below(X0,X1,sbu) ),
inference(resolution,[status(thm)],[f97,f91]) ).
fof(f237,plain,
admin_compartment_has_sso(admin,compartmenta,sso_compartmenta),
inference(resolution,[status(thm)],[f99,f192]) ).
fof(f238,plain,
admin_compartment_has_sso(admin,compartmentb,sso_compartmentb),
inference(resolution,[status(thm)],[f99,f189]) ).
fof(f239,plain,
! [X0] :
( admin_compartment_has_scg(admin,compartmenta,scg_compartmenta)
| ~ admin_compartment_has_sso(admin,compartmenta,sso_compartmenta)
| ~ oca_compartment_has_scg(X0,compartmenta,scg_compartmenta)
| ~ system_indi_is_oca(system,X0) ),
inference(resolution,[status(thm)],[f102,f194]) ).
fof(f240,plain,
! [X0] :
( admin_compartment_has_scg(admin,compartmentb,scg_compartmentb)
| ~ admin_compartment_has_sso(admin,compartmentb,sso_compartmentb)
| ~ oca_compartment_has_scg(X0,compartmentb,scg_compartmentb)
| ~ system_indi_is_oca(system,X0) ),
inference(resolution,[status(thm)],[f102,f191]) ).
fof(f242,plain,
! [X0,X1,X2,X3] :
( admin_file_has_compartments(admin,X2,cons(X0,X3))
| ~ system_file_needs_compartments(system,X2,cons(X0,X3))
| ~ admin_file_has_compartments_h(admin,X2,cons(X0,X3),X3)
| ~ sso_file_has_compartments(X1,X2,cons(X0,X3))
| ~ admin_compartment_has_sso(admin,X0,X1) ),
inference(resolution,[status(thm)],[f108,f104]) ).
fof(f245,plain,
admin_indi_has_citizenship(admin,alice,usa),
inference(resolution,[status(thm)],[f138,f216]) ).
fof(f246,plain,
! [X0] : loca_level_below(X0,secret,topsecret),
inference(resolution,[status(thm)],[f233,f94]) ).
fof(f247,plain,
! [X0] : loca_level_below(X0,confidential,secret),
inference(resolution,[status(thm)],[f234,f94]) ).
fof(f248,plain,
! [X0] : loca_level_below(X0,confidential,topsecret),
inference(resolution,[status(thm)],[f247,f233]) ).
fof(f249,plain,
! [X0,X1,X2,X3,X4,X5] :
( admin_file_has_level(admin,X3,X4)
| ~ admin_file_has_compartments(admin,X3,cons(X0,X5))
| ~ system_file_needs_level(system,X3,X4)
| ~ admin_file_has_level_h(admin,X3,X4,X5)
| ~ sso_file_has_level(X1,X3,X4,X2)
| ~ admin_compartment_has_scg(admin,X0,X2)
| ~ admin_compartment_has_sso(admin,X0,X1) ),
inference(resolution,[status(thm)],[f115,f111]) ).
fof(f252,plain,
! [X0] : loca_level_below(X0,sbu,confidential),
inference(resolution,[status(thm)],[f235,f94]) ).
fof(f253,plain,
! [X0] : loca_level_below(X0,sbu,secret),
inference(resolution,[status(thm)],[f252,f234]) ).
fof(f254,plain,
! [X0] : loca_level_below(X0,sbu,topsecret),
inference(resolution,[status(thm)],[f253,f233]) ).
fof(f255,plain,
( admin_indi_has_polygraph(admin,alice)
| ~ system_indi_is_polygraph_admin(system,polygraph_admin) ),
inference(resolution,[status(thm)],[f125,f217]) ).
fof(f256,plain,
admin_indi_has_polygraph(admin,alice),
inference(forward_subsumption_resolution,[status(thm)],[f255,f211]) ).
fof(f261,plain,
! [X0] : admin_indi_has_citizenship_for_file(admin,alice,X0),
inference(resolution,[status(thm)],[f179,f245]) ).
fof(f262,plain,
( admin_indi_has_credit(admin,alice)
| ~ system_indi_is_credit_admin(system,credit_admin) ),
inference(resolution,[status(thm)],[f128,f218]) ).
fof(f263,plain,
admin_indi_has_credit(admin,alice),
inference(forward_subsumption_resolution,[status(thm)],[f262,f212]) ).
fof(f264,plain,
! [X0] :
( admin_indi_has_background(admin,alice,X0)
| ~ loca_level_below(admin,X0,topsecret)
| ~ system_indi_is_background_admin(system,background_admin) ),
inference(resolution,[status(thm)],[f132,f219]) ).
fof(f265,plain,
! [X0] :
( admin_indi_has_background(admin,alice,X0)
| ~ loca_level_below(admin,X0,topsecret) ),
inference(forward_subsumption_resolution,[status(thm)],[f264,f213]) ).
fof(f266,plain,
( admin_indi_has_employment(admin,alice)
| ~ system_indi_is_hr_admin(system,hr_admin) ),
inference(resolution,[status(thm)],[f135,f220]) ).
fof(f267,plain,
admin_indi_has_employment(admin,alice),
inference(forward_subsumption_resolution,[status(thm)],[f266,f214]) ).
fof(f270,plain,
admin_indi_has_background(admin,alice,sbu),
inference(resolution,[status(thm)],[f265,f254]) ).
fof(f271,plain,
admin_indi_has_background(admin,alice,confidential),
inference(resolution,[status(thm)],[f265,f248]) ).
fof(f272,plain,
admin_indi_has_background(admin,alice,secret),
inference(resolution,[status(thm)],[f265,f246]) ).
fof(f273,plain,
admin_indi_has_background(admin,alice,topsecret),
inference(resolution,[status(thm)],[f265,f94]) ).
fof(f276,plain,
( admin_indi_has_need_to_know_for_file(admin,alice,secretfile)
| ~ state_file_has_owner(secretfile,owner_secretfile) ),
inference(resolution,[status(thm)],[f173,f227]) ).
fof(f278,plain,
admin_indi_has_need_to_know_for_file(admin,alice,secretfile),
inference(forward_subsumption_resolution,[status(thm)],[f276,f205]) ).
fof(f279,plain,
! [X0,X1] :
( admin_indi_has_level(admin,alice,X1)
| ~ admin_indi_has_background(admin,alice,X1)
| ~ loca_level_below(admin,X1,topsecret)
| ~ system_indi_is_level_admin(system,level_admin)
| ~ loca_level_below(admin,X1,X0)
| ~ admin_indi_has_credit(admin,alice)
| ~ admin_indi_has_employment(admin,alice)
| ~ admin_indi_has_polygraph(admin,alice)
| ~ admin_indi_has_citizenship(admin,alice,usa)
| ~ system_indi_needs_level(system,alice,X0) ),
inference(resolution,[status(thm)],[f142,f222]) ).
fof(f280,plain,
! [X0,X1] :
( admin_indi_has_level(admin,alice,X1)
| ~ admin_indi_has_background(admin,alice,X1)
| ~ loca_level_below(admin,X1,topsecret)
| ~ system_indi_is_level_admin(system,level_admin)
| ~ loca_level_below(admin,X1,X0)
| ~ admin_indi_has_credit(admin,alice)
| ~ admin_indi_has_employment(admin,alice)
| ~ admin_indi_has_polygraph(admin,alice)
| ~ system_indi_needs_level(system,alice,X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f279,f245]) ).
fof(f281,plain,
! [X0] :
( admin_indi_has_background_for_compartment(admin,X0,compartmenta)
| ~ admin_indi_has_background(admin,X0,unclassified)
| ~ system_indi_is_oca(system,oca) ),
inference(resolution,[status(thm)],[f149,f188]) ).
fof(f282,plain,
! [X0] :
( admin_indi_has_background_for_compartment(admin,X0,compartmentb)
| ~ admin_indi_has_background(admin,X0,topsecret)
| ~ system_indi_is_oca(system,oca) ),
inference(resolution,[status(thm)],[f149,f187]) ).
fof(f283,plain,
! [X0] :
( admin_indi_has_background_for_compartment(admin,X0,compartmenta)
| ~ admin_indi_has_background(admin,X0,unclassified) ),
inference(forward_subsumption_resolution,[status(thm)],[f281,f186]) ).
fof(f284,plain,
! [X0] :
( admin_indi_has_background_for_compartment(admin,X0,compartmentb)
| ~ admin_indi_has_background(admin,X0,topsecret) ),
inference(forward_subsumption_resolution,[status(thm)],[f282,f186]) ).
fof(f285,plain,
! [X0] : admin_indi_has_background_for_compartment(admin,X0,compartmenta),
inference(forward_subsumption_resolution,[status(thm)],[f283,f129]) ).
fof(f286,plain,
admin_indi_has_background_for_compartment(admin,alice,compartmentb),
inference(resolution,[status(thm)],[f284,f273]) ).
fof(f287,plain,
! [X0] :
( admin_indi_has_level_for_compartment(admin,X0,compartmenta)
| ~ admin_indi_has_level(admin,X0,sbu)
| ~ system_indi_is_oca(system,oca) ),
inference(resolution,[status(thm)],[f152,f188]) ).
fof(f288,plain,
! [X0] :
( admin_indi_has_level_for_compartment(admin,X0,compartmentb)
| ~ admin_indi_has_level(admin,X0,confidential)
| ~ system_indi_is_oca(system,oca) ),
inference(resolution,[status(thm)],[f152,f187]) ).
fof(f289,plain,
! [X0] :
( admin_indi_has_level_for_compartment(admin,X0,compartmenta)
| ~ admin_indi_has_level(admin,X0,sbu) ),
inference(forward_subsumption_resolution,[status(thm)],[f287,f186]) ).
fof(f290,plain,
! [X0] :
( admin_indi_has_level_for_compartment(admin,X0,compartmentb)
| ~ admin_indi_has_level(admin,X0,confidential) ),
inference(forward_subsumption_resolution,[status(thm)],[f288,f186]) ).
fof(f291,plain,
! [X0,X1,X2,X3,X4] :
( ~ admin_indi_has_compartments(admin,X3,X2)
| ~ admin_indi_has_level_for_compartment(admin,X3,X1)
| ~ admin_indi_has_background_for_compartment(admin,X3,X1)
| ~ sso_indi_has_compartment(X4,X3,X1)
| ~ admin_compartment_has_sso(admin,X1,X4)
| ~ admin_indi_has_credit_for_compartment(admin,X3,X1)
| ~ admin_indi_has_polygraph_for_compartment(admin,X3,X1)
| ~ admin_indi_has_citizenship(admin,X3,usa)
| ~ admin_indi_has_employment(admin,X3)
| ~ system_indi_needs_compartment(system,X3,X1)
| admin_indi_has_compartments_for_file(admin,X3,X0)
| ~ admin_file_has_compartments(admin,X0,cons(X1,X2)) ),
inference(resolution,[status(thm)],[f167,f146]) ).
fof(f298,plain,
! [X0] :
( admin_indi_has_polygraph_for_compartment(admin,X0,compartmentb)
| ~ admin_indi_has_polygraph(admin,X0)
| ~ system_indi_is_oca(system,oca) ),
inference(resolution,[status(thm)],[f155,f187]) ).
fof(f299,plain,
! [X0] :
( admin_indi_has_polygraph_for_compartment(admin,X0,compartmentb)
| ~ admin_indi_has_polygraph(admin,X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f298,f186]) ).
fof(f300,plain,
! [X0] :
( admin_indi_has_polygraph_for_compartment(admin,X0,compartmenta)
| ~ system_indi_is_oca(system,oca) ),
inference(resolution,[status(thm)],[f158,f188]) ).
fof(f301,plain,
! [X0] : admin_indi_has_polygraph_for_compartment(admin,X0,compartmenta),
inference(forward_subsumption_resolution,[status(thm)],[f300,f186]) ).
fof(f309,plain,
! [X0] :
( admin_indi_has_credit_for_compartment(admin,X0,compartmenta)
| ~ system_indi_is_oca(system,oca) ),
inference(resolution,[status(thm)],[f164,f188]) ).
fof(f310,plain,
! [X0] : admin_indi_has_credit_for_compartment(admin,X0,compartmenta),
inference(forward_subsumption_resolution,[status(thm)],[f309,f186]) ).
fof(f311,plain,
! [X0] :
( admin_indi_has_credit_for_compartment(admin,X0,compartmentb)
| ~ admin_indi_has_credit(admin,X0)
| ~ system_indi_is_oca(system,oca) ),
inference(resolution,[status(thm)],[f161,f187]) ).
fof(f312,plain,
! [X0] :
( admin_indi_has_credit_for_compartment(admin,X0,compartmentb)
| ~ admin_indi_has_credit(admin,X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f311,f186]) ).
fof(f313,plain,
! [X0] :
( admin_compartment_has_scg(admin,compartmenta,scg_compartmenta)
| ~ oca_compartment_has_scg(X0,compartmenta,scg_compartmenta)
| ~ system_indi_is_oca(system,X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f239,f237]) ).
fof(f314,plain,
( admin_compartment_has_scg(admin,compartmenta,scg_compartmenta)
| ~ system_indi_is_oca(system,oca) ),
inference(resolution,[status(thm)],[f313,f193]) ).
fof(f315,plain,
admin_compartment_has_scg(admin,compartmenta,scg_compartmenta),
inference(forward_subsumption_resolution,[status(thm)],[f314,f186]) ).
fof(f316,plain,
( ~ admin_indi_has_compartments_for_file(admin,alice,secretfile)
| ~ admin_indi_has_level_for_file(admin,alice,secretfile)
| ~ 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) ),
inference(resolution,[status(thm)],[f182,f232]) ).
fof(f317,plain,
( ~ admin_indi_has_compartments_for_file(admin,alice,secretfile)
| ~ admin_indi_has_level_for_file(admin,alice,secretfile)
| ~ admin_indi_has_need_to_know_for_file(admin,alice,secretfile)
| ~ admin_indi_has_citizenship_for_file(admin,alice,secretfile) ),
inference(forward_subsumption_resolution,[status(thm)],[f316,f195]) ).
fof(f318,plain,
! [X0] :
( admin_compartment_has_scg(admin,compartmentb,scg_compartmentb)
| ~ oca_compartment_has_scg(X0,compartmentb,scg_compartmentb)
| ~ system_indi_is_oca(system,X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f240,f238]) ).
fof(f319,plain,
( admin_compartment_has_scg(admin,compartmentb,scg_compartmentb)
| ~ system_indi_is_oca(system,oca) ),
inference(resolution,[status(thm)],[f318,f190]) ).
fof(f320,plain,
admin_compartment_has_scg(admin,compartmentb,scg_compartmentb),
inference(forward_subsumption_resolution,[status(thm)],[f319,f186]) ).
fof(f321,plain,
! [X0,X1,X2,X3,X4,X5] :
( ~ admin_file_has_compartments_h(admin,X2,cons(X0,cons(X3,X4)),X4)
| ~ sso_file_has_compartments(X5,X2,cons(X0,cons(X3,X4)))
| ~ admin_compartment_has_sso(admin,X3,X5)
| admin_file_has_compartments(admin,X2,cons(X0,cons(X3,X4)))
| ~ system_file_needs_compartments(system,X2,cons(X0,cons(X3,X4)))
| ~ sso_file_has_compartments(X1,X2,cons(X0,cons(X3,X4)))
| ~ admin_compartment_has_sso(admin,X0,X1) ),
inference(resolution,[status(thm)],[f242,f108]) ).
fof(f323,plain,
( ~ admin_indi_has_compartments_for_file(admin,alice,secretfile)
| ~ admin_indi_has_level_for_file(admin,alice,secretfile)
| ~ admin_indi_has_need_to_know_for_file(admin,alice,secretfile) ),
inference(forward_subsumption_resolution,[status(thm)],[f317,f261]) ).
fof(f324,plain,
( ~ admin_indi_has_compartments_for_file(admin,alice,secretfile)
| ~ admin_indi_has_level_for_file(admin,alice,secretfile) ),
inference(resolution,[status(thm)],[f323,f278]) ).
fof(f325,plain,
! [X0,X1] :
( admin_indi_has_level(admin,alice,X1)
| ~ admin_indi_has_background(admin,alice,X1)
| ~ loca_level_below(admin,X1,topsecret)
| ~ system_indi_is_level_admin(system,level_admin)
| ~ loca_level_below(admin,X1,X0)
| ~ admin_indi_has_credit(admin,alice)
| ~ admin_indi_has_employment(admin,alice)
| ~ system_indi_needs_level(system,alice,X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f280,f256]) ).
fof(f326,plain,
! [X0] :
( admin_indi_has_level(admin,alice,X0)
| ~ admin_indi_has_background(admin,alice,X0)
| ~ loca_level_below(admin,X0,topsecret)
| ~ system_indi_is_level_admin(system,level_admin)
| ~ loca_level_below(admin,X0,secret)
| ~ admin_indi_has_credit(admin,alice)
| ~ admin_indi_has_employment(admin,alice) ),
inference(resolution,[status(thm)],[f325,f221]) ).
fof(f327,plain,
! [X0] :
( admin_indi_has_level(admin,alice,X0)
| ~ admin_indi_has_background(admin,alice,X0)
| ~ loca_level_below(admin,X0,topsecret)
| ~ system_indi_is_level_admin(system,level_admin)
| ~ loca_level_below(admin,X0,secret)
| ~ admin_indi_has_credit(admin,alice) ),
inference(forward_subsumption_resolution,[status(thm)],[f326,f267]) ).
fof(f328,plain,
! [X0] :
( admin_indi_has_level(admin,alice,X0)
| ~ admin_indi_has_background(admin,alice,X0)
| ~ loca_level_below(admin,X0,topsecret)
| ~ system_indi_is_level_admin(system,level_admin)
| ~ loca_level_below(admin,X0,secret) ),
inference(forward_subsumption_resolution,[status(thm)],[f327,f263]) ).
fof(f330,plain,
( admin_indi_has_level(admin,alice,sbu)
| ~ admin_indi_has_background(admin,alice,sbu)
| ~ system_indi_is_level_admin(system,level_admin)
| ~ loca_level_below(admin,sbu,secret) ),
inference(resolution,[status(thm)],[f328,f254]) ).
fof(f331,plain,
( admin_indi_has_level(admin,alice,confidential)
| ~ admin_indi_has_background(admin,alice,confidential)
| ~ system_indi_is_level_admin(system,level_admin)
| ~ loca_level_below(admin,confidential,secret) ),
inference(resolution,[status(thm)],[f328,f248]) ).
fof(f332,plain,
( admin_indi_has_level(admin,alice,secret)
| ~ admin_indi_has_background(admin,alice,secret)
| ~ system_indi_is_level_admin(system,level_admin)
| ~ loca_level_below(admin,secret,secret) ),
inference(resolution,[status(thm)],[f328,f246]) ).
fof(f339,plain,
( admin_indi_has_level(admin,alice,sbu)
| ~ admin_indi_has_background(admin,alice,sbu)
| ~ system_indi_is_level_admin(system,level_admin) ),
inference(forward_subsumption_resolution,[status(thm)],[f330,f253]) ).
fof(f340,plain,
( admin_indi_has_level(admin,alice,confidential)
| ~ admin_indi_has_background(admin,alice,confidential)
| ~ system_indi_is_level_admin(system,level_admin) ),
inference(forward_subsumption_resolution,[status(thm)],[f331,f247]) ).
fof(f341,plain,
( admin_indi_has_level(admin,alice,secret)
| ~ admin_indi_has_background(admin,alice,secret)
| ~ system_indi_is_level_admin(system,level_admin) ),
inference(forward_subsumption_resolution,[status(thm)],[f332,f94]) ).
fof(f347,plain,
( admin_indi_has_level(admin,alice,sbu)
| ~ admin_indi_has_background(admin,alice,sbu) ),
inference(forward_subsumption_resolution,[status(thm)],[f339,f215]) ).
fof(f348,plain,
admin_indi_has_level(admin,alice,sbu),
inference(resolution,[status(thm)],[f347,f270]) ).
fof(f349,plain,
admin_indi_has_level_for_compartment(admin,alice,compartmenta),
inference(resolution,[status(thm)],[f348,f289]) ).
fof(f350,plain,
( admin_indi_has_level(admin,alice,confidential)
| ~ admin_indi_has_background(admin,alice,confidential) ),
inference(forward_subsumption_resolution,[status(thm)],[f340,f215]) ).
fof(f351,plain,
admin_indi_has_level(admin,alice,confidential),
inference(resolution,[status(thm)],[f350,f271]) ).
fof(f352,plain,
admin_indi_has_level_for_compartment(admin,alice,compartmentb),
inference(resolution,[status(thm)],[f351,f290]) ).
fof(f353,plain,
( admin_indi_has_level(admin,alice,secret)
| ~ admin_indi_has_background(admin,alice,secret) ),
inference(forward_subsumption_resolution,[status(thm)],[f341,f215]) ).
fof(f354,plain,
admin_indi_has_level(admin,alice,secret),
inference(resolution,[status(thm)],[f353,f272]) ).
fof(f356,plain,
! [X0,X1,X2,X3,X4] :
( ~ sso_file_has_compartments(X4,X2,cons(X0,cons(X3,nil)))
| ~ admin_compartment_has_sso(admin,X3,X4)
| admin_file_has_compartments(admin,X2,cons(X0,cons(X3,nil)))
| ~ system_file_needs_compartments(system,X2,cons(X0,cons(X3,nil)))
| ~ sso_file_has_compartments(X1,X2,cons(X0,cons(X3,nil)))
| ~ admin_compartment_has_sso(admin,X0,X1) ),
inference(resolution,[status(thm)],[f321,f105]) ).
fof(f358,plain,
! [X0] :
( ~ admin_compartment_has_sso(admin,compartmenta,sso_compartmenta)
| admin_file_has_compartments(admin,secretfile,cons(compartmentb,cons(compartmenta,nil)))
| ~ system_file_needs_compartments(system,secretfile,cons(compartmentb,cons(compartmenta,nil)))
| ~ sso_file_has_compartments(X0,secretfile,cons(compartmentb,cons(compartmenta,nil)))
| ~ admin_compartment_has_sso(admin,compartmentb,X0) ),
inference(resolution,[status(thm)],[f356,f198]) ).
fof(f360,plain,
! [X0] :
( ~ admin_compartment_has_sso(admin,compartmenta,sso_compartmenta)
| admin_file_has_compartments(admin,secretfile,cons(compartmentb,cons(compartmenta,nil)))
| ~ sso_file_has_compartments(X0,secretfile,cons(compartmentb,cons(compartmenta,nil)))
| ~ admin_compartment_has_sso(admin,compartmentb,X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f358,f196]) ).
fof(f362,plain,
! [X0] :
( admin_file_has_compartments(admin,secretfile,cons(compartmentb,cons(compartmenta,nil)))
| ~ sso_file_has_compartments(X0,secretfile,cons(compartmentb,cons(compartmenta,nil)))
| ~ admin_compartment_has_sso(admin,compartmentb,X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f360,f237]) ).
fof(f364,plain,
( admin_file_has_compartments(admin,secretfile,cons(compartmentb,cons(compartmenta,nil)))
| ~ admin_compartment_has_sso(admin,compartmentb,sso_compartmentb) ),
inference(resolution,[status(thm)],[f362,f197]) ).
fof(f365,plain,
admin_file_has_compartments(admin,secretfile,cons(compartmentb,cons(compartmenta,nil))),
inference(forward_subsumption_resolution,[status(thm)],[f364,f238]) ).
fof(f366,plain,
! [X0,X1] :
( ~ admin_indi_has_compartments(admin,X0,cons(compartmenta,nil))
| ~ admin_indi_has_level_for_compartment(admin,X0,compartmentb)
| ~ admin_indi_has_background_for_compartment(admin,X0,compartmentb)
| ~ sso_indi_has_compartment(X1,X0,compartmentb)
| ~ admin_compartment_has_sso(admin,compartmentb,X1)
| ~ admin_indi_has_credit_for_compartment(admin,X0,compartmentb)
| ~ admin_indi_has_polygraph_for_compartment(admin,X0,compartmentb)
| ~ admin_indi_has_citizenship(admin,X0,usa)
| ~ admin_indi_has_employment(admin,X0)
| ~ system_indi_needs_compartment(system,X0,compartmentb)
| admin_indi_has_compartments_for_file(admin,X0,secretfile) ),
inference(resolution,[status(thm)],[f365,f291]) ).
fof(f368,plain,
! [X0,X1,X2] :
( admin_file_has_level(admin,secretfile,X2)
| ~ system_file_needs_level(system,secretfile,X2)
| ~ admin_file_has_level_h(admin,secretfile,X2,cons(compartmenta,nil))
| ~ sso_file_has_level(X0,secretfile,X2,X1)
| ~ admin_compartment_has_scg(admin,compartmentb,X1)
| ~ admin_compartment_has_sso(admin,compartmentb,X0) ),
inference(resolution,[status(thm)],[f365,f249]) ).
fof(f371,plain,
! [X0,X1,X2,X3,X4] :
( ~ admin_file_has_level_h(admin,secretfile,X2,nil)
| ~ sso_file_has_level(X3,secretfile,X2,X4)
| ~ admin_compartment_has_scg(admin,compartmenta,X4)
| ~ admin_compartment_has_sso(admin,compartmenta,X3)
| admin_file_has_level(admin,secretfile,X2)
| ~ system_file_needs_level(system,secretfile,X2)
| ~ sso_file_has_level(X0,secretfile,X2,X1)
| ~ admin_compartment_has_scg(admin,compartmentb,X1)
| ~ admin_compartment_has_sso(admin,compartmentb,X0) ),
inference(resolution,[status(thm)],[f368,f115]) ).
fof(f372,plain,
! [X0,X1,X2,X3,X4] :
( ~ sso_file_has_level(X3,secretfile,X2,X4)
| ~ admin_compartment_has_scg(admin,compartmenta,X4)
| ~ admin_compartment_has_sso(admin,compartmenta,X3)
| admin_file_has_level(admin,secretfile,X2)
| ~ system_file_needs_level(system,secretfile,X2)
| ~ sso_file_has_level(X0,secretfile,X2,X1)
| ~ admin_compartment_has_scg(admin,compartmentb,X1)
| ~ admin_compartment_has_sso(admin,compartmentb,X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f371,f112]) ).
fof(f390,plain,
! [X0,X1] :
( ~ admin_compartment_has_scg(admin,compartmenta,scg_compartmenta)
| ~ admin_compartment_has_sso(admin,compartmenta,sso_compartmenta)
| admin_file_has_level(admin,secretfile,secret)
| ~ system_file_needs_level(system,secretfile,secret)
| ~ sso_file_has_level(X0,secretfile,secret,X1)
| ~ admin_compartment_has_scg(admin,compartmentb,X1)
| ~ admin_compartment_has_sso(admin,compartmentb,X0) ),
inference(resolution,[status(thm)],[f372,f201]) ).
fof(f392,plain,
! [X0,X1] :
( ~ admin_compartment_has_scg(admin,compartmenta,scg_compartmenta)
| ~ admin_compartment_has_sso(admin,compartmenta,sso_compartmenta)
| admin_file_has_level(admin,secretfile,secret)
| ~ sso_file_has_level(X0,secretfile,secret,X1)
| ~ admin_compartment_has_scg(admin,compartmentb,X1)
| ~ admin_compartment_has_sso(admin,compartmentb,X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f390,f199]) ).
fof(f394,plain,
! [X0,X1] :
( ~ admin_compartment_has_scg(admin,compartmenta,scg_compartmenta)
| admin_file_has_level(admin,secretfile,secret)
| ~ sso_file_has_level(X0,secretfile,secret,X1)
| ~ admin_compartment_has_scg(admin,compartmentb,X1)
| ~ admin_compartment_has_sso(admin,compartmentb,X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f392,f237]) ).
fof(f396,plain,
( ~ admin_compartment_has_scg(admin,compartmenta,scg_compartmenta)
| admin_file_has_level(admin,secretfile,secret)
| ~ admin_compartment_has_scg(admin,compartmentb,scg_compartmentb)
| ~ admin_compartment_has_sso(admin,compartmentb,sso_compartmentb) ),
inference(resolution,[status(thm)],[f394,f200]) ).
fof(f398,plain,
( ~ admin_compartment_has_scg(admin,compartmenta,scg_compartmenta)
| admin_file_has_level(admin,secretfile,secret)
| ~ admin_compartment_has_scg(admin,compartmentb,scg_compartmentb) ),
inference(forward_subsumption_resolution,[status(thm)],[f396,f238]) ).
fof(f401,plain,
( ~ admin_compartment_has_scg(admin,compartmenta,scg_compartmenta)
| admin_file_has_level(admin,secretfile,secret) ),
inference(forward_subsumption_resolution,[status(thm)],[f398,f320]) ).
fof(f402,plain,
admin_file_has_level(admin,secretfile,secret),
inference(resolution,[status(thm)],[f401,f315]) ).
fof(f403,plain,
! [X0] :
( admin_indi_has_level_for_file(admin,X0,secretfile)
| ~ admin_indi_has_level(admin,X0,secret) ),
inference(resolution,[status(thm)],[f402,f170]) ).
fof(f404,plain,
admin_indi_has_level_for_file(admin,alice,secretfile),
inference(resolution,[status(thm)],[f403,f354]) ).
fof(f405,plain,
~ admin_indi_has_compartments_for_file(admin,alice,secretfile),
inference(backward_subsumption_resolution,[status(thm)],[f324,f404]) ).
fof(f406,plain,
! [X0,X1,X2] :
( ~ admin_indi_has_compartments(admin,X0,nil)
| ~ admin_indi_has_level_for_compartment(admin,X0,compartmenta)
| ~ admin_indi_has_background_for_compartment(admin,X0,compartmenta)
| ~ sso_indi_has_compartment(X2,X0,compartmenta)
| ~ admin_compartment_has_sso(admin,compartmenta,X2)
| ~ admin_indi_has_credit_for_compartment(admin,X0,compartmenta)
| ~ admin_indi_has_polygraph_for_compartment(admin,X0,compartmenta)
| ~ admin_indi_has_citizenship(admin,X0,usa)
| ~ admin_indi_has_employment(admin,X0)
| ~ system_indi_needs_compartment(system,X0,compartmenta)
| ~ admin_indi_has_level_for_compartment(admin,X0,compartmentb)
| ~ admin_indi_has_background_for_compartment(admin,X0,compartmentb)
| ~ sso_indi_has_compartment(X1,X0,compartmentb)
| ~ admin_compartment_has_sso(admin,compartmentb,X1)
| ~ admin_indi_has_credit_for_compartment(admin,X0,compartmentb)
| ~ admin_indi_has_polygraph_for_compartment(admin,X0,compartmentb)
| ~ admin_indi_has_citizenship(admin,X0,usa)
| ~ admin_indi_has_employment(admin,X0)
| ~ system_indi_needs_compartment(system,X0,compartmentb)
| admin_indi_has_compartments_for_file(admin,X0,secretfile) ),
inference(resolution,[status(thm)],[f366,f146]) ).
fof(f407,plain,
! [X0,X1,X2] :
( ~ admin_indi_has_compartments(admin,X0,nil)
| ~ admin_indi_has_level_for_compartment(admin,X0,compartmenta)
| ~ admin_indi_has_background_for_compartment(admin,X0,compartmenta)
| ~ sso_indi_has_compartment(X2,X0,compartmenta)
| ~ admin_compartment_has_sso(admin,compartmenta,X2)
| ~ admin_indi_has_credit_for_compartment(admin,X0,compartmenta)
| ~ admin_indi_has_polygraph_for_compartment(admin,X0,compartmenta)
| ~ system_indi_needs_compartment(system,X0,compartmenta)
| ~ admin_indi_has_level_for_compartment(admin,X0,compartmentb)
| ~ admin_indi_has_background_for_compartment(admin,X0,compartmentb)
| ~ sso_indi_has_compartment(X1,X0,compartmentb)
| ~ admin_compartment_has_sso(admin,compartmentb,X1)
| ~ admin_indi_has_credit_for_compartment(admin,X0,compartmentb)
| ~ admin_indi_has_polygraph_for_compartment(admin,X0,compartmentb)
| ~ admin_indi_has_citizenship(admin,X0,usa)
| ~ admin_indi_has_employment(admin,X0)
| ~ system_indi_needs_compartment(system,X0,compartmentb)
| admin_indi_has_compartments_for_file(admin,X0,secretfile) ),
inference(duplicate_literals_removal,[status(thm)],[f406]) ).
fof(f408,plain,
! [X0,X1,X2] :
( ~ admin_indi_has_compartments(admin,X0,nil)
| ~ admin_indi_has_level_for_compartment(admin,X0,compartmenta)
| ~ admin_indi_has_background_for_compartment(admin,X0,compartmenta)
| ~ sso_indi_has_compartment(X2,X0,compartmenta)
| ~ admin_compartment_has_sso(admin,compartmenta,X2)
| ~ admin_indi_has_credit_for_compartment(admin,X0,compartmenta)
| ~ system_indi_needs_compartment(system,X0,compartmenta)
| ~ admin_indi_has_level_for_compartment(admin,X0,compartmentb)
| ~ admin_indi_has_background_for_compartment(admin,X0,compartmentb)
| ~ sso_indi_has_compartment(X1,X0,compartmentb)
| ~ admin_compartment_has_sso(admin,compartmentb,X1)
| ~ admin_indi_has_credit_for_compartment(admin,X0,compartmentb)
| ~ admin_indi_has_polygraph_for_compartment(admin,X0,compartmentb)
| ~ admin_indi_has_citizenship(admin,X0,usa)
| ~ admin_indi_has_employment(admin,X0)
| ~ system_indi_needs_compartment(system,X0,compartmentb)
| admin_indi_has_compartments_for_file(admin,X0,secretfile) ),
inference(forward_subsumption_resolution,[status(thm)],[f407,f301]) ).
fof(f409,plain,
! [X0,X1,X2] :
( ~ admin_indi_has_compartments(admin,X0,nil)
| ~ admin_indi_has_level_for_compartment(admin,X0,compartmenta)
| ~ admin_indi_has_background_for_compartment(admin,X0,compartmenta)
| ~ sso_indi_has_compartment(X2,X0,compartmenta)
| ~ admin_compartment_has_sso(admin,compartmenta,X2)
| ~ system_indi_needs_compartment(system,X0,compartmenta)
| ~ admin_indi_has_level_for_compartment(admin,X0,compartmentb)
| ~ admin_indi_has_background_for_compartment(admin,X0,compartmentb)
| ~ sso_indi_has_compartment(X1,X0,compartmentb)
| ~ admin_compartment_has_sso(admin,compartmentb,X1)
| ~ admin_indi_has_credit_for_compartment(admin,X0,compartmentb)
| ~ admin_indi_has_polygraph_for_compartment(admin,X0,compartmentb)
| ~ admin_indi_has_citizenship(admin,X0,usa)
| ~ admin_indi_has_employment(admin,X0)
| ~ system_indi_needs_compartment(system,X0,compartmentb)
| admin_indi_has_compartments_for_file(admin,X0,secretfile) ),
inference(forward_subsumption_resolution,[status(thm)],[f408,f310]) ).
fof(f413,plain,
! [X0,X1] :
( ~ admin_indi_has_compartments(admin,alice,nil)
| ~ admin_indi_has_level_for_compartment(admin,alice,compartmenta)
| ~ admin_indi_has_background_for_compartment(admin,alice,compartmenta)
| ~ sso_indi_has_compartment(X1,alice,compartmenta)
| ~ admin_compartment_has_sso(admin,compartmenta,X1)
| ~ system_indi_needs_compartment(system,alice,compartmenta)
| ~ admin_indi_has_level_for_compartment(admin,alice,compartmentb)
| ~ sso_indi_has_compartment(X0,alice,compartmentb)
| ~ admin_compartment_has_sso(admin,compartmentb,X0)
| ~ 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)
| ~ admin_indi_has_employment(admin,alice)
| ~ system_indi_needs_compartment(system,alice,compartmentb)
| admin_indi_has_compartments_for_file(admin,alice,secretfile) ),
inference(resolution,[status(thm)],[f409,f286]) ).
fof(f422,plain,
! [X0,X1] :
( ~ admin_indi_has_compartments(admin,alice,nil)
| ~ admin_indi_has_level_for_compartment(admin,alice,compartmenta)
| ~ admin_indi_has_background_for_compartment(admin,alice,compartmenta)
| ~ sso_indi_has_compartment(X1,alice,compartmenta)
| ~ admin_compartment_has_sso(admin,compartmenta,X1)
| ~ system_indi_needs_compartment(system,alice,compartmenta)
| ~ admin_indi_has_level_for_compartment(admin,alice,compartmentb)
| ~ sso_indi_has_compartment(X0,alice,compartmentb)
| ~ admin_compartment_has_sso(admin,compartmentb,X0)
| ~ 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)
| ~ admin_indi_has_employment(admin,alice)
| ~ system_indi_needs_compartment(system,alice,compartmentb) ),
inference(forward_subsumption_resolution,[status(thm)],[f413,f405]) ).
fof(f447,plain,
! [X0,X1] :
( ~ admin_indi_has_compartments(admin,alice,nil)
| ~ admin_indi_has_level_for_compartment(admin,alice,compartmenta)
| ~ admin_indi_has_background_for_compartment(admin,alice,compartmenta)
| ~ sso_indi_has_compartment(X1,alice,compartmenta)
| ~ admin_compartment_has_sso(admin,compartmenta,X1)
| ~ system_indi_needs_compartment(system,alice,compartmenta)
| ~ admin_indi_has_level_for_compartment(admin,alice,compartmentb)
| ~ sso_indi_has_compartment(X0,alice,compartmentb)
| ~ admin_compartment_has_sso(admin,compartmentb,X0)
| ~ 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)
| ~ admin_indi_has_employment(admin,alice) ),
inference(forward_subsumption_resolution,[status(thm)],[f422,f223]) ).
fof(f451,plain,
! [X0,X1] :
( ~ admin_indi_has_compartments(admin,alice,nil)
| ~ admin_indi_has_level_for_compartment(admin,alice,compartmenta)
| ~ admin_indi_has_background_for_compartment(admin,alice,compartmenta)
| ~ sso_indi_has_compartment(X1,alice,compartmenta)
| ~ admin_compartment_has_sso(admin,compartmenta,X1)
| ~ system_indi_needs_compartment(system,alice,compartmenta)
| ~ sso_indi_has_compartment(X0,alice,compartmentb)
| ~ admin_compartment_has_sso(admin,compartmentb,X0)
| ~ 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)
| ~ admin_indi_has_employment(admin,alice) ),
inference(resolution,[status(thm)],[f447,f352]) ).
fof(f460,plain,
! [X0,X1] :
( ~ admin_indi_has_compartments(admin,alice,nil)
| ~ admin_indi_has_level_for_compartment(admin,alice,compartmenta)
| ~ admin_indi_has_background_for_compartment(admin,alice,compartmenta)
| ~ sso_indi_has_compartment(X1,alice,compartmenta)
| ~ admin_compartment_has_sso(admin,compartmenta,X1)
| ~ system_indi_needs_compartment(system,alice,compartmenta)
| ~ sso_indi_has_compartment(X0,alice,compartmentb)
| ~ admin_compartment_has_sso(admin,compartmentb,X0)
| ~ 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) ),
inference(forward_subsumption_resolution,[status(thm)],[f451,f267]) ).
fof(f466,plain,
! [X0,X1] :
( ~ admin_indi_has_compartments(admin,alice,nil)
| ~ admin_indi_has_level_for_compartment(admin,alice,compartmenta)
| ~ admin_indi_has_background_for_compartment(admin,alice,compartmenta)
| ~ sso_indi_has_compartment(X1,alice,compartmenta)
| ~ admin_compartment_has_sso(admin,compartmenta,X1)
| ~ system_indi_needs_compartment(system,alice,compartmenta)
| ~ sso_indi_has_compartment(X0,alice,compartmentb)
| ~ admin_compartment_has_sso(admin,compartmentb,X0)
| ~ admin_indi_has_credit_for_compartment(admin,alice,compartmentb)
| ~ admin_indi_has_polygraph_for_compartment(admin,alice,compartmentb) ),
inference(forward_subsumption_resolution,[status(thm)],[f460,f245]) ).
fof(f470,plain,
! [X0,X1] :
( ~ admin_indi_has_compartments(admin,alice,nil)
| ~ admin_indi_has_level_for_compartment(admin,alice,compartmenta)
| ~ sso_indi_has_compartment(X1,alice,compartmenta)
| ~ admin_compartment_has_sso(admin,compartmenta,X1)
| ~ system_indi_needs_compartment(system,alice,compartmenta)
| ~ sso_indi_has_compartment(X0,alice,compartmentb)
| ~ admin_compartment_has_sso(admin,compartmentb,X0)
| ~ admin_indi_has_credit_for_compartment(admin,alice,compartmentb)
| ~ admin_indi_has_polygraph_for_compartment(admin,alice,compartmentb) ),
inference(resolution,[status(thm)],[f466,f285]) ).
fof(f475,plain,
! [X0,X1] :
( ~ admin_indi_has_compartments(admin,alice,nil)
| ~ admin_indi_has_level_for_compartment(admin,alice,compartmenta)
| ~ sso_indi_has_compartment(X1,alice,compartmenta)
| ~ admin_compartment_has_sso(admin,compartmenta,X1)
| ~ sso_indi_has_compartment(X0,alice,compartmentb)
| ~ admin_compartment_has_sso(admin,compartmentb,X0)
| ~ admin_indi_has_credit_for_compartment(admin,alice,compartmentb)
| ~ admin_indi_has_polygraph_for_compartment(admin,alice,compartmentb) ),
inference(forward_subsumption_resolution,[status(thm)],[f470,f224]) ).
fof(f477,plain,
! [X0,X1] :
( ~ admin_indi_has_compartments(admin,alice,nil)
| ~ sso_indi_has_compartment(X1,alice,compartmenta)
| ~ admin_compartment_has_sso(admin,compartmenta,X1)
| ~ sso_indi_has_compartment(X0,alice,compartmentb)
| ~ admin_compartment_has_sso(admin,compartmentb,X0)
| ~ admin_indi_has_credit_for_compartment(admin,alice,compartmentb)
| ~ admin_indi_has_polygraph_for_compartment(admin,alice,compartmentb) ),
inference(forward_subsumption_resolution,[status(thm)],[f475,f349]) ).
fof(f479,plain,
! [X0] :
( ~ admin_indi_has_compartments(admin,alice,nil)
| ~ sso_indi_has_compartment(X0,alice,compartmenta)
| ~ admin_compartment_has_sso(admin,compartmenta,X0)
| ~ admin_compartment_has_sso(admin,compartmentb,sso_compartmentb)
| ~ admin_indi_has_credit_for_compartment(admin,alice,compartmentb)
| ~ admin_indi_has_polygraph_for_compartment(admin,alice,compartmentb) ),
inference(resolution,[status(thm)],[f477,f225]) ).
fof(f482,plain,
! [X0] :
( ~ admin_indi_has_compartments(admin,alice,nil)
| ~ sso_indi_has_compartment(X0,alice,compartmenta)
| ~ admin_compartment_has_sso(admin,compartmenta,X0)
| ~ admin_indi_has_credit_for_compartment(admin,alice,compartmentb)
| ~ admin_indi_has_polygraph_for_compartment(admin,alice,compartmentb) ),
inference(forward_subsumption_resolution,[status(thm)],[f479,f238]) ).
fof(f484,plain,
! [X0] :
( ~ sso_indi_has_compartment(X0,alice,compartmenta)
| ~ admin_compartment_has_sso(admin,compartmenta,X0)
| ~ admin_indi_has_credit_for_compartment(admin,alice,compartmentb)
| ~ admin_indi_has_polygraph_for_compartment(admin,alice,compartmentb) ),
inference(forward_subsumption_resolution,[status(thm)],[f482,f143]) ).
fof(f486,plain,
( ~ admin_compartment_has_sso(admin,compartmenta,sso_compartmenta)
| ~ admin_indi_has_credit_for_compartment(admin,alice,compartmentb)
| ~ admin_indi_has_polygraph_for_compartment(admin,alice,compartmentb) ),
inference(resolution,[status(thm)],[f484,f226]) ).
fof(f488,plain,
( ~ admin_indi_has_credit_for_compartment(admin,alice,compartmentb)
| ~ admin_indi_has_polygraph_for_compartment(admin,alice,compartmentb) ),
inference(forward_subsumption_resolution,[status(thm)],[f486,f237]) ).
fof(f489,plain,
( ~ admin_indi_has_credit(admin,alice)
| ~ admin_indi_has_polygraph_for_compartment(admin,alice,compartmentb) ),
inference(resolution,[status(thm)],[f488,f312]) ).
fof(f490,plain,
~ admin_indi_has_polygraph_for_compartment(admin,alice,compartmentb),
inference(forward_subsumption_resolution,[status(thm)],[f489,f263]) ).
fof(f491,plain,
~ admin_indi_has_polygraph(admin,alice),
inference(resolution,[status(thm)],[f490,f299]) ).
fof(f492,plain,
$false,
inference(forward_subsumption_resolution,[status(thm)],[f491,f256]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWV437+1 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.10/0.36 % Computer : n026.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 : Mon Sep 21 08:54:38 UTC 2026
% 0.10/0.36 % CPUTime :
% 0.10/0.37 % Drodi V4.1.1
% 0.10/0.40 % Refutation found
% 0.10/0.40 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.10/0.40 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 0.10/0.44 % Elapsed time: 0.062923 seconds
% 0.10/0.44 % CPU time: 0.210615 seconds
% 0.10/0.44 % Total memory used: 57.862 MB
% 0.10/0.44 % Net memory used: 57.762 MB
%------------------------------------------------------------------------------