%------------------------------------------------------------------------------
% File : Beagle---0.9.52
% Problem : SWV437+1 : TPTP v9.0.0. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : java -Dfile.encoding=UTF-8 -Xms512M -Xmx4G -Xss10M -jar /export/starexec/sandbox/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox/solver/bin/cvc4-1.4-x86_64-linux-opt -liasolver cooper -t %d %s
% Computer : n032.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 : Wed Apr 9 09:30:35 PM UTC 2025
% Result : Theorem 7.40s 2.55s
% Output : CNFRefutation 7.74s
% Verified :
% SZS Type : Refutation
% Derivation depth : 16
% Number of leaves : 68
% Syntax : Number of formulae : 286 ( 155 unt; 0 typ; 0 def)
% Number of atoms : 646 ( 0 equ)
% Maximal formula atoms : 11 ( 2 avg)
% Number of connectives : 679 ( 319 ~; 283 |; 0 &)
% ( 0 <=>; 77 =>; 0 <=; 0 <~>)
% Maximal formula depth : 17 ( 4 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of types : 2 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 56 ( 55 usr; 1 prp; 0-6 aty)
% Number of functors : 34 ( 34 usr; 33 con; 0-2 aty)
% Number of variables : 337 ( 337 !; 0 ?; 0 :)
% Comments :
%------------------------------------------------------------------------------
%$ oca_compartment_is_compartment > sso_file_has_level > sso_file_has_citizenship > admin_indi_may_file > admin_file_has_level_h > admin_file_has_compartments_h > admin_file_has_citizenship_h > system_indi_needs_level > system_indi_needs_compartment > system_indi_is_counterintelligence > system_indi_has_citizenship > system_file_needs_level > system_file_needs_compartments > system_file_needs_citizenship > system_compartment_has_sso > sso_indi_has_compartment > sso_file_has_compartments > sso_compartment_has_scg > owner_indi_has_need_to_know > oca_compartment_has_scg > loca_level_direct_below > loca_level_below > level_admin_indi_has_level > background_admin_indi_has_background > admin_indi_has_polygraph_for_compartment > admin_indi_has_need_to_know_for_file > admin_indi_has_level_for_file > admin_indi_has_level_for_compartment > admin_indi_has_level > admin_indi_has_credit_for_compartment > admin_indi_has_compartments_for_file > admin_indi_has_compartments > admin_indi_has_citizenship_for_file > admin_indi_has_citizenship > admin_indi_has_background_for_compartment > admin_indi_has_background > admin_file_has_level > admin_file_has_compartments > admin_file_has_citizenship > admin_compartment_has_sso > admin_compartment_has_scg > system_indi_is_polygraph_admin > system_indi_is_oca > system_indi_is_level_admin > system_indi_is_hr_admin > system_indi_is_credit_admin > system_indi_is_background_admin > state_file_has_owner > polygraph_admin_indi_has_polygraph > hr_admin_indi_has_employment > credit_admin_indi_has_credit > admin_indi_has_polygraph > admin_indi_has_employment > admin_indi_has_credit > state_file_is_not_working_paper > cons > #nlpp > yes > usa > unclassified > topsecret > system > sso_compartmentb > sso_compartmenta > secretfile > secret > scg_compartmentb > scg_compartmenta > sbu > read > polygraph_admin > owner_secretfile > owner_not_secretfile > oca > not_secretfile > no > nil > level_admin > india > hr_admin > credit_admin > confidential > compartmentb > compartmenta > ci > background_admin > babu > anycountry > alice > admin
%Foreground sorts:
%Background operators:
%Foreground operators:
tff(secretfile,type,
secretfile: $i ).
tff(admin_indi_has_employment,type,
admin_indi_has_employment: ( $i * $i ) > $o ).
tff(admin_indi_may_file,type,
admin_indi_may_file: ( $i * $i * $i * $i ) > $o ).
tff(system_file_needs_level,type,
system_file_needs_level: ( $i * $i * $i ) > $o ).
tff(background_admin,type,
background_admin: $i ).
tff(polygraph_admin_indi_has_polygraph,type,
polygraph_admin_indi_has_polygraph: ( $i * $i ) > $o ).
tff(admin_indi_has_level_for_file,type,
admin_indi_has_level_for_file: ( $i * $i * $i ) > $o ).
tff(admin_indi_has_citizenship,type,
admin_indi_has_citizenship: ( $i * $i * $i ) > $o ).
tff(admin_indi_has_level_for_compartment,type,
admin_indi_has_level_for_compartment: ( $i * $i * $i ) > $o ).
tff(system_file_needs_citizenship,type,
system_file_needs_citizenship: ( $i * $i * $i ) > $o ).
tff(hr_admin,type,
hr_admin: $i ).
tff(babu,type,
babu: $i ).
tff(confidential,type,
confidential: $i ).
tff(scg_compartmenta,type,
scg_compartmenta: $i ).
tff(not_secretfile,type,
not_secretfile: $i ).
tff(india,type,
india: $i ).
tff(sso_compartmenta,type,
sso_compartmenta: $i ).
tff(admin_indi_has_credit,type,
admin_indi_has_credit: ( $i * $i ) > $o ).
tff(system_compartment_has_sso,type,
system_compartment_has_sso: ( $i * $i * $i ) > $o ).
tff(topsecret,type,
topsecret: $i ).
tff(owner_not_secretfile,type,
owner_not_secretfile: $i ).
tff(admin_indi_has_citizenship_for_file,type,
admin_indi_has_citizenship_for_file: ( $i * $i * $i ) > $o ).
tff(unclassified,type,
unclassified: $i ).
tff(compartmenta,type,
compartmenta: $i ).
tff(yes,type,
yes: $i ).
tff(system_indi_is_level_admin,type,
system_indi_is_level_admin: ( $i * $i ) > $o ).
tff(no,type,
no: $i ).
tff(read,type,
read: $i ).
tff(credit_admin,type,
credit_admin: $i ).
tff(system_file_needs_compartments,type,
system_file_needs_compartments: ( $i * $i * $i ) > $o ).
tff(admin_indi_has_compartments_for_file,type,
admin_indi_has_compartments_for_file: ( $i * $i * $i ) > $o ).
tff(sbu,type,
sbu: $i ).
tff(secret,type,
secret: $i ).
tff(admin_compartment_has_scg,type,
admin_compartment_has_scg: ( $i * $i * $i ) > $o ).
tff(usa,type,
usa: $i ).
tff(background_admin_indi_has_background,type,
background_admin_indi_has_background: ( $i * $i * $i ) > $o ).
tff(admin_file_has_level,type,
admin_file_has_level: ( $i * $i * $i ) > $o ).
tff(system_indi_is_oca,type,
system_indi_is_oca: ( $i * $i ) > $o ).
tff(system_indi_is_counterintelligence,type,
system_indi_is_counterintelligence: ( $i * $i * $i ) > $o ).
tff(admin_indi_has_need_to_know_for_file,type,
admin_indi_has_need_to_know_for_file: ( $i * $i * $i ) > $o ).
tff(system_indi_has_citizenship,type,
system_indi_has_citizenship: ( $i * $i * $i ) > $o ).
tff(admin,type,
admin: $i ).
tff(system_indi_needs_compartment,type,
system_indi_needs_compartment: ( $i * $i * $i ) > $o ).
tff(sso_file_has_level,type,
sso_file_has_level: ( $i * $i * $i * $i ) > $o ).
tff(system_indi_is_polygraph_admin,type,
system_indi_is_polygraph_admin: ( $i * $i ) > $o ).
tff(sso_compartmentb,type,
sso_compartmentb: $i ).
tff(scg_compartmentb,type,
scg_compartmentb: $i ).
tff(compartmentb,type,
compartmentb: $i ).
tff(sso_file_has_citizenship,type,
sso_file_has_citizenship: ( $i * $i * $i * $i ) > $o ).
tff(sso_file_has_compartments,type,
sso_file_has_compartments: ( $i * $i * $i ) > $o ).
tff(admin_indi_has_credit_for_compartment,type,
admin_indi_has_credit_for_compartment: ( $i * $i * $i ) > $o ).
tff(admin_file_has_compartments,type,
admin_file_has_compartments: ( $i * $i * $i ) > $o ).
tff(credit_admin_indi_has_credit,type,
credit_admin_indi_has_credit: ( $i * $i ) > $o ).
tff(admin_indi_has_polygraph,type,
admin_indi_has_polygraph: ( $i * $i ) > $o ).
tff(admin_file_has_citizenship,type,
admin_file_has_citizenship: ( $i * $i * $i ) > $o ).
tff(oca,type,
oca: $i ).
tff(state_file_has_owner,type,
state_file_has_owner: ( $i * $i ) > $o ).
tff(anycountry,type,
anycountry: $i ).
tff(system_indi_is_background_admin,type,
system_indi_is_background_admin: ( $i * $i ) > $o ).
tff(admin_indi_has_background,type,
admin_indi_has_background: ( $i * $i * $i ) > $o ).
tff(admin_file_has_citizenship_h,type,
admin_file_has_citizenship_h: ( $i * $i * $i * $i ) > $o ).
tff(sso_compartment_has_scg,type,
sso_compartment_has_scg: ( $i * $i * $i ) > $o ).
tff(admin_file_has_compartments_h,type,
admin_file_has_compartments_h: ( $i * $i * $i * $i ) > $o ).
tff(admin_indi_has_compartments,type,
admin_indi_has_compartments: ( $i * $i * $i ) > $o ).
tff(admin_file_has_level_h,type,
admin_file_has_level_h: ( $i * $i * $i * $i ) > $o ).
tff(hr_admin_indi_has_employment,type,
hr_admin_indi_has_employment: ( $i * $i ) > $o ).
tff(polygraph_admin,type,
polygraph_admin: $i ).
tff(cons,type,
cons: ( $i * $i ) > $i ).
tff(oca_compartment_has_scg,type,
oca_compartment_has_scg: ( $i * $i * $i ) > $o ).
tff(system,type,
system: $i ).
tff(loca_level_below,type,
loca_level_below: ( $i * $i * $i ) > $o ).
tff(admin_indi_has_polygraph_for_compartment,type,
admin_indi_has_polygraph_for_compartment: ( $i * $i * $i ) > $o ).
tff(state_file_is_not_working_paper,type,
state_file_is_not_working_paper: $i > $o ).
tff(level_admin,type,
level_admin: $i ).
tff(system_indi_is_hr_admin,type,
system_indi_is_hr_admin: ( $i * $i ) > $o ).
tff(admin_compartment_has_sso,type,
admin_compartment_has_sso: ( $i * $i * $i ) > $o ).
tff(system_indi_is_credit_admin,type,
system_indi_is_credit_admin: ( $i * $i ) > $o ).
tff(system_indi_needs_level,type,
system_indi_needs_level: ( $i * $i * $i ) > $o ).
tff(loca_level_direct_below,type,
loca_level_direct_below: ( $i * $i * $i ) > $o ).
tff(oca_compartment_is_compartment,type,
oca_compartment_is_compartment: ( $i * $i * $i * $i * $i * $i ) > $o ).
tff(admin_indi_has_background_for_compartment,type,
admin_indi_has_background_for_compartment: ( $i * $i * $i ) > $o ).
tff(owner_secretfile,type,
owner_secretfile: $i ).
tff(sso_indi_has_compartment,type,
sso_indi_has_compartment: ( $i * $i * $i ) > $o ).
tff(nil,type,
nil: $i ).
tff(level_admin_indi_has_level,type,
level_admin_indi_has_level: ( $i * $i * $i ) > $o ).
tff(alice,type,
alice: $i ).
tff(admin_indi_has_level,type,
admin_indi_has_level: ( $i * $i * $i ) > $o ).
tff(ci,type,
ci: $i ).
tff(owner_indi_has_need_to_know,type,
owner_indi_has_need_to_know: ( $i * $i * $i ) > $o ).
tff(f_316,hypothesis,
system_compartment_has_sso(system,compartmenta,sso_compartmenta),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax47) ).
tff(f_69,axiom,
! [C,SSO] :
( system_compartment_has_sso(system,C,SSO)
=> admin_compartment_has_sso(admin,C,SSO) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWV009+0.ax',ax6) ).
tff(f_310,hypothesis,
system_indi_is_oca(system,oca),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax41) ).
tff(f_317,hypothesis,
oca_compartment_has_scg(oca,compartmenta,scg_compartmenta),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax48) ).
tff(f_318,hypothesis,
sso_compartment_has_scg(sso_compartmenta,compartmenta,scg_compartmenta),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax49) ).
tff(f_79,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/sandbox/benchmark/Axioms/SWV009+0.ax',ax7) ).
tff(f_105,axiom,
! [F,L] : admin_file_has_level_h(admin,F,L,nil),
file('/export/starexec/sandbox/benchmark/Axioms/SWV009+0.ax',ax12) ).
tff(f_325,hypothesis,
sso_file_has_level(sso_compartmenta,secretfile,secret,scg_compartmenta),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax56) ).
tff(f_115,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/sandbox/benchmark/Axioms/SWV009+0.ax',ax13) ).
tff(f_313,hypothesis,
system_compartment_has_sso(system,compartmentb,sso_compartmentb),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax44) ).
tff(f_314,hypothesis,
oca_compartment_has_scg(oca,compartmentb,scg_compartmentb),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax45) ).
tff(f_315,hypothesis,
sso_compartment_has_scg(sso_compartmentb,compartmentb,scg_compartmentb),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax46) ).
tff(f_87,axiom,
! [F,CL] : admin_file_has_compartments_h(admin,F,CL,nil),
file('/export/starexec/sandbox/benchmark/Axioms/SWV009+0.ax',ax9) ).
tff(f_322,hypothesis,
sso_file_has_compartments(sso_compartmenta,secretfile,cons(compartmentb,cons(compartmenta,nil))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax53) ).
tff(f_95,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/sandbox/benchmark/Axioms/SWV009+0.ax',ax10) ).
tff(f_320,hypothesis,
system_file_needs_compartments(system,secretfile,cons(compartmentb,cons(compartmenta,nil))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax51) ).
tff(f_321,hypothesis,
sso_file_has_compartments(sso_compartmentb,secretfile,cons(compartmentb,cons(compartmenta,nil))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax52) ).
tff(f_85,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/sandbox/benchmark/Axioms/SWV009+0.ax',ax8) ).
tff(f_323,hypothesis,
system_file_needs_level(system,secretfile,secret),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax54) ).
tff(f_324,hypothesis,
sso_file_has_level(sso_compartmentb,secretfile,secret,scg_compartmentb),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax55) ).
tff(f_103,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/sandbox/benchmark/Axioms/SWV009+0.ax',ax11) ).
tff(f_59,axiom,
! [K,L] : loca_level_below(K,L,L),
file('/export/starexec/sandbox/benchmark/Axioms/SWV009+0.ax',ax4) ).
tff(f_345,hypothesis,
system_indi_needs_level(system,alice,secret),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax76) ).
tff(f_340,hypothesis,
system_indi_has_citizenship(system,alice,usa),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax71) ).
tff(f_169,axiom,
! [K,U] :
( system_indi_has_citizenship(system,K,U)
=> admin_indi_has_citizenship(admin,K,U) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWV009+0.ax',ax23) ).
tff(f_335,hypothesis,
system_indi_is_polygraph_admin(system,polygraph_admin),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax66) ).
tff(f_341,hypothesis,
polygraph_admin_indi_has_polygraph(polygraph_admin,alice),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax72) ).
tff(f_141,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/sandbox/benchmark/Axioms/SWV009+0.ax',ax17) ).
tff(f_338,hypothesis,
system_indi_is_hr_admin(system,hr_admin),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax69) ).
tff(f_344,hypothesis,
hr_admin_indi_has_employment(hr_admin,alice),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax75) ).
tff(f_163,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/sandbox/benchmark/Axioms/SWV009+0.ax',ax21) ).
tff(f_336,hypothesis,
system_indi_is_credit_admin(system,credit_admin),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax67) ).
tff(f_342,hypothesis,
credit_admin_indi_has_credit(credit_admin,alice),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax73) ).
tff(f_147,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/sandbox/benchmark/Axioms/SWV009+0.ax',ax18) ).
tff(f_339,hypothesis,
system_indi_is_level_admin(system,level_admin),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax70) ).
tff(f_337,hypothesis,
system_indi_is_background_admin(system,background_admin),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax68) ).
tff(f_343,hypothesis,
background_admin_indi_has_background(background_admin,alice,topsecret),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax74) ).
tff(f_57,axiom,
! [K] : loca_level_direct_below(K,secret,topsecret),
file('/export/starexec/sandbox/benchmark/Axioms/SWV009+0.ax',ax3) ).
tff(f_65,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/sandbox/benchmark/Axioms/SWV009+0.ax',ax5) ).
tff(f_157,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/sandbox/benchmark/Axioms/SWV009+0.ax',ax20) ).
tff(f_346,hypothesis,
level_admin_indi_has_level(level_admin,alice,topsecret),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax77) ).
tff(f_193,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/sandbox/benchmark/Axioms/SWV009+0.ax',ax25) ).
tff(f_273,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/sandbox/benchmark/Axioms/SWV009+0.ax',ax35) ).
tff(f_195,axiom,
! [K] : admin_indi_has_compartments(admin,K,nil),
file('/export/starexec/sandbox/benchmark/Axioms/SWV009+0.ax',ax26) ).
tff(f_348,hypothesis,
system_indi_needs_compartment(system,alice,compartmenta),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax79) ).
tff(f_312,hypothesis,
oca_compartment_is_compartment(oca,compartmenta,sbu,unclassified,no,no),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax43) ).
tff(f_247,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/sandbox/benchmark/Axioms/SWV009+0.ax',ax31) ).
tff(f_261,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/sandbox/benchmark/Axioms/SWV009+0.ax',ax33) ).
tff(f_149,axiom,
! [K] : admin_indi_has_background(admin,K,unclassified),
file('/export/starexec/sandbox/benchmark/Axioms/SWV009+0.ax',ax19) ).
tff(f_225,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/sandbox/benchmark/Axioms/SWV009+0.ax',ax28) ).
tff(f_350,hypothesis,
sso_indi_has_compartment(sso_compartmenta,alice,compartmenta),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax81) ).
tff(f_217,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/sandbox/benchmark/Axioms/SWV009+0.ax',ax27) ).
tff(f_55,axiom,
! [K] : loca_level_direct_below(K,confidential,secret),
file('/export/starexec/sandbox/benchmark/Axioms/SWV009+0.ax',ax2) ).
tff(f_53,axiom,
! [K] : loca_level_direct_below(K,sbu,confidential),
file('/export/starexec/sandbox/benchmark/Axioms/SWV009+0.ax',ax1) ).
tff(f_233,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/sandbox/benchmark/Axioms/SWV009+0.ax',ax29) ).
tff(f_289,axiom,
! [K,F] :
( admin_indi_has_citizenship(admin,K,usa)
=> admin_indi_has_citizenship_for_file(admin,K,F) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWV009+0.ax',ax38) ).
tff(f_319,hypothesis,
state_file_is_not_working_paper(secretfile),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax50) ).
tff(f_329,hypothesis,
state_file_has_owner(secretfile,owner_secretfile),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax60) ).
tff(f_351,hypothesis,
owner_indi_has_need_to_know(owner_secretfile,alice,secretfile),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax82) ).
tff(f_279,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/sandbox/benchmark/Axioms/SWV009+0.ax',ax36) ).
tff(f_301,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/sandbox/benchmark/Axioms/SWV009+0.ax',ax39) ).
tff(f_357,negated_conjecture,
~ admin_indi_may_file(admin,alice,secretfile,read),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',alicereadsecret) ).
tff(f_311,hypothesis,
oca_compartment_is_compartment(oca,compartmentb,confidential,topsecret,yes,yes),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax42) ).
tff(f_255,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/sandbox/benchmark/Axioms/SWV009+0.ax',ax32) ).
tff(f_241,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/sandbox/benchmark/Axioms/SWV009+0.ax',ax30) ).
tff(f_347,hypothesis,
system_indi_needs_compartment(system,alice,compartmentb),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax78) ).
tff(f_349,hypothesis,
sso_indi_has_compartment(sso_compartmentb,alice,compartmentb),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax80) ).
tff(f_267,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/sandbox/benchmark/Axioms/SWV009+0.ax',ax34) ).
tff(c_96,plain,
system_compartment_has_sso(system,compartmenta,sso_compartmenta),
inference(cnfTransformation,[status(thm)],[f_316]) ).
tff(c_198,plain,
! [C_148,SSO_149] :
( admin_compartment_has_sso(admin,C_148,SSO_149)
| ~ system_compartment_has_sso(system,C_148,SSO_149) ),
inference(cnfTransformation,[status(thm)],[f_69]) ).
tff(c_206,plain,
admin_compartment_has_sso(admin,compartmenta,sso_compartmenta),
inference(resolution,[status(thm)],[c_96,c_198]) ).
tff(c_84,plain,
system_indi_is_oca(system,oca),
inference(cnfTransformation,[status(thm)],[f_310]) ).
tff(c_98,plain,
oca_compartment_has_scg(oca,compartmenta,scg_compartmenta),
inference(cnfTransformation,[status(thm)],[f_317]) ).
tff(c_100,plain,
sso_compartment_has_scg(sso_compartmenta,compartmenta,scg_compartmenta),
inference(cnfTransformation,[status(thm)],[f_318]) ).
tff(c_547,plain,
! [C_306,SCG_307,SSO_308,OCA_309] :
( admin_compartment_has_scg(admin,C_306,SCG_307)
| ~ sso_compartment_has_scg(SSO_308,C_306,SCG_307)
| ~ admin_compartment_has_sso(admin,C_306,SSO_308)
| ~ oca_compartment_has_scg(OCA_309,C_306,SCG_307)
| ~ system_indi_is_oca(system,OCA_309) ),
inference(cnfTransformation,[status(thm)],[f_79]) ).
tff(c_551,plain,
! [OCA_309] :
( admin_compartment_has_scg(admin,compartmenta,scg_compartmenta)
| ~ admin_compartment_has_sso(admin,compartmenta,sso_compartmenta)
| ~ oca_compartment_has_scg(OCA_309,compartmenta,scg_compartmenta)
| ~ system_indi_is_oca(system,OCA_309) ),
inference(resolution,[status(thm)],[c_100,c_547]) ).
tff(c_557,plain,
! [OCA_309] :
( admin_compartment_has_scg(admin,compartmenta,scg_compartmenta)
| ~ oca_compartment_has_scg(OCA_309,compartmenta,scg_compartmenta)
| ~ system_indi_is_oca(system,OCA_309) ),
inference(demodulation,[status(thm),theory(equality)],[c_206,c_551]) ).
tff(c_576,plain,
! [OCA_316] :
( ~ oca_compartment_has_scg(OCA_316,compartmenta,scg_compartmenta)
| ~ system_indi_is_oca(system,OCA_316) ),
inference(splitLeft,[status(thm)],[c_557]) ).
tff(c_579,plain,
~ system_indi_is_oca(system,oca),
inference(resolution,[status(thm)],[c_98,c_576]) ).
tff(c_583,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_84,c_579]) ).
tff(c_584,plain,
admin_compartment_has_scg(admin,compartmenta,scg_compartmenta),
inference(splitRight,[status(thm)],[c_557]) ).
tff(c_26,plain,
! [F_29,L_30] : admin_file_has_level_h(admin,F_29,L_30,nil),
inference(cnfTransformation,[status(thm)],[f_105]) ).
tff(c_114,plain,
sso_file_has_level(sso_compartmenta,secretfile,secret,scg_compartmenta),
inference(cnfTransformation,[status(thm)],[f_325]) ).
tff(c_1385,plain,
! [F_565,CL_566,L_562,SCG_564,SSO_561,C_563] :
( admin_file_has_level_h(admin,F_565,L_562,cons(C_563,CL_566))
| ~ admin_file_has_level_h(admin,F_565,L_562,CL_566)
| ~ sso_file_has_level(SSO_561,F_565,L_562,SCG_564)
| ~ admin_compartment_has_scg(admin,C_563,SCG_564)
| ~ admin_compartment_has_sso(admin,C_563,SSO_561) ),
inference(cnfTransformation,[status(thm)],[f_115]) ).
tff(c_1391,plain,
! [C_563,CL_566] :
( admin_file_has_level_h(admin,secretfile,secret,cons(C_563,CL_566))
| ~ admin_file_has_level_h(admin,secretfile,secret,CL_566)
| ~ admin_compartment_has_scg(admin,C_563,scg_compartmenta)
| ~ admin_compartment_has_sso(admin,C_563,sso_compartmenta) ),
inference(resolution,[status(thm)],[c_114,c_1385]) ).
tff(c_90,plain,
system_compartment_has_sso(system,compartmentb,sso_compartmentb),
inference(cnfTransformation,[status(thm)],[f_313]) ).
tff(c_205,plain,
admin_compartment_has_sso(admin,compartmentb,sso_compartmentb),
inference(resolution,[status(thm)],[c_90,c_198]) ).
tff(c_92,plain,
oca_compartment_has_scg(oca,compartmentb,scg_compartmentb),
inference(cnfTransformation,[status(thm)],[f_314]) ).
tff(c_94,plain,
sso_compartment_has_scg(sso_compartmentb,compartmentb,scg_compartmentb),
inference(cnfTransformation,[status(thm)],[f_315]) ).
tff(c_549,plain,
! [OCA_309] :
( admin_compartment_has_scg(admin,compartmentb,scg_compartmentb)
| ~ admin_compartment_has_sso(admin,compartmentb,sso_compartmentb)
| ~ oca_compartment_has_scg(OCA_309,compartmentb,scg_compartmentb)
| ~ system_indi_is_oca(system,OCA_309) ),
inference(resolution,[status(thm)],[c_94,c_547]) ).
tff(c_554,plain,
! [OCA_309] :
( admin_compartment_has_scg(admin,compartmentb,scg_compartmentb)
| ~ oca_compartment_has_scg(OCA_309,compartmentb,scg_compartmentb)
| ~ system_indi_is_oca(system,OCA_309) ),
inference(demodulation,[status(thm),theory(equality)],[c_205,c_549]) ).
tff(c_559,plain,
! [OCA_310] :
( ~ oca_compartment_has_scg(OCA_310,compartmentb,scg_compartmentb)
| ~ system_indi_is_oca(system,OCA_310) ),
inference(splitLeft,[status(thm)],[c_554]) ).
tff(c_562,plain,
~ system_indi_is_oca(system,oca),
inference(resolution,[status(thm)],[c_92,c_559]) ).
tff(c_566,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_84,c_562]) ).
tff(c_567,plain,
admin_compartment_has_scg(admin,compartmentb,scg_compartmentb),
inference(splitRight,[status(thm)],[c_554]) ).
tff(c_20,plain,
! [F_19,CL_20] : admin_file_has_compartments_h(admin,F_19,CL_20,nil),
inference(cnfTransformation,[status(thm)],[f_87]) ).
tff(c_108,plain,
sso_file_has_compartments(sso_compartmenta,secretfile,cons(compartmentb,cons(compartmenta,nil))),
inference(cnfTransformation,[status(thm)],[f_322]) ).
tff(c_568,plain,
! [CL_315,C1_311,SSO_312,CL1_314,F_313] :
( admin_file_has_compartments_h(admin,F_313,CL_315,cons(C1_311,CL1_314))
| ~ admin_file_has_compartments_h(admin,F_313,CL_315,CL1_314)
| ~ sso_file_has_compartments(SSO_312,F_313,CL_315)
| ~ admin_compartment_has_sso(admin,C1_311,SSO_312) ),
inference(cnfTransformation,[status(thm)],[f_95]) ).
tff(c_1705,plain,
! [C1_630,CL1_631] :
( admin_file_has_compartments_h(admin,secretfile,cons(compartmentb,cons(compartmenta,nil)),cons(C1_630,CL1_631))
| ~ admin_file_has_compartments_h(admin,secretfile,cons(compartmentb,cons(compartmenta,nil)),CL1_631)
| ~ admin_compartment_has_sso(admin,C1_630,sso_compartmenta) ),
inference(resolution,[status(thm)],[c_108,c_568]) ).
tff(c_104,plain,
system_file_needs_compartments(system,secretfile,cons(compartmentb,cons(compartmenta,nil))),
inference(cnfTransformation,[status(thm)],[f_320]) ).
tff(c_106,plain,
sso_file_has_compartments(sso_compartmentb,secretfile,cons(compartmentb,cons(compartmenta,nil))),
inference(cnfTransformation,[status(thm)],[f_321]) ).
tff(c_1690,plain,
! [C1_628,CL1_629] :
( admin_file_has_compartments_h(admin,secretfile,cons(compartmentb,cons(compartmenta,nil)),cons(C1_628,CL1_629))
| ~ admin_file_has_compartments_h(admin,secretfile,cons(compartmentb,cons(compartmenta,nil)),CL1_629)
| ~ admin_compartment_has_sso(admin,C1_628,sso_compartmentb) ),
inference(resolution,[status(thm)],[c_106,c_568]) ).
tff(c_18,plain,
! [F_17,CL_18] :
( admin_file_has_compartments(admin,F_17,CL_18)
| ~ admin_file_has_compartments_h(admin,F_17,CL_18,CL_18)
| ~ system_file_needs_compartments(system,F_17,CL_18) ),
inference(cnfTransformation,[status(thm)],[f_85]) ).
tff(c_1694,plain,
( admin_file_has_compartments(admin,secretfile,cons(compartmentb,cons(compartmenta,nil)))
| ~ system_file_needs_compartments(system,secretfile,cons(compartmentb,cons(compartmenta,nil)))
| ~ admin_file_has_compartments_h(admin,secretfile,cons(compartmentb,cons(compartmenta,nil)),cons(compartmenta,nil))
| ~ admin_compartment_has_sso(admin,compartmentb,sso_compartmentb) ),
inference(resolution,[status(thm)],[c_1690,c_18]) ).
tff(c_1697,plain,
( admin_file_has_compartments(admin,secretfile,cons(compartmentb,cons(compartmenta,nil)))
| ~ admin_file_has_compartments_h(admin,secretfile,cons(compartmentb,cons(compartmenta,nil)),cons(compartmenta,nil)) ),
inference(demodulation,[status(thm),theory(equality)],[c_205,c_104,c_1694]) ).
tff(c_1698,plain,
~ admin_file_has_compartments_h(admin,secretfile,cons(compartmentb,cons(compartmenta,nil)),cons(compartmenta,nil)),
inference(splitLeft,[status(thm)],[c_1697]) ).
tff(c_1708,plain,
( ~ admin_file_has_compartments_h(admin,secretfile,cons(compartmentb,cons(compartmenta,nil)),nil)
| ~ admin_compartment_has_sso(admin,compartmenta,sso_compartmenta) ),
inference(resolution,[status(thm)],[c_1705,c_1698]) ).
tff(c_1716,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_206,c_20,c_1708]) ).
tff(c_1717,plain,
admin_file_has_compartments(admin,secretfile,cons(compartmentb,cons(compartmenta,nil))),
inference(splitRight,[status(thm)],[c_1697]) ).
tff(c_110,plain,
system_file_needs_level(system,secretfile,secret),
inference(cnfTransformation,[status(thm)],[f_323]) ).
tff(c_112,plain,
sso_file_has_level(sso_compartmentb,secretfile,secret,scg_compartmentb),
inference(cnfTransformation,[status(thm)],[f_324]) ).
tff(c_1394,plain,
! [C_577,CL_578] :
( admin_file_has_level_h(admin,secretfile,secret,cons(C_577,CL_578))
| ~ admin_file_has_level_h(admin,secretfile,secret,CL_578)
| ~ admin_compartment_has_scg(admin,C_577,scg_compartmentb)
| ~ admin_compartment_has_sso(admin,C_577,sso_compartmentb) ),
inference(resolution,[status(thm)],[c_112,c_1385]) ).
tff(c_24,plain,
! [F_26,L_27,CL_28] :
( admin_file_has_level(admin,F_26,L_27)
| ~ admin_file_has_level_h(admin,F_26,L_27,CL_28)
| ~ admin_file_has_compartments(admin,F_26,CL_28)
| ~ system_file_needs_level(system,F_26,L_27) ),
inference(cnfTransformation,[status(thm)],[f_103]) ).
tff(c_1397,plain,
! [C_577,CL_578] :
( admin_file_has_level(admin,secretfile,secret)
| ~ admin_file_has_compartments(admin,secretfile,cons(C_577,CL_578))
| ~ system_file_needs_level(system,secretfile,secret)
| ~ admin_file_has_level_h(admin,secretfile,secret,CL_578)
| ~ admin_compartment_has_scg(admin,C_577,scg_compartmentb)
| ~ admin_compartment_has_sso(admin,C_577,sso_compartmentb) ),
inference(resolution,[status(thm)],[c_1394,c_24]) ).
tff(c_1400,plain,
! [C_577,CL_578] :
( admin_file_has_level(admin,secretfile,secret)
| ~ admin_file_has_compartments(admin,secretfile,cons(C_577,CL_578))
| ~ admin_file_has_level_h(admin,secretfile,secret,CL_578)
| ~ admin_compartment_has_scg(admin,C_577,scg_compartmentb)
| ~ admin_compartment_has_sso(admin,C_577,sso_compartmentb) ),
inference(demodulation,[status(thm),theory(equality)],[c_110,c_1397]) ).
tff(c_1724,plain,
! [C_632,CL_633] :
( ~ admin_file_has_compartments(admin,secretfile,cons(C_632,CL_633))
| ~ admin_file_has_level_h(admin,secretfile,secret,CL_633)
| ~ admin_compartment_has_scg(admin,C_632,scg_compartmentb)
| ~ admin_compartment_has_sso(admin,C_632,sso_compartmentb) ),
inference(splitLeft,[status(thm)],[c_1400]) ).
tff(c_1727,plain,
( ~ admin_file_has_level_h(admin,secretfile,secret,cons(compartmenta,nil))
| ~ admin_compartment_has_scg(admin,compartmentb,scg_compartmentb)
| ~ admin_compartment_has_sso(admin,compartmentb,sso_compartmentb) ),
inference(resolution,[status(thm)],[c_1717,c_1724]) ).
tff(c_1730,plain,
~ admin_file_has_level_h(admin,secretfile,secret,cons(compartmenta,nil)),
inference(demodulation,[status(thm),theory(equality)],[c_205,c_567,c_1727]) ).
tff(c_1741,plain,
( ~ admin_file_has_level_h(admin,secretfile,secret,nil)
| ~ admin_compartment_has_scg(admin,compartmenta,scg_compartmenta)
| ~ admin_compartment_has_sso(admin,compartmenta,sso_compartmenta) ),
inference(resolution,[status(thm)],[c_1391,c_1730]) ).
tff(c_1748,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_206,c_584,c_26,c_1741]) ).
tff(c_1749,plain,
admin_file_has_level(admin,secretfile,secret),
inference(splitRight,[status(thm)],[c_1400]) ).
tff(c_10,plain,
! [K_5,L_6] : loca_level_below(K_5,L_6,L_6),
inference(cnfTransformation,[status(thm)],[f_59]) ).
tff(c_154,plain,
system_indi_needs_level(system,alice,secret),
inference(cnfTransformation,[status(thm)],[f_345]) ).
tff(c_144,plain,
system_indi_has_citizenship(system,alice,usa),
inference(cnfTransformation,[status(thm)],[f_340]) ).
tff(c_189,plain,
! [K_146,U_147] :
( admin_indi_has_citizenship(admin,K_146,U_147)
| ~ system_indi_has_citizenship(system,K_146,U_147) ),
inference(cnfTransformation,[status(thm)],[f_169]) ).
tff(c_196,plain,
admin_indi_has_citizenship(admin,alice,usa),
inference(resolution,[status(thm)],[c_144,c_189]) ).
tff(c_134,plain,
system_indi_is_polygraph_admin(system,polygraph_admin),
inference(cnfTransformation,[status(thm)],[f_335]) ).
tff(c_146,plain,
polygraph_admin_indi_has_polygraph(polygraph_admin,alice),
inference(cnfTransformation,[status(thm)],[f_341]) ).
tff(c_220,plain,
! [K_156,PA_157] :
( admin_indi_has_polygraph(admin,K_156)
| ~ polygraph_admin_indi_has_polygraph(PA_157,K_156)
| ~ system_indi_is_polygraph_admin(system,PA_157) ),
inference(cnfTransformation,[status(thm)],[f_141]) ).
tff(c_222,plain,
( admin_indi_has_polygraph(admin,alice)
| ~ system_indi_is_polygraph_admin(system,polygraph_admin) ),
inference(resolution,[status(thm)],[c_146,c_220]) ).
tff(c_225,plain,
admin_indi_has_polygraph(admin,alice),
inference(demodulation,[status(thm),theory(equality)],[c_134,c_222]) ).
tff(c_140,plain,
system_indi_is_hr_admin(system,hr_admin),
inference(cnfTransformation,[status(thm)],[f_338]) ).
tff(c_152,plain,
hr_admin_indi_has_employment(hr_admin,alice),
inference(cnfTransformation,[status(thm)],[f_344]) ).
tff(c_208,plain,
! [K_152,HR_153] :
( admin_indi_has_employment(admin,K_152)
| ~ hr_admin_indi_has_employment(HR_153,K_152)
| ~ system_indi_is_hr_admin(system,HR_153) ),
inference(cnfTransformation,[status(thm)],[f_163]) ).
tff(c_210,plain,
( admin_indi_has_employment(admin,alice)
| ~ system_indi_is_hr_admin(system,hr_admin) ),
inference(resolution,[status(thm)],[c_152,c_208]) ).
tff(c_213,plain,
admin_indi_has_employment(admin,alice),
inference(demodulation,[status(thm),theory(equality)],[c_140,c_210]) ).
tff(c_136,plain,
system_indi_is_credit_admin(system,credit_admin),
inference(cnfTransformation,[status(thm)],[f_336]) ).
tff(c_148,plain,
credit_admin_indi_has_credit(credit_admin,alice),
inference(cnfTransformation,[status(thm)],[f_342]) ).
tff(c_214,plain,
! [K_154,CA_155] :
( admin_indi_has_credit(admin,K_154)
| ~ credit_admin_indi_has_credit(CA_155,K_154)
| ~ system_indi_is_credit_admin(system,CA_155) ),
inference(cnfTransformation,[status(thm)],[f_147]) ).
tff(c_216,plain,
( admin_indi_has_credit(admin,alice)
| ~ system_indi_is_credit_admin(system,credit_admin) ),
inference(resolution,[status(thm)],[c_148,c_214]) ).
tff(c_219,plain,
admin_indi_has_credit(admin,alice),
inference(demodulation,[status(thm),theory(equality)],[c_136,c_216]) ).
tff(c_142,plain,
system_indi_is_level_admin(system,level_admin),
inference(cnfTransformation,[status(thm)],[f_339]) ).
tff(c_138,plain,
system_indi_is_background_admin(system,background_admin),
inference(cnfTransformation,[status(thm)],[f_337]) ).
tff(c_150,plain,
background_admin_indi_has_background(background_admin,alice,topsecret),
inference(cnfTransformation,[status(thm)],[f_343]) ).
tff(c_8,plain,
! [K_4] : loca_level_direct_below(K_4,secret,topsecret),
inference(cnfTransformation,[status(thm)],[f_57]) ).
tff(c_267,plain,
! [K_178,L_179,L11_180,L1_181] :
( loca_level_below(K_178,L_179,L11_180)
| ~ loca_level_below(K_178,L_179,L1_181)
| ~ loca_level_direct_below(K_178,L1_181,L11_180) ),
inference(cnfTransformation,[status(thm)],[f_65]) ).
tff(c_271,plain,
! [K_182,L_183,L11_184] :
( loca_level_below(K_182,L_183,L11_184)
| ~ loca_level_direct_below(K_182,L_183,L11_184) ),
inference(resolution,[status(thm)],[c_10,c_267]) ).
tff(c_284,plain,
! [K_4] : loca_level_below(K_4,secret,topsecret),
inference(resolution,[status(thm)],[c_8,c_271]) ).
tff(c_371,plain,
! [K_224,L_225,L1_226,BA_227] :
( admin_indi_has_background(admin,K_224,L_225)
| ~ loca_level_below(admin,L_225,L1_226)
| ~ background_admin_indi_has_background(BA_227,K_224,L1_226)
| ~ system_indi_is_background_admin(system,BA_227) ),
inference(cnfTransformation,[status(thm)],[f_157]) ).
tff(c_462,plain,
! [K_257,BA_258] :
( admin_indi_has_background(admin,K_257,secret)
| ~ background_admin_indi_has_background(BA_258,K_257,topsecret)
| ~ system_indi_is_background_admin(system,BA_258) ),
inference(resolution,[status(thm)],[c_284,c_371]) ).
tff(c_465,plain,
( admin_indi_has_background(admin,alice,secret)
| ~ system_indi_is_background_admin(system,background_admin) ),
inference(resolution,[status(thm)],[c_150,c_462]) ).
tff(c_468,plain,
admin_indi_has_background(admin,alice,secret),
inference(demodulation,[status(thm),theory(equality)],[c_138,c_465]) ).
tff(c_156,plain,
level_admin_indi_has_level(level_admin,alice,topsecret),
inference(cnfTransformation,[status(thm)],[f_346]) ).
tff(c_1431,plain,
! [L_595,K_597,LA_594,L11_596,L1_593] :
( admin_indi_has_level(admin,K_597,L_595)
| ~ admin_indi_has_background(admin,K_597,L_595)
| ~ loca_level_below(admin,L_595,L11_596)
| ~ level_admin_indi_has_level(LA_594,K_597,L11_596)
| ~ system_indi_is_level_admin(system,LA_594)
| ~ loca_level_below(admin,L_595,L1_593)
| ~ admin_indi_has_credit(admin,K_597)
| ~ admin_indi_has_employment(admin,K_597)
| ~ admin_indi_has_polygraph(admin,K_597)
| ~ admin_indi_has_citizenship(admin,K_597,usa)
| ~ system_indi_needs_level(system,K_597,L1_593) ),
inference(cnfTransformation,[status(thm)],[f_193]) ).
tff(c_1806,plain,
! [K_650,LA_651,L1_652] :
( admin_indi_has_level(admin,K_650,secret)
| ~ admin_indi_has_background(admin,K_650,secret)
| ~ level_admin_indi_has_level(LA_651,K_650,topsecret)
| ~ system_indi_is_level_admin(system,LA_651)
| ~ loca_level_below(admin,secret,L1_652)
| ~ admin_indi_has_credit(admin,K_650)
| ~ admin_indi_has_employment(admin,K_650)
| ~ admin_indi_has_polygraph(admin,K_650)
| ~ admin_indi_has_citizenship(admin,K_650,usa)
| ~ system_indi_needs_level(system,K_650,L1_652) ),
inference(resolution,[status(thm)],[c_284,c_1431]) ).
tff(c_1808,plain,
! [L1_652] :
( 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,L1_652)
| ~ 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,L1_652) ),
inference(resolution,[status(thm)],[c_156,c_1806]) ).
tff(c_1811,plain,
! [L1_652] :
( admin_indi_has_level(admin,alice,secret)
| ~ loca_level_below(admin,secret,L1_652)
| ~ system_indi_needs_level(system,alice,L1_652) ),
inference(demodulation,[status(thm),theory(equality)],[c_196,c_225,c_213,c_219,c_142,c_468,c_1808]) ).
tff(c_1814,plain,
! [L1_656] :
( ~ loca_level_below(admin,secret,L1_656)
| ~ system_indi_needs_level(system,alice,L1_656) ),
inference(splitLeft,[status(thm)],[c_1811]) ).
tff(c_1817,plain,
~ loca_level_below(admin,secret,secret),
inference(resolution,[status(thm)],[c_154,c_1814]) ).
tff(c_1821,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_10,c_1817]) ).
tff(c_1822,plain,
admin_indi_has_level(admin,alice,secret),
inference(splitRight,[status(thm)],[c_1811]) ).
tff(c_72,plain,
! [K_114,F_115,L_116] :
( admin_indi_has_level_for_file(admin,K_114,F_115)
| ~ admin_indi_has_level(admin,K_114,L_116)
| ~ admin_file_has_level(admin,F_115,L_116) ),
inference(cnfTransformation,[status(thm)],[f_273]) ).
tff(c_1829,plain,
! [F_657] :
( admin_indi_has_level_for_file(admin,alice,F_657)
| ~ admin_file_has_level(admin,F_657,secret) ),
inference(resolution,[status(thm)],[c_1822,c_72]) ).
tff(c_54,plain,
! [K_68] : admin_indi_has_compartments(admin,K_68,nil),
inference(cnfTransformation,[status(thm)],[f_195]) ).
tff(c_160,plain,
system_indi_needs_compartment(system,alice,compartmenta),
inference(cnfTransformation,[status(thm)],[f_348]) ).
tff(c_88,plain,
oca_compartment_is_compartment(oca,compartmenta,sbu,unclassified,no,no),
inference(cnfTransformation,[status(thm)],[f_312]) ).
tff(c_334,plain,
! [C_203,OCA_202,L1_206,B1_201,K_204,L2_205] :
( admin_indi_has_polygraph_for_compartment(admin,K_204,C_203)
| ~ oca_compartment_is_compartment(OCA_202,C_203,L1_206,L2_205,B1_201,no)
| ~ system_indi_is_oca(system,OCA_202) ),
inference(cnfTransformation,[status(thm)],[f_247]) ).
tff(c_336,plain,
! [K_204] :
( admin_indi_has_polygraph_for_compartment(admin,K_204,compartmenta)
| ~ system_indi_is_oca(system,oca) ),
inference(resolution,[status(thm)],[c_88,c_334]) ).
tff(c_339,plain,
! [K_204] : admin_indi_has_polygraph_for_compartment(admin,K_204,compartmenta),
inference(demodulation,[status(thm),theory(equality)],[c_84,c_336]) ).
tff(c_355,plain,
! [OCA_214,K_217,L2_216,L1_218,B2_215,C_219] :
( admin_indi_has_credit_for_compartment(admin,K_217,C_219)
| ~ oca_compartment_is_compartment(OCA_214,C_219,L1_218,L2_216,no,B2_215)
| ~ system_indi_is_oca(system,OCA_214) ),
inference(cnfTransformation,[status(thm)],[f_261]) ).
tff(c_357,plain,
! [K_217] :
( admin_indi_has_credit_for_compartment(admin,K_217,compartmenta)
| ~ system_indi_is_oca(system,oca) ),
inference(resolution,[status(thm)],[c_88,c_355]) ).
tff(c_360,plain,
! [K_217] : admin_indi_has_credit_for_compartment(admin,K_217,compartmenta),
inference(demodulation,[status(thm),theory(equality)],[c_84,c_357]) ).
tff(c_40,plain,
! [K_52] : admin_indi_has_background(admin,K_52,unclassified),
inference(cnfTransformation,[status(thm)],[f_149]) ).
tff(c_512,plain,
! [K_286,B1_287,C_285,B2_290,L1_289,OCA_288,L2_284] :
( admin_indi_has_background_for_compartment(admin,K_286,C_285)
| ~ admin_indi_has_background(admin,K_286,L2_284)
| ~ oca_compartment_is_compartment(OCA_288,C_285,L1_289,L2_284,B1_287,B2_290)
| ~ system_indi_is_oca(system,OCA_288) ),
inference(cnfTransformation,[status(thm)],[f_225]) ).
tff(c_540,plain,
! [B2_299,B1_304,L1_302,K_303,OCA_301,C_300] :
( admin_indi_has_background_for_compartment(admin,K_303,C_300)
| ~ oca_compartment_is_compartment(OCA_301,C_300,L1_302,unclassified,B1_304,B2_299)
| ~ system_indi_is_oca(system,OCA_301) ),
inference(resolution,[status(thm)],[c_40,c_512]) ).
tff(c_542,plain,
! [K_303] :
( admin_indi_has_background_for_compartment(admin,K_303,compartmenta)
| ~ system_indi_is_oca(system,oca) ),
inference(resolution,[status(thm)],[c_88,c_540]) ).
tff(c_545,plain,
! [K_303] : admin_indi_has_background_for_compartment(admin,K_303,compartmenta),
inference(demodulation,[status(thm),theory(equality)],[c_84,c_542]) ).
tff(c_164,plain,
sso_indi_has_compartment(sso_compartmenta,alice,compartmenta),
inference(cnfTransformation,[status(thm)],[f_350]) ).
tff(c_981,plain,
! [K_414,C_415,CL_416,SSO_417] :
( admin_indi_has_compartments(admin,K_414,cons(C_415,CL_416))
| ~ admin_indi_has_compartments(admin,K_414,CL_416)
| ~ admin_indi_has_level_for_compartment(admin,K_414,C_415)
| ~ admin_indi_has_background_for_compartment(admin,K_414,C_415)
| ~ sso_indi_has_compartment(SSO_417,K_414,C_415)
| ~ admin_compartment_has_sso(admin,C_415,SSO_417)
| ~ admin_indi_has_credit_for_compartment(admin,K_414,C_415)
| ~ admin_indi_has_polygraph_for_compartment(admin,K_414,C_415)
| ~ admin_indi_has_citizenship(admin,K_414,usa)
| ~ admin_indi_has_employment(admin,K_414)
| ~ system_indi_needs_compartment(system,K_414,C_415) ),
inference(cnfTransformation,[status(thm)],[f_217]) ).
tff(c_983,plain,
! [CL_416] :
( admin_indi_has_compartments(admin,alice,cons(compartmenta,CL_416))
| ~ admin_indi_has_compartments(admin,alice,CL_416)
| ~ admin_indi_has_level_for_compartment(admin,alice,compartmenta)
| ~ admin_indi_has_background_for_compartment(admin,alice,compartmenta)
| ~ admin_compartment_has_sso(admin,compartmenta,sso_compartmenta)
| ~ admin_indi_has_credit_for_compartment(admin,alice,compartmenta)
| ~ admin_indi_has_polygraph_for_compartment(admin,alice,compartmenta)
| ~ admin_indi_has_citizenship(admin,alice,usa)
| ~ admin_indi_has_employment(admin,alice)
| ~ system_indi_needs_compartment(system,alice,compartmenta) ),
inference(resolution,[status(thm)],[c_164,c_981]) ).
tff(c_988,plain,
! [CL_416] :
( admin_indi_has_compartments(admin,alice,cons(compartmenta,CL_416))
| ~ admin_indi_has_compartments(admin,alice,CL_416)
| ~ admin_indi_has_level_for_compartment(admin,alice,compartmenta) ),
inference(demodulation,[status(thm),theory(equality)],[c_160,c_213,c_196,c_339,c_360,c_206,c_545,c_983]) ).
tff(c_992,plain,
~ admin_indi_has_level_for_compartment(admin,alice,compartmenta),
inference(splitLeft,[status(thm)],[c_988]) ).
tff(c_6,plain,
! [K_3] : loca_level_direct_below(K_3,confidential,secret),
inference(cnfTransformation,[status(thm)],[f_55]) ).
tff(c_4,plain,
! [K_2] : loca_level_direct_below(K_2,sbu,confidential),
inference(cnfTransformation,[status(thm)],[f_53]) ).
tff(c_300,plain,
! [K_190] : loca_level_below(K_190,sbu,confidential),
inference(resolution,[status(thm)],[c_4,c_271]) ).
tff(c_12,plain,
! [K_7,L_8,L11_10,L1_9] :
( loca_level_below(K_7,L_8,L11_10)
| ~ loca_level_below(K_7,L_8,L1_9)
| ~ loca_level_direct_below(K_7,L1_9,L11_10) ),
inference(cnfTransformation,[status(thm)],[f_65]) ).
tff(c_345,plain,
! [K_209,L11_210] :
( loca_level_below(K_209,sbu,L11_210)
| ~ loca_level_direct_below(K_209,confidential,L11_210) ),
inference(resolution,[status(thm)],[c_300,c_12]) ).
tff(c_349,plain,
! [K_3] : loca_level_below(K_3,sbu,secret),
inference(resolution,[status(thm)],[c_6,c_345]) ).
tff(c_350,plain,
! [K_211] : loca_level_below(K_211,sbu,secret),
inference(resolution,[status(thm)],[c_6,c_345]) ).
tff(c_362,plain,
! [K_221,L11_222] :
( loca_level_below(K_221,sbu,L11_222)
| ~ loca_level_direct_below(K_221,secret,L11_222) ),
inference(resolution,[status(thm)],[c_350,c_12]) ).
tff(c_366,plain,
! [K_4] : loca_level_below(K_4,sbu,topsecret),
inference(resolution,[status(thm)],[c_8,c_362]) ).
tff(c_489,plain,
! [K_273,BA_274] :
( admin_indi_has_background(admin,K_273,sbu)
| ~ background_admin_indi_has_background(BA_274,K_273,topsecret)
| ~ system_indi_is_background_admin(system,BA_274) ),
inference(resolution,[status(thm)],[c_366,c_371]) ).
tff(c_492,plain,
( admin_indi_has_background(admin,alice,sbu)
| ~ system_indi_is_background_admin(system,background_admin) ),
inference(resolution,[status(thm)],[c_150,c_489]) ).
tff(c_495,plain,
admin_indi_has_background(admin,alice,sbu),
inference(demodulation,[status(thm),theory(equality)],[c_138,c_492]) ).
tff(c_843,plain,
! [L_395,L1_393,LA_394,K_397,L11_396] :
( admin_indi_has_level(admin,K_397,L_395)
| ~ admin_indi_has_background(admin,K_397,L_395)
| ~ loca_level_below(admin,L_395,L11_396)
| ~ level_admin_indi_has_level(LA_394,K_397,L11_396)
| ~ system_indi_is_level_admin(system,LA_394)
| ~ loca_level_below(admin,L_395,L1_393)
| ~ admin_indi_has_credit(admin,K_397)
| ~ admin_indi_has_employment(admin,K_397)
| ~ admin_indi_has_polygraph(admin,K_397)
| ~ admin_indi_has_citizenship(admin,K_397,usa)
| ~ system_indi_needs_level(system,K_397,L1_393) ),
inference(cnfTransformation,[status(thm)],[f_193]) ).
tff(c_1183,plain,
! [K_494,LA_495,L1_496] :
( admin_indi_has_level(admin,K_494,sbu)
| ~ admin_indi_has_background(admin,K_494,sbu)
| ~ level_admin_indi_has_level(LA_495,K_494,topsecret)
| ~ system_indi_is_level_admin(system,LA_495)
| ~ loca_level_below(admin,sbu,L1_496)
| ~ admin_indi_has_credit(admin,K_494)
| ~ admin_indi_has_employment(admin,K_494)
| ~ admin_indi_has_polygraph(admin,K_494)
| ~ admin_indi_has_citizenship(admin,K_494,usa)
| ~ system_indi_needs_level(system,K_494,L1_496) ),
inference(resolution,[status(thm)],[c_366,c_843]) ).
tff(c_1185,plain,
! [L1_496] :
( 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,L1_496)
| ~ 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,L1_496) ),
inference(resolution,[status(thm)],[c_156,c_1183]) ).
tff(c_1188,plain,
! [L1_496] :
( admin_indi_has_level(admin,alice,sbu)
| ~ loca_level_below(admin,sbu,L1_496)
| ~ system_indi_needs_level(system,alice,L1_496) ),
inference(demodulation,[status(thm),theory(equality)],[c_196,c_225,c_213,c_219,c_142,c_495,c_1185]) ).
tff(c_1190,plain,
! [L1_497] :
( ~ loca_level_below(admin,sbu,L1_497)
| ~ system_indi_needs_level(system,alice,L1_497) ),
inference(splitLeft,[status(thm)],[c_1188]) ).
tff(c_1193,plain,
~ loca_level_below(admin,sbu,secret),
inference(resolution,[status(thm)],[c_154,c_1190]) ).
tff(c_1197,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_349,c_1193]) ).
tff(c_1198,plain,
admin_indi_has_level(admin,alice,sbu),
inference(splitRight,[status(thm)],[c_1188]) ).
tff(c_60,plain,
! [C_81,B1_85,L1_83,B2_86,K_80,L2_84,OCA_82] :
( admin_indi_has_level_for_compartment(admin,K_80,C_81)
| ~ admin_indi_has_level(admin,K_80,L1_83)
| ~ oca_compartment_is_compartment(OCA_82,C_81,L1_83,L2_84,B1_85,B2_86)
| ~ system_indi_is_oca(system,OCA_82) ),
inference(cnfTransformation,[status(thm)],[f_233]) ).
tff(c_1206,plain,
! [OCA_500,L2_502,B1_499,C_501,B2_503] :
( admin_indi_has_level_for_compartment(admin,alice,C_501)
| ~ oca_compartment_is_compartment(OCA_500,C_501,sbu,L2_502,B1_499,B2_503)
| ~ system_indi_is_oca(system,OCA_500) ),
inference(resolution,[status(thm)],[c_1198,c_60]) ).
tff(c_1209,plain,
( admin_indi_has_level_for_compartment(admin,alice,compartmenta)
| ~ system_indi_is_oca(system,oca) ),
inference(resolution,[status(thm)],[c_88,c_1206]) ).
tff(c_1212,plain,
admin_indi_has_level_for_compartment(admin,alice,compartmenta),
inference(demodulation,[status(thm),theory(equality)],[c_84,c_1209]) ).
tff(c_1214,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_992,c_1212]) ).
tff(c_1215,plain,
! [CL_416] :
( admin_indi_has_compartments(admin,alice,cons(compartmenta,CL_416))
| ~ admin_indi_has_compartments(admin,alice,CL_416) ),
inference(splitRight,[status(thm)],[c_988]) ).
tff(c_78,plain,
! [K_123,F_124] :
( admin_indi_has_citizenship_for_file(admin,K_123,F_124)
| ~ admin_indi_has_citizenship(admin,K_123,usa) ),
inference(cnfTransformation,[status(thm)],[f_289]) ).
tff(c_102,plain,
state_file_is_not_working_paper(secretfile),
inference(cnfTransformation,[status(thm)],[f_319]) ).
tff(c_122,plain,
state_file_has_owner(secretfile,owner_secretfile),
inference(cnfTransformation,[status(thm)],[f_329]) ).
tff(c_166,plain,
owner_indi_has_need_to_know(owner_secretfile,alice,secretfile),
inference(cnfTransformation,[status(thm)],[f_351]) ).
tff(c_226,plain,
! [K_158,F_159,OWR_160] :
( admin_indi_has_need_to_know_for_file(admin,K_158,F_159)
| ~ owner_indi_has_need_to_know(OWR_160,K_158,F_159)
| ~ state_file_has_owner(F_159,OWR_160) ),
inference(cnfTransformation,[status(thm)],[f_279]) ).
tff(c_232,plain,
( admin_indi_has_need_to_know_for_file(admin,alice,secretfile)
| ~ state_file_has_owner(secretfile,owner_secretfile) ),
inference(resolution,[status(thm)],[c_166,c_226]) ).
tff(c_241,plain,
admin_indi_has_need_to_know_for_file(admin,alice,secretfile),
inference(demodulation,[status(thm),theory(equality)],[c_122,c_232]) ).
tff(c_592,plain,
! [K_322,F_323] :
( admin_indi_may_file(admin,K_322,F_323,read)
| ~ admin_indi_has_compartments_for_file(admin,K_322,F_323)
| ~ admin_indi_has_level_for_file(admin,K_322,F_323)
| ~ admin_indi_has_need_to_know_for_file(admin,K_322,F_323)
| ~ admin_indi_has_citizenship_for_file(admin,K_322,F_323)
| ~ state_file_is_not_working_paper(F_323) ),
inference(cnfTransformation,[status(thm)],[f_301]) ).
tff(c_176,plain,
~ admin_indi_may_file(admin,alice,secretfile,read),
inference(cnfTransformation,[status(thm)],[f_357]) ).
tff(c_595,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)],[c_592,c_176]) ).
tff(c_598,plain,
( ~ admin_indi_has_compartments_for_file(admin,alice,secretfile)
| ~ admin_indi_has_level_for_file(admin,alice,secretfile)
| ~ admin_indi_has_citizenship_for_file(admin,alice,secretfile) ),
inference(demodulation,[status(thm),theory(equality)],[c_102,c_241,c_595]) ).
tff(c_599,plain,
~ admin_indi_has_citizenship_for_file(admin,alice,secretfile),
inference(splitLeft,[status(thm)],[c_598]) ).
tff(c_608,plain,
~ admin_indi_has_citizenship(admin,alice,usa),
inference(resolution,[status(thm)],[c_78,c_599]) ).
tff(c_614,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_196,c_608]) ).
tff(c_615,plain,
( ~ admin_indi_has_level_for_file(admin,alice,secretfile)
| ~ admin_indi_has_compartments_for_file(admin,alice,secretfile) ),
inference(splitRight,[status(thm)],[c_598]) ).
tff(c_617,plain,
~ admin_indi_has_compartments_for_file(admin,alice,secretfile),
inference(splitLeft,[status(thm)],[c_615]) ).
tff(c_573,plain,
! [C1_311,CL1_314] :
( admin_file_has_compartments_h(admin,secretfile,cons(compartmentb,cons(compartmenta,nil)),cons(C1_311,CL1_314))
| ~ admin_file_has_compartments_h(admin,secretfile,cons(compartmentb,cons(compartmenta,nil)),CL1_314)
| ~ admin_compartment_has_sso(admin,C1_311,sso_compartmenta) ),
inference(resolution,[status(thm)],[c_108,c_568]) ).
tff(c_973,plain,
! [C1_412,CL1_413] :
( admin_file_has_compartments_h(admin,secretfile,cons(compartmentb,cons(compartmenta,nil)),cons(C1_412,CL1_413))
| ~ admin_file_has_compartments_h(admin,secretfile,cons(compartmentb,cons(compartmenta,nil)),CL1_413)
| ~ admin_compartment_has_sso(admin,C1_412,sso_compartmentb) ),
inference(resolution,[status(thm)],[c_106,c_568]) ).
tff(c_977,plain,
( admin_file_has_compartments(admin,secretfile,cons(compartmentb,cons(compartmenta,nil)))
| ~ system_file_needs_compartments(system,secretfile,cons(compartmentb,cons(compartmenta,nil)))
| ~ admin_file_has_compartments_h(admin,secretfile,cons(compartmentb,cons(compartmenta,nil)),cons(compartmenta,nil))
| ~ admin_compartment_has_sso(admin,compartmentb,sso_compartmentb) ),
inference(resolution,[status(thm)],[c_973,c_18]) ).
tff(c_980,plain,
( admin_file_has_compartments(admin,secretfile,cons(compartmentb,cons(compartmenta,nil)))
| ~ admin_file_has_compartments_h(admin,secretfile,cons(compartmentb,cons(compartmenta,nil)),cons(compartmenta,nil)) ),
inference(demodulation,[status(thm),theory(equality)],[c_205,c_104,c_977]) ).
tff(c_1222,plain,
~ admin_file_has_compartments_h(admin,secretfile,cons(compartmentb,cons(compartmenta,nil)),cons(compartmenta,nil)),
inference(splitLeft,[status(thm)],[c_980]) ).
tff(c_1228,plain,
( ~ admin_file_has_compartments_h(admin,secretfile,cons(compartmentb,cons(compartmenta,nil)),nil)
| ~ admin_compartment_has_sso(admin,compartmenta,sso_compartmenta) ),
inference(resolution,[status(thm)],[c_573,c_1222]) ).
tff(c_1235,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_206,c_20,c_1228]) ).
tff(c_1236,plain,
admin_file_has_compartments(admin,secretfile,cons(compartmentb,cons(compartmenta,nil))),
inference(splitRight,[status(thm)],[c_980]) ).
tff(c_86,plain,
oca_compartment_is_compartment(oca,compartmentb,confidential,topsecret,yes,yes),
inference(cnfTransformation,[status(thm)],[f_311]) ).
tff(c_481,plain,
! [OCA_269,B2_264,L1_268,L2_267,K_266,C_265] :
( admin_indi_has_credit_for_compartment(admin,K_266,C_265)
| ~ admin_indi_has_credit(admin,K_266)
| ~ oca_compartment_is_compartment(OCA_269,C_265,L1_268,L2_267,yes,B2_264)
| ~ system_indi_is_oca(system,OCA_269) ),
inference(cnfTransformation,[status(thm)],[f_255]) ).
tff(c_483,plain,
! [K_266] :
( admin_indi_has_credit_for_compartment(admin,K_266,compartmentb)
| ~ admin_indi_has_credit(admin,K_266)
| ~ system_indi_is_oca(system,oca) ),
inference(resolution,[status(thm)],[c_86,c_481]) ).
tff(c_486,plain,
! [K_266] :
( admin_indi_has_credit_for_compartment(admin,K_266,compartmentb)
| ~ admin_indi_has_credit(admin,K_266) ),
inference(demodulation,[status(thm),theory(equality)],[c_84,c_483]) ).
tff(c_439,plain,
! [L1_241,B1_236,K_238,L2_237,OCA_239,C_240] :
( admin_indi_has_polygraph_for_compartment(admin,K_238,C_240)
| ~ admin_indi_has_polygraph(admin,K_238)
| ~ oca_compartment_is_compartment(OCA_239,C_240,L1_241,L2_237,B1_236,yes)
| ~ system_indi_is_oca(system,OCA_239) ),
inference(cnfTransformation,[status(thm)],[f_241]) ).
tff(c_441,plain,
! [K_238] :
( admin_indi_has_polygraph_for_compartment(admin,K_238,compartmentb)
| ~ admin_indi_has_polygraph(admin,K_238)
| ~ system_indi_is_oca(system,oca) ),
inference(resolution,[status(thm)],[c_86,c_439]) ).
tff(c_444,plain,
! [K_238] :
( admin_indi_has_polygraph_for_compartment(admin,K_238,compartmentb)
| ~ admin_indi_has_polygraph(admin,K_238) ),
inference(demodulation,[status(thm),theory(equality)],[c_84,c_441]) ).
tff(c_158,plain,
system_indi_needs_compartment(system,alice,compartmentb),
inference(cnfTransformation,[status(thm)],[f_347]) ).
tff(c_453,plain,
! [K_250,L_251,BA_252] :
( admin_indi_has_background(admin,K_250,L_251)
| ~ background_admin_indi_has_background(BA_252,K_250,L_251)
| ~ system_indi_is_background_admin(system,BA_252) ),
inference(resolution,[status(thm)],[c_10,c_371]) ).
tff(c_456,plain,
( admin_indi_has_background(admin,alice,topsecret)
| ~ system_indi_is_background_admin(system,background_admin) ),
inference(resolution,[status(thm)],[c_150,c_453]) ).
tff(c_459,plain,
admin_indi_has_background(admin,alice,topsecret),
inference(demodulation,[status(thm),theory(equality)],[c_138,c_456]) ).
tff(c_585,plain,
! [B1_321,OCA_319,L1_320,C_318,B2_317] :
( admin_indi_has_background_for_compartment(admin,alice,C_318)
| ~ oca_compartment_is_compartment(OCA_319,C_318,L1_320,topsecret,B1_321,B2_317)
| ~ system_indi_is_oca(system,OCA_319) ),
inference(resolution,[status(thm)],[c_459,c_512]) ).
tff(c_588,plain,
( admin_indi_has_background_for_compartment(admin,alice,compartmentb)
| ~ system_indi_is_oca(system,oca) ),
inference(resolution,[status(thm)],[c_86,c_585]) ).
tff(c_591,plain,
admin_indi_has_background_for_compartment(admin,alice,compartmentb),
inference(demodulation,[status(thm),theory(equality)],[c_84,c_588]) ).
tff(c_162,plain,
sso_indi_has_compartment(sso_compartmentb,alice,compartmentb),
inference(cnfTransformation,[status(thm)],[f_349]) ).
tff(c_985,plain,
! [CL_416] :
( admin_indi_has_compartments(admin,alice,cons(compartmentb,CL_416))
| ~ admin_indi_has_compartments(admin,alice,CL_416)
| ~ admin_indi_has_level_for_compartment(admin,alice,compartmentb)
| ~ admin_indi_has_background_for_compartment(admin,alice,compartmentb)
| ~ 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)
| ~ admin_indi_has_citizenship(admin,alice,usa)
| ~ admin_indi_has_employment(admin,alice)
| ~ system_indi_needs_compartment(system,alice,compartmentb) ),
inference(resolution,[status(thm)],[c_162,c_981]) ).
tff(c_991,plain,
! [CL_416] :
( admin_indi_has_compartments(admin,alice,cons(compartmentb,CL_416))
| ~ admin_indi_has_compartments(admin,alice,CL_416)
| ~ admin_indi_has_level_for_compartment(admin,alice,compartmentb)
| ~ admin_indi_has_credit_for_compartment(admin,alice,compartmentb)
| ~ admin_indi_has_polygraph_for_compartment(admin,alice,compartmentb) ),
inference(demodulation,[status(thm),theory(equality)],[c_158,c_213,c_196,c_205,c_591,c_985]) ).
tff(c_1242,plain,
~ admin_indi_has_polygraph_for_compartment(admin,alice,compartmentb),
inference(splitLeft,[status(thm)],[c_991]) ).
tff(c_1251,plain,
~ admin_indi_has_polygraph(admin,alice),
inference(resolution,[status(thm)],[c_444,c_1242]) ).
tff(c_1255,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_225,c_1251]) ).
tff(c_1256,plain,
! [CL_416] :
( ~ admin_indi_has_credit_for_compartment(admin,alice,compartmentb)
| ~ admin_indi_has_level_for_compartment(admin,alice,compartmentb)
| admin_indi_has_compartments(admin,alice,cons(compartmentb,CL_416))
| ~ admin_indi_has_compartments(admin,alice,CL_416) ),
inference(splitRight,[status(thm)],[c_991]) ).
tff(c_1258,plain,
~ admin_indi_has_level_for_compartment(admin,alice,compartmentb),
inference(splitLeft,[status(thm)],[c_1256]) ).
tff(c_285,plain,
! [K_3] : loca_level_below(K_3,confidential,secret),
inference(resolution,[status(thm)],[c_6,c_271]) ).
tff(c_292,plain,
! [K_186] : loca_level_below(K_186,confidential,secret),
inference(resolution,[status(thm)],[c_6,c_271]) ).
tff(c_329,plain,
! [K_199,L11_200] :
( loca_level_below(K_199,confidential,L11_200)
| ~ loca_level_direct_below(K_199,secret,L11_200) ),
inference(resolution,[status(thm)],[c_292,c_12]) ).
tff(c_333,plain,
! [K_4] : loca_level_below(K_4,confidential,topsecret),
inference(resolution,[status(thm)],[c_8,c_329]) ).
tff(c_474,plain,
! [K_262,BA_263] :
( admin_indi_has_background(admin,K_262,confidential)
| ~ background_admin_indi_has_background(BA_263,K_262,topsecret)
| ~ system_indi_is_background_admin(system,BA_263) ),
inference(resolution,[status(thm)],[c_333,c_371]) ).
tff(c_477,plain,
( admin_indi_has_background(admin,alice,confidential)
| ~ system_indi_is_background_admin(system,background_admin) ),
inference(resolution,[status(thm)],[c_150,c_474]) ).
tff(c_480,plain,
admin_indi_has_background(admin,alice,confidential),
inference(demodulation,[status(thm),theory(equality)],[c_138,c_477]) ).
tff(c_1298,plain,
! [K_535,LA_536,L1_537] :
( admin_indi_has_level(admin,K_535,confidential)
| ~ admin_indi_has_background(admin,K_535,confidential)
| ~ level_admin_indi_has_level(LA_536,K_535,topsecret)
| ~ system_indi_is_level_admin(system,LA_536)
| ~ loca_level_below(admin,confidential,L1_537)
| ~ admin_indi_has_credit(admin,K_535)
| ~ admin_indi_has_employment(admin,K_535)
| ~ admin_indi_has_polygraph(admin,K_535)
| ~ admin_indi_has_citizenship(admin,K_535,usa)
| ~ system_indi_needs_level(system,K_535,L1_537) ),
inference(resolution,[status(thm)],[c_333,c_843]) ).
tff(c_1300,plain,
! [L1_537] :
( 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,L1_537)
| ~ 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,L1_537) ),
inference(resolution,[status(thm)],[c_156,c_1298]) ).
tff(c_1303,plain,
! [L1_537] :
( admin_indi_has_level(admin,alice,confidential)
| ~ loca_level_below(admin,confidential,L1_537)
| ~ system_indi_needs_level(system,alice,L1_537) ),
inference(demodulation,[status(thm),theory(equality)],[c_196,c_225,c_213,c_219,c_142,c_480,c_1300]) ).
tff(c_1305,plain,
! [L1_538] :
( ~ loca_level_below(admin,confidential,L1_538)
| ~ system_indi_needs_level(system,alice,L1_538) ),
inference(splitLeft,[status(thm)],[c_1303]) ).
tff(c_1308,plain,
~ loca_level_below(admin,confidential,secret),
inference(resolution,[status(thm)],[c_154,c_1305]) ).
tff(c_1312,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_285,c_1308]) ).
tff(c_1313,plain,
admin_indi_has_level(admin,alice,confidential),
inference(splitRight,[status(thm)],[c_1303]) ).
tff(c_1321,plain,
! [B2_544,C_542,OCA_541,L2_543,B1_540] :
( admin_indi_has_level_for_compartment(admin,alice,C_542)
| ~ oca_compartment_is_compartment(OCA_541,C_542,confidential,L2_543,B1_540,B2_544)
| ~ system_indi_is_oca(system,OCA_541) ),
inference(resolution,[status(thm)],[c_1313,c_60]) ).
tff(c_1324,plain,
( admin_indi_has_level_for_compartment(admin,alice,compartmentb)
| ~ system_indi_is_oca(system,oca) ),
inference(resolution,[status(thm)],[c_86,c_1321]) ).
tff(c_1327,plain,
admin_indi_has_level_for_compartment(admin,alice,compartmentb),
inference(demodulation,[status(thm),theory(equality)],[c_84,c_1324]) ).
tff(c_1329,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_1258,c_1327]) ).
tff(c_1330,plain,
! [CL_416] :
( ~ admin_indi_has_credit_for_compartment(admin,alice,compartmentb)
| admin_indi_has_compartments(admin,alice,cons(compartmentb,CL_416))
| ~ admin_indi_has_compartments(admin,alice,CL_416) ),
inference(splitRight,[status(thm)],[c_1256]) ).
tff(c_1344,plain,
~ admin_indi_has_credit_for_compartment(admin,alice,compartmentb),
inference(splitLeft,[status(thm)],[c_1330]) ).
tff(c_1353,plain,
~ admin_indi_has_credit(admin,alice),
inference(resolution,[status(thm)],[c_486,c_1344]) ).
tff(c_1357,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_219,c_1353]) ).
tff(c_1360,plain,
! [CL_553] :
( admin_indi_has_compartments(admin,alice,cons(compartmentb,CL_553))
| ~ admin_indi_has_compartments(admin,alice,CL_553) ),
inference(splitRight,[status(thm)],[c_1330]) ).
tff(c_70,plain,
! [K_111,F_112,CL_113] :
( admin_indi_has_compartments_for_file(admin,K_111,F_112)
| ~ admin_indi_has_compartments(admin,K_111,CL_113)
| ~ admin_file_has_compartments(admin,F_112,CL_113) ),
inference(cnfTransformation,[status(thm)],[f_267]) ).
tff(c_1364,plain,
! [F_554,CL_555] :
( admin_indi_has_compartments_for_file(admin,alice,F_554)
| ~ admin_file_has_compartments(admin,F_554,cons(compartmentb,CL_555))
| ~ admin_indi_has_compartments(admin,alice,CL_555) ),
inference(resolution,[status(thm)],[c_1360,c_70]) ).
tff(c_1367,plain,
( admin_indi_has_compartments_for_file(admin,alice,secretfile)
| ~ admin_indi_has_compartments(admin,alice,cons(compartmenta,nil)) ),
inference(resolution,[status(thm)],[c_1236,c_1364]) ).
tff(c_1370,plain,
~ admin_indi_has_compartments(admin,alice,cons(compartmenta,nil)),
inference(negUnitSimplification,[status(thm)],[c_617,c_1367]) ).
tff(c_1373,plain,
~ admin_indi_has_compartments(admin,alice,nil),
inference(resolution,[status(thm)],[c_1215,c_1370]) ).
tff(c_1377,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_54,c_1373]) ).
tff(c_1378,plain,
~ admin_indi_has_level_for_file(admin,alice,secretfile),
inference(splitRight,[status(thm)],[c_615]) ).
tff(c_1832,plain,
~ admin_file_has_level(admin,secretfile,secret),
inference(resolution,[status(thm)],[c_1829,c_1378]) ).
tff(c_1836,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_1749,c_1832]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.08 % Problem : SWV437+1 : TPTP v9.0.0. Released v4.0.0.
% 0.00/0.09 % Command : java -Dfile.encoding=UTF-8 -Xms512M -Xmx4G -Xss10M -jar /export/starexec/sandbox/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox/solver/bin/cvc4-1.4-x86_64-linux-opt -liasolver cooper -t %d %s
% 0.08/0.28 % Computer : n032.cluster.edu
% 0.08/0.28 % Model : x86_64 x86_64
% 0.08/0.28 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.28 % Memory : 8042.1875MB
% 0.08/0.28 % OS : Linux 3.10.0-693.el7.x86_64
% 0.08/0.28 % CPULimit : 300
% 0.08/0.28 % WCLimit : 300
% 0.08/0.28 % DateTime : Wed Apr 9 03:26:45 EDT 2025
% 0.08/0.28 % CPUTime :
% 7.40/2.55 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p
% 7.40/2.58
% 7.40/2.58 % SZS output start CNFRefutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------