%------------------------------------------------------------------------------
% File : Leo-III---1.8.0
% Problem : SEU585^1 : TPTP v9.3.1. Released v3.7.0.
% Transfm : none
% Format : tptp:raw
% Command : java -Xss128m -Xmx2g -Xms1g -jar /export/starexec/sandbox/solver/bin/leo3.jar /export/starexec/sandbox/benchmark/theBenchmark.p -t 300 -p --atp eprover=/export/starexec/sandbox/solver/bin/externals/eprover --instantiate 39
% Computer : n013.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Wed Sep 30 08:28:39 AM UTC 2026
% Result : Theorem 87.89s 19.70s
% Output : Refutation 89.50s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SEU585^1 : TPTP v9.3.1. Released v3.7.0.
% 0.00/0.08 % Command : java -Xss128m -Xmx2g -Xms1g -jar /export/starexec/sandbox/solver/bin/leo3.jar /export/starexec/sandbox/benchmark/theBenchmark.p -t 300 -p --atp eprover=/export/starexec/sandbox/solver/bin/externals/eprover --instantiate 39
% 0.09/0.20 % Computer : n013.cluster.edu
% 0.09/0.20 % Model : x86_64 x86_64
% 0.09/0.20 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.20 % Memory : 8046.5625MB
% 0.09/0.20 % OS : Linux 6.8.0-71-generic
% 0.09/0.20 % CPULimit : 300
% 0.09/0.20 % WCLimit : 300
% 0.09/0.20 % DateTime : Tue Sep 29 13:51:51 UTC 2026
% 0.09/0.20 % CPUTime :
% 0.09/0.20 Running java -Xss128m -Xmx2g -Xms1g -jar /export/starexec/sandbox/solver/bin/leo3.jar /export/starexec/sandbox/benchmark/theBenchmark.p -t 300 -p --atp eprover=/export/starexec/sandbox/solver/bin/externals/eprover --instantiate 39
% 0.90/0.78 % [INFO] Parsing problem /export/starexec/sandbox/benchmark/theBenchmark.p ...
% 2.15/1.13 % [INFO] Parsing done (350ms).
% 2.15/1.15 % [INFO] Running in sequential loop mode.
% 2.86/1.54 % [INFO] eprover registered as external prover.
% 2.86/1.55 % [INFO] Scanning for conjecture ...
% 3.91/1.93 % [INFO] Found a conjecture (or negated_conjecture) and 0 axioms. Running axiom selection ...
% 3.91/2.01 % [INFO] Axiom selection finished. Selected 0 axioms (removed 0 axioms).
% 3.91/2.02 % [INFO] Problem is higher-order (TPTP THF).
% 3.91/2.02 % [INFO] Type checking passed.
% 3.91/2.03 % [CONFIG] Using configuration: timeout(300) with strategy<name(default),share(1.0),primSubst(3),sos(false),unifierCount(4),uniDepth(8),boolExt(true),choice(true),renaming(true),funcspec(false), domConstr(0),specialInstances(39),restrictUniAttempts(true),termOrdering(CPO)>. Searching for refutation ...
% 87.89/19.69 % External prover 'e' found a proof!
% 87.89/19.69 % [INFO] Killing All external provers ...
% 87.89/19.69 % Time passed: 19351ms (effective reasoning time: 18540ms)
% 87.89/19.69 % Solved by strategy<name(default),share(1.0),primSubst(3),sos(false),unifierCount(4),uniDepth(8),boolExt(true),choice(true),renaming(true),funcspec(false), domConstr(0),specialInstances(39),restrictUniAttempts(true),termOrdering(CPO)>
% 87.89/19.70 % Axioms used in derivation (0):
% 87.89/19.70 % No. of inferences in proof: 533
% 87.89/19.70 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p : 19351 ms resp. 18540 ms w/o parsing
% 89.50/19.97 % SZS output start Refutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% 89.50/19.97 thf(in_decl, type, in: ($i > ($i > $o))).
% 89.50/19.97 thf(exu_decl, type, exu: (($i > $o) > $o)).
% 89.50/19.97 thf(setextAx_decl, type, setextAx: $o).
% 89.50/19.97 thf(emptyset_decl, type, emptyset: $i).
% 89.50/19.97 thf(emptysetAx_decl, type, emptysetAx: $o).
% 89.50/19.97 thf(setadjoin_decl, type, setadjoin: ($i > ($i > $i))).
% 89.50/19.97 thf(setadjoinAx_decl, type, setadjoinAx: $o).
% 89.50/19.97 thf(powerset_decl, type, powerset: ($i > $i)).
% 89.50/19.97 thf(powersetAx_decl, type, powersetAx: $o).
% 89.50/19.97 thf(setunion_decl, type, setunion: ($i > $i)).
% 89.50/19.97 thf(setunionAx_decl, type, setunionAx: $o).
% 89.50/19.97 thf(omega_decl, type, omega: $i).
% 89.50/19.97 thf(omega0Ax_decl, type, omega0Ax: $o).
% 89.50/19.97 thf(omegaSAx_decl, type, omegaSAx: $o).
% 89.50/19.97 thf(omegaIndAx_decl, type, omegaIndAx: $o).
% 89.50/19.97 thf(replAx_decl, type, replAx: $o).
% 89.50/19.97 thf(foundationAx_decl, type, foundationAx: $o).
% 89.50/19.97 thf(wellorderingAx_decl, type, wellorderingAx: $o).
% 89.50/19.97 thf(descr_decl, type, descr: (($i > $o) > $i)).
% 89.50/19.97 thf(descrp_decl, type, descrp: $o).
% 89.50/19.97 thf(dsetconstr_decl, type, dsetconstr: ($i > (($i > $o) > $i))).
% 89.50/19.97 thf(dsetconstrI_decl, type, dsetconstrI: $o).
% 89.50/19.97 thf(dsetconstrEL_decl, type, dsetconstrEL: $o).
% 89.50/19.97 thf(dsetconstrER_decl, type, dsetconstrER: $o).
% 89.50/19.97 thf(exuE1_decl, type, exuE1: $o).
% 89.50/19.97 thf(prop2set_decl, type, prop2set: ($o > $i)).
% 89.50/19.97 thf(prop2setE_decl, type, prop2setE: $o).
% 89.50/19.97 thf(emptysetE_decl, type, emptysetE: $o).
% 89.50/19.97 thf(emptysetimpfalse_decl, type, emptysetimpfalse: $o).
% 89.50/19.97 thf(notinemptyset_decl, type, notinemptyset: $o).
% 89.50/19.97 thf(exuE3e_decl, type, exuE3e: $o).
% 89.50/19.97 thf(setext_decl, type, setext: $o).
% 89.50/19.97 thf(emptyI_decl, type, emptyI: $o).
% 89.50/19.97 thf(noeltsimpempty_decl, type, noeltsimpempty: $o).
% 89.50/19.97 thf(setbeta_decl, type, setbeta: $o).
% 89.50/19.97 thf(nonempty_decl, type, nonempty: ($i > $o)).
% 89.50/19.97 thf(nonemptyE1_decl, type, nonemptyE1: $o).
% 89.50/19.97 thf(nonemptyI_decl, type, nonemptyI: $o).
% 89.50/19.97 thf(nonemptyI1_decl, type, nonemptyI1: $o).
% 89.50/19.97 thf(setadjoinIL_decl, type, setadjoinIL: $o).
% 89.50/19.97 thf(emptyinunitempty_decl, type, emptyinunitempty: $o).
% 89.50/19.97 thf(setadjoinIR_decl, type, setadjoinIR: $o).
% 89.50/19.97 thf(setadjoinE_decl, type, setadjoinE: $o).
% 89.50/19.97 thf(setadjoinOr_decl, type, setadjoinOr: $o).
% 89.50/19.97 thf(setoftrueEq_decl, type, setoftrueEq: $o).
% 89.50/19.97 thf(powersetI_decl, type, powersetI: $o).
% 89.50/19.97 thf(emptyinPowerset_decl, type, emptyinPowerset: $o).
% 89.50/19.97 thf(emptyInPowerset_decl, type, emptyInPowerset: $o).
% 89.50/19.97 thf(powersetE_decl, type, powersetE: $o).
% 89.50/19.97 thf(setunionI_decl, type, setunionI: $o).
% 89.50/19.97 thf(setunionE_decl, type, setunionE: $o).
% 89.50/19.97 thf(subPowSU_decl, type, subPowSU: $o).
% 89.50/19.97 thf(exuE2_decl, type, exuE2: $o).
% 89.50/19.97 thf(nonemptyImpWitness_decl, type, nonemptyImpWitness: $o).
% 89.50/19.97 thf(uniqinunit_decl, type, uniqinunit: $o).
% 89.50/19.97 thf(notinsingleton_decl, type, notinsingleton: $o).
% 89.50/19.97 thf(eqinunit_decl, type, eqinunit: $o).
% 89.50/19.97 thf(singletonsswitch_decl, type, singletonsswitch: $o).
% 89.50/19.97 thf(upairsetE_decl, type, upairsetE: $o).
% 89.50/19.97 thf(upairsetIL_decl, type, upairsetIL: $o).
% 89.50/19.97 thf(upairsetIR_decl, type, upairsetIR: $o).
% 89.50/19.97 thf(emptyE1_decl, type, emptyE1: $o).
% 89.50/19.97 thf(vacuousDall_decl, type, vacuousDall: $o).
% 89.50/19.97 thf(quantDeMorgan1_decl, type, quantDeMorgan1: $o).
% 89.50/19.97 thf(quantDeMorgan2_decl, type, quantDeMorgan2: $o).
% 89.50/19.97 thf(quantDeMorgan3_decl, type, quantDeMorgan3: $o).
% 89.50/19.97 thf(quantDeMorgan4_decl, type, quantDeMorgan4: $o).
% 89.50/19.97 thf(prop2setI_decl, type, prop2setI: $o).
% 89.50/19.97 thf(set2prop_decl, type, set2prop: ($i > $o)).
% 89.50/19.97 thf(prop2set2propI_decl, type, prop2set2propI: $o).
% 89.50/19.97 thf(notdexE_decl, type, notdexE: $o).
% 89.50/19.97 thf(notdallE_decl, type, notdallE: $o).
% 89.50/19.97 thf(exuI1_decl, type, exuI1: $o).
% 89.50/19.97 thf(exuI3_decl, type, exuI3: $o).
% 89.50/19.97 thf(exuI2_decl, type, exuI2: $o).
% 89.50/19.97 thf(inCongP_decl, type, inCongP: $o).
% 89.50/19.97 thf(in__Cong_decl, type, in__Cong: $o).
% 89.50/19.97 thf(exuE3u_decl, type, exuE3u: $o).
% 89.50/19.97 thf(exu__Cong_decl, type, exu__Cong: $o).
% 89.50/19.97 thf(emptyset__Cong_decl, type, emptyset__Cong: $o).
% 89.50/19.97 thf(setadjoin__Cong_decl, type, setadjoin__Cong: $o).
% 89.50/19.97 thf(powerset__Cong_decl, type, powerset__Cong: $o).
% 89.50/19.97 thf(setunion__Cong_decl, type, setunion__Cong: $o).
% 89.50/19.97 thf(omega__Cong_decl, type, omega__Cong: $o).
% 89.50/19.97 thf(exuEu_decl, type, exuEu: $o).
% 89.50/19.97 thf(descr__Cong_decl, type, descr__Cong: $o).
% 89.50/19.97 thf(dsetconstr__Cong_decl, type, dsetconstr__Cong: $o).
% 89.50/19.97 thf(subset_decl, type, subset: ($i > ($i > $o))).
% 89.50/19.97 thf(subsetI1_decl, type, subsetI1: $o).
% 89.50/19.97 thf(eqimpsubset2_decl, type, eqimpsubset2: $o).
% 89.50/19.97 thf(eqimpsubset1_decl, type, eqimpsubset1: $o).
% 89.50/19.97 thf(subsetI2_decl, type, subsetI2: $o).
% 89.50/19.97 thf(emptysetsubset_decl, type, emptysetsubset: $o).
% 89.50/19.97 thf(subsetE_decl, type, subsetE: $o).
% 89.50/19.97 thf(subsetE2_decl, type, subsetE2: $o).
% 89.50/19.97 thf(notsubsetI_decl, type, notsubsetI: $o).
% 89.50/19.97 thf(notequalI1_decl, type, notequalI1: $o).
% 89.50/19.97 thf(notequalI2_decl, type, notequalI2: $o).
% 89.50/19.97 thf(subsetRefl_decl, type, subsetRefl: $o).
% 89.50/19.97 thf(subsetTrans_decl, type, subsetTrans: $o).
% 89.50/19.97 thf(setadjoinSub_decl, type, setadjoinSub: $o).
% 89.50/19.97 thf(setadjoinSub2_decl, type, setadjoinSub2: $o).
% 89.50/19.97 thf(subset2powerset_decl, type, subset2powerset: $o).
% 89.50/19.97 thf(setextsub_decl, type, setextsub: $o).
% 89.50/19.97 thf(subsetemptysetimpeq_decl, type, subsetemptysetimpeq: $o).
% 89.50/19.97 thf(powersetI1_decl, type, powersetI1: $o).
% 89.50/19.97 thf(powersetE1_decl, type, powersetE1: $o).
% 89.50/19.97 thf(inPowerset_decl, type, inPowerset: $o).
% 89.50/19.97 thf(powersetsubset_decl, type, powersetsubset: $o).
% 89.50/19.97 thf(sepInPowerset_decl, type, sepInPowerset: $o).
% 89.50/19.97 thf(sepSubset_decl, type, sepSubset: $o).
% 89.50/19.97 thf(binunion_decl, type, binunion: ($i > ($i > $i))).
% 89.50/19.97 thf(binunionIL_decl, type, binunionIL: $o).
% 89.50/19.97 thf(upairset2IR_decl, type, upairset2IR: $o).
% 89.50/19.97 thf(binunionIR_decl, type, binunionIR: $o).
% 89.50/19.97 thf(sk1_decl, type, sk1: ($i > ($i > $i))).
% 89.50/19.97 thf(sk2_decl, type, sk2: ($i > $i)).
% 89.50/19.97 thf(sk3_decl, type, sk3: ($i > (($i > ($i > $o)) > $i))).
% 89.50/19.97 thf(sk4_decl, type, sk4: ($i > ($i > (($i > ($i > $o)) > $i)))).
% 89.50/19.97 thf(sk5_decl, type, sk5: ($i > (($i > ($i > $o)) > $i))).
% 89.50/19.97 thf(sk6_decl, type, sk6: ($i > $i)).
% 89.50/19.97 thf(sk7_decl, type, sk7: ($i > $i)).
% 89.50/19.97 thf(sk8_decl, type, sk8: ($i > ($i > ($i > $i)))).
% 89.50/19.97 thf(sk9_decl, type, sk9: ($i > ($i > $o))).
% 89.50/19.97 thf(sk10_decl, type, sk10: ($i > ($i > $i))).
% 89.50/19.97 thf(sk11_decl, type, sk11: ($i > ($i > $i))).
% 89.50/19.97 thf(sk12_decl, type, sk12: ($i > ($i > $i))).
% 89.50/19.97 thf(sk13_decl, type, sk13: ($i > (($i > $o) > $i))).
% 89.50/19.97 thf(sk14_decl, type, sk14: ($i > (($i > $o) > $i))).
% 89.50/19.97 thf(sk15_decl, type, sk15: (($i > $o) > $i)).
% 89.50/19.97 thf(sk16_decl, type, sk16: ($i > ($i > $i))).
% 89.50/19.97 thf(sk17_decl, type, sk17: ($i > ($i > $i))).
% 89.50/19.97 thf(sk18_decl, type, sk18: ($i > $i)).
% 89.50/19.97 thf(sk19_decl, type, sk19: ($i > $i)).
% 89.50/19.97 thf(sk20_decl, type, sk20: ($i > $i)).
% 89.50/19.97 thf(sk21_decl, type, sk21: ($i > ($i > $i))).
% 89.50/19.97 thf(sk22_decl, type, sk22: ($o > ($i > ($i > $i)))).
% 89.50/19.97 thf(sk23_decl, type, sk23: ($i > (($i > $o) > $i))).
% 89.50/19.97 thf(sk24_decl, type, sk24: (($i > $o) > $i)).
% 89.50/19.97 thf(sk25_decl, type, sk25: ($i > $i)).
% 89.50/19.97 thf(sk26_decl, type, sk26: (($i > $o) > ($i > $i))).
% 89.50/19.97 thf(sk27_decl, type, sk27: (($i > $o) > ($i > $i))).
% 89.50/19.97 thf(sk28_decl, type, sk28: (($i > $o) > ($i > $i))).
% 89.50/19.97 thf(sk29_decl, type, sk29: (($i > $o) > ($i > $i))).
% 89.50/19.97 thf(sk30_decl, type, sk30: (($i > $o) > ($i > $i))).
% 89.50/19.97 thf(sk31_decl, type, sk31: (($i > $o) > ($i > $i))).
% 89.50/19.97 thf(sk32_decl, type, sk32: (($i > $o) > $i)).
% 89.50/19.97 thf(sk33_decl, type, sk33: (($i > $o) > $i)).
% 89.50/19.97 thf(sk34_decl, type, sk34: (($i > $o) > $i)).
% 89.50/19.97 thf(sk35_decl, type, sk35: ($i > (($i > $o) > $i))).
% 89.50/19.97 thf(sk36_decl, type, sk36: (($i > $o) > $i)).
% 89.50/19.97 thf(sk37_decl, type, sk37: ($i > (($i > $o) > $i))).
% 89.50/19.97 thf(sk38_decl, type, sk38: (($i > $o) > (($i > $o) > $i))).
% 89.50/19.97 thf(sk39_decl, type, sk39: (($i > $o) > (($i > $o) > $i))).
% 89.50/19.97 thf(sk40_decl, type, sk40: ($i > (($i > $o) > $i))).
% 89.50/19.97 thf(sk41_decl, type, sk41: (($i > $o) > (($i > $o) > $o))).
% 89.50/19.97 thf(sk42_decl, type, sk42: (($i > $o) > (($i > $o) > $i))).
% 89.50/19.97 thf(sk43_decl, type, sk43: (($i > $o) > (($i > $o) > $i))).
% 89.50/19.97 thf(sk44_decl, type, sk44: ($i > (($i > $o) > (($i > $o) > $i)))).
% 89.50/19.97 thf(sk45_decl, type, sk45: ($i > (($i > $o) > (($i > $o) > $i)))).
% 89.50/19.97 thf(sk46_decl, type, sk46: (($i > $o) > (($i > $o) > ($i > ($i > $i))))).
% 89.50/19.97 thf(sk47_decl, type, sk47: (($i > $o) > (($i > $o) > ($i > ($i > $i))))).
% 89.50/19.97 thf(sk48_decl, type, sk48: ($i > ($i > $i))).
% 89.50/19.97 thf(sk49_decl, type, sk49: ($i > ($i > $i))).
% 89.50/19.97 thf(sk50_decl, type, sk50: $i).
% 89.50/19.97 thf(sk51_decl, type, sk51: $i).
% 89.50/19.97 thf(sk52_decl, type, sk52: $i).
% 89.50/19.97 thf(sk53_decl, type, sk53: $o).
% 89.50/19.97 thf(sk174_decl, type, sk174: $i).
% 89.50/19.97 thf(sk177_decl, type, sk177: $i).
% 89.50/19.97 thf(sk200_decl, type, sk200: $i).
% 89.50/19.97 thf(sk203_decl, type, sk203: $i).
% 89.50/19.97 thf(exu_def, definition, exu = (^ [A:($i > $o)]: ? [B:$i]: ((A @ B) & ! [C:$i]: ((A @ C) => (B = C)))) ).
% 89.50/19.97 thf(setextAx_def, definition, setextAx = (! [A:$i,B:$i]: ((! [C:$i]: ((in @ C @ A) = (in @ C @ B))) => (A = B))) ).
% 89.50/19.97 thf(emptysetAx_def, definition, emptysetAx = (! [A:$i]: ~ (in @ A @ emptyset)) ).
% 89.50/19.97 thf(setadjoinAx_def, definition, setadjoinAx = (! [A:$i,B:$i,C:$i]: ((in @ C @ (setadjoin @ A @ B)) = ((C = A) | (in @ C @ B)))) ).
% 89.50/19.97 thf(powersetAx_def, definition, powersetAx = (! [A:$i,B:$i]: ((in @ B @ (powerset @ A)) = (! [C:$i]: ((in @ C @ B) => (in @ C @ A))))) ).
% 89.50/19.97 thf(setunionAx_def, definition, setunionAx = (! [A:$i,B:$i]: ((in @ B @ (setunion @ A)) = (? [C:$i]: ((in @ B @ C) & (in @ C @ A))))) ).
% 89.50/19.97 thf(omega0Ax_def, definition, omega0Ax = (in @ emptyset @ omega) ).
% 89.50/19.97 thf(omegaSAx_def, definition, omegaSAx = (! [A:$i]: ((in @ A @ omega) => (in @ (setadjoin @ A @ A) @ omega))) ).
% 89.50/19.97 thf(omegaIndAx_def, definition, omegaIndAx = (! [A:$i]: (((in @ emptyset @ A) & ! [B:$i]: (((in @ B @ omega) & (in @ B @ A)) => (in @ (setadjoin @ B @ B) @ A))) => (! [B:$i]: ((in @ B @ omega) => (in @ B @ A))))) ).
% 89.50/19.97 thf(replAx_def, definition, replAx = (! [A:($i > ($i > $o)),B:$i]: ((! [C:$i]: ((in @ C @ B) => (exu @ (A @ C)))) => (? [C:$i]: ! [D:$i]: ((in @ D @ C) = (? [E:$i]: ((in @ E @ B) & (A @ E @ D))))))) ).
% 89.50/19.97 thf(foundationAx_def, definition, foundationAx = (! [A:$i]: ((? [B:$i]: (in @ B @ A)) => (? [B:$i]: ((in @ B @ A) & ~ (? [C:$i]: ((in @ C @ B) & (in @ C @ A))))))) ).
% 89.50/19.97 thf(wellorderingAx_def, definition, wellorderingAx = (! [A:$i]: ? [B:$i]: (! [C:$i]: ((in @ C @ B) => (! [D:$i]: ((in @ D @ C) => (in @ D @ A)))) & ! [C:$i,D:$i]: (((in @ C @ A) & (in @ D @ A)) => ((! [E:$i]: ((in @ E @ B) => ((in @ C @ E) = (in @ D @ E)))) => (C = D))) & ! [C:$i,D:$i]: (((in @ C @ B) & (in @ D @ B)) => (! [E:$i]: ((in @ E @ C) => (in @ E @ D)) | ! [E:$i]: ((in @ E @ D) => (in @ E @ C)))) & ! [C:$i]: ((! [D:$i]: ((in @ D @ C) => (in @ D @ A)) & ? [D:$i]: (in @ D @ C)) => (? [D:$i,E:$i]: ((in @ D @ B) & (in @ E @ C) & ~ (? [F:$i]: ((in @ F @ D) & (in @ F @ C))) & ! [F:$i]: ((in @ F @ B) => (! [G:$i]: ((in @ G @ F) => (in @ G @ D)) | (in @ E @ F)))))))) ).
% 89.50/19.97 thf(descrp_def, definition, descrp = (! [A:($i > $o)]: ((exu @ (A)) => (A @ (descr @ (A))))) ).
% 89.50/19.97 thf(dsetconstrI_def, definition, dsetconstrI = (! [A:$i,B:($i > $o),C:$i]: ((in @ C @ A) => ((B @ C) => (in @ C @ (dsetconstr @ A @ (B)))))) ).
% 89.50/19.97 thf(dsetconstrEL_def, definition, dsetconstrEL = (! [A:$i,B:($i > $o),C:$i]: ((in @ C @ (dsetconstr @ A @ (B))) => (in @ C @ A))) ).
% 89.50/19.97 thf(dsetconstrER_def, definition, dsetconstrER = (! [A:$i,B:($i > $o),C:$i]: ((in @ C @ (dsetconstr @ A @ (B))) => (B @ C))) ).
% 89.50/19.97 thf(exuE1_def, definition, exuE1 = (! [A:($i > $o)]: ((exu @ (A)) => (? [B:$i]: ((A @ B) & ! [C:$i]: ((A @ C) => (B = C)))))) ).
% 89.50/19.97 thf(prop2setE_def, definition, prop2setE = (! [A:$o,B:$i]: ((in @ B @ (prop2set @ A)) => (A))) ).
% 89.50/19.97 thf(emptysetE_def, definition, emptysetE = (! [A:$i]: ((in @ A @ emptyset) => (! [B:$o]: (B)))) ).
% 89.50/19.97 thf(emptysetimpfalse_def, definition, emptysetimpfalse = (! [A:$i]: ((in @ A @ emptyset) => (($false)))) ).
% 89.50/19.97 thf(notinemptyset_def, definition, notinemptyset = (! [A:$i]: ~ (in @ A @ emptyset)) ).
% 89.50/19.97 thf(exuE3e_def, definition, exuE3e = (! [A:($i > $o)]: ((exu @ (A)) => (? [B:$i]: (A @ B)))) ).
% 89.50/19.97 thf(setext_def, definition, setext = (! [A:$i,B:$i]: ((! [C:$i]: ((in @ C @ A) => (in @ C @ B))) => ((! [C:$i]: ((in @ C @ B) => (in @ C @ A))) => (A = B)))) ).
% 89.50/19.97 thf(emptyI_def, definition, emptyI = (! [A:$i]: ((! [B:$i]: ~ (in @ B @ A)) => (A = emptyset))) ).
% 89.50/19.97 thf(noeltsimpempty_def, definition, noeltsimpempty = (! [A:$i]: ((! [B:$i]: ~ (in @ B @ A)) => (A = emptyset))) ).
% 89.50/19.97 thf(setbeta_def, definition, setbeta = (! [A:$i,B:($i > $o),C:$i]: ((in @ C @ A) => ((in @ C @ (dsetconstr @ A @ (B))) = (B @ C)))) ).
% 89.50/19.97 thf(nonempty_def, definition, nonempty = (^ [A:$i]: (A != emptyset)) ).
% 89.50/19.97 thf(nonemptyE1_def, definition, nonemptyE1 = (! [A:$i]: ((nonempty @ A) => (? [B:$i]: (in @ B @ A)))) ).
% 89.50/19.97 thf(nonemptyI_def, definition, nonemptyI = (! [A:$i,B:($i > $o),C:$i]: ((in @ C @ A) => ((B @ C) => (nonempty @ (dsetconstr @ A @ (B)))))) ).
% 89.50/19.97 thf(nonemptyI1_def, definition, nonemptyI1 = (! [A:$i]: ((? [B:$i]: (in @ B @ A)) => (nonempty @ A))) ).
% 89.50/19.97 thf(setadjoinIL_def, definition, setadjoinIL = (! [A:$i,B:$i]: (in @ A @ (setadjoin @ A @ B))) ).
% 89.50/19.97 thf(emptyinunitempty_def, definition, emptyinunitempty = (in @ emptyset @ (setadjoin @ emptyset @ emptyset)) ).
% 89.50/19.97 thf(setadjoinIR_def, definition, setadjoinIR = (! [A:$i,B:$i,C:$i]: ((in @ C @ B) => (in @ C @ (setadjoin @ A @ B)))) ).
% 89.50/19.97 thf(setadjoinE_def, definition, setadjoinE = (! [A:$i,B:$i,C:$i]: ((in @ C @ (setadjoin @ A @ B)) => (! [D:$o]: (((C = A) => (D)) => (((in @ C @ B) => (D)) => (D)))))) ).
% 89.50/19.97 thf(setadjoinOr_def, definition, setadjoinOr = (! [A:$i,B:$i,C:$i]: ((in @ C @ (setadjoin @ A @ B)) => ((C = A) | (in @ C @ B)))) ).
% 89.50/19.97 thf(setoftrueEq_def, definition, setoftrueEq = (! [A:$i]: ((dsetconstr @ A @ (^ [B:$i]: (($true)))) = A)) ).
% 89.50/19.97 thf(powersetI_def, definition, powersetI = (! [A:$i,B:$i]: ((! [C:$i]: ((in @ C @ B) => (in @ C @ A))) => (in @ B @ (powerset @ A)))) ).
% 89.50/19.97 thf(emptyinPowerset_def, definition, emptyinPowerset = (! [A:$i]: (in @ emptyset @ (powerset @ A))) ).
% 89.50/19.97 thf(emptyInPowerset_def, definition, emptyInPowerset = (! [A:$i]: (in @ emptyset @ (powerset @ A))) ).
% 89.50/19.97 thf(powersetE_def, definition, powersetE = (! [A:$i,B:$i,C:$i]: ((in @ B @ (powerset @ A)) => ((in @ C @ B) => (in @ C @ A)))) ).
% 89.50/19.97 thf(setunionI_def, definition, setunionI = (! [A:$i,B:$i,C:$i]: ((in @ B @ C) => ((in @ C @ A) => (in @ B @ (setunion @ A))))) ).
% 89.50/19.97 thf(setunionE_def, definition, setunionE = (! [A:$i,B:$i]: ((in @ B @ (setunion @ A)) => (! [C:$o]: ((! [D:$i]: ((in @ B @ D) => ((in @ D @ A) => (C)))) => (C))))) ).
% 89.50/19.97 thf(subPowSU_def, definition, subPowSU = (! [A:$i,B:$i]: ((in @ B @ A) => (in @ B @ (powerset @ (setunion @ A))))) ).
% 89.50/19.97 thf(exuE2_def, definition, exuE2 = (! [A:($i > $o)]: ((exu @ (A)) => (? [B:$i]: ! [C:$i]: ((A @ C) = (C = B))))) ).
% 89.50/19.97 thf(nonemptyImpWitness_def, definition, nonemptyImpWitness = (! [A:$i]: ((nonempty @ A) => (? [B:$i]: ((in @ B @ A) & (($true)))))) ).
% 89.50/19.97 thf(uniqinunit_def, definition, uniqinunit = (! [A:$i,B:$i]: ((in @ A @ (setadjoin @ B @ emptyset)) => (A = B))) ).
% 89.50/19.97 thf(notinsingleton_def, definition, notinsingleton = (! [A:$i,B:$i]: ((A != B) => (~ (in @ B @ (setadjoin @ A @ emptyset))))) ).
% 89.50/19.97 thf(eqinunit_def, definition, eqinunit = (! [A:$i,B:$i]: ((A = B) => (in @ A @ (setadjoin @ B @ emptyset)))) ).
% 89.50/19.97 thf(singletonsswitch_def, definition, singletonsswitch = (! [A:$i,B:$i]: ((in @ A @ (setadjoin @ B @ emptyset)) => (in @ B @ (setadjoin @ A @ emptyset)))) ).
% 89.50/19.97 thf(upairsetE_def, definition, upairsetE = (! [A:$i,B:$i,C:$i]: ((in @ C @ (setadjoin @ A @ (setadjoin @ B @ emptyset))) => ((C = A) | (C = B)))) ).
% 89.50/19.97 thf(upairsetIL_def, definition, upairsetIL = (! [A:$i,B:$i]: (in @ A @ (setadjoin @ A @ (setadjoin @ B @ emptyset)))) ).
% 89.50/19.97 thf(upairsetIR_def, definition, upairsetIR = (! [A:$i,B:$i]: (in @ B @ (setadjoin @ A @ (setadjoin @ B @ emptyset)))) ).
% 89.50/19.97 thf(emptyE1_def, definition, emptyE1 = (! [A:$i,B:($i > $o)]: ((? [C:$i]: ((in @ C @ A) & (B @ C))) => (((dsetconstr @ A @ (B)) = emptyset) => (($false))))) ).
% 89.50/19.97 thf(vacuousDall_def, definition, vacuousDall = (! [A:($i > $o),B:$i]: ((in @ B @ emptyset) => (A @ B))) ).
% 89.50/19.97 thf(quantDeMorgan1_def, definition, quantDeMorgan1 = (! [A:$i,B:($i > $o)]: ((~ (! [C:$i]: ((in @ C @ A) => (B @ C)))) => (? [C:$i]: ((in @ C @ A) & ~ (B @ C))))) ).
% 89.50/19.97 thf(quantDeMorgan2_def, definition, quantDeMorgan2 = (! [A:$i,B:($i > $o)]: ((! [C:$i]: ((in @ C @ A) => (~ (B @ C)))) => (~ (? [C:$i]: ((in @ C @ A) & (B @ C)))))) ).
% 89.50/19.97 thf(quantDeMorgan3_def, definition, quantDeMorgan3 = (! [A:$i,B:($i > $o)]: ((~ (? [C:$i]: ((in @ C @ A) & (B @ C)))) => (! [C:$i]: ((in @ C @ A) => (~ (B @ C)))))) ).
% 89.50/19.97 thf(quantDeMorgan4_def, definition, quantDeMorgan4 = (! [A:$i,B:($i > $o)]: ((? [C:$i]: ((in @ C @ A) & ~ (B @ C))) => (~ (! [C:$i]: ((in @ C @ A) => (B @ C)))))) ).
% 89.50/19.97 thf(prop2setI_def, definition, prop2setI = (! [A:$o]: ((A) => (in @ emptyset @ (prop2set @ A)))) ).
% 89.50/19.97 thf(prop2set2propI_def, definition, prop2set2propI = (! [A:$o]: ((A) => (set2prop @ (prop2set @ A)))) ).
% 89.50/19.97 thf(notdexE_def, definition, notdexE = (! [A:$i,B:($i > $o)]: ((~ (? [C:$i]: ((in @ C @ A) & (B @ C)))) => (! [C:$i]: ((in @ C @ A) => (~ (B @ C)))))) ).
% 89.50/19.97 thf(notdallE_def, definition, notdallE = (! [A:$i,B:($i > $o)]: ((~ (! [C:$i]: ((in @ C @ A) => (B @ C)))) => (? [C:$i]: ((in @ C @ A) & ~ (B @ C))))) ).
% 89.50/19.97 thf(exuI1_def, definition, exuI1 = (! [A:($i > $o)]: ((? [B:$i]: ((A @ B) & ! [C:$i]: ((A @ C) => (B = C)))) => (exu @ (A)))) ).
% 89.50/19.97 thf(exuI3_def, definition, exuI3 = (! [A:($i > $o)]: ((? [B:$i]: (A @ B)) => ((! [B:$i,C:$i]: ((A @ B) => ((A @ C) => (B = C)))) => (exu @ (A))))) ).
% 89.50/19.97 thf(exuI2_def, definition, exuI2 = (! [A:($i > $o)]: ((? [B:$i]: ! [C:$i]: ((A @ C) = (C = B))) => (exu @ (A)))) ).
% 89.50/19.97 thf(inCongP_def, definition, inCongP = (! [A:$i,B:$i]: ((A = B) => (! [C:$i,D:$i]: ((C = D) => ((in @ C @ A) => (in @ D @ B)))))) ).
% 89.50/19.97 thf(in__Cong_def, definition, in__Cong = (! [A:$i,B:$i]: ((A = B) => (! [C:$i,D:$i]: ((C = D) => ((in @ C @ A) = (in @ D @ B)))))) ).
% 89.50/19.97 thf(exuE3u_def, definition, exuE3u = (! [A:($i > $o)]: ((exu @ (A)) => (! [B:$i,C:$i]: ((A @ B) => ((A @ C) => (B = C)))))) ).
% 89.50/19.97 thf(exu__Cong_def, definition, exu__Cong = (! [A:($i > $o),B:($i > $o)]: ((! [C:$i,D:$i]: ((C = D) => ((A @ C) = (B @ D)))) => ((exu @ (A)) = (exu @ (B))))) ).
% 89.50/19.97 thf(emptyset__Cong_def, definition, emptyset__Cong = (emptyset = emptyset) ).
% 89.50/19.97 thf(setadjoin__Cong_def, definition, setadjoin__Cong = (! [A:$i,B:$i]: ((A = B) => (! [C:$i,D:$i]: ((C = D) => ((setadjoin @ A @ C) = (setadjoin @ B @ D)))))) ).
% 89.50/19.97 thf(powerset__Cong_def, definition, powerset__Cong = (! [A:$i,B:$i]: ((A = B) => ((powerset @ A) = (powerset @ B)))) ).
% 89.50/19.97 thf(setunion__Cong_def, definition, setunion__Cong = (! [A:$i,B:$i]: ((A = B) => ((setunion @ A) = (setunion @ B)))) ).
% 89.50/19.97 thf(omega__Cong_def, definition, omega__Cong = (omega = omega) ).
% 89.50/19.97 thf(exuEu_def, definition, exuEu = (! [A:($i > $o)]: ((exu @ (A)) => (! [B:$i,C:$i]: ((A @ B) => ((A @ C) => (B = C)))))) ).
% 89.50/19.97 thf(descr__Cong_def, definition, descr__Cong = (! [A:($i > $o),B:($i > $o)]: ((! [C:$i,D:$i]: ((C = D) => ((A @ C) = (B @ D)))) => ((exu @ (A)) => ((exu @ (B)) => ((descr @ (A)) = (descr @ (B))))))) ).
% 89.50/19.97 thf(dsetconstr__Cong_def, definition, dsetconstr__Cong = (! [A:$i,B:$i]: ((A = B) => (! [C:($i > $o),D:($i > $o)]: ((! [E:$i]: ((in @ E @ A) => (! [F:$i]: ((in @ F @ B) => ((E = F) => ((C @ E) = (D @ F))))))) => ((dsetconstr @ A @ (C)) = (dsetconstr @ B @ (D))))))) ).
% 89.50/19.97 thf(subsetI1_def, definition, subsetI1 = (! [A:$i,B:$i]: ((! [C:$i]: ((in @ C @ A) => (in @ C @ B))) => (subset @ A @ B))) ).
% 89.50/19.97 thf(eqimpsubset2_def, definition, eqimpsubset2 = (! [A:$i,B:$i]: ((A = B) => (subset @ B @ A))) ).
% 89.50/19.97 thf(eqimpsubset1_def, definition, eqimpsubset1 = (! [A:$i,B:$i]: ((A = B) => (subset @ A @ B))) ).
% 89.50/19.97 thf(subsetI2_def, definition, subsetI2 = (! [A:$i,B:$i]: ((! [C:$i]: ((in @ C @ A) => (in @ C @ B))) => (subset @ A @ B))) ).
% 89.50/19.97 thf(emptysetsubset_def, definition, emptysetsubset = (! [A:$i]: (subset @ emptyset @ A)) ).
% 89.50/19.97 thf(subsetE_def, definition, subsetE = (! [A:$i,B:$i,C:$i]: ((subset @ A @ B) => ((in @ C @ A) => (in @ C @ B)))) ).
% 89.50/19.97 thf(subsetE2_def, definition, subsetE2 = (! [A:$i,B:$i,C:$i]: ((subset @ A @ B) => ((~ (in @ C @ B)) => (~ (in @ C @ A))))) ).
% 89.50/19.97 thf(notsubsetI_def, definition, notsubsetI = (! [A:$i,B:$i,C:$i]: ((in @ C @ A) => ((~ (in @ C @ B)) => (~ (subset @ A @ B))))) ).
% 89.50/19.97 thf(notequalI1_def, definition, notequalI1 = (! [A:$i,B:$i]: ((~ (subset @ A @ B)) => (A != B))) ).
% 89.50/19.97 thf(notequalI2_def, definition, notequalI2 = (! [A:$i,B:$i,C:$i]: ((in @ C @ A) => ((~ (in @ C @ B)) => (A != B)))) ).
% 89.50/19.97 thf(subsetRefl_def, definition, subsetRefl = (! [A:$i]: (subset @ A @ A)) ).
% 89.50/19.97 thf(subsetTrans_def, definition, subsetTrans = (! [A:$i,B:$i,C:$i]: ((subset @ A @ B) => ((subset @ B @ C) => (subset @ A @ C)))) ).
% 89.50/19.97 thf(setadjoinSub_def, definition, setadjoinSub = (! [A:$i,B:$i]: (subset @ B @ (setadjoin @ A @ B))) ).
% 89.50/19.97 thf(setadjoinSub2_def, definition, setadjoinSub2 = (! [A:$i,B:$i,C:$i]: ((subset @ A @ C) => (subset @ A @ (setadjoin @ B @ C)))) ).
% 89.50/19.97 thf(subset2powerset_def, definition, subset2powerset = (! [A:$i,B:$i]: ((subset @ A @ B) => (in @ A @ (powerset @ B)))) ).
% 89.50/19.97 thf(setextsub_def, definition, setextsub = (! [A:$i,B:$i]: ((subset @ A @ B) => ((subset @ B @ A) => (A = B)))) ).
% 89.50/19.97 thf(subsetemptysetimpeq_def, definition, subsetemptysetimpeq = (! [A:$i]: ((subset @ A @ emptyset) => (A = emptyset))) ).
% 89.50/19.97 thf(powersetI1_def, definition, powersetI1 = (! [A:$i,B:$i]: ((subset @ B @ A) => (in @ B @ (powerset @ A)))) ).
% 89.50/19.97 thf(powersetE1_def, definition, powersetE1 = (! [A:$i,B:$i]: ((in @ B @ (powerset @ A)) => (subset @ B @ A))) ).
% 89.50/19.97 thf(inPowerset_def, definition, inPowerset = (! [A:$i]: (in @ A @ (powerset @ A))) ).
% 89.50/19.97 thf(powersetsubset_def, definition, powersetsubset = (! [A:$i,B:$i]: ((subset @ A @ B) => (subset @ (powerset @ A) @ (powerset @ B)))) ).
% 89.50/19.97 thf(sepInPowerset_def, definition, sepInPowerset = (! [A:$i,B:($i > $o)]: (in @ (dsetconstr @ A @ (B)) @ (powerset @ A))) ).
% 89.50/19.97 thf(sepSubset_def, definition, sepSubset = (! [A:$i,B:($i > $o)]: (subset @ (dsetconstr @ A @ (B)) @ A)) ).
% 89.50/19.97 thf(binunion_def, definition, binunion = (^ [A:$i,B:$i]: (setunion @ (setadjoin @ A @ (setadjoin @ B @ emptyset)))) ).
% 89.50/19.97 thf(binunionIL_def, definition, binunionIL = (! [A:$i,B:$i,C:$i]: ((in @ C @ A) => (in @ C @ (binunion @ A @ B)))) ).
% 89.50/19.97 thf(upairset2IR_def, definition, upairset2IR = (! [A:$i,B:$i]: (in @ B @ (setadjoin @ A @ (setadjoin @ B @ emptyset)))) ).
% 89.50/19.97 thf(binunionIR_def, definition, binunionIR = (! [A:$i,B:$i,C:$i]: ((in @ C @ B) => (in @ C @ (binunion @ A @ B)))) ).
% 89.50/19.97 thf(sk1_def, definition, sk1 = (^ [A:$i,B:$i]: (@+ [C:$i]: ~ ((in @ C @ B) = (in @ C @ A)))) ).
% 89.50/19.97 thf(sk2_def, definition, sk2 = (^ [A:$i]: (@+ [B:$i]: ~ (((in @ B @ omega) & (in @ B @ A)) => (in @ (setadjoin @ B @ B) @ A)))) ).
% 89.50/19.97 thf(sk3_def, definition, sk3 = (^ [A:$i,B:($i > ($i > $o))]: (@+ [C:$i]: ~ ((in @ C @ A) => (? [D:$i]: ((B @ C @ D) & ! [E:$i]: ((B @ C @ E) => (D = E))))))) ).
% 89.50/19.97 thf(sk4_def, definition, sk4 = (^ [A:$i,B:$i,C:($i > ($i > $o))]: (@+ [D:$i]: ~ ((C @ (sk3 @ B @ C) @ D) => (A = D)))) ).
% 89.50/19.97 thf(sk5_def, definition, sk5 = (^ [A:$i,B:($i > ($i > $o))]: (@+ [C:$i]: ! [D:$i]: ((in @ D @ C) = (? [E:$i]: ((in @ E @ A) & (B @ E @ D)))))) ).
% 89.50/19.97 thf(sk6_def, definition, sk6 = (^ [A:$i]: (@+ [B:$i]: ((in @ B @ A) & ~ (? [C:$i]: ((in @ C @ B) & (in @ C @ A)))))) ).
% 89.50/19.97 thf(sk7_def, definition, sk7 = (^ [A:$i]: (@+ [B:$i]: (! [C:$i]: ((in @ C @ B) => (! [D:$i]: ((in @ D @ C) => (in @ D @ A)))) & ! [C:$i,D:$i]: (((in @ C @ A) & (in @ D @ A)) => ((! [E:$i]: ((in @ E @ B) => ((in @ C @ E) = (in @ D @ E)))) => (C = D))) & ! [C:$i,D:$i]: (((in @ C @ B) & (in @ D @ B)) => (! [E:$i]: ((in @ E @ C) => (in @ E @ D)) | ! [E:$i]: ((in @ E @ D) => (in @ E @ C)))) & ! [C:$i]: ((! [D:$i]: ((in @ D @ C) => (in @ D @ A)) & ? [D:$i]: (in @ D @ C)) => (? [D:$i]: ((in @ D @ B) & ? [E:$i]: ((in @ E @ C) & ~ (? [F:$i]: ((in @ F @ D) & (in @ F @ C))) & ! [F:$i]: ((in @ F @ B) => (! [G:$i]: ((in @ G @ F) => (in @ G @ D)) | (in @ E @ F)))))))))) ).
% 89.50/19.97 thf(sk8_def, definition, sk8 = (^ [A:$i,B:$i,C:$i]: (@+ [D:$i]: ~ ((in @ D @ (sk7 @ C)) => ((in @ B @ D) = (in @ A @ D))))) ).
% 89.50/19.97 thf(sk10_def, definition, sk10 = (^ [A:$i,B:$i]: (@+ [C:$i]: ~ ((in @ C @ A) => (in @ C @ B)))) ).
% 89.50/19.97 thf(sk11_def, definition, sk11 = (^ [A:$i,B:$i]: (@+ [C:$i]: ((in @ C @ (sk7 @ B)) & ? [D:$i]: ((in @ D @ A) & ~ (? [E:$i]: ((in @ E @ C) & (in @ E @ A))) & ! [E:$i]: ((in @ E @ (sk7 @ B)) => (! [F:$i]: ((in @ F @ E) => (in @ F @ C)) | (in @ D @ E))))))) ).
% 89.50/19.97 thf(sk12_def, definition, sk12 = (^ [A:$i,B:$i]: (@+ [C:$i]: ((in @ C @ A) & ~ (? [D:$i]: ((in @ D @ (sk11 @ A @ B)) & (in @ D @ A))) & ! [D:$i]: ((in @ D @ (sk7 @ B)) => (! [E:$i]: ((in @ E @ D) => (in @ E @ (sk11 @ A @ B))) | (in @ C @ D)))))) ).
% 89.50/19.97 thf(sk13_def, definition, sk13 = (^ [A:$i,B:($i > $o)]: (@+ [C:$i]: ~ ((B @ C) => (A = C)))) ).
% 89.50/19.97 thf(sk14_def, definition, sk14 = (^ [A:$i,B:($i > $o)]: (@+ [C:$i]: ~ ((B @ C) => (A = C)))) ).
% 89.50/19.97 thf(sk15_def, definition, sk15 = ((@+) @ $i) ).
% 89.50/19.97 thf(sk16_def, definition, sk16 = (^ [A:$i,B:$i]: (@+ [C:$i]: ~ ((in @ C @ B) => (in @ C @ A)))) ).
% 89.50/19.97 thf(sk17_def, definition, sk17 = (^ [A:$i,B:$i]: (@+ [C:$i]: ~ ((in @ C @ A) => (in @ C @ B)))) ).
% 89.50/19.97 thf(sk18_def, definition, sk18 = (^ [A:$i]: (@+ [B:$i]: (in @ B @ A))) ).
% 89.50/19.97 thf(sk19_def, definition, sk19 = (^ [A:$i]: (@+ [B:$i]: (in @ B @ A))) ).
% 89.50/19.97 thf(sk20_def, definition, sk20 = (^ [A:$i]: (@+ [B:$i]: (in @ B @ A))) ).
% 89.50/19.97 thf(sk21_def, definition, sk21 = (^ [A:$i,B:$i]: (@+ [C:$i]: ~ ((in @ C @ A) => (in @ C @ B)))) ).
% 89.50/19.97 thf(sk22_def, definition, sk22 = (^ [A:$o,B:$i,C:$i]: (@+ [D:$i]: ~ ((in @ B @ D) => ((in @ D @ C) => (A))))) ).
% 89.50/19.97 thf(sk23_def, definition, sk23 = (^ [A:$i,B:($i > $o)]: (@+ [C:$i]: ~ ((B @ C) => (A = C)))) ).
% 89.50/19.97 thf(sk24_def, definition, sk24 = (^ [A:($i > $o)]: (@+ [B:$i]: ! [C:$i]: ((A @ C) = (C = B)))) ).
% 89.50/19.97 thf(sk25_def, definition, sk25 = (^ [A:$i]: (@+ [B:$i]: (in @ B @ A))) ).
% 89.50/19.97 thf(sk26_def, definition, sk26 = (^ [A:($i > $o),B:$i]: (@+ [C:$i]: ((in @ C @ B) & ~ (A @ C)))) ).
% 89.50/19.97 thf(sk27_def, definition, sk27 = (^ [A:($i > $o),B:$i]: (@+ [C:$i]: ~ ((in @ C @ B) => (~ (A @ C))))) ).
% 89.50/19.97 thf(sk28_def, definition, sk28 = (^ [A:($i > $o),B:$i]: (@+ [C:$i]: ((in @ C @ B) & (A @ C)))) ).
% 89.50/19.97 thf(sk29_def, definition, sk29 = (^ [A:($i > $o),B:$i]: (@+ [C:$i]: ~ ((in @ C @ B) => (A @ C)))) ).
% 89.50/19.97 thf(sk30_def, definition, sk30 = (^ [A:($i > $o),B:$i]: (@+ [C:$i]: ((in @ C @ B) & (A @ C)))) ).
% 89.50/19.97 thf(sk31_def, definition, sk31 = (^ [A:($i > $o),B:$i]: (@+ [C:$i]: ((in @ C @ B) & ~ (A @ C)))) ).
% 89.50/19.97 thf(sk32_def, definition, sk32 = (^ [A:($i > $o)]: (@+ [B:$i]: ~ ((A @ B) => (! [C:$i]: ((A @ C) => (B = C)))))) ).
% 89.50/19.97 thf(sk33_def, definition, sk33 = (^ [A:($i > $o)]: (@+ [B:$i]: ~ ((A @ B) => ((sk32 @ A) = B)))) ).
% 89.50/19.97 thf(sk34_def, definition, sk34 = (^ [A:($i > $o)]: (@+ [B:$i]: ((A @ B) & ! [C:$i]: ((A @ C) => (B = C))))) ).
% 89.50/19.97 thf(sk35_def, definition, sk35 = (^ [A:$i,B:($i > $o)]: (@+ [C:$i]: ~ ((B @ C) = (C = A)))) ).
% 89.50/19.97 thf(sk36_def, definition, sk36 = (^ [A:($i > $o)]: (@+ [B:$i]: ((A @ B) & ! [C:$i]: ((A @ C) => (B = C))))) ).
% 89.50/19.97 thf(sk37_def, definition, sk37 = (^ [A:$i,B:($i > $o)]: (@+ [C:$i]: ~ ((B @ C) => (A = C)))) ).
% 89.50/19.97 thf(sk38_def, definition, sk38 = (^ [A:($i > $o),B:($i > $o)]: (@+ [C:$i]: ~ (! [D:$i]: ((C = D) => ((B @ C) = (A @ D)))))) ).
% 89.50/19.97 thf(sk39_def, definition, sk39 = (^ [A:($i > $o),B:($i > $o)]: (@+ [C:$i]: ~ (((sk38 @ A @ B) = C) => ((B @ (sk38 @ A @ B)) = (A @ C))))) ).
% 89.50/19.97 thf(sk40_def, definition, sk40 = (^ [A:$i,B:($i > $o)]: (@+ [C:$i]: ~ ((B @ C) => (A = C)))) ).
% 89.50/19.97 thf(sk42_def, definition, sk42 = (^ [A:($i > $o),B:($i > $o)]: (@+ [C:$i]: ~ (! [D:$i]: ((C = D) => ((B @ C) = (A @ D)))))) ).
% 89.50/19.97 thf(sk43_def, definition, sk43 = (^ [A:($i > $o),B:($i > $o)]: (@+ [C:$i]: ~ (((sk42 @ A @ B) = C) => ((B @ (sk42 @ A @ B)) = (A @ C))))) ).
% 89.50/19.97 thf(sk44_def, definition, sk44 = (^ [A:$i,B:($i > $o),C:($i > $o)]: (@+ [D:$i]: ~ ((C @ D) => (A = D)))) ).
% 89.50/19.97 thf(sk45_def, definition, sk45 = (^ [A:$i,B:($i > $o),C:($i > $o)]: (@+ [D:$i]: ~ ((B @ D) => (A = D)))) ).
% 89.50/19.97 thf(sk46_def, definition, sk46 = (^ [A:($i > $o),B:($i > $o),C:$i,D:$i]: (@+ [E:$i]: ~ ((in @ E @ D) => (! [F:$i]: ((in @ F @ C) => ((E = F) => ((B @ E) = (A @ F)))))))) ).
% 89.50/19.97 thf(sk47_def, definition, sk47 = (^ [A:($i > $o),B:($i > $o),C:$i,D:$i]: (@+ [E:$i]: ~ ((in @ E @ C) => (((sk46 @ A @ B @ C @ D) = E) => ((B @ (sk46 @ A @ B @ C @ D)) = (A @ E)))))) ).
% 89.50/19.97 thf(sk48_def, definition, sk48 = (^ [A:$i,B:$i]: (@+ [C:$i]: ~ ((in @ C @ B) => (in @ C @ A)))) ).
% 89.50/19.97 thf(sk49_def, definition, sk49 = (^ [A:$i,B:$i]: (@+ [C:$i]: ~ ((in @ C @ B) => (in @ C @ A)))) ).
% 89.50/19.97 thf(sk50_def, definition, sk50 = (@+ [A:$i]: ~ (! [B:$i,C:$i]: ((in @ C @ (setunion @ (setadjoin @ A @ (setadjoin @ B @ emptyset)))) => (! [D:$o]: (((in @ C @ A) => (D)) => (((in @ C @ B) => (D)) => (D))))))) ).
% 89.50/19.97 thf(sk51_def, definition, sk51 = (@+ [A:$i]: ~ (! [B:$i]: ((in @ B @ (setunion @ (setadjoin @ sk50 @ (setadjoin @ A @ emptyset)))) => (! [C:$o]: (((in @ B @ sk50) => (C)) => (((in @ B @ A) => (C)) => (C))))))) ).
% 89.50/19.97 thf(sk52_def, definition, sk52 = (@+ [A:$i]: ~ ((in @ A @ (setunion @ (setadjoin @ sk50 @ (setadjoin @ sk51 @ emptyset)))) => (! [B:$o]: (((in @ A @ sk50) => (B)) => (((in @ A @ sk51) => (B)) => (B)))))) ).
% 89.50/19.97 thf(sk53_def, definition, sk53 = (@+ [A:$o]: ~ (((in @ sk52 @ sk50) => (A)) => (((in @ sk52 @ sk51) => (A)) => (A)))) ).
% 89.50/19.97 thf(sk174_def, definition, sk174 = (@+ [A:$i]: ((in @ (sk25 @ (setunion @ (setadjoin @ sk50 @ (setadjoin @ sk51 @ emptyset)))) @ A) & (in @ A @ (setadjoin @ sk50 @ (setadjoin @ sk51 @ emptyset))))) ).
% 89.50/19.97 thf(sk177_def, definition, sk177 = (@+ [A:$i]: ((in @ (sk25 @ (setunion @ (setadjoin @ sk50 @ (setadjoin @ sk51 @ emptyset)))) @ A) & (in @ A @ (setadjoin @ sk50 @ (setadjoin @ sk51 @ emptyset))))) ).
% 89.50/19.97 thf(sk200_def, definition, sk200 = (@+ [A:$i]: ((in @ sk52 @ A) & (in @ A @ (setadjoin @ sk50 @ (setadjoin @ sk51 @ emptyset))))) ).
% 89.50/19.97 thf(sk203_def, definition, sk203 = (@+ [A:$i]: ((in @ sk52 @ A) & (in @ A @ (setadjoin @ sk50 @ (setadjoin @ sk51 @ emptyset))))) ).
% 89.50/19.97 thf(1,conjecture,(((setextAx) => ((emptysetAx) => ((setadjoinAx) => ((powersetAx) => ((setunionAx) => ((omega0Ax) => ((omegaSAx) => ((omegaIndAx) => ((replAx) => ((foundationAx) => ((wellorderingAx) => ((descrp) => ((dsetconstrI) => ((dsetconstrEL) => ((dsetconstrER) => ((exuE1) => ((prop2setE) => ((emptysetE) => ((emptysetimpfalse) => ((notinemptyset) => ((exuE3e) => ((setext) => ((emptyI) => ((noeltsimpempty) => ((setbeta) => ((nonemptyE1) => ((nonemptyI) => ((nonemptyI1) => ((setadjoinIL) => ((emptyinunitempty) => ((setadjoinIR) => ((setadjoinE) => ((setadjoinOr) => ((setoftrueEq) => ((powersetI) => ((emptyinPowerset) => ((emptyInPowerset) => ((powersetE) => ((setunionI) => ((setunionE) => ((subPowSU) => ((exuE2) => ((nonemptyImpWitness) => ((uniqinunit) => ((notinsingleton) => ((eqinunit) => ((singletonsswitch) => ((upairsetE) => ((upairsetIL) => ((upairsetIR) => ((emptyE1) => ((vacuousDall) => ((quantDeMorgan1) => ((quantDeMorgan2) => ((quantDeMorgan3) => ((quantDeMorgan4) => ((prop2setI) => ((prop2set2propI) => ((notdexE) => ((notdallE) => ((exuI1) => ((exuI3) => ((exuI2) => ((inCongP) => ((in__Cong) => ((exuE3u) => ((exu__Cong) => ((emptyset__Cong) => ((setadjoin__Cong) => ((powerset__Cong) => ((setunion__Cong) => ((omega__Cong) => ((exuEu) => ((descr__Cong) => ((dsetconstr__Cong) => ((subsetI1) => ((eqimpsubset2) => ((eqimpsubset1) => ((subsetI2) => ((emptysetsubset) => ((subsetE) => ((subsetE2) => ((notsubsetI) => ((notequalI1) => ((notequalI2) => ((subsetRefl) => ((subsetTrans) => ((setadjoinSub) => ((setadjoinSub2) => ((subset2powerset) => ((setextsub) => ((subsetemptysetimpeq) => ((powersetI1) => ((powersetE1) => ((inPowerset) => ((powersetsubset) => ((sepInPowerset) => ((sepSubset) => ((binunionIL) => ((upairset2IR) => ((binunionIR) => (! [A:$i,B:$i,C:$i,D:$o]: ((in @ C @ (binunion @ A @ B)) => (((in @ C @ A) => (D)) => (((in @ C @ B) => (D)) => (D))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',binunionEcases)).
% 89.50/19.97 thf(2,negated_conjecture,((~ ((setextAx) => ((emptysetAx) => ((setadjoinAx) => ((powersetAx) => ((setunionAx) => ((omega0Ax) => ((omegaSAx) => ((omegaIndAx) => ((replAx) => ((foundationAx) => ((wellorderingAx) => ((descrp) => ((dsetconstrI) => ((dsetconstrEL) => ((dsetconstrER) => ((exuE1) => ((prop2setE) => ((emptysetE) => ((emptysetimpfalse) => ((notinemptyset) => ((exuE3e) => ((setext) => ((emptyI) => ((noeltsimpempty) => ((setbeta) => ((nonemptyE1) => ((nonemptyI) => ((nonemptyI1) => ((setadjoinIL) => ((emptyinunitempty) => ((setadjoinIR) => ((setadjoinE) => ((setadjoinOr) => ((setoftrueEq) => ((powersetI) => ((emptyinPowerset) => ((emptyInPowerset) => ((powersetE) => ((setunionI) => ((setunionE) => ((subPowSU) => ((exuE2) => ((nonemptyImpWitness) => ((uniqinunit) => ((notinsingleton) => ((eqinunit) => ((singletonsswitch) => ((upairsetE) => ((upairsetIL) => ((upairsetIR) => ((emptyE1) => ((vacuousDall) => ((quantDeMorgan1) => ((quantDeMorgan2) => ((quantDeMorgan3) => ((quantDeMorgan4) => ((prop2setI) => ((prop2set2propI) => ((notdexE) => ((notdallE) => ((exuI1) => ((exuI3) => ((exuI2) => ((inCongP) => ((in__Cong) => ((exuE3u) => ((exu__Cong) => ((emptyset__Cong) => ((setadjoin__Cong) => ((powerset__Cong) => ((setunion__Cong) => ((omega__Cong) => ((exuEu) => ((descr__Cong) => ((dsetconstr__Cong) => ((subsetI1) => ((eqimpsubset2) => ((eqimpsubset1) => ((subsetI2) => ((emptysetsubset) => ((subsetE) => ((subsetE2) => ((notsubsetI) => ((notequalI1) => ((notequalI2) => ((subsetRefl) => ((subsetTrans) => ((setadjoinSub) => ((setadjoinSub2) => ((subset2powerset) => ((setextsub) => ((subsetemptysetimpeq) => ((powersetI1) => ((powersetE1) => ((inPowerset) => ((powersetsubset) => ((sepInPowerset) => ((sepSubset) => ((binunionIL) => ((upairset2IR) => ((binunionIR) => (! [A:$i,B:$i,C:$i,D:$o]: ((in @ C @ (binunion @ A @ B)) => (((in @ C @ A) => (D)) => (((in @ C @ B) => (D)) => (D)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))),inference(neg_conjecture,[status(cth)],[1])).
% 89.50/19.97 thf(3,plain,((~ ((! [A:$i,B:$i]: ((! [C:$i]: ((in @ C @ A) = (in @ C @ B))) => (A = B))) => ((! [A:$i]: ~ (in @ A @ emptyset)) => ((! [A:$i,B:$i,C:$i]: ((in @ C @ (setadjoin @ A @ B)) = ((C = A) | (in @ C @ B)))) => ((! [A:$i,B:$i]: ((in @ B @ (powerset @ A)) = (! [C:$i]: ((in @ C @ B) => (in @ C @ A))))) => ((! [A:$i,B:$i]: ((in @ B @ (setunion @ A)) = (? [C:$i]: ((in @ B @ C) & (in @ C @ A))))) => ((in @ emptyset @ omega) => ((! [A:$i]: ((in @ A @ omega) => (in @ (setadjoin @ A @ A) @ omega))) => ((! [A:$i]: (((in @ emptyset @ A) & ! [B:$i]: (((in @ B @ omega) & (in @ B @ A)) => (in @ (setadjoin @ B @ B) @ A))) => (! [B:$i]: ((in @ B @ omega) => (in @ B @ A))))) => ((! [A:($i > ($i > $o)),B:$i]: ((! [C:$i]: ((in @ C @ B) => (? [D:$i]: ((A @ C @ D) & ! [E:$i]: ((A @ C @ E) => (D = E)))))) => (? [C:$i]: ! [D:$i]: ((in @ D @ C) = (? [E:$i]: ((in @ E @ B) & (A @ E @ D))))))) => ((! [A:$i]: ((? [B:$i]: (in @ B @ A)) => (? [B:$i]: ((in @ B @ A) & ~ (? [C:$i]: ((in @ C @ B) & (in @ C @ A))))))) => ((! [A:$i]: ? [B:$i]: (! [C:$i]: ((in @ C @ B) => (! [D:$i]: ((in @ D @ C) => (in @ D @ A)))) & ! [C:$i,D:$i]: (((in @ C @ A) & (in @ D @ A)) => ((! [E:$i]: ((in @ E @ B) => ((in @ C @ E) = (in @ D @ E)))) => (C = D))) & ! [C:$i,D:$i]: (((in @ C @ B) & (in @ D @ B)) => (! [E:$i]: ((in @ E @ C) => (in @ E @ D)) | ! [E:$i]: ((in @ E @ D) => (in @ E @ C)))) & ! [C:$i]: ((! [D:$i]: ((in @ D @ C) => (in @ D @ A)) & ? [D:$i]: (in @ D @ C)) => (? [D:$i,E:$i]: ((in @ D @ B) & (in @ E @ C) & ~ (? [F:$i]: ((in @ F @ D) & (in @ F @ C))) & ! [F:$i]: ((in @ F @ B) => (! [G:$i]: ((in @ G @ F) => (in @ G @ D)) | (in @ E @ F)))))))) => ((! [A:($i > $o)]: ((? [B:$i]: ((A @ B) & ! [C:$i]: ((A @ C) => (B = C)))) => (A @ (descr @ (A))))) => ((! [A:$i,B:($i > $o),C:$i]: ((in @ C @ A) => ((B @ C) => (in @ C @ (dsetconstr @ A @ (B)))))) => ((! [A:$i,B:($i > $o),C:$i]: ((in @ C @ (dsetconstr @ A @ (B))) => (in @ C @ A))) => ((! [A:$i,B:($i > $o),C:$i]: ((in @ C @ (dsetconstr @ A @ (B))) => (B @ C))) => ((! [A:$o,B:$i]: ((in @ B @ (prop2set @ A)) => (A))) => ((! [A:$i]: ((in @ A @ emptyset) => (! [B:$o]: (B)))) => ((! [A:$i]: ~ (in @ A @ emptyset)) => ((! [A:$i]: ~ (in @ A @ emptyset)) => ((! [A:($i > $o)]: ((? [B:$i]: ((A @ B) & ! [C:$i]: ((A @ C) => (B = C)))) => (? [B:$i]: (A @ B)))) => ((! [A:$i,B:$i]: ((! [C:$i]: ((in @ C @ A) => (in @ C @ B))) => ((! [C:$i]: ((in @ C @ B) => (in @ C @ A))) => (A = B)))) => ((! [A:$i]: ((! [B:$i]: ~ (in @ B @ A)) => (A = emptyset))) => ((! [A:$i]: ((! [B:$i]: ~ (in @ B @ A)) => (A = emptyset))) => ((! [A:$i,B:($i > $o),C:$i]: ((in @ C @ A) => ((in @ C @ (dsetconstr @ A @ (B))) = (B @ C)))) => ((! [A:$i]: ((~ (A = emptyset)) => (? [B:$i]: (in @ B @ A)))) => ((! [A:$i,B:($i > $o),C:$i]: ((in @ C @ A) => ((B @ C) => (~ ((dsetconstr @ A @ (B)) = emptyset))))) => ((! [A:$i]: ((? [B:$i]: (in @ B @ A)) => (~ (A = emptyset)))) => ((! [A:$i,B:$i]: (in @ A @ (setadjoin @ A @ B))) => ((in @ emptyset @ (setadjoin @ emptyset @ emptyset)) => ((! [A:$i,B:$i,C:$i]: ((in @ C @ B) => (in @ C @ (setadjoin @ A @ B)))) => ((! [A:$i,B:$i,C:$i]: ((in @ C @ (setadjoin @ A @ B)) => (! [D:$o]: (((C = A) => (D)) => (((in @ C @ B) => (D)) => (D)))))) => ((! [A:$i,B:$i,C:$i]: ((in @ C @ (setadjoin @ A @ B)) => ((C = A) | (in @ C @ B)))) => ((! [A:$i]: ((dsetconstr @ A @ (^ [B:$i]: (($true)))) = A)) => ((! [A:$i,B:$i]: ((! [C:$i]: ((in @ C @ B) => (in @ C @ A))) => (in @ B @ (powerset @ A)))) => ((! [A:$i]: (in @ emptyset @ (powerset @ A))) => ((! [A:$i]: (in @ emptyset @ (powerset @ A))) => ((! [A:$i,B:$i,C:$i]: ((in @ B @ (powerset @ A)) => ((in @ C @ B) => (in @ C @ A)))) => ((! [A:$i,B:$i,C:$i]: ((in @ B @ C) => ((in @ C @ A) => (in @ B @ (setunion @ A))))) => ((! [A:$i,B:$i]: ((in @ B @ (setunion @ A)) => (! [C:$o]: ((! [D:$i]: ((in @ B @ D) => ((in @ D @ A) => (C)))) => (C))))) => ((! [A:$i,B:$i]: ((in @ B @ A) => (in @ B @ (powerset @ (setunion @ A))))) => ((! [A:($i > $o)]: ((? [B:$i]: ((A @ B) & ! [C:$i]: ((A @ C) => (B = C)))) => (? [B:$i]: ! [C:$i]: ((A @ C) = (C = B))))) => ((! [A:$i]: ((~ (A = emptyset)) => (? [B:$i]: (in @ B @ A)))) => ((! [A:$i,B:$i]: ((in @ A @ (setadjoin @ B @ emptyset)) => (A = B))) => ((! [A:$i,B:$i]: ((~ (A = B)) => (~ (in @ B @ (setadjoin @ A @ emptyset))))) => ((! [A:$i,B:$i]: ((A = B) => (in @ A @ (setadjoin @ B @ emptyset)))) => ((! [A:$i,B:$i]: ((in @ A @ (setadjoin @ B @ emptyset)) => (in @ B @ (setadjoin @ A @ emptyset)))) => ((! [A:$i,B:$i,C:$i]: ((in @ C @ (setadjoin @ A @ (setadjoin @ B @ emptyset))) => ((C = A) | (C = B)))) => ((! [A:$i,B:$i]: (in @ A @ (setadjoin @ A @ (setadjoin @ B @ emptyset)))) => ((! [A:$i,B:$i]: (in @ B @ (setadjoin @ A @ (setadjoin @ B @ emptyset)))) => ((! [A:$i,B:($i > $o)]: ((? [C:$i]: ((in @ C @ A) & (B @ C))) => (~ ((dsetconstr @ A @ (B)) = emptyset)))) => ((! [A:($i > $o),B:$i]: ((in @ B @ emptyset) => (A @ B))) => ((! [A:$i,B:($i > $o)]: ((~ (! [C:$i]: ((in @ C @ A) => (B @ C)))) => (? [C:$i]: ((in @ C @ A) & ~ (B @ C))))) => ((! [A:$i,B:($i > $o)]: ((! [C:$i]: ((in @ C @ A) => (~ (B @ C)))) => (~ (? [C:$i]: ((in @ C @ A) & (B @ C)))))) => ((! [A:$i,B:($i > $o)]: ((~ (? [C:$i]: ((in @ C @ A) & (B @ C)))) => (! [C:$i]: ((in @ C @ A) => (~ (B @ C)))))) => ((! [A:$i,B:($i > $o)]: ((? [C:$i]: ((in @ C @ A) & ~ (B @ C))) => (~ (! [C:$i]: ((in @ C @ A) => (B @ C)))))) => ((! [A:$o]: ((A) => (in @ emptyset @ (prop2set @ A)))) => ((! [A:$o]: ((A) => (set2prop @ (prop2set @ A)))) => ((! [A:$i,B:($i > $o)]: ((~ (? [C:$i]: ((in @ C @ A) & (B @ C)))) => (! [C:$i]: ((in @ C @ A) => (~ (B @ C)))))) => ((! [A:$i,B:($i > $o)]: ((~ (! [C:$i]: ((in @ C @ A) => (B @ C)))) => (? [C:$i]: ((in @ C @ A) & ~ (B @ C))))) => ((! [A:($i > $o)]: ((? [B:$i]: (A @ B)) => ((! [B:$i,C:$i]: ((A @ B) => ((A @ C) => (B = C)))) => (? [B:$i]: ((A @ B) & ! [C:$i]: ((A @ C) => (B = C))))))) => ((! [A:($i > $o)]: ((? [B:$i]: ! [C:$i]: ((A @ C) = (C = B))) => (? [B:$i]: ((A @ B) & ! [C:$i]: ((A @ C) => (B = C)))))) => ((! [A:$i,B:$i]: ((A = B) => (! [C:$i,D:$i]: ((C = D) => ((in @ C @ A) => (in @ D @ B)))))) => ((! [A:$i,B:$i]: ((A = B) => (! [C:$i,D:$i]: ((C = D) => ((in @ C @ A) = (in @ D @ B)))))) => ((! [A:($i > $o)]: ((? [B:$i]: ((A @ B) & ! [C:$i]: ((A @ C) => (B = C)))) => (! [B:$i,C:$i]: ((A @ B) => ((A @ C) => (B = C)))))) => ((! [A:($i > $o),B:($i > $o)]: ((! [C:$i,D:$i]: ((C = D) => ((A @ C) = (B @ D)))) => ((? [C:$i]: ((A @ C) & ! [D:$i]: ((A @ D) => (C = D)))) = (? [C:$i]: ((B @ C) & ! [D:$i]: ((B @ D) => (C = D))))))) => ((! [A:$i,B:$i]: ((A = B) => (! [C:$i,D:$i]: ((C = D) => ((setadjoin @ A @ C) = (setadjoin @ B @ D)))))) => ((! [A:$i,B:$i]: ((A = B) => ((powerset @ A) = (powerset @ B)))) => ((! [A:$i,B:$i]: ((A = B) => ((setunion @ A) = (setunion @ B)))) => ((! [A:($i > $o)]: ((? [B:$i]: ((A @ B) & ! [C:$i]: ((A @ C) => (B = C)))) => (! [B:$i,C:$i]: ((A @ B) => ((A @ C) => (B = C)))))) => ((! [A:($i > $o),B:($i > $o)]: ((! [C:$i,D:$i]: ((C = D) => ((A @ C) = (B @ D)))) => ((? [C:$i]: ((A @ C) & ! [D:$i]: ((A @ D) => (C = D)))) => ((? [C:$i]: ((B @ C) & ! [D:$i]: ((B @ D) => (C = D)))) => ((descr @ (A)) = (descr @ (B))))))) => ((! [A:$i,B:$i]: ((A = B) => (! [C:($i > $o),D:($i > $o)]: ((! [E:$i]: ((in @ E @ A) => (! [F:$i]: ((in @ F @ B) => ((E = F) => ((C @ E) = (D @ F))))))) => ((dsetconstr @ A @ (C)) = (dsetconstr @ B @ (D))))))) => ((! [A:$i,B:$i]: ((! [C:$i]: ((in @ C @ A) => (in @ C @ B))) => (subset @ A @ B))) => ((! [A:$i,B:$i]: ((A = B) => (subset @ B @ A))) => ((! [A:$i,B:$i]: ((A = B) => (subset @ A @ B))) => ((! [A:$i,B:$i]: ((! [C:$i]: ((in @ C @ A) => (in @ C @ B))) => (subset @ A @ B))) => ((! [A:$i]: (subset @ emptyset @ A)) => ((! [A:$i,B:$i,C:$i]: ((subset @ A @ B) => ((in @ C @ A) => (in @ C @ B)))) => ((! [A:$i,B:$i,C:$i]: ((subset @ A @ B) => ((~ (in @ C @ B)) => (~ (in @ C @ A))))) => ((! [A:$i,B:$i,C:$i]: ((in @ C @ A) => ((~ (in @ C @ B)) => (~ (subset @ A @ B))))) => ((! [A:$i,B:$i]: ((~ (subset @ A @ B)) => (~ (A = B)))) => ((! [A:$i,B:$i,C:$i]: ((in @ C @ A) => ((~ (in @ C @ B)) => (~ (A = B))))) => ((! [A:$i]: (subset @ A @ A)) => ((! [A:$i,B:$i,C:$i]: ((subset @ A @ B) => ((subset @ B @ C) => (subset @ A @ C)))) => ((! [A:$i,B:$i]: (subset @ B @ (setadjoin @ A @ B))) => ((! [A:$i,B:$i,C:$i]: ((subset @ A @ C) => (subset @ A @ (setadjoin @ B @ C)))) => ((! [A:$i,B:$i]: ((subset @ A @ B) => (in @ A @ (powerset @ B)))) => ((! [A:$i,B:$i]: ((subset @ A @ B) => ((subset @ B @ A) => (A = B)))) => ((! [A:$i]: ((subset @ A @ emptyset) => (A = emptyset))) => ((! [A:$i,B:$i]: ((subset @ B @ A) => (in @ B @ (powerset @ A)))) => ((! [A:$i,B:$i]: ((in @ B @ (powerset @ A)) => (subset @ B @ A))) => ((! [A:$i]: (in @ A @ (powerset @ A))) => ((! [A:$i,B:$i]: ((subset @ A @ B) => (subset @ (powerset @ A) @ (powerset @ B)))) => ((! [A:$i,B:($i > $o)]: (in @ (dsetconstr @ A @ (B)) @ (powerset @ A))) => ((! [A:$i,B:($i > $o)]: (subset @ (dsetconstr @ A @ (B)) @ A)) => ((! [A:$i,B:$i,C:$i]: ((in @ C @ A) => (in @ C @ (setunion @ (setadjoin @ A @ (setadjoin @ B @ emptyset)))))) => ((! [A:$i,B:$i]: (in @ B @ (setadjoin @ A @ (setadjoin @ B @ emptyset)))) => ((! [A:$i,B:$i,C:$i]: ((in @ C @ B) => (in @ C @ (setunion @ (setadjoin @ A @ (setadjoin @ B @ emptyset)))))) => (! [A:$i,B:$i,C:$i,D:$o]: ((in @ C @ (setunion @ (setadjoin @ A @ (setadjoin @ B @ emptyset)))) => (((in @ C @ A) => (D)) => (((in @ C @ B) => (D)) => (D)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[2])).
% 89.50/19.97 thf(4,plain,((~ ((! [A:$i,B:$i]: ((! [C:$i]: ((in @ C @ A) = (in @ C @ B))) => (A = B))) => ((~ (? [A:$i]: (in @ A @ emptyset))) => ((! [A:$i,B:$i,C:$i]: ((in @ C @ (setadjoin @ A @ B)) = ((C = A) | (in @ C @ B)))) => ((! [A:$i,B:$i]: ((in @ B @ (powerset @ A)) = (! [C:$i]: ((in @ C @ B) => (in @ C @ A))))) => ((! [A:$i,B:$i]: ((in @ B @ (setunion @ A)) = (? [C:$i]: ((in @ B @ C) & (in @ C @ A))))) => ((in @ emptyset @ omega) => ((! [A:$i]: ((in @ A @ omega) => (in @ (setadjoin @ A @ A) @ omega))) => ((! [A:$i]: (((in @ emptyset @ A) & ! [B:$i]: (((in @ B @ omega) & (in @ B @ A)) => (in @ (setadjoin @ B @ B) @ A))) => (! [B:$i]: ((in @ B @ omega) => (in @ B @ A))))) => ((! [A:($i > ($i > $o)),B:$i]: ((! [C:$i]: ((in @ C @ B) => (? [D:$i]: ((A @ C @ D) & ! [E:$i]: ((A @ C @ E) => (D = E)))))) => (? [C:$i]: ! [D:$i]: ((in @ D @ C) = (? [E:$i]: ((in @ E @ B) & (A @ E @ D))))))) => ((! [A:$i]: ((? [B:$i]: (in @ B @ A)) => (? [B:$i]: ((in @ B @ A) & ~ (? [C:$i]: ((in @ C @ B) & (in @ C @ A))))))) => ((! [A:$i]: ? [B:$i]: (! [C:$i]: ((in @ C @ B) => (! [D:$i]: ((in @ D @ C) => (in @ D @ A)))) & ! [C:$i,D:$i]: (((in @ C @ A) & (in @ D @ A)) => ((! [E:$i]: ((in @ E @ B) => ((in @ C @ E) = (in @ D @ E)))) => (C = D))) & ! [C:$i,D:$i]: (((in @ C @ B) & (in @ D @ B)) => (! [E:$i]: ((in @ E @ C) => (in @ E @ D)) | ! [E:$i]: ((in @ E @ D) => (in @ E @ C)))) & ! [C:$i]: ((! [D:$i]: ((in @ D @ C) => (in @ D @ A)) & ? [D:$i]: (in @ D @ C)) => (? [D:$i]: ((in @ D @ B) & ? [E:$i]: ((in @ E @ C) & ~ (? [F:$i]: ((in @ F @ D) & (in @ F @ C))) & ! [F:$i]: ((in @ F @ B) => (! [G:$i]: ((in @ G @ F) => (in @ G @ D)) | (in @ E @ F))))))))) => ((! [A:($i > $o)]: ((? [B:$i]: ((A @ B) & ! [C:$i]: ((A @ C) => (B = C)))) => (A @ (descr @ (A))))) => ((! [A:$i,B:($i > $o),C:$i]: ((in @ C @ A) => ((B @ C) => (in @ C @ (dsetconstr @ A @ (B)))))) => ((! [A:$i,B:($i > $o),C:$i]: ((in @ C @ (dsetconstr @ A @ (B))) => (in @ C @ A))) => ((! [A:$i,B:($i > $o),C:$i]: ((in @ C @ (dsetconstr @ A @ (B))) => (B @ C))) => ((! [A:$o]: ((? [B:$i]: (in @ B @ (prop2set @ A))) => (A))) => (((? [A:$i]: (in @ A @ emptyset)) => (! [A:$o]: (A))) => ((~ (? [A:$i]: (in @ A @ emptyset))) => ((~ (? [A:$i]: (in @ A @ emptyset))) => ((! [A:($i > $o)]: ((? [B:$i]: ((A @ B) & ! [C:$i]: ((A @ C) => (B = C)))) => (? [B:$i]: (A @ B)))) => ((! [A:$i,B:$i]: ((! [C:$i]: ((in @ C @ A) => (in @ C @ B))) => ((! [C:$i]: ((in @ C @ B) => (in @ C @ A))) => (A = B)))) => ((! [A:$i]: ((~ (? [B:$i]: (in @ B @ A))) => (A = emptyset))) => ((! [A:$i]: ((~ (? [B:$i]: (in @ B @ A))) => (A = emptyset))) => ((! [A:$i,B:($i > $o),C:$i]: ((in @ C @ A) => ((in @ C @ (dsetconstr @ A @ (B))) = (B @ C)))) => ((! [A:$i]: ((~ (A = emptyset)) => (? [B:$i]: (in @ B @ A)))) => ((! [A:$i,B:($i > $o),C:$i]: ((in @ C @ A) => ((B @ C) => (~ ((dsetconstr @ A @ (B)) = emptyset))))) => ((! [A:$i]: ((? [B:$i]: (in @ B @ A)) => (~ (A = emptyset)))) => ((! [A:$i,B:$i]: (in @ A @ (setadjoin @ A @ B))) => ((in @ emptyset @ (setadjoin @ emptyset @ emptyset)) => ((! [A:$i,B:$i,C:$i]: ((in @ C @ B) => (in @ C @ (setadjoin @ A @ B)))) => ((! [A:$i,B:$i,C:$i]: ((in @ C @ (setadjoin @ A @ B)) => (! [D:$o]: (((C = A) => (D)) => (((in @ C @ B) => (D)) => (D)))))) => ((! [A:$i,B:$i,C:$i]: ((in @ C @ (setadjoin @ A @ B)) => ((C = A) | (in @ C @ B)))) => ((! [A:$i]: ((dsetconstr @ A @ (^ [B:$i]: (($true)))) = A)) => ((! [A:$i,B:$i]: ((! [C:$i]: ((in @ C @ B) => (in @ C @ A))) => (in @ B @ (powerset @ A)))) => ((! [A:$i]: (in @ emptyset @ (powerset @ A))) => ((! [A:$i]: (in @ emptyset @ (powerset @ A))) => ((! [A:$i,B:$i]: ((in @ B @ (powerset @ A)) => (! [C:$i]: ((in @ C @ B) => (in @ C @ A))))) => ((! [A:$i,B:$i,C:$i]: ((in @ B @ C) => ((in @ C @ A) => (in @ B @ (setunion @ A))))) => ((! [A:$i,B:$i]: ((in @ B @ (setunion @ A)) => (! [C:$o]: ((! [D:$i]: ((in @ B @ D) => ((in @ D @ A) => (C)))) => (C))))) => ((! [A:$i,B:$i]: ((in @ B @ A) => (in @ B @ (powerset @ (setunion @ A))))) => ((! [A:($i > $o)]: ((? [B:$i]: ((A @ B) & ! [C:$i]: ((A @ C) => (B = C)))) => (? [B:$i]: ! [C:$i]: ((A @ C) = (C = B))))) => ((! [A:$i]: ((~ (A = emptyset)) => (? [B:$i]: (in @ B @ A)))) => ((! [A:$i,B:$i]: ((in @ A @ (setadjoin @ B @ emptyset)) => (A = B))) => ((! [A:$i,B:$i]: ((~ (A = B)) => (~ (in @ B @ (setadjoin @ A @ emptyset))))) => ((! [A:$i,B:$i]: ((A = B) => (in @ A @ (setadjoin @ B @ emptyset)))) => ((! [A:$i,B:$i]: ((in @ A @ (setadjoin @ B @ emptyset)) => (in @ B @ (setadjoin @ A @ emptyset)))) => ((! [A:$i,B:$i,C:$i]: ((in @ C @ (setadjoin @ A @ (setadjoin @ B @ emptyset))) => ((C = A) | (C = B)))) => ((! [A:$i,B:$i]: (in @ A @ (setadjoin @ A @ (setadjoin @ B @ emptyset)))) => ((! [A:$i,B:$i]: (in @ B @ (setadjoin @ A @ (setadjoin @ B @ emptyset)))) => ((! [A:$i,B:($i > $o)]: ((? [C:$i]: ((in @ C @ A) & (B @ C))) => (~ ((dsetconstr @ A @ (B)) = emptyset)))) => ((! [A:($i > $o),B:$i]: ((in @ B @ emptyset) => (A @ B))) => ((! [A:$i,B:($i > $o)]: ((~ (! [C:$i]: ((in @ C @ A) => (B @ C)))) => (? [C:$i]: ((in @ C @ A) & ~ (B @ C))))) => ((! [A:$i,B:($i > $o)]: ((! [C:$i]: ((in @ C @ A) => (~ (B @ C)))) => (~ (? [C:$i]: ((in @ C @ A) & (B @ C)))))) => ((! [A:$i,B:($i > $o)]: ((~ (? [C:$i]: ((in @ C @ A) & (B @ C)))) => (! [C:$i]: ((in @ C @ A) => (~ (B @ C)))))) => ((! [A:$i,B:($i > $o)]: ((? [C:$i]: ((in @ C @ A) & ~ (B @ C))) => (~ (! [C:$i]: ((in @ C @ A) => (B @ C)))))) => ((! [A:$o]: ((A) => (in @ emptyset @ (prop2set @ A)))) => ((! [A:$o]: ((A) => (set2prop @ (prop2set @ A)))) => ((! [A:$i,B:($i > $o)]: ((~ (? [C:$i]: ((in @ C @ A) & (B @ C)))) => (! [C:$i]: ((in @ C @ A) => (~ (B @ C)))))) => ((! [A:$i,B:($i > $o)]: ((~ (! [C:$i]: ((in @ C @ A) => (B @ C)))) => (? [C:$i]: ((in @ C @ A) & ~ (B @ C))))) => ((! [A:($i > $o)]: ((? [B:$i]: (A @ B)) => ((! [B:$i]: ((A @ B) => (! [C:$i]: ((A @ C) => (B = C))))) => (? [B:$i]: ((A @ B) & ! [C:$i]: ((A @ C) => (B = C))))))) => ((! [A:($i > $o)]: ((? [B:$i]: ! [C:$i]: ((A @ C) = (C = B))) => (? [B:$i]: ((A @ B) & ! [C:$i]: ((A @ C) => (B = C)))))) => ((! [A:$i,B:$i]: ((A = B) => (! [C:$i,D:$i]: ((C = D) => ((in @ C @ A) => (in @ D @ B)))))) => ((! [A:$i,B:$i]: ((A = B) => (! [C:$i,D:$i]: ((C = D) => ((in @ C @ A) = (in @ D @ B)))))) => ((! [A:($i > $o)]: ((? [B:$i]: ((A @ B) & ! [C:$i]: ((A @ C) => (B = C)))) => (! [B:$i]: ((A @ B) => (! [C:$i]: ((A @ C) => (B = C))))))) => ((! [A:($i > $o),B:($i > $o)]: ((! [C:$i,D:$i]: ((C = D) => ((A @ C) = (B @ D)))) => ((? [C:$i]: ((A @ C) & ! [D:$i]: ((A @ D) => (C = D)))) = (? [C:$i]: ((B @ C) & ! [D:$i]: ((B @ D) => (C = D))))))) => ((! [A:$i,B:$i]: ((A = B) => (! [C:$i,D:$i]: ((C = D) => ((setadjoin @ A @ C) = (setadjoin @ B @ D)))))) => ((! [A:$i,B:$i]: ((A = B) => ((powerset @ A) = (powerset @ B)))) => ((! [A:$i,B:$i]: ((A = B) => ((setunion @ A) = (setunion @ B)))) => ((! [A:($i > $o)]: ((? [B:$i]: ((A @ B) & ! [C:$i]: ((A @ C) => (B = C)))) => (! [B:$i]: ((A @ B) => (! [C:$i]: ((A @ C) => (B = C))))))) => ((! [A:($i > $o),B:($i > $o)]: ((! [C:$i,D:$i]: ((C = D) => ((A @ C) = (B @ D)))) => ((? [C:$i]: ((A @ C) & ! [D:$i]: ((A @ D) => (C = D)))) => ((? [C:$i]: ((B @ C) & ! [D:$i]: ((B @ D) => (C = D)))) => ((descr @ (A)) = (descr @ (B))))))) => ((! [A:$i,B:$i]: ((A = B) => (! [C:($i > $o),D:($i > $o)]: ((! [E:$i]: ((in @ E @ A) => (! [F:$i]: ((in @ F @ B) => ((E = F) => ((C @ E) = (D @ F))))))) => ((dsetconstr @ A @ (C)) = (dsetconstr @ B @ (D))))))) => ((! [A:$i,B:$i]: ((! [C:$i]: ((in @ C @ A) => (in @ C @ B))) => (subset @ A @ B))) => ((! [A:$i,B:$i]: ((A = B) => (subset @ B @ A))) => ((! [A:$i,B:$i]: ((A = B) => (subset @ A @ B))) => ((! [A:$i,B:$i]: ((! [C:$i]: ((in @ C @ A) => (in @ C @ B))) => (subset @ A @ B))) => ((! [A:$i]: (subset @ emptyset @ A)) => ((! [A:$i,B:$i]: ((subset @ A @ B) => (! [C:$i]: ((in @ C @ A) => (in @ C @ B))))) => ((! [A:$i,B:$i]: ((subset @ A @ B) => (! [C:$i]: ((~ (in @ C @ B)) => (~ (in @ C @ A)))))) => ((! [A:$i,B:$i,C:$i]: ((in @ C @ A) => ((~ (in @ C @ B)) => (~ (subset @ A @ B))))) => ((! [A:$i,B:$i]: ((~ (subset @ A @ B)) => (~ (A = B)))) => ((! [A:$i,B:$i,C:$i]: ((in @ C @ A) => ((~ (in @ C @ B)) => (~ (A = B))))) => ((! [A:$i]: (subset @ A @ A)) => ((! [A:$i,B:$i]: ((subset @ A @ B) => (! [C:$i]: ((subset @ B @ C) => (subset @ A @ C))))) => ((! [A:$i,B:$i]: (subset @ B @ (setadjoin @ A @ B))) => ((! [A:$i,B:$i,C:$i]: ((subset @ A @ C) => (subset @ A @ (setadjoin @ B @ C)))) => ((! [A:$i,B:$i]: ((subset @ A @ B) => (in @ A @ (powerset @ B)))) => ((! [A:$i,B:$i]: ((subset @ A @ B) => ((subset @ B @ A) => (A = B)))) => ((! [A:$i]: ((subset @ A @ emptyset) => (A = emptyset))) => ((! [A:$i,B:$i]: ((subset @ B @ A) => (in @ B @ (powerset @ A)))) => ((! [A:$i,B:$i]: ((in @ B @ (powerset @ A)) => (subset @ B @ A))) => ((! [A:$i]: (in @ A @ (powerset @ A))) => ((! [A:$i,B:$i]: ((subset @ A @ B) => (subset @ (powerset @ A) @ (powerset @ B)))) => ((! [A:$i,B:($i > $o)]: (in @ (dsetconstr @ A @ (B)) @ (powerset @ A))) => ((! [A:$i,B:($i > $o)]: (subset @ (dsetconstr @ A @ (B)) @ A)) => ((! [A:$i,B:$i,C:$i]: ((in @ C @ A) => (in @ C @ (setunion @ (setadjoin @ A @ (setadjoin @ B @ emptyset)))))) => ((! [A:$i,B:$i]: (in @ B @ (setadjoin @ A @ (setadjoin @ B @ emptyset)))) => ((! [A:$i,B:$i,C:$i]: ((in @ C @ B) => (in @ C @ (setunion @ (setadjoin @ A @ (setadjoin @ B @ emptyset)))))) => (! [A:$i,B:$i,C:$i]: ((in @ C @ (setunion @ (setadjoin @ A @ (setadjoin @ B @ emptyset)))) => (! [D:$o]: (((in @ C @ A) => (D)) => (((in @ C @ B) => (D)) => (D))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))),inference(miniscope,[status(thm)],[3])).
% 89.50/19.97 thf(5,plain,(! [ZZZZZZZZZ:$i,ZZZZZZZZY:$i,ZZZZZZZZX:$i,ZZZZZZZZW:$i,ZZZZZZZZV:$i,ZZZZZZZZU:$i,ZZZZZZZZT:$i,ZZZZZZZZS:$i,ZZZZZZZZR:($i > $o),ZZZZZZZZQ:$i,ZZZZZZZZP:($i > $o),ZZZZZZZZO:$i,ZZZZZZZZN:$i,ZZZZZZZZM:$i,ZZZZZZZZL:$i,ZZZZZZZZK:$i,ZZZZZZZZJ:$i,ZZZZZZZZI:$i,ZZZZZZZZH:$i,ZZZZZZZZG:$i,ZZZZZZZZF:$i,ZZZZZZZZE:$i,ZZZZZZZZD:$i,ZZZZZZZZC:$i,ZZZZZZZZB:$i,ZZZZZZZZA:$i,ZZZZZZZZ:$i,ZZZZZZZY:$i,ZZZZZZZX:$i,ZZZZZZZW:$i,ZZZZZZZV:$i,ZZZZZZZU:$i,ZZZZZZZT:$i,ZZZZZZZS:$i,ZZZZZZZR:$i,ZZZZZZZQ:$i,ZZZZZZZP:$i,ZZZZZZZO:$i,ZZZZZZZN:$i,ZZZZZZZM:$i,ZZZZZZZL:$i,ZZZZZZZK:$i,ZZZZZZZJ:$i,ZZZZZZZI:$i,ZZZZZZZH:$i,ZZZZZZZG:$i,ZZZZZZZF:$i,ZZZZZZZE:$i,ZZZZZZZD:$i,ZZZZZZZC:$i,ZZZZZZZB:$i,ZZZZZZZA:$i,ZZZZZZZ:$i,ZZZZZZY:$i,ZZZZZZX:$i,ZZZZZZW:$i,ZZZZZZV:($i > $o),ZZZZZZU:($i > $o),ZZZZZZT:$i,ZZZZZZS:$i,ZZZZZZR:$i,ZZZZZZQ:$i,ZZZZZZP:($i > $o),ZZZZZZO:($i > $o),ZZZZZZN:$i,ZZZZZZM:$i,ZZZZZZL:$i,ZZZZZZK:($i > $o),ZZZZZZJ:$i,ZZZZZZI:$i,ZZZZZZH:$i,ZZZZZZG:$i,ZZZZZZF:$i,ZZZZZZE:$i,ZZZZZZD:$i,ZZZZZZC:$i,ZZZZZZB:($i > $o),ZZZZZZA:($i > $o),ZZZZZZ:$i,ZZZZZY:$i,ZZZZZX:$i,ZZZZZW:($i > $o),ZZZZZV:$i,ZZZZZU:$i,ZZZZZT:$i,ZZZZZS:$i,ZZZZZR:$i,ZZZZZQ:$i,ZZZZZP:$i,ZZZZZO:$i,ZZZZZN:$i,ZZZZZM:$i,ZZZZZL:($i > $o),ZZZZZK:$i,ZZZZZJ:$i,ZZZZZI:($i > $o),ZZZZZH:$i,ZZZZZG:($i > $o),ZZZZZF:$i,ZZZZZE:$i,ZZZZZD:($i > $o),ZZZZZC:$i,ZZZZZB:$o,ZZZZZA:$o,ZZZZZ:$i,ZZZZY:($i > $o),ZZZZX:$i,ZZZZW:$i,ZZZZV:($i > $o),ZZZZU:$i,ZZZZT:$i,ZZZZS:($i > $o),ZZZZR:$i,ZZZZQ:$i,ZZZZP:($i > $o),ZZZZO:$i,ZZZZN:$i,ZZZZM:($i > $o),ZZZZL:$i,ZZZZK:($i > $o),ZZZZJ:$i,ZZZZI:$i,ZZZZH:$i,ZZZZG:$i,ZZZZF:$i,ZZZZE:$i,ZZZZD:$i,ZZZZC:$i,ZZZZB:$i,ZZZZA:$i,ZZZZ:$i,ZZZY:$i,ZZZX:$i,ZZZW:$i,ZZZV:$i,ZZZU:$i,ZZZT:$i,ZZZS:$i,ZZZR:$i,ZZZQ:($i > $o),ZZZP:$i,ZZZO:$i,ZZZN:$o,ZZZM:$i,ZZZL:$i,ZZZK:$i,ZZZJ:$i,ZZZI:$i,ZZZH:$i,ZZZG:$i,ZZZF:$i,ZZZE:$i,ZZZD:$i,ZZZC:$i,ZZZB:$i,ZZZA:$i,ZZZ:$i,ZZY:$i,ZZX:$i,ZZW:$o,ZZV:$i,ZZU:$i,ZZT:$i,ZZS:$i,ZZR:$i,ZZQ:$i,ZZP:$i,ZZO:$i,ZZN:$i,ZZM:$i,ZZL:$i,ZZK:($i > $o),ZZJ:$i,ZZI:$i,ZZH:$i,ZZG:($i > $o),ZZF:$i,ZZE:$i,ZZD:$i,ZZC:$i,ZZB:$i,ZZA:$i,ZZ:($i > $o),ZY:$i,ZX:$i,ZW:$o,ZV:$i,ZU:$i,ZT:$o,ZS:$i,ZR:($i > $o),ZQ:$i,ZP:$i,ZO:($i > $o),ZN:$i,ZM:$i,ZL:($i > $o),ZK:$i,ZJ:$i,ZI:($i > $o),ZH:$i,ZG:$i,ZF:$i,ZE:$i,ZD:$i,ZC:$i,ZB:$i,ZA:$i,Z:$i,Y:$i,X:$i,W:$i,V:$i,U:$i,T:$i,S:$i,R:$i,Q:$i,P:$i,O:$i,N:($i > ($i > $o)),M:$i,L:$i,K:$i,J:$i,I:$i,H:$i,G:$i,F:$i,E:$i,D:$i,C:$i,B:$i,A:$i] : (((~ ((in @ (sk1 @ B @ A) @ A) = (in @ (sk1 @ B @ A) @ B)) | (A = B)) & ~ (in @ C @ emptyset) & ((in @ F @ (setadjoin @ D @ E)) = ((F = D) | (in @ F @ E))) & ((in @ H @ (powerset @ G)) = (! [ZZZZZZZZZA:$i]: ((in @ ZZZZZZZZZA @ H) => (in @ ZZZZZZZZZA @ G)))) & ((in @ J @ (setunion @ I)) = (? [ZZZZZZZZZA:$i]: ((in @ J @ ZZZZZZZZZA) & (in @ ZZZZZZZZZA @ I)))) & (in @ emptyset @ omega) & (~ (in @ K @ omega) | (in @ (setadjoin @ K @ K) @ omega)) & (~ (in @ emptyset @ L) | (in @ (sk2 @ L) @ omega) | ~ (in @ M @ omega) | (in @ M @ L)) & (~ (in @ emptyset @ L) | (in @ (sk2 @ L) @ L) | ~ (in @ M @ omega) | (in @ M @ L)) & (~ (in @ emptyset @ L) | ~ (in @ (setadjoin @ (sk2 @ L) @ (sk2 @ L)) @ L) | ~ (in @ M @ omega) | (in @ M @ L)) & ((in @ (sk3 @ O @ (N)) @ O) | ((in @ Q @ (sk5 @ O @ (N))) = (? [ZZZZZZZZZA:$i]: ((in @ ZZZZZZZZZA @ O) & (N @ ZZZZZZZZZA @ Q))))) & (~ (N @ (sk3 @ O @ (N)) @ P) | (N @ (sk3 @ O @ (N)) @ (sk4 @ P @ O @ (N))) | ((in @ Q @ (sk5 @ O @ (N))) = (? [ZZZZZZZZZA:$i]: ((in @ ZZZZZZZZZA @ O) & (N @ ZZZZZZZZZA @ Q))))) & (~ (N @ (sk3 @ O @ (N)) @ P) | ~ (P = (sk4 @ P @ O @ (N))) | ((in @ Q @ (sk5 @ O @ (N))) = (? [ZZZZZZZZZA:$i]: ((in @ ZZZZZZZZZA @ O) & (N @ ZZZZZZZZZA @ Q))))) & (~ (in @ S @ R) | (in @ (sk6 @ R) @ R)) & (~ (in @ S @ R) | ~ (in @ T @ (sk6 @ R)) | ~ (in @ T @ R)) & (~ (in @ V @ (sk7 @ U)) | ~ (in @ W @ V) | (in @ W @ U)) & (~ (in @ X @ U) | ~ (in @ Y @ U) | (in @ (sk8 @ Y @ X @ U) @ (sk7 @ U)) | (X = Y)) & (~ (in @ X @ U) | ~ (in @ Y @ U) | ~ ((in @ X @ (sk8 @ Y @ X @ U)) = (in @ Y @ (sk8 @ Y @ X @ U))) | (X = Y)) & (~ (in @ Z @ (sk7 @ U)) | ~ (in @ ZA @ (sk7 @ U)) | ~ (in @ ZB @ Z) | (in @ ZB @ ZA) | ~ (in @ ZC @ ZA) | (in @ ZC @ Z)) & ((in @ (sk10 @ ZD @ U) @ ZD) | ~ (in @ ZE @ ZD) | (sk9 @ U @ ZD)) & (~ (in @ (sk10 @ ZD @ U) @ U) | ~ (in @ ZE @ ZD) | (sk9 @ U @ ZD)) & (~ (sk9 @ U @ ZD) | (in @ (sk11 @ ZD @ U) @ (sk7 @ U))) & (~ (sk9 @ U @ ZD) | (in @ (sk12 @ ZD @ U) @ ZD)) & (~ (sk9 @ U @ ZD) | ~ (in @ ZF @ (sk11 @ ZD @ U)) | ~ (in @ ZF @ ZD)) & (~ (sk9 @ U @ ZD) | ~ (in @ ZG @ (sk7 @ U)) | ~ (in @ ZH @ ZG) | (in @ ZH @ (sk11 @ ZD @ U)) | (in @ (sk12 @ ZD @ U) @ ZG)) & (~ (ZI @ ZJ) | (ZI @ (sk13 @ ZJ @ (ZI))) | (ZI @ (descr @ (ZI)))) & (~ (ZI @ ZJ) | ~ (ZJ = (sk13 @ ZJ @ (ZI))) | (ZI @ (descr @ (ZI)))) & (~ (in @ ZM @ ZK) | ~ (ZL @ ZM) | (in @ ZM @ (dsetconstr @ ZK @ (ZL)))) & (~ (in @ ZP @ (dsetconstr @ ZN @ (ZO))) | (in @ ZP @ ZN)) & (~ (in @ ZS @ (dsetconstr @ ZQ @ (ZR))) | (ZR @ ZS)) & (~ (in @ ZU @ (prop2set @ ZT)) | (ZT)) & (~ (in @ ZV @ emptyset) | (ZW)) & ~ (in @ ZX @ emptyset) & ~ (in @ ZY @ emptyset) & (~ (ZZ @ ZZA) | (ZZ @ (sk14 @ ZZA @ (ZZ))) | (ZZ @ (sk15 @ (ZZ)))) & (~ (ZZ @ ZZA) | ~ (ZZA = (sk14 @ ZZA @ (ZZ))) | (ZZ @ (sk15 @ (ZZ)))) & ((in @ (sk16 @ ZZC @ ZZB) @ ZZB) | (in @ (sk17 @ ZZC @ ZZB) @ ZZC) | (ZZB = ZZC)) & ((in @ (sk16 @ ZZC @ ZZB) @ ZZB) | ~ (in @ (sk17 @ ZZC @ ZZB) @ ZZB) | (ZZB = ZZC)) & (~ (in @ (sk16 @ ZZC @ ZZB) @ ZZC) | (in @ (sk17 @ ZZC @ ZZB) @ ZZC) | (ZZB = ZZC)) & (~ (in @ (sk16 @ ZZC @ ZZB) @ ZZC) | ~ (in @ (sk17 @ ZZC @ ZZB) @ ZZB) | (ZZB = ZZC)) & ((in @ (sk18 @ ZZD) @ ZZD) | (ZZD = emptyset)) & ((in @ (sk19 @ ZZE) @ ZZE) | (ZZE = emptyset)) & (~ (in @ ZZH @ ZZF) | ((in @ ZZH @ (dsetconstr @ ZZF @ (ZZG))) = (ZZG @ ZZH))) & ((ZZI = emptyset) | (in @ (sk20 @ ZZI) @ ZZI)) & (~ (in @ ZZL @ ZZJ) | ~ (ZZK @ ZZL) | ~ ((dsetconstr @ ZZJ @ (ZZK)) = emptyset)) & (~ (in @ ZZN @ ZZM) | ~ (ZZM = emptyset)) & (in @ ZZO @ (setadjoin @ ZZO @ ZZP)) & (in @ emptyset @ (setadjoin @ emptyset @ emptyset)) & (~ (in @ ZZS @ ZZR) | (in @ ZZS @ (setadjoin @ ZZQ @ ZZR))) & (~ (in @ ZZV @ (setadjoin @ ZZT @ ZZU)) | (ZZV = ZZT) | (in @ ZZV @ ZZU) | (ZZW)) & (~ (in @ ZZV @ (setadjoin @ ZZT @ ZZU)) | (ZZV = ZZT) | ~ (ZZW) | (ZZW)) & (~ (in @ ZZV @ (setadjoin @ ZZT @ ZZU)) | ~ (ZZW) | (in @ ZZV @ ZZU) | (ZZW)) & (~ (in @ ZZV @ (setadjoin @ ZZT @ ZZU)) | ~ (ZZW) | ~ (ZZW) | (ZZW)) & (~ (in @ ZZZ @ (setadjoin @ ZZX @ ZZY)) | (ZZZ = ZZX) | (in @ ZZZ @ ZZY)) & ((dsetconstr @ ZZZA @ (^ [ZZZZZZZZZA:$i]: (($true)))) = ZZZA) & ((in @ (sk21 @ ZZZC @ ZZZB) @ ZZZC) | (in @ ZZZC @ (powerset @ ZZZB))) & (~ (in @ (sk21 @ ZZZC @ ZZZB) @ ZZZB) | (in @ ZZZC @ (powerset @ ZZZB))) & (in @ emptyset @ (powerset @ ZZZD)) & (in @ emptyset @ (powerset @ ZZZE)) & (~ (in @ ZZZG @ (powerset @ ZZZF)) | ~ (in @ ZZZH @ ZZZG) | (in @ ZZZH @ ZZZF)) & (~ (in @ ZZZJ @ ZZZK) | ~ (in @ ZZZK @ ZZZI) | (in @ ZZZJ @ (setunion @ ZZZI))) & (~ (in @ ZZZM @ (setunion @ ZZZL)) | (in @ ZZZM @ (sk22 @ ZZZN @ ZZZM @ ZZZL)) | (ZZZN)) & (~ (in @ ZZZM @ (setunion @ ZZZL)) | (in @ (sk22 @ ZZZN @ ZZZM @ ZZZL) @ ZZZL) | (ZZZN)) & (~ (in @ ZZZM @ (setunion @ ZZZL)) | ~ (ZZZN) | (ZZZN)) & (~ (in @ ZZZP @ ZZZO) | (in @ ZZZP @ (powerset @ (setunion @ ZZZO)))) & (~ (ZZZQ @ ZZZR) | (ZZZQ @ (sk23 @ ZZZR @ (ZZZQ))) | ((ZZZQ @ ZZZS) = (ZZZS = (sk24 @ (ZZZQ))))) & (~ (ZZZQ @ ZZZR) | ~ (ZZZR = (sk23 @ ZZZR @ (ZZZQ))) | ((ZZZQ @ ZZZS) = (ZZZS = (sk24 @ (ZZZQ))))) & ((ZZZT = emptyset) | (in @ (sk25 @ ZZZT) @ ZZZT)) & (~ (in @ ZZZU @ (setadjoin @ ZZZV @ emptyset)) | (ZZZU = ZZZV)) & ((ZZZW = ZZZX) | ~ (in @ ZZZX @ (setadjoin @ ZZZW @ emptyset))) & (~ (ZZZY = ZZZZ) | (in @ ZZZY @ (setadjoin @ ZZZZ @ emptyset))) & (~ (in @ ZZZZA @ (setadjoin @ ZZZZB @ emptyset)) | (in @ ZZZZB @ (setadjoin @ ZZZZA @ emptyset))) & (~ (in @ ZZZZE @ (setadjoin @ ZZZZC @ (setadjoin @ ZZZZD @ emptyset))) | (ZZZZE = ZZZZC) | (ZZZZE = ZZZZD)) & (in @ ZZZZF @ (setadjoin @ ZZZZF @ (setadjoin @ ZZZZG @ emptyset))) & (in @ ZZZZI @ (setadjoin @ ZZZZH @ (setadjoin @ ZZZZI @ emptyset))) & (~ (in @ ZZZZL @ ZZZZJ) | ~ (ZZZZK @ ZZZZL) | ~ ((dsetconstr @ ZZZZJ @ (ZZZZK)) = emptyset)) & (~ (in @ ZZZZN @ emptyset) | (ZZZZM @ ZZZZN)) & (~ (in @ ZZZZQ @ ZZZZO) | (ZZZZP @ ZZZZQ) | (in @ (sk26 @ (ZZZZP) @ ZZZZO) @ ZZZZO)) & (~ (in @ ZZZZQ @ ZZZZO) | (ZZZZP @ ZZZZQ) | ~ (ZZZZP @ (sk26 @ (ZZZZP) @ ZZZZO))) & ((in @ (sk27 @ (ZZZZS) @ ZZZZR) @ ZZZZR) | ~ (in @ ZZZZT @ ZZZZR) | ~ (ZZZZS @ ZZZZT)) & ((ZZZZS @ (sk27 @ (ZZZZS) @ ZZZZR)) | ~ (in @ ZZZZT @ ZZZZR) | ~ (ZZZZS @ ZZZZT)) & ((in @ (sk28 @ (ZZZZV) @ ZZZZU) @ ZZZZU) | ~ (in @ ZZZZW @ ZZZZU) | ~ (ZZZZV @ ZZZZW)) & ((ZZZZV @ (sk28 @ (ZZZZV) @ ZZZZU)) | ~ (in @ ZZZZW @ ZZZZU) | ~ (ZZZZV @ ZZZZW)) & (~ (in @ ZZZZZ @ ZZZZX) | (ZZZZY @ ZZZZZ) | (in @ (sk29 @ (ZZZZY) @ ZZZZX) @ ZZZZX)) & (~ (in @ ZZZZZ @ ZZZZX) | (ZZZZY @ ZZZZZ) | ~ (ZZZZY @ (sk29 @ (ZZZZY) @ ZZZZX))) & (~ (ZZZZZA) | (in @ emptyset @ (prop2set @ ZZZZZA))) & (~ (ZZZZZB) | (set2prop @ (prop2set @ ZZZZZB))) & ((in @ (sk30 @ (ZZZZZD) @ ZZZZZC) @ ZZZZZC) | ~ (in @ ZZZZZE @ ZZZZZC) | ~ (ZZZZZD @ ZZZZZE)) & ((ZZZZZD @ (sk30 @ (ZZZZZD) @ ZZZZZC)) | ~ (in @ ZZZZZE @ ZZZZZC) | ~ (ZZZZZD @ ZZZZZE)) & (~ (in @ ZZZZZH @ ZZZZZF) | (ZZZZZG @ ZZZZZH) | (in @ (sk31 @ (ZZZZZG) @ ZZZZZF) @ ZZZZZF)) & (~ (in @ ZZZZZH @ ZZZZZF) | (ZZZZZG @ ZZZZZH) | ~ (ZZZZZG @ (sk31 @ (ZZZZZG) @ ZZZZZF))) & (~ (ZZZZZI @ ZZZZZJ) | (ZZZZZI @ (sk32 @ (ZZZZZI))) | (ZZZZZI @ (sk34 @ (ZZZZZI)))) & (~ (ZZZZZI @ ZZZZZJ) | (ZZZZZI @ (sk32 @ (ZZZZZI))) | ~ (ZZZZZI @ ZZZZZK) | ((sk34 @ (ZZZZZI)) = ZZZZZK)) & (~ (ZZZZZI @ ZZZZZJ) | (ZZZZZI @ (sk33 @ (ZZZZZI))) | (ZZZZZI @ (sk34 @ (ZZZZZI)))) & (~ (ZZZZZI @ ZZZZZJ) | (ZZZZZI @ (sk33 @ (ZZZZZI))) | ~ (ZZZZZI @ ZZZZZK) | ((sk34 @ (ZZZZZI)) = ZZZZZK)) & (~ (ZZZZZI @ ZZZZZJ) | ~ ((sk32 @ (ZZZZZI)) = (sk33 @ (ZZZZZI))) | (ZZZZZI @ (sk34 @ (ZZZZZI)))) & (~ (ZZZZZI @ ZZZZZJ) | ~ ((sk32 @ (ZZZZZI)) = (sk33 @ (ZZZZZI))) | ~ (ZZZZZI @ ZZZZZK) | ((sk34 @ (ZZZZZI)) = ZZZZZK)) & (~ ((ZZZZZL @ (sk35 @ ZZZZZM @ (ZZZZZL))) = ((sk35 @ ZZZZZM @ (ZZZZZL)) = ZZZZZM)) | (ZZZZZL @ (sk36 @ (ZZZZZL)))) & (~ ((ZZZZZL @ (sk35 @ ZZZZZM @ (ZZZZZL))) = ((sk35 @ ZZZZZM @ (ZZZZZL)) = ZZZZZM)) | ~ (ZZZZZL @ ZZZZZN) | ((sk36 @ (ZZZZZL)) = ZZZZZN)) & (~ (ZZZZZO = ZZZZZP) | ~ (ZZZZZQ = ZZZZZR) | ~ (in @ ZZZZZQ @ ZZZZZO) | (in @ ZZZZZR @ ZZZZZP)) & (~ (ZZZZZS = ZZZZZT) | ~ (ZZZZZU = ZZZZZV) | ((in @ ZZZZZU @ ZZZZZS) = (in @ ZZZZZV @ ZZZZZT))) & (~ (ZZZZZW @ ZZZZZX) | (ZZZZZW @ (sk37 @ ZZZZZX @ (ZZZZZW))) | ~ (ZZZZZW @ ZZZZZY) | ~ (ZZZZZW @ ZZZZZZ) | (ZZZZZY = ZZZZZZ)) & (~ (ZZZZZW @ ZZZZZX) | ~ (ZZZZZX = (sk37 @ ZZZZZX @ (ZZZZZW))) | ~ (ZZZZZW @ ZZZZZY) | ~ (ZZZZZW @ ZZZZZZ) | (ZZZZZY = ZZZZZZ)) & (((sk38 @ (ZZZZZZB) @ (ZZZZZZA)) = (sk39 @ (ZZZZZZB) @ (ZZZZZZA))) | ((? [ZZZZZZZZZA:$i]: ((ZZZZZZA @ ZZZZZZZZZA) & ! [ZZZZZZZZZB:$i]: ((ZZZZZZA @ ZZZZZZZZZB) => (ZZZZZZZZZA = ZZZZZZZZZB)))) = (? [ZZZZZZZZZA:$i]: ((ZZZZZZB @ ZZZZZZZZZA) & ! [ZZZZZZZZZB:$i]: ((ZZZZZZB @ ZZZZZZZZZB) => (ZZZZZZZZZA = ZZZZZZZZZB)))))) & (~ ((ZZZZZZA @ (sk38 @ (ZZZZZZB) @ (ZZZZZZA))) = (ZZZZZZB @ (sk39 @ (ZZZZZZB) @ (ZZZZZZA)))) | ((? [ZZZZZZZZZA:$i]: ((ZZZZZZA @ ZZZZZZZZZA) & ! [ZZZZZZZZZB:$i]: ((ZZZZZZA @ ZZZZZZZZZB) => (ZZZZZZZZZA = ZZZZZZZZZB)))) = (? [ZZZZZZZZZA:$i]: ((ZZZZZZB @ ZZZZZZZZZA) & ! [ZZZZZZZZZB:$i]: ((ZZZZZZB @ ZZZZZZZZZB) => (ZZZZZZZZZA = ZZZZZZZZZB)))))) & (~ (ZZZZZZC = ZZZZZZD) | ~ (ZZZZZZE = ZZZZZZF) | ((setadjoin @ ZZZZZZC @ ZZZZZZE) = (setadjoin @ ZZZZZZD @ ZZZZZZF))) & (~ (ZZZZZZG = ZZZZZZH) | ((powerset @ ZZZZZZG) = (powerset @ ZZZZZZH))) & (~ (ZZZZZZI = ZZZZZZJ) | ((setunion @ ZZZZZZI) = (setunion @ ZZZZZZJ))) & (~ (ZZZZZZK @ ZZZZZZL) | (ZZZZZZK @ (sk40 @ ZZZZZZL @ (ZZZZZZK))) | ~ (ZZZZZZK @ ZZZZZZM) | ~ (ZZZZZZK @ ZZZZZZN) | (ZZZZZZM = ZZZZZZN)) & (~ (ZZZZZZK @ ZZZZZZL) | ~ (ZZZZZZL = (sk40 @ ZZZZZZL @ (ZZZZZZK))) | ~ (ZZZZZZK @ ZZZZZZM) | ~ (ZZZZZZK @ ZZZZZZN) | (ZZZZZZM = ZZZZZZN)) & (((sk42 @ (ZZZZZZP) @ (ZZZZZZO)) = (sk43 @ (ZZZZZZP) @ (ZZZZZZO))) | (sk41 @ ZZZZZZO @ ZZZZZZP)) & (~ ((ZZZZZZO @ (sk42 @ (ZZZZZZP) @ (ZZZZZZO))) = (ZZZZZZP @ (sk43 @ (ZZZZZZP) @ (ZZZZZZO)))) | (sk41 @ ZZZZZZO @ ZZZZZZP)) & (~ (sk41 @ ZZZZZZO @ ZZZZZZP) | ~ (ZZZZZZO @ ZZZZZZQ) | (ZZZZZZO @ (sk44 @ ZZZZZZQ @ (ZZZZZZP) @ (ZZZZZZO))) | ~ (ZZZZZZP @ ZZZZZZR) | (ZZZZZZP @ (sk45 @ ZZZZZZR @ (ZZZZZZP) @ (ZZZZZZO))) | ((descr @ (ZZZZZZO)) = (descr @ (ZZZZZZP)))) & (~ (sk41 @ ZZZZZZO @ ZZZZZZP) | ~ (ZZZZZZO @ ZZZZZZQ) | (ZZZZZZO @ (sk44 @ ZZZZZZQ @ (ZZZZZZP) @ (ZZZZZZO))) | ~ (ZZZZZZP @ ZZZZZZR) | ~ (ZZZZZZR = (sk45 @ ZZZZZZR @ (ZZZZZZP) @ (ZZZZZZO))) | ((descr @ (ZZZZZZO)) = (descr @ (ZZZZZZP)))) & (~ (sk41 @ ZZZZZZO @ ZZZZZZP) | ~ (ZZZZZZO @ ZZZZZZQ) | ~ (ZZZZZZQ = (sk44 @ ZZZZZZQ @ (ZZZZZZP) @ (ZZZZZZO))) | ~ (ZZZZZZP @ ZZZZZZR) | (ZZZZZZP @ (sk45 @ ZZZZZZR @ (ZZZZZZP) @ (ZZZZZZO))) | ((descr @ (ZZZZZZO)) = (descr @ (ZZZZZZP)))) & (~ (sk41 @ ZZZZZZO @ ZZZZZZP) | ~ (ZZZZZZO @ ZZZZZZQ) | ~ (ZZZZZZQ = (sk44 @ ZZZZZZQ @ (ZZZZZZP) @ (ZZZZZZO))) | ~ (ZZZZZZP @ ZZZZZZR) | ~ (ZZZZZZR = (sk45 @ ZZZZZZR @ (ZZZZZZP) @ (ZZZZZZO))) | ((descr @ (ZZZZZZO)) = (descr @ (ZZZZZZP)))) & (~ (ZZZZZZS = ZZZZZZT) | (in @ (sk46 @ (ZZZZZZV) @ (ZZZZZZU) @ ZZZZZZT @ ZZZZZZS) @ ZZZZZZS) | ((dsetconstr @ ZZZZZZS @ (ZZZZZZU)) = (dsetconstr @ ZZZZZZT @ (ZZZZZZV)))) & (~ (ZZZZZZS = ZZZZZZT) | (in @ (sk47 @ (ZZZZZZV) @ (ZZZZZZU) @ ZZZZZZT @ ZZZZZZS) @ ZZZZZZT) | ((dsetconstr @ ZZZZZZS @ (ZZZZZZU)) = (dsetconstr @ ZZZZZZT @ (ZZZZZZV)))) & (~ (ZZZZZZS = ZZZZZZT) | ((sk46 @ (ZZZZZZV) @ (ZZZZZZU) @ ZZZZZZT @ ZZZZZZS) = (sk47 @ (ZZZZZZV) @ (ZZZZZZU) @ ZZZZZZT @ ZZZZZZS)) | ((dsetconstr @ ZZZZZZS @ (ZZZZZZU)) = (dsetconstr @ ZZZZZZT @ (ZZZZZZV)))) & (~ (ZZZZZZS = ZZZZZZT) | ~ ((ZZZZZZU @ (sk46 @ (ZZZZZZV) @ (ZZZZZZU) @ ZZZZZZT @ ZZZZZZS)) = (ZZZZZZV @ (sk47 @ (ZZZZZZV) @ (ZZZZZZU) @ ZZZZZZT @ ZZZZZZS))) | ((dsetconstr @ ZZZZZZS @ (ZZZZZZU)) = (dsetconstr @ ZZZZZZT @ (ZZZZZZV)))) & ((in @ (sk48 @ ZZZZZZX @ ZZZZZZW) @ ZZZZZZW) | (subset @ ZZZZZZW @ ZZZZZZX)) & (~ (in @ (sk48 @ ZZZZZZX @ ZZZZZZW) @ ZZZZZZX) | (subset @ ZZZZZZW @ ZZZZZZX)) & (~ (ZZZZZZY = ZZZZZZZ) | (subset @ ZZZZZZZ @ ZZZZZZY)) & (~ (ZZZZZZZA = ZZZZZZZB) | (subset @ ZZZZZZZA @ ZZZZZZZB)) & ((in @ (sk49 @ ZZZZZZZD @ ZZZZZZZC) @ ZZZZZZZC) | (subset @ ZZZZZZZC @ ZZZZZZZD)) & (~ (in @ (sk49 @ ZZZZZZZD @ ZZZZZZZC) @ ZZZZZZZD) | (subset @ ZZZZZZZC @ ZZZZZZZD)) & (subset @ emptyset @ ZZZZZZZE) & (~ (subset @ ZZZZZZZF @ ZZZZZZZG) | ~ (in @ ZZZZZZZH @ ZZZZZZZF) | (in @ ZZZZZZZH @ ZZZZZZZG)) & (~ (subset @ ZZZZZZZI @ ZZZZZZZJ) | (in @ ZZZZZZZK @ ZZZZZZZJ) | ~ (in @ ZZZZZZZK @ ZZZZZZZI)) & (~ (in @ ZZZZZZZN @ ZZZZZZZL) | (in @ ZZZZZZZN @ ZZZZZZZM) | ~ (subset @ ZZZZZZZL @ ZZZZZZZM)) & ((subset @ ZZZZZZZO @ ZZZZZZZP) | ~ (ZZZZZZZO = ZZZZZZZP)) & (~ (in @ ZZZZZZZS @ ZZZZZZZQ) | (in @ ZZZZZZZS @ ZZZZZZZR) | ~ (ZZZZZZZQ = ZZZZZZZR)) & (subset @ ZZZZZZZT @ ZZZZZZZT) & (~ (subset @ ZZZZZZZU @ ZZZZZZZV) | ~ (subset @ ZZZZZZZV @ ZZZZZZZW) | (subset @ ZZZZZZZU @ ZZZZZZZW)) & (subset @ ZZZZZZZY @ (setadjoin @ ZZZZZZZX @ ZZZZZZZY)) & (~ (subset @ ZZZZZZZZ @ ZZZZZZZZB) | (subset @ ZZZZZZZZ @ (setadjoin @ ZZZZZZZZA @ ZZZZZZZZB))) & (~ (subset @ ZZZZZZZZC @ ZZZZZZZZD) | (in @ ZZZZZZZZC @ (powerset @ ZZZZZZZZD))) & (~ (subset @ ZZZZZZZZE @ ZZZZZZZZF) | ~ (subset @ ZZZZZZZZF @ ZZZZZZZZE) | (ZZZZZZZZE = ZZZZZZZZF)) & (~ (subset @ ZZZZZZZZG @ emptyset) | (ZZZZZZZZG = emptyset)) & (~ (subset @ ZZZZZZZZI @ ZZZZZZZZH) | (in @ ZZZZZZZZI @ (powerset @ ZZZZZZZZH))) & (~ (in @ ZZZZZZZZK @ (powerset @ ZZZZZZZZJ)) | (subset @ ZZZZZZZZK @ ZZZZZZZZJ)) & (in @ ZZZZZZZZL @ (powerset @ ZZZZZZZZL)) & (~ (subset @ ZZZZZZZZM @ ZZZZZZZZN) | (subset @ (powerset @ ZZZZZZZZM) @ (powerset @ ZZZZZZZZN))) & (in @ (dsetconstr @ ZZZZZZZZO @ (ZZZZZZZZP)) @ (powerset @ ZZZZZZZZO)) & (subset @ (dsetconstr @ ZZZZZZZZQ @ (ZZZZZZZZR)) @ ZZZZZZZZQ) & (~ (in @ ZZZZZZZZU @ ZZZZZZZZS) | (in @ ZZZZZZZZU @ (setunion @ (setadjoin @ ZZZZZZZZS @ (setadjoin @ ZZZZZZZZT @ emptyset))))) & (in @ ZZZZZZZZW @ (setadjoin @ ZZZZZZZZV @ (setadjoin @ ZZZZZZZZW @ emptyset))) & (~ (in @ ZZZZZZZZZ @ ZZZZZZZZY) | (in @ ZZZZZZZZZ @ (setunion @ (setadjoin @ ZZZZZZZZX @ (setadjoin @ ZZZZZZZZY @ emptyset))))) & (in @ sk52 @ (setunion @ (setadjoin @ sk50 @ (setadjoin @ sk51 @ emptyset)))) & (~ (in @ sk52 @ sk50) | (sk53)) & (~ (in @ sk52 @ sk51) | (sk53)) & ~ (sk53)))),inference(cnf,[status(esa)],[4])).
% 89.50/19.97 thf(92,plain,(! [A:$i] : ((A = emptyset) | (in @ (sk25 @ A) @ A))),inference(cnfConj,[status(thm)],[5])).
% 89.50/19.97 thf(255,plain,(! [A:$i] : ((A = emptyset) | (in @ (sk25 @ A) @ A))),inference(lifteq,[status(thm)],[92])).
% 89.50/19.97 thf(256,plain,(! [A:$i] : ((A = emptyset) | (in @ (sk25 @ A) @ A))),inference(simp,[status(thm)],[255])).
% 89.50/19.97 thf(34,plain,((in @ sk52 @ (setunion @ (setadjoin @ sk50 @ (setadjoin @ sk51 @ emptyset))))),inference(cnfConj,[status(thm)],[5])).
% 89.50/19.97 thf(25,plain,(! [A:$i] : ((~ (in @ A @ emptyset)))),inference(cnfConj,[status(thm)],[5])).
% 89.50/19.97 thf(202,plain,(! [A:$i] : ((~ (in @ A @ emptyset)))),inference(simp,[status(thm)],[25])).
% 89.50/19.97 thf(460,plain,(! [A:$i] : (~ (($true)) | ((in @ sk52 @ (setunion @ (setadjoin @ sk50 @ (setadjoin @ sk51 @ emptyset)))) != (in @ A @ emptyset)))),inference(paramod_ordered,[status(thm)],[34,202])).
% 89.50/19.97 thf(461,plain,(! [A:$i] : (((in @ sk52 @ (setunion @ (setadjoin @ sk50 @ (setadjoin @ sk51 @ emptyset)))) != (in @ A @ emptyset)))),inference(simp,[status(thm)],[460])).
% 89.50/19.97 thf(464,plain,(! [A:$i] : ((sk52 != A) | ((setunion @ (setadjoin @ sk50 @ (setadjoin @ sk51 @ emptyset))) != emptyset))),inference(simp,[status(thm)],[461])).
% 89.50/19.97 thf(465,plain,(((setunion @ (setadjoin @ sk50 @ (setadjoin @ sk51 @ emptyset))) != emptyset)),inference(simp,[status(thm)],[464])).
% 89.50/19.97 thf(928,plain,(! [A:$i] : ((in @ (sk25 @ A) @ A) | (emptyset != emptyset) | (A != (setunion @ (setadjoin @ sk50 @ (setadjoin @ sk51 @ emptyset)))))),inference(paramod_ordered,[status(thm)],[256,465])).
% 89.50/19.97 thf(929,plain,(! [A:$i] : ((in @ (sk25 @ A) @ A) | (A != (setunion @ (setadjoin @ sk50 @ (setadjoin @ sk51 @ emptyset)))))),inference(simp,[status(thm)],[928])).
% 89.50/19.97 thf(930,plain,((in @ (sk25 @ (setunion @ (setadjoin @ sk50 @ (setadjoin @ sk51 @ emptyset)))) @ (setunion @ (setadjoin @ sk50 @ (setadjoin @ sk51 @ emptyset))))),inference(pattern_uni,[status(thm)],[929:[bind(A, $thf(setunion @ (setadjoin @ sk50 @ (setadjoin @ sk51 @ emptyset))))]])).
% 89.50/19.97 thf(142,plain,(! [B:$i,A:$i] : ((~ (subset @ A @ B)) | (in @ A @ (powerset @ B)))),inference(cnfConj,[status(thm)],[5])).
% 89.50/19.97 thf(192,plain,(! [B:$i,A:$i] : ((~ (subset @ A @ B)) | (in @ A @ (powerset @ B)))),inference(simp,[status(thm)],[142])).
% 89.50/19.97 thf(7,plain,(! [B:$i,A:$i] : (((in @ B @ (setunion @ A)) = (? [C:$i]: ((in @ B @ C) & (in @ C @ A)))))),inference(cnfConj,[status(thm)],[5])).
% 89.50/19.97 thf(324,plain,(! [B:$i,A:$i] : (((in @ B @ (setunion @ A)) = (? [C:$i]: ((in @ B @ C) & (in @ C @ A)))))),inference(lifteq,[status(thm)],[7])).
% 89.50/19.97 thf(325,plain,(! [B:$i,A:$i] : (((in @ B @ (setunion @ A)) = (? [C:$i]: ((in @ B @ C) & (in @ C @ A)))))),inference(simp,[status(thm)],[324])).
% 89.50/19.97 thf(6591,plain,(! [B:$i,A:$i] : ((? [C:$i]: ((in @ B @ C) & (in @ C @ A))) | ((in @ B @ (setunion @ A)) != (in @ sk52 @ (setunion @ (setadjoin @ sk50 @ (setadjoin @ sk51 @ emptyset))))))),inference(paramod_ordered,[status(thm)],[325,34])).
% 89.50/19.97 thf(6592,plain,((? [A:$i]: ((in @ sk52 @ A) & (in @ A @ (setadjoin @ sk50 @ (setadjoin @ sk51 @ emptyset)))))),inference(pattern_uni,[status(thm)],[6591:[bind(A, $thf(setadjoin @ sk50 @ (setadjoin @ sk51 @ emptyset))),bind(B, $thf(sk52))]])).
% 89.50/19.97 thf(6947,plain,(((in @ sk52 @ sk200) & (in @ sk200 @ (setadjoin @ sk50 @ (setadjoin @ sk51 @ emptyset))))),inference(cnf,[status(esa)],[6592])).
% 89.50/19.97 thf(6948,plain,((in @ sk52 @ sk200)),inference(cnfConj,[status(thm)],[6947])).
% 89.50/19.97 thf(10,plain,((~ (in @ sk52 @ sk51)) | sk53),inference(cnfConj,[status(thm)],[5])).
% 89.50/19.97 thf(54,plain,(~ (sk53)),inference(cnfConj,[status(thm)],[5])).
% 89.50/19.97 thf(440,plain,((~ (in @ sk52 @ sk51)) | ($false)),inference(rewrite,[status(thm)],[10,54])).
% 89.50/19.97 thf(441,plain,((~ (in @ sk52 @ sk51))),inference(simp,[status(thm)],[440])).
% 89.50/19.97 thf(7081,plain,(~ (($true)) | ((in @ sk52 @ sk200) != (in @ sk52 @ sk51))),inference(paramod_ordered,[status(thm)],[6948,441])).
% 89.50/19.97 thf(7082,plain,(((in @ sk52 @ sk200) != (in @ sk52 @ sk51))),inference(simp,[status(thm)],[7081])).
% 89.50/19.97 thf(7103,plain,((sk52 != sk52) | (sk200 != sk51)),inference(simp,[status(thm)],[7082])).
% 89.50/19.97 thf(7159,plain,((sk200 != sk51)),inference(simp,[status(thm)],[7103])).
% 89.50/19.97 thf(24,plain,(! [A:$i] : ((in @ A @ (powerset @ A)))),inference(cnfConj,[status(thm)],[5])).
% 89.50/19.97 thf(199,plain,(! [A:$i] : ((in @ A @ (powerset @ A)))),inference(simp,[status(thm)],[24])).
% 89.50/19.97 thf(45,plain,((~ (in @ sk52 @ sk50)) | sk53),inference(cnfConj,[status(thm)],[5])).
% 89.50/19.97 thf(448,plain,((~ (in @ sk52 @ sk50)) | ($false)),inference(rewrite,[status(thm)],[45,54])).
% 89.50/19.97 thf(449,plain,((~ (in @ sk52 @ sk50))),inference(simp,[status(thm)],[448])).
% 89.50/19.97 thf(608,plain,(! [A:$i] : (~ (($true)) | ((in @ A @ (powerset @ A)) != (in @ sk52 @ sk50)))),inference(paramod_ordered,[status(thm)],[199,449])).
% 89.50/19.97 thf(609,plain,(! [A:$i] : (((in @ A @ (powerset @ A)) != (in @ sk52 @ sk50)))),inference(simp,[status(thm)],[608])).
% 89.50/19.97 thf(623,plain,(! [A:$i] : ((A != sk52) | ((powerset @ A) != sk50))),inference(simp,[status(thm)],[609])).
% 89.50/19.97 thf(629,plain,(((powerset @ sk52) != sk50)),inference(simp,[status(thm)],[623])).
% 89.50/19.97 thf(94,plain,(! [B:$i,A:$i] : ((~ (A = B)) | (in @ A @ (setadjoin @ B @ emptyset)))),inference(cnfConj,[status(thm)],[5])).
% 89.50/19.97 thf(412,plain,(! [B:$i,A:$i] : ((A != B) | (in @ A @ (setadjoin @ B @ emptyset)))),inference(lifteq,[status(thm)],[94])).
% 89.50/19.97 thf(413,plain,(! [A:$i] : ((in @ A @ (setadjoin @ A @ emptyset)))),inference(simp,[status(thm)],[412])).
% 89.50/19.97 thf(738,plain,(! [A:$i] : (~ (($true)) | ((in @ A @ (setadjoin @ A @ emptyset)) != (in @ sk52 @ sk51)))),inference(paramod_ordered,[status(thm)],[413,441])).
% 89.50/19.97 thf(739,plain,(! [A:$i] : (((in @ A @ (setadjoin @ A @ emptyset)) != (in @ sk52 @ sk51)))),inference(simp,[status(thm)],[738])).
% 89.50/19.97 thf(750,plain,(! [A:$i] : ((A != sk52) | ((setadjoin @ A @ emptyset) != sk51))),inference(simp,[status(thm)],[739])).
% 89.50/19.97 thf(760,plain,(((setadjoin @ sk52 @ emptyset) != sk51)),inference(simp,[status(thm)],[750])).
% 89.50/19.97 thf(145,plain,(! [B:($i > $o),A:$i] : ((subset @ (dsetconstr @ A @ (B)) @ A))),inference(cnfConj,[status(thm)],[5])).
% 89.50/19.97 thf(347,plain,(! [B:($i > $o),A:$i] : ((subset @ (dsetconstr @ A @ (B)) @ A))),inference(simp,[status(thm)],[145])).
% 89.50/19.97 thf(6553,plain,(! [B:$i,A:$i] : ((? [C:$i]: ((in @ B @ C) & (in @ C @ A))) | ((in @ (sk25 @ (setunion @ (setadjoin @ sk50 @ (setadjoin @ sk51 @ emptyset)))) @ (setunion @ (setadjoin @ sk50 @ (setadjoin @ sk51 @ emptyset)))) != (in @ B @ (setunion @ A))))),inference(paramod_ordered,[status(thm)],[930,325])).
% 89.50/19.97 thf(6554,plain,((? [A:$i]: ((in @ (sk25 @ (setunion @ (setadjoin @ sk50 @ (setadjoin @ sk51 @ emptyset)))) @ A) & (in @ A @ (setadjoin @ sk50 @ (setadjoin @ sk51 @ emptyset)))))),inference(pattern_uni,[status(thm)],[6553:[bind(A, $thf(setadjoin @ sk50 @ (setadjoin @ sk51 @ emptyset))),bind(B, $thf(sk25 @ (setunion @ (setadjoin @ sk50 @ (setadjoin @ sk51 @ emptyset)))))]])).
% 89.50/19.97 thf(6805,plain,(((in @ (sk25 @ (setunion @ (setadjoin @ sk50 @ (setadjoin @ sk51 @ emptyset)))) @ sk177) & (in @ sk177 @ (setadjoin @ sk50 @ (setadjoin @ sk51 @ emptyset))))),inference(cnf,[status(esa)],[6554])).
% 89.50/19.97 thf(6806,plain,((in @ (sk25 @ (setunion @ (setadjoin @ sk50 @ (setadjoin @ sk51 @ emptyset)))) @ sk177)),inference(cnfConj,[status(thm)],[6805])).
% 89.50/19.97 thf(10574,plain,(! [A:$i] : (~ (($true)) | ((in @ (sk25 @ (setunion @ (setadjoin @ sk50 @ (setadjoin @ sk51 @ emptyset)))) @ sk177) != (in @ A @ emptyset)))),inference(paramod_ordered,[status(thm)],[6806,202])).
% 89.50/19.97 thf(10575,plain,(! [A:$i] : (((in @ (sk25 @ (setunion @ (setadjoin @ sk50 @ (setadjoin @ sk51 @ emptyset)))) @ sk177) != (in @ A @ emptyset)))),inference(simp,[status(thm)],[10574])).
% 89.50/19.97 thf(10694,plain,(! [A:$i] : (((sk25 @ (setunion @ (setadjoin @ sk50 @ (setadjoin @ sk51 @ emptyset)))) != A) | (sk177 != emptyset))),inference(simp,[status(thm)],[10575])).
% 89.50/19.97 thf(10736,plain,((sk177 != emptyset)),inference(simp,[status(thm)],[10694])).
% 89.50/19.97 thf(10757,plain,(! [A:$i] : ((in @ (sk25 @ A) @ A) | (emptyset != emptyset) | (A != sk177))),inference(paramod_ordered,[status(thm)],[256,10736])).
% 89.50/19.97 thf(10758,plain,(! [A:$i] : ((in @ (sk25 @ A) @ A) | (A != sk177))),inference(simp,[status(thm)],[10757])).
% 89.50/19.97 thf(10759,plain,((in @ (sk25 @ sk177) @ sk177)),inference(pattern_uni,[status(thm)],[10758:[bind(A, $thf(sk177))]])).
% 89.50/19.97 thf(10817,plain,(~ (($true)) | ((in @ (sk25 @ sk177) @ sk177) != (in @ sk52 @ sk51))),inference(paramod_ordered,[status(thm)],[10759,441])).
% 89.50/19.97 thf(10818,plain,(((in @ (sk25 @ sk177) @ sk177) != (in @ sk52 @ sk51))),inference(simp,[status(thm)],[10817])).
% 89.50/19.97 thf(10844,plain,(((sk25 @ sk177) != sk52) | (sk177 != sk51)),inference(simp,[status(thm)],[10818])).
% 89.50/19.97 thf(29,plain,(! [B:($i > $o),A:($i > $o)] : ((~ ((A @ (sk42 @ (B) @ (A))) = (B @ (sk43 @ (B) @ (A))))) | (sk41 @ A @ B))),inference(cnfConj,[status(thm)],[5])).
% 89.50/19.97 thf(216,plain,(! [B:($i > $o),A:($i > $o)] : (((A @ (sk42 @ (B) @ (A))) != (B @ (sk43 @ (B) @ (A)))) | (sk41 @ A @ B))),inference(lifteq,[status(thm)],[29])).
% 89.50/19.97 thf(217,plain,(! [B:($i > $o),A:($i > $o)] : (((A @ (sk42 @ (B) @ (A))) != (B @ (sk43 @ (B) @ (A)))) | (sk41 @ A @ B))),inference(simp,[status(thm)],[216])).
% 89.50/19.97 thf(6593,plain,(! [B:$i,A:$i] : ((? [C:$i]: ((in @ B @ C) & (in @ C @ A))) | ((in @ sk52 @ (setunion @ (setadjoin @ sk50 @ (setadjoin @ sk51 @ emptyset)))) != (in @ B @ (setunion @ A))))),inference(paramod_ordered,[status(thm)],[34,325])).
% 89.50/19.97 thf(6594,plain,((? [A:$i]: ((in @ sk52 @ A) & (in @ A @ (setadjoin @ sk50 @ (setadjoin @ sk51 @ emptyset)))))),inference(pattern_uni,[status(thm)],[6593:[bind(A, $thf(setadjoin @ sk50 @ (setadjoin @ sk51 @ emptyset))),bind(B, $thf(sk52))]])).
% 89.50/19.97 thf(6960,plain,(((in @ sk52 @ sk203) & (in @ sk203 @ (setadjoin @ sk50 @ (setadjoin @ sk51 @ emptyset))))),inference(cnf,[status(esa)],[6594])).
% 89.50/19.97 thf(6961,plain,((in @ sk52 @ sk203)),inference(cnfConj,[status(thm)],[6960])).
% 89.50/19.97 thf(57,plain,(! [B:$i,A:$i] : ((~ (in @ B @ A)) | (in @ B @ (powerset @ (setunion @ A))))),inference(cnfConj,[status(thm)],[5])).
% 89.50/19.97 thf(214,plain,(! [B:$i,A:$i] : ((~ (in @ B @ A)) | (in @ B @ (powerset @ (setunion @ A))))),inference(simp,[status(thm)],[57])).
% 89.50/19.97 thf(11835,plain,(! [B:$i,A:$i] : (~ (($true)) | (in @ B @ (powerset @ (setunion @ A))) | ((in @ sk52 @ sk203) != (in @ B @ A)))),inference(paramod_ordered,[status(thm)],[6961,214])).
% 89.50/19.97 thf(11836,plain,(! [B:$i,A:$i] : ((in @ B @ (powerset @ (setunion @ A))) | ((in @ sk52 @ sk203) != (in @ B @ A)))),inference(simp,[status(thm)],[11835])).
% 89.50/19.97 thf(11837,plain,((in @ sk52 @ (powerset @ (setunion @ sk203)))),inference(pattern_uni,[status(thm)],[11836:[bind(A, $thf(sk203)),bind(B, $thf(sk52))]])).
% 89.50/19.97 thf(12038,plain,(! [B:$i,A:$i] : (~ (($true)) | (in @ B @ (powerset @ (setunion @ A))) | ((in @ sk52 @ (powerset @ (setunion @ sk203))) != (in @ B @ A)))),inference(paramod_ordered,[status(thm)],[11837,214])).
% 89.50/19.97 thf(12039,plain,(! [B:$i,A:$i] : ((in @ B @ (powerset @ (setunion @ A))) | ((in @ sk52 @ (powerset @ (setunion @ sk203))) != (in @ B @ A)))),inference(simp,[status(thm)],[12038])).
% 89.50/19.97 thf(12040,plain,((in @ sk52 @ (powerset @ (setunion @ (powerset @ (setunion @ sk203)))))),inference(pattern_uni,[status(thm)],[12039:[bind(A, $thf(powerset @ (setunion @ sk203))),bind(B, $thf(sk52))]])).
% 89.50/19.97 thf(146,plain,(! [A:$o] : (~ (A) | (set2prop @ (prop2set @ A)))),inference(cnfConj,[status(thm)],[5])).
% 89.50/19.97 thf(406,plain,(! [A:$o] : (~ (A) | (set2prop @ (prop2set @ A)))),inference(simp,[status(thm)],[146])).
% 89.50/19.97 thf(1433,plain,((set2prop @ (prop2set @ ($true)))),inference(simp,[status(thm)],[406])).
% 89.50/19.97 thf(1554,plain,(! [A:$i] : ((in @ (sk25 @ A) @ A) | (set2prop @ emptyset) | (A != (prop2set @ ($true))))),inference(paramod_ordered,[status(thm)],[256,1433])).
% 89.50/19.97 thf(1555,plain,((in @ (sk25 @ (prop2set @ ($true))) @ (prop2set @ ($true))) | (set2prop @ emptyset)),inference(pattern_uni,[status(thm)],[1554:[bind(A, $thf(prop2set @ ($true)))]])).
% 89.50/19.97 thf(3240,plain,(! [A:$i] : ((set2prop @ emptyset) | ~ (($true)) | ((in @ (sk25 @ (prop2set @ ($true))) @ (prop2set @ ($true))) != (in @ A @ emptyset)))),inference(paramod_ordered,[status(thm)],[1555,202])).
% 89.50/19.97 thf(3241,plain,(! [A:$i] : ((set2prop @ emptyset) | ((in @ (sk25 @ (prop2set @ ($true))) @ (prop2set @ ($true))) != (in @ A @ emptyset)))),inference(simp,[status(thm)],[3240])).
% 89.50/19.97 thf(3272,plain,(! [A:$i] : ((set2prop @ emptyset) | ((sk25 @ (prop2set @ ($true))) != A) | ((prop2set @ ($true)) != emptyset))),inference(simp,[status(thm)],[3241])).
% 89.50/19.97 thf(3285,plain,((set2prop @ emptyset) | ((prop2set @ ($true)) != emptyset)),inference(simp,[status(thm)],[3272])).
% 89.50/19.97 thf(21,plain,(! [B:$i,A:$i] : ((subset @ B @ (setadjoin @ A @ B)))),inference(cnfConj,[status(thm)],[5])).
% 89.50/19.97 thf(253,plain,(! [B:$i,A:$i] : ((subset @ B @ (setadjoin @ A @ B)))),inference(simp,[status(thm)],[21])).
% 89.50/19.97 thf(2600,plain,(! [D:$i,C:$i,B:$i,A:$i] : (~ (($true)) | (in @ C @ (powerset @ D)) | ((subset @ B @ (setadjoin @ A @ B)) != (subset @ C @ D)))),inference(paramod_ordered,[status(thm)],[253,192])).
% 89.50/19.97 thf(2601,plain,(! [D:$i,C:$i,B:$i,A:$i] : ((in @ C @ (powerset @ D)) | ((subset @ B @ (setadjoin @ A @ B)) != (subset @ C @ D)))),inference(simp,[status(thm)],[2600])).
% 89.50/19.97 thf(2602,plain,(! [B:$i,A:$i] : ((in @ B @ (powerset @ (setadjoin @ A @ B))))),inference(pattern_uni,[status(thm)],[2601:[bind(A, $thf(E)),bind(B, $thf(F)),bind(C, $thf(F)),bind(D, $thf(setadjoin @ E @ F))]])).
% 89.50/19.97 thf(2613,plain,(! [B:$i,A:$i] : ((in @ B @ (powerset @ (setadjoin @ A @ B))))),inference(simp,[status(thm)],[2602])).
% 89.50/19.97 thf(2638,plain,(! [B:$i,A:$i] : (~ (($true)) | ((in @ B @ (powerset @ (setadjoin @ A @ B))) != (in @ sk52 @ sk51)))),inference(paramod_ordered,[status(thm)],[2613,441])).
% 89.50/19.97 thf(2639,plain,(! [B:$i,A:$i] : (((in @ B @ (powerset @ (setadjoin @ A @ B))) != (in @ sk52 @ sk51)))),inference(simp,[status(thm)],[2638])).
% 89.50/19.97 thf(2655,plain,(! [B:$i,A:$i] : ((B != sk52) | ((powerset @ (setadjoin @ A @ B)) != sk51))),inference(simp,[status(thm)],[2639])).
% 89.50/19.97 thf(2676,plain,(! [A:$i] : (((powerset @ (setadjoin @ A @ sk52)) != sk51))),inference(simp,[status(thm)],[2655])).
% 89.50/19.97 thf(52,plain,(! [B:$i,A:($i > $o)] : ((~ (A @ B)) | (A @ (sk32 @ (A))) | (A @ (sk34 @ (A))))),inference(cnfConj,[status(thm)],[5])).
% 89.50/19.97 thf(203,plain,(! [B:$i,A:($i > $o)] : ((~ (A @ B)) | (A @ (sk32 @ (A))) | (A @ (sk34 @ (A))))),inference(simp,[status(thm)],[52])).
% 89.50/19.97 thf(4578,plain,(! [B:$i,A:($i > $o)] : (~ (($true)) | (A @ (sk32 @ (A))) | (A @ (sk34 @ (A))) | ((set2prop @ (prop2set @ ($true))) != (A @ B)))),inference(paramod_ordered,[status(thm)],[1433,203])).
% 89.50/19.97 thf(4579,plain,(! [B:$i,A:($i > $o)] : ((A @ (sk32 @ (A))) | (A @ (sk34 @ (A))) | ((set2prop @ (prop2set @ ($true))) != (A @ B)))),inference(simp,[status(thm)],[4578])).
% 89.50/19.97 thf(4960,plain,((set2prop @ (sk32 @ (set2prop))) | (set2prop @ (sk34 @ (set2prop)))),inference(pre_uni,[status(thm)],[4579:[bind(A, $thf(set2prop)),bind(B, $thf(prop2set @ ($true)))]])).
% 89.50/19.97 thf(20,plain,(! [B:$i,A:$i] : ((in @ A @ (setadjoin @ A @ B)))),inference(cnfConj,[status(thm)],[5])).
% 89.50/19.97 thf(209,plain,(! [B:$i,A:$i] : ((in @ A @ (setadjoin @ A @ B)))),inference(simp,[status(thm)],[20])).
% 89.50/19.97 thf(765,plain,(! [C:$i,B:$i,A:$i] : (~ (($true)) | ((in @ A @ (setadjoin @ A @ B)) != (in @ C @ emptyset)))),inference(paramod_ordered,[status(thm)],[209,202])).
% 89.50/19.97 thf(766,plain,(! [C:$i,B:$i,A:$i] : (((in @ A @ (setadjoin @ A @ B)) != (in @ C @ emptyset)))),inference(simp,[status(thm)],[765])).
% 89.50/19.97 thf(781,plain,(! [C:$i,B:$i,A:$i] : ((A != C) | ((setadjoin @ A @ B) != emptyset))),inference(simp,[status(thm)],[766])).
% 89.50/19.97 thf(790,plain,(! [B:$i,A:$i] : (((setadjoin @ B @ A) != emptyset))),inference(simp,[status(thm)],[781])).
% 89.50/19.97 thf(1102,plain,(! [C:$i,B:$i,A:$i] : ((in @ (sk25 @ A) @ A) | (emptyset != emptyset) | (A != (setadjoin @ C @ B)))),inference(paramod_ordered,[status(thm)],[256,790])).
% 89.50/19.97 thf(1103,plain,(! [C:$i,B:$i,A:$i] : ((in @ (sk25 @ A) @ A) | (A != (setadjoin @ C @ B)))),inference(simp,[status(thm)],[1102])).
% 89.50/19.97 thf(1104,plain,(! [B:$i,A:$i] : ((in @ (sk25 @ (setadjoin @ A @ B)) @ (setadjoin @ A @ B)))),inference(pattern_uni,[status(thm)],[1103:[bind(A, $thf(setadjoin @ D @ E)),bind(B, $thf(E)),bind(C, $thf(D))]])).
% 89.50/19.98 thf(1142,plain,(! [B:$i,A:$i] : ((in @ (sk25 @ (setadjoin @ A @ B)) @ (setadjoin @ A @ B)))),inference(simp,[status(thm)],[1104])).
% 89.50/19.98 thf(7190,plain,(! [A:$i] : (~ (($true)) | ((in @ sk52 @ sk203) != (in @ A @ emptyset)))),inference(paramod_ordered,[status(thm)],[6961,202])).
% 89.50/19.98 thf(7191,plain,(! [A:$i] : (((in @ sk52 @ sk203) != (in @ A @ emptyset)))),inference(simp,[status(thm)],[7190])).
% 89.50/19.98 thf(7250,plain,(! [A:$i] : ((sk52 != A) | (sk203 != emptyset))),inference(simp,[status(thm)],[7191])).
% 89.50/19.98 thf(7282,plain,((sk203 != emptyset)),inference(simp,[status(thm)],[7250])).
% 89.50/19.98 thf(7312,plain,(! [A:$i] : ((in @ (sk25 @ A) @ A) | (emptyset != emptyset) | (A != sk203))),inference(paramod_ordered,[status(thm)],[256,7282])).
% 89.50/19.98 thf(7313,plain,(! [A:$i] : ((in @ (sk25 @ A) @ A) | (A != sk203))),inference(simp,[status(thm)],[7312])).
% 89.50/19.98 thf(7314,plain,((in @ (sk25 @ sk203) @ sk203)),inference(pattern_uni,[status(thm)],[7313:[bind(A, $thf(sk203))]])).
% 89.50/19.98 thf(11682,plain,(! [B:$i,A:$i] : (~ (($true)) | (in @ B @ (powerset @ (setunion @ A))) | ((in @ (sk25 @ sk203) @ sk203) != (in @ B @ A)))),inference(paramod_ordered,[status(thm)],[7314,214])).
% 89.50/19.98 thf(11683,plain,(! [B:$i,A:$i] : ((in @ B @ (powerset @ (setunion @ A))) | ((in @ (sk25 @ sk203) @ sk203) != (in @ B @ A)))),inference(simp,[status(thm)],[11682])).
% 89.50/19.98 thf(11684,plain,((in @ (sk25 @ sk203) @ (powerset @ (setunion @ sk203)))),inference(pattern_uni,[status(thm)],[11683:[bind(A, $thf(sk203)),bind(B, $thf(sk25 @ sk203))]])).
% 89.50/19.98 thf(6551,plain,(! [B:$i,A:$i] : ((? [C:$i]: ((in @ B @ C) & (in @ C @ A))) | ((in @ B @ (setunion @ A)) != (in @ (sk25 @ (setunion @ (setadjoin @ sk50 @ (setadjoin @ sk51 @ emptyset)))) @ (setunion @ (setadjoin @ sk50 @ (setadjoin @ sk51 @ emptyset))))))),inference(paramod_ordered,[status(thm)],[325,930])).
% 89.50/19.98 thf(6552,plain,((? [A:$i]: ((in @ (sk25 @ (setunion @ (setadjoin @ sk50 @ (setadjoin @ sk51 @ emptyset)))) @ A) & (in @ A @ (setadjoin @ sk50 @ (setadjoin @ sk51 @ emptyset)))))),inference(pattern_uni,[status(thm)],[6551:[bind(A, $thf(setadjoin @ sk50 @ (setadjoin @ sk51 @ emptyset))),bind(B, $thf(sk25 @ (setunion @ (setadjoin @ sk50 @ (setadjoin @ sk51 @ emptyset)))))]])).
% 89.50/19.98 thf(6792,plain,(((in @ (sk25 @ (setunion @ (setadjoin @ sk50 @ (setadjoin @ sk51 @ emptyset)))) @ sk174) & (in @ sk174 @ (setadjoin @ sk50 @ (setadjoin @ sk51 @ emptyset))))),inference(cnf,[status(esa)],[6552])).
% 89.50/19.98 thf(6793,plain,((in @ (sk25 @ (setunion @ (setadjoin @ sk50 @ (setadjoin @ sk51 @ emptyset)))) @ sk174)),inference(cnfConj,[status(thm)],[6792])).
% 89.50/19.98 thf(10235,plain,(! [A:$i] : (~ (($true)) | ((in @ (sk25 @ (setunion @ (setadjoin @ sk50 @ (setadjoin @ sk51 @ emptyset)))) @ sk174) != (in @ A @ emptyset)))),inference(paramod_ordered,[status(thm)],[6793,202])).
% 89.50/19.98 thf(10236,plain,(! [A:$i] : (((in @ (sk25 @ (setunion @ (setadjoin @ sk50 @ (setadjoin @ sk51 @ emptyset)))) @ sk174) != (in @ A @ emptyset)))),inference(simp,[status(thm)],[10235])).
% 89.50/19.98 thf(10355,plain,(! [A:$i] : (((sk25 @ (setunion @ (setadjoin @ sk50 @ (setadjoin @ sk51 @ emptyset)))) != A) | (sk174 != emptyset))),inference(simp,[status(thm)],[10236])).
% 89.50/19.98 thf(10403,plain,((sk174 != emptyset)),inference(simp,[status(thm)],[10355])).
% 89.50/19.98 thf(10418,plain,(! [A:$i] : ((in @ (sk25 @ A) @ A) | (emptyset != emptyset) | (A != sk174))),inference(paramod_ordered,[status(thm)],[256,10403])).
% 89.50/19.98 thf(10419,plain,(! [A:$i] : ((in @ (sk25 @ A) @ A) | (A != sk174))),inference(simp,[status(thm)],[10418])).
% 89.50/19.98 thf(10420,plain,((in @ (sk25 @ sk174) @ sk174)),inference(pattern_uni,[status(thm)],[10419:[bind(A, $thf(sk174))]])).
% 89.50/19.98 thf(11714,plain,(! [B:$i,A:$i] : (~ (($true)) | (in @ B @ (powerset @ (setunion @ A))) | ((in @ (sk25 @ sk174) @ sk174) != (in @ B @ A)))),inference(paramod_ordered,[status(thm)],[10420,214])).
% 89.50/19.98 thf(11715,plain,(! [B:$i,A:$i] : ((in @ B @ (powerset @ (setunion @ A))) | ((in @ (sk25 @ sk174) @ sk174) != (in @ B @ A)))),inference(simp,[status(thm)],[11714])).
% 89.50/19.98 thf(11716,plain,((in @ (sk25 @ sk174) @ (powerset @ (setunion @ sk174)))),inference(pattern_uni,[status(thm)],[11715:[bind(A, $thf(sk174)),bind(B, $thf(sk25 @ sk174))]])).
% 89.50/19.98 thf(12994,plain,(! [A:$i] : (~ (($true)) | ((in @ (sk25 @ sk174) @ (powerset @ (setunion @ sk174))) != (in @ A @ emptyset)))),inference(paramod_ordered,[status(thm)],[11716,202])).
% 89.50/19.98 thf(12995,plain,(! [A:$i] : (((in @ (sk25 @ sk174) @ (powerset @ (setunion @ sk174))) != (in @ A @ emptyset)))),inference(simp,[status(thm)],[12994])).
% 89.50/19.98 thf(13095,plain,(! [A:$i] : (((sk25 @ sk174) != A) | ((powerset @ (setunion @ sk174)) != emptyset))),inference(simp,[status(thm)],[12995])).
% 89.50/19.98 thf(13127,plain,(((powerset @ (setunion @ sk174)) != emptyset)),inference(simp,[status(thm)],[13095])).
% 89.50/19.98 thf(115,plain,(! [B:$i,A:$o] : ((~ (in @ B @ (prop2set @ A))) | A)),inference(cnfConj,[status(thm)],[5])).
% 89.50/19.98 thf(187,plain,(! [B:$i,A:$o] : ((~ (in @ B @ (prop2set @ A))) | A)),inference(simp,[status(thm)],[115])).
% 89.50/19.98 thf(1480,plain,(! [C:$i,B:$o,A:$i] : ((A = emptyset) | ~ (($true)) | B | ((in @ (sk25 @ A) @ A) != (in @ C @ (prop2set @ B))))),inference(paramod_ordered,[status(thm)],[256,187])).
% 89.50/19.98 thf(1481,plain,(! [C:$i,B:$o,A:$i] : ((A = emptyset) | B | ((in @ (sk25 @ A) @ A) != (in @ C @ (prop2set @ B))))),inference(simp,[status(thm)],[1480])).
% 89.50/19.98 thf(1482,plain,(! [A:$o] : (((prop2set @ A) = emptyset) | A)),inference(pattern_uni,[status(thm)],[1481:[bind(A, $thf(prop2set @ E)),bind(B, $thf(E)),bind(C, $thf(sk25 @ (prop2set @ E)))]])).
% 89.50/19.98 thf(1529,plain,(! [A:$o] : (((prop2set @ A) = emptyset) | A)),inference(simp,[status(thm)],[1482])).
% 89.50/19.98 thf(11838,plain,(! [B:$i,A:$i] : (~ (($true)) | (in @ B @ (powerset @ (setunion @ A))) | ((in @ sk52 @ sk200) != (in @ B @ A)))),inference(paramod_ordered,[status(thm)],[6948,214])).
% 89.50/19.98 thf(11839,plain,(! [B:$i,A:$i] : ((in @ B @ (powerset @ (setunion @ A))) | ((in @ sk52 @ sk200) != (in @ B @ A)))),inference(simp,[status(thm)],[11838])).
% 89.50/19.98 thf(11840,plain,((in @ sk52 @ (powerset @ (setunion @ sk200)))),inference(pattern_uni,[status(thm)],[11839:[bind(A, $thf(sk200)),bind(B, $thf(sk52))]])).
% 89.50/19.98 thf(12209,plain,(! [A:$i] : (~ (($true)) | ((in @ sk52 @ (powerset @ (setunion @ sk200))) != (in @ A @ emptyset)))),inference(paramod_ordered,[status(thm)],[11840,202])).
% 89.50/19.98 thf(12210,plain,(! [A:$i] : (((in @ sk52 @ (powerset @ (setunion @ sk200))) != (in @ A @ emptyset)))),inference(simp,[status(thm)],[12209])).
% 89.50/19.98 thf(12315,plain,(! [A:$i] : ((sk52 != A) | ((powerset @ (setunion @ sk200)) != emptyset))),inference(simp,[status(thm)],[12210])).
% 89.50/19.98 thf(12351,plain,(((powerset @ (setunion @ sk200)) != emptyset)),inference(simp,[status(thm)],[12315])).
% 89.50/19.98 thf(64,plain,((in @ emptyset @ omega)),inference(cnfConj,[status(thm)],[5])).
% 89.50/19.98 thf(1489,plain,(! [B:$i,A:$o] : (~ (($true)) | A | ((in @ emptyset @ omega) != (in @ B @ (prop2set @ A))))),inference(paramod_ordered,[status(thm)],[64,187])).
% 89.50/19.98 thf(1490,plain,(! [B:$i,A:$o] : (A | ((in @ emptyset @ omega) != (in @ B @ (prop2set @ A))))),inference(simp,[status(thm)],[1489])).
% 89.50/19.98 thf(1523,plain,(! [B:$i,A:$o] : (A | (emptyset != B) | ((prop2set @ A) != omega))),inference(simp,[status(thm)],[1490])).
% 89.50/19.98 thf(1550,plain,(! [A:$o] : (A | ((prop2set @ A) != omega))),inference(simp,[status(thm)],[1523])).
% 89.50/19.98 thf(3345,plain,(! [A:$o] : ((~ (A)) | ((prop2set @ (~ (A))) != omega))),inference(prim_subst,[status(thm)],[1550:[bind(A, $thf(~ (B)))]])).
% 89.50/19.98 thf(3361,plain,(! [A:$o] : (~ (A) | ((prop2set @ (~ (A))) != omega))),inference(cnf,[status(esa)],[3345])).
% 89.50/19.98 thf(3362,plain,(! [A:$o] : (~ (A) | ((prop2set @ (~ (A))) != omega))),inference(simp,[status(thm)],[3361])).
% 89.50/19.98 thf(3729,plain,(! [A:$i] : ((~ (set2prop @ A)) | ((prop2set @ (~ (set2prop @ A))) != omega))),inference(prim_subst,[status(thm)],[3362:[bind(A, $thf(set2prop @ B))]])).
% 89.50/19.98 thf(3750,plain,(! [A:$i] : ((~ (set2prop @ A)) | ((prop2set @ (~ (set2prop @ A))) != omega))),inference(simp,[status(thm)],[3729])).
% 89.50/19.98 thf(4537,plain,(! [A:$i] : (((prop2set @ ($true)) != emptyset) | ~ (($true)) | ((prop2set @ (~ (set2prop @ A))) != omega) | ((set2prop @ emptyset) != (set2prop @ A)))),inference(paramod_ordered,[status(thm)],[3285,3750])).
% 89.50/19.98 thf(4538,plain,(! [A:$i] : (((prop2set @ ($true)) != emptyset) | ((prop2set @ (~ (set2prop @ A))) != omega) | ((set2prop @ emptyset) != (set2prop @ A)))),inference(simp,[status(thm)],[4537])).
% 89.50/19.98 thf(4539,plain,(((prop2set @ ($true)) != emptyset) | ((prop2set @ (~ (set2prop @ emptyset))) != omega)),inference(pattern_uni,[status(thm)],[4538:[bind(A, $thf(emptyset))]])).
% 89.50/19.98 thf(88,plain,(! [C:$i,B:$i,A:$i] : ((~ (in @ C @ A)) | (in @ C @ B) | (~ (subset @ A @ B)))),inference(cnfConj,[status(thm)],[5])).
% 89.50/19.98 thf(184,plain,(! [C:$i,B:$i,A:$i] : ((~ (in @ C @ A)) | (in @ C @ B) | (~ (subset @ A @ B)))),inference(simp,[status(thm)],[88])).
% 89.50/19.98 thf(434,plain,(! [A:$i] : (~ (($true)) | ((in @ emptyset @ omega) != (in @ A @ emptyset)))),inference(paramod_ordered,[status(thm)],[64,202])).
% 89.50/19.98 thf(435,plain,(! [A:$i] : (((in @ emptyset @ omega) != (in @ A @ emptyset)))),inference(simp,[status(thm)],[434])).
% 89.50/19.98 thf(437,plain,(! [A:$i] : ((emptyset != A) | (omega != emptyset))),inference(simp,[status(thm)],[435])).
% 89.50/19.98 thf(439,plain,((omega != emptyset)),inference(simp,[status(thm)],[437])).
% 89.50/19.98 thf(893,plain,(! [A:$i] : ((in @ (sk25 @ A) @ A) | (emptyset != emptyset) | (A != omega))),inference(paramod_ordered,[status(thm)],[256,439])).
% 89.50/19.98 thf(894,plain,(! [A:$i] : ((in @ (sk25 @ A) @ A) | (A != omega))),inference(simp,[status(thm)],[893])).
% 89.50/19.98 thf(895,plain,((in @ (sk25 @ omega) @ omega)),inference(pattern_uni,[status(thm)],[894:[bind(A, $thf(omega))]])).
% 89.50/19.98 thf(1168,plain,(~ (($true)) | ((in @ (sk25 @ omega) @ omega) != (in @ sk52 @ sk50))),inference(paramod_ordered,[status(thm)],[895,449])).
% 89.50/19.98 thf(1169,plain,(((in @ (sk25 @ omega) @ omega) != (in @ sk52 @ sk50))),inference(simp,[status(thm)],[1168])).
% 89.50/19.98 thf(1191,plain,(((sk25 @ omega) != sk52) | (sk50 != omega)),inference(simp,[status(thm)],[1169])).
% 89.50/19.98 thf(72,plain,(! [B:$i,A:($i > $o)] : ((~ (A @ B)) | (~ ((sk32 @ (A)) = (sk33 @ (A)))) | (A @ (sk34 @ (A))))),inference(cnfConj,[status(thm)],[5])).
% 89.50/19.98 thf(174,plain,(! [A:$i] : ((~ (A = A)) | (~ ((sk32 @ ((=) @ $i @ A)) = (sk33 @ ((=) @ $i @ A)))) | (A = (sk34 @ ((=) @ $i @ A))))),inference(replace_leibeq,[status(thm)],[72:[bind(A, $thf((=) @ $i @ B))]])).
% 89.50/19.98 thf(195,plain,(! [A:$i] : ((A != A) | ((sk33 @ ((=) @ $i @ A)) != (sk32 @ ((=) @ $i @ A))) | (A = (sk34 @ ((=) @ $i @ A))))),inference(lifteq,[status(thm)],[174])).
% 89.50/19.98 thf(196,plain,(! [A:$i] : (((sk33 @ ((=) @ $i @ A)) != (sk32 @ ((=) @ $i @ A))) | (A = (sk34 @ ((=) @ $i @ A))))),inference(simp,[status(thm)],[195])).
% 89.50/19.98 thf(12026,plain,(~ (($true)) | ((in @ sk52 @ (powerset @ (setunion @ sk203))) != (in @ sk52 @ sk51))),inference(paramod_ordered,[status(thm)],[11837,441])).
% 89.50/19.98 thf(12027,plain,(((in @ sk52 @ (powerset @ (setunion @ sk203))) != (in @ sk52 @ sk51))),inference(simp,[status(thm)],[12026])).
% 89.50/19.98 thf(12080,plain,((sk52 != sk52) | ((powerset @ (setunion @ sk203)) != sk51)),inference(simp,[status(thm)],[12027])).
% 89.50/19.98 thf(12122,plain,(((powerset @ (setunion @ sk203)) != sk51)),inference(simp,[status(thm)],[12080])).
% 89.50/19.98 thf(93,plain,(! [A:$i] : ((in @ emptyset @ (powerset @ A)))),inference(cnfConj,[status(thm)],[5])).
% 89.50/19.98 thf(212,plain,(! [A:$i] : ((in @ emptyset @ (powerset @ A)))),inference(simp,[status(thm)],[93])).
% 89.50/19.98 thf(475,plain,(! [B:$i,A:$i] : (~ (($true)) | ((in @ emptyset @ (powerset @ A)) != (in @ B @ emptyset)))),inference(paramod_ordered,[status(thm)],[212,202])).
% 89.50/19.98 thf(476,plain,(! [B:$i,A:$i] : (((in @ emptyset @ (powerset @ A)) != (in @ B @ emptyset)))),inference(simp,[status(thm)],[475])).
% 89.50/19.98 thf(479,plain,(! [B:$i,A:$i] : ((emptyset != B) | ((powerset @ A) != emptyset))),inference(simp,[status(thm)],[476])).
% 89.50/19.98 thf(480,plain,(! [A:$i] : (((powerset @ A) != emptyset))),inference(simp,[status(thm)],[479])).
% 89.50/19.98 thf(967,plain,(! [B:$i,A:$i] : ((in @ (sk25 @ A) @ A) | (emptyset != emptyset) | (A != (powerset @ B)))),inference(paramod_ordered,[status(thm)],[256,480])).
% 89.50/19.98 thf(968,plain,(! [B:$i,A:$i] : ((in @ (sk25 @ A) @ A) | (A != (powerset @ B)))),inference(simp,[status(thm)],[967])).
% 89.50/19.98 thf(969,plain,(! [A:$i] : ((in @ (sk25 @ (powerset @ A)) @ (powerset @ A)))),inference(pattern_uni,[status(thm)],[968:[bind(A, $thf(powerset @ C)),bind(B, $thf(C))]])).
% 89.50/19.98 thf(1160,plain,(! [A:$i] : ((in @ (sk25 @ (powerset @ A)) @ (powerset @ A)))),inference(simp,[status(thm)],[969])).
% 89.50/19.98 thf(1285,plain,(! [A:$i] : (~ (($true)) | ((in @ (sk25 @ (powerset @ A)) @ (powerset @ A)) != (in @ sk52 @ sk51)))),inference(paramod_ordered,[status(thm)],[1160,441])).
% 89.50/19.98 thf(1286,plain,(! [A:$i] : (((in @ (sk25 @ (powerset @ A)) @ (powerset @ A)) != (in @ sk52 @ sk51)))),inference(simp,[status(thm)],[1285])).
% 89.50/19.98 thf(1298,plain,(! [A:$i] : (((sk25 @ (powerset @ A)) != sk52) | ((powerset @ A) != sk51))),inference(simp,[status(thm)],[1286])).
% 89.50/19.98 thf(7059,plain,(! [A:$i] : ((in @ (sk25 @ A) @ A) | (in @ emptyset @ sk200) | (A != sk52))),inference(paramod_ordered,[status(thm)],[256,6948])).
% 89.50/19.98 thf(7060,plain,((in @ (sk25 @ sk52) @ sk52) | (in @ emptyset @ sk200)),inference(pattern_uni,[status(thm)],[7059:[bind(A, $thf(sk52))]])).
% 89.50/19.98 thf(42,plain,(! [D:($i > $o),C:($i > $o),B:$i,A:$i] : ((~ (A = B)) | (in @ (sk46 @ (D) @ (C) @ B @ A) @ A) | ((dsetconstr @ A @ (C)) = (dsetconstr @ B @ (D))))),inference(cnfConj,[status(thm)],[5])).
% 89.50/19.98 thf(197,plain,(! [D:($i > $o),C:($i > $o),B:$i,A:$i] : ((A != B) | ((dsetconstr @ A @ (C)) = (dsetconstr @ B @ (D))) | (in @ (sk46 @ (D) @ (C) @ B @ A) @ A))),inference(lifteq,[status(thm)],[42])).
% 89.50/19.98 thf(198,plain,(! [C:($i > $o),B:($i > $o),A:$i] : (((dsetconstr @ A @ (B)) = (dsetconstr @ A @ (C))) | (in @ (sk46 @ (C) @ (B) @ A @ A) @ A))),inference(simp,[status(thm)],[197])).
% 89.50/19.98 thf(3783,plain,(! [D:$i,C:($i > $o),B:($i > $o),A:$i] : (((dsetconstr @ A @ (B)) = (dsetconstr @ A @ (C))) | ~ (($true)) | ((in @ (sk46 @ (C) @ (B) @ A @ A) @ A) != (in @ D @ emptyset)))),inference(paramod_ordered,[status(thm)],[198,202])).
% 89.50/19.98 thf(3784,plain,(! [D:$i,C:($i > $o),B:($i > $o),A:$i] : (((dsetconstr @ A @ (B)) = (dsetconstr @ A @ (C))) | ((in @ (sk46 @ (C) @ (B) @ A @ A) @ A) != (in @ D @ emptyset)))),inference(simp,[status(thm)],[3783])).
% 89.50/19.98 thf(3785,plain,(! [B:($i > $o),A:($i > $o)] : (((dsetconstr @ emptyset @ (B)) = (dsetconstr @ emptyset @ (A))))),inference(pattern_uni,[status(thm)],[3784:[bind(A, $thf(emptyset)),bind(B, $thf(F)),bind(C, $thf(E)),bind(D, $thf(sk46 @ (E) @ (F) @ emptyset @ emptyset))]])).
% 89.50/19.98 thf(3836,plain,(! [B:($i > $o),A:($i > $o)] : (((dsetconstr @ emptyset @ (B)) = (dsetconstr @ emptyset @ (A))))),inference(simp,[status(thm)],[3785])).
% 89.50/19.98 thf(91,plain,(! [A:$i] : (((dsetconstr @ A @ (^ [B:$i]: (($true)))) = A))),inference(cnfConj,[status(thm)],[5])).
% 89.50/19.98 thf(330,plain,(! [A:$i] : (((dsetconstr @ A @ (^ [B:$i]: (($true)))) = A))),inference(lifteq,[status(thm)],[91])).
% 89.50/19.98 thf(331,plain,(! [A:$i] : (((dsetconstr @ A @ (^ [B:$i]: (($true)))) = A))),inference(simp,[status(thm)],[330])).
% 89.50/19.98 thf(3918,plain,(! [C:$i,B:($i > $o),A:($i > $o)] : (((dsetconstr @ emptyset @ (A)) = C) | ((dsetconstr @ emptyset @ (B)) != (dsetconstr @ C @ (^ [D:$i]: (($true))))))),inference(paramod_ordered,[status(thm)],[3836,331])).
% 89.50/19.98 thf(3919,plain,(! [A:($i > $o)] : (((dsetconstr @ emptyset @ (A)) = emptyset))),inference(pattern_uni,[status(thm)],[3918:[bind(A, $thf(A)),bind(B, $thf(^ [D:$i]: (($true)))),bind(C, $thf(emptyset))]])).
% 89.50/19.98 thf(444,plain,(~ (($true)) | ((in @ sk52 @ sk51) != (in @ emptyset @ omega))),inference(paramod_ordered,[status(thm)],[64,441])).
% 89.50/19.98 thf(445,plain,(((in @ sk52 @ sk51) != (in @ emptyset @ omega))),inference(simp,[status(thm)],[444])).
% 89.50/19.98 thf(447,plain,((sk52 != emptyset) | (sk51 != omega)),inference(simp,[status(thm)],[445])).
% 89.50/19.98 thf(1084,plain,(! [A:$i] : ((in @ (sk25 @ A) @ A) | (emptyset != emptyset) | (sk51 != omega) | (A != sk52))),inference(paramod_ordered,[status(thm)],[256,447])).
% 89.50/19.98 thf(1085,plain,(! [A:$i] : ((in @ (sk25 @ A) @ A) | (sk51 != omega) | (A != sk52))),inference(simp,[status(thm)],[1084])).
% 89.50/19.98 thf(1086,plain,((in @ (sk25 @ sk52) @ sk52) | (sk51 != omega)),inference(pattern_uni,[status(thm)],[1085:[bind(A, $thf(sk52))]])).
% 89.50/19.98 thf(2830,plain,((sk51 != omega) | ~ (($true)) | ((in @ (sk25 @ sk52) @ sk52) != (in @ sk52 @ sk51))),inference(paramod_ordered,[status(thm)],[1086,441])).
% 89.50/19.98 thf(2831,plain,((sk51 != omega) | ((in @ (sk25 @ sk52) @ sk52) != (in @ sk52 @ sk51))),inference(simp,[status(thm)],[2830])).
% 89.50/19.98 thf(2852,plain,((sk51 != omega) | ((sk25 @ sk52) != sk52) | (sk52 != sk51)),inference(simp,[status(thm)],[2831])).
% 89.50/19.98 thf(11772,plain,(! [B:$i,A:$i] : (~ (($true)) | (in @ B @ (powerset @ (setunion @ A))) | ((in @ (sk25 @ sk177) @ sk177) != (in @ B @ A)))),inference(paramod_ordered,[status(thm)],[10759,214])).
% 89.50/19.98 thf(11773,plain,(! [B:$i,A:$i] : ((in @ B @ (powerset @ (setunion @ A))) | ((in @ (sk25 @ sk177) @ sk177) != (in @ B @ A)))),inference(simp,[status(thm)],[11772])).
% 89.50/19.98 thf(11774,plain,((in @ (sk25 @ sk177) @ (powerset @ (setunion @ sk177)))),inference(pattern_uni,[status(thm)],[11773:[bind(A, $thf(sk177)),bind(B, $thf(sk25 @ sk177))]])).
% 89.50/19.98 thf(13623,plain,(! [A:$i] : (~ (($true)) | ((in @ (sk25 @ sk177) @ (powerset @ (setunion @ sk177))) != (in @ A @ emptyset)))),inference(paramod_ordered,[status(thm)],[11774,202])).
% 89.50/19.98 thf(13624,plain,(! [A:$i] : (((in @ (sk25 @ sk177) @ (powerset @ (setunion @ sk177))) != (in @ A @ emptyset)))),inference(simp,[status(thm)],[13623])).
% 89.50/19.98 thf(13748,plain,(! [A:$i] : (((sk25 @ sk177) != A) | ((powerset @ (setunion @ sk177)) != emptyset))),inference(simp,[status(thm)],[13624])).
% 89.50/19.98 thf(13788,plain,(((powerset @ (setunion @ sk177)) != emptyset)),inference(simp,[status(thm)],[13748])).
% 89.50/19.98 thf(7188,plain,(~ (($true)) | ((in @ sk52 @ sk203) != (in @ sk52 @ sk50))),inference(paramod_ordered,[status(thm)],[6961,449])).
% 89.50/19.98 thf(7189,plain,(((in @ sk52 @ sk203) != (in @ sk52 @ sk50))),inference(simp,[status(thm)],[7188])).
% 89.50/19.98 thf(7242,plain,((sk52 != sk52) | (sk203 != sk50)),inference(simp,[status(thm)],[7189])).
% 89.50/19.98 thf(7268,plain,((sk203 != sk50)),inference(simp,[status(thm)],[7242])).
% 89.50/19.98 thf(12282,plain,(! [B:$i,A:$i] : (~ (($true)) | (in @ B @ (powerset @ (setunion @ A))) | ((in @ sk52 @ (powerset @ (setunion @ sk200))) != (in @ B @ A)))),inference(paramod_ordered,[status(thm)],[11840,214])).
% 89.50/19.98 thf(12283,plain,(! [B:$i,A:$i] : ((in @ B @ (powerset @ (setunion @ A))) | ((in @ sk52 @ (powerset @ (setunion @ sk200))) != (in @ B @ A)))),inference(simp,[status(thm)],[12282])).
% 89.50/19.98 thf(12284,plain,((in @ sk52 @ (powerset @ (setunion @ (powerset @ (setunion @ sk200)))))),inference(pattern_uni,[status(thm)],[12283:[bind(A, $thf(powerset @ (setunion @ sk200))),bind(B, $thf(sk52))]])).
% 89.50/19.98 thf(16252,plain,(~ (($true)) | ((in @ sk52 @ (powerset @ (setunion @ (powerset @ (setunion @ sk200))))) != (in @ sk52 @ sk50))),inference(paramod_ordered,[status(thm)],[12284,449])).
% 89.50/19.98 thf(16253,plain,(((in @ sk52 @ (powerset @ (setunion @ (powerset @ (setunion @ sk200))))) != (in @ sk52 @ sk50))),inference(simp,[status(thm)],[16252])).
% 89.50/19.98 thf(16381,plain,((sk52 != sk52) | ((powerset @ (setunion @ (powerset @ (setunion @ sk200)))) != sk50)),inference(simp,[status(thm)],[16253])).
% 89.50/19.98 thf(16448,plain,(((powerset @ (setunion @ (powerset @ (setunion @ sk200)))) != sk50)),inference(simp,[status(thm)],[16381])).
% 89.50/19.98 thf(11763,plain,(! [B:$i,A:$i] : (~ (($true)) | (in @ B @ (powerset @ (setunion @ A))) | ((in @ (sk25 @ omega) @ omega) != (in @ B @ A)))),inference(paramod_ordered,[status(thm)],[895,214])).
% 89.50/19.98 thf(11764,plain,(! [B:$i,A:$i] : ((in @ B @ (powerset @ (setunion @ A))) | ((in @ (sk25 @ omega) @ omega) != (in @ B @ A)))),inference(simp,[status(thm)],[11763])).
% 89.50/19.98 thf(11765,plain,((in @ (sk25 @ omega) @ (powerset @ (setunion @ omega)))),inference(pattern_uni,[status(thm)],[11764:[bind(A, $thf(omega)),bind(B, $thf(sk25 @ omega))]])).
% 89.50/19.98 thf(13194,plain,(~ (($true)) | ((in @ (sk25 @ omega) @ (powerset @ (setunion @ omega))) != (in @ sk52 @ sk50))),inference(paramod_ordered,[status(thm)],[11765,449])).
% 89.50/19.98 thf(13195,plain,(((in @ (sk25 @ omega) @ (powerset @ (setunion @ omega))) != (in @ sk52 @ sk50))),inference(simp,[status(thm)],[13194])).
% 89.50/19.98 thf(13290,plain,(((sk25 @ omega) != sk52) | ((powerset @ (setunion @ omega)) != sk50)),inference(simp,[status(thm)],[13195])).
% 89.50/19.98 thf(106,plain,(! [D:$i,C:$i,B:$i,A:($i > ($i > $o))] : ((~ (A @ (sk3 @ B @ (A)) @ C)) | (~ (C = (sk4 @ C @ B @ (A)))) | ((in @ D @ (sk5 @ B @ (A))) = (? [E:$i]: ((in @ E @ B) & (A @ E @ D)))))),inference(cnfConj,[status(thm)],[5])).
% 89.50/19.98 thf(220,plain,(! [D:$i,C:$i,B:$i,A:($i > ($i > $o))] : (((sk4 @ C @ B @ (A)) != C) | ((in @ D @ (sk5 @ B @ (A))) = (? [E:$i]: ((in @ E @ B) & (A @ E @ D)))) | (~ (A @ (sk3 @ B @ (A)) @ C)))),inference(lifteq,[status(thm)],[106])).
% 89.50/19.98 thf(221,plain,(! [D:$i,C:$i,B:$i,A:($i > ($i > $o))] : (((sk4 @ C @ B @ (A)) != C) | ((in @ D @ (sk5 @ B @ (A))) = (? [E:$i]: ((in @ E @ B) & (A @ E @ D)))) | (~ (A @ (sk3 @ B @ (A)) @ C)))),inference(simp,[status(thm)],[220])).
% 89.50/19.98 thf(125,plain,(! [B:$i,A:$i] : ((~ (in @ (sk48 @ B @ A) @ B)) | (subset @ A @ B))),inference(cnfConj,[status(thm)],[5])).
% 89.50/19.98 thf(206,plain,(! [B:$i,A:$i] : ((~ (in @ (sk48 @ B @ A) @ B)) | (subset @ A @ B))),inference(simp,[status(thm)],[125])).
% 89.50/19.98 thf(37,plain,(! [C:$i,B:$i,A:($i > ($i > $o))] : ((in @ (sk3 @ B @ (A)) @ B) | ((in @ C @ (sk5 @ B @ (A))) = (? [D:$i]: ((in @ D @ B) & (A @ D @ C)))))),inference(cnfConj,[status(thm)],[5])).
% 89.50/19.98 thf(200,plain,(! [C:$i,B:$i,A:($i > ($i > $o))] : (((in @ C @ (sk5 @ B @ (A))) = (? [D:$i]: ((in @ D @ B) & (A @ D @ C)))) | (in @ (sk3 @ B @ (A)) @ B))),inference(lifteq,[status(thm)],[37])).
% 89.50/19.98 thf(201,plain,(! [C:$i,B:$i,A:($i > ($i > $o))] : (((in @ C @ (sk5 @ B @ (A))) = (? [D:$i]: ((in @ D @ B) & (A @ D @ C)))) | (in @ (sk3 @ B @ (A)) @ B))),inference(simp,[status(thm)],[200])).
% 89.50/19.98 thf(11965,plain,(! [A:$i] : (~ (($true)) | ((in @ sk52 @ (powerset @ (setunion @ sk203))) != (in @ A @ emptyset)))),inference(paramod_ordered,[status(thm)],[11837,202])).
% 89.50/19.98 thf(11966,plain,(! [A:$i] : (((in @ sk52 @ (powerset @ (setunion @ sk203))) != (in @ A @ emptyset)))),inference(simp,[status(thm)],[11965])).
% 89.50/19.98 thf(12067,plain,(! [A:$i] : ((sk52 != A) | ((powerset @ (setunion @ sk203)) != emptyset))),inference(simp,[status(thm)],[11966])).
% 89.50/19.98 thf(12100,plain,(((powerset @ (setunion @ sk203)) != emptyset)),inference(simp,[status(thm)],[12067])).
% 89.50/19.98 thf(12207,plain,(~ (($true)) | ((in @ sk52 @ (powerset @ (setunion @ sk200))) != (in @ sk52 @ sk50))),inference(paramod_ordered,[status(thm)],[11840,449])).
% 89.50/19.98 thf(12208,plain,(((in @ sk52 @ (powerset @ (setunion @ sk200))) != (in @ sk52 @ sk50))),inference(simp,[status(thm)],[12207])).
% 89.50/19.98 thf(12325,plain,((sk52 != sk52) | ((powerset @ (setunion @ sk200)) != sk50)),inference(simp,[status(thm)],[12208])).
% 89.50/19.98 thf(12365,plain,(((powerset @ (setunion @ sk200)) != sk50)),inference(simp,[status(thm)],[12325])).
% 89.50/19.98 thf(458,plain,(~ (($true)) | ((in @ sk52 @ (setunion @ (setadjoin @ sk50 @ (setadjoin @ sk51 @ emptyset)))) != (in @ sk52 @ sk50))),inference(paramod_ordered,[status(thm)],[34,449])).
% 89.50/19.98 thf(459,plain,(((in @ sk52 @ (setunion @ (setadjoin @ sk50 @ (setadjoin @ sk51 @ emptyset)))) != (in @ sk52 @ sk50))),inference(simp,[status(thm)],[458])).
% 89.50/19.98 thf(463,plain,((sk52 != sk52) | ((setunion @ (setadjoin @ sk50 @ (setadjoin @ sk51 @ emptyset))) != sk50)),inference(simp,[status(thm)],[459])).
% 89.50/19.98 thf(467,plain,(((setunion @ (setadjoin @ sk50 @ (setadjoin @ sk51 @ emptyset))) != sk50)),inference(simp,[status(thm)],[463])).
% 89.50/19.98 thf(2627,plain,(! [C:$i,B:$i,A:$i] : (~ (($true)) | ((in @ B @ (powerset @ (setadjoin @ A @ B))) != (in @ C @ emptyset)))),inference(paramod_ordered,[status(thm)],[2613,202])).
% 89.50/19.98 thf(2628,plain,(! [C:$i,B:$i,A:$i] : (((in @ B @ (powerset @ (setadjoin @ A @ B))) != (in @ C @ emptyset)))),inference(simp,[status(thm)],[2627])).
% 89.50/19.98 thf(2651,plain,(! [C:$i,B:$i,A:$i] : ((B != C) | ((powerset @ (setadjoin @ A @ B)) != emptyset))),inference(simp,[status(thm)],[2628])).
% 89.50/19.98 thf(2670,plain,(! [B:$i,A:$i] : (((powerset @ (setadjoin @ A @ B)) != emptyset))),inference(simp,[status(thm)],[2651])).
% 89.50/19.98 thf(616,plain,(! [A:$i] : (~ (($true)) | ((in @ A @ (powerset @ A)) != (in @ sk52 @ sk51)))),inference(paramod_ordered,[status(thm)],[199,441])).
% 89.50/19.98 thf(617,plain,(! [A:$i] : (((in @ A @ (powerset @ A)) != (in @ sk52 @ sk51)))),inference(simp,[status(thm)],[616])).
% 89.50/19.98 thf(624,plain,(! [A:$i] : ((A != sk52) | ((powerset @ A) != sk51))),inference(simp,[status(thm)],[617])).
% 89.50/19.98 thf(625,plain,(((powerset @ sk52) != sk51)),inference(simp,[status(thm)],[624])).
% 89.50/19.98 thf(13196,plain,(! [A:$i] : (~ (($true)) | ((in @ (sk25 @ omega) @ (powerset @ (setunion @ omega))) != (in @ A @ emptyset)))),inference(paramod_ordered,[status(thm)],[11765,202])).
% 89.50/19.98 thf(13197,plain,(! [A:$i] : (((in @ (sk25 @ omega) @ (powerset @ (setunion @ omega))) != (in @ A @ emptyset)))),inference(simp,[status(thm)],[13196])).
% 89.50/19.98 thf(13308,plain,(! [A:$i] : (((sk25 @ omega) != A) | ((powerset @ (setunion @ omega)) != emptyset))),inference(simp,[status(thm)],[13197])).
% 89.50/19.98 thf(13362,plain,(((powerset @ (setunion @ omega)) != emptyset)),inference(simp,[status(thm)],[13308])).
% 89.50/19.98 thf(15927,plain,(! [A:$i] : (~ (($true)) | ((in @ sk52 @ (powerset @ (setunion @ (powerset @ (setunion @ sk203))))) != (in @ A @ emptyset)))),inference(paramod_ordered,[status(thm)],[12040,202])).
% 89.50/19.98 thf(15928,plain,(! [A:$i] : (((in @ sk52 @ (powerset @ (setunion @ (powerset @ (setunion @ sk203))))) != (in @ A @ emptyset)))),inference(simp,[status(thm)],[15927])).
% 89.50/19.98 thf(16059,plain,(! [A:$i] : ((sk52 != A) | ((powerset @ (setunion @ (powerset @ (setunion @ sk203)))) != emptyset))),inference(simp,[status(thm)],[15928])).
% 89.50/19.98 thf(16108,plain,(((powerset @ (setunion @ (powerset @ (setunion @ sk203)))) != emptyset)),inference(simp,[status(thm)],[16059])).
% 89.50/19.98 thf(84,plain,(! [D:$i,C:$i,B:($i > $o),A:($i > $o)] : ((~ (sk41 @ A @ B)) | (~ (A @ C)) | (A @ (sk44 @ C @ (B) @ (A))) | (~ (B @ D)) | (B @ (sk45 @ D @ (B) @ (A))) | ((descr @ (A)) = (descr @ (B))))),inference(cnfConj,[status(thm)],[5])).
% 89.50/19.98 thf(224,plain,(! [D:$i,C:$i,B:($i > $o),A:($i > $o)] : (((descr @ (A)) = (descr @ (B))) | (~ (sk41 @ A @ B)) | (~ (A @ C)) | (A @ (sk44 @ C @ (B) @ (A))) | (~ (B @ D)) | (B @ (sk45 @ D @ (B) @ (A))))),inference(lifteq,[status(thm)],[84])).
% 89.50/19.98 thf(225,plain,(! [D:$i,C:$i,B:($i > $o),A:($i > $o)] : (((descr @ (A)) = (descr @ (B))) | (~ (sk41 @ A @ B)) | (~ (A @ C)) | (A @ (sk44 @ C @ (B) @ (A))) | (~ (B @ D)) | (B @ (sk45 @ D @ (B) @ (A))))),inference(simp,[status(thm)],[224])).
% 89.50/19.98 thf(15925,plain,(~ (($true)) | ((in @ sk52 @ (powerset @ (setunion @ (powerset @ (setunion @ sk203))))) != (in @ sk52 @ sk50))),inference(paramod_ordered,[status(thm)],[12040,449])).
% 89.50/19.98 thf(15926,plain,(((in @ sk52 @ (powerset @ (setunion @ (powerset @ (setunion @ sk203))))) != (in @ sk52 @ sk50))),inference(simp,[status(thm)],[15925])).
% 89.50/19.98 thf(16039,plain,((sk52 != sk52) | ((powerset @ (setunion @ (powerset @ (setunion @ sk203)))) != sk50)),inference(simp,[status(thm)],[15926])).
% 89.50/19.98 thf(16083,plain,(((powerset @ (setunion @ (powerset @ (setunion @ sk203)))) != sk50)),inference(simp,[status(thm)],[16039])).
% 89.50/19.98 thf(452,plain,(~ (($true)) | ((in @ sk52 @ sk50) != (in @ emptyset @ omega))),inference(paramod_ordered,[status(thm)],[64,449])).
% 89.50/19.98 thf(453,plain,(((in @ sk52 @ sk50) != (in @ emptyset @ omega))),inference(simp,[status(thm)],[452])).
% 89.50/19.98 thf(455,plain,((sk52 != emptyset) | (sk50 != omega)),inference(simp,[status(thm)],[453])).
% 89.50/19.98 thf(1036,plain,(! [A:$i] : ((in @ (sk25 @ A) @ A) | (emptyset != emptyset) | (sk50 != omega) | (A != sk52))),inference(paramod_ordered,[status(thm)],[256,455])).
% 89.50/19.98 thf(1037,plain,(! [A:$i] : ((in @ (sk25 @ A) @ A) | (sk50 != omega) | (A != sk52))),inference(simp,[status(thm)],[1036])).
% 89.50/19.98 thf(1038,plain,((in @ (sk25 @ sk52) @ sk52) | (sk50 != omega)),inference(pattern_uni,[status(thm)],[1037:[bind(A, $thf(sk52))]])).
% 89.50/19.98 thf(2542,plain,((sk50 != omega) | ~ (($true)) | ((in @ (sk25 @ sk52) @ sk52) != (in @ sk52 @ sk50))),inference(paramod_ordered,[status(thm)],[1038,449])).
% 89.50/19.98 thf(2543,plain,((sk50 != omega) | ((in @ (sk25 @ sk52) @ sk52) != (in @ sk52 @ sk50))),inference(simp,[status(thm)],[2542])).
% 89.50/19.98 thf(2581,plain,((sk50 != omega) | ((sk25 @ sk52) != sk52) | (sk52 != sk50)),inference(simp,[status(thm)],[2543])).
% 89.50/19.98 thf(58,plain,(! [B:$i,A:$i] : ((in @ B @ (setadjoin @ A @ (setadjoin @ B @ emptyset))))),inference(cnfConj,[status(thm)],[5])).
% 89.50/19.98 thf(400,plain,(! [B:$i,A:$i] : ((in @ B @ (setadjoin @ A @ (setadjoin @ B @ emptyset))))),inference(simp,[status(thm)],[58])).
% 89.50/19.98 thf(3021,plain,(! [B:$i,A:$i] : (~ (($true)) | ((in @ B @ (setadjoin @ A @ (setadjoin @ B @ emptyset))) != (in @ sk52 @ sk50)))),inference(paramod_ordered,[status(thm)],[400,449])).
% 89.50/19.98 thf(3022,plain,(! [B:$i,A:$i] : (((in @ B @ (setadjoin @ A @ (setadjoin @ B @ emptyset))) != (in @ sk52 @ sk50)))),inference(simp,[status(thm)],[3021])).
% 89.50/19.98 thf(3053,plain,(! [B:$i,A:$i] : ((B != sk52) | ((setadjoin @ A @ (setadjoin @ B @ emptyset)) != sk50))),inference(simp,[status(thm)],[3022])).
% 89.50/19.98 thf(3074,plain,(! [A:$i] : (((setadjoin @ A @ (setadjoin @ sk52 @ emptyset)) != sk50))),inference(simp,[status(thm)],[3053])).
% 89.50/19.98 thf(4527,plain,(! [A:$i] : (~ (($true)) | ((prop2set @ (~ (set2prop @ A))) != omega) | ((set2prop @ (prop2set @ ($true))) != (set2prop @ A)))),inference(paramod_ordered,[status(thm)],[1433,3750])).
% 89.50/19.98 thf(4528,plain,(! [A:$i] : (((prop2set @ (~ (set2prop @ A))) != omega) | ((set2prop @ (prop2set @ ($true))) != (set2prop @ A)))),inference(simp,[status(thm)],[4527])).
% 89.50/19.98 thf(4529,plain,(((prop2set @ (~ (set2prop @ (prop2set @ ($true))))) != omega)),inference(pattern_uni,[status(thm)],[4528:[bind(A, $thf(prop2set @ ($true)))]])).
% 89.50/19.98 thf(5316,plain,(((prop2set @ (~ (($true)))) != omega)),inference(rewrite,[status(thm)],[4529,1433])).
% 89.50/19.98 thf(5317,plain,(((prop2set @ ($false)) != omega)),inference(simp,[status(thm)],[5316])).
% 89.50/19.98 thf(48,plain,((in @ emptyset @ (setadjoin @ emptyset @ emptyset))),inference(cnfConj,[status(thm)],[5])).
% 89.50/19.98 thf(432,plain,(! [A:$i] : (~ (($true)) | ((in @ emptyset @ (setadjoin @ emptyset @ emptyset)) != (in @ A @ emptyset)))),inference(paramod_ordered,[status(thm)],[48,202])).
% 89.50/19.98 thf(433,plain,(! [A:$i] : (((in @ emptyset @ (setadjoin @ emptyset @ emptyset)) != (in @ A @ emptyset)))),inference(simp,[status(thm)],[432])).
% 89.50/19.98 thf(436,plain,(! [A:$i] : ((emptyset != A) | ((setadjoin @ emptyset @ emptyset) != emptyset))),inference(simp,[status(thm)],[433])).
% 89.50/19.98 thf(438,plain,(((setadjoin @ emptyset @ emptyset) != emptyset)),inference(simp,[status(thm)],[436])).
% 89.50/19.98 thf(1041,plain,(! [A:$i] : ((in @ (sk25 @ A) @ A) | (emptyset != emptyset) | (A != (setadjoin @ emptyset @ emptyset)))),inference(paramod_ordered,[status(thm)],[256,438])).
% 89.50/19.98 thf(1042,plain,(! [A:$i] : ((in @ (sk25 @ A) @ A) | (A != (setadjoin @ emptyset @ emptyset)))),inference(simp,[status(thm)],[1041])).
% 89.50/19.98 thf(1043,plain,((in @ (sk25 @ (setadjoin @ emptyset @ emptyset)) @ (setadjoin @ emptyset @ emptyset))),inference(pattern_uni,[status(thm)],[1042:[bind(A, $thf(setadjoin @ emptyset @ emptyset))]])).
% 89.50/19.98 thf(1243,plain,(~ (($true)) | ((in @ (sk25 @ (setadjoin @ emptyset @ emptyset)) @ (setadjoin @ emptyset @ emptyset)) != (in @ sk52 @ sk51))),inference(paramod_ordered,[status(thm)],[1043,441])).
% 89.50/19.98 thf(1244,plain,(((in @ (sk25 @ (setadjoin @ emptyset @ emptyset)) @ (setadjoin @ emptyset @ emptyset)) != (in @ sk52 @ sk51))),inference(simp,[status(thm)],[1243])).
% 89.50/19.98 thf(1263,plain,(((sk25 @ (setadjoin @ emptyset @ emptyset)) != sk52) | ((setadjoin @ emptyset @ emptyset) != sk51)),inference(simp,[status(thm)],[1244])).
% 89.50/19.98 thf(763,plain,(! [B:$i,A:$i] : (~ (($true)) | ((in @ A @ (setadjoin @ A @ B)) != (in @ sk52 @ sk50)))),inference(paramod_ordered,[status(thm)],[209,449])).
% 89.50/19.98 thf(764,plain,(! [B:$i,A:$i] : (((in @ A @ (setadjoin @ A @ B)) != (in @ sk52 @ sk50)))),inference(simp,[status(thm)],[763])).
% 89.50/19.98 thf(783,plain,(! [B:$i,A:$i] : ((A != sk52) | ((setadjoin @ A @ B) != sk50))),inference(simp,[status(thm)],[764])).
% 89.50/19.98 thf(792,plain,(! [A:$i] : (((setadjoin @ sk52 @ A) != sk50))),inference(simp,[status(thm)],[783])).
% 89.50/19.98 thf(110,plain,(! [B:$i,A:($i > $o)] : ((~ (A @ B)) | (A @ (sk14 @ B @ (A))) | (A @ (sk15 @ (A))))),inference(cnfConj,[status(thm)],[5])).
% 89.50/19.98 thf(205,plain,(! [B:$i,A:($i > $o)] : ((~ (A @ B)) | (A @ (sk14 @ B @ (A))) | (A @ (sk15 @ (A))))),inference(simp,[status(thm)],[110])).
% 89.50/19.98 thf(13062,plain,(~ (($true)) | ((in @ (sk25 @ sk174) @ (powerset @ (setunion @ sk174))) != (in @ sk52 @ sk51))),inference(paramod_ordered,[status(thm)],[11716,441])).
% 89.50/19.98 thf(13063,plain,(((in @ (sk25 @ sk174) @ (powerset @ (setunion @ sk174))) != (in @ sk52 @ sk51))),inference(simp,[status(thm)],[13062])).
% 89.50/19.98 thf(13105,plain,(((sk25 @ sk174) != sk52) | ((powerset @ (setunion @ sk174)) != sk51)),inference(simp,[status(thm)],[13063])).
% 89.50/19.98 thf(4067,plain,(! [D:$i,C:$i,B:$i,A:($i > ($i > $o))] : (((in @ C @ (sk5 @ B @ (A))) = (? [E:$i]: ((in @ E @ B) & (A @ E @ C)))) | ~ (($true)) | ((in @ (sk3 @ B @ (A)) @ B) != (in @ D @ emptyset)))),inference(paramod_ordered,[status(thm)],[201,202])).
% 89.50/19.98 thf(4068,plain,(! [D:$i,C:$i,B:$i,A:($i > ($i > $o))] : (((in @ C @ (sk5 @ B @ (A))) = (? [E:$i]: ((in @ E @ B) & (A @ E @ C)))) | ((in @ (sk3 @ B @ (A)) @ B) != (in @ D @ emptyset)))),inference(simp,[status(thm)],[4067])).
% 89.50/19.98 thf(4069,plain,(! [B:($i > ($i > $o)),A:$i] : (((in @ A @ (sk5 @ emptyset @ (B))) = (? [C:$i]: ((in @ C @ emptyset) & (B @ C @ A)))))),inference(pattern_uni,[status(thm)],[4068:[bind(A, $thf(F)),bind(B, $thf(emptyset)),bind(C, $thf(C)),bind(D, $thf(sk3 @ emptyset @ (F)))]])).
% 89.50/19.98 thf(4368,plain,(! [B:($i > ($i > $o)),A:$i] : (((in @ A @ (sk5 @ emptyset @ (B))) = (? [C:$i]: ((in @ C @ emptyset) & (B @ C @ A)))))),inference(simp,[status(thm)],[4069])).
% 89.50/19.98 thf(11308,plain,(! [B:($i > ($i > $o)),A:$i] : (((in @ A @ (sk5 @ emptyset @ (B))) = (? [C:$i]: ((($false)) & (B @ C @ A)))))),inference(rewrite,[status(thm)],[4368,202])).
% 89.50/19.98 thf(11309,plain,(! [B:($i > ($i > $o)),A:$i] : ((~ (in @ A @ (sk5 @ emptyset @ (B)))))),inference(simp,[status(thm)],[11308])).
% 89.50/19.98 thf(11338,plain,(! [C:($i > ($i > $o)),B:$i,A:$i] : ((A = emptyset) | ~ (($true)) | ((in @ (sk25 @ A) @ A) != (in @ B @ (sk5 @ emptyset @ (C)))))),inference(paramod_ordered,[status(thm)],[256,11309])).
% 89.50/19.98 thf(11339,plain,(! [C:($i > ($i > $o)),B:$i,A:$i] : ((A = emptyset) | ((in @ (sk25 @ A) @ A) != (in @ B @ (sk5 @ emptyset @ (C)))))),inference(simp,[status(thm)],[11338])).
% 89.50/19.98 thf(11340,plain,(! [A:($i > ($i > $o))] : (((sk5 @ emptyset @ (A)) = emptyset))),inference(pattern_uni,[status(thm)],[11339:[bind(A, $thf(sk5 @ emptyset @ (F))),bind(B, $thf(sk25 @ (sk5 @ emptyset @ (F)))),bind(C, $thf(F))]])).
% 89.50/19.98 thf(11506,plain,(! [A:($i > ($i > $o))] : (((sk5 @ emptyset @ (A)) = emptyset))),inference(simp,[status(thm)],[11340])).
% 89.50/19.98 thf(3023,plain,(! [C:$i,B:$i,A:$i] : (~ (($true)) | ((in @ B @ (setadjoin @ A @ (setadjoin @ B @ emptyset))) != (in @ C @ emptyset)))),inference(paramod_ordered,[status(thm)],[400,202])).
% 89.50/19.98 thf(3024,plain,(! [C:$i,B:$i,A:$i] : (((in @ B @ (setadjoin @ A @ (setadjoin @ B @ emptyset))) != (in @ C @ emptyset)))),inference(simp,[status(thm)],[3023])).
% 89.50/19.98 thf(3058,plain,(! [C:$i,B:$i,A:$i] : ((B != C) | ((setadjoin @ A @ (setadjoin @ B @ emptyset)) != emptyset))),inference(simp,[status(thm)],[3024])).
% 89.50/19.98 thf(3079,plain,(! [B:$i,A:$i] : (((setadjoin @ A @ (setadjoin @ B @ emptyset)) != emptyset))),inference(simp,[status(thm)],[3058])).
% 89.50/19.98 thf(16006,plain,(~ (($true)) | ((in @ sk52 @ (powerset @ (setunion @ (powerset @ (setunion @ sk203))))) != (in @ sk52 @ sk51))),inference(paramod_ordered,[status(thm)],[12040,441])).
% 89.50/19.98 thf(16007,plain,(((in @ sk52 @ (powerset @ (setunion @ (powerset @ (setunion @ sk203))))) != (in @ sk52 @ sk51))),inference(simp,[status(thm)],[16006])).
% 89.50/19.98 thf(16043,plain,((sk52 != sk52) | ((powerset @ (setunion @ (powerset @ (setunion @ sk203)))) != sk51)),inference(simp,[status(thm)],[16007])).
% 89.50/19.98 thf(16095,plain,(((powerset @ (setunion @ (powerset @ (setunion @ sk203)))) != sk51)),inference(simp,[status(thm)],[16043])).
% 89.50/19.98 thf(69,plain,(! [B:$i,A:$i] : ((~ (A = B)) | (subset @ A @ B))),inference(cnfConj,[status(thm)],[5])).
% 89.50/19.98 thf(179,plain,(! [B:$i,A:$i] : ((A != B) | (subset @ A @ B))),inference(lifteq,[status(thm)],[69])).
% 89.50/19.98 thf(180,plain,(! [A:$i] : ((subset @ A @ A))),inference(simp,[status(thm)],[179])).
% 89.50/19.98 thf(99,plain,(! [A:$i] : ((subset @ emptyset @ A))),inference(cnfConj,[status(thm)],[5])).
% 89.50/19.98 thf(375,plain,(! [A:$i] : ((subset @ emptyset @ A))),inference(simp,[status(thm)],[99])).
% 89.50/19.98 thf(56,plain,(! [B:$i,A:$i] : ((~ (in @ (sk16 @ B @ A) @ B)) | (in @ (sk17 @ B @ A) @ B) | (A = B))),inference(cnfConj,[status(thm)],[5])).
% 89.50/19.98 thf(190,plain,(! [B:$i,A:$i] : ((A = B) | (~ (in @ (sk16 @ B @ A) @ B)) | (in @ (sk17 @ B @ A) @ B))),inference(lifteq,[status(thm)],[56])).
% 89.50/19.98 thf(191,plain,(! [B:$i,A:$i] : ((A = B) | (~ (in @ (sk16 @ B @ A) @ B)) | (in @ (sk17 @ B @ A) @ B))),inference(simp,[status(thm)],[190])).
% 89.50/19.98 thf(6949,plain,((in @ sk200 @ (setadjoin @ sk50 @ (setadjoin @ sk51 @ emptyset)))),inference(cnfConj,[status(thm)],[6947])).
% 89.50/19.98 thf(7201,plain,(! [A:$i] : ((in @ (sk25 @ A) @ A) | (in @ emptyset @ sk203) | (A != sk52))),inference(paramod_ordered,[status(thm)],[256,6961])).
% 89.50/19.98 thf(7202,plain,((in @ (sk25 @ sk52) @ sk52) | (in @ emptyset @ sk203)),inference(pattern_uni,[status(thm)],[7201:[bind(A, $thf(sk52))]])).
% 89.50/19.98 thf(13849,plain,(! [A:$i] : ((in @ emptyset @ sk203) | ~ (($true)) | ((in @ (sk25 @ sk52) @ sk52) != (in @ A @ emptyset)))),inference(paramod_ordered,[status(thm)],[7202,202])).
% 89.50/19.98 thf(13850,plain,(! [A:$i] : ((in @ emptyset @ sk203) | ((in @ (sk25 @ sk52) @ sk52) != (in @ A @ emptyset)))),inference(simp,[status(thm)],[13849])).
% 89.50/19.98 thf(13937,plain,(! [A:$i] : ((in @ emptyset @ sk203) | ((sk25 @ sk52) != A) | (sk52 != emptyset))),inference(simp,[status(thm)],[13850])).
% 89.50/19.98 thf(13999,plain,((in @ emptyset @ sk203) | (sk52 != emptyset)),inference(simp,[status(thm)],[13937])).
% 89.50/19.98 thf(6794,plain,((in @ sk174 @ (setadjoin @ sk50 @ (setadjoin @ sk51 @ emptyset)))),inference(cnfConj,[status(thm)],[6792])).
% 89.50/19.98 thf(8546,plain,(! [A:$i] : (~ (($true)) | ((in @ sk174 @ (setadjoin @ sk50 @ (setadjoin @ sk51 @ emptyset))) != (in @ A @ emptyset)))),inference(paramod_ordered,[status(thm)],[6794,202])).
% 89.50/19.98 thf(8547,plain,(! [A:$i] : (((in @ sk174 @ (setadjoin @ sk50 @ (setadjoin @ sk51 @ emptyset))) != (in @ A @ emptyset)))),inference(simp,[status(thm)],[8546])).
% 89.50/19.98 thf(8653,plain,(! [A:$i] : ((sk174 != A) | ((setadjoin @ sk50 @ (setadjoin @ sk51 @ emptyset)) != emptyset))),inference(simp,[status(thm)],[8547])).
% 89.50/19.98 thf(8697,plain,(((setadjoin @ sk50 @ (setadjoin @ sk51 @ emptyset)) != emptyset)),inference(simp,[status(thm)],[8653])).
% 89.50/19.98 thf(14,plain,(! [B:$i,A:$i] : ((~ (in @ emptyset @ A)) | (~ (in @ (setadjoin @ (sk2 @ A) @ (sk2 @ A)) @ A)) | (~ (in @ B @ omega)) | (in @ B @ A))),inference(cnfConj,[status(thm)],[5])).
% 89.50/19.98 thf(204,plain,(! [B:$i,A:$i] : ((~ (in @ emptyset @ A)) | (~ (in @ (setadjoin @ (sk2 @ A) @ (sk2 @ A)) @ A)) | (~ (in @ B @ omega)) | (in @ B @ A))),inference(simp,[status(thm)],[14])).
% 89.50/19.98 thf(456,plain,(~ (($true)) | ((in @ sk52 @ (setunion @ (setadjoin @ sk50 @ (setadjoin @ sk51 @ emptyset)))) != (in @ sk52 @ sk51))),inference(paramod_ordered,[status(thm)],[34,441])).
% 89.50/19.98 thf(457,plain,(((in @ sk52 @ (setunion @ (setadjoin @ sk50 @ (setadjoin @ sk51 @ emptyset)))) != (in @ sk52 @ sk51))),inference(simp,[status(thm)],[456])).
% 89.50/19.98 thf(462,plain,((sk52 != sk52) | ((setunion @ (setadjoin @ sk50 @ (setadjoin @ sk51 @ emptyset))) != sk51)),inference(simp,[status(thm)],[457])).
% 89.50/19.98 thf(466,plain,(((setunion @ (setadjoin @ sk50 @ (setadjoin @ sk51 @ emptyset))) != sk51)),inference(simp,[status(thm)],[462])).
% 89.50/19.98 thf(10766,plain,(~ (($true)) | ((in @ (sk25 @ sk177) @ sk177) != (in @ sk52 @ sk50))),inference(paramod_ordered,[status(thm)],[10759,449])).
% 89.50/19.98 thf(10767,plain,(((in @ (sk25 @ sk177) @ sk177) != (in @ sk52 @ sk50))),inference(simp,[status(thm)],[10766])).
% 89.50/19.98 thf(10857,plain,(((sk25 @ sk177) != sk52) | (sk177 != sk50)),inference(simp,[status(thm)],[10767])).
% 89.50/19.98 thf(7048,plain,(! [A:$i] : (~ (($true)) | ((in @ sk52 @ sk200) != (in @ A @ emptyset)))),inference(paramod_ordered,[status(thm)],[6948,202])).
% 89.50/19.98 thf(7049,plain,(! [A:$i] : (((in @ sk52 @ sk200) != (in @ A @ emptyset)))),inference(simp,[status(thm)],[7048])).
% 89.50/19.98 thf(7100,plain,(! [A:$i] : ((sk52 != A) | (sk200 != emptyset))),inference(simp,[status(thm)],[7049])).
% 89.50/19.98 thf(7154,plain,((sk200 != emptyset)),inference(simp,[status(thm)],[7100])).
% 89.50/19.98 thf(7170,plain,(! [A:$i] : ((in @ (sk25 @ A) @ A) | (emptyset != emptyset) | (A != sk200))),inference(paramod_ordered,[status(thm)],[256,7154])).
% 89.50/19.98 thf(7171,plain,(! [A:$i] : ((in @ (sk25 @ A) @ A) | (A != sk200))),inference(simp,[status(thm)],[7170])).
% 89.50/19.98 thf(7172,plain,((in @ (sk25 @ sk200) @ sk200)),inference(pattern_uni,[status(thm)],[7171:[bind(A, $thf(sk200))]])).
% 89.50/19.98 thf(11769,plain,(! [B:$i,A:$i] : (~ (($true)) | (in @ B @ (powerset @ (setunion @ A))) | ((in @ (sk25 @ sk200) @ sk200) != (in @ B @ A)))),inference(paramod_ordered,[status(thm)],[7172,214])).
% 89.50/19.98 thf(11770,plain,(! [B:$i,A:$i] : ((in @ B @ (powerset @ (setunion @ A))) | ((in @ (sk25 @ sk200) @ sk200) != (in @ B @ A)))),inference(simp,[status(thm)],[11769])).
% 89.50/19.98 thf(11771,plain,((in @ (sk25 @ sk200) @ (powerset @ (setunion @ sk200)))),inference(pattern_uni,[status(thm)],[11770:[bind(A, $thf(sk200)),bind(B, $thf(sk25 @ sk200))]])).
% 89.50/19.98 thf(124,plain,(! [B:($i > $o),A:$i] : ((in @ (dsetconstr @ A @ (B)) @ (powerset @ A)))),inference(cnfConj,[status(thm)],[5])).
% 89.50/19.98 thf(271,plain,(! [B:($i > $o),A:$i] : ((in @ (dsetconstr @ A @ (B)) @ (powerset @ A)))),inference(simp,[status(thm)],[124])).
% 89.50/19.98 thf(157,plain,(! [C:$i,B:($i > $o),A:$i] : ((~ (in @ C @ A)) | (~ (B @ C)) | (~ ((dsetconstr @ A @ (B)) = emptyset)))),inference(cnfConj,[status(thm)],[5])).
% 89.50/19.98 thf(207,plain,(! [C:$i,B:($i > $o),A:$i] : (((dsetconstr @ A @ (B)) != emptyset) | (~ (in @ C @ A)) | (~ (B @ C)))),inference(lifteq,[status(thm)],[157])).
% 89.50/19.98 thf(208,plain,(! [C:$i,B:($i > $o),A:$i] : (((dsetconstr @ A @ (B)) != emptyset) | (~ (in @ C @ A)) | (~ (B @ C)))),inference(simp,[status(thm)],[207])).
% 89.50/19.98 thf(471,plain,(! [A:$i] : (~ (($true)) | ((in @ emptyset @ (powerset @ A)) != (in @ sk52 @ sk51)))),inference(paramod_ordered,[status(thm)],[212,441])).
% 89.50/19.98 thf(472,plain,(! [A:$i] : (((in @ emptyset @ (powerset @ A)) != (in @ sk52 @ sk51)))),inference(simp,[status(thm)],[471])).
% 89.50/19.98 thf(477,plain,(! [A:$i] : ((sk52 != emptyset) | ((powerset @ A) != sk51))),inference(simp,[status(thm)],[472])).
% 89.50/19.98 thf(152,plain,(! [C:$i,B:$i,A:$i] : ((~ (sk9 @ A @ B)) | (~ (in @ C @ (sk11 @ B @ A))) | (~ (in @ C @ B)))),inference(cnfConj,[status(thm)],[5])).
% 89.50/19.98 thf(213,plain,(! [C:$i,B:$i,A:$i] : ((~ (sk9 @ A @ B)) | (~ (in @ C @ (sk11 @ B @ A))) | (~ (in @ C @ B)))),inference(simp,[status(thm)],[152])).
% 89.50/19.98 thf(11963,plain,(~ (($true)) | ((in @ sk52 @ (powerset @ (setunion @ sk203))) != (in @ sk52 @ sk50))),inference(paramod_ordered,[status(thm)],[11837,449])).
% 89.50/19.98 thf(11964,plain,(((in @ sk52 @ (powerset @ (setunion @ sk203))) != (in @ sk52 @ sk50))),inference(simp,[status(thm)],[11963])).
% 89.50/19.98 thf(12077,plain,((sk52 != sk52) | ((powerset @ (setunion @ sk203)) != sk50)),inference(simp,[status(thm)],[11964])).
% 89.50/19.98 thf(12111,plain,(((powerset @ (setunion @ sk203)) != sk50)),inference(simp,[status(thm)],[12077])).
% 89.50/19.98 thf(2813,plain,((sk51 != omega) | ~ (($true)) | ((in @ (sk25 @ sk52) @ sk52) != (in @ sk52 @ sk50))),inference(paramod_ordered,[status(thm)],[1086,449])).
% 89.50/19.98 thf(2814,plain,((sk51 != omega) | ((in @ (sk25 @ sk52) @ sk52) != (in @ sk52 @ sk50))),inference(simp,[status(thm)],[2813])).
% 89.50/19.98 thf(2842,plain,((sk51 != omega) | ((sk25 @ sk52) != sk52) | (sk52 != sk50)),inference(simp,[status(thm)],[2814])).
% 89.50/19.98 thf(7079,plain,(! [B:$i,A:$o] : (~ (($true)) | A | ((in @ sk52 @ sk200) != (in @ B @ (prop2set @ A))))),inference(paramod_ordered,[status(thm)],[6948,187])).
% 89.50/19.98 thf(7080,plain,(! [B:$i,A:$o] : (A | ((in @ sk52 @ sk200) != (in @ B @ (prop2set @ A))))),inference(simp,[status(thm)],[7079])).
% 89.50/19.98 thf(7104,plain,(! [B:$i,A:$o] : (A | (sk52 != B) | ((prop2set @ A) != sk200))),inference(simp,[status(thm)],[7080])).
% 89.50/19.98 thf(7119,plain,(! [A:$o] : (A | ((prop2set @ A) != sk200))),inference(simp,[status(thm)],[7104])).
% 89.50/19.98 thf(121,plain,(! [D:($i > $o),C:($i > $o),B:$i,A:$i] : ((~ (A = B)) | ((sk46 @ (D) @ (C) @ B @ A) = (sk47 @ (D) @ (C) @ B @ A)) | ((dsetconstr @ A @ (C)) = (dsetconstr @ B @ (D))))),inference(cnfConj,[status(thm)],[5])).
% 89.50/19.98 thf(222,plain,(! [D:($i > $o),C:($i > $o),B:$i,A:$i] : ((A != B) | ((sk47 @ (D) @ (C) @ B @ A) = (sk46 @ (D) @ (C) @ B @ A)) | ((dsetconstr @ A @ (C)) = (dsetconstr @ B @ (D))))),inference(lifteq,[status(thm)],[121])).
% 89.50/19.98 thf(223,plain,(! [C:($i > $o),B:($i > $o),A:$i] : (((sk47 @ (C) @ (B) @ A @ A) = (sk46 @ (C) @ (B) @ A @ A)) | ((dsetconstr @ A @ (B)) = (dsetconstr @ A @ (C))))),inference(simp,[status(thm)],[222])).
% 89.50/19.98 thf(147,plain,(! [C:$i,B:($i > $o),A:$i] : ((~ (in @ C @ A)) | (B @ C) | (~ (B @ (sk26 @ (B) @ A))))),inference(cnfConj,[status(thm)],[5])).
% 89.50/19.98 thf(226,plain,(! [C:$i,B:($i > $o),A:$i] : ((~ (in @ C @ A)) | (B @ C) | (~ (B @ (sk26 @ (B) @ A))))),inference(simp,[status(thm)],[147])).
% 89.50/19.98 thf(16254,plain,(! [A:$i] : (~ (($true)) | ((in @ sk52 @ (powerset @ (setunion @ (powerset @ (setunion @ sk200))))) != (in @ A @ emptyset)))),inference(paramod_ordered,[status(thm)],[12284,202])).
% 89.50/19.98 thf(16255,plain,(! [A:$i] : (((in @ sk52 @ (powerset @ (setunion @ (powerset @ (setunion @ sk200))))) != (in @ A @ emptyset)))),inference(simp,[status(thm)],[16254])).
% 89.50/19.98 thf(16372,plain,(! [A:$i] : ((sk52 != A) | ((powerset @ (setunion @ (powerset @ (setunion @ sk200)))) != emptyset))),inference(simp,[status(thm)],[16255])).
% 89.50/19.98 thf(16435,plain,(((powerset @ (setunion @ (powerset @ (setunion @ sk200)))) != emptyset)),inference(simp,[status(thm)],[16372])).
% 89.50/19.98 thf(10427,plain,(~ (($true)) | ((in @ (sk25 @ sk174) @ sk174) != (in @ sk52 @ sk50))),inference(paramod_ordered,[status(thm)],[10420,449])).
% 89.50/19.98 thf(10428,plain,(((in @ (sk25 @ sk174) @ sk174) != (in @ sk52 @ sk50))),inference(simp,[status(thm)],[10427])).
% 89.50/19.98 thf(10517,plain,(((sk25 @ sk174) != sk52) | (sk174 != sk50)),inference(simp,[status(thm)],[10428])).
% 89.50/19.98 thf(1275,plain,(! [A:$i] : (~ (($true)) | ((in @ (sk25 @ (powerset @ A)) @ (powerset @ A)) != (in @ sk52 @ sk50)))),inference(paramod_ordered,[status(thm)],[1160,449])).
% 89.50/19.98 thf(1276,plain,(! [A:$i] : (((in @ (sk25 @ (powerset @ A)) @ (powerset @ A)) != (in @ sk52 @ sk50)))),inference(simp,[status(thm)],[1275])).
% 89.50/19.98 thf(1304,plain,(! [A:$i] : (((sk25 @ (powerset @ A)) != sk52) | ((powerset @ A) != sk50))),inference(simp,[status(thm)],[1276])).
% 89.50/19.98 thf(6962,plain,((in @ sk203 @ (setadjoin @ sk50 @ (setadjoin @ sk51 @ emptyset)))),inference(cnfConj,[status(thm)],[6960])).
% 89.50/19.98 thf(7046,plain,(~ (($true)) | ((in @ sk52 @ sk200) != (in @ sk52 @ sk50))),inference(paramod_ordered,[status(thm)],[6948,449])).
% 89.50/19.98 thf(7047,plain,(((in @ sk52 @ sk200) != (in @ sk52 @ sk50))),inference(simp,[status(thm)],[7046])).
% 89.50/19.98 thf(7109,plain,((sk52 != sk52) | (sk200 != sk50)),inference(simp,[status(thm)],[7047])).
% 89.50/19.98 thf(7122,plain,((sk200 != sk50)),inference(simp,[status(thm)],[7109])).
% 89.50/19.98 thf(730,plain,(! [A:$i] : (~ (($true)) | ((in @ A @ (setadjoin @ A @ emptyset)) != (in @ sk52 @ sk50)))),inference(paramod_ordered,[status(thm)],[413,449])).
% 89.50/19.98 thf(731,plain,(! [A:$i] : (((in @ A @ (setadjoin @ A @ emptyset)) != (in @ sk52 @ sk50)))),inference(simp,[status(thm)],[730])).
% 89.50/19.98 thf(752,plain,(! [A:$i] : ((A != sk52) | ((setadjoin @ A @ emptyset) != sk50))),inference(simp,[status(thm)],[731])).
% 89.50/19.98 thf(754,plain,(((setadjoin @ sk52 @ emptyset) != sk50)),inference(simp,[status(thm)],[752])).
% 89.50/19.98 thf(153,plain,(! [B:($i > $o),A:($i > $o)] : (((sk38 @ (B) @ (A)) = (sk39 @ (B) @ (A))) | ((? [C:$i]: ((A @ C) & ! [D:$i]: ((A @ D) => (C = D)))) = (? [C:$i]: ((B @ C) & ! [D:$i]: ((B @ D) => (C = D))))))),inference(cnfConj,[status(thm)],[5])).
% 89.50/19.98 thf(193,plain,(! [B:($i > $o),A:($i > $o)] : (((sk39 @ (B) @ (A)) = (sk38 @ (B) @ (A))) | ((? [C:$i]: ((A @ C) & ! [D:$i]: ((A @ D) => (C = D)))) = (? [C:$i]: ((B @ C) & ! [D:$i]: ((B @ D) => (C = D))))))),inference(lifteq,[status(thm)],[153])).
% 89.50/19.98 thf(194,plain,(! [B:($i > $o),A:($i > $o)] : (((sk39 @ (B) @ (A)) = (sk38 @ (B) @ (A))) | ((? [C:$i]: ((A @ C) & ! [D:$i]: ((A @ D) => (C = D)))) = (? [C:$i]: ((B @ C) & ! [D:$i]: ((B @ D) => (C = D))))))),inference(simp,[status(thm)],[193])).
% 89.50/19.98 thf(956,plain,(! [A:$i] : ((A = emptyset) | ~ (($true)) | ((in @ (sk25 @ A) @ A) != (in @ sk52 @ sk50)))),inference(paramod_ordered,[status(thm)],[256,449])).
% 89.50/19.98 thf(957,plain,(! [A:$i] : ((A = emptyset) | ((in @ (sk25 @ A) @ A) != (in @ sk52 @ sk50)))),inference(simp,[status(thm)],[956])).
% 89.50/19.98 thf(1127,plain,(! [A:$i] : ((A = emptyset) | ((sk25 @ A) != sk52) | (A != sk50))),inference(simp,[status(thm)],[957])).
% 89.50/19.98 thf(1145,plain,((sk50 = emptyset) | ((sk25 @ sk50) != sk52)),inference(simp,[status(thm)],[1127])).
% 89.50/19.98 thf(3038,plain,(! [B:$i,A:$i] : (~ (($true)) | ((in @ B @ (setadjoin @ A @ (setadjoin @ B @ emptyset))) != (in @ sk52 @ sk51)))),inference(paramod_ordered,[status(thm)],[400,441])).
% 89.50/19.98 thf(3039,plain,(! [B:$i,A:$i] : (((in @ B @ (setadjoin @ A @ (setadjoin @ B @ emptyset))) != (in @ sk52 @ sk51)))),inference(simp,[status(thm)],[3038])).
% 89.50/19.98 thf(3059,plain,(! [B:$i,A:$i] : ((B != sk52) | ((setadjoin @ A @ (setadjoin @ B @ emptyset)) != sk51))),inference(simp,[status(thm)],[3039])).
% 89.50/19.98 thf(3080,plain,(! [A:$i] : (((setadjoin @ A @ (setadjoin @ sk52 @ emptyset)) != sk51))),inference(simp,[status(thm)],[3059])).
% 89.50/19.98 thf(1510,plain,(! [A:$i] : ((~ (in @ A @ (prop2set @ ($false)))) | ($false))),inference(prim_subst,[status(thm)],[187:[bind(A, $thf(($false)))]])).
% 89.50/19.98 thf(1537,plain,(! [A:$i] : ((~ (in @ A @ (prop2set @ ($false)))))),inference(simp,[status(thm)],[1510])).
% 89.50/19.98 thf(1577,plain,(! [B:$i,A:$i] : ((A = emptyset) | ~ (($true)) | ((in @ (sk25 @ A) @ A) != (in @ B @ (prop2set @ ($false)))))),inference(paramod_ordered,[status(thm)],[256,1537])).
% 89.50/19.98 thf(1578,plain,(! [B:$i,A:$i] : ((A = emptyset) | ((in @ (sk25 @ A) @ A) != (in @ B @ (prop2set @ ($false)))))),inference(simp,[status(thm)],[1577])).
% 89.50/19.98 thf(1579,plain,(((prop2set @ ($false)) = emptyset)),inference(pattern_uni,[status(thm)],[1578:[bind(A, $thf(prop2set @ ($false))),bind(B, $thf(sk25 @ (prop2set @ ($false))))]])).
% 89.50/19.98 thf(771,plain,(! [B:$i,A:$i] : (~ (($true)) | ((in @ A @ (setadjoin @ A @ B)) != (in @ sk52 @ sk51)))),inference(paramod_ordered,[status(thm)],[209,441])).
% 89.50/19.98 thf(772,plain,(! [B:$i,A:$i] : (((in @ A @ (setadjoin @ A @ B)) != (in @ sk52 @ sk51)))),inference(simp,[status(thm)],[771])).
% 89.50/19.98 thf(782,plain,(! [B:$i,A:$i] : ((A != sk52) | ((setadjoin @ A @ B) != sk51))),inference(simp,[status(thm)],[772])).
% 89.50/19.98 thf(791,plain,(! [A:$i] : (((setadjoin @ sk52 @ A) != sk51))),inference(simp,[status(thm)],[782])).
% 89.50/19.98 thf(138,plain,(! [C:$i,B:$i,A:($i > $o)] : ((~ (A @ B)) | (~ (B = (sk23 @ B @ (A)))) | ((A @ C) = (C = (sk24 @ (A)))))),inference(cnfConj,[status(thm)],[5])).
% 89.50/19.98 thf(181,plain,(! [C:$i,B:$i,A:($i > $o)] : (((sk23 @ B @ (A)) != B) | ((A @ C) = (C = (sk24 @ (A)))) | (~ (A @ B)))),inference(lifteq,[status(thm)],[138])).
% 89.50/19.98 thf(182,plain,(! [C:$i,B:$i,A:($i > $o)] : (((sk23 @ B @ (A)) != B) | ((A @ C) = (C = (sk24 @ (A)))) | (~ (A @ B)))),inference(simp,[status(thm)],[181])).
% 89.50/19.98 thf(442,plain,(~ (($true)) | ((in @ emptyset @ (setadjoin @ emptyset @ emptyset)) != (in @ sk52 @ sk51))),inference(paramod_ordered,[status(thm)],[48,441])).
% 89.50/19.98 thf(443,plain,(((in @ emptyset @ (setadjoin @ emptyset @ emptyset)) != (in @ sk52 @ sk51))),inference(simp,[status(thm)],[442])).
% 89.50/19.98 thf(446,plain,((sk52 != emptyset) | ((setadjoin @ emptyset @ emptyset) != sk51)),inference(simp,[status(thm)],[443])).
% 89.50/19.98 thf(7324,plain,(! [B:$i,A:($i > $o)] : (~ (($true)) | (A @ (sk14 @ B @ (A))) | (A @ (sk15 @ (A))) | ((set2prop @ (prop2set @ ($true))) != (A @ B)))),inference(paramod_ordered,[status(thm)],[1433,205])).
% 89.50/19.98 thf(7325,plain,(! [B:$i,A:($i > $o)] : ((A @ (sk14 @ B @ (A))) | (A @ (sk15 @ (A))) | ((set2prop @ (prop2set @ ($true))) != (A @ B)))),inference(simp,[status(thm)],[7324])).
% 89.50/19.98 thf(7676,plain,((set2prop @ (sk14 @ (prop2set @ ($true)) @ (set2prop))) | (set2prop @ (sk15 @ (set2prop)))),inference(pre_uni,[status(thm)],[7325:[bind(A, $thf(set2prop)),bind(B, $thf(prop2set @ ($true)))]])).
% 89.50/19.98 thf(9409,plain,(! [A:$i] : ((in @ emptyset @ sk200) | ~ (($true)) | ((in @ (sk25 @ sk52) @ sk52) != (in @ A @ emptyset)))),inference(paramod_ordered,[status(thm)],[7060,202])).
% 89.50/19.98 thf(9410,plain,(! [A:$i] : ((in @ emptyset @ sk200) | ((in @ (sk25 @ sk52) @ sk52) != (in @ A @ emptyset)))),inference(simp,[status(thm)],[9409])).
% 89.50/19.98 thf(9486,plain,(! [A:$i] : ((in @ emptyset @ sk200) | ((sk25 @ sk52) != A) | (sk52 != emptyset))),inference(simp,[status(thm)],[9410])).
% 89.50/19.98 thf(9515,plain,((in @ emptyset @ sk200) | (sk52 != emptyset)),inference(simp,[status(thm)],[9486])).
% 89.50/19.98 thf(27,plain,(! [B:$i,A:$i] : (((in @ B @ (powerset @ A)) = (! [C:$i]: ((in @ C @ B) => (in @ C @ A)))))),inference(cnfConj,[status(thm)],[5])).
% 89.50/19.98 thf(303,plain,(! [B:$i,A:$i] : (((in @ B @ (powerset @ A)) = (! [C:$i]: ((in @ C @ B) => (in @ C @ A)))))),inference(lifteq,[status(thm)],[27])).
% 89.50/19.98 thf(304,plain,(! [B:$i,A:$i] : (((in @ B @ (powerset @ A)) = (! [C:$i]: ((in @ C @ B) => (in @ C @ A)))))),inference(simp,[status(thm)],[303])).
% 89.50/19.98 thf(144,plain,(! [B:$i,A:($i > $o)] : ((~ (A @ B)) | (A @ (sk13 @ B @ (A))) | (A @ (descr @ (A))))),inference(cnfConj,[status(thm)],[5])).
% 89.50/19.98 thf(170,plain,(! [A:$i] : ((~ (A = A)) | (A = (sk13 @ A @ ((=) @ $i @ A))) | (A = (descr @ ((=) @ $i @ A))))),inference(replace_leibeq,[status(thm)],[144:[bind(A, $thf((=) @ $i @ B))]])).
% 89.50/19.98 thf(185,plain,(! [A:$i] : ((A != A) | ((sk13 @ A @ ((=) @ $i @ A)) = A) | (A = (descr @ ((=) @ $i @ A))))),inference(lifteq,[status(thm)],[170])).
% 89.50/19.98 thf(186,plain,(! [A:$i] : (((sk13 @ A @ ((=) @ $i @ A)) = A) | (A = (descr @ ((=) @ $i @ A))))),inference(simp,[status(thm)],[185])).
% 89.50/19.98 thf(2559,plain,((sk50 != omega) | ~ (($true)) | ((in @ (sk25 @ sk52) @ sk52) != (in @ sk52 @ sk51))),inference(paramod_ordered,[status(thm)],[1038,441])).
% 89.50/19.98 thf(2560,plain,((sk50 != omega) | ((in @ (sk25 @ sk52) @ sk52) != (in @ sk52 @ sk51))),inference(simp,[status(thm)],[2559])).
% 89.50/19.98 thf(2576,plain,((sk50 != omega) | ((sk25 @ sk52) != sk52) | (sk52 != sk51)),inference(simp,[status(thm)],[2560])).
% 89.50/19.98 thf(473,plain,(! [A:$i] : (~ (($true)) | ((in @ emptyset @ (powerset @ A)) != (in @ sk52 @ sk50)))),inference(paramod_ordered,[status(thm)],[212,449])).
% 89.50/19.98 thf(474,plain,(! [A:$i] : (((in @ emptyset @ (powerset @ A)) != (in @ sk52 @ sk50)))),inference(simp,[status(thm)],[473])).
% 89.50/19.98 thf(478,plain,(! [A:$i] : ((sk52 != emptyset) | ((powerset @ A) != sk50))),inference(simp,[status(thm)],[474])).
% 89.50/19.98 thf(5527,plain,(! [C:$i,B:$i,A:$i] : (~ (($true)) | ((in @ (sk25 @ (setadjoin @ A @ B)) @ (setadjoin @ A @ B)) != (in @ C @ emptyset)))),inference(paramod_ordered,[status(thm)],[1142,202])).
% 89.50/19.98 thf(5528,plain,(! [C:$i,B:$i,A:$i] : (((in @ (sk25 @ (setadjoin @ A @ B)) @ (setadjoin @ A @ B)) != (in @ C @ emptyset)))),inference(simp,[status(thm)],[5527])).
% 89.50/19.98 thf(5574,plain,(! [C:$i,B:$i,A:$i] : (((sk25 @ (setadjoin @ A @ B)) != C) | ((setadjoin @ A @ B) != emptyset))),inference(simp,[status(thm)],[5528])).
% 89.50/19.98 thf(5590,plain,(! [B:$i,A:$i] : (((setadjoin @ A @ B) != emptyset))),inference(simp,[status(thm)],[5574])).
% 89.50/19.98 thf(101,plain,(! [B:$i,A:$i] : ((~ (in @ emptyset @ A)) | (in @ (sk2 @ A) @ A) | (~ (in @ B @ omega)) | (in @ B @ A))),inference(cnfConj,[status(thm)],[5])).
% 89.50/19.98 thf(183,plain,(! [B:$i,A:$i] : ((~ (in @ emptyset @ A)) | (in @ (sk2 @ A) @ A) | (~ (in @ B @ omega)) | (in @ B @ A))),inference(simp,[status(thm)],[101])).
% 89.50/19.98 thf(1070,plain,(! [A:$i] : ((A = emptyset) | ~ (($true)) | ((in @ (sk25 @ A) @ A) != (in @ sk52 @ sk51)))),inference(paramod_ordered,[status(thm)],[256,441])).
% 89.50/19.98 thf(1071,plain,(! [A:$i] : ((A = emptyset) | ((in @ (sk25 @ A) @ A) != (in @ sk52 @ sk51)))),inference(simp,[status(thm)],[1070])).
% 89.50/19.98 thf(1130,plain,(! [A:$i] : ((A = emptyset) | ((sk25 @ A) != sk52) | (A != sk51))),inference(simp,[status(thm)],[1071])).
% 89.50/19.98 thf(1148,plain,((sk51 = emptyset) | ((sk25 @ sk51) != sk52)),inference(simp,[status(thm)],[1130])).
% 89.50/19.98 thf(10478,plain,(~ (($true)) | ((in @ (sk25 @ sk174) @ sk174) != (in @ sk52 @ sk51))),inference(paramod_ordered,[status(thm)],[10420,441])).
% 89.50/19.98 thf(10479,plain,(((in @ (sk25 @ sk174) @ sk174) != (in @ sk52 @ sk51))),inference(simp,[status(thm)],[10478])).
% 89.50/19.98 thf(10515,plain,(((sk25 @ sk174) != sk52) | (sk174 != sk51)),inference(simp,[status(thm)],[10479])).
% 89.50/19.98 thf(16333,plain,(~ (($true)) | ((in @ sk52 @ (powerset @ (setunion @ (powerset @ (setunion @ sk200))))) != (in @ sk52 @ sk51))),inference(paramod_ordered,[status(thm)],[12284,441])).
% 89.50/19.98 thf(16334,plain,(((in @ sk52 @ (powerset @ (setunion @ (powerset @ (setunion @ sk200))))) != (in @ sk52 @ sk51))),inference(simp,[status(thm)],[16333])).
% 89.50/19.98 thf(16363,plain,((sk52 != sk52) | ((powerset @ (setunion @ (powerset @ (setunion @ sk200)))) != sk51)),inference(simp,[status(thm)],[16334])).
% 89.50/19.98 thf(16426,plain,(((powerset @ (setunion @ (powerset @ (setunion @ sk200)))) != sk51)),inference(simp,[status(thm)],[16363])).
% 89.50/19.98 thf(12992,plain,(~ (($true)) | ((in @ (sk25 @ sk174) @ (powerset @ (setunion @ sk174))) != (in @ sk52 @ sk50))),inference(paramod_ordered,[status(thm)],[11716,449])).
% 89.50/19.98 thf(12993,plain,(((in @ (sk25 @ sk174) @ (powerset @ (setunion @ sk174))) != (in @ sk52 @ sk50))),inference(simp,[status(thm)],[12992])).
% 89.50/19.98 thf(13101,plain,(((sk25 @ sk174) != sk52) | ((powerset @ (setunion @ sk174)) != sk50)),inference(simp,[status(thm)],[12993])).
% 89.50/19.98 thf(7223,plain,(~ (($true)) | ((in @ sk52 @ sk203) != (in @ sk52 @ sk51))),inference(paramod_ordered,[status(thm)],[6961,441])).
% 89.50/19.98 thf(7224,plain,(((in @ sk52 @ sk203) != (in @ sk52 @ sk51))),inference(simp,[status(thm)],[7223])).
% 89.50/19.98 thf(7254,plain,((sk52 != sk52) | (sk203 != sk51)),inference(simp,[status(thm)],[7224])).
% 89.50/19.98 thf(7291,plain,((sk203 != sk51)),inference(simp,[status(thm)],[7254])).
% 89.50/19.98 thf(1178,plain,(~ (($true)) | ((in @ (sk25 @ omega) @ omega) != (in @ sk52 @ sk51))),inference(paramod_ordered,[status(thm)],[895,441])).
% 89.50/19.98 thf(1179,plain,(((in @ (sk25 @ omega) @ omega) != (in @ sk52 @ sk51))),inference(simp,[status(thm)],[1178])).
% 89.50/19.98 thf(1197,plain,(((sk25 @ omega) != sk52) | (sk51 != omega)),inference(simp,[status(thm)],[1179])).
% 89.50/19.98 thf(1217,plain,(~ (($true)) | ((in @ (sk25 @ (setadjoin @ emptyset @ emptyset)) @ (setadjoin @ emptyset @ emptyset)) != (in @ sk52 @ sk50))),inference(paramod_ordered,[status(thm)],[1043,449])).
% 89.50/19.98 thf(1218,plain,(((in @ (sk25 @ (setadjoin @ emptyset @ emptyset)) @ (setadjoin @ emptyset @ emptyset)) != (in @ sk52 @ sk50))),inference(simp,[status(thm)],[1217])).
% 89.50/19.98 thf(1261,plain,(((sk25 @ (setadjoin @ emptyset @ emptyset)) != sk52) | ((setadjoin @ emptyset @ emptyset) != sk50)),inference(simp,[status(thm)],[1218])).
% 89.50/19.98 thf(6807,plain,((in @ sk177 @ (setadjoin @ sk50 @ (setadjoin @ sk51 @ emptyset)))),inference(cnfConj,[status(thm)],[6805])).
% 89.50/19.98 thf(2625,plain,(! [B:$i,A:$i] : (~ (($true)) | ((in @ B @ (powerset @ (setadjoin @ A @ B))) != (in @ sk52 @ sk50)))),inference(paramod_ordered,[status(thm)],[2613,449])).
% 89.50/19.98 thf(2626,plain,(! [B:$i,A:$i] : (((in @ B @ (powerset @ (setadjoin @ A @ B))) != (in @ sk52 @ sk50)))),inference(simp,[status(thm)],[2625])).
% 89.50/19.98 thf(2652,plain,(! [B:$i,A:$i] : ((B != sk52) | ((powerset @ (setadjoin @ A @ B)) != sk50))),inference(simp,[status(thm)],[2626])).
% 89.50/19.98 thf(2672,plain,(! [A:$i] : (((powerset @ (setadjoin @ A @ sk52)) != sk50))),inference(simp,[status(thm)],[2652])).
% 89.50/19.98 thf(78,plain,(! [C:$i,B:$i,A:$i] : ((~ (in @ C @ B)) | (in @ C @ (setunion @ (setadjoin @ A @ (setadjoin @ B @ emptyset)))))),inference(cnfConj,[status(thm)],[5])).
% 89.50/19.98 thf(215,plain,(! [C:$i,B:$i,A:$i] : ((~ (in @ C @ B)) | (in @ C @ (setunion @ (setadjoin @ A @ (setadjoin @ B @ emptyset)))))),inference(simp,[status(thm)],[78])).
% 89.50/19.98 thf(732,plain,(! [B:$i,A:$i] : (~ (($true)) | ((in @ A @ (setadjoin @ A @ emptyset)) != (in @ B @ emptyset)))),inference(paramod_ordered,[status(thm)],[413,202])).
% 89.50/19.98 thf(733,plain,(! [B:$i,A:$i] : (((in @ A @ (setadjoin @ A @ emptyset)) != (in @ B @ emptyset)))),inference(simp,[status(thm)],[732])).
% 89.50/19.98 thf(753,plain,(! [B:$i,A:$i] : ((A != B) | ((setadjoin @ A @ emptyset) != emptyset))),inference(simp,[status(thm)],[733])).
% 89.50/19.98 thf(755,plain,(! [A:$i] : (((setadjoin @ A @ emptyset) != emptyset))),inference(simp,[status(thm)],[753])).
% 89.50/19.98 thf(13264,plain,(~ (($true)) | ((in @ (sk25 @ omega) @ (powerset @ (setunion @ omega))) != (in @ sk52 @ sk51))),inference(paramod_ordered,[status(thm)],[11765,441])).
% 89.50/19.98 thf(13265,plain,(((in @ (sk25 @ omega) @ (powerset @ (setunion @ omega))) != (in @ sk52 @ sk51))),inference(simp,[status(thm)],[13264])).
% 89.50/19.98 thf(13306,plain,(((sk25 @ omega) != sk52) | ((powerset @ (setunion @ omega)) != sk51)),inference(simp,[status(thm)],[13265])).
% 89.50/19.98 thf(12270,plain,(~ (($true)) | ((in @ sk52 @ (powerset @ (setunion @ sk200))) != (in @ sk52 @ sk51))),inference(paramod_ordered,[status(thm)],[11840,441])).
% 89.50/19.98 thf(12271,plain,(((in @ sk52 @ (powerset @ (setunion @ sk200))) != (in @ sk52 @ sk51))),inference(simp,[status(thm)],[12270])).
% 89.50/19.98 thf(12323,plain,((sk52 != sk52) | ((powerset @ (setunion @ sk200)) != sk51)),inference(simp,[status(thm)],[12271])).
% 89.50/19.98 thf(12359,plain,(((powerset @ (setunion @ sk200)) != sk51)),inference(simp,[status(thm)],[12323])).
% 89.50/19.98 thf(450,plain,(~ (($true)) | ((in @ emptyset @ (setadjoin @ emptyset @ emptyset)) != (in @ sk52 @ sk50))),inference(paramod_ordered,[status(thm)],[48,449])).
% 89.50/19.98 thf(451,plain,(((in @ emptyset @ (setadjoin @ emptyset @ emptyset)) != (in @ sk52 @ sk50))),inference(simp,[status(thm)],[450])).
% 89.50/19.98 thf(454,plain,((sk52 != emptyset) | ((setadjoin @ emptyset @ emptyset) != sk50)),inference(simp,[status(thm)],[451])).
% 89.50/19.98 thf(25726,plain,(($false)),inference(e,[status(thm)],[930,192,7159,629,760,347,10844,217,12040,3285,2676,4960,449,1142,202,11684,13127,1529,12351,4539,184,1191,196,12122,1298,7060,3919,325,11716,2852,13788,7268,16448,253,13290,480,221,1433,206,439,201,12100,12365,467,2670,625,1555,7314,3750,13362,16108,256,1160,225,2613,11774,212,16083,2581,3074,5317,1263,792,1086,205,13105,11506,11837,34,3079,16095,180,375,64,10420,191,6949,13999,8697,204,54,6794,466,11765,10857,187,406,11771,7282,271,208,477,213,12111,895,198,2842,7119,12284,455,223,226,3,16435,438,7172,7154,10517,1304,10759,6962,209,7122,754,194,10736,1145,6806,3080,199,331,441,1038,11840,1579,791,182,7202,446,6793,465,7676,203,9515,304,186,2576,478,5590,214,447,183,1148,790,10515,16426,13101,7291,400,1197,3362,1261,6807,1550,10403,2672,6961,215,755,13306,12359,454,6948])).
% 89.50/19.98 % SZS output end Refutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% 89.50/19.98 % [INFO] Killing All external provers ...
%------------------------------------------------------------------------------