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