%------------------------------------------------------------------------------ % File : cvc5-SAT---1.3.4 % Problem : NUM923_10 : TPTP v9.2.1. Released v8.2.0. % Transfm : none % Format : tptp:raw % Command : /export/starexec/sandbox2/solver/bin/do_cvc5 /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % Computer : n011.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 08:42:37 AM UTC 2026 % Result : Satisfiable 135.65s 136.02s % Output : Model 135.65s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.11/0.12 % Problem : NUM923_10 : TPTP v9.2.1. Released v8.2.0. % 0.11/0.13 % Command : /export/starexec/sandbox2/solver/bin/do_cvc5 /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % 0.16/0.34 % Computer : n011.cluster.edu % 0.16/0.34 % Model : x86_64 x86_64 % 0.16/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.16/0.34 % Memory : 8042.1875MB % 0.16/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.16/0.34 % CPULimit : 300 % 0.16/0.34 % WCLimit : 300 % 0.16/0.34 % DateTime : Tue Jun 2 12:31:35 EDT 2026 % 0.16/0.34 % CPUTime : % 0.26/0.51 %----Disproving TF0_NAR % 0.26/0.52 --- Run --finite-model-find --sort-inference --uf-ss-fair at 60... % 0.36/0.57 --- Run --mbqi at 45... % 45.41/45.68 --- Run --mbqi --mbqi-enum --mbqi-enum-choice-grammar --mbqi-enum-global-syms-grammar --no-cegqi --no-sygus-inst at 45... % 90.55/90.82 --- Run --full-saturate-quant at 45... % 135.65/135.97 --- Run --finite-model-find --fmf-bound --macros-quant at 60... % 135.65/136.02 % SZS status Satisfiable % 135.65/136.02 % SZS output start Model % 135.65/136.02 ( % 135.65/136.02 ; cardinality of $$unsorted is 1 % 135.65/136.02 ; rep: (as @$$unsorted_0 $$unsorted) % 135.65/136.02 ; cardinality of tptp.bool is 1 % 135.65/136.02 ; rep: (as @tptp.bool_0 tptp.bool) % 135.65/136.02 ; cardinality of tptp.int is 1 % 135.65/136.02 ; rep: (as @tptp.int_0 tptp.int) % 135.65/136.02 ; cardinality of tptp.fun_Pr974702441t_bool is 1 % 135.65/136.02 ; rep: (as @tptp.fun_Pr974702441t_bool_0 tptp.fun_Pr974702441t_bool) % 135.65/136.02 ; cardinality of tptp.product_prod_int_int is 1 % 135.65/136.02 ; rep: (as @tptp.product_prod_int_int_0 tptp.product_prod_int_int) % 135.65/136.02 (define-fun tptp.minus_minus_int (($x1 tptp.int) ($x2 tptp.int)) tptp.int (as @tptp.int_0 tptp.int)) % 135.65/136.02 (define-fun tptp.plus_plus_int (($x1 tptp.int) ($x2 tptp.int)) tptp.int (as @tptp.int_0 tptp.int)) % 135.65/136.02 (define-fun tptp.times_times_int (($x1 tptp.int) ($x2 tptp.int)) tptp.int (as @tptp.int_0 tptp.int)) % 135.65/136.02 (define-fun tptp.ord_less_eq_int (($x1 tptp.int) ($x2 tptp.int)) tptp.bool (as @tptp.bool_0 tptp.bool)) % 135.65/136.02 (define-fun tptp.product_Pair_int_int (($x1 tptp.int) ($x2 tptp.int)) tptp.product_prod_int_int (as @tptp.product_prod_int_int_0 tptp.product_prod_int_int)) % 135.65/136.02 (define-fun tptp.produc262399358t_bool (($x1 tptp.fun_Pr974702441t_bool) ($x2 tptp.int) ($x3 tptp.int)) tptp.bool (as @tptp.bool_0 tptp.bool)) % 135.65/136.02 (define-fun tptp.twoSqu1431725154sum2sq (($x1 tptp.int)) tptp.bool (as @tptp.bool_0 tptp.bool)) % 135.65/136.02 (define-fun tptp.twoSqu1319573848sum2sq (($x1 tptp.product_prod_int_int)) tptp.int (as @tptp.int_0 tptp.int)) % 135.65/136.02 (define-fun tptp.hAPP_P603027463t_bool (($x1 tptp.fun_Pr974702441t_bool) ($x2 tptp.product_prod_int_int)) tptp.bool (as @tptp.bool_0 tptp.bool)) % 135.65/136.02 (define-fun tptp.hBOOL (($x1 tptp.bool)) Bool true) % 135.65/136.02 (define-fun tptp.a () tptp.int (as @tptp.int_0 tptp.int)) % 135.65/136.02 (define-fun tptp.b () tptp.int (as @tptp.int_0 tptp.int)) % 135.65/136.02 (define-fun tptp.p () tptp.int (as @tptp.int_0 tptp.int)) % 135.65/136.02 (define-fun tptp.q () tptp.int (as @tptp.int_0 tptp.int)) % 135.65/136.02 ) % 135.65/136.02 % SZS output end Model % 135.65/136.02 % cvc5 exiting %------------------------------------------------------------------------------