%------------------------------------------------------------------------------
% File : hopCoP---0.1
% Problem : SWV437+1 : TPTP v9.0.0. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : /export/starexec/sandbox2/solver/bin/execute.py 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n022.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Fri Jul 25 04:47:00 PM UTC 2025
% Result : Theorem 0.11s 0.32s
% Output : CNFRefutation 0.11s
% Verified :
% SZS Type : Refutation
% Derivation depth : 4
% Number of leaves : 74
% Syntax : Number of formulae : 389 ( 244 unt; 0 def)
% Number of atoms : 796 ( 0 equ)
% Maximal formula atoms : 11 ( 2 avg)
% Number of connectives : 732 ( 325 ~; 322 |; 0 &)
% ( 0 <=>; 85 =>; 0 <=; 0 <~>)
% Maximal formula depth : 16 ( 3 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 55 ( 54 usr; 1 prp; 0-6 aty)
% Number of functors : 28 ( 28 usr; 27 con; 0-2 aty)
% Number of variables : 242 ( 32 sgn 121 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(alicereadsecret,plain,
admin_indi_may_file(admin,alice,secretfile,read),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',alicereadsecret) ).
fof(alicereadsecret_negated,plain,
~ admin_indi_may_file(admin,alice,secretfile,read),
inference(negate_conjecture,[status(cth)],[alicereadsecret]) ).
cnf(87,plain,
~ admin_indi_may_file(admin,alice,secretfile,read),
inference(cnf,[status(esa)],[alicereadsecret_negated]) ).
cnf(l0,plain,
~ admin_indi_may_file(admin,alice,secretfile,read),
inference(instantiation,[status(thm)],[87]) ).
fof(ax39,plain,
! [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('Axioms/SWV009+0.ax',ax39) ).
cnf(39,plain,
( ~ admin_indi_has_citizenship_for_file(admin,X0,X1)
| ~ admin_indi_has_need_to_know_for_file(admin,X0,X1)
| ~ admin_indi_has_compartments_for_file(admin,X0,X1)
| ~ admin_indi_has_level_for_file(admin,X0,X1)
| ~ state_file_is_not_working_paper(X1)
| admin_indi_may_file(admin,X0,X1,read) ),
inference(cnf,[status(esa)],[ax39]) ).
cnf(l1,plain,
( ~ admin_indi_has_citizenship_for_file(admin,alice,secretfile)
| ~ admin_indi_has_need_to_know_for_file(admin,alice,secretfile)
| ~ admin_indi_has_compartments_for_file(admin,alice,secretfile)
| ~ admin_indi_has_level_for_file(admin,alice,secretfile)
| ~ state_file_is_not_working_paper(secretfile)
| admin_indi_may_file(admin,alice,secretfile,read) ),
inference(instantiation,[status(thm)],[39]) ).
fof(ax37,plain,
! [K,F,L] :
( admin_file_has_citizenship(admin,F,L)
=> ( admin_indi_has_citizenship(admin,K,L)
=> admin_indi_has_citizenship_for_file(admin,K,F) ) ),
file('Axioms/SWV009+0.ax',ax37) ).
cnf(37,plain,
( ~ admin_file_has_citizenship(admin,X0,X1)
| ~ admin_indi_has_citizenship(admin,X2,X1)
| admin_indi_has_citizenship_for_file(admin,X2,X0) ),
inference(cnf,[status(esa)],[ax37]) ).
cnf(l2,plain,
( ~ admin_file_has_citizenship(admin,secretfile,usa)
| ~ admin_indi_has_citizenship(admin,alice,usa)
| admin_indi_has_citizenship_for_file(admin,alice,secretfile) ),
inference(instantiation,[status(thm)],[37]) ).
fof(ax35,plain,
! [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('Axioms/SWV009+0.ax',ax35) ).
cnf(35,plain,
( ~ admin_file_has_level(admin,X0,X1)
| ~ admin_indi_has_level(admin,X2,X1)
| admin_indi_has_level_for_file(admin,X2,X0) ),
inference(cnf,[status(esa)],[ax35]) ).
cnf(l4,plain,
( ~ admin_file_has_level(admin,secretfile,secret)
| ~ admin_indi_has_level(admin,alice,secret)
| admin_indi_has_level_for_file(admin,alice,secretfile) ),
inference(instantiation,[status(thm)],[35]) ).
fof(ax34,plain,
! [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('Axioms/SWV009+0.ax',ax34) ).
cnf(34,plain,
( ~ admin_file_has_compartments(admin,X0,X1)
| ~ admin_indi_has_compartments(admin,X2,X1)
| admin_indi_has_compartments_for_file(admin,X2,X0) ),
inference(cnf,[status(esa)],[ax34]) ).
cnf(l5,plain,
( ~ admin_file_has_compartments(admin,secretfile,cons(compartmentb,cons(compartmenta,nil)))
| ~ admin_indi_has_compartments(admin,alice,cons(compartmentb,cons(compartmenta,nil)))
| admin_indi_has_compartments_for_file(admin,alice,secretfile) ),
inference(instantiation,[status(thm)],[34]) ).
fof(ax25,plain,
! [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('Axioms/SWV009+0.ax',ax25) ).
cnf(25,plain,
( ~ loca_level_below(admin,X0,X1)
| ~ loca_level_below(admin,X0,X2)
| ~ admin_indi_has_background(admin,X3,X0)
| ~ system_indi_is_level_admin(system,X4)
| ~ admin_indi_has_polygraph(admin,X3)
| ~ admin_indi_has_employment(admin,X3)
| ~ admin_indi_has_credit(admin,X3)
| ~ admin_indi_has_citizenship(admin,X3,usa)
| ~ level_admin_indi_has_level(X4,X3,X2)
| ~ system_indi_needs_level(system,X3,X1)
| admin_indi_has_level(admin,X3,X0) ),
inference(cnf,[status(esa)],[ax25]) ).
cnf(l6,plain,
( ~ loca_level_below(admin,secret,secret)
| ~ loca_level_below(admin,secret,topsecret)
| ~ admin_indi_has_background(admin,alice,secret)
| ~ system_indi_is_level_admin(system,level_admin)
| ~ admin_indi_has_polygraph(admin,alice)
| ~ admin_indi_has_employment(admin,alice)
| ~ admin_indi_has_credit(admin,alice)
| ~ admin_indi_has_citizenship(admin,alice,usa)
| ~ level_admin_indi_has_level(level_admin,alice,topsecret)
| ~ system_indi_needs_level(system,alice,secret)
| admin_indi_has_level(admin,alice,secret) ),
inference(instantiation,[status(thm)],[25]) ).
fof(ax4,plain,
! [K,L] : loca_level_below(K,L,L),
file('Axioms/SWV009+0.ax',ax4) ).
cnf(4,plain,
loca_level_below(X0,X1,X1),
inference(cnf,[status(esa)],[ax4]) ).
cnf(l7,plain,
loca_level_below(admin,secret,secret),
inference(instantiation,[status(thm)],[4]) ).
fof(ax70,plain,
system_indi_is_level_admin(system,level_admin),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax70) ).
cnf(70,plain,
system_indi_is_level_admin(system,level_admin),
inference(cnf,[status(esa)],[ax70]) ).
cnf(l8,plain,
system_indi_is_level_admin(system,level_admin),
inference(instantiation,[status(thm)],[70]) ).
fof(ax50,plain,
state_file_is_not_working_paper(secretfile),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax50) ).
cnf(50,plain,
state_file_is_not_working_paper(secretfile),
inference(cnf,[status(esa)],[ax50]) ).
cnf(l9,plain,
state_file_is_not_working_paper(secretfile),
inference(instantiation,[status(thm)],[50]) ).
fof(ax14,plain,
! [F,U,CL] :
( system_file_needs_citizenship(system,F,U)
=> ( admin_file_has_compartments(admin,F,CL)
=> ( admin_file_has_citizenship_h(admin,F,U,CL)
=> admin_file_has_citizenship(admin,F,U) ) ) ),
file('Axioms/SWV009+0.ax',ax14) ).
cnf(14,plain,
( ~ admin_file_has_compartments(admin,X0,X1)
| ~ system_file_needs_citizenship(system,X0,X2)
| ~ admin_file_has_citizenship_h(admin,X0,X2,X1)
| admin_file_has_citizenship(admin,X0,X2) ),
inference(cnf,[status(esa)],[ax14]) ).
cnf(l10,plain,
( ~ admin_file_has_compartments(admin,secretfile,cons(compartmentb,cons(compartmenta,nil)))
| ~ system_file_needs_citizenship(system,secretfile,usa)
| ~ admin_file_has_citizenship_h(admin,secretfile,usa,cons(compartmentb,cons(compartmenta,nil)))
| admin_file_has_citizenship(admin,secretfile,usa) ),
inference(instantiation,[status(thm)],[14]) ).
fof(ax8,plain,
! [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('Axioms/SWV009+0.ax',ax8) ).
cnf(8,plain,
( ~ admin_file_has_compartments_h(admin,X0,X1,X1)
| ~ system_file_needs_compartments(system,X0,X1)
| admin_file_has_compartments(admin,X0,X1) ),
inference(cnf,[status(esa)],[ax8]) ).
cnf(l11,plain,
( ~ admin_file_has_compartments_h(admin,secretfile,cons(compartmentb,cons(compartmenta,nil)),cons(compartmentb,cons(compartmenta,nil)))
| ~ system_file_needs_compartments(system,secretfile,cons(compartmentb,cons(compartmenta,nil)))
| admin_file_has_compartments(admin,secretfile,cons(compartmentb,cons(compartmenta,nil))) ),
inference(instantiation,[status(thm)],[8]) ).
fof(ax5,plain,
! [K,L,L1,L11] :
( loca_level_direct_below(K,L1,L11)
=> ( loca_level_below(K,L,L1)
=> loca_level_below(K,L,L11) ) ),
file('Axioms/SWV009+0.ax',ax5) ).
cnf(5,plain,
( ~ loca_level_direct_below(X0,X1,X2)
| ~ loca_level_below(X0,X3,X1)
| loca_level_below(X0,X3,X2) ),
inference(cnf,[status(esa)],[ax5]) ).
cnf(l12,plain,
( ~ loca_level_direct_below(admin,secret,topsecret)
| ~ loca_level_below(admin,secret,secret)
| loca_level_below(admin,secret,topsecret) ),
inference(instantiation,[status(thm)],[5]) ).
fof(ax23,plain,
! [K,U] :
( system_indi_has_citizenship(system,K,U)
=> admin_indi_has_citizenship(admin,K,U) ),
file('Axioms/SWV009+0.ax',ax23) ).
cnf(23,plain,
( ~ system_indi_has_citizenship(system,X0,X1)
| admin_indi_has_citizenship(admin,X0,X1) ),
inference(cnf,[status(esa)],[ax23]) ).
cnf(l13,plain,
( ~ system_indi_has_citizenship(system,alice,usa)
| admin_indi_has_citizenship(admin,alice,usa) ),
inference(instantiation,[status(thm)],[23]) ).
cnf(l14,plain,
( ~ admin_file_has_compartments_h(admin,secretfile,cons(compartmentb,cons(compartmenta,nil)),cons(compartmentb,cons(compartmenta,nil)))
| ~ system_file_needs_compartments(system,secretfile,cons(compartmentb,cons(compartmenta,nil)))
| admin_file_has_compartments(admin,secretfile,cons(compartmentb,cons(compartmenta,nil))) ),
inference(instantiation,[status(thm)],[8]) ).
cnf(l15,plain,
( ~ system_indi_has_citizenship(system,alice,usa)
| admin_indi_has_citizenship(admin,alice,usa) ),
inference(instantiation,[status(thm)],[23]) ).
fof(ax18,plain,
! [K,CA] :
( system_indi_is_credit_admin(system,CA)
=> ( credit_admin_indi_has_credit(CA,K)
=> admin_indi_has_credit(admin,K) ) ),
file('Axioms/SWV009+0.ax',ax18) ).
cnf(18,plain,
( ~ system_indi_is_credit_admin(system,X0)
| ~ credit_admin_indi_has_credit(X0,X1)
| admin_indi_has_credit(admin,X1) ),
inference(cnf,[status(esa)],[ax18]) ).
cnf(l16,plain,
( ~ system_indi_is_credit_admin(system,credit_admin)
| ~ credit_admin_indi_has_credit(credit_admin,alice)
| admin_indi_has_credit(admin,alice) ),
inference(instantiation,[status(thm)],[18]) ).
fof(ax17,plain,
! [K,PA] :
( system_indi_is_polygraph_admin(system,PA)
=> ( polygraph_admin_indi_has_polygraph(PA,K)
=> admin_indi_has_polygraph(admin,K) ) ),
file('Axioms/SWV009+0.ax',ax17) ).
cnf(17,plain,
( ~ system_indi_is_polygraph_admin(system,X0)
| ~ polygraph_admin_indi_has_polygraph(X0,X1)
| admin_indi_has_polygraph(admin,X1) ),
inference(cnf,[status(esa)],[ax17]) ).
cnf(l17,plain,
( ~ system_indi_is_polygraph_admin(system,polygraph_admin)
| ~ polygraph_admin_indi_has_polygraph(polygraph_admin,alice)
| admin_indi_has_polygraph(admin,alice) ),
inference(instantiation,[status(thm)],[17]) ).
fof(ax57,plain,
system_file_needs_citizenship(system,secretfile,usa),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax57) ).
cnf(57,plain,
system_file_needs_citizenship(system,secretfile,usa),
inference(cnf,[status(esa)],[ax57]) ).
cnf(l20,plain,
system_file_needs_citizenship(system,secretfile,usa),
inference(instantiation,[status(thm)],[57]) ).
fof(ax77,plain,
level_admin_indi_has_level(level_admin,alice,topsecret),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax77) ).
cnf(77,plain,
level_admin_indi_has_level(level_admin,alice,topsecret),
inference(cnf,[status(esa)],[ax77]) ).
cnf(l27,plain,
level_admin_indi_has_level(level_admin,alice,topsecret),
inference(instantiation,[status(thm)],[77]) ).
fof(ax67,plain,
system_indi_is_credit_admin(system,credit_admin),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax67) ).
cnf(67,plain,
system_indi_is_credit_admin(system,credit_admin),
inference(cnf,[status(esa)],[ax67]) ).
cnf(l25,plain,
system_indi_is_credit_admin(system,credit_admin),
inference(instantiation,[status(thm)],[67]) ).
cnf(l28,plain,
loca_level_below(admin,secret,secret),
inference(instantiation,[status(thm)],[4]) ).
fof(ax3,plain,
! [K] : loca_level_direct_below(K,secret,topsecret),
file('Axioms/SWV009+0.ax',ax3) ).
cnf(3,plain,
loca_level_direct_below(X0,secret,topsecret),
inference(cnf,[status(esa)],[ax3]) ).
cnf(l18,plain,
loca_level_direct_below(admin,secret,topsecret),
inference(instantiation,[status(thm)],[3]) ).
fof(ax51,plain,
system_file_needs_compartments(system,secretfile,cons(compartmentb,cons(compartmenta,nil))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax51) ).
cnf(51,plain,
system_file_needs_compartments(system,secretfile,cons(compartmentb,cons(compartmenta,nil))),
inference(cnf,[status(esa)],[ax51]) ).
cnf(l81,plain,
system_file_needs_compartments(system,secretfile,cons(compartmentb,cons(compartmenta,nil))),
inference(instantiation,[status(thm)],[51]) ).
fof(ax36,plain,
! [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('Axioms/SWV009+0.ax',ax36) ).
cnf(36,plain,
( ~ state_file_has_owner(X0,X1)
| ~ owner_indi_has_need_to_know(X1,X2,X0)
| admin_indi_has_need_to_know_for_file(admin,X2,X0) ),
inference(cnf,[status(esa)],[ax36]) ).
cnf(l3,plain,
( ~ state_file_has_owner(secretfile,owner_secretfile)
| ~ owner_indi_has_need_to_know(owner_secretfile,alice,secretfile)
| admin_indi_has_need_to_know_for_file(admin,alice,secretfile) ),
inference(instantiation,[status(thm)],[36]) ).
fof(ax10,plain,
! [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('Axioms/SWV009+0.ax',ax10) ).
cnf(10,plain,
( ~ admin_compartment_has_sso(admin,X0,X1)
| ~ admin_file_has_compartments_h(admin,X2,X3,X4)
| ~ sso_file_has_compartments(X1,X2,X3)
| admin_file_has_compartments_h(admin,X2,X3,cons(X0,X4)) ),
inference(cnf,[status(esa)],[ax10]) ).
cnf(l31,plain,
( ~ admin_compartment_has_sso(admin,compartmentb,sso_compartmentb)
| ~ admin_file_has_compartments_h(admin,secretfile,cons(compartmentb,cons(compartmenta,nil)),cons(compartmenta,nil))
| ~ sso_file_has_compartments(sso_compartmentb,secretfile,cons(compartmentb,cons(compartmenta,nil)))
| admin_file_has_compartments_h(admin,secretfile,cons(compartmentb,cons(compartmenta,nil)),cons(compartmentb,cons(compartmenta,nil))) ),
inference(instantiation,[status(thm)],[10]) ).
fof(ax76,plain,
system_indi_needs_level(system,alice,secret),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax76) ).
cnf(76,plain,
system_indi_needs_level(system,alice,secret),
inference(cnf,[status(esa)],[ax76]) ).
cnf(l73,plain,
system_indi_needs_level(system,alice,secret),
inference(instantiation,[status(thm)],[76]) ).
fof(ax82,plain,
owner_indi_has_need_to_know(owner_secretfile,alice,secretfile),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax82) ).
cnf(82,plain,
owner_indi_has_need_to_know(owner_secretfile,alice,secretfile),
inference(cnf,[status(esa)],[ax82]) ).
cnf(l67,plain,
owner_indi_has_need_to_know(owner_secretfile,alice,secretfile),
inference(instantiation,[status(thm)],[82]) ).
fof(ax73,plain,
credit_admin_indi_has_credit(credit_admin,alice),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax73) ).
cnf(73,plain,
credit_admin_indi_has_credit(credit_admin,alice),
inference(cnf,[status(esa)],[ax73]) ).
cnf(l80,plain,
credit_admin_indi_has_credit(credit_admin,alice),
inference(instantiation,[status(thm)],[73]) ).
fof(ax71,plain,
system_indi_has_citizenship(system,alice,usa),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax71) ).
cnf(71,plain,
system_indi_has_citizenship(system,alice,usa),
inference(cnf,[status(esa)],[ax71]) ).
cnf(l82,plain,
system_indi_has_citizenship(system,alice,usa),
inference(instantiation,[status(thm)],[71]) ).
fof(ax6,plain,
! [C,SSO] :
( system_compartment_has_sso(system,C,SSO)
=> admin_compartment_has_sso(admin,C,SSO) ),
file('Axioms/SWV009+0.ax',ax6) ).
cnf(6,plain,
( ~ system_compartment_has_sso(system,X0,X1)
| admin_compartment_has_sso(admin,X0,X1) ),
inference(cnf,[status(esa)],[ax6]) ).
cnf(l79,plain,
( ~ system_compartment_has_sso(system,compartmentb,sso_compartmentb)
| admin_compartment_has_sso(admin,compartmentb,sso_compartmentb) ),
inference(instantiation,[status(thm)],[6]) ).
fof(ax60,plain,
state_file_has_owner(secretfile,owner_secretfile),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax60) ).
cnf(60,plain,
state_file_has_owner(secretfile,owner_secretfile),
inference(cnf,[status(esa)],[ax60]) ).
cnf(l65,plain,
state_file_has_owner(secretfile,owner_secretfile),
inference(instantiation,[status(thm)],[60]) ).
cnf(l56,plain,
system_indi_has_citizenship(system,alice,usa),
inference(instantiation,[status(thm)],[71]) ).
fof(ax21,plain,
! [K,HR] :
( system_indi_is_hr_admin(system,HR)
=> ( hr_admin_indi_has_employment(HR,K)
=> admin_indi_has_employment(admin,K) ) ),
file('Axioms/SWV009+0.ax',ax21) ).
cnf(21,plain,
( ~ hr_admin_indi_has_employment(X0,X1)
| ~ system_indi_is_hr_admin(system,X0)
| admin_indi_has_employment(admin,X1) ),
inference(cnf,[status(esa)],[ax21]) ).
cnf(l26,plain,
( ~ hr_admin_indi_has_employment(hr_admin,alice)
| ~ system_indi_is_hr_admin(system,hr_admin)
| admin_indi_has_employment(admin,alice) ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l21,plain,
system_file_needs_compartments(system,secretfile,cons(compartmentb,cons(compartmenta,nil))),
inference(instantiation,[status(thm)],[51]) ).
fof(ax27,plain,
! [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('Axioms/SWV009+0.ax',ax27) ).
cnf(27,plain,
( ~ admin_compartment_has_sso(admin,X0,X1)
| ~ admin_indi_has_employment(admin,X2)
| ~ admin_indi_has_citizenship(admin,X2,usa)
| ~ admin_indi_has_polygraph_for_compartment(admin,X2,X0)
| ~ admin_indi_has_credit_for_compartment(admin,X2,X0)
| ~ admin_indi_has_background_for_compartment(admin,X2,X0)
| ~ sso_indi_has_compartment(X1,X2,X0)
| ~ admin_indi_has_level_for_compartment(admin,X2,X0)
| ~ admin_indi_has_compartments(admin,X2,X3)
| ~ system_indi_needs_compartment(system,X2,X0)
| admin_indi_has_compartments(admin,X2,cons(X0,X3)) ),
inference(cnf,[status(esa)],[ax27]) ).
cnf(l32,plain,
( ~ admin_compartment_has_sso(admin,compartmentb,sso_compartmentb)
| ~ admin_indi_has_employment(admin,alice)
| ~ admin_indi_has_citizenship(admin,alice,usa)
| ~ admin_indi_has_polygraph_for_compartment(admin,alice,compartmentb)
| ~ admin_indi_has_credit_for_compartment(admin,alice,compartmentb)
| ~ admin_indi_has_background_for_compartment(admin,alice,compartmentb)
| ~ sso_indi_has_compartment(sso_compartmentb,alice,compartmentb)
| ~ admin_indi_has_level_for_compartment(admin,alice,compartmentb)
| ~ admin_indi_has_compartments(admin,alice,cons(compartmenta,nil))
| ~ system_indi_needs_compartment(system,alice,compartmentb)
| admin_indi_has_compartments(admin,alice,cons(compartmentb,cons(compartmenta,nil))) ),
inference(instantiation,[status(thm)],[27]) ).
cnf(l34,plain,
( ~ admin_compartment_has_sso(admin,compartmenta,sso_compartmenta)
| ~ admin_indi_has_employment(admin,alice)
| ~ admin_indi_has_citizenship(admin,alice,usa)
| ~ admin_indi_has_polygraph_for_compartment(admin,alice,compartmenta)
| ~ admin_indi_has_credit_for_compartment(admin,alice,compartmenta)
| ~ admin_indi_has_background_for_compartment(admin,alice,compartmenta)
| ~ sso_indi_has_compartment(sso_compartmenta,alice,compartmenta)
| ~ admin_indi_has_level_for_compartment(admin,alice,compartmenta)
| ~ admin_indi_has_compartments(admin,alice,nil)
| ~ system_indi_needs_compartment(system,alice,compartmenta)
| admin_indi_has_compartments(admin,alice,cons(compartmenta,nil)) ),
inference(instantiation,[status(thm)],[27]) ).
cnf(l19,plain,
( ~ admin_compartment_has_sso(admin,compartmentb,sso_compartmentb)
| ~ admin_file_has_compartments_h(admin,secretfile,cons(compartmentb,cons(compartmenta,nil)),cons(compartmenta,nil))
| ~ sso_file_has_compartments(sso_compartmentb,secretfile,cons(compartmentb,cons(compartmenta,nil)))
| admin_file_has_compartments_h(admin,secretfile,cons(compartmentb,cons(compartmenta,nil)),cons(compartmentb,cons(compartmenta,nil))) ),
inference(instantiation,[status(thm)],[10]) ).
cnf(l83,plain,
( ~ system_indi_has_citizenship(system,alice,usa)
| admin_indi_has_citizenship(admin,alice,usa) ),
inference(instantiation,[status(thm)],[23]) ).
fof(ax29,plain,
! [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('Axioms/SWV009+0.ax',ax29) ).
cnf(29,plain,
( ~ system_indi_is_oca(system,X0)
| ~ admin_indi_has_level(admin,X1,X2)
| ~ oca_compartment_is_compartment(X0,X3,X2,X4,X5,X6)
| admin_indi_has_level_for_compartment(admin,X1,X3) ),
inference(cnf,[status(esa)],[ax29]) ).
cnf(l43,plain,
( ~ system_indi_is_oca(system,oca)
| ~ admin_indi_has_level(admin,alice,confidential)
| ~ oca_compartment_is_compartment(oca,compartmentb,confidential,topsecret,yes,yes)
| admin_indi_has_level_for_compartment(admin,alice,compartmentb) ),
inference(instantiation,[status(thm)],[29]) ).
fof(ax42,plain,
oca_compartment_is_compartment(oca,compartmentb,confidential,topsecret,yes,yes),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax42) ).
cnf(42,plain,
oca_compartment_is_compartment(oca,compartmentb,confidential,topsecret,yes,yes),
inference(cnf,[status(esa)],[ax42]) ).
cnf(l49,plain,
oca_compartment_is_compartment(oca,compartmentb,confidential,topsecret,yes,yes),
inference(instantiation,[status(thm)],[42]) ).
cnf(l84,plain,
( ~ system_compartment_has_sso(system,compartmentb,sso_compartmentb)
| admin_compartment_has_sso(admin,compartmentb,sso_compartmentb) ),
inference(instantiation,[status(thm)],[6]) ).
fof(ax78,plain,
system_indi_needs_compartment(system,alice,compartmentb),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax78) ).
cnf(78,plain,
system_indi_needs_compartment(system,alice,compartmentb),
inference(cnf,[status(esa)],[ax78]) ).
cnf(l78,plain,
system_indi_needs_compartment(system,alice,compartmentb),
inference(instantiation,[status(thm)],[78]) ).
fof(ax69,plain,
system_indi_is_hr_admin(system,hr_admin),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax69) ).
cnf(69,plain,
system_indi_is_hr_admin(system,hr_admin),
inference(cnf,[status(esa)],[ax69]) ).
cnf(l41,plain,
system_indi_is_hr_admin(system,hr_admin),
inference(instantiation,[status(thm)],[69]) ).
cnf(l53,plain,
( ~ hr_admin_indi_has_employment(hr_admin,alice)
| ~ system_indi_is_hr_admin(system,hr_admin)
| admin_indi_has_employment(admin,alice) ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l39,plain,
( ~ hr_admin_indi_has_employment(hr_admin,alice)
| ~ system_indi_is_hr_admin(system,hr_admin)
| admin_indi_has_employment(admin,alice) ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l57,plain,
( ~ loca_level_below(admin,confidential,secret)
| ~ loca_level_below(admin,confidential,topsecret)
| ~ admin_indi_has_background(admin,alice,confidential)
| ~ system_indi_is_level_admin(system,level_admin)
| ~ admin_indi_has_polygraph(admin,alice)
| ~ admin_indi_has_employment(admin,alice)
| ~ admin_indi_has_credit(admin,alice)
| ~ admin_indi_has_citizenship(admin,alice,usa)
| ~ level_admin_indi_has_level(level_admin,alice,topsecret)
| ~ system_indi_needs_level(system,alice,secret)
| admin_indi_has_level(admin,alice,confidential) ),
inference(instantiation,[status(thm)],[25]) ).
cnf(l74,plain,
( ~ system_compartment_has_sso(system,compartmentb,sso_compartmentb)
| admin_compartment_has_sso(admin,compartmentb,sso_compartmentb) ),
inference(instantiation,[status(thm)],[6]) ).
cnf(l85,plain,
system_indi_has_citizenship(system,alice,usa),
inference(instantiation,[status(thm)],[71]) ).
cnf(l58,plain,
level_admin_indi_has_level(level_admin,alice,topsecret),
inference(instantiation,[status(thm)],[77]) ).
cnf(l72,plain,
( ~ hr_admin_indi_has_employment(hr_admin,alice)
| ~ system_indi_is_hr_admin(system,hr_admin)
| admin_indi_has_employment(admin,alice) ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l86,plain,
( ~ admin_compartment_has_sso(admin,compartmenta,sso_compartmenta)
| ~ admin_file_has_compartments_h(admin,secretfile,cons(compartmentb,cons(compartmenta,nil)),nil)
| ~ sso_file_has_compartments(sso_compartmenta,secretfile,cons(compartmentb,cons(compartmenta,nil)))
| admin_file_has_compartments_h(admin,secretfile,cons(compartmentb,cons(compartmenta,nil)),cons(compartmenta,nil)) ),
inference(instantiation,[status(thm)],[10]) ).
fof(ax80,plain,
sso_indi_has_compartment(sso_compartmentb,alice,compartmentb),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax80) ).
cnf(80,plain,
sso_indi_has_compartment(sso_compartmentb,alice,compartmentb),
inference(cnf,[status(esa)],[ax80]) ).
cnf(l36,plain,
sso_indi_has_compartment(sso_compartmentb,alice,compartmentb),
inference(instantiation,[status(thm)],[80]) ).
cnf(l87,plain,
system_indi_needs_level(system,alice,secret),
inference(instantiation,[status(thm)],[76]) ).
cnf(l88,plain,
( ~ system_indi_is_polygraph_admin(system,polygraph_admin)
| ~ polygraph_admin_indi_has_polygraph(polygraph_admin,alice)
| admin_indi_has_polygraph(admin,alice) ),
inference(instantiation,[status(thm)],[17]) ).
cnf(l60,plain,
system_indi_is_hr_admin(system,hr_admin),
inference(instantiation,[status(thm)],[69]) ).
fof(ax66,plain,
system_indi_is_polygraph_admin(system,polygraph_admin),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax66) ).
cnf(66,plain,
system_indi_is_polygraph_admin(system,polygraph_admin),
inference(cnf,[status(esa)],[ax66]) ).
cnf(l22,plain,
system_indi_is_polygraph_admin(system,polygraph_admin),
inference(instantiation,[status(thm)],[66]) ).
fof(ax75,plain,
hr_admin_indi_has_employment(hr_admin,alice),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax75) ).
cnf(75,plain,
hr_admin_indi_has_employment(hr_admin,alice),
inference(cnf,[status(esa)],[ax75]) ).
cnf(l89,plain,
hr_admin_indi_has_employment(hr_admin,alice),
inference(instantiation,[status(thm)],[75]) ).
fof(ax44,plain,
system_compartment_has_sso(system,compartmentb,sso_compartmentb),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax44) ).
cnf(44,plain,
system_compartment_has_sso(system,compartmentb,sso_compartmentb),
inference(cnf,[status(esa)],[ax44]) ).
cnf(l90,plain,
system_compartment_has_sso(system,compartmentb,sso_compartmentb),
inference(instantiation,[status(thm)],[44]) ).
cnf(l91,plain,
system_indi_is_hr_admin(system,hr_admin),
inference(instantiation,[status(thm)],[69]) ).
cnf(l35,plain,
( ~ admin_compartment_has_sso(admin,compartmenta,sso_compartmenta)
| ~ admin_file_has_compartments_h(admin,secretfile,cons(compartmentb,cons(compartmenta,nil)),nil)
| ~ sso_file_has_compartments(sso_compartmenta,secretfile,cons(compartmentb,cons(compartmenta,nil)))
| admin_file_has_compartments_h(admin,secretfile,cons(compartmentb,cons(compartmenta,nil)),cons(compartmenta,nil)) ),
inference(instantiation,[status(thm)],[10]) ).
cnf(l62,plain,
( ~ system_indi_is_credit_admin(system,credit_admin)
| ~ credit_admin_indi_has_credit(credit_admin,alice)
| admin_indi_has_credit(admin,alice) ),
inference(instantiation,[status(thm)],[18]) ).
cnf(l37,plain,
( ~ system_compartment_has_sso(system,compartmenta,sso_compartmenta)
| admin_compartment_has_sso(admin,compartmenta,sso_compartmenta) ),
inference(instantiation,[status(thm)],[6]) ).
fof(ax28,plain,
! [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('Axioms/SWV009+0.ax',ax28) ).
cnf(28,plain,
( ~ system_indi_is_oca(system,X0)
| ~ admin_indi_has_background(admin,X1,X2)
| ~ oca_compartment_is_compartment(X0,X3,X4,X2,X5,X6)
| admin_indi_has_background_for_compartment(admin,X1,X3) ),
inference(cnf,[status(esa)],[ax28]) ).
cnf(l44,plain,
( ~ system_indi_is_oca(system,oca)
| ~ admin_indi_has_background(admin,alice,topsecret)
| ~ oca_compartment_is_compartment(oca,compartmentb,confidential,topsecret,yes,yes)
| admin_indi_has_background_for_compartment(admin,alice,compartmentb) ),
inference(instantiation,[status(thm)],[28]) ).
cnf(l92,plain,
( ~ system_indi_is_oca(system,oca)
| ~ admin_indi_has_background(admin,alice,unclassified)
| ~ oca_compartment_is_compartment(oca,compartmenta,sbu,unclassified,no,no)
| admin_indi_has_background_for_compartment(admin,alice,compartmenta) ),
inference(instantiation,[status(thm)],[28]) ).
fof(ax16,plain,
! [F,U,C,CL,SSO,SCG] :
( admin_compartment_has_sso(admin,C,SSO)
=> ( admin_compartment_has_scg(admin,C,SCG)
=> ( sso_file_has_citizenship(SSO,F,U,SCG)
=> ( admin_file_has_citizenship_h(admin,F,U,CL)
=> admin_file_has_citizenship_h(admin,F,U,cons(C,CL)) ) ) ) ),
file('Axioms/SWV009+0.ax',ax16) ).
cnf(16,plain,
( ~ admin_compartment_has_scg(admin,X0,X1)
| ~ admin_compartment_has_sso(admin,X0,X2)
| ~ admin_file_has_citizenship_h(admin,X3,X4,X5)
| ~ sso_file_has_citizenship(X2,X3,X4,X1)
| admin_file_has_citizenship_h(admin,X3,X4,cons(X0,X5)) ),
inference(cnf,[status(esa)],[ax16]) ).
cnf(l29,plain,
( ~ admin_compartment_has_scg(admin,compartmentb,scg_compartmentb)
| ~ admin_compartment_has_sso(admin,compartmentb,sso_compartmentb)
| ~ admin_file_has_citizenship_h(admin,secretfile,usa,cons(compartmenta,nil))
| ~ sso_file_has_citizenship(sso_compartmentb,secretfile,usa,scg_compartmentb)
| admin_file_has_citizenship_h(admin,secretfile,usa,cons(compartmentb,cons(compartmenta,nil))) ),
inference(instantiation,[status(thm)],[16]) ).
fof(ax52,plain,
sso_file_has_compartments(sso_compartmentb,secretfile,cons(compartmentb,cons(compartmenta,nil))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax52) ).
cnf(52,plain,
sso_file_has_compartments(sso_compartmentb,secretfile,cons(compartmentb,cons(compartmenta,nil))),
inference(cnf,[status(esa)],[ax52]) ).
cnf(l93,plain,
sso_file_has_compartments(sso_compartmentb,secretfile,cons(compartmentb,cons(compartmenta,nil))),
inference(instantiation,[status(thm)],[52]) ).
cnf(l94,plain,
system_compartment_has_sso(system,compartmentb,sso_compartmentb),
inference(instantiation,[status(thm)],[44]) ).
fof(ax26,plain,
! [K] : admin_indi_has_compartments(admin,K,nil),
file('Axioms/SWV009+0.ax',ax26) ).
cnf(26,plain,
admin_indi_has_compartments(admin,X0,nil),
inference(cnf,[status(esa)],[ax26]) ).
cnf(l95,plain,
admin_indi_has_compartments(admin,alice,nil),
inference(instantiation,[status(thm)],[26]) ).
fof(ax9,plain,
! [F,CL] : admin_file_has_compartments_h(admin,F,CL,nil),
file('Axioms/SWV009+0.ax',ax9) ).
cnf(9,plain,
admin_file_has_compartments_h(admin,X0,X1,nil),
inference(cnf,[status(esa)],[ax9]) ).
cnf(l96,plain,
admin_file_has_compartments_h(admin,secretfile,cons(compartmentb,cons(compartmenta,nil)),nil),
inference(instantiation,[status(thm)],[9]) ).
cnf(l42,plain,
( ~ system_compartment_has_sso(system,compartmenta,sso_compartmenta)
| admin_compartment_has_sso(admin,compartmenta,sso_compartmenta) ),
inference(instantiation,[status(thm)],[6]) ).
fof(ax19,plain,
! [K] : admin_indi_has_background(admin,K,unclassified),
file('Axioms/SWV009+0.ax',ax19) ).
cnf(19,plain,
admin_indi_has_background(admin,X0,unclassified),
inference(cnf,[status(esa)],[ax19]) ).
cnf(l97,plain,
admin_indi_has_background(admin,alice,unclassified),
inference(instantiation,[status(thm)],[19]) ).
fof(ax20,plain,
! [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('Axioms/SWV009+0.ax',ax20) ).
cnf(20,plain,
( ~ loca_level_below(admin,X0,X1)
| ~ system_indi_is_background_admin(system,X2)
| ~ background_admin_indi_has_background(X2,X3,X1)
| admin_indi_has_background(admin,X3,X0) ),
inference(cnf,[status(esa)],[ax20]) ).
cnf(l98,plain,
( ~ loca_level_below(admin,confidential,topsecret)
| ~ system_indi_is_background_admin(system,background_admin)
| ~ background_admin_indi_has_background(background_admin,alice,topsecret)
| admin_indi_has_background(admin,alice,confidential) ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l64,plain,
( ~ loca_level_direct_below(admin,secret,topsecret)
| ~ loca_level_below(admin,confidential,secret)
| loca_level_below(admin,confidential,topsecret) ),
inference(instantiation,[status(thm)],[5]) ).
cnf(l99,plain,
( ~ loca_level_direct_below(admin,secret,topsecret)
| ~ loca_level_below(admin,confidential,secret)
| loca_level_below(admin,confidential,topsecret) ),
inference(instantiation,[status(thm)],[5]) ).
fof(ax41,plain,
system_indi_is_oca(system,oca),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax41) ).
cnf(41,plain,
system_indi_is_oca(system,oca),
inference(cnf,[status(esa)],[ax41]) ).
cnf(l70,plain,
system_indi_is_oca(system,oca),
inference(instantiation,[status(thm)],[41]) ).
cnf(l76,plain,
system_indi_is_oca(system,oca),
inference(instantiation,[status(thm)],[41]) ).
cnf(l33,plain,
hr_admin_indi_has_employment(hr_admin,alice),
inference(instantiation,[status(thm)],[75]) ).
fof(ax7,plain,
! [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('Axioms/SWV009+0.ax',ax7) ).
cnf(7,plain,
( ~ admin_compartment_has_sso(admin,X0,X1)
| ~ system_indi_is_oca(system,X2)
| ~ oca_compartment_has_scg(X2,X0,X3)
| ~ sso_compartment_has_scg(X1,X0,X3)
| admin_compartment_has_scg(admin,X0,X3) ),
inference(cnf,[status(esa)],[ax7]) ).
cnf(l147,plain,
( ~ admin_compartment_has_sso(admin,compartmentb,sso_compartmentb)
| ~ system_indi_is_oca(system,oca)
| ~ oca_compartment_has_scg(oca,compartmentb,scg_compartmentb)
| ~ sso_compartment_has_scg(sso_compartmentb,compartmentb,scg_compartmentb)
| admin_compartment_has_scg(admin,compartmentb,scg_compartmentb) ),
inference(instantiation,[status(thm)],[7]) ).
fof(ax43,plain,
oca_compartment_is_compartment(oca,compartmenta,sbu,unclassified,no,no),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax43) ).
cnf(43,plain,
oca_compartment_is_compartment(oca,compartmenta,sbu,unclassified,no,no),
inference(cnf,[status(esa)],[ax43]) ).
cnf(l143,plain,
oca_compartment_is_compartment(oca,compartmenta,sbu,unclassified,no,no),
inference(instantiation,[status(thm)],[43]) ).
cnf(l102,plain,
hr_admin_indi_has_employment(hr_admin,alice),
inference(instantiation,[status(thm)],[75]) ).
cnf(l105,plain,
credit_admin_indi_has_credit(credit_admin,alice),
inference(instantiation,[status(thm)],[73]) ).
cnf(l66,plain,
( ~ loca_level_below(admin,secret,topsecret)
| ~ system_indi_is_background_admin(system,background_admin)
| ~ background_admin_indi_has_background(background_admin,alice,topsecret)
| admin_indi_has_background(admin,alice,secret) ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l146,plain,
system_indi_is_hr_admin(system,hr_admin),
inference(instantiation,[status(thm)],[69]) ).
fof(ax32,plain,
! [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('Axioms/SWV009+0.ax',ax32) ).
cnf(32,plain,
( ~ system_indi_is_oca(system,X0)
| ~ admin_indi_has_credit(admin,X1)
| ~ oca_compartment_is_compartment(X0,X2,X3,X4,yes,X5)
| admin_indi_has_credit_for_compartment(admin,X1,X2) ),
inference(cnf,[status(esa)],[ax32]) ).
cnf(l38,plain,
( ~ system_indi_is_oca(system,oca)
| ~ admin_indi_has_credit(admin,alice)
| ~ oca_compartment_is_compartment(oca,compartmentb,confidential,topsecret,yes,yes)
| admin_indi_has_credit_for_compartment(admin,alice,compartmentb) ),
inference(instantiation,[status(thm)],[32]) ).
fof(ax72,plain,
polygraph_admin_indi_has_polygraph(polygraph_admin,alice),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax72) ).
cnf(72,plain,
polygraph_admin_indi_has_polygraph(polygraph_admin,alice),
inference(cnf,[status(esa)],[ax72]) ).
cnf(l30,plain,
polygraph_admin_indi_has_polygraph(polygraph_admin,alice),
inference(instantiation,[status(thm)],[72]) ).
cnf(l47,plain,
system_indi_is_oca(system,oca),
inference(instantiation,[status(thm)],[41]) ).
cnf(l71,plain,
( ~ system_indi_is_credit_admin(system,credit_admin)
| ~ credit_admin_indi_has_credit(credit_admin,alice)
| admin_indi_has_credit(admin,alice) ),
inference(instantiation,[status(thm)],[18]) ).
cnf(l104,plain,
system_indi_is_credit_admin(system,credit_admin),
inference(instantiation,[status(thm)],[67]) ).
cnf(l100,plain,
( ~ loca_level_direct_below(admin,confidential,secret)
| ~ loca_level_below(admin,confidential,confidential)
| loca_level_below(admin,confidential,secret) ),
inference(instantiation,[status(thm)],[5]) ).
fof(ax33,plain,
! [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('Axioms/SWV009+0.ax',ax33) ).
cnf(33,plain,
( ~ system_indi_is_oca(system,X0)
| ~ oca_compartment_is_compartment(X0,X1,X2,X3,no,X4)
| admin_indi_has_credit_for_compartment(admin,X5,X1) ),
inference(cnf,[status(esa)],[ax33]) ).
cnf(l45,plain,
( ~ system_indi_is_oca(system,oca)
| ~ oca_compartment_is_compartment(oca,compartmenta,sbu,unclassified,no,no)
| admin_indi_has_credit_for_compartment(admin,alice,compartmenta) ),
inference(instantiation,[status(thm)],[33]) ).
cnf(l168,plain,
oca_compartment_is_compartment(oca,compartmenta,sbu,unclassified,no,no),
inference(instantiation,[status(thm)],[43]) ).
cnf(l149,plain,
system_indi_is_polygraph_admin(system,polygraph_admin),
inference(instantiation,[status(thm)],[66]) ).
cnf(l115,plain,
polygraph_admin_indi_has_polygraph(polygraph_admin,alice),
inference(instantiation,[status(thm)],[72]) ).
cnf(l77,plain,
oca_compartment_is_compartment(oca,compartmentb,confidential,topsecret,yes,yes),
inference(instantiation,[status(thm)],[42]) ).
fof(ax46,plain,
sso_compartment_has_scg(sso_compartmentb,compartmentb,scg_compartmentb),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax46) ).
cnf(46,plain,
sso_compartment_has_scg(sso_compartmentb,compartmentb,scg_compartmentb),
inference(cnf,[status(esa)],[ax46]) ).
cnf(l175,plain,
sso_compartment_has_scg(sso_compartmentb,compartmentb,scg_compartmentb),
inference(instantiation,[status(thm)],[46]) ).
cnf(l48,plain,
hr_admin_indi_has_employment(hr_admin,alice),
inference(instantiation,[status(thm)],[75]) ).
cnf(l173,plain,
loca_level_below(admin,confidential,confidential),
inference(instantiation,[status(thm)],[4]) ).
cnf(l134,plain,
( ~ system_compartment_has_sso(system,compartmenta,sso_compartmenta)
| admin_compartment_has_sso(admin,compartmenta,sso_compartmenta) ),
inference(instantiation,[status(thm)],[6]) ).
fof(ax31,plain,
! [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('Axioms/SWV009+0.ax',ax31) ).
cnf(31,plain,
( ~ system_indi_is_oca(system,X0)
| ~ oca_compartment_is_compartment(X0,X1,X2,X3,X4,no)
| admin_indi_has_polygraph_for_compartment(admin,X5,X1) ),
inference(cnf,[status(esa)],[ax31]) ).
cnf(l108,plain,
( ~ system_indi_is_oca(system,oca)
| ~ oca_compartment_is_compartment(oca,compartmenta,sbu,unclassified,no,no)
| admin_indi_has_polygraph_for_compartment(admin,alice,compartmenta) ),
inference(instantiation,[status(thm)],[31]) ).
cnf(l138,plain,
system_indi_is_level_admin(system,level_admin),
inference(instantiation,[status(thm)],[70]) ).
fof(ax45,plain,
oca_compartment_has_scg(oca,compartmentb,scg_compartmentb),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax45) ).
cnf(45,plain,
oca_compartment_has_scg(oca,compartmentb,scg_compartmentb),
inference(cnf,[status(esa)],[ax45]) ).
cnf(l154,plain,
oca_compartment_has_scg(oca,compartmentb,scg_compartmentb),
inference(instantiation,[status(thm)],[45]) ).
cnf(l128,plain,
system_indi_is_oca(system,oca),
inference(instantiation,[status(thm)],[41]) ).
fof(ax68,plain,
system_indi_is_background_admin(system,background_admin),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax68) ).
cnf(68,plain,
system_indi_is_background_admin(system,background_admin),
inference(cnf,[status(esa)],[ax68]) ).
cnf(l141,plain,
system_indi_is_background_admin(system,background_admin),
inference(instantiation,[status(thm)],[68]) ).
fof(ax74,plain,
background_admin_indi_has_background(background_admin,alice,topsecret),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax74) ).
cnf(74,plain,
background_admin_indi_has_background(background_admin,alice,topsecret),
inference(cnf,[status(esa)],[ax74]) ).
cnf(l140,plain,
background_admin_indi_has_background(background_admin,alice,topsecret),
inference(instantiation,[status(thm)],[74]) ).
fof(ax81,plain,
sso_indi_has_compartment(sso_compartmenta,alice,compartmenta),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax81) ).
cnf(81,plain,
sso_indi_has_compartment(sso_compartmenta,alice,compartmenta),
inference(cnf,[status(esa)],[ax81]) ).
cnf(l55,plain,
sso_indi_has_compartment(sso_compartmenta,alice,compartmenta),
inference(instantiation,[status(thm)],[81]) ).
cnf(l118,plain,
( ~ system_compartment_has_sso(system,compartmentb,sso_compartmentb)
| admin_compartment_has_sso(admin,compartmentb,sso_compartmentb) ),
inference(instantiation,[status(thm)],[6]) ).
cnf(l117,plain,
( ~ system_indi_is_oca(system,oca)
| ~ admin_indi_has_level(admin,alice,sbu)
| ~ oca_compartment_is_compartment(oca,compartmenta,sbu,unclassified,no,no)
| admin_indi_has_level_for_compartment(admin,alice,compartmenta) ),
inference(instantiation,[status(thm)],[29]) ).
fof(ax53,plain,
sso_file_has_compartments(sso_compartmenta,secretfile,cons(compartmentb,cons(compartmenta,nil))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax53) ).
cnf(53,plain,
sso_file_has_compartments(sso_compartmenta,secretfile,cons(compartmentb,cons(compartmenta,nil))),
inference(cnf,[status(esa)],[ax53]) ).
cnf(l52,plain,
sso_file_has_compartments(sso_compartmenta,secretfile,cons(compartmentb,cons(compartmenta,nil))),
inference(instantiation,[status(thm)],[53]) ).
cnf(l124,plain,
system_indi_is_oca(system,oca),
inference(instantiation,[status(thm)],[41]) ).
fof(ax47,plain,
system_compartment_has_sso(system,compartmenta,sso_compartmenta),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax47) ).
cnf(47,plain,
system_compartment_has_sso(system,compartmenta,sso_compartmenta),
inference(cnf,[status(esa)],[ax47]) ).
cnf(l69,plain,
system_compartment_has_sso(system,compartmenta,sso_compartmenta),
inference(instantiation,[status(thm)],[47]) ).
fof(ax58,plain,
sso_file_has_citizenship(sso_compartmentb,secretfile,usa,scg_compartmentb),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax58) ).
cnf(58,plain,
sso_file_has_citizenship(sso_compartmentb,secretfile,usa,scg_compartmentb),
inference(cnf,[status(esa)],[ax58]) ).
cnf(l109,plain,
sso_file_has_citizenship(sso_compartmentb,secretfile,usa,scg_compartmentb),
inference(instantiation,[status(thm)],[58]) ).
cnf(l103,plain,
system_compartment_has_sso(system,compartmentb,sso_compartmentb),
inference(instantiation,[status(thm)],[44]) ).
cnf(l51,plain,
system_compartment_has_sso(system,compartmenta,sso_compartmenta),
inference(instantiation,[status(thm)],[47]) ).
cnf(l111,plain,
loca_level_direct_below(admin,secret,topsecret),
inference(instantiation,[status(thm)],[3]) ).
cnf(l178,plain,
( ~ system_compartment_has_sso(system,compartmentb,sso_compartmentb)
| admin_compartment_has_sso(admin,compartmentb,sso_compartmentb) ),
inference(instantiation,[status(thm)],[6]) ).
cnf(l171,plain,
credit_admin_indi_has_credit(credit_admin,alice),
inference(instantiation,[status(thm)],[73]) ).
cnf(l163,plain,
( ~ admin_compartment_has_scg(admin,compartmenta,scg_compartmenta)
| ~ admin_compartment_has_sso(admin,compartmenta,sso_compartmenta)
| ~ admin_file_has_citizenship_h(admin,secretfile,usa,nil)
| ~ sso_file_has_citizenship(sso_compartmenta,secretfile,usa,scg_compartmenta)
| admin_file_has_citizenship_h(admin,secretfile,usa,cons(compartmenta,nil)) ),
inference(instantiation,[status(thm)],[16]) ).
cnf(l114,plain,
sso_file_has_compartments(sso_compartmenta,secretfile,cons(compartmentb,cons(compartmenta,nil))),
inference(instantiation,[status(thm)],[53]) ).
cnf(l180,plain,
system_compartment_has_sso(system,compartmenta,sso_compartmenta),
inference(instantiation,[status(thm)],[47]) ).
fof(ax11,plain,
! [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('Axioms/SWV009+0.ax',ax11) ).
cnf(11,plain,
( ~ system_file_needs_level(system,X0,X1)
| ~ admin_file_has_compartments(admin,X0,X2)
| ~ admin_file_has_level_h(admin,X0,X1,X2)
| admin_file_has_level(admin,X0,X1) ),
inference(cnf,[status(esa)],[ax11]) ).
cnf(l23,plain,
( ~ system_file_needs_level(system,secretfile,secret)
| ~ admin_file_has_compartments(admin,secretfile,cons(compartmentb,cons(compartmenta,nil)))
| ~ admin_file_has_level_h(admin,secretfile,secret,cons(compartmentb,cons(compartmenta,nil)))
| admin_file_has_level(admin,secretfile,secret) ),
inference(instantiation,[status(thm)],[11]) ).
cnf(l59,plain,
( ~ system_indi_has_citizenship(system,alice,usa)
| admin_indi_has_citizenship(admin,alice,usa) ),
inference(instantiation,[status(thm)],[23]) ).
fof(ax30,plain,
! [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('Axioms/SWV009+0.ax',ax30) ).
cnf(30,plain,
( ~ system_indi_is_oca(system,X0)
| ~ admin_indi_has_polygraph(admin,X1)
| ~ oca_compartment_is_compartment(X0,X2,X3,X4,X5,yes)
| admin_indi_has_polygraph_for_compartment(admin,X1,X2) ),
inference(cnf,[status(esa)],[ax30]) ).
cnf(l50,plain,
( ~ system_indi_is_oca(system,oca)
| ~ admin_indi_has_polygraph(admin,alice)
| ~ oca_compartment_is_compartment(oca,compartmentb,confidential,topsecret,yes,yes)
| admin_indi_has_polygraph_for_compartment(admin,alice,compartmentb) ),
inference(instantiation,[status(thm)],[30]) ).
fof(ax54,plain,
system_file_needs_level(system,secretfile,secret),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax54) ).
cnf(54,plain,
system_file_needs_level(system,secretfile,secret),
inference(cnf,[status(esa)],[ax54]) ).
cnf(l122,plain,
system_file_needs_level(system,secretfile,secret),
inference(instantiation,[status(thm)],[54]) ).
cnf(l133,plain,
admin_file_has_compartments_h(admin,secretfile,cons(compartmentb,cons(compartmenta,nil)),nil),
inference(instantiation,[status(thm)],[9]) ).
cnf(l165,plain,
( ~ system_compartment_has_sso(system,compartmenta,sso_compartmenta)
| admin_compartment_has_sso(admin,compartmenta,sso_compartmenta) ),
inference(instantiation,[status(thm)],[6]) ).
cnf(l54,plain,
system_indi_is_oca(system,oca),
inference(instantiation,[status(thm)],[41]) ).
cnf(l40,plain,
sso_file_has_compartments(sso_compartmentb,secretfile,cons(compartmentb,cons(compartmenta,nil))),
inference(instantiation,[status(thm)],[52]) ).
cnf(l63,plain,
( ~ loca_level_direct_below(admin,confidential,secret)
| ~ loca_level_below(admin,confidential,confidential)
| loca_level_below(admin,confidential,secret) ),
inference(instantiation,[status(thm)],[5]) ).
cnf(l130,plain,
loca_level_below(admin,confidential,confidential),
inference(instantiation,[status(thm)],[4]) ).
cnf(l142,plain,
system_compartment_has_sso(system,compartmentb,sso_compartmentb),
inference(instantiation,[status(thm)],[44]) ).
fof(ax79,plain,
system_indi_needs_compartment(system,alice,compartmenta),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax79) ).
cnf(79,plain,
system_indi_needs_compartment(system,alice,compartmenta),
inference(cnf,[status(esa)],[ax79]) ).
cnf(l61,plain,
system_indi_needs_compartment(system,alice,compartmenta),
inference(instantiation,[status(thm)],[79]) ).
cnf(l186,plain,
system_compartment_has_sso(system,compartmenta,sso_compartmenta),
inference(instantiation,[status(thm)],[47]) ).
cnf(l121,plain,
oca_compartment_is_compartment(oca,compartmenta,sbu,unclassified,no,no),
inference(instantiation,[status(thm)],[43]) ).
cnf(l68,plain,
system_indi_has_citizenship(system,alice,usa),
inference(instantiation,[status(thm)],[71]) ).
cnf(l75,plain,
loca_level_direct_below(admin,secret,topsecret),
inference(instantiation,[status(thm)],[3]) ).
fof(ax2,plain,
! [K] : loca_level_direct_below(K,confidential,secret),
file('Axioms/SWV009+0.ax',ax2) ).
cnf(2,plain,
loca_level_direct_below(X0,confidential,secret),
inference(cnf,[status(esa)],[ax2]) ).
cnf(l110,plain,
loca_level_direct_below(admin,confidential,secret),
inference(instantiation,[status(thm)],[2]) ).
cnf(l177,plain,
loca_level_direct_below(admin,confidential,secret),
inference(instantiation,[status(thm)],[2]) ).
cnf(l172,plain,
oca_compartment_is_compartment(oca,compartmentb,confidential,topsecret,yes,yes),
inference(instantiation,[status(thm)],[42]) ).
cnf(l151,plain,
system_indi_is_oca(system,oca),
inference(instantiation,[status(thm)],[41]) ).
fof(ax13,plain,
! [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('Axioms/SWV009+0.ax',ax13) ).
cnf(13,plain,
( ~ admin_compartment_has_scg(admin,X0,X1)
| ~ admin_compartment_has_sso(admin,X0,X2)
| ~ admin_file_has_level_h(admin,X3,X4,X5)
| ~ sso_file_has_level(X2,X3,X4,X1)
| admin_file_has_level_h(admin,X3,X4,cons(X0,X5)) ),
inference(cnf,[status(esa)],[ax13]) ).
cnf(l144,plain,
( ~ admin_compartment_has_scg(admin,compartmentb,scg_compartmentb)
| ~ admin_compartment_has_sso(admin,compartmentb,sso_compartmentb)
| ~ admin_file_has_level_h(admin,secretfile,secret,cons(compartmenta,nil))
| ~ sso_file_has_level(sso_compartmentb,secretfile,secret,scg_compartmentb)
| admin_file_has_level_h(admin,secretfile,secret,cons(compartmentb,cons(compartmenta,nil))) ),
inference(instantiation,[status(thm)],[13]) ).
fof(ax59,plain,
sso_file_has_citizenship(sso_compartmenta,secretfile,usa,scg_compartmenta),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax59) ).
cnf(59,plain,
sso_file_has_citizenship(sso_compartmenta,secretfile,usa,scg_compartmenta),
inference(cnf,[status(esa)],[ax59]) ).
cnf(l183,plain,
sso_file_has_citizenship(sso_compartmenta,secretfile,usa,scg_compartmenta),
inference(instantiation,[status(thm)],[59]) ).
cnf(l126,plain,
system_indi_is_oca(system,oca),
inference(instantiation,[status(thm)],[41]) ).
cnf(l179,plain,
system_compartment_has_sso(system,compartmentb,sso_compartmentb),
inference(instantiation,[status(thm)],[44]) ).
cnf(l205,plain,
( ~ admin_compartment_has_sso(admin,compartmentb,sso_compartmentb)
| ~ system_indi_is_oca(system,oca)
| ~ oca_compartment_has_scg(oca,compartmentb,scg_compartmentb)
| ~ sso_compartment_has_scg(sso_compartmentb,compartmentb,scg_compartmentb)
| admin_compartment_has_scg(admin,compartmentb,scg_compartmentb) ),
inference(instantiation,[status(thm)],[7]) ).
cnf(l145,plain,
( ~ system_compartment_has_sso(system,compartmentb,sso_compartmentb)
| admin_compartment_has_sso(admin,compartmentb,sso_compartmentb) ),
inference(instantiation,[status(thm)],[6]) ).
cnf(l206,plain,
oca_compartment_has_scg(oca,compartmentb,scg_compartmentb),
inference(instantiation,[status(thm)],[45]) ).
cnf(l120,plain,
( ~ loca_level_direct_below(admin,confidential,secret)
| ~ loca_level_below(admin,confidential,confidential)
| loca_level_below(admin,confidential,secret) ),
inference(instantiation,[status(thm)],[5]) ).
fof(ax15,plain,
! [F,U] : admin_file_has_citizenship_h(admin,F,U,nil),
file('Axioms/SWV009+0.ax',ax15) ).
cnf(15,plain,
admin_file_has_citizenship_h(admin,X0,X1,nil),
inference(cnf,[status(esa)],[ax15]) ).
cnf(l167,plain,
admin_file_has_citizenship_h(admin,secretfile,usa,nil),
inference(instantiation,[status(thm)],[15]) ).
cnf(l181,plain,
oca_compartment_is_compartment(oca,compartmentb,confidential,topsecret,yes,yes),
inference(instantiation,[status(thm)],[42]) ).
cnf(l24,plain,
( ~ admin_file_has_compartments_h(admin,secretfile,cons(compartmentb,cons(compartmenta,nil)),cons(compartmentb,cons(compartmenta,nil)))
| ~ system_file_needs_compartments(system,secretfile,cons(compartmentb,cons(compartmenta,nil)))
| admin_file_has_compartments(admin,secretfile,cons(compartmentb,cons(compartmenta,nil))) ),
inference(instantiation,[status(thm)],[8]) ).
cnf(l207,plain,
( ~ system_compartment_has_sso(system,compartmentb,sso_compartmentb)
| admin_compartment_has_sso(admin,compartmentb,sso_compartmentb) ),
inference(instantiation,[status(thm)],[6]) ).
fof(ax55,plain,
sso_file_has_level(sso_compartmentb,secretfile,secret,scg_compartmentb),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax55) ).
cnf(55,plain,
sso_file_has_level(sso_compartmentb,secretfile,secret,scg_compartmentb),
inference(cnf,[status(esa)],[ax55]) ).
cnf(l150,plain,
sso_file_has_level(sso_compartmentb,secretfile,secret,scg_compartmentb),
inference(instantiation,[status(thm)],[55]) ).
cnf(l119,plain,
oca_compartment_is_compartment(oca,compartmenta,sbu,unclassified,no,no),
inference(instantiation,[status(thm)],[43]) ).
cnf(l159,plain,
( ~ admin_compartment_has_sso(admin,compartmentb,sso_compartmentb)
| ~ admin_file_has_compartments_h(admin,secretfile,cons(compartmentb,cons(compartmenta,nil)),cons(compartmenta,nil))
| ~ sso_file_has_compartments(sso_compartmentb,secretfile,cons(compartmentb,cons(compartmenta,nil)))
| admin_file_has_compartments_h(admin,secretfile,cons(compartmentb,cons(compartmenta,nil)),cons(compartmentb,cons(compartmenta,nil))) ),
inference(instantiation,[status(thm)],[10]) ).
cnf(l208,plain,
sso_compartment_has_scg(sso_compartmentb,compartmentb,scg_compartmentb),
inference(instantiation,[status(thm)],[46]) ).
cnf(l170,plain,
system_indi_is_oca(system,oca),
inference(instantiation,[status(thm)],[41]) ).
cnf(l101,plain,
( ~ system_indi_has_citizenship(system,alice,usa)
| admin_indi_has_citizenship(admin,alice,usa) ),
inference(instantiation,[status(thm)],[23]) ).
cnf(l209,plain,
loca_level_below(admin,confidential,confidential),
inference(instantiation,[status(thm)],[4]) ).
cnf(l210,plain,
( ~ system_compartment_has_sso(system,compartmentb,sso_compartmentb)
| admin_compartment_has_sso(admin,compartmentb,sso_compartmentb) ),
inference(instantiation,[status(thm)],[6]) ).
cnf(l136,plain,
( ~ loca_level_below(admin,sbu,secret)
| ~ loca_level_below(admin,sbu,topsecret)
| ~ admin_indi_has_background(admin,alice,sbu)
| ~ system_indi_is_level_admin(system,level_admin)
| ~ admin_indi_has_polygraph(admin,alice)
| ~ admin_indi_has_employment(admin,alice)
| ~ admin_indi_has_credit(admin,alice)
| ~ admin_indi_has_citizenship(admin,alice,usa)
| ~ level_admin_indi_has_level(level_admin,alice,topsecret)
| ~ system_indi_needs_level(system,alice,secret)
| admin_indi_has_level(admin,alice,sbu) ),
inference(instantiation,[status(thm)],[25]) ).
cnf(l187,plain,
( ~ system_indi_is_polygraph_admin(system,polygraph_admin)
| ~ polygraph_admin_indi_has_polygraph(polygraph_admin,alice)
| admin_indi_has_polygraph(admin,alice) ),
inference(instantiation,[status(thm)],[17]) ).
cnf(l211,plain,
( ~ admin_compartment_has_scg(admin,compartmenta,scg_compartmenta)
| ~ admin_compartment_has_sso(admin,compartmenta,sso_compartmenta)
| ~ admin_file_has_level_h(admin,secretfile,secret,nil)
| ~ sso_file_has_level(sso_compartmenta,secretfile,secret,scg_compartmenta)
| admin_file_has_level_h(admin,secretfile,secret,cons(compartmenta,nil)) ),
inference(instantiation,[status(thm)],[13]) ).
cnf(l135,plain,
system_indi_is_background_admin(system,background_admin),
inference(instantiation,[status(thm)],[68]) ).
cnf(l160,plain,
( ~ admin_compartment_has_sso(admin,compartmenta,sso_compartmenta)
| ~ admin_file_has_compartments_h(admin,secretfile,cons(compartmentb,cons(compartmenta,nil)),nil)
| ~ sso_file_has_compartments(sso_compartmenta,secretfile,cons(compartmentb,cons(compartmenta,nil)))
| admin_file_has_compartments_h(admin,secretfile,cons(compartmentb,cons(compartmenta,nil)),cons(compartmenta,nil)) ),
inference(instantiation,[status(thm)],[10]) ).
cnf(l212,plain,
system_indi_is_level_admin(system,level_admin),
inference(instantiation,[status(thm)],[70]) ).
cnf(l213,plain,
system_indi_is_polygraph_admin(system,polygraph_admin),
inference(instantiation,[status(thm)],[66]) ).
cnf(l201,plain,
level_admin_indi_has_level(level_admin,alice,topsecret),
inference(instantiation,[status(thm)],[77]) ).
cnf(l190,plain,
polygraph_admin_indi_has_polygraph(polygraph_admin,alice),
inference(instantiation,[status(thm)],[72]) ).
cnf(l214,plain,
system_compartment_has_sso(system,compartmentb,sso_compartmentb),
inference(instantiation,[status(thm)],[44]) ).
cnf(l215,plain,
system_compartment_has_sso(system,compartmentb,sso_compartmentb),
inference(instantiation,[status(thm)],[44]) ).
cnf(l216,plain,
( ~ system_compartment_has_sso(system,compartmenta,sso_compartmenta)
| admin_compartment_has_sso(admin,compartmenta,sso_compartmenta) ),
inference(instantiation,[status(thm)],[6]) ).
cnf(l129,plain,
background_admin_indi_has_background(background_admin,alice,topsecret),
inference(instantiation,[status(thm)],[74]) ).
cnf(l162,plain,
( ~ system_compartment_has_sso(system,compartmenta,sso_compartmenta)
| admin_compartment_has_sso(admin,compartmenta,sso_compartmenta) ),
inference(instantiation,[status(thm)],[6]) ).
cnf(l217,plain,
system_indi_is_oca(system,oca),
inference(instantiation,[status(thm)],[41]) ).
cnf(l169,plain,
system_indi_is_credit_admin(system,credit_admin),
inference(instantiation,[status(thm)],[67]) ).
cnf(l113,plain,
system_indi_has_citizenship(system,alice,usa),
inference(instantiation,[status(thm)],[71]) ).
cnf(l139,plain,
( ~ loca_level_direct_below(admin,confidential,secret)
| ~ loca_level_below(admin,sbu,confidential)
| loca_level_below(admin,sbu,secret) ),
inference(instantiation,[status(thm)],[5]) ).
cnf(l191,plain,
( ~ system_indi_is_credit_admin(system,credit_admin)
| ~ credit_admin_indi_has_credit(credit_admin,alice)
| admin_indi_has_credit(admin,alice) ),
inference(instantiation,[status(thm)],[18]) ).
cnf(l148,plain,
system_compartment_has_sso(system,compartmentb,sso_compartmentb),
inference(instantiation,[status(thm)],[44]) ).
cnf(l174,plain,
( ~ system_indi_is_polygraph_admin(system,polygraph_admin)
| ~ polygraph_admin_indi_has_polygraph(polygraph_admin,alice)
| admin_indi_has_polygraph(admin,alice) ),
inference(instantiation,[status(thm)],[17]) ).
cnf(l166,plain,
sso_file_has_compartments(sso_compartmentb,secretfile,cons(compartmentb,cons(compartmenta,nil))),
inference(instantiation,[status(thm)],[52]) ).
cnf(l132,plain,
loca_level_direct_below(admin,confidential,secret),
inference(instantiation,[status(thm)],[2]) ).
cnf(l221,plain,
admin_file_has_compartments_h(admin,secretfile,cons(compartmentb,cons(compartmenta,nil)),nil),
inference(instantiation,[status(thm)],[9]) ).
cnf(l156,plain,
system_indi_needs_level(system,alice,secret),
inference(instantiation,[status(thm)],[76]) ).
cnf(l155,plain,
( ~ loca_level_below(admin,sbu,topsecret)
| ~ system_indi_is_background_admin(system,background_admin)
| ~ background_admin_indi_has_background(background_admin,alice,topsecret)
| admin_indi_has_background(admin,alice,sbu) ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l204,plain,
system_file_needs_compartments(system,secretfile,cons(compartmentb,cons(compartmenta,nil))),
inference(instantiation,[status(thm)],[51]) ).
cnf(l195,plain,
credit_admin_indi_has_credit(credit_admin,alice),
inference(instantiation,[status(thm)],[73]) ).
cnf(l227,plain,
background_admin_indi_has_background(background_admin,alice,topsecret),
inference(instantiation,[status(thm)],[74]) ).
cnf(l196,plain,
( ~ loca_level_direct_below(admin,secret,topsecret)
| ~ loca_level_below(admin,sbu,secret)
| loca_level_below(admin,sbu,topsecret) ),
inference(instantiation,[status(thm)],[5]) ).
cnf(l223,plain,
( ~ admin_compartment_has_sso(admin,compartmenta,sso_compartmenta)
| ~ system_indi_is_oca(system,oca)
| ~ oca_compartment_has_scg(oca,compartmenta,scg_compartmenta)
| ~ sso_compartment_has_scg(sso_compartmenta,compartmenta,scg_compartmenta)
| admin_compartment_has_scg(admin,compartmenta,scg_compartmenta) ),
inference(instantiation,[status(thm)],[7]) ).
cnf(l182,plain,
( ~ admin_compartment_has_sso(admin,compartmenta,sso_compartmenta)
| ~ system_indi_is_oca(system,oca)
| ~ oca_compartment_has_scg(oca,compartmenta,scg_compartmenta)
| ~ sso_compartment_has_scg(sso_compartmenta,compartmenta,scg_compartmenta)
| admin_compartment_has_scg(admin,compartmenta,scg_compartmenta) ),
inference(instantiation,[status(thm)],[7]) ).
cnf(l228,plain,
loca_level_direct_below(admin,confidential,secret),
inference(instantiation,[status(thm)],[2]) ).
cnf(l188,plain,
( ~ system_compartment_has_sso(system,compartmenta,sso_compartmenta)
| admin_compartment_has_sso(admin,compartmenta,sso_compartmenta) ),
inference(instantiation,[status(thm)],[6]) ).
cnf(l229,plain,
loca_level_direct_below(admin,secret,topsecret),
inference(instantiation,[status(thm)],[3]) ).
cnf(l230,plain,
system_indi_is_credit_admin(system,credit_admin),
inference(instantiation,[status(thm)],[67]) ).
cnf(l219,plain,
system_compartment_has_sso(system,compartmenta,sso_compartmenta),
inference(instantiation,[status(thm)],[47]) ).
cnf(l46,plain,
( ~ loca_level_below(admin,topsecret,topsecret)
| ~ system_indi_is_background_admin(system,background_admin)
| ~ background_admin_indi_has_background(background_admin,alice,topsecret)
| admin_indi_has_background(admin,alice,topsecret) ),
inference(instantiation,[status(thm)],[20]) ).
fof(ax48,plain,
oca_compartment_has_scg(oca,compartmenta,scg_compartmenta),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax48) ).
cnf(48,plain,
oca_compartment_has_scg(oca,compartmenta,scg_compartmenta),
inference(cnf,[status(esa)],[ax48]) ).
cnf(l200,plain,
oca_compartment_has_scg(oca,compartmenta,scg_compartmenta),
inference(instantiation,[status(thm)],[48]) ).
cnf(l198,plain,
polygraph_admin_indi_has_polygraph(polygraph_admin,alice),
inference(instantiation,[status(thm)],[72]) ).
cnf(l231,plain,
system_compartment_has_sso(system,compartmenta,sso_compartmenta),
inference(instantiation,[status(thm)],[47]) ).
cnf(l232,plain,
( ~ loca_level_direct_below(admin,sbu,confidential)
| ~ loca_level_below(admin,sbu,sbu)
| loca_level_below(admin,sbu,confidential) ),
inference(instantiation,[status(thm)],[5]) ).
cnf(l202,plain,
( ~ hr_admin_indi_has_employment(hr_admin,alice)
| ~ system_indi_is_hr_admin(system,hr_admin)
| admin_indi_has_employment(admin,alice) ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l107,plain,
background_admin_indi_has_background(background_admin,alice,topsecret),
inference(instantiation,[status(thm)],[74]) ).
cnf(l233,plain,
system_indi_is_oca(system,oca),
inference(instantiation,[status(thm)],[41]) ).
fof(ax49,plain,
sso_compartment_has_scg(sso_compartmenta,compartmenta,scg_compartmenta),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax49) ).
cnf(49,plain,
sso_compartment_has_scg(sso_compartmenta,compartmenta,scg_compartmenta),
inference(cnf,[status(esa)],[ax49]) ).
cnf(l193,plain,
sso_compartment_has_scg(sso_compartmenta,compartmenta,scg_compartmenta),
inference(instantiation,[status(thm)],[49]) ).
cnf(l234,plain,
( ~ loca_level_direct_below(admin,secret,topsecret)
| ~ loca_level_below(admin,sbu,secret)
| loca_level_below(admin,sbu,topsecret) ),
inference(instantiation,[status(thm)],[5]) ).
fof(ax1,plain,
! [K] : loca_level_direct_below(K,sbu,confidential),
file('Axioms/SWV009+0.ax',ax1) ).
cnf(1,plain,
loca_level_direct_below(X0,sbu,confidential),
inference(cnf,[status(esa)],[ax1]) ).
cnf(l235,plain,
loca_level_direct_below(admin,sbu,confidential),
inference(instantiation,[status(thm)],[1]) ).
cnf(l176,plain,
( ~ loca_level_direct_below(admin,secret,topsecret)
| ~ loca_level_below(admin,secret,secret)
| loca_level_below(admin,secret,topsecret) ),
inference(instantiation,[status(thm)],[5]) ).
cnf(l224,plain,
( ~ system_compartment_has_sso(system,compartmenta,sso_compartmenta)
| admin_compartment_has_sso(admin,compartmenta,sso_compartmenta) ),
inference(instantiation,[status(thm)],[6]) ).
cnf(l164,plain,
system_compartment_has_sso(system,compartmenta,sso_compartmenta),
inference(instantiation,[status(thm)],[47]) ).
cnf(l184,plain,
system_indi_is_oca(system,oca),
inference(instantiation,[status(thm)],[41]) ).
cnf(l242,plain,
( ~ loca_level_direct_below(admin,confidential,secret)
| ~ loca_level_below(admin,sbu,confidential)
| loca_level_below(admin,sbu,secret) ),
inference(instantiation,[status(thm)],[5]) ).
cnf(l192,plain,
system_indi_is_polygraph_admin(system,polygraph_admin),
inference(instantiation,[status(thm)],[66]) ).
cnf(l241,plain,
loca_level_direct_below(admin,secret,topsecret),
inference(instantiation,[status(thm)],[3]) ).
cnf(l243,plain,
system_compartment_has_sso(system,compartmenta,sso_compartmenta),
inference(instantiation,[status(thm)],[47]) ).
cnf(l238,plain,
hr_admin_indi_has_employment(hr_admin,alice),
inference(instantiation,[status(thm)],[75]) ).
fof(ax56,plain,
sso_file_has_level(sso_compartmenta,secretfile,secret,scg_compartmenta),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax56) ).
cnf(56,plain,
sso_file_has_level(sso_compartmenta,secretfile,secret,scg_compartmenta),
inference(cnf,[status(esa)],[ax56]) ).
cnf(l218,plain,
sso_file_has_level(sso_compartmenta,secretfile,secret,scg_compartmenta),
inference(instantiation,[status(thm)],[56]) ).
cnf(l161,plain,
sso_file_has_compartments(sso_compartmenta,secretfile,cons(compartmentb,cons(compartmenta,nil))),
inference(instantiation,[status(thm)],[53]) ).
cnf(l185,plain,
loca_level_below(admin,secret,secret),
inference(instantiation,[status(thm)],[4]) ).
cnf(l239,plain,
sso_compartment_has_scg(sso_compartmenta,compartmenta,scg_compartmenta),
inference(instantiation,[status(thm)],[49]) ).
cnf(l244,plain,
( ~ loca_level_direct_below(admin,sbu,confidential)
| ~ loca_level_below(admin,sbu,sbu)
| loca_level_below(admin,sbu,confidential) ),
inference(instantiation,[status(thm)],[5]) ).
cnf(l237,plain,
loca_level_below(admin,sbu,sbu),
inference(instantiation,[status(thm)],[4]) ).
cnf(l157,plain,
system_indi_is_background_admin(system,background_admin),
inference(instantiation,[status(thm)],[68]) ).
cnf(l106,plain,
system_indi_is_background_admin(system,background_admin),
inference(instantiation,[status(thm)],[68]) ).
cnf(l203,plain,
loca_level_direct_below(admin,secret,topsecret),
inference(instantiation,[status(thm)],[3]) ).
cnf(l240,plain,
system_indi_is_hr_admin(system,hr_admin),
inference(instantiation,[status(thm)],[69]) ).
cnf(l236,plain,
( ~ loca_level_direct_below(admin,confidential,secret)
| ~ loca_level_below(admin,sbu,confidential)
| loca_level_below(admin,sbu,secret) ),
inference(instantiation,[status(thm)],[5]) ).
cnf(l251,plain,
loca_level_below(admin,sbu,sbu),
inference(instantiation,[status(thm)],[4]) ).
fof(ax12,plain,
! [F,L] : admin_file_has_level_h(admin,F,L,nil),
file('Axioms/SWV009+0.ax',ax12) ).
cnf(12,plain,
admin_file_has_level_h(admin,X0,X1,nil),
inference(cnf,[status(esa)],[ax12]) ).
cnf(l220,plain,
admin_file_has_level_h(admin,secretfile,secret,nil),
inference(instantiation,[status(thm)],[12]) ).
cnf(l248,plain,
oca_compartment_has_scg(oca,compartmenta,scg_compartmenta),
inference(instantiation,[status(thm)],[48]) ).
cnf(l250,plain,
loca_level_direct_below(admin,sbu,confidential),
inference(instantiation,[status(thm)],[1]) ).
cnf(l249,plain,
loca_level_direct_below(admin,confidential,secret),
inference(instantiation,[status(thm)],[2]) ).
cnf(l153,plain,
( ~ system_indi_has_citizenship(system,alice,usa)
| admin_indi_has_citizenship(admin,alice,usa) ),
inference(instantiation,[status(thm)],[23]) ).
cnf(l112,plain,
loca_level_below(admin,topsecret,topsecret),
inference(instantiation,[status(thm)],[4]) ).
cnf(l246,plain,
( ~ loca_level_direct_below(admin,sbu,confidential)
| ~ loca_level_below(admin,sbu,sbu)
| loca_level_below(admin,sbu,confidential) ),
inference(instantiation,[status(thm)],[5]) ).
cnf(l194,plain,
system_indi_has_citizenship(system,alice,usa),
inference(instantiation,[status(thm)],[71]) ).
cnf(l247,plain,
loca_level_below(admin,sbu,sbu),
inference(instantiation,[status(thm)],[4]) ).
cnf(l255,plain,
loca_level_direct_below(admin,sbu,confidential),
inference(instantiation,[status(thm)],[1]) ).
cnf(l245,plain,
loca_level_direct_below(admin,confidential,secret),
inference(instantiation,[status(thm)],[2]) ).
cnf(final,plain,
$false,
inference(ground_refutation,[status(thm)],[l0,l1,l2,l4,l5,l6,l7,l8,l9,l10,l11,l12,l13,l14,l15,l16,l17,l20,l27,l25,l28,l18,l81,l3,l31,l73,l67,l80,l82,l79,l65,l56,l26,l21,l32,l34,l19,l83,l43,l49,l84,l78,l41,l53,l39,l57,l74,l85,l58,l72,l86,l36,l87,l88,l60,l22,l89,l90,l91,l35,l62,l37,l44,l92,l29,l93,l94,l95,l96,l42,l97,l98,l64,l99,l70,l76,l33,l147,l143,l102,l105,l66,l146,l38,l30,l47,l71,l104,l100,l45,l168,l149,l115,l77,l175,l48,l173,l134,l108,l138,l154,l128,l141,l140,l55,l118,l117,l52,l124,l69,l109,l103,l51,l111,l178,l171,l163,l114,l180,l23,l59,l50,l122,l133,l165,l54,l40,l63,l130,l142,l61,l186,l121,l68,l75,l110,l177,l172,l151,l144,l183,l126,l179,l205,l145,l206,l120,l167,l181,l24,l207,l150,l119,l159,l208,l170,l101,l209,l210,l136,l187,l211,l135,l160,l212,l213,l201,l190,l214,l215,l216,l129,l162,l217,l169,l113,l139,l191,l148,l174,l166,l132,l221,l156,l155,l204,l195,l227,l196,l223,l182,l228,l188,l229,l230,l219,l46,l200,l198,l231,l232,l202,l107,l233,l193,l234,l235,l176,l224,l164,l184,l242,l192,l241,l243,l238,l218,l161,l185,l239,l244,l237,l157,l106,l203,l240,l236,l251,l220,l248,l250,l249,l153,l112,l246,l194,l247,l255,l245]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.07 % Problem : SWV437+1 : TPTP v9.0.0. Released v4.0.0.
% 0.00/0.07 % Command : /export/starexec/sandbox2/solver/bin/execute.py 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.06/0.26 % Computer : n022.cluster.edu
% 0.06/0.26 % Model : x86_64 x86_64
% 0.06/0.26 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.06/0.26 % Memory : 8042.1875MB
% 0.06/0.26 % OS : Linux 3.10.0-693.el7.x86_64
% 0.06/0.26 % CPULimit : 300
% 0.06/0.26 % WCLimit : 300
% 0.06/0.26 % DateTime : Tue Jul 22 09:37:34 EDT 2025
% 0.06/0.26 % CPUTime :
% 0.06/0.26 % launching worker at depth: 1
% 0.06/0.26 % launching worker at depth: 2
% 0.06/0.26 % launching worker at depth: 3
% 0.06/0.26 % launching worker at depth: 4
% 0.06/0.26 % launching worker at depth: 5
% 0.06/0.26 % launching worker at depth: 6
% 0.06/0.26 % launching worker at depth: 8
% 0.06/0.26 % launching worker at depth: 7
% 0.06/0.26 % launching worker at depth: 9
% 0.06/0.26 % launching worker at depth: 10
% 0.06/0.26 % launching worker at depth: 11
% 0.06/0.26 % launching worker at depth: 12
% 0.06/0.27 % launching worker at depth: 13
% 0.06/0.27 % launching worker at depth: 14
% 0.06/0.27 % launching worker at depth: 15
% 0.06/0.30 % launching worker at depth: 16
% 0.06/0.30 % launching worker at depth: 17
% 0.11/0.31 % launching worker at depth: 18
% 0.11/0.32 % SZS status Theorem for theBenchmark
% 0.11/0.32 % SZS output start CNFRefutation
% See solution above
%------------------------------------------------------------------------------