%------------------------------------------------------------------------------
% File : Z3---4.15.1
% Problem : ITP012_1 : TPTP v9.0.0. Bugfixed v7.5.0.
% Transfm : none
% Format : tptp
% Command : run_E %s %d THM
% Computer : n015.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 : Sat Jun 21 05:11:23 AM UTC 2025
% Result : Theorem 39.06s 39.28s
% Output : Proof 39.21s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : ITP012_1 : TPTP v9.0.0. Bugfixed v7.5.0.
% 0.00/0.12 % Command : run_E %s %d THM
% 0.12/0.33 % Computer : n015.cluster.edu
% 0.12/0.33 % Model : x86_64 x86_64
% 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.33 % Memory : 8042.1875MB
% 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.33 % CPULimit : 300
% 0.12/0.34 % WCLimit : 300
% 0.12/0.34 % DateTime : Thu Jun 19 18:11:10 EDT 2025
% 0.12/0.34 % CPUTime :
% 39.06/39.28 % SZS status Theorem
% 39.06/39.28 % SZS output start Proof
% 39.06/39.28 tff(mono_2Ec_2Ebool_2EF_2E0_type, type, (
% 39.06/39.28 mono_2Ec_2Ebool_2EF_2E0: mono_2Etyop_2Emin_2Ebool)).
% 39.06/39.28 tff(mono_2Ec_2Ebool_2ET_2E0_type, type, (
% 39.06/39.28 mono_2Ec_2Ebool_2ET_2E0: mono_2Etyop_2Emin_2Ebool)).
% 39.06/39.28 tff(mono_2Ec_2Einteger_2Eint__divides_2E2_type, type, (
% 39.06/39.28 mono_2Ec_2Einteger_2Eint__divides_2E2: ( mono_2Etyop_2Einteger_2Eint * mono_2Etyop_2Einteger_2Eint ) > mono_2Etyop_2Emin_2Ebool)).
% 39.06/39.28 tff(mono_2Ec_2Einteger_2Eint__neg_2E1_type, type, (
% 39.06/39.28 mono_2Ec_2Einteger_2Eint__neg_2E1: mono_2Etyop_2Einteger_2Eint > mono_2Etyop_2Einteger_2Eint)).
% 39.06/39.28 tff(tptp_fun_V1q_2E0_8_type, type, (
% 39.06/39.28 tptp_fun_V1q_2E0_8: mono_2Etyop_2Einteger_2Eint)).
% 39.06/39.28 tff(tptp_fun_V0p_2E0_9_type, type, (
% 39.06/39.28 tptp_fun_V0p_2E0_9: mono_2Etyop_2Einteger_2Eint)).
% 39.06/39.28 tff(p_type, type, (
% 39.06/39.28 p: mono_2Etyop_2Emin_2Ebool > $o)).
% 39.06/39.28 tff(tptp_fun_V2r_2E0_7_type, type, (
% 39.06/39.28 tptp_fun_V2r_2E0_7: mono_2Etyop_2Einteger_2Eint)).
% 39.06/39.28 tff(mono_2Ec_2Einteger_2Eint__add_2E2_type, type, (
% 39.06/39.28 mono_2Ec_2Einteger_2Eint__add_2E2: ( mono_2Etyop_2Einteger_2Eint * mono_2Etyop_2Einteger_2Eint ) > mono_2Etyop_2Einteger_2Eint)).
% 39.06/39.28 tff(mono_2Ec_2Einteger_2Eint__sub_2E2_type, type, (
% 39.06/39.28 mono_2Ec_2Einteger_2Eint__sub_2E2: ( mono_2Etyop_2Einteger_2Eint * mono_2Etyop_2Einteger_2Eint ) > mono_2Etyop_2Einteger_2Eint)).
% 39.06/39.28 tff(1,plain,
% 39.06/39.28 ((~p(mono_2Ec_2Ebool_2EF_2E0)) <=> (~p(mono_2Ec_2Ebool_2EF_2E0))),
% 39.06/39.28 inference(rewrite,[status(thm)],[])).
% 39.06/39.28 tff(2,axiom,(~p(mono_2Ec_2Ebool_2EF_2E0)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','reserved_2Eho_2Enotfalse')).
% 39.06/39.28 tff(3,plain,
% 39.06/39.28 (~p(mono_2Ec_2Ebool_2EF_2E0)),
% 39.06/39.28 inference(modus_ponens,[status(thm)],[2, 1])).
% 39.06/39.28 tff(4,plain,
% 39.06/39.28 (((~p(mono_2Ec_2Ebool_2EF_2E0)) | p(mono_2Ec_2Einteger_2Eint__divides_2E2(V0p_2E0!9, mono_2Ec_2Einteger_2Eint__neg_2E1(V1q_2E0!8)))) | p(mono_2Ec_2Ebool_2EF_2E0)),
% 39.06/39.28 inference(tautology,[status(thm)],[])).
% 39.06/39.28 tff(5,plain,
% 39.06/39.28 ((~p(mono_2Ec_2Ebool_2EF_2E0)) | p(mono_2Ec_2Einteger_2Eint__divides_2E2(V0p_2E0!9, mono_2Ec_2Einteger_2Eint__neg_2E1(V1q_2E0!8)))),
% 39.06/39.28 inference(unit_resolution,[status(thm)],[4, 3])).
% 39.06/39.28 tff(6,plain,
% 39.06/39.28 (^[V0x_2E0: mono_2Etyop_2Einteger_2Eint, V1y_2E0: mono_2Etyop_2Einteger_2Eint] : refl((mono_2Ec_2Einteger_2Eint__sub_2E2(V0x_2E0, V1y_2E0) = mono_2Ec_2Einteger_2Eint__add_2E2(V0x_2E0, mono_2Ec_2Einteger_2Eint__neg_2E1(V1y_2E0))) <=> (mono_2Ec_2Einteger_2Eint__sub_2E2(V0x_2E0, V1y_2E0) = mono_2Ec_2Einteger_2Eint__add_2E2(V0x_2E0, mono_2Ec_2Einteger_2Eint__neg_2E1(V1y_2E0))))),
% 39.06/39.28 inference(bind,[status(th)],[])).
% 39.06/39.28 tff(7,plain,
% 39.06/39.28 (![V0x_2E0: mono_2Etyop_2Einteger_2Eint, V1y_2E0: mono_2Etyop_2Einteger_2Eint] : (mono_2Ec_2Einteger_2Eint__sub_2E2(V0x_2E0, V1y_2E0) = mono_2Ec_2Einteger_2Eint__add_2E2(V0x_2E0, mono_2Ec_2Einteger_2Eint__neg_2E1(V1y_2E0))) <=> ![V0x_2E0: mono_2Etyop_2Einteger_2Eint, V1y_2E0: mono_2Etyop_2Einteger_2Eint] : (mono_2Ec_2Einteger_2Eint__sub_2E2(V0x_2E0, V1y_2E0) = mono_2Ec_2Einteger_2Eint__add_2E2(V0x_2E0, mono_2Ec_2Einteger_2Eint__neg_2E1(V1y_2E0)))),
% 39.06/39.28 inference(quant_intro,[status(thm)],[6])).
% 39.06/39.28 tff(8,plain,
% 39.06/39.28 (![V0x_2E0: mono_2Etyop_2Einteger_2Eint, V1y_2E0: mono_2Etyop_2Einteger_2Eint] : (mono_2Ec_2Einteger_2Eint__sub_2E2(V0x_2E0, V1y_2E0) = mono_2Ec_2Einteger_2Eint__add_2E2(V0x_2E0, mono_2Ec_2Einteger_2Eint__neg_2E1(V1y_2E0))) <=> ![V0x_2E0: mono_2Etyop_2Einteger_2Eint, V1y_2E0: mono_2Etyop_2Einteger_2Eint] : (mono_2Ec_2Einteger_2Eint__sub_2E2(V0x_2E0, V1y_2E0) = mono_2Ec_2Einteger_2Eint__add_2E2(V0x_2E0, mono_2Ec_2Einteger_2Eint__neg_2E1(V1y_2E0)))),
% 39.06/39.28 inference(rewrite,[status(thm)],[])).
% 39.06/39.28 tff(9,axiom,(![V0x_2E0: mono_2Etyop_2Einteger_2Eint, V1y_2E0: mono_2Etyop_2Einteger_2Eint] : (mono_2Ec_2Einteger_2Eint__sub_2E2(V0x_2E0, V1y_2E0) = mono_2Ec_2Einteger_2Eint__add_2E2(V0x_2E0, mono_2Ec_2Einteger_2Eint__neg_2E1(V1y_2E0)))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','thm_2Einteger_2Eint__sub')).
% 39.06/39.28 tff(10,plain,
% 39.06/39.28 (![V0x_2E0: mono_2Etyop_2Einteger_2Eint, V1y_2E0: mono_2Etyop_2Einteger_2Eint] : (mono_2Ec_2Einteger_2Eint__sub_2E2(V0x_2E0, V1y_2E0) = mono_2Ec_2Einteger_2Eint__add_2E2(V0x_2E0, mono_2Ec_2Einteger_2Eint__neg_2E1(V1y_2E0)))),
% 39.06/39.28 inference(modus_ponens,[status(thm)],[9, 8])).
% 39.06/39.28 tff(11,plain,(
% 39.06/39.28 ![V0x_2E0: mono_2Etyop_2Einteger_2Eint, V1y_2E0: mono_2Etyop_2Einteger_2Eint] : (mono_2Ec_2Einteger_2Eint__sub_2E2(V0x_2E0, V1y_2E0) = mono_2Ec_2Einteger_2Eint__add_2E2(V0x_2E0, mono_2Ec_2Einteger_2Eint__neg_2E1(V1y_2E0)))),
% 39.06/39.28 inference(skolemize,[status(sab)],[10])).
% 39.06/39.28 tff(12,plain,
% 39.06/39.28 (![V0x_2E0: mono_2Etyop_2Einteger_2Eint, V1y_2E0: mono_2Etyop_2Einteger_2Eint] : (mono_2Ec_2Einteger_2Eint__sub_2E2(V0x_2E0, V1y_2E0) = mono_2Ec_2Einteger_2Eint__add_2E2(V0x_2E0, mono_2Ec_2Einteger_2Eint__neg_2E1(V1y_2E0)))),
% 39.06/39.28 inference(modus_ponens,[status(thm)],[11, 7])).
% 39.06/39.28 tff(13,plain,
% 39.06/39.28 ((~![V0x_2E0: mono_2Etyop_2Einteger_2Eint, V1y_2E0: mono_2Etyop_2Einteger_2Eint] : (mono_2Ec_2Einteger_2Eint__sub_2E2(V0x_2E0, V1y_2E0) = mono_2Ec_2Einteger_2Eint__add_2E2(V0x_2E0, mono_2Ec_2Einteger_2Eint__neg_2E1(V1y_2E0)))) | (mono_2Ec_2Einteger_2Eint__sub_2E2(V2r_2E0!7, V1q_2E0!8) = mono_2Ec_2Einteger_2Eint__add_2E2(V2r_2E0!7, mono_2Ec_2Einteger_2Eint__neg_2E1(V1q_2E0!8)))),
% 39.06/39.28 inference(quant_inst,[status(thm)],[])).
% 39.06/39.28 tff(14,plain,
% 39.06/39.28 (mono_2Ec_2Einteger_2Eint__sub_2E2(V2r_2E0!7, V1q_2E0!8) = mono_2Ec_2Einteger_2Eint__add_2E2(V2r_2E0!7, mono_2Ec_2Einteger_2Eint__neg_2E1(V1q_2E0!8))),
% 39.06/39.28 inference(unit_resolution,[status(thm)],[13, 12])).
% 39.06/39.28 tff(15,plain,
% 39.06/39.28 (mono_2Ec_2Einteger_2Eint__add_2E2(V2r_2E0!7, mono_2Ec_2Einteger_2Eint__neg_2E1(V1q_2E0!8)) = mono_2Ec_2Einteger_2Eint__sub_2E2(V2r_2E0!7, V1q_2E0!8)),
% 39.06/39.28 inference(symmetry,[status(thm)],[14])).
% 39.06/39.28 tff(16,plain,
% 39.06/39.28 (mono_2Ec_2Einteger_2Eint__divides_2E2(V0p_2E0!9, mono_2Ec_2Einteger_2Eint__add_2E2(V2r_2E0!7, mono_2Ec_2Einteger_2Eint__neg_2E1(V1q_2E0!8))) = mono_2Ec_2Einteger_2Eint__divides_2E2(V0p_2E0!9, mono_2Ec_2Einteger_2Eint__sub_2E2(V2r_2E0!7, V1q_2E0!8))),
% 39.06/39.28 inference(monotonicity,[status(thm)],[15])).
% 39.06/39.28 tff(17,plain,
% 39.06/39.28 ((mono_2Ec_2Einteger_2Eint__divides_2E2(V0p_2E0!9, mono_2Ec_2Einteger_2Eint__add_2E2(V2r_2E0!7, mono_2Ec_2Einteger_2Eint__neg_2E1(V1q_2E0!8))) = mono_2Ec_2Einteger_2Eint__divides_2E2(V0p_2E0!9, V2r_2E0!7)) <=> (mono_2Ec_2Einteger_2Eint__divides_2E2(V0p_2E0!9, mono_2Ec_2Einteger_2Eint__sub_2E2(V2r_2E0!7, V1q_2E0!8)) = mono_2Ec_2Einteger_2Eint__divides_2E2(V0p_2E0!9, V2r_2E0!7))),
% 39.06/39.28 inference(monotonicity,[status(thm)],[16])).
% 39.06/39.28 tff(18,plain,
% 39.06/39.28 ((mono_2Ec_2Einteger_2Eint__divides_2E2(V0p_2E0!9, mono_2Ec_2Einteger_2Eint__sub_2E2(V2r_2E0!7, V1q_2E0!8)) = mono_2Ec_2Einteger_2Eint__divides_2E2(V0p_2E0!9, V2r_2E0!7)) <=> (mono_2Ec_2Einteger_2Eint__divides_2E2(V0p_2E0!9, mono_2Ec_2Einteger_2Eint__add_2E2(V2r_2E0!7, mono_2Ec_2Einteger_2Eint__neg_2E1(V1q_2E0!8))) = mono_2Ec_2Einteger_2Eint__divides_2E2(V0p_2E0!9, V2r_2E0!7))),
% 39.06/39.28 inference(symmetry,[status(thm)],[17])).
% 39.06/39.28 tff(19,plain,
% 39.06/39.28 ((~(mono_2Ec_2Einteger_2Eint__divides_2E2(V0p_2E0!9, mono_2Ec_2Einteger_2Eint__sub_2E2(V2r_2E0!7, V1q_2E0!8)) = mono_2Ec_2Einteger_2Eint__divides_2E2(V0p_2E0!9, V2r_2E0!7))) <=> (~(mono_2Ec_2Einteger_2Eint__divides_2E2(V0p_2E0!9, mono_2Ec_2Einteger_2Eint__add_2E2(V2r_2E0!7, mono_2Ec_2Einteger_2Eint__neg_2E1(V1q_2E0!8))) = mono_2Ec_2Einteger_2Eint__divides_2E2(V0p_2E0!9, V2r_2E0!7)))),
% 39.06/39.28 inference(monotonicity,[status(thm)],[18])).
% 39.06/39.28 tff(20,plain,
% 39.06/39.28 ((~![V0p_2E0: mono_2Etyop_2Einteger_2Eint, V1q_2E0: mono_2Etyop_2Einteger_2Eint, V2r_2E0: mono_2Etyop_2Einteger_2Eint] : ((~p(mono_2Ec_2Einteger_2Eint__divides_2E2(V0p_2E0, V1q_2E0))) | (mono_2Ec_2Einteger_2Eint__divides_2E2(V0p_2E0, mono_2Ec_2Einteger_2Eint__sub_2E2(V2r_2E0, V1q_2E0)) = mono_2Ec_2Einteger_2Eint__divides_2E2(V0p_2E0, V2r_2E0)))) <=> (~![V0p_2E0: mono_2Etyop_2Einteger_2Eint, V1q_2E0: mono_2Etyop_2Einteger_2Eint, V2r_2E0: mono_2Etyop_2Einteger_2Eint] : ((~p(mono_2Ec_2Einteger_2Eint__divides_2E2(V0p_2E0, V1q_2E0))) | (mono_2Ec_2Einteger_2Eint__divides_2E2(V0p_2E0, mono_2Ec_2Einteger_2Eint__sub_2E2(V2r_2E0, V1q_2E0)) = mono_2Ec_2Einteger_2Eint__divides_2E2(V0p_2E0, V2r_2E0))))),
% 39.06/39.28 inference(rewrite,[status(thm)],[])).
% 39.06/39.28 tff(21,plain,
% 39.06/39.28 ((~![V0p_2E0: mono_2Etyop_2Einteger_2Eint, V1q_2E0: mono_2Etyop_2Einteger_2Eint, V2r_2E0: mono_2Etyop_2Einteger_2Eint] : (p(mono_2Ec_2Einteger_2Eint__divides_2E2(V0p_2E0, V1q_2E0)) => (mono_2Ec_2Einteger_2Eint__divides_2E2(V0p_2E0, mono_2Ec_2Einteger_2Eint__sub_2E2(V2r_2E0, V1q_2E0)) = mono_2Ec_2Einteger_2Eint__divides_2E2(V0p_2E0, V2r_2E0)))) <=> (~![V0p_2E0: mono_2Etyop_2Einteger_2Eint, V1q_2E0: mono_2Etyop_2Einteger_2Eint, V2r_2E0: mono_2Etyop_2Einteger_2Eint] : ((~p(mono_2Ec_2Einteger_2Eint__divides_2E2(V0p_2E0, V1q_2E0))) | (mono_2Ec_2Einteger_2Eint__divides_2E2(V0p_2E0, mono_2Ec_2Einteger_2Eint__sub_2E2(V2r_2E0, V1q_2E0)) = mono_2Ec_2Einteger_2Eint__divides_2E2(V0p_2E0, V2r_2E0))))),
% 39.06/39.28 inference(rewrite,[status(thm)],[])).
% 39.06/39.28 tff(22,axiom,(~![V0p_2E0: mono_2Etyop_2Einteger_2Eint, V1q_2E0: mono_2Etyop_2Einteger_2Eint, V2r_2E0: mono_2Etyop_2Einteger_2Eint] : (p(mono_2Ec_2Einteger_2Eint__divides_2E2(V0p_2E0, V1q_2E0)) => (mono_2Ec_2Einteger_2Eint__divides_2E2(V0p_2E0, mono_2Ec_2Einteger_2Eint__sub_2E2(V2r_2E0, V1q_2E0)) = mono_2Ec_2Einteger_2Eint__divides_2E2(V0p_2E0, V2r_2E0)))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','thm_2Einteger_2EINT__DIVIDES__RSUB')).
% 39.06/39.28 tff(23,plain,
% 39.06/39.28 (~![V0p_2E0: mono_2Etyop_2Einteger_2Eint, V1q_2E0: mono_2Etyop_2Einteger_2Eint, V2r_2E0: mono_2Etyop_2Einteger_2Eint] : ((~p(mono_2Ec_2Einteger_2Eint__divides_2E2(V0p_2E0, V1q_2E0))) | (mono_2Ec_2Einteger_2Eint__divides_2E2(V0p_2E0, mono_2Ec_2Einteger_2Eint__sub_2E2(V2r_2E0, V1q_2E0)) = mono_2Ec_2Einteger_2Eint__divides_2E2(V0p_2E0, V2r_2E0)))),
% 39.06/39.28 inference(modus_ponens,[status(thm)],[22, 21])).
% 39.06/39.28 tff(24,plain,
% 39.06/39.28 (~![V0p_2E0: mono_2Etyop_2Einteger_2Eint, V1q_2E0: mono_2Etyop_2Einteger_2Eint, V2r_2E0: mono_2Etyop_2Einteger_2Eint] : ((~p(mono_2Ec_2Einteger_2Eint__divides_2E2(V0p_2E0, V1q_2E0))) | (mono_2Ec_2Einteger_2Eint__divides_2E2(V0p_2E0, mono_2Ec_2Einteger_2Eint__sub_2E2(V2r_2E0, V1q_2E0)) = mono_2Ec_2Einteger_2Eint__divides_2E2(V0p_2E0, V2r_2E0)))),
% 39.06/39.28 inference(modus_ponens,[status(thm)],[23, 20])).
% 39.06/39.28 tff(25,plain,
% 39.06/39.28 (~![V0p_2E0: mono_2Etyop_2Einteger_2Eint, V1q_2E0: mono_2Etyop_2Einteger_2Eint, V2r_2E0: mono_2Etyop_2Einteger_2Eint] : ((~p(mono_2Ec_2Einteger_2Eint__divides_2E2(V0p_2E0, V1q_2E0))) | (mono_2Ec_2Einteger_2Eint__divides_2E2(V0p_2E0, mono_2Ec_2Einteger_2Eint__sub_2E2(V2r_2E0, V1q_2E0)) = mono_2Ec_2Einteger_2Eint__divides_2E2(V0p_2E0, V2r_2E0)))),
% 39.06/39.28 inference(modus_ponens,[status(thm)],[24, 20])).
% 39.06/39.28 tff(26,plain,
% 39.06/39.28 (~![V0p_2E0: mono_2Etyop_2Einteger_2Eint, V1q_2E0: mono_2Etyop_2Einteger_2Eint, V2r_2E0: mono_2Etyop_2Einteger_2Eint] : ((~p(mono_2Ec_2Einteger_2Eint__divides_2E2(V0p_2E0, V1q_2E0))) | (mono_2Ec_2Einteger_2Eint__divides_2E2(V0p_2E0, mono_2Ec_2Einteger_2Eint__sub_2E2(V2r_2E0, V1q_2E0)) = mono_2Ec_2Einteger_2Eint__divides_2E2(V0p_2E0, V2r_2E0)))),
% 39.06/39.28 inference(modus_ponens,[status(thm)],[25, 20])).
% 39.06/39.28 tff(27,plain,(
% 39.06/39.28 ~((~p(mono_2Ec_2Einteger_2Eint__divides_2E2(V0p_2E0!9, V1q_2E0!8))) | (mono_2Ec_2Einteger_2Eint__divides_2E2(V0p_2E0!9, mono_2Ec_2Einteger_2Eint__sub_2E2(V2r_2E0!7, V1q_2E0!8)) = mono_2Ec_2Einteger_2Eint__divides_2E2(V0p_2E0!9, V2r_2E0!7)))),
% 39.06/39.28 inference(skolemize,[status(sab)],[26])).
% 39.06/39.28 tff(28,plain,
% 39.06/39.28 (~(mono_2Ec_2Einteger_2Eint__divides_2E2(V0p_2E0!9, mono_2Ec_2Einteger_2Eint__sub_2E2(V2r_2E0!7, V1q_2E0!8)) = mono_2Ec_2Einteger_2Eint__divides_2E2(V0p_2E0!9, V2r_2E0!7))),
% 39.06/39.28 inference(or_elim,[status(thm)],[27])).
% 39.06/39.28 tff(29,plain,
% 39.06/39.28 (~(mono_2Ec_2Einteger_2Eint__divides_2E2(V0p_2E0!9, mono_2Ec_2Einteger_2Eint__add_2E2(V2r_2E0!7, mono_2Ec_2Einteger_2Eint__neg_2E1(V1q_2E0!8))) = mono_2Ec_2Einteger_2Eint__divides_2E2(V0p_2E0!9, V2r_2E0!7))),
% 39.06/39.28 inference(modus_ponens,[status(thm)],[28, 19])).
% 39.06/39.28 tff(30,plain,
% 39.06/39.28 (^[V0p_2E0: mono_2Etyop_2Einteger_2Eint, V1q_2E0: mono_2Etyop_2Einteger_2Eint, V2r_2E0: mono_2Etyop_2Einteger_2Eint] : refl(((~p(mono_2Ec_2Einteger_2Eint__divides_2E2(V0p_2E0, V1q_2E0))) | (mono_2Ec_2Einteger_2Eint__divides_2E2(V0p_2E0, mono_2Ec_2Einteger_2Eint__add_2E2(V2r_2E0, V1q_2E0)) = mono_2Ec_2Einteger_2Eint__divides_2E2(V0p_2E0, V2r_2E0))) <=> ((~p(mono_2Ec_2Einteger_2Eint__divides_2E2(V0p_2E0, V1q_2E0))) | (mono_2Ec_2Einteger_2Eint__divides_2E2(V0p_2E0, mono_2Ec_2Einteger_2Eint__add_2E2(V2r_2E0, V1q_2E0)) = mono_2Ec_2Einteger_2Eint__divides_2E2(V0p_2E0, V2r_2E0))))),
% 39.06/39.28 inference(bind,[status(th)],[])).
% 39.06/39.28 tff(31,plain,
% 39.06/39.28 (![V0p_2E0: mono_2Etyop_2Einteger_2Eint, V1q_2E0: mono_2Etyop_2Einteger_2Eint, V2r_2E0: mono_2Etyop_2Einteger_2Eint] : ((~p(mono_2Ec_2Einteger_2Eint__divides_2E2(V0p_2E0, V1q_2E0))) | (mono_2Ec_2Einteger_2Eint__divides_2E2(V0p_2E0, mono_2Ec_2Einteger_2Eint__add_2E2(V2r_2E0, V1q_2E0)) = mono_2Ec_2Einteger_2Eint__divides_2E2(V0p_2E0, V2r_2E0))) <=> ![V0p_2E0: mono_2Etyop_2Einteger_2Eint, V1q_2E0: mono_2Etyop_2Einteger_2Eint, V2r_2E0: mono_2Etyop_2Einteger_2Eint] : ((~p(mono_2Ec_2Einteger_2Eint__divides_2E2(V0p_2E0, V1q_2E0))) | (mono_2Ec_2Einteger_2Eint__divides_2E2(V0p_2E0, mono_2Ec_2Einteger_2Eint__add_2E2(V2r_2E0, V1q_2E0)) = mono_2Ec_2Einteger_2Eint__divides_2E2(V0p_2E0, V2r_2E0)))),
% 39.06/39.28 inference(quant_intro,[status(thm)],[30])).
% 39.06/39.28 tff(32,plain,
% 39.06/39.28 (![V0p_2E0: mono_2Etyop_2Einteger_2Eint, V1q_2E0: mono_2Etyop_2Einteger_2Eint, V2r_2E0: mono_2Etyop_2Einteger_2Eint] : ((~p(mono_2Ec_2Einteger_2Eint__divides_2E2(V0p_2E0, V1q_2E0))) | (mono_2Ec_2Einteger_2Eint__divides_2E2(V0p_2E0, mono_2Ec_2Einteger_2Eint__add_2E2(V2r_2E0, V1q_2E0)) = mono_2Ec_2Einteger_2Eint__divides_2E2(V0p_2E0, V2r_2E0))) <=> ![V0p_2E0: mono_2Etyop_2Einteger_2Eint, V1q_2E0: mono_2Etyop_2Einteger_2Eint, V2r_2E0: mono_2Etyop_2Einteger_2Eint] : ((~p(mono_2Ec_2Einteger_2Eint__divides_2E2(V0p_2E0, V1q_2E0))) | (mono_2Ec_2Einteger_2Eint__divides_2E2(V0p_2E0, mono_2Ec_2Einteger_2Eint__add_2E2(V2r_2E0, V1q_2E0)) = mono_2Ec_2Einteger_2Eint__divides_2E2(V0p_2E0, V2r_2E0)))),
% 39.06/39.28 inference(rewrite,[status(thm)],[])).
% 39.06/39.28 tff(33,plain,
% 39.06/39.28 (^[V0p_2E0: mono_2Etyop_2Einteger_2Eint, V1q_2E0: mono_2Etyop_2Einteger_2Eint, V2r_2E0: mono_2Etyop_2Einteger_2Eint] : rewrite((p(mono_2Ec_2Einteger_2Eint__divides_2E2(V0p_2E0, V1q_2E0)) => (mono_2Ec_2Einteger_2Eint__divides_2E2(V0p_2E0, mono_2Ec_2Einteger_2Eint__add_2E2(V2r_2E0, V1q_2E0)) = mono_2Ec_2Einteger_2Eint__divides_2E2(V0p_2E0, V2r_2E0))) <=> ((~p(mono_2Ec_2Einteger_2Eint__divides_2E2(V0p_2E0, V1q_2E0))) | (mono_2Ec_2Einteger_2Eint__divides_2E2(V0p_2E0, mono_2Ec_2Einteger_2Eint__add_2E2(V2r_2E0, V1q_2E0)) = mono_2Ec_2Einteger_2Eint__divides_2E2(V0p_2E0, V2r_2E0))))),
% 39.06/39.28 inference(bind,[status(th)],[])).
% 39.06/39.28 tff(34,plain,
% 39.06/39.28 (![V0p_2E0: mono_2Etyop_2Einteger_2Eint, V1q_2E0: mono_2Etyop_2Einteger_2Eint, V2r_2E0: mono_2Etyop_2Einteger_2Eint] : (p(mono_2Ec_2Einteger_2Eint__divides_2E2(V0p_2E0, V1q_2E0)) => (mono_2Ec_2Einteger_2Eint__divides_2E2(V0p_2E0, mono_2Ec_2Einteger_2Eint__add_2E2(V2r_2E0, V1q_2E0)) = mono_2Ec_2Einteger_2Eint__divides_2E2(V0p_2E0, V2r_2E0))) <=> ![V0p_2E0: mono_2Etyop_2Einteger_2Eint, V1q_2E0: mono_2Etyop_2Einteger_2Eint, V2r_2E0: mono_2Etyop_2Einteger_2Eint] : ((~p(mono_2Ec_2Einteger_2Eint__divides_2E2(V0p_2E0, V1q_2E0))) | (mono_2Ec_2Einteger_2Eint__divides_2E2(V0p_2E0, mono_2Ec_2Einteger_2Eint__add_2E2(V2r_2E0, V1q_2E0)) = mono_2Ec_2Einteger_2Eint__divides_2E2(V0p_2E0, V2r_2E0)))),
% 39.06/39.28 inference(quant_intro,[status(thm)],[33])).
% 39.06/39.28 tff(35,axiom,(![V0p_2E0: mono_2Etyop_2Einteger_2Eint, V1q_2E0: mono_2Etyop_2Einteger_2Eint, V2r_2E0: mono_2Etyop_2Einteger_2Eint] : (p(mono_2Ec_2Einteger_2Eint__divides_2E2(V0p_2E0, V1q_2E0)) => (mono_2Ec_2Einteger_2Eint__divides_2E2(V0p_2E0, mono_2Ec_2Einteger_2Eint__add_2E2(V2r_2E0, V1q_2E0)) = mono_2Ec_2Einteger_2Eint__divides_2E2(V0p_2E0, V2r_2E0)))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','thm_2Einteger_2EINT__DIVIDES__RADD')).
% 39.06/39.28 tff(36,plain,
% 39.06/39.28 (![V0p_2E0: mono_2Etyop_2Einteger_2Eint, V1q_2E0: mono_2Etyop_2Einteger_2Eint, V2r_2E0: mono_2Etyop_2Einteger_2Eint] : ((~p(mono_2Ec_2Einteger_2Eint__divides_2E2(V0p_2E0, V1q_2E0))) | (mono_2Ec_2Einteger_2Eint__divides_2E2(V0p_2E0, mono_2Ec_2Einteger_2Eint__add_2E2(V2r_2E0, V1q_2E0)) = mono_2Ec_2Einteger_2Eint__divides_2E2(V0p_2E0, V2r_2E0)))),
% 39.06/39.28 inference(modus_ponens,[status(thm)],[35, 34])).
% 39.06/39.28 tff(37,plain,
% 39.06/39.28 (![V0p_2E0: mono_2Etyop_2Einteger_2Eint, V1q_2E0: mono_2Etyop_2Einteger_2Eint, V2r_2E0: mono_2Etyop_2Einteger_2Eint] : ((~p(mono_2Ec_2Einteger_2Eint__divides_2E2(V0p_2E0, V1q_2E0))) | (mono_2Ec_2Einteger_2Eint__divides_2E2(V0p_2E0, mono_2Ec_2Einteger_2Eint__add_2E2(V2r_2E0, V1q_2E0)) = mono_2Ec_2Einteger_2Eint__divides_2E2(V0p_2E0, V2r_2E0)))),
% 39.06/39.28 inference(modus_ponens,[status(thm)],[36, 32])).
% 39.06/39.28 tff(38,plain,(
% 39.06/39.28 ![V0p_2E0: mono_2Etyop_2Einteger_2Eint, V1q_2E0: mono_2Etyop_2Einteger_2Eint, V2r_2E0: mono_2Etyop_2Einteger_2Eint] : ((~p(mono_2Ec_2Einteger_2Eint__divides_2E2(V0p_2E0, V1q_2E0))) | (mono_2Ec_2Einteger_2Eint__divides_2E2(V0p_2E0, mono_2Ec_2Einteger_2Eint__add_2E2(V2r_2E0, V1q_2E0)) = mono_2Ec_2Einteger_2Eint__divides_2E2(V0p_2E0, V2r_2E0)))),
% 39.06/39.28 inference(skolemize,[status(sab)],[37])).
% 39.06/39.28 tff(39,plain,
% 39.06/39.28 (![V0p_2E0: mono_2Etyop_2Einteger_2Eint, V1q_2E0: mono_2Etyop_2Einteger_2Eint, V2r_2E0: mono_2Etyop_2Einteger_2Eint] : ((~p(mono_2Ec_2Einteger_2Eint__divides_2E2(V0p_2E0, V1q_2E0))) | (mono_2Ec_2Einteger_2Eint__divides_2E2(V0p_2E0, mono_2Ec_2Einteger_2Eint__add_2E2(V2r_2E0, V1q_2E0)) = mono_2Ec_2Einteger_2Eint__divides_2E2(V0p_2E0, V2r_2E0)))),
% 39.06/39.28 inference(modus_ponens,[status(thm)],[38, 31])).
% 39.06/39.28 tff(40,plain,
% 39.06/39.28 (((~![V0p_2E0: mono_2Etyop_2Einteger_2Eint, V1q_2E0: mono_2Etyop_2Einteger_2Eint, V2r_2E0: mono_2Etyop_2Einteger_2Eint] : ((~p(mono_2Ec_2Einteger_2Eint__divides_2E2(V0p_2E0, V1q_2E0))) | (mono_2Ec_2Einteger_2Eint__divides_2E2(V0p_2E0, mono_2Ec_2Einteger_2Eint__add_2E2(V2r_2E0, V1q_2E0)) = mono_2Ec_2Einteger_2Eint__divides_2E2(V0p_2E0, V2r_2E0)))) | ((~p(mono_2Ec_2Einteger_2Eint__divides_2E2(V0p_2E0!9, mono_2Ec_2Einteger_2Eint__neg_2E1(V1q_2E0!8)))) | (mono_2Ec_2Einteger_2Eint__divides_2E2(V0p_2E0!9, mono_2Ec_2Einteger_2Eint__add_2E2(V2r_2E0!7, mono_2Ec_2Einteger_2Eint__neg_2E1(V1q_2E0!8))) = mono_2Ec_2Einteger_2Eint__divides_2E2(V0p_2E0!9, V2r_2E0!7)))) <=> ((~![V0p_2E0: mono_2Etyop_2Einteger_2Eint, V1q_2E0: mono_2Etyop_2Einteger_2Eint, V2r_2E0: mono_2Etyop_2Einteger_2Eint] : ((~p(mono_2Ec_2Einteger_2Eint__divides_2E2(V0p_2E0, V1q_2E0))) | (mono_2Ec_2Einteger_2Eint__divides_2E2(V0p_2E0, mono_2Ec_2Einteger_2Eint__add_2E2(V2r_2E0, V1q_2E0)) = mono_2Ec_2Einteger_2Eint__divides_2E2(V0p_2E0, V2r_2E0)))) | (~p(mono_2Ec_2Einteger_2Eint__divides_2E2(V0p_2E0!9, mono_2Ec_2Einteger_2Eint__neg_2E1(V1q_2E0!8)))) | (mono_2Ec_2Einteger_2Eint__divides_2E2(V0p_2E0!9, mono_2Ec_2Einteger_2Eint__add_2E2(V2r_2E0!7, mono_2Ec_2Einteger_2Eint__neg_2E1(V1q_2E0!8))) = mono_2Ec_2Einteger_2Eint__divides_2E2(V0p_2E0!9, V2r_2E0!7)))),
% 39.06/39.28 inference(rewrite,[status(thm)],[])).
% 39.06/39.28 tff(41,plain,
% 39.06/39.28 ((~![V0p_2E0: mono_2Etyop_2Einteger_2Eint, V1q_2E0: mono_2Etyop_2Einteger_2Eint, V2r_2E0: mono_2Etyop_2Einteger_2Eint] : ((~p(mono_2Ec_2Einteger_2Eint__divides_2E2(V0p_2E0, V1q_2E0))) | (mono_2Ec_2Einteger_2Eint__divides_2E2(V0p_2E0, mono_2Ec_2Einteger_2Eint__add_2E2(V2r_2E0, V1q_2E0)) = mono_2Ec_2Einteger_2Eint__divides_2E2(V0p_2E0, V2r_2E0)))) | ((~p(mono_2Ec_2Einteger_2Eint__divides_2E2(V0p_2E0!9, mono_2Ec_2Einteger_2Eint__neg_2E1(V1q_2E0!8)))) | (mono_2Ec_2Einteger_2Eint__divides_2E2(V0p_2E0!9, mono_2Ec_2Einteger_2Eint__add_2E2(V2r_2E0!7, mono_2Ec_2Einteger_2Eint__neg_2E1(V1q_2E0!8))) = mono_2Ec_2Einteger_2Eint__divides_2E2(V0p_2E0!9, V2r_2E0!7)))),
% 39.06/39.28 inference(quant_inst,[status(thm)],[])).
% 39.06/39.28 tff(42,plain,
% 39.06/39.28 ((~![V0p_2E0: mono_2Etyop_2Einteger_2Eint, V1q_2E0: mono_2Etyop_2Einteger_2Eint, V2r_2E0: mono_2Etyop_2Einteger_2Eint] : ((~p(mono_2Ec_2Einteger_2Eint__divides_2E2(V0p_2E0, V1q_2E0))) | (mono_2Ec_2Einteger_2Eint__divides_2E2(V0p_2E0, mono_2Ec_2Einteger_2Eint__add_2E2(V2r_2E0, V1q_2E0)) = mono_2Ec_2Einteger_2Eint__divides_2E2(V0p_2E0, V2r_2E0)))) | (~p(mono_2Ec_2Einteger_2Eint__divides_2E2(V0p_2E0!9, mono_2Ec_2Einteger_2Eint__neg_2E1(V1q_2E0!8)))) | (mono_2Ec_2Einteger_2Eint__divides_2E2(V0p_2E0!9, mono_2Ec_2Einteger_2Eint__add_2E2(V2r_2E0!7, mono_2Ec_2Einteger_2Eint__neg_2E1(V1q_2E0!8))) = mono_2Ec_2Einteger_2Eint__divides_2E2(V0p_2E0!9, V2r_2E0!7))),
% 39.06/39.28 inference(modus_ponens,[status(thm)],[41, 40])).
% 39.06/39.28 tff(43,plain,
% 39.06/39.28 ((~p(mono_2Ec_2Einteger_2Eint__divides_2E2(V0p_2E0!9, mono_2Ec_2Einteger_2Eint__neg_2E1(V1q_2E0!8)))) | (mono_2Ec_2Einteger_2Eint__divides_2E2(V0p_2E0!9, mono_2Ec_2Einteger_2Eint__add_2E2(V2r_2E0!7, mono_2Ec_2Einteger_2Eint__neg_2E1(V1q_2E0!8))) = mono_2Ec_2Einteger_2Eint__divides_2E2(V0p_2E0!9, V2r_2E0!7))),
% 39.06/39.28 inference(unit_resolution,[status(thm)],[42, 39])).
% 39.06/39.28 tff(44,plain,
% 39.06/39.28 (~p(mono_2Ec_2Einteger_2Eint__divides_2E2(V0p_2E0!9, mono_2Ec_2Einteger_2Eint__neg_2E1(V1q_2E0!8)))),
% 39.06/39.28 inference(unit_resolution,[status(thm)],[43, 29])).
% 39.06/39.28 tff(45,plain,
% 39.06/39.28 ((p(mono_2Ec_2Ebool_2EF_2E0) | (~p(mono_2Ec_2Einteger_2Eint__divides_2E2(V0p_2E0!9, mono_2Ec_2Einteger_2Eint__neg_2E1(V1q_2E0!8))))) | p(mono_2Ec_2Einteger_2Eint__divides_2E2(V0p_2E0!9, mono_2Ec_2Einteger_2Eint__neg_2E1(V1q_2E0!8)))),
% 39.06/39.28 inference(tautology,[status(thm)],[])).
% 39.06/39.28 tff(46,plain,
% 39.06/39.28 (p(mono_2Ec_2Ebool_2EF_2E0) | (~p(mono_2Ec_2Einteger_2Eint__divides_2E2(V0p_2E0!9, mono_2Ec_2Einteger_2Eint__neg_2E1(V1q_2E0!8))))),
% 39.06/39.28 inference(unit_resolution,[status(thm)],[45, 44])).
% 39.06/39.28 tff(47,plain,
% 39.06/39.28 (^[V0t1_2E0: mono_2Etyop_2Emin_2Ebool, V1t2_2E0: mono_2Etyop_2Emin_2Ebool] : refl(((V0t1_2E0 = V1t2_2E0) | (~((~p(V1t2_2E0)) | p(V0t1_2E0))) | (~(p(V1t2_2E0) | (~p(V0t1_2E0))))) <=> ((V0t1_2E0 = V1t2_2E0) | (~((~p(V1t2_2E0)) | p(V0t1_2E0))) | (~(p(V1t2_2E0) | (~p(V0t1_2E0))))))),
% 39.06/39.28 inference(bind,[status(th)],[])).
% 39.06/39.28 tff(48,plain,
% 39.06/39.28 (![V0t1_2E0: mono_2Etyop_2Emin_2Ebool, V1t2_2E0: mono_2Etyop_2Emin_2Ebool] : ((V0t1_2E0 = V1t2_2E0) | (~((~p(V1t2_2E0)) | p(V0t1_2E0))) | (~(p(V1t2_2E0) | (~p(V0t1_2E0))))) <=> ![V0t1_2E0: mono_2Etyop_2Emin_2Ebool, V1t2_2E0: mono_2Etyop_2Emin_2Ebool] : ((V0t1_2E0 = V1t2_2E0) | (~((~p(V1t2_2E0)) | p(V0t1_2E0))) | (~(p(V1t2_2E0) | (~p(V0t1_2E0)))))),
% 39.06/39.28 inference(quant_intro,[status(thm)],[47])).
% 39.06/39.28 tff(49,plain,
% 39.06/39.28 (![V0t1_2E0: mono_2Etyop_2Emin_2Ebool, V1t2_2E0: mono_2Etyop_2Emin_2Ebool] : ((V0t1_2E0 = V1t2_2E0) | (~((~p(V1t2_2E0)) | p(V0t1_2E0))) | (~(p(V1t2_2E0) | (~p(V0t1_2E0))))) <=> ![V0t1_2E0: mono_2Etyop_2Emin_2Ebool, V1t2_2E0: mono_2Etyop_2Emin_2Ebool] : ((V0t1_2E0 = V1t2_2E0) | (~((~p(V1t2_2E0)) | p(V0t1_2E0))) | (~(p(V1t2_2E0) | (~p(V0t1_2E0)))))),
% 39.06/39.28 inference(rewrite,[status(thm)],[])).
% 39.06/39.28 tff(50,plain,
% 39.06/39.28 (^[V0t1_2E0: mono_2Etyop_2Emin_2Ebool, V1t2_2E0: mono_2Etyop_2Emin_2Ebool] : trans(monotonicity(rewrite((p(V0t1_2E0) => p(V1t2_2E0)) <=> (p(V1t2_2E0) | (~p(V0t1_2E0)))), trans(monotonicity(rewrite((p(V1t2_2E0) => p(V0t1_2E0)) <=> ((~p(V1t2_2E0)) | p(V0t1_2E0))), (((p(V1t2_2E0) => p(V0t1_2E0)) => (V0t1_2E0 = V1t2_2E0)) <=> (((~p(V1t2_2E0)) | p(V0t1_2E0)) => (V0t1_2E0 = V1t2_2E0)))), rewrite((((~p(V1t2_2E0)) | p(V0t1_2E0)) => (V0t1_2E0 = V1t2_2E0)) <=> ((~((~p(V1t2_2E0)) | p(V0t1_2E0))) | (V0t1_2E0 = V1t2_2E0))), (((p(V1t2_2E0) => p(V0t1_2E0)) => (V0t1_2E0 = V1t2_2E0)) <=> ((~((~p(V1t2_2E0)) | p(V0t1_2E0))) | (V0t1_2E0 = V1t2_2E0)))), (((p(V0t1_2E0) => p(V1t2_2E0)) => ((p(V1t2_2E0) => p(V0t1_2E0)) => (V0t1_2E0 = V1t2_2E0))) <=> ((p(V1t2_2E0) | (~p(V0t1_2E0))) => ((~((~p(V1t2_2E0)) | p(V0t1_2E0))) | (V0t1_2E0 = V1t2_2E0))))), rewrite(((p(V1t2_2E0) | (~p(V0t1_2E0))) => ((~((~p(V1t2_2E0)) | p(V0t1_2E0))) | (V0t1_2E0 = V1t2_2E0))) <=> ((V0t1_2E0 = V1t2_2E0) | (~((~p(V1t2_2E0)) | p(V0t1_2E0))) | (~(p(V1t2_2E0) | (~p(V0t1_2E0)))))), (((p(V0t1_2E0) => p(V1t2_2E0)) => ((p(V1t2_2E0) => p(V0t1_2E0)) => (V0t1_2E0 = V1t2_2E0))) <=> ((V0t1_2E0 = V1t2_2E0) | (~((~p(V1t2_2E0)) | p(V0t1_2E0))) | (~(p(V1t2_2E0) | (~p(V0t1_2E0)))))))),
% 39.06/39.28 inference(bind,[status(th)],[])).
% 39.06/39.28 tff(51,plain,
% 39.06/39.28 (![V0t1_2E0: mono_2Etyop_2Emin_2Ebool, V1t2_2E0: mono_2Etyop_2Emin_2Ebool] : ((p(V0t1_2E0) => p(V1t2_2E0)) => ((p(V1t2_2E0) => p(V0t1_2E0)) => (V0t1_2E0 = V1t2_2E0))) <=> ![V0t1_2E0: mono_2Etyop_2Emin_2Ebool, V1t2_2E0: mono_2Etyop_2Emin_2Ebool] : ((V0t1_2E0 = V1t2_2E0) | (~((~p(V1t2_2E0)) | p(V0t1_2E0))) | (~(p(V1t2_2E0) | (~p(V0t1_2E0)))))),
% 39.06/39.28 inference(quant_intro,[status(thm)],[50])).
% 39.06/39.28 tff(52,axiom,(![V0t1_2E0: mono_2Etyop_2Emin_2Ebool, V1t2_2E0: mono_2Etyop_2Emin_2Ebool] : ((p(V0t1_2E0) => p(V1t2_2E0)) => ((p(V1t2_2E0) => p(V0t1_2E0)) => (V0t1_2E0 = V1t2_2E0)))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','thm_2Ebool_2EIMP__ANTISYM__AX')).
% 39.06/39.28 tff(53,plain,
% 39.06/39.28 (![V0t1_2E0: mono_2Etyop_2Emin_2Ebool, V1t2_2E0: mono_2Etyop_2Emin_2Ebool] : ((V0t1_2E0 = V1t2_2E0) | (~((~p(V1t2_2E0)) | p(V0t1_2E0))) | (~(p(V1t2_2E0) | (~p(V0t1_2E0)))))),
% 39.06/39.28 inference(modus_ponens,[status(thm)],[52, 51])).
% 39.06/39.28 tff(54,plain,
% 39.06/39.28 (![V0t1_2E0: mono_2Etyop_2Emin_2Ebool, V1t2_2E0: mono_2Etyop_2Emin_2Ebool] : ((V0t1_2E0 = V1t2_2E0) | (~((~p(V1t2_2E0)) | p(V0t1_2E0))) | (~(p(V1t2_2E0) | (~p(V0t1_2E0)))))),
% 39.06/39.28 inference(modus_ponens,[status(thm)],[53, 49])).
% 39.06/39.28 tff(55,plain,(
% 39.06/39.28 ![V0t1_2E0: mono_2Etyop_2Emin_2Ebool, V1t2_2E0: mono_2Etyop_2Emin_2Ebool] : ((V0t1_2E0 = V1t2_2E0) | (~((~p(V1t2_2E0)) | p(V0t1_2E0))) | (~(p(V1t2_2E0) | (~p(V0t1_2E0)))))),
% 39.06/39.28 inference(skolemize,[status(sab)],[54])).
% 39.06/39.28 tff(56,plain,
% 39.06/39.28 (![V0t1_2E0: mono_2Etyop_2Emin_2Ebool, V1t2_2E0: mono_2Etyop_2Emin_2Ebool] : ((V0t1_2E0 = V1t2_2E0) | (~((~p(V1t2_2E0)) | p(V0t1_2E0))) | (~(p(V1t2_2E0) | (~p(V0t1_2E0)))))),
% 39.06/39.28 inference(modus_ponens,[status(thm)],[55, 48])).
% 39.06/39.28 tff(57,plain,
% 39.06/39.28 (((~![V0t1_2E0: mono_2Etyop_2Emin_2Ebool, V1t2_2E0: mono_2Etyop_2Emin_2Ebool] : ((V0t1_2E0 = V1t2_2E0) | (~((~p(V1t2_2E0)) | p(V0t1_2E0))) | (~(p(V1t2_2E0) | (~p(V0t1_2E0)))))) | ((mono_2Ec_2Einteger_2Eint__divides_2E2(V0p_2E0!9, mono_2Ec_2Einteger_2Eint__neg_2E1(V1q_2E0!8)) = mono_2Ec_2Ebool_2EF_2E0) | (~(p(mono_2Ec_2Ebool_2EF_2E0) | (~p(mono_2Ec_2Einteger_2Eint__divides_2E2(V0p_2E0!9, mono_2Ec_2Einteger_2Eint__neg_2E1(V1q_2E0!8)))))) | (~((~p(mono_2Ec_2Ebool_2EF_2E0)) | p(mono_2Ec_2Einteger_2Eint__divides_2E2(V0p_2E0!9, mono_2Ec_2Einteger_2Eint__neg_2E1(V1q_2E0!8))))))) <=> ((~![V0t1_2E0: mono_2Etyop_2Emin_2Ebool, V1t2_2E0: mono_2Etyop_2Emin_2Ebool] : ((V0t1_2E0 = V1t2_2E0) | (~((~p(V1t2_2E0)) | p(V0t1_2E0))) | (~(p(V1t2_2E0) | (~p(V0t1_2E0)))))) | (mono_2Ec_2Einteger_2Eint__divides_2E2(V0p_2E0!9, mono_2Ec_2Einteger_2Eint__neg_2E1(V1q_2E0!8)) = mono_2Ec_2Ebool_2EF_2E0) | (~(p(mono_2Ec_2Ebool_2EF_2E0) | (~p(mono_2Ec_2Einteger_2Eint__divides_2E2(V0p_2E0!9, mono_2Ec_2Einteger_2Eint__neg_2E1(V1q_2E0!8)))))) | (~((~p(mono_2Ec_2Ebool_2EF_2E0)) | p(mono_2Ec_2Einteger_2Eint__divides_2E2(V0p_2E0!9, mono_2Ec_2Einteger_2Eint__neg_2E1(V1q_2E0!8))))))),
% 39.06/39.28 inference(rewrite,[status(thm)],[])).
% 39.06/39.28 tff(58,plain,
% 39.06/39.28 (((mono_2Ec_2Einteger_2Eint__divides_2E2(V0p_2E0!9, mono_2Ec_2Einteger_2Eint__neg_2E1(V1q_2E0!8)) = mono_2Ec_2Ebool_2EF_2E0) | (~((~p(mono_2Ec_2Ebool_2EF_2E0)) | p(mono_2Ec_2Einteger_2Eint__divides_2E2(V0p_2E0!9, mono_2Ec_2Einteger_2Eint__neg_2E1(V1q_2E0!8))))) | (~(p(mono_2Ec_2Ebool_2EF_2E0) | (~p(mono_2Ec_2Einteger_2Eint__divides_2E2(V0p_2E0!9, mono_2Ec_2Einteger_2Eint__neg_2E1(V1q_2E0!8))))))) <=> ((mono_2Ec_2Einteger_2Eint__divides_2E2(V0p_2E0!9, mono_2Ec_2Einteger_2Eint__neg_2E1(V1q_2E0!8)) = mono_2Ec_2Ebool_2EF_2E0) | (~(p(mono_2Ec_2Ebool_2EF_2E0) | (~p(mono_2Ec_2Einteger_2Eint__divides_2E2(V0p_2E0!9, mono_2Ec_2Einteger_2Eint__neg_2E1(V1q_2E0!8)))))) | (~((~p(mono_2Ec_2Ebool_2EF_2E0)) | p(mono_2Ec_2Einteger_2Eint__divides_2E2(V0p_2E0!9, mono_2Ec_2Einteger_2Eint__neg_2E1(V1q_2E0!8))))))),
% 39.06/39.28 inference(rewrite,[status(thm)],[])).
% 39.06/39.28 tff(59,plain,
% 39.06/39.28 (((~![V0t1_2E0: mono_2Etyop_2Emin_2Ebool, V1t2_2E0: mono_2Etyop_2Emin_2Ebool] : ((V0t1_2E0 = V1t2_2E0) | (~((~p(V1t2_2E0)) | p(V0t1_2E0))) | (~(p(V1t2_2E0) | (~p(V0t1_2E0)))))) | ((mono_2Ec_2Einteger_2Eint__divides_2E2(V0p_2E0!9, mono_2Ec_2Einteger_2Eint__neg_2E1(V1q_2E0!8)) = mono_2Ec_2Ebool_2EF_2E0) | (~((~p(mono_2Ec_2Ebool_2EF_2E0)) | p(mono_2Ec_2Einteger_2Eint__divides_2E2(V0p_2E0!9, mono_2Ec_2Einteger_2Eint__neg_2E1(V1q_2E0!8))))) | (~(p(mono_2Ec_2Ebool_2EF_2E0) | (~p(mono_2Ec_2Einteger_2Eint__divides_2E2(V0p_2E0!9, mono_2Ec_2Einteger_2Eint__neg_2E1(V1q_2E0!8)))))))) <=> ((~![V0t1_2E0: mono_2Etyop_2Emin_2Ebool, V1t2_2E0: mono_2Etyop_2Emin_2Ebool] : ((V0t1_2E0 = V1t2_2E0) | (~((~p(V1t2_2E0)) | p(V0t1_2E0))) | (~(p(V1t2_2E0) | (~p(V0t1_2E0)))))) | ((mono_2Ec_2Einteger_2Eint__divides_2E2(V0p_2E0!9, mono_2Ec_2Einteger_2Eint__neg_2E1(V1q_2E0!8)) = mono_2Ec_2Ebool_2EF_2E0) | (~(p(mono_2Ec_2Ebool_2EF_2E0) | (~p(mono_2Ec_2Einteger_2Eint__divides_2E2(V0p_2E0!9, mono_2Ec_2Einteger_2Eint__neg_2E1(V1q_2E0!8)))))) | (~((~p(mono_2Ec_2Ebool_2EF_2E0)) | p(mono_2Ec_2Einteger_2Eint__divides_2E2(V0p_2E0!9, mono_2Ec_2Einteger_2Eint__neg_2E1(V1q_2E0!8)))))))),
% 39.06/39.28 inference(monotonicity,[status(thm)],[58])).
% 39.06/39.28 tff(60,plain,
% 39.06/39.28 (((~![V0t1_2E0: mono_2Etyop_2Emin_2Ebool, V1t2_2E0: mono_2Etyop_2Emin_2Ebool] : ((V0t1_2E0 = V1t2_2E0) | (~((~p(V1t2_2E0)) | p(V0t1_2E0))) | (~(p(V1t2_2E0) | (~p(V0t1_2E0)))))) | ((mono_2Ec_2Einteger_2Eint__divides_2E2(V0p_2E0!9, mono_2Ec_2Einteger_2Eint__neg_2E1(V1q_2E0!8)) = mono_2Ec_2Ebool_2EF_2E0) | (~((~p(mono_2Ec_2Ebool_2EF_2E0)) | p(mono_2Ec_2Einteger_2Eint__divides_2E2(V0p_2E0!9, mono_2Ec_2Einteger_2Eint__neg_2E1(V1q_2E0!8))))) | (~(p(mono_2Ec_2Ebool_2EF_2E0) | (~p(mono_2Ec_2Einteger_2Eint__divides_2E2(V0p_2E0!9, mono_2Ec_2Einteger_2Eint__neg_2E1(V1q_2E0!8)))))))) <=> ((~![V0t1_2E0: mono_2Etyop_2Emin_2Ebool, V1t2_2E0: mono_2Etyop_2Emin_2Ebool] : ((V0t1_2E0 = V1t2_2E0) | (~((~p(V1t2_2E0)) | p(V0t1_2E0))) | (~(p(V1t2_2E0) | (~p(V0t1_2E0)))))) | (mono_2Ec_2Einteger_2Eint__divides_2E2(V0p_2E0!9, mono_2Ec_2Einteger_2Eint__neg_2E1(V1q_2E0!8)) = mono_2Ec_2Ebool_2EF_2E0) | (~(p(mono_2Ec_2Ebool_2EF_2E0) | (~p(mono_2Ec_2Einteger_2Eint__divides_2E2(V0p_2E0!9, mono_2Ec_2Einteger_2Eint__neg_2E1(V1q_2E0!8)))))) | (~((~p(mono_2Ec_2Ebool_2EF_2E0)) | p(mono_2Ec_2Einteger_2Eint__divides_2E2(V0p_2E0!9, mono_2Ec_2Einteger_2Eint__neg_2E1(V1q_2E0!8))))))),
% 39.06/39.28 inference(transitivity,[status(thm)],[59, 57])).
% 39.06/39.28 tff(61,plain,
% 39.06/39.28 ((~![V0t1_2E0: mono_2Etyop_2Emin_2Ebool, V1t2_2E0: mono_2Etyop_2Emin_2Ebool] : ((V0t1_2E0 = V1t2_2E0) | (~((~p(V1t2_2E0)) | p(V0t1_2E0))) | (~(p(V1t2_2E0) | (~p(V0t1_2E0)))))) | ((mono_2Ec_2Einteger_2Eint__divides_2E2(V0p_2E0!9, mono_2Ec_2Einteger_2Eint__neg_2E1(V1q_2E0!8)) = mono_2Ec_2Ebool_2EF_2E0) | (~((~p(mono_2Ec_2Ebool_2EF_2E0)) | p(mono_2Ec_2Einteger_2Eint__divides_2E2(V0p_2E0!9, mono_2Ec_2Einteger_2Eint__neg_2E1(V1q_2E0!8))))) | (~(p(mono_2Ec_2Ebool_2EF_2E0) | (~p(mono_2Ec_2Einteger_2Eint__divides_2E2(V0p_2E0!9, mono_2Ec_2Einteger_2Eint__neg_2E1(V1q_2E0!8)))))))),
% 39.06/39.28 inference(quant_inst,[status(thm)],[])).
% 39.06/39.28 tff(62,plain,
% 39.06/39.28 ((~![V0t1_2E0: mono_2Etyop_2Emin_2Ebool, V1t2_2E0: mono_2Etyop_2Emin_2Ebool] : ((V0t1_2E0 = V1t2_2E0) | (~((~p(V1t2_2E0)) | p(V0t1_2E0))) | (~(p(V1t2_2E0) | (~p(V0t1_2E0)))))) | (mono_2Ec_2Einteger_2Eint__divides_2E2(V0p_2E0!9, mono_2Ec_2Einteger_2Eint__neg_2E1(V1q_2E0!8)) = mono_2Ec_2Ebool_2EF_2E0) | (~(p(mono_2Ec_2Ebool_2EF_2E0) | (~p(mono_2Ec_2Einteger_2Eint__divides_2E2(V0p_2E0!9, mono_2Ec_2Einteger_2Eint__neg_2E1(V1q_2E0!8)))))) | (~((~p(mono_2Ec_2Ebool_2EF_2E0)) | p(mono_2Ec_2Einteger_2Eint__divides_2E2(V0p_2E0!9, mono_2Ec_2Einteger_2Eint__neg_2E1(V1q_2E0!8)))))),
% 39.06/39.28 inference(modus_ponens,[status(thm)],[61, 60])).
% 39.06/39.28 tff(63,plain,
% 39.06/39.28 (mono_2Ec_2Einteger_2Eint__divides_2E2(V0p_2E0!9, mono_2Ec_2Einteger_2Eint__neg_2E1(V1q_2E0!8)) = mono_2Ec_2Ebool_2EF_2E0),
% 39.06/39.28 inference(unit_resolution,[status(thm)],[62, 56, 46, 5])).
% 39.06/39.28 tff(64,plain,
% 39.06/39.28 (^[V0p_2E0: mono_2Etyop_2Einteger_2Eint, V1q_2E0: mono_2Etyop_2Einteger_2Eint] : refl((~((~(mono_2Ec_2Einteger_2Eint__divides_2E2(V0p_2E0, mono_2Ec_2Einteger_2Eint__neg_2E1(V1q_2E0)) = mono_2Ec_2Einteger_2Eint__divides_2E2(V0p_2E0, V1q_2E0))) | (~(mono_2Ec_2Einteger_2Eint__divides_2E2(mono_2Ec_2Einteger_2Eint__neg_2E1(V0p_2E0), V1q_2E0) = mono_2Ec_2Einteger_2Eint__divides_2E2(V0p_2E0, V1q_2E0))))) <=> (~((~(mono_2Ec_2Einteger_2Eint__divides_2E2(V0p_2E0, mono_2Ec_2Einteger_2Eint__neg_2E1(V1q_2E0)) = mono_2Ec_2Einteger_2Eint__divides_2E2(V0p_2E0, V1q_2E0))) | (~(mono_2Ec_2Einteger_2Eint__divides_2E2(mono_2Ec_2Einteger_2Eint__neg_2E1(V0p_2E0), V1q_2E0) = mono_2Ec_2Einteger_2Eint__divides_2E2(V0p_2E0, V1q_2E0))))))),
% 39.06/39.28 inference(bind,[status(th)],[])).
% 39.06/39.28 tff(65,plain,
% 39.06/39.28 (![V0p_2E0: mono_2Etyop_2Einteger_2Eint, V1q_2E0: mono_2Etyop_2Einteger_2Eint] : (~((~(mono_2Ec_2Einteger_2Eint__divides_2E2(V0p_2E0, mono_2Ec_2Einteger_2Eint__neg_2E1(V1q_2E0)) = mono_2Ec_2Einteger_2Eint__divides_2E2(V0p_2E0, V1q_2E0))) | (~(mono_2Ec_2Einteger_2Eint__divides_2E2(mono_2Ec_2Einteger_2Eint__neg_2E1(V0p_2E0), V1q_2E0) = mono_2Ec_2Einteger_2Eint__divides_2E2(V0p_2E0, V1q_2E0))))) <=> ![V0p_2E0: mono_2Etyop_2Einteger_2Eint, V1q_2E0: mono_2Etyop_2Einteger_2Eint] : (~((~(mono_2Ec_2Einteger_2Eint__divides_2E2(V0p_2E0, mono_2Ec_2Einteger_2Eint__neg_2E1(V1q_2E0)) = mono_2Ec_2Einteger_2Eint__divides_2E2(V0p_2E0, V1q_2E0))) | (~(mono_2Ec_2Einteger_2Eint__divides_2E2(mono_2Ec_2Einteger_2Eint__neg_2E1(V0p_2E0), V1q_2E0) = mono_2Ec_2Einteger_2Eint__divides_2E2(V0p_2E0, V1q_2E0)))))),
% 39.06/39.28 inference(quant_intro,[status(thm)],[64])).
% 39.06/39.28 tff(66,plain,
% 39.06/39.28 (^[V0p_2E0: mono_2Etyop_2Einteger_2Eint, V1q_2E0: mono_2Etyop_2Einteger_2Eint] : rewrite(((mono_2Ec_2Einteger_2Eint__divides_2E2(V0p_2E0, mono_2Ec_2Einteger_2Eint__neg_2E1(V1q_2E0)) = mono_2Ec_2Einteger_2Eint__divides_2E2(V0p_2E0, V1q_2E0)) & (mono_2Ec_2Einteger_2Eint__divides_2E2(mono_2Ec_2Einteger_2Eint__neg_2E1(V0p_2E0), V1q_2E0) = mono_2Ec_2Einteger_2Eint__divides_2E2(V0p_2E0, V1q_2E0))) <=> (~((~(mono_2Ec_2Einteger_2Eint__divides_2E2(V0p_2E0, mono_2Ec_2Einteger_2Eint__neg_2E1(V1q_2E0)) = mono_2Ec_2Einteger_2Eint__divides_2E2(V0p_2E0, V1q_2E0))) | (~(mono_2Ec_2Einteger_2Eint__divides_2E2(mono_2Ec_2Einteger_2Eint__neg_2E1(V0p_2E0), V1q_2E0) = mono_2Ec_2Einteger_2Eint__divides_2E2(V0p_2E0, V1q_2E0))))))),
% 39.06/39.28 inference(bind,[status(th)],[])).
% 39.06/39.28 tff(67,plain,
% 39.06/39.28 (![V0p_2E0: mono_2Etyop_2Einteger_2Eint, V1q_2E0: mono_2Etyop_2Einteger_2Eint] : ((mono_2Ec_2Einteger_2Eint__divides_2E2(V0p_2E0, mono_2Ec_2Einteger_2Eint__neg_2E1(V1q_2E0)) = mono_2Ec_2Einteger_2Eint__divides_2E2(V0p_2E0, V1q_2E0)) & (mono_2Ec_2Einteger_2Eint__divides_2E2(mono_2Ec_2Einteger_2Eint__neg_2E1(V0p_2E0), V1q_2E0) = mono_2Ec_2Einteger_2Eint__divides_2E2(V0p_2E0, V1q_2E0))) <=> ![V0p_2E0: mono_2Etyop_2Einteger_2Eint, V1q_2E0: mono_2Etyop_2Einteger_2Eint] : (~((~(mono_2Ec_2Einteger_2Eint__divides_2E2(V0p_2E0, mono_2Ec_2Einteger_2Eint__neg_2E1(V1q_2E0)) = mono_2Ec_2Einteger_2Eint__divides_2E2(V0p_2E0, V1q_2E0))) | (~(mono_2Ec_2Einteger_2Eint__divides_2E2(mono_2Ec_2Einteger_2Eint__neg_2E1(V0p_2E0), V1q_2E0) = mono_2Ec_2Einteger_2Eint__divides_2E2(V0p_2E0, V1q_2E0)))))),
% 39.06/39.28 inference(quant_intro,[status(thm)],[66])).
% 39.06/39.28 tff(68,plain,
% 39.06/39.28 (![V0p_2E0: mono_2Etyop_2Einteger_2Eint, V1q_2E0: mono_2Etyop_2Einteger_2Eint] : ((mono_2Ec_2Einteger_2Eint__divides_2E2(V0p_2E0, mono_2Ec_2Einteger_2Eint__neg_2E1(V1q_2E0)) = mono_2Ec_2Einteger_2Eint__divides_2E2(V0p_2E0, V1q_2E0)) & (mono_2Ec_2Einteger_2Eint__divides_2E2(mono_2Ec_2Einteger_2Eint__neg_2E1(V0p_2E0), V1q_2E0) = mono_2Ec_2Einteger_2Eint__divides_2E2(V0p_2E0, V1q_2E0))) <=> ![V0p_2E0: mono_2Etyop_2Einteger_2Eint, V1q_2E0: mono_2Etyop_2Einteger_2Eint] : ((mono_2Ec_2Einteger_2Eint__divides_2E2(V0p_2E0, mono_2Ec_2Einteger_2Eint__neg_2E1(V1q_2E0)) = mono_2Ec_2Einteger_2Eint__divides_2E2(V0p_2E0, V1q_2E0)) & (mono_2Ec_2Einteger_2Eint__divides_2E2(mono_2Ec_2Einteger_2Eint__neg_2E1(V0p_2E0), V1q_2E0) = mono_2Ec_2Einteger_2Eint__divides_2E2(V0p_2E0, V1q_2E0)))),
% 39.06/39.28 inference(rewrite,[status(thm)],[])).
% 39.06/39.28 tff(69,axiom,(![V0p_2E0: mono_2Etyop_2Einteger_2Eint, V1q_2E0: mono_2Etyop_2Einteger_2Eint] : ((mono_2Ec_2Einteger_2Eint__divides_2E2(V0p_2E0, mono_2Ec_2Einteger_2Eint__neg_2E1(V1q_2E0)) = mono_2Ec_2Einteger_2Eint__divides_2E2(V0p_2E0, V1q_2E0)) & (mono_2Ec_2Einteger_2Eint__divides_2E2(mono_2Ec_2Einteger_2Eint__neg_2E1(V0p_2E0), V1q_2E0) = mono_2Ec_2Einteger_2Eint__divides_2E2(V0p_2E0, V1q_2E0)))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','thm_2Einteger_2EINT__DIVIDES__NEG')).
% 39.06/39.28 tff(70,plain,
% 39.06/39.28 (![V0p_2E0: mono_2Etyop_2Einteger_2Eint, V1q_2E0: mono_2Etyop_2Einteger_2Eint] : ((mono_2Ec_2Einteger_2Eint__divides_2E2(V0p_2E0, mono_2Ec_2Einteger_2Eint__neg_2E1(V1q_2E0)) = mono_2Ec_2Einteger_2Eint__divides_2E2(V0p_2E0, V1q_2E0)) & (mono_2Ec_2Einteger_2Eint__divides_2E2(mono_2Ec_2Einteger_2Eint__neg_2E1(V0p_2E0), V1q_2E0) = mono_2Ec_2Einteger_2Eint__divides_2E2(V0p_2E0, V1q_2E0)))),
% 39.06/39.28 inference(modus_ponens,[status(thm)],[69, 68])).
% 39.06/39.28 tff(71,plain,(
% 39.06/39.28 ![V0p_2E0: mono_2Etyop_2Einteger_2Eint, V1q_2E0: mono_2Etyop_2Einteger_2Eint] : ((mono_2Ec_2Einteger_2Eint__divides_2E2(V0p_2E0, mono_2Ec_2Einteger_2Eint__neg_2E1(V1q_2E0)) = mono_2Ec_2Einteger_2Eint__divides_2E2(V0p_2E0, V1q_2E0)) & (mono_2Ec_2Einteger_2Eint__divides_2E2(mono_2Ec_2Einteger_2Eint__neg_2E1(V0p_2E0), V1q_2E0) = mono_2Ec_2Einteger_2Eint__divides_2E2(V0p_2E0, V1q_2E0)))),
% 39.06/39.28 inference(skolemize,[status(sab)],[70])).
% 39.06/39.28 tff(72,plain,
% 39.06/39.28 (![V0p_2E0: mono_2Etyop_2Einteger_2Eint, V1q_2E0: mono_2Etyop_2Einteger_2Eint] : (~((~(mono_2Ec_2Einteger_2Eint__divides_2E2(V0p_2E0, mono_2Ec_2Einteger_2Eint__neg_2E1(V1q_2E0)) = mono_2Ec_2Einteger_2Eint__divides_2E2(V0p_2E0, V1q_2E0))) | (~(mono_2Ec_2Einteger_2Eint__divides_2E2(mono_2Ec_2Einteger_2Eint__neg_2E1(V0p_2E0), V1q_2E0) = mono_2Ec_2Einteger_2Eint__divides_2E2(V0p_2E0, V1q_2E0)))))),
% 39.06/39.28 inference(modus_ponens,[status(thm)],[71, 67])).
% 39.06/39.28 tff(73,plain,
% 39.06/39.28 (![V0p_2E0: mono_2Etyop_2Einteger_2Eint, V1q_2E0: mono_2Etyop_2Einteger_2Eint] : (~((~(mono_2Ec_2Einteger_2Eint__divides_2E2(V0p_2E0, mono_2Ec_2Einteger_2Eint__neg_2E1(V1q_2E0)) = mono_2Ec_2Einteger_2Eint__divides_2E2(V0p_2E0, V1q_2E0))) | (~(mono_2Ec_2Einteger_2Eint__divides_2E2(mono_2Ec_2Einteger_2Eint__neg_2E1(V0p_2E0), V1q_2E0) = mono_2Ec_2Einteger_2Eint__divides_2E2(V0p_2E0, V1q_2E0)))))),
% 39.06/39.28 inference(modus_ponens,[status(thm)],[72, 65])).
% 39.06/39.28 tff(74,plain,
% 39.06/39.28 ((~![V0p_2E0: mono_2Etyop_2Einteger_2Eint, V1q_2E0: mono_2Etyop_2Einteger_2Eint] : (~((~(mono_2Ec_2Einteger_2Eint__divides_2E2(V0p_2E0, mono_2Ec_2Einteger_2Eint__neg_2E1(V1q_2E0)) = mono_2Ec_2Einteger_2Eint__divides_2E2(V0p_2E0, V1q_2E0))) | (~(mono_2Ec_2Einteger_2Eint__divides_2E2(mono_2Ec_2Einteger_2Eint__neg_2E1(V0p_2E0), V1q_2E0) = mono_2Ec_2Einteger_2Eint__divides_2E2(V0p_2E0, V1q_2E0)))))) | (~((~(mono_2Ec_2Einteger_2Eint__divides_2E2(V0p_2E0!9, mono_2Ec_2Einteger_2Eint__neg_2E1(V1q_2E0!8)) = mono_2Ec_2Einteger_2Eint__divides_2E2(V0p_2E0!9, V1q_2E0!8))) | (~(mono_2Ec_2Einteger_2Eint__divides_2E2(mono_2Ec_2Einteger_2Eint__neg_2E1(V0p_2E0!9), V1q_2E0!8) = mono_2Ec_2Einteger_2Eint__divides_2E2(V0p_2E0!9, V1q_2E0!8)))))),
% 39.06/39.28 inference(quant_inst,[status(thm)],[])).
% 39.06/39.28 tff(75,plain,
% 39.06/39.28 (~((~(mono_2Ec_2Einteger_2Eint__divides_2E2(V0p_2E0!9, mono_2Ec_2Einteger_2Eint__neg_2E1(V1q_2E0!8)) = mono_2Ec_2Einteger_2Eint__divides_2E2(V0p_2E0!9, V1q_2E0!8))) | (~(mono_2Ec_2Einteger_2Eint__divides_2E2(mono_2Ec_2Einteger_2Eint__neg_2E1(V0p_2E0!9), V1q_2E0!8) = mono_2Ec_2Einteger_2Eint__divides_2E2(V0p_2E0!9, V1q_2E0!8))))),
% 39.06/39.28 inference(unit_resolution,[status(thm)],[74, 73])).
% 39.06/39.28 tff(76,plain,
% 39.06/39.28 (((~(mono_2Ec_2Einteger_2Eint__divides_2E2(V0p_2E0!9, mono_2Ec_2Einteger_2Eint__neg_2E1(V1q_2E0!8)) = mono_2Ec_2Einteger_2Eint__divides_2E2(V0p_2E0!9, V1q_2E0!8))) | (~(mono_2Ec_2Einteger_2Eint__divides_2E2(mono_2Ec_2Einteger_2Eint__neg_2E1(V0p_2E0!9), V1q_2E0!8) = mono_2Ec_2Einteger_2Eint__divides_2E2(V0p_2E0!9, V1q_2E0!8)))) | (mono_2Ec_2Einteger_2Eint__divides_2E2(V0p_2E0!9, mono_2Ec_2Einteger_2Eint__neg_2E1(V1q_2E0!8)) = mono_2Ec_2Einteger_2Eint__divides_2E2(V0p_2E0!9, V1q_2E0!8))),
% 39.06/39.28 inference(tautology,[status(thm)],[])).
% 39.06/39.28 tff(77,plain,
% 39.06/39.28 (mono_2Ec_2Einteger_2Eint__divides_2E2(V0p_2E0!9, mono_2Ec_2Einteger_2Eint__neg_2E1(V1q_2E0!8)) = mono_2Ec_2Einteger_2Eint__divides_2E2(V0p_2E0!9, V1q_2E0!8)),
% 39.06/39.28 inference(unit_resolution,[status(thm)],[76, 75])).
% 39.06/39.28 tff(78,plain,
% 39.06/39.28 (mono_2Ec_2Einteger_2Eint__divides_2E2(V0p_2E0!9, V1q_2E0!8) = mono_2Ec_2Einteger_2Eint__divides_2E2(V0p_2E0!9, mono_2Ec_2Einteger_2Eint__neg_2E1(V1q_2E0!8))),
% 39.06/39.28 inference(symmetry,[status(thm)],[77])).
% 39.06/39.28 tff(79,plain,
% 39.06/39.28 (p(mono_2Ec_2Ebool_2ET_2E0) <=> p(mono_2Ec_2Ebool_2ET_2E0)),
% 39.06/39.28 inference(rewrite,[status(thm)],[])).
% 39.06/39.28 tff(80,axiom,(p(mono_2Ec_2Ebool_2ET_2E0)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','reserved_2Eho_2Etruth')).
% 39.06/39.28 tff(81,plain,
% 39.06/39.28 (p(mono_2Ec_2Ebool_2ET_2E0)),
% 39.06/39.28 inference(modus_ponens,[status(thm)],[80, 79])).
% 39.06/39.28 tff(82,plain,
% 39.06/39.28 ((p(mono_2Ec_2Ebool_2ET_2E0) | (~p(mono_2Ec_2Einteger_2Eint__divides_2E2(V0p_2E0!9, V1q_2E0!8)))) | (~p(mono_2Ec_2Ebool_2ET_2E0))),
% 39.06/39.28 inference(tautology,[status(thm)],[])).
% 39.06/39.28 tff(83,plain,
% 39.06/39.28 (p(mono_2Ec_2Ebool_2ET_2E0) | (~p(mono_2Ec_2Einteger_2Eint__divides_2E2(V0p_2E0!9, V1q_2E0!8)))),
% 39.06/39.28 inference(unit_resolution,[status(thm)],[82, 81])).
% 39.06/39.28 tff(84,plain,
% 39.06/39.28 (p(mono_2Ec_2Einteger_2Eint__divides_2E2(V0p_2E0!9, V1q_2E0!8))),
% 39.06/39.28 inference(or_elim,[status(thm)],[27])).
% 39.06/39.28 tff(85,plain,
% 39.06/39.28 (((~p(mono_2Ec_2Ebool_2ET_2E0)) | p(mono_2Ec_2Einteger_2Eint__divides_2E2(V0p_2E0!9, V1q_2E0!8))) | (~p(mono_2Ec_2Einteger_2Eint__divides_2E2(V0p_2E0!9, V1q_2E0!8)))),
% 39.06/39.28 inference(tautology,[status(thm)],[])).
% 39.06/39.28 tff(86,plain,
% 39.06/39.28 ((~p(mono_2Ec_2Ebool_2ET_2E0)) | p(mono_2Ec_2Einteger_2Eint__divides_2E2(V0p_2E0!9, V1q_2E0!8))),
% 39.06/39.28 inference(unit_resolution,[status(thm)],[85, 84])).
% 39.06/39.28 tff(87,plain,
% 39.06/39.28 (((~![V0t1_2E0: mono_2Etyop_2Emin_2Ebool, V1t2_2E0: mono_2Etyop_2Emin_2Ebool] : ((V0t1_2E0 = V1t2_2E0) | (~((~p(V1t2_2E0)) | p(V0t1_2E0))) | (~(p(V1t2_2E0) | (~p(V0t1_2E0)))))) | ((~((~p(mono_2Ec_2Ebool_2ET_2E0)) | p(mono_2Ec_2Einteger_2Eint__divides_2E2(V0p_2E0!9, V1q_2E0!8)))) | (mono_2Ec_2Einteger_2Eint__divides_2E2(V0p_2E0!9, V1q_2E0!8) = mono_2Ec_2Ebool_2ET_2E0) | (~(p(mono_2Ec_2Ebool_2ET_2E0) | (~p(mono_2Ec_2Einteger_2Eint__divides_2E2(V0p_2E0!9, V1q_2E0!8))))))) <=> ((~![V0t1_2E0: mono_2Etyop_2Emin_2Ebool, V1t2_2E0: mono_2Etyop_2Emin_2Ebool] : ((V0t1_2E0 = V1t2_2E0) | (~((~p(V1t2_2E0)) | p(V0t1_2E0))) | (~(p(V1t2_2E0) | (~p(V0t1_2E0)))))) | (~((~p(mono_2Ec_2Ebool_2ET_2E0)) | p(mono_2Ec_2Einteger_2Eint__divides_2E2(V0p_2E0!9, V1q_2E0!8)))) | (mono_2Ec_2Einteger_2Eint__divides_2E2(V0p_2E0!9, V1q_2E0!8) = mono_2Ec_2Ebool_2ET_2E0) | (~(p(mono_2Ec_2Ebool_2ET_2E0) | (~p(mono_2Ec_2Einteger_2Eint__divides_2E2(V0p_2E0!9, V1q_2E0!8))))))),
% 39.06/39.28 inference(rewrite,[status(thm)],[])).
% 39.06/39.28 tff(88,plain,
% 39.06/39.28 (((mono_2Ec_2Einteger_2Eint__divides_2E2(V0p_2E0!9, V1q_2E0!8) = mono_2Ec_2Ebool_2ET_2E0) | (~((~p(mono_2Ec_2Ebool_2ET_2E0)) | p(mono_2Ec_2Einteger_2Eint__divides_2E2(V0p_2E0!9, V1q_2E0!8)))) | (~(p(mono_2Ec_2Ebool_2ET_2E0) | (~p(mono_2Ec_2Einteger_2Eint__divides_2E2(V0p_2E0!9, V1q_2E0!8)))))) <=> ((~((~p(mono_2Ec_2Ebool_2ET_2E0)) | p(mono_2Ec_2Einteger_2Eint__divides_2E2(V0p_2E0!9, V1q_2E0!8)))) | (mono_2Ec_2Einteger_2Eint__divides_2E2(V0p_2E0!9, V1q_2E0!8) = mono_2Ec_2Ebool_2ET_2E0) | (~(p(mono_2Ec_2Ebool_2ET_2E0) | (~p(mono_2Ec_2Einteger_2Eint__divides_2E2(V0p_2E0!9, V1q_2E0!8))))))),
% 39.06/39.28 inference(rewrite,[status(thm)],[])).
% 39.06/39.28 tff(89,plain,
% 39.06/39.28 (((~![V0t1_2E0: mono_2Etyop_2Emin_2Ebool, V1t2_2E0: mono_2Etyop_2Emin_2Ebool] : ((V0t1_2E0 = V1t2_2E0) | (~((~p(V1t2_2E0)) | p(V0t1_2E0))) | (~(p(V1t2_2E0) | (~p(V0t1_2E0)))))) | ((mono_2Ec_2Einteger_2Eint__divides_2E2(V0p_2E0!9, V1q_2E0!8) = mono_2Ec_2Ebool_2ET_2E0) | (~((~p(mono_2Ec_2Ebool_2ET_2E0)) | p(mono_2Ec_2Einteger_2Eint__divides_2E2(V0p_2E0!9, V1q_2E0!8)))) | (~(p(mono_2Ec_2Ebool_2ET_2E0) | (~p(mono_2Ec_2Einteger_2Eint__divides_2E2(V0p_2E0!9, V1q_2E0!8))))))) <=> ((~![V0t1_2E0: mono_2Etyop_2Emin_2Ebool, V1t2_2E0: mono_2Etyop_2Emin_2Ebool] : ((V0t1_2E0 = V1t2_2E0) | (~((~p(V1t2_2E0)) | p(V0t1_2E0))) | (~(p(V1t2_2E0) | (~p(V0t1_2E0)))))) | ((~((~p(mono_2Ec_2Ebool_2ET_2E0)) | p(mono_2Ec_2Einteger_2Eint__divides_2E2(V0p_2E0!9, V1q_2E0!8)))) | (mono_2Ec_2Einteger_2Eint__divides_2E2(V0p_2E0!9, V1q_2E0!8) = mono_2Ec_2Ebool_2ET_2E0) | (~(p(mono_2Ec_2Ebool_2ET_2E0) | (~p(mono_2Ec_2Einteger_2Eint__divides_2E2(V0p_2E0!9, V1q_2E0!8)))))))),
% 39.06/39.28 inference(monotonicity,[status(thm)],[88])).
% 39.06/39.28 tff(90,plain,
% 39.06/39.28 (((~![V0t1_2E0: mono_2Etyop_2Emin_2Ebool, V1t2_2E0: mono_2Etyop_2Emin_2Ebool] : ((V0t1_2E0 = V1t2_2E0) | (~((~p(V1t2_2E0)) | p(V0t1_2E0))) | (~(p(V1t2_2E0) | (~p(V0t1_2E0)))))) | ((mono_2Ec_2Einteger_2Eint__divides_2E2(V0p_2E0!9, V1q_2E0!8) = mono_2Ec_2Ebool_2ET_2E0) | (~((~p(mono_2Ec_2Ebool_2ET_2E0)) | p(mono_2Ec_2Einteger_2Eint__divides_2E2(V0p_2E0!9, V1q_2E0!8)))) | (~(p(mono_2Ec_2Ebool_2ET_2E0) | (~p(mono_2Ec_2Einteger_2Eint__divides_2E2(V0p_2E0!9, V1q_2E0!8))))))) <=> ((~![V0t1_2E0: mono_2Etyop_2Emin_2Ebool, V1t2_2E0: mono_2Etyop_2Emin_2Ebool] : ((V0t1_2E0 = V1t2_2E0) | (~((~p(V1t2_2E0)) | p(V0t1_2E0))) | (~(p(V1t2_2E0) | (~p(V0t1_2E0)))))) | (~((~p(mono_2Ec_2Ebool_2ET_2E0)) | p(mono_2Ec_2Einteger_2Eint__divides_2E2(V0p_2E0!9, V1q_2E0!8)))) | (mono_2Ec_2Einteger_2Eint__divides_2E2(V0p_2E0!9, V1q_2E0!8) = mono_2Ec_2Ebool_2ET_2E0) | (~(p(mono_2Ec_2Ebool_2ET_2E0) | (~p(mono_2Ec_2Einteger_2Eint__divides_2E2(V0p_2E0!9, V1q_2E0!8))))))),
% 39.06/39.28 inference(transitivity,[status(thm)],[89, 87])).
% 39.06/39.28 tff(91,plain,
% 39.06/39.28 ((~![V0t1_2E0: mono_2Etyop_2Emin_2Ebool, V1t2_2E0: mono_2Etyop_2Emin_2Ebool] : ((V0t1_2E0 = V1t2_2E0) | (~((~p(V1t2_2E0)) | p(V0t1_2E0))) | (~(p(V1t2_2E0) | (~p(V0t1_2E0)))))) | ((mono_2Ec_2Einteger_2Eint__divides_2E2(V0p_2E0!9, V1q_2E0!8) = mono_2Ec_2Ebool_2ET_2E0) | (~((~p(mono_2Ec_2Ebool_2ET_2E0)) | p(mono_2Ec_2Einteger_2Eint__divides_2E2(V0p_2E0!9, V1q_2E0!8)))) | (~(p(mono_2Ec_2Ebool_2ET_2E0) | (~p(mono_2Ec_2Einteger_2Eint__divides_2E2(V0p_2E0!9, V1q_2E0!8))))))),
% 39.06/39.28 inference(quant_inst,[status(thm)],[])).
% 39.06/39.28 tff(92,plain,
% 39.06/39.28 ((~![V0t1_2E0: mono_2Etyop_2Emin_2Ebool, V1t2_2E0: mono_2Etyop_2Emin_2Ebool] : ((V0t1_2E0 = V1t2_2E0) | (~((~p(V1t2_2E0)) | p(V0t1_2E0))) | (~(p(V1t2_2E0) | (~p(V0t1_2E0)))))) | (~((~p(mono_2Ec_2Ebool_2ET_2E0)) | p(mono_2Ec_2Einteger_2Eint__divides_2E2(V0p_2E0!9, V1q_2E0!8)))) | (mono_2Ec_2Einteger_2Eint__divides_2E2(V0p_2E0!9, V1q_2E0!8) = mono_2Ec_2Ebool_2ET_2E0) | (~(p(mono_2Ec_2Ebool_2ET_2E0) | (~p(mono_2Ec_2Einteger_2Eint__divides_2E2(V0p_2E0!9, V1q_2E0!8)))))),
% 39.06/39.28 inference(modus_ponens,[status(thm)],[91, 90])).
% 39.06/39.28 tff(93,plain,
% 39.06/39.28 (mono_2Ec_2Einteger_2Eint__divides_2E2(V0p_2E0!9, V1q_2E0!8) = mono_2Ec_2Ebool_2ET_2E0),
% 39.06/39.28 inference(unit_resolution,[status(thm)],[92, 56, 86, 83])).
% 39.06/39.28 tff(94,plain,
% 39.06/39.28 (mono_2Ec_2Ebool_2ET_2E0 = mono_2Ec_2Einteger_2Eint__divides_2E2(V0p_2E0!9, V1q_2E0!8)),
% 39.06/39.28 inference(symmetry,[status(thm)],[93])).
% 39.06/39.28 tff(95,plain,
% 39.06/39.28 (mono_2Ec_2Ebool_2ET_2E0 = mono_2Ec_2Ebool_2EF_2E0),
% 39.06/39.28 inference(transitivity,[status(thm)],[94, 78, 63])).
% 39.06/39.28 tff(96,plain,
% 39.06/39.28 (^[V0r_2E0: mono_2Etyop_2Emin_2Ebool, V1q_2E0: mono_2Etyop_2Emin_2Ebool, V2p_2E0: mono_2Etyop_2Emin_2Ebool] : refl((~(((~(p(V2p_2E0) | p(V1q_2E0) | p(V0r_2E0))) | (~(p(V2p_2E0) | (~p(V1q_2E0)) | (~p(V0r_2E0)))) | (~((~p(V2p_2E0)) | p(V1q_2E0) | (~p(V0r_2E0)))) | (~((~p(V2p_2E0)) | p(V0r_2E0) | (~p(V1q_2E0))))) <=> (p(V2p_2E0) <=> (V1q_2E0 = V0r_2E0)))) <=> (~(((~(p(V2p_2E0) | p(V1q_2E0) | p(V0r_2E0))) | (~(p(V2p_2E0) | (~p(V1q_2E0)) | (~p(V0r_2E0)))) | (~((~p(V2p_2E0)) | p(V1q_2E0) | (~p(V0r_2E0)))) | (~((~p(V2p_2E0)) | p(V0r_2E0) | (~p(V1q_2E0))))) <=> (p(V2p_2E0) <=> (V1q_2E0 = V0r_2E0)))))),
% 39.06/39.28 inference(bind,[status(th)],[])).
% 39.06/39.28 tff(97,plain,
% 39.06/39.28 (![V0r_2E0: mono_2Etyop_2Emin_2Ebool, V1q_2E0: mono_2Etyop_2Emin_2Ebool, V2p_2E0: mono_2Etyop_2Emin_2Ebool] : (~(((~(p(V2p_2E0) | p(V1q_2E0) | p(V0r_2E0))) | (~(p(V2p_2E0) | (~p(V1q_2E0)) | (~p(V0r_2E0)))) | (~((~p(V2p_2E0)) | p(V1q_2E0) | (~p(V0r_2E0)))) | (~((~p(V2p_2E0)) | p(V0r_2E0) | (~p(V1q_2E0))))) <=> (p(V2p_2E0) <=> (V1q_2E0 = V0r_2E0)))) <=> ![V0r_2E0: mono_2Etyop_2Emin_2Ebool, V1q_2E0: mono_2Etyop_2Emin_2Ebool, V2p_2E0: mono_2Etyop_2Emin_2Ebool] : (~(((~(p(V2p_2E0) | p(V1q_2E0) | p(V0r_2E0))) | (~(p(V2p_2E0) | (~p(V1q_2E0)) | (~p(V0r_2E0)))) | (~((~p(V2p_2E0)) | p(V1q_2E0) | (~p(V0r_2E0)))) | (~((~p(V2p_2E0)) | p(V0r_2E0) | (~p(V1q_2E0))))) <=> (p(V2p_2E0) <=> (V1q_2E0 = V0r_2E0))))),
% 39.06/39.28 inference(quant_intro,[status(thm)],[96])).
% 39.06/39.28 tff(98,plain,
% 39.06/39.28 (^[V0r_2E0: mono_2Etyop_2Emin_2Ebool, V1q_2E0: mono_2Etyop_2Emin_2Ebool, V2p_2E0: mono_2Etyop_2Emin_2Ebool] : trans(trans(monotonicity(trans(monotonicity(rewrite(((~p(V2p_2E0)) | p(V1q_2E0) | (~p(V0r_2E0))) <=> ((~p(V2p_2E0)) | p(V1q_2E0) | (~p(V0r_2E0)))), rewrite(((~p(V2p_2E0)) | p(V0r_2E0) | (~p(V1q_2E0))) <=> ((~p(V2p_2E0)) | p(V0r_2E0) | (~p(V1q_2E0)))), (((p(V2p_2E0) | p(V1q_2E0) | p(V0r_2E0)) & (p(V2p_2E0) | (~p(V1q_2E0)) | (~p(V0r_2E0))) & ((~p(V2p_2E0)) | p(V1q_2E0) | (~p(V0r_2E0))) & ((~p(V2p_2E0)) | p(V0r_2E0) | (~p(V1q_2E0)))) <=> ((p(V2p_2E0) | p(V1q_2E0) | p(V0r_2E0)) & (p(V2p_2E0) | (~p(V1q_2E0)) | (~p(V0r_2E0))) & ((~p(V2p_2E0)) | p(V1q_2E0) | (~p(V0r_2E0))) & ((~p(V2p_2E0)) | p(V0r_2E0) | (~p(V1q_2E0)))))), rewrite(((p(V2p_2E0) | p(V1q_2E0) | p(V0r_2E0)) & (p(V2p_2E0) | (~p(V1q_2E0)) | (~p(V0r_2E0))) & ((~p(V2p_2E0)) | p(V1q_2E0) | (~p(V0r_2E0))) & ((~p(V2p_2E0)) | p(V0r_2E0) | (~p(V1q_2E0)))) <=> (~((~(p(V2p_2E0) | p(V1q_2E0) | p(V0r_2E0))) | (~(p(V2p_2E0) | (~p(V1q_2E0)) | (~p(V0r_2E0)))) | (~((~p(V2p_2E0)) | p(V1q_2E0) | (~p(V0r_2E0)))) | (~((~p(V2p_2E0)) | p(V0r_2E0) | (~p(V1q_2E0))))))), (((p(V2p_2E0) | p(V1q_2E0) | p(V0r_2E0)) & (p(V2p_2E0) | (~p(V1q_2E0)) | (~p(V0r_2E0))) & ((~p(V2p_2E0)) | p(V1q_2E0) | (~p(V0r_2E0))) & ((~p(V2p_2E0)) | p(V0r_2E0) | (~p(V1q_2E0)))) <=> (~((~(p(V2p_2E0) | p(V1q_2E0) | p(V0r_2E0))) | (~(p(V2p_2E0) | (~p(V1q_2E0)) | (~p(V0r_2E0)))) | (~((~p(V2p_2E0)) | p(V1q_2E0) | (~p(V0r_2E0)))) | (~((~p(V2p_2E0)) | p(V0r_2E0) | (~p(V1q_2E0)))))))), (((p(V2p_2E0) <=> (V1q_2E0 = V0r_2E0)) <=> ((p(V2p_2E0) | p(V1q_2E0) | p(V0r_2E0)) & (p(V2p_2E0) | (~p(V1q_2E0)) | (~p(V0r_2E0))) & ((~p(V2p_2E0)) | p(V1q_2E0) | (~p(V0r_2E0))) & ((~p(V2p_2E0)) | p(V0r_2E0) | (~p(V1q_2E0))))) <=> ((p(V2p_2E0) <=> (V1q_2E0 = V0r_2E0)) <=> (~((~(p(V2p_2E0) | p(V1q_2E0) | p(V0r_2E0))) | (~(p(V2p_2E0) | (~p(V1q_2E0)) | (~p(V0r_2E0)))) | (~((~p(V2p_2E0)) | p(V1q_2E0) | (~p(V0r_2E0)))) | (~((~p(V2p_2E0)) | p(V0r_2E0) | (~p(V1q_2E0))))))))), rewrite(((p(V2p_2E0) <=> (V1q_2E0 = V0r_2E0)) <=> (~((~(p(V2p_2E0) | p(V1q_2E0) | p(V0r_2E0))) | (~(p(V2p_2E0) | (~p(V1q_2E0)) | (~p(V0r_2E0)))) | (~((~p(V2p_2E0)) | p(V1q_2E0) | (~p(V0r_2E0)))) | (~((~p(V2p_2E0)) | p(V0r_2E0) | (~p(V1q_2E0))))))) <=> (~(((~(p(V2p_2E0) | p(V1q_2E0) | p(V0r_2E0))) | (~(p(V2p_2E0) | (~p(V1q_2E0)) | (~p(V0r_2E0)))) | (~((~p(V2p_2E0)) | p(V1q_2E0) | (~p(V0r_2E0)))) | (~((~p(V2p_2E0)) | p(V0r_2E0) | (~p(V1q_2E0))))) <=> (p(V2p_2E0) <=> (V1q_2E0 = V0r_2E0))))), (((p(V2p_2E0) <=> (V1q_2E0 = V0r_2E0)) <=> ((p(V2p_2E0) | p(V1q_2E0) | p(V0r_2E0)) & (p(V2p_2E0) | (~p(V1q_2E0)) | (~p(V0r_2E0))) & ((~p(V2p_2E0)) | p(V1q_2E0) | (~p(V0r_2E0))) & ((~p(V2p_2E0)) | p(V0r_2E0) | (~p(V1q_2E0))))) <=> (~(((~(p(V2p_2E0) | p(V1q_2E0) | p(V0r_2E0))) | (~(p(V2p_2E0) | (~p(V1q_2E0)) | (~p(V0r_2E0)))) | (~((~p(V2p_2E0)) | p(V1q_2E0) | (~p(V0r_2E0)))) | (~((~p(V2p_2E0)) | p(V0r_2E0) | (~p(V1q_2E0))))) <=> (p(V2p_2E0) <=> (V1q_2E0 = V0r_2E0)))))), rewrite((~(((~(p(V2p_2E0) | p(V1q_2E0) | p(V0r_2E0))) | (~(p(V2p_2E0) | (~p(V1q_2E0)) | (~p(V0r_2E0)))) | (~((~p(V2p_2E0)) | p(V1q_2E0) | (~p(V0r_2E0)))) | (~((~p(V2p_2E0)) | p(V0r_2E0) | (~p(V1q_2E0))))) <=> (p(V2p_2E0) <=> (V1q_2E0 = V0r_2E0)))) <=> (~(((~(p(V2p_2E0) | p(V1q_2E0) | p(V0r_2E0))) | (~(p(V2p_2E0) | (~p(V1q_2E0)) | (~p(V0r_2E0)))) | (~((~p(V2p_2E0)) | p(V1q_2E0) | (~p(V0r_2E0)))) | (~((~p(V2p_2E0)) | p(V0r_2E0) | (~p(V1q_2E0))))) <=> (p(V2p_2E0) <=> (V1q_2E0 = V0r_2E0))))), (((p(V2p_2E0) <=> (V1q_2E0 = V0r_2E0)) <=> ((p(V2p_2E0) | p(V1q_2E0) | p(V0r_2E0)) & (p(V2p_2E0) | (~p(V1q_2E0)) | (~p(V0r_2E0))) & ((~p(V2p_2E0)) | p(V1q_2E0) | (~p(V0r_2E0))) & ((~p(V2p_2E0)) | p(V0r_2E0) | (~p(V1q_2E0))))) <=> (~(((~(p(V2p_2E0) | p(V1q_2E0) | p(V0r_2E0))) | (~(p(V2p_2E0) | (~p(V1q_2E0)) | (~p(V0r_2E0)))) | (~((~p(V2p_2E0)) | p(V1q_2E0) | (~p(V0r_2E0)))) | (~((~p(V2p_2E0)) | p(V0r_2E0) | (~p(V1q_2E0))))) <=> (p(V2p_2E0) <=> (V1q_2E0 = V0r_2E0))))))),
% 39.06/39.28 inference(bind,[status(th)],[])).
% 39.06/39.28 tff(99,plain,
% 39.06/39.28 (![V0r_2E0: mono_2Etyop_2Emin_2Ebool, V1q_2E0: mono_2Etyop_2Emin_2Ebool, V2p_2E0: mono_2Etyop_2Emin_2Ebool] : ((p(V2p_2E0) <=> (V1q_2E0 = V0r_2E0)) <=> ((p(V2p_2E0) | p(V1q_2E0) | p(V0r_2E0)) & (p(V2p_2E0) | (~p(V1q_2E0)) | (~p(V0r_2E0))) & ((~p(V2p_2E0)) | p(V1q_2E0) | (~p(V0r_2E0))) & ((~p(V2p_2E0)) | p(V0r_2E0) | (~p(V1q_2E0))))) <=> ![V0r_2E0: mono_2Etyop_2Emin_2Ebool, V1q_2E0: mono_2Etyop_2Emin_2Ebool, V2p_2E0: mono_2Etyop_2Emin_2Ebool] : (~(((~(p(V2p_2E0) | p(V1q_2E0) | p(V0r_2E0))) | (~(p(V2p_2E0) | (~p(V1q_2E0)) | (~p(V0r_2E0)))) | (~((~p(V2p_2E0)) | p(V1q_2E0) | (~p(V0r_2E0)))) | (~((~p(V2p_2E0)) | p(V0r_2E0) | (~p(V1q_2E0))))) <=> (p(V2p_2E0) <=> (V1q_2E0 = V0r_2E0))))),
% 39.06/39.28 inference(quant_intro,[status(thm)],[98])).
% 39.06/39.28 tff(100,plain,
% 39.06/39.28 (![V0r_2E0: mono_2Etyop_2Emin_2Ebool, V1q_2E0: mono_2Etyop_2Emin_2Ebool, V2p_2E0: mono_2Etyop_2Emin_2Ebool] : ((p(V2p_2E0) <=> (V1q_2E0 = V0r_2E0)) <=> ((p(V2p_2E0) | p(V1q_2E0) | p(V0r_2E0)) & (p(V2p_2E0) | (~p(V1q_2E0)) | (~p(V0r_2E0))) & ((~p(V2p_2E0)) | p(V1q_2E0) | (~p(V0r_2E0))) & ((~p(V2p_2E0)) | p(V0r_2E0) | (~p(V1q_2E0))))) <=> ![V0r_2E0: mono_2Etyop_2Emin_2Ebool, V1q_2E0: mono_2Etyop_2Emin_2Ebool, V2p_2E0: mono_2Etyop_2Emin_2Ebool] : ((p(V2p_2E0) <=> (V1q_2E0 = V0r_2E0)) <=> ((p(V2p_2E0) | p(V1q_2E0) | p(V0r_2E0)) & (p(V2p_2E0) | (~p(V1q_2E0)) | (~p(V0r_2E0))) & ((~p(V2p_2E0)) | p(V1q_2E0) | (~p(V0r_2E0))) & ((~p(V2p_2E0)) | p(V0r_2E0) | (~p(V1q_2E0)))))),
% 39.06/39.28 inference(rewrite,[status(thm)],[])).
% 39.06/39.28 tff(101,plain,
% 39.06/39.28 (^[V0r_2E0: mono_2Etyop_2Emin_2Ebool, V1q_2E0: mono_2Etyop_2Emin_2Ebool, V2p_2E0: mono_2Etyop_2Emin_2Ebool] : rewrite(((p(V2p_2E0) <=> (V1q_2E0 = V0r_2E0)) <=> (((((p(V2p_2E0) | p(V1q_2E0)) | p(V0r_2E0)) & ((p(V2p_2E0) | (~p(V0r_2E0))) | (~p(V1q_2E0)))) & ((p(V1q_2E0) | (~p(V0r_2E0))) | (~p(V2p_2E0)))) & ((p(V0r_2E0) | (~p(V1q_2E0))) | (~p(V2p_2E0))))) <=> ((p(V2p_2E0) <=> (V1q_2E0 = V0r_2E0)) <=> ((p(V2p_2E0) | p(V1q_2E0) | p(V0r_2E0)) & (p(V2p_2E0) | (~p(V1q_2E0)) | (~p(V0r_2E0))) & ((~p(V2p_2E0)) | p(V1q_2E0) | (~p(V0r_2E0))) & ((~p(V2p_2E0)) | p(V0r_2E0) | (~p(V1q_2E0))))))),
% 39.06/39.28 inference(bind,[status(th)],[])).
% 39.06/39.28 tff(102,plain,
% 39.06/39.28 (![V0r_2E0: mono_2Etyop_2Emin_2Ebool, V1q_2E0: mono_2Etyop_2Emin_2Ebool, V2p_2E0: mono_2Etyop_2Emin_2Ebool] : ((p(V2p_2E0) <=> (V1q_2E0 = V0r_2E0)) <=> (((((p(V2p_2E0) | p(V1q_2E0)) | p(V0r_2E0)) & ((p(V2p_2E0) | (~p(V0r_2E0))) | (~p(V1q_2E0)))) & ((p(V1q_2E0) | (~p(V0r_2E0))) | (~p(V2p_2E0)))) & ((p(V0r_2E0) | (~p(V1q_2E0))) | (~p(V2p_2E0))))) <=> ![V0r_2E0: mono_2Etyop_2Emin_2Ebool, V1q_2E0: mono_2Etyop_2Emin_2Ebool, V2p_2E0: mono_2Etyop_2Emin_2Ebool] : ((p(V2p_2E0) <=> (V1q_2E0 = V0r_2E0)) <=> ((p(V2p_2E0) | p(V1q_2E0) | p(V0r_2E0)) & (p(V2p_2E0) | (~p(V1q_2E0)) | (~p(V0r_2E0))) & ((~p(V2p_2E0)) | p(V1q_2E0) | (~p(V0r_2E0))) & ((~p(V2p_2E0)) | p(V0r_2E0) | (~p(V1q_2E0)))))),
% 39.06/39.28 inference(quant_intro,[status(thm)],[101])).
% 39.06/39.28 tff(103,axiom,(![V0r_2E0: mono_2Etyop_2Emin_2Ebool, V1q_2E0: mono_2Etyop_2Emin_2Ebool, V2p_2E0: mono_2Etyop_2Emin_2Ebool] : ((p(V2p_2E0) <=> (V1q_2E0 = V0r_2E0)) <=> (((((p(V2p_2E0) | p(V1q_2E0)) | p(V0r_2E0)) & ((p(V2p_2E0) | (~p(V0r_2E0))) | (~p(V1q_2E0)))) & ((p(V1q_2E0) | (~p(V0r_2E0))) | (~p(V2p_2E0)))) & ((p(V0r_2E0) | (~p(V1q_2E0))) | (~p(V2p_2E0)))))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','thm_2Esat_2Edc__eq')).
% 39.06/39.28 tff(104,plain,
% 39.06/39.28 (![V0r_2E0: mono_2Etyop_2Emin_2Ebool, V1q_2E0: mono_2Etyop_2Emin_2Ebool, V2p_2E0: mono_2Etyop_2Emin_2Ebool] : ((p(V2p_2E0) <=> (V1q_2E0 = V0r_2E0)) <=> ((p(V2p_2E0) | p(V1q_2E0) | p(V0r_2E0)) & (p(V2p_2E0) | (~p(V1q_2E0)) | (~p(V0r_2E0))) & ((~p(V2p_2E0)) | p(V1q_2E0) | (~p(V0r_2E0))) & ((~p(V2p_2E0)) | p(V0r_2E0) | (~p(V1q_2E0)))))),
% 39.06/39.28 inference(modus_ponens,[status(thm)],[103, 102])).
% 39.06/39.28 tff(105,plain,
% 39.06/39.28 (![V0r_2E0: mono_2Etyop_2Emin_2Ebool, V1q_2E0: mono_2Etyop_2Emin_2Ebool, V2p_2E0: mono_2Etyop_2Emin_2Ebool] : ((p(V2p_2E0) <=> (V1q_2E0 = V0r_2E0)) <=> ((p(V2p_2E0) | p(V1q_2E0) | p(V0r_2E0)) & (p(V2p_2E0) | (~p(V1q_2E0)) | (~p(V0r_2E0))) & ((~p(V2p_2E0)) | p(V1q_2E0) | (~p(V0r_2E0))) & ((~p(V2p_2E0)) | p(V0r_2E0) | (~p(V1q_2E0)))))),
% 39.06/39.28 inference(modus_ponens,[status(thm)],[104, 100])).
% 39.06/39.28 tff(106,plain,(
% 39.06/39.28 ![V0r_2E0: mono_2Etyop_2Emin_2Ebool, V1q_2E0: mono_2Etyop_2Emin_2Ebool, V2p_2E0: mono_2Etyop_2Emin_2Ebool] : ((p(V2p_2E0) <=> (V1q_2E0 = V0r_2E0)) <=> ((p(V2p_2E0) | p(V1q_2E0) | p(V0r_2E0)) & (p(V2p_2E0) | (~p(V1q_2E0)) | (~p(V0r_2E0))) & ((~p(V2p_2E0)) | p(V1q_2E0) | (~p(V0r_2E0))) & ((~p(V2p_2E0)) | p(V0r_2E0) | (~p(V1q_2E0)))))),
% 39.06/39.28 inference(skolemize,[status(sab)],[105])).
% 39.06/39.28 tff(107,plain,
% 39.06/39.28 (![V0r_2E0: mono_2Etyop_2Emin_2Ebool, V1q_2E0: mono_2Etyop_2Emin_2Ebool, V2p_2E0: mono_2Etyop_2Emin_2Ebool] : (~(((~(p(V2p_2E0) | p(V1q_2E0) | p(V0r_2E0))) | (~(p(V2p_2E0) | (~p(V1q_2E0)) | (~p(V0r_2E0)))) | (~((~p(V2p_2E0)) | p(V1q_2E0) | (~p(V0r_2E0)))) | (~((~p(V2p_2E0)) | p(V0r_2E0) | (~p(V1q_2E0))))) <=> (p(V2p_2E0) <=> (V1q_2E0 = V0r_2E0))))),
% 39.06/39.28 inference(modus_ponens,[status(thm)],[106, 99])).
% 39.06/39.28 tff(108,plain,
% 39.06/39.28 (![V0r_2E0: mono_2Etyop_2Emin_2Ebool, V1q_2E0: mono_2Etyop_2Emin_2Ebool, V2p_2E0: mono_2Etyop_2Emin_2Ebool] : (~(((~(p(V2p_2E0) | p(V1q_2E0) | p(V0r_2E0))) | (~(p(V2p_2E0) | (~p(V1q_2E0)) | (~p(V0r_2E0)))) | (~((~p(V2p_2E0)) | p(V1q_2E0) | (~p(V0r_2E0)))) | (~((~p(V2p_2E0)) | p(V0r_2E0) | (~p(V1q_2E0))))) <=> (p(V2p_2E0) <=> (V1q_2E0 = V0r_2E0))))),
% 39.06/39.29 inference(modus_ponens,[status(thm)],[107, 97])).
% 39.06/39.29 tff(109,plain,
% 39.06/39.29 (((~![V0r_2E0: mono_2Etyop_2Emin_2Ebool, V1q_2E0: mono_2Etyop_2Emin_2Ebool, V2p_2E0: mono_2Etyop_2Emin_2Ebool] : (~(((~(p(V2p_2E0) | p(V1q_2E0) | p(V0r_2E0))) | (~(p(V2p_2E0) | (~p(V1q_2E0)) | (~p(V0r_2E0)))) | (~((~p(V2p_2E0)) | p(V1q_2E0) | (~p(V0r_2E0)))) | (~((~p(V2p_2E0)) | p(V0r_2E0) | (~p(V1q_2E0))))) <=> (p(V2p_2E0) <=> (V1q_2E0 = V0r_2E0))))) | (~(((~(p(mono_2Ec_2Ebool_2EF_2E0) | p(mono_2Ec_2Ebool_2ET_2E0))) | (~(p(mono_2Ec_2Ebool_2EF_2E0) | (~p(mono_2Ec_2Ebool_2ET_2E0))))) <=> (p(mono_2Ec_2Ebool_2ET_2E0) <=> (mono_2Ec_2Ebool_2ET_2E0 = mono_2Ec_2Ebool_2EF_2E0))))) <=> ((~![V0r_2E0: mono_2Etyop_2Emin_2Ebool, V1q_2E0: mono_2Etyop_2Emin_2Ebool, V2p_2E0: mono_2Etyop_2Emin_2Ebool] : (~(((~(p(V2p_2E0) | p(V1q_2E0) | p(V0r_2E0))) | (~(p(V2p_2E0) | (~p(V1q_2E0)) | (~p(V0r_2E0)))) | (~((~p(V2p_2E0)) | p(V1q_2E0) | (~p(V0r_2E0)))) | (~((~p(V2p_2E0)) | p(V0r_2E0) | (~p(V1q_2E0))))) <=> (p(V2p_2E0) <=> (V1q_2E0 = V0r_2E0))))) | (~(((~(p(mono_2Ec_2Ebool_2EF_2E0) | p(mono_2Ec_2Ebool_2ET_2E0))) | (~(p(mono_2Ec_2Ebool_2EF_2E0) | (~p(mono_2Ec_2Ebool_2ET_2E0))))) <=> (p(mono_2Ec_2Ebool_2ET_2E0) <=> (mono_2Ec_2Ebool_2ET_2E0 = mono_2Ec_2Ebool_2EF_2E0)))))),
% 39.06/39.29 inference(rewrite,[status(thm)],[])).
% 39.06/39.29 tff(110,plain,
% 39.06/39.29 ((~(((~(p(mono_2Ec_2Ebool_2EF_2E0) | p(mono_2Ec_2Ebool_2ET_2E0))) | (~(p(mono_2Ec_2Ebool_2EF_2E0) | (~p(mono_2Ec_2Ebool_2ET_2E0))))) <=> (p(mono_2Ec_2Ebool_2ET_2E0) <=> (mono_2Ec_2Ebool_2ET_2E0 = mono_2Ec_2Ebool_2EF_2E0)))) <=> (~(((~(p(mono_2Ec_2Ebool_2EF_2E0) | p(mono_2Ec_2Ebool_2ET_2E0))) | (~(p(mono_2Ec_2Ebool_2EF_2E0) | (~p(mono_2Ec_2Ebool_2ET_2E0))))) <=> (p(mono_2Ec_2Ebool_2ET_2E0) <=> (mono_2Ec_2Ebool_2ET_2E0 = mono_2Ec_2Ebool_2EF_2E0))))),
% 39.06/39.29 inference(rewrite,[status(thm)],[])).
% 39.06/39.29 tff(111,plain,
% 39.06/39.29 ((((~(p(mono_2Ec_2Ebool_2ET_2E0) | p(mono_2Ec_2Ebool_2ET_2E0) | p(mono_2Ec_2Ebool_2EF_2E0))) | (~(p(mono_2Ec_2Ebool_2ET_2E0) | (~p(mono_2Ec_2Ebool_2ET_2E0)) | (~p(mono_2Ec_2Ebool_2EF_2E0)))) | (~((~p(mono_2Ec_2Ebool_2ET_2E0)) | p(mono_2Ec_2Ebool_2ET_2E0) | (~p(mono_2Ec_2Ebool_2EF_2E0)))) | (~((~p(mono_2Ec_2Ebool_2ET_2E0)) | p(mono_2Ec_2Ebool_2EF_2E0) | (~p(mono_2Ec_2Ebool_2ET_2E0))))) <=> (p(mono_2Ec_2Ebool_2ET_2E0) <=> (mono_2Ec_2Ebool_2ET_2E0 = mono_2Ec_2Ebool_2EF_2E0))) <=> (((~(p(mono_2Ec_2Ebool_2EF_2E0) | p(mono_2Ec_2Ebool_2ET_2E0))) | (~(p(mono_2Ec_2Ebool_2EF_2E0) | (~p(mono_2Ec_2Ebool_2ET_2E0))))) <=> (p(mono_2Ec_2Ebool_2ET_2E0) <=> (mono_2Ec_2Ebool_2ET_2E0 = mono_2Ec_2Ebool_2EF_2E0)))),
% 39.06/39.29 inference(rewrite,[status(thm)],[])).
% 39.06/39.29 tff(112,plain,
% 39.06/39.29 ((~(((~(p(mono_2Ec_2Ebool_2ET_2E0) | p(mono_2Ec_2Ebool_2ET_2E0) | p(mono_2Ec_2Ebool_2EF_2E0))) | (~(p(mono_2Ec_2Ebool_2ET_2E0) | (~p(mono_2Ec_2Ebool_2ET_2E0)) | (~p(mono_2Ec_2Ebool_2EF_2E0)))) | (~((~p(mono_2Ec_2Ebool_2ET_2E0)) | p(mono_2Ec_2Ebool_2ET_2E0) | (~p(mono_2Ec_2Ebool_2EF_2E0)))) | (~((~p(mono_2Ec_2Ebool_2ET_2E0)) | p(mono_2Ec_2Ebool_2EF_2E0) | (~p(mono_2Ec_2Ebool_2ET_2E0))))) <=> (p(mono_2Ec_2Ebool_2ET_2E0) <=> (mono_2Ec_2Ebool_2ET_2E0 = mono_2Ec_2Ebool_2EF_2E0)))) <=> (~(((~(p(mono_2Ec_2Ebool_2EF_2E0) | p(mono_2Ec_2Ebool_2ET_2E0))) | (~(p(mono_2Ec_2Ebool_2EF_2E0) | (~p(mono_2Ec_2Ebool_2ET_2E0))))) <=> (p(mono_2Ec_2Ebool_2ET_2E0) <=> (mono_2Ec_2Ebool_2ET_2E0 = mono_2Ec_2Ebool_2EF_2E0))))),
% 39.06/39.29 inference(monotonicity,[status(thm)],[111])).
% 39.06/39.29 tff(113,plain,
% 39.06/39.29 ((~(((~(p(mono_2Ec_2Ebool_2ET_2E0) | p(mono_2Ec_2Ebool_2ET_2E0) | p(mono_2Ec_2Ebool_2EF_2E0))) | (~(p(mono_2Ec_2Ebool_2ET_2E0) | (~p(mono_2Ec_2Ebool_2ET_2E0)) | (~p(mono_2Ec_2Ebool_2EF_2E0)))) | (~((~p(mono_2Ec_2Ebool_2ET_2E0)) | p(mono_2Ec_2Ebool_2ET_2E0) | (~p(mono_2Ec_2Ebool_2EF_2E0)))) | (~((~p(mono_2Ec_2Ebool_2ET_2E0)) | p(mono_2Ec_2Ebool_2EF_2E0) | (~p(mono_2Ec_2Ebool_2ET_2E0))))) <=> (p(mono_2Ec_2Ebool_2ET_2E0) <=> (mono_2Ec_2Ebool_2ET_2E0 = mono_2Ec_2Ebool_2EF_2E0)))) <=> (~(((~(p(mono_2Ec_2Ebool_2EF_2E0) | p(mono_2Ec_2Ebool_2ET_2E0))) | (~(p(mono_2Ec_2Ebool_2EF_2E0) | (~p(mono_2Ec_2Ebool_2ET_2E0))))) <=> (p(mono_2Ec_2Ebool_2ET_2E0) <=> (mono_2Ec_2Ebool_2ET_2E0 = mono_2Ec_2Ebool_2EF_2E0))))),
% 39.06/39.29 inference(transitivity,[status(thm)],[112, 110])).
% 39.06/39.29 tff(114,plain,
% 39.06/39.29 (((~![V0r_2E0: mono_2Etyop_2Emin_2Ebool, V1q_2E0: mono_2Etyop_2Emin_2Ebool, V2p_2E0: mono_2Etyop_2Emin_2Ebool] : (~(((~(p(V2p_2E0) | p(V1q_2E0) | p(V0r_2E0))) | (~(p(V2p_2E0) | (~p(V1q_2E0)) | (~p(V0r_2E0)))) | (~((~p(V2p_2E0)) | p(V1q_2E0) | (~p(V0r_2E0)))) | (~((~p(V2p_2E0)) | p(V0r_2E0) | (~p(V1q_2E0))))) <=> (p(V2p_2E0) <=> (V1q_2E0 = V0r_2E0))))) | (~(((~(p(mono_2Ec_2Ebool_2ET_2E0) | p(mono_2Ec_2Ebool_2ET_2E0) | p(mono_2Ec_2Ebool_2EF_2E0))) | (~(p(mono_2Ec_2Ebool_2ET_2E0) | (~p(mono_2Ec_2Ebool_2ET_2E0)) | (~p(mono_2Ec_2Ebool_2EF_2E0)))) | (~((~p(mono_2Ec_2Ebool_2ET_2E0)) | p(mono_2Ec_2Ebool_2ET_2E0) | (~p(mono_2Ec_2Ebool_2EF_2E0)))) | (~((~p(mono_2Ec_2Ebool_2ET_2E0)) | p(mono_2Ec_2Ebool_2EF_2E0) | (~p(mono_2Ec_2Ebool_2ET_2E0))))) <=> (p(mono_2Ec_2Ebool_2ET_2E0) <=> (mono_2Ec_2Ebool_2ET_2E0 = mono_2Ec_2Ebool_2EF_2E0))))) <=> ((~![V0r_2E0: mono_2Etyop_2Emin_2Ebool, V1q_2E0: mono_2Etyop_2Emin_2Ebool, V2p_2E0: mono_2Etyop_2Emin_2Ebool] : (~(((~(p(V2p_2E0) | p(V1q_2E0) | p(V0r_2E0))) | (~(p(V2p_2E0) | (~p(V1q_2E0)) | (~p(V0r_2E0)))) | (~((~p(V2p_2E0)) | p(V1q_2E0) | (~p(V0r_2E0)))) | (~((~p(V2p_2E0)) | p(V0r_2E0) | (~p(V1q_2E0))))) <=> (p(V2p_2E0) <=> (V1q_2E0 = V0r_2E0))))) | (~(((~(p(mono_2Ec_2Ebool_2EF_2E0) | p(mono_2Ec_2Ebool_2ET_2E0))) | (~(p(mono_2Ec_2Ebool_2EF_2E0) | (~p(mono_2Ec_2Ebool_2ET_2E0))))) <=> (p(mono_2Ec_2Ebool_2ET_2E0) <=> (mono_2Ec_2Ebool_2ET_2E0 = mono_2Ec_2Ebool_2EF_2E0)))))),
% 39.06/39.29 inference(monotonicity,[status(thm)],[113])).
% 39.06/39.29 tff(115,plain,
% 39.06/39.29 (((~![V0r_2E0: mono_2Etyop_2Emin_2Ebool, V1q_2E0: mono_2Etyop_2Emin_2Ebool, V2p_2E0: mono_2Etyop_2Emin_2Ebool] : (~(((~(p(V2p_2E0) | p(V1q_2E0) | p(V0r_2E0))) | (~(p(V2p_2E0) | (~p(V1q_2E0)) | (~p(V0r_2E0)))) | (~((~p(V2p_2E0)) | p(V1q_2E0) | (~p(V0r_2E0)))) | (~((~p(V2p_2E0)) | p(V0r_2E0) | (~p(V1q_2E0))))) <=> (p(V2p_2E0) <=> (V1q_2E0 = V0r_2E0))))) | (~(((~(p(mono_2Ec_2Ebool_2ET_2E0) | p(mono_2Ec_2Ebool_2ET_2E0) | p(mono_2Ec_2Ebool_2EF_2E0))) | (~(p(mono_2Ec_2Ebool_2ET_2E0) | (~p(mono_2Ec_2Ebool_2ET_2E0)) | (~p(mono_2Ec_2Ebool_2EF_2E0)))) | (~((~p(mono_2Ec_2Ebool_2ET_2E0)) | p(mono_2Ec_2Ebool_2ET_2E0) | (~p(mono_2Ec_2Ebool_2EF_2E0)))) | (~((~p(mono_2Ec_2Ebool_2ET_2E0)) | p(mono_2Ec_2Ebool_2EF_2E0) | (~p(mono_2Ec_2Ebool_2ET_2E0))))) <=> (p(mono_2Ec_2Ebool_2ET_2E0) <=> (mono_2Ec_2Ebool_2ET_2E0 = mono_2Ec_2Ebool_2EF_2E0))))) <=> ((~![V0r_2E0: mono_2Etyop_2Emin_2Ebool, V1q_2E0: mono_2Etyop_2Emin_2Ebool, V2p_2E0: mono_2Etyop_2Emin_2Ebool] : (~(((~(p(V2p_2E0) | p(V1q_2E0) | p(V0r_2E0))) | (~(p(V2p_2E0) | (~p(V1q_2E0)) | (~p(V0r_2E0)))) | (~((~p(V2p_2E0)) | p(V1q_2E0) | (~p(V0r_2E0)))) | (~((~p(V2p_2E0)) | p(V0r_2E0) | (~p(V1q_2E0))))) <=> (p(V2p_2E0) <=> (V1q_2E0 = V0r_2E0))))) | (~(((~(p(mono_2Ec_2Ebool_2EF_2E0) | p(mono_2Ec_2Ebool_2ET_2E0))) | (~(p(mono_2Ec_2Ebool_2EF_2E0) | (~p(mono_2Ec_2Ebool_2ET_2E0))))) <=> (p(mono_2Ec_2Ebool_2ET_2E0) <=> (mono_2Ec_2Ebool_2ET_2E0 = mono_2Ec_2Ebool_2EF_2E0)))))),
% 39.06/39.29 inference(transitivity,[status(thm)],[114, 109])).
% 39.06/39.29 tff(116,plain,
% 39.06/39.29 ((~![V0r_2E0: mono_2Etyop_2Emin_2Ebool, V1q_2E0: mono_2Etyop_2Emin_2Ebool, V2p_2E0: mono_2Etyop_2Emin_2Ebool] : (~(((~(p(V2p_2E0) | p(V1q_2E0) | p(V0r_2E0))) | (~(p(V2p_2E0) | (~p(V1q_2E0)) | (~p(V0r_2E0)))) | (~((~p(V2p_2E0)) | p(V1q_2E0) | (~p(V0r_2E0)))) | (~((~p(V2p_2E0)) | p(V0r_2E0) | (~p(V1q_2E0))))) <=> (p(V2p_2E0) <=> (V1q_2E0 = V0r_2E0))))) | (~(((~(p(mono_2Ec_2Ebool_2ET_2E0) | p(mono_2Ec_2Ebool_2ET_2E0) | p(mono_2Ec_2Ebool_2EF_2E0))) | (~(p(mono_2Ec_2Ebool_2ET_2E0) | (~p(mono_2Ec_2Ebool_2ET_2E0)) | (~p(mono_2Ec_2Ebool_2EF_2E0)))) | (~((~p(mono_2Ec_2Ebool_2ET_2E0)) | p(mono_2Ec_2Ebool_2ET_2E0) | (~p(mono_2Ec_2Ebool_2EF_2E0)))) | (~((~p(mono_2Ec_2Ebool_2ET_2E0)) | p(mono_2Ec_2Ebool_2EF_2E0) | (~p(mono_2Ec_2Ebool_2ET_2E0))))) <=> (p(mono_2Ec_2Ebool_2ET_2E0) <=> (mono_2Ec_2Ebool_2ET_2E0 = mono_2Ec_2Ebool_2EF_2E0))))),
% 39.06/39.29 inference(quant_inst,[status(thm)],[])).
% 39.06/39.29 tff(117,plain,
% 39.06/39.29 ((~![V0r_2E0: mono_2Etyop_2Emin_2Ebool, V1q_2E0: mono_2Etyop_2Emin_2Ebool, V2p_2E0: mono_2Etyop_2Emin_2Ebool] : (~(((~(p(V2p_2E0) | p(V1q_2E0) | p(V0r_2E0))) | (~(p(V2p_2E0) | (~p(V1q_2E0)) | (~p(V0r_2E0)))) | (~((~p(V2p_2E0)) | p(V1q_2E0) | (~p(V0r_2E0)))) | (~((~p(V2p_2E0)) | p(V0r_2E0) | (~p(V1q_2E0))))) <=> (p(V2p_2E0) <=> (V1q_2E0 = V0r_2E0))))) | (~(((~(p(mono_2Ec_2Ebool_2EF_2E0) | p(mono_2Ec_2Ebool_2ET_2E0))) | (~(p(mono_2Ec_2Ebool_2EF_2E0) | (~p(mono_2Ec_2Ebool_2ET_2E0))))) <=> (p(mono_2Ec_2Ebool_2ET_2E0) <=> (mono_2Ec_2Ebool_2ET_2E0 = mono_2Ec_2Ebool_2EF_2E0))))),
% 39.21/39.45 inference(modus_ponens,[status(thm)],[116, 115])).
% 39.21/39.45 tff(118,plain,
% 39.21/39.45 (~(((~(p(mono_2Ec_2Ebool_2EF_2E0) | p(mono_2Ec_2Ebool_2ET_2E0))) | (~(p(mono_2Ec_2Ebool_2EF_2E0) | (~p(mono_2Ec_2Ebool_2ET_2E0))))) <=> (p(mono_2Ec_2Ebool_2ET_2E0) <=> (mono_2Ec_2Ebool_2ET_2E0 = mono_2Ec_2Ebool_2EF_2E0)))),
% 39.21/39.45 inference(unit_resolution,[status(thm)],[117, 108])).
% 39.21/39.45 tff(119,plain,
% 39.21/39.45 ((~(p(mono_2Ec_2Ebool_2EF_2E0) | (~p(mono_2Ec_2Ebool_2ET_2E0)))) | p(mono_2Ec_2Ebool_2EF_2E0) | (~p(mono_2Ec_2Ebool_2ET_2E0))),
% 39.21/39.45 inference(tautology,[status(thm)],[])).
% 39.21/39.45 tff(120,plain,
% 39.21/39.45 (~(p(mono_2Ec_2Ebool_2EF_2E0) | (~p(mono_2Ec_2Ebool_2ET_2E0)))),
% 39.21/39.45 inference(unit_resolution,[status(thm)],[119, 81, 3])).
% 39.21/39.45 tff(121,plain,
% 39.21/39.45 (((~(p(mono_2Ec_2Ebool_2EF_2E0) | p(mono_2Ec_2Ebool_2ET_2E0))) | (~(p(mono_2Ec_2Ebool_2EF_2E0) | (~p(mono_2Ec_2Ebool_2ET_2E0))))) | (p(mono_2Ec_2Ebool_2EF_2E0) | (~p(mono_2Ec_2Ebool_2ET_2E0)))),
% 39.21/39.45 inference(tautology,[status(thm)],[])).
% 39.21/39.45 tff(122,plain,
% 39.21/39.45 ((~(p(mono_2Ec_2Ebool_2EF_2E0) | p(mono_2Ec_2Ebool_2ET_2E0))) | (~(p(mono_2Ec_2Ebool_2EF_2E0) | (~p(mono_2Ec_2Ebool_2ET_2E0))))),
% 39.21/39.45 inference(unit_resolution,[status(thm)],[121, 120])).
% 39.21/39.45 tff(123,plain,
% 39.21/39.45 ((((~(p(mono_2Ec_2Ebool_2EF_2E0) | p(mono_2Ec_2Ebool_2ET_2E0))) | (~(p(mono_2Ec_2Ebool_2EF_2E0) | (~p(mono_2Ec_2Ebool_2ET_2E0))))) <=> (p(mono_2Ec_2Ebool_2ET_2E0) <=> (mono_2Ec_2Ebool_2ET_2E0 = mono_2Ec_2Ebool_2EF_2E0))) | (~((~(p(mono_2Ec_2Ebool_2EF_2E0) | p(mono_2Ec_2Ebool_2ET_2E0))) | (~(p(mono_2Ec_2Ebool_2EF_2E0) | (~p(mono_2Ec_2Ebool_2ET_2E0)))))) | (~(p(mono_2Ec_2Ebool_2ET_2E0) <=> (mono_2Ec_2Ebool_2ET_2E0 = mono_2Ec_2Ebool_2EF_2E0)))),
% 39.21/39.45 inference(tautology,[status(thm)],[])).
% 39.21/39.45 tff(124,plain,
% 39.21/39.45 ((((~(p(mono_2Ec_2Ebool_2EF_2E0) | p(mono_2Ec_2Ebool_2ET_2E0))) | (~(p(mono_2Ec_2Ebool_2EF_2E0) | (~p(mono_2Ec_2Ebool_2ET_2E0))))) <=> (p(mono_2Ec_2Ebool_2ET_2E0) <=> (mono_2Ec_2Ebool_2ET_2E0 = mono_2Ec_2Ebool_2EF_2E0))) | (~(p(mono_2Ec_2Ebool_2ET_2E0) <=> (mono_2Ec_2Ebool_2ET_2E0 = mono_2Ec_2Ebool_2EF_2E0)))),
% 39.21/39.45 inference(unit_resolution,[status(thm)],[123, 122])).
% 39.21/39.45 tff(125,plain,
% 39.21/39.45 (~(p(mono_2Ec_2Ebool_2ET_2E0) <=> (mono_2Ec_2Ebool_2ET_2E0 = mono_2Ec_2Ebool_2EF_2E0))),
% 39.21/39.45 inference(unit_resolution,[status(thm)],[124, 118])).
% 39.21/39.45 tff(126,plain,
% 39.21/39.45 ((p(mono_2Ec_2Ebool_2ET_2E0) <=> (mono_2Ec_2Ebool_2ET_2E0 = mono_2Ec_2Ebool_2EF_2E0)) | (~p(mono_2Ec_2Ebool_2ET_2E0)) | (~(mono_2Ec_2Ebool_2ET_2E0 = mono_2Ec_2Ebool_2EF_2E0))),
% 39.21/39.45 inference(tautology,[status(thm)],[])).
% 39.21/39.45 tff(127,plain,
% 39.21/39.45 ((p(mono_2Ec_2Ebool_2ET_2E0) <=> (mono_2Ec_2Ebool_2ET_2E0 = mono_2Ec_2Ebool_2EF_2E0)) | (~(mono_2Ec_2Ebool_2ET_2E0 = mono_2Ec_2Ebool_2EF_2E0))),
% 39.21/39.45 inference(unit_resolution,[status(thm)],[126, 81])).
% 39.21/39.45 tff(128,plain,
% 39.21/39.45 (~(mono_2Ec_2Ebool_2ET_2E0 = mono_2Ec_2Ebool_2EF_2E0)),
% 39.21/39.45 inference(unit_resolution,[status(thm)],[127, 125])).
% 39.21/39.45 tff(129,plain,
% 39.21/39.45 ($false),
% 39.21/39.45 inference(unit_resolution,[status(thm)],[128, 95])).
% 39.21/39.45 % SZS output end Proof
% 39.21/39.45 % E exiting
%------------------------------------------------------------------------------