%------------------------------------------------------------------------------ % File : cvc5---1.3.4 % Problem : ITP009_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 : n028.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:28 AM UTC 2026 % Result : Theorem 128.96s 129.85s % Output : Proof 128.96s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.10 % Problem : ITP009_1 : TPTP v9.2.1. Bugfixed v7.5.0. % 0.00/0.11 % Command : /export/starexec/sandbox2/solver/bin/do_cvc5 /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM % 0.13/0.32 % Computer : n028.cluster.edu % 0.13/0.32 % Model : x86_64 x86_64 % 0.13/0.32 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.32 % Memory : 8042.1875MB % 0.13/0.32 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.32 % CPULimit : 300 % 0.13/0.32 % WCLimit : 300 % 0.13/0.32 % DateTime : Tue Jun 2 03:45:50 EDT 2026 % 0.13/0.32 % CPUTime : % 0.28/0.50 %----Proving TF0_NAR, FOF, or CNF % 128.96/129.85 --- Run --decision=internal --simplification=none --no-inst-no-entail --no-cbqi --full-saturate-quant at 15... % 128.96/129.85 --- Run --no-e-matching --full-saturate-quant at 6... % 128.96/129.85 --- Run --no-e-matching --enum-inst-sum --full-saturate-quant at 6... % 128.96/129.85 --- Run --finite-model-find --uf-ss=no-minimal at 6... % 128.96/129.85 --- Run --multi-trigger-when-single --full-saturate-quant at 30... % 128.96/129.85 --- Run --trigger-sel=max --full-saturate-quant at 15... % 128.96/129.85 --- Run --multi-trigger-when-single --multi-trigger-priority --full-saturate-quant at 33... % 128.96/129.85 --- Run --multi-trigger-cache --full-saturate-quant at 15... % 128.96/129.85 --- Run --prenex-quant=none --full-saturate-quant at 30... % 128.96/129.85 % SZS status Theorem % 128.96/129.85 % SZS output start Proof % 128.96/129.85 ( % 128.96/129.85 (declare-sort tptp.mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29_29 0) % 128.96/129.85 (declare-sort tptp.mono_2Etyop_2Emin_2Ebool 0) % 128.96/129.85 (declare-sort tptp.mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29 0) % 128.96/129.85 (declare-sort tptp.d 0) % 128.96/129.85 (declare-sort tptp.u 0) % 128.96/129.85 (declare-sort tptp.du 0) % 128.96/129.85 (declare-const tptp.mono_2Ec_2Ebool_2E_7E_2E0 tptp.mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29) % 128.96/129.85 (declare-const tptp.c_2Equotient_2Erespects_2E2 (-> tptp.du tptp.du tptp.u)) % 128.96/129.85 (declare-const tptp.c_2Equotient_2Erespects_2E0 tptp.u) % 128.96/129.85 (declare-const tptp.mono_2Ec_2Ebool_2E_5C_2F_2E0 tptp.mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29_29) % 128.96/129.85 (declare-const tptp.c_2Ecombin_2EW_2E2 (-> tptp.du tptp.du tptp.u)) % 128.96/129.85 (declare-const tptp.c_2Ecombin_2EW_2E0 tptp.u) % 128.96/129.85 (declare-const tptp.c_2Equotient_2EQUOTIENT_2E3 (-> tptp.du tptp.du tptp.du tptp.u)) % 128.96/129.85 (declare-const tptp.c_2Equotient_2EQUOTIENT_2E0 tptp.u) % 128.96/129.85 (declare-const tptp.c_2Ebool_2E_3F_2E0 tptp.u) % 128.96/129.85 (declare-const tptp.mono_2Ec_2Emin_2E_3D_3D_3E_2E0 tptp.mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29_29) % 128.96/129.85 (declare-const tptp.c_2Equotient_2E_3D_3D_3D_3E_2E4 (-> tptp.du tptp.du tptp.du tptp.du tptp.u)) % 128.96/129.85 (declare-const tptp.c_2Equotient_2E_3D_3D_3D_3E_2E2 (-> tptp.du tptp.du tptp.u)) % 128.96/129.85 (declare-const tptp.c_2Equotient_2E_3D_3D_3D_3E_2E0 tptp.u) % 128.96/129.85 (declare-const tptp.c_2Emin_2E_3D_2E0 tptp.u) % 128.96/129.85 (declare-const tptp.mono_2Eapp_2E2_2Emono_2Etyop_2Emin_2Ebool_20mono_2Etyop_2Emin_2Ebool (-> tptp.mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29 tptp.mono_2Etyop_2Emin_2Ebool tptp.mono_2Etyop_2Emin_2Ebool)) % 128.96/129.85 (declare-const tptp.mono_2Ec_2Emin_2E_3D_3D_3E_2E2 (-> tptp.mono_2Etyop_2Emin_2Ebool tptp.mono_2Etyop_2Emin_2Ebool tptp.mono_2Etyop_2Emin_2Ebool)) % 128.96/129.85 (declare-const tptp.c_2Emin_2E_3D_2E2 (-> tptp.du tptp.du tptp.u)) % 128.96/129.85 (declare-const tptp.mono_2Ec_2Ebool_2E_5C_2F_2E2 (-> tptp.mono_2Etyop_2Emin_2Ebool tptp.mono_2Etyop_2Emin_2Ebool tptp.mono_2Etyop_2Emin_2Ebool)) % 128.96/129.85 (declare-const tptp.mono_2Ec_2Ebool_2E_2F_5C_2E2 (-> tptp.mono_2Etyop_2Emin_2Ebool tptp.mono_2Etyop_2Emin_2Ebool tptp.mono_2Etyop_2Emin_2Ebool)) % 128.96/129.85 (declare-const tptp.combin_k_2E0 tptp.u) % 128.96/129.85 (declare-const tptp.j_mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29 (-> tptp.du tptp.mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29)) % 128.96/129.85 (declare-const tptp.combin_i_2E0 tptp.u) % 128.96/129.85 (declare-const tptp.mono_2Ec_2Ebool_2EF_2E0 tptp.mono_2Etyop_2Emin_2Ebool) % 128.96/129.85 (declare-const tptp.mono_2Ec_2Ebool_2ET_2E0 tptp.mono_2Etyop_2Emin_2Ebool) % 128.96/129.85 (declare-const tptp.p (-> tptp.mono_2Etyop_2Emin_2Ebool Bool)) % 128.96/129.85 (declare-const tptp.j_mono_2Etyop_2Emin_2Ebool (-> tptp.du tptp.mono_2Etyop_2Emin_2Ebool)) % 128.96/129.85 (declare-const tptp.mono_2Ec_2Ebool_2E_7E_2E1 (-> tptp.mono_2Etyop_2Emin_2Ebool tptp.mono_2Etyop_2Emin_2Ebool)) % 128.96/129.85 (declare-const tptp.tyop_2Emin_2Ebool tptp.d) % 128.96/129.85 (declare-const tptp.app_2E2 (-> tptp.du tptp.du tptp.u)) % 128.96/129.85 (declare-const tptp.i_mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29_29 (-> tptp.mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29_29 tptp.u)) % 128.96/129.85 (declare-const tptp.s (-> tptp.d tptp.u tptp.du)) % 128.96/129.85 (declare-const tptp.i_mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29 (-> tptp.mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29 tptp.u)) % 128.96/129.85 (declare-const tptp.tyop_2Emin_2Efun (-> tptp.d tptp.d tptp.d)) % 128.96/129.85 (declare-const tptp.i_mono_2Etyop_2Emin_2Ebool (-> tptp.mono_2Etyop_2Emin_2Ebool tptp.u)) % 128.96/129.85 (declare-const tptp.c_2Ebool_2E_21_2E1 (-> tptp.du tptp.u)) % 128.96/129.85 (declare-const tptp.c_2Ebool_2E_3F_2E1 (-> tptp.du tptp.u)) % 128.96/129.85 (declare-const tptp.combin_s_2E0 tptp.u) % 128.96/129.85 (declare-const tptp.j_mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29_29 (-> tptp.du tptp.mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29_29)) % 128.96/129.85 (declare-const tptp.c_2Ebool_2E_21_2E0 tptp.u) % 128.96/129.85 (declare-const tptp.c_2Equotient_2E_2D_2D_3E_2E0 tptp.u) % 128.96/129.85 (declare-const tptp.c_2Equotient_2E_2D_2D_3E_2E2 (-> tptp.du tptp.du tptp.u)) % 128.96/129.85 (declare-const tptp.c_2Equotient_2E_2D_2D_3E_2E3 (-> tptp.du tptp.du tptp.du tptp.u)) % 128.96/129.85 (declare-const tptp.mono_2Ec_2Ebool_2E_2F_5C_2E0 tptp.mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29_29) % 128.96/129.85 (declare-const tptp.mono_2Eapp_2E2_2Emono_2Etyop_2Emin_2Ebool_20mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29 (-> tptp.mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29_29 tptp.mono_2Etyop_2Emin_2Ebool tptp.mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29)) % 128.96/129.85 (define @t1 () (@var "V1g_2E0" tptp.u)) % 128.96/129.85 (define @t2 () (@var "A_27b" tptp.d)) % 128.96/129.85 (define @t3 () (@var "A_27a" tptp.d)) % 128.96/129.85 (define @t4 () (tptp.tyop_2Emin_2Efun @t3 @t2)) % 128.96/129.85 (define @t5 () (tptp.s @t4 @t1)) % 128.96/129.85 (define @t6 () (@var "V0f_2E0" tptp.u)) % 128.96/129.85 (define @t7 () (tptp.s @t4 @t6)) % 128.96/129.85 (define @t8 () (@var "V2x_2E0" tptp.u)) % 128.96/129.85 (define @t9 () (tptp.s @t3 @t8)) % 128.96/129.85 (define @t10 () (tptp.s @t2 (tptp.app_2E2 @t5 @t9))) % 128.96/129.85 (define @t11 () (@var "V1_2E0" tptp.mono_2Etyop_2Emin_2Ebool)) % 128.96/129.85 (define @t12 () (@var "V0_2E0" tptp.mono_2Etyop_2Emin_2Ebool)) % 128.96/129.85 (define @t13 () (tptp.p @t11)) % 128.96/129.85 (define @t14 () (tptp.p @t12)) % 128.96/129.85 (define @t15 () (@list @t12 @t11)) % 128.96/129.85 (define @t16 () (tptp.p tptp.mono_2Ec_2Ebool_2ET_2E0)) % 128.96/129.85 (define @t17 () (tptp.p tptp.mono_2Ec_2Ebool_2EF_2E0)) % 128.96/129.85 (define @t18 () (@var "V0t_2E0" tptp.mono_2Etyop_2Emin_2Ebool)) % 128.96/129.85 (define @t19 () (= @t18 tptp.mono_2Ec_2Ebool_2EF_2E0)) % 128.96/129.85 (define @t20 () (= @t18 tptp.mono_2Ec_2Ebool_2ET_2E0)) % 128.96/129.85 (define @t21 () (@list @t18)) % 128.96/129.85 (define @t22 () (@var "V0x_2E0" tptp.u)) % 128.96/129.85 (define @t23 () (tptp.s @t3 @t22)) % 128.96/129.85 (define @t24 () (@var "V1y_2E0" tptp.u)) % 128.96/129.85 (define @t25 () (tptp.tyop_2Emin_2Efun @t2 @t3)) % 128.96/129.85 (define @t26 () (@var "A_27c" tptp.d)) % 128.96/129.85 (define @t27 () (tptp.tyop_2Emin_2Efun @t2 @t26)) % 128.96/129.85 (define @t28 () (tptp.tyop_2Emin_2Efun @t3 @t27)) % 128.96/129.85 (define @t29 () (tptp.s @t28 @t6)) % 128.96/129.85 (define @t30 () (tptp.tyop_2Emin_2Efun @t3 @t26)) % 128.96/129.85 (define @t31 () (tptp.tyop_2Emin_2Efun @t4 @t30)) % 128.96/129.85 (define @t32 () (@list @t12)) % 128.96/129.85 (define @t33 () (@var "V1_2E0" tptp.u)) % 128.96/129.85 (define @t34 () (tptp.s @t3 @t33)) % 128.96/129.85 (define @t35 () (@var "V0_2E0" tptp.u)) % 128.96/129.85 (define @t36 () (tptp.s @t3 @t35)) % 128.96/129.85 (define @t37 () (@var "V1x_2E0" tptp.u)) % 128.96/129.85 (define @t38 () (tptp.s @t3 @t37)) % 128.96/129.85 (define @t39 () (tptp.tyop_2Emin_2Efun @t3 tptp.tyop_2Emin_2Ebool)) % 128.96/129.85 (define @t40 () (tptp.s @t39 @t6)) % 128.96/129.85 (define @t41 () (tptp.p (tptp.j_mono_2Etyop_2Emin_2Ebool (tptp.s tptp.tyop_2Emin_2Ebool (tptp.app_2E2 @t40 @t38))))) % 128.96/129.85 (define @t42 () (@list @t37)) % 128.96/129.85 (define @t43 () (@list @t3 @t6)) % 128.96/129.85 (define @t44 () (tptp.s tptp.tyop_2Emin_2Ebool @t35)) % 128.96/129.85 (define @t45 () (tptp.s tptp.tyop_2Emin_2Ebool (tptp.i_mono_2Etyop_2Emin_2Ebool (tptp.j_mono_2Etyop_2Emin_2Ebool @t44)))) % 128.96/129.85 (define @t46 () (@list @t35)) % 128.96/129.85 (define @t47 () (forall @t46 (= @t45 @t44))) % 128.96/129.85 (define @t48 () (tptp.tyop_2Emin_2Efun tptp.tyop_2Emin_2Ebool tptp.tyop_2Emin_2Ebool)) % 128.96/129.85 (define @t49 () (tptp.s @t48 @t35)) % 128.96/129.85 (define @t50 () (tptp.tyop_2Emin_2Efun tptp.tyop_2Emin_2Ebool @t48)) % 128.96/129.85 (define @t51 () (tptp.s @t50 @t35)) % 128.96/129.85 (define @t52 () (@var "V0_2E0" tptp.mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29)) % 128.96/129.85 (define @t53 () (tptp.s @t48 (tptp.i_mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29 @t52))) % 128.96/129.85 (define @t54 () (@var "V0_2E0" tptp.mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29_29)) % 128.96/129.85 (define @t55 () (tptp.s @t50 (tptp.i_mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29_29 @t54))) % 128.96/129.85 (define @t56 () (@var "X0_2E0" tptp.u)) % 128.96/129.85 (define @t57 () (tptp.s @t39 @t56)) % 128.96/129.85 (define @t58 () (tptp.tyop_2Emin_2Efun @t39 tptp.tyop_2Emin_2Ebool)) % 128.96/129.85 (define @t59 () (@list @t3 @t56)) % 128.96/129.85 (define @t60 () (@var "X1_2E0" tptp.u)) % 128.96/129.85 (define @t61 () (@var "A_27d" tptp.d)) % 128.96/129.85 (define @t62 () (tptp.tyop_2Emin_2Efun @t61 @t2)) % 128.96/129.85 (define @t63 () (tptp.s @t62 @t60)) % 128.96/129.85 (define @t64 () (tptp.s @t30 @t56)) % 128.96/129.85 (define @t65 () (tptp.tyop_2Emin_2Efun @t26 @t61)) % 128.96/129.85 (define @t66 () (tptp.tyop_2Emin_2Efun @t65 @t4)) % 128.96/129.85 (define @t67 () (tptp.tyop_2Emin_2Efun @t62 @t66)) % 128.96/129.85 (define @t68 () (@list @t3 @t2 @t26 @t61 @t56 @t60)) % 128.96/129.85 (define @t69 () (tptp.tyop_2Emin_2Efun @t2 @t61)) % 128.96/129.85 (define @t70 () (tptp.s @t69 @t60)) % 128.96/129.85 (define @t71 () (tptp.tyop_2Emin_2Efun @t26 @t3)) % 128.96/129.85 (define @t72 () (tptp.s @t71 @t56)) % 128.96/129.85 (define @t73 () (tptp.tyop_2Emin_2Efun @t4 @t65)) % 128.96/129.85 (define @t74 () (tptp.tyop_2Emin_2Efun @t69 @t73)) % 128.96/129.85 (define @t75 () (tptp.s @t73 (tptp.app_2E2 (tptp.s @t74 (tptp.app_2E2 (tptp.s (tptp.tyop_2Emin_2Efun @t71 @t74) tptp.c_2Equotient_2E_2D_2D_3E_2E0) @t72)) @t70))) % 128.96/129.85 (define @t76 () (@var "X2_2E0" tptp.u)) % 128.96/129.85 (define @t77 () (tptp.s @t4 @t76)) % 128.96/129.85 (define @t78 () (@list @t3 @t2 @t26 @t61 @t56 @t60 @t76)) % 128.96/129.85 (define @t79 () (@var "X1_2E0" tptp.mono_2Etyop_2Emin_2Ebool)) % 128.96/129.85 (define @t80 () (@var "X0_2E0" tptp.mono_2Etyop_2Emin_2Ebool)) % 128.96/129.85 (define @t81 () (tptp.p @t79)) % 128.96/129.85 (define @t82 () (tptp.p @t80)) % 128.96/129.85 (define @t83 () (@list @t80 @t79)) % 128.96/129.85 (define @t84 () (tptp.s @t3 @t60)) % 128.96/129.85 (define @t85 () (tptp.s @t3 @t56)) % 128.96/129.85 (define @t86 () (tptp.tyop_2Emin_2Efun @t3 @t39)) % 128.96/129.85 (define @t87 () (tptp.tyop_2Emin_2Efun @t2 (tptp.tyop_2Emin_2Efun @t2 tptp.tyop_2Emin_2Ebool))) % 128.96/129.85 (define @t88 () (tptp.s @t87 @t60)) % 128.96/129.85 (define @t89 () (tptp.s @t86 @t56)) % 128.96/129.85 (define @t90 () (tptp.tyop_2Emin_2Efun @t4 tptp.tyop_2Emin_2Ebool)) % 128.96/129.85 (define @t91 () (tptp.tyop_2Emin_2Efun @t4 @t90)) % 128.96/129.85 (define @t92 () (tptp.tyop_2Emin_2Efun @t87 @t91)) % 128.96/129.85 (define @t93 () (tptp.s @t91 (tptp.app_2E2 (tptp.s @t92 (tptp.app_2E2 (tptp.s (tptp.tyop_2Emin_2Efun @t86 @t92) tptp.c_2Equotient_2E_3D_3D_3D_3E_2E0) @t89)) @t88))) % 128.96/129.85 (define @t94 () (@list @t3 @t2 @t56 @t60)) % 128.96/129.85 (define @t95 () (@var "X3_2E0" tptp.u)) % 128.96/129.85 (define @t96 () (tptp.s @t4 @t95)) % 128.96/129.85 (define @t97 () (tptp.s @t25 @t76)) % 128.96/129.85 (define @t98 () (tptp.s @t4 @t60)) % 128.96/129.85 (define @t99 () (tptp.tyop_2Emin_2Efun @t25 tptp.tyop_2Emin_2Ebool)) % 128.96/129.85 (define @t100 () (tptp.tyop_2Emin_2Efun @t4 @t99)) % 128.96/129.85 (define @t101 () (tptp.s @t71 @t76)) % 128.96/129.85 (define @t102 () (tptp.s @t30 @t60)) % 128.96/129.85 (define @t103 () (tptp.tyop_2Emin_2Efun @t71 tptp.tyop_2Emin_2Ebool)) % 128.96/129.85 (define @t104 () (tptp.tyop_2Emin_2Efun @t30 @t103)) % 128.96/129.85 (define @t105 () (tptp.s @t62 @t76)) % 128.96/129.85 (define @t106 () (tptp.s @t87 @t56)) % 128.96/129.85 (define @t107 () (tptp.tyop_2Emin_2Efun @t62 tptp.tyop_2Emin_2Ebool)) % 128.96/129.85 (define @t108 () (tptp.tyop_2Emin_2Efun @t69 @t107)) % 128.96/129.85 (define @t109 () (tptp.s @t66 @t76)) % 128.96/129.85 (define @t110 () (tptp.s @t73 @t60)) % 128.96/129.85 (define @t111 () (tptp.s @t91 @t56)) % 128.96/129.85 (define @t112 () (tptp.tyop_2Emin_2Efun @t66 tptp.tyop_2Emin_2Ebool)) % 128.96/129.85 (define @t113 () (tptp.tyop_2Emin_2Efun @t73 @t112)) % 128.96/129.85 (define @t114 () (tptp.tyop_2Emin_2Efun @t3 @t4)) % 128.96/129.85 (define @t115 () (tptp.s @t114 @t56)) % 128.96/129.85 (define @t116 () (tptp.tyop_2Emin_2Efun @t114 @t4)) % 128.96/129.85 (define @t117 () (tptp.s @t116 tptp.c_2Ecombin_2EW_2E0)) % 128.96/129.85 (define @t118 () (tptp.s tptp.tyop_2Emin_2Ebool (tptp.i_mono_2Etyop_2Emin_2Ebool @t11))) % 128.96/129.85 (define @t119 () (@var "V1t2_2E0" tptp.mono_2Etyop_2Emin_2Ebool)) % 128.96/129.85 (define @t120 () (@var "V0t1_2E0" tptp.mono_2Etyop_2Emin_2Ebool)) % 128.96/129.85 (define @t121 () (tptp.p @t120)) % 128.96/129.85 (define @t122 () (tptp.p @t119)) % 128.96/129.85 (define @t123 () (tptp.p @t18)) % 128.96/129.85 (define @t124 () (not @t123)) % 128.96/129.85 (define @t125 () (@var "V2t3_2E0" tptp.mono_2Etyop_2Emin_2Ebool)) % 128.96/129.85 (define @t126 () (tptp.p @t125)) % 128.96/129.85 (define @t127 () (tptp.s @t114 @t6)) % 128.96/129.85 (define @t128 () (forall (@list @t3 @t2 @t6 @t37) (= (tptp.s @t2 (tptp.c_2Ecombin_2EW_2E2 @t127 @t38)) (tptp.s @t2 (tptp.app_2E2 (tptp.s @t4 (tptp.app_2E2 @t127 @t38)) @t38))))) % 128.96/129.85 (define @t129 () (@var "V4s_2E0" tptp.u)) % 128.96/129.85 (define @t130 () (tptp.s @t3 @t129)) % 128.96/129.85 (define @t131 () (@var "V1abs_2E0" tptp.u)) % 128.96/129.85 (define @t132 () (tptp.s @t4 @t131)) % 128.96/129.85 (define @t133 () (@var "V3r_2E0" tptp.u)) % 128.96/129.85 (define @t134 () (tptp.s @t3 @t133)) % 128.96/129.85 (define @t135 () (@var "V0R_2E0" tptp.u)) % 128.96/129.85 (define @t136 () (tptp.s @t86 @t135)) % 128.96/129.85 (define @t137 () (tptp.s @t39 (tptp.app_2E2 @t136 @t134))) % 128.96/129.85 (define @t138 () (@list @t133 @t129)) % 128.96/129.85 (define @t139 () (forall @t138 (= (tptp.p (tptp.j_mono_2Etyop_2Emin_2Ebool (tptp.s tptp.tyop_2Emin_2Ebool (tptp.app_2E2 @t137 @t130)))) (and (tptp.p (tptp.j_mono_2Etyop_2Emin_2Ebool (tptp.s tptp.tyop_2Emin_2Ebool (tptp.app_2E2 @t137 @t134)))) (tptp.p (tptp.j_mono_2Etyop_2Emin_2Ebool (tptp.s tptp.tyop_2Emin_2Ebool (tptp.app_2E2 (tptp.s @t39 (tptp.app_2E2 @t136 @t130)) @t130)))) (= (tptp.s @t2 (tptp.app_2E2 @t132 @t134)) (tptp.s @t2 (tptp.app_2E2 @t132 @t130))))))) % 128.96/129.85 (define @t140 () (@var "V2rep_2E0" tptp.u)) % 128.96/129.85 (define @t141 () (tptp.p (tptp.j_mono_2Etyop_2Emin_2Ebool (tptp.s tptp.tyop_2Emin_2Ebool (tptp.c_2Equotient_2EQUOTIENT_2E3 @t136 @t132 (tptp.s @t25 @t140)))))) % 128.96/129.85 (define @t142 () (forall (@list @t3 @t2 @t135 @t131 @t140) (=> @t141 @t139))) % 128.96/129.85 (define @t143 () (@var "V5rep2_2E0" tptp.u)) % 128.96/129.85 (define @t144 () (tptp.s @t62 @t143)) % 128.96/129.85 (define @t145 () (@var "V1abs1_2E0" tptp.u)) % 128.96/129.85 (define @t146 () (tptp.s @t30 @t145)) % 128.96/129.85 (define @t147 () (@var "V4abs2_2E0" tptp.u)) % 128.96/129.85 (define @t148 () (tptp.s @t69 @t147)) % 128.96/129.85 (define @t149 () (@var "V2rep1_2E0" tptp.u)) % 128.96/129.85 (define @t150 () (tptp.s @t71 @t149)) % 128.96/129.85 (define @t151 () (@var "V3R2_2E0" tptp.u)) % 128.96/129.85 (define @t152 () (tptp.s @t87 @t151)) % 128.96/129.85 (define @t153 () (@var "V0R1_2E0" tptp.u)) % 128.96/129.85 (define @t154 () (tptp.s @t86 @t153)) % 128.96/129.85 (define @t155 () (tptp.s @t91 (tptp.c_2Equotient_2E_3D_3D_3D_3E_2E2 @t154 @t152))) % 128.96/129.85 (define @t156 () (tptp.p (tptp.j_mono_2Etyop_2Emin_2Ebool (tptp.s tptp.tyop_2Emin_2Ebool (tptp.c_2Equotient_2EQUOTIENT_2E3 @t155 (tptp.s @t73 (tptp.c_2Equotient_2E_2D_2D_3E_2E2 @t150 @t148)) (tptp.s @t66 (tptp.c_2Equotient_2E_2D_2D_3E_2E2 @t146 @t144))))))) % 128.96/129.85 (define @t157 () (tptp.p (tptp.j_mono_2Etyop_2Emin_2Ebool (tptp.s tptp.tyop_2Emin_2Ebool (tptp.c_2Equotient_2EQUOTIENT_2E3 @t152 @t148 @t144))))) % 128.96/129.85 (define @t158 () (@list @t151 @t147 @t143)) % 128.96/129.85 (define @t159 () (forall @t158 (=> @t157 @t156))) % 128.96/129.85 (define @t160 () (tptp.p (tptp.j_mono_2Etyop_2Emin_2Ebool (tptp.s tptp.tyop_2Emin_2Ebool (tptp.c_2Equotient_2EQUOTIENT_2E3 @t154 @t146 @t150))))) % 128.96/129.85 (define @t161 () (=> @t160 @t159)) % 128.96/129.85 (define @t162 () (@list @t3 @t2 @t26 @t61 @t153 @t145 @t149)) % 128.96/129.85 (define @t163 () (forall @t162 @t161)) % 128.96/129.85 (define @t164 () (tptp.s @t116 tptp.c_2Equotient_2Erespects_2E0)) % 128.96/129.85 (define @t165 () (@list @t3 @t2)) % 128.96/129.85 (define @t166 () (forall @t165 (= @t164 @t117))) % 128.96/129.85 (define @t167 () (@var "V7g_2E0" tptp.u)) % 128.96/129.85 (define @t168 () (tptp.s @t4 @t167)) % 128.96/129.85 (define @t169 () (@var "V6f_2E0" tptp.u)) % 128.96/129.85 (define @t170 () (tptp.s @t4 @t169)) % 128.96/129.85 (define @t171 () (@list @t169 @t167)) % 128.96/129.85 (define @t172 () (forall @t171 (= (tptp.p (tptp.j_mono_2Etyop_2Emin_2Ebool (tptp.s tptp.tyop_2Emin_2Ebool (tptp.c_2Equotient_2E_3D_3D_3D_3E_2E4 @t154 @t152 @t170 @t168)))) (and (tptp.p (tptp.j_mono_2Etyop_2Emin_2Ebool (tptp.s tptp.tyop_2Emin_2Ebool (tptp.c_2Equotient_2Erespects_2E2 @t155 @t170)))) (tptp.p (tptp.j_mono_2Etyop_2Emin_2Ebool (tptp.s tptp.tyop_2Emin_2Ebool (tptp.c_2Equotient_2Erespects_2E2 @t155 @t168)))) (= (tptp.s @t65 (tptp.c_2Equotient_2E_2D_2D_3E_2E3 @t150 @t148 @t170)) (tptp.s @t65 (tptp.c_2Equotient_2E_2D_2D_3E_2E3 @t150 @t148 @t168))))))) % 128.96/129.85 (define @t173 () (forall @t158 (=> @t157 @t172))) % 128.96/129.85 (define @t174 () (=> @t160 @t173)) % 128.96/129.85 (define @t175 () (forall @t162 @t174)) % 128.96/129.85 (define @t176 () (not @t175)) % 128.96/129.85 (define @t177 () (not @t157)) % 128.96/129.85 (define @t178 () (forall @t158 (or @t177 @t172))) % 128.96/129.85 (define @t179 () (forall @t162 (or (not @t160) @t178))) % 128.96/129.85 (define @t180 () (@quantifiers_skolemize @t179 1)) % 128.96/129.85 (define @t181 () (@quantifiers_skolemize @t179 0)) % 128.96/129.85 (define @t182 () (tptp.tyop_2Emin_2Efun @t181 @t180)) % 128.96/129.85 (define @t183 () (tptp.s @t182 @t167)) % 128.96/129.85 (define @t184 () (@quantifiers_skolemize @t179 3)) % 128.96/129.85 (define @t185 () (tptp.tyop_2Emin_2Efun @t180 @t184)) % 128.96/129.85 (define @t186 () (tptp.s @t185 @t147)) % 128.96/129.85 (define @t187 () (@quantifiers_skolemize @t179 6)) % 128.96/129.85 (define @t188 () (@quantifiers_skolemize @t179 2)) % 128.96/129.85 (define @t189 () (tptp.tyop_2Emin_2Efun @t188 @t181)) % 128.96/129.85 (define @t190 () (tptp.s @t189 @t187)) % 128.96/129.85 (define @t191 () (tptp.tyop_2Emin_2Efun @t188 @t184)) % 128.96/129.85 (define @t192 () (tptp.s @t182 @t169)) % 128.96/129.85 (define @t193 () (tptp.tyop_2Emin_2Efun @t180 (tptp.tyop_2Emin_2Efun @t180 tptp.tyop_2Emin_2Ebool))) % 128.96/129.85 (define @t194 () (tptp.s @t193 @t151)) % 128.96/129.85 (define @t195 () (@quantifiers_skolemize @t179 4)) % 128.96/129.85 (define @t196 () (tptp.tyop_2Emin_2Efun @t181 (tptp.tyop_2Emin_2Efun @t181 tptp.tyop_2Emin_2Ebool))) % 128.96/129.85 (define @t197 () (tptp.s @t196 @t195)) % 128.96/129.85 (define @t198 () (tptp.tyop_2Emin_2Efun @t182 tptp.tyop_2Emin_2Ebool)) % 128.96/129.85 (define @t199 () (tptp.tyop_2Emin_2Efun @t182 @t198)) % 128.96/129.85 (define @t200 () (tptp.s @t199 (tptp.c_2Equotient_2E_3D_3D_3D_3E_2E2 @t197 @t194))) % 128.96/129.85 (define @t201 () (tptp.tyop_2Emin_2Efun @t184 @t180)) % 128.96/129.85 (define @t202 () (tptp.s @t201 @t143)) % 128.96/129.85 (define @t203 () (not (tptp.p (tptp.j_mono_2Etyop_2Emin_2Ebool (tptp.s tptp.tyop_2Emin_2Ebool (tptp.c_2Equotient_2EQUOTIENT_2E3 @t194 @t186 @t202)))))) % 128.96/129.85 (define @t204 () (forall @t158 (or @t203 (forall @t171 (= (tptp.p (tptp.j_mono_2Etyop_2Emin_2Ebool (tptp.s tptp.tyop_2Emin_2Ebool (tptp.c_2Equotient_2E_3D_3D_3D_3E_2E4 @t197 @t194 @t192 @t183)))) (and (tptp.p (tptp.j_mono_2Etyop_2Emin_2Ebool (tptp.s tptp.tyop_2Emin_2Ebool (tptp.c_2Equotient_2Erespects_2E2 @t200 @t192)))) (tptp.p (tptp.j_mono_2Etyop_2Emin_2Ebool (tptp.s tptp.tyop_2Emin_2Ebool (tptp.c_2Equotient_2Erespects_2E2 @t200 @t183)))) (= (tptp.s @t191 (tptp.c_2Equotient_2E_2D_2D_3E_2E3 @t190 @t186 @t192)) (tptp.s @t191 (tptp.c_2Equotient_2E_2D_2D_3E_2E3 @t190 @t186 @t183))))))))) % 128.96/129.85 (define @t205 () (@quantifiers_skolemize @t204 1)) % 128.96/129.85 (define @t206 () (tptp.s @t185 @t205)) % 128.96/129.85 (define @t207 () (@quantifiers_skolemize @t204 0)) % 128.96/129.85 (define @t208 () (tptp.s @t193 @t207)) % 128.96/129.85 (define @t209 () (tptp.c_2Equotient_2E_3D_3D_3D_3E_2E2 @t197 @t208)) % 128.96/129.85 (define @t210 () (tptp.s @t199 @t209)) % 128.96/129.85 (define @t211 () (forall @t171 (= (tptp.p (tptp.j_mono_2Etyop_2Emin_2Ebool (tptp.s tptp.tyop_2Emin_2Ebool (tptp.c_2Equotient_2E_3D_3D_3D_3E_2E4 @t197 @t208 @t192 @t183)))) (and (tptp.p (tptp.j_mono_2Etyop_2Emin_2Ebool (tptp.s tptp.tyop_2Emin_2Ebool (tptp.c_2Equotient_2Erespects_2E2 @t210 @t192)))) (tptp.p (tptp.j_mono_2Etyop_2Emin_2Ebool (tptp.s tptp.tyop_2Emin_2Ebool (tptp.c_2Equotient_2Erespects_2E2 @t210 @t183)))) (= (tptp.s @t191 (tptp.c_2Equotient_2E_2D_2D_3E_2E3 @t190 @t206 @t192)) (tptp.s @t191 (tptp.c_2Equotient_2E_2D_2D_3E_2E3 @t190 @t206 @t183))))))) % 128.96/129.85 (define @t212 () (@quantifiers_skolemize @t211 0)) % 128.96/129.85 (define @t213 () (@quantifiers_skolemize @t211 1)) % 128.96/129.85 (define @t214 () (@quantifiers_skolemize @t179 5)) % 128.96/129.85 (define @t215 () (tptp.s (tptp.tyop_2Emin_2Efun @t181 @t188) @t214)) % 128.96/129.85 (define @t216 () (tptp.p (tptp.j_mono_2Etyop_2Emin_2Ebool (tptp.s tptp.tyop_2Emin_2Ebool (tptp.c_2Equotient_2EQUOTIENT_2E3 @t197 @t215 @t190))))) % 128.96/129.85 (define @t217 () (not @t216)) % 128.96/129.85 (define @t218 () (or @t217 @t204)) % 128.96/129.85 (define @t219 () (@list true)) % 128.96/129.85 (define @t220 () (@list @t218)) % 128.96/129.85 (define @t221 () (@quantifiers_skolemize @t204 2)) % 128.96/129.85 (define @t222 () (tptp.s @t201 @t221)) % 128.96/129.85 (define @t223 () (tptp.p (tptp.j_mono_2Etyop_2Emin_2Ebool (tptp.s tptp.tyop_2Emin_2Ebool (tptp.c_2Equotient_2EQUOTIENT_2E3 @t208 @t206 @t222))))) % 128.96/129.85 (define @t224 () (not @t223)) % 128.96/129.85 (define @t225 () (or @t224 @t211)) % 128.96/129.85 (define @t226 () (@list @t225)) % 128.96/129.85 (define @t227 () (tptp.s @t182 @t213)) % 128.96/129.85 (define @t228 () (tptp.s @t191 (tptp.c_2Equotient_2E_2D_2D_3E_2E3 @t190 @t206 @t227))) % 128.96/129.85 (define @t229 () (tptp.s @t182 @t212)) % 128.96/129.85 (define @t230 () (tptp.s @t191 (tptp.c_2Equotient_2E_2D_2D_3E_2E3 @t190 @t206 @t229))) % 128.96/129.85 (define @t231 () (= @t230 @t228)) % 128.96/129.85 (define @t232 () (tptp.c_2Equotient_2Erespects_2E2 @t210 @t227)) % 128.96/129.85 (define @t233 () (tptp.s tptp.tyop_2Emin_2Ebool @t232)) % 128.96/129.85 (define @t234 () (tptp.j_mono_2Etyop_2Emin_2Ebool @t233)) % 128.96/129.85 (define @t235 () (tptp.p @t234)) % 128.96/129.85 (define @t236 () (tptp.c_2Equotient_2Erespects_2E2 @t210 @t229)) % 128.96/129.85 (define @t237 () (tptp.s tptp.tyop_2Emin_2Ebool @t236)) % 128.96/129.85 (define @t238 () (tptp.j_mono_2Etyop_2Emin_2Ebool @t237)) % 128.96/129.85 (define @t239 () (tptp.p @t238)) % 128.96/129.85 (define @t240 () (and @t239 @t235 @t231)) % 128.96/129.85 (define @t241 () (tptp.c_2Equotient_2E_3D_3D_3D_3E_2E4 @t197 @t208 @t229 @t227)) % 128.96/129.85 (define @t242 () (tptp.s tptp.tyop_2Emin_2Ebool @t241)) % 128.96/129.85 (define @t243 () (tptp.j_mono_2Etyop_2Emin_2Ebool @t242)) % 128.96/129.85 (define @t244 () (tptp.p @t243)) % 128.96/129.85 (define @t245 () (= @t244 @t240)) % 128.96/129.85 (define @t246 () (tptp.tyop_2Emin_2Efun @t193 @t199)) % 128.96/129.85 (define @t247 () (tptp.app_2E2 (tptp.s @t246 (tptp.app_2E2 (tptp.s (tptp.tyop_2Emin_2Efun @t196 @t246) tptp.c_2Equotient_2E_3D_3D_3D_3E_2E0) @t197)) @t208)) % 128.96/129.85 (define @t248 () (tptp.s @t199 @t247)) % 128.96/129.85 (define @t249 () (tptp.app_2E2 @t248 @t229)) % 128.96/129.85 (define @t250 () (tptp.s @t198 @t249)) % 128.96/129.85 (define @t251 () (tptp.app_2E2 @t250 @t227)) % 128.96/129.85 (define @t252 () (= @t242 (tptp.s tptp.tyop_2Emin_2Ebool (tptp.i_mono_2Etyop_2Emin_2Ebool @t243)))) % 128.96/129.85 (define @t253 () (= @t210 @t248)) % 128.96/129.85 (define @t254 () (tptp.s tptp.tyop_2Emin_2Ebool @t251)) % 128.96/129.85 (define @t255 () (tptp.j_mono_2Etyop_2Emin_2Ebool @t254)) % 128.96/129.85 (define @t256 () (= @t243 @t255)) % 128.96/129.85 (define @t257 () (tptp.i_mono_2Etyop_2Emin_2Ebool @t255)) % 128.96/129.85 (define @t258 () (tptp.s tptp.tyop_2Emin_2Ebool @t257)) % 128.96/129.85 (define @t259 () (= @t254 @t258)) % 128.96/129.85 (define @t260 () (tptp.app_2E2 @t210 @t229)) % 128.96/129.85 (define @t261 () (tptp.s @t198 @t260)) % 128.96/129.85 (define @t262 () (tptp.app_2E2 @t261 @t227)) % 128.96/129.85 (define @t263 () (tptp.s tptp.tyop_2Emin_2Ebool @t262)) % 128.96/129.85 (define @t264 () (tptp.j_mono_2Etyop_2Emin_2Ebool @t263)) % 128.96/129.85 (define @t265 () (tptp.p @t264)) % 128.96/129.85 (define @t266 () (and @t244 @t252 @t253 @t256 @t259)) % 128.96/129.85 (define @t267 () (tptp.c_2Equotient_2E_2D_2D_3E_2E2 @t215 @t222)) % 128.96/129.85 (define @t268 () (tptp.c_2Equotient_2E_2D_2D_3E_2E2 @t190 @t206)) % 128.96/129.85 (define @t269 () (forall @t158 (or @t177 @t156))) % 128.96/129.85 (define @t270 () (tptp.tyop_2Emin_2Efun @t191 @t182)) % 128.96/129.85 (define @t271 () (tptp.tyop_2Emin_2Efun @t182 @t191)) % 128.96/129.85 (define @t272 () (forall @t158 (or @t203 (tptp.p (tptp.j_mono_2Etyop_2Emin_2Ebool (tptp.s tptp.tyop_2Emin_2Ebool (tptp.c_2Equotient_2EQUOTIENT_2E3 @t200 (tptp.s @t271 (tptp.c_2Equotient_2E_2D_2D_3E_2E2 @t190 @t186)) (tptp.s @t270 (tptp.c_2Equotient_2E_2D_2D_3E_2E2 @t215 @t202))))))))) % 128.96/129.85 (define @t273 () (or @t217 @t272)) % 128.96/129.85 (define @t274 () (@list false false)) % 128.96/129.85 (define @t275 () (tptp.s @t270 @t267)) % 128.96/129.85 (define @t276 () (tptp.s @t271 @t268)) % 128.96/129.85 (define @t277 () (tptp.p (tptp.j_mono_2Etyop_2Emin_2Ebool (tptp.s tptp.tyop_2Emin_2Ebool (tptp.c_2Equotient_2EQUOTIENT_2E3 @t210 @t276 @t275))))) % 128.96/129.85 (define @t278 () (or @t224 @t277)) % 128.96/129.85 (define @t279 () (tptp.s @t182 @t129)) % 128.96/129.85 (define @t280 () (tptp.s @t182 @t133)) % 128.96/129.85 (define @t281 () (= (tptp.s @t191 (tptp.app_2E2 @t276 @t280)) (tptp.s @t191 (tptp.app_2E2 @t276 @t279)))) % 128.96/129.85 (define @t282 () (tptp.s @t198 (tptp.app_2E2 @t210 @t280))) % 128.96/129.85 (define @t283 () (forall @t138 (= (tptp.p (tptp.j_mono_2Etyop_2Emin_2Ebool (tptp.s tptp.tyop_2Emin_2Ebool (tptp.app_2E2 @t282 @t279)))) (and (tptp.p (tptp.j_mono_2Etyop_2Emin_2Ebool (tptp.s tptp.tyop_2Emin_2Ebool (tptp.app_2E2 @t282 @t280)))) (tptp.p (tptp.j_mono_2Etyop_2Emin_2Ebool (tptp.s tptp.tyop_2Emin_2Ebool (tptp.app_2E2 (tptp.s @t198 (tptp.app_2E2 @t210 @t279)) @t279)))) @t281)))) % 128.96/129.85 (define @t284 () (not @t277)) % 128.96/129.85 (define @t285 () (or @t284 @t283)) % 128.96/129.85 (define @t286 () (@list @t212 @t213)) % 128.96/129.85 (define @t287 () (tptp.app_2E2 @t276 @t227)) % 128.96/129.85 (define @t288 () (tptp.s @t191 @t287)) % 128.96/129.85 (define @t289 () (tptp.app_2E2 @t276 @t229)) % 128.96/129.85 (define @t290 () (tptp.s @t191 @t289)) % 128.96/129.85 (define @t291 () (= @t290 @t288)) % 128.96/129.85 (define @t292 () (tptp.s tptp.tyop_2Emin_2Ebool (tptp.app_2E2 (tptp.s @t198 (tptp.app_2E2 @t210 @t227)) @t227))) % 128.96/129.85 (define @t293 () (tptp.p (tptp.j_mono_2Etyop_2Emin_2Ebool @t292))) % 128.96/129.85 (define @t294 () (tptp.s tptp.tyop_2Emin_2Ebool (tptp.app_2E2 @t261 @t229))) % 128.96/129.85 (define @t295 () (tptp.j_mono_2Etyop_2Emin_2Ebool @t294)) % 128.96/129.85 (define @t296 () (tptp.p @t295)) % 128.96/129.85 (define @t297 () (and @t296 @t293 @t291)) % 128.96/129.85 (define @t298 () (= @t265 @t297)) % 128.96/129.85 (define @t299 () (not @t297)) % 128.96/129.85 (define @t300 () (tptp.tyop_2Emin_2Efun @t199 @t198)) % 128.96/129.85 (define @t301 () (tptp.s @t300 tptp.c_2Equotient_2Erespects_2E0)) % 128.96/129.85 (define @t302 () (tptp.app_2E2 @t301 @t210)) % 128.96/129.85 (define @t303 () (tptp.s @t198 @t302)) % 128.96/129.85 (define @t304 () (tptp.app_2E2 @t303 @t229)) % 128.96/129.85 (define @t305 () (@list @t182 tptp.tyop_2Emin_2Ebool @t209 @t212)) % 128.96/129.85 (define @t306 () (tptp.s @t300 tptp.c_2Ecombin_2EW_2E0)) % 128.96/129.85 (define @t307 () (forall @t165 (= @t117 @t164))) % 128.96/129.85 (define @t308 () (= @t306 @t301)) % 128.96/129.85 (define @t309 () (= @t301 @t306)) % 128.96/129.85 (define @t310 () (@list false)) % 128.96/129.85 (define @t311 () (tptp.i_mono_2Etyop_2Emin_2Ebool @t238)) % 128.96/129.85 (define @t312 () (tptp.s tptp.tyop_2Emin_2Ebool @t311)) % 128.96/129.85 (define @t313 () (= @t237 @t312)) % 128.96/129.85 (define @t314 () (tptp.s tptp.tyop_2Emin_2Ebool @t304)) % 128.96/129.85 (define @t315 () (tptp.j_mono_2Etyop_2Emin_2Ebool @t314)) % 128.96/129.85 (define @t316 () (= @t238 @t315)) % 128.96/129.85 (define @t317 () (tptp.i_mono_2Etyop_2Emin_2Ebool @t315)) % 128.96/129.85 (define @t318 () (tptp.s tptp.tyop_2Emin_2Ebool @t317)) % 128.96/129.85 (define @t319 () (= @t314 @t318)) % 128.96/129.85 (define @t320 () (tptp.s tptp.tyop_2Emin_2Ebool (tptp.c_2Ecombin_2EW_2E2 @t210 @t229))) % 128.96/129.85 (define @t321 () (= @t320 @t294)) % 128.96/129.85 (define @t322 () (tptp.app_2E2 @t306 @t210)) % 128.96/129.85 (define @t323 () (tptp.s @t198 @t322)) % 128.96/129.85 (define @t324 () (tptp.app_2E2 @t323 @t229)) % 128.96/129.85 (define @t325 () (tptp.s tptp.tyop_2Emin_2Ebool @t324)) % 128.96/129.85 (define @t326 () (= @t320 @t325)) % 128.96/129.85 (define @t327 () (tptp.app_2E2 @t250 @t229)) % 128.96/129.85 (define @t328 () (tptp.s tptp.tyop_2Emin_2Ebool @t327)) % 128.96/129.85 (define @t329 () (tptp.j_mono_2Etyop_2Emin_2Ebool @t328)) % 128.96/129.85 (define @t330 () (tptp.p @t329)) % 128.96/129.85 (define @t331 () (tptp.app_2E2 @t306 @t248)) % 128.96/129.85 (define @t332 () (tptp.s @t198 @t331)) % 128.96/129.85 (define @t333 () (tptp.app_2E2 @t332 @t229)) % 128.96/129.85 (define @t334 () (and @t313 @t253 @t316 @t319 @t321 @t309 @t296 @t326)) % 128.96/129.85 (define @t335 () (not @t326)) % 128.96/129.85 (define @t336 () (not @t309)) % 128.96/129.85 (define @t337 () (not @t321)) % 128.96/129.85 (define @t338 () (not @t319)) % 128.96/129.85 (define @t339 () (not @t316)) % 128.96/129.85 (define @t340 () (not @t253)) % 128.96/129.85 (define @t341 () (not @t313)) % 128.96/129.85 (define @t342 () (tptp.s tptp.tyop_2Emin_2Ebool (tptp.c_2Ecombin_2EW_2E2 @t210 @t227))) % 128.96/129.85 (define @t343 () (= @t342 @t292)) % 128.96/129.85 (define @t344 () (@list @t182 tptp.tyop_2Emin_2Ebool @t209 @t213)) % 128.96/129.85 (define @t345 () (= @t292 @t342)) % 128.96/129.85 (define @t346 () (tptp.app_2E2 @t303 @t227)) % 128.96/129.85 (define @t347 () (tptp.i_mono_2Etyop_2Emin_2Ebool @t234)) % 128.96/129.85 (define @t348 () (tptp.s tptp.tyop_2Emin_2Ebool @t347)) % 128.96/129.85 (define @t349 () (= @t233 @t348)) % 128.96/129.85 (define @t350 () (tptp.s tptp.tyop_2Emin_2Ebool @t346)) % 128.96/129.85 (define @t351 () (tptp.j_mono_2Etyop_2Emin_2Ebool @t350)) % 128.96/129.85 (define @t352 () (= @t234 @t351)) % 128.96/129.85 (define @t353 () (tptp.i_mono_2Etyop_2Emin_2Ebool @t351)) % 128.96/129.85 (define @t354 () (tptp.s tptp.tyop_2Emin_2Ebool @t353)) % 128.96/129.85 (define @t355 () (= @t350 @t354)) % 128.96/129.85 (define @t356 () (tptp.app_2E2 @t323 @t227)) % 128.96/129.85 (define @t357 () (tptp.s tptp.tyop_2Emin_2Ebool @t356)) % 128.96/129.85 (define @t358 () (= @t342 @t357)) % 128.96/129.85 (define @t359 () (tptp.app_2E2 @t248 @t227)) % 128.96/129.85 (define @t360 () (tptp.s @t198 @t359)) % 128.96/129.85 (define @t361 () (tptp.app_2E2 @t360 @t227)) % 128.96/129.85 (define @t362 () (tptp.s tptp.tyop_2Emin_2Ebool @t361)) % 128.96/129.85 (define @t363 () (tptp.j_mono_2Etyop_2Emin_2Ebool @t362)) % 128.96/129.85 (define @t364 () (tptp.p @t363)) % 128.96/129.85 (define @t365 () (and @t253 @t309 @t293 @t349 @t352 @t345 @t355 @t358)) % 128.96/129.85 (define @t366 () (not @t358)) % 128.96/129.85 (define @t367 () (not @t355)) % 128.96/129.85 (define @t368 () (not @t345)) % 128.96/129.85 (define @t369 () (not @t352)) % 128.96/129.85 (define @t370 () (not @t349)) % 128.96/129.85 (define @t371 () (tptp.tyop_2Emin_2Efun @t185 @t271)) % 128.96/129.85 (define @t372 () (tptp.s @t271 (tptp.app_2E2 (tptp.s @t371 (tptp.app_2E2 (tptp.s (tptp.tyop_2Emin_2Efun @t189 @t371) tptp.c_2Equotient_2E_2D_2D_3E_2E0) @t190)) @t206))) % 128.96/129.85 (define @t373 () (= @t276 @t372)) % 128.96/129.85 (define @t374 () (tptp.app_2E2 @t372 @t227)) % 128.96/129.85 (define @t375 () (tptp.s @t191 @t374)) % 128.96/129.85 (define @t376 () (= @t228 @t375)) % 128.96/129.85 (define @t377 () (tptp.app_2E2 @t372 @t229)) % 128.96/129.85 (define @t378 () (tptp.s @t191 @t377)) % 128.96/129.85 (define @t379 () (= @t230 @t378)) % 128.96/129.85 (define @t380 () (and @t373 @t291 @t376 @t379)) % 128.96/129.85 (define @t381 () (not @t379)) % 128.96/129.85 (define @t382 () (not @t376)) % 128.96/129.85 (define @t383 () (not @t291)) % 128.96/129.85 (define @t384 () (not @t373)) % 128.96/129.85 (define @t385 () (not @t244)) % 128.96/129.85 (define @t386 () (not @t240)) % 128.96/129.85 (define @t387 () (@list @t240)) % 128.96/129.85 (define @t388 () (and @t231 @t373 @t376 @t379)) % 128.96/129.85 (define @t389 () (and @t235 @t253 @t309 @t349 @t352 @t345 @t355 @t358)) % 128.96/129.85 (define @t390 () (@list false false false false false false false false)) % 128.96/129.85 (define @t391 () (and @t239 @t313 @t253 @t316 @t319 @t321 @t309 @t326)) % 128.96/129.85 (define @t392 () (tptp.c_2Equotient_2EQUOTIENT_2E3 @t248 @t276 @t275)) % 128.96/129.85 (define @t393 () (tptp.s tptp.tyop_2Emin_2Ebool @t392)) % 128.96/129.85 (define @t394 () (tptp.j_mono_2Etyop_2Emin_2Ebool @t393)) % 128.96/129.85 (define @t395 () (tptp.p @t394)) % 128.96/129.85 (define @t396 () (tptp.s @t198 (tptp.app_2E2 @t248 @t280))) % 128.96/129.85 (define @t397 () (forall @t138 (= (tptp.p (tptp.j_mono_2Etyop_2Emin_2Ebool (tptp.s tptp.tyop_2Emin_2Ebool (tptp.app_2E2 @t396 @t279)))) (and (tptp.p (tptp.j_mono_2Etyop_2Emin_2Ebool (tptp.s tptp.tyop_2Emin_2Ebool (tptp.app_2E2 @t396 @t280)))) (tptp.p (tptp.j_mono_2Etyop_2Emin_2Ebool (tptp.s tptp.tyop_2Emin_2Ebool (tptp.app_2E2 (tptp.s @t198 (tptp.app_2E2 @t248 @t279)) @t279)))) @t281)))) % 128.96/129.85 (define @t398 () (not @t395)) % 128.96/129.85 (define @t399 () (or @t398 @t397)) % 128.96/129.85 (define @t400 () (tptp.p @t255)) % 128.96/129.85 (define @t401 () (not @t400)) % 128.96/129.85 (define @t402 () (not @t256)) % 128.96/129.85 (define @t403 () (and @t385 @t256)) % 128.96/129.85 (define @t404 () (@list true false)) % 128.96/129.85 (define @t405 () (and @t330 @t364 @t291)) % 128.96/129.85 (define @t406 () (= @t400 @t405)) % 128.96/129.85 (define @t407 () (not @t405)) % 128.96/129.85 (assume @p1 (forall (@list @t3 @t2 @t6 @t1) (=> (forall (@list @t8) (= (tptp.s @t2 (tptp.app_2E2 @t7 @t9)) @t10)) (= @t7 @t5)))) % 128.96/129.85 (assume @p2 (forall @t15 (=> (= @t14 @t13) (= @t12 @t11)))) % 128.96/129.85 (assume @p3 @t16) % 128.96/129.85 (assume @p4 (not @t17)) % 128.96/129.85 (assume @p5 (forall @t21 (or @t20 @t19))) % 128.96/129.85 (assume @p6 (forall (@list @t3 @t22) (= (tptp.s @t3 (tptp.app_2E2 (tptp.s (tptp.tyop_2Emin_2Efun @t3 @t3) tptp.combin_i_2E0) @t23)) @t23))) % 128.96/129.85 (assume @p7 (forall (@list @t3 @t2 @t22 @t24) (= (tptp.s @t3 (tptp.app_2E2 (tptp.s @t25 (tptp.app_2E2 (tptp.s (tptp.tyop_2Emin_2Efun @t3 @t25) tptp.combin_k_2E0) @t23)) (tptp.s @t2 @t24))) @t23))) % 128.96/129.85 (assume @p8 (forall (@list @t3 @t2 @t26 @t6 @t1 @t8) (= (tptp.s @t26 (tptp.app_2E2 (tptp.s @t30 (tptp.app_2E2 (tptp.s @t31 (tptp.app_2E2 (tptp.s (tptp.tyop_2Emin_2Efun @t28 @t31) tptp.combin_s_2E0) @t29)) @t5)) @t9)) (tptp.s @t26 (tptp.app_2E2 (tptp.s @t27 (tptp.app_2E2 @t29 @t9)) @t10))))) % 128.96/129.85 (assume @p9 (forall @t15 (= (tptp.p (tptp.mono_2Ec_2Ebool_2E_2F_5C_2E2 @t12 @t11)) (and @t14 @t13)))) % 128.96/129.85 (assume @p10 (forall @t15 (= (tptp.p (tptp.mono_2Ec_2Ebool_2E_5C_2F_2E2 @t12 @t11)) (or @t14 @t13)))) % 128.96/129.85 (assume @p11 (forall @t32 (= (tptp.p (tptp.mono_2Ec_2Ebool_2E_7E_2E1 @t12)) (not @t14)))) % 128.96/129.85 (assume @p12 (forall @t15 (= (tptp.p (tptp.mono_2Ec_2Emin_2E_3D_3D_3E_2E2 @t12 @t11)) (=> @t14 @t13)))) % 128.96/129.85 (assume @p13 (forall (@list @t3 @t35 @t33) (= (tptp.p (tptp.j_mono_2Etyop_2Emin_2Ebool (tptp.s tptp.tyop_2Emin_2Ebool (tptp.c_2Emin_2E_3D_2E2 @t36 @t34)))) (= @t36 @t34)))) % 128.96/129.85 (assume @p14 (forall @t43 (= (tptp.p (tptp.j_mono_2Etyop_2Emin_2Ebool (tptp.s tptp.tyop_2Emin_2Ebool (tptp.c_2Ebool_2E_21_2E1 @t40)))) (forall @t42 @t41)))) % 128.96/129.85 (assume @p15 (forall @t43 (= (tptp.p (tptp.j_mono_2Etyop_2Emin_2Ebool (tptp.s tptp.tyop_2Emin_2Ebool (tptp.c_2Ebool_2E_3F_2E1 @t40)))) (exists @t42 @t41)))) % 128.96/129.85 (assume @p16 @t47) % 128.96/129.85 (assume @p17 (forall @t46 (= (tptp.s @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))) % 128.96/129.85 (assume @p18 (forall @t46 (= (tptp.s @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))) % 128.96/129.85 (assume @p19 (forall @t32 (= (tptp.j_mono_2Etyop_2Emin_2Ebool (tptp.s tptp.tyop_2Emin_2Ebool (tptp.i_mono_2Etyop_2Emin_2Ebool @t12))) @t12))) % 128.96/129.85 (assume @p20 (forall (@list @t52) (= (tptp.j_mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29 @t53) @t52))) % 128.96/129.85 (assume @p21 (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))) % 128.96/129.85 (assume @p22 (forall @t59 (= (tptp.j_mono_2Etyop_2Emin_2Ebool (tptp.s tptp.tyop_2Emin_2Ebool (tptp.c_2Ebool_2E_21_2E1 @t57))) (tptp.j_mono_2Etyop_2Emin_2Ebool (tptp.s tptp.tyop_2Emin_2Ebool (tptp.app_2E2 (tptp.s @t58 tptp.c_2Ebool_2E_21_2E0) @t57)))))) % 128.96/129.85 (assume @p23 (forall @t68 (= (tptp.s @t66 (tptp.c_2Equotient_2E_2D_2D_3E_2E2 @t64 @t63)) (tptp.s @t66 (tptp.app_2E2 (tptp.s @t67 (tptp.app_2E2 (tptp.s (tptp.tyop_2Emin_2Efun @t30 @t67) tptp.c_2Equotient_2E_2D_2D_3E_2E0) @t64)) @t63))))) % 128.96/129.85 (assume @p24 (forall @t68 (= (tptp.s @t73 (tptp.c_2Equotient_2E_2D_2D_3E_2E2 @t72 @t70)) @t75))) % 128.96/129.85 (assume @p25 (forall @t78 (= (tptp.s @t65 (tptp.c_2Equotient_2E_2D_2D_3E_2E3 @t72 @t70 @t77)) (tptp.s @t65 (tptp.app_2E2 @t75 @t77))))) % 128.96/129.85 (assume @p26 (forall @t83 (= (and @t82 @t81) (tptp.p (tptp.mono_2Eapp_2E2_2Emono_2Etyop_2Emin_2Ebool_20mono_2Etyop_2Emin_2Ebool (tptp.mono_2Eapp_2E2_2Emono_2Etyop_2Emin_2Ebool_20mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29 tptp.mono_2Ec_2Ebool_2E_2F_5C_2E0 @t80) @t79))))) % 128.96/129.85 (assume @p27 (forall (@list @t3 @t56 @t60) (= (= @t85 @t84) (tptp.p (tptp.j_mono_2Etyop_2Emin_2Ebool (tptp.s tptp.tyop_2Emin_2Ebool (tptp.app_2E2 (tptp.s @t39 (tptp.app_2E2 (tptp.s @t86 tptp.c_2Emin_2E_3D_2E0) @t85)) @t84))))))) % 128.96/129.85 (assume @p28 (forall @t94 (= (tptp.s @t91 (tptp.c_2Equotient_2E_3D_3D_3D_3E_2E2 @t89 @t88)) @t93))) % 128.96/129.85 (assume @p29 (forall (@list @t3 @t2 @t56 @t60 @t76 @t95) (= (tptp.j_mono_2Etyop_2Emin_2Ebool (tptp.s tptp.tyop_2Emin_2Ebool (tptp.c_2Equotient_2E_3D_3D_3D_3E_2E4 @t89 @t88 @t77 @t96))) (tptp.j_mono_2Etyop_2Emin_2Ebool (tptp.s tptp.tyop_2Emin_2Ebool (tptp.app_2E2 (tptp.s @t90 (tptp.app_2E2 @t93 @t77)) @t96)))))) % 128.96/129.85 (assume @p30 (forall @t83 (= (=> @t82 @t81) (tptp.p (tptp.mono_2Eapp_2E2_2Emono_2Etyop_2Emin_2Ebool_20mono_2Etyop_2Emin_2Ebool (tptp.mono_2Eapp_2E2_2Emono_2Etyop_2Emin_2Ebool_20mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29 tptp.mono_2Ec_2Emin_2E_3D_3D_3E_2E0 @t80) @t79))))) % 128.96/129.85 (assume @p31 (forall @t59 (= (tptp.j_mono_2Etyop_2Emin_2Ebool (tptp.s tptp.tyop_2Emin_2Ebool (tptp.c_2Ebool_2E_3F_2E1 @t57))) (tptp.j_mono_2Etyop_2Emin_2Ebool (tptp.s tptp.tyop_2Emin_2Ebool (tptp.app_2E2 (tptp.s @t58 tptp.c_2Ebool_2E_3F_2E0) @t57)))))) % 128.96/129.85 (assume @p32 (forall (@list @t3 @t2 @t56 @t60 @t76) (= (tptp.j_mono_2Etyop_2Emin_2Ebool (tptp.s tptp.tyop_2Emin_2Ebool (tptp.c_2Equotient_2EQUOTIENT_2E3 @t89 @t98 @t97))) (tptp.j_mono_2Etyop_2Emin_2Ebool (tptp.s tptp.tyop_2Emin_2Ebool (tptp.app_2E2 (tptp.s @t99 (tptp.app_2E2 (tptp.s @t100 (tptp.app_2E2 (tptp.s (tptp.tyop_2Emin_2Efun @t86 @t100) tptp.c_2Equotient_2EQUOTIENT_2E0) @t89)) @t98)) @t97)))))) % 128.96/129.85 (assume @p33 (forall (@list @t3 @t26 @t56 @t60 @t76) (= (tptp.j_mono_2Etyop_2Emin_2Ebool (tptp.s tptp.tyop_2Emin_2Ebool (tptp.c_2Equotient_2EQUOTIENT_2E3 @t89 @t102 @t101))) (tptp.j_mono_2Etyop_2Emin_2Ebool (tptp.s tptp.tyop_2Emin_2Ebool (tptp.app_2E2 (tptp.s @t103 (tptp.app_2E2 (tptp.s @t104 (tptp.app_2E2 (tptp.s (tptp.tyop_2Emin_2Efun @t86 @t104) tptp.c_2Equotient_2EQUOTIENT_2E0) @t89)) @t102)) @t101)))))) % 128.96/129.85 (assume @p34 (forall (@list @t2 @t61 @t56 @t60 @t76) (= (tptp.j_mono_2Etyop_2Emin_2Ebool (tptp.s tptp.tyop_2Emin_2Ebool (tptp.c_2Equotient_2EQUOTIENT_2E3 @t106 @t70 @t105))) (tptp.j_mono_2Etyop_2Emin_2Ebool (tptp.s tptp.tyop_2Emin_2Ebool (tptp.app_2E2 (tptp.s @t107 (tptp.app_2E2 (tptp.s @t108 (tptp.app_2E2 (tptp.s (tptp.tyop_2Emin_2Efun @t87 @t108) tptp.c_2Equotient_2EQUOTIENT_2E0) @t106)) @t70)) @t105)))))) % 128.96/129.85 (assume @p35 (forall @t78 (= (tptp.j_mono_2Etyop_2Emin_2Ebool (tptp.s tptp.tyop_2Emin_2Ebool (tptp.c_2Equotient_2EQUOTIENT_2E3 @t111 @t110 @t109))) (tptp.j_mono_2Etyop_2Emin_2Ebool (tptp.s tptp.tyop_2Emin_2Ebool (tptp.app_2E2 (tptp.s @t112 (tptp.app_2E2 (tptp.s @t113 (tptp.app_2E2 (tptp.s (tptp.tyop_2Emin_2Efun @t91 @t113) tptp.c_2Equotient_2EQUOTIENT_2E0) @t111)) @t110)) @t109)))))) % 128.96/129.85 (assume @p36 (forall @t94 (= (tptp.s @t2 (tptp.c_2Ecombin_2EW_2E2 @t115 @t84)) (tptp.s @t2 (tptp.app_2E2 (tptp.s @t4 (tptp.app_2E2 @t117 @t115)) @t84))))) % 128.96/129.85 (assume @p37 (forall @t83 (= (or @t82 @t81) (tptp.p (tptp.mono_2Eapp_2E2_2Emono_2Etyop_2Emin_2Ebool_20mono_2Etyop_2Emin_2Ebool (tptp.mono_2Eapp_2E2_2Emono_2Etyop_2Emin_2Ebool_20mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29 tptp.mono_2Ec_2Ebool_2E_5C_2F_2E0 @t80) @t79))))) % 128.96/129.85 (assume @p38 (forall @t94 (= (tptp.j_mono_2Etyop_2Emin_2Ebool (tptp.s tptp.tyop_2Emin_2Ebool (tptp.c_2Equotient_2Erespects_2E2 @t111 @t98))) (tptp.j_mono_2Etyop_2Emin_2Ebool (tptp.s tptp.tyop_2Emin_2Ebool (tptp.app_2E2 (tptp.s @t90 (tptp.app_2E2 (tptp.s (tptp.tyop_2Emin_2Efun @t91 @t90) tptp.c_2Equotient_2Erespects_2E0) @t111)) @t98)))))) % 128.96/129.85 (assume @p39 (forall (@list @t80) (= (not @t82) (tptp.p (tptp.mono_2Eapp_2E2_2Emono_2Etyop_2Emin_2Ebool_20mono_2Etyop_2Emin_2Ebool tptp.mono_2Ec_2Ebool_2E_7E_2E0 @t80))))) % 128.96/129.85 (assume @p40 (forall (@list @t52 @t11) (= (tptp.s tptp.tyop_2Emin_2Ebool (tptp.i_mono_2Etyop_2Emin_2Ebool (tptp.mono_2Eapp_2E2_2Emono_2Etyop_2Emin_2Ebool_20mono_2Etyop_2Emin_2Ebool @t52 @t11))) (tptp.s tptp.tyop_2Emin_2Ebool (tptp.app_2E2 @t53 @t118))))) % 128.96/129.85 (assume @p41 (forall (@list @t54 @t11) (= (tptp.s @t48 (tptp.i_mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29 (tptp.mono_2Eapp_2E2_2Emono_2Etyop_2Emin_2Ebool_20mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29 @t54 @t11))) (tptp.s @t48 (tptp.app_2E2 @t55 @t118))))) % 128.96/129.85 (assume @p42 (forall (@list @t120 @t119) (=> (=> @t121 @t122) (=> (=> @t122 @t121) (= @t120 @t119))))) % 128.96/129.85 (assume @p43 (forall @t21 (and (= (and @t16 @t123) @t123) (= (and @t123 @t16) @t123) (= (and @t17 @t123) @t17) (= (and @t123 @t17) @t17) (= (and @t123 @t123) @t123)))) % 128.96/129.85 (assume @p44 (forall @t21 (and (= (= tptp.mono_2Ec_2Ebool_2ET_2E0 @t18) @t123) (= @t20 @t123) (= (= tptp.mono_2Ec_2Ebool_2EF_2E0 @t18) @t124) (= @t19 @t124)))) % 128.96/129.85 (assume @p45 (forall (@list @t120 @t119 @t125) (= (=> @t121 (=> @t122 @t126)) (=> (and @t121 @t122) @t126)))) % 128.96/129.85 (assume @p46 @t128) % 128.96/129.85 (assume @p47 @t142) % 128.96/129.85 (assume @p48 @t163) % 128.96/129.85 (assume @p49 @t166) % 128.96/129.85 (assume @p50 @t176) % 128.96/129.85 (assume @p51 true) % 128.96/129.85 (step @p52 :rule instantiate :premises (@p25) :args ((@list @t181 @t180 @t188 @t184 @t187 @t205 @t212))) % 128.96/129.85 (step @p53 :rule instantiate :premises (@p25) :args ((@list @t181 @t180 @t188 @t184 @t187 @t205 @t213))) % 128.96/129.85 (step @p54 :rule instantiate :premises (@p23) :args ((@list @t188 @t184 @t181 @t180 @t187 @t205))) % 128.96/129.85 (step @p55 :rule bool-impl-elim :args (@t160 @t178)) % 128.96/129.85 (step @p56 :rule cong :premises (@p55) :args ((forall @t162 (=> @t160 @t178)))) % 128.96/129.85 (step @p57 :rule bool-impl-elim :args (@t157 @t172)) % 128.96/129.85 (step @p58 :rule cong :premises (@p57) :args (@t173)) % 128.96/129.85 (step @p59 :rule refl :args (@t160)) % 128.96/129.85 (step @p60 :rule cong :premises (@p59 @p58) :args (@t174)) % 128.96/129.85 (step @p61 :rule cong :premises (@p60) :args (@t175)) % 128.96/129.85 (step @p62 :rule trans :premises (@p61 @p56)) % 128.96/129.85 (step @p63 :rule cong :premises (@p62) :args (@t176)) % 128.96/129.85 (step @p64 :rule eq_resolve :premises (@p50 @p63)) % 128.96/129.85 (step @p65 :rule skolemize :premises (@p64)) % 128.96/129.85 (step @p66 :rule cnf_or_neg :args (@t218 1)) % 128.96/129.85 (step @p67 :rule chain_m_resolution :premises (@p66 @p65) :args ((not @t204) @t219 @t220)) % 128.96/129.85 (step @p68 :rule skolemize :premises (@p67)) % 128.96/129.85 (step @p69 :rule cnf_or_neg :args (@t225 1)) % 128.96/129.85 (step @p70 :rule chain_m_resolution :premises (@p69 @p68) :args ((not @t211) @t219 @t226)) % 128.96/129.85 (step @p71 :rule skolemize :premises (@p70)) % 128.96/129.85 (step @p72 :rule cnf_equiv_neg2 :args (@t245)) % 128.96/129.85 (step @p73 :rule eq-symm :args (@t45 @t44)) % 128.96/129.85 (step @p74 :rule cong :premises (@p73) :args (@t47)) % 128.96/129.85 (step @p75 :rule eq_resolve :premises (@p16 @p74)) % 128.96/129.85 (step @p76 :rule instantiate :premises (@p75) :args ((@list @t241))) % 128.96/129.85 (step @p77 :rule instantiate :premises (@p28) :args ((@list @t181 @t180 @t195 @t207))) % 128.96/129.85 (step @p78 :rule instantiate :premises (@p29) :args ((@list @t181 @t180 @t195 @t207 @t212 @t213))) % 128.96/129.85 (step @p79 :rule instantiate :premises (@p75) :args ((@list @t251))) % 128.96/129.85 (assume-push @p570 @t244) % 128.96/129.85 (assume-push @p571 @t252) % 128.96/129.85 (assume-push @p572 @t253) % 128.96/129.85 (assume-push @p573 @t256) % 128.96/129.85 (assume-push @p574 @t259) % 128.96/129.85 (assume-push @p575 @t244) % 128.96/129.85 (assume-push @p576 @t252) % 128.96/129.85 (assume-push @p577 @t256) % 128.96/129.85 (assume-push @p578 @t259) % 128.96/129.85 (assume-push @p579 @t253) % 128.96/129.85 (step @p90 :rule true_intro :premises (@p570)) % 128.96/129.85 (step @p91 :rule symm :premises (@p76)) % 128.96/129.85 (step @p92 :rule symm :premises (@p78)) % 128.96/129.85 (step @p93 :rule cong :premises (@p92) :args (@t257)) % 128.96/129.85 (step @p94 :rule refl :args (tptp.tyop_2Emin_2Ebool)) % 128.96/129.85 (step @p95 :rule cong :premises (@p94 @p93) :args (@t258)) % 128.96/129.85 (step @p96 :rule refl :args (@t227)) % 128.96/129.85 (step @p97 :rule refl :args (@t229)) % 128.96/129.85 (step @p98 :rule cong :premises (@p77 @p97) :args (@t260)) % 128.96/129.85 (step @p99 :rule refl :args (@t198)) % 128.96/129.85 (step @p100 :rule cong :premises (@p99 @p98) :args (@t261)) % 128.96/129.85 (step @p101 :rule cong :premises (@p100 @p96) :args (@t262)) % 128.96/129.85 (step @p102 :rule cong :premises (@p94 @p101) :args (@t263)) % 128.96/129.85 (step @p103 :rule trans :premises (@p102 @p79 @p95 @p91)) % 128.96/129.85 (step @p104 :rule cong :premises (@p103) :args (@t264)) % 128.96/129.85 (step @p105 :rule cong :premises (@p104) :args (@t265)) % 128.96/129.85 (step @p106 :rule trans :premises (@p105 @p90)) % 128.96/129.85 (step @p107 :rule true_elim :premises (@p106)) % 128.96/129.85 (step-pop @p580 :rule scope :premises (@p107)) % 128.96/129.85 (step-pop @p581 :rule scope :premises (@p580)) % 128.96/129.85 (step-pop @p582 :rule scope :premises (@p581)) % 128.96/129.85 (step-pop @p583 :rule scope :premises (@p582)) % 128.96/129.85 (step-pop @p584 :rule scope :premises (@p583)) % 128.96/129.85 (step @p108 :rule process_scope :premises (@p584) :args (@t265)) % 128.96/129.85 (step @p114 :rule and_intro :premises (@p570 @p76 @p78 @p79 @p77)) % 128.96/129.85 (step @p115 :rule modus_ponens :premises (@p114 @p108)) % 128.96/129.85 (step-pop @p585 :rule scope :premises (@p115)) % 128.96/129.85 (step-pop @p586 :rule scope :premises (@p585)) % 128.96/129.85 (step-pop @p587 :rule scope :premises (@p586)) % 128.96/129.85 (step-pop @p588 :rule scope :premises (@p587)) % 128.96/129.85 (step-pop @p589 :rule scope :premises (@p588)) % 128.96/129.85 (step @p116 :rule process_scope :premises (@p589) :args (@t265)) % 128.96/129.85 (step @p122 :rule implies_elim :premises (@p116)) % 128.96/129.85 (step @p123 :rule cnf_and_neg :args (@t266)) % 128.96/129.85 (step @p124 :rule resolution :premises (@p123 @p122) :args (true @t266)) % 128.96/129.85 (step @p125 :rule bool-impl-elim :args (@t141 @t139)) % 128.96/129.85 (step @p126 :rule cong :premises (@p125) :args (@t142)) % 128.96/129.85 (step @p127 :rule eq_resolve :premises (@p47 @p126)) % 128.96/129.85 (step @p128 :rule instantiate :premises (@p127) :args ((@list @t182 @t191 @t209 @t268 @t267))) % 128.96/129.85 (step @p129 :rule bool-impl-elim :args (@t160 @t269)) % 128.96/129.85 (step @p130 :rule cong :premises (@p129) :args ((forall @t162 (=> @t160 @t269)))) % 128.96/129.85 (step @p131 :rule bool-impl-elim :args (@t157 @t156)) % 128.96/129.85 (step @p132 :rule cong :premises (@p131) :args (@t159)) % 128.96/129.85 (step @p133 :rule cong :premises (@p59 @p132) :args (@t161)) % 128.96/129.85 (step @p134 :rule cong :premises (@p133) :args (@t163)) % 128.96/129.85 (step @p135 :rule trans :premises (@p134 @p130)) % 128.96/129.85 (step @p136 :rule eq_resolve :premises (@p48 @p135)) % 128.96/129.85 (step @p137 :rule instantiate :premises (@p136) :args ((@list @t181 @t180 @t188 @t184 @t195 @t214 @t187))) % 128.96/129.85 (step @p138 :rule bool-double-not-elim :args (@t216)) % 128.96/129.85 (step @p139 :rule refl :args (@t218)) % 128.96/129.85 (step @p140 :rule nary_cong :premises (@p139 @p138) :args ((or @t218 (not @t217)))) % 128.96/129.85 (step @p141 :rule cnf_or_neg :args (@t218 0)) % 128.96/129.85 (step @p142 :rule eq_resolve :premises (@p141 @p140)) % 128.96/129.85 (step @p143 :rule reordering :premises (@p142) :args ((or @t216 @t218))) % 128.96/129.85 (step @p144 :rule chain_m_resolution :premises (@p143 @p65) :args (@t216 @t219 @t220)) % 128.96/129.85 (step @p145 :rule cnf_or_pos :args (@t273)) % 128.96/129.85 (step @p146 :rule reordering :premises (@p145) :args ((or @t217 @t272 (not @t273)))) % 128.96/129.85 (step @p147 :rule chain_m_resolution :premises (@p146 @p144 @p137) :args (@t272 @t274 (@list @t216 @t273))) % 128.96/129.85 (step @p148 :rule instantiate :premises (@p147) :args ((@list @t207 @t205 @t221))) % 128.96/129.85 (step @p149 :rule bool-double-not-elim :args (@t223)) % 128.96/129.85 (step @p150 :rule refl :args (@t225)) % 128.96/129.85 (step @p151 :rule nary_cong :premises (@p150 @p149) :args ((or @t225 (not @t224)))) % 128.96/129.85 (step @p152 :rule cnf_or_neg :args (@t225 0)) % 128.96/129.85 (step @p153 :rule eq_resolve :premises (@p152 @p151)) % 128.96/129.85 (step @p154 :rule reordering :premises (@p153) :args ((or @t223 @t225))) % 128.96/129.85 (step @p155 :rule chain_m_resolution :premises (@p154 @p68) :args (@t223 @t219 @t226)) % 128.96/129.85 (step @p156 :rule cnf_or_pos :args (@t278)) % 128.96/129.85 (step @p157 :rule reordering :premises (@p156) :args ((or @t224 @t277 (not @t278)))) % 128.96/129.85 (step @p158 :rule chain_m_resolution :premises (@p157 @p155 @p148) :args (@t277 @t274 (@list @t223 @t278))) % 128.96/129.85 (step @p159 :rule cnf_or_pos :args (@t285)) % 128.96/129.85 (step @p160 :rule reordering :premises (@p159) :args ((or @t284 @t283 (not @t285)))) % 128.96/129.85 (step @p161 :rule chain_m_resolution :premises (@p160 @p158 @p128) :args (@t283 @t274 (@list @t277 @t285))) % 128.96/129.85 (step @p162 :rule instantiate :premises (@p161) :args (@t286)) % 128.96/129.85 (step @p163 :rule cnf_equiv_pos1 :args (@t298)) % 128.96/129.85 (step @p164 :rule reordering :premises (@p163) :args ((or @t297 (not @t265) (not @t298)))) % 128.96/129.85 (step @p165 :rule cnf_and_pos :args (@t297 0)) % 128.96/129.85 (step @p166 :rule reordering :premises (@p165) :args ((or @t296 @t299))) % 128.96/129.85 (step @p167 :rule cnf_and_pos :args (@t297 1)) % 128.96/129.85 (step @p168 :rule reordering :premises (@p167) :args ((or @t293 @t299))) % 128.96/129.85 (step @p169 :rule cnf_and_pos :args (@t297 2)) % 128.96/129.85 (step @p170 :rule reordering :premises (@p169) :args ((or @t291 @t299))) % 128.96/129.85 (step @p171 :rule instantiate :premises (@p75) :args ((@list @t236))) % 128.96/129.85 (step @p172 :rule instantiate :premises (@p38) :args ((@list @t181 @t180 @t209 @t212))) % 128.96/129.85 (step @p173 :rule instantiate :premises (@p75) :args ((@list @t304))) % 128.96/129.85 (step @p174 :rule instantiate :premises (@p46) :args (@t305)) % 128.96/129.85 (step @p175 :rule eq-symm :args (@t164 @t117)) % 128.96/129.85 (step @p176 :rule cong :premises (@p175) :args (@t166)) % 128.96/129.85 (step @p177 :rule eq_resolve :premises (@p49 @p176)) % 128.96/129.85 (step @p178 :rule eq-symm :args (@t306 @t301)) % 128.96/129.85 (step @p179 :rule refl :args (@t307)) % 128.96/129.85 (step @p180 :rule cong :premises (@p179 @p178) :args ((=> @t307 @t308))) % 128.96/129.85 (assume-push @p590 @t307) % 128.96/129.85 (step @p182 :rule instantiate :premises (@p177) :args ((@list @t182 tptp.tyop_2Emin_2Ebool))) % 128.96/129.85 (step-pop @p591 :rule scope :premises (@p182)) % 128.96/129.85 (step @p183 :rule process_scope :premises (@p591) :args (@t308)) % 128.96/129.85 (step @p185 :rule eq_resolve :premises (@p183 @p180)) % 128.96/129.85 (step @p186 :rule implies_elim :premises (@p185)) % 128.96/129.85 (step @p187 :rule chain_m_resolution :premises (@p186 @p177) :args (@t309 @t310 (@list @t307))) % 128.96/129.85 (step @p188 :rule instantiate :premises (@p36) :args (@t305)) % 128.96/129.85 (assume-push @p592 @t313) % 128.96/129.85 (assume-push @p593 @t253) % 128.96/129.85 (assume-push @p594 @t316) % 128.96/129.85 (assume-push @p595 @t319) % 128.96/129.85 (assume-push @p596 @t321) % 128.96/129.85 (assume-push @p597 @t309) % 128.96/129.85 (assume-push @p598 @t296) % 128.96/129.85 (assume-push @p599 @t326) % 128.96/129.85 (assume-push @p600 @t296) % 128.96/129.85 (assume-push @p601 @t253) % 128.96/129.85 (assume-push @p602 @t321) % 128.96/129.85 (assume-push @p603 @t326) % 128.96/129.85 (assume-push @p604 @t309) % 128.96/129.85 (assume-push @p605 @t319) % 128.96/129.85 (assume-push @p606 @t316) % 128.96/129.85 (assume-push @p607 @t313) % 128.96/129.85 (step @p205 :rule true_intro :premises (@p598)) % 128.96/129.85 (step @p97 :rule refl :args (@t229)) % 128.96/129.85 (step @p206 :rule symm :premises (@p77)) % 128.96/129.85 (step @p207 :rule cong :premises (@p206 @p97) :args (@t249)) % 128.96/129.85 (step @p99 :rule refl :args (@t198)) % 128.96/129.85 (step @p208 :rule cong :premises (@p99 @p207) :args (@t250)) % 128.96/129.85 (step @p209 :rule cong :premises (@p208 @p97) :args (@t327)) % 128.96/129.85 (step @p94 :rule refl :args (tptp.tyop_2Emin_2Ebool)) % 128.96/129.85 (step @p210 :rule cong :premises (@p94 @p209) :args (@t328)) % 128.96/129.85 (step @p211 :rule cong :premises (@p210) :args (@t329)) % 128.96/129.85 (step @p212 :rule cong :premises (@p211) :args (@t330)) % 128.96/129.85 (step @p213 :rule symm :premises (@p211)) % 128.96/129.85 (step @p214 :rule symm :premises (@p188)) % 128.96/129.85 (step @p215 :rule refl :args (@t306)) % 128.96/129.85 (step @p216 :rule cong :premises (@p215 @p206) :args (@t331)) % 128.96/129.85 (step @p217 :rule cong :premises (@p187 @p77) :args (@t302)) % 128.96/129.85 (step @p218 :rule trans :premises (@p217 @p216)) % 128.96/129.85 (step @p219 :rule cong :premises (@p99 @p218) :args (@t303)) % 128.96/129.85 (step @p220 :rule symm :premises (@p217)) % 128.96/129.85 (step @p221 :rule cong :premises (@p99 @p220) :args (@t332)) % 128.96/129.85 (step @p222 :rule trans :premises (@p221 @p219)) % 128.96/129.85 (step @p223 :rule cong :premises (@p222 @p97) :args (@t333)) % 128.96/129.85 (step @p224 :rule symm :premises (@p221)) % 128.96/129.85 (step @p225 :rule cong :premises (@p224 @p97) :args (@t304)) % 128.96/129.85 (step @p226 :rule trans :premises (@p225 @p223)) % 128.96/129.85 (step @p227 :rule cong :premises (@p94 @p226) :args (@t314)) % 128.96/129.85 (step @p228 :rule symm :premises (@p173)) % 128.96/129.85 (step @p229 :rule cong :premises (@p172) :args (@t311)) % 128.96/129.85 (step @p230 :rule cong :premises (@p94 @p229) :args (@t312)) % 128.96/129.85 (step @p231 :rule trans :premises (@p171 @p230 @p228 @p227 @p214 @p174)) % 128.96/129.85 (step @p232 :rule cong :premises (@p231) :args (@t238)) % 128.96/129.85 (step @p233 :rule trans :premises (@p232 @p213)) % 128.96/129.85 (step @p234 :rule cong :premises (@p233) :args (@t239)) % 128.96/129.85 (step @p235 :rule trans :premises (@p234 @p212 @p205)) % 128.96/129.85 (step @p236 :rule true_elim :premises (@p235)) % 128.96/129.85 (step-pop @p608 :rule scope :premises (@p236)) % 128.96/129.85 (step-pop @p609 :rule scope :premises (@p608)) % 128.96/129.85 (step-pop @p610 :rule scope :premises (@p609)) % 128.96/129.85 (step-pop @p611 :rule scope :premises (@p610)) % 128.96/129.85 (step-pop @p612 :rule scope :premises (@p611)) % 128.96/129.85 (step-pop @p613 :rule scope :premises (@p612)) % 128.96/129.85 (step-pop @p614 :rule scope :premises (@p613)) % 128.96/129.85 (step-pop @p615 :rule scope :premises (@p614)) % 128.96/129.85 (step @p237 :rule process_scope :premises (@p615) :args (@t239)) % 128.96/129.85 (step @p246 :rule and_intro :premises (@p598 @p77 @p174 @p188 @p187 @p173 @p172 @p171)) % 128.96/129.85 (step @p247 :rule modus_ponens :premises (@p246 @p237)) % 128.96/129.85 (step-pop @p616 :rule scope :premises (@p247)) % 128.96/129.85 (step-pop @p617 :rule scope :premises (@p616)) % 128.96/129.85 (step-pop @p618 :rule scope :premises (@p617)) % 128.96/129.85 (step-pop @p619 :rule scope :premises (@p618)) % 128.96/129.85 (step-pop @p620 :rule scope :premises (@p619)) % 128.96/129.85 (step-pop @p621 :rule scope :premises (@p620)) % 128.96/129.85 (step-pop @p622 :rule scope :premises (@p621)) % 128.96/129.85 (step-pop @p623 :rule scope :premises (@p622)) % 128.96/129.85 (step @p248 :rule process_scope :premises (@p623) :args (@t239)) % 128.96/129.85 (step @p257 :rule implies_elim :premises (@p248)) % 128.96/129.85 (step @p258 :rule cnf_and_neg :args (@t334)) % 128.96/129.85 (step @p259 :rule resolution :premises (@p258 @p257) :args (true @t334)) % 128.96/129.85 (step @p260 :rule reordering :premises (@p259) :args ((or @t239 @t341 @t340 @t339 @t338 @t337 @t336 (not @t296) @t335))) % 128.96/129.85 (step @p261 :rule instantiate :premises (@p75) :args ((@list @t232))) % 128.96/129.85 (step @p262 :rule instantiate :premises (@p38) :args ((@list @t181 @t180 @t209 @t213))) % 128.96/129.85 (step @p263 :rule eq-symm :args (@t342 @t292)) % 128.96/129.85 (step @p264 :rule refl :args (@t128)) % 128.96/129.85 (step @p265 :rule cong :premises (@p264 @p263) :args ((=> @t128 @t343))) % 128.96/129.85 (assume-push @p624 @t128) % 128.96/129.85 (step @p267 :rule instantiate :premises (@p46) :args (@t344)) % 128.96/129.85 (step-pop @p625 :rule scope :premises (@p267)) % 128.96/129.85 (step @p268 :rule process_scope :premises (@p625) :args (@t343)) % 128.96/129.85 (step @p270 :rule eq_resolve :premises (@p268 @p265)) % 128.96/129.85 (step @p271 :rule implies_elim :premises (@p270)) % 128.96/129.85 (step @p272 :rule chain_m_resolution :premises (@p271 @p46) :args (@t345 @t310 (@list @t128))) % 128.96/129.85 (step @p273 :rule instantiate :premises (@p75) :args ((@list @t346))) % 128.96/129.85 (step @p274 :rule instantiate :premises (@p36) :args (@t344)) % 128.96/129.85 (assume-push @p626 @t253) % 128.96/129.85 (assume-push @p627 @t309) % 128.96/129.85 (assume-push @p628 @t293) % 128.96/129.85 (assume-push @p629 @t349) % 128.96/129.85 (assume-push @p630 @t352) % 128.96/129.85 (assume-push @p631 @t345) % 128.96/129.85 (assume-push @p632 @t355) % 128.96/129.85 (assume-push @p633 @t358) % 128.96/129.85 (assume-push @p634 @t293) % 128.96/129.85 (assume-push @p635 @t253) % 128.96/129.85 (assume-push @p636 @t345) % 128.96/129.85 (assume-push @p637 @t358) % 128.96/129.85 (assume-push @p638 @t309) % 128.96/129.85 (assume-push @p639 @t355) % 128.96/129.85 (assume-push @p640 @t352) % 128.96/129.85 (assume-push @p641 @t349) % 128.96/129.85 (step @p291 :rule true_intro :premises (@p628)) % 128.96/129.85 (step @p96 :rule refl :args (@t227)) % 128.96/129.85 (step @p206 :rule symm :premises (@p77)) % 128.96/129.85 (step @p292 :rule cong :premises (@p206 @p96) :args (@t359)) % 128.96/129.85 (step @p99 :rule refl :args (@t198)) % 128.96/129.85 (step @p293 :rule cong :premises (@p99 @p292) :args (@t360)) % 128.96/129.85 (step @p294 :rule cong :premises (@p293 @p96) :args (@t361)) % 128.96/129.85 (step @p94 :rule refl :args (tptp.tyop_2Emin_2Ebool)) % 128.96/129.85 (step @p295 :rule cong :premises (@p94 @p294) :args (@t362)) % 128.96/129.85 (step @p296 :rule cong :premises (@p295) :args (@t363)) % 128.96/129.85 (step @p297 :rule cong :premises (@p296) :args (@t364)) % 128.96/129.85 (step @p298 :rule symm :premises (@p295)) % 128.96/129.85 (step @p267 :rule instantiate :premises (@p46) :args (@t344)) % 128.96/129.85 (step @p299 :rule symm :premises (@p274)) % 128.96/129.85 (step @p215 :rule refl :args (@t306)) % 128.96/129.85 (step @p216 :rule cong :premises (@p215 @p206) :args (@t331)) % 128.96/129.85 (step @p217 :rule cong :premises (@p187 @p77) :args (@t302)) % 128.96/129.85 (step @p218 :rule trans :premises (@p217 @p216)) % 128.96/129.85 (step @p219 :rule cong :premises (@p99 @p218) :args (@t303)) % 128.96/129.85 (step @p300 :rule cong :premises (@p219 @p96) :args (@t346)) % 128.96/129.85 (step @p301 :rule cong :premises (@p94 @p300) :args (@t350)) % 128.96/129.85 (step @p302 :rule symm :premises (@p273)) % 128.96/129.85 (step @p303 :rule cong :premises (@p262) :args (@t347)) % 128.96/129.85 (step @p304 :rule cong :premises (@p94 @p303) :args (@t348)) % 128.96/129.85 (step @p305 :rule trans :premises (@p261 @p304 @p302 @p301 @p299 @p267 @p298)) % 128.96/129.85 (step @p306 :rule cong :premises (@p305) :args (@t234)) % 128.96/129.85 (step @p307 :rule cong :premises (@p306) :args (@t235)) % 128.96/129.85 (step @p308 :rule trans :premises (@p307 @p297 @p291)) % 128.96/129.85 (step @p309 :rule true_elim :premises (@p308)) % 128.96/129.85 (step-pop @p642 :rule scope :premises (@p309)) % 128.96/129.85 (step-pop @p643 :rule scope :premises (@p642)) % 128.96/129.85 (step-pop @p644 :rule scope :premises (@p643)) % 128.96/129.85 (step-pop @p645 :rule scope :premises (@p644)) % 128.96/129.85 (step-pop @p646 :rule scope :premises (@p645)) % 128.96/129.85 (step-pop @p647 :rule scope :premises (@p646)) % 128.96/129.85 (step-pop @p648 :rule scope :premises (@p647)) % 128.96/129.85 (step-pop @p649 :rule scope :premises (@p648)) % 128.96/129.85 (step @p310 :rule process_scope :premises (@p649) :args (@t235)) % 128.96/129.85 (step @p319 :rule and_intro :premises (@p628 @p77 @p272 @p274 @p187 @p273 @p262 @p261)) % 128.96/129.85 (step @p320 :rule modus_ponens :premises (@p319 @p310)) % 128.96/129.85 (step-pop @p650 :rule scope :premises (@p320)) % 128.96/129.85 (step-pop @p651 :rule scope :premises (@p650)) % 128.96/129.85 (step-pop @p652 :rule scope :premises (@p651)) % 128.96/129.85 (step-pop @p653 :rule scope :premises (@p652)) % 128.96/129.85 (step-pop @p654 :rule scope :premises (@p653)) % 128.96/129.85 (step-pop @p655 :rule scope :premises (@p654)) % 128.96/129.85 (step-pop @p656 :rule scope :premises (@p655)) % 128.96/129.85 (step-pop @p657 :rule scope :premises (@p656)) % 128.96/129.85 (step @p321 :rule process_scope :premises (@p657) :args (@t235)) % 128.96/129.85 (step @p330 :rule implies_elim :premises (@p321)) % 128.96/129.85 (step @p331 :rule cnf_and_neg :args (@t365)) % 128.96/129.85 (step @p332 :rule resolution :premises (@p331 @p330) :args (true @t365)) % 128.96/129.85 (step @p333 :rule reordering :premises (@p332) :args ((or @t235 @t340 @t336 (not @t293) @t370 @t369 @t368 @t367 @t366))) % 128.96/129.85 (assume-push @p658 @t373) % 128.96/129.85 (assume-push @p659 @t291) % 128.96/129.85 (assume-push @p660 @t376) % 128.96/129.85 (assume-push @p661 @t379) % 128.96/129.85 (assume-push @p662 @t376) % 128.96/129.85 (assume-push @p663 @t373) % 128.96/129.85 (assume-push @p664 @t291) % 128.96/129.85 (assume-push @p665 @t379) % 128.96/129.85 (step @p342 :rule symm :premises (@p53)) % 128.96/129.85 (step @p96 :rule refl :args (@t227)) % 128.96/129.85 (step @p343 :rule cong :premises (@p54 @p96) :args (@t287)) % 128.96/129.85 (step @p344 :rule refl :args (@t191)) % 128.96/129.85 (step @p345 :rule cong :premises (@p344 @p343) :args (@t288)) % 128.96/129.85 (step @p97 :rule refl :args (@t229)) % 128.96/129.85 (step @p346 :rule symm :premises (@p54)) % 128.96/129.85 (step @p347 :rule cong :premises (@p346 @p97) :args (@t377)) % 128.96/129.85 (step @p348 :rule cong :premises (@p344 @p347) :args (@t378)) % 128.96/129.85 (step @p349 :rule trans :premises (@p52 @p348 @p659 @p345 @p342)) % 128.96/129.85 (step-pop @p666 :rule scope :premises (@p349)) % 128.96/129.85 (step-pop @p667 :rule scope :premises (@p666)) % 128.96/129.85 (step-pop @p668 :rule scope :premises (@p667)) % 128.96/129.85 (step-pop @p669 :rule scope :premises (@p668)) % 128.96/129.85 (step @p350 :rule process_scope :premises (@p669) :args (@t231)) % 128.96/129.85 (step @p355 :rule and_intro :premises (@p53 @p54 @p659 @p52)) % 128.96/129.85 (step @p356 :rule modus_ponens :premises (@p355 @p350)) % 128.96/129.85 (step-pop @p670 :rule scope :premises (@p356)) % 128.96/129.85 (step-pop @p671 :rule scope :premises (@p670)) % 128.96/129.85 (step-pop @p672 :rule scope :premises (@p671)) % 128.96/129.85 (step-pop @p673 :rule scope :premises (@p672)) % 128.96/129.85 (step @p357 :rule process_scope :premises (@p673) :args (@t231)) % 128.96/129.85 (step @p362 :rule implies_elim :premises (@p357)) % 128.96/129.85 (step @p363 :rule cnf_and_neg :args (@t380)) % 128.96/129.85 (step @p364 :rule resolution :premises (@p363 @p362) :args (true @t380)) % 128.96/129.85 (step @p365 :rule reordering :premises (@p364) :args ((or @t231 @t384 @t383 @t382 @t381))) % 128.96/129.85 (step @p366 :rule cnf_and_neg :args (@t240)) % 128.96/129.85 (step @p367 :rule chain_m_resolution :premises (@p366 @p365 @p52 @p53 @p54 @p333 @p274 @p273 @p272 @p262 @p261 @p187 @p77 @p260 @p188 @p187 @p174 @p173 @p172 @p77 @p171 @p170 @p168 @p166 @p164 @p162 @p124 @p79 @p78 @p77 @p76 @p72 @p71) :args (@t385 (@list false false false false false false false false false false false false false false false false false false false false false false false false false false false false false false true true) (@list @t231 @t379 @t376 @t373 @t235 @t358 @t355 @t345 @t352 @t349 @t309 @t253 @t239 @t326 @t309 @t321 @t319 @t316 @t253 @t313 @t291 @t293 @t296 @t297 @t298 @t265 @t259 @t256 @t253 @t252 @t240 @t245))) % 128.96/129.85 (step @p368 :rule cnf_equiv_neg1 :args (@t245)) % 128.96/129.85 (step @p369 :rule reordering :premises (@p368) :args ((or @t244 @t240 @t245))) % 128.96/129.85 (step @p370 :rule chain_m_resolution :premises (@p369 @p367 @p71) :args (@t240 (@list true true) (@list @t244 @t245))) % 128.96/129.85 (step @p371 :rule cnf_and_pos :args (@t240 2)) % 128.96/129.85 (step @p372 :rule reordering :premises (@p371) :args ((or @t231 @t386))) % 128.96/129.85 (step @p373 :rule chain_m_resolution :premises (@p372 @p370) :args (@t231 @t310 @t387)) % 128.96/129.85 (assume-push @p674 @t231) % 128.96/129.85 (assume-push @p675 @t373) % 128.96/129.85 (assume-push @p676 @t376) % 128.96/129.85 (assume-push @p677 @t379) % 128.96/129.85 (assume-push @p678 @t373) % 128.96/129.85 (assume-push @p679 @t376) % 128.96/129.85 (assume-push @p680 @t231) % 128.96/129.85 (assume-push @p681 @t379) % 128.96/129.85 (step @p96 :rule refl :args (@t227)) % 128.96/129.85 (step @p346 :rule symm :premises (@p54)) % 128.96/129.85 (step @p382 :rule cong :premises (@p346 @p96) :args (@t374)) % 128.96/129.85 (step @p344 :rule refl :args (@t191)) % 128.96/129.85 (step @p383 :rule cong :premises (@p344 @p382) :args (@t375)) % 128.96/129.85 (step @p384 :rule symm :premises (@p52)) % 128.96/129.85 (step @p97 :rule refl :args (@t229)) % 128.96/129.85 (step @p385 :rule cong :premises (@p54 @p97) :args (@t289)) % 128.96/129.85 (step @p386 :rule cong :premises (@p344 @p385) :args (@t290)) % 128.96/129.85 (step @p387 :rule trans :premises (@p386 @p384 @p674 @p53 @p383)) % 128.96/129.85 (step-pop @p682 :rule scope :premises (@p387)) % 128.96/129.85 (step-pop @p683 :rule scope :premises (@p682)) % 128.96/129.85 (step-pop @p684 :rule scope :premises (@p683)) % 128.96/129.85 (step-pop @p685 :rule scope :premises (@p684)) % 128.96/129.85 (step @p388 :rule process_scope :premises (@p685) :args (@t291)) % 128.96/129.85 (step @p393 :rule and_intro :premises (@p54 @p53 @p674 @p52)) % 128.96/129.85 (step @p394 :rule modus_ponens :premises (@p393 @p388)) % 128.96/129.85 (step-pop @p686 :rule scope :premises (@p394)) % 128.96/129.85 (step-pop @p687 :rule scope :premises (@p686)) % 128.96/129.85 (step-pop @p688 :rule scope :premises (@p687)) % 128.96/129.85 (step-pop @p689 :rule scope :premises (@p688)) % 128.96/129.85 (step @p395 :rule process_scope :premises (@p689) :args (@t291)) % 128.96/129.85 (step @p400 :rule implies_elim :premises (@p395)) % 128.96/129.85 (step @p401 :rule cnf_and_neg :args (@t388)) % 128.96/129.85 (step @p402 :rule resolution :premises (@p401 @p400) :args (true @t388)) % 128.96/129.85 (step @p403 :rule reordering :premises (@p402) :args ((or (not @t231) @t291 @t384 @t382 @t381))) % 128.96/129.85 (step @p404 :rule chain_m_resolution :premises (@p403 @p373 @p54 @p53 @p52) :args (@t291 (@list false false false false) (@list @t231 @t373 @t376 @t379))) % 128.96/129.85 (step @p405 :rule cnf_and_pos :args (@t240 1)) % 128.96/129.85 (step @p406 :rule reordering :premises (@p405) :args ((or @t235 @t386))) % 128.96/129.85 (step @p407 :rule chain_m_resolution :premises (@p406 @p370) :args (@t235 @t310 @t387)) % 128.96/129.85 (assume-push @p690 @t235) % 128.96/129.85 (assume-push @p691 @t253) % 128.96/129.85 (assume-push @p692 @t309) % 128.96/129.85 (assume-push @p693 @t349) % 128.96/129.85 (assume-push @p694 @t352) % 128.96/129.85 (assume-push @p695 @t345) % 128.96/129.85 (assume-push @p696 @t355) % 128.96/129.85 (assume-push @p697 @t358) % 128.96/129.85 (assume-push @p698 @t235) % 128.96/129.85 (assume-push @p699 @t349) % 128.96/129.85 (assume-push @p700 @t352) % 128.96/129.85 (assume-push @p701 @t355) % 128.96/129.85 (assume-push @p702 @t309) % 128.96/129.85 (assume-push @p703 @t253) % 128.96/129.85 (assume-push @p704 @t358) % 128.96/129.85 (assume-push @p705 @t345) % 128.96/129.85 (step @p424 :rule true_intro :premises (@p690)) % 128.96/129.85 (step @p425 :rule symm :premises (@p261)) % 128.96/129.85 (step @p426 :rule symm :premises (@p262)) % 128.96/129.85 (step @p427 :rule cong :premises (@p426) :args (@t353)) % 128.96/129.85 (step @p94 :rule refl :args (tptp.tyop_2Emin_2Ebool)) % 128.96/129.85 (step @p428 :rule cong :premises (@p94 @p427) :args (@t354)) % 128.96/129.85 (step @p96 :rule refl :args (@t227)) % 128.96/129.85 (step @p217 :rule cong :premises (@p187 @p77) :args (@t302)) % 128.96/129.85 (step @p220 :rule symm :premises (@p217)) % 128.96/129.85 (step @p215 :rule refl :args (@t306)) % 128.96/129.85 (step @p429 :rule cong :premises (@p215 @p77) :args (@t322)) % 128.96/129.85 (step @p430 :rule trans :premises (@p429 @p220)) % 128.96/129.85 (step @p99 :rule refl :args (@t198)) % 128.96/129.85 (step @p431 :rule cong :premises (@p99 @p430) :args (@t323)) % 128.96/129.85 (step @p432 :rule cong :premises (@p431 @p96) :args (@t356)) % 128.96/129.85 (step @p433 :rule cong :premises (@p94 @p432) :args (@t357)) % 128.96/129.85 (step @p206 :rule symm :premises (@p77)) % 128.96/129.85 (step @p292 :rule cong :premises (@p206 @p96) :args (@t359)) % 128.96/129.85 (step @p293 :rule cong :premises (@p99 @p292) :args (@t360)) % 128.96/129.85 (step @p294 :rule cong :premises (@p293 @p96) :args (@t361)) % 128.96/129.85 (step @p295 :rule cong :premises (@p94 @p294) :args (@t362)) % 128.96/129.85 (step @p434 :rule trans :premises (@p295 @p272 @p274 @p433 @p273 @p428 @p425)) % 128.96/129.85 (step @p435 :rule cong :premises (@p434) :args (@t363)) % 128.96/129.85 (step @p436 :rule cong :premises (@p435) :args (@t364)) % 128.96/129.85 (step @p437 :rule trans :premises (@p436 @p424)) % 128.96/129.85 (step @p438 :rule true_elim :premises (@p437)) % 128.96/129.85 (step-pop @p706 :rule scope :premises (@p438)) % 128.96/129.85 (step-pop @p707 :rule scope :premises (@p706)) % 128.96/129.85 (step-pop @p708 :rule scope :premises (@p707)) % 128.96/129.85 (step-pop @p709 :rule scope :premises (@p708)) % 128.96/129.85 (step-pop @p710 :rule scope :premises (@p709)) % 128.96/129.85 (step-pop @p711 :rule scope :premises (@p710)) % 128.96/129.85 (step-pop @p712 :rule scope :premises (@p711)) % 128.96/129.85 (step-pop @p713 :rule scope :premises (@p712)) % 128.96/129.85 (step @p439 :rule process_scope :premises (@p713) :args (@t364)) % 128.96/129.85 (step @p448 :rule and_intro :premises (@p690 @p261 @p262 @p273 @p187 @p77 @p274 @p272)) % 128.96/129.85 (step @p449 :rule modus_ponens :premises (@p448 @p439)) % 128.96/129.85 (step-pop @p714 :rule scope :premises (@p449)) % 128.96/129.85 (step-pop @p715 :rule scope :premises (@p714)) % 128.96/129.85 (step-pop @p716 :rule scope :premises (@p715)) % 128.96/129.85 (step-pop @p717 :rule scope :premises (@p716)) % 128.96/129.85 (step-pop @p718 :rule scope :premises (@p717)) % 128.96/129.85 (step-pop @p719 :rule scope :premises (@p718)) % 128.96/129.85 (step-pop @p720 :rule scope :premises (@p719)) % 128.96/129.85 (step-pop @p721 :rule scope :premises (@p720)) % 128.96/129.85 (step @p450 :rule process_scope :premises (@p721) :args (@t364)) % 128.96/129.85 (step @p459 :rule implies_elim :premises (@p450)) % 128.96/129.85 (step @p460 :rule cnf_and_neg :args (@t389)) % 128.96/129.85 (step @p461 :rule resolution :premises (@p460 @p459) :args (true @t389)) % 128.96/129.85 (step @p462 :rule reordering :premises (@p461) :args ((or (not @t235) @t340 @t364 @t336 @t370 @t369 @t368 @t367 @t366))) % 128.96/129.85 (step @p463 :rule chain_m_resolution :premises (@p462 @p407 @p77 @p187 @p261 @p262 @p272 @p273 @p274) :args (@t364 @t390 (@list @t235 @t253 @t309 @t349 @t352 @t345 @t355 @t358))) % 128.96/129.85 (step @p464 :rule cnf_and_pos :args (@t240 0)) % 128.96/129.85 (step @p465 :rule reordering :premises (@p464) :args ((or @t239 @t386))) % 128.96/129.85 (step @p466 :rule chain_m_resolution :premises (@p465 @p370) :args (@t239 @t310 @t387)) % 128.96/129.85 (assume-push @p722 @t239) % 128.96/129.85 (assume-push @p723 @t313) % 128.96/129.85 (assume-push @p724 @t253) % 128.96/129.85 (assume-push @p725 @t316) % 128.96/129.85 (assume-push @p726 @t319) % 128.96/129.85 (assume-push @p727 @t321) % 128.96/129.85 (assume-push @p728 @t309) % 128.96/129.85 (assume-push @p729 @t326) % 128.96/129.85 (assume-push @p730 @t239) % 128.96/129.85 (assume-push @p731 @t313) % 128.96/129.85 (assume-push @p732 @t316) % 128.96/129.85 (assume-push @p733 @t319) % 128.96/129.85 (assume-push @p734 @t309) % 128.96/129.85 (assume-push @p735 @t253) % 128.96/129.85 (assume-push @p736 @t326) % 128.96/129.85 (assume-push @p737 @t321) % 128.96/129.85 (step @p483 :rule true_intro :premises (@p722)) % 128.96/129.85 (step @p484 :rule symm :premises (@p171)) % 128.96/129.85 (step @p485 :rule symm :premises (@p172)) % 128.96/129.85 (step @p486 :rule cong :premises (@p485) :args (@t317)) % 128.96/129.85 (step @p94 :rule refl :args (tptp.tyop_2Emin_2Ebool)) % 128.96/129.85 (step @p487 :rule cong :premises (@p94 @p486) :args (@t318)) % 128.96/129.85 (step @p97 :rule refl :args (@t229)) % 128.96/129.85 (step @p217 :rule cong :premises (@p187 @p77) :args (@t302)) % 128.96/129.85 (step @p220 :rule symm :premises (@p217)) % 128.96/129.85 (step @p99 :rule refl :args (@t198)) % 128.96/129.85 (step @p221 :rule cong :premises (@p99 @p220) :args (@t332)) % 128.96/129.85 (step @p488 :rule cong :premises (@p221 @p97) :args (@t333)) % 128.96/129.85 (step @p224 :rule symm :premises (@p221)) % 128.96/129.85 (step @p215 :rule refl :args (@t306)) % 128.96/129.85 (step @p429 :rule cong :premises (@p215 @p77) :args (@t322)) % 128.96/129.85 (step @p430 :rule trans :premises (@p429 @p220)) % 128.96/129.85 (step @p431 :rule cong :premises (@p99 @p430) :args (@t323)) % 128.96/129.85 (step @p489 :rule trans :premises (@p431 @p224)) % 128.96/129.85 (step @p490 :rule cong :premises (@p489 @p97) :args (@t324)) % 128.96/129.85 (step @p491 :rule trans :premises (@p490 @p488)) % 128.96/129.85 (step @p492 :rule cong :premises (@p94 @p491) :args (@t325)) % 128.96/129.86 (step @p493 :rule symm :premises (@p174)) % 128.96/129.86 (step @p494 :rule trans :premises (@p493 @p188 @p492 @p173 @p487 @p484)) % 128.96/129.86 (step @p495 :rule cong :premises (@p494) :args (@t295)) % 128.96/129.86 (step @p206 :rule symm :premises (@p77)) % 128.96/129.86 (step @p207 :rule cong :premises (@p206 @p97) :args (@t249)) % 128.96/129.86 (step @p208 :rule cong :premises (@p99 @p207) :args (@t250)) % 128.96/129.86 (step @p209 :rule cong :premises (@p208 @p97) :args (@t327)) % 128.96/129.86 (step @p210 :rule cong :premises (@p94 @p209) :args (@t328)) % 128.96/129.86 (step @p211 :rule cong :premises (@p210) :args (@t329)) % 128.96/129.86 (step @p496 :rule trans :premises (@p211 @p495)) % 128.96/129.86 (step @p497 :rule cong :premises (@p496) :args (@t330)) % 128.96/129.86 (step @p498 :rule trans :premises (@p497 @p483)) % 128.96/129.86 (step @p499 :rule true_elim :premises (@p498)) % 128.96/129.86 (step-pop @p738 :rule scope :premises (@p499)) % 128.96/129.86 (step-pop @p739 :rule scope :premises (@p738)) % 128.96/129.86 (step-pop @p740 :rule scope :premises (@p739)) % 128.96/129.86 (step-pop @p741 :rule scope :premises (@p740)) % 128.96/129.86 (step-pop @p742 :rule scope :premises (@p741)) % 128.96/129.86 (step-pop @p743 :rule scope :premises (@p742)) % 128.96/129.86 (step-pop @p744 :rule scope :premises (@p743)) % 128.96/129.86 (step-pop @p745 :rule scope :premises (@p744)) % 128.96/129.86 (step @p500 :rule process_scope :premises (@p745) :args (@t330)) % 128.96/129.86 (step @p509 :rule and_intro :premises (@p722 @p171 @p172 @p173 @p187 @p77 @p188 @p174)) % 128.96/129.86 (step @p510 :rule modus_ponens :premises (@p509 @p500)) % 128.96/129.86 (step-pop @p746 :rule scope :premises (@p510)) % 128.96/129.86 (step-pop @p747 :rule scope :premises (@p746)) % 128.96/129.86 (step-pop @p748 :rule scope :premises (@p747)) % 128.96/129.86 (step-pop @p749 :rule scope :premises (@p748)) % 128.96/129.86 (step-pop @p750 :rule scope :premises (@p749)) % 128.96/129.86 (step-pop @p751 :rule scope :premises (@p750)) % 128.96/129.86 (step-pop @p752 :rule scope :premises (@p751)) % 128.96/129.86 (step-pop @p753 :rule scope :premises (@p752)) % 128.96/129.86 (step @p511 :rule process_scope :premises (@p753) :args (@t330)) % 128.96/129.86 (step @p520 :rule implies_elim :premises (@p511)) % 128.96/129.86 (step @p521 :rule cnf_and_neg :args (@t391)) % 128.96/129.86 (step @p522 :rule resolution :premises (@p521 @p520) :args (true @t391)) % 128.96/129.86 (step @p523 :rule reordering :premises (@p522) :args ((or (not @t239) @t341 @t340 @t339 @t338 @t330 @t337 @t336 @t335))) % 128.96/129.86 (step @p524 :rule chain_m_resolution :premises (@p523 @p466 @p171 @p77 @p172 @p173 @p174 @p187 @p188) :args (@t330 @t390 (@list @t239 @t313 @t253 @t316 @t319 @t321 @t309 @t326))) % 128.96/129.86 (step @p525 :rule instantiate :premises (@p127) :args ((@list @t182 @t191 @t247 @t268 @t267))) % 128.96/129.86 (step @p526 :rule true_intro :premises (@p158)) % 128.96/129.86 (step @p527 :rule refl :args (@t275)) % 128.96/129.86 (step @p528 :rule refl :args (@t276)) % 128.96/129.86 (step @p206 :rule symm :premises (@p77)) % 128.96/129.86 (step @p529 :rule cong :premises (@p206 @p528 @p527) :args (@t392)) % 128.96/129.86 (step @p94 :rule refl :args (tptp.tyop_2Emin_2Ebool)) % 128.96/129.86 (step @p530 :rule cong :premises (@p94 @p529) :args (@t393)) % 128.96/129.86 (step @p531 :rule cong :premises (@p530) :args (@t394)) % 128.96/129.86 (step @p532 :rule cong :premises (@p531) :args (@t395)) % 128.96/129.86 (step @p533 :rule trans :premises (@p532 @p526)) % 128.96/129.86 (step @p534 :rule true_elim :premises (@p533)) % 128.96/129.86 (step @p535 :rule cnf_or_pos :args (@t399)) % 128.96/129.86 (step @p536 :rule reordering :premises (@p535) :args ((or @t398 @t397 (not @t399)))) % 128.96/129.86 (step @p537 :rule chain_m_resolution :premises (@p536 @p534 @p525) :args (@t397 @t274 (@list @t395 @t399))) % 128.96/129.86 (step @p538 :rule instantiate :premises (@p537) :args (@t286)) % 128.96/129.86 (step @p539 :rule refl :args (@t401)) % 128.96/129.86 (step @p540 :rule refl :args (@t402)) % 128.96/129.86 (step @p541 :rule bool-double-not-elim :args (@t244)) % 128.96/129.86 (step @p542 :rule nary_cong :premises (@p541 @p540 @p539) :args ((or (not @t385) @t402 @t401))) % 128.96/129.86 (assume-push @p754 @t385) % 128.96/129.86 (assume-push @p755 @t256) % 128.96/129.86 (assume-push @p756 @t385) % 128.96/129.86 (assume-push @p757 @t256) % 128.96/129.86 (step @p547 :rule false_intro :premises (@p754)) % 128.96/129.86 (step @p92 :rule symm :premises (@p78)) % 128.96/129.86 (step @p548 :rule cong :premises (@p92) :args (@t400)) % 128.96/129.86 (step @p549 :rule trans :premises (@p548 @p547)) % 128.96/129.86 (step @p550 :rule false_elim :premises (@p549)) % 128.96/129.86 (step-pop @p758 :rule scope :premises (@p550)) % 128.96/129.86 (step-pop @p759 :rule scope :premises (@p758)) % 128.96/129.86 (step @p551 :rule process_scope :premises (@p759) :args (@t401)) % 128.96/129.86 (step @p554 :rule and_intro :premises (@p754 @p78)) % 128.96/129.86 (step @p555 :rule modus_ponens :premises (@p554 @p551)) % 128.96/129.86 (step-pop @p760 :rule scope :premises (@p555)) % 128.96/129.86 (step-pop @p761 :rule scope :premises (@p760)) % 128.96/129.86 (step @p556 :rule process_scope :premises (@p761) :args (@t401)) % 128.96/129.86 (step @p559 :rule implies_elim :premises (@p556)) % 128.96/129.86 (step @p560 :rule cnf_and_neg :args (@t403)) % 128.96/129.86 (step @p561 :rule resolution :premises (@p560 @p559) :args (true @t403)) % 128.96/129.86 (step @p562 :rule eq_resolve :premises (@p561 @p542)) % 128.96/129.86 (step @p563 :rule chain_m_resolution :premises (@p562 @p367 @p78) :args (@t401 @t404 (@list @t244 @t256))) % 128.96/129.86 (step @p564 :rule cnf_equiv_pos2 :args (@t406)) % 128.96/129.86 (step @p565 :rule reordering :premises (@p564) :args ((or @t400 @t407 (not @t406)))) % 128.96/129.86 (step @p566 :rule chain_m_resolution :premises (@p565 @p563 @p538) :args (@t407 @t404 (@list @t400 @t406))) % 128.96/129.86 (step @p567 :rule cnf_and_neg :args (@t405)) % 128.96/129.86 (step @p568 :rule reordering :premises (@p567) :args ((or @t405 @t383 (not @t330) (not @t364)))) % 128.96/129.86 (step @p569 false :rule chain_m_resolution :premises (@p568 @p566 @p524 @p463 @p404) :args (false (@list true false false false) (@list @t405 @t330 @t364 @t291))) % 128.96/129.86 ) % 128.96/129.86 % SZS output end Proof % 128.96/129.86 % cvc5 exiting %------------------------------------------------------------------------------