%------------------------------------------------------------------------------ % File : cvc5-SAT---1.3.4 % Problem : ITP325_10 : TPTP v9.2.1. Released v8.2.0. % Transfm : none % Format : tptp:raw % Command : /export/starexec/sandbox/solver/bin/do_cvc5 /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % Computer : n011.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8042.1875MB % OS : Linux 3.10.0-693.el7.x86_64 % CPULimit : 300s % WCLimit : 300s % DateTime : Wed Jun 3 08:27:55 AM UTC 2026 % Result : Satisfiable 140.60s 140.97s % Output : Model 140.60s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : ITP325_10 : TPTP v9.2.1. Released v8.2.0. % 0.12/0.13 % Command : /export/starexec/sandbox/solver/bin/do_cvc5 /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % 0.15/0.34 % Computer : n011.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:00:04 EDT 2026 % 0.15/0.34 % CPUTime : % 0.39/0.66 %----Disproving TF0_NAR % 0.39/0.67 --- Run --finite-model-find --sort-inference --uf-ss-fair at 60... % 0.50/0.73 --- Run --mbqi at 45... % 0.57/45.91 --- Run --mbqi --mbqi-enum --mbqi-enum-choice-grammar --mbqi-enum-global-syms-grammar --no-cegqi --no-sygus-inst at 45... % 90.77/91.10 --- Run --full-saturate-quant at 45... % 135.90/136.27 --- Run --finite-model-find --fmf-bound --macros-quant at 60... % 140.60/140.97 % SZS status Satisfiable % 140.60/140.97 % SZS output start Model % 140.60/140.98 ( % 140.60/140.98 ; cardinality of $$unsorted is 1 % 140.60/140.98 ; rep: (as @$$unsorted_0 $$unsorted) % 140.60/140.98 ; cardinality of |tptp.'B_a_b_vec_fun$'| is 2 % 140.60/140.98 ; rep: (as |@_tptp.'B_a_b_vec_fun$'__0| |tptp.'B_a_b_vec_fun$'|) % 140.60/140.98 ; rep: (as |@_tptp.'B_a_b_vec_fun$'__1| |tptp.'B_a_b_vec_fun$'|) % 140.60/140.98 ; cardinality of |tptp.'A_b_vec_n_vec_a_fun$'| is 1 % 140.60/140.98 ; rep: (as |@_tptp.'A_b_vec_n_vec_a_fun$'__0| |tptp.'A_b_vec_n_vec_a_fun$'|) % 140.60/140.98 ; cardinality of |tptp.'N_a_b_vec_n_vec_bool_fun_fun$'| is 1 % 140.60/140.98 ; rep: (as |@_tptp.'N_a_b_vec_n_vec_bool_fun_fun$'__0| |tptp.'N_a_b_vec_n_vec_bool_fun_fun$'|) % 140.60/140.98 ; cardinality of |tptp.'A_b_vec_n_vec$'| is 2 % 140.60/140.98 ; rep: (as |@_tptp.'A_b_vec_n_vec$'__0| |tptp.'A_b_vec_n_vec$'|) % 140.60/140.98 ; rep: (as |@_tptp.'A_b_vec_n_vec$'__1| |tptp.'A_b_vec_n_vec$'|) % 140.60/140.98 ; cardinality of |tptp.'N_a_b_vec_n_vec_n_vec_fun$'| is 2 % 140.60/140.98 ; rep: (as |@_tptp.'N_a_b_vec_n_vec_n_vec_fun$'__0| |tptp.'N_a_b_vec_n_vec_n_vec_fun$'|) % 140.60/140.98 ; rep: (as |@_tptp.'N_a_b_vec_n_vec_n_vec_fun$'__1| |tptp.'N_a_b_vec_n_vec_n_vec_fun$'|) % 140.60/140.98 ; cardinality of |tptp.'A_b_vec_a_b_vec_fun$'| is 2 % 140.60/140.98 ; rep: (as |@_tptp.'A_b_vec_a_b_vec_fun$'__0| |tptp.'A_b_vec_a_b_vec_fun$'|) % 140.60/140.98 ; rep: (as |@_tptp.'A_b_vec_a_b_vec_fun$'__1| |tptp.'A_b_vec_a_b_vec_fun$'|) % 140.60/140.98 ; cardinality of |tptp.'A_a_n_vec_fun$'| is 1 % 140.60/140.98 ; rep: (as |@_tptp.'A_a_n_vec_fun$'__0| |tptp.'A_a_n_vec_fun$'|) % 140.60/140.98 ; cardinality of |tptp.'N_a_b_vec_bool_fun_fun$'| is 1 % 140.60/140.98 ; rep: (as |@_tptp.'N_a_b_vec_bool_fun_fun$'__0| |tptp.'N_a_b_vec_bool_fun_fun$'|) % 140.60/140.98 ; cardinality of |tptp.'A_n_vec_a_fun$'| is 1 % 140.60/140.98 ; rep: (as |@_tptp.'A_n_vec_a_fun$'__0| |tptp.'A_n_vec_a_fun$'|) % 140.60/140.98 ; cardinality of |tptp.'A_n_vec_b_vec$'| is 1 % 140.60/140.98 ; rep: (as |@_tptp.'A_n_vec_b_vec$'__0| |tptp.'A_n_vec_b_vec$'|) % 140.60/140.98 ; cardinality of |tptp.'A_b_vec_n_vec_n_vec$'| is 2 % 140.60/140.98 ; rep: (as |@_tptp.'A_b_vec_n_vec_n_vec$'__0| |tptp.'A_b_vec_n_vec_n_vec$'|) % 140.60/140.98 ; rep: (as |@_tptp.'A_b_vec_n_vec_n_vec$'__1| |tptp.'A_b_vec_n_vec_n_vec$'|) % 140.60/140.98 ; cardinality of |tptp.'N_a_n_vec_fun$'| is 2 % 140.60/140.98 ; rep: (as |@_tptp.'N_a_n_vec_fun$'__0| |tptp.'N_a_n_vec_fun$'|) % 140.60/140.98 ; rep: (as |@_tptp.'N_a_n_vec_fun$'__1| |tptp.'N_a_n_vec_fun$'|) % 140.60/140.98 ; cardinality of |tptp.'A_n_vec_a_b_vec_fun$'| is 1 % 140.60/140.98 ; rep: (as |@_tptp.'A_n_vec_a_b_vec_fun$'__0| |tptp.'A_n_vec_a_b_vec_fun$'|) % 140.60/140.98 ; cardinality of |tptp.'A_a_b_vec_fun$'| is 1 % 140.60/140.98 ; rep: (as |@_tptp.'A_a_b_vec_fun$'__0| |tptp.'A_a_b_vec_fun$'|) % 140.60/140.98 ; cardinality of |tptp.'A_b_vec_b_vec$'| is 2 % 140.60/140.98 ; rep: (as |@_tptp.'A_b_vec_b_vec$'__0| |tptp.'A_b_vec_b_vec$'|) % 140.60/140.98 ; rep: (as |@_tptp.'A_b_vec_b_vec$'__1| |tptp.'A_b_vec_b_vec$'|) % 140.60/140.98 ; cardinality of |tptp.'A_n_vec_n_vec$'| is 2 % 140.60/140.98 ; rep: (as |@_tptp.'A_n_vec_n_vec$'__0| |tptp.'A_n_vec_n_vec$'|) % 140.60/140.98 ; rep: (as |@_tptp.'A_n_vec_n_vec$'__1| |tptp.'A_n_vec_n_vec$'|) % 140.60/140.98 ; cardinality of |tptp.'N_a_n_vec_bool_fun_fun$'| is 1 % 140.60/140.98 ; rep: (as |@_tptp.'N_a_n_vec_bool_fun_fun$'__0| |tptp.'N_a_n_vec_bool_fun_fun$'|) % 140.60/140.98 ; cardinality of |tptp.'B$'| is 1 % 140.60/140.98 ; rep: (as |@_tptp.'B$'__0| |tptp.'B$'|) % 140.60/140.98 ; cardinality of |tptp.'A_a_b_vec_n_vec_fun$'| is 2 % 140.60/140.98 ; rep: (as |@_tptp.'A_a_b_vec_n_vec_fun$'__0| |tptp.'A_a_b_vec_n_vec_fun$'|) % 140.60/140.98 ; rep: (as |@_tptp.'A_a_b_vec_n_vec_fun$'__1| |tptp.'A_a_b_vec_n_vec_fun$'|) % 140.60/140.98 ; cardinality of |tptp.'A_b_vec$'| is 2 % 140.60/140.98 ; rep: (as |@_tptp.'A_b_vec$'__0| |tptp.'A_b_vec$'|) % 140.60/140.98 ; rep: (as |@_tptp.'A_b_vec$'__1| |tptp.'A_b_vec$'|) % 140.60/140.98 ; cardinality of |tptp.'N$'| is 1 % 140.60/140.98 ; rep: (as |@_tptp.'N$'__0| |tptp.'N$'|) % 140.60/140.98 ; cardinality of |tptp.'N_a_b_vec_b_vec_fun$'| is 2 % 140.60/140.98 ; rep: (as |@_tptp.'N_a_b_vec_b_vec_fun$'__0| |tptp.'N_a_b_vec_b_vec_fun$'|) % 140.60/140.98 ; rep: (as |@_tptp.'N_a_b_vec_b_vec_fun$'__1| |tptp.'N_a_b_vec_b_vec_fun$'|) % 140.60/140.98 ; cardinality of |tptp.'A_b_vec_n_vec_bool_fun$'| is 1 % 140.60/140.98 ; rep: (as |@_tptp.'A_b_vec_n_vec_bool_fun$'__0| |tptp.'A_b_vec_n_vec_bool_fun$'|) % 140.60/140.98 ; cardinality of |tptp.'B_a_fun$'| is 2 % 140.60/140.98 ; rep: (as |@_tptp.'B_a_fun$'__0| |tptp.'B_a_fun$'|) % 140.60/140.98 ; rep: (as |@_tptp.'B_a_fun$'__1| |tptp.'B_a_fun$'|) % 140.60/140.98 ; cardinality of tptp.tlbool is 2 % 140.60/140.98 ; rep: (as @tptp.tlbool_0 tptp.tlbool) % 140.60/140.98 ; rep: (as @tptp.tlbool_1 tptp.tlbool) % 140.60/140.98 ; cardinality of |tptp.'N_a_bool_fun_fun$'| is 1 % 140.60/140.98 ; rep: (as |@_tptp.'N_a_bool_fun_fun$'__0| |tptp.'N_a_bool_fun_fun$'|) % 140.60/140.98 ; cardinality of |tptp.'A_bool_fun$'| is 1 % 140.60/140.98 ; rep: (as |@_tptp.'A_bool_fun$'__0| |tptp.'A_bool_fun$'|) % 140.60/140.98 ; cardinality of |tptp.'N_a_fun$'| is 2 % 140.60/140.98 ; rep: (as |@_tptp.'N_a_fun$'__0| |tptp.'N_a_fun$'|) % 140.60/140.98 ; rep: (as |@_tptp.'N_a_fun$'__1| |tptp.'N_a_fun$'|) % 140.60/140.98 ; cardinality of |tptp.'N_a_b_vec_fun$'| is 2 % 140.60/140.98 ; rep: (as |@_tptp.'N_a_b_vec_fun$'__0| |tptp.'N_a_b_vec_fun$'|) % 140.60/140.98 ; rep: (as |@_tptp.'N_a_b_vec_fun$'__1| |tptp.'N_a_b_vec_fun$'|) % 140.60/140.98 ; cardinality of |tptp.'A_b_vec_n_vec_a_b_vec_n_vec_fun$'| is 2 % 140.60/140.98 ; rep: (as |@_tptp.'A_b_vec_n_vec_a_b_vec_n_vec_fun$'__0| |tptp.'A_b_vec_n_vec_a_b_vec_n_vec_fun$'|) % 140.60/140.98 ; rep: (as |@_tptp.'A_b_vec_n_vec_a_b_vec_n_vec_fun$'__1| |tptp.'A_b_vec_n_vec_a_b_vec_n_vec_fun$'|) % 140.60/140.98 ; cardinality of |tptp.'A$'| is 2 % 140.60/140.98 ; rep: (as |@_tptp.'A$'__0| |tptp.'A$'|) % 140.60/140.98 ; rep: (as |@_tptp.'A$'__1| |tptp.'A$'|) % 140.60/140.98 ; cardinality of |tptp.'N_n_fun$'| is 1 % 140.60/140.98 ; rep: (as |@_tptp.'N_n_fun$'__0| |tptp.'N_n_fun$'|) % 140.60/140.98 ; cardinality of |tptp.'A_n_vec$'| is 2 % 140.60/140.98 ; rep: (as |@_tptp.'A_n_vec$'__0| |tptp.'A_n_vec$'|) % 140.60/140.98 ; rep: (as |@_tptp.'A_n_vec$'__1| |tptp.'A_n_vec$'|) % 140.60/140.98 ; cardinality of |tptp.'A_b_vec_b_vec_n_vec$'| is 1 % 140.60/140.98 ; rep: (as |@_tptp.'A_b_vec_b_vec_n_vec$'__0| |tptp.'A_b_vec_b_vec_n_vec$'|) % 140.60/140.98 ; cardinality of |tptp.'A_n_vec_a_n_vec_fun$'| is 2 % 140.60/140.98 ; rep: (as |@_tptp.'A_n_vec_a_n_vec_fun$'__0| |tptp.'A_n_vec_a_n_vec_fun$'|) % 140.60/140.98 ; rep: (as |@_tptp.'A_n_vec_a_n_vec_fun$'__1| |tptp.'A_n_vec_a_n_vec_fun$'|) % 140.60/140.98 ; cardinality of |tptp.'B_a_n_vec_fun$'| is 2 % 140.60/140.98 ; rep: (as |@_tptp.'B_a_n_vec_fun$'__0| |tptp.'B_a_n_vec_fun$'|) % 140.60/140.98 ; rep: (as |@_tptp.'B_a_n_vec_fun$'__1| |tptp.'B_a_n_vec_fun$'|) % 140.60/140.98 ; cardinality of |tptp.'A_a_fun$'| is 2 % 140.60/140.98 ; rep: (as |@_tptp.'A_a_fun$'__0| |tptp.'A_a_fun$'|) % 140.60/140.98 ; rep: (as |@_tptp.'A_a_fun$'__1| |tptp.'A_a_fun$'|) % 140.60/140.98 ; cardinality of |tptp.'A_b_vec_n_vec_n_vec_n_vec$'| is 2 % 140.60/140.98 ; rep: (as |@_tptp.'A_b_vec_n_vec_n_vec_n_vec$'__0| |tptp.'A_b_vec_n_vec_n_vec_n_vec$'|) % 140.60/140.98 ; rep: (as |@_tptp.'A_b_vec_n_vec_n_vec_n_vec$'__1| |tptp.'A_b_vec_n_vec_n_vec_n_vec$'|) % 140.60/140.98 ; cardinality of |tptp.'A_n_vec_n_vec_n_vec$'| is 1 % 140.60/140.98 ; rep: (as |@_tptp.'A_n_vec_n_vec_n_vec$'__0| |tptp.'A_n_vec_n_vec_n_vec$'|) % 140.60/140.98 ; cardinality of |tptp.'A_b_vec_a_fun$'| is 1 % 140.60/140.98 ; rep: (as |@_tptp.'A_b_vec_a_fun$'__0| |tptp.'A_b_vec_a_fun$'|) % 140.60/140.98 ; cardinality of |tptp.'A_b_vec_bool_fun$'| is 1 % 140.60/140.98 ; rep: (as |@_tptp.'A_b_vec_bool_fun$'__0| |tptp.'A_b_vec_bool_fun$'|) % 140.60/140.98 ; cardinality of |tptp.'A_b_vec_n_vec_n_vec_a_b_vec_n_vec_n_vec_fun$'| is 2 % 140.60/140.98 ; rep: (as |@_tptp.'A_b_vec_n_vec_n_vec_a_b_vec_n_vec_n_vec_fun$'__0| |tptp.'A_b_vec_n_vec_n_vec_a_b_vec_n_vec_n_vec_fun$'|) % 140.60/140.98 ; rep: (as |@_tptp.'A_b_vec_n_vec_n_vec_a_b_vec_n_vec_n_vec_fun$'__1| |tptp.'A_b_vec_n_vec_n_vec_a_b_vec_n_vec_n_vec_fun$'|) % 140.60/140.98 ; cardinality of |tptp.'A_n_vec_bool_fun$'| is 1 % 140.60/140.98 ; rep: (as |@_tptp.'A_n_vec_bool_fun$'__0| |tptp.'A_n_vec_bool_fun$'|) % 140.60/140.98 ; cardinality of |tptp.'N_n_bool_fun_fun$'| is 2 % 140.60/140.98 ; rep: (as |@_tptp.'N_n_bool_fun_fun$'__0| |tptp.'N_n_bool_fun_fun$'|) % 140.60/140.98 ; rep: (as |@_tptp.'N_n_bool_fun_fun$'__1| |tptp.'N_n_bool_fun_fun$'|) % 140.60/140.98 ; cardinality of |tptp.'B_a_bool_fun_fun$'| is 1 % 140.60/140.98 ; rep: (as |@_tptp.'B_a_bool_fun_fun$'__0| |tptp.'B_a_bool_fun_fun$'|) % 140.60/140.98 ; cardinality of |tptp.'N_bool_fun$'| is 2 % 140.60/140.98 ; rep: (as |@_tptp.'N_bool_fun$'__0| |tptp.'N_bool_fun$'|) % 140.60/140.98 ; rep: (as |@_tptp.'N_bool_fun$'__1| |tptp.'N_bool_fun$'|) % 140.60/140.98 ; cardinality of |tptp.'N_a_b_vec_n_vec_fun$'| is 2 % 140.60/140.98 ; rep: (as |@_tptp.'N_a_b_vec_n_vec_fun$'__0| |tptp.'N_a_b_vec_n_vec_fun$'|) % 140.60/140.98 ; rep: (as |@_tptp.'N_a_b_vec_n_vec_fun$'__1| |tptp.'N_a_b_vec_n_vec_fun$'|) % 140.60/140.98 ; cardinality of |tptp.'N_a_n_vec_n_vec_fun$'| is 2 % 140.60/140.98 ; rep: (as |@_tptp.'N_a_n_vec_n_vec_fun$'__0| |tptp.'N_a_n_vec_n_vec_fun$'|) % 140.60/140.98 ; rep: (as |@_tptp.'N_a_n_vec_n_vec_fun$'__1| |tptp.'N_a_n_vec_n_vec_fun$'|) % 140.60/140.98 (define-fun |tptp.'uul$'| (($x1 |tptp.'A_b_vec_n_vec_n_vec$'|) ($x2 |tptp.'N$'|) ($x3 |tptp.'N$'|) ($x4 |tptp.'N$'|)) |tptp.'N_a_b_vec_fun$'| (ite (and (= (as |@_tptp.'A_b_vec_n_vec_n_vec$'__0| |tptp.'A_b_vec_n_vec_n_vec$'|) $x1) (= (as |@_tptp.'N$'__0| |tptp.'N$'|) $x2) (= (as |@_tptp.'N$'__0| |tptp.'N$'|) $x3) (= (as |@_tptp.'N$'__0| |tptp.'N$'|) $x4)) (as |@_tptp.'N_a_b_vec_fun$'__0| |tptp.'N_a_b_vec_fun$'|) (as |@_tptp.'N_a_b_vec_fun$'__1| |tptp.'N_a_b_vec_fun$'|))) % 140.60/140.98 (define-fun |tptp.'times$b'| (($x1 |tptp.'A_b_vec$'|)) |tptp.'A_b_vec_a_b_vec_fun$'| (ite (= (as |@_tptp.'A_b_vec$'__1| |tptp.'A_b_vec$'|) $x1) (as |@_tptp.'A_b_vec_a_b_vec_fun$'__0| |tptp.'A_b_vec_a_b_vec_fun$'|) (as |@_tptp.'A_b_vec_a_b_vec_fun$'__1| |tptp.'A_b_vec_a_b_vec_fun$'|))) % 140.60/140.98 (define-fun |tptp.'uwy$'| (($x1 |tptp.'A_b_vec_n_vec$'|)) |tptp.'N_a_b_vec_n_vec_fun$'| (ite (= (as |@_tptp.'A_b_vec_n_vec$'__1| |tptp.'A_b_vec_n_vec$'|) $x1) (as |@_tptp.'N_a_b_vec_n_vec_fun$'__0| |tptp.'N_a_b_vec_n_vec_fun$'|) (as |@_tptp.'N_a_b_vec_n_vec_fun$'__1| |tptp.'N_a_b_vec_n_vec_fun$'|))) % 140.60/140.98 (define-fun |tptp.'interchange_columns$a'| ((BOUND_VARIABLE_6992 |tptp.'A_b_vec_n_vec_n_vec$'|) (BOUND_VARIABLE_6993 |tptp.'N$'|) (BOUND_VARIABLE_6994 |tptp.'N$'|)) |tptp.'A_b_vec_n_vec_n_vec$'| (ite (= (as |@_tptp.'N_a_b_vec_n_vec_fun$'__1| |tptp.'N_a_b_vec_n_vec_fun$'|) (ite (and (= BOUND_VARIABLE_6992 (as |@_tptp.'A_b_vec_n_vec_n_vec$'__1| |tptp.'A_b_vec_n_vec_n_vec$'|)) (= BOUND_VARIABLE_6993 (as |@_tptp.'N$'__0| |tptp.'N$'|)) (= BOUND_VARIABLE_6994 (as |@_tptp.'N$'__0| |tptp.'N$'|))) (as |@_tptp.'N_a_b_vec_n_vec_fun$'__0| |tptp.'N_a_b_vec_n_vec_fun$'|) (as |@_tptp.'N_a_b_vec_n_vec_fun$'__1| |tptp.'N_a_b_vec_n_vec_fun$'|))) (as |@_tptp.'A_b_vec_n_vec_n_vec$'__0| |tptp.'A_b_vec_n_vec_n_vec$'|) (as |@_tptp.'A_b_vec_n_vec_n_vec$'__1| |tptp.'A_b_vec_n_vec_n_vec$'|))) % 140.60/140.98 (define-fun |tptp.'uwg$'| (($x1 |tptp.'A_b_vec_n_vec$'|) ($x2 |tptp.'N$'|) ($x3 |tptp.'B$'|)) |tptp.'N_a_b_vec_fun$'| (ite (and (= (as |@_tptp.'A_b_vec_n_vec$'__0| |tptp.'A_b_vec_n_vec$'|) $x1) (= (as |@_tptp.'N$'__0| |tptp.'N$'|) $x2) (= (as |@_tptp.'B$'__0| |tptp.'B$'|) $x3)) (as |@_tptp.'N_a_b_vec_fun$'__0| |tptp.'N_a_b_vec_fun$'|) (as |@_tptp.'N_a_b_vec_fun$'__1| |tptp.'N_a_b_vec_fun$'|))) % 140.60/140.98 (define-fun |tptp.'fun_app$p'| (($x1 |tptp.'A_n_vec_a_n_vec_fun$'|) ($x2 |tptp.'A_n_vec$'|)) |tptp.'A_n_vec$'| (ite (and (= (as |@_tptp.'A_n_vec_a_n_vec_fun$'__0| |tptp.'A_n_vec_a_n_vec_fun$'|) $x1) (= (as |@_tptp.'A_n_vec$'__0| |tptp.'A_n_vec$'|) $x2)) (as |@_tptp.'A_n_vec$'__0| |tptp.'A_n_vec$'|) (as |@_tptp.'A_n_vec$'__1| |tptp.'A_n_vec$'|))) % 140.60/140.98 (define-fun |tptp.'uxm$'| (($x1 |tptp.'A_b_vec_n_vec_n_vec$'|) ($x2 |tptp.'A_b_vec_n_vec_n_vec$'|)) |tptp.'N_a_b_vec_n_vec_fun$'| (ite (and (= (as |@_tptp.'A_b_vec_n_vec_n_vec$'__1| |tptp.'A_b_vec_n_vec_n_vec$'|) $x1) (= (as |@_tptp.'A_b_vec_n_vec_n_vec$'__1| |tptp.'A_b_vec_n_vec_n_vec$'|) $x2)) (as |@_tptp.'N_a_b_vec_n_vec_fun$'__0| |tptp.'N_a_b_vec_n_vec_fun$'|) (as |@_tptp.'N_a_b_vec_n_vec_fun$'__1| |tptp.'N_a_b_vec_n_vec_fun$'|))) % 140.60/140.98 (define-fun |tptp.'uvk$'| (($x1 |tptp.'A_a_b_vec_fun$'|) ($x2 |tptp.'A_b_vec_n_vec$'|)) |tptp.'N_a_b_vec_b_vec_fun$'| (as |@_tptp.'N_a_b_vec_b_vec_fun$'__0| |tptp.'N_a_b_vec_b_vec_fun$'|)) % 140.60/140.98 (define-fun |tptp.'uxg$'| (($x1 |tptp.'A_b_vec_n_vec_n_vec$'|) ($x2 |tptp.'N$'|) ($x3 |tptp.'A_b_vec$'|)) |tptp.'N_a_b_vec_n_vec_fun$'| (ite (and (= (as |@_tptp.'A_b_vec_n_vec_n_vec$'__1| |tptp.'A_b_vec_n_vec_n_vec$'|) $x1) (= (as |@_tptp.'N$'__0| |tptp.'N$'|) $x2) (= (as |@_tptp.'A_b_vec$'__0| |tptp.'A_b_vec$'|) $x3)) (as |@_tptp.'N_a_b_vec_n_vec_fun$'__0| |tptp.'N_a_b_vec_n_vec_fun$'|) (as |@_tptp.'N_a_b_vec_n_vec_fun$'__1| |tptp.'N_a_b_vec_n_vec_fun$'|))) % 140.60/140.98 (define-fun |tptp.'uwl$'| (($x1 |tptp.'A_b_vec_n_vec_n_vec$'|) ($x2 |tptp.'N$'|)) |tptp.'N_a_b_vec_n_vec_fun$'| (ite (and (= (as |@_tptp.'A_b_vec_n_vec_n_vec$'__1| |tptp.'A_b_vec_n_vec_n_vec$'|) $x1) (= (as |@_tptp.'N$'__0| |tptp.'N$'|) $x2)) (as |@_tptp.'N_a_b_vec_n_vec_fun$'__0| |tptp.'N_a_b_vec_n_vec_fun$'|) (as |@_tptp.'N_a_b_vec_n_vec_fun$'__1| |tptp.'N_a_b_vec_n_vec_fun$'|))) % 140.60/140.98 (define-fun |tptp.'uvm$'| (($x1 |tptp.'A_b_vec_a_fun$'|) ($x2 |tptp.'A_b_vec_n_vec_n_vec$'|)) |tptp.'N_a_n_vec_fun$'| (as |@_tptp.'N_a_n_vec_fun$'__1| |tptp.'N_a_n_vec_fun$'|)) % 140.60/140.98 (define-fun |tptp.'uuk$'| (($x1 |tptp.'A_b_vec_b_vec$'|) ($x2 |tptp.'B$'|) ($x3 |tptp.'B$'|)) |tptp.'B_a_b_vec_fun$'| (ite (and (= (as |@_tptp.'A_b_vec_b_vec$'__0| |tptp.'A_b_vec_b_vec$'|) $x1) (= (as |@_tptp.'B$'__0| |tptp.'B$'|) $x2) (= (as |@_tptp.'B$'__0| |tptp.'B$'|) $x3)) (as |@_tptp.'B_a_b_vec_fun$'__0| |tptp.'B_a_b_vec_fun$'|) (as |@_tptp.'B_a_b_vec_fun$'__1| |tptp.'B_a_b_vec_fun$'|))) % 140.60/140.98 (define-fun |tptp.'interchange_columns_row$'| ((BOUND_VARIABLE_6895 |tptp.'A_b_vec_n_vec_n_vec$'|) (BOUND_VARIABLE_6896 |tptp.'N$'|) (BOUND_VARIABLE_6897 |tptp.'N$'|)) |tptp.'N_a_b_vec_n_vec_fun$'| (ite (= (as |@_tptp.'A_b_vec_n_vec_n_vec$'__1| |tptp.'A_b_vec_n_vec_n_vec$'|) (ite (= (as |@_tptp.'N_a_b_vec_n_vec_fun$'__1| |tptp.'N_a_b_vec_n_vec_fun$'|) (ite (and (= BOUND_VARIABLE_6895 (as |@_tptp.'A_b_vec_n_vec_n_vec$'__1| |tptp.'A_b_vec_n_vec_n_vec$'|)) (= BOUND_VARIABLE_6896 (as |@_tptp.'N$'__0| |tptp.'N$'|)) (= BOUND_VARIABLE_6897 (as |@_tptp.'N$'__0| |tptp.'N$'|))) (as |@_tptp.'N_a_b_vec_n_vec_fun$'__0| |tptp.'N_a_b_vec_n_vec_fun$'|) (as |@_tptp.'N_a_b_vec_n_vec_fun$'__1| |tptp.'N_a_b_vec_n_vec_fun$'|))) (as |@_tptp.'A_b_vec_n_vec_n_vec$'__0| |tptp.'A_b_vec_n_vec_n_vec$'|) (as |@_tptp.'A_b_vec_n_vec_n_vec$'__1| |tptp.'A_b_vec_n_vec_n_vec$'|))) (as |@_tptp.'N_a_b_vec_n_vec_fun$'__0| |tptp.'N_a_b_vec_n_vec_fun$'|) (as |@_tptp.'N_a_b_vec_n_vec_fun$'__1| |tptp.'N_a_b_vec_n_vec_fun$'|))) % 140.60/140.98 (define-fun |tptp.'less$'| () |tptp.'N_n_bool_fun_fun$'| (as |@_tptp.'N_n_bool_fun_fun$'__0| |tptp.'N_n_bool_fun_fun$'|)) % 140.60/140.98 (define-fun |tptp.'uminus$e'| ((BOUND_VARIABLE_49470 |tptp.'A_n_vec_n_vec$'|)) |tptp.'A_n_vec_n_vec$'| (as |@_tptp.'A_n_vec_n_vec$'__1| |tptp.'A_n_vec_n_vec$'|)) % 140.60/140.98 (define-fun |tptp.'uub$'| (($x1 |tptp.'A_n_vec_n_vec$'|)) |tptp.'N_a_n_vec_fun$'| (as |@_tptp.'N_a_n_vec_fun$'__1| |tptp.'N_a_n_vec_fun$'|)) % 140.60/140.98 (define-fun |tptp.'uminus$f'| ((BOUND_VARIABLE_49483 |tptp.'A_b_vec_b_vec$'|)) |tptp.'A_b_vec_b_vec$'| (as |@_tptp.'A_b_vec_b_vec$'__1| |tptp.'A_b_vec_b_vec$'|)) % 140.60/140.98 (define-fun |tptp.'uvq$'| (($x1 |tptp.'A_a_b_vec_n_vec_fun$'|) ($x2 |tptp.'A_n_vec_n_vec$'|)) |tptp.'N_a_b_vec_n_vec_n_vec_fun$'| (ite (and (= (as |@_tptp.'A_a_b_vec_n_vec_fun$'__0| |tptp.'A_a_b_vec_n_vec_fun$'|) $x1) (= (as |@_tptp.'A_n_vec_n_vec$'__0| |tptp.'A_n_vec_n_vec$'|) $x2)) (as |@_tptp.'N_a_b_vec_n_vec_n_vec_fun$'__0| |tptp.'N_a_b_vec_n_vec_n_vec_fun$'|) (as |@_tptp.'N_a_b_vec_n_vec_n_vec_fun$'__1| |tptp.'N_a_b_vec_n_vec_n_vec_fun$'|))) % 140.60/140.98 (define-fun |tptp.'interchange_rows_row$b'| ((BOUND_VARIABLE_6868 |tptp.'A_b_vec_n_vec$'|) (BOUND_VARIABLE_6869 |tptp.'N$'|) (BOUND_VARIABLE_6870 |tptp.'N$'|)) |tptp.'N_a_b_vec_fun$'| (ite (= (as |@_tptp.'A_b_vec_n_vec$'__0| |tptp.'A_b_vec_n_vec$'|) (ite (and (= (as |@_tptp.'N_a_b_vec_n_vec_fun$'__1| |tptp.'N_a_b_vec_n_vec_fun$'|) (ite (and (= BOUND_VARIABLE_6868 (as |@_tptp.'A_b_vec_n_vec$'__1| |tptp.'A_b_vec_n_vec$'|)) (= BOUND_VARIABLE_6869 (as |@_tptp.'N$'__0| |tptp.'N$'|))) (as |@_tptp.'N_a_b_vec_n_vec_fun$'__0| |tptp.'N_a_b_vec_n_vec_fun$'|) (as |@_tptp.'N_a_b_vec_n_vec_fun$'__1| |tptp.'N_a_b_vec_n_vec_fun$'|))) (= BOUND_VARIABLE_6870 (as |@_tptp.'N$'__0| |tptp.'N$'|))) (as |@_tptp.'A_b_vec_n_vec$'__0| |tptp.'A_b_vec_n_vec$'|) (as |@_tptp.'A_b_vec_n_vec$'__1| |tptp.'A_b_vec_n_vec$'|))) (as |@_tptp.'N_a_b_vec_fun$'__0| |tptp.'N_a_b_vec_fun$'|) (as |@_tptp.'N_a_b_vec_fun$'__1| |tptp.'N_a_b_vec_fun$'|))) % 140.60/140.98 (define-fun |tptp.'uva$'| (($x1 |tptp.'A_a_b_vec_fun$'|) ($x2 |tptp.'A_n_vec_n_vec$'|)) |tptp.'N_a_b_vec_n_vec_fun$'| (as |@_tptp.'N_a_b_vec_n_vec_fun$'__0| |tptp.'N_a_b_vec_n_vec_fun$'|)) % 140.60/140.98 (define-fun |tptp.'uup$'| (($x1 |tptp.'A_n_vec_n_vec$'|) ($x2 |tptp.'N$'|) ($x3 |tptp.'N$'|) ($x4 |tptp.'N$'|)) |tptp.'N_a_fun$'| (ite (and (= (as |@_tptp.'A_n_vec_n_vec$'__0| |tptp.'A_n_vec_n_vec$'|) $x1) (= (as |@_tptp.'N$'__0| |tptp.'N$'|) $x2) (= (as |@_tptp.'N$'__0| |tptp.'N$'|) $x3) (= (as |@_tptp.'N$'__0| |tptp.'N$'|) $x4)) (as |@_tptp.'N_a_fun$'__0| |tptp.'N_a_fun$'|) (as |@_tptp.'N_a_fun$'__1| |tptp.'N_a_fun$'|))) % 140.60/140.98 (define-fun |tptp.'fun_app$k'| (($x1 |tptp.'A_b_vec_a_b_vec_fun$'|) ($x2 |tptp.'A_b_vec$'|)) |tptp.'A_b_vec$'| (ite (and (= (as |@_tptp.'A_b_vec_a_b_vec_fun$'__1| |tptp.'A_b_vec_a_b_vec_fun$'|) $x1) (= (as |@_tptp.'A_b_vec$'__0| |tptp.'A_b_vec$'|) $x2)) (as |@_tptp.'A_b_vec$'__0| |tptp.'A_b_vec$'|) (as |@_tptp.'A_b_vec$'__1| |tptp.'A_b_vec$'|))) % 140.60/140.98 (define-fun |tptp.'columnvector$g'| ((BOUND_VARIABLE_7330 |tptp.'A_n_vec$'|)) |tptp.'A_b_vec_n_vec$'| (ite (= (as |@_tptp.'N_a_b_vec_fun$'__0| |tptp.'N_a_b_vec_fun$'|) (ite (= BOUND_VARIABLE_7330 (as |@_tptp.'A_n_vec$'__1| |tptp.'A_n_vec$'|)) (as |@_tptp.'N_a_b_vec_fun$'__0| |tptp.'N_a_b_vec_fun$'|) (as |@_tptp.'N_a_b_vec_fun$'__1| |tptp.'N_a_b_vec_fun$'|))) (as |@_tptp.'A_b_vec_n_vec$'__0| |tptp.'A_b_vec_n_vec$'|) (as |@_tptp.'A_b_vec_n_vec$'__1| |tptp.'A_b_vec_n_vec$'|))) % 140.60/140.98 (define-fun |tptp.'row_add_row$'| ((BOUND_VARIABLE_49553 |tptp.'A_b_vec_n_vec_n_vec$'|) (BOUND_VARIABLE_49555 |tptp.'N$'|) (BOUND_VARIABLE_49557 |tptp.'N$'|) (BOUND_VARIABLE_49559 |tptp.'A_b_vec$'|)) |tptp.'N_a_b_vec_n_vec_fun$'| (as |@_tptp.'N_a_b_vec_n_vec_fun$'__1| |tptp.'N_a_b_vec_n_vec_fun$'|)) % 140.60/140.98 (define-fun |tptp.'one$c'| () |tptp.'A_b_vec$'| (as |@_tptp.'A_b_vec$'__0| |tptp.'A_b_vec$'|)) % 140.60/140.98 (define-fun |tptp.'uxf$'| (($x1 |tptp.'A_b_vec_n_vec_n_vec$'|) ($x2 |tptp.'N$'|) ($x3 |tptp.'A_b_vec$'|) ($x4 |tptp.'N$'|)) |tptp.'N_a_b_vec_fun$'| (ite (and (= (as |@_tptp.'A_b_vec_n_vec_n_vec$'__1| |tptp.'A_b_vec_n_vec_n_vec$'|) $x1) (= (as |@_tptp.'N$'__0| |tptp.'N$'|) $x2) (= (as |@_tptp.'A_b_vec$'__1| |tptp.'A_b_vec$'|) $x3) (= (as |@_tptp.'N$'__0| |tptp.'N$'|) $x4)) (as |@_tptp.'N_a_b_vec_fun$'__0| |tptp.'N_a_b_vec_fun$'|) (ite (and (= (as |@_tptp.'A_b_vec_n_vec_n_vec$'__0| |tptp.'A_b_vec_n_vec_n_vec$'|) $x1) (= (as |@_tptp.'N$'__0| |tptp.'N$'|) $x2) (= (as |@_tptp.'A_b_vec$'__1| |tptp.'A_b_vec$'|) $x3) (= (as |@_tptp.'N$'__0| |tptp.'N$'|) $x4)) (as |@_tptp.'N_a_b_vec_fun$'__0| |tptp.'N_a_b_vec_fun$'|) (ite (and (= (as |@_tptp.'A_b_vec_n_vec_n_vec$'__0| |tptp.'A_b_vec_n_vec_n_vec$'|) $x1) (= (as |@_tptp.'N$'__0| |tptp.'N$'|) $x2) (= (as |@_tptp.'A_b_vec$'__0| |tptp.'A_b_vec$'|) $x3) (= (as |@_tptp.'N$'__0| |tptp.'N$'|) $x4)) (as |@_tptp.'N_a_b_vec_fun$'__0| |tptp.'N_a_b_vec_fun$'|) (as |@_tptp.'N_a_b_vec_fun$'__1| |tptp.'N_a_b_vec_fun$'|))))) % 140.60/140.98 (define-fun |tptp.'uuy$'| (($x1 |tptp.'A_a_fun$'|) ($x2 |tptp.'A_b_vec_n_vec$'|)) |tptp.'N_a_b_vec_fun$'| (ite (and (= (as |@_tptp.'A_a_fun$'__1| |tptp.'A_a_fun$'|) $x1) (= (as |@_tptp.'A_b_vec_n_vec$'__0| |tptp.'A_b_vec_n_vec$'|) $x2)) (as |@_tptp.'N_a_b_vec_fun$'__0| |tptp.'N_a_b_vec_fun$'|) (ite (and (= (as |@_tptp.'A_a_fun$'__1| |tptp.'A_a_fun$'|) $x1) (= (as |@_tptp.'A_b_vec_n_vec$'__1| |tptp.'A_b_vec_n_vec$'|) $x2)) (as |@_tptp.'N_a_b_vec_fun$'__0| |tptp.'N_a_b_vec_fun$'|) (ite (and (= (as |@_tptp.'A_a_fun$'__0| |tptp.'A_a_fun$'|) $x1) (= (as |@_tptp.'A_b_vec_n_vec$'__0| |tptp.'A_b_vec_n_vec$'|) $x2)) (as |@_tptp.'N_a_b_vec_fun$'__0| |tptp.'N_a_b_vec_fun$'|) (as |@_tptp.'N_a_b_vec_fun$'__1| |tptp.'N_a_b_vec_fun$'|))))) % 140.60/140.98 (define-fun |tptp.'uwm$'| (($x1 |tptp.'A_b_vec_n_vec_n_vec$'|)) |tptp.'N_a_b_vec_n_vec_n_vec_fun$'| (ite (= (as |@_tptp.'A_b_vec_n_vec_n_vec$'__1| |tptp.'A_b_vec_n_vec_n_vec$'|) $x1) (as |@_tptp.'N_a_b_vec_n_vec_n_vec_fun$'__0| |tptp.'N_a_b_vec_n_vec_n_vec_fun$'|) (as |@_tptp.'N_a_b_vec_n_vec_n_vec_fun$'__1| |tptp.'N_a_b_vec_n_vec_n_vec_fun$'|))) % 140.60/140.98 (define-fun |tptp.'least$'| (($x1 |tptp.'N_bool_fun$'|)) |tptp.'N$'| (as |@_tptp.'N$'__0| |tptp.'N$'|)) % 140.60/140.98 (define-fun |tptp.'fun_app$ad'| (($x1 |tptp.'B_a_bool_fun_fun$'|) ($x2 |tptp.'B$'|)) |tptp.'A_bool_fun$'| (as |@_tptp.'A_bool_fun$'__0| |tptp.'A_bool_fun$'|)) % 140.60/140.98 (define-fun |tptp.'map_matrix$h'| (($x1 |tptp.'A_b_vec_n_vec_a_fun$'|) ($x2 |tptp.'A_b_vec_n_vec_n_vec_n_vec$'|)) |tptp.'A_n_vec_n_vec$'| (ite (and (= (as |@_tptp.'A_b_vec_n_vec_a_fun$'__0| |tptp.'A_b_vec_n_vec_a_fun$'|) $x1) (= (as |@_tptp.'A_b_vec_n_vec_n_vec_n_vec$'__1| |tptp.'A_b_vec_n_vec_n_vec_n_vec$'|) $x2)) (as |@_tptp.'A_n_vec_n_vec$'__0| |tptp.'A_n_vec_n_vec$'|) (as |@_tptp.'A_n_vec_n_vec$'__1| |tptp.'A_n_vec_n_vec$'|))) % 140.60/140.98 (define-fun |tptp.'uwf$'| (($x1 |tptp.'A_b_vec_n_vec$'|) ($x2 |tptp.'N$'|) ($x3 |tptp.'B$'|)) |tptp.'N_bool_fun$'| (ite (and (= (as |@_tptp.'A_b_vec_n_vec$'__0| |tptp.'A_b_vec_n_vec$'|) $x1) (= (as |@_tptp.'N$'__0| |tptp.'N$'|) $x2) (= (as |@_tptp.'B$'__0| |tptp.'B$'|) $x3)) (as |@_tptp.'N_bool_fun$'__0| |tptp.'N_bool_fun$'|) (as |@_tptp.'N_bool_fun$'__1| |tptp.'N_bool_fun$'|))) % 140.60/140.98 (define-fun |tptp.'a$a'| () |tptp.'A_b_vec_n_vec$'| (as |@_tptp.'A_b_vec_n_vec$'__1| |tptp.'A_b_vec_n_vec$'|)) % 140.60/140.98 (define-fun |tptp.'vec_lambda$f'| (($x1 |tptp.'N_a_n_vec_n_vec_fun$'|)) |tptp.'A_n_vec_n_vec_n_vec$'| (as |@_tptp.'A_n_vec_n_vec_n_vec$'__0| |tptp.'A_n_vec_n_vec_n_vec$'|)) % 140.60/140.98 (define-fun |tptp.'mult_row$b'| ((BOUND_VARIABLE_7414 |tptp.'A_b_vec_n_vec_n_vec$'|) (BOUND_VARIABLE_7415 |tptp.'N$'|) (BOUND_VARIABLE_7416 |tptp.'A_b_vec$'|)) |tptp.'A_b_vec_n_vec_n_vec$'| (ite (= (as |@_tptp.'N_a_b_vec_n_vec_fun$'__1| |tptp.'N_a_b_vec_n_vec_fun$'|) (ite (and (= BOUND_VARIABLE_7414 (as |@_tptp.'A_b_vec_n_vec_n_vec$'__1| |tptp.'A_b_vec_n_vec_n_vec$'|)) (= BOUND_VARIABLE_7415 (as |@_tptp.'N$'__0| |tptp.'N$'|)) (= BOUND_VARIABLE_7416 (as |@_tptp.'A_b_vec$'__0| |tptp.'A_b_vec$'|))) (as |@_tptp.'N_a_b_vec_n_vec_fun$'__0| |tptp.'N_a_b_vec_n_vec_fun$'|) (as |@_tptp.'N_a_b_vec_n_vec_fun$'__1| |tptp.'N_a_b_vec_n_vec_fun$'|))) (as |@_tptp.'A_b_vec_n_vec_n_vec$'__0| |tptp.'A_b_vec_n_vec_n_vec$'|) (as |@_tptp.'A_b_vec_n_vec_n_vec$'__1| |tptp.'A_b_vec_n_vec_n_vec$'|))) % 140.60/140.98 (define-fun |tptp.'uvg$'| (($x1 |tptp.'A_a_fun$'|) ($x2 |tptp.'A_b_vec_b_vec$'|)) |tptp.'B_a_b_vec_fun$'| (ite (and (= (as |@_tptp.'A_a_fun$'__0| |tptp.'A_a_fun$'|) $x1) (= (as |@_tptp.'A_b_vec_b_vec$'__0| |tptp.'A_b_vec_b_vec$'|) $x2)) (as |@_tptp.'B_a_b_vec_fun$'__0| |tptp.'B_a_b_vec_fun$'|) (as |@_tptp.'B_a_b_vec_fun$'__1| |tptp.'B_a_b_vec_fun$'|))) % 140.60/140.98 (define-fun |tptp.'rowvector$b'| ((BOUND_VARIABLE_7249 |tptp.'A_b_vec_n_vec$'|)) |tptp.'A_b_vec_n_vec_n_vec$'| (ite (= (as |@_tptp.'N_a_b_vec_n_vec_fun$'__1| |tptp.'N_a_b_vec_n_vec_fun$'|) (ite (= BOUND_VARIABLE_7249 (as |@_tptp.'A_b_vec_n_vec$'__1| |tptp.'A_b_vec_n_vec$'|)) (as |@_tptp.'N_a_b_vec_n_vec_fun$'__0| |tptp.'N_a_b_vec_n_vec_fun$'|) (as |@_tptp.'N_a_b_vec_n_vec_fun$'__1| |tptp.'N_a_b_vec_n_vec_fun$'|))) (as |@_tptp.'A_b_vec_n_vec_n_vec$'__0| |tptp.'A_b_vec_n_vec_n_vec$'|) (as |@_tptp.'A_b_vec_n_vec_n_vec$'__1| |tptp.'A_b_vec_n_vec_n_vec$'|))) % 140.60/140.98 (define-fun |tptp.'uum$'| (($x1 |tptp.'A_b_vec_n_vec_n_vec$'|) ($x2 |tptp.'N$'|) ($x3 |tptp.'N$'|)) |tptp.'N_a_b_vec_n_vec_fun$'| (ite (and (= (as |@_tptp.'A_b_vec_n_vec_n_vec$'__1| |tptp.'A_b_vec_n_vec_n_vec$'|) $x1) (= (as |@_tptp.'N$'__0| |tptp.'N$'|) $x2) (= (as |@_tptp.'N$'__0| |tptp.'N$'|) $x3)) (as |@_tptp.'N_a_b_vec_n_vec_fun$'__0| |tptp.'N_a_b_vec_n_vec_fun$'|) (as |@_tptp.'N_a_b_vec_n_vec_fun$'__1| |tptp.'N_a_b_vec_n_vec_fun$'|))) % 140.60/140.98 (define-fun |tptp.'uwc$'| () |tptp.'N_a_b_vec_fun$'| (as |@_tptp.'N_a_b_vec_fun$'__1| |tptp.'N_a_b_vec_fun$'|)) % 140.60/140.98 (define-fun |tptp.'uxl$'| (($x1 |tptp.'A_n_vec$'|) ($x2 |tptp.'A_n_vec$'|)) |tptp.'N_a_fun$'| (ite (and (= (as |@_tptp.'A_n_vec$'__0| |tptp.'A_n_vec$'|) $x1) (= (as |@_tptp.'A_n_vec$'__0| |tptp.'A_n_vec$'|) $x2)) (as |@_tptp.'N_a_fun$'__0| |tptp.'N_a_fun$'|) (as |@_tptp.'N_a_fun$'__1| |tptp.'N_a_fun$'|))) % 140.60/140.98 (define-fun |tptp.'uux$'| (($x1 |tptp.'A_a_fun$'|) ($x2 |tptp.'A_b_vec_n_vec$'|) ($x3 |tptp.'N$'|)) |tptp.'B_a_fun$'| (ite (and (= (as |@_tptp.'A_a_fun$'__0| |tptp.'A_a_fun$'|) $x1) (= (as |@_tptp.'A_b_vec_n_vec$'__1| |tptp.'A_b_vec_n_vec$'|) $x2) (= (as |@_tptp.'N$'__0| |tptp.'N$'|) $x3)) (as |@_tptp.'B_a_fun$'__0| |tptp.'B_a_fun$'|) (as |@_tptp.'B_a_fun$'__1| |tptp.'B_a_fun$'|))) % 140.60/140.98 (define-fun |tptp.'times$e'| ((BOUND_VARIABLE_7530 |tptp.'A_n_vec_n_vec$'|) (BOUND_VARIABLE_7531 |tptp.'A_n_vec_n_vec$'|)) |tptp.'A_n_vec_n_vec$'| (ite (= (as |@_tptp.'N_a_n_vec_fun$'__0| |tptp.'N_a_n_vec_fun$'|) (ite (and (= BOUND_VARIABLE_7530 (as |@_tptp.'A_n_vec_n_vec$'__0| |tptp.'A_n_vec_n_vec$'|)) (= BOUND_VARIABLE_7531 (as |@_tptp.'A_n_vec_n_vec$'__0| |tptp.'A_n_vec_n_vec$'|))) (as |@_tptp.'N_a_n_vec_fun$'__0| |tptp.'N_a_n_vec_fun$'|) (as |@_tptp.'N_a_n_vec_fun$'__1| |tptp.'N_a_n_vec_fun$'|))) (as |@_tptp.'A_n_vec_n_vec$'__0| |tptp.'A_n_vec_n_vec$'|) (as |@_tptp.'A_n_vec_n_vec$'__1| |tptp.'A_n_vec_n_vec$'|))) % 140.60/140.98 (define-fun |tptp.'row_add_row$b'| ((BOUND_VARIABLE_7373 |tptp.'A_b_vec_n_vec$'|) (BOUND_VARIABLE_7374 |tptp.'N$'|) (BOUND_VARIABLE_7375 |tptp.'N$'|) (BOUND_VARIABLE_7376 |tptp.'A$'|)) |tptp.'N_a_b_vec_fun$'| (ite (= (as |@_tptp.'A_b_vec_n_vec$'__0| |tptp.'A_b_vec_n_vec$'|) (ite (= BOUND_VARIABLE_7376 (as |@_tptp.'A$'__0| |tptp.'A$'|)) (as |@_tptp.'A_b_vec_n_vec$'__0| |tptp.'A_b_vec_n_vec$'|) (as |@_tptp.'A_b_vec_n_vec$'__1| |tptp.'A_b_vec_n_vec$'|))) (as |@_tptp.'N_a_b_vec_fun$'__0| |tptp.'N_a_b_vec_fun$'|) (as |@_tptp.'N_a_b_vec_fun$'__1| |tptp.'N_a_b_vec_fun$'|))) % 140.60/140.98 (define-fun |tptp.'uud$'| (($x1 |tptp.'A_n_vec$'|)) |tptp.'N_a_fun$'| (as |@_tptp.'N_a_fun$'__1| |tptp.'N_a_fun$'|)) % 140.60/140.98 (define-fun |tptp.'interchange_rows$'| (($x1 |tptp.'A_b_vec_n_vec$'|) ($x2 |tptp.'N$'|)) |tptp.'N_a_b_vec_n_vec_fun$'| (ite (and (= (as |@_tptp.'A_b_vec_n_vec$'__1| |tptp.'A_b_vec_n_vec$'|) $x1) (= (as |@_tptp.'N$'__0| |tptp.'N$'|) $x2)) (as |@_tptp.'N_a_b_vec_n_vec_fun$'__0| |tptp.'N_a_b_vec_n_vec_fun$'|) (as |@_tptp.'N_a_b_vec_n_vec_fun$'__1| |tptp.'N_a_b_vec_n_vec_fun$'|))) % 140.60/140.98 (define-fun |tptp.'fun_app$g'| (($x1 |tptp.'N_a_b_vec_b_vec_fun$'|) ($x2 |tptp.'N$'|)) |tptp.'A_b_vec_b_vec$'| (ite (and (= (as |@_tptp.'N_a_b_vec_b_vec_fun$'__0| |tptp.'N_a_b_vec_b_vec_fun$'|) $x1) (= (as |@_tptp.'N$'__0| |tptp.'N$'|) $x2)) (as |@_tptp.'A_b_vec_b_vec$'__0| |tptp.'A_b_vec_b_vec$'|) (as |@_tptp.'A_b_vec_b_vec$'__1| |tptp.'A_b_vec_b_vec$'|))) % 140.60/140.98 (define-fun |tptp.'uvn$'| (($x1 |tptp.'A_n_vec_a_fun$'|) ($x2 |tptp.'A_n_vec_n_vec_n_vec$'|) ($x3 |tptp.'N$'|)) |tptp.'N_a_fun$'| (as |@_tptp.'N_a_fun$'__1| |tptp.'N_a_fun$'|)) % 140.60/140.98 (define-fun |tptp.'one$d'| () |tptp.'A_b_vec_n_vec_n_vec$'| (as |@_tptp.'A_b_vec_n_vec_n_vec$'__1| |tptp.'A_b_vec_n_vec_n_vec$'|)) % 140.60/140.98 (define-fun |tptp.'uuc$'| (($x1 |tptp.'A_b_vec_b_vec$'|)) |tptp.'B_a_b_vec_fun$'| (as |@_tptp.'B_a_b_vec_fun$'__1| |tptp.'B_a_b_vec_fun$'|)) % 140.60/140.98 (define-fun |tptp.'uue$'| (($x1 |tptp.'A_b_vec_n_vec_n_vec$'|)) |tptp.'N_a_b_vec_n_vec_fun$'| (as |@_tptp.'N_a_b_vec_n_vec_fun$'__1| |tptp.'N_a_b_vec_n_vec_fun$'|)) % 140.60/140.98 (define-fun |tptp.'m$'| () |tptp.'N$'| (as |@_tptp.'N$'__0| |tptp.'N$'|)) % 140.60/140.98 (define-fun |tptp.'uvp$'| (($x1 |tptp.'A_a_b_vec_n_vec_fun$'|) ($x2 |tptp.'A_n_vec_n_vec$'|) ($x3 |tptp.'N$'|)) |tptp.'N_a_b_vec_n_vec_fun$'| (ite (and (= (as |@_tptp.'A_a_b_vec_n_vec_fun$'__0| |tptp.'A_a_b_vec_n_vec_fun$'|) $x1) (= (as |@_tptp.'A_n_vec_n_vec$'__0| |tptp.'A_n_vec_n_vec$'|) $x2) (= (as |@_tptp.'N$'__0| |tptp.'N$'|) $x3)) (as |@_tptp.'N_a_b_vec_n_vec_fun$'__0| |tptp.'N_a_b_vec_n_vec_fun$'|) (as |@_tptp.'N_a_b_vec_n_vec_fun$'__1| |tptp.'N_a_b_vec_n_vec_fun$'|))) % 140.60/140.98 (define-fun |tptp.'uua$'| (($x1 |tptp.'A_b_vec_n_vec$'|) ($x2 |tptp.'A_b_vec_n_vec$'|)) |tptp.'N_a_b_vec_fun$'| (ite (and (= (as |@_tptp.'A_b_vec_n_vec$'__0| |tptp.'A_b_vec_n_vec$'|) $x1) (= (as |@_tptp.'A_b_vec_n_vec$'__0| |tptp.'A_b_vec_n_vec$'|) $x2)) (as |@_tptp.'N_a_b_vec_fun$'__0| |tptp.'N_a_b_vec_fun$'|) (ite (and (= (as |@_tptp.'A_b_vec_n_vec$'__1| |tptp.'A_b_vec_n_vec$'|) $x1) (= (as |@_tptp.'A_b_vec_n_vec$'__0| |tptp.'A_b_vec_n_vec$'|) $x2)) (as |@_tptp.'N_a_b_vec_fun$'__0| |tptp.'N_a_b_vec_fun$'|) (as |@_tptp.'N_a_b_vec_fun$'__1| |tptp.'N_a_b_vec_fun$'|)))) % 140.60/140.98 (define-fun |tptp.'uvi$'| (($x1 |tptp.'A_a_n_vec_fun$'|) ($x2 |tptp.'A_n_vec_n_vec$'|)) |tptp.'N_a_n_vec_n_vec_fun$'| (as |@_tptp.'N_a_n_vec_n_vec_fun$'__0| |tptp.'N_a_n_vec_n_vec_fun$'|)) % 140.60/140.98 (define-fun |tptp.'zero$b'| () |tptp.'A_b_vec_n_vec$'| (as |@_tptp.'A_b_vec_n_vec$'__0| |tptp.'A_b_vec_n_vec$'|)) % 140.60/140.98 (define-fun |tptp.'interchange_columns_row$b'| ((BOUND_VARIABLE_6908 |tptp.'A_b_vec_n_vec$'|) (BOUND_VARIABLE_6909 |tptp.'B$'|) (BOUND_VARIABLE_6910 |tptp.'B$'|)) |tptp.'N_a_b_vec_fun$'| (ite (= (as |@_tptp.'A_b_vec_n_vec$'__0| |tptp.'A_b_vec_n_vec$'|) (ite (= (as |@_tptp.'N_a_b_vec_fun$'__0| |tptp.'N_a_b_vec_fun$'|) (ite (and (= BOUND_VARIABLE_6908 (as |@_tptp.'A_b_vec_n_vec$'__0| |tptp.'A_b_vec_n_vec$'|)) (= BOUND_VARIABLE_6909 (as |@_tptp.'B$'__0| |tptp.'B$'|)) (= BOUND_VARIABLE_6910 (as |@_tptp.'B$'__0| |tptp.'B$'|))) (as |@_tptp.'N_a_b_vec_fun$'__0| |tptp.'N_a_b_vec_fun$'|) (as |@_tptp.'N_a_b_vec_fun$'__1| |tptp.'N_a_b_vec_fun$'|))) (as |@_tptp.'A_b_vec_n_vec$'__0| |tptp.'A_b_vec_n_vec$'|) (as |@_tptp.'A_b_vec_n_vec$'__1| |tptp.'A_b_vec_n_vec$'|))) (as |@_tptp.'N_a_b_vec_fun$'__0| |tptp.'N_a_b_vec_fun$'|) (as |@_tptp.'N_a_b_vec_fun$'__1| |tptp.'N_a_b_vec_fun$'|))) % 140.60/140.98 (define-fun |tptp.'uxo$'| (($x1 |tptp.'A_b_vec_n_vec$'|) ($x2 |tptp.'A_b_vec_n_vec$'|)) |tptp.'N_a_b_vec_fun$'| (ite (and (= (as |@_tptp.'A_b_vec_n_vec$'__0| |tptp.'A_b_vec_n_vec$'|) $x1) (= (as |@_tptp.'A_b_vec_n_vec$'__0| |tptp.'A_b_vec_n_vec$'|) $x2)) (as |@_tptp.'N_a_b_vec_fun$'__0| |tptp.'N_a_b_vec_fun$'|) (ite (and (= (as |@_tptp.'A_b_vec_n_vec$'__0| |tptp.'A_b_vec_n_vec$'|) $x1) (= (as |@_tptp.'A_b_vec_n_vec$'__1| |tptp.'A_b_vec_n_vec$'|) $x2)) (as |@_tptp.'N_a_b_vec_fun$'__0| |tptp.'N_a_b_vec_fun$'|) (ite (and (= (as |@_tptp.'A_b_vec_n_vec$'__1| |tptp.'A_b_vec_n_vec$'|) $x1) (= (as |@_tptp.'A_b_vec_n_vec$'__0| |tptp.'A_b_vec_n_vec$'|) $x2)) (as |@_tptp.'N_a_b_vec_fun$'__0| |tptp.'N_a_b_vec_fun$'|) (as |@_tptp.'N_a_b_vec_fun$'__1| |tptp.'N_a_b_vec_fun$'|))))) % 140.60/140.98 (define-fun |tptp.'zero$c'| () |tptp.'A_n_vec$'| (as |@_tptp.'A_n_vec$'__1| |tptp.'A_n_vec$'|)) % 140.60/140.98 (define-fun |tptp.'uwn$'| (($x1 |tptp.'A_b_vec$'|) ($x2 |tptp.'B$'|)) |tptp.'N_a_fun$'| (ite (and (= (as |@_tptp.'A_b_vec$'__0| |tptp.'A_b_vec$'|) $x1) (= (as |@_tptp.'B$'__0| |tptp.'B$'|) $x2)) (as |@_tptp.'N_a_fun$'__0| |tptp.'N_a_fun$'|) (as |@_tptp.'N_a_fun$'__1| |tptp.'N_a_fun$'|))) % 140.60/140.98 (define-fun |tptp.'uvu$'| () |tptp.'B_a_fun$'| (as |@_tptp.'B_a_fun$'__1| |tptp.'B_a_fun$'|)) % 140.60/140.98 (define-fun |tptp.'columnvector$'| ((BOUND_VARIABLE_7267 |tptp.'A_b_vec_n_vec_n_vec$'|)) |tptp.'A_b_vec_n_vec_n_vec_n_vec$'| (ite (= (as |@_tptp.'N_a_b_vec_n_vec_n_vec_fun$'__0| |tptp.'N_a_b_vec_n_vec_n_vec_fun$'|) (ite (= BOUND_VARIABLE_7267 (as |@_tptp.'A_b_vec_n_vec_n_vec$'__1| |tptp.'A_b_vec_n_vec_n_vec$'|)) (as |@_tptp.'N_a_b_vec_n_vec_n_vec_fun$'__0| |tptp.'N_a_b_vec_n_vec_n_vec_fun$'|) (as |@_tptp.'N_a_b_vec_n_vec_n_vec_fun$'__1| |tptp.'N_a_b_vec_n_vec_n_vec_fun$'|))) (as |@_tptp.'A_b_vec_n_vec_n_vec_n_vec$'__0| |tptp.'A_b_vec_n_vec_n_vec_n_vec$'|) (as |@_tptp.'A_b_vec_n_vec_n_vec_n_vec$'__1| |tptp.'A_b_vec_n_vec_n_vec_n_vec$'|))) % 140.60/140.98 (define-fun |tptp.'zero$e'| () |tptp.'A_n_vec_n_vec$'| (as |@_tptp.'A_n_vec_n_vec$'__1| |tptp.'A_n_vec_n_vec$'|)) % 140.60/140.98 (define-fun |tptp.'map_matrix$a'| ((BOUND_VARIABLE_7063 |tptp.'A_a_fun$'|) (BOUND_VARIABLE_7064 |tptp.'A_n_vec_n_vec$'|)) |tptp.'A_n_vec_n_vec$'| (ite (= (as |@_tptp.'N_a_n_vec_fun$'__0| |tptp.'N_a_n_vec_fun$'|) (ite (and (= BOUND_VARIABLE_7063 (as |@_tptp.'A_a_fun$'__0| |tptp.'A_a_fun$'|)) (= BOUND_VARIABLE_7064 (as |@_tptp.'A_n_vec_n_vec$'__0| |tptp.'A_n_vec_n_vec$'|))) (as |@_tptp.'N_a_n_vec_fun$'__0| |tptp.'N_a_n_vec_fun$'|) (as |@_tptp.'N_a_n_vec_fun$'__1| |tptp.'N_a_n_vec_fun$'|))) (as |@_tptp.'A_n_vec_n_vec$'__0| |tptp.'A_n_vec_n_vec$'|) (as |@_tptp.'A_n_vec_n_vec$'__1| |tptp.'A_n_vec_n_vec$'|))) % 140.60/140.98 (define-fun |tptp.'uwi$'| (($x1 |tptp.'A_b_vec$'|)) |tptp.'B_a_b_vec_fun$'| (ite (= (as |@_tptp.'A_b_vec$'__0| |tptp.'A_b_vec$'|) $x1) (as |@_tptp.'B_a_b_vec_fun$'__0| |tptp.'B_a_b_vec_fun$'|) (as |@_tptp.'B_a_b_vec_fun$'__1| |tptp.'B_a_b_vec_fun$'|))) % 140.60/140.98 (define-fun |tptp.'map_matrix$e'| ((BOUND_VARIABLE_49776 |tptp.'A_a_n_vec_fun$'|) (BOUND_VARIABLE_49778 |tptp.'A_n_vec_n_vec$'|)) |tptp.'A_n_vec_n_vec_n_vec$'| (as |@_tptp.'A_n_vec_n_vec_n_vec$'__0| |tptp.'A_n_vec_n_vec_n_vec$'|)) % 140.60/140.98 (define-fun |tptp.'vec_nth$c'| (($x1 |tptp.'A_n_vec_n_vec$'|)) |tptp.'N_a_n_vec_fun$'| (ite (= (as |@_tptp.'A_n_vec_n_vec$'__0| |tptp.'A_n_vec_n_vec$'|) $x1) (as |@_tptp.'N_a_n_vec_fun$'__0| |tptp.'N_a_n_vec_fun$'|) (as |@_tptp.'N_a_n_vec_fun$'__1| |tptp.'N_a_n_vec_fun$'|))) % 140.60/140.98 (define-fun |tptp.'fun_app$f'| (($x1 |tptp.'N_a_n_vec_fun$'|) ($x2 |tptp.'N$'|)) |tptp.'A_n_vec$'| (ite (and (= (as |@_tptp.'N_a_n_vec_fun$'__0| |tptp.'N_a_n_vec_fun$'|) $x1) (= (as |@_tptp.'N$'__0| |tptp.'N$'|) $x2)) (as |@_tptp.'A_n_vec$'__0| |tptp.'A_n_vec$'|) (as |@_tptp.'A_n_vec$'__1| |tptp.'A_n_vec$'|))) % 140.60/140.98 (define-fun |tptp.'uvh$'| (($x1 |tptp.'A_a_n_vec_fun$'|) ($x2 |tptp.'A_n_vec_n_vec$'|) ($x3 |tptp.'N$'|)) |tptp.'N_a_n_vec_fun$'| (as |@_tptp.'N_a_n_vec_fun$'__0| |tptp.'N_a_n_vec_fun$'|)) % 140.60/140.98 (define-fun |tptp.'vec_nth$a'| (($x1 |tptp.'A_b_vec_n_vec$'|)) |tptp.'N_a_b_vec_fun$'| (ite (= (as |@_tptp.'A_b_vec_n_vec$'__0| |tptp.'A_b_vec_n_vec$'|) $x1) (as |@_tptp.'N_a_b_vec_fun$'__0| |tptp.'N_a_b_vec_fun$'|) (as |@_tptp.'N_a_b_vec_fun$'__1| |tptp.'N_a_b_vec_fun$'|))) % 140.60/140.98 (define-fun |tptp.'uvz$'| () |tptp.'B_a_b_vec_fun$'| (as |@_tptp.'B_a_b_vec_fun$'__0| |tptp.'B_a_b_vec_fun$'|)) % 140.60/140.98 (define-fun |tptp.'vec_lambda$e'| (($x1 |tptp.'N_a_b_vec_n_vec_fun$'|)) |tptp.'A_b_vec_n_vec_n_vec$'| (ite (= (as |@_tptp.'N_a_b_vec_n_vec_fun$'__1| |tptp.'N_a_b_vec_n_vec_fun$'|) $x1) (as |@_tptp.'A_b_vec_n_vec_n_vec$'__0| |tptp.'A_b_vec_n_vec_n_vec$'|) (as |@_tptp.'A_b_vec_n_vec_n_vec$'__1| |tptp.'A_b_vec_n_vec_n_vec$'|))) % 140.60/140.98 (define-fun |tptp.'uxu$'| () |tptp.'A_n_vec_a_n_vec_fun$'| (as |@_tptp.'A_n_vec_a_n_vec_fun$'__0| |tptp.'A_n_vec_a_n_vec_fun$'|)) % 140.60/140.98 (define-fun |tptp.'fun_app$a'| (($x1 |tptp.'B_a_fun$'|) ($x2 |tptp.'B$'|)) |tptp.'A$'| (ite (and (= (as |@_tptp.'B_a_fun$'__1| |tptp.'B_a_fun$'|) $x1) (= (as |@_tptp.'B$'__0| |tptp.'B$'|) $x2)) (as |@_tptp.'A$'__0| |tptp.'A$'|) (as |@_tptp.'A$'__1| |tptp.'A$'|))) % 140.60/140.98 (define-fun |tptp.'vec_nth$b'| (($x1 |tptp.'A_b_vec_n_vec_n_vec$'|)) |tptp.'N_a_b_vec_n_vec_fun$'| (ite (= (as |@_tptp.'A_b_vec_n_vec_n_vec$'__1| |tptp.'A_b_vec_n_vec_n_vec$'|) $x1) (as |@_tptp.'N_a_b_vec_n_vec_fun$'__0| |tptp.'N_a_b_vec_n_vec_fun$'|) (as |@_tptp.'N_a_b_vec_n_vec_fun$'__1| |tptp.'N_a_b_vec_n_vec_fun$'|))) % 140.60/140.98 (define-fun |tptp.'uxj$'| (($x1 |tptp.'A_n_vec_n_vec$'|) ($x2 |tptp.'A_n_vec_n_vec$'|)) |tptp.'N_a_n_vec_fun$'| (ite (and (= (as |@_tptp.'A_n_vec_n_vec$'__0| |tptp.'A_n_vec_n_vec$'|) $x1) (= (as |@_tptp.'A_n_vec_n_vec$'__0| |tptp.'A_n_vec_n_vec$'|) $x2)) (as |@_tptp.'N_a_n_vec_fun$'__0| |tptp.'N_a_n_vec_fun$'|) (as |@_tptp.'N_a_n_vec_fun$'__1| |tptp.'N_a_n_vec_fun$'|))) % 140.60/140.98 (define-fun |tptp.'vec_lambda$a'| (($x1 |tptp.'N_a_b_vec_fun$'|)) |tptp.'A_b_vec_n_vec$'| (ite (= (as |@_tptp.'N_a_b_vec_fun$'__0| |tptp.'N_a_b_vec_fun$'|) $x1) (as |@_tptp.'A_b_vec_n_vec$'__0| |tptp.'A_b_vec_n_vec$'|) (as |@_tptp.'A_b_vec_n_vec$'__1| |tptp.'A_b_vec_n_vec$'|))) % 140.60/140.98 (define-fun |tptp.'fun_app$ae'| (($x1 |tptp.'A_b_vec_bool_fun$'|) ($x2 |tptp.'A_b_vec$'|)) Bool true) % 140.60/140.98 (define-fun |tptp.'vec_lambda$'| (($x1 |tptp.'B_a_fun$'|)) |tptp.'A_b_vec$'| (ite (= (as |@_tptp.'B_a_fun$'__0| |tptp.'B_a_fun$'|) $x1) (as |@_tptp.'A_b_vec$'__0| |tptp.'A_b_vec$'|) (as |@_tptp.'A_b_vec$'__1| |tptp.'A_b_vec$'|))) % 140.60/140.98 (define-fun |tptp.'vec_lambda$i'| ((_arg_1 |tptp.'B_a_n_vec_fun$'|)) |tptp.'A_n_vec_b_vec$'| (as |@_tptp.'A_n_vec_b_vec$'__0| |tptp.'A_n_vec_b_vec$'|)) % 140.60/140.98 (define-fun |tptp.'i$'| () |tptp.'N$'| (as |@_tptp.'N$'__0| |tptp.'N$'|)) % 140.60/140.98 (define-fun |tptp.'n$'| () |tptp.'N$'| (as |@_tptp.'N$'__0| |tptp.'N$'|)) % 140.60/140.98 (define-fun |tptp.'uvo$'| (($x1 |tptp.'A_n_vec_a_fun$'|) ($x2 |tptp.'A_n_vec_n_vec_n_vec$'|)) |tptp.'N_a_n_vec_fun$'| (as |@_tptp.'N_a_n_vec_fun$'__1| |tptp.'N_a_n_vec_fun$'|)) % 140.60/140.98 (define-fun |tptp.'uxp$'| () |tptp.'A_n_vec_a_n_vec_fun$'| (as |@_tptp.'A_n_vec_a_n_vec_fun$'__1| |tptp.'A_n_vec_a_n_vec_fun$'|)) % 140.60/140.98 (define-fun |tptp.'zero$d'| () |tptp.'A_b_vec$'| (as |@_tptp.'A_b_vec$'__1| |tptp.'A_b_vec$'|)) % 140.60/140.98 (define-fun |tptp.'columnvector$b'| ((BOUND_VARIABLE_49809 |tptp.'A_n_vec_n_vec$'|)) |tptp.'A_n_vec_n_vec_n_vec$'| (as |@_tptp.'A_n_vec_n_vec_n_vec$'__0| |tptp.'A_n_vec_n_vec_n_vec$'|)) % 140.60/140.98 (define-fun |tptp.'fun_app$q'| (($x1 |tptp.'A_n_vec_a_fun$'|) ($x2 |tptp.'A_n_vec$'|)) |tptp.'A$'| (as |@_tptp.'A$'__0| |tptp.'A$'|)) % 140.60/140.98 (define-fun |tptp.'fun_app$j'| (($x1 |tptp.'N_a_b_vec_n_vec_n_vec_fun$'|) ($x2 |tptp.'N$'|)) |tptp.'A_b_vec_n_vec_n_vec$'| (ite (and (= (as |@_tptp.'N_a_b_vec_n_vec_n_vec_fun$'__1| |tptp.'N_a_b_vec_n_vec_n_vec_fun$'|) $x1) (= (as |@_tptp.'N$'__0| |tptp.'N$'|) $x2)) (as |@_tptp.'A_b_vec_n_vec_n_vec$'__0| |tptp.'A_b_vec_n_vec_n_vec$'|) (as |@_tptp.'A_b_vec_n_vec_n_vec$'__1| |tptp.'A_b_vec_n_vec_n_vec$'|))) % 140.60/140.98 (define-fun |tptp.'uxx$'| () |tptp.'A_b_vec_a_b_vec_fun$'| (as |@_tptp.'A_b_vec_a_b_vec_fun$'__1| |tptp.'A_b_vec_a_b_vec_fun$'|)) % 140.60/140.98 (define-fun |tptp.'uuv$'| (($x1 |tptp.'A_b_vec_n_vec$'|) ($x2 |tptp.'N$'|) ($x3 |tptp.'N$'|) ($x4 |tptp.'N$'|)) |tptp.'B_a_fun$'| (ite (and (= (as |@_tptp.'A_b_vec_n_vec$'__1| |tptp.'A_b_vec_n_vec$'|) $x1) (= (as |@_tptp.'N$'__0| |tptp.'N$'|) $x2) (= (as |@_tptp.'N$'__0| |tptp.'N$'|) $x3) (= (as |@_tptp.'N$'__0| |tptp.'N$'|) $x4)) (as |@_tptp.'B_a_fun$'__0| |tptp.'B_a_fun$'|) (as |@_tptp.'B_a_fun$'__1| |tptp.'B_a_fun$'|))) % 140.60/140.98 (define-fun |tptp.'uminus$c'| () |tptp.'A_a_fun$'| (as |@_tptp.'A_a_fun$'__1| |tptp.'A_a_fun$'|)) % 140.60/140.98 (define-fun |tptp.'fun_app$h'| (($x1 |tptp.'N_a_n_vec_n_vec_fun$'|) ($x2 |tptp.'N$'|)) |tptp.'A_n_vec_n_vec$'| (ite (and (= (as |@_tptp.'N_a_n_vec_n_vec_fun$'__0| |tptp.'N_a_n_vec_n_vec_fun$'|) $x1) (= (as |@_tptp.'N$'__0| |tptp.'N$'|) $x2)) (as |@_tptp.'A_n_vec_n_vec$'__0| |tptp.'A_n_vec_n_vec$'|) (as |@_tptp.'A_n_vec_n_vec$'__1| |tptp.'A_n_vec_n_vec$'|))) % 140.60/140.98 (define-fun |tptp.'uxt$'| () |tptp.'A_a_fun$'| (as |@_tptp.'A_a_fun$'__1| |tptp.'A_a_fun$'|)) % 140.60/140.98 (define-fun |tptp.'fun_app$o'| (($x1 |tptp.'A_b_vec_n_vec_a_b_vec_n_vec_fun$'|) ($x2 |tptp.'A_b_vec_n_vec$'|)) |tptp.'A_b_vec_n_vec$'| (ite (and (= (as |@_tptp.'A_b_vec_n_vec_a_b_vec_n_vec_fun$'__1| |tptp.'A_b_vec_n_vec_a_b_vec_n_vec_fun$'|) $x1) (= (as |@_tptp.'A_b_vec_n_vec$'__0| |tptp.'A_b_vec_n_vec$'|) $x2)) (as |@_tptp.'A_b_vec_n_vec$'__0| |tptp.'A_b_vec_n_vec$'|) (ite (and (= (as |@_tptp.'A_b_vec_n_vec_a_b_vec_n_vec_fun$'__0| |tptp.'A_b_vec_n_vec_a_b_vec_n_vec_fun$'|) $x1) (= (as |@_tptp.'A_b_vec_n_vec$'__1| |tptp.'A_b_vec_n_vec$'|) $x2)) (as |@_tptp.'A_b_vec_n_vec$'__0| |tptp.'A_b_vec_n_vec$'|) (ite (and (= (as |@_tptp.'A_b_vec_n_vec_a_b_vec_n_vec_fun$'__0| |tptp.'A_b_vec_n_vec_a_b_vec_n_vec_fun$'|) $x1) (= (as |@_tptp.'A_b_vec_n_vec$'__0| |tptp.'A_b_vec_n_vec$'|) $x2)) (as |@_tptp.'A_b_vec_n_vec$'__0| |tptp.'A_b_vec_n_vec$'|) (as |@_tptp.'A_b_vec_n_vec$'__1| |tptp.'A_b_vec_n_vec$'|))))) % 140.60/140.98 (define-fun |tptp.'one$'| () |tptp.'A$'| (as |@_tptp.'A$'__1| |tptp.'A$'|)) % 140.60/140.98 (define-fun |tptp.'uve$'| (($x1 |tptp.'A_a_fun$'|) ($x2 |tptp.'A_n_vec_n_vec$'|)) |tptp.'N_a_n_vec_fun$'| (ite (and (= (as |@_tptp.'A_a_fun$'__0| |tptp.'A_a_fun$'|) $x1) (= (as |@_tptp.'A_n_vec_n_vec$'__0| |tptp.'A_n_vec_n_vec$'|) $x2)) (as |@_tptp.'N_a_n_vec_fun$'__0| |tptp.'N_a_n_vec_fun$'|) (as |@_tptp.'N_a_n_vec_fun$'__1| |tptp.'N_a_n_vec_fun$'|))) % 140.60/140.98 (define-fun |tptp.'uvy$'| () |tptp.'N_a_n_vec_fun$'| (as |@_tptp.'N_a_n_vec_fun$'__0| |tptp.'N_a_n_vec_fun$'|)) % 140.60/140.98 (define-fun |tptp.'times$d'| (($x1 |tptp.'A_b_vec_n_vec_n_vec$'|)) |tptp.'A_b_vec_n_vec_n_vec_a_b_vec_n_vec_n_vec_fun$'| (ite (= (as |@_tptp.'A_b_vec_n_vec_n_vec$'__1| |tptp.'A_b_vec_n_vec_n_vec$'|) $x1) (as |@_tptp.'A_b_vec_n_vec_n_vec_a_b_vec_n_vec_n_vec_fun$'__0| |tptp.'A_b_vec_n_vec_n_vec_a_b_vec_n_vec_n_vec_fun$'|) (as |@_tptp.'A_b_vec_n_vec_n_vec_a_b_vec_n_vec_n_vec_fun$'__1| |tptp.'A_b_vec_n_vec_n_vec_a_b_vec_n_vec_n_vec_fun$'|))) % 140.60/140.98 (define-fun |tptp.'uvj$'| (($x1 |tptp.'A_a_b_vec_fun$'|) ($x2 |tptp.'A_b_vec_n_vec$'|) ($x3 |tptp.'N$'|)) |tptp.'B_a_b_vec_fun$'| (as |@_tptp.'B_a_b_vec_fun$'__0| |tptp.'B_a_b_vec_fun$'|)) % 140.60/140.98 (define-fun |tptp.'uvb$'| (($x1 |tptp.'A_b_vec_a_b_vec_fun$'|) ($x2 |tptp.'A_b_vec_n_vec_n_vec$'|) ($x3 |tptp.'N$'|)) |tptp.'N_a_b_vec_fun$'| (ite (and (= (as |@_tptp.'A_b_vec_a_b_vec_fun$'__0| |tptp.'A_b_vec_a_b_vec_fun$'|) $x1) (= (as |@_tptp.'A_b_vec_n_vec_n_vec$'__1| |tptp.'A_b_vec_n_vec_n_vec$'|) $x2) (= (as |@_tptp.'N$'__0| |tptp.'N$'|) $x3)) (as |@_tptp.'N_a_b_vec_fun$'__0| |tptp.'N_a_b_vec_fun$'|) (ite (and (= (as |@_tptp.'A_b_vec_a_b_vec_fun$'__1| |tptp.'A_b_vec_a_b_vec_fun$'|) $x1) (= (as |@_tptp.'A_b_vec_n_vec_n_vec$'__0| |tptp.'A_b_vec_n_vec_n_vec$'|) $x2) (= (as |@_tptp.'N$'__0| |tptp.'N$'|) $x3)) (as |@_tptp.'N_a_b_vec_fun$'__0| |tptp.'N_a_b_vec_fun$'|) (ite (and (= (as |@_tptp.'A_b_vec_a_b_vec_fun$'__0| |tptp.'A_b_vec_a_b_vec_fun$'|) $x1) (= (as |@_tptp.'A_b_vec_n_vec_n_vec$'__0| |tptp.'A_b_vec_n_vec_n_vec$'|) $x2) (= (as |@_tptp.'N$'__0| |tptp.'N$'|) $x3)) (as |@_tptp.'N_a_b_vec_fun$'__0| |tptp.'N_a_b_vec_fun$'|) (as |@_tptp.'N_a_b_vec_fun$'__1| |tptp.'N_a_b_vec_fun$'|))))) % 140.60/140.98 (define-fun |tptp.'uwa$'| () |tptp.'B_a_fun$'| (as |@_tptp.'B_a_fun$'__0| |tptp.'B_a_fun$'|)) % 140.60/140.98 (define-fun |tptp.'columnvector$c'| ((BOUND_VARIABLE_49834 |tptp.'A_b_vec_n_vec$'|)) |tptp.'A_b_vec_b_vec_n_vec$'| (as |@_tptp.'A_b_vec_b_vec_n_vec$'__0| |tptp.'A_b_vec_b_vec_n_vec$'|)) % 140.60/140.98 (define-fun |tptp.'uuq$'| (($x1 |tptp.'A_n_vec_n_vec$'|) ($x2 |tptp.'N$'|) ($x3 |tptp.'N$'|)) |tptp.'N_a_n_vec_fun$'| (ite (and (= (as |@_tptp.'A_n_vec_n_vec$'__0| |tptp.'A_n_vec_n_vec$'|) $x1) (= (as |@_tptp.'N$'__0| |tptp.'N$'|) $x2) (= (as |@_tptp.'N$'__0| |tptp.'N$'|) $x3)) (as |@_tptp.'N_a_n_vec_fun$'__0| |tptp.'N_a_n_vec_fun$'|) (as |@_tptp.'N_a_n_vec_fun$'__1| |tptp.'N_a_n_vec_fun$'|))) % 140.60/140.98 (define-fun |tptp.'a$'| () |tptp.'A_b_vec_n_vec$'| (as |@_tptp.'A_b_vec_n_vec$'__1| |tptp.'A_b_vec_n_vec$'|)) % 140.60/140.98 (define-fun |tptp.'uvv$'| () |tptp.'N_a_b_vec_n_vec_fun$'| (as |@_tptp.'N_a_b_vec_n_vec_fun$'__1| |tptp.'N_a_b_vec_n_vec_fun$'|)) % 140.60/140.98 (define-fun |tptp.'fun_app$r'| (($x1 |tptp.'A_b_vec_a_fun$'|) ($x2 |tptp.'A_b_vec$'|)) |tptp.'A$'| (as |@_tptp.'A$'__0| |tptp.'A$'|)) % 140.60/140.98 (define-fun |tptp.'interchange_rows$a'| (($x1 |tptp.'A_n_vec_n_vec$'|) ($x2 |tptp.'N$'|)) |tptp.'N_a_n_vec_n_vec_fun$'| (ite (and (= (as |@_tptp.'A_n_vec_n_vec$'__0| |tptp.'A_n_vec_n_vec$'|) $x1) (= (as |@_tptp.'N$'__0| |tptp.'N$'|) $x2)) (as |@_tptp.'N_a_n_vec_n_vec_fun$'__0| |tptp.'N_a_n_vec_n_vec_fun$'|) (as |@_tptp.'N_a_n_vec_n_vec_fun$'__1| |tptp.'N_a_n_vec_n_vec_fun$'|))) % 140.60/140.98 (define-fun |tptp.'map_matrix$i'| ((BOUND_VARIABLE_7129 |tptp.'A_a_b_vec_n_vec_fun$'|) (BOUND_VARIABLE_7130 |tptp.'A_n_vec_n_vec$'|)) |tptp.'A_b_vec_n_vec_n_vec_n_vec$'| (ite (= (as |@_tptp.'N_a_b_vec_n_vec_n_vec_fun$'__0| |tptp.'N_a_b_vec_n_vec_n_vec_fun$'|) (ite (and (= BOUND_VARIABLE_7129 (as |@_tptp.'A_a_b_vec_n_vec_fun$'__0| |tptp.'A_a_b_vec_n_vec_fun$'|)) (= BOUND_VARIABLE_7130 (as |@_tptp.'A_n_vec_n_vec$'__0| |tptp.'A_n_vec_n_vec$'|))) (as |@_tptp.'N_a_b_vec_n_vec_n_vec_fun$'__0| |tptp.'N_a_b_vec_n_vec_n_vec_fun$'|) (as |@_tptp.'N_a_b_vec_n_vec_n_vec_fun$'__1| |tptp.'N_a_b_vec_n_vec_n_vec_fun$'|))) (as |@_tptp.'A_b_vec_n_vec_n_vec_n_vec$'__0| |tptp.'A_b_vec_n_vec_n_vec_n_vec$'|) (as |@_tptp.'A_b_vec_n_vec_n_vec_n_vec$'__1| |tptp.'A_b_vec_n_vec_n_vec_n_vec$'|))) % 140.60/140.98 (define-fun tptp.tltrue () tptp.tlbool (as @tptp.tlbool_1 tptp.tlbool)) % 140.60/140.98 (define-fun |tptp.'map_matrix$'| ((BOUND_VARIABLE_7030 |tptp.'A_a_fun$'|) (BOUND_VARIABLE_7031 |tptp.'A_b_vec_n_vec$'|)) |tptp.'A_b_vec_n_vec$'| (ite (= (as |@_tptp.'N_a_b_vec_fun$'__0| |tptp.'N_a_b_vec_fun$'|) (ite (and (= BOUND_VARIABLE_7030 (as |@_tptp.'A_a_fun$'__1| |tptp.'A_a_fun$'|)) (= BOUND_VARIABLE_7031 (as |@_tptp.'A_b_vec_n_vec$'__0| |tptp.'A_b_vec_n_vec$'|))) (as |@_tptp.'N_a_b_vec_fun$'__0| |tptp.'N_a_b_vec_fun$'|) (ite (and (= BOUND_VARIABLE_7030 (as |@_tptp.'A_a_fun$'__1| |tptp.'A_a_fun$'|)) (= BOUND_VARIABLE_7031 (as |@_tptp.'A_b_vec_n_vec$'__1| |tptp.'A_b_vec_n_vec$'|))) (as |@_tptp.'N_a_b_vec_fun$'__0| |tptp.'N_a_b_vec_fun$'|) (ite (and (= BOUND_VARIABLE_7030 (as |@_tptp.'A_a_fun$'__0| |tptp.'A_a_fun$'|)) (= BOUND_VARIABLE_7031 (as |@_tptp.'A_b_vec_n_vec$'__0| |tptp.'A_b_vec_n_vec$'|))) (as |@_tptp.'N_a_b_vec_fun$'__0| |tptp.'N_a_b_vec_fun$'|) (as |@_tptp.'N_a_b_vec_fun$'__1| |tptp.'N_a_b_vec_fun$'|))))) (as |@_tptp.'A_b_vec_n_vec$'__0| |tptp.'A_b_vec_n_vec$'|) (as |@_tptp.'A_b_vec_n_vec$'__1| |tptp.'A_b_vec_n_vec$'|))) % 140.60/140.98 (define-fun |tptp.'fun_app$d'| (($x1 |tptp.'N_a_b_vec_n_vec_fun$'|) ($x2 |tptp.'N$'|)) |tptp.'A_b_vec_n_vec$'| (ite (and (= (as |@_tptp.'N_a_b_vec_n_vec_fun$'__1| |tptp.'N_a_b_vec_n_vec_fun$'|) $x1) (= (as |@_tptp.'N$'__0| |tptp.'N$'|) $x2)) (as |@_tptp.'A_b_vec_n_vec$'__0| |tptp.'A_b_vec_n_vec$'|) (as |@_tptp.'A_b_vec_n_vec$'__1| |tptp.'A_b_vec_n_vec$'|))) % 140.60/140.98 (define-fun |tptp.'row_add$a'| (($x1 |tptp.'A_n_vec_n_vec$'|) ($x2 |tptp.'N$'|) ($x3 |tptp.'N$'|) ($x4 |tptp.'A$'|)) |tptp.'A_n_vec_n_vec$'| (as |@_tptp.'A_n_vec_n_vec$'__1| |tptp.'A_n_vec_n_vec$'|)) % 140.60/140.98 (define-fun |tptp.'map_matrix$k'| ((BOUND_VARIABLE_49891 |tptp.'A_a_b_vec_fun$'|) (BOUND_VARIABLE_49893 |tptp.'A_b_vec_n_vec$'|)) |tptp.'A_b_vec_b_vec_n_vec$'| (as |@_tptp.'A_b_vec_b_vec_n_vec$'__0| |tptp.'A_b_vec_b_vec_n_vec$'|)) % 140.60/140.98 (define-fun |tptp.'vec_lambda$b'| (($x1 |tptp.'N_a_fun$'|)) |tptp.'A_n_vec$'| (ite (= (as |@_tptp.'N_a_fun$'__0| |tptp.'N_a_fun$'|) $x1) (as |@_tptp.'A_n_vec$'__0| |tptp.'A_n_vec$'|) (as |@_tptp.'A_n_vec$'__1| |tptp.'A_n_vec$'|))) % 140.60/140.98 (define-fun |tptp.'vec_nth$d'| (($x1 |tptp.'A_b_vec_b_vec$'|)) |tptp.'B_a_b_vec_fun$'| (ite (= (as |@_tptp.'A_b_vec_b_vec$'__0| |tptp.'A_b_vec_b_vec$'|) $x1) (as |@_tptp.'B_a_b_vec_fun$'__0| |tptp.'B_a_b_vec_fun$'|) (as |@_tptp.'B_a_b_vec_fun$'__1| |tptp.'B_a_b_vec_fun$'|))) % 140.60/140.98 (define-fun |tptp.'less_eq$'| () |tptp.'N_n_bool_fun_fun$'| (as |@_tptp.'N_n_bool_fun_fun$'__1| |tptp.'N_n_bool_fun_fun$'|)) % 140.60/140.98 (define-fun |tptp.'uun$'| (($x1 |tptp.'A_b_vec_n_vec$'|) ($x2 |tptp.'B$'|) ($x3 |tptp.'B$'|) ($x4 |tptp.'N$'|)) |tptp.'B_a_fun$'| (ite (and (= (as |@_tptp.'A_b_vec_n_vec$'__1| |tptp.'A_b_vec_n_vec$'|) $x1) (= (as |@_tptp.'B$'__0| |tptp.'B$'|) $x2) (= (as |@_tptp.'B$'__0| |tptp.'B$'|) $x3) (= (as |@_tptp.'N$'__0| |tptp.'N$'|) $x4)) (as |@_tptp.'B_a_fun$'__0| |tptp.'B_a_fun$'|) (as |@_tptp.'B_a_fun$'__1| |tptp.'B_a_fun$'|))) % 140.60/140.98 (define-fun |tptp.'fun_app$ab'| (($x1 |tptp.'A_bool_fun$'|) ($x2 |tptp.'A$'|)) Bool true) % 140.60/140.98 (define-fun |tptp.'fun_app$ag'| (($x1 |tptp.'N_n_fun$'|) ($x2 |tptp.'N$'|)) |tptp.'N$'| (as |@_tptp.'N$'__0| |tptp.'N$'|)) % 140.60/140.98 (define-fun |tptp.'rowvector$'| ((BOUND_VARIABLE_7231 |tptp.'A_n_vec$'|)) |tptp.'A_n_vec_n_vec$'| (ite (= (as |@_tptp.'N_a_n_vec_fun$'__0| |tptp.'N_a_n_vec_fun$'|) (ite (= BOUND_VARIABLE_7231 (as |@_tptp.'A_n_vec$'__0| |tptp.'A_n_vec$'|)) (as |@_tptp.'N_a_n_vec_fun$'__0| |tptp.'N_a_n_vec_fun$'|) (as |@_tptp.'N_a_n_vec_fun$'__1| |tptp.'N_a_n_vec_fun$'|))) (as |@_tptp.'A_n_vec_n_vec$'__0| |tptp.'A_n_vec_n_vec$'|) (as |@_tptp.'A_n_vec_n_vec$'__1| |tptp.'A_n_vec_n_vec$'|))) % 140.60/140.98 (define-fun |tptp.'thesis$'| () Bool true) % 140.60/140.98 (define-fun |tptp.'uuf$'| (($x1 |tptp.'A_b_vec$'|)) |tptp.'B_a_fun$'| (as |@_tptp.'B_a_fun$'__1| |tptp.'B_a_fun$'|)) % 140.60/140.98 (define-fun |tptp.'uuw$'| (($x1 |tptp.'A_b_vec_n_vec$'|) ($x2 |tptp.'N$'|) ($x3 |tptp.'N$'|)) |tptp.'N_a_b_vec_fun$'| (ite (and (= (as |@_tptp.'A_b_vec_n_vec$'__0| |tptp.'A_b_vec_n_vec$'|) $x1) (= (as |@_tptp.'N$'__0| |tptp.'N$'|) $x2) (= (as |@_tptp.'N$'__0| |tptp.'N$'|) $x3)) (as |@_tptp.'N_a_b_vec_fun$'__0| |tptp.'N_a_b_vec_fun$'|) (as |@_tptp.'N_a_b_vec_fun$'__1| |tptp.'N_a_b_vec_fun$'|))) % 140.60/140.98 (define-fun |tptp.'fun_app$i'| (($x1 |tptp.'B_a_n_vec_fun$'|) ($x2 |tptp.'B$'|)) |tptp.'A_n_vec$'| (ite (and (= (as |@_tptp.'B_a_n_vec_fun$'__1| |tptp.'B_a_n_vec_fun$'|) $x1) (= (as |@_tptp.'B$'__0| |tptp.'B$'|) $x2)) (as |@_tptp.'A_n_vec$'__0| |tptp.'A_n_vec$'|) (as |@_tptp.'A_n_vec$'__1| |tptp.'A_n_vec$'|))) % 140.60/140.98 (define-fun |tptp.'fun_app$af'| (($x1 |tptp.'N_a_b_vec_bool_fun_fun$'|) ($x2 |tptp.'N$'|)) |tptp.'A_b_vec_bool_fun$'| (as |@_tptp.'A_b_vec_bool_fun$'__0| |tptp.'A_b_vec_bool_fun$'|)) % 140.60/140.98 (define-fun |tptp.'uwb$'| () |tptp.'N_a_b_vec_n_vec_fun$'| (as |@_tptp.'N_a_b_vec_n_vec_fun$'__0| |tptp.'N_a_b_vec_n_vec_fun$'|)) % 140.60/140.98 (define-fun |tptp.'j$'| () |tptp.'B$'| (as |@_tptp.'B$'__0| |tptp.'B$'|)) % 140.60/140.98 (define-fun |tptp.'interchange_rows_row$'| ((BOUND_VARIABLE_6838 |tptp.'A_b_vec_n_vec_n_vec$'|) (BOUND_VARIABLE_6839 |tptp.'N$'|) (BOUND_VARIABLE_6840 |tptp.'N$'|)) |tptp.'N_a_b_vec_n_vec_fun$'| (ite (= (as |@_tptp.'A_b_vec_n_vec_n_vec$'__1| |tptp.'A_b_vec_n_vec_n_vec$'|) (ite (and (= (as |@_tptp.'N_a_b_vec_n_vec_n_vec_fun$'__1| |tptp.'N_a_b_vec_n_vec_n_vec_fun$'|) (ite (and (= BOUND_VARIABLE_6838 (as |@_tptp.'A_b_vec_n_vec_n_vec$'__1| |tptp.'A_b_vec_n_vec_n_vec$'|)) (= BOUND_VARIABLE_6839 (as |@_tptp.'N$'__0| |tptp.'N$'|))) (as |@_tptp.'N_a_b_vec_n_vec_n_vec_fun$'__0| |tptp.'N_a_b_vec_n_vec_n_vec_fun$'|) (as |@_tptp.'N_a_b_vec_n_vec_n_vec_fun$'__1| |tptp.'N_a_b_vec_n_vec_n_vec_fun$'|))) (= BOUND_VARIABLE_6840 (as |@_tptp.'N$'__0| |tptp.'N$'|))) (as |@_tptp.'A_b_vec_n_vec_n_vec$'__0| |tptp.'A_b_vec_n_vec_n_vec$'|) (as |@_tptp.'A_b_vec_n_vec_n_vec$'__1| |tptp.'A_b_vec_n_vec_n_vec$'|))) (as |@_tptp.'N_a_b_vec_n_vec_fun$'__0| |tptp.'N_a_b_vec_n_vec_fun$'|) (as |@_tptp.'N_a_b_vec_n_vec_fun$'__1| |tptp.'N_a_b_vec_n_vec_fun$'|))) % 140.60/140.98 (define-fun |tptp.'uvr$'| () |tptp.'N_a_fun$'| (as |@_tptp.'N_a_fun$'__1| |tptp.'N_a_fun$'|)) % 140.60/140.98 (define-fun |tptp.'uwk$'| (($x1 |tptp.'A_b_vec$'|)) |tptp.'N_a_b_vec_fun$'| (ite (= (as |@_tptp.'A_b_vec$'__1| |tptp.'A_b_vec$'|) $x1) (as |@_tptp.'N_a_b_vec_fun$'__0| |tptp.'N_a_b_vec_fun$'|) (as |@_tptp.'N_a_b_vec_fun$'__1| |tptp.'N_a_b_vec_fun$'|))) % 140.60/140.98 (define-fun |tptp.'uug$'| (($x1 |tptp.'A_b_vec_n_vec$'|)) |tptp.'N_a_b_vec_fun$'| (as |@_tptp.'N_a_b_vec_fun$'__0| |tptp.'N_a_b_vec_fun$'|)) % 140.60/140.98 (define-fun |tptp.'uxs$'| () |tptp.'A_b_vec_a_b_vec_fun$'| (as |@_tptp.'A_b_vec_a_b_vec_fun$'__0| |tptp.'A_b_vec_a_b_vec_fun$'|)) % 140.60/140.98 (define-fun |tptp.'uvw$'| () |tptp.'N_a_b_vec_fun$'| (as |@_tptp.'N_a_b_vec_fun$'__0| |tptp.'N_a_b_vec_fun$'|)) % 140.60/140.98 (define-fun |tptp.'fun_app$v'| (($x1 |tptp.'A_n_vec_a_b_vec_fun$'|) ($x2 |tptp.'A_n_vec$'|)) |tptp.'A_b_vec$'| (as |@_tptp.'A_b_vec$'__1| |tptp.'A_b_vec$'|)) % 140.60/140.98 (define-fun |tptp.'one$b'| () |tptp.'A_n_vec$'| (as |@_tptp.'A_n_vec$'__0| |tptp.'A_n_vec$'|)) % 140.60/140.98 (define-fun |tptp.'uwv$'| (($x1 |tptp.'A_b_vec$'|) ($x2 |tptp.'B$'|)) |tptp.'B_a_fun$'| (ite (and (= (as |@_tptp.'A_b_vec$'__0| |tptp.'A_b_vec$'|) $x1) (= (as |@_tptp.'B$'__0| |tptp.'B$'|) $x2)) (as |@_tptp.'B_a_fun$'__0| |tptp.'B_a_fun$'|) (as |@_tptp.'B_a_fun$'__1| |tptp.'B_a_fun$'|))) % 140.60/140.98 (define-fun |tptp.'vec_nth$g'| (($x1 |tptp.'A_b_vec_n_vec_n_vec_n_vec$'|) ($x2 |tptp.'N$'|)) |tptp.'A_b_vec_n_vec_n_vec$'| (ite (and (= (as |@_tptp.'A_b_vec_n_vec_n_vec_n_vec$'__1| |tptp.'A_b_vec_n_vec_n_vec_n_vec$'|) $x1) (= (as |@_tptp.'N$'__0| |tptp.'N$'|) $x2)) (as |@_tptp.'A_b_vec_n_vec_n_vec$'__0| |tptp.'A_b_vec_n_vec_n_vec$'|) (as |@_tptp.'A_b_vec_n_vec_n_vec$'__1| |tptp.'A_b_vec_n_vec_n_vec$'|))) % 140.60/140.98 (define-fun |tptp.'times$c'| (($x1 |tptp.'A$'|)) |tptp.'A_a_fun$'| (ite (= (as |@_tptp.'A$'__1| |tptp.'A$'|) $x1) (as |@_tptp.'A_a_fun$'__0| |tptp.'A_a_fun$'|) (as |@_tptp.'A_a_fun$'__1| |tptp.'A_a_fun$'|))) % 140.60/140.98 (define-fun |tptp.'fun_app$'| (($x1 |tptp.'N_bool_fun$'|) ($x2 |tptp.'N$'|)) Bool (and (= (as |@_tptp.'N_bool_fun$'__1| |tptp.'N_bool_fun$'|) $x1) (= (as |@_tptp.'N$'__0| |tptp.'N$'|) $x2))) % 140.60/140.98 (define-fun |tptp.'uxi$'| (($x1 |tptp.'A_b_vec_n_vec$'|) ($x2 |tptp.'N$'|) ($x3 |tptp.'A$'|)) |tptp.'N_a_b_vec_fun$'| (ite (and (= (as |@_tptp.'A_b_vec_n_vec$'__0| |tptp.'A_b_vec_n_vec$'|) $x1) (= (as |@_tptp.'N$'__0| |tptp.'N$'|) $x2) (= (as |@_tptp.'A$'__1| |tptp.'A$'|) $x3)) (as |@_tptp.'N_a_b_vec_fun$'__0| |tptp.'N_a_b_vec_fun$'|) (ite (and (= (as |@_tptp.'A_b_vec_n_vec$'__0| |tptp.'A_b_vec_n_vec$'|) $x1) (= (as |@_tptp.'N$'__0| |tptp.'N$'|) $x2) (= (as |@_tptp.'A$'__0| |tptp.'A$'|) $x3)) (as |@_tptp.'N_a_b_vec_fun$'__0| |tptp.'N_a_b_vec_fun$'|) (ite (and (= (as |@_tptp.'A_b_vec_n_vec$'__1| |tptp.'A_b_vec_n_vec$'|) $x1) (= (as |@_tptp.'N$'__0| |tptp.'N$'|) $x2) (= (as |@_tptp.'A$'__0| |tptp.'A$'|) $x3)) (as |@_tptp.'N_a_b_vec_fun$'__0| |tptp.'N_a_b_vec_fun$'|) (as |@_tptp.'N_a_b_vec_fun$'__1| |tptp.'N_a_b_vec_fun$'|))))) % 140.60/140.98 (define-fun |tptp.'map_matrix$b'| ((BOUND_VARIABLE_49947 |tptp.'A_a_b_vec_fun$'|) (BOUND_VARIABLE_49949 |tptp.'A_n_vec_n_vec$'|)) |tptp.'A_b_vec_n_vec_n_vec$'| (as |@_tptp.'A_b_vec_n_vec_n_vec$'__1| |tptp.'A_b_vec_n_vec_n_vec$'|)) % 140.60/140.98 (define-fun |tptp.'uu$'| () |tptp.'N_bool_fun$'| (as |@_tptp.'N_bool_fun$'__1| |tptp.'N_bool_fun$'|)) % 140.60/140.98 (define-fun |tptp.'times$'| (($x1 |tptp.'A_b_vec_n_vec$'|)) |tptp.'A_b_vec_n_vec_a_b_vec_n_vec_fun$'| (ite (= (as |@_tptp.'A_b_vec_n_vec$'__0| |tptp.'A_b_vec_n_vec$'|) $x1) (as |@_tptp.'A_b_vec_n_vec_a_b_vec_n_vec_fun$'__0| |tptp.'A_b_vec_n_vec_a_b_vec_n_vec_fun$'|) (as |@_tptp.'A_b_vec_n_vec_a_b_vec_n_vec_fun$'__1| |tptp.'A_b_vec_n_vec_a_b_vec_n_vec_fun$'|))) % 140.60/140.98 (define-fun |tptp.'fun_app$t'| (($x1 |tptp.'A_a_b_vec_fun$'|) ($x2 |tptp.'A$'|)) |tptp.'A_b_vec$'| (as |@_tptp.'A_b_vec$'__0| |tptp.'A_b_vec$'|)) % 140.60/140.98 (define-fun |tptp.'uwx$'| (($x1 |tptp.'A_b_vec_n_vec$'|) ($x2 |tptp.'N$'|)) |tptp.'N_a_b_vec_fun$'| (ite (and (= (as |@_tptp.'A_b_vec_n_vec$'__0| |tptp.'A_b_vec_n_vec$'|) $x1) (= (as |@_tptp.'N$'__0| |tptp.'N$'|) $x2)) (as |@_tptp.'N_a_b_vec_fun$'__0| |tptp.'N_a_b_vec_fun$'|) (as |@_tptp.'N_a_b_vec_fun$'__1| |tptp.'N_a_b_vec_fun$'|))) % 140.60/140.98 (define-fun |tptp.'vec_lambda$g'| ((_arg_1 |tptp.'N_a_b_vec_b_vec_fun$'|)) |tptp.'A_b_vec_b_vec_n_vec$'| (as |@_tptp.'A_b_vec_b_vec_n_vec$'__0| |tptp.'A_b_vec_b_vec_n_vec$'|)) % 140.60/140.98 (define-fun |tptp.'interchange_rows$b'| (($x1 |tptp.'A_b_vec_n_vec_n_vec$'|) ($x2 |tptp.'N$'|)) |tptp.'N_a_b_vec_n_vec_n_vec_fun$'| (ite (and (= (as |@_tptp.'A_b_vec_n_vec_n_vec$'__1| |tptp.'A_b_vec_n_vec_n_vec$'|) $x1) (= (as |@_tptp.'N$'__0| |tptp.'N$'|) $x2)) (as |@_tptp.'N_a_b_vec_n_vec_n_vec_fun$'__0| |tptp.'N_a_b_vec_n_vec_n_vec_fun$'|) (as |@_tptp.'N_a_b_vec_n_vec_n_vec_fun$'__1| |tptp.'N_a_b_vec_n_vec_n_vec_fun$'|))) % 140.60/140.98 (define-fun |tptp.'fun_app$s'| (($x1 |tptp.'A_a_n_vec_fun$'|) ($x2 |tptp.'A$'|)) |tptp.'A_n_vec$'| (as |@_tptp.'A_n_vec$'__0| |tptp.'A_n_vec$'|)) % 140.60/140.98 (define-fun |tptp.'divide$'| (($x1 |tptp.'A$'|)) |tptp.'A_a_fun$'| (as |@_tptp.'A_a_fun$'__0| |tptp.'A_a_fun$'|)) % 140.60/140.98 (define-fun |tptp.'uxy$'| () |tptp.'A_a_fun$'| (as |@_tptp.'A_a_fun$'__0| |tptp.'A_a_fun$'|)) % 140.60/140.98 (define-fun |tptp.'columnvector$a'| ((BOUND_VARIABLE_49966 |tptp.'A_b_vec$'|)) |tptp.'A_n_vec_b_vec$'| (as |@_tptp.'A_n_vec_b_vec$'__0| |tptp.'A_n_vec_b_vec$'|)) % 140.60/140.98 (define-fun |tptp.'fun_app$m'| (($x1 |tptp.'A_a_fun$'|) ($x2 |tptp.'A$'|)) |tptp.'A$'| (ite (and (= (as |@_tptp.'A_a_fun$'__0| |tptp.'A_a_fun$'|) $x1) (= (as |@_tptp.'A$'__0| |tptp.'A$'|) $x2)) (as |@_tptp.'A$'__0| |tptp.'A$'|) (ite (and (= (as |@_tptp.'A_a_fun$'__1| |tptp.'A_a_fun$'|) $x1) (= (as |@_tptp.'A$'__0| |tptp.'A$'|) $x2)) (as |@_tptp.'A$'__0| |tptp.'A$'|) (ite (and (= (as |@_tptp.'A_a_fun$'__1| |tptp.'A_a_fun$'|) $x1) (= (as |@_tptp.'A$'__1| |tptp.'A$'|) $x2)) (as |@_tptp.'A$'__0| |tptp.'A$'|) (as |@_tptp.'A$'__1| |tptp.'A$'|))))) % 140.60/140.98 (define-fun |tptp.'uvd$'| (($x1 |tptp.'A_a_fun$'|) ($x2 |tptp.'A_n_vec_n_vec$'|) ($x3 |tptp.'N$'|)) |tptp.'N_a_fun$'| (ite (and (= (as |@_tptp.'A_a_fun$'__0| |tptp.'A_a_fun$'|) $x1) (= (as |@_tptp.'A_n_vec_n_vec$'__0| |tptp.'A_n_vec_n_vec$'|) $x2) (= (as |@_tptp.'N$'__0| |tptp.'N$'|) $x3)) (as |@_tptp.'N_a_fun$'__0| |tptp.'N_a_fun$'|) (as |@_tptp.'N_a_fun$'__1| |tptp.'N_a_fun$'|))) % 140.60/140.98 (define-fun |tptp.'uwz$'| (($x1 |tptp.'A_n_vec$'|) ($x2 |tptp.'N$'|)) |tptp.'B_a_fun$'| (ite (and (= (as |@_tptp.'A_n_vec$'__0| |tptp.'A_n_vec$'|) $x1) (= (as |@_tptp.'N$'__0| |tptp.'N$'|) $x2)) (as |@_tptp.'B_a_fun$'__0| |tptp.'B_a_fun$'|) (as |@_tptp.'B_a_fun$'__1| |tptp.'B_a_fun$'|))) % 140.60/140.98 (define-fun |tptp.'uwd$'| (($x1 |tptp.'A_n_vec_n_vec$'|) ($x2 |tptp.'N$'|)) |tptp.'N_n_bool_fun_fun$'| (ite (and (= (as |@_tptp.'A_n_vec_n_vec$'__1| |tptp.'A_n_vec_n_vec$'|) $x1) (= (as |@_tptp.'N$'__0| |tptp.'N$'|) $x2)) (as |@_tptp.'N_n_bool_fun_fun$'__0| |tptp.'N_n_bool_fun_fun$'|) (as |@_tptp.'N_n_bool_fun_fun$'__1| |tptp.'N_n_bool_fun_fun$'|))) % 140.60/140.98 (define-fun |tptp.'interchange_rows_row$a'| ((BOUND_VARIABLE_6853 |tptp.'A_n_vec_n_vec$'|) (BOUND_VARIABLE_6854 |tptp.'N$'|) (BOUND_VARIABLE_6855 |tptp.'N$'|)) |tptp.'N_a_n_vec_fun$'| (ite (= (as |@_tptp.'A_n_vec_n_vec$'__0| |tptp.'A_n_vec_n_vec$'|) (ite (and (= (as |@_tptp.'N_a_n_vec_n_vec_fun$'__0| |tptp.'N_a_n_vec_n_vec_fun$'|) (ite (and (= BOUND_VARIABLE_6853 (as |@_tptp.'A_n_vec_n_vec$'__0| |tptp.'A_n_vec_n_vec$'|)) (= BOUND_VARIABLE_6854 (as |@_tptp.'N$'__0| |tptp.'N$'|))) (as |@_tptp.'N_a_n_vec_n_vec_fun$'__0| |tptp.'N_a_n_vec_n_vec_fun$'|) (as |@_tptp.'N_a_n_vec_n_vec_fun$'__1| |tptp.'N_a_n_vec_n_vec_fun$'|))) (= BOUND_VARIABLE_6855 (as |@_tptp.'N$'__0| |tptp.'N$'|))) (as |@_tptp.'A_n_vec_n_vec$'__0| |tptp.'A_n_vec_n_vec$'|) (as |@_tptp.'A_n_vec_n_vec$'__1| |tptp.'A_n_vec_n_vec$'|))) (as |@_tptp.'N_a_n_vec_fun$'__0| |tptp.'N_a_n_vec_fun$'|) (as |@_tptp.'N_a_n_vec_fun$'__1| |tptp.'N_a_n_vec_fun$'|))) % 140.60/140.98 (define-fun |tptp.'times$a'| (($x1 |tptp.'A_n_vec$'|)) |tptp.'A_n_vec_a_n_vec_fun$'| (ite (= (as |@_tptp.'A_n_vec$'__0| |tptp.'A_n_vec$'|) $x1) (as |@_tptp.'A_n_vec_a_n_vec_fun$'__0| |tptp.'A_n_vec_a_n_vec_fun$'|) (as |@_tptp.'A_n_vec_a_n_vec_fun$'__1| |tptp.'A_n_vec_a_n_vec_fun$'|))) % 140.60/140.98 (define-fun |tptp.'uur$'| (($x1 |tptp.'A_b_vec_b_vec$'|) ($x2 |tptp.'B$'|) ($x3 |tptp.'B$'|) ($x4 |tptp.'B$'|)) |tptp.'B_a_fun$'| (ite (and (= (as |@_tptp.'A_b_vec_b_vec$'__0| |tptp.'A_b_vec_b_vec$'|) $x1) (= (as |@_tptp.'B$'__0| |tptp.'B$'|) $x2) (= (as |@_tptp.'B$'__0| |tptp.'B$'|) $x3) (= (as |@_tptp.'B$'__0| |tptp.'B$'|) $x4)) (as |@_tptp.'B_a_fun$'__0| |tptp.'B_a_fun$'|) (as |@_tptp.'B_a_fun$'__1| |tptp.'B_a_fun$'|))) % 140.60/140.98 (define-fun |tptp.'uuz$'| (($x1 |tptp.'A_a_b_vec_fun$'|) ($x2 |tptp.'A_n_vec_n_vec$'|) ($x3 |tptp.'N$'|)) |tptp.'N_a_b_vec_fun$'| (as |@_tptp.'N_a_b_vec_fun$'__1| |tptp.'N_a_b_vec_fun$'|)) % 140.60/140.98 (define-fun |tptp.'fun_app$x'| (($x1 |tptp.'A_b_vec_n_vec_bool_fun$'|) ($x2 |tptp.'A_b_vec_n_vec$'|)) Bool true) % 140.60/140.98 (define-fun |tptp.'uwr$'| (($x1 |tptp.'A_b_vec_n_vec$'|) ($x2 |tptp.'N$'|)) |tptp.'B_a_b_vec_fun$'| (ite (and (= (as |@_tptp.'A_b_vec_n_vec$'__1| |tptp.'A_b_vec_n_vec$'|) $x1) (= (as |@_tptp.'N$'__0| |tptp.'N$'|) $x2)) (as |@_tptp.'B_a_b_vec_fun$'__0| |tptp.'B_a_b_vec_fun$'|) (as |@_tptp.'B_a_b_vec_fun$'__1| |tptp.'B_a_b_vec_fun$'|))) % 140.60/140.98 (define-fun |tptp.'interchange_columns$c'| ((BOUND_VARIABLE_6979 |tptp.'A_b_vec_b_vec$'|) (BOUND_VARIABLE_6980 |tptp.'B$'|) (BOUND_VARIABLE_6981 |tptp.'B$'|)) |tptp.'A_b_vec_b_vec$'| (ite (= (as |@_tptp.'B_a_b_vec_fun$'__0| |tptp.'B_a_b_vec_fun$'|) (ite (and (= BOUND_VARIABLE_6979 (as |@_tptp.'A_b_vec_b_vec$'__0| |tptp.'A_b_vec_b_vec$'|)) (= BOUND_VARIABLE_6980 (as |@_tptp.'B$'__0| |tptp.'B$'|)) (= BOUND_VARIABLE_6981 (as |@_tptp.'B$'__0| |tptp.'B$'|))) (as |@_tptp.'B_a_b_vec_fun$'__0| |tptp.'B_a_b_vec_fun$'|) (as |@_tptp.'B_a_b_vec_fun$'__1| |tptp.'B_a_b_vec_fun$'|))) (as |@_tptp.'A_b_vec_b_vec$'__0| |tptp.'A_b_vec_b_vec$'|) (as |@_tptp.'A_b_vec_b_vec$'__1| |tptp.'A_b_vec_b_vec$'|))) % 140.60/140.98 (define-fun |tptp.'uvt$'| () |tptp.'B_a_b_vec_fun$'| (as |@_tptp.'B_a_b_vec_fun$'__1| |tptp.'B_a_b_vec_fun$'|)) % 140.60/140.98 (define-fun |tptp.'uuu$'| (($x1 |tptp.'A_b_vec_n_vec_n_vec$'|) ($x2 |tptp.'N$'|) ($x3 |tptp.'N$'|)) |tptp.'N_a_b_vec_n_vec_fun$'| (ite (and (= (as |@_tptp.'A_b_vec_n_vec_n_vec$'__1| |tptp.'A_b_vec_n_vec_n_vec$'|) $x1) (= (as |@_tptp.'N$'__0| |tptp.'N$'|) $x2) (= (as |@_tptp.'N$'__0| |tptp.'N$'|) $x3)) (as |@_tptp.'N_a_b_vec_n_vec_fun$'__0| |tptp.'N_a_b_vec_n_vec_fun$'|) (as |@_tptp.'N_a_b_vec_n_vec_fun$'__1| |tptp.'N_a_b_vec_n_vec_fun$'|))) % 140.60/140.98 (define-fun |tptp.'row_add_row$a'| ((BOUND_VARIABLE_50042 |tptp.'A_n_vec_n_vec$'|) (BOUND_VARIABLE_50044 |tptp.'N$'|) (BOUND_VARIABLE_50046 |tptp.'N$'|) (BOUND_VARIABLE_50048 |tptp.'A$'|)) |tptp.'N_a_n_vec_fun$'| (as |@_tptp.'N_a_n_vec_fun$'__1| |tptp.'N_a_n_vec_fun$'|)) % 140.60/140.98 (define-fun |tptp.'uvs$'| () |tptp.'N_a_n_vec_fun$'| (as |@_tptp.'N_a_n_vec_fun$'__1| |tptp.'N_a_n_vec_fun$'|)) % 140.60/140.98 (define-fun |tptp.'fun_app$u'| (($x1 |tptp.'A_b_vec_n_vec_n_vec_a_b_vec_n_vec_n_vec_fun$'|) ($x2 |tptp.'A_b_vec_n_vec_n_vec$'|)) |tptp.'A_b_vec_n_vec_n_vec$'| (ite (and (= (as |@_tptp.'A_b_vec_n_vec_n_vec_a_b_vec_n_vec_n_vec_fun$'__1| |tptp.'A_b_vec_n_vec_n_vec_a_b_vec_n_vec_n_vec_fun$'|) $x1) (= (as |@_tptp.'A_b_vec_n_vec_n_vec$'__1| |tptp.'A_b_vec_n_vec_n_vec$'|) $x2)) (as |@_tptp.'A_b_vec_n_vec_n_vec$'__0| |tptp.'A_b_vec_n_vec_n_vec$'|) (ite (and (= (as |@_tptp.'A_b_vec_n_vec_n_vec_a_b_vec_n_vec_n_vec_fun$'__0| |tptp.'A_b_vec_n_vec_n_vec_a_b_vec_n_vec_n_vec_fun$'|) $x1) (= (as |@_tptp.'A_b_vec_n_vec_n_vec$'__0| |tptp.'A_b_vec_n_vec_n_vec$'|) $x2)) (as |@_tptp.'A_b_vec_n_vec_n_vec$'__0| |tptp.'A_b_vec_n_vec_n_vec$'|) (ite (and (= (as |@_tptp.'A_b_vec_n_vec_n_vec_a_b_vec_n_vec_n_vec_fun$'__1| |tptp.'A_b_vec_n_vec_n_vec_a_b_vec_n_vec_n_vec_fun$'|) $x1) (= (as |@_tptp.'A_b_vec_n_vec_n_vec$'__0| |tptp.'A_b_vec_n_vec_n_vec$'|) $x2)) (as |@_tptp.'A_b_vec_n_vec_n_vec$'__0| |tptp.'A_b_vec_n_vec_n_vec$'|) (as |@_tptp.'A_b_vec_n_vec_n_vec$'__1| |tptp.'A_b_vec_n_vec_n_vec$'|))))) % 140.60/140.98 (define-fun |tptp.'uxd$'| (($x1 |tptp.'A_b_vec_b_vec$'|) ($x2 |tptp.'B$'|) ($x3 |tptp.'A$'|) ($x4 |tptp.'B$'|)) |tptp.'B_a_fun$'| (ite (and (= (as |@_tptp.'A_b_vec_b_vec$'__0| |tptp.'A_b_vec_b_vec$'|) $x1) (= (as |@_tptp.'B$'__0| |tptp.'B$'|) $x2) (= (as |@_tptp.'A$'__1| |tptp.'A$'|) $x3) (= (as |@_tptp.'B$'__0| |tptp.'B$'|) $x4)) (as |@_tptp.'B_a_fun$'__0| |tptp.'B_a_fun$'|) (as |@_tptp.'B_a_fun$'__1| |tptp.'B_a_fun$'|))) % 140.60/140.98 (define-fun |tptp.'uvc$'| (($x1 |tptp.'A_b_vec_a_b_vec_fun$'|) ($x2 |tptp.'A_b_vec_n_vec_n_vec$'|)) |tptp.'N_a_b_vec_n_vec_fun$'| (ite (and (= (as |@_tptp.'A_b_vec_a_b_vec_fun$'__1| |tptp.'A_b_vec_a_b_vec_fun$'|) $x1) (= (as |@_tptp.'A_b_vec_n_vec_n_vec$'__1| |tptp.'A_b_vec_n_vec_n_vec$'|) $x2)) (as |@_tptp.'N_a_b_vec_n_vec_fun$'__0| |tptp.'N_a_b_vec_n_vec_fun$'|) (as |@_tptp.'N_a_b_vec_n_vec_fun$'__1| |tptp.'N_a_b_vec_n_vec_fun$'|))) % 140.60/140.98 (define-fun |tptp.'uws$'| (($x1 |tptp.'A_b_vec_n_vec$'|)) |tptp.'N_a_b_vec_b_vec_fun$'| (ite (= (as |@_tptp.'A_b_vec_n_vec$'__1| |tptp.'A_b_vec_n_vec$'|) $x1) (as |@_tptp.'N_a_b_vec_b_vec_fun$'__0| |tptp.'N_a_b_vec_b_vec_fun$'|) (as |@_tptp.'N_a_b_vec_b_vec_fun$'__1| |tptp.'N_a_b_vec_b_vec_fun$'|))) % 140.60/140.98 (define-fun |tptp.'fun_app$n'| (($x1 |tptp.'A_a_b_vec_n_vec_fun$'|) ($x2 |tptp.'A$'|)) |tptp.'A_b_vec_n_vec$'| (ite (and (= (as |@_tptp.'A_a_b_vec_n_vec_fun$'__1| |tptp.'A_a_b_vec_n_vec_fun$'|) $x1) (= (as |@_tptp.'A$'__1| |tptp.'A$'|) $x2)) (as |@_tptp.'A_b_vec_n_vec$'__0| |tptp.'A_b_vec_n_vec$'|) (ite (and (= (as |@_tptp.'A_a_b_vec_n_vec_fun$'__1| |tptp.'A_a_b_vec_n_vec_fun$'|) $x1) (= (as |@_tptp.'A$'__0| |tptp.'A$'|) $x2)) (as |@_tptp.'A_b_vec_n_vec$'__0| |tptp.'A_b_vec_n_vec$'|) (ite (and (= (as |@_tptp.'A_a_b_vec_n_vec_fun$'__0| |tptp.'A_a_b_vec_n_vec_fun$'|) $x1) (= (as |@_tptp.'A$'__0| |tptp.'A$'|) $x2)) (as |@_tptp.'A_b_vec_n_vec$'__0| |tptp.'A_b_vec_n_vec$'|) (as |@_tptp.'A_b_vec_n_vec$'__1| |tptp.'A_b_vec_n_vec$'|))))) % 140.60/140.98 (define-fun |tptp.'rowvector$c'| ((BOUND_VARIABLE_7258 |tptp.'A_b_vec$'|)) |tptp.'A_b_vec_n_vec$'| (ite (= (as |@_tptp.'N_a_b_vec_fun$'__0| |tptp.'N_a_b_vec_fun$'|) (ite (= BOUND_VARIABLE_7258 (as |@_tptp.'A_b_vec$'__1| |tptp.'A_b_vec$'|)) (as |@_tptp.'N_a_b_vec_fun$'__0| |tptp.'N_a_b_vec_fun$'|) (as |@_tptp.'N_a_b_vec_fun$'__1| |tptp.'N_a_b_vec_fun$'|))) (as |@_tptp.'A_b_vec_n_vec$'__0| |tptp.'A_b_vec_n_vec$'|) (as |@_tptp.'A_b_vec_n_vec$'__1| |tptp.'A_b_vec_n_vec$'|))) % 140.60/140.98 (define-fun |tptp.'fun_app$e'| (($x1 |tptp.'B_a_b_vec_fun$'|) ($x2 |tptp.'B$'|)) |tptp.'A_b_vec$'| (ite (and (= (as |@_tptp.'B_a_b_vec_fun$'__0| |tptp.'B_a_b_vec_fun$'|) $x1) (= (as |@_tptp.'B$'__0| |tptp.'B$'|) $x2)) (as |@_tptp.'A_b_vec$'__0| |tptp.'A_b_vec$'|) (as |@_tptp.'A_b_vec$'__1| |tptp.'A_b_vec$'|))) % 140.60/140.98 (define-fun |tptp.'mult_row$c'| ((BOUND_VARIABLE_7401 |tptp.'A_b_vec_b_vec$'|) (BOUND_VARIABLE_7402 |tptp.'B$'|) (BOUND_VARIABLE_7403 |tptp.'A$'|)) |tptp.'A_b_vec_b_vec$'| (ite (= (as |@_tptp.'B_a_b_vec_fun$'__0| |tptp.'B_a_b_vec_fun$'|) (ite (and (= BOUND_VARIABLE_7401 (as |@_tptp.'A_b_vec_b_vec$'__0| |tptp.'A_b_vec_b_vec$'|)) (= BOUND_VARIABLE_7402 (as |@_tptp.'B$'__0| |tptp.'B$'|)) (= BOUND_VARIABLE_7403 (as |@_tptp.'A$'__1| |tptp.'A$'|))) (as |@_tptp.'B_a_b_vec_fun$'__0| |tptp.'B_a_b_vec_fun$'|) (as |@_tptp.'B_a_b_vec_fun$'__1| |tptp.'B_a_b_vec_fun$'|))) (as |@_tptp.'A_b_vec_b_vec$'__0| |tptp.'A_b_vec_b_vec$'|) (as |@_tptp.'A_b_vec_b_vec$'__1| |tptp.'A_b_vec_b_vec$'|))) % 140.60/140.98 (define-fun |tptp.'gauss_Jordan_in_ij$'| ((BOUND_VARIABLE_7154 |tptp.'A_b_vec_n_vec$'|) (BOUND_VARIABLE_7155 |tptp.'N$'|) (BOUND_VARIABLE_7156 |tptp.'B$'|)) |tptp.'A_b_vec_n_vec$'| (ite (= (as |@_tptp.'N_a_b_vec_fun$'__0| |tptp.'N_a_b_vec_fun$'|) (ite (and (= BOUND_VARIABLE_7154 (as |@_tptp.'A_b_vec_n_vec$'__0| |tptp.'A_b_vec_n_vec$'|)) (= BOUND_VARIABLE_7155 (as |@_tptp.'N$'__0| |tptp.'N$'|)) (= BOUND_VARIABLE_7156 (as |@_tptp.'B$'__0| |tptp.'B$'|))) (as |@_tptp.'N_a_b_vec_fun$'__0| |tptp.'N_a_b_vec_fun$'|) (as |@_tptp.'N_a_b_vec_fun$'__1| |tptp.'N_a_b_vec_fun$'|))) (as |@_tptp.'A_b_vec_n_vec$'__0| |tptp.'A_b_vec_n_vec$'|) (as |@_tptp.'A_b_vec_n_vec$'__1| |tptp.'A_b_vec_n_vec$'|))) % 140.60/140.98 (define-fun |tptp.'columnvector$d'| ((BOUND_VARIABLE_7303 |tptp.'A_n_vec$'|)) |tptp.'A_n_vec_n_vec$'| (ite (= (as |@_tptp.'N_a_n_vec_fun$'__0| |tptp.'N_a_n_vec_fun$'|) (ite (= BOUND_VARIABLE_7303 (as |@_tptp.'A_n_vec$'__0| |tptp.'A_n_vec$'|)) (as |@_tptp.'N_a_n_vec_fun$'__0| |tptp.'N_a_n_vec_fun$'|) (as |@_tptp.'N_a_n_vec_fun$'__1| |tptp.'N_a_n_vec_fun$'|))) (as |@_tptp.'A_n_vec_n_vec$'__0| |tptp.'A_n_vec_n_vec$'|) (as |@_tptp.'A_n_vec_n_vec$'__1| |tptp.'A_n_vec_n_vec$'|))) % 140.60/140.98 (define-fun |tptp.'times$f'| ((BOUND_VARIABLE_7541 |tptp.'A_b_vec_b_vec$'|) (BOUND_VARIABLE_7542 |tptp.'A_b_vec_b_vec$'|)) |tptp.'A_b_vec_b_vec$'| (ite (= (as |@_tptp.'B_a_b_vec_fun$'__0| |tptp.'B_a_b_vec_fun$'|) (ite (and (= BOUND_VARIABLE_7541 (as |@_tptp.'A_b_vec_b_vec$'__0| |tptp.'A_b_vec_b_vec$'|)) (= BOUND_VARIABLE_7542 (as |@_tptp.'A_b_vec_b_vec$'__0| |tptp.'A_b_vec_b_vec$'|))) (as |@_tptp.'B_a_b_vec_fun$'__0| |tptp.'B_a_b_vec_fun$'|) (as |@_tptp.'B_a_b_vec_fun$'__1| |tptp.'B_a_b_vec_fun$'|))) (as |@_tptp.'A_b_vec_b_vec$'__0| |tptp.'A_b_vec_b_vec$'|) (as |@_tptp.'A_b_vec_b_vec$'__1| |tptp.'A_b_vec_b_vec$'|))) % 140.60/140.98 (define-fun |tptp.'row_add$'| (($x1 |tptp.'A_b_vec_n_vec$'|) ($x2 |tptp.'N$'|) ($x3 |tptp.'N$'|)) |tptp.'A_a_b_vec_n_vec_fun$'| (as |@_tptp.'A_a_b_vec_n_vec_fun$'__0| |tptp.'A_a_b_vec_n_vec_fun$'|)) % 140.60/140.98 (define-fun |tptp.'uxe$'| (($x1 |tptp.'A_b_vec_b_vec$'|) ($x2 |tptp.'B$'|) ($x3 |tptp.'A$'|)) |tptp.'B_a_b_vec_fun$'| (ite (and (= (as |@_tptp.'A_b_vec_b_vec$'__0| |tptp.'A_b_vec_b_vec$'|) $x1) (= (as |@_tptp.'B$'__0| |tptp.'B$'|) $x2) (= (as |@_tptp.'A$'__1| |tptp.'A$'|) $x3)) (as |@_tptp.'B_a_b_vec_fun$'__0| |tptp.'B_a_b_vec_fun$'|) (as |@_tptp.'B_a_b_vec_fun$'__1| |tptp.'B_a_b_vec_fun$'|))) % 140.60/140.98 (define-fun |tptp.'fun_app$l'| (($x1 |tptp.'N_a_fun$'|) ($x2 |tptp.'N$'|)) |tptp.'A$'| (ite (and (= (as |@_tptp.'N_a_fun$'__1| |tptp.'N_a_fun$'|) $x1) (= (as |@_tptp.'N$'__0| |tptp.'N$'|) $x2)) (as |@_tptp.'A$'__0| |tptp.'A$'|) (as |@_tptp.'A$'__1| |tptp.'A$'|))) % 140.60/140.98 (define-fun |tptp.'uminus$d'| ((BOUND_VARIABLE_50137 |tptp.'A_b_vec_n_vec_n_vec$'|)) |tptp.'A_b_vec_n_vec_n_vec$'| (as |@_tptp.'A_b_vec_n_vec_n_vec$'__0| |tptp.'A_b_vec_n_vec_n_vec$'|)) % 140.60/140.98 (define-fun |tptp.'one$a'| () |tptp.'A_b_vec_n_vec$'| (as |@_tptp.'A_b_vec_n_vec$'__1| |tptp.'A_b_vec_n_vec$'|)) % 140.60/140.98 (define-fun |tptp.'uxc$'| (($x1 |tptp.'A_n_vec_n_vec$'|) ($x2 |tptp.'N$'|) ($x3 |tptp.'A$'|)) |tptp.'N_a_n_vec_fun$'| (ite (and (= (as |@_tptp.'A_n_vec_n_vec$'__0| |tptp.'A_n_vec_n_vec$'|) $x1) (= (as |@_tptp.'N$'__0| |tptp.'N$'|) $x2) (= (as |@_tptp.'A$'__1| |tptp.'A$'|) $x3)) (as |@_tptp.'N_a_n_vec_fun$'__0| |tptp.'N_a_n_vec_fun$'|) (as |@_tptp.'N_a_n_vec_fun$'__1| |tptp.'N_a_n_vec_fun$'|))) % 140.60/140.98 (define-fun |tptp.'mult_row_row$a'| ((BOUND_VARIABLE_6809 |tptp.'A_n_vec_n_vec$'|) (BOUND_VARIABLE_6810 |tptp.'N$'|) (BOUND_VARIABLE_6811 |tptp.'A$'|)) |tptp.'N_a_n_vec_fun$'| (ite (= (as |@_tptp.'A_n_vec_n_vec$'__0| |tptp.'A_n_vec_n_vec$'|) (ite (= (as |@_tptp.'N_a_n_vec_fun$'__0| |tptp.'N_a_n_vec_fun$'|) (ite (and (= BOUND_VARIABLE_6809 (as |@_tptp.'A_n_vec_n_vec$'__0| |tptp.'A_n_vec_n_vec$'|)) (= BOUND_VARIABLE_6810 (as |@_tptp.'N$'__0| |tptp.'N$'|)) (= BOUND_VARIABLE_6811 (as |@_tptp.'A$'__1| |tptp.'A$'|))) (as |@_tptp.'N_a_n_vec_fun$'__0| |tptp.'N_a_n_vec_fun$'|) (as |@_tptp.'N_a_n_vec_fun$'__1| |tptp.'N_a_n_vec_fun$'|))) (as |@_tptp.'A_n_vec_n_vec$'__0| |tptp.'A_n_vec_n_vec$'|) (as |@_tptp.'A_n_vec_n_vec$'__1| |tptp.'A_n_vec_n_vec$'|))) (as |@_tptp.'N_a_n_vec_fun$'__0| |tptp.'N_a_n_vec_fun$'|) (as |@_tptp.'N_a_n_vec_fun$'__1| |tptp.'N_a_n_vec_fun$'|))) % 140.60/140.98 (define-fun |tptp.'uxv$'| () |tptp.'A_b_vec_n_vec_n_vec_a_b_vec_n_vec_n_vec_fun$'| (as |@_tptp.'A_b_vec_n_vec_n_vec_a_b_vec_n_vec_n_vec_fun$'__0| |tptp.'A_b_vec_n_vec_n_vec_a_b_vec_n_vec_n_vec_fun$'|)) % 140.60/140.98 (define-fun |tptp.'interchange_columns_row$a'| ((BOUND_VARIABLE_6882 |tptp.'A_n_vec_n_vec$'|) (BOUND_VARIABLE_6883 |tptp.'N$'|) (BOUND_VARIABLE_6884 |tptp.'N$'|)) |tptp.'N_a_n_vec_fun$'| (ite (= (as |@_tptp.'A_n_vec_n_vec$'__0| |tptp.'A_n_vec_n_vec$'|) (ite (= (as |@_tptp.'N_a_n_vec_fun$'__0| |tptp.'N_a_n_vec_fun$'|) (ite (and (= BOUND_VARIABLE_6882 (as |@_tptp.'A_n_vec_n_vec$'__0| |tptp.'A_n_vec_n_vec$'|)) (= BOUND_VARIABLE_6883 (as |@_tptp.'N$'__0| |tptp.'N$'|)) (= BOUND_VARIABLE_6884 (as |@_tptp.'N$'__0| |tptp.'N$'|))) (as |@_tptp.'N_a_n_vec_fun$'__0| |tptp.'N_a_n_vec_fun$'|) (as |@_tptp.'N_a_n_vec_fun$'__1| |tptp.'N_a_n_vec_fun$'|))) (as |@_tptp.'A_n_vec_n_vec$'__0| |tptp.'A_n_vec_n_vec$'|) (as |@_tptp.'A_n_vec_n_vec$'__1| |tptp.'A_n_vec_n_vec$'|))) (as |@_tptp.'N_a_n_vec_fun$'__0| |tptp.'N_a_n_vec_fun$'|) (as |@_tptp.'N_a_n_vec_fun$'__1| |tptp.'N_a_n_vec_fun$'|))) % 140.60/140.98 (define-fun |tptp.'row_add$b'| ((_arg_1 |tptp.'A_b_vec_n_vec_n_vec$'|) (_arg_2 |tptp.'N$'|) (_arg_3 |tptp.'N$'|) (_arg_4 |tptp.'A_b_vec$'|)) |tptp.'A_b_vec_n_vec_n_vec$'| (as |@_tptp.'A_b_vec_n_vec_n_vec$'__0| |tptp.'A_b_vec_n_vec_n_vec$'|)) % 140.60/140.98 (define-fun |tptp.'uvf$'| (($x1 |tptp.'A_a_fun$'|) ($x2 |tptp.'A_b_vec_b_vec$'|) ($x3 |tptp.'B$'|)) |tptp.'B_a_fun$'| (ite (and (= (as |@_tptp.'A_a_fun$'__0| |tptp.'A_a_fun$'|) $x1) (= (as |@_tptp.'A_b_vec_b_vec$'__0| |tptp.'A_b_vec_b_vec$'|) $x2) (= (as |@_tptp.'B$'__0| |tptp.'B$'|) $x3)) (as |@_tptp.'B_a_fun$'__0| |tptp.'B_a_fun$'|) (as |@_tptp.'B_a_fun$'__1| |tptp.'B_a_fun$'|))) % 140.60/140.98 (define-fun |tptp.'fun_app$z'| (($x1 |tptp.'A_n_vec_bool_fun$'|) ($x2 |tptp.'A_n_vec$'|)) Bool true) % 140.60/140.98 (define-fun |tptp.'one$f'| () |tptp.'A_b_vec_b_vec$'| (as |@_tptp.'A_b_vec_b_vec$'__0| |tptp.'A_b_vec_b_vec$'|)) % 140.60/140.98 (define-fun |tptp.'uwo$'| (($x1 |tptp.'A_b_vec$'|)) |tptp.'B_a_n_vec_fun$'| (ite (= (as |@_tptp.'A_b_vec$'__1| |tptp.'A_b_vec$'|) $x1) (as |@_tptp.'B_a_n_vec_fun$'__0| |tptp.'B_a_n_vec_fun$'|) (as |@_tptp.'B_a_n_vec_fun$'__1| |tptp.'B_a_n_vec_fun$'|))) % 140.60/140.98 (define-fun |tptp.'mult_row_row$b'| ((BOUND_VARIABLE_6823 |tptp.'A_b_vec_n_vec$'|) (BOUND_VARIABLE_6824 |tptp.'N$'|) (BOUND_VARIABLE_6825 |tptp.'A$'|)) |tptp.'N_a_b_vec_fun$'| (ite (= (as |@_tptp.'A_b_vec_n_vec$'__0| |tptp.'A_b_vec_n_vec$'|) (ite (and (= (as |@_tptp.'A_a_b_vec_n_vec_fun$'__1| |tptp.'A_a_b_vec_n_vec_fun$'|) (ite (and (= BOUND_VARIABLE_6823 (as |@_tptp.'A_b_vec_n_vec$'__1| |tptp.'A_b_vec_n_vec$'|)) (= BOUND_VARIABLE_6824 (as |@_tptp.'N$'__0| |tptp.'N$'|))) (as |@_tptp.'A_a_b_vec_n_vec_fun$'__0| |tptp.'A_a_b_vec_n_vec_fun$'|) (as |@_tptp.'A_a_b_vec_n_vec_fun$'__1| |tptp.'A_a_b_vec_n_vec_fun$'|))) (= BOUND_VARIABLE_6825 (as |@_tptp.'A$'__1| |tptp.'A$'|))) (as |@_tptp.'A_b_vec_n_vec$'__0| |tptp.'A_b_vec_n_vec$'|) (ite (and (= (as |@_tptp.'A_a_b_vec_n_vec_fun$'__1| |tptp.'A_a_b_vec_n_vec_fun$'|) (ite (and (= BOUND_VARIABLE_6823 (as |@_tptp.'A_b_vec_n_vec$'__1| |tptp.'A_b_vec_n_vec$'|)) (= BOUND_VARIABLE_6824 (as |@_tptp.'N$'__0| |tptp.'N$'|))) (as |@_tptp.'A_a_b_vec_n_vec_fun$'__0| |tptp.'A_a_b_vec_n_vec_fun$'|) (as |@_tptp.'A_a_b_vec_n_vec_fun$'__1| |tptp.'A_a_b_vec_n_vec_fun$'|))) (= BOUND_VARIABLE_6825 (as |@_tptp.'A$'__0| |tptp.'A$'|))) (as |@_tptp.'A_b_vec_n_vec$'__0| |tptp.'A_b_vec_n_vec$'|) (ite (and (= (as |@_tptp.'A_a_b_vec_n_vec_fun$'__0| |tptp.'A_a_b_vec_n_vec_fun$'|) (ite (and (= BOUND_VARIABLE_6823 (as |@_tptp.'A_b_vec_n_vec$'__1| |tptp.'A_b_vec_n_vec$'|)) (= BOUND_VARIABLE_6824 (as |@_tptp.'N$'__0| |tptp.'N$'|))) (as |@_tptp.'A_a_b_vec_n_vec_fun$'__0| |tptp.'A_a_b_vec_n_vec_fun$'|) (as |@_tptp.'A_a_b_vec_n_vec_fun$'__1| |tptp.'A_a_b_vec_n_vec_fun$'|))) (= BOUND_VARIABLE_6825 (as |@_tptp.'A$'__0| |tptp.'A$'|))) (as |@_tptp.'A_b_vec_n_vec$'__0| |tptp.'A_b_vec_n_vec$'|) (as |@_tptp.'A_b_vec_n_vec$'__1| |tptp.'A_b_vec_n_vec$'|))))) (as |@_tptp.'N_a_b_vec_fun$'__0| |tptp.'N_a_b_vec_fun$'|) (as |@_tptp.'N_a_b_vec_fun$'__1| |tptp.'N_a_b_vec_fun$'|))) % 140.60/140.98 (define-fun |tptp.'zero$'| () |tptp.'A$'| (as |@_tptp.'A$'__0| |tptp.'A$'|)) % 140.60/140.98 (define-fun |tptp.'interchange_A$'| () |tptp.'A_b_vec_n_vec$'| (as |@_tptp.'A_b_vec_n_vec$'__1| |tptp.'A_b_vec_n_vec$'|)) % 140.60/140.98 (define-fun |tptp.'uwt$'| (($x1 |tptp.'A_n_vec$'|) ($x2 |tptp.'N$'|)) |tptp.'N_a_fun$'| (ite (and (= (as |@_tptp.'A_n_vec$'__0| |tptp.'A_n_vec$'|) $x1) (= (as |@_tptp.'N$'__0| |tptp.'N$'|) $x2)) (as |@_tptp.'N_a_fun$'__0| |tptp.'N_a_fun$'|) (as |@_tptp.'N_a_fun$'__1| |tptp.'N_a_fun$'|))) % 140.60/140.98 (define-fun |tptp.'columnvector$e'| ((BOUND_VARIABLE_7312 |tptp.'A_b_vec$'|)) |tptp.'A_b_vec_b_vec$'| (ite (= (as |@_tptp.'B_a_b_vec_fun$'__0| |tptp.'B_a_b_vec_fun$'|) (ite (= BOUND_VARIABLE_7312 (as |@_tptp.'A_b_vec$'__0| |tptp.'A_b_vec$'|)) (as |@_tptp.'B_a_b_vec_fun$'__0| |tptp.'B_a_b_vec_fun$'|) (as |@_tptp.'B_a_b_vec_fun$'__1| |tptp.'B_a_b_vec_fun$'|))) (as |@_tptp.'A_b_vec_b_vec$'__0| |tptp.'A_b_vec_b_vec$'|) (as |@_tptp.'A_b_vec_b_vec$'__1| |tptp.'A_b_vec_b_vec$'|))) % 140.60/140.98 (define-fun |tptp.'uvx$'| () |tptp.'N_a_fun$'| (as |@_tptp.'N_a_fun$'__0| |tptp.'N_a_fun$'|)) % 140.60/140.98 (define-fun |tptp.'uvl$'| (($x1 |tptp.'A_b_vec_a_fun$'|) ($x2 |tptp.'A_b_vec_n_vec_n_vec$'|) ($x3 |tptp.'N$'|)) |tptp.'N_a_fun$'| (as |@_tptp.'N_a_fun$'__1| |tptp.'N_a_fun$'|)) % 140.60/140.98 (define-fun tptp.tlfalse () tptp.tlbool (as @tptp.tlbool_0 tptp.tlbool)) % 140.60/140.98 (define-fun |tptp.'fun_app$b'| (($x1 |tptp.'N_a_b_vec_fun$'|) ($x2 |tptp.'N$'|)) |tptp.'A_b_vec$'| (ite (and (= (as |@_tptp.'N_a_b_vec_fun$'__1| |tptp.'N_a_b_vec_fun$'|) $x1) (= (as |@_tptp.'N$'__0| |tptp.'N$'|) $x2)) (as |@_tptp.'A_b_vec$'__0| |tptp.'A_b_vec$'|) (as |@_tptp.'A_b_vec$'__1| |tptp.'A_b_vec$'|))) % 140.60/140.98 (define-fun |tptp.'mult_row$a'| ((BOUND_VARIABLE_7388 |tptp.'A_n_vec_n_vec$'|) (BOUND_VARIABLE_7389 |tptp.'N$'|) (BOUND_VARIABLE_7390 |tptp.'A$'|)) |tptp.'A_n_vec_n_vec$'| (ite (= (as |@_tptp.'N_a_n_vec_fun$'__0| |tptp.'N_a_n_vec_fun$'|) (ite (and (= BOUND_VARIABLE_7388 (as |@_tptp.'A_n_vec_n_vec$'__0| |tptp.'A_n_vec_n_vec$'|)) (= BOUND_VARIABLE_7389 (as |@_tptp.'N$'__0| |tptp.'N$'|)) (= BOUND_VARIABLE_7390 (as |@_tptp.'A$'__1| |tptp.'A$'|))) (as |@_tptp.'N_a_n_vec_fun$'__0| |tptp.'N_a_n_vec_fun$'|) (as |@_tptp.'N_a_n_vec_fun$'__1| |tptp.'N_a_n_vec_fun$'|))) (as |@_tptp.'A_n_vec_n_vec$'__0| |tptp.'A_n_vec_n_vec$'|) (as |@_tptp.'A_n_vec_n_vec$'__1| |tptp.'A_n_vec_n_vec$'|))) % 140.60/140.98 (define-fun |tptp.'uxb$'| (($x1 |tptp.'A_n_vec_n_vec$'|) ($x2 |tptp.'N$'|) ($x3 |tptp.'A$'|) ($x4 |tptp.'N$'|)) |tptp.'N_a_fun$'| (ite (and (= (as |@_tptp.'A_n_vec_n_vec$'__0| |tptp.'A_n_vec_n_vec$'|) $x1) (= (as |@_tptp.'N$'__0| |tptp.'N$'|) $x2) (= (as |@_tptp.'A$'__1| |tptp.'A$'|) $x3) (= (as |@_tptp.'N$'__0| |tptp.'N$'|) $x4)) (as |@_tptp.'N_a_fun$'__0| |tptp.'N_a_fun$'|) (as |@_tptp.'N_a_fun$'__1| |tptp.'N_a_fun$'|))) % 140.60/140.98 (define-fun |tptp.'uwe$'| (($x1 |tptp.'A_n_vec_n_vec$'|) ($x2 |tptp.'N$'|) ($x3 |tptp.'N$'|)) |tptp.'N_a_n_vec_fun$'| (ite (and (= (as |@_tptp.'A_n_vec_n_vec$'__0| |tptp.'A_n_vec_n_vec$'|) $x1) (= (as |@_tptp.'N$'__0| |tptp.'N$'|) $x2) (= (as |@_tptp.'N$'__0| |tptp.'N$'|) $x3)) (as |@_tptp.'N_a_n_vec_fun$'__0| |tptp.'N_a_n_vec_fun$'|) (as |@_tptp.'N_a_n_vec_fun$'__1| |tptp.'N_a_n_vec_fun$'|))) % 140.60/140.98 (define-fun |tptp.'vec_nth$'| (($x1 |tptp.'A_b_vec$'|)) |tptp.'B_a_fun$'| (ite (= (as |@_tptp.'A_b_vec$'__0| |tptp.'A_b_vec$'|) $x1) (as |@_tptp.'B_a_fun$'__0| |tptp.'B_a_fun$'|) (as |@_tptp.'B_a_fun$'__1| |tptp.'B_a_fun$'|))) % 140.60/140.98 (define-fun |tptp.'uminus$'| ((BOUND_VARIABLE_50281 |tptp.'A_b_vec_n_vec$'|)) |tptp.'A_b_vec_n_vec$'| (as |@_tptp.'A_b_vec_n_vec$'__0| |tptp.'A_b_vec_n_vec$'|)) % 140.60/140.98 (define-fun |tptp.'map_matrix$j'| ((BOUND_VARIABLE_7074 |tptp.'A_a_fun$'|) (BOUND_VARIABLE_7075 |tptp.'A_b_vec_b_vec$'|)) |tptp.'A_b_vec_b_vec$'| (ite (= (as |@_tptp.'B_a_b_vec_fun$'__0| |tptp.'B_a_b_vec_fun$'|) (ite (and (= BOUND_VARIABLE_7074 (as |@_tptp.'A_a_fun$'__0| |tptp.'A_a_fun$'|)) (= BOUND_VARIABLE_7075 (as |@_tptp.'A_b_vec_b_vec$'__0| |tptp.'A_b_vec_b_vec$'|))) (as |@_tptp.'B_a_b_vec_fun$'__0| |tptp.'B_a_b_vec_fun$'|) (as |@_tptp.'B_a_b_vec_fun$'__1| |tptp.'B_a_b_vec_fun$'|))) (as |@_tptp.'A_b_vec_b_vec$'__0| |tptp.'A_b_vec_b_vec$'|) (as |@_tptp.'A_b_vec_b_vec$'__1| |tptp.'A_b_vec_b_vec$'|))) % 140.60/140.98 (define-fun |tptp.'zero$a'| () |tptp.'A_b_vec_n_vec_n_vec$'| (as |@_tptp.'A_b_vec_n_vec_n_vec$'__0| |tptp.'A_b_vec_n_vec_n_vec$'|)) % 140.60/140.98 (define-fun |tptp.'fun_app$c'| (($x1 |tptp.'N_n_bool_fun_fun$'|) ($x2 |tptp.'N$'|)) |tptp.'N_bool_fun$'| (ite (and (= (as |@_tptp.'N_n_bool_fun_fun$'__0| |tptp.'N_n_bool_fun_fun$'|) $x1) (= (as |@_tptp.'N$'__0| |tptp.'N$'|) $x2)) (as |@_tptp.'N_bool_fun$'__0| |tptp.'N_bool_fun$'|) (as |@_tptp.'N_bool_fun$'__1| |tptp.'N_bool_fun$'|))) % 140.60/140.98 (define-fun |tptp.'uwu$'| (($x1 |tptp.'A_n_vec$'|)) |tptp.'N_a_n_vec_fun$'| (ite (= (as |@_tptp.'A_n_vec$'__0| |tptp.'A_n_vec$'|) $x1) (as |@_tptp.'N_a_n_vec_fun$'__0| |tptp.'N_a_n_vec_fun$'|) (as |@_tptp.'N_a_n_vec_fun$'__1| |tptp.'N_a_n_vec_fun$'|))) % 140.60/140.98 (define-fun |tptp.'mult_row$'| (($x1 |tptp.'A_b_vec_n_vec$'|) ($x2 |tptp.'N$'|)) |tptp.'A_a_b_vec_n_vec_fun$'| (ite (and (= (as |@_tptp.'A_b_vec_n_vec$'__1| |tptp.'A_b_vec_n_vec$'|) $x1) (= (as |@_tptp.'N$'__0| |tptp.'N$'|) $x2)) (as |@_tptp.'A_a_b_vec_n_vec_fun$'__0| |tptp.'A_a_b_vec_n_vec_fun$'|) (as |@_tptp.'A_a_b_vec_n_vec_fun$'__1| |tptp.'A_a_b_vec_n_vec_fun$'|))) % 140.60/140.98 (define-fun |tptp.'uxn$'| (($x1 |tptp.'A_b_vec$'|) ($x2 |tptp.'A_b_vec$'|)) |tptp.'B_a_fun$'| (ite (and (= (as |@_tptp.'A_b_vec$'__0| |tptp.'A_b_vec$'|) $x1) (= (as |@_tptp.'A_b_vec$'__0| |tptp.'A_b_vec$'|) $x2)) (as |@_tptp.'B_a_fun$'__0| |tptp.'B_a_fun$'|) (as |@_tptp.'B_a_fun$'__1| |tptp.'B_a_fun$'|))) % 140.60/140.98 (define-fun |tptp.'uwp$'| (($x1 |tptp.'A_n_vec_n_vec$'|) ($x2 |tptp.'N$'|)) |tptp.'N_a_n_vec_fun$'| (ite (and (= (as |@_tptp.'A_n_vec_n_vec$'__0| |tptp.'A_n_vec_n_vec$'|) $x1) (= (as |@_tptp.'N$'__0| |tptp.'N$'|) $x2)) (as |@_tptp.'N_a_n_vec_fun$'__0| |tptp.'N_a_n_vec_fun$'|) (as |@_tptp.'N_a_n_vec_fun$'__1| |tptp.'N_a_n_vec_fun$'|))) % 140.60/140.98 (define-fun |tptp.'uminus$b'| () |tptp.'A_b_vec_a_b_vec_fun$'| (as |@_tptp.'A_b_vec_a_b_vec_fun$'__0| |tptp.'A_b_vec_a_b_vec_fun$'|)) % 140.60/140.98 (define-fun |tptp.'uuj$'| (($x1 |tptp.'A_b_vec_b_vec$'|) ($x2 |tptp.'B$'|) ($x3 |tptp.'B$'|) ($x4 |tptp.'B$'|)) |tptp.'B_a_fun$'| (ite (and (= (as |@_tptp.'A_b_vec_b_vec$'__0| |tptp.'A_b_vec_b_vec$'|) $x1) (= (as |@_tptp.'B$'__0| |tptp.'B$'|) $x2) (= (as |@_tptp.'B$'__0| |tptp.'B$'|) $x3) (= (as |@_tptp.'B$'__0| |tptp.'B$'|) $x4)) (as |@_tptp.'B_a_fun$'__0| |tptp.'B_a_fun$'|) (as |@_tptp.'B_a_fun$'__1| |tptp.'B_a_fun$'|))) % 140.60/140.98 (define-fun |tptp.'uxk$'| (($x1 |tptp.'A_b_vec_b_vec$'|) ($x2 |tptp.'A_b_vec_b_vec$'|)) |tptp.'B_a_b_vec_fun$'| (ite (and (= (as |@_tptp.'A_b_vec_b_vec$'__0| |tptp.'A_b_vec_b_vec$'|) $x1) (= (as |@_tptp.'A_b_vec_b_vec$'__0| |tptp.'A_b_vec_b_vec$'|) $x2)) (as |@_tptp.'B_a_b_vec_fun$'__0| |tptp.'B_a_b_vec_fun$'|) (as |@_tptp.'B_a_b_vec_fun$'__1| |tptp.'B_a_b_vec_fun$'|))) % 140.60/140.98 (define-fun |tptp.'gauss_Jordan_in_ij$a'| ((BOUND_VARIABLE_7141 |tptp.'A_n_vec_n_vec$'|) (BOUND_VARIABLE_7142 |tptp.'N$'|) (BOUND_VARIABLE_7143 |tptp.'N$'|)) |tptp.'A_n_vec_n_vec$'| (ite (= (as |@_tptp.'N_a_n_vec_fun$'__0| |tptp.'N_a_n_vec_fun$'|) (ite (and (= BOUND_VARIABLE_7141 (as |@_tptp.'A_n_vec_n_vec$'__0| |tptp.'A_n_vec_n_vec$'|)) (= BOUND_VARIABLE_7142 (as |@_tptp.'N$'__0| |tptp.'N$'|)) (= BOUND_VARIABLE_7143 (as |@_tptp.'N$'__0| |tptp.'N$'|))) (as |@_tptp.'N_a_n_vec_fun$'__0| |tptp.'N_a_n_vec_fun$'|) (as |@_tptp.'N_a_n_vec_fun$'__1| |tptp.'N_a_n_vec_fun$'|))) (as |@_tptp.'A_n_vec_n_vec$'__0| |tptp.'A_n_vec_n_vec$'|) (as |@_tptp.'A_n_vec_n_vec$'__1| |tptp.'A_n_vec_n_vec$'|))) % 140.60/140.98 (define-fun |tptp.'uww$'| (($x1 |tptp.'A_b_vec$'|)) |tptp.'B_a_b_vec_fun$'| (ite (= (as |@_tptp.'A_b_vec$'__0| |tptp.'A_b_vec$'|) $x1) (as |@_tptp.'B_a_b_vec_fun$'__0| |tptp.'B_a_b_vec_fun$'|) (as |@_tptp.'B_a_b_vec_fun$'__1| |tptp.'B_a_b_vec_fun$'|))) % 140.60/140.98 (define-fun |tptp.'interchange_columns$b'| ((BOUND_VARIABLE_7005 |tptp.'A_b_vec_n_vec$'|) (BOUND_VARIABLE_7006 |tptp.'B$'|) (BOUND_VARIABLE_7007 |tptp.'B$'|)) |tptp.'A_b_vec_n_vec$'| (ite (= (as |@_tptp.'N_a_b_vec_fun$'__0| |tptp.'N_a_b_vec_fun$'|) (ite (and (= BOUND_VARIABLE_7005 (as |@_tptp.'A_b_vec_n_vec$'__0| |tptp.'A_b_vec_n_vec$'|)) (= BOUND_VARIABLE_7006 (as |@_tptp.'B$'__0| |tptp.'B$'|)) (= BOUND_VARIABLE_7007 (as |@_tptp.'B$'__0| |tptp.'B$'|))) (as |@_tptp.'N_a_b_vec_fun$'__0| |tptp.'N_a_b_vec_fun$'|) (as |@_tptp.'N_a_b_vec_fun$'__1| |tptp.'N_a_b_vec_fun$'|))) (as |@_tptp.'A_b_vec_n_vec$'__0| |tptp.'A_b_vec_n_vec$'|) (as |@_tptp.'A_b_vec_n_vec$'__1| |tptp.'A_b_vec_n_vec$'|))) % 140.60/140.98 (define-fun |tptp.'uuo$'| (($x1 |tptp.'A_b_vec_n_vec$'|) ($x2 |tptp.'B$'|) ($x3 |tptp.'B$'|)) |tptp.'N_a_b_vec_fun$'| (ite (and (= (as |@_tptp.'A_b_vec_n_vec$'__0| |tptp.'A_b_vec_n_vec$'|) $x1) (= (as |@_tptp.'B$'__0| |tptp.'B$'|) $x2) (= (as |@_tptp.'B$'__0| |tptp.'B$'|) $x3)) (as |@_tptp.'N_a_b_vec_fun$'__0| |tptp.'N_a_b_vec_fun$'|) (as |@_tptp.'N_a_b_vec_fun$'__1| |tptp.'N_a_b_vec_fun$'|))) % 140.60/140.98 (define-fun |tptp.'vec_nth$e'| (($x1 |tptp.'A_n_vec$'|)) |tptp.'N_a_fun$'| (ite (= (as |@_tptp.'A_n_vec$'__0| |tptp.'A_n_vec$'|) $x1) (as |@_tptp.'N_a_fun$'__0| |tptp.'N_a_fun$'|) (as |@_tptp.'N_a_fun$'__1| |tptp.'N_a_fun$'|))) % 140.60/140.98 (define-fun |tptp.'map_matrix$f'| ((BOUND_VARIABLE_7052 |tptp.'A_b_vec_a_b_vec_fun$'|) (BOUND_VARIABLE_7053 |tptp.'A_b_vec_n_vec_n_vec$'|)) |tptp.'A_b_vec_n_vec_n_vec$'| (ite (= (as |@_tptp.'N_a_b_vec_n_vec_fun$'__1| |tptp.'N_a_b_vec_n_vec_fun$'|) (ite (and (= BOUND_VARIABLE_7052 (as |@_tptp.'A_b_vec_a_b_vec_fun$'__1| |tptp.'A_b_vec_a_b_vec_fun$'|)) (= BOUND_VARIABLE_7053 (as |@_tptp.'A_b_vec_n_vec_n_vec$'__1| |tptp.'A_b_vec_n_vec_n_vec$'|))) (as |@_tptp.'N_a_b_vec_n_vec_fun$'__0| |tptp.'N_a_b_vec_n_vec_fun$'|) (as |@_tptp.'N_a_b_vec_n_vec_fun$'__1| |tptp.'N_a_b_vec_n_vec_fun$'|))) (as |@_tptp.'A_b_vec_n_vec_n_vec$'__0| |tptp.'A_b_vec_n_vec_n_vec$'|) (as |@_tptp.'A_b_vec_n_vec_n_vec$'__1| |tptp.'A_b_vec_n_vec_n_vec$'|))) % 140.60/140.98 (define-fun |tptp.'interchange_columns$'| ((BOUND_VARIABLE_6966 |tptp.'A_n_vec_n_vec$'|) (BOUND_VARIABLE_6967 |tptp.'N$'|) (BOUND_VARIABLE_6968 |tptp.'N$'|)) |tptp.'A_n_vec_n_vec$'| (ite (= (as |@_tptp.'N_a_n_vec_fun$'__0| |tptp.'N_a_n_vec_fun$'|) (ite (and (= BOUND_VARIABLE_6966 (as |@_tptp.'A_n_vec_n_vec$'__0| |tptp.'A_n_vec_n_vec$'|)) (= BOUND_VARIABLE_6967 (as |@_tptp.'N$'__0| |tptp.'N$'|)) (= BOUND_VARIABLE_6968 (as |@_tptp.'N$'__0| |tptp.'N$'|))) (as |@_tptp.'N_a_n_vec_fun$'__0| |tptp.'N_a_n_vec_fun$'|) (as |@_tptp.'N_a_n_vec_fun$'__1| |tptp.'N_a_n_vec_fun$'|))) (as |@_tptp.'A_n_vec_n_vec$'__0| |tptp.'A_n_vec_n_vec$'|) (as |@_tptp.'A_n_vec_n_vec$'__1| |tptp.'A_n_vec_n_vec$'|))) % 140.60/140.98 (define-fun |tptp.'uut$'| (($x1 |tptp.'A_b_vec_n_vec_n_vec$'|) ($x2 |tptp.'N$'|) ($x3 |tptp.'N$'|) ($x4 |tptp.'N$'|)) |tptp.'N_a_b_vec_fun$'| (ite (and (= (as |@_tptp.'A_b_vec_n_vec_n_vec$'__0| |tptp.'A_b_vec_n_vec_n_vec$'|) $x1) (= (as |@_tptp.'N$'__0| |tptp.'N$'|) $x2) (= (as |@_tptp.'N$'__0| |tptp.'N$'|) $x3) (= (as |@_tptp.'N$'__0| |tptp.'N$'|) $x4)) (as |@_tptp.'N_a_b_vec_fun$'__0| |tptp.'N_a_b_vec_fun$'|) (as |@_tptp.'N_a_b_vec_fun$'__1| |tptp.'N_a_b_vec_fun$'|))) % 140.60/140.98 (define-fun |tptp.'uminus$a'| ((BOUND_VARIABLE_50385 |tptp.'A_n_vec$'|)) |tptp.'A_n_vec$'| (as |@_tptp.'A_n_vec$'__1| |tptp.'A_n_vec$'|)) % 140.60/140.98 (define-fun |tptp.'fun_app$y'| (($x1 |tptp.'N_a_b_vec_n_vec_bool_fun_fun$'|) ($x2 |tptp.'N$'|)) |tptp.'A_b_vec_n_vec_bool_fun$'| (as |@_tptp.'A_b_vec_n_vec_bool_fun$'__0| |tptp.'A_b_vec_n_vec_bool_fun$'|)) % 140.60/140.98 (define-fun |tptp.'uuh$'| (($x1 |tptp.'A_n_vec_n_vec$'|) ($x2 |tptp.'N$'|) ($x3 |tptp.'N$'|) ($x4 |tptp.'N$'|)) |tptp.'N_a_fun$'| (ite (and (= (as |@_tptp.'A_n_vec_n_vec$'__0| |tptp.'A_n_vec_n_vec$'|) $x1) (= (as |@_tptp.'N$'__0| |tptp.'N$'|) $x2) (= (as |@_tptp.'N$'__0| |tptp.'N$'|) $x3) (= (as |@_tptp.'N$'__0| |tptp.'N$'|) $x4)) (as |@_tptp.'N_a_fun$'__0| |tptp.'N_a_fun$'|) (as |@_tptp.'N_a_fun$'__1| |tptp.'N_a_fun$'|))) % 140.60/140.98 (define-fun |tptp.'uwh$'| (($x1 |tptp.'A_n_vec$'|)) |tptp.'N_a_n_vec_fun$'| (ite (= (as |@_tptp.'A_n_vec$'__0| |tptp.'A_n_vec$'|) $x1) (as |@_tptp.'N_a_n_vec_fun$'__0| |tptp.'N_a_n_vec_fun$'|) (as |@_tptp.'N_a_n_vec_fun$'__1| |tptp.'N_a_n_vec_fun$'|))) % 140.60/140.98 (define-fun |tptp.'vec_lambda$h'| (($x1 |tptp.'N_a_b_vec_n_vec_n_vec_fun$'|)) |tptp.'A_b_vec_n_vec_n_vec_n_vec$'| (ite (= (as |@_tptp.'N_a_b_vec_n_vec_n_vec_fun$'__0| |tptp.'N_a_b_vec_n_vec_n_vec_fun$'|) $x1) (as |@_tptp.'A_b_vec_n_vec_n_vec_n_vec$'__0| |tptp.'A_b_vec_n_vec_n_vec_n_vec$'|) (as |@_tptp.'A_b_vec_n_vec_n_vec_n_vec$'__1| |tptp.'A_b_vec_n_vec_n_vec_n_vec$'|))) % 140.60/140.98 (define-fun |tptp.'uxr$'| () |tptp.'A_b_vec_n_vec_a_b_vec_n_vec_fun$'| (as |@_tptp.'A_b_vec_n_vec_a_b_vec_n_vec_fun$'__0| |tptp.'A_b_vec_n_vec_a_b_vec_n_vec_fun$'|)) % 140.60/140.98 (define-fun |tptp.'vec_nth$f'| (($x1 |tptp.'A_n_vec_n_vec_n_vec$'|) ($x2 |tptp.'N$'|)) |tptp.'A_n_vec_n_vec$'| (as |@_tptp.'A_n_vec_n_vec$'__0| |tptp.'A_n_vec_n_vec$'|)) % 140.60/140.98 (define-fun |tptp.'uxa$'| (($x1 |tptp.'A_n_vec$'|)) |tptp.'N_a_b_vec_fun$'| (ite (= (as |@_tptp.'A_n_vec$'__1| |tptp.'A_n_vec$'|) $x1) (as |@_tptp.'N_a_b_vec_fun$'__0| |tptp.'N_a_b_vec_fun$'|) (as |@_tptp.'N_a_b_vec_fun$'__1| |tptp.'N_a_b_vec_fun$'|))) % 140.60/140.98 (define-fun |tptp.'mult_row_row$'| ((BOUND_VARIABLE_6796 |tptp.'A_b_vec_n_vec_n_vec$'|) (BOUND_VARIABLE_6797 |tptp.'N$'|) (BOUND_VARIABLE_6798 |tptp.'A_b_vec$'|)) |tptp.'N_a_b_vec_n_vec_fun$'| (ite (= (as |@_tptp.'A_b_vec_n_vec_n_vec$'__1| |tptp.'A_b_vec_n_vec_n_vec$'|) (ite (= (as |@_tptp.'N_a_b_vec_n_vec_fun$'__1| |tptp.'N_a_b_vec_n_vec_fun$'|) (ite (and (= BOUND_VARIABLE_6796 (as |@_tptp.'A_b_vec_n_vec_n_vec$'__1| |tptp.'A_b_vec_n_vec_n_vec$'|)) (= BOUND_VARIABLE_6797 (as |@_tptp.'N$'__0| |tptp.'N$'|)) (= BOUND_VARIABLE_6798 (as |@_tptp.'A_b_vec$'__0| |tptp.'A_b_vec$'|))) (as |@_tptp.'N_a_b_vec_n_vec_fun$'__0| |tptp.'N_a_b_vec_n_vec_fun$'|) (as |@_tptp.'N_a_b_vec_n_vec_fun$'__1| |tptp.'N_a_b_vec_n_vec_fun$'|))) (as |@_tptp.'A_b_vec_n_vec_n_vec$'__0| |tptp.'A_b_vec_n_vec_n_vec$'|) (as |@_tptp.'A_b_vec_n_vec_n_vec$'__1| |tptp.'A_b_vec_n_vec_n_vec$'|))) (as |@_tptp.'N_a_b_vec_n_vec_fun$'__0| |tptp.'N_a_b_vec_n_vec_fun$'|) (as |@_tptp.'N_a_b_vec_n_vec_fun$'__1| |tptp.'N_a_b_vec_n_vec_fun$'|))) % 140.60/140.98 (define-fun |tptp.'uxq$'| () |tptp.'A_b_vec_n_vec_n_vec_a_b_vec_n_vec_n_vec_fun$'| (as |@_tptp.'A_b_vec_n_vec_n_vec_a_b_vec_n_vec_n_vec_fun$'__1| |tptp.'A_b_vec_n_vec_n_vec_a_b_vec_n_vec_n_vec_fun$'|)) % 140.60/140.98 (define-fun |tptp.'uui$'| (($x1 |tptp.'A_n_vec_n_vec$'|) ($x2 |tptp.'N$'|) ($x3 |tptp.'N$'|)) |tptp.'N_a_n_vec_fun$'| (ite (and (= (as |@_tptp.'A_n_vec_n_vec$'__0| |tptp.'A_n_vec_n_vec$'|) $x1) (= (as |@_tptp.'N$'__0| |tptp.'N$'|) $x2) (= (as |@_tptp.'N$'__0| |tptp.'N$'|) $x3)) (as |@_tptp.'N_a_n_vec_fun$'__0| |tptp.'N_a_n_vec_fun$'|) (as |@_tptp.'N_a_n_vec_fun$'__1| |tptp.'N_a_n_vec_fun$'|))) % 140.60/140.98 (define-fun |tptp.'fun_app$aa'| (($x1 |tptp.'N_a_n_vec_bool_fun_fun$'|) ($x2 |tptp.'N$'|)) |tptp.'A_n_vec_bool_fun$'| (as |@_tptp.'A_n_vec_bool_fun$'__0| |tptp.'A_n_vec_bool_fun$'|)) % 140.60/140.98 (define-fun |tptp.'rowvector$a'| ((BOUND_VARIABLE_7240 |tptp.'A_b_vec$'|)) |tptp.'A_b_vec_b_vec$'| (ite (= (as |@_tptp.'B_a_b_vec_fun$'__0| |tptp.'B_a_b_vec_fun$'|) (ite (= BOUND_VARIABLE_7240 (as |@_tptp.'A_b_vec$'__0| |tptp.'A_b_vec$'|)) (as |@_tptp.'B_a_b_vec_fun$'__0| |tptp.'B_a_b_vec_fun$'|) (as |@_tptp.'B_a_b_vec_fun$'__1| |tptp.'B_a_b_vec_fun$'|))) (as |@_tptp.'A_b_vec_b_vec$'__0| |tptp.'A_b_vec_b_vec$'|) (as |@_tptp.'A_b_vec_b_vec$'__1| |tptp.'A_b_vec_b_vec$'|))) % 140.60/140.98 (define-fun |tptp.'map_matrix$c'| ((BOUND_VARIABLE_50443 |tptp.'A_b_vec_a_fun$'|) (BOUND_VARIABLE_50445 |tptp.'A_b_vec_n_vec_n_vec$'|)) |tptp.'A_n_vec_n_vec$'| (as |@_tptp.'A_n_vec_n_vec$'__1| |tptp.'A_n_vec_n_vec$'|)) % 140.60/140.98 (define-fun |tptp.'uus$'| (($x1 |tptp.'A_b_vec_b_vec$'|) ($x2 |tptp.'B$'|) ($x3 |tptp.'B$'|)) |tptp.'B_a_b_vec_fun$'| (ite (and (= (as |@_tptp.'A_b_vec_b_vec$'__0| |tptp.'A_b_vec_b_vec$'|) $x1) (= (as |@_tptp.'B$'__0| |tptp.'B$'|) $x2) (= (as |@_tptp.'B$'__0| |tptp.'B$'|) $x3)) (as |@_tptp.'B_a_b_vec_fun$'__0| |tptp.'B_a_b_vec_fun$'|) (as |@_tptp.'B_a_b_vec_fun$'__1| |tptp.'B_a_b_vec_fun$'|))) % 140.60/140.98 (define-fun |tptp.'zero$f'| () |tptp.'A_b_vec_b_vec$'| (as |@_tptp.'A_b_vec_b_vec$'__1| |tptp.'A_b_vec_b_vec$'|)) % 140.60/140.98 (define-fun |tptp.'map_matrix$g'| (($x1 |tptp.'A_n_vec_a_b_vec_fun$'|) ($x2 |tptp.'A_n_vec_n_vec_n_vec$'|)) |tptp.'A_b_vec_n_vec_n_vec$'| (as |@_tptp.'A_b_vec_n_vec_n_vec$'__0| |tptp.'A_b_vec_n_vec_n_vec$'|)) % 140.60/140.98 (define-fun |tptp.'map_matrix$d'| ((BOUND_VARIABLE_50459 |tptp.'A_n_vec_a_fun$'|) (BOUND_VARIABLE_50461 |tptp.'A_n_vec_n_vec_n_vec$'|)) |tptp.'A_n_vec_n_vec$'| (as |@_tptp.'A_n_vec_n_vec$'__1| |tptp.'A_n_vec_n_vec$'|)) % 140.60/140.98 (define-fun |tptp.'uwj$'| (($x1 |tptp.'A_b_vec_n_vec$'|)) |tptp.'N_a_b_vec_n_vec_fun$'| (ite (= (as |@_tptp.'A_b_vec_n_vec$'__1| |tptp.'A_b_vec_n_vec$'|) $x1) (as |@_tptp.'N_a_b_vec_n_vec_fun$'__0| |tptp.'N_a_b_vec_n_vec_fun$'|) (as |@_tptp.'N_a_b_vec_n_vec_fun$'__1| |tptp.'N_a_b_vec_n_vec_fun$'|))) % 140.60/140.98 (define-fun |tptp.'vec_lambda$c'| (($x1 |tptp.'B_a_b_vec_fun$'|)) |tptp.'A_b_vec_b_vec$'| (ite (= (as |@_tptp.'B_a_b_vec_fun$'__0| |tptp.'B_a_b_vec_fun$'|) $x1) (as |@_tptp.'A_b_vec_b_vec$'__0| |tptp.'A_b_vec_b_vec$'|) (as |@_tptp.'A_b_vec_b_vec$'__1| |tptp.'A_b_vec_b_vec$'|))) % 140.60/140.98 (define-fun |tptp.'uwq$'| (($x1 |tptp.'A_n_vec_n_vec$'|)) |tptp.'N_a_n_vec_n_vec_fun$'| (ite (= (as |@_tptp.'A_n_vec_n_vec$'__0| |tptp.'A_n_vec_n_vec$'|) $x1) (as |@_tptp.'N_a_n_vec_n_vec_fun$'__0| |tptp.'N_a_n_vec_n_vec_fun$'|) (as |@_tptp.'N_a_n_vec_n_vec_fun$'__1| |tptp.'N_a_n_vec_n_vec_fun$'|))) % 140.60/140.98 (define-fun |tptp.'uxh$'| (($x1 |tptp.'A_b_vec_n_vec$'|) ($x2 |tptp.'N$'|) ($x3 |tptp.'A$'|) ($x4 |tptp.'N$'|)) |tptp.'B_a_fun$'| (ite (and (= (as |@_tptp.'A_b_vec_n_vec$'__1| |tptp.'A_b_vec_n_vec$'|) $x1) (= (as |@_tptp.'N$'__0| |tptp.'N$'|) $x2) (= (as |@_tptp.'A$'__1| |tptp.'A$'|) $x3) (= (as |@_tptp.'N$'__0| |tptp.'N$'|) $x4)) (as |@_tptp.'B_a_fun$'__0| |tptp.'B_a_fun$'|) (as |@_tptp.'B_a_fun$'__1| |tptp.'B_a_fun$'|))) % 140.60/140.98 (define-fun |tptp.'columnvector$f'| ((BOUND_VARIABLE_7321 |tptp.'A_b_vec_n_vec$'|)) |tptp.'A_b_vec_n_vec_n_vec$'| (ite (= (as |@_tptp.'N_a_b_vec_n_vec_fun$'__1| |tptp.'N_a_b_vec_n_vec_fun$'|) (ite (= BOUND_VARIABLE_7321 (as |@_tptp.'A_b_vec_n_vec$'__1| |tptp.'A_b_vec_n_vec$'|)) (as |@_tptp.'N_a_b_vec_n_vec_fun$'__0| |tptp.'N_a_b_vec_n_vec_fun$'|) (as |@_tptp.'N_a_b_vec_n_vec_fun$'__1| |tptp.'N_a_b_vec_n_vec_fun$'|))) (as |@_tptp.'A_b_vec_n_vec_n_vec$'__0| |tptp.'A_b_vec_n_vec_n_vec$'|) (as |@_tptp.'A_b_vec_n_vec_n_vec$'__1| |tptp.'A_b_vec_n_vec_n_vec$'|))) % 140.60/140.98 (define-fun |tptp.'fun_app$ac'| (($x1 |tptp.'N_a_bool_fun_fun$'|) ($x2 |tptp.'N$'|)) |tptp.'A_bool_fun$'| (as |@_tptp.'A_bool_fun$'__0| |tptp.'A_bool_fun$'|)) % 140.60/140.98 (define-fun |tptp.'one$e'| () |tptp.'A_n_vec_n_vec$'| (as |@_tptp.'A_n_vec_n_vec$'__0| |tptp.'A_n_vec_n_vec$'|)) % 140.60/140.98 (define-fun |tptp.'uxw$'| () |tptp.'A_b_vec_n_vec_a_b_vec_n_vec_fun$'| (as |@_tptp.'A_b_vec_n_vec_a_b_vec_n_vec_fun$'__1| |tptp.'A_b_vec_n_vec_a_b_vec_n_vec_fun$'|)) % 140.60/140.98 (define-fun |tptp.'vec_lambda$d'| (($x1 |tptp.'N_a_n_vec_fun$'|)) |tptp.'A_n_vec_n_vec$'| (ite (= (as |@_tptp.'N_a_n_vec_fun$'__0| |tptp.'N_a_n_vec_fun$'|) $x1) (as |@_tptp.'A_n_vec_n_vec$'__0| |tptp.'A_n_vec_n_vec$'|) (as |@_tptp.'A_n_vec_n_vec$'__1| |tptp.'A_n_vec_n_vec$'|))) % 140.60/140.98 (define-fun |tptp.'fun_app$w'| (($x1 |tptp.'A_b_vec_n_vec_a_fun$'|) ($x2 |tptp.'A_b_vec_n_vec$'|)) |tptp.'A$'| (ite (and (= (as |@_tptp.'A_b_vec_n_vec_a_fun$'__0| |tptp.'A_b_vec_n_vec_a_fun$'|) $x1) (= (as |@_tptp.'A_b_vec_n_vec$'__1| |tptp.'A_b_vec_n_vec$'|) $x2)) (as |@_tptp.'A$'__0| |tptp.'A$'|) (as |@_tptp.'A$'__1| |tptp.'A$'|))) % 140.60/140.98 (define-fun |tptp.'interchange_rows$c'| ((BOUND_VARIABLE_7018 |tptp.'A_b_vec_b_vec$'|) (BOUND_VARIABLE_7019 |tptp.'B$'|) (BOUND_VARIABLE_7020 |tptp.'B$'|)) |tptp.'A_b_vec_b_vec$'| (ite (= (as |@_tptp.'B_a_b_vec_fun$'__0| |tptp.'B_a_b_vec_fun$'|) (ite (and (= BOUND_VARIABLE_7018 (as |@_tptp.'A_b_vec_b_vec$'__0| |tptp.'A_b_vec_b_vec$'|)) (= BOUND_VARIABLE_7019 (as |@_tptp.'B$'__0| |tptp.'B$'|)) (= BOUND_VARIABLE_7020 (as |@_tptp.'B$'__0| |tptp.'B$'|))) (as |@_tptp.'B_a_b_vec_fun$'__0| |tptp.'B_a_b_vec_fun$'|) (as |@_tptp.'B_a_b_vec_fun$'__1| |tptp.'B_a_b_vec_fun$'|))) (as |@_tptp.'A_b_vec_b_vec$'__0| |tptp.'A_b_vec_b_vec$'|) (as |@_tptp.'A_b_vec_b_vec$'__1| |tptp.'A_b_vec_b_vec$'|))) % 140.60/140.98 ) % 140.60/140.98 % SZS output end Model % 140.60/140.98 % cvc5 exiting %------------------------------------------------------------------------------