%------------------------------------------------------------------------------ % File : cvc5---1.3.4 % Problem : ITP010^1 : TPTP v9.2.1. Bugfixed v7.5.0. % Transfm : none % Format : tptp:raw % Command : /export/starexec/sandbox2/solver/bin/do_cvc5 /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM % Computer : n025.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:24:29 AM UTC 2026 % Result : Theorem 0.37s 0.57s % Output : Proof 0.37s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : ITP010^1 : TPTP v9.2.1. Bugfixed v7.5.0. % 0.12/0.13 % Command : /export/starexec/sandbox2/solver/bin/do_cvc5 /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM % 0.18/0.34 % Computer : n025.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 03:47:01 EDT 2026 % 0.18/0.34 % CPUTime : % 0.31/0.50 %----Proving TH0 % 0.37/0.57 --- Run --mbqi --mbqi-enum --mbqi-enum-choice-grammar --mbqi-enum-global-syms-grammar --sygus-grammar-ho-partial --no-cegqi --no-sygus-inst at 90s... % 0.37/0.57 % SZS status Theorem % 0.37/0.57 % SZS output start Proof % 0.37/0.57 ( % 0.37/0.57 (declare-sort tptp.u 0) % 0.37/0.57 (declare-sort tptp.du 0) % 0.37/0.57 (declare-sort tptp.d 0) % 0.37/0.57 (declare-const tptp.c_2Ecardinal_2Ecardleq_2E2 (-> tptp.du tptp.du tptp.u)) % 0.37/0.57 (declare-const tptp.c_2Ecardinal_2Ecardleq_2E0 tptp.u) % 0.37/0.57 (declare-const tptp.i_mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29_29 (-> (-> Bool Bool Bool) tptp.u)) % 0.37/0.57 (declare-const tptp.j_mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29_29 (-> tptp.du Bool Bool Bool)) % 0.37/0.57 (declare-const tptp.c_2Emin_2E_3D_2E0 tptp.u) % 0.37/0.57 (declare-const tptp.i_mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29 (-> (-> Bool Bool) tptp.u)) % 0.37/0.57 (declare-const tptp.j_mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29 (-> tptp.du Bool Bool)) % 0.37/0.57 (declare-const tptp.i_mono_2Etyop_2Emin_2Ebool (-> Bool tptp.u)) % 0.37/0.57 (declare-const tptp.c_2Ebool_2E_3F_2E1 (-> tptp.du tptp.u)) % 0.37/0.57 (declare-const tptp.c_2Ebool_2E_21_2E1 (-> tptp.du tptp.u)) % 0.37/0.57 (declare-const tptp.tyop_2Emin_2Efun (-> tptp.d tptp.d tptp.d)) % 0.37/0.57 (declare-const tptp.s (-> tptp.d tptp.u tptp.du)) % 0.37/0.57 (declare-const tptp.mono_2Ec_2Ebool_2EF Bool) % 0.37/0.57 (declare-const tptp.combin_k_2E0 tptp.u) % 0.37/0.57 (declare-const tptp.mono_2Ec_2Ebool_2ET Bool) % 0.37/0.57 (declare-const tptp.combin_s_2E0 tptp.u) % 0.37/0.57 (declare-const tptp.app_2E2 (-> tptp.du tptp.du tptp.u)) % 0.37/0.57 (declare-const tptp.mono_2Ec_2Ebool_2E_2F_5C (-> Bool Bool Bool)) % 0.37/0.57 (declare-const tptp.c_2Ebool_2E_3F_2E0 tptp.u) % 0.37/0.57 (declare-const tptp.j_mono_2Etyop_2Emin_2Ebool (-> tptp.du Bool)) % 0.37/0.57 (declare-const tptp.c_2Ebool_2E_21_2E0 tptp.u) % 0.37/0.57 (declare-const tptp.mono_2Ec_2Ebool_2E_5C_2F (-> Bool Bool Bool)) % 0.37/0.57 (declare-const tptp.tyop_2Emin_2Ebool tptp.d) % 0.37/0.57 (declare-const tptp.mono_2Ec_2Ebool_2E_7E (-> Bool Bool)) % 0.37/0.57 (declare-const tptp.combin_i_2E0 tptp.u) % 0.37/0.57 (declare-const tptp.mono_2Ec_2Emin_2E_3D_3D_3E (-> Bool Bool Bool)) % 0.37/0.57 (declare-const tptp.c_2Emin_2E_3D_2E2 (-> tptp.du tptp.du tptp.u)) % 0.37/0.57 (define @t1 () (@var "V1g_2E0" tptp.u)) % 0.37/0.57 (define @t2 () (@var "A_27b" tptp.d)) % 0.37/0.57 (define @t3 () (@var "A_27a" tptp.d)) % 0.37/0.57 (define @t4 () (_ tptp.tyop_2Emin_2Efun @t3)) % 0.37/0.57 (define @t5 () (_ @t4 @t2)) % 0.37/0.57 (define @t6 () (_ tptp.s @t5)) % 0.37/0.57 (define @t7 () (_ @t6 @t1)) % 0.37/0.57 (define @t8 () (@var "V0f_2E0" tptp.u)) % 0.37/0.57 (define @t9 () (_ @t6 @t8)) % 0.37/0.57 (define @t10 () (@var "V2x_2E0" tptp.u)) % 0.37/0.57 (define @t11 () (_ tptp.s @t3)) % 0.37/0.57 (define @t12 () (_ @t11 @t10)) % 0.37/0.57 (define @t13 () (_ tptp.s @t2)) % 0.37/0.57 (define @t14 () (_ @t13 (_ (_ tptp.app_2E2 @t7) @t12))) % 0.37/0.57 (define @t15 () (@var "V0x_2E0" tptp.u)) % 0.37/0.57 (define @t16 () (_ @t11 @t15)) % 0.37/0.57 (define @t17 () (@list @t3 @t15)) % 0.37/0.57 (define @t18 () (@var "V1y_2E0" tptp.u)) % 0.37/0.57 (define @t19 () (_ tptp.tyop_2Emin_2Efun @t2)) % 0.37/0.57 (define @t20 () (_ @t19 @t3)) % 0.37/0.57 (define @t21 () (@var "A_27c" tptp.d)) % 0.37/0.57 (define @t22 () (_ @t19 @t21)) % 0.37/0.57 (define @t23 () (_ @t4 @t22)) % 0.37/0.57 (define @t24 () (_ (_ tptp.s @t23) @t8)) % 0.37/0.57 (define @t25 () (_ tptp.s @t21)) % 0.37/0.57 (define @t26 () (_ @t4 @t21)) % 0.37/0.57 (define @t27 () (_ (_ tptp.tyop_2Emin_2Efun @t5) @t26)) % 0.37/0.57 (define @t28 () (@var "V1" Bool)) % 0.37/0.57 (define @t29 () (@var "V0" Bool)) % 0.37/0.57 (define @t30 () (@list @t29 @t28)) % 0.37/0.57 (define @t31 () (@list @t29)) % 0.37/0.57 (define @t32 () (@var "V1_2E0" tptp.u)) % 0.37/0.57 (define @t33 () (_ @t11 @t32)) % 0.37/0.57 (define @t34 () (@var "V0_2E0" tptp.u)) % 0.37/0.57 (define @t35 () (_ @t11 @t34)) % 0.37/0.57 (define @t36 () (_ tptp.s tptp.tyop_2Emin_2Ebool)) % 0.37/0.57 (define @t37 () (@var "V1x_2E0" tptp.u)) % 0.37/0.57 (define @t38 () (_ @t4 tptp.tyop_2Emin_2Ebool)) % 0.37/0.57 (define @t39 () (_ tptp.s @t38)) % 0.37/0.57 (define @t40 () (_ @t39 @t8)) % 0.37/0.57 (define @t41 () (_ tptp.j_mono_2Etyop_2Emin_2Ebool (_ @t36 (_ (_ tptp.app_2E2 @t40) (_ @t11 @t37))))) % 0.37/0.57 (define @t42 () (@list @t37)) % 0.37/0.57 (define @t43 () (@list @t3 @t8)) % 0.37/0.57 (define @t44 () (_ @t36 @t34)) % 0.37/0.57 (define @t45 () (@list @t34)) % 0.37/0.57 (define @t46 () (_ tptp.tyop_2Emin_2Efun tptp.tyop_2Emin_2Ebool)) % 0.37/0.57 (define @t47 () (_ @t46 tptp.tyop_2Emin_2Ebool)) % 0.37/0.57 (define @t48 () (_ tptp.s @t47)) % 0.37/0.57 (define @t49 () (_ @t48 @t34)) % 0.37/0.57 (define @t50 () (_ tptp.s (_ @t46 @t47))) % 0.37/0.57 (define @t51 () (_ @t50 @t34)) % 0.37/0.57 (define @t52 () (@var "V0" (-> Bool Bool))) % 0.37/0.57 (define @t53 () (_ @t48 (_ tptp.i_mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29 @t52))) % 0.37/0.57 (define @t54 () (@var "V0" (-> Bool Bool Bool))) % 0.37/0.57 (define @t55 () (_ @t50 (_ tptp.i_mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29_29 @t54))) % 0.37/0.57 (define @t56 () (@var "X0_2E0" tptp.u)) % 0.37/0.57 (define @t57 () (_ @t39 @t56)) % 0.37/0.57 (define @t58 () (_ tptp.tyop_2Emin_2Efun @t38)) % 0.37/0.57 (define @t59 () (_ @t58 tptp.tyop_2Emin_2Ebool)) % 0.37/0.57 (define @t60 () (_ tptp.s @t59)) % 0.37/0.57 (define @t61 () (@list @t3 @t56)) % 0.37/0.57 (define @t62 () (@var "X1_2E0" tptp.u)) % 0.37/0.57 (define @t63 () (_ @t11 @t62)) % 0.37/0.57 (define @t64 () (_ @t11 @t56)) % 0.37/0.57 (define @t65 () (_ @t19 tptp.tyop_2Emin_2Ebool)) % 0.37/0.57 (define @t66 () (_ tptp.s @t65)) % 0.37/0.57 (define @t67 () (_ @t66 @t62)) % 0.37/0.57 (define @t68 () (_ tptp.tyop_2Emin_2Efun @t65)) % 0.37/0.57 (define @t69 () (_ @t68 tptp.tyop_2Emin_2Ebool)) % 0.37/0.57 (define @t70 () (@list @t3 @t2 @t56 @t62)) % 0.37/0.57 (define @t71 () (_ @t39 @t62)) % 0.37/0.57 (define @t72 () (_ @t66 @t56)) % 0.37/0.57 (define @t73 () (_ @t36 (_ tptp.i_mono_2Etyop_2Emin_2Ebool @t28))) % 0.37/0.57 (define @t74 () (_ @t52 @t28)) % 0.37/0.57 (define @t75 () (@list @t52 @t28)) % 0.37/0.57 (define @t76 () (_ @t54 @t28)) % 0.37/0.57 (define @t77 () (@list @t54 @t28)) % 0.37/0.57 (define @t78 () (@var "V0t" Bool)) % 0.37/0.57 (define @t79 () (=> tptp.mono_2Ec_2Ebool_2EF @t78)) % 0.37/0.57 (define @t80 () (@list @t78)) % 0.37/0.57 (define @t81 () (not @t78)) % 0.37/0.57 (define @t82 () (forall @t80 (= (not @t81) @t78))) % 0.37/0.57 (define @t83 () (@var "V0s_2E0" tptp.u)) % 0.37/0.57 (define @t84 () (_ @t39 @t83)) % 0.37/0.57 (define @t85 () (@var "V1t_2E0" tptp.u)) % 0.37/0.57 (define @t86 () (_ @t66 @t85)) % 0.37/0.57 (define @t87 () (_ tptp.j_mono_2Etyop_2Emin_2Ebool (_ @t36 (_ (_ tptp.c_2Ecardinal_2Ecardleq_2E2 @t84) @t86)))) % 0.37/0.57 (define @t88 () (@list @t3 @t2 @t83 @t85)) % 0.37/0.57 (define @t89 () (@var "V0A" Bool)) % 0.37/0.57 (define @t90 () (=> (not @t89) tptp.mono_2Ec_2Ebool_2EF)) % 0.37/0.57 (define @t91 () (@list @t89)) % 0.37/0.57 (define @t92 () (@var "V0B" Bool)) % 0.37/0.57 (define @t93 () (=> (not @t92) tptp.mono_2Ec_2Ebool_2EF)) % 0.37/0.57 (define @t94 () (@var "V1A" Bool)) % 0.37/0.57 (define @t95 () (@list @t92 @t94)) % 0.37/0.57 (define @t96 () (@var "V2p" Bool)) % 0.37/0.57 (define @t97 () (not @t96)) % 0.37/0.57 (define @t98 () (@var "V1q" Bool)) % 0.37/0.57 (define @t99 () (not @t98)) % 0.37/0.57 (define @t100 () (@var "V0r" Bool)) % 0.37/0.57 (define @t101 () (not @t100)) % 0.37/0.57 (define @t102 () (@var "V1p" Bool)) % 0.37/0.57 (define @t103 () (@var "V0q" Bool)) % 0.37/0.57 (define @t104 () (not @t103)) % 0.37/0.57 (define @t105 () (not @t87)) % 0.37/0.57 (define @t106 () (forall @t88 (= @t105 @t105))) % 0.37/0.57 (define @t107 () (not @t106)) % 0.37/0.57 (assume @p1 (forall (@list @t3 @t2 @t8 @t1) (=> (forall (@list @t10) (= (_ @t13 (_ (_ tptp.app_2E2 @t9) @t12)) @t14)) (= @t9 @t7)))) % 0.37/0.57 (assume @p2 (forall @t17 (= (_ @t11 (_ (_ tptp.app_2E2 (_ (_ tptp.s (_ @t4 @t3)) tptp.combin_i_2E0)) @t16)) @t16))) % 0.37/0.57 (assume @p3 (forall (@list @t3 @t2 @t15 @t18) (= (_ @t11 (_ (_ tptp.app_2E2 (_ (_ tptp.s @t20) (_ (_ tptp.app_2E2 (_ (_ tptp.s (_ @t4 @t20)) tptp.combin_k_2E0)) @t16))) (_ @t13 @t18))) @t16))) % 0.37/0.57 (assume @p4 (forall (@list @t3 @t2 @t21 @t8 @t1 @t10) (= (_ @t25 (_ (_ tptp.app_2E2 (_ (_ tptp.s @t26) (_ (_ tptp.app_2E2 (_ (_ tptp.s @t27) (_ (_ tptp.app_2E2 (_ (_ tptp.s (_ (_ tptp.tyop_2Emin_2Efun @t23) @t27)) tptp.combin_s_2E0)) @t24))) @t7))) @t12)) (_ @t25 (_ (_ tptp.app_2E2 (_ (_ tptp.s @t22) (_ (_ tptp.app_2E2 @t24) @t12))) @t14))))) % 0.37/0.57 (assume @p5 (forall @t30 (= (_ (_ tptp.mono_2Ec_2Ebool_2E_2F_5C @t29) @t28) (and @t29 @t28)))) % 0.37/0.57 (assume @p6 (forall @t30 (= (_ (_ tptp.mono_2Ec_2Ebool_2E_5C_2F @t29) @t28) (or @t29 @t28)))) % 0.37/0.57 (assume @p7 (forall @t31 (= (_ tptp.mono_2Ec_2Ebool_2E_7E @t29) (not @t29)))) % 0.37/0.57 (assume @p8 (forall @t30 (= (_ (_ tptp.mono_2Ec_2Emin_2E_3D_3D_3E @t29) @t28) (=> @t29 @t28)))) % 0.37/0.57 (assume @p9 (forall (@list @t3 @t34 @t32) (= (_ tptp.j_mono_2Etyop_2Emin_2Ebool (_ @t36 (_ (_ tptp.c_2Emin_2E_3D_2E2 @t35) @t33))) (= @t35 @t33)))) % 0.37/0.57 (assume @p10 (forall @t43 (= (_ tptp.j_mono_2Etyop_2Emin_2Ebool (_ @t36 (_ tptp.c_2Ebool_2E_21_2E1 @t40))) (forall @t42 @t41)))) % 0.37/0.57 (assume @p11 (forall @t43 (= (_ tptp.j_mono_2Etyop_2Emin_2Ebool (_ @t36 (_ tptp.c_2Ebool_2E_3F_2E1 @t40))) (exists @t42 @t41)))) % 0.37/0.57 (assume @p12 (forall @t45 (= (_ @t36 (_ tptp.i_mono_2Etyop_2Emin_2Ebool (_ tptp.j_mono_2Etyop_2Emin_2Ebool @t44))) @t44))) % 0.37/0.57 (assume @p13 (forall @t45 (= (_ @t48 (_ tptp.i_mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29 (_ tptp.j_mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29 @t49))) @t49))) % 0.37/0.57 (assume @p14 (forall @t45 (= (_ @t50 (_ tptp.i_mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29_29 (_ tptp.j_mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29_29 @t51))) @t51))) % 0.37/0.57 (assume @p15 (forall @t31 (= (_ tptp.j_mono_2Etyop_2Emin_2Ebool (_ @t36 (_ tptp.i_mono_2Etyop_2Emin_2Ebool @t29))) @t29))) % 0.37/0.57 (assume @p16 (forall (@list @t52) (= (_ tptp.j_mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29 @t53) @t52))) % 0.37/0.57 (assume @p17 (forall (@list @t54) (= (_ tptp.j_mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29_29 @t55) @t54))) % 0.37/0.57 (assume @p18 (forall @t61 (= (_ tptp.j_mono_2Etyop_2Emin_2Ebool (_ @t36 (_ tptp.c_2Ebool_2E_21_2E1 @t57))) (_ tptp.j_mono_2Etyop_2Emin_2Ebool (_ @t36 (_ (_ tptp.app_2E2 (_ @t60 tptp.c_2Ebool_2E_21_2E0)) @t57)))))) % 0.37/0.57 (assume @p19 (forall (@list @t3 @t56 @t62) (= (= @t64 @t63) (_ tptp.j_mono_2Etyop_2Emin_2Ebool (_ @t36 (_ (_ tptp.app_2E2 (_ @t39 (_ (_ tptp.app_2E2 (_ (_ tptp.s (_ @t4 @t38)) tptp.c_2Emin_2E_3D_2E0)) @t64))) @t63)))))) % 0.37/0.57 (assume @p20 (forall @t61 (= (_ tptp.j_mono_2Etyop_2Emin_2Ebool (_ @t36 (_ tptp.c_2Ebool_2E_3F_2E1 @t57))) (_ tptp.j_mono_2Etyop_2Emin_2Ebool (_ @t36 (_ (_ tptp.app_2E2 (_ @t60 tptp.c_2Ebool_2E_3F_2E0)) @t57)))))) % 0.37/0.57 (assume @p21 (forall @t70 (= (_ tptp.j_mono_2Etyop_2Emin_2Ebool (_ @t36 (_ (_ tptp.c_2Ecardinal_2Ecardleq_2E2 @t57) @t67))) (_ tptp.j_mono_2Etyop_2Emin_2Ebool (_ @t36 (_ (_ tptp.app_2E2 (_ (_ tptp.s @t69) (_ (_ tptp.app_2E2 (_ (_ tptp.s (_ @t58 @t69)) tptp.c_2Ecardinal_2Ecardleq_2E0)) @t57))) @t67)))))) % 0.37/0.57 (assume @p22 (forall @t70 (= (_ tptp.j_mono_2Etyop_2Emin_2Ebool (_ @t36 (_ (_ tptp.c_2Ecardinal_2Ecardleq_2E2 @t72) @t71))) (_ tptp.j_mono_2Etyop_2Emin_2Ebool (_ @t36 (_ (_ tptp.app_2E2 (_ @t60 (_ (_ tptp.app_2E2 (_ (_ tptp.s (_ @t68 @t59)) tptp.c_2Ecardinal_2Ecardleq_2E0)) @t72))) @t71)))))) % 0.37/0.57 (assume @p23 (forall @t75 (= (_ @t36 (_ tptp.i_mono_2Etyop_2Emin_2Ebool @t74)) (_ @t36 (_ (_ tptp.app_2E2 @t53) @t73))))) % 0.37/0.57 (assume @p24 (forall @t77 (= (_ @t48 (_ tptp.i_mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29 @t76)) (_ @t48 (_ (_ tptp.app_2E2 @t55) @t73))))) % 0.37/0.57 (assume @p25 (forall @t75 (= @t74 @t74))) % 0.37/0.57 (assume @p26 (forall @t77 (= @t76 @t76))) % 0.37/0.57 (assume @p27 tptp.mono_2Ec_2Ebool_2ET) % 0.37/0.57 (assume @p28 (forall @t80 @t79)) % 0.37/0.57 (assume @p29 (forall (@list @t3 @t78) (= (forall @t42 @t78) @t78))) % 0.37/0.57 (assume @p30 (forall @t80 (and (= (=> tptp.mono_2Ec_2Ebool_2ET @t78) @t78) (= (=> @t78 tptp.mono_2Ec_2Ebool_2ET) tptp.mono_2Ec_2Ebool_2ET) (= @t79 tptp.mono_2Ec_2Ebool_2ET) (= (=> @t78 @t78) tptp.mono_2Ec_2Ebool_2ET) (= (=> @t78 tptp.mono_2Ec_2Ebool_2EF) @t81)))) % 0.37/0.57 (assume @p31 (and @t82 (= (not tptp.mono_2Ec_2Ebool_2ET) tptp.mono_2Ec_2Ebool_2EF) (= (not tptp.mono_2Ec_2Ebool_2EF) tptp.mono_2Ec_2Ebool_2ET))) % 0.37/0.57 (assume @p32 (forall @t17 (= (= @t16 @t16) tptp.mono_2Ec_2Ebool_2ET))) % 0.37/0.57 (assume @p33 (forall @t80 (and (= (= tptp.mono_2Ec_2Ebool_2ET @t78) @t78) (= (= @t78 tptp.mono_2Ec_2Ebool_2ET) @t78) (= (= tptp.mono_2Ec_2Ebool_2EF @t78) @t81) (= (= @t78 tptp.mono_2Ec_2Ebool_2EF) @t81)))) % 0.37/0.57 (assume @p34 (forall @t88 (or @t87 (_ tptp.j_mono_2Etyop_2Emin_2Ebool (_ @t36 (_ (_ tptp.c_2Ecardinal_2Ecardleq_2E2 @t86) @t84)))))) % 0.37/0.57 (assume @p35 @t82) % 0.37/0.57 (assume @p36 (forall @t91 (=> @t89 @t90))) % 0.37/0.57 (assume @p37 (forall @t95 (= (=> (not (or @t94 @t92)) tptp.mono_2Ec_2Ebool_2EF) (=> (=> @t94 tptp.mono_2Ec_2Ebool_2EF) @t93)))) % 0.37/0.57 (assume @p38 (forall @t95 (= (=> (not (or (not @t94) @t92)) tptp.mono_2Ec_2Ebool_2EF) (=> @t94 @t93)))) % 0.37/0.57 (assume @p39 (forall @t91 (=> @t90 (=> (=> @t89 tptp.mono_2Ec_2Ebool_2EF) tptp.mono_2Ec_2Ebool_2EF)))) % 0.37/0.57 (assume @p40 (forall (@list @t100 @t98 @t96) (= (= @t96 (= @t98 @t100)) (and (or @t96 @t98 @t100) (or @t96 @t101 @t99) (or @t98 @t101 @t97) (or @t100 @t99 @t97))))) % 0.37/0.57 (assume @p41 (forall (@list @t103 @t102) (= (= @t102 @t104) (and (or @t102 @t103) (or @t104 (not @t102)))))) % 0.37/0.57 (assume @p42 @t107) % 0.37/0.58 (assume @p43 true) % 0.37/0.58 (step @p44 :rule evaluate :args ((not true))) % 0.37/0.58 (step @p45 :rule quant-unused-vars :args ((= (forall @t88 true) true))) % 0.37/0.58 (step @p46 :rule eq-refl :args (@t105)) % 0.37/0.58 (step @p47 :rule cong :premises (@p46) :args (@t106)) % 0.37/0.58 (step @p48 :rule trans :premises (@p47 @p45)) % 0.37/0.58 (step @p49 :rule cong :premises (@p48) :args (@t107)) % 0.37/0.58 (step @p50 :rule trans :premises (@p49 @p44)) % 0.37/0.58 (step @p51 false :rule eq_resolve :premises (@p42 @p50)) % 0.37/0.58 ) % 0.37/0.58 % SZS output end Proof % 0.37/0.58 % cvc5 exiting %------------------------------------------------------------------------------