%------------------------------------------------------------------------------
% File : Z3---4.15.1
% Problem : SWX033+1 : TPTP v9.1.0. Released v9.1.0.
% Transfm : none
% Format : tptp
% Command : run_E %s %d THM
% Computer : n012.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:37:48 AM UTC 2025
% Result : Theorem 0.20s 0.39s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12 % Problem : SWX033+1 : TPTP v9.1.0. Released v9.1.0.
% 0.03/0.12 % Command : run_E %s %d THM
% 0.12/0.33 % Computer : n012.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.33 % WCLimit : 300
% 0.12/0.33 % DateTime : Fri Jun 20 12:18:40 EDT 2025
% 0.12/0.33 % CPUTime :
% 0.20/0.39 % SZS status Theorem
% 0.20/0.39 % SZS output start Proof
% 0.20/0.39 tff(tptp_fun______type, type, (
% 0.20/0.39 tptp_fun_____: ( $i * $i ) > $i)).
% 0.20/0.39 tff(tptp_fun_Xx_36_type, type, (
% 0.20/0.39 tptp_fun_Xx_36: $i)).
% 0.20/0.39 tff(nat_succeeds_type, type, (
% 0.20/0.39 nat_succeeds: $i > $o)).
% 0.20/0.39 tff(tptp_fun_Xz_34_type, type, (
% 0.20/0.39 tptp_fun_Xz_34: $i)).
% 0.20/0.39 tff(tptp_fun_Xy_35_type, type, (
% 0.20/0.39 tptp_fun_Xy_35: $i)).
% 0.20/0.39 tff(tptp_fun_Xx2_31_type, type, (
% 0.20/0.39 tptp_fun_Xx2_31: $i)).
% 0.20/0.39 tff(s_type, type, (
% 0.20/0.39 s: $i > $i)).
% 0.20/0.39 tff(tptp_fun_Xx_30_type, type, (
% 0.20/0.39 tptp_fun_Xx_30: $i)).
% 0.20/0.39 tff(tptp_fun__0__type, type, (
% 0.20/0.39 tptp_fun__0_: $i)).
% 0.20/0.39 tff(tptp_fun_Xz_32_type, type, (
% 0.20/0.39 tptp_fun_Xz_32: $i)).
% 0.20/0.39 tff(tptp_fun_Xy_33_type, type, (
% 0.20/0.39 tptp_fun_Xy_33: $i)).
% 0.20/0.39 tff(inj_37_type, type, (
% 0.20/0.39 inj_37: $i > $i)).
% 0.20/0.39 tff(1,plain,
% 0.20/0.39 ((~![Xx: $i, Xy: $i, Xz: $i] : ((~(nat_succeeds(Xx) & (tptp_fun_____(Xx, Xy) = tptp_fun_____(Xx, Xz)))) | (Xy = Xz))) <=> (~![Xx: $i, Xy: $i, Xz: $i] : ((~(nat_succeeds(Xx) & (tptp_fun_____(Xx, Xy) = tptp_fun_____(Xx, Xz)))) | (Xy = Xz)))),
% 0.20/0.39 inference(rewrite,[status(thm)],[])).
% 0.20/0.39 tff(2,plain,
% 0.20/0.39 ((~![Xx: $i, Xy: $i, Xz: $i] : ((nat_succeeds(Xx) & (tptp_fun_____(Xx, Xy) = tptp_fun_____(Xx, Xz))) => (Xy = Xz))) <=> (~![Xx: $i, Xy: $i, Xz: $i] : ((~(nat_succeeds(Xx) & (tptp_fun_____(Xx, Xy) = tptp_fun_____(Xx, Xz)))) | (Xy = Xz)))),
% 0.20/0.39 inference(rewrite,[status(thm)],[])).
% 0.20/0.39 tff(3,axiom,(~![Xx: $i, Xy: $i, Xz: $i] : ((nat_succeeds(Xx) & (tptp_fun_____(Xx, Xy) = tptp_fun_____(Xx, Xz))) => (Xy = Xz))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p',''lemma-(plus:injective:second)'')).
% 0.20/0.39 tff(4,plain,
% 0.20/0.39 (~![Xx: $i, Xy: $i, Xz: $i] : ((~(nat_succeeds(Xx) & (tptp_fun_____(Xx, Xy) = tptp_fun_____(Xx, Xz)))) | (Xy = Xz))),
% 0.20/0.39 inference(modus_ponens,[status(thm)],[3, 2])).
% 0.20/0.39 tff(5,plain,
% 0.20/0.39 (~![Xx: $i, Xy: $i, Xz: $i] : ((~(nat_succeeds(Xx) & (tptp_fun_____(Xx, Xy) = tptp_fun_____(Xx, Xz)))) | (Xy = Xz))),
% 0.20/0.39 inference(modus_ponens,[status(thm)],[4, 1])).
% 0.20/0.39 tff(6,plain,
% 0.20/0.39 (~![Xx: $i, Xy: $i, Xz: $i] : ((~(nat_succeeds(Xx) & (tptp_fun_____(Xx, Xy) = tptp_fun_____(Xx, Xz)))) | (Xy = Xz))),
% 0.20/0.39 inference(modus_ponens,[status(thm)],[5, 1])).
% 0.20/0.39 tff(7,plain,
% 0.20/0.39 (~![Xx: $i, Xy: $i, Xz: $i] : ((~(nat_succeeds(Xx) & (tptp_fun_____(Xx, Xy) = tptp_fun_____(Xx, Xz)))) | (Xy = Xz))),
% 0.20/0.39 inference(modus_ponens,[status(thm)],[6, 1])).
% 0.20/0.39 tff(8,plain,(
% 0.20/0.39 ~((~(nat_succeeds(Xx!36) & (tptp_fun_____(Xx!36, Xy!35) = tptp_fun_____(Xx!36, Xz!34)))) | (Xy!35 = Xz!34))),
% 0.20/0.39 inference(skolemize,[status(sab)],[7])).
% 0.20/0.39 tff(9,plain,
% 0.20/0.39 (nat_succeeds(Xx!36) & (tptp_fun_____(Xx!36, Xy!35) = tptp_fun_____(Xx!36, Xz!34))),
% 0.20/0.39 inference(or_elim,[status(thm)],[8])).
% 0.20/0.39 tff(10,plain,
% 0.20/0.39 (nat_succeeds(Xx!36)),
% 0.20/0.39 inference(and_elim,[status(thm)],[9])).
% 0.20/0.39 tff(11,plain,
% 0.20/0.39 (^[Xy: $i] : refl((tptp_fun_____(|'0'|, Xy) = Xy) <=> (tptp_fun_____(|'0'|, Xy) = Xy))),
% 0.20/0.39 inference(bind,[status(th)],[])).
% 0.20/0.39 tff(12,plain,
% 0.20/0.39 (![Xy: $i] : (tptp_fun_____(|'0'|, Xy) = Xy) <=> ![Xy: $i] : (tptp_fun_____(|'0'|, Xy) = Xy)),
% 0.20/0.39 inference(quant_intro,[status(thm)],[11])).
% 0.20/0.39 tff(13,plain,
% 0.20/0.39 (![Xy: $i] : (tptp_fun_____(|'0'|, Xy) = Xy) <=> ![Xy: $i] : (tptp_fun_____(|'0'|, Xy) = Xy)),
% 0.20/0.39 inference(rewrite,[status(thm)],[])).
% 0.20/0.39 tff(14,axiom,(![Xy: $i] : (tptp_fun_____(|'0'|, Xy) = Xy)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p',''corollary-(plus:zero)'')).
% 0.20/0.39 tff(15,plain,
% 0.20/0.39 (![Xy: $i] : (tptp_fun_____(|'0'|, Xy) = Xy)),
% 0.20/0.39 inference(modus_ponens,[status(thm)],[14, 13])).
% 0.20/0.39 tff(16,plain,(
% 0.20/0.39 ![Xy: $i] : (tptp_fun_____(|'0'|, Xy) = Xy)),
% 0.20/0.39 inference(skolemize,[status(sab)],[15])).
% 0.20/0.39 tff(17,plain,
% 0.20/0.39 (![Xy: $i] : (tptp_fun_____(|'0'|, Xy) = Xy)),
% 0.20/0.39 inference(modus_ponens,[status(thm)],[16, 12])).
% 0.20/0.39 tff(18,plain,
% 0.20/0.39 ((~![Xy: $i] : (tptp_fun_____(|'0'|, Xy) = Xy)) | (tptp_fun_____(|'0'|, Xz!32) = Xz!32)),
% 0.20/0.39 inference(quant_inst,[status(thm)],[])).
% 0.20/0.39 tff(19,plain,
% 0.20/0.39 (tptp_fun_____(|'0'|, Xz!32) = Xz!32),
% 0.20/0.39 inference(unit_resolution,[status(thm)],[18, 17])).
% 0.20/0.39 tff(20,assumption,(~((~(tptp_fun_____(Xx!30, Xy!33) = tptp_fun_____(Xx!30, Xz!32))) | (Xy!33 = Xz!32) | (~((Xx!30 = |'0'|) | (~((~(Xx!30 = s(Xx2!31))) | (~nat_succeeds(Xx2!31)) | (~![Xy: $i, Xz: $i] : ((~(tptp_fun_____(Xx2!31, Xy) = tptp_fun_____(Xx2!31, Xz))) | (Xy = Xz))))))))), introduced(assumption)).
% 0.20/0.39 tff(21,plain,
% 0.20/0.39 (((~(tptp_fun_____(Xx!30, Xy!33) = tptp_fun_____(Xx!30, Xz!32))) | (Xy!33 = Xz!32) | (~((Xx!30 = |'0'|) | (~((~(Xx!30 = s(Xx2!31))) | (~nat_succeeds(Xx2!31)) | (~![Xy: $i, Xz: $i] : ((~(tptp_fun_____(Xx2!31, Xy) = tptp_fun_____(Xx2!31, Xz))) | (Xy = Xz)))))))) | ((Xx!30 = |'0'|) | (~((~(Xx!30 = s(Xx2!31))) | (~nat_succeeds(Xx2!31)) | (~![Xy: $i, Xz: $i] : ((~(tptp_fun_____(Xx2!31, Xy) = tptp_fun_____(Xx2!31, Xz))) | (Xy = Xz))))))),
% 0.20/0.39 inference(tautology,[status(thm)],[])).
% 0.20/0.39 tff(22,plain,
% 0.20/0.39 ((Xx!30 = |'0'|) | (~((~(Xx!30 = s(Xx2!31))) | (~nat_succeeds(Xx2!31)) | (~![Xy: $i, Xz: $i] : ((~(tptp_fun_____(Xx2!31, Xy) = tptp_fun_____(Xx2!31, Xz))) | (Xy = Xz)))))),
% 0.20/0.39 inference(unit_resolution,[status(thm)],[21, 20])).
% 0.20/0.39 tff(23,plain,
% 0.20/0.39 (((~(tptp_fun_____(Xx!30, Xy!33) = tptp_fun_____(Xx!30, Xz!32))) | (Xy!33 = Xz!32) | (~((Xx!30 = |'0'|) | (~((~(Xx!30 = s(Xx2!31))) | (~nat_succeeds(Xx2!31)) | (~![Xy: $i, Xz: $i] : ((~(tptp_fun_____(Xx2!31, Xy) = tptp_fun_____(Xx2!31, Xz))) | (Xy = Xz)))))))) | (~(Xy!33 = Xz!32))),
% 0.20/0.39 inference(tautology,[status(thm)],[])).
% 0.20/0.39 tff(24,plain,
% 0.20/0.39 (~(Xy!33 = Xz!32)),
% 0.20/0.39 inference(unit_resolution,[status(thm)],[23, 20])).
% 0.20/0.39 tff(25,plain,
% 0.20/0.39 (((~(tptp_fun_____(Xx!30, Xy!33) = tptp_fun_____(Xx!30, Xz!32))) | (Xy!33 = Xz!32) | (~((Xx!30 = |'0'|) | (~((~(Xx!30 = s(Xx2!31))) | (~nat_succeeds(Xx2!31)) | (~![Xy: $i, Xz: $i] : ((~(tptp_fun_____(Xx2!31, Xy) = tptp_fun_____(Xx2!31, Xz))) | (Xy = Xz)))))))) | (tptp_fun_____(Xx!30, Xy!33) = tptp_fun_____(Xx!30, Xz!32))),
% 0.20/0.39 inference(tautology,[status(thm)],[])).
% 0.20/0.39 tff(26,plain,
% 0.20/0.39 (tptp_fun_____(Xx!30, Xy!33) = tptp_fun_____(Xx!30, Xz!32)),
% 0.20/0.39 inference(unit_resolution,[status(thm)],[25, 20])).
% 0.20/0.39 tff(27,plain,
% 0.20/0.39 (![Xk!0: $i] : (inj_37(s(Xk!0)) = Xk!0) <=> ![Xk!0: $i] : (inj_37(s(Xk!0)) = Xk!0)),
% 0.20/0.39 inference(rewrite,[status(thm)],[])).
% 0.20/0.39 tff(28,plain,
% 0.20/0.39 (![Xx4: $i, Xx5: $i] : ((~(s(Xx4) = s(Xx5))) | (Xx4 = Xx5)) <=> ![Xk!0: $i] : (inj_37(s(Xk!0)) = Xk!0)),
% 0.20/0.39 inference(rewrite,[status(thm)],[])).
% 0.20/0.39 tff(29,plain,
% 0.20/0.39 (![Xx4: $i, Xx5: $i] : ((~(s(Xx4) = s(Xx5))) | (Xx4 = Xx5)) <=> ![Xx4: $i, Xx5: $i] : ((~(s(Xx4) = s(Xx5))) | (Xx4 = Xx5))),
% 0.20/0.39 inference(rewrite,[status(thm)],[])).
% 0.20/0.39 tff(30,plain,
% 0.20/0.39 (^[Xx4: $i, Xx5: $i] : rewrite(((s(Xx4) = s(Xx5)) => (Xx4 = Xx5)) <=> ((~(s(Xx4) = s(Xx5))) | (Xx4 = Xx5)))),
% 0.20/0.39 inference(bind,[status(th)],[])).
% 0.20/0.39 tff(31,plain,
% 0.20/0.39 (![Xx4: $i, Xx5: $i] : ((s(Xx4) = s(Xx5)) => (Xx4 = Xx5)) <=> ![Xx4: $i, Xx5: $i] : ((~(s(Xx4) = s(Xx5))) | (Xx4 = Xx5))),
% 0.20/0.39 inference(quant_intro,[status(thm)],[30])).
% 0.20/0.39 tff(32,axiom,(![Xx4: $i, Xx5: $i] : ((s(Xx4) = s(Xx5)) => (Xx4 = Xx5))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','id2')).
% 0.20/0.39 tff(33,plain,
% 0.20/0.39 (![Xx4: $i, Xx5: $i] : ((~(s(Xx4) = s(Xx5))) | (Xx4 = Xx5))),
% 0.20/0.39 inference(modus_ponens,[status(thm)],[32, 31])).
% 0.20/0.39 tff(34,plain,
% 0.20/0.39 (![Xx4: $i, Xx5: $i] : ((~(s(Xx4) = s(Xx5))) | (Xx4 = Xx5))),
% 0.20/0.39 inference(modus_ponens,[status(thm)],[33, 29])).
% 0.20/0.39 tff(35,plain,(
% 0.20/0.39 ![Xx4: $i, Xx5: $i] : ((~(s(Xx4) = s(Xx5))) | (Xx4 = Xx5))),
% 0.20/0.39 inference(skolemize,[status(sab)],[34])).
% 0.20/0.39 tff(36,plain,
% 0.20/0.39 (![Xk!0: $i] : (inj_37(s(Xk!0)) = Xk!0)),
% 0.20/0.39 inference(modus_ponens,[status(thm)],[35, 28])).
% 0.20/0.39 tff(37,plain,
% 0.20/0.39 (![Xk!0: $i] : (inj_37(s(Xk!0)) = Xk!0)),
% 0.20/0.39 inference(modus_ponens,[status(thm)],[36, 27])).
% 0.20/0.39 tff(38,plain,
% 0.20/0.39 ((~![Xk!0: $i] : (inj_37(s(Xk!0)) = Xk!0)) | (inj_37(s(tptp_fun_____(Xx2!31, Xz!32))) = tptp_fun_____(Xx2!31, Xz!32))),
% 0.20/0.39 inference(quant_inst,[status(thm)],[])).
% 0.20/0.39 tff(39,plain,
% 0.20/0.39 (inj_37(s(tptp_fun_____(Xx2!31, Xz!32))) = tptp_fun_____(Xx2!31, Xz!32)),
% 0.20/0.39 inference(unit_resolution,[status(thm)],[38, 37])).
% 0.20/0.39 tff(40,assumption,(~((~(Xx!30 = s(Xx2!31))) | (~nat_succeeds(Xx2!31)) | (~![Xy: $i, Xz: $i] : ((~(tptp_fun_____(Xx2!31, Xy) = tptp_fun_____(Xx2!31, Xz))) | (Xy = Xz))))), introduced(assumption)).
% 0.20/0.39 tff(41,plain,
% 0.20/0.39 (((~(Xx!30 = s(Xx2!31))) | (~nat_succeeds(Xx2!31)) | (~![Xy: $i, Xz: $i] : ((~(tptp_fun_____(Xx2!31, Xy) = tptp_fun_____(Xx2!31, Xz))) | (Xy = Xz)))) | nat_succeeds(Xx2!31)),
% 0.20/0.40 inference(tautology,[status(thm)],[])).
% 0.20/0.40 tff(42,plain,
% 0.20/0.40 (nat_succeeds(Xx2!31)),
% 0.20/0.40 inference(unit_resolution,[status(thm)],[41, 40])).
% 0.20/0.40 tff(43,plain,
% 0.20/0.40 (^[Xx: $i, Xy: $i] : refl(((~nat_succeeds(Xx)) | (tptp_fun_____(s(Xx), Xy) = s(tptp_fun_____(Xx, Xy)))) <=> ((~nat_succeeds(Xx)) | (tptp_fun_____(s(Xx), Xy) = s(tptp_fun_____(Xx, Xy)))))),
% 0.20/0.40 inference(bind,[status(th)],[])).
% 0.20/0.40 tff(44,plain,
% 0.20/0.40 (![Xx: $i, Xy: $i] : ((~nat_succeeds(Xx)) | (tptp_fun_____(s(Xx), Xy) = s(tptp_fun_____(Xx, Xy)))) <=> ![Xx: $i, Xy: $i] : ((~nat_succeeds(Xx)) | (tptp_fun_____(s(Xx), Xy) = s(tptp_fun_____(Xx, Xy))))),
% 0.20/0.40 inference(quant_intro,[status(thm)],[43])).
% 0.20/0.40 tff(45,plain,
% 0.20/0.40 (![Xx: $i, Xy: $i] : ((~nat_succeeds(Xx)) | (tptp_fun_____(s(Xx), Xy) = s(tptp_fun_____(Xx, Xy)))) <=> ![Xx: $i, Xy: $i] : ((~nat_succeeds(Xx)) | (tptp_fun_____(s(Xx), Xy) = s(tptp_fun_____(Xx, Xy))))),
% 0.20/0.40 inference(rewrite,[status(thm)],[])).
% 0.20/0.40 tff(46,plain,
% 0.20/0.40 (^[Xx: $i, Xy: $i] : rewrite((nat_succeeds(Xx) => (tptp_fun_____(s(Xx), Xy) = s(tptp_fun_____(Xx, Xy)))) <=> ((~nat_succeeds(Xx)) | (tptp_fun_____(s(Xx), Xy) = s(tptp_fun_____(Xx, Xy)))))),
% 0.20/0.40 inference(bind,[status(th)],[])).
% 0.20/0.40 tff(47,plain,
% 0.20/0.40 (![Xx: $i, Xy: $i] : (nat_succeeds(Xx) => (tptp_fun_____(s(Xx), Xy) = s(tptp_fun_____(Xx, Xy)))) <=> ![Xx: $i, Xy: $i] : ((~nat_succeeds(Xx)) | (tptp_fun_____(s(Xx), Xy) = s(tptp_fun_____(Xx, Xy))))),
% 0.20/0.40 inference(quant_intro,[status(thm)],[46])).
% 0.20/0.40 tff(48,axiom,(![Xx: $i, Xy: $i] : (nat_succeeds(Xx) => (tptp_fun_____(s(Xx), Xy) = s(tptp_fun_____(Xx, Xy))))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p',''corollary-(plus:successor)'')).
% 0.20/0.40 tff(49,plain,
% 0.20/0.40 (![Xx: $i, Xy: $i] : ((~nat_succeeds(Xx)) | (tptp_fun_____(s(Xx), Xy) = s(tptp_fun_____(Xx, Xy))))),
% 0.20/0.40 inference(modus_ponens,[status(thm)],[48, 47])).
% 0.20/0.40 tff(50,plain,
% 0.20/0.40 (![Xx: $i, Xy: $i] : ((~nat_succeeds(Xx)) | (tptp_fun_____(s(Xx), Xy) = s(tptp_fun_____(Xx, Xy))))),
% 0.20/0.40 inference(modus_ponens,[status(thm)],[49, 45])).
% 0.20/0.40 tff(51,plain,(
% 0.20/0.40 ![Xx: $i, Xy: $i] : ((~nat_succeeds(Xx)) | (tptp_fun_____(s(Xx), Xy) = s(tptp_fun_____(Xx, Xy))))),
% 0.20/0.40 inference(skolemize,[status(sab)],[50])).
% 0.20/0.40 tff(52,plain,
% 0.20/0.40 (![Xx: $i, Xy: $i] : ((~nat_succeeds(Xx)) | (tptp_fun_____(s(Xx), Xy) = s(tptp_fun_____(Xx, Xy))))),
% 0.20/0.40 inference(modus_ponens,[status(thm)],[51, 44])).
% 0.20/0.40 tff(53,plain,
% 0.20/0.40 (((~![Xx: $i, Xy: $i] : ((~nat_succeeds(Xx)) | (tptp_fun_____(s(Xx), Xy) = s(tptp_fun_____(Xx, Xy))))) | ((~nat_succeeds(Xx2!31)) | (tptp_fun_____(s(Xx2!31), Xy!33) = s(tptp_fun_____(Xx2!31, Xy!33))))) <=> ((~![Xx: $i, Xy: $i] : ((~nat_succeeds(Xx)) | (tptp_fun_____(s(Xx), Xy) = s(tptp_fun_____(Xx, Xy))))) | (~nat_succeeds(Xx2!31)) | (tptp_fun_____(s(Xx2!31), Xy!33) = s(tptp_fun_____(Xx2!31, Xy!33))))),
% 0.20/0.40 inference(rewrite,[status(thm)],[])).
% 0.20/0.40 tff(54,plain,
% 0.20/0.40 ((~![Xx: $i, Xy: $i] : ((~nat_succeeds(Xx)) | (tptp_fun_____(s(Xx), Xy) = s(tptp_fun_____(Xx, Xy))))) | ((~nat_succeeds(Xx2!31)) | (tptp_fun_____(s(Xx2!31), Xy!33) = s(tptp_fun_____(Xx2!31, Xy!33))))),
% 0.20/0.40 inference(quant_inst,[status(thm)],[])).
% 0.20/0.40 tff(55,plain,
% 0.20/0.40 ((~![Xx: $i, Xy: $i] : ((~nat_succeeds(Xx)) | (tptp_fun_____(s(Xx), Xy) = s(tptp_fun_____(Xx, Xy))))) | (~nat_succeeds(Xx2!31)) | (tptp_fun_____(s(Xx2!31), Xy!33) = s(tptp_fun_____(Xx2!31, Xy!33)))),
% 0.20/0.40 inference(modus_ponens,[status(thm)],[54, 53])).
% 0.20/0.40 tff(56,plain,
% 0.20/0.40 (tptp_fun_____(s(Xx2!31), Xy!33) = s(tptp_fun_____(Xx2!31, Xy!33))),
% 0.20/0.40 inference(unit_resolution,[status(thm)],[55, 52, 42])).
% 0.20/0.40 tff(57,plain,
% 0.20/0.40 (((~(Xx!30 = s(Xx2!31))) | (~nat_succeeds(Xx2!31)) | (~![Xy: $i, Xz: $i] : ((~(tptp_fun_____(Xx2!31, Xy) = tptp_fun_____(Xx2!31, Xz))) | (Xy = Xz)))) | (Xx!30 = s(Xx2!31))),
% 0.20/0.40 inference(tautology,[status(thm)],[])).
% 0.20/0.40 tff(58,plain,
% 0.20/0.40 (Xx!30 = s(Xx2!31)),
% 0.20/0.40 inference(unit_resolution,[status(thm)],[57, 40])).
% 0.20/0.40 tff(59,plain,
% 0.20/0.40 (s(Xx2!31) = Xx!30),
% 0.20/0.40 inference(symmetry,[status(thm)],[58])).
% 0.20/0.40 tff(60,plain,
% 0.20/0.40 (tptp_fun_____(s(Xx2!31), Xy!33) = tptp_fun_____(Xx!30, Xy!33)),
% 0.20/0.40 inference(monotonicity,[status(thm)],[59])).
% 0.20/0.40 tff(61,plain,
% 0.20/0.40 (tptp_fun_____(Xx!30, Xy!33) = tptp_fun_____(s(Xx2!31), Xy!33)),
% 0.20/0.40 inference(symmetry,[status(thm)],[60])).
% 0.20/0.40 tff(62,assumption,(tptp_fun_____(Xx!30, Xy!33) = tptp_fun_____(Xx!30, Xz!32)), introduced(assumption)).
% 0.20/0.40 tff(63,plain,
% 0.20/0.40 (tptp_fun_____(Xx!30, Xz!32) = tptp_fun_____(Xx!30, Xy!33)),
% 0.20/0.40 inference(symmetry,[status(thm)],[62])).
% 0.20/0.40 tff(64,plain,
% 0.20/0.40 (tptp_fun_____(s(Xx2!31), Xz!32) = tptp_fun_____(Xx!30, Xz!32)),
% 0.20/0.40 inference(monotonicity,[status(thm)],[59])).
% 0.20/0.40 tff(65,plain,
% 0.20/0.40 (((~![Xx: $i, Xy: $i] : ((~nat_succeeds(Xx)) | (tptp_fun_____(s(Xx), Xy) = s(tptp_fun_____(Xx, Xy))))) | ((~nat_succeeds(Xx2!31)) | (tptp_fun_____(s(Xx2!31), Xz!32) = s(tptp_fun_____(Xx2!31, Xz!32))))) <=> ((~![Xx: $i, Xy: $i] : ((~nat_succeeds(Xx)) | (tptp_fun_____(s(Xx), Xy) = s(tptp_fun_____(Xx, Xy))))) | (~nat_succeeds(Xx2!31)) | (tptp_fun_____(s(Xx2!31), Xz!32) = s(tptp_fun_____(Xx2!31, Xz!32))))),
% 0.20/0.40 inference(rewrite,[status(thm)],[])).
% 0.20/0.40 tff(66,plain,
% 0.20/0.40 ((~![Xx: $i, Xy: $i] : ((~nat_succeeds(Xx)) | (tptp_fun_____(s(Xx), Xy) = s(tptp_fun_____(Xx, Xy))))) | ((~nat_succeeds(Xx2!31)) | (tptp_fun_____(s(Xx2!31), Xz!32) = s(tptp_fun_____(Xx2!31, Xz!32))))),
% 0.20/0.40 inference(quant_inst,[status(thm)],[])).
% 0.20/0.40 tff(67,plain,
% 0.20/0.40 ((~![Xx: $i, Xy: $i] : ((~nat_succeeds(Xx)) | (tptp_fun_____(s(Xx), Xy) = s(tptp_fun_____(Xx, Xy))))) | (~nat_succeeds(Xx2!31)) | (tptp_fun_____(s(Xx2!31), Xz!32) = s(tptp_fun_____(Xx2!31, Xz!32)))),
% 0.20/0.40 inference(modus_ponens,[status(thm)],[66, 65])).
% 0.20/0.40 tff(68,plain,
% 0.20/0.40 (tptp_fun_____(s(Xx2!31), Xz!32) = s(tptp_fun_____(Xx2!31, Xz!32))),
% 0.20/0.40 inference(unit_resolution,[status(thm)],[67, 52, 42])).
% 0.20/0.40 tff(69,plain,
% 0.20/0.40 (s(tptp_fun_____(Xx2!31, Xz!32)) = tptp_fun_____(s(Xx2!31), Xz!32)),
% 0.20/0.40 inference(symmetry,[status(thm)],[68])).
% 0.20/0.40 tff(70,plain,
% 0.20/0.40 (s(tptp_fun_____(Xx2!31, Xz!32)) = s(tptp_fun_____(Xx2!31, Xy!33))),
% 0.20/0.40 inference(transitivity,[status(thm)],[69, 64, 63, 61, 56])).
% 0.20/0.40 tff(71,plain,
% 0.20/0.40 (inj_37(s(tptp_fun_____(Xx2!31, Xz!32))) = inj_37(s(tptp_fun_____(Xx2!31, Xy!33)))),
% 0.20/0.40 inference(monotonicity,[status(thm)],[70])).
% 0.20/0.40 tff(72,plain,
% 0.20/0.40 (inj_37(s(tptp_fun_____(Xx2!31, Xy!33))) = inj_37(s(tptp_fun_____(Xx2!31, Xz!32)))),
% 0.20/0.40 inference(symmetry,[status(thm)],[71])).
% 0.20/0.40 tff(73,plain,
% 0.20/0.40 ((~![Xk!0: $i] : (inj_37(s(Xk!0)) = Xk!0)) | (inj_37(s(tptp_fun_____(Xx2!31, Xy!33))) = tptp_fun_____(Xx2!31, Xy!33))),
% 0.20/0.40 inference(quant_inst,[status(thm)],[])).
% 0.20/0.40 tff(74,plain,
% 0.20/0.40 (inj_37(s(tptp_fun_____(Xx2!31, Xy!33))) = tptp_fun_____(Xx2!31, Xy!33)),
% 0.20/0.40 inference(unit_resolution,[status(thm)],[73, 37])).
% 0.20/0.40 tff(75,plain,
% 0.20/0.40 (tptp_fun_____(Xx2!31, Xy!33) = inj_37(s(tptp_fun_____(Xx2!31, Xy!33)))),
% 0.20/0.40 inference(symmetry,[status(thm)],[74])).
% 0.20/0.40 tff(76,plain,
% 0.20/0.40 (tptp_fun_____(Xx2!31, Xy!33) = tptp_fun_____(Xx2!31, Xz!32)),
% 0.20/0.40 inference(transitivity,[status(thm)],[75, 72, 39])).
% 0.20/0.40 tff(77,plain,
% 0.20/0.40 (((~(Xx!30 = s(Xx2!31))) | (~nat_succeeds(Xx2!31)) | (~![Xy: $i, Xz: $i] : ((~(tptp_fun_____(Xx2!31, Xy) = tptp_fun_____(Xx2!31, Xz))) | (Xy = Xz)))) | ![Xy: $i, Xz: $i] : ((~(tptp_fun_____(Xx2!31, Xy) = tptp_fun_____(Xx2!31, Xz))) | (Xy = Xz))),
% 0.20/0.40 inference(tautology,[status(thm)],[])).
% 0.20/0.40 tff(78,plain,
% 0.20/0.40 (![Xy: $i, Xz: $i] : ((~(tptp_fun_____(Xx2!31, Xy) = tptp_fun_____(Xx2!31, Xz))) | (Xy = Xz))),
% 0.20/0.40 inference(unit_resolution,[status(thm)],[77, 40])).
% 0.20/0.40 tff(79,assumption,(~(Xy!33 = Xz!32)), introduced(assumption)).
% 0.20/0.40 tff(80,plain,
% 0.20/0.40 (((~![Xy: $i, Xz: $i] : ((~(tptp_fun_____(Xx2!31, Xy) = tptp_fun_____(Xx2!31, Xz))) | (Xy = Xz))) | ((~(tptp_fun_____(Xx2!31, Xy!33) = tptp_fun_____(Xx2!31, Xz!32))) | (Xy!33 = Xz!32))) <=> ((~![Xy: $i, Xz: $i] : ((~(tptp_fun_____(Xx2!31, Xy) = tptp_fun_____(Xx2!31, Xz))) | (Xy = Xz))) | (~(tptp_fun_____(Xx2!31, Xy!33) = tptp_fun_____(Xx2!31, Xz!32))) | (Xy!33 = Xz!32))),
% 0.20/0.40 inference(rewrite,[status(thm)],[])).
% 0.20/0.40 tff(81,plain,
% 0.20/0.40 ((~![Xy: $i, Xz: $i] : ((~(tptp_fun_____(Xx2!31, Xy) = tptp_fun_____(Xx2!31, Xz))) | (Xy = Xz))) | ((~(tptp_fun_____(Xx2!31, Xy!33) = tptp_fun_____(Xx2!31, Xz!32))) | (Xy!33 = Xz!32))),
% 0.20/0.40 inference(quant_inst,[status(thm)],[])).
% 0.20/0.40 tff(82,plain,
% 0.20/0.40 ((~![Xy: $i, Xz: $i] : ((~(tptp_fun_____(Xx2!31, Xy) = tptp_fun_____(Xx2!31, Xz))) | (Xy = Xz))) | (~(tptp_fun_____(Xx2!31, Xy!33) = tptp_fun_____(Xx2!31, Xz!32))) | (Xy!33 = Xz!32)),
% 0.20/0.40 inference(modus_ponens,[status(thm)],[81, 80])).
% 0.20/0.40 tff(83,plain,
% 0.20/0.40 (~(tptp_fun_____(Xx2!31, Xy!33) = tptp_fun_____(Xx2!31, Xz!32))),
% 0.20/0.40 inference(unit_resolution,[status(thm)],[82, 79, 78])).
% 0.20/0.40 tff(84,plain,
% 0.20/0.40 ($false),
% 0.20/0.40 inference(unit_resolution,[status(thm)],[83, 76])).
% 0.20/0.40 tff(85,plain,(((~(Xx!30 = s(Xx2!31))) | (~nat_succeeds(Xx2!31)) | (~![Xy: $i, Xz: $i] : ((~(tptp_fun_____(Xx2!31, Xy) = tptp_fun_____(Xx2!31, Xz))) | (Xy = Xz)))) | (~(tptp_fun_____(Xx!30, Xy!33) = tptp_fun_____(Xx!30, Xz!32))) | (Xy!33 = Xz!32)), inference(lemma,lemma(discharge,[]))).
% 0.20/0.40 tff(86,plain,
% 0.20/0.40 ((~(Xx!30 = s(Xx2!31))) | (~nat_succeeds(Xx2!31)) | (~![Xy: $i, Xz: $i] : ((~(tptp_fun_____(Xx2!31, Xy) = tptp_fun_____(Xx2!31, Xz))) | (Xy = Xz)))),
% 0.20/0.40 inference(unit_resolution,[status(thm)],[85, 26, 24])).
% 0.20/0.40 tff(87,plain,
% 0.20/0.40 ((~((Xx!30 = |'0'|) | (~((~(Xx!30 = s(Xx2!31))) | (~nat_succeeds(Xx2!31)) | (~![Xy: $i, Xz: $i] : ((~(tptp_fun_____(Xx2!31, Xy) = tptp_fun_____(Xx2!31, Xz))) | (Xy = Xz))))))) | (Xx!30 = |'0'|) | (~((~(Xx!30 = s(Xx2!31))) | (~nat_succeeds(Xx2!31)) | (~![Xy: $i, Xz: $i] : ((~(tptp_fun_____(Xx2!31, Xy) = tptp_fun_____(Xx2!31, Xz))) | (Xy = Xz)))))),
% 0.20/0.40 inference(tautology,[status(thm)],[])).
% 0.20/0.40 tff(88,plain,
% 0.20/0.40 (Xx!30 = |'0'|),
% 0.20/0.40 inference(unit_resolution,[status(thm)],[87, 86, 22])).
% 0.20/0.40 tff(89,plain,
% 0.20/0.40 (|'0'| = Xx!30),
% 0.20/0.40 inference(symmetry,[status(thm)],[88])).
% 0.20/0.40 tff(90,plain,
% 0.20/0.40 (tptp_fun_____(|'0'|, Xz!32) = tptp_fun_____(Xx!30, Xz!32)),
% 0.20/0.40 inference(monotonicity,[status(thm)],[89])).
% 0.20/0.40 tff(91,plain,
% 0.20/0.40 (tptp_fun_____(Xx!30, Xz!32) = tptp_fun_____(|'0'|, Xz!32)),
% 0.20/0.40 inference(symmetry,[status(thm)],[90])).
% 0.20/0.40 tff(92,plain,
% 0.20/0.40 (tptp_fun_____(|'0'|, Xy!33) = tptp_fun_____(Xx!30, Xy!33)),
% 0.20/0.40 inference(monotonicity,[status(thm)],[89])).
% 0.20/0.40 tff(93,plain,
% 0.20/0.40 ((~![Xy: $i] : (tptp_fun_____(|'0'|, Xy) = Xy)) | (tptp_fun_____(|'0'|, Xy!33) = Xy!33)),
% 0.20/0.40 inference(quant_inst,[status(thm)],[])).
% 0.20/0.40 tff(94,plain,
% 0.20/0.40 (tptp_fun_____(|'0'|, Xy!33) = Xy!33),
% 0.20/0.40 inference(unit_resolution,[status(thm)],[93, 17])).
% 0.20/0.40 tff(95,plain,
% 0.20/0.40 (Xy!33 = tptp_fun_____(|'0'|, Xy!33)),
% 0.20/0.40 inference(symmetry,[status(thm)],[94])).
% 0.20/0.40 tff(96,plain,
% 0.20/0.40 (Xy!33 = Xz!32),
% 0.20/0.40 inference(transitivity,[status(thm)],[95, 92, 26, 91, 19])).
% 0.20/0.40 tff(97,plain,
% 0.20/0.40 ($false),
% 0.20/0.40 inference(unit_resolution,[status(thm)],[24, 96])).
% 0.20/0.40 tff(98,plain,((~(tptp_fun_____(Xx!30, Xy!33) = tptp_fun_____(Xx!30, Xz!32))) | (Xy!33 = Xz!32) | (~((Xx!30 = |'0'|) | (~((~(Xx!30 = s(Xx2!31))) | (~nat_succeeds(Xx2!31)) | (~![Xy: $i, Xz: $i] : ((~(tptp_fun_____(Xx2!31, Xy) = tptp_fun_____(Xx2!31, Xz))) | (Xy = Xz)))))))), inference(lemma,lemma(discharge,[]))).
% 0.20/0.40 tff(99,plain,
% 0.20/0.40 (((~((~(tptp_fun_____(Xx!30, Xy!33) = tptp_fun_____(Xx!30, Xz!32))) | (Xy!33 = Xz!32) | (~((Xx!30 = |'0'|) | (~((~(Xx!30 = s(Xx2!31))) | (~nat_succeeds(Xx2!31)) | (~![Xy: $i, Xz: $i] : ((~(tptp_fun_____(Xx2!31, Xy) = tptp_fun_____(Xx2!31, Xz))) | (Xy = Xz))))))))) | ![Xx: $i] : ((~nat_succeeds(Xx)) | ![Xy: $i, Xz: $i] : ((~(tptp_fun_____(Xx, Xy) = tptp_fun_____(Xx, Xz))) | (Xy = Xz)))) <=> ((~((~(tptp_fun_____(Xx!30, Xy!33) = tptp_fun_____(Xx!30, Xz!32))) | (Xy!33 = Xz!32) | (~((Xx!30 = |'0'|) | (~((~(Xx!30 = s(Xx2!31))) | (~nat_succeeds(Xx2!31)) | (~![Xy: $i, Xz: $i] : ((~(tptp_fun_____(Xx2!31, Xy) = tptp_fun_____(Xx2!31, Xz))) | (Xy = Xz))))))))) | ![Xx: $i] : ((~nat_succeeds(Xx)) | ![Xy: $i, Xz: $i] : ((~(tptp_fun_____(Xx, Xy) = tptp_fun_____(Xx, Xz))) | (Xy = Xz))))),
% 0.20/0.40 inference(rewrite,[status(thm)],[])).
% 0.20/0.40 tff(100,plain,
% 0.20/0.40 (((((Xx!30 = |'0'|) | ((Xx!30 = s(Xx2!31)) & nat_succeeds(Xx2!31) & ![Xy: $i, Xz: $i] : ((~(tptp_fun_____(Xx2!31, Xy) = tptp_fun_____(Xx2!31, Xz))) | (Xy = Xz)))) & (~((~(tptp_fun_____(Xx!30, Xy!33) = tptp_fun_____(Xx!30, Xz!32))) | (Xy!33 = Xz!32)))) | ![Xx: $i] : ((~nat_succeeds(Xx)) | ![Xy: $i, Xz: $i] : ((~(tptp_fun_____(Xx, Xy) = tptp_fun_____(Xx, Xz))) | (Xy = Xz)))) <=> ((~((~(tptp_fun_____(Xx!30, Xy!33) = tptp_fun_____(Xx!30, Xz!32))) | (Xy!33 = Xz!32) | (~((Xx!30 = |'0'|) | (~((~(Xx!30 = s(Xx2!31))) | (~nat_succeeds(Xx2!31)) | (~![Xy: $i, Xz: $i] : ((~(tptp_fun_____(Xx2!31, Xy) = tptp_fun_____(Xx2!31, Xz))) | (Xy = Xz))))))))) | ![Xx: $i] : ((~nat_succeeds(Xx)) | ![Xy: $i, Xz: $i] : ((~(tptp_fun_____(Xx, Xy) = tptp_fun_____(Xx, Xz))) | (Xy = Xz))))),
% 0.20/0.41 inference(rewrite,[status(thm)],[])).
% 0.20/0.41 tff(101,plain,
% 0.20/0.41 (((Xx!30 = s(Xx2!31)) & nat_succeeds(Xx2!31) & ![Xy: $i, Xz: $i] : ((~(tptp_fun_____(Xx2!31, Xy) = tptp_fun_____(Xx2!31, Xz))) | (Xy = Xz))) <=> ((Xx!30 = s(Xx2!31)) & nat_succeeds(Xx2!31) & ![Xy: $i, Xz: $i] : ((~(tptp_fun_____(Xx2!31, Xy) = tptp_fun_____(Xx2!31, Xz))) | (Xy = Xz)))),
% 0.20/0.41 inference(rewrite,[status(thm)],[])).
% 0.20/0.41 tff(102,plain,
% 0.20/0.41 (((Xx!30 = |'0'|) | ((Xx!30 = s(Xx2!31)) & nat_succeeds(Xx2!31) & ![Xy: $i, Xz: $i] : ((~(tptp_fun_____(Xx2!31, Xy) = tptp_fun_____(Xx2!31, Xz))) | (Xy = Xz)))) <=> ((Xx!30 = |'0'|) | ((Xx!30 = s(Xx2!31)) & nat_succeeds(Xx2!31) & ![Xy: $i, Xz: $i] : ((~(tptp_fun_____(Xx2!31, Xy) = tptp_fun_____(Xx2!31, Xz))) | (Xy = Xz))))),
% 0.20/0.41 inference(monotonicity,[status(thm)],[101])).
% 0.20/0.41 tff(103,plain,
% 0.20/0.41 ((((Xx!30 = |'0'|) | ((Xx!30 = s(Xx2!31)) & nat_succeeds(Xx2!31) & ![Xy: $i, Xz: $i] : ((~(tptp_fun_____(Xx2!31, Xy) = tptp_fun_____(Xx2!31, Xz))) | (Xy = Xz)))) & (~((~(tptp_fun_____(Xx!30, Xy!33) = tptp_fun_____(Xx!30, Xz!32))) | (Xy!33 = Xz!32)))) <=> (((Xx!30 = |'0'|) | ((Xx!30 = s(Xx2!31)) & nat_succeeds(Xx2!31) & ![Xy: $i, Xz: $i] : ((~(tptp_fun_____(Xx2!31, Xy) = tptp_fun_____(Xx2!31, Xz))) | (Xy = Xz)))) & (~((~(tptp_fun_____(Xx!30, Xy!33) = tptp_fun_____(Xx!30, Xz!32))) | (Xy!33 = Xz!32))))),
% 0.20/0.41 inference(monotonicity,[status(thm)],[102])).
% 0.20/0.41 tff(104,plain,
% 0.20/0.41 (((((Xx!30 = |'0'|) | ((Xx!30 = s(Xx2!31)) & nat_succeeds(Xx2!31) & ![Xy: $i, Xz: $i] : ((~(tptp_fun_____(Xx2!31, Xy) = tptp_fun_____(Xx2!31, Xz))) | (Xy = Xz)))) & (~((~(tptp_fun_____(Xx!30, Xy!33) = tptp_fun_____(Xx!30, Xz!32))) | (Xy!33 = Xz!32)))) | ![Xx: $i] : ((~nat_succeeds(Xx)) | ![Xy: $i, Xz: $i] : ((~(tptp_fun_____(Xx, Xy) = tptp_fun_____(Xx, Xz))) | (Xy = Xz)))) <=> ((((Xx!30 = |'0'|) | ((Xx!30 = s(Xx2!31)) & nat_succeeds(Xx2!31) & ![Xy: $i, Xz: $i] : ((~(tptp_fun_____(Xx2!31, Xy) = tptp_fun_____(Xx2!31, Xz))) | (Xy = Xz)))) & (~((~(tptp_fun_____(Xx!30, Xy!33) = tptp_fun_____(Xx!30, Xz!32))) | (Xy!33 = Xz!32)))) | ![Xx: $i] : ((~nat_succeeds(Xx)) | ![Xy: $i, Xz: $i] : ((~(tptp_fun_____(Xx, Xy) = tptp_fun_____(Xx, Xz))) | (Xy = Xz))))),
% 0.20/0.41 inference(monotonicity,[status(thm)],[103])).
% 0.20/0.41 tff(105,plain,
% 0.20/0.41 (((~![Xx: $i] : ((~((Xx = |'0'|) | ?[Xx2: $i] : ((Xx = s(Xx2)) & nat_succeeds(Xx2) & ![Xy: $i, Xz: $i] : ((~(tptp_fun_____(Xx2, Xy) = tptp_fun_____(Xx2, Xz))) | (Xy = Xz))))) | ![Xy: $i, Xz: $i] : ((~(tptp_fun_____(Xx, Xy) = tptp_fun_____(Xx, Xz))) | (Xy = Xz)))) | ![Xx: $i] : ((~nat_succeeds(Xx)) | ![Xy: $i, Xz: $i] : ((~(tptp_fun_____(Xx, Xy) = tptp_fun_____(Xx, Xz))) | (Xy = Xz)))) <=> ((~![Xx: $i] : ((~((Xx = |'0'|) | ?[Xx2: $i] : ((Xx = s(Xx2)) & nat_succeeds(Xx2) & ![Xy: $i, Xz: $i] : ((~(tptp_fun_____(Xx2, Xy) = tptp_fun_____(Xx2, Xz))) | (Xy = Xz))))) | ![Xy: $i, Xz: $i] : ((~(tptp_fun_____(Xx, Xy) = tptp_fun_____(Xx, Xz))) | (Xy = Xz)))) | ![Xx: $i] : ((~nat_succeeds(Xx)) | ![Xy: $i, Xz: $i] : ((~(tptp_fun_____(Xx, Xy) = tptp_fun_____(Xx, Xz))) | (Xy = Xz))))),
% 0.20/0.41 inference(rewrite,[status(thm)],[])).
% 0.20/0.41 tff(106,plain,
% 0.20/0.41 ((![Xx: $i] : ((~((Xx = |'0'|) | ?[Xx2: $i] : ((Xx = s(Xx2)) & nat_succeeds(Xx2) & ![Xy: $i, Xz: $i] : ((~(tptp_fun_____(Xx2, Xy) = tptp_fun_____(Xx2, Xz))) | (Xy = Xz))))) | ![Xy: $i, Xz: $i] : ((~(tptp_fun_____(Xx, Xy) = tptp_fun_____(Xx, Xz))) | (Xy = Xz))) => ![Xx: $i] : ((~nat_succeeds(Xx)) | ![Xy: $i, Xz: $i] : ((~(tptp_fun_____(Xx, Xy) = tptp_fun_____(Xx, Xz))) | (Xy = Xz)))) <=> ((~![Xx: $i] : ((~((Xx = |'0'|) | ?[Xx2: $i] : ((Xx = s(Xx2)) & nat_succeeds(Xx2) & ![Xy: $i, Xz: $i] : ((~(tptp_fun_____(Xx2, Xy) = tptp_fun_____(Xx2, Xz))) | (Xy = Xz))))) | ![Xy: $i, Xz: $i] : ((~(tptp_fun_____(Xx, Xy) = tptp_fun_____(Xx, Xz))) | (Xy = Xz)))) | ![Xx: $i] : ((~nat_succeeds(Xx)) | ![Xy: $i, Xz: $i] : ((~(tptp_fun_____(Xx, Xy) = tptp_fun_____(Xx, Xz))) | (Xy = Xz))))),
% 0.20/0.41 inference(rewrite,[status(thm)],[])).
% 0.20/0.41 tff(107,plain,
% 0.20/0.41 (^[Xx: $i] : trans(monotonicity(quant_intro(proof_bind(^[Xy: $i, Xz: $i] : rewrite(((tptp_fun_____(Xx, Xy) = tptp_fun_____(Xx, Xz)) => (Xy = Xz)) <=> ((~(tptp_fun_____(Xx, Xy) = tptp_fun_____(Xx, Xz))) | (Xy = Xz)))), (![Xy: $i, Xz: $i] : ((tptp_fun_____(Xx, Xy) = tptp_fun_____(Xx, Xz)) => (Xy = Xz)) <=> ![Xy: $i, Xz: $i] : ((~(tptp_fun_____(Xx, Xy) = tptp_fun_____(Xx, Xz))) | (Xy = Xz)))), ((nat_succeeds(Xx) => ![Xy: $i, Xz: $i] : ((tptp_fun_____(Xx, Xy) = tptp_fun_____(Xx, Xz)) => (Xy = Xz))) <=> (nat_succeeds(Xx) => ![Xy: $i, Xz: $i] : ((~(tptp_fun_____(Xx, Xy) = tptp_fun_____(Xx, Xz))) | (Xy = Xz))))), rewrite((nat_succeeds(Xx) => ![Xy: $i, Xz: $i] : ((~(tptp_fun_____(Xx, Xy) = tptp_fun_____(Xx, Xz))) | (Xy = Xz))) <=> ((~nat_succeeds(Xx)) | ![Xy: $i, Xz: $i] : ((~(tptp_fun_____(Xx, Xy) = tptp_fun_____(Xx, Xz))) | (Xy = Xz)))), ((nat_succeeds(Xx) => ![Xy: $i, Xz: $i] : ((tptp_fun_____(Xx, Xy) = tptp_fun_____(Xx, Xz)) => (Xy = Xz))) <=> ((~nat_succeeds(Xx)) | ![Xy: $i, Xz: $i] : ((~(tptp_fun_____(Xx, Xy) = tptp_fun_____(Xx, Xz))) | (Xy = Xz)))))),
% 0.20/0.41 inference(bind,[status(th)],[])).
% 0.20/0.41 tff(108,plain,
% 0.20/0.41 (![Xx: $i] : (nat_succeeds(Xx) => ![Xy: $i, Xz: $i] : ((tptp_fun_____(Xx, Xy) = tptp_fun_____(Xx, Xz)) => (Xy = Xz))) <=> ![Xx: $i] : ((~nat_succeeds(Xx)) | ![Xy: $i, Xz: $i] : ((~(tptp_fun_____(Xx, Xy) = tptp_fun_____(Xx, Xz))) | (Xy = Xz)))),
% 0.20/0.41 inference(quant_intro,[status(thm)],[107])).
% 0.20/0.41 tff(109,plain,
% 0.20/0.41 (^[Xx: $i] : trans(monotonicity(trans(monotonicity(quant_intro(proof_bind(^[Xx2: $i] : trans(monotonicity(quant_intro(proof_bind(^[Xy: $i, Xz: $i] : rewrite(((tptp_fun_____(Xx2, Xy) = tptp_fun_____(Xx2, Xz)) => (Xy = Xz)) <=> ((~(tptp_fun_____(Xx2, Xy) = tptp_fun_____(Xx2, Xz))) | (Xy = Xz)))), (![Xy: $i, Xz: $i] : ((tptp_fun_____(Xx2, Xy) = tptp_fun_____(Xx2, Xz)) => (Xy = Xz)) <=> ![Xy: $i, Xz: $i] : ((~(tptp_fun_____(Xx2, Xy) = tptp_fun_____(Xx2, Xz))) | (Xy = Xz)))), ((((Xx = s(Xx2)) & nat_succeeds(Xx2)) & ![Xy: $i, Xz: $i] : ((tptp_fun_____(Xx2, Xy) = tptp_fun_____(Xx2, Xz)) => (Xy = Xz))) <=> (((Xx = s(Xx2)) & nat_succeeds(Xx2)) & ![Xy: $i, Xz: $i] : ((~(tptp_fun_____(Xx2, Xy) = tptp_fun_____(Xx2, Xz))) | (Xy = Xz))))), rewrite((((Xx = s(Xx2)) & nat_succeeds(Xx2)) & ![Xy: $i, Xz: $i] : ((~(tptp_fun_____(Xx2, Xy) = tptp_fun_____(Xx2, Xz))) | (Xy = Xz))) <=> ((Xx = s(Xx2)) & nat_succeeds(Xx2) & ![Xy: $i, Xz: $i] : ((~(tptp_fun_____(Xx2, Xy) = tptp_fun_____(Xx2, Xz))) | (Xy = Xz)))), ((((Xx = s(Xx2)) & nat_succeeds(Xx2)) & ![Xy: $i, Xz: $i] : ((tptp_fun_____(Xx2, Xy) = tptp_fun_____(Xx2, Xz)) => (Xy = Xz))) <=> ((Xx = s(Xx2)) & nat_succeeds(Xx2) & ![Xy: $i, Xz: $i] : ((~(tptp_fun_____(Xx2, Xy) = tptp_fun_____(Xx2, Xz))) | (Xy = Xz)))))), (?[Xx2: $i] : (((Xx = s(Xx2)) & nat_succeeds(Xx2)) & ![Xy: $i, Xz: $i] : ((tptp_fun_____(Xx2, Xy) = tptp_fun_____(Xx2, Xz)) => (Xy = Xz))) <=> ?[Xx2: $i] : ((Xx = s(Xx2)) & nat_succeeds(Xx2) & ![Xy: $i, Xz: $i] : ((~(tptp_fun_____(Xx2, Xy) = tptp_fun_____(Xx2, Xz))) | (Xy = Xz))))), ((?[Xx2: $i] : (((Xx = s(Xx2)) & nat_succeeds(Xx2)) & ![Xy: $i, Xz: $i] : ((tptp_fun_____(Xx2, Xy) = tptp_fun_____(Xx2, Xz)) => (Xy = Xz))) | (Xx = |'0'|)) <=> (?[Xx2: $i] : ((Xx = s(Xx2)) & nat_succeeds(Xx2) & ![Xy: $i, Xz: $i] : ((~(tptp_fun_____(Xx2, Xy) = tptp_fun_____(Xx2, Xz))) | (Xy = Xz))) | (Xx = |'0'|)))), rewrite((?[Xx2: $i] : ((Xx = s(Xx2)) & nat_succeeds(Xx2) & ![Xy: $i, Xz: $i] : ((~(tptp_fun_____(Xx2, Xy) = tptp_fun_____(Xx2, Xz))) | (Xy = Xz))) | (Xx = |'0'|)) <=> ((Xx = |'0'|) | ?[Xx2: $i] : ((Xx = s(Xx2)) & nat_succeeds(Xx2) & ![Xy: $i, Xz: $i] : ((~(tptp_fun_____(Xx2, Xy) = tptp_fun_____(Xx2, Xz))) | (Xy = Xz))))), ((?[Xx2: $i] : (((Xx = s(Xx2)) & nat_succeeds(Xx2)) & ![Xy: $i, Xz: $i] : ((tptp_fun_____(Xx2, Xy) = tptp_fun_____(Xx2, Xz)) => (Xy = Xz))) | (Xx = |'0'|)) <=> ((Xx = |'0'|) | ?[Xx2: $i] : ((Xx = s(Xx2)) & nat_succeeds(Xx2) & ![Xy: $i, Xz: $i] : ((~(tptp_fun_____(Xx2, Xy) = tptp_fun_____(Xx2, Xz))) | (Xy = Xz)))))), quant_intro(proof_bind(^[Xy: $i, Xz: $i] : rewrite(((tptp_fun_____(Xx, Xy) = tptp_fun_____(Xx, Xz)) => (Xy = Xz)) <=> ((~(tptp_fun_____(Xx, Xy) = tptp_fun_____(Xx, Xz))) | (Xy = Xz)))), (![Xy: $i, Xz: $i] : ((tptp_fun_____(Xx, Xy) = tptp_fun_____(Xx, Xz)) => (Xy = Xz)) <=> ![Xy: $i, Xz: $i] : ((~(tptp_fun_____(Xx, Xy) = tptp_fun_____(Xx, Xz))) | (Xy = Xz)))), (((?[Xx2: $i] : (((Xx = s(Xx2)) & nat_succeeds(Xx2)) & ![Xy: $i, Xz: $i] : ((tptp_fun_____(Xx2, Xy) = tptp_fun_____(Xx2, Xz)) => (Xy = Xz))) | (Xx = |'0'|)) => ![Xy: $i, Xz: $i] : ((tptp_fun_____(Xx, Xy) = tptp_fun_____(Xx, Xz)) => (Xy = Xz))) <=> (((Xx = |'0'|) | ?[Xx2: $i] : ((Xx = s(Xx2)) & nat_succeeds(Xx2) & ![Xy: $i, Xz: $i] : ((~(tptp_fun_____(Xx2, Xy) = tptp_fun_____(Xx2, Xz))) | (Xy = Xz)))) => ![Xy: $i, Xz: $i] : ((~(tptp_fun_____(Xx, Xy) = tptp_fun_____(Xx, Xz))) | (Xy = Xz))))), rewrite((((Xx = |'0'|) | ?[Xx2: $i] : ((Xx = s(Xx2)) & nat_succeeds(Xx2) & ![Xy: $i, Xz: $i] : ((~(tptp_fun_____(Xx2, Xy) = tptp_fun_____(Xx2, Xz))) | (Xy = Xz)))) => ![Xy: $i, Xz: $i] : ((~(tptp_fun_____(Xx, Xy) = tptp_fun_____(Xx, Xz))) | (Xy = Xz))) <=> ((~((Xx = |'0'|) | ?[Xx2: $i] : ((Xx = s(Xx2)) & nat_succeeds(Xx2) & ![Xy: $i, Xz: $i] : ((~(tptp_fun_____(Xx2, Xy) = tptp_fun_____(Xx2, Xz))) | (Xy = Xz))))) | ![Xy: $i, Xz: $i] : ((~(tptp_fun_____(Xx, Xy) = tptp_fun_____(Xx, Xz))) | (Xy = Xz)))), (((?[Xx2: $i] : (((Xx = s(Xx2)) & nat_succeeds(Xx2)) & ![Xy: $i, Xz: $i] : ((tptp_fun_____(Xx2, Xy) = tptp_fun_____(Xx2, Xz)) => (Xy = Xz))) | (Xx = |'0'|)) => ![Xy: $i, Xz: $i] : ((tptp_fun_____(Xx, Xy) = tptp_fun_____(Xx, Xz)) => (Xy = Xz))) <=> ((~((Xx = |'0'|) | ?[Xx2: $i] : ((Xx = s(Xx2)) & nat_succeeds(Xx2) & ![Xy: $i, Xz: $i] : ((~(tptp_fun_____(Xx2, Xy) = tptp_fun_____(Xx2, Xz))) | (Xy = Xz))))) | ![Xy: $i, Xz: $i] : ((~(tptp_fun_____(Xx, Xy) = tptp_fun_____(Xx, Xz))) | (Xy = Xz)))))),
% 0.20/0.41 inference(bind,[status(th)],[])).
% 0.20/0.41 tff(110,plain,
% 0.20/0.41 (![Xx: $i] : ((?[Xx2: $i] : (((Xx = s(Xx2)) & nat_succeeds(Xx2)) & ![Xy: $i, Xz: $i] : ((tptp_fun_____(Xx2, Xy) = tptp_fun_____(Xx2, Xz)) => (Xy = Xz))) | (Xx = |'0'|)) => ![Xy: $i, Xz: $i] : ((tptp_fun_____(Xx, Xy) = tptp_fun_____(Xx, Xz)) => (Xy = Xz))) <=> ![Xx: $i] : ((~((Xx = |'0'|) | ?[Xx2: $i] : ((Xx = s(Xx2)) & nat_succeeds(Xx2) & ![Xy: $i, Xz: $i] : ((~(tptp_fun_____(Xx2, Xy) = tptp_fun_____(Xx2, Xz))) | (Xy = Xz))))) | ![Xy: $i, Xz: $i] : ((~(tptp_fun_____(Xx, Xy) = tptp_fun_____(Xx, Xz))) | (Xy = Xz)))),
% 0.20/0.41 inference(quant_intro,[status(thm)],[109])).
% 0.20/0.41 tff(111,plain,
% 0.20/0.41 ((![Xx: $i] : ((?[Xx2: $i] : (((Xx = s(Xx2)) & nat_succeeds(Xx2)) & ![Xy: $i, Xz: $i] : ((tptp_fun_____(Xx2, Xy) = tptp_fun_____(Xx2, Xz)) => (Xy = Xz))) | (Xx = |'0'|)) => ![Xy: $i, Xz: $i] : ((tptp_fun_____(Xx, Xy) = tptp_fun_____(Xx, Xz)) => (Xy = Xz))) => ![Xx: $i] : (nat_succeeds(Xx) => ![Xy: $i, Xz: $i] : ((tptp_fun_____(Xx, Xy) = tptp_fun_____(Xx, Xz)) => (Xy = Xz)))) <=> (![Xx: $i] : ((~((Xx = |'0'|) | ?[Xx2: $i] : ((Xx = s(Xx2)) & nat_succeeds(Xx2) & ![Xy: $i, Xz: $i] : ((~(tptp_fun_____(Xx2, Xy) = tptp_fun_____(Xx2, Xz))) | (Xy = Xz))))) | ![Xy: $i, Xz: $i] : ((~(tptp_fun_____(Xx, Xy) = tptp_fun_____(Xx, Xz))) | (Xy = Xz))) => ![Xx: $i] : ((~nat_succeeds(Xx)) | ![Xy: $i, Xz: $i] : ((~(tptp_fun_____(Xx, Xy) = tptp_fun_____(Xx, Xz))) | (Xy = Xz))))),
% 0.20/0.41 inference(monotonicity,[status(thm)],[110, 108])).
% 0.20/0.41 tff(112,plain,
% 0.20/0.41 ((![Xx: $i] : ((?[Xx2: $i] : (((Xx = s(Xx2)) & nat_succeeds(Xx2)) & ![Xy: $i, Xz: $i] : ((tptp_fun_____(Xx2, Xy) = tptp_fun_____(Xx2, Xz)) => (Xy = Xz))) | (Xx = |'0'|)) => ![Xy: $i, Xz: $i] : ((tptp_fun_____(Xx, Xy) = tptp_fun_____(Xx, Xz)) => (Xy = Xz))) => ![Xx: $i] : (nat_succeeds(Xx) => ![Xy: $i, Xz: $i] : ((tptp_fun_____(Xx, Xy) = tptp_fun_____(Xx, Xz)) => (Xy = Xz)))) <=> ((~![Xx: $i] : ((~((Xx = |'0'|) | ?[Xx2: $i] : ((Xx = s(Xx2)) & nat_succeeds(Xx2) & ![Xy: $i, Xz: $i] : ((~(tptp_fun_____(Xx2, Xy) = tptp_fun_____(Xx2, Xz))) | (Xy = Xz))))) | ![Xy: $i, Xz: $i] : ((~(tptp_fun_____(Xx, Xy) = tptp_fun_____(Xx, Xz))) | (Xy = Xz)))) | ![Xx: $i] : ((~nat_succeeds(Xx)) | ![Xy: $i, Xz: $i] : ((~(tptp_fun_____(Xx, Xy) = tptp_fun_____(Xx, Xz))) | (Xy = Xz))))),
% 0.20/0.41 inference(transitivity,[status(thm)],[111, 106])).
% 0.20/0.41 tff(113,axiom,(![Xx: $i] : ((?[Xx2: $i] : (((Xx = s(Xx2)) & nat_succeeds(Xx2)) & ![Xy: $i, Xz: $i] : ((tptp_fun_____(Xx2, Xy) = tptp_fun_____(Xx2, Xz)) => (Xy = Xz))) | (Xx = |'0'|)) => ![Xy: $i, Xz: $i] : ((tptp_fun_____(Xx, Xy) = tptp_fun_____(Xx, Xz)) => (Xy = Xz))) => ![Xx: $i] : (nat_succeeds(Xx) => ![Xy: $i, Xz: $i] : ((tptp_fun_____(Xx, Xy) = tptp_fun_____(Xx, Xz)) => (Xy = Xz)))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','induction')).
% 0.20/0.41 tff(114,plain,
% 0.20/0.41 ((~![Xx: $i] : ((~((Xx = |'0'|) | ?[Xx2: $i] : ((Xx = s(Xx2)) & nat_succeeds(Xx2) & ![Xy: $i, Xz: $i] : ((~(tptp_fun_____(Xx2, Xy) = tptp_fun_____(Xx2, Xz))) | (Xy = Xz))))) | ![Xy: $i, Xz: $i] : ((~(tptp_fun_____(Xx, Xy) = tptp_fun_____(Xx, Xz))) | (Xy = Xz)))) | ![Xx: $i] : ((~nat_succeeds(Xx)) | ![Xy: $i, Xz: $i] : ((~(tptp_fun_____(Xx, Xy) = tptp_fun_____(Xx, Xz))) | (Xy = Xz)))),
% 0.20/0.41 inference(modus_ponens,[status(thm)],[113, 112])).
% 0.20/0.41 tff(115,plain,
% 0.20/0.41 ((~![Xx: $i] : ((~((Xx = |'0'|) | ?[Xx2: $i] : ((Xx = s(Xx2)) & nat_succeeds(Xx2) & ![Xy: $i, Xz: $i] : ((~(tptp_fun_____(Xx2, Xy) = tptp_fun_____(Xx2, Xz))) | (Xy = Xz))))) | ![Xy: $i, Xz: $i] : ((~(tptp_fun_____(Xx, Xy) = tptp_fun_____(Xx, Xz))) | (Xy = Xz)))) | ![Xx: $i] : ((~nat_succeeds(Xx)) | ![Xy: $i, Xz: $i] : ((~(tptp_fun_____(Xx, Xy) = tptp_fun_____(Xx, Xz))) | (Xy = Xz)))),
% 0.20/0.41 inference(modus_ponens,[status(thm)],[114, 105])).
% 0.20/0.41 tff(116,plain,
% 0.20/0.41 ((~![Xx: $i] : ((~((Xx = |'0'|) | ?[Xx2: $i] : ((Xx = s(Xx2)) & nat_succeeds(Xx2) & ![Xy: $i, Xz: $i] : ((~(tptp_fun_____(Xx2, Xy) = tptp_fun_____(Xx2, Xz))) | (Xy = Xz))))) | ![Xy: $i, Xz: $i] : ((~(tptp_fun_____(Xx, Xy) = tptp_fun_____(Xx, Xz))) | (Xy = Xz)))) | ![Xx: $i] : ((~nat_succeeds(Xx)) | ![Xy: $i, Xz: $i] : ((~(tptp_fun_____(Xx, Xy) = tptp_fun_____(Xx, Xz))) | (Xy = Xz)))),
% 0.20/0.41 inference(modus_ponens,[status(thm)],[115, 105])).
% 0.20/0.41 tff(117,plain,
% 0.20/0.41 ((~![Xx: $i] : ((~((Xx = |'0'|) | ?[Xx2: $i] : ((Xx = s(Xx2)) & nat_succeeds(Xx2) & ![Xy: $i, Xz: $i] : ((~(tptp_fun_____(Xx2, Xy) = tptp_fun_____(Xx2, Xz))) | (Xy = Xz))))) | ![Xy: $i, Xz: $i] : ((~(tptp_fun_____(Xx, Xy) = tptp_fun_____(Xx, Xz))) | (Xy = Xz)))) | ![Xx: $i] : ((~nat_succeeds(Xx)) | ![Xy: $i, Xz: $i] : ((~(tptp_fun_____(Xx, Xy) = tptp_fun_____(Xx, Xz))) | (Xy = Xz)))),
% 0.20/0.41 inference(modus_ponens,[status(thm)],[116, 105])).
% 0.20/0.41 Proof display could not be completed: monotonicity rule is not handled
% 0.20/0.42 % E exiting
%------------------------------------------------------------------------------