%------------------------------------------------------------------------------ % File : cvc5-SAT---1.3.4 % Problem : ITP333_1 : TPTP v9.2.1. Released v8.0.0. % Transfm : none % Format : tptp:raw % Command : /export/starexec/sandbox2/solver/bin/do_cvc5 /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % Computer : n008.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 : CounterSatisfiable 140.07s 140.35s % Output : Model 140.07s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : ITP333_1 : TPTP v9.2.1. Released v8.0.0. % 0.12/0.13 % Command : /export/starexec/sandbox2/solver/bin/do_cvc5 /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % 0.15/0.34 % Computer : n008.cluster.edu % 0.15/0.34 % Model : x86_64 x86_64 % 0.15/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.15/0.34 % Memory : 8042.1875MB % 0.15/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.15/0.34 % CPULimit : 300 % 0.15/0.34 % WCLimit : 300 % 0.15/0.34 % DateTime : Tue Jun 2 05:01:03 EDT 2026 % 0.15/0.34 % CPUTime : % 0.46/0.72 %----Disproving TF0_NAR % 140.07/140.35 --- Run --finite-model-find --sort-inference --uf-ss-fair at 60... % 140.07/140.35 --- Run --mbqi at 45... % 140.07/140.35 --- Run --mbqi --mbqi-enum --mbqi-enum-choice-grammar --mbqi-enum-global-syms-grammar --no-cegqi --no-sygus-inst at 45... % 140.07/140.35 --- Run --full-saturate-quant at 45... % 140.07/140.35 --- Run --finite-model-find --fmf-bound --macros-quant at 60... % 140.07/140.35 % SZS status CounterSatisfiable % 140.07/140.35 % SZS output start Model % 140.07/140.35 ( % 140.07/140.35 ; cardinality of $$unsorted is 1 % 140.07/140.35 ; rep: (as @$$unsorted_0 $$unsorted) % 140.07/140.35 ; cardinality of |tptp.'C_b_c_vec_a_vec_fun$'| is 1 % 140.07/140.35 ; rep: (as |@_tptp.'C_b_c_vec_a_vec_fun$'__0| |tptp.'C_b_c_vec_a_vec_fun$'|) % 140.07/140.35 ; cardinality of |tptp.'B_a_vec_set$'| is 1 % 140.07/140.35 ; rep: (as |@_tptp.'B_a_vec_set$'__0| |tptp.'B_a_vec_set$'|) % 140.07/140.35 ; cardinality of |tptp.'B_d_vec_b_fun$'| is 1 % 140.07/140.35 ; rep: (as |@_tptp.'B_d_vec_b_fun$'__0| |tptp.'B_d_vec_b_fun$'|) % 140.07/140.35 ; cardinality of |tptp.'B_d_vec_bool_fun$'| is 1 % 140.07/140.35 ; rep: (as |@_tptp.'B_d_vec_bool_fun$'__0| |tptp.'B_d_vec_bool_fun$'|) % 140.07/140.35 ; cardinality of |tptp.'B_a_vec_a_vec$'| is 1 % 140.07/140.35 ; rep: (as |@_tptp.'B_a_vec_a_vec$'__0| |tptp.'B_a_vec_a_vec$'|) % 140.07/140.35 ; cardinality of |tptp.'B_c_vec_set$'| is 1 % 140.07/140.35 ; rep: (as |@_tptp.'B_c_vec_set$'__0| |tptp.'B_c_vec_set$'|) % 140.07/140.35 ; cardinality of |tptp.'C_b_d_vec_fun$'| is 1 % 140.07/140.35 ; rep: (as |@_tptp.'C_b_d_vec_fun$'__0| |tptp.'C_b_d_vec_fun$'|) % 140.07/140.35 ; cardinality of |tptp.'B_d_vec_a_vec_c_vec$'| is 1 % 140.07/140.35 ; rep: (as |@_tptp.'B_d_vec_a_vec_c_vec$'__0| |tptp.'B_d_vec_a_vec_c_vec$'|) % 140.07/140.35 ; cardinality of |tptp.'D_b_a_vec_fun$'| is 1 % 140.07/140.35 ; rep: (as |@_tptp.'D_b_a_vec_fun$'__0| |tptp.'D_b_a_vec_fun$'|) % 140.07/140.35 ; cardinality of |tptp.'B_c_vec_a_vec_c_vec$'| is 1 % 140.07/140.35 ; rep: (as |@_tptp.'B_c_vec_a_vec_c_vec$'__0| |tptp.'B_c_vec_a_vec_c_vec$'|) % 140.07/140.35 ; cardinality of |tptp.'A_b_d_vec_bool_fun_fun$'| is 1 % 140.07/140.35 ; rep: (as |@_tptp.'A_b_d_vec_bool_fun_fun$'__0| |tptp.'A_b_d_vec_bool_fun_fun$'|) % 140.07/140.35 ; cardinality of |tptp.'C_b_a_vec_c_vec_fun$'| is 1 % 140.07/140.35 ; rep: (as |@_tptp.'C_b_a_vec_c_vec_fun$'__0| |tptp.'C_b_a_vec_c_vec_fun$'|) % 140.07/140.35 ; cardinality of |tptp.'A_b_fun_set$'| is 1 % 140.07/140.35 ; rep: (as |@_tptp.'A_b_fun_set$'__0| |tptp.'A_b_fun_set$'|) % 140.07/140.35 ; cardinality of |tptp.'B_b_fun$'| is 1 % 140.07/140.35 ; rep: (as |@_tptp.'B_b_fun$'__0| |tptp.'B_b_fun$'|) % 140.07/140.36 ; cardinality of |tptp.'B_b_c_vec_fun$'| is 1 % 140.07/140.36 ; rep: (as |@_tptp.'B_b_c_vec_fun$'__0| |tptp.'B_b_c_vec_fun$'|) % 140.07/140.36 ; cardinality of |tptp.'A_b_a_vec_fun$'| is 1 % 140.07/140.36 ; rep: (as |@_tptp.'A_b_a_vec_fun$'__0| |tptp.'A_b_a_vec_fun$'|) % 140.07/140.36 ; cardinality of |tptp.'C_b_bool_fun_fun$'| is 1 % 140.07/140.36 ; rep: (as |@_tptp.'C_b_bool_fun_fun$'__0| |tptp.'C_b_bool_fun_fun$'|) % 140.07/140.36 ; cardinality of |tptp.'D_b_fun$'| is 1 % 140.07/140.36 ; rep: (as |@_tptp.'D_b_fun$'__0| |tptp.'D_b_fun$'|) % 140.07/140.36 ; cardinality of |tptp.'B_c_vec_bool_fun$'| is 1 % 140.07/140.36 ; rep: (as |@_tptp.'B_c_vec_bool_fun$'__0| |tptp.'B_c_vec_bool_fun$'|) % 140.07/140.36 ; cardinality of |tptp.'A_b_d_vec_a_vec_fun$'| is 1 % 140.07/140.36 ; rep: (as |@_tptp.'A_b_d_vec_a_vec_fun$'__0| |tptp.'A_b_d_vec_a_vec_fun$'|) % 140.07/140.36 ; cardinality of |tptp.'A_b_bool_fun_fun$'| is 1 % 140.07/140.36 ; rep: (as |@_tptp.'A_b_bool_fun_fun$'__0| |tptp.'A_b_bool_fun_fun$'|) % 140.07/140.36 ; cardinality of |tptp.'C_b_a_vec_fun$'| is 1 % 140.07/140.36 ; rep: (as |@_tptp.'C_b_a_vec_fun$'__0| |tptp.'C_b_a_vec_fun$'|) % 140.07/140.36 ; cardinality of |tptp.'C_b_a_vec_fun_set$'| is 1 % 140.07/140.36 ; rep: (as |@_tptp.'C_b_a_vec_fun_set$'__0| |tptp.'C_b_a_vec_fun_set$'|) % 140.07/140.36 ; cardinality of |tptp.'B_a_vec_c_vec_c_vec$'| is 1 % 140.07/140.36 ; rep: (as |@_tptp.'B_a_vec_c_vec_c_vec$'__0| |tptp.'B_a_vec_c_vec_c_vec$'|) % 140.07/140.36 ; cardinality of |tptp.'D$'| is 1 % 140.07/140.36 ; rep: (as |@_tptp.'D$'__0| |tptp.'D$'|) % 140.07/140.36 ; cardinality of |tptp.'C_b_a_vec_fun_bool_fun$'| is 1 % 140.07/140.36 ; rep: (as |@_tptp.'C_b_a_vec_fun_bool_fun$'__0| |tptp.'C_b_a_vec_fun_bool_fun$'|) % 140.07/140.36 ; cardinality of |tptp.'B_c_vec_b_fun$'| is 1 % 140.07/140.36 ; rep: (as |@_tptp.'B_c_vec_b_fun$'__0| |tptp.'B_c_vec_b_fun$'|) % 140.07/140.36 ; cardinality of |tptp.'B_d_vec_d_vec$'| is 1 % 140.07/140.36 ; rep: (as |@_tptp.'B_d_vec_d_vec$'__0| |tptp.'B_d_vec_d_vec$'|) % 140.07/140.36 ; cardinality of |tptp.'C_b_d_vec_a_vec_fun$'| is 1 % 140.07/140.36 ; rep: (as |@_tptp.'C_b_d_vec_a_vec_fun$'__0| |tptp.'C_b_d_vec_a_vec_fun$'|) % 140.07/140.36 ; cardinality of |tptp.'A_b_d_vec_fun_bool_fun$'| is 1 % 140.07/140.36 ; rep: (as |@_tptp.'A_b_d_vec_fun_bool_fun$'__0| |tptp.'A_b_d_vec_fun_bool_fun$'|) % 140.07/140.36 ; cardinality of |tptp.'B_a_vec$'| is 1 % 140.07/140.36 ; rep: (as |@_tptp.'B_a_vec$'__0| |tptp.'B_a_vec$'|) % 140.07/140.36 ; cardinality of |tptp.'B_c_vec_a_vec$'| is 1 % 140.07/140.36 ; rep: (as |@_tptp.'B_c_vec_a_vec$'__0| |tptp.'B_c_vec_a_vec$'|) % 140.07/140.36 ; cardinality of |tptp.'C_b_a_vec_bool_fun_fun$'| is 1 % 140.07/140.36 ; rep: (as |@_tptp.'C_b_a_vec_bool_fun_fun$'__0| |tptp.'C_b_a_vec_bool_fun_fun$'|) % 140.07/140.36 ; cardinality of |tptp.'B$'| is 1 % 140.07/140.36 ; rep: (as |@_tptp.'B$'__0| |tptp.'B$'|) % 140.07/140.36 ; cardinality of |tptp.'B_a_vec_d_vec$'| is 1 % 140.07/140.36 ; rep: (as |@_tptp.'B_a_vec_d_vec$'__0| |tptp.'B_a_vec_d_vec$'|) % 140.07/140.36 ; cardinality of |tptp.'D_b_d_vec_fun$'| is 1 % 140.07/140.36 ; rep: (as |@_tptp.'D_b_d_vec_fun$'__0| |tptp.'D_b_d_vec_fun$'|) % 140.07/140.36 ; cardinality of |tptp.'B_d_vec_d_vec_a_vec$'| is 1 % 140.07/140.36 ; rep: (as |@_tptp.'B_d_vec_d_vec_a_vec$'__0| |tptp.'B_d_vec_d_vec_a_vec$'|) % 140.07/140.36 ; cardinality of |tptp.'C$'| is 1 % 140.07/140.36 ; rep: (as |@_tptp.'C$'__0| |tptp.'C$'|) % 140.07/140.36 ; cardinality of |tptp.'B_c_vec_a_vec_set$'| is 1 % 140.07/140.36 ; rep: (as |@_tptp.'B_c_vec_a_vec_set$'__0| |tptp.'B_c_vec_a_vec_set$'|) % 140.07/140.36 ; cardinality of |tptp.'A_b_c_vec_fun_bool_fun$'| is 1 % 140.07/140.36 ; rep: (as |@_tptp.'A_b_c_vec_fun_bool_fun$'__0| |tptp.'A_b_c_vec_fun_bool_fun$'|) % 140.07/140.36 ; cardinality of |tptp.'D_b_d_vec_bool_fun_fun$'| is 1 % 140.07/140.36 ; rep: (as |@_tptp.'D_b_d_vec_bool_fun_fun$'__0| |tptp.'D_b_d_vec_bool_fun_fun$'|) % 140.07/140.36 ; cardinality of |tptp.'C_b_fun$'| is 1 % 140.07/140.36 ; rep: (as |@_tptp.'C_b_fun$'__0| |tptp.'C_b_fun$'|) % 140.07/140.36 ; cardinality of |tptp.'A_b_a_vec_c_vec_fun$'| is 1 % 140.07/140.36 ; rep: (as |@_tptp.'A_b_a_vec_c_vec_fun$'__0| |tptp.'A_b_a_vec_c_vec_fun$'|) % 140.07/140.36 ; cardinality of |tptp.'C_b_c_vec_fun$'| is 1 % 140.07/140.36 ; rep: (as |@_tptp.'C_b_c_vec_fun$'__0| |tptp.'C_b_c_vec_fun$'|) % 140.07/140.36 ; cardinality of |tptp.'B_a_vec_c_vec$'| is 1 % 140.07/140.36 ; rep: (as |@_tptp.'B_a_vec_c_vec$'__0| |tptp.'B_a_vec_c_vec$'|) % 140.07/140.36 ; cardinality of |tptp.'D_b_d_vec_fun_set$'| is 1 % 140.07/140.36 ; rep: (as |@_tptp.'D_b_d_vec_fun_set$'__0| |tptp.'D_b_d_vec_fun_set$'|) % 140.07/140.36 ; cardinality of |tptp.'B_d_vec_d_vec_d_vec$'| is 1 % 140.07/140.36 ; rep: (as |@_tptp.'B_d_vec_d_vec_d_vec$'__0| |tptp.'B_d_vec_d_vec_d_vec$'|) % 140.07/140.36 ; cardinality of |tptp.'D_b_d_vec_fun_bool_fun$'| is 1 % 140.07/140.36 ; rep: (as |@_tptp.'D_b_d_vec_fun_bool_fun$'__0| |tptp.'D_b_d_vec_fun_bool_fun$'|) % 140.07/140.36 ; cardinality of |tptp.'A_b_d_vec_fun$'| is 1 % 140.07/140.36 ; rep: (as |@_tptp.'A_b_d_vec_fun$'__0| |tptp.'A_b_d_vec_fun$'|) % 140.07/140.36 ; cardinality of |tptp.'D_b_c_vec_fun$'| is 1 % 140.07/140.36 ; rep: (as |@_tptp.'D_b_c_vec_fun$'__0| |tptp.'D_b_c_vec_fun$'|) % 140.07/140.36 ; cardinality of |tptp.'D_b_fun_bool_fun$'| is 1 % 140.07/140.36 ; rep: (as |@_tptp.'D_b_fun_bool_fun$'__0| |tptp.'D_b_fun_bool_fun$'|) % 140.07/140.36 ; cardinality of tptp.tlbool is 2 % 140.07/140.36 ; rep: (as @tptp.tlbool_0 tptp.tlbool) % 140.07/140.36 ; rep: (as @tptp.tlbool_1 tptp.tlbool) % 140.07/140.36 ; cardinality of |tptp.'C_b_fun_set$'| is 1 % 140.07/140.36 ; rep: (as |@_tptp.'C_b_fun_set$'__0| |tptp.'C_b_fun_set$'|) % 140.07/140.36 ; cardinality of |tptp.'B_d_vec_a_vec_set$'| is 1 % 140.07/140.36 ; rep: (as |@_tptp.'B_d_vec_a_vec_set$'__0| |tptp.'B_d_vec_a_vec_set$'|) % 140.07/140.36 ; cardinality of |tptp.'B_d_vec_a_vec_a_vec$'| is 1 % 140.07/140.36 ; rep: (as |@_tptp.'B_d_vec_a_vec_a_vec$'__0| |tptp.'B_d_vec_a_vec_a_vec$'|) % 140.07/140.36 ; cardinality of |tptp.'A_b_c_vec_fun$'| is 2 % 140.07/140.36 ; rep: (as |@_tptp.'A_b_c_vec_fun$'__0| |tptp.'A_b_c_vec_fun$'|) % 140.07/140.36 ; rep: (as |@_tptp.'A_b_c_vec_fun$'__1| |tptp.'A_b_c_vec_fun$'|) % 140.07/140.36 ; cardinality of |tptp.'A_b_c_vec_a_vec_fun$'| is 1 % 140.07/140.36 ; rep: (as |@_tptp.'A_b_c_vec_a_vec_fun$'__0| |tptp.'A_b_c_vec_a_vec_fun$'|) % 140.07/140.36 ; cardinality of |tptp.'B_d_vec_a_vec$'| is 1 % 140.07/140.36 ; rep: (as |@_tptp.'B_d_vec_a_vec$'__0| |tptp.'B_d_vec_a_vec$'|) % 140.07/140.36 ; cardinality of |tptp.'D_b_bool_fun_fun$'| is 1 % 140.07/140.36 ; rep: (as |@_tptp.'D_b_bool_fun_fun$'__0| |tptp.'D_b_bool_fun_fun$'|) % 140.07/140.36 ; cardinality of |tptp.'A_b_c_vec_bool_fun_fun$'| is 1 % 140.07/140.36 ; rep: (as |@_tptp.'A_b_c_vec_bool_fun_fun$'__0| |tptp.'A_b_c_vec_bool_fun_fun$'|) % 140.07/140.36 ; cardinality of |tptp.'B_b_d_vec_fun$'| is 1 % 140.07/140.36 ; rep: (as |@_tptp.'B_b_d_vec_fun$'__0| |tptp.'B_b_d_vec_fun$'|) % 140.07/140.36 ; cardinality of |tptp.'B_d_vec_a_vec_bool_fun$'| is 1 % 140.07/140.36 ; rep: (as |@_tptp.'B_d_vec_a_vec_bool_fun$'__0| |tptp.'B_d_vec_a_vec_bool_fun$'|) % 140.07/140.36 ; cardinality of |tptp.'B_d_vec_c_vec$'| is 1 % 140.07/140.36 ; rep: (as |@_tptp.'B_d_vec_c_vec$'__0| |tptp.'B_d_vec_c_vec$'|) % 140.07/140.36 ; cardinality of |tptp.'A_b_c_vec_a_vec_bool_fun_fun$'| is 1 % 140.07/140.36 ; rep: (as |@_tptp.'A_b_c_vec_a_vec_bool_fun_fun$'__0| |tptp.'A_b_c_vec_a_vec_bool_fun_fun$'|) % 140.07/140.36 ; cardinality of |tptp.'B_c_vec_a_vec_a_vec$'| is 1 % 140.07/140.36 ; rep: (as |@_tptp.'B_c_vec_a_vec_a_vec$'__0| |tptp.'B_c_vec_a_vec_a_vec$'|) % 140.07/140.36 ; cardinality of |tptp.'A_b_fun$'| is 1 % 140.07/140.36 ; rep: (as |@_tptp.'A_b_fun$'__0| |tptp.'A_b_fun$'|) % 140.07/140.36 ; cardinality of |tptp.'B_set$'| is 1 % 140.07/140.36 ; rep: (as |@_tptp.'B_set$'__0| |tptp.'B_set$'|) % 140.07/140.36 ; cardinality of |tptp.'A_b_fun_bool_fun$'| is 1 % 140.07/140.36 ; rep: (as |@_tptp.'A_b_fun_bool_fun$'__0| |tptp.'A_b_fun_bool_fun$'|) % 140.07/140.36 ; cardinality of |tptp.'A$'| is 1 % 140.07/140.36 ; rep: (as |@_tptp.'A$'__0| |tptp.'A$'|) % 140.07/140.36 ; cardinality of |tptp.'D_b_fun_set$'| is 1 % 140.07/140.36 ; rep: (as |@_tptp.'D_b_fun_set$'__0| |tptp.'D_b_fun_set$'|) % 140.07/140.36 ; cardinality of |tptp.'C_b_fun_bool_fun$'| is 1 % 140.07/140.36 ; rep: (as |@_tptp.'C_b_fun_bool_fun$'__0| |tptp.'C_b_fun_bool_fun$'|) % 140.07/140.36 ; cardinality of |tptp.'B_a_vec_b_fun$'| is 1 % 140.07/140.36 ; rep: (as |@_tptp.'B_a_vec_b_fun$'__0| |tptp.'B_a_vec_b_fun$'|) % 140.07/140.36 ; cardinality of |tptp.'B_c_vec_c_vec$'| is 1 % 140.07/140.36 ; rep: (as |@_tptp.'B_c_vec_c_vec$'__0| |tptp.'B_c_vec_c_vec$'|) % 140.07/140.36 ; cardinality of |tptp.'B_a_vec_c_vec_a_vec$'| is 1 % 140.07/140.36 ; rep: (as |@_tptp.'B_a_vec_c_vec_a_vec$'__0| |tptp.'B_a_vec_c_vec_a_vec$'|) % 140.07/140.36 ; cardinality of |tptp.'A_b_c_vec_fun_set$'| is 1 % 140.07/140.36 ; rep: (as |@_tptp.'A_b_c_vec_fun_set$'__0| |tptp.'A_b_c_vec_fun_set$'|) % 140.07/140.36 ; cardinality of |tptp.'B_c_vec_a_vec_a_vec_bool_fun$'| is 1 % 140.07/140.36 ; rep: (as |@_tptp.'B_c_vec_a_vec_a_vec_bool_fun$'__0| |tptp.'B_c_vec_a_vec_a_vec_bool_fun$'|) % 140.07/140.36 ; cardinality of |tptp.'B_d_vec$'| is 1 % 140.07/140.36 ; rep: (as |@_tptp.'B_d_vec$'__0| |tptp.'B_d_vec$'|) % 140.07/140.36 ; cardinality of |tptp.'B_a_vec_bool_fun$'| is 1 % 140.07/140.36 ; rep: (as |@_tptp.'B_a_vec_bool_fun$'__0| |tptp.'B_a_vec_bool_fun$'|) % 140.07/140.36 ; cardinality of |tptp.'B_c_vec_a_vec_bool_fun$'| is 1 % 140.07/140.36 ; rep: (as |@_tptp.'B_c_vec_a_vec_bool_fun$'__0| |tptp.'B_c_vec_a_vec_bool_fun$'|) % 140.07/140.36 ; cardinality of |tptp.'B_c_vec$'| is 1 % 140.07/140.36 ; rep: (as |@_tptp.'B_c_vec$'__0| |tptp.'B_c_vec$'|) % 140.07/140.36 ; cardinality of |tptp.'A_b_c_vec_a_vec_fun_bool_fun$'| is 1 % 140.07/140.36 ; rep: (as |@_tptp.'A_b_c_vec_a_vec_fun_bool_fun$'__0| |tptp.'A_b_c_vec_a_vec_fun_bool_fun$'|) % 140.07/140.36 ; cardinality of |tptp.'B_a_vec_c_vec_bool_fun$'| is 1 % 140.07/140.36 ; rep: (as |@_tptp.'B_a_vec_c_vec_bool_fun$'__0| |tptp.'B_a_vec_c_vec_bool_fun$'|) % 140.07/140.36 ; cardinality of |tptp.'A_b_c_vec_a_vec_fun_set$'| is 1 % 140.07/140.36 ; rep: (as |@_tptp.'A_b_c_vec_a_vec_fun_set$'__0| |tptp.'A_b_c_vec_a_vec_fun_set$'|) % 140.07/140.36 ; cardinality of |tptp.'B_b_a_vec_fun$'| is 1 % 140.07/140.36 ; rep: (as |@_tptp.'B_b_a_vec_fun$'__0| |tptp.'B_b_a_vec_fun$'|) % 140.07/140.36 ; cardinality of |tptp.'B_d_vec_set$'| is 1 % 140.07/140.36 ; rep: (as |@_tptp.'B_d_vec_set$'__0| |tptp.'B_d_vec_set$'|) % 140.07/140.36 ; cardinality of |tptp.'A_b_d_vec_fun_set$'| is 1 % 140.07/140.36 ; rep: (as |@_tptp.'A_b_d_vec_fun_set$'__0| |tptp.'A_b_d_vec_fun_set$'|) % 140.07/140.36 ; cardinality of |tptp.'B_c_vec_d_vec$'| is 1 % 140.07/140.36 ; rep: (as |@_tptp.'B_c_vec_d_vec$'__0| |tptp.'B_c_vec_d_vec$'|) % 140.07/140.36 ; cardinality of |tptp.'B_bool_fun$'| is 1 % 140.07/140.36 ; rep: (as |@_tptp.'B_bool_fun$'__0| |tptp.'B_bool_fun$'|) % 140.07/140.36 (define-fun |tptp.'uminus$h'| ((BOUND_VARIABLE_56919 |tptp.'B_c_vec_a_vec_a_vec$'|)) |tptp.'B_c_vec_a_vec_a_vec$'| (as |@_tptp.'B_c_vec_a_vec_a_vec$'__0| |tptp.'B_c_vec_a_vec_a_vec$'|)) % 140.07/140.36 (define-fun |tptp.'uxq$'| (($x1 |tptp.'B_d_vec$'|) ($x2 |tptp.'D$'|)) |tptp.'C_b_fun$'| (as |@_tptp.'C_b_fun$'__0| |tptp.'C_b_fun$'|)) % 140.07/140.36 (define-fun |tptp.'gauss_Jordan_wrapper$i'| ((BOUND_VARIABLE_56944 |tptp.'C$'|) (BOUND_VARIABLE_56946 |tptp.'C$'|) (BOUND_VARIABLE_56948 |tptp.'B_a_vec_c_vec$'|) (BOUND_VARIABLE_56950 |tptp.'B_c_vec_c_vec$'|)) |tptp.'B_a_vec_c_vec$'| (as |@_tptp.'B_a_vec_c_vec$'__0| |tptp.'B_a_vec_c_vec$'|)) % 140.07/140.36 (define-fun |tptp.'mult_column_row$d'| ((BOUND_VARIABLE_56971 |tptp.'B_d_vec_a_vec$'|) (BOUND_VARIABLE_56973 |tptp.'D$'|) (BOUND_VARIABLE_56975 |tptp.'B$'|)) |tptp.'A_b_d_vec_fun$'| (as |@_tptp.'A_b_d_vec_fun$'__0| |tptp.'A_b_d_vec_fun$'|)) % 140.07/140.36 (define-fun |tptp.'uxd$'| (($x1 |tptp.'D$'|) ($x2 |tptp.'B_d_vec_a_vec$'|)) |tptp.'A_b_fun$'| (as |@_tptp.'A_b_fun$'__0| |tptp.'A_b_fun$'|)) % 140.07/140.36 (define-fun |tptp.'fun_app$z'| (($x1 |tptp.'B_b_c_vec_fun$'|) ($x2 |tptp.'B$'|)) |tptp.'B_c_vec$'| (as |@_tptp.'B_c_vec$'__0| |tptp.'B_c_vec$'|)) % 140.07/140.36 (define-fun |tptp.'uvs$'| (($x1 |tptp.'B_c_vec$'|)) |tptp.'A_b_c_vec_fun$'| (as |@_tptp.'A_b_c_vec_fun$'__1| |tptp.'A_b_c_vec_fun$'|)) % 140.07/140.36 (define-fun |tptp.'uza$'| (($x1 |tptp.'B_d_vec_d_vec$'|) ($x2 |tptp.'D$'|) ($x3 |tptp.'D$'|) ($x4 |tptp.'B$'|)) |tptp.'D_b_d_vec_fun$'| (as |@_tptp.'D_b_d_vec_fun$'__0| |tptp.'D_b_d_vec_fun$'|)) % 140.07/140.36 (define-fun |tptp.'uminus$'| () |tptp.'B_b_fun$'| (as |@_tptp.'B_b_fun$'__0| |tptp.'B_b_fun$'|)) % 140.07/140.36 (define-fun |tptp.'uys$'| (($x1 |tptp.'B_a_vec_c_vec$'|) ($x2 |tptp.'A$'|) ($x3 |tptp.'B$'|)) |tptp.'C_b_a_vec_fun$'| (as |@_tptp.'C_b_a_vec_fun$'__0| |tptp.'C_b_a_vec_fun$'|)) % 140.07/140.36 (define-fun |tptp.'columnvector$d'| ((BOUND_VARIABLE_56985 |tptp.'B_d_vec$'|)) |tptp.'B_a_vec_d_vec$'| (as |@_tptp.'B_a_vec_d_vec$'__0| |tptp.'B_a_vec_d_vec$'|)) % 140.07/140.36 (define-fun |tptp.'vap$'| (($x1 |tptp.'B_a_vec_c_vec$'|) ($x2 |tptp.'A$'|) ($x3 |tptp.'A$'|) ($x4 |tptp.'B$'|)) |tptp.'C_b_a_vec_fun$'| (as |@_tptp.'C_b_a_vec_fun$'__0| |tptp.'C_b_a_vec_fun$'|)) % 140.07/140.36 (define-fun |tptp.'uuf$'| (($x1 |tptp.'D$'|) ($x2 |tptp.'C$'|) ($x3 |tptp.'B_d_vec_d_vec$'|) ($x4 |tptp.'B_c_vec_d_vec$'|)) |tptp.'D_b_d_vec_fun$'| (as |@_tptp.'D_b_d_vec_fun$'__0| |tptp.'D_b_d_vec_fun$'|)) % 140.07/140.36 (define-fun |tptp.'transpose$g'| ((BOUND_VARIABLE_56998 |tptp.'B_a_vec_a_vec$'|)) |tptp.'B_a_vec_a_vec$'| (as |@_tptp.'B_a_vec_a_vec$'__0| |tptp.'B_a_vec_a_vec$'|)) % 140.07/140.36 (define-fun |tptp.'uminus$g'| ((BOUND_VARIABLE_57007 |tptp.'B_a_vec_c_vec$'|)) |tptp.'B_a_vec_c_vec$'| (as |@_tptp.'B_a_vec_c_vec$'__0| |tptp.'B_a_vec_c_vec$'|)) % 140.07/140.36 (define-fun |tptp.'vec_lambda$f'| (($x1 |tptp.'D_b_d_vec_fun$'|)) |tptp.'B_d_vec_d_vec$'| (as |@_tptp.'B_d_vec_d_vec$'__0| |tptp.'B_d_vec_d_vec$'|)) % 140.07/140.36 (define-fun |tptp.'uxw$'| (($x1 |tptp.'B_a_vec$'|) ($x2 |tptp.'A$'|)) |tptp.'A_b_fun$'| (as |@_tptp.'A_b_fun$'__0| |tptp.'A_b_fun$'|)) % 140.07/140.36 (define-fun |tptp.'uug$'| (($x1 |tptp.'D$'|) ($x2 |tptp.'A$'|) ($x3 |tptp.'B_d_vec_d_vec$'|) ($x4 |tptp.'B_a_vec_d_vec$'|)) |tptp.'D_b_d_vec_fun$'| (as |@_tptp.'D_b_d_vec_fun$'__0| |tptp.'D_b_d_vec_fun$'|)) % 140.07/140.36 (define-fun |tptp.'uyh$'| (($x1 |tptp.'B_a_vec_c_vec$'|) ($x2 |tptp.'C$'|) ($x3 |tptp.'C$'|)) |tptp.'C_b_a_vec_fun$'| (as |@_tptp.'C_b_a_vec_fun$'__0| |tptp.'C_b_a_vec_fun$'|)) % 140.07/140.36 (define-fun |tptp.'gauss_Jordan_wrapper$'| ((BOUND_VARIABLE_57031 |tptp.'A$'|) (BOUND_VARIABLE_57033 |tptp.'C$'|) (BOUND_VARIABLE_57035 |tptp.'B_d_vec_a_vec$'|) (BOUND_VARIABLE_57037 |tptp.'B_c_vec_a_vec$'|)) |tptp.'B_d_vec_a_vec$'| (as |@_tptp.'B_d_vec_a_vec$'__0| |tptp.'B_d_vec_a_vec$'|)) % 140.07/140.36 (define-fun |tptp.'member$f'| (($x1 |tptp.'B_c_vec_a_vec$'|) ($x2 |tptp.'B_c_vec_a_vec_set$'|)) Bool false) % 140.07/140.36 (define-fun |tptp.'column_add$a'| ((BOUND_VARIABLE_57061 |tptp.'B_a_vec_c_vec$'|) (BOUND_VARIABLE_57063 |tptp.'A$'|) (BOUND_VARIABLE_57065 |tptp.'A$'|) (BOUND_VARIABLE_57067 |tptp.'B$'|)) |tptp.'B_a_vec_c_vec$'| (as |@_tptp.'B_a_vec_c_vec$'__0| |tptp.'B_a_vec_c_vec$'|)) % 140.07/140.36 (define-fun |tptp.'uww$'| (($x1 |tptp.'B_d_vec_d_vec$'|)) |tptp.'D_b_d_vec_fun$'| (as |@_tptp.'D_b_d_vec_fun$'__0| |tptp.'D_b_d_vec_fun$'|)) % 140.07/140.36 (define-fun |tptp.'fun_app$an'| (($x1 |tptp.'A_b_d_vec_bool_fun_fun$'|) ($x2 |tptp.'A$'|)) |tptp.'B_d_vec_bool_fun$'| (as |@_tptp.'B_d_vec_bool_fun$'__0| |tptp.'B_d_vec_bool_fun$'|)) % 140.07/140.36 (define-fun |tptp.'vaz$'| (($x1 |tptp.'B_d_vec$'|) ($x2 |tptp.'B_d_vec_a_vec$'|)) |tptp.'A_b_d_vec_fun$'| (as |@_tptp.'A_b_d_vec_fun$'__0| |tptp.'A_b_d_vec_fun$'|)) % 140.07/140.36 (define-fun |tptp.'transpose$e'| ((BOUND_VARIABLE_57077 |tptp.'B_d_vec_c_vec$'|)) |tptp.'B_c_vec_d_vec$'| (as |@_tptp.'B_c_vec_d_vec$'__0| |tptp.'B_c_vec_d_vec$'|)) % 140.07/140.36 (define-fun |tptp.'uyb$'| (($x1 |tptp.'B_a_vec$'|)) |tptp.'A_b_d_vec_fun$'| (as |@_tptp.'A_b_d_vec_fun$'__0| |tptp.'A_b_d_vec_fun$'|)) % 140.07/140.36 (define-fun |tptp.'uzh$'| (($x1 |tptp.'B_c_vec_a_vec$'|) ($x2 |tptp.'A$'|) ($x3 |tptp.'A$'|) ($x4 |tptp.'B$'|) ($x5 |tptp.'A$'|)) |tptp.'C_b_fun$'| (as |@_tptp.'C_b_fun$'__0| |tptp.'C_b_fun$'|)) % 140.07/140.36 (define-fun |tptp.'member$'| ((BOUND_VARIABLE_57092 |tptp.'D_b_fun$'|) (BOUND_VARIABLE_57094 |tptp.'D_b_fun_set$'|)) Bool true) % 140.07/140.36 (define-fun |tptp.'plus$i'| (($x1 |tptp.'A_b_d_vec_fun$'|) ($x2 |tptp.'A_b_d_vec_fun$'|)) |tptp.'A_b_d_vec_fun$'| (as |@_tptp.'A_b_d_vec_fun$'__0| |tptp.'A_b_d_vec_fun$'|)) % 140.07/140.36 (define-fun |tptp.'val$'| (($x1 |tptp.'B_a_vec_c_vec$'|) ($x2 |tptp.'A$'|) ($x3 |tptp.'A$'|) ($x4 |tptp.'B$'|) ($x5 |tptp.'C$'|)) |tptp.'A_b_fun$'| (as |@_tptp.'A_b_fun$'__0| |tptp.'A_b_fun$'|)) % 140.07/140.36 (define-fun |tptp.'member$j'| (($x1 |tptp.'C_b_a_vec_fun$'|) ($x2 |tptp.'C_b_a_vec_fun_set$'|)) Bool true) % 140.07/140.36 (define-fun |tptp.'fun_app$at'| (($x1 |tptp.'B_a_vec_c_vec_bool_fun$'|) ($x2 |tptp.'B_a_vec_c_vec$'|)) Bool false) % 140.07/140.36 (define-fun |tptp.'mult_column_row$c'| ((BOUND_VARIABLE_57115 |tptp.'B_c_vec_a_vec$'|) (BOUND_VARIABLE_57117 |tptp.'C$'|) (BOUND_VARIABLE_57119 |tptp.'B$'|)) |tptp.'A_b_c_vec_fun$'| (as |@_tptp.'A_b_c_vec_fun$'__1| |tptp.'A_b_c_vec_fun$'|)) % 140.07/140.36 (define-fun |tptp.'uvw$'| (($x1 |tptp.'B_c_vec_a_vec$'|) ($x2 |tptp.'C$'|) ($x3 |tptp.'C$'|) ($x4 |tptp.'A$'|)) |tptp.'C_b_fun$'| (as |@_tptp.'C_b_fun$'__0| |tptp.'C_b_fun$'|)) % 140.07/140.36 (define-fun |tptp.'vec_nth$e'| (($x1 |tptp.'B_d_vec_c_vec$'|)) |tptp.'C_b_d_vec_fun$'| (as |@_tptp.'C_b_d_vec_fun$'__0| |tptp.'C_b_d_vec_fun$'|)) % 140.07/140.36 (define-fun |tptp.'uuu$'| (($x1 |tptp.'B_b_fun$'|) ($x2 |tptp.'B_c_vec_a_vec$'|) ($x3 |tptp.'A$'|)) |tptp.'C_b_fun$'| (as |@_tptp.'C_b_fun$'__0| |tptp.'C_b_fun$'|)) % 140.07/140.36 (define-fun |tptp.'plus$b'| ((BOUND_VARIABLE_57134 |tptp.'B_c_vec$'|) (BOUND_VARIABLE_57136 |tptp.'B_c_vec$'|)) |tptp.'B_c_vec$'| (as |@_tptp.'B_c_vec$'__0| |tptp.'B_c_vec$'|)) % 140.07/140.36 (define-fun |tptp.'uvh$'| (($x1 |tptp.'B_c_vec_b_fun$'|) ($x2 |tptp.'B_c_vec_a_vec_a_vec$'|)) |tptp.'A_b_a_vec_fun$'| (as |@_tptp.'A_b_a_vec_fun$'__0| |tptp.'A_b_a_vec_fun$'|)) % 140.07/140.36 (define-fun |tptp.'uyw$'| (($x1 |tptp.'B_d_vec_a_vec$'|) ($x2 |tptp.'D$'|) ($x3 |tptp.'B$'|)) |tptp.'A_b_d_vec_fun$'| (as |@_tptp.'A_b_d_vec_fun$'__0| |tptp.'A_b_d_vec_fun$'|)) % 140.07/140.36 (define-fun |tptp.'times$b'| ((BOUND_VARIABLE_57134 |tptp.'B_c_vec$'|) (BOUND_VARIABLE_57136 |tptp.'B_c_vec$'|)) |tptp.'B_c_vec$'| (as |@_tptp.'B_c_vec$'__0| |tptp.'B_c_vec$'|)) % 140.07/140.36 (define-fun |tptp.'row$e'| ((BOUND_VARIABLE_57157 |tptp.'D$'|) (BOUND_VARIABLE_57159 |tptp.'B_a_vec_d_vec$'|)) |tptp.'B_a_vec$'| (as |@_tptp.'B_a_vec$'__0| |tptp.'B_a_vec$'|)) % 140.07/140.36 (define-fun |tptp.'gauss_Jordan_wrapper$f'| ((BOUND_VARIABLE_57184 |tptp.'D$'|) (BOUND_VARIABLE_57186 |tptp.'A$'|) (BOUND_VARIABLE_57188 |tptp.'B_d_vec_d_vec$'|) (BOUND_VARIABLE_57190 |tptp.'B_a_vec_d_vec$'|)) |tptp.'B_d_vec_d_vec$'| (as |@_tptp.'B_d_vec_d_vec$'__0| |tptp.'B_d_vec_d_vec$'|)) % 140.07/140.36 (define-fun |tptp.'elt_set_plus$e'| (($x1 |tptp.'B_d_vec$'|) ($x2 |tptp.'B_d_vec_set$'|)) |tptp.'B_d_vec_set$'| (as |@_tptp.'B_d_vec_set$'__0| |tptp.'B_d_vec_set$'|)) % 140.07/140.36 (define-fun |tptp.'fun_app$ac'| (($x1 |tptp.'A_b_c_vec_a_vec_bool_fun_fun$'|) ($x2 |tptp.'A$'|)) |tptp.'B_c_vec_a_vec_bool_fun$'| (as |@_tptp.'B_c_vec_a_vec_bool_fun$'__0| |tptp.'B_c_vec_a_vec_bool_fun$'|)) % 140.07/140.36 (define-fun |tptp.'map_matrix$i'| ((BOUND_VARIABLE_57204 |tptp.'B_d_vec_b_fun$'|) (BOUND_VARIABLE_57206 |tptp.'B_d_vec_a_vec_c_vec$'|)) |tptp.'B_a_vec_c_vec$'| (as |@_tptp.'B_a_vec_c_vec$'__0| |tptp.'B_a_vec_c_vec$'|)) % 140.07/140.36 (define-fun |tptp.'columnvector$e'| ((BOUND_VARIABLE_57215 |tptp.'B_a_vec$'|)) |tptp.'B_a_vec_a_vec$'| (as |@_tptp.'B_a_vec_a_vec$'__0| |tptp.'B_a_vec_a_vec$'|)) % 140.07/140.36 (define-fun |tptp.'uwd$'| (($x1 |tptp.'B_c_vec_a_vec$'|) ($x2 |tptp.'C$'|)) |tptp.'A_b_fun$'| (as |@_tptp.'A_b_fun$'__0| |tptp.'A_b_fun$'|)) % 140.07/140.36 (define-fun |tptp.'member$c'| (($x1 |tptp.'B$'|) ($x2 |tptp.'B_set$'|)) Bool false) % 140.07/140.36 (define-fun |tptp.'top$'| () |tptp.'A_b_c_vec_a_vec_fun_set$'| (as |@_tptp.'A_b_c_vec_a_vec_fun_set$'__0| |tptp.'A_b_c_vec_a_vec_fun_set$'|)) % 140.07/140.36 (define-fun |tptp.'fun_app$ab'| (($x1 |tptp.'B_c_vec_a_vec_bool_fun$'|) ($x2 |tptp.'B_c_vec_a_vec$'|)) Bool true) % 140.07/140.36 (define-fun |tptp.'uyf$'| (($x1 |tptp.'B_d_vec_a_vec$'|)) |tptp.'A_b_d_vec_a_vec_fun$'| (as |@_tptp.'A_b_d_vec_a_vec_fun$'__0| |tptp.'A_b_d_vec_a_vec_fun$'|)) % 140.07/140.36 (define-fun |tptp.'uxn$'| (($x1 |tptp.'B_a_vec$'|)) |tptp.'A_b_c_vec_fun$'| (as |@_tptp.'A_b_c_vec_fun$'__1| |tptp.'A_b_c_vec_fun$'|)) % 140.07/140.36 (define-fun |tptp.'times$k'| (($x1 |tptp.'D_b_fun$'|) ($x2 |tptp.'D_b_fun$'|)) |tptp.'D_b_fun$'| (as |@_tptp.'D_b_fun$'__0| |tptp.'D_b_fun$'|)) % 140.07/140.36 (define-fun |tptp.'columnvector_row$b'| (($x1 |tptp.'B_d_vec$'|)) |tptp.'D_b_c_vec_fun$'| (as |@_tptp.'D_b_c_vec_fun$'__0| |tptp.'D_b_c_vec_fun$'|)) % 140.07/140.36 (define-fun |tptp.'less_eq$'| (($x1 |tptp.'A_b_d_vec_fun_set$'|) ($x2 |tptp.'A_b_d_vec_fun_set$'|)) Bool true) % 140.07/140.36 (define-fun |tptp.'uyg$'| (($x1 |tptp.'B_d_vec_d_vec$'|) ($x2 |tptp.'D$'|) ($x3 |tptp.'D$'|)) |tptp.'D_b_d_vec_fun$'| (as |@_tptp.'D_b_d_vec_fun$'__0| |tptp.'D_b_d_vec_fun$'|)) % 140.07/140.36 (define-fun |tptp.'vec_nth$o'| (($x1 |tptp.'B_d_vec_a_vec_c_vec$'|) ($x2 |tptp.'C$'|)) |tptp.'B_d_vec_a_vec$'| (as |@_tptp.'B_d_vec_a_vec$'__0| |tptp.'B_d_vec_a_vec$'|)) % 140.07/140.36 (define-fun |tptp.'plus$h'| ((BOUND_VARIABLE_57229 |tptp.'B_d_vec_a_vec$'|) (BOUND_VARIABLE_57231 |tptp.'B_d_vec_a_vec$'|)) |tptp.'B_d_vec_a_vec$'| (as |@_tptp.'B_d_vec_a_vec$'__0| |tptp.'B_d_vec_a_vec$'|)) % 140.07/140.36 (define-fun |tptp.'plus$o'| (($x1 |tptp.'B_set$'|) ($x2 |tptp.'B_set$'|)) |tptp.'B_set$'| (as |@_tptp.'B_set$'__0| |tptp.'B_set$'|)) % 140.07/140.36 (define-fun |tptp.'mult_row$c'| ((BOUND_VARIABLE_57250 |tptp.'B_d_vec_a_vec$'|) (BOUND_VARIABLE_57252 |tptp.'A$'|) (BOUND_VARIABLE_57254 |tptp.'B$'|)) |tptp.'B_d_vec_a_vec$'| (as |@_tptp.'B_d_vec_a_vec$'__0| |tptp.'B_d_vec_a_vec$'|)) % 140.07/140.36 (define-fun |tptp.'vaj$'| (($x1 |tptp.'B_d_vec_d_vec$'|) ($x2 |tptp.'D$'|) ($x3 |tptp.'D$'|) ($x4 |tptp.'B$'|) ($x5 |tptp.'D$'|)) |tptp.'D_b_fun$'| (as |@_tptp.'D_b_fun$'__0| |tptp.'D_b_fun$'|)) % 140.07/140.36 (define-fun |tptp.'mult_row$d'| ((BOUND_VARIABLE_57273 |tptp.'B_c_vec_a_vec$'|) (BOUND_VARIABLE_57275 |tptp.'A$'|) (BOUND_VARIABLE_57277 |tptp.'B$'|)) |tptp.'B_c_vec_a_vec$'| (as |@_tptp.'B_c_vec_a_vec$'__0| |tptp.'B_c_vec_a_vec$'|)) % 140.07/140.36 (define-fun |tptp.'uxa$'| (($x1 |tptp.'B_a_vec_d_vec$'|)) |tptp.'A_b_d_vec_fun$'| (as |@_tptp.'A_b_d_vec_fun$'__0| |tptp.'A_b_d_vec_fun$'|)) % 140.07/140.36 (define-fun |tptp.'plus$k'| (($x1 |tptp.'D_b_fun$'|) ($x2 |tptp.'D_b_fun$'|)) |tptp.'D_b_fun$'| (as |@_tptp.'D_b_fun$'__0| |tptp.'D_b_fun$'|)) % 140.07/140.36 (define-fun |tptp.'uuq$'| (($x1 |tptp.'B_a_vec_c_vec$'|)) |tptp.'C_b_a_vec_fun$'| (as |@_tptp.'C_b_a_vec_fun$'__0| |tptp.'C_b_a_vec_fun$'|)) % 140.07/140.36 (define-fun |tptp.'column$a'| ((BOUND_VARIABLE_57291 |tptp.'D$'|) (BOUND_VARIABLE_57293 |tptp.'B_d_vec_a_vec$'|)) |tptp.'B_a_vec$'| (as |@_tptp.'B_a_vec$'__0| |tptp.'B_a_vec$'|)) % 140.07/140.36 (define-fun |tptp.'uwf$'| (($x1 |tptp.'B_c_vec_a_vec_a_vec$'|) ($x2 |tptp.'A$'|)) |tptp.'A_b_c_vec_fun$'| (as |@_tptp.'A_b_c_vec_fun$'__1| |tptp.'A_b_c_vec_fun$'|)) % 140.07/140.36 (define-fun |tptp.'uminus$j'| ((BOUND_VARIABLE_57302 |tptp.'B_c_vec_d_vec$'|)) |tptp.'B_c_vec_d_vec$'| (as |@_tptp.'B_c_vec_d_vec$'__0| |tptp.'B_c_vec_d_vec$'|)) % 140.07/140.36 (define-fun |tptp.'uus$'| (($x1 |tptp.'B_d_vec_c_vec$'|)) |tptp.'C_b_d_vec_fun$'| (as |@_tptp.'C_b_d_vec_fun$'__0| |tptp.'C_b_d_vec_fun$'|)) % 140.07/140.36 (define-fun |tptp.'uum$'| (($x1 |tptp.'B_c_vec_a_vec$'|)) |tptp.'A_b_c_vec_fun$'| (as |@_tptp.'A_b_c_vec_fun$'__1| |tptp.'A_b_c_vec_fun$'|)) % 140.07/140.36 (define-fun |tptp.'uve$'| (($x1 |tptp.'B_b_d_vec_fun$'|) ($x2 |tptp.'B_a_vec_c_vec$'|) ($x3 |tptp.'C$'|)) |tptp.'A_b_d_vec_fun$'| (as |@_tptp.'A_b_d_vec_fun$'__0| |tptp.'A_b_d_vec_fun$'|)) % 140.07/140.36 (define-fun |tptp.'vec_lambda$l'| (($x1 |tptp.'C_b_d_vec_a_vec_fun$'|)) |tptp.'B_d_vec_a_vec_c_vec$'| (as |@_tptp.'B_d_vec_a_vec_c_vec$'__0| |tptp.'B_d_vec_a_vec_c_vec$'|)) % 140.07/140.36 (define-fun |tptp.'rowvector$b'| ((BOUND_VARIABLE_57311 |tptp.'B_c_vec_a_vec$'|)) |tptp.'B_c_vec_a_vec_a_vec$'| (as |@_tptp.'B_c_vec_a_vec_a_vec$'__0| |tptp.'B_c_vec_a_vec_a_vec$'|)) % 140.07/140.36 (define-fun |tptp.'vec_lambda$j'| (($x1 |tptp.'C_b_c_vec_a_vec_fun$'|)) |tptp.'B_c_vec_a_vec_c_vec$'| (as |@_tptp.'B_c_vec_a_vec_c_vec$'__0| |tptp.'B_c_vec_a_vec_c_vec$'|)) % 140.07/140.36 (define-fun |tptp.'fun_app$as'| (($x1 |tptp.'A_b_fun_bool_fun$'|) ($x2 |tptp.'A_b_fun$'|)) Bool false) % 140.07/140.36 (define-fun |tptp.'uzv$'| (($x1 |tptp.'B_c_vec$'|) ($x2 |tptp.'B_c_vec$'|)) |tptp.'C_b_fun$'| (as |@_tptp.'C_b_fun$'__0| |tptp.'C_b_fun$'|)) % 140.07/140.36 (define-fun |tptp.'member$k'| (($x1 |tptp.'C_b_fun$'|) ($x2 |tptp.'C_b_fun_set$'|)) Bool true) % 140.07/140.36 (define-fun |tptp.'uua$'| (($x1 |tptp.'A$'|) ($x2 |tptp.'C$'|) ($x3 |tptp.'B_d_vec_a_vec$'|) ($x4 |tptp.'B_c_vec_a_vec$'|)) |tptp.'A_b_d_vec_fun$'| (as |@_tptp.'A_b_d_vec_fun$'__0| |tptp.'A_b_d_vec_fun$'|)) % 140.07/140.36 (define-fun |tptp.'fun_app$w'| (($x1 |tptp.'B_c_vec_b_fun$'|) ($x2 |tptp.'B_c_vec$'|)) |tptp.'B$'| (as |@_tptp.'B$'__0| |tptp.'B$'|)) % 140.07/140.36 (define-fun |tptp.'uzb$'| (($x1 |tptp.'B_a_vec_c_vec$'|) ($x2 |tptp.'C$'|) ($x3 |tptp.'C$'|) ($x4 |tptp.'B$'|) ($x5 |tptp.'C$'|)) |tptp.'A_b_fun$'| (as |@_tptp.'A_b_fun$'__0| |tptp.'A_b_fun$'|)) % 140.07/140.36 (define-fun |tptp.'fun_app$ag'| (($x1 |tptp.'C_b_a_vec_bool_fun_fun$'|) ($x2 |tptp.'C$'|)) |tptp.'B_a_vec_bool_fun$'| (as |@_tptp.'B_a_vec_bool_fun$'__0| |tptp.'B_a_vec_bool_fun$'|)) % 140.07/140.36 (define-fun |tptp.'interchange_columns_row$c'| ((BOUND_VARIABLE_57330 |tptp.'B_c_vec_a_vec$'|) (BOUND_VARIABLE_57332 |tptp.'C$'|) (BOUND_VARIABLE_57334 |tptp.'C$'|)) |tptp.'A_b_c_vec_fun$'| (as |@_tptp.'A_b_c_vec_fun$'__1| |tptp.'A_b_c_vec_fun$'|)) % 140.07/140.36 (define-fun |tptp.'column$h'| ((BOUND_VARIABLE_57348 |tptp.'C$'|) (BOUND_VARIABLE_57350 |tptp.'B_a_vec_c_vec_c_vec$'|)) |tptp.'B_a_vec_c_vec$'| (as |@_tptp.'B_a_vec_c_vec$'__0| |tptp.'B_a_vec_c_vec$'|)) % 140.07/140.36 (define-fun |tptp.'columnvector_row$'| (($x1 |tptp.'B_c_vec_a_vec$'|)) |tptp.'A_b_c_vec_a_vec_fun$'| (as |@_tptp.'A_b_c_vec_a_vec_fun$'__0| |tptp.'A_b_c_vec_a_vec_fun$'|)) % 140.07/140.36 (define-fun |tptp.'uuz$'| (($x1 |tptp.'B_b_fun$'|) ($x2 |tptp.'B_d_vec_a_vec$'|)) |tptp.'A_b_d_vec_fun$'| (as |@_tptp.'A_b_d_vec_fun$'__0| |tptp.'A_b_d_vec_fun$'|)) % 140.07/140.36 (define-fun |tptp.'map_matrix$'| ((BOUND_VARIABLE_57364 |tptp.'B_b_fun$'|) (BOUND_VARIABLE_57366 |tptp.'B_c_vec_a_vec$'|)) |tptp.'B_c_vec_a_vec$'| (as |@_tptp.'B_c_vec_a_vec$'__0| |tptp.'B_c_vec_a_vec$'|)) % 140.07/140.36 (define-fun |tptp.'fun_app$r'| (($x1 |tptp.'A_b_fun$'|) ($x2 |tptp.'A$'|)) |tptp.'B$'| (as |@_tptp.'B$'__0| |tptp.'B$'|)) % 140.07/140.36 (define-fun |tptp.'times$m'| (($x1 |tptp.'A_b_c_vec_fun$'|) ($x2 |tptp.'A_b_c_vec_fun$'|)) |tptp.'A_b_c_vec_fun$'| (as |@_tptp.'A_b_c_vec_fun$'__1| |tptp.'A_b_c_vec_fun$'|)) % 140.07/140.36 (define-fun |tptp.'interchange_columns_row$'| ((BOUND_VARIABLE_57386 |tptp.'B_d_vec_d_vec$'|) (BOUND_VARIABLE_57388 |tptp.'D$'|) (BOUND_VARIABLE_57390 |tptp.'D$'|)) |tptp.'D_b_d_vec_fun$'| (as |@_tptp.'D_b_d_vec_fun$'__0| |tptp.'D_b_d_vec_fun$'|)) % 140.07/140.36 (define-fun |tptp.'vec_nth$p'| (($x1 |tptp.'B_c_vec_a_vec_c_vec$'|) ($x2 |tptp.'C$'|)) |tptp.'B_c_vec_a_vec$'| (as |@_tptp.'B_c_vec_a_vec$'__0| |tptp.'B_c_vec_a_vec$'|)) % 140.07/140.36 (define-fun |tptp.'interchange_rows$e'| ((BOUND_VARIABLE_57411 |tptp.'B_a_vec_d_vec$'|) (BOUND_VARIABLE_57413 |tptp.'D$'|) (BOUND_VARIABLE_57415 |tptp.'D$'|)) |tptp.'B_a_vec_d_vec$'| (as |@_tptp.'B_a_vec_d_vec$'__0| |tptp.'B_a_vec_d_vec$'|)) % 140.07/140.36 (define-fun |tptp.'vec_lambda$b'| (($x1 |tptp.'D_b_fun$'|)) |tptp.'B_d_vec$'| (as |@_tptp.'B_d_vec$'__0| |tptp.'B_d_vec$'|)) % 140.07/140.36 (define-fun |tptp.'columns$c'| ((BOUND_VARIABLE_57425 |tptp.'B_c_vec_a_vec$'|)) |tptp.'B_a_vec_set$'| (as |@_tptp.'B_a_vec_set$'__0| |tptp.'B_a_vec_set$'|)) % 140.07/140.36 (define-fun |tptp.'plus$d'| (($x1 |tptp.'B$'|)) |tptp.'B_b_fun$'| (as |@_tptp.'B_b_fun$'__0| |tptp.'B_b_fun$'|)) % 140.07/140.36 (define-fun |tptp.'uuw$'| (($x1 |tptp.'B_b_fun$'|) ($x2 |tptp.'B_a_vec_c_vec$'|) ($x3 |tptp.'C$'|)) |tptp.'A_b_fun$'| (as |@_tptp.'A_b_fun$'__0| |tptp.'A_b_fun$'|)) % 140.07/140.36 (define-fun |tptp.'fun_app$n'| (($x1 |tptp.'A_b_c_vec_a_vec_fun$'|) ($x2 |tptp.'A$'|)) |tptp.'B_c_vec_a_vec$'| (as |@_tptp.'B_c_vec_a_vec$'__0| |tptp.'B_c_vec_a_vec$'|)) % 140.07/140.36 (define-fun |tptp.'uzx$'| (($x1 |tptp.'B_a_vec$'|) ($x2 |tptp.'B_a_vec$'|)) |tptp.'A_b_fun$'| (as |@_tptp.'A_b_fun$'__0| |tptp.'A_b_fun$'|)) % 140.07/140.36 (define-fun |tptp.'fun_app$u'| (($x1 |tptp.'C_b_c_vec_a_vec_fun$'|) ($x2 |tptp.'C$'|)) |tptp.'B_c_vec_a_vec$'| (as |@_tptp.'B_c_vec_a_vec$'__0| |tptp.'B_c_vec_a_vec$'|)) % 140.07/140.36 (define-fun |tptp.'top$e'| () |tptp.'A_b_c_vec_fun_set$'| (as |@_tptp.'A_b_c_vec_fun_set$'__0| |tptp.'A_b_c_vec_fun_set$'|)) % 140.07/140.36 (define-fun |tptp.'vah$'| (($x1 |tptp.'B_d_vec_a_vec$'|) ($x2 |tptp.'B_d_vec_a_vec$'|)) |tptp.'A_b_d_vec_fun$'| (as |@_tptp.'A_b_d_vec_fun$'__0| |tptp.'A_b_d_vec_fun$'|)) % 140.07/140.36 (define-fun |tptp.'fun_app$am'| (($x1 |tptp.'D_b_bool_fun_fun$'|) ($x2 |tptp.'D$'|)) |tptp.'B_bool_fun$'| (as |@_tptp.'B_bool_fun$'__0| |tptp.'B_bool_fun$'|)) % 140.07/140.36 (define-fun |tptp.'map_matrix$n'| (($x1 |tptp.'B_b_d_vec_fun$'|) ($x2 |tptp.'B_d_vec_a_vec$'|)) |tptp.'B_d_vec_d_vec_a_vec$'| (as |@_tptp.'B_d_vec_d_vec_a_vec$'__0| |tptp.'B_d_vec_d_vec_a_vec$'|)) % 140.07/140.36 (define-fun |tptp.'uminus$e'| ((BOUND_VARIABLE_57432 |tptp.'B_d_vec_a_vec$'|)) |tptp.'B_d_vec_a_vec$'| (as |@_tptp.'B_d_vec_a_vec$'__0| |tptp.'B_d_vec_a_vec$'|)) % 140.07/140.36 (define-fun |tptp.'column$e'| ((BOUND_VARIABLE_57446 |tptp.'C$'|) (BOUND_VARIABLE_57448 |tptp.'B_c_vec_c_vec$'|)) |tptp.'B_c_vec$'| (as |@_tptp.'B_c_vec$'__0| |tptp.'B_c_vec$'|)) % 140.07/140.36 (define-fun |tptp.'vbh$'| (($x1 |tptp.'B_c_vec$'|)) |tptp.'A_b_c_vec_fun$'| (as |@_tptp.'A_b_c_vec_fun$'__1| |tptp.'A_b_c_vec_fun$'|)) % 140.07/140.36 (define-fun |tptp.'uwy$'| (($x1 |tptp.'B_c_vec_c_vec$'|)) |tptp.'C_b_c_vec_fun$'| (as |@_tptp.'C_b_c_vec_fun$'__0| |tptp.'C_b_c_vec_fun$'|)) % 140.07/140.36 (define-fun |tptp.'member$a'| ((BOUND_VARIABLE_57463 |tptp.'A_b_d_vec_fun$'|) (BOUND_VARIABLE_57465 |tptp.'A_b_d_vec_fun_set$'|)) Bool true) % 140.07/140.36 (define-fun |tptp.'uvb$'| (($x1 |tptp.'B_b_c_vec_fun$'|) ($x2 |tptp.'B_a_vec_c_vec$'|)) |tptp.'C_b_c_vec_a_vec_fun$'| (as |@_tptp.'C_b_c_vec_a_vec_fun$'__0| |tptp.'C_b_c_vec_a_vec_fun$'|)) % 140.07/140.36 (define-fun |tptp.'uxz$'| (($x1 |tptp.'B_c_vec$'|)) |tptp.'C_b_a_vec_fun$'| (as |@_tptp.'C_b_a_vec_fun$'__0| |tptp.'C_b_a_vec_fun$'|)) % 140.07/140.36 (define-fun |tptp.'mult_row_row$d'| ((BOUND_VARIABLE_57482 |tptp.'B_d_vec_a_vec$'|) (BOUND_VARIABLE_57484 |tptp.'A$'|) (BOUND_VARIABLE_57486 |tptp.'B$'|)) |tptp.'A_b_d_vec_fun$'| (as |@_tptp.'A_b_d_vec_fun$'__0| |tptp.'A_b_d_vec_fun$'|)) % 140.07/140.36 (define-fun |tptp.'row_add_row$d'| ((BOUND_VARIABLE_57510 |tptp.'B_d_vec_a_vec$'|) (BOUND_VARIABLE_57512 |tptp.'A$'|) (BOUND_VARIABLE_57514 |tptp.'A$'|) (BOUND_VARIABLE_57516 |tptp.'B$'|)) |tptp.'A_b_d_vec_fun$'| (as |@_tptp.'A_b_d_vec_fun$'__0| |tptp.'A_b_d_vec_fun$'|)) % 140.07/140.36 (define-fun |tptp.'interchange_columns$b'| ((BOUND_VARIABLE_57535 |tptp.'B_c_vec_a_vec_a_vec$'|) (BOUND_VARIABLE_57537 |tptp.'A$'|) (BOUND_VARIABLE_57539 |tptp.'A$'|)) |tptp.'B_c_vec_a_vec_a_vec$'| (as |@_tptp.'B_c_vec_a_vec_a_vec$'__0| |tptp.'B_c_vec_a_vec_a_vec$'|)) % 140.07/140.36 (define-fun |tptp.'vam$'| (($x1 |tptp.'B_c_vec_a_vec$'|) ($x2 |tptp.'C$'|) ($x3 |tptp.'C$'|) ($x4 |tptp.'B$'|) ($x5 |tptp.'A$'|)) |tptp.'C_b_fun$'| (as |@_tptp.'C_b_fun$'__0| |tptp.'C_b_fun$'|)) % 140.07/140.36 (define-fun |tptp.'uwu$'| (($x1 |tptp.'B_a_vec_c_vec$'|)) |tptp.'A_b_c_vec_fun$'| (as |@_tptp.'A_b_c_vec_fun$'__0| |tptp.'A_b_c_vec_fun$'|)) % 140.07/140.36 (define-fun |tptp.'elt_set_plus$'| (($x1 |tptp.'A_b_d_vec_fun$'|) ($x2 |tptp.'A_b_d_vec_fun_set$'|)) |tptp.'A_b_d_vec_fun_set$'| (as |@_tptp.'A_b_d_vec_fun_set$'__0| |tptp.'A_b_d_vec_fun_set$'|)) % 140.07/140.36 (define-fun |tptp.'transpose_row$d'| ((BOUND_VARIABLE_57548 |tptp.'B_a_vec_d_vec$'|)) |tptp.'A_b_d_vec_fun$'| (as |@_tptp.'A_b_d_vec_fun$'__0| |tptp.'A_b_d_vec_fun$'|)) % 140.07/140.36 (define-fun |tptp.'uup$'| (($x1 |tptp.'B_d_vec_d_vec$'|)) |tptp.'D_b_d_vec_fun$'| (as |@_tptp.'D_b_d_vec_fun$'__0| |tptp.'D_b_d_vec_fun$'|)) % 140.07/140.36 (define-fun |tptp.'i$'| () |tptp.'A$'| (as |@_tptp.'A$'__0| |tptp.'A$'|)) % 140.07/140.36 (define-fun |tptp.'uwa$'| (($x1 |tptp.'B_a_vec_c_vec$'|) ($x2 |tptp.'C$'|) ($x3 |tptp.'C$'|) ($x4 |tptp.'C$'|)) |tptp.'A_b_fun$'| (as |@_tptp.'A_b_fun$'__0| |tptp.'A_b_fun$'|)) % 140.07/140.36 (define-fun |tptp.'plus$'| ((BOUND_VARIABLE_57560 |tptp.'B_c_vec_a_vec$'|) (BOUND_VARIABLE_57562 |tptp.'B_c_vec_a_vec$'|)) |tptp.'B_c_vec_a_vec$'| (as |@_tptp.'B_c_vec_a_vec$'__0| |tptp.'B_c_vec_a_vec$'|)) % 140.07/140.36 (define-fun |tptp.'vat$'| (($x1 |tptp.'B_d_vec$'|) ($x2 |tptp.'B_d_vec_d_vec$'|)) |tptp.'D_b_d_vec_fun$'| (as |@_tptp.'D_b_d_vec_fun$'__0| |tptp.'D_b_d_vec_fun$'|)) % 140.07/140.36 (define-fun |tptp.'transpose_row$f'| ((BOUND_VARIABLE_57576 |tptp.'B_c_vec_c_vec$'|) (BOUND_VARIABLE_57578 |tptp.'C$'|)) |tptp.'B_c_vec$'| (as |@_tptp.'B_c_vec$'__0| |tptp.'B_c_vec$'|)) % 140.07/140.36 (define-fun |tptp.'row$'| ((BOUND_VARIABLE_57595 |tptp.'D$'|) (BOUND_VARIABLE_57597 |tptp.'B_d_vec_d_vec$'|)) |tptp.'B_d_vec$'| (as |@_tptp.'B_d_vec$'__0| |tptp.'B_d_vec$'|)) % 140.07/140.36 (define-fun |tptp.'fun_app$'| (($x1 |tptp.'A_b_c_vec_fun$'|) ($x2 |tptp.'A$'|)) |tptp.'B_c_vec$'| (as |@_tptp.'B_c_vec$'__0| |tptp.'B_c_vec$'|)) % 140.07/140.36 (define-fun |tptp.'gauss_Jordan_wrapper$e'| ((BOUND_VARIABLE_57621 |tptp.'D$'|) (BOUND_VARIABLE_57623 |tptp.'C$'|) (BOUND_VARIABLE_57625 |tptp.'B_d_vec_d_vec$'|) (BOUND_VARIABLE_57627 |tptp.'B_c_vec_d_vec$'|)) |tptp.'B_d_vec_d_vec$'| (as |@_tptp.'B_d_vec_d_vec$'__0| |tptp.'B_d_vec_d_vec$'|)) % 140.07/140.36 (define-fun |tptp.'uul$'| (($x1 |tptp.'B_d_vec_a_vec$'|)) |tptp.'A_b_d_vec_fun$'| (as |@_tptp.'A_b_d_vec_fun$'__0| |tptp.'A_b_d_vec_fun$'|)) % 140.07/140.36 (define-fun |tptp.'columnvector$i'| ((BOUND_VARIABLE_57640 |tptp.'B_d_vec_a_vec$'|)) |tptp.'B_d_vec_a_vec_a_vec$'| (as |@_tptp.'B_d_vec_a_vec_a_vec$'__0| |tptp.'B_d_vec_a_vec_a_vec$'|)) % 140.07/140.36 (define-fun |tptp.'uwm$'| (($x1 |tptp.'B_a_vec_c_vec_c_vec$'|) ($x2 |tptp.'C$'|)) |tptp.'C_b_a_vec_fun$'| (as |@_tptp.'C_b_a_vec_fun$'__0| |tptp.'C_b_a_vec_fun$'|)) % 140.07/140.36 (define-fun |tptp.'column_add$c'| ((BOUND_VARIABLE_57662 |tptp.'B_d_vec_a_vec$'|) (BOUND_VARIABLE_57664 |tptp.'D$'|) (BOUND_VARIABLE_57666 |tptp.'D$'|) (BOUND_VARIABLE_57668 |tptp.'B$'|)) |tptp.'B_d_vec_a_vec$'| (as |@_tptp.'B_d_vec_a_vec$'__0| |tptp.'B_d_vec_a_vec$'|)) % 140.07/140.36 (define-fun |tptp.'uun$'| (($x1 |tptp.'B_c_vec$'|)) |tptp.'C_b_fun$'| (as |@_tptp.'C_b_fun$'__0| |tptp.'C_b_fun$'|)) % 140.07/140.36 (define-fun |tptp.'mult_column$d'| ((BOUND_VARIABLE_57685 |tptp.'B_c_vec_a_vec$'|) (BOUND_VARIABLE_57687 |tptp.'C$'|) (BOUND_VARIABLE_57689 |tptp.'B$'|)) |tptp.'B_c_vec_a_vec$'| (as |@_tptp.'B_c_vec_a_vec$'__0| |tptp.'B_c_vec_a_vec$'|)) % 140.07/140.36 (define-fun |tptp.'collect$b'| (($x1 |tptp.'A_b_c_vec_fun_bool_fun$'|)) |tptp.'A_b_c_vec_fun_set$'| (as |@_tptp.'A_b_c_vec_fun_set$'__0| |tptp.'A_b_c_vec_fun_set$'|)) % 140.07/140.36 (define-fun |tptp.'plus$c'| ((BOUND_VARIABLE_57703 |tptp.'B_a_vec$'|) (BOUND_VARIABLE_57705 |tptp.'B_a_vec$'|)) |tptp.'B_a_vec$'| (as |@_tptp.'B_a_vec$'__0| |tptp.'B_a_vec$'|)) % 140.07/140.36 (define-fun |tptp.'top$a'| () |tptp.'D_b_d_vec_fun_set$'| (as |@_tptp.'D_b_d_vec_fun_set$'__0| |tptp.'D_b_d_vec_fun_set$'|)) % 140.07/140.36 (define-fun |tptp.'uvo$'| (($x1 |tptp.'B_a_vec$'|)) |tptp.'A_b_a_vec_fun$'| (as |@_tptp.'A_b_a_vec_fun$'__0| |tptp.'A_b_a_vec_fun$'|)) % 140.07/140.36 (define-fun |tptp.'plus$p'| (($x1 |tptp.'B_d_vec_a_vec_set$'|) ($x2 |tptp.'B_d_vec_a_vec_set$'|)) |tptp.'B_d_vec_a_vec_set$'| (as |@_tptp.'B_d_vec_a_vec_set$'__0| |tptp.'B_d_vec_a_vec_set$'|)) % 140.07/140.36 (define-fun |tptp.'interchange_rows$c'| (($x1 |tptp.'B_d_vec_a_vec$'|) ($x2 |tptp.'A$'|)) |tptp.'A_b_d_vec_a_vec_fun$'| (as |@_tptp.'A_b_d_vec_a_vec_fun$'__0| |tptp.'A_b_d_vec_a_vec_fun$'|)) % 140.07/140.36 (define-fun |tptp.'plus$j'| (($x1 |tptp.'A_b_d_vec_fun_set$'|) ($x2 |tptp.'A_b_d_vec_fun_set$'|)) |tptp.'A_b_d_vec_fun_set$'| (as |@_tptp.'A_b_d_vec_fun_set$'__0| |tptp.'A_b_d_vec_fun_set$'|)) % 140.07/140.36 (define-fun |tptp.'vav$'| (($x1 |tptp.'B$'|) ($x2 |tptp.'B_c_vec$'|)) |tptp.'C_b_fun$'| (as |@_tptp.'C_b_fun$'__0| |tptp.'C_b_fun$'|)) % 140.07/140.36 (define-fun |tptp.'uxo$'| (($x1 |tptp.'B_c_vec_a_vec$'|) ($x2 |tptp.'A$'|)) |tptp.'A_b_c_vec_fun$'| (as |@_tptp.'A_b_c_vec_fun$'__1| |tptp.'A_b_c_vec_fun$'|)) % 140.07/140.36 (define-fun |tptp.'elt_set_plus$c'| (($x1 |tptp.'B$'|) ($x2 |tptp.'B_set$'|)) |tptp.'B_set$'| (as |@_tptp.'B_set$'__0| |tptp.'B_set$'|)) % 140.07/140.36 (define-fun |tptp.'map_matrix$j'| (($x1 |tptp.'B_b_fun$'|) ($x2 |tptp.'B_d_vec_d_vec$'|)) |tptp.'B_d_vec_d_vec$'| (as |@_tptp.'B_d_vec_d_vec$'__0| |tptp.'B_d_vec_d_vec$'|)) % 140.07/140.36 (define-fun |tptp.'plus$q'| (($x1 |tptp.'B_d_vec_set$'|) ($x2 |tptp.'B_d_vec_set$'|)) |tptp.'B_d_vec_set$'| (as |@_tptp.'B_d_vec_set$'__0| |tptp.'B_d_vec_set$'|)) % 140.07/140.36 (define-fun |tptp.'uzg$'| (($x1 |tptp.'B_d_vec_a_vec$'|) ($x2 |tptp.'A$'|) ($x3 |tptp.'A$'|) ($x4 |tptp.'B$'|)) |tptp.'A_b_d_vec_fun$'| (as |@_tptp.'A_b_d_vec_fun$'__0| |tptp.'A_b_d_vec_fun$'|)) % 140.07/140.36 (define-fun |tptp.'vec$f'| ((BOUND_VARIABLE_57714 |tptp.'B_a_vec$'|)) |tptp.'B_a_vec_c_vec$'| (as |@_tptp.'B_a_vec_c_vec$'__0| |tptp.'B_a_vec_c_vec$'|)) % 140.07/140.36 (define-fun |tptp.'uminus$i'| ((BOUND_VARIABLE_57724 |tptp.'B_d_vec_c_vec$'|)) |tptp.'B_d_vec_c_vec$'| (as |@_tptp.'B_d_vec_c_vec$'__0| |tptp.'B_d_vec_c_vec$'|)) % 140.07/140.36 (define-fun |tptp.'transpose_row$'| ((BOUND_VARIABLE_57734 |tptp.'B_c_vec_a_vec$'|)) |tptp.'C_b_a_vec_fun$'| (as |@_tptp.'C_b_a_vec_fun$'__0| |tptp.'C_b_a_vec_fun$'|)) % 140.07/140.36 (define-fun |tptp.'vec_lambda$m'| ((_arg_1 |tptp.'A_b_a_vec_fun$'|)) |tptp.'B_a_vec_a_vec$'| (as |@_tptp.'B_a_vec_a_vec$'__0| |tptp.'B_a_vec_a_vec$'|)) % 140.07/140.36 (define-fun |tptp.'uzr$'| (($x1 |tptp.'B_c_vec_a_vec$'|) ($x2 |tptp.'A$'|) ($x3 |tptp.'B$'|) ($x4 |tptp.'A$'|)) |tptp.'C_b_fun$'| (as |@_tptp.'C_b_fun$'__0| |tptp.'C_b_fun$'|)) % 140.07/140.36 (define-fun |tptp.'columnvector_row$h'| ((BOUND_VARIABLE_57748 |tptp.'B_a_vec_c_vec$'|) (BOUND_VARIABLE_57750 |tptp.'C$'|)) |tptp.'B_a_vec_c_vec$'| (as |@_tptp.'B_a_vec_c_vec$'__0| |tptp.'B_a_vec_c_vec$'|)) % 140.07/140.36 (define-fun |tptp.'vae$'| (($x1 |tptp.'B_c_vec_a_vec_a_vec$'|) ($x2 |tptp.'B_c_vec_a_vec_a_vec$'|)) |tptp.'A_b_c_vec_a_vec_fun$'| (as |@_tptp.'A_b_c_vec_a_vec_fun$'__0| |tptp.'A_b_c_vec_a_vec_fun$'|)) % 140.07/140.36 (define-fun |tptp.'column$i'| ((BOUND_VARIABLE_57764 |tptp.'A$'|) (BOUND_VARIABLE_57766 |tptp.'B_d_vec_a_vec_a_vec$'|)) |tptp.'B_d_vec_a_vec$'| (as |@_tptp.'B_d_vec_a_vec$'__0| |tptp.'B_d_vec_a_vec$'|)) % 140.07/140.36 (define-fun |tptp.'uzm$'| (($x1 |tptp.'B_a_vec_c_vec$'|) ($x2 |tptp.'C$'|) ($x3 |tptp.'B$'|)) |tptp.'C_b_a_vec_fun$'| (as |@_tptp.'C_b_a_vec_fun$'__0| |tptp.'C_b_a_vec_fun$'|)) % 140.07/140.36 (define-fun |tptp.'uzk$'| (($x1 |tptp.'B_d_vec_d_vec$'|) ($x2 |tptp.'D$'|) ($x3 |tptp.'B$'|)) |tptp.'D_b_d_vec_fun$'| (as |@_tptp.'D_b_d_vec_fun$'__0| |tptp.'D_b_d_vec_fun$'|)) % 140.07/140.36 (define-fun |tptp.'mult_column$a'| ((BOUND_VARIABLE_57781 |tptp.'B_a_vec_c_vec$'|) (BOUND_VARIABLE_57783 |tptp.'A$'|) (BOUND_VARIABLE_57785 |tptp.'B$'|)) |tptp.'B_a_vec_c_vec$'| (as |@_tptp.'B_a_vec_c_vec$'__0| |tptp.'B_a_vec_c_vec$'|)) % 140.07/140.36 (define-fun |tptp.'mult_column$c'| ((BOUND_VARIABLE_57800 |tptp.'B_d_vec_a_vec$'|) (BOUND_VARIABLE_57802 |tptp.'D$'|) (BOUND_VARIABLE_57804 |tptp.'B$'|)) |tptp.'B_d_vec_a_vec$'| (as |@_tptp.'B_d_vec_a_vec$'__0| |tptp.'B_d_vec_a_vec$'|)) % 140.07/140.36 (define-fun |tptp.'uvt$'| (($x1 |tptp.'B_d_vec_d_vec$'|) ($x2 |tptp.'D$'|) ($x3 |tptp.'D$'|) ($x4 |tptp.'D$'|)) |tptp.'D_b_fun$'| (as |@_tptp.'D_b_fun$'__0| |tptp.'D_b_fun$'|)) % 140.07/140.36 (define-fun |tptp.'plus$g'| ((BOUND_VARIABLE_57816 |tptp.'B_a_vec_c_vec$'|) (BOUND_VARIABLE_57818 |tptp.'B_a_vec_c_vec$'|)) |tptp.'B_a_vec_c_vec$'| (as |@_tptp.'B_a_vec_c_vec$'__0| |tptp.'B_a_vec_c_vec$'|)) % 140.07/140.36 (define-fun |tptp.'less_eq$a'| (($x1 |tptp.'D_b_fun_set$'|) ($x2 |tptp.'D_b_fun_set$'|)) Bool true) % 140.07/140.36 (define-fun |tptp.'uyi$'| (($x1 |tptp.'B_c_vec_a_vec_a_vec$'|) ($x2 |tptp.'A$'|) ($x3 |tptp.'A$'|)) |tptp.'A_b_c_vec_a_vec_fun$'| (as |@_tptp.'A_b_c_vec_a_vec_fun$'__0| |tptp.'A_b_c_vec_a_vec_fun$'|)) % 140.07/140.36 (define-fun |tptp.'plus$r'| (($x1 |tptp.'B_c_vec_a_vec_set$'|) ($x2 |tptp.'B_c_vec_a_vec_set$'|)) |tptp.'B_c_vec_a_vec_set$'| (as |@_tptp.'B_c_vec_a_vec_set$'__0| |tptp.'B_c_vec_a_vec_set$'|)) % 140.07/140.36 (define-fun |tptp.'columns$b'| ((BOUND_VARIABLE_57828 |tptp.'B_d_vec_a_vec$'|)) |tptp.'B_a_vec_set$'| (as |@_tptp.'B_a_vec_set$'__0| |tptp.'B_a_vec_set$'|)) % 140.07/140.36 (define-fun |tptp.'column_add_row$c'| ((BOUND_VARIABLE_57848 |tptp.'B_c_vec_a_vec$'|) (BOUND_VARIABLE_57850 |tptp.'C$'|) (BOUND_VARIABLE_57852 |tptp.'C$'|) (BOUND_VARIABLE_57854 |tptp.'B$'|)) |tptp.'A_b_c_vec_fun$'| (as |@_tptp.'A_b_c_vec_fun$'__1| |tptp.'A_b_c_vec_fun$'|)) % 140.07/140.36 (define-fun |tptp.'fun_app$ao'| (($x1 |tptp.'A_b_c_vec_a_vec_fun_bool_fun$'|) ($x2 |tptp.'A_b_c_vec_a_vec_fun$'|)) Bool false) % 140.07/140.36 (define-fun |tptp.'elt_set_plus$a'| (($x1 |tptp.'D_b_fun$'|) ($x2 |tptp.'D_b_fun_set$'|)) |tptp.'D_b_fun_set$'| (as |@_tptp.'D_b_fun_set$'__0| |tptp.'D_b_fun_set$'|)) % 140.07/140.36 (define-fun |tptp.'mult_column$b'| ((BOUND_VARIABLE_57873 |tptp.'B_c_vec_a_vec_a_vec$'|) (BOUND_VARIABLE_57875 |tptp.'A$'|) (BOUND_VARIABLE_57877 |tptp.'B_c_vec$'|)) |tptp.'B_c_vec_a_vec_a_vec$'| (as |@_tptp.'B_c_vec_a_vec_a_vec$'__0| |tptp.'B_c_vec_a_vec_a_vec$'|)) % 140.07/140.36 (define-fun |tptp.'fun_app$h'| (($x1 |tptp.'C_b_a_vec_c_vec_fun$'|) ($x2 |tptp.'C$'|)) |tptp.'B_a_vec_c_vec$'| (as |@_tptp.'B_a_vec_c_vec$'__0| |tptp.'B_a_vec_c_vec$'|)) % 140.07/140.36 (define-fun |tptp.'fun_app$ap'| (($x1 |tptp.'D_b_d_vec_fun_bool_fun$'|) ($x2 |tptp.'D_b_d_vec_fun$'|)) Bool false) % 140.07/140.36 (define-fun |tptp.'vec_lambda$k'| ((_arg_1 |tptp.'A_b_a_vec_c_vec_fun$'|)) |tptp.'B_a_vec_c_vec_a_vec$'| (as |@_tptp.'B_a_vec_c_vec_a_vec$'__0| |tptp.'B_a_vec_c_vec_a_vec$'|)) % 140.07/140.36 (define-fun |tptp.'uxv$'| (($x1 |tptp.'B_d_vec$'|)) |tptp.'D_b_a_vec_fun$'| (as |@_tptp.'D_b_a_vec_fun$'__0| |tptp.'D_b_a_vec_fun$'|)) % 140.07/140.36 (define-fun |tptp.'times$'| ((BOUND_VARIABLE_57560 |tptp.'B_c_vec_a_vec$'|) (BOUND_VARIABLE_57562 |tptp.'B_c_vec_a_vec$'|)) |tptp.'B_c_vec_a_vec$'| (as |@_tptp.'B_c_vec_a_vec$'__0| |tptp.'B_c_vec_a_vec$'|)) % 140.07/140.36 (define-fun |tptp.'transpose_row$b'| ((BOUND_VARIABLE_57896 |tptp.'B_c_vec_a_vec_a_vec$'|)) |tptp.'A_b_c_vec_a_vec_fun$'| (as |@_tptp.'A_b_c_vec_a_vec_fun$'__0| |tptp.'A_b_c_vec_a_vec_fun$'|)) % 140.07/140.36 (define-fun |tptp.'gauss_Jordan_wrapper$g'| ((BOUND_VARIABLE_57920 |tptp.'A$'|) (BOUND_VARIABLE_57922 |tptp.'A$'|) (BOUND_VARIABLE_57924 |tptp.'B_c_vec_a_vec$'|) (BOUND_VARIABLE_57926 |tptp.'B_a_vec_a_vec$'|)) |tptp.'B_c_vec_a_vec$'| (as |@_tptp.'B_c_vec_a_vec$'__0| |tptp.'B_c_vec_a_vec$'|)) % 140.07/140.36 (define-fun |tptp.'elt_set_times$e'| (($x1 |tptp.'B_d_vec$'|) ($x2 |tptp.'B_d_vec_set$'|)) |tptp.'B_d_vec_set$'| (as |@_tptp.'B_d_vec_set$'__0| |tptp.'B_d_vec_set$'|)) % 140.07/140.36 (define-fun |tptp.'uwp$'| (($x1 |tptp.'B_c_vec_a_vec_a_vec$'|) ($x2 |tptp.'A$'|) ($x3 |tptp.'A$'|)) |tptp.'A_b_c_vec_a_vec_fun$'| (as |@_tptp.'A_b_c_vec_a_vec_fun$'__0| |tptp.'A_b_c_vec_a_vec_fun$'|)) % 140.07/140.36 (define-fun |tptp.'member$e'| (($x1 |tptp.'B_d_vec$'|) ($x2 |tptp.'B_d_vec_set$'|)) Bool false) % 140.07/140.36 (define-fun |tptp.'transpose_row$g'| ((BOUND_VARIABLE_57935 |tptp.'B_a_vec_c_vec$'|)) |tptp.'A_b_c_vec_fun$'| (as |@_tptp.'A_b_c_vec_fun$'__1| |tptp.'A_b_c_vec_fun$'|)) % 140.07/140.36 (define-fun |tptp.'column$j'| ((BOUND_VARIABLE_57950 |tptp.'A$'|) (BOUND_VARIABLE_57952 |tptp.'B_a_vec_d_vec$'|)) |tptp.'B_d_vec$'| (as |@_tptp.'B_d_vec$'__0| |tptp.'B_d_vec$'|)) % 140.07/140.36 (define-fun |tptp.'fun_app$o'| (($x1 |tptp.'D_b_d_vec_fun$'|) ($x2 |tptp.'D$'|)) |tptp.'B_d_vec$'| (as |@_tptp.'B_d_vec$'__0| |tptp.'B_d_vec$'|)) % 140.07/140.36 (define-fun |tptp.'vec_nth$r'| (($x1 |tptp.'B_d_vec_d_vec_a_vec$'|) ($x2 |tptp.'A$'|)) |tptp.'B_d_vec_d_vec$'| (as |@_tptp.'B_d_vec_d_vec$'__0| |tptp.'B_d_vec_d_vec$'|)) % 140.07/140.36 (define-fun |tptp.'member$d'| (($x1 |tptp.'B_d_vec_a_vec$'|) ($x2 |tptp.'B_d_vec_a_vec_set$'|)) Bool false) % 140.07/140.36 (define-fun |tptp.'vector_scalar_mult$g'| ((BOUND_VARIABLE_57964 |tptp.'B_c_vec$'|) (BOUND_VARIABLE_57966 |tptp.'B_c_vec_a_vec$'|)) |tptp.'B_c_vec_a_vec$'| (as |@_tptp.'B_c_vec_a_vec$'__0| |tptp.'B_c_vec_a_vec$'|)) % 140.07/140.36 (define-fun |tptp.'uxm$'| (($x1 |tptp.'B_a_vec$'|) ($x2 |tptp.'A$'|)) |tptp.'C_b_fun$'| (as |@_tptp.'C_b_fun$'__0| |tptp.'C_b_fun$'|)) % 140.07/140.36 (define-fun |tptp.'columnvector$f'| ((BOUND_VARIABLE_57975 |tptp.'B_c_vec$'|)) |tptp.'B_a_vec_c_vec$'| (as |@_tptp.'B_a_vec_c_vec$'__0| |tptp.'B_a_vec_c_vec$'|)) % 140.07/140.36 (define-fun |tptp.'uyl$'| (($x1 |tptp.'B_d_vec$'|) ($x2 |tptp.'D$'|)) |tptp.'D_b_fun$'| (as |@_tptp.'D_b_fun$'__0| |tptp.'D_b_fun$'|)) % 140.07/140.36 (define-fun |tptp.'uyo$'| (($x1 |tptp.'A_b_c_vec_fun_set$'|)) |tptp.'A_b_c_vec_fun_bool_fun$'| (as |@_tptp.'A_b_c_vec_fun_bool_fun$'__0| |tptp.'A_b_c_vec_fun_bool_fun$'|)) % 140.07/140.36 (define-fun |tptp.'vec_nth$b'| (($x1 |tptp.'B_d_vec_a_vec$'|)) |tptp.'A_b_d_vec_fun$'| (as |@_tptp.'A_b_d_vec_fun$'__0| |tptp.'A_b_d_vec_fun$'|)) % 140.07/140.36 (define-fun |tptp.'uvz$'| (($x1 |tptp.'B_c_vec_a_vec_a_vec$'|) ($x2 |tptp.'A$'|) ($x3 |tptp.'A$'|) ($x4 |tptp.'A$'|)) |tptp.'A_b_c_vec_fun$'| (as |@_tptp.'A_b_c_vec_fun$'__1| |tptp.'A_b_c_vec_fun$'|)) % 140.07/140.36 (define-fun |tptp.'vaw$'| (($x1 |tptp.'B_c_vec_a_vec$'|) ($x2 |tptp.'B_c_vec_a_vec_a_vec$'|)) |tptp.'A_b_c_vec_a_vec_fun$'| (as |@_tptp.'A_b_c_vec_a_vec_fun$'__0| |tptp.'A_b_c_vec_a_vec_fun$'|)) % 140.07/140.36 (define-fun |tptp.'columnvector$g'| ((BOUND_VARIABLE_57984 |tptp.'B_a_vec$'|)) |tptp.'B_d_vec_a_vec$'| (as |@_tptp.'B_d_vec_a_vec$'__0| |tptp.'B_d_vec_a_vec$'|)) % 140.07/140.36 (define-fun |tptp.'uwx$'| (($x1 |tptp.'B_d_vec_c_vec$'|)) |tptp.'D_b_c_vec_fun$'| (as |@_tptp.'D_b_c_vec_fun$'__0| |tptp.'D_b_c_vec_fun$'|)) % 140.07/140.36 (define-fun |tptp.'uzf$'| (($x1 |tptp.'B_d_vec_a_vec$'|) ($x2 |tptp.'A$'|) ($x3 |tptp.'A$'|) ($x4 |tptp.'B$'|) ($x5 |tptp.'A$'|)) |tptp.'D_b_fun$'| (as |@_tptp.'D_b_fun$'__0| |tptp.'D_b_fun$'|)) % 140.07/140.36 (define-fun |tptp.'uyu$'| (($x1 |tptp.'B_c_vec_a_vec_a_vec$'|) ($x2 |tptp.'A$'|) ($x3 |tptp.'B_c_vec$'|)) |tptp.'A_b_c_vec_a_vec_fun$'| (as |@_tptp.'A_b_c_vec_a_vec_fun$'__0| |tptp.'A_b_c_vec_a_vec_fun$'|)) % 140.07/140.36 (define-fun |tptp.'rows$'| (($x1 |tptp.'B_c_vec_a_vec$'|)) |tptp.'B_c_vec_set$'| (as |@_tptp.'B_c_vec_set$'__0| |tptp.'B_c_vec_set$'|)) % 140.07/140.36 (define-fun |tptp.'fun_app$j'| (($x1 |tptp.'A_b_a_vec_fun$'|) ($x2 |tptp.'A$'|)) |tptp.'B_a_vec$'| (as |@_tptp.'B_a_vec$'__0| |tptp.'B_a_vec$'|)) % 140.07/140.36 (define-fun |tptp.'columnvector_row$i'| ((BOUND_VARIABLE_57998 |tptp.'B_d_vec_a_vec$'|) (BOUND_VARIABLE_58000 |tptp.'A$'|)) |tptp.'B_d_vec_a_vec$'| (as |@_tptp.'B_d_vec_a_vec$'__0| |tptp.'B_d_vec_a_vec$'|)) % 140.07/140.36 (define-fun |tptp.'plus$s'| (($x1 |tptp.'B_c_vec_set$'|) ($x2 |tptp.'B_c_vec_set$'|)) |tptp.'B_c_vec_set$'| (as |@_tptp.'B_c_vec_set$'__0| |tptp.'B_c_vec_set$'|)) % 140.07/140.36 (define-fun |tptp.'vec_nth$s'| (($x1 |tptp.'B_d_vec_d_vec_d_vec$'|) ($x2 |tptp.'D$'|)) |tptp.'B_d_vec_d_vec$'| (as |@_tptp.'B_d_vec_d_vec$'__0| |tptp.'B_d_vec_d_vec$'|)) % 140.07/140.36 (define-fun |tptp.'elt_set_plus$g'| (($x1 |tptp.'B_c_vec$'|) ($x2 |tptp.'B_c_vec_set$'|)) |tptp.'B_c_vec_set$'| (as |@_tptp.'B_c_vec_set$'__0| |tptp.'B_c_vec_set$'|)) % 140.07/140.36 (define-fun |tptp.'uminus$d'| ((BOUND_VARIABLE_58007 |tptp.'B_a_vec$'|)) |tptp.'B_a_vec$'| (as |@_tptp.'B_a_vec$'__0| |tptp.'B_a_vec$'|)) % 140.07/140.36 (define-fun |tptp.'map_matrix$b'| ((BOUND_VARIABLE_58019 |tptp.'B_b_fun$'|) (BOUND_VARIABLE_58021 |tptp.'B_d_vec_a_vec$'|)) |tptp.'B_d_vec_a_vec$'| (as |@_tptp.'B_d_vec_a_vec$'__0| |tptp.'B_d_vec_a_vec$'|)) % 140.07/140.36 (define-fun |tptp.'member$b'| ((BOUND_VARIABLE_58044 |tptp.'A_b_c_vec_fun$'|) (BOUND_VARIABLE_58046 |tptp.'A_b_c_vec_fun_set$'|)) Bool (= (as |@_tptp.'A_b_c_vec_fun$'__1| |tptp.'A_b_c_vec_fun$'|) BOUND_VARIABLE_58044)) % 140.07/140.36 (define-fun |tptp.'vec_lambda$d'| (($x1 |tptp.'C_b_fun$'|)) |tptp.'B_c_vec$'| (as |@_tptp.'B_c_vec$'__0| |tptp.'B_c_vec$'|)) % 140.07/140.36 (define-fun |tptp.'mult_column_row$b'| ((BOUND_VARIABLE_58069 |tptp.'B_a_vec_c_vec$'|) (BOUND_VARIABLE_58071 |tptp.'A$'|) (BOUND_VARIABLE_58073 |tptp.'B$'|)) |tptp.'C_b_a_vec_fun$'| (as |@_tptp.'C_b_a_vec_fun$'__0| |tptp.'C_b_a_vec_fun$'|)) % 140.07/140.36 (define-fun |tptp.'j$'| () |tptp.'D$'| (as |@_tptp.'D$'__0| |tptp.'D$'|)) % 140.07/140.36 (define-fun |tptp.'uxy$'| (($x1 |tptp.'B_c_vec$'|) ($x2 |tptp.'C$'|)) |tptp.'A_b_fun$'| (as |@_tptp.'A_b_fun$'__0| |tptp.'A_b_fun$'|)) % 140.07/140.36 (define-fun |tptp.'uyj$'| (($x1 |tptp.'B_d_vec_a_vec$'|) ($x2 |tptp.'A$'|) ($x3 |tptp.'A$'|)) |tptp.'A_b_d_vec_fun$'| (as |@_tptp.'A_b_d_vec_fun$'__0| |tptp.'A_b_d_vec_fun$'|)) % 140.07/140.36 (define-fun |tptp.'vas$'| (($x1 |tptp.'B_c_vec_a_vec$'|) ($x2 |tptp.'C$'|) ($x3 |tptp.'C$'|) ($x4 |tptp.'B$'|)) |tptp.'A_b_c_vec_fun$'| (as |@_tptp.'A_b_c_vec_fun$'__1| |tptp.'A_b_c_vec_fun$'|)) % 140.07/140.36 (define-fun |tptp.'fun_app$x'| (($x1 |tptp.'B_a_vec_b_fun$'|) ($x2 |tptp.'B_a_vec$'|)) |tptp.'B$'| (as |@_tptp.'B$'__0| |tptp.'B$'|)) % 140.07/140.36 (define-fun |tptp.'mult_column$'| ((BOUND_VARIABLE_58092 |tptp.'B_d_vec_d_vec$'|) (BOUND_VARIABLE_58094 |tptp.'D$'|) (BOUND_VARIABLE_58096 |tptp.'B$'|)) |tptp.'B_d_vec_d_vec$'| (as |@_tptp.'B_d_vec_d_vec$'__0| |tptp.'B_d_vec_d_vec$'|)) % 140.07/140.36 (define-fun |tptp.'columnvector_row$e'| ((BOUND_VARIABLE_58110 |tptp.'B_d_vec$'|) (BOUND_VARIABLE_58112 |tptp.'D$'|)) |tptp.'B_a_vec$'| (as |@_tptp.'B_a_vec$'__0| |tptp.'B_a_vec$'|)) % 140.07/140.36 (define-fun |tptp.'vbf$'| (($x1 |tptp.'B_d_vec$'|)) |tptp.'A_b_d_vec_fun$'| (as |@_tptp.'A_b_d_vec_fun$'__0| |tptp.'A_b_d_vec_fun$'|)) % 140.07/140.36 (define-fun |tptp.'elt_set_times$b'| (($x1 |tptp.'A_b_c_vec_fun$'|) ($x2 |tptp.'A_b_c_vec_fun_set$'|)) |tptp.'A_b_c_vec_fun_set$'| (as |@_tptp.'A_b_c_vec_fun_set$'__0| |tptp.'A_b_c_vec_fun_set$'|)) % 140.07/140.36 (define-fun |tptp.'interchange_columns_row$d'| ((BOUND_VARIABLE_58131 |tptp.'B_d_vec_a_vec$'|) (BOUND_VARIABLE_58133 |tptp.'D$'|) (BOUND_VARIABLE_58135 |tptp.'D$'|)) |tptp.'A_b_d_vec_fun$'| (as |@_tptp.'A_b_d_vec_fun$'__0| |tptp.'A_b_d_vec_fun$'|)) % 140.07/140.36 (define-fun |tptp.'vec$g'| () |tptp.'B_b_a_vec_fun$'| (as |@_tptp.'B_b_a_vec_fun$'__0| |tptp.'B_b_a_vec_fun$'|)) % 140.07/140.36 (define-fun |tptp.'rowvector$a'| ((BOUND_VARIABLE_57714 |tptp.'B_a_vec$'|)) |tptp.'B_a_vec_c_vec$'| (as |@_tptp.'B_a_vec_c_vec$'__0| |tptp.'B_a_vec_c_vec$'|)) % 140.07/140.36 (define-fun |tptp.'uya$'| (($x1 |tptp.'B_a_vec$'|) ($x2 |tptp.'A$'|)) |tptp.'D_b_fun$'| (as |@_tptp.'D_b_fun$'__0| |tptp.'D_b_fun$'|)) % 140.07/140.36 (define-fun |tptp.'row_add_row$a'| ((BOUND_VARIABLE_58165 |tptp.'B_d_vec_d_vec$'|) (BOUND_VARIABLE_58167 |tptp.'D$'|) (BOUND_VARIABLE_58169 |tptp.'D$'|) (BOUND_VARIABLE_58171 |tptp.'B$'|)) |tptp.'D_b_d_vec_fun$'| (as |@_tptp.'D_b_d_vec_fun$'__0| |tptp.'D_b_d_vec_fun$'|)) % 140.07/140.36 (define-fun |tptp.'uminus$c'| ((BOUND_VARIABLE_58178 |tptp.'B_c_vec$'|)) |tptp.'B_c_vec$'| (as |@_tptp.'B_c_vec$'__0| |tptp.'B_c_vec$'|)) % 140.07/140.36 (define-fun |tptp.'map_matrix$l'| (($x1 |tptp.'B_d_vec_b_fun$'|) ($x2 |tptp.'B_d_vec_d_vec_a_vec$'|)) |tptp.'B_d_vec_a_vec$'| (as |@_tptp.'B_d_vec_a_vec$'__0| |tptp.'B_d_vec_a_vec$'|)) % 140.07/140.36 (define-fun |tptp.'vbd$'| (($x1 |tptp.'B$'|)) |tptp.'C_b_fun$'| (as |@_tptp.'C_b_fun$'__0| |tptp.'C_b_fun$'|)) % 140.07/140.36 (define-fun |tptp.'columns$d'| ((BOUND_VARIABLE_58188 |tptp.'B_a_vec_d_vec$'|)) |tptp.'B_d_vec_set$'| (as |@_tptp.'B_d_vec_set$'__0| |tptp.'B_d_vec_set$'|)) % 140.07/140.36 (define-fun |tptp.'uvd$'| (($x1 |tptp.'B_b_a_vec_fun$'|) ($x2 |tptp.'B_c_vec_a_vec$'|)) |tptp.'A_b_a_vec_c_vec_fun$'| (as |@_tptp.'A_b_a_vec_c_vec_fun$'__0| |tptp.'A_b_a_vec_c_vec_fun$'|)) % 140.07/140.36 (define-fun tptp.tltrue () tptp.tlbool (as @tptp.tlbool_1 tptp.tlbool)) % 140.07/140.36 (define-fun |tptp.'fun_app$p'| (($x1 |tptp.'C_b_d_vec_fun$'|) ($x2 |tptp.'C$'|)) |tptp.'B_d_vec$'| (as |@_tptp.'B_d_vec$'__0| |tptp.'B_d_vec$'|)) % 140.07/140.36 (define-fun |tptp.'uym$'| (($x1 |tptp.'A_b_d_vec_fun_set$'|)) |tptp.'A_b_d_vec_fun_bool_fun$'| (as |@_tptp.'A_b_d_vec_fun_bool_fun$'__0| |tptp.'A_b_d_vec_fun_bool_fun$'|)) % 140.07/140.36 (define-fun |tptp.'vec$'| () |tptp.'B_b_c_vec_fun$'| (as |@_tptp.'B_b_c_vec_fun$'__0| |tptp.'B_b_c_vec_fun$'|)) % 140.07/140.36 (define-fun |tptp.'interchange_rows_row$c'| ((BOUND_VARIABLE_58208 |tptp.'B_c_vec_a_vec$'|) (BOUND_VARIABLE_58210 |tptp.'A$'|) (BOUND_VARIABLE_58212 |tptp.'A$'|)) |tptp.'A_b_c_vec_fun$'| (as |@_tptp.'A_b_c_vec_fun$'__1| |tptp.'A_b_c_vec_fun$'|)) % 140.07/140.36 (define-fun |tptp.'columnvector_row$g'| ((BOUND_VARIABLE_58226 |tptp.'B_a_vec$'|) (BOUND_VARIABLE_58228 |tptp.'A$'|)) |tptp.'B_a_vec$'| (as |@_tptp.'B_a_vec$'__0| |tptp.'B_a_vec$'|)) % 140.07/140.36 (define-fun |tptp.'columnvector_row$c'| ((BOUND_VARIABLE_58240 |tptp.'B_c_vec$'|) (BOUND_VARIABLE_58242 |tptp.'C$'|)) |tptp.'B_c_vec$'| (as |@_tptp.'B_c_vec$'__0| |tptp.'B_c_vec$'|)) % 140.07/140.36 (define-fun |tptp.'columnvector$'| ((BOUND_VARIABLE_58252 |tptp.'B_a_vec$'|)) |tptp.'B_c_vec_a_vec$'| (as |@_tptp.'B_c_vec_a_vec$'__0| |tptp.'B_c_vec_a_vec$'|)) % 140.07/140.36 (define-fun |tptp.'plus$l'| (($x1 |tptp.'D_b_fun_set$'|) ($x2 |tptp.'D_b_fun_set$'|)) |tptp.'D_b_fun_set$'| (as |@_tptp.'D_b_fun_set$'__0| |tptp.'D_b_fun_set$'|)) % 140.07/140.36 (define-fun |tptp.'uyk$'| (($x1 |tptp.'B_c_vec_a_vec$'|) ($x2 |tptp.'A$'|) ($x3 |tptp.'A$'|)) |tptp.'A_b_c_vec_fun$'| (as |@_tptp.'A_b_c_vec_fun$'__1| |tptp.'A_b_c_vec_fun$'|)) % 140.07/140.36 (define-fun |tptp.'fun_app$a'| (($x1 |tptp.'B_b_fun$'|) ($x2 |tptp.'B$'|)) |tptp.'B$'| (as |@_tptp.'B$'__0| |tptp.'B$'|)) % 140.07/140.36 (define-fun |tptp.'fun_app$ad'| (($x1 |tptp.'B_d_vec_bool_fun$'|) ($x2 |tptp.'B_d_vec$'|)) Bool true) % 140.07/140.36 (define-fun |tptp.'transpose$c'| ((BOUND_VARIABLE_56919 |tptp.'B_c_vec_a_vec_a_vec$'|)) |tptp.'B_c_vec_a_vec_a_vec$'| (as |@_tptp.'B_c_vec_a_vec_a_vec$'__0| |tptp.'B_c_vec_a_vec_a_vec$'|)) % 140.07/140.36 (define-fun |tptp.'vec_lambda$a'| (($x1 |tptp.'C_b_a_vec_fun$'|)) |tptp.'B_a_vec_c_vec$'| (as |@_tptp.'B_a_vec_c_vec$'__0| |tptp.'B_a_vec_c_vec$'|)) % 140.07/140.36 (define-fun |tptp.'vec$c'| ((BOUND_VARIABLE_58264 |tptp.'B_c_vec$'|)) |tptp.'B_c_vec_a_vec$'| (as |@_tptp.'B_c_vec_a_vec$'__0| |tptp.'B_c_vec_a_vec$'|)) % 140.07/140.36 (define-fun |tptp.'fun_app$ar'| (($x1 |tptp.'C_b_fun_bool_fun$'|) ($x2 |tptp.'C_b_fun$'|)) Bool false) % 140.07/140.36 (define-fun |tptp.'fun_app$s'| (($x1 |tptp.'C_b_d_vec_a_vec_fun$'|) ($x2 |tptp.'C$'|)) |tptp.'B_d_vec_a_vec$'| (as |@_tptp.'B_d_vec_a_vec$'__0| |tptp.'B_d_vec_a_vec$'|)) % 140.07/140.36 (define-fun |tptp.'vbg$'| (($x1 |tptp.'B$'|)) |tptp.'A_b_fun$'| (as |@_tptp.'A_b_fun$'__0| |tptp.'A_b_fun$'|)) % 140.07/140.36 (define-fun |tptp.'vector_scalar_mult$b'| ((BOUND_VARIABLE_58277 |tptp.'B$'|) (BOUND_VARIABLE_58279 |tptp.'B_c_vec$'|)) |tptp.'B_c_vec$'| (as |@_tptp.'B_c_vec$'__0| |tptp.'B_c_vec$'|)) % 140.07/140.36 (define-fun |tptp.'fun_app$aj'| (($x1 |tptp.'A_b_bool_fun_fun$'|) ($x2 |tptp.'A$'|)) |tptp.'B_bool_fun$'| (as |@_tptp.'B_bool_fun$'__0| |tptp.'B_bool_fun$'|)) % 140.07/140.36 (define-fun |tptp.'mult_row_row$a'| ((BOUND_VARIABLE_58299 |tptp.'B_c_vec_a_vec_a_vec$'|) (BOUND_VARIABLE_58301 |tptp.'A$'|) (BOUND_VARIABLE_58303 |tptp.'B_c_vec$'|)) |tptp.'A_b_c_vec_a_vec_fun$'| (as |@_tptp.'A_b_c_vec_a_vec_fun$'__0| |tptp.'A_b_c_vec_a_vec_fun$'|)) % 140.07/140.36 (define-fun |tptp.'columnvector$a'| ((BOUND_VARIABLE_57311 |tptp.'B_c_vec_a_vec$'|)) |tptp.'B_c_vec_a_vec_a_vec$'| (as |@_tptp.'B_c_vec_a_vec_a_vec$'__0| |tptp.'B_c_vec_a_vec_a_vec$'|)) % 140.07/140.36 (define-fun |tptp.'column_add$d'| ((BOUND_VARIABLE_58325 |tptp.'B_c_vec_a_vec$'|) (BOUND_VARIABLE_58327 |tptp.'C$'|) (BOUND_VARIABLE_58329 |tptp.'C$'|) (BOUND_VARIABLE_58331 |tptp.'B$'|)) |tptp.'B_c_vec_a_vec$'| (as |@_tptp.'B_c_vec_a_vec$'__0| |tptp.'B_c_vec_a_vec$'|)) % 140.07/140.36 (define-fun |tptp.'map_matrix$d'| ((BOUND_VARIABLE_58346 |tptp.'B_b_a_vec_fun$'|) (BOUND_VARIABLE_58348 |tptp.'B_c_vec_a_vec$'|)) |tptp.'B_a_vec_c_vec_a_vec$'| (as |@_tptp.'B_a_vec_c_vec_a_vec$'__0| |tptp.'B_a_vec_c_vec_a_vec$'|)) % 140.07/140.36 (define-fun |tptp.'rowvector$c'| ((BOUND_VARIABLE_58358 |tptp.'B_d_vec$'|)) |tptp.'B_d_vec_a_vec$'| (as |@_tptp.'B_d_vec_a_vec$'__0| |tptp.'B_d_vec_a_vec$'|)) % 140.07/140.36 (define-fun |tptp.'uut$'| (($x1 |tptp.'B_c_vec_d_vec$'|)) |tptp.'D_b_c_vec_fun$'| (as |@_tptp.'D_b_c_vec_fun$'__0| |tptp.'D_b_c_vec_fun$'|)) % 140.07/140.36 (define-fun |tptp.'times$n'| (($x1 |tptp.'A_b_c_vec_fun_set$'|) ($x2 |tptp.'A_b_c_vec_fun_set$'|)) |tptp.'A_b_c_vec_fun_set$'| (as |@_tptp.'A_b_c_vec_fun_set$'__0| |tptp.'A_b_c_vec_fun_set$'|)) % 140.07/140.36 (define-fun |tptp.'uvx$'| (($x1 |tptp.'B_d_vec_a_vec$'|) ($x2 |tptp.'D$'|) ($x3 |tptp.'D$'|) ($x4 |tptp.'A$'|)) |tptp.'D_b_fun$'| (as |@_tptp.'D_b_fun$'__0| |tptp.'D_b_fun$'|)) % 140.07/140.36 (define-fun |tptp.'times$r'| (($x1 |tptp.'B_c_vec_a_vec_set$'|) ($x2 |tptp.'B_c_vec_a_vec_set$'|)) |tptp.'B_c_vec_a_vec_set$'| (as |@_tptp.'B_c_vec_a_vec_set$'__0| |tptp.'B_c_vec_a_vec_set$'|)) % 140.07/140.36 (define-fun |tptp.'plus$n'| (($x1 |tptp.'A_b_c_vec_fun_set$'|) ($x2 |tptp.'A_b_c_vec_fun_set$'|)) |tptp.'A_b_c_vec_fun_set$'| (as |@_tptp.'A_b_c_vec_fun_set$'__0| |tptp.'A_b_c_vec_fun_set$'|)) % 140.07/140.36 (define-fun |tptp.'uwq$'| (($x1 |tptp.'B_d_vec_a_vec$'|) ($x2 |tptp.'D$'|) ($x3 |tptp.'D$'|)) |tptp.'A_b_d_vec_fun$'| (as |@_tptp.'A_b_d_vec_fun$'__0| |tptp.'A_b_d_vec_fun$'|)) % 140.07/140.36 (define-fun |tptp.'times$j'| (($x1 |tptp.'A_b_d_vec_fun_set$'|) ($x2 |tptp.'A_b_d_vec_fun_set$'|)) |tptp.'A_b_d_vec_fun_set$'| (as |@_tptp.'A_b_d_vec_fun_set$'__0| |tptp.'A_b_d_vec_fun_set$'|)) % 140.07/140.36 (define-fun |tptp.'times$f'| ((BOUND_VARIABLE_58373 |tptp.'B_d_vec_d_vec$'|) (BOUND_VARIABLE_58375 |tptp.'B_d_vec_d_vec$'|)) |tptp.'B_d_vec_d_vec$'| (as |@_tptp.'B_d_vec_d_vec$'__0| |tptp.'B_d_vec_d_vec$'|)) % 140.07/140.36 (define-fun |tptp.'times$s'| (($x1 |tptp.'B_c_vec_set$'|) ($x2 |tptp.'B_c_vec_set$'|)) |tptp.'B_c_vec_set$'| (as |@_tptp.'B_c_vec_set$'__0| |tptp.'B_c_vec_set$'|)) % 140.07/140.36 (define-fun |tptp.'top$b'| () |tptp.'C_b_a_vec_fun_set$'| (as |@_tptp.'C_b_a_vec_fun_set$'__0| |tptp.'C_b_a_vec_fun_set$'|)) % 140.07/140.36 (define-fun |tptp.'uwt$'| (($x1 |tptp.'B_d_vec_a_vec$'|)) |tptp.'D_b_a_vec_fun$'| (as |@_tptp.'D_b_a_vec_fun$'__0| |tptp.'D_b_a_vec_fun$'|)) % 140.07/140.36 (define-fun |tptp.'transpose$a'| ((BOUND_VARIABLE_58385 |tptp.'B_d_vec_a_vec$'|)) |tptp.'B_a_vec_d_vec$'| (as |@_tptp.'B_a_vec_d_vec$'__0| |tptp.'B_a_vec_d_vec$'|)) % 140.07/140.36 (define-fun |tptp.'vec_lambda$q'| ((_arg_1 |tptp.'A_b_d_vec_a_vec_fun$'|)) |tptp.'B_d_vec_a_vec_a_vec$'| (as |@_tptp.'B_d_vec_a_vec_a_vec$'__0| |tptp.'B_d_vec_a_vec_a_vec$'|)) % 140.07/140.36 (define-fun |tptp.'uvc$'| (($x1 |tptp.'B_b_a_vec_fun$'|) ($x2 |tptp.'B_c_vec_a_vec$'|) ($x3 |tptp.'A$'|)) |tptp.'C_b_a_vec_fun$'| (as |@_tptp.'C_b_a_vec_fun$'__0| |tptp.'C_b_a_vec_fun$'|)) % 140.07/140.36 (define-fun |tptp.'rows$c'| (($x1 |tptp.'B_a_vec_c_vec$'|)) |tptp.'B_a_vec_set$'| (as |@_tptp.'B_a_vec_set$'__0| |tptp.'B_a_vec_set$'|)) % 140.07/140.36 (define-fun |tptp.'vec_lambda$i'| (($x1 |tptp.'D_b_c_vec_fun$'|)) |tptp.'B_c_vec_d_vec$'| (as |@_tptp.'B_c_vec_d_vec$'__0| |tptp.'B_c_vec_d_vec$'|)) % 140.07/140.36 (define-fun |tptp.'uxk$'| (($x1 |tptp.'C$'|) ($x2 |tptp.'B_a_vec_c_vec_c_vec$'|)) |tptp.'C_b_a_vec_fun$'| (as |@_tptp.'C_b_a_vec_fun$'__0| |tptp.'C_b_a_vec_fun$'|)) % 140.07/140.36 (define-fun |tptp.'member$g'| (($x1 |tptp.'B_c_vec$'|) ($x2 |tptp.'B_c_vec_set$'|)) Bool false) % 140.07/140.36 (define-fun |tptp.'vec_lambda$g'| (($x1 |tptp.'A_b_c_vec_a_vec_fun$'|)) |tptp.'B_c_vec_a_vec_a_vec$'| (as |@_tptp.'B_c_vec_a_vec_a_vec$'__0| |tptp.'B_c_vec_a_vec_a_vec$'|)) % 140.07/140.36 (define-fun |tptp.'a$'| () |tptp.'B_c_vec_a_vec$'| (as |@_tptp.'B_c_vec_a_vec$'__0| |tptp.'B_c_vec_a_vec$'|)) % 140.07/140.36 (define-fun |tptp.'uyt$'| (($x1 |tptp.'B_c_vec_a_vec_a_vec$'|) ($x2 |tptp.'A$'|) ($x3 |tptp.'B_c_vec$'|) ($x4 |tptp.'A$'|)) |tptp.'A_b_c_vec_fun$'| (as |@_tptp.'A_b_c_vec_fun$'__1| |tptp.'A_b_c_vec_fun$'|)) % 140.07/140.36 (define-fun |tptp.'uux$'| (($x1 |tptp.'B_b_fun$'|) ($x2 |tptp.'B_a_vec_c_vec$'|)) |tptp.'C_b_a_vec_fun$'| (as |@_tptp.'C_b_a_vec_fun$'__0| |tptp.'C_b_a_vec_fun$'|)) % 140.07/140.36 (define-fun |tptp.'elt_set_times$g'| (($x1 |tptp.'B_c_vec$'|) ($x2 |tptp.'B_c_vec_set$'|)) |tptp.'B_c_vec_set$'| (as |@_tptp.'B_c_vec_set$'__0| |tptp.'B_c_vec_set$'|)) % 140.07/140.36 (define-fun |tptp.'vaa$'| (($x1 |tptp.'B_c_vec_a_vec$'|) ($x2 |tptp.'B_c_vec_a_vec$'|)) |tptp.'A_b_c_vec_fun$'| (as |@_tptp.'A_b_c_vec_fun$'__1| |tptp.'A_b_c_vec_fun$'|)) % 140.07/140.36 (define-fun |tptp.'elt_set_times$f'| (($x1 |tptp.'B_c_vec_a_vec$'|) ($x2 |tptp.'B_c_vec_a_vec_set$'|)) |tptp.'B_c_vec_a_vec_set$'| (as |@_tptp.'B_c_vec_a_vec_set$'__0| |tptp.'B_c_vec_a_vec_set$'|)) % 140.07/140.36 (define-fun |tptp.'column_add_row$d'| ((BOUND_VARIABLE_58406 |tptp.'B_d_vec_a_vec$'|) (BOUND_VARIABLE_58408 |tptp.'D$'|) (BOUND_VARIABLE_58410 |tptp.'D$'|) (BOUND_VARIABLE_58412 |tptp.'B$'|)) |tptp.'A_b_d_vec_fun$'| (as |@_tptp.'A_b_d_vec_fun$'__0| |tptp.'A_b_d_vec_fun$'|)) % 140.07/140.36 (define-fun |tptp.'interchange_rows_row$'| ((BOUND_VARIABLE_57386 |tptp.'B_d_vec_d_vec$'|) (BOUND_VARIABLE_57388 |tptp.'D$'|) (BOUND_VARIABLE_57390 |tptp.'D$'|)) |tptp.'D_b_d_vec_fun$'| (as |@_tptp.'D_b_d_vec_fun$'__0| |tptp.'D_b_d_vec_fun$'|)) % 140.07/140.36 (define-fun |tptp.'interchange_columns$c'| ((BOUND_VARIABLE_58440 |tptp.'B_d_vec_a_vec$'|) (BOUND_VARIABLE_58442 |tptp.'D$'|) (BOUND_VARIABLE_58444 |tptp.'D$'|)) |tptp.'B_d_vec_a_vec$'| (as |@_tptp.'B_d_vec_a_vec$'__0| |tptp.'B_d_vec_a_vec$'|)) % 140.07/140.36 (define-fun |tptp.'uzu$'| (($x1 |tptp.'B_a_vec_c_vec$'|) ($x2 |tptp.'B_a_vec_c_vec$'|)) |tptp.'C_b_a_vec_fun$'| (as |@_tptp.'C_b_a_vec_fun$'__0| |tptp.'C_b_a_vec_fun$'|)) % 140.07/140.36 (define-fun |tptp.'vector_scalar_mult$e'| ((BOUND_VARIABLE_58459 |tptp.'B$'|) (BOUND_VARIABLE_58461 |tptp.'B_d_vec$'|)) |tptp.'B_d_vec$'| (as |@_tptp.'B_d_vec$'__0| |tptp.'B_d_vec$'|)) % 140.07/140.36 (define-fun |tptp.'uzz$'| (($x1 |tptp.'B_d_vec_a_vec$'|) ($x2 |tptp.'B_d_vec_a_vec$'|)) |tptp.'A_b_d_vec_fun$'| (as |@_tptp.'A_b_d_vec_fun$'__0| |tptp.'A_b_d_vec_fun$'|)) % 140.07/140.36 (define-fun |tptp.'transpose$i'| ((BOUND_VARIABLE_58474 |tptp.'B_a_vec_c_vec_c_vec$'|)) |tptp.'B_a_vec_c_vec_c_vec$'| (as |@_tptp.'B_a_vec_c_vec_c_vec$'__0| |tptp.'B_a_vec_c_vec_c_vec$'|)) % 140.07/140.36 (define-fun |tptp.'uzo$'| (($x1 |tptp.'B_c_vec_a_vec_a_vec$'|) ($x2 |tptp.'A$'|) ($x3 |tptp.'B_c_vec$'|)) |tptp.'A_b_c_vec_a_vec_fun$'| (as |@_tptp.'A_b_c_vec_a_vec_fun$'__0| |tptp.'A_b_c_vec_a_vec_fun$'|)) % 140.07/140.36 (define-fun |tptp.'times$a'| ((BOUND_VARIABLE_58486 |tptp.'B_d_vec$'|) (BOUND_VARIABLE_58488 |tptp.'B_d_vec$'|)) |tptp.'B_d_vec$'| (as |@_tptp.'B_d_vec$'__0| |tptp.'B_d_vec$'|)) % 140.07/140.36 (define-fun |tptp.'vec_nth$a'| (($x1 |tptp.'B_d_vec$'|)) |tptp.'D_b_fun$'| (as |@_tptp.'D_b_fun$'__0| |tptp.'D_b_fun$'|)) % 140.07/140.36 (define-fun |tptp.'fun_app$al'| (($x1 |tptp.'A_b_c_vec_bool_fun_fun$'|) ($x2 |tptp.'A$'|)) |tptp.'B_c_vec_bool_fun$'| (as |@_tptp.'B_c_vec_bool_fun$'__0| |tptp.'B_c_vec_bool_fun$'|)) % 140.07/140.36 (define-fun |tptp.'map_matrix$k'| (($x1 |tptp.'B_b_c_vec_fun$'|) ($x2 |tptp.'B_a_vec_a_vec$'|)) |tptp.'B_c_vec_a_vec_a_vec$'| (as |@_tptp.'B_c_vec_a_vec_a_vec$'__0| |tptp.'B_c_vec_a_vec_a_vec$'|)) % 140.07/140.36 (define-fun |tptp.'interchange_columns$'| ((BOUND_VARIABLE_58507 |tptp.'B_d_vec_d_vec$'|) (BOUND_VARIABLE_58509 |tptp.'D$'|) (BOUND_VARIABLE_58511 |tptp.'D$'|)) |tptp.'B_d_vec_d_vec$'| (as |@_tptp.'B_d_vec_d_vec$'__0| |tptp.'B_d_vec_d_vec$'|)) % 140.07/140.36 (define-fun |tptp.'b$'| () |tptp.'B_d_vec_a_vec$'| (as |@_tptp.'B_d_vec_a_vec$'__0| |tptp.'B_d_vec_a_vec$'|)) % 140.07/140.36 (define-fun |tptp.'uvj$'| (($x1 |tptp.'B_a_vec_b_fun$'|) ($x2 |tptp.'B_a_vec_c_vec_a_vec$'|)) |tptp.'A_b_c_vec_fun$'| (as |@_tptp.'A_b_c_vec_fun$'__1| |tptp.'A_b_c_vec_fun$'|)) % 140.07/140.36 (define-fun |tptp.'uvi$'| (($x1 |tptp.'B_a_vec_b_fun$'|) ($x2 |tptp.'B_a_vec_c_vec_a_vec$'|) ($x3 |tptp.'A$'|)) |tptp.'C_b_fun$'| (as |@_tptp.'C_b_fun$'__0| |tptp.'C_b_fun$'|)) % 140.07/140.36 (define-fun |tptp.'vec_lambda$o'| ((_arg_1 |tptp.'C_b_c_vec_fun$'|)) |tptp.'B_c_vec_c_vec$'| (as |@_tptp.'B_c_vec_c_vec$'__0| |tptp.'B_c_vec_c_vec$'|)) % 140.07/140.36 (define-fun |tptp.'vag$'| (($x1 |tptp.'B_d_vec$'|) ($x2 |tptp.'B_d_vec$'|)) |tptp.'D_b_fun$'| (as |@_tptp.'D_b_fun$'__0| |tptp.'D_b_fun$'|)) % 140.07/140.36 (define-fun |tptp.'uur$'| (($x1 |tptp.'B_c_vec_a_vec_a_vec$'|)) |tptp.'A_b_c_vec_a_vec_fun$'| (as |@_tptp.'A_b_c_vec_a_vec_fun$'__0| |tptp.'A_b_c_vec_a_vec_fun$'|)) % 140.07/140.36 (define-fun |tptp.'interchange_rows$'| ((BOUND_VARIABLE_58507 |tptp.'B_d_vec_d_vec$'|) (BOUND_VARIABLE_58509 |tptp.'D$'|) (BOUND_VARIABLE_58511 |tptp.'D$'|)) |tptp.'B_d_vec_d_vec$'| (as |@_tptp.'B_d_vec_d_vec$'__0| |tptp.'B_d_vec_d_vec$'|)) % 140.07/140.36 (define-fun |tptp.'uzc$'| (($x1 |tptp.'B_a_vec_c_vec$'|) ($x2 |tptp.'C$'|) ($x3 |tptp.'C$'|) ($x4 |tptp.'B$'|)) |tptp.'C_b_a_vec_fun$'| (as |@_tptp.'C_b_a_vec_fun$'__0| |tptp.'C_b_a_vec_fun$'|)) % 140.07/140.36 (define-fun |tptp.'top$c'| () |tptp.'C_b_fun_set$'| (as |@_tptp.'C_b_fun_set$'__0| |tptp.'C_b_fun_set$'|)) % 140.07/140.36 (define-fun |tptp.'uvr$'| (($x1 |tptp.'B_d_vec$'|)) |tptp.'A_b_d_vec_fun$'| (as |@_tptp.'A_b_d_vec_fun$'__0| |tptp.'A_b_d_vec_fun$'|)) % 140.07/140.36 (define-fun |tptp.'vec_nth$q'| (($x1 |tptp.'B_a_vec_c_vec_a_vec$'|) ($x2 |tptp.'A$'|)) |tptp.'B_a_vec_c_vec$'| (as |@_tptp.'B_a_vec_c_vec$'__0| |tptp.'B_a_vec_c_vec$'|)) % 140.07/140.36 (define-fun |tptp.'transpose$f'| ((BOUND_VARIABLE_58532 |tptp.'B_c_vec_c_vec$'|)) |tptp.'B_c_vec_c_vec$'| (as |@_tptp.'B_c_vec_c_vec$'__0| |tptp.'B_c_vec_c_vec$'|)) % 140.07/140.36 (define-fun |tptp.'columns$a'| ((BOUND_VARIABLE_58542 |tptp.'B_c_vec_a_vec_a_vec$'|)) |tptp.'B_c_vec_a_vec_set$'| (as |@_tptp.'B_c_vec_a_vec_set$'__0| |tptp.'B_c_vec_a_vec_set$'|)) % 140.07/140.36 (define-fun |tptp.'vector_scalar_mult$d'| ((BOUND_VARIABLE_58555 |tptp.'B$'|) (BOUND_VARIABLE_58557 |tptp.'B_a_vec$'|)) |tptp.'B_a_vec$'| (as |@_tptp.'B_a_vec$'__0| |tptp.'B_a_vec$'|)) % 140.07/140.36 (define-fun |tptp.'vector_scalar_mult$f'| ((BOUND_VARIABLE_58569 |tptp.'B_d_vec$'|) (BOUND_VARIABLE_58571 |tptp.'B_d_vec_a_vec$'|)) |tptp.'B_d_vec_a_vec$'| (as |@_tptp.'B_d_vec_a_vec$'__0| |tptp.'B_d_vec_a_vec$'|)) % 140.07/140.36 (define-fun |tptp.'vec_lambda$n'| (($x1 |tptp.'D_b_a_vec_fun$'|)) |tptp.'B_a_vec_d_vec$'| (as |@_tptp.'B_a_vec_d_vec$'__0| |tptp.'B_a_vec_d_vec$'|)) % 140.07/140.36 (define-fun |tptp.'fun_app$aa'| (($x1 |tptp.'B_b_a_vec_fun$'|) ($x2 |tptp.'B$'|)) |tptp.'B_a_vec$'| (as |@_tptp.'B_a_vec$'__0| |tptp.'B_a_vec$'|)) % 140.07/140.36 (define-fun |tptp.'uxg$'| (($x1 |tptp.'D$'|) ($x2 |tptp.'B_d_vec_c_vec$'|)) |tptp.'C_b_fun$'| (as |@_tptp.'C_b_fun$'__0| |tptp.'C_b_fun$'|)) % 140.07/140.36 (define-fun |tptp.'uuk$'| (($x1 |tptp.'B_d_vec$'|)) |tptp.'D_b_fun$'| (as |@_tptp.'D_b_fun$'__0| |tptp.'D_b_fun$'|)) % 140.07/140.36 (define-fun |tptp.'transpose_row$h'| ((BOUND_VARIABLE_58583 |tptp.'B_a_vec_a_vec$'|) (BOUND_VARIABLE_58585 |tptp.'A$'|)) |tptp.'B_a_vec$'| (as |@_tptp.'B_a_vec$'__0| |tptp.'B_a_vec$'|)) % 140.07/140.36 (define-fun |tptp.'times$l'| (($x1 |tptp.'D_b_fun_set$'|) ($x2 |tptp.'D_b_fun_set$'|)) |tptp.'D_b_fun_set$'| (as |@_tptp.'D_b_fun_set$'__0| |tptp.'D_b_fun_set$'|)) % 140.07/140.36 (define-fun |tptp.'transpose_row$j'| (($x1 |tptp.'B_d_vec_a_vec_a_vec$'|) ($x2 |tptp.'A$'|)) |tptp.'B_d_vec_a_vec$'| (as |@_tptp.'B_d_vec_a_vec$'__0| |tptp.'B_d_vec_a_vec$'|)) % 140.07/140.36 (define-fun |tptp.'uzy$'| (($x1 |tptp.'B_d_vec$'|) ($x2 |tptp.'B_d_vec$'|)) |tptp.'D_b_fun$'| (as |@_tptp.'D_b_fun$'__0| |tptp.'D_b_fun$'|)) % 140.07/140.36 (define-fun |tptp.'interchange_columns$e'| ((BOUND_VARIABLE_58607 |tptp.'B_a_vec_d_vec$'|) (BOUND_VARIABLE_58609 |tptp.'A$'|) (BOUND_VARIABLE_58611 |tptp.'A$'|)) |tptp.'B_a_vec_d_vec$'| (as |@_tptp.'B_a_vec_d_vec$'__0| |tptp.'B_a_vec_d_vec$'|)) % 140.07/140.36 (define-fun |tptp.'uyx$'| (($x1 |tptp.'B_c_vec_a_vec$'|) ($x2 |tptp.'C$'|) ($x3 |tptp.'B$'|) ($x4 |tptp.'A$'|)) |tptp.'C_b_fun$'| (as |@_tptp.'C_b_fun$'__0| |tptp.'C_b_fun$'|)) % 140.07/140.36 (define-fun |tptp.'uyp$'| (($x1 |tptp.'B_d_vec_d_vec$'|) ($x2 |tptp.'D$'|) ($x3 |tptp.'B$'|) ($x4 |tptp.'D$'|)) |tptp.'D_b_fun$'| (as |@_tptp.'D_b_fun$'__0| |tptp.'D_b_fun$'|)) % 140.07/140.36 (define-fun |tptp.'times$i'| (($x1 |tptp.'A_b_d_vec_fun$'|) ($x2 |tptp.'A_b_d_vec_fun$'|)) |tptp.'A_b_d_vec_fun$'| (as |@_tptp.'A_b_d_vec_fun$'__0| |tptp.'A_b_d_vec_fun$'|)) % 140.07/140.36 (define-fun |tptp.'fun_app$i'| (($x1 |tptp.'C_b_a_vec_fun$'|) ($x2 |tptp.'C$'|)) |tptp.'B_a_vec$'| (as |@_tptp.'B_a_vec$'__0| |tptp.'B_a_vec$'|)) % 140.07/140.36 (define-fun |tptp.'fun_app$aq'| (($x1 |tptp.'C_b_a_vec_fun_bool_fun$'|) ($x2 |tptp.'C_b_a_vec_fun$'|)) Bool false) % 140.07/140.36 (define-fun |tptp.'vec$b'| () |tptp.'B_b_d_vec_fun$'| (as |@_tptp.'B_b_d_vec_fun$'__0| |tptp.'B_b_d_vec_fun$'|)) % 140.07/140.36 (define-fun |tptp.'elt_set_times$d'| (($x1 |tptp.'B_d_vec_a_vec$'|) ($x2 |tptp.'B_d_vec_a_vec_set$'|)) |tptp.'B_d_vec_a_vec_set$'| (as |@_tptp.'B_d_vec_a_vec_set$'__0| |tptp.'B_d_vec_a_vec_set$'|)) % 140.07/140.36 (define-fun |tptp.'row_add$d'| ((BOUND_VARIABLE_58631 |tptp.'B_c_vec_a_vec_a_vec$'|) (BOUND_VARIABLE_58633 |tptp.'A$'|) (BOUND_VARIABLE_58635 |tptp.'A$'|) (BOUND_VARIABLE_58637 |tptp.'B_c_vec$'|)) |tptp.'B_c_vec_a_vec_a_vec$'| (as |@_tptp.'B_c_vec_a_vec_a_vec$'__0| |tptp.'B_c_vec_a_vec_a_vec$'|)) % 140.07/140.36 (define-fun |tptp.'gauss_Jordan_wrapper$h'| ((BOUND_VARIABLE_58662 |tptp.'C$'|) (BOUND_VARIABLE_58664 |tptp.'D$'|) (BOUND_VARIABLE_58666 |tptp.'B_a_vec_c_vec$'|) (BOUND_VARIABLE_58668 |tptp.'B_d_vec_c_vec$'|)) |tptp.'B_a_vec_c_vec$'| (as |@_tptp.'B_a_vec_c_vec$'__0| |tptp.'B_a_vec_c_vec$'|)) % 140.07/140.36 (define-fun |tptp.'member$i'| (($x1 |tptp.'D_b_d_vec_fun$'|) ($x2 |tptp.'D_b_d_vec_fun_set$'|)) Bool true) % 140.07/140.36 (define-fun |tptp.'fun_app$q'| (($x1 |tptp.'C_b_fun$'|) ($x2 |tptp.'C$'|)) |tptp.'B$'| (as |@_tptp.'B$'__0| |tptp.'B$'|)) % 140.07/140.36 (define-fun |tptp.'vec_nth$j'| (($x1 |tptp.'B_a_vec_c_vec_c_vec$'|) ($x2 |tptp.'C$'|)) |tptp.'B_a_vec_c_vec$'| (as |@_tptp.'B_a_vec_c_vec$'__0| |tptp.'B_a_vec_c_vec$'|)) % 140.07/140.36 (define-fun |tptp.'plus$m'| (($x1 |tptp.'A_b_c_vec_fun$'|) ($x2 |tptp.'A_b_c_vec_fun$'|)) |tptp.'A_b_c_vec_fun$'| (as |@_tptp.'A_b_c_vec_fun$'__1| |tptp.'A_b_c_vec_fun$'|)) % 140.07/140.36 (define-fun |tptp.'vec_nth$d'| (($x1 |tptp.'B_d_vec_d_vec$'|)) |tptp.'D_b_d_vec_fun$'| (as |@_tptp.'D_b_d_vec_fun$'__0| |tptp.'D_b_d_vec_fun$'|)) % 140.07/140.36 (define-fun |tptp.'times$h'| ((BOUND_VARIABLE_57229 |tptp.'B_d_vec_a_vec$'|) (BOUND_VARIABLE_57231 |tptp.'B_d_vec_a_vec$'|)) |tptp.'B_d_vec_a_vec$'| (as |@_tptp.'B_d_vec_a_vec$'__0| |tptp.'B_d_vec_a_vec$'|)) % 140.07/140.36 (define-fun |tptp.'column_add_row$'| ((BOUND_VARIABLE_58165 |tptp.'B_d_vec_d_vec$'|) (BOUND_VARIABLE_58167 |tptp.'D$'|) (BOUND_VARIABLE_58169 |tptp.'D$'|) (BOUND_VARIABLE_58171 |tptp.'B$'|)) |tptp.'D_b_d_vec_fun$'| (as |@_tptp.'D_b_d_vec_fun$'__0| |tptp.'D_b_d_vec_fun$'|)) % 140.07/140.36 (define-fun |tptp.'gauss_Jordan_wrapper$d'| ((BOUND_VARIABLE_58704 |tptp.'D$'|) (BOUND_VARIABLE_58706 |tptp.'D$'|) (BOUND_VARIABLE_58708 |tptp.'B_d_vec_d_vec$'|) (BOUND_VARIABLE_58710 |tptp.'B_d_vec_d_vec$'|)) |tptp.'B_d_vec_d_vec$'| (as |@_tptp.'B_d_vec_d_vec$'__0| |tptp.'B_d_vec_d_vec$'|)) % 140.07/140.36 (define-fun |tptp.'uxh$'| (($x1 |tptp.'C$'|) ($x2 |tptp.'B_c_vec_c_vec$'|)) |tptp.'C_b_fun$'| (as |@_tptp.'C_b_fun$'__0| |tptp.'C_b_fun$'|)) % 140.07/140.36 (define-fun |tptp.'vec_nth$l'| (($x1 |tptp.'B_a_vec_d_vec$'|)) |tptp.'D_b_a_vec_fun$'| (as |@_tptp.'D_b_a_vec_fun$'__0| |tptp.'D_b_a_vec_fun$'|)) % 140.07/140.36 (define-fun |tptp.'uxx$'| (($x1 |tptp.'B_a_vec$'|)) |tptp.'A_b_a_vec_fun$'| (as |@_tptp.'A_b_a_vec_fun$'__0| |tptp.'A_b_a_vec_fun$'|)) % 140.07/140.36 (define-fun |tptp.'uvy$'| (($x1 |tptp.'B_d_vec_d_vec$'|) ($x2 |tptp.'D$'|) ($x3 |tptp.'D$'|) ($x4 |tptp.'D$'|)) |tptp.'D_b_fun$'| (as |@_tptp.'D_b_fun$'__0| |tptp.'D_b_fun$'|)) % 140.07/140.36 (define-fun |tptp.'column_add_row$a'| ((BOUND_VARIABLE_58730 |tptp.'B_c_vec_a_vec_a_vec$'|) (BOUND_VARIABLE_58732 |tptp.'A$'|) (BOUND_VARIABLE_58734 |tptp.'A$'|) (BOUND_VARIABLE_58736 |tptp.'B_c_vec$'|)) |tptp.'A_b_c_vec_a_vec_fun$'| (as |@_tptp.'A_b_c_vec_a_vec_fun$'__0| |tptp.'A_b_c_vec_a_vec_fun$'|)) % 140.07/140.36 (define-fun |tptp.'vec_nth$n'| (($x1 |tptp.'B_d_vec_a_vec_a_vec$'|) ($x2 |tptp.'A$'|)) |tptp.'B_d_vec_a_vec$'| (as |@_tptp.'B_d_vec_a_vec$'__0| |tptp.'B_d_vec_a_vec$'|)) % 140.07/140.36 (define-fun |tptp.'columnvector_row$d'| (($x1 |tptp.'B_a_vec$'|)) |tptp.'A_b_c_vec_fun$'| (as |@_tptp.'A_b_c_vec_fun$'__1| |tptp.'A_b_c_vec_fun$'|)) % 140.07/140.36 (define-fun |tptp.'vec_nth$g'| (($x1 |tptp.'B_a_vec_c_vec$'|)) |tptp.'C_b_a_vec_fun$'| (as |@_tptp.'C_b_a_vec_fun$'__0| |tptp.'C_b_a_vec_fun$'|)) % 140.07/140.36 (define-fun |tptp.'column$b'| ((BOUND_VARIABLE_58750 |tptp.'A$'|) (BOUND_VARIABLE_58752 |tptp.'B_c_vec_a_vec_a_vec$'|)) |tptp.'B_c_vec_a_vec$'| (as |@_tptp.'B_c_vec_a_vec$'__0| |tptp.'B_c_vec_a_vec$'|)) % 140.07/140.36 (define-fun |tptp.'times$d'| (($x1 |tptp.'B$'|)) |tptp.'B_b_fun$'| (as |@_tptp.'B_b_fun$'__0| |tptp.'B_b_fun$'|)) % 140.07/140.36 (define-fun |tptp.'transpose_row$c'| ((BOUND_VARIABLE_58761 |tptp.'B_d_vec_d_vec$'|)) |tptp.'D_b_d_vec_fun$'| (as |@_tptp.'D_b_d_vec_fun$'__0| |tptp.'D_b_d_vec_fun$'|)) % 140.07/140.36 (define-fun |tptp.'uzt$'| (($x1 |tptp.'B_d_vec_d_vec$'|) ($x2 |tptp.'B_d_vec_d_vec$'|)) |tptp.'D_b_d_vec_fun$'| (as |@_tptp.'D_b_d_vec_fun$'__0| |tptp.'D_b_d_vec_fun$'|)) % 140.07/140.36 (define-fun |tptp.'vec_lambda$c'| (($x1 |tptp.'A_b_fun$'|)) |tptp.'B_a_vec$'| (as |@_tptp.'B_a_vec$'__0| |tptp.'B_a_vec$'|)) % 140.07/140.36 (define-fun |tptp.'uwe$'| (($x1 |tptp.'B_d_vec_a_vec$'|) ($x2 |tptp.'D$'|)) |tptp.'A_b_fun$'| (as |@_tptp.'A_b_fun$'__0| |tptp.'A_b_fun$'|)) % 140.07/140.36 (define-fun |tptp.'row_add_row$b'| ((BOUND_VARIABLE_58788 |tptp.'B_a_vec_c_vec$'|) (BOUND_VARIABLE_58790 |tptp.'C$'|) (BOUND_VARIABLE_58792 |tptp.'C$'|) (BOUND_VARIABLE_58794 |tptp.'B$'|)) |tptp.'C_b_a_vec_fun$'| (as |@_tptp.'C_b_a_vec_fun$'__0| |tptp.'C_b_a_vec_fun$'|)) % 140.07/140.36 (define-fun |tptp.'elt_set_times$'| (($x1 |tptp.'A_b_d_vec_fun$'|) ($x2 |tptp.'A_b_d_vec_fun_set$'|)) |tptp.'A_b_d_vec_fun_set$'| (as |@_tptp.'A_b_d_vec_fun_set$'__0| |tptp.'A_b_d_vec_fun_set$'|)) % 140.07/140.36 (define-fun |tptp.'uws$'| (($x1 |tptp.'B_c_vec_a_vec$'|)) |tptp.'C_b_a_vec_fun$'| (as |@_tptp.'C_b_a_vec_fun$'__0| |tptp.'C_b_a_vec_fun$'|)) % 140.07/140.36 (define-fun |tptp.'uyc$'| (($x1 |tptp.'B_a_vec_c_vec$'|) ($x2 |tptp.'C$'|)) |tptp.'C_b_a_vec_fun$'| (as |@_tptp.'C_b_a_vec_fun$'__0| |tptp.'C_b_a_vec_fun$'|)) % 140.07/140.36 (define-fun |tptp.'fun_app$ak'| (($x1 |tptp.'B_c_vec_bool_fun$'|) ($x2 |tptp.'B_c_vec$'|)) Bool true) % 140.07/140.36 (define-fun |tptp.'fun_app$e'| (($x1 |tptp.'A_b_d_vec_fun_bool_fun$'|) ($x2 |tptp.'A_b_d_vec_fun$'|)) Bool true) % 140.07/140.36 (define-fun |tptp.'uzp$'| (($x1 |tptp.'B_d_vec_a_vec$'|) ($x2 |tptp.'A$'|) ($x3 |tptp.'B$'|) ($x4 |tptp.'A$'|)) |tptp.'D_b_fun$'| (as |@_tptp.'D_b_fun$'__0| |tptp.'D_b_fun$'|)) % 140.07/140.36 (define-fun |tptp.'uub$'| (($x1 |tptp.'A$'|) ($x2 |tptp.'D$'|) ($x3 |tptp.'B_d_vec_a_vec$'|) ($x4 |tptp.'B_d_vec_a_vec$'|)) |tptp.'A_b_d_vec_fun$'| (as |@_tptp.'A_b_d_vec_fun$'__0| |tptp.'A_b_d_vec_fun$'|)) % 140.07/140.36 (define-fun |tptp.'vec$e'| (($x1 |tptp.'B_d_vec$'|)) |tptp.'B_d_vec_d_vec$'| (as |@_tptp.'B_d_vec_d_vec$'__0| |tptp.'B_d_vec_d_vec$'|)) % 140.07/140.36 (define-fun |tptp.'row$c'| ((BOUND_VARIABLE_58810 |tptp.'A$'|) (BOUND_VARIABLE_58812 |tptp.'B_c_vec_a_vec$'|)) |tptp.'B_c_vec$'| (as |@_tptp.'B_c_vec$'__0| |tptp.'B_c_vec$'|)) % 140.07/140.36 (define-fun |tptp.'column_add$'| ((BOUND_VARIABLE_58832 |tptp.'B_d_vec_d_vec$'|) (BOUND_VARIABLE_58834 |tptp.'D$'|) (BOUND_VARIABLE_58836 |tptp.'D$'|) (BOUND_VARIABLE_58838 |tptp.'B$'|)) |tptp.'B_d_vec_d_vec$'| (as |@_tptp.'B_d_vec_d_vec$'__0| |tptp.'B_d_vec_d_vec$'|)) % 140.07/140.36 (define-fun |tptp.'rows$d'| (($x1 |tptp.'B_d_vec_a_vec$'|)) |tptp.'B_d_vec_set$'| (as |@_tptp.'B_d_vec_set$'__0| |tptp.'B_d_vec_set$'|)) % 140.07/140.36 (define-fun |tptp.'column$f'| ((BOUND_VARIABLE_58852 |tptp.'A$'|) (BOUND_VARIABLE_58854 |tptp.'B_a_vec_c_vec$'|)) |tptp.'B_c_vec$'| (as |@_tptp.'B_c_vec$'__0| |tptp.'B_c_vec$'|)) % 140.07/140.36 (define-fun |tptp.'uwo$'| (($x1 |tptp.'B_a_vec_c_vec$'|) ($x2 |tptp.'A$'|) ($x3 |tptp.'A$'|)) |tptp.'C_b_a_vec_fun$'| (as |@_tptp.'C_b_a_vec_fun$'__0| |tptp.'C_b_a_vec_fun$'|)) % 140.07/140.36 (define-fun |tptp.'uyn$'| (($x1 |tptp.'D_b_fun_set$'|)) |tptp.'D_b_fun_bool_fun$'| (as |@_tptp.'D_b_fun_bool_fun$'__0| |tptp.'D_b_fun_bool_fun$'|)) % 140.07/140.36 (define-fun |tptp.'times$g'| ((BOUND_VARIABLE_57816 |tptp.'B_a_vec_c_vec$'|) (BOUND_VARIABLE_57818 |tptp.'B_a_vec_c_vec$'|)) |tptp.'B_a_vec_c_vec$'| (as |@_tptp.'B_a_vec_c_vec$'__0| |tptp.'B_a_vec_c_vec$'|)) % 140.07/140.36 (define-fun |tptp.'plus$e'| ((BOUND_VARIABLE_58871 |tptp.'B_c_vec_a_vec_a_vec$'|) (BOUND_VARIABLE_58873 |tptp.'B_c_vec_a_vec_a_vec$'|)) |tptp.'B_c_vec_a_vec_a_vec$'| (as |@_tptp.'B_c_vec_a_vec_a_vec$'__0| |tptp.'B_c_vec_a_vec_a_vec$'|)) % 140.07/140.36 (define-fun |tptp.'vbc$'| (($x1 |tptp.'B_a_vec$'|)) |tptp.'C_b_a_vec_fun$'| (as |@_tptp.'C_b_a_vec_fun$'__0| |tptp.'C_b_a_vec_fun$'|)) % 140.07/140.36 (define-fun |tptp.'uyd$'| (($x1 |tptp.'B_a_vec_c_vec$'|)) |tptp.'C_b_a_vec_c_vec_fun$'| (as |@_tptp.'C_b_a_vec_c_vec_fun$'__0| |tptp.'C_b_a_vec_c_vec_fun$'|)) % 140.07/140.36 (define-fun |tptp.'rows$a'| (($x1 |tptp.'B_c_vec_a_vec_a_vec$'|)) |tptp.'B_c_vec_a_vec_set$'| (as |@_tptp.'B_c_vec_a_vec_set$'__0| |tptp.'B_c_vec_a_vec_set$'|)) % 140.07/140.36 (define-fun |tptp.'fun_app$c'| (($x1 |tptp.'A_b_d_vec_fun$'|) ($x2 |tptp.'A$'|)) |tptp.'B_d_vec$'| (as |@_tptp.'B_d_vec$'__0| |tptp.'B_d_vec$'|)) % 140.07/140.36 (define-fun |tptp.'uwj$'| (($x1 |tptp.'B_c_vec_c_vec$'|) ($x2 |tptp.'C$'|)) |tptp.'C_b_fun$'| (as |@_tptp.'C_b_fun$'__0| |tptp.'C_b_fun$'|)) % 140.07/140.36 (define-fun |tptp.'uuc$'| (($x1 |tptp.'A$'|) ($x2 |tptp.'C$'|) ($x3 |tptp.'B_c_vec_a_vec$'|) ($x4 |tptp.'B_c_vec_a_vec$'|)) |tptp.'A_b_c_vec_fun$'| (as |@_tptp.'A_b_c_vec_fun$'__1| |tptp.'A_b_c_vec_fun$'|)) % 140.07/140.36 (define-fun |tptp.'fun_app$ai'| (($x1 |tptp.'C_b_bool_fun_fun$'|) ($x2 |tptp.'C$'|)) |tptp.'B_bool_fun$'| (as |@_tptp.'B_bool_fun$'__0| |tptp.'B_bool_fun$'|)) % 140.07/140.36 (define-fun |tptp.'gauss_Jordan_wrapper$a'| ((BOUND_VARIABLE_58893 |tptp.'A$'|) (BOUND_VARIABLE_58895 |tptp.'D$'|) (BOUND_VARIABLE_58897 |tptp.'B_d_vec_a_vec$'|) (BOUND_VARIABLE_58899 |tptp.'B_d_vec_a_vec$'|)) |tptp.'B_d_vec_a_vec$'| (as |@_tptp.'B_d_vec_a_vec$'__0| |tptp.'B_d_vec_a_vec$'|)) % 140.07/140.36 (define-fun |tptp.'vec_lambda$'| (($x1 |tptp.'A_b_d_vec_fun$'|)) |tptp.'B_d_vec_a_vec$'| (as |@_tptp.'B_d_vec_a_vec$'__0| |tptp.'B_d_vec_a_vec$'|)) % 140.07/140.36 (define-fun |tptp.'fun_app$m'| (($x1 |tptp.'D_b_c_vec_fun$'|) ($x2 |tptp.'D$'|)) |tptp.'B_c_vec$'| (as |@_tptp.'B_c_vec$'__0| |tptp.'B_c_vec$'|)) % 140.07/140.36 (define-fun |tptp.'map_matrix$c'| ((BOUND_VARIABLE_58914 |tptp.'B_b_c_vec_fun$'|) (BOUND_VARIABLE_58916 |tptp.'B_a_vec_c_vec$'|)) |tptp.'B_c_vec_a_vec_c_vec$'| (as |@_tptp.'B_c_vec_a_vec_c_vec$'__0| |tptp.'B_c_vec_a_vec_c_vec$'|)) % 140.07/140.36 (define-fun |tptp.'columnvector$c'| ((BOUND_VARIABLE_58925 |tptp.'B_c_vec$'|)) |tptp.'B_c_vec_c_vec$'| (as |@_tptp.'B_c_vec_c_vec$'__0| |tptp.'B_c_vec_c_vec$'|)) % 140.07/140.36 (define-fun |tptp.'uxc$'| (($x1 |tptp.'C$'|) ($x2 |tptp.'B_c_vec_a_vec$'|)) |tptp.'A_b_fun$'| (as |@_tptp.'A_b_fun$'__0| |tptp.'A_b_fun$'|)) % 140.07/140.36 (define-fun |tptp.'vaq$'| (($x1 |tptp.'B_c_vec_a_vec_a_vec$'|) ($x2 |tptp.'A$'|) ($x3 |tptp.'A$'|) ($x4 |tptp.'B_c_vec$'|)) |tptp.'A_b_c_vec_a_vec_fun$'| (as |@_tptp.'A_b_c_vec_a_vec_fun$'__0| |tptp.'A_b_c_vec_a_vec_fun$'|)) % 140.07/140.36 (define-fun |tptp.'uminus$f'| ((BOUND_VARIABLE_58932 |tptp.'B_d_vec_d_vec$'|)) |tptp.'B_d_vec_d_vec$'| (as |@_tptp.'B_d_vec_d_vec$'__0| |tptp.'B_d_vec_d_vec$'|)) % 140.07/140.36 (define-fun |tptp.'columnvector$b'| ((BOUND_VARIABLE_58942 |tptp.'B_d_vec$'|)) |tptp.'B_c_vec_d_vec$'| (as |@_tptp.'B_c_vec_d_vec$'__0| |tptp.'B_c_vec_d_vec$'|)) % 140.07/140.36 (define-fun |tptp.'var$'| (($x1 |tptp.'B_d_vec_a_vec$'|) ($x2 |tptp.'D$'|) ($x3 |tptp.'D$'|) ($x4 |tptp.'B$'|)) |tptp.'A_b_d_vec_fun$'| (as |@_tptp.'A_b_d_vec_fun$'__0| |tptp.'A_b_d_vec_fun$'|)) % 140.07/140.36 (define-fun |tptp.'vad$'| (($x1 |tptp.'B_c_vec$'|) ($x2 |tptp.'B_c_vec$'|)) |tptp.'C_b_fun$'| (as |@_tptp.'C_b_fun$'__0| |tptp.'C_b_fun$'|)) % 140.07/140.36 (define-fun |tptp.'uuj$'| (($x1 |tptp.'C$'|) ($x2 |tptp.'C$'|) ($x3 |tptp.'B_a_vec_c_vec$'|) ($x4 |tptp.'B_c_vec_c_vec$'|)) |tptp.'C_b_a_vec_fun$'| (as |@_tptp.'C_b_a_vec_fun$'__0| |tptp.'C_b_a_vec_fun$'|)) % 140.07/140.36 (define-fun |tptp.'member$l'| (($x1 |tptp.'A_b_fun$'|) ($x2 |tptp.'A_b_fun_set$'|)) Bool true) % 140.07/140.36 (define-fun |tptp.'uuh$'| (($x1 |tptp.'A$'|) ($x2 |tptp.'A$'|) ($x3 |tptp.'B_c_vec_a_vec$'|) ($x4 |tptp.'B_a_vec_a_vec$'|)) |tptp.'A_b_c_vec_fun$'| (as |@_tptp.'A_b_c_vec_fun$'__1| |tptp.'A_b_c_vec_fun$'|)) % 140.07/140.36 (define-fun |tptp.'collect$'| (($x1 |tptp.'A_b_d_vec_fun_bool_fun$'|)) |tptp.'A_b_d_vec_fun_set$'| (as |@_tptp.'A_b_d_vec_fun_set$'__0| |tptp.'A_b_d_vec_fun_set$'|)) % 140.07/140.36 (define-fun |tptp.'vec_nth$'| (($x1 |tptp.'B_c_vec_a_vec$'|)) |tptp.'A_b_c_vec_fun$'| (as |@_tptp.'A_b_c_vec_fun$'__1| |tptp.'A_b_c_vec_fun$'|)) % 140.07/140.36 (define-fun |tptp.'interchange_columns$a'| ((BOUND_VARIABLE_58961 |tptp.'B_a_vec_c_vec$'|) (BOUND_VARIABLE_58963 |tptp.'A$'|) (BOUND_VARIABLE_58965 |tptp.'A$'|)) |tptp.'B_a_vec_c_vec$'| (as |@_tptp.'B_a_vec_c_vec$'__0| |tptp.'B_a_vec_c_vec$'|)) % 140.07/140.36 (define-fun |tptp.'uwn$'| (($x1 |tptp.'B_d_vec_d_vec$'|) ($x2 |tptp.'D$'|) ($x3 |tptp.'D$'|)) |tptp.'D_b_d_vec_fun$'| (as |@_tptp.'D_b_d_vec_fun$'__0| |tptp.'D_b_d_vec_fun$'|)) % 140.07/140.36 (define-fun |tptp.'vec_nth$c'| (($x1 |tptp.'B_c_vec_a_vec_a_vec$'|)) |tptp.'A_b_c_vec_a_vec_fun$'| (as |@_tptp.'A_b_c_vec_a_vec_fun$'__0| |tptp.'A_b_c_vec_a_vec_fun$'|)) % 140.07/140.36 (define-fun |tptp.'vec_lambda$h'| (($x1 |tptp.'C_b_d_vec_fun$'|)) |tptp.'B_d_vec_c_vec$'| (as |@_tptp.'B_d_vec_c_vec$'__0| |tptp.'B_d_vec_c_vec$'|)) % 140.07/140.36 (define-fun |tptp.'vbe$'| (($x1 |tptp.'B_c_vec_a_vec$'|)) |tptp.'A_b_c_vec_a_vec_fun$'| (as |@_tptp.'A_b_c_vec_a_vec_fun$'__0| |tptp.'A_b_c_vec_a_vec_fun$'|)) % 140.07/140.36 (define-fun |tptp.'uuo$'| (($x1 |tptp.'B_a_vec$'|)) |tptp.'A_b_fun$'| (as |@_tptp.'A_b_fun$'__0| |tptp.'A_b_fun$'|)) % 140.07/140.36 (define-fun |tptp.'uxs$'| (($x1 |tptp.'B_c_vec$'|) ($x2 |tptp.'C$'|)) |tptp.'C_b_fun$'| (as |@_tptp.'C_b_fun$'__0| |tptp.'C_b_fun$'|)) % 140.07/140.36 (define-fun |tptp.'vector_scalar_mult$'| ((BOUND_VARIABLE_58977 |tptp.'B_d_vec$'|) (BOUND_VARIABLE_58979 |tptp.'B_d_vec_d_vec$'|)) |tptp.'B_d_vec_d_vec$'| (as |@_tptp.'B_d_vec_d_vec$'__0| |tptp.'B_d_vec_d_vec$'|)) % 140.07/140.36 (define-fun |tptp.'times$o'| (($x1 |tptp.'B_set$'|) ($x2 |tptp.'B_set$'|)) |tptp.'B_set$'| (as |@_tptp.'B_set$'__0| |tptp.'B_set$'|)) % 140.07/140.36 (define-fun |tptp.'member$h'| (($x1 |tptp.'A_b_c_vec_a_vec_fun$'|) ($x2 |tptp.'A_b_c_vec_a_vec_fun_set$'|)) Bool true) % 140.07/140.36 (define-fun |tptp.'vaf$'| (($x1 |tptp.'B_a_vec$'|) ($x2 |tptp.'B_a_vec$'|)) |tptp.'A_b_fun$'| (as |@_tptp.'A_b_fun$'__0| |tptp.'A_b_fun$'|)) % 140.07/140.36 (define-fun |tptp.'uzs$'| (($x1 |tptp.'B_c_vec_a_vec$'|) ($x2 |tptp.'A$'|) ($x3 |tptp.'B$'|)) |tptp.'A_b_c_vec_fun$'| (as |@_tptp.'A_b_c_vec_fun$'__1| |tptp.'A_b_c_vec_fun$'|)) % 140.07/140.36 (define-fun |tptp.'vec_lambda$p'| ((_arg_1 |tptp.'C_b_a_vec_c_vec_fun$'|)) |tptp.'B_a_vec_c_vec_c_vec$'| (as |@_tptp.'B_a_vec_c_vec_c_vec$'__0| |tptp.'B_a_vec_c_vec_c_vec$'|)) % 140.07/140.36 (define-fun |tptp.'top$g'| () |tptp.'A_b_d_vec_fun_set$'| (as |@_tptp.'A_b_d_vec_fun_set$'__0| |tptp.'A_b_d_vec_fun_set$'|)) % 140.07/140.36 (define-fun |tptp.'uxj$'| (($x1 |tptp.'A$'|) ($x2 |tptp.'B_a_vec_a_vec$'|)) |tptp.'A_b_fun$'| (as |@_tptp.'A_b_fun$'__0| |tptp.'A_b_fun$'|)) % 140.07/140.36 (define-fun |tptp.'mult_row_row$c'| ((BOUND_VARIABLE_58997 |tptp.'B_c_vec_a_vec$'|) (BOUND_VARIABLE_58999 |tptp.'A$'|) (BOUND_VARIABLE_59001 |tptp.'B$'|)) |tptp.'A_b_c_vec_fun$'| (as |@_tptp.'A_b_c_vec_fun$'__1| |tptp.'A_b_c_vec_fun$'|)) % 140.07/140.36 (define-fun |tptp.'plus$f'| ((BOUND_VARIABLE_58373 |tptp.'B_d_vec_d_vec$'|) (BOUND_VARIABLE_58375 |tptp.'B_d_vec_d_vec$'|)) |tptp.'B_d_vec_d_vec$'| (as |@_tptp.'B_d_vec_d_vec$'__0| |tptp.'B_d_vec_d_vec$'|)) % 140.07/140.36 (define-fun |tptp.'uwv$'| (($x1 |tptp.'B_c_vec_a_vec_a_vec$'|)) |tptp.'A_b_c_vec_a_vec_fun$'| (as |@_tptp.'A_b_c_vec_a_vec_fun$'__0| |tptp.'A_b_c_vec_a_vec_fun$'|)) % 140.07/140.36 (define-fun |tptp.'uud$'| (($x1 |tptp.'A$'|) ($x2 |tptp.'D$'|) ($x3 |tptp.'B_c_vec_a_vec$'|) ($x4 |tptp.'B_d_vec_a_vec$'|)) |tptp.'A_b_c_vec_fun$'| (as |@_tptp.'A_b_c_vec_fun$'__1| |tptp.'A_b_c_vec_fun$'|)) % 140.07/140.36 (define-fun |tptp.'fun_app$g'| (($x1 |tptp.'A_b_d_vec_a_vec_fun$'|) ($x2 |tptp.'A$'|)) |tptp.'B_d_vec_a_vec$'| (as |@_tptp.'B_d_vec_a_vec$'__0| |tptp.'B_d_vec_a_vec$'|)) % 140.07/140.36 (define-fun |tptp.'vec$d'| ((BOUND_VARIABLE_57311 |tptp.'B_c_vec_a_vec$'|)) |tptp.'B_c_vec_a_vec_a_vec$'| (as |@_tptp.'B_c_vec_a_vec_a_vec$'__0| |tptp.'B_c_vec_a_vec_a_vec$'|)) % 140.07/140.36 (define-fun |tptp.'rows$b'| (($x1 |tptp.'B_a_vec_d_vec$'|)) |tptp.'B_a_vec_set$'| (as |@_tptp.'B_a_vec_set$'__0| |tptp.'B_a_vec_set$'|)) % 140.07/140.36 (define-fun |tptp.'vao$'| (($x1 |tptp.'B_d_vec_d_vec$'|) ($x2 |tptp.'D$'|) ($x3 |tptp.'D$'|) ($x4 |tptp.'B$'|)) |tptp.'D_b_d_vec_fun$'| (as |@_tptp.'D_b_d_vec_fun$'__0| |tptp.'D_b_d_vec_fun$'|)) % 140.07/140.36 (define-fun |tptp.'uuv$'| (($x1 |tptp.'B_b_fun$'|) ($x2 |tptp.'B_c_vec_a_vec$'|)) |tptp.'A_b_c_vec_fun$'| (as |@_tptp.'A_b_c_vec_fun$'__1| |tptp.'A_b_c_vec_fun$'|)) % 140.07/140.36 (define-fun |tptp.'uwi$'| (($x1 |tptp.'B_d_vec_c_vec$'|) ($x2 |tptp.'D$'|)) |tptp.'C_b_fun$'| (as |@_tptp.'C_b_fun$'__0| |tptp.'C_b_fun$'|)) % 140.07/140.36 (define-fun |tptp.'vba$'| (($x1 |tptp.'B_c_vec$'|) ($x2 |tptp.'B_c_vec_a_vec$'|)) |tptp.'A_b_c_vec_fun$'| (as |@_tptp.'A_b_c_vec_fun$'__1| |tptp.'A_b_c_vec_fun$'|)) % 140.07/140.36 (define-fun |tptp.'fun_app$t'| (($x1 |tptp.'A_b_a_vec_c_vec_fun$'|) ($x2 |tptp.'A$'|)) |tptp.'B_a_vec_c_vec$'| (as |@_tptp.'B_a_vec_c_vec$'__0| |tptp.'B_a_vec_c_vec$'|)) % 140.07/140.36 (define-fun |tptp.'uwb$'| (($x1 |tptp.'B_c_vec_a_vec$'|) ($x2 |tptp.'A$'|) ($x3 |tptp.'A$'|) ($x4 |tptp.'A$'|)) |tptp.'C_b_fun$'| (as |@_tptp.'C_b_fun$'__0| |tptp.'C_b_fun$'|)) % 140.07/140.36 (define-fun |tptp.'elt_set_plus$d'| (($x1 |tptp.'B_d_vec_a_vec$'|) ($x2 |tptp.'B_d_vec_a_vec_set$'|)) |tptp.'B_d_vec_a_vec_set$'| (as |@_tptp.'B_d_vec_a_vec_set$'__0| |tptp.'B_d_vec_a_vec_set$'|)) % 140.07/140.36 (define-fun |tptp.'elt_set_times$c'| (($x1 |tptp.'B$'|) ($x2 |tptp.'B_set$'|)) |tptp.'B_set$'| (as |@_tptp.'B_set$'__0| |tptp.'B_set$'|)) % 140.07/140.36 (define-fun |tptp.'times$q'| (($x1 |tptp.'B_d_vec_set$'|) ($x2 |tptp.'B_d_vec_set$'|)) |tptp.'B_d_vec_set$'| (as |@_tptp.'B_d_vec_set$'__0| |tptp.'B_d_vec_set$'|)) % 140.07/140.36 (define-fun |tptp.'elt_set_plus$f'| (($x1 |tptp.'B_c_vec_a_vec$'|) ($x2 |tptp.'B_c_vec_a_vec_set$'|)) |tptp.'B_c_vec_a_vec_set$'| (as |@_tptp.'B_c_vec_a_vec_set$'__0| |tptp.'B_c_vec_a_vec_set$'|)) % 140.07/140.36 (define-fun |tptp.'column$'| ((BOUND_VARIABLE_59022 |tptp.'C$'|) (BOUND_VARIABLE_59024 |tptp.'B_c_vec_a_vec$'|)) |tptp.'B_a_vec$'| (as |@_tptp.'B_a_vec$'__0| |tptp.'B_a_vec$'|)) % 140.07/140.36 (define-fun |tptp.'uvu$'| (($x1 |tptp.'B_c_vec_a_vec_a_vec$'|) ($x2 |tptp.'A$'|) ($x3 |tptp.'A$'|) ($x4 |tptp.'A$'|)) |tptp.'A_b_c_vec_fun$'| (as |@_tptp.'A_b_c_vec_fun$'__1| |tptp.'A_b_c_vec_fun$'|)) % 140.07/140.36 (define-fun tptp.tlfalse () tptp.tlbool (as @tptp.tlbool_0 tptp.tlbool)) % 140.07/140.36 (define-fun |tptp.'fun_app$af'| (($x1 |tptp.'B_a_vec_bool_fun$'|) ($x2 |tptp.'B_a_vec$'|)) Bool true) % 140.07/140.36 (define-fun |tptp.'column$g'| ((BOUND_VARIABLE_59038 |tptp.'A$'|) (BOUND_VARIABLE_59040 |tptp.'B_a_vec_a_vec$'|)) |tptp.'B_a_vec$'| (as |@_tptp.'B_a_vec$'__0| |tptp.'B_a_vec$'|)) % 140.07/140.36 (define-fun |tptp.'vbb$'| (($x1 |tptp.'B$'|)) |tptp.'D_b_fun$'| (as |@_tptp.'D_b_fun$'__0| |tptp.'D_b_fun$'|)) % 140.07/140.36 (define-fun |tptp.'uvn$'| (($x1 |tptp.'B_d_vec_b_fun$'|) ($x2 |tptp.'B_d_vec_a_vec_c_vec$'|)) |tptp.'C_b_a_vec_fun$'| (as |@_tptp.'C_b_a_vec_fun$'__0| |tptp.'C_b_a_vec_fun$'|)) % 140.07/140.36 (define-fun |tptp.'uwc$'| (($x1 |tptp.'B_d_vec_a_vec$'|) ($x2 |tptp.'A$'|) ($x3 |tptp.'A$'|) ($x4 |tptp.'A$'|)) |tptp.'D_b_fun$'| (as |@_tptp.'D_b_fun$'__0| |tptp.'D_b_fun$'|)) % 140.07/140.36 (define-fun |tptp.'uzw$'| (($x1 |tptp.'B_c_vec_a_vec_a_vec$'|) ($x2 |tptp.'B_c_vec_a_vec_a_vec$'|)) |tptp.'A_b_c_vec_a_vec_fun$'| (as |@_tptp.'A_b_c_vec_a_vec_fun$'__0| |tptp.'A_b_c_vec_a_vec_fun$'|)) % 140.07/140.36 (define-fun |tptp.'fun_app$av'| (($x1 |tptp.'B_d_vec_a_vec_bool_fun$'|) ($x2 |tptp.'B_d_vec_a_vec$'|)) Bool false) % 140.07/140.36 (define-fun |tptp.'vak$'| (($x1 |tptp.'B_c_vec_a_vec_a_vec$'|) ($x2 |tptp.'A$'|) ($x3 |tptp.'A$'|) ($x4 |tptp.'B_c_vec$'|) ($x5 |tptp.'A$'|)) |tptp.'A_b_c_vec_fun$'| (as |@_tptp.'A_b_c_vec_fun$'__1| |tptp.'A_b_c_vec_fun$'|)) % 140.07/140.36 (define-fun |tptp.'row_add_row$c'| ((BOUND_VARIABLE_59064 |tptp.'B_c_vec_a_vec$'|) (BOUND_VARIABLE_59066 |tptp.'A$'|) (BOUND_VARIABLE_59068 |tptp.'A$'|) (BOUND_VARIABLE_59070 |tptp.'B$'|)) |tptp.'A_b_c_vec_fun$'| (as |@_tptp.'A_b_c_vec_fun$'__1| |tptp.'A_b_c_vec_fun$'|)) % 140.07/140.36 (define-fun |tptp.'columnvector_row$f'| (($x1 |tptp.'B_c_vec$'|)) |tptp.'C_b_a_vec_fun$'| (as |@_tptp.'C_b_a_vec_fun$'__0| |tptp.'C_b_a_vec_fun$'|)) % 140.07/140.36 (define-fun |tptp.'vector_scalar_mult$c'| ((BOUND_VARIABLE_59082 |tptp.'B_c_vec_a_vec$'|) (BOUND_VARIABLE_59084 |tptp.'B_c_vec_a_vec_a_vec$'|)) |tptp.'B_c_vec_a_vec_a_vec$'| (as |@_tptp.'B_c_vec_a_vec_a_vec$'__0| |tptp.'B_c_vec_a_vec_a_vec$'|)) % 140.07/140.36 (define-fun |tptp.'row_add$'| ((BOUND_VARIABLE_59104 |tptp.'B_c_vec_a_vec$'|) (BOUND_VARIABLE_59106 |tptp.'A$'|) (BOUND_VARIABLE_59108 |tptp.'A$'|) (BOUND_VARIABLE_59110 |tptp.'B$'|)) |tptp.'B_c_vec_a_vec$'| (as |@_tptp.'B_c_vec_a_vec$'__0| |tptp.'B_c_vec_a_vec$'|)) % 140.07/140.36 (define-fun |tptp.'row_add$c'| ((BOUND_VARIABLE_59130 |tptp.'B_d_vec_a_vec$'|) (BOUND_VARIABLE_59132 |tptp.'A$'|) (BOUND_VARIABLE_59134 |tptp.'A$'|) (BOUND_VARIABLE_59136 |tptp.'B$'|)) |tptp.'B_d_vec_a_vec$'| (as |@_tptp.'B_d_vec_a_vec$'__0| |tptp.'B_d_vec_a_vec$'|)) % 140.07/140.36 (define-fun |tptp.'uxi$'| (($x1 |tptp.'A$'|) ($x2 |tptp.'B_a_vec_c_vec$'|)) |tptp.'C_b_fun$'| (as |@_tptp.'C_b_fun$'__0| |tptp.'C_b_fun$'|)) % 140.07/140.36 (define-fun |tptp.'map_matrix$f'| ((BOUND_VARIABLE_59151 |tptp.'B_c_vec_b_fun$'|) (BOUND_VARIABLE_59153 |tptp.'B_c_vec_a_vec_a_vec$'|)) |tptp.'B_a_vec_a_vec$'| (as |@_tptp.'B_a_vec_a_vec$'__0| |tptp.'B_a_vec_a_vec$'|)) % 140.07/140.36 (define-fun |tptp.'uze$'| (($x1 |tptp.'B_c_vec_a_vec_a_vec$'|) ($x2 |tptp.'A$'|) ($x3 |tptp.'A$'|) ($x4 |tptp.'B_c_vec$'|)) |tptp.'A_b_c_vec_a_vec_fun$'| (as |@_tptp.'A_b_c_vec_a_vec_fun$'__0| |tptp.'A_b_c_vec_a_vec_fun$'|)) % 140.07/140.36 (define-fun |tptp.'fun_app$ah'| (($x1 |tptp.'B_bool_fun$'|) ($x2 |tptp.'B$'|)) Bool true) % 140.07/140.36 (define-fun |tptp.'interchange_columns_row$b'| ((BOUND_VARIABLE_59172 |tptp.'B_a_vec_c_vec$'|) (BOUND_VARIABLE_59174 |tptp.'A$'|) (BOUND_VARIABLE_59176 |tptp.'A$'|)) |tptp.'C_b_a_vec_fun$'| (as |@_tptp.'C_b_a_vec_fun$'__0| |tptp.'C_b_a_vec_fun$'|)) % 140.07/140.36 (define-fun |tptp.'times$p'| (($x1 |tptp.'B_d_vec_a_vec_set$'|) ($x2 |tptp.'B_d_vec_a_vec_set$'|)) |tptp.'B_d_vec_a_vec_set$'| (as |@_tptp.'B_d_vec_a_vec_set$'__0| |tptp.'B_d_vec_a_vec_set$'|)) % 140.07/140.36 (define-fun |tptp.'uvg$'| (($x1 |tptp.'B_c_vec_b_fun$'|) ($x2 |tptp.'B_c_vec_a_vec_a_vec$'|) ($x3 |tptp.'A$'|)) |tptp.'A_b_fun$'| (as |@_tptp.'A_b_fun$'__0| |tptp.'A_b_fun$'|)) % 140.07/140.36 (define-fun |tptp.'uue$'| (($x1 |tptp.'D$'|) ($x2 |tptp.'D$'|) ($x3 |tptp.'B_d_vec_d_vec$'|) ($x4 |tptp.'B_d_vec_d_vec$'|)) |tptp.'D_b_d_vec_fun$'| (as |@_tptp.'D_b_d_vec_fun$'__0| |tptp.'D_b_d_vec_fun$'|)) % 140.07/140.36 (define-fun |tptp.'column_add$b'| ((BOUND_VARIABLE_58631 |tptp.'B_c_vec_a_vec_a_vec$'|) (BOUND_VARIABLE_58633 |tptp.'A$'|) (BOUND_VARIABLE_58635 |tptp.'A$'|) (BOUND_VARIABLE_58637 |tptp.'B_c_vec$'|)) |tptp.'B_c_vec_a_vec_a_vec$'| (as |@_tptp.'B_c_vec_a_vec_a_vec$'__0| |tptp.'B_c_vec_a_vec_a_vec$'|)) % 140.07/140.36 (define-fun |tptp.'uvk$'| (($x1 |tptp.'B_c_vec_b_fun$'|) ($x2 |tptp.'B_c_vec_a_vec_c_vec$'|) ($x3 |tptp.'C$'|)) |tptp.'A_b_fun$'| (as |@_tptp.'A_b_fun$'__0| |tptp.'A_b_fun$'|)) % 140.07/140.36 (define-fun |tptp.'row_add$b'| ((BOUND_VARIABLE_59209 |tptp.'B_a_vec_c_vec$'|) (BOUND_VARIABLE_59211 |tptp.'C$'|) (BOUND_VARIABLE_59213 |tptp.'C$'|) (BOUND_VARIABLE_59215 |tptp.'B$'|)) |tptp.'B_a_vec_c_vec$'| (as |@_tptp.'B_a_vec_c_vec$'__0| |tptp.'B_a_vec_c_vec$'|)) % 140.07/140.36 (define-fun |tptp.'column$c'| ((BOUND_VARIABLE_57595 |tptp.'D$'|) (BOUND_VARIABLE_57597 |tptp.'B_d_vec_d_vec$'|)) |tptp.'B_d_vec$'| (as |@_tptp.'B_d_vec$'__0| |tptp.'B_d_vec$'|)) % 140.07/140.36 (define-fun |tptp.'fun_app$y'| (($x1 |tptp.'B_b_d_vec_fun$'|) ($x2 |tptp.'B$'|)) |tptp.'B_d_vec$'| (as |@_tptp.'B_d_vec$'__0| |tptp.'B_d_vec$'|)) % 140.07/140.36 (define-fun |tptp.'transpose_row$a'| ((BOUND_VARIABLE_59230 |tptp.'B_d_vec_a_vec$'|)) |tptp.'D_b_a_vec_fun$'| (as |@_tptp.'D_b_a_vec_fun$'__0| |tptp.'D_b_a_vec_fun$'|)) % 140.07/140.36 (define-fun |tptp.'top$f'| () |tptp.'D_b_fun_set$'| (as |@_tptp.'D_b_fun_set$'__0| |tptp.'D_b_fun_set$'|)) % 140.07/140.36 (define-fun |tptp.'mult_column_row$'| ((BOUND_VARIABLE_59245 |tptp.'B_d_vec_d_vec$'|) (BOUND_VARIABLE_59247 |tptp.'D$'|) (BOUND_VARIABLE_59249 |tptp.'B$'|)) |tptp.'D_b_d_vec_fun$'| (as |@_tptp.'D_b_d_vec_fun$'__0| |tptp.'D_b_d_vec_fun$'|)) % 140.07/140.36 (define-fun |tptp.'transpose_row$i'| ((BOUND_VARIABLE_59261 |tptp.'B_a_vec_c_vec_c_vec$'|) (BOUND_VARIABLE_59263 |tptp.'C$'|)) |tptp.'B_a_vec_c_vec$'| (as |@_tptp.'B_a_vec_c_vec$'__0| |tptp.'B_a_vec_c_vec$'|)) % 140.07/140.36 (define-fun |tptp.'uyz$'| (($x1 |tptp.'B_d_vec_d_vec$'|) ($x2 |tptp.'D$'|) ($x3 |tptp.'D$'|) ($x4 |tptp.'B$'|) ($x5 |tptp.'D$'|)) |tptp.'D_b_fun$'| (as |@_tptp.'D_b_fun$'__0| |tptp.'D_b_fun$'|)) % 140.07/140.36 (define-fun |tptp.'row$d'| ((BOUND_VARIABLE_59279 |tptp.'A$'|) (BOUND_VARIABLE_59281 |tptp.'B_d_vec_a_vec$'|)) |tptp.'B_d_vec$'| (as |@_tptp.'B_d_vec$'__0| |tptp.'B_d_vec$'|)) % 140.07/140.36 (define-fun |tptp.'uyv$'| (($x1 |tptp.'B_d_vec_a_vec$'|) ($x2 |tptp.'D$'|) ($x3 |tptp.'B$'|) ($x4 |tptp.'A$'|)) |tptp.'D_b_fun$'| (as |@_tptp.'D_b_fun$'__0| |tptp.'D_b_fun$'|)) % 140.07/140.36 (define-fun |tptp.'interchange_rows_row$d'| ((BOUND_VARIABLE_59301 |tptp.'B_d_vec_a_vec$'|) (BOUND_VARIABLE_59303 |tptp.'A$'|) (BOUND_VARIABLE_59305 |tptp.'A$'|)) |tptp.'A_b_d_vec_fun$'| (as |@_tptp.'A_b_d_vec_fun$'__0| |tptp.'A_b_d_vec_fun$'|)) % 140.07/140.36 (define-fun |tptp.'interchange_columns_row$a'| ((BOUND_VARIABLE_59324 |tptp.'B_c_vec_a_vec_a_vec$'|) (BOUND_VARIABLE_59326 |tptp.'A$'|) (BOUND_VARIABLE_59328 |tptp.'A$'|)) |tptp.'A_b_c_vec_a_vec_fun$'| (as |@_tptp.'A_b_c_vec_a_vec_fun$'__0| |tptp.'A_b_c_vec_a_vec_fun$'|)) % 140.07/140.36 (define-fun |tptp.'times$c'| ((BOUND_VARIABLE_57703 |tptp.'B_a_vec$'|) (BOUND_VARIABLE_57705 |tptp.'B_a_vec$'|)) |tptp.'B_a_vec$'| (as |@_tptp.'B_a_vec$'__0| |tptp.'B_a_vec$'|)) % 140.07/140.36 (define-fun |tptp.'fun_app$v'| (($x1 |tptp.'B_d_vec_b_fun$'|) ($x2 |tptp.'B_d_vec$'|)) |tptp.'B$'| (as |@_tptp.'B$'__0| |tptp.'B$'|)) % 140.07/140.36 (define-fun |tptp.'uxu$'| (($x1 |tptp.'B_d_vec$'|) ($x2 |tptp.'D$'|)) |tptp.'A_b_fun$'| (as |@_tptp.'A_b_fun$'__0| |tptp.'A_b_fun$'|)) % 140.07/140.36 (define-fun |tptp.'fun_app$ae'| (($x1 |tptp.'D_b_d_vec_bool_fun_fun$'|) ($x2 |tptp.'D$'|)) |tptp.'B_d_vec_bool_fun$'| (as |@_tptp.'B_d_vec_bool_fun$'__0| |tptp.'B_d_vec_bool_fun$'|)) % 140.07/140.36 (define-fun |tptp.'interchange_columns$d'| ((BOUND_VARIABLE_59352 |tptp.'B_c_vec_a_vec$'|) (BOUND_VARIABLE_59354 |tptp.'C$'|) (BOUND_VARIABLE_59356 |tptp.'C$'|)) |tptp.'B_c_vec_a_vec$'| (as |@_tptp.'B_c_vec_a_vec$'__0| |tptp.'B_c_vec_a_vec$'|)) % 140.07/140.36 (define-fun |tptp.'transpose$d'| ((BOUND_VARIABLE_58932 |tptp.'B_d_vec_d_vec$'|)) |tptp.'B_d_vec_d_vec$'| (as |@_tptp.'B_d_vec_d_vec$'__0| |tptp.'B_d_vec_d_vec$'|)) % 140.07/140.36 (define-fun |tptp.'vac$'| (($x1 |tptp.'B_a_vec_c_vec$'|) ($x2 |tptp.'B_a_vec_c_vec$'|)) |tptp.'C_b_a_vec_fun$'| (as |@_tptp.'C_b_a_vec_fun$'__0| |tptp.'C_b_a_vec_fun$'|)) % 140.07/140.36 (define-fun |tptp.'vec_nth$f'| (($x1 |tptp.'B_c_vec_d_vec$'|)) |tptp.'D_b_c_vec_fun$'| (as |@_tptp.'D_b_c_vec_fun$'__0| |tptp.'D_b_c_vec_fun$'|)) % 140.07/140.36 (define-fun |tptp.'columnvector_row$a'| (($x1 |tptp.'B_d_vec$'|)) |tptp.'D_b_d_vec_fun$'| (as |@_tptp.'D_b_d_vec_fun$'__0| |tptp.'D_b_d_vec_fun$'|)) % 140.07/140.36 (define-fun |tptp.'uzl$'| (($x1 |tptp.'B_a_vec_c_vec$'|) ($x2 |tptp.'C$'|) ($x3 |tptp.'B$'|) ($x4 |tptp.'C$'|)) |tptp.'A_b_fun$'| (as |@_tptp.'A_b_fun$'__0| |tptp.'A_b_fun$'|)) % 140.07/140.36 (define-fun |tptp.'columnvector_row$j'| (($x1 |tptp.'B_c_vec$'|)) |tptp.'C_b_d_vec_fun$'| (as |@_tptp.'C_b_d_vec_fun$'__0| |tptp.'C_b_d_vec_fun$'|)) % 140.07/140.36 (define-fun |tptp.'column_add_row$b'| ((BOUND_VARIABLE_59378 |tptp.'B_a_vec_c_vec$'|) (BOUND_VARIABLE_59380 |tptp.'A$'|) (BOUND_VARIABLE_59382 |tptp.'A$'|) (BOUND_VARIABLE_59384 |tptp.'B$'|)) |tptp.'C_b_a_vec_fun$'| (as |@_tptp.'C_b_a_vec_fun$'__0| |tptp.'C_b_a_vec_fun$'|)) % 140.07/140.36 (define-fun |tptp.'fun_app$f'| (($x1 |tptp.'A_b_c_vec_fun_bool_fun$'|) ($x2 |tptp.'A_b_c_vec_fun$'|)) Bool (and (= (as |@_tptp.'A_b_c_vec_fun_bool_fun$'__0| |tptp.'A_b_c_vec_fun_bool_fun$'|) $x1) (= (as |@_tptp.'A_b_c_vec_fun$'__1| |tptp.'A_b_c_vec_fun$'|) $x2))) % 140.07/140.36 (define-fun |tptp.'uzn$'| (($x1 |tptp.'B_c_vec_a_vec_a_vec$'|) ($x2 |tptp.'A$'|) ($x3 |tptp.'B_c_vec$'|) ($x4 |tptp.'A$'|)) |tptp.'A_b_c_vec_fun$'| (as |@_tptp.'A_b_c_vec_fun$'__1| |tptp.'A_b_c_vec_fun$'|)) % 140.07/140.36 (define-fun |tptp.'uzj$'| (($x1 |tptp.'B_d_vec_d_vec$'|) ($x2 |tptp.'D$'|) ($x3 |tptp.'B$'|) ($x4 |tptp.'D$'|)) |tptp.'D_b_fun$'| (as |@_tptp.'D_b_fun$'__0| |tptp.'D_b_fun$'|)) % 140.07/140.36 (define-fun |tptp.'transpose_row$k'| (($x1 |tptp.'B_c_vec_d_vec$'|)) |tptp.'C_b_d_vec_fun$'| (as |@_tptp.'C_b_d_vec_fun$'__0| |tptp.'C_b_d_vec_fun$'|)) % 140.07/140.36 (define-fun |tptp.'interchange_rows_row$b'| ((BOUND_VARIABLE_59403 |tptp.'B_a_vec_c_vec$'|) (BOUND_VARIABLE_59405 |tptp.'C$'|) (BOUND_VARIABLE_59407 |tptp.'C$'|)) |tptp.'C_b_a_vec_fun$'| (as |@_tptp.'C_b_a_vec_fun$'__0| |tptp.'C_b_a_vec_fun$'|)) % 140.07/140.36 (define-fun |tptp.'rowvector$d'| ((BOUND_VARIABLE_58264 |tptp.'B_c_vec$'|)) |tptp.'B_c_vec_a_vec$'| (as |@_tptp.'B_c_vec_a_vec$'__0| |tptp.'B_c_vec_a_vec$'|)) % 140.07/140.36 (define-fun |tptp.'vec_nth$k'| (($x1 |tptp.'B_c_vec_c_vec$'|) ($x2 |tptp.'C$'|)) |tptp.'B_c_vec$'| (as |@_tptp.'B_c_vec$'__0| |tptp.'B_c_vec$'|)) % 140.07/140.36 (define-fun |tptp.'row$b'| ((BOUND_VARIABLE_59425 |tptp.'C$'|) (BOUND_VARIABLE_59427 |tptp.'B_a_vec_c_vec$'|)) |tptp.'B_a_vec$'| (as |@_tptp.'B_a_vec$'__0| |tptp.'B_a_vec$'|)) % 140.07/140.36 (define-fun |tptp.'mult_row_row$b'| ((BOUND_VARIABLE_59442 |tptp.'B_a_vec_c_vec$'|) (BOUND_VARIABLE_59444 |tptp.'C$'|) (BOUND_VARIABLE_59446 |tptp.'B$'|)) |tptp.'C_b_a_vec_fun$'| (as |@_tptp.'C_b_a_vec_fun$'__0| |tptp.'C_b_a_vec_fun$'|)) % 140.07/140.36 (define-fun |tptp.'top$d'| () |tptp.'A_b_fun_set$'| (as |@_tptp.'A_b_fun_set$'__0| |tptp.'A_b_fun_set$'|)) % 140.07/140.36 (define-fun |tptp.'interchange_rows$b'| ((BOUND_VARIABLE_57535 |tptp.'B_c_vec_a_vec_a_vec$'|) (BOUND_VARIABLE_57537 |tptp.'A$'|) (BOUND_VARIABLE_57539 |tptp.'A$'|)) |tptp.'B_c_vec_a_vec_a_vec$'| (as |@_tptp.'B_c_vec_a_vec_a_vec$'__0| |tptp.'B_c_vec_a_vec_a_vec$'|)) % 140.07/140.36 (define-fun |tptp.'mult_row$b'| ((BOUND_VARIABLE_57873 |tptp.'B_c_vec_a_vec_a_vec$'|) (BOUND_VARIABLE_57875 |tptp.'A$'|) (BOUND_VARIABLE_57877 |tptp.'B_c_vec$'|)) |tptp.'B_c_vec_a_vec_a_vec$'| (as |@_tptp.'B_c_vec_a_vec_a_vec$'__0| |tptp.'B_c_vec_a_vec_a_vec$'|)) % 140.07/140.36 (define-fun |tptp.'uwl$'| (($x1 |tptp.'B_a_vec_a_vec$'|) ($x2 |tptp.'A$'|)) |tptp.'A_b_fun$'| (as |@_tptp.'A_b_fun$'__0| |tptp.'A_b_fun$'|)) % 140.07/140.36 (define-fun |tptp.'interchange_rows$d'| (($x1 |tptp.'B_c_vec_a_vec$'|) ($x2 |tptp.'A$'|)) |tptp.'A_b_c_vec_a_vec_fun$'| (as |@_tptp.'A_b_c_vec_a_vec_fun$'__0| |tptp.'A_b_c_vec_a_vec_fun$'|)) % 140.07/140.36 (define-fun |tptp.'vax$'| (($x1 |tptp.'B$'|) ($x2 |tptp.'B_a_vec$'|)) |tptp.'A_b_fun$'| (as |@_tptp.'A_b_fun$'__0| |tptp.'A_b_fun$'|)) % 140.07/140.36 (define-fun |tptp.'uwk$'| (($x1 |tptp.'B_a_vec_c_vec$'|) ($x2 |tptp.'A$'|)) |tptp.'C_b_fun$'| (as |@_tptp.'C_b_fun$'__0| |tptp.'C_b_fun$'|)) % 140.07/140.36 (define-fun |tptp.'transpose_row$e'| (($x1 |tptp.'B_d_vec_c_vec$'|)) |tptp.'D_b_c_vec_fun$'| (as |@_tptp.'D_b_c_vec_fun$'__0| |tptp.'D_b_c_vec_fun$'|)) % 140.07/140.36 (define-fun |tptp.'columnvector_row$k'| (($x1 |tptp.'B_a_vec$'|)) |tptp.'A_b_d_vec_fun$'| (as |@_tptp.'A_b_d_vec_fun$'__0| |tptp.'A_b_d_vec_fun$'|)) % 140.07/140.36 (define-fun |tptp.'fun_app$d'| (($x1 |tptp.'D_b_fun_bool_fun$'|) ($x2 |tptp.'D_b_fun$'|)) Bool true) % 140.07/140.36 (define-fun |tptp.'fun_app$au'| (($x1 |tptp.'B_c_vec_a_vec_a_vec_bool_fun$'|) ($x2 |tptp.'B_c_vec_a_vec_a_vec$'|)) Bool false) % 140.07/140.36 (define-fun |tptp.'map_matrix$g'| ((BOUND_VARIABLE_59476 |tptp.'B_a_vec_b_fun$'|) (BOUND_VARIABLE_59478 |tptp.'B_a_vec_c_vec_a_vec$'|)) |tptp.'B_c_vec_a_vec$'| (as |@_tptp.'B_c_vec_a_vec$'__0| |tptp.'B_c_vec_a_vec$'|)) % 140.07/140.36 (define-fun |tptp.'map_matrix$e'| ((BOUND_VARIABLE_59493 |tptp.'B_b_d_vec_fun$'|) (BOUND_VARIABLE_59495 |tptp.'B_a_vec_c_vec$'|)) |tptp.'B_d_vec_a_vec_c_vec$'| (as |@_tptp.'B_d_vec_a_vec_c_vec$'__0| |tptp.'B_d_vec_a_vec_c_vec$'|)) % 140.07/140.36 (define-fun |tptp.'elt_set_times$a'| (($x1 |tptp.'D_b_fun$'|) ($x2 |tptp.'D_b_fun_set$'|)) |tptp.'D_b_fun_set$'| (as |@_tptp.'D_b_fun_set$'__0| |tptp.'D_b_fun_set$'|)) % 140.07/140.36 (define-fun |tptp.'vec_lambda$e'| (($x1 |tptp.'A_b_c_vec_fun$'|)) |tptp.'B_c_vec_a_vec$'| (as |@_tptp.'B_c_vec_a_vec$'__0| |tptp.'B_c_vec_a_vec$'|)) % 140.07/140.36 (define-fun |tptp.'row$a'| ((BOUND_VARIABLE_58750 |tptp.'A$'|) (BOUND_VARIABLE_58752 |tptp.'B_c_vec_a_vec_a_vec$'|)) |tptp.'B_c_vec_a_vec$'| (as |@_tptp.'B_c_vec_a_vec$'__0| |tptp.'B_c_vec_a_vec$'|)) % 140.07/140.36 (define-fun |tptp.'uuy$'| (($x1 |tptp.'B_b_fun$'|) ($x2 |tptp.'B_d_vec_a_vec$'|) ($x3 |tptp.'A$'|)) |tptp.'D_b_fun$'| (as |@_tptp.'D_b_fun$'__0| |tptp.'D_b_fun$'|)) % 140.07/140.36 (define-fun |tptp.'uwh$'| (($x1 |tptp.'B_a_vec_d_vec$'|) ($x2 |tptp.'A$'|)) |tptp.'D_b_fun$'| (as |@_tptp.'D_b_fun$'__0| |tptp.'D_b_fun$'|)) % 140.07/140.36 (define-fun |tptp.'mult_row_row$'| ((BOUND_VARIABLE_59245 |tptp.'B_d_vec_d_vec$'|) (BOUND_VARIABLE_59247 |tptp.'D$'|) (BOUND_VARIABLE_59249 |tptp.'B$'|)) |tptp.'D_b_d_vec_fun$'| (as |@_tptp.'D_b_d_vec_fun$'__0| |tptp.'D_b_d_vec_fun$'|)) % 140.07/140.36 (define-fun |tptp.'gauss_Jordan_wrapper$c'| ((BOUND_VARIABLE_59533 |tptp.'A$'|) (BOUND_VARIABLE_59535 |tptp.'D$'|) (BOUND_VARIABLE_59537 |tptp.'B_c_vec_a_vec$'|) (BOUND_VARIABLE_59539 |tptp.'B_d_vec_a_vec$'|)) |tptp.'B_c_vec_a_vec$'| (as |@_tptp.'B_c_vec_a_vec$'__0| |tptp.'B_c_vec_a_vec$'|)) % 140.07/140.36 (define-fun |tptp.'collect$a'| (($x1 |tptp.'D_b_fun_bool_fun$'|)) |tptp.'D_b_fun_set$'| (as |@_tptp.'D_b_fun_set$'__0| |tptp.'D_b_fun_set$'|)) % 140.07/140.36 (define-fun |tptp.'times$e'| ((BOUND_VARIABLE_58871 |tptp.'B_c_vec_a_vec_a_vec$'|) (BOUND_VARIABLE_58873 |tptp.'B_c_vec_a_vec_a_vec$'|)) |tptp.'B_c_vec_a_vec_a_vec$'| (as |@_tptp.'B_c_vec_a_vec_a_vec$'__0| |tptp.'B_c_vec_a_vec_a_vec$'|)) % 140.07/140.36 (define-fun |tptp.'gauss_Jordan_wrapper$b'| ((BOUND_VARIABLE_59564 |tptp.'A$'|) (BOUND_VARIABLE_59566 |tptp.'C$'|) (BOUND_VARIABLE_59568 |tptp.'B_c_vec_a_vec$'|) (BOUND_VARIABLE_59570 |tptp.'B_c_vec_a_vec$'|)) |tptp.'B_c_vec_a_vec$'| (as |@_tptp.'B_c_vec_a_vec$'__0| |tptp.'B_c_vec_a_vec$'|)) % 140.07/140.36 (define-fun |tptp.'vec_nth$i'| (($x1 |tptp.'B_a_vec$'|)) |tptp.'A_b_fun$'| (as |@_tptp.'A_b_fun$'__0| |tptp.'A_b_fun$'|)) % 140.07/140.36 (define-fun |tptp.'rowvector$e'| ((BOUND_VARIABLE_59579 |tptp.'B_a_vec$'|)) |tptp.'B_a_vec_d_vec$'| (as |@_tptp.'B_a_vec_d_vec$'__0| |tptp.'B_a_vec_d_vec$'|)) % 140.07/140.36 (define-fun |tptp.'fun_app$l'| (($x1 |tptp.'C_b_c_vec_fun$'|) ($x2 |tptp.'C$'|)) |tptp.'B_c_vec$'| (as |@_tptp.'B_c_vec$'__0| |tptp.'B_c_vec$'|)) % 140.07/140.36 (define-fun |tptp.'vab$'| (($x1 |tptp.'B_d_vec_d_vec$'|) ($x2 |tptp.'B_d_vec_d_vec$'|)) |tptp.'D_b_d_vec_fun$'| (as |@_tptp.'D_b_d_vec_fun$'__0| |tptp.'D_b_d_vec_fun$'|)) % 140.07/140.36 (define-fun |tptp.'uvl$'| (($x1 |tptp.'B_c_vec_b_fun$'|) ($x2 |tptp.'B_c_vec_a_vec_c_vec$'|)) |tptp.'C_b_a_vec_fun$'| (as |@_tptp.'C_b_a_vec_fun$'__0| |tptp.'C_b_a_vec_fun$'|)) % 140.07/140.36 (define-fun |tptp.'interchange_rows_row$a'| ((BOUND_VARIABLE_59324 |tptp.'B_c_vec_a_vec_a_vec$'|) (BOUND_VARIABLE_59326 |tptp.'A$'|) (BOUND_VARIABLE_59328 |tptp.'A$'|)) |tptp.'A_b_c_vec_a_vec_fun$'| (as |@_tptp.'A_b_c_vec_a_vec_fun$'__0| |tptp.'A_b_c_vec_a_vec_fun$'|)) % 140.07/140.36 (define-fun |tptp.'uzd$'| (($x1 |tptp.'B_c_vec_a_vec_a_vec$'|) ($x2 |tptp.'A$'|) ($x3 |tptp.'A$'|) ($x4 |tptp.'B_c_vec$'|) ($x5 |tptp.'A$'|)) |tptp.'A_b_c_vec_fun$'| (as |@_tptp.'A_b_c_vec_fun$'__1| |tptp.'A_b_c_vec_fun$'|)) % 140.07/140.36 (define-fun |tptp.'uyq$'| (($x1 |tptp.'B_d_vec_d_vec$'|) ($x2 |tptp.'D$'|) ($x3 |tptp.'B$'|)) |tptp.'D_b_d_vec_fun$'| (as |@_tptp.'D_b_d_vec_fun$'__0| |tptp.'D_b_d_vec_fun$'|)) % 140.07/140.36 (define-fun |tptp.'uwg$'| (($x1 |tptp.'B_d_vec_d_vec$'|) ($x2 |tptp.'D$'|)) |tptp.'D_b_fun$'| (as |@_tptp.'D_b_fun$'__0| |tptp.'D_b_fun$'|)) % 140.07/140.36 (define-fun |tptp.'row_add$a'| ((BOUND_VARIABLE_58832 |tptp.'B_d_vec_d_vec$'|) (BOUND_VARIABLE_58834 |tptp.'D$'|) (BOUND_VARIABLE_58836 |tptp.'D$'|) (BOUND_VARIABLE_58838 |tptp.'B$'|)) |tptp.'B_d_vec_d_vec$'| (as |@_tptp.'B_d_vec_d_vec$'__0| |tptp.'B_d_vec_d_vec$'|)) % 140.07/140.36 (define-fun |tptp.'uxp$'| (($x1 |tptp.'B_c_vec_a_vec$'|)) |tptp.'A_b_c_vec_a_vec_fun$'| (as |@_tptp.'A_b_c_vec_a_vec_fun$'__0| |tptp.'A_b_c_vec_a_vec_fun$'|)) % 140.07/140.36 (define-fun |tptp.'uwz$'| (($x1 |tptp.'B_a_vec_a_vec$'|)) |tptp.'A_b_a_vec_fun$'| (as |@_tptp.'A_b_a_vec_fun$'__0| |tptp.'A_b_a_vec_fun$'|)) % 140.07/140.36 (define-fun |tptp.'uxe$'| (($x1 |tptp.'A$'|) ($x2 |tptp.'B_c_vec_a_vec_a_vec$'|)) |tptp.'A_b_c_vec_fun$'| (as |@_tptp.'A_b_c_vec_fun$'__1| |tptp.'A_b_c_vec_fun$'|)) % 140.07/140.36 (define-fun |tptp.'uye$'| (($x1 |tptp.'B_d_vec_a_vec$'|) ($x2 |tptp.'A$'|)) |tptp.'A_b_d_vec_fun$'| (as |@_tptp.'A_b_d_vec_fun$'__0| |tptp.'A_b_d_vec_fun$'|)) % 140.07/140.36 (define-fun |tptp.'uvp$'| (($x1 |tptp.'B_a_vec$'|)) |tptp.'C_b_a_vec_fun$'| (as |@_tptp.'C_b_a_vec_fun$'__0| |tptp.'C_b_a_vec_fun$'|)) % 140.07/140.36 (define-fun |tptp.'rowvector$'| ((BOUND_VARIABLE_57215 |tptp.'B_a_vec$'|)) |tptp.'B_a_vec_a_vec$'| (as |@_tptp.'B_a_vec_a_vec$'__0| |tptp.'B_a_vec_a_vec$'|)) % 140.07/140.36 (define-fun |tptp.'elt_set_plus$b'| (($x1 |tptp.'A_b_c_vec_fun$'|) ($x2 |tptp.'A_b_c_vec_fun_set$'|)) |tptp.'A_b_c_vec_fun_set$'| (as |@_tptp.'A_b_c_vec_fun_set$'__0| |tptp.'A_b_c_vec_fun_set$'|)) % 140.07/140.36 (define-fun |tptp.'transpose$'| ((BOUND_VARIABLE_59609 |tptp.'B_c_vec_a_vec$'|)) |tptp.'B_a_vec_c_vec$'| (as |@_tptp.'B_a_vec_c_vec$'__0| |tptp.'B_a_vec_c_vec$'|)) % 140.07/140.36 (define-fun |tptp.'transpose$h'| ((BOUND_VARIABLE_59618 |tptp.'B_a_vec_d_vec$'|)) |tptp.'B_d_vec_a_vec$'| (as |@_tptp.'B_d_vec_a_vec$'__0| |tptp.'B_d_vec_a_vec$'|)) % 140.07/140.36 (define-fun |tptp.'columns$'| ((BOUND_VARIABLE_59629 |tptp.'B_a_vec_c_vec$'|)) |tptp.'B_c_vec_set$'| (as |@_tptp.'B_c_vec_set$'__0| |tptp.'B_c_vec_set$'|)) % 140.07/140.36 (define-fun |tptp.'interchange_rows$a'| ((BOUND_VARIABLE_59646 |tptp.'B_a_vec_c_vec$'|) (BOUND_VARIABLE_59648 |tptp.'C$'|) (BOUND_VARIABLE_59650 |tptp.'C$'|)) |tptp.'B_a_vec_c_vec$'| (as |@_tptp.'B_a_vec_c_vec$'__0| |tptp.'B_a_vec_c_vec$'|)) % 140.07/140.36 (define-fun |tptp.'map_matrix$m'| (($x1 |tptp.'B_d_vec_b_fun$'|) ($x2 |tptp.'B_d_vec_d_vec_d_vec$'|)) |tptp.'B_d_vec_d_vec$'| (as |@_tptp.'B_d_vec_d_vec$'__0| |tptp.'B_d_vec_d_vec$'|)) % 140.07/140.36 (define-fun |tptp.'fun_app$k'| (($x1 |tptp.'D_b_a_vec_fun$'|) ($x2 |tptp.'D$'|)) |tptp.'B_a_vec$'| (as |@_tptp.'B_a_vec$'__0| |tptp.'B_a_vec$'|)) % 140.07/140.36 (define-fun |tptp.'uva$'| (($x1 |tptp.'B_b_c_vec_fun$'|) ($x2 |tptp.'B_a_vec_c_vec$'|) ($x3 |tptp.'C$'|)) |tptp.'A_b_c_vec_fun$'| (as |@_tptp.'A_b_c_vec_fun$'__1| |tptp.'A_b_c_vec_fun$'|)) % 140.07/140.36 (define-fun |tptp.'uminus$b'| ((BOUND_VARIABLE_59657 |tptp.'B_d_vec$'|)) |tptp.'B_d_vec$'| (as |@_tptp.'B_d_vec$'__0| |tptp.'B_d_vec$'|)) % 140.07/140.36 (define-fun |tptp.'uu$'| () |tptp.'A_b_c_vec_fun$'| (as |@_tptp.'A_b_c_vec_fun$'__0| |tptp.'A_b_c_vec_fun$'|)) % 140.07/140.36 (define-fun |tptp.'mult_row$a'| ((BOUND_VARIABLE_59672 |tptp.'B_a_vec_c_vec$'|) (BOUND_VARIABLE_59674 |tptp.'C$'|) (BOUND_VARIABLE_59676 |tptp.'B$'|)) |tptp.'B_a_vec_c_vec$'| (as |@_tptp.'B_a_vec_c_vec$'__0| |tptp.'B_a_vec_c_vec$'|)) % 140.07/140.36 (define-fun |tptp.'uui$'| (($x1 |tptp.'C$'|) ($x2 |tptp.'D$'|) ($x3 |tptp.'B_a_vec_c_vec$'|) ($x4 |tptp.'B_d_vec_c_vec$'|)) |tptp.'C_b_a_vec_fun$'| (as |@_tptp.'C_b_a_vec_fun$'__0| |tptp.'C_b_a_vec_fun$'|)) % 140.07/140.36 (define-fun |tptp.'vau$'| (($x1 |tptp.'B_a_vec$'|) ($x2 |tptp.'B_a_vec_c_vec$'|)) |tptp.'C_b_a_vec_fun$'| (as |@_tptp.'C_b_a_vec_fun$'__0| |tptp.'C_b_a_vec_fun$'|)) % 140.07/140.36 (define-fun |tptp.'uxt$'| (($x1 |tptp.'B_c_vec$'|)) |tptp.'C_b_c_vec_fun$'| (as |@_tptp.'C_b_c_vec_fun$'__0| |tptp.'C_b_c_vec_fun$'|)) % 140.07/140.36 (define-fun |tptp.'mult_row$'| ((BOUND_VARIABLE_58092 |tptp.'B_d_vec_d_vec$'|) (BOUND_VARIABLE_58094 |tptp.'D$'|) (BOUND_VARIABLE_58096 |tptp.'B$'|)) |tptp.'B_d_vec_d_vec$'| (as |@_tptp.'B_d_vec_d_vec$'__0| |tptp.'B_d_vec_d_vec$'|)) % 140.07/140.36 (define-fun |tptp.'uyr$'| (($x1 |tptp.'B_a_vec_c_vec$'|) ($x2 |tptp.'A$'|) ($x3 |tptp.'B$'|) ($x4 |tptp.'C$'|)) |tptp.'A_b_fun$'| (as |@_tptp.'A_b_fun$'__0| |tptp.'A_b_fun$'|)) % 140.07/140.36 (define-fun |tptp.'uzq$'| (($x1 |tptp.'B_d_vec_a_vec$'|) ($x2 |tptp.'A$'|) ($x3 |tptp.'B$'|)) |tptp.'A_b_d_vec_fun$'| (as |@_tptp.'A_b_d_vec_fun$'__0| |tptp.'A_b_d_vec_fun$'|)) % 140.07/140.36 (define-fun |tptp.'uminus$a'| ((BOUND_VARIABLE_59691 |tptp.'B_c_vec_a_vec$'|)) |tptp.'B_c_vec_a_vec$'| (as |@_tptp.'B_c_vec_a_vec$'__0| |tptp.'B_c_vec_a_vec$'|)) % 140.07/140.36 (define-fun |tptp.'uyy$'| (($x1 |tptp.'B_c_vec_a_vec$'|) ($x2 |tptp.'C$'|) ($x3 |tptp.'B$'|)) |tptp.'A_b_c_vec_fun$'| (as |@_tptp.'A_b_c_vec_fun$'__1| |tptp.'A_b_c_vec_fun$'|)) % 140.07/140.36 (define-fun |tptp.'less_eq$b'| (($x1 |tptp.'A_b_c_vec_fun_set$'|) ($x2 |tptp.'A_b_c_vec_fun_set$'|)) Bool true) % 140.07/140.36 (define-fun |tptp.'uvq$'| (($x1 |tptp.'B_c_vec_a_vec$'|)) |tptp.'A_b_c_vec_a_vec_fun$'| (as |@_tptp.'A_b_c_vec_a_vec_fun$'__0| |tptp.'A_b_c_vec_a_vec_fun$'|)) % 140.07/140.36 (define-fun |tptp.'vector_scalar_mult$a'| ((BOUND_VARIABLE_59703 |tptp.'B_a_vec$'|) (BOUND_VARIABLE_59705 |tptp.'B_a_vec_c_vec$'|)) |tptp.'B_a_vec_c_vec$'| (as |@_tptp.'B_a_vec_c_vec$'__0| |tptp.'B_a_vec_c_vec$'|)) % 140.07/140.36 (define-fun |tptp.'vec_nth$m'| (($x1 |tptp.'B_a_vec_a_vec$'|) ($x2 |tptp.'A$'|)) |tptp.'B_a_vec$'| (as |@_tptp.'B_a_vec$'__0| |tptp.'B_a_vec$'|)) % 140.07/140.36 (define-fun |tptp.'map_matrix$a'| ((BOUND_VARIABLE_59717 |tptp.'B_b_fun$'|) (BOUND_VARIABLE_59719 |tptp.'B_a_vec_c_vec$'|)) |tptp.'B_a_vec_c_vec$'| (as |@_tptp.'B_a_vec_c_vec$'__0| |tptp.'B_a_vec_c_vec$'|)) % 140.07/140.36 (define-fun |tptp.'uxf$'| (($x1 |tptp.'D$'|) ($x2 |tptp.'B_d_vec_d_vec$'|)) |tptp.'D_b_fun$'| (as |@_tptp.'D_b_fun$'__0| |tptp.'D_b_fun$'|)) % 140.07/140.36 (define-fun |tptp.'map_matrix$h'| ((BOUND_VARIABLE_59733 |tptp.'B_c_vec_b_fun$'|) (BOUND_VARIABLE_59735 |tptp.'B_c_vec_a_vec_c_vec$'|)) |tptp.'B_a_vec_c_vec$'| (as |@_tptp.'B_a_vec_c_vec$'__0| |tptp.'B_a_vec_c_vec$'|)) % 140.07/140.36 (define-fun |tptp.'vay$'| (($x1 |tptp.'B$'|) ($x2 |tptp.'B_d_vec$'|)) |tptp.'D_b_fun$'| (as |@_tptp.'D_b_fun$'__0| |tptp.'D_b_fun$'|)) % 140.07/140.36 (define-fun |tptp.'vai$'| (($x1 |tptp.'B_c_vec_a_vec$'|) ($x2 |tptp.'B_c_vec_a_vec$'|)) |tptp.'A_b_c_vec_fun$'| (as |@_tptp.'A_b_c_vec_fun$'__0| |tptp.'A_b_c_vec_fun$'|)) % 140.07/140.36 (define-fun |tptp.'plus$a'| ((BOUND_VARIABLE_58486 |tptp.'B_d_vec$'|) (BOUND_VARIABLE_58488 |tptp.'B_d_vec$'|)) |tptp.'B_d_vec$'| (as |@_tptp.'B_d_vec$'__0| |tptp.'B_d_vec$'|)) % 140.07/140.36 (define-fun |tptp.'row_add_row$'| ((BOUND_VARIABLE_58730 |tptp.'B_c_vec_a_vec_a_vec$'|) (BOUND_VARIABLE_58732 |tptp.'A$'|) (BOUND_VARIABLE_58734 |tptp.'A$'|) (BOUND_VARIABLE_58736 |tptp.'B_c_vec$'|)) |tptp.'A_b_c_vec_a_vec_fun$'| (as |@_tptp.'A_b_c_vec_a_vec_fun$'__0| |tptp.'A_b_c_vec_a_vec_fun$'|)) % 140.07/140.36 (define-fun |tptp.'mult_column_row$a'| ((BOUND_VARIABLE_58299 |tptp.'B_c_vec_a_vec_a_vec$'|) (BOUND_VARIABLE_58301 |tptp.'A$'|) (BOUND_VARIABLE_58303 |tptp.'B_c_vec$'|)) |tptp.'A_b_c_vec_a_vec_fun$'| (as |@_tptp.'A_b_c_vec_a_vec_fun$'__0| |tptp.'A_b_c_vec_a_vec_fun$'|)) % 140.07/140.36 (define-fun |tptp.'columnvector$h'| ((BOUND_VARIABLE_59772 |tptp.'B_a_vec_c_vec$'|)) |tptp.'B_a_vec_c_vec_c_vec$'| (as |@_tptp.'B_a_vec_c_vec_c_vec$'__0| |tptp.'B_a_vec_c_vec_c_vec$'|)) % 140.07/140.36 (define-fun |tptp.'transpose$b'| ((BOUND_VARIABLE_59781 |tptp.'B_a_vec_c_vec$'|)) |tptp.'B_c_vec_a_vec$'| (as |@_tptp.'B_c_vec_a_vec$'__0| |tptp.'B_c_vec_a_vec$'|)) % 140.07/140.36 (define-fun |tptp.'uzi$'| (($x1 |tptp.'B_c_vec_a_vec$'|) ($x2 |tptp.'A$'|) ($x3 |tptp.'A$'|) ($x4 |tptp.'B$'|)) |tptp.'A_b_c_vec_fun$'| (as |@_tptp.'A_b_c_vec_fun$'__1| |tptp.'A_b_c_vec_fun$'|)) % 140.07/140.36 (define-fun |tptp.'vec_nth$h'| (($x1 |tptp.'B_c_vec$'|)) |tptp.'C_b_fun$'| (as |@_tptp.'C_b_fun$'__0| |tptp.'C_b_fun$'|)) % 140.07/140.36 (define-fun |tptp.'vec$a'| ((BOUND_VARIABLE_58358 |tptp.'B_d_vec$'|)) |tptp.'B_d_vec_a_vec$'| (as |@_tptp.'B_d_vec_a_vec$'__0| |tptp.'B_d_vec_a_vec$'|)) % 140.07/140.36 (define-fun |tptp.'column$d'| ((BOUND_VARIABLE_59797 |tptp.'D$'|) (BOUND_VARIABLE_59799 |tptp.'B_d_vec_c_vec$'|)) |tptp.'B_c_vec$'| (as |@_tptp.'B_c_vec$'__0| |tptp.'B_c_vec$'|)) % 140.07/140.36 (define-fun |tptp.'uvf$'| (($x1 |tptp.'B_b_d_vec_fun$'|) ($x2 |tptp.'B_a_vec_c_vec$'|)) |tptp.'C_b_d_vec_a_vec_fun$'| (as |@_tptp.'C_b_d_vec_a_vec_fun$'__0| |tptp.'C_b_d_vec_a_vec_fun$'|)) % 140.07/140.36 (define-fun |tptp.'uvv$'| (($x1 |tptp.'B_a_vec_c_vec$'|) ($x2 |tptp.'A$'|) ($x3 |tptp.'A$'|) ($x4 |tptp.'C$'|)) |tptp.'A_b_fun$'| (as |@_tptp.'A_b_fun$'__0| |tptp.'A_b_fun$'|)) % 140.07/140.36 (define-fun |tptp.'uxl$'| (($x1 |tptp.'A$'|) ($x2 |tptp.'B_d_vec_a_vec_a_vec$'|)) |tptp.'A_b_d_vec_fun$'| (as |@_tptp.'A_b_d_vec_fun$'__0| |tptp.'A_b_d_vec_fun$'|)) % 140.07/140.36 (define-fun |tptp.'uwr$'| (($x1 |tptp.'B_c_vec_a_vec$'|) ($x2 |tptp.'C$'|) ($x3 |tptp.'C$'|)) |tptp.'A_b_c_vec_fun$'| (as |@_tptp.'A_b_c_vec_fun$'__1| |tptp.'A_b_c_vec_fun$'|)) % 140.07/140.36 (define-fun |tptp.'fun_app$b'| (($x1 |tptp.'D_b_fun$'|) ($x2 |tptp.'D$'|)) |tptp.'B$'| (as |@_tptp.'B$'__0| |tptp.'B$'|)) % 140.07/140.36 (define-fun |tptp.'uxr$'| (($x1 |tptp.'B_d_vec$'|)) |tptp.'D_b_c_vec_fun$'| (as |@_tptp.'D_b_c_vec_fun$'__0| |tptp.'D_b_c_vec_fun$'|)) % 140.07/140.36 (define-fun |tptp.'uvm$'| (($x1 |tptp.'B_d_vec_b_fun$'|) ($x2 |tptp.'B_d_vec_a_vec_c_vec$'|) ($x3 |tptp.'C$'|)) |tptp.'A_b_fun$'| (as |@_tptp.'A_b_fun$'__0| |tptp.'A_b_fun$'|)) % 140.07/140.36 (define-fun |tptp.'van$'| (($x1 |tptp.'B_d_vec_a_vec$'|) ($x2 |tptp.'D$'|) ($x3 |tptp.'D$'|) ($x4 |tptp.'B$'|) ($x5 |tptp.'A$'|)) |tptp.'D_b_fun$'| (as |@_tptp.'D_b_fun$'__0| |tptp.'D_b_fun$'|)) % 140.07/140.36 (define-fun |tptp.'uxb$'| (($x1 |tptp.'B_a_vec_c_vec_c_vec$'|)) |tptp.'C_b_a_vec_c_vec_fun$'| (as |@_tptp.'C_b_a_vec_c_vec_fun$'__0| |tptp.'C_b_a_vec_c_vec_fun$'|)) % 140.07/140.36 ) % 140.07/140.36 % SZS output end Model % 140.07/140.36 % cvc5 exiting %------------------------------------------------------------------------------