%------------------------------------------------------------------------------
% File : Z3---4.15.1
% Problem : SWX047+1 : TPTP v9.1.0. Released v9.1.0.
% Transfm : none
% Format : tptp
% Command : run_E %s %d THM
% Computer : n009.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:49 AM UTC 2025
% Result : Theorem 0.38s 0.59s
% Output : Proof 0.38s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.13 % Problem : SWX047+1 : TPTP v9.1.0. Released v9.1.0.
% 0.07/0.13 % Command : run_E %s %d THM
% 0.14/0.34 % Computer : n009.cluster.edu
% 0.14/0.34 % Model : x86_64 x86_64
% 0.14/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.34 % Memory : 8042.1875MB
% 0.14/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.34 % CPULimit : 300
% 0.14/0.34 % WCLimit : 300
% 0.14/0.34 % DateTime : Fri Jun 20 12:20:48 EDT 2025
% 0.14/0.34 % CPUTime :
% 0.38/0.59 % SZS status Theorem
% 0.38/0.59 % SZS output start Proof
% 0.38/0.59 tff(tptp_fun_____succeeds__type, type, (
% 0.38/0.59 tptp_fun_____succeeds_: ( $i * $i ) > $o)).
% 0.38/0.59 tff(tptp_fun______type, type, (
% 0.38/0.59 tptp_fun_____: ( $i * $i ) > $i)).
% 0.38/0.59 tff(tptp_fun_Xz_40_type, type, (
% 0.38/0.59 tptp_fun_Xz_40: $i)).
% 0.38/0.59 tff(tptp_fun______type, type, (
% 0.38/0.59 tptp_fun_____: ( $i * $i ) > $i)).
% 0.38/0.59 tff(tptp_fun_Xx2_26_type, type, (
% 0.38/0.59 tptp_fun_Xx2_26: $i > $i)).
% 0.38/0.59 tff(tptp_fun_Xx_42_type, type, (
% 0.38/0.59 tptp_fun_Xx_42: $i)).
% 0.38/0.59 tff(tptp_fun_Xy_41_type, type, (
% 0.38/0.59 tptp_fun_Xy_41: $i)).
% 0.38/0.59 tff(nat_succeeds_type, type, (
% 0.38/0.59 nat_succeeds: $i > $o)).
% 0.38/0.59 tff(tptp_fun__0__type, type, (
% 0.38/0.59 tptp_fun__0_: $i)).
% 0.38/0.59 tff(s_type, type, (
% 0.38/0.59 s: $i > $i)).
% 0.38/0.59 tff(tptp_fun______succeeds__type, type, (
% 0.38/0.59 tptp_fun______succeeds_: ( $i * $i ) > $o)).
% 0.38/0.59 tff(1,plain,
% 0.38/0.59 ((~![Xx: $i, Xy: $i, Xz: $i] : ((~(nat_succeeds(Xx) & (~(Xx = |'0'|)) & tptp_fun_____succeeds_(Xy, Xz) & nat_succeeds(Xz))) | tptp_fun_____succeeds_(tptp_fun_____(Xx, Xy), tptp_fun_____(Xx, Xz)))) <=> (~![Xx: $i, Xy: $i, Xz: $i] : ((~(nat_succeeds(Xx) & (~(Xx = |'0'|)) & tptp_fun_____succeeds_(Xy, Xz) & nat_succeeds(Xz))) | tptp_fun_____succeeds_(tptp_fun_____(Xx, Xy), tptp_fun_____(Xx, Xz))))),
% 0.38/0.59 inference(rewrite,[status(thm)],[])).
% 0.38/0.59 tff(2,plain,
% 0.38/0.59 ((~![Xx: $i, Xy: $i, Xz: $i] : ((((nat_succeeds(Xx) & (~(Xx = |'0'|))) & tptp_fun_____succeeds_(Xy, Xz)) & nat_succeeds(Xz)) => tptp_fun_____succeeds_(tptp_fun_____(Xx, Xy), tptp_fun_____(Xx, Xz)))) <=> (~![Xx: $i, Xy: $i, Xz: $i] : ((~(nat_succeeds(Xx) & (~(Xx = |'0'|)) & tptp_fun_____succeeds_(Xy, Xz) & nat_succeeds(Xz))) | tptp_fun_____succeeds_(tptp_fun_____(Xx, Xy), tptp_fun_____(Xx, Xz))))),
% 0.38/0.59 inference(rewrite,[status(thm)],[])).
% 0.38/0.59 tff(3,axiom,(~![Xx: $i, Xy: $i, Xz: $i] : ((((nat_succeeds(Xx) & (~(Xx = |'0'|))) & tptp_fun_____succeeds_(Xy, Xz)) & nat_succeeds(Xz)) => tptp_fun_____succeeds_(tptp_fun_____(Xx, Xy), tptp_fun_____(Xx, Xz)))), file('/export/starexec/sandbox/benchmark/theBenchmark.p',''lemma-(times:less:second)'')).
% 0.38/0.59 tff(4,plain,
% 0.38/0.59 (~![Xx: $i, Xy: $i, Xz: $i] : ((~(nat_succeeds(Xx) & (~(Xx = |'0'|)) & tptp_fun_____succeeds_(Xy, Xz) & nat_succeeds(Xz))) | tptp_fun_____succeeds_(tptp_fun_____(Xx, Xy), tptp_fun_____(Xx, Xz)))),
% 0.38/0.59 inference(modus_ponens,[status(thm)],[3, 2])).
% 0.38/0.59 tff(5,plain,
% 0.38/0.59 (~![Xx: $i, Xy: $i, Xz: $i] : ((~(nat_succeeds(Xx) & (~(Xx = |'0'|)) & tptp_fun_____succeeds_(Xy, Xz) & nat_succeeds(Xz))) | tptp_fun_____succeeds_(tptp_fun_____(Xx, Xy), tptp_fun_____(Xx, Xz)))),
% 0.38/0.59 inference(modus_ponens,[status(thm)],[4, 1])).
% 0.38/0.59 tff(6,plain,
% 0.38/0.59 (~![Xx: $i, Xy: $i, Xz: $i] : ((~(nat_succeeds(Xx) & (~(Xx = |'0'|)) & tptp_fun_____succeeds_(Xy, Xz) & nat_succeeds(Xz))) | tptp_fun_____succeeds_(tptp_fun_____(Xx, Xy), tptp_fun_____(Xx, Xz)))),
% 0.38/0.59 inference(modus_ponens,[status(thm)],[5, 1])).
% 0.38/0.59 tff(7,plain,
% 0.38/0.59 (~![Xx: $i, Xy: $i, Xz: $i] : ((~(nat_succeeds(Xx) & (~(Xx = |'0'|)) & tptp_fun_____succeeds_(Xy, Xz) & nat_succeeds(Xz))) | tptp_fun_____succeeds_(tptp_fun_____(Xx, Xy), tptp_fun_____(Xx, Xz)))),
% 0.38/0.59 inference(modus_ponens,[status(thm)],[6, 1])).
% 0.38/0.59 tff(8,plain,(
% 0.38/0.59 ~((~(nat_succeeds(Xx!42) & (~(Xx!42 = |'0'|)) & tptp_fun_____succeeds_(Xy!41, Xz!40) & nat_succeeds(Xz!40))) | tptp_fun_____succeeds_(tptp_fun_____(Xx!42, Xy!41), tptp_fun_____(Xx!42, Xz!40)))),
% 0.38/0.59 inference(skolemize,[status(sab)],[7])).
% 0.38/0.59 tff(9,plain,
% 0.38/0.59 (nat_succeeds(Xx!42) & (~(Xx!42 = |'0'|)) & tptp_fun_____succeeds_(Xy!41, Xz!40) & nat_succeeds(Xz!40)),
% 0.38/0.59 inference(or_elim,[status(thm)],[8])).
% 0.38/0.59 tff(10,plain,
% 0.38/0.59 (nat_succeeds(Xz!40)),
% 0.38/0.59 inference(and_elim,[status(thm)],[9])).
% 0.38/0.59 tff(11,plain,
% 0.38/0.59 (nat_succeeds(Xx!42)),
% 0.38/0.59 inference(and_elim,[status(thm)],[9])).
% 0.38/0.59 tff(12,plain,
% 0.38/0.59 (^[Xx: $i, Xy: $i] : refl(((tptp_fun_____(Xx, Xy) = tptp_fun_____(Xy, Xx)) | (~nat_succeeds(Xy)) | (~nat_succeeds(Xx))) <=> ((tptp_fun_____(Xx, Xy) = tptp_fun_____(Xy, Xx)) | (~nat_succeeds(Xy)) | (~nat_succeeds(Xx))))),
% 0.38/0.59 inference(bind,[status(th)],[])).
% 0.38/0.59 tff(13,plain,
% 0.38/0.59 (![Xx: $i, Xy: $i] : ((tptp_fun_____(Xx, Xy) = tptp_fun_____(Xy, Xx)) | (~nat_succeeds(Xy)) | (~nat_succeeds(Xx))) <=> ![Xx: $i, Xy: $i] : ((tptp_fun_____(Xx, Xy) = tptp_fun_____(Xy, Xx)) | (~nat_succeeds(Xy)) | (~nat_succeeds(Xx)))),
% 0.38/0.59 inference(quant_intro,[status(thm)],[12])).
% 0.38/0.59 tff(14,plain,
% 0.38/0.59 (^[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(Xx) & nat_succeeds(Xy))) | (tptp_fun_____(Xx, Xy) = tptp_fun_____(Xy, Xx))) <=> (((~nat_succeeds(Xy)) | (~nat_succeeds(Xx))) | (tptp_fun_____(Xx, Xy) = tptp_fun_____(Xy, Xx))))), rewrite((((~nat_succeeds(Xy)) | (~nat_succeeds(Xx))) | (tptp_fun_____(Xx, Xy) = tptp_fun_____(Xy, Xx))) <=> ((tptp_fun_____(Xx, Xy) = tptp_fun_____(Xy, Xx)) | (~nat_succeeds(Xy)) | (~nat_succeeds(Xx)))), (((~(nat_succeeds(Xx) & nat_succeeds(Xy))) | (tptp_fun_____(Xx, Xy) = tptp_fun_____(Xy, Xx))) <=> ((tptp_fun_____(Xx, Xy) = tptp_fun_____(Xy, Xx)) | (~nat_succeeds(Xy)) | (~nat_succeeds(Xx)))))),
% 0.38/0.59 inference(bind,[status(th)],[])).
% 0.38/0.59 tff(15,plain,
% 0.38/0.59 (![Xx: $i, Xy: $i] : ((~(nat_succeeds(Xx) & nat_succeeds(Xy))) | (tptp_fun_____(Xx, Xy) = tptp_fun_____(Xy, Xx))) <=> ![Xx: $i, Xy: $i] : ((tptp_fun_____(Xx, Xy) = tptp_fun_____(Xy, Xx)) | (~nat_succeeds(Xy)) | (~nat_succeeds(Xx)))),
% 0.38/0.59 inference(quant_intro,[status(thm)],[14])).
% 0.38/0.59 tff(16,plain,
% 0.38/0.59 (![Xx: $i, Xy: $i] : ((~(nat_succeeds(Xx) & nat_succeeds(Xy))) | (tptp_fun_____(Xx, Xy) = tptp_fun_____(Xy, Xx))) <=> ![Xx: $i, Xy: $i] : ((~(nat_succeeds(Xx) & nat_succeeds(Xy))) | (tptp_fun_____(Xx, Xy) = tptp_fun_____(Xy, Xx)))),
% 0.38/0.59 inference(rewrite,[status(thm)],[])).
% 0.38/0.59 tff(17,plain,
% 0.38/0.59 (^[Xx: $i, Xy: $i] : rewrite(((nat_succeeds(Xx) & nat_succeeds(Xy)) => (tptp_fun_____(Xx, Xy) = tptp_fun_____(Xy, Xx))) <=> ((~(nat_succeeds(Xx) & nat_succeeds(Xy))) | (tptp_fun_____(Xx, Xy) = tptp_fun_____(Xy, Xx))))),
% 0.38/0.59 inference(bind,[status(th)],[])).
% 0.38/0.59 tff(18,plain,
% 0.38/0.59 (![Xx: $i, Xy: $i] : ((nat_succeeds(Xx) & nat_succeeds(Xy)) => (tptp_fun_____(Xx, Xy) = tptp_fun_____(Xy, Xx))) <=> ![Xx: $i, Xy: $i] : ((~(nat_succeeds(Xx) & nat_succeeds(Xy))) | (tptp_fun_____(Xx, Xy) = tptp_fun_____(Xy, Xx)))),
% 0.38/0.59 inference(quant_intro,[status(thm)],[17])).
% 0.38/0.59 tff(19,axiom,(![Xx: $i, Xy: $i] : ((nat_succeeds(Xx) & nat_succeeds(Xy)) => (tptp_fun_____(Xx, Xy) = tptp_fun_____(Xy, Xx)))), file('/export/starexec/sandbox/benchmark/theBenchmark.p',''theorem-(times:commutative)'')).
% 0.38/0.59 tff(20,plain,
% 0.38/0.59 (![Xx: $i, Xy: $i] : ((~(nat_succeeds(Xx) & nat_succeeds(Xy))) | (tptp_fun_____(Xx, Xy) = tptp_fun_____(Xy, Xx)))),
% 0.38/0.59 inference(modus_ponens,[status(thm)],[19, 18])).
% 0.38/0.59 tff(21,plain,
% 0.38/0.59 (![Xx: $i, Xy: $i] : ((~(nat_succeeds(Xx) & nat_succeeds(Xy))) | (tptp_fun_____(Xx, Xy) = tptp_fun_____(Xy, Xx)))),
% 0.38/0.59 inference(modus_ponens,[status(thm)],[20, 16])).
% 0.38/0.59 tff(22,plain,(
% 0.38/0.59 ![Xx: $i, Xy: $i] : ((~(nat_succeeds(Xx) & nat_succeeds(Xy))) | (tptp_fun_____(Xx, Xy) = tptp_fun_____(Xy, Xx)))),
% 0.38/0.59 inference(skolemize,[status(sab)],[21])).
% 0.38/0.59 tff(23,plain,
% 0.38/0.59 (![Xx: $i, Xy: $i] : ((tptp_fun_____(Xx, Xy) = tptp_fun_____(Xy, Xx)) | (~nat_succeeds(Xy)) | (~nat_succeeds(Xx)))),
% 0.38/0.59 inference(modus_ponens,[status(thm)],[22, 15])).
% 0.38/0.59 tff(24,plain,
% 0.38/0.59 (![Xx: $i, Xy: $i] : ((tptp_fun_____(Xx, Xy) = tptp_fun_____(Xy, Xx)) | (~nat_succeeds(Xy)) | (~nat_succeeds(Xx)))),
% 0.38/0.59 inference(modus_ponens,[status(thm)],[23, 13])).
% 0.38/0.59 tff(25,plain,
% 0.38/0.59 (((~![Xx: $i, Xy: $i] : ((tptp_fun_____(Xx, Xy) = tptp_fun_____(Xy, Xx)) | (~nat_succeeds(Xy)) | (~nat_succeeds(Xx)))) | ((~nat_succeeds(Xx!42)) | (~nat_succeeds(Xz!40)) | (tptp_fun_____(Xz!40, Xx!42) = tptp_fun_____(Xx!42, Xz!40)))) <=> ((~![Xx: $i, Xy: $i] : ((tptp_fun_____(Xx, Xy) = tptp_fun_____(Xy, Xx)) | (~nat_succeeds(Xy)) | (~nat_succeeds(Xx)))) | (~nat_succeeds(Xx!42)) | (~nat_succeeds(Xz!40)) | (tptp_fun_____(Xz!40, Xx!42) = tptp_fun_____(Xx!42, Xz!40)))),
% 0.38/0.59 inference(rewrite,[status(thm)],[])).
% 0.38/0.59 tff(26,plain,
% 0.38/0.59 (((tptp_fun_____(Xz!40, Xx!42) = tptp_fun_____(Xx!42, Xz!40)) | (~nat_succeeds(Xx!42)) | (~nat_succeeds(Xz!40))) <=> ((~nat_succeeds(Xx!42)) | (~nat_succeeds(Xz!40)) | (tptp_fun_____(Xz!40, Xx!42) = tptp_fun_____(Xx!42, Xz!40)))),
% 0.38/0.59 inference(rewrite,[status(thm)],[])).
% 0.38/0.59 tff(27,plain,
% 0.38/0.59 (((~![Xx: $i, Xy: $i] : ((tptp_fun_____(Xx, Xy) = tptp_fun_____(Xy, Xx)) | (~nat_succeeds(Xy)) | (~nat_succeeds(Xx)))) | ((tptp_fun_____(Xz!40, Xx!42) = tptp_fun_____(Xx!42, Xz!40)) | (~nat_succeeds(Xx!42)) | (~nat_succeeds(Xz!40)))) <=> ((~![Xx: $i, Xy: $i] : ((tptp_fun_____(Xx, Xy) = tptp_fun_____(Xy, Xx)) | (~nat_succeeds(Xy)) | (~nat_succeeds(Xx)))) | ((~nat_succeeds(Xx!42)) | (~nat_succeeds(Xz!40)) | (tptp_fun_____(Xz!40, Xx!42) = tptp_fun_____(Xx!42, Xz!40))))),
% 0.38/0.59 inference(monotonicity,[status(thm)],[26])).
% 0.38/0.59 tff(28,plain,
% 0.38/0.59 (((~![Xx: $i, Xy: $i] : ((tptp_fun_____(Xx, Xy) = tptp_fun_____(Xy, Xx)) | (~nat_succeeds(Xy)) | (~nat_succeeds(Xx)))) | ((tptp_fun_____(Xz!40, Xx!42) = tptp_fun_____(Xx!42, Xz!40)) | (~nat_succeeds(Xx!42)) | (~nat_succeeds(Xz!40)))) <=> ((~![Xx: $i, Xy: $i] : ((tptp_fun_____(Xx, Xy) = tptp_fun_____(Xy, Xx)) | (~nat_succeeds(Xy)) | (~nat_succeeds(Xx)))) | (~nat_succeeds(Xx!42)) | (~nat_succeeds(Xz!40)) | (tptp_fun_____(Xz!40, Xx!42) = tptp_fun_____(Xx!42, Xz!40)))),
% 0.38/0.59 inference(transitivity,[status(thm)],[27, 25])).
% 0.38/0.59 tff(29,plain,
% 0.38/0.59 ((~![Xx: $i, Xy: $i] : ((tptp_fun_____(Xx, Xy) = tptp_fun_____(Xy, Xx)) | (~nat_succeeds(Xy)) | (~nat_succeeds(Xx)))) | ((tptp_fun_____(Xz!40, Xx!42) = tptp_fun_____(Xx!42, Xz!40)) | (~nat_succeeds(Xx!42)) | (~nat_succeeds(Xz!40)))),
% 0.38/0.59 inference(quant_inst,[status(thm)],[])).
% 0.38/0.59 tff(30,plain,
% 0.38/0.59 ((~![Xx: $i, Xy: $i] : ((tptp_fun_____(Xx, Xy) = tptp_fun_____(Xy, Xx)) | (~nat_succeeds(Xy)) | (~nat_succeeds(Xx)))) | (~nat_succeeds(Xx!42)) | (~nat_succeeds(Xz!40)) | (tptp_fun_____(Xz!40, Xx!42) = tptp_fun_____(Xx!42, Xz!40))),
% 0.38/0.59 inference(modus_ponens,[status(thm)],[29, 28])).
% 0.38/0.59 tff(31,plain,
% 0.38/0.59 (tptp_fun_____(Xz!40, Xx!42) = tptp_fun_____(Xx!42, Xz!40)),
% 0.38/0.59 inference(unit_resolution,[status(thm)],[30, 24, 11, 10])).
% 0.38/0.59 tff(32,plain,
% 0.38/0.59 (^[Xx1: $i] : refl((~((~((Xx1 = |'0'|) | (~nat_succeeds(Xx1)) | (~((~(Xx1 = s(tptp_fun_Xx2_26(Xx1)))) | (~nat_succeeds(tptp_fun_Xx2_26(Xx1))))))) | (~(nat_succeeds(Xx1) | (~((Xx1 = |'0'|) | (~![Xx2: $i] : ((~(Xx1 = s(Xx2))) | (~nat_succeeds(Xx2)))))))))) <=> (~((~((Xx1 = |'0'|) | (~nat_succeeds(Xx1)) | (~((~(Xx1 = s(tptp_fun_Xx2_26(Xx1)))) | (~nat_succeeds(tptp_fun_Xx2_26(Xx1))))))) | (~(nat_succeeds(Xx1) | (~((Xx1 = |'0'|) | (~![Xx2: $i] : ((~(Xx1 = s(Xx2))) | (~nat_succeeds(Xx2)))))))))))),
% 0.38/0.59 inference(bind,[status(th)],[])).
% 0.38/0.59 tff(33,plain,
% 0.38/0.59 (![Xx1: $i] : (~((~((Xx1 = |'0'|) | (~nat_succeeds(Xx1)) | (~((~(Xx1 = s(tptp_fun_Xx2_26(Xx1)))) | (~nat_succeeds(tptp_fun_Xx2_26(Xx1))))))) | (~(nat_succeeds(Xx1) | (~((Xx1 = |'0'|) | (~![Xx2: $i] : ((~(Xx1 = s(Xx2))) | (~nat_succeeds(Xx2)))))))))) <=> ![Xx1: $i] : (~((~((Xx1 = |'0'|) | (~nat_succeeds(Xx1)) | (~((~(Xx1 = s(tptp_fun_Xx2_26(Xx1)))) | (~nat_succeeds(tptp_fun_Xx2_26(Xx1))))))) | (~(nat_succeeds(Xx1) | (~((Xx1 = |'0'|) | (~![Xx2: $i] : ((~(Xx1 = s(Xx2))) | (~nat_succeeds(Xx2))))))))))),
% 0.38/0.59 inference(quant_intro,[status(thm)],[32])).
% 0.38/0.59 tff(34,plain,
% 0.38/0.59 (^[Xx1: $i] : rewrite((~((~((Xx1 = |'0'|) | (~nat_succeeds(Xx1)) | (~((~(Xx1 = s(tptp_fun_Xx2_26(Xx1)))) | (~nat_succeeds(tptp_fun_Xx2_26(Xx1))))))) | (~(nat_succeeds(Xx1) | (~((Xx1 = |'0'|) | (~![Xx2: $i] : ((~(Xx1 = s(Xx2))) | (~nat_succeeds(Xx2)))))))))) <=> (~((~((Xx1 = |'0'|) | (~nat_succeeds(Xx1)) | (~((~(Xx1 = s(tptp_fun_Xx2_26(Xx1)))) | (~nat_succeeds(tptp_fun_Xx2_26(Xx1))))))) | (~(nat_succeeds(Xx1) | (~((Xx1 = |'0'|) | (~![Xx2: $i] : ((~(Xx1 = s(Xx2))) | (~nat_succeeds(Xx2)))))))))))),
% 0.38/0.59 inference(bind,[status(th)],[])).
% 0.38/0.59 tff(35,plain,
% 0.38/0.59 (![Xx1: $i] : (~((~((Xx1 = |'0'|) | (~nat_succeeds(Xx1)) | (~((~(Xx1 = s(tptp_fun_Xx2_26(Xx1)))) | (~nat_succeeds(tptp_fun_Xx2_26(Xx1))))))) | (~(nat_succeeds(Xx1) | (~((Xx1 = |'0'|) | (~![Xx2: $i] : ((~(Xx1 = s(Xx2))) | (~nat_succeeds(Xx2)))))))))) <=> ![Xx1: $i] : (~((~((Xx1 = |'0'|) | (~nat_succeeds(Xx1)) | (~((~(Xx1 = s(tptp_fun_Xx2_26(Xx1)))) | (~nat_succeeds(tptp_fun_Xx2_26(Xx1))))))) | (~(nat_succeeds(Xx1) | (~((Xx1 = |'0'|) | (~![Xx2: $i] : ((~(Xx1 = s(Xx2))) | (~nat_succeeds(Xx2))))))))))),
% 0.38/0.59 inference(quant_intro,[status(thm)],[34])).
% 0.38/0.59 tff(36,plain,
% 0.38/0.59 (![Xx1: $i] : (~((~((Xx1 = |'0'|) | (~nat_succeeds(Xx1)) | (~((~(Xx1 = s(tptp_fun_Xx2_26(Xx1)))) | (~nat_succeeds(tptp_fun_Xx2_26(Xx1))))))) | (~(nat_succeeds(Xx1) | (~((Xx1 = |'0'|) | (~![Xx2: $i] : ((~(Xx1 = s(Xx2))) | (~nat_succeeds(Xx2)))))))))) <=> ![Xx1: $i] : (~((~((Xx1 = |'0'|) | (~nat_succeeds(Xx1)) | (~((~(Xx1 = s(tptp_fun_Xx2_26(Xx1)))) | (~nat_succeeds(tptp_fun_Xx2_26(Xx1))))))) | (~(nat_succeeds(Xx1) | (~((Xx1 = |'0'|) | (~![Xx2: $i] : ((~(Xx1 = s(Xx2))) | (~nat_succeeds(Xx2))))))))))),
% 0.38/0.59 inference(transitivity,[status(thm)],[35, 33])).
% 0.38/0.59 tff(37,plain,
% 0.38/0.59 (^[Xx1: $i] : trans(monotonicity(trans(monotonicity(rewrite(((Xx1 = s(tptp_fun_Xx2_26(Xx1))) & nat_succeeds(tptp_fun_Xx2_26(Xx1))) <=> (~((~(Xx1 = s(tptp_fun_Xx2_26(Xx1)))) | (~nat_succeeds(tptp_fun_Xx2_26(Xx1)))))), (((Xx1 = |'0'|) | (~nat_succeeds(Xx1)) | ((Xx1 = s(tptp_fun_Xx2_26(Xx1))) & nat_succeeds(tptp_fun_Xx2_26(Xx1)))) <=> ((Xx1 = |'0'|) | (~nat_succeeds(Xx1)) | (~((~(Xx1 = s(tptp_fun_Xx2_26(Xx1)))) | (~nat_succeeds(tptp_fun_Xx2_26(Xx1)))))))), rewrite(((Xx1 = |'0'|) | (~nat_succeeds(Xx1)) | (~((~(Xx1 = s(tptp_fun_Xx2_26(Xx1)))) | (~nat_succeeds(tptp_fun_Xx2_26(Xx1)))))) <=> ((Xx1 = |'0'|) | (~nat_succeeds(Xx1)) | (~((~(Xx1 = s(tptp_fun_Xx2_26(Xx1)))) | (~nat_succeeds(tptp_fun_Xx2_26(Xx1))))))), (((Xx1 = |'0'|) | (~nat_succeeds(Xx1)) | ((Xx1 = s(tptp_fun_Xx2_26(Xx1))) & nat_succeeds(tptp_fun_Xx2_26(Xx1)))) <=> ((Xx1 = |'0'|) | (~nat_succeeds(Xx1)) | (~((~(Xx1 = s(tptp_fun_Xx2_26(Xx1)))) | (~nat_succeeds(tptp_fun_Xx2_26(Xx1)))))))), rewrite((nat_succeeds(Xx1) | ((~(Xx1 = |'0'|)) & ![Xx2: $i] : (~((Xx1 = s(Xx2)) & nat_succeeds(Xx2))))) <=> (nat_succeeds(Xx1) | (~((Xx1 = |'0'|) | (~![Xx2: $i] : ((~(Xx1 = s(Xx2))) | (~nat_succeeds(Xx2)))))))), ((((Xx1 = |'0'|) | (~nat_succeeds(Xx1)) | ((Xx1 = s(tptp_fun_Xx2_26(Xx1))) & nat_succeeds(tptp_fun_Xx2_26(Xx1)))) & (nat_succeeds(Xx1) | ((~(Xx1 = |'0'|)) & ![Xx2: $i] : (~((Xx1 = s(Xx2)) & nat_succeeds(Xx2)))))) <=> (((Xx1 = |'0'|) | (~nat_succeeds(Xx1)) | (~((~(Xx1 = s(tptp_fun_Xx2_26(Xx1)))) | (~nat_succeeds(tptp_fun_Xx2_26(Xx1)))))) & (nat_succeeds(Xx1) | (~((Xx1 = |'0'|) | (~![Xx2: $i] : ((~(Xx1 = s(Xx2))) | (~nat_succeeds(Xx2)))))))))), rewrite((((Xx1 = |'0'|) | (~nat_succeeds(Xx1)) | (~((~(Xx1 = s(tptp_fun_Xx2_26(Xx1)))) | (~nat_succeeds(tptp_fun_Xx2_26(Xx1)))))) & (nat_succeeds(Xx1) | (~((Xx1 = |'0'|) | (~![Xx2: $i] : ((~(Xx1 = s(Xx2))) | (~nat_succeeds(Xx2)))))))) <=> (~((~((Xx1 = |'0'|) | (~nat_succeeds(Xx1)) | (~((~(Xx1 = s(tptp_fun_Xx2_26(Xx1)))) | (~nat_succeeds(tptp_fun_Xx2_26(Xx1))))))) | (~(nat_succeeds(Xx1) | (~((Xx1 = |'0'|) | (~![Xx2: $i] : ((~(Xx1 = s(Xx2))) | (~nat_succeeds(Xx2))))))))))), ((((Xx1 = |'0'|) | (~nat_succeeds(Xx1)) | ((Xx1 = s(tptp_fun_Xx2_26(Xx1))) & nat_succeeds(tptp_fun_Xx2_26(Xx1)))) & (nat_succeeds(Xx1) | ((~(Xx1 = |'0'|)) & ![Xx2: $i] : (~((Xx1 = s(Xx2)) & nat_succeeds(Xx2)))))) <=> (~((~((Xx1 = |'0'|) | (~nat_succeeds(Xx1)) | (~((~(Xx1 = s(tptp_fun_Xx2_26(Xx1)))) | (~nat_succeeds(tptp_fun_Xx2_26(Xx1))))))) | (~(nat_succeeds(Xx1) | (~((Xx1 = |'0'|) | (~![Xx2: $i] : ((~(Xx1 = s(Xx2))) | (~nat_succeeds(Xx2))))))))))))),
% 0.38/0.59 inference(bind,[status(th)],[])).
% 0.38/0.59 tff(38,plain,
% 0.38/0.59 (![Xx1: $i] : (((Xx1 = |'0'|) | (~nat_succeeds(Xx1)) | ((Xx1 = s(tptp_fun_Xx2_26(Xx1))) & nat_succeeds(tptp_fun_Xx2_26(Xx1)))) & (nat_succeeds(Xx1) | ((~(Xx1 = |'0'|)) & ![Xx2: $i] : (~((Xx1 = s(Xx2)) & nat_succeeds(Xx2)))))) <=> ![Xx1: $i] : (~((~((Xx1 = |'0'|) | (~nat_succeeds(Xx1)) | (~((~(Xx1 = s(tptp_fun_Xx2_26(Xx1)))) | (~nat_succeeds(tptp_fun_Xx2_26(Xx1))))))) | (~(nat_succeeds(Xx1) | (~((Xx1 = |'0'|) | (~![Xx2: $i] : ((~(Xx1 = s(Xx2))) | (~nat_succeeds(Xx2))))))))))),
% 0.38/0.59 inference(quant_intro,[status(thm)],[37])).
% 0.38/0.59 tff(39,plain,
% 0.38/0.59 (^[Xx1: $i] : rewrite((((~nat_succeeds(Xx1)) | ((Xx1 = |'0'|) | ((Xx1 = s(tptp_fun_Xx2_26(Xx1))) & nat_succeeds(tptp_fun_Xx2_26(Xx1))))) & (nat_succeeds(Xx1) | ((~(Xx1 = |'0'|)) & ![Xx2: $i] : (~((Xx1 = s(Xx2)) & nat_succeeds(Xx2)))))) <=> (((Xx1 = |'0'|) | (~nat_succeeds(Xx1)) | ((Xx1 = s(tptp_fun_Xx2_26(Xx1))) & nat_succeeds(tptp_fun_Xx2_26(Xx1)))) & (nat_succeeds(Xx1) | ((~(Xx1 = |'0'|)) & ![Xx2: $i] : (~((Xx1 = s(Xx2)) & nat_succeeds(Xx2)))))))),
% 0.38/0.60 inference(bind,[status(th)],[])).
% 0.38/0.60 tff(40,plain,
% 0.38/0.60 (![Xx1: $i] : (((~nat_succeeds(Xx1)) | ((Xx1 = |'0'|) | ((Xx1 = s(tptp_fun_Xx2_26(Xx1))) & nat_succeeds(tptp_fun_Xx2_26(Xx1))))) & (nat_succeeds(Xx1) | ((~(Xx1 = |'0'|)) & ![Xx2: $i] : (~((Xx1 = s(Xx2)) & nat_succeeds(Xx2)))))) <=> ![Xx1: $i] : (((Xx1 = |'0'|) | (~nat_succeeds(Xx1)) | ((Xx1 = s(tptp_fun_Xx2_26(Xx1))) & nat_succeeds(tptp_fun_Xx2_26(Xx1)))) & (nat_succeeds(Xx1) | ((~(Xx1 = |'0'|)) & ![Xx2: $i] : (~((Xx1 = s(Xx2)) & nat_succeeds(Xx2))))))),
% 0.38/0.60 inference(quant_intro,[status(thm)],[39])).
% 0.38/0.60 tff(41,plain,
% 0.38/0.60 (![Xx1: $i] : (nat_succeeds(Xx1) <=> ((Xx1 = |'0'|) | ?[Xx2: $i] : ((Xx1 = s(Xx2)) & nat_succeeds(Xx2)))) <=> ![Xx1: $i] : (nat_succeeds(Xx1) <=> ((Xx1 = |'0'|) | ?[Xx2: $i] : ((Xx1 = s(Xx2)) & nat_succeeds(Xx2))))),
% 0.38/0.60 inference(rewrite,[status(thm)],[])).
% 0.38/0.60 tff(42,plain,
% 0.38/0.60 (^[Xx1: $i] : rewrite((nat_succeeds(Xx1) <=> (?[Xx2: $i] : ((Xx1 = s(Xx2)) & nat_succeeds(Xx2)) | (Xx1 = |'0'|))) <=> (nat_succeeds(Xx1) <=> ((Xx1 = |'0'|) | ?[Xx2: $i] : ((Xx1 = s(Xx2)) & nat_succeeds(Xx2)))))),
% 0.38/0.60 inference(bind,[status(th)],[])).
% 0.38/0.60 tff(43,plain,
% 0.38/0.60 (![Xx1: $i] : (nat_succeeds(Xx1) <=> (?[Xx2: $i] : ((Xx1 = s(Xx2)) & nat_succeeds(Xx2)) | (Xx1 = |'0'|))) <=> ![Xx1: $i] : (nat_succeeds(Xx1) <=> ((Xx1 = |'0'|) | ?[Xx2: $i] : ((Xx1 = s(Xx2)) & nat_succeeds(Xx2))))),
% 0.38/0.60 inference(quant_intro,[status(thm)],[42])).
% 0.38/0.60 tff(44,axiom,(![Xx1: $i] : (nat_succeeds(Xx1) <=> (?[Xx2: $i] : ((Xx1 = s(Xx2)) & nat_succeeds(Xx2)) | (Xx1 = |'0'|)))), file('/export/starexec/sandbox/benchmark/theBenchmark.p','id27')).
% 0.38/0.60 tff(45,plain,
% 0.38/0.60 (![Xx1: $i] : (nat_succeeds(Xx1) <=> ((Xx1 = |'0'|) | ?[Xx2: $i] : ((Xx1 = s(Xx2)) & nat_succeeds(Xx2))))),
% 0.38/0.60 inference(modus_ponens,[status(thm)],[44, 43])).
% 0.38/0.60 tff(46,plain,
% 0.38/0.60 (![Xx1: $i] : (nat_succeeds(Xx1) <=> ((Xx1 = |'0'|) | ?[Xx2: $i] : ((Xx1 = s(Xx2)) & nat_succeeds(Xx2))))),
% 0.38/0.60 inference(modus_ponens,[status(thm)],[45, 41])).
% 0.38/0.60 tff(47,plain,(
% 0.38/0.60 ![Xx1: $i] : (((~nat_succeeds(Xx1)) | ((Xx1 = |'0'|) | ((Xx1 = s(tptp_fun_Xx2_26(Xx1))) & nat_succeeds(tptp_fun_Xx2_26(Xx1))))) & (nat_succeeds(Xx1) | ((~(Xx1 = |'0'|)) & ![Xx2: $i] : (~((Xx1 = s(Xx2)) & nat_succeeds(Xx2))))))),
% 0.38/0.60 inference(skolemize,[status(sab)],[46])).
% 0.38/0.60 tff(48,plain,
% 0.38/0.60 (![Xx1: $i] : (((Xx1 = |'0'|) | (~nat_succeeds(Xx1)) | ((Xx1 = s(tptp_fun_Xx2_26(Xx1))) & nat_succeeds(tptp_fun_Xx2_26(Xx1)))) & (nat_succeeds(Xx1) | ((~(Xx1 = |'0'|)) & ![Xx2: $i] : (~((Xx1 = s(Xx2)) & nat_succeeds(Xx2))))))),
% 0.38/0.60 inference(modus_ponens,[status(thm)],[47, 40])).
% 0.38/0.60 tff(49,plain,
% 0.38/0.60 (![Xx1: $i] : (~((~((Xx1 = |'0'|) | (~nat_succeeds(Xx1)) | (~((~(Xx1 = s(tptp_fun_Xx2_26(Xx1)))) | (~nat_succeeds(tptp_fun_Xx2_26(Xx1))))))) | (~(nat_succeeds(Xx1) | (~((Xx1 = |'0'|) | (~![Xx2: $i] : ((~(Xx1 = s(Xx2))) | (~nat_succeeds(Xx2))))))))))),
% 0.38/0.60 inference(modus_ponens,[status(thm)],[48, 38])).
% 0.38/0.60 tff(50,plain,
% 0.38/0.60 (![Xx1: $i] : (~((~((Xx1 = |'0'|) | (~nat_succeeds(Xx1)) | (~((~(Xx1 = s(tptp_fun_Xx2_26(Xx1)))) | (~nat_succeeds(tptp_fun_Xx2_26(Xx1))))))) | (~(nat_succeeds(Xx1) | (~((Xx1 = |'0'|) | (~![Xx2: $i] : ((~(Xx1 = s(Xx2))) | (~nat_succeeds(Xx2))))))))))),
% 0.38/0.60 inference(modus_ponens,[status(thm)],[49, 36])).
% 0.38/0.60 tff(51,plain,
% 0.38/0.60 (((~![Xx1: $i] : (~((~((Xx1 = |'0'|) | (~nat_succeeds(Xx1)) | (~((~(Xx1 = s(tptp_fun_Xx2_26(Xx1)))) | (~nat_succeeds(tptp_fun_Xx2_26(Xx1))))))) | (~(nat_succeeds(Xx1) | (~((Xx1 = |'0'|) | (~![Xx2: $i] : ((~(Xx1 = s(Xx2))) | (~nat_succeeds(Xx2))))))))))) | (~((~((Xx!42 = |'0'|) | (~nat_succeeds(Xx!42)) | (~((~nat_succeeds(tptp_fun_Xx2_26(Xx!42))) | (~(Xx!42 = s(tptp_fun_Xx2_26(Xx!42)))))))) | (~(nat_succeeds(Xx!42) | (~((Xx!42 = |'0'|) | (~![Xx2: $i] : ((~nat_succeeds(Xx2)) | (~(Xx!42 = s(Xx2)))))))))))) <=> ((~![Xx1: $i] : (~((~((Xx1 = |'0'|) | (~nat_succeeds(Xx1)) | (~((~(Xx1 = s(tptp_fun_Xx2_26(Xx1)))) | (~nat_succeeds(tptp_fun_Xx2_26(Xx1))))))) | (~(nat_succeeds(Xx1) | (~((Xx1 = |'0'|) | (~![Xx2: $i] : ((~(Xx1 = s(Xx2))) | (~nat_succeeds(Xx2))))))))))) | (~((~((Xx!42 = |'0'|) | (~nat_succeeds(Xx!42)) | (~((~nat_succeeds(tptp_fun_Xx2_26(Xx!42))) | (~(Xx!42 = s(tptp_fun_Xx2_26(Xx!42)))))))) | (~(nat_succeeds(Xx!42) | (~((Xx!42 = |'0'|) | (~![Xx2: $i] : ((~nat_succeeds(Xx2)) | (~(Xx!42 = s(Xx2))))))))))))),
% 0.38/0.60 inference(rewrite,[status(thm)],[])).
% 0.38/0.60 tff(52,plain,
% 0.38/0.60 ((~((~((Xx!42 = |'0'|) | (~nat_succeeds(Xx!42)) | (~((~(Xx!42 = s(tptp_fun_Xx2_26(Xx!42)))) | (~nat_succeeds(tptp_fun_Xx2_26(Xx!42))))))) | (~(nat_succeeds(Xx!42) | (~((Xx!42 = |'0'|) | (~![Xx2: $i] : ((~(Xx!42 = s(Xx2))) | (~nat_succeeds(Xx2)))))))))) <=> (~((~((Xx!42 = |'0'|) | (~nat_succeeds(Xx!42)) | (~((~nat_succeeds(tptp_fun_Xx2_26(Xx!42))) | (~(Xx!42 = s(tptp_fun_Xx2_26(Xx!42)))))))) | (~(nat_succeeds(Xx!42) | (~((Xx!42 = |'0'|) | (~![Xx2: $i] : ((~nat_succeeds(Xx2)) | (~(Xx!42 = s(Xx2)))))))))))),
% 0.38/0.60 inference(rewrite,[status(thm)],[])).
% 0.38/0.60 tff(53,plain,
% 0.38/0.60 (((~![Xx1: $i] : (~((~((Xx1 = |'0'|) | (~nat_succeeds(Xx1)) | (~((~(Xx1 = s(tptp_fun_Xx2_26(Xx1)))) | (~nat_succeeds(tptp_fun_Xx2_26(Xx1))))))) | (~(nat_succeeds(Xx1) | (~((Xx1 = |'0'|) | (~![Xx2: $i] : ((~(Xx1 = s(Xx2))) | (~nat_succeeds(Xx2))))))))))) | (~((~((Xx!42 = |'0'|) | (~nat_succeeds(Xx!42)) | (~((~(Xx!42 = s(tptp_fun_Xx2_26(Xx!42)))) | (~nat_succeeds(tptp_fun_Xx2_26(Xx!42))))))) | (~(nat_succeeds(Xx!42) | (~((Xx!42 = |'0'|) | (~![Xx2: $i] : ((~(Xx!42 = s(Xx2))) | (~nat_succeeds(Xx2))))))))))) <=> ((~![Xx1: $i] : (~((~((Xx1 = |'0'|) | (~nat_succeeds(Xx1)) | (~((~(Xx1 = s(tptp_fun_Xx2_26(Xx1)))) | (~nat_succeeds(tptp_fun_Xx2_26(Xx1))))))) | (~(nat_succeeds(Xx1) | (~((Xx1 = |'0'|) | (~![Xx2: $i] : ((~(Xx1 = s(Xx2))) | (~nat_succeeds(Xx2))))))))))) | (~((~((Xx!42 = |'0'|) | (~nat_succeeds(Xx!42)) | (~((~nat_succeeds(tptp_fun_Xx2_26(Xx!42))) | (~(Xx!42 = s(tptp_fun_Xx2_26(Xx!42)))))))) | (~(nat_succeeds(Xx!42) | (~((Xx!42 = |'0'|) | (~![Xx2: $i] : ((~nat_succeeds(Xx2)) | (~(Xx!42 = s(Xx2))))))))))))),
% 0.38/0.60 inference(monotonicity,[status(thm)],[52])).
% 0.38/0.60 tff(54,plain,
% 0.38/0.60 (((~![Xx1: $i] : (~((~((Xx1 = |'0'|) | (~nat_succeeds(Xx1)) | (~((~(Xx1 = s(tptp_fun_Xx2_26(Xx1)))) | (~nat_succeeds(tptp_fun_Xx2_26(Xx1))))))) | (~(nat_succeeds(Xx1) | (~((Xx1 = |'0'|) | (~![Xx2: $i] : ((~(Xx1 = s(Xx2))) | (~nat_succeeds(Xx2))))))))))) | (~((~((Xx!42 = |'0'|) | (~nat_succeeds(Xx!42)) | (~((~(Xx!42 = s(tptp_fun_Xx2_26(Xx!42)))) | (~nat_succeeds(tptp_fun_Xx2_26(Xx!42))))))) | (~(nat_succeeds(Xx!42) | (~((Xx!42 = |'0'|) | (~![Xx2: $i] : ((~(Xx!42 = s(Xx2))) | (~nat_succeeds(Xx2))))))))))) <=> ((~![Xx1: $i] : (~((~((Xx1 = |'0'|) | (~nat_succeeds(Xx1)) | (~((~(Xx1 = s(tptp_fun_Xx2_26(Xx1)))) | (~nat_succeeds(tptp_fun_Xx2_26(Xx1))))))) | (~(nat_succeeds(Xx1) | (~((Xx1 = |'0'|) | (~![Xx2: $i] : ((~(Xx1 = s(Xx2))) | (~nat_succeeds(Xx2))))))))))) | (~((~((Xx!42 = |'0'|) | (~nat_succeeds(Xx!42)) | (~((~nat_succeeds(tptp_fun_Xx2_26(Xx!42))) | (~(Xx!42 = s(tptp_fun_Xx2_26(Xx!42)))))))) | (~(nat_succeeds(Xx!42) | (~((Xx!42 = |'0'|) | (~![Xx2: $i] : ((~nat_succeeds(Xx2)) | (~(Xx!42 = s(Xx2))))))))))))),
% 0.38/0.60 inference(transitivity,[status(thm)],[53, 51])).
% 0.38/0.60 tff(55,plain,
% 0.38/0.60 ((~![Xx1: $i] : (~((~((Xx1 = |'0'|) | (~nat_succeeds(Xx1)) | (~((~(Xx1 = s(tptp_fun_Xx2_26(Xx1)))) | (~nat_succeeds(tptp_fun_Xx2_26(Xx1))))))) | (~(nat_succeeds(Xx1) | (~((Xx1 = |'0'|) | (~![Xx2: $i] : ((~(Xx1 = s(Xx2))) | (~nat_succeeds(Xx2))))))))))) | (~((~((Xx!42 = |'0'|) | (~nat_succeeds(Xx!42)) | (~((~(Xx!42 = s(tptp_fun_Xx2_26(Xx!42)))) | (~nat_succeeds(tptp_fun_Xx2_26(Xx!42))))))) | (~(nat_succeeds(Xx!42) | (~((Xx!42 = |'0'|) | (~![Xx2: $i] : ((~(Xx!42 = s(Xx2))) | (~nat_succeeds(Xx2))))))))))),
% 0.38/0.60 inference(quant_inst,[status(thm)],[])).
% 0.38/0.60 tff(56,plain,
% 0.38/0.60 ((~![Xx1: $i] : (~((~((Xx1 = |'0'|) | (~nat_succeeds(Xx1)) | (~((~(Xx1 = s(tptp_fun_Xx2_26(Xx1)))) | (~nat_succeeds(tptp_fun_Xx2_26(Xx1))))))) | (~(nat_succeeds(Xx1) | (~((Xx1 = |'0'|) | (~![Xx2: $i] : ((~(Xx1 = s(Xx2))) | (~nat_succeeds(Xx2))))))))))) | (~((~((Xx!42 = |'0'|) | (~nat_succeeds(Xx!42)) | (~((~nat_succeeds(tptp_fun_Xx2_26(Xx!42))) | (~(Xx!42 = s(tptp_fun_Xx2_26(Xx!42)))))))) | (~(nat_succeeds(Xx!42) | (~((Xx!42 = |'0'|) | (~![Xx2: $i] : ((~nat_succeeds(Xx2)) | (~(Xx!42 = s(Xx2)))))))))))),
% 0.38/0.60 inference(modus_ponens,[status(thm)],[55, 54])).
% 0.38/0.60 tff(57,plain,
% 0.38/0.60 (~((~((Xx!42 = |'0'|) | (~nat_succeeds(Xx!42)) | (~((~nat_succeeds(tptp_fun_Xx2_26(Xx!42))) | (~(Xx!42 = s(tptp_fun_Xx2_26(Xx!42)))))))) | (~(nat_succeeds(Xx!42) | (~((Xx!42 = |'0'|) | (~![Xx2: $i] : ((~nat_succeeds(Xx2)) | (~(Xx!42 = s(Xx2))))))))))),
% 0.38/0.60 inference(unit_resolution,[status(thm)],[56, 50])).
% 0.38/0.60 tff(58,plain,
% 0.38/0.60 (((~((Xx!42 = |'0'|) | (~nat_succeeds(Xx!42)) | (~((~nat_succeeds(tptp_fun_Xx2_26(Xx!42))) | (~(Xx!42 = s(tptp_fun_Xx2_26(Xx!42)))))))) | (~(nat_succeeds(Xx!42) | (~((Xx!42 = |'0'|) | (~![Xx2: $i] : ((~nat_succeeds(Xx2)) | (~(Xx!42 = s(Xx2)))))))))) | ((Xx!42 = |'0'|) | (~nat_succeeds(Xx!42)) | (~((~nat_succeeds(tptp_fun_Xx2_26(Xx!42))) | (~(Xx!42 = s(tptp_fun_Xx2_26(Xx!42)))))))),
% 0.38/0.60 inference(tautology,[status(thm)],[])).
% 0.38/0.60 tff(59,plain,
% 0.38/0.60 ((Xx!42 = |'0'|) | (~nat_succeeds(Xx!42)) | (~((~nat_succeeds(tptp_fun_Xx2_26(Xx!42))) | (~(Xx!42 = s(tptp_fun_Xx2_26(Xx!42))))))),
% 0.38/0.60 inference(unit_resolution,[status(thm)],[58, 57])).
% 0.38/0.60 tff(60,plain,
% 0.38/0.60 (~(Xx!42 = |'0'|)),
% 0.38/0.60 inference(and_elim,[status(thm)],[9])).
% 0.38/0.60 tff(61,plain,
% 0.38/0.60 ((~((Xx!42 = |'0'|) | (~nat_succeeds(Xx!42)) | (~((~nat_succeeds(tptp_fun_Xx2_26(Xx!42))) | (~(Xx!42 = s(tptp_fun_Xx2_26(Xx!42)))))))) | (Xx!42 = |'0'|) | (~nat_succeeds(Xx!42)) | (~((~nat_succeeds(tptp_fun_Xx2_26(Xx!42))) | (~(Xx!42 = s(tptp_fun_Xx2_26(Xx!42))))))),
% 0.38/0.60 inference(tautology,[status(thm)],[])).
% 0.38/0.60 tff(62,plain,
% 0.38/0.60 ((~((Xx!42 = |'0'|) | (~nat_succeeds(Xx!42)) | (~((~nat_succeeds(tptp_fun_Xx2_26(Xx!42))) | (~(Xx!42 = s(tptp_fun_Xx2_26(Xx!42)))))))) | (~((~nat_succeeds(tptp_fun_Xx2_26(Xx!42))) | (~(Xx!42 = s(tptp_fun_Xx2_26(Xx!42))))))),
% 0.38/0.60 inference(unit_resolution,[status(thm)],[61, 11, 60])).
% 0.38/0.60 tff(63,plain,
% 0.38/0.60 (~((~nat_succeeds(tptp_fun_Xx2_26(Xx!42))) | (~(Xx!42 = s(tptp_fun_Xx2_26(Xx!42)))))),
% 0.38/0.60 inference(unit_resolution,[status(thm)],[62, 59])).
% 0.38/0.60 tff(64,plain,
% 0.38/0.60 (((~nat_succeeds(tptp_fun_Xx2_26(Xx!42))) | (~(Xx!42 = s(tptp_fun_Xx2_26(Xx!42))))) | (Xx!42 = s(tptp_fun_Xx2_26(Xx!42)))),
% 0.38/0.60 inference(tautology,[status(thm)],[])).
% 0.38/0.60 tff(65,plain,
% 0.38/0.60 (Xx!42 = s(tptp_fun_Xx2_26(Xx!42))),
% 0.38/0.60 inference(unit_resolution,[status(thm)],[64, 63])).
% 0.38/0.60 tff(66,plain,
% 0.38/0.60 (s(tptp_fun_Xx2_26(Xx!42)) = Xx!42),
% 0.38/0.60 inference(symmetry,[status(thm)],[65])).
% 0.38/0.60 tff(67,plain,
% 0.38/0.60 (tptp_fun_____(Xz!40, s(tptp_fun_Xx2_26(Xx!42))) = tptp_fun_____(Xz!40, Xx!42)),
% 0.38/0.60 inference(monotonicity,[status(thm)],[66])).
% 0.38/0.60 tff(68,plain,
% 0.38/0.60 (((~nat_succeeds(tptp_fun_Xx2_26(Xx!42))) | (~(Xx!42 = s(tptp_fun_Xx2_26(Xx!42))))) | nat_succeeds(tptp_fun_Xx2_26(Xx!42))),
% 0.38/0.60 inference(tautology,[status(thm)],[])).
% 0.38/0.60 tff(69,plain,
% 0.38/0.60 (nat_succeeds(tptp_fun_Xx2_26(Xx!42))),
% 0.38/0.60 inference(unit_resolution,[status(thm)],[68, 63])).
% 0.38/0.60 tff(70,plain,
% 0.38/0.60 (^[Xy: $i, Xx: $i] : refl(((tptp_fun_____(tptp_fun_____(Xy, Xx), Xy) = tptp_fun_____(Xy, s(Xx))) | (~nat_succeeds(Xx)) | (~nat_succeeds(Xy))) <=> ((tptp_fun_____(tptp_fun_____(Xy, Xx), Xy) = tptp_fun_____(Xy, s(Xx))) | (~nat_succeeds(Xx)) | (~nat_succeeds(Xy))))),
% 0.38/0.60 inference(bind,[status(th)],[])).
% 0.38/0.60 tff(71,plain,
% 0.38/0.60 (![Xy: $i, Xx: $i] : ((tptp_fun_____(tptp_fun_____(Xy, Xx), Xy) = tptp_fun_____(Xy, s(Xx))) | (~nat_succeeds(Xx)) | (~nat_succeeds(Xy))) <=> ![Xy: $i, Xx: $i] : ((tptp_fun_____(tptp_fun_____(Xy, Xx), Xy) = tptp_fun_____(Xy, s(Xx))) | (~nat_succeeds(Xx)) | (~nat_succeeds(Xy)))),
% 0.38/0.60 inference(quant_intro,[status(thm)],[70])).
% 0.38/0.60 tff(72,plain,
% 0.38/0.60 (^[Xy: $i, Xx: $i] : trans(monotonicity(trans(monotonicity(rewrite((nat_succeeds(Xy) & nat_succeeds(Xx)) <=> (~((~nat_succeeds(Xx)) | (~nat_succeeds(Xy))))), ((~(nat_succeeds(Xy) & nat_succeeds(Xx))) <=> (~(~((~nat_succeeds(Xx)) | (~nat_succeeds(Xy))))))), rewrite((~(~((~nat_succeeds(Xx)) | (~nat_succeeds(Xy))))) <=> ((~nat_succeeds(Xx)) | (~nat_succeeds(Xy)))), ((~(nat_succeeds(Xy) & nat_succeeds(Xx))) <=> ((~nat_succeeds(Xx)) | (~nat_succeeds(Xy))))), (((~(nat_succeeds(Xy) & nat_succeeds(Xx))) | (tptp_fun_____(tptp_fun_____(Xy, Xx), Xy) = tptp_fun_____(Xy, s(Xx)))) <=> (((~nat_succeeds(Xx)) | (~nat_succeeds(Xy))) | (tptp_fun_____(tptp_fun_____(Xy, Xx), Xy) = tptp_fun_____(Xy, s(Xx)))))), rewrite((((~nat_succeeds(Xx)) | (~nat_succeeds(Xy))) | (tptp_fun_____(tptp_fun_____(Xy, Xx), Xy) = tptp_fun_____(Xy, s(Xx)))) <=> ((tptp_fun_____(tptp_fun_____(Xy, Xx), Xy) = tptp_fun_____(Xy, s(Xx))) | (~nat_succeeds(Xx)) | (~nat_succeeds(Xy)))), (((~(nat_succeeds(Xy) & nat_succeeds(Xx))) | (tptp_fun_____(tptp_fun_____(Xy, Xx), Xy) = tptp_fun_____(Xy, s(Xx)))) <=> ((tptp_fun_____(tptp_fun_____(Xy, Xx), Xy) = tptp_fun_____(Xy, s(Xx))) | (~nat_succeeds(Xx)) | (~nat_succeeds(Xy)))))),
% 0.38/0.60 inference(bind,[status(th)],[])).
% 0.38/0.60 tff(73,plain,
% 0.38/0.60 (![Xy: $i, Xx: $i] : ((~(nat_succeeds(Xy) & nat_succeeds(Xx))) | (tptp_fun_____(tptp_fun_____(Xy, Xx), Xy) = tptp_fun_____(Xy, s(Xx)))) <=> ![Xy: $i, Xx: $i] : ((tptp_fun_____(tptp_fun_____(Xy, Xx), Xy) = tptp_fun_____(Xy, s(Xx))) | (~nat_succeeds(Xx)) | (~nat_succeeds(Xy)))),
% 0.38/0.60 inference(quant_intro,[status(thm)],[72])).
% 0.38/0.60 tff(74,plain,
% 0.38/0.60 (![Xy: $i, Xx: $i] : ((~(nat_succeeds(Xy) & nat_succeeds(Xx))) | (tptp_fun_____(tptp_fun_____(Xy, Xx), Xy) = tptp_fun_____(Xy, s(Xx)))) <=> ![Xy: $i, Xx: $i] : ((~(nat_succeeds(Xy) & nat_succeeds(Xx))) | (tptp_fun_____(tptp_fun_____(Xy, Xx), Xy) = tptp_fun_____(Xy, s(Xx))))),
% 0.38/0.60 inference(rewrite,[status(thm)],[])).
% 0.38/0.60 tff(75,plain,
% 0.38/0.60 (^[Xy: $i, Xx: $i] : rewrite(((nat_succeeds(Xy) & nat_succeeds(Xx)) => (tptp_fun_____(tptp_fun_____(Xy, Xx), Xy) = tptp_fun_____(Xy, s(Xx)))) <=> ((~(nat_succeeds(Xy) & nat_succeeds(Xx))) | (tptp_fun_____(tptp_fun_____(Xy, Xx), Xy) = tptp_fun_____(Xy, s(Xx)))))),
% 0.38/0.60 inference(bind,[status(th)],[])).
% 0.38/0.60 tff(76,plain,
% 0.38/0.60 (![Xy: $i, Xx: $i] : ((nat_succeeds(Xy) & nat_succeeds(Xx)) => (tptp_fun_____(tptp_fun_____(Xy, Xx), Xy) = tptp_fun_____(Xy, s(Xx)))) <=> ![Xy: $i, Xx: $i] : ((~(nat_succeeds(Xy) & nat_succeeds(Xx))) | (tptp_fun_____(tptp_fun_____(Xy, Xx), Xy) = tptp_fun_____(Xy, s(Xx))))),
% 0.38/0.60 inference(quant_intro,[status(thm)],[75])).
% 0.38/0.60 tff(77,axiom,(![Xy: $i, Xx: $i] : ((nat_succeeds(Xy) & nat_succeeds(Xx)) => (tptp_fun_____(tptp_fun_____(Xy, Xx), Xy) = tptp_fun_____(Xy, s(Xx))))), file('/export/starexec/sandbox/benchmark/theBenchmark.p',''lemma-(times:successor)'')).
% 0.38/0.60 tff(78,plain,
% 0.38/0.60 (![Xy: $i, Xx: $i] : ((~(nat_succeeds(Xy) & nat_succeeds(Xx))) | (tptp_fun_____(tptp_fun_____(Xy, Xx), Xy) = tptp_fun_____(Xy, s(Xx))))),
% 0.38/0.60 inference(modus_ponens,[status(thm)],[77, 76])).
% 0.38/0.60 tff(79,plain,
% 0.38/0.60 (![Xy: $i, Xx: $i] : ((~(nat_succeeds(Xy) & nat_succeeds(Xx))) | (tptp_fun_____(tptp_fun_____(Xy, Xx), Xy) = tptp_fun_____(Xy, s(Xx))))),
% 0.38/0.60 inference(modus_ponens,[status(thm)],[78, 74])).
% 0.38/0.60 tff(80,plain,(
% 0.38/0.60 ![Xy: $i, Xx: $i] : ((~(nat_succeeds(Xy) & nat_succeeds(Xx))) | (tptp_fun_____(tptp_fun_____(Xy, Xx), Xy) = tptp_fun_____(Xy, s(Xx))))),
% 0.38/0.60 inference(skolemize,[status(sab)],[79])).
% 0.38/0.60 tff(81,plain,
% 0.38/0.60 (![Xy: $i, Xx: $i] : ((tptp_fun_____(tptp_fun_____(Xy, Xx), Xy) = tptp_fun_____(Xy, s(Xx))) | (~nat_succeeds(Xx)) | (~nat_succeeds(Xy)))),
% 0.38/0.60 inference(modus_ponens,[status(thm)],[80, 73])).
% 0.38/0.60 tff(82,plain,
% 0.38/0.60 (![Xy: $i, Xx: $i] : ((tptp_fun_____(tptp_fun_____(Xy, Xx), Xy) = tptp_fun_____(Xy, s(Xx))) | (~nat_succeeds(Xx)) | (~nat_succeeds(Xy)))),
% 0.38/0.60 inference(modus_ponens,[status(thm)],[81, 71])).
% 0.38/0.60 tff(83,plain,
% 0.38/0.60 (((~![Xy: $i, Xx: $i] : ((tptp_fun_____(tptp_fun_____(Xy, Xx), Xy) = tptp_fun_____(Xy, s(Xx))) | (~nat_succeeds(Xx)) | (~nat_succeeds(Xy)))) | ((~nat_succeeds(Xz!40)) | (~nat_succeeds(tptp_fun_Xx2_26(Xx!42))) | (tptp_fun_____(tptp_fun_____(Xz!40, tptp_fun_Xx2_26(Xx!42)), Xz!40) = tptp_fun_____(Xz!40, s(tptp_fun_Xx2_26(Xx!42)))))) <=> ((~![Xy: $i, Xx: $i] : ((tptp_fun_____(tptp_fun_____(Xy, Xx), Xy) = tptp_fun_____(Xy, s(Xx))) | (~nat_succeeds(Xx)) | (~nat_succeeds(Xy)))) | (~nat_succeeds(Xz!40)) | (~nat_succeeds(tptp_fun_Xx2_26(Xx!42))) | (tptp_fun_____(tptp_fun_____(Xz!40, tptp_fun_Xx2_26(Xx!42)), Xz!40) = tptp_fun_____(Xz!40, s(tptp_fun_Xx2_26(Xx!42)))))),
% 0.38/0.60 inference(rewrite,[status(thm)],[])).
% 0.38/0.60 tff(84,plain,
% 0.38/0.60 (((tptp_fun_____(tptp_fun_____(Xz!40, tptp_fun_Xx2_26(Xx!42)), Xz!40) = tptp_fun_____(Xz!40, s(tptp_fun_Xx2_26(Xx!42)))) | (~nat_succeeds(tptp_fun_Xx2_26(Xx!42))) | (~nat_succeeds(Xz!40))) <=> ((~nat_succeeds(Xz!40)) | (~nat_succeeds(tptp_fun_Xx2_26(Xx!42))) | (tptp_fun_____(tptp_fun_____(Xz!40, tptp_fun_Xx2_26(Xx!42)), Xz!40) = tptp_fun_____(Xz!40, s(tptp_fun_Xx2_26(Xx!42)))))),
% 0.38/0.60 inference(rewrite,[status(thm)],[])).
% 0.38/0.60 tff(85,plain,
% 0.38/0.60 (((~![Xy: $i, Xx: $i] : ((tptp_fun_____(tptp_fun_____(Xy, Xx), Xy) = tptp_fun_____(Xy, s(Xx))) | (~nat_succeeds(Xx)) | (~nat_succeeds(Xy)))) | ((tptp_fun_____(tptp_fun_____(Xz!40, tptp_fun_Xx2_26(Xx!42)), Xz!40) = tptp_fun_____(Xz!40, s(tptp_fun_Xx2_26(Xx!42)))) | (~nat_succeeds(tptp_fun_Xx2_26(Xx!42))) | (~nat_succeeds(Xz!40)))) <=> ((~![Xy: $i, Xx: $i] : ((tptp_fun_____(tptp_fun_____(Xy, Xx), Xy) = tptp_fun_____(Xy, s(Xx))) | (~nat_succeeds(Xx)) | (~nat_succeeds(Xy)))) | ((~nat_succeeds(Xz!40)) | (~nat_succeeds(tptp_fun_Xx2_26(Xx!42))) | (tptp_fun_____(tptp_fun_____(Xz!40, tptp_fun_Xx2_26(Xx!42)), Xz!40) = tptp_fun_____(Xz!40, s(tptp_fun_Xx2_26(Xx!42))))))),
% 0.38/0.60 inference(monotonicity,[status(thm)],[84])).
% 0.38/0.60 tff(86,plain,
% 0.38/0.60 (((~![Xy: $i, Xx: $i] : ((tptp_fun_____(tptp_fun_____(Xy, Xx), Xy) = tptp_fun_____(Xy, s(Xx))) | (~nat_succeeds(Xx)) | (~nat_succeeds(Xy)))) | ((tptp_fun_____(tptp_fun_____(Xz!40, tptp_fun_Xx2_26(Xx!42)), Xz!40) = tptp_fun_____(Xz!40, s(tptp_fun_Xx2_26(Xx!42)))) | (~nat_succeeds(tptp_fun_Xx2_26(Xx!42))) | (~nat_succeeds(Xz!40)))) <=> ((~![Xy: $i, Xx: $i] : ((tptp_fun_____(tptp_fun_____(Xy, Xx), Xy) = tptp_fun_____(Xy, s(Xx))) | (~nat_succeeds(Xx)) | (~nat_succeeds(Xy)))) | (~nat_succeeds(Xz!40)) | (~nat_succeeds(tptp_fun_Xx2_26(Xx!42))) | (tptp_fun_____(tptp_fun_____(Xz!40, tptp_fun_Xx2_26(Xx!42)), Xz!40) = tptp_fun_____(Xz!40, s(tptp_fun_Xx2_26(Xx!42)))))),
% 0.38/0.60 inference(transitivity,[status(thm)],[85, 83])).
% 0.38/0.60 tff(87,plain,
% 0.38/0.60 ((~![Xy: $i, Xx: $i] : ((tptp_fun_____(tptp_fun_____(Xy, Xx), Xy) = tptp_fun_____(Xy, s(Xx))) | (~nat_succeeds(Xx)) | (~nat_succeeds(Xy)))) | ((tptp_fun_____(tptp_fun_____(Xz!40, tptp_fun_Xx2_26(Xx!42)), Xz!40) = tptp_fun_____(Xz!40, s(tptp_fun_Xx2_26(Xx!42)))) | (~nat_succeeds(tptp_fun_Xx2_26(Xx!42))) | (~nat_succeeds(Xz!40)))),
% 0.38/0.60 inference(quant_inst,[status(thm)],[])).
% 0.38/0.60 tff(88,plain,
% 0.38/0.60 ((~![Xy: $i, Xx: $i] : ((tptp_fun_____(tptp_fun_____(Xy, Xx), Xy) = tptp_fun_____(Xy, s(Xx))) | (~nat_succeeds(Xx)) | (~nat_succeeds(Xy)))) | (~nat_succeeds(Xz!40)) | (~nat_succeeds(tptp_fun_Xx2_26(Xx!42))) | (tptp_fun_____(tptp_fun_____(Xz!40, tptp_fun_Xx2_26(Xx!42)), Xz!40) = tptp_fun_____(Xz!40, s(tptp_fun_Xx2_26(Xx!42))))),
% 0.38/0.60 inference(modus_ponens,[status(thm)],[87, 86])).
% 0.38/0.60 tff(89,plain,
% 0.38/0.60 (tptp_fun_____(tptp_fun_____(Xz!40, tptp_fun_Xx2_26(Xx!42)), Xz!40) = tptp_fun_____(Xz!40, s(tptp_fun_Xx2_26(Xx!42)))),
% 0.38/0.60 inference(unit_resolution,[status(thm)],[88, 82, 10, 69])).
% 0.38/0.60 tff(90,plain,
% 0.38/0.60 (tptp_fun_____(tptp_fun_____(Xz!40, tptp_fun_Xx2_26(Xx!42)), Xz!40) = tptp_fun_____(Xx!42, Xz!40)),
% 0.38/0.60 inference(transitivity,[status(thm)],[89, 67, 31])).
% 0.38/0.60 tff(91,plain,
% 0.38/0.60 (tptp_fun_____succeeds_(Xy!41, Xz!40)),
% 0.38/0.60 inference(and_elim,[status(thm)],[9])).
% 0.38/0.60 tff(92,plain,
% 0.38/0.60 (^[Xx: $i, Xy: $i] : refl((nat_succeeds(Xx) | (~tptp_fun_____succeeds_(Xx, Xy))) <=> (nat_succeeds(Xx) | (~tptp_fun_____succeeds_(Xx, Xy))))),
% 0.38/0.60 inference(bind,[status(th)],[])).
% 0.38/0.60 tff(93,plain,
% 0.38/0.60 (![Xx: $i, Xy: $i] : (nat_succeeds(Xx) | (~tptp_fun_____succeeds_(Xx, Xy))) <=> ![Xx: $i, Xy: $i] : (nat_succeeds(Xx) | (~tptp_fun_____succeeds_(Xx, Xy)))),
% 0.38/0.60 inference(quant_intro,[status(thm)],[92])).
% 0.38/0.60 tff(94,plain,
% 0.38/0.60 (![Xx: $i, Xy: $i] : (nat_succeeds(Xx) | (~tptp_fun_____succeeds_(Xx, Xy))) <=> ![Xx: $i, Xy: $i] : (nat_succeeds(Xx) | (~tptp_fun_____succeeds_(Xx, Xy)))),
% 0.38/0.60 inference(rewrite,[status(thm)],[])).
% 0.38/0.60 tff(95,plain,
% 0.38/0.60 (^[Xx: $i, Xy: $i] : rewrite((tptp_fun_____succeeds_(Xx, Xy) => nat_succeeds(Xx)) <=> (nat_succeeds(Xx) | (~tptp_fun_____succeeds_(Xx, Xy))))),
% 0.38/0.60 inference(bind,[status(th)],[])).
% 0.38/0.60 tff(96,plain,
% 0.38/0.60 (![Xx: $i, Xy: $i] : (tptp_fun_____succeeds_(Xx, Xy) => nat_succeeds(Xx)) <=> ![Xx: $i, Xy: $i] : (nat_succeeds(Xx) | (~tptp_fun_____succeeds_(Xx, Xy)))),
% 0.38/0.60 inference(quant_intro,[status(thm)],[95])).
% 0.38/0.60 tff(97,axiom,(![Xx: $i, Xy: $i] : (tptp_fun_____succeeds_(Xx, Xy) => nat_succeeds(Xx))), file('/export/starexec/sandbox/benchmark/theBenchmark.p',''lemma-(less:types)'')).
% 0.38/0.60 tff(98,plain,
% 0.38/0.60 (![Xx: $i, Xy: $i] : (nat_succeeds(Xx) | (~tptp_fun_____succeeds_(Xx, Xy)))),
% 0.38/0.60 inference(modus_ponens,[status(thm)],[97, 96])).
% 0.38/0.60 tff(99,plain,
% 0.38/0.60 (![Xx: $i, Xy: $i] : (nat_succeeds(Xx) | (~tptp_fun_____succeeds_(Xx, Xy)))),
% 0.38/0.60 inference(modus_ponens,[status(thm)],[98, 94])).
% 0.38/0.60 tff(100,plain,(
% 0.38/0.60 ![Xx: $i, Xy: $i] : (nat_succeeds(Xx) | (~tptp_fun_____succeeds_(Xx, Xy)))),
% 0.38/0.60 inference(skolemize,[status(sab)],[99])).
% 0.38/0.60 tff(101,plain,
% 0.38/0.60 (![Xx: $i, Xy: $i] : (nat_succeeds(Xx) | (~tptp_fun_____succeeds_(Xx, Xy)))),
% 0.38/0.60 inference(modus_ponens,[status(thm)],[100, 93])).
% 0.38/0.60 tff(102,plain,
% 0.38/0.60 (((~![Xx: $i, Xy: $i] : (nat_succeeds(Xx) | (~tptp_fun_____succeeds_(Xx, Xy)))) | (nat_succeeds(Xy!41) | (~tptp_fun_____succeeds_(Xy!41, Xz!40)))) <=> ((~![Xx: $i, Xy: $i] : (nat_succeeds(Xx) | (~tptp_fun_____succeeds_(Xx, Xy)))) | nat_succeeds(Xy!41) | (~tptp_fun_____succeeds_(Xy!41, Xz!40)))),
% 0.38/0.60 inference(rewrite,[status(thm)],[])).
% 0.38/0.60 tff(103,plain,
% 0.38/0.60 ((~![Xx: $i, Xy: $i] : (nat_succeeds(Xx) | (~tptp_fun_____succeeds_(Xx, Xy)))) | (nat_succeeds(Xy!41) | (~tptp_fun_____succeeds_(Xy!41, Xz!40)))),
% 0.38/0.60 inference(quant_inst,[status(thm)],[])).
% 0.38/0.60 tff(104,plain,
% 0.38/0.60 ((~![Xx: $i, Xy: $i] : (nat_succeeds(Xx) | (~tptp_fun_____succeeds_(Xx, Xy)))) | nat_succeeds(Xy!41) | (~tptp_fun_____succeeds_(Xy!41, Xz!40))),
% 0.38/0.60 inference(modus_ponens,[status(thm)],[103, 102])).
% 0.38/0.60 tff(105,plain,
% 0.38/0.60 (nat_succeeds(Xy!41)),
% 0.38/0.60 inference(unit_resolution,[status(thm)],[104, 101, 91])).
% 0.38/0.60 tff(106,plain,
% 0.38/0.60 (((~![Xx: $i, Xy: $i] : ((tptp_fun_____(Xx, Xy) = tptp_fun_____(Xy, Xx)) | (~nat_succeeds(Xy)) | (~nat_succeeds(Xx)))) | ((~nat_succeeds(Xx!42)) | (~nat_succeeds(Xy!41)) | (tptp_fun_____(Xy!41, Xx!42) = tptp_fun_____(Xx!42, Xy!41)))) <=> ((~![Xx: $i, Xy: $i] : ((tptp_fun_____(Xx, Xy) = tptp_fun_____(Xy, Xx)) | (~nat_succeeds(Xy)) | (~nat_succeeds(Xx)))) | (~nat_succeeds(Xx!42)) | (~nat_succeeds(Xy!41)) | (tptp_fun_____(Xy!41, Xx!42) = tptp_fun_____(Xx!42, Xy!41)))),
% 0.38/0.60 inference(rewrite,[status(thm)],[])).
% 0.38/0.60 tff(107,plain,
% 0.38/0.60 (((tptp_fun_____(Xy!41, Xx!42) = tptp_fun_____(Xx!42, Xy!41)) | (~nat_succeeds(Xx!42)) | (~nat_succeeds(Xy!41))) <=> ((~nat_succeeds(Xx!42)) | (~nat_succeeds(Xy!41)) | (tptp_fun_____(Xy!41, Xx!42) = tptp_fun_____(Xx!42, Xy!41)))),
% 0.38/0.60 inference(rewrite,[status(thm)],[])).
% 0.38/0.60 tff(108,plain,
% 0.38/0.60 (((~![Xx: $i, Xy: $i] : ((tptp_fun_____(Xx, Xy) = tptp_fun_____(Xy, Xx)) | (~nat_succeeds(Xy)) | (~nat_succeeds(Xx)))) | ((tptp_fun_____(Xy!41, Xx!42) = tptp_fun_____(Xx!42, Xy!41)) | (~nat_succeeds(Xx!42)) | (~nat_succeeds(Xy!41)))) <=> ((~![Xx: $i, Xy: $i] : ((tptp_fun_____(Xx, Xy) = tptp_fun_____(Xy, Xx)) | (~nat_succeeds(Xy)) | (~nat_succeeds(Xx)))) | ((~nat_succeeds(Xx!42)) | (~nat_succeeds(Xy!41)) | (tptp_fun_____(Xy!41, Xx!42) = tptp_fun_____(Xx!42, Xy!41))))),
% 0.38/0.60 inference(monotonicity,[status(thm)],[107])).
% 0.38/0.60 tff(109,plain,
% 0.38/0.60 (((~![Xx: $i, Xy: $i] : ((tptp_fun_____(Xx, Xy) = tptp_fun_____(Xy, Xx)) | (~nat_succeeds(Xy)) | (~nat_succeeds(Xx)))) | ((tptp_fun_____(Xy!41, Xx!42) = tptp_fun_____(Xx!42, Xy!41)) | (~nat_succeeds(Xx!42)) | (~nat_succeeds(Xy!41)))) <=> ((~![Xx: $i, Xy: $i] : ((tptp_fun_____(Xx, Xy) = tptp_fun_____(Xy, Xx)) | (~nat_succeeds(Xy)) | (~nat_succeeds(Xx)))) | (~nat_succeeds(Xx!42)) | (~nat_succeeds(Xy!41)) | (tptp_fun_____(Xy!41, Xx!42) = tptp_fun_____(Xx!42, Xy!41)))),
% 0.38/0.60 inference(transitivity,[status(thm)],[108, 106])).
% 0.38/0.60 tff(110,plain,
% 0.38/0.60 ((~![Xx: $i, Xy: $i] : ((tptp_fun_____(Xx, Xy) = tptp_fun_____(Xy, Xx)) | (~nat_succeeds(Xy)) | (~nat_succeeds(Xx)))) | ((tptp_fun_____(Xy!41, Xx!42) = tptp_fun_____(Xx!42, Xy!41)) | (~nat_succeeds(Xx!42)) | (~nat_succeeds(Xy!41)))),
% 0.38/0.60 inference(quant_inst,[status(thm)],[])).
% 0.38/0.60 tff(111,plain,
% 0.38/0.60 ((~![Xx: $i, Xy: $i] : ((tptp_fun_____(Xx, Xy) = tptp_fun_____(Xy, Xx)) | (~nat_succeeds(Xy)) | (~nat_succeeds(Xx)))) | (~nat_succeeds(Xx!42)) | (~nat_succeeds(Xy!41)) | (tptp_fun_____(Xy!41, Xx!42) = tptp_fun_____(Xx!42, Xy!41))),
% 0.38/0.60 inference(modus_ponens,[status(thm)],[110, 109])).
% 0.38/0.60 tff(112,plain,
% 0.38/0.60 (tptp_fun_____(Xy!41, Xx!42) = tptp_fun_____(Xx!42, Xy!41)),
% 0.38/0.60 inference(unit_resolution,[status(thm)],[111, 24, 11, 105])).
% 0.38/0.60 tff(113,plain,
% 0.38/0.60 (tptp_fun_____(Xy!41, s(tptp_fun_Xx2_26(Xx!42))) = tptp_fun_____(Xy!41, Xx!42)),
% 0.38/0.60 inference(monotonicity,[status(thm)],[66])).
% 0.38/0.60 tff(114,plain,
% 0.38/0.60 (((~![Xy: $i, Xx: $i] : ((tptp_fun_____(tptp_fun_____(Xy, Xx), Xy) = tptp_fun_____(Xy, s(Xx))) | (~nat_succeeds(Xx)) | (~nat_succeeds(Xy)))) | ((~nat_succeeds(tptp_fun_Xx2_26(Xx!42))) | (~nat_succeeds(Xy!41)) | (tptp_fun_____(tptp_fun_____(Xy!41, tptp_fun_Xx2_26(Xx!42)), Xy!41) = tptp_fun_____(Xy!41, s(tptp_fun_Xx2_26(Xx!42)))))) <=> ((~![Xy: $i, Xx: $i] : ((tptp_fun_____(tptp_fun_____(Xy, Xx), Xy) = tptp_fun_____(Xy, s(Xx))) | (~nat_succeeds(Xx)) | (~nat_succeeds(Xy)))) | (~nat_succeeds(tptp_fun_Xx2_26(Xx!42))) | (~nat_succeeds(Xy!41)) | (tptp_fun_____(tptp_fun_____(Xy!41, tptp_fun_Xx2_26(Xx!42)), Xy!41) = tptp_fun_____(Xy!41, s(tptp_fun_Xx2_26(Xx!42)))))),
% 0.38/0.60 inference(rewrite,[status(thm)],[])).
% 0.38/0.60 tff(115,plain,
% 0.38/0.60 (((tptp_fun_____(tptp_fun_____(Xy!41, tptp_fun_Xx2_26(Xx!42)), Xy!41) = tptp_fun_____(Xy!41, s(tptp_fun_Xx2_26(Xx!42)))) | (~nat_succeeds(tptp_fun_Xx2_26(Xx!42))) | (~nat_succeeds(Xy!41))) <=> ((~nat_succeeds(tptp_fun_Xx2_26(Xx!42))) | (~nat_succeeds(Xy!41)) | (tptp_fun_____(tptp_fun_____(Xy!41, tptp_fun_Xx2_26(Xx!42)), Xy!41) = tptp_fun_____(Xy!41, s(tptp_fun_Xx2_26(Xx!42)))))),
% 0.38/0.60 inference(rewrite,[status(thm)],[])).
% 0.38/0.60 tff(116,plain,
% 0.38/0.60 (((~![Xy: $i, Xx: $i] : ((tptp_fun_____(tptp_fun_____(Xy, Xx), Xy) = tptp_fun_____(Xy, s(Xx))) | (~nat_succeeds(Xx)) | (~nat_succeeds(Xy)))) | ((tptp_fun_____(tptp_fun_____(Xy!41, tptp_fun_Xx2_26(Xx!42)), Xy!41) = tptp_fun_____(Xy!41, s(tptp_fun_Xx2_26(Xx!42)))) | (~nat_succeeds(tptp_fun_Xx2_26(Xx!42))) | (~nat_succeeds(Xy!41)))) <=> ((~![Xy: $i, Xx: $i] : ((tptp_fun_____(tptp_fun_____(Xy, Xx), Xy) = tptp_fun_____(Xy, s(Xx))) | (~nat_succeeds(Xx)) | (~nat_succeeds(Xy)))) | ((~nat_succeeds(tptp_fun_Xx2_26(Xx!42))) | (~nat_succeeds(Xy!41)) | (tptp_fun_____(tptp_fun_____(Xy!41, tptp_fun_Xx2_26(Xx!42)), Xy!41) = tptp_fun_____(Xy!41, s(tptp_fun_Xx2_26(Xx!42))))))),
% 0.38/0.60 inference(monotonicity,[status(thm)],[115])).
% 0.38/0.60 tff(117,plain,
% 0.38/0.60 (((~![Xy: $i, Xx: $i] : ((tptp_fun_____(tptp_fun_____(Xy, Xx), Xy) = tptp_fun_____(Xy, s(Xx))) | (~nat_succeeds(Xx)) | (~nat_succeeds(Xy)))) | ((tptp_fun_____(tptp_fun_____(Xy!41, tptp_fun_Xx2_26(Xx!42)), Xy!41) = tptp_fun_____(Xy!41, s(tptp_fun_Xx2_26(Xx!42)))) | (~nat_succeeds(tptp_fun_Xx2_26(Xx!42))) | (~nat_succeeds(Xy!41)))) <=> ((~![Xy: $i, Xx: $i] : ((tptp_fun_____(tptp_fun_____(Xy, Xx), Xy) = tptp_fun_____(Xy, s(Xx))) | (~nat_succeeds(Xx)) | (~nat_succeeds(Xy)))) | (~nat_succeeds(tptp_fun_Xx2_26(Xx!42))) | (~nat_succeeds(Xy!41)) | (tptp_fun_____(tptp_fun_____(Xy!41, tptp_fun_Xx2_26(Xx!42)), Xy!41) = tptp_fun_____(Xy!41, s(tptp_fun_Xx2_26(Xx!42)))))),
% 0.38/0.60 inference(transitivity,[status(thm)],[116, 114])).
% 0.38/0.60 tff(118,plain,
% 0.38/0.60 ((~![Xy: $i, Xx: $i] : ((tptp_fun_____(tptp_fun_____(Xy, Xx), Xy) = tptp_fun_____(Xy, s(Xx))) | (~nat_succeeds(Xx)) | (~nat_succeeds(Xy)))) | ((tptp_fun_____(tptp_fun_____(Xy!41, tptp_fun_Xx2_26(Xx!42)), Xy!41) = tptp_fun_____(Xy!41, s(tptp_fun_Xx2_26(Xx!42)))) | (~nat_succeeds(tptp_fun_Xx2_26(Xx!42))) | (~nat_succeeds(Xy!41)))),
% 0.38/0.60 inference(quant_inst,[status(thm)],[])).
% 0.38/0.60 tff(119,plain,
% 0.38/0.60 ((~![Xy: $i, Xx: $i] : ((tptp_fun_____(tptp_fun_____(Xy, Xx), Xy) = tptp_fun_____(Xy, s(Xx))) | (~nat_succeeds(Xx)) | (~nat_succeeds(Xy)))) | (~nat_succeeds(tptp_fun_Xx2_26(Xx!42))) | (~nat_succeeds(Xy!41)) | (tptp_fun_____(tptp_fun_____(Xy!41, tptp_fun_Xx2_26(Xx!42)), Xy!41) = tptp_fun_____(Xy!41, s(tptp_fun_Xx2_26(Xx!42))))),
% 0.38/0.60 inference(modus_ponens,[status(thm)],[118, 117])).
% 0.38/0.60 tff(120,plain,
% 0.38/0.60 (tptp_fun_____(tptp_fun_____(Xy!41, tptp_fun_Xx2_26(Xx!42)), Xy!41) = tptp_fun_____(Xy!41, s(tptp_fun_Xx2_26(Xx!42)))),
% 0.38/0.60 inference(unit_resolution,[status(thm)],[119, 82, 105, 69])).
% 0.38/0.60 tff(121,plain,
% 0.38/0.60 (tptp_fun_____(tptp_fun_____(Xy!41, tptp_fun_Xx2_26(Xx!42)), Xy!41) = tptp_fun_____(Xx!42, Xy!41)),
% 0.38/0.60 inference(transitivity,[status(thm)],[120, 113, 112])).
% 0.38/0.60 tff(122,plain,
% 0.38/0.60 (tptp_fun_____succeeds_(tptp_fun_____(tptp_fun_____(Xy!41, tptp_fun_Xx2_26(Xx!42)), Xy!41), tptp_fun_____(tptp_fun_____(Xz!40, tptp_fun_Xx2_26(Xx!42)), Xz!40)) <=> tptp_fun_____succeeds_(tptp_fun_____(Xx!42, Xy!41), tptp_fun_____(Xx!42, Xz!40))),
% 0.38/0.60 inference(monotonicity,[status(thm)],[121, 90])).
% 0.38/0.60 tff(123,plain,
% 0.38/0.60 (tptp_fun_____succeeds_(tptp_fun_____(Xx!42, Xy!41), tptp_fun_____(Xx!42, Xz!40)) <=> tptp_fun_____succeeds_(tptp_fun_____(tptp_fun_____(Xy!41, tptp_fun_Xx2_26(Xx!42)), Xy!41), tptp_fun_____(tptp_fun_____(Xz!40, tptp_fun_Xx2_26(Xx!42)), Xz!40))),
% 0.38/0.60 inference(symmetry,[status(thm)],[122])).
% 0.38/0.60 tff(124,plain,
% 0.38/0.60 ((~tptp_fun_____succeeds_(tptp_fun_____(Xx!42, Xy!41), tptp_fun_____(Xx!42, Xz!40))) <=> (~tptp_fun_____succeeds_(tptp_fun_____(tptp_fun_____(Xy!41, tptp_fun_Xx2_26(Xx!42)), Xy!41), tptp_fun_____(tptp_fun_____(Xz!40, tptp_fun_Xx2_26(Xx!42)), Xz!40)))),
% 0.38/0.60 inference(monotonicity,[status(thm)],[123])).
% 0.38/0.60 tff(125,plain,
% 0.38/0.60 (~tptp_fun_____succeeds_(tptp_fun_____(Xx!42, Xy!41), tptp_fun_____(Xx!42, Xz!40))),
% 0.38/0.60 inference(or_elim,[status(thm)],[8])).
% 0.38/0.60 tff(126,plain,
% 0.38/0.60 (~tptp_fun_____succeeds_(tptp_fun_____(tptp_fun_____(Xy!41, tptp_fun_Xx2_26(Xx!42)), Xy!41), tptp_fun_____(tptp_fun_____(Xz!40, tptp_fun_Xx2_26(Xx!42)), Xz!40))),
% 0.38/0.60 inference(modus_ponens,[status(thm)],[125, 124])).
% 0.38/0.60 tff(127,plain,
% 0.38/0.60 (^[Xx: $i, Xy: $i] : refl(((~tptp_fun_____succeeds_(Xx, Xy)) | tptp_fun______succeeds_(Xx, Xy)) <=> ((~tptp_fun_____succeeds_(Xx, Xy)) | tptp_fun______succeeds_(Xx, Xy)))),
% 0.38/0.60 inference(bind,[status(th)],[])).
% 0.38/0.60 tff(128,plain,
% 0.38/0.60 (![Xx: $i, Xy: $i] : ((~tptp_fun_____succeeds_(Xx, Xy)) | tptp_fun______succeeds_(Xx, Xy)) <=> ![Xx: $i, Xy: $i] : ((~tptp_fun_____succeeds_(Xx, Xy)) | tptp_fun______succeeds_(Xx, Xy))),
% 0.38/0.60 inference(quant_intro,[status(thm)],[127])).
% 0.38/0.60 tff(129,plain,
% 0.38/0.60 (![Xx: $i, Xy: $i] : ((~tptp_fun_____succeeds_(Xx, Xy)) | tptp_fun______succeeds_(Xx, Xy)) <=> ![Xx: $i, Xy: $i] : ((~tptp_fun_____succeeds_(Xx, Xy)) | tptp_fun______succeeds_(Xx, Xy))),
% 0.38/0.60 inference(rewrite,[status(thm)],[])).
% 0.38/0.60 tff(130,plain,
% 0.38/0.60 (^[Xx: $i, Xy: $i] : rewrite((tptp_fun_____succeeds_(Xx, Xy) => tptp_fun______succeeds_(Xx, Xy)) <=> ((~tptp_fun_____succeeds_(Xx, Xy)) | tptp_fun______succeeds_(Xx, Xy)))),
% 0.38/0.60 inference(bind,[status(th)],[])).
% 0.38/0.60 tff(131,plain,
% 0.38/0.60 (![Xx: $i, Xy: $i] : (tptp_fun_____succeeds_(Xx, Xy) => tptp_fun______succeeds_(Xx, Xy)) <=> ![Xx: $i, Xy: $i] : ((~tptp_fun_____succeeds_(Xx, Xy)) | tptp_fun______succeeds_(Xx, Xy))),
% 0.38/0.60 inference(quant_intro,[status(thm)],[130])).
% 0.38/0.60 tff(132,axiom,(![Xx: $i, Xy: $i] : (tptp_fun_____succeeds_(Xx, Xy) => tptp_fun______succeeds_(Xx, Xy))), file('/export/starexec/sandbox/benchmark/theBenchmark.p',''lemma-(less:leq)'')).
% 0.38/0.60 tff(133,plain,
% 0.38/0.60 (![Xx: $i, Xy: $i] : ((~tptp_fun_____succeeds_(Xx, Xy)) | tptp_fun______succeeds_(Xx, Xy))),
% 0.38/0.60 inference(modus_ponens,[status(thm)],[132, 131])).
% 0.38/0.60 tff(134,plain,
% 0.38/0.60 (![Xx: $i, Xy: $i] : ((~tptp_fun_____succeeds_(Xx, Xy)) | tptp_fun______succeeds_(Xx, Xy))),
% 0.38/0.60 inference(modus_ponens,[status(thm)],[133, 129])).
% 0.38/0.60 tff(135,plain,(
% 0.38/0.60 ![Xx: $i, Xy: $i] : ((~tptp_fun_____succeeds_(Xx, Xy)) | tptp_fun______succeeds_(Xx, Xy))),
% 0.38/0.60 inference(skolemize,[status(sab)],[134])).
% 0.38/0.60 tff(136,plain,
% 0.38/0.60 (![Xx: $i, Xy: $i] : ((~tptp_fun_____succeeds_(Xx, Xy)) | tptp_fun______succeeds_(Xx, Xy))),
% 0.38/0.60 inference(modus_ponens,[status(thm)],[135, 128])).
% 0.38/0.60 tff(137,plain,
% 0.38/0.60 (((~![Xx: $i, Xy: $i] : ((~tptp_fun_____succeeds_(Xx, Xy)) | tptp_fun______succeeds_(Xx, Xy))) | ((~tptp_fun_____succeeds_(Xy!41, Xz!40)) | tptp_fun______succeeds_(Xy!41, Xz!40))) <=> ((~![Xx: $i, Xy: $i] : ((~tptp_fun_____succeeds_(Xx, Xy)) | tptp_fun______succeeds_(Xx, Xy))) | (~tptp_fun_____succeeds_(Xy!41, Xz!40)) | tptp_fun______succeeds_(Xy!41, Xz!40))),
% 0.38/0.60 inference(rewrite,[status(thm)],[])).
% 0.38/0.60 tff(138,plain,
% 0.38/0.60 ((~![Xx: $i, Xy: $i] : ((~tptp_fun_____succeeds_(Xx, Xy)) | tptp_fun______succeeds_(Xx, Xy))) | ((~tptp_fun_____succeeds_(Xy!41, Xz!40)) | tptp_fun______succeeds_(Xy!41, Xz!40))),
% 0.38/0.60 inference(quant_inst,[status(thm)],[])).
% 0.38/0.60 tff(139,plain,
% 0.38/0.60 ((~![Xx: $i, Xy: $i] : ((~tptp_fun_____succeeds_(Xx, Xy)) | tptp_fun______succeeds_(Xx, Xy))) | (~tptp_fun_____succeeds_(Xy!41, Xz!40)) | tptp_fun______succeeds_(Xy!41, Xz!40)),
% 0.38/0.60 inference(modus_ponens,[status(thm)],[138, 137])).
% 0.38/0.60 tff(140,plain,
% 0.38/0.60 (tptp_fun______succeeds_(Xy!41, Xz!40)),
% 0.38/0.60 inference(unit_resolution,[status(thm)],[139, 136, 91])).
% 0.38/0.60 tff(141,plain,
% 0.38/0.60 (^[Xx: $i, Xy: $i, Xz: $i] : refl((tptp_fun______succeeds_(tptp_fun_____(Xx, Xz), tptp_fun_____(Xy, Xz)) | (~nat_succeeds(Xz)) | (~nat_succeeds(Xy)) | (~tptp_fun______succeeds_(Xx, Xy))) <=> (tptp_fun______succeeds_(tptp_fun_____(Xx, Xz), tptp_fun_____(Xy, Xz)) | (~nat_succeeds(Xz)) | (~nat_succeeds(Xy)) | (~tptp_fun______succeeds_(Xx, Xy))))),
% 0.38/0.60 inference(bind,[status(th)],[])).
% 0.38/0.60 tff(142,plain,
% 0.38/0.60 (![Xx: $i, Xy: $i, Xz: $i] : (tptp_fun______succeeds_(tptp_fun_____(Xx, Xz), tptp_fun_____(Xy, Xz)) | (~nat_succeeds(Xz)) | (~nat_succeeds(Xy)) | (~tptp_fun______succeeds_(Xx, Xy))) <=> ![Xx: $i, Xy: $i, Xz: $i] : (tptp_fun______succeeds_(tptp_fun_____(Xx, Xz), tptp_fun_____(Xy, Xz)) | (~nat_succeeds(Xz)) | (~nat_succeeds(Xy)) | (~tptp_fun______succeeds_(Xx, Xy)))),
% 0.38/0.60 inference(quant_intro,[status(thm)],[141])).
% 0.38/0.60 tff(143,plain,
% 0.38/0.60 (^[Xx: $i, Xy: $i, Xz: $i] : trans(monotonicity(trans(monotonicity(rewrite((tptp_fun______succeeds_(Xx, Xy) & nat_succeeds(Xy) & nat_succeeds(Xz)) <=> (~((~nat_succeeds(Xz)) | (~nat_succeeds(Xy)) | (~tptp_fun______succeeds_(Xx, Xy))))), ((~(tptp_fun______succeeds_(Xx, Xy) & nat_succeeds(Xy) & nat_succeeds(Xz))) <=> (~(~((~nat_succeeds(Xz)) | (~nat_succeeds(Xy)) | (~tptp_fun______succeeds_(Xx, Xy))))))), rewrite((~(~((~nat_succeeds(Xz)) | (~nat_succeeds(Xy)) | (~tptp_fun______succeeds_(Xx, Xy))))) <=> ((~nat_succeeds(Xz)) | (~nat_succeeds(Xy)) | (~tptp_fun______succeeds_(Xx, Xy)))), ((~(tptp_fun______succeeds_(Xx, Xy) & nat_succeeds(Xy) & nat_succeeds(Xz))) <=> ((~nat_succeeds(Xz)) | (~nat_succeeds(Xy)) | (~tptp_fun______succeeds_(Xx, Xy))))), (((~(tptp_fun______succeeds_(Xx, Xy) & nat_succeeds(Xy) & nat_succeeds(Xz))) | tptp_fun______succeeds_(tptp_fun_____(Xx, Xz), tptp_fun_____(Xy, Xz))) <=> (((~nat_succeeds(Xz)) | (~nat_succeeds(Xy)) | (~tptp_fun______succeeds_(Xx, Xy))) | tptp_fun______succeeds_(tptp_fun_____(Xx, Xz), tptp_fun_____(Xy, Xz))))), rewrite((((~nat_succeeds(Xz)) | (~nat_succeeds(Xy)) | (~tptp_fun______succeeds_(Xx, Xy))) | tptp_fun______succeeds_(tptp_fun_____(Xx, Xz), tptp_fun_____(Xy, Xz))) <=> (tptp_fun______succeeds_(tptp_fun_____(Xx, Xz), tptp_fun_____(Xy, Xz)) | (~nat_succeeds(Xz)) | (~nat_succeeds(Xy)) | (~tptp_fun______succeeds_(Xx, Xy)))), (((~(tptp_fun______succeeds_(Xx, Xy) & nat_succeeds(Xy) & nat_succeeds(Xz))) | tptp_fun______succeeds_(tptp_fun_____(Xx, Xz), tptp_fun_____(Xy, Xz))) <=> (tptp_fun______succeeds_(tptp_fun_____(Xx, Xz), tptp_fun_____(Xy, Xz)) | (~nat_succeeds(Xz)) | (~nat_succeeds(Xy)) | (~tptp_fun______succeeds_(Xx, Xy)))))),
% 0.38/0.60 inference(bind,[status(th)],[])).
% 0.38/0.60 tff(144,plain,
% 0.38/0.60 (![Xx: $i, Xy: $i, Xz: $i] : ((~(tptp_fun______succeeds_(Xx, Xy) & nat_succeeds(Xy) & nat_succeeds(Xz))) | tptp_fun______succeeds_(tptp_fun_____(Xx, Xz), tptp_fun_____(Xy, Xz))) <=> ![Xx: $i, Xy: $i, Xz: $i] : (tptp_fun______succeeds_(tptp_fun_____(Xx, Xz), tptp_fun_____(Xy, Xz)) | (~nat_succeeds(Xz)) | (~nat_succeeds(Xy)) | (~tptp_fun______succeeds_(Xx, Xy)))),
% 0.38/0.60 inference(quant_intro,[status(thm)],[143])).
% 0.38/0.60 tff(145,plain,
% 0.38/0.60 (![Xx: $i, Xy: $i, Xz: $i] : ((~(tptp_fun______succeeds_(Xx, Xy) & nat_succeeds(Xy) & nat_succeeds(Xz))) | tptp_fun______succeeds_(tptp_fun_____(Xx, Xz), tptp_fun_____(Xy, Xz))) <=> ![Xx: $i, Xy: $i, Xz: $i] : ((~(tptp_fun______succeeds_(Xx, Xy) & nat_succeeds(Xy) & nat_succeeds(Xz))) | tptp_fun______succeeds_(tptp_fun_____(Xx, Xz), tptp_fun_____(Xy, Xz)))),
% 0.38/0.61 inference(rewrite,[status(thm)],[])).
% 0.38/0.61 tff(146,plain,
% 0.38/0.61 (^[Xx: $i, Xy: $i, Xz: $i] : trans(monotonicity(rewrite(((tptp_fun______succeeds_(Xx, Xy) & nat_succeeds(Xy)) & nat_succeeds(Xz)) <=> (tptp_fun______succeeds_(Xx, Xy) & nat_succeeds(Xy) & nat_succeeds(Xz))), ((((tptp_fun______succeeds_(Xx, Xy) & nat_succeeds(Xy)) & nat_succeeds(Xz)) => tptp_fun______succeeds_(tptp_fun_____(Xx, Xz), tptp_fun_____(Xy, Xz))) <=> ((tptp_fun______succeeds_(Xx, Xy) & nat_succeeds(Xy) & nat_succeeds(Xz)) => tptp_fun______succeeds_(tptp_fun_____(Xx, Xz), tptp_fun_____(Xy, Xz))))), rewrite(((tptp_fun______succeeds_(Xx, Xy) & nat_succeeds(Xy) & nat_succeeds(Xz)) => tptp_fun______succeeds_(tptp_fun_____(Xx, Xz), tptp_fun_____(Xy, Xz))) <=> ((~(tptp_fun______succeeds_(Xx, Xy) & nat_succeeds(Xy) & nat_succeeds(Xz))) | tptp_fun______succeeds_(tptp_fun_____(Xx, Xz), tptp_fun_____(Xy, Xz)))), ((((tptp_fun______succeeds_(Xx, Xy) & nat_succeeds(Xy)) & nat_succeeds(Xz)) => tptp_fun______succeeds_(tptp_fun_____(Xx, Xz), tptp_fun_____(Xy, Xz))) <=> ((~(tptp_fun______succeeds_(Xx, Xy) & nat_succeeds(Xy) & nat_succeeds(Xz))) | tptp_fun______succeeds_(tptp_fun_____(Xx, Xz), tptp_fun_____(Xy, Xz)))))),
% 0.38/0.61 inference(bind,[status(th)],[])).
% 0.38/0.61 tff(147,plain,
% 0.38/0.61 (![Xx: $i, Xy: $i, Xz: $i] : (((tptp_fun______succeeds_(Xx, Xy) & nat_succeeds(Xy)) & nat_succeeds(Xz)) => tptp_fun______succeeds_(tptp_fun_____(Xx, Xz), tptp_fun_____(Xy, Xz))) <=> ![Xx: $i, Xy: $i, Xz: $i] : ((~(tptp_fun______succeeds_(Xx, Xy) & nat_succeeds(Xy) & nat_succeeds(Xz))) | tptp_fun______succeeds_(tptp_fun_____(Xx, Xz), tptp_fun_____(Xy, Xz)))),
% 0.38/0.61 inference(quant_intro,[status(thm)],[146])).
% 0.38/0.61 tff(148,axiom,(![Xx: $i, Xy: $i, Xz: $i] : (((tptp_fun______succeeds_(Xx, Xy) & nat_succeeds(Xy)) & nat_succeeds(Xz)) => tptp_fun______succeeds_(tptp_fun_____(Xx, Xz), tptp_fun_____(Xy, Xz)))), file('/export/starexec/sandbox/benchmark/theBenchmark.p',''corollary-(times:leq:first)'')).
% 0.38/0.61 tff(149,plain,
% 0.38/0.61 (![Xx: $i, Xy: $i, Xz: $i] : ((~(tptp_fun______succeeds_(Xx, Xy) & nat_succeeds(Xy) & nat_succeeds(Xz))) | tptp_fun______succeeds_(tptp_fun_____(Xx, Xz), tptp_fun_____(Xy, Xz)))),
% 0.38/0.61 inference(modus_ponens,[status(thm)],[148, 147])).
% 0.38/0.61 tff(150,plain,
% 0.38/0.61 (![Xx: $i, Xy: $i, Xz: $i] : ((~(tptp_fun______succeeds_(Xx, Xy) & nat_succeeds(Xy) & nat_succeeds(Xz))) | tptp_fun______succeeds_(tptp_fun_____(Xx, Xz), tptp_fun_____(Xy, Xz)))),
% 0.38/0.61 inference(modus_ponens,[status(thm)],[149, 145])).
% 0.38/0.61 tff(151,plain,(
% 0.38/0.61 ![Xx: $i, Xy: $i, Xz: $i] : ((~(tptp_fun______succeeds_(Xx, Xy) & nat_succeeds(Xy) & nat_succeeds(Xz))) | tptp_fun______succeeds_(tptp_fun_____(Xx, Xz), tptp_fun_____(Xy, Xz)))),
% 0.38/0.61 inference(skolemize,[status(sab)],[150])).
% 0.38/0.61 tff(152,plain,
% 0.38/0.61 (![Xx: $i, Xy: $i, Xz: $i] : (tptp_fun______succeeds_(tptp_fun_____(Xx, Xz), tptp_fun_____(Xy, Xz)) | (~nat_succeeds(Xz)) | (~nat_succeeds(Xy)) | (~tptp_fun______succeeds_(Xx, Xy)))),
% 0.38/0.61 inference(modus_ponens,[status(thm)],[151, 144])).
% 0.38/0.61 tff(153,plain,
% 0.38/0.61 (![Xx: $i, Xy: $i, Xz: $i] : (tptp_fun______succeeds_(tptp_fun_____(Xx, Xz), tptp_fun_____(Xy, Xz)) | (~nat_succeeds(Xz)) | (~nat_succeeds(Xy)) | (~tptp_fun______succeeds_(Xx, Xy)))),
% 0.38/0.61 inference(modus_ponens,[status(thm)],[152, 142])).
% 0.38/0.61 tff(154,plain,
% 0.38/0.61 (((~![Xx: $i, Xy: $i, Xz: $i] : (tptp_fun______succeeds_(tptp_fun_____(Xx, Xz), tptp_fun_____(Xy, Xz)) | (~nat_succeeds(Xz)) | (~nat_succeeds(Xy)) | (~tptp_fun______succeeds_(Xx, Xy)))) | ((~nat_succeeds(Xz!40)) | (~nat_succeeds(tptp_fun_Xx2_26(Xx!42))) | (~tptp_fun______succeeds_(Xy!41, Xz!40)) | tptp_fun______succeeds_(tptp_fun_____(Xy!41, tptp_fun_Xx2_26(Xx!42)), tptp_fun_____(Xz!40, tptp_fun_Xx2_26(Xx!42))))) <=> ((~![Xx: $i, Xy: $i, Xz: $i] : (tptp_fun______succeeds_(tptp_fun_____(Xx, Xz), tptp_fun_____(Xy, Xz)) | (~nat_succeeds(Xz)) | (~nat_succeeds(Xy)) | (~tptp_fun______succeeds_(Xx, Xy)))) | (~nat_succeeds(Xz!40)) | (~nat_succeeds(tptp_fun_Xx2_26(Xx!42))) | (~tptp_fun______succeeds_(Xy!41, Xz!40)) | tptp_fun______succeeds_(tptp_fun_____(Xy!41, tptp_fun_Xx2_26(Xx!42)), tptp_fun_____(Xz!40, tptp_fun_Xx2_26(Xx!42))))),
% 0.38/0.61 inference(rewrite,[status(thm)],[])).
% 0.38/0.61 tff(155,plain,
% 0.38/0.61 ((tptp_fun______succeeds_(tptp_fun_____(Xy!41, tptp_fun_Xx2_26(Xx!42)), tptp_fun_____(Xz!40, tptp_fun_Xx2_26(Xx!42))) | (~nat_succeeds(tptp_fun_Xx2_26(Xx!42))) | (~nat_succeeds(Xz!40)) | (~tptp_fun______succeeds_(Xy!41, Xz!40))) <=> ((~nat_succeeds(Xz!40)) | (~nat_succeeds(tptp_fun_Xx2_26(Xx!42))) | (~tptp_fun______succeeds_(Xy!41, Xz!40)) | tptp_fun______succeeds_(tptp_fun_____(Xy!41, tptp_fun_Xx2_26(Xx!42)), tptp_fun_____(Xz!40, tptp_fun_Xx2_26(Xx!42))))),
% 0.38/0.61 inference(rewrite,[status(thm)],[])).
% 0.38/0.61 tff(156,plain,
% 0.38/0.61 (((~![Xx: $i, Xy: $i, Xz: $i] : (tptp_fun______succeeds_(tptp_fun_____(Xx, Xz), tptp_fun_____(Xy, Xz)) | (~nat_succeeds(Xz)) | (~nat_succeeds(Xy)) | (~tptp_fun______succeeds_(Xx, Xy)))) | (tptp_fun______succeeds_(tptp_fun_____(Xy!41, tptp_fun_Xx2_26(Xx!42)), tptp_fun_____(Xz!40, tptp_fun_Xx2_26(Xx!42))) | (~nat_succeeds(tptp_fun_Xx2_26(Xx!42))) | (~nat_succeeds(Xz!40)) | (~tptp_fun______succeeds_(Xy!41, Xz!40)))) <=> ((~![Xx: $i, Xy: $i, Xz: $i] : (tptp_fun______succeeds_(tptp_fun_____(Xx, Xz), tptp_fun_____(Xy, Xz)) | (~nat_succeeds(Xz)) | (~nat_succeeds(Xy)) | (~tptp_fun______succeeds_(Xx, Xy)))) | ((~nat_succeeds(Xz!40)) | (~nat_succeeds(tptp_fun_Xx2_26(Xx!42))) | (~tptp_fun______succeeds_(Xy!41, Xz!40)) | tptp_fun______succeeds_(tptp_fun_____(Xy!41, tptp_fun_Xx2_26(Xx!42)), tptp_fun_____(Xz!40, tptp_fun_Xx2_26(Xx!42)))))),
% 0.38/0.61 inference(monotonicity,[status(thm)],[155])).
% 0.38/0.61 tff(157,plain,
% 0.38/0.61 (((~![Xx: $i, Xy: $i, Xz: $i] : (tptp_fun______succeeds_(tptp_fun_____(Xx, Xz), tptp_fun_____(Xy, Xz)) | (~nat_succeeds(Xz)) | (~nat_succeeds(Xy)) | (~tptp_fun______succeeds_(Xx, Xy)))) | (tptp_fun______succeeds_(tptp_fun_____(Xy!41, tptp_fun_Xx2_26(Xx!42)), tptp_fun_____(Xz!40, tptp_fun_Xx2_26(Xx!42))) | (~nat_succeeds(tptp_fun_Xx2_26(Xx!42))) | (~nat_succeeds(Xz!40)) | (~tptp_fun______succeeds_(Xy!41, Xz!40)))) <=> ((~![Xx: $i, Xy: $i, Xz: $i] : (tptp_fun______succeeds_(tptp_fun_____(Xx, Xz), tptp_fun_____(Xy, Xz)) | (~nat_succeeds(Xz)) | (~nat_succeeds(Xy)) | (~tptp_fun______succeeds_(Xx, Xy)))) | (~nat_succeeds(Xz!40)) | (~nat_succeeds(tptp_fun_Xx2_26(Xx!42))) | (~tptp_fun______succeeds_(Xy!41, Xz!40)) | tptp_fun______succeeds_(tptp_fun_____(Xy!41, tptp_fun_Xx2_26(Xx!42)), tptp_fun_____(Xz!40, tptp_fun_Xx2_26(Xx!42))))),
% 0.38/0.61 inference(transitivity,[status(thm)],[156, 154])).
% 0.38/0.61 tff(158,plain,
% 0.38/0.61 ((~![Xx: $i, Xy: $i, Xz: $i] : (tptp_fun______succeeds_(tptp_fun_____(Xx, Xz), tptp_fun_____(Xy, Xz)) | (~nat_succeeds(Xz)) | (~nat_succeeds(Xy)) | (~tptp_fun______succeeds_(Xx, Xy)))) | (tptp_fun______succeeds_(tptp_fun_____(Xy!41, tptp_fun_Xx2_26(Xx!42)), tptp_fun_____(Xz!40, tptp_fun_Xx2_26(Xx!42))) | (~nat_succeeds(tptp_fun_Xx2_26(Xx!42))) | (~nat_succeeds(Xz!40)) | (~tptp_fun______succeeds_(Xy!41, Xz!40)))),
% 0.38/0.61 inference(quant_inst,[status(thm)],[])).
% 0.38/0.61 tff(159,plain,
% 0.38/0.61 ((~![Xx: $i, Xy: $i, Xz: $i] : (tptp_fun______succeeds_(tptp_fun_____(Xx, Xz), tptp_fun_____(Xy, Xz)) | (~nat_succeeds(Xz)) | (~nat_succeeds(Xy)) | (~tptp_fun______succeeds_(Xx, Xy)))) | (~nat_succeeds(Xz!40)) | (~nat_succeeds(tptp_fun_Xx2_26(Xx!42))) | (~tptp_fun______succeeds_(Xy!41, Xz!40)) | tptp_fun______succeeds_(tptp_fun_____(Xy!41, tptp_fun_Xx2_26(Xx!42)), tptp_fun_____(Xz!40, tptp_fun_Xx2_26(Xx!42)))),
% 0.38/0.61 inference(modus_ponens,[status(thm)],[158, 157])).
% 0.38/0.61 tff(160,plain,
% 0.38/0.61 (tptp_fun______succeeds_(tptp_fun_____(Xy!41, tptp_fun_Xx2_26(Xx!42)), tptp_fun_____(Xz!40, tptp_fun_Xx2_26(Xx!42)))),
% 0.38/0.61 inference(unit_resolution,[status(thm)],[159, 153, 10, 140, 69])).
% 0.38/0.61 tff(161,plain,
% 0.38/0.61 (^[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.38/0.61 inference(bind,[status(th)],[])).
% 0.38/0.61 tff(162,plain,
% 0.38/0.61 (![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.38/0.61 inference(quant_intro,[status(thm)],[161])).
% 0.38/0.61 tff(163,plain,
% 0.38/0.61 (^[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.38/0.61 inference(bind,[status(th)],[])).
% 0.38/0.61 tff(164,plain,
% 0.38/0.61 (![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.38/0.61 inference(quant_intro,[status(thm)],[163])).
% 0.38/0.61 tff(165,plain,
% 0.38/0.61 (![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.38/0.61 inference(rewrite,[status(thm)],[])).
% 0.38/0.61 tff(166,plain,
% 0.38/0.61 (^[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.38/0.61 inference(bind,[status(th)],[])).
% 0.38/0.61 tff(167,plain,
% 0.38/0.61 (![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.38/0.61 inference(quant_intro,[status(thm)],[166])).
% 0.38/0.61 tff(168,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-(times:types)'')).
% 0.38/0.61 tff(169,plain,
% 0.38/0.61 (![Xx: $i, Xy: $i] : (nat_succeeds(tptp_fun_____(Xx, Xy)) | (~(nat_succeeds(Xx) & nat_succeeds(Xy))))),
% 0.38/0.61 inference(modus_ponens,[status(thm)],[168, 167])).
% 0.38/0.61 tff(170,plain,
% 0.38/0.61 (![Xx: $i, Xy: $i] : (nat_succeeds(tptp_fun_____(Xx, Xy)) | (~(nat_succeeds(Xx) & nat_succeeds(Xy))))),
% 0.38/0.61 inference(modus_ponens,[status(thm)],[169, 165])).
% 0.38/0.61 tff(171,plain,(
% 0.38/0.61 ![Xx: $i, Xy: $i] : (nat_succeeds(tptp_fun_____(Xx, Xy)) | (~(nat_succeeds(Xx) & nat_succeeds(Xy))))),
% 0.38/0.61 inference(skolemize,[status(sab)],[170])).
% 0.38/0.61 tff(172,plain,
% 0.38/0.61 (![Xx: $i, Xy: $i] : (nat_succeeds(tptp_fun_____(Xx, Xy)) | (~nat_succeeds(Xy)) | (~nat_succeeds(Xx)))),
% 0.38/0.61 inference(modus_ponens,[status(thm)],[171, 164])).
% 0.38/0.61 tff(173,plain,
% 0.38/0.61 (![Xx: $i, Xy: $i] : (nat_succeeds(tptp_fun_____(Xx, Xy)) | (~nat_succeeds(Xy)) | (~nat_succeeds(Xx)))),
% 0.38/0.61 inference(modus_ponens,[status(thm)],[172, 162])).
% 0.38/0.61 tff(174,plain,
% 0.38/0.61 (((~![Xx: $i, Xy: $i] : (nat_succeeds(tptp_fun_____(Xx, Xy)) | (~nat_succeeds(Xy)) | (~nat_succeeds(Xx)))) | ((~nat_succeeds(Xz!40)) | (~nat_succeeds(tptp_fun_Xx2_26(Xx!42))) | nat_succeeds(tptp_fun_____(Xz!40, tptp_fun_Xx2_26(Xx!42))))) <=> ((~![Xx: $i, Xy: $i] : (nat_succeeds(tptp_fun_____(Xx, Xy)) | (~nat_succeeds(Xy)) | (~nat_succeeds(Xx)))) | (~nat_succeeds(Xz!40)) | (~nat_succeeds(tptp_fun_Xx2_26(Xx!42))) | nat_succeeds(tptp_fun_____(Xz!40, tptp_fun_Xx2_26(Xx!42))))),
% 0.38/0.61 inference(rewrite,[status(thm)],[])).
% 0.38/0.61 tff(175,plain,
% 0.38/0.61 ((nat_succeeds(tptp_fun_____(Xz!40, tptp_fun_Xx2_26(Xx!42))) | (~nat_succeeds(tptp_fun_Xx2_26(Xx!42))) | (~nat_succeeds(Xz!40))) <=> ((~nat_succeeds(Xz!40)) | (~nat_succeeds(tptp_fun_Xx2_26(Xx!42))) | nat_succeeds(tptp_fun_____(Xz!40, tptp_fun_Xx2_26(Xx!42))))),
% 0.38/0.61 inference(rewrite,[status(thm)],[])).
% 0.38/0.61 tff(176,plain,
% 0.38/0.61 (((~![Xx: $i, Xy: $i] : (nat_succeeds(tptp_fun_____(Xx, Xy)) | (~nat_succeeds(Xy)) | (~nat_succeeds(Xx)))) | (nat_succeeds(tptp_fun_____(Xz!40, tptp_fun_Xx2_26(Xx!42))) | (~nat_succeeds(tptp_fun_Xx2_26(Xx!42))) | (~nat_succeeds(Xz!40)))) <=> ((~![Xx: $i, Xy: $i] : (nat_succeeds(tptp_fun_____(Xx, Xy)) | (~nat_succeeds(Xy)) | (~nat_succeeds(Xx)))) | ((~nat_succeeds(Xz!40)) | (~nat_succeeds(tptp_fun_Xx2_26(Xx!42))) | nat_succeeds(tptp_fun_____(Xz!40, tptp_fun_Xx2_26(Xx!42)))))),
% 0.38/0.61 inference(monotonicity,[status(thm)],[175])).
% 0.38/0.61 tff(177,plain,
% 0.38/0.61 (((~![Xx: $i, Xy: $i] : (nat_succeeds(tptp_fun_____(Xx, Xy)) | (~nat_succeeds(Xy)) | (~nat_succeeds(Xx)))) | (nat_succeeds(tptp_fun_____(Xz!40, tptp_fun_Xx2_26(Xx!42))) | (~nat_succeeds(tptp_fun_Xx2_26(Xx!42))) | (~nat_succeeds(Xz!40)))) <=> ((~![Xx: $i, Xy: $i] : (nat_succeeds(tptp_fun_____(Xx, Xy)) | (~nat_succeeds(Xy)) | (~nat_succeeds(Xx)))) | (~nat_succeeds(Xz!40)) | (~nat_succeeds(tptp_fun_Xx2_26(Xx!42))) | nat_succeeds(tptp_fun_____(Xz!40, tptp_fun_Xx2_26(Xx!42))))),
% 0.38/0.61 inference(transitivity,[status(thm)],[176, 174])).
% 0.38/0.61 tff(178,plain,
% 0.38/0.61 ((~![Xx: $i, Xy: $i] : (nat_succeeds(tptp_fun_____(Xx, Xy)) | (~nat_succeeds(Xy)) | (~nat_succeeds(Xx)))) | (nat_succeeds(tptp_fun_____(Xz!40, tptp_fun_Xx2_26(Xx!42))) | (~nat_succeeds(tptp_fun_Xx2_26(Xx!42))) | (~nat_succeeds(Xz!40)))),
% 0.38/0.61 inference(quant_inst,[status(thm)],[])).
% 0.38/0.61 tff(179,plain,
% 0.38/0.61 ((~![Xx: $i, Xy: $i] : (nat_succeeds(tptp_fun_____(Xx, Xy)) | (~nat_succeeds(Xy)) | (~nat_succeeds(Xx)))) | (~nat_succeeds(Xz!40)) | (~nat_succeeds(tptp_fun_Xx2_26(Xx!42))) | nat_succeeds(tptp_fun_____(Xz!40, tptp_fun_Xx2_26(Xx!42)))),
% 0.38/0.61 inference(modus_ponens,[status(thm)],[178, 177])).
% 0.38/0.61 tff(180,plain,
% 0.38/0.61 (nat_succeeds(tptp_fun_____(Xz!40, tptp_fun_Xx2_26(Xx!42)))),
% 0.38/0.61 inference(unit_resolution,[status(thm)],[179, 173, 10, 69])).
% 0.38/0.61 tff(181,plain,
% 0.38/0.61 (^[Xx1: $i, Xx2: $i, Xy1: $i, Xy2: $i] : refl((tptp_fun_____succeeds_(tptp_fun_____(Xx1, Xx2), tptp_fun_____(Xy1, Xy2)) | (~nat_succeeds(Xy1)) | (~tptp_fun______succeeds_(Xx1, Xy1)) | (~tptp_fun_____succeeds_(Xx2, Xy2))) <=> (tptp_fun_____succeeds_(tptp_fun_____(Xx1, Xx2), tptp_fun_____(Xy1, Xy2)) | (~nat_succeeds(Xy1)) | (~tptp_fun______succeeds_(Xx1, Xy1)) | (~tptp_fun_____succeeds_(Xx2, Xy2))))),
% 0.38/0.61 inference(bind,[status(th)],[])).
% 0.38/0.61 tff(182,plain,
% 0.38/0.61 (![Xx1: $i, Xx2: $i, Xy1: $i, Xy2: $i] : (tptp_fun_____succeeds_(tptp_fun_____(Xx1, Xx2), tptp_fun_____(Xy1, Xy2)) | (~nat_succeeds(Xy1)) | (~tptp_fun______succeeds_(Xx1, Xy1)) | (~tptp_fun_____succeeds_(Xx2, Xy2))) <=> ![Xx1: $i, Xx2: $i, Xy1: $i, Xy2: $i] : (tptp_fun_____succeeds_(tptp_fun_____(Xx1, Xx2), tptp_fun_____(Xy1, Xy2)) | (~nat_succeeds(Xy1)) | (~tptp_fun______succeeds_(Xx1, Xy1)) | (~tptp_fun_____succeeds_(Xx2, Xy2)))),
% 0.38/0.61 inference(quant_intro,[status(thm)],[181])).
% 0.38/0.61 tff(183,plain,
% 0.38/0.61 (^[Xx1: $i, Xx2: $i, Xy1: $i, Xy2: $i] : trans(monotonicity(trans(monotonicity(rewrite((tptp_fun______succeeds_(Xx1, Xy1) & tptp_fun_____succeeds_(Xx2, Xy2) & nat_succeeds(Xy1)) <=> (~((~nat_succeeds(Xy1)) | (~tptp_fun______succeeds_(Xx1, Xy1)) | (~tptp_fun_____succeeds_(Xx2, Xy2))))), ((~(tptp_fun______succeeds_(Xx1, Xy1) & tptp_fun_____succeeds_(Xx2, Xy2) & nat_succeeds(Xy1))) <=> (~(~((~nat_succeeds(Xy1)) | (~tptp_fun______succeeds_(Xx1, Xy1)) | (~tptp_fun_____succeeds_(Xx2, Xy2))))))), rewrite((~(~((~nat_succeeds(Xy1)) | (~tptp_fun______succeeds_(Xx1, Xy1)) | (~tptp_fun_____succeeds_(Xx2, Xy2))))) <=> ((~nat_succeeds(Xy1)) | (~tptp_fun______succeeds_(Xx1, Xy1)) | (~tptp_fun_____succeeds_(Xx2, Xy2)))), ((~(tptp_fun______succeeds_(Xx1, Xy1) & tptp_fun_____succeeds_(Xx2, Xy2) & nat_succeeds(Xy1))) <=> ((~nat_succeeds(Xy1)) | (~tptp_fun______succeeds_(Xx1, Xy1)) | (~tptp_fun_____succeeds_(Xx2, Xy2))))), (((~(tptp_fun______succeeds_(Xx1, Xy1) & tptp_fun_____succeeds_(Xx2, Xy2) & nat_succeeds(Xy1))) | tptp_fun_____succeeds_(tptp_fun_____(Xx1, Xx2), tptp_fun_____(Xy1, Xy2))) <=> (((~nat_succeeds(Xy1)) | (~tptp_fun______succeeds_(Xx1, Xy1)) | (~tptp_fun_____succeeds_(Xx2, Xy2))) | tptp_fun_____succeeds_(tptp_fun_____(Xx1, Xx2), tptp_fun_____(Xy1, Xy2))))), rewrite((((~nat_succeeds(Xy1)) | (~tptp_fun______succeeds_(Xx1, Xy1)) | (~tptp_fun_____succeeds_(Xx2, Xy2))) | tptp_fun_____succeeds_(tptp_fun_____(Xx1, Xx2), tptp_fun_____(Xy1, Xy2))) <=> (tptp_fun_____succeeds_(tptp_fun_____(Xx1, Xx2), tptp_fun_____(Xy1, Xy2)) | (~nat_succeeds(Xy1)) | (~tptp_fun______succeeds_(Xx1, Xy1)) | (~tptp_fun_____succeeds_(Xx2, Xy2)))), (((~(tptp_fun______succeeds_(Xx1, Xy1) & tptp_fun_____succeeds_(Xx2, Xy2) & nat_succeeds(Xy1))) | tptp_fun_____succeeds_(tptp_fun_____(Xx1, Xx2), tptp_fun_____(Xy1, Xy2))) <=> (tptp_fun_____succeeds_(tptp_fun_____(Xx1, Xx2), tptp_fun_____(Xy1, Xy2)) | (~nat_succeeds(Xy1)) | (~tptp_fun______succeeds_(Xx1, Xy1)) | (~tptp_fun_____succeeds_(Xx2, Xy2)))))),
% 0.38/0.61 inference(bind,[status(th)],[])).
% 0.38/0.61 tff(184,plain,
% 0.38/0.61 (![Xx1: $i, Xx2: $i, Xy1: $i, Xy2: $i] : ((~(tptp_fun______succeeds_(Xx1, Xy1) & tptp_fun_____succeeds_(Xx2, Xy2) & nat_succeeds(Xy1))) | tptp_fun_____succeeds_(tptp_fun_____(Xx1, Xx2), tptp_fun_____(Xy1, Xy2))) <=> ![Xx1: $i, Xx2: $i, Xy1: $i, Xy2: $i] : (tptp_fun_____succeeds_(tptp_fun_____(Xx1, Xx2), tptp_fun_____(Xy1, Xy2)) | (~nat_succeeds(Xy1)) | (~tptp_fun______succeeds_(Xx1, Xy1)) | (~tptp_fun_____succeeds_(Xx2, Xy2)))),
% 0.38/0.61 inference(quant_intro,[status(thm)],[183])).
% 0.38/0.61 tff(185,plain,
% 0.38/0.61 (![Xx1: $i, Xx2: $i, Xy1: $i, Xy2: $i] : ((~(tptp_fun______succeeds_(Xx1, Xy1) & tptp_fun_____succeeds_(Xx2, Xy2) & nat_succeeds(Xy1))) | tptp_fun_____succeeds_(tptp_fun_____(Xx1, Xx2), tptp_fun_____(Xy1, Xy2))) <=> ![Xx1: $i, Xx2: $i, Xy1: $i, Xy2: $i] : ((~(tptp_fun______succeeds_(Xx1, Xy1) & tptp_fun_____succeeds_(Xx2, Xy2) & nat_succeeds(Xy1))) | tptp_fun_____succeeds_(tptp_fun_____(Xx1, Xx2), tptp_fun_____(Xy1, Xy2)))),
% 0.38/0.61 inference(rewrite,[status(thm)],[])).
% 0.38/0.61 tff(186,plain,
% 0.38/0.61 (^[Xx1: $i, Xx2: $i, Xy1: $i, Xy2: $i] : trans(monotonicity(rewrite(((tptp_fun______succeeds_(Xx1, Xy1) & tptp_fun_____succeeds_(Xx2, Xy2)) & nat_succeeds(Xy1)) <=> (tptp_fun______succeeds_(Xx1, Xy1) & tptp_fun_____succeeds_(Xx2, Xy2) & nat_succeeds(Xy1))), ((((tptp_fun______succeeds_(Xx1, Xy1) & tptp_fun_____succeeds_(Xx2, Xy2)) & nat_succeeds(Xy1)) => tptp_fun_____succeeds_(tptp_fun_____(Xx1, Xx2), tptp_fun_____(Xy1, Xy2))) <=> ((tptp_fun______succeeds_(Xx1, Xy1) & tptp_fun_____succeeds_(Xx2, Xy2) & nat_succeeds(Xy1)) => tptp_fun_____succeeds_(tptp_fun_____(Xx1, Xx2), tptp_fun_____(Xy1, Xy2))))), rewrite(((tptp_fun______succeeds_(Xx1, Xy1) & tptp_fun_____succeeds_(Xx2, Xy2) & nat_succeeds(Xy1)) => tptp_fun_____succeeds_(tptp_fun_____(Xx1, Xx2), tptp_fun_____(Xy1, Xy2))) <=> ((~(tptp_fun______succeeds_(Xx1, Xy1) & tptp_fun_____succeeds_(Xx2, Xy2) & nat_succeeds(Xy1))) | tptp_fun_____succeeds_(tptp_fun_____(Xx1, Xx2), tptp_fun_____(Xy1, Xy2)))), ((((tptp_fun______succeeds_(Xx1, Xy1) & tptp_fun_____succeeds_(Xx2, Xy2)) & nat_succeeds(Xy1)) => tptp_fun_____succeeds_(tptp_fun_____(Xx1, Xx2), tptp_fun_____(Xy1, Xy2))) <=> ((~(tptp_fun______succeeds_(Xx1, Xy1) & tptp_fun_____succeeds_(Xx2, Xy2) & nat_succeeds(Xy1))) | tptp_fun_____succeeds_(tptp_fun_____(Xx1, Xx2), tptp_fun_____(Xy1, Xy2)))))),
% 0.38/0.61 inference(bind,[status(th)],[])).
% 0.38/0.61 tff(187,plain,
% 0.38/0.61 (![Xx1: $i, Xx2: $i, Xy1: $i, Xy2: $i] : (((tptp_fun______succeeds_(Xx1, Xy1) & tptp_fun_____succeeds_(Xx2, Xy2)) & nat_succeeds(Xy1)) => tptp_fun_____succeeds_(tptp_fun_____(Xx1, Xx2), tptp_fun_____(Xy1, Xy2))) <=> ![Xx1: $i, Xx2: $i, Xy1: $i, Xy2: $i] : ((~(tptp_fun______succeeds_(Xx1, Xy1) & tptp_fun_____succeeds_(Xx2, Xy2) & nat_succeeds(Xy1))) | tptp_fun_____succeeds_(tptp_fun_____(Xx1, Xx2), tptp_fun_____(Xy1, Xy2)))),
% 0.38/0.61 inference(quant_intro,[status(thm)],[186])).
% 0.38/0.61 tff(188,axiom,(![Xx1: $i, Xx2: $i, Xy1: $i, Xy2: $i] : (((tptp_fun______succeeds_(Xx1, Xy1) & tptp_fun_____succeeds_(Xx2, Xy2)) & nat_succeeds(Xy1)) => tptp_fun_____succeeds_(tptp_fun_____(Xx1, Xx2), tptp_fun_____(Xy1, Xy2)))), file('/export/starexec/sandbox/benchmark/theBenchmark.p',''lemma-(plus:leq:less)'')).
% 0.38/0.61 tff(189,plain,
% 0.38/0.61 (![Xx1: $i, Xx2: $i, Xy1: $i, Xy2: $i] : ((~(tptp_fun______succeeds_(Xx1, Xy1) & tptp_fun_____succeeds_(Xx2, Xy2) & nat_succeeds(Xy1))) | tptp_fun_____succeeds_(tptp_fun_____(Xx1, Xx2), tptp_fun_____(Xy1, Xy2)))),
% 0.38/0.61 inference(modus_ponens,[status(thm)],[188, 187])).
% 0.38/0.61 tff(190,plain,
% 0.38/0.61 (![Xx1: $i, Xx2: $i, Xy1: $i, Xy2: $i] : ((~(tptp_fun______succeeds_(Xx1, Xy1) & tptp_fun_____succeeds_(Xx2, Xy2) & nat_succeeds(Xy1))) | tptp_fun_____succeeds_(tptp_fun_____(Xx1, Xx2), tptp_fun_____(Xy1, Xy2)))),
% 0.38/0.61 inference(modus_ponens,[status(thm)],[189, 185])).
% 0.38/0.61 tff(191,plain,(
% 0.38/0.61 ![Xx1: $i, Xx2: $i, Xy1: $i, Xy2: $i] : ((~(tptp_fun______succeeds_(Xx1, Xy1) & tptp_fun_____succeeds_(Xx2, Xy2) & nat_succeeds(Xy1))) | tptp_fun_____succeeds_(tptp_fun_____(Xx1, Xx2), tptp_fun_____(Xy1, Xy2)))),
% 0.38/0.61 inference(skolemize,[status(sab)],[190])).
% 0.38/0.61 tff(192,plain,
% 0.38/0.61 (![Xx1: $i, Xx2: $i, Xy1: $i, Xy2: $i] : (tptp_fun_____succeeds_(tptp_fun_____(Xx1, Xx2), tptp_fun_____(Xy1, Xy2)) | (~nat_succeeds(Xy1)) | (~tptp_fun______succeeds_(Xx1, Xy1)) | (~tptp_fun_____succeeds_(Xx2, Xy2)))),
% 0.38/0.61 inference(modus_ponens,[status(thm)],[191, 184])).
% 0.38/0.61 tff(193,plain,
% 0.38/0.61 (![Xx1: $i, Xx2: $i, Xy1: $i, Xy2: $i] : (tptp_fun_____succeeds_(tptp_fun_____(Xx1, Xx2), tptp_fun_____(Xy1, Xy2)) | (~nat_succeeds(Xy1)) | (~tptp_fun______succeeds_(Xx1, Xy1)) | (~tptp_fun_____succeeds_(Xx2, Xy2)))),
% 0.38/0.61 inference(modus_ponens,[status(thm)],[192, 182])).
% 0.38/0.61 tff(194,plain,
% 0.38/0.61 (((~![Xx1: $i, Xx2: $i, Xy1: $i, Xy2: $i] : (tptp_fun_____succeeds_(tptp_fun_____(Xx1, Xx2), tptp_fun_____(Xy1, Xy2)) | (~nat_succeeds(Xy1)) | (~tptp_fun______succeeds_(Xx1, Xy1)) | (~tptp_fun_____succeeds_(Xx2, Xy2)))) | ((~tptp_fun_____succeeds_(Xy!41, Xz!40)) | (~nat_succeeds(tptp_fun_____(Xz!40, tptp_fun_Xx2_26(Xx!42)))) | tptp_fun_____succeeds_(tptp_fun_____(tptp_fun_____(Xy!41, tptp_fun_Xx2_26(Xx!42)), Xy!41), tptp_fun_____(tptp_fun_____(Xz!40, tptp_fun_Xx2_26(Xx!42)), Xz!40)) | (~tptp_fun______succeeds_(tptp_fun_____(Xy!41, tptp_fun_Xx2_26(Xx!42)), tptp_fun_____(Xz!40, tptp_fun_Xx2_26(Xx!42)))))) <=> ((~![Xx1: $i, Xx2: $i, Xy1: $i, Xy2: $i] : (tptp_fun_____succeeds_(tptp_fun_____(Xx1, Xx2), tptp_fun_____(Xy1, Xy2)) | (~nat_succeeds(Xy1)) | (~tptp_fun______succeeds_(Xx1, Xy1)) | (~tptp_fun_____succeeds_(Xx2, Xy2)))) | (~tptp_fun_____succeeds_(Xy!41, Xz!40)) | (~nat_succeeds(tptp_fun_____(Xz!40, tptp_fun_Xx2_26(Xx!42)))) | tptp_fun_____succeeds_(tptp_fun_____(tptp_fun_____(Xy!41, tptp_fun_Xx2_26(Xx!42)), Xy!41), tptp_fun_____(tptp_fun_____(Xz!40, tptp_fun_Xx2_26(Xx!42)), Xz!40)) | (~tptp_fun______succeeds_(tptp_fun_____(Xy!41, tptp_fun_Xx2_26(Xx!42)), tptp_fun_____(Xz!40, tptp_fun_Xx2_26(Xx!42)))))),
% 0.38/0.61 inference(rewrite,[status(thm)],[])).
% 0.38/0.61 tff(195,plain,
% 0.38/0.61 ((tptp_fun_____succeeds_(tptp_fun_____(tptp_fun_____(Xy!41, tptp_fun_Xx2_26(Xx!42)), Xy!41), tptp_fun_____(tptp_fun_____(Xz!40, tptp_fun_Xx2_26(Xx!42)), Xz!40)) | (~nat_succeeds(tptp_fun_____(Xz!40, tptp_fun_Xx2_26(Xx!42)))) | (~tptp_fun______succeeds_(tptp_fun_____(Xy!41, tptp_fun_Xx2_26(Xx!42)), tptp_fun_____(Xz!40, tptp_fun_Xx2_26(Xx!42)))) | (~tptp_fun_____succeeds_(Xy!41, Xz!40))) <=> ((~tptp_fun_____succeeds_(Xy!41, Xz!40)) | (~nat_succeeds(tptp_fun_____(Xz!40, tptp_fun_Xx2_26(Xx!42)))) | tptp_fun_____succeeds_(tptp_fun_____(tptp_fun_____(Xy!41, tptp_fun_Xx2_26(Xx!42)), Xy!41), tptp_fun_____(tptp_fun_____(Xz!40, tptp_fun_Xx2_26(Xx!42)), Xz!40)) | (~tptp_fun______succeeds_(tptp_fun_____(Xy!41, tptp_fun_Xx2_26(Xx!42)), tptp_fun_____(Xz!40, tptp_fun_Xx2_26(Xx!42)))))),
% 0.38/0.61 inference(rewrite,[status(thm)],[])).
% 0.38/0.61 tff(196,plain,
% 0.38/0.61 (((~![Xx1: $i, Xx2: $i, Xy1: $i, Xy2: $i] : (tptp_fun_____succeeds_(tptp_fun_____(Xx1, Xx2), tptp_fun_____(Xy1, Xy2)) | (~nat_succeeds(Xy1)) | (~tptp_fun______succeeds_(Xx1, Xy1)) | (~tptp_fun_____succeeds_(Xx2, Xy2)))) | (tptp_fun_____succeeds_(tptp_fun_____(tptp_fun_____(Xy!41, tptp_fun_Xx2_26(Xx!42)), Xy!41), tptp_fun_____(tptp_fun_____(Xz!40, tptp_fun_Xx2_26(Xx!42)), Xz!40)) | (~nat_succeeds(tptp_fun_____(Xz!40, tptp_fun_Xx2_26(Xx!42)))) | (~tptp_fun______succeeds_(tptp_fun_____(Xy!41, tptp_fun_Xx2_26(Xx!42)), tptp_fun_____(Xz!40, tptp_fun_Xx2_26(Xx!42)))) | (~tptp_fun_____succeeds_(Xy!41, Xz!40)))) <=> ((~![Xx1: $i, Xx2: $i, Xy1: $i, Xy2: $i] : (tptp_fun_____succeeds_(tptp_fun_____(Xx1, Xx2), tptp_fun_____(Xy1, Xy2)) | (~nat_succeeds(Xy1)) | (~tptp_fun______succeeds_(Xx1, Xy1)) | (~tptp_fun_____succeeds_(Xx2, Xy2)))) | ((~tptp_fun_____succeeds_(Xy!41, Xz!40)) | (~nat_succeeds(tptp_fun_____(Xz!40, tptp_fun_Xx2_26(Xx!42)))) | tptp_fun_____succeeds_(tptp_fun_____(tptp_fun_____(Xy!41, tptp_fun_Xx2_26(Xx!42)), Xy!41), tptp_fun_____(tptp_fun_____(Xz!40, tptp_fun_Xx2_26(Xx!42)), Xz!40)) | (~tptp_fun______succeeds_(tptp_fun_____(Xy!41, tptp_fun_Xx2_26(Xx!42)), tptp_fun_____(Xz!40, tptp_fun_Xx2_26(Xx!42))))))),
% 0.38/0.62 inference(monotonicity,[status(thm)],[195])).
% 0.38/0.62 tff(197,plain,
% 0.38/0.62 (((~![Xx1: $i, Xx2: $i, Xy1: $i, Xy2: $i] : (tptp_fun_____succeeds_(tptp_fun_____(Xx1, Xx2), tptp_fun_____(Xy1, Xy2)) | (~nat_succeeds(Xy1)) | (~tptp_fun______succeeds_(Xx1, Xy1)) | (~tptp_fun_____succeeds_(Xx2, Xy2)))) | (tptp_fun_____succeeds_(tptp_fun_____(tptp_fun_____(Xy!41, tptp_fun_Xx2_26(Xx!42)), Xy!41), tptp_fun_____(tptp_fun_____(Xz!40, tptp_fun_Xx2_26(Xx!42)), Xz!40)) | (~nat_succeeds(tptp_fun_____(Xz!40, tptp_fun_Xx2_26(Xx!42)))) | (~tptp_fun______succeeds_(tptp_fun_____(Xy!41, tptp_fun_Xx2_26(Xx!42)), tptp_fun_____(Xz!40, tptp_fun_Xx2_26(Xx!42)))) | (~tptp_fun_____succeeds_(Xy!41, Xz!40)))) <=> ((~![Xx1: $i, Xx2: $i, Xy1: $i, Xy2: $i] : (tptp_fun_____succeeds_(tptp_fun_____(Xx1, Xx2), tptp_fun_____(Xy1, Xy2)) | (~nat_succeeds(Xy1)) | (~tptp_fun______succeeds_(Xx1, Xy1)) | (~tptp_fun_____succeeds_(Xx2, Xy2)))) | (~tptp_fun_____succeeds_(Xy!41, Xz!40)) | (~nat_succeeds(tptp_fun_____(Xz!40, tptp_fun_Xx2_26(Xx!42)))) | tptp_fun_____succeeds_(tptp_fun_____(tptp_fun_____(Xy!41, tptp_fun_Xx2_26(Xx!42)), Xy!41), tptp_fun_____(tptp_fun_____(Xz!40, tptp_fun_Xx2_26(Xx!42)), Xz!40)) | (~tptp_fun______succeeds_(tptp_fun_____(Xy!41, tptp_fun_Xx2_26(Xx!42)), tptp_fun_____(Xz!40, tptp_fun_Xx2_26(Xx!42)))))),
% 0.38/0.62 inference(transitivity,[status(thm)],[196, 194])).
% 0.38/0.62 tff(198,plain,
% 0.38/0.62 ((~![Xx1: $i, Xx2: $i, Xy1: $i, Xy2: $i] : (tptp_fun_____succeeds_(tptp_fun_____(Xx1, Xx2), tptp_fun_____(Xy1, Xy2)) | (~nat_succeeds(Xy1)) | (~tptp_fun______succeeds_(Xx1, Xy1)) | (~tptp_fun_____succeeds_(Xx2, Xy2)))) | (tptp_fun_____succeeds_(tptp_fun_____(tptp_fun_____(Xy!41, tptp_fun_Xx2_26(Xx!42)), Xy!41), tptp_fun_____(tptp_fun_____(Xz!40, tptp_fun_Xx2_26(Xx!42)), Xz!40)) | (~nat_succeeds(tptp_fun_____(Xz!40, tptp_fun_Xx2_26(Xx!42)))) | (~tptp_fun______succeeds_(tptp_fun_____(Xy!41, tptp_fun_Xx2_26(Xx!42)), tptp_fun_____(Xz!40, tptp_fun_Xx2_26(Xx!42)))) | (~tptp_fun_____succeeds_(Xy!41, Xz!40)))),
% 0.38/0.62 inference(quant_inst,[status(thm)],[])).
% 0.38/0.62 tff(199,plain,
% 0.38/0.62 ((~![Xx1: $i, Xx2: $i, Xy1: $i, Xy2: $i] : (tptp_fun_____succeeds_(tptp_fun_____(Xx1, Xx2), tptp_fun_____(Xy1, Xy2)) | (~nat_succeeds(Xy1)) | (~tptp_fun______succeeds_(Xx1, Xy1)) | (~tptp_fun_____succeeds_(Xx2, Xy2)))) | (~tptp_fun_____succeeds_(Xy!41, Xz!40)) | (~nat_succeeds(tptp_fun_____(Xz!40, tptp_fun_Xx2_26(Xx!42)))) | tptp_fun_____succeeds_(tptp_fun_____(tptp_fun_____(Xy!41, tptp_fun_Xx2_26(Xx!42)), Xy!41), tptp_fun_____(tptp_fun_____(Xz!40, tptp_fun_Xx2_26(Xx!42)), Xz!40)) | (~tptp_fun______succeeds_(tptp_fun_____(Xy!41, tptp_fun_Xx2_26(Xx!42)), tptp_fun_____(Xz!40, tptp_fun_Xx2_26(Xx!42))))),
% 0.38/0.62 inference(modus_ponens,[status(thm)],[198, 197])).
% 0.38/0.62 tff(200,plain,
% 0.38/0.62 ((~nat_succeeds(tptp_fun_____(Xz!40, tptp_fun_Xx2_26(Xx!42)))) | tptp_fun_____succeeds_(tptp_fun_____(tptp_fun_____(Xy!41, tptp_fun_Xx2_26(Xx!42)), Xy!41), tptp_fun_____(tptp_fun_____(Xz!40, tptp_fun_Xx2_26(Xx!42)), Xz!40)) | (~tptp_fun______succeeds_(tptp_fun_____(Xy!41, tptp_fun_Xx2_26(Xx!42)), tptp_fun_____(Xz!40, tptp_fun_Xx2_26(Xx!42))))),
% 0.38/0.62 inference(unit_resolution,[status(thm)],[199, 193, 91])).
% 0.38/0.62 tff(201,plain,
% 0.38/0.62 (tptp_fun_____succeeds_(tptp_fun_____(tptp_fun_____(Xy!41, tptp_fun_Xx2_26(Xx!42)), Xy!41), tptp_fun_____(tptp_fun_____(Xz!40, tptp_fun_Xx2_26(Xx!42)), Xz!40))),
% 0.38/0.62 inference(unit_resolution,[status(thm)],[200, 180, 160])).
% 0.38/0.62 tff(202,plain,
% 0.38/0.62 ($false),
% 0.38/0.62 inference(unit_resolution,[status(thm)],[201, 126])).
% 0.38/0.62 % SZS output end Proof
% 0.38/0.62 % E exiting
%------------------------------------------------------------------------------