%------------------------------------------------------------------------------
% File : Z3---4.15.1
% Problem : RNG090+2 : TPTP v9.0.0. Released v4.0.0.
% Transfm : none
% Format : tptp
% Command : run_E %s %d THM
% Computer : n003.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:24:10 AM UTC 2025
% Result : Theorem 162.95s 163.18s
% Output : Proof 162.95s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.08/0.12 % Problem : RNG090+2 : TPTP v9.0.0. Released v4.0.0.
% 0.08/0.12 % Command : run_E %s %d THM
% 0.11/0.33 % Computer : n003.cluster.edu
% 0.11/0.33 % Model : x86_64 x86_64
% 0.11/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.33 % Memory : 8042.1875MB
% 0.11/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.11/0.33 % CPULimit : 300
% 0.11/0.33 % WCLimit : 300
% 0.11/0.33 % DateTime : Fri Jun 20 03:19:39 EDT 2025
% 0.11/0.33 % CPUTime :
% 162.95/163.18 % SZS status Theorem
% 162.95/163.18 % SZS output start Proof
% 162.95/163.18 tff(sdtpldt0_type, type, (
% 162.95/163.18 sdtpldt0: ( $i * $i ) > $i)).
% 162.95/163.18 tff(xn_type, type, (
% 162.95/163.18 xn: $i)).
% 162.95/163.18 tff(xl_type, type, (
% 162.95/163.18 xl: $i)).
% 162.95/163.18 tff(xm_type, type, (
% 162.95/163.18 xm: $i)).
% 162.95/163.18 tff(xk_type, type, (
% 162.95/163.18 xk: $i)).
% 162.95/163.18 tff(xy_type, type, (
% 162.95/163.18 xy: $i)).
% 162.95/163.18 tff(xx_type, type, (
% 162.95/163.18 xx: $i)).
% 162.95/163.18 tff(aElement0_type, type, (
% 162.95/163.18 aElement0: $i > $o)).
% 162.95/163.18 tff(aElementOf0_type, type, (
% 162.95/163.18 aElementOf0: ( $i * $i ) > $o)).
% 162.95/163.18 tff(xJ_type, type, (
% 162.95/163.18 xJ: $i)).
% 162.95/163.18 tff(aSet0_type, type, (
% 162.95/163.18 aSet0: $i > $o)).
% 162.95/163.18 tff(aIdeal0_type, type, (
% 162.95/163.18 aIdeal0: $i > $o)).
% 162.95/163.18 tff(xI_type, type, (
% 162.95/163.18 xI: $i)).
% 162.95/163.18 tff(sdtasdt0_type, type, (
% 162.95/163.18 sdtasdt0: ( $i * $i ) > $i)).
% 162.95/163.18 tff(sz10_type, type, (
% 162.95/163.18 sz10: $i)).
% 162.95/163.18 tff(tptp_fun_W1_11_type, type, (
% 162.95/163.18 tptp_fun_W1_11: $i)).
% 162.95/163.18 tff(tptp_fun_W0_12_type, type, (
% 162.95/163.18 tptp_fun_W0_12: $i)).
% 162.95/163.18 tff(sdtpldt1_type, type, (
% 162.95/163.18 sdtpldt1: ( $i * $i ) > $i)).
% 162.95/163.18 tff(xz_type, type, (
% 162.95/163.18 xz: $i)).
% 162.95/163.18 tff(tptp_fun_W1_13_type, type, (
% 162.95/163.18 tptp_fun_W1_13: $i)).
% 162.95/163.18 tff(tptp_fun_W0_14_type, type, (
% 162.95/163.18 tptp_fun_W0_14: $i)).
% 162.95/163.18 tff(1,plain,
% 162.95/163.18 (aSet0(xJ) <=> aSet0(xJ)),
% 162.95/163.18 inference(rewrite,[status(thm)],[])).
% 162.95/163.18 tff(2,axiom,(((((aSet0(xI) & ![W0: $i] : (aElementOf0(W0, xI) => (![W1: $i] : (aElementOf0(W1, xI) => aElementOf0(sdtpldt0(W0, W1), xI)) & ![W1: $i] : (aElement0(W1) => aElementOf0(sdtasdt0(W1, W0), xI))))) & aIdeal0(xI)) & aSet0(xJ)) & ![W0: $i] : (aElementOf0(W0, xJ) => (![W1: $i] : (aElementOf0(W1, xJ) => aElementOf0(sdtpldt0(W0, W1), xJ)) & ![W1: $i] : (aElement0(W1) => aElementOf0(sdtasdt0(W1, W0), xJ))))) & aIdeal0(xJ)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','m__870')).
% 162.95/163.18 tff(3,plain,
% 162.95/163.18 ((((aSet0(xI) & ![W0: $i] : (aElementOf0(W0, xI) => (![W1: $i] : (aElementOf0(W1, xI) => aElementOf0(sdtpldt0(W0, W1), xI)) & ![W1: $i] : (aElement0(W1) => aElementOf0(sdtasdt0(W1, W0), xI))))) & aIdeal0(xI)) & aSet0(xJ)) & ![W0: $i] : (aElementOf0(W0, xJ) => (![W1: $i] : (aElementOf0(W1, xJ) => aElementOf0(sdtpldt0(W0, W1), xJ)) & ![W1: $i] : (aElement0(W1) => aElementOf0(sdtasdt0(W1, W0), xJ))))),
% 162.95/163.18 inference(and_elim,[status(thm)],[2])).
% 162.95/163.18 tff(4,plain,
% 162.95/163.18 (((aSet0(xI) & ![W0: $i] : (aElementOf0(W0, xI) => (![W1: $i] : (aElementOf0(W1, xI) => aElementOf0(sdtpldt0(W0, W1), xI)) & ![W1: $i] : (aElement0(W1) => aElementOf0(sdtasdt0(W1, W0), xI))))) & aIdeal0(xI)) & aSet0(xJ)),
% 162.95/163.18 inference(and_elim,[status(thm)],[3])).
% 162.95/163.18 tff(5,plain,
% 162.95/163.18 (aSet0(xJ)),
% 162.95/163.18 inference(and_elim,[status(thm)],[4])).
% 162.95/163.18 tff(6,plain,
% 162.95/163.18 (aSet0(xJ)),
% 162.95/163.18 inference(modus_ponens,[status(thm)],[5, 1])).
% 162.95/163.18 tff(7,plain,
% 162.95/163.18 (^[W0: $i] : refl(((~aSet0(W0)) | ![W1: $i] : (aElement0(W1) | (~aElementOf0(W1, W0)))) <=> ((~aSet0(W0)) | ![W1: $i] : (aElement0(W1) | (~aElementOf0(W1, W0)))))),
% 162.95/163.18 inference(bind,[status(th)],[])).
% 162.95/163.18 tff(8,plain,
% 162.95/163.18 (![W0: $i] : ((~aSet0(W0)) | ![W1: $i] : (aElement0(W1) | (~aElementOf0(W1, W0)))) <=> ![W0: $i] : ((~aSet0(W0)) | ![W1: $i] : (aElement0(W1) | (~aElementOf0(W1, W0))))),
% 162.95/163.18 inference(quant_intro,[status(thm)],[7])).
% 162.95/163.18 tff(9,plain,
% 162.95/163.18 (^[W0: $i] : rewrite(((~aSet0(W0)) | ![W1: $i] : (aElement0(W1) | (~aElementOf0(W1, W0)))) <=> ((~aSet0(W0)) | ![W1: $i] : (aElement0(W1) | (~aElementOf0(W1, W0)))))),
% 162.95/163.18 inference(bind,[status(th)],[])).
% 162.95/163.18 tff(10,plain,
% 162.95/163.18 (![W0: $i] : ((~aSet0(W0)) | ![W1: $i] : (aElement0(W1) | (~aElementOf0(W1, W0)))) <=> ![W0: $i] : ((~aSet0(W0)) | ![W1: $i] : (aElement0(W1) | (~aElementOf0(W1, W0))))),
% 162.95/163.18 inference(quant_intro,[status(thm)],[9])).
% 162.95/163.18 tff(11,plain,
% 162.95/163.18 (![W0: $i] : ((~aSet0(W0)) | ![W1: $i] : (aElement0(W1) | (~aElementOf0(W1, W0)))) <=> ![W0: $i] : ((~aSet0(W0)) | ![W1: $i] : (aElement0(W1) | (~aElementOf0(W1, W0))))),
% 162.95/163.18 inference(transitivity,[status(thm)],[10, 8])).
% 162.95/163.18 tff(12,plain,
% 162.95/163.18 (![W0: $i] : ((~aSet0(W0)) | ![W1: $i] : (aElement0(W1) | (~aElementOf0(W1, W0)))) <=> ![W0: $i] : ((~aSet0(W0)) | ![W1: $i] : (aElement0(W1) | (~aElementOf0(W1, W0))))),
% 162.95/163.18 inference(rewrite,[status(thm)],[])).
% 162.95/163.18 tff(13,plain,
% 162.95/163.18 (^[W0: $i] : trans(monotonicity(quant_intro(proof_bind(^[W1: $i] : rewrite((aElementOf0(W1, W0) => aElement0(W1)) <=> (aElement0(W1) | (~aElementOf0(W1, W0))))), (![W1: $i] : (aElementOf0(W1, W0) => aElement0(W1)) <=> ![W1: $i] : (aElement0(W1) | (~aElementOf0(W1, W0))))), ((aSet0(W0) => ![W1: $i] : (aElementOf0(W1, W0) => aElement0(W1))) <=> (aSet0(W0) => ![W1: $i] : (aElement0(W1) | (~aElementOf0(W1, W0)))))), rewrite((aSet0(W0) => ![W1: $i] : (aElement0(W1) | (~aElementOf0(W1, W0)))) <=> ((~aSet0(W0)) | ![W1: $i] : (aElement0(W1) | (~aElementOf0(W1, W0))))), ((aSet0(W0) => ![W1: $i] : (aElementOf0(W1, W0) => aElement0(W1))) <=> ((~aSet0(W0)) | ![W1: $i] : (aElement0(W1) | (~aElementOf0(W1, W0))))))),
% 162.95/163.18 inference(bind,[status(th)],[])).
% 162.95/163.18 tff(14,plain,
% 162.95/163.18 (![W0: $i] : (aSet0(W0) => ![W1: $i] : (aElementOf0(W1, W0) => aElement0(W1))) <=> ![W0: $i] : ((~aSet0(W0)) | ![W1: $i] : (aElement0(W1) | (~aElementOf0(W1, W0))))),
% 162.95/163.18 inference(quant_intro,[status(thm)],[13])).
% 162.95/163.18 tff(15,axiom,(![W0: $i] : (aSet0(W0) => ![W1: $i] : (aElementOf0(W1, W0) => aElement0(W1)))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','mEOfElem')).
% 162.95/163.18 tff(16,plain,
% 162.95/163.18 (![W0: $i] : ((~aSet0(W0)) | ![W1: $i] : (aElement0(W1) | (~aElementOf0(W1, W0))))),
% 162.95/163.18 inference(modus_ponens,[status(thm)],[15, 14])).
% 162.95/163.18 tff(17,plain,
% 162.95/163.18 (![W0: $i] : ((~aSet0(W0)) | ![W1: $i] : (aElement0(W1) | (~aElementOf0(W1, W0))))),
% 162.95/163.18 inference(modus_ponens,[status(thm)],[16, 12])).
% 162.95/163.18 tff(18,plain,(
% 162.95/163.18 ![W0: $i] : ((~aSet0(W0)) | ![W1: $i] : (aElement0(W1) | (~aElementOf0(W1, W0))))),
% 162.95/163.18 inference(skolemize,[status(sab)],[17])).
% 162.95/163.18 tff(19,plain,
% 162.95/163.18 (![W0: $i] : ((~aSet0(W0)) | ![W1: $i] : (aElement0(W1) | (~aElementOf0(W1, W0))))),
% 162.95/163.18 inference(modus_ponens,[status(thm)],[18, 11])).
% 162.95/163.18 tff(20,plain,
% 162.95/163.18 (((~![W0: $i] : ((~aSet0(W0)) | ![W1: $i] : (aElement0(W1) | (~aElementOf0(W1, W0))))) | ((~aSet0(xJ)) | ![W1: $i] : (aElement0(W1) | (~aElementOf0(W1, xJ))))) <=> ((~![W0: $i] : ((~aSet0(W0)) | ![W1: $i] : (aElement0(W1) | (~aElementOf0(W1, W0))))) | (~aSet0(xJ)) | ![W1: $i] : (aElement0(W1) | (~aElementOf0(W1, xJ))))),
% 162.95/163.18 inference(rewrite,[status(thm)],[])).
% 162.95/163.18 tff(21,plain,
% 162.95/163.18 ((~![W0: $i] : ((~aSet0(W0)) | ![W1: $i] : (aElement0(W1) | (~aElementOf0(W1, W0))))) | ((~aSet0(xJ)) | ![W1: $i] : (aElement0(W1) | (~aElementOf0(W1, xJ))))),
% 162.95/163.18 inference(quant_inst,[status(thm)],[])).
% 162.95/163.18 tff(22,plain,
% 162.95/163.18 ((~![W0: $i] : ((~aSet0(W0)) | ![W1: $i] : (aElement0(W1) | (~aElementOf0(W1, W0))))) | (~aSet0(xJ)) | ![W1: $i] : (aElement0(W1) | (~aElementOf0(W1, xJ)))),
% 162.95/163.18 inference(modus_ponens,[status(thm)],[21, 20])).
% 162.95/163.18 tff(23,plain,
% 162.95/163.18 (![W1: $i] : (aElement0(W1) | (~aElementOf0(W1, xJ)))),
% 162.95/163.18 inference(unit_resolution,[status(thm)],[22, 19, 6])).
% 162.95/163.18 tff(24,plain,
% 162.95/163.18 (aElementOf0(xl, xJ) <=> aElementOf0(xl, xJ)),
% 162.95/163.18 inference(rewrite,[status(thm)],[])).
% 162.95/163.18 tff(25,axiom,((aElementOf0(xk, xI) & aElementOf0(xl, xJ)) & (xx = sdtpldt0(xk, xl))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','m__934')).
% 162.95/163.18 tff(26,plain,
% 162.95/163.18 (aElementOf0(xk, xI) & aElementOf0(xl, xJ)),
% 162.95/163.18 inference(and_elim,[status(thm)],[25])).
% 162.95/163.18 tff(27,plain,
% 162.95/163.18 (aElementOf0(xl, xJ)),
% 162.95/163.18 inference(and_elim,[status(thm)],[26])).
% 162.95/163.18 tff(28,plain,
% 162.95/163.18 (aElementOf0(xl, xJ)),
% 162.95/163.18 inference(modus_ponens,[status(thm)],[27, 24])).
% 162.95/163.18 tff(29,plain,
% 162.95/163.18 (((~![W1: $i] : (aElement0(W1) | (~aElementOf0(W1, xJ)))) | (aElement0(xl) | (~aElementOf0(xl, xJ)))) <=> ((~![W1: $i] : (aElement0(W1) | (~aElementOf0(W1, xJ)))) | aElement0(xl) | (~aElementOf0(xl, xJ)))),
% 162.95/163.18 inference(rewrite,[status(thm)],[])).
% 162.95/163.18 tff(30,plain,
% 162.95/163.18 ((~![W1: $i] : (aElement0(W1) | (~aElementOf0(W1, xJ)))) | (aElement0(xl) | (~aElementOf0(xl, xJ)))),
% 162.95/163.18 inference(quant_inst,[status(thm)],[])).
% 162.95/163.18 tff(31,plain,
% 162.95/163.18 ((~![W1: $i] : (aElement0(W1) | (~aElementOf0(W1, xJ)))) | aElement0(xl) | (~aElementOf0(xl, xJ))),
% 162.95/163.18 inference(modus_ponens,[status(thm)],[30, 29])).
% 162.95/163.18 tff(32,plain,
% 162.95/163.18 (aElement0(xl)),
% 162.95/163.18 inference(unit_resolution,[status(thm)],[31, 28, 23])).
% 162.95/163.18 tff(33,plain,
% 162.95/163.18 (aSet0(xI) <=> aSet0(xI)),
% 162.95/163.18 inference(rewrite,[status(thm)],[])).
% 162.95/163.18 tff(34,plain,
% 162.95/163.18 ((aSet0(xI) & ![W0: $i] : (aElementOf0(W0, xI) => (![W1: $i] : (aElementOf0(W1, xI) => aElementOf0(sdtpldt0(W0, W1), xI)) & ![W1: $i] : (aElement0(W1) => aElementOf0(sdtasdt0(W1, W0), xI))))) & aIdeal0(xI)),
% 162.95/163.18 inference(and_elim,[status(thm)],[4])).
% 162.95/163.18 tff(35,plain,
% 162.95/163.18 (aSet0(xI) & ![W0: $i] : (aElementOf0(W0, xI) => (![W1: $i] : (aElementOf0(W1, xI) => aElementOf0(sdtpldt0(W0, W1), xI)) & ![W1: $i] : (aElement0(W1) => aElementOf0(sdtasdt0(W1, W0), xI))))),
% 162.95/163.18 inference(and_elim,[status(thm)],[34])).
% 162.95/163.18 tff(36,plain,
% 162.95/163.18 (aSet0(xI)),
% 162.95/163.18 inference(and_elim,[status(thm)],[35])).
% 162.95/163.18 tff(37,plain,
% 162.95/163.18 (aSet0(xI)),
% 162.95/163.18 inference(modus_ponens,[status(thm)],[36, 33])).
% 162.95/163.18 tff(38,plain,
% 162.95/163.18 (((~![W0: $i] : ((~aSet0(W0)) | ![W1: $i] : (aElement0(W1) | (~aElementOf0(W1, W0))))) | ((~aSet0(xI)) | ![W1: $i] : (aElement0(W1) | (~aElementOf0(W1, xI))))) <=> ((~![W0: $i] : ((~aSet0(W0)) | ![W1: $i] : (aElement0(W1) | (~aElementOf0(W1, W0))))) | (~aSet0(xI)) | ![W1: $i] : (aElement0(W1) | (~aElementOf0(W1, xI))))),
% 162.95/163.18 inference(rewrite,[status(thm)],[])).
% 162.95/163.18 tff(39,plain,
% 162.95/163.18 ((~![W0: $i] : ((~aSet0(W0)) | ![W1: $i] : (aElement0(W1) | (~aElementOf0(W1, W0))))) | ((~aSet0(xI)) | ![W1: $i] : (aElement0(W1) | (~aElementOf0(W1, xI))))),
% 162.95/163.18 inference(quant_inst,[status(thm)],[])).
% 162.95/163.18 tff(40,plain,
% 162.95/163.18 ((~![W0: $i] : ((~aSet0(W0)) | ![W1: $i] : (aElement0(W1) | (~aElementOf0(W1, W0))))) | (~aSet0(xI)) | ![W1: $i] : (aElement0(W1) | (~aElementOf0(W1, xI)))),
% 162.95/163.18 inference(modus_ponens,[status(thm)],[39, 38])).
% 162.95/163.18 tff(41,plain,
% 162.95/163.18 (![W1: $i] : (aElement0(W1) | (~aElementOf0(W1, xI)))),
% 162.95/163.18 inference(unit_resolution,[status(thm)],[40, 19, 37])).
% 162.95/163.18 tff(42,plain,
% 162.95/163.18 (aElementOf0(sdtpldt0(xk, xm), xI) <=> aElementOf0(sdtpldt0(xk, xm), xI)),
% 162.95/163.18 inference(rewrite,[status(thm)],[])).
% 162.95/163.18 tff(43,axiom,(aElementOf0(sdtpldt0(xk, xm), xI) & aElementOf0(sdtpldt0(xl, xn), xJ)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','m__994')).
% 162.95/163.18 tff(44,plain,
% 162.95/163.18 (aElementOf0(sdtpldt0(xk, xm), xI)),
% 162.95/163.18 inference(and_elim,[status(thm)],[43])).
% 162.95/163.18 tff(45,plain,
% 162.95/163.18 (aElementOf0(sdtpldt0(xk, xm), xI)),
% 162.95/163.18 inference(modus_ponens,[status(thm)],[44, 42])).
% 162.95/163.18 tff(46,plain,
% 162.95/163.18 (((~![W1: $i] : (aElement0(W1) | (~aElementOf0(W1, xI)))) | (aElement0(sdtpldt0(xk, xm)) | (~aElementOf0(sdtpldt0(xk, xm), xI)))) <=> ((~![W1: $i] : (aElement0(W1) | (~aElementOf0(W1, xI)))) | aElement0(sdtpldt0(xk, xm)) | (~aElementOf0(sdtpldt0(xk, xm), xI)))),
% 162.95/163.18 inference(rewrite,[status(thm)],[])).
% 162.95/163.18 tff(47,plain,
% 162.95/163.18 ((~![W1: $i] : (aElement0(W1) | (~aElementOf0(W1, xI)))) | (aElement0(sdtpldt0(xk, xm)) | (~aElementOf0(sdtpldt0(xk, xm), xI)))),
% 162.95/163.18 inference(quant_inst,[status(thm)],[])).
% 162.95/163.18 tff(48,plain,
% 162.95/163.18 ((~![W1: $i] : (aElement0(W1) | (~aElementOf0(W1, xI)))) | aElement0(sdtpldt0(xk, xm)) | (~aElementOf0(sdtpldt0(xk, xm), xI))),
% 162.95/163.18 inference(modus_ponens,[status(thm)],[47, 46])).
% 162.95/163.18 tff(49,plain,
% 162.95/163.18 (aElement0(sdtpldt0(xk, xm))),
% 162.95/163.18 inference(unit_resolution,[status(thm)],[48, 45, 41])).
% 162.95/163.18 tff(50,plain,
% 162.95/163.18 (aElementOf0(xn, xJ) <=> aElementOf0(xn, xJ)),
% 162.95/163.18 inference(rewrite,[status(thm)],[])).
% 162.95/163.18 tff(51,axiom,((aElementOf0(xm, xI) & aElementOf0(xn, xJ)) & (xy = sdtpldt0(xm, xn))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','m__967')).
% 162.95/163.18 tff(52,plain,
% 162.95/163.18 (aElementOf0(xm, xI) & aElementOf0(xn, xJ)),
% 162.95/163.18 inference(and_elim,[status(thm)],[51])).
% 162.95/163.18 tff(53,plain,
% 162.95/163.18 (aElementOf0(xn, xJ)),
% 162.95/163.18 inference(and_elim,[status(thm)],[52])).
% 162.95/163.18 tff(54,plain,
% 162.95/163.18 (aElementOf0(xn, xJ)),
% 162.95/163.18 inference(modus_ponens,[status(thm)],[53, 50])).
% 162.95/163.18 tff(55,plain,
% 162.95/163.18 (((~![W1: $i] : (aElement0(W1) | (~aElementOf0(W1, xJ)))) | (aElement0(xn) | (~aElementOf0(xn, xJ)))) <=> ((~![W1: $i] : (aElement0(W1) | (~aElementOf0(W1, xJ)))) | aElement0(xn) | (~aElementOf0(xn, xJ)))),
% 162.95/163.18 inference(rewrite,[status(thm)],[])).
% 162.95/163.18 tff(56,plain,
% 162.95/163.18 ((~![W1: $i] : (aElement0(W1) | (~aElementOf0(W1, xJ)))) | (aElement0(xn) | (~aElementOf0(xn, xJ)))),
% 162.95/163.18 inference(quant_inst,[status(thm)],[])).
% 162.95/163.18 tff(57,plain,
% 162.95/163.18 ((~![W1: $i] : (aElement0(W1) | (~aElementOf0(W1, xJ)))) | aElement0(xn) | (~aElementOf0(xn, xJ))),
% 162.95/163.18 inference(modus_ponens,[status(thm)],[56, 55])).
% 162.95/163.18 tff(58,plain,
% 162.95/163.18 (aElement0(xn)),
% 162.95/163.18 inference(unit_resolution,[status(thm)],[57, 54, 23])).
% 162.95/163.18 tff(59,plain,
% 162.95/163.18 (^[W0: $i, W1: $i, W2: $i] : refl(((sdtpldt0(sdtpldt0(W0, W1), W2) = sdtpldt0(W0, sdtpldt0(W1, W2))) | (~aElement0(W2)) | (~aElement0(W1)) | (~aElement0(W0))) <=> ((sdtpldt0(sdtpldt0(W0, W1), W2) = sdtpldt0(W0, sdtpldt0(W1, W2))) | (~aElement0(W2)) | (~aElement0(W1)) | (~aElement0(W0))))),
% 162.95/163.18 inference(bind,[status(th)],[])).
% 162.95/163.18 tff(60,plain,
% 162.95/163.18 (![W0: $i, W1: $i, W2: $i] : ((sdtpldt0(sdtpldt0(W0, W1), W2) = sdtpldt0(W0, sdtpldt0(W1, W2))) | (~aElement0(W2)) | (~aElement0(W1)) | (~aElement0(W0))) <=> ![W0: $i, W1: $i, W2: $i] : ((sdtpldt0(sdtpldt0(W0, W1), W2) = sdtpldt0(W0, sdtpldt0(W1, W2))) | (~aElement0(W2)) | (~aElement0(W1)) | (~aElement0(W0)))),
% 162.95/163.18 inference(quant_intro,[status(thm)],[59])).
% 162.95/163.18 tff(61,plain,
% 162.95/163.18 (^[W0: $i, W1: $i, W2: $i] : trans(monotonicity(trans(monotonicity(rewrite((aElement0(W0) & aElement0(W1) & aElement0(W2)) <=> (~((~aElement0(W2)) | (~aElement0(W1)) | (~aElement0(W0))))), ((~(aElement0(W0) & aElement0(W1) & aElement0(W2))) <=> (~(~((~aElement0(W2)) | (~aElement0(W1)) | (~aElement0(W0))))))), rewrite((~(~((~aElement0(W2)) | (~aElement0(W1)) | (~aElement0(W0))))) <=> ((~aElement0(W2)) | (~aElement0(W1)) | (~aElement0(W0)))), ((~(aElement0(W0) & aElement0(W1) & aElement0(W2))) <=> ((~aElement0(W2)) | (~aElement0(W1)) | (~aElement0(W0))))), (((~(aElement0(W0) & aElement0(W1) & aElement0(W2))) | (sdtpldt0(sdtpldt0(W0, W1), W2) = sdtpldt0(W0, sdtpldt0(W1, W2)))) <=> (((~aElement0(W2)) | (~aElement0(W1)) | (~aElement0(W0))) | (sdtpldt0(sdtpldt0(W0, W1), W2) = sdtpldt0(W0, sdtpldt0(W1, W2)))))), rewrite((((~aElement0(W2)) | (~aElement0(W1)) | (~aElement0(W0))) | (sdtpldt0(sdtpldt0(W0, W1), W2) = sdtpldt0(W0, sdtpldt0(W1, W2)))) <=> ((sdtpldt0(sdtpldt0(W0, W1), W2) = sdtpldt0(W0, sdtpldt0(W1, W2))) | (~aElement0(W2)) | (~aElement0(W1)) | (~aElement0(W0)))), (((~(aElement0(W0) & aElement0(W1) & aElement0(W2))) | (sdtpldt0(sdtpldt0(W0, W1), W2) = sdtpldt0(W0, sdtpldt0(W1, W2)))) <=> ((sdtpldt0(sdtpldt0(W0, W1), W2) = sdtpldt0(W0, sdtpldt0(W1, W2))) | (~aElement0(W2)) | (~aElement0(W1)) | (~aElement0(W0)))))),
% 162.95/163.18 inference(bind,[status(th)],[])).
% 162.95/163.18 tff(62,plain,
% 162.95/163.18 (![W0: $i, W1: $i, W2: $i] : ((~(aElement0(W0) & aElement0(W1) & aElement0(W2))) | (sdtpldt0(sdtpldt0(W0, W1), W2) = sdtpldt0(W0, sdtpldt0(W1, W2)))) <=> ![W0: $i, W1: $i, W2: $i] : ((sdtpldt0(sdtpldt0(W0, W1), W2) = sdtpldt0(W0, sdtpldt0(W1, W2))) | (~aElement0(W2)) | (~aElement0(W1)) | (~aElement0(W0)))),
% 162.95/163.18 inference(quant_intro,[status(thm)],[61])).
% 162.95/163.18 tff(63,plain,
% 162.95/163.18 (![W0: $i, W1: $i, W2: $i] : ((~(aElement0(W0) & aElement0(W1) & aElement0(W2))) | (sdtpldt0(sdtpldt0(W0, W1), W2) = sdtpldt0(W0, sdtpldt0(W1, W2)))) <=> ![W0: $i, W1: $i, W2: $i] : ((~(aElement0(W0) & aElement0(W1) & aElement0(W2))) | (sdtpldt0(sdtpldt0(W0, W1), W2) = sdtpldt0(W0, sdtpldt0(W1, W2))))),
% 162.95/163.18 inference(rewrite,[status(thm)],[])).
% 162.95/163.18 tff(64,plain,
% 162.95/163.18 (^[W0: $i, W1: $i, W2: $i] : trans(monotonicity(rewrite(((aElement0(W0) & aElement0(W1)) & aElement0(W2)) <=> (aElement0(W0) & aElement0(W1) & aElement0(W2))), ((((aElement0(W0) & aElement0(W1)) & aElement0(W2)) => (sdtpldt0(sdtpldt0(W0, W1), W2) = sdtpldt0(W0, sdtpldt0(W1, W2)))) <=> ((aElement0(W0) & aElement0(W1) & aElement0(W2)) => (sdtpldt0(sdtpldt0(W0, W1), W2) = sdtpldt0(W0, sdtpldt0(W1, W2)))))), rewrite(((aElement0(W0) & aElement0(W1) & aElement0(W2)) => (sdtpldt0(sdtpldt0(W0, W1), W2) = sdtpldt0(W0, sdtpldt0(W1, W2)))) <=> ((~(aElement0(W0) & aElement0(W1) & aElement0(W2))) | (sdtpldt0(sdtpldt0(W0, W1), W2) = sdtpldt0(W0, sdtpldt0(W1, W2))))), ((((aElement0(W0) & aElement0(W1)) & aElement0(W2)) => (sdtpldt0(sdtpldt0(W0, W1), W2) = sdtpldt0(W0, sdtpldt0(W1, W2)))) <=> ((~(aElement0(W0) & aElement0(W1) & aElement0(W2))) | (sdtpldt0(sdtpldt0(W0, W1), W2) = sdtpldt0(W0, sdtpldt0(W1, W2))))))),
% 162.95/163.19 inference(bind,[status(th)],[])).
% 162.95/163.19 tff(65,plain,
% 162.95/163.19 (![W0: $i, W1: $i, W2: $i] : (((aElement0(W0) & aElement0(W1)) & aElement0(W2)) => (sdtpldt0(sdtpldt0(W0, W1), W2) = sdtpldt0(W0, sdtpldt0(W1, W2)))) <=> ![W0: $i, W1: $i, W2: $i] : ((~(aElement0(W0) & aElement0(W1) & aElement0(W2))) | (sdtpldt0(sdtpldt0(W0, W1), W2) = sdtpldt0(W0, sdtpldt0(W1, W2))))),
% 162.95/163.19 inference(quant_intro,[status(thm)],[64])).
% 162.95/163.19 tff(66,axiom,(![W0: $i, W1: $i, W2: $i] : (((aElement0(W0) & aElement0(W1)) & aElement0(W2)) => (sdtpldt0(sdtpldt0(W0, W1), W2) = sdtpldt0(W0, sdtpldt0(W1, W2))))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','mAddAsso')).
% 162.95/163.19 tff(67,plain,
% 162.95/163.19 (![W0: $i, W1: $i, W2: $i] : ((~(aElement0(W0) & aElement0(W1) & aElement0(W2))) | (sdtpldt0(sdtpldt0(W0, W1), W2) = sdtpldt0(W0, sdtpldt0(W1, W2))))),
% 162.95/163.19 inference(modus_ponens,[status(thm)],[66, 65])).
% 162.95/163.19 tff(68,plain,
% 162.95/163.19 (![W0: $i, W1: $i, W2: $i] : ((~(aElement0(W0) & aElement0(W1) & aElement0(W2))) | (sdtpldt0(sdtpldt0(W0, W1), W2) = sdtpldt0(W0, sdtpldt0(W1, W2))))),
% 162.95/163.19 inference(modus_ponens,[status(thm)],[67, 63])).
% 162.95/163.19 tff(69,plain,(
% 162.95/163.19 ![W0: $i, W1: $i, W2: $i] : ((~(aElement0(W0) & aElement0(W1) & aElement0(W2))) | (sdtpldt0(sdtpldt0(W0, W1), W2) = sdtpldt0(W0, sdtpldt0(W1, W2))))),
% 162.95/163.19 inference(skolemize,[status(sab)],[68])).
% 162.95/163.19 tff(70,plain,
% 162.95/163.19 (![W0: $i, W1: $i, W2: $i] : ((sdtpldt0(sdtpldt0(W0, W1), W2) = sdtpldt0(W0, sdtpldt0(W1, W2))) | (~aElement0(W2)) | (~aElement0(W1)) | (~aElement0(W0)))),
% 162.95/163.19 inference(modus_ponens,[status(thm)],[69, 62])).
% 162.95/163.19 tff(71,plain,
% 162.95/163.19 (![W0: $i, W1: $i, W2: $i] : ((sdtpldt0(sdtpldt0(W0, W1), W2) = sdtpldt0(W0, sdtpldt0(W1, W2))) | (~aElement0(W2)) | (~aElement0(W1)) | (~aElement0(W0)))),
% 162.95/163.19 inference(modus_ponens,[status(thm)],[70, 60])).
% 162.95/163.19 tff(72,plain,
% 162.95/163.19 (((~![W0: $i, W1: $i, W2: $i] : ((sdtpldt0(sdtpldt0(W0, W1), W2) = sdtpldt0(W0, sdtpldt0(W1, W2))) | (~aElement0(W2)) | (~aElement0(W1)) | (~aElement0(W0)))) | ((~aElement0(xl)) | (~aElement0(xn)) | (sdtpldt0(sdtpldt0(sdtpldt0(xk, xm), xl), xn) = sdtpldt0(sdtpldt0(xk, xm), sdtpldt0(xl, xn))) | (~aElement0(sdtpldt0(xk, xm))))) <=> ((~![W0: $i, W1: $i, W2: $i] : ((sdtpldt0(sdtpldt0(W0, W1), W2) = sdtpldt0(W0, sdtpldt0(W1, W2))) | (~aElement0(W2)) | (~aElement0(W1)) | (~aElement0(W0)))) | (~aElement0(xl)) | (~aElement0(xn)) | (sdtpldt0(sdtpldt0(sdtpldt0(xk, xm), xl), xn) = sdtpldt0(sdtpldt0(xk, xm), sdtpldt0(xl, xn))) | (~aElement0(sdtpldt0(xk, xm))))),
% 162.95/163.19 inference(rewrite,[status(thm)],[])).
% 162.95/163.19 tff(73,plain,
% 162.95/163.19 (((sdtpldt0(sdtpldt0(sdtpldt0(xk, xm), xl), xn) = sdtpldt0(sdtpldt0(xk, xm), sdtpldt0(xl, xn))) | (~aElement0(xn)) | (~aElement0(xl)) | (~aElement0(sdtpldt0(xk, xm)))) <=> ((~aElement0(xl)) | (~aElement0(xn)) | (sdtpldt0(sdtpldt0(sdtpldt0(xk, xm), xl), xn) = sdtpldt0(sdtpldt0(xk, xm), sdtpldt0(xl, xn))) | (~aElement0(sdtpldt0(xk, xm))))),
% 162.95/163.19 inference(rewrite,[status(thm)],[])).
% 162.95/163.19 tff(74,plain,
% 162.95/163.19 (((~![W0: $i, W1: $i, W2: $i] : ((sdtpldt0(sdtpldt0(W0, W1), W2) = sdtpldt0(W0, sdtpldt0(W1, W2))) | (~aElement0(W2)) | (~aElement0(W1)) | (~aElement0(W0)))) | ((sdtpldt0(sdtpldt0(sdtpldt0(xk, xm), xl), xn) = sdtpldt0(sdtpldt0(xk, xm), sdtpldt0(xl, xn))) | (~aElement0(xn)) | (~aElement0(xl)) | (~aElement0(sdtpldt0(xk, xm))))) <=> ((~![W0: $i, W1: $i, W2: $i] : ((sdtpldt0(sdtpldt0(W0, W1), W2) = sdtpldt0(W0, sdtpldt0(W1, W2))) | (~aElement0(W2)) | (~aElement0(W1)) | (~aElement0(W0)))) | ((~aElement0(xl)) | (~aElement0(xn)) | (sdtpldt0(sdtpldt0(sdtpldt0(xk, xm), xl), xn) = sdtpldt0(sdtpldt0(xk, xm), sdtpldt0(xl, xn))) | (~aElement0(sdtpldt0(xk, xm)))))),
% 162.95/163.19 inference(monotonicity,[status(thm)],[73])).
% 162.95/163.19 tff(75,plain,
% 162.95/163.19 (((~![W0: $i, W1: $i, W2: $i] : ((sdtpldt0(sdtpldt0(W0, W1), W2) = sdtpldt0(W0, sdtpldt0(W1, W2))) | (~aElement0(W2)) | (~aElement0(W1)) | (~aElement0(W0)))) | ((sdtpldt0(sdtpldt0(sdtpldt0(xk, xm), xl), xn) = sdtpldt0(sdtpldt0(xk, xm), sdtpldt0(xl, xn))) | (~aElement0(xn)) | (~aElement0(xl)) | (~aElement0(sdtpldt0(xk, xm))))) <=> ((~![W0: $i, W1: $i, W2: $i] : ((sdtpldt0(sdtpldt0(W0, W1), W2) = sdtpldt0(W0, sdtpldt0(W1, W2))) | (~aElement0(W2)) | (~aElement0(W1)) | (~aElement0(W0)))) | (~aElement0(xl)) | (~aElement0(xn)) | (sdtpldt0(sdtpldt0(sdtpldt0(xk, xm), xl), xn) = sdtpldt0(sdtpldt0(xk, xm), sdtpldt0(xl, xn))) | (~aElement0(sdtpldt0(xk, xm))))),
% 162.95/163.19 inference(transitivity,[status(thm)],[74, 72])).
% 162.95/163.19 tff(76,plain,
% 162.95/163.19 ((~![W0: $i, W1: $i, W2: $i] : ((sdtpldt0(sdtpldt0(W0, W1), W2) = sdtpldt0(W0, sdtpldt0(W1, W2))) | (~aElement0(W2)) | (~aElement0(W1)) | (~aElement0(W0)))) | ((sdtpldt0(sdtpldt0(sdtpldt0(xk, xm), xl), xn) = sdtpldt0(sdtpldt0(xk, xm), sdtpldt0(xl, xn))) | (~aElement0(xn)) | (~aElement0(xl)) | (~aElement0(sdtpldt0(xk, xm))))),
% 162.95/163.19 inference(quant_inst,[status(thm)],[])).
% 162.95/163.19 tff(77,plain,
% 162.95/163.19 ((~![W0: $i, W1: $i, W2: $i] : ((sdtpldt0(sdtpldt0(W0, W1), W2) = sdtpldt0(W0, sdtpldt0(W1, W2))) | (~aElement0(W2)) | (~aElement0(W1)) | (~aElement0(W0)))) | (~aElement0(xl)) | (~aElement0(xn)) | (sdtpldt0(sdtpldt0(sdtpldt0(xk, xm), xl), xn) = sdtpldt0(sdtpldt0(xk, xm), sdtpldt0(xl, xn))) | (~aElement0(sdtpldt0(xk, xm)))),
% 162.95/163.19 inference(modus_ponens,[status(thm)],[76, 75])).
% 162.95/163.19 tff(78,plain,
% 162.95/163.19 ((~aElement0(xl)) | (~aElement0(xn)) | (sdtpldt0(sdtpldt0(sdtpldt0(xk, xm), xl), xn) = sdtpldt0(sdtpldt0(xk, xm), sdtpldt0(xl, xn))) | (~aElement0(sdtpldt0(xk, xm)))),
% 162.95/163.19 inference(unit_resolution,[status(thm)],[77, 71])).
% 162.95/163.19 tff(79,plain,
% 162.95/163.19 (sdtpldt0(sdtpldt0(sdtpldt0(xk, xm), xl), xn) = sdtpldt0(sdtpldt0(xk, xm), sdtpldt0(xl, xn))),
% 162.95/163.19 inference(unit_resolution,[status(thm)],[78, 58, 49, 32])).
% 162.95/163.19 tff(80,plain,
% 162.95/163.19 (^[W0: $i, W1: $i] : refl((aElement0(sdtpldt0(W0, W1)) | (~aElement0(W1)) | (~aElement0(W0))) <=> (aElement0(sdtpldt0(W0, W1)) | (~aElement0(W1)) | (~aElement0(W0))))),
% 162.95/163.19 inference(bind,[status(th)],[])).
% 162.95/163.19 tff(81,plain,
% 162.95/163.19 (![W0: $i, W1: $i] : (aElement0(sdtpldt0(W0, W1)) | (~aElement0(W1)) | (~aElement0(W0))) <=> ![W0: $i, W1: $i] : (aElement0(sdtpldt0(W0, W1)) | (~aElement0(W1)) | (~aElement0(W0)))),
% 162.95/163.19 inference(quant_intro,[status(thm)],[80])).
% 162.95/163.19 tff(82,plain,
% 162.95/163.19 (^[W0: $i, W1: $i] : trans(monotonicity(trans(monotonicity(rewrite((aElement0(W0) & aElement0(W1)) <=> (~((~aElement0(W1)) | (~aElement0(W0))))), ((~(aElement0(W0) & aElement0(W1))) <=> (~(~((~aElement0(W1)) | (~aElement0(W0))))))), rewrite((~(~((~aElement0(W1)) | (~aElement0(W0))))) <=> ((~aElement0(W1)) | (~aElement0(W0)))), ((~(aElement0(W0) & aElement0(W1))) <=> ((~aElement0(W1)) | (~aElement0(W0))))), ((aElement0(sdtpldt0(W0, W1)) | (~(aElement0(W0) & aElement0(W1)))) <=> (aElement0(sdtpldt0(W0, W1)) | ((~aElement0(W1)) | (~aElement0(W0)))))), rewrite((aElement0(sdtpldt0(W0, W1)) | ((~aElement0(W1)) | (~aElement0(W0)))) <=> (aElement0(sdtpldt0(W0, W1)) | (~aElement0(W1)) | (~aElement0(W0)))), ((aElement0(sdtpldt0(W0, W1)) | (~(aElement0(W0) & aElement0(W1)))) <=> (aElement0(sdtpldt0(W0, W1)) | (~aElement0(W1)) | (~aElement0(W0)))))),
% 162.95/163.19 inference(bind,[status(th)],[])).
% 162.95/163.19 tff(83,plain,
% 162.95/163.19 (![W0: $i, W1: $i] : (aElement0(sdtpldt0(W0, W1)) | (~(aElement0(W0) & aElement0(W1)))) <=> ![W0: $i, W1: $i] : (aElement0(sdtpldt0(W0, W1)) | (~aElement0(W1)) | (~aElement0(W0)))),
% 162.95/163.19 inference(quant_intro,[status(thm)],[82])).
% 162.95/163.19 tff(84,plain,
% 162.95/163.19 (![W0: $i, W1: $i] : (aElement0(sdtpldt0(W0, W1)) | (~(aElement0(W0) & aElement0(W1)))) <=> ![W0: $i, W1: $i] : (aElement0(sdtpldt0(W0, W1)) | (~(aElement0(W0) & aElement0(W1))))),
% 162.95/163.19 inference(rewrite,[status(thm)],[])).
% 162.95/163.19 tff(85,plain,
% 162.95/163.19 (^[W0: $i, W1: $i] : rewrite(((aElement0(W0) & aElement0(W1)) => aElement0(sdtpldt0(W0, W1))) <=> (aElement0(sdtpldt0(W0, W1)) | (~(aElement0(W0) & aElement0(W1)))))),
% 162.95/163.19 inference(bind,[status(th)],[])).
% 162.95/163.19 tff(86,plain,
% 162.95/163.19 (![W0: $i, W1: $i] : ((aElement0(W0) & aElement0(W1)) => aElement0(sdtpldt0(W0, W1))) <=> ![W0: $i, W1: $i] : (aElement0(sdtpldt0(W0, W1)) | (~(aElement0(W0) & aElement0(W1))))),
% 162.95/163.19 inference(quant_intro,[status(thm)],[85])).
% 162.95/163.19 tff(87,axiom,(![W0: $i, W1: $i] : ((aElement0(W0) & aElement0(W1)) => aElement0(sdtpldt0(W0, W1)))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','mSortsB')).
% 162.95/163.19 tff(88,plain,
% 162.95/163.19 (![W0: $i, W1: $i] : (aElement0(sdtpldt0(W0, W1)) | (~(aElement0(W0) & aElement0(W1))))),
% 162.95/163.19 inference(modus_ponens,[status(thm)],[87, 86])).
% 162.95/163.19 tff(89,plain,
% 162.95/163.19 (![W0: $i, W1: $i] : (aElement0(sdtpldt0(W0, W1)) | (~(aElement0(W0) & aElement0(W1))))),
% 162.95/163.19 inference(modus_ponens,[status(thm)],[88, 84])).
% 162.95/163.19 tff(90,plain,(
% 162.95/163.19 ![W0: $i, W1: $i] : (aElement0(sdtpldt0(W0, W1)) | (~(aElement0(W0) & aElement0(W1))))),
% 162.95/163.19 inference(skolemize,[status(sab)],[89])).
% 162.95/163.19 tff(91,plain,
% 162.95/163.19 (![W0: $i, W1: $i] : (aElement0(sdtpldt0(W0, W1)) | (~aElement0(W1)) | (~aElement0(W0)))),
% 162.95/163.19 inference(modus_ponens,[status(thm)],[90, 83])).
% 162.95/163.19 tff(92,plain,
% 162.95/163.19 (![W0: $i, W1: $i] : (aElement0(sdtpldt0(W0, W1)) | (~aElement0(W1)) | (~aElement0(W0)))),
% 162.95/163.19 inference(modus_ponens,[status(thm)],[91, 81])).
% 162.95/163.19 tff(93,plain,
% 162.95/163.19 (((~![W0: $i, W1: $i] : (aElement0(sdtpldt0(W0, W1)) | (~aElement0(W1)) | (~aElement0(W0)))) | ((~aElement0(xl)) | (~aElement0(sdtpldt0(xk, xm))) | aElement0(sdtpldt0(sdtpldt0(xk, xm), xl)))) <=> ((~![W0: $i, W1: $i] : (aElement0(sdtpldt0(W0, W1)) | (~aElement0(W1)) | (~aElement0(W0)))) | (~aElement0(xl)) | (~aElement0(sdtpldt0(xk, xm))) | aElement0(sdtpldt0(sdtpldt0(xk, xm), xl)))),
% 162.95/163.19 inference(rewrite,[status(thm)],[])).
% 162.95/163.19 tff(94,plain,
% 162.95/163.19 ((aElement0(sdtpldt0(sdtpldt0(xk, xm), xl)) | (~aElement0(xl)) | (~aElement0(sdtpldt0(xk, xm)))) <=> ((~aElement0(xl)) | (~aElement0(sdtpldt0(xk, xm))) | aElement0(sdtpldt0(sdtpldt0(xk, xm), xl)))),
% 162.95/163.19 inference(rewrite,[status(thm)],[])).
% 162.95/163.19 tff(95,plain,
% 162.95/163.19 (((~![W0: $i, W1: $i] : (aElement0(sdtpldt0(W0, W1)) | (~aElement0(W1)) | (~aElement0(W0)))) | (aElement0(sdtpldt0(sdtpldt0(xk, xm), xl)) | (~aElement0(xl)) | (~aElement0(sdtpldt0(xk, xm))))) <=> ((~![W0: $i, W1: $i] : (aElement0(sdtpldt0(W0, W1)) | (~aElement0(W1)) | (~aElement0(W0)))) | ((~aElement0(xl)) | (~aElement0(sdtpldt0(xk, xm))) | aElement0(sdtpldt0(sdtpldt0(xk, xm), xl))))),
% 162.95/163.19 inference(monotonicity,[status(thm)],[94])).
% 162.95/163.19 tff(96,plain,
% 162.95/163.19 (((~![W0: $i, W1: $i] : (aElement0(sdtpldt0(W0, W1)) | (~aElement0(W1)) | (~aElement0(W0)))) | (aElement0(sdtpldt0(sdtpldt0(xk, xm), xl)) | (~aElement0(xl)) | (~aElement0(sdtpldt0(xk, xm))))) <=> ((~![W0: $i, W1: $i] : (aElement0(sdtpldt0(W0, W1)) | (~aElement0(W1)) | (~aElement0(W0)))) | (~aElement0(xl)) | (~aElement0(sdtpldt0(xk, xm))) | aElement0(sdtpldt0(sdtpldt0(xk, xm), xl)))),
% 162.95/163.19 inference(transitivity,[status(thm)],[95, 93])).
% 162.95/163.19 tff(97,plain,
% 162.95/163.19 ((~![W0: $i, W1: $i] : (aElement0(sdtpldt0(W0, W1)) | (~aElement0(W1)) | (~aElement0(W0)))) | (aElement0(sdtpldt0(sdtpldt0(xk, xm), xl)) | (~aElement0(xl)) | (~aElement0(sdtpldt0(xk, xm))))),
% 162.95/163.19 inference(quant_inst,[status(thm)],[])).
% 162.95/163.19 tff(98,plain,
% 162.95/163.19 ((~![W0: $i, W1: $i] : (aElement0(sdtpldt0(W0, W1)) | (~aElement0(W1)) | (~aElement0(W0)))) | (~aElement0(xl)) | (~aElement0(sdtpldt0(xk, xm))) | aElement0(sdtpldt0(sdtpldt0(xk, xm), xl))),
% 162.95/163.19 inference(modus_ponens,[status(thm)],[97, 96])).
% 162.95/163.19 tff(99,plain,
% 162.95/163.19 (aElement0(sdtpldt0(sdtpldt0(xk, xm), xl))),
% 162.95/163.19 inference(unit_resolution,[status(thm)],[98, 92, 32, 49])).
% 162.95/163.19 tff(100,plain,
% 162.95/163.19 (^[W0: $i, W1: $i] : refl(((sdtpldt0(W0, W1) = sdtpldt0(W1, W0)) | (~aElement0(W1)) | (~aElement0(W0))) <=> ((sdtpldt0(W0, W1) = sdtpldt0(W1, W0)) | (~aElement0(W1)) | (~aElement0(W0))))),
% 162.95/163.19 inference(bind,[status(th)],[])).
% 162.95/163.19 tff(101,plain,
% 162.95/163.19 (![W0: $i, W1: $i] : ((sdtpldt0(W0, W1) = sdtpldt0(W1, W0)) | (~aElement0(W1)) | (~aElement0(W0))) <=> ![W0: $i, W1: $i] : ((sdtpldt0(W0, W1) = sdtpldt0(W1, W0)) | (~aElement0(W1)) | (~aElement0(W0)))),
% 162.95/163.19 inference(quant_intro,[status(thm)],[100])).
% 162.95/163.19 tff(102,plain,
% 162.95/163.19 (^[W0: $i, W1: $i] : trans(monotonicity(trans(monotonicity(rewrite((aElement0(W0) & aElement0(W1)) <=> (~((~aElement0(W1)) | (~aElement0(W0))))), ((~(aElement0(W0) & aElement0(W1))) <=> (~(~((~aElement0(W1)) | (~aElement0(W0))))))), rewrite((~(~((~aElement0(W1)) | (~aElement0(W0))))) <=> ((~aElement0(W1)) | (~aElement0(W0)))), ((~(aElement0(W0) & aElement0(W1))) <=> ((~aElement0(W1)) | (~aElement0(W0))))), (((~(aElement0(W0) & aElement0(W1))) | (sdtpldt0(W0, W1) = sdtpldt0(W1, W0))) <=> (((~aElement0(W1)) | (~aElement0(W0))) | (sdtpldt0(W0, W1) = sdtpldt0(W1, W0))))), rewrite((((~aElement0(W1)) | (~aElement0(W0))) | (sdtpldt0(W0, W1) = sdtpldt0(W1, W0))) <=> ((sdtpldt0(W0, W1) = sdtpldt0(W1, W0)) | (~aElement0(W1)) | (~aElement0(W0)))), (((~(aElement0(W0) & aElement0(W1))) | (sdtpldt0(W0, W1) = sdtpldt0(W1, W0))) <=> ((sdtpldt0(W0, W1) = sdtpldt0(W1, W0)) | (~aElement0(W1)) | (~aElement0(W0)))))),
% 162.95/163.19 inference(bind,[status(th)],[])).
% 162.95/163.19 tff(103,plain,
% 162.95/163.19 (![W0: $i, W1: $i] : ((~(aElement0(W0) & aElement0(W1))) | (sdtpldt0(W0, W1) = sdtpldt0(W1, W0))) <=> ![W0: $i, W1: $i] : ((sdtpldt0(W0, W1) = sdtpldt0(W1, W0)) | (~aElement0(W1)) | (~aElement0(W0)))),
% 162.95/163.19 inference(quant_intro,[status(thm)],[102])).
% 162.95/163.19 tff(104,plain,
% 162.95/163.19 (![W0: $i, W1: $i] : ((~(aElement0(W0) & aElement0(W1))) | (sdtpldt0(W0, W1) = sdtpldt0(W1, W0))) <=> ![W0: $i, W1: $i] : ((~(aElement0(W0) & aElement0(W1))) | (sdtpldt0(W0, W1) = sdtpldt0(W1, W0)))),
% 162.95/163.19 inference(rewrite,[status(thm)],[])).
% 162.95/163.19 tff(105,plain,
% 162.95/163.19 (^[W0: $i, W1: $i] : rewrite(((aElement0(W0) & aElement0(W1)) => (sdtpldt0(W0, W1) = sdtpldt0(W1, W0))) <=> ((~(aElement0(W0) & aElement0(W1))) | (sdtpldt0(W0, W1) = sdtpldt0(W1, W0))))),
% 162.95/163.19 inference(bind,[status(th)],[])).
% 162.95/163.19 tff(106,plain,
% 162.95/163.19 (![W0: $i, W1: $i] : ((aElement0(W0) & aElement0(W1)) => (sdtpldt0(W0, W1) = sdtpldt0(W1, W0))) <=> ![W0: $i, W1: $i] : ((~(aElement0(W0) & aElement0(W1))) | (sdtpldt0(W0, W1) = sdtpldt0(W1, W0)))),
% 162.95/163.19 inference(quant_intro,[status(thm)],[105])).
% 162.95/163.19 tff(107,axiom,(![W0: $i, W1: $i] : ((aElement0(W0) & aElement0(W1)) => (sdtpldt0(W0, W1) = sdtpldt0(W1, W0)))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','mAddComm')).
% 162.95/163.19 tff(108,plain,
% 162.95/163.19 (![W0: $i, W1: $i] : ((~(aElement0(W0) & aElement0(W1))) | (sdtpldt0(W0, W1) = sdtpldt0(W1, W0)))),
% 162.95/163.19 inference(modus_ponens,[status(thm)],[107, 106])).
% 162.95/163.19 tff(109,plain,
% 162.95/163.19 (![W0: $i, W1: $i] : ((~(aElement0(W0) & aElement0(W1))) | (sdtpldt0(W0, W1) = sdtpldt0(W1, W0)))),
% 162.95/163.19 inference(modus_ponens,[status(thm)],[108, 104])).
% 162.95/163.19 tff(110,plain,(
% 162.95/163.19 ![W0: $i, W1: $i] : ((~(aElement0(W0) & aElement0(W1))) | (sdtpldt0(W0, W1) = sdtpldt0(W1, W0)))),
% 162.95/163.19 inference(skolemize,[status(sab)],[109])).
% 162.95/163.19 tff(111,plain,
% 162.95/163.19 (![W0: $i, W1: $i] : ((sdtpldt0(W0, W1) = sdtpldt0(W1, W0)) | (~aElement0(W1)) | (~aElement0(W0)))),
% 162.95/163.19 inference(modus_ponens,[status(thm)],[110, 103])).
% 162.95/163.19 tff(112,plain,
% 162.95/163.19 (![W0: $i, W1: $i] : ((sdtpldt0(W0, W1) = sdtpldt0(W1, W0)) | (~aElement0(W1)) | (~aElement0(W0)))),
% 162.95/163.19 inference(modus_ponens,[status(thm)],[111, 101])).
% 162.95/163.19 tff(113,plain,
% 162.95/163.19 (((~![W0: $i, W1: $i] : ((sdtpldt0(W0, W1) = sdtpldt0(W1, W0)) | (~aElement0(W1)) | (~aElement0(W0)))) | ((~aElement0(xn)) | (sdtpldt0(xn, sdtpldt0(sdtpldt0(xk, xm), xl)) = sdtpldt0(sdtpldt0(sdtpldt0(xk, xm), xl), xn)) | (~aElement0(sdtpldt0(sdtpldt0(xk, xm), xl))))) <=> ((~![W0: $i, W1: $i] : ((sdtpldt0(W0, W1) = sdtpldt0(W1, W0)) | (~aElement0(W1)) | (~aElement0(W0)))) | (~aElement0(xn)) | (sdtpldt0(xn, sdtpldt0(sdtpldt0(xk, xm), xl)) = sdtpldt0(sdtpldt0(sdtpldt0(xk, xm), xl), xn)) | (~aElement0(sdtpldt0(sdtpldt0(xk, xm), xl))))),
% 162.95/163.19 inference(rewrite,[status(thm)],[])).
% 162.95/163.19 tff(114,plain,
% 162.95/163.19 (((sdtpldt0(xn, sdtpldt0(sdtpldt0(xk, xm), xl)) = sdtpldt0(sdtpldt0(sdtpldt0(xk, xm), xl), xn)) | (~aElement0(sdtpldt0(sdtpldt0(xk, xm), xl))) | (~aElement0(xn))) <=> ((~aElement0(xn)) | (sdtpldt0(xn, sdtpldt0(sdtpldt0(xk, xm), xl)) = sdtpldt0(sdtpldt0(sdtpldt0(xk, xm), xl), xn)) | (~aElement0(sdtpldt0(sdtpldt0(xk, xm), xl))))),
% 162.95/163.19 inference(rewrite,[status(thm)],[])).
% 162.95/163.19 tff(115,plain,
% 162.95/163.19 (((~![W0: $i, W1: $i] : ((sdtpldt0(W0, W1) = sdtpldt0(W1, W0)) | (~aElement0(W1)) | (~aElement0(W0)))) | ((sdtpldt0(xn, sdtpldt0(sdtpldt0(xk, xm), xl)) = sdtpldt0(sdtpldt0(sdtpldt0(xk, xm), xl), xn)) | (~aElement0(sdtpldt0(sdtpldt0(xk, xm), xl))) | (~aElement0(xn)))) <=> ((~![W0: $i, W1: $i] : ((sdtpldt0(W0, W1) = sdtpldt0(W1, W0)) | (~aElement0(W1)) | (~aElement0(W0)))) | ((~aElement0(xn)) | (sdtpldt0(xn, sdtpldt0(sdtpldt0(xk, xm), xl)) = sdtpldt0(sdtpldt0(sdtpldt0(xk, xm), xl), xn)) | (~aElement0(sdtpldt0(sdtpldt0(xk, xm), xl)))))),
% 162.95/163.19 inference(monotonicity,[status(thm)],[114])).
% 162.95/163.19 tff(116,plain,
% 162.95/163.19 (((~![W0: $i, W1: $i] : ((sdtpldt0(W0, W1) = sdtpldt0(W1, W0)) | (~aElement0(W1)) | (~aElement0(W0)))) | ((sdtpldt0(xn, sdtpldt0(sdtpldt0(xk, xm), xl)) = sdtpldt0(sdtpldt0(sdtpldt0(xk, xm), xl), xn)) | (~aElement0(sdtpldt0(sdtpldt0(xk, xm), xl))) | (~aElement0(xn)))) <=> ((~![W0: $i, W1: $i] : ((sdtpldt0(W0, W1) = sdtpldt0(W1, W0)) | (~aElement0(W1)) | (~aElement0(W0)))) | (~aElement0(xn)) | (sdtpldt0(xn, sdtpldt0(sdtpldt0(xk, xm), xl)) = sdtpldt0(sdtpldt0(sdtpldt0(xk, xm), xl), xn)) | (~aElement0(sdtpldt0(sdtpldt0(xk, xm), xl))))),
% 162.95/163.19 inference(transitivity,[status(thm)],[115, 113])).
% 162.95/163.19 tff(117,plain,
% 162.95/163.19 ((~![W0: $i, W1: $i] : ((sdtpldt0(W0, W1) = sdtpldt0(W1, W0)) | (~aElement0(W1)) | (~aElement0(W0)))) | ((sdtpldt0(xn, sdtpldt0(sdtpldt0(xk, xm), xl)) = sdtpldt0(sdtpldt0(sdtpldt0(xk, xm), xl), xn)) | (~aElement0(sdtpldt0(sdtpldt0(xk, xm), xl))) | (~aElement0(xn)))),
% 162.95/163.19 inference(quant_inst,[status(thm)],[])).
% 162.95/163.19 tff(118,plain,
% 162.95/163.19 ((~![W0: $i, W1: $i] : ((sdtpldt0(W0, W1) = sdtpldt0(W1, W0)) | (~aElement0(W1)) | (~aElement0(W0)))) | (~aElement0(xn)) | (sdtpldt0(xn, sdtpldt0(sdtpldt0(xk, xm), xl)) = sdtpldt0(sdtpldt0(sdtpldt0(xk, xm), xl), xn)) | (~aElement0(sdtpldt0(sdtpldt0(xk, xm), xl)))),
% 162.95/163.19 inference(modus_ponens,[status(thm)],[117, 116])).
% 162.95/163.19 tff(119,plain,
% 162.95/163.19 ((sdtpldt0(xn, sdtpldt0(sdtpldt0(xk, xm), xl)) = sdtpldt0(sdtpldt0(sdtpldt0(xk, xm), xl), xn)) | (~aElement0(sdtpldt0(sdtpldt0(xk, xm), xl)))),
% 162.95/163.19 inference(unit_resolution,[status(thm)],[118, 112, 58])).
% 162.95/163.19 tff(120,plain,
% 162.95/163.19 (sdtpldt0(xn, sdtpldt0(sdtpldt0(xk, xm), xl)) = sdtpldt0(sdtpldt0(sdtpldt0(xk, xm), xl), xn)),
% 162.95/163.19 inference(unit_resolution,[status(thm)],[119, 99])).
% 162.95/163.19 tff(121,plain,
% 162.95/163.19 (aElementOf0(xk, xI) <=> aElementOf0(xk, xI)),
% 162.95/163.19 inference(rewrite,[status(thm)],[])).
% 162.95/163.19 tff(122,plain,
% 162.95/163.19 (aElementOf0(xk, xI)),
% 162.95/163.19 inference(and_elim,[status(thm)],[26])).
% 162.95/163.19 tff(123,plain,
% 162.95/163.19 (aElementOf0(xk, xI)),
% 162.95/163.19 inference(modus_ponens,[status(thm)],[122, 121])).
% 162.95/163.19 tff(124,plain,
% 162.95/163.19 (((~![W1: $i] : (aElement0(W1) | (~aElementOf0(W1, xI)))) | (aElement0(xk) | (~aElementOf0(xk, xI)))) <=> ((~![W1: $i] : (aElement0(W1) | (~aElementOf0(W1, xI)))) | aElement0(xk) | (~aElementOf0(xk, xI)))),
% 162.95/163.19 inference(rewrite,[status(thm)],[])).
% 162.95/163.19 tff(125,plain,
% 162.95/163.19 ((~![W1: $i] : (aElement0(W1) | (~aElementOf0(W1, xI)))) | (aElement0(xk) | (~aElementOf0(xk, xI)))),
% 162.95/163.19 inference(quant_inst,[status(thm)],[])).
% 162.95/163.19 tff(126,plain,
% 162.95/163.19 ((~![W1: $i] : (aElement0(W1) | (~aElementOf0(W1, xI)))) | aElement0(xk) | (~aElementOf0(xk, xI))),
% 162.95/163.19 inference(modus_ponens,[status(thm)],[125, 124])).
% 162.95/163.19 tff(127,plain,
% 162.95/163.19 (aElement0(xk)),
% 162.95/163.19 inference(unit_resolution,[status(thm)],[126, 123, 41])).
% 162.95/163.19 tff(128,plain,
% 162.95/163.19 (aElementOf0(xm, xI) <=> aElementOf0(xm, xI)),
% 162.95/163.19 inference(rewrite,[status(thm)],[])).
% 162.95/163.19 tff(129,plain,
% 162.95/163.19 (aElementOf0(xm, xI)),
% 162.95/163.19 inference(and_elim,[status(thm)],[52])).
% 162.95/163.19 tff(130,plain,
% 162.95/163.19 (aElementOf0(xm, xI)),
% 162.95/163.19 inference(modus_ponens,[status(thm)],[129, 128])).
% 162.95/163.19 tff(131,plain,
% 162.95/163.19 (((~![W1: $i] : (aElement0(W1) | (~aElementOf0(W1, xI)))) | (aElement0(xm) | (~aElementOf0(xm, xI)))) <=> ((~![W1: $i] : (aElement0(W1) | (~aElementOf0(W1, xI)))) | aElement0(xm) | (~aElementOf0(xm, xI)))),
% 162.95/163.19 inference(rewrite,[status(thm)],[])).
% 162.95/163.19 tff(132,plain,
% 162.95/163.19 ((~![W1: $i] : (aElement0(W1) | (~aElementOf0(W1, xI)))) | (aElement0(xm) | (~aElementOf0(xm, xI)))),
% 162.95/163.19 inference(quant_inst,[status(thm)],[])).
% 162.95/163.19 tff(133,plain,
% 162.95/163.19 ((~![W1: $i] : (aElement0(W1) | (~aElementOf0(W1, xI)))) | aElement0(xm) | (~aElementOf0(xm, xI))),
% 162.95/163.19 inference(modus_ponens,[status(thm)],[132, 131])).
% 162.95/163.19 tff(134,plain,
% 162.95/163.19 (aElement0(xm)),
% 162.95/163.19 inference(unit_resolution,[status(thm)],[133, 130, 41])).
% 162.95/163.19 tff(135,plain,
% 162.95/163.19 (((~![W0: $i, W1: $i] : ((sdtpldt0(W0, W1) = sdtpldt0(W1, W0)) | (~aElement0(W1)) | (~aElement0(W0)))) | ((~aElement0(xk)) | (~aElement0(xm)) | (sdtpldt0(xm, xk) = sdtpldt0(xk, xm)))) <=> ((~![W0: $i, W1: $i] : ((sdtpldt0(W0, W1) = sdtpldt0(W1, W0)) | (~aElement0(W1)) | (~aElement0(W0)))) | (~aElement0(xk)) | (~aElement0(xm)) | (sdtpldt0(xm, xk) = sdtpldt0(xk, xm)))),
% 162.95/163.19 inference(rewrite,[status(thm)],[])).
% 162.95/163.19 tff(136,plain,
% 162.95/163.19 (((sdtpldt0(xm, xk) = sdtpldt0(xk, xm)) | (~aElement0(xk)) | (~aElement0(xm))) <=> ((~aElement0(xk)) | (~aElement0(xm)) | (sdtpldt0(xm, xk) = sdtpldt0(xk, xm)))),
% 162.95/163.19 inference(rewrite,[status(thm)],[])).
% 162.95/163.19 tff(137,plain,
% 162.95/163.19 (((~![W0: $i, W1: $i] : ((sdtpldt0(W0, W1) = sdtpldt0(W1, W0)) | (~aElement0(W1)) | (~aElement0(W0)))) | ((sdtpldt0(xm, xk) = sdtpldt0(xk, xm)) | (~aElement0(xk)) | (~aElement0(xm)))) <=> ((~![W0: $i, W1: $i] : ((sdtpldt0(W0, W1) = sdtpldt0(W1, W0)) | (~aElement0(W1)) | (~aElement0(W0)))) | ((~aElement0(xk)) | (~aElement0(xm)) | (sdtpldt0(xm, xk) = sdtpldt0(xk, xm))))),
% 162.95/163.19 inference(monotonicity,[status(thm)],[136])).
% 162.95/163.19 tff(138,plain,
% 162.95/163.19 (((~![W0: $i, W1: $i] : ((sdtpldt0(W0, W1) = sdtpldt0(W1, W0)) | (~aElement0(W1)) | (~aElement0(W0)))) | ((sdtpldt0(xm, xk) = sdtpldt0(xk, xm)) | (~aElement0(xk)) | (~aElement0(xm)))) <=> ((~![W0: $i, W1: $i] : ((sdtpldt0(W0, W1) = sdtpldt0(W1, W0)) | (~aElement0(W1)) | (~aElement0(W0)))) | (~aElement0(xk)) | (~aElement0(xm)) | (sdtpldt0(xm, xk) = sdtpldt0(xk, xm)))),
% 162.95/163.19 inference(transitivity,[status(thm)],[137, 135])).
% 162.95/163.19 tff(139,plain,
% 162.95/163.19 ((~![W0: $i, W1: $i] : ((sdtpldt0(W0, W1) = sdtpldt0(W1, W0)) | (~aElement0(W1)) | (~aElement0(W0)))) | ((sdtpldt0(xm, xk) = sdtpldt0(xk, xm)) | (~aElement0(xk)) | (~aElement0(xm)))),
% 162.95/163.19 inference(quant_inst,[status(thm)],[])).
% 162.95/163.19 tff(140,plain,
% 162.95/163.19 ((~![W0: $i, W1: $i] : ((sdtpldt0(W0, W1) = sdtpldt0(W1, W0)) | (~aElement0(W1)) | (~aElement0(W0)))) | (~aElement0(xk)) | (~aElement0(xm)) | (sdtpldt0(xm, xk) = sdtpldt0(xk, xm))),
% 162.95/163.19 inference(modus_ponens,[status(thm)],[139, 138])).
% 162.95/163.19 tff(141,plain,
% 162.95/163.19 ((~aElement0(xk)) | (~aElement0(xm)) | (sdtpldt0(xm, xk) = sdtpldt0(xk, xm))),
% 162.95/163.19 inference(unit_resolution,[status(thm)],[140, 112])).
% 162.95/163.19 tff(142,plain,
% 162.95/163.19 (sdtpldt0(xm, xk) = sdtpldt0(xk, xm)),
% 162.95/163.19 inference(unit_resolution,[status(thm)],[141, 134, 127])).
% 162.95/163.19 tff(143,plain,
% 162.95/163.19 (sdtpldt0(sdtpldt0(xm, xk), xl) = sdtpldt0(sdtpldt0(xk, xm), xl)),
% 162.95/163.19 inference(monotonicity,[status(thm)],[142])).
% 162.95/163.19 tff(144,plain,
% 162.95/163.19 (((~![W0: $i, W1: $i, W2: $i] : ((sdtpldt0(sdtpldt0(W0, W1), W2) = sdtpldt0(W0, sdtpldt0(W1, W2))) | (~aElement0(W2)) | (~aElement0(W1)) | (~aElement0(W0)))) | ((~aElement0(xl)) | (~aElement0(xk)) | (~aElement0(xm)) | (sdtpldt0(sdtpldt0(xm, xk), xl) = sdtpldt0(xm, sdtpldt0(xk, xl))))) <=> ((~![W0: $i, W1: $i, W2: $i] : ((sdtpldt0(sdtpldt0(W0, W1), W2) = sdtpldt0(W0, sdtpldt0(W1, W2))) | (~aElement0(W2)) | (~aElement0(W1)) | (~aElement0(W0)))) | (~aElement0(xl)) | (~aElement0(xk)) | (~aElement0(xm)) | (sdtpldt0(sdtpldt0(xm, xk), xl) = sdtpldt0(xm, sdtpldt0(xk, xl))))),
% 162.95/163.19 inference(rewrite,[status(thm)],[])).
% 162.95/163.19 tff(145,plain,
% 162.95/163.19 (((sdtpldt0(sdtpldt0(xm, xk), xl) = sdtpldt0(xm, sdtpldt0(xk, xl))) | (~aElement0(xl)) | (~aElement0(xk)) | (~aElement0(xm))) <=> ((~aElement0(xl)) | (~aElement0(xk)) | (~aElement0(xm)) | (sdtpldt0(sdtpldt0(xm, xk), xl) = sdtpldt0(xm, sdtpldt0(xk, xl))))),
% 162.95/163.19 inference(rewrite,[status(thm)],[])).
% 162.95/163.19 tff(146,plain,
% 162.95/163.19 (((~![W0: $i, W1: $i, W2: $i] : ((sdtpldt0(sdtpldt0(W0, W1), W2) = sdtpldt0(W0, sdtpldt0(W1, W2))) | (~aElement0(W2)) | (~aElement0(W1)) | (~aElement0(W0)))) | ((sdtpldt0(sdtpldt0(xm, xk), xl) = sdtpldt0(xm, sdtpldt0(xk, xl))) | (~aElement0(xl)) | (~aElement0(xk)) | (~aElement0(xm)))) <=> ((~![W0: $i, W1: $i, W2: $i] : ((sdtpldt0(sdtpldt0(W0, W1), W2) = sdtpldt0(W0, sdtpldt0(W1, W2))) | (~aElement0(W2)) | (~aElement0(W1)) | (~aElement0(W0)))) | ((~aElement0(xl)) | (~aElement0(xk)) | (~aElement0(xm)) | (sdtpldt0(sdtpldt0(xm, xk), xl) = sdtpldt0(xm, sdtpldt0(xk, xl)))))),
% 162.95/163.19 inference(monotonicity,[status(thm)],[145])).
% 162.95/163.19 tff(147,plain,
% 162.95/163.19 (((~![W0: $i, W1: $i, W2: $i] : ((sdtpldt0(sdtpldt0(W0, W1), W2) = sdtpldt0(W0, sdtpldt0(W1, W2))) | (~aElement0(W2)) | (~aElement0(W1)) | (~aElement0(W0)))) | ((sdtpldt0(sdtpldt0(xm, xk), xl) = sdtpldt0(xm, sdtpldt0(xk, xl))) | (~aElement0(xl)) | (~aElement0(xk)) | (~aElement0(xm)))) <=> ((~![W0: $i, W1: $i, W2: $i] : ((sdtpldt0(sdtpldt0(W0, W1), W2) = sdtpldt0(W0, sdtpldt0(W1, W2))) | (~aElement0(W2)) | (~aElement0(W1)) | (~aElement0(W0)))) | (~aElement0(xl)) | (~aElement0(xk)) | (~aElement0(xm)) | (sdtpldt0(sdtpldt0(xm, xk), xl) = sdtpldt0(xm, sdtpldt0(xk, xl))))),
% 162.95/163.19 inference(transitivity,[status(thm)],[146, 144])).
% 162.95/163.19 tff(148,plain,
% 162.95/163.19 ((~![W0: $i, W1: $i, W2: $i] : ((sdtpldt0(sdtpldt0(W0, W1), W2) = sdtpldt0(W0, sdtpldt0(W1, W2))) | (~aElement0(W2)) | (~aElement0(W1)) | (~aElement0(W0)))) | ((sdtpldt0(sdtpldt0(xm, xk), xl) = sdtpldt0(xm, sdtpldt0(xk, xl))) | (~aElement0(xl)) | (~aElement0(xk)) | (~aElement0(xm)))),
% 162.95/163.19 inference(quant_inst,[status(thm)],[])).
% 162.95/163.19 tff(149,plain,
% 162.95/163.19 ((~![W0: $i, W1: $i, W2: $i] : ((sdtpldt0(sdtpldt0(W0, W1), W2) = sdtpldt0(W0, sdtpldt0(W1, W2))) | (~aElement0(W2)) | (~aElement0(W1)) | (~aElement0(W0)))) | (~aElement0(xl)) | (~aElement0(xk)) | (~aElement0(xm)) | (sdtpldt0(sdtpldt0(xm, xk), xl) = sdtpldt0(xm, sdtpldt0(xk, xl)))),
% 162.95/163.19 inference(modus_ponens,[status(thm)],[148, 147])).
% 162.95/163.19 tff(150,plain,
% 162.95/163.19 (sdtpldt0(sdtpldt0(xm, xk), xl) = sdtpldt0(xm, sdtpldt0(xk, xl))),
% 162.95/163.19 inference(unit_resolution,[status(thm)],[149, 71, 32, 127, 134])).
% 162.95/163.19 tff(151,plain,
% 162.95/163.19 (sdtpldt0(xm, sdtpldt0(xk, xl)) = sdtpldt0(sdtpldt0(xm, xk), xl)),
% 162.95/163.19 inference(symmetry,[status(thm)],[150])).
% 162.95/163.19 tff(152,plain,
% 162.95/163.19 ((xx = sdtpldt0(xk, xl)) <=> (xx = sdtpldt0(xk, xl))),
% 162.95/163.19 inference(rewrite,[status(thm)],[])).
% 162.95/163.19 tff(153,plain,
% 162.95/163.19 (xx = sdtpldt0(xk, xl)),
% 162.95/163.19 inference(and_elim,[status(thm)],[25])).
% 162.95/163.19 tff(154,plain,
% 162.95/163.19 (xx = sdtpldt0(xk, xl)),
% 162.95/163.19 inference(modus_ponens,[status(thm)],[153, 152])).
% 162.95/163.19 tff(155,plain,
% 162.95/163.19 (^[W0: $i] : refl(((~aElement0(W0)) | (~((~(sdtasdt0(W0, sz10) = W0)) | (~(W0 = sdtasdt0(sz10, W0)))))) <=> ((~aElement0(W0)) | (~((~(sdtasdt0(W0, sz10) = W0)) | (~(W0 = sdtasdt0(sz10, W0)))))))),
% 162.95/163.19 inference(bind,[status(th)],[])).
% 162.95/163.19 tff(156,plain,
% 162.95/163.19 (![W0: $i] : ((~aElement0(W0)) | (~((~(sdtasdt0(W0, sz10) = W0)) | (~(W0 = sdtasdt0(sz10, W0)))))) <=> ![W0: $i] : ((~aElement0(W0)) | (~((~(sdtasdt0(W0, sz10) = W0)) | (~(W0 = sdtasdt0(sz10, W0))))))),
% 162.95/163.19 inference(quant_intro,[status(thm)],[155])).
% 162.95/163.19 tff(157,plain,
% 162.95/163.19 (^[W0: $i] : rewrite(((~aElement0(W0)) | ((sdtasdt0(W0, sz10) = W0) & (W0 = sdtasdt0(sz10, W0)))) <=> ((~aElement0(W0)) | (~((~(sdtasdt0(W0, sz10) = W0)) | (~(W0 = sdtasdt0(sz10, W0)))))))),
% 162.95/163.19 inference(bind,[status(th)],[])).
% 162.95/163.19 tff(158,plain,
% 162.95/163.19 (![W0: $i] : ((~aElement0(W0)) | ((sdtasdt0(W0, sz10) = W0) & (W0 = sdtasdt0(sz10, W0)))) <=> ![W0: $i] : ((~aElement0(W0)) | (~((~(sdtasdt0(W0, sz10) = W0)) | (~(W0 = sdtasdt0(sz10, W0))))))),
% 162.95/163.19 inference(quant_intro,[status(thm)],[157])).
% 162.95/163.19 tff(159,plain,
% 162.95/163.19 (![W0: $i] : ((~aElement0(W0)) | ((sdtasdt0(W0, sz10) = W0) & (W0 = sdtasdt0(sz10, W0)))) <=> ![W0: $i] : ((~aElement0(W0)) | ((sdtasdt0(W0, sz10) = W0) & (W0 = sdtasdt0(sz10, W0))))),
% 162.95/163.19 inference(rewrite,[status(thm)],[])).
% 162.95/163.19 tff(160,plain,
% 162.95/163.19 (^[W0: $i] : rewrite((aElement0(W0) => ((sdtasdt0(W0, sz10) = W0) & (W0 = sdtasdt0(sz10, W0)))) <=> ((~aElement0(W0)) | ((sdtasdt0(W0, sz10) = W0) & (W0 = sdtasdt0(sz10, W0)))))),
% 162.95/163.19 inference(bind,[status(th)],[])).
% 162.95/163.19 tff(161,plain,
% 162.95/163.19 (![W0: $i] : (aElement0(W0) => ((sdtasdt0(W0, sz10) = W0) & (W0 = sdtasdt0(sz10, W0)))) <=> ![W0: $i] : ((~aElement0(W0)) | ((sdtasdt0(W0, sz10) = W0) & (W0 = sdtasdt0(sz10, W0))))),
% 162.95/163.19 inference(quant_intro,[status(thm)],[160])).
% 162.95/163.19 tff(162,axiom,(![W0: $i] : (aElement0(W0) => ((sdtasdt0(W0, sz10) = W0) & (W0 = sdtasdt0(sz10, W0))))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','mMulUnit')).
% 162.95/163.19 tff(163,plain,
% 162.95/163.19 (![W0: $i] : ((~aElement0(W0)) | ((sdtasdt0(W0, sz10) = W0) & (W0 = sdtasdt0(sz10, W0))))),
% 162.95/163.19 inference(modus_ponens,[status(thm)],[162, 161])).
% 162.95/163.19 tff(164,plain,
% 162.95/163.19 (![W0: $i] : ((~aElement0(W0)) | ((sdtasdt0(W0, sz10) = W0) & (W0 = sdtasdt0(sz10, W0))))),
% 162.95/163.19 inference(modus_ponens,[status(thm)],[163, 159])).
% 162.95/163.19 tff(165,plain,(
% 162.95/163.19 ![W0: $i] : ((~aElement0(W0)) | ((sdtasdt0(W0, sz10) = W0) & (W0 = sdtasdt0(sz10, W0))))),
% 162.95/163.19 inference(skolemize,[status(sab)],[164])).
% 162.95/163.19 tff(166,plain,
% 162.95/163.19 (![W0: $i] : ((~aElement0(W0)) | (~((~(sdtasdt0(W0, sz10) = W0)) | (~(W0 = sdtasdt0(sz10, W0))))))),
% 162.95/163.19 inference(modus_ponens,[status(thm)],[165, 158])).
% 162.95/163.19 tff(167,plain,
% 162.95/163.19 (![W0: $i] : ((~aElement0(W0)) | (~((~(sdtasdt0(W0, sz10) = W0)) | (~(W0 = sdtasdt0(sz10, W0))))))),
% 162.95/163.19 inference(modus_ponens,[status(thm)],[166, 156])).
% 162.95/163.19 tff(168,plain,
% 162.95/163.19 (((~![W0: $i] : ((~aElement0(W0)) | (~((~(sdtasdt0(W0, sz10) = W0)) | (~(W0 = sdtasdt0(sz10, W0))))))) | ((~aElement0(xm)) | (~((~(sdtasdt0(xm, sz10) = xm)) | (~(xm = sdtasdt0(sz10, xm))))))) <=> ((~![W0: $i] : ((~aElement0(W0)) | (~((~(sdtasdt0(W0, sz10) = W0)) | (~(W0 = sdtasdt0(sz10, W0))))))) | (~aElement0(xm)) | (~((~(sdtasdt0(xm, sz10) = xm)) | (~(xm = sdtasdt0(sz10, xm))))))),
% 162.95/163.19 inference(rewrite,[status(thm)],[])).
% 162.95/163.19 tff(169,plain,
% 162.95/163.19 ((~![W0: $i] : ((~aElement0(W0)) | (~((~(sdtasdt0(W0, sz10) = W0)) | (~(W0 = sdtasdt0(sz10, W0))))))) | ((~aElement0(xm)) | (~((~(sdtasdt0(xm, sz10) = xm)) | (~(xm = sdtasdt0(sz10, xm))))))),
% 162.95/163.19 inference(quant_inst,[status(thm)],[])).
% 162.95/163.19 tff(170,plain,
% 162.95/163.19 ((~![W0: $i] : ((~aElement0(W0)) | (~((~(sdtasdt0(W0, sz10) = W0)) | (~(W0 = sdtasdt0(sz10, W0))))))) | (~aElement0(xm)) | (~((~(sdtasdt0(xm, sz10) = xm)) | (~(xm = sdtasdt0(sz10, xm)))))),
% 162.95/163.19 inference(modus_ponens,[status(thm)],[169, 168])).
% 162.95/163.19 tff(171,plain,
% 162.95/163.19 (~((~(sdtasdt0(xm, sz10) = xm)) | (~(xm = sdtasdt0(sz10, xm))))),
% 162.95/163.19 inference(unit_resolution,[status(thm)],[170, 167, 134])).
% 162.95/163.19 tff(172,plain,
% 162.95/163.19 (((~(sdtasdt0(xm, sz10) = xm)) | (~(xm = sdtasdt0(sz10, xm)))) | (sdtasdt0(xm, sz10) = xm)),
% 162.95/163.19 inference(tautology,[status(thm)],[])).
% 162.95/163.19 tff(173,plain,
% 162.95/163.19 (sdtasdt0(xm, sz10) = xm),
% 162.95/163.19 inference(unit_resolution,[status(thm)],[172, 171])).
% 162.95/163.19 tff(174,plain,
% 162.95/163.19 (^[W0: $i, W1: $i] : refl(((sdtasdt0(W0, W1) = sdtasdt0(W1, W0)) | (~aElement0(W1)) | (~aElement0(W0))) <=> ((sdtasdt0(W0, W1) = sdtasdt0(W1, W0)) | (~aElement0(W1)) | (~aElement0(W0))))),
% 162.95/163.19 inference(bind,[status(th)],[])).
% 162.95/163.19 tff(175,plain,
% 162.95/163.19 (![W0: $i, W1: $i] : ((sdtasdt0(W0, W1) = sdtasdt0(W1, W0)) | (~aElement0(W1)) | (~aElement0(W0))) <=> ![W0: $i, W1: $i] : ((sdtasdt0(W0, W1) = sdtasdt0(W1, W0)) | (~aElement0(W1)) | (~aElement0(W0)))),
% 162.95/163.19 inference(quant_intro,[status(thm)],[174])).
% 162.95/163.19 tff(176,plain,
% 162.95/163.19 (^[W0: $i, W1: $i] : trans(monotonicity(trans(monotonicity(rewrite((aElement0(W0) & aElement0(W1)) <=> (~((~aElement0(W1)) | (~aElement0(W0))))), ((~(aElement0(W0) & aElement0(W1))) <=> (~(~((~aElement0(W1)) | (~aElement0(W0))))))), rewrite((~(~((~aElement0(W1)) | (~aElement0(W0))))) <=> ((~aElement0(W1)) | (~aElement0(W0)))), ((~(aElement0(W0) & aElement0(W1))) <=> ((~aElement0(W1)) | (~aElement0(W0))))), (((~(aElement0(W0) & aElement0(W1))) | (sdtasdt0(W0, W1) = sdtasdt0(W1, W0))) <=> (((~aElement0(W1)) | (~aElement0(W0))) | (sdtasdt0(W0, W1) = sdtasdt0(W1, W0))))), rewrite((((~aElement0(W1)) | (~aElement0(W0))) | (sdtasdt0(W0, W1) = sdtasdt0(W1, W0))) <=> ((sdtasdt0(W0, W1) = sdtasdt0(W1, W0)) | (~aElement0(W1)) | (~aElement0(W0)))), (((~(aElement0(W0) & aElement0(W1))) | (sdtasdt0(W0, W1) = sdtasdt0(W1, W0))) <=> ((sdtasdt0(W0, W1) = sdtasdt0(W1, W0)) | (~aElement0(W1)) | (~aElement0(W0)))))),
% 162.95/163.19 inference(bind,[status(th)],[])).
% 162.95/163.19 tff(177,plain,
% 162.95/163.19 (![W0: $i, W1: $i] : ((~(aElement0(W0) & aElement0(W1))) | (sdtasdt0(W0, W1) = sdtasdt0(W1, W0))) <=> ![W0: $i, W1: $i] : ((sdtasdt0(W0, W1) = sdtasdt0(W1, W0)) | (~aElement0(W1)) | (~aElement0(W0)))),
% 162.95/163.19 inference(quant_intro,[status(thm)],[176])).
% 162.95/163.19 tff(178,plain,
% 162.95/163.19 (![W0: $i, W1: $i] : ((~(aElement0(W0) & aElement0(W1))) | (sdtasdt0(W0, W1) = sdtasdt0(W1, W0))) <=> ![W0: $i, W1: $i] : ((~(aElement0(W0) & aElement0(W1))) | (sdtasdt0(W0, W1) = sdtasdt0(W1, W0)))),
% 162.95/163.19 inference(rewrite,[status(thm)],[])).
% 162.95/163.19 tff(179,plain,
% 162.95/163.19 (^[W0: $i, W1: $i] : rewrite(((aElement0(W0) & aElement0(W1)) => (sdtasdt0(W0, W1) = sdtasdt0(W1, W0))) <=> ((~(aElement0(W0) & aElement0(W1))) | (sdtasdt0(W0, W1) = sdtasdt0(W1, W0))))),
% 162.95/163.19 inference(bind,[status(th)],[])).
% 162.95/163.19 tff(180,plain,
% 162.95/163.19 (![W0: $i, W1: $i] : ((aElement0(W0) & aElement0(W1)) => (sdtasdt0(W0, W1) = sdtasdt0(W1, W0))) <=> ![W0: $i, W1: $i] : ((~(aElement0(W0) & aElement0(W1))) | (sdtasdt0(W0, W1) = sdtasdt0(W1, W0)))),
% 162.95/163.19 inference(quant_intro,[status(thm)],[179])).
% 162.95/163.19 tff(181,axiom,(![W0: $i, W1: $i] : ((aElement0(W0) & aElement0(W1)) => (sdtasdt0(W0, W1) = sdtasdt0(W1, W0)))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','mMulComm')).
% 162.95/163.19 tff(182,plain,
% 162.95/163.19 (![W0: $i, W1: $i] : ((~(aElement0(W0) & aElement0(W1))) | (sdtasdt0(W0, W1) = sdtasdt0(W1, W0)))),
% 162.95/163.19 inference(modus_ponens,[status(thm)],[181, 180])).
% 162.95/163.19 tff(183,plain,
% 162.95/163.19 (![W0: $i, W1: $i] : ((~(aElement0(W0) & aElement0(W1))) | (sdtasdt0(W0, W1) = sdtasdt0(W1, W0)))),
% 162.95/163.19 inference(modus_ponens,[status(thm)],[182, 178])).
% 162.95/163.19 tff(184,plain,(
% 162.95/163.19 ![W0: $i, W1: $i] : ((~(aElement0(W0) & aElement0(W1))) | (sdtasdt0(W0, W1) = sdtasdt0(W1, W0)))),
% 162.95/163.19 inference(skolemize,[status(sab)],[183])).
% 162.95/163.19 tff(185,plain,
% 162.95/163.19 (![W0: $i, W1: $i] : ((sdtasdt0(W0, W1) = sdtasdt0(W1, W0)) | (~aElement0(W1)) | (~aElement0(W0)))),
% 162.95/163.19 inference(modus_ponens,[status(thm)],[184, 177])).
% 162.95/163.19 tff(186,plain,
% 162.95/163.19 (![W0: $i, W1: $i] : ((sdtasdt0(W0, W1) = sdtasdt0(W1, W0)) | (~aElement0(W1)) | (~aElement0(W0)))),
% 162.95/163.19 inference(modus_ponens,[status(thm)],[185, 175])).
% 162.95/163.19 tff(187,plain,
% 162.95/163.19 (aElement0(sz10) <=> aElement0(sz10)),
% 162.95/163.19 inference(rewrite,[status(thm)],[])).
% 162.95/163.19 tff(188,axiom,(aElement0(sz10)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','mSortsC_01')).
% 162.95/163.19 tff(189,plain,
% 162.95/163.19 (aElement0(sz10)),
% 162.95/163.19 inference(modus_ponens,[status(thm)],[188, 187])).
% 162.95/163.19 tff(190,plain,
% 162.95/163.19 (((~![W0: $i, W1: $i] : ((sdtasdt0(W0, W1) = sdtasdt0(W1, W0)) | (~aElement0(W1)) | (~aElement0(W0)))) | ((~aElement0(xm)) | (~aElement0(sz10)) | (sdtasdt0(xm, sz10) = sdtasdt0(sz10, xm)))) <=> ((~![W0: $i, W1: $i] : ((sdtasdt0(W0, W1) = sdtasdt0(W1, W0)) | (~aElement0(W1)) | (~aElement0(W0)))) | (~aElement0(xm)) | (~aElement0(sz10)) | (sdtasdt0(xm, sz10) = sdtasdt0(sz10, xm)))),
% 162.95/163.19 inference(rewrite,[status(thm)],[])).
% 162.95/163.19 tff(191,plain,
% 162.95/163.19 (((sdtasdt0(xm, sz10) = sdtasdt0(sz10, xm)) | (~aElement0(sz10)) | (~aElement0(xm))) <=> ((~aElement0(xm)) | (~aElement0(sz10)) | (sdtasdt0(xm, sz10) = sdtasdt0(sz10, xm)))),
% 162.95/163.19 inference(rewrite,[status(thm)],[])).
% 162.95/163.19 tff(192,plain,
% 162.95/163.19 (((~![W0: $i, W1: $i] : ((sdtasdt0(W0, W1) = sdtasdt0(W1, W0)) | (~aElement0(W1)) | (~aElement0(W0)))) | ((sdtasdt0(xm, sz10) = sdtasdt0(sz10, xm)) | (~aElement0(sz10)) | (~aElement0(xm)))) <=> ((~![W0: $i, W1: $i] : ((sdtasdt0(W0, W1) = sdtasdt0(W1, W0)) | (~aElement0(W1)) | (~aElement0(W0)))) | ((~aElement0(xm)) | (~aElement0(sz10)) | (sdtasdt0(xm, sz10) = sdtasdt0(sz10, xm))))),
% 162.95/163.19 inference(monotonicity,[status(thm)],[191])).
% 162.95/163.19 tff(193,plain,
% 162.95/163.19 (((~![W0: $i, W1: $i] : ((sdtasdt0(W0, W1) = sdtasdt0(W1, W0)) | (~aElement0(W1)) | (~aElement0(W0)))) | ((sdtasdt0(xm, sz10) = sdtasdt0(sz10, xm)) | (~aElement0(sz10)) | (~aElement0(xm)))) <=> ((~![W0: $i, W1: $i] : ((sdtasdt0(W0, W1) = sdtasdt0(W1, W0)) | (~aElement0(W1)) | (~aElement0(W0)))) | (~aElement0(xm)) | (~aElement0(sz10)) | (sdtasdt0(xm, sz10) = sdtasdt0(sz10, xm)))),
% 162.95/163.19 inference(transitivity,[status(thm)],[192, 190])).
% 162.95/163.19 tff(194,plain,
% 162.95/163.19 ((~![W0: $i, W1: $i] : ((sdtasdt0(W0, W1) = sdtasdt0(W1, W0)) | (~aElement0(W1)) | (~aElement0(W0)))) | ((sdtasdt0(xm, sz10) = sdtasdt0(sz10, xm)) | (~aElement0(sz10)) | (~aElement0(xm)))),
% 162.95/163.19 inference(quant_inst,[status(thm)],[])).
% 162.95/163.19 tff(195,plain,
% 162.95/163.19 ((~![W0: $i, W1: $i] : ((sdtasdt0(W0, W1) = sdtasdt0(W1, W0)) | (~aElement0(W1)) | (~aElement0(W0)))) | (~aElement0(xm)) | (~aElement0(sz10)) | (sdtasdt0(xm, sz10) = sdtasdt0(sz10, xm))),
% 162.95/163.19 inference(modus_ponens,[status(thm)],[194, 193])).
% 162.95/163.19 tff(196,plain,
% 162.95/163.19 (sdtasdt0(xm, sz10) = sdtasdt0(sz10, xm)),
% 162.95/163.19 inference(unit_resolution,[status(thm)],[195, 189, 186, 134])).
% 162.95/163.19 tff(197,plain,
% 162.95/163.19 (sdtasdt0(sz10, xm) = sdtasdt0(xm, sz10)),
% 162.95/163.19 inference(symmetry,[status(thm)],[196])).
% 162.95/163.19 tff(198,plain,
% 162.95/163.19 (sdtasdt0(sz10, xm) = xm),
% 162.95/163.19 inference(transitivity,[status(thm)],[197, 173])).
% 162.95/163.19 tff(199,plain,
% 162.95/163.19 (sdtpldt0(sdtasdt0(sz10, xm), xx) = sdtpldt0(xm, sdtpldt0(xk, xl))),
% 162.95/163.19 inference(monotonicity,[status(thm)],[198, 154])).
% 162.95/163.19 tff(200,plain,
% 162.95/163.19 (sdtpldt0(sdtasdt0(sz10, xm), xx) = sdtpldt0(sdtpldt0(xk, xm), xl)),
% 162.95/163.19 inference(transitivity,[status(thm)],[199, 151, 143])).
% 162.95/163.19 tff(201,plain,
% 162.95/163.19 (((~![W0: $i] : ((~aElement0(W0)) | (~((~(sdtasdt0(W0, sz10) = W0)) | (~(W0 = sdtasdt0(sz10, W0))))))) | ((~aElement0(xn)) | (~((~(sdtasdt0(xn, sz10) = xn)) | (~(xn = sdtasdt0(sz10, xn))))))) <=> ((~![W0: $i] : ((~aElement0(W0)) | (~((~(sdtasdt0(W0, sz10) = W0)) | (~(W0 = sdtasdt0(sz10, W0))))))) | (~aElement0(xn)) | (~((~(sdtasdt0(xn, sz10) = xn)) | (~(xn = sdtasdt0(sz10, xn))))))),
% 162.95/163.19 inference(rewrite,[status(thm)],[])).
% 162.95/163.19 tff(202,plain,
% 162.95/163.19 ((~![W0: $i] : ((~aElement0(W0)) | (~((~(sdtasdt0(W0, sz10) = W0)) | (~(W0 = sdtasdt0(sz10, W0))))))) | ((~aElement0(xn)) | (~((~(sdtasdt0(xn, sz10) = xn)) | (~(xn = sdtasdt0(sz10, xn))))))),
% 162.95/163.20 inference(quant_inst,[status(thm)],[])).
% 162.95/163.20 tff(203,plain,
% 162.95/163.20 ((~![W0: $i] : ((~aElement0(W0)) | (~((~(sdtasdt0(W0, sz10) = W0)) | (~(W0 = sdtasdt0(sz10, W0))))))) | (~aElement0(xn)) | (~((~(sdtasdt0(xn, sz10) = xn)) | (~(xn = sdtasdt0(sz10, xn)))))),
% 162.95/163.20 inference(modus_ponens,[status(thm)],[202, 201])).
% 162.95/163.20 tff(204,plain,
% 162.95/163.20 (~((~(sdtasdt0(xn, sz10) = xn)) | (~(xn = sdtasdt0(sz10, xn))))),
% 162.95/163.20 inference(unit_resolution,[status(thm)],[203, 167, 58])).
% 162.95/163.20 tff(205,plain,
% 162.95/163.20 (((~(sdtasdt0(xn, sz10) = xn)) | (~(xn = sdtasdt0(sz10, xn)))) | (sdtasdt0(xn, sz10) = xn)),
% 162.95/163.20 inference(tautology,[status(thm)],[])).
% 162.95/163.20 tff(206,plain,
% 162.95/163.20 (sdtasdt0(xn, sz10) = xn),
% 162.95/163.20 inference(unit_resolution,[status(thm)],[205, 204])).
% 162.95/163.20 tff(207,plain,
% 162.95/163.20 (((~![W0: $i, W1: $i] : ((sdtasdt0(W0, W1) = sdtasdt0(W1, W0)) | (~aElement0(W1)) | (~aElement0(W0)))) | ((~aElement0(xn)) | (~aElement0(sz10)) | (sdtasdt0(xn, sz10) = sdtasdt0(sz10, xn)))) <=> ((~![W0: $i, W1: $i] : ((sdtasdt0(W0, W1) = sdtasdt0(W1, W0)) | (~aElement0(W1)) | (~aElement0(W0)))) | (~aElement0(xn)) | (~aElement0(sz10)) | (sdtasdt0(xn, sz10) = sdtasdt0(sz10, xn)))),
% 162.95/163.20 inference(rewrite,[status(thm)],[])).
% 162.95/163.20 tff(208,plain,
% 162.95/163.20 (((sdtasdt0(xn, sz10) = sdtasdt0(sz10, xn)) | (~aElement0(sz10)) | (~aElement0(xn))) <=> ((~aElement0(xn)) | (~aElement0(sz10)) | (sdtasdt0(xn, sz10) = sdtasdt0(sz10, xn)))),
% 162.95/163.20 inference(rewrite,[status(thm)],[])).
% 162.95/163.20 tff(209,plain,
% 162.95/163.20 (((~![W0: $i, W1: $i] : ((sdtasdt0(W0, W1) = sdtasdt0(W1, W0)) | (~aElement0(W1)) | (~aElement0(W0)))) | ((sdtasdt0(xn, sz10) = sdtasdt0(sz10, xn)) | (~aElement0(sz10)) | (~aElement0(xn)))) <=> ((~![W0: $i, W1: $i] : ((sdtasdt0(W0, W1) = sdtasdt0(W1, W0)) | (~aElement0(W1)) | (~aElement0(W0)))) | ((~aElement0(xn)) | (~aElement0(sz10)) | (sdtasdt0(xn, sz10) = sdtasdt0(sz10, xn))))),
% 162.95/163.20 inference(monotonicity,[status(thm)],[208])).
% 162.95/163.20 tff(210,plain,
% 162.95/163.20 (((~![W0: $i, W1: $i] : ((sdtasdt0(W0, W1) = sdtasdt0(W1, W0)) | (~aElement0(W1)) | (~aElement0(W0)))) | ((sdtasdt0(xn, sz10) = sdtasdt0(sz10, xn)) | (~aElement0(sz10)) | (~aElement0(xn)))) <=> ((~![W0: $i, W1: $i] : ((sdtasdt0(W0, W1) = sdtasdt0(W1, W0)) | (~aElement0(W1)) | (~aElement0(W0)))) | (~aElement0(xn)) | (~aElement0(sz10)) | (sdtasdt0(xn, sz10) = sdtasdt0(sz10, xn)))),
% 162.95/163.20 inference(transitivity,[status(thm)],[209, 207])).
% 162.95/163.20 tff(211,plain,
% 162.95/163.20 ((~![W0: $i, W1: $i] : ((sdtasdt0(W0, W1) = sdtasdt0(W1, W0)) | (~aElement0(W1)) | (~aElement0(W0)))) | ((sdtasdt0(xn, sz10) = sdtasdt0(sz10, xn)) | (~aElement0(sz10)) | (~aElement0(xn)))),
% 162.95/163.20 inference(quant_inst,[status(thm)],[])).
% 162.95/163.20 tff(212,plain,
% 162.95/163.20 ((~![W0: $i, W1: $i] : ((sdtasdt0(W0, W1) = sdtasdt0(W1, W0)) | (~aElement0(W1)) | (~aElement0(W0)))) | (~aElement0(xn)) | (~aElement0(sz10)) | (sdtasdt0(xn, sz10) = sdtasdt0(sz10, xn))),
% 162.95/163.20 inference(modus_ponens,[status(thm)],[211, 210])).
% 162.95/163.20 tff(213,plain,
% 162.95/163.20 (sdtasdt0(xn, sz10) = sdtasdt0(sz10, xn)),
% 162.95/163.20 inference(unit_resolution,[status(thm)],[212, 189, 186, 58])).
% 162.95/163.20 tff(214,plain,
% 162.95/163.20 (sdtasdt0(sz10, xn) = sdtasdt0(xn, sz10)),
% 162.95/163.20 inference(symmetry,[status(thm)],[213])).
% 162.95/163.20 tff(215,plain,
% 162.95/163.20 (sdtasdt0(sz10, xn) = xn),
% 162.95/163.20 inference(transitivity,[status(thm)],[214, 206])).
% 162.95/163.20 tff(216,plain,
% 162.95/163.20 (sdtpldt0(sdtasdt0(sz10, xn), sdtpldt0(sdtasdt0(sz10, xm), xx)) = sdtpldt0(xn, sdtpldt0(sdtpldt0(xk, xm), xl))),
% 162.95/163.20 inference(monotonicity,[status(thm)],[215, 200])).
% 162.95/163.20 tff(217,plain,
% 162.95/163.20 (^[W0: $i, W1: $i] : refl((aElement0(sdtasdt0(W0, W1)) | (~aElement0(W1)) | (~aElement0(W0))) <=> (aElement0(sdtasdt0(W0, W1)) | (~aElement0(W1)) | (~aElement0(W0))))),
% 162.95/163.20 inference(bind,[status(th)],[])).
% 162.95/163.20 tff(218,plain,
% 162.95/163.20 (![W0: $i, W1: $i] : (aElement0(sdtasdt0(W0, W1)) | (~aElement0(W1)) | (~aElement0(W0))) <=> ![W0: $i, W1: $i] : (aElement0(sdtasdt0(W0, W1)) | (~aElement0(W1)) | (~aElement0(W0)))),
% 162.95/163.20 inference(quant_intro,[status(thm)],[217])).
% 162.95/163.20 tff(219,plain,
% 162.95/163.20 (^[W0: $i, W1: $i] : trans(monotonicity(trans(monotonicity(rewrite((aElement0(W0) & aElement0(W1)) <=> (~((~aElement0(W1)) | (~aElement0(W0))))), ((~(aElement0(W0) & aElement0(W1))) <=> (~(~((~aElement0(W1)) | (~aElement0(W0))))))), rewrite((~(~((~aElement0(W1)) | (~aElement0(W0))))) <=> ((~aElement0(W1)) | (~aElement0(W0)))), ((~(aElement0(W0) & aElement0(W1))) <=> ((~aElement0(W1)) | (~aElement0(W0))))), ((aElement0(sdtasdt0(W0, W1)) | (~(aElement0(W0) & aElement0(W1)))) <=> (aElement0(sdtasdt0(W0, W1)) | ((~aElement0(W1)) | (~aElement0(W0)))))), rewrite((aElement0(sdtasdt0(W0, W1)) | ((~aElement0(W1)) | (~aElement0(W0)))) <=> (aElement0(sdtasdt0(W0, W1)) | (~aElement0(W1)) | (~aElement0(W0)))), ((aElement0(sdtasdt0(W0, W1)) | (~(aElement0(W0) & aElement0(W1)))) <=> (aElement0(sdtasdt0(W0, W1)) | (~aElement0(W1)) | (~aElement0(W0)))))),
% 162.95/163.20 inference(bind,[status(th)],[])).
% 162.95/163.20 tff(220,plain,
% 162.95/163.20 (![W0: $i, W1: $i] : (aElement0(sdtasdt0(W0, W1)) | (~(aElement0(W0) & aElement0(W1)))) <=> ![W0: $i, W1: $i] : (aElement0(sdtasdt0(W0, W1)) | (~aElement0(W1)) | (~aElement0(W0)))),
% 162.95/163.20 inference(quant_intro,[status(thm)],[219])).
% 162.95/163.20 tff(221,plain,
% 162.95/163.20 (![W0: $i, W1: $i] : (aElement0(sdtasdt0(W0, W1)) | (~(aElement0(W0) & aElement0(W1)))) <=> ![W0: $i, W1: $i] : (aElement0(sdtasdt0(W0, W1)) | (~(aElement0(W0) & aElement0(W1))))),
% 162.95/163.20 inference(rewrite,[status(thm)],[])).
% 162.95/163.20 tff(222,plain,
% 162.95/163.20 (^[W0: $i, W1: $i] : rewrite(((aElement0(W0) & aElement0(W1)) => aElement0(sdtasdt0(W0, W1))) <=> (aElement0(sdtasdt0(W0, W1)) | (~(aElement0(W0) & aElement0(W1)))))),
% 162.95/163.20 inference(bind,[status(th)],[])).
% 162.95/163.20 tff(223,plain,
% 162.95/163.20 (![W0: $i, W1: $i] : ((aElement0(W0) & aElement0(W1)) => aElement0(sdtasdt0(W0, W1))) <=> ![W0: $i, W1: $i] : (aElement0(sdtasdt0(W0, W1)) | (~(aElement0(W0) & aElement0(W1))))),
% 162.95/163.20 inference(quant_intro,[status(thm)],[222])).
% 162.95/163.20 tff(224,axiom,(![W0: $i, W1: $i] : ((aElement0(W0) & aElement0(W1)) => aElement0(sdtasdt0(W0, W1)))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','mSortsB_02')).
% 162.95/163.20 tff(225,plain,
% 162.95/163.20 (![W0: $i, W1: $i] : (aElement0(sdtasdt0(W0, W1)) | (~(aElement0(W0) & aElement0(W1))))),
% 162.95/163.20 inference(modus_ponens,[status(thm)],[224, 223])).
% 162.95/163.20 tff(226,plain,
% 162.95/163.20 (![W0: $i, W1: $i] : (aElement0(sdtasdt0(W0, W1)) | (~(aElement0(W0) & aElement0(W1))))),
% 162.95/163.20 inference(modus_ponens,[status(thm)],[225, 221])).
% 162.95/163.20 tff(227,plain,(
% 162.95/163.20 ![W0: $i, W1: $i] : (aElement0(sdtasdt0(W0, W1)) | (~(aElement0(W0) & aElement0(W1))))),
% 162.95/163.20 inference(skolemize,[status(sab)],[226])).
% 162.95/163.20 tff(228,plain,
% 162.95/163.20 (![W0: $i, W1: $i] : (aElement0(sdtasdt0(W0, W1)) | (~aElement0(W1)) | (~aElement0(W0)))),
% 162.95/163.20 inference(modus_ponens,[status(thm)],[227, 220])).
% 162.95/163.20 tff(229,plain,
% 162.95/163.20 (![W0: $i, W1: $i] : (aElement0(sdtasdt0(W0, W1)) | (~aElement0(W1)) | (~aElement0(W0)))),
% 162.95/163.20 inference(modus_ponens,[status(thm)],[228, 218])).
% 162.95/163.20 tff(230,plain,
% 162.95/163.20 (((~![W0: $i, W1: $i] : (aElement0(sdtasdt0(W0, W1)) | (~aElement0(W1)) | (~aElement0(W0)))) | ((~aElement0(xm)) | (~aElement0(sz10)) | aElement0(sdtasdt0(sz10, xm)))) <=> ((~![W0: $i, W1: $i] : (aElement0(sdtasdt0(W0, W1)) | (~aElement0(W1)) | (~aElement0(W0)))) | (~aElement0(xm)) | (~aElement0(sz10)) | aElement0(sdtasdt0(sz10, xm)))),
% 162.95/163.20 inference(rewrite,[status(thm)],[])).
% 162.95/163.20 tff(231,plain,
% 162.95/163.20 ((aElement0(sdtasdt0(sz10, xm)) | (~aElement0(xm)) | (~aElement0(sz10))) <=> ((~aElement0(xm)) | (~aElement0(sz10)) | aElement0(sdtasdt0(sz10, xm)))),
% 162.95/163.20 inference(rewrite,[status(thm)],[])).
% 162.95/163.20 tff(232,plain,
% 162.95/163.20 (((~![W0: $i, W1: $i] : (aElement0(sdtasdt0(W0, W1)) | (~aElement0(W1)) | (~aElement0(W0)))) | (aElement0(sdtasdt0(sz10, xm)) | (~aElement0(xm)) | (~aElement0(sz10)))) <=> ((~![W0: $i, W1: $i] : (aElement0(sdtasdt0(W0, W1)) | (~aElement0(W1)) | (~aElement0(W0)))) | ((~aElement0(xm)) | (~aElement0(sz10)) | aElement0(sdtasdt0(sz10, xm))))),
% 162.95/163.20 inference(monotonicity,[status(thm)],[231])).
% 162.95/163.20 tff(233,plain,
% 162.95/163.20 (((~![W0: $i, W1: $i] : (aElement0(sdtasdt0(W0, W1)) | (~aElement0(W1)) | (~aElement0(W0)))) | (aElement0(sdtasdt0(sz10, xm)) | (~aElement0(xm)) | (~aElement0(sz10)))) <=> ((~![W0: $i, W1: $i] : (aElement0(sdtasdt0(W0, W1)) | (~aElement0(W1)) | (~aElement0(W0)))) | (~aElement0(xm)) | (~aElement0(sz10)) | aElement0(sdtasdt0(sz10, xm)))),
% 162.95/163.20 inference(transitivity,[status(thm)],[232, 230])).
% 162.95/163.20 tff(234,plain,
% 162.95/163.20 ((~![W0: $i, W1: $i] : (aElement0(sdtasdt0(W0, W1)) | (~aElement0(W1)) | (~aElement0(W0)))) | (aElement0(sdtasdt0(sz10, xm)) | (~aElement0(xm)) | (~aElement0(sz10)))),
% 162.95/163.20 inference(quant_inst,[status(thm)],[])).
% 162.95/163.20 tff(235,plain,
% 162.95/163.20 ((~![W0: $i, W1: $i] : (aElement0(sdtasdt0(W0, W1)) | (~aElement0(W1)) | (~aElement0(W0)))) | (~aElement0(xm)) | (~aElement0(sz10)) | aElement0(sdtasdt0(sz10, xm))),
% 162.95/163.20 inference(modus_ponens,[status(thm)],[234, 233])).
% 162.95/163.20 tff(236,plain,
% 162.95/163.20 (aElement0(sdtasdt0(sz10, xm))),
% 162.95/163.20 inference(unit_resolution,[status(thm)],[235, 189, 229, 134])).
% 162.95/163.20 tff(237,plain,
% 162.95/163.20 (((~![W0: $i, W1: $i] : (aElement0(sdtasdt0(W0, W1)) | (~aElement0(W1)) | (~aElement0(W0)))) | ((~aElement0(xn)) | (~aElement0(sz10)) | aElement0(sdtasdt0(sz10, xn)))) <=> ((~![W0: $i, W1: $i] : (aElement0(sdtasdt0(W0, W1)) | (~aElement0(W1)) | (~aElement0(W0)))) | (~aElement0(xn)) | (~aElement0(sz10)) | aElement0(sdtasdt0(sz10, xn)))),
% 162.95/163.20 inference(rewrite,[status(thm)],[])).
% 162.95/163.20 tff(238,plain,
% 162.95/163.20 ((aElement0(sdtasdt0(sz10, xn)) | (~aElement0(xn)) | (~aElement0(sz10))) <=> ((~aElement0(xn)) | (~aElement0(sz10)) | aElement0(sdtasdt0(sz10, xn)))),
% 162.95/163.20 inference(rewrite,[status(thm)],[])).
% 162.95/163.20 tff(239,plain,
% 162.95/163.20 (((~![W0: $i, W1: $i] : (aElement0(sdtasdt0(W0, W1)) | (~aElement0(W1)) | (~aElement0(W0)))) | (aElement0(sdtasdt0(sz10, xn)) | (~aElement0(xn)) | (~aElement0(sz10)))) <=> ((~![W0: $i, W1: $i] : (aElement0(sdtasdt0(W0, W1)) | (~aElement0(W1)) | (~aElement0(W0)))) | ((~aElement0(xn)) | (~aElement0(sz10)) | aElement0(sdtasdt0(sz10, xn))))),
% 162.95/163.20 inference(monotonicity,[status(thm)],[238])).
% 162.95/163.20 tff(240,plain,
% 162.95/163.20 (((~![W0: $i, W1: $i] : (aElement0(sdtasdt0(W0, W1)) | (~aElement0(W1)) | (~aElement0(W0)))) | (aElement0(sdtasdt0(sz10, xn)) | (~aElement0(xn)) | (~aElement0(sz10)))) <=> ((~![W0: $i, W1: $i] : (aElement0(sdtasdt0(W0, W1)) | (~aElement0(W1)) | (~aElement0(W0)))) | (~aElement0(xn)) | (~aElement0(sz10)) | aElement0(sdtasdt0(sz10, xn)))),
% 162.95/163.20 inference(transitivity,[status(thm)],[239, 237])).
% 162.95/163.20 tff(241,plain,
% 162.95/163.20 ((~![W0: $i, W1: $i] : (aElement0(sdtasdt0(W0, W1)) | (~aElement0(W1)) | (~aElement0(W0)))) | (aElement0(sdtasdt0(sz10, xn)) | (~aElement0(xn)) | (~aElement0(sz10)))),
% 162.95/163.20 inference(quant_inst,[status(thm)],[])).
% 162.95/163.20 tff(242,plain,
% 162.95/163.20 ((~![W0: $i, W1: $i] : (aElement0(sdtasdt0(W0, W1)) | (~aElement0(W1)) | (~aElement0(W0)))) | (~aElement0(xn)) | (~aElement0(sz10)) | aElement0(sdtasdt0(sz10, xn))),
% 162.95/163.20 inference(modus_ponens,[status(thm)],[241, 240])).
% 162.95/163.20 tff(243,plain,
% 162.95/163.20 (aElement0(sdtasdt0(sz10, xn))),
% 162.95/163.20 inference(unit_resolution,[status(thm)],[242, 189, 229, 58])).
% 162.95/163.20 tff(244,plain,
% 162.95/163.20 (?[W0: $i, W1: $i] : (aElementOf0(W0, xI) & aElementOf0(W1, xJ) & (sdtpldt0(W0, W1) = xx)) <=> ?[W0: $i, W1: $i] : (aElementOf0(W0, xI) & aElementOf0(W1, xJ) & (sdtpldt0(W0, W1) = xx))),
% 162.95/163.20 inference(rewrite,[status(thm)],[])).
% 162.95/163.20 tff(245,plain,
% 162.95/163.20 (^[W0: $i, W1: $i] : rewrite(((aElementOf0(W0, xI) & aElementOf0(W1, xJ)) & (sdtpldt0(W0, W1) = xx)) <=> (aElementOf0(W0, xI) & aElementOf0(W1, xJ) & (sdtpldt0(W0, W1) = xx)))),
% 162.95/163.20 inference(bind,[status(th)],[])).
% 162.95/163.20 tff(246,plain,
% 162.95/163.20 (?[W0: $i, W1: $i] : ((aElementOf0(W0, xI) & aElementOf0(W1, xJ)) & (sdtpldt0(W0, W1) = xx)) <=> ?[W0: $i, W1: $i] : (aElementOf0(W0, xI) & aElementOf0(W1, xJ) & (sdtpldt0(W0, W1) = xx))),
% 162.95/163.20 inference(quant_intro,[status(thm)],[245])).
% 162.95/163.20 tff(247,axiom,((((?[W0: $i, W1: $i] : ((aElementOf0(W0, xI) & aElementOf0(W1, xJ)) & (sdtpldt0(W0, W1) = xx)) & aElementOf0(xx, sdtpldt1(xI, xJ))) & ?[W0: $i, W1: $i] : ((aElementOf0(W0, xI) & aElementOf0(W1, xJ)) & (sdtpldt0(W0, W1) = xy))) & aElementOf0(xy, sdtpldt1(xI, xJ))) & aElement0(xz)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','m__901')).
% 162.95/163.20 tff(248,plain,
% 162.95/163.20 (((?[W0: $i, W1: $i] : ((aElementOf0(W0, xI) & aElementOf0(W1, xJ)) & (sdtpldt0(W0, W1) = xx)) & aElementOf0(xx, sdtpldt1(xI, xJ))) & ?[W0: $i, W1: $i] : ((aElementOf0(W0, xI) & aElementOf0(W1, xJ)) & (sdtpldt0(W0, W1) = xy))) & aElementOf0(xy, sdtpldt1(xI, xJ))),
% 162.95/163.20 inference(and_elim,[status(thm)],[247])).
% 162.95/163.20 tff(249,plain,
% 162.95/163.20 ((?[W0: $i, W1: $i] : ((aElementOf0(W0, xI) & aElementOf0(W1, xJ)) & (sdtpldt0(W0, W1) = xx)) & aElementOf0(xx, sdtpldt1(xI, xJ))) & ?[W0: $i, W1: $i] : ((aElementOf0(W0, xI) & aElementOf0(W1, xJ)) & (sdtpldt0(W0, W1) = xy))),
% 162.95/163.20 inference(and_elim,[status(thm)],[248])).
% 162.95/163.20 tff(250,plain,
% 162.95/163.20 (?[W0: $i, W1: $i] : ((aElementOf0(W0, xI) & aElementOf0(W1, xJ)) & (sdtpldt0(W0, W1) = xx)) & aElementOf0(xx, sdtpldt1(xI, xJ))),
% 162.95/163.20 inference(and_elim,[status(thm)],[249])).
% 162.95/163.20 tff(251,plain,
% 162.95/163.20 (?[W0: $i, W1: $i] : ((aElementOf0(W0, xI) & aElementOf0(W1, xJ)) & (sdtpldt0(W0, W1) = xx))),
% 162.95/163.20 inference(and_elim,[status(thm)],[250])).
% 162.95/163.20 tff(252,plain,
% 162.95/163.20 (?[W0: $i, W1: $i] : (aElementOf0(W0, xI) & aElementOf0(W1, xJ) & (sdtpldt0(W0, W1) = xx))),
% 162.95/163.20 inference(modus_ponens,[status(thm)],[251, 246])).
% 162.95/163.20 tff(253,plain,
% 162.95/163.20 (?[W0: $i, W1: $i] : (aElementOf0(W0, xI) & aElementOf0(W1, xJ) & (sdtpldt0(W0, W1) = xx))),
% 162.95/163.20 inference(modus_ponens,[status(thm)],[252, 244])).
% 162.95/163.20 tff(254,plain,(
% 162.95/163.20 aElementOf0(W0!12, xI) & aElementOf0(W1!11, xJ) & (sdtpldt0(W0!12, W1!11) = xx)),
% 162.95/163.20 inference(skolemize,[status(sab)],[253])).
% 162.95/163.20 tff(255,plain,
% 162.95/163.20 (sdtpldt0(W0!12, W1!11) = xx),
% 162.95/163.20 inference(and_elim,[status(thm)],[254])).
% 162.95/163.20 tff(256,plain,
% 162.95/163.20 (aElement0(sdtpldt0(W0!12, W1!11)) <=> aElement0(xx)),
% 162.95/163.20 inference(monotonicity,[status(thm)],[255])).
% 162.95/163.20 tff(257,plain,
% 162.95/163.20 (aElementOf0(W0!12, xI)),
% 162.95/163.20 inference(and_elim,[status(thm)],[254])).
% 162.95/163.20 tff(258,plain,
% 162.95/163.20 (((~![W1: $i] : (aElement0(W1) | (~aElementOf0(W1, xI)))) | (aElement0(W0!12) | (~aElementOf0(W0!12, xI)))) <=> ((~![W1: $i] : (aElement0(W1) | (~aElementOf0(W1, xI)))) | aElement0(W0!12) | (~aElementOf0(W0!12, xI)))),
% 162.95/163.20 inference(rewrite,[status(thm)],[])).
% 162.95/163.20 tff(259,plain,
% 162.95/163.20 ((~![W1: $i] : (aElement0(W1) | (~aElementOf0(W1, xI)))) | (aElement0(W0!12) | (~aElementOf0(W0!12, xI)))),
% 162.95/163.20 inference(quant_inst,[status(thm)],[])).
% 162.95/163.20 tff(260,plain,
% 162.95/163.20 ((~![W1: $i] : (aElement0(W1) | (~aElementOf0(W1, xI)))) | aElement0(W0!12) | (~aElementOf0(W0!12, xI))),
% 162.95/163.20 inference(modus_ponens,[status(thm)],[259, 258])).
% 162.95/163.20 tff(261,plain,
% 162.95/163.20 (aElement0(W0!12)),
% 162.95/163.20 inference(unit_resolution,[status(thm)],[260, 257, 41])).
% 162.95/163.20 tff(262,plain,
% 162.95/163.20 (aElementOf0(W1!11, xJ)),
% 162.95/163.20 inference(and_elim,[status(thm)],[254])).
% 162.95/163.20 tff(263,plain,
% 162.95/163.20 (((~![W1: $i] : (aElement0(W1) | (~aElementOf0(W1, xJ)))) | (aElement0(W1!11) | (~aElementOf0(W1!11, xJ)))) <=> ((~![W1: $i] : (aElement0(W1) | (~aElementOf0(W1, xJ)))) | aElement0(W1!11) | (~aElementOf0(W1!11, xJ)))),
% 162.95/163.20 inference(rewrite,[status(thm)],[])).
% 162.95/163.20 tff(264,plain,
% 162.95/163.20 ((~![W1: $i] : (aElement0(W1) | (~aElementOf0(W1, xJ)))) | (aElement0(W1!11) | (~aElementOf0(W1!11, xJ)))),
% 162.95/163.20 inference(quant_inst,[status(thm)],[])).
% 162.95/163.20 tff(265,plain,
% 162.95/163.20 ((~![W1: $i] : (aElement0(W1) | (~aElementOf0(W1, xJ)))) | aElement0(W1!11) | (~aElementOf0(W1!11, xJ))),
% 162.95/163.20 inference(modus_ponens,[status(thm)],[264, 263])).
% 162.95/163.20 tff(266,plain,
% 162.95/163.20 (aElement0(W1!11)),
% 162.95/163.20 inference(unit_resolution,[status(thm)],[265, 262, 23])).
% 162.95/163.20 tff(267,plain,
% 162.95/163.20 (((~![W0: $i, W1: $i] : (aElement0(sdtpldt0(W0, W1)) | (~aElement0(W1)) | (~aElement0(W0)))) | ((~aElement0(W1!11)) | (~aElement0(W0!12)) | aElement0(sdtpldt0(W0!12, W1!11)))) <=> ((~![W0: $i, W1: $i] : (aElement0(sdtpldt0(W0, W1)) | (~aElement0(W1)) | (~aElement0(W0)))) | (~aElement0(W1!11)) | (~aElement0(W0!12)) | aElement0(sdtpldt0(W0!12, W1!11)))),
% 162.95/163.20 inference(rewrite,[status(thm)],[])).
% 162.95/163.20 tff(268,plain,
% 162.95/163.20 ((aElement0(sdtpldt0(W0!12, W1!11)) | (~aElement0(W1!11)) | (~aElement0(W0!12))) <=> ((~aElement0(W1!11)) | (~aElement0(W0!12)) | aElement0(sdtpldt0(W0!12, W1!11)))),
% 162.95/163.20 inference(rewrite,[status(thm)],[])).
% 162.95/163.20 tff(269,plain,
% 162.95/163.20 (((~![W0: $i, W1: $i] : (aElement0(sdtpldt0(W0, W1)) | (~aElement0(W1)) | (~aElement0(W0)))) | (aElement0(sdtpldt0(W0!12, W1!11)) | (~aElement0(W1!11)) | (~aElement0(W0!12)))) <=> ((~![W0: $i, W1: $i] : (aElement0(sdtpldt0(W0, W1)) | (~aElement0(W1)) | (~aElement0(W0)))) | ((~aElement0(W1!11)) | (~aElement0(W0!12)) | aElement0(sdtpldt0(W0!12, W1!11))))),
% 162.95/163.20 inference(monotonicity,[status(thm)],[268])).
% 162.95/163.20 tff(270,plain,
% 162.95/163.20 (((~![W0: $i, W1: $i] : (aElement0(sdtpldt0(W0, W1)) | (~aElement0(W1)) | (~aElement0(W0)))) | (aElement0(sdtpldt0(W0!12, W1!11)) | (~aElement0(W1!11)) | (~aElement0(W0!12)))) <=> ((~![W0: $i, W1: $i] : (aElement0(sdtpldt0(W0, W1)) | (~aElement0(W1)) | (~aElement0(W0)))) | (~aElement0(W1!11)) | (~aElement0(W0!12)) | aElement0(sdtpldt0(W0!12, W1!11)))),
% 162.95/163.20 inference(transitivity,[status(thm)],[269, 267])).
% 162.95/163.20 tff(271,plain,
% 162.95/163.20 ((~![W0: $i, W1: $i] : (aElement0(sdtpldt0(W0, W1)) | (~aElement0(W1)) | (~aElement0(W0)))) | (aElement0(sdtpldt0(W0!12, W1!11)) | (~aElement0(W1!11)) | (~aElement0(W0!12)))),
% 162.95/163.20 inference(quant_inst,[status(thm)],[])).
% 162.95/163.20 tff(272,plain,
% 162.95/163.20 ((~![W0: $i, W1: $i] : (aElement0(sdtpldt0(W0, W1)) | (~aElement0(W1)) | (~aElement0(W0)))) | (~aElement0(W1!11)) | (~aElement0(W0!12)) | aElement0(sdtpldt0(W0!12, W1!11))),
% 162.95/163.20 inference(modus_ponens,[status(thm)],[271, 270])).
% 162.95/163.20 tff(273,plain,
% 162.95/163.20 ((~aElement0(W1!11)) | (~aElement0(W0!12)) | aElement0(sdtpldt0(W0!12, W1!11))),
% 162.95/163.20 inference(unit_resolution,[status(thm)],[272, 92])).
% 162.95/163.20 tff(274,plain,
% 162.95/163.20 (aElement0(sdtpldt0(W0!12, W1!11))),
% 162.95/163.20 inference(unit_resolution,[status(thm)],[273, 266, 261])).
% 162.95/163.20 tff(275,plain,
% 162.95/163.20 (aElement0(xx)),
% 162.95/163.20 inference(modus_ponens,[status(thm)],[274, 256])).
% 162.95/163.20 tff(276,plain,
% 162.95/163.20 (((~![W0: $i, W1: $i, W2: $i] : ((sdtpldt0(sdtpldt0(W0, W1), W2) = sdtpldt0(W0, sdtpldt0(W1, W2))) | (~aElement0(W2)) | (~aElement0(W1)) | (~aElement0(W0)))) | ((~aElement0(xx)) | (~aElement0(sdtasdt0(sz10, xm))) | (~aElement0(sdtasdt0(sz10, xn))) | (sdtpldt0(sdtpldt0(sdtasdt0(sz10, xn), sdtasdt0(sz10, xm)), xx) = sdtpldt0(sdtasdt0(sz10, xn), sdtpldt0(sdtasdt0(sz10, xm), xx))))) <=> ((~![W0: $i, W1: $i, W2: $i] : ((sdtpldt0(sdtpldt0(W0, W1), W2) = sdtpldt0(W0, sdtpldt0(W1, W2))) | (~aElement0(W2)) | (~aElement0(W1)) | (~aElement0(W0)))) | (~aElement0(xx)) | (~aElement0(sdtasdt0(sz10, xm))) | (~aElement0(sdtasdt0(sz10, xn))) | (sdtpldt0(sdtpldt0(sdtasdt0(sz10, xn), sdtasdt0(sz10, xm)), xx) = sdtpldt0(sdtasdt0(sz10, xn), sdtpldt0(sdtasdt0(sz10, xm), xx))))),
% 162.95/163.20 inference(rewrite,[status(thm)],[])).
% 162.95/163.20 tff(277,plain,
% 162.95/163.20 (((sdtpldt0(sdtpldt0(sdtasdt0(sz10, xn), sdtasdt0(sz10, xm)), xx) = sdtpldt0(sdtasdt0(sz10, xn), sdtpldt0(sdtasdt0(sz10, xm), xx))) | (~aElement0(xx)) | (~aElement0(sdtasdt0(sz10, xm))) | (~aElement0(sdtasdt0(sz10, xn)))) <=> ((~aElement0(xx)) | (~aElement0(sdtasdt0(sz10, xm))) | (~aElement0(sdtasdt0(sz10, xn))) | (sdtpldt0(sdtpldt0(sdtasdt0(sz10, xn), sdtasdt0(sz10, xm)), xx) = sdtpldt0(sdtasdt0(sz10, xn), sdtpldt0(sdtasdt0(sz10, xm), xx))))),
% 162.95/163.20 inference(rewrite,[status(thm)],[])).
% 162.95/163.20 tff(278,plain,
% 162.95/163.20 (((~![W0: $i, W1: $i, W2: $i] : ((sdtpldt0(sdtpldt0(W0, W1), W2) = sdtpldt0(W0, sdtpldt0(W1, W2))) | (~aElement0(W2)) | (~aElement0(W1)) | (~aElement0(W0)))) | ((sdtpldt0(sdtpldt0(sdtasdt0(sz10, xn), sdtasdt0(sz10, xm)), xx) = sdtpldt0(sdtasdt0(sz10, xn), sdtpldt0(sdtasdt0(sz10, xm), xx))) | (~aElement0(xx)) | (~aElement0(sdtasdt0(sz10, xm))) | (~aElement0(sdtasdt0(sz10, xn))))) <=> ((~![W0: $i, W1: $i, W2: $i] : ((sdtpldt0(sdtpldt0(W0, W1), W2) = sdtpldt0(W0, sdtpldt0(W1, W2))) | (~aElement0(W2)) | (~aElement0(W1)) | (~aElement0(W0)))) | ((~aElement0(xx)) | (~aElement0(sdtasdt0(sz10, xm))) | (~aElement0(sdtasdt0(sz10, xn))) | (sdtpldt0(sdtpldt0(sdtasdt0(sz10, xn), sdtasdt0(sz10, xm)), xx) = sdtpldt0(sdtasdt0(sz10, xn), sdtpldt0(sdtasdt0(sz10, xm), xx)))))),
% 162.95/163.20 inference(monotonicity,[status(thm)],[277])).
% 162.95/163.20 tff(279,plain,
% 162.95/163.20 (((~![W0: $i, W1: $i, W2: $i] : ((sdtpldt0(sdtpldt0(W0, W1), W2) = sdtpldt0(W0, sdtpldt0(W1, W2))) | (~aElement0(W2)) | (~aElement0(W1)) | (~aElement0(W0)))) | ((sdtpldt0(sdtpldt0(sdtasdt0(sz10, xn), sdtasdt0(sz10, xm)), xx) = sdtpldt0(sdtasdt0(sz10, xn), sdtpldt0(sdtasdt0(sz10, xm), xx))) | (~aElement0(xx)) | (~aElement0(sdtasdt0(sz10, xm))) | (~aElement0(sdtasdt0(sz10, xn))))) <=> ((~![W0: $i, W1: $i, W2: $i] : ((sdtpldt0(sdtpldt0(W0, W1), W2) = sdtpldt0(W0, sdtpldt0(W1, W2))) | (~aElement0(W2)) | (~aElement0(W1)) | (~aElement0(W0)))) | (~aElement0(xx)) | (~aElement0(sdtasdt0(sz10, xm))) | (~aElement0(sdtasdt0(sz10, xn))) | (sdtpldt0(sdtpldt0(sdtasdt0(sz10, xn), sdtasdt0(sz10, xm)), xx) = sdtpldt0(sdtasdt0(sz10, xn), sdtpldt0(sdtasdt0(sz10, xm), xx))))),
% 162.95/163.20 inference(transitivity,[status(thm)],[278, 276])).
% 162.95/163.20 tff(280,plain,
% 162.95/163.20 ((~![W0: $i, W1: $i, W2: $i] : ((sdtpldt0(sdtpldt0(W0, W1), W2) = sdtpldt0(W0, sdtpldt0(W1, W2))) | (~aElement0(W2)) | (~aElement0(W1)) | (~aElement0(W0)))) | ((sdtpldt0(sdtpldt0(sdtasdt0(sz10, xn), sdtasdt0(sz10, xm)), xx) = sdtpldt0(sdtasdt0(sz10, xn), sdtpldt0(sdtasdt0(sz10, xm), xx))) | (~aElement0(xx)) | (~aElement0(sdtasdt0(sz10, xm))) | (~aElement0(sdtasdt0(sz10, xn))))),
% 162.95/163.20 inference(quant_inst,[status(thm)],[])).
% 162.95/163.20 tff(281,plain,
% 162.95/163.20 ((~![W0: $i, W1: $i, W2: $i] : ((sdtpldt0(sdtpldt0(W0, W1), W2) = sdtpldt0(W0, sdtpldt0(W1, W2))) | (~aElement0(W2)) | (~aElement0(W1)) | (~aElement0(W0)))) | (~aElement0(xx)) | (~aElement0(sdtasdt0(sz10, xm))) | (~aElement0(sdtasdt0(sz10, xn))) | (sdtpldt0(sdtpldt0(sdtasdt0(sz10, xn), sdtasdt0(sz10, xm)), xx) = sdtpldt0(sdtasdt0(sz10, xn), sdtpldt0(sdtasdt0(sz10, xm), xx)))),
% 162.95/163.20 inference(modus_ponens,[status(thm)],[280, 279])).
% 162.95/163.20 tff(282,plain,
% 162.95/163.20 (sdtpldt0(sdtpldt0(sdtasdt0(sz10, xn), sdtasdt0(sz10, xm)), xx) = sdtpldt0(sdtasdt0(sz10, xn), sdtpldt0(sdtasdt0(sz10, xm), xx))),
% 162.95/163.20 inference(unit_resolution,[status(thm)],[281, 71, 275, 243, 236])).
% 162.95/163.20 tff(283,plain,
% 162.95/163.20 (sdtpldt0(sdtasdt0(sz10, xn), sdtasdt0(sz10, xm)) = sdtpldt0(xn, xm)),
% 162.95/163.20 inference(monotonicity,[status(thm)],[215, 198])).
% 162.95/163.20 tff(284,plain,
% 162.95/163.20 (sdtpldt0(xn, xm) = sdtpldt0(sdtasdt0(sz10, xn), sdtasdt0(sz10, xm))),
% 162.95/163.20 inference(symmetry,[status(thm)],[283])).
% 162.95/163.20 tff(285,plain,
% 162.95/163.20 (((~![W0: $i, W1: $i] : ((sdtpldt0(W0, W1) = sdtpldt0(W1, W0)) | (~aElement0(W1)) | (~aElement0(W0)))) | ((~aElement0(xn)) | (~aElement0(xm)) | (sdtpldt0(xn, xm) = sdtpldt0(xm, xn)))) <=> ((~![W0: $i, W1: $i] : ((sdtpldt0(W0, W1) = sdtpldt0(W1, W0)) | (~aElement0(W1)) | (~aElement0(W0)))) | (~aElement0(xn)) | (~aElement0(xm)) | (sdtpldt0(xn, xm) = sdtpldt0(xm, xn)))),
% 162.95/163.20 inference(rewrite,[status(thm)],[])).
% 162.95/163.20 tff(286,plain,
% 162.95/163.20 (((sdtpldt0(xn, xm) = sdtpldt0(xm, xn)) | (~aElement0(xm)) | (~aElement0(xn))) <=> ((~aElement0(xn)) | (~aElement0(xm)) | (sdtpldt0(xn, xm) = sdtpldt0(xm, xn)))),
% 162.95/163.20 inference(rewrite,[status(thm)],[])).
% 162.95/163.20 tff(287,plain,
% 162.95/163.20 (((~![W0: $i, W1: $i] : ((sdtpldt0(W0, W1) = sdtpldt0(W1, W0)) | (~aElement0(W1)) | (~aElement0(W0)))) | ((sdtpldt0(xn, xm) = sdtpldt0(xm, xn)) | (~aElement0(xm)) | (~aElement0(xn)))) <=> ((~![W0: $i, W1: $i] : ((sdtpldt0(W0, W1) = sdtpldt0(W1, W0)) | (~aElement0(W1)) | (~aElement0(W0)))) | ((~aElement0(xn)) | (~aElement0(xm)) | (sdtpldt0(xn, xm) = sdtpldt0(xm, xn))))),
% 162.95/163.20 inference(monotonicity,[status(thm)],[286])).
% 162.95/163.20 tff(288,plain,
% 162.95/163.20 (((~![W0: $i, W1: $i] : ((sdtpldt0(W0, W1) = sdtpldt0(W1, W0)) | (~aElement0(W1)) | (~aElement0(W0)))) | ((sdtpldt0(xn, xm) = sdtpldt0(xm, xn)) | (~aElement0(xm)) | (~aElement0(xn)))) <=> ((~![W0: $i, W1: $i] : ((sdtpldt0(W0, W1) = sdtpldt0(W1, W0)) | (~aElement0(W1)) | (~aElement0(W0)))) | (~aElement0(xn)) | (~aElement0(xm)) | (sdtpldt0(xn, xm) = sdtpldt0(xm, xn)))),
% 162.95/163.20 inference(transitivity,[status(thm)],[287, 285])).
% 162.95/163.20 tff(289,plain,
% 162.95/163.20 ((~![W0: $i, W1: $i] : ((sdtpldt0(W0, W1) = sdtpldt0(W1, W0)) | (~aElement0(W1)) | (~aElement0(W0)))) | ((sdtpldt0(xn, xm) = sdtpldt0(xm, xn)) | (~aElement0(xm)) | (~aElement0(xn)))),
% 162.95/163.20 inference(quant_inst,[status(thm)],[])).
% 162.95/163.20 tff(290,plain,
% 162.95/163.20 ((~![W0: $i, W1: $i] : ((sdtpldt0(W0, W1) = sdtpldt0(W1, W0)) | (~aElement0(W1)) | (~aElement0(W0)))) | (~aElement0(xn)) | (~aElement0(xm)) | (sdtpldt0(xn, xm) = sdtpldt0(xm, xn))),
% 162.95/163.20 inference(modus_ponens,[status(thm)],[289, 288])).
% 162.95/163.20 tff(291,plain,
% 162.95/163.20 ((~aElement0(xn)) | (~aElement0(xm)) | (sdtpldt0(xn, xm) = sdtpldt0(xm, xn))),
% 162.95/163.20 inference(unit_resolution,[status(thm)],[290, 112])).
% 162.95/163.20 tff(292,plain,
% 162.95/163.20 (sdtpldt0(xn, xm) = sdtpldt0(xm, xn)),
% 162.95/163.20 inference(unit_resolution,[status(thm)],[291, 58, 134])).
% 162.95/163.20 tff(293,plain,
% 162.95/163.20 (sdtpldt0(xm, xn) = sdtpldt0(xn, xm)),
% 162.95/163.20 inference(symmetry,[status(thm)],[292])).
% 162.95/163.20 tff(294,plain,
% 162.95/163.20 ((xy = sdtpldt0(xm, xn)) <=> (xy = sdtpldt0(xm, xn))),
% 162.95/163.20 inference(rewrite,[status(thm)],[])).
% 162.95/163.20 tff(295,plain,
% 162.95/163.20 (xy = sdtpldt0(xm, xn)),
% 162.95/163.20 inference(and_elim,[status(thm)],[51])).
% 162.95/163.20 tff(296,plain,
% 162.95/163.20 (xy = sdtpldt0(xm, xn)),
% 162.95/163.20 inference(modus_ponens,[status(thm)],[295, 294])).
% 162.95/163.20 tff(297,plain,
% 162.95/163.20 (xy = sdtpldt0(sdtasdt0(sz10, xn), sdtasdt0(sz10, xm))),
% 162.95/163.20 inference(transitivity,[status(thm)],[296, 293, 284])).
% 162.95/163.20 tff(298,plain,
% 162.95/163.20 (sdtpldt0(xy, xx) = sdtpldt0(sdtpldt0(sdtasdt0(sz10, xn), sdtasdt0(sz10, xm)), xx)),
% 162.95/163.20 inference(monotonicity,[status(thm)],[297])).
% 162.95/163.20 tff(299,plain,
% 162.95/163.20 (?[W0: $i, W1: $i] : (aElementOf0(W0, xI) & aElementOf0(W1, xJ) & (sdtpldt0(W0, W1) = xy)) <=> ?[W0: $i, W1: $i] : (aElementOf0(W0, xI) & aElementOf0(W1, xJ) & (sdtpldt0(W0, W1) = xy))),
% 162.95/163.20 inference(rewrite,[status(thm)],[])).
% 162.95/163.20 tff(300,plain,
% 162.95/163.20 (^[W0: $i, W1: $i] : rewrite(((aElementOf0(W0, xI) & aElementOf0(W1, xJ)) & (sdtpldt0(W0, W1) = xy)) <=> (aElementOf0(W0, xI) & aElementOf0(W1, xJ) & (sdtpldt0(W0, W1) = xy)))),
% 162.95/163.20 inference(bind,[status(th)],[])).
% 162.95/163.20 tff(301,plain,
% 162.95/163.20 (?[W0: $i, W1: $i] : ((aElementOf0(W0, xI) & aElementOf0(W1, xJ)) & (sdtpldt0(W0, W1) = xy)) <=> ?[W0: $i, W1: $i] : (aElementOf0(W0, xI) & aElementOf0(W1, xJ) & (sdtpldt0(W0, W1) = xy))),
% 162.95/163.20 inference(quant_intro,[status(thm)],[300])).
% 162.95/163.20 tff(302,plain,
% 162.95/163.20 (?[W0: $i, W1: $i] : ((aElementOf0(W0, xI) & aElementOf0(W1, xJ)) & (sdtpldt0(W0, W1) = xy))),
% 162.95/163.20 inference(and_elim,[status(thm)],[249])).
% 162.95/163.20 tff(303,plain,
% 162.95/163.20 (?[W0: $i, W1: $i] : (aElementOf0(W0, xI) & aElementOf0(W1, xJ) & (sdtpldt0(W0, W1) = xy))),
% 162.95/163.20 inference(modus_ponens,[status(thm)],[302, 301])).
% 162.95/163.20 tff(304,plain,
% 162.95/163.20 (?[W0: $i, W1: $i] : (aElementOf0(W0, xI) & aElementOf0(W1, xJ) & (sdtpldt0(W0, W1) = xy))),
% 162.95/163.20 inference(modus_ponens,[status(thm)],[303, 299])).
% 162.95/163.20 tff(305,plain,(
% 162.95/163.20 aElementOf0(W0!14, xI) & aElementOf0(W1!13, xJ) & (sdtpldt0(W0!14, W1!13) = xy)),
% 162.95/163.20 inference(skolemize,[status(sab)],[304])).
% 162.95/163.20 tff(306,plain,
% 162.95/163.20 (sdtpldt0(W0!14, W1!13) = xy),
% 162.95/163.20 inference(and_elim,[status(thm)],[305])).
% 162.95/163.20 tff(307,plain,
% 162.95/163.20 (aElement0(sdtpldt0(W0!14, W1!13)) <=> aElement0(xy)),
% 162.95/163.20 inference(monotonicity,[status(thm)],[306])).
% 162.95/163.20 tff(308,plain,
% 162.95/163.20 (aElementOf0(W0!14, xI)),
% 162.95/163.20 inference(and_elim,[status(thm)],[305])).
% 162.95/163.20 tff(309,plain,
% 162.95/163.20 (((~![W1: $i] : (aElement0(W1) | (~aElementOf0(W1, xI)))) | (aElement0(W0!14) | (~aElementOf0(W0!14, xI)))) <=> ((~![W1: $i] : (aElement0(W1) | (~aElementOf0(W1, xI)))) | aElement0(W0!14) | (~aElementOf0(W0!14, xI)))),
% 162.95/163.20 inference(rewrite,[status(thm)],[])).
% 162.95/163.20 tff(310,plain,
% 162.95/163.20 ((~![W1: $i] : (aElement0(W1) | (~aElementOf0(W1, xI)))) | (aElement0(W0!14) | (~aElementOf0(W0!14, xI)))),
% 162.95/163.20 inference(quant_inst,[status(thm)],[])).
% 162.95/163.20 tff(311,plain,
% 162.95/163.20 ((~![W1: $i] : (aElement0(W1) | (~aElementOf0(W1, xI)))) | aElement0(W0!14) | (~aElementOf0(W0!14, xI))),
% 162.95/163.20 inference(modus_ponens,[status(thm)],[310, 309])).
% 162.95/163.20 tff(312,plain,
% 162.95/163.20 (aElement0(W0!14)),
% 162.95/163.20 inference(unit_resolution,[status(thm)],[311, 308, 41])).
% 162.95/163.20 tff(313,plain,
% 162.95/163.20 (aElementOf0(W1!13, xJ)),
% 162.95/163.20 inference(and_elim,[status(thm)],[305])).
% 162.95/163.20 tff(314,plain,
% 162.95/163.20 (((~![W1: $i] : (aElement0(W1) | (~aElementOf0(W1, xJ)))) | (aElement0(W1!13) | (~aElementOf0(W1!13, xJ)))) <=> ((~![W1: $i] : (aElement0(W1) | (~aElementOf0(W1, xJ)))) | aElement0(W1!13) | (~aElementOf0(W1!13, xJ)))),
% 162.95/163.20 inference(rewrite,[status(thm)],[])).
% 162.95/163.20 tff(315,plain,
% 162.95/163.20 ((~![W1: $i] : (aElement0(W1) | (~aElementOf0(W1, xJ)))) | (aElement0(W1!13) | (~aElementOf0(W1!13, xJ)))),
% 162.95/163.20 inference(quant_inst,[status(thm)],[])).
% 162.95/163.20 tff(316,plain,
% 162.95/163.20 ((~![W1: $i] : (aElement0(W1) | (~aElementOf0(W1, xJ)))) | aElement0(W1!13) | (~aElementOf0(W1!13, xJ))),
% 162.95/163.20 inference(modus_ponens,[status(thm)],[315, 314])).
% 162.95/163.20 tff(317,plain,
% 162.95/163.20 (aElement0(W1!13)),
% 162.95/163.20 inference(unit_resolution,[status(thm)],[316, 313, 23])).
% 162.95/163.20 tff(318,plain,
% 162.95/163.20 (((~![W0: $i, W1: $i] : (aElement0(sdtpldt0(W0, W1)) | (~aElement0(W1)) | (~aElement0(W0)))) | ((~aElement0(W1!13)) | (~aElement0(W0!14)) | aElement0(sdtpldt0(W0!14, W1!13)))) <=> ((~![W0: $i, W1: $i] : (aElement0(sdtpldt0(W0, W1)) | (~aElement0(W1)) | (~aElement0(W0)))) | (~aElement0(W1!13)) | (~aElement0(W0!14)) | aElement0(sdtpldt0(W0!14, W1!13)))),
% 162.95/163.20 inference(rewrite,[status(thm)],[])).
% 162.95/163.20 tff(319,plain,
% 162.95/163.20 ((aElement0(sdtpldt0(W0!14, W1!13)) | (~aElement0(W1!13)) | (~aElement0(W0!14))) <=> ((~aElement0(W1!13)) | (~aElement0(W0!14)) | aElement0(sdtpldt0(W0!14, W1!13)))),
% 162.95/163.20 inference(rewrite,[status(thm)],[])).
% 162.95/163.20 tff(320,plain,
% 162.95/163.20 (((~![W0: $i, W1: $i] : (aElement0(sdtpldt0(W0, W1)) | (~aElement0(W1)) | (~aElement0(W0)))) | (aElement0(sdtpldt0(W0!14, W1!13)) | (~aElement0(W1!13)) | (~aElement0(W0!14)))) <=> ((~![W0: $i, W1: $i] : (aElement0(sdtpldt0(W0, W1)) | (~aElement0(W1)) | (~aElement0(W0)))) | ((~aElement0(W1!13)) | (~aElement0(W0!14)) | aElement0(sdtpldt0(W0!14, W1!13))))),
% 162.95/163.20 inference(monotonicity,[status(thm)],[319])).
% 162.95/163.20 tff(321,plain,
% 162.95/163.20 (((~![W0: $i, W1: $i] : (aElement0(sdtpldt0(W0, W1)) | (~aElement0(W1)) | (~aElement0(W0)))) | (aElement0(sdtpldt0(W0!14, W1!13)) | (~aElement0(W1!13)) | (~aElement0(W0!14)))) <=> ((~![W0: $i, W1: $i] : (aElement0(sdtpldt0(W0, W1)) | (~aElement0(W1)) | (~aElement0(W0)))) | (~aElement0(W1!13)) | (~aElement0(W0!14)) | aElement0(sdtpldt0(W0!14, W1!13)))),
% 162.95/163.20 inference(transitivity,[status(thm)],[320, 318])).
% 162.95/163.20 tff(322,plain,
% 162.95/163.20 ((~![W0: $i, W1: $i] : (aElement0(sdtpldt0(W0, W1)) | (~aElement0(W1)) | (~aElement0(W0)))) | (aElement0(sdtpldt0(W0!14, W1!13)) | (~aElement0(W1!13)) | (~aElement0(W0!14)))),
% 162.95/163.20 inference(quant_inst,[status(thm)],[])).
% 162.95/163.20 tff(323,plain,
% 162.95/163.20 ((~![W0: $i, W1: $i] : (aElement0(sdtpldt0(W0, W1)) | (~aElement0(W1)) | (~aElement0(W0)))) | (~aElement0(W1!13)) | (~aElement0(W0!14)) | aElement0(sdtpldt0(W0!14, W1!13))),
% 162.95/163.20 inference(modus_ponens,[status(thm)],[322, 321])).
% 162.95/163.20 tff(324,plain,
% 162.95/163.20 ((~aElement0(W1!13)) | (~aElement0(W0!14)) | aElement0(sdtpldt0(W0!14, W1!13))),
% 162.95/163.20 inference(unit_resolution,[status(thm)],[323, 92])).
% 162.95/163.20 tff(325,plain,
% 162.95/163.20 (aElement0(sdtpldt0(W0!14, W1!13))),
% 162.95/163.20 inference(unit_resolution,[status(thm)],[324, 317, 312])).
% 162.95/163.20 tff(326,plain,
% 162.95/163.20 (aElement0(xy)),
% 162.95/163.20 inference(modus_ponens,[status(thm)],[325, 307])).
% 162.95/163.20 tff(327,plain,
% 162.95/163.20 (((~![W0: $i, W1: $i] : ((sdtpldt0(W0, W1) = sdtpldt0(W1, W0)) | (~aElement0(W1)) | (~aElement0(W0)))) | ((~aElement0(xy)) | (~aElement0(xx)) | (sdtpldt0(xy, xx) = sdtpldt0(xx, xy)))) <=> ((~![W0: $i, W1: $i] : ((sdtpldt0(W0, W1) = sdtpldt0(W1, W0)) | (~aElement0(W1)) | (~aElement0(W0)))) | (~aElement0(xy)) | (~aElement0(xx)) | (sdtpldt0(xy, xx) = sdtpldt0(xx, xy)))),
% 162.95/163.20 inference(rewrite,[status(thm)],[])).
% 162.95/163.20 tff(328,plain,
% 162.95/163.20 (((sdtpldt0(xy, xx) = sdtpldt0(xx, xy)) | (~aElement0(xx)) | (~aElement0(xy))) <=> ((~aElement0(xy)) | (~aElement0(xx)) | (sdtpldt0(xy, xx) = sdtpldt0(xx, xy)))),
% 162.95/163.20 inference(rewrite,[status(thm)],[])).
% 162.95/163.20 tff(329,plain,
% 162.95/163.20 (((~![W0: $i, W1: $i] : ((sdtpldt0(W0, W1) = sdtpldt0(W1, W0)) | (~aElement0(W1)) | (~aElement0(W0)))) | ((sdtpldt0(xy, xx) = sdtpldt0(xx, xy)) | (~aElement0(xx)) | (~aElement0(xy)))) <=> ((~![W0: $i, W1: $i] : ((sdtpldt0(W0, W1) = sdtpldt0(W1, W0)) | (~aElement0(W1)) | (~aElement0(W0)))) | ((~aElement0(xy)) | (~aElement0(xx)) | (sdtpldt0(xy, xx) = sdtpldt0(xx, xy))))),
% 162.95/163.20 inference(monotonicity,[status(thm)],[328])).
% 162.95/163.20 tff(330,plain,
% 162.95/163.20 (((~![W0: $i, W1: $i] : ((sdtpldt0(W0, W1) = sdtpldt0(W1, W0)) | (~aElement0(W1)) | (~aElement0(W0)))) | ((sdtpldt0(xy, xx) = sdtpldt0(xx, xy)) | (~aElement0(xx)) | (~aElement0(xy)))) <=> ((~![W0: $i, W1: $i] : ((sdtpldt0(W0, W1) = sdtpldt0(W1, W0)) | (~aElement0(W1)) | (~aElement0(W0)))) | (~aElement0(xy)) | (~aElement0(xx)) | (sdtpldt0(xy, xx) = sdtpldt0(xx, xy)))),
% 162.95/163.20 inference(transitivity,[status(thm)],[329, 327])).
% 162.95/163.20 tff(331,plain,
% 162.95/163.20 ((~![W0: $i, W1: $i] : ((sdtpldt0(W0, W1) = sdtpldt0(W1, W0)) | (~aElement0(W1)) | (~aElement0(W0)))) | ((sdtpldt0(xy, xx) = sdtpldt0(xx, xy)) | (~aElement0(xx)) | (~aElement0(xy)))),
% 162.95/163.20 inference(quant_inst,[status(thm)],[])).
% 162.95/163.20 tff(332,plain,
% 162.95/163.20 ((~![W0: $i, W1: $i] : ((sdtpldt0(W0, W1) = sdtpldt0(W1, W0)) | (~aElement0(W1)) | (~aElement0(W0)))) | (~aElement0(xy)) | (~aElement0(xx)) | (sdtpldt0(xy, xx) = sdtpldt0(xx, xy))),
% 162.95/163.20 inference(modus_ponens,[status(thm)],[331, 330])).
% 162.95/163.22 tff(333,plain,
% 162.95/163.22 ((~aElement0(xy)) | (~aElement0(xx)) | (sdtpldt0(xy, xx) = sdtpldt0(xx, xy))),
% 162.95/163.22 inference(unit_resolution,[status(thm)],[332, 112])).
% 162.95/163.22 tff(334,plain,
% 162.95/163.22 (sdtpldt0(xy, xx) = sdtpldt0(xx, xy)),
% 162.95/163.22 inference(unit_resolution,[status(thm)],[333, 326, 275])).
% 162.95/163.22 tff(335,plain,
% 162.95/163.22 (sdtpldt0(xx, xy) = sdtpldt0(xy, xx)),
% 162.95/163.22 inference(symmetry,[status(thm)],[334])).
% 162.95/163.22 tff(336,plain,
% 162.95/163.22 (sdtpldt0(xx, xy) = sdtpldt0(sdtpldt0(xk, xm), sdtpldt0(xl, xn))),
% 162.95/163.22 inference(transitivity,[status(thm)],[335, 298, 282, 216, 120, 79])).
% 162.95/163.22 tff(337,plain,
% 162.95/163.22 ((~(sdtpldt0(xx, xy) = sdtpldt0(sdtpldt0(xk, xm), sdtpldt0(xl, xn)))) <=> (~(sdtpldt0(xx, xy) = sdtpldt0(sdtpldt0(xk, xm), sdtpldt0(xl, xn))))),
% 162.95/163.22 inference(rewrite,[status(thm)],[])).
% 162.95/163.22 tff(338,axiom,(~(sdtpldt0(xx, xy) = sdtpldt0(sdtpldt0(xk, xm), sdtpldt0(xl, xn)))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','m__')).
% 162.95/163.22 tff(339,plain,
% 162.95/163.22 (~(sdtpldt0(xx, xy) = sdtpldt0(sdtpldt0(xk, xm), sdtpldt0(xl, xn)))),
% 162.95/163.22 inference(modus_ponens,[status(thm)],[338, 337])).
% 162.95/163.22 tff(340,plain,
% 162.95/163.22 ($false),
% 162.95/163.22 inference(unit_resolution,[status(thm)],[339, 336])).
% 162.95/163.22 % SZS output end Proof
% 162.95/163.22 % E exiting
%------------------------------------------------------------------------------