%------------------------------------------------------------------------------
% File : Z3---4.15.1
% Problem : NUM836+2 : TPTP v9.0.0. Released v4.1.0.
% Transfm : none
% Format : tptp
% Command : run_E %s %d THM
% Computer : n006.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:22:10 AM UTC 2025
% Result : Theorem 0.17s 0.36s
% Output : Proof 0.17s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.11/0.11 % Problem : NUM836+2 : TPTP v9.0.0. Released v4.1.0.
% 0.11/0.11 % Command : run_E %s %d THM
% 0.11/0.32 % Computer : n006.cluster.edu
% 0.11/0.32 % Model : x86_64 x86_64
% 0.11/0.32 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.32 % Memory : 8042.1875MB
% 0.11/0.32 % OS : Linux 3.10.0-693.el7.x86_64
% 0.11/0.32 % CPULimit : 300
% 0.11/0.32 % WCLimit : 300
% 0.11/0.32 % DateTime : Fri Jun 20 02:01:05 EDT 2025
% 0.11/0.32 % CPUTime :
% 0.17/0.36 % SZS status Theorem
% 0.17/0.36 % SZS output start Proof
% 0.17/0.36 tff(vplus_type, type, (
% 0.17/0.36 vplus: ( $i * $i ) > $i)).
% 0.17/0.36 tff(tptp_fun_Vd201_0_type, type, (
% 0.17/0.36 tptp_fun_Vd201_0: ( $i * $i ) > $i)).
% 0.17/0.36 tff(vd204_type, type, (
% 0.17/0.36 vd204: $i)).
% 0.17/0.36 tff(vd203_type, type, (
% 0.17/0.36 vd203: $i)).
% 0.17/0.36 tff(tptp_fun_Vd196_1_type, type, (
% 0.17/0.36 tptp_fun_Vd196_1: ( $i * $i ) > $i)).
% 0.17/0.36 tff(greater_type, type, (
% 0.17/0.36 greater: ( $i * $i ) > $o)).
% 0.17/0.36 tff(less_type, type, (
% 0.17/0.36 less: ( $i * $i ) > $o)).
% 0.17/0.36 tff(1,plain,
% 0.17/0.36 (^[Vd46: $i, Vd47: $i, Vd48: $i] : refl((vplus(vplus(Vd46, Vd47), Vd48) = vplus(Vd46, vplus(Vd47, Vd48))) <=> (vplus(vplus(Vd46, Vd47), Vd48) = vplus(Vd46, vplus(Vd47, Vd48))))),
% 0.17/0.36 inference(bind,[status(th)],[])).
% 0.17/0.36 tff(2,plain,
% 0.17/0.36 (![Vd46: $i, Vd47: $i, Vd48: $i] : (vplus(vplus(Vd46, Vd47), Vd48) = vplus(Vd46, vplus(Vd47, Vd48))) <=> ![Vd46: $i, Vd47: $i, Vd48: $i] : (vplus(vplus(Vd46, Vd47), Vd48) = vplus(Vd46, vplus(Vd47, Vd48)))),
% 0.17/0.36 inference(quant_intro,[status(thm)],[1])).
% 0.17/0.36 tff(3,plain,
% 0.17/0.36 (![Vd46: $i, Vd47: $i, Vd48: $i] : (vplus(vplus(Vd46, Vd47), Vd48) = vplus(Vd46, vplus(Vd47, Vd48))) <=> ![Vd46: $i, Vd47: $i, Vd48: $i] : (vplus(vplus(Vd46, Vd47), Vd48) = vplus(Vd46, vplus(Vd47, Vd48)))),
% 0.17/0.36 inference(rewrite,[status(thm)],[])).
% 0.17/0.36 tff(4,axiom,(![Vd46: $i, Vd47: $i, Vd48: $i] : (vplus(vplus(Vd46, Vd47), Vd48) = vplus(Vd46, vplus(Vd47, Vd48)))), file('/export/starexec/sandbox/benchmark/theBenchmark.p',''ass(cond(33, 0), 0)'')).
% 0.17/0.36 tff(5,plain,
% 0.17/0.36 (![Vd46: $i, Vd47: $i, Vd48: $i] : (vplus(vplus(Vd46, Vd47), Vd48) = vplus(Vd46, vplus(Vd47, Vd48)))),
% 0.17/0.36 inference(modus_ponens,[status(thm)],[4, 3])).
% 0.17/0.36 tff(6,plain,(
% 0.17/0.36 ![Vd46: $i, Vd47: $i, Vd48: $i] : (vplus(vplus(Vd46, Vd47), Vd48) = vplus(Vd46, vplus(Vd47, Vd48)))),
% 0.17/0.36 inference(skolemize,[status(sab)],[5])).
% 0.17/0.36 tff(7,plain,
% 0.17/0.36 (![Vd46: $i, Vd47: $i, Vd48: $i] : (vplus(vplus(Vd46, Vd47), Vd48) = vplus(Vd46, vplus(Vd47, Vd48)))),
% 0.17/0.36 inference(modus_ponens,[status(thm)],[6, 2])).
% 0.17/0.36 tff(8,plain,
% 0.17/0.36 ((~![Vd46: $i, Vd47: $i, Vd48: $i] : (vplus(vplus(Vd46, Vd47), Vd48) = vplus(Vd46, vplus(Vd47, Vd48)))) | (vplus(vplus(vplus(vd203, tptp_fun_Vd201_0(vd203, vd204)), tptp_fun_Vd196_1(vd203, vd204)), tptp_fun_Vd201_0(vd203, vd204)) = vplus(vplus(vd203, tptp_fun_Vd201_0(vd203, vd204)), vplus(tptp_fun_Vd196_1(vd203, vd204), tptp_fun_Vd201_0(vd203, vd204))))),
% 0.17/0.36 inference(quant_inst,[status(thm)],[])).
% 0.17/0.36 tff(9,plain,
% 0.17/0.36 (vplus(vplus(vplus(vd203, tptp_fun_Vd201_0(vd203, vd204)), tptp_fun_Vd196_1(vd203, vd204)), tptp_fun_Vd201_0(vd203, vd204)) = vplus(vplus(vd203, tptp_fun_Vd201_0(vd203, vd204)), vplus(tptp_fun_Vd196_1(vd203, vd204), tptp_fun_Vd201_0(vd203, vd204)))),
% 0.17/0.36 inference(unit_resolution,[status(thm)],[8, 7])).
% 0.17/0.36 tff(10,plain,
% 0.17/0.36 (^[Vd193: $i, Vd194: $i] : refl((~((~((~greater(Vd194, Vd193)) | (Vd194 = vplus(Vd193, tptp_fun_Vd196_1(Vd194, Vd193))))) | (~(greater(Vd194, Vd193) | ![Vd196: $i] : (~(Vd194 = vplus(Vd193, Vd196))))))) <=> (~((~((~greater(Vd194, Vd193)) | (Vd194 = vplus(Vd193, tptp_fun_Vd196_1(Vd194, Vd193))))) | (~(greater(Vd194, Vd193) | ![Vd196: $i] : (~(Vd194 = vplus(Vd193, Vd196))))))))),
% 0.17/0.36 inference(bind,[status(th)],[])).
% 0.17/0.36 tff(11,plain,
% 0.17/0.36 (![Vd193: $i, Vd194: $i] : (~((~((~greater(Vd194, Vd193)) | (Vd194 = vplus(Vd193, tptp_fun_Vd196_1(Vd194, Vd193))))) | (~(greater(Vd194, Vd193) | ![Vd196: $i] : (~(Vd194 = vplus(Vd193, Vd196))))))) <=> ![Vd193: $i, Vd194: $i] : (~((~((~greater(Vd194, Vd193)) | (Vd194 = vplus(Vd193, tptp_fun_Vd196_1(Vd194, Vd193))))) | (~(greater(Vd194, Vd193) | ![Vd196: $i] : (~(Vd194 = vplus(Vd193, Vd196)))))))),
% 0.17/0.36 inference(quant_intro,[status(thm)],[10])).
% 0.17/0.36 tff(12,plain,
% 0.17/0.36 (^[Vd193: $i, Vd194: $i] : rewrite((~((~((~greater(Vd194, Vd193)) | (Vd194 = vplus(Vd193, tptp_fun_Vd196_1(Vd194, Vd193))))) | (~(greater(Vd194, Vd193) | ![Vd196: $i] : (~(Vd194 = vplus(Vd193, Vd196))))))) <=> (~((~((~greater(Vd194, Vd193)) | (Vd194 = vplus(Vd193, tptp_fun_Vd196_1(Vd194, Vd193))))) | (~(greater(Vd194, Vd193) | ![Vd196: $i] : (~(Vd194 = vplus(Vd193, Vd196))))))))),
% 0.17/0.36 inference(bind,[status(th)],[])).
% 0.17/0.36 tff(13,plain,
% 0.17/0.36 (![Vd193: $i, Vd194: $i] : (~((~((~greater(Vd194, Vd193)) | (Vd194 = vplus(Vd193, tptp_fun_Vd196_1(Vd194, Vd193))))) | (~(greater(Vd194, Vd193) | ![Vd196: $i] : (~(Vd194 = vplus(Vd193, Vd196))))))) <=> ![Vd193: $i, Vd194: $i] : (~((~((~greater(Vd194, Vd193)) | (Vd194 = vplus(Vd193, tptp_fun_Vd196_1(Vd194, Vd193))))) | (~(greater(Vd194, Vd193) | ![Vd196: $i] : (~(Vd194 = vplus(Vd193, Vd196)))))))),
% 0.17/0.36 inference(quant_intro,[status(thm)],[12])).
% 0.17/0.36 tff(14,plain,
% 0.17/0.36 (![Vd193: $i, Vd194: $i] : (~((~((~greater(Vd194, Vd193)) | (Vd194 = vplus(Vd193, tptp_fun_Vd196_1(Vd194, Vd193))))) | (~(greater(Vd194, Vd193) | ![Vd196: $i] : (~(Vd194 = vplus(Vd193, Vd196))))))) <=> ![Vd193: $i, Vd194: $i] : (~((~((~greater(Vd194, Vd193)) | (Vd194 = vplus(Vd193, tptp_fun_Vd196_1(Vd194, Vd193))))) | (~(greater(Vd194, Vd193) | ![Vd196: $i] : (~(Vd194 = vplus(Vd193, Vd196)))))))),
% 0.17/0.36 inference(transitivity,[status(thm)],[13, 11])).
% 0.17/0.36 tff(15,plain,
% 0.17/0.36 (^[Vd193: $i, Vd194: $i] : trans(monotonicity(rewrite((greater(Vd194, Vd193) | ![Vd196: $i] : (~(Vd194 = vplus(Vd193, Vd196)))) <=> (greater(Vd194, Vd193) | ![Vd196: $i] : (~(Vd194 = vplus(Vd193, Vd196))))), ((((~greater(Vd194, Vd193)) | (Vd194 = vplus(Vd193, tptp_fun_Vd196_1(Vd194, Vd193)))) & (greater(Vd194, Vd193) | ![Vd196: $i] : (~(Vd194 = vplus(Vd193, Vd196))))) <=> (((~greater(Vd194, Vd193)) | (Vd194 = vplus(Vd193, tptp_fun_Vd196_1(Vd194, Vd193)))) & (greater(Vd194, Vd193) | ![Vd196: $i] : (~(Vd194 = vplus(Vd193, Vd196))))))), rewrite((((~greater(Vd194, Vd193)) | (Vd194 = vplus(Vd193, tptp_fun_Vd196_1(Vd194, Vd193)))) & (greater(Vd194, Vd193) | ![Vd196: $i] : (~(Vd194 = vplus(Vd193, Vd196))))) <=> (~((~((~greater(Vd194, Vd193)) | (Vd194 = vplus(Vd193, tptp_fun_Vd196_1(Vd194, Vd193))))) | (~(greater(Vd194, Vd193) | ![Vd196: $i] : (~(Vd194 = vplus(Vd193, Vd196)))))))), ((((~greater(Vd194, Vd193)) | (Vd194 = vplus(Vd193, tptp_fun_Vd196_1(Vd194, Vd193)))) & (greater(Vd194, Vd193) | ![Vd196: $i] : (~(Vd194 = vplus(Vd193, Vd196))))) <=> (~((~((~greater(Vd194, Vd193)) | (Vd194 = vplus(Vd193, tptp_fun_Vd196_1(Vd194, Vd193))))) | (~(greater(Vd194, Vd193) | ![Vd196: $i] : (~(Vd194 = vplus(Vd193, Vd196)))))))))),
% 0.17/0.36 inference(bind,[status(th)],[])).
% 0.17/0.36 tff(16,plain,
% 0.17/0.36 (![Vd193: $i, Vd194: $i] : (((~greater(Vd194, Vd193)) | (Vd194 = vplus(Vd193, tptp_fun_Vd196_1(Vd194, Vd193)))) & (greater(Vd194, Vd193) | ![Vd196: $i] : (~(Vd194 = vplus(Vd193, Vd196))))) <=> ![Vd193: $i, Vd194: $i] : (~((~((~greater(Vd194, Vd193)) | (Vd194 = vplus(Vd193, tptp_fun_Vd196_1(Vd194, Vd193))))) | (~(greater(Vd194, Vd193) | ![Vd196: $i] : (~(Vd194 = vplus(Vd193, Vd196)))))))),
% 0.17/0.36 inference(quant_intro,[status(thm)],[15])).
% 0.17/0.36 tff(17,plain,
% 0.17/0.36 (![Vd193: $i, Vd194: $i] : (greater(Vd194, Vd193) <=> ?[Vd196: $i] : (Vd194 = vplus(Vd193, Vd196))) <=> ![Vd193: $i, Vd194: $i] : (greater(Vd194, Vd193) <=> ?[Vd196: $i] : (Vd194 = vplus(Vd193, Vd196)))),
% 0.17/0.36 inference(rewrite,[status(thm)],[])).
% 0.17/0.36 tff(18,axiom,(![Vd193: $i, Vd194: $i] : (greater(Vd194, Vd193) <=> ?[Vd196: $i] : (Vd194 = vplus(Vd193, Vd196)))), file('/export/starexec/sandbox/benchmark/theBenchmark.p',''def(cond(conseq(axiom(3)), 11), 1)'')).
% 0.17/0.36 tff(19,plain,
% 0.17/0.36 (![Vd193: $i, Vd194: $i] : (greater(Vd194, Vd193) <=> ?[Vd196: $i] : (Vd194 = vplus(Vd193, Vd196)))),
% 0.17/0.36 inference(modus_ponens,[status(thm)],[18, 17])).
% 0.17/0.36 tff(20,plain,(
% 0.17/0.36 ![Vd193: $i, Vd194: $i] : (((~greater(Vd194, Vd193)) | (Vd194 = vplus(Vd193, tptp_fun_Vd196_1(Vd194, Vd193)))) & (greater(Vd194, Vd193) | ![Vd196: $i] : (~(Vd194 = vplus(Vd193, Vd196)))))),
% 0.17/0.36 inference(skolemize,[status(sab)],[19])).
% 0.17/0.36 tff(21,plain,
% 0.17/0.36 (![Vd193: $i, Vd194: $i] : (~((~((~greater(Vd194, Vd193)) | (Vd194 = vplus(Vd193, tptp_fun_Vd196_1(Vd194, Vd193))))) | (~(greater(Vd194, Vd193) | ![Vd196: $i] : (~(Vd194 = vplus(Vd193, Vd196)))))))),
% 0.17/0.36 inference(modus_ponens,[status(thm)],[20, 16])).
% 0.17/0.36 tff(22,plain,
% 0.17/0.36 (![Vd193: $i, Vd194: $i] : (~((~((~greater(Vd194, Vd193)) | (Vd194 = vplus(Vd193, tptp_fun_Vd196_1(Vd194, Vd193))))) | (~(greater(Vd194, Vd193) | ![Vd196: $i] : (~(Vd194 = vplus(Vd193, Vd196)))))))),
% 0.17/0.36 inference(modus_ponens,[status(thm)],[21, 14])).
% 0.17/0.36 tff(23,plain,
% 0.17/0.36 ((~![Vd193: $i, Vd194: $i] : (~((~((~greater(Vd194, Vd193)) | (Vd194 = vplus(Vd193, tptp_fun_Vd196_1(Vd194, Vd193))))) | (~(greater(Vd194, Vd193) | ![Vd196: $i] : (~(Vd194 = vplus(Vd193, Vd196)))))))) | (~((~((~greater(vd203, vd204)) | (vd203 = vplus(vd204, tptp_fun_Vd196_1(vd203, vd204))))) | (~(greater(vd203, vd204) | ![Vd196: $i] : (~(vd203 = vplus(vd204, Vd196)))))))),
% 0.17/0.36 inference(quant_inst,[status(thm)],[])).
% 0.17/0.36 tff(24,plain,
% 0.17/0.36 (~((~((~greater(vd203, vd204)) | (vd203 = vplus(vd204, tptp_fun_Vd196_1(vd203, vd204))))) | (~(greater(vd203, vd204) | ![Vd196: $i] : (~(vd203 = vplus(vd204, Vd196))))))),
% 0.17/0.36 inference(unit_resolution,[status(thm)],[23, 22])).
% 0.17/0.36 tff(25,plain,
% 0.17/0.36 (((~((~greater(vd203, vd204)) | (vd203 = vplus(vd204, tptp_fun_Vd196_1(vd203, vd204))))) | (~(greater(vd203, vd204) | ![Vd196: $i] : (~(vd203 = vplus(vd204, Vd196)))))) | ((~greater(vd203, vd204)) | (vd203 = vplus(vd204, tptp_fun_Vd196_1(vd203, vd204))))),
% 0.17/0.36 inference(tautology,[status(thm)],[])).
% 0.17/0.36 tff(26,plain,
% 0.17/0.36 ((~greater(vd203, vd204)) | (vd203 = vplus(vd204, tptp_fun_Vd196_1(vd203, vd204)))),
% 0.17/0.36 inference(unit_resolution,[status(thm)],[25, 24])).
% 0.17/0.36 tff(27,plain,
% 0.17/0.36 (greater(vd203, vd204) <=> greater(vd203, vd204)),
% 0.17/0.36 inference(rewrite,[status(thm)],[])).
% 0.17/0.36 tff(28,axiom,(~((~greater(vd203, vd204)) | (~less(vd203, vd204)))), file('/export/starexec/sandbox/benchmark/theBenchmark.p',''dis(ex(cond(conseq(131), 0), 1))'')).
% 0.17/0.36 tff(29,plain,
% 0.17/0.36 (greater(vd203, vd204)),
% 0.17/0.36 inference(or_elim,[status(thm)],[28])).
% 0.17/0.36 tff(30,plain,
% 0.17/0.36 (greater(vd203, vd204)),
% 0.17/0.36 inference(modus_ponens,[status(thm)],[29, 27])).
% 0.17/0.36 tff(31,plain,
% 0.17/0.36 ((~((~greater(vd203, vd204)) | (vd203 = vplus(vd204, tptp_fun_Vd196_1(vd203, vd204))))) | (~greater(vd203, vd204)) | (vd203 = vplus(vd204, tptp_fun_Vd196_1(vd203, vd204)))),
% 0.17/0.36 inference(tautology,[status(thm)],[])).
% 0.17/0.36 tff(32,plain,
% 0.17/0.36 ((~((~greater(vd203, vd204)) | (vd203 = vplus(vd204, tptp_fun_Vd196_1(vd203, vd204))))) | (vd203 = vplus(vd204, tptp_fun_Vd196_1(vd203, vd204)))),
% 0.17/0.36 inference(unit_resolution,[status(thm)],[31, 30])).
% 0.17/0.36 tff(33,plain,
% 0.17/0.36 (vd203 = vplus(vd204, tptp_fun_Vd196_1(vd203, vd204))),
% 0.17/0.36 inference(unit_resolution,[status(thm)],[32, 26])).
% 0.17/0.36 tff(34,plain,
% 0.17/0.36 (vplus(vd204, tptp_fun_Vd196_1(vd203, vd204)) = vd203),
% 0.17/0.36 inference(symmetry,[status(thm)],[33])).
% 0.17/0.36 tff(35,plain,
% 0.17/0.36 (^[Vd198: $i, Vd199: $i] : refl((~((~((~less(Vd199, Vd198)) | (Vd198 = vplus(Vd199, tptp_fun_Vd201_0(Vd199, Vd198))))) | (~(less(Vd199, Vd198) | ![Vd201: $i] : (~(Vd198 = vplus(Vd199, Vd201))))))) <=> (~((~((~less(Vd199, Vd198)) | (Vd198 = vplus(Vd199, tptp_fun_Vd201_0(Vd199, Vd198))))) | (~(less(Vd199, Vd198) | ![Vd201: $i] : (~(Vd198 = vplus(Vd199, Vd201))))))))),
% 0.17/0.36 inference(bind,[status(th)],[])).
% 0.17/0.36 tff(36,plain,
% 0.17/0.36 (![Vd198: $i, Vd199: $i] : (~((~((~less(Vd199, Vd198)) | (Vd198 = vplus(Vd199, tptp_fun_Vd201_0(Vd199, Vd198))))) | (~(less(Vd199, Vd198) | ![Vd201: $i] : (~(Vd198 = vplus(Vd199, Vd201))))))) <=> ![Vd198: $i, Vd199: $i] : (~((~((~less(Vd199, Vd198)) | (Vd198 = vplus(Vd199, tptp_fun_Vd201_0(Vd199, Vd198))))) | (~(less(Vd199, Vd198) | ![Vd201: $i] : (~(Vd198 = vplus(Vd199, Vd201)))))))),
% 0.17/0.37 inference(quant_intro,[status(thm)],[35])).
% 0.17/0.37 tff(37,plain,
% 0.17/0.37 (^[Vd198: $i, Vd199: $i] : rewrite((~((~((~less(Vd199, Vd198)) | (Vd198 = vplus(Vd199, tptp_fun_Vd201_0(Vd199, Vd198))))) | (~(less(Vd199, Vd198) | ![Vd201: $i] : (~(Vd198 = vplus(Vd199, Vd201))))))) <=> (~((~((~less(Vd199, Vd198)) | (Vd198 = vplus(Vd199, tptp_fun_Vd201_0(Vd199, Vd198))))) | (~(less(Vd199, Vd198) | ![Vd201: $i] : (~(Vd198 = vplus(Vd199, Vd201))))))))),
% 0.17/0.37 inference(bind,[status(th)],[])).
% 0.17/0.37 tff(38,plain,
% 0.17/0.37 (![Vd198: $i, Vd199: $i] : (~((~((~less(Vd199, Vd198)) | (Vd198 = vplus(Vd199, tptp_fun_Vd201_0(Vd199, Vd198))))) | (~(less(Vd199, Vd198) | ![Vd201: $i] : (~(Vd198 = vplus(Vd199, Vd201))))))) <=> ![Vd198: $i, Vd199: $i] : (~((~((~less(Vd199, Vd198)) | (Vd198 = vplus(Vd199, tptp_fun_Vd201_0(Vd199, Vd198))))) | (~(less(Vd199, Vd198) | ![Vd201: $i] : (~(Vd198 = vplus(Vd199, Vd201)))))))),
% 0.17/0.37 inference(quant_intro,[status(thm)],[37])).
% 0.17/0.37 tff(39,plain,
% 0.17/0.37 (![Vd198: $i, Vd199: $i] : (~((~((~less(Vd199, Vd198)) | (Vd198 = vplus(Vd199, tptp_fun_Vd201_0(Vd199, Vd198))))) | (~(less(Vd199, Vd198) | ![Vd201: $i] : (~(Vd198 = vplus(Vd199, Vd201))))))) <=> ![Vd198: $i, Vd199: $i] : (~((~((~less(Vd199, Vd198)) | (Vd198 = vplus(Vd199, tptp_fun_Vd201_0(Vd199, Vd198))))) | (~(less(Vd199, Vd198) | ![Vd201: $i] : (~(Vd198 = vplus(Vd199, Vd201)))))))),
% 0.17/0.37 inference(transitivity,[status(thm)],[38, 36])).
% 0.17/0.37 tff(40,plain,
% 0.17/0.37 (^[Vd198: $i, Vd199: $i] : trans(monotonicity(rewrite((less(Vd199, Vd198) | ![Vd201: $i] : (~(Vd198 = vplus(Vd199, Vd201)))) <=> (less(Vd199, Vd198) | ![Vd201: $i] : (~(Vd198 = vplus(Vd199, Vd201))))), ((((~less(Vd199, Vd198)) | (Vd198 = vplus(Vd199, tptp_fun_Vd201_0(Vd199, Vd198)))) & (less(Vd199, Vd198) | ![Vd201: $i] : (~(Vd198 = vplus(Vd199, Vd201))))) <=> (((~less(Vd199, Vd198)) | (Vd198 = vplus(Vd199, tptp_fun_Vd201_0(Vd199, Vd198)))) & (less(Vd199, Vd198) | ![Vd201: $i] : (~(Vd198 = vplus(Vd199, Vd201))))))), rewrite((((~less(Vd199, Vd198)) | (Vd198 = vplus(Vd199, tptp_fun_Vd201_0(Vd199, Vd198)))) & (less(Vd199, Vd198) | ![Vd201: $i] : (~(Vd198 = vplus(Vd199, Vd201))))) <=> (~((~((~less(Vd199, Vd198)) | (Vd198 = vplus(Vd199, tptp_fun_Vd201_0(Vd199, Vd198))))) | (~(less(Vd199, Vd198) | ![Vd201: $i] : (~(Vd198 = vplus(Vd199, Vd201)))))))), ((((~less(Vd199, Vd198)) | (Vd198 = vplus(Vd199, tptp_fun_Vd201_0(Vd199, Vd198)))) & (less(Vd199, Vd198) | ![Vd201: $i] : (~(Vd198 = vplus(Vd199, Vd201))))) <=> (~((~((~less(Vd199, Vd198)) | (Vd198 = vplus(Vd199, tptp_fun_Vd201_0(Vd199, Vd198))))) | (~(less(Vd199, Vd198) | ![Vd201: $i] : (~(Vd198 = vplus(Vd199, Vd201)))))))))),
% 0.17/0.37 inference(bind,[status(th)],[])).
% 0.17/0.37 tff(41,plain,
% 0.17/0.37 (![Vd198: $i, Vd199: $i] : (((~less(Vd199, Vd198)) | (Vd198 = vplus(Vd199, tptp_fun_Vd201_0(Vd199, Vd198)))) & (less(Vd199, Vd198) | ![Vd201: $i] : (~(Vd198 = vplus(Vd199, Vd201))))) <=> ![Vd198: $i, Vd199: $i] : (~((~((~less(Vd199, Vd198)) | (Vd198 = vplus(Vd199, tptp_fun_Vd201_0(Vd199, Vd198))))) | (~(less(Vd199, Vd198) | ![Vd201: $i] : (~(Vd198 = vplus(Vd199, Vd201)))))))),
% 0.17/0.37 inference(quant_intro,[status(thm)],[40])).
% 0.17/0.37 tff(42,plain,
% 0.17/0.37 (![Vd198: $i, Vd199: $i] : (less(Vd199, Vd198) <=> ?[Vd201: $i] : (Vd198 = vplus(Vd199, Vd201))) <=> ![Vd198: $i, Vd199: $i] : (less(Vd199, Vd198) <=> ?[Vd201: $i] : (Vd198 = vplus(Vd199, Vd201)))),
% 0.17/0.37 inference(rewrite,[status(thm)],[])).
% 0.17/0.37 tff(43,axiom,(![Vd198: $i, Vd199: $i] : (less(Vd199, Vd198) <=> ?[Vd201: $i] : (Vd198 = vplus(Vd199, Vd201)))), file('/export/starexec/sandbox/benchmark/theBenchmark.p',''def(cond(conseq(axiom(3)), 12), 1)'')).
% 0.17/0.37 tff(44,plain,
% 0.17/0.37 (![Vd198: $i, Vd199: $i] : (less(Vd199, Vd198) <=> ?[Vd201: $i] : (Vd198 = vplus(Vd199, Vd201)))),
% 0.17/0.37 inference(modus_ponens,[status(thm)],[43, 42])).
% 0.17/0.37 tff(45,plain,(
% 0.17/0.37 ![Vd198: $i, Vd199: $i] : (((~less(Vd199, Vd198)) | (Vd198 = vplus(Vd199, tptp_fun_Vd201_0(Vd199, Vd198)))) & (less(Vd199, Vd198) | ![Vd201: $i] : (~(Vd198 = vplus(Vd199, Vd201)))))),
% 0.17/0.37 inference(skolemize,[status(sab)],[44])).
% 0.17/0.37 tff(46,plain,
% 0.17/0.37 (![Vd198: $i, Vd199: $i] : (~((~((~less(Vd199, Vd198)) | (Vd198 = vplus(Vd199, tptp_fun_Vd201_0(Vd199, Vd198))))) | (~(less(Vd199, Vd198) | ![Vd201: $i] : (~(Vd198 = vplus(Vd199, Vd201)))))))),
% 0.17/0.37 inference(modus_ponens,[status(thm)],[45, 41])).
% 0.17/0.37 tff(47,plain,
% 0.17/0.37 (![Vd198: $i, Vd199: $i] : (~((~((~less(Vd199, Vd198)) | (Vd198 = vplus(Vd199, tptp_fun_Vd201_0(Vd199, Vd198))))) | (~(less(Vd199, Vd198) | ![Vd201: $i] : (~(Vd198 = vplus(Vd199, Vd201)))))))),
% 0.17/0.37 inference(modus_ponens,[status(thm)],[46, 39])).
% 0.17/0.37 tff(48,plain,
% 0.17/0.37 ((~![Vd198: $i, Vd199: $i] : (~((~((~less(Vd199, Vd198)) | (Vd198 = vplus(Vd199, tptp_fun_Vd201_0(Vd199, Vd198))))) | (~(less(Vd199, Vd198) | ![Vd201: $i] : (~(Vd198 = vplus(Vd199, Vd201)))))))) | (~((~((~less(vd203, vd204)) | (vd204 = vplus(vd203, tptp_fun_Vd201_0(vd203, vd204))))) | (~(less(vd203, vd204) | ![Vd201: $i] : (~(vd204 = vplus(vd203, Vd201)))))))),
% 0.17/0.37 inference(quant_inst,[status(thm)],[])).
% 0.17/0.37 tff(49,plain,
% 0.17/0.37 (~((~((~less(vd203, vd204)) | (vd204 = vplus(vd203, tptp_fun_Vd201_0(vd203, vd204))))) | (~(less(vd203, vd204) | ![Vd201: $i] : (~(vd204 = vplus(vd203, Vd201))))))),
% 0.17/0.37 inference(unit_resolution,[status(thm)],[48, 47])).
% 0.17/0.37 tff(50,plain,
% 0.17/0.37 (((~((~less(vd203, vd204)) | (vd204 = vplus(vd203, tptp_fun_Vd201_0(vd203, vd204))))) | (~(less(vd203, vd204) | ![Vd201: $i] : (~(vd204 = vplus(vd203, Vd201)))))) | ((~less(vd203, vd204)) | (vd204 = vplus(vd203, tptp_fun_Vd201_0(vd203, vd204))))),
% 0.17/0.37 inference(tautology,[status(thm)],[])).
% 0.17/0.37 tff(51,plain,
% 0.17/0.37 ((~less(vd203, vd204)) | (vd204 = vplus(vd203, tptp_fun_Vd201_0(vd203, vd204)))),
% 0.17/0.37 inference(unit_resolution,[status(thm)],[50, 49])).
% 0.17/0.37 tff(52,plain,
% 0.17/0.37 (less(vd203, vd204) <=> less(vd203, vd204)),
% 0.17/0.37 inference(rewrite,[status(thm)],[])).
% 0.17/0.37 tff(53,plain,
% 0.17/0.37 (less(vd203, vd204)),
% 0.17/0.37 inference(or_elim,[status(thm)],[28])).
% 0.17/0.37 tff(54,plain,
% 0.17/0.37 (less(vd203, vd204)),
% 0.17/0.37 inference(modus_ponens,[status(thm)],[53, 52])).
% 0.17/0.37 tff(55,plain,
% 0.17/0.37 ((~((~less(vd203, vd204)) | (vd204 = vplus(vd203, tptp_fun_Vd201_0(vd203, vd204))))) | (~less(vd203, vd204)) | (vd204 = vplus(vd203, tptp_fun_Vd201_0(vd203, vd204)))),
% 0.17/0.37 inference(tautology,[status(thm)],[])).
% 0.17/0.37 tff(56,plain,
% 0.17/0.37 ((~((~less(vd203, vd204)) | (vd204 = vplus(vd203, tptp_fun_Vd201_0(vd203, vd204))))) | (vd204 = vplus(vd203, tptp_fun_Vd201_0(vd203, vd204)))),
% 0.17/0.37 inference(unit_resolution,[status(thm)],[55, 54])).
% 0.17/0.37 tff(57,plain,
% 0.17/0.37 (vd204 = vplus(vd203, tptp_fun_Vd201_0(vd203, vd204))),
% 0.17/0.37 inference(unit_resolution,[status(thm)],[56, 51])).
% 0.17/0.37 tff(58,plain,
% 0.17/0.37 (vplus(vd203, tptp_fun_Vd201_0(vd203, vd204)) = vd204),
% 0.17/0.37 inference(symmetry,[status(thm)],[57])).
% 0.17/0.37 tff(59,plain,
% 0.17/0.37 (vplus(vplus(vd203, tptp_fun_Vd201_0(vd203, vd204)), tptp_fun_Vd196_1(vd203, vd204)) = vplus(vd204, tptp_fun_Vd196_1(vd203, vd204))),
% 0.17/0.37 inference(monotonicity,[status(thm)],[58])).
% 0.17/0.37 tff(60,plain,
% 0.17/0.37 (vplus(vplus(vd203, tptp_fun_Vd201_0(vd203, vd204)), tptp_fun_Vd196_1(vd203, vd204)) = vd203),
% 0.17/0.37 inference(transitivity,[status(thm)],[59, 34])).
% 0.17/0.37 tff(61,plain,
% 0.17/0.37 (vplus(vplus(vplus(vd203, tptp_fun_Vd201_0(vd203, vd204)), tptp_fun_Vd196_1(vd203, vd204)), tptp_fun_Vd201_0(vd203, vd204)) = vplus(vd203, tptp_fun_Vd201_0(vd203, vd204))),
% 0.17/0.37 inference(monotonicity,[status(thm)],[60])).
% 0.17/0.37 tff(62,plain,
% 0.17/0.37 (vplus(vd203, tptp_fun_Vd201_0(vd203, vd204)) = vplus(vplus(vplus(vd203, tptp_fun_Vd201_0(vd203, vd204)), tptp_fun_Vd196_1(vd203, vd204)), tptp_fun_Vd201_0(vd203, vd204))),
% 0.17/0.37 inference(symmetry,[status(thm)],[61])).
% 0.17/0.37 tff(63,plain,
% 0.17/0.37 (vplus(vd203, tptp_fun_Vd201_0(vd203, vd204)) = vplus(vplus(vd203, tptp_fun_Vd201_0(vd203, vd204)), vplus(tptp_fun_Vd196_1(vd203, vd204), tptp_fun_Vd201_0(vd203, vd204)))),
% 0.17/0.37 inference(transitivity,[status(thm)],[62, 9])).
% 0.17/0.37 tff(64,plain,
% 0.17/0.37 (^[Vd121: $i, Vd123: $i] : refl((~(Vd121 = vplus(Vd121, Vd123))) <=> (~(Vd121 = vplus(Vd121, Vd123))))),
% 0.17/0.37 inference(bind,[status(th)],[])).
% 0.17/0.37 tff(65,plain,
% 0.17/0.37 (![Vd121: $i, Vd123: $i] : (~(Vd121 = vplus(Vd121, Vd123))) <=> ![Vd121: $i, Vd123: $i] : (~(Vd121 = vplus(Vd121, Vd123)))),
% 0.17/0.37 inference(quant_intro,[status(thm)],[64])).
% 0.17/0.37 tff(66,plain,
% 0.17/0.37 (![Vd121: $i] : ![Vd123: $i] : (~(Vd121 = vplus(Vd121, Vd123))) <=> ![Vd121: $i, Vd123: $i] : (~(Vd121 = vplus(Vd121, Vd123)))),
% 0.17/0.37 inference(pull_quant,[status(thm)],[])).
% 0.17/0.37 tff(67,plain,
% 0.17/0.37 (![Vd121: $i] : (~?[Vd123: $i] : (Vd121 = vplus(Vd121, Vd123))) <=> ![Vd121: $i] : (~?[Vd123: $i] : (Vd121 = vplus(Vd121, Vd123)))),
% 0.17/0.37 inference(rewrite,[status(thm)],[])).
% 0.17/0.37 tff(68,plain,
% 0.17/0.37 (![Vd120: $i, Vd121: $i] : (~?[Vd123: $i] : (Vd121 = vplus(Vd121, Vd123))) <=> ![Vd121: $i] : (~?[Vd123: $i] : (Vd121 = vplus(Vd121, Vd123)))),
% 0.17/0.37 inference(elim_unused_vars,[status(thm)],[])).
% 0.17/0.37 tff(69,plain,
% 0.17/0.37 (![Vd120: $i, Vd121: $i] : ((~(Vd120 = Vd121)) | (~?[Vd123: $i] : (Vd120 = vplus(Vd121, Vd123)))) <=> ![Vd120: $i, Vd121: $i] : (~?[Vd123: $i] : (Vd121 = vplus(Vd121, Vd123)))),
% 0.17/0.37 inference(destructive_equality_resolution,[status(thm)],[])).
% 0.17/0.37 tff(70,plain,
% 0.17/0.37 (![Vd120: $i, Vd121: $i] : ((~(Vd120 = Vd121)) | (~?[Vd123: $i] : (Vd120 = vplus(Vd121, Vd123)))) <=> ![Vd121: $i] : (~?[Vd123: $i] : (Vd121 = vplus(Vd121, Vd123)))),
% 0.17/0.37 inference(transitivity,[status(thm)],[69, 68])).
% 0.17/0.37 tff(71,axiom,(![Vd120: $i, Vd121: $i] : ((~(Vd120 = Vd121)) | (~?[Vd123: $i] : (Vd120 = vplus(Vd121, Vd123))))), file('/export/starexec/sandbox/benchmark/theBenchmark.p',''ass(cond(goal(88), 0), 3)'')).
% 0.17/0.37 tff(72,plain,
% 0.17/0.37 (![Vd121: $i] : (~?[Vd123: $i] : (Vd121 = vplus(Vd121, Vd123)))),
% 0.17/0.37 inference(modus_ponens,[status(thm)],[71, 70])).
% 0.17/0.37 tff(73,plain,
% 0.17/0.37 (![Vd121: $i] : (~?[Vd123: $i] : (Vd121 = vplus(Vd121, Vd123)))),
% 0.17/0.37 inference(modus_ponens,[status(thm)],[72, 67])).
% 0.17/0.37 tff(74,plain,(
% 0.17/0.37 ![Vd121: $i] : ![Vd123: $i] : (~(Vd121 = vplus(Vd121, Vd123)))),
% 0.17/0.37 inference(skolemize,[status(sab)],[73])).
% 0.17/0.37 tff(75,plain,
% 0.17/0.37 (![Vd121: $i, Vd123: $i] : (~(Vd121 = vplus(Vd121, Vd123)))),
% 0.17/0.37 inference(modus_ponens,[status(thm)],[74, 66])).
% 0.17/0.37 tff(76,plain,
% 0.17/0.37 (![Vd121: $i, Vd123: $i] : (~(Vd121 = vplus(Vd121, Vd123)))),
% 0.17/0.37 inference(modus_ponens,[status(thm)],[75, 65])).
% 0.17/0.37 tff(77,plain,
% 0.17/0.37 ((~![Vd121: $i, Vd123: $i] : (~(Vd121 = vplus(Vd121, Vd123)))) | (~(vplus(vd203, tptp_fun_Vd201_0(vd203, vd204)) = vplus(vplus(vd203, tptp_fun_Vd201_0(vd203, vd204)), vplus(tptp_fun_Vd196_1(vd203, vd204), tptp_fun_Vd201_0(vd203, vd204)))))),
% 0.17/0.37 inference(quant_inst,[status(thm)],[])).
% 0.17/0.37 tff(78,plain,
% 0.17/0.37 ($false),
% 0.17/0.37 inference(unit_resolution,[status(thm)],[77, 76, 63])).
% 0.17/0.37 % SZS output end Proof
% 0.17/0.37 % E exiting
%------------------------------------------------------------------------------