%------------------------------------------------------------------------------ % File : cvc5-SAT---1.3.4 % Problem : ITP385_1 : TPTP v9.2.1. Released v8.0.0. % Transfm : none % Format : tptp:raw % Command : /export/starexec/sandbox2/solver/bin/do_cvc5 /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % Computer : n010.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:59 AM UTC 2026 % Result : CounterSatisfiable 140.13s 140.49s % Output : Model 140.13s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : ITP385_1 : TPTP v9.2.1. Released v8.0.0. % 0.14/0.13 % Command : /export/starexec/sandbox2/solver/bin/do_cvc5 /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % 0.18/0.34 % Computer : n010.cluster.edu % 0.18/0.34 % Model : x86_64 x86_64 % 0.18/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.18/0.34 % Memory : 8042.1875MB % 0.18/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.18/0.34 % CPULimit : 300 % 0.18/0.34 % WCLimit : 300 % 0.18/0.34 % DateTime : Tue Jun 2 05:06:10 EDT 2026 % 0.18/0.35 % CPUTime : % 0.43/0.66 %----Disproving TF0_NAR % 140.13/140.49 --- Run --finite-model-find --sort-inference --uf-ss-fair at 60... % 140.13/140.49 --- Run --mbqi at 45... % 140.13/140.49 --- Run --mbqi --mbqi-enum --mbqi-enum-choice-grammar --mbqi-enum-global-syms-grammar --no-cegqi --no-sygus-inst at 45... % 140.13/140.49 --- Run --full-saturate-quant at 45... % 140.13/140.49 --- Run --finite-model-find --fmf-bound --macros-quant at 60... % 140.13/140.49 % SZS status CounterSatisfiable % 140.13/140.49 % SZS output start Model % 140.13/140.49 ( % 140.13/140.49 ; cardinality of $$unsorted is 1 % 140.13/140.49 ; rep: (as @$$unsorted_0 $$unsorted) % 140.13/140.49 ; cardinality of |tptp.'B_b_option_fun_b_option_fun$'| is 2 % 140.13/140.49 ; rep: (as |@_tptp.'B_b_option_fun_b_option_fun$'__0| |tptp.'B_b_option_fun_b_option_fun$'|) % 140.13/140.49 ; rep: (as |@_tptp.'B_b_option_fun_b_option_fun$'__1| |tptp.'B_b_option_fun_b_option_fun$'|) % 140.13/140.49 ; cardinality of |tptp.'A_a_prod_set$'| is 2 % 140.13/140.49 ; rep: (as |@_tptp.'A_a_prod_set$'__0| |tptp.'A_a_prod_set$'|) % 140.13/140.49 ; rep: (as |@_tptp.'A_a_prod_set$'__1| |tptp.'A_a_prod_set$'|) % 140.13/140.49 ; cardinality of |tptp.'B_d_prod$'| is 1 % 140.13/140.49 ; rep: (as |@_tptp.'B_d_prod$'__0| |tptp.'B_d_prod$'|) % 140.13/140.49 ; cardinality of |tptp.'D_bool_fun$'| is 2 % 140.13/140.49 ; rep: (as |@_tptp.'D_bool_fun$'__0| |tptp.'D_bool_fun$'|) % 140.13/140.49 ; rep: (as |@_tptp.'D_bool_fun$'__1| |tptp.'D_bool_fun$'|) % 140.13/140.49 ; cardinality of |tptp.'D_d_prod_set$'| is 1 % 140.13/140.49 ; rep: (as |@_tptp.'D_d_prod_set$'__0| |tptp.'D_d_prod_set$'|) % 140.13/140.49 ; cardinality of |tptp.'B_c_prod$'| is 1 % 140.13/140.49 ; rep: (as |@_tptp.'B_c_prod$'__0| |tptp.'B_c_prod$'|) % 140.13/140.49 ; cardinality of |tptp.'A_a_prod$'| is 1 % 140.13/140.49 ; rep: (as |@_tptp.'A_a_prod$'__0| |tptp.'A_a_prod$'|) % 140.13/140.49 ; cardinality of |tptp.'C_c_option_fun$'| is 2 % 140.13/140.49 ; rep: (as |@_tptp.'C_c_option_fun$'__0| |tptp.'C_c_option_fun$'|) % 140.13/140.49 ; rep: (as |@_tptp.'C_c_option_fun$'__1| |tptp.'C_c_option_fun$'|) % 140.13/140.49 ; cardinality of |tptp.'C_option$'| is 2 % 140.13/140.49 ; rep: (as |@_tptp.'C_option$'__0| |tptp.'C_option$'|) % 140.13/140.49 ; rep: (as |@_tptp.'C_option$'__1| |tptp.'C_option$'|) % 140.13/140.49 ; cardinality of |tptp.'B_option$'| is 2 % 140.13/140.49 ; rep: (as |@_tptp.'B_option$'__0| |tptp.'B_option$'|) % 140.13/140.49 ; rep: (as |@_tptp.'B_option$'__1| |tptp.'B_option$'|) % 140.13/140.49 ; cardinality of |tptp.'D_d_fun$'| is 1 % 140.13/140.49 ; rep: (as |@_tptp.'D_d_fun$'__0| |tptp.'D_d_fun$'|) % 140.13/140.49 ; cardinality of |tptp.'B_option_c_option_bool_fun_fun$'| is 1 % 140.13/140.49 ; rep: (as |@_tptp.'B_option_c_option_bool_fun_fun$'__0| |tptp.'B_option_c_option_bool_fun_fun$'|) % 140.13/140.49 ; cardinality of |tptp.'B_d_option_fun$'| is 1 % 140.13/140.49 ; rep: (as |@_tptp.'B_d_option_fun$'__0| |tptp.'B_d_option_fun$'|) % 140.13/140.49 ; cardinality of |tptp.'C_c_prod$'| is 1 % 140.13/140.49 ; rep: (as |@_tptp.'C_c_prod$'__0| |tptp.'C_c_prod$'|) % 140.13/140.49 ; cardinality of |tptp.'A_d_prod_set$'| is 1 % 140.13/140.49 ; rep: (as |@_tptp.'A_d_prod_set$'__0| |tptp.'A_d_prod_set$'|) % 140.13/140.49 ; cardinality of |tptp.'C_a_prod_set$'| is 1 % 140.13/140.49 ; rep: (as |@_tptp.'C_a_prod_set$'__0| |tptp.'C_a_prod_set$'|) % 140.13/140.49 ; cardinality of |tptp.'B_b_fun$'| is 1 % 140.13/140.49 ; rep: (as |@_tptp.'B_b_fun$'__0| |tptp.'B_b_fun$'|) % 140.13/140.49 ; cardinality of |tptp.'C_c_c_fun_fun$'| is 1 % 140.13/140.49 ; rep: (as |@_tptp.'C_c_c_fun_fun$'__0| |tptp.'C_c_c_fun_fun$'|) % 140.13/140.49 ; cardinality of |tptp.'C_c_fun$'| is 1 % 140.13/140.49 ; rep: (as |@_tptp.'C_c_fun$'__0| |tptp.'C_c_fun$'|) % 140.13/140.49 ; cardinality of |tptp.'B_option_b_option_fun$'| is 2 % 140.13/140.49 ; rep: (as |@_tptp.'B_option_b_option_fun$'__0| |tptp.'B_option_b_option_fun$'|) % 140.13/140.49 ; rep: (as |@_tptp.'B_option_b_option_fun$'__1| |tptp.'B_option_b_option_fun$'|) % 140.13/140.49 ; cardinality of |tptp.'B_c_option_fun$'| is 1 % 140.13/140.49 ; rep: (as |@_tptp.'B_c_option_fun$'__0| |tptp.'B_c_option_fun$'|) % 140.13/140.49 ; cardinality of |tptp.'C_a_option_fun$'| is 1 % 140.13/140.49 ; rep: (as |@_tptp.'C_a_option_fun$'__0| |tptp.'C_a_option_fun$'|) % 140.13/140.49 ; cardinality of |tptp.'C_a_prod$'| is 1 % 140.13/140.49 ; rep: (as |@_tptp.'C_a_prod$'__0| |tptp.'C_a_prod$'|) % 140.13/140.49 ; cardinality of |tptp.'C_option_set$'| is 4 % 140.13/140.49 ; rep: (as |@_tptp.'C_option_set$'__0| |tptp.'C_option_set$'|) % 140.13/140.49 ; rep: (as |@_tptp.'C_option_set$'__1| |tptp.'C_option_set$'|) % 140.13/140.49 ; rep: (as |@_tptp.'C_option_set$'__2| |tptp.'C_option_set$'|) % 140.13/140.49 ; rep: (as |@_tptp.'C_option_set$'__3| |tptp.'C_option_set$'|) % 140.13/140.49 ; cardinality of |tptp.'D_b_prod_set$'| is 1 % 140.13/140.49 ; rep: (as |@_tptp.'D_b_prod_set$'__0| |tptp.'D_b_prod_set$'|) % 140.13/140.49 ; cardinality of |tptp.'D$'| is 1 % 140.13/140.49 ; rep: (as |@_tptp.'D$'__0| |tptp.'D$'|) % 140.13/140.49 ; cardinality of |tptp.'D_b_option_fun$'| is 1 % 140.13/140.49 ; rep: (as |@_tptp.'D_b_option_fun$'__0| |tptp.'D_b_option_fun$'|) % 140.13/140.49 ; cardinality of |tptp.'D_d_d_fun_fun$'| is 1 % 140.13/140.49 ; rep: (as |@_tptp.'D_d_d_fun_fun$'__0| |tptp.'D_d_d_fun_fun$'|) % 140.13/140.49 ; cardinality of |tptp.'B_d_prod_set$'| is 1 % 140.13/140.49 ; rep: (as |@_tptp.'B_d_prod_set$'__0| |tptp.'B_d_prod_set$'|) % 140.13/140.49 ; cardinality of |tptp.'C_option_c_option_bool_fun_fun$'| is 1 % 140.13/140.49 ; rep: (as |@_tptp.'C_option_c_option_bool_fun_fun$'__0| |tptp.'C_option_c_option_bool_fun_fun$'|) % 140.13/140.49 ; cardinality of |tptp.'D_b_prod$'| is 1 % 140.13/140.49 ; rep: (as |@_tptp.'D_b_prod$'__0| |tptp.'D_b_prod$'|) % 140.13/140.49 ; cardinality of |tptp.'A_b_prod_set$'| is 1 % 140.13/140.49 ; rep: (as |@_tptp.'A_b_prod_set$'__0| |tptp.'A_b_prod_set$'|) % 140.13/140.49 ; cardinality of |tptp.'B_b_prod_set$'| is 2 % 140.13/140.49 ; rep: (as |@_tptp.'B_b_prod_set$'__0| |tptp.'B_b_prod_set$'|) % 140.13/140.49 ; rep: (as |@_tptp.'B_b_prod_set$'__1| |tptp.'B_b_prod_set$'|) % 140.13/140.49 ; cardinality of |tptp.'C_b_option_fun$'| is 1 % 140.13/140.49 ; rep: (as |@_tptp.'C_b_option_fun$'__0| |tptp.'C_b_option_fun$'|) % 140.13/140.49 ; cardinality of |tptp.'B$'| is 1 % 140.13/140.49 ; rep: (as |@_tptp.'B$'__0| |tptp.'B$'|) % 140.13/140.49 ; cardinality of |tptp.'C_option_b_option_bool_fun_fun$'| is 1 % 140.13/140.49 ; rep: (as |@_tptp.'C_option_b_option_bool_fun_fun$'__0| |tptp.'C_option_b_option_bool_fun_fun$'|) % 140.13/140.49 ; cardinality of |tptp.'C_b_prod_bool_fun$'| is 1 % 140.13/140.49 ; rep: (as |@_tptp.'C_b_prod_bool_fun$'__0| |tptp.'C_b_prod_bool_fun$'|) % 140.13/140.49 ; cardinality of |tptp.'C$'| is 1 % 140.13/140.49 ; rep: (as |@_tptp.'C$'__0| |tptp.'C$'|) % 140.13/140.49 ; cardinality of |tptp.'D_option_bool_fun$'| is 1 % 140.13/140.49 ; rep: (as |@_tptp.'D_option_bool_fun$'__0| |tptp.'D_option_bool_fun$'|) % 140.13/140.49 ; cardinality of |tptp.'C_c_prod_set$'| is 1 % 140.13/140.49 ; rep: (as |@_tptp.'C_c_prod_set$'__0| |tptp.'C_c_prod_set$'|) % 140.13/140.49 ; cardinality of |tptp.'A_c_prod_bool_fun$'| is 1 % 140.13/140.49 ; rep: (as |@_tptp.'A_c_prod_bool_fun$'__0| |tptp.'A_c_prod_bool_fun$'|) % 140.13/140.49 ; cardinality of |tptp.'D_option_d_option_bool_fun_fun$'| is 1 % 140.13/140.49 ; rep: (as |@_tptp.'D_option_d_option_bool_fun_fun$'__0| |tptp.'D_option_d_option_bool_fun_fun$'|) % 140.13/140.49 ; cardinality of |tptp.'A_option$'| is 2 % 140.13/140.49 ; rep: (as |@_tptp.'A_option$'__0| |tptp.'A_option$'|) % 140.13/140.49 ; rep: (as |@_tptp.'A_option$'__1| |tptp.'A_option$'|) % 140.13/140.49 ; cardinality of |tptp.'D_a_option_fun$'| is 1 % 140.13/140.49 ; rep: (as |@_tptp.'D_a_option_fun$'__0| |tptp.'D_a_option_fun$'|) % 140.13/140.49 ; cardinality of |tptp.'D_set$'| is 2 % 140.13/140.49 ; rep: (as |@_tptp.'D_set$'__0| |tptp.'D_set$'|) % 140.13/140.49 ; rep: (as |@_tptp.'D_set$'__1| |tptp.'D_set$'|) % 140.13/140.49 ; cardinality of |tptp.'C_d_prod_set$'| is 1 % 140.13/140.49 ; rep: (as |@_tptp.'C_d_prod_set$'__0| |tptp.'C_d_prod_set$'|) % 140.13/140.49 ; cardinality of |tptp.'B_option_d_option_bool_fun_fun$'| is 1 % 140.13/140.49 ; rep: (as |@_tptp.'B_option_d_option_bool_fun_fun$'__0| |tptp.'B_option_d_option_bool_fun_fun$'|) % 140.13/140.49 ; cardinality of |tptp.'A_a_option_fun_a_b_option_fun_fun$'| is 2 % 140.13/140.49 ; rep: (as |@_tptp.'A_a_option_fun_a_b_option_fun_fun$'__0| |tptp.'A_a_option_fun_a_b_option_fun_fun$'|) % 140.13/140.49 ; rep: (as |@_tptp.'A_a_option_fun_a_b_option_fun_fun$'__1| |tptp.'A_a_option_fun_a_b_option_fun_fun$'|) % 140.13/140.49 ; cardinality of |tptp.'D_c_option_fun$'| is 1 % 140.13/140.49 ; rep: (as |@_tptp.'D_c_option_fun$'__0| |tptp.'D_c_option_fun$'|) % 140.13/140.49 ; cardinality of |tptp.'A_c_prod_set$'| is 1 % 140.13/140.49 ; rep: (as |@_tptp.'A_c_prod_set$'__0| |tptp.'A_c_prod_set$'|) % 140.13/140.49 ; cardinality of |tptp.'C_d_prod_bool_fun$'| is 1 % 140.13/140.49 ; rep: (as |@_tptp.'C_d_prod_bool_fun$'__0| |tptp.'C_d_prod_bool_fun$'|) % 140.13/140.49 ; cardinality of |tptp.'B_b_prod$'| is 1 % 140.13/140.49 ; rep: (as |@_tptp.'B_b_prod$'__0| |tptp.'B_b_prod$'|) % 140.13/140.49 ; cardinality of |tptp.'D_option_b_option_bool_fun_fun$'| is 1 % 140.13/140.49 ; rep: (as |@_tptp.'D_option_b_option_bool_fun_fun$'__0| |tptp.'D_option_b_option_bool_fun_fun$'|) % 140.13/140.49 ; cardinality of |tptp.'A_d_option_fun$'| is 1 % 140.13/140.49 ; rep: (as |@_tptp.'A_d_option_fun$'__0| |tptp.'A_d_option_fun$'|) % 140.13/140.49 ; cardinality of |tptp.'B_c_prod_set$'| is 1 % 140.13/140.49 ; rep: (as |@_tptp.'B_c_prod_set$'__0| |tptp.'B_c_prod_set$'|) % 140.13/140.49 ; cardinality of |tptp.'A_a_option_fun$'| is 2 % 140.13/140.49 ; rep: (as |@_tptp.'A_a_option_fun$'__0| |tptp.'A_a_option_fun$'|) % 140.13/140.49 ; rep: (as |@_tptp.'A_a_option_fun$'__1| |tptp.'A_a_option_fun$'|) % 140.13/140.49 ; cardinality of |tptp.'A_d_prod$'| is 1 % 140.13/140.49 ; rep: (as |@_tptp.'A_d_prod$'__0| |tptp.'A_d_prod$'|) % 140.13/140.49 ; cardinality of |tptp.'A_bool_fun$'| is 2 % 140.13/140.49 ; rep: (as |@_tptp.'A_bool_fun$'__0| |tptp.'A_bool_fun$'|) % 140.13/140.49 ; rep: (as |@_tptp.'A_bool_fun$'__1| |tptp.'A_bool_fun$'|) % 140.13/140.49 ; cardinality of |tptp.'A_b_prod$'| is 1 % 140.13/140.49 ; rep: (as |@_tptp.'A_b_prod$'__0| |tptp.'A_b_prod$'|) % 140.13/140.49 ; cardinality of |tptp.'A_set$'| is 2 % 140.13/140.49 ; rep: (as |@_tptp.'A_set$'__0| |tptp.'A_set$'|) % 140.13/140.49 ; rep: (as |@_tptp.'A_set$'__1| |tptp.'A_set$'|) % 140.13/140.49 ; cardinality of |tptp.'A_d_prod_bool_fun$'| is 1 % 140.13/140.49 ; rep: (as |@_tptp.'A_d_prod_bool_fun$'__0| |tptp.'A_d_prod_bool_fun$'|) % 140.13/140.49 ; cardinality of |tptp.'A_a_option_fun_a_d_option_fun_fun$'| is 1 % 140.13/140.49 ; rep: (as |@_tptp.'A_a_option_fun_a_d_option_fun_fun$'__0| |tptp.'A_a_option_fun_a_d_option_fun_fun$'|) % 140.13/140.49 ; cardinality of |tptp.'C_bool_fun$'| is 2 % 140.13/140.49 ; rep: (as |@_tptp.'C_bool_fun$'__0| |tptp.'C_bool_fun$'|) % 140.13/140.49 ; rep: (as |@_tptp.'C_bool_fun$'__1| |tptp.'C_bool_fun$'|) % 140.13/140.49 ; cardinality of |tptp.'B_set$'| is 2 % 140.13/140.49 ; rep: (as |@_tptp.'B_set$'__0| |tptp.'B_set$'|) % 140.13/140.49 ; rep: (as |@_tptp.'B_set$'__1| |tptp.'B_set$'|) % 140.13/140.49 ; cardinality of |tptp.'D_option_d_option_fun$'| is 2 % 140.13/140.49 ; rep: (as |@_tptp.'D_option_d_option_fun$'__0| |tptp.'D_option_d_option_fun$'|) % 140.13/140.49 ; rep: (as |@_tptp.'D_option_d_option_fun$'__1| |tptp.'D_option_d_option_fun$'|) % 140.13/140.49 ; cardinality of |tptp.'A$'| is 1 % 140.13/140.49 ; rep: (as |@_tptp.'A$'__0| |tptp.'A$'|) % 140.13/140.49 ; cardinality of |tptp.'A_c_prod$'| is 1 % 140.13/140.49 ; rep: (as |@_tptp.'A_c_prod$'__0| |tptp.'A_c_prod$'|) % 140.13/140.49 ; cardinality of |tptp.'B_option_option$'| is 3 % 140.13/140.49 ; rep: (as |@_tptp.'B_option_option$'__0| |tptp.'B_option_option$'|) % 140.13/140.49 ; rep: (as |@_tptp.'B_option_option$'__1| |tptp.'B_option_option$'|) % 140.13/140.49 ; rep: (as |@_tptp.'B_option_option$'__2| |tptp.'B_option_option$'|) % 140.13/140.49 ; cardinality of |tptp.'A_b_option_fun$'| is 2 % 140.13/140.49 ; rep: (as |@_tptp.'A_b_option_fun$'__0| |tptp.'A_b_option_fun$'|) % 140.13/140.49 ; rep: (as |@_tptp.'A_b_option_fun$'__1| |tptp.'A_b_option_fun$'|) % 140.13/140.49 ; cardinality of |tptp.'D_option_set$'| is 2 % 140.13/140.49 ; rep: (as |@_tptp.'D_option_set$'__0| |tptp.'D_option_set$'|) % 140.13/140.49 ; rep: (as |@_tptp.'D_option_set$'__1| |tptp.'D_option_set$'|) % 140.13/140.49 ; cardinality of |tptp.'B_a_option_fun$'| is 1 % 140.13/140.49 ; rep: (as |@_tptp.'B_a_option_fun$'__0| |tptp.'B_a_option_fun$'|) % 140.13/140.49 ; cardinality of |tptp.'C_option_c_option_fun$'| is 2 % 140.13/140.49 ; rep: (as |@_tptp.'C_option_c_option_fun$'__0| |tptp.'C_option_c_option_fun$'|) % 140.13/140.49 ; rep: (as |@_tptp.'C_option_c_option_fun$'__1| |tptp.'C_option_c_option_fun$'|) % 140.13/140.49 ; cardinality of |tptp.'C_option_d_option_bool_fun_fun$'| is 1 % 140.13/140.49 ; rep: (as |@_tptp.'C_option_d_option_bool_fun_fun$'__0| |tptp.'C_option_d_option_bool_fun_fun$'|) % 140.13/140.49 ; cardinality of |tptp.'D_d_option_fun_d_option_fun$'| is 2 % 140.13/140.49 ; rep: (as |@_tptp.'D_d_option_fun_d_option_fun$'__0| |tptp.'D_d_option_fun_d_option_fun$'|) % 140.13/140.49 ; rep: (as |@_tptp.'D_d_option_fun_d_option_fun$'__1| |tptp.'D_d_option_fun_d_option_fun$'|) % 140.13/140.49 ; cardinality of |tptp.'B_b_b_fun_fun$'| is 1 % 140.13/140.49 ; rep: (as |@_tptp.'B_b_b_fun_fun$'__0| |tptp.'B_b_b_fun_fun$'|) % 140.13/140.49 ; cardinality of |tptp.'D_option_c_option_bool_fun_fun$'| is 1 % 140.13/140.49 ; rep: (as |@_tptp.'D_option_c_option_bool_fun_fun$'__0| |tptp.'D_option_c_option_bool_fun_fun$'|) % 140.13/140.49 ; cardinality of |tptp.'B_b_option_fun$'| is 2 % 140.13/140.49 ; rep: (as |@_tptp.'B_b_option_fun$'__0| |tptp.'B_b_option_fun$'|) % 140.13/140.49 ; rep: (as |@_tptp.'B_b_option_fun$'__1| |tptp.'B_b_option_fun$'|) % 140.13/140.49 ; cardinality of |tptp.'C_option_option$'| is 2 % 140.13/140.49 ; rep: (as |@_tptp.'C_option_option$'__0| |tptp.'C_option_option$'|) % 140.13/140.49 ; rep: (as |@_tptp.'C_option_option$'__1| |tptp.'C_option_option$'|) % 140.13/140.49 ; cardinality of |tptp.'A_b_prod_bool_fun$'| is 1 % 140.13/140.49 ; rep: (as |@_tptp.'A_b_prod_bool_fun$'__0| |tptp.'A_b_prod_bool_fun$'|) % 140.13/140.49 ; cardinality of |tptp.'C_option_bool_fun$'| is 1 % 140.13/140.49 ; rep: (as |@_tptp.'C_option_bool_fun$'__0| |tptp.'C_option_bool_fun$'|) % 140.13/140.49 ; cardinality of |tptp.'D_option$'| is 2 % 140.13/140.49 ; rep: (as |@_tptp.'D_option$'__0| |tptp.'D_option$'|) % 140.13/140.49 ; rep: (as |@_tptp.'D_option$'__1| |tptp.'D_option$'|) % 140.13/140.49 ; cardinality of |tptp.'A_a_option_fun_a_c_option_fun_fun$'| is 1 % 140.13/140.49 ; rep: (as |@_tptp.'A_a_option_fun_a_c_option_fun_fun$'__0| |tptp.'A_a_option_fun_a_c_option_fun_fun$'|) % 140.13/140.49 ; cardinality of |tptp.'C_c_option_fun_c_option_fun$'| is 2 % 140.13/140.49 ; rep: (as |@_tptp.'C_c_option_fun_c_option_fun$'__0| |tptp.'C_c_option_fun_c_option_fun$'|) % 140.13/140.49 ; rep: (as |@_tptp.'C_c_option_fun_c_option_fun$'__1| |tptp.'C_c_option_fun_c_option_fun$'|) % 140.13/140.49 ; cardinality of |tptp.'C_b_prod$'| is 1 % 140.13/140.49 ; rep: (as |@_tptp.'C_b_prod$'__0| |tptp.'C_b_prod$'|) % 140.13/140.49 ; cardinality of |tptp.'C_d_prod$'| is 1 % 140.13/140.49 ; rep: (as |@_tptp.'C_d_prod$'__0| |tptp.'C_d_prod$'|) % 140.13/140.49 ; cardinality of |tptp.'C_d_option_fun$'| is 1 % 140.13/140.49 ; rep: (as |@_tptp.'C_d_option_fun$'__0| |tptp.'C_d_option_fun$'|) % 140.13/140.49 ; cardinality of |tptp.'B_option_bool_fun$'| is 4 % 140.13/140.49 ; rep: (as |@_tptp.'B_option_bool_fun$'__0| |tptp.'B_option_bool_fun$'|) % 140.13/140.49 ; rep: (as |@_tptp.'B_option_bool_fun$'__1| |tptp.'B_option_bool_fun$'|) % 140.13/140.49 ; rep: (as |@_tptp.'B_option_bool_fun$'__2| |tptp.'B_option_bool_fun$'|) % 140.13/140.49 ; rep: (as |@_tptp.'B_option_bool_fun$'__3| |tptp.'B_option_bool_fun$'|) % 140.13/140.49 ; cardinality of |tptp.'D_d_prod$'| is 1 % 140.13/140.49 ; rep: (as |@_tptp.'D_d_prod$'__0| |tptp.'D_d_prod$'|) % 140.13/140.49 ; cardinality of |tptp.'C_set$'| is 2 % 140.13/140.49 ; rep: (as |@_tptp.'C_set$'__0| |tptp.'C_set$'|) % 140.13/140.49 ; rep: (as |@_tptp.'C_set$'__1| |tptp.'C_set$'|) % 140.13/140.49 ; cardinality of |tptp.'B_option_b_option_bool_fun_fun$'| is 1 % 140.13/140.49 ; rep: (as |@_tptp.'B_option_b_option_bool_fun_fun$'__0| |tptp.'B_option_b_option_bool_fun_fun$'|) % 140.13/140.49 ; cardinality of |tptp.'B_bool_fun$'| is 2 % 140.13/140.49 ; rep: (as |@_tptp.'B_bool_fun$'__0| |tptp.'B_bool_fun$'|) % 140.13/140.49 ; rep: (as |@_tptp.'B_bool_fun$'__1| |tptp.'B_bool_fun$'|) % 140.13/140.49 ; cardinality of |tptp.'D_d_option_fun$'| is 2 % 140.13/140.49 ; rep: (as |@_tptp.'D_d_option_fun$'__0| |tptp.'D_d_option_fun$'|) % 140.13/140.49 ; rep: (as |@_tptp.'D_d_option_fun$'__1| |tptp.'D_d_option_fun$'|) % 140.13/140.49 ; cardinality of |tptp.'A_c_option_fun$'| is 1 % 140.13/140.49 ; rep: (as |@_tptp.'A_c_option_fun$'__0| |tptp.'A_c_option_fun$'|) % 140.13/140.49 ; cardinality of |tptp.'B_option_set$'| is 4 % 140.13/140.49 ; rep: (as |@_tptp.'B_option_set$'__0| |tptp.'B_option_set$'|) % 140.13/140.49 ; rep: (as |@_tptp.'B_option_set$'__1| |tptp.'B_option_set$'|) % 140.13/140.49 ; rep: (as |@_tptp.'B_option_set$'__2| |tptp.'B_option_set$'|) % 140.13/140.49 ; rep: (as |@_tptp.'B_option_set$'__3| |tptp.'B_option_set$'|) % 140.13/140.49 ; cardinality of |tptp.'C_b_prod_set$'| is 1 % 140.13/140.49 ; rep: (as |@_tptp.'C_b_prod_set$'__0| |tptp.'C_b_prod_set$'|) % 140.13/140.49 (define-fun |tptp.'relcomp$a'| (($x1 |tptp.'C_d_prod_set$'|) ($x2 |tptp.'D_b_prod_set$'|)) |tptp.'C_b_prod_set$'| (as |@_tptp.'C_b_prod_set$'__0| |tptp.'C_b_prod_set$'|)) % 140.13/140.49 (define-fun |tptp.'the_elem$'| (($x1 |tptp.'B_option_set$'|)) |tptp.'B_option$'| (ite (= (as |@_tptp.'B_option_set$'__1| |tptp.'B_option_set$'|) $x1) (as |@_tptp.'B_option$'__0| |tptp.'B_option$'|) (as |@_tptp.'B_option$'__1| |tptp.'B_option$'|))) % 140.13/140.49 (define-fun |tptp.'fun_app$g'| (($x1 |tptp.'A_a_option_fun_a_b_option_fun_fun$'|) ($x2 |tptp.'A_a_option_fun$'|)) |tptp.'A_b_option_fun$'| (ite (and (= (as |@_tptp.'A_a_option_fun_a_b_option_fun_fun$'__0| |tptp.'A_a_option_fun_a_b_option_fun_fun$'|) $x1) (= (as |@_tptp.'A_a_option_fun$'__0| |tptp.'A_a_option_fun$'|) $x2)) (as |@_tptp.'A_b_option_fun$'__0| |tptp.'A_b_option_fun$'|) (ite (and (= (as |@_tptp.'A_a_option_fun_a_b_option_fun_fun$'__1| |tptp.'A_a_option_fun_a_b_option_fun_fun$'|) $x1) (= (as |@_tptp.'A_a_option_fun$'__1| |tptp.'A_a_option_fun$'|) $x2)) (as |@_tptp.'A_b_option_fun$'__0| |tptp.'A_b_option_fun$'|) (as |@_tptp.'A_b_option_fun$'__1| |tptp.'A_b_option_fun$'|)))) % 140.13/140.49 (define-fun |tptp.'pair$g'| (($x1 |tptp.'A$'|) ($x2 |tptp.'D$'|)) |tptp.'A_d_prod$'| (as |@_tptp.'A_d_prod$'__0| |tptp.'A_d_prod$'|)) % 140.13/140.49 (define-fun |tptp.'image$c'| (($x1 |tptp.'A_b_prod_set$'|) ($x2 |tptp.'A_set$'|)) |tptp.'B_set$'| (as |@_tptp.'B_set$'__0| |tptp.'B_set$'|)) % 140.13/140.49 (define-fun |tptp.'fun_app$m'| ((BOUND_VARIABLE_58370 |tptp.'C_b_option_fun$'|) (BOUND_VARIABLE_58372 |tptp.'C$'|)) |tptp.'B_option$'| (as |@_tptp.'B_option$'__0| |tptp.'B_option$'|)) % 140.13/140.49 (define-fun |tptp.'insert$c'| (($x1 |tptp.'C$'|) ($x2 |tptp.'C_set$'|)) |tptp.'C_set$'| (as |@_tptp.'C_set$'__1| |tptp.'C_set$'|)) % 140.13/140.49 (define-fun |tptp.'relcomp$r'| (($x1 |tptp.'A_a_prod_set$'|) ($x2 |tptp.'A_b_prod_set$'|)) |tptp.'A_b_prod_set$'| (as |@_tptp.'A_b_prod_set$'__0| |tptp.'A_b_prod_set$'|)) % 140.13/140.49 (define-fun |tptp.'map_comp$g'| (($x1 |tptp.'A_d_option_fun$'|) ($x2 |tptp.'C_a_option_fun$'|)) |tptp.'C_d_option_fun$'| (as |@_tptp.'C_d_option_fun$'__0| |tptp.'C_d_option_fun$'|)) % 140.13/140.49 (define-fun |tptp.'dom$d'| (($x1 |tptp.'A_b_option_fun$'|)) |tptp.'A_set$'| (as |@_tptp.'A_set$'__0| |tptp.'A_set$'|)) % 140.13/140.49 (define-fun |tptp.'member$b'| ((BOUND_VARIABLE_9510 |tptp.'C$'|) (BOUND_VARIABLE_9511 |tptp.'C_set$'|)) Bool (and (= (as |@_tptp.'C_bool_fun$'__0| |tptp.'C_bool_fun$'|) (ite (= BOUND_VARIABLE_9511 (as |@_tptp.'C_set$'__1| |tptp.'C_set$'|)) (as |@_tptp.'C_bool_fun$'__0| |tptp.'C_bool_fun$'|) (as |@_tptp.'C_bool_fun$'__1| |tptp.'C_bool_fun$'|))) (= BOUND_VARIABLE_9510 (as |@_tptp.'C$'__0| |tptp.'C$'|)))) % 140.13/140.49 (define-fun |tptp.'bind$h'| (($x1 |tptp.'B_option$'|)) |tptp.'B_b_option_fun_b_option_fun$'| (ite (= (as |@_tptp.'B_option$'__0| |tptp.'B_option$'|) $x1) (as |@_tptp.'B_b_option_fun_b_option_fun$'__0| |tptp.'B_b_option_fun_b_option_fun$'|) (as |@_tptp.'B_b_option_fun_b_option_fun$'__1| |tptp.'B_b_option_fun_b_option_fun$'|))) % 140.13/140.49 (define-fun |tptp.'fun_upd$b'| (($x1 |tptp.'A_d_option_fun$'|) ($x2 |tptp.'A$'|) ($x3 |tptp.'D_option$'|)) |tptp.'A_d_option_fun$'| (as |@_tptp.'A_d_option_fun$'__0| |tptp.'A_d_option_fun$'|)) % 140.13/140.49 (define-fun |tptp.'less_eq$a'| (($x1 |tptp.'C_d_prod_set$'|) ($x2 |tptp.'C_d_prod_set$'|)) Bool false) % 140.13/140.49 (define-fun |tptp.'restrict_map$i'| (($x1 |tptp.'A_b_option_fun$'|) ($x2 |tptp.'A_set$'|)) |tptp.'A_b_option_fun$'| (ite (and (= (as |@_tptp.'A_b_option_fun$'__1| |tptp.'A_b_option_fun$'|) $x1) (= (as |@_tptp.'A_set$'__0| |tptp.'A_set$'|) $x2)) (as |@_tptp.'A_b_option_fun$'__0| |tptp.'A_b_option_fun$'|) (ite (and (= (as |@_tptp.'A_b_option_fun$'__0| |tptp.'A_b_option_fun$'|) $x1) (= (as |@_tptp.'A_set$'__0| |tptp.'A_set$'|) $x2)) (as |@_tptp.'A_b_option_fun$'__0| |tptp.'A_b_option_fun$'|) (ite (and (= (as |@_tptp.'A_b_option_fun$'__1| |tptp.'A_b_option_fun$'|) $x1) (= (as |@_tptp.'A_set$'__1| |tptp.'A_set$'|) $x2)) (as |@_tptp.'A_b_option_fun$'__0| |tptp.'A_b_option_fun$'|) (as |@_tptp.'A_b_option_fun$'__1| |tptp.'A_b_option_fun$'|))))) % 140.13/140.49 (define-fun |tptp.'some$a'| () |tptp.'C_c_option_fun$'| (as |@_tptp.'C_c_option_fun$'__0| |tptp.'C_c_option_fun$'|)) % 140.13/140.49 (define-fun |tptp.'collect$'| (($x1 |tptp.'B_option_bool_fun$'|)) |tptp.'B_option_set$'| (ite (= (as |@_tptp.'B_option_bool_fun$'__0| |tptp.'B_option_bool_fun$'|) $x1) (as |@_tptp.'B_option_set$'__0| |tptp.'B_option_set$'|) (ite (= (as |@_tptp.'B_option_bool_fun$'__1| |tptp.'B_option_bool_fun$'|) $x1) (as |@_tptp.'B_option_set$'__1| |tptp.'B_option_set$'|) (ite (= (as |@_tptp.'B_option_bool_fun$'__3| |tptp.'B_option_bool_fun$'|) $x1) (as |@_tptp.'B_option_set$'__2| |tptp.'B_option_set$'|) (as |@_tptp.'B_option_set$'__3| |tptp.'B_option_set$'|))))) % 140.13/140.49 (define-fun |tptp.'fun_app$y'| (($x1 |tptp.'D_option_d_option_bool_fun_fun$'|) ($x2 |tptp.'D_option$'|)) |tptp.'D_option_bool_fun$'| (as |@_tptp.'D_option_bool_fun$'__0| |tptp.'D_option_bool_fun$'|)) % 140.13/140.49 (define-fun |tptp.'fun_app$af'| (($x1 |tptp.'D_d_option_fun_d_option_fun$'|) ($x2 |tptp.'D_d_option_fun$'|)) |tptp.'D_option$'| (ite (and (= (as |@_tptp.'D_d_option_fun_d_option_fun$'__0| |tptp.'D_d_option_fun_d_option_fun$'|) $x1) (= (as |@_tptp.'D_d_option_fun$'__0| |tptp.'D_d_option_fun$'|) $x2)) (as |@_tptp.'D_option$'__0| |tptp.'D_option$'|) (ite (and (= (as |@_tptp.'D_d_option_fun_d_option_fun$'__0| |tptp.'D_d_option_fun_d_option_fun$'|) $x1) (= (as |@_tptp.'D_d_option_fun$'__1| |tptp.'D_d_option_fun$'|) $x2)) (as |@_tptp.'D_option$'__0| |tptp.'D_option$'|) (ite (and (= (as |@_tptp.'D_d_option_fun_d_option_fun$'__1| |tptp.'D_d_option_fun_d_option_fun$'|) $x1) (= (as |@_tptp.'D_d_option_fun$'__1| |tptp.'D_d_option_fun$'|) $x2)) (as |@_tptp.'D_option$'__0| |tptp.'D_option$'|) (as |@_tptp.'D_option$'__1| |tptp.'D_option$'|))))) % 140.13/140.49 (define-fun |tptp.'relcomp$t'| (($x1 |tptp.'A_b_prod_set$'|) ($x2 |tptp.'B_c_prod_set$'|)) |tptp.'A_c_prod_set$'| (as |@_tptp.'A_c_prod_set$'__0| |tptp.'A_c_prod_set$'|)) % 140.13/140.49 (define-fun |tptp.'less_eq$e'| (($x1 |tptp.'C_b_prod_set$'|) ($x2 |tptp.'C_b_prod_set$'|)) Bool true) % 140.13/140.49 (define-fun |tptp.'member$m'| (($x1 |tptp.'C_b_prod$'|) ($x2 |tptp.'C_b_prod_set$'|)) Bool false) % 140.13/140.49 (define-fun |tptp.'member$c'| ((BOUND_VARIABLE_9521 |tptp.'B$'|) (BOUND_VARIABLE_9522 |tptp.'B_set$'|)) Bool (and (= (as |@_tptp.'B_bool_fun$'__0| |tptp.'B_bool_fun$'|) (ite (= BOUND_VARIABLE_9522 (as |@_tptp.'B_set$'__1| |tptp.'B_set$'|)) (as |@_tptp.'B_bool_fun$'__0| |tptp.'B_bool_fun$'|) (as |@_tptp.'B_bool_fun$'__1| |tptp.'B_bool_fun$'|))) (= BOUND_VARIABLE_9521 (as |@_tptp.'B$'__0| |tptp.'B$'|)))) % 140.13/140.49 (define-fun |tptp.'insert$e'| (($x1 |tptp.'B$'|) ($x2 |tptp.'B_set$'|)) |tptp.'B_set$'| (as |@_tptp.'B_set$'__1| |tptp.'B_set$'|)) % 140.13/140.49 (define-fun |tptp.'fun_app$ab'| (($x1 |tptp.'B_option_d_option_bool_fun_fun$'|) ($x2 |tptp.'B_option$'|)) |tptp.'D_option_bool_fun$'| (as |@_tptp.'D_option_bool_fun$'__0| |tptp.'D_option_bool_fun$'|)) % 140.13/140.49 (define-fun |tptp.'bot$m'| () |tptp.'B_option_set$'| (as |@_tptp.'B_option_set$'__0| |tptp.'B_option_set$'|)) % 140.13/140.49 (define-fun |tptp.'inj_on$a'| (($x1 |tptp.'D_d_option_fun$'|) ($x2 |tptp.'D_set$'|)) Bool true) % 140.13/140.49 (define-fun |tptp.'member$d'| ((BOUND_VARIABLE_9532 |tptp.'A$'|) (BOUND_VARIABLE_9533 |tptp.'A_set$'|)) Bool (and (= (as |@_tptp.'A_bool_fun$'__1| |tptp.'A_bool_fun$'|) (ite (= BOUND_VARIABLE_9533 (as |@_tptp.'A_set$'__0| |tptp.'A_set$'|)) (as |@_tptp.'A_bool_fun$'__0| |tptp.'A_bool_fun$'|) (as |@_tptp.'A_bool_fun$'__1| |tptp.'A_bool_fun$'|))) (= BOUND_VARIABLE_9532 (as |@_tptp.'A$'__0| |tptp.'A$'|)))) % 140.13/140.49 (define-fun |tptp.'graph$i'| (($x1 |tptp.'B_d_option_fun$'|)) |tptp.'B_d_prod_set$'| (as |@_tptp.'B_d_prod_set$'__0| |tptp.'B_d_prod_set$'|)) % 140.13/140.49 (define-fun |tptp.'map_add$d'| (($x1 |tptp.'A_b_option_fun$'|) ($x2 |tptp.'A_b_option_fun$'|)) |tptp.'A_b_option_fun$'| (ite (and (= (as |@_tptp.'A_b_option_fun$'__0| |tptp.'A_b_option_fun$'|) $x1) (= (as |@_tptp.'A_b_option_fun$'__1| |tptp.'A_b_option_fun$'|) $x2)) (as |@_tptp.'A_b_option_fun$'__0| |tptp.'A_b_option_fun$'|) (ite (and (= (as |@_tptp.'A_b_option_fun$'__1| |tptp.'A_b_option_fun$'|) $x1) (= (as |@_tptp.'A_b_option_fun$'__0| |tptp.'A_b_option_fun$'|) $x2)) (as |@_tptp.'A_b_option_fun$'__0| |tptp.'A_b_option_fun$'|) (as |@_tptp.'A_b_option_fun$'__1| |tptp.'A_b_option_fun$'|)))) % 140.13/140.49 (define-fun |tptp.'fun_app$ax'| (($x1 |tptp.'D_a_option_fun$'|) ($x2 |tptp.'D$'|)) |tptp.'A_option$'| (as |@_tptp.'A_option$'__0| |tptp.'A_option$'|)) % 140.13/140.49 (define-fun |tptp.'member$f'| (($x1 |tptp.'A_a_prod$'|) ($x2 |tptp.'A_a_prod_set$'|)) Bool (and (= (as |@_tptp.'A_a_prod$'__0| |tptp.'A_a_prod$'|) $x1) (= (as |@_tptp.'A_a_prod_set$'__1| |tptp.'A_a_prod_set$'|) $x2))) % 140.13/140.49 (define-fun |tptp.'the$d'| (($x1 |tptp.'A_option$'|)) |tptp.'A$'| (as |@_tptp.'A$'__0| |tptp.'A$'|)) % 140.13/140.49 (define-fun |tptp.'image$f'| (($x1 |tptp.'C_c_option_fun$'|) ($x2 |tptp.'C_set$'|)) |tptp.'C_option_set$'| (ite (and (= (as |@_tptp.'C_c_option_fun$'__0| |tptp.'C_c_option_fun$'|) $x1) (= (as |@_tptp.'C_set$'__1| |tptp.'C_set$'|) $x2)) (as |@_tptp.'C_option_set$'__0| |tptp.'C_option_set$'|) (as |@_tptp.'C_option_set$'__1| |tptp.'C_option_set$'|))) % 140.13/140.49 (define-fun |tptp.'fun_app$ad'| (($x1 |tptp.'C_c_option_fun_c_option_fun$'|) ($x2 |tptp.'C_c_option_fun$'|)) |tptp.'C_option$'| (ite (and (= (as |@_tptp.'C_c_option_fun_c_option_fun$'__0| |tptp.'C_c_option_fun_c_option_fun$'|) $x1) (= (as |@_tptp.'C_c_option_fun$'__0| |tptp.'C_c_option_fun$'|) $x2)) (as |@_tptp.'C_option$'__0| |tptp.'C_option$'|) (ite (and (= (as |@_tptp.'C_c_option_fun_c_option_fun$'__0| |tptp.'C_c_option_fun_c_option_fun$'|) $x1) (= (as |@_tptp.'C_c_option_fun$'__1| |tptp.'C_c_option_fun$'|) $x2)) (as |@_tptp.'C_option$'__0| |tptp.'C_option$'|) (ite (and (= (as |@_tptp.'C_c_option_fun_c_option_fun$'__1| |tptp.'C_c_option_fun_c_option_fun$'|) $x1) (= (as |@_tptp.'C_c_option_fun$'__1| |tptp.'C_c_option_fun$'|) $x2)) (as |@_tptp.'C_option$'__0| |tptp.'C_option$'|) (as |@_tptp.'C_option$'__1| |tptp.'C_option$'|))))) % 140.13/140.49 (define-fun |tptp.'member$o'| (($x1 |tptp.'D_b_prod$'|) ($x2 |tptp.'D_b_prod_set$'|)) Bool true) % 140.13/140.49 (define-fun |tptp.'fun_app$j'| (($x1 |tptp.'C_d_option_fun$'|) ($x2 |tptp.'C$'|)) |tptp.'D_option$'| (as |@_tptp.'D_option$'__0| |tptp.'D_option$'|)) % 140.13/140.49 (define-fun |tptp.'uub$'| (($x1 |tptp.'C_set$'|)) |tptp.'C_bool_fun$'| (ite (= (as |@_tptp.'C_set$'__1| |tptp.'C_set$'|) $x1) (as |@_tptp.'C_bool_fun$'__0| |tptp.'C_bool_fun$'|) (as |@_tptp.'C_bool_fun$'__1| |tptp.'C_bool_fun$'|))) % 140.13/140.49 (define-fun |tptp.'finite$'| (($x1 |tptp.'C_d_prod_set$'|)) Bool true) % 140.13/140.49 (define-fun |tptp.'fun_app$e'| (($x1 |tptp.'A_a_option_fun_a_d_option_fun_fun$'|) ($x2 |tptp.'A_a_option_fun$'|)) |tptp.'A_d_option_fun$'| (as |@_tptp.'A_d_option_fun$'__0| |tptp.'A_d_option_fun$'|)) % 140.13/140.49 (define-fun |tptp.'member$g'| (($x1 |tptp.'B_c_prod$'|) ($x2 |tptp.'B_c_prod_set$'|)) Bool false) % 140.13/140.49 (define-fun |tptp.'bot$e'| () |tptp.'A_c_prod_set$'| (as |@_tptp.'A_c_prod_set$'__0| |tptp.'A_c_prod_set$'|)) % 140.13/140.49 (define-fun |tptp.'pair$i'| (($x1 |tptp.'A$'|) ($x2 |tptp.'B$'|)) |tptp.'A_b_prod$'| (as |@_tptp.'A_b_prod$'__0| |tptp.'A_b_prod$'|)) % 140.13/140.49 (define-fun |tptp.'member$j'| (($x1 |tptp.'A_c_prod$'|) ($x2 |tptp.'A_c_prod_set$'|)) Bool false) % 140.13/140.49 (define-fun |tptp.'restrict_map$'| (($x1 |tptp.'C_a_option_fun$'|) ($x2 |tptp.'C_set$'|)) |tptp.'C_a_option_fun$'| (as |@_tptp.'C_a_option_fun$'__0| |tptp.'C_a_option_fun$'|)) % 140.13/140.49 (define-fun |tptp.'inj_on$'| (($x1 |tptp.'C_c_option_fun$'|) ($x2 |tptp.'C_set$'|)) Bool true) % 140.13/140.49 (define-fun |tptp.'fun_app$i'| (($x1 |tptp.'A_a_option_fun$'|) ($x2 |tptp.'A$'|)) |tptp.'A_option$'| (ite (and (= (as |@_tptp.'A_a_option_fun$'__1| |tptp.'A_a_option_fun$'|) $x1) (= (as |@_tptp.'A$'__0| |tptp.'A$'|) $x2)) (as |@_tptp.'A_option$'__0| |tptp.'A_option$'|) (as |@_tptp.'A_option$'__1| |tptp.'A_option$'|))) % 140.13/140.49 (define-fun |tptp.'none$d'| () |tptp.'B_option_option$'| (as |@_tptp.'B_option_option$'__0| |tptp.'B_option_option$'|)) % 140.13/140.49 (define-fun |tptp.'finite$a'| (($x1 |tptp.'C_set$'|)) Bool true) % 140.13/140.49 (define-fun |tptp.'map_comp$c'| (($x1 |tptp.'C_d_option_fun$'|) ($x2 |tptp.'A_c_option_fun$'|)) |tptp.'A_d_option_fun$'| (as |@_tptp.'A_d_option_fun$'__0| |tptp.'A_d_option_fun$'|)) % 140.13/140.49 (define-fun |tptp.'member$i'| (($x1 |tptp.'B_b_prod$'|) ($x2 |tptp.'B_b_prod_set$'|)) Bool (and (= (as |@_tptp.'B_b_prod$'__0| |tptp.'B_b_prod$'|) $x1) (= (as |@_tptp.'B_b_prod_set$'__1| |tptp.'B_b_prod_set$'|) $x2))) % 140.13/140.49 (define-fun |tptp.'restrict_map$e'| (($x1 |tptp.'A_c_option_fun$'|) ($x2 |tptp.'A_set$'|)) |tptp.'A_c_option_fun$'| (as |@_tptp.'A_c_option_fun$'__0| |tptp.'A_c_option_fun$'|)) % 140.13/140.49 (define-fun |tptp.'relcomp$m'| (($x1 |tptp.'C_b_prod_set$'|) ($x2 |tptp.'B_b_prod_set$'|)) |tptp.'C_b_prod_set$'| (as |@_tptp.'C_b_prod_set$'__0| |tptp.'C_b_prod_set$'|)) % 140.13/140.49 (define-fun |tptp.'inf$'| (($x1 |tptp.'C_set$'|) ($x2 |tptp.'C_set$'|)) |tptp.'C_set$'| (as |@_tptp.'C_set$'__1| |tptp.'C_set$'|)) % 140.13/140.49 (define-fun |tptp.'relcomp$d'| (($x1 |tptp.'C_c_prod_set$'|) ($x2 |tptp.'C_d_prod_set$'|)) |tptp.'C_d_prod_set$'| (as |@_tptp.'C_d_prod_set$'__0| |tptp.'C_d_prod_set$'|)) % 140.13/140.49 (define-fun |tptp.'these$b'| (($x1 |tptp.'B_option_set$'|)) |tptp.'B_set$'| (ite (= (as |@_tptp.'B_option_set$'__0| |tptp.'B_option_set$'|) $x1) (as |@_tptp.'B_set$'__0| |tptp.'B_set$'|) (ite (= (as |@_tptp.'B_option_set$'__1| |tptp.'B_option_set$'|) $x1) (as |@_tptp.'B_set$'__0| |tptp.'B_set$'|) (as |@_tptp.'B_set$'__1| |tptp.'B_set$'|)))) % 140.13/140.49 (define-fun |tptp.'these$a'| (($x1 |tptp.'D_option_set$'|)) |tptp.'D_set$'| (ite (= (as |@_tptp.'D_option_set$'__1| |tptp.'D_option_set$'|) $x1) (as |@_tptp.'D_set$'__0| |tptp.'D_set$'|) (as |@_tptp.'D_set$'__1| |tptp.'D_set$'|))) % 140.13/140.49 (define-fun |tptp.'bot$l'| () |tptp.'D_b_prod_set$'| (as |@_tptp.'D_b_prod_set$'__0| |tptp.'D_b_prod_set$'|)) % 140.13/140.49 (define-fun |tptp.'pair$a'| (($x1 |tptp.'A$'|) ($x2 |tptp.'A$'|)) |tptp.'A_a_prod$'| (as |@_tptp.'A_a_prod$'__0| |tptp.'A_a_prod$'|)) % 140.13/140.49 (define-fun |tptp.'restrict_map$a'| (($x1 |tptp.'A_a_option_fun$'|) ($x2 |tptp.'A_set$'|)) |tptp.'A_a_option_fun$'| (ite (and (= (as |@_tptp.'A_a_option_fun$'__0| |tptp.'A_a_option_fun$'|) $x1) (= (as |@_tptp.'A_set$'__1| |tptp.'A_set$'|) $x2)) (as |@_tptp.'A_a_option_fun$'__0| |tptp.'A_a_option_fun$'|) (as |@_tptp.'A_a_option_fun$'__1| |tptp.'A_a_option_fun$'|))) % 140.13/140.49 (define-fun |tptp.'fun_app$t'| (($x1 |tptp.'D_option_bool_fun$'|) ($x2 |tptp.'D_option$'|)) Bool (and (= (as |@_tptp.'D_option_bool_fun$'__0| |tptp.'D_option_bool_fun$'|) $x1) (= (as |@_tptp.'D_option$'__0| |tptp.'D_option$'|) $x2))) % 140.13/140.49 (define-fun |tptp.'graph$h'| (($x1 |tptp.'D_d_option_fun$'|)) |tptp.'D_d_prod_set$'| (as |@_tptp.'D_d_prod_set$'__0| |tptp.'D_d_prod_set$'|)) % 140.13/140.49 (define-fun |tptp.'finite$e'| (($x1 |tptp.'A_c_prod_set$'|)) Bool true) % 140.13/140.49 (define-fun |tptp.'fun_app$ae'| (($x1 |tptp.'D_c_option_fun$'|) ($x2 |tptp.'D$'|)) |tptp.'C_option$'| (as |@_tptp.'C_option$'__0| |tptp.'C_option$'|)) % 140.13/140.49 (define-fun |tptp.'fun_app$l'| (($x1 |tptp.'A_d_option_fun$'|) ($x2 |tptp.'A$'|)) |tptp.'D_option$'| (as |@_tptp.'D_option$'__0| |tptp.'D_option$'|)) % 140.13/140.49 (define-fun |tptp.'restrict_map$f'| (($x1 |tptp.'C_d_option_fun$'|) ($x2 |tptp.'C_set$'|)) |tptp.'C_d_option_fun$'| (as |@_tptp.'C_d_option_fun$'__0| |tptp.'C_d_option_fun$'|)) % 140.13/140.49 (define-fun |tptp.'relcomp$c'| (($x1 |tptp.'A_c_prod_set$'|) ($x2 |tptp.'C_d_prod_set$'|)) |tptp.'A_d_prod_set$'| (as |@_tptp.'A_d_prod_set$'__0| |tptp.'A_d_prod_set$'|)) % 140.13/140.49 (define-fun |tptp.'fun_app$z'| (($x1 |tptp.'D_option_b_option_bool_fun_fun$'|) ($x2 |tptp.'D_option$'|)) |tptp.'B_option_bool_fun$'| (as |@_tptp.'B_option_bool_fun$'__0| |tptp.'B_option_bool_fun$'|)) % 140.13/140.49 (define-fun |tptp.'bot$k'| () |tptp.'B_b_prod_set$'| (as |@_tptp.'B_b_prod_set$'__0| |tptp.'B_b_prod_set$'|)) % 140.13/140.49 (define-fun |tptp.'sup$a'| (($x1 |tptp.'A_d_prod_set$'|) ($x2 |tptp.'A_d_prod_set$'|)) |tptp.'A_d_prod_set$'| (as |@_tptp.'A_d_prod_set$'__0| |tptp.'A_d_prod_set$'|)) % 140.13/140.49 (define-fun |tptp.'ran$h'| (($x1 |tptp.'D_d_option_fun$'|)) |tptp.'D_set$'| (as |@_tptp.'D_set$'__0| |tptp.'D_set$'|)) % 140.13/140.49 (define-fun |tptp.'restrict_map$l'| (($x1 |tptp.'D_d_option_fun$'|) ($x2 |tptp.'D_set$'|)) |tptp.'D_d_option_fun$'| (ite (and (= (as |@_tptp.'D_d_option_fun$'__0| |tptp.'D_d_option_fun$'|) $x1) (= (as |@_tptp.'D_set$'__1| |tptp.'D_set$'|) $x2)) (as |@_tptp.'D_d_option_fun$'__0| |tptp.'D_d_option_fun$'|) (as |@_tptp.'D_d_option_fun$'__1| |tptp.'D_d_option_fun$'|))) % 140.13/140.49 (define-fun |tptp.'fun_app$h'| (($x1 |tptp.'A_c_option_fun$'|) ($x2 |tptp.'A$'|)) |tptp.'C_option$'| (as |@_tptp.'C_option$'__0| |tptp.'C_option$'|)) % 140.13/140.49 (define-fun |tptp.'ran$g'| (($x1 |tptp.'A_c_option_fun$'|)) |tptp.'C_set$'| (as |@_tptp.'C_set$'__0| |tptp.'C_set$'|)) % 140.13/140.49 (define-fun |tptp.'pair$l'| (($x1 |tptp.'D$'|) ($x2 |tptp.'D$'|)) |tptp.'D_d_prod$'| (as |@_tptp.'D_d_prod$'__0| |tptp.'D_d_prod$'|)) % 140.13/140.49 (define-fun |tptp.'member$r'| (($x1 |tptp.'C_option$'|) ($x2 |tptp.'C_option_set$'|)) Bool (or (and (= (as |@_tptp.'C_option$'__0| |tptp.'C_option$'|) $x1) (= (as |@_tptp.'C_option_set$'__2| |tptp.'C_option_set$'|) $x2)) (and (= (as |@_tptp.'C_option$'__1| |tptp.'C_option$'|) $x1) (= (as |@_tptp.'C_option_set$'__3| |tptp.'C_option_set$'|) $x2)) (and (= (as |@_tptp.'C_option$'__1| |tptp.'C_option$'|) $x1) (= (as |@_tptp.'C_option_set$'__0| |tptp.'C_option_set$'|) $x2)))) % 140.13/140.49 (define-fun |tptp.'set_option$a'| (($x1 |tptp.'A_option$'|)) |tptp.'A_set$'| (ite (= (as |@_tptp.'A_option$'__0| |tptp.'A_option$'|) $x1) (as |@_tptp.'A_set$'__0| |tptp.'A_set$'|) (as |@_tptp.'A_set$'__1| |tptp.'A_set$'|))) % 140.13/140.49 (define-fun |tptp.'is_none$a'| () |tptp.'D_option_bool_fun$'| (as |@_tptp.'D_option_bool_fun$'__0| |tptp.'D_option_bool_fun$'|)) % 140.13/140.49 (define-fun |tptp.'fun_app$u'| (($x1 |tptp.'C_option_c_option_bool_fun_fun$'|) ($x2 |tptp.'C_option$'|)) |tptp.'C_option_bool_fun$'| (as |@_tptp.'C_option_bool_fun$'__0| |tptp.'C_option_bool_fun$'|)) % 140.13/140.49 (define-fun |tptp.'insert$d'| (($x1 |tptp.'D$'|) ($x2 |tptp.'D_set$'|)) |tptp.'D_set$'| (as |@_tptp.'D_set$'__1| |tptp.'D_set$'|)) % 140.13/140.49 (define-fun |tptp.'map_add$a'| (($x1 |tptp.'C_b_option_fun$'|) ($x2 |tptp.'C_b_option_fun$'|)) |tptp.'C_b_option_fun$'| (as |@_tptp.'C_b_option_fun$'__0| |tptp.'C_b_option_fun$'|)) % 140.13/140.49 (define-fun |tptp.'insert$a'| (($x1 |tptp.'B_option$'|) ($x2 |tptp.'B_option_set$'|)) |tptp.'B_option_set$'| (ite (and (= (as |@_tptp.'B_option$'__0| |tptp.'B_option$'|) $x1) (= (as |@_tptp.'B_option_set$'__1| |tptp.'B_option_set$'|) $x2)) (as |@_tptp.'B_option_set$'__1| |tptp.'B_option_set$'|) (ite (and (= (as |@_tptp.'B_option$'__0| |tptp.'B_option$'|) $x1) (= (as |@_tptp.'B_option_set$'__0| |tptp.'B_option_set$'|) $x2)) (as |@_tptp.'B_option_set$'__1| |tptp.'B_option_set$'|) (ite (and (= (as |@_tptp.'B_option$'__1| |tptp.'B_option$'|) $x1) (= (as |@_tptp.'B_option_set$'__3| |tptp.'B_option_set$'|) $x2)) (as |@_tptp.'B_option_set$'__2| |tptp.'B_option_set$'|) (ite (and (= (as |@_tptp.'B_option$'__0| |tptp.'B_option$'|) $x1) (= (as |@_tptp.'B_option_set$'__2| |tptp.'B_option_set$'|) $x2)) (as |@_tptp.'B_option_set$'__2| |tptp.'B_option_set$'|) (ite (and (= (as |@_tptp.'B_option$'__1| |tptp.'B_option$'|) $x1) (= (as |@_tptp.'B_option_set$'__1| |tptp.'B_option_set$'|) $x2)) (as |@_tptp.'B_option_set$'__2| |tptp.'B_option_set$'|) (ite (and (= (as |@_tptp.'B_option$'__0| |tptp.'B_option$'|) $x1) (= (as |@_tptp.'B_option_set$'__3| |tptp.'B_option_set$'|) $x2)) (as |@_tptp.'B_option_set$'__2| |tptp.'B_option_set$'|) (ite (and (= (as |@_tptp.'B_option$'__1| |tptp.'B_option$'|) $x1) (= (as |@_tptp.'B_option_set$'__0| |tptp.'B_option_set$'|) $x2)) (as |@_tptp.'B_option_set$'__2| |tptp.'B_option_set$'|) (as |@_tptp.'B_option_set$'__3| |tptp.'B_option_set$'|))))))))) % 140.13/140.49 (define-fun |tptp.'the$a'| (($x1 |tptp.'D_option$'|)) |tptp.'D$'| (as |@_tptp.'D$'__0| |tptp.'D$'|)) % 140.13/140.49 (define-fun |tptp.'image$e'| (($x1 |tptp.'C_b_prod_set$'|) ($x2 |tptp.'C_set$'|)) |tptp.'B_set$'| (as |@_tptp.'B_set$'__0| |tptp.'B_set$'|)) % 140.13/140.49 (define-fun |tptp.'fun_app$n'| (($x1 |tptp.'A_b_option_fun$'|) ($x2 |tptp.'A$'|)) |tptp.'B_option$'| (as |@_tptp.'B_option$'__0| |tptp.'B_option$'|)) % 140.13/140.49 (define-fun |tptp.'fun_app$w'| (($x1 |tptp.'C_option_b_option_bool_fun_fun$'|) ($x2 |tptp.'C_option$'|)) |tptp.'B_option_bool_fun$'| (as |@_tptp.'B_option_bool_fun$'__0| |tptp.'B_option_bool_fun$'|)) % 140.13/140.49 (define-fun |tptp.'graph$l'| (($x1 |tptp.'B_b_option_fun$'|)) |tptp.'B_b_prod_set$'| (ite (= (as |@_tptp.'B_b_option_fun$'__1| |tptp.'B_b_option_fun$'|) $x1) (as |@_tptp.'B_b_prod_set$'__0| |tptp.'B_b_prod_set$'|) (as |@_tptp.'B_b_prod_set$'__1| |tptp.'B_b_prod_set$'|))) % 140.13/140.49 (define-fun |tptp.'b$'| () |tptp.'C_d_option_fun$'| (as |@_tptp.'C_d_option_fun$'__0| |tptp.'C_d_option_fun$'|)) % 140.13/140.49 (define-fun |tptp.'relcomp$f'| (($x1 |tptp.'C_d_prod_set$'|) ($x2 |tptp.'D_d_prod_set$'|)) |tptp.'C_d_prod_set$'| (as |@_tptp.'C_d_prod_set$'__0| |tptp.'C_d_prod_set$'|)) % 140.13/140.49 (define-fun |tptp.'restrict_map$o'| (($x1 |tptp.'B_a_option_fun$'|) ($x2 |tptp.'B_set$'|)) |tptp.'B_a_option_fun$'| (as |@_tptp.'B_a_option_fun$'__0| |tptp.'B_a_option_fun$'|)) % 140.13/140.49 (define-fun |tptp.'fun_app$ay'| (($x1 |tptp.'B_a_option_fun$'|) ($x2 |tptp.'B$'|)) |tptp.'A_option$'| (as |@_tptp.'A_option$'__0| |tptp.'A_option$'|)) % 140.13/140.49 (define-fun |tptp.'the$c'| (($x1 |tptp.'B_option_option$'|)) |tptp.'B_option$'| (ite (= (as |@_tptp.'B_option_option$'__1| |tptp.'B_option_option$'|) $x1) (as |@_tptp.'B_option$'__0| |tptp.'B_option$'|) (as |@_tptp.'B_option$'__1| |tptp.'B_option$'|))) % 140.13/140.49 (define-fun |tptp.'map_comp$k'| (($x1 |tptp.'B_d_option_fun$'|) ($x2 |tptp.'C_b_option_fun$'|)) |tptp.'C_d_option_fun$'| (as |@_tptp.'C_d_option_fun$'__0| |tptp.'C_d_option_fun$'|)) % 140.13/140.49 (define-fun |tptp.'ran$i'| (($x1 |tptp.'B_d_option_fun$'|)) |tptp.'D_set$'| (as |@_tptp.'D_set$'__0| |tptp.'D_set$'|)) % 140.13/140.49 (define-fun |tptp.'restrict_map$m'| (($x1 |tptp.'D_b_option_fun$'|) ($x2 |tptp.'D_set$'|)) |tptp.'D_b_option_fun$'| (as |@_tptp.'D_b_option_fun$'__0| |tptp.'D_b_option_fun$'|)) % 140.13/140.49 (define-fun |tptp.'map_comp$f'| (($x1 |tptp.'A_b_option_fun$'|)) |tptp.'A_a_option_fun_a_b_option_fun_fun$'| (ite (= (as |@_tptp.'A_b_option_fun$'__0| |tptp.'A_b_option_fun$'|) $x1) (as |@_tptp.'A_a_option_fun_a_b_option_fun_fun$'__0| |tptp.'A_a_option_fun_a_b_option_fun_fun$'|) (as |@_tptp.'A_a_option_fun_a_b_option_fun_fun$'__1| |tptp.'A_a_option_fun_a_b_option_fun_fun$'|))) % 140.13/140.49 (define-fun |tptp.'a$'| () |tptp.'D_b_option_fun$'| (as |@_tptp.'D_b_option_fun$'__0| |tptp.'D_b_option_fun$'|)) % 140.13/140.49 (define-fun |tptp.'bind$b'| (($x1 |tptp.'C_option$'|) ($x2 |tptp.'C_b_option_fun$'|)) |tptp.'B_option$'| (as |@_tptp.'B_option$'__0| |tptp.'B_option$'|)) % 140.13/140.49 (define-fun |tptp.'combine_options$a'| (($x1 |tptp.'D_d_d_fun_fun$'|) ($x2 |tptp.'D_option$'|)) |tptp.'D_option_d_option_fun$'| (ite (and (= (as |@_tptp.'D_d_d_fun_fun$'__0| |tptp.'D_d_d_fun_fun$'|) $x1) (= (as |@_tptp.'D_option$'__0| |tptp.'D_option$'|) $x2)) (as |@_tptp.'D_option_d_option_fun$'__0| |tptp.'D_option_d_option_fun$'|) (as |@_tptp.'D_option_d_option_fun$'__1| |tptp.'D_option_d_option_fun$'|))) % 140.13/140.49 (define-fun |tptp.'map_add$'| (($x1 |tptp.'C_d_option_fun$'|) ($x2 |tptp.'C_d_option_fun$'|)) |tptp.'C_d_option_fun$'| (as |@_tptp.'C_d_option_fun$'__0| |tptp.'C_d_option_fun$'|)) % 140.13/140.49 (define-fun |tptp.'member$q'| (($x1 |tptp.'D_d_prod$'|) ($x2 |tptp.'D_d_prod_set$'|)) Bool true) % 140.13/140.49 (define-fun |tptp.'fun_app$ao'| (($x1 |tptp.'D_d_d_fun_fun$'|) ($x2 |tptp.'D$'|)) |tptp.'D_d_fun$'| (as |@_tptp.'D_d_fun$'__0| |tptp.'D_d_fun$'|)) % 140.13/140.49 (define-fun |tptp.'uua$'| (($x1 |tptp.'D_set$'|)) |tptp.'D_bool_fun$'| (ite (= (as |@_tptp.'D_set$'__1| |tptp.'D_set$'|) $x1) (as |@_tptp.'D_bool_fun$'__0| |tptp.'D_bool_fun$'|) (as |@_tptp.'D_bool_fun$'__1| |tptp.'D_bool_fun$'|))) % 140.13/140.49 (define-fun |tptp.'graph$g'| (($x1 |tptp.'C_a_option_fun$'|)) |tptp.'C_a_prod_set$'| (as |@_tptp.'C_a_prod_set$'__0| |tptp.'C_a_prod_set$'|)) % 140.13/140.49 (define-fun |tptp.'inf$a'| (($x1 |tptp.'A_set$'|) ($x2 |tptp.'A_set$'|)) |tptp.'A_set$'| (ite (and (= (as |@_tptp.'A_set$'__0| |tptp.'A_set$'|) $x1) (= (as |@_tptp.'A_set$'__0| |tptp.'A_set$'|) $x2)) (as |@_tptp.'A_set$'__1| |tptp.'A_set$'|) (as |@_tptp.'A_set$'__0| |tptp.'A_set$'|))) % 140.13/140.49 (define-fun |tptp.'sup$c'| (($x1 |tptp.'A_b_prod_set$'|) ($x2 |tptp.'A_b_prod_set$'|)) |tptp.'A_b_prod_set$'| (as |@_tptp.'A_b_prod_set$'__0| |tptp.'A_b_prod_set$'|)) % 140.13/140.49 (define-fun |tptp.'less_eq$d'| (($x1 |tptp.'A_b_prod_set$'|) ($x2 |tptp.'A_b_prod_set$'|)) Bool true) % 140.13/140.49 (define-fun |tptp.'map_comp$i'| (($x1 |tptp.'C_d_option_fun$'|) ($x2 |tptp.'C_c_option_fun$'|)) |tptp.'C_d_option_fun$'| (as |@_tptp.'C_d_option_fun$'__0| |tptp.'C_d_option_fun$'|)) % 140.13/140.49 (define-fun |tptp.'restrict_map$g'| (($x1 |tptp.'A_d_option_fun$'|) ($x2 |tptp.'A_set$'|)) |tptp.'A_d_option_fun$'| (as |@_tptp.'A_d_option_fun$'__0| |tptp.'A_d_option_fun$'|)) % 140.13/140.49 (define-fun |tptp.'these$'| (($x1 |tptp.'C_option_set$'|)) |tptp.'C_set$'| (ite (= (as |@_tptp.'C_option_set$'__1| |tptp.'C_option_set$'|) $x1) (as |@_tptp.'C_set$'__0| |tptp.'C_set$'|) (ite (= (as |@_tptp.'C_option_set$'__2| |tptp.'C_option_set$'|) $x1) (as |@_tptp.'C_set$'__0| |tptp.'C_set$'|) (as |@_tptp.'C_set$'__1| |tptp.'C_set$'|)))) % 140.13/140.49 (define-fun |tptp.'restrict_map$k'| (($x1 |tptp.'C_c_option_fun$'|) ($x2 |tptp.'C_set$'|)) |tptp.'C_c_option_fun$'| (ite (and (= (as |@_tptp.'C_c_option_fun$'__0| |tptp.'C_c_option_fun$'|) $x1) (= (as |@_tptp.'C_set$'__1| |tptp.'C_set$'|) $x2)) (as |@_tptp.'C_c_option_fun$'__0| |tptp.'C_c_option_fun$'|) (as |@_tptp.'C_c_option_fun$'__1| |tptp.'C_c_option_fun$'|))) % 140.13/140.49 (define-fun |tptp.'ran$a'| (($x1 |tptp.'C_a_option_fun$'|)) |tptp.'A_set$'| (as |@_tptp.'A_set$'__0| |tptp.'A_set$'|)) % 140.13/140.49 (define-fun |tptp.'set_option$b'| (($x1 |tptp.'C_option$'|)) |tptp.'C_set$'| (ite (= (as |@_tptp.'C_option$'__0| |tptp.'C_option$'|) $x1) (as |@_tptp.'C_set$'__0| |tptp.'C_set$'|) (as |@_tptp.'C_set$'__1| |tptp.'C_set$'|))) % 140.13/140.49 (define-fun |tptp.'pair$b'| (($x1 |tptp.'B$'|) ($x2 |tptp.'C$'|)) |tptp.'B_c_prod$'| (as |@_tptp.'B_c_prod$'__0| |tptp.'B_c_prod$'|)) % 140.13/140.49 (define-fun |tptp.'fun_app$au'| (($x1 |tptp.'A_d_prod_bool_fun$'|) ($x2 |tptp.'A_d_prod$'|)) Bool false) % 140.13/140.49 (define-fun |tptp.'some$'| () |tptp.'A_a_option_fun$'| (as |@_tptp.'A_a_option_fun$'__0| |tptp.'A_a_option_fun$'|)) % 140.13/140.49 (define-fun |tptp.'the_elem$a'| (($x1 |tptp.'D_set$'|)) |tptp.'D$'| (as |@_tptp.'D$'__0| |tptp.'D$'|)) % 140.13/140.49 (define-fun |tptp.'the$b'| (($x1 |tptp.'B_option$'|)) |tptp.'B$'| (as |@_tptp.'B$'__0| |tptp.'B$'|)) % 140.13/140.49 (define-fun |tptp.'fun_app$aj'| (($x1 |tptp.'C_option_c_option_fun$'|) ($x2 |tptp.'C_option$'|)) |tptp.'C_option$'| (ite (and (= (as |@_tptp.'C_option_c_option_fun$'__0| |tptp.'C_option_c_option_fun$'|) $x1) (= (as |@_tptp.'C_option$'__0| |tptp.'C_option$'|) $x2)) (as |@_tptp.'C_option$'__0| |tptp.'C_option$'|) (as |@_tptp.'C_option$'__1| |tptp.'C_option$'|))) % 140.13/140.49 (define-fun |tptp.'relcomp$k'| (($x1 |tptp.'A_b_prod_set$'|) ($x2 |tptp.'B_b_prod_set$'|)) |tptp.'A_b_prod_set$'| (as |@_tptp.'A_b_prod_set$'__0| |tptp.'A_b_prod_set$'|)) % 140.13/140.49 (define-fun |tptp.'relcomp$e'| (($x1 |tptp.'C_a_prod_set$'|) ($x2 |tptp.'A_d_prod_set$'|)) |tptp.'C_d_prod_set$'| (as |@_tptp.'C_d_prod_set$'__0| |tptp.'C_d_prod_set$'|)) % 140.13/140.49 (define-fun |tptp.'collect$a'| (($x1 |tptp.'D_bool_fun$'|)) |tptp.'D_set$'| (ite (= (as |@_tptp.'D_bool_fun$'__1| |tptp.'D_bool_fun$'|) $x1) (as |@_tptp.'D_set$'__0| |tptp.'D_set$'|) (as |@_tptp.'D_set$'__1| |tptp.'D_set$'|))) % 140.13/140.49 (define-fun |tptp.'uud$'| (($x1 |tptp.'A_set$'|)) |tptp.'A_bool_fun$'| (ite (= (as |@_tptp.'A_set$'__0| |tptp.'A_set$'|) $x1) (as |@_tptp.'A_bool_fun$'__0| |tptp.'A_bool_fun$'|) (as |@_tptp.'A_bool_fun$'__1| |tptp.'A_bool_fun$'|))) % 140.13/140.49 (define-fun |tptp.'relcomp$b'| (($x1 |tptp.'A_d_prod_set$'|) ($x2 |tptp.'D_b_prod_set$'|)) |tptp.'A_b_prod_set$'| (as |@_tptp.'A_b_prod_set$'__0| |tptp.'A_b_prod_set$'|)) % 140.13/140.49 (define-fun |tptp.'dom$'| (($x1 |tptp.'C_d_option_fun$'|)) |tptp.'C_set$'| (as |@_tptp.'C_set$'__0| |tptp.'C_set$'|)) % 140.13/140.49 (define-fun |tptp.'none$c'| () |tptp.'B_option$'| (as |@_tptp.'B_option$'__0| |tptp.'B_option$'|)) % 140.13/140.49 (define-fun |tptp.'restrict_map$n'| (($x1 |tptp.'D_a_option_fun$'|) ($x2 |tptp.'D_set$'|)) |tptp.'D_a_option_fun$'| (as |@_tptp.'D_a_option_fun$'__0| |tptp.'D_a_option_fun$'|)) % 140.13/140.49 (define-fun |tptp.'ran$c'| (($x1 |tptp.'A_a_option_fun$'|)) |tptp.'A_set$'| (as |@_tptp.'A_set$'__0| |tptp.'A_set$'|)) % 140.13/140.49 (define-fun |tptp.'graph$e'| (($x1 |tptp.'A_d_option_fun$'|)) |tptp.'A_d_prod_set$'| (as |@_tptp.'A_d_prod_set$'__0| |tptp.'A_d_prod_set$'|)) % 140.13/140.49 (define-fun |tptp.'insert$'| (($x1 |tptp.'C_option$'|) ($x2 |tptp.'C_option_set$'|)) |tptp.'C_option_set$'| (ite (and (= (as |@_tptp.'C_option$'__0| |tptp.'C_option$'|) $x1) (= (as |@_tptp.'C_option_set$'__0| |tptp.'C_option_set$'|) $x2)) (as |@_tptp.'C_option_set$'__0| |tptp.'C_option_set$'|) (ite (and (= (as |@_tptp.'C_option$'__1| |tptp.'C_option$'|) $x1) (= (as |@_tptp.'C_option_set$'__0| |tptp.'C_option_set$'|) $x2)) (as |@_tptp.'C_option_set$'__0| |tptp.'C_option_set$'|) (ite (and (= (as |@_tptp.'C_option$'__1| |tptp.'C_option$'|) $x1) (= (as |@_tptp.'C_option_set$'__2| |tptp.'C_option_set$'|) $x2)) (as |@_tptp.'C_option_set$'__0| |tptp.'C_option_set$'|) (ite (and (= (as |@_tptp.'C_option$'__0| |tptp.'C_option$'|) $x1) (= (as |@_tptp.'C_option_set$'__3| |tptp.'C_option_set$'|) $x2)) (as |@_tptp.'C_option_set$'__0| |tptp.'C_option_set$'|) (ite (and (= (as |@_tptp.'C_option$'__0| |tptp.'C_option$'|) $x1) (= (as |@_tptp.'C_option_set$'__2| |tptp.'C_option_set$'|) $x2)) (as |@_tptp.'C_option_set$'__2| |tptp.'C_option_set$'|) (ite (and (= (as |@_tptp.'C_option$'__0| |tptp.'C_option$'|) $x1) (= (as |@_tptp.'C_option_set$'__1| |tptp.'C_option_set$'|) $x2)) (as |@_tptp.'C_option_set$'__2| |tptp.'C_option_set$'|) (as |@_tptp.'C_option_set$'__3| |tptp.'C_option_set$'|)))))))) % 140.13/140.49 (define-fun |tptp.'pair$j'| (($x1 |tptp.'D$'|) ($x2 |tptp.'B$'|)) |tptp.'D_b_prod$'| (as |@_tptp.'D_b_prod$'__0| |tptp.'D_b_prod$'|)) % 140.13/140.49 (define-fun |tptp.'collect$d'| (($x1 |tptp.'A_bool_fun$'|)) |tptp.'A_set$'| (ite (= (as |@_tptp.'A_bool_fun$'__0| |tptp.'A_bool_fun$'|) $x1) (as |@_tptp.'A_set$'__0| |tptp.'A_set$'|) (as |@_tptp.'A_set$'__1| |tptp.'A_set$'|))) % 140.13/140.49 (define-fun |tptp.'insert$g'| (($x1 |tptp.'A_c_prod$'|) ($x2 |tptp.'A_c_prod_set$'|)) |tptp.'A_c_prod_set$'| (as |@_tptp.'A_c_prod_set$'__0| |tptp.'A_c_prod_set$'|)) % 140.13/140.49 (define-fun |tptp.'fun_app$b'| (($x1 |tptp.'C_bool_fun$'|) ($x2 |tptp.'C$'|)) Bool (and (= (as |@_tptp.'C_bool_fun$'__0| |tptp.'C_bool_fun$'|) $x1) (= (as |@_tptp.'C$'__0| |tptp.'C$'|) $x2))) % 140.13/140.49 (define-fun |tptp.'relcomp$q'| (($x1 |tptp.'A_c_prod_set$'|) ($x2 |tptp.'C_c_prod_set$'|)) |tptp.'A_c_prod_set$'| (as |@_tptp.'A_c_prod_set$'__0| |tptp.'A_c_prod_set$'|)) % 140.13/140.49 (define-fun |tptp.'less_eq$'| (($x1 |tptp.'A_c_prod_set$'|) ($x2 |tptp.'A_c_prod_set$'|)) Bool false) % 140.13/140.49 (define-fun |tptp.'inj_on$b'| (($x1 |tptp.'B_b_option_fun$'|) ($x2 |tptp.'B_set$'|)) Bool true) % 140.13/140.49 (define-fun |tptp.'fun_upd$a'| (($x1 |tptp.'C_d_option_fun$'|) ($x2 |tptp.'C$'|) ($x3 |tptp.'D_option$'|)) |tptp.'C_d_option_fun$'| (as |@_tptp.'C_d_option_fun$'__0| |tptp.'C_d_option_fun$'|)) % 140.13/140.49 (define-fun |tptp.'pair$'| (($x1 |tptp.'C$'|) ($x2 |tptp.'A$'|)) |tptp.'C_a_prod$'| (as |@_tptp.'C_a_prod$'__0| |tptp.'C_a_prod$'|)) % 140.13/140.49 (define-fun |tptp.'relcomp$g'| (($x1 |tptp.'C_b_prod_set$'|) ($x2 |tptp.'B_d_prod_set$'|)) |tptp.'C_d_prod_set$'| (as |@_tptp.'C_d_prod_set$'__0| |tptp.'C_d_prod_set$'|)) % 140.13/140.49 (define-fun |tptp.'relcomp$'| (($x1 |tptp.'A_c_prod_set$'|) ($x2 |tptp.'C_b_prod_set$'|)) |tptp.'A_b_prod_set$'| (as |@_tptp.'A_b_prod_set$'__0| |tptp.'A_b_prod_set$'|)) % 140.13/140.49 (define-fun |tptp.'set_option$d'| (($x1 |tptp.'B_option$'|)) |tptp.'B_set$'| (ite (= (as |@_tptp.'B_option$'__0| |tptp.'B_option$'|) $x1) (as |@_tptp.'B_set$'__0| |tptp.'B_set$'|) (as |@_tptp.'B_set$'__1| |tptp.'B_set$'|))) % 140.13/140.49 (define-fun |tptp.'image$h'| (($x1 |tptp.'B_b_option_fun$'|) ($x2 |tptp.'B_set$'|)) |tptp.'B_option_set$'| (ite (and (= (as |@_tptp.'B_b_option_fun$'__0| |tptp.'B_b_option_fun$'|) $x1) (= (as |@_tptp.'B_set$'__0| |tptp.'B_set$'|) $x2)) (as |@_tptp.'B_option_set$'__0| |tptp.'B_option_set$'|) (ite (and (= (as |@_tptp.'B_b_option_fun$'__0| |tptp.'B_b_option_fun$'|) $x1) (= (as |@_tptp.'B_set$'__1| |tptp.'B_set$'|) $x2)) (as |@_tptp.'B_option_set$'__2| |tptp.'B_option_set$'|) (as |@_tptp.'B_option_set$'__1| |tptp.'B_option_set$'|)))) % 140.13/140.49 (define-fun |tptp.'pair$d'| (($x1 |tptp.'B$'|) ($x2 |tptp.'B$'|)) |tptp.'B_b_prod$'| (as |@_tptp.'B_b_prod$'__0| |tptp.'B_b_prod$'|)) % 140.13/140.49 (define-fun |tptp.'is_none$b'| () |tptp.'C_option_bool_fun$'| (as |@_tptp.'C_option_bool_fun$'__0| |tptp.'C_option_bool_fun$'|)) % 140.13/140.49 (define-fun |tptp.'member$'| ((BOUND_VARIABLE_9488 |tptp.'B_option$'|) (BOUND_VARIABLE_9489 |tptp.'B_option_set$'|)) Bool (or (and (= (as |@_tptp.'B_option_bool_fun$'__1| |tptp.'B_option_bool_fun$'|) (ite (= BOUND_VARIABLE_9489 (as |@_tptp.'B_option_set$'__0| |tptp.'B_option_set$'|)) (as |@_tptp.'B_option_bool_fun$'__0| |tptp.'B_option_bool_fun$'|) (ite (= BOUND_VARIABLE_9489 (as |@_tptp.'B_option_set$'__1| |tptp.'B_option_set$'|)) (as |@_tptp.'B_option_bool_fun$'__1| |tptp.'B_option_bool_fun$'|) (ite (= BOUND_VARIABLE_9489 (as |@_tptp.'B_option_set$'__3| |tptp.'B_option_set$'|)) (as |@_tptp.'B_option_bool_fun$'__2| |tptp.'B_option_bool_fun$'|) (as |@_tptp.'B_option_bool_fun$'__3| |tptp.'B_option_bool_fun$'|))))) (= BOUND_VARIABLE_9488 (as |@_tptp.'B_option$'__0| |tptp.'B_option$'|))) (and (= (as |@_tptp.'B_option_bool_fun$'__3| |tptp.'B_option_bool_fun$'|) (ite (= BOUND_VARIABLE_9489 (as |@_tptp.'B_option_set$'__0| |tptp.'B_option_set$'|)) (as |@_tptp.'B_option_bool_fun$'__0| |tptp.'B_option_bool_fun$'|) (ite (= BOUND_VARIABLE_9489 (as |@_tptp.'B_option_set$'__1| |tptp.'B_option_set$'|)) (as |@_tptp.'B_option_bool_fun$'__1| |tptp.'B_option_bool_fun$'|) (ite (= BOUND_VARIABLE_9489 (as |@_tptp.'B_option_set$'__3| |tptp.'B_option_set$'|)) (as |@_tptp.'B_option_bool_fun$'__2| |tptp.'B_option_bool_fun$'|) (as |@_tptp.'B_option_bool_fun$'__3| |tptp.'B_option_bool_fun$'|))))) (= BOUND_VARIABLE_9488 (as |@_tptp.'B_option$'__1| |tptp.'B_option$'|))) (and (= (as |@_tptp.'B_option_bool_fun$'__2| |tptp.'B_option_bool_fun$'|) (ite (= BOUND_VARIABLE_9489 (as |@_tptp.'B_option_set$'__0| |tptp.'B_option_set$'|)) (as |@_tptp.'B_option_bool_fun$'__0| |tptp.'B_option_bool_fun$'|) (ite (= BOUND_VARIABLE_9489 (as |@_tptp.'B_option_set$'__1| |tptp.'B_option_set$'|)) (as |@_tptp.'B_option_bool_fun$'__1| |tptp.'B_option_bool_fun$'|) (ite (= BOUND_VARIABLE_9489 (as |@_tptp.'B_option_set$'__3| |tptp.'B_option_set$'|)) (as |@_tptp.'B_option_bool_fun$'__2| |tptp.'B_option_bool_fun$'|) (as |@_tptp.'B_option_bool_fun$'__3| |tptp.'B_option_bool_fun$'|))))) (= BOUND_VARIABLE_9488 (as |@_tptp.'B_option$'__0| |tptp.'B_option$'|))) (and (= (as |@_tptp.'B_option_bool_fun$'__2| |tptp.'B_option_bool_fun$'|) (ite (= BOUND_VARIABLE_9489 (as |@_tptp.'B_option_set$'__0| |tptp.'B_option_set$'|)) (as |@_tptp.'B_option_bool_fun$'__0| |tptp.'B_option_bool_fun$'|) (ite (= BOUND_VARIABLE_9489 (as |@_tptp.'B_option_set$'__1| |tptp.'B_option_set$'|)) (as |@_tptp.'B_option_bool_fun$'__1| |tptp.'B_option_bool_fun$'|) (ite (= BOUND_VARIABLE_9489 (as |@_tptp.'B_option_set$'__3| |tptp.'B_option_set$'|)) (as |@_tptp.'B_option_bool_fun$'__2| |tptp.'B_option_bool_fun$'|) (as |@_tptp.'B_option_bool_fun$'__3| |tptp.'B_option_bool_fun$'|))))) (= BOUND_VARIABLE_9488 (as |@_tptp.'B_option$'__1| |tptp.'B_option$'|))))) % 140.13/140.49 (define-fun |tptp.'fun_app$s'| (($x1 |tptp.'C_option_bool_fun$'|) ($x2 |tptp.'C_option$'|)) Bool (and (= (as |@_tptp.'C_option_bool_fun$'__0| |tptp.'C_option_bool_fun$'|) $x1) (= (as |@_tptp.'C_option$'__0| |tptp.'C_option$'|) $x2))) % 140.13/140.49 (define-fun |tptp.'uu$'| (($x1 |tptp.'B_option_set$'|)) |tptp.'B_option_bool_fun$'| (ite (= (as |@_tptp.'B_option_set$'__0| |tptp.'B_option_set$'|) $x1) (as |@_tptp.'B_option_bool_fun$'__0| |tptp.'B_option_bool_fun$'|) (ite (= (as |@_tptp.'B_option_set$'__1| |tptp.'B_option_set$'|) $x1) (as |@_tptp.'B_option_bool_fun$'__1| |tptp.'B_option_bool_fun$'|) (ite (= (as |@_tptp.'B_option_set$'__3| |tptp.'B_option_set$'|) $x1) (as |@_tptp.'B_option_bool_fun$'__2| |tptp.'B_option_bool_fun$'|) (as |@_tptp.'B_option_bool_fun$'__3| |tptp.'B_option_bool_fun$'|))))) % 140.13/140.49 (define-fun |tptp.'bot$a'| () |tptp.'C_set$'| (as |@_tptp.'C_set$'__0| |tptp.'C_set$'|)) % 140.13/140.49 (define-fun |tptp.'bind$f'| (($x1 |tptp.'B_option$'|) ($x2 |tptp.'B_c_option_fun$'|)) |tptp.'C_option$'| (as |@_tptp.'C_option$'__0| |tptp.'C_option$'|)) % 140.13/140.49 (define-fun |tptp.'some$d'| (($x1 |tptp.'B_option$'|)) |tptp.'B_option_option$'| (ite (= (as |@_tptp.'B_option$'__0| |tptp.'B_option$'|) $x1) (as |@_tptp.'B_option_option$'__1| |tptp.'B_option_option$'|) (as |@_tptp.'B_option_option$'__2| |tptp.'B_option_option$'|))) % 140.13/140.49 (define-fun |tptp.'graph$k'| (($x1 |tptp.'B_c_option_fun$'|)) |tptp.'B_c_prod_set$'| (as |@_tptp.'B_c_prod_set$'__0| |tptp.'B_c_prod_set$'|)) % 140.13/140.49 (define-fun |tptp.'combine_options$'| (($x1 |tptp.'C_c_c_fun_fun$'|) ($x2 |tptp.'C_option$'|)) |tptp.'C_option_c_option_fun$'| (ite (and (= (as |@_tptp.'C_c_c_fun_fun$'__0| |tptp.'C_c_c_fun_fun$'|) $x1) (= (as |@_tptp.'C_option$'__0| |tptp.'C_option$'|) $x2)) (as |@_tptp.'C_option_c_option_fun$'__0| |tptp.'C_option_c_option_fun$'|) (as |@_tptp.'C_option_c_option_fun$'__1| |tptp.'C_option_c_option_fun$'|))) % 140.13/140.49 (define-fun |tptp.'image$a'| (($x1 |tptp.'C_d_prod_set$'|) ($x2 |tptp.'C_set$'|)) |tptp.'D_set$'| (as |@_tptp.'D_set$'__0| |tptp.'D_set$'|)) % 140.13/140.49 (define-fun |tptp.'fun_app$aa'| (($x1 |tptp.'B_option_c_option_bool_fun_fun$'|) ($x2 |tptp.'B_option$'|)) |tptp.'C_option_bool_fun$'| (as |@_tptp.'C_option_bool_fun$'__0| |tptp.'C_option_bool_fun$'|)) % 140.13/140.49 (define-fun |tptp.'fun_app$an'| (($x1 |tptp.'D_d_fun$'|) ($x2 |tptp.'D$'|)) |tptp.'D$'| (as |@_tptp.'D$'__0| |tptp.'D$'|)) % 140.13/140.49 (define-fun |tptp.'bot$b'| () |tptp.'B_set$'| (as |@_tptp.'B_set$'__0| |tptp.'B_set$'|)) % 140.13/140.49 (define-fun |tptp.'insert$j'| (($x1 |tptp.'C_b_prod$'|) ($x2 |tptp.'C_b_prod_set$'|)) |tptp.'C_b_prod_set$'| (as |@_tptp.'C_b_prod_set$'__0| |tptp.'C_b_prod_set$'|)) % 140.13/140.49 (define-fun |tptp.'collect$b'| (($x1 |tptp.'C_bool_fun$'|)) |tptp.'C_set$'| (ite (= (as |@_tptp.'C_bool_fun$'__1| |tptp.'C_bool_fun$'|) $x1) (as |@_tptp.'C_set$'__0| |tptp.'C_set$'|) (as |@_tptp.'C_set$'__1| |tptp.'C_set$'|))) % 140.13/140.49 (define-fun |tptp.'restrict_map$b'| (($x1 |tptp.'B_c_option_fun$'|) ($x2 |tptp.'B_set$'|)) |tptp.'B_c_option_fun$'| (as |@_tptp.'B_c_option_fun$'__0| |tptp.'B_c_option_fun$'|)) % 140.13/140.49 (define-fun |tptp.'graph$j'| (($x1 |tptp.'A_a_option_fun$'|)) |tptp.'A_a_prod_set$'| (ite (= (as |@_tptp.'A_a_option_fun$'__1| |tptp.'A_a_option_fun$'|) $x1) (as |@_tptp.'A_a_prod_set$'__0| |tptp.'A_a_prod_set$'|) (as |@_tptp.'A_a_prod_set$'__1| |tptp.'A_a_prod_set$'|))) % 140.13/140.49 (define-fun |tptp.'bot$s'| () |tptp.'A_bool_fun$'| (as |@_tptp.'A_bool_fun$'__0| |tptp.'A_bool_fun$'|)) % 140.13/140.49 (define-fun |tptp.'pair$c'| (($x1 |tptp.'B$'|) ($x2 |tptp.'D$'|)) |tptp.'B_d_prod$'| (as |@_tptp.'B_d_prod$'__0| |tptp.'B_d_prod$'|)) % 140.13/140.49 (define-fun |tptp.'uuc$'| (($x1 |tptp.'B_set$'|)) |tptp.'B_bool_fun$'| (ite (= (as |@_tptp.'B_set$'__1| |tptp.'B_set$'|) $x1) (as |@_tptp.'B_bool_fun$'__0| |tptp.'B_bool_fun$'|) (as |@_tptp.'B_bool_fun$'__1| |tptp.'B_bool_fun$'|))) % 140.13/140.49 (define-fun |tptp.'fun_upd$c'| (($x1 |tptp.'C_b_option_fun$'|) ($x2 |tptp.'C$'|) ($x3 |tptp.'B_option$'|)) |tptp.'C_b_option_fun$'| (as |@_tptp.'C_b_option_fun$'__0| |tptp.'C_b_option_fun$'|)) % 140.13/140.49 (define-fun |tptp.'fun_app$al'| (($x1 |tptp.'C_c_c_fun_fun$'|) ($x2 |tptp.'C$'|)) |tptp.'C_c_fun$'| (as |@_tptp.'C_c_fun$'__0| |tptp.'C_c_fun$'|)) % 140.13/140.49 (define-fun |tptp.'fun_app$at'| (($x1 |tptp.'C_b_prod_bool_fun$'|) ($x2 |tptp.'C_b_prod$'|)) Bool false) % 140.13/140.49 (define-fun |tptp.'fun_app$'| (($x1 |tptp.'B_option_bool_fun$'|) ($x2 |tptp.'B_option$'|)) Bool (or (and (= (as |@_tptp.'B_option_bool_fun$'__1| |tptp.'B_option_bool_fun$'|) $x1) (= (as |@_tptp.'B_option$'__0| |tptp.'B_option$'|) $x2)) (and (= (as |@_tptp.'B_option_bool_fun$'__3| |tptp.'B_option_bool_fun$'|) $x1) (= (as |@_tptp.'B_option$'__1| |tptp.'B_option$'|) $x2)) (and (= (as |@_tptp.'B_option_bool_fun$'__2| |tptp.'B_option_bool_fun$'|) $x1) (= (as |@_tptp.'B_option$'__0| |tptp.'B_option$'|) $x2)) (and (= (as |@_tptp.'B_option_bool_fun$'__2| |tptp.'B_option_bool_fun$'|) $x1) (= (as |@_tptp.'B_option$'__1| |tptp.'B_option$'|) $x2)))) % 140.13/140.49 (define-fun |tptp.'bot$n'| () |tptp.'C_option_set$'| (as |@_tptp.'C_option_set$'__1| |tptp.'C_option_set$'|)) % 140.13/140.49 (define-fun |tptp.'finite$c'| (($x1 |tptp.'A_d_prod_set$'|)) Bool true) % 140.13/140.49 (define-fun |tptp.'ran$d'| (($x1 |tptp.'D_c_option_fun$'|)) |tptp.'C_set$'| (as |@_tptp.'C_set$'__0| |tptp.'C_set$'|)) % 140.13/140.49 (define-fun |tptp.'bot$r'| () |tptp.'B_bool_fun$'| (as |@_tptp.'B_bool_fun$'__1| |tptp.'B_bool_fun$'|)) % 140.13/140.49 (define-fun |tptp.'restrict_map$h'| (($x1 |tptp.'C_b_option_fun$'|) ($x2 |tptp.'C_set$'|)) |tptp.'C_b_option_fun$'| (as |@_tptp.'C_b_option_fun$'__0| |tptp.'C_b_option_fun$'|)) % 140.13/140.49 (define-fun |tptp.'member$e'| (($x1 |tptp.'C_a_prod$'|) ($x2 |tptp.'C_a_prod_set$'|)) Bool false) % 140.13/140.49 (define-fun |tptp.'fun_app$ar'| (($x1 |tptp.'B_b_b_fun_fun$'|) ($x2 |tptp.'B$'|)) |tptp.'B_b_fun$'| (as |@_tptp.'B_b_fun$'__0| |tptp.'B_b_fun$'|)) % 140.13/140.49 (define-fun |tptp.'relcomp$l'| (($x1 |tptp.'D_b_prod_set$'|) ($x2 |tptp.'B_b_prod_set$'|)) |tptp.'D_b_prod_set$'| (as |@_tptp.'D_b_prod_set$'__0| |tptp.'D_b_prod_set$'|)) % 140.13/140.49 (define-fun |tptp.'curry$c'| (($x1 |tptp.'A_c_prod_bool_fun$'|) ($x2 |tptp.'A$'|)) |tptp.'C_bool_fun$'| (as |@_tptp.'C_bool_fun$'__1| |tptp.'C_bool_fun$'|)) % 140.13/140.49 (define-fun |tptp.'graph$f'| (($x1 |tptp.'C_c_option_fun$'|)) |tptp.'C_c_prod_set$'| (as |@_tptp.'C_c_prod_set$'__0| |tptp.'C_c_prod_set$'|)) % 140.13/140.49 (define-fun |tptp.'finite$d'| (($x1 |tptp.'A_set$'|)) Bool true) % 140.13/140.49 (define-fun |tptp.'image$g'| (($x1 |tptp.'D_d_option_fun$'|) ($x2 |tptp.'D_set$'|)) |tptp.'D_option_set$'| (ite (and (= (as |@_tptp.'D_d_option_fun$'__0| |tptp.'D_d_option_fun$'|) $x1) (= (as |@_tptp.'D_set$'__1| |tptp.'D_set$'|) $x2)) (as |@_tptp.'D_option_set$'__0| |tptp.'D_option_set$'|) (as |@_tptp.'D_option_set$'__1| |tptp.'D_option_set$'|))) % 140.13/140.49 (define-fun |tptp.'bot$p'| () |tptp.'D_bool_fun$'| (as |@_tptp.'D_bool_fun$'__1| |tptp.'D_bool_fun$'|)) % 140.13/140.49 (define-fun |tptp.'fun_app$av'| (($x1 |tptp.'A_c_prod_bool_fun$'|) ($x2 |tptp.'A_c_prod$'|)) Bool false) % 140.13/140.49 (define-fun |tptp.'graph$c'| (($x1 |tptp.'C_d_option_fun$'|)) |tptp.'C_d_prod_set$'| (as |@_tptp.'C_d_prod_set$'__0| |tptp.'C_d_prod_set$'|)) % 140.13/140.49 (define-fun |tptp.'map_comp$d'| (($x1 |tptp.'A_d_option_fun$'|)) |tptp.'A_a_option_fun_a_d_option_fun_fun$'| (as |@_tptp.'A_a_option_fun_a_d_option_fun_fun$'__0| |tptp.'A_a_option_fun_a_d_option_fun_fun$'|)) % 140.13/140.49 (define-fun |tptp.'insert$i'| (($x1 |tptp.'A_d_prod$'|) ($x2 |tptp.'A_d_prod_set$'|)) |tptp.'A_d_prod_set$'| (as |@_tptp.'A_d_prod_set$'__0| |tptp.'A_d_prod_set$'|)) % 140.13/140.49 (define-fun |tptp.'sup$b'| (($x1 |tptp.'D_b_prod_set$'|) ($x2 |tptp.'D_b_prod_set$'|)) |tptp.'D_b_prod_set$'| (as |@_tptp.'D_b_prod_set$'__0| |tptp.'D_b_prod_set$'|)) % 140.13/140.49 (define-fun |tptp.'the_elem$d'| (($x1 |tptp.'A_set$'|)) |tptp.'A$'| (as |@_tptp.'A$'__0| |tptp.'A$'|)) % 140.13/140.49 (define-fun |tptp.'none$b'| () |tptp.'D_option$'| (as |@_tptp.'D_option$'__0| |tptp.'D_option$'|)) % 140.13/140.49 (define-fun |tptp.'set_option$e'| (($x1 |tptp.'C_option_option$'|)) |tptp.'C_option_set$'| (ite (= (as |@_tptp.'C_option_option$'__0| |tptp.'C_option_option$'|) $x1) (as |@_tptp.'C_option_set$'__2| |tptp.'C_option_set$'|) (as |@_tptp.'C_option_set$'__3| |tptp.'C_option_set$'|))) % 140.13/140.49 (define-fun |tptp.'c$'| () |tptp.'A_c_option_fun$'| (as |@_tptp.'A_c_option_fun$'__0| |tptp.'A_c_option_fun$'|)) % 140.13/140.49 (define-fun |tptp.'bot$t'| () |tptp.'D_option_set$'| (as |@_tptp.'D_option_set$'__1| |tptp.'D_option_set$'|)) % 140.13/140.49 (define-fun |tptp.'fun_app$ai'| (($x1 |tptp.'B_b_option_fun_b_option_fun$'|) ($x2 |tptp.'B_b_option_fun$'|)) |tptp.'B_option$'| (ite (and (= (as |@_tptp.'B_b_option_fun_b_option_fun$'__0| |tptp.'B_b_option_fun_b_option_fun$'|) $x1) (= (as |@_tptp.'B_b_option_fun$'__0| |tptp.'B_b_option_fun$'|) $x2)) (as |@_tptp.'B_option$'__0| |tptp.'B_option$'|) (ite (and (= (as |@_tptp.'B_b_option_fun_b_option_fun$'__0| |tptp.'B_b_option_fun_b_option_fun$'|) $x1) (= (as |@_tptp.'B_b_option_fun$'__1| |tptp.'B_b_option_fun$'|) $x2)) (as |@_tptp.'B_option$'__0| |tptp.'B_option$'|) (ite (and (= (as |@_tptp.'B_b_option_fun_b_option_fun$'__1| |tptp.'B_b_option_fun_b_option_fun$'|) $x1) (= (as |@_tptp.'B_b_option_fun$'__1| |tptp.'B_b_option_fun$'|) $x2)) (as |@_tptp.'B_option$'__0| |tptp.'B_option$'|) (as |@_tptp.'B_option$'__1| |tptp.'B_option$'|))))) % 140.13/140.49 (define-fun |tptp.'bot$g'| () |tptp.'A_d_prod_set$'| (as |@_tptp.'A_d_prod_set$'__0| |tptp.'A_d_prod_set$'|)) % 140.13/140.49 (define-fun |tptp.'bot$h'| () |tptp.'C_d_prod_set$'| (as |@_tptp.'C_d_prod_set$'__0| |tptp.'C_d_prod_set$'|)) % 140.13/140.49 (define-fun |tptp.'relcomp$o'| (($x1 |tptp.'A_a_prod_set$'|) ($x2 |tptp.'A_c_prod_set$'|)) |tptp.'A_c_prod_set$'| (as |@_tptp.'A_c_prod_set$'__0| |tptp.'A_c_prod_set$'|)) % 140.13/140.49 (define-fun |tptp.'map_comp$b'| (($x1 |tptp.'D_b_option_fun$'|) ($x2 |tptp.'A_d_option_fun$'|)) |tptp.'A_b_option_fun$'| (as |@_tptp.'A_b_option_fun$'__0| |tptp.'A_b_option_fun$'|)) % 140.13/140.49 (define-fun |tptp.'insert$h'| (($x1 |tptp.'C_d_prod$'|) ($x2 |tptp.'C_d_prod_set$'|)) |tptp.'C_d_prod_set$'| (as |@_tptp.'C_d_prod_set$'__0| |tptp.'C_d_prod_set$'|)) % 140.13/140.49 (define-fun |tptp.'restrict_map$d'| (($x1 |tptp.'B_b_option_fun$'|) ($x2 |tptp.'B_set$'|)) |tptp.'B_b_option_fun$'| (ite (and (= (as |@_tptp.'B_b_option_fun$'__0| |tptp.'B_b_option_fun$'|) $x1) (= (as |@_tptp.'B_set$'__1| |tptp.'B_set$'|) $x2)) (as |@_tptp.'B_b_option_fun$'__0| |tptp.'B_b_option_fun$'|) (as |@_tptp.'B_b_option_fun$'__1| |tptp.'B_b_option_fun$'|))) % 140.13/140.49 (define-fun |tptp.'bind$a'| (($x1 |tptp.'C_option$'|) ($x2 |tptp.'C_d_option_fun$'|)) |tptp.'D_option$'| (as |@_tptp.'D_option$'__0| |tptp.'D_option$'|)) % 140.13/140.49 (define-fun |tptp.'fun_app$c'| (($x1 |tptp.'B_bool_fun$'|) ($x2 |tptp.'B$'|)) Bool (and (= (as |@_tptp.'B_bool_fun$'__0| |tptp.'B_bool_fun$'|) $x1) (= (as |@_tptp.'B$'__0| |tptp.'B$'|) $x2))) % 140.13/140.49 (define-fun |tptp.'restrict_map$c'| (($x1 |tptp.'B_d_option_fun$'|) ($x2 |tptp.'B_set$'|)) |tptp.'B_d_option_fun$'| (as |@_tptp.'B_d_option_fun$'__0| |tptp.'B_d_option_fun$'|)) % 140.13/140.49 (define-fun |tptp.'fun_app$f'| (($x1 |tptp.'A_a_option_fun_a_c_option_fun_fun$'|) ($x2 |tptp.'A_a_option_fun$'|)) |tptp.'A_c_option_fun$'| (as |@_tptp.'A_c_option_fun$'__0| |tptp.'A_c_option_fun$'|)) % 140.13/140.49 (define-fun |tptp.'dom$b'| (($x1 |tptp.'A_d_option_fun$'|)) |tptp.'A_set$'| (as |@_tptp.'A_set$'__0| |tptp.'A_set$'|)) % 140.13/140.49 (define-fun |tptp.'fun_app$as'| (($x1 |tptp.'C_d_prod_bool_fun$'|) ($x2 |tptp.'C_d_prod$'|)) Bool false) % 140.13/140.49 (define-fun |tptp.'bind$e'| (($x1 |tptp.'D_option$'|) ($x2 |tptp.'D_b_option_fun$'|)) |tptp.'B_option$'| (as |@_tptp.'B_option$'__0| |tptp.'B_option$'|)) % 140.13/140.49 (define-fun |tptp.'sup$'| (($x1 |tptp.'C_d_prod_set$'|) ($x2 |tptp.'C_d_prod_set$'|)) |tptp.'C_d_prod_set$'| (as |@_tptp.'C_d_prod_set$'__0| |tptp.'C_d_prod_set$'|)) % 140.13/140.49 (define-fun |tptp.'graph$a'| (($x1 |tptp.'A_c_option_fun$'|)) |tptp.'A_c_prod_set$'| (as |@_tptp.'A_c_prod_set$'__0| |tptp.'A_c_prod_set$'|)) % 140.13/140.49 (define-fun |tptp.'bot$i'| () |tptp.'C_b_prod_set$'| (as |@_tptp.'C_b_prod_set$'__0| |tptp.'C_b_prod_set$'|)) % 140.13/140.49 (define-fun |tptp.'graph$b'| (($x1 |tptp.'C_b_option_fun$'|)) |tptp.'C_b_prod_set$'| (as |@_tptp.'C_b_prod_set$'__0| |tptp.'C_b_prod_set$'|)) % 140.13/140.49 (define-fun |tptp.'set_option$'| (($x1 |tptp.'B_option_option$'|)) |tptp.'B_option_set$'| (ite (= (as |@_tptp.'B_option_option$'__0| |tptp.'B_option_option$'|) $x1) (as |@_tptp.'B_option_set$'__0| |tptp.'B_option_set$'|) (ite (= (as |@_tptp.'B_option_option$'__1| |tptp.'B_option_option$'|) $x1) (as |@_tptp.'B_option_set$'__1| |tptp.'B_option_set$'|) (as |@_tptp.'B_option_set$'__2| |tptp.'B_option_set$'|)))) % 140.13/140.49 (define-fun |tptp.'none$a'| () |tptp.'C_option$'| (as |@_tptp.'C_option$'__0| |tptp.'C_option$'|)) % 140.13/140.49 (define-fun |tptp.'map_comp$a'| (($x1 |tptp.'D_b_option_fun$'|) ($x2 |tptp.'C_d_option_fun$'|)) |tptp.'C_b_option_fun$'| (as |@_tptp.'C_b_option_fun$'__0| |tptp.'C_b_option_fun$'|)) % 140.13/140.49 (define-fun |tptp.'map_comp$e'| (($x1 |tptp.'A_c_option_fun$'|)) |tptp.'A_a_option_fun_a_c_option_fun_fun$'| (as |@_tptp.'A_a_option_fun_a_c_option_fun_fun$'__0| |tptp.'A_a_option_fun_a_c_option_fun_fun$'|)) % 140.13/140.49 (define-fun |tptp.'map_add$c'| (($x1 |tptp.'A_c_option_fun$'|) ($x2 |tptp.'A_c_option_fun$'|)) |tptp.'A_c_option_fun$'| (as |@_tptp.'A_c_option_fun$'__0| |tptp.'A_c_option_fun$'|)) % 140.13/140.49 (define-fun |tptp.'map_comp$j'| (($x1 |tptp.'D_d_option_fun$'|) ($x2 |tptp.'C_d_option_fun$'|)) |tptp.'C_d_option_fun$'| (as |@_tptp.'C_d_option_fun$'__0| |tptp.'C_d_option_fun$'|)) % 140.13/140.49 (define-fun |tptp.'ran$'| (($x1 |tptp.'D_a_option_fun$'|)) |tptp.'A_set$'| (as |@_tptp.'A_set$'__0| |tptp.'A_set$'|)) % 140.13/140.49 (define-fun |tptp.'fun_app$ah'| ((BOUND_VARIABLE_58489 |tptp.'B_d_option_fun$'|) (BOUND_VARIABLE_58491 |tptp.'B$'|)) |tptp.'D_option$'| (as |@_tptp.'D_option$'__0| |tptp.'D_option$'|)) % 140.13/140.49 (define-fun |tptp.'less_eq$c'| (($x1 |tptp.'D_b_prod_set$'|) ($x2 |tptp.'D_b_prod_set$'|)) Bool true) % 140.13/140.49 (define-fun |tptp.'graph$'| (($x1 |tptp.'A_b_option_fun$'|)) |tptp.'A_b_prod_set$'| (as |@_tptp.'A_b_prod_set$'__0| |tptp.'A_b_prod_set$'|)) % 140.13/140.49 (define-fun |tptp.'relcomp$h'| (($x1 |tptp.'C_c_prod_set$'|) ($x2 |tptp.'C_b_prod_set$'|)) |tptp.'C_b_prod_set$'| (as |@_tptp.'C_b_prod_set$'__0| |tptp.'C_b_prod_set$'|)) % 140.13/140.49 (define-fun |tptp.'fun_app$am'| (($x1 |tptp.'D_option_d_option_fun$'|) ($x2 |tptp.'D_option$'|)) |tptp.'D_option$'| (ite (and (= (as |@_tptp.'D_option_d_option_fun$'__0| |tptp.'D_option_d_option_fun$'|) $x1) (= (as |@_tptp.'D_option$'__0| |tptp.'D_option$'|) $x2)) (as |@_tptp.'D_option$'__0| |tptp.'D_option$'|) (as |@_tptp.'D_option$'__1| |tptp.'D_option$'|))) % 140.13/140.49 (define-fun |tptp.'relcomp$p'| (($x1 |tptp.'A_a_prod_set$'|) ($x2 |tptp.'A_d_prod_set$'|)) |tptp.'A_d_prod_set$'| (as |@_tptp.'A_d_prod_set$'__0| |tptp.'A_d_prod_set$'|)) % 140.13/140.49 (define-fun |tptp.'image$d'| (($x1 |tptp.'D_b_prod_set$'|) ($x2 |tptp.'D_set$'|)) |tptp.'B_set$'| (as |@_tptp.'B_set$'__0| |tptp.'B_set$'|)) % 140.13/140.49 (define-fun |tptp.'fun_app$ag'| ((BOUND_VARIABLE_58511 |tptp.'B_c_option_fun$'|) (BOUND_VARIABLE_58513 |tptp.'B$'|)) |tptp.'C_option$'| (as |@_tptp.'C_option$'__0| |tptp.'C_option$'|)) % 140.13/140.49 (define-fun |tptp.'member$h'| (($x1 |tptp.'B_d_prod$'|) ($x2 |tptp.'B_d_prod_set$'|)) Bool false) % 140.13/140.49 (define-fun |tptp.'map_comp$l'| (($x1 |tptp.'C_b_option_fun$'|) ($x2 |tptp.'C_c_option_fun$'|)) |tptp.'C_b_option_fun$'| (as |@_tptp.'C_b_option_fun$'__0| |tptp.'C_b_option_fun$'|)) % 140.13/140.49 (define-fun |tptp.'member$p'| (($x1 |tptp.'C_c_prod$'|) ($x2 |tptp.'C_c_prod_set$'|)) Bool true) % 140.13/140.49 (define-fun |tptp.'fun_app$k'| (($x1 |tptp.'C_a_option_fun$'|) ($x2 |tptp.'C$'|)) |tptp.'A_option$'| (as |@_tptp.'A_option$'__0| |tptp.'A_option$'|)) % 140.13/140.49 (define-fun |tptp.'bot$q'| () |tptp.'C_bool_fun$'| (as |@_tptp.'C_bool_fun$'__1| |tptp.'C_bool_fun$'|)) % 140.13/140.49 (define-fun |tptp.'fun_app$p'| (($x1 |tptp.'D_d_option_fun$'|) ($x2 |tptp.'D$'|)) |tptp.'D_option$'| (ite (and (= (as |@_tptp.'D_d_option_fun$'__1| |tptp.'D_d_option_fun$'|) $x1) (= (as |@_tptp.'D$'__0| |tptp.'D$'|) $x2)) (as |@_tptp.'D_option$'__0| |tptp.'D_option$'|) (as |@_tptp.'D_option$'__1| |tptp.'D_option$'|))) % 140.13/140.49 (define-fun |tptp.'pair$e'| (($x1 |tptp.'A$'|) ($x2 |tptp.'C$'|)) |tptp.'A_c_prod$'| (as |@_tptp.'A_c_prod$'__0| |tptp.'A_c_prod$'|)) % 140.13/140.49 (define-fun |tptp.'sup$d'| (($x1 |tptp.'C_b_prod_set$'|) ($x2 |tptp.'C_b_prod_set$'|)) |tptp.'C_b_prod_set$'| (as |@_tptp.'C_b_prod_set$'__0| |tptp.'C_b_prod_set$'|)) % 140.13/140.49 (define-fun |tptp.'finite$b'| (($x1 |tptp.'C_b_prod_set$'|)) Bool true) % 140.13/140.49 (define-fun |tptp.'fun_app$a'| (($x1 |tptp.'D_bool_fun$'|) ($x2 |tptp.'D$'|)) Bool (and (= (as |@_tptp.'D_bool_fun$'__0| |tptp.'D_bool_fun$'|) $x1) (= (as |@_tptp.'D$'__0| |tptp.'D$'|) $x2))) % 140.13/140.49 (define-fun |tptp.'curry$d'| (($x1 |tptp.'A_b_prod_bool_fun$'|) ($x2 |tptp.'A$'|)) |tptp.'B_bool_fun$'| (as |@_tptp.'B_bool_fun$'__1| |tptp.'B_bool_fun$'|)) % 140.13/140.49 (define-fun |tptp.'pair$f'| (($x1 |tptp.'C$'|) ($x2 |tptp.'D$'|)) |tptp.'C_d_prod$'| (as |@_tptp.'C_d_prod$'__0| |tptp.'C_d_prod$'|)) % 140.13/140.49 (define-fun |tptp.'is_none$'| () |tptp.'B_option_bool_fun$'| (as |@_tptp.'B_option_bool_fun$'__1| |tptp.'B_option_bool_fun$'|)) % 140.13/140.49 (define-fun |tptp.'bind$d'| (($x1 |tptp.'D_option$'|)) |tptp.'D_d_option_fun_d_option_fun$'| (ite (= (as |@_tptp.'D_option$'__0| |tptp.'D_option$'|) $x1) (as |@_tptp.'D_d_option_fun_d_option_fun$'__0| |tptp.'D_d_option_fun_d_option_fun$'|) (as |@_tptp.'D_d_option_fun_d_option_fun$'__1| |tptp.'D_d_option_fun_d_option_fun$'|))) % 140.13/140.49 (define-fun |tptp.'pair$h'| (($x1 |tptp.'C$'|) ($x2 |tptp.'B$'|)) |tptp.'C_b_prod$'| (as |@_tptp.'C_b_prod$'__0| |tptp.'C_b_prod$'|)) % 140.13/140.49 (define-fun |tptp.'fun_app$aq'| (($x1 |tptp.'B_b_fun$'|) ($x2 |tptp.'B$'|)) |tptp.'B$'| (as |@_tptp.'B$'__0| |tptp.'B$'|)) % 140.13/140.49 (define-fun |tptp.'less_eq$b'| (($x1 |tptp.'A_d_prod_set$'|) ($x2 |tptp.'A_d_prod_set$'|)) Bool false) % 140.13/140.49 (define-fun |tptp.'graph$d'| (($x1 |tptp.'D_b_option_fun$'|)) |tptp.'D_b_prod_set$'| (as |@_tptp.'D_b_prod_set$'__0| |tptp.'D_b_prod_set$'|)) % 140.13/140.49 (define-fun |tptp.'fun_app$r'| (($x1 |tptp.'B_b_option_fun$'|) ($x2 |tptp.'B$'|)) |tptp.'B_option$'| (ite (and (= (as |@_tptp.'B_b_option_fun$'__1| |tptp.'B_b_option_fun$'|) $x1) (= (as |@_tptp.'B$'__0| |tptp.'B$'|) $x2)) (as |@_tptp.'B_option$'__0| |tptp.'B_option$'|) (as |@_tptp.'B_option$'__1| |tptp.'B_option$'|))) % 140.13/140.49 (define-fun |tptp.'map_comp$'| (($x1 |tptp.'C_b_option_fun$'|) ($x2 |tptp.'A_c_option_fun$'|)) |tptp.'A_b_option_fun$'| (as |@_tptp.'A_b_option_fun$'__1| |tptp.'A_b_option_fun$'|)) % 140.13/140.49 (define-fun |tptp.'collect$c'| (($x1 |tptp.'B_bool_fun$'|)) |tptp.'B_set$'| (ite (= (as |@_tptp.'B_bool_fun$'__1| |tptp.'B_bool_fun$'|) $x1) (as |@_tptp.'B_set$'__0| |tptp.'B_set$'|) (as |@_tptp.'B_set$'__1| |tptp.'B_set$'|))) % 140.13/140.49 (define-fun |tptp.'fun_app$aw'| (($x1 |tptp.'A_b_prod_bool_fun$'|) ($x2 |tptp.'A_b_prod$'|)) Bool false) % 140.13/140.49 (define-fun |tptp.'bind$'| (($x1 |tptp.'C_option$'|)) |tptp.'C_c_option_fun_c_option_fun$'| (ite (= (as |@_tptp.'C_option$'__0| |tptp.'C_option$'|) $x1) (as |@_tptp.'C_c_option_fun_c_option_fun$'__0| |tptp.'C_c_option_fun_c_option_fun$'|) (as |@_tptp.'C_c_option_fun_c_option_fun$'__1| |tptp.'C_c_option_fun_c_option_fun$'|))) % 140.13/140.49 (define-fun |tptp.'insert$b'| (($x1 |tptp.'A$'|) ($x2 |tptp.'A_set$'|)) |tptp.'A_set$'| (as |@_tptp.'A_set$'__1| |tptp.'A_set$'|)) % 140.13/140.49 (define-fun |tptp.'relcomp$n'| (($x1 |tptp.'A_b_prod_set$'|) ($x2 |tptp.'B_d_prod_set$'|)) |tptp.'A_d_prod_set$'| (as |@_tptp.'A_d_prod_set$'__0| |tptp.'A_d_prod_set$'|)) % 140.13/140.49 (define-fun |tptp.'relcomp$s'| (($x1 |tptp.'D_d_prod_set$'|) ($x2 |tptp.'D_b_prod_set$'|)) |tptp.'D_b_prod_set$'| (as |@_tptp.'D_b_prod_set$'__0| |tptp.'D_b_prod_set$'|)) % 140.13/140.49 (define-fun |tptp.'curry$b'| (($x1 |tptp.'A_d_prod_bool_fun$'|) ($x2 |tptp.'A$'|)) |tptp.'D_bool_fun$'| (as |@_tptp.'D_bool_fun$'__1| |tptp.'D_bool_fun$'|)) % 140.13/140.49 (define-fun |tptp.'member$k'| (($x1 |tptp.'C_d_prod$'|) ($x2 |tptp.'C_d_prod_set$'|)) Bool false) % 140.13/140.49 (define-fun |tptp.'relcomp$j'| (($x1 |tptp.'A_d_prod_set$'|) ($x2 |tptp.'D_d_prod_set$'|)) |tptp.'A_d_prod_set$'| (as |@_tptp.'A_d_prod_set$'__0| |tptp.'A_d_prod_set$'|)) % 140.13/140.49 (define-fun |tptp.'map_add$b'| (($x1 |tptp.'A_d_option_fun$'|) ($x2 |tptp.'A_d_option_fun$'|)) |tptp.'A_d_option_fun$'| (as |@_tptp.'A_d_option_fun$'__0| |tptp.'A_d_option_fun$'|)) % 140.13/140.49 (define-fun |tptp.'the_elem$b'| (($x1 |tptp.'C_set$'|)) |tptp.'C$'| (as |@_tptp.'C$'__0| |tptp.'C$'|)) % 140.13/140.49 (define-fun |tptp.'finite$f'| (($x1 |tptp.'A_b_prod_set$'|)) Bool true) % 140.13/140.49 (define-fun |tptp.'fun_app$ap'| (($x1 |tptp.'B_option_b_option_fun$'|) ($x2 |tptp.'B_option$'|)) |tptp.'B_option$'| (ite (and (= (as |@_tptp.'B_option_b_option_fun$'__0| |tptp.'B_option_b_option_fun$'|) $x1) (= (as |@_tptp.'B_option$'__0| |tptp.'B_option$'|) $x2)) (as |@_tptp.'B_option$'__0| |tptp.'B_option$'|) (as |@_tptp.'B_option$'__1| |tptp.'B_option$'|))) % 140.13/140.49 (define-fun |tptp.'bot$c'| () |tptp.'A_set$'| (as |@_tptp.'A_set$'__0| |tptp.'A_set$'|)) % 140.13/140.49 (define-fun |tptp.'member$l'| (($x1 |tptp.'A_d_prod$'|) ($x2 |tptp.'A_d_prod_set$'|)) Bool false) % 140.13/140.49 (define-fun |tptp.'some$e'| (($x1 |tptp.'C_option$'|)) |tptp.'C_option_option$'| (ite (= (as |@_tptp.'C_option$'__0| |tptp.'C_option$'|) $x1) (as |@_tptp.'C_option_option$'__0| |tptp.'C_option_option$'|) (as |@_tptp.'C_option_option$'__1| |tptp.'C_option_option$'|))) % 140.13/140.49 (define-fun |tptp.'dom$a'| (($x1 |tptp.'C_b_option_fun$'|)) |tptp.'C_set$'| (as |@_tptp.'C_set$'__0| |tptp.'C_set$'|)) % 140.13/140.49 (define-fun |tptp.'insert$f'| (($x1 |tptp.'D_option$'|) ($x2 |tptp.'D_option_set$'|)) |tptp.'D_option_set$'| (ite (and (= (as |@_tptp.'D_option$'__1| |tptp.'D_option$'|) $x1) (= (as |@_tptp.'D_option_set$'__1| |tptp.'D_option_set$'|) $x2)) (as |@_tptp.'D_option_set$'__0| |tptp.'D_option_set$'|) (ite (and (= (as |@_tptp.'D_option$'__0| |tptp.'D_option$'|) $x1) (= (as |@_tptp.'D_option_set$'__0| |tptp.'D_option_set$'|) $x2)) (as |@_tptp.'D_option_set$'__0| |tptp.'D_option_set$'|) (ite (and (= (as |@_tptp.'D_option$'__1| |tptp.'D_option$'|) $x1) (= (as |@_tptp.'D_option_set$'__0| |tptp.'D_option_set$'|) $x2)) (as |@_tptp.'D_option_set$'__0| |tptp.'D_option_set$'|) (as |@_tptp.'D_option_set$'__1| |tptp.'D_option_set$'|))))) % 140.13/140.49 (define-fun |tptp.'fun_upd$'| (($x1 |tptp.'A_c_option_fun$'|) ($x2 |tptp.'A$'|) ($x3 |tptp.'C_option$'|)) |tptp.'A_c_option_fun$'| (as |@_tptp.'A_c_option_fun$'__0| |tptp.'A_c_option_fun$'|)) % 140.13/140.49 (define-fun |tptp.'sup$e'| (($x1 |tptp.'A_c_prod_set$'|) ($x2 |tptp.'A_c_prod_set$'|)) |tptp.'A_c_prod_set$'| (as |@_tptp.'A_c_prod_set$'__0| |tptp.'A_c_prod_set$'|)) % 140.13/140.49 (define-fun |tptp.'bind$c'| (($x1 |tptp.'D_option$'|) ($x2 |tptp.'D_c_option_fun$'|)) |tptp.'C_option$'| (as |@_tptp.'C_option$'__0| |tptp.'C_option$'|)) % 140.13/140.49 (define-fun |tptp.'image$b'| (($x1 |tptp.'A_c_prod_set$'|) ($x2 |tptp.'A_set$'|)) |tptp.'C_set$'| (as |@_tptp.'C_set$'__0| |tptp.'C_set$'|)) % 140.13/140.49 (define-fun |tptp.'fun_app$ak'| (($x1 |tptp.'C_c_fun$'|) ($x2 |tptp.'C$'|)) |tptp.'C$'| (as |@_tptp.'C$'__0| |tptp.'C$'|)) % 140.13/140.49 (define-fun |tptp.'member$a'| ((BOUND_VARIABLE_9499 |tptp.'D$'|) (BOUND_VARIABLE_9500 |tptp.'D_set$'|)) Bool (and (= (as |@_tptp.'D_bool_fun$'__0| |tptp.'D_bool_fun$'|) (ite (= BOUND_VARIABLE_9500 (as |@_tptp.'D_set$'__1| |tptp.'D_set$'|)) (as |@_tptp.'D_bool_fun$'__0| |tptp.'D_bool_fun$'|) (as |@_tptp.'D_bool_fun$'__1| |tptp.'D_bool_fun$'|))) (= BOUND_VARIABLE_9499 (as |@_tptp.'D$'__0| |tptp.'D$'|)))) % 140.13/140.49 (define-fun |tptp.'bind$g'| (($x1 |tptp.'B_option$'|) ($x2 |tptp.'B_d_option_fun$'|)) |tptp.'D_option$'| (as |@_tptp.'D_option$'__0| |tptp.'D_option$'|)) % 140.13/140.49 (define-fun |tptp.'bot$o'| () |tptp.'B_option_bool_fun$'| (as |@_tptp.'B_option_bool_fun$'__0| |tptp.'B_option_bool_fun$'|)) % 140.13/140.49 (define-fun |tptp.'set_option$c'| (($x1 |tptp.'D_option$'|)) |tptp.'D_set$'| (ite (= (as |@_tptp.'D_option$'__0| |tptp.'D_option$'|) $x1) (as |@_tptp.'D_set$'__0| |tptp.'D_set$'|) (as |@_tptp.'D_set$'__1| |tptp.'D_set$'|))) % 140.13/140.49 (define-fun |tptp.'bot$'| () |tptp.'D_set$'| (as |@_tptp.'D_set$'__0| |tptp.'D_set$'|)) % 140.13/140.49 (define-fun |tptp.'curry$a'| (($x1 |tptp.'C_b_prod_bool_fun$'|) ($x2 |tptp.'C$'|)) |tptp.'B_bool_fun$'| (as |@_tptp.'B_bool_fun$'__1| |tptp.'B_bool_fun$'|)) % 140.13/140.49 (define-fun |tptp.'some$c'| () |tptp.'B_b_option_fun$'| (as |@_tptp.'B_b_option_fun$'__0| |tptp.'B_b_option_fun$'|)) % 140.13/140.49 (define-fun |tptp.'bot$j'| () |tptp.'B_c_prod_set$'| (as |@_tptp.'B_c_prod_set$'__0| |tptp.'B_c_prod_set$'|)) % 140.13/140.49 (define-fun |tptp.'relcomp$i'| (($x1 |tptp.'C_a_prod_set$'|) ($x2 |tptp.'A_b_prod_set$'|)) |tptp.'C_b_prod_set$'| (as |@_tptp.'C_b_prod_set$'__0| |tptp.'C_b_prod_set$'|)) % 140.13/140.49 (define-fun |tptp.'curry$'| (($x1 |tptp.'C_d_prod_bool_fun$'|) ($x2 |tptp.'C$'|)) |tptp.'D_bool_fun$'| (as |@_tptp.'D_bool_fun$'__1| |tptp.'D_bool_fun$'|)) % 140.13/140.49 (define-fun |tptp.'fun_app$o'| (($x1 |tptp.'C_c_option_fun$'|) ($x2 |tptp.'C$'|)) |tptp.'C_option$'| (ite (and (= (as |@_tptp.'C_c_option_fun$'__1| |tptp.'C_c_option_fun$'|) $x1) (= (as |@_tptp.'C$'__0| |tptp.'C$'|) $x2)) (as |@_tptp.'C_option$'__0| |tptp.'C_option$'|) (as |@_tptp.'C_option$'__1| |tptp.'C_option$'|))) % 140.13/140.49 (define-fun |tptp.'image$'| (($x1 |tptp.'A_d_prod_set$'|) ($x2 |tptp.'A_set$'|)) |tptp.'D_set$'| (as |@_tptp.'D_set$'__0| |tptp.'D_set$'|)) % 140.13/140.49 (define-fun |tptp.'restrict_map$j'| (($x1 |tptp.'D_c_option_fun$'|) ($x2 |tptp.'D_set$'|)) |tptp.'D_c_option_fun$'| (as |@_tptp.'D_c_option_fun$'__0| |tptp.'D_c_option_fun$'|)) % 140.13/140.49 (define-fun |tptp.'fun_app$q'| (($x1 |tptp.'D_b_option_fun$'|) ($x2 |tptp.'D$'|)) |tptp.'B_option$'| (as |@_tptp.'B_option$'__0| |tptp.'B_option$'|)) % 140.13/140.49 (define-fun |tptp.'fun_app$d'| (($x1 |tptp.'A_bool_fun$'|) ($x2 |tptp.'A$'|)) Bool (and (= (as |@_tptp.'A_bool_fun$'__1| |tptp.'A_bool_fun$'|) $x1) (= (as |@_tptp.'A$'__0| |tptp.'A$'|) $x2))) % 140.13/140.49 (define-fun |tptp.'pair$k'| (($x1 |tptp.'C$'|) ($x2 |tptp.'C$'|)) |tptp.'C_c_prod$'| (as |@_tptp.'C_c_prod$'__0| |tptp.'C_c_prod$'|)) % 140.13/140.49 (define-fun |tptp.'fun_app$x'| (($x1 |tptp.'D_option_c_option_bool_fun_fun$'|) ($x2 |tptp.'D_option$'|)) |tptp.'C_option_bool_fun$'| (as |@_tptp.'C_option_bool_fun$'__0| |tptp.'C_option_bool_fun$'|)) % 140.13/140.49 (define-fun |tptp.'member$s'| (($x1 |tptp.'D_option$'|) ($x2 |tptp.'D_option_set$'|)) Bool (and (= (as |@_tptp.'D_option$'__1| |tptp.'D_option$'|) $x1) (= (as |@_tptp.'D_option_set$'__0| |tptp.'D_option_set$'|) $x2))) % 140.13/140.49 (define-fun |tptp.'fun_app$ac'| (($x1 |tptp.'B_option_b_option_bool_fun_fun$'|) ($x2 |tptp.'B_option$'|)) |tptp.'B_option_bool_fun$'| (as |@_tptp.'B_option_bool_fun$'__0| |tptp.'B_option_bool_fun$'|)) % 140.13/140.49 (define-fun |tptp.'dom$c'| (($x1 |tptp.'A_c_option_fun$'|)) |tptp.'A_set$'| (as |@_tptp.'A_set$'__0| |tptp.'A_set$'|)) % 140.13/140.49 (define-fun |tptp.'bot$f'| () |tptp.'A_a_prod_set$'| (as |@_tptp.'A_a_prod_set$'__0| |tptp.'A_a_prod_set$'|)) % 140.13/140.49 (define-fun |tptp.'combine_options$b'| (($x1 |tptp.'B_b_b_fun_fun$'|) ($x2 |tptp.'B_option$'|)) |tptp.'B_option_b_option_fun$'| (ite (and (= (as |@_tptp.'B_b_b_fun_fun$'__0| |tptp.'B_b_b_fun_fun$'|) $x1) (= (as |@_tptp.'B_option$'__0| |tptp.'B_option$'|) $x2)) (as |@_tptp.'B_option_b_option_fun$'__0| |tptp.'B_option_b_option_fun$'|) (as |@_tptp.'B_option_b_option_fun$'__1| |tptp.'B_option_b_option_fun$'|))) % 140.13/140.49 (define-fun |tptp.'the_elem$c'| (($x1 |tptp.'B_set$'|)) |tptp.'B$'| (as |@_tptp.'B$'__0| |tptp.'B$'|)) % 140.13/140.49 (define-fun |tptp.'the$'| (($x1 |tptp.'C_option$'|)) |tptp.'C$'| (as |@_tptp.'C$'__0| |tptp.'C$'|)) % 140.13/140.49 (define-fun |tptp.'fun_upd$d'| (($x1 |tptp.'A_b_option_fun$'|) ($x2 |tptp.'A$'|) ($x3 |tptp.'B_option$'|)) |tptp.'A_b_option_fun$'| (as |@_tptp.'A_b_option_fun$'__0| |tptp.'A_b_option_fun$'|)) % 140.13/140.49 (define-fun |tptp.'ran$e'| (($x1 |tptp.'C_c_option_fun$'|)) |tptp.'C_set$'| (as |@_tptp.'C_set$'__0| |tptp.'C_set$'|)) % 140.13/140.49 (define-fun |tptp.'fun_app$v'| (($x1 |tptp.'C_option_d_option_bool_fun_fun$'|) ($x2 |tptp.'C_option$'|)) |tptp.'D_option_bool_fun$'| (as |@_tptp.'D_option_bool_fun$'__0| |tptp.'D_option_bool_fun$'|)) % 140.13/140.49 (define-fun |tptp.'none$'| () |tptp.'A_option$'| (as |@_tptp.'A_option$'__0| |tptp.'A_option$'|)) % 140.13/140.49 (define-fun |tptp.'bot$d'| () |tptp.'A_b_prod_set$'| (as |@_tptp.'A_b_prod_set$'__0| |tptp.'A_b_prod_set$'|)) % 140.13/140.49 (define-fun |tptp.'ran$b'| (($x1 |tptp.'B_a_option_fun$'|)) |tptp.'A_set$'| (as |@_tptp.'A_set$'__0| |tptp.'A_set$'|)) % 140.13/140.49 (define-fun |tptp.'insert$k'| (($x1 |tptp.'A_b_prod$'|) ($x2 |tptp.'A_b_prod_set$'|)) |tptp.'A_b_prod_set$'| (as |@_tptp.'A_b_prod_set$'__0| |tptp.'A_b_prod_set$'|)) % 140.13/140.49 (define-fun |tptp.'member$n'| (($x1 |tptp.'A_b_prod$'|) ($x2 |tptp.'A_b_prod_set$'|)) Bool false) % 140.13/140.49 (define-fun |tptp.'map_comp$h'| (($x1 |tptp.'A_b_option_fun$'|) ($x2 |tptp.'C_a_option_fun$'|)) |tptp.'C_b_option_fun$'| (as |@_tptp.'C_b_option_fun$'__0| |tptp.'C_b_option_fun$'|)) % 140.13/140.49 (define-fun |tptp.'some$b'| () |tptp.'D_d_option_fun$'| (as |@_tptp.'D_d_option_fun$'__0| |tptp.'D_d_option_fun$'|)) % 140.13/140.49 (define-fun |tptp.'ran$f'| (($x1 |tptp.'B_c_option_fun$'|)) |tptp.'C_set$'| (as |@_tptp.'C_set$'__0| |tptp.'C_set$'|)) % 140.13/140.49 ) % 140.13/140.49 % SZS output end Model % 140.13/140.49 % cvc5 exiting %------------------------------------------------------------------------------