%------------------------------------------------------------------------------ % File : cvc5-SAT---1.3.4 % Problem : ITP322_10 : TPTP v9.2.1. Released v8.2.0. % Transfm : none % Format : tptp:raw % Command : /export/starexec/sandbox/solver/bin/do_cvc5 /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % Computer : n002.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8042.1875MB % OS : Linux 3.10.0-693.el7.x86_64 % CPULimit : 300s % WCLimit : 300s % DateTime : Wed Jun 3 08:27:55 AM UTC 2026 % Result : Satisfiable 137.57s 137.85s % Output : Model 137.57s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : ITP322_10 : TPTP v9.2.1. Released v8.2.0. % 0.12/0.13 % Command : /export/starexec/sandbox/solver/bin/do_cvc5 /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % 0.17/0.34 % Computer : n002.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 04:59:33 EDT 2026 % 0.17/0.34 % CPUTime : % 0.40/0.66 %----Disproving TF0_NAR % 0.40/0.68 --- Run --finite-model-find --sort-inference --uf-ss-fair at 60... % 0.51/0.73 --- Run --mbqi at 45... % 45.61/45.83 --- Run --mbqi --mbqi-enum --mbqi-enum-choice-grammar --mbqi-enum-global-syms-grammar --no-cegqi --no-sygus-inst at 45... % 45.65/90.91 --- Run --full-saturate-quant at 45... % 135.79/136.04 --- Run --finite-model-find --fmf-bound --macros-quant at 60... % 137.57/137.85 % SZS status Satisfiable % 137.57/137.85 % SZS output start Model % 137.57/137.86 ( % 137.57/137.86 ; cardinality of $$unsorted is 1 % 137.57/137.86 ; rep: (as @$$unsorted_0 $$unsorted) % 137.57/137.86 ; cardinality of |tptp.'B_bool_fun_b_bool_fun_fun$'| is 4 % 137.57/137.86 ; rep: (as |@_tptp.'B_bool_fun_b_bool_fun_fun$'__0| |tptp.'B_bool_fun_b_bool_fun_fun$'|) % 137.57/137.86 ; rep: (as |@_tptp.'B_bool_fun_b_bool_fun_fun$'__1| |tptp.'B_bool_fun_b_bool_fun_fun$'|) % 137.57/137.86 ; rep: (as |@_tptp.'B_bool_fun_b_bool_fun_fun$'__2| |tptp.'B_bool_fun_b_bool_fun_fun$'|) % 137.57/137.86 ; rep: (as |@_tptp.'B_bool_fun_b_bool_fun_fun$'__3| |tptp.'B_bool_fun_b_bool_fun_fun$'|) % 137.57/137.86 ; cardinality of |tptp.'B_bool_fun_b_bool_fun_bool_fun_fun$'| is 2 % 137.57/137.86 ; rep: (as |@_tptp.'B_bool_fun_b_bool_fun_bool_fun_fun$'__0| |tptp.'B_bool_fun_b_bool_fun_bool_fun_fun$'|) % 137.57/137.86 ; rep: (as |@_tptp.'B_bool_fun_b_bool_fun_bool_fun_fun$'__1| |tptp.'B_bool_fun_b_bool_fun_bool_fun_fun$'|) % 137.57/137.86 ; cardinality of |tptp.'B_bool_fun_bool_fun$'| is 3 % 137.57/137.86 ; rep: (as |@_tptp.'B_bool_fun_bool_fun$'__0| |tptp.'B_bool_fun_bool_fun$'|) % 137.57/137.86 ; rep: (as |@_tptp.'B_bool_fun_bool_fun$'__1| |tptp.'B_bool_fun_bool_fun$'|) % 137.57/137.86 ; rep: (as |@_tptp.'B_bool_fun_bool_fun$'__2| |tptp.'B_bool_fun_bool_fun$'|) % 137.57/137.86 ; cardinality of |tptp.'B$'| is 1 % 137.57/137.86 ; rep: (as |@_tptp.'B$'__0| |tptp.'B$'|) % 137.57/137.86 ; cardinality of |tptp.'B_bool_fun_b_set_fun$'| is 1 % 137.57/137.86 ; rep: (as |@_tptp.'B_bool_fun_b_set_fun$'__0| |tptp.'B_bool_fun_b_set_fun$'|) % 137.57/137.86 ; cardinality of |tptp.'B_set_b_set_bool_fun_fun$'| is 2 % 137.57/137.86 ; rep: (as |@_tptp.'B_set_b_set_bool_fun_fun$'__0| |tptp.'B_set_b_set_bool_fun_fun$'|) % 137.57/137.86 ; rep: (as |@_tptp.'B_set_b_set_bool_fun_fun$'__1| |tptp.'B_set_b_set_bool_fun_fun$'|) % 137.57/137.86 ; cardinality of |tptp.'B_bool_fun_b_bool_fun_b_bool_fun_fun_fun$'| is 3 % 137.57/137.86 ; rep: (as |@_tptp.'B_bool_fun_b_bool_fun_b_bool_fun_fun_fun$'__0| |tptp.'B_bool_fun_b_bool_fun_b_bool_fun_fun_fun$'|) % 137.57/137.86 ; rep: (as |@_tptp.'B_bool_fun_b_bool_fun_b_bool_fun_fun_fun$'__1| |tptp.'B_bool_fun_b_bool_fun_b_bool_fun_fun_fun$'|) % 137.57/137.86 ; rep: (as |@_tptp.'B_bool_fun_b_bool_fun_b_bool_fun_fun_fun$'__2| |tptp.'B_bool_fun_b_bool_fun_b_bool_fun_fun_fun$'|) % 137.57/137.86 ; cardinality of tptp.tlbool is 2 % 137.57/137.86 ; rep: (as @tptp.tlbool_0 tptp.tlbool) % 137.57/137.86 ; rep: (as @tptp.tlbool_1 tptp.tlbool) % 137.57/137.86 ; cardinality of |tptp.'B_set_b_set_b_set_fun_fun$'| is 3 % 137.57/137.86 ; rep: (as |@_tptp.'B_set_b_set_b_set_fun_fun$'__0| |tptp.'B_set_b_set_b_set_fun_fun$'|) % 137.57/137.86 ; rep: (as |@_tptp.'B_set_b_set_b_set_fun_fun$'__1| |tptp.'B_set_b_set_b_set_fun_fun$'|) % 137.57/137.86 ; rep: (as |@_tptp.'B_set_b_set_b_set_fun_fun$'__2| |tptp.'B_set_b_set_b_set_fun_fun$'|) % 137.57/137.86 ; cardinality of |tptp.'B_b_bool_fun_fun$'| is 1 % 137.57/137.86 ; rep: (as |@_tptp.'B_b_bool_fun_fun$'__0| |tptp.'B_b_bool_fun_fun$'|) % 137.57/137.86 ; cardinality of |tptp.'B_set$'| is 2 % 137.57/137.86 ; rep: (as |@_tptp.'B_set$'__0| |tptp.'B_set$'|) % 137.57/137.86 ; rep: (as |@_tptp.'B_set$'__1| |tptp.'B_set$'|) % 137.57/137.86 ; cardinality of |tptp.'B_set_b_bool_fun_fun$'| is 1 % 137.57/137.86 ; rep: (as |@_tptp.'B_set_b_bool_fun_fun$'__0| |tptp.'B_set_b_bool_fun_fun$'|) % 137.57/137.86 ; cardinality of |tptp.'B_set_bool_fun$'| is 3 % 137.57/137.86 ; rep: (as |@_tptp.'B_set_bool_fun$'__0| |tptp.'B_set_bool_fun$'|) % 137.57/137.86 ; rep: (as |@_tptp.'B_set_bool_fun$'__1| |tptp.'B_set_bool_fun$'|) % 137.57/137.86 ; rep: (as |@_tptp.'B_set_bool_fun$'__2| |tptp.'B_set_bool_fun$'|) % 137.57/137.86 ; cardinality of |tptp.'Bool_bool_fun$'| is 2 % 137.57/137.86 ; rep: (as |@_tptp.'Bool_bool_fun$'__0| |tptp.'Bool_bool_fun$'|) % 137.57/137.86 ; rep: (as |@_tptp.'Bool_bool_fun$'__1| |tptp.'Bool_bool_fun$'|) % 137.57/137.86 ; cardinality of |tptp.'B_set_b_set_fun$'| is 4 % 137.57/137.86 ; rep: (as |@_tptp.'B_set_b_set_fun$'__0| |tptp.'B_set_b_set_fun$'|) % 137.57/137.86 ; rep: (as |@_tptp.'B_set_b_set_fun$'__1| |tptp.'B_set_b_set_fun$'|) % 137.57/137.86 ; rep: (as |@_tptp.'B_set_b_set_fun$'__2| |tptp.'B_set_b_set_fun$'|) % 137.57/137.86 ; rep: (as |@_tptp.'B_set_b_set_fun$'__3| |tptp.'B_set_b_set_fun$'|) % 137.57/137.86 ; cardinality of |tptp.'B_bool_fun$'| is 2 % 137.57/137.86 ; rep: (as |@_tptp.'B_bool_fun$'__0| |tptp.'B_bool_fun$'|) % 137.57/137.86 ; rep: (as |@_tptp.'B_bool_fun$'__1| |tptp.'B_bool_fun$'|) % 137.57/137.86 ; cardinality of |tptp.'Bool_bool_bool_fun_fun$'| is 1 % 137.57/137.86 ; rep: (as |@_tptp.'Bool_bool_bool_fun_fun$'__0| |tptp.'Bool_bool_bool_fun_fun$'|) % 137.57/137.86 (define-fun tptp.def_12 () tptp.tlbool (as @tptp.tlbool_1 tptp.tlbool)) % 137.57/137.86 (define-fun tptp.def_33 (($x1 |tptp.'B_bool_fun$'|) ($x2 |tptp.'B$'|)) tptp.tlbool (ite (and (= (as |@_tptp.'B_bool_fun$'__0| |tptp.'B_bool_fun$'|) $x1) (= (as |@_tptp.'B$'__0| |tptp.'B$'|) $x2)) (as @tptp.tlbool_0 tptp.tlbool) (as @tptp.tlbool_1 tptp.tlbool))) % 137.57/137.86 (define-fun |tptp.'semilattice_neutr$'| ((_arg_1 |tptp.'Bool_bool_bool_fun_fun$'|) (_arg_2 tptp.tlbool)) Bool true) % 137.57/137.86 (define-fun tptp.def_15 (($x1 |tptp.'B_bool_fun$'|) ($x2 |tptp.'B$'|)) tptp.tlbool (ite (and (= (as |@_tptp.'B_bool_fun$'__0| |tptp.'B_bool_fun$'|) $x1) (= (as |@_tptp.'B$'__0| |tptp.'B$'|) $x2)) (as @tptp.tlbool_0 tptp.tlbool) (as @tptp.tlbool_1 tptp.tlbool))) % 137.57/137.86 (define-fun tptp.def_17 () tptp.tlbool (as @tptp.tlbool_1 tptp.tlbool)) % 137.57/137.86 (define-fun tptp.def_39 (($x1 tptp.tlbool)) tptp.tlbool (ite (= (as @tptp.tlbool_1 tptp.tlbool) $x1) (as @tptp.tlbool_0 tptp.tlbool) (as @tptp.tlbool_1 tptp.tlbool))) % 137.57/137.86 (define-fun |tptp.'fun_app$i'| (($x1 |tptp.'B_set_bool_fun$'|) ($x2 |tptp.'B_set$'|)) Bool (or (and (= (as |@_tptp.'B_set_bool_fun$'__2| |tptp.'B_set_bool_fun$'|) $x1) (= (as |@_tptp.'B_set$'__0| |tptp.'B_set$'|) $x2)) (and (= (as |@_tptp.'B_set_bool_fun$'__1| |tptp.'B_set_bool_fun$'|) $x1) (= (as |@_tptp.'B_set$'__1| |tptp.'B_set$'|) $x2)) (and (= (as |@_tptp.'B_set_bool_fun$'__2| |tptp.'B_set_bool_fun$'|) $x1) (= (as |@_tptp.'B_set$'__1| |tptp.'B_set$'|) $x2)))) % 137.57/137.86 (define-fun |tptp.'less_eq$a'| () |tptp.'B_bool_fun_b_bool_fun_bool_fun_fun$'| (as |@_tptp.'B_bool_fun_b_bool_fun_bool_fun_fun$'__1| |tptp.'B_bool_fun_b_bool_fun_bool_fun_fun$'|)) % 137.57/137.86 (define-fun |tptp.'bot$a'| () Bool false) % 137.57/137.86 (define-fun |tptp.'top$a'| () Bool true) % 137.57/137.86 (define-fun |tptp.'a$'| () |tptp.'B$'| (as |@_tptp.'B$'__0| |tptp.'B$'|)) % 137.57/137.86 (define-fun |tptp.'fun_app$b'| (($x1 |tptp.'B_set_b_set_fun$'|) ($x2 |tptp.'B_set$'|)) |tptp.'B_set$'| (ite (and (= (as |@_tptp.'B_set_b_set_fun$'__2| |tptp.'B_set_b_set_fun$'|) $x1) (= (as |@_tptp.'B_set$'__0| |tptp.'B_set$'|) $x2)) (as |@_tptp.'B_set$'__0| |tptp.'B_set$'|) (ite (and (= (as |@_tptp.'B_set_b_set_fun$'__3| |tptp.'B_set_b_set_fun$'|) $x1) (= (as |@_tptp.'B_set$'__1| |tptp.'B_set$'|) $x2)) (as |@_tptp.'B_set$'__0| |tptp.'B_set$'|) (ite (and (= (as |@_tptp.'B_set_b_set_fun$'__0| |tptp.'B_set_b_set_fun$'|) $x1) (= (as |@_tptp.'B_set$'__1| |tptp.'B_set$'|) $x2)) (as |@_tptp.'B_set$'__0| |tptp.'B_set$'|) (ite (and (= (as |@_tptp.'B_set_b_set_fun$'__3| |tptp.'B_set_b_set_fun$'|) $x1) (= (as |@_tptp.'B_set$'__0| |tptp.'B_set$'|) $x2)) (as |@_tptp.'B_set$'__0| |tptp.'B_set$'|) (as |@_tptp.'B_set$'__1| |tptp.'B_set$'|)))))) % 137.57/137.86 (define-fun |tptp.'semilattice_neutr$b'| ((_arg_1 |tptp.'B_set_b_set_b_set_fun_fun$'|) (_arg_2 |tptp.'B_set$'|)) Bool true) % 137.57/137.86 (define-fun tptp.def_36 (($x1 tptp.tlbool)) tptp.tlbool (ite (= (as @tptp.tlbool_1 tptp.tlbool) $x1) (as @tptp.tlbool_0 tptp.tlbool) (as @tptp.tlbool_1 tptp.tlbool))) % 137.57/137.86 (define-fun tptp.def_6 () tptp.tlbool (as @tptp.tlbool_1 tptp.tlbool)) % 137.57/137.86 (define-fun tptp.def_21 (($x1 |tptp.'B_bool_fun$'|) ($x2 |tptp.'B$'|)) tptp.tlbool (ite (and (= (as |@_tptp.'B_bool_fun$'__0| |tptp.'B_bool_fun$'|) $x1) (= (as |@_tptp.'B$'__0| |tptp.'B$'|) $x2)) (as @tptp.tlbool_0 tptp.tlbool) (as @tptp.tlbool_1 tptp.tlbool))) % 137.57/137.86 (define-fun |tptp.'less_eq$b'| ((BOUND_VARIABLE_5923 tptp.tlbool) (BOUND_VARIABLE_5924 tptp.tlbool)) Bool (not (and (= BOUND_VARIABLE_5923 (as @tptp.tlbool_0 tptp.tlbool)) (= BOUND_VARIABLE_5924 (as @tptp.tlbool_1 tptp.tlbool))))) % 137.57/137.86 (define-fun |tptp.'collect$'| () |tptp.'B_bool_fun_b_set_fun$'| (as |@_tptp.'B_bool_fun_b_set_fun$'__0| |tptp.'B_bool_fun_b_set_fun$'|)) % 137.57/137.86 (define-fun tptp.def_29 () tptp.tlbool (as @tptp.tlbool_1 tptp.tlbool)) % 137.57/137.86 (define-fun |tptp.'member$'| ((BOUND_VARIABLE_5247 |tptp.'B$'|) (BOUND_VARIABLE_5248 |tptp.'B_set$'|)) Bool (= (as @tptp.tlbool_0 tptp.tlbool) (ite (and (= (as |@_tptp.'B_bool_fun$'__0| |tptp.'B_bool_fun$'|) (ite (= BOUND_VARIABLE_5248 (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_5247 (as |@_tptp.'B$'__0| |tptp.'B$'|))) (as @tptp.tlbool_0 tptp.tlbool) (as @tptp.tlbool_1 tptp.tlbool)))) % 137.57/137.86 (define-fun tptp.def_4 () tptp.tlbool (as @tptp.tlbool_0 tptp.tlbool)) % 137.57/137.86 (define-fun tptp.def_5 () tptp.tlbool (as @tptp.tlbool_1 tptp.tlbool)) % 137.57/137.86 (define-fun |tptp.'top$b'| () |tptp.'B_bool_fun$'| (as |@_tptp.'B_bool_fun$'__0| |tptp.'B_bool_fun$'|)) % 137.57/137.86 (define-fun tptp.def_32 () tptp.tlbool (as @tptp.tlbool_0 tptp.tlbool)) % 137.57/137.86 (define-fun tptp.def_8 (($x1 |tptp.'B_bool_fun$'|) ($x2 |tptp.'B$'|)) tptp.tlbool (ite (and (= (as |@_tptp.'B_bool_fun$'__0| |tptp.'B_bool_fun$'|) $x1) (= (as |@_tptp.'B$'__0| |tptp.'B$'|) $x2)) (as @tptp.tlbool_0 tptp.tlbool) (as @tptp.tlbool_1 tptp.tlbool))) % 137.57/137.86 (define-fun |tptp.'uminus$'| () |tptp.'B_set_b_set_fun$'| (as |@_tptp.'B_set_b_set_fun$'__0| |tptp.'B_set_b_set_fun$'|)) % 137.57/137.86 (define-fun |tptp.'fun_app$j'| (($x1 |tptp.'B_set_b_set_bool_fun_fun$'|) ($x2 |tptp.'B_set$'|)) |tptp.'B_set_bool_fun$'| (ite (and (= (as |@_tptp.'B_set_b_set_bool_fun_fun$'__0| |tptp.'B_set_b_set_bool_fun_fun$'|) $x1) (= (as |@_tptp.'B_set$'__1| |tptp.'B_set$'|) $x2)) (as |@_tptp.'B_set_bool_fun$'__0| |tptp.'B_set_bool_fun$'|) (ite (and (= (as |@_tptp.'B_set_b_set_bool_fun_fun$'__1| |tptp.'B_set_b_set_bool_fun_fun$'|) $x1) (= (as |@_tptp.'B_set$'__1| |tptp.'B_set$'|) $x2)) (as |@_tptp.'B_set_bool_fun$'__1| |tptp.'B_set_bool_fun$'|) (ite (and (= (as |@_tptp.'B_set_b_set_bool_fun_fun$'__0| |tptp.'B_set_b_set_bool_fun_fun$'|) $x1) (= (as |@_tptp.'B_set$'__0| |tptp.'B_set$'|) $x2)) (as |@_tptp.'B_set_bool_fun$'__1| |tptp.'B_set_bool_fun$'|) (as |@_tptp.'B_set_bool_fun$'__2| |tptp.'B_set_bool_fun$'|))))) % 137.57/137.86 (define-fun |tptp.'fun_app$f'| (($x1 |tptp.'Bool_bool_bool_fun_fun$'|) ($x2 tptp.tlbool)) |tptp.'Bool_bool_fun$'| (ite (and (= (as |@_tptp.'Bool_bool_bool_fun_fun$'__0| |tptp.'Bool_bool_bool_fun_fun$'|) $x1) (= (as @tptp.tlbool_1 tptp.tlbool) $x2)) (as |@_tptp.'Bool_bool_fun$'__0| |tptp.'Bool_bool_fun$'|) (as |@_tptp.'Bool_bool_fun$'__1| |tptp.'Bool_bool_fun$'|))) % 137.57/137.86 (define-fun |tptp.'fun_app$a'| (($x1 |tptp.'B_set_b_bool_fun_fun$'|) ($x2 |tptp.'B_set$'|)) |tptp.'B_bool_fun$'| (ite (and (= (as |@_tptp.'B_set_b_bool_fun_fun$'__0| |tptp.'B_set_b_bool_fun_fun$'|) $x1) (= (as |@_tptp.'B_set$'__1| |tptp.'B_set$'|) $x2)) (as |@_tptp.'B_bool_fun$'__0| |tptp.'B_bool_fun$'|) (as |@_tptp.'B_bool_fun$'__1| |tptp.'B_bool_fun$'|))) % 137.57/137.86 (define-fun tptp.def_3 () tptp.tlbool (as @tptp.tlbool_0 tptp.tlbool)) % 137.57/137.86 (define-fun |tptp.'fun_app$c'| (($x1 |tptp.'B_set_b_set_b_set_fun_fun$'|) ($x2 |tptp.'B_set$'|)) |tptp.'B_set_b_set_fun$'| (ite (and (= (as |@_tptp.'B_set_b_set_b_set_fun_fun$'__2| |tptp.'B_set_b_set_b_set_fun_fun$'|) $x1) (= (as |@_tptp.'B_set$'__1| |tptp.'B_set$'|) $x2)) (as |@_tptp.'B_set_b_set_fun$'__0| |tptp.'B_set_b_set_fun$'|) (ite (and (= (as |@_tptp.'B_set_b_set_b_set_fun_fun$'__0| |tptp.'B_set_b_set_b_set_fun_fun$'|) $x1) (= (as |@_tptp.'B_set$'__1| |tptp.'B_set$'|) $x2)) (as |@_tptp.'B_set_b_set_fun$'__1| |tptp.'B_set_b_set_fun$'|) (ite (and (= (as |@_tptp.'B_set_b_set_b_set_fun_fun$'__1| |tptp.'B_set_b_set_b_set_fun_fun$'|) $x1) (= (as |@_tptp.'B_set$'__1| |tptp.'B_set$'|) $x2)) (as |@_tptp.'B_set_b_set_fun$'__2| |tptp.'B_set_b_set_fun$'|) (ite (and (= (as |@_tptp.'B_set_b_set_b_set_fun_fun$'__0| |tptp.'B_set_b_set_b_set_fun_fun$'|) $x1) (= (as |@_tptp.'B_set$'__0| |tptp.'B_set$'|) $x2)) (as |@_tptp.'B_set_b_set_fun$'__2| |tptp.'B_set_b_set_fun$'|) (as |@_tptp.'B_set_b_set_fun$'__3| |tptp.'B_set_b_set_fun$'|)))))) % 137.57/137.86 (define-fun tptp.def_22 (($x1 |tptp.'B_bool_fun$'|) ($x2 |tptp.'B$'|)) tptp.tlbool (ite (and (= (as |@_tptp.'B_bool_fun$'__0| |tptp.'B_bool_fun$'|) $x1) (= (as |@_tptp.'B$'__0| |tptp.'B$'|) $x2)) (as @tptp.tlbool_0 tptp.tlbool) (as @tptp.tlbool_1 tptp.tlbool))) % 137.57/137.86 (define-fun tptp.def_40 (($x1 tptp.tlbool)) tptp.tlbool (ite (= (as @tptp.tlbool_1 tptp.tlbool) $x1) (as @tptp.tlbool_0 tptp.tlbool) (as @tptp.tlbool_1 tptp.tlbool))) % 137.57/137.86 (define-fun |tptp.'uminus$b'| ((BOUND_VARIABLE_6423 tptp.tlbool)) Bool (= (as @tptp.tlbool_0 tptp.tlbool) (ite (= BOUND_VARIABLE_6423 (as @tptp.tlbool_1 tptp.tlbool)) (as @tptp.tlbool_0 tptp.tlbool) (as @tptp.tlbool_1 tptp.tlbool)))) % 137.57/137.86 (define-fun |tptp.'is_empty$'| (($x1 |tptp.'B_set$'|)) Bool (= (as |@_tptp.'B_set$'__0| |tptp.'B_set$'|) $x1)) % 137.57/137.86 (define-fun |tptp.'insert$'| (($x1 |tptp.'B$'|)) |tptp.'B_set_b_set_fun$'| (as |@_tptp.'B_set_b_set_fun$'__1| |tptp.'B_set_b_set_fun$'|)) % 137.57/137.86 (define-fun |tptp.'fun_app$m'| (($x1 |tptp.'B_bool_fun_b_bool_fun_bool_fun_fun$'|) ($x2 |tptp.'B_bool_fun$'|)) |tptp.'B_bool_fun_bool_fun$'| (ite (and (= (as |@_tptp.'B_bool_fun_b_bool_fun_bool_fun_fun$'__0| |tptp.'B_bool_fun_b_bool_fun_bool_fun_fun$'|) $x1) (= (as |@_tptp.'B_bool_fun$'__0| |tptp.'B_bool_fun$'|) $x2)) (as |@_tptp.'B_bool_fun_bool_fun$'__0| |tptp.'B_bool_fun_bool_fun$'|) (ite (and (= (as |@_tptp.'B_bool_fun_b_bool_fun_bool_fun_fun$'__1| |tptp.'B_bool_fun_b_bool_fun_bool_fun_fun$'|) $x1) (= (as |@_tptp.'B_bool_fun$'__1| |tptp.'B_bool_fun$'|) $x2)) (as |@_tptp.'B_bool_fun_bool_fun$'__1| |tptp.'B_bool_fun_bool_fun$'|) (as |@_tptp.'B_bool_fun_bool_fun$'__2| |tptp.'B_bool_fun_bool_fun$'|)))) % 137.57/137.86 (define-fun |tptp.'top$'| () |tptp.'B_set$'| (as |@_tptp.'B_set$'__1| |tptp.'B_set$'|)) % 137.57/137.86 (define-fun tptp.def_37 (($x1 tptp.tlbool) ($x2 tptp.tlbool)) tptp.tlbool (ite (and (= (as @tptp.tlbool_0 tptp.tlbool) $x1) (= (as @tptp.tlbool_0 tptp.tlbool) $x2)) (as @tptp.tlbool_0 tptp.tlbool) (ite (and (= (as @tptp.tlbool_1 tptp.tlbool) $x1) (= (as @tptp.tlbool_0 tptp.tlbool) $x2)) (as @tptp.tlbool_0 tptp.tlbool) (ite (and (= (as @tptp.tlbool_0 tptp.tlbool) $x1) (= (as @tptp.tlbool_1 tptp.tlbool) $x2)) (as @tptp.tlbool_0 tptp.tlbool) (as @tptp.tlbool_1 tptp.tlbool))))) % 137.57/137.86 (define-fun tptp.tltrue () tptp.tlbool (as @tptp.tlbool_0 tptp.tlbool)) % 137.57/137.86 (define-fun tptp.def_19 (($x1 |tptp.'B_bool_fun$'|) ($x2 |tptp.'B$'|)) tptp.tlbool (ite (and (= (as |@_tptp.'B_bool_fun$'__0| |tptp.'B_bool_fun$'|) $x1) (= (as |@_tptp.'B$'__0| |tptp.'B$'|) $x2)) (as @tptp.tlbool_0 tptp.tlbool) (as @tptp.tlbool_1 tptp.tlbool))) % 137.57/137.86 (define-fun |tptp.'inf$'| () |tptp.'B_bool_fun_b_bool_fun_b_bool_fun_fun_fun$'| (as |@_tptp.'B_bool_fun_b_bool_fun_b_bool_fun_fun_fun$'__1| |tptp.'B_bool_fun_b_bool_fun_b_bool_fun_fun_fun$'|)) % 137.57/137.86 (define-fun tptp.def_24 (($x1 |tptp.'B_bool_fun$'|) ($x2 |tptp.'B$'|)) tptp.tlbool (ite (and (= (as |@_tptp.'B_bool_fun$'__0| |tptp.'B_bool_fun$'|) $x1) (= (as |@_tptp.'B$'__0| |tptp.'B$'|) $x2)) (as @tptp.tlbool_0 tptp.tlbool) (as @tptp.tlbool_1 tptp.tlbool))) % 137.57/137.86 (define-fun |tptp.'minus$'| () |tptp.'B_set_b_set_b_set_fun_fun$'| (as |@_tptp.'B_set_b_set_b_set_fun_fun$'__2| |tptp.'B_set_b_set_b_set_fun_fun$'|)) % 137.57/137.86 (define-fun tptp.def_26 (($x1 |tptp.'B_bool_fun$'|) ($x2 |tptp.'B$'|)) tptp.tlbool (ite (and (= (as |@_tptp.'B_bool_fun$'__0| |tptp.'B_bool_fun$'|) $x1) (= (as |@_tptp.'B$'__0| |tptp.'B$'|) $x2)) (as @tptp.tlbool_0 tptp.tlbool) (as @tptp.tlbool_1 tptp.tlbool))) % 137.57/137.86 (define-fun |tptp.'remove$'| (($x1 |tptp.'B$'|)) |tptp.'B_set_b_set_fun$'| (as |@_tptp.'B_set_b_set_fun$'__3| |tptp.'B_set_b_set_fun$'|)) % 137.57/137.86 (define-fun tptp.def_18 () tptp.tlbool (as @tptp.tlbool_1 tptp.tlbool)) % 137.57/137.86 (define-fun |tptp.'semilattice_neutr$a'| ((_arg_1 |tptp.'B_bool_fun_b_bool_fun_b_bool_fun_fun_fun$'|) (_arg_2 |tptp.'B_bool_fun$'|)) Bool true) % 137.57/137.86 (define-fun tptp.def_2 () tptp.tlbool (as @tptp.tlbool_0 tptp.tlbool)) % 137.57/137.86 (define-fun |tptp.'is_singleton$'| ((BOUND_VARIABLE_33183 |tptp.'B_set$'|)) Bool (= (as |@_tptp.'B_set$'__1| |tptp.'B_set$'|) BOUND_VARIABLE_33183)) % 137.57/137.86 (define-fun |tptp.'fun_app$e'| (($x1 |tptp.'Bool_bool_fun$'|) ($x2 tptp.tlbool)) Bool (or (and (= (as |@_tptp.'Bool_bool_fun$'__1| |tptp.'Bool_bool_fun$'|) $x1) (= (as @tptp.tlbool_1 tptp.tlbool) $x2)) (and (= (as |@_tptp.'Bool_bool_fun$'__0| |tptp.'Bool_bool_fun$'|) $x1) (= (as @tptp.tlbool_0 tptp.tlbool) $x2)) (and (= (as |@_tptp.'Bool_bool_fun$'__1| |tptp.'Bool_bool_fun$'|) $x1) (= (as @tptp.tlbool_0 tptp.tlbool) $x2)))) % 137.57/137.86 (define-fun tptp.def_16 (($x1 |tptp.'B_bool_fun$'|) ($x2 |tptp.'B$'|)) tptp.tlbool (ite (and (= (as |@_tptp.'B_bool_fun$'__0| |tptp.'B_bool_fun$'|) $x1) (= (as |@_tptp.'B$'__0| |tptp.'B$'|) $x2)) (as @tptp.tlbool_0 tptp.tlbool) (as @tptp.tlbool_1 tptp.tlbool))) % 137.57/137.86 (define-fun tptp.def_14 (($x1 |tptp.'B_bool_fun$'|) ($x2 |tptp.'B$'|)) tptp.tlbool (ite (and (= (as |@_tptp.'B_bool_fun$'__0| |tptp.'B_bool_fun$'|) $x1) (= (as |@_tptp.'B$'__0| |tptp.'B$'|) $x2)) (as @tptp.tlbool_0 tptp.tlbool) (as @tptp.tlbool_1 tptp.tlbool))) % 137.57/137.86 (define-fun |tptp.'less$'| () |tptp.'B_set_b_set_bool_fun_fun$'| (as |@_tptp.'B_set_b_set_bool_fun_fun$'__0| |tptp.'B_set_b_set_bool_fun_fun$'|)) % 137.57/137.86 (define-fun |tptp.'sup$b'| () |tptp.'B_bool_fun_b_bool_fun_b_bool_fun_fun_fun$'| (as |@_tptp.'B_bool_fun_b_bool_fun_b_bool_fun_fun_fun$'__0| |tptp.'B_bool_fun_b_bool_fun_b_bool_fun_fun_fun$'|)) % 137.57/137.86 (define-fun |tptp.'fun_app$k'| (($x1 |tptp.'B_b_bool_fun_fun$'|) ($x2 |tptp.'B$'|)) |tptp.'B_bool_fun$'| (as |@_tptp.'B_bool_fun$'__0| |tptp.'B_bool_fun$'|)) % 137.57/137.86 (define-fun tptp.def_9 (($x1 |tptp.'B_bool_fun$'|) ($x2 |tptp.'B$'|)) tptp.tlbool (ite (and (= (as |@_tptp.'B_bool_fun$'__0| |tptp.'B_bool_fun$'|) $x1) (= (as |@_tptp.'B$'__0| |tptp.'B$'|) $x2)) (as @tptp.tlbool_0 tptp.tlbool) (as @tptp.tlbool_1 tptp.tlbool))) % 137.57/137.86 (define-fun tptp.def_20 (($x1 |tptp.'B_bool_fun$'|) ($x2 |tptp.'B$'|)) tptp.tlbool (ite (and (= (as |@_tptp.'B_bool_fun$'__0| |tptp.'B_bool_fun$'|) $x1) (= (as |@_tptp.'B$'__0| |tptp.'B$'|) $x2)) (as @tptp.tlbool_0 tptp.tlbool) (as @tptp.tlbool_1 tptp.tlbool))) % 137.57/137.86 (define-fun tptp.def_10 (($x1 |tptp.'B_bool_fun$'|) ($x2 |tptp.'B$'|)) tptp.tlbool (ite (and (= (as |@_tptp.'B_bool_fun$'__0| |tptp.'B_bool_fun$'|) $x1) (= (as |@_tptp.'B$'__0| |tptp.'B$'|) $x2)) (as @tptp.tlbool_0 tptp.tlbool) (as @tptp.tlbool_1 tptp.tlbool))) % 137.57/137.86 (define-fun tptp.def_27 () tptp.tlbool (as @tptp.tlbool_1 tptp.tlbool)) % 137.57/137.86 (define-fun |tptp.'sup$'| () |tptp.'B_set_b_set_b_set_fun_fun$'| (as |@_tptp.'B_set_b_set_b_set_fun_fun$'__0| |tptp.'B_set_b_set_b_set_fun_fun$'|)) % 137.57/137.86 (define-fun tptp.def_34 () tptp.tlbool (as @tptp.tlbool_0 tptp.tlbool)) % 137.57/137.86 (define-fun |tptp.'pairwise$'| (($x1 |tptp.'B_b_bool_fun_fun$'|) ($x2 |tptp.'B_set$'|)) Bool true) % 137.57/137.86 (define-fun |tptp.'uu$'| () |tptp.'B_set_b_bool_fun_fun$'| (as |@_tptp.'B_set_b_bool_fun_fun$'__0| |tptp.'B_set_b_bool_fun_fun$'|)) % 137.57/137.86 (define-fun tptp.def_1 () tptp.tlbool (as @tptp.tlbool_0 tptp.tlbool)) % 137.57/137.86 (define-fun tptp.def_25 (($x1 |tptp.'B_bool_fun$'|) ($x2 |tptp.'B$'|)) tptp.tlbool (ite (and (= (as |@_tptp.'B_bool_fun$'__0| |tptp.'B_bool_fun$'|) $x1) (= (as |@_tptp.'B$'__0| |tptp.'B$'|) $x2)) (as @tptp.tlbool_0 tptp.tlbool) (as @tptp.tlbool_1 tptp.tlbool))) % 137.57/137.86 (define-fun tptp.def_13 (($x1 |tptp.'B_bool_fun$'|) ($x2 |tptp.'B$'|)) tptp.tlbool (ite (and (= (as |@_tptp.'B_bool_fun$'__0| |tptp.'B_bool_fun$'|) $x1) (= (as |@_tptp.'B$'__0| |tptp.'B$'|) $x2)) (as @tptp.tlbool_0 tptp.tlbool) (as @tptp.tlbool_1 tptp.tlbool))) % 137.57/137.86 (define-fun |tptp.'uminus$a'| () |tptp.'B_bool_fun_b_bool_fun_fun$'| (as |@_tptp.'B_bool_fun_b_bool_fun_fun$'__0| |tptp.'B_bool_fun_b_bool_fun_fun$'|)) % 137.57/137.86 (define-fun tptp.def_41 (($x1 |tptp.'B_bool_fun$'|) ($x2 |tptp.'B$'|)) tptp.tlbool (ite (and (= (as |@_tptp.'B_bool_fun$'__0| |tptp.'B_bool_fun$'|) $x1) (= (as |@_tptp.'B$'__0| |tptp.'B$'|) $x2)) (as @tptp.tlbool_0 tptp.tlbool) (as @tptp.tlbool_1 tptp.tlbool))) % 137.57/137.86 (define-fun |tptp.'bot$b'| () |tptp.'B_bool_fun$'| (as |@_tptp.'B_bool_fun$'__1| |tptp.'B_bool_fun$'|)) % 137.57/137.86 (define-fun tptp.def_7 () tptp.tlbool (as @tptp.tlbool_1 tptp.tlbool)) % 137.57/137.86 (define-fun |tptp.'minus$a'| () |tptp.'B_bool_fun_b_bool_fun_b_bool_fun_fun_fun$'| (as |@_tptp.'B_bool_fun_b_bool_fun_b_bool_fun_fun_fun$'__2| |tptp.'B_bool_fun_b_bool_fun_b_bool_fun_fun_fun$'|)) % 137.57/137.86 (define-fun |tptp.'ordering_top$'| ((_arg_1 |tptp.'B_bool_fun_b_bool_fun_bool_fun_fun$'|) (_arg_2 |tptp.'B_bool_fun_b_bool_fun_bool_fun_fun$'|) (_arg_3 |tptp.'B_bool_fun$'|)) Bool true) % 137.57/137.86 (define-fun tptp.def_38 (($x1 tptp.tlbool) ($x2 tptp.tlbool)) tptp.tlbool (ite (and (= (as @tptp.tlbool_1 tptp.tlbool) $x1) (= (as @tptp.tlbool_1 tptp.tlbool) $x2)) (as @tptp.tlbool_0 tptp.tlbool) (ite (and (= (as @tptp.tlbool_1 tptp.tlbool) $x1) (= (as @tptp.tlbool_0 tptp.tlbool) $x2)) (as @tptp.tlbool_0 tptp.tlbool) (ite (and (= (as @tptp.tlbool_0 tptp.tlbool) $x1) (= (as @tptp.tlbool_0 tptp.tlbool) $x2)) (as @tptp.tlbool_0 tptp.tlbool) (as @tptp.tlbool_1 tptp.tlbool))))) % 137.57/137.86 (define-fun tptp.tlfalse () tptp.tlbool (as @tptp.tlbool_1 tptp.tlbool)) % 137.57/137.86 (define-fun |tptp.'inf$a'| () |tptp.'B_set_b_set_b_set_fun_fun$'| (as |@_tptp.'B_set_b_set_b_set_fun_fun$'__1| |tptp.'B_set_b_set_b_set_fun_fun$'|)) % 137.57/137.86 (define-fun tptp.def_31 () tptp.tlbool (as @tptp.tlbool_0 tptp.tlbool)) % 137.57/137.86 (define-fun |tptp.'the_elem$'| (($x1 |tptp.'B_set$'|)) |tptp.'B$'| (as |@_tptp.'B$'__0| |tptp.'B$'|)) % 137.57/137.86 (define-fun tptp.def_28 () tptp.tlbool (as @tptp.tlbool_1 tptp.tlbool)) % 137.57/137.86 (define-fun |tptp.'bot$'| () |tptp.'B_set$'| (as |@_tptp.'B_set$'__0| |tptp.'B_set$'|)) % 137.57/137.86 (define-fun tptp.def_30 () tptp.tlbool (as @tptp.tlbool_0 tptp.tlbool)) % 137.57/137.86 (define-fun |tptp.'b$'| () |tptp.'B$'| (as |@_tptp.'B$'__0| |tptp.'B$'|)) % 137.57/137.86 (define-fun |tptp.'less$a'| () |tptp.'B_bool_fun_b_bool_fun_bool_fun_fun$'| (as |@_tptp.'B_bool_fun_b_bool_fun_bool_fun_fun$'__0| |tptp.'B_bool_fun_b_bool_fun_bool_fun_fun$'|)) % 137.57/137.86 (define-fun |tptp.'less_eq$'| () |tptp.'B_set_b_set_bool_fun_fun$'| (as |@_tptp.'B_set_b_set_bool_fun_fun$'__1| |tptp.'B_set_b_set_bool_fun_fun$'|)) % 137.57/137.86 (define-fun tptp.def_35 () tptp.tlbool (as @tptp.tlbool_1 tptp.tlbool)) % 137.57/137.86 (define-fun |tptp.'ordering_top$a'| (($x1 |tptp.'B_set_b_set_bool_fun_fun$'|) ($x2 |tptp.'B_set_b_set_bool_fun_fun$'|) ($x3 |tptp.'B_set$'|)) Bool (and (= (as |@_tptp.'B_set_b_set_bool_fun_fun$'__1| |tptp.'B_set_b_set_bool_fun_fun$'|) $x1) (= (as |@_tptp.'B_set_b_set_bool_fun_fun$'__0| |tptp.'B_set_b_set_bool_fun_fun$'|) $x2) (= (as |@_tptp.'B_set$'__1| |tptp.'B_set$'|) $x3))) % 137.57/137.86 (define-fun |tptp.'fun_app$'| ((BOUND_VARIABLE_6280 |tptp.'B_bool_fun$'|) (BOUND_VARIABLE_6281 |tptp.'B$'|)) Bool (= (as @tptp.tlbool_0 tptp.tlbool) (ite (and (= BOUND_VARIABLE_6280 (as |@_tptp.'B_bool_fun$'__0| |tptp.'B_bool_fun$'|)) (= BOUND_VARIABLE_6281 (as |@_tptp.'B$'__0| |tptp.'B$'|))) (as @tptp.tlbool_0 tptp.tlbool) (as @tptp.tlbool_1 tptp.tlbool)))) % 137.57/137.86 (define-fun tptp.def_42 (($x1 tptp.tlbool)) tptp.tlbool (ite (= (as @tptp.tlbool_1 tptp.tlbool) $x1) (as @tptp.tlbool_0 tptp.tlbool) (as @tptp.tlbool_1 tptp.tlbool))) % 137.57/137.86 (define-fun |tptp.'fun_app$l'| (($x1 |tptp.'B_bool_fun_bool_fun$'|) ($x2 |tptp.'B_bool_fun$'|)) Bool (or (and (= (as |@_tptp.'B_bool_fun_bool_fun$'__1| |tptp.'B_bool_fun_bool_fun$'|) $x1) (= (as |@_tptp.'B_bool_fun$'__1| |tptp.'B_bool_fun$'|) $x2)) (and (= (as |@_tptp.'B_bool_fun_bool_fun$'__2| |tptp.'B_bool_fun_bool_fun$'|) $x1) (= (as |@_tptp.'B_bool_fun$'__0| |tptp.'B_bool_fun$'|) $x2)) (and (= (as |@_tptp.'B_bool_fun_bool_fun$'__1| |tptp.'B_bool_fun_bool_fun$'|) $x1) (= (as |@_tptp.'B_bool_fun$'__0| |tptp.'B_bool_fun$'|) $x2)))) % 137.57/137.86 (define-fun tptp.def_23 (($x1 |tptp.'B_bool_fun$'|) ($x2 |tptp.'B$'|)) tptp.tlbool (ite (and (= (as |@_tptp.'B_bool_fun$'__0| |tptp.'B_bool_fun$'|) $x1) (= (as |@_tptp.'B$'__0| |tptp.'B$'|) $x2)) (as @tptp.tlbool_0 tptp.tlbool) (as @tptp.tlbool_1 tptp.tlbool))) % 137.57/137.86 (define-fun |tptp.'fun_app$h'| (($x1 |tptp.'B_bool_fun_b_bool_fun_b_bool_fun_fun_fun$'|) ($x2 |tptp.'B_bool_fun$'|)) |tptp.'B_bool_fun_b_bool_fun_fun$'| (ite (and (= (as |@_tptp.'B_bool_fun_b_bool_fun_b_bool_fun_fun_fun$'__2| |tptp.'B_bool_fun_b_bool_fun_b_bool_fun_fun_fun$'|) $x1) (= (as |@_tptp.'B_bool_fun$'__0| |tptp.'B_bool_fun$'|) $x2)) (as |@_tptp.'B_bool_fun_b_bool_fun_fun$'__0| |tptp.'B_bool_fun_b_bool_fun_fun$'|) (ite (and (= (as |@_tptp.'B_bool_fun_b_bool_fun_b_bool_fun_fun_fun$'__2| |tptp.'B_bool_fun_b_bool_fun_b_bool_fun_fun_fun$'|) $x1) (= (as |@_tptp.'B_bool_fun$'__1| |tptp.'B_bool_fun$'|) $x2)) (as |@_tptp.'B_bool_fun_b_bool_fun_fun$'__1| |tptp.'B_bool_fun_b_bool_fun_fun$'|) (ite (and (= (as |@_tptp.'B_bool_fun_b_bool_fun_b_bool_fun_fun_fun$'__1| |tptp.'B_bool_fun_b_bool_fun_b_bool_fun_fun_fun$'|) $x1) (= (as |@_tptp.'B_bool_fun$'__1| |tptp.'B_bool_fun$'|) $x2)) (as |@_tptp.'B_bool_fun_b_bool_fun_fun$'__1| |tptp.'B_bool_fun_b_bool_fun_fun$'|) (ite (and (= (as |@_tptp.'B_bool_fun_b_bool_fun_b_bool_fun_fun_fun$'__1| |tptp.'B_bool_fun_b_bool_fun_b_bool_fun_fun_fun$'|) $x1) (= (as |@_tptp.'B_bool_fun$'__0| |tptp.'B_bool_fun$'|) $x2)) (as |@_tptp.'B_bool_fun_b_bool_fun_fun$'__2| |tptp.'B_bool_fun_b_bool_fun_fun$'|) (ite (and (= (as |@_tptp.'B_bool_fun_b_bool_fun_b_bool_fun_fun_fun$'__0| |tptp.'B_bool_fun_b_bool_fun_b_bool_fun_fun_fun$'|) $x1) (= (as |@_tptp.'B_bool_fun$'__1| |tptp.'B_bool_fun$'|) $x2)) (as |@_tptp.'B_bool_fun_b_bool_fun_fun$'__2| |tptp.'B_bool_fun_b_bool_fun_fun$'|) (as |@_tptp.'B_bool_fun_b_bool_fun_fun$'__3| |tptp.'B_bool_fun_b_bool_fun_fun$'|))))))) % 137.57/137.86 (define-fun |tptp.'minus$b'| (($x1 tptp.tlbool) ($x2 tptp.tlbool)) Bool (and (= (as @tptp.tlbool_0 tptp.tlbool) $x1) (= (as @tptp.tlbool_1 tptp.tlbool) $x2))) % 137.57/137.86 (define-fun |tptp.'sup$a'| () |tptp.'Bool_bool_bool_fun_fun$'| (as |@_tptp.'Bool_bool_bool_fun_fun$'__0| |tptp.'Bool_bool_bool_fun_fun$'|)) % 137.57/137.86 (define-fun |tptp.'ordering_top_axioms$'| (($x1 |tptp.'B_set_b_set_bool_fun_fun$'|) ($x2 |tptp.'B_set$'|)) Bool true) % 137.57/137.86 (define-fun |tptp.'fun_app$g'| (($x1 |tptp.'B_bool_fun_b_bool_fun_fun$'|) ($x2 |tptp.'B_bool_fun$'|)) |tptp.'B_bool_fun$'| (ite (and (= (as |@_tptp.'B_bool_fun_b_bool_fun_fun$'__0| |tptp.'B_bool_fun_b_bool_fun_fun$'|) $x1) (= (as |@_tptp.'B_bool_fun$'__1| |tptp.'B_bool_fun$'|) $x2)) (as |@_tptp.'B_bool_fun$'__0| |tptp.'B_bool_fun$'|) (ite (and (= (as |@_tptp.'B_bool_fun_b_bool_fun_fun$'__2| |tptp.'B_bool_fun_b_bool_fun_fun$'|) $x1) (= (as |@_tptp.'B_bool_fun$'__0| |tptp.'B_bool_fun$'|) $x2)) (as |@_tptp.'B_bool_fun$'__0| |tptp.'B_bool_fun$'|) (ite (and (= (as |@_tptp.'B_bool_fun_b_bool_fun_fun$'__3| |tptp.'B_bool_fun_b_bool_fun_fun$'|) $x1) (= (as |@_tptp.'B_bool_fun$'__0| |tptp.'B_bool_fun$'|) $x2)) (as |@_tptp.'B_bool_fun$'__0| |tptp.'B_bool_fun$'|) (ite (and (= (as |@_tptp.'B_bool_fun_b_bool_fun_fun$'__3| |tptp.'B_bool_fun_b_bool_fun_fun$'|) $x1) (= (as |@_tptp.'B_bool_fun$'__1| |tptp.'B_bool_fun$'|) $x2)) (as |@_tptp.'B_bool_fun$'__0| |tptp.'B_bool_fun$'|) (as |@_tptp.'B_bool_fun$'__1| |tptp.'B_bool_fun$'|)))))) % 137.57/137.86 (define-fun |tptp.'fun_app$d'| (($x1 |tptp.'B_bool_fun_b_set_fun$'|) ($x2 |tptp.'B_bool_fun$'|)) |tptp.'B_set$'| (ite (and (= (as |@_tptp.'B_bool_fun_b_set_fun$'__0| |tptp.'B_bool_fun_b_set_fun$'|) $x1) (= (as |@_tptp.'B_bool_fun$'__1| |tptp.'B_bool_fun$'|) $x2)) (as |@_tptp.'B_set$'__0| |tptp.'B_set$'|) (as |@_tptp.'B_set$'__1| |tptp.'B_set$'|))) % 137.57/137.86 (define-fun tptp.def_11 (($x1 |tptp.'B_bool_fun$'|) ($x2 |tptp.'B$'|)) tptp.tlbool (ite (and (= (as |@_tptp.'B_bool_fun$'__0| |tptp.'B_bool_fun$'|) $x1) (= (as |@_tptp.'B$'__0| |tptp.'B$'|) $x2)) (as @tptp.tlbool_0 tptp.tlbool) (as @tptp.tlbool_1 tptp.tlbool))) % 137.57/137.86 ) % 137.57/137.86 % SZS output end Model % 137.57/137.86 % cvc5 exiting %------------------------------------------------------------------------------