%------------------------------------------------------------------------------ % File : cvc5-SAT---1.3.4 % Problem : COM002_10 : TPTP v9.2.1. Released v8.2.0. % Transfm : none % Format : tptp:raw % Command : /export/starexec/sandbox/solver/bin/do_cvc5 /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % Computer : n025.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:10:50 AM UTC 2026 % Result : Satisfiable 0.33s 0.58s % Output : Model 0.33s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : COM002_10 : TPTP v9.2.1. Released v8.2.0. % 0.13/0.13 % Command : /export/starexec/sandbox/solver/bin/do_cvc5 /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % 0.16/0.34 % Computer : n025.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 : Mon Jun 1 20:27:46 EDT 2026 % 0.16/0.34 % CPUTime : % 0.20/0.48 %----Disproving TF0_NAR % 0.33/0.50 --- Run --finite-model-find --sort-inference --uf-ss-fair at 60... % 0.33/0.55 --- Run --mbqi at 45... % 0.33/0.58 % SZS status Satisfiable % 0.33/0.58 % SZS output start Model % 0.33/0.58 ( % 0.33/0.58 ; cardinality of $$unsorted is 1 % 0.33/0.58 ; rep: (as @$$unsorted_0 $$unsorted) % 0.33/0.58 ; cardinality of tptp.state is 8 % 0.33/0.58 ; rep: (as @tptp.state_0 tptp.state) % 0.33/0.58 ; rep: (as @tptp.state_1 tptp.state) % 0.33/0.58 ; rep: (as @tptp.state_2 tptp.state) % 0.33/0.58 ; rep: (as @tptp.state_3 tptp.state) % 0.33/0.58 ; rep: (as @tptp.state_4 tptp.state) % 0.33/0.58 ; rep: (as @tptp.state_5 tptp.state) % 0.33/0.58 ; rep: (as @tptp.state_6 tptp.state) % 0.33/0.58 ; rep: (as @tptp.state_7 tptp.state) % 0.33/0.58 ; cardinality of tptp.label is 2 % 0.33/0.58 ; rep: (as @tptp.label_0 tptp.label) % 0.33/0.58 ; rep: (as @tptp.label_1 tptp.label) % 0.33/0.58 ; cardinality of tptp.statement is 7 % 0.33/0.58 ; rep: (as @tptp.statement_0 tptp.statement) % 0.33/0.58 ; rep: (as @tptp.statement_1 tptp.statement) % 0.33/0.58 ; rep: (as @tptp.statement_2 tptp.statement) % 0.33/0.58 ; rep: (as @tptp.statement_3 tptp.statement) % 0.33/0.58 ; rep: (as @tptp.statement_4 tptp.statement) % 0.33/0.58 ; rep: (as @tptp.statement_5 tptp.statement) % 0.33/0.58 ; rep: (as @tptp.statement_6 tptp.statement) % 0.33/0.58 ; cardinality of tptp.register is 2 % 0.33/0.58 ; rep: (as @tptp.register_0 tptp.register) % 0.33/0.58 ; rep: (as @tptp.register_1 tptp.register) % 0.33/0.58 ; cardinality of tptp.number is 6 % 0.33/0.58 ; rep: (as @tptp.number_0 tptp.number) % 0.33/0.58 ; rep: (as @tptp.number_1 tptp.number) % 0.33/0.58 ; rep: (as @tptp.number_2 tptp.number) % 0.33/0.58 ; rep: (as @tptp.number_3 tptp.number) % 0.33/0.58 ; rep: (as @tptp.number_4 tptp.number) % 0.33/0.58 ; rep: (as @tptp.number_5 tptp.number) % 0.33/0.58 ; cardinality of tptp.boolean is 1 % 0.33/0.58 ; rep: (as @tptp.boolean_0 tptp.boolean) % 0.33/0.58 (define-fun tptp.p1 () tptp.state (as @tptp.state_0 tptp.state)) % 0.33/0.58 (define-fun tptp.p2 () tptp.state (as @tptp.state_1 tptp.state)) % 0.33/0.58 (define-fun tptp.p3 () tptp.state (as @tptp.state_2 tptp.state)) % 0.33/0.58 (define-fun tptp.p4 () tptp.state (as @tptp.state_3 tptp.state)) % 0.33/0.58 (define-fun tptp.p5 () tptp.state (as @tptp.state_4 tptp.state)) % 0.33/0.58 (define-fun tptp.p6 () tptp.state (as @tptp.state_5 tptp.state)) % 0.33/0.58 (define-fun tptp.p7 () tptp.state (as @tptp.state_6 tptp.state)) % 0.33/0.58 (define-fun tptp.p8 () tptp.state (as @tptp.state_7 tptp.state)) % 0.33/0.58 (define-fun tptp.n () tptp.number (as @tptp.number_0 tptp.number)) % 0.33/0.58 (define-fun tptp.n0 () tptp.number (as @tptp.number_1 tptp.number)) % 0.33/0.58 (define-fun tptp.n1 () tptp.number (as @tptp.number_2 tptp.number)) % 0.33/0.58 (define-fun tptp.n2 () tptp.number (as @tptp.number_3 tptp.number)) % 0.33/0.58 (define-fun tptp.register_j () tptp.register (as @tptp.register_0 tptp.register)) % 0.33/0.58 (define-fun tptp.register_k () tptp.register (as @tptp.register_1 tptp.register)) % 0.33/0.58 (define-fun tptp.out () tptp.label (as @tptp.label_0 tptp.label)) % 0.33/0.58 (define-fun tptp.loop () tptp.label (as @tptp.label_1 tptp.label)) % 0.33/0.58 (define-fun tptp.equal_function ((_arg_1 tptp.register) (_arg_2 tptp.number)) tptp.boolean (as @tptp.boolean_0 tptp.boolean)) % 0.33/0.58 (define-fun tptp.assign ((_arg_1 tptp.register) (_arg_2 tptp.number)) tptp.statement (ite (= (as @tptp.register_0 tptp.register) _arg_1) (ite (= (as @tptp.number_1 tptp.number) _arg_2) (as @tptp.statement_0 tptp.statement) (as @tptp.statement_5 tptp.statement)) (ite (= (as @tptp.register_1 tptp.register) _arg_1) (ite (= (as @tptp.number_2 tptp.number) _arg_2) (as @tptp.statement_1 tptp.statement) (ite (= (as @tptp.number_4 tptp.number) _arg_2) (as @tptp.statement_4 tptp.statement) (as @tptp.statement_5 tptp.statement))) (as @tptp.statement_5 tptp.statement)))) % 0.33/0.58 (define-fun tptp.goto ((_arg_1 tptp.label)) tptp.statement (ite (= (as @tptp.label_0 tptp.label) _arg_1) (as @tptp.statement_3 tptp.statement) (as @tptp.statement_6 tptp.statement))) % 0.33/0.58 (define-fun tptp.ifthen ((_arg_1 tptp.boolean) (_arg_2 tptp.state)) tptp.statement (as @tptp.statement_2 tptp.statement)) % 0.33/0.58 (define-fun tptp.plus ((_arg_1 tptp.register) (_arg_2 tptp.number)) tptp.number (as @tptp.number_5 tptp.number)) % 0.33/0.58 (define-fun tptp.times ((_arg_1 tptp.number) (_arg_2 tptp.register)) tptp.number (as @tptp.number_4 tptp.number)) % 0.33/0.58 (define-fun tptp.follows ((_arg_1 tptp.state) (_arg_2 tptp.state)) Bool true) % 0.33/0.58 (define-fun tptp.succeeds ((_arg_1 tptp.state) (_arg_2 tptp.state)) Bool true) % 0.33/0.58 (define-fun tptp.labels ((_arg_1 tptp.label) (_arg_2 tptp.state)) Bool true) % 0.33/0.58 (define-fun tptp.has ((_arg_1 tptp.state) (_arg_2 tptp.statement)) Bool true) % 0.33/0.58 ) % 0.33/0.58 % SZS output end Model % 0.33/0.58 % cvc5 exiting %------------------------------------------------------------------------------