%------------------------------------------------------------------------------
% File : Zipperpin---2.1.9999
% Problem : SWV437+1 : TPTP v9.2.0. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : python3 /export/starexec/sandbox/solver/bin/portfolio.lams.parallel.py %s %d /export/starexec/sandbox/tmp/tmp.Y8e3rdMWL0 true
% Computer : n010.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 : Thu Oct 2 05:01:10 PM UTC 2025
% Result : Theorem 1.27s 0.92s
% Output : Refutation 1.27s
% Verified :
% SZS Type : Refutation
% Derivation depth : 19
% Number of leaves : 68
% Syntax : Number of formulae : 305 ( 166 unt; 0 typ; 0 def)
% Number of atoms : 667 ( 0 equ; 0 cnn)
% Maximal formula atoms : 11 ( 2 avg)
% Number of connectives : 2861 ( 291 ~; 285 |; 0 &;2208 @)
% ( 0 <=>; 77 =>; 0 <=; 0 <~>)
% Maximal formula depth : 20 ( 7 avg)
% Number of types : 2 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of symbols : 79 ( 78 usr; 28 con; 0-6 aty)
% Number of variables : 441 ( 0 ^; 441 !; 0 ?; 441 :)
% Comments :
%------------------------------------------------------------------------------
thf(credit_admin_indi_has_credit_type,type,
credit_admin_indi_has_credit: $i > $i > $o ).
thf(sso_compartmenta_type,type,
sso_compartmenta: $i ).
thf(admin_indi_has_citizenship_type,type,
admin_indi_has_citizenship: $i > $i > $i > $o ).
thf(admin_compartment_has_sso_type,type,
admin_compartment_has_sso: $i > $i > $i > $o ).
thf(scg_compartmenta_type,type,
scg_compartmenta: $i ).
thf(system_compartment_has_sso_type,type,
system_compartment_has_sso: $i > $i > $i > $o ).
thf(state_file_is_not_working_paper_type,type,
state_file_is_not_working_paper: $i > $o ).
thf(level_admin_type,type,
level_admin: $i ).
thf(read_type,type,
read: $i ).
thf(cons_type,type,
cons: $i > $i > $i ).
thf(polygraph_admin_type,type,
polygraph_admin: $i ).
thf(admin_indi_may_file_type,type,
admin_indi_may_file: $i > $i > $i > $i > $o ).
thf(unclassified_type,type,
unclassified: $i ).
thf(oca_compartment_is_compartment_type,type,
oca_compartment_is_compartment: $i > $i > $i > $i > $i > $i > $o ).
thf(admin_indi_has_credit_type,type,
admin_indi_has_credit: $i > $i > $o ).
thf(admin_indi_has_citizenship_for_file_type,type,
admin_indi_has_citizenship_for_file: $i > $i > $i > $o ).
thf(no_type,type,
no: $i ).
thf(admin_indi_has_compartments_type,type,
admin_indi_has_compartments: $i > $i > $i > $o ).
thf(sso_compartment_has_scg_type,type,
sso_compartment_has_scg: $i > $i > $i > $o ).
thf(sso_file_has_level_type,type,
sso_file_has_level: $i > $i > $i > $i > $o ).
thf(sso_compartmentb_type,type,
sso_compartmentb: $i ).
thf(owner_secretfile_type,type,
owner_secretfile: $i ).
thf(secret_type,type,
secret: $i ).
thf(admin_file_has_compartments_h_type,type,
admin_file_has_compartments_h: $i > $i > $i > $i > $o ).
thf(compartmenta_type,type,
compartmenta: $i ).
thf(system_file_needs_compartments_type,type,
system_file_needs_compartments: $i > $i > $i > $o ).
thf(admin_indi_has_level_type,type,
admin_indi_has_level: $i > $i > $i > $o ).
thf(hr_admin_indi_has_employment_type,type,
hr_admin_indi_has_employment: $i > $i > $o ).
thf(loca_level_direct_below_type,type,
loca_level_direct_below: $i > $i > $i > $o ).
thf(background_admin_type,type,
background_admin: $i ).
thf(admin_type,type,
admin: $i ).
thf(system_indi_needs_compartment_type,type,
system_indi_needs_compartment: $i > $i > $i > $o ).
thf(admin_indi_has_polygraph_type,type,
admin_indi_has_polygraph: $i > $i > $o ).
thf(alice_type,type,
alice: $i ).
thf(hr_admin_type,type,
hr_admin: $i ).
thf(secretfile_type,type,
secretfile: $i ).
thf(system_file_needs_level_type,type,
system_file_needs_level: $i > $i > $i > $o ).
thf(admin_file_has_level_h_type,type,
admin_file_has_level_h: $i > $i > $i > $i > $o ).
thf(nil_type,type,
nil: $i ).
thf(owner_indi_has_need_to_know_type,type,
owner_indi_has_need_to_know: $i > $i > $i > $o ).
thf(system_type,type,
system: $i ).
thf(system_indi_is_level_admin_type,type,
system_indi_is_level_admin: $i > $i > $o ).
thf(polygraph_admin_indi_has_polygraph_type,type,
polygraph_admin_indi_has_polygraph: $i > $i > $o ).
thf(level_admin_indi_has_level_type,type,
level_admin_indi_has_level: $i > $i > $i > $o ).
thf(system_indi_has_citizenship_type,type,
system_indi_has_citizenship: $i > $i > $i > $o ).
thf(compartmentb_type,type,
compartmentb: $i ).
thf(topsecret_type,type,
topsecret: $i ).
thf(system_indi_is_oca_type,type,
system_indi_is_oca: $i > $i > $o ).
thf(sbu_type,type,
sbu: $i ).
thf(oca_type,type,
oca: $i ).
thf(admin_file_has_level_type,type,
admin_file_has_level: $i > $i > $i > $o ).
thf(admin_compartment_has_scg_type,type,
admin_compartment_has_scg: $i > $i > $i > $o ).
thf(admin_indi_has_polygraph_for_compartment_type,type,
admin_indi_has_polygraph_for_compartment: $i > $i > $i > $o ).
thf(yes_type,type,
yes: $i ).
thf(admin_indi_has_credit_for_compartment_type,type,
admin_indi_has_credit_for_compartment: $i > $i > $i > $o ).
thf(admin_indi_has_background_type,type,
admin_indi_has_background: $i > $i > $i > $o ).
thf(admin_indi_has_level_for_file_type,type,
admin_indi_has_level_for_file: $i > $i > $i > $o ).
thf(usa_type,type,
usa: $i ).
thf(system_indi_is_hr_admin_type,type,
system_indi_is_hr_admin: $i > $i > $o ).
thf(scg_compartmentb_type,type,
scg_compartmentb: $i ).
thf(admin_indi_has_need_to_know_for_file_type,type,
admin_indi_has_need_to_know_for_file: $i > $i > $i > $o ).
thf(admin_indi_has_compartments_for_file_type,type,
admin_indi_has_compartments_for_file: $i > $i > $i > $o ).
thf(oca_compartment_has_scg_type,type,
oca_compartment_has_scg: $i > $i > $i > $o ).
thf(sso_file_has_compartments_type,type,
sso_file_has_compartments: $i > $i > $i > $o ).
thf(sso_indi_has_compartment_type,type,
sso_indi_has_compartment: $i > $i > $i > $o ).
thf(system_indi_is_polygraph_admin_type,type,
system_indi_is_polygraph_admin: $i > $i > $o ).
thf(confidential_type,type,
confidential: $i ).
thf(loca_level_below_type,type,
loca_level_below: $i > $i > $i > $o ).
thf(admin_file_has_compartments_type,type,
admin_file_has_compartments: $i > $i > $i > $o ).
thf(credit_admin_type,type,
credit_admin: $i ).
thf(system_indi_is_credit_admin_type,type,
system_indi_is_credit_admin: $i > $i > $o ).
thf(admin_indi_has_employment_type,type,
admin_indi_has_employment: $i > $i > $o ).
thf(background_admin_indi_has_background_type,type,
background_admin_indi_has_background: $i > $i > $i > $o ).
thf(admin_indi_has_level_for_compartment_type,type,
admin_indi_has_level_for_compartment: $i > $i > $i > $o ).
thf(system_indi_needs_level_type,type,
system_indi_needs_level: $i > $i > $i > $o ).
thf(system_indi_is_background_admin_type,type,
system_indi_is_background_admin: $i > $i > $o ).
thf(state_file_has_owner_type,type,
state_file_has_owner: $i > $i > $o ).
thf(admin_indi_has_background_for_compartment_type,type,
admin_indi_has_background_for_compartment: $i > $i > $i > $o ).
thf(ax80,axiom,
sso_indi_has_compartment @ sso_compartmentb @ alice @ compartmentb ).
thf(zip_derived_cl80,plain,
sso_indi_has_compartment @ sso_compartmentb @ alice @ compartmentb,
inference(cnf,[status(esa)],[ax80]) ).
thf(ax51,axiom,
system_file_needs_compartments @ system @ secretfile @ ( cons @ compartmentb @ ( cons @ compartmenta @ nil ) ) ).
thf(zip_derived_cl51,plain,
system_file_needs_compartments @ system @ secretfile @ ( cons @ compartmentb @ ( cons @ compartmenta @ nil ) ),
inference(cnf,[status(esa)],[ax51]) ).
thf(ax8,axiom,
! [F: $i,CL: $i] :
( ( system_file_needs_compartments @ system @ F @ CL )
=> ( ( admin_file_has_compartments_h @ admin @ F @ CL @ CL )
=> ( admin_file_has_compartments @ admin @ F @ CL ) ) ) ).
thf(zip_derived_cl8,plain,
! [X0: $i,X1: $i] :
( ~ ( admin_file_has_compartments_h @ admin @ X0 @ X1 @ X1 )
| ( admin_file_has_compartments @ admin @ X0 @ X1 )
| ~ ( system_file_needs_compartments @ system @ X0 @ X1 ) ),
inference(cnf,[status(esa)],[ax8]) ).
thf(zip_derived_cl120,plain,
( ~ ( admin_file_has_compartments_h @ admin @ secretfile @ ( cons @ compartmentb @ ( cons @ compartmenta @ nil ) ) @ ( cons @ compartmentb @ ( cons @ compartmenta @ nil ) ) )
| ( admin_file_has_compartments @ admin @ secretfile @ ( cons @ compartmentb @ ( cons @ compartmenta @ nil ) ) ) ),
inference('s_sup-',[status(thm)],[zip_derived_cl51,zip_derived_cl8]) ).
thf(ax44,axiom,
system_compartment_has_sso @ system @ compartmentb @ sso_compartmentb ).
thf(zip_derived_cl44,plain,
system_compartment_has_sso @ system @ compartmentb @ sso_compartmentb,
inference(cnf,[status(esa)],[ax44]) ).
thf(ax6,axiom,
! [C: $i,SSO: $i] :
( ( system_compartment_has_sso @ system @ C @ SSO )
=> ( admin_compartment_has_sso @ admin @ C @ SSO ) ) ).
thf(zip_derived_cl6,plain,
! [X0: $i,X1: $i] :
( ( admin_compartment_has_sso @ admin @ X0 @ X1 )
| ~ ( system_compartment_has_sso @ system @ X0 @ X1 ) ),
inference(cnf,[status(esa)],[ax6]) ).
thf(zip_derived_cl92,plain,
admin_compartment_has_sso @ admin @ compartmentb @ sso_compartmentb,
inference('s_sup-',[status(thm)],[zip_derived_cl44,zip_derived_cl6]) ).
thf(ax10,axiom,
! [F: $i,CL: $i,C1: $i,CL1: $i,SSO: $i] :
( ( 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 ) ) ) ) ) ).
thf(zip_derived_cl10,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( ( admin_file_has_compartments_h @ admin @ X0 @ X1 @ ( cons @ X2 @ X3 ) )
| ~ ( admin_file_has_compartments_h @ admin @ X0 @ X1 @ X3 )
| ~ ( admin_compartment_has_sso @ admin @ X2 @ X4 )
| ~ ( sso_file_has_compartments @ X4 @ X0 @ X1 ) ),
inference(cnf,[status(esa)],[ax10]) ).
thf(zip_derived_cl104,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( admin_file_has_compartments_h @ admin @ X2 @ X1 @ ( cons @ compartmentb @ X0 ) )
| ~ ( admin_file_has_compartments_h @ admin @ X2 @ X1 @ X0 )
| ~ ( sso_file_has_compartments @ sso_compartmentb @ X2 @ X1 ) ),
inference('s_sup-',[status(thm)],[zip_derived_cl92,zip_derived_cl10]) ).
thf(zip_derived_cl194,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 ) )
| ~ ( sso_file_has_compartments @ sso_compartmentb @ secretfile @ ( cons @ compartmentb @ ( cons @ compartmenta @ nil ) ) ) ),
inference('s_sup+',[status(thm)],[zip_derived_cl120,zip_derived_cl104]) ).
thf(ax52,axiom,
sso_file_has_compartments @ sso_compartmentb @ secretfile @ ( cons @ compartmentb @ ( cons @ compartmenta @ nil ) ) ).
thf(zip_derived_cl52,plain,
sso_file_has_compartments @ sso_compartmentb @ secretfile @ ( cons @ compartmentb @ ( cons @ compartmenta @ nil ) ),
inference(cnf,[status(esa)],[ax52]) ).
thf(zip_derived_cl195,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(demod,[status(thm)],[zip_derived_cl194,zip_derived_cl52]) ).
thf(ax47,axiom,
system_compartment_has_sso @ system @ compartmenta @ sso_compartmenta ).
thf(zip_derived_cl47,plain,
system_compartment_has_sso @ system @ compartmenta @ sso_compartmenta,
inference(cnf,[status(esa)],[ax47]) ).
thf(zip_derived_cl6_001,plain,
! [X0: $i,X1: $i] :
( ( admin_compartment_has_sso @ admin @ X0 @ X1 )
| ~ ( system_compartment_has_sso @ system @ X0 @ X1 ) ),
inference(cnf,[status(esa)],[ax6]) ).
thf(zip_derived_cl93,plain,
admin_compartment_has_sso @ admin @ compartmenta @ sso_compartmenta,
inference('s_sup-',[status(thm)],[zip_derived_cl47,zip_derived_cl6]) ).
thf(zip_derived_cl10_002,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( ( admin_file_has_compartments_h @ admin @ X0 @ X1 @ ( cons @ X2 @ X3 ) )
| ~ ( admin_file_has_compartments_h @ admin @ X0 @ X1 @ X3 )
| ~ ( admin_compartment_has_sso @ admin @ X2 @ X4 )
| ~ ( sso_file_has_compartments @ X4 @ X0 @ X1 ) ),
inference(cnf,[status(esa)],[ax10]) ).
thf(zip_derived_cl105,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( admin_file_has_compartments_h @ admin @ X2 @ X1 @ ( cons @ compartmenta @ X0 ) )
| ~ ( admin_file_has_compartments_h @ admin @ X2 @ X1 @ X0 )
| ~ ( sso_file_has_compartments @ sso_compartmenta @ X2 @ X1 ) ),
inference('s_sup-',[status(thm)],[zip_derived_cl93,zip_derived_cl10]) ).
thf(zip_derived_cl212,plain,
( ( admin_file_has_compartments @ admin @ secretfile @ ( cons @ compartmentb @ ( cons @ compartmenta @ nil ) ) )
| ~ ( 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 ) ) ) ),
inference('s_sup+',[status(thm)],[zip_derived_cl195,zip_derived_cl105]) ).
thf(ax9,axiom,
! [F: $i,CL: $i] : ( admin_file_has_compartments_h @ admin @ F @ CL @ nil ) ).
thf(zip_derived_cl9,plain,
! [X0: $i,X1: $i] : ( admin_file_has_compartments_h @ admin @ X0 @ X1 @ nil ),
inference(cnf,[status(esa)],[ax9]) ).
thf(ax53,axiom,
sso_file_has_compartments @ sso_compartmenta @ secretfile @ ( cons @ compartmentb @ ( cons @ compartmenta @ nil ) ) ).
thf(zip_derived_cl53,plain,
sso_file_has_compartments @ sso_compartmenta @ secretfile @ ( cons @ compartmentb @ ( cons @ compartmenta @ nil ) ),
inference(cnf,[status(esa)],[ax53]) ).
thf(zip_derived_cl214,plain,
admin_file_has_compartments @ admin @ secretfile @ ( cons @ compartmentb @ ( cons @ compartmenta @ nil ) ),
inference(demod,[status(thm)],[zip_derived_cl212,zip_derived_cl9,zip_derived_cl53]) ).
thf(ax34,axiom,
! [K: $i,F: $i,CL: $i] :
( ( admin_file_has_compartments @ admin @ F @ CL )
=> ( ( admin_indi_has_compartments @ admin @ K @ CL )
=> ( admin_indi_has_compartments_for_file @ admin @ K @ F ) ) ) ).
thf(zip_derived_cl34,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( admin_indi_has_compartments_for_file @ admin @ X0 @ X1 )
| ~ ( admin_file_has_compartments @ admin @ X1 @ X2 )
| ~ ( admin_indi_has_compartments @ admin @ X0 @ X2 ) ),
inference(cnf,[status(esa)],[ax34]) ).
thf(zip_derived_cl215,plain,
! [X0: $i] :
( ( admin_indi_has_compartments_for_file @ admin @ X0 @ secretfile )
| ~ ( admin_indi_has_compartments @ admin @ X0 @ ( cons @ compartmentb @ ( cons @ compartmenta @ nil ) ) ) ),
inference('s_sup-',[status(thm)],[zip_derived_cl214,zip_derived_cl34]) ).
thf(ax75,axiom,
hr_admin_indi_has_employment @ hr_admin @ alice ).
thf(zip_derived_cl75,plain,
hr_admin_indi_has_employment @ hr_admin @ alice,
inference(cnf,[status(esa)],[ax75]) ).
thf(ax69,axiom,
system_indi_is_hr_admin @ system @ hr_admin ).
thf(zip_derived_cl69,plain,
system_indi_is_hr_admin @ system @ hr_admin,
inference(cnf,[status(esa)],[ax69]) ).
thf(ax21,axiom,
! [K: $i,HR: $i] :
( ( system_indi_is_hr_admin @ system @ HR )
=> ( ( hr_admin_indi_has_employment @ HR @ K )
=> ( admin_indi_has_employment @ admin @ K ) ) ) ).
thf(zip_derived_cl21,plain,
! [X0: $i,X1: $i] :
( ( admin_indi_has_employment @ admin @ X0 )
| ~ ( system_indi_is_hr_admin @ system @ X1 )
| ~ ( hr_admin_indi_has_employment @ X1 @ X0 ) ),
inference(cnf,[status(esa)],[ax21]) ).
thf(zip_derived_cl99,plain,
! [X0: $i] :
( ( admin_indi_has_employment @ admin @ X0 )
| ~ ( hr_admin_indi_has_employment @ hr_admin @ X0 ) ),
inference('s_sup-',[status(thm)],[zip_derived_cl69,zip_derived_cl21]) ).
thf(zip_derived_cl121,plain,
admin_indi_has_employment @ admin @ alice,
inference('s_sup-',[status(thm)],[zip_derived_cl75,zip_derived_cl99]) ).
thf(ax27,axiom,
! [K: $i,C: $i,CL: $i,SSO: $i] :
( ( 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 ) ) ) ) ) ) ) ) ) ) ) ) ).
thf(zip_derived_cl27,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ~ ( admin_indi_has_employment @ admin @ X0 )
| ~ ( admin_indi_has_polygraph_for_compartment @ admin @ X0 @ X1 )
| ~ ( admin_indi_has_background_for_compartment @ admin @ X0 @ X1 )
| ~ ( admin_indi_has_compartments @ admin @ X0 @ X2 )
| ( admin_indi_has_compartments @ admin @ X0 @ ( cons @ X1 @ X2 ) )
| ~ ( admin_indi_has_level_for_compartment @ admin @ X0 @ X1 )
| ~ ( admin_indi_has_credit_for_compartment @ admin @ X0 @ X1 )
| ~ ( admin_indi_has_citizenship @ admin @ X0 @ usa )
| ~ ( system_indi_needs_compartment @ system @ X0 @ X1 )
| ~ ( sso_indi_has_compartment @ X3 @ X0 @ X1 )
| ~ ( admin_compartment_has_sso @ admin @ X1 @ X3 ) ),
inference(cnf,[status(esa)],[ax27]) ).
thf(zip_derived_cl137,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ ( admin_indi_has_polygraph_for_compartment @ admin @ alice @ X0 )
| ~ ( admin_indi_has_background_for_compartment @ admin @ alice @ X0 )
| ~ ( admin_indi_has_compartments @ admin @ alice @ X1 )
| ( admin_indi_has_compartments @ admin @ alice @ ( cons @ X0 @ X1 ) )
| ~ ( admin_indi_has_level_for_compartment @ admin @ alice @ X0 )
| ~ ( admin_indi_has_credit_for_compartment @ admin @ alice @ X0 )
| ~ ( admin_indi_has_citizenship @ admin @ alice @ usa )
| ~ ( system_indi_needs_compartment @ system @ alice @ X0 )
| ~ ( sso_indi_has_compartment @ X2 @ alice @ X0 )
| ~ ( admin_compartment_has_sso @ admin @ X0 @ X2 ) ),
inference('s_sup-',[status(thm)],[zip_derived_cl121,zip_derived_cl27]) ).
thf(ax71,axiom,
system_indi_has_citizenship @ system @ alice @ usa ).
thf(zip_derived_cl71,plain,
system_indi_has_citizenship @ system @ alice @ usa,
inference(cnf,[status(esa)],[ax71]) ).
thf(ax23,axiom,
! [K: $i,U: $i] :
( ( system_indi_has_citizenship @ system @ K @ U )
=> ( admin_indi_has_citizenship @ admin @ K @ U ) ) ).
thf(zip_derived_cl23,plain,
! [X0: $i,X1: $i] :
( ( admin_indi_has_citizenship @ admin @ X0 @ X1 )
| ~ ( system_indi_has_citizenship @ system @ X0 @ X1 ) ),
inference(cnf,[status(esa)],[ax23]) ).
thf(zip_derived_cl100,plain,
admin_indi_has_citizenship @ admin @ alice @ usa,
inference('s_sup-',[status(thm)],[zip_derived_cl71,zip_derived_cl23]) ).
thf(zip_derived_cl138,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ ( admin_indi_has_polygraph_for_compartment @ admin @ alice @ X0 )
| ~ ( admin_indi_has_background_for_compartment @ admin @ alice @ X0 )
| ~ ( admin_indi_has_compartments @ admin @ alice @ X1 )
| ( admin_indi_has_compartments @ admin @ alice @ ( cons @ X0 @ X1 ) )
| ~ ( admin_indi_has_level_for_compartment @ admin @ alice @ X0 )
| ~ ( admin_indi_has_credit_for_compartment @ admin @ alice @ X0 )
| ~ ( system_indi_needs_compartment @ system @ alice @ X0 )
| ~ ( sso_indi_has_compartment @ X2 @ alice @ X0 )
| ~ ( admin_compartment_has_sso @ admin @ X0 @ X2 ) ),
inference(demod,[status(thm)],[zip_derived_cl137,zip_derived_cl100]) ).
thf(zip_derived_cl313,plain,
! [X0: $i] :
( ( admin_indi_has_compartments_for_file @ admin @ alice @ secretfile )
| ~ ( admin_indi_has_polygraph_for_compartment @ admin @ alice @ compartmentb )
| ~ ( admin_indi_has_background_for_compartment @ admin @ alice @ compartmentb )
| ~ ( admin_indi_has_compartments @ admin @ alice @ ( cons @ compartmenta @ nil ) )
| ~ ( admin_indi_has_level_for_compartment @ admin @ alice @ compartmentb )
| ~ ( admin_indi_has_credit_for_compartment @ admin @ alice @ compartmentb )
| ~ ( system_indi_needs_compartment @ system @ alice @ compartmentb )
| ~ ( sso_indi_has_compartment @ X0 @ alice @ compartmentb )
| ~ ( admin_compartment_has_sso @ admin @ compartmentb @ X0 ) ),
inference('s_sup+',[status(thm)],[zip_derived_cl215,zip_derived_cl138]) ).
thf(ax42,axiom,
oca_compartment_is_compartment @ oca @ compartmentb @ confidential @ topsecret @ yes @ yes ).
thf(zip_derived_cl42,plain,
oca_compartment_is_compartment @ oca @ compartmentb @ confidential @ topsecret @ yes @ yes,
inference(cnf,[status(esa)],[ax42]) ).
thf(ax41,axiom,
system_indi_is_oca @ system @ oca ).
thf(zip_derived_cl41,plain,
system_indi_is_oca @ system @ oca,
inference(cnf,[status(esa)],[ax41]) ).
thf(ax72,axiom,
polygraph_admin_indi_has_polygraph @ polygraph_admin @ alice ).
thf(zip_derived_cl72,plain,
polygraph_admin_indi_has_polygraph @ polygraph_admin @ alice,
inference(cnf,[status(esa)],[ax72]) ).
thf(ax66,axiom,
system_indi_is_polygraph_admin @ system @ polygraph_admin ).
thf(zip_derived_cl66,plain,
system_indi_is_polygraph_admin @ system @ polygraph_admin,
inference(cnf,[status(esa)],[ax66]) ).
thf(ax17,axiom,
! [K: $i,PA: $i] :
( ( system_indi_is_polygraph_admin @ system @ PA )
=> ( ( polygraph_admin_indi_has_polygraph @ PA @ K )
=> ( admin_indi_has_polygraph @ admin @ K ) ) ) ).
thf(zip_derived_cl17,plain,
! [X0: $i,X1: $i] :
( ( admin_indi_has_polygraph @ admin @ X0 )
| ~ ( system_indi_is_polygraph_admin @ system @ X1 )
| ~ ( polygraph_admin_indi_has_polygraph @ X1 @ X0 ) ),
inference(cnf,[status(esa)],[ax17]) ).
thf(zip_derived_cl97,plain,
! [X0: $i] :
( ( admin_indi_has_polygraph @ admin @ X0 )
| ~ ( polygraph_admin_indi_has_polygraph @ polygraph_admin @ X0 ) ),
inference('s_sup-',[status(thm)],[zip_derived_cl66,zip_derived_cl17]) ).
thf(zip_derived_cl103,plain,
admin_indi_has_polygraph @ admin @ alice,
inference('s_sup-',[status(thm)],[zip_derived_cl72,zip_derived_cl97]) ).
thf(ax30,axiom,
! [K: $i,C: $i,OCA: $i,L1: $i,L2: $i,B1: $i] :
( ( 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 ) ) ) ) ).
thf(zip_derived_cl30,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] :
( ( admin_indi_has_polygraph_for_compartment @ admin @ X0 @ X1 )
| ~ ( admin_indi_has_polygraph @ admin @ X0 )
| ~ ( system_indi_is_oca @ system @ X2 )
| ~ ( oca_compartment_is_compartment @ X2 @ X1 @ X3 @ X4 @ X5 @ yes ) ),
inference(cnf,[status(esa)],[ax30]) ).
thf(zip_derived_cl125,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( ( admin_indi_has_polygraph_for_compartment @ admin @ alice @ X0 )
| ~ ( system_indi_is_oca @ system @ X1 )
| ~ ( oca_compartment_is_compartment @ X1 @ X0 @ X4 @ X3 @ X2 @ yes ) ),
inference('s_sup-',[status(thm)],[zip_derived_cl103,zip_derived_cl30]) ).
thf(zip_derived_cl190,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ( admin_indi_has_polygraph_for_compartment @ admin @ alice @ X0 )
| ~ ( oca_compartment_is_compartment @ oca @ X0 @ X3 @ X2 @ X1 @ yes ) ),
inference('s_sup-',[status(thm)],[zip_derived_cl41,zip_derived_cl125]) ).
thf(zip_derived_cl191,plain,
admin_indi_has_polygraph_for_compartment @ admin @ alice @ compartmentb,
inference('s_sup-',[status(thm)],[zip_derived_cl42,zip_derived_cl190]) ).
thf(zip_derived_cl42_003,plain,
oca_compartment_is_compartment @ oca @ compartmentb @ confidential @ topsecret @ yes @ yes,
inference(cnf,[status(esa)],[ax42]) ).
thf(ax74,axiom,
background_admin_indi_has_background @ background_admin @ alice @ topsecret ).
thf(zip_derived_cl74,plain,
background_admin_indi_has_background @ background_admin @ alice @ topsecret,
inference(cnf,[status(esa)],[ax74]) ).
thf(ax4,axiom,
! [K: $i,L: $i] : ( loca_level_below @ K @ L @ L ) ).
thf(zip_derived_cl4,plain,
! [X0: $i,X1: $i] : ( loca_level_below @ X0 @ X1 @ X1 ),
inference(cnf,[status(esa)],[ax4]) ).
thf(ax68,axiom,
system_indi_is_background_admin @ system @ background_admin ).
thf(zip_derived_cl68,plain,
system_indi_is_background_admin @ system @ background_admin,
inference(cnf,[status(esa)],[ax68]) ).
thf(ax20,axiom,
! [K: $i,L: $i,BA: $i,L1: $i] :
( ( 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 ) ) ) ) ).
thf(zip_derived_cl20,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ( admin_indi_has_background @ admin @ X0 @ X1 )
| ~ ( system_indi_is_background_admin @ system @ X2 )
| ~ ( loca_level_below @ admin @ X1 @ X3 )
| ~ ( background_admin_indi_has_background @ X2 @ X0 @ X3 ) ),
inference(cnf,[status(esa)],[ax20]) ).
thf(zip_derived_cl119,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( admin_indi_has_background @ admin @ X1 @ X0 )
| ~ ( loca_level_below @ admin @ X0 @ X2 )
| ~ ( background_admin_indi_has_background @ background_admin @ X1 @ X2 ) ),
inference('s_sup-',[status(thm)],[zip_derived_cl68,zip_derived_cl20]) ).
thf(zip_derived_cl148,plain,
! [X0: $i,X1: $i] :
( ( admin_indi_has_background @ admin @ X1 @ X0 )
| ~ ( background_admin_indi_has_background @ background_admin @ X1 @ X0 ) ),
inference('s_sup-',[status(thm)],[zip_derived_cl4,zip_derived_cl119]) ).
thf(zip_derived_cl163,plain,
admin_indi_has_background @ admin @ alice @ topsecret,
inference('s_sup-',[status(thm)],[zip_derived_cl74,zip_derived_cl148]) ).
thf(zip_derived_cl41_004,plain,
system_indi_is_oca @ system @ oca,
inference(cnf,[status(esa)],[ax41]) ).
thf(ax28,axiom,
! [K: $i,C: $i,OCA: $i,L1: $i,L2: $i,B1: $i,B2: $i] :
( ( 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 ) ) ) ) ).
thf(zip_derived_cl28,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i] :
( ( admin_indi_has_background_for_compartment @ admin @ X0 @ X1 )
| ~ ( admin_indi_has_background @ admin @ X0 @ X2 )
| ~ ( system_indi_is_oca @ system @ X3 )
| ~ ( oca_compartment_is_compartment @ X3 @ X1 @ X4 @ X2 @ X5 @ X6 ) ),
inference(cnf,[status(esa)],[ax28]) ).
thf(zip_derived_cl129,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] :
( ( admin_indi_has_background_for_compartment @ admin @ X1 @ X0 )
| ~ ( admin_indi_has_background @ admin @ X1 @ X2 )
| ~ ( oca_compartment_is_compartment @ oca @ X0 @ X5 @ X2 @ X4 @ X3 ) ),
inference('s_sup-',[status(thm)],[zip_derived_cl41,zip_derived_cl28]) ).
thf(zip_derived_cl201,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ( admin_indi_has_background_for_compartment @ admin @ alice @ X0 )
| ~ ( oca_compartment_is_compartment @ oca @ X0 @ X3 @ topsecret @ X2 @ X1 ) ),
inference('s_sup-',[status(thm)],[zip_derived_cl163,zip_derived_cl129]) ).
thf(zip_derived_cl203,plain,
admin_indi_has_background_for_compartment @ admin @ alice @ compartmentb,
inference('s_sup-',[status(thm)],[zip_derived_cl42,zip_derived_cl201]) ).
thf(zip_derived_cl42_005,plain,
oca_compartment_is_compartment @ oca @ compartmentb @ confidential @ topsecret @ yes @ yes,
inference(cnf,[status(esa)],[ax42]) ).
thf(zip_derived_cl4_006,plain,
! [X0: $i,X1: $i] : ( loca_level_below @ X0 @ X1 @ X1 ),
inference(cnf,[status(esa)],[ax4]) ).
thf(ax2,axiom,
! [K: $i] : ( loca_level_direct_below @ K @ confidential @ secret ) ).
thf(zip_derived_cl2,plain,
! [X0: $i] : ( loca_level_direct_below @ X0 @ confidential @ secret ),
inference(cnf,[status(esa)],[ax2]) ).
thf(ax5,axiom,
! [K: $i,L: $i,L1: $i,L11: $i] :
( ( loca_level_direct_below @ K @ L1 @ L11 )
=> ( ( loca_level_below @ K @ L @ L1 )
=> ( loca_level_below @ K @ L @ L11 ) ) ) ).
thf(zip_derived_cl5,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ~ ( loca_level_below @ X0 @ X1 @ X2 )
| ~ ( loca_level_direct_below @ X0 @ X2 @ X3 )
| ( loca_level_below @ X0 @ X1 @ X3 ) ),
inference(cnf,[status(esa)],[ax5]) ).
thf(zip_derived_cl90,plain,
! [X0: $i,X1: $i] :
( ~ ( loca_level_below @ X0 @ X1 @ confidential )
| ( loca_level_below @ X0 @ X1 @ secret ) ),
inference('s_sup-',[status(thm)],[zip_derived_cl2,zip_derived_cl5]) ).
thf(zip_derived_cl141,plain,
! [X0: $i] : ( loca_level_below @ X0 @ confidential @ secret ),
inference('s_sup-',[status(thm)],[zip_derived_cl4,zip_derived_cl90]) ).
thf(ax3,axiom,
! [K: $i] : ( loca_level_direct_below @ K @ secret @ topsecret ) ).
thf(zip_derived_cl3,plain,
! [X0: $i] : ( loca_level_direct_below @ X0 @ secret @ topsecret ),
inference(cnf,[status(esa)],[ax3]) ).
thf(zip_derived_cl5_007,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ~ ( loca_level_below @ X0 @ X1 @ X2 )
| ~ ( loca_level_direct_below @ X0 @ X2 @ X3 )
| ( loca_level_below @ X0 @ X1 @ X3 ) ),
inference(cnf,[status(esa)],[ax5]) ).
thf(zip_derived_cl91,plain,
! [X0: $i,X1: $i] :
( ~ ( loca_level_below @ X0 @ X1 @ secret )
| ( loca_level_below @ X0 @ X1 @ topsecret ) ),
inference('s_sup-',[status(thm)],[zip_derived_cl3,zip_derived_cl5]) ).
thf(zip_derived_cl145,plain,
! [X0: $i] : ( loca_level_below @ X0 @ confidential @ topsecret ),
inference('s_sup-',[status(thm)],[zip_derived_cl141,zip_derived_cl91]) ).
thf(zip_derived_cl141_008,plain,
! [X0: $i] : ( loca_level_below @ X0 @ confidential @ secret ),
inference('s_sup-',[status(thm)],[zip_derived_cl4,zip_derived_cl90]) ).
thf(ax70,axiom,
system_indi_is_level_admin @ system @ level_admin ).
thf(zip_derived_cl70,plain,
system_indi_is_level_admin @ system @ level_admin,
inference(cnf,[status(esa)],[ax70]) ).
thf(zip_derived_cl121_009,plain,
admin_indi_has_employment @ admin @ alice,
inference('s_sup-',[status(thm)],[zip_derived_cl75,zip_derived_cl99]) ).
thf(ax25,axiom,
! [K: $i,L: $i,L1: $i,LA: $i,L11: $i] :
( ( 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 ) ) ) ) ) ) ) ) ) ) ) ).
thf(zip_derived_cl25,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( ~ ( admin_indi_has_citizenship @ admin @ X0 @ usa )
| ~ ( admin_indi_has_employment @ admin @ X0 )
| ~ ( loca_level_below @ admin @ X1 @ X2 )
| ~ ( admin_indi_has_background @ admin @ X0 @ X1 )
| ( admin_indi_has_level @ admin @ X0 @ X1 )
| ~ ( system_indi_is_level_admin @ system @ X3 )
| ~ ( admin_indi_has_credit @ admin @ X0 )
| ~ ( admin_indi_has_polygraph @ admin @ X0 )
| ~ ( system_indi_needs_level @ system @ X0 @ X2 )
| ~ ( loca_level_below @ admin @ X1 @ X4 )
| ~ ( level_admin_indi_has_level @ X3 @ X0 @ X4 ) ),
inference(cnf,[status(esa)],[ax25]) ).
thf(zip_derived_cl135,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ~ ( admin_indi_has_citizenship @ admin @ alice @ usa )
| ~ ( loca_level_below @ admin @ X1 @ X0 )
| ~ ( admin_indi_has_background @ admin @ alice @ X1 )
| ( admin_indi_has_level @ admin @ alice @ X1 )
| ~ ( system_indi_is_level_admin @ system @ X2 )
| ~ ( admin_indi_has_credit @ admin @ alice )
| ~ ( admin_indi_has_polygraph @ admin @ alice )
| ~ ( system_indi_needs_level @ system @ alice @ X0 )
| ~ ( loca_level_below @ admin @ X1 @ X3 )
| ~ ( level_admin_indi_has_level @ X2 @ alice @ X3 ) ),
inference('s_sup-',[status(thm)],[zip_derived_cl121,zip_derived_cl25]) ).
thf(zip_derived_cl100_010,plain,
admin_indi_has_citizenship @ admin @ alice @ usa,
inference('s_sup-',[status(thm)],[zip_derived_cl71,zip_derived_cl23]) ).
thf(ax73,axiom,
credit_admin_indi_has_credit @ credit_admin @ alice ).
thf(zip_derived_cl73,plain,
credit_admin_indi_has_credit @ credit_admin @ alice,
inference(cnf,[status(esa)],[ax73]) ).
thf(ax67,axiom,
system_indi_is_credit_admin @ system @ credit_admin ).
thf(zip_derived_cl67,plain,
system_indi_is_credit_admin @ system @ credit_admin,
inference(cnf,[status(esa)],[ax67]) ).
thf(ax18,axiom,
! [K: $i,CA: $i] :
( ( system_indi_is_credit_admin @ system @ CA )
=> ( ( credit_admin_indi_has_credit @ CA @ K )
=> ( admin_indi_has_credit @ admin @ K ) ) ) ).
thf(zip_derived_cl18,plain,
! [X0: $i,X1: $i] :
( ( admin_indi_has_credit @ admin @ X0 )
| ~ ( system_indi_is_credit_admin @ system @ X1 )
| ~ ( credit_admin_indi_has_credit @ X1 @ X0 ) ),
inference(cnf,[status(esa)],[ax18]) ).
thf(zip_derived_cl98,plain,
! [X0: $i] :
( ( admin_indi_has_credit @ admin @ X0 )
| ~ ( credit_admin_indi_has_credit @ credit_admin @ X0 ) ),
inference('s_sup-',[status(thm)],[zip_derived_cl67,zip_derived_cl18]) ).
thf(zip_derived_cl113,plain,
admin_indi_has_credit @ admin @ alice,
inference('s_sup-',[status(thm)],[zip_derived_cl73,zip_derived_cl98]) ).
thf(zip_derived_cl103_011,plain,
admin_indi_has_polygraph @ admin @ alice,
inference('s_sup-',[status(thm)],[zip_derived_cl72,zip_derived_cl97]) ).
thf(zip_derived_cl136,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ~ ( loca_level_below @ admin @ X1 @ X0 )
| ~ ( admin_indi_has_background @ admin @ alice @ X1 )
| ( admin_indi_has_level @ admin @ alice @ X1 )
| ~ ( system_indi_is_level_admin @ system @ X2 )
| ~ ( system_indi_needs_level @ system @ alice @ X0 )
| ~ ( loca_level_below @ admin @ X1 @ X3 )
| ~ ( level_admin_indi_has_level @ X2 @ alice @ X3 ) ),
inference(demod,[status(thm)],[zip_derived_cl135,zip_derived_cl100,zip_derived_cl113,zip_derived_cl103]) ).
thf(zip_derived_cl274,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ ( loca_level_below @ admin @ X1 @ X0 )
| ~ ( admin_indi_has_background @ admin @ alice @ X1 )
| ( admin_indi_has_level @ admin @ alice @ X1 )
| ~ ( system_indi_needs_level @ system @ alice @ X0 )
| ~ ( loca_level_below @ admin @ X1 @ X2 )
| ~ ( level_admin_indi_has_level @ level_admin @ alice @ X2 ) ),
inference('s_sup-',[status(thm)],[zip_derived_cl70,zip_derived_cl136]) ).
thf(zip_derived_cl285,plain,
! [X0: $i] :
( ~ ( admin_indi_has_background @ admin @ alice @ confidential )
| ( admin_indi_has_level @ admin @ alice @ confidential )
| ~ ( system_indi_needs_level @ system @ alice @ secret )
| ~ ( loca_level_below @ admin @ confidential @ X0 )
| ~ ( level_admin_indi_has_level @ level_admin @ alice @ X0 ) ),
inference('s_sup-',[status(thm)],[zip_derived_cl141,zip_derived_cl274]) ).
thf(zip_derived_cl74_012,plain,
background_admin_indi_has_background @ background_admin @ alice @ topsecret,
inference(cnf,[status(esa)],[ax74]) ).
thf(zip_derived_cl145_013,plain,
! [X0: $i] : ( loca_level_below @ X0 @ confidential @ topsecret ),
inference('s_sup-',[status(thm)],[zip_derived_cl141,zip_derived_cl91]) ).
thf(zip_derived_cl119_014,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( admin_indi_has_background @ admin @ X1 @ X0 )
| ~ ( loca_level_below @ admin @ X0 @ X2 )
| ~ ( background_admin_indi_has_background @ background_admin @ X1 @ X2 ) ),
inference('s_sup-',[status(thm)],[zip_derived_cl68,zip_derived_cl20]) ).
thf(zip_derived_cl157,plain,
! [X0: $i] :
( ( admin_indi_has_background @ admin @ X0 @ confidential )
| ~ ( background_admin_indi_has_background @ background_admin @ X0 @ topsecret ) ),
inference('s_sup-',[status(thm)],[zip_derived_cl145,zip_derived_cl119]) ).
thf(zip_derived_cl167,plain,
admin_indi_has_background @ admin @ alice @ confidential,
inference('s_sup-',[status(thm)],[zip_derived_cl74,zip_derived_cl157]) ).
thf(ax76,axiom,
system_indi_needs_level @ system @ alice @ secret ).
thf(zip_derived_cl76,plain,
system_indi_needs_level @ system @ alice @ secret,
inference(cnf,[status(esa)],[ax76]) ).
thf(zip_derived_cl295,plain,
! [X0: $i] :
( ( admin_indi_has_level @ admin @ alice @ confidential )
| ~ ( loca_level_below @ admin @ confidential @ X0 )
| ~ ( level_admin_indi_has_level @ level_admin @ alice @ X0 ) ),
inference(demod,[status(thm)],[zip_derived_cl285,zip_derived_cl167,zip_derived_cl76]) ).
thf(zip_derived_cl307,plain,
( ( admin_indi_has_level @ admin @ alice @ confidential )
| ~ ( level_admin_indi_has_level @ level_admin @ alice @ topsecret ) ),
inference('s_sup-',[status(thm)],[zip_derived_cl145,zip_derived_cl295]) ).
thf(ax77,axiom,
level_admin_indi_has_level @ level_admin @ alice @ topsecret ).
thf(zip_derived_cl77,plain,
level_admin_indi_has_level @ level_admin @ alice @ topsecret,
inference(cnf,[status(esa)],[ax77]) ).
thf(zip_derived_cl308,plain,
admin_indi_has_level @ admin @ alice @ confidential,
inference(demod,[status(thm)],[zip_derived_cl307,zip_derived_cl77]) ).
thf(zip_derived_cl41_015,plain,
system_indi_is_oca @ system @ oca,
inference(cnf,[status(esa)],[ax41]) ).
thf(ax29,axiom,
! [K: $i,C: $i,OCA: $i,L1: $i,L2: $i,B1: $i,B2: $i] :
( ( 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 ) ) ) ) ).
thf(zip_derived_cl29,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i] :
( ( admin_indi_has_level_for_compartment @ admin @ X0 @ X1 )
| ~ ( admin_indi_has_level @ admin @ X0 @ X2 )
| ~ ( system_indi_is_oca @ system @ X3 )
| ~ ( oca_compartment_is_compartment @ X3 @ X1 @ X2 @ X4 @ X5 @ X6 ) ),
inference(cnf,[status(esa)],[ax29]) ).
thf(zip_derived_cl133,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] :
( ( admin_indi_has_level_for_compartment @ admin @ X1 @ X0 )
| ~ ( admin_indi_has_level @ admin @ X1 @ X2 )
| ~ ( oca_compartment_is_compartment @ oca @ X0 @ X2 @ X5 @ X4 @ X3 ) ),
inference('s_sup-',[status(thm)],[zip_derived_cl41,zip_derived_cl29]) ).
thf(zip_derived_cl309,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ( admin_indi_has_level_for_compartment @ admin @ alice @ X0 )
| ~ ( oca_compartment_is_compartment @ oca @ X0 @ confidential @ X3 @ X2 @ X1 ) ),
inference('s_sup-',[status(thm)],[zip_derived_cl308,zip_derived_cl133]) ).
thf(zip_derived_cl310,plain,
admin_indi_has_level_for_compartment @ admin @ alice @ compartmentb,
inference('s_sup-',[status(thm)],[zip_derived_cl42,zip_derived_cl309]) ).
thf(zip_derived_cl42_016,plain,
oca_compartment_is_compartment @ oca @ compartmentb @ confidential @ topsecret @ yes @ yes,
inference(cnf,[status(esa)],[ax42]) ).
thf(zip_derived_cl41_017,plain,
system_indi_is_oca @ system @ oca,
inference(cnf,[status(esa)],[ax41]) ).
thf(zip_derived_cl113_018,plain,
admin_indi_has_credit @ admin @ alice,
inference('s_sup-',[status(thm)],[zip_derived_cl73,zip_derived_cl98]) ).
thf(ax32,axiom,
! [K: $i,C: $i,OCA: $i,L1: $i,L2: $i,B2: $i] :
( ( 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 ) ) ) ) ).
thf(zip_derived_cl32,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] :
( ( admin_indi_has_credit_for_compartment @ admin @ X0 @ X1 )
| ~ ( admin_indi_has_credit @ admin @ X0 )
| ~ ( system_indi_is_oca @ system @ X2 )
| ~ ( oca_compartment_is_compartment @ X2 @ X1 @ X3 @ X4 @ yes @ X5 ) ),
inference(cnf,[status(esa)],[ax32]) ).
thf(zip_derived_cl126,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( ( admin_indi_has_credit_for_compartment @ admin @ alice @ X0 )
| ~ ( system_indi_is_oca @ system @ X1 )
| ~ ( oca_compartment_is_compartment @ X1 @ X0 @ X4 @ X3 @ yes @ X2 ) ),
inference('s_sup-',[status(thm)],[zip_derived_cl113,zip_derived_cl32]) ).
thf(zip_derived_cl192,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ( admin_indi_has_credit_for_compartment @ admin @ alice @ X0 )
| ~ ( oca_compartment_is_compartment @ oca @ X0 @ X3 @ X2 @ yes @ X1 ) ),
inference('s_sup-',[status(thm)],[zip_derived_cl41,zip_derived_cl126]) ).
thf(zip_derived_cl196,plain,
admin_indi_has_credit_for_compartment @ admin @ alice @ compartmentb,
inference('s_sup-',[status(thm)],[zip_derived_cl42,zip_derived_cl192]) ).
thf(ax78,axiom,
system_indi_needs_compartment @ system @ alice @ compartmentb ).
thf(zip_derived_cl78,plain,
system_indi_needs_compartment @ system @ alice @ compartmentb,
inference(cnf,[status(esa)],[ax78]) ).
thf(zip_derived_cl316,plain,
! [X0: $i] :
( ( admin_indi_has_compartments_for_file @ admin @ alice @ secretfile )
| ~ ( admin_indi_has_compartments @ admin @ alice @ ( cons @ compartmenta @ nil ) )
| ~ ( sso_indi_has_compartment @ X0 @ alice @ compartmentb )
| ~ ( admin_compartment_has_sso @ admin @ compartmentb @ X0 ) ),
inference(demod,[status(thm)],[zip_derived_cl313,zip_derived_cl191,zip_derived_cl203,zip_derived_cl310,zip_derived_cl196,zip_derived_cl78]) ).
thf(zip_derived_cl4_019,plain,
! [X0: $i,X1: $i] : ( loca_level_below @ X0 @ X1 @ X1 ),
inference(cnf,[status(esa)],[ax4]) ).
thf(zip_derived_cl91_020,plain,
! [X0: $i,X1: $i] :
( ~ ( loca_level_below @ X0 @ X1 @ secret )
| ( loca_level_below @ X0 @ X1 @ topsecret ) ),
inference('s_sup-',[status(thm)],[zip_derived_cl3,zip_derived_cl5]) ).
thf(zip_derived_cl144,plain,
! [X0: $i] : ( loca_level_below @ X0 @ secret @ topsecret ),
inference('s_sup-',[status(thm)],[zip_derived_cl4,zip_derived_cl91]) ).
thf(zip_derived_cl74_021,plain,
background_admin_indi_has_background @ background_admin @ alice @ topsecret,
inference(cnf,[status(esa)],[ax74]) ).
thf(zip_derived_cl144_022,plain,
! [X0: $i] : ( loca_level_below @ X0 @ secret @ topsecret ),
inference('s_sup-',[status(thm)],[zip_derived_cl4,zip_derived_cl91]) ).
thf(zip_derived_cl119_023,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( admin_indi_has_background @ admin @ X1 @ X0 )
| ~ ( loca_level_below @ admin @ X0 @ X2 )
| ~ ( background_admin_indi_has_background @ background_admin @ X1 @ X2 ) ),
inference('s_sup-',[status(thm)],[zip_derived_cl68,zip_derived_cl20]) ).
thf(zip_derived_cl158,plain,
! [X0: $i] :
( ( admin_indi_has_background @ admin @ X0 @ secret )
| ~ ( background_admin_indi_has_background @ background_admin @ X0 @ topsecret ) ),
inference('s_sup-',[status(thm)],[zip_derived_cl144,zip_derived_cl119]) ).
thf(zip_derived_cl168,plain,
admin_indi_has_background @ admin @ alice @ secret,
inference('s_sup-',[status(thm)],[zip_derived_cl74,zip_derived_cl158]) ).
thf(zip_derived_cl4_024,plain,
! [X0: $i,X1: $i] : ( loca_level_below @ X0 @ X1 @ X1 ),
inference(cnf,[status(esa)],[ax4]) ).
thf(zip_derived_cl274_025,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ ( loca_level_below @ admin @ X1 @ X0 )
| ~ ( admin_indi_has_background @ admin @ alice @ X1 )
| ( admin_indi_has_level @ admin @ alice @ X1 )
| ~ ( system_indi_needs_level @ system @ alice @ X0 )
| ~ ( loca_level_below @ admin @ X1 @ X2 )
| ~ ( level_admin_indi_has_level @ level_admin @ alice @ X2 ) ),
inference('s_sup-',[status(thm)],[zip_derived_cl70,zip_derived_cl136]) ).
thf(zip_derived_cl277,plain,
! [X0: $i,X1: $i] :
( ~ ( admin_indi_has_background @ admin @ alice @ X0 )
| ( admin_indi_has_level @ admin @ alice @ X0 )
| ~ ( system_indi_needs_level @ system @ alice @ X0 )
| ~ ( loca_level_below @ admin @ X0 @ X1 )
| ~ ( level_admin_indi_has_level @ level_admin @ alice @ X1 ) ),
inference('s_sup-',[status(thm)],[zip_derived_cl4,zip_derived_cl274]) ).
thf(zip_derived_cl327,plain,
! [X0: $i] :
( ( admin_indi_has_level @ admin @ alice @ secret )
| ~ ( system_indi_needs_level @ system @ alice @ secret )
| ~ ( loca_level_below @ admin @ secret @ X0 )
| ~ ( level_admin_indi_has_level @ level_admin @ alice @ X0 ) ),
inference('s_sup-',[status(thm)],[zip_derived_cl168,zip_derived_cl277]) ).
thf(zip_derived_cl76_026,plain,
system_indi_needs_level @ system @ alice @ secret,
inference(cnf,[status(esa)],[ax76]) ).
thf(zip_derived_cl332,plain,
! [X0: $i] :
( ( admin_indi_has_level @ admin @ alice @ secret )
| ~ ( loca_level_below @ admin @ secret @ X0 )
| ~ ( level_admin_indi_has_level @ level_admin @ alice @ X0 ) ),
inference(demod,[status(thm)],[zip_derived_cl327,zip_derived_cl76]) ).
thf(zip_derived_cl334,plain,
( ( admin_indi_has_level @ admin @ alice @ secret )
| ~ ( level_admin_indi_has_level @ level_admin @ alice @ topsecret ) ),
inference('s_sup-',[status(thm)],[zip_derived_cl144,zip_derived_cl332]) ).
thf(zip_derived_cl77_027,plain,
level_admin_indi_has_level @ level_admin @ alice @ topsecret,
inference(cnf,[status(esa)],[ax77]) ).
thf(zip_derived_cl335,plain,
admin_indi_has_level @ admin @ alice @ secret,
inference(demod,[status(thm)],[zip_derived_cl334,zip_derived_cl77]) ).
thf(zip_derived_cl214_028,plain,
admin_file_has_compartments @ admin @ secretfile @ ( cons @ compartmentb @ ( cons @ compartmenta @ nil ) ),
inference(demod,[status(thm)],[zip_derived_cl212,zip_derived_cl9,zip_derived_cl53]) ).
thf(ax54,axiom,
system_file_needs_level @ system @ secretfile @ secret ).
thf(zip_derived_cl54,plain,
system_file_needs_level @ system @ secretfile @ secret,
inference(cnf,[status(esa)],[ax54]) ).
thf(ax11,axiom,
! [F: $i,L: $i,CL: $i] :
( ( 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 ) ) ) ) ).
thf(zip_derived_cl11,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( admin_file_has_level @ admin @ X0 @ X1 )
| ~ ( system_file_needs_level @ system @ X0 @ X1 )
| ~ ( admin_file_has_level_h @ admin @ X0 @ X1 @ X2 )
| ~ ( admin_file_has_compartments @ admin @ X0 @ X2 ) ),
inference(cnf,[status(esa)],[ax11]) ).
thf(zip_derived_cl114,plain,
! [X0: $i] :
( ( admin_file_has_level @ admin @ secretfile @ secret )
| ~ ( admin_file_has_level_h @ admin @ secretfile @ secret @ X0 )
| ~ ( admin_file_has_compartments @ admin @ secretfile @ X0 ) ),
inference('s_sup-',[status(thm)],[zip_derived_cl54,zip_derived_cl11]) ).
thf(zip_derived_cl216,plain,
( ( admin_file_has_level @ admin @ secretfile @ secret )
| ~ ( admin_file_has_level_h @ admin @ secretfile @ secret @ ( cons @ compartmentb @ ( cons @ compartmenta @ nil ) ) ) ),
inference('s_sup-',[status(thm)],[zip_derived_cl214,zip_derived_cl114]) ).
thf(ax55,axiom,
sso_file_has_level @ sso_compartmentb @ secretfile @ secret @ scg_compartmentb ).
thf(zip_derived_cl55,plain,
sso_file_has_level @ sso_compartmentb @ secretfile @ secret @ scg_compartmentb,
inference(cnf,[status(esa)],[ax55]) ).
thf(ax46,axiom,
sso_compartment_has_scg @ sso_compartmentb @ compartmentb @ scg_compartmentb ).
thf(zip_derived_cl46,plain,
sso_compartment_has_scg @ sso_compartmentb @ compartmentb @ scg_compartmentb,
inference(cnf,[status(esa)],[ax46]) ).
thf(zip_derived_cl92_029,plain,
admin_compartment_has_sso @ admin @ compartmentb @ sso_compartmentb,
inference('s_sup-',[status(thm)],[zip_derived_cl44,zip_derived_cl6]) ).
thf(zip_derived_cl41_030,plain,
system_indi_is_oca @ system @ oca,
inference(cnf,[status(esa)],[ax41]) ).
thf(ax7,axiom,
! [OCA: $i,C: $i,SSO: $i,SCG: $i] :
( ( 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 ) ) ) ) ) ).
thf(zip_derived_cl7,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ~ ( admin_compartment_has_sso @ admin @ X0 @ X1 )
| ~ ( system_indi_is_oca @ system @ X2 )
| ( admin_compartment_has_scg @ admin @ X0 @ X3 )
| ~ ( sso_compartment_has_scg @ X1 @ X0 @ X3 )
| ~ ( oca_compartment_has_scg @ X2 @ X0 @ X3 ) ),
inference(cnf,[status(esa)],[ax7]) ).
thf(zip_derived_cl94,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ ( admin_compartment_has_sso @ admin @ X1 @ X0 )
| ( admin_compartment_has_scg @ admin @ X1 @ X2 )
| ~ ( sso_compartment_has_scg @ X0 @ X1 @ X2 )
| ~ ( oca_compartment_has_scg @ oca @ X1 @ X2 ) ),
inference('s_sup-',[status(thm)],[zip_derived_cl41,zip_derived_cl7]) ).
thf(zip_derived_cl164,plain,
! [X0: $i] :
( ( admin_compartment_has_scg @ admin @ compartmentb @ X0 )
| ~ ( sso_compartment_has_scg @ sso_compartmentb @ compartmentb @ X0 )
| ~ ( oca_compartment_has_scg @ oca @ compartmentb @ X0 ) ),
inference('s_sup-',[status(thm)],[zip_derived_cl92,zip_derived_cl94]) ).
thf(zip_derived_cl186,plain,
( ( admin_compartment_has_scg @ admin @ compartmentb @ scg_compartmentb )
| ~ ( oca_compartment_has_scg @ oca @ compartmentb @ scg_compartmentb ) ),
inference('s_sup-',[status(thm)],[zip_derived_cl46,zip_derived_cl164]) ).
thf(ax45,axiom,
oca_compartment_has_scg @ oca @ compartmentb @ scg_compartmentb ).
thf(zip_derived_cl45,plain,
oca_compartment_has_scg @ oca @ compartmentb @ scg_compartmentb,
inference(cnf,[status(esa)],[ax45]) ).
thf(zip_derived_cl187,plain,
admin_compartment_has_scg @ admin @ compartmentb @ scg_compartmentb,
inference(demod,[status(thm)],[zip_derived_cl186,zip_derived_cl45]) ).
thf(zip_derived_cl92_031,plain,
admin_compartment_has_sso @ admin @ compartmentb @ sso_compartmentb,
inference('s_sup-',[status(thm)],[zip_derived_cl44,zip_derived_cl6]) ).
thf(ax13,axiom,
! [F: $i,L: $i,C: $i,CL: $i,SSO: $i,SCG: $i] :
( ( 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 ) ) ) ) ) ) ).
thf(zip_derived_cl13,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] :
( ~ ( admin_file_has_level_h @ admin @ X0 @ X1 @ X2 )
| ( admin_file_has_level_h @ admin @ X0 @ X1 @ ( cons @ X3 @ X2 ) )
| ~ ( admin_compartment_has_sso @ admin @ X3 @ X4 )
| ~ ( sso_file_has_level @ X4 @ X0 @ X1 @ X5 )
| ~ ( admin_compartment_has_scg @ admin @ X3 @ X5 ) ),
inference(cnf,[status(esa)],[ax13]) ).
thf(zip_derived_cl123,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ~ ( admin_file_has_level_h @ admin @ X2 @ X1 @ X0 )
| ( admin_file_has_level_h @ admin @ X2 @ X1 @ ( cons @ compartmentb @ X0 ) )
| ~ ( sso_file_has_level @ sso_compartmentb @ X2 @ X1 @ X3 )
| ~ ( admin_compartment_has_scg @ admin @ compartmentb @ X3 ) ),
inference('s_sup-',[status(thm)],[zip_derived_cl92,zip_derived_cl13]) ).
thf(zip_derived_cl204,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ ( admin_file_has_level_h @ admin @ X2 @ X1 @ X0 )
| ( admin_file_has_level_h @ admin @ X2 @ X1 @ ( cons @ compartmentb @ X0 ) )
| ~ ( sso_file_has_level @ sso_compartmentb @ X2 @ X1 @ scg_compartmentb ) ),
inference('s_sup-',[status(thm)],[zip_derived_cl187,zip_derived_cl123]) ).
thf(zip_derived_cl206,plain,
! [X0: $i] :
( ~ ( admin_file_has_level_h @ admin @ secretfile @ secret @ X0 )
| ( admin_file_has_level_h @ admin @ secretfile @ secret @ ( cons @ compartmentb @ X0 ) ) ),
inference('s_sup-',[status(thm)],[zip_derived_cl55,zip_derived_cl204]) ).
thf(zip_derived_cl223,plain,
( ( admin_file_has_level @ admin @ secretfile @ secret )
| ~ ( admin_file_has_level_h @ admin @ secretfile @ secret @ ( cons @ compartmenta @ nil ) ) ),
inference('s_sup+',[status(thm)],[zip_derived_cl216,zip_derived_cl206]) ).
thf(ax12,axiom,
! [F: $i,L: $i] : ( admin_file_has_level_h @ admin @ F @ L @ nil ) ).
thf(zip_derived_cl12,plain,
! [X0: $i,X1: $i] : ( admin_file_has_level_h @ admin @ X0 @ X1 @ nil ),
inference(cnf,[status(esa)],[ax12]) ).
thf(ax56,axiom,
sso_file_has_level @ sso_compartmenta @ secretfile @ secret @ scg_compartmenta ).
thf(zip_derived_cl56,plain,
sso_file_has_level @ sso_compartmenta @ secretfile @ secret @ scg_compartmenta,
inference(cnf,[status(esa)],[ax56]) ).
thf(ax49,axiom,
sso_compartment_has_scg @ sso_compartmenta @ compartmenta @ scg_compartmenta ).
thf(zip_derived_cl49,plain,
sso_compartment_has_scg @ sso_compartmenta @ compartmenta @ scg_compartmenta,
inference(cnf,[status(esa)],[ax49]) ).
thf(zip_derived_cl93_032,plain,
admin_compartment_has_sso @ admin @ compartmenta @ sso_compartmenta,
inference('s_sup-',[status(thm)],[zip_derived_cl47,zip_derived_cl6]) ).
thf(zip_derived_cl94_033,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ ( admin_compartment_has_sso @ admin @ X1 @ X0 )
| ( admin_compartment_has_scg @ admin @ X1 @ X2 )
| ~ ( sso_compartment_has_scg @ X0 @ X1 @ X2 )
| ~ ( oca_compartment_has_scg @ oca @ X1 @ X2 ) ),
inference('s_sup-',[status(thm)],[zip_derived_cl41,zip_derived_cl7]) ).
thf(zip_derived_cl165,plain,
! [X0: $i] :
( ( admin_compartment_has_scg @ admin @ compartmenta @ X0 )
| ~ ( sso_compartment_has_scg @ sso_compartmenta @ compartmenta @ X0 )
| ~ ( oca_compartment_has_scg @ oca @ compartmenta @ X0 ) ),
inference('s_sup-',[status(thm)],[zip_derived_cl93,zip_derived_cl94]) ).
thf(zip_derived_cl188,plain,
( ( admin_compartment_has_scg @ admin @ compartmenta @ scg_compartmenta )
| ~ ( oca_compartment_has_scg @ oca @ compartmenta @ scg_compartmenta ) ),
inference('s_sup-',[status(thm)],[zip_derived_cl49,zip_derived_cl165]) ).
thf(ax48,axiom,
oca_compartment_has_scg @ oca @ compartmenta @ scg_compartmenta ).
thf(zip_derived_cl48,plain,
oca_compartment_has_scg @ oca @ compartmenta @ scg_compartmenta,
inference(cnf,[status(esa)],[ax48]) ).
thf(zip_derived_cl189,plain,
admin_compartment_has_scg @ admin @ compartmenta @ scg_compartmenta,
inference(demod,[status(thm)],[zip_derived_cl188,zip_derived_cl48]) ).
thf(zip_derived_cl93_034,plain,
admin_compartment_has_sso @ admin @ compartmenta @ sso_compartmenta,
inference('s_sup-',[status(thm)],[zip_derived_cl47,zip_derived_cl6]) ).
thf(zip_derived_cl13_035,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] :
( ~ ( admin_file_has_level_h @ admin @ X0 @ X1 @ X2 )
| ( admin_file_has_level_h @ admin @ X0 @ X1 @ ( cons @ X3 @ X2 ) )
| ~ ( admin_compartment_has_sso @ admin @ X3 @ X4 )
| ~ ( sso_file_has_level @ X4 @ X0 @ X1 @ X5 )
| ~ ( admin_compartment_has_scg @ admin @ X3 @ X5 ) ),
inference(cnf,[status(esa)],[ax13]) ).
thf(zip_derived_cl124,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ~ ( admin_file_has_level_h @ admin @ X2 @ X1 @ X0 )
| ( admin_file_has_level_h @ admin @ X2 @ X1 @ ( cons @ compartmenta @ X0 ) )
| ~ ( sso_file_has_level @ sso_compartmenta @ X2 @ X1 @ X3 )
| ~ ( admin_compartment_has_scg @ admin @ compartmenta @ X3 ) ),
inference('s_sup-',[status(thm)],[zip_derived_cl93,zip_derived_cl13]) ).
thf(zip_derived_cl219,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ ( admin_file_has_level_h @ admin @ X2 @ X1 @ X0 )
| ( admin_file_has_level_h @ admin @ X2 @ X1 @ ( cons @ compartmenta @ X0 ) )
| ~ ( sso_file_has_level @ sso_compartmenta @ X2 @ X1 @ scg_compartmenta ) ),
inference('s_sup-',[status(thm)],[zip_derived_cl189,zip_derived_cl124]) ).
thf(zip_derived_cl226,plain,
! [X0: $i] :
( ~ ( admin_file_has_level_h @ admin @ secretfile @ secret @ X0 )
| ( admin_file_has_level_h @ admin @ secretfile @ secret @ ( cons @ compartmenta @ X0 ) ) ),
inference('s_sup-',[status(thm)],[zip_derived_cl56,zip_derived_cl219]) ).
thf(zip_derived_cl227,plain,
admin_file_has_level_h @ admin @ secretfile @ secret @ ( cons @ compartmenta @ nil ),
inference('s_sup-',[status(thm)],[zip_derived_cl12,zip_derived_cl226]) ).
thf(zip_derived_cl231,plain,
admin_file_has_level @ admin @ secretfile @ secret,
inference(demod,[status(thm)],[zip_derived_cl223,zip_derived_cl227]) ).
thf(ax35,axiom,
! [K: $i,F: $i,L: $i] :
( ( admin_file_has_level @ admin @ F @ L )
=> ( ( admin_indi_has_level @ admin @ K @ L )
=> ( admin_indi_has_level_for_file @ admin @ K @ F ) ) ) ).
thf(zip_derived_cl35,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( admin_indi_has_level_for_file @ admin @ X0 @ X1 )
| ~ ( admin_file_has_level @ admin @ X1 @ X2 )
| ~ ( admin_indi_has_level @ admin @ X0 @ X2 ) ),
inference(cnf,[status(esa)],[ax35]) ).
thf(zip_derived_cl234,plain,
! [X0: $i] :
( ( admin_indi_has_level_for_file @ admin @ X0 @ secretfile )
| ~ ( admin_indi_has_level @ admin @ X0 @ secret ) ),
inference('s_sup-',[status(thm)],[zip_derived_cl231,zip_derived_cl35]) ).
thf(zip_derived_cl337,plain,
admin_indi_has_level_for_file @ admin @ alice @ secretfile,
inference('s_sup-',[status(thm)],[zip_derived_cl335,zip_derived_cl234]) ).
thf(zip_derived_cl100_036,plain,
admin_indi_has_citizenship @ admin @ alice @ usa,
inference('s_sup-',[status(thm)],[zip_derived_cl71,zip_derived_cl23]) ).
thf(ax38,axiom,
! [K: $i,F: $i] :
( ( admin_indi_has_citizenship @ admin @ K @ usa )
=> ( admin_indi_has_citizenship_for_file @ admin @ K @ F ) ) ).
thf(zip_derived_cl38,plain,
! [X0: $i,X1: $i] :
( ~ ( admin_indi_has_citizenship @ admin @ X0 @ usa )
| ( admin_indi_has_citizenship_for_file @ admin @ X0 @ X1 ) ),
inference(cnf,[status(esa)],[ax38]) ).
thf(zip_derived_cl102,plain,
! [X0: $i] : ( admin_indi_has_citizenship_for_file @ admin @ alice @ X0 ),
inference('s_sup-',[status(thm)],[zip_derived_cl100,zip_derived_cl38]) ).
thf(ax39,axiom,
! [K: $i,F: $i] :
( ( 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 ) ) ) ) ) ) ).
thf(zip_derived_cl39,plain,
! [X0: $i,X1: $i] :
( ~ ( admin_indi_has_citizenship_for_file @ admin @ X0 @ X1 )
| ~ ( admin_indi_has_level_for_file @ admin @ X0 @ X1 )
| ( admin_indi_may_file @ admin @ X0 @ X1 @ read )
| ~ ( admin_indi_has_compartments_for_file @ admin @ X0 @ X1 )
| ~ ( admin_indi_has_need_to_know_for_file @ admin @ X0 @ X1 )
| ~ ( state_file_is_not_working_paper @ X1 ) ),
inference(cnf,[status(esa)],[ax39]) ).
thf(zip_derived_cl134,plain,
! [X0: $i] :
( ~ ( admin_indi_has_level_for_file @ admin @ alice @ X0 )
| ( admin_indi_may_file @ admin @ alice @ X0 @ read )
| ~ ( admin_indi_has_compartments_for_file @ admin @ alice @ X0 )
| ~ ( admin_indi_has_need_to_know_for_file @ admin @ alice @ X0 )
| ~ ( state_file_is_not_working_paper @ X0 ) ),
inference('s_sup-',[status(thm)],[zip_derived_cl102,zip_derived_cl39]) ).
thf(zip_derived_cl338,plain,
( ( admin_indi_may_file @ admin @ alice @ secretfile @ read )
| ~ ( admin_indi_has_compartments_for_file @ admin @ alice @ secretfile )
| ~ ( admin_indi_has_need_to_know_for_file @ admin @ alice @ secretfile )
| ~ ( state_file_is_not_working_paper @ secretfile ) ),
inference('s_sup-',[status(thm)],[zip_derived_cl337,zip_derived_cl134]) ).
thf(ax82,axiom,
owner_indi_has_need_to_know @ owner_secretfile @ alice @ secretfile ).
thf(zip_derived_cl82,plain,
owner_indi_has_need_to_know @ owner_secretfile @ alice @ secretfile,
inference(cnf,[status(esa)],[ax82]) ).
thf(ax36,axiom,
! [K: $i,F: $i,OWR: $i] :
( ( 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 ) ) ) ).
thf(zip_derived_cl36,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( admin_indi_has_need_to_know_for_file @ admin @ X0 @ X1 )
| ~ ( state_file_has_owner @ X1 @ X2 )
| ~ ( owner_indi_has_need_to_know @ X2 @ X0 @ X1 ) ),
inference(cnf,[status(esa)],[ax36]) ).
thf(zip_derived_cl106,plain,
( ( admin_indi_has_need_to_know_for_file @ admin @ alice @ secretfile )
| ~ ( state_file_has_owner @ secretfile @ owner_secretfile ) ),
inference('s_sup-',[status(thm)],[zip_derived_cl82,zip_derived_cl36]) ).
thf(ax60,axiom,
state_file_has_owner @ secretfile @ owner_secretfile ).
thf(zip_derived_cl60,plain,
state_file_has_owner @ secretfile @ owner_secretfile,
inference(cnf,[status(esa)],[ax60]) ).
thf(zip_derived_cl109,plain,
admin_indi_has_need_to_know_for_file @ admin @ alice @ secretfile,
inference(demod,[status(thm)],[zip_derived_cl106,zip_derived_cl60]) ).
thf(ax50,axiom,
state_file_is_not_working_paper @ secretfile ).
thf(zip_derived_cl50,plain,
state_file_is_not_working_paper @ secretfile,
inference(cnf,[status(esa)],[ax50]) ).
thf(zip_derived_cl339,plain,
( ( admin_indi_may_file @ admin @ alice @ secretfile @ read )
| ~ ( admin_indi_has_compartments_for_file @ admin @ alice @ secretfile ) ),
inference(demod,[status(thm)],[zip_derived_cl338,zip_derived_cl109,zip_derived_cl50]) ).
thf(alicereadsecret,conjecture,
admin_indi_may_file @ admin @ alice @ secretfile @ read ).
thf(zf_stmt_0,negated_conjecture,
~ ( admin_indi_may_file @ admin @ alice @ secretfile @ read ),
inference('cnf.neg',[status(esa)],[alicereadsecret]) ).
thf(zip_derived_cl87,plain,
~ ( admin_indi_may_file @ admin @ alice @ secretfile @ read ),
inference(cnf,[status(esa)],[zf_stmt_0]) ).
thf(zip_derived_cl340,plain,
~ ( admin_indi_has_compartments_for_file @ admin @ alice @ secretfile ),
inference(clc,[status(thm)],[zip_derived_cl339,zip_derived_cl87]) ).
thf(zip_derived_cl341,plain,
! [X0: $i] :
( ~ ( admin_indi_has_compartments @ admin @ alice @ ( cons @ compartmenta @ nil ) )
| ~ ( sso_indi_has_compartment @ X0 @ alice @ compartmentb )
| ~ ( admin_compartment_has_sso @ admin @ compartmentb @ X0 ) ),
inference(demod,[status(thm)],[zip_derived_cl316,zip_derived_cl340]) ).
thf(ax26,axiom,
! [K: $i] : ( admin_indi_has_compartments @ admin @ K @ nil ) ).
thf(zip_derived_cl26,plain,
! [X0: $i] : ( admin_indi_has_compartments @ admin @ X0 @ nil ),
inference(cnf,[status(esa)],[ax26]) ).
thf(ax81,axiom,
sso_indi_has_compartment @ sso_compartmenta @ alice @ compartmenta ).
thf(zip_derived_cl81,plain,
sso_indi_has_compartment @ sso_compartmenta @ alice @ compartmenta,
inference(cnf,[status(esa)],[ax81]) ).
thf(ax43,axiom,
oca_compartment_is_compartment @ oca @ compartmenta @ sbu @ unclassified @ no @ no ).
thf(zip_derived_cl43,plain,
oca_compartment_is_compartment @ oca @ compartmenta @ sbu @ unclassified @ no @ no,
inference(cnf,[status(esa)],[ax43]) ).
thf(zip_derived_cl41_037,plain,
system_indi_is_oca @ system @ oca,
inference(cnf,[status(esa)],[ax41]) ).
thf(ax31,axiom,
! [K: $i,C: $i,OCA: $i,L1: $i,L2: $i,B1: $i] :
( ( 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 ) ) ) ).
thf(zip_derived_cl31,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] :
( ( admin_indi_has_polygraph_for_compartment @ admin @ X0 @ X1 )
| ~ ( system_indi_is_oca @ system @ X2 )
| ~ ( oca_compartment_is_compartment @ X2 @ X1 @ X3 @ X4 @ X5 @ no ) ),
inference(cnf,[status(esa)],[ax31]) ).
thf(zip_derived_cl116,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( ( admin_indi_has_polygraph_for_compartment @ admin @ X1 @ X0 )
| ~ ( oca_compartment_is_compartment @ oca @ X0 @ X4 @ X3 @ X2 @ no ) ),
inference('s_sup-',[status(thm)],[zip_derived_cl41,zip_derived_cl31]) ).
thf(zip_derived_cl176,plain,
! [X0: $i] : ( admin_indi_has_polygraph_for_compartment @ admin @ X0 @ compartmenta ),
inference('s_sup-',[status(thm)],[zip_derived_cl43,zip_derived_cl116]) ).
thf(zip_derived_cl138_038,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ ( admin_indi_has_polygraph_for_compartment @ admin @ alice @ X0 )
| ~ ( admin_indi_has_background_for_compartment @ admin @ alice @ X0 )
| ~ ( admin_indi_has_compartments @ admin @ alice @ X1 )
| ( admin_indi_has_compartments @ admin @ alice @ ( cons @ X0 @ X1 ) )
| ~ ( admin_indi_has_level_for_compartment @ admin @ alice @ X0 )
| ~ ( admin_indi_has_credit_for_compartment @ admin @ alice @ X0 )
| ~ ( system_indi_needs_compartment @ system @ alice @ X0 )
| ~ ( sso_indi_has_compartment @ X2 @ alice @ X0 )
| ~ ( admin_compartment_has_sso @ admin @ X0 @ X2 ) ),
inference(demod,[status(thm)],[zip_derived_cl137,zip_derived_cl100]) ).
thf(zip_derived_cl311,plain,
! [X0: $i,X1: $i] :
( ~ ( admin_indi_has_background_for_compartment @ admin @ alice @ compartmenta )
| ~ ( admin_indi_has_compartments @ admin @ alice @ X0 )
| ( admin_indi_has_compartments @ admin @ alice @ ( cons @ compartmenta @ X0 ) )
| ~ ( admin_indi_has_level_for_compartment @ admin @ alice @ compartmenta )
| ~ ( admin_indi_has_credit_for_compartment @ admin @ alice @ compartmenta )
| ~ ( system_indi_needs_compartment @ system @ alice @ compartmenta )
| ~ ( sso_indi_has_compartment @ X1 @ alice @ compartmenta )
| ~ ( admin_compartment_has_sso @ admin @ compartmenta @ X1 ) ),
inference('s_sup-',[status(thm)],[zip_derived_cl176,zip_derived_cl138]) ).
thf(zip_derived_cl43_039,plain,
oca_compartment_is_compartment @ oca @ compartmenta @ sbu @ unclassified @ no @ no,
inference(cnf,[status(esa)],[ax43]) ).
thf(ax19,axiom,
! [K: $i] : ( admin_indi_has_background @ admin @ K @ unclassified ) ).
thf(zip_derived_cl19,plain,
! [X0: $i] : ( admin_indi_has_background @ admin @ X0 @ unclassified ),
inference(cnf,[status(esa)],[ax19]) ).
thf(zip_derived_cl129_040,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] :
( ( admin_indi_has_background_for_compartment @ admin @ X1 @ X0 )
| ~ ( admin_indi_has_background @ admin @ X1 @ X2 )
| ~ ( oca_compartment_is_compartment @ oca @ X0 @ X5 @ X2 @ X4 @ X3 ) ),
inference('s_sup-',[status(thm)],[zip_derived_cl41,zip_derived_cl28]) ).
thf(zip_derived_cl197,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( ( admin_indi_has_background_for_compartment @ admin @ X0 @ X1 )
| ~ ( oca_compartment_is_compartment @ oca @ X1 @ X4 @ unclassified @ X3 @ X2 ) ),
inference('s_sup-',[status(thm)],[zip_derived_cl19,zip_derived_cl129]) ).
thf(zip_derived_cl202,plain,
! [X0: $i] : ( admin_indi_has_background_for_compartment @ admin @ X0 @ compartmenta ),
inference('s_sup-',[status(thm)],[zip_derived_cl43,zip_derived_cl197]) ).
thf(zip_derived_cl43_041,plain,
oca_compartment_is_compartment @ oca @ compartmenta @ sbu @ unclassified @ no @ no,
inference(cnf,[status(esa)],[ax43]) ).
thf(zip_derived_cl4_042,plain,
! [X0: $i,X1: $i] : ( loca_level_below @ X0 @ X1 @ X1 ),
inference(cnf,[status(esa)],[ax4]) ).
thf(ax1,axiom,
! [K: $i] : ( loca_level_direct_below @ K @ sbu @ confidential ) ).
thf(zip_derived_cl1,plain,
! [X0: $i] : ( loca_level_direct_below @ X0 @ sbu @ confidential ),
inference(cnf,[status(esa)],[ax1]) ).
thf(zip_derived_cl5_043,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ~ ( loca_level_below @ X0 @ X1 @ X2 )
| ~ ( loca_level_direct_below @ X0 @ X2 @ X3 )
| ( loca_level_below @ X0 @ X1 @ X3 ) ),
inference(cnf,[status(esa)],[ax5]) ).
thf(zip_derived_cl89,plain,
! [X0: $i,X1: $i] :
( ~ ( loca_level_below @ X0 @ X1 @ sbu )
| ( loca_level_below @ X0 @ X1 @ confidential ) ),
inference('s_sup-',[status(thm)],[zip_derived_cl1,zip_derived_cl5]) ).
thf(zip_derived_cl139,plain,
! [X0: $i] : ( loca_level_below @ X0 @ sbu @ confidential ),
inference('s_sup-',[status(thm)],[zip_derived_cl4,zip_derived_cl89]) ).
thf(zip_derived_cl90_044,plain,
! [X0: $i,X1: $i] :
( ~ ( loca_level_below @ X0 @ X1 @ confidential )
| ( loca_level_below @ X0 @ X1 @ secret ) ),
inference('s_sup-',[status(thm)],[zip_derived_cl2,zip_derived_cl5]) ).
thf(zip_derived_cl143,plain,
! [X0: $i] : ( loca_level_below @ X0 @ sbu @ secret ),
inference('s_sup-',[status(thm)],[zip_derived_cl139,zip_derived_cl90]) ).
thf(zip_derived_cl91_045,plain,
! [X0: $i,X1: $i] :
( ~ ( loca_level_below @ X0 @ X1 @ secret )
| ( loca_level_below @ X0 @ X1 @ topsecret ) ),
inference('s_sup-',[status(thm)],[zip_derived_cl3,zip_derived_cl5]) ).
thf(zip_derived_cl147,plain,
! [X0: $i] : ( loca_level_below @ X0 @ sbu @ topsecret ),
inference('s_sup-',[status(thm)],[zip_derived_cl143,zip_derived_cl91]) ).
thf(zip_derived_cl143_046,plain,
! [X0: $i] : ( loca_level_below @ X0 @ sbu @ secret ),
inference('s_sup-',[status(thm)],[zip_derived_cl139,zip_derived_cl90]) ).
thf(zip_derived_cl274_047,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ ( loca_level_below @ admin @ X1 @ X0 )
| ~ ( admin_indi_has_background @ admin @ alice @ X1 )
| ( admin_indi_has_level @ admin @ alice @ X1 )
| ~ ( system_indi_needs_level @ system @ alice @ X0 )
| ~ ( loca_level_below @ admin @ X1 @ X2 )
| ~ ( level_admin_indi_has_level @ level_admin @ alice @ X2 ) ),
inference('s_sup-',[status(thm)],[zip_derived_cl70,zip_derived_cl136]) ).
thf(zip_derived_cl283,plain,
! [X0: $i] :
( ~ ( admin_indi_has_background @ admin @ alice @ sbu )
| ( admin_indi_has_level @ admin @ alice @ sbu )
| ~ ( system_indi_needs_level @ system @ alice @ secret )
| ~ ( loca_level_below @ admin @ sbu @ X0 )
| ~ ( level_admin_indi_has_level @ level_admin @ alice @ X0 ) ),
inference('s_sup-',[status(thm)],[zip_derived_cl143,zip_derived_cl274]) ).
thf(zip_derived_cl74_048,plain,
background_admin_indi_has_background @ background_admin @ alice @ topsecret,
inference(cnf,[status(esa)],[ax74]) ).
thf(zip_derived_cl147_049,plain,
! [X0: $i] : ( loca_level_below @ X0 @ sbu @ topsecret ),
inference('s_sup-',[status(thm)],[zip_derived_cl143,zip_derived_cl91]) ).
thf(zip_derived_cl119_050,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( admin_indi_has_background @ admin @ X1 @ X0 )
| ~ ( loca_level_below @ admin @ X0 @ X2 )
| ~ ( background_admin_indi_has_background @ background_admin @ X1 @ X2 ) ),
inference('s_sup-',[status(thm)],[zip_derived_cl68,zip_derived_cl20]) ).
thf(zip_derived_cl155,plain,
! [X0: $i] :
( ( admin_indi_has_background @ admin @ X0 @ sbu )
| ~ ( background_admin_indi_has_background @ background_admin @ X0 @ topsecret ) ),
inference('s_sup-',[status(thm)],[zip_derived_cl147,zip_derived_cl119]) ).
thf(zip_derived_cl166,plain,
admin_indi_has_background @ admin @ alice @ sbu,
inference('s_sup-',[status(thm)],[zip_derived_cl74,zip_derived_cl155]) ).
thf(zip_derived_cl76_051,plain,
system_indi_needs_level @ system @ alice @ secret,
inference(cnf,[status(esa)],[ax76]) ).
thf(zip_derived_cl293,plain,
! [X0: $i] :
( ( admin_indi_has_level @ admin @ alice @ sbu )
| ~ ( loca_level_below @ admin @ sbu @ X0 )
| ~ ( level_admin_indi_has_level @ level_admin @ alice @ X0 ) ),
inference(demod,[status(thm)],[zip_derived_cl283,zip_derived_cl166,zip_derived_cl76]) ).
thf(zip_derived_cl301,plain,
( ( admin_indi_has_level @ admin @ alice @ sbu )
| ~ ( level_admin_indi_has_level @ level_admin @ alice @ topsecret ) ),
inference('s_sup-',[status(thm)],[zip_derived_cl147,zip_derived_cl293]) ).
thf(zip_derived_cl77_052,plain,
level_admin_indi_has_level @ level_admin @ alice @ topsecret,
inference(cnf,[status(esa)],[ax77]) ).
thf(zip_derived_cl302,plain,
admin_indi_has_level @ admin @ alice @ sbu,
inference(demod,[status(thm)],[zip_derived_cl301,zip_derived_cl77]) ).
thf(zip_derived_cl133_053,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] :
( ( admin_indi_has_level_for_compartment @ admin @ X1 @ X0 )
| ~ ( admin_indi_has_level @ admin @ X1 @ X2 )
| ~ ( oca_compartment_is_compartment @ oca @ X0 @ X2 @ X5 @ X4 @ X3 ) ),
inference('s_sup-',[status(thm)],[zip_derived_cl41,zip_derived_cl29]) ).
thf(zip_derived_cl303,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ( admin_indi_has_level_for_compartment @ admin @ alice @ X0 )
| ~ ( oca_compartment_is_compartment @ oca @ X0 @ sbu @ X3 @ X2 @ X1 ) ),
inference('s_sup-',[status(thm)],[zip_derived_cl302,zip_derived_cl133]) ).
thf(zip_derived_cl304,plain,
admin_indi_has_level_for_compartment @ admin @ alice @ compartmenta,
inference('s_sup-',[status(thm)],[zip_derived_cl43,zip_derived_cl303]) ).
thf(zip_derived_cl43_054,plain,
oca_compartment_is_compartment @ oca @ compartmenta @ sbu @ unclassified @ no @ no,
inference(cnf,[status(esa)],[ax43]) ).
thf(zip_derived_cl41_055,plain,
system_indi_is_oca @ system @ oca,
inference(cnf,[status(esa)],[ax41]) ).
thf(ax33,axiom,
! [K: $i,C: $i,OCA: $i,L1: $i,L2: $i,B2: $i] :
( ( 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 ) ) ) ).
thf(zip_derived_cl33,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] :
( ( admin_indi_has_credit_for_compartment @ admin @ X0 @ X1 )
| ~ ( system_indi_is_oca @ system @ X2 )
| ~ ( oca_compartment_is_compartment @ X2 @ X1 @ X3 @ X4 @ no @ X5 ) ),
inference(cnf,[status(esa)],[ax33]) ).
thf(zip_derived_cl117,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( ( admin_indi_has_credit_for_compartment @ admin @ X1 @ X0 )
| ~ ( oca_compartment_is_compartment @ oca @ X0 @ X4 @ X3 @ no @ X2 ) ),
inference('s_sup-',[status(thm)],[zip_derived_cl41,zip_derived_cl33]) ).
thf(zip_derived_cl177,plain,
! [X0: $i] : ( admin_indi_has_credit_for_compartment @ admin @ X0 @ compartmenta ),
inference('s_sup-',[status(thm)],[zip_derived_cl43,zip_derived_cl117]) ).
thf(ax79,axiom,
system_indi_needs_compartment @ system @ alice @ compartmenta ).
thf(zip_derived_cl79,plain,
system_indi_needs_compartment @ system @ alice @ compartmenta,
inference(cnf,[status(esa)],[ax79]) ).
thf(zip_derived_cl314,plain,
! [X0: $i,X1: $i] :
( ~ ( admin_indi_has_compartments @ admin @ alice @ X0 )
| ( admin_indi_has_compartments @ admin @ alice @ ( cons @ compartmenta @ X0 ) )
| ~ ( sso_indi_has_compartment @ X1 @ alice @ compartmenta )
| ~ ( admin_compartment_has_sso @ admin @ compartmenta @ X1 ) ),
inference(demod,[status(thm)],[zip_derived_cl311,zip_derived_cl202,zip_derived_cl304,zip_derived_cl177,zip_derived_cl79]) ).
thf(zip_derived_cl354,plain,
! [X0: $i] :
( ~ ( admin_indi_has_compartments @ admin @ alice @ X0 )
| ( admin_indi_has_compartments @ admin @ alice @ ( cons @ compartmenta @ X0 ) )
| ~ ( admin_compartment_has_sso @ admin @ compartmenta @ sso_compartmenta ) ),
inference('s_sup-',[status(thm)],[zip_derived_cl81,zip_derived_cl314]) ).
thf(zip_derived_cl93_056,plain,
admin_compartment_has_sso @ admin @ compartmenta @ sso_compartmenta,
inference('s_sup-',[status(thm)],[zip_derived_cl47,zip_derived_cl6]) ).
thf(zip_derived_cl355,plain,
! [X0: $i] :
( ~ ( admin_indi_has_compartments @ admin @ alice @ X0 )
| ( admin_indi_has_compartments @ admin @ alice @ ( cons @ compartmenta @ X0 ) ) ),
inference(demod,[status(thm)],[zip_derived_cl354,zip_derived_cl93]) ).
thf(zip_derived_cl356,plain,
admin_indi_has_compartments @ admin @ alice @ ( cons @ compartmenta @ nil ),
inference('s_sup-',[status(thm)],[zip_derived_cl26,zip_derived_cl355]) ).
thf(zip_derived_cl357,plain,
! [X0: $i] :
( ~ ( sso_indi_has_compartment @ X0 @ alice @ compartmentb )
| ~ ( admin_compartment_has_sso @ admin @ compartmentb @ X0 ) ),
inference(demod,[status(thm)],[zip_derived_cl341,zip_derived_cl356]) ).
thf(zip_derived_cl359,plain,
~ ( admin_compartment_has_sso @ admin @ compartmentb @ sso_compartmentb ),
inference('s_sup-',[status(thm)],[zip_derived_cl80,zip_derived_cl357]) ).
thf(zip_derived_cl92_057,plain,
admin_compartment_has_sso @ admin @ compartmentb @ sso_compartmentb,
inference('s_sup-',[status(thm)],[zip_derived_cl44,zip_derived_cl6]) ).
thf(zip_derived_cl360,plain,
$false,
inference(demod,[status(thm)],[zip_derived_cl359,zip_derived_cl92]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.08 % Problem : SWV437+1 : TPTP v9.2.0. Released v4.0.0.
% 0.00/0.09 % Command : python3 /export/starexec/sandbox/solver/bin/portfolio.lams.parallel.py %s %d /export/starexec/sandbox/tmp/tmp.Y8e3rdMWL0 true
% 0.08/0.28 % Computer : n010.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 Oct 1 12:50:08 EDT 2025
% 0.08/0.28 % CPUTime :
% 0.08/0.28 % Running portfolio for 300 s
% 0.08/0.28 % File : /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.08/0.29 % Number of cores: 8
% 0.08/0.29 % Python version: Python 3.6.8
% 0.08/0.29 % Running in FO mode
% 0.13/0.54 % Total configuration time : 435
% 0.13/0.54 % Estimated wc time : 1092
% 0.13/0.54 % Estimated cpu time (7 cpus) : 156.0
% 1.02/0.64 % /export/starexec/sandbox/solver/bin/fo/fo6_bce.sh running for 75s
% 1.02/0.65 % /export/starexec/sandbox/solver/bin/fo/fo7.sh running for 63s
% 1.02/0.65 % /export/starexec/sandbox/solver/bin/fo/fo3_bce.sh running for 75s
% 1.02/0.65 % /export/starexec/sandbox/solver/bin/fo/fo1_av.sh running for 75s
% 1.02/0.66 % /export/starexec/sandbox/solver/bin/fo/fo13.sh running for 50s
% 1.02/0.66 % /export/starexec/sandbox/solver/bin/fo/fo5.sh running for 50s
% 1.02/0.66 % /export/starexec/sandbox/solver/bin/fo/fo4.sh running for 50s
% 1.02/0.69 % /export/starexec/sandbox/solver/bin/fo/fo1_lcnf.sh running for 50s
% 1.02/0.70 % /export/starexec/sandbox/solver/bin/fo/fo17_bce.sh running for 50s
% 1.02/0.70 % /export/starexec/sandbox/solver/bin/fo/fo8.sh running for 50s
% 1.27/0.92 % Solved by fo/fo13.sh.
% 1.27/0.92 % done 252 iterations in 0.212s
% 1.27/0.92 % SZS status Theorem for '/export/starexec/sandbox/benchmark/theBenchmark.p'
% 1.27/0.92 % SZS output start Refutation
% See solution above
% 1.27/0.92
% 1.27/0.92
% 1.27/0.92 % Terminating...
% 1.53/0.97 % Runner terminated.
% 1.53/0.98 % Zipperpin 1.5 exiting
%------------------------------------------------------------------------------