%------------------------------------------------------------------------------ % File : Crossbow---0.1 % Problem : SWV439+1 : TPTP v8.1.0. Released v4.0.0. % Transfm : none % Format : tptp:raw % Command : do_Crossbow---0.1 %s % Computer : n021.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8042.1875MB % OS : Linux 3.10.0-693.el7.x86_64 % CPULimit : 300s % WCLimit : 600s % DateTime : Wed Jul 20 16:32:34 EDT 2022 % Result : CounterSatisfiable 5.29s 5.45s % Output : FiniteModel 5.29s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.04/0.13 % Problem : SWV439+1 : TPTP v8.1.0. Released v4.0.0. % 0.04/0.14 % Command : do_Crossbow---0.1 %s % 0.15/0.36 % Computer : n021.cluster.edu % 0.15/0.36 % Model : x86_64 x86_64 % 0.15/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.15/0.36 % Memory : 8042.1875MB % 0.15/0.36 % OS : Linux 3.10.0-693.el7.x86_64 % 0.15/0.36 % CPULimit : 300 % 0.15/0.36 % WCLimit : 600 % 0.15/0.36 % DateTime : Thu Jun 16 04:00:14 EDT 2022 % 0.15/0.36 % CPUTime : % 0.15/0.36 /export/starexec/sandbox/solver/bin % 0.15/0.37 crossbow.opt % 0.15/0.37 do_Crossbow---0.1 % 0.15/0.37 eprover % 0.15/0.37 runsolver % 0.15/0.37 starexec_run_Crossbow---0.1 % 5.29/5.45 % SZS status CounterSatisfiable for theBenchmark.p % 5.29/5.45 % SZS output start FiniteModel for theBenchmark.p % 5.29/5.45 % domain size: 2 % 5.29/5.45 fof(interp, fi_domain, ![X] : (X = 0 | X = 1)). % 5.29/5.45 fof(interp, fi_functors, admin = 0). % 5.29/5.45 fof(interp, fi_predicates, admin_compartment_has_scg(0, 0, 0) & % 5.29/5.45 ~admin_compartment_has_scg(0, 0, 1) & % 5.29/5.45 ~admin_compartment_has_scg(0, 1, 0) & % 5.29/5.45 ~admin_compartment_has_scg(0, 1, 1) & % 5.29/5.45 admin_compartment_has_scg(1, 0, 0) & % 5.29/5.45 ~admin_compartment_has_scg(1, 0, 1) & % 5.29/5.45 ~admin_compartment_has_scg(1, 1, 0) & % 5.29/5.45 ~admin_compartment_has_scg(1, 1, 1)). % 5.29/5.45 fof(interp, fi_predicates, admin_compartment_has_sso(0, 0, 0) & % 5.29/5.45 ~admin_compartment_has_sso(0, 0, 1) & % 5.29/5.45 ~admin_compartment_has_sso(0, 1, 0) & % 5.29/5.45 ~admin_compartment_has_sso(0, 1, 1) & % 5.29/5.45 admin_compartment_has_sso(1, 0, 0) & % 5.29/5.45 ~admin_compartment_has_sso(1, 0, 1) & % 5.29/5.45 ~admin_compartment_has_sso(1, 1, 0) & % 5.29/5.45 ~admin_compartment_has_sso(1, 1, 1)). % 5.29/5.45 fof(interp, fi_predicates, admin_file_has_citizenship(0, 0, 0) & % 5.29/5.45 ~admin_file_has_citizenship(0, 0, 1) & % 5.29/5.45 admin_file_has_citizenship(0, 1, 0) & % 5.29/5.45 ~admin_file_has_citizenship(0, 1, 1) & % 5.29/5.45 admin_file_has_citizenship(1, 0, 0) & % 5.29/5.45 ~admin_file_has_citizenship(1, 0, 1) & % 5.29/5.45 admin_file_has_citizenship(1, 1, 0) & % 5.29/5.45 ~admin_file_has_citizenship(1, 1, 1)). % 5.29/5.45 fof(interp, fi_predicates, admin_file_has_citizenship_h(0, 0, 0, 0) & % 5.29/5.45 ~admin_file_has_citizenship_h(0, 0, 0, 1) & % 5.29/5.45 admin_file_has_citizenship_h(0, 0, 1, 0) & % 5.29/5.45 ~admin_file_has_citizenship_h(0, 0, 1, 1) & % 5.29/5.45 admin_file_has_citizenship_h(0, 1, 0, 0) & % 5.29/5.45 ~admin_file_has_citizenship_h(0, 1, 0, 1) & % 5.29/5.45 admin_file_has_citizenship_h(0, 1, 1, 0) & % 5.29/5.45 ~admin_file_has_citizenship_h(0, 1, 1, 1) & % 5.29/5.45 admin_file_has_citizenship_h(1, 0, 0, 0) & % 5.29/5.45 ~admin_file_has_citizenship_h(1, 0, 0, 1) & % 5.29/5.45 admin_file_has_citizenship_h(1, 0, 1, 0) & % 5.29/5.45 ~admin_file_has_citizenship_h(1, 0, 1, 1) & % 5.29/5.45 admin_file_has_citizenship_h(1, 1, 0, 0) & % 5.29/5.45 ~admin_file_has_citizenship_h(1, 1, 0, 1) & % 5.29/5.45 admin_file_has_citizenship_h(1, 1, 1, 0) & % 5.29/5.45 ~admin_file_has_citizenship_h(1, 1, 1, 1)). % 5.29/5.45 fof(interp, fi_predicates, admin_file_has_compartments(0, 0, 0) & % 5.29/5.45 ~admin_file_has_compartments(0, 0, 1) & % 5.29/5.45 admin_file_has_compartments(0, 1, 0) & % 5.29/5.45 ~admin_file_has_compartments(0, 1, 1) & % 5.29/5.45 admin_file_has_compartments(1, 0, 0) & % 5.29/5.45 ~admin_file_has_compartments(1, 0, 1) & % 5.29/5.45 admin_file_has_compartments(1, 1, 0) & % 5.29/5.45 ~admin_file_has_compartments(1, 1, 1)). % 5.29/5.45 fof(interp, fi_predicates, admin_file_has_compartments_h(0, 0, 0, 0) & % 5.29/5.45 ~admin_file_has_compartments_h(0, 0, 0, 1) & % 5.29/5.45 admin_file_has_compartments_h(0, 0, 1, 0) & % 5.29/5.45 ~admin_file_has_compartments_h(0, 0, 1, 1) & % 5.29/5.45 admin_file_has_compartments_h(0, 1, 0, 0) & % 5.29/5.45 ~admin_file_has_compartments_h(0, 1, 0, 1) & % 5.29/5.45 admin_file_has_compartments_h(0, 1, 1, 0) & % 5.29/5.45 ~admin_file_has_compartments_h(0, 1, 1, 1) & % 5.29/5.45 admin_file_has_compartments_h(1, 0, 0, 0) & % 5.29/5.45 ~admin_file_has_compartments_h(1, 0, 0, 1) & % 5.29/5.45 admin_file_has_compartments_h(1, 0, 1, 0) & % 5.29/5.45 ~admin_file_has_compartments_h(1, 0, 1, 1) & % 5.29/5.45 admin_file_has_compartments_h(1, 1, 0, 0) & % 5.29/5.45 ~admin_file_has_compartments_h(1, 1, 0, 1) & % 5.29/5.45 admin_file_has_compartments_h(1, 1, 1, 0) & % 5.29/5.45 ~admin_file_has_compartments_h(1, 1, 1, 1)). % 5.29/5.45 fof(interp, fi_predicates, admin_file_has_level(0, 0, 0) & % 5.29/5.45 ~admin_file_has_level(0, 0, 1) & % 5.29/5.45 ~admin_file_has_level(0, 1, 0) & % 5.29/5.45 admin_file_has_level(0, 1, 1) & % 5.29/5.45 admin_file_has_level(1, 0, 0) & % 5.29/5.45 ~admin_file_has_level(1, 0, 1) & % 5.29/5.45 ~admin_file_has_level(1, 1, 0) & % 5.29/5.45 admin_file_has_level(1, 1, 1)). % 5.29/5.45 fof(interp, fi_predicates, admin_file_has_level_h(0, 0, 0, 0) & % 5.29/5.45 ~admin_file_has_level_h(0, 0, 0, 1) & % 5.29/5.45 admin_file_has_level_h(0, 0, 1, 0) & % 5.29/5.45 ~admin_file_has_level_h(0, 0, 1, 1) & % 5.29/5.45 admin_file_has_level_h(0, 1, 0, 0) & % 5.29/5.45 ~admin_file_has_level_h(0, 1, 0, 1) & % 5.29/5.45 admin_file_has_level_h(0, 1, 1, 0) & % 5.29/5.45 ~admin_file_has_level_h(0, 1, 1, 1) & % 5.29/5.45 admin_file_has_level_h(1, 0, 0, 0) & % 5.29/5.45 ~admin_file_has_level_h(1, 0, 0, 1) & % 5.29/5.45 admin_file_has_level_h(1, 0, 1, 0) & % 5.29/5.45 ~admin_file_has_level_h(1, 0, 1, 1) & % 5.29/5.45 admin_file_has_level_h(1, 1, 0, 0) & % 5.29/5.45 ~admin_file_has_level_h(1, 1, 0, 1) & % 5.29/5.45 admin_file_has_level_h(1, 1, 1, 0) & % 5.29/5.45 ~admin_file_has_level_h(1, 1, 1, 1)). % 5.29/5.45 fof(interp, fi_predicates, admin_indi_has_background(0, 0, 0) & % 5.29/5.45 admin_indi_has_background(0, 0, 1) & % 5.29/5.45 admin_indi_has_background(0, 1, 0) & % 5.29/5.45 admin_indi_has_background(0, 1, 1) & % 5.29/5.45 admin_indi_has_background(1, 0, 0) & % 5.29/5.45 admin_indi_has_background(1, 0, 1) & % 5.29/5.45 admin_indi_has_background(1, 1, 0) & % 5.29/5.45 admin_indi_has_background(1, 1, 1)). % 5.29/5.45 fof(interp, fi_predicates, admin_indi_has_background_for_compartment(0, 0, 0) & % 5.29/5.45 admin_indi_has_background_for_compartment(0, 0, 1) & % 5.29/5.45 admin_indi_has_background_for_compartment(0, 1, 0) & % 5.29/5.45 admin_indi_has_background_for_compartment(0, 1, 1) & % 5.29/5.45 admin_indi_has_background_for_compartment(1, 0, 0) & % 5.29/5.45 admin_indi_has_background_for_compartment(1, 0, 1) & % 5.29/5.45 admin_indi_has_background_for_compartment(1, 1, 0) & % 5.29/5.45 admin_indi_has_background_for_compartment(1, 1, 1)). % 5.29/5.45 fof(interp, fi_predicates, admin_indi_has_citizenship(0, 0, 0) & % 5.29/5.45 ~admin_indi_has_citizenship(0, 0, 1) & % 5.29/5.45 admin_indi_has_citizenship(0, 1, 0) & % 5.29/5.45 ~admin_indi_has_citizenship(0, 1, 1) & % 5.29/5.45 admin_indi_has_citizenship(1, 0, 0) & % 5.29/5.45 ~admin_indi_has_citizenship(1, 0, 1) & % 5.29/5.45 admin_indi_has_citizenship(1, 1, 0) & % 5.29/5.45 ~admin_indi_has_citizenship(1, 1, 1)). % 5.29/5.45 fof(interp, fi_predicates, admin_indi_has_citizenship_for_file(0, 0, 0) & % 5.29/5.45 admin_indi_has_citizenship_for_file(0, 0, 1) & % 5.29/5.45 admin_indi_has_citizenship_for_file(0, 1, 0) & % 5.29/5.45 admin_indi_has_citizenship_for_file(0, 1, 1) & % 5.29/5.45 admin_indi_has_citizenship_for_file(1, 0, 0) & % 5.29/5.45 admin_indi_has_citizenship_for_file(1, 0, 1) & % 5.29/5.45 admin_indi_has_citizenship_for_file(1, 1, 0) & % 5.29/5.45 admin_indi_has_citizenship_for_file(1, 1, 1)). % 5.29/5.45 fof(interp, fi_predicates, admin_indi_has_compartments(0, 0, 0) & % 5.29/5.45 ~admin_indi_has_compartments(0, 0, 1) & % 5.29/5.45 admin_indi_has_compartments(0, 1, 0) & % 5.29/5.45 ~admin_indi_has_compartments(0, 1, 1) & % 5.29/5.45 admin_indi_has_compartments(1, 0, 0) & % 5.29/5.45 ~admin_indi_has_compartments(1, 0, 1) & % 5.29/5.45 admin_indi_has_compartments(1, 1, 0) & % 5.29/5.45 ~admin_indi_has_compartments(1, 1, 1)). % 5.29/5.45 fof(interp, fi_predicates, admin_indi_has_compartments_for_file(0, 0, 0) & % 5.29/5.45 admin_indi_has_compartments_for_file(0, 0, 1) & % 5.29/5.45 admin_indi_has_compartments_for_file(0, 1, 0) & % 5.29/5.45 admin_indi_has_compartments_for_file(0, 1, 1) & % 5.29/5.45 admin_indi_has_compartments_for_file(1, 0, 0) & % 5.29/5.45 admin_indi_has_compartments_for_file(1, 0, 1) & % 5.29/5.45 admin_indi_has_compartments_for_file(1, 1, 0) & % 5.29/5.45 admin_indi_has_compartments_for_file(1, 1, 1)). % 5.29/5.45 fof(interp, fi_predicates, admin_indi_has_credit(0, 0) & % 5.29/5.45 ~admin_indi_has_credit(0, 1) & % 5.29/5.45 admin_indi_has_credit(1, 0) & % 5.29/5.45 ~admin_indi_has_credit(1, 1)). % 5.29/5.45 fof(interp, fi_predicates, admin_indi_has_credit_for_compartment(0, 0, 0) & % 5.29/5.45 admin_indi_has_credit_for_compartment(0, 0, 1) & % 5.29/5.45 admin_indi_has_credit_for_compartment(0, 1, 0) & % 5.29/5.45 admin_indi_has_credit_for_compartment(0, 1, 1) & % 5.29/5.45 admin_indi_has_credit_for_compartment(1, 0, 0) & % 5.29/5.45 admin_indi_has_credit_for_compartment(1, 0, 1) & % 5.29/5.45 admin_indi_has_credit_for_compartment(1, 1, 0) & % 5.29/5.45 admin_indi_has_credit_for_compartment(1, 1, 1)). % 5.29/5.45 fof(interp, fi_predicates, admin_indi_has_employment(0, 0) & % 5.29/5.45 ~admin_indi_has_employment(0, 1) & % 5.29/5.45 admin_indi_has_employment(1, 0) & % 5.29/5.45 ~admin_indi_has_employment(1, 1)). % 5.29/5.45 fof(interp, fi_predicates, admin_indi_has_level(0, 0, 0) & % 5.29/5.45 admin_indi_has_level(0, 0, 1) & % 5.29/5.45 ~admin_indi_has_level(0, 1, 0) & % 5.29/5.45 admin_indi_has_level(0, 1, 1) & % 5.29/5.45 admin_indi_has_level(1, 0, 0) & % 5.29/5.45 admin_indi_has_level(1, 0, 1) & % 5.29/5.45 ~admin_indi_has_level(1, 1, 0) & % 5.29/5.45 admin_indi_has_level(1, 1, 1)). % 5.29/5.45 fof(interp, fi_predicates, admin_indi_has_level_for_compartment(0, 0, 0) & % 5.29/5.45 ~admin_indi_has_level_for_compartment(0, 0, 1) & % 5.29/5.45 ~admin_indi_has_level_for_compartment(0, 1, 0) & % 5.29/5.45 ~admin_indi_has_level_for_compartment(0, 1, 1) & % 5.29/5.45 admin_indi_has_level_for_compartment(1, 0, 0) & % 5.29/5.45 ~admin_indi_has_level_for_compartment(1, 0, 1) & % 5.29/5.45 ~admin_indi_has_level_for_compartment(1, 1, 0) & % 5.29/5.45 ~admin_indi_has_level_for_compartment(1, 1, 1)). % 5.29/5.45 fof(interp, fi_predicates, admin_indi_has_level_for_file(0, 0, 0) & % 5.29/5.45 admin_indi_has_level_for_file(0, 0, 1) & % 5.29/5.45 ~admin_indi_has_level_for_file(0, 1, 0) & % 5.29/5.45 admin_indi_has_level_for_file(0, 1, 1) & % 5.29/5.45 admin_indi_has_level_for_file(1, 0, 0) & % 5.29/5.45 admin_indi_has_level_for_file(1, 0, 1) & % 5.29/5.45 ~admin_indi_has_level_for_file(1, 1, 0) & % 5.29/5.45 admin_indi_has_level_for_file(1, 1, 1)). % 5.29/5.45 fof(interp, fi_predicates, admin_indi_has_need_to_know_for_file(0, 0, 0) & % 5.29/5.45 ~admin_indi_has_need_to_know_for_file(0, 0, 1) & % 5.29/5.45 admin_indi_has_need_to_know_for_file(0, 1, 0) & % 5.29/5.45 admin_indi_has_need_to_know_for_file(0, 1, 1) & % 5.29/5.45 admin_indi_has_need_to_know_for_file(1, 0, 0) & % 5.29/5.45 ~admin_indi_has_need_to_know_for_file(1, 0, 1) & % 5.29/5.45 admin_indi_has_need_to_know_for_file(1, 1, 0) & % 5.29/5.45 admin_indi_has_need_to_know_for_file(1, 1, 1)). % 5.29/5.45 fof(interp, fi_predicates, admin_indi_has_polygraph(0, 0) & % 5.29/5.45 ~admin_indi_has_polygraph(0, 1) & % 5.29/5.45 admin_indi_has_polygraph(1, 0) & % 5.29/5.45 ~admin_indi_has_polygraph(1, 1)). % 5.29/5.45 fof(interp, fi_predicates, admin_indi_has_polygraph_for_compartment(0, 0, 0) & % 5.29/5.45 admin_indi_has_polygraph_for_compartment(0, 0, 1) & % 5.29/5.45 admin_indi_has_polygraph_for_compartment(0, 1, 0) & % 5.29/5.45 admin_indi_has_polygraph_for_compartment(0, 1, 1) & % 5.29/5.45 admin_indi_has_polygraph_for_compartment(1, 0, 0) & % 5.29/5.45 admin_indi_has_polygraph_for_compartment(1, 0, 1) & % 5.29/5.45 admin_indi_has_polygraph_for_compartment(1, 1, 0) & % 5.29/5.45 admin_indi_has_polygraph_for_compartment(1, 1, 1)). % 5.29/5.45 fof(interp, fi_predicates, admin_indi_may_file(0, 0, 0, 0) & % 5.29/5.45 admin_indi_may_file(0, 0, 0, 1) & % 5.29/5.45 ~admin_indi_may_file(0, 0, 1, 0) & % 5.29/5.45 ~admin_indi_may_file(0, 0, 1, 1) & % 5.29/5.45 ~admin_indi_may_file(0, 1, 0, 0) & % 5.29/5.45 ~admin_indi_may_file(0, 1, 0, 1) & % 5.29/5.45 admin_indi_may_file(0, 1, 1, 0) & % 5.29/5.45 admin_indi_may_file(0, 1, 1, 1) & % 5.29/5.45 admin_indi_may_file(1, 0, 0, 0) & % 5.29/5.45 admin_indi_may_file(1, 0, 0, 1) & % 5.29/5.45 ~admin_indi_may_file(1, 0, 1, 0) & % 5.29/5.45 ~admin_indi_may_file(1, 0, 1, 1) & % 5.29/5.45 ~admin_indi_may_file(1, 1, 0, 0) & % 5.29/5.45 ~admin_indi_may_file(1, 1, 0, 1) & % 5.29/5.45 admin_indi_may_file(1, 1, 1, 0) & % 5.29/5.45 admin_indi_may_file(1, 1, 1, 1)). % 5.29/5.45 fof(interp, fi_functors, alice = 0). % 5.29/5.45 fof(interp, fi_functors, anycountry = 0). % 5.29/5.45 fof(interp, fi_functors, babu = 1). % 5.29/5.45 fof(interp, fi_functors, background_admin = 0). % 5.29/5.45 fof(interp, fi_predicates, background_admin_indi_has_background(0, 0, 0) & % 5.29/5.45 ~background_admin_indi_has_background(0, 0, 1) & % 5.29/5.45 ~background_admin_indi_has_background(0, 1, 0) & % 5.29/5.45 ~background_admin_indi_has_background(0, 1, 1) & % 5.29/5.45 background_admin_indi_has_background(1, 0, 0) & % 5.29/5.45 ~background_admin_indi_has_background(1, 0, 1) & % 5.29/5.45 ~background_admin_indi_has_background(1, 1, 0) & % 5.29/5.45 ~background_admin_indi_has_background(1, 1, 1)). % 5.29/5.45 fof(interp, fi_functors, ci = 0). % 5.29/5.45 fof(interp, fi_functors, compartmenta = 0). % 5.29/5.45 fof(interp, fi_functors, compartmentb = 0). % 5.29/5.45 fof(interp, fi_functors, confidential = 0). % 5.29/5.45 fof(interp, fi_functors, cons(0, 0) = 0 & cons(0, 1) = 1 & cons(1, 0) = 0 & % 5.29/5.45 cons(1, 1) = 0). % 5.29/5.45 fof(interp, fi_functors, credit_admin = 0). % 5.29/5.45 fof(interp, fi_predicates, credit_admin_indi_has_credit(0, 0) & % 5.29/5.45 ~credit_admin_indi_has_credit(0, 1) & % 5.29/5.45 credit_admin_indi_has_credit(1, 0) & % 5.29/5.45 ~credit_admin_indi_has_credit(1, 1)). % 5.29/5.45 fof(interp, fi_functors, hr_admin = 0). % 5.29/5.45 fof(interp, fi_predicates, hr_admin_indi_has_employment(0, 0) & % 5.29/5.45 ~hr_admin_indi_has_employment(0, 1) & % 5.29/5.45 hr_admin_indi_has_employment(1, 0) & % 5.29/5.45 ~hr_admin_indi_has_employment(1, 1)). % 5.29/5.45 fof(interp, fi_functors, india = 0). % 5.29/5.45 fof(interp, fi_functors, level_admin = 0). % 5.29/5.45 fof(interp, fi_predicates, level_admin_indi_has_level(0, 0, 0) & % 5.29/5.45 ~level_admin_indi_has_level(0, 0, 1) & % 5.29/5.45 ~level_admin_indi_has_level(0, 1, 0) & % 5.29/5.45 ~level_admin_indi_has_level(0, 1, 1) & % 5.29/5.45 level_admin_indi_has_level(1, 0, 0) & % 5.29/5.45 ~level_admin_indi_has_level(1, 0, 1) & % 5.29/5.45 ~level_admin_indi_has_level(1, 1, 0) & % 5.29/5.45 ~level_admin_indi_has_level(1, 1, 1)). % 5.29/5.45 fof(interp, fi_predicates, loca_level_below(0, 0, 0) & % 5.29/5.45 ~loca_level_below(0, 0, 1) & % 5.29/5.45 loca_level_below(0, 1, 0) & % 5.29/5.45 loca_level_below(0, 1, 1) & % 5.29/5.45 loca_level_below(1, 0, 0) & % 5.29/5.45 ~loca_level_below(1, 0, 1) & % 5.29/5.45 loca_level_below(1, 1, 0) & % 5.29/5.45 loca_level_below(1, 1, 1)). % 5.29/5.45 fof(interp, fi_predicates, loca_level_direct_below(0, 0, 0) & % 5.29/5.45 ~loca_level_direct_below(0, 0, 1) & % 5.29/5.45 loca_level_direct_below(0, 1, 0) & % 5.29/5.45 ~loca_level_direct_below(0, 1, 1) & % 5.29/5.45 loca_level_direct_below(1, 0, 0) & % 5.29/5.45 ~loca_level_direct_below(1, 0, 1) & % 5.29/5.45 loca_level_direct_below(1, 1, 0) & % 5.29/5.45 ~loca_level_direct_below(1, 1, 1)). % 5.29/5.45 fof(interp, fi_functors, nil = 0). % 5.29/5.45 fof(interp, fi_functors, no = 0). % 5.29/5.45 fof(interp, fi_functors, not_secretfile = 1). % 5.29/5.45 fof(interp, fi_functors, oca = 0). % 5.29/5.45 fof(interp, fi_predicates, oca_compartment_has_scg(0, 0, 0) & % 5.29/5.45 ~oca_compartment_has_scg(0, 0, 1) & % 5.29/5.45 ~oca_compartment_has_scg(0, 1, 0) & % 5.29/5.45 ~oca_compartment_has_scg(0, 1, 1) & % 5.29/5.45 oca_compartment_has_scg(1, 0, 0) & % 5.29/5.45 ~oca_compartment_has_scg(1, 0, 1) & % 5.29/5.45 ~oca_compartment_has_scg(1, 1, 0) & % 5.29/5.45 ~oca_compartment_has_scg(1, 1, 1)). % 5.29/5.45 fof(interp, fi_predicates, oca_compartment_is_compartment(0, 0, 0, 0, 0, 0) & % 5.29/5.45 ~oca_compartment_is_compartment(0, 0, 0, 0, 0, 1) & % 5.29/5.45 ~oca_compartment_is_compartment(0, 0, 0, 0, 1, 0) & % 5.29/5.45 ~oca_compartment_is_compartment(0, 0, 0, 0, 1, 1) & % 5.29/5.45 oca_compartment_is_compartment(0, 0, 0, 1, 0, 0) & % 5.29/5.45 ~oca_compartment_is_compartment(0, 0, 0, 1, 0, 1) & % 5.29/5.45 ~oca_compartment_is_compartment(0, 0, 0, 1, 1, 0) & % 5.29/5.45 ~oca_compartment_is_compartment(0, 0, 0, 1, 1, 1) & % 5.29/5.45 ~oca_compartment_is_compartment(0, 0, 1, 0, 0, 0) & % 5.29/5.45 ~oca_compartment_is_compartment(0, 0, 1, 0, 0, 1) & % 5.29/5.45 ~oca_compartment_is_compartment(0, 0, 1, 0, 1, 0) & % 5.29/5.45 ~oca_compartment_is_compartment(0, 0, 1, 0, 1, 1) & % 5.29/5.45 ~oca_compartment_is_compartment(0, 0, 1, 1, 0, 0) & % 5.29/5.45 ~oca_compartment_is_compartment(0, 0, 1, 1, 0, 1) & % 5.29/5.45 ~oca_compartment_is_compartment(0, 0, 1, 1, 1, 0) & % 5.29/5.45 ~oca_compartment_is_compartment(0, 0, 1, 1, 1, 1) & % 5.29/5.45 ~oca_compartment_is_compartment(0, 1, 0, 0, 0, 0) & % 5.29/5.45 ~oca_compartment_is_compartment(0, 1, 0, 0, 0, 1) & % 5.29/5.45 ~oca_compartment_is_compartment(0, 1, 0, 0, 1, 0) & % 5.29/5.45 ~oca_compartment_is_compartment(0, 1, 0, 0, 1, 1) & % 5.29/5.45 ~oca_compartment_is_compartment(0, 1, 0, 1, 0, 0) & % 5.29/5.45 ~oca_compartment_is_compartment(0, 1, 0, 1, 0, 1) & % 5.29/5.45 ~oca_compartment_is_compartment(0, 1, 0, 1, 1, 0) & % 5.29/5.45 ~oca_compartment_is_compartment(0, 1, 0, 1, 1, 1) & % 5.29/5.45 ~oca_compartment_is_compartment(0, 1, 1, 0, 0, 0) & % 5.29/5.45 ~oca_compartment_is_compartment(0, 1, 1, 0, 0, 1) & % 5.29/5.45 ~oca_compartment_is_compartment(0, 1, 1, 0, 1, 0) & % 5.29/5.45 ~oca_compartment_is_compartment(0, 1, 1, 0, 1, 1) & % 5.29/5.45 ~oca_compartment_is_compartment(0, 1, 1, 1, 0, 0) & % 5.29/5.45 ~oca_compartment_is_compartment(0, 1, 1, 1, 0, 1) & % 5.29/5.45 ~oca_compartment_is_compartment(0, 1, 1, 1, 1, 0) & % 5.29/5.45 ~oca_compartment_is_compartment(0, 1, 1, 1, 1, 1) & % 5.29/5.45 oca_compartment_is_compartment(1, 0, 0, 0, 0, 0) & % 5.29/5.45 ~oca_compartment_is_compartment(1, 0, 0, 0, 0, 1) & % 5.29/5.45 ~oca_compartment_is_compartment(1, 0, 0, 0, 1, 0) & % 5.29/5.45 ~oca_compartment_is_compartment(1, 0, 0, 0, 1, 1) & % 5.29/5.45 oca_compartment_is_compartment(1, 0, 0, 1, 0, 0) & % 5.29/5.45 ~oca_compartment_is_compartment(1, 0, 0, 1, 0, 1) & % 5.29/5.45 ~oca_compartment_is_compartment(1, 0, 0, 1, 1, 0) & % 5.29/5.45 ~oca_compartment_is_compartment(1, 0, 0, 1, 1, 1) & % 5.29/5.45 ~oca_compartment_is_compartment(1, 0, 1, 0, 0, 0) & % 5.29/5.45 ~oca_compartment_is_compartment(1, 0, 1, 0, 0, 1) & % 5.29/5.45 ~oca_compartment_is_compartment(1, 0, 1, 0, 1, 0) & % 5.29/5.45 ~oca_compartment_is_compartment(1, 0, 1, 0, 1, 1) & % 5.29/5.45 ~oca_compartment_is_compartment(1, 0, 1, 1, 0, 0) & % 5.29/5.45 ~oca_compartment_is_compartment(1, 0, 1, 1, 0, 1) & % 5.29/5.45 ~oca_compartment_is_compartment(1, 0, 1, 1, 1, 0) & % 5.29/5.45 ~oca_compartment_is_compartment(1, 0, 1, 1, 1, 1) & % 5.29/5.45 ~oca_compartment_is_compartment(1, 1, 0, 0, 0, 0) & % 5.29/5.45 ~oca_compartment_is_compartment(1, 1, 0, 0, 0, 1) & % 5.29/5.45 ~oca_compartment_is_compartment(1, 1, 0, 0, 1, 0) & % 5.29/5.45 ~oca_compartment_is_compartment(1, 1, 0, 0, 1, 1) & % 5.29/5.45 ~oca_compartment_is_compartment(1, 1, 0, 1, 0, 0) & % 5.29/5.45 ~oca_compartment_is_compartment(1, 1, 0, 1, 0, 1) & % 5.29/5.45 ~oca_compartment_is_compartment(1, 1, 0, 1, 1, 0) & % 5.29/5.45 ~oca_compartment_is_compartment(1, 1, 0, 1, 1, 1) & % 5.29/5.45 ~oca_compartment_is_compartment(1, 1, 1, 0, 0, 0) & % 5.29/5.45 ~oca_compartment_is_compartment(1, 1, 1, 0, 0, 1) & % 5.29/5.45 ~oca_compartment_is_compartment(1, 1, 1, 0, 1, 0) & % 5.29/5.45 ~oca_compartment_is_compartment(1, 1, 1, 0, 1, 1) & % 5.29/5.45 ~oca_compartment_is_compartment(1, 1, 1, 1, 0, 0) & % 5.29/5.45 ~oca_compartment_is_compartment(1, 1, 1, 1, 0, 1) & % 5.29/5.45 ~oca_compartment_is_compartment(1, 1, 1, 1, 1, 0) & % 5.29/5.45 ~oca_compartment_is_compartment(1, 1, 1, 1, 1, 1)). % 5.29/5.45 fof(interp, fi_predicates, owner_indi_has_need_to_know(0, 0, 0) & % 5.29/5.45 owner_indi_has_need_to_know(0, 0, 1) & % 5.29/5.45 ~owner_indi_has_need_to_know(0, 1, 0) & % 5.29/5.45 ~owner_indi_has_need_to_know(0, 1, 1) & % 5.29/5.45 ~owner_indi_has_need_to_know(1, 0, 0) & % 5.29/5.45 ~owner_indi_has_need_to_know(1, 0, 1) & % 5.29/5.45 owner_indi_has_need_to_know(1, 1, 0) & % 5.29/5.45 owner_indi_has_need_to_know(1, 1, 1)). % 5.29/5.45 fof(interp, fi_functors, owner_not_secretfile = 1). % 5.29/5.45 fof(interp, fi_functors, owner_secretfile = 0). % 5.29/5.45 fof(interp, fi_functors, polygraph_admin = 0). % 5.29/5.45 fof(interp, fi_predicates, polygraph_admin_indi_has_polygraph(0, 0) & % 5.29/5.45 ~polygraph_admin_indi_has_polygraph(0, 1) & % 5.29/5.45 polygraph_admin_indi_has_polygraph(1, 0) & % 5.29/5.45 ~polygraph_admin_indi_has_polygraph(1, 1)). % 5.29/5.45 fof(interp, fi_functors, read = 0). % 5.29/5.45 fof(interp, fi_functors, sbu = 0). % 5.29/5.45 fof(interp, fi_functors, scg_compartmenta = 0). % 5.29/5.45 fof(interp, fi_functors, scg_compartmentb = 0). % 5.29/5.45 fof(interp, fi_functors, secret = 0). % 5.29/5.45 fof(interp, fi_functors, secretfile = 0). % 5.29/5.45 fof(interp, fi_predicates, sso_compartment_has_scg(0, 0, 0) & % 5.29/5.45 ~sso_compartment_has_scg(0, 0, 1) & % 5.29/5.45 ~sso_compartment_has_scg(0, 1, 0) & % 5.29/5.45 ~sso_compartment_has_scg(0, 1, 1) & % 5.29/5.45 ~sso_compartment_has_scg(1, 0, 0) & % 5.29/5.45 ~sso_compartment_has_scg(1, 0, 1) & % 5.29/5.45 ~sso_compartment_has_scg(1, 1, 0) & % 5.29/5.45 ~sso_compartment_has_scg(1, 1, 1)). % 5.29/5.45 fof(interp, fi_functors, sso_compartmenta = 0). % 5.29/5.45 fof(interp, fi_functors, sso_compartmentb = 0). % 5.29/5.45 fof(interp, fi_predicates, sso_file_has_citizenship(0, 0, 0, 0) & % 5.29/5.45 ~sso_file_has_citizenship(0, 0, 0, 1) & % 5.29/5.45 ~sso_file_has_citizenship(0, 0, 1, 0) & % 5.29/5.45 ~sso_file_has_citizenship(0, 0, 1, 1) & % 5.29/5.45 ~sso_file_has_citizenship(0, 1, 0, 0) & % 5.29/5.45 ~sso_file_has_citizenship(0, 1, 0, 1) & % 5.29/5.45 ~sso_file_has_citizenship(0, 1, 1, 0) & % 5.29/5.45 ~sso_file_has_citizenship(0, 1, 1, 1) & % 5.29/5.45 ~sso_file_has_citizenship(1, 0, 0, 0) & % 5.29/5.45 ~sso_file_has_citizenship(1, 0, 0, 1) & % 5.29/5.45 ~sso_file_has_citizenship(1, 0, 1, 0) & % 5.29/5.45 ~sso_file_has_citizenship(1, 0, 1, 1) & % 5.29/5.45 ~sso_file_has_citizenship(1, 1, 0, 0) & % 5.29/5.45 ~sso_file_has_citizenship(1, 1, 0, 1) & % 5.29/5.45 ~sso_file_has_citizenship(1, 1, 1, 0) & % 5.29/5.45 ~sso_file_has_citizenship(1, 1, 1, 1)). % 5.29/5.45 fof(interp, fi_predicates, sso_file_has_compartments(0, 0, 0) & % 5.29/5.45 ~sso_file_has_compartments(0, 0, 1) & % 5.29/5.45 ~sso_file_has_compartments(0, 1, 0) & % 5.29/5.45 ~sso_file_has_compartments(0, 1, 1) & % 5.29/5.45 ~sso_file_has_compartments(1, 0, 0) & % 5.29/5.45 ~sso_file_has_compartments(1, 0, 1) & % 5.29/5.45 ~sso_file_has_compartments(1, 1, 0) & % 5.29/5.45 ~sso_file_has_compartments(1, 1, 1)). % 5.29/5.45 fof(interp, fi_predicates, sso_file_has_level(0, 0, 0, 0) & % 5.29/5.45 ~sso_file_has_level(0, 0, 0, 1) & % 5.29/5.45 ~sso_file_has_level(0, 0, 1, 0) & % 5.29/5.45 ~sso_file_has_level(0, 0, 1, 1) & % 5.29/5.45 ~sso_file_has_level(0, 1, 0, 0) & % 5.29/5.45 ~sso_file_has_level(0, 1, 0, 1) & % 5.29/5.45 ~sso_file_has_level(0, 1, 1, 0) & % 5.29/5.45 ~sso_file_has_level(0, 1, 1, 1) & % 5.29/5.45 ~sso_file_has_level(1, 0, 0, 0) & % 5.29/5.45 ~sso_file_has_level(1, 0, 0, 1) & % 5.29/5.45 ~sso_file_has_level(1, 0, 1, 0) & % 5.29/5.45 ~sso_file_has_level(1, 0, 1, 1) & % 5.29/5.45 ~sso_file_has_level(1, 1, 0, 0) & % 5.29/5.45 ~sso_file_has_level(1, 1, 0, 1) & % 5.29/5.45 ~sso_file_has_level(1, 1, 1, 0) & % 5.29/5.45 ~sso_file_has_level(1, 1, 1, 1)). % 5.29/5.45 fof(interp, fi_predicates, sso_indi_has_compartment(0, 0, 0) & % 5.29/5.45 ~sso_indi_has_compartment(0, 0, 1) & % 5.29/5.45 ~sso_indi_has_compartment(0, 1, 0) & % 5.29/5.45 ~sso_indi_has_compartment(0, 1, 1) & % 5.29/5.45 ~sso_indi_has_compartment(1, 0, 0) & % 5.29/5.45 ~sso_indi_has_compartment(1, 0, 1) & % 5.29/5.45 ~sso_indi_has_compartment(1, 1, 0) & % 5.29/5.45 ~sso_indi_has_compartment(1, 1, 1)). % 5.29/5.45 fof(interp, fi_predicates, state_file_has_owner(0, 0) & % 5.29/5.45 state_file_has_owner(0, 1) & % 5.29/5.45 ~state_file_has_owner(1, 0) & % 5.29/5.45 state_file_has_owner(1, 1)). % 5.29/5.45 fof(interp, fi_predicates, state_file_is_not_working_paper(0) & % 5.29/5.45 state_file_is_not_working_paper(1)). % 5.29/5.45 fof(interp, fi_functors, system = 0). % 5.29/5.45 fof(interp, fi_predicates, system_compartment_has_sso(0, 0, 0) & % 5.29/5.45 ~system_compartment_has_sso(0, 0, 1) & % 5.29/5.45 ~system_compartment_has_sso(0, 1, 0) & % 5.29/5.45 ~system_compartment_has_sso(0, 1, 1) & % 5.29/5.45 system_compartment_has_sso(1, 0, 0) & % 5.29/5.45 ~system_compartment_has_sso(1, 0, 1) & % 5.29/5.45 ~system_compartment_has_sso(1, 1, 0) & % 5.29/5.45 ~system_compartment_has_sso(1, 1, 1)). % 5.29/5.45 fof(interp, fi_predicates, system_file_needs_citizenship(0, 0, 0) & % 5.29/5.45 ~system_file_needs_citizenship(0, 0, 1) & % 5.29/5.45 system_file_needs_citizenship(0, 1, 0) & % 5.29/5.45 ~system_file_needs_citizenship(0, 1, 1) & % 5.29/5.45 system_file_needs_citizenship(1, 0, 0) & % 5.29/5.45 ~system_file_needs_citizenship(1, 0, 1) & % 5.29/5.45 system_file_needs_citizenship(1, 1, 0) & % 5.29/5.45 ~system_file_needs_citizenship(1, 1, 1)). % 5.29/5.45 fof(interp, fi_predicates, system_file_needs_compartments(0, 0, 0) & % 5.29/5.45 ~system_file_needs_compartments(0, 0, 1) & % 5.29/5.45 system_file_needs_compartments(0, 1, 0) & % 5.29/5.45 ~system_file_needs_compartments(0, 1, 1) & % 5.29/5.45 system_file_needs_compartments(1, 0, 0) & % 5.29/5.45 ~system_file_needs_compartments(1, 0, 1) & % 5.29/5.45 system_file_needs_compartments(1, 1, 0) & % 5.29/5.45 ~system_file_needs_compartments(1, 1, 1)). % 5.29/5.45 fof(interp, fi_predicates, system_file_needs_level(0, 0, 0) & % 5.29/5.45 ~system_file_needs_level(0, 0, 1) & % 5.29/5.45 ~system_file_needs_level(0, 1, 0) & % 5.29/5.45 system_file_needs_level(0, 1, 1) & % 5.29/5.45 system_file_needs_level(1, 0, 0) & % 5.29/5.45 ~system_file_needs_level(1, 0, 1) & % 5.29/5.45 ~system_file_needs_level(1, 1, 0) & % 5.29/5.45 system_file_needs_level(1, 1, 1)). % 5.29/5.45 fof(interp, fi_predicates, system_indi_has_citizenship(0, 0, 0) & % 5.29/5.45 ~system_indi_has_citizenship(0, 0, 1) & % 5.29/5.45 system_indi_has_citizenship(0, 1, 0) & % 5.29/5.45 ~system_indi_has_citizenship(0, 1, 1) & % 5.29/5.45 system_indi_has_citizenship(1, 0, 0) & % 5.29/5.45 ~system_indi_has_citizenship(1, 0, 1) & % 5.29/5.45 system_indi_has_citizenship(1, 1, 0) & % 5.29/5.45 ~system_indi_has_citizenship(1, 1, 1)). % 5.29/5.45 fof(interp, fi_predicates, system_indi_is_background_admin(0, 0) & % 5.29/5.45 system_indi_is_background_admin(0, 1) & % 5.29/5.45 system_indi_is_background_admin(1, 0) & % 5.29/5.45 system_indi_is_background_admin(1, 1)). % 5.29/5.45 fof(interp, fi_predicates, system_indi_is_counterintelligence(0, 0, 0) & % 5.29/5.45 ~system_indi_is_counterintelligence(0, 0, 1) & % 5.29/5.45 ~system_indi_is_counterintelligence(0, 1, 0) & % 5.29/5.45 ~system_indi_is_counterintelligence(0, 1, 1) & % 5.29/5.45 system_indi_is_counterintelligence(1, 0, 0) & % 5.29/5.45 ~system_indi_is_counterintelligence(1, 0, 1) & % 5.29/5.45 ~system_indi_is_counterintelligence(1, 1, 0) & % 5.29/5.45 ~system_indi_is_counterintelligence(1, 1, 1)). % 5.29/5.45 fof(interp, fi_predicates, system_indi_is_credit_admin(0, 0) & % 5.29/5.45 system_indi_is_credit_admin(0, 1) & % 5.29/5.45 system_indi_is_credit_admin(1, 0) & % 5.29/5.45 system_indi_is_credit_admin(1, 1)). % 5.29/5.45 fof(interp, fi_predicates, system_indi_is_hr_admin(0, 0) & % 5.29/5.45 system_indi_is_hr_admin(0, 1) & % 5.29/5.46 system_indi_is_hr_admin(1, 0) & % 5.29/5.46 system_indi_is_hr_admin(1, 1)). % 5.29/5.46 fof(interp, fi_predicates, system_indi_is_level_admin(0, 0) & % 5.29/5.46 system_indi_is_level_admin(0, 1) & % 5.29/5.46 system_indi_is_level_admin(1, 0) & % 5.29/5.46 system_indi_is_level_admin(1, 1)). % 5.29/5.46 fof(interp, fi_predicates, system_indi_is_oca(0, 0) & system_indi_is_oca(0, 1) & % 5.29/5.46 system_indi_is_oca(1, 0) & % 5.29/5.46 system_indi_is_oca(1, 1)). % 5.29/5.46 fof(interp, fi_predicates, system_indi_is_polygraph_admin(0, 0) & % 5.29/5.46 system_indi_is_polygraph_admin(0, 1) & % 5.29/5.46 system_indi_is_polygraph_admin(1, 0) & % 5.29/5.46 system_indi_is_polygraph_admin(1, 1)). % 5.29/5.46 fof(interp, fi_predicates, system_indi_needs_compartment(0, 0, 0) & % 5.29/5.46 ~system_indi_needs_compartment(0, 0, 1) & % 5.29/5.46 ~system_indi_needs_compartment(0, 1, 0) & % 5.29/5.46 ~system_indi_needs_compartment(0, 1, 1) & % 5.29/5.46 system_indi_needs_compartment(1, 0, 0) & % 5.29/5.46 ~system_indi_needs_compartment(1, 0, 1) & % 5.29/5.46 ~system_indi_needs_compartment(1, 1, 0) & % 5.29/5.46 ~system_indi_needs_compartment(1, 1, 1)). % 5.29/5.46 fof(interp, fi_predicates, system_indi_needs_level(0, 0, 0) & % 5.29/5.46 ~system_indi_needs_level(0, 0, 1) & % 5.29/5.46 ~system_indi_needs_level(0, 1, 0) & % 5.29/5.46 ~system_indi_needs_level(0, 1, 1) & % 5.29/5.46 system_indi_needs_level(1, 0, 0) & % 5.29/5.46 ~system_indi_needs_level(1, 0, 1) & % 5.29/5.46 ~system_indi_needs_level(1, 1, 0) & % 5.29/5.46 ~system_indi_needs_level(1, 1, 1)). % 5.29/5.46 fof(interp, fi_functors, topsecret = 0). % 5.29/5.46 fof(interp, fi_functors, unclassified = 1). % 5.29/5.46 fof(interp, fi_functors, usa = 0). % 5.29/5.46 fof(interp, fi_functors, yes = 0). % 5.29/5.46 % SZS output end FiniteModel for theBenchmark.p % 5.29/5.46 % 16 lemma(s) from E % 5.29/5.46 % cnf(cl, axiom, admin_indi_has_citizenship(admin, babu, india)). % 5.29/5.46 % cnf(cl, axiom, admin_indi_has_citizenship(admin, alice, usa)). % 5.29/5.46 % cnf(cl, axiom, loca_level_below(A, confidential, secret)). % 5.29/5.46 % cnf(cl, axiom, loca_level_below(A, sbu, confidential)). % 5.29/5.46 % cnf(cl, axiom, loca_level_below(A, unclassified, sbu)). % 5.29/5.46 % cnf(cl, axiom, loca_level_below(A, secret, topsecret)). % 5.29/5.46 % cnf(cl, axiom, loca_level_below(A, sbu, secret)). % 5.29/5.46 % cnf(cl, axiom, loca_level_below(A, unclassified, secret)). % 5.29/5.46 % cnf(cl, axiom, admin_indi_has_polygraph_for_compartment(admin, A, compartmenta)). % 5.29/5.46 % cnf(cl, axiom, admin_indi_has_credit_for_compartment(admin, A, compartmenta)). % 5.29/5.46 % cnf(cl, axiom, loca_level_below(A, confidential, topsecret)). % 5.29/5.46 % cnf(cl, axiom, loca_level_below(A, unclassified, confidential)). % 5.29/5.46 % cnf(cl, axiom, loca_level_below(A, sbu, topsecret)). % 5.29/5.46 % cnf(cl, axiom, loca_level_below(A, unclassified, topsecret)). % 5.29/5.46 % cnf(cl, axiom, admin_indi_has_background(admin, alice, topsecret)). % 5.29/5.46 % cnf(cl, axiom, admin_indi_has_background_for_compartment(admin, A, compartmenta)). % 5.29/5.46 % 92 pred(s) % 5.29/5.46 % 36 func(s) % 5.29/5.46 % 19 sort(s) % 5.29/5.46 % 143 clause(s) % 5.29/5.46 % Instantiating 1 (5046 ms) % 5.29/5.46 % Solving (5047 ms) % 5.29/5.46 % Instantiating 2 (5048 ms) % 5.29/5.46 % Solving (5049 ms) % 5.29/5.46 % % 5.29/5.46 % 1 model found (5052 ms) %------------------------------------------------------------------------------