%------------------------------------------------------------------------------ % File : cvc5-SAT---1.3.4 % Problem : SWV440+1 : TPTP v9.2.1. Released v4.0.0. % Transfm : none % Format : tptp:raw % Command : /export/starexec/sandbox/solver/bin/do_cvc5 /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % Computer : n007.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8042.1875MB % OS : Linux 3.10.0-693.el7.x86_64 % CPULimit : 300s % WCLimit : 300s % DateTime : Wed Jun 3 09:03:24 AM UTC 2026 % Result : CounterSatisfiable 36.52s 36.85s % Output : Model 36.52s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.13 % Problem : SWV440+1 : TPTP v9.2.1. Released v4.0.0. % 0.00/0.14 % Command : /export/starexec/sandbox/solver/bin/do_cvc5 /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % 0.17/0.35 % Computer : n007.cluster.edu % 0.17/0.35 % Model : x86_64 x86_64 % 0.17/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.17/0.35 % Memory : 8042.1875MB % 0.17/0.35 % OS : Linux 3.10.0-693.el7.x86_64 % 0.17/0.35 % CPULimit : 300 % 0.17/0.35 % WCLimit : 300 % 0.17/0.35 % DateTime : Tue Jun 2 20:17:11 EDT 2026 % 0.17/0.35 % CPUTime : % 0.28/0.53 %----Disproving FOF, CNF % 36.52/36.85 --- Run --decision=internal --simplification=none --no-inst-no-entail --no-cbqi --full-saturate-quant at 12... % 36.52/36.85 --- Run --no-e-matching --full-saturate-quant at 12... % 36.52/36.85 --- Run --no-e-matching --enum-inst-sum --full-saturate-quant at 12... % 36.52/36.85 --- Run --finite-model-find --uf-ss=no-minimal at 54... % 36.52/36.85 % SZS status CounterSatisfiable % 36.52/36.85 % SZS output start Model % 36.52/36.85 ( % 36.52/36.85 ; cardinality of $$unsorted is 3 % 36.52/36.85 ; rep: (as @$$unsorted_0 $$unsorted) % 36.52/36.85 ; rep: (as @$$unsorted_1 $$unsorted) % 36.52/36.85 ; rep: (as @$$unsorted_2 $$unsorted) % 36.52/36.85 (define-fun tptp.unclassified () $$unsorted (as @$$unsorted_0 $$unsorted)) % 36.52/36.85 (define-fun tptp.sbu () $$unsorted (as @$$unsorted_0 $$unsorted)) % 36.52/36.85 (define-fun tptp.loca_level_direct_below (($x1 $$unsorted) ($x2 $$unsorted) ($x3 $$unsorted)) Bool true) % 36.52/36.85 (define-fun tptp.confidential () $$unsorted (as @$$unsorted_0 $$unsorted)) % 36.52/36.85 (define-fun tptp.secret () $$unsorted (as @$$unsorted_0 $$unsorted)) % 36.52/36.85 (define-fun tptp.topsecret () $$unsorted (as @$$unsorted_0 $$unsorted)) % 36.52/36.85 (define-fun tptp.loca_level_below (($x1 $$unsorted) ($x2 $$unsorted) ($x3 $$unsorted)) Bool true) % 36.52/36.85 (define-fun tptp.system () $$unsorted (as @$$unsorted_0 $$unsorted)) % 36.52/36.85 (define-fun tptp.system_compartment_has_sso (($x1 $$unsorted) ($x2 $$unsorted) ($x3 $$unsorted)) Bool true) % 36.52/36.85 (define-fun tptp.admin () $$unsorted (as @$$unsorted_0 $$unsorted)) % 36.52/36.85 (define-fun tptp.admin_compartment_has_sso (($x1 $$unsorted) ($x2 $$unsorted) ($x3 $$unsorted)) Bool true) % 36.52/36.85 (define-fun tptp.system_indi_is_oca (($x1 $$unsorted) ($x2 $$unsorted)) Bool true) % 36.52/36.85 (define-fun tptp.oca_compartment_has_scg (($x1 $$unsorted) ($x2 $$unsorted) ($x3 $$unsorted)) Bool true) % 36.52/36.85 (define-fun tptp.sso_compartment_has_scg (($x1 $$unsorted) ($x2 $$unsorted) ($x3 $$unsorted)) Bool true) % 36.52/36.85 (define-fun tptp.admin_compartment_has_scg (($x1 $$unsorted) ($x2 $$unsorted) ($x3 $$unsorted)) Bool true) % 36.52/36.85 (define-fun tptp.system_file_needs_compartments (($x1 $$unsorted) ($x2 $$unsorted) ($x3 $$unsorted)) Bool (or (and (= (as @$$unsorted_0 $$unsorted) $x1) (= (as @$$unsorted_0 $$unsorted) $x2) (= (as @$$unsorted_0 $$unsorted) $x3)) (and (= (as @$$unsorted_0 $$unsorted) $x1) (= (as @$$unsorted_1 $$unsorted) $x2) (= (as @$$unsorted_0 $$unsorted) $x3)))) % 36.52/36.85 (define-fun tptp.admin_file_has_compartments_h (($x1 $$unsorted) ($x2 $$unsorted) ($x3 $$unsorted) ($x4 $$unsorted)) Bool true) % 36.52/36.85 (define-fun tptp.admin_file_has_compartments (($x1 $$unsorted) ($x2 $$unsorted) ($x3 $$unsorted)) Bool (or (and (= (as @$$unsorted_0 $$unsorted) $x1) (= (as @$$unsorted_1 $$unsorted) $x2) (= (as @$$unsorted_0 $$unsorted) $x3)) (and (= (as @$$unsorted_0 $$unsorted) $x1) (= (as @$$unsorted_0 $$unsorted) $x2) (= (as @$$unsorted_0 $$unsorted) $x3)))) % 36.52/36.85 (define-fun tptp.nil () $$unsorted (as @$$unsorted_0 $$unsorted)) % 36.52/36.85 (define-fun tptp.sso_file_has_compartments (($x1 $$unsorted) ($x2 $$unsorted) ($x3 $$unsorted)) Bool true) % 36.52/36.85 (define-fun tptp.cons (($x1 $$unsorted) ($x2 $$unsorted)) $$unsorted (as @$$unsorted_0 $$unsorted)) % 36.52/36.85 (define-fun tptp.system_file_needs_level (($x1 $$unsorted) ($x2 $$unsorted) ($x3 $$unsorted)) Bool (or (and (= (as @$$unsorted_0 $$unsorted) $x1) (= (as @$$unsorted_0 $$unsorted) $x2) (= (as @$$unsorted_0 $$unsorted) $x3)) (and (= (as @$$unsorted_0 $$unsorted) $x1) (= (as @$$unsorted_1 $$unsorted) $x2) (= (as @$$unsorted_0 $$unsorted) $x3)))) % 36.52/36.85 (define-fun tptp.admin_file_has_level_h (($x1 $$unsorted) ($x2 $$unsorted) ($x3 $$unsorted) ($x4 $$unsorted)) Bool true) % 36.52/36.85 (define-fun tptp.admin_file_has_level (($x1 $$unsorted) ($x2 $$unsorted) ($x3 $$unsorted)) Bool (or (and (= (as @$$unsorted_0 $$unsorted) $x1) (= (as @$$unsorted_1 $$unsorted) $x2) (= (as @$$unsorted_0 $$unsorted) $x3)) (and (= (as @$$unsorted_0 $$unsorted) $x1) (= (as @$$unsorted_0 $$unsorted) $x2) (= (as @$$unsorted_0 $$unsorted) $x3)))) % 36.52/36.85 (define-fun tptp.sso_file_has_level (($x1 $$unsorted) ($x2 $$unsorted) ($x3 $$unsorted) ($x4 $$unsorted)) Bool true) % 36.52/36.85 (define-fun tptp.system_file_needs_citizenship (($x1 $$unsorted) ($x2 $$unsorted) ($x3 $$unsorted)) Bool true) % 36.52/36.85 (define-fun tptp.admin_file_has_citizenship_h (($x1 $$unsorted) ($x2 $$unsorted) ($x3 $$unsorted) ($x4 $$unsorted)) Bool true) % 36.52/36.85 (define-fun tptp.admin_file_has_citizenship (($x1 $$unsorted) ($x2 $$unsorted) ($x3 $$unsorted)) Bool true) % 36.52/36.85 (define-fun tptp.sso_file_has_citizenship (($x1 $$unsorted) ($x2 $$unsorted) ($x3 $$unsorted) ($x4 $$unsorted)) Bool true) % 36.52/36.85 (define-fun tptp.system_indi_is_polygraph_admin (($x1 $$unsorted) ($x2 $$unsorted)) Bool true) % 36.52/36.85 (define-fun tptp.polygraph_admin_indi_has_polygraph (($x1 $$unsorted) ($x2 $$unsorted)) Bool true) % 36.52/36.85 (define-fun tptp.admin_indi_has_polygraph (($x1 $$unsorted) ($x2 $$unsorted)) Bool true) % 36.52/36.85 (define-fun tptp.system_indi_is_credit_admin (($x1 $$unsorted) ($x2 $$unsorted)) Bool true) % 36.52/36.85 (define-fun tptp.credit_admin_indi_has_credit (($x1 $$unsorted) ($x2 $$unsorted)) Bool true) % 36.52/36.85 (define-fun tptp.admin_indi_has_credit (($x1 $$unsorted) ($x2 $$unsorted)) Bool true) % 36.52/36.85 (define-fun tptp.admin_indi_has_background (($x1 $$unsorted) ($x2 $$unsorted) ($x3 $$unsorted)) Bool true) % 36.52/36.85 (define-fun tptp.system_indi_is_background_admin (($x1 $$unsorted) ($x2 $$unsorted)) Bool true) % 36.52/36.85 (define-fun tptp.background_admin_indi_has_background (($x1 $$unsorted) ($x2 $$unsorted) ($x3 $$unsorted)) Bool true) % 36.52/36.85 (define-fun tptp.system_indi_is_hr_admin (($x1 $$unsorted) ($x2 $$unsorted)) Bool true) % 36.52/36.85 (define-fun tptp.hr_admin_indi_has_employment (($x1 $$unsorted) ($x2 $$unsorted)) Bool true) % 36.52/36.85 (define-fun tptp.admin_indi_has_employment (($x1 $$unsorted) ($x2 $$unsorted)) Bool true) % 36.52/36.85 (define-fun tptp.anycountry () $$unsorted (as @$$unsorted_0 $$unsorted)) % 36.52/36.85 (define-fun tptp.admin_indi_has_citizenship (($x1 $$unsorted) ($x2 $$unsorted) ($x3 $$unsorted)) Bool true) % 36.52/36.85 (define-fun tptp.system_indi_has_citizenship (($x1 $$unsorted) ($x2 $$unsorted) ($x3 $$unsorted)) Bool true) % 36.52/36.85 (define-fun tptp.admin_indi_has_level (($x1 $$unsorted) ($x2 $$unsorted) ($x3 $$unsorted)) Bool true) % 36.52/36.85 (define-fun tptp.system_indi_needs_level (($x1 $$unsorted) ($x2 $$unsorted) ($x3 $$unsorted)) Bool true) % 36.52/36.85 (define-fun tptp.usa () $$unsorted (as @$$unsorted_0 $$unsorted)) % 36.52/36.85 (define-fun tptp.system_indi_is_level_admin (($x1 $$unsorted) ($x2 $$unsorted)) Bool true) % 36.52/36.85 (define-fun tptp.level_admin_indi_has_level (($x1 $$unsorted) ($x2 $$unsorted) ($x3 $$unsorted)) Bool true) % 36.52/36.85 (define-fun tptp.admin_indi_has_compartments (($x1 $$unsorted) ($x2 $$unsorted) ($x3 $$unsorted)) Bool true) % 36.52/36.85 (define-fun tptp.system_indi_needs_compartment (($x1 $$unsorted) ($x2 $$unsorted) ($x3 $$unsorted)) Bool true) % 36.52/36.85 (define-fun tptp.admin_indi_has_polygraph_for_compartment (($x1 $$unsorted) ($x2 $$unsorted) ($x3 $$unsorted)) Bool true) % 36.52/36.85 (define-fun tptp.admin_indi_has_credit_for_compartment (($x1 $$unsorted) ($x2 $$unsorted) ($x3 $$unsorted)) Bool true) % 36.52/36.85 (define-fun tptp.sso_indi_has_compartment (($x1 $$unsorted) ($x2 $$unsorted) ($x3 $$unsorted)) Bool true) % 36.52/36.85 (define-fun tptp.admin_indi_has_background_for_compartment (($x1 $$unsorted) ($x2 $$unsorted) ($x3 $$unsorted)) Bool true) % 36.52/36.85 (define-fun tptp.admin_indi_has_level_for_compartment (($x1 $$unsorted) ($x2 $$unsorted) ($x3 $$unsorted)) Bool true) % 36.52/36.85 (define-fun tptp.oca_compartment_is_compartment (($x1 $$unsorted) ($x2 $$unsorted) ($x3 $$unsorted) ($x4 $$unsorted) ($x5 $$unsorted) ($x6 $$unsorted)) Bool true) % 36.52/36.85 (define-fun tptp.yes () $$unsorted (as @$$unsorted_0 $$unsorted)) % 36.52/36.85 (define-fun tptp.no () $$unsorted (as @$$unsorted_0 $$unsorted)) % 36.52/36.85 (define-fun tptp.admin_indi_has_compartments_for_file (($x1 $$unsorted) ($x2 $$unsorted) ($x3 $$unsorted)) Bool true) % 36.52/36.85 (define-fun tptp.admin_indi_has_level_for_file (($x1 $$unsorted) ($x2 $$unsorted) ($x3 $$unsorted)) Bool true) % 36.52/36.85 (define-fun tptp.state_file_has_owner (($x1 $$unsorted) ($x2 $$unsorted)) Bool (or (and (= (as @$$unsorted_0 $$unsorted) $x1) (= (as @$$unsorted_0 $$unsorted) $x2)) (and (= (as @$$unsorted_1 $$unsorted) $x1) (= (as @$$unsorted_1 $$unsorted) $x2)))) % 36.52/36.85 (define-fun tptp.owner_indi_has_need_to_know (($x1 $$unsorted) ($x2 $$unsorted) ($x3 $$unsorted)) Bool (or (and (= (as @$$unsorted_0 $$unsorted) $x1) (= (as @$$unsorted_0 $$unsorted) $x2) (= (as @$$unsorted_0 $$unsorted) $x3)) (and (= (as @$$unsorted_0 $$unsorted) $x1) (= (as @$$unsorted_0 $$unsorted) $x2) (= (as @$$unsorted_1 $$unsorted) $x3)) (and (= (as @$$unsorted_1 $$unsorted) $x1) (= (as @$$unsorted_2 $$unsorted) $x2) (= (as @$$unsorted_1 $$unsorted) $x3)))) % 36.52/36.85 (define-fun tptp.admin_indi_has_need_to_know_for_file (($x1 $$unsorted) ($x2 $$unsorted) ($x3 $$unsorted)) Bool (or (and (= (as @$$unsorted_0 $$unsorted) $x1) (= (as @$$unsorted_0 $$unsorted) $x2) (= (as @$$unsorted_0 $$unsorted) $x3)) (and (= (as @$$unsorted_0 $$unsorted) $x1) (= (as @$$unsorted_2 $$unsorted) $x2) (= (as @$$unsorted_1 $$unsorted) $x3)))) % 36.52/36.85 (define-fun tptp.admin_indi_has_citizenship_for_file (($x1 $$unsorted) ($x2 $$unsorted) ($x3 $$unsorted)) Bool true) % 36.52/36.85 (define-fun tptp.state_file_is_not_working_paper (($x1 $$unsorted)) Bool true) % 36.52/36.85 (define-fun tptp.read () $$unsorted (as @$$unsorted_0 $$unsorted)) % 36.52/36.85 (define-fun tptp.admin_indi_may_file (($x1 $$unsorted) ($x2 $$unsorted) ($x3 $$unsorted) ($x4 $$unsorted)) Bool (or (and (= (as @$$unsorted_0 $$unsorted) $x1) (= (as @$$unsorted_0 $$unsorted) $x2) (= (as @$$unsorted_0 $$unsorted) $x3) (= (as @$$unsorted_0 $$unsorted) $x4)) (and (= (as @$$unsorted_0 $$unsorted) $x1) (= (as @$$unsorted_2 $$unsorted) $x2) (= (as @$$unsorted_1 $$unsorted) $x3) (= (as @$$unsorted_0 $$unsorted) $x4)))) % 36.52/36.85 (define-fun tptp.system_indi_is_counterintelligence (($x1 $$unsorted) ($x2 $$unsorted) ($x3 $$unsorted)) Bool (and (= (as @$$unsorted_0 $$unsorted) $x1) (= (as @$$unsorted_0 $$unsorted) $x2) (= (as @$$unsorted_0 $$unsorted) $x3))) % 36.52/36.85 (define-fun tptp.oca () $$unsorted (as @$$unsorted_0 $$unsorted)) % 36.52/36.85 (define-fun tptp.compartmentb () $$unsorted (as @$$unsorted_0 $$unsorted)) % 36.52/36.85 (define-fun tptp.compartmenta () $$unsorted (as @$$unsorted_0 $$unsorted)) % 36.52/36.85 (define-fun tptp.sso_compartmentb () $$unsorted (as @$$unsorted_0 $$unsorted)) % 36.52/36.85 (define-fun tptp.scg_compartmentb () $$unsorted (as @$$unsorted_0 $$unsorted)) % 36.52/36.85 (define-fun tptp.sso_compartmenta () $$unsorted (as @$$unsorted_0 $$unsorted)) % 36.52/36.85 (define-fun tptp.scg_compartmenta () $$unsorted (as @$$unsorted_0 $$unsorted)) % 36.52/36.85 (define-fun tptp.secretfile () $$unsorted (as @$$unsorted_0 $$unsorted)) % 36.52/36.85 (define-fun tptp.owner_secretfile () $$unsorted (as @$$unsorted_0 $$unsorted)) % 36.52/36.85 (define-fun tptp.not_secretfile () $$unsorted (as @$$unsorted_1 $$unsorted)) % 36.52/36.85 (define-fun tptp.owner_not_secretfile () $$unsorted (as @$$unsorted_1 $$unsorted)) % 36.52/36.85 (define-fun tptp.polygraph_admin () $$unsorted (as @$$unsorted_0 $$unsorted)) % 36.52/36.85 (define-fun tptp.credit_admin () $$unsorted (as @$$unsorted_0 $$unsorted)) % 36.52/36.85 (define-fun tptp.background_admin () $$unsorted (as @$$unsorted_0 $$unsorted)) % 36.52/36.85 (define-fun tptp.hr_admin () $$unsorted (as @$$unsorted_0 $$unsorted)) % 36.52/36.85 (define-fun tptp.level_admin () $$unsorted (as @$$unsorted_0 $$unsorted)) % 36.52/36.85 (define-fun tptp.alice () $$unsorted (as @$$unsorted_0 $$unsorted)) % 36.52/36.85 (define-fun tptp.babu () $$unsorted (as @$$unsorted_2 $$unsorted)) % 36.52/36.85 (define-fun tptp.india () $$unsorted (as @$$unsorted_0 $$unsorted)) % 36.52/36.85 (define-fun tptp.ci () $$unsorted (as @$$unsorted_0 $$unsorted)) % 36.52/36.85 ) % 36.52/36.85 % SZS output end Model % 36.52/36.85 % cvc5 exiting %------------------------------------------------------------------------------