%------------------------------------------------------------------------------ % File : cocATP---0.2.0 % Problem : SWV438^1 : TPTP v6.1.0. Bugfixed v4.0.1. % Transfm : none % Format : tptp:raw % Command : python CASC.py /export/starexec/sandbox/benchmark/theBenchmark.p % Computer : n094.star.cs.uiowa.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2609 0 2.40GHz % Memory : 32286.75MB % OS : Linux 2.6.32-431.20.3.el6.x86_64 % CPULimit : 300s % DateTime : Thu Jul 17 13:35:59 EDT 2014 % Result : Timeout 300.04s % Output : None % Verified : % SZS Type : None (Parsing solution fails) % Syntax : Number of formulae : 0 % Comments : %------------------------------------------------------------------------------ %----NO SOLUTION OUTPUT BY SYSTEM %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % % Problem : SWV438^1 : TPTP v6.1.0. Bugfixed v4.0.1. % % Command : python CASC.py /export/starexec/sandbox/benchmark/theBenchmark.p % % Computer : n094.star.cs.uiowa.edu % % Model : x86_64 x86_64 % % CPU : Intel(R) Xeon(R) CPU E5-2609 0 @ 2.40GHz % % Memory : 32286.75MB % % OS : Linux 2.6.32-431.20.3.el6.x86_64 % % CPULimit : 300 % % DateTime : Thu Jul 17 09:56:21 CDT 2014 % % CPUTime : 300.04 % Python 2.7.5 % Using paths ['/home/cristobal/cocATP/CASC/TPTP/', '/export/starexec/sandbox/benchmark/', '/export/starexec/sandbox/benchmark/'] % Failed to open /home/cristobal/cocATP/CASC/TPTP/Axioms/LCL008^0.ax, trying next directory % FOF formula (<kernel.Constant object at 0x1460d88>, <kernel.Constant object at 0x14603b0>) of role type named current_world % Using role type % Declaring current_world:fofType % FOF formula (<kernel.Constant object at 0x14603b0>, <kernel.DependentProduct object at 0x1084dd0>) of role type named prop_a % Using role type % Declaring prop_a:(fofType->Prop) % FOF formula (<kernel.Constant object at 0x1460320>, <kernel.DependentProduct object at 0x1084c20>) of role type named prop_b % Using role type % Declaring prop_b:(fofType->Prop) % FOF formula (<kernel.Constant object at 0x1460320>, <kernel.DependentProduct object at 0x1084cb0>) of role type named prop_c % Using role type % Declaring prop_c:(fofType->Prop) % FOF formula (<kernel.Constant object at 0x1084cb0>, <kernel.DependentProduct object at 0x10847a0>) of role type named mfalse_decl % Using role type % Declaring mfalse:(fofType->Prop) % FOF formula (((eq (fofType->Prop)) mfalse) (fun (X:fofType)=> False)) of role definition named mfalse % A new definition: (((eq (fofType->Prop)) mfalse) (fun (X:fofType)=> False)) % Defined: mfalse:=(fun (X:fofType)=> False) % FOF formula (<kernel.Constant object at 0x10848c0>, <kernel.DependentProduct object at 0x10847a0>) of role type named mtrue_decl % Using role type % Declaring mtrue:(fofType->Prop) % FOF formula (((eq (fofType->Prop)) mtrue) (fun (X:fofType)=> True)) of role definition named mtrue % A new definition: (((eq (fofType->Prop)) mtrue) (fun (X:fofType)=> True)) % Defined: mtrue:=(fun (X:fofType)=> True) % FOF formula (<kernel.Constant object at 0x1084f80>, <kernel.DependentProduct object at 0x1084a28>) of role type named mnot_decl % Using role type % Declaring mnot:((fofType->Prop)->(fofType->Prop)) % FOF formula (((eq ((fofType->Prop)->(fofType->Prop))) mnot) (fun (X:(fofType->Prop)) (U:fofType)=> ((X U)->False))) of role definition named mnot % A new definition: (((eq ((fofType->Prop)->(fofType->Prop))) mnot) (fun (X:(fofType->Prop)) (U:fofType)=> ((X U)->False))) % Defined: mnot:=(fun (X:(fofType->Prop)) (U:fofType)=> ((X U)->False)) % FOF formula (<kernel.Constant object at 0x10848c0>, <kernel.DependentProduct object at 0x1084488>) of role type named mor_decl % Using role type % Declaring mor:((fofType->Prop)->((fofType->Prop)->(fofType->Prop))) % FOF formula (((eq ((fofType->Prop)->((fofType->Prop)->(fofType->Prop)))) mor) (fun (X:(fofType->Prop)) (Y:(fofType->Prop)) (U:fofType)=> ((or (X U)) (Y U)))) of role definition named mor % A new definition: (((eq ((fofType->Prop)->((fofType->Prop)->(fofType->Prop)))) mor) (fun (X:(fofType->Prop)) (Y:(fofType->Prop)) (U:fofType)=> ((or (X U)) (Y U)))) % Defined: mor:=(fun (X:(fofType->Prop)) (Y:(fofType->Prop)) (U:fofType)=> ((or (X U)) (Y U))) % FOF formula (<kernel.Constant object at 0x14be200>, <kernel.DependentProduct object at 0x1084fc8>) of role type named mand_decl % Using role type % Declaring mand:((fofType->Prop)->((fofType->Prop)->(fofType->Prop))) % FOF formula (((eq ((fofType->Prop)->((fofType->Prop)->(fofType->Prop)))) mand) (fun (X:(fofType->Prop)) (Y:(fofType->Prop)) (U:fofType)=> ((and (X U)) (Y U)))) of role definition named mand % A new definition: (((eq ((fofType->Prop)->((fofType->Prop)->(fofType->Prop)))) mand) (fun (X:(fofType->Prop)) (Y:(fofType->Prop)) (U:fofType)=> ((and (X U)) (Y U)))) % Defined: mand:=(fun (X:(fofType->Prop)) (Y:(fofType->Prop)) (U:fofType)=> ((and (X U)) (Y U))) % FOF formula (<kernel.Constant object at 0x10847e8>, <kernel.DependentProduct object at 0x1084d40>) of role type named mimpl_decl % Using role type % Declaring mimpl:((fofType->Prop)->((fofType->Prop)->(fofType->Prop))) % FOF formula (((eq ((fofType->Prop)->((fofType->Prop)->(fofType->Prop)))) mimpl) (fun (U:(fofType->Prop)) (V:(fofType->Prop))=> ((mor (mnot U)) V))) of role definition named mimpl % A new definition: (((eq ((fofType->Prop)->((fofType->Prop)->(fofType->Prop)))) mimpl) (fun (U:(fofType->Prop)) (V:(fofType->Prop))=> ((mor (mnot U)) V))) % Defined: mimpl:=(fun (U:(fofType->Prop)) (V:(fofType->Prop))=> ((mor (mnot U)) V)) % FOF formula (<kernel.Constant object at 0x1084fc8>, <kernel.DependentProduct object at 0x1084f80>) of role type named miff_decl % Using role type % Declaring miff:((fofType->Prop)->((fofType->Prop)->(fofType->Prop))) % FOF formula (((eq ((fofType->Prop)->((fofType->Prop)->(fofType->Prop)))) miff) (fun (U:(fofType->Prop)) (V:(fofType->Prop))=> ((mand ((mimpl U) V)) ((mimpl V) U)))) of role definition named miff % A new definition: (((eq ((fofType->Prop)->((fofType->Prop)->(fofType->Prop)))) miff) (fun (U:(fofType->Prop)) (V:(fofType->Prop))=> ((mand ((mimpl U) V)) ((mimpl V) U)))) % Defined: miff:=(fun (U:(fofType->Prop)) (V:(fofType->Prop))=> ((mand ((mimpl U) V)) ((mimpl V) U))) % FOF formula (<kernel.Constant object at 0x10847e8>, <kernel.DependentProduct object at 0x1084908>) of role type named mbox_decl % Using role type % Declaring mbox:((fofType->(fofType->Prop))->((fofType->Prop)->(fofType->Prop))) % FOF formula (((eq ((fofType->(fofType->Prop))->((fofType->Prop)->(fofType->Prop)))) mbox) (fun (R:(fofType->(fofType->Prop))) (P:(fofType->Prop)) (X:fofType)=> (forall (Y:fofType), (((R X) Y)->(P Y))))) of role definition named mbox % A new definition: (((eq ((fofType->(fofType->Prop))->((fofType->Prop)->(fofType->Prop)))) mbox) (fun (R:(fofType->(fofType->Prop))) (P:(fofType->Prop)) (X:fofType)=> (forall (Y:fofType), (((R X) Y)->(P Y))))) % Defined: mbox:=(fun (R:(fofType->(fofType->Prop))) (P:(fofType->Prop)) (X:fofType)=> (forall (Y:fofType), (((R X) Y)->(P Y)))) % FOF formula (<kernel.Constant object at 0x1084fc8>, <kernel.DependentProduct object at 0x107a710>) of role type named mdia_decl % Using role type % Declaring mdia:((fofType->(fofType->Prop))->((fofType->Prop)->(fofType->Prop))) % FOF formula (((eq ((fofType->(fofType->Prop))->((fofType->Prop)->(fofType->Prop)))) mdia) (fun (R:(fofType->(fofType->Prop))) (P:(fofType->Prop)) (X:fofType)=> ((ex fofType) (fun (Y:fofType)=> ((and ((R X) Y)) (P Y)))))) of role definition named mdia % A new definition: (((eq ((fofType->(fofType->Prop))->((fofType->Prop)->(fofType->Prop)))) mdia) (fun (R:(fofType->(fofType->Prop))) (P:(fofType->Prop)) (X:fofType)=> ((ex fofType) (fun (Y:fofType)=> ((and ((R X) Y)) (P Y)))))) % Defined: mdia:=(fun (R:(fofType->(fofType->Prop))) (P:(fofType->Prop)) (X:fofType)=> ((ex fofType) (fun (Y:fofType)=> ((and ((R X) Y)) (P Y))))) % FOF formula (<kernel.Constant object at 0x107a2d8>, <kernel.Type object at 0x107a950>) of role type named individuals_decl % Using role type % Declaring individuals:Type % FOF formula (<kernel.Constant object at 0x107a5a8>, <kernel.DependentProduct object at 0x107a290>) of role type named mall_decl % Using role type % Declaring mall:((individuals->(fofType->Prop))->(fofType->Prop)) % FOF formula (((eq ((individuals->(fofType->Prop))->(fofType->Prop))) mall) (fun (P:(individuals->(fofType->Prop))) (W:fofType)=> (forall (X:individuals), ((P X) W)))) of role definition named mall % A new definition: (((eq ((individuals->(fofType->Prop))->(fofType->Prop))) mall) (fun (P:(individuals->(fofType->Prop))) (W:fofType)=> (forall (X:individuals), ((P X) W)))) % Defined: mall:=(fun (P:(individuals->(fofType->Prop))) (W:fofType)=> (forall (X:individuals), ((P X) W))) % FOF formula (<kernel.Constant object at 0x107a6c8>, <kernel.DependentProduct object at 0x107a710>) of role type named mexists_decl % Using role type % Declaring mexists:((individuals->(fofType->Prop))->(fofType->Prop)) % FOF formula (((eq ((individuals->(fofType->Prop))->(fofType->Prop))) mexists) (fun (P:(individuals->(fofType->Prop))) (W:fofType)=> ((ex individuals) (fun (X:individuals)=> ((P X) W))))) of role definition named mexists % A new definition: (((eq ((individuals->(fofType->Prop))->(fofType->Prop))) mexists) (fun (P:(individuals->(fofType->Prop))) (W:fofType)=> ((ex individuals) (fun (X:individuals)=> ((P X) W))))) % Defined: mexists:=(fun (P:(individuals->(fofType->Prop))) (W:fofType)=> ((ex individuals) (fun (X:individuals)=> ((P X) W)))) % FOF formula (<kernel.Constant object at 0x107a5a8>, <kernel.DependentProduct object at 0x107a5f0>) of role type named mvalid_decl % Using role type % Declaring mvalid:((fofType->Prop)->Prop) % FOF formula (((eq ((fofType->Prop)->Prop)) mvalid) (fun (P:(fofType->Prop))=> (forall (W:fofType), (P W)))) of role definition named mvalid % A new definition: (((eq ((fofType->Prop)->Prop)) mvalid) (fun (P:(fofType->Prop))=> (forall (W:fofType), (P W)))) % Defined: mvalid:=(fun (P:(fofType->Prop))=> (forall (W:fofType), (P W))) % FOF formula (<kernel.Constant object at 0x107a6c8>, <kernel.DependentProduct object at 0x107a0e0>) of role type named msatisfiable_decl % Using role type % Declaring msatisfiable:((fofType->Prop)->Prop) % FOF formula (((eq ((fofType->Prop)->Prop)) msatisfiable) (fun (P:(fofType->Prop))=> ((ex fofType) (fun (W:fofType)=> (P W))))) of role definition named msatisfiable % A new definition: (((eq ((fofType->Prop)->Prop)) msatisfiable) (fun (P:(fofType->Prop))=> ((ex fofType) (fun (W:fofType)=> (P W))))) % Defined: msatisfiable:=(fun (P:(fofType->Prop))=> ((ex fofType) (fun (W:fofType)=> (P W)))) % FOF formula (<kernel.Constant object at 0x107a5a8>, <kernel.DependentProduct object at 0x107a680>) of role type named mcountersatisfiable_decl % Using role type % Declaring mcountersatisfiable:((fofType->Prop)->Prop) % FOF formula (((eq ((fofType->Prop)->Prop)) mcountersatisfiable) (fun (P:(fofType->Prop))=> ((ex fofType) (fun (W:fofType)=> ((P W)->False))))) of role definition named mcountersatisfiable % A new definition: (((eq ((fofType->Prop)->Prop)) mcountersatisfiable) (fun (P:(fofType->Prop))=> ((ex fofType) (fun (W:fofType)=> ((P W)->False))))) % Defined: mcountersatisfiable:=(fun (P:(fofType->Prop))=> ((ex fofType) (fun (W:fofType)=> ((P W)->False)))) % FOF formula (<kernel.Constant object at 0x107a6c8>, <kernel.DependentProduct object at 0x107ab48>) of role type named minvalid_decl % Using role type % Declaring minvalid:((fofType->Prop)->Prop) % FOF formula (((eq ((fofType->Prop)->Prop)) minvalid) (fun (P:(fofType->Prop))=> (forall (W:fofType), ((P W)->False)))) of role definition named minvalid % A new definition: (((eq ((fofType->Prop)->Prop)) minvalid) (fun (P:(fofType->Prop))=> (forall (W:fofType), ((P W)->False)))) % Defined: minvalid:=(fun (P:(fofType->Prop))=> (forall (W:fofType), ((P W)->False))) % Failed to open /home/cristobal/cocATP/CASC/TPTP/Axioms/LCL009^0.ax, trying next directory % FOF formula (<kernel.Constant object at 0x1460320>, <kernel.DependentProduct object at 0x14be248>) of role type named reli % Using role type % Declaring reli:(fofType->(fofType->Prop)) % FOF formula (<kernel.Constant object at 0x1460320>, <kernel.DependentProduct object at 0x14be200>) of role type named relr % Using role type % Declaring relr:(fofType->(fofType->Prop)) % FOF formula (<kernel.Constant object at 0x1461170>, <kernel.DependentProduct object at 0x1084c20>) of role type named cs4_atom_decl % Using role type % Declaring cs4_atom:((fofType->Prop)->(fofType->Prop)) % FOF formula (<kernel.Constant object at 0x14615f0>, <kernel.DependentProduct object at 0x14be200>) of role type named cs4_and_decl % Using role type % Declaring cs4_and:((fofType->Prop)->((fofType->Prop)->(fofType->Prop))) % FOF formula (<kernel.Constant object at 0x1461170>, <kernel.DependentProduct object at 0x1084dd0>) of role type named cs4_or_decl % Using role type % Declaring cs4_or:((fofType->Prop)->((fofType->Prop)->(fofType->Prop))) % FOF formula (<kernel.Constant object at 0x1461170>, <kernel.DependentProduct object at 0x1084b00>) of role type named cs4_impl_decl % Using role type % Declaring cs4_impl:((fofType->Prop)->((fofType->Prop)->(fofType->Prop))) % FOF formula (<kernel.Constant object at 0x14befc8>, <kernel.DependentProduct object at 0x10849e0>) of role type named cs4_true_decl % Using role type % Declaring cs4_true:(fofType->Prop) % FOF formula (<kernel.Constant object at 0x14be200>, <kernel.DependentProduct object at 0x1084c20>) of role type named cs4_false_decl % Using role type % Declaring cs4_false:(fofType->Prop) % FOF formula (<kernel.Constant object at 0x14befc8>, <kernel.DependentProduct object at 0x1084b90>) of role type named cs4_all_decl % Using role type % Declaring cs4_all:((individuals->(fofType->Prop))->(fofType->Prop)) % FOF formula (<kernel.Constant object at 0x14befc8>, <kernel.DependentProduct object at 0x10849e0>) of role type named cs4_box_decl % Using role type % Declaring cs4_box:((fofType->Prop)->(fofType->Prop)) % FOF formula (((eq ((fofType->Prop)->(fofType->Prop))) cs4_atom) (fun (P:(fofType->Prop))=> ((mbox reli) P))) of role definition named cs4_atom % A new definition: (((eq ((fofType->Prop)->(fofType->Prop))) cs4_atom) (fun (P:(fofType->Prop))=> ((mbox reli) P))) % Defined: cs4_atom:=(fun (P:(fofType->Prop))=> ((mbox reli) P)) % FOF formula (((eq ((fofType->Prop)->((fofType->Prop)->(fofType->Prop)))) cs4_and) (fun (A:(fofType->Prop)) (B:(fofType->Prop))=> ((mand A) B))) of role definition named cs4_and % A new definition: (((eq ((fofType->Prop)->((fofType->Prop)->(fofType->Prop)))) cs4_and) (fun (A:(fofType->Prop)) (B:(fofType->Prop))=> ((mand A) B))) % Defined: cs4_and:=(fun (A:(fofType->Prop)) (B:(fofType->Prop))=> ((mand A) B)) % FOF formula (((eq ((fofType->Prop)->((fofType->Prop)->(fofType->Prop)))) cs4_or) (fun (A:(fofType->Prop)) (B:(fofType->Prop))=> ((mor A) B))) of role definition named cs4_or % A new definition: (((eq ((fofType->Prop)->((fofType->Prop)->(fofType->Prop)))) cs4_or) (fun (A:(fofType->Prop)) (B:(fofType->Prop))=> ((mor A) B))) % Defined: cs4_or:=(fun (A:(fofType->Prop)) (B:(fofType->Prop))=> ((mor A) B)) % FOF formula (((eq ((fofType->Prop)->((fofType->Prop)->(fofType->Prop)))) cs4_impl) (fun (A:(fofType->Prop)) (B:(fofType->Prop))=> ((mbox reli) ((mimpl A) B)))) of role definition named cs4_impl % A new definition: (((eq ((fofType->Prop)->((fofType->Prop)->(fofType->Prop)))) cs4_impl) (fun (A:(fofType->Prop)) (B:(fofType->Prop))=> ((mbox reli) ((mimpl A) B)))) % Defined: cs4_impl:=(fun (A:(fofType->Prop)) (B:(fofType->Prop))=> ((mbox reli) ((mimpl A) B))) % FOF formula (((eq (fofType->Prop)) cs4_true) mtrue) of role definition named cs4_true % A new definition: (((eq (fofType->Prop)) cs4_true) mtrue) % Defined: cs4_true:=mtrue % FOF formula (((eq (fofType->Prop)) cs4_false) mfalse) of role definition named cs4_false % A new definition: (((eq (fofType->Prop)) cs4_false) mfalse) % Defined: cs4_false:=mfalse % FOF formula (((eq ((individuals->(fofType->Prop))->(fofType->Prop))) cs4_all) (fun (A:(individuals->(fofType->Prop)))=> ((mbox reli) (mall A)))) of role definition named cs4_all % A new definition: (((eq ((individuals->(fofType->Prop))->(fofType->Prop))) cs4_all) (fun (A:(individuals->(fofType->Prop)))=> ((mbox reli) (mall A)))) % Defined: cs4_all:=(fun (A:(individuals->(fofType->Prop)))=> ((mbox reli) (mall A))) % FOF formula (((eq ((fofType->Prop)->(fofType->Prop))) cs4_box) (fun (A:(fofType->Prop))=> ((mbox reli) ((mbox relr) A)))) of role definition named cs4_box % A new definition: (((eq ((fofType->Prop)->(fofType->Prop))) cs4_box) (fun (A:(fofType->Prop))=> ((mbox reli) ((mbox relr) A)))) % Defined: cs4_box:=(fun (A:(fofType->Prop))=> ((mbox reli) ((mbox relr) A))) % FOF formula (<kernel.Constant object at 0x10845f0>, <kernel.DependentProduct object at 0x1084b90>) of role type named cs4_valid_decl % Using role type % Declaring cs4_valid:((fofType->Prop)->Prop) % FOF formula (((eq ((fofType->Prop)->Prop)) cs4_valid) (fun (A:(fofType->Prop))=> (mvalid A))) of role definition named cs4_valid_def % A new definition: (((eq ((fofType->Prop)->Prop)) cs4_valid) (fun (A:(fofType->Prop))=> (mvalid A))) % Defined: cs4_valid:=(fun (A:(fofType->Prop))=> (mvalid A)) % FOF formula (forall (A:(fofType->Prop)), (mvalid ((mimpl ((mbox reli) A)) A))) of role axiom named refl_axiom_i % A new axiom: (forall (A:(fofType->Prop)), (mvalid ((mimpl ((mbox reli) A)) A))) % FOF formula (forall (A:(fofType->Prop)), (mvalid ((mimpl ((mbox relr) A)) A))) of role axiom named refl_axiom_r % A new axiom: (forall (A:(fofType->Prop)), (mvalid ((mimpl ((mbox relr) A)) A))) % FOF formula (forall (A:(fofType->Prop)), (mvalid ((mimpl ((mbox reli) A)) ((mbox reli) ((mbox reli) A))))) of role axiom named trans_axiom_i % A new axiom: (forall (A:(fofType->Prop)), (mvalid ((mimpl ((mbox reli) A)) ((mbox reli) ((mbox reli) A))))) % FOF formula (forall (A:(fofType->Prop)), (mvalid ((mimpl ((mbox relr) A)) ((mbox relr) ((mbox relr) A))))) of role axiom named trans_axiom_r % A new axiom: (forall (A:(fofType->Prop)), (mvalid ((mimpl ((mbox relr) A)) ((mbox relr) ((mbox relr) A))))) % FOF formula (forall (A:(fofType->Prop)), (mvalid ((mimpl ((mbox reli) ((mbox relr) A))) ((mbox relr) ((mbox reli) A))))) of role axiom named ax_i_r_commute % A new axiom: (forall (A:(fofType->Prop)), (mvalid ((mimpl ((mbox reli) ((mbox relr) A))) ((mbox relr) ((mbox reli) A))))) % Failed to open /home/cristobal/cocATP/CASC/TPTP/Axioms/SWV010^0.ax, trying next directory % FOF formula (<kernel.Constant object at 0x1461170>, <kernel.DependentProduct object at 0x1084488>) of role type named princ_inj % Using role type % Declaring princ_inj:(individuals->(fofType->Prop)) % FOF formula (<kernel.Constant object at 0x1461170>, <kernel.DependentProduct object at 0x1084488>) of role type named bl_atom_decl % Using role type % Declaring bl_atom:((fofType->Prop)->(fofType->Prop)) % FOF formula (<kernel.Constant object at 0x14be248>, <kernel.DependentProduct object at 0x1084488>) of role type named bl_princ_decl % Using role type % Declaring bl_princ:((fofType->Prop)->(fofType->Prop)) % FOF formula (<kernel.Constant object at 0x14be200>, <kernel.DependentProduct object at 0x1084440>) of role type named bl_and_decl % Using role type % Declaring bl_and:((fofType->Prop)->((fofType->Prop)->(fofType->Prop))) % FOF formula (<kernel.Constant object at 0x14be248>, <kernel.DependentProduct object at 0x1084c20>) of role type named bl_or_decl % Using role type % Declaring bl_or:((fofType->Prop)->((fofType->Prop)->(fofType->Prop))) % FOF formula (<kernel.Constant object at 0x14be248>, <kernel.DependentProduct object at 0x1084cb0>) of role type named bl_impl_decl % Using role type % Declaring bl_impl:((fofType->Prop)->((fofType->Prop)->(fofType->Prop))) % FOF formula (<kernel.Constant object at 0x1084dd0>, <kernel.DependentProduct object at 0x1084a28>) of role type named bl_all_decl % Using role type % Declaring bl_all:((individuals->(fofType->Prop))->(fofType->Prop)) % FOF formula (<kernel.Constant object at 0x10845a8>, <kernel.DependentProduct object at 0x1084c20>) of role type named bl_true_decl % Using role type % Declaring bl_true:(fofType->Prop) % FOF formula (<kernel.Constant object at 0x1084488>, <kernel.DependentProduct object at 0x10847e8>) of role type named bl_false_decl % Using role type % Declaring bl_false:(fofType->Prop) % FOF formula (<kernel.Constant object at 0x1084cb0>, <kernel.DependentProduct object at 0x10847a0>) of role type named bl_says_decl % Using role type % Declaring bl_says:(individuals->((fofType->Prop)->(fofType->Prop))) % FOF formula (((eq ((fofType->Prop)->(fofType->Prop))) bl_atom) (fun (P:(fofType->Prop))=> (cs4_atom P))) of role definition named bl_atom % A new definition: (((eq ((fofType->Prop)->(fofType->Prop))) bl_atom) (fun (P:(fofType->Prop))=> (cs4_atom P))) % Defined: bl_atom:=(fun (P:(fofType->Prop))=> (cs4_atom P)) % FOF formula (((eq ((fofType->Prop)->(fofType->Prop))) bl_princ) (fun (P:(fofType->Prop))=> (cs4_atom P))) of role definition named bl_princ % A new definition: (((eq ((fofType->Prop)->(fofType->Prop))) bl_princ) (fun (P:(fofType->Prop))=> (cs4_atom P))) % Defined: bl_princ:=(fun (P:(fofType->Prop))=> (cs4_atom P)) % FOF formula (((eq ((fofType->Prop)->((fofType->Prop)->(fofType->Prop)))) bl_and) (fun (A:(fofType->Prop)) (B:(fofType->Prop))=> ((cs4_and A) B))) of role definition named bl_and % A new definition: (((eq ((fofType->Prop)->((fofType->Prop)->(fofType->Prop)))) bl_and) (fun (A:(fofType->Prop)) (B:(fofType->Prop))=> ((cs4_and A) B))) % Defined: bl_and:=(fun (A:(fofType->Prop)) (B:(fofType->Prop))=> ((cs4_and A) B)) % FOF formula (((eq ((fofType->Prop)->((fofType->Prop)->(fofType->Prop)))) bl_or) (fun (A:(fofType->Prop)) (B:(fofType->Prop))=> ((cs4_or A) B))) of role definition named bl_or % A new definition: (((eq ((fofType->Prop)->((fofType->Prop)->(fofType->Prop)))) bl_or) (fun (A:(fofType->Prop)) (B:(fofType->Prop))=> ((cs4_or A) B))) % Defined: bl_or:=(fun (A:(fofType->Prop)) (B:(fofType->Prop))=> ((cs4_or A) B)) % FOF formula (((eq ((fofType->Prop)->((fofType->Prop)->(fofType->Prop)))) bl_impl) (fun (A:(fofType->Prop)) (B:(fofType->Prop))=> ((cs4_impl A) B))) of role definition named bl_impl % A new definition: (((eq ((fofType->Prop)->((fofType->Prop)->(fofType->Prop)))) bl_impl) (fun (A:(fofType->Prop)) (B:(fofType->Prop))=> ((cs4_impl A) B))) % Defined: bl_impl:=(fun (A:(fofType->Prop)) (B:(fofType->Prop))=> ((cs4_impl A) B)) % FOF formula (((eq ((individuals->(fofType->Prop))->(fofType->Prop))) bl_all) (fun (A:(individuals->(fofType->Prop)))=> (cs4_all A))) of role definition named bl_all % A new definition: (((eq ((individuals->(fofType->Prop))->(fofType->Prop))) bl_all) (fun (A:(individuals->(fofType->Prop)))=> (cs4_all A))) % Defined: bl_all:=(fun (A:(individuals->(fofType->Prop)))=> (cs4_all A)) % FOF formula (((eq (fofType->Prop)) bl_true) cs4_true) of role definition named bl_true % A new definition: (((eq (fofType->Prop)) bl_true) cs4_true) % Defined: bl_true:=cs4_true % FOF formula (((eq (fofType->Prop)) bl_false) cs4_false) of role definition named bl_false % A new definition: (((eq (fofType->Prop)) bl_false) cs4_false) % Defined: bl_false:=cs4_false % FOF formula (((eq (individuals->((fofType->Prop)->(fofType->Prop)))) bl_says) (fun (K:individuals) (A:(fofType->Prop))=> (cs4_box ((cs4_impl (bl_princ (princ_inj K))) A)))) of role definition named bl_says % A new definition: (((eq (individuals->((fofType->Prop)->(fofType->Prop)))) bl_says) (fun (K:individuals) (A:(fofType->Prop))=> (cs4_box ((cs4_impl (bl_princ (princ_inj K))) A)))) % Defined: bl_says:=(fun (K:individuals) (A:(fofType->Prop))=> (cs4_box ((cs4_impl (bl_princ (princ_inj K))) A))) % FOF formula (<kernel.Constant object at 0x10849e0>, <kernel.DependentProduct object at 0x10845a8>) of role type named bl_valid_decl % Using role type % Declaring bl_valid:((fofType->Prop)->Prop) % FOF formula (((eq ((fofType->Prop)->Prop)) bl_valid) mvalid) of role definition named bl_valid_def % A new definition: (((eq ((fofType->Prop)->Prop)) bl_valid) mvalid) % Defined: bl_valid:=mvalid % FOF formula (<kernel.Constant object at 0x1084b90>, <kernel.Constant object at 0x1084710>) of role type named loca_decl % Using role type % Declaring loca:individuals % FOF formula (cs4_valid (cs4_all (fun (K:individuals)=> ((cs4_impl (princ_inj K)) (princ_inj loca))))) of role axiom named loca_strength % A new axiom: (cs4_valid (cs4_all (fun (K:individuals)=> ((cs4_impl (princ_inj K)) (princ_inj loca))))) % FOF formula (<kernel.Constant object at 0x1069680>, <kernel.Constant object at 0x10695a8>) of role type named ctime_decl % Using role type % Declaring ctime:individuals % FOF formula (<kernel.Constant object at 0x1069758>, <kernel.Constant object at 0x10695a8>) of role type named ninfty_decl % Using role type % Declaring ninfty:individuals % FOF formula (<kernel.Constant object at 0x1069950>, <kernel.Constant object at 0x10695a8>) of role type named pinfty_decl % Using role type % Declaring pinfty:individuals % FOF formula (<kernel.Constant object at 0x1069680>, <kernel.Constant object at 0x10695a8>) of role type named read_decl % Using role type % Declaring read:individuals % FOF formula (<kernel.Constant object at 0x1069758>, <kernel.Constant object at 0x10695a8>) of role type named write_decl % Using role type % Declaring write:individuals % FOF formula (<kernel.Constant object at 0x1069950>, <kernel.Constant object at 0x10695a8>) of role type named execute_decl % Using role type % Declaring execute:individuals % FOF formula (<kernel.Constant object at 0x1069680>, <kernel.Constant object at 0x1069758>) of role type named identity_decl % Using role type % Declaring identity:individuals % FOF formula (<kernel.Constant object at 0x1069950>, <kernel.Constant object at 0x14601b8>) of role type named govern_decl % Using role type % Declaring govern:individuals % FOF formula (<kernel.Constant object at 0x1069758>, <kernel.DependentProduct object at 0x1460f80>) of role type named prim_str2file_decl % Using role type % Declaring prim_str2file:(individuals->individuals) % FOF formula (<kernel.Constant object at 0x10695a8>, <kernel.DependentProduct object at 0x1460ea8>) of role type named prim_date2time_decl % Using role type % Declaring prim_date2time:(individuals->individuals) % FOF formula (<kernel.Constant object at 0x1069758>, <kernel.DependentProduct object at 0x1460e60>) of role type named prim_int2time_decl % Using role type % Declaring prim_int2time:(individuals->individuals) % FOF formula (<kernel.Constant object at 0x1069758>, <kernel.DependentProduct object at 0x1460f38>) of role type named prim_int2principal_decl % Using role type % Declaring prim_int2principal:(individuals->individuals) % FOF formula (<kernel.Constant object at 0x1460ea8>, <kernel.DependentProduct object at 0x1460e18>) of role type named time2exp_decl % Using role type % Declaring time2exp:(individuals->individuals) % FOF formula (<kernel.Constant object at 0x1460e60>, <kernel.DependentProduct object at 0x14601b8>) of role type named exp_add_decl % Using role type % Declaring exp_add:(individuals->(individuals->individuals)) % FOF formula (<kernel.Constant object at 0x1460f38>, <kernel.DependentProduct object at 0x1460ef0>) of role type named exp_subtract_decl % Using role type % Declaring exp_subtract:(individuals->(individuals->individuals)) % FOF formula (<kernel.Constant object at 0x1460e18>, <kernel.DependentProduct object at 0x1460c68>) of role type named exp_min_decl % Using role type % Declaring exp_min:(individuals->(individuals->individuals)) % FOF formula (<kernel.Constant object at 0x14601b8>, <kernel.DependentProduct object at 0x1460098>) of role type named exp_max_decl % Using role type % Declaring exp_max:(individuals->(individuals->individuals)) % FOF formula (<kernel.Constant object at 0x1460ef0>, <kernel.Constant object at 0x1460098>) of role type named unclassified_decl % Using role type % Declaring unclassified:individuals % FOF formula (<kernel.Constant object at 0x1460e18>, <kernel.Constant object at 0x1460098>) of role type named sbu_decl % Using role type % Declaring sbu:individuals % FOF formula (<kernel.Constant object at 0x14601b8>, <kernel.Constant object at 0x1460098>) of role type named confidential_decl % Using role type % Declaring confidential:individuals % FOF formula (<kernel.Constant object at 0x1460ef0>, <kernel.Constant object at 0x1460098>) of role type named secret_decl % Using role type % Declaring secret:individuals % FOF formula (<kernel.Constant object at 0x1460e18>, <kernel.Constant object at 0x1460098>) of role type named topsecret_decl % Using role type % Declaring topsecret:individuals % FOF formula (<kernel.Constant object at 0x14601b8>, <kernel.Constant object at 0x1460098>) of role type named admin_decl % Using role type % Declaring admin:individuals % FOF formula (<kernel.Constant object at 0x1460ef0>, <kernel.Constant object at 0x1460098>) of role type named system_decl % Using role type % Declaring system:individuals % FOF formula (<kernel.Constant object at 0x1460e18>, <kernel.Constant object at 0x1460098>) of role type named nil_decl % Using role type % Declaring nil:individuals % FOF formula (<kernel.Constant object at 0x14601b8>, <kernel.DependentProduct object at 0x1461488>) of role type named cons_decl % Using role type % Declaring cons:(individuals->(individuals->individuals)) % FOF formula (<kernel.Constant object at 0x1460ef0>, <kernel.Constant object at 0x14615f0>) of role type named anycountry_decl % Using role type % Declaring anycountry:individuals % FOF formula (<kernel.Constant object at 0x14601b8>, <kernel.Constant object at 0x1461440>) of role type named usa_decl % Using role type % Declaring usa:individuals % FOF formula (<kernel.Constant object at 0x1460ef0>, <kernel.Constant object at 0x1461ab8>) of role type named yes_decl % Using role type % Declaring yes:individuals % FOF formula (<kernel.Constant object at 0x1460098>, <kernel.Constant object at 0x1461ab8>) of role type named no_decl % Using role type % Declaring no:individuals % FOF formula (<kernel.Constant object at 0x1460098>, <kernel.Constant object at 0x1461ab8>) of role type named is_working_paper_decl % Using role type % Declaring is_working_paper:individuals % FOF formula (<kernel.Constant object at 0x1461170>, <kernel.Constant object at 0x1461b00>) of role type named is_not_working_paper_decl % Using role type % Declaring is_not_working_paper:individuals % FOF formula (<kernel.Constant object at 0x1461488>, <kernel.Constant object at 0x14befc8>) of role type named oca_decl % Using role type % Declaring oca:individuals % FOF formula (<kernel.Constant object at 0x1461b00>, <kernel.Constant object at 0x14be200>) of role type named compartmentb_decl % Using role type % Declaring compartmentb:individuals % FOF formula (<kernel.Constant object at 0x1461488>, <kernel.Constant object at 0x14be200>) of role type named sso_compartmentb_decl % Using role type % Declaring sso_compartmentb:individuals % FOF formula (<kernel.Constant object at 0x1461b00>, <kernel.Constant object at 0x14be248>) of role type named scg_compartmentb_decl % Using role type % Declaring scg_compartmentb:individuals % FOF formula (<kernel.Constant object at 0x1461b00>, <kernel.Constant object at 0x1084b90>) of role type named compartmenta_decl % Using role type % Declaring compartmenta:individuals % FOF formula (<kernel.Constant object at 0x14be248>, <kernel.Constant object at 0x10843b0>) of role type named sso_compartmenta_decl % Using role type % Declaring sso_compartmenta:individuals % FOF formula (<kernel.Constant object at 0x14be638>, <kernel.Constant object at 0x1084440>) of role type named scg_compartmenta_decl % Using role type % Declaring scg_compartmenta:individuals % FOF formula (<kernel.Constant object at 0x14be200>, <kernel.Constant object at 0x1084440>) of role type named secretfile_decl % Using role type % Declaring secretfile:individuals % FOF formula (<kernel.Constant object at 0x14be200>, <kernel.Constant object at 0x1084440>) of role type named not_secretfile_decl % Using role type % Declaring not_secretfile:individuals % FOF formula (<kernel.Constant object at 0x1084dd0>, <kernel.Constant object at 0x1084440>) of role type named alice_decl % Using role type % Declaring alice:individuals % FOF formula (<kernel.Constant object at 0x10847e8>, <kernel.Constant object at 0x1084440>) of role type named babu_decl % Using role type % Declaring babu:individuals % FOF formula (<kernel.Constant object at 0x1084a28>, <kernel.Constant object at 0x1084440>) of role type named india_decl % Using role type % Declaring india:individuals % FOF formula (<kernel.Constant object at 0x1084dd0>, <kernel.Constant object at 0x1084440>) of role type named polygraph_admin_decl % Using role type % Declaring polygraph_admin:individuals % FOF formula (<kernel.Constant object at 0x10847e8>, <kernel.Constant object at 0x1084440>) of role type named credit_admin_decl % Using role type % Declaring credit_admin:individuals % FOF formula (<kernel.Constant object at 0x1084a28>, <kernel.Constant object at 0x1084440>) of role type named background_admin_decl % Using role type % Declaring background_admin:individuals % FOF formula (<kernel.Constant object at 0x1084dd0>, <kernel.Constant object at 0x1084440>) of role type named hr_admin_decl % Using role type % Declaring hr_admin:individuals % FOF formula (<kernel.Constant object at 0x10847e8>, <kernel.Constant object at 0x1084440>) of role type named level_admin_decl % Using role type % Declaring level_admin:individuals % FOF formula (<kernel.Constant object at 0x1084a28>, <kernel.Constant object at 0x1084440>) of role type named owner_secretfile_decl % Using role type % Declaring owner_secretfile:individuals % FOF formula (<kernel.Constant object at 0x1084dd0>, <kernel.Constant object at 0x1084440>) of role type named owner_not_secretfile_decl % Using role type % Declaring owner_not_secretfile:individuals % FOF formula (<kernel.Constant object at 0x10847e8>, <kernel.Constant object at 0x1084440>) of role type named ci_decl % Using role type % Declaring ci:individuals % FOF formula (<kernel.Constant object at 0x10843b0>, <kernel.DependentProduct object at 0x10847e8>) of role type named loca_level_direct_below_decl % Using role type % Declaring loca_level_direct_below:(individuals->(individuals->(fofType->Prop))) % FOF formula (<kernel.Constant object at 0x10849e0>, <kernel.DependentProduct object at 0x10845f0>) of role type named loca_level_below_decl % Using role type % Declaring loca_level_below:(individuals->(individuals->(fofType->Prop))) % FOF formula (<kernel.Constant object at 0x1084a28>, <kernel.DependentProduct object at 0x10849e0>) of role type named system_compartment_has_sso_decl % Using role type % Declaring system_compartment_has_sso:(individuals->(individuals->(fofType->Prop))) % FOF formula (<kernel.Constant object at 0x1084440>, <kernel.DependentProduct object at 0x10845f0>) of role type named admin_compartment_has_sso_decl % Using role type % Declaring admin_compartment_has_sso:(individuals->(individuals->(fofType->Prop))) % FOF formula (<kernel.Constant object at 0x10847e8>, <kernel.DependentProduct object at 0x107a248>) of role type named system_indi_is_oca_decl % Using role type % Declaring system_indi_is_oca:(individuals->(fofType->Prop)) % FOF formula (<kernel.Constant object at 0x1084a70>, <kernel.DependentProduct object at 0x10845a8>) of role type named oca_compartment_has_scg_decl % Using role type % Declaring oca_compartment_has_scg:(individuals->(individuals->(fofType->Prop))) % FOF formula (<kernel.Constant object at 0x1084a28>, <kernel.DependentProduct object at 0x107a5f0>) of role type named sso_compartment_has_scg_decl % Using role type % Declaring sso_compartment_has_scg:(individuals->(individuals->(fofType->Prop))) % FOF formula (<kernel.Constant object at 0x1084440>, <kernel.DependentProduct object at 0x107a560>) of role type named admin_compartment_has_scg_decl % Using role type % Declaring admin_compartment_has_scg:(individuals->(individuals->(fofType->Prop))) % FOF formula (<kernel.Constant object at 0x10845a8>, <kernel.DependentProduct object at 0x107a7a0>) of role type named system_file_needs_compartments_decl % Using role type % Declaring system_file_needs_compartments:(individuals->(individuals->(fofType->Prop))) % FOF formula (<kernel.Constant object at 0x107acb0>, <kernel.DependentProduct object at 0x107ab90>) of role type named admin_file_has_compartments_h_decl % Using role type % Declaring admin_file_has_compartments_h:(individuals->(individuals->(individuals->(fofType->Prop)))) % FOF formula (<kernel.Constant object at 0x10848c0>, <kernel.DependentProduct object at 0x107a5f0>) of role type named admin_file_has_compartments_decl % Using role type % Declaring admin_file_has_compartments:(individuals->(individuals->(fofType->Prop))) % FOF formula (<kernel.Constant object at 0x10848c0>, <kernel.DependentProduct object at 0x107a8c0>) of role type named sso_file_has_compartments_decl % Using role type % Declaring sso_file_has_compartments:(individuals->(individuals->(fofType->Prop))) % FOF formula (<kernel.Constant object at 0x107a710>, <kernel.DependentProduct object at 0x107a7a0>) of role type named system_file_needs_level_decl % Using role type % Declaring system_file_needs_level:(individuals->(individuals->(fofType->Prop))) % FOF formula (<kernel.Constant object at 0x107a128>, <kernel.DependentProduct object at 0x107acb0>) of role type named admin_file_has_level_h_decl % Using role type % Declaring admin_file_has_level_h:(individuals->(individuals->(individuals->(fofType->Prop)))) % FOF formula (<kernel.Constant object at 0x107a488>, <kernel.DependentProduct object at 0x107a248>) of role type named admin_file_has_level_decl % Using role type % Declaring admin_file_has_level:(individuals->(individuals->(fofType->Prop))) % FOF formula (<kernel.Constant object at 0x107a2d8>, <kernel.DependentProduct object at 0x107ab90>) of role type named sso_file_has_level_decl % Using role type % Declaring sso_file_has_level:(individuals->(individuals->(individuals->(fofType->Prop)))) % FOF formula (<kernel.Constant object at 0x107a2d8>, <kernel.DependentProduct object at 0x107ab90>) of role type named system_file_needs_citizenship_decl % Using role type % Declaring system_file_needs_citizenship:(individuals->(individuals->(fofType->Prop))) % FOF formula (<kernel.Constant object at 0x107a4d0>, <kernel.DependentProduct object at 0x107a2d8>) of role type named admin_file_has_citizenship_h_decl % Using role type % Declaring admin_file_has_citizenship_h:(individuals->(individuals->(individuals->(fofType->Prop)))) % FOF formula (<kernel.Constant object at 0x107a248>, <kernel.DependentProduct object at 0x107a440>) of role type named admin_file_has_citizenship_decl % Using role type % Declaring admin_file_has_citizenship:(individuals->(individuals->(fofType->Prop))) % FOF formula (<kernel.Constant object at 0x107a758>, <kernel.DependentProduct object at 0x107a128>) of role type named sso_file_has_citizenship_decl % Using role type % Declaring sso_file_has_citizenship:(individuals->(individuals->(individuals->(fofType->Prop)))) % FOF formula (<kernel.Constant object at 0x107a6c8>, <kernel.DependentProduct object at 0x107a488>) of role type named system_indi_is_polygraph_admin_decl % Using role type % Declaring system_indi_is_polygraph_admin:(individuals->(fofType->Prop)) % FOF formula (<kernel.Constant object at 0x107a680>, <kernel.DependentProduct object at 0x107a1b8>) of role type named polygraph_admin_indi_has_polygraph_decl % Using role type % Declaring polygraph_admin_indi_has_polygraph:(individuals->(fofType->Prop)) % FOF formula (<kernel.Constant object at 0x107a638>, <kernel.DependentProduct object at 0x107a440>) of role type named admin_indi_has_polygraph_decl % Using role type % Declaring admin_indi_has_polygraph:(individuals->(fofType->Prop)) % FOF formula (<kernel.Constant object at 0x107a128>, <kernel.DependentProduct object at 0x107a1b8>) of role type named system_indi_is_credit_admin_decl % Using role type % Declaring system_indi_is_credit_admin:(individuals->(fofType->Prop)) % FOF formula (<kernel.Constant object at 0x107a680>, <kernel.DependentProduct object at 0x107a518>) of role type named credit_admin_indi_has_credit_decl % Using role type % Declaring credit_admin_indi_has_credit:(individuals->(fofType->Prop)) % FOF formula (<kernel.Constant object at 0x107a440>, <kernel.DependentProduct object at 0x107a518>) of role type named admin_indi_has_credit_decl % Using role type % Declaring admin_indi_has_credit:(individuals->(fofType->Prop)) % FOF formula (<kernel.Constant object at 0x107a6c8>, <kernel.DependentProduct object at 0x107a440>) of role type named admin_indi_has_background_decl % Using role type % Declaring admin_indi_has_background:(individuals->(individuals->(fofType->Prop))) % FOF formula (<kernel.Constant object at 0x107a128>, <kernel.DependentProduct object at 0x107a758>) of role type named system_indi_is_background_admin_decl % Using role type % Declaring system_indi_is_background_admin:(individuals->(fofType->Prop)) % FOF formula (<kernel.Constant object at 0x107a518>, <kernel.DependentProduct object at 0x107aa70>) of role type named background_admin_indi_has_background_decl % Using role type % Declaring background_admin_indi_has_background:(individuals->(individuals->(fofType->Prop))) % FOF formula (<kernel.Constant object at 0x107a1b8>, <kernel.DependentProduct object at 0x107ac68>) of role type named system_indi_is_hr_admin_decl % Using role type % Declaring system_indi_is_hr_admin:(individuals->(fofType->Prop)) % FOF formula (<kernel.Constant object at 0x107a680>, <kernel.DependentProduct object at 0x107a878>) of role type named hr_admin_indi_has_employment_decl % Using role type % Declaring hr_admin_indi_has_employment:(individuals->(fofType->Prop)) % FOF formula (<kernel.Constant object at 0x107a9e0>, <kernel.DependentProduct object at 0x107ac68>) of role type named admin_indi_has_employment_decl % Using role type % Declaring admin_indi_has_employment:(individuals->(fofType->Prop)) % FOF formula (<kernel.Constant object at 0x107a128>, <kernel.DependentProduct object at 0x107a7e8>) of role type named admin_indi_has_citizenship_decl % Using role type % Declaring admin_indi_has_citizenship:(individuals->(individuals->(fofType->Prop))) % FOF formula (<kernel.Constant object at 0x107a1b8>, <kernel.DependentProduct object at 0x107acf8>) of role type named system_indi_has_citizenship_decl % Using role type % Declaring system_indi_has_citizenship:(individuals->(individuals->(fofType->Prop))) % FOF formula (<kernel.Constant object at 0x107ab00>, <kernel.DependentProduct object at 0x107a908>) of role type named admin_indi_has_level_decl % Using role type % Declaring admin_indi_has_level:(individuals->(individuals->(fofType->Prop))) % FOF formula (<kernel.Constant object at 0x107a878>, <kernel.DependentProduct object at 0x107ab00>) of role type named system_indi_needs_level_decl % Using role type % Declaring system_indi_needs_level:(individuals->(individuals->(fofType->Prop))) % FOF formula (<kernel.Constant object at 0x107a128>, <kernel.DependentProduct object at 0x107a908>) of role type named system_indi_is_level_admin_decl % Using role type % Declaring system_indi_is_level_admin:(individuals->(fofType->Prop)) % FOF formula (<kernel.Constant object at 0x107a950>, <kernel.DependentProduct object at 0x107ad40>) of role type named level_admin_indi_has_level_decl % Using role type % Declaring level_admin_indi_has_level:(individuals->(individuals->(fofType->Prop))) % FOF formula (<kernel.Constant object at 0x107acf8>, <kernel.DependentProduct object at 0x107ae18>) of role type named admin_indi_has_compartments_decl % Using role type % Declaring admin_indi_has_compartments:(individuals->(individuals->(fofType->Prop))) % FOF formula (<kernel.Constant object at 0x107aef0>, <kernel.DependentProduct object at 0x107acf8>) of role type named system_indi_needs_compartment_decl % Using role type % Declaring system_indi_needs_compartment:(individuals->(individuals->(fofType->Prop))) % FOF formula (<kernel.Constant object at 0x107add0>, <kernel.DependentProduct object at 0x107a9e0>) of role type named admin_indi_has_polygraph_for_compartment_decl % Using role type % Declaring admin_indi_has_polygraph_for_compartment:(individuals->(individuals->(fofType->Prop))) % FOF formula (<kernel.Constant object at 0x107ae18>, <kernel.DependentProduct object at 0x107af80>) of role type named admin_indi_has_credit_for_compartment_decl % Using role type % Declaring admin_indi_has_credit_for_compartment:(individuals->(individuals->(fofType->Prop))) % FOF formula (<kernel.Constant object at 0x107ae60>, <kernel.DependentProduct object at 0x107ae18>) of role type named sso_indi_has_compartment_decl % Using role type % Declaring sso_indi_has_compartment:(individuals->(individuals->(fofType->Prop))) % FOF formula (<kernel.Constant object at 0x107acf8>, <kernel.DependentProduct object at 0x107afc8>) of role type named admin_indi_has_background_for_compartment_decl % Using role type % Declaring admin_indi_has_background_for_compartment:(individuals->(individuals->(fofType->Prop))) % FOF formula (<kernel.Constant object at 0x107af80>, <kernel.DependentProduct object at 0x107af38>) of role type named admin_indi_has_level_for_compartment_decl % Using role type % Declaring admin_indi_has_level_for_compartment:(individuals->(individuals->(fofType->Prop))) % FOF formula (<kernel.Constant object at 0x107af80>, <kernel.DependentProduct object at 0x1459098>) of role type named oca_compartment_is_compartment_decl % Using role type % Declaring oca_compartment_is_compartment:(individuals->(individuals->(individuals->(individuals->(individuals->(fofType->Prop)))))) % FOF formula (<kernel.Constant object at 0x107ab00>, <kernel.DependentProduct object at 0x107acf8>) of role type named admin_indi_has_compartments_for_file_decl % Using role type % Declaring admin_indi_has_compartments_for_file:(individuals->(individuals->(fofType->Prop))) % FOF formula (<kernel.Constant object at 0x107acf8>, <kernel.DependentProduct object at 0x1459248>) of role type named admin_indi_has_level_for_file_decl % Using role type % Declaring admin_indi_has_level_for_file:(individuals->(individuals->(fofType->Prop))) % FOF formula (<kernel.Constant object at 0x107a878>, <kernel.DependentProduct object at 0x14591b8>) of role type named p_owner_decl % Using role type % Declaring p_owner:(individuals->(individuals->(fofType->Prop))) % FOF formula (<kernel.Constant object at 0x107ab00>, <kernel.DependentProduct object at 0x14590e0>) of role type named owner_indi_has_need_to_know_decl % Using role type % Declaring owner_indi_has_need_to_know:(individuals->(individuals->(fofType->Prop))) % FOF formula (<kernel.Constant object at 0x107acf8>, <kernel.DependentProduct object at 0x14591b8>) of role type named admin_indi_has_need_to_know_for_file_decl % Using role type % Declaring admin_indi_has_need_to_know_for_file:(individuals->(individuals->(fofType->Prop))) % FOF formula (<kernel.Constant object at 0x1459200>, <kernel.DependentProduct object at 0x14592d8>) of role type named admin_indi_has_citizenship_for_file_decl % Using role type % Declaring admin_indi_has_citizenship_for_file:(individuals->(individuals->(fofType->Prop))) % FOF formula (<kernel.Constant object at 0x107ab00>, <kernel.DependentProduct object at 0x1459290>) of role type named p_has_xattr_decl % Using role type % Declaring p_has_xattr:(individuals->(individuals->(individuals->(fofType->Prop)))) % FOF formula (<kernel.Constant object at 0x14591b8>, <kernel.DependentProduct object at 0x1459440>) of role type named admin_file_has_not_expired_decl % Using role type % Declaring admin_file_has_not_expired:(individuals->(fofType->Prop)) % FOF formula (<kernel.Constant object at 0x1459200>, <kernel.DependentProduct object at 0x1459170>) of role type named may_decl % Using role type % Declaring may:(individuals->(individuals->(individuals->(fofType->Prop)))) % FOF formula (<kernel.Constant object at 0x14593b0>, <kernel.DependentProduct object at 0x1459200>) of role type named system_indi_is_counterintelligence_decl % Using role type % Declaring system_indi_is_counterintelligence:(individuals->(individuals->(fofType->Prop))) % FOF formula (bl_valid ((bl_says loca) (bl_atom ((loca_level_direct_below unclassified) sbu)))) of role axiom named ax0 % A new axiom: (bl_valid ((bl_says loca) (bl_atom ((loca_level_direct_below unclassified) sbu)))) % FOF formula (bl_valid ((bl_says loca) (bl_atom ((loca_level_direct_below sbu) confidential)))) of role axiom named ax1 % A new axiom: (bl_valid ((bl_says loca) (bl_atom ((loca_level_direct_below sbu) confidential)))) % FOF formula (bl_valid ((bl_says loca) (bl_atom ((loca_level_direct_below confidential) secret)))) of role axiom named ax2 % A new axiom: (bl_valid ((bl_says loca) (bl_atom ((loca_level_direct_below confidential) secret)))) % FOF formula (bl_valid ((bl_says loca) (bl_atom ((loca_level_direct_below secret) topsecret)))) of role axiom named ax3 % A new axiom: (bl_valid ((bl_says loca) (bl_atom ((loca_level_direct_below secret) topsecret)))) % FOF formula (bl_valid ((bl_says loca) (bl_all (fun (L:individuals)=> (bl_atom ((loca_level_below L) L)))))) of role axiom named ax4 % A new axiom: (bl_valid ((bl_says loca) (bl_all (fun (L:individuals)=> (bl_atom ((loca_level_below L) L)))))) % FOF formula (bl_valid ((bl_says loca) (bl_all (fun (L:individuals)=> (bl_all (fun (L1:individuals)=> (bl_all (fun (L11:individuals)=> ((bl_impl (bl_atom ((loca_level_direct_below L1) L11))) ((bl_impl (bl_atom ((loca_level_below L) L1))) (bl_atom ((loca_level_below L) L11)))))))))))) of role axiom named ax5 % A new axiom: (bl_valid ((bl_says loca) (bl_all (fun (L:individuals)=> (bl_all (fun (L1:individuals)=> (bl_all (fun (L11:individuals)=> ((bl_impl (bl_atom ((loca_level_direct_below L1) L11))) ((bl_impl (bl_atom ((loca_level_below L) L1))) (bl_atom ((loca_level_below L) L11)))))))))))) % FOF formula (bl_valid ((bl_says admin) (bl_all (fun (C:individuals)=> (bl_all (fun (SSO:individuals)=> ((bl_impl ((bl_says system) (bl_atom ((system_compartment_has_sso C) SSO)))) (bl_atom ((admin_compartment_has_sso C) SSO))))))))) of role axiom named ax6 % A new axiom: (bl_valid ((bl_says admin) (bl_all (fun (C:individuals)=> (bl_all (fun (SSO:individuals)=> ((bl_impl ((bl_says system) (bl_atom ((system_compartment_has_sso C) SSO)))) (bl_atom ((admin_compartment_has_sso C) SSO))))))))) % FOF formula (bl_valid ((bl_says admin) (bl_all (fun (OCA:individuals)=> (bl_all (fun (C:individuals)=> (bl_all (fun (SSO:individuals)=> (bl_all (fun (SCG:individuals)=> ((bl_impl ((bl_says system) (bl_atom (system_indi_is_oca OCA)))) ((bl_impl ((bl_says OCA) (bl_atom ((oca_compartment_has_scg C) SCG)))) ((bl_impl (bl_atom ((admin_compartment_has_sso C) SSO))) ((bl_impl ((bl_says SSO) (bl_atom ((sso_compartment_has_scg C) SCG)))) (bl_atom ((admin_compartment_has_scg C) SCG)))))))))))))))) of role axiom named ax7 % A new axiom: (bl_valid ((bl_says admin) (bl_all (fun (OCA:individuals)=> (bl_all (fun (C:individuals)=> (bl_all (fun (SSO:individuals)=> (bl_all (fun (SCG:individuals)=> ((bl_impl ((bl_says system) (bl_atom (system_indi_is_oca OCA)))) ((bl_impl ((bl_says OCA) (bl_atom ((oca_compartment_has_scg C) SCG)))) ((bl_impl (bl_atom ((admin_compartment_has_sso C) SSO))) ((bl_impl ((bl_says SSO) (bl_atom ((sso_compartment_has_scg C) SCG)))) (bl_atom ((admin_compartment_has_scg C) SCG)))))))))))))))) % FOF formula (bl_valid ((bl_says admin) (bl_all (fun (F:individuals)=> (bl_all (fun (CL:individuals)=> ((bl_impl ((bl_says system) (bl_atom ((system_file_needs_compartments F) CL)))) ((bl_impl (bl_atom (((admin_file_has_compartments_h F) CL) CL))) (bl_atom ((admin_file_has_compartments F) CL)))))))))) of role axiom named ax8 % A new axiom: (bl_valid ((bl_says admin) (bl_all (fun (F:individuals)=> (bl_all (fun (CL:individuals)=> ((bl_impl ((bl_says system) (bl_atom ((system_file_needs_compartments F) CL)))) ((bl_impl (bl_atom (((admin_file_has_compartments_h F) CL) CL))) (bl_atom ((admin_file_has_compartments F) CL)))))))))) % FOF formula (bl_valid ((bl_says admin) (bl_all (fun (F:individuals)=> (bl_all (fun (CL:individuals)=> (bl_atom (((admin_file_has_compartments_h F) CL) nil)))))))) of role axiom named ax9 % A new axiom: (bl_valid ((bl_says admin) (bl_all (fun (F:individuals)=> (bl_all (fun (CL:individuals)=> (bl_atom (((admin_file_has_compartments_h F) CL) nil)))))))) % FOF formula (bl_valid ((bl_says admin) (bl_all (fun (F:individuals)=> (bl_all (fun (CL:individuals)=> (bl_all (fun (C1:individuals)=> (bl_all (fun (CL1:individuals)=> (bl_all (fun (SSO:individuals)=> ((bl_impl (bl_atom ((admin_compartment_has_sso C1) SSO))) ((bl_impl ((bl_says SSO) (bl_atom ((sso_file_has_compartments F) CL)))) ((bl_impl (bl_atom (((admin_file_has_compartments_h F) CL) CL1))) (bl_atom (((admin_file_has_compartments_h F) CL) ((cons C1) CL1)))))))))))))))))) of role axiom named ax10 % A new axiom: (bl_valid ((bl_says admin) (bl_all (fun (F:individuals)=> (bl_all (fun (CL:individuals)=> (bl_all (fun (C1:individuals)=> (bl_all (fun (CL1:individuals)=> (bl_all (fun (SSO:individuals)=> ((bl_impl (bl_atom ((admin_compartment_has_sso C1) SSO))) ((bl_impl ((bl_says SSO) (bl_atom ((sso_file_has_compartments F) CL)))) ((bl_impl (bl_atom (((admin_file_has_compartments_h F) CL) CL1))) (bl_atom (((admin_file_has_compartments_h F) CL) ((cons C1) CL1)))))))))))))))))) % FOF formula (bl_valid ((bl_says admin) (bl_all (fun (F:individuals)=> (bl_all (fun (L:individuals)=> (bl_all (fun (CL:individuals)=> ((bl_impl ((bl_says system) (bl_atom ((system_file_needs_level F) L)))) ((bl_impl (bl_atom ((admin_file_has_compartments F) CL))) ((bl_impl (bl_atom (((admin_file_has_level_h F) L) CL))) (bl_atom ((admin_file_has_level F) L))))))))))))) of role axiom named ax11 % A new axiom: (bl_valid ((bl_says admin) (bl_all (fun (F:individuals)=> (bl_all (fun (L:individuals)=> (bl_all (fun (CL:individuals)=> ((bl_impl ((bl_says system) (bl_atom ((system_file_needs_level F) L)))) ((bl_impl (bl_atom ((admin_file_has_compartments F) CL))) ((bl_impl (bl_atom (((admin_file_has_level_h F) L) CL))) (bl_atom ((admin_file_has_level F) L))))))))))))) % FOF formula (bl_valid ((bl_says admin) (bl_all (fun (F:individuals)=> (bl_all (fun (L:individuals)=> (bl_atom (((admin_file_has_level_h F) L) nil)))))))) of role axiom named ax12 % A new axiom: (bl_valid ((bl_says admin) (bl_all (fun (F:individuals)=> (bl_all (fun (L:individuals)=> (bl_atom (((admin_file_has_level_h F) L) nil)))))))) % FOF formula (bl_valid ((bl_says admin) (bl_all (fun (F:individuals)=> (bl_all (fun (L:individuals)=> (bl_all (fun (C:individuals)=> (bl_all (fun (CL:individuals)=> (bl_all (fun (SSO:individuals)=> (bl_all (fun (SCG:individuals)=> ((bl_impl (bl_atom ((admin_compartment_has_sso C) SSO))) ((bl_impl (bl_atom ((admin_compartment_has_scg C) SCG))) ((bl_impl ((bl_says SSO) (bl_atom (((sso_file_has_level F) L) SCG)))) ((bl_impl (bl_atom (((admin_file_has_level_h F) L) CL))) (bl_atom (((admin_file_has_level_h F) L) ((cons C) CL))))))))))))))))))))) of role axiom named ax13 % A new axiom: (bl_valid ((bl_says admin) (bl_all (fun (F:individuals)=> (bl_all (fun (L:individuals)=> (bl_all (fun (C:individuals)=> (bl_all (fun (CL:individuals)=> (bl_all (fun (SSO:individuals)=> (bl_all (fun (SCG:individuals)=> ((bl_impl (bl_atom ((admin_compartment_has_sso C) SSO))) ((bl_impl (bl_atom ((admin_compartment_has_scg C) SCG))) ((bl_impl ((bl_says SSO) (bl_atom (((sso_file_has_level F) L) SCG)))) ((bl_impl (bl_atom (((admin_file_has_level_h F) L) CL))) (bl_atom (((admin_file_has_level_h F) L) ((cons C) CL))))))))))))))))))))) % FOF formula (bl_valid ((bl_says admin) (bl_all (fun (F:individuals)=> (bl_all (fun (U:individuals)=> (bl_all (fun (CL:individuals)=> ((bl_impl ((bl_says system) (bl_atom ((system_file_needs_citizenship F) U)))) ((bl_impl (bl_atom ((admin_file_has_compartments F) CL))) ((bl_impl (bl_atom (((admin_file_has_citizenship_h F) U) CL))) (bl_atom ((admin_file_has_citizenship F) U))))))))))))) of role axiom named ax14 % A new axiom: (bl_valid ((bl_says admin) (bl_all (fun (F:individuals)=> (bl_all (fun (U:individuals)=> (bl_all (fun (CL:individuals)=> ((bl_impl ((bl_says system) (bl_atom ((system_file_needs_citizenship F) U)))) ((bl_impl (bl_atom ((admin_file_has_compartments F) CL))) ((bl_impl (bl_atom (((admin_file_has_citizenship_h F) U) CL))) (bl_atom ((admin_file_has_citizenship F) U))))))))))))) % FOF formula (bl_valid ((bl_says admin) (bl_all (fun (F:individuals)=> (bl_all (fun (U:individuals)=> (bl_atom (((admin_file_has_citizenship_h F) U) nil)))))))) of role axiom named ax15 % A new axiom: (bl_valid ((bl_says admin) (bl_all (fun (F:individuals)=> (bl_all (fun (U:individuals)=> (bl_atom (((admin_file_has_citizenship_h F) U) nil)))))))) % FOF formula (bl_valid ((bl_says admin) (bl_all (fun (F:individuals)=> (bl_all (fun (U:individuals)=> (bl_all (fun (C:individuals)=> (bl_all (fun (CL:individuals)=> (bl_all (fun (SSO:individuals)=> (bl_all (fun (SCG:individuals)=> ((bl_impl (bl_atom ((admin_compartment_has_sso C) SSO))) ((bl_impl (bl_atom ((admin_compartment_has_scg C) SCG))) ((bl_impl ((bl_says SSO) (bl_atom (((sso_file_has_citizenship F) U) SCG)))) ((bl_impl (bl_atom (((admin_file_has_citizenship_h F) U) CL))) (bl_atom (((admin_file_has_citizenship_h F) U) ((cons C) CL))))))))))))))))))))) of role axiom named ax16 % A new axiom: (bl_valid ((bl_says admin) (bl_all (fun (F:individuals)=> (bl_all (fun (U:individuals)=> (bl_all (fun (C:individuals)=> (bl_all (fun (CL:individuals)=> (bl_all (fun (SSO:individuals)=> (bl_all (fun (SCG:individuals)=> ((bl_impl (bl_atom ((admin_compartment_has_sso C) SSO))) ((bl_impl (bl_atom ((admin_compartment_has_scg C) SCG))) ((bl_impl ((bl_says SSO) (bl_atom (((sso_file_has_citizenship F) U) SCG)))) ((bl_impl (bl_atom (((admin_file_has_citizenship_h F) U) CL))) (bl_atom (((admin_file_has_citizenship_h F) U) ((cons C) CL))))))))))))))))))))) % FOF formula (bl_valid ((bl_says admin) (bl_all (fun (K:individuals)=> (bl_all (fun (PA:individuals)=> ((bl_impl ((bl_says system) (bl_atom (system_indi_is_polygraph_admin PA)))) ((bl_impl ((bl_says PA) (bl_atom (polygraph_admin_indi_has_polygraph K)))) (bl_atom (admin_indi_has_polygraph K)))))))))) of role axiom named ax17 % A new axiom: (bl_valid ((bl_says admin) (bl_all (fun (K:individuals)=> (bl_all (fun (PA:individuals)=> ((bl_impl ((bl_says system) (bl_atom (system_indi_is_polygraph_admin PA)))) ((bl_impl ((bl_says PA) (bl_atom (polygraph_admin_indi_has_polygraph K)))) (bl_atom (admin_indi_has_polygraph K)))))))))) % FOF formula (bl_valid ((bl_says admin) (bl_all (fun (K:individuals)=> (bl_all (fun (CA:individuals)=> ((bl_impl ((bl_says system) (bl_atom (system_indi_is_credit_admin CA)))) ((bl_impl ((bl_says CA) (bl_atom (credit_admin_indi_has_credit K)))) (bl_atom (admin_indi_has_credit K)))))))))) of role axiom named ax18 % A new axiom: (bl_valid ((bl_says admin) (bl_all (fun (K:individuals)=> (bl_all (fun (CA:individuals)=> ((bl_impl ((bl_says system) (bl_atom (system_indi_is_credit_admin CA)))) ((bl_impl ((bl_says CA) (bl_atom (credit_admin_indi_has_credit K)))) (bl_atom (admin_indi_has_credit K)))))))))) % FOF formula (bl_valid ((bl_says admin) (bl_all (fun (K:individuals)=> (bl_atom ((admin_indi_has_background K) unclassified)))))) of role axiom named ax19 % A new axiom: (bl_valid ((bl_says admin) (bl_all (fun (K:individuals)=> (bl_atom ((admin_indi_has_background K) unclassified)))))) % FOF formula (bl_valid ((bl_says admin) (bl_all (fun (K:individuals)=> (bl_all (fun (L:individuals)=> (bl_all (fun (BA:individuals)=> (bl_all (fun (L1:individuals)=> ((bl_impl ((bl_says system) (bl_atom (system_indi_is_background_admin BA)))) ((bl_impl ((bl_says BA) (bl_atom ((background_admin_indi_has_background K) L1)))) ((bl_impl (bl_atom ((loca_level_below L) L1))) (bl_atom ((admin_indi_has_background K) L))))))))))))))) of role axiom named ax20 % A new axiom: (bl_valid ((bl_says admin) (bl_all (fun (K:individuals)=> (bl_all (fun (L:individuals)=> (bl_all (fun (BA:individuals)=> (bl_all (fun (L1:individuals)=> ((bl_impl ((bl_says system) (bl_atom (system_indi_is_background_admin BA)))) ((bl_impl ((bl_says BA) (bl_atom ((background_admin_indi_has_background K) L1)))) ((bl_impl (bl_atom ((loca_level_below L) L1))) (bl_atom ((admin_indi_has_background K) L))))))))))))))) % FOF formula (bl_valid ((bl_says admin) (bl_all (fun (K:individuals)=> (bl_all (fun (HR:individuals)=> ((bl_impl ((bl_says system) (bl_atom (system_indi_is_hr_admin HR)))) ((bl_impl ((bl_says HR) (bl_atom (hr_admin_indi_has_employment K)))) (bl_atom (admin_indi_has_employment K)))))))))) of role axiom named ax21 % A new axiom: (bl_valid ((bl_says admin) (bl_all (fun (K:individuals)=> (bl_all (fun (HR:individuals)=> ((bl_impl ((bl_says system) (bl_atom (system_indi_is_hr_admin HR)))) ((bl_impl ((bl_says HR) (bl_atom (hr_admin_indi_has_employment K)))) (bl_atom (admin_indi_has_employment K)))))))))) % FOF formula (bl_valid ((bl_says admin) (bl_all (fun (K:individuals)=> (bl_atom ((admin_indi_has_citizenship K) anycountry)))))) of role axiom named ax22 % A new axiom: (bl_valid ((bl_says admin) (bl_all (fun (K:individuals)=> (bl_atom ((admin_indi_has_citizenship K) anycountry)))))) % FOF formula (bl_valid ((bl_says admin) (bl_all (fun (K:individuals)=> (bl_all (fun (U:individuals)=> ((bl_impl ((bl_says system) (bl_atom ((system_indi_has_citizenship K) U)))) (bl_atom ((admin_indi_has_citizenship K) U))))))))) of role axiom named ax23 % A new axiom: (bl_valid ((bl_says admin) (bl_all (fun (K:individuals)=> (bl_all (fun (U:individuals)=> ((bl_impl ((bl_says system) (bl_atom ((system_indi_has_citizenship K) U)))) (bl_atom ((admin_indi_has_citizenship K) U))))))))) % FOF formula (bl_valid ((bl_says admin) (bl_all (fun (K:individuals)=> (bl_atom ((admin_indi_has_level K) unclassified)))))) of role axiom named ax24 % A new axiom: (bl_valid ((bl_says admin) (bl_all (fun (K:individuals)=> (bl_atom ((admin_indi_has_level K) unclassified)))))) % FOF formula (bl_valid ((bl_says admin) (bl_all (fun (K:individuals)=> (bl_all (fun (L:individuals)=> (bl_all (fun (L1:individuals)=> (bl_all (fun (LA:individuals)=> (bl_all (fun (L11:individuals)=> ((bl_impl ((bl_says system) (bl_atom ((system_indi_needs_level K) L1)))) ((bl_impl (bl_atom ((admin_indi_has_citizenship K) usa))) ((bl_impl (bl_atom (admin_indi_has_polygraph K))) ((bl_impl (bl_atom (admin_indi_has_employment K))) ((bl_impl (bl_atom (admin_indi_has_credit K))) ((bl_impl (bl_atom ((loca_level_below L) L1))) ((bl_impl ((bl_says system) (bl_atom (system_indi_is_level_admin LA)))) ((bl_impl ((bl_says LA) (bl_atom ((level_admin_indi_has_level K) L11)))) ((bl_impl (bl_atom ((loca_level_below L) L11))) ((bl_impl (bl_atom ((admin_indi_has_background K) L))) (bl_atom ((admin_indi_has_level K) L)))))))))))))))))))))))) of role axiom named ax25 % A new axiom: (bl_valid ((bl_says admin) (bl_all (fun (K:individuals)=> (bl_all (fun (L:individuals)=> (bl_all (fun (L1:individuals)=> (bl_all (fun (LA:individuals)=> (bl_all (fun (L11:individuals)=> ((bl_impl ((bl_says system) (bl_atom ((system_indi_needs_level K) L1)))) ((bl_impl (bl_atom ((admin_indi_has_citizenship K) usa))) ((bl_impl (bl_atom (admin_indi_has_polygraph K))) ((bl_impl (bl_atom (admin_indi_has_employment K))) ((bl_impl (bl_atom (admin_indi_has_credit K))) ((bl_impl (bl_atom ((loca_level_below L) L1))) ((bl_impl ((bl_says system) (bl_atom (system_indi_is_level_admin LA)))) ((bl_impl ((bl_says LA) (bl_atom ((level_admin_indi_has_level K) L11)))) ((bl_impl (bl_atom ((loca_level_below L) L11))) ((bl_impl (bl_atom ((admin_indi_has_background K) L))) (bl_atom ((admin_indi_has_level K) L)))))))))))))))))))))))) % FOF formula (bl_valid ((bl_says admin) (bl_all (fun (K:individuals)=> (bl_atom ((admin_indi_has_compartments K) nil)))))) of role axiom named ax26 % A new axiom: (bl_valid ((bl_says admin) (bl_all (fun (K:individuals)=> (bl_atom ((admin_indi_has_compartments K) nil)))))) % FOF formula (bl_valid ((bl_says admin) (bl_all (fun (K:individuals)=> (bl_all (fun (C:individuals)=> (bl_all (fun (CL:individuals)=> (bl_all (fun (SSO:individuals)=> ((bl_impl ((bl_says system) (bl_atom ((system_indi_needs_compartment K) C)))) ((bl_impl (bl_atom (admin_indi_has_employment K))) ((bl_impl (bl_atom ((admin_indi_has_citizenship K) usa))) ((bl_impl (bl_atom ((admin_indi_has_polygraph_for_compartment K) C))) ((bl_impl (bl_atom ((admin_indi_has_credit_for_compartment K) C))) ((bl_impl (bl_atom ((admin_compartment_has_sso C) SSO))) ((bl_impl ((bl_says SSO) (bl_atom ((sso_indi_has_compartment K) C)))) ((bl_impl (bl_atom ((admin_indi_has_background_for_compartment K) C))) ((bl_impl (bl_atom ((admin_indi_has_level_for_compartment K) C))) ((bl_impl (bl_atom ((admin_indi_has_compartments K) CL))) (bl_atom ((admin_indi_has_compartments K) ((cons C) CL))))))))))))))))))))))) of role axiom named ax27 % A new axiom: (bl_valid ((bl_says admin) (bl_all (fun (K:individuals)=> (bl_all (fun (C:individuals)=> (bl_all (fun (CL:individuals)=> (bl_all (fun (SSO:individuals)=> ((bl_impl ((bl_says system) (bl_atom ((system_indi_needs_compartment K) C)))) ((bl_impl (bl_atom (admin_indi_has_employment K))) ((bl_impl (bl_atom ((admin_indi_has_citizenship K) usa))) ((bl_impl (bl_atom ((admin_indi_has_polygraph_for_compartment K) C))) ((bl_impl (bl_atom ((admin_indi_has_credit_for_compartment K) C))) ((bl_impl (bl_atom ((admin_compartment_has_sso C) SSO))) ((bl_impl ((bl_says SSO) (bl_atom ((sso_indi_has_compartment K) C)))) ((bl_impl (bl_atom ((admin_indi_has_background_for_compartment K) C))) ((bl_impl (bl_atom ((admin_indi_has_level_for_compartment K) C))) ((bl_impl (bl_atom ((admin_indi_has_compartments K) CL))) (bl_atom ((admin_indi_has_compartments K) ((cons C) CL))))))))))))))))))))))) % FOF formula (bl_valid ((bl_says admin) (bl_all (fun (K:individuals)=> (bl_all (fun (C:individuals)=> (bl_all (fun (OCA:individuals)=> (bl_all (fun (L1:individuals)=> (bl_all (fun (L2:individuals)=> (bl_all (fun (B1:individuals)=> (bl_all (fun (B2:individuals)=> ((bl_impl ((bl_says system) (bl_atom (system_indi_is_oca OCA)))) ((bl_impl ((bl_says OCA) (bl_atom (((((oca_compartment_is_compartment C) L1) L2) B1) B2)))) ((bl_impl (bl_atom ((admin_indi_has_background K) L2))) (bl_atom ((admin_indi_has_background_for_compartment K) C))))))))))))))))))))) of role axiom named ax28 % A new axiom: (bl_valid ((bl_says admin) (bl_all (fun (K:individuals)=> (bl_all (fun (C:individuals)=> (bl_all (fun (OCA:individuals)=> (bl_all (fun (L1:individuals)=> (bl_all (fun (L2:individuals)=> (bl_all (fun (B1:individuals)=> (bl_all (fun (B2:individuals)=> ((bl_impl ((bl_says system) (bl_atom (system_indi_is_oca OCA)))) ((bl_impl ((bl_says OCA) (bl_atom (((((oca_compartment_is_compartment C) L1) L2) B1) B2)))) ((bl_impl (bl_atom ((admin_indi_has_background K) L2))) (bl_atom ((admin_indi_has_background_for_compartment K) C))))))))))))))))))))) % FOF formula (bl_valid ((bl_says admin) (bl_all (fun (K:individuals)=> (bl_all (fun (C:individuals)=> (bl_all (fun (OCA:individuals)=> (bl_all (fun (L1:individuals)=> (bl_all (fun (L2:individuals)=> (bl_all (fun (B1:individuals)=> (bl_all (fun (B2:individuals)=> ((bl_impl ((bl_says system) (bl_atom (system_indi_is_oca OCA)))) ((bl_impl ((bl_says OCA) (bl_atom (((((oca_compartment_is_compartment C) L1) L2) B1) B2)))) ((bl_impl (bl_atom ((admin_indi_has_level K) L1))) (bl_atom ((admin_indi_has_level_for_compartment K) C))))))))))))))))))))) of role axiom named ax29 % A new axiom: (bl_valid ((bl_says admin) (bl_all (fun (K:individuals)=> (bl_all (fun (C:individuals)=> (bl_all (fun (OCA:individuals)=> (bl_all (fun (L1:individuals)=> (bl_all (fun (L2:individuals)=> (bl_all (fun (B1:individuals)=> (bl_all (fun (B2:individuals)=> ((bl_impl ((bl_says system) (bl_atom (system_indi_is_oca OCA)))) ((bl_impl ((bl_says OCA) (bl_atom (((((oca_compartment_is_compartment C) L1) L2) B1) B2)))) ((bl_impl (bl_atom ((admin_indi_has_level K) L1))) (bl_atom ((admin_indi_has_level_for_compartment K) C))))))))))))))))))))) % FOF formula (bl_valid ((bl_says admin) (bl_all (fun (K:individuals)=> (bl_all (fun (C:individuals)=> (bl_all (fun (OCA:individuals)=> (bl_all (fun (L1:individuals)=> (bl_all (fun (L2:individuals)=> (bl_all (fun (B1:individuals)=> ((bl_impl ((bl_says system) (bl_atom (system_indi_is_oca OCA)))) ((bl_impl ((bl_says OCA) (bl_atom (((((oca_compartment_is_compartment C) L1) L2) B1) yes)))) ((bl_impl (bl_atom (admin_indi_has_polygraph K))) (bl_atom ((admin_indi_has_polygraph_for_compartment K) C))))))))))))))))))) of role axiom named ax30 % A new axiom: (bl_valid ((bl_says admin) (bl_all (fun (K:individuals)=> (bl_all (fun (C:individuals)=> (bl_all (fun (OCA:individuals)=> (bl_all (fun (L1:individuals)=> (bl_all (fun (L2:individuals)=> (bl_all (fun (B1:individuals)=> ((bl_impl ((bl_says system) (bl_atom (system_indi_is_oca OCA)))) ((bl_impl ((bl_says OCA) (bl_atom (((((oca_compartment_is_compartment C) L1) L2) B1) yes)))) ((bl_impl (bl_atom (admin_indi_has_polygraph K))) (bl_atom ((admin_indi_has_polygraph_for_compartment K) C))))))))))))))))))) % FOF formula (bl_valid ((bl_says admin) (bl_all (fun (K:individuals)=> (bl_all (fun (C:individuals)=> (bl_all (fun (OCA:individuals)=> (bl_all (fun (L1:individuals)=> (bl_all (fun (L2:individuals)=> (bl_all (fun (B1:individuals)=> ((bl_impl ((bl_says system) (bl_atom (system_indi_is_oca OCA)))) ((bl_impl ((bl_says OCA) (bl_atom (((((oca_compartment_is_compartment C) L1) L2) B1) no)))) (bl_atom ((admin_indi_has_polygraph_for_compartment K) C)))))))))))))))))) of role axiom named ax31 % A new axiom: (bl_valid ((bl_says admin) (bl_all (fun (K:individuals)=> (bl_all (fun (C:individuals)=> (bl_all (fun (OCA:individuals)=> (bl_all (fun (L1:individuals)=> (bl_all (fun (L2:individuals)=> (bl_all (fun (B1:individuals)=> ((bl_impl ((bl_says system) (bl_atom (system_indi_is_oca OCA)))) ((bl_impl ((bl_says OCA) (bl_atom (((((oca_compartment_is_compartment C) L1) L2) B1) no)))) (bl_atom ((admin_indi_has_polygraph_for_compartment K) C)))))))))))))))))) % FOF formula (bl_valid ((bl_says admin) (bl_all (fun (K:individuals)=> (bl_all (fun (C:individuals)=> (bl_all (fun (OCA:individuals)=> (bl_all (fun (L1:individuals)=> (bl_all (fun (L2:individuals)=> (bl_all (fun (B2:individuals)=> ((bl_impl ((bl_says system) (bl_atom (system_indi_is_oca OCA)))) ((bl_impl ((bl_says OCA) (bl_atom (((((oca_compartment_is_compartment C) L1) L2) yes) B2)))) ((bl_impl (bl_atom (admin_indi_has_credit K))) (bl_atom ((admin_indi_has_credit_for_compartment K) C))))))))))))))))))) of role axiom named ax32 % A new axiom: (bl_valid ((bl_says admin) (bl_all (fun (K:individuals)=> (bl_all (fun (C:individuals)=> (bl_all (fun (OCA:individuals)=> (bl_all (fun (L1:individuals)=> (bl_all (fun (L2:individuals)=> (bl_all (fun (B2:individuals)=> ((bl_impl ((bl_says system) (bl_atom (system_indi_is_oca OCA)))) ((bl_impl ((bl_says OCA) (bl_atom (((((oca_compartment_is_compartment C) L1) L2) yes) B2)))) ((bl_impl (bl_atom (admin_indi_has_credit K))) (bl_atom ((admin_indi_has_credit_for_compartment K) C))))))))))))))))))) % FOF formula (bl_valid ((bl_says admin) (bl_all (fun (K:individuals)=> (bl_all (fun (C:individuals)=> (bl_all (fun (OCA:individuals)=> (bl_all (fun (L1:individuals)=> (bl_all (fun (L2:individuals)=> (bl_all (fun (B2:individuals)=> ((bl_impl ((bl_says system) (bl_atom (system_indi_is_oca OCA)))) ((bl_impl ((bl_says OCA) (bl_atom (((((oca_compartment_is_compartment C) L1) L2) no) B2)))) (bl_atom ((admin_indi_has_credit_for_compartment K) C)))))))))))))))))) of role axiom named ax33 % A new axiom: (bl_valid ((bl_says admin) (bl_all (fun (K:individuals)=> (bl_all (fun (C:individuals)=> (bl_all (fun (OCA:individuals)=> (bl_all (fun (L1:individuals)=> (bl_all (fun (L2:individuals)=> (bl_all (fun (B2:individuals)=> ((bl_impl ((bl_says system) (bl_atom (system_indi_is_oca OCA)))) ((bl_impl ((bl_says OCA) (bl_atom (((((oca_compartment_is_compartment C) L1) L2) no) B2)))) (bl_atom ((admin_indi_has_credit_for_compartment K) C)))))))))))))))))) % FOF formula (bl_valid ((bl_says admin) (bl_all (fun (K:individuals)=> (bl_all (fun (F:individuals)=> (bl_all (fun (CL:individuals)=> ((bl_impl (bl_atom ((admin_file_has_compartments F) CL))) ((bl_impl (bl_atom ((admin_indi_has_compartments K) CL))) (bl_atom ((admin_indi_has_compartments_for_file K) F)))))))))))) of role axiom named ax34 % A new axiom: (bl_valid ((bl_says admin) (bl_all (fun (K:individuals)=> (bl_all (fun (F:individuals)=> (bl_all (fun (CL:individuals)=> ((bl_impl (bl_atom ((admin_file_has_compartments F) CL))) ((bl_impl (bl_atom ((admin_indi_has_compartments K) CL))) (bl_atom ((admin_indi_has_compartments_for_file K) F)))))))))))) % FOF formula (bl_valid ((bl_says admin) (bl_all (fun (K:individuals)=> (bl_all (fun (F:individuals)=> (bl_all (fun (L:individuals)=> ((bl_impl (bl_atom ((admin_file_has_level F) L))) ((bl_impl (bl_atom ((admin_indi_has_level K) L))) (bl_atom ((admin_indi_has_level_for_file K) F)))))))))))) of role axiom named ax35 % A new axiom: (bl_valid ((bl_says admin) (bl_all (fun (K:individuals)=> (bl_all (fun (F:individuals)=> (bl_all (fun (L:individuals)=> ((bl_impl (bl_atom ((admin_file_has_level F) L))) ((bl_impl (bl_atom ((admin_indi_has_level K) L))) (bl_atom ((admin_indi_has_level_for_file K) F)))))))))))) % FOF formula (bl_valid ((bl_says admin) (bl_all (fun (K:individuals)=> (bl_all (fun (F:individuals)=> (bl_all (fun (O:individuals)=> ((bl_impl ((bl_says loca) (bl_atom ((p_owner F) O)))) ((bl_impl ((bl_says O) (bl_atom ((owner_indi_has_need_to_know K) F)))) (bl_atom ((admin_indi_has_need_to_know_for_file K) F)))))))))))) of role axiom named ax36 % A new axiom: (bl_valid ((bl_says admin) (bl_all (fun (K:individuals)=> (bl_all (fun (F:individuals)=> (bl_all (fun (O:individuals)=> ((bl_impl ((bl_says loca) (bl_atom ((p_owner F) O)))) ((bl_impl ((bl_says O) (bl_atom ((owner_indi_has_need_to_know K) F)))) (bl_atom ((admin_indi_has_need_to_know_for_file K) F)))))))))))) % FOF formula (bl_valid ((bl_says admin) (bl_all (fun (K:individuals)=> (bl_all (fun (F:individuals)=> (bl_all (fun (L:individuals)=> ((bl_impl (bl_atom ((admin_file_has_citizenship F) L))) ((bl_impl (bl_atom ((admin_indi_has_citizenship K) L))) (bl_atom ((admin_indi_has_citizenship_for_file K) F)))))))))))) of role axiom named ax37 % A new axiom: (bl_valid ((bl_says admin) (bl_all (fun (K:individuals)=> (bl_all (fun (F:individuals)=> (bl_all (fun (L:individuals)=> ((bl_impl (bl_atom ((admin_file_has_citizenship F) L))) ((bl_impl (bl_atom ((admin_indi_has_citizenship K) L))) (bl_atom ((admin_indi_has_citizenship_for_file K) F)))))))))))) % FOF formula (bl_valid ((bl_says admin) (bl_all (fun (K:individuals)=> (bl_all (fun (F:individuals)=> ((bl_impl (bl_atom ((admin_indi_has_citizenship K) usa))) (bl_atom ((admin_indi_has_citizenship_for_file K) F))))))))) of role axiom named ax38 % A new axiom: (bl_valid ((bl_says admin) (bl_all (fun (K:individuals)=> (bl_all (fun (F:individuals)=> ((bl_impl (bl_atom ((admin_indi_has_citizenship K) usa))) (bl_atom ((admin_indi_has_citizenship_for_file K) F))))))))) % FOF formula (bl_valid ((bl_says admin) (bl_all (fun (K:individuals)=> (bl_all (fun (F:individuals)=> ((bl_impl ((bl_says loca) (bl_atom (((p_has_xattr F) is_working_paper) yes)))) ((bl_impl ((bl_says loca) (bl_atom ((p_owner F) K)))) ((bl_impl (bl_atom (admin_file_has_not_expired F))) (bl_atom (((may K) F) read))))))))))) of role axiom named ax39 % A new axiom: (bl_valid ((bl_says admin) (bl_all (fun (K:individuals)=> (bl_all (fun (F:individuals)=> ((bl_impl ((bl_says loca) (bl_atom (((p_has_xattr F) is_working_paper) yes)))) ((bl_impl ((bl_says loca) (bl_atom ((p_owner F) K)))) ((bl_impl (bl_atom (admin_file_has_not_expired F))) (bl_atom (((may K) F) read))))))))))) % FOF formula (bl_valid ((bl_says admin) (bl_all (fun (K:individuals)=> (bl_all (fun (F:individuals)=> ((bl_impl ((bl_says loca) (bl_atom (((p_has_xattr F) is_not_working_paper) yes)))) ((bl_impl (bl_atom ((admin_indi_has_citizenship_for_file K) F))) ((bl_impl (bl_atom ((admin_indi_has_need_to_know_for_file K) F))) ((bl_impl (bl_atom ((admin_indi_has_level_for_file K) F))) ((bl_impl (bl_atom ((admin_indi_has_compartments_for_file K) F))) (bl_atom (((may K) F) read))))))))))))) of role axiom named ax40 % A new axiom: (bl_valid ((bl_says admin) (bl_all (fun (K:individuals)=> (bl_all (fun (F:individuals)=> ((bl_impl ((bl_says loca) (bl_atom (((p_has_xattr F) is_not_working_paper) yes)))) ((bl_impl (bl_atom ((admin_indi_has_citizenship_for_file K) F))) ((bl_impl (bl_atom ((admin_indi_has_need_to_know_for_file K) F))) ((bl_impl (bl_atom ((admin_indi_has_level_for_file K) F))) ((bl_impl (bl_atom ((admin_indi_has_compartments_for_file K) F))) (bl_atom (((may K) F) read))))))))))))) % FOF formula (bl_valid ((bl_says admin) (bl_all (fun (K:individuals)=> (bl_all (fun (F:individuals)=> (bl_all (fun (K1:individuals)=> ((bl_impl ((bl_says loca) (bl_atom ((p_owner F) K1)))) ((bl_impl ((bl_says system) (bl_atom ((system_indi_is_counterintelligence K) K1)))) (bl_atom (((may K) F) read)))))))))))) of role axiom named ax41 % A new axiom: (bl_valid ((bl_says admin) (bl_all (fun (K:individuals)=> (bl_all (fun (F:individuals)=> (bl_all (fun (K1:individuals)=> ((bl_impl ((bl_says loca) (bl_atom ((p_owner F) K1)))) ((bl_impl ((bl_says system) (bl_atom ((system_indi_is_counterintelligence K) K1)))) (bl_atom (((may K) F) read)))))))))))) % FOF formula (bl_valid ((bl_says system) (bl_atom (system_indi_is_oca oca)))) of role axiom named ax42 % A new axiom: (bl_valid ((bl_says system) (bl_atom (system_indi_is_oca oca)))) % FOF formula (bl_valid ((bl_says system) (bl_atom ((system_compartment_has_sso compartmentb) sso_compartmentb)))) of role axiom named ax43 % A new axiom: (bl_valid ((bl_says system) (bl_atom ((system_compartment_has_sso compartmentb) sso_compartmentb)))) % FOF formula (bl_valid ((bl_says oca) (bl_atom ((oca_compartment_has_scg compartmentb) scg_compartmentb)))) of role axiom named ax44 % A new axiom: (bl_valid ((bl_says oca) (bl_atom ((oca_compartment_has_scg compartmentb) scg_compartmentb)))) % FOF formula (bl_valid ((bl_says sso_compartmentb) (bl_atom ((sso_compartment_has_scg compartmentb) scg_compartmentb)))) of role axiom named ax45 % A new axiom: (bl_valid ((bl_says sso_compartmentb) (bl_atom ((sso_compartment_has_scg compartmentb) scg_compartmentb)))) % FOF formula (bl_valid ((bl_says system) (bl_atom ((system_compartment_has_sso compartmenta) sso_compartmenta)))) of role axiom named ax46 % A new axiom: (bl_valid ((bl_says system) (bl_atom ((system_compartment_has_sso compartmenta) sso_compartmenta)))) % FOF formula (bl_valid ((bl_says oca) (bl_atom ((oca_compartment_has_scg compartmenta) scg_compartmenta)))) of role axiom named ax47 % A new axiom: (bl_valid ((bl_says oca) (bl_atom ((oca_compartment_has_scg compartmenta) scg_compartmenta)))) % FOF formula (bl_valid ((bl_says sso_compartmenta) (bl_atom ((sso_compartment_has_scg compartmenta) scg_compartmenta)))) of role axiom named ax48 % A new axiom: (bl_valid ((bl_says sso_compartmenta) (bl_atom ((sso_compartment_has_scg compartmenta) scg_compartmenta)))) % FOF formula (bl_valid ((bl_says loca) (bl_atom (((p_has_xattr secretfile) is_not_working_paper) yes)))) of role axiom named ax49 % A new axiom: (bl_valid ((bl_says loca) (bl_atom (((p_has_xattr secretfile) is_not_working_paper) yes)))) % FOF formula (bl_valid ((bl_says system) (bl_atom ((system_file_needs_compartments secretfile) ((cons compartmentb) ((cons compartmenta) nil)))))) of role axiom named ax50 % A new axiom: (bl_valid ((bl_says system) (bl_atom ((system_file_needs_compartments secretfile) ((cons compartmentb) ((cons compartmenta) nil)))))) % FOF formula (bl_valid ((bl_says sso_compartmentb) (bl_atom ((sso_file_has_compartments secretfile) ((cons compartmentb) ((cons compartmenta) nil)))))) of role axiom named ax51 % A new axiom: (bl_valid ((bl_says sso_compartmentb) (bl_atom ((sso_file_has_compartments secretfile) ((cons compartmentb) ((cons compartmenta) nil)))))) % FOF formula (bl_valid ((bl_says sso_compartmenta) (bl_atom ((sso_file_has_compartments secretfile) ((cons compartmentb) ((cons compartmenta) nil)))))) of role axiom named ax52 % A new axiom: (bl_valid ((bl_says sso_compartmenta) (bl_atom ((sso_file_has_compartments secretfile) ((cons compartmentb) ((cons compartmenta) nil)))))) % FOF formula (bl_valid ((bl_says loca) (bl_atom (((p_has_xattr not_secretfile) is_not_working_paper) yes)))) of role axiom named ax53 % A new axiom: (bl_valid ((bl_says loca) (bl_atom (((p_has_xattr not_secretfile) is_not_working_paper) yes)))) % FOF formula (bl_valid ((bl_says system) (bl_atom ((system_file_needs_compartments not_secretfile) nil)))) of role axiom named ax54 % A new axiom: (bl_valid ((bl_says system) (bl_atom ((system_file_needs_compartments not_secretfile) nil)))) % FOF formula (bl_valid ((bl_says system) (bl_atom ((system_file_needs_level secretfile) secret)))) of role axiom named ax55 % A new axiom: (bl_valid ((bl_says system) (bl_atom ((system_file_needs_level secretfile) secret)))) % FOF formula (bl_valid ((bl_says sso_compartmentb) (bl_atom (((sso_file_has_level secretfile) secret) scg_compartmentb)))) of role axiom named ax56 % A new axiom: (bl_valid ((bl_says sso_compartmentb) (bl_atom (((sso_file_has_level secretfile) secret) scg_compartmentb)))) % FOF formula (bl_valid ((bl_says sso_compartmenta) (bl_atom (((sso_file_has_level secretfile) secret) scg_compartmenta)))) of role axiom named ax57 % A new axiom: (bl_valid ((bl_says sso_compartmenta) (bl_atom (((sso_file_has_level secretfile) secret) scg_compartmenta)))) % FOF formula (bl_valid ((bl_says system) (bl_atom ((system_file_needs_level not_secretfile) unclassified)))) of role axiom named ax58 % A new axiom: (bl_valid ((bl_says system) (bl_atom ((system_file_needs_level not_secretfile) unclassified)))) % FOF formula (bl_valid ((bl_says system) (bl_atom ((system_file_needs_citizenship secretfile) usa)))) of role axiom named ax59 % A new axiom: (bl_valid ((bl_says system) (bl_atom ((system_file_needs_citizenship secretfile) usa)))) % FOF formula (bl_valid ((bl_says sso_compartmentb) (bl_atom (((sso_file_has_citizenship secretfile) usa) scg_compartmentb)))) of role axiom named ax60 % A new axiom: (bl_valid ((bl_says sso_compartmentb) (bl_atom (((sso_file_has_citizenship secretfile) usa) scg_compartmentb)))) % FOF formula (bl_valid ((bl_says sso_compartmenta) (bl_atom (((sso_file_has_citizenship secretfile) usa) scg_compartmenta)))) of role axiom named ax61 % A new axiom: (bl_valid ((bl_says sso_compartmenta) (bl_atom (((sso_file_has_citizenship secretfile) usa) scg_compartmenta)))) % FOF formula (bl_valid ((bl_says system) (bl_atom ((system_file_needs_citizenship not_secretfile) anycountry)))) of role axiom named ax62 % A new axiom: (bl_valid ((bl_says system) (bl_atom ((system_file_needs_citizenship not_secretfile) anycountry)))) % FOF formula (bl_valid ((bl_says system) (bl_atom ((system_indi_has_citizenship alice) usa)))) of role axiom named ax63 % A new axiom: (bl_valid ((bl_says system) (bl_atom ((system_indi_has_citizenship alice) usa)))) % FOF formula (bl_valid ((bl_says system) (bl_atom ((system_indi_has_citizenship babu) india)))) of role axiom named ax64 % A new axiom: (bl_valid ((bl_says system) (bl_atom ((system_indi_has_citizenship babu) india)))) % FOF formula (bl_valid ((bl_says system) (bl_atom (system_indi_is_polygraph_admin polygraph_admin)))) of role axiom named ax65 % A new axiom: (bl_valid ((bl_says system) (bl_atom (system_indi_is_polygraph_admin polygraph_admin)))) % FOF formula (bl_valid ((bl_says system) (bl_atom (system_indi_is_credit_admin credit_admin)))) of role axiom named ax66 % A new axiom: (bl_valid ((bl_says system) (bl_atom (system_indi_is_credit_admin credit_admin)))) % FOF formula (bl_valid ((bl_says system) (bl_atom (system_indi_is_background_admin background_admin)))) of role axiom named ax67 % A new axiom: (bl_valid ((bl_says system) (bl_atom (system_indi_is_background_admin background_admin)))) % FOF formula (bl_valid ((bl_says system) (bl_atom (system_indi_is_hr_admin hr_admin)))) of role axiom named ax68 % A new axiom: (bl_valid ((bl_says system) (bl_atom (system_indi_is_hr_admin hr_admin)))) % FOF formula (bl_valid ((bl_says polygraph_admin) (bl_atom (polygraph_admin_indi_has_polygraph alice)))) of role axiom named ax69 % A new axiom: (bl_valid ((bl_says polygraph_admin) (bl_atom (polygraph_admin_indi_has_polygraph alice)))) % FOF formula (bl_valid ((bl_says credit_admin) (bl_atom (credit_admin_indi_has_credit alice)))) of role axiom named ax70 % A new axiom: (bl_valid ((bl_says credit_admin) (bl_atom (credit_admin_indi_has_credit alice)))) % FOF formula (bl_valid ((bl_says background_admin) (bl_atom ((background_admin_indi_has_background alice) topsecret)))) of role axiom named ax71 % A new axiom: (bl_valid ((bl_says background_admin) (bl_atom ((background_admin_indi_has_background alice) topsecret)))) % FOF formula (bl_valid ((bl_says hr_admin) (bl_atom (hr_admin_indi_has_employment alice)))) of role axiom named ax72 % A new axiom: (bl_valid ((bl_says hr_admin) (bl_atom (hr_admin_indi_has_employment alice)))) % FOF formula (bl_valid ((bl_says system) (bl_atom (system_indi_is_level_admin level_admin)))) of role axiom named ax73 % A new axiom: (bl_valid ((bl_says system) (bl_atom (system_indi_is_level_admin level_admin)))) % FOF formula (bl_valid ((bl_says system) (bl_atom ((system_indi_needs_level alice) secret)))) of role axiom named ax74 % A new axiom: (bl_valid ((bl_says system) (bl_atom ((system_indi_needs_level alice) secret)))) % FOF formula (bl_valid ((bl_says level_admin) (bl_atom ((level_admin_indi_has_level alice) topsecret)))) of role axiom named ax75 % A new axiom: (bl_valid ((bl_says level_admin) (bl_atom ((level_admin_indi_has_level alice) topsecret)))) % FOF formula (bl_valid ((bl_says system) (bl_atom ((system_indi_needs_compartment alice) compartmentb)))) of role axiom named ax76 % A new axiom: (bl_valid ((bl_says system) (bl_atom ((system_indi_needs_compartment alice) compartmentb)))) % FOF formula (bl_valid ((bl_says system) (bl_atom ((system_indi_needs_compartment alice) compartmenta)))) of role axiom named ax77 % A new axiom: (bl_valid ((bl_says system) (bl_atom ((system_indi_needs_compartment alice) compartmenta)))) % FOF formula (bl_valid ((bl_says sso_compartmentb) (bl_atom ((sso_indi_has_compartment alice) compartmentb)))) of role axiom named ax78 % A new axiom: (bl_valid ((bl_says sso_compartmentb) (bl_atom ((sso_indi_has_compartment alice) compartmentb)))) % FOF formula (bl_valid ((bl_says sso_compartmenta) (bl_atom ((sso_indi_has_compartment alice) compartmenta)))) of role axiom named ax79 % A new axiom: (bl_valid ((bl_says sso_compartmenta) (bl_atom ((sso_indi_has_compartment alice) compartmenta)))) % FOF formula (bl_valid ((bl_says oca) (bl_atom (((((oca_compartment_is_compartment compartmentb) confidential) topsecret) yes) yes)))) of role axiom named ax80 % A new axiom: (bl_valid ((bl_says oca) (bl_atom (((((oca_compartment_is_compartment compartmentb) confidential) topsecret) yes) yes)))) % FOF formula (bl_valid ((bl_says oca) (bl_atom (((((oca_compartment_is_compartment compartmenta) sbu) unclassified) no) no)))) of role axiom named ax81 % A new axiom: (bl_valid ((bl_says oca) (bl_atom (((((oca_compartment_is_compartment compartmenta) sbu) unclassified) no) no)))) % FOF formula (bl_valid ((bl_says loca) (bl_atom ((p_owner secretfile) owner_secretfile)))) of role axiom named ax82 % A new axiom: (bl_valid ((bl_says loca) (bl_atom ((p_owner secretfile) owner_secretfile)))) % FOF formula (bl_valid ((bl_says loca) (bl_atom ((p_owner not_secretfile) owner_not_secretfile)))) of role axiom named ax83 % A new axiom: (bl_valid ((bl_says loca) (bl_atom ((p_owner not_secretfile) owner_not_secretfile)))) % FOF formula (bl_valid ((bl_says owner_secretfile) (bl_atom ((owner_indi_has_need_to_know alice) secretfile)))) of role axiom named ax84 % A new axiom: (bl_valid ((bl_says owner_secretfile) (bl_atom ((owner_indi_has_need_to_know alice) secretfile)))) % FOF formula (bl_valid ((bl_says owner_not_secretfile) (bl_atom ((owner_indi_has_need_to_know alice) not_secretfile)))) of role axiom named ax85 % A new axiom: (bl_valid ((bl_says owner_not_secretfile) (bl_atom ((owner_indi_has_need_to_know alice) not_secretfile)))) % FOF formula (bl_valid ((bl_says owner_not_secretfile) (bl_atom ((owner_indi_has_need_to_know babu) not_secretfile)))) of role axiom named ax86 % A new axiom: (bl_valid ((bl_says owner_not_secretfile) (bl_atom ((owner_indi_has_need_to_know babu) not_secretfile)))) % FOF formula (bl_valid ((bl_says system) (bl_atom ((system_indi_is_counterintelligence ci) alice)))) of role axiom named ax87 % A new axiom: (bl_valid ((bl_says system) (bl_atom ((system_indi_is_counterintelligence ci) alice)))) % FOF formula (bl_valid ((bl_says admin) (bl_atom (((may babu) not_secretfile) read)))) of role conjecture named babureadnotsecret % Conjecture to prove = (bl_valid ((bl_says admin) (bl_atom (((may babu) not_secretfile) read)))):Prop % We need to prove ['(bl_valid ((bl_says admin) (bl_atom (((may babu) not_secretfile) read))))'] % Parameter fofType:Type. % Parameter current_world:fofType. % Parameter prop_a:(fofType->Prop). % Parameter prop_b:(fofType->Prop). % Parameter prop_c:(fofType->Prop). % Definition mfalse:=(fun (X:fofType)=> False):(fofType->Prop). % Definition mtrue:=(fun (X:fofType)=> True):(fofType->Prop). % Definition mnot:=(fun (X:(fofType->Prop)) (U:fofType)=> ((X U)->False)):((fofType->Prop)->(fofType->Prop)). % Definition mor:=(fun (X:(fofType->Prop)) (Y:(fofType->Prop)) (U:fofType)=> ((or (X U)) (Y U))):((fofType->Prop)->((fofType->Prop)->(fofType->Prop))). % Definition mand:=(fun (X:(fofType->Prop)) (Y:(fofType->Prop)) (U:fofType)=> ((and (X U)) (Y U))):((fofType->Prop)->((fofType->Prop)->(fofType->Prop))). % Definition mimpl:=(fun (U:(fofType->Prop)) (V:(fofType->Prop))=> ((mor (mnot U)) V)):((fofType->Prop)->((fofType->Prop)->(fofType->Prop))). % Definition miff:=(fun (U:(fofType->Prop)) (V:(fofType->Prop))=> ((mand ((mimpl U) V)) ((mimpl V) U))):((fofType->Prop)->((fofType->Prop)->(fofType->Prop))). % Definition mbox:=(fun (R:(fofType->(fofType->Prop))) (P:(fofType->Prop)) (X:fofType)=> (forall (Y:fofType), (((R X) Y)->(P Y)))):((fofType->(fofType->Prop))->((fofType->Prop)->(fofType->Prop))). % Definition mdia:=(fun (R:(fofType->(fofType->Prop))) (P:(fofType->Prop)) (X:fofType)=> ((ex fofType) (fun (Y:fofType)=> ((and ((R X) Y)) (P Y))))):((fofType->(fofType->Prop))->((fofType->Prop)->(fofType->Prop))). % Parameter individuals:Type. % Definition mall:=(fun (P:(individuals->(fofType->Prop))) (W:fofType)=> (forall (X:individuals), ((P X) W))):((individuals->(fofType->Prop))->(fofType->Prop)). % Definition mexists:=(fun (P:(individuals->(fofType->Prop))) (W:fofType)=> ((ex individuals) (fun (X:individuals)=> ((P X) W)))):((individuals->(fofType->Prop))->(fofType->Prop)). % Definition mvalid:=(fun (P:(fofType->Prop))=> (forall (W:fofType), (P W))):((fofType->Prop)->Prop). % Definition msatisfiable:=(fun (P:(fofType->Prop))=> ((ex fofType) (fun (W:fofType)=> (P W)))):((fofType->Prop)->Prop). % Definition mcountersatisfiable:=(fun (P:(fofType->Prop))=> ((ex fofType) (fun (W:fofType)=> ((P W)->False)))):((fofType->Prop)->Prop). % Definition minvalid:=(fun (P:(fofType->Prop))=> (forall (W:fofType), ((P W)->False))):((fofType->Prop)->Prop). % Parameter reli:(fofType->(fofType->Prop)). % Parameter relr:(fofType->(fofType->Prop)). % Definition cs4_atom:=(fun (P:(fofType->Prop))=> ((mbox reli) P)):((fofType->Prop)->(fofType->Prop)). % Definition cs4_and:=(fun (A:(fofType->Prop)) (B:(fofType->Prop))=> ((mand A) B)):((fofType->Prop)->((fofType->Prop)->(fofType->Prop))). % Definition cs4_or:=(fun (A:(fofType->Prop)) (B:(fofType->Prop))=> ((mor A) B)):((fofType->Prop)->((fofType->Prop)->(fofType->Prop))). % Definition cs4_impl:=(fun (A:(fofType->Prop)) (B:(fofType->Prop))=> ((mbox reli) ((mimpl A) B))):((fofType->Prop)->((fofType->Prop)->(fofType->Prop))). % Definition cs4_true:=mtrue:(fofType->Prop). % Definition cs4_false:=mfalse:(fofType->Prop). % Definition cs4_all:=(fun (A:(individuals->(fofType->Prop)))=> ((mbox reli) (mall A))):((individuals->(fofType->Prop))->(fofType->Prop)). % Definition cs4_box:=(fun (A:(fofType->Prop))=> ((mbox reli) ((mbox relr) A))):((fofType->Prop)->(fofType->Prop)). % Definition cs4_valid:=(fun (A:(fofType->Prop))=> (mvalid A)):((fofType->Prop)->Prop). % Axiom refl_axiom_i:(forall (A:(fofType->Prop)), (mvalid ((mimpl ((mbox reli) A)) A))). % Axiom refl_axiom_r:(forall (A:(fofType->Prop)), (mvalid ((mimpl ((mbox relr) A)) A))). % Axiom trans_axiom_i:(forall (A:(fofType->Prop)), (mvalid ((mimpl ((mbox reli) A)) ((mbox reli) ((mbox reli) A))))). % Axiom trans_axiom_r:(forall (A:(fofType->Prop)), (mvalid ((mimpl ((mbox relr) A)) ((mbox relr) ((mbox relr) A))))). % Axiom ax_i_r_commute:(forall (A:(fofType->Prop)), (mvalid ((mimpl ((mbox reli) ((mbox relr) A))) ((mbox relr) ((mbox reli) A))))). % Parameter princ_inj:(individuals->(fofType->Prop)). % Definition bl_atom:=(fun (P:(fofType->Prop))=> (cs4_atom P)):((fofType->Prop)->(fofType->Prop)). % Definition bl_princ:=(fun (P:(fofType->Prop))=> (cs4_atom P)):((fofType->Prop)->(fofType->Prop)). % Definition bl_and:=(fun (A:(fofType->Prop)) (B:(fofType->Prop))=> ((cs4_and A) B)):((fofType->Prop)->((fofType->Prop)->(fofType->Prop))). % Definition bl_or:=(fun (A:(fofType->Prop)) (B:(fofType->Prop))=> ((cs4_or A) B)):((fofType->Prop)->((fofType->Prop)->(fofType->Prop))). % Definition bl_impl:=(fun (A:(fofType->Prop)) (B:(fofType->Prop))=> ((cs4_impl A) B)):((fofType->Prop)->((fofType->Prop)->(fofType->Prop))). % Definition bl_all:=(fun (A:(individuals->(fofType->Prop)))=> (cs4_all A)):((individuals->(fofType->Prop))->(fofType->Prop)). % Definition bl_true:=cs4_true:(fofType->Prop). % Definition bl_false:=cs4_false:(fofType->Prop). % Definition bl_says:=(fun (K:individuals) (A:(fofType->Prop))=> (cs4_box ((cs4_impl (bl_princ (princ_inj K))) A))):(individuals->((fofType->Prop)->(fofType->Prop))). % Definition bl_valid:=mvalid:((fofType->Prop)->Prop). % Parameter loca:individuals. % Axiom loca_strength:(cs4_valid (cs4_all (fun (K:individuals)=> ((cs4_impl (princ_inj K)) (princ_inj loca))))). % Parameter ctime:individuals. % Parameter ninfty:individuals. % Parameter pinfty:individuals. % Parameter read:individuals. % Parameter write:individuals. % Parameter execute:individuals. % Parameter identity:individuals. % Parameter govern:individuals. % Parameter prim_str2file:(individuals->individuals). % Parameter prim_date2time:(individuals->individuals). % Parameter prim_int2time:(individuals->individuals). % Parameter prim_int2principal:(individuals->individuals). % Parameter time2exp:(individuals->individuals). % Parameter exp_add:(individuals->(individuals->individuals)). % Parameter exp_subtract:(individuals->(individuals->individuals)). % Parameter exp_min:(individuals->(individuals->individuals)). % Parameter exp_max:(individuals->(individuals->individuals)). % Parameter unclassified:individuals. % Parameter sbu:individuals. % Parameter confidential:individuals. % Parameter secret:individuals. % Parameter topsecret:individuals. % Parameter admin:individuals. % Parameter system:individuals. % Parameter nil:individuals. % Parameter cons:(individuals->(individuals->individuals)). % Parameter anycountry:individuals. % Parameter usa:individuals. % Parameter yes:individuals. % Parameter no:individuals. % Parameter is_working_paper:individuals. % Parameter is_not_working_paper:individuals. % Parameter oca:individuals. % Parameter compartmentb:individuals. % Parameter sso_compartmentb:individuals. % Parameter scg_compartmentb:individuals. % Parameter compartmenta:individuals. % Parameter sso_compartmenta:individuals. % Parameter scg_compartmenta:individuals. % Parameter secretfile:individuals. % Parameter not_secretfile:individuals. % Parameter alice:individuals. % Parameter babu:individuals. % Parameter india:individuals. % Parameter polygraph_admin:individuals. % Parameter credit_admin:individuals. % Parameter background_admin:individuals. % Parameter hr_admin:individuals. % Parameter level_admin:individuals. % Parameter owner_secretfile:individuals. % Parameter owner_not_secretfile:individuals. % Parameter ci:individuals. % Parameter loca_level_direct_below:(individuals->(individuals->(fofType->Prop))). % Parameter loca_level_below:(individuals->(individuals->(fofType->Prop))). % Parameter system_compartment_has_sso:(individuals->(individuals->(fofType->Prop))). % Parameter admin_compartment_has_sso:(individuals->(individuals->(fofType->Prop))). % Parameter system_indi_is_oca:(individuals->(fofType->Prop)). % Parameter oca_compartment_has_scg:(individuals->(individuals->(fofType->Prop))). % Parameter sso_compartment_has_scg:(individuals->(individuals->(fofType->Prop))). % Parameter admin_compartment_has_scg:(individuals->(individuals->(fofType->Prop))). % Parameter system_file_needs_compartments:(individuals->(individuals->(fofType->Prop))). % Parameter admin_file_has_compartments_h:(individuals->(individuals->(individuals->(fofType->Prop)))). % Parameter admin_file_has_compartments:(individuals->(individuals->(fofType->Prop))). % Parameter sso_file_has_compartments:(individuals->(individuals->(fofType->Prop))). % Parameter system_file_needs_level:(individuals->(individuals->(fofType->Prop))). % Parameter admin_file_has_level_h:(individuals->(individuals->(individuals->(fofType->Prop)))). % Parameter admin_file_has_level:(individuals->(individuals->(fofType->Prop))). % Parameter sso_file_has_level:(individuals->(individuals->(individuals->(fofType->Prop)))). % Parameter system_file_needs_citizenship:(individuals->(individuals->(fofType->Prop))). % Parameter admin_file_has_citizenship_h:(individuals->(individuals->(individuals->(fofType->Prop)))). % Parameter admin_file_has_citizenship:(individuals->(individuals->(fofType->Prop))). % Parameter sso_file_has_citizenship:(individuals->(individuals->(individuals->(fofType->Prop)))). % Parameter system_indi_is_polygraph_admin:(individuals->(fofType->Prop)). % Parameter polygraph_admin_indi_has_polygraph:(individuals->(fofType->Prop)). % Parameter admin_indi_has_polygraph:(individuals->(fofType->Prop)). % Parameter system_indi_is_credit_admin:(individuals->(fofType->Prop)). % Parameter credit_admin_indi_has_credit:(individuals->(fofType->Prop)). % Parameter admin_indi_has_credit:(individuals->(fofType->Prop)). % Parameter admin_indi_has_background:(individuals->(individuals->(fofType->Prop))). % Parameter system_indi_is_background_admin:(individuals->(fofType->Prop)). % Parameter background_admin_indi_has_background:(individuals->(individuals->(fofType->Prop))). % Parameter system_indi_is_hr_admin:(individuals->(fofType->Prop)). % Parameter hr_admin_indi_has_employment:(individuals->(fofType->Prop)). % Parameter admin_indi_has_employment:(individuals->(fofType->Prop)). % Parameter admin_indi_has_citizenship:(individuals->(individuals->(fofType->Prop))). % Parameter system_indi_has_citizenship:(individuals->(individuals->(fofType->Prop))). % Parameter admin_indi_has_level:(individuals->(individuals->(fofType->Prop))). % Parameter system_indi_needs_level:(individuals->(individuals->(fofType->Prop))). % Parameter system_indi_is_level_admin:(individuals->(fofType->Prop)). % Parameter level_admin_indi_has_level:(individuals->(individuals->(fofType->Prop))). % Parameter admin_indi_has_compartments:(individuals->(individuals->(fofType->Prop))). % Parameter system_indi_needs_compartment:(individuals->(individuals->(fofType->Prop))). % Parameter admin_indi_has_polygraph_for_compartment:(individuals->(individuals->(fofType->Prop))). % Parameter admin_indi_has_credit_for_compartment:(individuals->(individuals->(fofType->Prop))). % Parameter sso_indi_has_compartment:(individuals->(individuals->(fofType->Prop))). % Parameter admin_indi_has_background_for_compartment:(individuals->(individuals->(fofType->Prop))). % Parameter admin_indi_has_level_for_compartment:(individuals->(individuals->(fofType->Prop))). % Parameter oca_compartment_is_compartment:(individuals->(individuals->(individuals->(individuals->(individuals->(fofType->Prop)))))). % Parameter admin_indi_has_compartments_for_file:(individuals->(individuals->(fofType->Prop))). % Parameter admin_indi_has_level_for_file:(individuals->(individuals->(fofType->Prop))). % Parameter p_owner:(individuals->(individuals->(fofType->Prop))). % Parameter owner_indi_has_need_to_know:(individuals->(individuals->(fofType->Prop))). % Parameter admin_indi_has_need_to_know_for_file:(individuals->(individuals->(fofType->Prop))). % Parameter admin_indi_has_citizenship_for_file:(individuals->(individuals->(fofType->Prop))). % Parameter p_has_xattr:(individuals->(individuals->(individuals->(fofType->Prop)))). % Parameter admin_file_has_not_expired:(individuals->(fofType->Prop)). % Parameter may:(individuals->(individuals->(individuals->(fofType->Prop)))). % Parameter system_indi_is_counterintelligence:(individuals->(individuals->(fofType->Prop))). % Axiom ax0:(bl_valid ((bl_says loca) (bl_atom ((loca_level_direct_below unclassified) sbu)))). % Axiom ax1:(bl_valid ((bl_says loca) (bl_atom ((loca_level_direct_below sbu) confidential)))). % Axiom ax2:(bl_valid ((bl_says loca) (bl_atom ((loca_level_direct_below confidential) secret)))). % Axiom ax3:(bl_valid ((bl_says loca) (bl_atom ((loca_level_direct_below secret) topsecret)))). % Axiom ax4:(bl_valid ((bl_says loca) (bl_all (fun (L:individuals)=> (bl_atom ((loca_level_below L) L)))))). % Axiom ax5:(bl_valid ((bl_says loca) (bl_all (fun (L:individuals)=> (bl_all (fun (L1:individuals)=> (bl_all (fun (L11:individuals)=> ((bl_impl (bl_atom ((loca_level_direct_below L1) L11))) ((bl_impl (bl_atom ((loca_level_below L) L1))) (bl_atom ((loca_level_below L) L11)))))))))))). % Axiom ax6:(bl_valid ((bl_says admin) (bl_all (fun (C:individuals)=> (bl_all (fun (SSO:individuals)=> ((bl_impl ((bl_says system) (bl_atom ((system_compartment_has_sso C) SSO)))) (bl_atom ((admin_compartment_has_sso C) SSO))))))))). % Axiom ax7:(bl_valid ((bl_says admin) (bl_all (fun (OCA:individuals)=> (bl_all (fun (C:individuals)=> (bl_all (fun (SSO:individuals)=> (bl_all (fun (SCG:individuals)=> ((bl_impl ((bl_says system) (bl_atom (system_indi_is_oca OCA)))) ((bl_impl ((bl_says OCA) (bl_atom ((oca_compartment_has_scg C) SCG)))) ((bl_impl (bl_atom ((admin_compartment_has_sso C) SSO))) ((bl_impl ((bl_says SSO) (bl_atom ((sso_compartment_has_scg C) SCG)))) (bl_atom ((admin_compartment_has_scg C) SCG)))))))))))))))). % Axiom ax8:(bl_valid ((bl_says admin) (bl_all (fun (F:individuals)=> (bl_all (fun (CL:individuals)=> ((bl_impl ((bl_says system) (bl_atom ((system_file_needs_compartments F) CL)))) ((bl_impl (bl_atom (((admin_file_has_compartments_h F) CL) CL))) (bl_atom ((admin_file_has_compartments F) CL)))))))))). % Axiom ax9:(bl_valid ((bl_says admin) (bl_all (fun (F:individuals)=> (bl_all (fun (CL:individuals)=> (bl_atom (((admin_file_has_compartments_h F) CL) nil)))))))). % Axiom ax10:(bl_valid ((bl_says admin) (bl_all (fun (F:individuals)=> (bl_all (fun (CL:individuals)=> (bl_all (fun (C1:individuals)=> (bl_all (fun (CL1:individuals)=> (bl_all (fun (SSO:individuals)=> ((bl_impl (bl_atom ((admin_compartment_has_sso C1) SSO))) ((bl_impl ((bl_says SSO) (bl_atom ((sso_file_has_compartments F) CL)))) ((bl_impl (bl_atom (((admin_file_has_compartments_h F) CL) CL1))) (bl_atom (((admin_file_has_compartments_h F) CL) ((cons C1) CL1)))))))))))))))))). % Axiom ax11:(bl_valid ((bl_says admin) (bl_all (fun (F:individuals)=> (bl_all (fun (L:individuals)=> (bl_all (fun (CL:individuals)=> ((bl_impl ((bl_says system) (bl_atom ((system_file_needs_level F) L)))) ((bl_impl (bl_atom ((admin_file_has_compartments F) CL))) ((bl_impl (bl_atom (((admin_file_has_level_h F) L) CL))) (bl_atom ((admin_file_has_level F) L))))))))))))). % Axiom ax12:(bl_valid ((bl_says admin) (bl_all (fun (F:individuals)=> (bl_all (fun (L:individuals)=> (bl_atom (((admin_file_has_level_h F) L) nil)))))))). % Axiom ax13:(bl_valid ((bl_says admin) (bl_all (fun (F:individuals)=> (bl_all (fun (L:individuals)=> (bl_all (fun (C:individuals)=> (bl_all (fun (CL:individuals)=> (bl_all (fun (SSO:individuals)=> (bl_all (fun (SCG:individuals)=> ((bl_impl (bl_atom ((admin_compartment_has_sso C) SSO))) ((bl_impl (bl_atom ((admin_compartment_has_scg C) SCG))) ((bl_impl ((bl_says SSO) (bl_atom (((sso_file_has_level F) L) SCG)))) ((bl_impl (bl_atom (((admin_file_has_level_h F) L) CL))) (bl_atom (((admin_file_has_level_h F) L) ((cons C) CL))))))))))))))))))))). % Axiom ax14:(bl_valid ((bl_says admin) (bl_all (fun (F:individuals)=> (bl_all (fun (U:individuals)=> (bl_all (fun (CL:individuals)=> ((bl_impl ((bl_says system) (bl_atom ((system_file_needs_citizenship F) U)))) ((bl_impl (bl_atom ((admin_file_has_compartments F) CL))) ((bl_impl (bl_atom (((admin_file_has_citizenship_h F) U) CL))) (bl_atom ((admin_file_has_citizenship F) U))))))))))))). % Axiom ax15:(bl_valid ((bl_says admin) (bl_all (fun (F:individuals)=> (bl_all (fun (U:individuals)=> (bl_atom (((admin_file_has_citizenship_h F) U) nil)))))))). % Axiom ax16:(bl_valid ((bl_says admin) (bl_all (fun (F:individuals)=> (bl_all (fun (U:individuals)=> (bl_all (fun (C:individuals)=> (bl_all (fun (CL:individuals)=> (bl_all (fun (SSO:individuals)=> (bl_all (fun (SCG:individuals)=> ((bl_impl (bl_atom ((admin_compartment_has_sso C) SSO))) ((bl_impl (bl_atom ((admin_compartment_has_scg C) SCG))) ((bl_impl ((bl_says SSO) (bl_atom (((sso_file_has_citizenship F) U) SCG)))) ((bl_impl (bl_atom (((admin_file_has_citizenship_h F) U) CL))) (bl_atom (((admin_file_has_citizenship_h F) U) ((cons C) CL))))))))))))))))))))). % Axiom ax17:(bl_valid ((bl_says admin) (bl_all (fun (K:individuals)=> (bl_all (fun (PA:individuals)=> ((bl_impl ((bl_says system) (bl_atom (system_indi_is_polygraph_admin PA)))) ((bl_impl ((bl_says PA) (bl_atom (polygraph_admin_indi_has_polygraph K)))) (bl_atom (admin_indi_has_polygraph K)))))))))). % Axiom ax18:(bl_valid ((bl_says admin) (bl_all (fun (K:individuals)=> (bl_all (fun (CA:individuals)=> ((bl_impl ((bl_says system) (bl_atom (system_indi_is_credit_admin CA)))) ((bl_impl ((bl_says CA) (bl_atom (credit_admin_indi_has_credit K)))) (bl_atom (admin_indi_has_credit K)))))))))). % Axiom ax19:(bl_valid ((bl_says admin) (bl_all (fun (K:individuals)=> (bl_atom ((admin_indi_has_background K) unclassified)))))). % Axiom ax20:(bl_valid ((bl_says admin) (bl_all (fun (K:individuals)=> (bl_all (fun (L:individuals)=> (bl_all (fun (BA:individuals)=> (bl_all (fun (L1:individuals)=> ((bl_impl ((bl_says system) (bl_atom (system_indi_is_background_admin BA)))) ((bl_impl ((bl_says BA) (bl_atom ((background_admin_indi_has_background K) L1)))) ((bl_impl (bl_atom ((loca_level_below L) L1))) (bl_atom ((admin_indi_has_background K) L))))))))))))))). % Axiom ax21:(bl_valid ((bl_says admin) (bl_all (fun (K:individuals)=> (bl_all (fun (HR:individuals)=> ((bl_impl ((bl_says system) (bl_atom (system_indi_is_hr_admin HR)))) ((bl_impl ((bl_says HR) (bl_atom (hr_admin_indi_has_employment K)))) (bl_atom (admin_indi_has_employment K)))))))))). % Axiom ax22:(bl_valid ((bl_says admin) (bl_all (fun (K:individuals)=> (bl_atom ((admin_indi_has_citizenship K) anycountry)))))). % Axiom ax23:(bl_valid ((bl_says admin) (bl_all (fun (K:individuals)=> (bl_all (fun (U:individuals)=> ((bl_impl ((bl_says system) (bl_atom ((system_indi_has_citizenship K) U)))) (bl_atom ((admin_indi_has_citizenship K) U))))))))). % Axiom ax24:(bl_valid ((bl_says admin) (bl_all (fun (K:individuals)=> (bl_atom ((admin_indi_has_level K) unclassified)))))). % Axiom ax25:(bl_valid ((bl_says admin) (bl_all (fun (K:individuals)=> (bl_all (fun (L:individuals)=> (bl_all (fun (L1:individuals)=> (bl_all (fun (LA:individuals)=> (bl_all (fun (L11:individuals)=> ((bl_impl ((bl_says system) (bl_atom ((system_indi_needs_level K) L1)))) ((bl_impl (bl_atom ((admin_indi_has_citizenship K) usa))) ((bl_impl (bl_atom (admin_indi_has_polygraph K))) ((bl_impl (bl_atom (admin_indi_has_employment K))) ((bl_impl (bl_atom (admin_indi_has_credit K))) ((bl_impl (bl_atom ((loca_level_below L) L1))) ((bl_impl ((bl_says system) (bl_atom (system_indi_is_level_admin LA)))) ((bl_impl ((bl_says LA) (bl_atom ((level_admin_indi_has_level K) L11)))) ((bl_impl (bl_atom ((loca_level_below L) L11))) ((bl_impl (bl_atom ((admin_indi_has_background K) L))) (bl_atom ((admin_indi_has_level K) L)))))))))))))))))))))))). % Axiom ax26:(bl_valid ((bl_says admin) (bl_all (fun (K:individuals)=> (bl_atom ((admin_indi_has_compartments K) nil)))))). % Axiom ax27:(bl_valid ((bl_says admin) (bl_all (fun (K:individuals)=> (bl_all (fun (C:individuals)=> (bl_all (fun (CL:individuals)=> (bl_all (fun (SSO:individuals)=> ((bl_impl ((bl_says system) (bl_atom ((system_indi_needs_compartment K) C)))) ((bl_impl (bl_atom (admin_indi_has_employment K))) ((bl_impl (bl_atom ((admin_indi_has_citizenship K) usa))) ((bl_impl (bl_atom ((admin_indi_has_polygraph_for_compartment K) C))) ((bl_impl (bl_atom ((admin_indi_has_credit_for_compartment K) C))) ((bl_impl (bl_atom ((admin_compartment_has_sso C) SSO))) ((bl_impl ((bl_says SSO) (bl_atom ((sso_indi_has_compartment K) C)))) ((bl_impl (bl_atom ((admin_indi_has_background_for_compartment K) C))) ((bl_impl (bl_atom ((admin_indi_has_level_for_compartment K) C))) ((bl_impl (bl_atom ((admin_indi_has_compartments K) CL))) (bl_atom ((admin_indi_has_compartments K) ((cons C) CL))))))))))))))))))))))). % Axiom ax28:(bl_valid ((bl_says admin) (bl_all (fun (K:individuals)=> (bl_all (fun (C:individuals)=> (bl_all (fun (OCA:individuals)=> (bl_all (fun (L1:individuals)=> (bl_all (fun (L2:individuals)=> (bl_all (fun (B1:individuals)=> (bl_all (fun (B2:individuals)=> ((bl_impl ((bl_says system) (bl_atom (system_indi_is_oca OCA)))) ((bl_impl ((bl_says OCA) (bl_atom (((((oca_compartment_is_compartment C) L1) L2) B1) B2)))) ((bl_impl (bl_atom ((admin_indi_has_background K) L2))) (bl_atom ((admin_indi_has_background_for_compartment K) C))))))))))))))))))))). % Axiom ax29:(bl_valid ((bl_says admin) (bl_all (fun (K:individuals)=> (bl_all (fun (C:individuals)=> (bl_all (fun (OCA:individuals)=> (bl_all (fun (L1:individuals)=> (bl_all (fun (L2:individuals)=> (bl_all (fun (B1:individuals)=> (bl_all (fun (B2:individuals)=> ((bl_impl ((bl_says system) (bl_atom (system_indi_is_oca OCA)))) ((bl_impl ((bl_says OCA) (bl_atom (((((oca_compartment_is_compartment C) L1) L2) B1) B2)))) ((bl_impl (bl_atom ((admin_indi_has_level K) L1))) (bl_atom ((admin_indi_has_level_for_compartment K) C))))))))))))))))))))). % Axiom ax30:(bl_valid ((bl_says admin) (bl_all (fun (K:individuals)=> (bl_all (fun (C:individuals)=> (bl_all (fun (OCA:individuals)=> (bl_all (fun (L1:individuals)=> (bl_all (fun (L2:individuals)=> (bl_all (fun (B1:individuals)=> ((bl_impl ((bl_says system) (bl_atom (system_indi_is_oca OCA)))) ((bl_impl ((bl_says OCA) (bl_atom (((((oca_compartment_is_compartment C) L1) L2) B1) yes)))) ((bl_impl (bl_atom (admin_indi_has_polygraph K))) (bl_atom ((admin_indi_has_polygraph_for_compartment K) C))))))))))))))))))). % Axiom ax31:(bl_valid ((bl_says admin) (bl_all (fun (K:individuals)=> (bl_all (fun (C:individuals)=> (bl_all (fun (OCA:individuals)=> (bl_all (fun (L1:individuals)=> (bl_all (fun (L2:individuals)=> (bl_all (fun (B1:individuals)=> ((bl_impl ((bl_says system) (bl_atom (system_indi_is_oca OCA)))) ((bl_impl ((bl_says OCA) (bl_atom (((((oca_compartment_is_compartment C) L1) L2) B1) no)))) (bl_atom ((admin_indi_has_polygraph_for_compartment K) C)))))))))))))))))). % Axiom ax32:(bl_valid ((bl_says admin) (bl_all (fun (K:individuals)=> (bl_all (fun (C:individuals)=> (bl_all (fun (OCA:individuals)=> (bl_all (fun (L1:individuals)=> (bl_all (fun (L2:individuals)=> (bl_all (fun (B2:individuals)=> ((bl_impl ((bl_says system) (bl_atom (system_indi_is_oca OCA)))) ((bl_impl ((bl_says OCA) (bl_atom (((((oca_compartment_is_compartment C) L1) L2) yes) B2)))) ((bl_impl (bl_atom (admin_indi_has_credit K))) (bl_atom ((admin_indi_has_credit_for_compartment K) C))))))))))))))))))). % Axiom ax33:(bl_valid ((bl_says admin) (bl_all (fun (K:individuals)=> (bl_all (fun (C:individuals)=> (bl_all (fun (OCA:individuals)=> (bl_all (fun (L1:individuals)=> (bl_all (fun (L2:individuals)=> (bl_all (fun (B2:individuals)=> ((bl_impl ((bl_says system) (bl_atom (system_indi_is_oca OCA)))) ((bl_impl ((bl_says OCA) (bl_atom (((((oca_compartment_is_compartment C) L1) L2) no) B2)))) (bl_atom ((admin_indi_has_credit_for_compartment K) C)))))))))))))))))). % Axiom ax34:(bl_valid ((bl_says admin) (bl_all (fun (K:individuals)=> (bl_all (fun (F:individuals)=> (bl_all (fun (CL:individuals)=> ((bl_impl (bl_atom ((admin_file_has_compartments F) CL))) ((bl_impl (bl_atom ((admin_indi_has_compartments K) CL))) (bl_atom ((admin_indi_has_compartments_for_file K) F)))))))))))). % Axiom ax35:(bl_valid ((bl_says admin) (bl_all (fun (K:individuals)=> (bl_all (fun (F:individuals)=> (bl_all (fun (L:individuals)=> ((bl_impl (bl_atom ((admin_file_has_level F) L))) ((bl_impl (bl_atom ((admin_indi_has_level K) L))) (bl_atom ((admin_indi_has_level_for_file K) F)))))))))))). % Axiom ax36:(bl_valid ((bl_says admin) (bl_all (fun (K:individuals)=> (bl_all (fun (F:individuals)=> (bl_all (fun (O:individuals)=> ((bl_impl ((bl_says loca) (bl_atom ((p_owner F) O)))) ((bl_impl ((bl_says O) (bl_atom ((owner_indi_has_need_to_know K) F)))) (bl_atom ((admin_indi_has_need_to_know_for_file K) F)))))))))))). % Axiom ax37:(bl_valid ((bl_says admin) (bl_all (fun (K:individuals)=> (bl_all (fun (F:individuals)=> (bl_all (fun (L:individuals)=> ((bl_impl (bl_atom ((admin_file_has_citizenship F) L))) ((bl_impl (bl_atom ((admin_indi_has_citizenship K) L))) (bl_atom ((admin_indi_has_citizenship_for_file K) F)))))))))))). % Axiom ax38:(bl_valid ((bl_says admin) (bl_all (fun (K:individuals)=> (bl_all (fun (F:individuals)=> ((bl_impl (bl_atom ((admin_indi_has_citizenship K) usa))) (bl_atom ((admin_indi_has_citizenship_for_file K) F))))))))). % Axiom ax39:(bl_valid ((bl_says admin) (bl_all (fun (K:individuals)=> (bl_all (fun (F:individuals)=> ((bl_impl ((bl_says loca) (bl_atom (((p_has_xattr F) is_working_paper) yes)))) ((bl_impl ((bl_says loca) (bl_atom ((p_owner F) K)))) ((bl_impl (bl_atom (admin_file_has_not_expired F))) (bl_atom (((may K) F) read))))))))))). % Axiom ax40:(bl_valid ((bl_says admin) (bl_all (fun (K:individuals)=> (bl_all (fun (F:individuals)=> ((bl_impl ((bl_says loca) (bl_atom (((p_has_xattr F) is_not_working_paper) yes)))) ((bl_impl (bl_atom ((admin_indi_has_citizenship_for_file K) F))) ((bl_impl (bl_atom ((admin_indi_has_need_to_know_for_file K) F))) ((bl_impl (bl_atom ((admin_indi_has_level_for_file K) F))) ((bl_impl (bl_atom ((admin_indi_has_compartments_for_file K) F))) (bl_atom (((may K) F) read))))))))))))). % Axiom ax41:(bl_valid ((bl_says admin) (bl_all (fun (K:individuals)=> (bl_all (fun (F:individuals)=> (bl_all (fun (K1:individuals)=> ((bl_impl ((bl_says loca) (bl_atom ((p_owner F) K1)))) ((bl_impl ((bl_says system) (bl_atom ((system_indi_is_counterintelligence K) K1)))) (bl_atom (((may K) F) read)))))))))))). % Axiom ax42:(bl_valid ((bl_says system) (bl_atom (system_indi_is_oca oca)))). % Axiom ax43:(bl_valid ((bl_says system) (bl_atom ((system_compartment_has_sso compartmentb) sso_compartmentb)))). % Axiom ax44:(bl_valid ((bl_says oca) (bl_atom ((oca_compartment_has_scg compartmentb) scg_compartmentb)))). % Axiom ax45:(bl_valid ((bl_says sso_compartmentb) (bl_atom ((sso_compartment_has_scg compartmentb) scg_compartmentb)))). % Axiom ax46:(bl_valid ((bl_says system) (bl_atom ((system_compartment_has_sso compartmenta) sso_compartmenta)))). % Axiom ax47:(bl_valid ((bl_says oca) (bl_atom ((oca_compartment_has_scg compartmenta) scg_compartmenta)))). % Axiom ax48:(bl_valid ((bl_says sso_compartmenta) (bl_atom ((sso_compartment_has_scg compartmenta) scg_compartmenta)))). % Axiom ax49:(bl_valid ((bl_says loca) (bl_atom (((p_has_xattr secretfile) is_not_working_paper) yes)))). % Axiom ax50:(bl_valid ((bl_says system) (bl_atom ((system_file_needs_compartments secretfile) ((cons compartmentb) ((cons compartmenta) nil)))))). % Axiom ax51:(bl_valid ((bl_says sso_compartmentb) (bl_atom ((sso_file_has_compartments secretfile) ((cons compartmentb) ((cons compartmenta) nil)))))). % Axiom ax52:(bl_valid ((bl_says sso_compartmenta) (bl_atom ((sso_file_has_compartments secretfile) ((cons compartmentb) ((cons compartmenta) nil)))))). % Axiom ax53:(bl_valid ((bl_says loca) (bl_atom (((p_has_xattr not_secretfile) is_not_working_paper) yes)))). % Axiom ax54:(bl_valid ((bl_says system) (bl_atom ((system_file_needs_compartments not_secretfile) nil)))). % Axiom ax55:(bl_valid ((bl_says system) (bl_atom ((system_file_needs_level secretfile) secret)))). % Axiom ax56:(bl_valid ((bl_says sso_compartmentb) (bl_atom (((sso_file_has_level secretfile) secret) scg_compartmentb)))). % Axiom ax57:(bl_valid ((bl_says sso_compartmenta) (bl_atom (((sso_file_has_level secretfile) secret) scg_compartmenta)))). % Axiom ax58:(bl_valid ((bl_says system) (bl_atom ((system_file_needs_level not_secretfile) unclassified)))). % Axiom ax59:(bl_valid ((bl_says system) (bl_atom ((system_file_needs_citizenship secretfile) usa)))). % Axiom ax60:(bl_valid ((bl_says sso_compartmentb) (bl_atom (((sso_file_has_citizenship secretfile) usa) scg_compartmentb)))). % Axiom ax61:(bl_valid ((bl_says sso_compartmenta % EOF %------------------------------------------------------------------------------