%------------------------------------------------------------------------------ % File : cvc5---1.3.4 % Problem : ITP001_4 : 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 : n020.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:20 AM UTC 2026 % Result : Theorem 0.40s 0.63s % Output : Proof 0.40s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : ITP001_4 : 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.15/0.34 % Computer : n020.cluster.edu % 0.15/0.34 % Model : x86_64 x86_64 % 0.15/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.15/0.34 % Memory : 8042.1875MB % 0.15/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.15/0.34 % CPULimit : 300 % 0.15/0.34 % WCLimit : 300 % 0.15/0.34 % DateTime : Tue Jun 2 03:33:10 EDT 2026 % 0.15/0.34 % CPUTime : % 0.30/0.54 %----Proving TF0_NAR, FOF, or CNF % 0.40/0.63 --- Run --decision=internal --simplification=none --no-inst-no-entail --no-cbqi --full-saturate-quant at 15... % 0.40/0.63 % SZS status Theorem % 0.40/0.63 % SZS output start Proof % 0.40/0.63 ( % 0.40/0.63 (declare-sort tptp.mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Eind_2Ctyop_2Emin_2Eind_29 0) % 0.40/0.63 (declare-sort tptp.mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Efun_28tyop_2Emin_2Eind_2Ctyop_2Emin_2Eind_29_2Ctyop_2Emin_2Ebool_29 0) % 0.40/0.63 (declare-sort tptp.mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29_29 0) % 0.40/0.63 (declare-sort tptp.mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29 0) % 0.40/0.63 (declare-sort tptp.mono_2Etyop_2Emin_2Ebool 0) % 0.40/0.63 (declare-sort tptp.d 0) % 0.40/0.63 (declare-sort tptp.u 0) % 0.40/0.63 (declare-sort tptp.du 0) % 0.40/0.63 (declare-const tptp.c_2Ebool_2Eliteral__case_2E2 (-> tptp.du tptp.du tptp.u)) % 0.40/0.63 (declare-const tptp.c_2Ebool_2Eliteral__case_2E0 tptp.u) % 0.40/0.63 (declare-const tptp.c_2Ebool_2ETYPE__DEFINITION_2E2 (-> tptp.du tptp.du tptp.u)) % 0.40/0.63 (declare-const tptp.c_2Ebool_2ETYPE__DEFINITION_2E0 tptp.u) % 0.40/0.63 (declare-const tptp.c_2Ebool_2ERES__FORALL_2E2 (-> tptp.du tptp.du tptp.u)) % 0.40/0.63 (declare-const tptp.c_2Ebool_2ERES__FORALL_2E0 tptp.u) % 0.40/0.63 (declare-const tptp.c_2Ebool_2ERES__EXISTS_2E2 (-> tptp.du tptp.du tptp.u)) % 0.40/0.63 (declare-const tptp.c_2Ebool_2ERES__EXISTS_2E0 tptp.u) % 0.40/0.63 (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) % 0.40/0.63 (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)) % 0.40/0.63 (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)) % 0.40/0.63 (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)) % 0.40/0.63 (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)) % 0.40/0.63 (declare-const tptp.c_2Emin_2E_40_2E0 tptp.u) % 0.40/0.63 (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)) % 0.40/0.63 (declare-const tptp.c_2Ebool_2ERES__EXISTS__UNIQUE_2E0 tptp.u) % 0.40/0.63 (declare-const tptp.c_2Emin_2E_3D_2E0 tptp.u) % 0.40/0.63 (declare-const tptp.i_mono_2Etyop_2Emin_2Ebool (-> tptp.mono_2Etyop_2Emin_2Ebool tptp.u)) % 0.40/0.63 (declare-const tptp.c_2Ebool_2E_3F_21_2E0 tptp.u) % 0.40/0.63 (declare-const tptp.c_2Ebool_2ERES__SELECT_2E2 (-> tptp.du tptp.du tptp.u)) % 0.40/0.63 (declare-const tptp.c_2Ebool_2E_3F_2E1 (-> tptp.du tptp.u)) % 0.40/0.63 (declare-const tptp.mono_2Ec_2Ebool_2EONE__ONE_2E0_2Emono_2Etyop_2Emin_2Eind_20mono_2Etyop_2Emin_2Eind tptp.mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Efun_28tyop_2Emin_2Eind_2Ctyop_2Emin_2Eind_29_2Ctyop_2Emin_2Ebool_29) % 0.40/0.63 (declare-const tptp.j_mono_2Etyop_2Emin_2Ebool (-> tptp.du tptp.mono_2Etyop_2Emin_2Ebool)) % 0.40/0.63 (declare-const tptp.tyop_2Emin_2Ebool tptp.d) % 0.40/0.63 (declare-const tptp.c_2Ebool_2ERES__EXISTS__UNIQUE_2E2 (-> tptp.du tptp.du tptp.u)) % 0.40/0.63 (declare-const tptp.c_2Emin_2E_3D_2E2 (-> tptp.du tptp.du tptp.u)) % 0.40/0.63 (declare-const tptp.c_2Ebool_2ECOND_2E0 tptp.u) % 0.40/0.63 (declare-const tptp.tyop_2Emin_2Efun (-> tptp.d tptp.d tptp.d)) % 0.40/0.63 (declare-const tptp.j_mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Efun_28tyop_2Emin_2Eind_2Ctyop_2Emin_2Eind_29_2Ctyop_2Emin_2Ebool_29 (-> tptp.du tptp.mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Efun_28tyop_2Emin_2Eind_2Ctyop_2Emin_2Eind_29_2Ctyop_2Emin_2Ebool_29)) % 0.40/0.63 (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)) % 0.40/0.63 (declare-const tptp.c_2Ebool_2ECOND_2E3 (-> tptp.du tptp.du tptp.du tptp.u)) % 0.40/0.63 (declare-const tptp.s (-> tptp.d tptp.u tptp.du)) % 0.40/0.63 (declare-const tptp.c_2Ebool_2EONTO_2E0 tptp.u) % 0.40/0.63 (declare-const tptp.mono_2Ec_2Ebool_2EF_2E0 tptp.mono_2Etyop_2Emin_2Ebool) % 0.40/0.63 (declare-const tptp.c_2Ebool_2ELET_2E0 tptp.u) % 0.40/0.63 (declare-const tptp.combin_i_2E0 tptp.u) % 0.40/0.63 (declare-const tptp.c_2Ebool_2EDATATYPE_2E1 (-> tptp.du tptp.u)) % 0.40/0.63 (declare-const tptp.app_2E2 (-> tptp.du tptp.du tptp.u)) % 0.40/0.63 (declare-const tptp.mono_2Ec_2Ebool_2EONTO_2E1_2Emono_2Etyop_2Emin_2Eind_20mono_2Etyop_2Emin_2Eind (-> tptp.mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Eind_2Ctyop_2Emin_2Eind_29 tptp.mono_2Etyop_2Emin_2Ebool)) % 0.40/0.63 (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)) % 0.40/0.63 (declare-const tptp.i_mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Eind_2Ctyop_2Emin_2Eind_29 (-> tptp.mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Eind_2Ctyop_2Emin_2Eind_29 tptp.u)) % 0.40/0.63 (declare-const tptp.mono_2Ec_2Ebool_2ET_2E0 tptp.mono_2Etyop_2Emin_2Ebool) % 0.40/0.63 (declare-const tptp.c_2Ebool_2EONE__ONE_2E0 tptp.u) % 0.40/0.63 (declare-const tptp.combin_s_2E0 tptp.u) % 0.40/0.63 (declare-const tptp.mono_2Ec_2Ebool_2E_7E_2E1 (-> tptp.mono_2Etyop_2Emin_2Ebool tptp.mono_2Etyop_2Emin_2Ebool)) % 0.40/0.63 (declare-const tptp.c_2Ebool_2ERES__SELECT_2E0 tptp.u) % 0.40/0.63 (declare-const tptp.c_2Ebool_2E_3F_2E0 tptp.u) % 0.40/0.63 (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)) % 0.40/0.63 (declare-const tptp.mono_2Ec_2Ebool_2EBOUNDED_2E1 (-> tptp.mono_2Etyop_2Emin_2Ebool tptp.mono_2Etyop_2Emin_2Ebool)) % 0.40/0.63 (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) % 0.40/0.63 (declare-const tptp.mono_2Ec_2Ebool_2E_7E_2E0 tptp.mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29) % 0.40/0.63 (declare-const tptp.tyop_2Emin_2Eind tptp.d) % 0.40/0.63 (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)) % 0.40/0.63 (declare-const tptp.i_mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Efun_28tyop_2Emin_2Eind_2Ctyop_2Emin_2Eind_29_2Ctyop_2Emin_2Ebool_29 (-> tptp.mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Efun_28tyop_2Emin_2Eind_2Ctyop_2Emin_2Eind_29_2Ctyop_2Emin_2Ebool_29 tptp.u)) % 0.40/0.63 (declare-const tptp.j_mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Eind_2Ctyop_2Emin_2Eind_29 (-> tptp.du tptp.mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Eind_2Ctyop_2Emin_2Eind_29)) % 0.40/0.63 (declare-const tptp.c_2Ebool_2E_3F_21_2E1 (-> tptp.du tptp.u)) % 0.40/0.63 (declare-const tptp.c_2Emin_2E_40_2E1 (-> tptp.du tptp.u)) % 0.40/0.63 (declare-const tptp.mono_2Ec_2Ebool_2EBOUNDED_2E0 tptp.mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29) % 0.40/0.63 (declare-const tptp.c_2Ebool_2EDATATYPE_2E0 tptp.u) % 0.40/0.63 (declare-const tptp.c_2Ebool_2EIN_2E0 tptp.u) % 0.40/0.63 (declare-const tptp.p (-> tptp.mono_2Etyop_2Emin_2Ebool Bool)) % 0.40/0.63 (declare-const tptp.c_2Ebool_2EIN_2E2 (-> tptp.du tptp.du tptp.u)) % 0.40/0.63 (declare-const tptp.combin_k_2E0 tptp.u) % 0.40/0.63 (declare-const tptp.c_2Ebool_2ELET_2E2 (-> tptp.du tptp.du tptp.u)) % 0.40/0.63 (declare-const tptp.c_2Ebool_2E_21_2E0 tptp.u) % 0.40/0.63 (declare-const tptp.c_2Ebool_2EONE__ONE_2E1 (-> tptp.du tptp.u)) % 0.40/0.63 (declare-const tptp.mono_2Eapp_2E2_2Emono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Eind_2Ctyop_2Emin_2Eind_29_20mono_2Etyop_2Emin_2Ebool (-> tptp.mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Efun_28tyop_2Emin_2Eind_2Ctyop_2Emin_2Eind_29_2Ctyop_2Emin_2Ebool_29 tptp.mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Eind_2Ctyop_2Emin_2Eind_29 tptp.mono_2Etyop_2Emin_2Ebool)) % 0.40/0.63 (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) % 0.40/0.63 (declare-const tptp.mono_2Ec_2Ebool_2EONE__ONE_2E1_2Emono_2Etyop_2Emin_2Eind_20mono_2Etyop_2Emin_2Eind (-> tptp.mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Eind_2Ctyop_2Emin_2Eind_29 tptp.mono_2Etyop_2Emin_2Ebool)) % 0.40/0.63 (declare-const tptp.c_2Ebool_2E_21_2E1 (-> tptp.du tptp.u)) % 0.40/0.63 (declare-const tptp.c_2Ebool_2EONTO_2E1 (-> tptp.du tptp.u)) % 0.40/0.63 (declare-const tptp.mono_2Ec_2Ebool_2EONTO_2E0_2Emono_2Etyop_2Emin_2Eind_20mono_2Etyop_2Emin_2Eind tptp.mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Efun_28tyop_2Emin_2Eind_2Ctyop_2Emin_2Eind_29_2Ctyop_2Emin_2Ebool_29) % 0.40/0.63 (define @t1 () (@var "V1g_2E0" tptp.u)) % 0.40/0.63 (define @t2 () (@var "A_27b" tptp.d)) % 0.40/0.63 (define @t3 () (@var "A_27a" tptp.d)) % 0.40/0.63 (define @t4 () (tptp.tyop_2Emin_2Efun @t3 @t2)) % 0.40/0.63 (define @t5 () (tptp.s @t4 @t1)) % 0.40/0.63 (define @t6 () (@var "V0f_2E0" tptp.u)) % 0.40/0.63 (define @t7 () (tptp.s @t4 @t6)) % 0.40/0.63 (define @t8 () (@var "V2x_2E0" tptp.u)) % 0.40/0.63 (define @t9 () (tptp.s @t3 @t8)) % 0.40/0.63 (define @t10 () (tptp.s @t2 (tptp.app_2E2 @t5 @t9))) % 0.40/0.63 (define @t11 () (@list @t8)) % 0.40/0.63 (define @t12 () (@var "V1_2E0" tptp.mono_2Etyop_2Emin_2Ebool)) % 0.40/0.63 (define @t13 () (@var "V0_2E0" tptp.mono_2Etyop_2Emin_2Ebool)) % 0.40/0.63 (define @t14 () (tptp.p @t12)) % 0.40/0.63 (define @t15 () (tptp.p @t13)) % 0.40/0.63 (define @t16 () (@list @t13 @t12)) % 0.40/0.63 (define @t17 () (tptp.p tptp.mono_2Ec_2Ebool_2ET_2E0)) % 0.40/0.63 (define @t18 () (tptp.p tptp.mono_2Ec_2Ebool_2EF_2E0)) % 0.40/0.63 (define @t19 () (@var "V0t_2E0" tptp.mono_2Etyop_2Emin_2Ebool)) % 0.40/0.63 (define @t20 () (@list @t19)) % 0.40/0.63 (define @t21 () (@var "V0x_2E0" tptp.u)) % 0.40/0.63 (define @t22 () (tptp.s @t3 @t21)) % 0.40/0.63 (define @t23 () (tptp.tyop_2Emin_2Efun @t3 @t3)) % 0.40/0.63 (define @t24 () (@list @t3 @t21)) % 0.40/0.63 (define @t25 () (@var "V1y_2E0" tptp.u)) % 0.40/0.63 (define @t26 () (tptp.s @t2 @t25)) % 0.40/0.63 (define @t27 () (tptp.tyop_2Emin_2Efun @t2 @t3)) % 0.40/0.63 (define @t28 () (@var "A_27c" tptp.d)) % 0.40/0.63 (define @t29 () (tptp.tyop_2Emin_2Efun @t2 @t28)) % 0.40/0.63 (define @t30 () (tptp.tyop_2Emin_2Efun @t3 @t29)) % 0.40/0.63 (define @t31 () (tptp.s @t30 @t6)) % 0.40/0.63 (define @t32 () (tptp.tyop_2Emin_2Efun @t3 @t28)) % 0.40/0.63 (define @t33 () (tptp.tyop_2Emin_2Efun @t4 @t32)) % 0.40/0.63 (define @t34 () (@list @t13)) % 0.40/0.63 (define @t35 () (@var "V1_2E0" tptp.u)) % 0.40/0.63 (define @t36 () (tptp.s @t3 @t35)) % 0.40/0.63 (define @t37 () (@var "V0_2E0" tptp.u)) % 0.40/0.63 (define @t38 () (tptp.s @t3 @t37)) % 0.40/0.63 (define @t39 () (@var "V1x_2E0" tptp.u)) % 0.40/0.63 (define @t40 () (tptp.s @t3 @t39)) % 0.40/0.63 (define @t41 () (tptp.tyop_2Emin_2Efun @t3 tptp.tyop_2Emin_2Ebool)) % 0.40/0.63 (define @t42 () (tptp.s @t41 @t6)) % 0.40/0.63 (define @t43 () (tptp.p (tptp.j_mono_2Etyop_2Emin_2Ebool (tptp.s tptp.tyop_2Emin_2Ebool (tptp.app_2E2 @t42 @t40))))) % 0.40/0.63 (define @t44 () (@list @t39)) % 0.40/0.63 (define @t45 () (@list @t3 @t6)) % 0.40/0.63 (define @t46 () (tptp.s tptp.tyop_2Emin_2Ebool @t37)) % 0.40/0.63 (define @t47 () (@list @t37)) % 0.40/0.63 (define @t48 () (tptp.tyop_2Emin_2Efun tptp.tyop_2Emin_2Ebool tptp.tyop_2Emin_2Ebool)) % 0.40/0.63 (define @t49 () (tptp.s @t48 @t37)) % 0.40/0.63 (define @t50 () (tptp.tyop_2Emin_2Efun tptp.tyop_2Emin_2Ebool @t48)) % 0.40/0.63 (define @t51 () (tptp.s @t50 @t37)) % 0.40/0.63 (define @t52 () (@var "V0_2E0" tptp.mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29)) % 0.40/0.63 (define @t53 () (tptp.s @t48 (tptp.i_mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29 @t52))) % 0.40/0.63 (define @t54 () (@var "V0_2E0" tptp.mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29_29)) % 0.40/0.63 (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))) % 0.40/0.63 (define @t56 () (@var "X0_2E0" tptp.u)) % 0.40/0.63 (define @t57 () (tptp.s @t41 @t56)) % 0.40/0.63 (define @t58 () (tptp.tyop_2Emin_2Efun @t41 tptp.tyop_2Emin_2Ebool)) % 0.40/0.63 (define @t59 () (@list @t3 @t56)) % 0.40/0.63 (define @t60 () (@var "X1_2E0" tptp.mono_2Etyop_2Emin_2Ebool)) % 0.40/0.63 (define @t61 () (@var "X0_2E0" tptp.mono_2Etyop_2Emin_2Ebool)) % 0.40/0.63 (define @t62 () (tptp.p @t60)) % 0.40/0.63 (define @t63 () (tptp.p @t61)) % 0.40/0.63 (define @t64 () (@list @t61 @t60)) % 0.40/0.63 (define @t65 () (@var "X1_2E0" tptp.u)) % 0.40/0.63 (define @t66 () (tptp.s @t3 @t65)) % 0.40/0.63 (define @t67 () (tptp.s @t3 @t56)) % 0.40/0.63 (define @t68 () (tptp.tyop_2Emin_2Efun @t3 @t41)) % 0.40/0.63 (define @t69 () (@list @t3 @t56 @t65)) % 0.40/0.63 (define @t70 () (@list @t61)) % 0.40/0.63 (define @t71 () (tptp.s tptp.tyop_2Emin_2Ebool (tptp.i_mono_2Etyop_2Emin_2Ebool @t12))) % 0.40/0.63 (define @t72 () (tptp.tyop_2Emin_2Efun tptp.tyop_2Emin_2Eind tptp.tyop_2Emin_2Eind)) % 0.40/0.63 (define @t73 () (tptp.tyop_2Emin_2Efun @t72 tptp.tyop_2Emin_2Ebool)) % 0.40/0.63 (define @t74 () (tptp.s @t73 @t37)) % 0.40/0.63 (define @t75 () (tptp.s @t72 @t37)) % 0.40/0.63 (define @t76 () (@var "V0_2E0" tptp.mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Efun_28tyop_2Emin_2Eind_2Ctyop_2Emin_2Eind_29_2Ctyop_2Emin_2Ebool_29)) % 0.40/0.63 (define @t77 () (tptp.s @t73 (tptp.i_mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Efun_28tyop_2Emin_2Eind_2Ctyop_2Emin_2Eind_29_2Ctyop_2Emin_2Ebool_29 @t76))) % 0.40/0.63 (define @t78 () (@var "V0_2E0" tptp.mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Eind_2Ctyop_2Emin_2Eind_29)) % 0.40/0.63 (define @t79 () (tptp.s @t72 (tptp.i_mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Eind_2Ctyop_2Emin_2Eind_29 @t78))) % 0.40/0.63 (define @t80 () (@list @t78)) % 0.40/0.63 (define @t81 () (tptp.tyop_2Emin_2Efun @t41 @t3)) % 0.40/0.63 (define @t82 () (@var "X2_2E0" tptp.u)) % 0.40/0.63 (define @t83 () (tptp.s @t3 @t82)) % 0.40/0.63 (define @t84 () (tptp.s tptp.tyop_2Emin_2Ebool (tptp.i_mono_2Etyop_2Emin_2Ebool @t61))) % 0.40/0.63 (define @t85 () (tptp.tyop_2Emin_2Efun @t3 @t23)) % 0.40/0.63 (define @t86 () (tptp.s @t41 @t65)) % 0.40/0.63 (define @t87 () (tptp.s @t4 @t56)) % 0.40/0.63 (define @t88 () (tptp.tyop_2Emin_2Efun @t4 @t4)) % 0.40/0.63 (define @t89 () (@list @t3 @t2 @t56 @t65)) % 0.40/0.63 (define @t90 () (tptp.tyop_2Emin_2Efun @t4 tptp.tyop_2Emin_2Ebool)) % 0.40/0.63 (define @t91 () (@list @t3 @t2 @t56)) % 0.40/0.63 (define @t92 () (@var "X0_2E0" tptp.mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Eind_2Ctyop_2Emin_2Eind_29)) % 0.40/0.63 (define @t93 () (@list @t92)) % 0.40/0.63 (define @t94 () (tptp.tyop_2Emin_2Efun @t41 @t58)) % 0.40/0.63 (define @t95 () (tptp.s @t27 @t65)) % 0.40/0.63 (define @t96 () (tptp.tyop_2Emin_2Efun @t27 tptp.tyop_2Emin_2Ebool)) % 0.40/0.63 (define @t97 () (@var "V1_2E0" tptp.mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Eind_2Ctyop_2Emin_2Eind_29)) % 0.40/0.63 (define @t98 () (@var "V0M_2E0" tptp.u)) % 0.40/0.63 (define @t99 () (tptp.s @t2 (tptp.app_2E2 (tptp.s @t4 @t98) @t40))) % 0.40/0.63 (define @t100 () (@var "V0P_2E0" tptp.u)) % 0.40/0.63 (define @t101 () (tptp.s @t41 @t100)) % 0.40/0.63 (define @t102 () (@var "V0f_2E0" tptp.mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Eind_2Ctyop_2Emin_2Eind_29)) % 0.40/0.63 (define @t103 () (@var "V0x_2E0" tptp.mono_2Etyop_2Emin_2Ebool)) % 0.40/0.63 (define @t104 () (@list @t103)) % 0.40/0.63 (define @t105 () (tptp.s @t41 @t21)) % 0.40/0.63 (define @t106 () (tptp.j_mono_2Etyop_2Emin_2Ebool (tptp.s tptp.tyop_2Emin_2Ebool (tptp.app_2E2 @t105 @t40)))) % 0.40/0.63 (define @t107 () (tptp.j_mono_2Etyop_2Emin_2Ebool (tptp.s tptp.tyop_2Emin_2Ebool (tptp.c_2Ebool_2E_3F_2E1 @t105)))) % 0.40/0.63 (define @t108 () (@var "V2t_2E0" tptp.mono_2Etyop_2Emin_2Ebool)) % 0.40/0.63 (define @t109 () (tptp.p @t108)) % 0.40/0.63 (define @t110 () (@var "V1x_27_2E0" tptp.mono_2Etyop_2Emin_2Ebool)) % 0.40/0.63 (define @t111 () (tptp.p @t110)) % 0.40/0.63 (define @t112 () (=> @t111 @t109)) % 0.40/0.63 (define @t113 () (tptp.p @t103)) % 0.40/0.63 (define @t114 () (@list @t108)) % 0.40/0.63 (define @t115 () (@list @t103 @t110)) % 0.40/0.63 (define @t116 () (@var "V2y_2E0" tptp.u)) % 0.40/0.63 (define @t117 () (tptp.s @t3 @t116)) % 0.40/0.63 (define @t118 () (@var "V1x_27_2E0" tptp.u)) % 0.40/0.63 (define @t119 () (tptp.s @t3 @t118)) % 0.40/0.63 (define @t120 () (tptp.s @t4 @t21)) % 0.40/0.63 (define @t121 () (tptp.s @t2 (tptp.app_2E2 @t120 @t119))) % 0.40/0.63 (define @t122 () (@list @t3 @t2 @t21 @t118)) % 0.40/0.63 (define @t123 () (@var "V2x_27_27_2E0" tptp.u)) % 0.40/0.63 (define @t124 () (tptp.s @t3 @t123)) % 0.40/0.63 (define @t125 () (tptp.s tptp.tyop_2Emin_2Ebool (tptp.i_mono_2Etyop_2Emin_2Ebool @t103))) % 0.40/0.63 (define @t126 () (@var "F0_2E0" tptp.u)) % 0.40/0.63 (define @t127 () (tptp.tyop_2Emin_2Efun @t3 @t68)) % 0.40/0.63 (define @t128 () (tptp.s @t41 (tptp.app_2E2 (tptp.s @t68 (tptp.app_2E2 (tptp.s @t127 (tptp.app_2E2 (tptp.s (tptp.tyop_2Emin_2Efun tptp.tyop_2Emin_2Ebool @t127) @t126) @t125)) @t119)) @t124))) % 0.40/0.63 (define @t129 () (@var "V3x_2E0" tptp.u)) % 0.40/0.63 (define @t130 () (tptp.s @t3 @t129)) % 0.40/0.63 (define @t131 () (@list @t3 @t126)) % 0.40/0.63 (define @t132 () (@var "V2x2_2E0" tptp.u)) % 0.40/0.63 (define @t133 () (tptp.s @t3 @t132)) % 0.40/0.63 (define @t134 () (@var "V1x1_2E0" tptp.u)) % 0.40/0.63 (define @t135 () (tptp.s @t3 @t134)) % 0.40/0.63 (define @t136 () (@list @t3 @t2 @t21)) % 0.40/0.63 (define @t137 () (@var "V5x_27_2E0" tptp.u)) % 0.40/0.63 (define @t138 () (tptp.s @t27 @t118)) % 0.40/0.63 (define @t139 () (@var "V4x_2E0" tptp.u)) % 0.40/0.63 (define @t140 () (tptp.s @t3 @t139)) % 0.40/0.63 (define @t141 () (@var "V3x_27_27_2E0" tptp.u)) % 0.40/0.63 (define @t142 () (tptp.s @t2 @t141)) % 0.40/0.63 (define @t143 () (@var "V2x_27_2E0" tptp.u)) % 0.40/0.63 (define @t144 () (tptp.s @t2 @t143)) % 0.40/0.63 (define @t145 () (tptp.s @t41 @t118)) % 0.40/0.63 (define @t146 () (@list @t3 @t21 @t118)) % 0.40/0.63 (define @t147 () (tptp.j_mono_2Etyop_2Emin_2Ebool (tptp.s tptp.tyop_2Emin_2Ebool (tptp.app_2E2 @t145 @t9)))) % 0.40/0.63 (define @t148 () (tptp.p @t147)) % 0.40/0.63 (define @t149 () (tptp.p (tptp.j_mono_2Etyop_2Emin_2Ebool (tptp.s tptp.tyop_2Emin_2Ebool (tptp.c_2Ebool_2EIN_2E2 @t9 @t105))))) % 0.40/0.63 (define @t150 () (and @t149 @t148)) % 0.40/0.63 (define @t151 () (@var "F1_2E0" tptp.u)) % 0.40/0.63 (define @t152 () (tptp.tyop_2Emin_2Efun @t41 @t41)) % 0.40/0.63 (define @t153 () (tptp.tyop_2Emin_2Efun @t41 @t152)) % 0.40/0.63 (define @t154 () (tptp.s @t41 (tptp.app_2E2 (tptp.s @t152 (tptp.app_2E2 (tptp.s @t153 @t151) @t105)) @t145))) % 0.40/0.63 (define @t155 () (tptp.s @t41 (tptp.app_2E2 (tptp.s @t152 @t126) @t145))) % 0.40/0.63 (define @t156 () (@list @t21 @t118)) % 0.40/0.63 (define @t157 () (@var "F2_2E0" tptp.u)) % 0.40/0.63 (define @t158 () (tptp.s @t41 (tptp.app_2E2 (tptp.s @t68 (tptp.app_2E2 (tptp.s (tptp.tyop_2Emin_2Efun @t41 @t68) @t157) @t145)) @t130))) % 0.40/0.63 (define @t159 () (@var "V4y_2E0" tptp.u)) % 0.40/0.63 (define @t160 () (tptp.s @t3 @t159)) % 0.40/0.63 (define @t161 () (tptp.s @t41 (tptp.app_2E2 (tptp.s @t152 (tptp.app_2E2 (tptp.s @t153 @t126) @t105)) @t145))) % 0.40/0.63 (assume @p1 (forall (@list @t3 @t2 @t6 @t1) (=> (forall @t11 (= (tptp.s @t2 (tptp.app_2E2 @t7 @t9)) @t10)) (= @t7 @t5)))) % 0.40/0.63 (assume @p2 (forall @t16 (=> (= @t15 @t14) (= @t13 @t12)))) % 0.40/0.63 (assume @p3 @t17) % 0.40/0.63 (assume @p4 (not @t18)) % 0.40/0.63 (assume @p5 (forall @t20 (or (= @t19 tptp.mono_2Ec_2Ebool_2ET_2E0) (= @t19 tptp.mono_2Ec_2Ebool_2EF_2E0)))) % 0.40/0.63 (assume @p6 (forall @t24 (= (tptp.s @t3 (tptp.app_2E2 (tptp.s @t23 tptp.combin_i_2E0) @t22)) @t22))) % 0.40/0.63 (assume @p7 (forall (@list @t3 @t2 @t21 @t25) (= (tptp.s @t3 (tptp.app_2E2 (tptp.s @t27 (tptp.app_2E2 (tptp.s (tptp.tyop_2Emin_2Efun @t3 @t27) tptp.combin_k_2E0) @t22)) @t26)) @t22))) % 0.40/0.63 (assume @p8 (forall (@list @t3 @t2 @t28 @t6 @t1 @t8) (= (tptp.s @t28 (tptp.app_2E2 (tptp.s @t32 (tptp.app_2E2 (tptp.s @t33 (tptp.app_2E2 (tptp.s (tptp.tyop_2Emin_2Efun @t30 @t33) tptp.combin_s_2E0) @t31)) @t5)) @t9)) (tptp.s @t28 (tptp.app_2E2 (tptp.s @t29 (tptp.app_2E2 @t31 @t9)) @t10))))) % 0.40/0.63 (assume @p9 (forall @t16 (= (tptp.p (tptp.mono_2Ec_2Ebool_2E_2F_5C_2E2 @t13 @t12)) (and @t15 @t14)))) % 0.40/0.63 (assume @p10 (forall @t16 (= (tptp.p (tptp.mono_2Ec_2Ebool_2E_5C_2F_2E2 @t13 @t12)) (or @t15 @t14)))) % 0.40/0.63 (assume @p11 (forall @t34 (= (tptp.p (tptp.mono_2Ec_2Ebool_2E_7E_2E1 @t13)) (not @t15)))) % 0.40/0.63 (assume @p12 (forall @t16 (= (tptp.p (tptp.mono_2Ec_2Emin_2E_3D_3D_3E_2E2 @t13 @t12)) (=> @t15 @t14)))) % 0.40/0.63 (assume @p13 (forall (@list @t3 @t37 @t35) (= (tptp.p (tptp.j_mono_2Etyop_2Emin_2Ebool (tptp.s tptp.tyop_2Emin_2Ebool (tptp.c_2Emin_2E_3D_2E2 @t38 @t36)))) (= @t38 @t36)))) % 0.40/0.63 (assume @p14 (forall @t45 (= (tptp.p (tptp.j_mono_2Etyop_2Emin_2Ebool (tptp.s tptp.tyop_2Emin_2Ebool (tptp.c_2Ebool_2E_21_2E1 @t42)))) (forall @t44 @t43)))) % 0.40/0.63 (assume @p15 (forall @t45 (= (tptp.p (tptp.j_mono_2Etyop_2Emin_2Ebool (tptp.s tptp.tyop_2Emin_2Ebool (tptp.c_2Ebool_2E_3F_2E1 @t42)))) (exists @t44 @t43)))) % 0.40/0.63 (assume @p16 (forall @t47 (= (tptp.s tptp.tyop_2Emin_2Ebool (tptp.i_mono_2Etyop_2Emin_2Ebool (tptp.j_mono_2Etyop_2Emin_2Ebool @t46))) @t46))) % 0.40/0.63 (assume @p17 (forall @t47 (= (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))) % 0.40/0.63 (assume @p18 (forall @t47 (= (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))) % 0.40/0.63 (assume @p19 (forall @t34 (= (tptp.j_mono_2Etyop_2Emin_2Ebool (tptp.s tptp.tyop_2Emin_2Ebool (tptp.i_mono_2Etyop_2Emin_2Ebool @t13))) @t13))) % 0.40/0.63 (assume @p20 (forall (@list @t52) (= (tptp.j_mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29 @t53) @t52))) % 0.40/0.63 (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))) % 0.40/0.63 (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)))))) % 0.40/0.63 (assume @p23 (forall @t64 (= (and @t63 @t62) (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 @t61) @t60))))) % 0.40/0.63 (assume @p24 (forall @t69 (= (= @t67 @t66) (tptp.p (tptp.j_mono_2Etyop_2Emin_2Ebool (tptp.s tptp.tyop_2Emin_2Ebool (tptp.app_2E2 (tptp.s @t41 (tptp.app_2E2 (tptp.s @t68 tptp.c_2Emin_2E_3D_2E0) @t67)) @t66))))))) % 0.40/0.63 (assume @p25 (forall @t64 (= (=> @t63 @t62) (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 @t61) @t60))))) % 0.40/0.63 (assume @p26 (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)))))) % 0.40/0.63 (assume @p27 (forall @t64 (= (or @t63 @t62) (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 @t61) @t60))))) % 0.40/0.63 (assume @p28 (forall @t70 (= (not @t63) (tptp.p (tptp.mono_2Eapp_2E2_2Emono_2Etyop_2Emin_2Ebool_20mono_2Etyop_2Emin_2Ebool tptp.mono_2Ec_2Ebool_2E_7E_2E0 @t61))))) % 0.40/0.63 (assume @p29 (forall (@list @t52 @t12) (= (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 @t12))) (tptp.s tptp.tyop_2Emin_2Ebool (tptp.app_2E2 @t53 @t71))))) % 0.40/0.63 (assume @p30 (forall (@list @t54 @t12) (= (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 @t12))) (tptp.s @t48 (tptp.app_2E2 @t55 @t71))))) % 0.40/0.63 (assume @p31 (forall @t47 (= (tptp.s @t73 (tptp.i_mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Efun_28tyop_2Emin_2Eind_2Ctyop_2Emin_2Eind_29_2Ctyop_2Emin_2Ebool_29 (tptp.j_mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Efun_28tyop_2Emin_2Eind_2Ctyop_2Emin_2Eind_29_2Ctyop_2Emin_2Ebool_29 @t74))) @t74))) % 0.40/0.63 (assume @p32 (forall @t47 (= (tptp.s @t72 (tptp.i_mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Eind_2Ctyop_2Emin_2Eind_29 (tptp.j_mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Eind_2Ctyop_2Emin_2Eind_29 @t75))) @t75))) % 0.40/0.63 (assume @p33 (forall (@list @t76) (= (tptp.j_mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Efun_28tyop_2Emin_2Eind_2Ctyop_2Emin_2Eind_29_2Ctyop_2Emin_2Ebool_29 @t77) @t76))) % 0.40/0.63 (assume @p34 (forall @t80 (= (tptp.j_mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Eind_2Ctyop_2Emin_2Eind_29 @t79) @t78))) % 0.40/0.63 (assume @p35 (forall @t59 (= (tptp.j_mono_2Etyop_2Emin_2Ebool (tptp.s tptp.tyop_2Emin_2Ebool (tptp.c_2Ebool_2E_3F_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_3F_21_2E0) @t57)))))) % 0.40/0.63 (assume @p36 (forall @t59 (= (tptp.s @t3 (tptp.c_2Emin_2E_40_2E1 @t57)) (tptp.s @t3 (tptp.app_2E2 (tptp.s @t81 tptp.c_2Emin_2E_40_2E0) @t57))))) % 0.40/0.63 (assume @p37 (forall @t70 (= (tptp.mono_2Ec_2Ebool_2EBOUNDED_2E1 @t61) (tptp.mono_2Eapp_2E2_2Emono_2Etyop_2Emin_2Ebool_20mono_2Etyop_2Emin_2Ebool tptp.mono_2Ec_2Ebool_2EBOUNDED_2E0 @t61)))) % 0.40/0.63 (assume @p38 (forall (@list @t3 @t61 @t65 @t82) (= (tptp.s @t3 (tptp.c_2Ebool_2ECOND_2E3 @t84 @t66 @t83)) (tptp.s @t3 (tptp.app_2E2 (tptp.s @t23 (tptp.app_2E2 (tptp.s @t85 (tptp.app_2E2 (tptp.s (tptp.tyop_2Emin_2Efun tptp.tyop_2Emin_2Ebool @t85) tptp.c_2Ebool_2ECOND_2E0) @t84)) @t66)) @t83))))) % 0.40/0.63 (assume @p39 (forall @t59 (= (tptp.j_mono_2Etyop_2Emin_2Ebool (tptp.s tptp.tyop_2Emin_2Ebool (tptp.c_2Ebool_2EDATATYPE_2E1 @t67))) (tptp.j_mono_2Etyop_2Emin_2Ebool (tptp.s tptp.tyop_2Emin_2Ebool (tptp.app_2E2 (tptp.s @t41 tptp.c_2Ebool_2EDATATYPE_2E0) @t67)))))) % 0.40/0.63 (assume @p40 (forall @t69 (= (tptp.j_mono_2Etyop_2Emin_2Ebool (tptp.s tptp.tyop_2Emin_2Ebool (tptp.c_2Ebool_2EIN_2E2 @t67 @t86))) (tptp.j_mono_2Etyop_2Emin_2Ebool (tptp.s tptp.tyop_2Emin_2Ebool (tptp.app_2E2 (tptp.s @t58 (tptp.app_2E2 (tptp.s (tptp.tyop_2Emin_2Efun @t3 @t58) tptp.c_2Ebool_2EIN_2E0) @t67)) @t86)))))) % 0.40/0.63 (assume @p41 (forall @t89 (= (tptp.s @t2 (tptp.c_2Ebool_2ELET_2E2 @t87 @t66)) (tptp.s @t2 (tptp.app_2E2 (tptp.s @t4 (tptp.app_2E2 (tptp.s @t88 tptp.c_2Ebool_2ELET_2E0) @t87)) @t66))))) % 0.40/0.63 (assume @p42 (forall @t91 (= (tptp.j_mono_2Etyop_2Emin_2Ebool (tptp.s tptp.tyop_2Emin_2Ebool (tptp.c_2Ebool_2EONE__ONE_2E1 @t87))) (tptp.j_mono_2Etyop_2Emin_2Ebool (tptp.s tptp.tyop_2Emin_2Ebool (tptp.app_2E2 (tptp.s @t90 tptp.c_2Ebool_2EONE__ONE_2E0) @t87)))))) % 0.40/0.63 (assume @p43 (forall @t93 (= (tptp.mono_2Ec_2Ebool_2EONE__ONE_2E1_2Emono_2Etyop_2Emin_2Eind_20mono_2Etyop_2Emin_2Eind @t92) (tptp.mono_2Eapp_2E2_2Emono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Eind_2Ctyop_2Emin_2Eind_29_20mono_2Etyop_2Emin_2Ebool tptp.mono_2Ec_2Ebool_2EONE__ONE_2E0_2Emono_2Etyop_2Emin_2Eind_20mono_2Etyop_2Emin_2Eind @t92)))) % 0.40/0.63 (assume @p44 (forall @t91 (= (tptp.j_mono_2Etyop_2Emin_2Ebool (tptp.s tptp.tyop_2Emin_2Ebool (tptp.c_2Ebool_2EONTO_2E1 @t87))) (tptp.j_mono_2Etyop_2Emin_2Ebool (tptp.s tptp.tyop_2Emin_2Ebool (tptp.app_2E2 (tptp.s @t90 tptp.c_2Ebool_2EONTO_2E0) @t87)))))) % 0.40/0.63 (assume @p45 (forall @t93 (= (tptp.mono_2Ec_2Ebool_2EONTO_2E1_2Emono_2Etyop_2Emin_2Eind_20mono_2Etyop_2Emin_2Eind @t92) (tptp.mono_2Eapp_2E2_2Emono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Eind_2Ctyop_2Emin_2Eind_29_20mono_2Etyop_2Emin_2Ebool tptp.mono_2Ec_2Ebool_2EONTO_2E0_2Emono_2Etyop_2Emin_2Eind_20mono_2Etyop_2Emin_2Eind @t92)))) % 0.40/0.63 (assume @p46 (forall @t69 (= (tptp.j_mono_2Etyop_2Emin_2Ebool (tptp.s tptp.tyop_2Emin_2Ebool (tptp.c_2Ebool_2ERES__EXISTS_2E2 @t57 @t86))) (tptp.j_mono_2Etyop_2Emin_2Ebool (tptp.s tptp.tyop_2Emin_2Ebool (tptp.app_2E2 (tptp.s @t58 (tptp.app_2E2 (tptp.s @t94 tptp.c_2Ebool_2ERES__EXISTS_2E0) @t57)) @t86)))))) % 0.40/0.63 (assume @p47 (forall @t69 (= (tptp.j_mono_2Etyop_2Emin_2Ebool (tptp.s tptp.tyop_2Emin_2Ebool (tptp.c_2Ebool_2ERES__EXISTS__UNIQUE_2E2 @t57 @t86))) (tptp.j_mono_2Etyop_2Emin_2Ebool (tptp.s tptp.tyop_2Emin_2Ebool (tptp.app_2E2 (tptp.s @t58 (tptp.app_2E2 (tptp.s @t94 tptp.c_2Ebool_2ERES__EXISTS__UNIQUE_2E0) @t57)) @t86)))))) % 0.40/0.63 (assume @p48 (forall @t69 (= (tptp.j_mono_2Etyop_2Emin_2Ebool (tptp.s tptp.tyop_2Emin_2Ebool (tptp.c_2Ebool_2ERES__FORALL_2E2 @t57 @t86))) (tptp.j_mono_2Etyop_2Emin_2Ebool (tptp.s tptp.tyop_2Emin_2Ebool (tptp.app_2E2 (tptp.s @t58 (tptp.app_2E2 (tptp.s @t94 tptp.c_2Ebool_2ERES__FORALL_2E0) @t57)) @t86)))))) % 0.40/0.63 (assume @p49 (forall @t69 (= (tptp.s @t3 (tptp.c_2Ebool_2ERES__SELECT_2E2 @t57 @t86)) (tptp.s @t3 (tptp.app_2E2 (tptp.s @t81 (tptp.app_2E2 (tptp.s (tptp.tyop_2Emin_2Efun @t41 @t81) tptp.c_2Ebool_2ERES__SELECT_2E0) @t57)) @t86))))) % 0.40/0.63 (assume @p50 (forall @t89 (= (tptp.j_mono_2Etyop_2Emin_2Ebool (tptp.s tptp.tyop_2Emin_2Ebool (tptp.c_2Ebool_2ETYPE__DEFINITION_2E2 @t57 @t95))) (tptp.j_mono_2Etyop_2Emin_2Ebool (tptp.s tptp.tyop_2Emin_2Ebool (tptp.app_2E2 (tptp.s @t96 (tptp.app_2E2 (tptp.s (tptp.tyop_2Emin_2Efun @t41 @t96) tptp.c_2Ebool_2ETYPE__DEFINITION_2E0) @t57)) @t95)))))) % 0.40/0.63 (assume @p51 (forall @t89 (= (tptp.s @t2 (tptp.c_2Ebool_2Eliteral__case_2E2 @t87 @t66)) (tptp.s @t2 (tptp.app_2E2 (tptp.s @t4 (tptp.app_2E2 (tptp.s @t88 tptp.c_2Ebool_2Eliteral__case_2E0) @t87)) @t66))))) % 0.40/0.63 (assume @p52 (forall (@list @t76 @t97) (= (tptp.s tptp.tyop_2Emin_2Ebool (tptp.i_mono_2Etyop_2Emin_2Ebool (tptp.mono_2Eapp_2E2_2Emono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Eind_2Ctyop_2Emin_2Eind_29_20mono_2Etyop_2Emin_2Ebool @t76 @t97))) (tptp.s tptp.tyop_2Emin_2Ebool (tptp.app_2E2 @t77 (tptp.s @t72 (tptp.i_mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Eind_2Ctyop_2Emin_2Eind_29 @t97))))))) % 0.40/0.63 (assume @p53 (= (tptp.s @t73 (tptp.i_mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Efun_28tyop_2Emin_2Eind_2Ctyop_2Emin_2Eind_29_2Ctyop_2Emin_2Ebool_29 tptp.mono_2Ec_2Ebool_2EONE__ONE_2E0_2Emono_2Etyop_2Emin_2Eind_20mono_2Etyop_2Emin_2Eind)) (tptp.s @t73 tptp.c_2Ebool_2EONE__ONE_2E0))) % 0.40/0.63 (assume @p54 (forall @t80 (= (tptp.s tptp.tyop_2Emin_2Ebool (tptp.i_mono_2Etyop_2Emin_2Ebool (tptp.mono_2Ec_2Ebool_2EONE__ONE_2E1_2Emono_2Etyop_2Emin_2Eind_20mono_2Etyop_2Emin_2Eind @t78))) (tptp.s tptp.tyop_2Emin_2Ebool (tptp.c_2Ebool_2EONE__ONE_2E1 @t79))))) % 0.40/0.63 (assume @p55 (= (tptp.s @t73 (tptp.i_mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Efun_28tyop_2Emin_2Eind_2Ctyop_2Emin_2Eind_29_2Ctyop_2Emin_2Ebool_29 tptp.mono_2Ec_2Ebool_2EONTO_2E0_2Emono_2Etyop_2Emin_2Eind_20mono_2Etyop_2Emin_2Eind)) (tptp.s @t73 tptp.c_2Ebool_2EONTO_2E0))) % 0.40/0.63 (assume @p56 (forall @t80 (= (tptp.s tptp.tyop_2Emin_2Ebool (tptp.i_mono_2Etyop_2Emin_2Ebool (tptp.mono_2Ec_2Ebool_2EONTO_2E1_2Emono_2Etyop_2Emin_2Eind_20mono_2Etyop_2Emin_2Eind @t78))) (tptp.s tptp.tyop_2Emin_2Ebool (tptp.c_2Ebool_2EONTO_2E1 @t79))))) % 0.40/0.63 (assume @p57 (forall (@list @t3 @t2 @t98 @t39) (= @t99 @t99))) % 0.40/0.63 (assume @p58 (forall (@list @t3 @t100 @t39) (=> (tptp.p (tptp.j_mono_2Etyop_2Emin_2Ebool (tptp.s tptp.tyop_2Emin_2Ebool (tptp.app_2E2 @t101 @t40)))) (tptp.p (tptp.j_mono_2Etyop_2Emin_2Ebool (tptp.s tptp.tyop_2Emin_2Ebool (tptp.app_2E2 @t101 (tptp.s @t3 (tptp.c_2Emin_2E_40_2E1 @t101))))))))) % 0.40/0.63 (assume @p59 (exists (@list @t102) (and (tptp.p (tptp.mono_2Ec_2Ebool_2EONE__ONE_2E1_2Emono_2Etyop_2Emin_2Eind_20mono_2Etyop_2Emin_2Eind @t102)) (not (tptp.p (tptp.mono_2Ec_2Ebool_2EONTO_2E1_2Emono_2Etyop_2Emin_2Eind_20mono_2Etyop_2Emin_2Eind @t102)))))) % 0.40/0.63 (assume @p60 (= @t17 (forall @t104 (= @t103 @t103)))) % 0.40/0.63 (assume @p61 (forall @t24 (= (tptp.p (tptp.j_mono_2Etyop_2Emin_2Ebool (tptp.s tptp.tyop_2Emin_2Ebool (tptp.c_2Ebool_2E_21_2E1 @t105)))) (forall @t44 (= @t106 tptp.mono_2Ec_2Ebool_2ET_2E0))))) % 0.40/0.63 (assume @p62 (forall @t24 (= @t107 (tptp.j_mono_2Etyop_2Emin_2Ebool (tptp.s tptp.tyop_2Emin_2Ebool (tptp.app_2E2 @t105 (tptp.s @t3 (tptp.c_2Emin_2E_40_2E1 @t105)))))))) % 0.40/0.63 (assume @p63 (forall @t115 (= (and @t113 @t111) (forall @t114 (=> (=> @t113 @t112) @t109))))) % 0.40/0.63 (assume @p64 (forall @t115 (= (or @t113 @t111) (forall @t114 (=> (=> @t113 @t109) (=> @t112 @t109)))))) % 0.40/0.63 (assume @p65 (= @t18 (forall @t20 (tptp.p @t19)))) % 0.40/0.63 (assume @p66 (forall @t104 (= (not @t113) (=> @t113 @t18)))) % 0.40/0.63 (assume @p67 (forall @t24 (= (tptp.p (tptp.j_mono_2Etyop_2Emin_2Ebool (tptp.s tptp.tyop_2Emin_2Ebool (tptp.c_2Ebool_2E_3F_21_2E1 @t105)))) (and (tptp.p @t107) (forall (@list @t39 @t116) (=> (and (tptp.p @t106) (tptp.p (tptp.j_mono_2Etyop_2Emin_2Ebool (tptp.s tptp.tyop_2Emin_2Ebool (tptp.app_2E2 @t105 @t117))))) (= @t40 @t117))))))) % 0.40/0.63 (assume @p68 (forall @t122 (= (tptp.s @t2 (tptp.c_2Ebool_2ELET_2E2 @t120 @t119)) @t121))) % 0.40/0.63 (assume @p69 (forall @t131 (=> (forall (@list @t103 @t118 @t123 @t129) (= (tptp.p (tptp.j_mono_2Etyop_2Emin_2Ebool (tptp.s tptp.tyop_2Emin_2Ebool (tptp.app_2E2 @t128 @t130)))) (and (=> (= @t103 tptp.mono_2Ec_2Ebool_2ET_2E0) (= @t130 @t119)) (=> (= @t103 tptp.mono_2Ec_2Ebool_2EF_2E0) (= @t130 @t124))))) (forall (@list @t103 @t118 @t123) (= (tptp.s @t3 (tptp.c_2Ebool_2ECOND_2E3 @t125 @t119 @t124)) (tptp.s @t3 (tptp.c_2Emin_2E_40_2E1 @t128))))))) % 0.40/0.63 (assume @p70 (forall @t136 (= (tptp.p (tptp.j_mono_2Etyop_2Emin_2Ebool (tptp.s tptp.tyop_2Emin_2Ebool (tptp.c_2Ebool_2EONE__ONE_2E1 @t120)))) (forall (@list @t134 @t132) (=> (= (tptp.s @t2 (tptp.app_2E2 @t120 @t135)) (tptp.s @t2 (tptp.app_2E2 @t120 @t133))) (= @t135 @t133)))))) % 0.40/0.63 (assume @p71 (forall @t136 (= (tptp.p (tptp.j_mono_2Etyop_2Emin_2Ebool (tptp.s tptp.tyop_2Emin_2Ebool (tptp.c_2Ebool_2EONTO_2E1 @t120)))) (forall (@list @t25) (exists @t11 (= @t26 (tptp.s @t2 (tptp.app_2E2 @t120 @t9)))))))) % 0.40/0.63 (assume @p72 (forall @t122 (= (tptp.p (tptp.j_mono_2Etyop_2Emin_2Ebool (tptp.s tptp.tyop_2Emin_2Ebool (tptp.c_2Ebool_2ETYPE__DEFINITION_2E2 @t105 @t138)))) (and (forall (@list @t143 @t141) (=> (= (tptp.s @t3 (tptp.app_2E2 @t138 @t144)) (tptp.s @t3 (tptp.app_2E2 @t138 @t142))) (= @t144 @t142))) (forall (@list @t139) (= (tptp.p (tptp.j_mono_2Etyop_2Emin_2Ebool (tptp.s tptp.tyop_2Emin_2Ebool (tptp.app_2E2 @t105 @t140)))) (exists (@list @t137) (= @t140 (tptp.s @t3 (tptp.app_2E2 @t138 (tptp.s @t2 @t137))))))))))) % 0.40/0.63 (assume @p73 (forall @t122 (= (tptp.s @t2 (tptp.c_2Ebool_2Eliteral__case_2E2 @t120 @t119)) @t121))) % 0.40/0.63 (assume @p74 (forall @t146 (= (tptp.j_mono_2Etyop_2Emin_2Ebool (tptp.s tptp.tyop_2Emin_2Ebool (tptp.c_2Ebool_2EIN_2E2 @t22 @t145))) (tptp.j_mono_2Etyop_2Emin_2Ebool (tptp.s tptp.tyop_2Emin_2Ebool (tptp.app_2E2 @t145 @t22)))))) % 0.40/0.63 (assume @p75 (forall @t146 (= (tptp.p (tptp.j_mono_2Etyop_2Emin_2Ebool (tptp.s tptp.tyop_2Emin_2Ebool (tptp.c_2Ebool_2ERES__FORALL_2E2 @t105 @t145)))) (forall @t11 (=> @t149 @t148))))) % 0.40/0.63 (assume @p76 (forall @t146 (= (tptp.p (tptp.j_mono_2Etyop_2Emin_2Ebool (tptp.s tptp.tyop_2Emin_2Ebool (tptp.c_2Ebool_2ERES__EXISTS_2E2 @t105 @t145)))) (exists @t11 @t150)))) % 0.40/0.63 (assume @p77 (forall (@list @t3 @t157 @t151 @t126) (=> (forall (@list @t118 @t129 @t159) (= (tptp.p (tptp.j_mono_2Etyop_2Emin_2Ebool (tptp.s tptp.tyop_2Emin_2Ebool (tptp.app_2E2 @t158 @t160)))) (=> (and (tptp.p (tptp.j_mono_2Etyop_2Emin_2Ebool (tptp.s tptp.tyop_2Emin_2Ebool (tptp.app_2E2 @t145 @t130)))) (tptp.p (tptp.j_mono_2Etyop_2Emin_2Ebool (tptp.s tptp.tyop_2Emin_2Ebool (tptp.app_2E2 @t145 @t160))))) (= @t130 @t160)))) (=> (forall (@list @t21 @t118 @t129) (= (tptp.j_mono_2Etyop_2Emin_2Ebool (tptp.s tptp.tyop_2Emin_2Ebool (tptp.app_2E2 @t154 @t130))) (tptp.j_mono_2Etyop_2Emin_2Ebool (tptp.s tptp.tyop_2Emin_2Ebool (tptp.c_2Ebool_2ERES__FORALL_2E2 @t105 @t158))))) (=> (forall (@list @t118 @t8) (= (tptp.j_mono_2Etyop_2Emin_2Ebool (tptp.s tptp.tyop_2Emin_2Ebool (tptp.app_2E2 @t155 @t9))) @t147)) (forall @t156 (= (tptp.p (tptp.j_mono_2Etyop_2Emin_2Ebool (tptp.s tptp.tyop_2Emin_2Ebool (tptp.c_2Ebool_2ERES__EXISTS__UNIQUE_2E2 @t105 @t145)))) (and (tptp.p (tptp.j_mono_2Etyop_2Emin_2Ebool (tptp.s tptp.tyop_2Emin_2Ebool (tptp.c_2Ebool_2ERES__EXISTS_2E2 @t105 @t155)))) (tptp.p (tptp.j_mono_2Etyop_2Emin_2Ebool (tptp.s tptp.tyop_2Emin_2Ebool (tptp.c_2Ebool_2ERES__FORALL_2E2 @t105 @t154)))))))))))) % 0.40/0.63 (assume @p78 (forall @t131 (=> (forall (@list @t21 @t118 @t8) (= (tptp.p (tptp.j_mono_2Etyop_2Emin_2Ebool (tptp.s tptp.tyop_2Emin_2Ebool (tptp.app_2E2 @t161 @t9)))) @t150)) (forall @t156 (= (tptp.s @t3 (tptp.c_2Ebool_2ERES__SELECT_2E2 @t105 @t145)) (tptp.s @t3 (tptp.c_2Emin_2E_40_2E1 @t161))))))) % 0.40/0.63 (assume @p79 (forall @t104 (= (tptp.mono_2Ec_2Ebool_2EBOUNDED_2E1 @t103) tptp.mono_2Ec_2Ebool_2ET_2E0))) % 0.40/0.63 (assume @p80 (forall @t24 (= (tptp.j_mono_2Etyop_2Emin_2Ebool (tptp.s tptp.tyop_2Emin_2Ebool (tptp.c_2Ebool_2EDATATYPE_2E1 @t22))) tptp.mono_2Ec_2Ebool_2ET_2E0))) % 0.40/0.63 (assume @p81 (not @t17)) % 0.40/0.63 (assume @p82 true) % 0.40/0.63 (step @p83 false :rule chain_m_resolution :premises (@p81 @p3) :args (false (@list false) (@list @t17))) % 0.40/0.63 ) % 0.40/0.63 % SZS output end Proof % 0.40/0.63 % cvc5 exiting %------------------------------------------------------------------------------