%------------------------------------------------------------------------------
% File : Z3---4.15.1
% Problem : NUM505+3 : TPTP v9.0.0. Released v4.0.0.
% Transfm : none
% Format : tptp
% Command : run_E %s %d THM
% Computer : n016.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:21:12 AM UTC 2025
% Result : Theorem 0.39s 0.56s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.04/0.14 % Problem : NUM505+3 : TPTP v9.0.0. Released v4.0.0.
% 0.04/0.14 % Command : run_E %s %d THM
% 0.14/0.36 % Computer : n016.cluster.edu
% 0.14/0.36 % Model : x86_64 x86_64
% 0.14/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.36 % Memory : 8042.1875MB
% 0.14/0.36 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.36 % CPULimit : 300
% 0.14/0.36 % WCLimit : 300
% 0.14/0.36 % DateTime : Fri Jun 20 01:19:17 EDT 2025
% 0.14/0.36 % CPUTime :
% 0.39/0.56 % SZS status Theorem
% 0.39/0.56 % SZS output start Proof
% 0.39/0.56 tff(sdtlseqdt0_type, type, (
% 0.39/0.56 sdtlseqdt0: ( $i * $i ) > $o)).
% 0.39/0.56 tff(xp_type, type, (
% 0.39/0.56 xp: $i)).
% 0.39/0.56 tff(xk_type, type, (
% 0.39/0.56 xk: $i)).
% 0.39/0.56 tff(sdtsldt0_type, type, (
% 0.39/0.56 sdtsldt0: ( $i * $i ) > $i)).
% 0.39/0.56 tff(sdtasdt0_type, type, (
% 0.39/0.56 sdtasdt0: ( $i * $i ) > $i)).
% 0.39/0.56 tff(xm_type, type, (
% 0.39/0.56 xm: $i)).
% 0.39/0.56 tff(xn_type, type, (
% 0.39/0.56 xn: $i)).
% 0.39/0.56 tff(aNaturalNumber0_type, type, (
% 0.39/0.56 aNaturalNumber0: $i > $o)).
% 0.39/0.56 tff(sdtpldt0_type, type, (
% 0.39/0.56 sdtpldt0: ( $i * $i ) > $i)).
% 0.39/0.56 tff(sz00_type, type, (
% 0.39/0.56 sz00: $i)).
% 0.39/0.56 tff(1,plain,
% 0.39/0.56 ((xk = sdtsldt0(sdtasdt0(xn, xm), xp)) <=> (xk = sdtsldt0(sdtasdt0(xn, xm), xp))),
% 0.39/0.56 inference(rewrite,[status(thm)],[])).
% 0.39/0.56 tff(2,axiom,((aNaturalNumber0(xk) & (sdtasdt0(xn, xm) = sdtasdt0(xp, xk))) & (xk = sdtsldt0(sdtasdt0(xn, xm), xp))), file('/export/starexec/sandbox/benchmark/theBenchmark.p','m__2306')).
% 0.39/0.56 tff(3,plain,
% 0.39/0.56 (xk = sdtsldt0(sdtasdt0(xn, xm), xp)),
% 0.39/0.56 inference(and_elim,[status(thm)],[2])).
% 0.39/0.56 tff(4,plain,
% 0.39/0.56 (xk = sdtsldt0(sdtasdt0(xn, xm), xp)),
% 0.39/0.56 inference(modus_ponens,[status(thm)],[3, 1])).
% 0.39/0.56 tff(5,plain,
% 0.39/0.56 (sdtsldt0(sdtasdt0(xn, xm), xp) = xk),
% 0.39/0.56 inference(symmetry,[status(thm)],[4])).
% 0.39/0.56 tff(6,plain,
% 0.39/0.56 (sdtlseqdt0(sdtsldt0(sdtasdt0(xn, xm), xp), xp) <=> sdtlseqdt0(xk, xp)),
% 0.39/0.56 inference(monotonicity,[status(thm)],[5])).
% 0.39/0.56 tff(7,plain,
% 0.39/0.56 (aNaturalNumber0(sdtsldt0(sdtasdt0(xn, xm), xp)) <=> aNaturalNumber0(xk)),
% 0.39/0.56 inference(monotonicity,[status(thm)],[5])).
% 0.39/0.56 tff(8,plain,
% 0.39/0.56 (aNaturalNumber0(xk) <=> aNaturalNumber0(sdtsldt0(sdtasdt0(xn, xm), xp))),
% 0.39/0.56 inference(symmetry,[status(thm)],[7])).
% 0.39/0.56 tff(9,plain,
% 0.39/0.56 (aNaturalNumber0(xk) <=> aNaturalNumber0(xk)),
% 0.39/0.56 inference(rewrite,[status(thm)],[])).
% 0.39/0.56 tff(10,plain,
% 0.39/0.56 (aNaturalNumber0(xk) & (sdtasdt0(xn, xm) = sdtasdt0(xp, xk))),
% 0.39/0.56 inference(and_elim,[status(thm)],[2])).
% 0.39/0.56 tff(11,plain,
% 0.39/0.56 (aNaturalNumber0(xk)),
% 0.39/0.56 inference(and_elim,[status(thm)],[10])).
% 0.39/0.56 tff(12,plain,
% 0.39/0.56 (aNaturalNumber0(xk)),
% 0.39/0.56 inference(modus_ponens,[status(thm)],[11, 9])).
% 0.39/0.56 tff(13,plain,
% 0.39/0.56 (aNaturalNumber0(sdtsldt0(sdtasdt0(xn, xm), xp))),
% 0.39/0.56 inference(modus_ponens,[status(thm)],[12, 8])).
% 0.39/0.56 tff(14,plain,
% 0.39/0.56 (sdtlseqdt0(xp, sdtsldt0(sdtasdt0(xn, xm), xp)) <=> sdtlseqdt0(xp, xk)),
% 0.39/0.56 inference(monotonicity,[status(thm)],[5])).
% 0.39/0.56 tff(15,plain,
% 0.39/0.56 (sdtlseqdt0(xp, xk) <=> sdtlseqdt0(xp, sdtsldt0(sdtasdt0(xn, xm), xp))),
% 0.39/0.56 inference(symmetry,[status(thm)],[14])).
% 0.39/0.56 tff(16,plain,
% 0.39/0.56 ((~sdtlseqdt0(xp, xk)) <=> (~sdtlseqdt0(xp, sdtsldt0(sdtasdt0(xn, xm), xp)))),
% 0.39/0.56 inference(monotonicity,[status(thm)],[15])).
% 0.39/0.56 tff(17,plain,
% 0.39/0.56 ((~sdtlseqdt0(xp, xk)) <=> (~sdtlseqdt0(xp, xk))),
% 0.39/0.56 inference(rewrite,[status(thm)],[])).
% 0.39/0.56 tff(18,plain,
% 0.39/0.56 ((~((~(?[W0: $i] : (aNaturalNumber0(W0) & (sdtpldt0(xp, W0) = xk)) | sdtlseqdt0(xp, xk))) => ((~(xk = xp)) & (?[W0: $i] : (aNaturalNumber0(W0) & (sdtpldt0(xk, W0) = xp)) | sdtlseqdt0(xk, xp))))) <=> (~(sdtlseqdt0(xp, xk) | ?[W0: $i] : (aNaturalNumber0(W0) & (sdtpldt0(xp, W0) = xk)) | ((~(xk = xp)) & (sdtlseqdt0(xk, xp) | ?[W0: $i] : (aNaturalNumber0(W0) & (sdtpldt0(xk, W0) = xp))))))),
% 0.39/0.56 inference(rewrite,[status(thm)],[])).
% 0.39/0.56 tff(19,axiom,(~((~(?[W0: $i] : (aNaturalNumber0(W0) & (sdtpldt0(xp, W0) = xk)) | sdtlseqdt0(xp, xk))) => ((~(xk = xp)) & (?[W0: $i] : (aNaturalNumber0(W0) & (sdtpldt0(xk, W0) = xp)) | sdtlseqdt0(xk, xp))))), file('/export/starexec/sandbox/benchmark/theBenchmark.p','m__')).
% 0.39/0.56 tff(20,plain,
% 0.39/0.56 (~(sdtlseqdt0(xp, xk) | ?[W0: $i] : (aNaturalNumber0(W0) & (sdtpldt0(xp, W0) = xk)) | ((~(xk = xp)) & (sdtlseqdt0(xk, xp) | ?[W0: $i] : (aNaturalNumber0(W0) & (sdtpldt0(xk, W0) = xp)))))),
% 0.39/0.56 inference(modus_ponens,[status(thm)],[19, 18])).
% 0.39/0.56 tff(21,plain,
% 0.39/0.56 (~sdtlseqdt0(xp, xk)),
% 0.39/0.56 inference(or_elim,[status(thm)],[20])).
% 0.39/0.56 tff(22,plain,
% 0.39/0.56 (~sdtlseqdt0(xp, xk)),
% 0.39/0.56 inference(modus_ponens,[status(thm)],[21, 17])).
% 0.39/0.56 tff(23,plain,
% 0.39/0.56 (~sdtlseqdt0(xp, sdtsldt0(sdtasdt0(xn, xm), xp))),
% 0.39/0.56 inference(modus_ponens,[status(thm)],[22, 16])).
% 0.39/0.56 tff(24,plain,
% 0.39/0.56 (((xp = sdtsldt0(sdtasdt0(xn, xm), xp)) | (~sdtlseqdt0(xp, sdtsldt0(sdtasdt0(xn, xm), xp)))) | sdtlseqdt0(xp, sdtsldt0(sdtasdt0(xn, xm), xp))),
% 0.39/0.56 inference(tautology,[status(thm)],[])).
% 0.39/0.56 tff(25,plain,
% 0.39/0.56 ((xp = sdtsldt0(sdtasdt0(xn, xm), xp)) | (~sdtlseqdt0(xp, sdtsldt0(sdtasdt0(xn, xm), xp)))),
% 0.39/0.56 inference(unit_resolution,[status(thm)],[24, 23])).
% 0.39/0.56 tff(26,plain,
% 0.39/0.56 (aNaturalNumber0(xp) <=> aNaturalNumber0(xp)),
% 0.39/0.56 inference(rewrite,[status(thm)],[])).
% 0.39/0.56 tff(27,axiom,((aNaturalNumber0(xn) & aNaturalNumber0(xm)) & aNaturalNumber0(xp)), file('/export/starexec/sandbox/benchmark/theBenchmark.p','m__1837')).
% 0.39/0.56 tff(28,plain,
% 0.39/0.56 (aNaturalNumber0(xp)),
% 0.39/0.56 inference(and_elim,[status(thm)],[27])).
% 0.39/0.56 tff(29,plain,
% 0.39/0.56 (aNaturalNumber0(xp)),
% 0.39/0.56 inference(modus_ponens,[status(thm)],[28, 26])).
% 0.39/0.56 tff(30,plain,
% 0.39/0.56 (^[W0: $i, W1: $i] : refl((sdtlseqdt0(W0, W1) | (~aNaturalNumber0(W1)) | (~aNaturalNumber0(W0)) | (~((W1 = W0) | (~sdtlseqdt0(W1, W0))))) <=> (sdtlseqdt0(W0, W1) | (~aNaturalNumber0(W1)) | (~aNaturalNumber0(W0)) | (~((W1 = W0) | (~sdtlseqdt0(W1, W0))))))),
% 0.39/0.56 inference(bind,[status(th)],[])).
% 0.39/0.56 tff(31,plain,
% 0.39/0.56 (![W0: $i, W1: $i] : (sdtlseqdt0(W0, W1) | (~aNaturalNumber0(W1)) | (~aNaturalNumber0(W0)) | (~((W1 = W0) | (~sdtlseqdt0(W1, W0))))) <=> ![W0: $i, W1: $i] : (sdtlseqdt0(W0, W1) | (~aNaturalNumber0(W1)) | (~aNaturalNumber0(W0)) | (~((W1 = W0) | (~sdtlseqdt0(W1, W0)))))),
% 0.39/0.56 inference(quant_intro,[status(thm)],[30])).
% 0.39/0.56 tff(32,plain,
% 0.39/0.56 (^[W0: $i, W1: $i] : trans(monotonicity(rewrite(((~(W1 = W0)) & sdtlseqdt0(W1, W0)) <=> (~((W1 = W0) | (~sdtlseqdt0(W1, W0))))), trans(monotonicity(rewrite((aNaturalNumber0(W0) & aNaturalNumber0(W1)) <=> (~((~aNaturalNumber0(W1)) | (~aNaturalNumber0(W0))))), ((~(aNaturalNumber0(W0) & aNaturalNumber0(W1))) <=> (~(~((~aNaturalNumber0(W1)) | (~aNaturalNumber0(W0))))))), rewrite((~(~((~aNaturalNumber0(W1)) | (~aNaturalNumber0(W0))))) <=> ((~aNaturalNumber0(W1)) | (~aNaturalNumber0(W0)))), ((~(aNaturalNumber0(W0) & aNaturalNumber0(W1))) <=> ((~aNaturalNumber0(W1)) | (~aNaturalNumber0(W0))))), ((sdtlseqdt0(W0, W1) | ((~(W1 = W0)) & sdtlseqdt0(W1, W0)) | (~(aNaturalNumber0(W0) & aNaturalNumber0(W1)))) <=> (sdtlseqdt0(W0, W1) | (~((W1 = W0) | (~sdtlseqdt0(W1, W0)))) | ((~aNaturalNumber0(W1)) | (~aNaturalNumber0(W0)))))), rewrite((sdtlseqdt0(W0, W1) | (~((W1 = W0) | (~sdtlseqdt0(W1, W0)))) | ((~aNaturalNumber0(W1)) | (~aNaturalNumber0(W0)))) <=> (sdtlseqdt0(W0, W1) | (~aNaturalNumber0(W1)) | (~aNaturalNumber0(W0)) | (~((W1 = W0) | (~sdtlseqdt0(W1, W0)))))), ((sdtlseqdt0(W0, W1) | ((~(W1 = W0)) & sdtlseqdt0(W1, W0)) | (~(aNaturalNumber0(W0) & aNaturalNumber0(W1)))) <=> (sdtlseqdt0(W0, W1) | (~aNaturalNumber0(W1)) | (~aNaturalNumber0(W0)) | (~((W1 = W0) | (~sdtlseqdt0(W1, W0)))))))),
% 0.39/0.56 inference(bind,[status(th)],[])).
% 0.39/0.56 tff(33,plain,
% 0.39/0.56 (![W0: $i, W1: $i] : (sdtlseqdt0(W0, W1) | ((~(W1 = W0)) & sdtlseqdt0(W1, W0)) | (~(aNaturalNumber0(W0) & aNaturalNumber0(W1)))) <=> ![W0: $i, W1: $i] : (sdtlseqdt0(W0, W1) | (~aNaturalNumber0(W1)) | (~aNaturalNumber0(W0)) | (~((W1 = W0) | (~sdtlseqdt0(W1, W0)))))),
% 0.39/0.56 inference(quant_intro,[status(thm)],[32])).
% 0.39/0.56 tff(34,plain,
% 0.39/0.56 (![W0: $i, W1: $i] : (sdtlseqdt0(W0, W1) | ((~(W1 = W0)) & sdtlseqdt0(W1, W0)) | (~(aNaturalNumber0(W0) & aNaturalNumber0(W1)))) <=> ![W0: $i, W1: $i] : (sdtlseqdt0(W0, W1) | ((~(W1 = W0)) & sdtlseqdt0(W1, W0)) | (~(aNaturalNumber0(W0) & aNaturalNumber0(W1))))),
% 0.39/0.56 inference(rewrite,[status(thm)],[])).
% 0.39/0.56 tff(35,plain,
% 0.39/0.56 (^[W0: $i, W1: $i] : rewrite(((aNaturalNumber0(W0) & aNaturalNumber0(W1)) => (sdtlseqdt0(W0, W1) | ((~(W1 = W0)) & sdtlseqdt0(W1, W0)))) <=> (sdtlseqdt0(W0, W1) | ((~(W1 = W0)) & sdtlseqdt0(W1, W0)) | (~(aNaturalNumber0(W0) & aNaturalNumber0(W1)))))),
% 0.39/0.56 inference(bind,[status(th)],[])).
% 0.39/0.56 tff(36,plain,
% 0.39/0.56 (![W0: $i, W1: $i] : ((aNaturalNumber0(W0) & aNaturalNumber0(W1)) => (sdtlseqdt0(W0, W1) | ((~(W1 = W0)) & sdtlseqdt0(W1, W0)))) <=> ![W0: $i, W1: $i] : (sdtlseqdt0(W0, W1) | ((~(W1 = W0)) & sdtlseqdt0(W1, W0)) | (~(aNaturalNumber0(W0) & aNaturalNumber0(W1))))),
% 0.39/0.56 inference(quant_intro,[status(thm)],[35])).
% 0.39/0.56 tff(37,axiom,(![W0: $i, W1: $i] : ((aNaturalNumber0(W0) & aNaturalNumber0(W1)) => (sdtlseqdt0(W0, W1) | ((~(W1 = W0)) & sdtlseqdt0(W1, W0))))), file('/export/starexec/sandbox/benchmark/theBenchmark.p','mLETotal')).
% 0.39/0.56 tff(38,plain,
% 0.39/0.56 (![W0: $i, W1: $i] : (sdtlseqdt0(W0, W1) | ((~(W1 = W0)) & sdtlseqdt0(W1, W0)) | (~(aNaturalNumber0(W0) & aNaturalNumber0(W1))))),
% 0.39/0.56 inference(modus_ponens,[status(thm)],[37, 36])).
% 0.39/0.56 tff(39,plain,
% 0.39/0.56 (![W0: $i, W1: $i] : (sdtlseqdt0(W0, W1) | ((~(W1 = W0)) & sdtlseqdt0(W1, W0)) | (~(aNaturalNumber0(W0) & aNaturalNumber0(W1))))),
% 0.39/0.56 inference(modus_ponens,[status(thm)],[38, 34])).
% 0.39/0.56 tff(40,plain,(
% 0.39/0.56 ![W0: $i, W1: $i] : (sdtlseqdt0(W0, W1) | ((~(W1 = W0)) & sdtlseqdt0(W1, W0)) | (~(aNaturalNumber0(W0) & aNaturalNumber0(W1))))),
% 0.39/0.56 inference(skolemize,[status(sab)],[39])).
% 0.39/0.56 tff(41,plain,
% 0.39/0.56 (![W0: $i, W1: $i] : (sdtlseqdt0(W0, W1) | (~aNaturalNumber0(W1)) | (~aNaturalNumber0(W0)) | (~((W1 = W0) | (~sdtlseqdt0(W1, W0)))))),
% 0.39/0.56 inference(modus_ponens,[status(thm)],[40, 33])).
% 0.39/0.56 tff(42,plain,
% 0.39/0.56 (![W0: $i, W1: $i] : (sdtlseqdt0(W0, W1) | (~aNaturalNumber0(W1)) | (~aNaturalNumber0(W0)) | (~((W1 = W0) | (~sdtlseqdt0(W1, W0)))))),
% 0.39/0.56 inference(modus_ponens,[status(thm)],[41, 31])).
% 0.39/0.56 tff(43,plain,
% 0.39/0.56 (((~![W0: $i, W1: $i] : (sdtlseqdt0(W0, W1) | (~aNaturalNumber0(W1)) | (~aNaturalNumber0(W0)) | (~((W1 = W0) | (~sdtlseqdt0(W1, W0)))))) | ((~aNaturalNumber0(xp)) | (~aNaturalNumber0(sdtsldt0(sdtasdt0(xn, xm), xp))) | sdtlseqdt0(sdtsldt0(sdtasdt0(xn, xm), xp), xp) | (~((xp = sdtsldt0(sdtasdt0(xn, xm), xp)) | (~sdtlseqdt0(xp, sdtsldt0(sdtasdt0(xn, xm), xp))))))) <=> ((~![W0: $i, W1: $i] : (sdtlseqdt0(W0, W1) | (~aNaturalNumber0(W1)) | (~aNaturalNumber0(W0)) | (~((W1 = W0) | (~sdtlseqdt0(W1, W0)))))) | (~aNaturalNumber0(xp)) | (~aNaturalNumber0(sdtsldt0(sdtasdt0(xn, xm), xp))) | sdtlseqdt0(sdtsldt0(sdtasdt0(xn, xm), xp), xp) | (~((xp = sdtsldt0(sdtasdt0(xn, xm), xp)) | (~sdtlseqdt0(xp, sdtsldt0(sdtasdt0(xn, xm), xp))))))),
% 0.39/0.56 inference(rewrite,[status(thm)],[])).
% 0.39/0.56 tff(44,plain,
% 0.39/0.56 ((sdtlseqdt0(sdtsldt0(sdtasdt0(xn, xm), xp), xp) | (~aNaturalNumber0(xp)) | (~aNaturalNumber0(sdtsldt0(sdtasdt0(xn, xm), xp))) | (~((xp = sdtsldt0(sdtasdt0(xn, xm), xp)) | (~sdtlseqdt0(xp, sdtsldt0(sdtasdt0(xn, xm), xp)))))) <=> ((~aNaturalNumber0(xp)) | (~aNaturalNumber0(sdtsldt0(sdtasdt0(xn, xm), xp))) | sdtlseqdt0(sdtsldt0(sdtasdt0(xn, xm), xp), xp) | (~((xp = sdtsldt0(sdtasdt0(xn, xm), xp)) | (~sdtlseqdt0(xp, sdtsldt0(sdtasdt0(xn, xm), xp))))))),
% 0.39/0.56 inference(rewrite,[status(thm)],[])).
% 0.39/0.56 tff(45,plain,
% 0.39/0.56 ((~((xp = sdtsldt0(sdtasdt0(xn, xm), xp)) | (~sdtlseqdt0(xp, sdtsldt0(sdtasdt0(xn, xm), xp))))) <=> (~((xp = sdtsldt0(sdtasdt0(xn, xm), xp)) | (~sdtlseqdt0(xp, sdtsldt0(sdtasdt0(xn, xm), xp)))))),
% 0.39/0.56 inference(rewrite,[status(thm)],[])).
% 0.39/0.56 tff(46,plain,
% 0.39/0.56 ((sdtlseqdt0(sdtsldt0(sdtasdt0(xn, xm), xp), xp) | (~aNaturalNumber0(xp)) | (~aNaturalNumber0(sdtsldt0(sdtasdt0(xn, xm), xp))) | (~((xp = sdtsldt0(sdtasdt0(xn, xm), xp)) | (~sdtlseqdt0(xp, sdtsldt0(sdtasdt0(xn, xm), xp)))))) <=> (sdtlseqdt0(sdtsldt0(sdtasdt0(xn, xm), xp), xp) | (~aNaturalNumber0(xp)) | (~aNaturalNumber0(sdtsldt0(sdtasdt0(xn, xm), xp))) | (~((xp = sdtsldt0(sdtasdt0(xn, xm), xp)) | (~sdtlseqdt0(xp, sdtsldt0(sdtasdt0(xn, xm), xp))))))),
% 0.39/0.56 inference(monotonicity,[status(thm)],[45])).
% 0.39/0.56 tff(47,plain,
% 0.39/0.56 ((sdtlseqdt0(sdtsldt0(sdtasdt0(xn, xm), xp), xp) | (~aNaturalNumber0(xp)) | (~aNaturalNumber0(sdtsldt0(sdtasdt0(xn, xm), xp))) | (~((xp = sdtsldt0(sdtasdt0(xn, xm), xp)) | (~sdtlseqdt0(xp, sdtsldt0(sdtasdt0(xn, xm), xp)))))) <=> ((~aNaturalNumber0(xp)) | (~aNaturalNumber0(sdtsldt0(sdtasdt0(xn, xm), xp))) | sdtlseqdt0(sdtsldt0(sdtasdt0(xn, xm), xp), xp) | (~((xp = sdtsldt0(sdtasdt0(xn, xm), xp)) | (~sdtlseqdt0(xp, sdtsldt0(sdtasdt0(xn, xm), xp))))))),
% 0.39/0.56 inference(transitivity,[status(thm)],[46, 44])).
% 0.39/0.56 tff(48,plain,
% 0.39/0.56 (((~![W0: $i, W1: $i] : (sdtlseqdt0(W0, W1) | (~aNaturalNumber0(W1)) | (~aNaturalNumber0(W0)) | (~((W1 = W0) | (~sdtlseqdt0(W1, W0)))))) | (sdtlseqdt0(sdtsldt0(sdtasdt0(xn, xm), xp), xp) | (~aNaturalNumber0(xp)) | (~aNaturalNumber0(sdtsldt0(sdtasdt0(xn, xm), xp))) | (~((xp = sdtsldt0(sdtasdt0(xn, xm), xp)) | (~sdtlseqdt0(xp, sdtsldt0(sdtasdt0(xn, xm), xp))))))) <=> ((~![W0: $i, W1: $i] : (sdtlseqdt0(W0, W1) | (~aNaturalNumber0(W1)) | (~aNaturalNumber0(W0)) | (~((W1 = W0) | (~sdtlseqdt0(W1, W0)))))) | ((~aNaturalNumber0(xp)) | (~aNaturalNumber0(sdtsldt0(sdtasdt0(xn, xm), xp))) | sdtlseqdt0(sdtsldt0(sdtasdt0(xn, xm), xp), xp) | (~((xp = sdtsldt0(sdtasdt0(xn, xm), xp)) | (~sdtlseqdt0(xp, sdtsldt0(sdtasdt0(xn, xm), xp)))))))),
% 0.39/0.56 inference(monotonicity,[status(thm)],[47])).
% 0.39/0.56 tff(49,plain,
% 0.39/0.56 (((~![W0: $i, W1: $i] : (sdtlseqdt0(W0, W1) | (~aNaturalNumber0(W1)) | (~aNaturalNumber0(W0)) | (~((W1 = W0) | (~sdtlseqdt0(W1, W0)))))) | (sdtlseqdt0(sdtsldt0(sdtasdt0(xn, xm), xp), xp) | (~aNaturalNumber0(xp)) | (~aNaturalNumber0(sdtsldt0(sdtasdt0(xn, xm), xp))) | (~((xp = sdtsldt0(sdtasdt0(xn, xm), xp)) | (~sdtlseqdt0(xp, sdtsldt0(sdtasdt0(xn, xm), xp))))))) <=> ((~![W0: $i, W1: $i] : (sdtlseqdt0(W0, W1) | (~aNaturalNumber0(W1)) | (~aNaturalNumber0(W0)) | (~((W1 = W0) | (~sdtlseqdt0(W1, W0)))))) | (~aNaturalNumber0(xp)) | (~aNaturalNumber0(sdtsldt0(sdtasdt0(xn, xm), xp))) | sdtlseqdt0(sdtsldt0(sdtasdt0(xn, xm), xp), xp) | (~((xp = sdtsldt0(sdtasdt0(xn, xm), xp)) | (~sdtlseqdt0(xp, sdtsldt0(sdtasdt0(xn, xm), xp))))))),
% 0.39/0.56 inference(transitivity,[status(thm)],[48, 43])).
% 0.39/0.56 tff(50,plain,
% 0.39/0.56 ((~![W0: $i, W1: $i] : (sdtlseqdt0(W0, W1) | (~aNaturalNumber0(W1)) | (~aNaturalNumber0(W0)) | (~((W1 = W0) | (~sdtlseqdt0(W1, W0)))))) | (sdtlseqdt0(sdtsldt0(sdtasdt0(xn, xm), xp), xp) | (~aNaturalNumber0(xp)) | (~aNaturalNumber0(sdtsldt0(sdtasdt0(xn, xm), xp))) | (~((xp = sdtsldt0(sdtasdt0(xn, xm), xp)) | (~sdtlseqdt0(xp, sdtsldt0(sdtasdt0(xn, xm), xp))))))),
% 0.39/0.56 inference(quant_inst,[status(thm)],[])).
% 0.39/0.56 tff(51,plain,
% 0.39/0.56 ((~![W0: $i, W1: $i] : (sdtlseqdt0(W0, W1) | (~aNaturalNumber0(W1)) | (~aNaturalNumber0(W0)) | (~((W1 = W0) | (~sdtlseqdt0(W1, W0)))))) | (~aNaturalNumber0(xp)) | (~aNaturalNumber0(sdtsldt0(sdtasdt0(xn, xm), xp))) | sdtlseqdt0(sdtsldt0(sdtasdt0(xn, xm), xp), xp) | (~((xp = sdtsldt0(sdtasdt0(xn, xm), xp)) | (~sdtlseqdt0(xp, sdtsldt0(sdtasdt0(xn, xm), xp)))))),
% 0.39/0.56 inference(modus_ponens,[status(thm)],[50, 49])).
% 0.39/0.56 tff(52,plain,
% 0.39/0.56 ((~aNaturalNumber0(sdtsldt0(sdtasdt0(xn, xm), xp))) | sdtlseqdt0(sdtsldt0(sdtasdt0(xn, xm), xp), xp) | (~((xp = sdtsldt0(sdtasdt0(xn, xm), xp)) | (~sdtlseqdt0(xp, sdtsldt0(sdtasdt0(xn, xm), xp)))))),
% 0.39/0.56 inference(unit_resolution,[status(thm)],[51, 42, 29])).
% 0.39/0.56 tff(53,plain,
% 0.39/0.56 (sdtlseqdt0(sdtsldt0(sdtasdt0(xn, xm), xp), xp)),
% 0.39/0.56 inference(unit_resolution,[status(thm)],[52, 25, 13])).
% 0.39/0.56 tff(54,plain,
% 0.39/0.56 (sdtlseqdt0(xk, xp)),
% 0.39/0.56 inference(modus_ponens,[status(thm)],[53, 6])).
% 0.39/0.56 tff(55,plain,
% 0.39/0.56 ((xp = xk) <=> (xk = xp)),
% 0.39/0.56 inference(commutativity,[status(thm)],[])).
% 0.39/0.56 tff(56,plain,
% 0.39/0.56 (^[W0: $i] : refl(((~aNaturalNumber0(W0)) | (~((~(sdtpldt0(W0, sz00) = W0)) | (~(W0 = sdtpldt0(sz00, W0)))))) <=> ((~aNaturalNumber0(W0)) | (~((~(sdtpldt0(W0, sz00) = W0)) | (~(W0 = sdtpldt0(sz00, W0)))))))),
% 0.39/0.56 inference(bind,[status(th)],[])).
% 0.39/0.56 tff(57,plain,
% 0.39/0.56 (![W0: $i] : ((~aNaturalNumber0(W0)) | (~((~(sdtpldt0(W0, sz00) = W0)) | (~(W0 = sdtpldt0(sz00, W0)))))) <=> ![W0: $i] : ((~aNaturalNumber0(W0)) | (~((~(sdtpldt0(W0, sz00) = W0)) | (~(W0 = sdtpldt0(sz00, W0))))))),
% 0.39/0.56 inference(quant_intro,[status(thm)],[56])).
% 0.39/0.56 tff(58,plain,
% 0.39/0.56 (^[W0: $i] : rewrite(((~aNaturalNumber0(W0)) | ((sdtpldt0(W0, sz00) = W0) & (W0 = sdtpldt0(sz00, W0)))) <=> ((~aNaturalNumber0(W0)) | (~((~(sdtpldt0(W0, sz00) = W0)) | (~(W0 = sdtpldt0(sz00, W0)))))))),
% 0.39/0.56 inference(bind,[status(th)],[])).
% 0.39/0.56 tff(59,plain,
% 0.39/0.56 (![W0: $i] : ((~aNaturalNumber0(W0)) | ((sdtpldt0(W0, sz00) = W0) & (W0 = sdtpldt0(sz00, W0)))) <=> ![W0: $i] : ((~aNaturalNumber0(W0)) | (~((~(sdtpldt0(W0, sz00) = W0)) | (~(W0 = sdtpldt0(sz00, W0))))))),
% 0.39/0.56 inference(quant_intro,[status(thm)],[58])).
% 0.39/0.56 tff(60,plain,
% 0.39/0.56 (![W0: $i] : ((~aNaturalNumber0(W0)) | ((sdtpldt0(W0, sz00) = W0) & (W0 = sdtpldt0(sz00, W0)))) <=> ![W0: $i] : ((~aNaturalNumber0(W0)) | ((sdtpldt0(W0, sz00) = W0) & (W0 = sdtpldt0(sz00, W0))))),
% 0.39/0.56 inference(rewrite,[status(thm)],[])).
% 0.39/0.56 tff(61,plain,
% 0.39/0.56 (^[W0: $i] : rewrite((aNaturalNumber0(W0) => ((sdtpldt0(W0, sz00) = W0) & (W0 = sdtpldt0(sz00, W0)))) <=> ((~aNaturalNumber0(W0)) | ((sdtpldt0(W0, sz00) = W0) & (W0 = sdtpldt0(sz00, W0)))))),
% 0.39/0.57 inference(bind,[status(th)],[])).
% 0.39/0.57 tff(62,plain,
% 0.39/0.57 (![W0: $i] : (aNaturalNumber0(W0) => ((sdtpldt0(W0, sz00) = W0) & (W0 = sdtpldt0(sz00, W0)))) <=> ![W0: $i] : ((~aNaturalNumber0(W0)) | ((sdtpldt0(W0, sz00) = W0) & (W0 = sdtpldt0(sz00, W0))))),
% 0.39/0.57 inference(quant_intro,[status(thm)],[61])).
% 0.39/0.57 tff(63,axiom,(![W0: $i] : (aNaturalNumber0(W0) => ((sdtpldt0(W0, sz00) = W0) & (W0 = sdtpldt0(sz00, W0))))), file('/export/starexec/sandbox/benchmark/theBenchmark.p','m_AddZero')).
% 0.39/0.57 tff(64,plain,
% 0.39/0.57 (![W0: $i] : ((~aNaturalNumber0(W0)) | ((sdtpldt0(W0, sz00) = W0) & (W0 = sdtpldt0(sz00, W0))))),
% 0.39/0.57 inference(modus_ponens,[status(thm)],[63, 62])).
% 0.39/0.57 tff(65,plain,
% 0.39/0.57 (![W0: $i] : ((~aNaturalNumber0(W0)) | ((sdtpldt0(W0, sz00) = W0) & (W0 = sdtpldt0(sz00, W0))))),
% 0.39/0.57 inference(modus_ponens,[status(thm)],[64, 60])).
% 0.39/0.57 tff(66,plain,(
% 0.39/0.57 ![W0: $i] : ((~aNaturalNumber0(W0)) | ((sdtpldt0(W0, sz00) = W0) & (W0 = sdtpldt0(sz00, W0))))),
% 0.39/0.57 inference(skolemize,[status(sab)],[65])).
% 0.39/0.57 tff(67,plain,
% 0.39/0.57 (![W0: $i] : ((~aNaturalNumber0(W0)) | (~((~(sdtpldt0(W0, sz00) = W0)) | (~(W0 = sdtpldt0(sz00, W0))))))),
% 0.39/0.57 inference(modus_ponens,[status(thm)],[66, 59])).
% 0.39/0.57 tff(68,plain,
% 0.39/0.57 (![W0: $i] : ((~aNaturalNumber0(W0)) | (~((~(sdtpldt0(W0, sz00) = W0)) | (~(W0 = sdtpldt0(sz00, W0))))))),
% 0.39/0.57 inference(modus_ponens,[status(thm)],[67, 57])).
% 0.39/0.57 tff(69,plain,
% 0.39/0.57 (((~![W0: $i] : ((~aNaturalNumber0(W0)) | (~((~(sdtpldt0(W0, sz00) = W0)) | (~(W0 = sdtpldt0(sz00, W0))))))) | ((~aNaturalNumber0(xp)) | (~((~(sdtpldt0(xp, sz00) = xp)) | (~(xp = sdtpldt0(sz00, xp))))))) <=> ((~![W0: $i] : ((~aNaturalNumber0(W0)) | (~((~(sdtpldt0(W0, sz00) = W0)) | (~(W0 = sdtpldt0(sz00, W0))))))) | (~aNaturalNumber0(xp)) | (~((~(sdtpldt0(xp, sz00) = xp)) | (~(xp = sdtpldt0(sz00, xp))))))),
% 0.39/0.57 inference(rewrite,[status(thm)],[])).
% 0.39/0.57 tff(70,plain,
% 0.39/0.57 ((~![W0: $i] : ((~aNaturalNumber0(W0)) | (~((~(sdtpldt0(W0, sz00) = W0)) | (~(W0 = sdtpldt0(sz00, W0))))))) | ((~aNaturalNumber0(xp)) | (~((~(sdtpldt0(xp, sz00) = xp)) | (~(xp = sdtpldt0(sz00, xp))))))),
% 0.39/0.57 inference(quant_inst,[status(thm)],[])).
% 0.39/0.57 tff(71,plain,
% 0.39/0.57 ((~![W0: $i] : ((~aNaturalNumber0(W0)) | (~((~(sdtpldt0(W0, sz00) = W0)) | (~(W0 = sdtpldt0(sz00, W0))))))) | (~aNaturalNumber0(xp)) | (~((~(sdtpldt0(xp, sz00) = xp)) | (~(xp = sdtpldt0(sz00, xp)))))),
% 0.39/0.57 inference(modus_ponens,[status(thm)],[70, 69])).
% 0.39/0.57 tff(72,plain,
% 0.39/0.57 (~((~(sdtpldt0(xp, sz00) = xp)) | (~(xp = sdtpldt0(sz00, xp))))),
% 0.39/0.57 inference(unit_resolution,[status(thm)],[71, 68, 29])).
% 0.39/0.57 tff(73,plain,
% 0.39/0.57 (((~(sdtpldt0(xp, sz00) = xp)) | (~(xp = sdtpldt0(sz00, xp)))) | (sdtpldt0(xp, sz00) = xp)),
% 0.39/0.57 inference(tautology,[status(thm)],[])).
% 0.39/0.57 tff(74,plain,
% 0.39/0.57 (sdtpldt0(xp, sz00) = xp),
% 0.39/0.57 inference(unit_resolution,[status(thm)],[73, 72])).
% 0.39/0.57 tff(75,plain,
% 0.39/0.57 ((sdtpldt0(xp, sz00) = xk) <=> (xp = xk)),
% 0.39/0.57 inference(monotonicity,[status(thm)],[74])).
% 0.39/0.57 tff(76,plain,
% 0.39/0.57 ((sdtpldt0(xp, sz00) = xk) <=> (xk = xp)),
% 0.39/0.57 inference(transitivity,[status(thm)],[75, 55])).
% 0.39/0.57 tff(77,plain,
% 0.39/0.57 ((~(sdtpldt0(xp, sz00) = xk)) <=> (~(xk = xp))),
% 0.39/0.57 inference(monotonicity,[status(thm)],[76])).
% 0.39/0.57 tff(78,plain,
% 0.39/0.57 (^[W0: $i] : refl(((~aNaturalNumber0(W0)) | (~(sdtpldt0(xp, W0) = xk))) <=> ((~aNaturalNumber0(W0)) | (~(sdtpldt0(xp, W0) = xk))))),
% 0.39/0.57 inference(bind,[status(th)],[])).
% 0.39/0.57 tff(79,plain,
% 0.39/0.57 (![W0: $i] : ((~aNaturalNumber0(W0)) | (~(sdtpldt0(xp, W0) = xk))) <=> ![W0: $i] : ((~aNaturalNumber0(W0)) | (~(sdtpldt0(xp, W0) = xk)))),
% 0.39/0.57 inference(quant_intro,[status(thm)],[78])).
% 0.39/0.57 tff(80,plain,
% 0.39/0.57 (^[W0: $i] : trans(monotonicity(rewrite((aNaturalNumber0(W0) & (sdtpldt0(xp, W0) = xk)) <=> (~((~aNaturalNumber0(W0)) | (~(sdtpldt0(xp, W0) = xk))))), ((~(aNaturalNumber0(W0) & (sdtpldt0(xp, W0) = xk))) <=> (~(~((~aNaturalNumber0(W0)) | (~(sdtpldt0(xp, W0) = xk))))))), rewrite((~(~((~aNaturalNumber0(W0)) | (~(sdtpldt0(xp, W0) = xk))))) <=> ((~aNaturalNumber0(W0)) | (~(sdtpldt0(xp, W0) = xk)))), ((~(aNaturalNumber0(W0) & (sdtpldt0(xp, W0) = xk))) <=> ((~aNaturalNumber0(W0)) | (~(sdtpldt0(xp, W0) = xk)))))),
% 0.39/0.57 inference(bind,[status(th)],[])).
% 0.39/0.57 tff(81,plain,
% 0.39/0.57 (![W0: $i] : (~(aNaturalNumber0(W0) & (sdtpldt0(xp, W0) = xk))) <=> ![W0: $i] : ((~aNaturalNumber0(W0)) | (~(sdtpldt0(xp, W0) = xk)))),
% 0.39/0.57 inference(quant_intro,[status(thm)],[80])).
% 0.39/0.57 tff(82,plain,
% 0.39/0.57 ((~?[W0: $i] : (aNaturalNumber0(W0) & (sdtpldt0(xp, W0) = xk))) <=> (~?[W0: $i] : (aNaturalNumber0(W0) & (sdtpldt0(xp, W0) = xk)))),
% 0.39/0.57 inference(rewrite,[status(thm)],[])).
% 0.39/0.57 tff(83,plain,
% 0.39/0.57 (~?[W0: $i] : (aNaturalNumber0(W0) & (sdtpldt0(xp, W0) = xk))),
% 0.39/0.57 inference(or_elim,[status(thm)],[20])).
% 0.39/0.57 tff(84,plain,
% 0.39/0.57 (~?[W0: $i] : (aNaturalNumber0(W0) & (sdtpldt0(xp, W0) = xk))),
% 0.39/0.57 inference(modus_ponens,[status(thm)],[83, 82])).
% 0.39/0.57 tff(85,plain,
% 0.39/0.57 (~?[W0: $i] : (aNaturalNumber0(W0) & (sdtpldt0(xp, W0) = xk))),
% 0.39/0.57 inference(modus_ponens,[status(thm)],[84, 82])).
% 0.39/0.57 tff(86,plain,
% 0.39/0.57 (~?[W0: $i] : (aNaturalNumber0(W0) & (sdtpldt0(xp, W0) = xk))),
% 0.39/0.57 inference(modus_ponens,[status(thm)],[85, 82])).
% 0.39/0.57 tff(87,plain,
% 0.39/0.57 (^[W0: $i] : refl($oeq((~(aNaturalNumber0(W0) & (sdtpldt0(xp, W0) = xk))), (~(aNaturalNumber0(W0) & (sdtpldt0(xp, W0) = xk)))))),
% 0.39/0.57 inference(bind,[status(th)],[])).
% 0.39/0.57 tff(88,plain,(
% 0.39/0.57 ![W0: $i] : (~(aNaturalNumber0(W0) & (sdtpldt0(xp, W0) = xk)))),
% 0.39/0.57 inference(nnf-neg,[status(sab)],[86, 87])).
% 0.39/0.57 tff(89,plain,
% 0.39/0.57 (![W0: $i] : ((~aNaturalNumber0(W0)) | (~(sdtpldt0(xp, W0) = xk)))),
% 0.39/0.57 inference(modus_ponens,[status(thm)],[88, 81])).
% 0.39/0.57 tff(90,plain,
% 0.39/0.57 (![W0: $i] : ((~aNaturalNumber0(W0)) | (~(sdtpldt0(xp, W0) = xk)))),
% 0.39/0.57 inference(modus_ponens,[status(thm)],[89, 79])).
% 0.39/0.57 tff(91,plain,
% 0.39/0.57 (aNaturalNumber0(sz00) <=> aNaturalNumber0(sz00)),
% 0.39/0.57 inference(rewrite,[status(thm)],[])).
% 0.39/0.57 tff(92,axiom,(aNaturalNumber0(sz00)), file('/export/starexec/sandbox/benchmark/theBenchmark.p','mSortsC')).
% 0.39/0.57 tff(93,plain,
% 0.39/0.57 (aNaturalNumber0(sz00)),
% 0.39/0.57 inference(modus_ponens,[status(thm)],[92, 91])).
% 0.39/0.57 tff(94,plain,
% 0.39/0.57 (((~![W0: $i] : ((~aNaturalNumber0(W0)) | (~(sdtpldt0(xp, W0) = xk)))) | ((~aNaturalNumber0(sz00)) | (~(sdtpldt0(xp, sz00) = xk)))) <=> ((~![W0: $i] : ((~aNaturalNumber0(W0)) | (~(sdtpldt0(xp, W0) = xk)))) | (~aNaturalNumber0(sz00)) | (~(sdtpldt0(xp, sz00) = xk)))),
% 0.39/0.57 inference(rewrite,[status(thm)],[])).
% 0.39/0.57 tff(95,plain,
% 0.39/0.57 ((~![W0: $i] : ((~aNaturalNumber0(W0)) | (~(sdtpldt0(xp, W0) = xk)))) | ((~aNaturalNumber0(sz00)) | (~(sdtpldt0(xp, sz00) = xk)))),
% 0.39/0.57 inference(quant_inst,[status(thm)],[])).
% 0.39/0.57 tff(96,plain,
% 0.39/0.57 ((~![W0: $i] : ((~aNaturalNumber0(W0)) | (~(sdtpldt0(xp, W0) = xk)))) | (~aNaturalNumber0(sz00)) | (~(sdtpldt0(xp, sz00) = xk))),
% 0.39/0.57 inference(modus_ponens,[status(thm)],[95, 94])).
% 0.39/0.57 tff(97,plain,
% 0.39/0.57 (~(sdtpldt0(xp, sz00) = xk)),
% 0.39/0.57 inference(unit_resolution,[status(thm)],[96, 93, 90])).
% 0.39/0.57 tff(98,plain,
% 0.39/0.57 (~(xk = xp)),
% 0.39/0.57 inference(modus_ponens,[status(thm)],[97, 77])).
% 0.39/0.57 tff(99,plain,
% 0.39/0.57 (((xk = xp) | (~(sdtlseqdt0(xk, xp) | (~![W0: $i] : ((~aNaturalNumber0(W0)) | (~(sdtpldt0(xk, W0) = xp))))))) <=> ((xk = xp) | (~(sdtlseqdt0(xk, xp) | (~![W0: $i] : ((~aNaturalNumber0(W0)) | (~(sdtpldt0(xk, W0) = xp)))))))),
% 0.39/0.57 inference(rewrite,[status(thm)],[])).
% 0.39/0.57 tff(100,plain,
% 0.39/0.57 (((xk = xp) | (~(sdtlseqdt0(xk, xp) | (~![W0: $i] : ((~aNaturalNumber0(W0)) | (~(sdtpldt0(xk, W0) = xp))))))) <=> ((xk = xp) | (~(sdtlseqdt0(xk, xp) | (~![W0: $i] : ((~aNaturalNumber0(W0)) | (~(sdtpldt0(xk, W0) = xp)))))))),
% 0.39/0.57 inference(rewrite,[status(thm)],[])).
% 0.39/0.57 tff(101,plain,
% 0.39/0.57 (((~sdtlseqdt0(xk, xp)) & ![W0: $i] : ((~aNaturalNumber0(W0)) | (~(sdtpldt0(xk, W0) = xp)))) <=> (~(sdtlseqdt0(xk, xp) | (~![W0: $i] : ((~aNaturalNumber0(W0)) | (~(sdtpldt0(xk, W0) = xp))))))),
% 0.39/0.57 inference(rewrite,[status(thm)],[])).
% 0.39/0.57 tff(102,plain,
% 0.39/0.57 (^[W0: $i] : trans(monotonicity(rewrite((aNaturalNumber0(W0) & (sdtpldt0(xk, W0) = xp)) <=> (~((~aNaturalNumber0(W0)) | (~(sdtpldt0(xk, W0) = xp))))), ((~(aNaturalNumber0(W0) & (sdtpldt0(xk, W0) = xp))) <=> (~(~((~aNaturalNumber0(W0)) | (~(sdtpldt0(xk, W0) = xp))))))), rewrite((~(~((~aNaturalNumber0(W0)) | (~(sdtpldt0(xk, W0) = xp))))) <=> ((~aNaturalNumber0(W0)) | (~(sdtpldt0(xk, W0) = xp)))), ((~(aNaturalNumber0(W0) & (sdtpldt0(xk, W0) = xp))) <=> ((~aNaturalNumber0(W0)) | (~(sdtpldt0(xk, W0) = xp)))))),
% 0.39/0.57 inference(bind,[status(th)],[])).
% 0.39/0.57 tff(103,plain,
% 0.39/0.57 (![W0: $i] : (~(aNaturalNumber0(W0) & (sdtpldt0(xk, W0) = xp))) <=> ![W0: $i] : ((~aNaturalNumber0(W0)) | (~(sdtpldt0(xk, W0) = xp)))),
% 0.39/0.57 inference(quant_intro,[status(thm)],[102])).
% 0.39/0.57 tff(104,plain,
% 0.39/0.57 (((~sdtlseqdt0(xk, xp)) & ![W0: $i] : (~(aNaturalNumber0(W0) & (sdtpldt0(xk, W0) = xp)))) <=> ((~sdtlseqdt0(xk, xp)) & ![W0: $i] : ((~aNaturalNumber0(W0)) | (~(sdtpldt0(xk, W0) = xp))))),
% 0.39/0.57 inference(monotonicity,[status(thm)],[103])).
% 0.39/0.57 tff(105,plain,
% 0.39/0.57 (((~sdtlseqdt0(xk, xp)) & ![W0: $i] : (~(aNaturalNumber0(W0) & (sdtpldt0(xk, W0) = xp)))) <=> (~(sdtlseqdt0(xk, xp) | (~![W0: $i] : ((~aNaturalNumber0(W0)) | (~(sdtpldt0(xk, W0) = xp))))))),
% 0.39/0.57 inference(transitivity,[status(thm)],[104, 101])).
% 0.39/0.57 tff(106,plain,
% 0.39/0.57 (((xk = xp) | ((~sdtlseqdt0(xk, xp)) & ![W0: $i] : (~(aNaturalNumber0(W0) & (sdtpldt0(xk, W0) = xp))))) <=> ((xk = xp) | (~(sdtlseqdt0(xk, xp) | (~![W0: $i] : ((~aNaturalNumber0(W0)) | (~(sdtpldt0(xk, W0) = xp)))))))),
% 0.39/0.57 inference(monotonicity,[status(thm)],[105])).
% 0.39/0.57 tff(107,plain,
% 0.39/0.57 (((xk = xp) | ((~sdtlseqdt0(xk, xp)) & ![W0: $i] : (~(aNaturalNumber0(W0) & (sdtpldt0(xk, W0) = xp))))) <=> ((xk = xp) | (~(sdtlseqdt0(xk, xp) | (~![W0: $i] : ((~aNaturalNumber0(W0)) | (~(sdtpldt0(xk, W0) = xp)))))))),
% 0.39/0.57 inference(transitivity,[status(thm)],[106, 100])).
% 0.39/0.57 tff(108,plain,
% 0.39/0.57 (((~sdtlseqdt0(xk, xp)) & ![W0: $i] : (~(aNaturalNumber0(W0) & (sdtpldt0(xk, W0) = xp)))) <=> ((~sdtlseqdt0(xk, xp)) & ![W0: $i] : (~(aNaturalNumber0(W0) & (sdtpldt0(xk, W0) = xp))))),
% 0.39/0.57 inference(rewrite,[status(thm)],[])).
% 0.39/0.57 tff(109,plain,
% 0.39/0.57 (((xk = xp) | ((~sdtlseqdt0(xk, xp)) & ![W0: $i] : (~(aNaturalNumber0(W0) & (sdtpldt0(xk, W0) = xp))))) <=> ((xk = xp) | ((~sdtlseqdt0(xk, xp)) & ![W0: $i] : (~(aNaturalNumber0(W0) & (sdtpldt0(xk, W0) = xp)))))),
% 0.39/0.57 inference(monotonicity,[status(thm)],[108])).
% 0.39/0.57 tff(110,plain,
% 0.39/0.57 ((sdtlseqdt0(xk, xp) | ?[W0: $i] : (aNaturalNumber0(W0) & (sdtpldt0(xk, W0) = xp))) <=> (sdtlseqdt0(xk, xp) | ?[W0: $i] : (aNaturalNumber0(W0) & (sdtpldt0(xk, W0) = xp)))),
% 0.39/0.57 inference(rewrite,[status(thm)],[])).
% 0.39/0.57 tff(111,plain,
% 0.39/0.57 (((~(xk = xp)) & (sdtlseqdt0(xk, xp) | ?[W0: $i] : (aNaturalNumber0(W0) & (sdtpldt0(xk, W0) = xp)))) <=> ((~(xk = xp)) & (sdtlseqdt0(xk, xp) | ?[W0: $i] : (aNaturalNumber0(W0) & (sdtpldt0(xk, W0) = xp))))),
% 0.39/0.57 inference(monotonicity,[status(thm)],[110])).
% 0.39/0.57 tff(112,plain,
% 0.39/0.57 ((~((~(xk = xp)) & (sdtlseqdt0(xk, xp) | ?[W0: $i] : (aNaturalNumber0(W0) & (sdtpldt0(xk, W0) = xp))))) <=> (~((~(xk = xp)) & (sdtlseqdt0(xk, xp) | ?[W0: $i] : (aNaturalNumber0(W0) & (sdtpldt0(xk, W0) = xp)))))),
% 0.39/0.57 inference(monotonicity,[status(thm)],[111])).
% 0.39/0.57 tff(113,plain,
% 0.39/0.57 ((~((~(xk = xp)) & (sdtlseqdt0(xk, xp) | ?[W0: $i] : (aNaturalNumber0(W0) & (sdtpldt0(xk, W0) = xp))))) <=> (~((~(xk = xp)) & (sdtlseqdt0(xk, xp) | ?[W0: $i] : (aNaturalNumber0(W0) & (sdtpldt0(xk, W0) = xp)))))),
% 0.39/0.57 inference(rewrite,[status(thm)],[])).
% 0.39/0.57 tff(114,plain,
% 0.39/0.57 (~((~(xk = xp)) & (sdtlseqdt0(xk, xp) | ?[W0: $i] : (aNaturalNumber0(W0) & (sdtpldt0(xk, W0) = xp))))),
% 0.39/0.57 inference(or_elim,[status(thm)],[20])).
% 0.39/0.57 tff(115,plain,
% 0.39/0.57 (~((~(xk = xp)) & (sdtlseqdt0(xk, xp) | ?[W0: $i] : (aNaturalNumber0(W0) & (sdtpldt0(xk, W0) = xp))))),
% 0.39/0.57 inference(modus_ponens,[status(thm)],[114, 112])).
% 0.39/0.57 tff(116,plain,
% 0.39/0.57 (~((~(xk = xp)) & (sdtlseqdt0(xk, xp) | ?[W0: $i] : (aNaturalNumber0(W0) & (sdtpldt0(xk, W0) = xp))))),
% 0.39/0.57 inference(modus_ponens,[status(thm)],[115, 113])).
% 0.39/0.57 tff(117,plain,
% 0.39/0.57 (~((~(xk = xp)) & (sdtlseqdt0(xk, xp) | ?[W0: $i] : (aNaturalNumber0(W0) & (sdtpldt0(xk, W0) = xp))))),
% 0.39/0.57 inference(modus_ponens,[status(thm)],[116, 112])).
% 0.39/0.57 unexpected number of arguments: (let ((a!1 (refl (~ (not (sdtlseqdt0 xk xp)) (not (sdtlseqdt0 xk xp)))))
% 0.39/0.57 (a!2 (proof-bind (lambda ((W0 $i))
% 0.39/0.57 (let ((a!1 (not (and (aNaturalNumber0 W0)
% 0.39/0.57 (= (sdtpldt0 xk W0) xp)))))
% 0.39/0.57 (refl (~ a!1 a!1))))))
% 0.39/0.57 (a!3 (exists ((W0 $i)) (and (aNaturalNumber0 W0) (= (sdtpldt0 xk W0) xp))))
% 0.39/0.57 (a!4 (forall ((W0 $i))
% 0.39/0.57 (not (and (aNaturalNumber0 W0) (= (sdtpldt0 xk W0) xp))))))
% 0.39/0.57 (let ((a!5 (~ (not (or (sdtlseqdt0 xk xp) a!3))
% 0.39/0.57 (and (not (sdtlseqdt0 xk xp)) a!4)))
% 0.39/0.57 (a!7 (not (and (not (= xk xp)) (or (sdtlseqdt0 xk xp) a!3))))
% 0.39/0.57 (a!8 (or (= xk xp) (and (not (sdtlseqdt0 xk xp)) a!4))))
% 0.39/0.57 (let ((a!6 (nnf-neg a!1 (nnf-neg a!2 (~ (not a!3) a!4)) a!5)))
% 0.39/0.57 (nnf-neg (refl (~ (= xk xp) (= xk xp))) a!6 (~ a!7 a!8)))))
% 0.39/0.57 Proof display could not be completed: unexpected number of arguments
% 0.39/0.58 % E exiting
%------------------------------------------------------------------------------