%------------------------------------------------------------------------------
% File : Z3---4.15.1
% Problem : NUM542+2 : TPTP v9.0.0. Released v4.0.0.
% Transfm : none
% Format : tptp
% Command : run_E %s %d THM
% Computer : n002.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Sat Jun 21 05:21:20 AM UTC 2025
% Result : Theorem 0.53s 0.72s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.06/0.12 % Problem : NUM542+2 : TPTP v9.0.0. Released v4.0.0.
% 0.06/0.12 % Command : run_E %s %d THM
% 0.12/0.33 % Computer : n002.cluster.edu
% 0.12/0.33 % Model : x86_64 x86_64
% 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.33 % Memory : 8042.1875MB
% 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.33 % CPULimit : 300
% 0.12/0.33 % WCLimit : 300
% 0.12/0.33 % DateTime : Fri Jun 20 01:25:46 EDT 2025
% 0.12/0.33 % CPUTime :
% 0.53/0.72 % SZS status Theorem
% 0.53/0.72 % SZS output start Proof
% 0.53/0.72 tff(aElementOf0_type, type, (
% 0.53/0.72 aElementOf0: ( $i * $i ) > $o)).
% 0.53/0.72 tff(szNzAzT0_type, type, (
% 0.53/0.72 szNzAzT0: $i)).
% 0.53/0.72 tff(szszuzczcdt0_type, type, (
% 0.53/0.72 szszuzczcdt0: $i > $i)).
% 0.53/0.72 tff(tptp_fun_W0_9_type, type, (
% 0.53/0.72 tptp_fun_W0_9: $i)).
% 0.53/0.72 tff(sz00_type, type, (
% 0.53/0.72 sz00: $i)).
% 0.53/0.72 tff(sdtlseqdt0_type, type, (
% 0.53/0.72 sdtlseqdt0: ( $i * $i ) > $o)).
% 0.53/0.72 tff(xm_type, type, (
% 0.53/0.72 xm: $i)).
% 0.53/0.72 tff(slbdtrb0_type, type, (
% 0.53/0.72 slbdtrb0: $i > $i)).
% 0.53/0.72 tff(xn_type, type, (
% 0.53/0.72 xn: $i)).
% 0.53/0.72 tff(aSet0_type, type, (
% 0.53/0.72 aSet0: $i > $o)).
% 0.53/0.72 tff(aSubsetOf0_type, type, (
% 0.53/0.72 aSubsetOf0: ( $i * $i ) > $o)).
% 0.53/0.72 tff(tptp_fun_W1_4_type, type, (
% 0.53/0.72 tptp_fun_W1_4: $i > $i)).
% 0.53/0.72 tff(1,assumption,(~(sdtlseqdt0(xm, xn) | (~aSubsetOf0(slbdtrb0(xm), slbdtrb0(xn))) | (~aSet0(slbdtrb0(xn))) | (~aSet0(slbdtrb0(xm))) | (~![W0: $i] : (~(((~aElementOf0(W0, szNzAzT0)) | (~sdtlseqdt0(szszuzczcdt0(W0), xn))) <=> aElementOf0(W0, slbdtrb0(xn))))) | (~![W0: $i] : (~(((~aElementOf0(W0, szNzAzT0)) | (~sdtlseqdt0(szszuzczcdt0(W0), xm))) <=> aElementOf0(W0, slbdtrb0(xm))))) | (~![W0: $i] : ((~aElementOf0(W0, slbdtrb0(xm))) | aElementOf0(W0, slbdtrb0(xn)))))), introduced(assumption)).
% 0.53/0.72 tff(2,plain,
% 0.53/0.72 ((sdtlseqdt0(xm, xn) | (~aSubsetOf0(slbdtrb0(xm), slbdtrb0(xn))) | (~aSet0(slbdtrb0(xn))) | (~aSet0(slbdtrb0(xm))) | (~![W0: $i] : (~(((~aElementOf0(W0, szNzAzT0)) | (~sdtlseqdt0(szszuzczcdt0(W0), xn))) <=> aElementOf0(W0, slbdtrb0(xn))))) | (~![W0: $i] : (~(((~aElementOf0(W0, szNzAzT0)) | (~sdtlseqdt0(szszuzczcdt0(W0), xm))) <=> aElementOf0(W0, slbdtrb0(xm))))) | (~![W0: $i] : ((~aElementOf0(W0, slbdtrb0(xm))) | aElementOf0(W0, slbdtrb0(xn))))) | ![W0: $i] : (~(((~aElementOf0(W0, szNzAzT0)) | (~sdtlseqdt0(szszuzczcdt0(W0), xn))) <=> aElementOf0(W0, slbdtrb0(xn))))),
% 0.53/0.72 inference(tautology,[status(thm)],[])).
% 0.53/0.72 tff(3,plain,
% 0.53/0.72 (![W0: $i] : (~(((~aElementOf0(W0, szNzAzT0)) | (~sdtlseqdt0(szszuzczcdt0(W0), xn))) <=> aElementOf0(W0, slbdtrb0(xn))))),
% 0.53/0.72 inference(unit_resolution,[status(thm)],[2, 1])).
% 0.53/0.72 tff(4,plain,
% 0.53/0.72 ((~![W0: $i] : (~(((~aElementOf0(W0, szNzAzT0)) | (~sdtlseqdt0(szszuzczcdt0(W0), xn))) <=> aElementOf0(W0, slbdtrb0(xn))))) | (~(((~aElementOf0(tptp_fun_W1_4(szszuzczcdt0(xn)), szNzAzT0)) | (~sdtlseqdt0(szszuzczcdt0(tptp_fun_W1_4(szszuzczcdt0(xn))), xn))) <=> aElementOf0(tptp_fun_W1_4(szszuzczcdt0(xn)), slbdtrb0(xn))))),
% 0.53/0.72 inference(quant_inst,[status(thm)],[])).
% 0.53/0.72 tff(5,plain,
% 0.53/0.72 (~(((~aElementOf0(tptp_fun_W1_4(szszuzczcdt0(xn)), szNzAzT0)) | (~sdtlseqdt0(szszuzczcdt0(tptp_fun_W1_4(szszuzczcdt0(xn))), xn))) <=> aElementOf0(tptp_fun_W1_4(szszuzczcdt0(xn)), slbdtrb0(xn)))),
% 0.53/0.72 inference(unit_resolution,[status(thm)],[4, 3])).
% 0.53/0.72 tff(6,plain,
% 0.53/0.72 (aElementOf0(xn, szNzAzT0) <=> aElementOf0(xn, szNzAzT0)),
% 0.53/0.72 inference(rewrite,[status(thm)],[])).
% 0.53/0.72 tff(7,axiom,(aElementOf0(xm, szNzAzT0) & aElementOf0(xn, szNzAzT0)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','m__1964')).
% 0.53/0.72 tff(8,plain,
% 0.53/0.72 (aElementOf0(xn, szNzAzT0)),
% 0.53/0.72 inference(and_elim,[status(thm)],[7])).
% 0.53/0.72 tff(9,plain,
% 0.53/0.72 (aElementOf0(xn, szNzAzT0)),
% 0.53/0.72 inference(modus_ponens,[status(thm)],[8, 6])).
% 0.53/0.72 tff(10,plain,
% 0.53/0.72 (^[W0: $i] : refl(((~aElementOf0(W0, szNzAzT0)) | (~((~aElementOf0(szszuzczcdt0(W0), szNzAzT0)) | (szszuzczcdt0(W0) = sz00)))) <=> ((~aElementOf0(W0, szNzAzT0)) | (~((~aElementOf0(szszuzczcdt0(W0), szNzAzT0)) | (szszuzczcdt0(W0) = sz00)))))),
% 0.53/0.72 inference(bind,[status(th)],[])).
% 0.53/0.72 tff(11,plain,
% 0.53/0.72 (![W0: $i] : ((~aElementOf0(W0, szNzAzT0)) | (~((~aElementOf0(szszuzczcdt0(W0), szNzAzT0)) | (szszuzczcdt0(W0) = sz00)))) <=> ![W0: $i] : ((~aElementOf0(W0, szNzAzT0)) | (~((~aElementOf0(szszuzczcdt0(W0), szNzAzT0)) | (szszuzczcdt0(W0) = sz00))))),
% 0.53/0.72 inference(quant_intro,[status(thm)],[10])).
% 0.53/0.72 tff(12,plain,
% 0.53/0.72 (^[W0: $i] : rewrite(((~aElementOf0(W0, szNzAzT0)) | (aElementOf0(szszuzczcdt0(W0), szNzAzT0) & (~(szszuzczcdt0(W0) = sz00)))) <=> ((~aElementOf0(W0, szNzAzT0)) | (~((~aElementOf0(szszuzczcdt0(W0), szNzAzT0)) | (szszuzczcdt0(W0) = sz00)))))),
% 0.53/0.72 inference(bind,[status(th)],[])).
% 0.53/0.72 tff(13,plain,
% 0.53/0.72 (![W0: $i] : ((~aElementOf0(W0, szNzAzT0)) | (aElementOf0(szszuzczcdt0(W0), szNzAzT0) & (~(szszuzczcdt0(W0) = sz00)))) <=> ![W0: $i] : ((~aElementOf0(W0, szNzAzT0)) | (~((~aElementOf0(szszuzczcdt0(W0), szNzAzT0)) | (szszuzczcdt0(W0) = sz00))))),
% 0.53/0.72 inference(quant_intro,[status(thm)],[12])).
% 0.53/0.72 tff(14,plain,
% 0.53/0.72 (![W0: $i] : ((~aElementOf0(W0, szNzAzT0)) | (aElementOf0(szszuzczcdt0(W0), szNzAzT0) & (~(szszuzczcdt0(W0) = sz00)))) <=> ![W0: $i] : ((~aElementOf0(W0, szNzAzT0)) | (aElementOf0(szszuzczcdt0(W0), szNzAzT0) & (~(szszuzczcdt0(W0) = sz00))))),
% 0.53/0.72 inference(rewrite,[status(thm)],[])).
% 0.53/0.72 tff(15,plain,
% 0.53/0.72 (^[W0: $i] : rewrite((aElementOf0(W0, szNzAzT0) => (aElementOf0(szszuzczcdt0(W0), szNzAzT0) & (~(szszuzczcdt0(W0) = sz00)))) <=> ((~aElementOf0(W0, szNzAzT0)) | (aElementOf0(szszuzczcdt0(W0), szNzAzT0) & (~(szszuzczcdt0(W0) = sz00)))))),
% 0.53/0.72 inference(bind,[status(th)],[])).
% 0.53/0.72 tff(16,plain,
% 0.53/0.72 (![W0: $i] : (aElementOf0(W0, szNzAzT0) => (aElementOf0(szszuzczcdt0(W0), szNzAzT0) & (~(szszuzczcdt0(W0) = sz00)))) <=> ![W0: $i] : ((~aElementOf0(W0, szNzAzT0)) | (aElementOf0(szszuzczcdt0(W0), szNzAzT0) & (~(szszuzczcdt0(W0) = sz00))))),
% 0.53/0.72 inference(quant_intro,[status(thm)],[15])).
% 0.53/0.72 tff(17,axiom,(![W0: $i] : (aElementOf0(W0, szNzAzT0) => (aElementOf0(szszuzczcdt0(W0), szNzAzT0) & (~(szszuzczcdt0(W0) = sz00))))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','mSuccNum')).
% 0.53/0.72 tff(18,plain,
% 0.53/0.72 (![W0: $i] : ((~aElementOf0(W0, szNzAzT0)) | (aElementOf0(szszuzczcdt0(W0), szNzAzT0) & (~(szszuzczcdt0(W0) = sz00))))),
% 0.53/0.72 inference(modus_ponens,[status(thm)],[17, 16])).
% 0.53/0.72 tff(19,plain,
% 0.53/0.72 (![W0: $i] : ((~aElementOf0(W0, szNzAzT0)) | (aElementOf0(szszuzczcdt0(W0), szNzAzT0) & (~(szszuzczcdt0(W0) = sz00))))),
% 0.53/0.72 inference(modus_ponens,[status(thm)],[18, 14])).
% 0.53/0.72 tff(20,plain,(
% 0.53/0.72 ![W0: $i] : ((~aElementOf0(W0, szNzAzT0)) | (aElementOf0(szszuzczcdt0(W0), szNzAzT0) & (~(szszuzczcdt0(W0) = sz00))))),
% 0.53/0.72 inference(skolemize,[status(sab)],[19])).
% 0.53/0.72 tff(21,plain,
% 0.53/0.72 (![W0: $i] : ((~aElementOf0(W0, szNzAzT0)) | (~((~aElementOf0(szszuzczcdt0(W0), szNzAzT0)) | (szszuzczcdt0(W0) = sz00))))),
% 0.53/0.72 inference(modus_ponens,[status(thm)],[20, 13])).
% 0.53/0.72 tff(22,plain,
% 0.53/0.72 (![W0: $i] : ((~aElementOf0(W0, szNzAzT0)) | (~((~aElementOf0(szszuzczcdt0(W0), szNzAzT0)) | (szszuzczcdt0(W0) = sz00))))),
% 0.53/0.72 inference(modus_ponens,[status(thm)],[21, 11])).
% 0.53/0.72 tff(23,plain,
% 0.53/0.72 (((~![W0: $i] : ((~aElementOf0(W0, szNzAzT0)) | (~((~aElementOf0(szszuzczcdt0(W0), szNzAzT0)) | (szszuzczcdt0(W0) = sz00))))) | ((~aElementOf0(xn, szNzAzT0)) | (~((~aElementOf0(szszuzczcdt0(xn), szNzAzT0)) | (szszuzczcdt0(xn) = sz00))))) <=> ((~![W0: $i] : ((~aElementOf0(W0, szNzAzT0)) | (~((~aElementOf0(szszuzczcdt0(W0), szNzAzT0)) | (szszuzczcdt0(W0) = sz00))))) | (~aElementOf0(xn, szNzAzT0)) | (~((~aElementOf0(szszuzczcdt0(xn), szNzAzT0)) | (szszuzczcdt0(xn) = sz00))))),
% 0.53/0.72 inference(rewrite,[status(thm)],[])).
% 0.53/0.72 tff(24,plain,
% 0.53/0.72 ((~![W0: $i] : ((~aElementOf0(W0, szNzAzT0)) | (~((~aElementOf0(szszuzczcdt0(W0), szNzAzT0)) | (szszuzczcdt0(W0) = sz00))))) | ((~aElementOf0(xn, szNzAzT0)) | (~((~aElementOf0(szszuzczcdt0(xn), szNzAzT0)) | (szszuzczcdt0(xn) = sz00))))),
% 0.53/0.72 inference(quant_inst,[status(thm)],[])).
% 0.53/0.72 tff(25,plain,
% 0.53/0.72 ((~![W0: $i] : ((~aElementOf0(W0, szNzAzT0)) | (~((~aElementOf0(szszuzczcdt0(W0), szNzAzT0)) | (szszuzczcdt0(W0) = sz00))))) | (~aElementOf0(xn, szNzAzT0)) | (~((~aElementOf0(szszuzczcdt0(xn), szNzAzT0)) | (szszuzczcdt0(xn) = sz00)))),
% 0.53/0.72 inference(modus_ponens,[status(thm)],[24, 23])).
% 0.53/0.72 tff(26,plain,
% 0.53/0.72 (~((~aElementOf0(szszuzczcdt0(xn), szNzAzT0)) | (szszuzczcdt0(xn) = sz00))),
% 0.53/0.72 inference(unit_resolution,[status(thm)],[25, 22, 9])).
% 0.53/0.72 tff(27,plain,
% 0.53/0.72 (((~aElementOf0(szszuzczcdt0(xn), szNzAzT0)) | (szszuzczcdt0(xn) = sz00)) | (~(szszuzczcdt0(xn) = sz00))),
% 0.53/0.72 inference(tautology,[status(thm)],[])).
% 0.53/0.72 tff(28,plain,
% 0.53/0.72 (~(szszuzczcdt0(xn) = sz00)),
% 0.53/0.72 inference(unit_resolution,[status(thm)],[27, 26])).
% 0.53/0.72 tff(29,plain,
% 0.53/0.72 (((~aElementOf0(szszuzczcdt0(xn), szNzAzT0)) | (szszuzczcdt0(xn) = sz00)) | aElementOf0(szszuzczcdt0(xn), szNzAzT0)),
% 0.53/0.72 inference(tautology,[status(thm)],[])).
% 0.53/0.72 tff(30,plain,
% 0.53/0.72 (aElementOf0(szszuzczcdt0(xn), szNzAzT0)),
% 0.53/0.72 inference(unit_resolution,[status(thm)],[29, 26])).
% 0.53/0.72 tff(31,plain,
% 0.53/0.72 (^[W0: $i] : refl(((W0 = sz00) | (~aElementOf0(W0, szNzAzT0)) | (~((~aElementOf0(tptp_fun_W1_4(W0), szNzAzT0)) | (~(W0 = szszuzczcdt0(tptp_fun_W1_4(W0))))))) <=> ((W0 = sz00) | (~aElementOf0(W0, szNzAzT0)) | (~((~aElementOf0(tptp_fun_W1_4(W0), szNzAzT0)) | (~(W0 = szszuzczcdt0(tptp_fun_W1_4(W0))))))))),
% 0.53/0.72 inference(bind,[status(th)],[])).
% 0.53/0.72 tff(32,plain,
% 0.53/0.72 (![W0: $i] : ((W0 = sz00) | (~aElementOf0(W0, szNzAzT0)) | (~((~aElementOf0(tptp_fun_W1_4(W0), szNzAzT0)) | (~(W0 = szszuzczcdt0(tptp_fun_W1_4(W0))))))) <=> ![W0: $i] : ((W0 = sz00) | (~aElementOf0(W0, szNzAzT0)) | (~((~aElementOf0(tptp_fun_W1_4(W0), szNzAzT0)) | (~(W0 = szszuzczcdt0(tptp_fun_W1_4(W0)))))))),
% 0.53/0.72 inference(quant_intro,[status(thm)],[31])).
% 0.53/0.72 tff(33,plain,
% 0.53/0.72 (^[W0: $i] : trans(monotonicity(rewrite((aElementOf0(tptp_fun_W1_4(W0), szNzAzT0) & (W0 = szszuzczcdt0(tptp_fun_W1_4(W0)))) <=> (~((~aElementOf0(tptp_fun_W1_4(W0), szNzAzT0)) | (~(W0 = szszuzczcdt0(tptp_fun_W1_4(W0))))))), (((W0 = sz00) | (~aElementOf0(W0, szNzAzT0)) | (aElementOf0(tptp_fun_W1_4(W0), szNzAzT0) & (W0 = szszuzczcdt0(tptp_fun_W1_4(W0))))) <=> ((W0 = sz00) | (~aElementOf0(W0, szNzAzT0)) | (~((~aElementOf0(tptp_fun_W1_4(W0), szNzAzT0)) | (~(W0 = szszuzczcdt0(tptp_fun_W1_4(W0))))))))), rewrite(((W0 = sz00) | (~aElementOf0(W0, szNzAzT0)) | (~((~aElementOf0(tptp_fun_W1_4(W0), szNzAzT0)) | (~(W0 = szszuzczcdt0(tptp_fun_W1_4(W0))))))) <=> ((W0 = sz00) | (~aElementOf0(W0, szNzAzT0)) | (~((~aElementOf0(tptp_fun_W1_4(W0), szNzAzT0)) | (~(W0 = szszuzczcdt0(tptp_fun_W1_4(W0)))))))), (((W0 = sz00) | (~aElementOf0(W0, szNzAzT0)) | (aElementOf0(tptp_fun_W1_4(W0), szNzAzT0) & (W0 = szszuzczcdt0(tptp_fun_W1_4(W0))))) <=> ((W0 = sz00) | (~aElementOf0(W0, szNzAzT0)) | (~((~aElementOf0(tptp_fun_W1_4(W0), szNzAzT0)) | (~(W0 = szszuzczcdt0(tptp_fun_W1_4(W0)))))))))),
% 0.53/0.72 inference(bind,[status(th)],[])).
% 0.53/0.72 tff(34,plain,
% 0.53/0.72 (![W0: $i] : ((W0 = sz00) | (~aElementOf0(W0, szNzAzT0)) | (aElementOf0(tptp_fun_W1_4(W0), szNzAzT0) & (W0 = szszuzczcdt0(tptp_fun_W1_4(W0))))) <=> ![W0: $i] : ((W0 = sz00) | (~aElementOf0(W0, szNzAzT0)) | (~((~aElementOf0(tptp_fun_W1_4(W0), szNzAzT0)) | (~(W0 = szszuzczcdt0(tptp_fun_W1_4(W0)))))))),
% 0.53/0.72 inference(quant_intro,[status(thm)],[33])).
% 0.53/0.72 tff(35,plain,
% 0.53/0.72 (^[W0: $i] : rewrite(((aElementOf0(tptp_fun_W1_4(W0), szNzAzT0) & (W0 = szszuzczcdt0(tptp_fun_W1_4(W0)))) | (W0 = sz00) | (~aElementOf0(W0, szNzAzT0))) <=> ((W0 = sz00) | (~aElementOf0(W0, szNzAzT0)) | (aElementOf0(tptp_fun_W1_4(W0), szNzAzT0) & (W0 = szszuzczcdt0(tptp_fun_W1_4(W0))))))),
% 0.53/0.72 inference(bind,[status(th)],[])).
% 0.53/0.72 tff(36,plain,
% 0.53/0.72 (![W0: $i] : ((aElementOf0(tptp_fun_W1_4(W0), szNzAzT0) & (W0 = szszuzczcdt0(tptp_fun_W1_4(W0)))) | (W0 = sz00) | (~aElementOf0(W0, szNzAzT0))) <=> ![W0: $i] : ((W0 = sz00) | (~aElementOf0(W0, szNzAzT0)) | (aElementOf0(tptp_fun_W1_4(W0), szNzAzT0) & (W0 = szszuzczcdt0(tptp_fun_W1_4(W0)))))),
% 0.53/0.72 inference(quant_intro,[status(thm)],[35])).
% 0.53/0.72 tff(37,plain,
% 0.53/0.72 (![W0: $i] : (?[W1: $i] : (aElementOf0(W1, szNzAzT0) & (W0 = szszuzczcdt0(W1))) | (W0 = sz00) | (~aElementOf0(W0, szNzAzT0))) <=> ![W0: $i] : (?[W1: $i] : (aElementOf0(W1, szNzAzT0) & (W0 = szszuzczcdt0(W1))) | (W0 = sz00) | (~aElementOf0(W0, szNzAzT0)))),
% 0.53/0.72 inference(rewrite,[status(thm)],[])).
% 0.53/0.72 tff(38,plain,
% 0.53/0.72 (^[W0: $i] : trans(monotonicity(rewrite(((W0 = sz00) | ?[W1: $i] : (aElementOf0(W1, szNzAzT0) & (W0 = szszuzczcdt0(W1)))) <=> ((W0 = sz00) | ?[W1: $i] : (aElementOf0(W1, szNzAzT0) & (W0 = szszuzczcdt0(W1))))), ((aElementOf0(W0, szNzAzT0) => ((W0 = sz00) | ?[W1: $i] : (aElementOf0(W1, szNzAzT0) & (W0 = szszuzczcdt0(W1))))) <=> (aElementOf0(W0, szNzAzT0) => ((W0 = sz00) | ?[W1: $i] : (aElementOf0(W1, szNzAzT0) & (W0 = szszuzczcdt0(W1))))))), rewrite((aElementOf0(W0, szNzAzT0) => ((W0 = sz00) | ?[W1: $i] : (aElementOf0(W1, szNzAzT0) & (W0 = szszuzczcdt0(W1))))) <=> (?[W1: $i] : (aElementOf0(W1, szNzAzT0) & (W0 = szszuzczcdt0(W1))) | (W0 = sz00) | (~aElementOf0(W0, szNzAzT0)))), ((aElementOf0(W0, szNzAzT0) => ((W0 = sz00) | ?[W1: $i] : (aElementOf0(W1, szNzAzT0) & (W0 = szszuzczcdt0(W1))))) <=> (?[W1: $i] : (aElementOf0(W1, szNzAzT0) & (W0 = szszuzczcdt0(W1))) | (W0 = sz00) | (~aElementOf0(W0, szNzAzT0)))))),
% 0.53/0.72 inference(bind,[status(th)],[])).
% 0.53/0.72 tff(39,plain,
% 0.53/0.72 (![W0: $i] : (aElementOf0(W0, szNzAzT0) => ((W0 = sz00) | ?[W1: $i] : (aElementOf0(W1, szNzAzT0) & (W0 = szszuzczcdt0(W1))))) <=> ![W0: $i] : (?[W1: $i] : (aElementOf0(W1, szNzAzT0) & (W0 = szszuzczcdt0(W1))) | (W0 = sz00) | (~aElementOf0(W0, szNzAzT0)))),
% 0.53/0.72 inference(quant_intro,[status(thm)],[38])).
% 0.53/0.72 tff(40,axiom,(![W0: $i] : (aElementOf0(W0, szNzAzT0) => ((W0 = sz00) | ?[W1: $i] : (aElementOf0(W1, szNzAzT0) & (W0 = szszuzczcdt0(W1)))))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','mNatExtra')).
% 0.53/0.72 tff(41,plain,
% 0.53/0.72 (![W0: $i] : (?[W1: $i] : (aElementOf0(W1, szNzAzT0) & (W0 = szszuzczcdt0(W1))) | (W0 = sz00) | (~aElementOf0(W0, szNzAzT0)))),
% 0.53/0.72 inference(modus_ponens,[status(thm)],[40, 39])).
% 0.53/0.72 tff(42,plain,
% 0.53/0.72 (![W0: $i] : (?[W1: $i] : (aElementOf0(W1, szNzAzT0) & (W0 = szszuzczcdt0(W1))) | (W0 = sz00) | (~aElementOf0(W0, szNzAzT0)))),
% 0.53/0.72 inference(modus_ponens,[status(thm)],[41, 37])).
% 0.53/0.72 tff(43,plain,(
% 0.53/0.72 ![W0: $i] : ((aElementOf0(tptp_fun_W1_4(W0), szNzAzT0) & (W0 = szszuzczcdt0(tptp_fun_W1_4(W0)))) | (W0 = sz00) | (~aElementOf0(W0, szNzAzT0)))),
% 0.53/0.72 inference(skolemize,[status(sab)],[42])).
% 0.53/0.72 tff(44,plain,
% 0.53/0.72 (![W0: $i] : ((W0 = sz00) | (~aElementOf0(W0, szNzAzT0)) | (aElementOf0(tptp_fun_W1_4(W0), szNzAzT0) & (W0 = szszuzczcdt0(tptp_fun_W1_4(W0)))))),
% 0.53/0.72 inference(modus_ponens,[status(thm)],[43, 36])).
% 0.53/0.72 tff(45,plain,
% 0.53/0.72 (![W0: $i] : ((W0 = sz00) | (~aElementOf0(W0, szNzAzT0)) | (~((~aElementOf0(tptp_fun_W1_4(W0), szNzAzT0)) | (~(W0 = szszuzczcdt0(tptp_fun_W1_4(W0)))))))),
% 0.53/0.72 inference(modus_ponens,[status(thm)],[44, 34])).
% 0.53/0.72 tff(46,plain,
% 0.53/0.72 (![W0: $i] : ((W0 = sz00) | (~aElementOf0(W0, szNzAzT0)) | (~((~aElementOf0(tptp_fun_W1_4(W0), szNzAzT0)) | (~(W0 = szszuzczcdt0(tptp_fun_W1_4(W0)))))))),
% 0.53/0.72 inference(modus_ponens,[status(thm)],[45, 32])).
% 0.53/0.72 tff(47,plain,
% 0.53/0.72 (((~![W0: $i] : ((W0 = sz00) | (~aElementOf0(W0, szNzAzT0)) | (~((~aElementOf0(tptp_fun_W1_4(W0), szNzAzT0)) | (~(W0 = szszuzczcdt0(tptp_fun_W1_4(W0)))))))) | ((~aElementOf0(szszuzczcdt0(xn), szNzAzT0)) | (szszuzczcdt0(xn) = sz00) | (~((~aElementOf0(tptp_fun_W1_4(szszuzczcdt0(xn)), szNzAzT0)) | (~(szszuzczcdt0(xn) = szszuzczcdt0(tptp_fun_W1_4(szszuzczcdt0(xn))))))))) <=> ((~![W0: $i] : ((W0 = sz00) | (~aElementOf0(W0, szNzAzT0)) | (~((~aElementOf0(tptp_fun_W1_4(W0), szNzAzT0)) | (~(W0 = szszuzczcdt0(tptp_fun_W1_4(W0)))))))) | (~aElementOf0(szszuzczcdt0(xn), szNzAzT0)) | (szszuzczcdt0(xn) = sz00) | (~((~aElementOf0(tptp_fun_W1_4(szszuzczcdt0(xn)), szNzAzT0)) | (~(szszuzczcdt0(xn) = szszuzczcdt0(tptp_fun_W1_4(szszuzczcdt0(xn))))))))),
% 0.53/0.72 inference(rewrite,[status(thm)],[])).
% 0.53/0.72 tff(48,plain,
% 0.53/0.72 (((szszuzczcdt0(xn) = sz00) | (~aElementOf0(szszuzczcdt0(xn), szNzAzT0)) | (~((~aElementOf0(tptp_fun_W1_4(szszuzczcdt0(xn)), szNzAzT0)) | (~(szszuzczcdt0(xn) = szszuzczcdt0(tptp_fun_W1_4(szszuzczcdt0(xn)))))))) <=> ((~aElementOf0(szszuzczcdt0(xn), szNzAzT0)) | (szszuzczcdt0(xn) = sz00) | (~((~aElementOf0(tptp_fun_W1_4(szszuzczcdt0(xn)), szNzAzT0)) | (~(szszuzczcdt0(xn) = szszuzczcdt0(tptp_fun_W1_4(szszuzczcdt0(xn))))))))),
% 0.53/0.72 inference(rewrite,[status(thm)],[])).
% 0.53/0.72 tff(49,plain,
% 0.53/0.72 (((~![W0: $i] : ((W0 = sz00) | (~aElementOf0(W0, szNzAzT0)) | (~((~aElementOf0(tptp_fun_W1_4(W0), szNzAzT0)) | (~(W0 = szszuzczcdt0(tptp_fun_W1_4(W0)))))))) | ((szszuzczcdt0(xn) = sz00) | (~aElementOf0(szszuzczcdt0(xn), szNzAzT0)) | (~((~aElementOf0(tptp_fun_W1_4(szszuzczcdt0(xn)), szNzAzT0)) | (~(szszuzczcdt0(xn) = szszuzczcdt0(tptp_fun_W1_4(szszuzczcdt0(xn))))))))) <=> ((~![W0: $i] : ((W0 = sz00) | (~aElementOf0(W0, szNzAzT0)) | (~((~aElementOf0(tptp_fun_W1_4(W0), szNzAzT0)) | (~(W0 = szszuzczcdt0(tptp_fun_W1_4(W0)))))))) | ((~aElementOf0(szszuzczcdt0(xn), szNzAzT0)) | (szszuzczcdt0(xn) = sz00) | (~((~aElementOf0(tptp_fun_W1_4(szszuzczcdt0(xn)), szNzAzT0)) | (~(szszuzczcdt0(xn) = szszuzczcdt0(tptp_fun_W1_4(szszuzczcdt0(xn)))))))))),
% 0.53/0.72 inference(monotonicity,[status(thm)],[48])).
% 0.53/0.72 tff(50,plain,
% 0.53/0.72 (((~![W0: $i] : ((W0 = sz00) | (~aElementOf0(W0, szNzAzT0)) | (~((~aElementOf0(tptp_fun_W1_4(W0), szNzAzT0)) | (~(W0 = szszuzczcdt0(tptp_fun_W1_4(W0)))))))) | ((szszuzczcdt0(xn) = sz00) | (~aElementOf0(szszuzczcdt0(xn), szNzAzT0)) | (~((~aElementOf0(tptp_fun_W1_4(szszuzczcdt0(xn)), szNzAzT0)) | (~(szszuzczcdt0(xn) = szszuzczcdt0(tptp_fun_W1_4(szszuzczcdt0(xn))))))))) <=> ((~![W0: $i] : ((W0 = sz00) | (~aElementOf0(W0, szNzAzT0)) | (~((~aElementOf0(tptp_fun_W1_4(W0), szNzAzT0)) | (~(W0 = szszuzczcdt0(tptp_fun_W1_4(W0)))))))) | (~aElementOf0(szszuzczcdt0(xn), szNzAzT0)) | (szszuzczcdt0(xn) = sz00) | (~((~aElementOf0(tptp_fun_W1_4(szszuzczcdt0(xn)), szNzAzT0)) | (~(szszuzczcdt0(xn) = szszuzczcdt0(tptp_fun_W1_4(szszuzczcdt0(xn))))))))),
% 0.53/0.72 inference(transitivity,[status(thm)],[49, 47])).
% 0.53/0.72 tff(51,plain,
% 0.53/0.72 ((~![W0: $i] : ((W0 = sz00) | (~aElementOf0(W0, szNzAzT0)) | (~((~aElementOf0(tptp_fun_W1_4(W0), szNzAzT0)) | (~(W0 = szszuzczcdt0(tptp_fun_W1_4(W0)))))))) | ((szszuzczcdt0(xn) = sz00) | (~aElementOf0(szszuzczcdt0(xn), szNzAzT0)) | (~((~aElementOf0(tptp_fun_W1_4(szszuzczcdt0(xn)), szNzAzT0)) | (~(szszuzczcdt0(xn) = szszuzczcdt0(tptp_fun_W1_4(szszuzczcdt0(xn))))))))),
% 0.53/0.72 inference(quant_inst,[status(thm)],[])).
% 0.53/0.72 tff(52,plain,
% 0.53/0.72 ((~![W0: $i] : ((W0 = sz00) | (~aElementOf0(W0, szNzAzT0)) | (~((~aElementOf0(tptp_fun_W1_4(W0), szNzAzT0)) | (~(W0 = szszuzczcdt0(tptp_fun_W1_4(W0)))))))) | (~aElementOf0(szszuzczcdt0(xn), szNzAzT0)) | (szszuzczcdt0(xn) = sz00) | (~((~aElementOf0(tptp_fun_W1_4(szszuzczcdt0(xn)), szNzAzT0)) | (~(szszuzczcdt0(xn) = szszuzczcdt0(tptp_fun_W1_4(szszuzczcdt0(xn)))))))),
% 0.53/0.72 inference(modus_ponens,[status(thm)],[51, 50])).
% 0.53/0.72 tff(53,plain,
% 0.53/0.72 (~((~aElementOf0(tptp_fun_W1_4(szszuzczcdt0(xn)), szNzAzT0)) | (~(szszuzczcdt0(xn) = szszuzczcdt0(tptp_fun_W1_4(szszuzczcdt0(xn))))))),
% 0.53/0.72 inference(unit_resolution,[status(thm)],[52, 46, 30, 28])).
% 0.53/0.72 tff(54,plain,
% 0.53/0.72 (((~aElementOf0(tptp_fun_W1_4(szszuzczcdt0(xn)), szNzAzT0)) | (~(szszuzczcdt0(xn) = szszuzczcdt0(tptp_fun_W1_4(szszuzczcdt0(xn)))))) | (szszuzczcdt0(xn) = szszuzczcdt0(tptp_fun_W1_4(szszuzczcdt0(xn))))),
% 0.53/0.72 inference(tautology,[status(thm)],[])).
% 0.53/0.72 tff(55,plain,
% 0.53/0.72 (szszuzczcdt0(xn) = szszuzczcdt0(tptp_fun_W1_4(szszuzczcdt0(xn)))),
% 0.53/0.72 inference(unit_resolution,[status(thm)],[54, 53])).
% 0.53/0.72 tff(56,plain,
% 0.53/0.72 (szszuzczcdt0(tptp_fun_W1_4(szszuzczcdt0(xn))) = szszuzczcdt0(xn)),
% 0.53/0.72 inference(symmetry,[status(thm)],[55])).
% 0.53/0.72 tff(57,plain,
% 0.53/0.72 (sdtlseqdt0(szszuzczcdt0(tptp_fun_W1_4(szszuzczcdt0(xn))), xn) <=> sdtlseqdt0(szszuzczcdt0(xn), xn)),
% 0.53/0.72 inference(monotonicity,[status(thm)],[56])).
% 0.53/0.72 tff(58,plain,
% 0.53/0.72 (sdtlseqdt0(szszuzczcdt0(xn), xn) <=> sdtlseqdt0(szszuzczcdt0(tptp_fun_W1_4(szszuzczcdt0(xn))), xn)),
% 0.53/0.72 inference(symmetry,[status(thm)],[57])).
% 0.53/0.72 tff(59,plain,
% 0.53/0.72 ((~sdtlseqdt0(szszuzczcdt0(xn), xn)) <=> (~sdtlseqdt0(szszuzczcdt0(tptp_fun_W1_4(szszuzczcdt0(xn))), xn))),
% 0.53/0.72 inference(monotonicity,[status(thm)],[58])).
% 0.53/0.72 tff(60,plain,
% 0.53/0.72 (^[W0: $i] : refl(((~aElementOf0(W0, szNzAzT0)) | (~(W0 = szszuzczcdt0(W0)))) <=> ((~aElementOf0(W0, szNzAzT0)) | (~(W0 = szszuzczcdt0(W0)))))),
% 0.53/0.72 inference(bind,[status(th)],[])).
% 0.53/0.72 tff(61,plain,
% 0.53/0.72 (![W0: $i] : ((~aElementOf0(W0, szNzAzT0)) | (~(W0 = szszuzczcdt0(W0)))) <=> ![W0: $i] : ((~aElementOf0(W0, szNzAzT0)) | (~(W0 = szszuzczcdt0(W0))))),
% 0.53/0.72 inference(quant_intro,[status(thm)],[60])).
% 0.53/0.72 tff(62,plain,
% 0.53/0.72 (![W0: $i] : ((~aElementOf0(W0, szNzAzT0)) | (~(W0 = szszuzczcdt0(W0)))) <=> ![W0: $i] : ((~aElementOf0(W0, szNzAzT0)) | (~(W0 = szszuzczcdt0(W0))))),
% 0.53/0.72 inference(rewrite,[status(thm)],[])).
% 0.53/0.72 tff(63,plain,
% 0.53/0.72 (^[W0: $i] : rewrite((aElementOf0(W0, szNzAzT0) => (~(W0 = szszuzczcdt0(W0)))) <=> ((~aElementOf0(W0, szNzAzT0)) | (~(W0 = szszuzczcdt0(W0)))))),
% 0.53/0.72 inference(bind,[status(th)],[])).
% 0.53/0.72 tff(64,plain,
% 0.53/0.72 (![W0: $i] : (aElementOf0(W0, szNzAzT0) => (~(W0 = szszuzczcdt0(W0)))) <=> ![W0: $i] : ((~aElementOf0(W0, szNzAzT0)) | (~(W0 = szszuzczcdt0(W0))))),
% 0.53/0.72 inference(quant_intro,[status(thm)],[63])).
% 0.53/0.72 tff(65,axiom,(![W0: $i] : (aElementOf0(W0, szNzAzT0) => (~(W0 = szszuzczcdt0(W0))))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','mNatNSucc')).
% 0.53/0.72 tff(66,plain,
% 0.53/0.72 (![W0: $i] : ((~aElementOf0(W0, szNzAzT0)) | (~(W0 = szszuzczcdt0(W0))))),
% 0.53/0.72 inference(modus_ponens,[status(thm)],[65, 64])).
% 0.53/0.72 tff(67,plain,
% 0.53/0.72 (![W0: $i] : ((~aElementOf0(W0, szNzAzT0)) | (~(W0 = szszuzczcdt0(W0))))),
% 0.53/0.72 inference(modus_ponens,[status(thm)],[66, 62])).
% 0.53/0.72 tff(68,plain,(
% 0.53/0.72 ![W0: $i] : ((~aElementOf0(W0, szNzAzT0)) | (~(W0 = szszuzczcdt0(W0))))),
% 0.53/0.72 inference(skolemize,[status(sab)],[67])).
% 0.53/0.72 tff(69,plain,
% 0.53/0.72 (![W0: $i] : ((~aElementOf0(W0, szNzAzT0)) | (~(W0 = szszuzczcdt0(W0))))),
% 0.53/0.72 inference(modus_ponens,[status(thm)],[68, 61])).
% 0.53/0.72 tff(70,plain,
% 0.53/0.72 (((~![W0: $i] : ((~aElementOf0(W0, szNzAzT0)) | (~(W0 = szszuzczcdt0(W0))))) | ((~aElementOf0(xn, szNzAzT0)) | (~(xn = szszuzczcdt0(xn))))) <=> ((~![W0: $i] : ((~aElementOf0(W0, szNzAzT0)) | (~(W0 = szszuzczcdt0(W0))))) | (~aElementOf0(xn, szNzAzT0)) | (~(xn = szszuzczcdt0(xn))))),
% 0.53/0.72 inference(rewrite,[status(thm)],[])).
% 0.53/0.72 tff(71,plain,
% 0.53/0.72 ((~![W0: $i] : ((~aElementOf0(W0, szNzAzT0)) | (~(W0 = szszuzczcdt0(W0))))) | ((~aElementOf0(xn, szNzAzT0)) | (~(xn = szszuzczcdt0(xn))))),
% 0.53/0.72 inference(quant_inst,[status(thm)],[])).
% 0.53/0.72 tff(72,plain,
% 0.53/0.72 ((~![W0: $i] : ((~aElementOf0(W0, szNzAzT0)) | (~(W0 = szszuzczcdt0(W0))))) | (~aElementOf0(xn, szNzAzT0)) | (~(xn = szszuzczcdt0(xn)))),
% 0.53/0.72 inference(modus_ponens,[status(thm)],[71, 70])).
% 0.53/0.72 tff(73,plain,
% 0.53/0.72 (~(xn = szszuzczcdt0(xn))),
% 0.53/0.72 inference(unit_resolution,[status(thm)],[72, 69, 9])).
% 0.53/0.72 tff(74,plain,
% 0.53/0.72 (^[W0: $i] : refl(((~aElementOf0(W0, szNzAzT0)) | sdtlseqdt0(W0, szszuzczcdt0(W0))) <=> ((~aElementOf0(W0, szNzAzT0)) | sdtlseqdt0(W0, szszuzczcdt0(W0))))),
% 0.53/0.72 inference(bind,[status(th)],[])).
% 0.53/0.72 tff(75,plain,
% 0.53/0.72 (![W0: $i] : ((~aElementOf0(W0, szNzAzT0)) | sdtlseqdt0(W0, szszuzczcdt0(W0))) <=> ![W0: $i] : ((~aElementOf0(W0, szNzAzT0)) | sdtlseqdt0(W0, szszuzczcdt0(W0)))),
% 0.53/0.72 inference(quant_intro,[status(thm)],[74])).
% 0.53/0.72 tff(76,plain,
% 0.53/0.72 (![W0: $i] : ((~aElementOf0(W0, szNzAzT0)) | sdtlseqdt0(W0, szszuzczcdt0(W0))) <=> ![W0: $i] : ((~aElementOf0(W0, szNzAzT0)) | sdtlseqdt0(W0, szszuzczcdt0(W0)))),
% 0.53/0.72 inference(rewrite,[status(thm)],[])).
% 0.53/0.72 tff(77,plain,
% 0.53/0.72 (^[W0: $i] : rewrite((aElementOf0(W0, szNzAzT0) => sdtlseqdt0(W0, szszuzczcdt0(W0))) <=> ((~aElementOf0(W0, szNzAzT0)) | sdtlseqdt0(W0, szszuzczcdt0(W0))))),
% 0.53/0.72 inference(bind,[status(th)],[])).
% 0.53/0.72 tff(78,plain,
% 0.53/0.72 (![W0: $i] : (aElementOf0(W0, szNzAzT0) => sdtlseqdt0(W0, szszuzczcdt0(W0))) <=> ![W0: $i] : ((~aElementOf0(W0, szNzAzT0)) | sdtlseqdt0(W0, szszuzczcdt0(W0)))),
% 0.53/0.72 inference(quant_intro,[status(thm)],[77])).
% 0.53/0.72 tff(79,axiom,(![W0: $i] : (aElementOf0(W0, szNzAzT0) => sdtlseqdt0(W0, szszuzczcdt0(W0)))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','mLessSucc')).
% 0.53/0.72 tff(80,plain,
% 0.53/0.72 (![W0: $i] : ((~aElementOf0(W0, szNzAzT0)) | sdtlseqdt0(W0, szszuzczcdt0(W0)))),
% 0.53/0.72 inference(modus_ponens,[status(thm)],[79, 78])).
% 0.53/0.72 tff(81,plain,
% 0.53/0.72 (![W0: $i] : ((~aElementOf0(W0, szNzAzT0)) | sdtlseqdt0(W0, szszuzczcdt0(W0)))),
% 0.53/0.72 inference(modus_ponens,[status(thm)],[80, 76])).
% 0.53/0.72 tff(82,plain,(
% 0.53/0.72 ![W0: $i] : ((~aElementOf0(W0, szNzAzT0)) | sdtlseqdt0(W0, szszuzczcdt0(W0)))),
% 0.53/0.72 inference(skolemize,[status(sab)],[81])).
% 0.53/0.72 tff(83,plain,
% 0.53/0.72 (![W0: $i] : ((~aElementOf0(W0, szNzAzT0)) | sdtlseqdt0(W0, szszuzczcdt0(W0)))),
% 0.53/0.72 inference(modus_ponens,[status(thm)],[82, 75])).
% 0.53/0.72 tff(84,plain,
% 0.53/0.72 (((~![W0: $i] : ((~aElementOf0(W0, szNzAzT0)) | sdtlseqdt0(W0, szszuzczcdt0(W0)))) | ((~aElementOf0(xn, szNzAzT0)) | sdtlseqdt0(xn, szszuzczcdt0(xn)))) <=> ((~![W0: $i] : ((~aElementOf0(W0, szNzAzT0)) | sdtlseqdt0(W0, szszuzczcdt0(W0)))) | (~aElementOf0(xn, szNzAzT0)) | sdtlseqdt0(xn, szszuzczcdt0(xn)))),
% 0.53/0.72 inference(rewrite,[status(thm)],[])).
% 0.53/0.72 tff(85,plain,
% 0.53/0.72 ((~![W0: $i] : ((~aElementOf0(W0, szNzAzT0)) | sdtlseqdt0(W0, szszuzczcdt0(W0)))) | ((~aElementOf0(xn, szNzAzT0)) | sdtlseqdt0(xn, szszuzczcdt0(xn)))),
% 0.53/0.72 inference(quant_inst,[status(thm)],[])).
% 0.53/0.72 tff(86,plain,
% 0.53/0.72 ((~![W0: $i] : ((~aElementOf0(W0, szNzAzT0)) | sdtlseqdt0(W0, szszuzczcdt0(W0)))) | (~aElementOf0(xn, szNzAzT0)) | sdtlseqdt0(xn, szszuzczcdt0(xn))),
% 0.53/0.72 inference(modus_ponens,[status(thm)],[85, 84])).
% 0.53/0.72 tff(87,plain,
% 0.53/0.72 (sdtlseqdt0(xn, szszuzczcdt0(xn))),
% 0.53/0.72 inference(unit_resolution,[status(thm)],[86, 83, 9])).
% 0.53/0.72 tff(88,plain,
% 0.53/0.72 (^[W0: $i, W1: $i] : refl(((W0 = W1) | (~aElementOf0(W1, szNzAzT0)) | (~aElementOf0(W0, szNzAzT0)) | (~sdtlseqdt0(W0, W1)) | (~sdtlseqdt0(W1, W0))) <=> ((W0 = W1) | (~aElementOf0(W1, szNzAzT0)) | (~aElementOf0(W0, szNzAzT0)) | (~sdtlseqdt0(W0, W1)) | (~sdtlseqdt0(W1, W0))))),
% 0.53/0.72 inference(bind,[status(th)],[])).
% 0.53/0.72 tff(89,plain,
% 0.53/0.72 (![W0: $i, W1: $i] : ((W0 = W1) | (~aElementOf0(W1, szNzAzT0)) | (~aElementOf0(W0, szNzAzT0)) | (~sdtlseqdt0(W0, W1)) | (~sdtlseqdt0(W1, W0))) <=> ![W0: $i, W1: $i] : ((W0 = W1) | (~aElementOf0(W1, szNzAzT0)) | (~aElementOf0(W0, szNzAzT0)) | (~sdtlseqdt0(W0, W1)) | (~sdtlseqdt0(W1, W0)))),
% 0.53/0.72 inference(quant_intro,[status(thm)],[88])).
% 0.53/0.72 tff(90,plain,
% 0.53/0.72 (^[W0: $i, W1: $i] : trans(monotonicity(trans(monotonicity(rewrite((aElementOf0(W0, szNzAzT0) & aElementOf0(W1, szNzAzT0)) <=> (~((~aElementOf0(W1, szNzAzT0)) | (~aElementOf0(W0, szNzAzT0))))), ((~(aElementOf0(W0, szNzAzT0) & aElementOf0(W1, szNzAzT0))) <=> (~(~((~aElementOf0(W1, szNzAzT0)) | (~aElementOf0(W0, szNzAzT0))))))), rewrite((~(~((~aElementOf0(W1, szNzAzT0)) | (~aElementOf0(W0, szNzAzT0))))) <=> ((~aElementOf0(W1, szNzAzT0)) | (~aElementOf0(W0, szNzAzT0)))), ((~(aElementOf0(W0, szNzAzT0) & aElementOf0(W1, szNzAzT0))) <=> ((~aElementOf0(W1, szNzAzT0)) | (~aElementOf0(W0, szNzAzT0))))), trans(monotonicity(rewrite((sdtlseqdt0(W0, W1) & sdtlseqdt0(W1, W0)) <=> (~((~sdtlseqdt0(W0, W1)) | (~sdtlseqdt0(W1, W0))))), ((~(sdtlseqdt0(W0, W1) & sdtlseqdt0(W1, W0))) <=> (~(~((~sdtlseqdt0(W0, W1)) | (~sdtlseqdt0(W1, W0))))))), rewrite((~(~((~sdtlseqdt0(W0, W1)) | (~sdtlseqdt0(W1, W0))))) <=> ((~sdtlseqdt0(W0, W1)) | (~sdtlseqdt0(W1, W0)))), ((~(sdtlseqdt0(W0, W1) & sdtlseqdt0(W1, W0))) <=> ((~sdtlseqdt0(W0, W1)) | (~sdtlseqdt0(W1, W0))))), (((W0 = W1) | (~(aElementOf0(W0, szNzAzT0) & aElementOf0(W1, szNzAzT0))) | (~(sdtlseqdt0(W0, W1) & sdtlseqdt0(W1, W0)))) <=> ((W0 = W1) | ((~aElementOf0(W1, szNzAzT0)) | (~aElementOf0(W0, szNzAzT0))) | ((~sdtlseqdt0(W0, W1)) | (~sdtlseqdt0(W1, W0)))))), rewrite(((W0 = W1) | ((~aElementOf0(W1, szNzAzT0)) | (~aElementOf0(W0, szNzAzT0))) | ((~sdtlseqdt0(W0, W1)) | (~sdtlseqdt0(W1, W0)))) <=> ((W0 = W1) | (~aElementOf0(W1, szNzAzT0)) | (~aElementOf0(W0, szNzAzT0)) | (~sdtlseqdt0(W0, W1)) | (~sdtlseqdt0(W1, W0)))), (((W0 = W1) | (~(aElementOf0(W0, szNzAzT0) & aElementOf0(W1, szNzAzT0))) | (~(sdtlseqdt0(W0, W1) & sdtlseqdt0(W1, W0)))) <=> ((W0 = W1) | (~aElementOf0(W1, szNzAzT0)) | (~aElementOf0(W0, szNzAzT0)) | (~sdtlseqdt0(W0, W1)) | (~sdtlseqdt0(W1, W0)))))),
% 0.53/0.72 inference(bind,[status(th)],[])).
% 0.53/0.72 tff(91,plain,
% 0.53/0.72 (![W0: $i, W1: $i] : ((W0 = W1) | (~(aElementOf0(W0, szNzAzT0) & aElementOf0(W1, szNzAzT0))) | (~(sdtlseqdt0(W0, W1) & sdtlseqdt0(W1, W0)))) <=> ![W0: $i, W1: $i] : ((W0 = W1) | (~aElementOf0(W1, szNzAzT0)) | (~aElementOf0(W0, szNzAzT0)) | (~sdtlseqdt0(W0, W1)) | (~sdtlseqdt0(W1, W0)))),
% 0.53/0.72 inference(quant_intro,[status(thm)],[90])).
% 0.53/0.72 tff(92,plain,
% 0.53/0.72 (![W0: $i, W1: $i] : ((W0 = W1) | (~(aElementOf0(W0, szNzAzT0) & aElementOf0(W1, szNzAzT0))) | (~(sdtlseqdt0(W0, W1) & sdtlseqdt0(W1, W0)))) <=> ![W0: $i, W1: $i] : ((W0 = W1) | (~(aElementOf0(W0, szNzAzT0) & aElementOf0(W1, szNzAzT0))) | (~(sdtlseqdt0(W0, W1) & sdtlseqdt0(W1, W0))))),
% 0.53/0.72 inference(rewrite,[status(thm)],[])).
% 0.53/0.72 tff(93,plain,
% 0.53/0.72 (^[W0: $i, W1: $i] : trans(monotonicity(rewrite(((sdtlseqdt0(W0, W1) & sdtlseqdt0(W1, W0)) => (W0 = W1)) <=> ((~(sdtlseqdt0(W0, W1) & sdtlseqdt0(W1, W0))) | (W0 = W1))), (((aElementOf0(W0, szNzAzT0) & aElementOf0(W1, szNzAzT0)) => ((sdtlseqdt0(W0, W1) & sdtlseqdt0(W1, W0)) => (W0 = W1))) <=> ((aElementOf0(W0, szNzAzT0) & aElementOf0(W1, szNzAzT0)) => ((~(sdtlseqdt0(W0, W1) & sdtlseqdt0(W1, W0))) | (W0 = W1))))), rewrite(((aElementOf0(W0, szNzAzT0) & aElementOf0(W1, szNzAzT0)) => ((~(sdtlseqdt0(W0, W1) & sdtlseqdt0(W1, W0))) | (W0 = W1))) <=> ((W0 = W1) | (~(aElementOf0(W0, szNzAzT0) & aElementOf0(W1, szNzAzT0))) | (~(sdtlseqdt0(W0, W1) & sdtlseqdt0(W1, W0))))), (((aElementOf0(W0, szNzAzT0) & aElementOf0(W1, szNzAzT0)) => ((sdtlseqdt0(W0, W1) & sdtlseqdt0(W1, W0)) => (W0 = W1))) <=> ((W0 = W1) | (~(aElementOf0(W0, szNzAzT0) & aElementOf0(W1, szNzAzT0))) | (~(sdtlseqdt0(W0, W1) & sdtlseqdt0(W1, W0))))))),
% 0.53/0.73 inference(bind,[status(th)],[])).
% 0.53/0.73 tff(94,plain,
% 0.53/0.73 (![W0: $i, W1: $i] : ((aElementOf0(W0, szNzAzT0) & aElementOf0(W1, szNzAzT0)) => ((sdtlseqdt0(W0, W1) & sdtlseqdt0(W1, W0)) => (W0 = W1))) <=> ![W0: $i, W1: $i] : ((W0 = W1) | (~(aElementOf0(W0, szNzAzT0) & aElementOf0(W1, szNzAzT0))) | (~(sdtlseqdt0(W0, W1) & sdtlseqdt0(W1, W0))))),
% 0.53/0.73 inference(quant_intro,[status(thm)],[93])).
% 0.53/0.73 tff(95,axiom,(![W0: $i, W1: $i] : ((aElementOf0(W0, szNzAzT0) & aElementOf0(W1, szNzAzT0)) => ((sdtlseqdt0(W0, W1) & sdtlseqdt0(W1, W0)) => (W0 = W1)))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','mLessASymm')).
% 0.53/0.73 tff(96,plain,
% 0.53/0.73 (![W0: $i, W1: $i] : ((W0 = W1) | (~(aElementOf0(W0, szNzAzT0) & aElementOf0(W1, szNzAzT0))) | (~(sdtlseqdt0(W0, W1) & sdtlseqdt0(W1, W0))))),
% 0.53/0.73 inference(modus_ponens,[status(thm)],[95, 94])).
% 0.53/0.73 tff(97,plain,
% 0.53/0.73 (![W0: $i, W1: $i] : ((W0 = W1) | (~(aElementOf0(W0, szNzAzT0) & aElementOf0(W1, szNzAzT0))) | (~(sdtlseqdt0(W0, W1) & sdtlseqdt0(W1, W0))))),
% 0.53/0.73 inference(modus_ponens,[status(thm)],[96, 92])).
% 0.53/0.73 tff(98,plain,(
% 0.53/0.73 ![W0: $i, W1: $i] : ((W0 = W1) | (~(aElementOf0(W0, szNzAzT0) & aElementOf0(W1, szNzAzT0))) | (~(sdtlseqdt0(W0, W1) & sdtlseqdt0(W1, W0))))),
% 0.53/0.73 inference(skolemize,[status(sab)],[97])).
% 0.53/0.73 tff(99,plain,
% 0.53/0.73 (![W0: $i, W1: $i] : ((W0 = W1) | (~aElementOf0(W1, szNzAzT0)) | (~aElementOf0(W0, szNzAzT0)) | (~sdtlseqdt0(W0, W1)) | (~sdtlseqdt0(W1, W0)))),
% 0.53/0.73 inference(modus_ponens,[status(thm)],[98, 91])).
% 0.53/0.73 tff(100,plain,
% 0.53/0.73 (![W0: $i, W1: $i] : ((W0 = W1) | (~aElementOf0(W1, szNzAzT0)) | (~aElementOf0(W0, szNzAzT0)) | (~sdtlseqdt0(W0, W1)) | (~sdtlseqdt0(W1, W0)))),
% 0.53/0.73 inference(modus_ponens,[status(thm)],[99, 89])).
% 0.53/0.73 tff(101,plain,
% 0.53/0.73 (((~![W0: $i, W1: $i] : ((W0 = W1) | (~aElementOf0(W1, szNzAzT0)) | (~aElementOf0(W0, szNzAzT0)) | (~sdtlseqdt0(W0, W1)) | (~sdtlseqdt0(W1, W0)))) | ((~aElementOf0(xn, szNzAzT0)) | (xn = szszuzczcdt0(xn)) | (~aElementOf0(szszuzczcdt0(xn), szNzAzT0)) | (~sdtlseqdt0(szszuzczcdt0(xn), xn)) | (~sdtlseqdt0(xn, szszuzczcdt0(xn))))) <=> ((~![W0: $i, W1: $i] : ((W0 = W1) | (~aElementOf0(W1, szNzAzT0)) | (~aElementOf0(W0, szNzAzT0)) | (~sdtlseqdt0(W0, W1)) | (~sdtlseqdt0(W1, W0)))) | (~aElementOf0(xn, szNzAzT0)) | (xn = szszuzczcdt0(xn)) | (~aElementOf0(szszuzczcdt0(xn), szNzAzT0)) | (~sdtlseqdt0(szszuzczcdt0(xn), xn)) | (~sdtlseqdt0(xn, szszuzczcdt0(xn))))),
% 0.53/0.73 inference(rewrite,[status(thm)],[])).
% 0.53/0.73 tff(102,plain,
% 0.53/0.73 (((xn = szszuzczcdt0(xn)) | (~aElementOf0(szszuzczcdt0(xn), szNzAzT0)) | (~aElementOf0(xn, szNzAzT0)) | (~sdtlseqdt0(xn, szszuzczcdt0(xn))) | (~sdtlseqdt0(szszuzczcdt0(xn), xn))) <=> ((~aElementOf0(xn, szNzAzT0)) | (xn = szszuzczcdt0(xn)) | (~aElementOf0(szszuzczcdt0(xn), szNzAzT0)) | (~sdtlseqdt0(szszuzczcdt0(xn), xn)) | (~sdtlseqdt0(xn, szszuzczcdt0(xn))))),
% 0.53/0.73 inference(rewrite,[status(thm)],[])).
% 0.53/0.73 tff(103,plain,
% 0.53/0.73 (((~![W0: $i, W1: $i] : ((W0 = W1) | (~aElementOf0(W1, szNzAzT0)) | (~aElementOf0(W0, szNzAzT0)) | (~sdtlseqdt0(W0, W1)) | (~sdtlseqdt0(W1, W0)))) | ((xn = szszuzczcdt0(xn)) | (~aElementOf0(szszuzczcdt0(xn), szNzAzT0)) | (~aElementOf0(xn, szNzAzT0)) | (~sdtlseqdt0(xn, szszuzczcdt0(xn))) | (~sdtlseqdt0(szszuzczcdt0(xn), xn)))) <=> ((~![W0: $i, W1: $i] : ((W0 = W1) | (~aElementOf0(W1, szNzAzT0)) | (~aElementOf0(W0, szNzAzT0)) | (~sdtlseqdt0(W0, W1)) | (~sdtlseqdt0(W1, W0)))) | ((~aElementOf0(xn, szNzAzT0)) | (xn = szszuzczcdt0(xn)) | (~aElementOf0(szszuzczcdt0(xn), szNzAzT0)) | (~sdtlseqdt0(szszuzczcdt0(xn), xn)) | (~sdtlseqdt0(xn, szszuzczcdt0(xn)))))),
% 0.53/0.73 inference(monotonicity,[status(thm)],[102])).
% 0.53/0.73 tff(104,plain,
% 0.53/0.73 (((~![W0: $i, W1: $i] : ((W0 = W1) | (~aElementOf0(W1, szNzAzT0)) | (~aElementOf0(W0, szNzAzT0)) | (~sdtlseqdt0(W0, W1)) | (~sdtlseqdt0(W1, W0)))) | ((xn = szszuzczcdt0(xn)) | (~aElementOf0(szszuzczcdt0(xn), szNzAzT0)) | (~aElementOf0(xn, szNzAzT0)) | (~sdtlseqdt0(xn, szszuzczcdt0(xn))) | (~sdtlseqdt0(szszuzczcdt0(xn), xn)))) <=> ((~![W0: $i, W1: $i] : ((W0 = W1) | (~aElementOf0(W1, szNzAzT0)) | (~aElementOf0(W0, szNzAzT0)) | (~sdtlseqdt0(W0, W1)) | (~sdtlseqdt0(W1, W0)))) | (~aElementOf0(xn, szNzAzT0)) | (xn = szszuzczcdt0(xn)) | (~aElementOf0(szszuzczcdt0(xn), szNzAzT0)) | (~sdtlseqdt0(szszuzczcdt0(xn), xn)) | (~sdtlseqdt0(xn, szszuzczcdt0(xn))))),
% 0.53/0.73 inference(transitivity,[status(thm)],[103, 101])).
% 0.53/0.73 tff(105,plain,
% 0.53/0.73 ((~![W0: $i, W1: $i] : ((W0 = W1) | (~aElementOf0(W1, szNzAzT0)) | (~aElementOf0(W0, szNzAzT0)) | (~sdtlseqdt0(W0, W1)) | (~sdtlseqdt0(W1, W0)))) | ((xn = szszuzczcdt0(xn)) | (~aElementOf0(szszuzczcdt0(xn), szNzAzT0)) | (~aElementOf0(xn, szNzAzT0)) | (~sdtlseqdt0(xn, szszuzczcdt0(xn))) | (~sdtlseqdt0(szszuzczcdt0(xn), xn)))),
% 0.53/0.73 inference(quant_inst,[status(thm)],[])).
% 0.53/0.73 tff(106,plain,
% 0.53/0.73 ((~![W0: $i, W1: $i] : ((W0 = W1) | (~aElementOf0(W1, szNzAzT0)) | (~aElementOf0(W0, szNzAzT0)) | (~sdtlseqdt0(W0, W1)) | (~sdtlseqdt0(W1, W0)))) | (~aElementOf0(xn, szNzAzT0)) | (xn = szszuzczcdt0(xn)) | (~aElementOf0(szszuzczcdt0(xn), szNzAzT0)) | (~sdtlseqdt0(szszuzczcdt0(xn), xn)) | (~sdtlseqdt0(xn, szszuzczcdt0(xn)))),
% 0.53/0.73 inference(modus_ponens,[status(thm)],[105, 104])).
% 0.53/0.73 tff(107,plain,
% 0.53/0.73 ((~aElementOf0(szszuzczcdt0(xn), szNzAzT0)) | (~sdtlseqdt0(szszuzczcdt0(xn), xn))),
% 0.53/0.73 inference(unit_resolution,[status(thm)],[106, 100, 9, 87, 73])).
% 0.53/0.73 tff(108,plain,
% 0.53/0.73 (~sdtlseqdt0(szszuzczcdt0(xn), xn)),
% 0.53/0.73 inference(unit_resolution,[status(thm)],[107, 30])).
% 0.53/0.73 tff(109,plain,
% 0.53/0.73 (~sdtlseqdt0(szszuzczcdt0(tptp_fun_W1_4(szszuzczcdt0(xn))), xn)),
% 0.53/0.73 inference(modus_ponens,[status(thm)],[108, 59])).
% 0.53/0.73 tff(110,plain,
% 0.53/0.73 (((~aElementOf0(tptp_fun_W1_4(szszuzczcdt0(xn)), szNzAzT0)) | (~sdtlseqdt0(szszuzczcdt0(tptp_fun_W1_4(szszuzczcdt0(xn))), xn))) | sdtlseqdt0(szszuzczcdt0(tptp_fun_W1_4(szszuzczcdt0(xn))), xn)),
% 0.53/0.73 inference(tautology,[status(thm)],[])).
% 0.53/0.73 tff(111,plain,
% 0.53/0.73 ((~aElementOf0(tptp_fun_W1_4(szszuzczcdt0(xn)), szNzAzT0)) | (~sdtlseqdt0(szszuzczcdt0(tptp_fun_W1_4(szszuzczcdt0(xn))), xn))),
% 0.53/0.73 inference(unit_resolution,[status(thm)],[110, 109])).
% 0.53/0.73 tff(112,plain,
% 0.53/0.73 ((((~aElementOf0(tptp_fun_W1_4(szszuzczcdt0(xn)), szNzAzT0)) | (~sdtlseqdt0(szszuzczcdt0(tptp_fun_W1_4(szszuzczcdt0(xn))), xn))) <=> aElementOf0(tptp_fun_W1_4(szszuzczcdt0(xn)), slbdtrb0(xn))) | (~((~aElementOf0(tptp_fun_W1_4(szszuzczcdt0(xn)), szNzAzT0)) | (~sdtlseqdt0(szszuzczcdt0(tptp_fun_W1_4(szszuzczcdt0(xn))), xn)))) | (~aElementOf0(tptp_fun_W1_4(szszuzczcdt0(xn)), slbdtrb0(xn)))),
% 0.53/0.73 inference(tautology,[status(thm)],[])).
% 0.53/0.73 tff(113,plain,
% 0.53/0.73 ((((~aElementOf0(tptp_fun_W1_4(szszuzczcdt0(xn)), szNzAzT0)) | (~sdtlseqdt0(szszuzczcdt0(tptp_fun_W1_4(szszuzczcdt0(xn))), xn))) <=> aElementOf0(tptp_fun_W1_4(szszuzczcdt0(xn)), slbdtrb0(xn))) | (~aElementOf0(tptp_fun_W1_4(szszuzczcdt0(xn)), slbdtrb0(xn)))),
% 0.53/0.73 inference(unit_resolution,[status(thm)],[112, 111])).
% 0.53/0.73 tff(114,plain,
% 0.53/0.73 (~aElementOf0(tptp_fun_W1_4(szszuzczcdt0(xn)), slbdtrb0(xn))),
% 0.53/0.73 inference(unit_resolution,[status(thm)],[113, 5])).
% 0.53/0.73 tff(115,plain,
% 0.53/0.73 ((sdtlseqdt0(xm, xn) | (~aSubsetOf0(slbdtrb0(xm), slbdtrb0(xn))) | (~aSet0(slbdtrb0(xn))) | (~aSet0(slbdtrb0(xm))) | (~![W0: $i] : (~(((~aElementOf0(W0, szNzAzT0)) | (~sdtlseqdt0(szszuzczcdt0(W0), xn))) <=> aElementOf0(W0, slbdtrb0(xn))))) | (~![W0: $i] : (~(((~aElementOf0(W0, szNzAzT0)) | (~sdtlseqdt0(szszuzczcdt0(W0), xm))) <=> aElementOf0(W0, slbdtrb0(xm))))) | (~![W0: $i] : ((~aElementOf0(W0, slbdtrb0(xm))) | aElementOf0(W0, slbdtrb0(xn))))) | ![W0: $i] : (~(((~aElementOf0(W0, szNzAzT0)) | (~sdtlseqdt0(szszuzczcdt0(W0), xm))) <=> aElementOf0(W0, slbdtrb0(xm))))),
% 0.53/0.73 inference(tautology,[status(thm)],[])).
% 0.53/0.73 tff(116,plain,
% 0.53/0.73 (![W0: $i] : (~(((~aElementOf0(W0, szNzAzT0)) | (~sdtlseqdt0(szszuzczcdt0(W0), xm))) <=> aElementOf0(W0, slbdtrb0(xm))))),
% 0.53/0.73 inference(unit_resolution,[status(thm)],[115, 1])).
% 0.53/0.73 tff(117,plain,
% 0.53/0.73 ((~![W0: $i] : (~(((~aElementOf0(W0, szNzAzT0)) | (~sdtlseqdt0(szszuzczcdt0(W0), xm))) <=> aElementOf0(W0, slbdtrb0(xm))))) | (~(((~aElementOf0(tptp_fun_W1_4(szszuzczcdt0(xn)), szNzAzT0)) | (~sdtlseqdt0(szszuzczcdt0(tptp_fun_W1_4(szszuzczcdt0(xn))), xm))) <=> aElementOf0(tptp_fun_W1_4(szszuzczcdt0(xn)), slbdtrb0(xm))))),
% 0.53/0.73 inference(quant_inst,[status(thm)],[])).
% 0.53/0.73 tff(118,plain,
% 0.53/0.73 (~(((~aElementOf0(tptp_fun_W1_4(szszuzczcdt0(xn)), szNzAzT0)) | (~sdtlseqdt0(szszuzczcdt0(tptp_fun_W1_4(szszuzczcdt0(xn))), xm))) <=> aElementOf0(tptp_fun_W1_4(szszuzczcdt0(xn)), slbdtrb0(xm)))),
% 0.53/0.73 inference(unit_resolution,[status(thm)],[117, 116])).
% 0.53/0.73 tff(119,plain,
% 0.53/0.73 (sdtlseqdt0(szszuzczcdt0(tptp_fun_W1_4(szszuzczcdt0(xn))), xm) <=> sdtlseqdt0(szszuzczcdt0(xn), xm)),
% 0.53/0.73 inference(monotonicity,[status(thm)],[56])).
% 0.53/0.73 tff(120,plain,
% 0.53/0.73 (sdtlseqdt0(szszuzczcdt0(xn), xm) <=> sdtlseqdt0(szszuzczcdt0(tptp_fun_W1_4(szszuzczcdt0(xn))), xm)),
% 0.53/0.73 inference(symmetry,[status(thm)],[119])).
% 0.53/0.73 tff(121,plain,
% 0.53/0.73 ((sdtlseqdt0(xm, xn) | (~aSubsetOf0(slbdtrb0(xm), slbdtrb0(xn))) | (~aSet0(slbdtrb0(xn))) | (~aSet0(slbdtrb0(xm))) | (~![W0: $i] : (~(((~aElementOf0(W0, szNzAzT0)) | (~sdtlseqdt0(szszuzczcdt0(W0), xn))) <=> aElementOf0(W0, slbdtrb0(xn))))) | (~![W0: $i] : (~(((~aElementOf0(W0, szNzAzT0)) | (~sdtlseqdt0(szszuzczcdt0(W0), xm))) <=> aElementOf0(W0, slbdtrb0(xm))))) | (~![W0: $i] : ((~aElementOf0(W0, slbdtrb0(xm))) | aElementOf0(W0, slbdtrb0(xn))))) | (~sdtlseqdt0(xm, xn))),
% 0.53/0.73 inference(tautology,[status(thm)],[])).
% 0.53/0.73 tff(122,plain,
% 0.53/0.73 (~sdtlseqdt0(xm, xn)),
% 0.53/0.73 inference(unit_resolution,[status(thm)],[121, 1])).
% 0.53/0.73 tff(123,plain,
% 0.53/0.73 (aElementOf0(xm, szNzAzT0) <=> aElementOf0(xm, szNzAzT0)),
% 0.53/0.73 inference(rewrite,[status(thm)],[])).
% 0.53/0.73 tff(124,plain,
% 0.53/0.73 (aElementOf0(xm, szNzAzT0)),
% 0.53/0.73 inference(and_elim,[status(thm)],[7])).
% 0.53/0.73 tff(125,plain,
% 0.53/0.73 (aElementOf0(xm, szNzAzT0)),
% 0.53/0.73 inference(modus_ponens,[status(thm)],[124, 123])).
% 0.53/0.73 tff(126,plain,
% 0.53/0.73 (^[W0: $i, W1: $i] : refl(((sdtlseqdt0(W0, W1) <=> sdtlseqdt0(szszuzczcdt0(W0), szszuzczcdt0(W1))) | (~aElementOf0(W1, szNzAzT0)) | (~aElementOf0(W0, szNzAzT0))) <=> ((sdtlseqdt0(W0, W1) <=> sdtlseqdt0(szszuzczcdt0(W0), szszuzczcdt0(W1))) | (~aElementOf0(W1, szNzAzT0)) | (~aElementOf0(W0, szNzAzT0))))),
% 0.53/0.73 inference(bind,[status(th)],[])).
% 0.53/0.73 tff(127,plain,
% 0.53/0.73 (![W0: $i, W1: $i] : ((sdtlseqdt0(W0, W1) <=> sdtlseqdt0(szszuzczcdt0(W0), szszuzczcdt0(W1))) | (~aElementOf0(W1, szNzAzT0)) | (~aElementOf0(W0, szNzAzT0))) <=> ![W0: $i, W1: $i] : ((sdtlseqdt0(W0, W1) <=> sdtlseqdt0(szszuzczcdt0(W0), szszuzczcdt0(W1))) | (~aElementOf0(W1, szNzAzT0)) | (~aElementOf0(W0, szNzAzT0)))),
% 0.53/0.73 inference(quant_intro,[status(thm)],[126])).
% 0.53/0.73 tff(128,plain,
% 0.53/0.73 (^[W0: $i, W1: $i] : trans(monotonicity(trans(monotonicity(rewrite((aElementOf0(W0, szNzAzT0) & aElementOf0(W1, szNzAzT0)) <=> (~((~aElementOf0(W1, szNzAzT0)) | (~aElementOf0(W0, szNzAzT0))))), ((~(aElementOf0(W0, szNzAzT0) & aElementOf0(W1, szNzAzT0))) <=> (~(~((~aElementOf0(W1, szNzAzT0)) | (~aElementOf0(W0, szNzAzT0))))))), rewrite((~(~((~aElementOf0(W1, szNzAzT0)) | (~aElementOf0(W0, szNzAzT0))))) <=> ((~aElementOf0(W1, szNzAzT0)) | (~aElementOf0(W0, szNzAzT0)))), ((~(aElementOf0(W0, szNzAzT0) & aElementOf0(W1, szNzAzT0))) <=> ((~aElementOf0(W1, szNzAzT0)) | (~aElementOf0(W0, szNzAzT0))))), (((~(aElementOf0(W0, szNzAzT0) & aElementOf0(W1, szNzAzT0))) | (sdtlseqdt0(W0, W1) <=> sdtlseqdt0(szszuzczcdt0(W0), szszuzczcdt0(W1)))) <=> (((~aElementOf0(W1, szNzAzT0)) | (~aElementOf0(W0, szNzAzT0))) | (sdtlseqdt0(W0, W1) <=> sdtlseqdt0(szszuzczcdt0(W0), szszuzczcdt0(W1)))))), rewrite((((~aElementOf0(W1, szNzAzT0)) | (~aElementOf0(W0, szNzAzT0))) | (sdtlseqdt0(W0, W1) <=> sdtlseqdt0(szszuzczcdt0(W0), szszuzczcdt0(W1)))) <=> ((sdtlseqdt0(W0, W1) <=> sdtlseqdt0(szszuzczcdt0(W0), szszuzczcdt0(W1))) | (~aElementOf0(W1, szNzAzT0)) | (~aElementOf0(W0, szNzAzT0)))), (((~(aElementOf0(W0, szNzAzT0) & aElementOf0(W1, szNzAzT0))) | (sdtlseqdt0(W0, W1) <=> sdtlseqdt0(szszuzczcdt0(W0), szszuzczcdt0(W1)))) <=> ((sdtlseqdt0(W0, W1) <=> sdtlseqdt0(szszuzczcdt0(W0), szszuzczcdt0(W1))) | (~aElementOf0(W1, szNzAzT0)) | (~aElementOf0(W0, szNzAzT0)))))),
% 0.53/0.73 inference(bind,[status(th)],[])).
% 0.53/0.73 tff(129,plain,
% 0.53/0.73 (![W0: $i, W1: $i] : ((~(aElementOf0(W0, szNzAzT0) & aElementOf0(W1, szNzAzT0))) | (sdtlseqdt0(W0, W1) <=> sdtlseqdt0(szszuzczcdt0(W0), szszuzczcdt0(W1)))) <=> ![W0: $i, W1: $i] : ((sdtlseqdt0(W0, W1) <=> sdtlseqdt0(szszuzczcdt0(W0), szszuzczcdt0(W1))) | (~aElementOf0(W1, szNzAzT0)) | (~aElementOf0(W0, szNzAzT0)))),
% 0.53/0.73 inference(quant_intro,[status(thm)],[128])).
% 0.53/0.73 tff(130,plain,
% 0.53/0.73 (![W0: $i, W1: $i] : ((~(aElementOf0(W0, szNzAzT0) & aElementOf0(W1, szNzAzT0))) | (sdtlseqdt0(W0, W1) <=> sdtlseqdt0(szszuzczcdt0(W0), szszuzczcdt0(W1)))) <=> ![W0: $i, W1: $i] : ((~(aElementOf0(W0, szNzAzT0) & aElementOf0(W1, szNzAzT0))) | (sdtlseqdt0(W0, W1) <=> sdtlseqdt0(szszuzczcdt0(W0), szszuzczcdt0(W1))))),
% 0.53/0.73 inference(rewrite,[status(thm)],[])).
% 0.53/0.73 tff(131,plain,
% 0.53/0.73 (^[W0: $i, W1: $i] : rewrite(((aElementOf0(W0, szNzAzT0) & aElementOf0(W1, szNzAzT0)) => (sdtlseqdt0(W0, W1) <=> sdtlseqdt0(szszuzczcdt0(W0), szszuzczcdt0(W1)))) <=> ((~(aElementOf0(W0, szNzAzT0) & aElementOf0(W1, szNzAzT0))) | (sdtlseqdt0(W0, W1) <=> sdtlseqdt0(szszuzczcdt0(W0), szszuzczcdt0(W1)))))),
% 0.53/0.73 inference(bind,[status(th)],[])).
% 0.53/0.73 tff(132,plain,
% 0.53/0.73 (![W0: $i, W1: $i] : ((aElementOf0(W0, szNzAzT0) & aElementOf0(W1, szNzAzT0)) => (sdtlseqdt0(W0, W1) <=> sdtlseqdt0(szszuzczcdt0(W0), szszuzczcdt0(W1)))) <=> ![W0: $i, W1: $i] : ((~(aElementOf0(W0, szNzAzT0) & aElementOf0(W1, szNzAzT0))) | (sdtlseqdt0(W0, W1) <=> sdtlseqdt0(szszuzczcdt0(W0), szszuzczcdt0(W1))))),
% 0.53/0.73 inference(quant_intro,[status(thm)],[131])).
% 0.53/0.73 tff(133,axiom,(![W0: $i, W1: $i] : ((aElementOf0(W0, szNzAzT0) & aElementOf0(W1, szNzAzT0)) => (sdtlseqdt0(W0, W1) <=> sdtlseqdt0(szszuzczcdt0(W0), szszuzczcdt0(W1))))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','mSuccLess')).
% 0.53/0.73 tff(134,plain,
% 0.53/0.73 (![W0: $i, W1: $i] : ((~(aElementOf0(W0, szNzAzT0) & aElementOf0(W1, szNzAzT0))) | (sdtlseqdt0(W0, W1) <=> sdtlseqdt0(szszuzczcdt0(W0), szszuzczcdt0(W1))))),
% 0.53/0.73 inference(modus_ponens,[status(thm)],[133, 132])).
% 0.53/0.73 tff(135,plain,
% 0.53/0.73 (![W0: $i, W1: $i] : ((~(aElementOf0(W0, szNzAzT0) & aElementOf0(W1, szNzAzT0))) | (sdtlseqdt0(W0, W1) <=> sdtlseqdt0(szszuzczcdt0(W0), szszuzczcdt0(W1))))),
% 0.53/0.73 inference(modus_ponens,[status(thm)],[134, 130])).
% 0.53/0.73 tff(136,plain,(
% 0.53/0.73 ![W0: $i, W1: $i] : ((~(aElementOf0(W0, szNzAzT0) & aElementOf0(W1, szNzAzT0))) | (sdtlseqdt0(W0, W1) <=> sdtlseqdt0(szszuzczcdt0(W0), szszuzczcdt0(W1))))),
% 0.53/0.73 inference(skolemize,[status(sab)],[135])).
% 0.53/0.73 tff(137,plain,
% 0.53/0.73 (![W0: $i, W1: $i] : ((sdtlseqdt0(W0, W1) <=> sdtlseqdt0(szszuzczcdt0(W0), szszuzczcdt0(W1))) | (~aElementOf0(W1, szNzAzT0)) | (~aElementOf0(W0, szNzAzT0)))),
% 0.53/0.73 inference(modus_ponens,[status(thm)],[136, 129])).
% 0.53/0.73 tff(138,plain,
% 0.53/0.73 (![W0: $i, W1: $i] : ((sdtlseqdt0(W0, W1) <=> sdtlseqdt0(szszuzczcdt0(W0), szszuzczcdt0(W1))) | (~aElementOf0(W1, szNzAzT0)) | (~aElementOf0(W0, szNzAzT0)))),
% 0.53/0.73 inference(modus_ponens,[status(thm)],[137, 127])).
% 0.53/0.73 tff(139,plain,
% 0.53/0.73 (((~![W0: $i, W1: $i] : ((sdtlseqdt0(W0, W1) <=> sdtlseqdt0(szszuzczcdt0(W0), szszuzczcdt0(W1))) | (~aElementOf0(W1, szNzAzT0)) | (~aElementOf0(W0, szNzAzT0)))) | ((~aElementOf0(xm, szNzAzT0)) | (~aElementOf0(xn, szNzAzT0)) | (sdtlseqdt0(xm, xn) <=> sdtlseqdt0(szszuzczcdt0(xm), szszuzczcdt0(xn))))) <=> ((~![W0: $i, W1: $i] : ((sdtlseqdt0(W0, W1) <=> sdtlseqdt0(szszuzczcdt0(W0), szszuzczcdt0(W1))) | (~aElementOf0(W1, szNzAzT0)) | (~aElementOf0(W0, szNzAzT0)))) | (~aElementOf0(xm, szNzAzT0)) | (~aElementOf0(xn, szNzAzT0)) | (sdtlseqdt0(xm, xn) <=> sdtlseqdt0(szszuzczcdt0(xm), szszuzczcdt0(xn))))),
% 0.53/0.73 inference(rewrite,[status(thm)],[])).
% 0.53/0.73 tff(140,plain,
% 0.53/0.73 (((sdtlseqdt0(xm, xn) <=> sdtlseqdt0(szszuzczcdt0(xm), szszuzczcdt0(xn))) | (~aElementOf0(xn, szNzAzT0)) | (~aElementOf0(xm, szNzAzT0))) <=> ((~aElementOf0(xm, szNzAzT0)) | (~aElementOf0(xn, szNzAzT0)) | (sdtlseqdt0(xm, xn) <=> sdtlseqdt0(szszuzczcdt0(xm), szszuzczcdt0(xn))))),
% 0.53/0.73 inference(rewrite,[status(thm)],[])).
% 0.53/0.73 tff(141,plain,
% 0.53/0.73 (((~![W0: $i, W1: $i] : ((sdtlseqdt0(W0, W1) <=> sdtlseqdt0(szszuzczcdt0(W0), szszuzczcdt0(W1))) | (~aElementOf0(W1, szNzAzT0)) | (~aElementOf0(W0, szNzAzT0)))) | ((sdtlseqdt0(xm, xn) <=> sdtlseqdt0(szszuzczcdt0(xm), szszuzczcdt0(xn))) | (~aElementOf0(xn, szNzAzT0)) | (~aElementOf0(xm, szNzAzT0)))) <=> ((~![W0: $i, W1: $i] : ((sdtlseqdt0(W0, W1) <=> sdtlseqdt0(szszuzczcdt0(W0), szszuzczcdt0(W1))) | (~aElementOf0(W1, szNzAzT0)) | (~aElementOf0(W0, szNzAzT0)))) | ((~aElementOf0(xm, szNzAzT0)) | (~aElementOf0(xn, szNzAzT0)) | (sdtlseqdt0(xm, xn) <=> sdtlseqdt0(szszuzczcdt0(xm), szszuzczcdt0(xn)))))),
% 0.53/0.73 inference(monotonicity,[status(thm)],[140])).
% 0.53/0.73 tff(142,plain,
% 0.53/0.73 (((~![W0: $i, W1: $i] : ((sdtlseqdt0(W0, W1) <=> sdtlseqdt0(szszuzczcdt0(W0), szszuzczcdt0(W1))) | (~aElementOf0(W1, szNzAzT0)) | (~aElementOf0(W0, szNzAzT0)))) | ((sdtlseqdt0(xm, xn) <=> sdtlseqdt0(szszuzczcdt0(xm), szszuzczcdt0(xn))) | (~aElementOf0(xn, szNzAzT0)) | (~aElementOf0(xm, szNzAzT0)))) <=> ((~![W0: $i, W1: $i] : ((sdtlseqdt0(W0, W1) <=> sdtlseqdt0(szszuzczcdt0(W0), szszuzczcdt0(W1))) | (~aElementOf0(W1, szNzAzT0)) | (~aElementOf0(W0, szNzAzT0)))) | (~aElementOf0(xm, szNzAzT0)) | (~aElementOf0(xn, szNzAzT0)) | (sdtlseqdt0(xm, xn) <=> sdtlseqdt0(szszuzczcdt0(xm), szszuzczcdt0(xn))))),
% 0.53/0.73 inference(transitivity,[status(thm)],[141, 139])).
% 0.53/0.73 tff(143,plain,
% 0.53/0.73 ((~![W0: $i, W1: $i] : ((sdtlseqdt0(W0, W1) <=> sdtlseqdt0(szszuzczcdt0(W0), szszuzczcdt0(W1))) | (~aElementOf0(W1, szNzAzT0)) | (~aElementOf0(W0, szNzAzT0)))) | ((sdtlseqdt0(xm, xn) <=> sdtlseqdt0(szszuzczcdt0(xm), szszuzczcdt0(xn))) | (~aElementOf0(xn, szNzAzT0)) | (~aElementOf0(xm, szNzAzT0)))),
% 0.53/0.73 inference(quant_inst,[status(thm)],[])).
% 0.53/0.73 tff(144,plain,
% 0.53/0.73 ((~![W0: $i, W1: $i] : ((sdtlseqdt0(W0, W1) <=> sdtlseqdt0(szszuzczcdt0(W0), szszuzczcdt0(W1))) | (~aElementOf0(W1, szNzAzT0)) | (~aElementOf0(W0, szNzAzT0)))) | (~aElementOf0(xm, szNzAzT0)) | (~aElementOf0(xn, szNzAzT0)) | (sdtlseqdt0(xm, xn) <=> sdtlseqdt0(szszuzczcdt0(xm), szszuzczcdt0(xn)))),
% 0.53/0.73 inference(modus_ponens,[status(thm)],[143, 142])).
% 0.53/0.73 tff(145,plain,
% 0.53/0.73 (sdtlseqdt0(xm, xn) <=> sdtlseqdt0(szszuzczcdt0(xm), szszuzczcdt0(xn))),
% 0.53/0.73 inference(unit_resolution,[status(thm)],[144, 138, 125, 9])).
% 0.53/0.73 tff(146,plain,
% 0.53/0.73 ((~(sdtlseqdt0(xm, xn) <=> sdtlseqdt0(szszuzczcdt0(xm), szszuzczcdt0(xn)))) | sdtlseqdt0(xm, xn) | (~sdtlseqdt0(szszuzczcdt0(xm), szszuzczcdt0(xn)))),
% 0.53/0.73 inference(tautology,[status(thm)],[])).
% 0.53/0.73 tff(147,plain,
% 0.53/0.73 (sdtlseqdt0(xm, xn) | (~sdtlseqdt0(szszuzczcdt0(xm), szszuzczcdt0(xn)))),
% 0.53/0.73 inference(unit_resolution,[status(thm)],[146, 145])).
% 0.53/0.73 tff(148,plain,
% 0.53/0.73 (~sdtlseqdt0(szszuzczcdt0(xm), szszuzczcdt0(xn))),
% 0.53/0.73 inference(unit_resolution,[status(thm)],[147, 122])).
% 0.53/0.73 tff(149,plain,
% 0.53/0.73 (^[W0: $i, W1: $i] : refl((sdtlseqdt0(W0, W1) | sdtlseqdt0(szszuzczcdt0(W1), W0) | (~aElementOf0(W1, szNzAzT0)) | (~aElementOf0(W0, szNzAzT0))) <=> (sdtlseqdt0(W0, W1) | sdtlseqdt0(szszuzczcdt0(W1), W0) | (~aElementOf0(W1, szNzAzT0)) | (~aElementOf0(W0, szNzAzT0))))),
% 0.53/0.73 inference(bind,[status(th)],[])).
% 0.53/0.73 tff(150,plain,
% 0.53/0.73 (![W0: $i, W1: $i] : (sdtlseqdt0(W0, W1) | sdtlseqdt0(szszuzczcdt0(W1), W0) | (~aElementOf0(W1, szNzAzT0)) | (~aElementOf0(W0, szNzAzT0))) <=> ![W0: $i, W1: $i] : (sdtlseqdt0(W0, W1) | sdtlseqdt0(szszuzczcdt0(W1), W0) | (~aElementOf0(W1, szNzAzT0)) | (~aElementOf0(W0, szNzAzT0)))),
% 0.53/0.73 inference(quant_intro,[status(thm)],[149])).
% 0.53/0.73 tff(151,plain,
% 0.53/0.73 (^[W0: $i, W1: $i] : trans(monotonicity(trans(monotonicity(rewrite((aElementOf0(W0, szNzAzT0) & aElementOf0(W1, szNzAzT0)) <=> (~((~aElementOf0(W1, szNzAzT0)) | (~aElementOf0(W0, szNzAzT0))))), ((~(aElementOf0(W0, szNzAzT0) & aElementOf0(W1, szNzAzT0))) <=> (~(~((~aElementOf0(W1, szNzAzT0)) | (~aElementOf0(W0, szNzAzT0))))))), rewrite((~(~((~aElementOf0(W1, szNzAzT0)) | (~aElementOf0(W0, szNzAzT0))))) <=> ((~aElementOf0(W1, szNzAzT0)) | (~aElementOf0(W0, szNzAzT0)))), ((~(aElementOf0(W0, szNzAzT0) & aElementOf0(W1, szNzAzT0))) <=> ((~aElementOf0(W1, szNzAzT0)) | (~aElementOf0(W0, szNzAzT0))))), ((sdtlseqdt0(W0, W1) | sdtlseqdt0(szszuzczcdt0(W1), W0) | (~(aElementOf0(W0, szNzAzT0) & aElementOf0(W1, szNzAzT0)))) <=> (sdtlseqdt0(W0, W1) | sdtlseqdt0(szszuzczcdt0(W1), W0) | ((~aElementOf0(W1, szNzAzT0)) | (~aElementOf0(W0, szNzAzT0)))))), rewrite((sdtlseqdt0(W0, W1) | sdtlseqdt0(szszuzczcdt0(W1), W0) | ((~aElementOf0(W1, szNzAzT0)) | (~aElementOf0(W0, szNzAzT0)))) <=> (sdtlseqdt0(W0, W1) | sdtlseqdt0(szszuzczcdt0(W1), W0) | (~aElementOf0(W1, szNzAzT0)) | (~aElementOf0(W0, szNzAzT0)))), ((sdtlseqdt0(W0, W1) | sdtlseqdt0(szszuzczcdt0(W1), W0) | (~(aElementOf0(W0, szNzAzT0) & aElementOf0(W1, szNzAzT0)))) <=> (sdtlseqdt0(W0, W1) | sdtlseqdt0(szszuzczcdt0(W1), W0) | (~aElementOf0(W1, szNzAzT0)) | (~aElementOf0(W0, szNzAzT0)))))),
% 0.53/0.73 inference(bind,[status(th)],[])).
% 0.53/0.73 tff(152,plain,
% 0.53/0.73 (![W0: $i, W1: $i] : (sdtlseqdt0(W0, W1) | sdtlseqdt0(szszuzczcdt0(W1), W0) | (~(aElementOf0(W0, szNzAzT0) & aElementOf0(W1, szNzAzT0)))) <=> ![W0: $i, W1: $i] : (sdtlseqdt0(W0, W1) | sdtlseqdt0(szszuzczcdt0(W1), W0) | (~aElementOf0(W1, szNzAzT0)) | (~aElementOf0(W0, szNzAzT0)))),
% 0.53/0.73 inference(quant_intro,[status(thm)],[151])).
% 0.53/0.73 tff(153,plain,
% 0.53/0.73 (![W0: $i, W1: $i] : (sdtlseqdt0(W0, W1) | sdtlseqdt0(szszuzczcdt0(W1), W0) | (~(aElementOf0(W0, szNzAzT0) & aElementOf0(W1, szNzAzT0)))) <=> ![W0: $i, W1: $i] : (sdtlseqdt0(W0, W1) | sdtlseqdt0(szszuzczcdt0(W1), W0) | (~(aElementOf0(W0, szNzAzT0) & aElementOf0(W1, szNzAzT0))))),
% 0.53/0.73 inference(rewrite,[status(thm)],[])).
% 0.53/0.73 tff(154,plain,
% 0.53/0.73 (^[W0: $i, W1: $i] : rewrite(((aElementOf0(W0, szNzAzT0) & aElementOf0(W1, szNzAzT0)) => (sdtlseqdt0(W0, W1) | sdtlseqdt0(szszuzczcdt0(W1), W0))) <=> (sdtlseqdt0(W0, W1) | sdtlseqdt0(szszuzczcdt0(W1), W0) | (~(aElementOf0(W0, szNzAzT0) & aElementOf0(W1, szNzAzT0)))))),
% 0.53/0.73 inference(bind,[status(th)],[])).
% 0.53/0.73 tff(155,plain,
% 0.53/0.73 (![W0: $i, W1: $i] : ((aElementOf0(W0, szNzAzT0) & aElementOf0(W1, szNzAzT0)) => (sdtlseqdt0(W0, W1) | sdtlseqdt0(szszuzczcdt0(W1), W0))) <=> ![W0: $i, W1: $i] : (sdtlseqdt0(W0, W1) | sdtlseqdt0(szszuzczcdt0(W1), W0) | (~(aElementOf0(W0, szNzAzT0) & aElementOf0(W1, szNzAzT0))))),
% 0.53/0.73 inference(quant_intro,[status(thm)],[154])).
% 0.53/0.73 tff(156,axiom,(![W0: $i, W1: $i] : ((aElementOf0(W0, szNzAzT0) & aElementOf0(W1, szNzAzT0)) => (sdtlseqdt0(W0, W1) | sdtlseqdt0(szszuzczcdt0(W1), W0)))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','mLessTotal')).
% 0.53/0.73 tff(157,plain,
% 0.53/0.73 (![W0: $i, W1: $i] : (sdtlseqdt0(W0, W1) | sdtlseqdt0(szszuzczcdt0(W1), W0) | (~(aElementOf0(W0, szNzAzT0) & aElementOf0(W1, szNzAzT0))))),
% 0.53/0.73 inference(modus_ponens,[status(thm)],[156, 155])).
% 0.53/0.73 tff(158,plain,
% 0.53/0.73 (![W0: $i, W1: $i] : (sdtlseqdt0(W0, W1) | sdtlseqdt0(szszuzczcdt0(W1), W0) | (~(aElementOf0(W0, szNzAzT0) & aElementOf0(W1, szNzAzT0))))),
% 0.53/0.73 inference(modus_ponens,[status(thm)],[157, 153])).
% 0.53/0.73 tff(159,plain,(
% 0.53/0.73 ![W0: $i, W1: $i] : (sdtlseqdt0(W0, W1) | sdtlseqdt0(szszuzczcdt0(W1), W0) | (~(aElementOf0(W0, szNzAzT0) & aElementOf0(W1, szNzAzT0))))),
% 0.53/0.73 inference(skolemize,[status(sab)],[158])).
% 0.53/0.73 tff(160,plain,
% 0.53/0.73 (![W0: $i, W1: $i] : (sdtlseqdt0(W0, W1) | sdtlseqdt0(szszuzczcdt0(W1), W0) | (~aElementOf0(W1, szNzAzT0)) | (~aElementOf0(W0, szNzAzT0)))),
% 0.53/0.73 inference(modus_ponens,[status(thm)],[159, 152])).
% 0.53/0.73 tff(161,plain,
% 0.53/0.73 (![W0: $i, W1: $i] : (sdtlseqdt0(W0, W1) | sdtlseqdt0(szszuzczcdt0(W1), W0) | (~aElementOf0(W1, szNzAzT0)) | (~aElementOf0(W0, szNzAzT0)))),
% 0.53/0.73 inference(modus_ponens,[status(thm)],[160, 150])).
% 0.53/0.73 tff(162,plain,
% 0.53/0.73 (((~![W0: $i, W1: $i] : (sdtlseqdt0(W0, W1) | sdtlseqdt0(szszuzczcdt0(W1), W0) | (~aElementOf0(W1, szNzAzT0)) | (~aElementOf0(W0, szNzAzT0)))) | ((~aElementOf0(xm, szNzAzT0)) | sdtlseqdt0(szszuzczcdt0(xm), szszuzczcdt0(xn)) | (~aElementOf0(szszuzczcdt0(xn), szNzAzT0)) | sdtlseqdt0(szszuzczcdt0(xn), xm))) <=> ((~![W0: $i, W1: $i] : (sdtlseqdt0(W0, W1) | sdtlseqdt0(szszuzczcdt0(W1), W0) | (~aElementOf0(W1, szNzAzT0)) | (~aElementOf0(W0, szNzAzT0)))) | (~aElementOf0(xm, szNzAzT0)) | sdtlseqdt0(szszuzczcdt0(xm), szszuzczcdt0(xn)) | (~aElementOf0(szszuzczcdt0(xn), szNzAzT0)) | sdtlseqdt0(szszuzczcdt0(xn), xm))),
% 0.53/0.73 inference(rewrite,[status(thm)],[])).
% 0.53/0.73 tff(163,plain,
% 0.53/0.73 ((sdtlseqdt0(szszuzczcdt0(xn), xm) | sdtlseqdt0(szszuzczcdt0(xm), szszuzczcdt0(xn)) | (~aElementOf0(xm, szNzAzT0)) | (~aElementOf0(szszuzczcdt0(xn), szNzAzT0))) <=> ((~aElementOf0(xm, szNzAzT0)) | sdtlseqdt0(szszuzczcdt0(xm), szszuzczcdt0(xn)) | (~aElementOf0(szszuzczcdt0(xn), szNzAzT0)) | sdtlseqdt0(szszuzczcdt0(xn), xm))),
% 0.53/0.73 inference(rewrite,[status(thm)],[])).
% 0.53/0.73 tff(164,plain,
% 0.53/0.73 (((~![W0: $i, W1: $i] : (sdtlseqdt0(W0, W1) | sdtlseqdt0(szszuzczcdt0(W1), W0) | (~aElementOf0(W1, szNzAzT0)) | (~aElementOf0(W0, szNzAzT0)))) | (sdtlseqdt0(szszuzczcdt0(xn), xm) | sdtlseqdt0(szszuzczcdt0(xm), szszuzczcdt0(xn)) | (~aElementOf0(xm, szNzAzT0)) | (~aElementOf0(szszuzczcdt0(xn), szNzAzT0)))) <=> ((~![W0: $i, W1: $i] : (sdtlseqdt0(W0, W1) | sdtlseqdt0(szszuzczcdt0(W1), W0) | (~aElementOf0(W1, szNzAzT0)) | (~aElementOf0(W0, szNzAzT0)))) | ((~aElementOf0(xm, szNzAzT0)) | sdtlseqdt0(szszuzczcdt0(xm), szszuzczcdt0(xn)) | (~aElementOf0(szszuzczcdt0(xn), szNzAzT0)) | sdtlseqdt0(szszuzczcdt0(xn), xm)))),
% 0.53/0.73 inference(monotonicity,[status(thm)],[163])).
% 0.53/0.73 tff(165,plain,
% 0.53/0.73 (((~![W0: $i, W1: $i] : (sdtlseqdt0(W0, W1) | sdtlseqdt0(szszuzczcdt0(W1), W0) | (~aElementOf0(W1, szNzAzT0)) | (~aElementOf0(W0, szNzAzT0)))) | (sdtlseqdt0(szszuzczcdt0(xn), xm) | sdtlseqdt0(szszuzczcdt0(xm), szszuzczcdt0(xn)) | (~aElementOf0(xm, szNzAzT0)) | (~aElementOf0(szszuzczcdt0(xn), szNzAzT0)))) <=> ((~![W0: $i, W1: $i] : (sdtlseqdt0(W0, W1) | sdtlseqdt0(szszuzczcdt0(W1), W0) | (~aElementOf0(W1, szNzAzT0)) | (~aElementOf0(W0, szNzAzT0)))) | (~aElementOf0(xm, szNzAzT0)) | sdtlseqdt0(szszuzczcdt0(xm), szszuzczcdt0(xn)) | (~aElementOf0(szszuzczcdt0(xn), szNzAzT0)) | sdtlseqdt0(szszuzczcdt0(xn), xm))),
% 0.53/0.73 inference(transitivity,[status(thm)],[164, 162])).
% 0.53/0.73 tff(166,plain,
% 0.53/0.73 ((~![W0: $i, W1: $i] : (sdtlseqdt0(W0, W1) | sdtlseqdt0(szszuzczcdt0(W1), W0) | (~aElementOf0(W1, szNzAzT0)) | (~aElementOf0(W0, szNzAzT0)))) | (sdtlseqdt0(szszuzczcdt0(xn), xm) | sdtlseqdt0(szszuzczcdt0(xm), szszuzczcdt0(xn)) | (~aElementOf0(xm, szNzAzT0)) | (~aElementOf0(szszuzczcdt0(xn), szNzAzT0)))),
% 0.53/0.73 inference(quant_inst,[status(thm)],[])).
% 0.53/0.73 tff(167,plain,
% 0.53/0.73 ((~![W0: $i, W1: $i] : (sdtlseqdt0(W0, W1) | sdtlseqdt0(szszuzczcdt0(W1), W0) | (~aElementOf0(W1, szNzAzT0)) | (~aElementOf0(W0, szNzAzT0)))) | (~aElementOf0(xm, szNzAzT0)) | sdtlseqdt0(szszuzczcdt0(xm), szszuzczcdt0(xn)) | (~aElementOf0(szszuzczcdt0(xn), szNzAzT0)) | sdtlseqdt0(szszuzczcdt0(xn), xm)),
% 0.53/0.73 inference(modus_ponens,[status(thm)],[166, 165])).
% 0.53/0.73 tff(168,plain,
% 0.53/0.73 (sdtlseqdt0(szszuzczcdt0(xm), szszuzczcdt0(xn)) | sdtlseqdt0(szszuzczcdt0(xn), xm)),
% 0.53/0.73 inference(unit_resolution,[status(thm)],[167, 161, 125, 30])).
% 0.53/0.73 tff(169,plain,
% 0.53/0.73 (sdtlseqdt0(szszuzczcdt0(xn), xm)),
% 0.53/0.73 inference(unit_resolution,[status(thm)],[168, 148])).
% 0.53/0.73 tff(170,plain,
% 0.53/0.73 (sdtlseqdt0(szszuzczcdt0(tptp_fun_W1_4(szszuzczcdt0(xn))), xm)),
% 0.53/0.73 inference(modus_ponens,[status(thm)],[169, 120])).
% 0.53/0.73 tff(171,plain,
% 0.53/0.73 (((~aElementOf0(tptp_fun_W1_4(szszuzczcdt0(xn)), szNzAzT0)) | (~(szszuzczcdt0(xn) = szszuzczcdt0(tptp_fun_W1_4(szszuzczcdt0(xn)))))) | aElementOf0(tptp_fun_W1_4(szszuzczcdt0(xn)), szNzAzT0)),
% 0.53/0.73 inference(tautology,[status(thm)],[])).
% 0.53/0.73 tff(172,plain,
% 0.53/0.73 (aElementOf0(tptp_fun_W1_4(szszuzczcdt0(xn)), szNzAzT0)),
% 0.53/0.73 inference(unit_resolution,[status(thm)],[171, 53])).
% 0.53/0.73 tff(173,plain,
% 0.53/0.73 ((~((~aElementOf0(tptp_fun_W1_4(szszuzczcdt0(xn)), szNzAzT0)) | (~sdtlseqdt0(szszuzczcdt0(tptp_fun_W1_4(szszuzczcdt0(xn))), xm)))) | (~aElementOf0(tptp_fun_W1_4(szszuzczcdt0(xn)), szNzAzT0)) | (~sdtlseqdt0(szszuzczcdt0(tptp_fun_W1_4(szszuzczcdt0(xn))), xm))),
% 0.53/0.73 inference(tautology,[status(thm)],[])).
% 0.53/0.73 tff(174,plain,
% 0.53/0.73 (~((~aElementOf0(tptp_fun_W1_4(szszuzczcdt0(xn)), szNzAzT0)) | (~sdtlseqdt0(szszuzczcdt0(tptp_fun_W1_4(szszuzczcdt0(xn))), xm)))),
% 0.53/0.73 inference(unit_resolution,[status(thm)],[173, 172, 170])).
% 0.53/0.73 tff(175,plain,
% 0.53/0.73 ((((~aElementOf0(tptp_fun_W1_4(szszuzczcdt0(xn)), szNzAzT0)) | (~sdtlseqdt0(szszuzczcdt0(tptp_fun_W1_4(szszuzczcdt0(xn))), xm))) <=> aElementOf0(tptp_fun_W1_4(szszuzczcdt0(xn)), slbdtrb0(xm))) | ((~aElementOf0(tptp_fun_W1_4(szszuzczcdt0(xn)), szNzAzT0)) | (~sdtlseqdt0(szszuzczcdt0(tptp_fun_W1_4(szszuzczcdt0(xn))), xm))) | aElementOf0(tptp_fun_W1_4(szszuzczcdt0(xn)), slbdtrb0(xm))),
% 0.53/0.73 inference(tautology,[status(thm)],[])).
% 0.53/0.73 tff(176,plain,
% 0.53/0.73 ((((~aElementOf0(tptp_fun_W1_4(szszuzczcdt0(xn)), szNzAzT0)) | (~sdtlseqdt0(szszuzczcdt0(tptp_fun_W1_4(szszuzczcdt0(xn))), xm))) <=> aElementOf0(tptp_fun_W1_4(szszuzczcdt0(xn)), slbdtrb0(xm))) | aElementOf0(tptp_fun_W1_4(szszuzczcdt0(xn)), slbdtrb0(xm))),
% 0.53/0.73 inference(unit_resolution,[status(thm)],[175, 174])).
% 0.53/0.73 tff(177,plain,
% 0.53/0.73 (aElementOf0(tptp_fun_W1_4(szszuzczcdt0(xn)), slbdtrb0(xm))),
% 0.53/0.73 inference(unit_resolution,[status(thm)],[176, 118])).
% 0.53/0.73 tff(178,plain,
% 0.53/0.73 ((sdtlseqdt0(xm, xn) | (~aSubsetOf0(slbdtrb0(xm), slbdtrb0(xn))) | (~aSet0(slbdtrb0(xn))) | (~aSet0(slbdtrb0(xm))) | (~![W0: $i] : (~(((~aElementOf0(W0, szNzAzT0)) | (~sdtlseqdt0(szszuzczcdt0(W0), xn))) <=> aElementOf0(W0, slbdtrb0(xn))))) | (~![W0: $i] : (~(((~aElementOf0(W0, szNzAzT0)) | (~sdtlseqdt0(szszuzczcdt0(W0), xm))) <=> aElementOf0(W0, slbdtrb0(xm))))) | (~![W0: $i] : ((~aElementOf0(W0, slbdtrb0(xm))) | aElementOf0(W0, slbdtrb0(xn))))) | ![W0: $i] : ((~aElementOf0(W0, slbdtrb0(xm))) | aElementOf0(W0, slbdtrb0(xn)))),
% 0.53/0.73 inference(tautology,[status(thm)],[])).
% 0.53/0.73 tff(179,plain,
% 0.53/0.73 (![W0: $i] : ((~aElementOf0(W0, slbdtrb0(xm))) | aElementOf0(W0, slbdtrb0(xn)))),
% 0.53/0.73 inference(unit_resolution,[status(thm)],[178, 1])).
% 0.53/0.73 tff(180,plain,
% 0.53/0.73 (((~![W0: $i] : ((~aElementOf0(W0, slbdtrb0(xm))) | aElementOf0(W0, slbdtrb0(xn)))) | ((~aElementOf0(tptp_fun_W1_4(szszuzczcdt0(xn)), slbdtrb0(xm))) | aElementOf0(tptp_fun_W1_4(szszuzczcdt0(xn)), slbdtrb0(xn)))) <=> ((~![W0: $i] : ((~aElementOf0(W0, slbdtrb0(xm))) | aElementOf0(W0, slbdtrb0(xn)))) | (~aElementOf0(tptp_fun_W1_4(szszuzczcdt0(xn)), slbdtrb0(xm))) | aElementOf0(tptp_fun_W1_4(szszuzczcdt0(xn)), slbdtrb0(xn)))),
% 0.53/0.73 inference(rewrite,[status(thm)],[])).
% 0.53/0.73 tff(181,plain,
% 0.53/0.73 ((~![W0: $i] : ((~aElementOf0(W0, slbdtrb0(xm))) | aElementOf0(W0, slbdtrb0(xn)))) | ((~aElementOf0(tptp_fun_W1_4(szszuzczcdt0(xn)), slbdtrb0(xm))) | aElementOf0(tptp_fun_W1_4(szszuzczcdt0(xn)), slbdtrb0(xn)))),
% 0.53/0.73 inference(quant_inst,[status(thm)],[])).
% 0.53/0.73 tff(182,plain,
% 0.53/0.73 ((~![W0: $i] : ((~aElementOf0(W0, slbdtrb0(xm))) | aElementOf0(W0, slbdtrb0(xn)))) | (~aElementOf0(tptp_fun_W1_4(szszuzczcdt0(xn)), slbdtrb0(xm))) | aElementOf0(tptp_fun_W1_4(szszuzczcdt0(xn)), slbdtrb0(xn))),
% 0.53/0.73 inference(modus_ponens,[status(thm)],[181, 180])).
% 0.53/0.73 tff(183,plain,
% 0.53/0.73 ($false),
% 0.53/0.73 inference(unit_resolution,[status(thm)],[182, 179, 177, 114])).
% 0.53/0.73 tff(184,plain,(sdtlseqdt0(xm, xn) | (~aSubsetOf0(slbdtrb0(xm), slbdtrb0(xn))) | (~aSet0(slbdtrb0(xn))) | (~aSet0(slbdtrb0(xm))) | (~![W0: $i] : (~(((~aElementOf0(W0, szNzAzT0)) | (~sdtlseqdt0(szszuzczcdt0(W0), xn))) <=> aElementOf0(W0, slbdtrb0(xn))))) | (~![W0: $i] : (~(((~aElementOf0(W0, szNzAzT0)) | (~sdtlseqdt0(szszuzczcdt0(W0), xm))) <=> aElementOf0(W0, slbdtrb0(xm))))) | (~![W0: $i] : ((~aElementOf0(W0, slbdtrb0(xm))) | aElementOf0(W0, slbdtrb0(xn))))), inference(lemma,lemma(discharge,[]))).
% 0.53/0.73 tff(185,plain,
% 0.53/0.73 (((~(aSubsetOf0(slbdtrb0(xm), slbdtrb0(xn)) | (~sdtlseqdt0(xm, xn)) | (~aElementOf0(W0!9, slbdtrb0(xm))) | aElementOf0(W0!9, slbdtrb0(xn)) | (~aSet0(slbdtrb0(xn))) | (~aSet0(slbdtrb0(xm))) | (~![W0: $i] : (~(((~aElementOf0(W0, szNzAzT0)) | (~sdtlseqdt0(szszuzczcdt0(W0), xn))) <=> aElementOf0(W0, slbdtrb0(xn))))) | (~![W0: $i] : (~(((~aElementOf0(W0, szNzAzT0)) | (~sdtlseqdt0(szszuzczcdt0(W0), xm))) <=> aElementOf0(W0, slbdtrb0(xm))))))) | (~(sdtlseqdt0(xm, xn) | (~aSubsetOf0(slbdtrb0(xm), slbdtrb0(xn))) | (~aSet0(slbdtrb0(xn))) | (~aSet0(slbdtrb0(xm))) | (~![W0: $i] : (~(((~aElementOf0(W0, szNzAzT0)) | (~sdtlseqdt0(szszuzczcdt0(W0), xn))) <=> aElementOf0(W0, slbdtrb0(xn))))) | (~![W0: $i] : (~(((~aElementOf0(W0, szNzAzT0)) | (~sdtlseqdt0(szszuzczcdt0(W0), xm))) <=> aElementOf0(W0, slbdtrb0(xm))))) | (~![W0: $i] : ((~aElementOf0(W0, slbdtrb0(xm))) | aElementOf0(W0, slbdtrb0(xn))))))) <=> ((~(aSubsetOf0(slbdtrb0(xm), slbdtrb0(xn)) | (~sdtlseqdt0(xm, xn)) | (~aElementOf0(W0!9, slbdtrb0(xm))) | aElementOf0(W0!9, slbdtrb0(xn)) | (~aSet0(slbdtrb0(xn))) | (~aSet0(slbdtrb0(xm))) | (~![W0: $i] : (~(((~aElementOf0(W0, szNzAzT0)) | (~sdtlseqdt0(szszuzczcdt0(W0), xn))) <=> aElementOf0(W0, slbdtrb0(xn))))) | (~![W0: $i] : (~(((~aElementOf0(W0, szNzAzT0)) | (~sdtlseqdt0(szszuzczcdt0(W0), xm))) <=> aElementOf0(W0, slbdtrb0(xm))))))) | (~(sdtlseqdt0(xm, xn) | (~aSubsetOf0(slbdtrb0(xm), slbdtrb0(xn))) | (~aSet0(slbdtrb0(xn))) | (~aSet0(slbdtrb0(xm))) | (~![W0: $i] : (~(((~aElementOf0(W0, szNzAzT0)) | (~sdtlseqdt0(szszuzczcdt0(W0), xn))) <=> aElementOf0(W0, slbdtrb0(xn))))) | (~![W0: $i] : (~(((~aElementOf0(W0, szNzAzT0)) | (~sdtlseqdt0(szszuzczcdt0(W0), xm))) <=> aElementOf0(W0, slbdtrb0(xm))))) | (~![W0: $i] : ((~aElementOf0(W0, slbdtrb0(xm))) | aElementOf0(W0, slbdtrb0(xn)))))))),
% 0.53/0.74 inference(rewrite,[status(thm)],[])).
% 0.53/0.74 tff(186,plain,
% 0.53/0.74 ((~(sdtlseqdt0(xm, xn) | (~aSubsetOf0(slbdtrb0(xm), slbdtrb0(xn))) | (~![W0: $i] : ((~aElementOf0(W0, slbdtrb0(xm))) | aElementOf0(W0, slbdtrb0(xn)))) | (~aSet0(slbdtrb0(xn))) | (~![W0: $i] : (~(((~aElementOf0(W0, szNzAzT0)) | (~sdtlseqdt0(szszuzczcdt0(W0), xn))) <=> aElementOf0(W0, slbdtrb0(xn))))) | (~aSet0(slbdtrb0(xm))) | (~![W0: $i] : (~(((~aElementOf0(W0, szNzAzT0)) | (~sdtlseqdt0(szszuzczcdt0(W0), xm))) <=> aElementOf0(W0, slbdtrb0(xm))))))) <=> (~(sdtlseqdt0(xm, xn) | (~aSubsetOf0(slbdtrb0(xm), slbdtrb0(xn))) | (~aSet0(slbdtrb0(xn))) | (~aSet0(slbdtrb0(xm))) | (~![W0: $i] : (~(((~aElementOf0(W0, szNzAzT0)) | (~sdtlseqdt0(szszuzczcdt0(W0), xn))) <=> aElementOf0(W0, slbdtrb0(xn))))) | (~![W0: $i] : (~(((~aElementOf0(W0, szNzAzT0)) | (~sdtlseqdt0(szszuzczcdt0(W0), xm))) <=> aElementOf0(W0, slbdtrb0(xm))))) | (~![W0: $i] : ((~aElementOf0(W0, slbdtrb0(xm))) | aElementOf0(W0, slbdtrb0(xn))))))),
% 0.53/0.74 inference(rewrite,[status(thm)],[])).
% 0.53/0.74 tff(187,plain,
% 0.53/0.74 ((~(aSubsetOf0(slbdtrb0(xm), slbdtrb0(xn)) | (~sdtlseqdt0(xm, xn)) | (~aElementOf0(W0!9, slbdtrb0(xm))) | aElementOf0(W0!9, slbdtrb0(xn)) | (~aSet0(slbdtrb0(xn))) | (~![W0: $i] : (~(((~aElementOf0(W0, szNzAzT0)) | (~sdtlseqdt0(szszuzczcdt0(W0), xn))) <=> aElementOf0(W0, slbdtrb0(xn))))) | (~aSet0(slbdtrb0(xm))) | (~![W0: $i] : (~(((~aElementOf0(W0, szNzAzT0)) | (~sdtlseqdt0(szszuzczcdt0(W0), xm))) <=> aElementOf0(W0, slbdtrb0(xm))))))) <=> (~(aSubsetOf0(slbdtrb0(xm), slbdtrb0(xn)) | (~sdtlseqdt0(xm, xn)) | (~aElementOf0(W0!9, slbdtrb0(xm))) | aElementOf0(W0!9, slbdtrb0(xn)) | (~aSet0(slbdtrb0(xn))) | (~aSet0(slbdtrb0(xm))) | (~![W0: $i] : (~(((~aElementOf0(W0, szNzAzT0)) | (~sdtlseqdt0(szszuzczcdt0(W0), xn))) <=> aElementOf0(W0, slbdtrb0(xn))))) | (~![W0: $i] : (~(((~aElementOf0(W0, szNzAzT0)) | (~sdtlseqdt0(szszuzczcdt0(W0), xm))) <=> aElementOf0(W0, slbdtrb0(xm)))))))),
% 0.53/0.74 inference(rewrite,[status(thm)],[])).
% 0.53/0.74 tff(188,plain,
% 0.53/0.74 (((~(aSubsetOf0(slbdtrb0(xm), slbdtrb0(xn)) | (~sdtlseqdt0(xm, xn)) | (~aElementOf0(W0!9, slbdtrb0(xm))) | aElementOf0(W0!9, slbdtrb0(xn)) | (~aSet0(slbdtrb0(xn))) | (~![W0: $i] : (~(((~aElementOf0(W0, szNzAzT0)) | (~sdtlseqdt0(szszuzczcdt0(W0), xn))) <=> aElementOf0(W0, slbdtrb0(xn))))) | (~aSet0(slbdtrb0(xm))) | (~![W0: $i] : (~(((~aElementOf0(W0, szNzAzT0)) | (~sdtlseqdt0(szszuzczcdt0(W0), xm))) <=> aElementOf0(W0, slbdtrb0(xm))))))) | (~(sdtlseqdt0(xm, xn) | (~aSubsetOf0(slbdtrb0(xm), slbdtrb0(xn))) | (~![W0: $i] : ((~aElementOf0(W0, slbdtrb0(xm))) | aElementOf0(W0, slbdtrb0(xn)))) | (~aSet0(slbdtrb0(xn))) | (~![W0: $i] : (~(((~aElementOf0(W0, szNzAzT0)) | (~sdtlseqdt0(szszuzczcdt0(W0), xn))) <=> aElementOf0(W0, slbdtrb0(xn))))) | (~aSet0(slbdtrb0(xm))) | (~![W0: $i] : (~(((~aElementOf0(W0, szNzAzT0)) | (~sdtlseqdt0(szszuzczcdt0(W0), xm))) <=> aElementOf0(W0, slbdtrb0(xm)))))))) <=> ((~(aSubsetOf0(slbdtrb0(xm), slbdtrb0(xn)) | (~sdtlseqdt0(xm, xn)) | (~aElementOf0(W0!9, slbdtrb0(xm))) | aElementOf0(W0!9, slbdtrb0(xn)) | (~aSet0(slbdtrb0(xn))) | (~aSet0(slbdtrb0(xm))) | (~![W0: $i] : (~(((~aElementOf0(W0, szNzAzT0)) | (~sdtlseqdt0(szszuzczcdt0(W0), xn))) <=> aElementOf0(W0, slbdtrb0(xn))))) | (~![W0: $i] : (~(((~aElementOf0(W0, szNzAzT0)) | (~sdtlseqdt0(szszuzczcdt0(W0), xm))) <=> aElementOf0(W0, slbdtrb0(xm))))))) | (~(sdtlseqdt0(xm, xn) | (~aSubsetOf0(slbdtrb0(xm), slbdtrb0(xn))) | (~aSet0(slbdtrb0(xn))) | (~aSet0(slbdtrb0(xm))) | (~![W0: $i] : (~(((~aElementOf0(W0, szNzAzT0)) | (~sdtlseqdt0(szszuzczcdt0(W0), xn))) <=> aElementOf0(W0, slbdtrb0(xn))))) | (~![W0: $i] : (~(((~aElementOf0(W0, szNzAzT0)) | (~sdtlseqdt0(szszuzczcdt0(W0), xm))) <=> aElementOf0(W0, slbdtrb0(xm))))) | (~![W0: $i] : ((~aElementOf0(W0, slbdtrb0(xm))) | aElementOf0(W0, slbdtrb0(xn)))))))),
% 0.53/0.74 inference(monotonicity,[status(thm)],[187, 186])).
% 0.53/0.74 tff(189,plain,
% 0.53/0.74 (((~(aSubsetOf0(slbdtrb0(xm), slbdtrb0(xn)) | (~sdtlseqdt0(xm, xn)) | (~aElementOf0(W0!9, slbdtrb0(xm))) | aElementOf0(W0!9, slbdtrb0(xn)) | (~aSet0(slbdtrb0(xn))) | (~![W0: $i] : (~(((~aElementOf0(W0, szNzAzT0)) | (~sdtlseqdt0(szszuzczcdt0(W0), xn))) <=> aElementOf0(W0, slbdtrb0(xn))))) | (~aSet0(slbdtrb0(xm))) | (~![W0: $i] : (~(((~aElementOf0(W0, szNzAzT0)) | (~sdtlseqdt0(szszuzczcdt0(W0), xm))) <=> aElementOf0(W0, slbdtrb0(xm))))))) | (~(sdtlseqdt0(xm, xn) | (~aSubsetOf0(slbdtrb0(xm), slbdtrb0(xn))) | (~![W0: $i] : ((~aElementOf0(W0, slbdtrb0(xm))) | aElementOf0(W0, slbdtrb0(xn)))) | (~aSet0(slbdtrb0(xn))) | (~![W0: $i] : (~(((~aElementOf0(W0, szNzAzT0)) | (~sdtlseqdt0(szszuzczcdt0(W0), xn))) <=> aElementOf0(W0, slbdtrb0(xn))))) | (~aSet0(slbdtrb0(xm))) | (~![W0: $i] : (~(((~aElementOf0(W0, szNzAzT0)) | (~sdtlseqdt0(szszuzczcdt0(W0), xm))) <=> aElementOf0(W0, slbdtrb0(xm)))))))) <=> ((~(aSubsetOf0(slbdtrb0(xm), slbdtrb0(xn)) | (~sdtlseqdt0(xm, xn)) | (~aElementOf0(W0!9, slbdtrb0(xm))) | aElementOf0(W0!9, slbdtrb0(xn)) | (~aSet0(slbdtrb0(xn))) | (~aSet0(slbdtrb0(xm))) | (~![W0: $i] : (~(((~aElementOf0(W0, szNzAzT0)) | (~sdtlseqdt0(szszuzczcdt0(W0), xn))) <=> aElementOf0(W0, slbdtrb0(xn))))) | (~![W0: $i] : (~(((~aElementOf0(W0, szNzAzT0)) | (~sdtlseqdt0(szszuzczcdt0(W0), xm))) <=> aElementOf0(W0, slbdtrb0(xm))))))) | (~(sdtlseqdt0(xm, xn) | (~aSubsetOf0(slbdtrb0(xm), slbdtrb0(xn))) | (~aSet0(slbdtrb0(xn))) | (~aSet0(slbdtrb0(xm))) | (~![W0: $i] : (~(((~aElementOf0(W0, szNzAzT0)) | (~sdtlseqdt0(szszuzczcdt0(W0), xn))) <=> aElementOf0(W0, slbdtrb0(xn))))) | (~![W0: $i] : (~(((~aElementOf0(W0, szNzAzT0)) | (~sdtlseqdt0(szszuzczcdt0(W0), xm))) <=> aElementOf0(W0, slbdtrb0(xm))))) | (~![W0: $i] : ((~aElementOf0(W0, slbdtrb0(xm))) | aElementOf0(W0, slbdtrb0(xn)))))))),
% 0.53/0.74 inference(transitivity,[status(thm)],[188, 185])).
% 0.53/0.74 tff(190,plain,
% 0.53/0.74 (((~(aSubsetOf0(slbdtrb0(xm), slbdtrb0(xn)) | (~sdtlseqdt0(xm, xn)) | (~aElementOf0(W0!9, slbdtrb0(xm))) | aElementOf0(W0!9, slbdtrb0(xn)) | (~aSet0(slbdtrb0(xn))) | (~![W0: $i] : (~(((~aElementOf0(W0, szNzAzT0)) | (~sdtlseqdt0(szszuzczcdt0(W0), xn))) <=> aElementOf0(W0, slbdtrb0(xn))))) | (~aSet0(slbdtrb0(xm))) | (~![W0: $i] : (~(((~aElementOf0(W0, szNzAzT0)) | (~sdtlseqdt0(szszuzczcdt0(W0), xm))) <=> aElementOf0(W0, slbdtrb0(xm))))))) | (~(sdtlseqdt0(xm, xn) | (~aSubsetOf0(slbdtrb0(xm), slbdtrb0(xn))) | (~![W0: $i] : ((~aElementOf0(W0, slbdtrb0(xm))) | aElementOf0(W0, slbdtrb0(xn)))) | (~aSet0(slbdtrb0(xn))) | (~![W0: $i] : (~(((~aElementOf0(W0, szNzAzT0)) | (~sdtlseqdt0(szszuzczcdt0(W0), xn))) <=> aElementOf0(W0, slbdtrb0(xn))))) | (~aSet0(slbdtrb0(xm))) | (~![W0: $i] : (~(((~aElementOf0(W0, szNzAzT0)) | (~sdtlseqdt0(szszuzczcdt0(W0), xm))) <=> aElementOf0(W0, slbdtrb0(xm)))))))) <=> ((~(aSubsetOf0(slbdtrb0(xm), slbdtrb0(xn)) | (~sdtlseqdt0(xm, xn)) | (~aElementOf0(W0!9, slbdtrb0(xm))) | aElementOf0(W0!9, slbdtrb0(xn)) | (~aSet0(slbdtrb0(xn))) | (~![W0: $i] : (~(((~aElementOf0(W0, szNzAzT0)) | (~sdtlseqdt0(szszuzczcdt0(W0), xn))) <=> aElementOf0(W0, slbdtrb0(xn))))) | (~aSet0(slbdtrb0(xm))) | (~![W0: $i] : (~(((~aElementOf0(W0, szNzAzT0)) | (~sdtlseqdt0(szszuzczcdt0(W0), xm))) <=> aElementOf0(W0, slbdtrb0(xm))))))) | (~(sdtlseqdt0(xm, xn) | (~aSubsetOf0(slbdtrb0(xm), slbdtrb0(xn))) | (~![W0: $i] : ((~aElementOf0(W0, slbdtrb0(xm))) | aElementOf0(W0, slbdtrb0(xn)))) | (~aSet0(slbdtrb0(xn))) | (~![W0: $i] : (~(((~aElementOf0(W0, szNzAzT0)) | (~sdtlseqdt0(szszuzczcdt0(W0), xn))) <=> aElementOf0(W0, slbdtrb0(xn))))) | (~aSet0(slbdtrb0(xm))) | (~![W0: $i] : (~(((~aElementOf0(W0, szNzAzT0)) | (~sdtlseqdt0(szszuzczcdt0(W0), xm))) <=> aElementOf0(W0, slbdtrb0(xm))))))))),
% 0.53/0.74 inference(rewrite,[status(thm)],[])).
% 0.53/0.74 tff(191,plain,
% 0.53/0.74 (((~(aSubsetOf0(slbdtrb0(xm), slbdtrb0(xn)) | (~sdtlseqdt0(xm, xn)) | (~aElementOf0(W0!9, slbdtrb0(xm))) | aElementOf0(W0!9, slbdtrb0(xn)) | (~aSet0(slbdtrb0(xn))) | (~![W0: $i] : (~(((~aElementOf0(W0, szNzAzT0)) | (~sdtlseqdt0(szszuzczcdt0(W0), xn))) <=> aElementOf0(W0, slbdtrb0(xn))))) | (~aSet0(slbdtrb0(xm))) | (~![W0: $i] : (~(((~aElementOf0(W0, szNzAzT0)) | (~sdtlseqdt0(szszuzczcdt0(W0), xm))) <=> aElementOf0(W0, slbdtrb0(xm))))))) | (~(sdtlseqdt0(xm, xn) | (~aSubsetOf0(slbdtrb0(xm), slbdtrb0(xn))) | (~![W0: $i] : ((~aElementOf0(W0, slbdtrb0(xm))) | aElementOf0(W0, slbdtrb0(xn)))) | (~aSet0(slbdtrb0(xn))) | (~![W0: $i] : (~(((~aElementOf0(W0, szNzAzT0)) | (~sdtlseqdt0(szszuzczcdt0(W0), xn))) <=> aElementOf0(W0, slbdtrb0(xn))))) | (~aSet0(slbdtrb0(xm))) | (~![W0: $i] : (~(((~aElementOf0(W0, szNzAzT0)) | (~sdtlseqdt0(szszuzczcdt0(W0), xm))) <=> aElementOf0(W0, slbdtrb0(xm)))))))) <=> ((~(aSubsetOf0(slbdtrb0(xm), slbdtrb0(xn)) | (~sdtlseqdt0(xm, xn)) | (~aElementOf0(W0!9, slbdtrb0(xm))) | aElementOf0(W0!9, slbdtrb0(xn)) | (~aSet0(slbdtrb0(xn))) | (~![W0: $i] : (~(((~aElementOf0(W0, szNzAzT0)) | (~sdtlseqdt0(szszuzczcdt0(W0), xn))) <=> aElementOf0(W0, slbdtrb0(xn))))) | (~aSet0(slbdtrb0(xm))) | (~![W0: $i] : (~(((~aElementOf0(W0, szNzAzT0)) | (~sdtlseqdt0(szszuzczcdt0(W0), xm))) <=> aElementOf0(W0, slbdtrb0(xm))))))) | (~(sdtlseqdt0(xm, xn) | (~aSubsetOf0(slbdtrb0(xm), slbdtrb0(xn))) | (~![W0: $i] : ((~aElementOf0(W0, slbdtrb0(xm))) | aElementOf0(W0, slbdtrb0(xn)))) | (~aSet0(slbdtrb0(xn))) | (~![W0: $i] : (~(((~aElementOf0(W0, szNzAzT0)) | (~sdtlseqdt0(szszuzczcdt0(W0), xn))) <=> aElementOf0(W0, slbdtrb0(xn))))) | (~aSet0(slbdtrb0(xm))) | (~![W0: $i] : (~(((~aElementOf0(W0, szNzAzT0)) | (~sdtlseqdt0(szszuzczcdt0(W0), xm))) <=> aElementOf0(W0, slbdtrb0(xm))))))))),
% 0.53/0.74 inference(rewrite,[status(thm)],[])).
% 0.53/0.74 tff(192,plain,
% 0.53/0.74 ((aSet0(slbdtrb0(xm)) & ![W0: $i] : (~(((~aElementOf0(W0, szNzAzT0)) | (~sdtlseqdt0(szszuzczcdt0(W0), xm))) <=> aElementOf0(W0, slbdtrb0(xm)))) & aSet0(slbdtrb0(xn)) & ![W0: $i] : (~(((~aElementOf0(W0, szNzAzT0)) | (~sdtlseqdt0(szszuzczcdt0(W0), xn))) <=> aElementOf0(W0, slbdtrb0(xn)))) & ![W0: $i] : ((~aElementOf0(W0, slbdtrb0(xm))) | aElementOf0(W0, slbdtrb0(xn))) & aSubsetOf0(slbdtrb0(xm), slbdtrb0(xn)) & (~sdtlseqdt0(xm, xn))) <=> (~(sdtlseqdt0(xm, xn) | (~aSubsetOf0(slbdtrb0(xm), slbdtrb0(xn))) | (~![W0: $i] : ((~aElementOf0(W0, slbdtrb0(xm))) | aElementOf0(W0, slbdtrb0(xn)))) | (~aSet0(slbdtrb0(xn))) | (~![W0: $i] : (~(((~aElementOf0(W0, szNzAzT0)) | (~sdtlseqdt0(szszuzczcdt0(W0), xn))) <=> aElementOf0(W0, slbdtrb0(xn))))) | (~aSet0(slbdtrb0(xm))) | (~![W0: $i] : (~(((~aElementOf0(W0, szNzAzT0)) | (~sdtlseqdt0(szszuzczcdt0(W0), xm))) <=> aElementOf0(W0, slbdtrb0(xm)))))))),
% 0.53/0.74 inference(rewrite,[status(thm)],[])).
% 0.53/0.74 tff(193,plain,
% 0.53/0.74 (^[W0: $i] : trans(trans(monotonicity(rewrite((aElementOf0(W0, szNzAzT0) & sdtlseqdt0(szszuzczcdt0(W0), xn)) <=> (~((~aElementOf0(W0, szNzAzT0)) | (~sdtlseqdt0(szszuzczcdt0(W0), xn))))), ((aElementOf0(W0, slbdtrb0(xn)) <=> (aElementOf0(W0, szNzAzT0) & sdtlseqdt0(szszuzczcdt0(W0), xn))) <=> (aElementOf0(W0, slbdtrb0(xn)) <=> (~((~aElementOf0(W0, szNzAzT0)) | (~sdtlseqdt0(szszuzczcdt0(W0), xn))))))), rewrite((aElementOf0(W0, slbdtrb0(xn)) <=> (~((~aElementOf0(W0, szNzAzT0)) | (~sdtlseqdt0(szszuzczcdt0(W0), xn))))) <=> (~(((~aElementOf0(W0, szNzAzT0)) | (~sdtlseqdt0(szszuzczcdt0(W0), xn))) <=> aElementOf0(W0, slbdtrb0(xn))))), ((aElementOf0(W0, slbdtrb0(xn)) <=> (aElementOf0(W0, szNzAzT0) & sdtlseqdt0(szszuzczcdt0(W0), xn))) <=> (~(((~aElementOf0(W0, szNzAzT0)) | (~sdtlseqdt0(szszuzczcdt0(W0), xn))) <=> aElementOf0(W0, slbdtrb0(xn)))))), rewrite((~(((~aElementOf0(W0, szNzAzT0)) | (~sdtlseqdt0(szszuzczcdt0(W0), xn))) <=> aElementOf0(W0, slbdtrb0(xn)))) <=> (~(((~aElementOf0(W0, szNzAzT0)) | (~sdtlseqdt0(szszuzczcdt0(W0), xn))) <=> aElementOf0(W0, slbdtrb0(xn))))), ((aElementOf0(W0, slbdtrb0(xn)) <=> (aElementOf0(W0, szNzAzT0) & sdtlseqdt0(szszuzczcdt0(W0), xn))) <=> (~(((~aElementOf0(W0, szNzAzT0)) | (~sdtlseqdt0(szszuzczcdt0(W0), xn))) <=> aElementOf0(W0, slbdtrb0(xn))))))),
% 0.53/0.74 inference(bind,[status(th)],[])).
% 0.53/0.74 tff(194,plain,
% 0.53/0.74 (![W0: $i] : (aElementOf0(W0, slbdtrb0(xn)) <=> (aElementOf0(W0, szNzAzT0) & sdtlseqdt0(szszuzczcdt0(W0), xn))) <=> ![W0: $i] : (~(((~aElementOf0(W0, szNzAzT0)) | (~sdtlseqdt0(szszuzczcdt0(W0), xn))) <=> aElementOf0(W0, slbdtrb0(xn))))),
% 0.53/0.74 inference(quant_intro,[status(thm)],[193])).
% 0.53/0.74 tff(195,plain,
% 0.53/0.74 (^[W0: $i] : trans(trans(monotonicity(rewrite((aElementOf0(W0, szNzAzT0) & sdtlseqdt0(szszuzczcdt0(W0), xm)) <=> (~((~aElementOf0(W0, szNzAzT0)) | (~sdtlseqdt0(szszuzczcdt0(W0), xm))))), ((aElementOf0(W0, slbdtrb0(xm)) <=> (aElementOf0(W0, szNzAzT0) & sdtlseqdt0(szszuzczcdt0(W0), xm))) <=> (aElementOf0(W0, slbdtrb0(xm)) <=> (~((~aElementOf0(W0, szNzAzT0)) | (~sdtlseqdt0(szszuzczcdt0(W0), xm))))))), rewrite((aElementOf0(W0, slbdtrb0(xm)) <=> (~((~aElementOf0(W0, szNzAzT0)) | (~sdtlseqdt0(szszuzczcdt0(W0), xm))))) <=> (~(((~aElementOf0(W0, szNzAzT0)) | (~sdtlseqdt0(szszuzczcdt0(W0), xm))) <=> aElementOf0(W0, slbdtrb0(xm))))), ((aElementOf0(W0, slbdtrb0(xm)) <=> (aElementOf0(W0, szNzAzT0) & sdtlseqdt0(szszuzczcdt0(W0), xm))) <=> (~(((~aElementOf0(W0, szNzAzT0)) | (~sdtlseqdt0(szszuzczcdt0(W0), xm))) <=> aElementOf0(W0, slbdtrb0(xm)))))), rewrite((~(((~aElementOf0(W0, szNzAzT0)) | (~sdtlseqdt0(szszuzczcdt0(W0), xm))) <=> aElementOf0(W0, slbdtrb0(xm)))) <=> (~(((~aElementOf0(W0, szNzAzT0)) | (~sdtlseqdt0(szszuzczcdt0(W0), xm))) <=> aElementOf0(W0, slbdtrb0(xm))))), ((aElementOf0(W0, slbdtrb0(xm)) <=> (aElementOf0(W0, szNzAzT0) & sdtlseqdt0(szszuzczcdt0(W0), xm))) <=> (~(((~aElementOf0(W0, szNzAzT0)) | (~sdtlseqdt0(szszuzczcdt0(W0), xm))) <=> aElementOf0(W0, slbdtrb0(xm))))))),
% 0.53/0.74 inference(bind,[status(th)],[])).
% 0.53/0.74 tff(196,plain,
% 0.53/0.74 (![W0: $i] : (aElementOf0(W0, slbdtrb0(xm)) <=> (aElementOf0(W0, szNzAzT0) & sdtlseqdt0(szszuzczcdt0(W0), xm))) <=> ![W0: $i] : (~(((~aElementOf0(W0, szNzAzT0)) | (~sdtlseqdt0(szszuzczcdt0(W0), xm))) <=> aElementOf0(W0, slbdtrb0(xm))))),
% 0.53/0.74 inference(quant_intro,[status(thm)],[195])).
% 0.53/0.74 tff(197,plain,
% 0.53/0.74 ((aSet0(slbdtrb0(xm)) & ![W0: $i] : (aElementOf0(W0, slbdtrb0(xm)) <=> (aElementOf0(W0, szNzAzT0) & sdtlseqdt0(szszuzczcdt0(W0), xm))) & aSet0(slbdtrb0(xn)) & ![W0: $i] : (aElementOf0(W0, slbdtrb0(xn)) <=> (aElementOf0(W0, szNzAzT0) & sdtlseqdt0(szszuzczcdt0(W0), xn))) & ![W0: $i] : ((~aElementOf0(W0, slbdtrb0(xm))) | aElementOf0(W0, slbdtrb0(xn))) & aSubsetOf0(slbdtrb0(xm), slbdtrb0(xn)) & (~sdtlseqdt0(xm, xn))) <=> (aSet0(slbdtrb0(xm)) & ![W0: $i] : (~(((~aElementOf0(W0, szNzAzT0)) | (~sdtlseqdt0(szszuzczcdt0(W0), xm))) <=> aElementOf0(W0, slbdtrb0(xm)))) & aSet0(slbdtrb0(xn)) & ![W0: $i] : (~(((~aElementOf0(W0, szNzAzT0)) | (~sdtlseqdt0(szszuzczcdt0(W0), xn))) <=> aElementOf0(W0, slbdtrb0(xn)))) & ![W0: $i] : ((~aElementOf0(W0, slbdtrb0(xm))) | aElementOf0(W0, slbdtrb0(xn))) & aSubsetOf0(slbdtrb0(xm), slbdtrb0(xn)) & (~sdtlseqdt0(xm, xn)))),
% 0.53/0.74 inference(monotonicity,[status(thm)],[196, 194])).
% 0.53/0.74 tff(198,plain,
% 0.53/0.74 ((aSet0(slbdtrb0(xm)) & ![W0: $i] : (aElementOf0(W0, slbdtrb0(xm)) <=> (aElementOf0(W0, szNzAzT0) & sdtlseqdt0(szszuzczcdt0(W0), xm))) & aSet0(slbdtrb0(xn)) & ![W0: $i] : (aElementOf0(W0, slbdtrb0(xn)) <=> (aElementOf0(W0, szNzAzT0) & sdtlseqdt0(szszuzczcdt0(W0), xn))) & ![W0: $i] : ((~aElementOf0(W0, slbdtrb0(xm))) | aElementOf0(W0, slbdtrb0(xn))) & aSubsetOf0(slbdtrb0(xm), slbdtrb0(xn)) & (~sdtlseqdt0(xm, xn))) <=> (~(sdtlseqdt0(xm, xn) | (~aSubsetOf0(slbdtrb0(xm), slbdtrb0(xn))) | (~![W0: $i] : ((~aElementOf0(W0, slbdtrb0(xm))) | aElementOf0(W0, slbdtrb0(xn)))) | (~aSet0(slbdtrb0(xn))) | (~![W0: $i] : (~(((~aElementOf0(W0, szNzAzT0)) | (~sdtlseqdt0(szszuzczcdt0(W0), xn))) <=> aElementOf0(W0, slbdtrb0(xn))))) | (~aSet0(slbdtrb0(xm))) | (~![W0: $i] : (~(((~aElementOf0(W0, szNzAzT0)) | (~sdtlseqdt0(szszuzczcdt0(W0), xm))) <=> aElementOf0(W0, slbdtrb0(xm)))))))),
% 0.53/0.74 inference(transitivity,[status(thm)],[197, 192])).
% 0.53/0.74 tff(199,plain,
% 0.53/0.74 (((~aSubsetOf0(slbdtrb0(xm), slbdtrb0(xn))) & (~((~aElementOf0(W0!9, slbdtrb0(xm))) | aElementOf0(W0!9, slbdtrb0(xn)))) & aSet0(slbdtrb0(xn)) & ![W0: $i] : (~(((~aElementOf0(W0, szNzAzT0)) | (~sdtlseqdt0(szszuzczcdt0(W0), xn))) <=> aElementOf0(W0, slbdtrb0(xn)))) & aSet0(slbdtrb0(xm)) & ![W0: $i] : (~(((~aElementOf0(W0, szNzAzT0)) | (~sdtlseqdt0(szszuzczcdt0(W0), xm))) <=> aElementOf0(W0, slbdtrb0(xm)))) & sdtlseqdt0(xm, xn)) <=> (~(aSubsetOf0(slbdtrb0(xm), slbdtrb0(xn)) | (~sdtlseqdt0(xm, xn)) | (~aElementOf0(W0!9, slbdtrb0(xm))) | aElementOf0(W0!9, slbdtrb0(xn)) | (~aSet0(slbdtrb0(xn))) | (~![W0: $i] : (~(((~aElementOf0(W0, szNzAzT0)) | (~sdtlseqdt0(szszuzczcdt0(W0), xn))) <=> aElementOf0(W0, slbdtrb0(xn))))) | (~aSet0(slbdtrb0(xm))) | (~![W0: $i] : (~(((~aElementOf0(W0, szNzAzT0)) | (~sdtlseqdt0(szszuzczcdt0(W0), xm))) <=> aElementOf0(W0, slbdtrb0(xm)))))))),
% 0.53/0.74 inference(rewrite,[status(thm)],[])).
% 0.53/0.74 tff(200,plain,
% 0.53/0.74 (((~aSubsetOf0(slbdtrb0(xm), slbdtrb0(xn))) & (~((~aElementOf0(W0!9, slbdtrb0(xm))) | aElementOf0(W0!9, slbdtrb0(xn)))) & aSet0(slbdtrb0(xn)) & ![W0: $i] : (aElementOf0(W0, slbdtrb0(xn)) <=> (aElementOf0(W0, szNzAzT0) & sdtlseqdt0(szszuzczcdt0(W0), xn))) & aSet0(slbdtrb0(xm)) & ![W0: $i] : (aElementOf0(W0, slbdtrb0(xm)) <=> (aElementOf0(W0, szNzAzT0) & sdtlseqdt0(szszuzczcdt0(W0), xm))) & sdtlseqdt0(xm, xn)) <=> ((~aSubsetOf0(slbdtrb0(xm), slbdtrb0(xn))) & (~((~aElementOf0(W0!9, slbdtrb0(xm))) | aElementOf0(W0!9, slbdtrb0(xn)))) & aSet0(slbdtrb0(xn)) & ![W0: $i] : (~(((~aElementOf0(W0, szNzAzT0)) | (~sdtlseqdt0(szszuzczcdt0(W0), xn))) <=> aElementOf0(W0, slbdtrb0(xn)))) & aSet0(slbdtrb0(xm)) & ![W0: $i] : (~(((~aElementOf0(W0, szNzAzT0)) | (~sdtlseqdt0(szszuzczcdt0(W0), xm))) <=> aElementOf0(W0, slbdtrb0(xm)))) & sdtlseqdt0(xm, xn))),
% 0.53/0.74 inference(monotonicity,[status(thm)],[194, 196])).
% 0.53/0.74 tff(201,plain,
% 0.53/0.74 (((~aSubsetOf0(slbdtrb0(xm), slbdtrb0(xn))) & (~((~aElementOf0(W0!9, slbdtrb0(xm))) | aElementOf0(W0!9, slbdtrb0(xn)))) & aSet0(slbdtrb0(xn)) & ![W0: $i] : (aElementOf0(W0, slbdtrb0(xn)) <=> (aElementOf0(W0, szNzAzT0) & sdtlseqdt0(szszuzczcdt0(W0), xn))) & aSet0(slbdtrb0(xm)) & ![W0: $i] : (aElementOf0(W0, slbdtrb0(xm)) <=> (aElementOf0(W0, szNzAzT0) & sdtlseqdt0(szszuzczcdt0(W0), xm))) & sdtlseqdt0(xm, xn)) <=> (~(aSubsetOf0(slbdtrb0(xm), slbdtrb0(xn)) | (~sdtlseqdt0(xm, xn)) | (~aElementOf0(W0!9, slbdtrb0(xm))) | aElementOf0(W0!9, slbdtrb0(xn)) | (~aSet0(slbdtrb0(xn))) | (~![W0: $i] : (~(((~aElementOf0(W0, szNzAzT0)) | (~sdtlseqdt0(szszuzczcdt0(W0), xn))) <=> aElementOf0(W0, slbdtrb0(xn))))) | (~aSet0(slbdtrb0(xm))) | (~![W0: $i] : (~(((~aElementOf0(W0, szNzAzT0)) | (~sdtlseqdt0(szszuzczcdt0(W0), xm))) <=> aElementOf0(W0, slbdtrb0(xm)))))))),
% 0.53/0.74 inference(transitivity,[status(thm)],[200, 199])).
% 0.53/0.74 tff(202,plain,
% 0.53/0.74 ((((~aSubsetOf0(slbdtrb0(xm), slbdtrb0(xn))) & (~((~aElementOf0(W0!9, slbdtrb0(xm))) | aElementOf0(W0!9, slbdtrb0(xn)))) & aSet0(slbdtrb0(xn)) & ![W0: $i] : (aElementOf0(W0, slbdtrb0(xn)) <=> (aElementOf0(W0, szNzAzT0) & sdtlseqdt0(szszuzczcdt0(W0), xn))) & aSet0(slbdtrb0(xm)) & ![W0: $i] : (aElementOf0(W0, slbdtrb0(xm)) <=> (aElementOf0(W0, szNzAzT0) & sdtlseqdt0(szszuzczcdt0(W0), xm))) & sdtlseqdt0(xm, xn)) | (aSet0(slbdtrb0(xm)) & ![W0: $i] : (aElementOf0(W0, slbdtrb0(xm)) <=> (aElementOf0(W0, szNzAzT0) & sdtlseqdt0(szszuzczcdt0(W0), xm))) & aSet0(slbdtrb0(xn)) & ![W0: $i] : (aElementOf0(W0, slbdtrb0(xn)) <=> (aElementOf0(W0, szNzAzT0) & sdtlseqdt0(szszuzczcdt0(W0), xn))) & ![W0: $i] : ((~aElementOf0(W0, slbdtrb0(xm))) | aElementOf0(W0, slbdtrb0(xn))) & aSubsetOf0(slbdtrb0(xm), slbdtrb0(xn)) & (~sdtlseqdt0(xm, xn)))) <=> ((~(aSubsetOf0(slbdtrb0(xm), slbdtrb0(xn)) | (~sdtlseqdt0(xm, xn)) | (~aElementOf0(W0!9, slbdtrb0(xm))) | aElementOf0(W0!9, slbdtrb0(xn)) | (~aSet0(slbdtrb0(xn))) | (~![W0: $i] : (~(((~aElementOf0(W0, szNzAzT0)) | (~sdtlseqdt0(szszuzczcdt0(W0), xn))) <=> aElementOf0(W0, slbdtrb0(xn))))) | (~aSet0(slbdtrb0(xm))) | (~![W0: $i] : (~(((~aElementOf0(W0, szNzAzT0)) | (~sdtlseqdt0(szszuzczcdt0(W0), xm))) <=> aElementOf0(W0, slbdtrb0(xm))))))) | (~(sdtlseqdt0(xm, xn) | (~aSubsetOf0(slbdtrb0(xm), slbdtrb0(xn))) | (~![W0: $i] : ((~aElementOf0(W0, slbdtrb0(xm))) | aElementOf0(W0, slbdtrb0(xn)))) | (~aSet0(slbdtrb0(xn))) | (~![W0: $i] : (~(((~aElementOf0(W0, szNzAzT0)) | (~sdtlseqdt0(szszuzczcdt0(W0), xn))) <=> aElementOf0(W0, slbdtrb0(xn))))) | (~aSet0(slbdtrb0(xm))) | (~![W0: $i] : (~(((~aElementOf0(W0, szNzAzT0)) | (~sdtlseqdt0(szszuzczcdt0(W0), xm))) <=> aElementOf0(W0, slbdtrb0(xm))))))))),
% 0.53/0.75 inference(monotonicity,[status(thm)],[201, 198])).
% 0.53/0.75 tff(203,plain,
% 0.53/0.75 ((((~aSubsetOf0(slbdtrb0(xm), slbdtrb0(xn))) & (~((~aElementOf0(W0!9, slbdtrb0(xm))) | aElementOf0(W0!9, slbdtrb0(xn)))) & aSet0(slbdtrb0(xn)) & ![W0: $i] : (aElementOf0(W0, slbdtrb0(xn)) <=> (aElementOf0(W0, szNzAzT0) & sdtlseqdt0(szszuzczcdt0(W0), xn))) & aSet0(slbdtrb0(xm)) & ![W0: $i] : (aElementOf0(W0, slbdtrb0(xm)) <=> (aElementOf0(W0, szNzAzT0) & sdtlseqdt0(szszuzczcdt0(W0), xm))) & sdtlseqdt0(xm, xn)) | (aSet0(slbdtrb0(xm)) & ![W0: $i] : (aElementOf0(W0, slbdtrb0(xm)) <=> (aElementOf0(W0, szNzAzT0) & sdtlseqdt0(szszuzczcdt0(W0), xm))) & aSet0(slbdtrb0(xn)) & ![W0: $i] : (aElementOf0(W0, slbdtrb0(xn)) <=> (aElementOf0(W0, szNzAzT0) & sdtlseqdt0(szszuzczcdt0(W0), xn))) & ![W0: $i] : ((~aElementOf0(W0, slbdtrb0(xm))) | aElementOf0(W0, slbdtrb0(xn))) & aSubsetOf0(slbdtrb0(xm), slbdtrb0(xn)) & (~sdtlseqdt0(xm, xn)))) <=> ((~(aSubsetOf0(slbdtrb0(xm), slbdtrb0(xn)) | (~sdtlseqdt0(xm, xn)) | (~aElementOf0(W0!9, slbdtrb0(xm))) | aElementOf0(W0!9, slbdtrb0(xn)) | (~aSet0(slbdtrb0(xn))) | (~![W0: $i] : (~(((~aElementOf0(W0, szNzAzT0)) | (~sdtlseqdt0(szszuzczcdt0(W0), xn))) <=> aElementOf0(W0, slbdtrb0(xn))))) | (~aSet0(slbdtrb0(xm))) | (~![W0: $i] : (~(((~aElementOf0(W0, szNzAzT0)) | (~sdtlseqdt0(szszuzczcdt0(W0), xm))) <=> aElementOf0(W0, slbdtrb0(xm))))))) | (~(sdtlseqdt0(xm, xn) | (~aSubsetOf0(slbdtrb0(xm), slbdtrb0(xn))) | (~![W0: $i] : ((~aElementOf0(W0, slbdtrb0(xm))) | aElementOf0(W0, slbdtrb0(xn)))) | (~aSet0(slbdtrb0(xn))) | (~![W0: $i] : (~(((~aElementOf0(W0, szNzAzT0)) | (~sdtlseqdt0(szszuzczcdt0(W0), xn))) <=> aElementOf0(W0, slbdtrb0(xn))))) | (~aSet0(slbdtrb0(xm))) | (~![W0: $i] : (~(((~aElementOf0(W0, szNzAzT0)) | (~sdtlseqdt0(szszuzczcdt0(W0), xm))) <=> aElementOf0(W0, slbdtrb0(xm))))))))),
% 0.53/0.75 inference(transitivity,[status(thm)],[202, 191])).
% 0.53/0.75 tff(204,plain,
% 0.53/0.75 ((((~aSubsetOf0(slbdtrb0(xm), slbdtrb0(xn))) & (~((~aElementOf0(W0!9, slbdtrb0(xm))) | aElementOf0(W0!9, slbdtrb0(xn)))) & aSet0(slbdtrb0(xn)) & ![W0: $i] : (aElementOf0(W0, slbdtrb0(xn)) <=> (aElementOf0(W0, szNzAzT0) & sdtlseqdt0(szszuzczcdt0(W0), xn))) & aSet0(slbdtrb0(xm)) & ![W0: $i] : (aElementOf0(W0, slbdtrb0(xm)) <=> (aElementOf0(W0, szNzAzT0) & sdtlseqdt0(szszuzczcdt0(W0), xm))) & sdtlseqdt0(xm, xn)) | (aSet0(slbdtrb0(xm)) & ![W0: $i] : (aElementOf0(W0, slbdtrb0(xm)) <=> (aElementOf0(W0, szNzAzT0) & sdtlseqdt0(szszuzczcdt0(W0), xm))) & aSet0(slbdtrb0(xn)) & ![W0: $i] : (aElementOf0(W0, slbdtrb0(xn)) <=> (aElementOf0(W0, szNzAzT0) & sdtlseqdt0(szszuzczcdt0(W0), xn))) & ![W0: $i] : ((~aElementOf0(W0, slbdtrb0(xm))) | aElementOf0(W0, slbdtrb0(xn))) & aSubsetOf0(slbdtrb0(xm), slbdtrb0(xn)) & (~sdtlseqdt0(xm, xn)))) <=> (((~aSubsetOf0(slbdtrb0(xm), slbdtrb0(xn))) & (~((~aElementOf0(W0!9, slbdtrb0(xm))) | aElementOf0(W0!9, slbdtrb0(xn)))) & aSet0(slbdtrb0(xn)) & ![W0: $i] : (aElementOf0(W0, slbdtrb0(xn)) <=> (aElementOf0(W0, szNzAzT0) & sdtlseqdt0(szszuzczcdt0(W0), xn))) & aSet0(slbdtrb0(xm)) & ![W0: $i] : (aElementOf0(W0, slbdtrb0(xm)) <=> (aElementOf0(W0, szNzAzT0) & sdtlseqdt0(szszuzczcdt0(W0), xm))) & sdtlseqdt0(xm, xn)) | (aSet0(slbdtrb0(xm)) & ![W0: $i] : (aElementOf0(W0, slbdtrb0(xm)) <=> (aElementOf0(W0, szNzAzT0) & sdtlseqdt0(szszuzczcdt0(W0), xm))) & aSet0(slbdtrb0(xn)) & ![W0: $i] : (aElementOf0(W0, slbdtrb0(xn)) <=> (aElementOf0(W0, szNzAzT0) & sdtlseqdt0(szszuzczcdt0(W0), xn))) & ![W0: $i] : ((~aElementOf0(W0, slbdtrb0(xm))) | aElementOf0(W0, slbdtrb0(xn))) & aSubsetOf0(slbdtrb0(xm), slbdtrb0(xn)) & (~sdtlseqdt0(xm, xn))))),
% 0.53/0.75 inference(rewrite,[status(thm)],[])).
% 0.53/0.75 tff(205,plain,
% 0.53/0.75 (((aSet0(slbdtrb0(xm)) & ![W0: $i] : (aElementOf0(W0, slbdtrb0(xm)) <=> (aElementOf0(W0, szNzAzT0) & sdtlseqdt0(szszuzczcdt0(W0), xm))) & aSet0(slbdtrb0(xn)) & ![W0: $i] : (aElementOf0(W0, slbdtrb0(xn)) <=> (aElementOf0(W0, szNzAzT0) & sdtlseqdt0(szszuzczcdt0(W0), xn))) & ![W0: $i] : ((~aElementOf0(W0, slbdtrb0(xm))) | aElementOf0(W0, slbdtrb0(xn))) & aSubsetOf0(slbdtrb0(xm), slbdtrb0(xn))) & (~sdtlseqdt0(xm, xn))) <=> (aSet0(slbdtrb0(xm)) & ![W0: $i] : (aElementOf0(W0, slbdtrb0(xm)) <=> (aElementOf0(W0, szNzAzT0) & sdtlseqdt0(szszuzczcdt0(W0), xm))) & aSet0(slbdtrb0(xn)) & ![W0: $i] : (aElementOf0(W0, slbdtrb0(xn)) <=> (aElementOf0(W0, szNzAzT0) & sdtlseqdt0(szszuzczcdt0(W0), xn))) & ![W0: $i] : ((~aElementOf0(W0, slbdtrb0(xm))) | aElementOf0(W0, slbdtrb0(xn))) & aSubsetOf0(slbdtrb0(xm), slbdtrb0(xn)) & (~sdtlseqdt0(xm, xn)))),
% 0.53/0.75 inference(rewrite,[status(thm)],[])).
% 0.53/0.75 tff(206,plain,
% 0.53/0.75 (((~aSubsetOf0(slbdtrb0(xm), slbdtrb0(xn))) & (~((~aElementOf0(W0!9, slbdtrb0(xm))) | aElementOf0(W0!9, slbdtrb0(xn)))) & (aSet0(slbdtrb0(xn)) & ![W0: $i] : (aElementOf0(W0, slbdtrb0(xn)) <=> (aElementOf0(W0, szNzAzT0) & sdtlseqdt0(szszuzczcdt0(W0), xn)))) & (aSet0(slbdtrb0(xm)) & ![W0: $i] : (aElementOf0(W0, slbdtrb0(xm)) <=> (aElementOf0(W0, szNzAzT0) & sdtlseqdt0(szszuzczcdt0(W0), xm)))) & sdtlseqdt0(xm, xn)) <=> ((~aSubsetOf0(slbdtrb0(xm), slbdtrb0(xn))) & (~((~aElementOf0(W0!9, slbdtrb0(xm))) | aElementOf0(W0!9, slbdtrb0(xn)))) & aSet0(slbdtrb0(xn)) & ![W0: $i] : (aElementOf0(W0, slbdtrb0(xn)) <=> (aElementOf0(W0, szNzAzT0) & sdtlseqdt0(szszuzczcdt0(W0), xn))) & aSet0(slbdtrb0(xm)) & ![W0: $i] : (aElementOf0(W0, slbdtrb0(xm)) <=> (aElementOf0(W0, szNzAzT0) & sdtlseqdt0(szszuzczcdt0(W0), xm))) & sdtlseqdt0(xm, xn))),
% 0.53/0.75 inference(rewrite,[status(thm)],[])).
% 0.53/0.75 tff(207,plain,
% 0.53/0.75 ((aSet0(slbdtrb0(xm)) & ![W0: $i] : (aElementOf0(W0, slbdtrb0(xm)) <=> (aElementOf0(W0, szNzAzT0) & sdtlseqdt0(szszuzczcdt0(W0), xm)))) <=> (aSet0(slbdtrb0(xm)) & ![W0: $i] : (aElementOf0(W0, slbdtrb0(xm)) <=> (aElementOf0(W0, szNzAzT0) & sdtlseqdt0(szszuzczcdt0(W0), xm))))),
% 0.53/0.75 inference(rewrite,[status(thm)],[])).
% 0.53/0.75 tff(208,plain,
% 0.53/0.75 ((aSet0(slbdtrb0(xn)) & ![W0: $i] : (aElementOf0(W0, slbdtrb0(xn)) <=> (aElementOf0(W0, szNzAzT0) & sdtlseqdt0(szszuzczcdt0(W0), xn)))) <=> (aSet0(slbdtrb0(xn)) & ![W0: $i] : (aElementOf0(W0, slbdtrb0(xn)) <=> (aElementOf0(W0, szNzAzT0) & sdtlseqdt0(szszuzczcdt0(W0), xn))))),
% 0.53/0.75 inference(rewrite,[status(thm)],[])).
% 0.53/0.75 tff(209,plain,
% 0.53/0.75 (((~aSubsetOf0(slbdtrb0(xm), slbdtrb0(xn))) & (~((~aElementOf0(W0!9, slbdtrb0(xm))) | aElementOf0(W0!9, slbdtrb0(xn)))) & (aSet0(slbdtrb0(xn)) & ![W0: $i] : (aElementOf0(W0, slbdtrb0(xn)) <=> (aElementOf0(W0, szNzAzT0) & sdtlseqdt0(szszuzczcdt0(W0), xn)))) & (aSet0(slbdtrb0(xm)) & ![W0: $i] : (aElementOf0(W0, slbdtrb0(xm)) <=> (aElementOf0(W0, szNzAzT0) & sdtlseqdt0(szszuzczcdt0(W0), xm)))) & sdtlseqdt0(xm, xn)) <=> ((~aSubsetOf0(slbdtrb0(xm), slbdtrb0(xn))) & (~((~aElementOf0(W0!9, slbdtrb0(xm))) | aElementOf0(W0!9, slbdtrb0(xn)))) & (aSet0(slbdtrb0(xn)) & ![W0: $i] : (aElementOf0(W0, slbdtrb0(xn)) <=> (aElementOf0(W0, szNzAzT0) & sdtlseqdt0(szszuzczcdt0(W0), xn)))) & (aSet0(slbdtrb0(xm)) & ![W0: $i] : (aElementOf0(W0, slbdtrb0(xm)) <=> (aElementOf0(W0, szNzAzT0) & sdtlseqdt0(szszuzczcdt0(W0), xm)))) & sdtlseqdt0(xm, xn))),
% 0.53/0.75 inference(monotonicity,[status(thm)],[208, 207])).
% 0.53/0.75 tff(210,plain,
% 0.53/0.75 (((~aSubsetOf0(slbdtrb0(xm), slbdtrb0(xn))) & (~((~aElementOf0(W0!9, slbdtrb0(xm))) | aElementOf0(W0!9, slbdtrb0(xn)))) & (aSet0(slbdtrb0(xn)) & ![W0: $i] : (aElementOf0(W0, slbdtrb0(xn)) <=> (aElementOf0(W0, szNzAzT0) & sdtlseqdt0(szszuzczcdt0(W0), xn)))) & (aSet0(slbdtrb0(xm)) & ![W0: $i] : (aElementOf0(W0, slbdtrb0(xm)) <=> (aElementOf0(W0, szNzAzT0) & sdtlseqdt0(szszuzczcdt0(W0), xm)))) & sdtlseqdt0(xm, xn)) <=> ((~aSubsetOf0(slbdtrb0(xm), slbdtrb0(xn))) & (~((~aElementOf0(W0!9, slbdtrb0(xm))) | aElementOf0(W0!9, slbdtrb0(xn)))) & aSet0(slbdtrb0(xn)) & ![W0: $i] : (aElementOf0(W0, slbdtrb0(xn)) <=> (aElementOf0(W0, szNzAzT0) & sdtlseqdt0(szszuzczcdt0(W0), xn))) & aSet0(slbdtrb0(xm)) & ![W0: $i] : (aElementOf0(W0, slbdtrb0(xm)) <=> (aElementOf0(W0, szNzAzT0) & sdtlseqdt0(szszuzczcdt0(W0), xm))) & sdtlseqdt0(xm, xn))),
% 0.53/0.75 inference(transitivity,[status(thm)],[209, 206])).
% 0.53/0.75 tff(211,plain,
% 0.53/0.75 ((((~aSubsetOf0(slbdtrb0(xm), slbdtrb0(xn))) & (~((~aElementOf0(W0!9, slbdtrb0(xm))) | aElementOf0(W0!9, slbdtrb0(xn)))) & (aSet0(slbdtrb0(xn)) & ![W0: $i] : (aElementOf0(W0, slbdtrb0(xn)) <=> (aElementOf0(W0, szNzAzT0) & sdtlseqdt0(szszuzczcdt0(W0), xn)))) & (aSet0(slbdtrb0(xm)) & ![W0: $i] : (aElementOf0(W0, slbdtrb0(xm)) <=> (aElementOf0(W0, szNzAzT0) & sdtlseqdt0(szszuzczcdt0(W0), xm)))) & sdtlseqdt0(xm, xn)) | ((aSet0(slbdtrb0(xm)) & ![W0: $i] : (aElementOf0(W0, slbdtrb0(xm)) <=> (aElementOf0(W0, szNzAzT0) & sdtlseqdt0(szszuzczcdt0(W0), xm))) & aSet0(slbdtrb0(xn)) & ![W0: $i] : (aElementOf0(W0, slbdtrb0(xn)) <=> (aElementOf0(W0, szNzAzT0) & sdtlseqdt0(szszuzczcdt0(W0), xn))) & ![W0: $i] : ((~aElementOf0(W0, slbdtrb0(xm))) | aElementOf0(W0, slbdtrb0(xn))) & aSubsetOf0(slbdtrb0(xm), slbdtrb0(xn))) & (~sdtlseqdt0(xm, xn)))) <=> (((~aSubsetOf0(slbdtrb0(xm), slbdtrb0(xn))) & (~((~aElementOf0(W0!9, slbdtrb0(xm))) | aElementOf0(W0!9, slbdtrb0(xn)))) & aSet0(slbdtrb0(xn)) & ![W0: $i] : (aElementOf0(W0, slbdtrb0(xn)) <=> (aElementOf0(W0, szNzAzT0) & sdtlseqdt0(szszuzczcdt0(W0), xn))) & aSet0(slbdtrb0(xm)) & ![W0: $i] : (aElementOf0(W0, slbdtrb0(xm)) <=> (aElementOf0(W0, szNzAzT0) & sdtlseqdt0(szszuzczcdt0(W0), xm))) & sdtlseqdt0(xm, xn)) | (aSet0(slbdtrb0(xm)) & ![W0: $i] : (aElementOf0(W0, slbdtrb0(xm)) <=> (aElementOf0(W0, szNzAzT0) & sdtlseqdt0(szszuzczcdt0(W0), xm))) & aSet0(slbdtrb0(xn)) & ![W0: $i] : (aElementOf0(W0, slbdtrb0(xn)) <=> (aElementOf0(W0, szNzAzT0) & sdtlseqdt0(szszuzczcdt0(W0), xn))) & ![W0: $i] : ((~aElementOf0(W0, slbdtrb0(xm))) | aElementOf0(W0, slbdtrb0(xn))) & aSubsetOf0(slbdtrb0(xm), slbdtrb0(xn)) & (~sdtlseqdt0(xm, xn))))),
% 0.53/0.75 inference(monotonicity,[status(thm)],[210, 205])).
% 0.53/0.75 tff(212,plain,
% 0.53/0.75 ((((~aSubsetOf0(slbdtrb0(xm), slbdtrb0(xn))) & (~((~aElementOf0(W0!9, slbdtrb0(xm))) | aElementOf0(W0!9, slbdtrb0(xn)))) & (aSet0(slbdtrb0(xn)) & ![W0: $i] : (aElementOf0(W0, slbdtrb0(xn)) <=> (aElementOf0(W0, szNzAzT0) & sdtlseqdt0(szszuzczcdt0(W0), xn)))) & (aSet0(slbdtrb0(xm)) & ![W0: $i] : (aElementOf0(W0, slbdtrb0(xm)) <=> (aElementOf0(W0, szNzAzT0) & sdtlseqdt0(szszuzczcdt0(W0), xm)))) & sdtlseqdt0(xm, xn)) | ((aSet0(slbdtrb0(xm)) & ![W0: $i] : (aElementOf0(W0, slbdtrb0(xm)) <=> (aElementOf0(W0, szNzAzT0) & sdtlseqdt0(szszuzczcdt0(W0), xm))) & aSet0(slbdtrb0(xn)) & ![W0: $i] : (aElementOf0(W0, slbdtrb0(xn)) <=> (aElementOf0(W0, szNzAzT0) & sdtlseqdt0(szszuzczcdt0(W0), xn))) & ![W0: $i] : ((~aElementOf0(W0, slbdtrb0(xm))) | aElementOf0(W0, slbdtrb0(xn))) & aSubsetOf0(slbdtrb0(xm), slbdtrb0(xn))) & (~sdtlseqdt0(xm, xn)))) <=> (((~aSubsetOf0(slbdtrb0(xm), slbdtrb0(xn))) & (~((~aElementOf0(W0!9, slbdtrb0(xm))) | aElementOf0(W0!9, slbdtrb0(xn)))) & aSet0(slbdtrb0(xn)) & ![W0: $i] : (aElementOf0(W0, slbdtrb0(xn)) <=> (aElementOf0(W0, szNzAzT0) & sdtlseqdt0(szszuzczcdt0(W0), xn))) & aSet0(slbdtrb0(xm)) & ![W0: $i] : (aElementOf0(W0, slbdtrb0(xm)) <=> (aElementOf0(W0, szNzAzT0) & sdtlseqdt0(szszuzczcdt0(W0), xm))) & sdtlseqdt0(xm, xn)) | (aSet0(slbdtrb0(xm)) & ![W0: $i] : (aElementOf0(W0, slbdtrb0(xm)) <=> (aElementOf0(W0, szNzAzT0) & sdtlseqdt0(szszuzczcdt0(W0), xm))) & aSet0(slbdtrb0(xn)) & ![W0: $i] : (aElementOf0(W0, slbdtrb0(xn)) <=> (aElementOf0(W0, szNzAzT0) & sdtlseqdt0(szszuzczcdt0(W0), xn))) & ![W0: $i] : ((~aElementOf0(W0, slbdtrb0(xm))) | aElementOf0(W0, slbdtrb0(xn))) & aSubsetOf0(slbdtrb0(xm), slbdtrb0(xn)) & (~sdtlseqdt0(xm, xn))))),
% 0.53/0.75 inference(transitivity,[status(thm)],[211, 204])).
% 0.53/0.75 tff(213,plain,
% 0.53/0.75 (((aSubsetOf0(slbdtrb0(xm), slbdtrb0(xn)) | ![W0: $i] : ((~aElementOf0(W0, slbdtrb0(xm))) | aElementOf0(W0, slbdtrb0(xn))) | (~(aSet0(slbdtrb0(xn)) & ![W0: $i] : (aElementOf0(W0, slbdtrb0(xn)) <=> (aElementOf0(W0, szNzAzT0) & sdtlseqdt0(szszuzczcdt0(W0), xn))))) | (~(aSet0(slbdtrb0(xm)) & ![W0: $i] : (aElementOf0(W0, slbdtrb0(xm)) <=> (aElementOf0(W0, szNzAzT0) & sdtlseqdt0(szszuzczcdt0(W0), xm))))) | (~sdtlseqdt0(xm, xn))) & ((~(aSet0(slbdtrb0(xm)) & ![W0: $i] : (aElementOf0(W0, slbdtrb0(xm)) <=> (aElementOf0(W0, szNzAzT0) & sdtlseqdt0(szszuzczcdt0(W0), xm))) & aSet0(slbdtrb0(xn)) & ![W0: $i] : (aElementOf0(W0, slbdtrb0(xn)) <=> (aElementOf0(W0, szNzAzT0) & sdtlseqdt0(szszuzczcdt0(W0), xn))) & ![W0: $i] : ((~aElementOf0(W0, slbdtrb0(xm))) | aElementOf0(W0, slbdtrb0(xn))) & aSubsetOf0(slbdtrb0(xm), slbdtrb0(xn)))) | sdtlseqdt0(xm, xn))) <=> ((aSubsetOf0(slbdtrb0(xm), slbdtrb0(xn)) | ![W0: $i] : ((~aElementOf0(W0, slbdtrb0(xm))) | aElementOf0(W0, slbdtrb0(xn))) | (~(aSet0(slbdtrb0(xn)) & ![W0: $i] : (aElementOf0(W0, slbdtrb0(xn)) <=> (aElementOf0(W0, szNzAzT0) & sdtlseqdt0(szszuzczcdt0(W0), xn))))) | (~(aSet0(slbdtrb0(xm)) & ![W0: $i] : (aElementOf0(W0, slbdtrb0(xm)) <=> (aElementOf0(W0, szNzAzT0) & sdtlseqdt0(szszuzczcdt0(W0), xm))))) | (~sdtlseqdt0(xm, xn))) & ((~(aSet0(slbdtrb0(xm)) & ![W0: $i] : (aElementOf0(W0, slbdtrb0(xm)) <=> (aElementOf0(W0, szNzAzT0) & sdtlseqdt0(szszuzczcdt0(W0), xm))) & aSet0(slbdtrb0(xn)) & ![W0: $i] : (aElementOf0(W0, slbdtrb0(xn)) <=> (aElementOf0(W0, szNzAzT0) & sdtlseqdt0(szszuzczcdt0(W0), xn))) & ![W0: $i] : ((~aElementOf0(W0, slbdtrb0(xm))) | aElementOf0(W0, slbdtrb0(xn))) & aSubsetOf0(slbdtrb0(xm), slbdtrb0(xn)))) | sdtlseqdt0(xm, xn)))),
% 0.59/0.75 inference(rewrite,[status(thm)],[])).
% 0.59/0.75 tff(214,plain,
% 0.59/0.75 ((~((aSubsetOf0(slbdtrb0(xm), slbdtrb0(xn)) | ![W0: $i] : ((~aElementOf0(W0, slbdtrb0(xm))) | aElementOf0(W0, slbdtrb0(xn))) | (~(aSet0(slbdtrb0(xn)) & ![W0: $i] : (aElementOf0(W0, slbdtrb0(xn)) <=> (aElementOf0(W0, szNzAzT0) & sdtlseqdt0(szszuzczcdt0(W0), xn))))) | (~(aSet0(slbdtrb0(xm)) & ![W0: $i] : (aElementOf0(W0, slbdtrb0(xm)) <=> (aElementOf0(W0, szNzAzT0) & sdtlseqdt0(szszuzczcdt0(W0), xm))))) | (~sdtlseqdt0(xm, xn))) & ((~(aSet0(slbdtrb0(xm)) & ![W0: $i] : (aElementOf0(W0, slbdtrb0(xm)) <=> (aElementOf0(W0, szNzAzT0) & sdtlseqdt0(szszuzczcdt0(W0), xm))) & aSet0(slbdtrb0(xn)) & ![W0: $i] : (aElementOf0(W0, slbdtrb0(xn)) <=> (aElementOf0(W0, szNzAzT0) & sdtlseqdt0(szszuzczcdt0(W0), xn))) & ![W0: $i] : ((~aElementOf0(W0, slbdtrb0(xm))) | aElementOf0(W0, slbdtrb0(xn))) & aSubsetOf0(slbdtrb0(xm), slbdtrb0(xn)))) | sdtlseqdt0(xm, xn)))) <=> (~((aSubsetOf0(slbdtrb0(xm), slbdtrb0(xn)) | ![W0: $i] : ((~aElementOf0(W0, slbdtrb0(xm))) | aElementOf0(W0, slbdtrb0(xn))) | (~(aSet0(slbdtrb0(xn)) & ![W0: $i] : (aElementOf0(W0, slbdtrb0(xn)) <=> (aElementOf0(W0, szNzAzT0) & sdtlseqdt0(szszuzczcdt0(W0), xn))))) | (~(aSet0(slbdtrb0(xm)) & ![W0: $i] : (aElementOf0(W0, slbdtrb0(xm)) <=> (aElementOf0(W0, szNzAzT0) & sdtlseqdt0(szszuzczcdt0(W0), xm))))) | (~sdtlseqdt0(xm, xn))) & ((~(aSet0(slbdtrb0(xm)) & ![W0: $i] : (aElementOf0(W0, slbdtrb0(xm)) <=> (aElementOf0(W0, szNzAzT0) & sdtlseqdt0(szszuzczcdt0(W0), xm))) & aSet0(slbdtrb0(xn)) & ![W0: $i] : (aElementOf0(W0, slbdtrb0(xn)) <=> (aElementOf0(W0, szNzAzT0) & sdtlseqdt0(szszuzczcdt0(W0), xn))) & ![W0: $i] : ((~aElementOf0(W0, slbdtrb0(xm))) | aElementOf0(W0, slbdtrb0(xn))) & aSubsetOf0(slbdtrb0(xm), slbdtrb0(xn)))) | sdtlseqdt0(xm, xn))))),
% 0.59/0.75 inference(monotonicity,[status(thm)],[213])).
% 0.59/0.75 tff(215,plain,
% 0.59/0.75 ((~((aSubsetOf0(slbdtrb0(xm), slbdtrb0(xn)) | ![W0: $i] : ((~aElementOf0(W0, slbdtrb0(xm))) | aElementOf0(W0, slbdtrb0(xn))) | (~(aSet0(slbdtrb0(xn)) & ![W0: $i] : (aElementOf0(W0, slbdtrb0(xn)) <=> (aElementOf0(W0, szNzAzT0) & sdtlseqdt0(szszuzczcdt0(W0), xn))))) | (~(aSet0(slbdtrb0(xm)) & ![W0: $i] : (aElementOf0(W0, slbdtrb0(xm)) <=> (aElementOf0(W0, szNzAzT0) & sdtlseqdt0(szszuzczcdt0(W0), xm))))) | (~sdtlseqdt0(xm, xn))) & ((~(aSet0(slbdtrb0(xm)) & ![W0: $i] : (aElementOf0(W0, slbdtrb0(xm)) <=> (aElementOf0(W0, szNzAzT0) & sdtlseqdt0(szszuzczcdt0(W0), xm))) & aSet0(slbdtrb0(xn)) & ![W0: $i] : (aElementOf0(W0, slbdtrb0(xn)) <=> (aElementOf0(W0, szNzAzT0) & sdtlseqdt0(szszuzczcdt0(W0), xn))) & ![W0: $i] : ((~aElementOf0(W0, slbdtrb0(xm))) | aElementOf0(W0, slbdtrb0(xn))) & aSubsetOf0(slbdtrb0(xm), slbdtrb0(xn)))) | sdtlseqdt0(xm, xn)))) <=> (~((aSubsetOf0(slbdtrb0(xm), slbdtrb0(xn)) | ![W0: $i] : ((~aElementOf0(W0, slbdtrb0(xm))) | aElementOf0(W0, slbdtrb0(xn))) | (~(aSet0(slbdtrb0(xn)) & ![W0: $i] : (aElementOf0(W0, slbdtrb0(xn)) <=> (aElementOf0(W0, szNzAzT0) & sdtlseqdt0(szszuzczcdt0(W0), xn))))) | (~(aSet0(slbdtrb0(xm)) & ![W0: $i] : (aElementOf0(W0, slbdtrb0(xm)) <=> (aElementOf0(W0, szNzAzT0) & sdtlseqdt0(szszuzczcdt0(W0), xm))))) | (~sdtlseqdt0(xm, xn))) & ((~(aSet0(slbdtrb0(xm)) & ![W0: $i] : (aElementOf0(W0, slbdtrb0(xm)) <=> (aElementOf0(W0, szNzAzT0) & sdtlseqdt0(szszuzczcdt0(W0), xm))) & aSet0(slbdtrb0(xn)) & ![W0: $i] : (aElementOf0(W0, slbdtrb0(xn)) <=> (aElementOf0(W0, szNzAzT0) & sdtlseqdt0(szszuzczcdt0(W0), xn))) & ![W0: $i] : ((~aElementOf0(W0, slbdtrb0(xm))) | aElementOf0(W0, slbdtrb0(xn))) & aSubsetOf0(slbdtrb0(xm), slbdtrb0(xn)))) | sdtlseqdt0(xm, xn))))),
% 0.59/0.75 inference(rewrite,[status(thm)],[])).
% 0.59/0.75 tff(216,plain,
% 0.59/0.75 ((~((sdtlseqdt0(xm, xn) => ((aSet0(slbdtrb0(xm)) & ![W0: $i] : (aElementOf0(W0, slbdtrb0(xm)) <=> (aElementOf0(W0, szNzAzT0) & sdtlseqdt0(szszuzczcdt0(W0), xm)))) => ((aSet0(slbdtrb0(xn)) & ![W0: $i] : (aElementOf0(W0, slbdtrb0(xn)) <=> (aElementOf0(W0, szNzAzT0) & sdtlseqdt0(szszuzczcdt0(W0), xn)))) => (![W0: $i] : (aElementOf0(W0, slbdtrb0(xm)) => aElementOf0(W0, slbdtrb0(xn))) | aSubsetOf0(slbdtrb0(xm), slbdtrb0(xn)))))) & ((((((aSet0(slbdtrb0(xm)) & ![W0: $i] : (aElementOf0(W0, slbdtrb0(xm)) <=> (aElementOf0(W0, szNzAzT0) & sdtlseqdt0(szszuzczcdt0(W0), xm)))) & aSet0(slbdtrb0(xn))) & ![W0: $i] : (aElementOf0(W0, slbdtrb0(xn)) <=> (aElementOf0(W0, szNzAzT0) & sdtlseqdt0(szszuzczcdt0(W0), xn)))) & ![W0: $i] : (aElementOf0(W0, slbdtrb0(xm)) => aElementOf0(W0, slbdtrb0(xn)))) & aSubsetOf0(slbdtrb0(xm), slbdtrb0(xn))) => sdtlseqdt0(xm, xn)))) <=> (~((aSubsetOf0(slbdtrb0(xm), slbdtrb0(xn)) | ![W0: $i] : ((~aElementOf0(W0, slbdtrb0(xm))) | aElementOf0(W0, slbdtrb0(xn))) | (~(aSet0(slbdtrb0(xn)) & ![W0: $i] : (aElementOf0(W0, slbdtrb0(xn)) <=> (aElementOf0(W0, szNzAzT0) & sdtlseqdt0(szszuzczcdt0(W0), xn))))) | (~(aSet0(slbdtrb0(xm)) & ![W0: $i] : (aElementOf0(W0, slbdtrb0(xm)) <=> (aElementOf0(W0, szNzAzT0) & sdtlseqdt0(szszuzczcdt0(W0), xm))))) | (~sdtlseqdt0(xm, xn))) & ((~(aSet0(slbdtrb0(xm)) & ![W0: $i] : (aElementOf0(W0, slbdtrb0(xm)) <=> (aElementOf0(W0, szNzAzT0) & sdtlseqdt0(szszuzczcdt0(W0), xm))) & aSet0(slbdtrb0(xn)) & ![W0: $i] : (aElementOf0(W0, slbdtrb0(xn)) <=> (aElementOf0(W0, szNzAzT0) & sdtlseqdt0(szszuzczcdt0(W0), xn))) & ![W0: $i] : ((~aElementOf0(W0, slbdtrb0(xm))) | aElementOf0(W0, slbdtrb0(xn))) & aSubsetOf0(slbdtrb0(xm), slbdtrb0(xn)))) | sdtlseqdt0(xm, xn))))),
% 0.59/0.75 inference(rewrite,[status(thm)],[])).
% 0.59/0.75 tff(217,axiom,(~((sdtlseqdt0(xm, xn) => ((aSet0(slbdtrb0(xm)) & ![W0: $i] : (aElementOf0(W0, slbdtrb0(xm)) <=> (aElementOf0(W0, szNzAzT0) & sdtlseqdt0(szszuzczcdt0(W0), xm)))) => ((aSet0(slbdtrb0(xn)) & ![W0: $i] : (aElementOf0(W0, slbdtrb0(xn)) <=> (aElementOf0(W0, szNzAzT0) & sdtlseqdt0(szszuzczcdt0(W0), xn)))) => (![W0: $i] : (aElementOf0(W0, slbdtrb0(xm)) => aElementOf0(W0, slbdtrb0(xn))) | aSubsetOf0(slbdtrb0(xm), slbdtrb0(xn)))))) & ((((((aSet0(slbdtrb0(xm)) & ![W0: $i] : (aElementOf0(W0, slbdtrb0(xm)) <=> (aElementOf0(W0, szNzAzT0) & sdtlseqdt0(szszuzczcdt0(W0), xm)))) & aSet0(slbdtrb0(xn))) & ![W0: $i] : (aElementOf0(W0, slbdtrb0(xn)) <=> (aElementOf0(W0, szNzAzT0) & sdtlseqdt0(szszuzczcdt0(W0), xn)))) & ![W0: $i] : (aElementOf0(W0, slbdtrb0(xm)) => aElementOf0(W0, slbdtrb0(xn)))) & aSubsetOf0(slbdtrb0(xm), slbdtrb0(xn))) => sdtlseqdt0(xm, xn)))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','m__')).
% 0.59/0.75 tff(218,plain,
% 0.59/0.75 (~((aSubsetOf0(slbdtrb0(xm), slbdtrb0(xn)) | ![W0: $i] : ((~aElementOf0(W0, slbdtrb0(xm))) | aElementOf0(W0, slbdtrb0(xn))) | (~(aSet0(slbdtrb0(xn)) & ![W0: $i] : (aElementOf0(W0, slbdtrb0(xn)) <=> (aElementOf0(W0, szNzAzT0) & sdtlseqdt0(szszuzczcdt0(W0), xn))))) | (~(aSet0(slbdtrb0(xm)) & ![W0: $i] : (aElementOf0(W0, slbdtrb0(xm)) <=> (aElementOf0(W0, szNzAzT0) & sdtlseqdt0(szszuzczcdt0(W0), xm))))) | (~sdtlseqdt0(xm, xn))) & ((~(aSet0(slbdtrb0(xm)) & ![W0: $i] : (aElementOf0(W0, slbdtrb0(xm)) <=> (aElementOf0(W0, szNzAzT0) & sdtlseqdt0(szszuzczcdt0(W0), xm))) & aSet0(slbdtrb0(xn)) & ![W0: $i] : (aElementOf0(W0, slbdtrb0(xn)) <=> (aElementOf0(W0, szNzAzT0) & sdtlseqdt0(szszuzczcdt0(W0), xn))) & ![W0: $i] : ((~aElementOf0(W0, slbdtrb0(xm))) | aElementOf0(W0, slbdtrb0(xn))) & aSubsetOf0(slbdtrb0(xm), slbdtrb0(xn)))) | sdtlseqdt0(xm, xn)))),
% 0.59/0.75 inference(modus_ponens,[status(thm)],[217, 216])).
% 0.60/0.76 tff(219,plain,
% 0.60/0.76 (~((aSubsetOf0(slbdtrb0(xm), slbdtrb0(xn)) | ![W0: $i] : ((~aElementOf0(W0, slbdtrb0(xm))) | aElementOf0(W0, slbdtrb0(xn))) | (~(aSet0(slbdtrb0(xn)) & ![W0: $i] : (aElementOf0(W0, slbdtrb0(xn)) <=> (aElementOf0(W0, szNzAzT0) & sdtlseqdt0(szszuzczcdt0(W0), xn))))) | (~(aSet0(slbdtrb0(xm)) & ![W0: $i] : (aElementOf0(W0, slbdtrb0(xm)) <=> (aElementOf0(W0, szNzAzT0) & sdtlseqdt0(szszuzczcdt0(W0), xm))))) | (~sdtlseqdt0(xm, xn))) & ((~(aSet0(slbdtrb0(xm)) & ![W0: $i] : (aElementOf0(W0, slbdtrb0(xm)) <=> (aElementOf0(W0, szNzAzT0) & sdtlseqdt0(szszuzczcdt0(W0), xm))) & aSet0(slbdtrb0(xn)) & ![W0: $i] : (aElementOf0(W0, slbdtrb0(xn)) <=> (aElementOf0(W0, szNzAzT0) & sdtlseqdt0(szszuzczcdt0(W0), xn))) & ![W0: $i] : ((~aElementOf0(W0, slbdtrb0(xm))) | aElementOf0(W0, slbdtrb0(xn))) & aSubsetOf0(slbdtrb0(xm), slbdtrb0(xn)))) | sdtlseqdt0(xm, xn)))),
% 0.60/0.76 inference(modus_ponens,[status(thm)],[218, 214])).
% 0.60/0.76 tff(220,plain,
% 0.60/0.76 (~((aSubsetOf0(slbdtrb0(xm), slbdtrb0(xn)) | ![W0: $i] : ((~aElementOf0(W0, slbdtrb0(xm))) | aElementOf0(W0, slbdtrb0(xn))) | (~(aSet0(slbdtrb0(xn)) & ![W0: $i] : (aElementOf0(W0, slbdtrb0(xn)) <=> (aElementOf0(W0, szNzAzT0) & sdtlseqdt0(szszuzczcdt0(W0), xn))))) | (~(aSet0(slbdtrb0(xm)) & ![W0: $i] : (aElementOf0(W0, slbdtrb0(xm)) <=> (aElementOf0(W0, szNzAzT0) & sdtlseqdt0(szszuzczcdt0(W0), xm))))) | (~sdtlseqdt0(xm, xn))) & ((~(aSet0(slbdtrb0(xm)) & ![W0: $i] : (aElementOf0(W0, slbdtrb0(xm)) <=> (aElementOf0(W0, szNzAzT0) & sdtlseqdt0(szszuzczcdt0(W0), xm))) & aSet0(slbdtrb0(xn)) & ![W0: $i] : (aElementOf0(W0, slbdtrb0(xn)) <=> (aElementOf0(W0, szNzAzT0) & sdtlseqdt0(szszuzczcdt0(W0), xn))) & ![W0: $i] : ((~aElementOf0(W0, slbdtrb0(xm))) | aElementOf0(W0, slbdtrb0(xn))) & aSubsetOf0(slbdtrb0(xm), slbdtrb0(xn)))) | sdtlseqdt0(xm, xn)))),
% 0.60/0.76 inference(modus_ponens,[status(thm)],[219, 215])).
% 0.60/0.76 tff(221,plain,
% 0.60/0.76 (~((aSubsetOf0(slbdtrb0(xm), slbdtrb0(xn)) | ![W0: $i] : ((~aElementOf0(W0, slbdtrb0(xm))) | aElementOf0(W0, slbdtrb0(xn))) | (~(aSet0(slbdtrb0(xn)) & ![W0: $i] : (aElementOf0(W0, slbdtrb0(xn)) <=> (aElementOf0(W0, szNzAzT0) & sdtlseqdt0(szszuzczcdt0(W0), xn))))) | (~(aSet0(slbdtrb0(xm)) & ![W0: $i] : (aElementOf0(W0, slbdtrb0(xm)) <=> (aElementOf0(W0, szNzAzT0) & sdtlseqdt0(szszuzczcdt0(W0), xm))))) | (~sdtlseqdt0(xm, xn))) & ((~(aSet0(slbdtrb0(xm)) & ![W0: $i] : (aElementOf0(W0, slbdtrb0(xm)) <=> (aElementOf0(W0, szNzAzT0) & sdtlseqdt0(szszuzczcdt0(W0), xm))) & aSet0(slbdtrb0(xn)) & ![W0: $i] : (aElementOf0(W0, slbdtrb0(xn)) <=> (aElementOf0(W0, szNzAzT0) & sdtlseqdt0(szszuzczcdt0(W0), xn))) & ![W0: $i] : ((~aElementOf0(W0, slbdtrb0(xm))) | aElementOf0(W0, slbdtrb0(xn))) & aSubsetOf0(slbdtrb0(xm), slbdtrb0(xn)))) | sdtlseqdt0(xm, xn)))),
% 0.60/0.76 inference(modus_ponens,[status(thm)],[220, 214])).
% 0.60/0.76 unexpected number of arguments: (let ((a!1 (~ (not (aSubsetOf0 (slbdtrb0 xm) (slbdtrb0 xn)))
% 0.60/0.76 (not (aSubsetOf0 (slbdtrb0 xm) (slbdtrb0 xn)))))
% 0.60/0.76 (a!2 (forall ((W0 $i))
% 0.60/0.76 (or (not (aElementOf0 W0 (slbdtrb0 xm)))
% 0.60/0.76 (aElementOf0 W0 (slbdtrb0 xn)))))
% 0.60/0.76 (a!3 (or (not (aElementOf0 W0!9 (slbdtrb0 xm)))
% 0.60/0.76 (aElementOf0 W0!9 (slbdtrb0 xn))))
% 0.60/0.76 (a!4 (refl (~ (aSet0 (slbdtrb0 xn)) (aSet0 (slbdtrb0 xn)))))
% 0.60/0.76 (a!5 (proof-bind (lambda ((W0 $i))
% 0.60/0.76 (let ((a!1 (= (aElementOf0 W0 (slbdtrb0 xn))
% 0.60/0.76 (and (aElementOf0 W0 szNzAzT0)
% 0.60/0.76 (sdtlseqdt0 (szszuzczcdt0 W0) xn)))))
% 0.60/0.76 (refl (~ a!1 a!1))))))
% 0.60/0.76 (a!6 (forall ((W0 $i))
% 0.60/0.76 (= (aElementOf0 W0 (slbdtrb0 xn))
% 0.60/0.76 (and (aElementOf0 W0 szNzAzT0)
% 0.60/0.76 (sdtlseqdt0 (szszuzczcdt0 W0) xn)))))
% 0.60/0.76 (a!11 (refl (~ (aSet0 (slbdtrb0 xm)) (aSet0 (slbdtrb0 xm)))))
% 0.60/0.76 (a!12 (proof-bind (lambda ((W0 $i))
% 0.60/0.76 (let ((a!1 (= (aElementOf0 W0 (slbdtrb0 xm))
% 0.60/0.76 (and (aElementOf0 W0 szNzAzT0)
% 0.60/0.76 (sdtlseqdt0 (szszuzczcdt0 W0) xm)))))
% 0.60/0.76 (refl (~ a!1 a!1))))))
% 0.60/0.76 (a!13 (forall ((W0 $i))
% 0.60/0.76 (= (aElementOf0 W0 (slbdtrb0 xm))
% 0.60/0.76 (and (aElementOf0 W0 szNzAzT0)
% 0.60/0.76 (sdtlseqdt0 (szszuzczcdt0 W0) xm)))))
% 0.60/0.76 (a!21 (proof-bind (lambda ((W0 $i))
% 0.60/0.76 (let ((a!1 (or (not (aElementOf0 W0 (slbdtrb0 xm)))
% 0.60/0.76 (aElementOf0 W0 (slbdtrb0 xn)))))
% 0.60/0.76 (refl (~ a!1 a!1))))))
% 0.60/0.76 (a!22 (refl (~ (aSubsetOf0 (slbdtrb0 xm) (slbdtrb0 xn))
% 0.60/0.76 (aSubsetOf0 (slbdtrb0 xm) (slbdtrb0 xn)))))
% 0.60/0.76 (a!25 (refl (~ (not (sdtlseqdt0 xm xn)) (not (sdtlseqdt0 xm xn))))))
% 0.60/0.76 (let ((a!7 (~ (and (aSet0 (slbdtrb0 xn)) a!6) (and (aSet0 (slbdtrb0 xn)) a!6)))
% 0.60/0.76 (a!8 (not (and (aSet0 (slbdtrb0 xn)) a!6)))
% 0.60/0.76 (a!14 (~ (and (aSet0 (slbdtrb0 xm)) a!13)
% 0.60/0.76 (and (aSet0 (slbdtrb0 xm)) a!13)))
% 0.60/0.76 (a!15 (not (and (aSet0 (slbdtrb0 xm)) a!13)))
% 0.60/0.76 (a!19 (and (not (aSubsetOf0 (slbdtrb0 xm) (slbdtrb0 xn)))
% 0.60/0.76 (not a!3)
% 0.60/0.76 (and (aSet0 (slbdtrb0 xn)) a!6)
% 0.60/0.76 (and (aSet0 (slbdtrb0 xm)) a!13)
% 0.60/0.76 (sdtlseqdt0 xm xn)))
% 0.60/0.76 (a!23 (and (aSet0 (slbdtrb0 xm))
% 0.60/0.76 a!13
% 0.60/0.76 (aSet0 (slbdtrb0 xn))
% 0.60/0.76 a!6
% 0.60/0.76 a!2
% 0.60/0.76 (aSubsetOf0 (slbdtrb0 xm) (slbdtrb0 xn)))))
% 0.60/0.76 (let ((a!9 (~ (not a!8) (and (aSet0 (slbdtrb0 xn)) a!6)))
% 0.60/0.76 (a!16 (~ (not a!15) (and (aSet0 (slbdtrb0 xm)) a!13)))
% 0.60/0.76 (a!18 (or (aSubsetOf0 (slbdtrb0 xm) (slbdtrb0 xn))
% 0.60/0.76 a!2
% 0.60/0.76 a!8
% 0.60/0.76 a!15
% 0.60/0.76 (not (sdtlseqdt0 xm xn))))
% 0.60/0.76 (a!24 (nnf-neg (monotonicity a!11
% 0.60/0.76 (nnf-pos a!12 (~ a!13 a!13))
% 0.60/0.76 a!4
% 0.60/0.76 (nnf-pos a!5 (~ a!6 a!6))
% 0.60/0.76 (nnf-pos a!21 (~ a!2 a!2))
% 0.60/0.76 a!22
% 0.60/0.76 (~ a!23 a!23))
% 0.60/0.76 (~ (not (not a!23)) a!23)))
% 0.60/0.76 (a!26 (~ (not (or (not a!23) (sdtlseqdt0 xm xn)))
% 0.60/0.76 (and a!23 (not (sdtlseqdt0 xm xn)))))
% 0.60/0.76 (a!28 (or a!19 (and a!23 (not (sdtlseqdt0 xm xn))))))
% 0.60/0.76 (let ((a!10 (nnf-neg (monotonicity a!4 (nnf-pos a!5 (~ a!6 a!6)) a!7) a!9))
% 0.60/0.76 (a!17 (nnf-neg (monotonicity a!11 (nnf-pos a!12 (~ a!13 a!13)) a!14) a!16))
% 0.60/0.76 (a!27 (not (and a!18 (or (not a!23) (sdtlseqdt0 xm xn))))))
% 0.60/0.76 (let ((a!20 (nnf-neg (refl a!1)
% 0.60/0.76 (sk (~ (not a!2) (not a!3)))
% 0.60/0.76 a!10
% 0.60/0.76 a!17
% 0.60/0.76 (refl (~ (sdtlseqdt0 xm xn) (sdtlseqdt0 xm xn)))
% 0.60/0.76 (~ (not a!18) a!19))))
% 0.60/0.76 (nnf-neg a!20 (nnf-neg a!24 a!25 a!26) (~ a!27 a!28)))))))
% 0.60/0.76 Proof display could not be completed: unexpected number of arguments
% 0.60/0.77 % E exiting
%------------------------------------------------------------------------------