%------------------------------------------------------------------------------ % File : cvc5-SAT---1.3.4 % Problem : ITP397_10 : TPTP v9.2.1. Released v8.2.0. % Transfm : none % Format : tptp:raw % Command : /export/starexec/sandbox2/solver/bin/do_cvc5 /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % Computer : n017.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:28:00 AM UTC 2026 % Result : Satisfiable 136.14s 136.90s % Output : Model 136.14s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : ITP397_10 : TPTP v9.2.1. Released v8.2.0. % 0.12/0.13 % Command : /export/starexec/sandbox2/solver/bin/do_cvc5 /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % 0.17/0.34 % Computer : n017.cluster.edu % 0.17/0.34 % Model : x86_64 x86_64 % 0.17/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.17/0.34 % Memory : 8042.1875MB % 0.17/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.17/0.34 % CPULimit : 300 % 0.17/0.34 % WCLimit : 300 % 0.17/0.34 % DateTime : Tue Jun 2 05:06:16 EDT 2026 % 0.17/0.34 % CPUTime : % 0.43/0.68 %----Disproving TF0_NAR % 0.43/0.69 --- Run --finite-model-find --sort-inference --uf-ss-fair at 60... % 0.53/0.74 --- Run --mbqi at 45... % 45.73/45.93 --- Run --mbqi --mbqi-enum --mbqi-enum-choice-grammar --mbqi-enum-global-syms-grammar --no-cegqi --no-sygus-inst at 45... % 90.85/91.13 --- Run --full-saturate-quant at 45... % 136.10/136.32 --- Run --finite-model-find --fmf-bound --macros-quant at 60... % 136.14/136.90 % SZS status Satisfiable % 136.14/136.90 % SZS output start Model % 136.14/136.91 ( % 136.14/136.91 ; cardinality of $$unsorted is 1 % 136.14/136.91 ; rep: (as @$$unsorted_0 $$unsorted) % 136.14/136.91 ; cardinality of |tptp.'A_ell2_a_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$'| is 1 % 136.14/136.91 ; rep: (as |@_tptp.'A_ell2_a_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$'__0| |tptp.'A_ell2_a_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$'|) % 136.14/136.91 ; cardinality of |tptp.'A_ell2_a_ell2_cblinfun$'| is 1 % 136.14/136.91 ; rep: (as |@_tptp.'A_ell2_a_ell2_cblinfun$'__0| |tptp.'A_ell2_a_ell2_cblinfun$'|) % 136.14/136.91 ; cardinality of |tptp.'B_b_prod_ell2_b_b_prod_ell2_cblinfun_c_a_prod_ell2_c_a_prod_ell2_cblinfun_fun$'| is 1 % 136.14/136.91 ; rep: (as |@_tptp.'B_b_prod_ell2_b_b_prod_ell2_cblinfun_c_a_prod_ell2_c_a_prod_ell2_cblinfun_fun$'__0| |tptp.'B_b_prod_ell2_b_b_prod_ell2_cblinfun_c_a_prod_ell2_c_a_prod_ell2_cblinfun_fun$'|) % 136.14/136.91 ; cardinality of |tptp.'C_ell2_c_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$'| is 1 % 136.14/136.91 ; rep: (as |@_tptp.'C_ell2_c_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$'__0| |tptp.'C_ell2_c_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$'|) % 136.14/136.91 ; cardinality of |tptp.'A_b_prod_ell2_a_b_prod_ell2_cblinfun_c_a_prod_ell2_c_a_prod_ell2_cblinfun_fun$'| is 1 % 136.14/136.91 ; rep: (as |@_tptp.'A_b_prod_ell2_a_b_prod_ell2_cblinfun_c_a_prod_ell2_c_a_prod_ell2_cblinfun_fun$'__0| |tptp.'A_b_prod_ell2_a_b_prod_ell2_cblinfun_c_a_prod_ell2_c_a_prod_ell2_cblinfun_fun$'|) % 136.14/136.91 ; cardinality of |tptp.'B_ell2_b_ell2_cblinfun$'| is 1 % 136.14/136.91 ; rep: (as |@_tptp.'B_ell2_b_ell2_cblinfun$'__0| |tptp.'B_ell2_b_ell2_cblinfun$'|) % 136.14/136.91 ; cardinality of |tptp.'A_ell2_a_ell2_cblinfun_set_a_ell2_a_ell2_cblinfun_set_fun$'| is 1 % 136.14/136.91 ; rep: (as |@_tptp.'A_ell2_a_ell2_cblinfun_set_a_ell2_a_ell2_cblinfun_set_fun$'__0| |tptp.'A_ell2_a_ell2_cblinfun_set_a_ell2_a_ell2_cblinfun_set_fun$'|) % 136.14/136.91 ; cardinality of |tptp.'A_b_prod_ell2_a_b_prod_ell2_cblinfun_c_c_prod_ell2_c_c_prod_ell2_cblinfun_fun$'| is 1 % 136.14/136.91 ; rep: (as |@_tptp.'A_b_prod_ell2_a_b_prod_ell2_cblinfun_c_c_prod_ell2_c_c_prod_ell2_cblinfun_fun$'__0| |tptp.'A_b_prod_ell2_a_b_prod_ell2_cblinfun_c_c_prod_ell2_c_c_prod_ell2_cblinfun_fun$'|) % 136.14/136.91 ; cardinality of |tptp.'B_b_prod_ell2_b_b_prod_ell2_cblinfun_c_c_prod_ell2_c_c_prod_ell2_cblinfun_fun$'| is 1 % 136.14/136.91 ; rep: (as |@_tptp.'B_b_prod_ell2_b_b_prod_ell2_cblinfun_c_c_prod_ell2_c_c_prod_ell2_cblinfun_fun$'__0| |tptp.'B_b_prod_ell2_b_b_prod_ell2_cblinfun_c_c_prod_ell2_c_c_prod_ell2_cblinfun_fun$'|) % 136.14/136.91 ; cardinality of |tptp.'B_a_prod_ell2_b_a_prod_ell2_cblinfun_c_a_prod_ell2_c_a_prod_ell2_cblinfun_fun$'| is 1 % 136.14/136.91 ; rep: (as |@_tptp.'B_a_prod_ell2_b_a_prod_ell2_cblinfun_c_a_prod_ell2_c_a_prod_ell2_cblinfun_fun$'__0| |tptp.'B_a_prod_ell2_b_a_prod_ell2_cblinfun_c_a_prod_ell2_c_a_prod_ell2_cblinfun_fun$'|) % 136.14/136.91 ; cardinality of |tptp.'Nat_set_nat_fun$'| is 1 % 136.14/136.91 ; rep: (as |@_tptp.'Nat_set_nat_fun$'__0| |tptp.'Nat_set_nat_fun$'|) % 136.14/136.91 ; cardinality of |tptp.'B_ell2_b_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun_set$'| is 1 % 136.14/136.91 ; rep: (as |@_tptp.'B_ell2_b_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun_set$'__0| |tptp.'B_ell2_b_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun_set$'|) % 136.14/136.91 ; cardinality of |tptp.'A_b_prod_ell2_a_b_prod_ell2_cblinfun_set$'| is 1 % 136.14/136.91 ; rep: (as |@_tptp.'A_b_prod_ell2_a_b_prod_ell2_cblinfun_set$'__0| |tptp.'A_b_prod_ell2_a_b_prod_ell2_cblinfun_set$'|) % 136.14/136.91 ; cardinality of |tptp.'A_a_prod_ell2_a_a_prod_ell2_cblinfun_a_a_prod_ell2_a_a_prod_ell2_cblinfun_fun$'| is 1 % 136.14/136.91 ; rep: (as |@_tptp.'A_a_prod_ell2_a_a_prod_ell2_cblinfun_a_a_prod_ell2_a_a_prod_ell2_cblinfun_fun$'__0| |tptp.'A_a_prod_ell2_a_a_prod_ell2_cblinfun_a_a_prod_ell2_a_a_prod_ell2_cblinfun_fun$'|) % 136.14/136.91 ; cardinality of |tptp.'Nat_nat_fun_set$'| is 1 % 136.14/136.91 ; rep: (as |@_tptp.'Nat_nat_fun_set$'__0| |tptp.'Nat_nat_fun_set$'|) % 136.14/136.91 ; cardinality of |tptp.'A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun_set$'| is 1 % 136.14/136.91 ; rep: (as |@_tptp.'A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun_set$'__0| |tptp.'A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun_set$'|) % 136.14/136.91 ; cardinality of |tptp.'B_a_prod_ell2_b_a_prod_ell2_cblinfun_a_b_prod_ell2_a_b_prod_ell2_cblinfun_fun$'| is 1 % 136.14/136.91 ; rep: (as |@_tptp.'B_a_prod_ell2_b_a_prod_ell2_cblinfun_a_b_prod_ell2_a_b_prod_ell2_cblinfun_fun$'__0| |tptp.'B_a_prod_ell2_b_a_prod_ell2_cblinfun_a_b_prod_ell2_a_b_prod_ell2_cblinfun_fun$'|) % 136.14/136.91 ; cardinality of |tptp.'C_ell2_c_ell2_cblinfun$'| is 1 % 136.14/136.91 ; rep: (as |@_tptp.'C_ell2_c_ell2_cblinfun$'__0| |tptp.'C_ell2_c_ell2_cblinfun$'|) % 136.14/136.91 ; cardinality of |tptp.'C_ell2_c_ell2_cblinfun_bool_fun$'| is 1 % 136.14/136.91 ; rep: (as |@_tptp.'C_ell2_c_ell2_cblinfun_bool_fun$'__0| |tptp.'C_ell2_c_ell2_cblinfun_bool_fun$'|) % 136.14/136.91 ; cardinality of |tptp.'B_a_prod_ell2_b_a_prod_ell2_cblinfun_c_b_prod_ell2_c_b_prod_ell2_cblinfun_fun$'| is 1 % 136.14/136.91 ; rep: (as |@_tptp.'B_a_prod_ell2_b_a_prod_ell2_cblinfun_c_b_prod_ell2_c_b_prod_ell2_cblinfun_fun$'__0| |tptp.'B_a_prod_ell2_b_a_prod_ell2_cblinfun_c_b_prod_ell2_c_b_prod_ell2_cblinfun_fun$'|) % 136.14/136.91 ; cardinality of |tptp.'A_a_prod_ell2_a_a_prod_ell2_cblinfun_c_a_prod_ell2_c_a_prod_ell2_cblinfun_fun$'| is 1 % 136.14/136.91 ; rep: (as |@_tptp.'A_a_prod_ell2_a_a_prod_ell2_cblinfun_c_a_prod_ell2_c_a_prod_ell2_cblinfun_fun$'__0| |tptp.'A_a_prod_ell2_a_a_prod_ell2_cblinfun_c_a_prod_ell2_c_a_prod_ell2_cblinfun_fun$'|) % 136.14/136.91 ; cardinality of |tptp.'A_a_prod_ell2_a_a_prod_ell2_cblinfun_a_c_prod_ell2_a_c_prod_ell2_cblinfun_fun$'| is 1 % 136.14/136.91 ; rep: (as |@_tptp.'A_a_prod_ell2_a_a_prod_ell2_cblinfun_a_c_prod_ell2_a_c_prod_ell2_cblinfun_fun$'__0| |tptp.'A_a_prod_ell2_a_a_prod_ell2_cblinfun_a_c_prod_ell2_a_c_prod_ell2_cblinfun_fun$'|) % 136.14/136.91 ; cardinality of |tptp.'Nat_nat_fun_nat_nat_fun_fun$'| is 1 % 136.14/136.91 ; rep: (as |@_tptp.'Nat_nat_fun_nat_nat_fun_fun$'__0| |tptp.'Nat_nat_fun_nat_nat_fun_fun$'|) % 136.14/136.91 ; cardinality of |tptp.'C_c_prod_ell2_c_c_prod_ell2_cblinfun_a_b_prod_ell2_a_b_prod_ell2_cblinfun_fun$'| is 1 % 136.14/136.91 ; rep: (as |@_tptp.'C_c_prod_ell2_c_c_prod_ell2_cblinfun_a_b_prod_ell2_a_b_prod_ell2_cblinfun_fun$'__0| |tptp.'C_c_prod_ell2_c_c_prod_ell2_cblinfun_a_b_prod_ell2_a_b_prod_ell2_cblinfun_fun$'|) % 136.14/136.91 ; cardinality of |tptp.'Nat_nat_fun$'| is 1 % 136.14/136.91 ; rep: (as |@_tptp.'Nat_nat_fun$'__0| |tptp.'Nat_nat_fun$'|) % 136.14/136.91 ; cardinality of |tptp.'B_ell2_b_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$'| is 1 % 136.14/136.91 ; rep: (as |@_tptp.'B_ell2_b_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$'__0| |tptp.'B_ell2_b_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$'|) % 136.14/136.91 ; cardinality of |tptp.'B_a_prod_ell2_b_a_prod_ell2_cblinfun_a_c_prod_ell2_a_c_prod_ell2_cblinfun_fun$'| is 1 % 136.14/136.91 ; rep: (as |@_tptp.'B_a_prod_ell2_b_a_prod_ell2_cblinfun_a_c_prod_ell2_a_c_prod_ell2_cblinfun_fun$'__0| |tptp.'B_a_prod_ell2_b_a_prod_ell2_cblinfun_a_c_prod_ell2_a_c_prod_ell2_cblinfun_fun$'|) % 136.14/136.91 ; cardinality of |tptp.'B_ell2_b_ell2_cblinfun_set_b_ell2_b_ell2_cblinfun_fun$'| is 1 % 136.14/136.91 ; rep: (as |@_tptp.'B_ell2_b_ell2_cblinfun_set_b_ell2_b_ell2_cblinfun_fun$'__0| |tptp.'B_ell2_b_ell2_cblinfun_set_b_ell2_b_ell2_cblinfun_fun$'|) % 136.14/136.91 ; cardinality of |tptp.'A_b_prod_ell2_a_b_prod_ell2_cblinfun_c_b_prod_ell2_c_b_prod_ell2_cblinfun_fun$'| is 1 % 136.14/136.91 ; rep: (as |@_tptp.'A_b_prod_ell2_a_b_prod_ell2_cblinfun_c_b_prod_ell2_c_b_prod_ell2_cblinfun_fun$'__0| |tptp.'A_b_prod_ell2_a_b_prod_ell2_cblinfun_c_b_prod_ell2_c_b_prod_ell2_cblinfun_fun$'|) % 136.14/136.91 ; cardinality of |tptp.'Nat$'| is 1 % 136.14/136.91 ; rep: (as |@_tptp.'Nat$'__0| |tptp.'Nat$'|) % 136.14/136.91 ; cardinality of |tptp.'A_ell2_a_ell2_cblinfun_set_a_ell2_a_ell2_cblinfun_fun$'| is 1 % 136.14/136.91 ; rep: (as |@_tptp.'A_ell2_a_ell2_cblinfun_set_a_ell2_a_ell2_cblinfun_fun$'__0| |tptp.'A_ell2_a_ell2_cblinfun_set_a_ell2_a_ell2_cblinfun_fun$'|) % 136.14/136.91 ; cardinality of |tptp.'A_ell2_a_ell2_cblinfun_bool_fun$'| is 1 % 136.14/136.91 ; rep: (as |@_tptp.'A_ell2_a_ell2_cblinfun_bool_fun$'__0| |tptp.'A_ell2_a_ell2_cblinfun_bool_fun$'|) % 136.14/136.91 ; cardinality of |tptp.'C_c_prod_ell2_c_c_prod_ell2_cblinfun_b_a_prod_ell2_b_a_prod_ell2_cblinfun_fun$'| is 1 % 136.14/136.91 ; rep: (as |@_tptp.'C_c_prod_ell2_c_c_prod_ell2_cblinfun_b_a_prod_ell2_b_a_prod_ell2_cblinfun_fun$'__0| |tptp.'C_c_prod_ell2_c_c_prod_ell2_cblinfun_b_a_prod_ell2_b_a_prod_ell2_cblinfun_fun$'|) % 136.14/136.91 ; cardinality of |tptp.'B_b_prod_ell2_b_b_prod_ell2_cblinfun_b_b_prod_ell2_b_b_prod_ell2_cblinfun_fun$'| is 1 % 136.14/136.91 ; rep: (as |@_tptp.'B_b_prod_ell2_b_b_prod_ell2_cblinfun_b_b_prod_ell2_b_b_prod_ell2_cblinfun_fun$'__0| |tptp.'B_b_prod_ell2_b_b_prod_ell2_cblinfun_b_b_prod_ell2_b_b_prod_ell2_cblinfun_fun$'|) % 136.14/136.91 ; cardinality of |tptp.'B_a_prod_ell2_b_a_prod_ell2_cblinfun_c_c_prod_ell2_c_c_prod_ell2_cblinfun_fun$'| is 1 % 136.14/136.91 ; rep: (as |@_tptp.'B_a_prod_ell2_b_a_prod_ell2_cblinfun_c_c_prod_ell2_c_c_prod_ell2_cblinfun_fun$'__0| |tptp.'B_a_prod_ell2_b_a_prod_ell2_cblinfun_c_c_prod_ell2_c_c_prod_ell2_cblinfun_fun$'|) % 136.14/136.91 ; cardinality of |tptp.'A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$'| is 1 % 136.14/136.91 ; rep: (as |@_tptp.'A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$'__0| |tptp.'A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$'|) % 136.14/136.91 ; cardinality of |tptp.'A_a_prod_ell2_a_a_prod_ell2_cblinfun_c_c_prod_ell2_c_c_prod_ell2_cblinfun_fun$'| is 1 % 136.14/136.91 ; rep: (as |@_tptp.'A_a_prod_ell2_a_a_prod_ell2_cblinfun_c_c_prod_ell2_c_c_prod_ell2_cblinfun_fun$'__0| |tptp.'A_a_prod_ell2_a_a_prod_ell2_cblinfun_c_c_prod_ell2_c_c_prod_ell2_cblinfun_fun$'|) % 136.14/136.91 ; cardinality of |tptp.'B_ell2_b_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun_b_ell2_b_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun_fun$'| is 1 % 136.14/136.91 ; rep: (as |@_tptp.'B_ell2_b_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun_b_ell2_b_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun_fun$'__0| |tptp.'B_ell2_b_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun_b_ell2_b_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun_fun$'|) % 136.14/136.91 ; cardinality of |tptp.'B_ell2_b_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$'| is 1 % 136.14/136.91 ; rep: (as |@_tptp.'B_ell2_b_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$'__0| |tptp.'B_ell2_b_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$'|) % 136.14/136.91 ; cardinality of |tptp.'B_ell2_b_ell2_cblinfun_set$'| is 1 % 136.14/136.91 ; rep: (as |@_tptp.'B_ell2_b_ell2_cblinfun_set$'__0| |tptp.'B_ell2_b_ell2_cblinfun_set$'|) % 136.14/136.91 ; cardinality of |tptp.'A_a_prod_ell2_a_a_prod_ell2_cblinfun_c_b_prod_ell2_c_b_prod_ell2_cblinfun_fun$'| is 1 % 136.14/136.91 ; rep: (as |@_tptp.'A_a_prod_ell2_a_a_prod_ell2_cblinfun_c_b_prod_ell2_c_b_prod_ell2_cblinfun_fun$'__0| |tptp.'A_a_prod_ell2_a_a_prod_ell2_cblinfun_c_b_prod_ell2_c_b_prod_ell2_cblinfun_fun$'|) % 136.14/136.91 ; cardinality of |tptp.'A_ell2_a_ell2_cblinfun_set$'| is 1 % 136.14/136.91 ; rep: (as |@_tptp.'A_ell2_a_ell2_cblinfun_set$'__0| |tptp.'A_ell2_a_ell2_cblinfun_set$'|) % 136.14/136.91 ; cardinality of |tptp.'B_b_prod_ell2_b_b_prod_ell2_cblinfun_c_b_prod_ell2_c_b_prod_ell2_cblinfun_fun$'| is 1 % 136.14/136.91 ; rep: (as |@_tptp.'B_b_prod_ell2_b_b_prod_ell2_cblinfun_c_b_prod_ell2_c_b_prod_ell2_cblinfun_fun$'__0| |tptp.'B_b_prod_ell2_b_b_prod_ell2_cblinfun_c_b_prod_ell2_c_b_prod_ell2_cblinfun_fun$'|) % 136.14/136.91 ; cardinality of |tptp.'A_b_prod_ell2_a_b_prod_ell2_cblinfun_a_c_prod_ell2_a_c_prod_ell2_cblinfun_fun$'| is 1 % 136.14/136.91 ; rep: (as |@_tptp.'A_b_prod_ell2_a_b_prod_ell2_cblinfun_a_c_prod_ell2_a_c_prod_ell2_cblinfun_fun$'__0| |tptp.'A_b_prod_ell2_a_b_prod_ell2_cblinfun_a_c_prod_ell2_a_c_prod_ell2_cblinfun_fun$'|) % 136.14/136.91 ; cardinality of |tptp.'A_b_prod_ell2_a_b_prod_ell2_cblinfun_b_a_prod_ell2_b_a_prod_ell2_cblinfun_fun$'| is 1 % 136.14/136.91 ; rep: (as |@_tptp.'A_b_prod_ell2_a_b_prod_ell2_cblinfun_b_a_prod_ell2_b_a_prod_ell2_cblinfun_fun$'__0| |tptp.'A_b_prod_ell2_a_b_prod_ell2_cblinfun_b_a_prod_ell2_b_a_prod_ell2_cblinfun_fun$'|) % 136.14/136.91 ; cardinality of |tptp.'A_a_prod_ell2_a_a_prod_ell2_cblinfun_b_b_prod_ell2_b_b_prod_ell2_cblinfun_fun$'| is 1 % 136.14/136.91 ; rep: (as |@_tptp.'A_a_prod_ell2_a_a_prod_ell2_cblinfun_b_b_prod_ell2_b_b_prod_ell2_cblinfun_fun$'__0| |tptp.'A_a_prod_ell2_a_a_prod_ell2_cblinfun_b_b_prod_ell2_b_b_prod_ell2_cblinfun_fun$'|) % 136.14/136.91 ; cardinality of |tptp.'A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun_a_ell2_a_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun_fun$'| is 1 % 136.14/136.91 ; rep: (as |@_tptp.'A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun_a_ell2_a_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun_fun$'__0| |tptp.'A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun_a_ell2_a_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun_fun$'|) % 136.14/136.91 ; cardinality of |tptp.'B_b_prod_ell2_b_b_prod_ell2_cblinfun_a_a_prod_ell2_a_a_prod_ell2_cblinfun_fun$'| is 1 % 136.14/136.91 ; rep: (as |@_tptp.'B_b_prod_ell2_b_b_prod_ell2_cblinfun_a_a_prod_ell2_a_a_prod_ell2_cblinfun_fun$'__0| |tptp.'B_b_prod_ell2_b_b_prod_ell2_cblinfun_a_a_prod_ell2_a_a_prod_ell2_cblinfun_fun$'|) % 136.14/136.91 ; cardinality of |tptp.'C_c_prod_ell2_c_c_prod_ell2_cblinfun_a_a_prod_ell2_a_a_prod_ell2_cblinfun_fun$'| is 1 % 136.14/136.91 ; rep: (as |@_tptp.'C_c_prod_ell2_c_c_prod_ell2_cblinfun_a_a_prod_ell2_a_a_prod_ell2_cblinfun_fun$'__0| |tptp.'C_c_prod_ell2_c_c_prod_ell2_cblinfun_a_a_prod_ell2_a_a_prod_ell2_cblinfun_fun$'|) % 136.14/136.91 ; cardinality of |tptp.'A_c_prod_ell2_a_c_prod_ell2_cblinfun_b_a_prod_ell2_b_a_prod_ell2_cblinfun_fun$'| is 1 % 136.14/136.91 ; rep: (as |@_tptp.'A_c_prod_ell2_a_c_prod_ell2_cblinfun_b_a_prod_ell2_b_a_prod_ell2_cblinfun_fun$'__0| |tptp.'A_c_prod_ell2_a_c_prod_ell2_cblinfun_b_a_prod_ell2_b_a_prod_ell2_cblinfun_fun$'|) % 136.14/136.91 ; cardinality of |tptp.'C_ell2_c_ell2_cblinfun_set_c_ell2_c_ell2_cblinfun_fun$'| is 1 % 136.14/136.91 ; rep: (as |@_tptp.'C_ell2_c_ell2_cblinfun_set_c_ell2_c_ell2_cblinfun_fun$'__0| |tptp.'C_ell2_c_ell2_cblinfun_set_c_ell2_c_ell2_cblinfun_fun$'|) % 136.14/136.91 ; cardinality of |tptp.'B_ell2_b_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$'| is 1 % 136.14/136.91 ; rep: (as |@_tptp.'B_ell2_b_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$'__0| |tptp.'B_ell2_b_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$'|) % 136.14/136.91 ; cardinality of |tptp.'B_ell2_b_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun_b_ell2_b_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun_fun$'| is 1 % 136.14/136.91 ; rep: (as |@_tptp.'B_ell2_b_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun_b_ell2_b_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun_fun$'__0| |tptp.'B_ell2_b_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun_b_ell2_b_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun_fun$'|) % 136.14/136.91 ; cardinality of |tptp.'C_c_prod_ell2_c_c_prod_ell2_cblinfun_b_b_prod_ell2_b_b_prod_ell2_cblinfun_fun$'| is 1 % 136.14/136.91 ; rep: (as |@_tptp.'C_c_prod_ell2_c_c_prod_ell2_cblinfun_b_b_prod_ell2_b_b_prod_ell2_cblinfun_fun$'__0| |tptp.'C_c_prod_ell2_c_c_prod_ell2_cblinfun_b_b_prod_ell2_b_b_prod_ell2_cblinfun_fun$'|) % 136.14/136.91 ; cardinality of |tptp.'B_b_prod_ell2_b_b_prod_ell2_cblinfun_set$'| is 1 % 136.14/136.91 ; rep: (as |@_tptp.'B_b_prod_ell2_b_b_prod_ell2_cblinfun_set$'__0| |tptp.'B_b_prod_ell2_b_b_prod_ell2_cblinfun_set$'|) % 136.14/136.91 ; cardinality of |tptp.'B_a_prod_ell2_b_a_prod_ell2_cblinfun_set$'| is 1 % 136.14/136.91 ; rep: (as |@_tptp.'B_a_prod_ell2_b_a_prod_ell2_cblinfun_set$'__0| |tptp.'B_a_prod_ell2_b_a_prod_ell2_cblinfun_set$'|) % 136.14/136.91 ; cardinality of |tptp.'A_a_prod_ell2_a_a_prod_ell2_cblinfun_set$'| is 1 % 136.14/136.91 ; rep: (as |@_tptp.'A_a_prod_ell2_a_a_prod_ell2_cblinfun_set$'__0| |tptp.'A_a_prod_ell2_a_a_prod_ell2_cblinfun_set$'|) % 136.14/136.91 ; cardinality of |tptp.'C_a_prod_ell2_c_a_prod_ell2_cblinfun_b_b_prod_ell2_b_b_prod_ell2_cblinfun_fun$'| is 1 % 136.14/136.91 ; rep: (as |@_tptp.'C_a_prod_ell2_c_a_prod_ell2_cblinfun_b_b_prod_ell2_b_b_prod_ell2_cblinfun_fun$'__0| |tptp.'C_a_prod_ell2_c_a_prod_ell2_cblinfun_b_b_prod_ell2_b_b_prod_ell2_cblinfun_fun$'|) % 136.14/136.91 ; cardinality of |tptp.'A_ell2_a_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$'| is 1 % 136.14/136.91 ; rep: (as |@_tptp.'A_ell2_a_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$'__0| |tptp.'A_ell2_a_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$'|) % 136.14/136.91 ; cardinality of |tptp.'B_b_prod_ell2_b_b_prod_ell2_cblinfun_a_c_prod_ell2_a_c_prod_ell2_cblinfun_fun$'| is 1 % 136.14/136.91 ; rep: (as |@_tptp.'B_b_prod_ell2_b_b_prod_ell2_cblinfun_a_c_prod_ell2_a_c_prod_ell2_cblinfun_fun$'__0| |tptp.'B_b_prod_ell2_b_b_prod_ell2_cblinfun_a_c_prod_ell2_a_c_prod_ell2_cblinfun_fun$'|) % 136.14/136.91 ; cardinality of |tptp.'B_ell2_b_ell2_cblinfun_bool_fun$'| is 1 % 136.14/136.91 ; rep: (as |@_tptp.'B_ell2_b_ell2_cblinfun_bool_fun$'__0| |tptp.'B_ell2_b_ell2_cblinfun_bool_fun$'|) % 136.14/136.91 ; cardinality of |tptp.'B_a_prod_ell2_b_a_prod_ell2_cblinfun_b_a_prod_ell2_b_a_prod_ell2_cblinfun_fun$'| is 1 % 136.14/136.91 ; rep: (as |@_tptp.'B_a_prod_ell2_b_a_prod_ell2_cblinfun_b_a_prod_ell2_b_a_prod_ell2_cblinfun_fun$'__0| |tptp.'B_a_prod_ell2_b_a_prod_ell2_cblinfun_b_a_prod_ell2_b_a_prod_ell2_cblinfun_fun$'|) % 136.14/136.91 ; cardinality of |tptp.'Nat_set$'| is 1 % 136.14/136.91 ; rep: (as |@_tptp.'Nat_set$'__0| |tptp.'Nat_set$'|) % 136.14/136.91 ; cardinality of |tptp.'A_b_prod_ell2_a_b_prod_ell2_cblinfun_a_b_prod_ell2_a_b_prod_ell2_cblinfun_fun$'| is 1 % 136.14/136.91 ; rep: (as |@_tptp.'A_b_prod_ell2_a_b_prod_ell2_cblinfun_a_b_prod_ell2_a_b_prod_ell2_cblinfun_fun$'__0| |tptp.'A_b_prod_ell2_a_b_prod_ell2_cblinfun_a_b_prod_ell2_a_b_prod_ell2_cblinfun_fun$'|) % 136.14/136.91 ; cardinality of |tptp.'C_ell2_c_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$'| is 1 % 136.14/136.91 ; rep: (as |@_tptp.'C_ell2_c_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$'__0| |tptp.'C_ell2_c_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$'|) % 136.14/136.91 ; cardinality of |tptp.'C_ell2_c_ell2_cblinfun_set$'| is 1 % 136.14/136.91 ; rep: (as |@_tptp.'C_ell2_c_ell2_cblinfun_set$'__0| |tptp.'C_ell2_c_ell2_cblinfun_set$'|) % 136.14/136.91 ; cardinality of |tptp.'C_a_prod_ell2_c_a_prod_ell2_cblinfun_a_b_prod_ell2_a_b_prod_ell2_cblinfun_fun$'| is 1 % 136.14/136.91 ; rep: (as |@_tptp.'C_a_prod_ell2_c_a_prod_ell2_cblinfun_a_b_prod_ell2_a_b_prod_ell2_cblinfun_fun$'__0| |tptp.'C_a_prod_ell2_c_a_prod_ell2_cblinfun_a_b_prod_ell2_a_b_prod_ell2_cblinfun_fun$'|) % 136.14/136.91 ; cardinality of |tptp.'A_c_prod_ell2_a_c_prod_ell2_cblinfun_b_b_prod_ell2_b_b_prod_ell2_cblinfun_fun$'| is 1 % 136.14/136.91 ; rep: (as |@_tptp.'A_c_prod_ell2_a_c_prod_ell2_cblinfun_b_b_prod_ell2_b_b_prod_ell2_cblinfun_fun$'__0| |tptp.'A_c_prod_ell2_a_c_prod_ell2_cblinfun_b_b_prod_ell2_b_b_prod_ell2_cblinfun_fun$'|) % 136.14/136.91 ; cardinality of |tptp.'B_ell2_b_ell2_cblinfun_set_b_ell2_b_ell2_cblinfun_set_fun$'| is 1 % 136.14/136.91 ; rep: (as |@_tptp.'B_ell2_b_ell2_cblinfun_set_b_ell2_b_ell2_cblinfun_set_fun$'__0| |tptp.'B_ell2_b_ell2_cblinfun_set_b_ell2_b_ell2_cblinfun_set_fun$'|) % 136.14/136.91 ; cardinality of |tptp.'C_ell2_c_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$'| is 1 % 136.14/136.91 ; rep: (as |@_tptp.'C_ell2_c_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$'__0| |tptp.'C_ell2_c_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$'|) % 136.14/136.91 (define-fun |tptp.'register$k'| (($x1 |tptp.'B_b_prod_ell2_b_b_prod_ell2_cblinfun_c_a_prod_ell2_c_a_prod_ell2_cblinfun_fun$'|)) Bool true) % 136.14/136.91 (define-fun |tptp.'register$j'| (($x1 |tptp.'B_a_prod_ell2_b_a_prod_ell2_cblinfun_c_c_prod_ell2_c_c_prod_ell2_cblinfun_fun$'|)) Bool true) % 136.14/136.91 (define-fun |tptp.'top$i'| () |tptp.'C_ell2_c_ell2_cblinfun_bool_fun$'| (as |@_tptp.'C_ell2_c_ell2_cblinfun_bool_fun$'__0| |tptp.'C_ell2_c_ell2_cblinfun_bool_fun$'|)) % 136.14/136.91 (define-fun |tptp.'clinear$g'| (($x1 |tptp.'C_ell2_c_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$'|)) Bool true) % 136.14/136.91 (define-fun |tptp.'register_tensor$v'| (($x1 |tptp.'B_ell2_b_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$'|) ($x2 |tptp.'A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$'|)) |tptp.'B_a_prod_ell2_b_a_prod_ell2_cblinfun_c_b_prod_ell2_c_b_prod_ell2_cblinfun_fun$'| (as |@_tptp.'B_a_prod_ell2_b_a_prod_ell2_cblinfun_c_b_prod_ell2_c_b_prod_ell2_cblinfun_fun$'__0| |tptp.'B_a_prod_ell2_b_a_prod_ell2_cblinfun_c_b_prod_ell2_c_b_prod_ell2_cblinfun_fun$'|)) % 136.14/136.91 (define-fun |tptp.'image$b'| (($x1 |tptp.'C_ell2_c_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$'|) ($x2 |tptp.'C_ell2_c_ell2_cblinfun_set$'|)) |tptp.'C_ell2_c_ell2_cblinfun_set$'| (as |@_tptp.'C_ell2_c_ell2_cblinfun_set$'__0| |tptp.'C_ell2_c_ell2_cblinfun_set$'|)) % 136.14/136.91 (define-fun |tptp.'inv_into$n'| (($x1 |tptp.'A_b_prod_ell2_a_b_prod_ell2_cblinfun_set$'|) ($x2 |tptp.'A_b_prod_ell2_a_b_prod_ell2_cblinfun_c_a_prod_ell2_c_a_prod_ell2_cblinfun_fun$'|)) |tptp.'C_a_prod_ell2_c_a_prod_ell2_cblinfun_a_b_prod_ell2_a_b_prod_ell2_cblinfun_fun$'| (as |@_tptp.'C_a_prod_ell2_c_a_prod_ell2_cblinfun_a_b_prod_ell2_a_b_prod_ell2_cblinfun_fun$'__0| |tptp.'C_a_prod_ell2_c_a_prod_ell2_cblinfun_a_b_prod_ell2_a_b_prod_ell2_cblinfun_fun$'|)) % 136.14/136.91 (define-fun |tptp.'comp$af'| (($x1 |tptp.'A_a_prod_ell2_a_a_prod_ell2_cblinfun_c_c_prod_ell2_c_c_prod_ell2_cblinfun_fun$'|) ($x2 |tptp.'B_b_prod_ell2_b_b_prod_ell2_cblinfun_a_a_prod_ell2_a_a_prod_ell2_cblinfun_fun$'|)) |tptp.'B_b_prod_ell2_b_b_prod_ell2_cblinfun_c_c_prod_ell2_c_c_prod_ell2_cblinfun_fun$'| (as |@_tptp.'B_b_prod_ell2_b_b_prod_ell2_cblinfun_c_c_prod_ell2_c_c_prod_ell2_cblinfun_fun$'__0| |tptp.'B_b_prod_ell2_b_b_prod_ell2_cblinfun_c_c_prod_ell2_c_c_prod_ell2_cblinfun_fun$'|)) % 136.14/136.91 (define-fun |tptp.'inv_into$d'| (($x1 |tptp.'Nat_set$'|) ($x2 |tptp.'Nat_nat_fun$'|)) |tptp.'Nat_nat_fun$'| (as |@_tptp.'Nat_nat_fun$'__0| |tptp.'Nat_nat_fun$'|)) % 136.14/136.91 (define-fun |tptp.'image$'| (($x1 |tptp.'A_ell2_a_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$'|) ($x2 |tptp.'A_ell2_a_ell2_cblinfun_set$'|)) |tptp.'C_ell2_c_ell2_cblinfun_set$'| (as |@_tptp.'C_ell2_c_ell2_cblinfun_set$'__0| |tptp.'C_ell2_c_ell2_cblinfun_set$'|)) % 136.14/136.91 (define-fun |tptp.'register_tensor$f'| (($x1 |tptp.'B_ell2_b_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$'|) ($x2 |tptp.'B_ell2_b_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$'|)) |tptp.'B_b_prod_ell2_b_b_prod_ell2_cblinfun_c_c_prod_ell2_c_c_prod_ell2_cblinfun_fun$'| (as |@_tptp.'B_b_prod_ell2_b_b_prod_ell2_cblinfun_c_c_prod_ell2_c_c_prod_ell2_cblinfun_fun$'__0| |tptp.'B_b_prod_ell2_b_b_prod_ell2_cblinfun_c_c_prod_ell2_c_c_prod_ell2_cblinfun_fun$'|)) % 136.14/136.91 (define-fun |tptp.'inv_into$'| (($x1 |tptp.'A_ell2_a_ell2_cblinfun_set$'|) ($x2 |tptp.'A_ell2_a_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$'|)) |tptp.'C_ell2_c_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$'| (as |@_tptp.'C_ell2_c_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$'__0| |tptp.'C_ell2_c_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$'|)) % 136.14/136.91 (define-fun |tptp.'fun_app$o'| (($x1 |tptp.'A_ell2_a_ell2_cblinfun_set_a_ell2_a_ell2_cblinfun_set_fun$'|) ($x2 |tptp.'A_ell2_a_ell2_cblinfun_set$'|)) |tptp.'A_ell2_a_ell2_cblinfun_set$'| (as |@_tptp.'A_ell2_a_ell2_cblinfun_set$'__0| |tptp.'A_ell2_a_ell2_cblinfun_set$'|)) % 136.14/136.91 (define-fun |tptp.'fun_app$q'| (($x1 |tptp.'A_ell2_a_ell2_cblinfun_bool_fun$'|) ($x2 |tptp.'A_ell2_a_ell2_cblinfun$'|)) Bool true) % 136.14/136.91 (define-fun |tptp.'fun_app$k'| (($x1 |tptp.'Nat_nat_fun_nat_nat_fun_fun$'|) ($x2 |tptp.'Nat_nat_fun$'|)) |tptp.'Nat_nat_fun$'| (as |@_tptp.'Nat_nat_fun$'__0| |tptp.'Nat_nat_fun$'|)) % 136.14/136.91 (define-fun |tptp.'inj_on$'| (($x1 |tptp.'A_ell2_a_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$'|) ($x2 |tptp.'A_ell2_a_ell2_cblinfun_set$'|)) Bool true) % 136.14/136.91 (define-fun |tptp.'register$n'| (($x1 |tptp.'A_a_prod_ell2_a_a_prod_ell2_cblinfun_c_c_prod_ell2_c_c_prod_ell2_cblinfun_fun$'|)) Bool true) % 136.14/136.91 (define-fun |tptp.'inv_into$b'| (($x1 |tptp.'A_ell2_a_ell2_cblinfun_set$'|) ($x2 |tptp.'A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$'|)) |tptp.'B_ell2_b_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$'| (as |@_tptp.'B_ell2_b_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$'__0| |tptp.'B_ell2_b_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$'|)) % 136.14/136.91 (define-fun |tptp.'fun_app$b'| (($x1 |tptp.'B_ell2_b_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$'|) ($x2 |tptp.'B_ell2_b_ell2_cblinfun$'|)) |tptp.'C_ell2_c_ell2_cblinfun$'| (as |@_tptp.'C_ell2_c_ell2_cblinfun$'__0| |tptp.'C_ell2_c_ell2_cblinfun$'|)) % 136.14/136.91 (define-fun |tptp.'register_tensor$h'| (($x1 |tptp.'A_ell2_a_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$'|) ($x2 |tptp.'B_ell2_b_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$'|)) |tptp.'A_b_prod_ell2_a_b_prod_ell2_cblinfun_c_a_prod_ell2_c_a_prod_ell2_cblinfun_fun$'| (as |@_tptp.'A_b_prod_ell2_a_b_prod_ell2_cblinfun_c_a_prod_ell2_c_a_prod_ell2_cblinfun_fun$'__0| |tptp.'A_b_prod_ell2_a_b_prod_ell2_cblinfun_c_a_prod_ell2_c_a_prod_ell2_cblinfun_fun$'|)) % 136.14/136.91 (define-fun |tptp.'image$h'| (($x1 |tptp.'C_ell2_c_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$'|) ($x2 |tptp.'C_ell2_c_ell2_cblinfun_set$'|)) |tptp.'A_ell2_a_ell2_cblinfun_set$'| (as |@_tptp.'A_ell2_a_ell2_cblinfun_set$'__0| |tptp.'A_ell2_a_ell2_cblinfun_set$'|)) % 136.14/136.91 (define-fun |tptp.'top$d'| () |tptp.'B_ell2_b_ell2_cblinfun_bool_fun$'| (as |@_tptp.'B_ell2_b_ell2_cblinfun_bool_fun$'__0| |tptp.'B_ell2_b_ell2_cblinfun_bool_fun$'|)) % 136.14/136.91 (define-fun |tptp.'comp$h'| (($x1 |tptp.'B_ell2_b_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$'|) ($x2 |tptp.'B_ell2_b_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$'|)) |tptp.'B_ell2_b_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$'| (as |@_tptp.'B_ell2_b_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$'__0| |tptp.'B_ell2_b_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$'|)) % 136.14/136.91 (define-fun |tptp.'comp$p'| (($x1 |tptp.'A_ell2_a_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$'|) ($x2 |tptp.'A_ell2_a_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$'|)) |tptp.'A_ell2_a_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$'| (as |@_tptp.'A_ell2_a_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$'__0| |tptp.'A_ell2_a_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$'|)) % 136.14/136.91 (define-fun |tptp.'inv_into$g'| (($x1 |tptp.'B_ell2_b_ell2_cblinfun_set$'|) ($x2 |tptp.'B_ell2_b_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$'|)) |tptp.'B_ell2_b_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$'| (as |@_tptp.'B_ell2_b_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$'__0| |tptp.'B_ell2_b_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$'|)) % 136.14/136.91 (define-fun |tptp.'inv_into$f'| (($x1 |tptp.'C_ell2_c_ell2_cblinfun_set$'|) ($x2 |tptp.'C_ell2_c_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$'|)) |tptp.'A_ell2_a_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$'| (as |@_tptp.'A_ell2_a_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$'__0| |tptp.'A_ell2_a_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$'|)) % 136.14/136.91 (define-fun |tptp.'f$'| () |tptp.'A_ell2_a_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$'| (as |@_tptp.'A_ell2_a_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$'__0| |tptp.'A_ell2_a_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$'|)) % 136.14/136.91 (define-fun |tptp.'inj_on$d'| (($x1 |tptp.'C_ell2_c_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$'|) ($x2 |tptp.'C_ell2_c_ell2_cblinfun_set$'|)) Bool true) % 136.14/136.91 (define-fun |tptp.'register_tensor$e'| (($x1 |tptp.'C_ell2_c_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$'|) ($x2 |tptp.'C_ell2_c_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$'|)) |tptp.'C_c_prod_ell2_c_c_prod_ell2_cblinfun_b_a_prod_ell2_b_a_prod_ell2_cblinfun_fun$'| (as |@_tptp.'C_c_prod_ell2_c_c_prod_ell2_cblinfun_b_a_prod_ell2_b_a_prod_ell2_cblinfun_fun$'__0| |tptp.'C_c_prod_ell2_c_c_prod_ell2_cblinfun_b_a_prod_ell2_b_a_prod_ell2_cblinfun_fun$'|)) % 136.14/136.91 (define-fun |tptp.'member$a'| (($x1 |tptp.'A_ell2_a_ell2_cblinfun$'|) ($x2 |tptp.'A_ell2_a_ell2_cblinfun_set$'|)) Bool true) % 136.14/136.91 (define-fun |tptp.'register_tensor$d'| (($x1 |tptp.'B_ell2_b_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$'|) ($x2 |tptp.'A_ell2_a_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$'|)) |tptp.'B_a_prod_ell2_b_a_prod_ell2_cblinfun_c_c_prod_ell2_c_c_prod_ell2_cblinfun_fun$'| (as |@_tptp.'B_a_prod_ell2_b_a_prod_ell2_cblinfun_c_c_prod_ell2_c_c_prod_ell2_cblinfun_fun$'__0| |tptp.'B_a_prod_ell2_b_a_prod_ell2_cblinfun_c_c_prod_ell2_c_c_prod_ell2_cblinfun_fun$'|)) % 136.14/136.91 (define-fun |tptp.'comp$e'| (($x1 |tptp.'C_ell2_c_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$'|) ($x2 |tptp.'A_ell2_a_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$'|)) |tptp.'A_ell2_a_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$'| (as |@_tptp.'A_ell2_a_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$'__0| |tptp.'A_ell2_a_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$'|)) % 136.14/136.91 (define-fun |tptp.'iso_register$h'| (($x1 |tptp.'B_b_prod_ell2_b_b_prod_ell2_cblinfun_a_a_prod_ell2_a_a_prod_ell2_cblinfun_fun$'|)) Bool true) % 136.14/136.91 (define-fun |tptp.'clinear$b'| (($x1 |tptp.'B_ell2_b_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$'|)) Bool true) % 136.14/136.91 (define-fun |tptp.'inv_into$e'| (($x1 |tptp.'C_ell2_c_ell2_cblinfun_set$'|) ($x2 |tptp.'C_ell2_c_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$'|)) |tptp.'B_ell2_b_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$'| (as |@_tptp.'B_ell2_b_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$'__0| |tptp.'B_ell2_b_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$'|)) % 136.14/136.91 (define-fun |tptp.'iso_register$d'| (($x1 |tptp.'C_ell2_c_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$'|)) Bool false) % 136.14/136.91 (define-fun |tptp.'iso_register$'| (($x1 |tptp.'B_ell2_b_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$'|)) Bool true) % 136.14/136.91 (define-fun |tptp.'inj_on$a'| (($x1 |tptp.'B_ell2_b_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$'|) ($x2 |tptp.'B_ell2_b_ell2_cblinfun_set$'|)) Bool true) % 136.14/136.91 (define-fun |tptp.'comp$ae'| (($x1 |tptp.'A_b_prod_ell2_a_b_prod_ell2_cblinfun_c_c_prod_ell2_c_c_prod_ell2_cblinfun_fun$'|) ($x2 |tptp.'B_a_prod_ell2_b_a_prod_ell2_cblinfun_a_b_prod_ell2_a_b_prod_ell2_cblinfun_fun$'|)) |tptp.'B_a_prod_ell2_b_a_prod_ell2_cblinfun_c_c_prod_ell2_c_c_prod_ell2_cblinfun_fun$'| (as |@_tptp.'B_a_prod_ell2_b_a_prod_ell2_cblinfun_c_c_prod_ell2_c_c_prod_ell2_cblinfun_fun$'__0| |tptp.'B_a_prod_ell2_b_a_prod_ell2_cblinfun_c_c_prod_ell2_c_c_prod_ell2_cblinfun_fun$'|)) % 136.14/136.91 (define-fun |tptp.'fun_app$l'| (($x1 |tptp.'C_ell2_c_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$'|) ($x2 |tptp.'C_ell2_c_ell2_cblinfun$'|)) |tptp.'A_ell2_a_ell2_cblinfun$'| (as |@_tptp.'A_ell2_a_ell2_cblinfun$'__0| |tptp.'A_ell2_a_ell2_cblinfun$'|)) % 136.14/136.91 (define-fun |tptp.'top$c'| () |tptp.'A_ell2_a_ell2_cblinfun_bool_fun$'| (as |@_tptp.'A_ell2_a_ell2_cblinfun_bool_fun$'__0| |tptp.'A_ell2_a_ell2_cblinfun_bool_fun$'|)) % 136.14/136.91 (define-fun |tptp.'inj_on$m'| (($x1 |tptp.'C_ell2_c_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$'|) ($x2 |tptp.'C_ell2_c_ell2_cblinfun_set$'|)) Bool true) % 136.14/136.91 (define-fun |tptp.'fun_app$t'| (($x1 |tptp.'A_ell2_a_ell2_cblinfun_set_a_ell2_a_ell2_cblinfun_fun$'|) ($x2 |tptp.'A_ell2_a_ell2_cblinfun_set$'|)) |tptp.'A_ell2_a_ell2_cblinfun$'| (as |@_tptp.'A_ell2_a_ell2_cblinfun$'__0| |tptp.'A_ell2_a_ell2_cblinfun$'|)) % 136.14/136.91 (define-fun |tptp.'register_tensor$u'| ((_arg_1 |tptp.'A_ell2_a_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$'|) (_arg_2 |tptp.'A_ell2_a_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$'|)) |tptp.'A_a_prod_ell2_a_a_prod_ell2_cblinfun_a_a_prod_ell2_a_a_prod_ell2_cblinfun_fun$'| (as |@_tptp.'A_a_prod_ell2_a_a_prod_ell2_cblinfun_a_a_prod_ell2_a_a_prod_ell2_cblinfun_fun$'__0| |tptp.'A_a_prod_ell2_a_a_prod_ell2_cblinfun_a_a_prod_ell2_a_a_prod_ell2_cblinfun_fun$'|)) % 136.14/136.91 (define-fun |tptp.'image$a'| (($x1 |tptp.'B_ell2_b_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$'|) ($x2 |tptp.'B_ell2_b_ell2_cblinfun_set$'|)) |tptp.'C_ell2_c_ell2_cblinfun_set$'| (as |@_tptp.'C_ell2_c_ell2_cblinfun_set$'__0| |tptp.'C_ell2_c_ell2_cblinfun_set$'|)) % 136.14/136.91 (define-fun |tptp.'comp$j'| (($x1 |tptp.'B_ell2_b_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$'|) ($x2 |tptp.'B_ell2_b_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$'|)) |tptp.'B_ell2_b_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$'| (as |@_tptp.'B_ell2_b_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$'__0| |tptp.'B_ell2_b_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$'|)) % 136.14/136.91 (define-fun |tptp.'inj_on$j'| (($x1 |tptp.'B_ell2_b_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun_b_ell2_b_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun_fun$'|) ($x2 |tptp.'B_ell2_b_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun_set$'|)) Bool true) % 136.14/136.91 (define-fun |tptp.'fun_app$h'| (($x1 |tptp.'A_ell2_a_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$'|) ($x2 |tptp.'A_ell2_a_ell2_cblinfun$'|)) |tptp.'A_ell2_a_ell2_cblinfun$'| (as |@_tptp.'A_ell2_a_ell2_cblinfun$'__0| |tptp.'A_ell2_a_ell2_cblinfun$'|)) % 136.14/136.91 (define-fun |tptp.'member$b'| (($x1 |tptp.'B_ell2_b_ell2_cblinfun$'|) ($x2 |tptp.'B_ell2_b_ell2_cblinfun_set$'|)) Bool true) % 136.14/136.91 (define-fun |tptp.'register$q'| (($x1 |tptp.'B_b_prod_ell2_b_b_prod_ell2_cblinfun_a_c_prod_ell2_a_c_prod_ell2_cblinfun_fun$'|)) Bool true) % 136.14/136.91 (define-fun |tptp.'register_tensor$m'| (($x1 |tptp.'A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$'|) ($x2 |tptp.'C_ell2_c_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$'|)) |tptp.'A_c_prod_ell2_a_c_prod_ell2_cblinfun_b_a_prod_ell2_b_a_prod_ell2_cblinfun_fun$'| (as |@_tptp.'A_c_prod_ell2_a_c_prod_ell2_cblinfun_b_a_prod_ell2_b_a_prod_ell2_cblinfun_fun$'__0| |tptp.'A_c_prod_ell2_a_c_prod_ell2_cblinfun_b_a_prod_ell2_b_a_prod_ell2_cblinfun_fun$'|)) % 136.14/136.91 (define-fun |tptp.'inj_on$e'| (($x1 |tptp.'B_ell2_b_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$'|) ($x2 |tptp.'B_ell2_b_ell2_cblinfun_set$'|)) Bool true) % 136.14/136.91 (define-fun |tptp.'collect$'| (($x1 |tptp.'C_ell2_c_ell2_cblinfun_bool_fun$'|)) |tptp.'C_ell2_c_ell2_cblinfun_set$'| (as |@_tptp.'C_ell2_c_ell2_cblinfun_set$'__0| |tptp.'C_ell2_c_ell2_cblinfun_set$'|)) % 136.14/136.91 (define-fun |tptp.'register_tensor$b'| (($x1 |tptp.'A_ell2_a_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$'|) ($x2 |tptp.'B_ell2_b_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$'|)) |tptp.'A_b_prod_ell2_a_b_prod_ell2_cblinfun_c_c_prod_ell2_c_c_prod_ell2_cblinfun_fun$'| (as |@_tptp.'A_b_prod_ell2_a_b_prod_ell2_cblinfun_c_c_prod_ell2_c_c_prod_ell2_cblinfun_fun$'__0| |tptp.'A_b_prod_ell2_a_b_prod_ell2_cblinfun_c_c_prod_ell2_c_c_prod_ell2_cblinfun_fun$'|)) % 136.14/136.91 (define-fun |tptp.'iso_register$f'| (($x1 |tptp.'B_ell2_b_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$'|)) Bool true) % 136.14/136.91 (define-fun |tptp.'id$a'| () |tptp.'A_ell2_a_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$'| (as |@_tptp.'A_ell2_a_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$'__0| |tptp.'A_ell2_a_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$'|)) % 136.14/136.91 (define-fun |tptp.'register_tensor$a'| (($x1 |tptp.'C_ell2_c_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$'|) ($x2 |tptp.'C_ell2_c_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$'|)) |tptp.'C_c_prod_ell2_c_c_prod_ell2_cblinfun_a_a_prod_ell2_a_a_prod_ell2_cblinfun_fun$'| (as |@_tptp.'C_c_prod_ell2_c_c_prod_ell2_cblinfun_a_a_prod_ell2_a_a_prod_ell2_cblinfun_fun$'__0| |tptp.'C_c_prod_ell2_c_c_prod_ell2_cblinfun_a_a_prod_ell2_a_a_prod_ell2_cblinfun_fun$'|)) % 136.14/136.91 (define-fun |tptp.'id$g'| () |tptp.'A_b_prod_ell2_a_b_prod_ell2_cblinfun_a_b_prod_ell2_a_b_prod_ell2_cblinfun_fun$'| (as |@_tptp.'A_b_prod_ell2_a_b_prod_ell2_cblinfun_a_b_prod_ell2_a_b_prod_ell2_cblinfun_fun$'__0| |tptp.'A_b_prod_ell2_a_b_prod_ell2_cblinfun_a_b_prod_ell2_a_b_prod_ell2_cblinfun_fun$'|)) % 136.14/136.91 (define-fun |tptp.'comp$ai'| (($x1 |tptp.'B_b_prod_ell2_b_b_prod_ell2_cblinfun_a_c_prod_ell2_a_c_prod_ell2_cblinfun_fun$'|) ($x2 |tptp.'A_a_prod_ell2_a_a_prod_ell2_cblinfun_b_b_prod_ell2_b_b_prod_ell2_cblinfun_fun$'|)) |tptp.'A_a_prod_ell2_a_a_prod_ell2_cblinfun_a_c_prod_ell2_a_c_prod_ell2_cblinfun_fun$'| (as |@_tptp.'A_a_prod_ell2_a_a_prod_ell2_cblinfun_a_c_prod_ell2_a_c_prod_ell2_cblinfun_fun$'__0| |tptp.'A_a_prod_ell2_a_a_prod_ell2_cblinfun_a_c_prod_ell2_a_c_prod_ell2_cblinfun_fun$'|)) % 136.14/136.91 (define-fun |tptp.'clinear$d'| (($x1 |tptp.'B_ell2_b_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$'|)) Bool true) % 136.14/136.91 (define-fun |tptp.'comp$g'| (($x1 |tptp.'C_ell2_c_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$'|) ($x2 |tptp.'A_ell2_a_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$'|)) |tptp.'A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$'| (as |@_tptp.'A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$'__0| |tptp.'A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$'|)) % 136.14/136.91 (define-fun |tptp.'inv_into$r'| (($x1 |tptp.'B_b_prod_ell2_b_b_prod_ell2_cblinfun_set$'|) ($x2 |tptp.'B_b_prod_ell2_b_b_prod_ell2_cblinfun_a_a_prod_ell2_a_a_prod_ell2_cblinfun_fun$'|)) |tptp.'A_a_prod_ell2_a_a_prod_ell2_cblinfun_b_b_prod_ell2_b_b_prod_ell2_cblinfun_fun$'| (as |@_tptp.'A_a_prod_ell2_a_a_prod_ell2_cblinfun_b_b_prod_ell2_b_b_prod_ell2_cblinfun_fun$'__0| |tptp.'A_a_prod_ell2_a_a_prod_ell2_cblinfun_b_b_prod_ell2_b_b_prod_ell2_cblinfun_fun$'|)) % 136.14/136.91 (define-fun |tptp.'fun_app$f'| (($x1 |tptp.'B_ell2_b_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun_b_ell2_b_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun_fun$'|) ($x2 |tptp.'B_ell2_b_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$'|)) |tptp.'B_ell2_b_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$'| (as |@_tptp.'B_ell2_b_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$'__0| |tptp.'B_ell2_b_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$'|)) % 136.14/136.91 (define-fun |tptp.'id$f'| () |tptp.'B_a_prod_ell2_b_a_prod_ell2_cblinfun_b_a_prod_ell2_b_a_prod_ell2_cblinfun_fun$'| (as |@_tptp.'B_a_prod_ell2_b_a_prod_ell2_cblinfun_b_a_prod_ell2_b_a_prod_ell2_cblinfun_fun$'__0| |tptp.'B_a_prod_ell2_b_a_prod_ell2_cblinfun_b_a_prod_ell2_b_a_prod_ell2_cblinfun_fun$'|)) % 136.14/136.91 (define-fun |tptp.'iso_register$c'| (($x1 |tptp.'B_ell2_b_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$'|)) Bool false) % 136.14/136.91 (define-fun |tptp.'register_tensor$i'| (($x1 |tptp.'C_ell2_c_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$'|) ($x2 |tptp.'A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$'|)) |tptp.'C_a_prod_ell2_c_a_prod_ell2_cblinfun_a_b_prod_ell2_a_b_prod_ell2_cblinfun_fun$'| (as |@_tptp.'C_a_prod_ell2_c_a_prod_ell2_cblinfun_a_b_prod_ell2_a_b_prod_ell2_cblinfun_fun$'__0| |tptp.'C_a_prod_ell2_c_a_prod_ell2_cblinfun_a_b_prod_ell2_a_b_prod_ell2_cblinfun_fun$'|)) % 136.14/136.91 (define-fun |tptp.'comp$'| (($x1 |tptp.'A_ell2_a_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$'|)) |tptp.'B_ell2_b_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun_b_ell2_b_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun_fun$'| (as |@_tptp.'B_ell2_b_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun_b_ell2_b_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun_fun$'__0| |tptp.'B_ell2_b_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun_b_ell2_b_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun_fun$'|)) % 136.14/136.91 (define-fun |tptp.'id$j'| () |tptp.'C_ell2_c_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$'| (as |@_tptp.'C_ell2_c_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$'__0| |tptp.'C_ell2_c_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$'|)) % 136.14/136.91 (define-fun |tptp.'comp$ag'| (($x1 |tptp.'A_b_prod_ell2_a_b_prod_ell2_cblinfun_c_a_prod_ell2_c_a_prod_ell2_cblinfun_fun$'|) ($x2 |tptp.'B_a_prod_ell2_b_a_prod_ell2_cblinfun_a_b_prod_ell2_a_b_prod_ell2_cblinfun_fun$'|)) |tptp.'B_a_prod_ell2_b_a_prod_ell2_cblinfun_c_a_prod_ell2_c_a_prod_ell2_cblinfun_fun$'| (as |@_tptp.'B_a_prod_ell2_b_a_prod_ell2_cblinfun_c_a_prod_ell2_c_a_prod_ell2_cblinfun_fun$'__0| |tptp.'B_a_prod_ell2_b_a_prod_ell2_cblinfun_c_a_prod_ell2_c_a_prod_ell2_cblinfun_fun$'|)) % 136.14/136.91 (define-fun |tptp.'image$g'| (($x1 |tptp.'Nat_nat_fun$'|) ($x2 |tptp.'Nat_set$'|)) |tptp.'Nat_set$'| (as |@_tptp.'Nat_set$'__0| |tptp.'Nat_set$'|)) % 136.14/136.91 (define-fun |tptp.'comp$ad'| (($x1 |tptp.'B_a_prod_ell2_b_a_prod_ell2_cblinfun_c_b_prod_ell2_c_b_prod_ell2_cblinfun_fun$'|) ($x2 |tptp.'A_b_prod_ell2_a_b_prod_ell2_cblinfun_b_a_prod_ell2_b_a_prod_ell2_cblinfun_fun$'|)) |tptp.'A_b_prod_ell2_a_b_prod_ell2_cblinfun_c_b_prod_ell2_c_b_prod_ell2_cblinfun_fun$'| (as |@_tptp.'A_b_prod_ell2_a_b_prod_ell2_cblinfun_c_b_prod_ell2_c_b_prod_ell2_cblinfun_fun$'__0| |tptp.'A_b_prod_ell2_a_b_prod_ell2_cblinfun_c_b_prod_ell2_c_b_prod_ell2_cblinfun_fun$'|)) % 136.14/136.91 (define-fun |tptp.'member$c'| (($x1 |tptp.'Nat$'|) ($x2 |tptp.'Nat_set$'|)) Bool true) % 136.14/136.91 (define-fun |tptp.'top$j'| () |tptp.'A_a_prod_ell2_a_a_prod_ell2_cblinfun_set$'| (as |@_tptp.'A_a_prod_ell2_a_a_prod_ell2_cblinfun_set$'__0| |tptp.'A_a_prod_ell2_a_a_prod_ell2_cblinfun_set$'|)) % 136.14/136.91 (define-fun |tptp.'comp$n'| (($x1 |tptp.'A_ell2_a_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$'|) ($x2 |tptp.'A_ell2_a_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$'|)) |tptp.'A_ell2_a_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$'| (as |@_tptp.'A_ell2_a_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$'__0| |tptp.'A_ell2_a_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$'|)) % 136.14/136.91 (define-fun |tptp.'iso_register$e'| (($x1 |tptp.'A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$'|)) Bool true) % 136.14/136.91 (define-fun |tptp.'collect$a'| (($x1 |tptp.'A_ell2_a_ell2_cblinfun_bool_fun$'|)) |tptp.'A_ell2_a_ell2_cblinfun_set$'| (as |@_tptp.'A_ell2_a_ell2_cblinfun_set$'__0| |tptp.'A_ell2_a_ell2_cblinfun_set$'|)) % 136.14/136.91 (define-fun |tptp.'comp$q'| (($x1 |tptp.'C_ell2_c_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$'|) ($x2 |tptp.'B_ell2_b_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$'|)) |tptp.'B_ell2_b_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$'| (as |@_tptp.'B_ell2_b_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$'__0| |tptp.'B_ell2_b_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$'|)) % 136.14/136.91 (define-fun |tptp.'inv_into$m'| (($x1 |tptp.'B_b_prod_ell2_b_b_prod_ell2_cblinfun_set$'|) ($x2 |tptp.'B_b_prod_ell2_b_b_prod_ell2_cblinfun_c_c_prod_ell2_c_c_prod_ell2_cblinfun_fun$'|)) |tptp.'C_c_prod_ell2_c_c_prod_ell2_cblinfun_b_b_prod_ell2_b_b_prod_ell2_cblinfun_fun$'| (as |@_tptp.'C_c_prod_ell2_c_c_prod_ell2_cblinfun_b_b_prod_ell2_b_b_prod_ell2_cblinfun_fun$'__0| |tptp.'C_c_prod_ell2_c_c_prod_ell2_cblinfun_b_b_prod_ell2_b_b_prod_ell2_cblinfun_fun$'|)) % 136.14/136.91 (define-fun |tptp.'register_tensor$s'| ((_arg_1 |tptp.'B_ell2_b_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$'|) (_arg_2 |tptp.'A_ell2_a_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$'|)) |tptp.'B_a_prod_ell2_b_a_prod_ell2_cblinfun_b_a_prod_ell2_b_a_prod_ell2_cblinfun_fun$'| (as |@_tptp.'B_a_prod_ell2_b_a_prod_ell2_cblinfun_b_a_prod_ell2_b_a_prod_ell2_cblinfun_fun$'__0| |tptp.'B_a_prod_ell2_b_a_prod_ell2_cblinfun_b_a_prod_ell2_b_a_prod_ell2_cblinfun_fun$'|)) % 136.14/136.91 (define-fun |tptp.'id$c'| () |tptp.'A_ell2_a_ell2_cblinfun_set_a_ell2_a_ell2_cblinfun_set_fun$'| (as |@_tptp.'A_ell2_a_ell2_cblinfun_set_a_ell2_a_ell2_cblinfun_set_fun$'__0| |tptp.'A_ell2_a_ell2_cblinfun_set_a_ell2_a_ell2_cblinfun_set_fun$'|)) % 136.14/136.91 (define-fun |tptp.'commutant$a'| (($x1 |tptp.'A_ell2_a_ell2_cblinfun_set$'|)) |tptp.'A_ell2_a_ell2_cblinfun_set$'| (as |@_tptp.'A_ell2_a_ell2_cblinfun_set$'__0| |tptp.'A_ell2_a_ell2_cblinfun_set$'|)) % 136.14/136.91 (define-fun |tptp.'comp$s'| (($x1 |tptp.'A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$'|) ($x2 |tptp.'C_ell2_c_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$'|)) |tptp.'C_ell2_c_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$'| (as |@_tptp.'C_ell2_c_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$'__0| |tptp.'C_ell2_c_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$'|)) % 136.14/136.91 (define-fun |tptp.'register_tensor$l'| (($x1 |tptp.'B_ell2_b_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$'|) ($x2 |tptp.'A_ell2_a_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$'|)) |tptp.'B_a_prod_ell2_b_a_prod_ell2_cblinfun_a_c_prod_ell2_a_c_prod_ell2_cblinfun_fun$'| (as |@_tptp.'B_a_prod_ell2_b_a_prod_ell2_cblinfun_a_c_prod_ell2_a_c_prod_ell2_cblinfun_fun$'__0| |tptp.'B_a_prod_ell2_b_a_prod_ell2_cblinfun_a_c_prod_ell2_a_c_prod_ell2_cblinfun_fun$'|)) % 136.14/136.91 (define-fun |tptp.'top$a'| () |tptp.'B_ell2_b_ell2_cblinfun_set$'| (as |@_tptp.'B_ell2_b_ell2_cblinfun_set$'__0| |tptp.'B_ell2_b_ell2_cblinfun_set$'|)) % 136.14/136.91 (define-fun |tptp.'commutant$'| (($x1 |tptp.'C_ell2_c_ell2_cblinfun_set$'|)) |tptp.'C_ell2_c_ell2_cblinfun_set$'| (as |@_tptp.'C_ell2_c_ell2_cblinfun_set$'__0| |tptp.'C_ell2_c_ell2_cblinfun_set$'|)) % 136.14/136.91 (define-fun |tptp.'register$b'| (($x1 |tptp.'B_ell2_b_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$'|)) Bool true) % 136.14/136.91 (define-fun |tptp.'top$g'| () |tptp.'B_ell2_b_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun_set$'| (as |@_tptp.'B_ell2_b_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun_set$'__0| |tptp.'B_ell2_b_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun_set$'|)) % 136.14/136.91 (define-fun |tptp.'id$e'| () |tptp.'B_b_prod_ell2_b_b_prod_ell2_cblinfun_b_b_prod_ell2_b_b_prod_ell2_cblinfun_fun$'| (as |@_tptp.'B_b_prod_ell2_b_b_prod_ell2_cblinfun_b_b_prod_ell2_b_b_prod_ell2_cblinfun_fun$'__0| |tptp.'B_b_prod_ell2_b_b_prod_ell2_cblinfun_b_b_prod_ell2_b_b_prod_ell2_cblinfun_fun$'|)) % 136.14/136.91 (define-fun |tptp.'clinear$a'| (($x1 |tptp.'B_ell2_b_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$'|)) Bool true) % 136.14/136.91 (define-fun |tptp.'fun_app$e'| (($x1 |tptp.'B_ell2_b_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$'|) ($x2 |tptp.'B_ell2_b_ell2_cblinfun$'|)) |tptp.'B_ell2_b_ell2_cblinfun$'| (as |@_tptp.'B_ell2_b_ell2_cblinfun$'__0| |tptp.'B_ell2_b_ell2_cblinfun$'|)) % 136.14/136.91 (define-fun |tptp.'comp$r'| (($x1 |tptp.'C_ell2_c_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$'|) ($x2 |tptp.'A_ell2_a_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$'|)) |tptp.'A_ell2_a_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$'| (as |@_tptp.'A_ell2_a_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$'__0| |tptp.'A_ell2_a_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$'|)) % 136.14/136.91 (define-fun |tptp.'bijection$b'| (($x1 |tptp.'B_ell2_b_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$'|)) Bool false) % 136.14/136.91 (define-fun |tptp.'register$p'| (($x1 |tptp.'A_a_prod_ell2_a_a_prod_ell2_cblinfun_c_b_prod_ell2_c_b_prod_ell2_cblinfun_fun$'|)) Bool true) % 136.14/136.91 (define-fun |tptp.'image$c'| (($x1 |tptp.'A_ell2_a_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$'|)) |tptp.'A_ell2_a_ell2_cblinfun_set_a_ell2_a_ell2_cblinfun_set_fun$'| (as |@_tptp.'A_ell2_a_ell2_cblinfun_set_a_ell2_a_ell2_cblinfun_set_fun$'__0| |tptp.'A_ell2_a_ell2_cblinfun_set_a_ell2_a_ell2_cblinfun_set_fun$'|)) % 136.14/136.91 (define-fun |tptp.'i$'| () |tptp.'B_ell2_b_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$'| (as |@_tptp.'B_ell2_b_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$'__0| |tptp.'B_ell2_b_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$'|)) % 136.14/136.91 (define-fun |tptp.'top$m'| () |tptp.'B_b_prod_ell2_b_b_prod_ell2_cblinfun_set$'| (as |@_tptp.'B_b_prod_ell2_b_b_prod_ell2_cblinfun_set$'__0| |tptp.'B_b_prod_ell2_b_b_prod_ell2_cblinfun_set$'|)) % 136.14/136.91 (define-fun |tptp.'fun_app$i'| (($x1 |tptp.'A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun_a_ell2_a_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun_fun$'|) ($x2 |tptp.'A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$'|)) |tptp.'A_ell2_a_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$'| (as |@_tptp.'A_ell2_a_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$'__0| |tptp.'A_ell2_a_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$'|)) % 136.14/136.91 (define-fun |tptp.'register$f'| (($x1 |tptp.'C_ell2_c_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$'|)) Bool true) % 136.14/136.91 (define-fun |tptp.'inv_into$k'| (($x1 |tptp.'A_b_prod_ell2_a_b_prod_ell2_cblinfun_set$'|) ($x2 |tptp.'A_b_prod_ell2_a_b_prod_ell2_cblinfun_c_c_prod_ell2_c_c_prod_ell2_cblinfun_fun$'|)) |tptp.'C_c_prod_ell2_c_c_prod_ell2_cblinfun_a_b_prod_ell2_a_b_prod_ell2_cblinfun_fun$'| (as |@_tptp.'C_c_prod_ell2_c_c_prod_ell2_cblinfun_a_b_prod_ell2_a_b_prod_ell2_cblinfun_fun$'__0| |tptp.'C_c_prod_ell2_c_c_prod_ell2_cblinfun_a_b_prod_ell2_a_b_prod_ell2_cblinfun_fun$'|)) % 136.14/136.91 (define-fun |tptp.'top$l'| () |tptp.'B_a_prod_ell2_b_a_prod_ell2_cblinfun_set$'| (as |@_tptp.'B_a_prod_ell2_b_a_prod_ell2_cblinfun_set$'__0| |tptp.'B_a_prod_ell2_b_a_prod_ell2_cblinfun_set$'|)) % 136.14/136.91 (define-fun |tptp.'comp$a'| (($x1 |tptp.'A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$'|)) |tptp.'B_ell2_b_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun_b_ell2_b_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun_fun$'| (as |@_tptp.'B_ell2_b_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun_b_ell2_b_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun_fun$'__0| |tptp.'B_ell2_b_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun_b_ell2_b_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun_fun$'|)) % 136.14/136.91 (define-fun |tptp.'fun_app$s'| (($x1 |tptp.'B_ell2_b_ell2_cblinfun_set_b_ell2_b_ell2_cblinfun_fun$'|) ($x2 |tptp.'B_ell2_b_ell2_cblinfun_set$'|)) |tptp.'B_ell2_b_ell2_cblinfun$'| (as |@_tptp.'B_ell2_b_ell2_cblinfun$'__0| |tptp.'B_ell2_b_ell2_cblinfun$'|)) % 136.14/136.91 (define-fun |tptp.'fun_app$c'| (($x1 |tptp.'A_ell2_a_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$'|) ($x2 |tptp.'A_ell2_a_ell2_cblinfun$'|)) |tptp.'C_ell2_c_ell2_cblinfun$'| (as |@_tptp.'C_ell2_c_ell2_cblinfun$'__0| |tptp.'C_ell2_c_ell2_cblinfun$'|)) % 136.14/136.91 (define-fun |tptp.'comp$aa'| (($x1 |tptp.'B_b_prod_ell2_b_b_prod_ell2_cblinfun_c_c_prod_ell2_c_c_prod_ell2_cblinfun_fun$'|) ($x2 |tptp.'A_a_prod_ell2_a_a_prod_ell2_cblinfun_b_b_prod_ell2_b_b_prod_ell2_cblinfun_fun$'|)) |tptp.'A_a_prod_ell2_a_a_prod_ell2_cblinfun_c_c_prod_ell2_c_c_prod_ell2_cblinfun_fun$'| (as |@_tptp.'A_a_prod_ell2_a_a_prod_ell2_cblinfun_c_c_prod_ell2_c_c_prod_ell2_cblinfun_fun$'__0| |tptp.'A_a_prod_ell2_a_a_prod_ell2_cblinfun_c_c_prod_ell2_c_c_prod_ell2_cblinfun_fun$'|)) % 136.14/136.91 (define-fun |tptp.'comp$w'| (($x1 |tptp.'B_ell2_b_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$'|) ($x2 |tptp.'C_ell2_c_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$'|)) |tptp.'C_ell2_c_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$'| (as |@_tptp.'C_ell2_c_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$'__0| |tptp.'C_ell2_c_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$'|)) % 136.14/136.91 (define-fun |tptp.'register_tensor$w'| (($x1 |tptp.'A_ell2_a_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$'|) ($x2 |tptp.'A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$'|)) |tptp.'A_a_prod_ell2_a_a_prod_ell2_cblinfun_c_b_prod_ell2_c_b_prod_ell2_cblinfun_fun$'| (as |@_tptp.'A_a_prod_ell2_a_a_prod_ell2_cblinfun_c_b_prod_ell2_c_b_prod_ell2_cblinfun_fun$'__0| |tptp.'A_a_prod_ell2_a_a_prod_ell2_cblinfun_c_b_prod_ell2_c_b_prod_ell2_cblinfun_fun$'|)) % 136.14/136.91 (define-fun |tptp.'fun_app$j'| (($x1 |tptp.'Nat_nat_fun$'|) ($x2 |tptp.'Nat$'|)) |tptp.'Nat$'| (as |@_tptp.'Nat$'__0| |tptp.'Nat$'|)) % 136.14/136.91 (define-fun |tptp.'inj_on$b'| (($x1 |tptp.'A_ell2_a_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$'|) ($x2 |tptp.'A_ell2_a_ell2_cblinfun_set$'|)) Bool true) % 136.14/136.91 (define-fun |tptp.'iso_register$b'| (($x1 |tptp.'C_ell2_c_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$'|)) Bool false) % 136.14/136.91 (define-fun |tptp.'register$r'| (($x1 |tptp.'B_a_prod_ell2_b_a_prod_ell2_cblinfun_a_c_prod_ell2_a_c_prod_ell2_cblinfun_fun$'|)) Bool true) % 136.14/136.91 (define-fun |tptp.'register$h'| (($x1 |tptp.'C_ell2_c_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$'|)) Bool false) % 136.14/136.91 (define-fun |tptp.'iso_register$a'| (($x1 |tptp.'A_ell2_a_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$'|)) Bool false) % 136.14/136.91 (define-fun |tptp.'id$i'| () |tptp.'Nat_nat_fun_nat_nat_fun_fun$'| (as |@_tptp.'Nat_nat_fun_nat_nat_fun_fun$'__0| |tptp.'Nat_nat_fun_nat_nat_fun_fun$'|)) % 136.14/136.91 (define-fun |tptp.'id_cblinfun$'| () |tptp.'B_ell2_b_ell2_cblinfun$'| (as |@_tptp.'B_ell2_b_ell2_cblinfun$'__0| |tptp.'B_ell2_b_ell2_cblinfun$'|)) % 136.14/136.91 (define-fun |tptp.'inv_into$l'| (($x1 |tptp.'B_a_prod_ell2_b_a_prod_ell2_cblinfun_set$'|) ($x2 |tptp.'B_a_prod_ell2_b_a_prod_ell2_cblinfun_c_c_prod_ell2_c_c_prod_ell2_cblinfun_fun$'|)) |tptp.'C_c_prod_ell2_c_c_prod_ell2_cblinfun_b_a_prod_ell2_b_a_prod_ell2_cblinfun_fun$'| (as |@_tptp.'C_c_prod_ell2_c_c_prod_ell2_cblinfun_b_a_prod_ell2_b_a_prod_ell2_cblinfun_fun$'__0| |tptp.'C_c_prod_ell2_c_c_prod_ell2_cblinfun_b_a_prod_ell2_b_a_prod_ell2_cblinfun_fun$'|)) % 136.14/136.91 (define-fun |tptp.'register_tensor$'| (($x1 |tptp.'A_ell2_a_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$'|) ($x2 |tptp.'A_ell2_a_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$'|)) |tptp.'A_a_prod_ell2_a_a_prod_ell2_cblinfun_c_c_prod_ell2_c_c_prod_ell2_cblinfun_fun$'| (as |@_tptp.'A_a_prod_ell2_a_a_prod_ell2_cblinfun_c_c_prod_ell2_c_c_prod_ell2_cblinfun_fun$'__0| |tptp.'A_a_prod_ell2_a_a_prod_ell2_cblinfun_c_c_prod_ell2_c_c_prod_ell2_cblinfun_fun$'|)) % 136.14/136.91 (define-fun |tptp.'top$b'| () |tptp.'C_ell2_c_ell2_cblinfun_set$'| (as |@_tptp.'C_ell2_c_ell2_cblinfun_set$'__0| |tptp.'C_ell2_c_ell2_cblinfun_set$'|)) % 136.14/136.91 (define-fun |tptp.'inv_into$j'| (($x1 |tptp.'A_a_prod_ell2_a_a_prod_ell2_cblinfun_set$'|) ($x2 |tptp.'A_a_prod_ell2_a_a_prod_ell2_cblinfun_c_c_prod_ell2_c_c_prod_ell2_cblinfun_fun$'|)) |tptp.'C_c_prod_ell2_c_c_prod_ell2_cblinfun_a_a_prod_ell2_a_a_prod_ell2_cblinfun_fun$'| (as |@_tptp.'C_c_prod_ell2_c_c_prod_ell2_cblinfun_a_a_prod_ell2_a_a_prod_ell2_cblinfun_fun$'__0| |tptp.'C_c_prod_ell2_c_c_prod_ell2_cblinfun_a_a_prod_ell2_a_a_prod_ell2_cblinfun_fun$'|)) % 136.14/136.91 (define-fun |tptp.'g$'| () |tptp.'B_ell2_b_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$'| (as |@_tptp.'B_ell2_b_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$'__0| |tptp.'B_ell2_b_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$'|)) % 136.14/136.91 (define-fun |tptp.'register_tensor$t'| ((_arg_1 |tptp.'A_ell2_a_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$'|) (_arg_2 |tptp.'B_ell2_b_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$'|)) |tptp.'A_b_prod_ell2_a_b_prod_ell2_cblinfun_a_b_prod_ell2_a_b_prod_ell2_cblinfun_fun$'| (as |@_tptp.'A_b_prod_ell2_a_b_prod_ell2_cblinfun_a_b_prod_ell2_a_b_prod_ell2_cblinfun_fun$'__0| |tptp.'A_b_prod_ell2_a_b_prod_ell2_cblinfun_a_b_prod_ell2_a_b_prod_ell2_cblinfun_fun$'|)) % 136.14/136.91 (define-fun |tptp.'image$i'| (($x1 |tptp.'C_ell2_c_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$'|) ($x2 |tptp.'C_ell2_c_ell2_cblinfun_set$'|)) |tptp.'B_ell2_b_ell2_cblinfun_set$'| (as |@_tptp.'B_ell2_b_ell2_cblinfun_set$'__0| |tptp.'B_ell2_b_ell2_cblinfun_set$'|)) % 136.14/136.91 (define-fun |tptp.'collect$b'| (($x1 |tptp.'B_ell2_b_ell2_cblinfun_bool_fun$'|)) |tptp.'B_ell2_b_ell2_cblinfun_set$'| (as |@_tptp.'B_ell2_b_ell2_cblinfun_set$'__0| |tptp.'B_ell2_b_ell2_cblinfun_set$'|)) % 136.14/136.91 (define-fun |tptp.'register$c'| (($x1 |tptp.'A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$'|)) Bool true) % 136.14/136.91 (define-fun |tptp.'comp$o'| (($x1 |tptp.'A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$'|) ($x2 |tptp.'A_ell2_a_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$'|)) |tptp.'A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$'| (as |@_tptp.'A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$'__0| |tptp.'A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$'|)) % 136.14/136.91 (define-fun |tptp.'register_tensor$q'| (($x1 |tptp.'A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$'|) ($x2 |tptp.'A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$'|)) |tptp.'A_a_prod_ell2_a_a_prod_ell2_cblinfun_b_b_prod_ell2_b_b_prod_ell2_cblinfun_fun$'| (as |@_tptp.'A_a_prod_ell2_a_a_prod_ell2_cblinfun_b_b_prod_ell2_b_b_prod_ell2_cblinfun_fun$'__0| |tptp.'A_a_prod_ell2_a_a_prod_ell2_cblinfun_b_b_prod_ell2_b_b_prod_ell2_cblinfun_fun$'|)) % 136.14/136.91 (define-fun |tptp.'comp$aj'| (($x1 |tptp.'B_a_prod_ell2_b_a_prod_ell2_cblinfun_a_c_prod_ell2_a_c_prod_ell2_cblinfun_fun$'|) ($x2 |tptp.'A_b_prod_ell2_a_b_prod_ell2_cblinfun_b_a_prod_ell2_b_a_prod_ell2_cblinfun_fun$'|)) |tptp.'A_b_prod_ell2_a_b_prod_ell2_cblinfun_a_c_prod_ell2_a_c_prod_ell2_cblinfun_fun$'| (as |@_tptp.'A_b_prod_ell2_a_b_prod_ell2_cblinfun_a_c_prod_ell2_a_c_prod_ell2_cblinfun_fun$'__0| |tptp.'A_b_prod_ell2_a_b_prod_ell2_cblinfun_a_c_prod_ell2_a_c_prod_ell2_cblinfun_fun$'|)) % 136.14/136.91 (define-fun |tptp.'inv_into$i'| (($x1 |tptp.'C_ell2_c_ell2_cblinfun_set$'|) ($x2 |tptp.'C_ell2_c_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$'|)) |tptp.'C_ell2_c_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$'| (as |@_tptp.'C_ell2_c_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$'__0| |tptp.'C_ell2_c_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$'|)) % 136.14/136.91 (define-fun |tptp.'commutant$b'| (($x1 |tptp.'B_ell2_b_ell2_cblinfun_set$'|)) |tptp.'B_ell2_b_ell2_cblinfun_set$'| (as |@_tptp.'B_ell2_b_ell2_cblinfun_set$'__0| |tptp.'B_ell2_b_ell2_cblinfun_set$'|)) % 136.14/136.91 (define-fun |tptp.'inv_into$q'| (($x1 |tptp.'B_b_prod_ell2_b_b_prod_ell2_cblinfun_set$'|) ($x2 |tptp.'B_b_prod_ell2_b_b_prod_ell2_cblinfun_a_c_prod_ell2_a_c_prod_ell2_cblinfun_fun$'|)) |tptp.'A_c_prod_ell2_a_c_prod_ell2_cblinfun_b_b_prod_ell2_b_b_prod_ell2_cblinfun_fun$'| (as |@_tptp.'A_c_prod_ell2_a_c_prod_ell2_cblinfun_b_b_prod_ell2_b_b_prod_ell2_cblinfun_fun$'__0| |tptp.'A_c_prod_ell2_a_c_prod_ell2_cblinfun_b_b_prod_ell2_b_b_prod_ell2_cblinfun_fun$'|)) % 136.14/136.91 (define-fun |tptp.'comp$i'| (($x1 |tptp.'A_ell2_a_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$'|) ($x2 |tptp.'B_ell2_b_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$'|)) |tptp.'B_ell2_b_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$'| (as |@_tptp.'B_ell2_b_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$'__0| |tptp.'B_ell2_b_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$'|)) % 136.14/136.91 (define-fun |tptp.'image$f'| (($x1 |tptp.'A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$'|) ($x2 |tptp.'A_ell2_a_ell2_cblinfun_set$'|)) |tptp.'B_ell2_b_ell2_cblinfun_set$'| (as |@_tptp.'B_ell2_b_ell2_cblinfun_set$'__0| |tptp.'B_ell2_b_ell2_cblinfun_set$'|)) % 136.14/136.91 (define-fun |tptp.'bijection$'| (($x1 |tptp.'Nat_nat_fun$'|)) Bool true) % 136.14/136.91 (define-fun |tptp.'fun_app$p'| (($x1 |tptp.'B_ell2_b_ell2_cblinfun_set_b_ell2_b_ell2_cblinfun_set_fun$'|) ($x2 |tptp.'B_ell2_b_ell2_cblinfun_set$'|)) |tptp.'B_ell2_b_ell2_cblinfun_set$'| (as |@_tptp.'B_ell2_b_ell2_cblinfun_set$'__0| |tptp.'B_ell2_b_ell2_cblinfun_set$'|)) % 136.14/136.91 (define-fun |tptp.'comp$v'| (($x1 |tptp.'C_ell2_c_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$'|) ($x2 |tptp.'C_ell2_c_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$'|)) |tptp.'C_ell2_c_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$'| (as |@_tptp.'C_ell2_c_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$'__0| |tptp.'C_ell2_c_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$'|)) % 136.14/136.91 (define-fun |tptp.'inv_into$o'| (($x1 |tptp.'B_b_prod_ell2_b_b_prod_ell2_cblinfun_set$'|) ($x2 |tptp.'B_b_prod_ell2_b_b_prod_ell2_cblinfun_c_a_prod_ell2_c_a_prod_ell2_cblinfun_fun$'|)) |tptp.'C_a_prod_ell2_c_a_prod_ell2_cblinfun_b_b_prod_ell2_b_b_prod_ell2_cblinfun_fun$'| (as |@_tptp.'C_a_prod_ell2_c_a_prod_ell2_cblinfun_b_b_prod_ell2_b_b_prod_ell2_cblinfun_fun$'__0| |tptp.'C_a_prod_ell2_c_a_prod_ell2_cblinfun_b_b_prod_ell2_b_b_prod_ell2_cblinfun_fun$'|)) % 136.14/136.91 (define-fun |tptp.'inj_on$k'| (($x1 |tptp.'A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun_a_ell2_a_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun_fun$'|) ($x2 |tptp.'A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun_set$'|)) Bool true) % 136.14/136.91 (define-fun |tptp.'register$'| (($x1 |tptp.'B_ell2_b_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$'|)) Bool true) % 136.14/136.91 (define-fun |tptp.'register$l'| (($x1 |tptp.'B_a_prod_ell2_b_a_prod_ell2_cblinfun_c_b_prod_ell2_c_b_prod_ell2_cblinfun_fun$'|)) Bool true) % 136.14/136.91 (define-fun |tptp.'fun_app$m'| (($x1 |tptp.'C_ell2_c_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$'|) ($x2 |tptp.'C_ell2_c_ell2_cblinfun$'|)) |tptp.'C_ell2_c_ell2_cblinfun$'| (as |@_tptp.'C_ell2_c_ell2_cblinfun$'__0| |tptp.'C_ell2_c_ell2_cblinfun$'|)) % 136.14/136.91 (define-fun |tptp.'register_tensor$z'| (($x1 |tptp.'A_ell2_a_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$'|) ($x2 |tptp.'B_ell2_b_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$'|)) |tptp.'A_b_prod_ell2_a_b_prod_ell2_cblinfun_c_b_prod_ell2_c_b_prod_ell2_cblinfun_fun$'| (as |@_tptp.'A_b_prod_ell2_a_b_prod_ell2_cblinfun_c_b_prod_ell2_c_b_prod_ell2_cblinfun_fun$'__0| |tptp.'A_b_prod_ell2_a_b_prod_ell2_cblinfun_c_b_prod_ell2_c_b_prod_ell2_cblinfun_fun$'|)) % 136.14/136.91 (define-fun |tptp.'clinear$c'| (($x1 |tptp.'A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$'|)) Bool true) % 136.14/136.91 (define-fun |tptp.'id$b'| () |tptp.'B_ell2_b_ell2_cblinfun_set_b_ell2_b_ell2_cblinfun_set_fun$'| (as |@_tptp.'B_ell2_b_ell2_cblinfun_set_b_ell2_b_ell2_cblinfun_set_fun$'__0| |tptp.'B_ell2_b_ell2_cblinfun_set_b_ell2_b_ell2_cblinfun_set_fun$'|)) % 136.14/136.91 (define-fun |tptp.'comp$ac'| (($x1 |tptp.'B_b_prod_ell2_b_b_prod_ell2_cblinfun_c_a_prod_ell2_c_a_prod_ell2_cblinfun_fun$'|) ($x2 |tptp.'A_a_prod_ell2_a_a_prod_ell2_cblinfun_b_b_prod_ell2_b_b_prod_ell2_cblinfun_fun$'|)) |tptp.'A_a_prod_ell2_a_a_prod_ell2_cblinfun_c_a_prod_ell2_c_a_prod_ell2_cblinfun_fun$'| (as |@_tptp.'A_a_prod_ell2_a_a_prod_ell2_cblinfun_c_a_prod_ell2_c_a_prod_ell2_cblinfun_fun$'__0| |tptp.'A_a_prod_ell2_a_a_prod_ell2_cblinfun_c_a_prod_ell2_c_a_prod_ell2_cblinfun_fun$'|)) % 136.14/136.91 (define-fun |tptp.'register$m'| (($x1 |tptp.'A_b_prod_ell2_a_b_prod_ell2_cblinfun_c_c_prod_ell2_c_c_prod_ell2_cblinfun_fun$'|)) Bool true) % 136.14/136.91 (define-fun |tptp.'register_tensor$k'| (($x1 |tptp.'C_ell2_c_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$'|) ($x2 |tptp.'A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$'|)) |tptp.'C_a_prod_ell2_c_a_prod_ell2_cblinfun_b_b_prod_ell2_b_b_prod_ell2_cblinfun_fun$'| (as |@_tptp.'C_a_prod_ell2_c_a_prod_ell2_cblinfun_b_b_prod_ell2_b_b_prod_ell2_cblinfun_fun$'__0| |tptp.'C_a_prod_ell2_c_a_prod_ell2_cblinfun_b_b_prod_ell2_b_b_prod_ell2_cblinfun_fun$'|)) % 136.14/136.91 (define-fun |tptp.'inv_into$c'| (($x1 |tptp.'B_ell2_b_ell2_cblinfun_set$'|) ($x2 |tptp.'B_ell2_b_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$'|)) |tptp.'A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$'| (as |@_tptp.'A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$'__0| |tptp.'A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$'|)) % 136.14/136.91 (define-fun |tptp.'comp$ab'| (($x1 |tptp.'B_a_prod_ell2_b_a_prod_ell2_cblinfun_c_c_prod_ell2_c_c_prod_ell2_cblinfun_fun$'|) ($x2 |tptp.'A_b_prod_ell2_a_b_prod_ell2_cblinfun_b_a_prod_ell2_b_a_prod_ell2_cblinfun_fun$'|)) |tptp.'A_b_prod_ell2_a_b_prod_ell2_cblinfun_c_c_prod_ell2_c_c_prod_ell2_cblinfun_fun$'| (as |@_tptp.'A_b_prod_ell2_a_b_prod_ell2_cblinfun_c_c_prod_ell2_c_c_prod_ell2_cblinfun_fun$'__0| |tptp.'A_b_prod_ell2_a_b_prod_ell2_cblinfun_c_c_prod_ell2_c_c_prod_ell2_cblinfun_fun$'|)) % 136.14/136.91 (define-fun |tptp.'inj_on$h'| (($x1 |tptp.'Nat_nat_fun_nat_nat_fun_fun$'|) ($x2 |tptp.'Nat_nat_fun_set$'|)) Bool true) % 136.14/136.91 (define-fun |tptp.'iso_register$g'| (($x1 |tptp.'A_ell2_a_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$'|)) Bool true) % 136.14/136.91 (define-fun |tptp.'register_tensor$ab'| (($x1 |tptp.'B_ell2_b_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$'|) ($x2 |tptp.'A_ell2_a_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$'|)) |tptp.'B_a_prod_ell2_b_a_prod_ell2_cblinfun_c_a_prod_ell2_c_a_prod_ell2_cblinfun_fun$'| (as |@_tptp.'B_a_prod_ell2_b_a_prod_ell2_cblinfun_c_a_prod_ell2_c_a_prod_ell2_cblinfun_fun$'__0| |tptp.'B_a_prod_ell2_b_a_prod_ell2_cblinfun_c_a_prod_ell2_c_a_prod_ell2_cblinfun_fun$'|)) % 136.14/136.91 (define-fun |tptp.'comp$l'| (($x1 |tptp.'B_ell2_b_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$'|) ($x2 |tptp.'B_ell2_b_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$'|)) |tptp.'B_ell2_b_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$'| (as |@_tptp.'B_ell2_b_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$'__0| |tptp.'B_ell2_b_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$'|)) % 136.14/136.91 (define-fun |tptp.'top$f'| () |tptp.'Nat_nat_fun_set$'| (as |@_tptp.'Nat_nat_fun_set$'__0| |tptp.'Nat_nat_fun_set$'|)) % 136.14/136.91 (define-fun |tptp.'comp$m'| (($x1 |tptp.'B_ell2_b_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$'|) ($x2 |tptp.'A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$'|)) |tptp.'A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$'| (as |@_tptp.'A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$'__0| |tptp.'A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$'|)) % 136.14/136.91 (define-fun |tptp.'uu$'| (($x1 |tptp.'C_ell2_c_ell2_cblinfun_set$'|)) |tptp.'C_ell2_c_ell2_cblinfun_bool_fun$'| (as |@_tptp.'C_ell2_c_ell2_cblinfun_bool_fun$'__0| |tptp.'C_ell2_c_ell2_cblinfun_bool_fun$'|)) % 136.14/136.91 (define-fun |tptp.'register_tensor$j'| (($x1 |tptp.'B_ell2_b_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$'|) ($x2 |tptp.'B_ell2_b_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$'|)) |tptp.'B_b_prod_ell2_b_b_prod_ell2_cblinfun_c_a_prod_ell2_c_a_prod_ell2_cblinfun_fun$'| (as |@_tptp.'B_b_prod_ell2_b_b_prod_ell2_cblinfun_c_a_prod_ell2_c_a_prod_ell2_cblinfun_fun$'__0| |tptp.'B_b_prod_ell2_b_b_prod_ell2_cblinfun_c_a_prod_ell2_c_a_prod_ell2_cblinfun_fun$'|)) % 136.14/136.91 (define-fun |tptp.'fun_app$d'| (($x1 |tptp.'B_ell2_b_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$'|) ($x2 |tptp.'B_ell2_b_ell2_cblinfun$'|)) |tptp.'A_ell2_a_ell2_cblinfun$'| (as |@_tptp.'A_ell2_a_ell2_cblinfun$'__0| |tptp.'A_ell2_a_ell2_cblinfun$'|)) % 136.14/136.91 (define-fun |tptp.'register$d'| (($x1 |tptp.'B_ell2_b_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$'|)) Bool true) % 136.14/136.91 (define-fun |tptp.'j$'| () |tptp.'A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$'| (as |@_tptp.'A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$'__0| |tptp.'A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$'|)) % 136.14/136.91 (define-fun |tptp.'register_tensor$o'| (($x1 |tptp.'A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$'|) ($x2 |tptp.'C_ell2_c_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$'|)) |tptp.'A_c_prod_ell2_a_c_prod_ell2_cblinfun_b_b_prod_ell2_b_b_prod_ell2_cblinfun_fun$'| (as |@_tptp.'A_c_prod_ell2_a_c_prod_ell2_cblinfun_b_b_prod_ell2_b_b_prod_ell2_cblinfun_fun$'__0| |tptp.'A_c_prod_ell2_a_c_prod_ell2_cblinfun_b_b_prod_ell2_b_b_prod_ell2_cblinfun_fun$'|)) % 136.14/136.91 (define-fun |tptp.'fun_app$g'| (($x1 |tptp.'A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$'|) ($x2 |tptp.'A_ell2_a_ell2_cblinfun$'|)) |tptp.'B_ell2_b_ell2_cblinfun$'| (as |@_tptp.'B_ell2_b_ell2_cblinfun$'__0| |tptp.'B_ell2_b_ell2_cblinfun$'|)) % 136.14/136.91 (define-fun |tptp.'register_tensor$c'| (($x1 |tptp.'C_ell2_c_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$'|) ($x2 |tptp.'C_ell2_c_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$'|)) |tptp.'C_c_prod_ell2_c_c_prod_ell2_cblinfun_a_b_prod_ell2_a_b_prod_ell2_cblinfun_fun$'| (as |@_tptp.'C_c_prod_ell2_c_c_prod_ell2_cblinfun_a_b_prod_ell2_a_b_prod_ell2_cblinfun_fun$'__0| |tptp.'C_c_prod_ell2_c_c_prod_ell2_cblinfun_a_b_prod_ell2_a_b_prod_ell2_cblinfun_fun$'|)) % 136.14/136.91 (define-fun |tptp.'register_tensor$y'| (($x1 |tptp.'A_ell2_a_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$'|) ($x2 |tptp.'A_ell2_a_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$'|)) |tptp.'A_a_prod_ell2_a_a_prod_ell2_cblinfun_c_a_prod_ell2_c_a_prod_ell2_cblinfun_fun$'| (as |@_tptp.'A_a_prod_ell2_a_a_prod_ell2_cblinfun_c_a_prod_ell2_c_a_prod_ell2_cblinfun_fun$'__0| |tptp.'A_a_prod_ell2_a_a_prod_ell2_cblinfun_c_a_prod_ell2_c_a_prod_ell2_cblinfun_fun$'|)) % 136.14/136.91 (define-fun |tptp.'id_cblinfun$a'| () |tptp.'A_ell2_a_ell2_cblinfun$'| (as |@_tptp.'A_ell2_a_ell2_cblinfun$'__0| |tptp.'A_ell2_a_ell2_cblinfun$'|)) % 136.14/136.91 (define-fun |tptp.'clinear$'| (($x1 |tptp.'A_ell2_a_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$'|)) Bool true) % 136.14/136.91 (define-fun |tptp.'register_tensor$ad'| (($x1 |tptp.'A_ell2_a_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$'|) ($x2 |tptp.'A_ell2_a_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$'|)) |tptp.'A_a_prod_ell2_a_a_prod_ell2_cblinfun_a_c_prod_ell2_a_c_prod_ell2_cblinfun_fun$'| (as |@_tptp.'A_a_prod_ell2_a_a_prod_ell2_cblinfun_a_c_prod_ell2_a_c_prod_ell2_cblinfun_fun$'__0| |tptp.'A_a_prod_ell2_a_a_prod_ell2_cblinfun_a_c_prod_ell2_a_c_prod_ell2_cblinfun_fun$'|)) % 136.14/136.91 (define-fun |tptp.'register_tensor$ac'| (($x1 |tptp.'B_ell2_b_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$'|) ($x2 |tptp.'B_ell2_b_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$'|)) |tptp.'B_b_prod_ell2_b_b_prod_ell2_cblinfun_c_b_prod_ell2_c_b_prod_ell2_cblinfun_fun$'| (as |@_tptp.'B_b_prod_ell2_b_b_prod_ell2_cblinfun_c_b_prod_ell2_c_b_prod_ell2_cblinfun_fun$'__0| |tptp.'B_b_prod_ell2_b_b_prod_ell2_cblinfun_c_b_prod_ell2_c_b_prod_ell2_cblinfun_fun$'|)) % 136.14/136.91 (define-fun |tptp.'id$d'| () |tptp.'Nat_nat_fun$'| (as |@_tptp.'Nat_nat_fun$'__0| |tptp.'Nat_nat_fun$'|)) % 136.14/136.91 (define-fun |tptp.'bijection$a'| (($x1 |tptp.'A_ell2_a_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$'|)) Bool false) % 136.14/136.91 (define-fun |tptp.'member$'| ((BOUND_VARIABLE_32411 |tptp.'C_ell2_c_ell2_cblinfun$'|) (BOUND_VARIABLE_32413 |tptp.'C_ell2_c_ell2_cblinfun_set$'|)) Bool true) % 136.14/136.91 (define-fun |tptp.'register_tensor$r'| ((_arg_1 |tptp.'B_ell2_b_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$'|) (_arg_2 |tptp.'B_ell2_b_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$'|)) |tptp.'B_b_prod_ell2_b_b_prod_ell2_cblinfun_b_b_prod_ell2_b_b_prod_ell2_cblinfun_fun$'| (as |@_tptp.'B_b_prod_ell2_b_b_prod_ell2_cblinfun_b_b_prod_ell2_b_b_prod_ell2_cblinfun_fun$'__0| |tptp.'B_b_prod_ell2_b_b_prod_ell2_cblinfun_b_b_prod_ell2_b_b_prod_ell2_cblinfun_fun$'|)) % 136.14/136.91 (define-fun |tptp.'fun_app$u'| (($x1 |tptp.'Nat_set_nat_fun$'|) ($x2 |tptp.'Nat_set$'|)) |tptp.'Nat$'| (as |@_tptp.'Nat$'__0| |tptp.'Nat$'|)) % 136.14/136.91 (define-fun |tptp.'clinear$f'| (($x1 |tptp.'C_ell2_c_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$'|)) Bool true) % 136.14/136.91 (define-fun |tptp.'comp$b'| (($x1 |tptp.'B_ell2_b_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$'|)) |tptp.'A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun_a_ell2_a_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun_fun$'| (as |@_tptp.'A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun_a_ell2_a_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun_fun$'__0| |tptp.'A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun_a_ell2_a_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun_fun$'|)) % 136.14/136.91 (define-fun |tptp.'register_tensor$ae'| (($x1 |tptp.'A_ell2_a_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$'|) ($x2 |tptp.'B_ell2_b_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$'|)) |tptp.'A_b_prod_ell2_a_b_prod_ell2_cblinfun_a_c_prod_ell2_a_c_prod_ell2_cblinfun_fun$'| (as |@_tptp.'A_b_prod_ell2_a_b_prod_ell2_cblinfun_a_c_prod_ell2_a_c_prod_ell2_cblinfun_fun$'__0| |tptp.'A_b_prod_ell2_a_b_prod_ell2_cblinfun_a_c_prod_ell2_a_c_prod_ell2_cblinfun_fun$'|)) % 136.14/136.91 (define-fun |tptp.'inj_on$c'| (($x1 |tptp.'B_ell2_b_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$'|) ($x2 |tptp.'B_ell2_b_ell2_cblinfun_set$'|)) Bool true) % 136.14/136.91 (define-fun |tptp.'image$e'| (($x1 |tptp.'B_ell2_b_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$'|) ($x2 |tptp.'B_ell2_b_ell2_cblinfun_set$'|)) |tptp.'A_ell2_a_ell2_cblinfun_set$'| (as |@_tptp.'A_ell2_a_ell2_cblinfun_set$'__0| |tptp.'A_ell2_a_ell2_cblinfun_set$'|)) % 136.14/136.91 (define-fun |tptp.'top$e'| () |tptp.'Nat_set$'| (as |@_tptp.'Nat_set$'__0| |tptp.'Nat_set$'|)) % 136.14/136.91 (define-fun |tptp.'fun_app$v'| (($x1 |tptp.'C_ell2_c_ell2_cblinfun_set_c_ell2_c_ell2_cblinfun_fun$'|) ($x2 |tptp.'C_ell2_c_ell2_cblinfun_set$'|)) |tptp.'C_ell2_c_ell2_cblinfun$'| (as |@_tptp.'C_ell2_c_ell2_cblinfun$'__0| |tptp.'C_ell2_c_ell2_cblinfun$'|)) % 136.14/136.91 (define-fun |tptp.'inj_on$f'| (($x1 |tptp.'A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$'|) ($x2 |tptp.'A_ell2_a_ell2_cblinfun_set$'|)) Bool true) % 136.14/136.91 (define-fun |tptp.'comp$y'| (($x1 |tptp.'A_ell2_a_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$'|) ($x2 |tptp.'C_ell2_c_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$'|)) |tptp.'C_ell2_c_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$'| (as |@_tptp.'C_ell2_c_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$'__0| |tptp.'C_ell2_c_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$'|)) % 136.14/136.91 (define-fun |tptp.'top$k'| () |tptp.'A_b_prod_ell2_a_b_prod_ell2_cblinfun_set$'| (as |@_tptp.'A_b_prod_ell2_a_b_prod_ell2_cblinfun_set$'__0| |tptp.'A_b_prod_ell2_a_b_prod_ell2_cblinfun_set$'|)) % 136.14/136.91 (define-fun |tptp.'comp$d'| (($x1 |tptp.'C_ell2_c_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$'|) ($x2 |tptp.'B_ell2_b_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$'|)) |tptp.'B_ell2_b_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$'| (as |@_tptp.'B_ell2_b_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$'__0| |tptp.'B_ell2_b_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$'|)) % 136.14/136.91 (define-fun |tptp.'register$o'| (($x1 |tptp.'A_b_prod_ell2_a_b_prod_ell2_cblinfun_c_a_prod_ell2_c_a_prod_ell2_cblinfun_fun$'|)) Bool true) % 136.14/136.91 (define-fun |tptp.'comp$x'| (($x1 |tptp.'C_ell2_c_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$'|) ($x2 |tptp.'C_ell2_c_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$'|)) |tptp.'C_ell2_c_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$'| (as |@_tptp.'C_ell2_c_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$'__0| |tptp.'C_ell2_c_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$'|)) % 136.14/136.91 (define-fun |tptp.'comp$u'| (($x1 |tptp.'B_ell2_b_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$'|) ($x2 |tptp.'C_ell2_c_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$'|)) |tptp.'C_ell2_c_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$'| (as |@_tptp.'C_ell2_c_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$'__0| |tptp.'C_ell2_c_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$'|)) % 136.14/136.91 (define-fun |tptp.'inv_into$h'| (($x1 |tptp.'A_ell2_a_ell2_cblinfun_set$'|) ($x2 |tptp.'A_ell2_a_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$'|)) |tptp.'A_ell2_a_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$'| (as |@_tptp.'A_ell2_a_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$'__0| |tptp.'A_ell2_a_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$'|)) % 136.14/136.91 (define-fun |tptp.'fun_app$r'| (($x1 |tptp.'B_ell2_b_ell2_cblinfun_bool_fun$'|) ($x2 |tptp.'B_ell2_b_ell2_cblinfun$'|)) Bool true) % 136.14/136.91 (define-fun |tptp.'fun_app$a'| (($x1 |tptp.'B_ell2_b_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun_b_ell2_b_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun_fun$'|) ($x2 |tptp.'B_ell2_b_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$'|)) |tptp.'B_ell2_b_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$'| (as |@_tptp.'B_ell2_b_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$'__0| |tptp.'B_ell2_b_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$'|)) % 136.14/136.91 (define-fun |tptp.'register_tensor$p'| (($x1 |tptp.'B_ell2_b_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$'|) ($x2 |tptp.'B_ell2_b_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$'|)) |tptp.'B_b_prod_ell2_b_b_prod_ell2_cblinfun_a_a_prod_ell2_a_a_prod_ell2_cblinfun_fun$'| (as |@_tptp.'B_b_prod_ell2_b_b_prod_ell2_cblinfun_a_a_prod_ell2_a_a_prod_ell2_cblinfun_fun$'__0| |tptp.'B_b_prod_ell2_b_b_prod_ell2_cblinfun_a_a_prod_ell2_a_a_prod_ell2_cblinfun_fun$'|)) % 136.14/136.91 (define-fun |tptp.'comp$t'| (($x1 |tptp.'A_ell2_a_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$'|) ($x2 |tptp.'C_ell2_c_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$'|)) |tptp.'C_ell2_c_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$'| (as |@_tptp.'C_ell2_c_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$'__0| |tptp.'C_ell2_c_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$'|)) % 136.14/136.91 (define-fun |tptp.'register$g'| (($x1 |tptp.'C_ell2_c_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$'|)) Bool false) % 136.14/136.91 (define-fun |tptp.'suc$'| () |tptp.'Nat_nat_fun$'| (as |@_tptp.'Nat_nat_fun$'__0| |tptp.'Nat_nat_fun$'|)) % 136.14/136.91 (define-fun |tptp.'comp$k'| (($x1 |tptp.'B_ell2_b_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$'|) ($x2 |tptp.'A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$'|)) |tptp.'A_ell2_a_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$'| (as |@_tptp.'A_ell2_a_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$'__0| |tptp.'A_ell2_a_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$'|)) % 136.14/136.91 (define-fun |tptp.'inv_into$p'| (($x1 |tptp.'B_a_prod_ell2_b_a_prod_ell2_cblinfun_set$'|) ($x2 |tptp.'B_a_prod_ell2_b_a_prod_ell2_cblinfun_a_c_prod_ell2_a_c_prod_ell2_cblinfun_fun$'|)) |tptp.'A_c_prod_ell2_a_c_prod_ell2_cblinfun_b_a_prod_ell2_b_a_prod_ell2_cblinfun_fun$'| (as |@_tptp.'A_c_prod_ell2_a_c_prod_ell2_cblinfun_b_a_prod_ell2_b_a_prod_ell2_cblinfun_fun$'__0| |tptp.'A_c_prod_ell2_a_c_prod_ell2_cblinfun_b_a_prod_ell2_b_a_prod_ell2_cblinfun_fun$'|)) % 136.14/136.91 (define-fun |tptp.'inj_on$g'| (($x1 |tptp.'Nat_nat_fun$'|) ($x2 |tptp.'Nat_set$'|)) Bool true) % 136.14/136.91 (define-fun |tptp.'top$h'| () |tptp.'A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun_set$'| (as |@_tptp.'A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun_set$'__0| |tptp.'A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun_set$'|)) % 136.14/136.91 (define-fun |tptp.'register_tensor$n'| (($x1 |tptp.'B_ell2_b_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$'|) ($x2 |tptp.'B_ell2_b_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$'|)) |tptp.'B_b_prod_ell2_b_b_prod_ell2_cblinfun_a_c_prod_ell2_a_c_prod_ell2_cblinfun_fun$'| (as |@_tptp.'B_b_prod_ell2_b_b_prod_ell2_cblinfun_a_c_prod_ell2_a_c_prod_ell2_cblinfun_fun$'__0| |tptp.'B_b_prod_ell2_b_b_prod_ell2_cblinfun_a_c_prod_ell2_a_c_prod_ell2_cblinfun_fun$'|)) % 136.14/136.91 (define-fun |tptp.'register_tensor$g'| (($x1 |tptp.'C_ell2_c_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$'|) ($x2 |tptp.'C_ell2_c_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$'|)) |tptp.'C_c_prod_ell2_c_c_prod_ell2_cblinfun_b_b_prod_ell2_b_b_prod_ell2_cblinfun_fun$'| (as |@_tptp.'C_c_prod_ell2_c_c_prod_ell2_cblinfun_b_b_prod_ell2_b_b_prod_ell2_cblinfun_fun$'__0| |tptp.'C_c_prod_ell2_c_c_prod_ell2_cblinfun_b_b_prod_ell2_b_b_prod_ell2_cblinfun_fun$'|)) % 136.14/136.91 (define-fun |tptp.'comp$z'| (($x1 |tptp.'B_ell2_b_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$'|) ($x2 |tptp.'C_ell2_c_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$'|)) |tptp.'C_ell2_c_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$'| (as |@_tptp.'C_ell2_c_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$'__0| |tptp.'C_ell2_c_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$'|)) % 136.14/136.91 (define-fun |tptp.'inj_on$i'| (($x1 |tptp.'B_ell2_b_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun_b_ell2_b_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun_fun$'|) ($x2 |tptp.'B_ell2_b_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun_set$'|)) Bool true) % 136.14/136.91 (define-fun |tptp.'comp$ah'| (($x1 |tptp.'A_a_prod_ell2_a_a_prod_ell2_cblinfun_c_b_prod_ell2_c_b_prod_ell2_cblinfun_fun$'|) ($x2 |tptp.'B_b_prod_ell2_b_b_prod_ell2_cblinfun_a_a_prod_ell2_a_a_prod_ell2_cblinfun_fun$'|)) |tptp.'B_b_prod_ell2_b_b_prod_ell2_cblinfun_c_b_prod_ell2_c_b_prod_ell2_cblinfun_fun$'| (as |@_tptp.'B_b_prod_ell2_b_b_prod_ell2_cblinfun_c_b_prod_ell2_c_b_prod_ell2_cblinfun_fun$'__0| |tptp.'B_b_prod_ell2_b_b_prod_ell2_cblinfun_c_b_prod_ell2_c_b_prod_ell2_cblinfun_fun$'|)) % 136.14/136.91 (define-fun |tptp.'register$i'| (($x1 |tptp.'B_b_prod_ell2_b_b_prod_ell2_cblinfun_c_c_prod_ell2_c_c_prod_ell2_cblinfun_fun$'|)) Bool true) % 136.14/136.91 (define-fun |tptp.'id$'| () |tptp.'B_ell2_b_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$'| (as |@_tptp.'B_ell2_b_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$'__0| |tptp.'B_ell2_b_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$'|)) % 136.14/136.91 (define-fun |tptp.'clinear$h'| (($x1 |tptp.'C_ell2_c_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$'|)) Bool true) % 136.14/136.91 (define-fun |tptp.'register$a'| (($x1 |tptp.'A_ell2_a_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$'|)) Bool true) % 136.14/136.91 (define-fun |tptp.'register_tensor$x'| (($x1 |tptp.'A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$'|) ($x2 |tptp.'B_ell2_b_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$'|)) |tptp.'A_b_prod_ell2_a_b_prod_ell2_cblinfun_b_a_prod_ell2_b_a_prod_ell2_cblinfun_fun$'| (as |@_tptp.'A_b_prod_ell2_a_b_prod_ell2_cblinfun_b_a_prod_ell2_b_a_prod_ell2_cblinfun_fun$'__0| |tptp.'A_b_prod_ell2_a_b_prod_ell2_cblinfun_b_a_prod_ell2_b_a_prod_ell2_cblinfun_fun$'|)) % 136.14/136.91 (define-fun |tptp.'fun_app$n'| (($x1 |tptp.'C_ell2_c_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$'|) ($x2 |tptp.'C_ell2_c_ell2_cblinfun$'|)) |tptp.'B_ell2_b_ell2_cblinfun$'| (as |@_tptp.'B_ell2_b_ell2_cblinfun$'__0| |tptp.'B_ell2_b_ell2_cblinfun$'|)) % 136.14/136.91 (define-fun |tptp.'top$'| () |tptp.'A_ell2_a_ell2_cblinfun_set$'| (as |@_tptp.'A_ell2_a_ell2_cblinfun_set$'__0| |tptp.'A_ell2_a_ell2_cblinfun_set$'|)) % 136.14/136.91 (define-fun |tptp.'comp$c'| (($x1 |tptp.'Nat_nat_fun$'|)) |tptp.'Nat_nat_fun_nat_nat_fun_fun$'| (as |@_tptp.'Nat_nat_fun_nat_nat_fun_fun$'__0| |tptp.'Nat_nat_fun_nat_nat_fun_fun$'|)) % 136.14/136.91 (define-fun |tptp.'inj_on$l'| (($x1 |tptp.'C_ell2_c_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$'|) ($x2 |tptp.'C_ell2_c_ell2_cblinfun_set$'|)) Bool true) % 136.14/136.91 (define-fun |tptp.'register_tensor$aa'| (($x1 |tptp.'B_ell2_b_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$'|) ($x2 |tptp.'A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$'|)) |tptp.'B_a_prod_ell2_b_a_prod_ell2_cblinfun_a_b_prod_ell2_a_b_prod_ell2_cblinfun_fun$'| (as |@_tptp.'B_a_prod_ell2_b_a_prod_ell2_cblinfun_a_b_prod_ell2_a_b_prod_ell2_cblinfun_fun$'__0| |tptp.'B_a_prod_ell2_b_a_prod_ell2_cblinfun_a_b_prod_ell2_a_b_prod_ell2_cblinfun_fun$'|)) % 136.14/136.91 (define-fun |tptp.'clinear$e'| (($x1 |tptp.'A_ell2_a_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$'|)) Bool true) % 136.14/136.91 (define-fun |tptp.'fun_app$'| (($x1 |tptp.'C_ell2_c_ell2_cblinfun_bool_fun$'|) ($x2 |tptp.'C_ell2_c_ell2_cblinfun$'|)) Bool true) % 136.14/136.91 (define-fun |tptp.'id$h'| () |tptp.'A_a_prod_ell2_a_a_prod_ell2_cblinfun_a_a_prod_ell2_a_a_prod_ell2_cblinfun_fun$'| (as |@_tptp.'A_a_prod_ell2_a_a_prod_ell2_cblinfun_a_a_prod_ell2_a_a_prod_ell2_cblinfun_fun$'__0| |tptp.'A_a_prod_ell2_a_a_prod_ell2_cblinfun_a_a_prod_ell2_a_a_prod_ell2_cblinfun_fun$'|)) % 136.14/136.91 (define-fun |tptp.'comp$f'| (($x1 |tptp.'C_ell2_c_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$'|) ($x2 |tptp.'B_ell2_b_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$'|)) |tptp.'B_ell2_b_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$'| (as |@_tptp.'B_ell2_b_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$'__0| |tptp.'B_ell2_b_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$'|)) % 136.14/136.91 (define-fun |tptp.'inv_into$a'| (($x1 |tptp.'B_ell2_b_ell2_cblinfun_set$'|) ($x2 |tptp.'B_ell2_b_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$'|)) |tptp.'C_ell2_c_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$'| (as |@_tptp.'C_ell2_c_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$'__0| |tptp.'C_ell2_c_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$'|)) % 136.14/136.91 (define-fun |tptp.'image$d'| (($x1 |tptp.'B_ell2_b_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$'|)) |tptp.'B_ell2_b_ell2_cblinfun_set_b_ell2_b_ell2_cblinfun_set_fun$'| (as |@_tptp.'B_ell2_b_ell2_cblinfun_set_b_ell2_b_ell2_cblinfun_set_fun$'__0| |tptp.'B_ell2_b_ell2_cblinfun_set_b_ell2_b_ell2_cblinfun_set_fun$'|)) % 136.14/136.91 (define-fun |tptp.'register$e'| (($x1 |tptp.'A_ell2_a_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$'|)) Bool true) % 136.14/136.91 ) % 136.14/136.91 % SZS output end Model % 136.14/136.91 % cvc5 exiting %------------------------------------------------------------------------------