%------------------------------------------------------------------------------
% File : Z3---4.15.1
% Problem : NUM540+1 : TPTP v9.0.0. Released v4.0.0.
% Transfm : none
% Format : tptp
% Command : run_E %s %d THM
% Computer : n013.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 94.91s 95.19s
% Output : Proof 95.07s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : NUM540+1 : TPTP v9.0.0. Released v4.0.0.
% 0.07/0.12 % Command : run_E %s %d THM
% 0.12/0.33 % Computer : n013.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:24:08 EDT 2025
% 0.12/0.33 % CPUTime :
% 94.91/95.19 % SZS status Theorem
% 94.91/95.19 % SZS output start Proof
% 94.91/95.19 tff(slbdtrb0_type, type, (
% 94.91/95.19 slbdtrb0: $i > $i)).
% 94.91/95.19 tff(sz00_type, type, (
% 94.91/95.19 sz00: $i)).
% 94.91/95.19 tff(tptp_fun_W1_4_type, type, (
% 94.91/95.19 tptp_fun_W1_4: $i > $i)).
% 94.91/95.19 tff(szszuzczcdt0_type, type, (
% 94.91/95.19 szszuzczcdt0: $i > $i)).
% 94.91/95.19 tff(aElementOf0_type, type, (
% 94.91/95.19 aElementOf0: ( $i * $i ) > $o)).
% 94.91/95.19 tff(tptp_fun_W1_0_type, type, (
% 94.91/95.19 tptp_fun_W1_0: $i > $i)).
% 94.91/95.19 tff(sdtlseqdt0_type, type, (
% 94.91/95.19 sdtlseqdt0: ( $i * $i ) > $o)).
% 94.91/95.19 tff(szNzAzT0_type, type, (
% 94.91/95.19 szNzAzT0: $i)).
% 94.91/95.19 tff(aSet0_type, type, (
% 94.91/95.19 aSet0: $i > $o)).
% 94.91/95.19 tff(slcrc0_type, type, (
% 94.91/95.19 slcrc0: $i)).
% 94.91/95.19 tff(sbrdtbr0_type, type, (
% 94.91/95.19 sbrdtbr0: $i > $i)).
% 94.91/95.19 tff(tptp_fun_W2_8_type, type, (
% 94.91/95.19 tptp_fun_W2_8: ( $i * $i ) > $i)).
% 94.91/95.19 tff(isFinite0_type, type, (
% 94.91/95.19 isFinite0: $i > $o)).
% 94.91/95.19 tff(1,plain,
% 94.91/95.19 (^[W0: $i] : rewrite((~((~((~(W0 = slcrc0)) | (~((~aSet0(W0)) | (~![W1: $i] : (~aElementOf0(W1, W0))))))) | (~((W0 = slcrc0) | (~aSet0(W0)) | aElementOf0(tptp_fun_W1_0(W0), W0))))) <=> (~((~((W0 = slcrc0) | (~aSet0(W0)) | aElementOf0(tptp_fun_W1_0(W0), W0))) | (~((~(W0 = slcrc0)) | (~((~aSet0(W0)) | (~![W1: $i] : (~aElementOf0(W1, W0))))))))))),
% 94.91/95.19 inference(bind,[status(th)],[])).
% 94.91/95.19 tff(2,plain,
% 94.91/95.19 (![W0: $i] : (~((~((~(W0 = slcrc0)) | (~((~aSet0(W0)) | (~![W1: $i] : (~aElementOf0(W1, W0))))))) | (~((W0 = slcrc0) | (~aSet0(W0)) | aElementOf0(tptp_fun_W1_0(W0), W0))))) <=> ![W0: $i] : (~((~((W0 = slcrc0) | (~aSet0(W0)) | aElementOf0(tptp_fun_W1_0(W0), W0))) | (~((~(W0 = slcrc0)) | (~((~aSet0(W0)) | (~![W1: $i] : (~aElementOf0(W1, W0)))))))))),
% 94.91/95.19 inference(quant_intro,[status(thm)],[1])).
% 94.91/95.19 tff(3,plain,
% 94.91/95.19 (^[W0: $i] : refl((~((~((~(W0 = slcrc0)) | (~((~aSet0(W0)) | (~![W1: $i] : (~aElementOf0(W1, W0))))))) | (~((W0 = slcrc0) | (~aSet0(W0)) | aElementOf0(tptp_fun_W1_0(W0), W0))))) <=> (~((~((~(W0 = slcrc0)) | (~((~aSet0(W0)) | (~![W1: $i] : (~aElementOf0(W1, W0))))))) | (~((W0 = slcrc0) | (~aSet0(W0)) | aElementOf0(tptp_fun_W1_0(W0), W0))))))),
% 94.91/95.19 inference(bind,[status(th)],[])).
% 94.91/95.19 tff(4,plain,
% 94.91/95.19 (![W0: $i] : (~((~((~(W0 = slcrc0)) | (~((~aSet0(W0)) | (~![W1: $i] : (~aElementOf0(W1, W0))))))) | (~((W0 = slcrc0) | (~aSet0(W0)) | aElementOf0(tptp_fun_W1_0(W0), W0))))) <=> ![W0: $i] : (~((~((~(W0 = slcrc0)) | (~((~aSet0(W0)) | (~![W1: $i] : (~aElementOf0(W1, W0))))))) | (~((W0 = slcrc0) | (~aSet0(W0)) | aElementOf0(tptp_fun_W1_0(W0), W0)))))),
% 94.91/95.19 inference(quant_intro,[status(thm)],[3])).
% 94.91/95.19 tff(5,plain,
% 94.91/95.19 (^[W0: $i] : rewrite((~((~((~(W0 = slcrc0)) | (~((~aSet0(W0)) | (~![W1: $i] : (~aElementOf0(W1, W0))))))) | (~((W0 = slcrc0) | (~aSet0(W0)) | aElementOf0(tptp_fun_W1_0(W0), W0))))) <=> (~((~((~(W0 = slcrc0)) | (~((~aSet0(W0)) | (~![W1: $i] : (~aElementOf0(W1, W0))))))) | (~((W0 = slcrc0) | (~aSet0(W0)) | aElementOf0(tptp_fun_W1_0(W0), W0))))))),
% 94.91/95.19 inference(bind,[status(th)],[])).
% 94.91/95.19 tff(6,plain,
% 94.91/95.19 (![W0: $i] : (~((~((~(W0 = slcrc0)) | (~((~aSet0(W0)) | (~![W1: $i] : (~aElementOf0(W1, W0))))))) | (~((W0 = slcrc0) | (~aSet0(W0)) | aElementOf0(tptp_fun_W1_0(W0), W0))))) <=> ![W0: $i] : (~((~((~(W0 = slcrc0)) | (~((~aSet0(W0)) | (~![W1: $i] : (~aElementOf0(W1, W0))))))) | (~((W0 = slcrc0) | (~aSet0(W0)) | aElementOf0(tptp_fun_W1_0(W0), W0)))))),
% 94.91/95.19 inference(quant_intro,[status(thm)],[5])).
% 94.91/95.19 tff(7,plain,
% 94.91/95.19 (![W0: $i] : (~((~((~(W0 = slcrc0)) | (~((~aSet0(W0)) | (~![W1: $i] : (~aElementOf0(W1, W0))))))) | (~((W0 = slcrc0) | (~aSet0(W0)) | aElementOf0(tptp_fun_W1_0(W0), W0))))) <=> ![W0: $i] : (~((~((~(W0 = slcrc0)) | (~((~aSet0(W0)) | (~![W1: $i] : (~aElementOf0(W1, W0))))))) | (~((W0 = slcrc0) | (~aSet0(W0)) | aElementOf0(tptp_fun_W1_0(W0), W0)))))),
% 94.91/95.19 inference(transitivity,[status(thm)],[6, 4])).
% 94.91/95.19 tff(8,plain,
% 94.91/95.19 (^[W0: $i] : trans(monotonicity(rewrite(((~(W0 = slcrc0)) | (aSet0(W0) & ![W1: $i] : (~aElementOf0(W1, W0)))) <=> ((~(W0 = slcrc0)) | (~((~aSet0(W0)) | (~![W1: $i] : (~aElementOf0(W1, W0))))))), rewrite(((W0 = slcrc0) | (~aSet0(W0)) | aElementOf0(tptp_fun_W1_0(W0), W0)) <=> ((W0 = slcrc0) | (~aSet0(W0)) | aElementOf0(tptp_fun_W1_0(W0), W0))), ((((~(W0 = slcrc0)) | (aSet0(W0) & ![W1: $i] : (~aElementOf0(W1, W0)))) & ((W0 = slcrc0) | (~aSet0(W0)) | aElementOf0(tptp_fun_W1_0(W0), W0))) <=> (((~(W0 = slcrc0)) | (~((~aSet0(W0)) | (~![W1: $i] : (~aElementOf0(W1, W0)))))) & ((W0 = slcrc0) | (~aSet0(W0)) | aElementOf0(tptp_fun_W1_0(W0), W0))))), rewrite((((~(W0 = slcrc0)) | (~((~aSet0(W0)) | (~![W1: $i] : (~aElementOf0(W1, W0)))))) & ((W0 = slcrc0) | (~aSet0(W0)) | aElementOf0(tptp_fun_W1_0(W0), W0))) <=> (~((~((~(W0 = slcrc0)) | (~((~aSet0(W0)) | (~![W1: $i] : (~aElementOf0(W1, W0))))))) | (~((W0 = slcrc0) | (~aSet0(W0)) | aElementOf0(tptp_fun_W1_0(W0), W0)))))), ((((~(W0 = slcrc0)) | (aSet0(W0) & ![W1: $i] : (~aElementOf0(W1, W0)))) & ((W0 = slcrc0) | (~aSet0(W0)) | aElementOf0(tptp_fun_W1_0(W0), W0))) <=> (~((~((~(W0 = slcrc0)) | (~((~aSet0(W0)) | (~![W1: $i] : (~aElementOf0(W1, W0))))))) | (~((W0 = slcrc0) | (~aSet0(W0)) | aElementOf0(tptp_fun_W1_0(W0), W0)))))))),
% 94.91/95.19 inference(bind,[status(th)],[])).
% 94.91/95.19 tff(9,plain,
% 94.91/95.19 (![W0: $i] : (((~(W0 = slcrc0)) | (aSet0(W0) & ![W1: $i] : (~aElementOf0(W1, W0)))) & ((W0 = slcrc0) | (~aSet0(W0)) | aElementOf0(tptp_fun_W1_0(W0), W0))) <=> ![W0: $i] : (~((~((~(W0 = slcrc0)) | (~((~aSet0(W0)) | (~![W1: $i] : (~aElementOf0(W1, W0))))))) | (~((W0 = slcrc0) | (~aSet0(W0)) | aElementOf0(tptp_fun_W1_0(W0), W0)))))),
% 94.91/95.19 inference(quant_intro,[status(thm)],[8])).
% 94.91/95.19 tff(10,plain,
% 94.91/95.19 (^[W0: $i] : rewrite((((~(W0 = slcrc0)) | (aSet0(W0) & ![W1: $i] : (~aElementOf0(W1, W0)))) & ((W0 = slcrc0) | ((~aSet0(W0)) | aElementOf0(tptp_fun_W1_0(W0), W0)))) <=> (((~(W0 = slcrc0)) | (aSet0(W0) & ![W1: $i] : (~aElementOf0(W1, W0)))) & ((W0 = slcrc0) | (~aSet0(W0)) | aElementOf0(tptp_fun_W1_0(W0), W0))))),
% 94.91/95.19 inference(bind,[status(th)],[])).
% 94.91/95.19 tff(11,plain,
% 94.91/95.19 (![W0: $i] : (((~(W0 = slcrc0)) | (aSet0(W0) & ![W1: $i] : (~aElementOf0(W1, W0)))) & ((W0 = slcrc0) | ((~aSet0(W0)) | aElementOf0(tptp_fun_W1_0(W0), W0)))) <=> ![W0: $i] : (((~(W0 = slcrc0)) | (aSet0(W0) & ![W1: $i] : (~aElementOf0(W1, W0)))) & ((W0 = slcrc0) | (~aSet0(W0)) | aElementOf0(tptp_fun_W1_0(W0), W0)))),
% 94.91/95.19 inference(quant_intro,[status(thm)],[10])).
% 94.91/95.19 tff(12,plain,
% 94.91/95.19 (![W0: $i] : ((W0 = slcrc0) <=> (aSet0(W0) & (~?[W1: $i] : aElementOf0(W1, W0)))) <=> ![W0: $i] : ((W0 = slcrc0) <=> (aSet0(W0) & (~?[W1: $i] : aElementOf0(W1, W0))))),
% 94.91/95.19 inference(rewrite,[status(thm)],[])).
% 94.91/95.19 tff(13,axiom,(![W0: $i] : ((W0 = slcrc0) <=> (aSet0(W0) & (~?[W1: $i] : aElementOf0(W1, W0))))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','mDefEmp')).
% 94.91/95.19 tff(14,plain,
% 94.91/95.19 (![W0: $i] : ((W0 = slcrc0) <=> (aSet0(W0) & (~?[W1: $i] : aElementOf0(W1, W0))))),
% 94.91/95.19 inference(modus_ponens,[status(thm)],[13, 12])).
% 94.91/95.19 tff(15,plain,(
% 94.91/95.19 ![W0: $i] : (((~(W0 = slcrc0)) | (aSet0(W0) & ![W1: $i] : (~aElementOf0(W1, W0)))) & ((W0 = slcrc0) | ((~aSet0(W0)) | aElementOf0(tptp_fun_W1_0(W0), W0))))),
% 94.91/95.19 inference(skolemize,[status(sab)],[14])).
% 94.91/95.19 tff(16,plain,
% 94.91/95.19 (![W0: $i] : (((~(W0 = slcrc0)) | (aSet0(W0) & ![W1: $i] : (~aElementOf0(W1, W0)))) & ((W0 = slcrc0) | (~aSet0(W0)) | aElementOf0(tptp_fun_W1_0(W0), W0)))),
% 94.91/95.19 inference(modus_ponens,[status(thm)],[15, 11])).
% 94.91/95.19 tff(17,plain,
% 94.91/95.19 (![W0: $i] : (~((~((~(W0 = slcrc0)) | (~((~aSet0(W0)) | (~![W1: $i] : (~aElementOf0(W1, W0))))))) | (~((W0 = slcrc0) | (~aSet0(W0)) | aElementOf0(tptp_fun_W1_0(W0), W0)))))),
% 94.91/95.19 inference(modus_ponens,[status(thm)],[16, 9])).
% 94.91/95.19 tff(18,plain,
% 94.91/95.19 (![W0: $i] : (~((~((~(W0 = slcrc0)) | (~((~aSet0(W0)) | (~![W1: $i] : (~aElementOf0(W1, W0))))))) | (~((W0 = slcrc0) | (~aSet0(W0)) | aElementOf0(tptp_fun_W1_0(W0), W0)))))),
% 94.91/95.19 inference(modus_ponens,[status(thm)],[17, 7])).
% 94.91/95.19 tff(19,plain,
% 94.91/95.19 (![W0: $i] : (~((~((W0 = slcrc0) | (~aSet0(W0)) | aElementOf0(tptp_fun_W1_0(W0), W0))) | (~((~(W0 = slcrc0)) | (~((~aSet0(W0)) | (~![W1: $i] : (~aElementOf0(W1, W0)))))))))),
% 94.91/95.19 inference(modus_ponens,[status(thm)],[18, 2])).
% 94.91/95.19 tff(20,plain,
% 94.91/95.19 ((~![W0: $i] : (~((~((W0 = slcrc0) | (~aSet0(W0)) | aElementOf0(tptp_fun_W1_0(W0), W0))) | (~((~(W0 = slcrc0)) | (~((~aSet0(W0)) | (~![W1: $i] : (~aElementOf0(W1, W0)))))))))) | (~((~((slbdtrb0(tptp_fun_W1_4(szszuzczcdt0(sz00))) = slcrc0) | (~aSet0(slbdtrb0(tptp_fun_W1_4(szszuzczcdt0(sz00))))) | aElementOf0(tptp_fun_W1_0(slbdtrb0(tptp_fun_W1_4(szszuzczcdt0(sz00)))), slbdtrb0(tptp_fun_W1_4(szszuzczcdt0(sz00)))))) | (~((~(slbdtrb0(tptp_fun_W1_4(szszuzczcdt0(sz00))) = slcrc0)) | (~((~aSet0(slbdtrb0(tptp_fun_W1_4(szszuzczcdt0(sz00))))) | (~![W1: $i] : (~aElementOf0(W1, slbdtrb0(tptp_fun_W1_4(szszuzczcdt0(sz00))))))))))))),
% 94.91/95.20 inference(quant_inst,[status(thm)],[])).
% 94.91/95.20 tff(21,plain,
% 94.91/95.20 (~((~((slbdtrb0(tptp_fun_W1_4(szszuzczcdt0(sz00))) = slcrc0) | (~aSet0(slbdtrb0(tptp_fun_W1_4(szszuzczcdt0(sz00))))) | aElementOf0(tptp_fun_W1_0(slbdtrb0(tptp_fun_W1_4(szszuzczcdt0(sz00)))), slbdtrb0(tptp_fun_W1_4(szszuzczcdt0(sz00)))))) | (~((~(slbdtrb0(tptp_fun_W1_4(szszuzczcdt0(sz00))) = slcrc0)) | (~((~aSet0(slbdtrb0(tptp_fun_W1_4(szszuzczcdt0(sz00))))) | (~![W1: $i] : (~aElementOf0(W1, slbdtrb0(tptp_fun_W1_4(szszuzczcdt0(sz00)))))))))))),
% 94.91/95.20 inference(unit_resolution,[status(thm)],[20, 19])).
% 94.91/95.20 tff(22,plain,
% 94.91/95.20 (((~((slbdtrb0(tptp_fun_W1_4(szszuzczcdt0(sz00))) = slcrc0) | (~aSet0(slbdtrb0(tptp_fun_W1_4(szszuzczcdt0(sz00))))) | aElementOf0(tptp_fun_W1_0(slbdtrb0(tptp_fun_W1_4(szszuzczcdt0(sz00)))), slbdtrb0(tptp_fun_W1_4(szszuzczcdt0(sz00)))))) | (~((~(slbdtrb0(tptp_fun_W1_4(szszuzczcdt0(sz00))) = slcrc0)) | (~((~aSet0(slbdtrb0(tptp_fun_W1_4(szszuzczcdt0(sz00))))) | (~![W1: $i] : (~aElementOf0(W1, slbdtrb0(tptp_fun_W1_4(szszuzczcdt0(sz00))))))))))) | ((slbdtrb0(tptp_fun_W1_4(szszuzczcdt0(sz00))) = slcrc0) | (~aSet0(slbdtrb0(tptp_fun_W1_4(szszuzczcdt0(sz00))))) | aElementOf0(tptp_fun_W1_0(slbdtrb0(tptp_fun_W1_4(szszuzczcdt0(sz00)))), slbdtrb0(tptp_fun_W1_4(szszuzczcdt0(sz00)))))),
% 94.91/95.20 inference(tautology,[status(thm)],[])).
% 94.91/95.20 tff(23,plain,
% 94.91/95.20 ((slbdtrb0(tptp_fun_W1_4(szszuzczcdt0(sz00))) = slcrc0) | (~aSet0(slbdtrb0(tptp_fun_W1_4(szszuzczcdt0(sz00))))) | aElementOf0(tptp_fun_W1_0(slbdtrb0(tptp_fun_W1_4(szszuzczcdt0(sz00)))), slbdtrb0(tptp_fun_W1_4(szszuzczcdt0(sz00))))),
% 94.91/95.20 inference(unit_resolution,[status(thm)],[22, 21])).
% 94.91/95.20 tff(24,assumption,((~((~aSet0(slbdtrb0(tptp_fun_W1_4(szszuzczcdt0(sz00))))) | (slbdtrb0(tptp_fun_W1_4(szszuzczcdt0(sz00))) = slbdtrb0(sbrdtbr0(slcrc0))) | (((~aElementOf0(tptp_fun_W2_8(slbdtrb0(tptp_fun_W1_4(szszuzczcdt0(sz00))), sbrdtbr0(slcrc0)), szNzAzT0)) | (~sdtlseqdt0(szszuzczcdt0(tptp_fun_W2_8(slbdtrb0(tptp_fun_W1_4(szszuzczcdt0(sz00))), sbrdtbr0(slcrc0))), sbrdtbr0(slcrc0)))) <=> aElementOf0(tptp_fun_W2_8(slbdtrb0(tptp_fun_W1_4(szszuzczcdt0(sz00))), sbrdtbr0(slcrc0)), slbdtrb0(tptp_fun_W1_4(szszuzczcdt0(sz00))))))) | (~((~(slbdtrb0(tptp_fun_W1_4(szszuzczcdt0(sz00))) = slbdtrb0(sbrdtbr0(slcrc0)))) | (~((~aSet0(slbdtrb0(tptp_fun_W1_4(szszuzczcdt0(sz00))))) | (~![W2: $i] : (~(((~aElementOf0(W2, szNzAzT0)) | (~sdtlseqdt0(szszuzczcdt0(W2), sbrdtbr0(slcrc0)))) <=> aElementOf0(W2, slbdtrb0(tptp_fun_W1_4(szszuzczcdt0(sz00)))))))))))), introduced(assumption)).
% 94.91/95.20 tff(25,assumption,((~aSet0(slcrc0)) | (~![W1: $i] : (~aElementOf0(W1, slcrc0)))), introduced(assumption)).
% 94.91/95.20 tff(26,plain,
% 94.91/95.20 (((~![W0: $i] : (~((~((W0 = slcrc0) | (~aSet0(W0)) | aElementOf0(tptp_fun_W1_0(W0), W0))) | (~((~(W0 = slcrc0)) | (~((~aSet0(W0)) | (~![W1: $i] : (~aElementOf0(W1, W0)))))))))) | (~((~aSet0(slcrc0)) | (~![W1: $i] : (~aElementOf0(W1, slcrc0)))))) <=> ((~![W0: $i] : (~((~((W0 = slcrc0) | (~aSet0(W0)) | aElementOf0(tptp_fun_W1_0(W0), W0))) | (~((~(W0 = slcrc0)) | (~((~aSet0(W0)) | (~![W1: $i] : (~aElementOf0(W1, W0)))))))))) | (~((~aSet0(slcrc0)) | (~![W1: $i] : (~aElementOf0(W1, slcrc0))))))),
% 94.91/95.20 inference(rewrite,[status(thm)],[])).
% 94.91/95.20 tff(27,plain,
% 94.91/95.20 ((~((~((slcrc0 = slcrc0) | (~aSet0(slcrc0)) | aElementOf0(tptp_fun_W1_0(slcrc0), slcrc0))) | (~((~(slcrc0 = slcrc0)) | (~((~aSet0(slcrc0)) | (~![W1: $i] : (~aElementOf0(W1, slcrc0))))))))) <=> (~((~aSet0(slcrc0)) | (~![W1: $i] : (~aElementOf0(W1, slcrc0)))))),
% 94.91/95.20 inference(rewrite,[status(thm)],[])).
% 94.91/95.20 tff(28,plain,
% 94.91/95.20 (((~![W0: $i] : (~((~((W0 = slcrc0) | (~aSet0(W0)) | aElementOf0(tptp_fun_W1_0(W0), W0))) | (~((~(W0 = slcrc0)) | (~((~aSet0(W0)) | (~![W1: $i] : (~aElementOf0(W1, W0)))))))))) | (~((~((slcrc0 = slcrc0) | (~aSet0(slcrc0)) | aElementOf0(tptp_fun_W1_0(slcrc0), slcrc0))) | (~((~(slcrc0 = slcrc0)) | (~((~aSet0(slcrc0)) | (~![W1: $i] : (~aElementOf0(W1, slcrc0)))))))))) <=> ((~![W0: $i] : (~((~((W0 = slcrc0) | (~aSet0(W0)) | aElementOf0(tptp_fun_W1_0(W0), W0))) | (~((~(W0 = slcrc0)) | (~((~aSet0(W0)) | (~![W1: $i] : (~aElementOf0(W1, W0)))))))))) | (~((~aSet0(slcrc0)) | (~![W1: $i] : (~aElementOf0(W1, slcrc0))))))),
% 94.91/95.20 inference(monotonicity,[status(thm)],[27])).
% 94.91/95.20 tff(29,plain,
% 94.91/95.20 (((~![W0: $i] : (~((~((W0 = slcrc0) | (~aSet0(W0)) | aElementOf0(tptp_fun_W1_0(W0), W0))) | (~((~(W0 = slcrc0)) | (~((~aSet0(W0)) | (~![W1: $i] : (~aElementOf0(W1, W0)))))))))) | (~((~((slcrc0 = slcrc0) | (~aSet0(slcrc0)) | aElementOf0(tptp_fun_W1_0(slcrc0), slcrc0))) | (~((~(slcrc0 = slcrc0)) | (~((~aSet0(slcrc0)) | (~![W1: $i] : (~aElementOf0(W1, slcrc0)))))))))) <=> ((~![W0: $i] : (~((~((W0 = slcrc0) | (~aSet0(W0)) | aElementOf0(tptp_fun_W1_0(W0), W0))) | (~((~(W0 = slcrc0)) | (~((~aSet0(W0)) | (~![W1: $i] : (~aElementOf0(W1, W0)))))))))) | (~((~aSet0(slcrc0)) | (~![W1: $i] : (~aElementOf0(W1, slcrc0))))))),
% 94.91/95.20 inference(transitivity,[status(thm)],[28, 26])).
% 94.91/95.20 tff(30,plain,
% 94.91/95.20 ((~![W0: $i] : (~((~((W0 = slcrc0) | (~aSet0(W0)) | aElementOf0(tptp_fun_W1_0(W0), W0))) | (~((~(W0 = slcrc0)) | (~((~aSet0(W0)) | (~![W1: $i] : (~aElementOf0(W1, W0)))))))))) | (~((~((slcrc0 = slcrc0) | (~aSet0(slcrc0)) | aElementOf0(tptp_fun_W1_0(slcrc0), slcrc0))) | (~((~(slcrc0 = slcrc0)) | (~((~aSet0(slcrc0)) | (~![W1: $i] : (~aElementOf0(W1, slcrc0)))))))))),
% 94.91/95.20 inference(quant_inst,[status(thm)],[])).
% 94.91/95.20 tff(31,plain,
% 94.91/95.20 ((~![W0: $i] : (~((~((W0 = slcrc0) | (~aSet0(W0)) | aElementOf0(tptp_fun_W1_0(W0), W0))) | (~((~(W0 = slcrc0)) | (~((~aSet0(W0)) | (~![W1: $i] : (~aElementOf0(W1, W0)))))))))) | (~((~aSet0(slcrc0)) | (~![W1: $i] : (~aElementOf0(W1, slcrc0)))))),
% 94.91/95.20 inference(modus_ponens,[status(thm)],[30, 29])).
% 94.91/95.20 tff(32,plain,
% 94.91/95.20 ($false),
% 94.91/95.20 inference(unit_resolution,[status(thm)],[31, 19, 25])).
% 94.91/95.20 tff(33,plain,(~((~aSet0(slcrc0)) | (~![W1: $i] : (~aElementOf0(W1, slcrc0))))), inference(lemma,lemma(discharge,[]))).
% 94.91/95.20 tff(34,plain,
% 94.91/95.20 (((~aSet0(slcrc0)) | (~![W1: $i] : (~aElementOf0(W1, slcrc0)))) | aSet0(slcrc0)),
% 94.91/95.20 inference(tautology,[status(thm)],[])).
% 94.91/95.20 tff(35,plain,
% 94.91/95.20 (aSet0(slcrc0)),
% 94.91/95.20 inference(unit_resolution,[status(thm)],[34, 33])).
% 94.91/95.20 tff(36,plain,
% 94.91/95.20 (^[W0: $i] : refl(((~aSet0(W0)) | (aElementOf0(sbrdtbr0(W0), szNzAzT0) <=> isFinite0(W0))) <=> ((~aSet0(W0)) | (aElementOf0(sbrdtbr0(W0), szNzAzT0) <=> isFinite0(W0))))),
% 94.91/95.20 inference(bind,[status(th)],[])).
% 94.91/95.20 tff(37,plain,
% 94.91/95.20 (![W0: $i] : ((~aSet0(W0)) | (aElementOf0(sbrdtbr0(W0), szNzAzT0) <=> isFinite0(W0))) <=> ![W0: $i] : ((~aSet0(W0)) | (aElementOf0(sbrdtbr0(W0), szNzAzT0) <=> isFinite0(W0)))),
% 94.91/95.20 inference(quant_intro,[status(thm)],[36])).
% 94.91/95.20 tff(38,plain,
% 94.91/95.20 (![W0: $i] : ((~aSet0(W0)) | (aElementOf0(sbrdtbr0(W0), szNzAzT0) <=> isFinite0(W0))) <=> ![W0: $i] : ((~aSet0(W0)) | (aElementOf0(sbrdtbr0(W0), szNzAzT0) <=> isFinite0(W0)))),
% 94.91/95.20 inference(rewrite,[status(thm)],[])).
% 94.91/95.20 tff(39,plain,
% 94.91/95.20 (^[W0: $i] : rewrite((aSet0(W0) => (aElementOf0(sbrdtbr0(W0), szNzAzT0) <=> isFinite0(W0))) <=> ((~aSet0(W0)) | (aElementOf0(sbrdtbr0(W0), szNzAzT0) <=> isFinite0(W0))))),
% 94.91/95.20 inference(bind,[status(th)],[])).
% 94.91/95.20 tff(40,plain,
% 94.91/95.20 (![W0: $i] : (aSet0(W0) => (aElementOf0(sbrdtbr0(W0), szNzAzT0) <=> isFinite0(W0))) <=> ![W0: $i] : ((~aSet0(W0)) | (aElementOf0(sbrdtbr0(W0), szNzAzT0) <=> isFinite0(W0)))),
% 94.91/95.20 inference(quant_intro,[status(thm)],[39])).
% 94.91/95.20 tff(41,axiom,(![W0: $i] : (aSet0(W0) => (aElementOf0(sbrdtbr0(W0), szNzAzT0) <=> isFinite0(W0)))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','mCardNum')).
% 94.91/95.20 tff(42,plain,
% 94.91/95.20 (![W0: $i] : ((~aSet0(W0)) | (aElementOf0(sbrdtbr0(W0), szNzAzT0) <=> isFinite0(W0)))),
% 94.91/95.20 inference(modus_ponens,[status(thm)],[41, 40])).
% 94.91/95.20 tff(43,plain,
% 94.91/95.20 (![W0: $i] : ((~aSet0(W0)) | (aElementOf0(sbrdtbr0(W0), szNzAzT0) <=> isFinite0(W0)))),
% 94.91/95.20 inference(modus_ponens,[status(thm)],[42, 38])).
% 94.91/95.20 tff(44,plain,(
% 94.91/95.20 ![W0: $i] : ((~aSet0(W0)) | (aElementOf0(sbrdtbr0(W0), szNzAzT0) <=> isFinite0(W0)))),
% 94.91/95.20 inference(skolemize,[status(sab)],[43])).
% 94.91/95.20 tff(45,plain,
% 94.91/95.20 (![W0: $i] : ((~aSet0(W0)) | (aElementOf0(sbrdtbr0(W0), szNzAzT0) <=> isFinite0(W0)))),
% 94.91/95.20 inference(modus_ponens,[status(thm)],[44, 37])).
% 94.91/95.20 tff(46,plain,
% 94.91/95.20 (((~![W0: $i] : ((~aSet0(W0)) | (aElementOf0(sbrdtbr0(W0), szNzAzT0) <=> isFinite0(W0)))) | ((~aSet0(slcrc0)) | (aElementOf0(sbrdtbr0(slcrc0), szNzAzT0) <=> isFinite0(slcrc0)))) <=> ((~![W0: $i] : ((~aSet0(W0)) | (aElementOf0(sbrdtbr0(W0), szNzAzT0) <=> isFinite0(W0)))) | (~aSet0(slcrc0)) | (aElementOf0(sbrdtbr0(slcrc0), szNzAzT0) <=> isFinite0(slcrc0)))),
% 94.91/95.20 inference(rewrite,[status(thm)],[])).
% 94.91/95.20 tff(47,plain,
% 94.91/95.20 ((~![W0: $i] : ((~aSet0(W0)) | (aElementOf0(sbrdtbr0(W0), szNzAzT0) <=> isFinite0(W0)))) | ((~aSet0(slcrc0)) | (aElementOf0(sbrdtbr0(slcrc0), szNzAzT0) <=> isFinite0(slcrc0)))),
% 94.91/95.20 inference(quant_inst,[status(thm)],[])).
% 94.91/95.20 tff(48,plain,
% 94.91/95.20 ((~![W0: $i] : ((~aSet0(W0)) | (aElementOf0(sbrdtbr0(W0), szNzAzT0) <=> isFinite0(W0)))) | (~aSet0(slcrc0)) | (aElementOf0(sbrdtbr0(slcrc0), szNzAzT0) <=> isFinite0(slcrc0))),
% 94.91/95.20 inference(modus_ponens,[status(thm)],[47, 46])).
% 94.91/95.20 tff(49,plain,
% 94.91/95.20 ((~aSet0(slcrc0)) | (aElementOf0(sbrdtbr0(slcrc0), szNzAzT0) <=> isFinite0(slcrc0))),
% 94.91/95.20 inference(unit_resolution,[status(thm)],[48, 45])).
% 94.91/95.20 tff(50,plain,
% 94.91/95.20 (aElementOf0(sbrdtbr0(slcrc0), szNzAzT0) <=> isFinite0(slcrc0)),
% 94.91/95.20 inference(unit_resolution,[status(thm)],[49, 35])).
% 94.91/95.20 tff(51,plain,
% 94.91/95.20 (isFinite0(slcrc0) <=> isFinite0(slcrc0)),
% 94.91/95.20 inference(rewrite,[status(thm)],[])).
% 94.91/95.20 tff(52,axiom,(isFinite0(slcrc0)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','mEmpFin')).
% 94.91/95.20 tff(53,plain,
% 94.91/95.20 (isFinite0(slcrc0)),
% 94.91/95.20 inference(modus_ponens,[status(thm)],[52, 51])).
% 94.91/95.20 tff(54,plain,
% 94.91/95.20 ((~(aElementOf0(sbrdtbr0(slcrc0), szNzAzT0) <=> isFinite0(slcrc0))) | aElementOf0(sbrdtbr0(slcrc0), szNzAzT0) | (~isFinite0(slcrc0))),
% 94.91/95.20 inference(tautology,[status(thm)],[])).
% 94.91/95.20 tff(55,plain,
% 94.91/95.20 ((~(aElementOf0(sbrdtbr0(slcrc0), szNzAzT0) <=> isFinite0(slcrc0))) | aElementOf0(sbrdtbr0(slcrc0), szNzAzT0)),
% 94.91/95.20 inference(unit_resolution,[status(thm)],[54, 53])).
% 94.91/95.20 tff(56,plain,
% 94.91/95.20 (aElementOf0(sbrdtbr0(slcrc0), szNzAzT0)),
% 94.91/95.20 inference(unit_resolution,[status(thm)],[55, 50])).
% 94.91/95.20 tff(57,plain,
% 94.91/95.20 (^[W0: $i] : rewrite(((~aElementOf0(W0, szNzAzT0)) | ![W1: $i] : (~((~((~(W1 = slbdtrb0(W0))) | (~((~aSet0(W1)) | (~![W2: $i] : (~(((~aElementOf0(W2, szNzAzT0)) | (~sdtlseqdt0(szszuzczcdt0(W2), W0))) <=> aElementOf0(W2, W1)))))))) | (~((W1 = slbdtrb0(W0)) | (~aSet0(W1)) | (((~aElementOf0(tptp_fun_W2_8(W1, W0), szNzAzT0)) | (~sdtlseqdt0(szszuzczcdt0(tptp_fun_W2_8(W1, W0)), W0))) <=> aElementOf0(tptp_fun_W2_8(W1, W0), W1))))))) <=> ((~aElementOf0(W0, szNzAzT0)) | ![W1: $i] : (~((~((W1 = slbdtrb0(W0)) | (~aSet0(W1)) | (((~aElementOf0(tptp_fun_W2_8(W1, W0), szNzAzT0)) | (~sdtlseqdt0(szszuzczcdt0(tptp_fun_W2_8(W1, W0)), W0))) <=> aElementOf0(tptp_fun_W2_8(W1, W0), W1)))) | (~((~(W1 = slbdtrb0(W0))) | (~((~aSet0(W1)) | (~![W2: $i] : (~(((~aElementOf0(W2, szNzAzT0)) | (~sdtlseqdt0(szszuzczcdt0(W2), W0))) <=> aElementOf0(W2, W1))))))))))))),
% 94.91/95.20 inference(bind,[status(th)],[])).
% 94.91/95.20 tff(58,plain,
% 94.91/95.20 (![W0: $i] : ((~aElementOf0(W0, szNzAzT0)) | ![W1: $i] : (~((~((~(W1 = slbdtrb0(W0))) | (~((~aSet0(W1)) | (~![W2: $i] : (~(((~aElementOf0(W2, szNzAzT0)) | (~sdtlseqdt0(szszuzczcdt0(W2), W0))) <=> aElementOf0(W2, W1)))))))) | (~((W1 = slbdtrb0(W0)) | (~aSet0(W1)) | (((~aElementOf0(tptp_fun_W2_8(W1, W0), szNzAzT0)) | (~sdtlseqdt0(szszuzczcdt0(tptp_fun_W2_8(W1, W0)), W0))) <=> aElementOf0(tptp_fun_W2_8(W1, W0), W1))))))) <=> ![W0: $i] : ((~aElementOf0(W0, szNzAzT0)) | ![W1: $i] : (~((~((W1 = slbdtrb0(W0)) | (~aSet0(W1)) | (((~aElementOf0(tptp_fun_W2_8(W1, W0), szNzAzT0)) | (~sdtlseqdt0(szszuzczcdt0(tptp_fun_W2_8(W1, W0)), W0))) <=> aElementOf0(tptp_fun_W2_8(W1, W0), W1)))) | (~((~(W1 = slbdtrb0(W0))) | (~((~aSet0(W1)) | (~![W2: $i] : (~(((~aElementOf0(W2, szNzAzT0)) | (~sdtlseqdt0(szszuzczcdt0(W2), W0))) <=> aElementOf0(W2, W1)))))))))))),
% 94.91/95.20 inference(quant_intro,[status(thm)],[57])).
% 94.91/95.20 tff(59,plain,
% 94.91/95.20 (^[W0: $i] : refl(((~aElementOf0(W0, szNzAzT0)) | ![W1: $i] : (~((~((~(W1 = slbdtrb0(W0))) | (~((~aSet0(W1)) | (~![W2: $i] : (~(((~aElementOf0(W2, szNzAzT0)) | (~sdtlseqdt0(szszuzczcdt0(W2), W0))) <=> aElementOf0(W2, W1)))))))) | (~((W1 = slbdtrb0(W0)) | (~aSet0(W1)) | (((~aElementOf0(tptp_fun_W2_8(W1, W0), szNzAzT0)) | (~sdtlseqdt0(szszuzczcdt0(tptp_fun_W2_8(W1, W0)), W0))) <=> aElementOf0(tptp_fun_W2_8(W1, W0), W1))))))) <=> ((~aElementOf0(W0, szNzAzT0)) | ![W1: $i] : (~((~((~(W1 = slbdtrb0(W0))) | (~((~aSet0(W1)) | (~![W2: $i] : (~(((~aElementOf0(W2, szNzAzT0)) | (~sdtlseqdt0(szszuzczcdt0(W2), W0))) <=> aElementOf0(W2, W1)))))))) | (~((W1 = slbdtrb0(W0)) | (~aSet0(W1)) | (((~aElementOf0(tptp_fun_W2_8(W1, W0), szNzAzT0)) | (~sdtlseqdt0(szszuzczcdt0(tptp_fun_W2_8(W1, W0)), W0))) <=> aElementOf0(tptp_fun_W2_8(W1, W0), W1))))))))),
% 94.91/95.20 inference(bind,[status(th)],[])).
% 94.91/95.20 tff(60,plain,
% 94.91/95.20 (![W0: $i] : ((~aElementOf0(W0, szNzAzT0)) | ![W1: $i] : (~((~((~(W1 = slbdtrb0(W0))) | (~((~aSet0(W1)) | (~![W2: $i] : (~(((~aElementOf0(W2, szNzAzT0)) | (~sdtlseqdt0(szszuzczcdt0(W2), W0))) <=> aElementOf0(W2, W1)))))))) | (~((W1 = slbdtrb0(W0)) | (~aSet0(W1)) | (((~aElementOf0(tptp_fun_W2_8(W1, W0), szNzAzT0)) | (~sdtlseqdt0(szszuzczcdt0(tptp_fun_W2_8(W1, W0)), W0))) <=> aElementOf0(tptp_fun_W2_8(W1, W0), W1))))))) <=> ![W0: $i] : ((~aElementOf0(W0, szNzAzT0)) | ![W1: $i] : (~((~((~(W1 = slbdtrb0(W0))) | (~((~aSet0(W1)) | (~![W2: $i] : (~(((~aElementOf0(W2, szNzAzT0)) | (~sdtlseqdt0(szszuzczcdt0(W2), W0))) <=> aElementOf0(W2, W1)))))))) | (~((W1 = slbdtrb0(W0)) | (~aSet0(W1)) | (((~aElementOf0(tptp_fun_W2_8(W1, W0), szNzAzT0)) | (~sdtlseqdt0(szszuzczcdt0(tptp_fun_W2_8(W1, W0)), W0))) <=> aElementOf0(tptp_fun_W2_8(W1, W0), W1)))))))),
% 94.91/95.20 inference(quant_intro,[status(thm)],[59])).
% 94.91/95.20 tff(61,plain,
% 94.91/95.20 (^[W0: $i] : rewrite(((~aElementOf0(W0, szNzAzT0)) | ![W1: $i] : (~((~((~(W1 = slbdtrb0(W0))) | (~((~aSet0(W1)) | (~![W2: $i] : (~(((~aElementOf0(W2, szNzAzT0)) | (~sdtlseqdt0(szszuzczcdt0(W2), W0))) <=> aElementOf0(W2, W1)))))))) | (~((W1 = slbdtrb0(W0)) | (~aSet0(W1)) | (((~aElementOf0(tptp_fun_W2_8(W1, W0), szNzAzT0)) | (~sdtlseqdt0(szszuzczcdt0(tptp_fun_W2_8(W1, W0)), W0))) <=> aElementOf0(tptp_fun_W2_8(W1, W0), W1))))))) <=> ((~aElementOf0(W0, szNzAzT0)) | ![W1: $i] : (~((~((~(W1 = slbdtrb0(W0))) | (~((~aSet0(W1)) | (~![W2: $i] : (~(((~aElementOf0(W2, szNzAzT0)) | (~sdtlseqdt0(szszuzczcdt0(W2), W0))) <=> aElementOf0(W2, W1)))))))) | (~((W1 = slbdtrb0(W0)) | (~aSet0(W1)) | (((~aElementOf0(tptp_fun_W2_8(W1, W0), szNzAzT0)) | (~sdtlseqdt0(szszuzczcdt0(tptp_fun_W2_8(W1, W0)), W0))) <=> aElementOf0(tptp_fun_W2_8(W1, W0), W1))))))))),
% 94.91/95.20 inference(bind,[status(th)],[])).
% 94.91/95.20 tff(62,plain,
% 94.91/95.20 (![W0: $i] : ((~aElementOf0(W0, szNzAzT0)) | ![W1: $i] : (~((~((~(W1 = slbdtrb0(W0))) | (~((~aSet0(W1)) | (~![W2: $i] : (~(((~aElementOf0(W2, szNzAzT0)) | (~sdtlseqdt0(szszuzczcdt0(W2), W0))) <=> aElementOf0(W2, W1)))))))) | (~((W1 = slbdtrb0(W0)) | (~aSet0(W1)) | (((~aElementOf0(tptp_fun_W2_8(W1, W0), szNzAzT0)) | (~sdtlseqdt0(szszuzczcdt0(tptp_fun_W2_8(W1, W0)), W0))) <=> aElementOf0(tptp_fun_W2_8(W1, W0), W1))))))) <=> ![W0: $i] : ((~aElementOf0(W0, szNzAzT0)) | ![W1: $i] : (~((~((~(W1 = slbdtrb0(W0))) | (~((~aSet0(W1)) | (~![W2: $i] : (~(((~aElementOf0(W2, szNzAzT0)) | (~sdtlseqdt0(szszuzczcdt0(W2), W0))) <=> aElementOf0(W2, W1)))))))) | (~((W1 = slbdtrb0(W0)) | (~aSet0(W1)) | (((~aElementOf0(tptp_fun_W2_8(W1, W0), szNzAzT0)) | (~sdtlseqdt0(szszuzczcdt0(tptp_fun_W2_8(W1, W0)), W0))) <=> aElementOf0(tptp_fun_W2_8(W1, W0), W1)))))))),
% 94.91/95.20 inference(quant_intro,[status(thm)],[61])).
% 94.91/95.20 tff(63,plain,
% 94.91/95.20 (![W0: $i] : ((~aElementOf0(W0, szNzAzT0)) | ![W1: $i] : (~((~((~(W1 = slbdtrb0(W0))) | (~((~aSet0(W1)) | (~![W2: $i] : (~(((~aElementOf0(W2, szNzAzT0)) | (~sdtlseqdt0(szszuzczcdt0(W2), W0))) <=> aElementOf0(W2, W1)))))))) | (~((W1 = slbdtrb0(W0)) | (~aSet0(W1)) | (((~aElementOf0(tptp_fun_W2_8(W1, W0), szNzAzT0)) | (~sdtlseqdt0(szszuzczcdt0(tptp_fun_W2_8(W1, W0)), W0))) <=> aElementOf0(tptp_fun_W2_8(W1, W0), W1))))))) <=> ![W0: $i] : ((~aElementOf0(W0, szNzAzT0)) | ![W1: $i] : (~((~((~(W1 = slbdtrb0(W0))) | (~((~aSet0(W1)) | (~![W2: $i] : (~(((~aElementOf0(W2, szNzAzT0)) | (~sdtlseqdt0(szszuzczcdt0(W2), W0))) <=> aElementOf0(W2, W1)))))))) | (~((W1 = slbdtrb0(W0)) | (~aSet0(W1)) | (((~aElementOf0(tptp_fun_W2_8(W1, W0), szNzAzT0)) | (~sdtlseqdt0(szszuzczcdt0(tptp_fun_W2_8(W1, W0)), W0))) <=> aElementOf0(tptp_fun_W2_8(W1, W0), W1)))))))),
% 94.91/95.20 inference(transitivity,[status(thm)],[62, 60])).
% 94.91/95.20 tff(64,plain,
% 94.91/95.20 (^[W0: $i] : rewrite(((~aElementOf0(W0, szNzAzT0)) | ![W1: $i] : (((~(W1 = slbdtrb0(W0))) | (aSet0(W1) & ![W2: $i] : (aElementOf0(W2, W1) <=> (aElementOf0(W2, szNzAzT0) & sdtlseqdt0(szszuzczcdt0(W2), W0))))) & ((W1 = slbdtrb0(W0)) | (~aSet0(W1)) | (~(aElementOf0(tptp_fun_W2_8(W1, W0), W1) <=> (aElementOf0(tptp_fun_W2_8(W1, W0), szNzAzT0) & sdtlseqdt0(szszuzczcdt0(tptp_fun_W2_8(W1, W0)), W0))))))) <=> ((~aElementOf0(W0, szNzAzT0)) | ![W1: $i] : (~((~((~(W1 = slbdtrb0(W0))) | (~((~aSet0(W1)) | (~![W2: $i] : (~(((~aElementOf0(W2, szNzAzT0)) | (~sdtlseqdt0(szszuzczcdt0(W2), W0))) <=> aElementOf0(W2, W1)))))))) | (~((W1 = slbdtrb0(W0)) | (~aSet0(W1)) | (((~aElementOf0(tptp_fun_W2_8(W1, W0), szNzAzT0)) | (~sdtlseqdt0(szszuzczcdt0(tptp_fun_W2_8(W1, W0)), W0))) <=> aElementOf0(tptp_fun_W2_8(W1, W0), W1))))))))),
% 94.91/95.20 inference(bind,[status(th)],[])).
% 94.91/95.20 tff(65,plain,
% 94.91/95.20 (![W0: $i] : ((~aElementOf0(W0, szNzAzT0)) | ![W1: $i] : (((~(W1 = slbdtrb0(W0))) | (aSet0(W1) & ![W2: $i] : (aElementOf0(W2, W1) <=> (aElementOf0(W2, szNzAzT0) & sdtlseqdt0(szszuzczcdt0(W2), W0))))) & ((W1 = slbdtrb0(W0)) | (~aSet0(W1)) | (~(aElementOf0(tptp_fun_W2_8(W1, W0), W1) <=> (aElementOf0(tptp_fun_W2_8(W1, W0), szNzAzT0) & sdtlseqdt0(szszuzczcdt0(tptp_fun_W2_8(W1, W0)), W0))))))) <=> ![W0: $i] : ((~aElementOf0(W0, szNzAzT0)) | ![W1: $i] : (~((~((~(W1 = slbdtrb0(W0))) | (~((~aSet0(W1)) | (~![W2: $i] : (~(((~aElementOf0(W2, szNzAzT0)) | (~sdtlseqdt0(szszuzczcdt0(W2), W0))) <=> aElementOf0(W2, W1)))))))) | (~((W1 = slbdtrb0(W0)) | (~aSet0(W1)) | (((~aElementOf0(tptp_fun_W2_8(W1, W0), szNzAzT0)) | (~sdtlseqdt0(szszuzczcdt0(tptp_fun_W2_8(W1, W0)), W0))) <=> aElementOf0(tptp_fun_W2_8(W1, W0), W1)))))))),
% 94.91/95.20 inference(quant_intro,[status(thm)],[64])).
% 94.91/95.20 tff(66,plain,
% 94.91/95.20 (^[W0: $i] : rewrite(((~aElementOf0(W0, szNzAzT0)) | ![W1: $i] : (((~(W1 = slbdtrb0(W0))) | (aSet0(W1) & ![W2: $i] : (aElementOf0(W2, W1) <=> (aElementOf0(W2, szNzAzT0) & sdtlseqdt0(szszuzczcdt0(W2), W0))))) & ((W1 = slbdtrb0(W0)) | ((~aSet0(W1)) | (~(aElementOf0(tptp_fun_W2_8(W1, W0), W1) <=> (aElementOf0(tptp_fun_W2_8(W1, W0), szNzAzT0) & sdtlseqdt0(szszuzczcdt0(tptp_fun_W2_8(W1, W0)), W0)))))))) <=> ((~aElementOf0(W0, szNzAzT0)) | ![W1: $i] : (((~(W1 = slbdtrb0(W0))) | (aSet0(W1) & ![W2: $i] : (aElementOf0(W2, W1) <=> (aElementOf0(W2, szNzAzT0) & sdtlseqdt0(szszuzczcdt0(W2), W0))))) & ((W1 = slbdtrb0(W0)) | (~aSet0(W1)) | (~(aElementOf0(tptp_fun_W2_8(W1, W0), W1) <=> (aElementOf0(tptp_fun_W2_8(W1, W0), szNzAzT0) & sdtlseqdt0(szszuzczcdt0(tptp_fun_W2_8(W1, W0)), W0))))))))),
% 94.91/95.20 inference(bind,[status(th)],[])).
% 94.91/95.20 tff(67,plain,
% 94.91/95.20 (![W0: $i] : ((~aElementOf0(W0, szNzAzT0)) | ![W1: $i] : (((~(W1 = slbdtrb0(W0))) | (aSet0(W1) & ![W2: $i] : (aElementOf0(W2, W1) <=> (aElementOf0(W2, szNzAzT0) & sdtlseqdt0(szszuzczcdt0(W2), W0))))) & ((W1 = slbdtrb0(W0)) | ((~aSet0(W1)) | (~(aElementOf0(tptp_fun_W2_8(W1, W0), W1) <=> (aElementOf0(tptp_fun_W2_8(W1, W0), szNzAzT0) & sdtlseqdt0(szszuzczcdt0(tptp_fun_W2_8(W1, W0)), W0)))))))) <=> ![W0: $i] : ((~aElementOf0(W0, szNzAzT0)) | ![W1: $i] : (((~(W1 = slbdtrb0(W0))) | (aSet0(W1) & ![W2: $i] : (aElementOf0(W2, W1) <=> (aElementOf0(W2, szNzAzT0) & sdtlseqdt0(szszuzczcdt0(W2), W0))))) & ((W1 = slbdtrb0(W0)) | (~aSet0(W1)) | (~(aElementOf0(tptp_fun_W2_8(W1, W0), W1) <=> (aElementOf0(tptp_fun_W2_8(W1, W0), szNzAzT0) & sdtlseqdt0(szszuzczcdt0(tptp_fun_W2_8(W1, W0)), W0)))))))),
% 94.91/95.20 inference(quant_intro,[status(thm)],[66])).
% 94.91/95.20 tff(68,plain,
% 94.91/95.20 (![W0: $i] : ((~aElementOf0(W0, szNzAzT0)) | ![W1: $i] : ((W1 = slbdtrb0(W0)) <=> (aSet0(W1) & ![W2: $i] : (aElementOf0(W2, W1) <=> (aElementOf0(W2, szNzAzT0) & sdtlseqdt0(szszuzczcdt0(W2), W0)))))) <=> ![W0: $i] : ((~aElementOf0(W0, szNzAzT0)) | ![W1: $i] : ((W1 = slbdtrb0(W0)) <=> (aSet0(W1) & ![W2: $i] : (aElementOf0(W2, W1) <=> (aElementOf0(W2, szNzAzT0) & sdtlseqdt0(szszuzczcdt0(W2), W0))))))),
% 94.91/95.20 inference(rewrite,[status(thm)],[])).
% 94.91/95.20 tff(69,plain,
% 94.91/95.20 (^[W0: $i] : rewrite((aElementOf0(W0, szNzAzT0) => ![W1: $i] : ((W1 = slbdtrb0(W0)) <=> (aSet0(W1) & ![W2: $i] : (aElementOf0(W2, W1) <=> (aElementOf0(W2, szNzAzT0) & sdtlseqdt0(szszuzczcdt0(W2), W0)))))) <=> ((~aElementOf0(W0, szNzAzT0)) | ![W1: $i] : ((W1 = slbdtrb0(W0)) <=> (aSet0(W1) & ![W2: $i] : (aElementOf0(W2, W1) <=> (aElementOf0(W2, szNzAzT0) & sdtlseqdt0(szszuzczcdt0(W2), W0)))))))),
% 94.91/95.20 inference(bind,[status(th)],[])).
% 94.91/95.20 tff(70,plain,
% 94.91/95.20 (![W0: $i] : (aElementOf0(W0, szNzAzT0) => ![W1: $i] : ((W1 = slbdtrb0(W0)) <=> (aSet0(W1) & ![W2: $i] : (aElementOf0(W2, W1) <=> (aElementOf0(W2, szNzAzT0) & sdtlseqdt0(szszuzczcdt0(W2), W0)))))) <=> ![W0: $i] : ((~aElementOf0(W0, szNzAzT0)) | ![W1: $i] : ((W1 = slbdtrb0(W0)) <=> (aSet0(W1) & ![W2: $i] : (aElementOf0(W2, W1) <=> (aElementOf0(W2, szNzAzT0) & sdtlseqdt0(szszuzczcdt0(W2), W0))))))),
% 94.91/95.20 inference(quant_intro,[status(thm)],[69])).
% 94.91/95.20 tff(71,axiom,(![W0: $i] : (aElementOf0(W0, szNzAzT0) => ![W1: $i] : ((W1 = slbdtrb0(W0)) <=> (aSet0(W1) & ![W2: $i] : (aElementOf0(W2, W1) <=> (aElementOf0(W2, szNzAzT0) & sdtlseqdt0(szszuzczcdt0(W2), W0))))))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','mDefSeg')).
% 94.91/95.20 tff(72,plain,
% 94.91/95.20 (![W0: $i] : ((~aElementOf0(W0, szNzAzT0)) | ![W1: $i] : ((W1 = slbdtrb0(W0)) <=> (aSet0(W1) & ![W2: $i] : (aElementOf0(W2, W1) <=> (aElementOf0(W2, szNzAzT0) & sdtlseqdt0(szszuzczcdt0(W2), W0))))))),
% 94.91/95.20 inference(modus_ponens,[status(thm)],[71, 70])).
% 94.91/95.20 tff(73,plain,
% 94.91/95.20 (![W0: $i] : ((~aElementOf0(W0, szNzAzT0)) | ![W1: $i] : ((W1 = slbdtrb0(W0)) <=> (aSet0(W1) & ![W2: $i] : (aElementOf0(W2, W1) <=> (aElementOf0(W2, szNzAzT0) & sdtlseqdt0(szszuzczcdt0(W2), W0))))))),
% 94.91/95.20 inference(modus_ponens,[status(thm)],[72, 68])).
% 94.91/95.20 tff(74,plain,(
% 94.91/95.20 ![W0: $i] : ((~aElementOf0(W0, szNzAzT0)) | ![W1: $i] : (((~(W1 = slbdtrb0(W0))) | (aSet0(W1) & ![W2: $i] : (aElementOf0(W2, W1) <=> (aElementOf0(W2, szNzAzT0) & sdtlseqdt0(szszuzczcdt0(W2), W0))))) & ((W1 = slbdtrb0(W0)) | ((~aSet0(W1)) | (~(aElementOf0(tptp_fun_W2_8(W1, W0), W1) <=> (aElementOf0(tptp_fun_W2_8(W1, W0), szNzAzT0) & sdtlseqdt0(szszuzczcdt0(tptp_fun_W2_8(W1, W0)), W0))))))))),
% 94.91/95.20 inference(skolemize,[status(sab)],[73])).
% 94.91/95.20 tff(75,plain,
% 94.91/95.20 (![W0: $i] : ((~aElementOf0(W0, szNzAzT0)) | ![W1: $i] : (((~(W1 = slbdtrb0(W0))) | (aSet0(W1) & ![W2: $i] : (aElementOf0(W2, W1) <=> (aElementOf0(W2, szNzAzT0) & sdtlseqdt0(szszuzczcdt0(W2), W0))))) & ((W1 = slbdtrb0(W0)) | (~aSet0(W1)) | (~(aElementOf0(tptp_fun_W2_8(W1, W0), W1) <=> (aElementOf0(tptp_fun_W2_8(W1, W0), szNzAzT0) & sdtlseqdt0(szszuzczcdt0(tptp_fun_W2_8(W1, W0)), W0)))))))),
% 94.91/95.20 inference(modus_ponens,[status(thm)],[74, 67])).
% 94.91/95.20 tff(76,plain,
% 94.91/95.20 (![W0: $i] : ((~aElementOf0(W0, szNzAzT0)) | ![W1: $i] : (~((~((~(W1 = slbdtrb0(W0))) | (~((~aSet0(W1)) | (~![W2: $i] : (~(((~aElementOf0(W2, szNzAzT0)) | (~sdtlseqdt0(szszuzczcdt0(W2), W0))) <=> aElementOf0(W2, W1)))))))) | (~((W1 = slbdtrb0(W0)) | (~aSet0(W1)) | (((~aElementOf0(tptp_fun_W2_8(W1, W0), szNzAzT0)) | (~sdtlseqdt0(szszuzczcdt0(tptp_fun_W2_8(W1, W0)), W0))) <=> aElementOf0(tptp_fun_W2_8(W1, W0), W1)))))))),
% 94.91/95.20 inference(modus_ponens,[status(thm)],[75, 65])).
% 94.91/95.20 tff(77,plain,
% 94.91/95.20 (![W0: $i] : ((~aElementOf0(W0, szNzAzT0)) | ![W1: $i] : (~((~((~(W1 = slbdtrb0(W0))) | (~((~aSet0(W1)) | (~![W2: $i] : (~(((~aElementOf0(W2, szNzAzT0)) | (~sdtlseqdt0(szszuzczcdt0(W2), W0))) <=> aElementOf0(W2, W1)))))))) | (~((W1 = slbdtrb0(W0)) | (~aSet0(W1)) | (((~aElementOf0(tptp_fun_W2_8(W1, W0), szNzAzT0)) | (~sdtlseqdt0(szszuzczcdt0(tptp_fun_W2_8(W1, W0)), W0))) <=> aElementOf0(tptp_fun_W2_8(W1, W0), W1)))))))),
% 94.91/95.20 inference(modus_ponens,[status(thm)],[76, 63])).
% 94.91/95.20 tff(78,plain,
% 94.91/95.20 (![W0: $i] : ((~aElementOf0(W0, szNzAzT0)) | ![W1: $i] : (~((~((W1 = slbdtrb0(W0)) | (~aSet0(W1)) | (((~aElementOf0(tptp_fun_W2_8(W1, W0), szNzAzT0)) | (~sdtlseqdt0(szszuzczcdt0(tptp_fun_W2_8(W1, W0)), W0))) <=> aElementOf0(tptp_fun_W2_8(W1, W0), W1)))) | (~((~(W1 = slbdtrb0(W0))) | (~((~aSet0(W1)) | (~![W2: $i] : (~(((~aElementOf0(W2, szNzAzT0)) | (~sdtlseqdt0(szszuzczcdt0(W2), W0))) <=> aElementOf0(W2, W1)))))))))))),
% 94.91/95.20 inference(modus_ponens,[status(thm)],[77, 58])).
% 94.91/95.20 tff(79,plain,
% 94.91/95.20 (((~![W0: $i] : ((~aElementOf0(W0, szNzAzT0)) | ![W1: $i] : (~((~((W1 = slbdtrb0(W0)) | (~aSet0(W1)) | (((~aElementOf0(tptp_fun_W2_8(W1, W0), szNzAzT0)) | (~sdtlseqdt0(szszuzczcdt0(tptp_fun_W2_8(W1, W0)), W0))) <=> aElementOf0(tptp_fun_W2_8(W1, W0), W1)))) | (~((~(W1 = slbdtrb0(W0))) | (~((~aSet0(W1)) | (~![W2: $i] : (~(((~aElementOf0(W2, szNzAzT0)) | (~sdtlseqdt0(szszuzczcdt0(W2), W0))) <=> aElementOf0(W2, W1)))))))))))) | ((~aElementOf0(sbrdtbr0(slcrc0), szNzAzT0)) | ![W1: $i] : (~((~((~aSet0(W1)) | (W1 = slbdtrb0(sbrdtbr0(slcrc0))) | (((~aElementOf0(tptp_fun_W2_8(W1, sbrdtbr0(slcrc0)), szNzAzT0)) | (~sdtlseqdt0(szszuzczcdt0(tptp_fun_W2_8(W1, sbrdtbr0(slcrc0))), sbrdtbr0(slcrc0)))) <=> aElementOf0(tptp_fun_W2_8(W1, sbrdtbr0(slcrc0)), W1)))) | (~((~(W1 = slbdtrb0(sbrdtbr0(slcrc0)))) | (~((~aSet0(W1)) | (~![W2: $i] : (~(((~aElementOf0(W2, szNzAzT0)) | (~sdtlseqdt0(szszuzczcdt0(W2), sbrdtbr0(slcrc0)))) <=> aElementOf0(W2, W1)))))))))))) <=> ((~![W0: $i] : ((~aElementOf0(W0, szNzAzT0)) | ![W1: $i] : (~((~((W1 = slbdtrb0(W0)) | (~aSet0(W1)) | (((~aElementOf0(tptp_fun_W2_8(W1, W0), szNzAzT0)) | (~sdtlseqdt0(szszuzczcdt0(tptp_fun_W2_8(W1, W0)), W0))) <=> aElementOf0(tptp_fun_W2_8(W1, W0), W1)))) | (~((~(W1 = slbdtrb0(W0))) | (~((~aSet0(W1)) | (~![W2: $i] : (~(((~aElementOf0(W2, szNzAzT0)) | (~sdtlseqdt0(szszuzczcdt0(W2), W0))) <=> aElementOf0(W2, W1)))))))))))) | (~aElementOf0(sbrdtbr0(slcrc0), szNzAzT0)) | ![W1: $i] : (~((~((~aSet0(W1)) | (W1 = slbdtrb0(sbrdtbr0(slcrc0))) | (((~aElementOf0(tptp_fun_W2_8(W1, sbrdtbr0(slcrc0)), szNzAzT0)) | (~sdtlseqdt0(szszuzczcdt0(tptp_fun_W2_8(W1, sbrdtbr0(slcrc0))), sbrdtbr0(slcrc0)))) <=> aElementOf0(tptp_fun_W2_8(W1, sbrdtbr0(slcrc0)), W1)))) | (~((~(W1 = slbdtrb0(sbrdtbr0(slcrc0)))) | (~((~aSet0(W1)) | (~![W2: $i] : (~(((~aElementOf0(W2, szNzAzT0)) | (~sdtlseqdt0(szszuzczcdt0(W2), sbrdtbr0(slcrc0)))) <=> aElementOf0(W2, W1)))))))))))),
% 94.91/95.20 inference(rewrite,[status(thm)],[])).
% 94.91/95.20 tff(80,plain,
% 94.91/95.20 (((~aElementOf0(sbrdtbr0(slcrc0), szNzAzT0)) | ![W1: $i] : (~((~((W1 = slbdtrb0(sbrdtbr0(slcrc0))) | (~aSet0(W1)) | (((~aElementOf0(tptp_fun_W2_8(W1, sbrdtbr0(slcrc0)), szNzAzT0)) | (~sdtlseqdt0(szszuzczcdt0(tptp_fun_W2_8(W1, sbrdtbr0(slcrc0))), sbrdtbr0(slcrc0)))) <=> aElementOf0(tptp_fun_W2_8(W1, sbrdtbr0(slcrc0)), W1)))) | (~((~(W1 = slbdtrb0(sbrdtbr0(slcrc0)))) | (~((~aSet0(W1)) | (~![W2: $i] : (~(((~aElementOf0(W2, szNzAzT0)) | (~sdtlseqdt0(szszuzczcdt0(W2), sbrdtbr0(slcrc0)))) <=> aElementOf0(W2, W1))))))))))) <=> ((~aElementOf0(sbrdtbr0(slcrc0), szNzAzT0)) | ![W1: $i] : (~((~((~aSet0(W1)) | (W1 = slbdtrb0(sbrdtbr0(slcrc0))) | (((~aElementOf0(tptp_fun_W2_8(W1, sbrdtbr0(slcrc0)), szNzAzT0)) | (~sdtlseqdt0(szszuzczcdt0(tptp_fun_W2_8(W1, sbrdtbr0(slcrc0))), sbrdtbr0(slcrc0)))) <=> aElementOf0(tptp_fun_W2_8(W1, sbrdtbr0(slcrc0)), W1)))) | (~((~(W1 = slbdtrb0(sbrdtbr0(slcrc0)))) | (~((~aSet0(W1)) | (~![W2: $i] : (~(((~aElementOf0(W2, szNzAzT0)) | (~sdtlseqdt0(szszuzczcdt0(W2), sbrdtbr0(slcrc0)))) <=> aElementOf0(W2, W1)))))))))))),
% 94.91/95.20 inference(rewrite,[status(thm)],[])).
% 94.91/95.20 tff(81,plain,
% 94.91/95.20 (((~![W0: $i] : ((~aElementOf0(W0, szNzAzT0)) | ![W1: $i] : (~((~((W1 = slbdtrb0(W0)) | (~aSet0(W1)) | (((~aElementOf0(tptp_fun_W2_8(W1, W0), szNzAzT0)) | (~sdtlseqdt0(szszuzczcdt0(tptp_fun_W2_8(W1, W0)), W0))) <=> aElementOf0(tptp_fun_W2_8(W1, W0), W1)))) | (~((~(W1 = slbdtrb0(W0))) | (~((~aSet0(W1)) | (~![W2: $i] : (~(((~aElementOf0(W2, szNzAzT0)) | (~sdtlseqdt0(szszuzczcdt0(W2), W0))) <=> aElementOf0(W2, W1)))))))))))) | ((~aElementOf0(sbrdtbr0(slcrc0), szNzAzT0)) | ![W1: $i] : (~((~((W1 = slbdtrb0(sbrdtbr0(slcrc0))) | (~aSet0(W1)) | (((~aElementOf0(tptp_fun_W2_8(W1, sbrdtbr0(slcrc0)), szNzAzT0)) | (~sdtlseqdt0(szszuzczcdt0(tptp_fun_W2_8(W1, sbrdtbr0(slcrc0))), sbrdtbr0(slcrc0)))) <=> aElementOf0(tptp_fun_W2_8(W1, sbrdtbr0(slcrc0)), W1)))) | (~((~(W1 = slbdtrb0(sbrdtbr0(slcrc0)))) | (~((~aSet0(W1)) | (~![W2: $i] : (~(((~aElementOf0(W2, szNzAzT0)) | (~sdtlseqdt0(szszuzczcdt0(W2), sbrdtbr0(slcrc0)))) <=> aElementOf0(W2, W1)))))))))))) <=> ((~![W0: $i] : ((~aElementOf0(W0, szNzAzT0)) | ![W1: $i] : (~((~((W1 = slbdtrb0(W0)) | (~aSet0(W1)) | (((~aElementOf0(tptp_fun_W2_8(W1, W0), szNzAzT0)) | (~sdtlseqdt0(szszuzczcdt0(tptp_fun_W2_8(W1, W0)), W0))) <=> aElementOf0(tptp_fun_W2_8(W1, W0), W1)))) | (~((~(W1 = slbdtrb0(W0))) | (~((~aSet0(W1)) | (~![W2: $i] : (~(((~aElementOf0(W2, szNzAzT0)) | (~sdtlseqdt0(szszuzczcdt0(W2), W0))) <=> aElementOf0(W2, W1)))))))))))) | ((~aElementOf0(sbrdtbr0(slcrc0), szNzAzT0)) | ![W1: $i] : (~((~((~aSet0(W1)) | (W1 = slbdtrb0(sbrdtbr0(slcrc0))) | (((~aElementOf0(tptp_fun_W2_8(W1, sbrdtbr0(slcrc0)), szNzAzT0)) | (~sdtlseqdt0(szszuzczcdt0(tptp_fun_W2_8(W1, sbrdtbr0(slcrc0))), sbrdtbr0(slcrc0)))) <=> aElementOf0(tptp_fun_W2_8(W1, sbrdtbr0(slcrc0)), W1)))) | (~((~(W1 = slbdtrb0(sbrdtbr0(slcrc0)))) | (~((~aSet0(W1)) | (~![W2: $i] : (~(((~aElementOf0(W2, szNzAzT0)) | (~sdtlseqdt0(szszuzczcdt0(W2), sbrdtbr0(slcrc0)))) <=> aElementOf0(W2, W1))))))))))))),
% 94.91/95.20 inference(monotonicity,[status(thm)],[80])).
% 94.91/95.20 tff(82,plain,
% 94.91/95.20 (((~![W0: $i] : ((~aElementOf0(W0, szNzAzT0)) | ![W1: $i] : (~((~((W1 = slbdtrb0(W0)) | (~aSet0(W1)) | (((~aElementOf0(tptp_fun_W2_8(W1, W0), szNzAzT0)) | (~sdtlseqdt0(szszuzczcdt0(tptp_fun_W2_8(W1, W0)), W0))) <=> aElementOf0(tptp_fun_W2_8(W1, W0), W1)))) | (~((~(W1 = slbdtrb0(W0))) | (~((~aSet0(W1)) | (~![W2: $i] : (~(((~aElementOf0(W2, szNzAzT0)) | (~sdtlseqdt0(szszuzczcdt0(W2), W0))) <=> aElementOf0(W2, W1)))))))))))) | ((~aElementOf0(sbrdtbr0(slcrc0), szNzAzT0)) | ![W1: $i] : (~((~((W1 = slbdtrb0(sbrdtbr0(slcrc0))) | (~aSet0(W1)) | (((~aElementOf0(tptp_fun_W2_8(W1, sbrdtbr0(slcrc0)), szNzAzT0)) | (~sdtlseqdt0(szszuzczcdt0(tptp_fun_W2_8(W1, sbrdtbr0(slcrc0))), sbrdtbr0(slcrc0)))) <=> aElementOf0(tptp_fun_W2_8(W1, sbrdtbr0(slcrc0)), W1)))) | (~((~(W1 = slbdtrb0(sbrdtbr0(slcrc0)))) | (~((~aSet0(W1)) | (~![W2: $i] : (~(((~aElementOf0(W2, szNzAzT0)) | (~sdtlseqdt0(szszuzczcdt0(W2), sbrdtbr0(slcrc0)))) <=> aElementOf0(W2, W1)))))))))))) <=> ((~![W0: $i] : ((~aElementOf0(W0, szNzAzT0)) | ![W1: $i] : (~((~((W1 = slbdtrb0(W0)) | (~aSet0(W1)) | (((~aElementOf0(tptp_fun_W2_8(W1, W0), szNzAzT0)) | (~sdtlseqdt0(szszuzczcdt0(tptp_fun_W2_8(W1, W0)), W0))) <=> aElementOf0(tptp_fun_W2_8(W1, W0), W1)))) | (~((~(W1 = slbdtrb0(W0))) | (~((~aSet0(W1)) | (~![W2: $i] : (~(((~aElementOf0(W2, szNzAzT0)) | (~sdtlseqdt0(szszuzczcdt0(W2), W0))) <=> aElementOf0(W2, W1)))))))))))) | (~aElementOf0(sbrdtbr0(slcrc0), szNzAzT0)) | ![W1: $i] : (~((~((~aSet0(W1)) | (W1 = slbdtrb0(sbrdtbr0(slcrc0))) | (((~aElementOf0(tptp_fun_W2_8(W1, sbrdtbr0(slcrc0)), szNzAzT0)) | (~sdtlseqdt0(szszuzczcdt0(tptp_fun_W2_8(W1, sbrdtbr0(slcrc0))), sbrdtbr0(slcrc0)))) <=> aElementOf0(tptp_fun_W2_8(W1, sbrdtbr0(slcrc0)), W1)))) | (~((~(W1 = slbdtrb0(sbrdtbr0(slcrc0)))) | (~((~aSet0(W1)) | (~![W2: $i] : (~(((~aElementOf0(W2, szNzAzT0)) | (~sdtlseqdt0(szszuzczcdt0(W2), sbrdtbr0(slcrc0)))) <=> aElementOf0(W2, W1)))))))))))),
% 94.91/95.20 inference(transitivity,[status(thm)],[81, 79])).
% 94.91/95.20 tff(83,plain,
% 94.91/95.20 ((~![W0: $i] : ((~aElementOf0(W0, szNzAzT0)) | ![W1: $i] : (~((~((W1 = slbdtrb0(W0)) | (~aSet0(W1)) | (((~aElementOf0(tptp_fun_W2_8(W1, W0), szNzAzT0)) | (~sdtlseqdt0(szszuzczcdt0(tptp_fun_W2_8(W1, W0)), W0))) <=> aElementOf0(tptp_fun_W2_8(W1, W0), W1)))) | (~((~(W1 = slbdtrb0(W0))) | (~((~aSet0(W1)) | (~![W2: $i] : (~(((~aElementOf0(W2, szNzAzT0)) | (~sdtlseqdt0(szszuzczcdt0(W2), W0))) <=> aElementOf0(W2, W1)))))))))))) | ((~aElementOf0(sbrdtbr0(slcrc0), szNzAzT0)) | ![W1: $i] : (~((~((W1 = slbdtrb0(sbrdtbr0(slcrc0))) | (~aSet0(W1)) | (((~aElementOf0(tptp_fun_W2_8(W1, sbrdtbr0(slcrc0)), szNzAzT0)) | (~sdtlseqdt0(szszuzczcdt0(tptp_fun_W2_8(W1, sbrdtbr0(slcrc0))), sbrdtbr0(slcrc0)))) <=> aElementOf0(tptp_fun_W2_8(W1, sbrdtbr0(slcrc0)), W1)))) | (~((~(W1 = slbdtrb0(sbrdtbr0(slcrc0)))) | (~((~aSet0(W1)) | (~![W2: $i] : (~(((~aElementOf0(W2, szNzAzT0)) | (~sdtlseqdt0(szszuzczcdt0(W2), sbrdtbr0(slcrc0)))) <=> aElementOf0(W2, W1)))))))))))),
% 94.91/95.20 inference(quant_inst,[status(thm)],[])).
% 94.91/95.20 tff(84,plain,
% 94.91/95.20 ((~![W0: $i] : ((~aElementOf0(W0, szNzAzT0)) | ![W1: $i] : (~((~((W1 = slbdtrb0(W0)) | (~aSet0(W1)) | (((~aElementOf0(tptp_fun_W2_8(W1, W0), szNzAzT0)) | (~sdtlseqdt0(szszuzczcdt0(tptp_fun_W2_8(W1, W0)), W0))) <=> aElementOf0(tptp_fun_W2_8(W1, W0), W1)))) | (~((~(W1 = slbdtrb0(W0))) | (~((~aSet0(W1)) | (~![W2: $i] : (~(((~aElementOf0(W2, szNzAzT0)) | (~sdtlseqdt0(szszuzczcdt0(W2), W0))) <=> aElementOf0(W2, W1)))))))))))) | (~aElementOf0(sbrdtbr0(slcrc0), szNzAzT0)) | ![W1: $i] : (~((~((~aSet0(W1)) | (W1 = slbdtrb0(sbrdtbr0(slcrc0))) | (((~aElementOf0(tptp_fun_W2_8(W1, sbrdtbr0(slcrc0)), szNzAzT0)) | (~sdtlseqdt0(szszuzczcdt0(tptp_fun_W2_8(W1, sbrdtbr0(slcrc0))), sbrdtbr0(slcrc0)))) <=> aElementOf0(tptp_fun_W2_8(W1, sbrdtbr0(slcrc0)), W1)))) | (~((~(W1 = slbdtrb0(sbrdtbr0(slcrc0)))) | (~((~aSet0(W1)) | (~![W2: $i] : (~(((~aElementOf0(W2, szNzAzT0)) | (~sdtlseqdt0(szszuzczcdt0(W2), sbrdtbr0(slcrc0)))) <=> aElementOf0(W2, W1))))))))))),
% 94.91/95.20 inference(modus_ponens,[status(thm)],[83, 82])).
% 94.91/95.20 tff(85,plain,
% 94.91/95.20 (![W1: $i] : (~((~((~aSet0(W1)) | (W1 = slbdtrb0(sbrdtbr0(slcrc0))) | (((~aElementOf0(tptp_fun_W2_8(W1, sbrdtbr0(slcrc0)), szNzAzT0)) | (~sdtlseqdt0(szszuzczcdt0(tptp_fun_W2_8(W1, sbrdtbr0(slcrc0))), sbrdtbr0(slcrc0)))) <=> aElementOf0(tptp_fun_W2_8(W1, sbrdtbr0(slcrc0)), W1)))) | (~((~(W1 = slbdtrb0(sbrdtbr0(slcrc0)))) | (~((~aSet0(W1)) | (~![W2: $i] : (~(((~aElementOf0(W2, szNzAzT0)) | (~sdtlseqdt0(szszuzczcdt0(W2), sbrdtbr0(slcrc0)))) <=> aElementOf0(W2, W1))))))))))),
% 94.91/95.20 inference(unit_resolution,[status(thm)],[84, 78, 56])).
% 94.91/95.20 tff(86,plain,
% 94.91/95.20 ((~![W1: $i] : (~((~((~aSet0(W1)) | (W1 = slbdtrb0(sbrdtbr0(slcrc0))) | (((~aElementOf0(tptp_fun_W2_8(W1, sbrdtbr0(slcrc0)), szNzAzT0)) | (~sdtlseqdt0(szszuzczcdt0(tptp_fun_W2_8(W1, sbrdtbr0(slcrc0))), sbrdtbr0(slcrc0)))) <=> aElementOf0(tptp_fun_W2_8(W1, sbrdtbr0(slcrc0)), W1)))) | (~((~(W1 = slbdtrb0(sbrdtbr0(slcrc0)))) | (~((~aSet0(W1)) | (~![W2: $i] : (~(((~aElementOf0(W2, szNzAzT0)) | (~sdtlseqdt0(szszuzczcdt0(W2), sbrdtbr0(slcrc0)))) <=> aElementOf0(W2, W1))))))))))) | (~((~((~aSet0(slbdtrb0(tptp_fun_W1_4(szszuzczcdt0(sz00))))) | (slbdtrb0(tptp_fun_W1_4(szszuzczcdt0(sz00))) = slbdtrb0(sbrdtbr0(slcrc0))) | (((~aElementOf0(tptp_fun_W2_8(slbdtrb0(tptp_fun_W1_4(szszuzczcdt0(sz00))), sbrdtbr0(slcrc0)), szNzAzT0)) | (~sdtlseqdt0(szszuzczcdt0(tptp_fun_W2_8(slbdtrb0(tptp_fun_W1_4(szszuzczcdt0(sz00))), sbrdtbr0(slcrc0))), sbrdtbr0(slcrc0)))) <=> aElementOf0(tptp_fun_W2_8(slbdtrb0(tptp_fun_W1_4(szszuzczcdt0(sz00))), sbrdtbr0(slcrc0)), slbdtrb0(tptp_fun_W1_4(szszuzczcdt0(sz00))))))) | (~((~(slbdtrb0(tptp_fun_W1_4(szszuzczcdt0(sz00))) = slbdtrb0(sbrdtbr0(slcrc0)))) | (~((~aSet0(slbdtrb0(tptp_fun_W1_4(szszuzczcdt0(sz00))))) | (~![W2: $i] : (~(((~aElementOf0(W2, szNzAzT0)) | (~sdtlseqdt0(szszuzczcdt0(W2), sbrdtbr0(slcrc0)))) <=> aElementOf0(W2, slbdtrb0(tptp_fun_W1_4(szszuzczcdt0(sz00)))))))))))))),
% 94.91/95.20 inference(quant_inst,[status(thm)],[])).
% 94.91/95.20 tff(87,plain,
% 94.91/95.20 ($false),
% 94.91/95.20 inference(unit_resolution,[status(thm)],[86, 85, 24])).
% 94.91/95.20 tff(88,plain,(~((~((~aSet0(slbdtrb0(tptp_fun_W1_4(szszuzczcdt0(sz00))))) | (slbdtrb0(tptp_fun_W1_4(szszuzczcdt0(sz00))) = slbdtrb0(sbrdtbr0(slcrc0))) | (((~aElementOf0(tptp_fun_W2_8(slbdtrb0(tptp_fun_W1_4(szszuzczcdt0(sz00))), sbrdtbr0(slcrc0)), szNzAzT0)) | (~sdtlseqdt0(szszuzczcdt0(tptp_fun_W2_8(slbdtrb0(tptp_fun_W1_4(szszuzczcdt0(sz00))), sbrdtbr0(slcrc0))), sbrdtbr0(slcrc0)))) <=> aElementOf0(tptp_fun_W2_8(slbdtrb0(tptp_fun_W1_4(szszuzczcdt0(sz00))), sbrdtbr0(slcrc0)), slbdtrb0(tptp_fun_W1_4(szszuzczcdt0(sz00))))))) | (~((~(slbdtrb0(tptp_fun_W1_4(szszuzczcdt0(sz00))) = slbdtrb0(sbrdtbr0(slcrc0)))) | (~((~aSet0(slbdtrb0(tptp_fun_W1_4(szszuzczcdt0(sz00))))) | (~![W2: $i] : (~(((~aElementOf0(W2, szNzAzT0)) | (~sdtlseqdt0(szszuzczcdt0(W2), sbrdtbr0(slcrc0)))) <=> aElementOf0(W2, slbdtrb0(tptp_fun_W1_4(szszuzczcdt0(sz00))))))))))))), inference(lemma,lemma(discharge,[]))).
% 94.91/95.20 tff(89,plain,
% 94.91/95.20 (((~((~aSet0(slbdtrb0(tptp_fun_W1_4(szszuzczcdt0(sz00))))) | (slbdtrb0(tptp_fun_W1_4(szszuzczcdt0(sz00))) = slbdtrb0(sbrdtbr0(slcrc0))) | (((~aElementOf0(tptp_fun_W2_8(slbdtrb0(tptp_fun_W1_4(szszuzczcdt0(sz00))), sbrdtbr0(slcrc0)), szNzAzT0)) | (~sdtlseqdt0(szszuzczcdt0(tptp_fun_W2_8(slbdtrb0(tptp_fun_W1_4(szszuzczcdt0(sz00))), sbrdtbr0(slcrc0))), sbrdtbr0(slcrc0)))) <=> aElementOf0(tptp_fun_W2_8(slbdtrb0(tptp_fun_W1_4(szszuzczcdt0(sz00))), sbrdtbr0(slcrc0)), slbdtrb0(tptp_fun_W1_4(szszuzczcdt0(sz00))))))) | (~((~(slbdtrb0(tptp_fun_W1_4(szszuzczcdt0(sz00))) = slbdtrb0(sbrdtbr0(slcrc0)))) | (~((~aSet0(slbdtrb0(tptp_fun_W1_4(szszuzczcdt0(sz00))))) | (~![W2: $i] : (~(((~aElementOf0(W2, szNzAzT0)) | (~sdtlseqdt0(szszuzczcdt0(W2), sbrdtbr0(slcrc0)))) <=> aElementOf0(W2, slbdtrb0(tptp_fun_W1_4(szszuzczcdt0(sz00)))))))))))) | ((~(slbdtrb0(tptp_fun_W1_4(szszuzczcdt0(sz00))) = slbdtrb0(sbrdtbr0(slcrc0)))) | (~((~aSet0(slbdtrb0(tptp_fun_W1_4(szszuzczcdt0(sz00))))) | (~![W2: $i] : (~(((~aElementOf0(W2, szNzAzT0)) | (~sdtlseqdt0(szszuzczcdt0(W2), sbrdtbr0(slcrc0)))) <=> aElementOf0(W2, slbdtrb0(tptp_fun_W1_4(szszuzczcdt0(sz00))))))))))),
% 94.91/95.20 inference(tautology,[status(thm)],[])).
% 94.91/95.20 tff(90,plain,
% 94.91/95.20 ((~(slbdtrb0(tptp_fun_W1_4(szszuzczcdt0(sz00))) = slbdtrb0(sbrdtbr0(slcrc0)))) | (~((~aSet0(slbdtrb0(tptp_fun_W1_4(szszuzczcdt0(sz00))))) | (~![W2: $i] : (~(((~aElementOf0(W2, szNzAzT0)) | (~sdtlseqdt0(szszuzczcdt0(W2), sbrdtbr0(slcrc0)))) <=> aElementOf0(W2, slbdtrb0(tptp_fun_W1_4(szszuzczcdt0(sz00)))))))))),
% 94.91/95.20 inference(unit_resolution,[status(thm)],[89, 88])).
% 94.91/95.20 tff(91,plain,
% 94.91/95.20 (^[W0: $i] : refl(((~aElementOf0(W0, szNzAzT0)) | (~((~aElementOf0(szszuzczcdt0(W0), szNzAzT0)) | (szszuzczcdt0(W0) = sz00)))) <=> ((~aElementOf0(W0, szNzAzT0)) | (~((~aElementOf0(szszuzczcdt0(W0), szNzAzT0)) | (szszuzczcdt0(W0) = sz00)))))),
% 94.91/95.20 inference(bind,[status(th)],[])).
% 94.91/95.20 tff(92,plain,
% 94.91/95.20 (![W0: $i] : ((~aElementOf0(W0, szNzAzT0)) | (~((~aElementOf0(szszuzczcdt0(W0), szNzAzT0)) | (szszuzczcdt0(W0) = sz00)))) <=> ![W0: $i] : ((~aElementOf0(W0, szNzAzT0)) | (~((~aElementOf0(szszuzczcdt0(W0), szNzAzT0)) | (szszuzczcdt0(W0) = sz00))))),
% 94.91/95.20 inference(quant_intro,[status(thm)],[91])).
% 94.91/95.20 tff(93,plain,
% 94.91/95.20 (^[W0: $i] : rewrite(((~aElementOf0(W0, szNzAzT0)) | (aElementOf0(szszuzczcdt0(W0), szNzAzT0) & (~(szszuzczcdt0(W0) = sz00)))) <=> ((~aElementOf0(W0, szNzAzT0)) | (~((~aElementOf0(szszuzczcdt0(W0), szNzAzT0)) | (szszuzczcdt0(W0) = sz00)))))),
% 94.91/95.20 inference(bind,[status(th)],[])).
% 94.91/95.20 tff(94,plain,
% 94.91/95.20 (![W0: $i] : ((~aElementOf0(W0, szNzAzT0)) | (aElementOf0(szszuzczcdt0(W0), szNzAzT0) & (~(szszuzczcdt0(W0) = sz00)))) <=> ![W0: $i] : ((~aElementOf0(W0, szNzAzT0)) | (~((~aElementOf0(szszuzczcdt0(W0), szNzAzT0)) | (szszuzczcdt0(W0) = sz00))))),
% 94.91/95.20 inference(quant_intro,[status(thm)],[93])).
% 94.91/95.20 tff(95,plain,
% 94.91/95.20 (![W0: $i] : ((~aElementOf0(W0, szNzAzT0)) | (aElementOf0(szszuzczcdt0(W0), szNzAzT0) & (~(szszuzczcdt0(W0) = sz00)))) <=> ![W0: $i] : ((~aElementOf0(W0, szNzAzT0)) | (aElementOf0(szszuzczcdt0(W0), szNzAzT0) & (~(szszuzczcdt0(W0) = sz00))))),
% 94.91/95.20 inference(rewrite,[status(thm)],[])).
% 94.91/95.20 tff(96,plain,
% 94.91/95.20 (^[W0: $i] : rewrite((aElementOf0(W0, szNzAzT0) => (aElementOf0(szszuzczcdt0(W0), szNzAzT0) & (~(szszuzczcdt0(W0) = sz00)))) <=> ((~aElementOf0(W0, szNzAzT0)) | (aElementOf0(szszuzczcdt0(W0), szNzAzT0) & (~(szszuzczcdt0(W0) = sz00)))))),
% 94.91/95.20 inference(bind,[status(th)],[])).
% 94.91/95.20 tff(97,plain,
% 94.91/95.20 (![W0: $i] : (aElementOf0(W0, szNzAzT0) => (aElementOf0(szszuzczcdt0(W0), szNzAzT0) & (~(szszuzczcdt0(W0) = sz00)))) <=> ![W0: $i] : ((~aElementOf0(W0, szNzAzT0)) | (aElementOf0(szszuzczcdt0(W0), szNzAzT0) & (~(szszuzczcdt0(W0) = sz00))))),
% 94.91/95.20 inference(quant_intro,[status(thm)],[96])).
% 94.91/95.20 tff(98,axiom,(![W0: $i] : (aElementOf0(W0, szNzAzT0) => (aElementOf0(szszuzczcdt0(W0), szNzAzT0) & (~(szszuzczcdt0(W0) = sz00))))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','mSuccNum')).
% 94.91/95.20 tff(99,plain,
% 94.91/95.20 (![W0: $i] : ((~aElementOf0(W0, szNzAzT0)) | (aElementOf0(szszuzczcdt0(W0), szNzAzT0) & (~(szszuzczcdt0(W0) = sz00))))),
% 94.91/95.20 inference(modus_ponens,[status(thm)],[98, 97])).
% 94.91/95.20 tff(100,plain,
% 94.91/95.20 (![W0: $i] : ((~aElementOf0(W0, szNzAzT0)) | (aElementOf0(szszuzczcdt0(W0), szNzAzT0) & (~(szszuzczcdt0(W0) = sz00))))),
% 94.91/95.21 inference(modus_ponens,[status(thm)],[99, 95])).
% 94.91/95.21 tff(101,plain,(
% 94.91/95.21 ![W0: $i] : ((~aElementOf0(W0, szNzAzT0)) | (aElementOf0(szszuzczcdt0(W0), szNzAzT0) & (~(szszuzczcdt0(W0) = sz00))))),
% 94.91/95.21 inference(skolemize,[status(sab)],[100])).
% 94.91/95.21 tff(102,plain,
% 94.91/95.21 (![W0: $i] : ((~aElementOf0(W0, szNzAzT0)) | (~((~aElementOf0(szszuzczcdt0(W0), szNzAzT0)) | (szszuzczcdt0(W0) = sz00))))),
% 94.91/95.21 inference(modus_ponens,[status(thm)],[101, 94])).
% 94.91/95.21 tff(103,plain,
% 94.91/95.21 (![W0: $i] : ((~aElementOf0(W0, szNzAzT0)) | (~((~aElementOf0(szszuzczcdt0(W0), szNzAzT0)) | (szszuzczcdt0(W0) = sz00))))),
% 94.91/95.21 inference(modus_ponens,[status(thm)],[102, 92])).
% 94.91/95.21 tff(104,plain,
% 94.91/95.21 (aElementOf0(sz00, szNzAzT0) <=> aElementOf0(sz00, szNzAzT0)),
% 94.91/95.21 inference(rewrite,[status(thm)],[])).
% 94.91/95.21 tff(105,axiom,(aElementOf0(sz00, szNzAzT0)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','mZeroNum')).
% 94.91/95.21 tff(106,plain,
% 94.91/95.21 (aElementOf0(sz00, szNzAzT0)),
% 94.91/95.21 inference(modus_ponens,[status(thm)],[105, 104])).
% 94.91/95.21 tff(107,plain,
% 94.91/95.21 (((~![W0: $i] : ((~aElementOf0(W0, szNzAzT0)) | (~((~aElementOf0(szszuzczcdt0(W0), szNzAzT0)) | (szszuzczcdt0(W0) = sz00))))) | ((~aElementOf0(sz00, szNzAzT0)) | (~((~aElementOf0(szszuzczcdt0(sz00), szNzAzT0)) | (szszuzczcdt0(sz00) = sz00))))) <=> ((~![W0: $i] : ((~aElementOf0(W0, szNzAzT0)) | (~((~aElementOf0(szszuzczcdt0(W0), szNzAzT0)) | (szszuzczcdt0(W0) = sz00))))) | (~aElementOf0(sz00, szNzAzT0)) | (~((~aElementOf0(szszuzczcdt0(sz00), szNzAzT0)) | (szszuzczcdt0(sz00) = sz00))))),
% 94.91/95.21 inference(rewrite,[status(thm)],[])).
% 94.91/95.21 tff(108,plain,
% 94.91/95.21 ((~![W0: $i] : ((~aElementOf0(W0, szNzAzT0)) | (~((~aElementOf0(szszuzczcdt0(W0), szNzAzT0)) | (szszuzczcdt0(W0) = sz00))))) | ((~aElementOf0(sz00, szNzAzT0)) | (~((~aElementOf0(szszuzczcdt0(sz00), szNzAzT0)) | (szszuzczcdt0(sz00) = sz00))))),
% 94.91/95.21 inference(quant_inst,[status(thm)],[])).
% 94.91/95.21 tff(109,plain,
% 94.91/95.21 ((~![W0: $i] : ((~aElementOf0(W0, szNzAzT0)) | (~((~aElementOf0(szszuzczcdt0(W0), szNzAzT0)) | (szszuzczcdt0(W0) = sz00))))) | (~aElementOf0(sz00, szNzAzT0)) | (~((~aElementOf0(szszuzczcdt0(sz00), szNzAzT0)) | (szszuzczcdt0(sz00) = sz00)))),
% 94.91/95.21 inference(modus_ponens,[status(thm)],[108, 107])).
% 94.91/95.21 tff(110,plain,
% 94.91/95.21 (~((~aElementOf0(szszuzczcdt0(sz00), szNzAzT0)) | (szszuzczcdt0(sz00) = sz00))),
% 94.91/95.21 inference(unit_resolution,[status(thm)],[109, 106, 103])).
% 94.91/95.21 tff(111,plain,
% 94.91/95.21 (((~aElementOf0(szszuzczcdt0(sz00), szNzAzT0)) | (szszuzczcdt0(sz00) = sz00)) | (~(szszuzczcdt0(sz00) = sz00))),
% 94.91/95.21 inference(tautology,[status(thm)],[])).
% 94.91/95.21 tff(112,plain,
% 94.91/95.21 (~(szszuzczcdt0(sz00) = sz00)),
% 94.91/95.21 inference(unit_resolution,[status(thm)],[111, 110])).
% 94.91/95.21 tff(113,plain,
% 94.91/95.21 (((~aElementOf0(szszuzczcdt0(sz00), szNzAzT0)) | (szszuzczcdt0(sz00) = sz00)) | aElementOf0(szszuzczcdt0(sz00), szNzAzT0)),
% 94.91/95.21 inference(tautology,[status(thm)],[])).
% 94.91/95.21 tff(114,plain,
% 94.91/95.21 (aElementOf0(szszuzczcdt0(sz00), szNzAzT0)),
% 94.91/95.21 inference(unit_resolution,[status(thm)],[113, 110])).
% 94.91/95.21 tff(115,plain,
% 94.91/95.21 (^[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))))))))),
% 94.91/95.21 inference(bind,[status(th)],[])).
% 94.91/95.21 tff(116,plain,
% 94.91/95.21 (![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)))))))),
% 94.91/95.21 inference(quant_intro,[status(thm)],[115])).
% 94.91/95.21 tff(117,plain,
% 94.91/95.21 (^[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)))))))))),
% 94.91/95.21 inference(bind,[status(th)],[])).
% 94.91/95.21 tff(118,plain,
% 94.91/95.21 (![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)))))))),
% 94.91/95.21 inference(quant_intro,[status(thm)],[117])).
% 94.91/95.21 tff(119,plain,
% 94.91/95.21 (^[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))))))),
% 94.91/95.21 inference(bind,[status(th)],[])).
% 94.91/95.21 tff(120,plain,
% 94.91/95.21 (![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)))))),
% 94.91/95.21 inference(quant_intro,[status(thm)],[119])).
% 94.91/95.21 tff(121,plain,
% 94.91/95.21 (![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)))),
% 94.91/95.21 inference(rewrite,[status(thm)],[])).
% 94.91/95.21 tff(122,plain,
% 94.91/95.21 (^[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)))))),
% 94.91/95.21 inference(bind,[status(th)],[])).
% 94.91/95.21 tff(123,plain,
% 94.91/95.21 (![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)))),
% 94.91/95.21 inference(quant_intro,[status(thm)],[122])).
% 94.91/95.21 tff(124,axiom,(![W0: $i] : (aElementOf0(W0, szNzAzT0) => ((W0 = sz00) | ?[W1: $i] : (aElementOf0(W1, szNzAzT0) & (W0 = szszuzczcdt0(W1)))))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','mNatExtra')).
% 94.91/95.21 tff(125,plain,
% 94.91/95.21 (![W0: $i] : (?[W1: $i] : (aElementOf0(W1, szNzAzT0) & (W0 = szszuzczcdt0(W1))) | (W0 = sz00) | (~aElementOf0(W0, szNzAzT0)))),
% 94.91/95.21 inference(modus_ponens,[status(thm)],[124, 123])).
% 94.91/95.21 tff(126,plain,
% 94.91/95.21 (![W0: $i] : (?[W1: $i] : (aElementOf0(W1, szNzAzT0) & (W0 = szszuzczcdt0(W1))) | (W0 = sz00) | (~aElementOf0(W0, szNzAzT0)))),
% 94.91/95.21 inference(modus_ponens,[status(thm)],[125, 121])).
% 94.91/95.21 tff(127,plain,(
% 94.91/95.21 ![W0: $i] : ((aElementOf0(tptp_fun_W1_4(W0), szNzAzT0) & (W0 = szszuzczcdt0(tptp_fun_W1_4(W0)))) | (W0 = sz00) | (~aElementOf0(W0, szNzAzT0)))),
% 94.91/95.21 inference(skolemize,[status(sab)],[126])).
% 94.91/95.21 tff(128,plain,
% 94.91/95.21 (![W0: $i] : ((W0 = sz00) | (~aElementOf0(W0, szNzAzT0)) | (aElementOf0(tptp_fun_W1_4(W0), szNzAzT0) & (W0 = szszuzczcdt0(tptp_fun_W1_4(W0)))))),
% 94.91/95.21 inference(modus_ponens,[status(thm)],[127, 120])).
% 94.91/95.21 tff(129,plain,
% 94.91/95.21 (![W0: $i] : ((W0 = sz00) | (~aElementOf0(W0, szNzAzT0)) | (~((~aElementOf0(tptp_fun_W1_4(W0), szNzAzT0)) | (~(W0 = szszuzczcdt0(tptp_fun_W1_4(W0)))))))),
% 94.91/95.21 inference(modus_ponens,[status(thm)],[128, 118])).
% 94.91/95.21 tff(130,plain,
% 94.91/95.21 (![W0: $i] : ((W0 = sz00) | (~aElementOf0(W0, szNzAzT0)) | (~((~aElementOf0(tptp_fun_W1_4(W0), szNzAzT0)) | (~(W0 = szszuzczcdt0(tptp_fun_W1_4(W0)))))))),
% 94.91/95.21 inference(modus_ponens,[status(thm)],[129, 116])).
% 94.91/95.21 tff(131,plain,
% 94.91/95.21 (((~![W0: $i] : ((W0 = sz00) | (~aElementOf0(W0, szNzAzT0)) | (~((~aElementOf0(tptp_fun_W1_4(W0), szNzAzT0)) | (~(W0 = szszuzczcdt0(tptp_fun_W1_4(W0)))))))) | ((~aElementOf0(szszuzczcdt0(sz00), szNzAzT0)) | (szszuzczcdt0(sz00) = sz00) | (~((~aElementOf0(tptp_fun_W1_4(szszuzczcdt0(sz00)), szNzAzT0)) | (~(szszuzczcdt0(sz00) = szszuzczcdt0(tptp_fun_W1_4(szszuzczcdt0(sz00))))))))) <=> ((~![W0: $i] : ((W0 = sz00) | (~aElementOf0(W0, szNzAzT0)) | (~((~aElementOf0(tptp_fun_W1_4(W0), szNzAzT0)) | (~(W0 = szszuzczcdt0(tptp_fun_W1_4(W0)))))))) | (~aElementOf0(szszuzczcdt0(sz00), szNzAzT0)) | (szszuzczcdt0(sz00) = sz00) | (~((~aElementOf0(tptp_fun_W1_4(szszuzczcdt0(sz00)), szNzAzT0)) | (~(szszuzczcdt0(sz00) = szszuzczcdt0(tptp_fun_W1_4(szszuzczcdt0(sz00))))))))),
% 94.91/95.21 inference(rewrite,[status(thm)],[])).
% 94.91/95.21 tff(132,plain,
% 94.91/95.21 (((szszuzczcdt0(sz00) = sz00) | (~aElementOf0(szszuzczcdt0(sz00), szNzAzT0)) | (~((~aElementOf0(tptp_fun_W1_4(szszuzczcdt0(sz00)), szNzAzT0)) | (~(szszuzczcdt0(sz00) = szszuzczcdt0(tptp_fun_W1_4(szszuzczcdt0(sz00)))))))) <=> ((~aElementOf0(szszuzczcdt0(sz00), szNzAzT0)) | (szszuzczcdt0(sz00) = sz00) | (~((~aElementOf0(tptp_fun_W1_4(szszuzczcdt0(sz00)), szNzAzT0)) | (~(szszuzczcdt0(sz00) = szszuzczcdt0(tptp_fun_W1_4(szszuzczcdt0(sz00))))))))),
% 94.91/95.21 inference(rewrite,[status(thm)],[])).
% 94.91/95.21 tff(133,plain,
% 94.91/95.21 (((~![W0: $i] : ((W0 = sz00) | (~aElementOf0(W0, szNzAzT0)) | (~((~aElementOf0(tptp_fun_W1_4(W0), szNzAzT0)) | (~(W0 = szszuzczcdt0(tptp_fun_W1_4(W0)))))))) | ((szszuzczcdt0(sz00) = sz00) | (~aElementOf0(szszuzczcdt0(sz00), szNzAzT0)) | (~((~aElementOf0(tptp_fun_W1_4(szszuzczcdt0(sz00)), szNzAzT0)) | (~(szszuzczcdt0(sz00) = szszuzczcdt0(tptp_fun_W1_4(szszuzczcdt0(sz00))))))))) <=> ((~![W0: $i] : ((W0 = sz00) | (~aElementOf0(W0, szNzAzT0)) | (~((~aElementOf0(tptp_fun_W1_4(W0), szNzAzT0)) | (~(W0 = szszuzczcdt0(tptp_fun_W1_4(W0)))))))) | ((~aElementOf0(szszuzczcdt0(sz00), szNzAzT0)) | (szszuzczcdt0(sz00) = sz00) | (~((~aElementOf0(tptp_fun_W1_4(szszuzczcdt0(sz00)), szNzAzT0)) | (~(szszuzczcdt0(sz00) = szszuzczcdt0(tptp_fun_W1_4(szszuzczcdt0(sz00)))))))))),
% 94.91/95.21 inference(monotonicity,[status(thm)],[132])).
% 94.91/95.21 tff(134,plain,
% 94.91/95.21 (((~![W0: $i] : ((W0 = sz00) | (~aElementOf0(W0, szNzAzT0)) | (~((~aElementOf0(tptp_fun_W1_4(W0), szNzAzT0)) | (~(W0 = szszuzczcdt0(tptp_fun_W1_4(W0)))))))) | ((szszuzczcdt0(sz00) = sz00) | (~aElementOf0(szszuzczcdt0(sz00), szNzAzT0)) | (~((~aElementOf0(tptp_fun_W1_4(szszuzczcdt0(sz00)), szNzAzT0)) | (~(szszuzczcdt0(sz00) = szszuzczcdt0(tptp_fun_W1_4(szszuzczcdt0(sz00))))))))) <=> ((~![W0: $i] : ((W0 = sz00) | (~aElementOf0(W0, szNzAzT0)) | (~((~aElementOf0(tptp_fun_W1_4(W0), szNzAzT0)) | (~(W0 = szszuzczcdt0(tptp_fun_W1_4(W0)))))))) | (~aElementOf0(szszuzczcdt0(sz00), szNzAzT0)) | (szszuzczcdt0(sz00) = sz00) | (~((~aElementOf0(tptp_fun_W1_4(szszuzczcdt0(sz00)), szNzAzT0)) | (~(szszuzczcdt0(sz00) = szszuzczcdt0(tptp_fun_W1_4(szszuzczcdt0(sz00))))))))),
% 94.91/95.21 inference(transitivity,[status(thm)],[133, 131])).
% 94.91/95.21 tff(135,plain,
% 94.91/95.21 ((~![W0: $i] : ((W0 = sz00) | (~aElementOf0(W0, szNzAzT0)) | (~((~aElementOf0(tptp_fun_W1_4(W0), szNzAzT0)) | (~(W0 = szszuzczcdt0(tptp_fun_W1_4(W0)))))))) | ((szszuzczcdt0(sz00) = sz00) | (~aElementOf0(szszuzczcdt0(sz00), szNzAzT0)) | (~((~aElementOf0(tptp_fun_W1_4(szszuzczcdt0(sz00)), szNzAzT0)) | (~(szszuzczcdt0(sz00) = szszuzczcdt0(tptp_fun_W1_4(szszuzczcdt0(sz00))))))))),
% 94.91/95.21 inference(quant_inst,[status(thm)],[])).
% 94.91/95.21 tff(136,plain,
% 94.91/95.21 ((~![W0: $i] : ((W0 = sz00) | (~aElementOf0(W0, szNzAzT0)) | (~((~aElementOf0(tptp_fun_W1_4(W0), szNzAzT0)) | (~(W0 = szszuzczcdt0(tptp_fun_W1_4(W0)))))))) | (~aElementOf0(szszuzczcdt0(sz00), szNzAzT0)) | (szszuzczcdt0(sz00) = sz00) | (~((~aElementOf0(tptp_fun_W1_4(szszuzczcdt0(sz00)), szNzAzT0)) | (~(szszuzczcdt0(sz00) = szszuzczcdt0(tptp_fun_W1_4(szszuzczcdt0(sz00)))))))),
% 94.91/95.21 inference(modus_ponens,[status(thm)],[135, 134])).
% 94.91/95.21 tff(137,plain,
% 94.91/95.21 (~((~aElementOf0(tptp_fun_W1_4(szszuzczcdt0(sz00)), szNzAzT0)) | (~(szszuzczcdt0(sz00) = szszuzczcdt0(tptp_fun_W1_4(szszuzczcdt0(sz00))))))),
% 94.91/95.21 inference(unit_resolution,[status(thm)],[136, 130, 114, 112])).
% 94.91/95.21 tff(138,plain,
% 94.91/95.21 (((~aElementOf0(tptp_fun_W1_4(szszuzczcdt0(sz00)), szNzAzT0)) | (~(szszuzczcdt0(sz00) = szszuzczcdt0(tptp_fun_W1_4(szszuzczcdt0(sz00)))))) | (szszuzczcdt0(sz00) = szszuzczcdt0(tptp_fun_W1_4(szszuzczcdt0(sz00))))),
% 94.91/95.21 inference(tautology,[status(thm)],[])).
% 94.91/95.21 tff(139,plain,
% 94.91/95.21 (szszuzczcdt0(sz00) = szszuzczcdt0(tptp_fun_W1_4(szszuzczcdt0(sz00)))),
% 94.91/95.21 inference(unit_resolution,[status(thm)],[138, 137])).
% 94.91/95.21 tff(140,plain,
% 94.91/95.21 (((~aElementOf0(tptp_fun_W1_4(szszuzczcdt0(sz00)), szNzAzT0)) | (~(szszuzczcdt0(sz00) = szszuzczcdt0(tptp_fun_W1_4(szszuzczcdt0(sz00)))))) | aElementOf0(tptp_fun_W1_4(szszuzczcdt0(sz00)), szNzAzT0)),
% 94.91/95.21 inference(tautology,[status(thm)],[])).
% 94.91/95.21 tff(141,plain,
% 94.91/95.21 (aElementOf0(tptp_fun_W1_4(szszuzczcdt0(sz00)), szNzAzT0)),
% 94.91/95.21 inference(unit_resolution,[status(thm)],[140, 137])).
% 94.91/95.21 tff(142,plain,
% 94.91/95.21 (^[W0: $i, W1: $i] : refl(((W0 = W1) | (~aElementOf0(W1, szNzAzT0)) | (~(szszuzczcdt0(W0) = szszuzczcdt0(W1))) | (~aElementOf0(W0, szNzAzT0))) <=> ((W0 = W1) | (~aElementOf0(W1, szNzAzT0)) | (~(szszuzczcdt0(W0) = szszuzczcdt0(W1))) | (~aElementOf0(W0, szNzAzT0))))),
% 94.91/95.21 inference(bind,[status(th)],[])).
% 94.91/95.21 tff(143,plain,
% 94.91/95.21 (![W0: $i, W1: $i] : ((W0 = W1) | (~aElementOf0(W1, szNzAzT0)) | (~(szszuzczcdt0(W0) = szszuzczcdt0(W1))) | (~aElementOf0(W0, szNzAzT0))) <=> ![W0: $i, W1: $i] : ((W0 = W1) | (~aElementOf0(W1, szNzAzT0)) | (~(szszuzczcdt0(W0) = szszuzczcdt0(W1))) | (~aElementOf0(W0, szNzAzT0)))),
% 94.91/95.21 inference(quant_intro,[status(thm)],[142])).
% 94.91/95.21 tff(144,plain,
% 94.91/95.21 (^[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))))), (((W0 = W1) | (~(szszuzczcdt0(W0) = szszuzczcdt0(W1))) | (~(aElementOf0(W0, szNzAzT0) & aElementOf0(W1, szNzAzT0)))) <=> ((W0 = W1) | (~(szszuzczcdt0(W0) = szszuzczcdt0(W1))) | ((~aElementOf0(W1, szNzAzT0)) | (~aElementOf0(W0, szNzAzT0)))))), rewrite(((W0 = W1) | (~(szszuzczcdt0(W0) = szszuzczcdt0(W1))) | ((~aElementOf0(W1, szNzAzT0)) | (~aElementOf0(W0, szNzAzT0)))) <=> ((W0 = W1) | (~aElementOf0(W1, szNzAzT0)) | (~(szszuzczcdt0(W0) = szszuzczcdt0(W1))) | (~aElementOf0(W0, szNzAzT0)))), (((W0 = W1) | (~(szszuzczcdt0(W0) = szszuzczcdt0(W1))) | (~(aElementOf0(W0, szNzAzT0) & aElementOf0(W1, szNzAzT0)))) <=> ((W0 = W1) | (~aElementOf0(W1, szNzAzT0)) | (~(szszuzczcdt0(W0) = szszuzczcdt0(W1))) | (~aElementOf0(W0, szNzAzT0)))))),
% 94.91/95.21 inference(bind,[status(th)],[])).
% 94.91/95.21 tff(145,plain,
% 94.91/95.21 (![W0: $i, W1: $i] : ((W0 = W1) | (~(szszuzczcdt0(W0) = szszuzczcdt0(W1))) | (~(aElementOf0(W0, szNzAzT0) & aElementOf0(W1, szNzAzT0)))) <=> ![W0: $i, W1: $i] : ((W0 = W1) | (~aElementOf0(W1, szNzAzT0)) | (~(szszuzczcdt0(W0) = szszuzczcdt0(W1))) | (~aElementOf0(W0, szNzAzT0)))),
% 94.91/95.21 inference(quant_intro,[status(thm)],[144])).
% 94.91/95.21 tff(146,plain,
% 94.91/95.21 (![W0: $i, W1: $i] : ((W0 = W1) | (~(szszuzczcdt0(W0) = szszuzczcdt0(W1))) | (~(aElementOf0(W0, szNzAzT0) & aElementOf0(W1, szNzAzT0)))) <=> ![W0: $i, W1: $i] : ((W0 = W1) | (~(szszuzczcdt0(W0) = szszuzczcdt0(W1))) | (~(aElementOf0(W0, szNzAzT0) & aElementOf0(W1, szNzAzT0))))),
% 94.91/95.21 inference(rewrite,[status(thm)],[])).
% 94.91/95.21 tff(147,plain,
% 94.91/95.21 (^[W0: $i, W1: $i] : trans(monotonicity(rewrite(((szszuzczcdt0(W0) = szszuzczcdt0(W1)) => (W0 = W1)) <=> ((~(szszuzczcdt0(W0) = szszuzczcdt0(W1))) | (W0 = W1))), (((aElementOf0(W0, szNzAzT0) & aElementOf0(W1, szNzAzT0)) => ((szszuzczcdt0(W0) = szszuzczcdt0(W1)) => (W0 = W1))) <=> ((aElementOf0(W0, szNzAzT0) & aElementOf0(W1, szNzAzT0)) => ((~(szszuzczcdt0(W0) = szszuzczcdt0(W1))) | (W0 = W1))))), rewrite(((aElementOf0(W0, szNzAzT0) & aElementOf0(W1, szNzAzT0)) => ((~(szszuzczcdt0(W0) = szszuzczcdt0(W1))) | (W0 = W1))) <=> ((W0 = W1) | (~(szszuzczcdt0(W0) = szszuzczcdt0(W1))) | (~(aElementOf0(W0, szNzAzT0) & aElementOf0(W1, szNzAzT0))))), (((aElementOf0(W0, szNzAzT0) & aElementOf0(W1, szNzAzT0)) => ((szszuzczcdt0(W0) = szszuzczcdt0(W1)) => (W0 = W1))) <=> ((W0 = W1) | (~(szszuzczcdt0(W0) = szszuzczcdt0(W1))) | (~(aElementOf0(W0, szNzAzT0) & aElementOf0(W1, szNzAzT0))))))),
% 94.91/95.21 inference(bind,[status(th)],[])).
% 94.91/95.21 tff(148,plain,
% 94.91/95.21 (![W0: $i, W1: $i] : ((aElementOf0(W0, szNzAzT0) & aElementOf0(W1, szNzAzT0)) => ((szszuzczcdt0(W0) = szszuzczcdt0(W1)) => (W0 = W1))) <=> ![W0: $i, W1: $i] : ((W0 = W1) | (~(szszuzczcdt0(W0) = szszuzczcdt0(W1))) | (~(aElementOf0(W0, szNzAzT0) & aElementOf0(W1, szNzAzT0))))),
% 94.91/95.21 inference(quant_intro,[status(thm)],[147])).
% 94.91/95.21 tff(149,axiom,(![W0: $i, W1: $i] : ((aElementOf0(W0, szNzAzT0) & aElementOf0(W1, szNzAzT0)) => ((szszuzczcdt0(W0) = szszuzczcdt0(W1)) => (W0 = W1)))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','mSuccEquSucc')).
% 94.91/95.21 tff(150,plain,
% 94.91/95.21 (![W0: $i, W1: $i] : ((W0 = W1) | (~(szszuzczcdt0(W0) = szszuzczcdt0(W1))) | (~(aElementOf0(W0, szNzAzT0) & aElementOf0(W1, szNzAzT0))))),
% 94.91/95.21 inference(modus_ponens,[status(thm)],[149, 148])).
% 94.91/95.21 tff(151,plain,
% 94.91/95.21 (![W0: $i, W1: $i] : ((W0 = W1) | (~(szszuzczcdt0(W0) = szszuzczcdt0(W1))) | (~(aElementOf0(W0, szNzAzT0) & aElementOf0(W1, szNzAzT0))))),
% 94.91/95.21 inference(modus_ponens,[status(thm)],[150, 146])).
% 94.91/95.21 tff(152,plain,(
% 94.91/95.21 ![W0: $i, W1: $i] : ((W0 = W1) | (~(szszuzczcdt0(W0) = szszuzczcdt0(W1))) | (~(aElementOf0(W0, szNzAzT0) & aElementOf0(W1, szNzAzT0))))),
% 94.91/95.21 inference(skolemize,[status(sab)],[151])).
% 94.91/95.21 tff(153,plain,
% 94.91/95.21 (![W0: $i, W1: $i] : ((W0 = W1) | (~aElementOf0(W1, szNzAzT0)) | (~(szszuzczcdt0(W0) = szszuzczcdt0(W1))) | (~aElementOf0(W0, szNzAzT0)))),
% 94.91/95.21 inference(modus_ponens,[status(thm)],[152, 145])).
% 94.91/95.21 tff(154,plain,
% 94.91/95.21 (![W0: $i, W1: $i] : ((W0 = W1) | (~aElementOf0(W1, szNzAzT0)) | (~(szszuzczcdt0(W0) = szszuzczcdt0(W1))) | (~aElementOf0(W0, szNzAzT0)))),
% 94.91/95.21 inference(modus_ponens,[status(thm)],[153, 143])).
% 94.91/95.21 tff(155,plain,
% 94.91/95.21 (((~![W0: $i, W1: $i] : ((W0 = W1) | (~aElementOf0(W1, szNzAzT0)) | (~(szszuzczcdt0(W0) = szszuzczcdt0(W1))) | (~aElementOf0(W0, szNzAzT0)))) | ((~aElementOf0(sz00, szNzAzT0)) | (~aElementOf0(tptp_fun_W1_4(szszuzczcdt0(sz00)), szNzAzT0)) | (~(szszuzczcdt0(sz00) = szszuzczcdt0(tptp_fun_W1_4(szszuzczcdt0(sz00))))) | (sz00 = tptp_fun_W1_4(szszuzczcdt0(sz00))))) <=> ((~![W0: $i, W1: $i] : ((W0 = W1) | (~aElementOf0(W1, szNzAzT0)) | (~(szszuzczcdt0(W0) = szszuzczcdt0(W1))) | (~aElementOf0(W0, szNzAzT0)))) | (~aElementOf0(sz00, szNzAzT0)) | (~aElementOf0(tptp_fun_W1_4(szszuzczcdt0(sz00)), szNzAzT0)) | (~(szszuzczcdt0(sz00) = szszuzczcdt0(tptp_fun_W1_4(szszuzczcdt0(sz00))))) | (sz00 = tptp_fun_W1_4(szszuzczcdt0(sz00))))),
% 94.91/95.21 inference(rewrite,[status(thm)],[])).
% 94.91/95.21 tff(156,plain,
% 94.91/95.21 (((sz00 = tptp_fun_W1_4(szszuzczcdt0(sz00))) | (~aElementOf0(tptp_fun_W1_4(szszuzczcdt0(sz00)), szNzAzT0)) | (~(szszuzczcdt0(sz00) = szszuzczcdt0(tptp_fun_W1_4(szszuzczcdt0(sz00))))) | (~aElementOf0(sz00, szNzAzT0))) <=> ((~aElementOf0(sz00, szNzAzT0)) | (~aElementOf0(tptp_fun_W1_4(szszuzczcdt0(sz00)), szNzAzT0)) | (~(szszuzczcdt0(sz00) = szszuzczcdt0(tptp_fun_W1_4(szszuzczcdt0(sz00))))) | (sz00 = tptp_fun_W1_4(szszuzczcdt0(sz00))))),
% 94.91/95.21 inference(rewrite,[status(thm)],[])).
% 94.91/95.21 tff(157,plain,
% 94.91/95.21 (((~![W0: $i, W1: $i] : ((W0 = W1) | (~aElementOf0(W1, szNzAzT0)) | (~(szszuzczcdt0(W0) = szszuzczcdt0(W1))) | (~aElementOf0(W0, szNzAzT0)))) | ((sz00 = tptp_fun_W1_4(szszuzczcdt0(sz00))) | (~aElementOf0(tptp_fun_W1_4(szszuzczcdt0(sz00)), szNzAzT0)) | (~(szszuzczcdt0(sz00) = szszuzczcdt0(tptp_fun_W1_4(szszuzczcdt0(sz00))))) | (~aElementOf0(sz00, szNzAzT0)))) <=> ((~![W0: $i, W1: $i] : ((W0 = W1) | (~aElementOf0(W1, szNzAzT0)) | (~(szszuzczcdt0(W0) = szszuzczcdt0(W1))) | (~aElementOf0(W0, szNzAzT0)))) | ((~aElementOf0(sz00, szNzAzT0)) | (~aElementOf0(tptp_fun_W1_4(szszuzczcdt0(sz00)), szNzAzT0)) | (~(szszuzczcdt0(sz00) = szszuzczcdt0(tptp_fun_W1_4(szszuzczcdt0(sz00))))) | (sz00 = tptp_fun_W1_4(szszuzczcdt0(sz00)))))),
% 94.91/95.21 inference(monotonicity,[status(thm)],[156])).
% 94.91/95.21 tff(158,plain,
% 94.91/95.21 (((~![W0: $i, W1: $i] : ((W0 = W1) | (~aElementOf0(W1, szNzAzT0)) | (~(szszuzczcdt0(W0) = szszuzczcdt0(W1))) | (~aElementOf0(W0, szNzAzT0)))) | ((sz00 = tptp_fun_W1_4(szszuzczcdt0(sz00))) | (~aElementOf0(tptp_fun_W1_4(szszuzczcdt0(sz00)), szNzAzT0)) | (~(szszuzczcdt0(sz00) = szszuzczcdt0(tptp_fun_W1_4(szszuzczcdt0(sz00))))) | (~aElementOf0(sz00, szNzAzT0)))) <=> ((~![W0: $i, W1: $i] : ((W0 = W1) | (~aElementOf0(W1, szNzAzT0)) | (~(szszuzczcdt0(W0) = szszuzczcdt0(W1))) | (~aElementOf0(W0, szNzAzT0)))) | (~aElementOf0(sz00, szNzAzT0)) | (~aElementOf0(tptp_fun_W1_4(szszuzczcdt0(sz00)), szNzAzT0)) | (~(szszuzczcdt0(sz00) = szszuzczcdt0(tptp_fun_W1_4(szszuzczcdt0(sz00))))) | (sz00 = tptp_fun_W1_4(szszuzczcdt0(sz00))))),
% 94.91/95.21 inference(transitivity,[status(thm)],[157, 155])).
% 94.91/95.21 tff(159,plain,
% 94.91/95.21 ((~![W0: $i, W1: $i] : ((W0 = W1) | (~aElementOf0(W1, szNzAzT0)) | (~(szszuzczcdt0(W0) = szszuzczcdt0(W1))) | (~aElementOf0(W0, szNzAzT0)))) | ((sz00 = tptp_fun_W1_4(szszuzczcdt0(sz00))) | (~aElementOf0(tptp_fun_W1_4(szszuzczcdt0(sz00)), szNzAzT0)) | (~(szszuzczcdt0(sz00) = szszuzczcdt0(tptp_fun_W1_4(szszuzczcdt0(sz00))))) | (~aElementOf0(sz00, szNzAzT0)))),
% 94.91/95.21 inference(quant_inst,[status(thm)],[])).
% 94.91/95.21 tff(160,plain,
% 94.91/95.21 ((~![W0: $i, W1: $i] : ((W0 = W1) | (~aElementOf0(W1, szNzAzT0)) | (~(szszuzczcdt0(W0) = szszuzczcdt0(W1))) | (~aElementOf0(W0, szNzAzT0)))) | (~aElementOf0(sz00, szNzAzT0)) | (~aElementOf0(tptp_fun_W1_4(szszuzczcdt0(sz00)), szNzAzT0)) | (~(szszuzczcdt0(sz00) = szszuzczcdt0(tptp_fun_W1_4(szszuzczcdt0(sz00))))) | (sz00 = tptp_fun_W1_4(szszuzczcdt0(sz00)))),
% 94.91/95.21 inference(modus_ponens,[status(thm)],[159, 158])).
% 94.91/95.21 tff(161,plain,
% 94.91/95.21 (sz00 = tptp_fun_W1_4(szszuzczcdt0(sz00))),
% 94.91/95.21 inference(unit_resolution,[status(thm)],[160, 106, 154, 141, 139])).
% 94.91/95.21 tff(162,plain,
% 94.91/95.21 (^[W0: $i] : refl(((~aSet0(W0)) | ((sbrdtbr0(W0) = sz00) <=> (W0 = slcrc0))) <=> ((~aSet0(W0)) | ((sbrdtbr0(W0) = sz00) <=> (W0 = slcrc0))))),
% 94.91/95.21 inference(bind,[status(th)],[])).
% 94.91/95.21 tff(163,plain,
% 94.91/95.21 (![W0: $i] : ((~aSet0(W0)) | ((sbrdtbr0(W0) = sz00) <=> (W0 = slcrc0))) <=> ![W0: $i] : ((~aSet0(W0)) | ((sbrdtbr0(W0) = sz00) <=> (W0 = slcrc0)))),
% 94.91/95.21 inference(quant_intro,[status(thm)],[162])).
% 94.91/95.21 tff(164,plain,
% 94.91/95.21 (![W0: $i] : ((~aSet0(W0)) | ((sbrdtbr0(W0) = sz00) <=> (W0 = slcrc0))) <=> ![W0: $i] : ((~aSet0(W0)) | ((sbrdtbr0(W0) = sz00) <=> (W0 = slcrc0)))),
% 94.91/95.21 inference(rewrite,[status(thm)],[])).
% 94.91/95.21 tff(165,plain,
% 94.91/95.21 (^[W0: $i] : rewrite((aSet0(W0) => ((sbrdtbr0(W0) = sz00) <=> (W0 = slcrc0))) <=> ((~aSet0(W0)) | ((sbrdtbr0(W0) = sz00) <=> (W0 = slcrc0))))),
% 94.91/95.21 inference(bind,[status(th)],[])).
% 94.91/95.21 tff(166,plain,
% 94.91/95.21 (![W0: $i] : (aSet0(W0) => ((sbrdtbr0(W0) = sz00) <=> (W0 = slcrc0))) <=> ![W0: $i] : ((~aSet0(W0)) | ((sbrdtbr0(W0) = sz00) <=> (W0 = slcrc0)))),
% 94.91/95.21 inference(quant_intro,[status(thm)],[165])).
% 94.91/95.21 tff(167,axiom,(![W0: $i] : (aSet0(W0) => ((sbrdtbr0(W0) = sz00) <=> (W0 = slcrc0)))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','mCardEmpty')).
% 94.91/95.21 tff(168,plain,
% 94.91/95.21 (![W0: $i] : ((~aSet0(W0)) | ((sbrdtbr0(W0) = sz00) <=> (W0 = slcrc0)))),
% 94.91/95.21 inference(modus_ponens,[status(thm)],[167, 166])).
% 94.91/95.21 tff(169,plain,
% 94.91/95.21 (![W0: $i] : ((~aSet0(W0)) | ((sbrdtbr0(W0) = sz00) <=> (W0 = slcrc0)))),
% 94.91/95.21 inference(modus_ponens,[status(thm)],[168, 164])).
% 94.91/95.21 tff(170,plain,(
% 94.91/95.21 ![W0: $i] : ((~aSet0(W0)) | ((sbrdtbr0(W0) = sz00) <=> (W0 = slcrc0)))),
% 94.91/95.21 inference(skolemize,[status(sab)],[169])).
% 94.91/95.21 tff(171,plain,
% 94.91/95.21 (![W0: $i] : ((~aSet0(W0)) | ((sbrdtbr0(W0) = sz00) <=> (W0 = slcrc0)))),
% 94.91/95.21 inference(modus_ponens,[status(thm)],[170, 163])).
% 94.91/95.21 tff(172,plain,
% 94.91/95.21 (((~![W0: $i] : ((~aSet0(W0)) | ((sbrdtbr0(W0) = sz00) <=> (W0 = slcrc0)))) | ((~aSet0(slcrc0)) | (sbrdtbr0(slcrc0) = sz00))) <=> ((~![W0: $i] : ((~aSet0(W0)) | ((sbrdtbr0(W0) = sz00) <=> (W0 = slcrc0)))) | (~aSet0(slcrc0)) | (sbrdtbr0(slcrc0) = sz00))),
% 94.91/95.21 inference(rewrite,[status(thm)],[])).
% 94.91/95.21 tff(173,plain,
% 94.91/95.21 (((~aSet0(slcrc0)) | ((sbrdtbr0(slcrc0) = sz00) <=> (slcrc0 = slcrc0))) <=> ((~aSet0(slcrc0)) | (sbrdtbr0(slcrc0) = sz00))),
% 94.91/95.21 inference(rewrite,[status(thm)],[])).
% 94.91/95.21 tff(174,plain,
% 94.91/95.21 (((~![W0: $i] : ((~aSet0(W0)) | ((sbrdtbr0(W0) = sz00) <=> (W0 = slcrc0)))) | ((~aSet0(slcrc0)) | ((sbrdtbr0(slcrc0) = sz00) <=> (slcrc0 = slcrc0)))) <=> ((~![W0: $i] : ((~aSet0(W0)) | ((sbrdtbr0(W0) = sz00) <=> (W0 = slcrc0)))) | ((~aSet0(slcrc0)) | (sbrdtbr0(slcrc0) = sz00)))),
% 94.91/95.21 inference(monotonicity,[status(thm)],[173])).
% 94.91/95.21 tff(175,plain,
% 94.91/95.21 (((~![W0: $i] : ((~aSet0(W0)) | ((sbrdtbr0(W0) = sz00) <=> (W0 = slcrc0)))) | ((~aSet0(slcrc0)) | ((sbrdtbr0(slcrc0) = sz00) <=> (slcrc0 = slcrc0)))) <=> ((~![W0: $i] : ((~aSet0(W0)) | ((sbrdtbr0(W0) = sz00) <=> (W0 = slcrc0)))) | (~aSet0(slcrc0)) | (sbrdtbr0(slcrc0) = sz00))),
% 94.91/95.21 inference(transitivity,[status(thm)],[174, 172])).
% 94.91/95.21 tff(176,plain,
% 94.91/95.21 ((~![W0: $i] : ((~aSet0(W0)) | ((sbrdtbr0(W0) = sz00) <=> (W0 = slcrc0)))) | ((~aSet0(slcrc0)) | ((sbrdtbr0(slcrc0) = sz00) <=> (slcrc0 = slcrc0)))),
% 94.91/95.21 inference(quant_inst,[status(thm)],[])).
% 94.91/95.21 tff(177,plain,
% 94.91/95.21 ((~![W0: $i] : ((~aSet0(W0)) | ((sbrdtbr0(W0) = sz00) <=> (W0 = slcrc0)))) | (~aSet0(slcrc0)) | (sbrdtbr0(slcrc0) = sz00)),
% 94.91/95.21 inference(modus_ponens,[status(thm)],[176, 175])).
% 94.91/95.21 tff(178,plain,
% 94.91/95.21 (sbrdtbr0(slcrc0) = sz00),
% 94.91/95.21 inference(unit_resolution,[status(thm)],[177, 35, 171])).
% 94.91/95.21 tff(179,plain,
% 94.91/95.21 (sbrdtbr0(slcrc0) = tptp_fun_W1_4(szszuzczcdt0(sz00))),
% 94.91/95.21 inference(transitivity,[status(thm)],[178, 161])).
% 94.91/95.21 tff(180,plain,
% 94.91/95.21 (slbdtrb0(sbrdtbr0(slcrc0)) = slbdtrb0(tptp_fun_W1_4(szszuzczcdt0(sz00)))),
% 94.91/95.21 inference(monotonicity,[status(thm)],[179])).
% 94.91/95.21 tff(181,plain,
% 94.91/95.21 (slbdtrb0(tptp_fun_W1_4(szszuzczcdt0(sz00))) = slbdtrb0(sbrdtbr0(slcrc0))),
% 94.91/95.21 inference(symmetry,[status(thm)],[180])).
% 94.91/95.21 tff(182,plain,
% 94.91/95.21 ((~((~(slbdtrb0(tptp_fun_W1_4(szszuzczcdt0(sz00))) = slbdtrb0(sbrdtbr0(slcrc0)))) | (~((~aSet0(slbdtrb0(tptp_fun_W1_4(szszuzczcdt0(sz00))))) | (~![W2: $i] : (~(((~aElementOf0(W2, szNzAzT0)) | (~sdtlseqdt0(szszuzczcdt0(W2), sbrdtbr0(slcrc0)))) <=> aElementOf0(W2, slbdtrb0(tptp_fun_W1_4(szszuzczcdt0(sz00))))))))))) | (~(slbdtrb0(tptp_fun_W1_4(szszuzczcdt0(sz00))) = slbdtrb0(sbrdtbr0(slcrc0)))) | (~((~aSet0(slbdtrb0(tptp_fun_W1_4(szszuzczcdt0(sz00))))) | (~![W2: $i] : (~(((~aElementOf0(W2, szNzAzT0)) | (~sdtlseqdt0(szszuzczcdt0(W2), sbrdtbr0(slcrc0)))) <=> aElementOf0(W2, slbdtrb0(tptp_fun_W1_4(szszuzczcdt0(sz00)))))))))),
% 94.91/95.21 inference(tautology,[status(thm)],[])).
% 94.91/95.21 tff(183,plain,
% 94.91/95.21 ((~((~(slbdtrb0(tptp_fun_W1_4(szszuzczcdt0(sz00))) = slbdtrb0(sbrdtbr0(slcrc0)))) | (~((~aSet0(slbdtrb0(tptp_fun_W1_4(szszuzczcdt0(sz00))))) | (~![W2: $i] : (~(((~aElementOf0(W2, szNzAzT0)) | (~sdtlseqdt0(szszuzczcdt0(W2), sbrdtbr0(slcrc0)))) <=> aElementOf0(W2, slbdtrb0(tptp_fun_W1_4(szszuzczcdt0(sz00))))))))))) | (~((~aSet0(slbdtrb0(tptp_fun_W1_4(szszuzczcdt0(sz00))))) | (~![W2: $i] : (~(((~aElementOf0(W2, szNzAzT0)) | (~sdtlseqdt0(szszuzczcdt0(W2), sbrdtbr0(slcrc0)))) <=> aElementOf0(W2, slbdtrb0(tptp_fun_W1_4(szszuzczcdt0(sz00)))))))))),
% 94.91/95.21 inference(unit_resolution,[status(thm)],[182, 181])).
% 94.91/95.21 tff(184,plain,
% 94.91/95.21 (~((~aSet0(slbdtrb0(tptp_fun_W1_4(szszuzczcdt0(sz00))))) | (~![W2: $i] : (~(((~aElementOf0(W2, szNzAzT0)) | (~sdtlseqdt0(szszuzczcdt0(W2), sbrdtbr0(slcrc0)))) <=> aElementOf0(W2, slbdtrb0(tptp_fun_W1_4(szszuzczcdt0(sz00))))))))),
% 94.91/95.21 inference(unit_resolution,[status(thm)],[183, 90])).
% 94.99/95.21 tff(185,plain,
% 94.99/95.21 (((~aSet0(slbdtrb0(tptp_fun_W1_4(szszuzczcdt0(sz00))))) | (~![W2: $i] : (~(((~aElementOf0(W2, szNzAzT0)) | (~sdtlseqdt0(szszuzczcdt0(W2), sbrdtbr0(slcrc0)))) <=> aElementOf0(W2, slbdtrb0(tptp_fun_W1_4(szszuzczcdt0(sz00)))))))) | aSet0(slbdtrb0(tptp_fun_W1_4(szszuzczcdt0(sz00))))),
% 94.99/95.21 inference(tautology,[status(thm)],[])).
% 94.99/95.21 tff(186,plain,
% 94.99/95.21 (aSet0(slbdtrb0(tptp_fun_W1_4(szszuzczcdt0(sz00))))),
% 94.99/95.21 inference(unit_resolution,[status(thm)],[185, 184])).
% 94.99/95.21 tff(187,plain,
% 94.99/95.21 (slbdtrb0(sz00) = slbdtrb0(tptp_fun_W1_4(szszuzczcdt0(sz00)))),
% 94.99/95.21 inference(monotonicity,[status(thm)],[161])).
% 94.99/95.21 tff(188,plain,
% 94.99/95.21 (slbdtrb0(tptp_fun_W1_4(szszuzczcdt0(sz00))) = slbdtrb0(sz00)),
% 94.99/95.21 inference(symmetry,[status(thm)],[187])).
% 94.99/95.21 tff(189,plain,
% 94.99/95.21 ((slbdtrb0(tptp_fun_W1_4(szszuzczcdt0(sz00))) = slcrc0) <=> (slbdtrb0(sz00) = slcrc0)),
% 94.99/95.21 inference(monotonicity,[status(thm)],[188])).
% 94.99/95.21 tff(190,plain,
% 94.99/95.21 ((slbdtrb0(sz00) = slcrc0) <=> (slbdtrb0(tptp_fun_W1_4(szszuzczcdt0(sz00))) = slcrc0)),
% 94.99/95.21 inference(symmetry,[status(thm)],[189])).
% 94.99/95.21 tff(191,plain,
% 94.99/95.21 ((~(slbdtrb0(sz00) = slcrc0)) <=> (~(slbdtrb0(tptp_fun_W1_4(szszuzczcdt0(sz00))) = slcrc0))),
% 94.99/95.21 inference(monotonicity,[status(thm)],[190])).
% 94.99/95.21 tff(192,plain,
% 94.99/95.21 ((~(slbdtrb0(sz00) = slcrc0)) <=> (~(slbdtrb0(sz00) = slcrc0))),
% 94.99/95.21 inference(rewrite,[status(thm)],[])).
% 94.99/95.21 tff(193,axiom,(~(slbdtrb0(sz00) = slcrc0)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','m__')).
% 94.99/95.21 tff(194,plain,
% 94.99/95.21 (~(slbdtrb0(sz00) = slcrc0)),
% 94.99/95.21 inference(modus_ponens,[status(thm)],[193, 192])).
% 94.99/95.21 tff(195,plain,
% 94.99/95.21 (~(slbdtrb0(tptp_fun_W1_4(szszuzczcdt0(sz00))) = slcrc0)),
% 94.99/95.21 inference(modus_ponens,[status(thm)],[194, 191])).
% 94.99/95.21 tff(196,plain,
% 94.99/95.21 ((~((slbdtrb0(tptp_fun_W1_4(szszuzczcdt0(sz00))) = slcrc0) | (~aSet0(slbdtrb0(tptp_fun_W1_4(szszuzczcdt0(sz00))))) | aElementOf0(tptp_fun_W1_0(slbdtrb0(tptp_fun_W1_4(szszuzczcdt0(sz00)))), slbdtrb0(tptp_fun_W1_4(szszuzczcdt0(sz00)))))) | (slbdtrb0(tptp_fun_W1_4(szszuzczcdt0(sz00))) = slcrc0) | (~aSet0(slbdtrb0(tptp_fun_W1_4(szszuzczcdt0(sz00))))) | aElementOf0(tptp_fun_W1_0(slbdtrb0(tptp_fun_W1_4(szszuzczcdt0(sz00)))), slbdtrb0(tptp_fun_W1_4(szszuzczcdt0(sz00))))),
% 94.99/95.21 inference(tautology,[status(thm)],[])).
% 94.99/95.21 tff(197,plain,
% 94.99/95.21 ((~((slbdtrb0(tptp_fun_W1_4(szszuzczcdt0(sz00))) = slcrc0) | (~aSet0(slbdtrb0(tptp_fun_W1_4(szszuzczcdt0(sz00))))) | aElementOf0(tptp_fun_W1_0(slbdtrb0(tptp_fun_W1_4(szszuzczcdt0(sz00)))), slbdtrb0(tptp_fun_W1_4(szszuzczcdt0(sz00)))))) | aElementOf0(tptp_fun_W1_0(slbdtrb0(tptp_fun_W1_4(szszuzczcdt0(sz00)))), slbdtrb0(tptp_fun_W1_4(szszuzczcdt0(sz00))))),
% 94.99/95.21 inference(unit_resolution,[status(thm)],[196, 195, 186])).
% 94.99/95.21 tff(198,plain,
% 94.99/95.21 (aElementOf0(tptp_fun_W1_0(slbdtrb0(tptp_fun_W1_4(szszuzczcdt0(sz00)))), slbdtrb0(tptp_fun_W1_4(szszuzczcdt0(sz00))))),
% 94.99/95.21 inference(unit_resolution,[status(thm)],[197, 23])).
% 94.99/95.21 tff(199,assumption,(~((~aElementOf0(tptp_fun_W1_0(slbdtrb0(tptp_fun_W1_4(szszuzczcdt0(sz00)))), szNzAzT0)) | (~sdtlseqdt0(szszuzczcdt0(tptp_fun_W1_0(slbdtrb0(tptp_fun_W1_4(szszuzczcdt0(sz00))))), sz00)))), introduced(assumption)).
% 94.99/95.21 tff(200,plain,
% 94.99/95.21 (((~aElementOf0(tptp_fun_W1_0(slbdtrb0(tptp_fun_W1_4(szszuzczcdt0(sz00)))), szNzAzT0)) | (~sdtlseqdt0(szszuzczcdt0(tptp_fun_W1_0(slbdtrb0(tptp_fun_W1_4(szszuzczcdt0(sz00))))), sz00))) | sdtlseqdt0(szszuzczcdt0(tptp_fun_W1_0(slbdtrb0(tptp_fun_W1_4(szszuzczcdt0(sz00))))), sz00)),
% 94.99/95.21 inference(tautology,[status(thm)],[])).
% 94.99/95.21 tff(201,plain,
% 94.99/95.21 (sdtlseqdt0(szszuzczcdt0(tptp_fun_W1_0(slbdtrb0(tptp_fun_W1_4(szszuzczcdt0(sz00))))), sz00)),
% 94.99/95.21 inference(unit_resolution,[status(thm)],[200, 199])).
% 94.99/95.21 tff(202,plain,
% 94.99/95.21 (((~aElementOf0(tptp_fun_W1_0(slbdtrb0(tptp_fun_W1_4(szszuzczcdt0(sz00)))), szNzAzT0)) | (~sdtlseqdt0(szszuzczcdt0(tptp_fun_W1_0(slbdtrb0(tptp_fun_W1_4(szszuzczcdt0(sz00))))), sz00))) | aElementOf0(tptp_fun_W1_0(slbdtrb0(tptp_fun_W1_4(szszuzczcdt0(sz00)))), szNzAzT0)),
% 94.99/95.21 inference(tautology,[status(thm)],[])).
% 94.99/95.21 tff(203,plain,
% 94.99/95.21 (aElementOf0(tptp_fun_W1_0(slbdtrb0(tptp_fun_W1_4(szszuzczcdt0(sz00)))), szNzAzT0)),
% 94.99/95.21 inference(unit_resolution,[status(thm)],[202, 199])).
% 94.99/95.21 tff(204,plain,
% 94.99/95.21 (^[W0: $i] : refl(((~aElementOf0(W0, szNzAzT0)) | (~sdtlseqdt0(szszuzczcdt0(W0), sz00))) <=> ((~aElementOf0(W0, szNzAzT0)) | (~sdtlseqdt0(szszuzczcdt0(W0), sz00))))),
% 94.99/95.21 inference(bind,[status(th)],[])).
% 94.99/95.21 tff(205,plain,
% 94.99/95.21 (![W0: $i] : ((~aElementOf0(W0, szNzAzT0)) | (~sdtlseqdt0(szszuzczcdt0(W0), sz00))) <=> ![W0: $i] : ((~aElementOf0(W0, szNzAzT0)) | (~sdtlseqdt0(szszuzczcdt0(W0), sz00)))),
% 94.99/95.21 inference(quant_intro,[status(thm)],[204])).
% 94.99/95.21 tff(206,plain,
% 94.99/95.21 (![W0: $i] : ((~aElementOf0(W0, szNzAzT0)) | (~sdtlseqdt0(szszuzczcdt0(W0), sz00))) <=> ![W0: $i] : ((~aElementOf0(W0, szNzAzT0)) | (~sdtlseqdt0(szszuzczcdt0(W0), sz00)))),
% 94.99/95.21 inference(rewrite,[status(thm)],[])).
% 94.99/95.21 tff(207,plain,
% 94.99/95.21 (^[W0: $i] : rewrite((aElementOf0(W0, szNzAzT0) => (~sdtlseqdt0(szszuzczcdt0(W0), sz00))) <=> ((~aElementOf0(W0, szNzAzT0)) | (~sdtlseqdt0(szszuzczcdt0(W0), sz00))))),
% 94.99/95.21 inference(bind,[status(th)],[])).
% 94.99/95.21 tff(208,plain,
% 94.99/95.21 (![W0: $i] : (aElementOf0(W0, szNzAzT0) => (~sdtlseqdt0(szszuzczcdt0(W0), sz00))) <=> ![W0: $i] : ((~aElementOf0(W0, szNzAzT0)) | (~sdtlseqdt0(szszuzczcdt0(W0), sz00)))),
% 94.99/95.21 inference(quant_intro,[status(thm)],[207])).
% 94.99/95.21 tff(209,axiom,(![W0: $i] : (aElementOf0(W0, szNzAzT0) => (~sdtlseqdt0(szszuzczcdt0(W0), sz00)))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','mNoScLessZr')).
% 94.99/95.21 tff(210,plain,
% 94.99/95.21 (![W0: $i] : ((~aElementOf0(W0, szNzAzT0)) | (~sdtlseqdt0(szszuzczcdt0(W0), sz00)))),
% 94.99/95.21 inference(modus_ponens,[status(thm)],[209, 208])).
% 94.99/95.21 tff(211,plain,
% 94.99/95.21 (![W0: $i] : ((~aElementOf0(W0, szNzAzT0)) | (~sdtlseqdt0(szszuzczcdt0(W0), sz00)))),
% 94.99/95.21 inference(modus_ponens,[status(thm)],[210, 206])).
% 94.99/95.21 tff(212,plain,(
% 94.99/95.21 ![W0: $i] : ((~aElementOf0(W0, szNzAzT0)) | (~sdtlseqdt0(szszuzczcdt0(W0), sz00)))),
% 94.99/95.21 inference(skolemize,[status(sab)],[211])).
% 94.99/95.21 tff(213,plain,
% 94.99/95.21 (![W0: $i] : ((~aElementOf0(W0, szNzAzT0)) | (~sdtlseqdt0(szszuzczcdt0(W0), sz00)))),
% 94.99/95.21 inference(modus_ponens,[status(thm)],[212, 205])).
% 94.99/95.21 tff(214,plain,
% 94.99/95.21 (((~![W0: $i] : ((~aElementOf0(W0, szNzAzT0)) | (~sdtlseqdt0(szszuzczcdt0(W0), sz00)))) | ((~aElementOf0(tptp_fun_W1_0(slbdtrb0(tptp_fun_W1_4(szszuzczcdt0(sz00)))), szNzAzT0)) | (~sdtlseqdt0(szszuzczcdt0(tptp_fun_W1_0(slbdtrb0(tptp_fun_W1_4(szszuzczcdt0(sz00))))), sz00)))) <=> ((~![W0: $i] : ((~aElementOf0(W0, szNzAzT0)) | (~sdtlseqdt0(szszuzczcdt0(W0), sz00)))) | (~aElementOf0(tptp_fun_W1_0(slbdtrb0(tptp_fun_W1_4(szszuzczcdt0(sz00)))), szNzAzT0)) | (~sdtlseqdt0(szszuzczcdt0(tptp_fun_W1_0(slbdtrb0(tptp_fun_W1_4(szszuzczcdt0(sz00))))), sz00)))),
% 94.99/95.21 inference(rewrite,[status(thm)],[])).
% 94.99/95.21 tff(215,plain,
% 94.99/95.21 ((~![W0: $i] : ((~aElementOf0(W0, szNzAzT0)) | (~sdtlseqdt0(szszuzczcdt0(W0), sz00)))) | ((~aElementOf0(tptp_fun_W1_0(slbdtrb0(tptp_fun_W1_4(szszuzczcdt0(sz00)))), szNzAzT0)) | (~sdtlseqdt0(szszuzczcdt0(tptp_fun_W1_0(slbdtrb0(tptp_fun_W1_4(szszuzczcdt0(sz00))))), sz00)))),
% 94.99/95.21 inference(quant_inst,[status(thm)],[])).
% 94.99/95.21 tff(216,plain,
% 94.99/95.21 ((~![W0: $i] : ((~aElementOf0(W0, szNzAzT0)) | (~sdtlseqdt0(szszuzczcdt0(W0), sz00)))) | (~aElementOf0(tptp_fun_W1_0(slbdtrb0(tptp_fun_W1_4(szszuzczcdt0(sz00)))), szNzAzT0)) | (~sdtlseqdt0(szszuzczcdt0(tptp_fun_W1_0(slbdtrb0(tptp_fun_W1_4(szszuzczcdt0(sz00))))), sz00))),
% 94.99/95.21 inference(modus_ponens,[status(thm)],[215, 214])).
% 94.99/95.21 tff(217,plain,
% 94.99/95.21 ($false),
% 94.99/95.21 inference(unit_resolution,[status(thm)],[216, 213, 203, 201])).
% 94.99/95.21 tff(218,plain,((~aElementOf0(tptp_fun_W1_0(slbdtrb0(tptp_fun_W1_4(szszuzczcdt0(sz00)))), szNzAzT0)) | (~sdtlseqdt0(szszuzczcdt0(tptp_fun_W1_0(slbdtrb0(tptp_fun_W1_4(szszuzczcdt0(sz00))))), sz00))), inference(lemma,lemma(discharge,[]))).
% 94.99/95.21 tff(219,plain,
% 94.99/95.21 ((((~aElementOf0(tptp_fun_W1_0(slbdtrb0(tptp_fun_W1_4(szszuzczcdt0(sz00)))), szNzAzT0)) | (~sdtlseqdt0(szszuzczcdt0(tptp_fun_W1_0(slbdtrb0(tptp_fun_W1_4(szszuzczcdt0(sz00))))), sz00))) <=> aElementOf0(tptp_fun_W1_0(slbdtrb0(tptp_fun_W1_4(szszuzczcdt0(sz00)))), slbdtrb0(tptp_fun_W1_4(szszuzczcdt0(sz00))))) | (~((~aElementOf0(tptp_fun_W1_0(slbdtrb0(tptp_fun_W1_4(szszuzczcdt0(sz00)))), szNzAzT0)) | (~sdtlseqdt0(szszuzczcdt0(tptp_fun_W1_0(slbdtrb0(tptp_fun_W1_4(szszuzczcdt0(sz00))))), sz00)))) | (~aElementOf0(tptp_fun_W1_0(slbdtrb0(tptp_fun_W1_4(szszuzczcdt0(sz00)))), slbdtrb0(tptp_fun_W1_4(szszuzczcdt0(sz00)))))),
% 94.99/95.22 inference(tautology,[status(thm)],[])).
% 94.99/95.22 tff(220,plain,
% 94.99/95.22 (((~aElementOf0(tptp_fun_W1_0(slbdtrb0(tptp_fun_W1_4(szszuzczcdt0(sz00)))), szNzAzT0)) | (~sdtlseqdt0(szszuzczcdt0(tptp_fun_W1_0(slbdtrb0(tptp_fun_W1_4(szszuzczcdt0(sz00))))), sz00))) <=> aElementOf0(tptp_fun_W1_0(slbdtrb0(tptp_fun_W1_4(szszuzczcdt0(sz00)))), slbdtrb0(tptp_fun_W1_4(szszuzczcdt0(sz00))))),
% 94.99/95.22 inference(unit_resolution,[status(thm)],[219, 218, 198])).
% 94.99/95.22 tff(221,plain,
% 94.99/95.22 (((~![W0: $i] : ((~aElementOf0(W0, szNzAzT0)) | ![W1: $i] : (~((~((W1 = slbdtrb0(W0)) | (~aSet0(W1)) | (((~aElementOf0(tptp_fun_W2_8(W1, W0), szNzAzT0)) | (~sdtlseqdt0(szszuzczcdt0(tptp_fun_W2_8(W1, W0)), W0))) <=> aElementOf0(tptp_fun_W2_8(W1, W0), W1)))) | (~((~(W1 = slbdtrb0(W0))) | (~((~aSet0(W1)) | (~![W2: $i] : (~(((~aElementOf0(W2, szNzAzT0)) | (~sdtlseqdt0(szszuzczcdt0(W2), W0))) <=> aElementOf0(W2, W1)))))))))))) | ((~aElementOf0(sz00, szNzAzT0)) | ![W1: $i] : (~((~((~aSet0(W1)) | (W1 = slbdtrb0(sz00)) | (((~aElementOf0(tptp_fun_W2_8(W1, sz00), szNzAzT0)) | (~sdtlseqdt0(szszuzczcdt0(tptp_fun_W2_8(W1, sz00)), sz00))) <=> aElementOf0(tptp_fun_W2_8(W1, sz00), W1)))) | (~((~(W1 = slbdtrb0(sz00))) | (~((~aSet0(W1)) | (~![W2: $i] : (~(((~aElementOf0(W2, szNzAzT0)) | (~sdtlseqdt0(szszuzczcdt0(W2), sz00))) <=> aElementOf0(W2, W1)))))))))))) <=> ((~![W0: $i] : ((~aElementOf0(W0, szNzAzT0)) | ![W1: $i] : (~((~((W1 = slbdtrb0(W0)) | (~aSet0(W1)) | (((~aElementOf0(tptp_fun_W2_8(W1, W0), szNzAzT0)) | (~sdtlseqdt0(szszuzczcdt0(tptp_fun_W2_8(W1, W0)), W0))) <=> aElementOf0(tptp_fun_W2_8(W1, W0), W1)))) | (~((~(W1 = slbdtrb0(W0))) | (~((~aSet0(W1)) | (~![W2: $i] : (~(((~aElementOf0(W2, szNzAzT0)) | (~sdtlseqdt0(szszuzczcdt0(W2), W0))) <=> aElementOf0(W2, W1)))))))))))) | (~aElementOf0(sz00, szNzAzT0)) | ![W1: $i] : (~((~((~aSet0(W1)) | (W1 = slbdtrb0(sz00)) | (((~aElementOf0(tptp_fun_W2_8(W1, sz00), szNzAzT0)) | (~sdtlseqdt0(szszuzczcdt0(tptp_fun_W2_8(W1, sz00)), sz00))) <=> aElementOf0(tptp_fun_W2_8(W1, sz00), W1)))) | (~((~(W1 = slbdtrb0(sz00))) | (~((~aSet0(W1)) | (~![W2: $i] : (~(((~aElementOf0(W2, szNzAzT0)) | (~sdtlseqdt0(szszuzczcdt0(W2), sz00))) <=> aElementOf0(W2, W1)))))))))))),
% 94.99/95.22 inference(rewrite,[status(thm)],[])).
% 94.99/95.22 tff(222,plain,
% 94.99/95.22 (((~aElementOf0(sz00, szNzAzT0)) | ![W1: $i] : (~((~((W1 = slbdtrb0(sz00)) | (~aSet0(W1)) | (((~aElementOf0(tptp_fun_W2_8(W1, sz00), szNzAzT0)) | (~sdtlseqdt0(szszuzczcdt0(tptp_fun_W2_8(W1, sz00)), sz00))) <=> aElementOf0(tptp_fun_W2_8(W1, sz00), W1)))) | (~((~(W1 = slbdtrb0(sz00))) | (~((~aSet0(W1)) | (~![W2: $i] : (~(((~aElementOf0(W2, szNzAzT0)) | (~sdtlseqdt0(szszuzczcdt0(W2), sz00))) <=> aElementOf0(W2, W1))))))))))) <=> ((~aElementOf0(sz00, szNzAzT0)) | ![W1: $i] : (~((~((~aSet0(W1)) | (W1 = slbdtrb0(sz00)) | (((~aElementOf0(tptp_fun_W2_8(W1, sz00), szNzAzT0)) | (~sdtlseqdt0(szszuzczcdt0(tptp_fun_W2_8(W1, sz00)), sz00))) <=> aElementOf0(tptp_fun_W2_8(W1, sz00), W1)))) | (~((~(W1 = slbdtrb0(sz00))) | (~((~aSet0(W1)) | (~![W2: $i] : (~(((~aElementOf0(W2, szNzAzT0)) | (~sdtlseqdt0(szszuzczcdt0(W2), sz00))) <=> aElementOf0(W2, W1)))))))))))),
% 94.99/95.22 inference(rewrite,[status(thm)],[])).
% 94.99/95.22 tff(223,plain,
% 94.99/95.22 (((~![W0: $i] : ((~aElementOf0(W0, szNzAzT0)) | ![W1: $i] : (~((~((W1 = slbdtrb0(W0)) | (~aSet0(W1)) | (((~aElementOf0(tptp_fun_W2_8(W1, W0), szNzAzT0)) | (~sdtlseqdt0(szszuzczcdt0(tptp_fun_W2_8(W1, W0)), W0))) <=> aElementOf0(tptp_fun_W2_8(W1, W0), W1)))) | (~((~(W1 = slbdtrb0(W0))) | (~((~aSet0(W1)) | (~![W2: $i] : (~(((~aElementOf0(W2, szNzAzT0)) | (~sdtlseqdt0(szszuzczcdt0(W2), W0))) <=> aElementOf0(W2, W1)))))))))))) | ((~aElementOf0(sz00, szNzAzT0)) | ![W1: $i] : (~((~((W1 = slbdtrb0(sz00)) | (~aSet0(W1)) | (((~aElementOf0(tptp_fun_W2_8(W1, sz00), szNzAzT0)) | (~sdtlseqdt0(szszuzczcdt0(tptp_fun_W2_8(W1, sz00)), sz00))) <=> aElementOf0(tptp_fun_W2_8(W1, sz00), W1)))) | (~((~(W1 = slbdtrb0(sz00))) | (~((~aSet0(W1)) | (~![W2: $i] : (~(((~aElementOf0(W2, szNzAzT0)) | (~sdtlseqdt0(szszuzczcdt0(W2), sz00))) <=> aElementOf0(W2, W1)))))))))))) <=> ((~![W0: $i] : ((~aElementOf0(W0, szNzAzT0)) | ![W1: $i] : (~((~((W1 = slbdtrb0(W0)) | (~aSet0(W1)) | (((~aElementOf0(tptp_fun_W2_8(W1, W0), szNzAzT0)) | (~sdtlseqdt0(szszuzczcdt0(tptp_fun_W2_8(W1, W0)), W0))) <=> aElementOf0(tptp_fun_W2_8(W1, W0), W1)))) | (~((~(W1 = slbdtrb0(W0))) | (~((~aSet0(W1)) | (~![W2: $i] : (~(((~aElementOf0(W2, szNzAzT0)) | (~sdtlseqdt0(szszuzczcdt0(W2), W0))) <=> aElementOf0(W2, W1)))))))))))) | ((~aElementOf0(sz00, szNzAzT0)) | ![W1: $i] : (~((~((~aSet0(W1)) | (W1 = slbdtrb0(sz00)) | (((~aElementOf0(tptp_fun_W2_8(W1, sz00), szNzAzT0)) | (~sdtlseqdt0(szszuzczcdt0(tptp_fun_W2_8(W1, sz00)), sz00))) <=> aElementOf0(tptp_fun_W2_8(W1, sz00), W1)))) | (~((~(W1 = slbdtrb0(sz00))) | (~((~aSet0(W1)) | (~![W2: $i] : (~(((~aElementOf0(W2, szNzAzT0)) | (~sdtlseqdt0(szszuzczcdt0(W2), sz00))) <=> aElementOf0(W2, W1))))))))))))),
% 94.99/95.22 inference(monotonicity,[status(thm)],[222])).
% 94.99/95.22 tff(224,plain,
% 94.99/95.22 (((~![W0: $i] : ((~aElementOf0(W0, szNzAzT0)) | ![W1: $i] : (~((~((W1 = slbdtrb0(W0)) | (~aSet0(W1)) | (((~aElementOf0(tptp_fun_W2_8(W1, W0), szNzAzT0)) | (~sdtlseqdt0(szszuzczcdt0(tptp_fun_W2_8(W1, W0)), W0))) <=> aElementOf0(tptp_fun_W2_8(W1, W0), W1)))) | (~((~(W1 = slbdtrb0(W0))) | (~((~aSet0(W1)) | (~![W2: $i] : (~(((~aElementOf0(W2, szNzAzT0)) | (~sdtlseqdt0(szszuzczcdt0(W2), W0))) <=> aElementOf0(W2, W1)))))))))))) | ((~aElementOf0(sz00, szNzAzT0)) | ![W1: $i] : (~((~((W1 = slbdtrb0(sz00)) | (~aSet0(W1)) | (((~aElementOf0(tptp_fun_W2_8(W1, sz00), szNzAzT0)) | (~sdtlseqdt0(szszuzczcdt0(tptp_fun_W2_8(W1, sz00)), sz00))) <=> aElementOf0(tptp_fun_W2_8(W1, sz00), W1)))) | (~((~(W1 = slbdtrb0(sz00))) | (~((~aSet0(W1)) | (~![W2: $i] : (~(((~aElementOf0(W2, szNzAzT0)) | (~sdtlseqdt0(szszuzczcdt0(W2), sz00))) <=> aElementOf0(W2, W1)))))))))))) <=> ((~![W0: $i] : ((~aElementOf0(W0, szNzAzT0)) | ![W1: $i] : (~((~((W1 = slbdtrb0(W0)) | (~aSet0(W1)) | (((~aElementOf0(tptp_fun_W2_8(W1, W0), szNzAzT0)) | (~sdtlseqdt0(szszuzczcdt0(tptp_fun_W2_8(W1, W0)), W0))) <=> aElementOf0(tptp_fun_W2_8(W1, W0), W1)))) | (~((~(W1 = slbdtrb0(W0))) | (~((~aSet0(W1)) | (~![W2: $i] : (~(((~aElementOf0(W2, szNzAzT0)) | (~sdtlseqdt0(szszuzczcdt0(W2), W0))) <=> aElementOf0(W2, W1)))))))))))) | (~aElementOf0(sz00, szNzAzT0)) | ![W1: $i] : (~((~((~aSet0(W1)) | (W1 = slbdtrb0(sz00)) | (((~aElementOf0(tptp_fun_W2_8(W1, sz00), szNzAzT0)) | (~sdtlseqdt0(szszuzczcdt0(tptp_fun_W2_8(W1, sz00)), sz00))) <=> aElementOf0(tptp_fun_W2_8(W1, sz00), W1)))) | (~((~(W1 = slbdtrb0(sz00))) | (~((~aSet0(W1)) | (~![W2: $i] : (~(((~aElementOf0(W2, szNzAzT0)) | (~sdtlseqdt0(szszuzczcdt0(W2), sz00))) <=> aElementOf0(W2, W1)))))))))))),
% 94.99/95.22 inference(transitivity,[status(thm)],[223, 221])).
% 94.99/95.22 tff(225,plain,
% 94.99/95.22 ((~![W0: $i] : ((~aElementOf0(W0, szNzAzT0)) | ![W1: $i] : (~((~((W1 = slbdtrb0(W0)) | (~aSet0(W1)) | (((~aElementOf0(tptp_fun_W2_8(W1, W0), szNzAzT0)) | (~sdtlseqdt0(szszuzczcdt0(tptp_fun_W2_8(W1, W0)), W0))) <=> aElementOf0(tptp_fun_W2_8(W1, W0), W1)))) | (~((~(W1 = slbdtrb0(W0))) | (~((~aSet0(W1)) | (~![W2: $i] : (~(((~aElementOf0(W2, szNzAzT0)) | (~sdtlseqdt0(szszuzczcdt0(W2), W0))) <=> aElementOf0(W2, W1)))))))))))) | ((~aElementOf0(sz00, szNzAzT0)) | ![W1: $i] : (~((~((W1 = slbdtrb0(sz00)) | (~aSet0(W1)) | (((~aElementOf0(tptp_fun_W2_8(W1, sz00), szNzAzT0)) | (~sdtlseqdt0(szszuzczcdt0(tptp_fun_W2_8(W1, sz00)), sz00))) <=> aElementOf0(tptp_fun_W2_8(W1, sz00), W1)))) | (~((~(W1 = slbdtrb0(sz00))) | (~((~aSet0(W1)) | (~![W2: $i] : (~(((~aElementOf0(W2, szNzAzT0)) | (~sdtlseqdt0(szszuzczcdt0(W2), sz00))) <=> aElementOf0(W2, W1)))))))))))),
% 94.99/95.22 inference(quant_inst,[status(thm)],[])).
% 94.99/95.22 tff(226,plain,
% 94.99/95.22 ((~![W0: $i] : ((~aElementOf0(W0, szNzAzT0)) | ![W1: $i] : (~((~((W1 = slbdtrb0(W0)) | (~aSet0(W1)) | (((~aElementOf0(tptp_fun_W2_8(W1, W0), szNzAzT0)) | (~sdtlseqdt0(szszuzczcdt0(tptp_fun_W2_8(W1, W0)), W0))) <=> aElementOf0(tptp_fun_W2_8(W1, W0), W1)))) | (~((~(W1 = slbdtrb0(W0))) | (~((~aSet0(W1)) | (~![W2: $i] : (~(((~aElementOf0(W2, szNzAzT0)) | (~sdtlseqdt0(szszuzczcdt0(W2), W0))) <=> aElementOf0(W2, W1)))))))))))) | (~aElementOf0(sz00, szNzAzT0)) | ![W1: $i] : (~((~((~aSet0(W1)) | (W1 = slbdtrb0(sz00)) | (((~aElementOf0(tptp_fun_W2_8(W1, sz00), szNzAzT0)) | (~sdtlseqdt0(szszuzczcdt0(tptp_fun_W2_8(W1, sz00)), sz00))) <=> aElementOf0(tptp_fun_W2_8(W1, sz00), W1)))) | (~((~(W1 = slbdtrb0(sz00))) | (~((~aSet0(W1)) | (~![W2: $i] : (~(((~aElementOf0(W2, szNzAzT0)) | (~sdtlseqdt0(szszuzczcdt0(W2), sz00))) <=> aElementOf0(W2, W1))))))))))),
% 94.99/95.22 inference(modus_ponens,[status(thm)],[225, 224])).
% 94.99/95.22 tff(227,plain,
% 94.99/95.22 (![W1: $i] : (~((~((~aSet0(W1)) | (W1 = slbdtrb0(sz00)) | (((~aElementOf0(tptp_fun_W2_8(W1, sz00), szNzAzT0)) | (~sdtlseqdt0(szszuzczcdt0(tptp_fun_W2_8(W1, sz00)), sz00))) <=> aElementOf0(tptp_fun_W2_8(W1, sz00), W1)))) | (~((~(W1 = slbdtrb0(sz00))) | (~((~aSet0(W1)) | (~![W2: $i] : (~(((~aElementOf0(W2, szNzAzT0)) | (~sdtlseqdt0(szszuzczcdt0(W2), sz00))) <=> aElementOf0(W2, W1))))))))))),
% 94.99/95.22 inference(unit_resolution,[status(thm)],[226, 106, 78])).
% 94.99/95.22 tff(228,plain,
% 94.99/95.22 ((~![W1: $i] : (~((~((~aSet0(W1)) | (W1 = slbdtrb0(sz00)) | (((~aElementOf0(tptp_fun_W2_8(W1, sz00), szNzAzT0)) | (~sdtlseqdt0(szszuzczcdt0(tptp_fun_W2_8(W1, sz00)), sz00))) <=> aElementOf0(tptp_fun_W2_8(W1, sz00), W1)))) | (~((~(W1 = slbdtrb0(sz00))) | (~((~aSet0(W1)) | (~![W2: $i] : (~(((~aElementOf0(W2, szNzAzT0)) | (~sdtlseqdt0(szszuzczcdt0(W2), sz00))) <=> aElementOf0(W2, W1))))))))))) | (~((~((~aSet0(slbdtrb0(tptp_fun_W1_4(szszuzczcdt0(sz00))))) | (slbdtrb0(tptp_fun_W1_4(szszuzczcdt0(sz00))) = slbdtrb0(sz00)) | (((~aElementOf0(tptp_fun_W2_8(slbdtrb0(tptp_fun_W1_4(szszuzczcdt0(sz00))), sz00), szNzAzT0)) | (~sdtlseqdt0(szszuzczcdt0(tptp_fun_W2_8(slbdtrb0(tptp_fun_W1_4(szszuzczcdt0(sz00))), sz00)), sz00))) <=> aElementOf0(tptp_fun_W2_8(slbdtrb0(tptp_fun_W1_4(szszuzczcdt0(sz00))), sz00), slbdtrb0(tptp_fun_W1_4(szszuzczcdt0(sz00))))))) | (~((~(slbdtrb0(tptp_fun_W1_4(szszuzczcdt0(sz00))) = slbdtrb0(sz00))) | (~((~aSet0(slbdtrb0(tptp_fun_W1_4(szszuzczcdt0(sz00))))) | (~![W2: $i] : (~(((~aElementOf0(W2, szNzAzT0)) | (~sdtlseqdt0(szszuzczcdt0(W2), sz00))) <=> aElementOf0(W2, slbdtrb0(tptp_fun_W1_4(szszuzczcdt0(sz00)))))))))))))),
% 94.99/95.22 inference(quant_inst,[status(thm)],[])).
% 94.99/95.22 tff(229,plain,
% 94.99/95.22 (~((~((~aSet0(slbdtrb0(tptp_fun_W1_4(szszuzczcdt0(sz00))))) | (slbdtrb0(tptp_fun_W1_4(szszuzczcdt0(sz00))) = slbdtrb0(sz00)) | (((~aElementOf0(tptp_fun_W2_8(slbdtrb0(tptp_fun_W1_4(szszuzczcdt0(sz00))), sz00), szNzAzT0)) | (~sdtlseqdt0(szszuzczcdt0(tptp_fun_W2_8(slbdtrb0(tptp_fun_W1_4(szszuzczcdt0(sz00))), sz00)), sz00))) <=> aElementOf0(tptp_fun_W2_8(slbdtrb0(tptp_fun_W1_4(szszuzczcdt0(sz00))), sz00), slbdtrb0(tptp_fun_W1_4(szszuzczcdt0(sz00))))))) | (~((~(slbdtrb0(tptp_fun_W1_4(szszuzczcdt0(sz00))) = slbdtrb0(sz00))) | (~((~aSet0(slbdtrb0(tptp_fun_W1_4(szszuzczcdt0(sz00))))) | (~![W2: $i] : (~(((~aElementOf0(W2, szNzAzT0)) | (~sdtlseqdt0(szszuzczcdt0(W2), sz00))) <=> aElementOf0(W2, slbdtrb0(tptp_fun_W1_4(szszuzczcdt0(sz00))))))))))))),
% 94.99/95.22 inference(unit_resolution,[status(thm)],[228, 227])).
% 94.99/95.22 tff(230,plain,
% 94.99/95.22 (((~((~aSet0(slbdtrb0(tptp_fun_W1_4(szszuzczcdt0(sz00))))) | (slbdtrb0(tptp_fun_W1_4(szszuzczcdt0(sz00))) = slbdtrb0(sz00)) | (((~aElementOf0(tptp_fun_W2_8(slbdtrb0(tptp_fun_W1_4(szszuzczcdt0(sz00))), sz00), szNzAzT0)) | (~sdtlseqdt0(szszuzczcdt0(tptp_fun_W2_8(slbdtrb0(tptp_fun_W1_4(szszuzczcdt0(sz00))), sz00)), sz00))) <=> aElementOf0(tptp_fun_W2_8(slbdtrb0(tptp_fun_W1_4(szszuzczcdt0(sz00))), sz00), slbdtrb0(tptp_fun_W1_4(szszuzczcdt0(sz00))))))) | (~((~(slbdtrb0(tptp_fun_W1_4(szszuzczcdt0(sz00))) = slbdtrb0(sz00))) | (~((~aSet0(slbdtrb0(tptp_fun_W1_4(szszuzczcdt0(sz00))))) | (~![W2: $i] : (~(((~aElementOf0(W2, szNzAzT0)) | (~sdtlseqdt0(szszuzczcdt0(W2), sz00))) <=> aElementOf0(W2, slbdtrb0(tptp_fun_W1_4(szszuzczcdt0(sz00)))))))))))) | ((~(slbdtrb0(tptp_fun_W1_4(szszuzczcdt0(sz00))) = slbdtrb0(sz00))) | (~((~aSet0(slbdtrb0(tptp_fun_W1_4(szszuzczcdt0(sz00))))) | (~![W2: $i] : (~(((~aElementOf0(W2, szNzAzT0)) | (~sdtlseqdt0(szszuzczcdt0(W2), sz00))) <=> aElementOf0(W2, slbdtrb0(tptp_fun_W1_4(szszuzczcdt0(sz00))))))))))),
% 94.99/95.22 inference(tautology,[status(thm)],[])).
% 95.07/95.29 tff(231,plain,
% 95.07/95.29 ((~(slbdtrb0(tptp_fun_W1_4(szszuzczcdt0(sz00))) = slbdtrb0(sz00))) | (~((~aSet0(slbdtrb0(tptp_fun_W1_4(szszuzczcdt0(sz00))))) | (~![W2: $i] : (~(((~aElementOf0(W2, szNzAzT0)) | (~sdtlseqdt0(szszuzczcdt0(W2), sz00))) <=> aElementOf0(W2, slbdtrb0(tptp_fun_W1_4(szszuzczcdt0(sz00)))))))))),
% 95.07/95.29 inference(unit_resolution,[status(thm)],[230, 229])).
% 95.07/95.29 tff(232,assumption,(slbdtrb0(tptp_fun_W1_4(szszuzczcdt0(sz00))) = slbdtrb0(sz00)), introduced(assumption)).
% 95.07/95.29 tff(233,plain,
% 95.07/95.29 ((~((~(slbdtrb0(tptp_fun_W1_4(szszuzczcdt0(sz00))) = slbdtrb0(sz00))) | (~((~aSet0(slbdtrb0(tptp_fun_W1_4(szszuzczcdt0(sz00))))) | (~![W2: $i] : (~(((~aElementOf0(W2, szNzAzT0)) | (~sdtlseqdt0(szszuzczcdt0(W2), sz00))) <=> aElementOf0(W2, slbdtrb0(tptp_fun_W1_4(szszuzczcdt0(sz00))))))))))) | (~(slbdtrb0(tptp_fun_W1_4(szszuzczcdt0(sz00))) = slbdtrb0(sz00))) | (~((~aSet0(slbdtrb0(tptp_fun_W1_4(szszuzczcdt0(sz00))))) | (~![W2: $i] : (~(((~aElementOf0(W2, szNzAzT0)) | (~sdtlseqdt0(szszuzczcdt0(W2), sz00))) <=> aElementOf0(W2, slbdtrb0(tptp_fun_W1_4(szszuzczcdt0(sz00)))))))))),
% 95.07/95.29 inference(tautology,[status(thm)],[])).
% 95.07/95.29 tff(234,plain,
% 95.07/95.29 ((~((~(slbdtrb0(tptp_fun_W1_4(szszuzczcdt0(sz00))) = slbdtrb0(sz00))) | (~((~aSet0(slbdtrb0(tptp_fun_W1_4(szszuzczcdt0(sz00))))) | (~![W2: $i] : (~(((~aElementOf0(W2, szNzAzT0)) | (~sdtlseqdt0(szszuzczcdt0(W2), sz00))) <=> aElementOf0(W2, slbdtrb0(tptp_fun_W1_4(szszuzczcdt0(sz00))))))))))) | (~((~aSet0(slbdtrb0(tptp_fun_W1_4(szszuzczcdt0(sz00))))) | (~![W2: $i] : (~(((~aElementOf0(W2, szNzAzT0)) | (~sdtlseqdt0(szszuzczcdt0(W2), sz00))) <=> aElementOf0(W2, slbdtrb0(tptp_fun_W1_4(szszuzczcdt0(sz00)))))))))),
% 95.07/95.29 inference(unit_resolution,[status(thm)],[233, 232])).
% 95.07/95.29 tff(235,plain,
% 95.07/95.29 (~((~aSet0(slbdtrb0(tptp_fun_W1_4(szszuzczcdt0(sz00))))) | (~![W2: $i] : (~(((~aElementOf0(W2, szNzAzT0)) | (~sdtlseqdt0(szszuzczcdt0(W2), sz00))) <=> aElementOf0(W2, slbdtrb0(tptp_fun_W1_4(szszuzczcdt0(sz00))))))))),
% 95.07/95.29 inference(unit_resolution,[status(thm)],[234, 231])).
% 95.07/95.29 tff(236,plain,
% 95.07/95.29 (((~aSet0(slbdtrb0(tptp_fun_W1_4(szszuzczcdt0(sz00))))) | (~![W2: $i] : (~(((~aElementOf0(W2, szNzAzT0)) | (~sdtlseqdt0(szszuzczcdt0(W2), sz00))) <=> aElementOf0(W2, slbdtrb0(tptp_fun_W1_4(szszuzczcdt0(sz00)))))))) | ![W2: $i] : (~(((~aElementOf0(W2, szNzAzT0)) | (~sdtlseqdt0(szszuzczcdt0(W2), sz00))) <=> aElementOf0(W2, slbdtrb0(tptp_fun_W1_4(szszuzczcdt0(sz00))))))),
% 95.07/95.29 inference(tautology,[status(thm)],[])).
% 95.07/95.29 tff(237,plain,
% 95.07/95.29 (![W2: $i] : (~(((~aElementOf0(W2, szNzAzT0)) | (~sdtlseqdt0(szszuzczcdt0(W2), sz00))) <=> aElementOf0(W2, slbdtrb0(tptp_fun_W1_4(szszuzczcdt0(sz00))))))),
% 95.07/95.29 inference(unit_resolution,[status(thm)],[236, 235])).
% 95.07/95.29 tff(238,plain,
% 95.07/95.29 ((~![W2: $i] : (~(((~aElementOf0(W2, szNzAzT0)) | (~sdtlseqdt0(szszuzczcdt0(W2), sz00))) <=> aElementOf0(W2, slbdtrb0(tptp_fun_W1_4(szszuzczcdt0(sz00))))))) | (~(((~aElementOf0(tptp_fun_W1_0(slbdtrb0(tptp_fun_W1_4(szszuzczcdt0(sz00)))), szNzAzT0)) | (~sdtlseqdt0(szszuzczcdt0(tptp_fun_W1_0(slbdtrb0(tptp_fun_W1_4(szszuzczcdt0(sz00))))), sz00))) <=> aElementOf0(tptp_fun_W1_0(slbdtrb0(tptp_fun_W1_4(szszuzczcdt0(sz00)))), slbdtrb0(tptp_fun_W1_4(szszuzczcdt0(sz00))))))),
% 95.07/95.29 inference(quant_inst,[status(thm)],[])).
% 95.07/95.29 tff(239,plain,
% 95.07/95.29 ($false),
% 95.07/95.29 inference(unit_resolution,[status(thm)],[238, 237, 220])).
% 95.07/95.29 tff(240,plain,(~(slbdtrb0(tptp_fun_W1_4(szszuzczcdt0(sz00))) = slbdtrb0(sz00))), inference(lemma,lemma(discharge,[]))).
% 95.07/95.29 tff(241,plain,
% 95.07/95.29 ($false),
% 95.07/95.29 inference(unit_resolution,[status(thm)],[188, 240])).
% 95.07/95.29 % SZS output end Proof
% 95.07/95.29 % E exiting
%------------------------------------------------------------------------------