%------------------------------------------------------------------------------ % File : cvc5-SAT---1.3.4 % Problem : ITP323_1 : TPTP v9.2.1. Released v8.0.0. % Transfm : none % Format : tptp:raw % Command : /export/starexec/sandbox/solver/bin/do_cvc5 /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % Computer : n020.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 : CounterSatisfiable 1.64s 1.87s % Output : Model 1.64s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : ITP323_1 : TPTP v9.2.1. Released v8.0.0. % 0.13/0.13 % Command : /export/starexec/sandbox/solver/bin/do_cvc5 /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % 0.17/0.35 % Computer : n020.cluster.edu % 0.17/0.35 % Model : x86_64 x86_64 % 0.17/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.17/0.35 % Memory : 8042.1875MB % 0.17/0.35 % OS : Linux 3.10.0-693.el7.x86_64 % 0.17/0.35 % CPULimit : 300 % 0.17/0.35 % WCLimit : 300 % 0.17/0.35 % DateTime : Tue Jun 2 05:00:25 EDT 2026 % 0.17/0.35 % CPUTime : % 0.47/0.62 %----Disproving TF0_NAR % 1.64/1.87 --- Run --finite-model-find --sort-inference --uf-ss-fair at 60... % 1.64/1.87 --- Run --mbqi at 45... % 1.64/1.87 % SZS status CounterSatisfiable % 1.64/1.87 % SZS output start Model % 1.64/1.87 ( % 1.64/1.87 ; cardinality of $$unsorted is 1 % 1.64/1.87 ; rep: (as @$$unsorted_0 $$unsorted) % 1.64/1.87 ; cardinality of |tptp.'B_a_vec_set$'| is 1 % 1.64/1.87 ; rep: (as |@_tptp.'B_a_vec_set$'__0| |tptp.'B_a_vec_set$'|) % 1.64/1.87 ; cardinality of |tptp.'B_a_vec_a_vec$'| is 1 % 1.64/1.87 ; rep: (as |@_tptp.'B_a_vec_a_vec$'__0| |tptp.'B_a_vec_a_vec$'|) % 1.64/1.87 ; cardinality of |tptp.'B_c_vec_set$'| is 1 % 1.64/1.87 ; rep: (as |@_tptp.'B_c_vec_set$'__0| |tptp.'B_c_vec_set$'|) % 1.64/1.87 ; cardinality of |tptp.'C_b_c_vec_bool_fun_fun$'| is 1 % 1.64/1.87 ; rep: (as |@_tptp.'C_b_c_vec_bool_fun_fun$'__0| |tptp.'C_b_c_vec_bool_fun_fun$'|) % 1.64/1.87 ; cardinality of |tptp.'B_c_vec_a_vec_a_vec_a_vec$'| is 1 % 1.64/1.87 ; rep: (as |@_tptp.'B_c_vec_a_vec_a_vec_a_vec$'__0| |tptp.'B_c_vec_a_vec_a_vec_a_vec$'|) % 1.64/1.87 ; cardinality of |tptp.'B_c_vec_a_vec_c_vec$'| is 1 % 1.64/1.87 ; rep: (as |@_tptp.'B_c_vec_a_vec_c_vec$'__0| |tptp.'B_c_vec_a_vec_c_vec$'|) % 1.64/1.87 ; cardinality of |tptp.'C_b_a_vec_c_vec_fun$'| is 1 % 1.64/1.87 ; rep: (as |@_tptp.'C_b_a_vec_c_vec_fun$'__0| |tptp.'C_b_a_vec_c_vec_fun$'|) % 1.64/1.87 ; cardinality of |tptp.'B_a_vec_a_vec_a_vec$'| is 1 % 1.64/1.87 ; rep: (as |@_tptp.'B_a_vec_a_vec_a_vec$'__0| |tptp.'B_a_vec_a_vec_a_vec$'|) % 1.64/1.87 ; cardinality of |tptp.'B_b_fun$'| is 3 % 1.64/1.87 ; rep: (as |@_tptp.'B_b_fun$'__0| |tptp.'B_b_fun$'|) % 1.64/1.87 ; rep: (as |@_tptp.'B_b_fun$'__1| |tptp.'B_b_fun$'|) % 1.64/1.87 ; rep: (as |@_tptp.'B_b_fun$'__2| |tptp.'B_b_fun$'|) % 1.64/1.87 ; cardinality of |tptp.'B_b_c_vec_fun$'| is 1 % 1.64/1.87 ; rep: (as |@_tptp.'B_b_c_vec_fun$'__0| |tptp.'B_b_c_vec_fun$'|) % 1.64/1.87 ; cardinality of |tptp.'A_b_a_vec_fun$'| is 1 % 1.64/1.87 ; rep: (as |@_tptp.'A_b_a_vec_fun$'__0| |tptp.'A_b_a_vec_fun$'|) % 1.64/1.87 ; cardinality of |tptp.'C_b_bool_fun_fun$'| is 1 % 1.64/1.87 ; rep: (as |@_tptp.'C_b_bool_fun_fun$'__0| |tptp.'C_b_bool_fun_fun$'|) % 1.64/1.87 ; cardinality of |tptp.'B_c_vec_bool_fun$'| is 1 % 1.64/1.87 ; rep: (as |@_tptp.'B_c_vec_bool_fun$'__0| |tptp.'B_c_vec_bool_fun$'|) % 1.64/1.87 ; cardinality of |tptp.'A_b_bool_fun_fun$'| is 1 % 1.64/1.87 ; rep: (as |@_tptp.'A_b_bool_fun_fun$'__0| |tptp.'A_b_bool_fun_fun$'|) % 1.64/1.87 ; cardinality of |tptp.'C_b_a_vec_fun$'| is 1 % 1.64/1.87 ; rep: (as |@_tptp.'C_b_a_vec_fun$'__0| |tptp.'C_b_a_vec_fun$'|) % 1.64/1.87 ; cardinality of |tptp.'B_c_vec_a_vec_b_c_vec_fun$'| is 1 % 1.64/1.87 ; rep: (as |@_tptp.'B_c_vec_a_vec_b_c_vec_fun$'__0| |tptp.'B_c_vec_a_vec_b_c_vec_fun$'|) % 1.64/1.87 ; cardinality of |tptp.'B_c_vec_b_fun$'| is 1 % 1.64/1.87 ; rep: (as |@_tptp.'B_c_vec_b_fun$'__0| |tptp.'B_c_vec_b_fun$'|) % 1.64/1.87 ; cardinality of |tptp.'B_a_vec$'| is 1 % 1.64/1.87 ; rep: (as |@_tptp.'B_a_vec$'__0| |tptp.'B_a_vec$'|) % 1.64/1.87 ; cardinality of |tptp.'A_b_a_vec_bool_fun_fun$'| is 1 % 1.64/1.87 ; rep: (as |@_tptp.'A_b_a_vec_bool_fun_fun$'__0| |tptp.'A_b_a_vec_bool_fun_fun$'|) % 1.64/1.87 ; cardinality of |tptp.'B_c_vec_a_vec$'| is 1 % 1.64/1.87 ; rep: (as |@_tptp.'B_c_vec_a_vec$'__0| |tptp.'B_c_vec_a_vec$'|) % 1.64/1.87 ; cardinality of |tptp.'C_b_a_vec_bool_fun_fun$'| is 1 % 1.64/1.87 ; rep: (as |@_tptp.'C_b_a_vec_bool_fun_fun$'__0| |tptp.'C_b_a_vec_bool_fun_fun$'|) % 1.64/1.87 ; cardinality of |tptp.'B$'| is 1 % 1.64/1.87 ; rep: (as |@_tptp.'B$'__0| |tptp.'B$'|) % 1.64/1.87 ; cardinality of |tptp.'C$'| is 1 % 1.64/1.87 ; rep: (as |@_tptp.'C$'__0| |tptp.'C$'|) % 1.64/1.87 ; cardinality of |tptp.'B_c_vec_a_vec_set$'| is 1 % 1.64/1.87 ; rep: (as |@_tptp.'B_c_vec_a_vec_set$'__0| |tptp.'B_c_vec_a_vec_set$'|) % 1.64/1.87 ; cardinality of |tptp.'C_b_fun$'| is 1 % 1.64/1.87 ; rep: (as |@_tptp.'C_b_fun$'__0| |tptp.'C_b_fun$'|) % 1.64/1.87 ; cardinality of |tptp.'B_c_vec_b_c_vec_fun$'| is 3 % 1.64/1.87 ; rep: (as |@_tptp.'B_c_vec_b_c_vec_fun$'__0| |tptp.'B_c_vec_b_c_vec_fun$'|) % 1.64/1.87 ; rep: (as |@_tptp.'B_c_vec_b_c_vec_fun$'__1| |tptp.'B_c_vec_b_c_vec_fun$'|) % 1.64/1.87 ; rep: (as |@_tptp.'B_c_vec_b_c_vec_fun$'__2| |tptp.'B_c_vec_b_c_vec_fun$'|) % 1.64/1.87 ; cardinality of |tptp.'C_b_c_vec_fun$'| is 1 % 1.64/1.87 ; rep: (as |@_tptp.'C_b_c_vec_fun$'__0| |tptp.'C_b_c_vec_fun$'|) % 1.64/1.87 ; cardinality of |tptp.'B_a_vec_c_vec$'| is 1 % 1.64/1.87 ; rep: (as |@_tptp.'B_a_vec_c_vec$'__0| |tptp.'B_a_vec_c_vec$'|) % 1.64/1.87 ; cardinality of |tptp.'B_c_vec_c_vec_a_vec$'| is 1 % 1.64/1.87 ; rep: (as |@_tptp.'B_c_vec_c_vec_a_vec$'__0| |tptp.'B_c_vec_c_vec_a_vec$'|) % 1.64/1.87 ; cardinality of tptp.tlbool is 2 % 1.64/1.87 ; rep: (as @tptp.tlbool_0 tptp.tlbool) % 1.64/1.87 ; rep: (as @tptp.tlbool_1 tptp.tlbool) % 1.64/1.87 ; cardinality of |tptp.'A_b_c_vec_fun$'| is 2 % 1.64/1.87 ; rep: (as |@_tptp.'A_b_c_vec_fun$'__0| |tptp.'A_b_c_vec_fun$'|) % 1.64/1.87 ; rep: (as |@_tptp.'A_b_c_vec_fun$'__1| |tptp.'A_b_c_vec_fun$'|) % 1.64/1.87 ; cardinality of |tptp.'A_b_c_vec_a_vec_a_vec_bool_fun_fun$'| is 1 % 1.64/1.87 ; rep: (as |@_tptp.'A_b_c_vec_a_vec_a_vec_bool_fun_fun$'__0| |tptp.'A_b_c_vec_a_vec_a_vec_bool_fun_fun$'|) % 1.64/1.87 ; cardinality of |tptp.'A_b_c_vec_a_vec_fun$'| is 2 % 1.64/1.87 ; rep: (as |@_tptp.'A_b_c_vec_a_vec_fun$'__0| |tptp.'A_b_c_vec_a_vec_fun$'|) % 1.64/1.87 ; rep: (as |@_tptp.'A_b_c_vec_a_vec_fun$'__1| |tptp.'A_b_c_vec_a_vec_fun$'|) % 1.64/1.87 ; cardinality of |tptp.'A_b_c_vec_a_vec_a_vec_fun$'| is 2 % 1.64/1.87 ; rep: (as |@_tptp.'A_b_c_vec_a_vec_a_vec_fun$'__0| |tptp.'A_b_c_vec_a_vec_a_vec_fun$'|) % 1.64/1.87 ; rep: (as |@_tptp.'A_b_c_vec_a_vec_a_vec_fun$'__1| |tptp.'A_b_c_vec_a_vec_a_vec_fun$'|) % 1.64/1.87 ; cardinality of |tptp.'B_a_vec_a_vec_c_vec$'| is 1 % 1.64/1.87 ; rep: (as |@_tptp.'B_a_vec_a_vec_c_vec$'__0| |tptp.'B_a_vec_a_vec_c_vec$'|) % 1.64/1.87 ; cardinality of |tptp.'A_b_c_vec_bool_fun_fun$'| is 1 % 1.64/1.87 ; rep: (as |@_tptp.'A_b_c_vec_bool_fun_fun$'__0| |tptp.'A_b_c_vec_bool_fun_fun$'|) % 1.64/1.87 ; cardinality of |tptp.'A_b_c_vec_a_vec_bool_fun_fun$'| is 1 % 1.64/1.87 ; rep: (as |@_tptp.'A_b_c_vec_a_vec_bool_fun_fun$'__0| |tptp.'A_b_c_vec_a_vec_bool_fun_fun$'|) % 1.64/1.87 ; cardinality of |tptp.'B_c_vec_a_vec_a_vec$'| is 1 % 1.64/1.87 ; rep: (as |@_tptp.'B_c_vec_a_vec_a_vec$'__0| |tptp.'B_c_vec_a_vec_a_vec$'|) % 1.64/1.87 ; cardinality of |tptp.'A_b_fun$'| is 1 % 1.64/1.87 ; rep: (as |@_tptp.'A_b_fun$'__0| |tptp.'A_b_fun$'|) % 1.64/1.87 ; cardinality of |tptp.'B_set$'| is 1 % 1.64/1.87 ; rep: (as |@_tptp.'B_set$'__0| |tptp.'B_set$'|) % 1.64/1.87 ; cardinality of |tptp.'B_c_vec_b_c_vec_a_vec_fun$'| is 1 % 1.64/1.87 ; rep: (as |@_tptp.'B_c_vec_b_c_vec_a_vec_fun$'__0| |tptp.'B_c_vec_b_c_vec_a_vec_fun$'|) % 1.64/1.87 ; cardinality of |tptp.'A$'| is 1 % 1.64/1.87 ; rep: (as |@_tptp.'A$'__0| |tptp.'A$'|) % 1.64/1.87 ; cardinality of |tptp.'B_set_set$'| is 1 % 1.64/1.87 ; rep: (as |@_tptp.'B_set_set$'__0| |tptp.'B_set_set$'|) % 1.64/1.87 ; cardinality of |tptp.'B_c_vec_a_vec_a_vec_set$'| is 1 % 1.64/1.87 ; rep: (as |@_tptp.'B_c_vec_a_vec_a_vec_set$'__0| |tptp.'B_c_vec_a_vec_a_vec_set$'|) % 1.64/1.87 ; cardinality of |tptp.'B_c_vec_c_vec$'| is 1 % 1.64/1.87 ; rep: (as |@_tptp.'B_c_vec_c_vec$'__0| |tptp.'B_c_vec_c_vec$'|) % 1.64/1.87 ; cardinality of |tptp.'B_a_vec_c_vec_a_vec$'| is 1 % 1.64/1.87 ; rep: (as |@_tptp.'B_a_vec_c_vec_a_vec$'__0| |tptp.'B_a_vec_c_vec_a_vec$'|) % 1.64/1.87 ; cardinality of |tptp.'B_c_vec_a_vec_a_vec_bool_fun$'| is 1 % 1.64/1.87 ; rep: (as |@_tptp.'B_c_vec_a_vec_a_vec_bool_fun$'__0| |tptp.'B_c_vec_a_vec_a_vec_bool_fun$'|) % 1.64/1.87 ; cardinality of |tptp.'B_a_vec_bool_fun$'| is 1 % 1.64/1.87 ; rep: (as |@_tptp.'B_a_vec_bool_fun$'__0| |tptp.'B_a_vec_bool_fun$'|) % 1.64/1.87 ; cardinality of |tptp.'B_c_vec_a_vec_bool_fun$'| is 1 % 1.64/1.87 ; rep: (as |@_tptp.'B_c_vec_a_vec_bool_fun$'__0| |tptp.'B_c_vec_a_vec_bool_fun$'|) % 1.64/1.87 ; cardinality of |tptp.'B_c_vec$'| is 1 % 1.64/1.87 ; rep: (as |@_tptp.'B_c_vec$'__0| |tptp.'B_c_vec$'|) % 1.64/1.87 ; cardinality of |tptp.'B_c_vec_set_set$'| is 1 % 1.64/1.87 ; rep: (as |@_tptp.'B_c_vec_set_set$'__0| |tptp.'B_c_vec_set_set$'|) % 1.64/1.87 ; cardinality of |tptp.'B_bool_fun$'| is 1 % 1.64/1.87 ; rep: (as |@_tptp.'B_bool_fun$'__0| |tptp.'B_bool_fun$'|) % 1.64/1.87 ; cardinality of |tptp.'B_c_vec_a_vec_set_set$'| is 1 % 1.64/1.87 ; rep: (as |@_tptp.'B_c_vec_a_vec_set_set$'__0| |tptp.'B_c_vec_a_vec_set_set$'|) % 1.64/1.87 (define-fun |tptp.'interchange_rows$'| ((_arg_1 |tptp.'B_a_vec_a_vec$'|) (_arg_2 |tptp.'A$'|) (_arg_3 |tptp.'A$'|)) |tptp.'B_a_vec_a_vec$'| (as |@_tptp.'B_a_vec_a_vec$'__0| |tptp.'B_a_vec_a_vec$'|)) % 1.64/1.87 (define-fun |tptp.'vec$g'| ((_arg_1 |tptp.'B_c_vec$'|)) |tptp.'B_c_vec_c_vec$'| (as |@_tptp.'B_c_vec_c_vec$'__0| |tptp.'B_c_vec_c_vec$'|)) % 1.64/1.87 (define-fun |tptp.'fun_app$r'| ((_arg_1 |tptp.'A_b_a_vec_bool_fun_fun$'|) (_arg_2 |tptp.'A$'|)) |tptp.'B_a_vec_bool_fun$'| (as |@_tptp.'B_a_vec_bool_fun$'__0| |tptp.'B_a_vec_bool_fun$'|)) % 1.64/1.87 (define-fun |tptp.'map_matrix$g'| ((_arg_1 |tptp.'B_b_fun$'|) (_arg_2 |tptp.'B_a_vec_a_vec$'|)) |tptp.'B_a_vec_a_vec$'| (as |@_tptp.'B_a_vec_a_vec$'__0| |tptp.'B_a_vec_a_vec$'|)) % 1.64/1.87 (define-fun |tptp.'times$j'| ((_arg_1 |tptp.'B_c_vec_a_vec_a_vec_set$'|) (_arg_2 |tptp.'B_c_vec_a_vec_a_vec_set$'|)) |tptp.'B_c_vec_a_vec_a_vec_set$'| (as |@_tptp.'B_c_vec_a_vec_a_vec_set$'__0| |tptp.'B_c_vec_a_vec_a_vec_set$'|)) % 1.64/1.87 (define-fun |tptp.'transpose_row$f'| ((_arg_1 |tptp.'B_c_vec_c_vec_a_vec$'|) (_arg_2 |tptp.'C$'|)) |tptp.'B_c_vec_a_vec$'| (as |@_tptp.'B_c_vec_a_vec$'__0| |tptp.'B_c_vec_a_vec$'|)) % 1.64/1.87 (define-fun |tptp.'vector_scalar_mult$b'| ((_arg_1 |tptp.'B_a_vec$'|) (_arg_2 |tptp.'B_a_vec_c_vec$'|)) |tptp.'B_a_vec_c_vec$'| (as |@_tptp.'B_a_vec_c_vec$'__0| |tptp.'B_a_vec_c_vec$'|)) % 1.64/1.87 (define-fun |tptp.'elt_set_plus$d'| ((_arg_1 |tptp.'B_set$'|) (_arg_2 |tptp.'B_set_set$'|)) |tptp.'B_set_set$'| (as |@_tptp.'B_set_set$'__0| |tptp.'B_set_set$'|)) % 1.64/1.87 (define-fun |tptp.'transpose_row$d'| ((_arg_1 |tptp.'B_a_vec_a_vec$'|)) |tptp.'A_b_a_vec_fun$'| (as |@_tptp.'A_b_a_vec_fun$'__0| |tptp.'A_b_a_vec_fun$'|)) % 1.64/1.87 (define-fun |tptp.'member$f'| ((_arg_1 |tptp.'B_c_vec_a_vec_set$'|) (_arg_2 |tptp.'B_c_vec_a_vec_set_set$'|)) Bool false) % 1.64/1.87 (define-fun |tptp.'vec_nth$b'| ((_arg_1 |tptp.'B_c_vec_c_vec$'|)) |tptp.'C_b_c_vec_fun$'| (as |@_tptp.'C_b_c_vec_fun$'__0| |tptp.'C_b_c_vec_fun$'|)) % 1.64/1.87 (define-fun |tptp.'interchange_rows$d'| ((_arg_1 |tptp.'B_c_vec_a_vec_a_vec$'|) (_arg_2 |tptp.'A$'|)) |tptp.'A_b_c_vec_a_vec_a_vec_fun$'| (as |@_tptp.'A_b_c_vec_a_vec_a_vec_fun$'__0| |tptp.'A_b_c_vec_a_vec_a_vec_fun$'|)) % 1.64/1.87 (define-fun |tptp.'row_add_row$'| ((_arg_1 |tptp.'B_c_vec_a_vec$'|) (_arg_2 |tptp.'A$'|) (_arg_3 |tptp.'A$'|) (_arg_4 |tptp.'B$'|)) |tptp.'A_b_c_vec_fun$'| (as |@_tptp.'A_b_c_vec_fun$'__0| |tptp.'A_b_c_vec_fun$'|)) % 1.64/1.87 (define-fun |tptp.'fun_app$g'| ((_arg_1 |tptp.'A_b_fun$'|) (_arg_2 |tptp.'A$'|)) |tptp.'B$'| (as |@_tptp.'B$'__0| |tptp.'B$'|)) % 1.64/1.87 (define-fun |tptp.'vector_scalar_mult$c'| ((_arg_1 |tptp.'B_c_vec$'|) (_arg_2 |tptp.'B_c_vec_c_vec$'|)) |tptp.'B_c_vec_c_vec$'| (as |@_tptp.'B_c_vec_c_vec$'__0| |tptp.'B_c_vec_c_vec$'|)) % 1.64/1.87 (define-fun |tptp.'vec$e'| ((_arg_1 |tptp.'B_c_vec_a_vec_a_vec$'|)) |tptp.'B_c_vec_a_vec_a_vec_a_vec$'| (as |@_tptp.'B_c_vec_a_vec_a_vec_a_vec$'__0| |tptp.'B_c_vec_a_vec_a_vec_a_vec$'|)) % 1.64/1.87 (define-fun |tptp.'vector_scalar_mult$e'| ((_arg_1 |tptp.'B_c_vec_a_vec$'|) (_arg_2 |tptp.'B_c_vec_a_vec_a_vec$'|)) |tptp.'B_c_vec_a_vec_a_vec$'| (as |@_tptp.'B_c_vec_a_vec_a_vec$'__0| |tptp.'B_c_vec_a_vec_a_vec$'|)) % 1.64/1.87 (define-fun |tptp.'columnvector_row$'| ((_arg_1 |tptp.'B_c_vec_a_vec$'|) (_arg_2 |tptp.'A$'|)) |tptp.'B_c_vec_a_vec$'| (as |@_tptp.'B_c_vec_a_vec$'__0| |tptp.'B_c_vec_a_vec$'|)) % 1.64/1.87 (define-fun |tptp.'vec$c'| () |tptp.'B_c_vec_b_c_vec_a_vec_fun$'| (as |@_tptp.'B_c_vec_b_c_vec_a_vec_fun$'__0| |tptp.'B_c_vec_b_c_vec_a_vec_fun$'|)) % 1.64/1.87 (define-fun |tptp.'fun_app$t'| ((_arg_1 |tptp.'A_b_c_vec_a_vec_a_vec_bool_fun_fun$'|) (_arg_2 |tptp.'A$'|)) |tptp.'B_c_vec_a_vec_a_vec_bool_fun$'| (as |@_tptp.'B_c_vec_a_vec_a_vec_bool_fun$'__0| |tptp.'B_c_vec_a_vec_a_vec_bool_fun$'|)) % 1.64/1.87 (define-fun |tptp.'vec_nth$l'| ((_arg_1 |tptp.'B_a_vec_a_vec_c_vec$'|) (_arg_2 |tptp.'C$'|)) |tptp.'B_a_vec_a_vec$'| (as |@_tptp.'B_a_vec_a_vec$'__0| |tptp.'B_a_vec_a_vec$'|)) % 1.64/1.87 (define-fun |tptp.'elt_set_times$'| ((_arg_1 |tptp.'B_a_vec$'|) (_arg_2 |tptp.'B_a_vec_set$'|)) |tptp.'B_a_vec_set$'| (as |@_tptp.'B_a_vec_set$'__0| |tptp.'B_a_vec_set$'|)) % 1.64/1.87 (define-fun |tptp.'plus$o'| ((_arg_1 |tptp.'B_set$'|) (_arg_2 |tptp.'B_set$'|)) |tptp.'B_set$'| (as |@_tptp.'B_set$'__0| |tptp.'B_set$'|)) % 1.64/1.87 (define-fun |tptp.'interchange_columns_row$d'| ((_arg_1 |tptp.'B_c_vec_a_vec_a_vec$'|) (_arg_2 |tptp.'A$'|) (_arg_3 |tptp.'A$'|)) |tptp.'A_b_c_vec_a_vec_fun$'| (as |@_tptp.'A_b_c_vec_a_vec_fun$'__1| |tptp.'A_b_c_vec_a_vec_fun$'|)) % 1.64/1.87 (define-fun |tptp.'interchange_columns$a'| ((_arg_1 |tptp.'B_c_vec_a_vec_a_vec_a_vec$'|) (_arg_2 |tptp.'A$'|) (_arg_3 |tptp.'A$'|)) |tptp.'B_c_vec_a_vec_a_vec_a_vec$'| (as |@_tptp.'B_c_vec_a_vec_a_vec_a_vec$'__0| |tptp.'B_c_vec_a_vec_a_vec_a_vec$'|)) % 1.64/1.87 (define-fun |tptp.'vector_scalar_mult$d'| ((_arg_1 |tptp.'B$'|)) |tptp.'B_c_vec_b_c_vec_fun$'| (as |@_tptp.'B_c_vec_b_c_vec_fun$'__0| |tptp.'B_c_vec_b_c_vec_fun$'|)) % 1.64/1.87 (define-fun |tptp.'map_matrix$c'| ((_arg_1 |tptp.'B_c_vec_b_c_vec_fun$'|) (_arg_2 |tptp.'B_c_vec_a_vec_a_vec$'|)) |tptp.'B_c_vec_a_vec_a_vec$'| (as |@_tptp.'B_c_vec_a_vec_a_vec$'__0| |tptp.'B_c_vec_a_vec_a_vec$'|)) % 1.64/1.87 (define-fun |tptp.'map_matrix$'| ((_arg_1 |tptp.'B_b_fun$'|) (_arg_2 |tptp.'B_c_vec_a_vec$'|)) |tptp.'B_c_vec_a_vec$'| (as |@_tptp.'B_c_vec_a_vec$'__0| |tptp.'B_c_vec_a_vec$'|)) % 1.64/1.87 (define-fun |tptp.'vec_nth$a'| ((_arg_1 |tptp.'B_c_vec$'|)) |tptp.'C_b_fun$'| (as |@_tptp.'C_b_fun$'__0| |tptp.'C_b_fun$'|)) % 1.64/1.87 (define-fun |tptp.'plus$m'| ((_arg_1 |tptp.'B_c_vec_a_vec_set$'|) (_arg_2 |tptp.'B_c_vec_a_vec_set$'|)) |tptp.'B_c_vec_a_vec_set$'| (as |@_tptp.'B_c_vec_a_vec_set$'__0| |tptp.'B_c_vec_a_vec_set$'|)) % 1.64/1.87 (define-fun |tptp.'collect$'| ((_arg_1 |tptp.'B_c_vec_bool_fun$'|)) |tptp.'B_c_vec_set$'| (as |@_tptp.'B_c_vec_set$'__0| |tptp.'B_c_vec_set$'|)) % 1.64/1.87 (define-fun |tptp.'map_matrix$a'| ((_arg_1 |tptp.'B_b_c_vec_fun$'|) (_arg_2 |tptp.'B_a_vec_a_vec$'|)) |tptp.'B_c_vec_a_vec_a_vec$'| (as |@_tptp.'B_c_vec_a_vec_a_vec$'__0| |tptp.'B_c_vec_a_vec_a_vec$'|)) % 1.64/1.87 (define-fun |tptp.'vec_nth$d'| ((_arg_1 |tptp.'B_c_vec_a_vec_a_vec_a_vec$'|)) |tptp.'A_b_c_vec_a_vec_a_vec_fun$'| (as |@_tptp.'A_b_c_vec_a_vec_a_vec_fun$'__1| |tptp.'A_b_c_vec_a_vec_a_vec_fun$'|)) % 1.64/1.87 (define-fun |tptp.'times$c'| ((_arg_1 |tptp.'B_a_vec_a_vec$'|) (_arg_2 |tptp.'B_a_vec_a_vec$'|)) |tptp.'B_a_vec_a_vec$'| (as |@_tptp.'B_a_vec_a_vec$'__0| |tptp.'B_a_vec_a_vec$'|)) % 1.64/1.87 (define-fun |tptp.'times$e'| ((_arg_1 |tptp.'B_c_vec_a_vec_a_vec_a_vec$'|) (_arg_2 |tptp.'B_c_vec_a_vec_a_vec_a_vec$'|)) |tptp.'B_c_vec_a_vec_a_vec_a_vec$'| (as |@_tptp.'B_c_vec_a_vec_a_vec_a_vec$'__0| |tptp.'B_c_vec_a_vec_a_vec_a_vec$'|)) % 1.64/1.87 (define-fun |tptp.'plus$k'| ((_arg_1 |tptp.'B_c_vec_set$'|) (_arg_2 |tptp.'B_c_vec_set$'|)) |tptp.'B_c_vec_set$'| (as |@_tptp.'B_c_vec_set$'__0| |tptp.'B_c_vec_set$'|)) % 1.64/1.87 (define-fun |tptp.'plus$j'| ((_arg_1 |tptp.'B_c_vec_a_vec_a_vec_set$'|) (_arg_2 |tptp.'B_c_vec_a_vec_a_vec_set$'|)) |tptp.'B_c_vec_a_vec_a_vec_set$'| (as |@_tptp.'B_c_vec_a_vec_a_vec_set$'__0| |tptp.'B_c_vec_a_vec_a_vec_set$'|)) % 1.64/1.87 (define-fun |tptp.'transpose$e'| ((_arg_1 |tptp.'B_a_vec_c_vec$'|)) |tptp.'B_c_vec_a_vec$'| (as |@_tptp.'B_c_vec_a_vec$'__0| |tptp.'B_c_vec_a_vec$'|)) % 1.64/1.87 (define-fun |tptp.'transpose$'| ((_arg_1 |tptp.'B_a_vec_a_vec$'|)) |tptp.'B_a_vec_a_vec$'| (as |@_tptp.'B_a_vec_a_vec$'__0| |tptp.'B_a_vec_a_vec$'|)) % 1.64/1.87 (define-fun |tptp.'fun_app$w'| ((_arg_1 |tptp.'C_b_bool_fun_fun$'|) (_arg_2 |tptp.'C$'|)) |tptp.'B_bool_fun$'| (as |@_tptp.'B_bool_fun$'__0| |tptp.'B_bool_fun$'|)) % 1.64/1.87 (define-fun |tptp.'fun_app$z'| ((_arg_1 |tptp.'A_b_c_vec_bool_fun_fun$'|) (_arg_2 |tptp.'A$'|)) |tptp.'B_c_vec_bool_fun$'| (as |@_tptp.'B_c_vec_bool_fun$'__0| |tptp.'B_c_vec_bool_fun$'|)) % 1.64/1.87 (define-fun |tptp.'interchange_rows$e'| ((_arg_1 |tptp.'B_c_vec_a_vec$'|) (_arg_2 |tptp.'A$'|)) |tptp.'A_b_c_vec_a_vec_fun$'| (as |@_tptp.'A_b_c_vec_a_vec_fun$'__0| |tptp.'A_b_c_vec_a_vec_fun$'|)) % 1.64/1.87 (define-fun |tptp.'q$'| () |tptp.'B$'| (as |@_tptp.'B$'__0| |tptp.'B$'|)) % 1.64/1.87 (define-fun |tptp.'elt_set_times$c'| ((_arg_1 |tptp.'B_c_vec_a_vec_set$'|) (_arg_2 |tptp.'B_c_vec_a_vec_set_set$'|)) |tptp.'B_c_vec_a_vec_set_set$'| (as |@_tptp.'B_c_vec_a_vec_set_set$'__0| |tptp.'B_c_vec_a_vec_set_set$'|)) % 1.64/1.87 (define-fun |tptp.'member$b'| ((_arg_1 |tptp.'B$'|) (_arg_2 |tptp.'B_set$'|)) Bool false) % 1.64/1.87 (define-fun |tptp.'member$'| ((_arg_1 |tptp.'B_c_vec_a_vec$'|) (_arg_2 |tptp.'B_c_vec_a_vec_set$'|)) Bool false) % 1.64/1.87 (define-fun |tptp.'vec_nth$j'| ((_arg_1 |tptp.'B_a_vec_a_vec_a_vec$'|) (_arg_2 |tptp.'A$'|)) |tptp.'B_a_vec_a_vec$'| (as |@_tptp.'B_a_vec_a_vec$'__0| |tptp.'B_a_vec_a_vec$'|)) % 1.64/1.87 (define-fun |tptp.'fun_app$a'| ((_arg_1 |tptp.'B_c_vec_bool_fun$'|) (_arg_2 |tptp.'B_c_vec$'|)) Bool false) % 1.64/1.87 (define-fun |tptp.'map_matrix$d'| ((_arg_1 |tptp.'B_c_vec_a_vec_b_c_vec_fun$'|) (_arg_2 |tptp.'B_c_vec_a_vec_a_vec_a_vec$'|)) |tptp.'B_c_vec_a_vec_a_vec$'| (as |@_tptp.'B_c_vec_a_vec_a_vec$'__0| |tptp.'B_c_vec_a_vec_a_vec$'|)) % 1.64/1.87 (define-fun |tptp.'plus$p'| ((_arg_1 |tptp.'B_set_set$'|) (_arg_2 |tptp.'B_set_set$'|)) |tptp.'B_set_set$'| (as |@_tptp.'B_set_set$'__0| |tptp.'B_set_set$'|)) % 1.64/1.87 (define-fun |tptp.'row_add_row$b'| ((_arg_1 |tptp.'B_c_vec_a_vec_a_vec_a_vec$'|) (_arg_2 |tptp.'A$'|) (_arg_3 |tptp.'A$'|) (_arg_4 |tptp.'B_c_vec_a_vec$'|) (_arg_5 |tptp.'A$'|)) |tptp.'B_c_vec_a_vec_a_vec$'| (as |@_tptp.'B_c_vec_a_vec_a_vec$'__0| |tptp.'B_c_vec_a_vec_a_vec$'|)) % 1.64/1.87 (define-fun |tptp.'plus$l'| ((_arg_1 |tptp.'B_c_vec_set_set$'|) (_arg_2 |tptp.'B_c_vec_set_set$'|)) |tptp.'B_c_vec_set_set$'| (as |@_tptp.'B_c_vec_set_set$'__0| |tptp.'B_c_vec_set_set$'|)) % 1.64/1.87 (define-fun |tptp.'fun_app$m'| ((_arg_1 |tptp.'B_c_vec_b_fun$'|) (_arg_2 |tptp.'B_c_vec$'|)) |tptp.'B$'| (as |@_tptp.'B$'__0| |tptp.'B$'|)) % 1.64/1.87 (define-fun |tptp.'vec$f'| ((_arg_1 |tptp.'B_a_vec$'|)) |tptp.'B_a_vec_c_vec$'| (as |@_tptp.'B_a_vec_c_vec$'__0| |tptp.'B_a_vec_c_vec$'|)) % 1.64/1.87 (define-fun |tptp.'transpose_row$'| ((_arg_1 |tptp.'B_c_vec_a_vec$'|)) |tptp.'C_b_a_vec_fun$'| (as |@_tptp.'C_b_a_vec_fun$'__0| |tptp.'C_b_a_vec_fun$'|)) % 1.64/1.87 (define-fun |tptp.'elt_set_times$e'| ((_arg_1 |tptp.'B$'|) (_arg_2 |tptp.'B_set$'|)) |tptp.'B_set$'| (as |@_tptp.'B_set$'__0| |tptp.'B_set$'|)) % 1.64/1.87 (define-fun |tptp.'interchange_columns_row$a'| ((_arg_1 |tptp.'B_c_vec_a_vec_a_vec_a_vec$'|) (_arg_2 |tptp.'A$'|) (_arg_3 |tptp.'A$'|)) |tptp.'A_b_c_vec_a_vec_a_vec_fun$'| (as |@_tptp.'A_b_c_vec_a_vec_a_vec_fun$'__1| |tptp.'A_b_c_vec_a_vec_a_vec_fun$'|)) % 1.64/1.87 (define-fun |tptp.'vec$a'| ((_arg_1 |tptp.'B_c_vec_a_vec$'|)) |tptp.'B_c_vec_a_vec_a_vec$'| (as |@_tptp.'B_c_vec_a_vec_a_vec$'__0| |tptp.'B_c_vec_a_vec_a_vec$'|)) % 1.64/1.87 (define-fun |tptp.'transpose_row$e'| ((_arg_1 |tptp.'B_c_vec_a_vec_a_vec_a_vec$'|)) |tptp.'A_b_c_vec_a_vec_a_vec_fun$'| (as |@_tptp.'A_b_c_vec_a_vec_a_vec_fun$'__1| |tptp.'A_b_c_vec_a_vec_a_vec_fun$'|)) % 1.64/1.87 (define-fun |tptp.'plus$g'| ((_arg_1 |tptp.'B_a_vec_c_vec$'|) (_arg_2 |tptp.'B_a_vec_c_vec$'|)) |tptp.'B_a_vec_c_vec$'| (as |@_tptp.'B_a_vec_c_vec$'__0| |tptp.'B_a_vec_c_vec$'|)) % 1.64/1.87 (define-fun |tptp.'fun_app$aa'| ((_arg_1 |tptp.'C_b_a_vec_c_vec_fun$'|) (_arg_2 |tptp.'C$'|)) |tptp.'B_a_vec_c_vec$'| (as |@_tptp.'B_a_vec_c_vec$'__0| |tptp.'B_a_vec_c_vec$'|)) % 1.64/1.87 (define-fun |tptp.'interchange_columns$'| ((_arg_1 |tptp.'B_a_vec_a_vec$'|) (_arg_2 |tptp.'A$'|) (_arg_3 |tptp.'A$'|)) |tptp.'B_a_vec_a_vec$'| (as |@_tptp.'B_a_vec_a_vec$'__0| |tptp.'B_a_vec_a_vec$'|)) % 1.64/1.87 (define-fun |tptp.'columnvector_row$a'| ((_arg_1 |tptp.'B_c_vec$'|) (_arg_2 |tptp.'C$'|)) |tptp.'B_c_vec$'| (as |@_tptp.'B_c_vec$'__0| |tptp.'B_c_vec$'|)) % 1.64/1.87 (define-fun |tptp.'interchange_columns$d'| ((_arg_1 |tptp.'B_c_vec_a_vec_a_vec$'|) (_arg_2 |tptp.'A$'|) (_arg_3 |tptp.'A$'|)) |tptp.'B_c_vec_a_vec_a_vec$'| (as |@_tptp.'B_c_vec_a_vec_a_vec$'__0| |tptp.'B_c_vec_a_vec_a_vec$'|)) % 1.64/1.87 (define-fun |tptp.'interchange_columns_row$e'| ((_arg_1 |tptp.'B_c_vec_a_vec$'|) (_arg_2 |tptp.'C$'|) (_arg_3 |tptp.'C$'|)) |tptp.'A_b_c_vec_fun$'| (as |@_tptp.'A_b_c_vec_fun$'__1| |tptp.'A_b_c_vec_fun$'|)) % 1.64/1.87 (define-fun |tptp.'interchange_columns$c'| ((_arg_1 |tptp.'B_a_vec_c_vec$'|) (_arg_2 |tptp.'A$'|) (_arg_3 |tptp.'A$'|)) |tptp.'B_a_vec_c_vec$'| (as |@_tptp.'B_a_vec_c_vec$'__0| |tptp.'B_a_vec_c_vec$'|)) % 1.64/1.87 (define-fun |tptp.'plus$c'| ((_arg_1 |tptp.'B_a_vec_a_vec$'|) (_arg_2 |tptp.'B_a_vec_a_vec$'|)) |tptp.'B_a_vec_a_vec$'| (as |@_tptp.'B_a_vec_a_vec$'__0| |tptp.'B_a_vec_a_vec$'|)) % 1.64/1.87 (define-fun |tptp.'fun_app$'| ((_arg_1 |tptp.'B_c_vec_a_vec_bool_fun$'|) (_arg_2 |tptp.'B_c_vec_a_vec$'|)) Bool false) % 1.64/1.87 (define-fun |tptp.'interchange_columns_row$b'| ((_arg_1 |tptp.'B_a_vec_a_vec$'|) (_arg_2 |tptp.'A$'|) (_arg_3 |tptp.'A$'|)) |tptp.'A_b_a_vec_fun$'| (as |@_tptp.'A_b_a_vec_fun$'__0| |tptp.'A_b_a_vec_fun$'|)) % 1.64/1.87 (define-fun |tptp.'vec$d'| ((_arg_1 |tptp.'B_a_vec$'|)) |tptp.'B_a_vec_a_vec$'| (as |@_tptp.'B_a_vec_a_vec$'__0| |tptp.'B_a_vec_a_vec$'|)) % 1.64/1.87 (define-fun |tptp.'times$i'| ((_arg_1 |tptp.'B_a_vec_set$'|) (_arg_2 |tptp.'B_a_vec_set$'|)) |tptp.'B_a_vec_set$'| (as |@_tptp.'B_a_vec_set$'__0| |tptp.'B_a_vec_set$'|)) % 1.64/1.87 (define-fun |tptp.'interchange_rows$c'| ((_arg_1 |tptp.'B_a_vec_c_vec$'|) (_arg_2 |tptp.'C$'|)) |tptp.'C_b_a_vec_c_vec_fun$'| (as |@_tptp.'C_b_a_vec_c_vec_fun$'__0| |tptp.'C_b_a_vec_c_vec_fun$'|)) % 1.64/1.87 (define-fun |tptp.'vector_scalar_mult$g'| ((_arg_1 |tptp.'B_c_vec$'|) (_arg_2 |tptp.'B_c_vec_a_vec$'|)) |tptp.'B_c_vec_a_vec$'| (as |@_tptp.'B_c_vec_a_vec$'__0| |tptp.'B_c_vec_a_vec$'|)) % 1.64/1.87 (define-fun |tptp.'fun_app$d'| ((_arg_1 |tptp.'C_b_c_vec_fun$'|) (_arg_2 |tptp.'C$'|)) |tptp.'B_c_vec$'| (as |@_tptp.'B_c_vec$'__0| |tptp.'B_c_vec$'|)) % 1.64/1.87 (define-fun |tptp.'fun_app$f'| ((_arg_1 |tptp.'A_b_c_vec_a_vec_a_vec_fun$'|) (_arg_2 |tptp.'A$'|)) |tptp.'B_c_vec_a_vec_a_vec$'| (as |@_tptp.'B_c_vec_a_vec_a_vec$'__0| |tptp.'B_c_vec_a_vec_a_vec$'|)) % 1.64/1.87 (define-fun |tptp.'transpose$c'| ((_arg_1 |tptp.'B_c_vec_a_vec$'|)) |tptp.'B_a_vec_c_vec$'| (as |@_tptp.'B_a_vec_c_vec$'__0| |tptp.'B_a_vec_c_vec$'|)) % 1.64/1.87 (define-fun |tptp.'vec_nth$k'| ((_arg_1 |tptp.'B_a_vec_c_vec_a_vec$'|) (_arg_2 |tptp.'A$'|)) |tptp.'B_a_vec_c_vec$'| (as |@_tptp.'B_a_vec_c_vec$'__0| |tptp.'B_a_vec_c_vec$'|)) % 1.64/1.87 (define-fun |tptp.'fun_app$u'| ((_arg_1 |tptp.'C_b_a_vec_bool_fun_fun$'|) (_arg_2 |tptp.'C$'|)) |tptp.'B_a_vec_bool_fun$'| (as |@_tptp.'B_a_vec_bool_fun$'__0| |tptp.'B_a_vec_bool_fun$'|)) % 1.64/1.87 (define-fun |tptp.'transpose$d'| ((_arg_1 |tptp.'B_c_vec_a_vec_a_vec$'|)) |tptp.'B_c_vec_a_vec_a_vec$'| (as |@_tptp.'B_c_vec_a_vec_a_vec$'__0| |tptp.'B_c_vec_a_vec_a_vec$'|)) % 1.64/1.87 (define-fun |tptp.'columnvector_row$h'| ((_arg_1 |tptp.'B_a_vec_c_vec$'|) (_arg_2 |tptp.'C$'|)) |tptp.'B_a_vec_a_vec$'| (as |@_tptp.'B_a_vec_a_vec$'__0| |tptp.'B_a_vec_a_vec$'|)) % 1.64/1.87 (define-fun |tptp.'elt_set_times$a'| ((_arg_1 |tptp.'B_c_vec_a_vec_a_vec$'|) (_arg_2 |tptp.'B_c_vec_a_vec_a_vec_set$'|)) |tptp.'B_c_vec_a_vec_a_vec_set$'| (as |@_tptp.'B_c_vec_a_vec_a_vec_set$'__0| |tptp.'B_c_vec_a_vec_a_vec_set$'|)) % 1.64/1.87 (define-fun |tptp.'elt_set_plus$g'| ((_arg_1 |tptp.'B_c_vec$'|) (_arg_2 |tptp.'B_c_vec_set$'|)) |tptp.'B_c_vec_set$'| (as |@_tptp.'B_c_vec_set$'__0| |tptp.'B_c_vec_set$'|)) % 1.64/1.87 (define-fun |tptp.'transpose_row$h'| ((_arg_1 |tptp.'B_a_vec_c_vec_a_vec$'|) (_arg_2 |tptp.'C$'|)) |tptp.'B_a_vec_a_vec$'| (as |@_tptp.'B_a_vec_a_vec$'__0| |tptp.'B_a_vec_a_vec$'|)) % 1.64/1.87 (define-fun |tptp.'b$'| () |tptp.'A$'| (as |@_tptp.'A$'__0| |tptp.'A$'|)) % 1.64/1.87 (define-fun |tptp.'map_matrix$i'| ((_arg_1 |tptp.'B_b_c_vec_fun$'|) (_arg_2 |tptp.'B_a_vec_c_vec$'|)) |tptp.'B_c_vec_a_vec_c_vec$'| (as |@_tptp.'B_c_vec_a_vec_c_vec$'__0| |tptp.'B_c_vec_a_vec_c_vec$'|)) % 1.64/1.87 (define-fun |tptp.'fun_app$o'| ((_arg_1 |tptp.'B_c_vec_a_vec_b_c_vec_fun$'|) (_arg_2 |tptp.'B_c_vec_a_vec$'|)) |tptp.'B_c_vec$'| (as |@_tptp.'B_c_vec$'__0| |tptp.'B_c_vec$'|)) % 1.64/1.87 (define-fun |tptp.'fun_app$e'| ((_arg_1 |tptp.'A_b_c_vec_a_vec_fun$'|) (_arg_2 |tptp.'A$'|)) |tptp.'B_c_vec_a_vec$'| (as |@_tptp.'B_c_vec_a_vec$'__0| |tptp.'B_c_vec_a_vec$'|)) % 1.64/1.87 (define-fun |tptp.'columnvector_row$e'| ((_arg_1 |tptp.'B_c_vec_a_vec_a_vec$'|) (_arg_2 |tptp.'A$'|)) |tptp.'B_c_vec_a_vec_a_vec$'| (as |@_tptp.'B_c_vec_a_vec_a_vec$'__0| |tptp.'B_c_vec_a_vec_a_vec$'|)) % 1.64/1.87 (define-fun |tptp.'interchange_columns_row$c'| ((_arg_1 |tptp.'B_a_vec_c_vec$'|) (_arg_2 |tptp.'A$'|) (_arg_3 |tptp.'A$'|)) |tptp.'C_b_a_vec_fun$'| (as |@_tptp.'C_b_a_vec_fun$'__0| |tptp.'C_b_a_vec_fun$'|)) % 1.64/1.87 (define-fun |tptp.'transpose$b'| ((_arg_1 |tptp.'B_c_vec_c_vec$'|)) |tptp.'B_c_vec_c_vec$'| (as |@_tptp.'B_c_vec_c_vec$'__0| |tptp.'B_c_vec_c_vec$'|)) % 1.64/1.87 (define-fun |tptp.'fun_app$q'| ((_arg_1 |tptp.'B_a_vec_bool_fun$'|) (_arg_2 |tptp.'B_a_vec$'|)) Bool false) % 1.64/1.87 (define-fun tptp.tltrue () tptp.tlbool (as @tptp.tlbool_0 tptp.tlbool)) % 1.64/1.87 (define-fun |tptp.'transpose_row$c'| ((_arg_1 |tptp.'B_a_vec_c_vec$'|)) |tptp.'A_b_c_vec_fun$'| (as |@_tptp.'A_b_c_vec_fun$'__1| |tptp.'A_b_c_vec_fun$'|)) % 1.64/1.87 (define-fun |tptp.'interchange_rows_row$e'| ((_arg_1 |tptp.'B_c_vec_a_vec$'|) (_arg_2 |tptp.'A$'|) (_arg_3 |tptp.'A$'|)) |tptp.'A_b_c_vec_fun$'| (as |@_tptp.'A_b_c_vec_fun$'__1| |tptp.'A_b_c_vec_fun$'|)) % 1.64/1.87 (define-fun |tptp.'uub$'| ((_arg_1 |tptp.'B_set$'|)) |tptp.'B_bool_fun$'| (as |@_tptp.'B_bool_fun$'__0| |tptp.'B_bool_fun$'|)) % 1.64/1.87 (define-fun |tptp.'times$l'| ((_arg_1 |tptp.'B_c_vec_set_set$'|) (_arg_2 |tptp.'B_c_vec_set_set$'|)) |tptp.'B_c_vec_set_set$'| (as |@_tptp.'B_c_vec_set_set$'__0| |tptp.'B_c_vec_set_set$'|)) % 1.64/1.87 (define-fun |tptp.'collect$b'| ((_arg_1 |tptp.'B_bool_fun$'|)) |tptp.'B_set$'| (as |@_tptp.'B_set$'__0| |tptp.'B_set$'|)) % 1.64/1.87 (define-fun |tptp.'map_matrix$h'| ((_arg_1 |tptp.'B_b_fun$'|) (_arg_2 |tptp.'B_a_vec_c_vec$'|)) |tptp.'B_a_vec_c_vec$'| (as |@_tptp.'B_a_vec_c_vec$'__0| |tptp.'B_a_vec_c_vec$'|)) % 1.64/1.87 (define-fun |tptp.'times$'| ((_arg_1 |tptp.'B$'|)) |tptp.'B_b_fun$'| (as |@_tptp.'B_b_fun$'__2| |tptp.'B_b_fun$'|)) % 1.64/1.87 (define-fun |tptp.'interchange_rows$a'| ((_arg_1 |tptp.'B_c_vec_a_vec_a_vec_a_vec$'|) (_arg_2 |tptp.'A$'|) (_arg_3 |tptp.'A$'|)) |tptp.'B_c_vec_a_vec_a_vec_a_vec$'| (as |@_tptp.'B_c_vec_a_vec_a_vec_a_vec$'__0| |tptp.'B_c_vec_a_vec_a_vec_a_vec$'|)) % 1.64/1.87 (define-fun |tptp.'interchange_rows_row$'| ((_arg_1 |tptp.'B_c_vec_c_vec$'|) (_arg_2 |tptp.'C$'|) (_arg_3 |tptp.'C$'|)) |tptp.'C_b_c_vec_fun$'| (as |@_tptp.'C_b_c_vec_fun$'__0| |tptp.'C_b_c_vec_fun$'|)) % 1.64/1.87 (define-fun |tptp.'elt_set_plus$c'| ((_arg_1 |tptp.'B_c_vec_a_vec_set$'|) (_arg_2 |tptp.'B_c_vec_a_vec_set_set$'|)) |tptp.'B_c_vec_a_vec_set_set$'| (as |@_tptp.'B_c_vec_a_vec_set_set$'__0| |tptp.'B_c_vec_a_vec_set_set$'|)) % 1.64/1.87 (define-fun |tptp.'interchange_rows$b'| ((_arg_1 |tptp.'B_c_vec_c_vec$'|) (_arg_2 |tptp.'C$'|) (_arg_3 |tptp.'C$'|)) |tptp.'B_c_vec_c_vec$'| (as |@_tptp.'B_c_vec_c_vec$'__0| |tptp.'B_c_vec_c_vec$'|)) % 1.64/1.87 (define-fun |tptp.'a$'| () |tptp.'B_c_vec_a_vec$'| (as |@_tptp.'B_c_vec_a_vec$'__0| |tptp.'B_c_vec_a_vec$'|)) % 1.64/1.87 (define-fun |tptp.'elt_set_times$g'| ((_arg_1 |tptp.'B_c_vec$'|) (_arg_2 |tptp.'B_c_vec_set$'|)) |tptp.'B_c_vec_set$'| (as |@_tptp.'B_c_vec_set$'__0| |tptp.'B_c_vec_set$'|)) % 1.64/1.87 (define-fun |tptp.'member$e'| ((_arg_1 |tptp.'B_c_vec_set$'|) (_arg_2 |tptp.'B_c_vec_set_set$'|)) Bool false) % 1.64/1.87 (define-fun |tptp.'elt_set_times$f'| ((_arg_1 |tptp.'B_c_vec_a_vec$'|) (_arg_2 |tptp.'B_c_vec_a_vec_set$'|)) |tptp.'B_c_vec_a_vec_set$'| (as |@_tptp.'B_c_vec_a_vec_set$'__0| |tptp.'B_c_vec_a_vec_set$'|)) % 1.64/1.87 (define-fun |tptp.'times$m'| ((_arg_1 |tptp.'B_c_vec_a_vec_set$'|) (_arg_2 |tptp.'B_c_vec_a_vec_set$'|)) |tptp.'B_c_vec_a_vec_set$'| (as |@_tptp.'B_c_vec_a_vec_set$'__0| |tptp.'B_c_vec_a_vec_set$'|)) % 1.64/1.87 (define-fun |tptp.'plus$'| ((_arg_1 |tptp.'B$'|)) |tptp.'B_b_fun$'| (as |@_tptp.'B_b_fun$'__1| |tptp.'B_b_fun$'|)) % 1.64/1.87 (define-fun |tptp.'elt_set_times$b'| ((_arg_1 |tptp.'B_c_vec_set$'|) (_arg_2 |tptp.'B_c_vec_set_set$'|)) |tptp.'B_c_vec_set_set$'| (as |@_tptp.'B_c_vec_set_set$'__0| |tptp.'B_c_vec_set_set$'|)) % 1.64/1.87 (define-fun |tptp.'plus$f'| ((_arg_1 |tptp.'B_c_vec_a_vec_a_vec$'|) (_arg_2 |tptp.'B_c_vec_a_vec_a_vec$'|)) |tptp.'B_c_vec_a_vec_a_vec$'| (as |@_tptp.'B_c_vec_a_vec_a_vec$'__0| |tptp.'B_c_vec_a_vec_a_vec$'|)) % 1.64/1.87 (define-fun |tptp.'vector_scalar_mult$a'| ((_arg_1 |tptp.'B_c_vec_a_vec_a_vec$'|) (_arg_2 |tptp.'B_c_vec_a_vec_a_vec_a_vec$'|)) |tptp.'B_c_vec_a_vec_a_vec_a_vec$'| (as |@_tptp.'B_c_vec_a_vec_a_vec_a_vec$'__0| |tptp.'B_c_vec_a_vec_a_vec_a_vec$'|)) % 1.64/1.87 (define-fun |tptp.'fun_app$y'| ((_arg_1 |tptp.'A_b_bool_fun_fun$'|) (_arg_2 |tptp.'A$'|)) |tptp.'B_bool_fun$'| (as |@_tptp.'B_bool_fun$'__0| |tptp.'B_bool_fun$'|)) % 1.64/1.87 (define-fun |tptp.'transpose_row$b'| ((_arg_1 |tptp.'B_c_vec_c_vec$'|)) |tptp.'C_b_c_vec_fun$'| (as |@_tptp.'C_b_c_vec_fun$'__0| |tptp.'C_b_c_vec_fun$'|)) % 1.64/1.87 (define-fun |tptp.'map_matrix$e'| ((_arg_1 |tptp.'B_c_vec_b_c_vec_a_vec_fun$'|) (_arg_2 |tptp.'B_c_vec_a_vec_a_vec$'|)) |tptp.'B_c_vec_a_vec_a_vec_a_vec$'| (as |@_tptp.'B_c_vec_a_vec_a_vec_a_vec$'__0| |tptp.'B_c_vec_a_vec_a_vec_a_vec$'|)) % 1.64/1.87 (define-fun |tptp.'row_add_row$c'| ((_arg_1 |tptp.'B_a_vec_a_vec$'|) (_arg_2 |tptp.'A$'|) (_arg_3 |tptp.'A$'|) (_arg_4 |tptp.'B$'|) (_arg_5 |tptp.'A$'|)) |tptp.'B_a_vec$'| (as |@_tptp.'B_a_vec$'__0| |tptp.'B_a_vec$'|)) % 1.64/1.87 (define-fun |tptp.'member$c'| ((_arg_1 |tptp.'B_a_vec$'|) (_arg_2 |tptp.'B_a_vec_set$'|)) Bool false) % 1.64/1.87 (define-fun |tptp.'interchange_rows_row$d'| ((_arg_1 |tptp.'B_c_vec_a_vec_a_vec$'|) (_arg_2 |tptp.'A$'|) (_arg_3 |tptp.'A$'|)) |tptp.'A_b_c_vec_a_vec_fun$'| (as |@_tptp.'A_b_c_vec_a_vec_fun$'__1| |tptp.'A_b_c_vec_a_vec_fun$'|)) % 1.64/1.87 (define-fun |tptp.'fun_app$x'| ((_arg_1 |tptp.'A_b_c_vec_a_vec_bool_fun_fun$'|) (_arg_2 |tptp.'A$'|)) |tptp.'B_c_vec_a_vec_bool_fun$'| (as |@_tptp.'B_c_vec_a_vec_bool_fun$'__0| |tptp.'B_c_vec_a_vec_bool_fun$'|)) % 1.64/1.87 (define-fun |tptp.'fun_app$i'| ((_arg_1 |tptp.'C_b_a_vec_fun$'|) (_arg_2 |tptp.'C$'|)) |tptp.'B_a_vec$'| (as |@_tptp.'B_a_vec$'__0| |tptp.'B_a_vec$'|)) % 1.64/1.87 (define-fun |tptp.'interchange_rows_row$c'| ((_arg_1 |tptp.'B_a_vec_c_vec$'|) (_arg_2 |tptp.'C$'|) (_arg_3 |tptp.'C$'|)) |tptp.'C_b_a_vec_fun$'| (as |@_tptp.'C_b_a_vec_fun$'__0| |tptp.'C_b_a_vec_fun$'|)) % 1.64/1.87 (define-fun |tptp.'a$a'| () |tptp.'A$'| (as |@_tptp.'A$'__0| |tptp.'A$'|)) % 1.64/1.87 (define-fun |tptp.'fun_app$n'| ((_arg_1 |tptp.'B_c_vec_b_c_vec_fun$'|) (_arg_2 |tptp.'B_c_vec$'|)) |tptp.'B_c_vec$'| (as |@_tptp.'B_c_vec$'__0| |tptp.'B_c_vec$'|)) % 1.64/1.87 (define-fun |tptp.'times$a'| ((_arg_1 |tptp.'B_c_vec_a_vec$'|) (_arg_2 |tptp.'B_c_vec_a_vec$'|)) |tptp.'B_c_vec_a_vec$'| (as |@_tptp.'B_c_vec_a_vec$'__0| |tptp.'B_c_vec_a_vec$'|)) % 1.64/1.87 (define-fun |tptp.'plus$e'| ((_arg_1 |tptp.'B_c_vec_a_vec_a_vec_a_vec$'|) (_arg_2 |tptp.'B_c_vec_a_vec_a_vec_a_vec$'|)) |tptp.'B_c_vec_a_vec_a_vec_a_vec$'| (as |@_tptp.'B_c_vec_a_vec_a_vec_a_vec$'__0| |tptp.'B_c_vec_a_vec_a_vec_a_vec$'|)) % 1.64/1.87 (define-fun |tptp.'times$b'| ((_arg_1 |tptp.'B_c_vec$'|)) |tptp.'B_c_vec_b_c_vec_fun$'| (as |@_tptp.'B_c_vec_b_c_vec_fun$'__1| |tptp.'B_c_vec_b_c_vec_fun$'|)) % 1.64/1.87 (define-fun |tptp.'vec$b'| () |tptp.'B_b_c_vec_fun$'| (as |@_tptp.'B_b_c_vec_fun$'__0| |tptp.'B_b_c_vec_fun$'|)) % 1.64/1.87 (define-fun |tptp.'vec_nth$g'| ((_arg_1 |tptp.'B_a_vec_c_vec$'|)) |tptp.'C_b_a_vec_fun$'| (as |@_tptp.'C_b_a_vec_fun$'__0| |tptp.'C_b_a_vec_fun$'|)) % 1.64/1.87 (define-fun |tptp.'plus$b'| ((_arg_1 |tptp.'B_c_vec$'|)) |tptp.'B_c_vec_b_c_vec_fun$'| (as |@_tptp.'B_c_vec_b_c_vec_fun$'__2| |tptp.'B_c_vec_b_c_vec_fun$'|)) % 1.64/1.87 (define-fun |tptp.'plus$a'| ((_arg_1 |tptp.'B_c_vec_a_vec$'|) (_arg_2 |tptp.'B_c_vec_a_vec$'|)) |tptp.'B_c_vec_a_vec$'| (as |@_tptp.'B_c_vec_a_vec$'__0| |tptp.'B_c_vec_a_vec$'|)) % 1.64/1.87 (define-fun |tptp.'columnvector_row$b'| ((_arg_1 |tptp.'B_a_vec$'|) (_arg_2 |tptp.'A$'|)) |tptp.'B_c_vec$'| (as |@_tptp.'B_c_vec$'__0| |tptp.'B_c_vec$'|)) % 1.64/1.87 (define-fun |tptp.'times$p'| ((_arg_1 |tptp.'B_set_set$'|) (_arg_2 |tptp.'B_set_set$'|)) |tptp.'B_set_set$'| (as |@_tptp.'B_set_set$'__0| |tptp.'B_set_set$'|)) % 1.64/1.87 (define-fun |tptp.'map_matrix$b'| ((_arg_1 |tptp.'B_c_vec_b_fun$'|) (_arg_2 |tptp.'B_c_vec_a_vec_a_vec$'|)) |tptp.'B_a_vec_a_vec$'| (as |@_tptp.'B_a_vec_a_vec$'__0| |tptp.'B_a_vec_a_vec$'|)) % 1.64/1.87 (define-fun |tptp.'times$g'| ((_arg_1 |tptp.'B_a_vec_c_vec$'|) (_arg_2 |tptp.'B_a_vec_c_vec$'|)) |tptp.'B_a_vec_c_vec$'| (as |@_tptp.'B_a_vec_c_vec$'__0| |tptp.'B_a_vec_c_vec$'|)) % 1.64/1.87 (define-fun |tptp.'plus$h'| ((_arg_1 |tptp.'B_c_vec_c_vec$'|) (_arg_2 |tptp.'B_c_vec_c_vec$'|)) |tptp.'B_c_vec_c_vec$'| (as |@_tptp.'B_c_vec_c_vec$'__0| |tptp.'B_c_vec_c_vec$'|)) % 1.64/1.87 (define-fun |tptp.'row_add_row$d'| ((_arg_1 |tptp.'B_a_vec_c_vec$'|) (_arg_2 |tptp.'C$'|) (_arg_3 |tptp.'C$'|) (_arg_4 |tptp.'B$'|) (_arg_5 |tptp.'C$'|)) |tptp.'B_a_vec$'| (as |@_tptp.'B_a_vec$'__0| |tptp.'B_a_vec$'|)) % 1.64/1.87 (define-fun |tptp.'vec_nth$f'| ((_arg_1 |tptp.'B_a_vec_a_vec$'|)) |tptp.'A_b_a_vec_fun$'| (as |@_tptp.'A_b_a_vec_fun$'__0| |tptp.'A_b_a_vec_fun$'|)) % 1.64/1.87 (define-fun |tptp.'uua$'| ((_arg_1 |tptp.'B_c_vec_a_vec_set$'|)) |tptp.'B_c_vec_a_vec_bool_fun$'| (as |@_tptp.'B_c_vec_a_vec_bool_fun$'__0| |tptp.'B_c_vec_a_vec_bool_fun$'|)) % 1.64/1.87 (define-fun |tptp.'elt_set_plus$'| ((_arg_1 |tptp.'B_a_vec$'|) (_arg_2 |tptp.'B_a_vec_set$'|)) |tptp.'B_a_vec_set$'| (as |@_tptp.'B_a_vec_set$'__0| |tptp.'B_a_vec_set$'|)) % 1.64/1.87 (define-fun |tptp.'times$f'| ((_arg_1 |tptp.'B_c_vec_a_vec_a_vec$'|) (_arg_2 |tptp.'B_c_vec_a_vec_a_vec$'|)) |tptp.'B_c_vec_a_vec_a_vec$'| (as |@_tptp.'B_c_vec_a_vec_a_vec$'__0| |tptp.'B_c_vec_a_vec_a_vec$'|)) % 1.64/1.87 (define-fun |tptp.'vec_nth$'| ((_arg_1 |tptp.'B_c_vec_a_vec$'|)) |tptp.'A_b_c_vec_fun$'| (as |@_tptp.'A_b_c_vec_fun$'__1| |tptp.'A_b_c_vec_fun$'|)) % 1.64/1.87 (define-fun |tptp.'vec_nth$c'| ((_arg_1 |tptp.'B_c_vec_a_vec_a_vec$'|)) |tptp.'A_b_c_vec_a_vec_fun$'| (as |@_tptp.'A_b_c_vec_a_vec_fun$'__1| |tptp.'A_b_c_vec_a_vec_fun$'|)) % 1.64/1.87 (define-fun |tptp.'columnvector_row$f'| ((_arg_1 |tptp.'B_c_vec_c_vec$'|) (_arg_2 |tptp.'C$'|)) |tptp.'B_c_vec_a_vec$'| (as |@_tptp.'B_c_vec_a_vec$'__0| |tptp.'B_c_vec_a_vec$'|)) % 1.64/1.87 (define-fun |tptp.'map_matrix$f'| ((_arg_1 |tptp.'B_b_fun$'|) (_arg_2 |tptp.'B_c_vec_c_vec$'|)) |tptp.'B_c_vec_c_vec$'| (as |@_tptp.'B_c_vec_c_vec$'__0| |tptp.'B_c_vec_c_vec$'|)) % 1.64/1.87 (define-fun |tptp.'times$o'| ((_arg_1 |tptp.'B_set$'|) (_arg_2 |tptp.'B_set$'|)) |tptp.'B_set$'| (as |@_tptp.'B_set$'__0| |tptp.'B_set$'|)) % 1.64/1.87 (define-fun |tptp.'collect$a'| ((_arg_1 |tptp.'B_c_vec_a_vec_bool_fun$'|)) |tptp.'B_c_vec_a_vec_set$'| (as |@_tptp.'B_c_vec_a_vec_set$'__0| |tptp.'B_c_vec_a_vec_set$'|)) % 1.64/1.87 (define-fun |tptp.'times$d'| ((_arg_1 |tptp.'B_a_vec$'|) (_arg_2 |tptp.'B_a_vec$'|)) |tptp.'B_a_vec$'| (as |@_tptp.'B_a_vec$'__0| |tptp.'B_a_vec$'|)) % 1.64/1.87 (define-fun |tptp.'columnvector_row$i'| ((_arg_1 |tptp.'B_a_vec_a_vec$'|) (_arg_2 |tptp.'A$'|)) |tptp.'B_a_vec_c_vec$'| (as |@_tptp.'B_a_vec_c_vec$'__0| |tptp.'B_a_vec_c_vec$'|)) % 1.64/1.87 (define-fun |tptp.'member$d'| ((_arg_1 |tptp.'B_c_vec_a_vec_a_vec$'|) (_arg_2 |tptp.'B_c_vec_a_vec_a_vec_set$'|)) Bool false) % 1.64/1.87 (define-fun |tptp.'less_eq$b'| ((_arg_1 |tptp.'B_set$'|) (_arg_2 |tptp.'B_set$'|)) Bool true) % 1.64/1.87 (define-fun |tptp.'row_add_row$e'| ((_arg_1 |tptp.'B_c_vec_a_vec_a_vec$'|) (_arg_2 |tptp.'A$'|) (_arg_3 |tptp.'A$'|) (_arg_4 |tptp.'B_c_vec$'|) (_arg_5 |tptp.'A$'|)) |tptp.'B_c_vec_a_vec$'| (as |@_tptp.'B_c_vec_a_vec$'__0| |tptp.'B_c_vec_a_vec$'|)) % 1.64/1.87 (define-fun |tptp.'times$k'| ((_arg_1 |tptp.'B_c_vec_set$'|) (_arg_2 |tptp.'B_c_vec_set$'|)) |tptp.'B_c_vec_set$'| (as |@_tptp.'B_c_vec_set$'__0| |tptp.'B_c_vec_set$'|)) % 1.64/1.87 (define-fun |tptp.'vec_nth$e'| ((_arg_1 |tptp.'B_a_vec$'|)) |tptp.'A_b_fun$'| (as |@_tptp.'A_b_fun$'__0| |tptp.'A_b_fun$'|)) % 1.64/1.87 (define-fun |tptp.'elt_set_plus$f'| ((_arg_1 |tptp.'B_c_vec_a_vec$'|) (_arg_2 |tptp.'B_c_vec_a_vec_set$'|)) |tptp.'B_c_vec_a_vec_set$'| (as |@_tptp.'B_c_vec_a_vec_set$'__0| |tptp.'B_c_vec_a_vec_set$'|)) % 1.64/1.87 (define-fun tptp.tlfalse () tptp.tlbool (as @tptp.tlbool_1 tptp.tlbool)) % 1.64/1.87 (define-fun |tptp.'fun_app$k'| ((_arg_1 |tptp.'B_b_fun$'|) (_arg_2 |tptp.'B$'|)) |tptp.'B$'| (as |@_tptp.'B$'__0| |tptp.'B$'|)) % 1.64/1.87 (define-fun |tptp.'elt_set_plus$e'| ((_arg_1 |tptp.'B$'|) (_arg_2 |tptp.'B_set$'|)) |tptp.'B_set$'| (as |@_tptp.'B_set$'__0| |tptp.'B_set$'|)) % 1.64/1.87 (define-fun |tptp.'row_add$'| ((_arg_1 |tptp.'B_c_vec_a_vec$'|) (_arg_2 |tptp.'A$'|) (_arg_3 |tptp.'A$'|) (_arg_4 |tptp.'B$'|)) |tptp.'B_c_vec_a_vec$'| (as |@_tptp.'B_c_vec_a_vec$'__0| |tptp.'B_c_vec_a_vec$'|)) % 1.64/1.87 (define-fun |tptp.'transpose$a'| ((_arg_1 |tptp.'B_c_vec_a_vec_a_vec_a_vec$'|)) |tptp.'B_c_vec_a_vec_a_vec_a_vec$'| (as |@_tptp.'B_c_vec_a_vec_a_vec_a_vec$'__0| |tptp.'B_c_vec_a_vec_a_vec_a_vec$'|)) % 1.64/1.87 (define-fun |tptp.'interchange_rows_row$b'| ((_arg_1 |tptp.'B_a_vec_a_vec$'|) (_arg_2 |tptp.'A$'|) (_arg_3 |tptp.'A$'|)) |tptp.'A_b_a_vec_fun$'| (as |@_tptp.'A_b_a_vec_fun$'__0| |tptp.'A_b_a_vec_fun$'|)) % 1.64/1.87 (define-fun |tptp.'transpose_row$i'| ((_arg_1 |tptp.'B_a_vec_a_vec_c_vec$'|) (_arg_2 |tptp.'A$'|)) |tptp.'B_a_vec_c_vec$'| (as |@_tptp.'B_a_vec_c_vec$'__0| |tptp.'B_a_vec_c_vec$'|)) % 1.64/1.87 (define-fun |tptp.'row_add_row$a'| ((_arg_1 |tptp.'B_c_vec_c_vec$'|) (_arg_2 |tptp.'C$'|) (_arg_3 |tptp.'C$'|) (_arg_4 |tptp.'B$'|) (_arg_5 |tptp.'C$'|)) |tptp.'B_c_vec$'| (as |@_tptp.'B_c_vec$'__0| |tptp.'B_c_vec$'|)) % 1.64/1.87 (define-fun |tptp.'fun_app$p'| ((_arg_1 |tptp.'B_c_vec_b_c_vec_a_vec_fun$'|) (_arg_2 |tptp.'B_c_vec$'|)) |tptp.'B_c_vec_a_vec$'| (as |@_tptp.'B_c_vec_a_vec$'__0| |tptp.'B_c_vec_a_vec$'|)) % 1.64/1.87 (define-fun |tptp.'elt_set_plus$a'| ((_arg_1 |tptp.'B_c_vec_a_vec_a_vec$'|) (_arg_2 |tptp.'B_c_vec_a_vec_a_vec_set$'|)) |tptp.'B_c_vec_a_vec_a_vec_set$'| (as |@_tptp.'B_c_vec_a_vec_a_vec_set$'__0| |tptp.'B_c_vec_a_vec_a_vec_set$'|)) % 1.64/1.87 (define-fun |tptp.'member$g'| ((_arg_1 |tptp.'B_set$'|) (_arg_2 |tptp.'B_set_set$'|)) Bool false) % 1.64/1.87 (define-fun |tptp.'transpose_row$a'| ((_arg_1 |tptp.'B_c_vec_a_vec_a_vec$'|)) |tptp.'A_b_c_vec_a_vec_fun$'| (as |@_tptp.'A_b_c_vec_a_vec_fun$'__1| |tptp.'A_b_c_vec_a_vec_fun$'|)) % 1.64/1.87 (define-fun |tptp.'vec$'| ((_arg_1 |tptp.'B$'|)) |tptp.'B_a_vec$'| (as |@_tptp.'B_a_vec$'__0| |tptp.'B_a_vec$'|)) % 1.64/1.87 (define-fun |tptp.'vec_nth$h'| ((_arg_1 |tptp.'B_c_vec_a_vec_c_vec$'|) (_arg_2 |tptp.'C$'|)) |tptp.'B_c_vec_a_vec$'| (as |@_tptp.'B_c_vec_a_vec$'__0| |tptp.'B_c_vec_a_vec$'|)) % 1.64/1.87 (define-fun |tptp.'elt_set_times$d'| ((_arg_1 |tptp.'B_set$'|) (_arg_2 |tptp.'B_set_set$'|)) |tptp.'B_set_set$'| (as |@_tptp.'B_set_set$'__0| |tptp.'B_set_set$'|)) % 1.64/1.87 (define-fun |tptp.'fun_app$c'| ((_arg_1 |tptp.'C_b_fun$'|) (_arg_2 |tptp.'C$'|)) |tptp.'B$'| (as |@_tptp.'B$'__0| |tptp.'B$'|)) % 1.64/1.87 (define-fun |tptp.'fun_app$s'| ((_arg_1 |tptp.'B_c_vec_a_vec_a_vec_bool_fun$'|) (_arg_2 |tptp.'B_c_vec_a_vec_a_vec$'|)) Bool false) % 1.64/1.87 (define-fun |tptp.'interchange_columns$b'| ((_arg_1 |tptp.'B_c_vec_c_vec$'|) (_arg_2 |tptp.'C$'|) (_arg_3 |tptp.'C$'|)) |tptp.'B_c_vec_c_vec$'| (as |@_tptp.'B_c_vec_c_vec$'__0| |tptp.'B_c_vec_c_vec$'|)) % 1.64/1.87 (define-fun |tptp.'plus$i'| ((_arg_1 |tptp.'B_a_vec_set$'|) (_arg_2 |tptp.'B_a_vec_set$'|)) |tptp.'B_a_vec_set$'| (as |@_tptp.'B_a_vec_set$'__0| |tptp.'B_a_vec_set$'|)) % 1.64/1.87 (define-fun |tptp.'less_eq$'| ((_arg_1 |tptp.'B_c_vec_set$'|) (_arg_2 |tptp.'B_c_vec_set$'|)) Bool true) % 1.64/1.87 (define-fun |tptp.'fun_app$l'| ((_arg_1 |tptp.'B_b_c_vec_fun$'|) (_arg_2 |tptp.'B$'|)) |tptp.'B_c_vec$'| (as |@_tptp.'B_c_vec$'__0| |tptp.'B_c_vec$'|)) % 1.64/1.87 (define-fun |tptp.'plus$d'| ((_arg_1 |tptp.'B_a_vec$'|) (_arg_2 |tptp.'B_a_vec$'|)) |tptp.'B_a_vec$'| (as |@_tptp.'B_a_vec$'__0| |tptp.'B_a_vec$'|)) % 1.64/1.87 (define-fun |tptp.'columnvector_row$g'| ((_arg_1 |tptp.'B_a_vec_a_vec$'|) (_arg_2 |tptp.'A$'|)) |tptp.'B_a_vec_a_vec$'| (as |@_tptp.'B_a_vec_a_vec$'__0| |tptp.'B_a_vec_a_vec$'|)) % 1.64/1.87 (define-fun |tptp.'fun_app$v'| ((_arg_1 |tptp.'C_b_c_vec_bool_fun_fun$'|) (_arg_2 |tptp.'C$'|)) |tptp.'B_c_vec_bool_fun$'| (as |@_tptp.'B_c_vec_bool_fun$'__0| |tptp.'B_c_vec_bool_fun$'|)) % 1.64/1.87 (define-fun |tptp.'transpose_row$g'| ((_arg_1 |tptp.'B_a_vec_a_vec_a_vec$'|) (_arg_2 |tptp.'A$'|)) |tptp.'B_a_vec_a_vec$'| (as |@_tptp.'B_a_vec_a_vec$'__0| |tptp.'B_a_vec_a_vec$'|)) % 1.64/1.87 (define-fun |tptp.'vec_nth$i'| ((_arg_1 |tptp.'B_c_vec_c_vec_a_vec$'|) (_arg_2 |tptp.'A$'|)) |tptp.'B_c_vec_c_vec$'| (as |@_tptp.'B_c_vec_c_vec$'__0| |tptp.'B_c_vec_c_vec$'|)) % 1.64/1.87 (define-fun |tptp.'vector_scalar_mult$'| ((_arg_1 |tptp.'B_a_vec$'|) (_arg_2 |tptp.'B_a_vec_a_vec$'|)) |tptp.'B_a_vec_a_vec$'| (as |@_tptp.'B_a_vec_a_vec$'__0| |tptp.'B_a_vec_a_vec$'|)) % 1.64/1.87 (define-fun |tptp.'interchange_columns$e'| ((_arg_1 |tptp.'B_c_vec_a_vec$'|) (_arg_2 |tptp.'C$'|) (_arg_3 |tptp.'C$'|)) |tptp.'B_c_vec_a_vec$'| (as |@_tptp.'B_c_vec_a_vec$'__0| |tptp.'B_c_vec_a_vec$'|)) % 1.64/1.87 (define-fun |tptp.'columnvector_row$c'| ((_arg_1 |tptp.'B_c_vec$'|) (_arg_2 |tptp.'C$'|)) |tptp.'B_a_vec$'| (as |@_tptp.'B_a_vec$'__0| |tptp.'B_a_vec$'|)) % 1.64/1.87 (define-fun |tptp.'uu$'| ((_arg_1 |tptp.'B_c_vec_set$'|)) |tptp.'B_c_vec_bool_fun$'| (as |@_tptp.'B_c_vec_bool_fun$'__0| |tptp.'B_c_vec_bool_fun$'|)) % 1.64/1.87 (define-fun |tptp.'less_eq$a'| ((_arg_1 |tptp.'B_c_vec_a_vec_set$'|) (_arg_2 |tptp.'B_c_vec_a_vec_set$'|)) Bool true) % 1.64/1.87 (define-fun |tptp.'times$n'| ((_arg_1 |tptp.'B_c_vec_a_vec_set_set$'|) (_arg_2 |tptp.'B_c_vec_a_vec_set_set$'|)) |tptp.'B_c_vec_a_vec_set_set$'| (as |@_tptp.'B_c_vec_a_vec_set_set$'__0| |tptp.'B_c_vec_a_vec_set_set$'|)) % 1.64/1.87 (define-fun |tptp.'fun_app$b'| ((_arg_1 |tptp.'B_bool_fun$'|) (_arg_2 |tptp.'B$'|)) Bool false) % 1.64/1.87 (define-fun |tptp.'interchange_rows_row$a'| ((_arg_1 |tptp.'B_c_vec_a_vec_a_vec_a_vec$'|) (_arg_2 |tptp.'A$'|) (_arg_3 |tptp.'A$'|)) |tptp.'A_b_c_vec_a_vec_a_vec_fun$'| (as |@_tptp.'A_b_c_vec_a_vec_a_vec_fun$'__1| |tptp.'A_b_c_vec_a_vec_a_vec_fun$'|)) % 1.64/1.87 (define-fun |tptp.'interchange_columns_row$'| ((_arg_1 |tptp.'B_c_vec_c_vec$'|) (_arg_2 |tptp.'C$'|) (_arg_3 |tptp.'C$'|)) |tptp.'C_b_c_vec_fun$'| (as |@_tptp.'C_b_c_vec_fun$'__0| |tptp.'C_b_c_vec_fun$'|)) % 1.64/1.87 (define-fun |tptp.'columnvector_row$d'| ((_arg_1 |tptp.'B_a_vec$'|) (_arg_2 |tptp.'A$'|)) |tptp.'B_a_vec$'| (as |@_tptp.'B_a_vec$'__0| |tptp.'B_a_vec$'|)) % 1.64/1.87 (define-fun |tptp.'elt_set_plus$b'| ((_arg_1 |tptp.'B_c_vec_set$'|) (_arg_2 |tptp.'B_c_vec_set_set$'|)) |tptp.'B_c_vec_set_set$'| (as |@_tptp.'B_c_vec_set_set$'__0| |tptp.'B_c_vec_set_set$'|)) % 1.64/1.87 (define-fun |tptp.'fun_app$j'| ((_arg_1 |tptp.'A_b_c_vec_fun$'|) (_arg_2 |tptp.'A$'|)) |tptp.'B_c_vec$'| (as |@_tptp.'B_c_vec$'__0| |tptp.'B_c_vec$'|)) % 1.64/1.87 (define-fun |tptp.'vector_scalar_mult$f'| ((_arg_1 |tptp.'B$'|) (_arg_2 |tptp.'B_a_vec$'|)) |tptp.'B_a_vec$'| (as |@_tptp.'B_a_vec$'__0| |tptp.'B_a_vec$'|)) % 1.64/1.87 (define-fun |tptp.'plus$n'| ((_arg_1 |tptp.'B_c_vec_a_vec_set_set$'|) (_arg_2 |tptp.'B_c_vec_a_vec_set_set$'|)) |tptp.'B_c_vec_a_vec_set_set$'| (as |@_tptp.'B_c_vec_a_vec_set_set$'__0| |tptp.'B_c_vec_a_vec_set_set$'|)) % 1.64/1.87 (define-fun |tptp.'times$h'| ((_arg_1 |tptp.'B_c_vec_c_vec$'|) (_arg_2 |tptp.'B_c_vec_c_vec$'|)) |tptp.'B_c_vec_c_vec$'| (as |@_tptp.'B_c_vec_c_vec$'__0| |tptp.'B_c_vec_c_vec$'|)) % 1.64/1.87 (define-fun |tptp.'member$a'| ((_arg_1 |tptp.'B_c_vec$'|) (_arg_2 |tptp.'B_c_vec_set$'|)) Bool false) % 1.64/1.87 (define-fun |tptp.'fun_app$h'| ((_arg_1 |tptp.'A_b_a_vec_fun$'|) (_arg_2 |tptp.'A$'|)) |tptp.'B_a_vec$'| (as |@_tptp.'B_a_vec$'__0| |tptp.'B_a_vec$'|)) % 1.64/1.87 ) % 1.64/1.87 % SZS output end Model % 1.64/1.88 % cvc5 exiting %------------------------------------------------------------------------------