%------------------------------------------------------------------------------ % File : cvc5-SAT---1.3.4 % Problem : ITP341_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 : n013.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:27:56 AM UTC 2026 % Result : Satisfiable 141.49s 141.77s % Output : Model 141.49s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : ITP341_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.19/0.35 % Computer : n013.cluster.edu % 0.19/0.35 % Model : x86_64 x86_64 % 0.19/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.19/0.35 % Memory : 8042.1875MB % 0.19/0.35 % OS : Linux 3.10.0-693.el7.x86_64 % 0.19/0.35 % CPULimit : 300 % 0.19/0.35 % WCLimit : 300 % 0.19/0.35 % DateTime : Tue Jun 2 05:01:45 EDT 2026 % 0.19/0.35 % CPUTime : % 0.38/0.61 %----Disproving TF0_NAR % 0.38/0.63 --- Run --finite-model-find --sort-inference --uf-ss-fair at 60... % 0.47/0.68 --- Run --mbqi at 45... % 45.85/46.03 --- Run --mbqi --mbqi-enum --mbqi-enum-choice-grammar --mbqi-enum-global-syms-grammar --no-cegqi --no-sygus-inst at 45... % 91.09/91.37 --- Run --full-saturate-quant at 45... % 136.40/136.69 --- Run --finite-model-find --fmf-bound --macros-quant at 60... % 141.49/141.77 % SZS status Satisfiable % 141.49/141.77 % SZS output start Model % 141.49/141.77 ( % 141.49/141.77 ; cardinality of $$unsorted is 1 % 141.49/141.77 ; rep: (as @$$unsorted_0 $$unsorted) % 141.49/141.77 ; cardinality of |tptp.'A_n_vec_n_vec_set_set$'| is 1 % 141.49/141.77 ; rep: (as |@_tptp.'A_n_vec_n_vec_set_set$'__0| |tptp.'A_n_vec_n_vec_set_set$'|) % 141.49/141.77 ; cardinality of |tptp.'A_set_set$'| is 1 % 141.49/141.77 ; rep: (as |@_tptp.'A_set_set$'__0| |tptp.'A_set_set$'|) % 141.49/141.77 ; cardinality of |tptp.'A_n_vec_set$'| is 1 % 141.49/141.77 ; rep: (as |@_tptp.'A_n_vec_set$'__0| |tptp.'A_n_vec_set$'|) % 141.49/141.77 ; cardinality of |tptp.'A_n_vec_n_vec_bool_fun$'| is 3 % 141.49/141.77 ; rep: (as |@_tptp.'A_n_vec_n_vec_bool_fun$'__0| |tptp.'A_n_vec_n_vec_bool_fun$'|) % 141.49/141.77 ; rep: (as |@_tptp.'A_n_vec_n_vec_bool_fun$'__1| |tptp.'A_n_vec_n_vec_bool_fun$'|) % 141.49/141.77 ; rep: (as |@_tptp.'A_n_vec_n_vec_bool_fun$'__2| |tptp.'A_n_vec_n_vec_bool_fun$'|) % 141.49/141.77 ; cardinality of |tptp.'A_n_vec_n_vec$'| is 2 % 141.49/141.77 ; rep: (as |@_tptp.'A_n_vec_n_vec$'__0| |tptp.'A_n_vec_n_vec$'|) % 141.49/141.77 ; rep: (as |@_tptp.'A_n_vec_n_vec$'__1| |tptp.'A_n_vec_n_vec$'|) % 141.49/141.77 ; cardinality of |tptp.'Nat$'| is 1 % 141.49/141.77 ; rep: (as |@_tptp.'Nat$'__0| |tptp.'Nat$'|) % 141.49/141.77 ; cardinality of |tptp.'A_n_vec_n_vec_set$'| is 3 % 141.49/141.77 ; rep: (as |@_tptp.'A_n_vec_n_vec_set$'__0| |tptp.'A_n_vec_n_vec_set$'|) % 141.49/141.77 ; rep: (as |@_tptp.'A_n_vec_n_vec_set$'__1| |tptp.'A_n_vec_n_vec_set$'|) % 141.49/141.77 ; rep: (as |@_tptp.'A_n_vec_n_vec_set$'__2| |tptp.'A_n_vec_n_vec_set$'|) % 141.49/141.77 ; cardinality of |tptp.'N$'| is 1 % 141.49/141.77 ; rep: (as |@_tptp.'N$'__0| |tptp.'N$'|) % 141.49/141.77 ; cardinality of |tptp.'Num$'| is 1 % 141.49/141.77 ; rep: (as |@_tptp.'Num$'__0| |tptp.'Num$'|) % 141.49/141.77 ; cardinality of |tptp.'Num_set$'| is 1 % 141.49/141.77 ; rep: (as |@_tptp.'Num_set$'__0| |tptp.'Num_set$'|) % 141.49/141.77 ; cardinality of tptp.tlbool is 2 % 141.49/141.77 ; rep: (as @tptp.tlbool_0 tptp.tlbool) % 141.49/141.77 ; rep: (as @tptp.tlbool_1 tptp.tlbool) % 141.49/141.77 ; cardinality of |tptp.'A_bool_fun$'| is 1 % 141.49/141.77 ; rep: (as |@_tptp.'A_bool_fun$'__0| |tptp.'A_bool_fun$'|) % 141.49/141.77 ; cardinality of |tptp.'A_set$'| is 1 % 141.49/141.77 ; rep: (as |@_tptp.'A_set$'__0| |tptp.'A_set$'|) % 141.49/141.77 ; cardinality of |tptp.'A_n_vec_set_set$'| is 1 % 141.49/141.77 ; rep: (as |@_tptp.'A_n_vec_set_set$'__0| |tptp.'A_n_vec_set_set$'|) % 141.49/141.77 ; cardinality of |tptp.'A$'| is 2 % 141.49/141.77 ; rep: (as |@_tptp.'A$'__0| |tptp.'A$'|) % 141.49/141.77 ; rep: (as |@_tptp.'A$'__1| |tptp.'A$'|) % 141.49/141.77 ; cardinality of |tptp.'A_n_vec$'| is 2 % 141.49/141.77 ; rep: (as |@_tptp.'A_n_vec$'__0| |tptp.'A_n_vec$'|) % 141.49/141.77 ; rep: (as |@_tptp.'A_n_vec$'__1| |tptp.'A_n_vec$'|) % 141.49/141.77 ; cardinality of |tptp.'A_a_fun$'| is 2 % 141.49/141.77 ; rep: (as |@_tptp.'A_a_fun$'__0| |tptp.'A_a_fun$'|) % 141.49/141.77 ; rep: (as |@_tptp.'A_a_fun$'__1| |tptp.'A_a_fun$'|) % 141.49/141.77 ; cardinality of |tptp.'A_n_vec_n_vec_n_vec$'| is 2 % 141.49/141.77 ; rep: (as |@_tptp.'A_n_vec_n_vec_n_vec$'__0| |tptp.'A_n_vec_n_vec_n_vec$'|) % 141.49/141.77 ; rep: (as |@_tptp.'A_n_vec_n_vec_n_vec$'__1| |tptp.'A_n_vec_n_vec_n_vec$'|) % 141.49/141.77 ; cardinality of |tptp.'A_n_vec_bool_fun$'| is 1 % 141.49/141.77 ; rep: (as |@_tptp.'A_n_vec_bool_fun$'__0| |tptp.'A_n_vec_bool_fun$'|) % 141.49/141.77 ; cardinality of |tptp.'N_a_n_vec_n_vec_fun$'| is 2 % 141.49/141.77 ; rep: (as |@_tptp.'N_a_n_vec_n_vec_fun$'__0| |tptp.'N_a_n_vec_n_vec_fun$'|) % 141.49/141.77 ; rep: (as |@_tptp.'N_a_n_vec_n_vec_fun$'__1| |tptp.'N_a_n_vec_n_vec_fun$'|) % 141.49/141.77 (define-fun |tptp.'numeral$a'| (($x1 |tptp.'Num$'|)) |tptp.'A_n_vec_n_vec$'| (as |@_tptp.'A_n_vec_n_vec$'__0| |tptp.'A_n_vec_n_vec$'|)) % 141.49/141.77 (define-fun |tptp.'uu$'| (($x1 |tptp.'A_set$'|)) |tptp.'A_bool_fun$'| (as |@_tptp.'A_bool_fun$'__0| |tptp.'A_bool_fun$'|)) % 141.49/141.77 (define-fun |tptp.'dbl_inc$a'| ((BOUND_VARIABLE_5076 |tptp.'A_n_vec$'|)) |tptp.'A_n_vec$'| (ite (= (as |@_tptp.'A_n_vec$'__1| |tptp.'A_n_vec$'|) (ite (and (= BOUND_VARIABLE_5076 (as |@_tptp.'A_n_vec$'__1| |tptp.'A_n_vec$'|)) (= BOUND_VARIABLE_5076 (as |@_tptp.'A_n_vec$'__0| |tptp.'A_n_vec$'|))) (as |@_tptp.'A_n_vec$'__0| |tptp.'A_n_vec$'|) (ite (and (= BOUND_VARIABLE_5076 (as |@_tptp.'A_n_vec$'__0| |tptp.'A_n_vec$'|)) (= BOUND_VARIABLE_5076 (as |@_tptp.'A_n_vec$'__1| |tptp.'A_n_vec$'|))) (as |@_tptp.'A_n_vec$'__0| |tptp.'A_n_vec$'|) (as |@_tptp.'A_n_vec$'__1| |tptp.'A_n_vec$'|)))) (as |@_tptp.'A_n_vec$'__0| |tptp.'A_n_vec$'|) (as |@_tptp.'A_n_vec$'__1| |tptp.'A_n_vec$'|))) % 141.49/141.77 (define-fun |tptp.'member$f'| (($x1 |tptp.'A_n_vec_set$'|) ($x2 |tptp.'A_n_vec_set_set$'|)) Bool false) % 141.49/141.77 (define-fun |tptp.'mat$'| (($x1 |tptp.'A$'|)) |tptp.'A_n_vec_n_vec$'| (ite (= (as |@_tptp.'A$'__1| |tptp.'A$'|) $x1) (as |@_tptp.'A_n_vec_n_vec$'__0| |tptp.'A_n_vec_n_vec$'|) (as |@_tptp.'A_n_vec_n_vec$'__1| |tptp.'A_n_vec_n_vec$'|))) % 141.49/141.77 (define-fun |tptp.'dbl_inc$'| ((BOUND_VARIABLE_5090 |tptp.'A_n_vec_n_vec$'|)) |tptp.'A_n_vec_n_vec$'| (ite (= (as |@_tptp.'A_n_vec_n_vec$'__1| |tptp.'A_n_vec_n_vec$'|) (ite (= BOUND_VARIABLE_5090 (as |@_tptp.'A_n_vec_n_vec$'__1| |tptp.'A_n_vec_n_vec$'|)) (as |@_tptp.'A_n_vec_n_vec$'__0| |tptp.'A_n_vec_n_vec$'|) (ite (= BOUND_VARIABLE_5090 (as |@_tptp.'A_n_vec_n_vec$'__0| |tptp.'A_n_vec_n_vec$'|)) (as |@_tptp.'A_n_vec_n_vec$'__0| |tptp.'A_n_vec_n_vec$'|) (as |@_tptp.'A_n_vec_n_vec$'__1| |tptp.'A_n_vec_n_vec$'|)))) (as |@_tptp.'A_n_vec_n_vec$'__0| |tptp.'A_n_vec_n_vec$'|) (as |@_tptp.'A_n_vec_n_vec$'__1| |tptp.'A_n_vec_n_vec$'|))) % 141.49/141.77 (define-fun |tptp.'uub$'| (($x1 |tptp.'A_n_vec_set$'|)) |tptp.'A_n_vec_bool_fun$'| (as |@_tptp.'A_n_vec_bool_fun$'__0| |tptp.'A_n_vec_bool_fun$'|)) % 141.49/141.77 (define-fun |tptp.'invertible$'| () |tptp.'A_n_vec_n_vec_bool_fun$'| (as |@_tptp.'A_n_vec_n_vec_bool_fun$'__0| |tptp.'A_n_vec_n_vec_bool_fun$'|)) % 141.49/141.77 (define-fun |tptp.'matrix_vector_mult$'| ((BOUND_VARIABLE_4618 |tptp.'A_n_vec_n_vec$'|) (BOUND_VARIABLE_4619 |tptp.'A_n_vec$'|)) |tptp.'A_n_vec$'| (ite (and (= BOUND_VARIABLE_4619 (as |@_tptp.'A_n_vec$'__0| |tptp.'A_n_vec$'|)) (= (as |@_tptp.'A_n_vec_n_vec$'__1| |tptp.'A_n_vec_n_vec$'|) (ite (= BOUND_VARIABLE_4618 (as |@_tptp.'A_n_vec_n_vec$'__0| |tptp.'A_n_vec_n_vec$'|)) (as |@_tptp.'A_n_vec_n_vec$'__0| |tptp.'A_n_vec_n_vec$'|) (as |@_tptp.'A_n_vec_n_vec$'__1| |tptp.'A_n_vec_n_vec$'|)))) (as |@_tptp.'A_n_vec$'__0| |tptp.'A_n_vec$'|) (as |@_tptp.'A_n_vec$'__1| |tptp.'A_n_vec$'|))) % 141.49/141.77 (define-fun |tptp.'times$d'| (($x1 |tptp.'A_n_vec_set$'|) ($x2 |tptp.'A_n_vec_set$'|)) |tptp.'A_n_vec_set$'| (as |@_tptp.'A_n_vec_set$'__0| |tptp.'A_n_vec_set$'|)) % 141.49/141.77 (define-fun |tptp.'vector_matrix_mult$a'| (($x1 |tptp.'A_n_vec$'|) ($x2 |tptp.'A_n_vec_n_vec$'|)) |tptp.'A_n_vec$'| (ite (and (= (as |@_tptp.'A_n_vec$'__0| |tptp.'A_n_vec$'|) $x1) (= (as |@_tptp.'A_n_vec_n_vec$'__1| |tptp.'A_n_vec_n_vec$'|) $x2)) (as |@_tptp.'A_n_vec$'__0| |tptp.'A_n_vec$'|) (as |@_tptp.'A_n_vec$'__1| |tptp.'A_n_vec$'|))) % 141.49/141.77 (define-fun |tptp.'axis$'| (($x1 |tptp.'N$'|) ($x2 |tptp.'A_n_vec$'|)) |tptp.'A_n_vec_n_vec$'| (ite (and (= (as |@_tptp.'N$'__0| |tptp.'N$'|) $x1) (= (as |@_tptp.'A_n_vec$'__1| |tptp.'A_n_vec$'|) $x2)) (as |@_tptp.'A_n_vec_n_vec$'__0| |tptp.'A_n_vec_n_vec$'|) (as |@_tptp.'A_n_vec_n_vec$'__1| |tptp.'A_n_vec_n_vec$'|))) % 141.49/141.77 (define-fun |tptp.'columnvector$'| ((BOUND_VARIABLE_36948 |tptp.'A_n_vec$'|)) |tptp.'A_n_vec_n_vec$'| (as |@_tptp.'A_n_vec_n_vec$'__0| |tptp.'A_n_vec_n_vec$'|)) % 141.49/141.77 (define-fun |tptp.'gauss_Jordan$'| (($x1 |tptp.'A_n_vec_n_vec$'|)) |tptp.'A_n_vec_n_vec$'| (ite (= (as |@_tptp.'A_n_vec_n_vec$'__0| |tptp.'A_n_vec_n_vec$'|) $x1) (as |@_tptp.'A_n_vec_n_vec$'__0| |tptp.'A_n_vec_n_vec$'|) (as |@_tptp.'A_n_vec_n_vec$'__1| |tptp.'A_n_vec_n_vec$'|))) % 141.49/141.77 (define-fun |tptp.'plus$g'| (($x1 |tptp.'A_n_vec_n_vec$'|) ($x2 |tptp.'A_n_vec_n_vec$'|)) |tptp.'A_n_vec_n_vec$'| (ite (and (= (as |@_tptp.'A_n_vec_n_vec$'__1| |tptp.'A_n_vec_n_vec$'|) $x1) (= (as |@_tptp.'A_n_vec_n_vec$'__1| |tptp.'A_n_vec_n_vec$'|) $x2)) (as |@_tptp.'A_n_vec_n_vec$'__0| |tptp.'A_n_vec_n_vec$'|) (ite (and (= (as |@_tptp.'A_n_vec_n_vec$'__0| |tptp.'A_n_vec_n_vec$'|) $x1) (= (as |@_tptp.'A_n_vec_n_vec$'__0| |tptp.'A_n_vec_n_vec$'|) $x2)) (as |@_tptp.'A_n_vec_n_vec$'__0| |tptp.'A_n_vec_n_vec$'|) (as |@_tptp.'A_n_vec_n_vec$'__1| |tptp.'A_n_vec_n_vec$'|)))) % 141.49/141.77 (define-fun |tptp.'member$'| ((BOUND_VARIABLE_4296 |tptp.'A_n_vec_n_vec$'|) (BOUND_VARIABLE_4297 |tptp.'A_n_vec_n_vec_set$'|)) Bool (or (and (= (as |@_tptp.'A_n_vec_n_vec_bool_fun$'__0| |tptp.'A_n_vec_n_vec_bool_fun$'|) (ite (= BOUND_VARIABLE_4297 (as |@_tptp.'A_n_vec_n_vec_set$'__0| |tptp.'A_n_vec_n_vec_set$'|)) (as |@_tptp.'A_n_vec_n_vec_bool_fun$'__0| |tptp.'A_n_vec_n_vec_bool_fun$'|) (ite (= BOUND_VARIABLE_4297 (as |@_tptp.'A_n_vec_n_vec_set$'__1| |tptp.'A_n_vec_n_vec_set$'|)) (as |@_tptp.'A_n_vec_n_vec_bool_fun$'__1| |tptp.'A_n_vec_n_vec_bool_fun$'|) (as |@_tptp.'A_n_vec_n_vec_bool_fun$'__2| |tptp.'A_n_vec_n_vec_bool_fun$'|)))) (= BOUND_VARIABLE_4296 (as |@_tptp.'A_n_vec_n_vec$'__1| |tptp.'A_n_vec_n_vec$'|))) (and (= (as |@_tptp.'A_n_vec_n_vec_bool_fun$'__2| |tptp.'A_n_vec_n_vec_bool_fun$'|) (ite (= BOUND_VARIABLE_4297 (as |@_tptp.'A_n_vec_n_vec_set$'__0| |tptp.'A_n_vec_n_vec_set$'|)) (as |@_tptp.'A_n_vec_n_vec_bool_fun$'__0| |tptp.'A_n_vec_n_vec_bool_fun$'|) (ite (= BOUND_VARIABLE_4297 (as |@_tptp.'A_n_vec_n_vec_set$'__1| |tptp.'A_n_vec_n_vec_set$'|)) (as |@_tptp.'A_n_vec_n_vec_bool_fun$'__1| |tptp.'A_n_vec_n_vec_bool_fun$'|) (as |@_tptp.'A_n_vec_n_vec_bool_fun$'__2| |tptp.'A_n_vec_n_vec_bool_fun$'|)))) (= BOUND_VARIABLE_4296 (as |@_tptp.'A_n_vec_n_vec$'__1| |tptp.'A_n_vec_n_vec$'|))) (and (= (as |@_tptp.'A_n_vec_n_vec_bool_fun$'__2| |tptp.'A_n_vec_n_vec_bool_fun$'|) (ite (= BOUND_VARIABLE_4297 (as |@_tptp.'A_n_vec_n_vec_set$'__0| |tptp.'A_n_vec_n_vec_set$'|)) (as |@_tptp.'A_n_vec_n_vec_bool_fun$'__0| |tptp.'A_n_vec_n_vec_bool_fun$'|) (ite (= BOUND_VARIABLE_4297 (as |@_tptp.'A_n_vec_n_vec_set$'__1| |tptp.'A_n_vec_n_vec_set$'|)) (as |@_tptp.'A_n_vec_n_vec_bool_fun$'__1| |tptp.'A_n_vec_n_vec_bool_fun$'|) (as |@_tptp.'A_n_vec_n_vec_bool_fun$'__2| |tptp.'A_n_vec_n_vec_bool_fun$'|)))) (= BOUND_VARIABLE_4296 (as |@_tptp.'A_n_vec_n_vec$'__0| |tptp.'A_n_vec_n_vec$'|))) (and (= (as |@_tptp.'A_n_vec_n_vec_bool_fun$'__1| |tptp.'A_n_vec_n_vec_bool_fun$'|) (ite (= BOUND_VARIABLE_4297 (as |@_tptp.'A_n_vec_n_vec_set$'__0| |tptp.'A_n_vec_n_vec_set$'|)) (as |@_tptp.'A_n_vec_n_vec_bool_fun$'__0| |tptp.'A_n_vec_n_vec_bool_fun$'|) (ite (= BOUND_VARIABLE_4297 (as |@_tptp.'A_n_vec_n_vec_set$'__1| |tptp.'A_n_vec_n_vec_set$'|)) (as |@_tptp.'A_n_vec_n_vec_bool_fun$'__1| |tptp.'A_n_vec_n_vec_bool_fun$'|) (as |@_tptp.'A_n_vec_n_vec_bool_fun$'__2| |tptp.'A_n_vec_n_vec_bool_fun$'|)))) (= BOUND_VARIABLE_4296 (as |@_tptp.'A_n_vec_n_vec$'__0| |tptp.'A_n_vec_n_vec$'|))))) % 141.49/141.77 (define-fun |tptp.'zero$d'| () |tptp.'A_set$'| (as |@_tptp.'A_set$'__0| |tptp.'A_set$'|)) % 141.49/141.77 (define-fun |tptp.'times$g'| (($x1 |tptp.'Num$'|) ($x2 |tptp.'Num$'|)) |tptp.'Num$'| (as |@_tptp.'Num$'__0| |tptp.'Num$'|)) % 141.49/141.77 (define-fun |tptp.'collect$a'| (($x1 |tptp.'A_n_vec_n_vec_bool_fun$'|)) |tptp.'A_n_vec_n_vec_set$'| (ite (= (as |@_tptp.'A_n_vec_n_vec_bool_fun$'__0| |tptp.'A_n_vec_n_vec_bool_fun$'|) $x1) (as |@_tptp.'A_n_vec_n_vec_set$'__0| |tptp.'A_n_vec_n_vec_set$'|) (ite (= (as |@_tptp.'A_n_vec_n_vec_bool_fun$'__1| |tptp.'A_n_vec_n_vec_bool_fun$'|) $x1) (as |@_tptp.'A_n_vec_n_vec_set$'__1| |tptp.'A_n_vec_n_vec_set$'|) (as |@_tptp.'A_n_vec_n_vec_set$'__2| |tptp.'A_n_vec_n_vec_set$'|)))) % 141.49/141.77 (define-fun |tptp.'zero$c'| () |tptp.'A_n_vec$'| (as |@_tptp.'A_n_vec$'__1| |tptp.'A_n_vec$'|)) % 141.49/141.77 (define-fun |tptp.'axis$a'| (($x1 |tptp.'N$'|) ($x2 |tptp.'A$'|)) |tptp.'A_n_vec$'| (ite (and (= (as |@_tptp.'N$'__0| |tptp.'N$'|) $x1) (= (as |@_tptp.'A$'__0| |tptp.'A$'|) $x2)) (as |@_tptp.'A_n_vec$'__0| |tptp.'A_n_vec$'|) (as |@_tptp.'A_n_vec$'__1| |tptp.'A_n_vec$'|))) % 141.49/141.77 (define-fun |tptp.'plus$c'| (($x1 |tptp.'A_n_vec_n_vec_set_set$'|) ($x2 |tptp.'A_n_vec_n_vec_set_set$'|)) |tptp.'A_n_vec_n_vec_set_set$'| (as |@_tptp.'A_n_vec_n_vec_set_set$'__0| |tptp.'A_n_vec_n_vec_set_set$'|)) % 141.49/141.77 (define-fun |tptp.'plus$i'| (($x1 |tptp.'A_n_vec_n_vec_n_vec$'|) ($x2 |tptp.'A_n_vec_n_vec_n_vec$'|)) |tptp.'A_n_vec_n_vec_n_vec$'| (ite (and (= (as |@_tptp.'A_n_vec_n_vec_n_vec$'__0| |tptp.'A_n_vec_n_vec_n_vec$'|) $x1) (= (as |@_tptp.'A_n_vec_n_vec_n_vec$'__0| |tptp.'A_n_vec_n_vec_n_vec$'|) $x2)) (as |@_tptp.'A_n_vec_n_vec_n_vec$'__0| |tptp.'A_n_vec_n_vec_n_vec$'|) (ite (and (= (as |@_tptp.'A_n_vec_n_vec_n_vec$'__1| |tptp.'A_n_vec_n_vec_n_vec$'|) $x1) (= (as |@_tptp.'A_n_vec_n_vec_n_vec$'__1| |tptp.'A_n_vec_n_vec_n_vec$'|) $x2)) (as |@_tptp.'A_n_vec_n_vec_n_vec$'__0| |tptp.'A_n_vec_n_vec_n_vec$'|) (as |@_tptp.'A_n_vec_n_vec_n_vec$'__1| |tptp.'A_n_vec_n_vec_n_vec$'|)))) % 141.49/141.77 (define-fun |tptp.'vec$a'| (($x1 |tptp.'A_n_vec$'|)) |tptp.'A_n_vec_n_vec$'| (ite (= (as |@_tptp.'A_n_vec$'__1| |tptp.'A_n_vec$'|) $x1) (as |@_tptp.'A_n_vec_n_vec$'__0| |tptp.'A_n_vec_n_vec$'|) (as |@_tptp.'A_n_vec_n_vec$'__1| |tptp.'A_n_vec_n_vec$'|))) % 141.49/141.77 (define-fun |tptp.'member$e'| (($x1 |tptp.'A_n_vec_n_vec_set$'|) ($x2 |tptp.'A_n_vec_n_vec_set_set$'|)) Bool false) % 141.49/141.77 (define-fun |tptp.'zero$f'| () |tptp.'A_n_vec_set$'| (as |@_tptp.'A_n_vec_set$'__0| |tptp.'A_n_vec_set$'|)) % 141.49/141.77 (define-fun |tptp.'times$a'| (($x1 |tptp.'A_n_vec$'|) ($x2 |tptp.'A_n_vec$'|)) |tptp.'A_n_vec$'| (ite (and (= (as |@_tptp.'A_n_vec$'__0| |tptp.'A_n_vec$'|) $x1) (= (as |@_tptp.'A_n_vec$'__0| |tptp.'A_n_vec$'|) $x2)) (as |@_tptp.'A_n_vec$'__0| |tptp.'A_n_vec$'|) (as |@_tptp.'A_n_vec$'__1| |tptp.'A_n_vec$'|))) % 141.49/141.77 (define-fun |tptp.'times$'| (($x1 |tptp.'A$'|) ($x2 |tptp.'A$'|)) |tptp.'A$'| (ite (and (= (as |@_tptp.'A$'__0| |tptp.'A$'|) $x1) (= (as |@_tptp.'A$'__0| |tptp.'A$'|) $x2)) (as |@_tptp.'A$'__0| |tptp.'A$'|) (as |@_tptp.'A$'__1| |tptp.'A$'|))) % 141.49/141.77 (define-fun |tptp.'member$d'| (($x1 |tptp.'Num$'|) ($x2 |tptp.'Num_set$'|)) Bool false) % 141.49/141.77 (define-fun |tptp.'collect$'| (($x1 |tptp.'A_bool_fun$'|)) |tptp.'A_set$'| (as |@_tptp.'A_set$'__0| |tptp.'A_set$'|)) % 141.49/141.77 (define-fun |tptp.'one$'| () |tptp.'A$'| (as |@_tptp.'A$'__0| |tptp.'A$'|)) % 141.49/141.77 (define-fun |tptp.'zero$b'| () |tptp.'A_n_vec_n_vec_n_vec$'| (as |@_tptp.'A_n_vec_n_vec_n_vec$'__0| |tptp.'A_n_vec_n_vec_n_vec$'|)) % 141.49/141.77 (define-fun |tptp.'matrix_inv$'| (($x1 |tptp.'A_n_vec_n_vec$'|)) |tptp.'A_n_vec_n_vec$'| (ite (= (as |@_tptp.'A_n_vec_n_vec$'__0| |tptp.'A_n_vec_n_vec$'|) $x1) (as |@_tptp.'A_n_vec_n_vec$'__0| |tptp.'A_n_vec_n_vec$'|) (as |@_tptp.'A_n_vec_n_vec$'__1| |tptp.'A_n_vec_n_vec$'|))) % 141.49/141.77 (define-fun |tptp.'member$b'| ((BOUND_VARIABLE_36997 |tptp.'A$'|) (BOUND_VARIABLE_36999 |tptp.'A_set$'|)) Bool true) % 141.49/141.77 (define-fun |tptp.'equivalent_matrices$'| (($x1 |tptp.'A_n_vec_n_vec$'|)) |tptp.'A_n_vec_n_vec_bool_fun$'| (ite (= (as |@_tptp.'A_n_vec_n_vec$'__1| |tptp.'A_n_vec_n_vec$'|) $x1) (as |@_tptp.'A_n_vec_n_vec_bool_fun$'__0| |tptp.'A_n_vec_n_vec_bool_fun$'|) (as |@_tptp.'A_n_vec_n_vec_bool_fun$'__1| |tptp.'A_n_vec_n_vec_bool_fun$'|))) % 141.49/141.77 (define-fun |tptp.'fun_app$b'| (($x1 |tptp.'A_bool_fun$'|) ($x2 |tptp.'A$'|)) Bool true) % 141.49/141.77 (define-fun |tptp.'plus$a'| (($x1 |tptp.'A_set_set$'|) ($x2 |tptp.'A_set_set$'|)) |tptp.'A_set_set$'| (as |@_tptp.'A_set_set$'__0| |tptp.'A_set_set$'|)) % 141.49/141.77 (define-fun |tptp.'plus$'| (($x1 |tptp.'A_set$'|) ($x2 |tptp.'A_set$'|)) |tptp.'A_set$'| (as |@_tptp.'A_set$'__0| |tptp.'A_set$'|)) % 141.49/141.77 (define-fun tptp.tltrue () tptp.tlbool (as @tptp.tlbool_1 tptp.tlbool)) % 141.49/141.77 (define-fun |tptp.'plus$h'| (($x1 |tptp.'A$'|) ($x2 |tptp.'A$'|)) |tptp.'A$'| (ite (and (= (as |@_tptp.'A$'__0| |tptp.'A$'|) $x1) (= (as |@_tptp.'A$'__1| |tptp.'A$'|) $x2)) (as |@_tptp.'A$'__0| |tptp.'A$'|) (ite (and (= (as |@_tptp.'A$'__1| |tptp.'A$'|) $x1) (= (as |@_tptp.'A$'__0| |tptp.'A$'|) $x2)) (as |@_tptp.'A$'__0| |tptp.'A$'|) (as |@_tptp.'A$'__1| |tptp.'A$'|)))) % 141.49/141.77 (define-fun |tptp.'one$b'| () |tptp.'A_n_vec_n_vec$'| (as |@_tptp.'A_n_vec_n_vec$'__1| |tptp.'A_n_vec_n_vec$'|)) % 141.49/141.77 (define-fun |tptp.'row_add$'| (($x1 |tptp.'A_n_vec_n_vec$'|) ($x2 |tptp.'N$'|) ($x3 |tptp.'N$'|) ($x4 |tptp.'A$'|)) |tptp.'A_n_vec_n_vec$'| (ite (and (= (as |@_tptp.'A_n_vec_n_vec$'__0| |tptp.'A_n_vec_n_vec$'|) $x1) (= (as |@_tptp.'N$'__0| |tptp.'N$'|) $x2) (= (as |@_tptp.'N$'__0| |tptp.'N$'|) $x3) (= (as |@_tptp.'A$'__1| |tptp.'A$'|) $x4)) (as |@_tptp.'A_n_vec_n_vec$'__0| |tptp.'A_n_vec_n_vec$'|) (ite (and (= (as |@_tptp.'A_n_vec_n_vec$'__0| |tptp.'A_n_vec_n_vec$'|) $x1) (= (as |@_tptp.'N$'__0| |tptp.'N$'|) $x2) (= (as |@_tptp.'N$'__0| |tptp.'N$'|) $x3) (= (as |@_tptp.'A$'__0| |tptp.'A$'|) $x4)) (as |@_tptp.'A_n_vec_n_vec$'__0| |tptp.'A_n_vec_n_vec$'|) (as |@_tptp.'A_n_vec_n_vec$'__1| |tptp.'A_n_vec_n_vec$'|)))) % 141.49/141.77 (define-fun |tptp.'numeral$'| (($x1 |tptp.'Num$'|)) |tptp.'A_n_vec$'| (as |@_tptp.'A_n_vec$'__1| |tptp.'A_n_vec$'|)) % 141.49/141.77 (define-fun |tptp.'rowvector$'| (($x1 |tptp.'A_n_vec$'|)) |tptp.'A_n_vec_n_vec$'| (as |@_tptp.'A_n_vec_n_vec$'__0| |tptp.'A_n_vec_n_vec$'|)) % 141.49/141.77 (define-fun |tptp.'gauss_Jordan_upt_k$'| (($x1 |tptp.'A_n_vec_n_vec$'|) ($x2 |tptp.'Nat$'|)) |tptp.'A_n_vec_n_vec$'| (ite (and (= (as |@_tptp.'A_n_vec_n_vec$'__0| |tptp.'A_n_vec_n_vec$'|) $x1) (= (as |@_tptp.'Nat$'__0| |tptp.'Nat$'|) $x2)) (as |@_tptp.'A_n_vec_n_vec$'__0| |tptp.'A_n_vec_n_vec$'|) (as |@_tptp.'A_n_vec_n_vec$'__1| |tptp.'A_n_vec_n_vec$'|))) % 141.49/141.77 (define-fun |tptp.'mat$a'| (($x1 |tptp.'A_n_vec$'|)) |tptp.'A_n_vec_n_vec_n_vec$'| (as |@_tptp.'A_n_vec_n_vec_n_vec$'__1| |tptp.'A_n_vec_n_vec_n_vec$'|)) % 141.49/141.77 (define-fun |tptp.'collect$b'| (($x1 |tptp.'A_n_vec_bool_fun$'|)) |tptp.'A_n_vec_set$'| (as |@_tptp.'A_n_vec_set$'__0| |tptp.'A_n_vec_set$'|)) % 141.49/141.77 (define-fun |tptp.'less_eq$'| (($x1 |tptp.'A_n_vec_set$'|) ($x2 |tptp.'A_n_vec_set$'|)) Bool true) % 141.49/141.77 (define-fun |tptp.'a$'| () |tptp.'A_n_vec_n_vec$'| (as |@_tptp.'A_n_vec_n_vec$'__1| |tptp.'A_n_vec_n_vec$'|)) % 141.49/141.77 (define-fun |tptp.'mult_column$'| (($x1 |tptp.'A_n_vec_n_vec$'|) ($x2 |tptp.'N$'|) ($x3 |tptp.'A$'|)) |tptp.'A_n_vec_n_vec$'| (ite (and (= (as |@_tptp.'A_n_vec_n_vec$'__0| |tptp.'A_n_vec_n_vec$'|) $x1) (= (as |@_tptp.'N$'__0| |tptp.'N$'|) $x2) (= (as |@_tptp.'A$'__0| |tptp.'A$'|) $x3)) (as |@_tptp.'A_n_vec_n_vec$'__0| |tptp.'A_n_vec_n_vec$'|) (ite (and (= (as |@_tptp.'A_n_vec_n_vec$'__0| |tptp.'A_n_vec_n_vec$'|) $x1) (= (as |@_tptp.'N$'__0| |tptp.'N$'|) $x2) (= (as |@_tptp.'A$'__1| |tptp.'A$'|) $x3)) (as |@_tptp.'A_n_vec_n_vec$'__0| |tptp.'A_n_vec_n_vec$'|) (as |@_tptp.'A_n_vec_n_vec$'__1| |tptp.'A_n_vec_n_vec$'|)))) % 141.49/141.77 (define-fun |tptp.'column_add$'| (($x1 |tptp.'A_n_vec_n_vec$'|) ($x2 |tptp.'N$'|) ($x3 |tptp.'N$'|) ($x4 |tptp.'A$'|)) |tptp.'A_n_vec_n_vec$'| (ite (and (= (as |@_tptp.'A_n_vec_n_vec$'__0| |tptp.'A_n_vec_n_vec$'|) $x1) (= (as |@_tptp.'N$'__0| |tptp.'N$'|) $x2) (= (as |@_tptp.'N$'__0| |tptp.'N$'|) $x3) (= (as |@_tptp.'A$'__1| |tptp.'A$'|) $x4)) (as |@_tptp.'A_n_vec_n_vec$'__0| |tptp.'A_n_vec_n_vec$'|) (ite (and (= (as |@_tptp.'A_n_vec_n_vec$'__0| |tptp.'A_n_vec_n_vec$'|) $x1) (= (as |@_tptp.'N$'__0| |tptp.'N$'|) $x2) (= (as |@_tptp.'N$'__0| |tptp.'N$'|) $x3) (= (as |@_tptp.'A$'__0| |tptp.'A$'|) $x4)) (as |@_tptp.'A_n_vec_n_vec$'__0| |tptp.'A_n_vec_n_vec$'|) (as |@_tptp.'A_n_vec_n_vec$'__1| |tptp.'A_n_vec_n_vec$'|)))) % 141.49/141.77 (define-fun |tptp.'fun_app$a'| (($x1 |tptp.'A_n_vec_bool_fun$'|) ($x2 |tptp.'A_n_vec$'|)) Bool true) % 141.49/141.77 (define-fun |tptp.'invertible$a'| (($x1 |tptp.'A_n_vec_n_vec_n_vec$'|)) Bool false) % 141.49/141.77 (define-fun |tptp.'reduced_row_echelon_form$'| () |tptp.'A_n_vec_n_vec_bool_fun$'| (as |@_tptp.'A_n_vec_n_vec_bool_fun$'__2| |tptp.'A_n_vec_n_vec_bool_fun$'|)) % 141.49/141.77 (define-fun |tptp.'plus$b'| (($x1 |tptp.'A_n_vec_n_vec_set$'|) ($x2 |tptp.'A_n_vec_n_vec_set$'|)) |tptp.'A_n_vec_n_vec_set$'| (ite (and (= (as |@_tptp.'A_n_vec_n_vec_set$'__0| |tptp.'A_n_vec_n_vec_set$'|) $x1) (= (as |@_tptp.'A_n_vec_n_vec_set$'__1| |tptp.'A_n_vec_n_vec_set$'|) $x2)) (as |@_tptp.'A_n_vec_n_vec_set$'__0| |tptp.'A_n_vec_n_vec_set$'|) (ite (and (= (as |@_tptp.'A_n_vec_n_vec_set$'__1| |tptp.'A_n_vec_n_vec_set$'|) $x1) (= (as |@_tptp.'A_n_vec_n_vec_set$'__0| |tptp.'A_n_vec_n_vec_set$'|) $x2)) (as |@_tptp.'A_n_vec_n_vec_set$'__0| |tptp.'A_n_vec_n_vec_set$'|) (ite (and (= (as |@_tptp.'A_n_vec_n_vec_set$'__1| |tptp.'A_n_vec_n_vec_set$'|) $x1) (= (as |@_tptp.'A_n_vec_n_vec_set$'__1| |tptp.'A_n_vec_n_vec_set$'|) $x2)) (as |@_tptp.'A_n_vec_n_vec_set$'__1| |tptp.'A_n_vec_n_vec_set$'|) (ite (and (= (as |@_tptp.'A_n_vec_n_vec_set$'__0| |tptp.'A_n_vec_n_vec_set$'|) $x1) (= (as |@_tptp.'A_n_vec_n_vec_set$'__0| |tptp.'A_n_vec_n_vec_set$'|) $x2)) (as |@_tptp.'A_n_vec_n_vec_set$'__1| |tptp.'A_n_vec_n_vec_set$'|) (as |@_tptp.'A_n_vec_n_vec_set$'__2| |tptp.'A_n_vec_n_vec_set$'|)))))) % 141.49/141.77 (define-fun |tptp.'one$a'| () |tptp.'A_n_vec$'| (as |@_tptp.'A_n_vec$'__0| |tptp.'A_n_vec$'|)) % 141.49/141.77 (define-fun |tptp.'divide$'| (($x1 |tptp.'A$'|)) |tptp.'A_a_fun$'| (ite (= (as |@_tptp.'A$'__1| |tptp.'A$'|) $x1) (as |@_tptp.'A_a_fun$'__0| |tptp.'A_a_fun$'|) (as |@_tptp.'A_a_fun$'__1| |tptp.'A_a_fun$'|))) % 141.49/141.77 (define-fun |tptp.'zero$a'| () |tptp.'A_n_vec_n_vec$'| (as |@_tptp.'A_n_vec_n_vec$'__0| |tptp.'A_n_vec_n_vec$'|)) % 141.49/141.77 (define-fun |tptp.'matrix_matrix_mult$'| (($x1 |tptp.'A_n_vec_n_vec$'|) ($x2 |tptp.'A_n_vec_n_vec$'|)) |tptp.'A_n_vec_n_vec$'| (ite (and (= (as |@_tptp.'A_n_vec_n_vec$'__1| |tptp.'A_n_vec_n_vec$'|) $x1) (= (as |@_tptp.'A_n_vec_n_vec$'__0| |tptp.'A_n_vec_n_vec$'|) $x2)) (as |@_tptp.'A_n_vec_n_vec$'__0| |tptp.'A_n_vec_n_vec$'|) (ite (and (= (as |@_tptp.'A_n_vec_n_vec$'__0| |tptp.'A_n_vec_n_vec$'|) $x1) (= (as |@_tptp.'A_n_vec_n_vec$'__1| |tptp.'A_n_vec_n_vec$'|) $x2)) (as |@_tptp.'A_n_vec_n_vec$'__0| |tptp.'A_n_vec_n_vec$'|) (ite (and (= (as |@_tptp.'A_n_vec_n_vec$'__0| |tptp.'A_n_vec_n_vec$'|) $x1) (= (as |@_tptp.'A_n_vec_n_vec$'__0| |tptp.'A_n_vec_n_vec$'|) $x2)) (as |@_tptp.'A_n_vec_n_vec$'__0| |tptp.'A_n_vec_n_vec$'|) (as |@_tptp.'A_n_vec_n_vec$'__1| |tptp.'A_n_vec_n_vec$'|))))) % 141.49/141.77 (define-fun |tptp.'transpose$'| (($x1 |tptp.'A_n_vec_n_vec$'|)) |tptp.'A_n_vec_n_vec$'| (ite (= (as |@_tptp.'A_n_vec_n_vec$'__0| |tptp.'A_n_vec_n_vec$'|) $x1) (as |@_tptp.'A_n_vec_n_vec$'__0| |tptp.'A_n_vec_n_vec$'|) (as |@_tptp.'A_n_vec_n_vec$'__1| |tptp.'A_n_vec_n_vec$'|))) % 141.49/141.77 (define-fun |tptp.'orthogonal_matrix$'| () |tptp.'A_n_vec_n_vec_bool_fun$'| (as |@_tptp.'A_n_vec_n_vec_bool_fun$'__0| |tptp.'A_n_vec_n_vec_bool_fun$'|)) % 141.49/141.77 (define-fun |tptp.'fun_app$d'| (($x1 |tptp.'A_a_fun$'|) ($x2 |tptp.'A$'|)) |tptp.'A$'| (ite (and (= (as |@_tptp.'A_a_fun$'__1| |tptp.'A_a_fun$'|) $x1) (= (as |@_tptp.'A$'__0| |tptp.'A$'|) $x2)) (as |@_tptp.'A$'__0| |tptp.'A$'|) (as |@_tptp.'A$'__1| |tptp.'A$'|))) % 141.49/141.77 (define-fun |tptp.'uua$'| (($x1 |tptp.'A_n_vec_n_vec_set$'|)) |tptp.'A_n_vec_n_vec_bool_fun$'| (ite (= (as |@_tptp.'A_n_vec_n_vec_set$'__0| |tptp.'A_n_vec_n_vec_set$'|) $x1) (as |@_tptp.'A_n_vec_n_vec_bool_fun$'__0| |tptp.'A_n_vec_n_vec_bool_fun$'|) (ite (= (as |@_tptp.'A_n_vec_n_vec_set$'__1| |tptp.'A_n_vec_n_vec_set$'|) $x1) (as |@_tptp.'A_n_vec_n_vec_bool_fun$'__1| |tptp.'A_n_vec_n_vec_bool_fun$'|) (as |@_tptp.'A_n_vec_n_vec_bool_fun$'__2| |tptp.'A_n_vec_n_vec_bool_fun$'|)))) % 141.49/141.77 (define-fun |tptp.'matrix_vector_mult$a'| ((BOUND_VARIABLE_4607 |tptp.'A_n_vec_n_vec_n_vec$'|) (BOUND_VARIABLE_4608 |tptp.'A_n_vec_n_vec$'|)) |tptp.'A_n_vec_n_vec$'| (ite (and (= BOUND_VARIABLE_4608 (as |@_tptp.'A_n_vec_n_vec$'__1| |tptp.'A_n_vec_n_vec$'|)) (= (as |@_tptp.'A_n_vec_n_vec_n_vec$'__0| |tptp.'A_n_vec_n_vec_n_vec$'|) (ite (= BOUND_VARIABLE_4607 (as |@_tptp.'A_n_vec_n_vec_n_vec$'__0| |tptp.'A_n_vec_n_vec_n_vec$'|)) (as |@_tptp.'A_n_vec_n_vec_n_vec$'__0| |tptp.'A_n_vec_n_vec_n_vec$'|) (as |@_tptp.'A_n_vec_n_vec_n_vec$'__1| |tptp.'A_n_vec_n_vec_n_vec$'|)))) (as |@_tptp.'A_n_vec_n_vec$'__0| |tptp.'A_n_vec_n_vec$'|) (ite (and (= BOUND_VARIABLE_4608 (as |@_tptp.'A_n_vec_n_vec$'__0| |tptp.'A_n_vec_n_vec$'|)) (= (as |@_tptp.'A_n_vec_n_vec_n_vec$'__0| |tptp.'A_n_vec_n_vec_n_vec$'|) (ite (= BOUND_VARIABLE_4607 (as |@_tptp.'A_n_vec_n_vec_n_vec$'__0| |tptp.'A_n_vec_n_vec_n_vec$'|)) (as |@_tptp.'A_n_vec_n_vec_n_vec$'__0| |tptp.'A_n_vec_n_vec_n_vec$'|) (as |@_tptp.'A_n_vec_n_vec_n_vec$'__1| |tptp.'A_n_vec_n_vec_n_vec$'|)))) (as |@_tptp.'A_n_vec_n_vec$'__0| |tptp.'A_n_vec_n_vec$'|) (ite (and (= BOUND_VARIABLE_4608 (as |@_tptp.'A_n_vec_n_vec$'__0| |tptp.'A_n_vec_n_vec$'|)) (= (as |@_tptp.'A_n_vec_n_vec_n_vec$'__1| |tptp.'A_n_vec_n_vec_n_vec$'|) (ite (= BOUND_VARIABLE_4607 (as |@_tptp.'A_n_vec_n_vec_n_vec$'__0| |tptp.'A_n_vec_n_vec_n_vec$'|)) (as |@_tptp.'A_n_vec_n_vec_n_vec$'__0| |tptp.'A_n_vec_n_vec_n_vec$'|) (as |@_tptp.'A_n_vec_n_vec_n_vec$'__1| |tptp.'A_n_vec_n_vec_n_vec$'|)))) (as |@_tptp.'A_n_vec_n_vec$'__0| |tptp.'A_n_vec_n_vec$'|) (as |@_tptp.'A_n_vec_n_vec$'__1| |tptp.'A_n_vec_n_vec$'|))))) % 141.49/141.77 (define-fun |tptp.'column$'| (($x1 |tptp.'N$'|) ($x2 |tptp.'A_n_vec_n_vec$'|)) |tptp.'A_n_vec$'| (as |@_tptp.'A_n_vec$'__1| |tptp.'A_n_vec$'|)) % 141.49/141.77 (define-fun |tptp.'vec$'| (($x1 |tptp.'A$'|)) |tptp.'A_n_vec$'| (ite (= (as |@_tptp.'A$'__0| |tptp.'A$'|) $x1) (as |@_tptp.'A_n_vec$'__0| |tptp.'A_n_vec$'|) (as |@_tptp.'A_n_vec$'__1| |tptp.'A_n_vec$'|))) % 141.49/141.77 (define-fun |tptp.'times$b'| (($x1 |tptp.'A_n_vec_n_vec$'|) ($x2 |tptp.'A_n_vec_n_vec$'|)) |tptp.'A_n_vec_n_vec$'| (ite (and (= (as |@_tptp.'A_n_vec_n_vec$'__0| |tptp.'A_n_vec_n_vec$'|) $x1) (= (as |@_tptp.'A_n_vec_n_vec$'__1| |tptp.'A_n_vec_n_vec$'|) $x2)) (as |@_tptp.'A_n_vec_n_vec$'__0| |tptp.'A_n_vec_n_vec$'|) (ite (and (= (as |@_tptp.'A_n_vec_n_vec$'__1| |tptp.'A_n_vec_n_vec$'|) $x1) (= (as |@_tptp.'A_n_vec_n_vec$'__0| |tptp.'A_n_vec_n_vec$'|) $x2)) (as |@_tptp.'A_n_vec_n_vec$'__0| |tptp.'A_n_vec_n_vec$'|) (ite (and (= (as |@_tptp.'A_n_vec_n_vec$'__0| |tptp.'A_n_vec_n_vec$'|) $x1) (= (as |@_tptp.'A_n_vec_n_vec$'__0| |tptp.'A_n_vec_n_vec$'|) $x2)) (as |@_tptp.'A_n_vec_n_vec$'__0| |tptp.'A_n_vec_n_vec$'|) (as |@_tptp.'A_n_vec_n_vec$'__1| |tptp.'A_n_vec_n_vec$'|))))) % 141.49/141.77 (define-fun |tptp.'one$c'| () |tptp.'A_set$'| (as |@_tptp.'A_set$'__0| |tptp.'A_set$'|)) % 141.49/141.77 (define-fun |tptp.'zero$'| () |tptp.'A$'| (as |@_tptp.'A$'__1| |tptp.'A$'|)) % 141.49/141.77 (define-fun |tptp.'plus$d'| (($x1 |tptp.'A_n_vec$'|) ($x2 |tptp.'A_n_vec$'|)) |tptp.'A_n_vec$'| (ite (and (= (as |@_tptp.'A_n_vec$'__1| |tptp.'A_n_vec$'|) $x1) (= (as |@_tptp.'A_n_vec$'__0| |tptp.'A_n_vec$'|) $x2)) (as |@_tptp.'A_n_vec$'__0| |tptp.'A_n_vec$'|) (ite (and (= (as |@_tptp.'A_n_vec$'__0| |tptp.'A_n_vec$'|) $x1) (= (as |@_tptp.'A_n_vec$'__1| |tptp.'A_n_vec$'|) $x2)) (as |@_tptp.'A_n_vec$'__0| |tptp.'A_n_vec$'|) (as |@_tptp.'A_n_vec$'__1| |tptp.'A_n_vec$'|)))) % 141.49/141.77 (define-fun |tptp.'fun_app$c'| (($x1 |tptp.'N_a_n_vec_n_vec_fun$'|) ($x2 |tptp.'N$'|)) |tptp.'A_n_vec_n_vec$'| (ite (and (= (as |@_tptp.'N_a_n_vec_n_vec_fun$'__1| |tptp.'N_a_n_vec_n_vec_fun$'|) $x1) (= (as |@_tptp.'N$'__0| |tptp.'N$'|) $x2)) (as |@_tptp.'A_n_vec_n_vec$'__0| |tptp.'A_n_vec_n_vec$'|) (as |@_tptp.'A_n_vec_n_vec$'__1| |tptp.'A_n_vec_n_vec$'|))) % 141.49/141.77 (define-fun tptp.tlfalse () tptp.tlbool (as @tptp.tlbool_0 tptp.tlbool)) % 141.49/141.77 (define-fun |tptp.'numeral$b'| (($x1 |tptp.'Num$'|)) |tptp.'A$'| (as |@_tptp.'A$'__0| |tptp.'A$'|)) % 141.49/141.77 (define-fun |tptp.'zero$e'| () |tptp.'A_n_vec_n_vec_set$'| (as |@_tptp.'A_n_vec_n_vec_set$'__1| |tptp.'A_n_vec_n_vec_set$'|)) % 141.49/141.77 (define-fun |tptp.'plus$e'| (($x1 |tptp.'A_n_vec_set$'|) ($x2 |tptp.'A_n_vec_set$'|)) |tptp.'A_n_vec_set$'| (as |@_tptp.'A_n_vec_set$'__0| |tptp.'A_n_vec_set$'|)) % 141.49/141.77 (define-fun |tptp.'times$h'| (($x1 |tptp.'Num_set$'|) ($x2 |tptp.'Num_set$'|)) |tptp.'Num_set$'| (as |@_tptp.'Num_set$'__0| |tptp.'Num_set$'|)) % 141.49/141.77 (define-fun |tptp.'less_eq$a'| (($x1 |tptp.'A_n_vec_n_vec_set$'|) ($x2 |tptp.'A_n_vec_n_vec_set$'|)) Bool (or (and (= (as |@_tptp.'A_n_vec_n_vec_set$'__0| |tptp.'A_n_vec_n_vec_set$'|) $x1) (= (as |@_tptp.'A_n_vec_n_vec_set$'__2| |tptp.'A_n_vec_n_vec_set$'|) $x2)) (and (= (as |@_tptp.'A_n_vec_n_vec_set$'__2| |tptp.'A_n_vec_n_vec_set$'|) $x1) (= (as |@_tptp.'A_n_vec_n_vec_set$'__2| |tptp.'A_n_vec_n_vec_set$'|) $x2)) (and (= (as |@_tptp.'A_n_vec_n_vec_set$'__1| |tptp.'A_n_vec_n_vec_set$'|) $x1) (= (as |@_tptp.'A_n_vec_n_vec_set$'__2| |tptp.'A_n_vec_n_vec_set$'|) $x2)) (and (= (as |@_tptp.'A_n_vec_n_vec_set$'__1| |tptp.'A_n_vec_n_vec_set$'|) $x1) (= (as |@_tptp.'A_n_vec_n_vec_set$'__1| |tptp.'A_n_vec_n_vec_set$'|) $x2)) (and (= (as |@_tptp.'A_n_vec_n_vec_set$'__0| |tptp.'A_n_vec_n_vec_set$'|) $x1) (= (as |@_tptp.'A_n_vec_n_vec_set$'__0| |tptp.'A_n_vec_n_vec_set$'|) $x2)))) % 141.49/141.77 (define-fun |tptp.'similar_matrices$'| (($x1 |tptp.'A_n_vec_n_vec$'|)) |tptp.'A_n_vec_n_vec_bool_fun$'| (ite (= (as |@_tptp.'A_n_vec_n_vec$'__1| |tptp.'A_n_vec_n_vec$'|) $x1) (as |@_tptp.'A_n_vec_n_vec_bool_fun$'__0| |tptp.'A_n_vec_n_vec_bool_fun$'|) (as |@_tptp.'A_n_vec_n_vec_bool_fun$'__1| |tptp.'A_n_vec_n_vec_bool_fun$'|))) % 141.49/141.77 (define-fun |tptp.'transpose$a'| (($x1 |tptp.'A_n_vec_n_vec_n_vec$'|)) |tptp.'A_n_vec_n_vec_n_vec$'| (ite (= (as |@_tptp.'A_n_vec_n_vec_n_vec$'__0| |tptp.'A_n_vec_n_vec_n_vec$'|) $x1) (as |@_tptp.'A_n_vec_n_vec_n_vec$'__0| |tptp.'A_n_vec_n_vec_n_vec$'|) (as |@_tptp.'A_n_vec_n_vec_n_vec$'__1| |tptp.'A_n_vec_n_vec_n_vec$'|))) % 141.49/141.77 (define-fun |tptp.'less_eq$b'| (($x1 |tptp.'A_set$'|) ($x2 |tptp.'A_set$'|)) Bool true) % 141.49/141.77 (define-fun |tptp.'member$c'| (($x1 |tptp.'A_set$'|) ($x2 |tptp.'A_set_set$'|)) Bool false) % 141.49/141.77 (define-fun |tptp.'member$a'| ((BOUND_VARIABLE_37058 |tptp.'A_n_vec$'|) (BOUND_VARIABLE_37060 |tptp.'A_n_vec_set$'|)) Bool true) % 141.49/141.77 (define-fun |tptp.'times$c'| (($x1 |tptp.'A_set$'|) ($x2 |tptp.'A_set$'|)) |tptp.'A_set$'| (as |@_tptp.'A_set$'__0| |tptp.'A_set$'|)) % 141.49/141.77 (define-fun |tptp.'interchange_columns$'| ((BOUND_VARIABLE_4373 |tptp.'A_n_vec_n_vec$'|) (BOUND_VARIABLE_4374 |tptp.'N$'|) (BOUND_VARIABLE_4375 |tptp.'N$'|)) |tptp.'A_n_vec_n_vec$'| (ite (= (as |@_tptp.'A_n_vec_n_vec$'__0| |tptp.'A_n_vec_n_vec$'|) (ite (and (= (as |@_tptp.'N_a_n_vec_n_vec_fun$'__1| |tptp.'N_a_n_vec_n_vec_fun$'|) (ite (and (= (as |@_tptp.'A_n_vec_n_vec$'__1| |tptp.'A_n_vec_n_vec$'|) (ite (= BOUND_VARIABLE_4373 (as |@_tptp.'A_n_vec_n_vec$'__0| |tptp.'A_n_vec_n_vec$'|)) (as |@_tptp.'A_n_vec_n_vec$'__0| |tptp.'A_n_vec_n_vec$'|) (as |@_tptp.'A_n_vec_n_vec$'__1| |tptp.'A_n_vec_n_vec$'|))) (= BOUND_VARIABLE_4374 (as |@_tptp.'N$'__0| |tptp.'N$'|))) (as |@_tptp.'N_a_n_vec_n_vec_fun$'__0| |tptp.'N_a_n_vec_n_vec_fun$'|) (as |@_tptp.'N_a_n_vec_n_vec_fun$'__1| |tptp.'N_a_n_vec_n_vec_fun$'|))) (= BOUND_VARIABLE_4375 (as |@_tptp.'N$'__0| |tptp.'N$'|))) (as |@_tptp.'A_n_vec_n_vec$'__0| |tptp.'A_n_vec_n_vec$'|) (as |@_tptp.'A_n_vec_n_vec$'__1| |tptp.'A_n_vec_n_vec$'|))) (as |@_tptp.'A_n_vec_n_vec$'__0| |tptp.'A_n_vec_n_vec$'|) (as |@_tptp.'A_n_vec_n_vec$'__1| |tptp.'A_n_vec_n_vec$'|))) % 141.49/141.77 (define-fun |tptp.'fun_app$'| (($x1 |tptp.'A_n_vec_n_vec_bool_fun$'|) ($x2 |tptp.'A_n_vec_n_vec$'|)) Bool (or (and (= (as |@_tptp.'A_n_vec_n_vec_bool_fun$'__0| |tptp.'A_n_vec_n_vec_bool_fun$'|) $x1) (= (as |@_tptp.'A_n_vec_n_vec$'__1| |tptp.'A_n_vec_n_vec$'|) $x2)) (and (= (as |@_tptp.'A_n_vec_n_vec_bool_fun$'__2| |tptp.'A_n_vec_n_vec_bool_fun$'|) $x1) (= (as |@_tptp.'A_n_vec_n_vec$'__1| |tptp.'A_n_vec_n_vec$'|) $x2)) (and (= (as |@_tptp.'A_n_vec_n_vec_bool_fun$'__2| |tptp.'A_n_vec_n_vec_bool_fun$'|) $x1) (= (as |@_tptp.'A_n_vec_n_vec$'__0| |tptp.'A_n_vec_n_vec$'|) $x2)) (and (= (as |@_tptp.'A_n_vec_n_vec_bool_fun$'__1| |tptp.'A_n_vec_n_vec_bool_fun$'|) $x1) (= (as |@_tptp.'A_n_vec_n_vec$'__0| |tptp.'A_n_vec_n_vec$'|) $x2)))) % 141.49/141.77 (define-fun |tptp.'vector_matrix_mult$'| (($x1 |tptp.'A_n_vec_n_vec$'|) ($x2 |tptp.'A_n_vec_n_vec_n_vec$'|)) |tptp.'A_n_vec_n_vec$'| (ite (and (= (as |@_tptp.'A_n_vec_n_vec$'__1| |tptp.'A_n_vec_n_vec$'|) $x1) (= (as |@_tptp.'A_n_vec_n_vec_n_vec$'__0| |tptp.'A_n_vec_n_vec_n_vec$'|) $x2)) (as |@_tptp.'A_n_vec_n_vec$'__0| |tptp.'A_n_vec_n_vec$'|) (ite (and (= (as |@_tptp.'A_n_vec_n_vec$'__0| |tptp.'A_n_vec_n_vec$'|) $x1) (= (as |@_tptp.'A_n_vec_n_vec_n_vec$'__0| |tptp.'A_n_vec_n_vec_n_vec$'|) $x2)) (as |@_tptp.'A_n_vec_n_vec$'__0| |tptp.'A_n_vec_n_vec$'|) (ite (and (= (as |@_tptp.'A_n_vec_n_vec$'__0| |tptp.'A_n_vec_n_vec$'|) $x1) (= (as |@_tptp.'A_n_vec_n_vec_n_vec$'__1| |tptp.'A_n_vec_n_vec_n_vec$'|) $x2)) (as |@_tptp.'A_n_vec_n_vec$'__0| |tptp.'A_n_vec_n_vec$'|) (as |@_tptp.'A_n_vec_n_vec$'__1| |tptp.'A_n_vec_n_vec$'|))))) % 141.49/141.77 (define-fun |tptp.'mult_row$'| (($x1 |tptp.'A_n_vec_n_vec$'|) ($x2 |tptp.'N$'|) ($x3 |tptp.'A$'|)) |tptp.'A_n_vec_n_vec$'| (ite (and (= (as |@_tptp.'A_n_vec_n_vec$'__0| |tptp.'A_n_vec_n_vec$'|) $x1) (= (as |@_tptp.'N$'__0| |tptp.'N$'|) $x2) (= (as |@_tptp.'A$'__1| |tptp.'A$'|) $x3)) (as |@_tptp.'A_n_vec_n_vec$'__0| |tptp.'A_n_vec_n_vec$'|) (ite (and (= (as |@_tptp.'A_n_vec_n_vec$'__0| |tptp.'A_n_vec_n_vec$'|) $x1) (= (as |@_tptp.'N$'__0| |tptp.'N$'|) $x2) (= (as |@_tptp.'A$'__0| |tptp.'A$'|) $x3)) (as |@_tptp.'A_n_vec_n_vec$'__0| |tptp.'A_n_vec_n_vec$'|) (as |@_tptp.'A_n_vec_n_vec$'__1| |tptp.'A_n_vec_n_vec$'|)))) % 141.49/141.77 (define-fun |tptp.'matrix_matrix_mult$a'| (($x1 |tptp.'A_n_vec_n_vec_n_vec$'|) ($x2 |tptp.'A_n_vec_n_vec_n_vec$'|)) |tptp.'A_n_vec_n_vec_n_vec$'| (ite (and (= (as |@_tptp.'A_n_vec_n_vec_n_vec$'__0| |tptp.'A_n_vec_n_vec_n_vec$'|) $x1) (= (as |@_tptp.'A_n_vec_n_vec_n_vec$'__0| |tptp.'A_n_vec_n_vec_n_vec$'|) $x2)) (as |@_tptp.'A_n_vec_n_vec_n_vec$'__0| |tptp.'A_n_vec_n_vec_n_vec$'|) (ite (and (= (as |@_tptp.'A_n_vec_n_vec_n_vec$'__1| |tptp.'A_n_vec_n_vec_n_vec$'|) $x1) (= (as |@_tptp.'A_n_vec_n_vec_n_vec$'__0| |tptp.'A_n_vec_n_vec_n_vec$'|) $x2)) (as |@_tptp.'A_n_vec_n_vec_n_vec$'__0| |tptp.'A_n_vec_n_vec_n_vec$'|) (ite (and (= (as |@_tptp.'A_n_vec_n_vec_n_vec$'__0| |tptp.'A_n_vec_n_vec_n_vec$'|) $x1) (= (as |@_tptp.'A_n_vec_n_vec_n_vec$'__1| |tptp.'A_n_vec_n_vec_n_vec$'|) $x2)) (as |@_tptp.'A_n_vec_n_vec_n_vec$'__0| |tptp.'A_n_vec_n_vec_n_vec$'|) (as |@_tptp.'A_n_vec_n_vec_n_vec$'__1| |tptp.'A_n_vec_n_vec_n_vec$'|))))) % 141.49/141.77 (define-fun |tptp.'dbl_inc$b'| (($x1 |tptp.'A$'|)) |tptp.'A$'| (as |@_tptp.'A$'__0| |tptp.'A$'|)) % 141.49/141.77 (define-fun |tptp.'interchange_rows$'| (($x1 |tptp.'A_n_vec_n_vec$'|) ($x2 |tptp.'N$'|)) |tptp.'N_a_n_vec_n_vec_fun$'| (ite (and (= (as |@_tptp.'A_n_vec_n_vec$'__1| |tptp.'A_n_vec_n_vec$'|) $x1) (= (as |@_tptp.'N$'__0| |tptp.'N$'|) $x2)) (as |@_tptp.'N_a_n_vec_n_vec_fun$'__0| |tptp.'N_a_n_vec_n_vec_fun$'|) (as |@_tptp.'N_a_n_vec_n_vec_fun$'__1| |tptp.'N_a_n_vec_n_vec_fun$'|))) % 141.49/141.77 (define-fun |tptp.'times$e'| (($x1 |tptp.'A_n_vec_n_vec_set$'|) ($x2 |tptp.'A_n_vec_n_vec_set$'|)) |tptp.'A_n_vec_n_vec_set$'| (ite (and (= (as |@_tptp.'A_n_vec_n_vec_set$'__0| |tptp.'A_n_vec_n_vec_set$'|) $x1) (= (as |@_tptp.'A_n_vec_n_vec_set$'__0| |tptp.'A_n_vec_n_vec_set$'|) $x2)) (as |@_tptp.'A_n_vec_n_vec_set$'__0| |tptp.'A_n_vec_n_vec_set$'|) (ite (and (= (as |@_tptp.'A_n_vec_n_vec_set$'__2| |tptp.'A_n_vec_n_vec_set$'|) $x1) (= (as |@_tptp.'A_n_vec_n_vec_set$'__1| |tptp.'A_n_vec_n_vec_set$'|) $x2)) (as |@_tptp.'A_n_vec_n_vec_set$'__1| |tptp.'A_n_vec_n_vec_set$'|) (ite (and (= (as |@_tptp.'A_n_vec_n_vec_set$'__1| |tptp.'A_n_vec_n_vec_set$'|) $x1) (= (as |@_tptp.'A_n_vec_n_vec_set$'__1| |tptp.'A_n_vec_n_vec_set$'|) $x2)) (as |@_tptp.'A_n_vec_n_vec_set$'__1| |tptp.'A_n_vec_n_vec_set$'|) (ite (and (= (as |@_tptp.'A_n_vec_n_vec_set$'__0| |tptp.'A_n_vec_n_vec_set$'|) $x1) (= (as |@_tptp.'A_n_vec_n_vec_set$'__1| |tptp.'A_n_vec_n_vec_set$'|) $x2)) (as |@_tptp.'A_n_vec_n_vec_set$'__1| |tptp.'A_n_vec_n_vec_set$'|) (ite (and (= (as |@_tptp.'A_n_vec_n_vec_set$'__1| |tptp.'A_n_vec_n_vec_set$'|) $x1) (= (as |@_tptp.'A_n_vec_n_vec_set$'__0| |tptp.'A_n_vec_n_vec_set$'|) $x2)) (as |@_tptp.'A_n_vec_n_vec_set$'__1| |tptp.'A_n_vec_n_vec_set$'|) (ite (and (= (as |@_tptp.'A_n_vec_n_vec_set$'__1| |tptp.'A_n_vec_n_vec_set$'|) $x1) (= (as |@_tptp.'A_n_vec_n_vec_set$'__2| |tptp.'A_n_vec_n_vec_set$'|) $x2)) (as |@_tptp.'A_n_vec_n_vec_set$'__1| |tptp.'A_n_vec_n_vec_set$'|) (as |@_tptp.'A_n_vec_n_vec_set$'__2| |tptp.'A_n_vec_n_vec_set$'|)))))))) % 141.49/141.77 (define-fun |tptp.'times$f'| (($x1 |tptp.'A_set_set$'|) ($x2 |tptp.'A_set_set$'|)) |tptp.'A_set_set$'| (as |@_tptp.'A_set_set$'__0| |tptp.'A_set_set$'|)) % 141.49/141.77 (define-fun |tptp.'p$'| () |tptp.'A_n_vec_n_vec$'| (as |@_tptp.'A_n_vec_n_vec$'__1| |tptp.'A_n_vec_n_vec$'|)) % 141.49/141.77 (define-fun |tptp.'plus$f'| (($x1 |tptp.'A_n_vec_set_set$'|) ($x2 |tptp.'A_n_vec_set_set$'|)) |tptp.'A_n_vec_set_set$'| (as |@_tptp.'A_n_vec_set_set$'__0| |tptp.'A_n_vec_set_set$'|)) % 141.49/141.77 ) % 141.49/141.77 % SZS output end Model % 141.49/141.78 % cvc5 exiting %------------------------------------------------------------------------------