%------------------------------------------------------------------------------
% File : FMB4J---0.1
% Problem : SWV440+1 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_fmb4j /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% Computer : n011.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Fri Sep 25 03:15:20 PM UTC 2026
% Result : CounterSatisfiable 2.41s 1.24s
% Output : FiniteModel 2.86s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
fof(domain,interpretation-domains,
! [X] :
( X = "d1"
| X = "d0" ) ).
fof(mappings,interpretation-mappings,
( confidential = "d0"
& nil = "d1"
& polygraph_admin = "d0"
& sso_compartmentb = "d0"
& hr_admin = "d1"
& sso_compartmenta = "d0"
& admin = "d1"
& yes = "d1"
& alice = "d1"
& cons("d1","d1") = "d0"
& cons("d0","d0") = "d0"
& cons("d0","d1") = "d0"
& cons("d1","d0") = "d0"
& secret = "d0"
& level_admin = "d0"
& compartmenta = "d1"
& compartmentb = "d1"
& anycountry = "d0"
& not_secretfile = "d1"
& sbu = "d1"
& credit_admin = "d0"
& topsecret = "d1"
& ci = "d0"
& owner_secretfile = "d0"
& india = "d0"
& unclassified = "d1"
& babu = "d0"
& oca = "d0"
& scg_compartmenta = "d1"
& system = "d0"
& scg_compartmentb = "d1"
& owner_not_secretfile = "d1"
& usa = "d0"
& secretfile = "d0"
& read = "d0"
& background_admin = "d0"
& no = "d0" ) ).
fof(predicate_mappings,interpretation-mappings,
( admin_indi_has_compartments_for_file("d1","d1","d1")
& admin_indi_has_compartments_for_file("d0","d0","d1")
& admin_indi_has_compartments_for_file("d1","d0","d0")
& admin_indi_has_compartments_for_file("d0","d1","d0")
& admin_indi_has_compartments_for_file("d1","d0","d1")
& admin_indi_has_compartments_for_file("d0","d1","d1")
& admin_indi_has_compartments_for_file("d1","d1","d0")
& ~ admin_indi_has_compartments_for_file("d0","d0","d0")
& system_file_needs_compartments("d1","d1","d1")
& system_file_needs_compartments("d1","d0","d0")
& system_file_needs_compartments("d0","d0","d1")
& system_file_needs_compartments("d0","d1","d0")
& system_file_needs_compartments("d1","d0","d1")
& system_file_needs_compartments("d1","d1","d0")
& system_file_needs_compartments("d0","d1","d1")
& system_file_needs_compartments("d0","d0","d0")
& ~ system_indi_is_level_admin("d0","d1")
& system_indi_is_level_admin("d1","d0")
& ~ system_indi_is_level_admin("d1","d1")
& system_indi_is_level_admin("d0","d0")
& ~ system_indi_is_polygraph_admin("d1","d1")
& system_indi_is_polygraph_admin("d0","d0")
& ~ system_indi_is_polygraph_admin("d0","d1")
& system_indi_is_polygraph_admin("d1","d0")
& ~ credit_admin_indi_has_credit("d1","d1")
& credit_admin_indi_has_credit("d0","d0")
& ~ credit_admin_indi_has_credit("d1","d0")
& credit_admin_indi_has_credit("d0","d1")
& admin_indi_has_background_for_compartment("d1","d1","d1")
& ~ admin_indi_has_background_for_compartment("d0","d0","d1")
& admin_indi_has_background_for_compartment("d1","d0","d0")
& ~ admin_indi_has_background_for_compartment("d0","d1","d0")
& admin_indi_has_background_for_compartment("d1","d0","d1")
& ~ admin_indi_has_background_for_compartment("d0","d1","d1")
& admin_indi_has_background_for_compartment("d1","d1","d0")
& ~ admin_indi_has_background_for_compartment("d0","d0","d0")
& state_file_has_owner("d1","d1")
& state_file_has_owner("d0","d0")
& state_file_has_owner("d0","d1")
& ~ state_file_has_owner("d1","d0")
& system_indi_has_citizenship("d1","d0","d1")
& ~ system_indi_has_citizenship("d0","d1","d1")
& ~ system_indi_has_citizenship("d1","d1","d0")
& system_indi_has_citizenship("d0","d0","d0")
& ~ system_indi_has_citizenship("d1","d1","d1")
& system_indi_has_citizenship("d0","d0","d1")
& system_indi_has_citizenship("d1","d0","d0")
& system_indi_has_citizenship("d0","d1","d0")
& ~ admin_file_has_level("d1","d0","d1")
& ~ admin_file_has_level("d0","d1","d1")
& admin_file_has_level("d1","d1","d0")
& ~ admin_file_has_level("d0","d0","d0")
& admin_file_has_level("d1","d1","d1")
& admin_file_has_level("d0","d0","d1")
& admin_file_has_level("d1","d0","d0")
& ~ admin_file_has_level("d0","d1","d0")
& ~ background_admin_indi_has_background("d1","d0","d1")
& background_admin_indi_has_background("d0","d1","d1")
& ~ background_admin_indi_has_background("d1","d1","d0")
& ~ background_admin_indi_has_background("d0","d0","d0")
& admin_indi_has_citizenship("d1","d1","d0")
& admin_indi_has_citizenship("d1","d0","d1")
& ~ admin_indi_has_citizenship("d0","d1","d1")
& admin_indi_has_citizenship("d0","d0","d0")
& ~ background_admin_indi_has_background("d1","d1","d1")
& ~ background_admin_indi_has_background("d0","d0","d1")
& ~ background_admin_indi_has_background("d1","d0","d0")
& ~ background_admin_indi_has_background("d0","d1","d0")
& ~ admin_indi_has_citizenship("d1","d1","d1")
& admin_indi_has_citizenship("d1","d0","d0")
& admin_indi_has_citizenship("d0","d1","d0")
& admin_indi_has_citizenship("d0","d0","d1")
& ~ polygraph_admin_indi_has_polygraph("d1","d1")
& polygraph_admin_indi_has_polygraph("d0","d0")
& ~ polygraph_admin_indi_has_polygraph("d1","d0")
& polygraph_admin_indi_has_polygraph("d0","d1")
& admin_indi_has_polygraph_for_compartment("d1","d0","d1")
& ~ admin_indi_has_polygraph_for_compartment("d0","d1","d1")
& admin_indi_has_polygraph_for_compartment("d1","d1","d0")
& ~ admin_indi_has_polygraph_for_compartment("d0","d0","d0")
& admin_indi_has_polygraph_for_compartment("d1","d1","d1")
& ~ admin_indi_has_polygraph_for_compartment("d0","d0","d1")
& admin_indi_has_polygraph_for_compartment("d1","d0","d0")
& ~ admin_indi_has_polygraph_for_compartment("d0","d1","d0")
& system_indi_is_hr_admin("d0","d1")
& system_indi_is_hr_admin("d1","d0")
& ~ system_indi_is_hr_admin("d1","d1")
& system_indi_is_hr_admin("d0","d0")
& admin_indi_has_citizenship_for_file("d1","d0","d1")
& ~ admin_indi_has_citizenship_for_file("d0","d1","d1")
& admin_indi_has_citizenship_for_file("d1","d1","d0")
& admin_indi_has_citizenship_for_file("d0","d0","d0")
& admin_indi_has_citizenship_for_file("d1","d1","d1")
& admin_indi_has_citizenship_for_file("d0","d0","d1")
& admin_indi_has_citizenship_for_file("d1","d0","d0")
& ~ admin_indi_has_citizenship_for_file("d0","d1","d0")
& ~ admin_indi_has_employment("d0","d1")
& admin_indi_has_employment("d1","d0")
& admin_indi_has_employment("d1","d1")
& admin_indi_has_employment("d0","d0")
& admin_indi_has_level_for_file("d1","d1","d0")
& admin_indi_has_level_for_file("d0","d1","d1")
& admin_indi_has_level_for_file("d0","d0","d0")
& loca_level_direct_below("d1","d1","d1")
& loca_level_direct_below("d0","d1","d0")
& admin_indi_has_level_for_file("d1","d0","d1")
& loca_level_direct_below("d0","d0","d1")
& loca_level_direct_below("d1","d0","d0")
& ~ system_indi_needs_level("d0","d0","d1")
& system_indi_needs_level("d0","d1","d0")
& system_indi_needs_level("d1","d0","d0")
& ~ system_indi_needs_level("d1","d1","d1")
& ~ admin_indi_has_level_for_file("d1","d0","d0")
& admin_indi_has_level_for_file("d1","d1","d1")
& ~ admin_indi_has_level_for_file("d0","d0","d1")
& admin_indi_has_level_for_file("d0","d1","d0")
& loca_level_direct_below("d0","d1","d1")
& loca_level_direct_below("d1","d1","d0")
& loca_level_direct_below("d1","d0","d1")
& loca_level_direct_below("d0","d0","d0")
& ~ system_indi_needs_level("d0","d1","d1")
& ~ system_indi_needs_level("d1","d1","d0")
& ~ system_indi_needs_level("d0","d0","d0")
& ~ system_indi_needs_level("d1","d0","d1")
& ~ system_file_needs_citizenship("d1","d0","d1")
& ~ system_file_needs_citizenship("d1","d1","d0")
& ~ system_file_needs_citizenship("d0","d1","d1")
& system_file_needs_citizenship("d0","d0","d0")
& system_file_needs_citizenship("d1","d1","d1")
& ~ system_file_needs_citizenship("d1","d0","d0")
& ~ system_file_needs_citizenship("d0","d0","d1")
& system_file_needs_citizenship("d0","d1","d0")
& ~ system_indi_is_oca("d0","d1")
& system_indi_is_oca("d1","d0")
& ~ system_indi_is_oca("d1","d1")
& system_indi_is_oca("d0","d0")
& admin_indi_has_compartments("d1","d0","d1")
& admin_indi_has_compartments("d1","d1","d0")
& admin_indi_has_compartments("d0","d1","d1")
& admin_indi_has_compartments("d0","d0","d0")
& admin_indi_has_compartments("d1","d1","d1")
& admin_indi_has_compartments("d1","d0","d0")
& admin_indi_has_compartments("d0","d0","d1")
& admin_indi_has_compartments("d0","d1","d0")
& ~ oca_compartment_is_compartment("d1","d0","d0","d0","d1","d1")
& ~ oca_compartment_is_compartment("d0","d0","d0","d0","d0","d1")
& ~ oca_compartment_is_compartment("d0","d0","d0","d1","d0","d0")
& ~ oca_compartment_is_compartment("d0","d1","d0","d0","d1","d1")
& ~ oca_compartment_is_compartment("d1","d1","d1","d1","d0","d1")
& ~ oca_compartment_is_compartment("d0","d1","d0","d1","d0","d1")
& ~ oca_compartment_is_compartment("d1","d0","d1","d0","d1","d0")
& ~ oca_compartment_is_compartment("d1","d1","d0","d1","d0","d0")
& oca_compartment_is_compartment("d0","d0","d0","d1","d1","d1")
& ~ oca_compartment_is_compartment("d1","d1","d1","d1","d1","d0")
& ~ oca_compartment_is_compartment("d1","d0","d0","d1","d0","d1")
& ~ oca_compartment_is_compartment("d1","d1","d1","d0","d0","d0")
& ~ oca_compartment_is_compartment("d1","d0","d1","d1","d1","d1")
& ~ oca_compartment_is_compartment("d0","d0","d1","d1","d1","d0")
& ~ oca_compartment_is_compartment("d1","d0","d1","d1","d0","d0")
& ~ oca_compartment_is_compartment("d0","d1","d1","d0","d1","d0")
& ~ oca_compartment_is_compartment("d0","d0","d1","d0","d0","d0")
& ~ oca_compartment_is_compartment("d1","d1","d0","d0","d1","d0")
& ~ oca_compartment_is_compartment("d0","d0","d1","d0","d1","d1")
& ~ oca_compartment_is_compartment("d1","d1","d0","d0","d0","d1")
& ~ oca_compartment_is_compartment("d1","d1","d1","d0","d1","d1")
& ~ oca_compartment_is_compartment("d0","d1","d1","d0","d0","d1")
& ~ oca_compartment_is_compartment("d1","d0","d0","d1","d1","d0")
& ~ oca_compartment_is_compartment("d0","d1","d0","d1","d1","d0")
& ~ oca_compartment_is_compartment("d1","d1","d0","d1","d1","d1")
& oca_compartment_is_compartment("d0","d1","d1","d1","d0","d0")
& ~ oca_compartment_is_compartment("d0","d1","d1","d1","d1","d1")
& ~ oca_compartment_is_compartment("d0","d0","d1","d1","d0","d1")
& ~ oca_compartment_is_compartment("d1","d0","d1","d0","d0","d1")
& ~ oca_compartment_is_compartment("d0","d0","d0","d0","d1","d0")
& ~ oca_compartment_is_compartment("d0","d1","d0","d0","d0","d0")
& ~ oca_compartment_is_compartment("d1","d0","d0","d0","d0","d0")
& ~ oca_compartment_is_compartment("d1","d1","d0","d1","d0","d1")
& ~ oca_compartment_is_compartment("d0","d1","d0","d1","d0","d0")
& ~ oca_compartment_is_compartment("d1","d1","d1","d0","d0","d1")
& ~ oca_compartment_is_compartment("d1","d1","d1","d0","d1","d0")
& ~ oca_compartment_is_compartment("d1","d0","d1","d0","d0","d0")
& ~ oca_compartment_is_compartment("d0","d1","d1","d1","d0","d1")
& ~ oca_compartment_is_compartment("d1","d1","d0","d1","d1","d0")
& ~ oca_compartment_is_compartment("d0","d0","d0","d1","d0","d1")
& ~ oca_compartment_is_compartment("d0","d0","d1","d0","d1","d0")
& oca_compartment_is_compartment("d0","d1","d0","d1","d1","d1")
& ~ oca_compartment_is_compartment("d0","d0","d1","d1","d0","d0")
& ~ oca_compartment_is_compartment("d1","d0","d0","d0","d1","d0")
& ~ oca_compartment_is_compartment("d1","d0","d0","d0","d0","d1")
& ~ oca_compartment_is_compartment("d1","d1","d0","d0","d1","d1")
& ~ oca_compartment_is_compartment("d1","d0","d0","d1","d0","d0")
& ~ oca_compartment_is_compartment("d0","d0","d0","d1","d1","d0")
& ~ oca_compartment_is_compartment("d1","d1","d0","d0","d0","d0")
& ~ oca_compartment_is_compartment("d0","d1","d0","d0","d0","d1")
& ~ oca_compartment_is_compartment("d0","d0","d1","d0","d0","d1")
& ~ oca_compartment_is_compartment("d1","d0","d1","d1","d1","d0")
& ~ oca_compartment_is_compartment("d1","d0","d1","d1","d0","d1")
& ~ oca_compartment_is_compartment("d1","d0","d0","d1","d1","d1")
& ~ oca_compartment_is_compartment("d0","d1","d1","d1","d1","d0")
& ~ oca_compartment_is_compartment("d0","d0","d0","d0","d1","d1")
& ~ oca_compartment_is_compartment("d0","d0","d1","d1","d1","d1")
& ~ oca_compartment_is_compartment("d1","d0","d1","d0","d1","d1")
& ~ oca_compartment_is_compartment("d1","d1","d1","d1","d1","d1")
& ~ oca_compartment_is_compartment("d0","d1","d1","d0","d1","d1")
& ~ oca_compartment_is_compartment("d1","d1","d1","d1","d0","d0")
& ~ oca_compartment_is_compartment("d0","d1","d0","d0","d1","d0")
& ~ oca_compartment_is_compartment("d0","d1","d1","d0","d0","d0")
& ~ oca_compartment_is_compartment("d0","d0","d0","d0","d0","d0")
& admin_compartment_has_scg("d1","d1","d1")
& ~ admin_compartment_has_scg("d0","d0","d1")
& ~ admin_compartment_has_scg("d0","d1","d0")
& admin_compartment_has_scg("d1","d0","d0")
& ~ admin_compartment_has_scg("d0","d1","d1")
& ~ admin_compartment_has_scg("d1","d0","d1")
& ~ admin_compartment_has_scg("d1","d1","d0")
& ~ admin_compartment_has_scg("d0","d0","d0")
& ~ owner_indi_has_need_to_know("d1","d1","d1")
& owner_indi_has_need_to_know("d1","d0","d0")
& owner_indi_has_need_to_know("d0","d0","d1")
& owner_indi_has_need_to_know("d0","d1","d0")
& owner_indi_has_need_to_know("d1","d0","d1")
& ~ owner_indi_has_need_to_know("d1","d1","d0")
& owner_indi_has_need_to_know("d0","d1","d1")
& owner_indi_has_need_to_know("d0","d0","d0")
& ~ sso_file_has_citizenship("d1","d0","d1","d1")
& ~ sso_file_has_citizenship("d1","d1","d0","d1")
& ~ sso_file_has_citizenship("d0","d1","d1","d1")
& sso_file_has_citizenship("d0","d0","d0","d1")
& ~ sso_file_has_citizenship("d1","d1","d1","d0")
& ~ sso_file_has_citizenship("d1","d0","d0","d0")
& ~ sso_file_has_citizenship("d0","d0","d1","d0")
& ~ sso_file_has_citizenship("d0","d1","d0","d0")
& ~ sso_file_has_citizenship("d1","d1","d1","d1")
& ~ sso_file_has_citizenship("d1","d0","d0","d1")
& ~ sso_file_has_citizenship("d0","d0","d1","d1")
& ~ sso_file_has_citizenship("d0","d1","d0","d1")
& ~ sso_file_has_citizenship("d1","d0","d1","d0")
& ~ sso_file_has_citizenship("d1","d1","d0","d0")
& ~ sso_file_has_citizenship("d0","d1","d1","d0")
& ~ sso_file_has_citizenship("d0","d0","d0","d0")
& ~ system_indi_is_background_admin("d0","d1")
& system_indi_is_background_admin("d1","d0")
& ~ system_indi_is_background_admin("d1","d1")
& system_indi_is_background_admin("d0","d0")
& ~ system_indi_needs_compartment("d1","d1","d1")
& ~ system_indi_needs_compartment("d0","d0","d1")
& system_indi_needs_compartment("d0","d1","d0")
& system_indi_needs_compartment("d1","d0","d0")
& system_indi_needs_compartment("d0","d1","d1")
& ~ system_indi_needs_compartment("d1","d0","d1")
& ~ system_indi_needs_compartment("d1","d1","d0")
& system_indi_needs_compartment("d0","d0","d0")
& state_file_is_not_working_paper("d0")
& state_file_is_not_working_paper("d1")
& system_file_needs_level("d1","d1","d1")
& system_file_needs_level("d1","d0","d0")
& ~ system_file_needs_level("d0","d0","d1")
& system_file_needs_level("d0","d1","d0")
& system_file_needs_level("d1","d0","d1")
& system_file_needs_level("d1","d1","d0")
& system_file_needs_level("d0","d1","d1")
& system_file_needs_level("d0","d0","d0")
& loca_level_below("d1","d0","d1")
& loca_level_below("d1","d1","d0")
& loca_level_below("d0","d1","d1")
& loca_level_below("d0","d0","d0")
& loca_level_below("d1","d1","d1")
& loca_level_below("d1","d0","d0")
& loca_level_below("d0","d0","d1")
& loca_level_below("d0","d1","d0")
& admin_file_has_citizenship_h("d1","d0","d1","d1")
& admin_file_has_citizenship_h("d1","d1","d1","d0")
& admin_file_has_citizenship_h("d0","d1","d1","d1")
& admin_file_has_citizenship_h("d0","d0","d1","d0")
& admin_file_has_citizenship_h("d1","d1","d0","d1")
& admin_file_has_citizenship_h("d1","d0","d0","d0")
& admin_file_has_citizenship_h("d0","d0","d0","d1")
& admin_file_has_citizenship_h("d0","d1","d0","d0")
& admin_file_has_citizenship_h("d1","d1","d1","d1")
& admin_file_has_citizenship_h("d1","d0","d1","d0")
& admin_file_has_citizenship_h("d0","d0","d1","d1")
& admin_file_has_citizenship_h("d0","d1","d1","d0")
& admin_file_has_citizenship_h("d1","d0","d0","d1")
& admin_file_has_citizenship_h("d1","d1","d0","d0")
& admin_file_has_citizenship_h("d0","d1","d0","d1")
& admin_file_has_citizenship_h("d0","d0","d0","d0")
& ~ admin_indi_may_file("d1","d1","d1","d1")
& admin_indi_may_file("d1","d0","d1","d0")
& admin_indi_may_file("d0","d0","d1","d1")
& ~ admin_indi_may_file("d0","d1","d1","d0")
& admin_indi_may_file("d1","d0","d0","d1")
& admin_indi_may_file("d1","d1","d0","d0")
& ~ admin_indi_may_file("d0","d1","d0","d1")
& ~ admin_indi_may_file("d0","d0","d0","d0")
& ~ admin_indi_may_file("d1","d0","d1","d1")
& ~ admin_indi_may_file("d1","d1","d1","d0")
& ~ admin_indi_may_file("d0","d1","d1","d1")
& admin_indi_may_file("d0","d0","d1","d0")
& ~ admin_indi_may_file("d1","d1","d0","d1")
& admin_indi_may_file("d1","d0","d0","d0")
& ~ admin_indi_may_file("d0","d0","d0","d1")
& ~ admin_indi_may_file("d0","d1","d0","d0")
& admin_indi_has_credit_for_compartment("d1","d1","d1")
& ~ admin_indi_has_credit_for_compartment("d0","d0","d1")
& admin_indi_has_credit_for_compartment("d1","d0","d0")
& ~ admin_indi_has_credit_for_compartment("d0","d1","d0")
& admin_indi_has_credit_for_compartment("d1","d0","d1")
& ~ admin_indi_has_credit_for_compartment("d0","d1","d1")
& admin_indi_has_credit_for_compartment("d1","d1","d0")
& ~ admin_indi_has_credit_for_compartment("d0","d0","d0")
& ~ system_indi_is_counterintelligence("d1","d1","d1")
& system_indi_is_counterintelligence("d1","d0","d0")
& ~ system_indi_is_counterintelligence("d0","d0","d1")
& ~ system_indi_is_counterintelligence("d0","d1","d0")
& ~ system_indi_is_counterintelligence("d1","d0","d1")
& ~ system_indi_is_counterintelligence("d1","d1","d0")
& ~ system_indi_is_counterintelligence("d0","d1","d1")
& system_indi_is_counterintelligence("d0","d0","d0")
& ~ hr_admin_indi_has_employment("d1","d0")
& ~ hr_admin_indi_has_employment("d0","d1")
& hr_admin_indi_has_employment("d1","d1")
& hr_admin_indi_has_employment("d0","d0")
& admin_indi_has_credit("d1","d0")
& ~ admin_indi_has_credit("d0","d1")
& admin_indi_has_credit("d1","d1")
& admin_indi_has_credit("d0","d0")
& admin_indi_has_background("d1","d0","d1")
& admin_indi_has_background("d0","d1","d1")
& admin_indi_has_background("d1","d1","d0")
& admin_indi_has_background("d0","d0","d0")
& admin_indi_has_background("d1","d1","d1")
& admin_indi_has_background("d0","d0","d1")
& admin_indi_has_background("d1","d0","d0")
& admin_indi_has_background("d0","d1","d0")
& admin_indi_has_need_to_know_for_file("d1","d1","d0")
& ~ admin_indi_has_need_to_know_for_file("d0","d1","d1")
& admin_indi_has_need_to_know_for_file("d1","d0","d1")
& admin_indi_has_need_to_know_for_file("d0","d0","d0")
& admin_indi_has_need_to_know_for_file("d0","d0","d1")
& ~ admin_indi_has_need_to_know_for_file("d1","d1","d1")
& admin_indi_has_need_to_know_for_file("d1","d0","d0")
& ~ admin_indi_has_need_to_know_for_file("d0","d1","d0")
& oca_compartment_has_scg("d0","d1","d1")
& ~ oca_compartment_has_scg("d1","d0","d1")
& ~ oca_compartment_has_scg("d1","d1","d0")
& oca_compartment_has_scg("d0","d0","d0")
& ~ oca_compartment_has_scg("d1","d1","d1")
& ~ oca_compartment_has_scg("d0","d0","d1")
& ~ oca_compartment_has_scg("d0","d1","d0")
& ~ oca_compartment_has_scg("d1","d0","d0")
& admin_indi_has_level_for_compartment("d1","d0","d1")
& ~ admin_indi_has_level_for_compartment("d0","d1","d1")
& admin_indi_has_level_for_compartment("d1","d1","d0")
& ~ admin_indi_has_level_for_compartment("d0","d0","d0")
& admin_indi_has_level_for_compartment("d1","d1","d1")
& ~ admin_indi_has_level_for_compartment("d0","d0","d1")
& admin_indi_has_level_for_compartment("d1","d0","d0")
& ~ admin_indi_has_level_for_compartment("d0","d1","d0")
& admin_file_has_compartments("d1","d1","d1")
& admin_file_has_compartments("d0","d0","d1")
& admin_file_has_compartments("d1","d0","d0")
& admin_file_has_compartments("d0","d1","d0")
& admin_file_has_compartments("d1","d0","d1")
& admin_file_has_compartments("d0","d1","d1")
& admin_file_has_compartments("d1","d1","d0")
& admin_file_has_compartments("d0","d0","d0")
& ~ system_compartment_has_sso("d1","d1","d1")
& ~ system_compartment_has_sso("d0","d0","d1")
& ~ system_compartment_has_sso("d1","d0","d0")
& system_compartment_has_sso("d0","d1","d0")
& ~ system_compartment_has_sso("d1","d0","d1")
& ~ system_compartment_has_sso("d0","d1","d1")
& ~ system_compartment_has_sso("d1","d1","d0")
& system_compartment_has_sso("d0","d0","d0")
& admin_file_has_level_h("d1","d1","d0","d0")
& admin_file_has_level_h("d1","d0","d0","d1")
& admin_file_has_level_h("d0","d1","d1","d0")
& admin_file_has_level_h("d0","d1","d0","d1")
& admin_file_has_level_h("d1","d1","d1","d1")
& admin_file_has_level_h("d0","d0","d1","d1")
& admin_file_has_level_h("d1","d0","d1","d0")
& admin_file_has_level_h("d0","d0","d0","d0")
& ~ sso_file_has_level("d1","d0","d1","d1")
& ~ sso_file_has_level("d1","d1","d0","d1")
& sso_file_has_level("d0","d0","d0","d1")
& ~ sso_file_has_level("d1","d1","d1","d0")
& ~ sso_file_has_level("d0","d0","d1","d0")
& ~ sso_file_has_level("d0","d1","d0","d0")
& ~ sso_file_has_level("d1","d0","d0","d0")
& ~ sso_file_has_level("d0","d1","d1","d1")
& admin_file_has_level_h("d0","d0","d0","d1")
& admin_file_has_level_h("d1","d1","d0","d1")
& admin_file_has_level_h("d1","d0","d1","d1")
& admin_file_has_level_h("d1","d0","d0","d0")
& admin_file_has_level_h("d1","d1","d1","d0")
& admin_file_has_level_h("d0","d0","d1","d0")
& admin_file_has_level_h("d0","d1","d1","d1")
& admin_file_has_level_h("d0","d1","d0","d0")
& ~ sso_file_has_level("d1","d1","d1","d1")
& ~ sso_file_has_level("d1","d0","d0","d1")
& ~ sso_file_has_level("d0","d0","d1","d1")
& ~ sso_file_has_level("d0","d1","d0","d1")
& ~ sso_file_has_level("d1","d0","d1","d0")
& ~ sso_file_has_level("d1","d1","d0","d0")
& ~ sso_file_has_level("d0","d1","d1","d0")
& ~ sso_file_has_level("d0","d0","d0","d0")
& admin_indi_has_polygraph("d1","d0")
& ~ admin_indi_has_polygraph("d0","d1")
& admin_indi_has_polygraph("d1","d1")
& admin_indi_has_polygraph("d0","d0")
& ~ sso_file_has_compartments("d1","d0","d1")
& ~ sso_file_has_compartments("d1","d1","d0")
& ~ sso_file_has_compartments("d0","d1","d1")
& sso_file_has_compartments("d0","d0","d0")
& ~ sso_file_has_compartments("d1","d1","d1")
& ~ sso_file_has_compartments("d1","d0","d0")
& ~ sso_file_has_compartments("d0","d0","d1")
& ~ sso_file_has_compartments("d0","d1","d0")
& ~ admin_file_has_citizenship("d1","d1","d1")
& ~ admin_file_has_citizenship("d0","d0","d1")
& admin_file_has_citizenship("d1","d0","d0")
& ~ admin_file_has_citizenship("d0","d1","d0")
& ~ admin_file_has_citizenship("d1","d0","d1")
& ~ admin_file_has_citizenship("d0","d1","d1")
& admin_file_has_citizenship("d1","d1","d0")
& ~ admin_file_has_citizenship("d0","d0","d0")
& ~ sso_compartment_has_scg("d1","d0","d1")
& sso_compartment_has_scg("d0","d1","d1")
& ~ sso_compartment_has_scg("d1","d1","d0")
& sso_compartment_has_scg("d0","d0","d0")
& ~ sso_compartment_has_scg("d1","d1","d1")
& ~ sso_compartment_has_scg("d0","d0","d1")
& ~ sso_compartment_has_scg("d1","d0","d0")
& ~ sso_compartment_has_scg("d0","d1","d0")
& ~ system_indi_is_credit_admin("d1","d1")
& system_indi_is_credit_admin("d0","d0")
& ~ system_indi_is_credit_admin("d0","d1")
& system_indi_is_credit_admin("d1","d0")
& ~ sso_indi_has_compartment("d1","d0","d1")
& ~ sso_indi_has_compartment("d1","d1","d0")
& sso_indi_has_compartment("d0","d1","d1")
& sso_indi_has_compartment("d0","d0","d0")
& ~ sso_indi_has_compartment("d1","d1","d1")
& ~ sso_indi_has_compartment("d1","d0","d0")
& ~ sso_indi_has_compartment("d0","d0","d1")
& ~ sso_indi_has_compartment("d0","d1","d0")
& ~ admin_compartment_has_sso("d1","d1","d1")
& admin_compartment_has_sso("d1","d0","d0")
& ~ admin_compartment_has_sso("d0","d0","d1")
& ~ admin_compartment_has_sso("d0","d1","d0")
& ~ admin_compartment_has_sso("d1","d0","d1")
& admin_compartment_has_sso("d1","d1","d0")
& ~ admin_compartment_has_sso("d0","d1","d1")
& ~ admin_compartment_has_sso("d0","d0","d0")
& admin_indi_has_level("d1","d0","d1")
& admin_indi_has_level("d0","d1","d1")
& admin_indi_has_level("d1","d1","d0")
& admin_indi_has_level("d0","d0","d0")
& admin_indi_has_level("d1","d1","d1")
& admin_indi_has_level("d0","d0","d1")
& ~ admin_indi_has_level("d1","d0","d0")
& admin_indi_has_level("d0","d1","d0")
& admin_file_has_compartments_h("d1","d1","d1","d1")
& admin_file_has_compartments_h("d1","d0","d1","d0")
& admin_file_has_compartments_h("d0","d0","d1","d1")
& admin_file_has_compartments_h("d0","d1","d1","d0")
& admin_file_has_compartments_h("d1","d0","d0","d1")
& admin_file_has_compartments_h("d1","d1","d0","d0")
& admin_file_has_compartments_h("d0","d1","d0","d1")
& admin_file_has_compartments_h("d0","d0","d0","d0")
& admin_file_has_compartments_h("d1","d0","d1","d1")
& admin_file_has_compartments_h("d1","d1","d1","d0")
& admin_file_has_compartments_h("d0","d1","d1","d1")
& admin_file_has_compartments_h("d0","d0","d1","d0")
& admin_file_has_compartments_h("d1","d1","d0","d1")
& admin_file_has_compartments_h("d1","d0","d0","d0")
& admin_file_has_compartments_h("d0","d0","d0","d1")
& admin_file_has_compartments_h("d0","d1","d0","d0")
& ~ level_admin_indi_has_level("d1","d0","d1")
& level_admin_indi_has_level("d0","d1","d1")
& ~ level_admin_indi_has_level("d1","d1","d0")
& ~ level_admin_indi_has_level("d0","d0","d0")
& ~ level_admin_indi_has_level("d1","d1","d1")
& ~ level_admin_indi_has_level("d0","d0","d1")
& ~ level_admin_indi_has_level("d1","d0","d0")
& ~ level_admin_indi_has_level("d0","d1","d0") ) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SWV440+1 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.03 % Command : run_fmb4j /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.07/0.35 % Computer : n011.cluster.edu
% 0.07/0.35 % Model : x86_64 x86_64
% 0.07/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.07/0.35 % Memory : 8046.5625MB
% 0.07/0.35 % OS : Linux 6.8.0-71-generic
% 0.07/0.35 % CPULimit : 300
% 0.07/0.35 % WCLimit : 300
% 0.07/0.35 % DateTime : Thu Sep 24 19:47:13 UTC 2026
% 0.07/0.36 % CPUTime :
% 0.07/0.36 Running run_fmb4j /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.12/0.42 Running: java -jar /export/starexec/sandbox2/solver/bin/FMB4J.jar /export/starexec/sandbox2/tmp/tmp.9D9v3Y4cAm/theBenchmark.cnf 300
% 0.59/0.73 % domain size: 1
% 0.87/0.83 % domain size: 2
% 2.41/1.23 % model found for domain size 2
% 2.41/1.24 % SZS status CounterSatisfiable for theBenchmark
% 2.41/1.24 % SZS output start FiniteModel for theBenchmark
% See solution above
% 2.86/1.36 % FMB4L exiting
%------------------------------------------------------------------------------