%------------------------------------------------------------------------------
% File : Refute---2015
% Problem : SWV440+1 : TPTP v6.4.0. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : isabelle tptp_refute %d %s
% Computer : n050.star.cs.uiowa.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2609 0 2.40GHz
% Memory : 32218.75MB
% OS : Linux 3.10.0-327.10.1.el7.x86_64
% CPULimit : 300s
% DateTime : Thu Apr 14 05:28:54 EDT 2016
% Result : CounterSatisfiable 137.75s
% Output : Assurance 0s
% Verified :
% SZS Type : None (Parsing solution fails)
% Syntax : Number of formulae : 0
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWV440+1 : TPTP v6.4.0. Released v4.0.0.
% 0.00/0.04 % Command : isabelle tptp_refute %d %s
% 0.03/0.23 % Computer : n050.star.cs.uiowa.edu
% 0.03/0.23 % Model : x86_64 x86_64
% 0.03/0.23 % CPU : Intel(R) Xeon(R) CPU E5-2609 0 @ 2.40GHz
% 0.03/0.23 % Memory : 32218.75MB
% 0.03/0.23 % OS : Linux 3.10.0-327.10.1.el7.x86_64
% 0.03/0.23 % CPULimit : 300
% 0.03/0.23 % DateTime : Fri Apr 8 15:34:09 CDT 2016
% 0.03/0.23 % CPUTime :
% 6.31/5.83 > val it = (): unit
% 6.71/6.22 Trying to find a model that refutes: bnd_admin_indi_may_file bnd_admin bnd_alice bnd_not_secretfile bnd_read
% 8.92/8.46 Unfolded term: [| bnd_system_indi_is_counterintelligence bnd_system bnd_ci
% 8.92/8.46 bnd_owner_secretfile;
% 8.92/8.46 bnd_owner_indi_has_need_to_know bnd_owner_not_secretfile bnd_babu
% 8.92/8.46 bnd_not_secretfile;
% 8.92/8.46 bnd_system_indi_has_citizenship bnd_system bnd_babu bnd_india;
% 8.92/8.46 bnd_owner_indi_has_need_to_know bnd_owner_secretfile bnd_alice
% 8.92/8.46 bnd_not_secretfile;
% 8.92/8.46 bnd_owner_indi_has_need_to_know bnd_owner_secretfile bnd_alice
% 8.92/8.46 bnd_secretfile;
% 8.92/8.46 bnd_sso_indi_has_compartment bnd_sso_compartmenta bnd_alice
% 8.92/8.46 bnd_compartmenta;
% 8.92/8.46 bnd_sso_indi_has_compartment bnd_sso_compartmentb bnd_alice
% 8.92/8.46 bnd_compartmentb;
% 8.92/8.46 bnd_system_indi_needs_compartment bnd_system bnd_alice bnd_compartmenta;
% 8.92/8.46 bnd_system_indi_needs_compartment bnd_system bnd_alice bnd_compartmentb;
% 8.92/8.46 bnd_level_admin_indi_has_level bnd_level_admin bnd_alice bnd_topsecret;
% 8.92/8.46 bnd_system_indi_needs_level bnd_system bnd_alice bnd_secret;
% 8.92/8.46 bnd_hr_admin_indi_has_employment bnd_hr_admin bnd_alice;
% 8.92/8.46 bnd_background_admin_indi_has_background bnd_background_admin bnd_alice
% 8.92/8.46 bnd_topsecret;
% 8.92/8.46 bnd_credit_admin_indi_has_credit bnd_credit_admin bnd_alice;
% 8.92/8.46 bnd_polygraph_admin_indi_has_polygraph bnd_polygraph_admin bnd_alice;
% 8.92/8.46 bnd_system_indi_has_citizenship bnd_system bnd_alice bnd_usa;
% 8.92/8.46 bnd_system_indi_is_level_admin bnd_system bnd_level_admin;
% 8.92/8.46 bnd_system_indi_is_hr_admin bnd_system bnd_hr_admin;
% 8.92/8.46 bnd_system_indi_is_background_admin bnd_system bnd_background_admin;
% 8.92/8.46 bnd_system_indi_is_credit_admin bnd_system bnd_credit_admin;
% 8.92/8.46 bnd_system_indi_is_polygraph_admin bnd_system bnd_polygraph_admin;
% 8.92/8.46 bnd_state_file_has_owner bnd_not_secretfile bnd_owner_not_secretfile;
% 8.92/8.46 bnd_system_file_needs_citizenship bnd_system bnd_not_secretfile
% 8.92/8.46 bnd_anycountry;
% 8.92/8.46 bnd_system_file_needs_level bnd_system bnd_not_secretfile
% 8.92/8.46 bnd_unclassified;
% 8.92/8.46 bnd_system_file_needs_compartments bnd_system bnd_not_secretfile bnd_nil;
% 8.92/8.46 bnd_state_file_is_not_working_paper bnd_not_secretfile;
% 8.92/8.46 bnd_state_file_has_owner bnd_secretfile bnd_owner_secretfile;
% 8.92/8.46 bnd_sso_file_has_citizenship bnd_sso_compartmenta bnd_secretfile bnd_usa
% 8.92/8.46 bnd_scg_compartmenta;
% 8.92/8.46 bnd_sso_file_has_citizenship bnd_sso_compartmentb bnd_secretfile bnd_usa
% 8.92/8.46 bnd_scg_compartmentb;
% 8.92/8.46 bnd_system_file_needs_citizenship bnd_system bnd_secretfile bnd_usa;
% 8.92/8.46 bnd_sso_file_has_level bnd_sso_compartmenta bnd_secretfile bnd_secret
% 8.92/8.46 bnd_scg_compartmenta;
% 8.92/8.46 bnd_sso_file_has_level bnd_sso_compartmentb bnd_secretfile bnd_secret
% 8.92/8.46 bnd_scg_compartmentb;
% 8.92/8.46 bnd_system_file_needs_level bnd_system bnd_secretfile bnd_secret;
% 8.92/8.46 bnd_sso_file_has_compartments bnd_sso_compartmenta bnd_secretfile
% 8.92/8.46 (bnd_cons bnd_compartmentb (bnd_cons bnd_compartmenta bnd_nil));
% 8.92/8.46 bnd_sso_file_has_compartments bnd_sso_compartmentb bnd_secretfile
% 8.92/8.46 (bnd_cons bnd_compartmentb (bnd_cons bnd_compartmenta bnd_nil));
% 8.92/8.46 bnd_system_file_needs_compartments bnd_system bnd_secretfile
% 8.92/8.46 (bnd_cons bnd_compartmentb (bnd_cons bnd_compartmenta bnd_nil));
% 8.92/8.46 bnd_state_file_is_not_working_paper bnd_secretfile;
% 8.92/8.46 bnd_sso_compartment_has_scg bnd_sso_compartmenta bnd_compartmenta
% 8.92/8.46 bnd_scg_compartmenta;
% 8.92/8.46 bnd_oca_compartment_has_scg bnd_oca bnd_compartmenta
% 8.92/8.46 bnd_scg_compartmenta;
% 8.92/8.46 bnd_system_compartment_has_sso bnd_system bnd_compartmenta
% 8.92/8.46 bnd_sso_compartmenta;
% 8.92/8.46 bnd_sso_compartment_has_scg bnd_sso_compartmentb bnd_compartmentb
% 8.92/8.46 bnd_scg_compartmentb;
% 8.92/8.46 bnd_oca_compartment_has_scg bnd_oca bnd_compartmentb
% 8.92/8.46 bnd_scg_compartmentb;
% 8.92/8.46 bnd_system_compartment_has_sso bnd_system bnd_compartmentb
% 8.92/8.46 bnd_sso_compartmentb;
% 8.92/8.46 bnd_oca_compartment_is_compartment bnd_oca bnd_compartmenta bnd_sbu
% 8.92/8.46 bnd_unclassified bnd_no bnd_no;
% 8.92/8.46 bnd_oca_compartment_is_compartment bnd_oca bnd_compartmentb
% 8.92/8.46 bnd_confidential bnd_topsecret bnd_yes bnd_yes;
% 8.92/8.46 bnd_system_indi_is_oca bnd_system bnd_oca;
% 8.92/8.46 ALL K F K1.
% 8.92/8.46 bnd_state_file_has_owner F K1 -->
% 8.92/8.46 bnd_system_indi_is_counterintelligence bnd_system K K1 -->
% 8.92/8.46 bnd_admin_indi_may_file bnd_admin K F bnd_read;
% 8.92/8.46 ALL K F.
% 8.92/8.46 bnd_state_file_is_not_working_paper F -->
% 8.92/8.46 bnd_admin_indi_has_citizenship_for_file bnd_admin K F -->
% 8.92/8.46 bnd_admin_indi_has_need_to_know_for_file bnd_admin K F -->
% 8.92/8.46 bnd_admin_indi_has_level_for_file bnd_admin K F -->
% 8.92/8.46 bnd_admin_indi_has_compartments_for_file bnd_admin K F -->
% 8.92/8.46 bnd_admin_indi_may_file bnd_admin K F bnd_read;
% 8.92/8.46 ALL K F.
% 8.92/8.46 bnd_admin_indi_has_citizenship bnd_admin K bnd_usa -->
% 8.92/8.46 bnd_admin_indi_has_citizenship_for_file bnd_admin K F;
% 8.92/8.46 ALL K F L.
% 8.92/8.46 bnd_admin_file_has_citizenship bnd_admin F L -->
% 8.92/8.46 bnd_admin_indi_has_citizenship bnd_admin K L -->
% 8.92/8.46 bnd_admin_indi_has_citizenship_for_file bnd_admin K F;
% 8.92/8.46 ALL K F OWR.
% 8.92/8.46 bnd_state_file_has_owner F OWR -->
% 8.92/8.46 bnd_owner_indi_has_need_to_know OWR K F -->
% 8.92/8.46 bnd_admin_indi_has_need_to_know_for_file bnd_admin K F;
% 8.92/8.46 ALL K F L.
% 8.92/8.46 bnd_admin_file_has_level bnd_admin F L -->
% 8.92/8.46 bnd_admin_indi_has_level bnd_admin K L -->
% 8.92/8.46 bnd_admin_indi_has_level_for_file bnd_admin K F;
% 8.92/8.46 ALL K F CL.
% 8.92/8.46 bnd_admin_file_has_compartments bnd_admin F CL -->
% 8.92/8.46 bnd_admin_indi_has_compartments bnd_admin K CL -->
% 8.92/8.47 bnd_admin_indi_has_compartments_for_file bnd_admin K F;
% 8.92/8.47 ALL K C OCA L1 L2 B2.
% 8.92/8.47 bnd_system_indi_is_oca bnd_system OCA -->
% 8.92/8.47 bnd_oca_compartment_is_compartment OCA C L1 L2 bnd_no B2 -->
% 8.92/8.47 bnd_admin_indi_has_credit_for_compartment bnd_admin K C;
% 8.92/8.47 ALL K C OCA L1 L2 B2.
% 8.92/8.47 bnd_system_indi_is_oca bnd_system OCA -->
% 8.92/8.47 bnd_oca_compartment_is_compartment OCA C L1 L2 bnd_yes B2 -->
% 8.92/8.47 bnd_admin_indi_has_credit bnd_admin K -->
% 8.92/8.47 bnd_admin_indi_has_credit_for_compartment bnd_admin K C;
% 8.92/8.47 ALL K C OCA L1 L2 B1.
% 8.92/8.47 bnd_system_indi_is_oca bnd_system OCA -->
% 8.92/8.47 bnd_oca_compartment_is_compartment OCA C L1 L2 B1 bnd_no -->
% 8.92/8.47 bnd_admin_indi_has_polygraph_for_compartment bnd_admin K C;
% 8.92/8.47 ALL K C OCA L1 L2 B1.
% 8.92/8.47 bnd_system_indi_is_oca bnd_system OCA -->
% 8.92/8.47 bnd_oca_compartment_is_compartment OCA C L1 L2 B1 bnd_yes -->
% 8.92/8.47 bnd_admin_indi_has_polygraph bnd_admin K -->
% 8.92/8.47 bnd_admin_indi_has_polygraph_for_compartment bnd_admin K C;
% 8.92/8.47 ALL K C OCA L1 L2 B1 B2.
% 8.92/8.47 bnd_system_indi_is_oca bnd_system OCA -->
% 8.92/8.47 bnd_oca_compartment_is_compartment OCA C L1 L2 B1 B2 -->
% 8.92/8.47 bnd_admin_indi_has_level bnd_admin K L1 -->
% 8.92/8.47 bnd_admin_indi_has_level_for_compartment bnd_admin K C;
% 8.92/8.47 ALL K C OCA L1 L2 B1 B2.
% 8.92/8.47 bnd_system_indi_is_oca bnd_system OCA -->
% 8.92/8.47 bnd_oca_compartment_is_compartment OCA C L1 L2 B1 B2 -->
% 8.92/8.47 bnd_admin_indi_has_background bnd_admin K L2 -->
% 8.92/8.47 bnd_admin_indi_has_background_for_compartment bnd_admin K C;
% 8.92/8.47 ALL K C CL SSO.
% 8.92/8.47 bnd_system_indi_needs_compartment bnd_system K C -->
% 8.92/8.47 bnd_admin_indi_has_employment bnd_admin K -->
% 8.92/8.47 bnd_admin_indi_has_citizenship bnd_admin K bnd_usa -->
% 8.92/8.47 bnd_admin_indi_has_polygraph_for_compartment bnd_admin K C -->
% 8.92/8.47 bnd_admin_indi_has_credit_for_compartment bnd_admin K C -->
% 8.92/8.47 bnd_admin_compartment_has_sso bnd_admin C SSO -->
% 8.92/8.47 bnd_sso_indi_has_compartment SSO K C -->
% 8.92/8.47 bnd_admin_indi_has_background_for_compartment bnd_admin K C -->
% 8.92/8.47 bnd_admin_indi_has_level_for_compartment bnd_admin K C -->
% 8.92/8.47 bnd_admin_indi_has_compartments bnd_admin K CL -->
% 8.92/8.47 bnd_admin_indi_has_compartments bnd_admin K (bnd_cons C CL);
% 8.92/8.47 ALL K. bnd_admin_indi_has_compartments bnd_admin K bnd_nil;
% 8.92/8.47 ALL K L L1 LA L11.
% 8.92/8.47 bnd_system_indi_needs_level bnd_system K L1 -->
% 8.92/8.47 bnd_admin_indi_has_citizenship bnd_admin K bnd_usa -->
% 8.92/8.47 bnd_admin_indi_has_polygraph bnd_admin K -->
% 8.92/8.47 bnd_admin_indi_has_employment bnd_admin K -->
% 8.92/8.47 bnd_admin_indi_has_credit bnd_admin K -->
% 8.92/8.47 bnd_loca_level_below bnd_admin L L1 -->
% 8.92/8.47 bnd_system_indi_is_level_admin bnd_system LA -->
% 8.92/8.47 bnd_level_admin_indi_has_level LA K L11 -->
% 8.92/8.47 bnd_loca_level_below bnd_admin L L11 -->
% 8.92/8.47 bnd_admin_indi_has_background bnd_admin K L -->
% 8.92/8.47 bnd_admin_indi_has_level bnd_admin K L;
% 8.92/8.47 ALL K. bnd_admin_indi_has_level bnd_admin K bnd_unclassified;
% 8.92/8.47 ALL K U.
% 8.92/8.47 bnd_system_indi_has_citizenship bnd_system K U -->
% 8.92/8.47 bnd_admin_indi_has_citizenship bnd_admin K U;
% 8.92/8.47 ALL K. bnd_admin_indi_has_citizenship bnd_admin K bnd_anycountry;
% 8.92/8.47 ALL K HR.
% 8.92/8.47 bnd_system_indi_is_hr_admin bnd_system HR -->
% 8.92/8.47 bnd_hr_admin_indi_has_employment HR K -->
% 8.92/8.47 bnd_admin_indi_has_employment bnd_admin K;
% 8.92/8.47 ALL K L BA L1.
% 8.92/8.47 bnd_system_indi_is_background_admin bnd_system BA -->
% 8.92/8.47 bnd_background_admin_indi_has_background BA K L1 -->
% 8.92/8.47 bnd_loca_level_below bnd_admin L L1 -->
% 8.92/8.47 bnd_admin_indi_has_background bnd_admin K L;
% 8.92/8.47 ALL K. bnd_admin_indi_has_background bnd_admin K bnd_unclassified;
% 8.92/8.47 ALL K CA.
% 8.92/8.47 bnd_system_indi_is_credit_admin bnd_system CA -->
% 8.92/8.47 bnd_credit_admin_indi_has_credit CA K -->
% 8.92/8.47 bnd_admin_indi_has_credit bnd_admin K;
% 8.92/8.47 ALL K PA.
% 8.92/8.47 bnd_system_indi_is_polygraph_admin bnd_system PA -->
% 8.92/8.47 bnd_polygraph_admin_indi_has_polygraph PA K -->
% 8.92/8.47 bnd_admin_indi_has_polygraph bnd_admin K;
% 8.92/8.47 ALL F U C CL SSO SCG.
% 8.92/8.47 bnd_admin_compartment_has_sso bnd_admin C SSO -->
% 8.92/8.47 bnd_admin_compartment_has_scg bnd_admin C SCG -->
% 8.92/8.47 bnd_sso_file_has_citizenship SSO F U SCG -->
% 8.92/8.47 bnd_admin_file_has_citizenship_h bnd_admin F U CL -->
% 8.92/8.47 bnd_admin_file_has_citizenship_h bnd_admin F U (bnd_cons C CL);
% 8.92/8.47 ALL F U. bnd_admin_file_has_citizenship_h bnd_admin F U bnd_nil;
% 8.92/8.47 ALL F U CL.
% 8.92/8.47 bnd_system_file_needs_citizenship bnd_system F U -->
% 8.92/8.47 bnd_admin_file_has_compartments bnd_admin F CL -->
% 8.92/8.47 bnd_admin_file_has_citizenship_h bnd_admin F U CL -->
% 8.92/8.47 bnd_admin_file_has_citizenship bnd_admin F U;
% 8.92/8.47 ALL F L C CL SSO SCG.
% 8.92/8.47 bnd_admin_compartment_has_sso bnd_admin C SSO -->
% 8.92/8.47 bnd_admin_compartment_has_scg bnd_admin C SCG -->
% 8.92/8.47 bnd_sso_file_has_level SSO F L SCG -->
% 8.92/8.47 bnd_admin_file_has_level_h bnd_admin F L CL -->
% 8.92/8.47 bnd_admin_file_has_level_h bnd_admin F L (bnd_cons C CL);
% 8.92/8.47 ALL F L. bnd_admin_file_has_level_h bnd_admin F L bnd_nil;
% 8.92/8.47 ALL F L CL.
% 8.92/8.47 bnd_system_file_needs_level bnd_system F L -->
% 8.92/8.47 bnd_admin_file_has_compartments bnd_admin F CL -->
% 8.92/8.47 bnd_admin_file_has_level_h bnd_admin F L CL -->
% 8.92/8.47 bnd_admin_file_has_level bnd_admin F L;
% 8.92/8.47 ALL F CL C1 CL1 SSO.
% 8.92/8.47 bnd_admin_compartment_has_sso bnd_admin C1 SSO -->
% 8.92/8.47 bnd_sso_file_has_compartments SSO F CL -->
% 8.92/8.47 bnd_admin_file_has_compartments_h bnd_admin F CL CL1 -->
% 8.92/8.47 bnd_admin_file_has_compartments_h bnd_admin F CL (bnd_cons C1 CL1);
% 8.92/8.47 ALL F CL. bnd_admin_file_has_compartments_h bnd_admin F CL bnd_nil;
% 8.92/8.47 ALL F CL.
% 8.92/8.47 bnd_system_file_needs_compartments bnd_system F CL -->
% 8.92/8.47 bnd_admin_file_has_compartments_h bnd_admin F CL CL -->
% 8.92/8.47 bnd_admin_file_has_compartments bnd_admin F CL;
% 8.92/8.47 ALL OCA C SSO SCG.
% 8.92/8.47 bnd_system_indi_is_oca bnd_system OCA -->
% 8.92/8.47 bnd_oca_compartment_has_scg OCA C SCG -->
% 8.92/8.47 bnd_admin_compartment_has_sso bnd_admin C SSO -->
% 8.92/8.47 bnd_sso_compartment_has_scg SSO C SCG -->
% 8.92/8.47 bnd_admin_compartment_has_scg bnd_admin C SCG;
% 8.92/8.47 ALL C SSO.
% 8.92/8.47 bnd_system_compartment_has_sso bnd_system C SSO -->
% 8.92/8.47 bnd_admin_compartment_has_sso bnd_admin C SSO;
% 8.92/8.47 ALL K L L1 L11.
% 8.92/8.47 bnd_loca_level_direct_below K L1 L11 -->
% 8.92/8.47 bnd_loca_level_below K L L1 --> bnd_loca_level_below K L L11;
% 8.92/8.47 ALL K L. bnd_loca_level_below K L L;
% 8.92/8.47 ALL K. bnd_loca_level_direct_below K bnd_secret bnd_topsecret;
% 8.92/8.47 ALL K. bnd_loca_level_direct_below K bnd_confidential bnd_secret;
% 8.92/8.47 ALL K. bnd_loca_level_direct_below K bnd_sbu bnd_confidential;
% 8.92/8.47 ALL K. bnd_loca_level_direct_below K bnd_unclassified bnd_sbu |]
% 8.92/8.47 ==> bnd_admin_indi_may_file bnd_admin bnd_alice bnd_not_secretfile bnd_read
% 8.92/8.47 Adding axioms...
% 8.92/8.48 Typedef.type_definition_def
% 19.72/19.24 ...done.
% 19.72/19.26 Ground types: ?'b, TPTP_Interpret.ind
% 19.72/19.26 Translating term (sizes: 1, 1) ...
% 26.14/25.68 Invoking SAT solver...
% 26.14/25.68 No model exists.
% 26.14/25.68 Translating term (sizes: 2, 1) ...
% 33.36/32.80 Invoking SAT solver...
% 33.36/32.80 No model exists.
% 33.36/32.80 Translating term (sizes: 1, 2) ...
% 132.81/131.99 Invoking SAT solver...
% 137.75/136.84 Model found:
% 137.75/136.84 Size of types: ?'b: 1, TPTP_Interpret.ind: 2
% 137.75/136.84 bnd_loca_level_direct_below: {(??.TPTP_Interpret.ind0,
% 137.75/136.84 {(??.TPTP_Interpret.ind0,
% 137.75/136.84 {(??.TPTP_Interpret.ind0, True), (??.TPTP_Interpret.ind1, False)}),
% 137.75/136.84 (??.TPTP_Interpret.ind1,
% 137.75/136.84 {(??.TPTP_Interpret.ind0, False), (??.TPTP_Interpret.ind1, True)})}),
% 137.75/136.84 (??.TPTP_Interpret.ind1,
% 137.75/136.84 {(??.TPTP_Interpret.ind0,
% 137.75/136.84 {(??.TPTP_Interpret.ind0, True), (??.TPTP_Interpret.ind1, False)}),
% 137.75/136.84 (??.TPTP_Interpret.ind1,
% 137.75/136.84 {(??.TPTP_Interpret.ind0, False), (??.TPTP_Interpret.ind1, True)})})}
% 137.75/136.84 bnd_admin_file_has_compartments_h: {(??.TPTP_Interpret.ind0,
% 137.75/136.84 {(??.TPTP_Interpret.ind0,
% 137.75/136.84 {(??.TPTP_Interpret.ind0,
% 137.75/136.84 {(??.TPTP_Interpret.ind0, True), (??.TPTP_Interpret.ind1, True)}),
% 137.75/136.84 (??.TPTP_Interpret.ind1,
% 137.75/136.84 {(??.TPTP_Interpret.ind0, True), (??.TPTP_Interpret.ind1, True)})}),
% 137.75/136.84 (??.TPTP_Interpret.ind1,
% 137.75/136.84 {(??.TPTP_Interpret.ind0,
% 137.75/136.84 {(??.TPTP_Interpret.ind0, True), (??.TPTP_Interpret.ind1, True)}),
% 137.75/136.84 (??.TPTP_Interpret.ind1,
% 137.75/136.84 {(??.TPTP_Interpret.ind0, True), (??.TPTP_Interpret.ind1, True)})})}),
% 137.75/136.84 (??.TPTP_Interpret.ind1,
% 137.75/136.84 {(??.TPTP_Interpret.ind0,
% 137.75/136.84 {(??.TPTP_Interpret.ind0,
% 137.75/136.84 {(??.TPTP_Interpret.ind0, True), (??.TPTP_Interpret.ind1, True)}),
% 137.75/136.84 (??.TPTP_Interpret.ind1,
% 137.75/136.84 {(??.TPTP_Interpret.ind0, True), (??.TPTP_Interpret.ind1, True)})}),
% 137.75/136.84 (??.TPTP_Interpret.ind1,
% 137.75/136.84 {(??.TPTP_Interpret.ind0,
% 137.75/136.84 {(??.TPTP_Interpret.ind0, True), (??.TPTP_Interpret.ind1, True)}),
% 137.75/136.84 (??.TPTP_Interpret.ind1,
% 137.75/136.84 {(??.TPTP_Interpret.ind0, True), (??.TPTP_Interpret.ind1, True)})})})}
% 137.75/136.84 bnd_admin_file_has_level_h: {(??.TPTP_Interpret.ind0,
% 137.75/136.84 {(??.TPTP_Interpret.ind0,
% 137.75/136.84 {(??.TPTP_Interpret.ind0,
% 137.75/136.84 {(??.TPTP_Interpret.ind0, True), (??.TPTP_Interpret.ind1, True)}),
% 137.75/136.84 (??.TPTP_Interpret.ind1,
% 137.75/136.84 {(??.TPTP_Interpret.ind0, True), (??.TPTP_Interpret.ind1, True)})}),
% 137.75/136.84 (??.TPTP_Interpret.ind1,
% 137.75/136.84 {(??.TPTP_Interpret.ind0,
% 137.75/136.84 {(??.TPTP_Interpret.ind0, True), (??.TPTP_Interpret.ind1, True)}),
% 137.75/136.84 (??.TPTP_Interpret.ind1,
% 137.75/136.84 {(??.TPTP_Interpret.ind0, True), (??.TPTP_Interpret.ind1, True)})})}),
% 137.75/136.84 (??.TPTP_Interpret.ind1,
% 137.75/136.84 {(??.TPTP_Interpret.ind0,
% 137.75/136.84 {(??.TPTP_Interpret.ind0,
% 137.75/136.84 {(??.TPTP_Interpret.ind0, True), (??.TPTP_Interpret.ind1, True)}),
% 137.75/136.84 (??.TPTP_Interpret.ind1,
% 137.75/136.84 {(??.TPTP_Interpret.ind0, True), (??.TPTP_Interpret.ind1, True)})}),
% 137.75/136.84 (??.TPTP_Interpret.ind1,
% 137.75/136.84 {(??.TPTP_Interpret.ind0,
% 137.75/136.84 {(??.TPTP_Interpret.ind0, True), (??.TPTP_Interpret.ind1, True)}),
% 137.75/136.84 (??.TPTP_Interpret.ind1,
% 137.75/136.84 {(??.TPTP_Interpret.ind0, True), (??.TPTP_Interpret.ind1, True)})})})}
% 137.75/136.84 bnd_admin_file_has_citizenship_h: {(??.TPTP_Interpret.ind0,
% 137.75/136.84 {(??.TPTP_Interpret.ind0,
% 137.75/136.84 {(??.TPTP_Interpret.ind0,
% 137.75/136.84 {(??.TPTP_Interpret.ind0, True), (??.TPTP_Interpret.ind1, True)}),
% 137.75/136.84 (??.TPTP_Interpret.ind1,
% 137.75/136.84 {(??.TPTP_Interpret.ind0, True), (??.TPTP_Interpret.ind1, True)})}),
% 137.75/136.84 (??.TPTP_Interpret.ind1,
% 137.75/136.84 {(??.TPTP_Interpret.ind0,
% 137.75/136.84 {(??.TPTP_Interpret.ind0, True), (??.TPTP_Interpret.ind1, True)}),
% 137.75/136.84 (??.TPTP_Interpret.ind1,
% 137.75/136.84 {(??.TPTP_Interpret.ind0, True), (??.TPTP_Interpret.ind1, True)})})}),
% 137.75/136.84 (??.TPTP_Interpret.ind1,
% 137.75/136.84 {(??.TPTP_Interpret.ind0,
% 137.75/136.84 {(??.TPTP_Interpret.ind0,
% 137.75/136.84 {(??.TPTP_Interpret.ind0, True), (??.TPTP_Interpret.ind1, True)}),
% 137.75/136.84 (??.TPTP_Interpret.ind1,
% 137.75/136.84 {(??.TPTP_Interpret.ind0, True), (??.TPTP_Interpret.ind1, True)})}),
% 137.75/136.84 (??.TPTP_Interpret.ind1,
% 137.75/136.84 {(??.TPTP_Interpret.ind0,
% 137.75/136.84 {(??.TPTP_Interpret.ind0, True), (??.TPTP_Interpret.ind1, True)}),
% 137.75/136.84 (??.TPTP_Interpret.ind1,
% 137.75/136.84 {(??.TPTP_Interpret.ind0, True), (??.TPTP_Interpret.ind1, True)})})})}
% 137.75/136.84 bnd_admin_compartment_has_scg: {(??.TPTP_Interpret.ind0,
% 137.75/136.84 {(??.TPTP_Interpret.ind0,
% 137.75/136.84 {(??.TPTP_Interpret.ind0, False), (??.TPTP_Interpret.ind1, True)}),
% 137.75/136.84 (??.TPTP_Interpret.ind1,
% 137.75/136.84 {(??.TPTP_Interpret.ind0, False), (??.TPTP_Interpret.ind1, False)})}),
% 137.75/136.84 (??.TPTP_Interpret.ind1,
% 137.75/136.84 {(??.TPTP_Interpret.ind0,
% 137.75/136.84 {(??.TPTP_Interpret.ind0, False), (??.TPTP_Interpret.ind1, False)}),
% 137.75/136.84 (??.TPTP_Interpret.ind1,
% 137.75/136.84 {(??.TPTP_Interpret.ind0, False), (??.TPTP_Interpret.ind1, False)})})}
% 137.75/136.84 bnd_loca_level_below: {(??.TPTP_Interpret.ind0,
% 137.75/136.84 {(??.TPTP_Interpret.ind0,
% 137.75/136.84 {(??.TPTP_Interpret.ind0, True), (??.TPTP_Interpret.ind1, False)}),
% 137.75/136.84 (??.TPTP_Interpret.ind1,
% 137.75/136.84 {(??.TPTP_Interpret.ind0, False), (??.TPTP_Interpret.ind1, True)})}),
% 137.75/136.84 (??.TPTP_Interpret.ind1,
% 137.75/136.84 {(??.TPTP_Interpret.ind0,
% 137.75/136.84 {(??.TPTP_Interpret.ind0, True), (??.TPTP_Interpret.ind1, False)}),
% 137.75/136.84 (??.TPTP_Interpret.ind1,
% 137.75/136.84 {(??.TPTP_Interpret.ind0, False), (??.TPTP_Interpret.ind1, True)})})}
% 137.75/136.84 bnd_admin_compartment_has_sso: {(??.TPTP_Interpret.ind0,
% 137.75/136.84 {(??.TPTP_Interpret.ind0,
% 137.75/136.84 {(??.TPTP_Interpret.ind0, False), (??.TPTP_Interpret.ind1, True)}),
% 137.75/136.84 (??.TPTP_Interpret.ind1,
% 137.75/136.84 {(??.TPTP_Interpret.ind0, False), (??.TPTP_Interpret.ind1, False)})}),
% 137.75/136.84 (??.TPTP_Interpret.ind1,
% 137.75/136.84 {(??.TPTP_Interpret.ind0,
% 137.75/136.84 {(??.TPTP_Interpret.ind0, False), (??.TPTP_Interpret.ind1, False)}),
% 137.75/136.84 (??.TPTP_Interpret.ind1,
% 137.75/136.84 {(??.TPTP_Interpret.ind0, False), (??.TPTP_Interpret.ind1, False)})})}
% 137.75/136.84 bnd_admin_indi_has_employment: {(??.TPTP_Interpret.ind0,
% 137.75/136.84 {(??.TPTP_Interpret.ind0, False), (??.TPTP_Interpret.ind1, True)}),
% 137.75/136.84 (??.TPTP_Interpret.ind1,
% 137.75/136.84 {(??.TPTP_Interpret.ind0, False), (??.TPTP_Interpret.ind1, False)})}
% 137.75/136.84 bnd_admin_indi_has_background_for_compartment: {(??.TPTP_Interpret.ind0,
% 137.75/136.84 {(??.TPTP_Interpret.ind0,
% 137.75/136.84 {(??.TPTP_Interpret.ind0, True), (??.TPTP_Interpret.ind1, True)}),
% 137.75/136.84 (??.TPTP_Interpret.ind1,
% 137.75/136.84 {(??.TPTP_Interpret.ind0, True), (??.TPTP_Interpret.ind1, True)})}),
% 137.75/136.84 (??.TPTP_Interpret.ind1,
% 137.75/136.84 {(??.TPTP_Interpret.ind0,
% 137.75/136.84 {(??.TPTP_Interpret.ind0, True), (??.TPTP_Interpret.ind1, True)}),
% 137.75/136.84 (??.TPTP_Interpret.ind1,
% 137.75/136.84 {(??.TPTP_Interpret.ind0, True), (??.TPTP_Interpret.ind1, True)})})}
% 137.75/136.84 bnd_admin_indi_has_background: {(??.TPTP_Interpret.ind0,
% 137.75/136.84 {(??.TPTP_Interpret.ind0,
% 137.75/136.84 {(??.TPTP_Interpret.ind0, False), (??.TPTP_Interpret.ind1, True)}),
% 137.75/136.84 (??.TPTP_Interpret.ind1,
% 137.75/136.84 {(??.TPTP_Interpret.ind0, False), (??.TPTP_Interpret.ind1, True)})}),
% 137.75/136.84 (??.TPTP_Interpret.ind1,
% 137.75/136.84 {(??.TPTP_Interpret.ind0,
% 137.75/136.84 {(??.TPTP_Interpret.ind0, False), (??.TPTP_Interpret.ind1, False)}),
% 137.75/136.84 (??.TPTP_Interpret.ind1,
% 137.75/136.84 {(??.TPTP_Interpret.ind0, False), (??.TPTP_Interpret.ind1, False)})})}
% 137.75/136.84 bnd_admin_indi_has_level_for_compartment: {(??.TPTP_Interpret.ind0,
% 137.75/136.84 {(??.TPTP_Interpret.ind0,
% 137.75/136.84 {(??.TPTP_Interpret.ind0, True), (??.TPTP_Interpret.ind1, True)}),
% 137.75/136.84 (??.TPTP_Interpret.ind1,
% 137.75/136.84 {(??.TPTP_Interpret.ind0, True), (??.TPTP_Interpret.ind1, True)})}),
% 137.75/136.84 (??.TPTP_Interpret.ind1,
% 137.75/136.84 {(??.TPTP_Interpret.ind0,
% 137.75/136.84 {(??.TPTP_Interpret.ind0, True), (??.TPTP_Interpret.ind1, True)}),
% 137.75/136.84 (??.TPTP_Interpret.ind1,
% 137.75/136.84 {(??.TPTP_Interpret.ind0, True), (??.TPTP_Interpret.ind1, True)})})}
% 137.75/136.84 bnd_admin_indi_has_polygraph: {(??.TPTP_Interpret.ind0,
% 137.75/136.84 {(??.TPTP_Interpret.ind0, False), (??.TPTP_Interpret.ind1, True)}),
% 137.75/136.84 (??.TPTP_Interpret.ind1,
% 137.75/136.84 {(??.TPTP_Interpret.ind0, False), (??.TPTP_Interpret.ind1, False)})}
% 137.75/136.84 bnd_admin_indi_has_polygraph_for_compartment: {(??.TPTP_Interpret.ind0,
% 137.75/136.84 {(??.TPTP_Interpret.ind0,
% 137.75/136.84 {(??.TPTP_Interpret.ind0, True), (??.TPTP_Interpret.ind1, True)}),
% 137.75/136.84 (??.TPTP_Interpret.ind1,
% 137.75/136.84 {(??.TPTP_Interpret.ind0, True), (??.TPTP_Interpret.ind1, True)})}),
% 137.75/136.84 (??.TPTP_Interpret.ind1,
% 137.75/136.84 {(??.TPTP_Interpret.ind0,
% 137.75/136.84 {(??.TPTP_Interpret.ind0, True), (??.TPTP_Interpret.ind1, True)}),
% 137.75/136.84 (??.TPTP_Interpret.ind1,
% 137.75/136.84 {(??.TPTP_Interpret.ind0, True), (??.TPTP_Interpret.ind1, True)})})}
% 137.75/136.84 bnd_admin_indi_has_credit: {(??.TPTP_Interpret.ind0,
% 137.75/136.84 {(??.TPTP_Interpret.ind0, False), (??.TPTP_Interpret.ind1, True)}),
% 137.75/136.84 (??.TPTP_Interpret.ind1,
% 137.75/136.84 {(??.TPTP_Interpret.ind0, False), (??.TPTP_Interpret.ind1, False)})}
% 137.75/136.84 bnd_admin_indi_has_credit_for_compartment: {(??.TPTP_Interpret.ind0,
% 137.75/136.84 {(??.TPTP_Interpret.ind0,
% 137.75/136.84 {(??.TPTP_Interpret.ind0, True), (??.TPTP_Interpret.ind1, True)}),
% 137.75/136.84 (??.TPTP_Interpret.ind1,
% 137.75/136.84 {(??.TPTP_Interpret.ind0, True), (??.TPTP_Interpret.ind1, True)})}),
% 137.75/136.84 (??.TPTP_Interpret.ind1,
% 137.75/136.84 {(??.TPTP_Interpret.ind0,
% 137.75/136.84 {(??.TPTP_Interpret.ind0, True), (??.TPTP_Interpret.ind1, True)}),
% 137.75/136.84 (??.TPTP_Interpret.ind1,
% 137.75/136.84 {(??.TPTP_Interpret.ind0, True), (??.TPTP_Interpret.ind1, True)})})}
% 137.75/136.84 bnd_admin_indi_has_compartments: {(??.TPTP_Interpret.ind0,
% 137.75/136.84 {(??.TPTP_Interpret.ind0,
% 137.75/136.84 {(??.TPTP_Interpret.ind0, True), (??.TPTP_Interpret.ind1, True)}),
% 137.75/136.84 (??.TPTP_Interpret.ind1,
% 137.75/136.84 {(??.TPTP_Interpret.ind0, True), (??.TPTP_Interpret.ind1, True)})}),
% 137.75/136.84 (??.TPTP_Interpret.ind1,
% 137.75/136.84 {(??.TPTP_Interpret.ind0,
% 137.75/136.84 {(??.TPTP_Interpret.ind0, True), (??.TPTP_Interpret.ind1, True)}),
% 137.75/136.84 (??.TPTP_Interpret.ind1,
% 137.75/136.84 {(??.TPTP_Interpret.ind0, True), (??.TPTP_Interpret.ind1, True)})})}
% 137.75/136.84 bnd_admin_file_has_compartments: {(??.TPTP_Interpret.ind0,
% 137.75/136.84 {(??.TPTP_Interpret.ind0,
% 137.75/136.84 {(??.TPTP_Interpret.ind0, True), (??.TPTP_Interpret.ind1, False)}),
% 137.75/136.84 (??.TPTP_Interpret.ind1,
% 137.75/136.84 {(??.TPTP_Interpret.ind0, True), (??.TPTP_Interpret.ind1, False)})}),
% 137.75/136.84 (??.TPTP_Interpret.ind1,
% 137.75/136.84 {(??.TPTP_Interpret.ind0,
% 137.75/136.84 {(??.TPTP_Interpret.ind0, False), (??.TPTP_Interpret.ind1, False)}),
% 137.75/136.84 (??.TPTP_Interpret.ind1,
% 137.75/136.84 {(??.TPTP_Interpret.ind0, False), (??.TPTP_Interpret.ind1, False)})})}
% 137.75/136.84 bnd_admin_indi_has_level: {(??.TPTP_Interpret.ind0,
% 137.75/136.84 {(??.TPTP_Interpret.ind0,
% 137.75/136.84 {(??.TPTP_Interpret.ind0, False), (??.TPTP_Interpret.ind1, True)}),
% 137.75/136.84 (??.TPTP_Interpret.ind1,
% 137.75/136.84 {(??.TPTP_Interpret.ind0, False), (??.TPTP_Interpret.ind1, True)})}),
% 137.75/136.84 (??.TPTP_Interpret.ind1,
% 137.75/136.84 {(??.TPTP_Interpret.ind0,
% 137.75/136.84 {(??.TPTP_Interpret.ind0, False), (??.TPTP_Interpret.ind1, False)}),
% 137.75/136.84 (??.TPTP_Interpret.ind1,
% 137.75/136.84 {(??.TPTP_Interpret.ind0, False), (??.TPTP_Interpret.ind1, False)})})}
% 137.75/136.84 bnd_admin_file_has_level: {(??.TPTP_Interpret.ind0,
% 137.75/136.84 {(??.TPTP_Interpret.ind0,
% 137.75/136.84 {(??.TPTP_Interpret.ind0, True), (??.TPTP_Interpret.ind1, True)}),
% 137.75/136.84 (??.TPTP_Interpret.ind1,
% 137.75/136.84 {(??.TPTP_Interpret.ind0, True), (??.TPTP_Interpret.ind1, True)})}),
% 137.75/136.84 (??.TPTP_Interpret.ind1,
% 137.75/136.84 {(??.TPTP_Interpret.ind0,
% 137.75/136.84 {(??.TPTP_Interpret.ind0, True), (??.TPTP_Interpret.ind1, True)}),
% 137.75/136.84 (??.TPTP_Interpret.ind1,
% 137.75/136.84 {(??.TPTP_Interpret.ind0, True), (??.TPTP_Interpret.ind1, True)})})}
% 137.75/136.84 bnd_admin_file_has_citizenship: {(??.TPTP_Interpret.ind0,
% 137.75/136.84 {(??.TPTP_Interpret.ind0,
% 137.75/136.84 {(??.TPTP_Interpret.ind0, True), (??.TPTP_Interpret.ind1, True)}),
% 137.75/136.84 (??.TPTP_Interpret.ind1,
% 137.75/136.84 {(??.TPTP_Interpret.ind0, True), (??.TPTP_Interpret.ind1, True)})}),
% 137.75/136.84 (??.TPTP_Interpret.ind1,
% 137.75/136.84 {(??.TPTP_Interpret.ind0,
% 137.75/136.84 {(??.TPTP_Interpret.ind0, True), (??.TPTP_Interpret.ind1, True)}),
% 137.75/136.84 (??.TPTP_Interpret.ind1,
% 137.75/136.84 {(??.TPTP_Interpret.ind0, True), (??.TPTP_Interpret.ind1, True)})})}
% 137.75/136.84 bnd_admin_indi_has_citizenship: {(??.TPTP_Interpret.ind0,
% 137.75/136.84 {(??.TPTP_Interpret.ind0,
% 137.75/136.84 {(??.TPTP_Interpret.ind0, False), (??.TPTP_Interpret.ind1, True)}),
% 137.75/136.84 (??.TPTP_Interpret.ind1,
% 137.75/136.84 {(??.TPTP_Interpret.ind0, True), (??.TPTP_Interpret.ind1, True)})}),
% 137.75/136.84 (??.TPTP_Interpret.ind1,
% 137.75/136.84 {(??.TPTP_Interpret.ind0,
% 137.75/136.84 {(??.TPTP_Interpret.ind0, False), (??.TPTP_Interpret.ind1, False)}),
% 137.75/136.84 (??.TPTP_Interpret.ind1,
% 137.75/136.84 {(??.TPTP_Interpret.ind0, False), (??.TPTP_Interpret.ind1, False)})})}
% 137.75/136.84 bnd_admin_indi_has_compartments_for_file: {(??.TPTP_Interpret.ind0,
% 137.75/136.84 {(??.TPTP_Interpret.ind0,
% 137.75/136.84 {(??.TPTP_Interpret.ind0, True), (??.TPTP_Interpret.ind1, True)}),
% 137.75/136.84 (??.TPTP_Interpret.ind1,
% 137.75/136.84 {(??.TPTP_Interpret.ind0, True), (??.TPTP_Interpret.ind1, True)})}),
% 137.75/136.84 (??.TPTP_Interpret.ind1,
% 137.75/136.84 {(??.TPTP_Interpret.ind0,
% 137.75/136.84 {(??.TPTP_Interpret.ind0, True), (??.TPTP_Interpret.ind1, True)}),
% 137.75/136.84 (??.TPTP_Interpret.ind1,
% 137.75/136.84 {(??.TPTP_Interpret.ind0, True), (??.TPTP_Interpret.ind1, True)})})}
% 137.75/136.84 bnd_admin_indi_has_level_for_file: {(??.TPTP_Interpret.ind0,
% 137.75/136.84 {(??.TPTP_Interpret.ind0,
% 137.75/136.84 {(??.TPTP_Interpret.ind0, True), (??.TPTP_Interpret.ind1, True)}),
% 137.75/136.84 (??.TPTP_Interpret.ind1,
% 137.75/136.84 {(??.TPTP_Interpret.ind0, True), (??.TPTP_Interpret.ind1, True)})}),
% 137.75/136.84 (??.TPTP_Interpret.ind1,
% 137.75/136.84 {(??.TPTP_Interpret.ind0,
% 137.75/136.84 {(??.TPTP_Interpret.ind0, True), (??.TPTP_Interpret.ind1, True)}),
% 137.75/136.84 (??.TPTP_Interpret.ind1,
% 137.75/136.84 {(??.TPTP_Interpret.ind0, True), (??.TPTP_Interpret.ind1, True)})})}
% 137.75/136.84 bnd_admin_indi_has_need_to_know_for_file: {(??.TPTP_Interpret.ind0,
% 137.75/136.84 {(??.TPTP_Interpret.ind0,
% 137.75/136.84 {(??.TPTP_Interpret.ind0, True), (??.TPTP_Interpret.ind1, True)}),
% 137.75/136.84 (??.TPTP_Interpret.ind1,
% 137.75/136.84 {(??.TPTP_Interpret.ind0, True), (??.TPTP_Interpret.ind1, False)})}),
% 137.75/136.84 (??.TPTP_Interpret.ind1,
% 137.75/136.84 {(??.TPTP_Interpret.ind0,
% 137.75/136.84 {(??.TPTP_Interpret.ind0, True), (??.TPTP_Interpret.ind1, True)}),
% 137.75/136.84 (??.TPTP_Interpret.ind1,
% 137.75/136.84 {(??.TPTP_Interpret.ind0, True), (??.TPTP_Interpret.ind1, True)})})}
% 137.75/136.84 bnd_admin_indi_has_citizenship_for_file: {(??.TPTP_Interpret.ind0,
% 137.75/136.84 {(??.TPTP_Interpret.ind0,
% 137.75/136.84 {(??.TPTP_Interpret.ind0, True), (??.TPTP_Interpret.ind1, True)}),
% 137.75/136.84 (??.TPTP_Interpret.ind1,
% 137.75/136.84 {(??.TPTP_Interpret.ind0, True), (??.TPTP_Interpret.ind1, True)})}),
% 137.75/136.84 (??.TPTP_Interpret.ind1,
% 137.75/136.84 {(??.TPTP_Interpret.ind0,
% 137.75/136.84 {(??.TPTP_Interpret.ind0, True), (??.TPTP_Interpret.ind1, True)}),
% 137.75/136.84 (??.TPTP_Interpret.ind1,
% 137.75/136.84 {(??.TPTP_Interpret.ind0, True), (??.TPTP_Interpret.ind1, True)})})}
% 137.75/136.84 bnd_read: ??.TPTP_Interpret.ind0
% 137.75/136.84 bnd_admin: ??.TPTP_Interpret.ind0
% 137.75/136.84 bnd_admin_indi_may_file: {(??.TPTP_Interpret.ind0,
% 137.75/136.84 {(??.TPTP_Interpret.ind0,
% 137.75/136.84 {(??.TPTP_Interpret.ind0,
% 137.75/136.84 {(??.TPTP_Interpret.ind0, True), (??.TPTP_Interpret.ind1, True)}),
% 137.75/136.84 (??.TPTP_Interpret.ind1,
% 137.75/136.84 {(??.TPTP_Interpret.ind0, True), (??.TPTP_Interpret.ind1, True)})}),
% 137.75/136.84 (??.TPTP_Interpret.ind1,
% 137.75/136.84 {(??.TPTP_Interpret.ind0,
% 137.75/136.84 {(??.TPTP_Interpret.ind0, True), (??.TPTP_Interpret.ind1, True)}),
% 137.75/136.84 (??.TPTP_Interpret.ind1,
% 137.75/136.84 {(??.TPTP_Interpret.ind0, False),
% 137.75/136.84 (??.TPTP_Interpret.ind1, True)})})}),
% 137.75/136.84 (??.TPTP_Interpret.ind1,
% 137.75/136.84 {(??.TPTP_Interpret.ind0,
% 137.75/136.84 {(??.TPTP_Interpret.ind0,
% 137.75/136.84 {(??.TPTP_Interpret.ind0, True), (??.TPTP_Interpret.ind1, True)}),
% 137.75/136.84 (??.TPTP_Interpret.ind1,
% 137.75/136.84 {(??.TPTP_Interpret.ind0, True), (??.TPTP_Interpret.ind1, True)})}),
% 137.75/136.84 (??.TPTP_Interpret.ind1,
% 137.75/136.84 {(??.TPTP_Interpret.ind0,
% 137.75/136.84 {(??.TPTP_Interpret.ind0, True), (??.TPTP_Interpret.ind1, True)}),
% 137.75/136.84 (??.TPTP_Interpret.ind1,
% 137.75/136.84 {(??.TPTP_Interpret.ind0, True), (??.TPTP_Interpret.ind1, True)})})})}
% 137.75/136.84 bnd_system_indi_is_oca: {(??.TPTP_Interpret.ind0,
% 137.75/136.84 {(??.TPTP_Interpret.ind0, False), (??.TPTP_Interpret.ind1, True)}),
% 137.75/136.84 (??.TPTP_Interpret.ind1,
% 137.75/136.84 {(??.TPTP_Interpret.ind0, False), (??.TPTP_Interpret.ind1, False)})}
% 137.75/136.84 bnd_yes: ??.TPTP_Interpret.ind0
% 137.75/136.84 bnd_confidential: ??.TPTP_Interpret.ind1
% 137.75/136.84 bnd_no: ??.TPTP_Interpret.ind0
% 137.75/136.84 bnd_sbu: ??.TPTP_Interpret.ind1
% 137.75/136.84 bnd_oca_compartment_is_compartment: {(??.TPTP_Interpret.ind0,
% 137.75/136.84 {(??.TPTP_Interpret.ind0,
% 137.75/136.84 {(??.TPTP_Interpret.ind0,
% 137.75/136.84 {(??.TPTP_Interpret.ind0,
% 137.75/136.84 {(??.TPTP_Interpret.ind0,
% 137.75/136.84 {(??.TPTP_Interpret.ind0, False),
% 137.75/136.84 (??.TPTP_Interpret.ind1, False)}),
% 137.75/136.84 (??.TPTP_Interpret.ind1,
% 137.75/136.84 {(??.TPTP_Interpret.ind0, False),
% 137.75/136.84 (??.TPTP_Interpret.ind1, False)})}),
% 137.75/136.84 (??.TPTP_Interpret.ind1,
% 137.75/136.84 {(??.TPTP_Interpret.ind0,
% 137.75/136.84 {(??.TPTP_Interpret.ind0, False),
% 137.75/136.84 (??.TPTP_Interpret.ind1, False)}),
% 137.75/136.84 (??.TPTP_Interpret.ind1,
% 137.75/136.84 {(??.TPTP_Interpret.ind0, False),
% 137.75/136.84 (??.TPTP_Interpret.ind1, False)})})}),
% 137.75/136.84 (??.TPTP_Interpret.ind1,
% 137.75/136.84 {(??.TPTP_Interpret.ind0,
% 137.75/136.84 {(??.TPTP_Interpret.ind0,
% 137.75/136.84 {(??.TPTP_Interpret.ind0, False),
% 137.75/136.84 (??.TPTP_Interpret.ind1, False)}),
% 137.75/136.84 (??.TPTP_Interpret.ind1,
% 137.75/136.84 {(??.TPTP_Interpret.ind0, False),
% 137.75/136.84 (??.TPTP_Interpret.ind1, False)})}),
% 137.75/136.84 (??.TPTP_Interpret.ind1,
% 137.75/136.84 {(??.TPTP_Interpret.ind0,
% 137.75/136.84 {(??.TPTP_Interpret.ind0, False),
% 137.75/136.84 (??.TPTP_Interpret.ind1, False)}),
% 137.75/136.84 (??.TPTP_Interpret.ind1,
% 137.75/136.84 {(??.TPTP_Interpret.ind0, False),
% 137.75/136.84 (??.TPTP_Interpret.ind1, False)})})})}),
% 137.75/136.84 (??.TPTP_Interpret.ind1,
% 137.75/136.84 {(??.TPTP_Interpret.ind0,
% 137.75/136.84 {(??.TPTP_Interpret.ind0,
% 137.75/136.84 {(??.TPTP_Interpret.ind0,
% 137.75/136.84 {(??.TPTP_Interpret.ind0, False),
% 137.75/136.84 (??.TPTP_Interpret.ind1, False)}),
% 137.75/136.84 (??.TPTP_Interpret.ind1,
% 137.75/136.84 {(??.TPTP_Interpret.ind0, False),
% 137.75/136.84 (??.TPTP_Interpret.ind1, False)})}),
% 137.75/136.84 (??.TPTP_Interpret.ind1,
% 137.75/136.84 {(??.TPTP_Interpret.ind0,
% 137.75/136.84 {(??.TPTP_Interpret.ind0, False),
% 137.75/136.84 (??.TPTP_Interpret.ind1, False)}),
% 137.75/136.84 (??.TPTP_Interpret.ind1,
% 137.75/136.84 {(??.TPTP_Interpret.ind0, False),
% 137.75/136.84 (??.TPTP_Interpret.ind1, False)})})}),
% 137.75/136.84 (??.TPTP_Interpret.ind1,
% 137.75/136.84 {(??.TPTP_Interpret.ind0,
% 137.75/136.84 {(??.TPTP_Interpret.ind0,
% 137.75/136.84 {(??.TPTP_Interpret.ind0, False),
% 137.75/136.84 (??.TPTP_Interpret.ind1, False)}),
% 137.75/136.84 (??.TPTP_Interpret.ind1,
% 137.75/136.84 {(??.TPTP_Interpret.ind0, False),
% 137.75/136.84 (??.TPTP_Interpret.ind1, False)})}),
% 137.75/136.84 (??.TPTP_Interpret.ind1,
% 137.75/136.84 {(??.TPTP_Interpret.ind0,
% 137.75/136.84 {(??.TPTP_Interpret.ind0, False),
% 137.75/136.84 (??.TPTP_Interpret.ind1, False)}),
% 137.75/136.84 (??.TPTP_Interpret.ind1,
% 137.75/136.84 {(??.TPTP_Interpret.ind0, False),
% 137.75/136.84 (??.TPTP_Interpret.ind1, False)})})})})}),
% 137.75/136.84 (??.TPTP_Interpret.ind1,
% 137.75/136.84 {(??.TPTP_Interpret.ind0,
% 137.75/136.84 {(??.TPTP_Interpret.ind0,
% 137.75/136.84 {(??.TPTP_Interpret.ind0,
% 137.75/136.84 {(??.TPTP_Interpret.ind0,
% 137.75/136.84 {(??.TPTP_Interpret.ind0, False),
% 137.75/136.84 (??.TPTP_Interpret.ind1, False)}),
% 137.75/136.84 (??.TPTP_Interpret.ind1,
% 137.75/136.84 {(??.TPTP_Interpret.ind0, False),
% 137.75/136.84 (??.TPTP_Interpret.ind1, False)})}),
% 137.75/136.84 (??.TPTP_Interpret.ind1,
% 137.75/136.84 {(??.TPTP_Interpret.ind0,
% 137.75/136.84 {(??.TPTP_Interpret.ind0, False),
% 137.75/136.84 (??.TPTP_Interpret.ind1, False)}),
% 137.75/136.84 (??.TPTP_Interpret.ind1,
% 137.75/136.84 {(??.TPTP_Interpret.ind0, False),
% 137.75/136.84 (??.TPTP_Interpret.ind1, False)})})}),
% 137.75/136.84 (??.TPTP_Interpret.ind1,
% 137.75/136.84 {(??.TPTP_Interpret.ind0,
% 137.75/136.84 {(??.TPTP_Interpret.ind0,
% 137.75/136.84 {(??.TPTP_Interpret.ind0, False),
% 137.75/136.84 (??.TPTP_Interpret.ind1, False)}),
% 137.75/136.84 (??.TPTP_Interpret.ind1,
% 137.75/136.84 {(??.TPTP_Interpret.ind0, False),
% 137.75/136.84 (??.TPTP_Interpret.ind1, False)})}),
% 137.75/136.84 (??.TPTP_Interpret.ind1,
% 137.75/136.84 {(??.TPTP_Interpret.ind0,
% 137.75/136.84 {(??.TPTP_Interpret.ind0, True),
% 137.75/136.84 (??.TPTP_Interpret.ind1, False)}),
% 137.75/136.84 (??.TPTP_Interpret.ind1,
% 137.75/136.84 {(??.TPTP_Interpret.ind0, False),
% 137.75/136.84 (??.TPTP_Interpret.ind1, False)})})})}),
% 137.75/136.84 (??.TPTP_Interpret.ind1,
% 137.75/136.84 {(??.TPTP_Interpret.ind0,
% 137.75/136.84 {(??.TPTP_Interpret.ind0,
% 137.75/136.84 {(??.TPTP_Interpret.ind0,
% 137.75/136.84 {(??.TPTP_Interpret.ind0, False),
% 137.75/136.84 (??.TPTP_Interpret.ind1, False)}),
% 137.75/136.84 (??.TPTP_Interpret.ind1,
% 137.75/136.84 {(??.TPTP_Interpret.ind0, False),
% 137.75/136.84 (??.TPTP_Interpret.ind1, False)})}),
% 137.75/136.84 (??.TPTP_Interpret.ind1,
% 137.75/136.84 {(??.TPTP_Interpret.ind0,
% 137.75/136.84 {(??.TPTP_Interpret.ind0, False),
% 137.75/136.84 (??.TPTP_Interpret.ind1, False)}),
% 137.75/136.84 (??.TPTP_Interpret.ind1,
% 137.75/136.84 {(??.TPTP_Interpret.ind0, False),
% 137.75/136.84 (??.TPTP_Interpret.ind1, False)})})}),
% 137.75/136.84 (??.TPTP_Interpret.ind1,
% 137.75/136.84 {(??.TPTP_Interpret.ind0,
% 137.75/136.84 {(??.TPTP_Interpret.ind0,
% 137.75/136.84 {(??.TPTP_Interpret.ind0, False),
% 137.75/136.84 (??.TPTP_Interpret.ind1, False)}),
% 137.75/136.84 (??.TPTP_Interpret.ind1,
% 137.75/136.84 {(??.TPTP_Interpret.ind0, False),
% 137.75/136.84 (??.TPTP_Interpret.ind1, False)})}),
% 137.75/136.84 (??.TPTP_Interpret.ind1,
% 137.75/136.84 {(??.TPTP_Interpret.ind0,
% 137.75/136.84 {(??.TPTP_Interpret.ind0, False),
% 137.75/136.84 (??.TPTP_Interpret.ind1, False)}),
% 137.75/136.84 (??.TPTP_Interpret.ind1,
% 137.75/136.84 {(??.TPTP_Interpret.ind0, False),
% 137.75/136.84 (??.TPTP_Interpret.ind1, False)})})})})})}
% 137.75/136.84 bnd_system_compartment_has_sso: {(??.TPTP_Interpret.ind0,
% 137.75/136.84 {(??.TPTP_Interpret.ind0,
% 137.75/136.84 {(??.TPTP_Interpret.ind0, False), (??.TPTP_Interpret.ind1, True)}),
% 137.75/136.84 (??.TPTP_Interpret.ind1,
% 137.75/136.84 {(??.TPTP_Interpret.ind0, False), (??.TPTP_Interpret.ind1, False)})}),
% 137.75/136.84 (??.TPTP_Interpret.ind1,
% 137.75/136.84 {(??.TPTP_Interpret.ind0,
% 137.75/136.84 {(??.TPTP_Interpret.ind0, True), (??.TPTP_Interpret.ind1, True)}),
% 137.75/136.84 (??.TPTP_Interpret.ind1,
% 137.75/136.84 {(??.TPTP_Interpret.ind0, True), (??.TPTP_Interpret.ind1, True)})})}
% 137.75/136.84 bnd_oca: ??.TPTP_Interpret.ind1
% 137.75/136.84 bnd_oca_compartment_has_scg: {(??.TPTP_Interpret.ind0,
% 137.75/136.84 {(??.TPTP_Interpret.ind0,
% 137.75/136.84 {(??.TPTP_Interpret.ind0, True), (??.TPTP_Interpret.ind1, True)}),
% 137.75/136.84 (??.TPTP_Interpret.ind1,
% 137.75/136.84 {(??.TPTP_Interpret.ind0, True), (??.TPTP_Interpret.ind1, True)})}),
% 137.75/136.84 (??.TPTP_Interpret.ind1,
% 137.75/136.84 {(??.TPTP_Interpret.ind0,
% 137.75/136.84 {(??.TPTP_Interpret.ind0, False), (??.TPTP_Interpret.ind1, True)}),
% 137.75/136.84 (??.TPTP_Interpret.ind1,
% 137.75/136.84 {(??.TPTP_Interpret.ind0, True), (??.TPTP_Interpret.ind1, True)})})}
% 137.75/136.84 bnd_sso_compartment_has_scg: {(??.TPTP_Interpret.ind0,
% 137.75/136.84 {(??.TPTP_Interpret.ind0,
% 137.75/136.84 {(??.TPTP_Interpret.ind0, True), (??.TPTP_Interpret.ind1, True)}),
% 137.75/136.84 (??.TPTP_Interpret.ind1,
% 137.75/136.84 {(??.TPTP_Interpret.ind0, True), (??.TPTP_Interpret.ind1, True)})}),
% 137.75/136.84 (??.TPTP_Interpret.ind1,
% 137.75/136.84 {(??.TPTP_Interpret.ind0,
% 137.75/136.84 {(??.TPTP_Interpret.ind0, True), (??.TPTP_Interpret.ind1, True)}),
% 137.75/136.84 (??.TPTP_Interpret.ind1,
% 137.75/136.84 {(??.TPTP_Interpret.ind0, True), (??.TPTP_Interpret.ind1, True)})})}
% 137.75/136.84 bnd_cons: {(??.TPTP_Interpret.ind0,
% 137.75/136.84 {(??.TPTP_Interpret.ind0, ??.TPTP_Interpret.ind0),
% 137.75/136.84 (??.TPTP_Interpret.ind1, ??.TPTP_Interpret.ind0)}),
% 137.75/136.84 (??.TPTP_Interpret.ind1,
% 137.75/136.84 {(??.TPTP_Interpret.ind0, ??.TPTP_Interpret.ind0),
% 137.75/136.84 (??.TPTP_Interpret.ind1, ??.TPTP_Interpret.ind0)})}
% 137.75/136.84 bnd_sso_file_has_compartments: {(??.TPTP_Interpret.ind0,
% 137.75/136.84 {(??.TPTP_Interpret.ind0,
% 137.75/136.84 {(??.TPTP_Interpret.ind0, False), (??.TPTP_Interpret.ind1, False)}),
% 137.75/136.84 (??.TPTP_Interpret.ind1,
% 137.75/136.84 {(??.TPTP_Interpret.ind0, False), (??.TPTP_Interpret.ind1, False)})}),
% 137.75/136.84 (??.TPTP_Interpret.ind1,
% 137.75/136.84 {(??.TPTP_Interpret.ind0,
% 137.75/136.84 {(??.TPTP_Interpret.ind0, True), (??.TPTP_Interpret.ind1, False)}),
% 137.75/136.84 (??.TPTP_Interpret.ind1,
% 137.75/136.84 {(??.TPTP_Interpret.ind0, False), (??.TPTP_Interpret.ind1, False)})})}
% 137.75/136.84 bnd_sso_file_has_level: {(??.TPTP_Interpret.ind0,
% 137.75/136.84 {(??.TPTP_Interpret.ind0,
% 137.75/136.84 {(??.TPTP_Interpret.ind0,
% 137.75/136.84 {(??.TPTP_Interpret.ind0, False), (??.TPTP_Interpret.ind1, False)}),
% 137.75/136.84 (??.TPTP_Interpret.ind1,
% 137.75/136.84 {(??.TPTP_Interpret.ind0, False), (??.TPTP_Interpret.ind1, False)})}),
% 137.75/136.84 (??.TPTP_Interpret.ind1,
% 137.75/136.84 {(??.TPTP_Interpret.ind0,
% 137.75/136.84 {(??.TPTP_Interpret.ind0, False), (??.TPTP_Interpret.ind1, False)}),
% 137.75/136.84 (??.TPTP_Interpret.ind1,
% 137.75/136.84 {(??.TPTP_Interpret.ind0, False),
% 137.75/136.84 (??.TPTP_Interpret.ind1, False)})})}),
% 137.75/136.84 (??.TPTP_Interpret.ind1,
% 137.75/136.84 {(??.TPTP_Interpret.ind0,
% 137.75/136.84 {(??.TPTP_Interpret.ind0,
% 137.75/136.84 {(??.TPTP_Interpret.ind0, False), (??.TPTP_Interpret.ind1, False)}),
% 137.75/136.84 (??.TPTP_Interpret.ind1,
% 137.75/136.84 {(??.TPTP_Interpret.ind0, False), (??.TPTP_Interpret.ind1, True)})}),
% 137.75/136.84 (??.TPTP_Interpret.ind1,
% 137.75/136.84 {(??.TPTP_Interpret.ind0,
% 137.75/136.84 {(??.TPTP_Interpret.ind0, False), (??.TPTP_Interpret.ind1, False)}),
% 137.75/136.84 (??.TPTP_Interpret.ind1,
% 137.75/136.84 {(??.TPTP_Interpret.ind0, False),
% 137.75/136.84 (??.TPTP_Interpret.ind1, False)})})})}
% 137.75/136.84 bnd_scg_compartmentb: ??.TPTP_Interpret.ind1
% 137.75/136.84 bnd_scg_compartmenta: ??.TPTP_Interpret.ind1
% 137.75/136.84 bnd_sso_file_has_citizenship: {(??.TPTP_Interpret.ind0,
% 137.75/136.84 {(??.TPTP_Interpret.ind0,
% 137.75/136.84 {(??.TPTP_Interpret.ind0,
% 137.75/136.84 {(??.TPTP_Interpret.ind0, False), (??.TPTP_Interpret.ind1, False)}),
% 137.75/136.84 (??.TPTP_Interpret.ind1,
% 137.75/136.84 {(??.TPTP_Interpret.ind0, False), (??.TPTP_Interpret.ind1, False)})}),
% 137.75/136.84 (??.TPTP_Interpret.ind1,
% 137.75/136.84 {(??.TPTP_Interpret.ind0,
% 137.75/136.84 {(??.TPTP_Interpret.ind0, False), (??.TPTP_Interpret.ind1, False)}),
% 137.75/136.84 (??.TPTP_Interpret.ind1,
% 137.75/136.84 {(??.TPTP_Interpret.ind0, False),
% 137.75/136.84 (??.TPTP_Interpret.ind1, False)})})}),
% 137.75/136.84 (??.TPTP_Interpret.ind1,
% 137.75/136.84 {(??.TPTP_Interpret.ind0,
% 137.75/136.84 {(??.TPTP_Interpret.ind0,
% 137.75/136.84 {(??.TPTP_Interpret.ind0, False), (??.TPTP_Interpret.ind1, True)}),
% 137.75/136.84 (??.TPTP_Interpret.ind1,
% 137.75/136.84 {(??.TPTP_Interpret.ind0, False), (??.TPTP_Interpret.ind1, False)})}),
% 137.75/136.84 (??.TPTP_Interpret.ind1,
% 137.75/136.84 {(??.TPTP_Interpret.ind0,
% 137.75/136.84 {(??.TPTP_Interpret.ind0, False), (??.TPTP_Interpret.ind1, False)}),
% 137.75/136.84 (??.TPTP_Interpret.ind1,
% 137.75/136.84 {(??.TPTP_Interpret.ind0, False),
% 137.75/136.84 (??.TPTP_Interpret.ind1, False)})})})}
% 137.75/136.84 bnd_state_file_is_not_working_paper: {(??.TPTP_Interpret.ind0, True), (??.TPTP_Interpret.ind1, True)}
% 137.75/136.84 bnd_nil: ??.TPTP_Interpret.ind0
% 137.75/136.84 bnd_system_file_needs_compartments: {(??.TPTP_Interpret.ind0,
% 137.75/136.84 {(??.TPTP_Interpret.ind0,
% 137.75/136.84 {(??.TPTP_Interpret.ind0, True), (??.TPTP_Interpret.ind1, False)}),
% 137.75/136.84 (??.TPTP_Interpret.ind1,
% 137.75/136.84 {(??.TPTP_Interpret.ind0, True), (??.TPTP_Interpret.ind1, False)})}),
% 137.75/136.84 (??.TPTP_Interpret.ind1,
% 137.75/136.84 {(??.TPTP_Interpret.ind0,
% 137.75/136.84 {(??.TPTP_Interpret.ind0, True), (??.TPTP_Interpret.ind1, True)}),
% 137.75/136.84 (??.TPTP_Interpret.ind1,
% 137.75/136.84 {(??.TPTP_Interpret.ind0, True), (??.TPTP_Interpret.ind1, True)})})}
% 137.75/136.84 bnd_unclassified: ??.TPTP_Interpret.ind1
% 137.75/136.84 bnd_system_file_needs_level: {(??.TPTP_Interpret.ind0,
% 137.75/136.84 {(??.TPTP_Interpret.ind0,
% 137.75/136.84 {(??.TPTP_Interpret.ind0, True), (??.TPTP_Interpret.ind1, True)}),
% 137.75/136.84 (??.TPTP_Interpret.ind1,
% 137.75/136.84 {(??.TPTP_Interpret.ind0, True), (??.TPTP_Interpret.ind1, True)})}),
% 137.75/136.84 (??.TPTP_Interpret.ind1,
% 137.75/136.84 {(??.TPTP_Interpret.ind0,
% 137.75/136.84 {(??.TPTP_Interpret.ind0, True), (??.TPTP_Interpret.ind1, True)}),
% 137.75/136.84 (??.TPTP_Interpret.ind1,
% 137.75/136.84 {(??.TPTP_Interpret.ind0, True), (??.TPTP_Interpret.ind1, True)})})}
% 137.75/136.84 bnd_anycountry: ??.TPTP_Interpret.ind1
% 137.75/136.84 bnd_system_file_needs_citizenship: {(??.TPTP_Interpret.ind0,
% 137.75/136.84 {(??.TPTP_Interpret.ind0,
% 137.75/136.84 {(??.TPTP_Interpret.ind0, True), (??.TPTP_Interpret.ind1, True)}),
% 137.75/136.84 (??.TPTP_Interpret.ind1,
% 137.75/136.84 {(??.TPTP_Interpret.ind0, True), (??.TPTP_Interpret.ind1, True)})}),
% 137.75/136.84 (??.TPTP_Interpret.ind1,
% 137.75/136.84 {(??.TPTP_Interpret.ind0,
% 137.75/136.84 {(??.TPTP_Interpret.ind0, True), (??.TPTP_Interpret.ind1, True)}),
% 137.75/136.84 (??.TPTP_Interpret.ind1,
% 137.75/136.84 {(??.TPTP_Interpret.ind0, True), (??.TPTP_Interpret.ind1, True)})})}
% 137.75/136.84 bnd_state_file_has_owner: {(??.TPTP_Interpret.ind0,
% 137.75/136.84 {(??.TPTP_Interpret.ind0, True), (??.TPTP_Interpret.ind1, False)}),
% 137.75/136.84 (??.TPTP_Interpret.ind1,
% 137.75/136.84 {(??.TPTP_Interpret.ind0, False), (??.TPTP_Interpret.ind1, True)})}
% 137.75/136.84 bnd_system_indi_is_polygraph_admin: {(??.TPTP_Interpret.ind0,
% 137.75/136.84 {(??.TPTP_Interpret.ind0, True), (??.TPTP_Interpret.ind1, False)}),
% 137.75/136.84 (??.TPTP_Interpret.ind1,
% 137.75/136.84 {(??.TPTP_Interpret.ind0, False), (??.TPTP_Interpret.ind1, False)})}
% 137.75/136.84 bnd_system_indi_is_credit_admin: {(??.TPTP_Interpret.ind0,
% 137.75/136.84 {(??.TPTP_Interpret.ind0, True), (??.TPTP_Interpret.ind1, False)}),
% 137.75/136.84 (??.TPTP_Interpret.ind1,
% 137.75/136.84 {(??.TPTP_Interpret.ind0, False), (??.TPTP_Interpret.ind1, False)})}
% 137.75/136.84 bnd_system_indi_is_background_admin: {(??.TPTP_Interpret.ind0,
% 137.75/136.84 {(??.TPTP_Interpret.ind0, False), (??.TPTP_Interpret.ind1, True)}),
% 137.75/136.84 (??.TPTP_Interpret.ind1,
% 137.75/136.84 {(??.TPTP_Interpret.ind0, False), (??.TPTP_Interpret.ind1, False)})}
% 137.75/136.84 bnd_system_indi_is_hr_admin: {(??.TPTP_Interpret.ind0,
% 137.75/136.84 {(??.TPTP_Interpret.ind0, True), (??.TPTP_Interpret.ind1, False)}),
% 137.75/136.84 (??.TPTP_Interpret.ind1,
% 137.75/136.84 {(??.TPTP_Interpret.ind0, False), (??.TPTP_Interpret.ind1, False)})}
% 137.75/136.84 bnd_system_indi_is_level_admin: {(??.TPTP_Interpret.ind0,
% 137.75/136.84 {(??.TPTP_Interpret.ind0, False), (??.TPTP_Interpret.ind1, True)}),
% 137.75/136.84 (??.TPTP_Interpret.ind1,
% 137.75/136.84 {(??.TPTP_Interpret.ind0, False), (??.TPTP_Interpret.ind1, False)})}
% 137.75/136.84 bnd_usa: ??.TPTP_Interpret.ind0
% 137.75/136.84 bnd_polygraph_admin: ??.TPTP_Interpret.ind0
% 137.75/136.84 bnd_polygraph_admin_indi_has_polygraph: {(??.TPTP_Interpret.ind0,
% 137.75/136.84 {(??.TPTP_Interpret.ind0, False), (??.TPTP_Interpret.ind1, True)}),
% 137.75/136.84 (??.TPTP_Interpret.ind1,
% 137.75/136.84 {(??.TPTP_Interpret.ind0, True), (??.TPTP_Interpret.ind1, True)})}
% 137.75/136.84 bnd_credit_admin: ??.TPTP_Interpret.ind0
% 137.75/136.84 bnd_credit_admin_indi_has_credit: {(??.TPTP_Interpret.ind0,
% 137.75/136.84 {(??.TPTP_Interpret.ind0, False), (??.TPTP_Interpret.ind1, True)}),
% 137.75/136.84 (??.TPTP_Interpret.ind1,
% 137.75/136.84 {(??.TPTP_Interpret.ind0, True), (??.TPTP_Interpret.ind1, True)})}
% 137.75/136.84 bnd_background_admin: ??.TPTP_Interpret.ind1
% 137.75/136.84 bnd_background_admin_indi_has_background: {(??.TPTP_Interpret.ind0,
% 137.75/136.84 {(??.TPTP_Interpret.ind0,
% 137.75/136.84 {(??.TPTP_Interpret.ind0, False), (??.TPTP_Interpret.ind1, False)}),
% 137.75/136.84 (??.TPTP_Interpret.ind1,
% 137.75/136.84 {(??.TPTP_Interpret.ind0, False), (??.TPTP_Interpret.ind1, False)})}),
% 137.75/136.84 (??.TPTP_Interpret.ind1,
% 137.75/136.84 {(??.TPTP_Interpret.ind0,
% 137.75/136.84 {(??.TPTP_Interpret.ind0, False), (??.TPTP_Interpret.ind1, False)}),
% 137.75/136.84 (??.TPTP_Interpret.ind1,
% 137.75/136.84 {(??.TPTP_Interpret.ind0, False), (??.TPTP_Interpret.ind1, True)})})}
% 137.75/136.84 bnd_hr_admin: ??.TPTP_Interpret.ind0
% 137.75/136.84 bnd_hr_admin_indi_has_employment: {(??.TPTP_Interpret.ind0,
% 137.75/136.84 {(??.TPTP_Interpret.ind0, False), (??.TPTP_Interpret.ind1, True)}),
% 137.75/136.84 (??.TPTP_Interpret.ind1,
% 137.75/136.84 {(??.TPTP_Interpret.ind0, True), (??.TPTP_Interpret.ind1, True)})}
% 137.75/136.84 bnd_secret: ??.TPTP_Interpret.ind1
% 137.75/136.84 bnd_system_indi_needs_level: {(??.TPTP_Interpret.ind0,
% 137.75/136.84 {(??.TPTP_Interpret.ind0,
% 137.75/136.84 {(??.TPTP_Interpret.ind0, False), (??.TPTP_Interpret.ind1, False)}),
% 137.75/136.84 (??.TPTP_Interpret.ind1,
% 137.75/136.84 {(??.TPTP_Interpret.ind0, False), (??.TPTP_Interpret.ind1, True)})}),
% 137.75/136.84 (??.TPTP_Interpret.ind1,
% 137.75/136.84 {(??.TPTP_Interpret.ind0,
% 137.75/136.84 {(??.TPTP_Interpret.ind0, False), (??.TPTP_Interpret.ind1, False)}),
% 137.75/136.84 (??.TPTP_Interpret.ind1,
% 137.75/136.84 {(??.TPTP_Interpret.ind0, False), (??.TPTP_Interpret.ind1, False)})})}
% 137.75/136.84 bnd_topsecret: ??.TPTP_Interpret.ind1
% 137.75/136.84 bnd_level_admin: ??.TPTP_Interpret.ind1
% 137.75/136.84 bnd_level_admin_indi_has_level: {(??.TPTP_Interpret.ind0,
% 137.75/136.84 {(??.TPTP_Interpret.ind0,
% 137.75/136.84 {(??.TPTP_Interpret.ind0, False), (??.TPTP_Interpret.ind1, False)}),
% 137.75/136.84 (??.TPTP_Interpret.ind1,
% 137.75/136.84 {(??.TPTP_Interpret.ind0, False), (??.TPTP_Interpret.ind1, False)})}),
% 137.75/136.84 (??.TPTP_Interpret.ind1,
% 137.75/136.84 {(??.TPTP_Interpret.ind0,
% 137.75/136.84 {(??.TPTP_Interpret.ind0, False), (??.TPTP_Interpret.ind1, False)}),
% 137.75/136.84 (??.TPTP_Interpret.ind1,
% 137.75/136.84 {(??.TPTP_Interpret.ind0, False), (??.TPTP_Interpret.ind1, True)})})}
% 137.75/136.84 bnd_system_indi_needs_compartment: {(??.TPTP_Interpret.ind0,
% 137.75/136.84 {(??.TPTP_Interpret.ind0,
% 137.75/136.84 {(??.TPTP_Interpret.ind0, False), (??.TPTP_Interpret.ind1, False)}),
% 137.75/136.84 (??.TPTP_Interpret.ind1,
% 137.75/136.84 {(??.TPTP_Interpret.ind0, True), (??.TPTP_Interpret.ind1, False)})}),
% 137.75/136.84 (??.TPTP_Interpret.ind1,
% 137.75/136.84 {(??.TPTP_Interpret.ind0,
% 137.75/136.84 {(??.TPTP_Interpret.ind0, False), (??.TPTP_Interpret.ind1, False)}),
% 137.75/136.84 (??.TPTP_Interpret.ind1,
% 137.75/136.84 {(??.TPTP_Interpret.ind0, False), (??.TPTP_Interpret.ind1, False)})})}
% 137.75/136.84 bnd_compartmentb: ??.TPTP_Interpret.ind0
% 137.75/136.84 bnd_sso_compartmentb: ??.TPTP_Interpret.ind1
% 137.75/136.84 bnd_compartmenta: ??.TPTP_Interpret.ind0
% 137.75/136.84 bnd_sso_compartmenta: ??.TPTP_Interpret.ind1
% 137.75/136.84 bnd_sso_indi_has_compartment: {(??.TPTP_Interpret.ind0,
% 137.75/136.84 {(??.TPTP_Interpret.ind0,
% 137.75/136.84 {(??.TPTP_Interpret.ind0, True), (??.TPTP_Interpret.ind1, True)}),
% 137.75/136.84 (??.TPTP_Interpret.ind1,
% 137.75/136.84 {(??.TPTP_Interpret.ind0, True), (??.TPTP_Interpret.ind1, True)})}),
% 137.75/136.84 (??.TPTP_Interpret.ind1,
% 137.75/136.84 {(??.TPTP_Interpret.ind0,
% 137.75/136.84 {(??.TPTP_Interpret.ind0, True), (??.TPTP_Interpret.ind1, True)}),
% 137.75/136.84 (??.TPTP_Interpret.ind1,
% 137.75/136.84 {(??.TPTP_Interpret.ind0, True), (??.TPTP_Interpret.ind1, True)})})}
% 137.75/136.84 bnd_secretfile: ??.TPTP_Interpret.ind0
% 137.75/136.84 bnd_alice: ??.TPTP_Interpret.ind1
% 137.75/136.84 bnd_india: ??.TPTP_Interpret.ind1
% 137.75/136.84 bnd_system_indi_has_citizenship: {(??.TPTP_Interpret.ind0,
% 137.75/136.84 {(??.TPTP_Interpret.ind0,
% 137.75/136.84 {(??.TPTP_Interpret.ind0, False), (??.TPTP_Interpret.ind1, True)}),
% 137.75/136.84 (??.TPTP_Interpret.ind1,
% 137.75/136.84 {(??.TPTP_Interpret.ind0, True), (??.TPTP_Interpret.ind1, True)})}),
% 137.75/136.84 (??.TPTP_Interpret.ind1,
% 137.75/136.84 {(??.TPTP_Interpret.ind0,
% 137.75/136.84 {(??.TPTP_Interpret.ind0, True), (??.TPTP_Interpret.ind1, True)}),
% 137.75/136.84 (??.TPTP_Interpret.ind1,
% 137.75/136.84 {(??.TPTP_Interpret.ind0, True), (??.TPTP_Interpret.ind1, True)})})}
% 137.75/136.84 bnd_not_secretfile: ??.TPTP_Interpret.ind1
% 137.75/136.84 bnd_babu: ??.TPTP_Interpret.ind0
% 137.75/136.84 bnd_owner_not_secretfile: ??.TPTP_Interpret.ind1
% 137.75/136.84 bnd_owner_indi_has_need_to_know: {(??.TPTP_Interpret.ind0,
% 137.75/136.84 {(??.TPTP_Interpret.ind0,
% 137.75/136.84 {(??.TPTP_Interpret.ind0, True), (??.TPTP_Interpret.ind1, True)}),
% 137.75/136.84 (??.TPTP_Interpret.ind1,
% 137.75/136.84 {(??.TPTP_Interpret.ind0, True), (??.TPTP_Interpret.ind1, True)})}),
% 137.75/136.84 (??.TPTP_Interpret.ind1,
% 137.75/136.84 {(??.TPTP_Interpret.ind0,
% 137.75/136.84 {(??.TPTP_Interpret.ind0, True), (??.TPTP_Interpret.ind1, True)}),
% 137.75/136.84 (??.TPTP_Interpret.ind1,
% 137.75/136.84 {(??.TPTP_Interpret.ind0, True), (??.TPTP_Interpret.ind1, False)})})}
% 137.75/136.84 bnd_owner_secretfile: ??.TPTP_Interpret.ind0
% 137.75/136.84 bnd_ci: ??.TPTP_Interpret.ind1
% 137.75/136.84 bnd_system: ??.TPTP_Interpret.ind0
% 137.75/136.84 bnd_system_indi_is_counterintelligence: {(??.TPTP_Interpret.ind0,
% 137.75/136.84 {(??.TPTP_Interpret.ind0,
% 137.75/136.84 {(??.TPTP_Interpret.ind0, False), (??.TPTP_Interpret.ind1, False)}),
% 137.75/136.84 (??.TPTP_Interpret.ind1,
% 137.75/136.84 {(??.TPTP_Interpret.ind0, True), (??.TPTP_Interpret.ind1, False)})}),
% 137.75/136.84 (??.TPTP_Interpret.ind1,
% 137.75/136.84 {(??.TPTP_Interpret.ind0,
% 137.75/136.84 {(??.TPTP_Interpret.ind0, False), (??.TPTP_Interpret.ind1, False)}),
% 137.75/136.84 (??.TPTP_Interpret.ind1,
% 137.75/136.84 {(??.TPTP_Interpret.ind0, False), (??.TPTP_Interpret.ind1, False)})})}
% 137.75/136.84
% 137.75/136.84 % SZS status CounterSatisfiable
%------------------------------------------------------------------------------