%------------------------------------------------------------------------------
% File : E---3.5.1
% Problem : SEU618^1 : TPTP v9.3.1. Released v3.7.0.
% Transfm : none
% Format : tptp:raw
% Command : run_E /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n006.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:24:45 AM UTC 2026
% Result : Theorem 3.16s 0.78s
% Output : CNFRefutation 3.16s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SEU618^1 : TPTP v9.3.1. Released v3.7.0.
% 0.00/0.04 % Command : run_E /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.08/0.18 % Computer : n006.cluster.edu
% 0.08/0.18 % Model : x86_64 x86_64
% 0.08/0.18 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.18 % Memory : 8046.5625MB
% 0.08/0.18 % OS : Linux 6.8.0-71-generic
% 0.08/0.18 % CPULimit : 300
% 0.08/0.18 % WCLimit : 300
% 0.08/0.18 % DateTime : Tue Sep 29 13:57:54 UTC 2026
% 0.08/0.18 % CPUTime :
% 0.08/0.18 Running run_E /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.08/0.23 Running higher-order theorem proving
% 0.21/0.26 Running: /export/starexec/sandbox/solver/bin/eprover-ho --delete-bad-limit=2000000000 --definitional-cnf=24 -s --print-statistics -R --print-version --proof-object --auto-schedule=8 --cpu-limit=300 /export/starexec/sandbox/tmp/tmp.0juZloQVyw/E---3.1_756803.p
% 3.16/0.78 % Version: 3.5.1-ho
% 3.16/0.78 % Preprocessing class: HSLMSLSSLLLCHFA.
% 3.16/0.78 % Scheduled 8 strats onto 8 cores with 300 seconds (2400 total)
% 3.16/0.78 % Starting ehoh_best5 with 300s (1) cores
% 3.16/0.78 % Starting almost_fo_3_lam with 300s (1) cores
% 3.16/0.78 % Starting new_bool_5 with 300s (1) cores
% 3.16/0.78 % Starting pre_casc_3 with 300s (1) cores
% 3.16/0.78 % Starting ho_unfolding_8 with 300s (1) cores
% 3.16/0.78 % Starting new_ho_10_cnf2 with 300s (1) cores
% 3.16/0.78 % Starting new_bool_3 with 300s (1) cores
% 3.16/0.78 % Starting new_ho_5 with 300s (1) cores
% 3.16/0.78 % new_ho_5 with pid 756857 completed with status 9
% 3.16/0.78 % new_bool_5 with pid 756852 completed with status 0
% 3.16/0.78 % Result found by new_bool_5
% 3.16/0.78 % Preprocessing class: HSLMSLSSLLLCHFA.
% 3.16/0.78 % Scheduled 8 strats onto 8 cores with 300 seconds (2400 total)
% 3.16/0.78 % Starting ehoh_best5 with 300s (1) cores
% 3.16/0.78 % Starting almost_fo_3_lam with 300s (1) cores
% 3.16/0.78 % Starting new_bool_5 with 300s (1) cores
% 3.16/0.78 % (lift_lambdas = 1, lambda_to_forall = 1,unroll_only_formulas = 1, sine = GSinE(CountFormulas,hypos,1.0,,1,20000,1.0))
% 3.16/0.78 % SinE strategy is GSinE(CountFormulas,hypos,1.0,,1,20000,1.0)
% 3.16/0.78 % Search class: HGHSM-FSLS31-MHFMMSBN
% 3.16/0.78 % Scheduled 7 strats onto 1 cores with 300 seconds (300 total)
% 3.16/0.78 % Starting SubtermCWHack with 28s (1) cores
% 3.16/0.78 % SubtermCWHack with pid 756865 completed with status 0
% 3.16/0.78 % Result found by SubtermCWHack
% 3.16/0.78 % Preprocessing class: HSLMSLSSLLLCHFA.
% 3.16/0.78 % Scheduled 8 strats onto 8 cores with 300 seconds (2400 total)
% 3.16/0.78 % Starting ehoh_best5 with 300s (1) cores
% 3.16/0.78 % Starting almost_fo_3_lam with 300s (1) cores
% 3.16/0.78 % Starting new_bool_5 with 300s (1) cores
% 3.16/0.78 % (lift_lambdas = 1, lambda_to_forall = 1,unroll_only_formulas = 1, sine = GSinE(CountFormulas,hypos,1.0,,1,20000,1.0))
% 3.16/0.78 % SinE strategy is GSinE(CountFormulas,hypos,1.0,,1,20000,1.0)
% 3.16/0.78 % Search class: HGHSM-FSLS31-MHFMMSBN
% 3.16/0.78 % Scheduled 7 strats onto 1 cores with 300 seconds (300 total)
% 3.16/0.78 % Starting SubtermCWHack with 28s (1) cores
% 3.16/0.78 % Preprocessing time : 0.002 s
% 3.16/0.78
% 3.16/0.78 % Proof found!
% 3.16/0.78 % SZS status Theorem
% 3.16/0.78 % SZS output start CNFRefutation
% 3.16/0.78 thf(decl_23, type, in: $i > $i > $o).
% 3.16/0.78 thf(decl_24, type, exu: ($i > $o) > $o).
% 3.16/0.78 thf(decl_25, type, setextAx: $o).
% 3.16/0.78 thf(decl_26, type, emptyset: $i).
% 3.16/0.78 thf(decl_27, type, emptysetAx: $o).
% 3.16/0.78 thf(decl_28, type, setadjoin: $i > $i > $i).
% 3.16/0.78 thf(decl_29, type, setadjoinAx: $o).
% 3.16/0.78 thf(decl_30, type, powerset: $i > $i).
% 3.16/0.78 thf(decl_31, type, powersetAx: $o).
% 3.16/0.78 thf(decl_32, type, setunion: $i > $i).
% 3.16/0.78 thf(decl_33, type, setunionAx: $o).
% 3.16/0.78 thf(decl_34, type, omega: $i).
% 3.16/0.78 thf(decl_35, type, omega0Ax: $o).
% 3.16/0.78 thf(decl_36, type, omegaSAx: $o).
% 3.16/0.78 thf(decl_37, type, omegaIndAx: $o).
% 3.16/0.78 thf(decl_38, type, replAx: $o).
% 3.16/0.78 thf(decl_39, type, foundationAx: $o).
% 3.16/0.78 thf(decl_40, type, wellorderingAx: $o).
% 3.16/0.78 thf(decl_41, type, descr: ($i > $o) > $i).
% 3.16/0.78 thf(decl_42, type, descrp: $o).
% 3.16/0.78 thf(decl_43, type, dsetconstr: $i > ($i > $o) > $i).
% 3.16/0.78 thf(decl_44, type, dsetconstrI: $o).
% 3.16/0.78 thf(decl_45, type, dsetconstrEL: $o).
% 3.16/0.78 thf(decl_46, type, dsetconstrER: $o).
% 3.16/0.78 thf(decl_47, type, exuE1: $o).
% 3.16/0.78 thf(decl_48, type, prop2set: $o > $i).
% 3.16/0.78 thf(decl_49, type, prop2setE: $o).
% 3.16/0.78 thf(decl_50, type, emptysetE: $o).
% 3.16/0.78 thf(decl_51, type, emptysetimpfalse: $o).
% 3.16/0.78 thf(decl_52, type, notinemptyset: $o).
% 3.16/0.78 thf(decl_53, type, exuE3e: $o).
% 3.16/0.78 thf(decl_54, type, setext: $o).
% 3.16/0.78 thf(decl_55, type, emptyI: $o).
% 3.16/0.78 thf(decl_56, type, noeltsimpempty: $o).
% 3.16/0.78 thf(decl_57, type, setbeta: $o).
% 3.16/0.78 thf(decl_58, type, nonempty: $i > $o).
% 3.16/0.78 thf(decl_59, type, nonemptyE1: $o).
% 3.16/0.78 thf(decl_60, type, nonemptyI: $o).
% 3.16/0.78 thf(decl_61, type, nonemptyI1: $o).
% 3.16/0.78 thf(decl_62, type, setadjoinIL: $o).
% 3.16/0.78 thf(decl_63, type, emptyinunitempty: $o).
% 3.16/0.78 thf(decl_64, type, setadjoinIR: $o).
% 3.16/0.78 thf(decl_65, type, setadjoinE: $o).
% 3.16/0.78 thf(decl_66, type, setadjoinOr: $o).
% 3.16/0.78 thf(decl_67, type, setoftrueEq: $o).
% 3.16/0.78 thf(decl_68, type, powersetI: $o).
% 3.16/0.78 thf(decl_69, type, emptyinPowerset: $o).
% 3.16/0.78 thf(decl_70, type, emptyInPowerset: $o).
% 3.16/0.78 thf(decl_71, type, powersetE: $o).
% 3.16/0.78 thf(decl_72, type, setunionI: $o).
% 3.16/0.78 thf(decl_73, type, setunionE: $o).
% 3.16/0.78 thf(decl_74, type, subPowSU: $o).
% 3.16/0.78 thf(decl_75, type, exuE2: $o).
% 3.16/0.78 thf(decl_76, type, nonemptyImpWitness: $o).
% 3.16/0.78 thf(decl_77, type, uniqinunit: $o).
% 3.16/0.78 thf(decl_78, type, notinsingleton: $o).
% 3.16/0.78 thf(decl_79, type, eqinunit: $o).
% 3.16/0.78 thf(decl_80, type, singletonsswitch: $o).
% 3.16/0.78 thf(decl_81, type, upairsetE: $o).
% 3.16/0.78 thf(decl_82, type, upairsetIL: $o).
% 3.16/0.78 thf(decl_83, type, upairsetIR: $o).
% 3.16/0.78 thf(decl_84, type, emptyE1: $o).
% 3.16/0.78 thf(decl_85, type, vacuousDall: $o).
% 3.16/0.78 thf(decl_86, type, quantDeMorgan1: $o).
% 3.16/0.78 thf(decl_87, type, quantDeMorgan2: $o).
% 3.16/0.78 thf(decl_88, type, quantDeMorgan3: $o).
% 3.16/0.78 thf(decl_89, type, quantDeMorgan4: $o).
% 3.16/0.78 thf(decl_90, type, prop2setI: $o).
% 3.16/0.78 thf(decl_92, type, prop2set2propI: $o).
% 3.16/0.78 thf(decl_93, type, notdexE: $o).
% 3.16/0.78 thf(decl_94, type, notdallE: $o).
% 3.16/0.78 thf(decl_95, type, exuI1: $o).
% 3.16/0.78 thf(decl_96, type, exuI3: $o).
% 3.16/0.78 thf(decl_97, type, exuI2: $o).
% 3.16/0.78 thf(decl_98, type, inCongP: $o).
% 3.16/0.78 thf(decl_99, type, in__Cong: $o).
% 3.16/0.78 thf(decl_100, type, exuE3u: $o).
% 3.16/0.78 thf(decl_101, type, exu__Cong: $o).
% 3.16/0.78 thf(decl_102, type, emptyset__Cong: $o).
% 3.16/0.78 thf(decl_103, type, setadjoin__Cong: $o).
% 3.16/0.78 thf(decl_104, type, powerset__Cong: $o).
% 3.16/0.78 thf(decl_105, type, setunion__Cong: $o).
% 3.16/0.78 thf(decl_106, type, omega__Cong: $o).
% 3.16/0.78 thf(decl_107, type, exuEu: $o).
% 3.16/0.78 thf(decl_108, type, descr__Cong: $o).
% 3.16/0.78 thf(decl_109, type, dsetconstr__Cong: $o).
% 3.16/0.78 thf(decl_110, type, subset: $i > $i > $o).
% 3.16/0.78 thf(decl_113, type, subsetI1: $o).
% 3.16/0.78 thf(decl_114, type, eqimpsubset2: $o).
% 3.16/0.78 thf(decl_115, type, eqimpsubset1: $o).
% 3.16/0.78 thf(decl_116, type, subsetI2: $o).
% 3.16/0.78 thf(decl_117, type, emptysetsubset: $o).
% 3.16/0.78 thf(decl_118, type, subsetE: $o).
% 3.16/0.78 thf(decl_119, type, subsetE2: $o).
% 3.16/0.78 thf(decl_120, type, notsubsetI: $o).
% 3.16/0.78 thf(decl_121, type, notequalI1: $o).
% 3.16/0.78 thf(decl_122, type, notequalI2: $o).
% 3.16/0.78 thf(decl_123, type, subsetRefl: $o).
% 3.16/0.78 thf(decl_124, type, subsetTrans: $o).
% 3.16/0.78 thf(decl_125, type, setadjoinSub: $o).
% 3.16/0.78 thf(decl_126, type, setadjoinSub2: $o).
% 3.16/0.78 thf(decl_127, type, subset2powerset: $o).
% 3.16/0.78 thf(decl_128, type, setextsub: $o).
% 3.16/0.78 thf(decl_129, type, subsetemptysetimpeq: $o).
% 3.16/0.78 thf(decl_130, type, powersetI1: $o).
% 3.16/0.78 thf(decl_131, type, powersetE1: $o).
% 3.16/0.78 thf(decl_132, type, inPowerset: $o).
% 3.16/0.78 thf(decl_133, type, powersetsubset: $o).
% 3.16/0.78 thf(decl_134, type, sepInPowerset: $o).
% 3.16/0.78 thf(decl_135, type, sepSubset: $o).
% 3.16/0.78 thf(decl_136, type, binunion: $i > $i > $i).
% 3.16/0.78 thf(decl_137, type, binunionIL: $o).
% 3.16/0.78 thf(decl_138, type, upairset2IR: $o).
% 3.16/0.78 thf(decl_139, type, binunionIR: $o).
% 3.16/0.79 thf(decl_140, type, binunionEcases: $o).
% 3.16/0.79 thf(decl_141, type, binunionE: $o).
% 3.16/0.79 thf(decl_142, type, binunionLsub: $o).
% 3.16/0.79 thf(decl_143, type, binunionRsub: $o).
% 3.16/0.79 thf(decl_144, type, binintersect: $i > $i > $i).
% 3.16/0.79 thf(decl_145, type, binintersectI: $o).
% 3.16/0.79 thf(decl_146, type, binintersectSubset5: $o).
% 3.16/0.79 thf(decl_147, type, binintersectEL: $o).
% 3.16/0.79 thf(decl_148, type, binintersectLsub: $o).
% 3.16/0.79 thf(decl_149, type, binintersectSubset2: $o).
% 3.16/0.79 thf(decl_150, type, binintersectSubset3: $o).
% 3.16/0.79 thf(decl_151, type, binintersectER: $o).
% 3.16/0.79 thf(decl_152, type, disjointsetsI1: $o).
% 3.16/0.79 thf(decl_153, type, binintersectRsub: $o).
% 3.16/0.79 thf(decl_154, type, binintersectSubset4: $o).
% 3.16/0.79 thf(decl_155, type, binintersectSubset1: $o).
% 3.16/0.79 thf(decl_156, type, bs114d: $o).
% 3.16/0.79 thf(decl_158, type, setminus: $i > $i > $i).
% 3.16/0.79 thf(decl_159, type, setminusI: $o).
% 3.16/0.79 thf(decl_160, type, setminusEL: $o).
% 3.16/0.79 thf(decl_161, type, setminusER: $o).
% 3.16/0.79 thf(decl_162, type, setminusSubset2: $o).
% 3.16/0.79 thf(decl_163, type, setminusERneg: $o).
% 3.16/0.79 thf(decl_164, type, setminusELneg: $o).
% 3.16/0.79 thf(decl_165, type, setminusILneg: $o).
% 3.16/0.79 thf(decl_166, type, setminusIRneg: $o).
% 3.16/0.79 thf(decl_167, type, setminusLsub: $o).
% 3.16/0.79 thf(decl_168, type, setminusSubset1: $o).
% 3.16/0.79 thf(decl_169, type, symdiff: $i > $i > $i).
% 3.16/0.79 thf(decl_170, type, symdiffE: $o).
% 3.16/0.79 thf(decl_171, type, symdiffI1: $o).
% 3.16/0.79 thf(decl_172, type, symdiffI2: $o).
% 3.16/0.79 thf(decl_173, type, symdiffIneg1: $o).
% 3.16/0.79 thf(decl_174, type, symdiffIneg2: $o).
% 3.16/0.79 thf(decl_176, type, secondinupair: $o).
% 3.16/0.79 thf(decl_177, type, setukpairIL: $o).
% 3.16/0.79 thf(decl_178, type, epred1_0: $o).
% 3.16/0.79 thf(decl_179, type, esk1_2: $i > $i > $i).
% 3.16/0.79 thf(decl_180, type, esk2_2: $i > $i > $i).
% 3.16/0.79 thf(decl_181, type, esk3_2: $i > $i > $i).
% 3.16/0.79 thf(decl_182, type, esk4_1: $i > $i).
% 3.16/0.79 thf(decl_183, type, esk5_2: ($i > $i > $o) > $i > $i).
% 3.16/0.79 thf(decl_184, type, esk6_2: ($i > $i > $o) > $i > $i).
% 3.16/0.79 thf(decl_185, type, esk7_3: ($i > $i > $o) > $i > $i > $i).
% 3.16/0.79 thf(decl_186, type, esk8_1: $i > $i).
% 3.16/0.79 thf(decl_187, type, esk9_1: ($i > $o) > $i).
% 3.16/0.79 thf(decl_188, type, esk10_1: ($i > $o) > $i).
% 3.16/0.79 thf(decl_189, type, esk11_2: $i > $i > $i).
% 3.16/0.79 thf(decl_190, type, esk12_2: $i > $i > $i).
% 3.16/0.79 thf(decl_191, type, esk13_1: $i > $i).
% 3.16/0.79 thf(decl_192, type, esk14_1: $i > $i).
% 3.16/0.79 thf(decl_193, type, esk15_1: $i > $i).
% 3.16/0.79 thf(decl_194, type, esk16_2: $i > $i > $i).
% 3.16/0.79 thf(decl_195, type, esk17_3: $i > $i > $o > $i).
% 3.16/0.79 thf(decl_196, type, esk18_1: ($i > $o) > $i).
% 3.16/0.79 thf(decl_197, type, esk19_1: $i > $i).
% 3.16/0.79 thf(decl_198, type, esk20_2: $i > ($i > $o) > $i).
% 3.16/0.79 thf(decl_199, type, esk21_2: $i > ($i > $o) > $i).
% 3.16/0.79 thf(decl_200, type, esk22_2: $i > ($i > $o) > $i).
% 3.16/0.79 thf(decl_201, type, esk23_2: $i > ($i > $o) > $i).
% 3.16/0.79 thf(decl_202, type, esk24_2: $i > ($i > $o) > $i).
% 3.16/0.79 thf(decl_203, type, esk25_2: $i > ($i > $o) > $i).
% 3.16/0.79 thf(decl_204, type, esk26_2: ($i > $o) > $i > $i).
% 3.16/0.79 thf(decl_205, type, esk27_1: ($i > $o) > $i).
% 3.16/0.79 thf(decl_206, type, esk28_1: ($i > $o) > $i).
% 3.16/0.79 thf(decl_207, type, esk29_2: ($i > $o) > $i > $i).
% 3.16/0.79 thf(decl_208, type, esk30_2: ($i > $o) > ($i > $o) > $i).
% 3.16/0.79 thf(decl_209, type, esk31_2: ($i > $o) > ($i > $o) > $i).
% 3.16/0.79 thf(decl_210, type, esk32_2: ($i > $o) > ($i > $o) > $i).
% 3.16/0.79 thf(decl_211, type, esk33_2: ($i > $o) > ($i > $o) > $i).
% 3.16/0.79 thf(decl_212, type, esk34_4: $i > $i > ($i > $o) > ($i > $o) > $i).
% 3.16/0.79 thf(decl_213, type, esk35_4: $i > $i > ($i > $o) > ($i > $o) > $i).
% 3.16/0.79 thf(decl_214, type, esk36_2: $i > $i > $i).
% 3.16/0.79 thf(decl_215, type, esk37_2: $i > $i > $i).
% 3.16/0.79 thf(decl_216, type, esk38_2: $i > $i > $i).
% 3.16/0.79 thf(decl_217, type, esk39_0: $i).
% 3.16/0.79 thf(decl_218, type, esk40_0: $i).
% 3.16/0.79 thf(setukpairIR, 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)=>((binunionEcases)=>((binunionE)=>((binunionLsub)=>((binunionRsub)=>((binintersectI)=>((binintersectSubset5)=>((binintersectEL)=>((binintersectLsub)=>((binintersectSubset2)=>((binintersectSubset3)=>((binintersectER)=>((disjointsetsI1)=>((binintersectRsub)=>((binintersectSubset4)=>((binintersectSubset1)=>((bs114d)=>((setminusI)=>((setminusEL)=>((setminusER)=>((setminusSubset2)=>((setminusERneg)=>((setminusELneg)=>((setminusILneg)=>((setminusIRneg)=>((setminusLsub)=>((setminusSubset1)=>((symdiffE)=>((symdiffI1)=>((symdiffI2)=>((symdiffIneg1)=>((symdiffIneg2)=>((secondinupair)=>((setukpairIL)=>![X2:$i, X3:$i]:((in @ X3 @ (setunion @ (setadjoin @ (setadjoin @ X2 @ emptyset) @ (setadjoin @ (setadjoin @ X2 @ (setadjoin @ X3 @ emptyset)) @ emptyset))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))), file('/export/starexec/sandbox/tmp/tmp.0juZloQVyw/E---3.1_756803.p', setukpairIR)).
% 3.16/0.79 thf(nonemptyI, axiom, ((nonemptyI)<=>![X4:$i, X1:$i > $o, X2:$i]:(((in @ X2 @ X4)=>((X1 @ X2)=>(nonempty @ (dsetconstr @ X4 @ (^[X3:$i]:((X1 @ X3))))))))), file('/export/starexec/sandbox/tmp/tmp.0juZloQVyw/E---3.1_756803.p', nonemptyI)).
% 3.16/0.79 thf(setbeta, axiom, ((setbeta)<=>![X4:$i, X1:$i > $o, X2:$i]:(((in @ X2 @ X4)=>((in @ X2 @ (dsetconstr @ X4 @ (^[X3:$i]:((X1 @ X3)))))<=>(X1 @ X2))))), file('/export/starexec/sandbox/tmp/tmp.0juZloQVyw/E---3.1_756803.p', setbeta)).
% 3.16/0.79 thf(setoftrueEq, axiom, ((setoftrueEq)<=>![X4:$i]:(((dsetconstr @ X4 @ (^[X2:$i]:(($true))))=(X4)))), file('/export/starexec/sandbox/tmp/tmp.0juZloQVyw/E---3.1_756803.p', setoftrueEq)).
% 3.16/0.79 thf(exuE2, axiom, ((exuE2)<=>![X1:$i > $o]:(((exu @ (^[X2:$i]:((X1 @ X2))))=>?[X2:$i]:(![X3:$i]:(((X1 @ X3)<=>((X3)=(X2)))))))), file('/export/starexec/sandbox/tmp/tmp.0juZloQVyw/E---3.1_756803.p', exuE2)).
% 3.16/0.79 thf(emptyE1, axiom, ((emptyE1)<=>![X4:$i, X1:$i > $o]:((?[X2:$i]:(((in @ X2 @ X4)&(X1 @ X2)))=>(((dsetconstr @ X4 @ (^[X2:$i]:((X1 @ X2))))=(emptyset))=>~($true))))), file('/export/starexec/sandbox/tmp/tmp.0juZloQVyw/E---3.1_756803.p', emptyE1)).
% 3.16/0.79 thf(exuI1, axiom, ((exuI1)<=>![X1:$i > $o]:((?[X2:$i]:(((X1 @ X2)&![X3:$i]:(((X1 @ X3)=>((X2)=(X3))))))=>(exu @ (^[X2:$i]:((X1 @ X2))))))), file('/export/starexec/sandbox/tmp/tmp.0juZloQVyw/E---3.1_756803.p', exuI1)).
% 3.16/0.79 thf(exuI3, axiom, ((exuI3)<=>![X1:$i > $o]:((?[X2:$i]:((X1 @ X2))=>(![X2:$i, X3:$i]:(((X1 @ X2)=>((X1 @ X3)=>((X2)=(X3)))))=>(exu @ (^[X2:$i]:((X1 @ X2)))))))), file('/export/starexec/sandbox/tmp/tmp.0juZloQVyw/E---3.1_756803.p', exuI3)).
% 3.16/0.79 thf(exu__Cong, axiom, ((exu__Cong)<=>![X1:$i > $o, X17:$i > $o]:((![X2:$i, X3:$i]:((((X2)=(X3))=>((X1 @ X2)<=>(X17 @ X3))))=>((exu @ (^[X2:$i]:((X1 @ X2))))<=>(exu @ (^[X2:$i]:((X17 @ X2)))))))), file('/export/starexec/sandbox/tmp/tmp.0juZloQVyw/E---3.1_756803.p', exu__Cong)).
% 3.16/0.79 thf(exuE3u, axiom, ((exuE3u)<=>![X1:$i > $o]:(((exu @ (^[X2:$i]:((X1 @ X2))))=>![X2:$i, X3:$i]:(((X1 @ X2)=>((X1 @ X3)=>((X2)=(X3)))))))), file('/export/starexec/sandbox/tmp/tmp.0juZloQVyw/E---3.1_756803.p', exuE3u)).
% 3.16/0.79 thf(exuI2, axiom, ((exuI2)<=>![X1:$i > $o]:((?[X2:$i]:(![X3:$i]:(((X1 @ X3)<=>((X3)=(X2)))))=>(exu @ (^[X2:$i]:((X1 @ X2))))))), file('/export/starexec/sandbox/tmp/tmp.0juZloQVyw/E---3.1_756803.p', exuI2)).
% 3.16/0.79 thf(dsetconstr__Cong, axiom, ((dsetconstr__Cong)<=>![X4:$i, X5:$i]:((((X4)=(X5))=>![X1:$i > $o, X17:$i > $o]:((![X2:$i]:(((in @ X2 @ X4)=>![X3:$i]:(((in @ X3 @ X5)=>(((X2)=(X3))=>((X1 @ X2)<=>(X17 @ X3)))))))=>((dsetconstr @ X4 @ (^[X2:$i]:((X1 @ X2))))=(dsetconstr @ X5 @ (^[X2:$i]:((X17 @ X2)))))))))), file('/export/starexec/sandbox/tmp/tmp.0juZloQVyw/E---3.1_756803.p', dsetconstr__Cong)).
% 3.16/0.79 thf(descr__Cong, axiom, ((descr__Cong)<=>![X1:$i > $o, X17:$i > $o]:((![X2:$i, X3:$i]:((((X2)=(X3))=>((X1 @ X2)<=>(X17 @ X3))))=>((exu @ (^[X2:$i]:((X1 @ X2))))=>((exu @ (^[X2:$i]:((X17 @ X2))))=>((descr @ (^[X2:$i]:((X1 @ X2))))=(descr @ (^[X2:$i]:((X17 @ X2)))))))))), file('/export/starexec/sandbox/tmp/tmp.0juZloQVyw/E---3.1_756803.p', descr__Cong)).
% 3.16/0.79 thf(exuEu, axiom, ((exuEu)<=>![X1:$i > $o]:(((exu @ (^[X2:$i]:((X1 @ X2))))=>![X2:$i, X3:$i]:(((X1 @ X2)=>((X1 @ X3)=>((X2)=(X3)))))))), file('/export/starexec/sandbox/tmp/tmp.0juZloQVyw/E---3.1_756803.p', exuEu)).
% 3.16/0.79 thf(sepSubset, axiom, ((sepSubset)<=>![X4:$i, X1:$i > $o]:((subset @ (dsetconstr @ X4 @ (^[X2:$i]:((X1 @ X2)))) @ X4))), file('/export/starexec/sandbox/tmp/tmp.0juZloQVyw/E---3.1_756803.p', sepSubset)).
% 3.16/0.79 thf(sepInPowerset, axiom, ((sepInPowerset)<=>![X4:$i, X1:$i > $o]:((in @ (dsetconstr @ X4 @ (^[X2:$i]:((X1 @ X2)))) @ (powerset @ X4)))), file('/export/starexec/sandbox/tmp/tmp.0juZloQVyw/E---3.1_756803.p', sepInPowerset)).
% 3.16/0.79 thf(exuE3e, axiom, ((exuE3e)<=>![X1:$i > $o]:(((exu @ (^[X2:$i]:((X1 @ X2))))=>?[X2:$i]:((X1 @ X2))))), file('/export/starexec/sandbox/tmp/tmp.0juZloQVyw/E---3.1_756803.p', exuE3e)).
% 3.16/0.79 thf(exuE1, axiom, ((exuE1)<=>![X1:$i > $o]:(((exu @ (^[X2:$i]:((X1 @ X2))))=>?[X2:$i]:(((X1 @ X2)&![X3:$i]:(((X1 @ X3)=>((X2)=(X3))))))))), file('/export/starexec/sandbox/tmp/tmp.0juZloQVyw/E---3.1_756803.p', exuE1)).
% 3.16/0.79 thf(dsetconstrER, axiom, ((dsetconstrER)<=>![X4:$i, X1:$i > $o, X2:$i]:(((in @ X2 @ (dsetconstr @ X4 @ (^[X3:$i]:((X1 @ X3)))))=>(X1 @ X2)))), file('/export/starexec/sandbox/tmp/tmp.0juZloQVyw/E---3.1_756803.p', dsetconstrER)).
% 3.16/0.79 thf(dsetconstrEL, axiom, ((dsetconstrEL)<=>![X4:$i, X1:$i > $o, X2:$i]:(((in @ X2 @ (dsetconstr @ X4 @ (^[X3:$i]:((X1 @ X3)))))=>(in @ X2 @ X4)))), file('/export/starexec/sandbox/tmp/tmp.0juZloQVyw/E---3.1_756803.p', dsetconstrEL)).
% 3.16/0.79 thf(dsetconstrI, axiom, ((dsetconstrI)<=>![X4:$i, X1:$i > $o, X2:$i]:(((in @ X2 @ X4)=>((X1 @ X2)=>(in @ X2 @ (dsetconstr @ X4 @ (^[X3:$i]:((X1 @ X3))))))))), file('/export/starexec/sandbox/tmp/tmp.0juZloQVyw/E---3.1_756803.p', dsetconstrI)).
% 3.16/0.79 thf(descrp, axiom, ((descrp)<=>![X1:$i > $o]:(((exu @ (^[X2:$i]:((X1 @ X2))))=>(X1 @ (descr @ (^[X2:$i]:((X1 @ X2)))))))), file('/export/starexec/sandbox/tmp/tmp.0juZloQVyw/E---3.1_756803.p', descrp)).
% 3.16/0.79 thf(replAx, axiom, ((replAx)<=>![X6:$i > $i > $o, X4:$i]:((![X2:$i]:(((in @ X2 @ X4)=>(exu @ (^[X3:$i]:((X6 @ X2 @ X3))))))=>?[X5:$i]:(![X2:$i]:(((in @ X2 @ X5)<=>?[X3:$i]:(((in @ X3 @ X4)&(X6 @ X3 @ X2))))))))), file('/export/starexec/sandbox/tmp/tmp.0juZloQVyw/E---3.1_756803.p', replAx)).
% 3.16/0.79 thf(binintersectLsub, axiom, ((binintersectLsub)<=>![X4:$i, X5:$i]:((subset @ (binintersect @ X4 @ X5) @ X4))), file('/export/starexec/sandbox/tmp/tmp.0juZloQVyw/E---3.1_756803.p', binintersectLsub)).
% 3.16/0.79 thf(binintersectSubset5, axiom, ((binintersectSubset5)<=>![X4:$i, X5:$i, X7:$i]:(((subset @ X7 @ X4)=>((subset @ X7 @ X5)=>(subset @ X7 @ (binintersect @ X4 @ X5)))))), file('/export/starexec/sandbox/tmp/tmp.0juZloQVyw/E---3.1_756803.p', binintersectSubset5)).
% 3.16/0.79 thf(binintersectEL, axiom, ((binintersectEL)<=>![X4:$i, X5:$i, X2:$i]:(((in @ X2 @ (binintersect @ X4 @ X5))=>(in @ X2 @ X4)))), file('/export/starexec/sandbox/tmp/tmp.0juZloQVyw/E---3.1_756803.p', binintersectEL)).
% 3.16/0.79 thf(binintersectSubset2, axiom, ((binintersectSubset2)<=>![X4:$i, X5:$i]:(((subset @ X4 @ X5)=>((binintersect @ X4 @ X5)=(X4))))), file('/export/starexec/sandbox/tmp/tmp.0juZloQVyw/E---3.1_756803.p', binintersectSubset2)).
% 3.16/0.79 thf(binintersectSubset3, axiom, ((binintersectSubset3)<=>![X4:$i, X5:$i]:((((binintersect @ X4 @ X5)=(X5))=>(subset @ X5 @ X4)))), file('/export/starexec/sandbox/tmp/tmp.0juZloQVyw/E---3.1_756803.p', binintersectSubset3)).
% 3.16/0.79 thf(binintersectER, axiom, ((binintersectER)<=>![X4:$i, X5:$i, X2:$i]:(((in @ X2 @ (binintersect @ X4 @ X5))=>(in @ X2 @ X5)))), file('/export/starexec/sandbox/tmp/tmp.0juZloQVyw/E---3.1_756803.p', binintersectER)).
% 3.16/0.79 thf(disjointsetsI1, axiom, ((disjointsetsI1)<=>![X4:$i, X5:$i]:((~(?[X2:$i]:(((in @ X2 @ X4)&(in @ X2 @ X5))))=>((binintersect @ X4 @ X5)=(emptyset))))), file('/export/starexec/sandbox/tmp/tmp.0juZloQVyw/E---3.1_756803.p', disjointsetsI1)).
% 3.16/0.79 thf(binintersectRsub, axiom, ((binintersectRsub)<=>![X4:$i, X5:$i]:((subset @ (binintersect @ X4 @ X5) @ X5))), file('/export/starexec/sandbox/tmp/tmp.0juZloQVyw/E---3.1_756803.p', binintersectRsub)).
% 3.16/0.79 thf(binintersectSubset4, axiom, ((binintersectSubset4)<=>![X4:$i, X5:$i]:(((subset @ X5 @ X4)=>((binintersect @ X4 @ X5)=(X5))))), file('/export/starexec/sandbox/tmp/tmp.0juZloQVyw/E---3.1_756803.p', binintersectSubset4)).
% 3.16/0.79 thf(nonemptyI1, axiom, ((nonemptyI1)<=>![X4:$i]:((?[X2:$i]:((in @ X2 @ X4))=>(nonempty @ X4)))), file('/export/starexec/sandbox/tmp/tmp.0juZloQVyw/E---3.1_756803.p', nonemptyI1)).
% 3.16/0.79 thf(binintersectSubset1, axiom, ((binintersectSubset1)<=>![X4:$i, X5:$i]:((((binintersect @ X4 @ X5)=(X4))=>(subset @ X4 @ X5)))), file('/export/starexec/sandbox/tmp/tmp.0juZloQVyw/E---3.1_756803.p', binintersectSubset1)).
% 3.16/0.79 thf(bs114d, axiom, ((bs114d)<=>![X4:$i, X5:$i, X7:$i]:(((binintersect @ X4 @ (binunion @ X5 @ X7))=(binunion @ (binintersect @ X4 @ X5) @ (binintersect @ X4 @ X7))))), file('/export/starexec/sandbox/tmp/tmp.0juZloQVyw/E---3.1_756803.p', bs114d)).
% 3.16/0.79 thf(nonemptyE1, axiom, ((nonemptyE1)<=>![X4:$i]:(((nonempty @ X4)=>?[X2:$i]:((in @ X2 @ X4))))), file('/export/starexec/sandbox/tmp/tmp.0juZloQVyw/E---3.1_756803.p', nonemptyE1)).
% 3.16/0.79 thf(setminusI, axiom, ((setminusI)<=>![X4:$i, X5:$i, X2:$i]:(((in @ X2 @ X4)=>(~((in @ X2 @ X5))=>(in @ X2 @ (setminus @ X4 @ X5)))))), file('/export/starexec/sandbox/tmp/tmp.0juZloQVyw/E---3.1_756803.p', setminusI)).
% 3.16/0.79 thf(setminusEL, axiom, ((setminusEL)<=>![X4:$i, X5:$i, X2:$i]:(((in @ X2 @ (setminus @ X4 @ X5))=>(in @ X2 @ X4)))), file('/export/starexec/sandbox/tmp/tmp.0juZloQVyw/E---3.1_756803.p', setminusEL)).
% 3.16/0.79 thf(noeltsimpempty, axiom, ((noeltsimpempty)<=>![X4:$i]:((![X2:$i]:(~((in @ X2 @ X4)))=>((X4)=(emptyset))))), file('/export/starexec/sandbox/tmp/tmp.0juZloQVyw/E---3.1_756803.p', noeltsimpempty)).
% 3.16/0.79 thf(setminusER, axiom, ((setminusER)<=>![X4:$i, X5:$i, X2:$i]:(((in @ X2 @ (setminus @ X4 @ X5))=>~((in @ X2 @ X5))))), file('/export/starexec/sandbox/tmp/tmp.0juZloQVyw/E---3.1_756803.p', setminusER)).
% 3.16/0.79 thf(emptyI, axiom, ((emptyI)<=>![X4:$i]:((![X2:$i]:(~((in @ X2 @ X4)))=>((X4)=(emptyset))))), file('/export/starexec/sandbox/tmp/tmp.0juZloQVyw/E---3.1_756803.p', emptyI)).
% 3.16/0.79 thf(setminusSubset2, axiom, ((setminusSubset2)<=>![X4:$i, X5:$i]:(((subset @ X4 @ X5)=>((setminus @ X4 @ X5)=(emptyset))))), file('/export/starexec/sandbox/tmp/tmp.0juZloQVyw/E---3.1_756803.p', setminusSubset2)).
% 3.16/0.79 thf(setext, axiom, ((setext)<=>![X4:$i, X5:$i]:((![X2:$i]:(((in @ X2 @ X4)=>(in @ X2 @ X5)))=>(![X2:$i]:(((in @ X2 @ X5)=>(in @ X2 @ X4)))=>((X4)=(X5)))))), file('/export/starexec/sandbox/tmp/tmp.0juZloQVyw/E---3.1_756803.p', setext)).
% 3.16/0.79 thf(setminusERneg, axiom, ((setminusERneg)<=>![X4:$i, X5:$i, X2:$i]:((~((in @ X2 @ (setminus @ X4 @ X5)))=>((in @ X2 @ X4)=>(in @ X2 @ X5))))), file('/export/starexec/sandbox/tmp/tmp.0juZloQVyw/E---3.1_756803.p', setminusERneg)).
% 3.16/0.79 thf(setadjoinIL, axiom, ((setadjoinIL)<=>![X2:$i, X3:$i]:((in @ X2 @ (setadjoin @ X2 @ X3)))), file('/export/starexec/sandbox/tmp/tmp.0juZloQVyw/E---3.1_756803.p', setadjoinIL)).
% 3.16/0.79 thf(setminusELneg, axiom, ((setminusELneg)<=>![X4:$i, X5:$i, X2:$i]:((~((in @ X2 @ (setminus @ X4 @ X5)))=>(~((in @ X2 @ X5))=>~((in @ X2 @ X4)))))), file('/export/starexec/sandbox/tmp/tmp.0juZloQVyw/E---3.1_756803.p', setminusELneg)).
% 3.16/0.79 thf(setminusILneg, axiom, ((setminusILneg)<=>![X4:$i, X5:$i, X2:$i]:((~((in @ X2 @ X4))=>~((in @ X2 @ (setminus @ X4 @ X5)))))), file('/export/starexec/sandbox/tmp/tmp.0juZloQVyw/E---3.1_756803.p', setminusILneg)).
% 3.16/0.79 thf(setminusIRneg, axiom, ((setminusIRneg)<=>![X4:$i, X5:$i, X2:$i]:(((in @ X2 @ X5)=>~((in @ X2 @ (setminus @ X4 @ X5)))))), file('/export/starexec/sandbox/tmp/tmp.0juZloQVyw/E---3.1_756803.p', setminusIRneg)).
% 3.16/0.79 thf(setminusLsub, axiom, ((setminusLsub)<=>![X4:$i, X5:$i]:((subset @ (setminus @ X4 @ X5) @ X4))), file('/export/starexec/sandbox/tmp/tmp.0juZloQVyw/E---3.1_756803.p', setminusLsub)).
% 3.16/0.79 thf(setminusSubset1, axiom, ((setminusSubset1)<=>![X4:$i, X5:$i]:((((setminus @ X4 @ X5)=(emptyset))=>(subset @ X4 @ X5)))), file('/export/starexec/sandbox/tmp/tmp.0juZloQVyw/E---3.1_756803.p', setminusSubset1)).
% 3.16/0.79 thf(symdiffE, axiom, ((symdiffE)<=>![X4:$i, X5:$i, X2:$i]:(((in @ X2 @ (symdiff @ X4 @ X5))=>![X20:$o]:((((in @ X2 @ X4)=>(~((in @ X2 @ X5))=>(X20)))=>((~((in @ X2 @ X4))=>((in @ X2 @ X5)=>(X20)))=>(X20))))))), file('/export/starexec/sandbox/tmp/tmp.0juZloQVyw/E---3.1_756803.p', symdiffE)).
% 3.16/0.79 thf(symdiffI1, axiom, ((symdiffI1)<=>![X4:$i, X5:$i, X2:$i]:(((in @ X2 @ X4)=>(~((in @ X2 @ X5))=>(in @ X2 @ (symdiff @ X4 @ X5)))))), file('/export/starexec/sandbox/tmp/tmp.0juZloQVyw/E---3.1_756803.p', symdiffI1)).
% 3.16/0.79 thf(symdiffI2, axiom, ((symdiffI2)<=>![X4:$i, X5:$i, X2:$i]:((~((in @ X2 @ X4))=>((in @ X2 @ X5)=>(in @ X2 @ (symdiff @ X4 @ X5)))))), file('/export/starexec/sandbox/tmp/tmp.0juZloQVyw/E---3.1_756803.p', symdiffI2)).
% 3.16/0.79 thf(symdiffIneg1, axiom, ((symdiffIneg1)<=>![X4:$i, X5:$i, X2:$i]:(((in @ X2 @ X4)=>((in @ X2 @ X5)=>~((in @ X2 @ (symdiff @ X4 @ X5))))))), file('/export/starexec/sandbox/tmp/tmp.0juZloQVyw/E---3.1_756803.p', symdiffIneg1)).
% 3.16/0.79 thf(symdiffIneg2, axiom, ((symdiffIneg2)<=>![X4:$i, X5:$i, X2:$i]:((~((in @ X2 @ X4))=>(~((in @ X2 @ X5))=>~((in @ X2 @ (symdiff @ X4 @ X5))))))), file('/export/starexec/sandbox/tmp/tmp.0juZloQVyw/E---3.1_756803.p', symdiffIneg2)).
% 3.16/0.79 thf(secondinupair, axiom, ((secondinupair)<=>![X2:$i, X3:$i]:((in @ X3 @ (setadjoin @ X2 @ (setadjoin @ X3 @ emptyset))))), file('/export/starexec/sandbox/tmp/tmp.0juZloQVyw/E---3.1_756803.p', secondinupair)).
% 3.16/0.79 thf(setukpairIL, axiom, ((setukpairIL)<=>![X2:$i, X3:$i]:((in @ X2 @ (setunion @ (setadjoin @ (setadjoin @ X2 @ emptyset) @ (setadjoin @ (setadjoin @ X2 @ (setadjoin @ X3 @ emptyset)) @ emptyset)))))), file('/export/starexec/sandbox/tmp/tmp.0juZloQVyw/E---3.1_756803.p', setukpairIL)).
% 3.16/0.79 thf(emptyinPowerset, axiom, ((emptyinPowerset)<=>![X4:$i]:((in @ emptyset @ (powerset @ X4)))), file('/export/starexec/sandbox/tmp/tmp.0juZloQVyw/E---3.1_756803.p', emptyinPowerset)).
% 3.16/0.79 thf(powersetI, axiom, ((powersetI)<=>![X4:$i, X5:$i]:((![X2:$i]:(((in @ X2 @ X5)=>(in @ X2 @ X4)))=>(in @ X5 @ (powerset @ X4))))), file('/export/starexec/sandbox/tmp/tmp.0juZloQVyw/E---3.1_756803.p', powersetI)).
% 3.16/0.79 thf(setadjoinOr, axiom, ((setadjoinOr)<=>![X2:$i, X4:$i, X3:$i]:(((in @ X3 @ (setadjoin @ X2 @ X4))=>(((X3)=(X2))|(in @ X3 @ X4))))), file('/export/starexec/sandbox/tmp/tmp.0juZloQVyw/E---3.1_756803.p', setadjoinOr)).
% 3.16/0.79 thf(setadjoinE, axiom, ((setadjoinE)<=>![X2:$i, X4:$i, X3:$i]:(((in @ X3 @ (setadjoin @ X2 @ X4))=>![X12:$o]:(((((X3)=(X2))=>(X12))=>(((in @ X3 @ X4)=>(X12))=>(X12))))))), file('/export/starexec/sandbox/tmp/tmp.0juZloQVyw/E---3.1_756803.p', setadjoinE)).
% 3.16/0.79 thf(setadjoinIR, axiom, ((setadjoinIR)<=>![X2:$i, X4:$i, X3:$i]:(((in @ X3 @ X4)=>(in @ X3 @ (setadjoin @ X2 @ X4))))), file('/export/starexec/sandbox/tmp/tmp.0juZloQVyw/E---3.1_756803.p', setadjoinIR)).
% 3.16/0.79 thf(emptyinunitempty, axiom, ((emptyinunitempty)<=>(in @ emptyset @ (setadjoin @ emptyset @ emptyset))), file('/export/starexec/sandbox/tmp/tmp.0juZloQVyw/E---3.1_756803.p', emptyinunitempty)).
% 3.16/0.79 thf(emptyInPowerset, axiom, ((emptyInPowerset)<=>![X4:$i]:((in @ emptyset @ (powerset @ X4)))), file('/export/starexec/sandbox/tmp/tmp.0juZloQVyw/E---3.1_756803.p', emptyInPowerset)).
% 3.16/0.79 thf(uniqinunit, axiom, ((uniqinunit)<=>![X2:$i, X3:$i]:(((in @ X2 @ (setadjoin @ X3 @ emptyset))=>((X2)=(X3))))), file('/export/starexec/sandbox/tmp/tmp.0juZloQVyw/E---3.1_756803.p', uniqinunit)).
% 3.16/0.79 thf(nonemptyImpWitness, axiom, ((nonemptyImpWitness)<=>![X4:$i]:(((nonempty @ X4)=>?[X2:$i]:(((in @ X2 @ X4)&($true)))))), file('/export/starexec/sandbox/tmp/tmp.0juZloQVyw/E---3.1_756803.p', nonemptyImpWitness)).
% 3.16/0.79 thf(subPowSU, axiom, ((subPowSU)<=>![X4:$i, X2:$i]:(((in @ X2 @ X4)=>(in @ X2 @ (powerset @ (setunion @ X4)))))), file('/export/starexec/sandbox/tmp/tmp.0juZloQVyw/E---3.1_756803.p', subPowSU)).
% 3.16/0.79 thf(setunionE, axiom, ((setunionE)<=>![X4:$i, X2:$i]:(((in @ X2 @ (setunion @ X4))=>![X13:$o]:((![X5:$i]:(((in @ X2 @ X5)=>((in @ X5 @ X4)=>(X13))))=>(X13)))))), file('/export/starexec/sandbox/tmp/tmp.0juZloQVyw/E---3.1_756803.p', setunionE)).
% 3.16/0.79 thf(setunionI, axiom, ((setunionI)<=>![X4:$i, X2:$i, X5:$i]:(((in @ X2 @ X5)=>((in @ X5 @ X4)=>(in @ X2 @ (setunion @ X4)))))), file('/export/starexec/sandbox/tmp/tmp.0juZloQVyw/E---3.1_756803.p', setunionI)).
% 3.16/0.79 thf(powersetE, axiom, ((powersetE)<=>![X4:$i, X5:$i, X2:$i]:(((in @ X5 @ (powerset @ X4))=>((in @ X2 @ X5)=>(in @ X2 @ X4))))), file('/export/starexec/sandbox/tmp/tmp.0juZloQVyw/E---3.1_756803.p', powersetE)).
% 3.16/0.79 thf(notinsingleton, axiom, ((notinsingleton)<=>![X2:$i, X3:$i]:((((X2)!=(X3))=>~((in @ X3 @ (setadjoin @ X2 @ emptyset)))))), file('/export/starexec/sandbox/tmp/tmp.0juZloQVyw/E---3.1_756803.p', notinsingleton)).
% 3.16/0.79 thf(emptysetsubset, axiom, ((emptysetsubset)<=>![X4:$i]:((subset @ emptyset @ X4))), file('/export/starexec/sandbox/tmp/tmp.0juZloQVyw/E---3.1_756803.p', emptysetsubset)).
% 3.16/0.79 thf(subsetI2, axiom, ((subsetI2)<=>![X4:$i, X5:$i]:((![X2:$i]:(((in @ X2 @ X4)=>(in @ X2 @ X5)))=>(subset @ X4 @ X5)))), file('/export/starexec/sandbox/tmp/tmp.0juZloQVyw/E---3.1_756803.p', subsetI2)).
% 3.16/0.79 thf(subsetRefl, axiom, ((subsetRefl)<=>![X4:$i]:((subset @ X4 @ X4))), file('/export/starexec/sandbox/tmp/tmp.0juZloQVyw/E---3.1_756803.p', subsetRefl)).
% 3.16/0.79 thf(powersetI1, axiom, ((powersetI1)<=>![X4:$i, X5:$i]:(((subset @ X5 @ X4)=>(in @ X5 @ (powerset @ X4))))), file('/export/starexec/sandbox/tmp/tmp.0juZloQVyw/E---3.1_756803.p', powersetI1)).
% 3.16/0.79 thf(subsetemptysetimpeq, axiom, ((subsetemptysetimpeq)<=>![X4:$i]:(((subset @ X4 @ emptyset)=>((X4)=(emptyset))))), file('/export/starexec/sandbox/tmp/tmp.0juZloQVyw/E---3.1_756803.p', subsetemptysetimpeq)).
% 3.16/0.79 thf(setextsub, axiom, ((setextsub)<=>![X4:$i, X5:$i]:(((subset @ X4 @ X5)=>((subset @ X5 @ X4)=>((X4)=(X5)))))), file('/export/starexec/sandbox/tmp/tmp.0juZloQVyw/E---3.1_756803.p', setextsub)).
% 3.16/0.79 thf(vacuousDall, axiom, ((vacuousDall)<=>![X1:$i > $o, X2:$i]:(((in @ X2 @ emptyset)=>(X1 @ X2)))), file('/export/starexec/sandbox/tmp/tmp.0juZloQVyw/E---3.1_756803.p', vacuousDall)).
% 3.16/0.79 thf(upairsetIR, axiom, ((upairsetIR)<=>![X2:$i, X3:$i]:((in @ X3 @ (setadjoin @ X2 @ (setadjoin @ X3 @ emptyset))))), file('/export/starexec/sandbox/tmp/tmp.0juZloQVyw/E---3.1_756803.p', upairsetIR)).
% 3.16/0.79 thf(upairsetIL, axiom, ((upairsetIL)<=>![X2:$i, X3:$i]:((in @ X2 @ (setadjoin @ X2 @ (setadjoin @ X3 @ emptyset))))), file('/export/starexec/sandbox/tmp/tmp.0juZloQVyw/E---3.1_756803.p', upairsetIL)).
% 3.16/0.79 thf(upairsetE, axiom, ((upairsetE)<=>![X2:$i, X3:$i, X14:$i]:(((in @ X14 @ (setadjoin @ X2 @ (setadjoin @ X3 @ emptyset)))=>(((X14)=(X2))|((X14)=(X3)))))), file('/export/starexec/sandbox/tmp/tmp.0juZloQVyw/E---3.1_756803.p', upairsetE)).
% 3.16/0.79 thf(singletonsswitch, axiom, ((singletonsswitch)<=>![X2:$i, X3:$i]:(((in @ X2 @ (setadjoin @ X3 @ emptyset))=>(in @ X3 @ (setadjoin @ X2 @ emptyset))))), file('/export/starexec/sandbox/tmp/tmp.0juZloQVyw/E---3.1_756803.p', singletonsswitch)).
% 3.16/0.79 thf(eqinunit, axiom, ((eqinunit)<=>![X2:$i, X3:$i]:((((X2)=(X3))=>(in @ X2 @ (setadjoin @ X3 @ emptyset))))), file('/export/starexec/sandbox/tmp/tmp.0juZloQVyw/E---3.1_756803.p', eqinunit)).
% 3.16/0.79 thf(quantDeMorgan1, axiom, ((quantDeMorgan1)<=>![X4:$i, X1:$i > $o]:((~(![X2:$i]:(((in @ X2 @ X4)=>(X1 @ X2))))=>?[X2:$i]:(((in @ X2 @ X4)&~((X1 @ X2))))))), file('/export/starexec/sandbox/tmp/tmp.0juZloQVyw/E---3.1_756803.p', quantDeMorgan1)).
% 3.16/0.79 thf(notdallE, axiom, ((notdallE)<=>![X4:$i, X1:$i > $o]:((~(![X2:$i]:(((in @ X2 @ X4)=>(X1 @ X2))))=>?[X2:$i]:(((in @ X2 @ X4)&~((X1 @ X2))))))), file('/export/starexec/sandbox/tmp/tmp.0juZloQVyw/E---3.1_756803.p', notdallE)).
% 3.16/0.79 thf(notdexE, axiom, ((notdexE)<=>![X4:$i, X1:$i > $o]:((~(?[X2:$i]:(((in @ X2 @ X4)&(X1 @ X2))))=>![X2:$i]:(((in @ X2 @ X4)=>~((X1 @ X2))))))), file('/export/starexec/sandbox/tmp/tmp.0juZloQVyw/E---3.1_756803.p', notdexE)).
% 3.16/0.79 thf(prop2setI, axiom, ((prop2setI)<=>![X15:$o]:(((X15)=>(in @ emptyset @ (prop2set @ ((X15))))))), file('/export/starexec/sandbox/tmp/tmp.0juZloQVyw/E---3.1_756803.p', prop2setI)).
% 3.16/0.79 thf(quantDeMorgan4, axiom, ((quantDeMorgan4)<=>![X4:$i, X1:$i > $o]:((?[X2:$i]:(((in @ X2 @ X4)&~((X1 @ X2))))=>~(![X2:$i]:(((in @ X2 @ X4)=>(X1 @ X2))))))), file('/export/starexec/sandbox/tmp/tmp.0juZloQVyw/E---3.1_756803.p', quantDeMorgan4)).
% 3.16/0.79 thf(quantDeMorgan3, axiom, ((quantDeMorgan3)<=>![X4:$i, X1:$i > $o]:((~(?[X2:$i]:(((in @ X2 @ X4)&(X1 @ X2))))=>![X2:$i]:(((in @ X2 @ X4)=>~((X1 @ X2))))))), file('/export/starexec/sandbox/tmp/tmp.0juZloQVyw/E---3.1_756803.p', quantDeMorgan3)).
% 3.16/0.79 thf(quantDeMorgan2, axiom, ((quantDeMorgan2)<=>![X4:$i, X1:$i > $o]:((![X2:$i]:(((in @ X2 @ X4)=>~((X1 @ X2))))=>~(?[X2:$i]:(((in @ X2 @ X4)&(X1 @ X2))))))), file('/export/starexec/sandbox/tmp/tmp.0juZloQVyw/E---3.1_756803.p', quantDeMorgan2)).
% 3.16/0.79 thf(setadjoin__Cong, axiom, ((setadjoin__Cong)<=>![X2:$i, X3:$i]:((((X2)=(X3))=>![X14:$i, X18:$i]:((((X14)=(X18))=>((setadjoin @ X2 @ X14)=(setadjoin @ X3 @ X18))))))), file('/export/starexec/sandbox/tmp/tmp.0juZloQVyw/E---3.1_756803.p', setadjoin__Cong)).
% 3.16/0.79 thf(emptyset__Cong, axiom, ((emptyset__Cong)<=>((emptyset)=(emptyset))), file('/export/starexec/sandbox/tmp/tmp.0juZloQVyw/E---3.1_756803.p', emptyset__Cong)).
% 3.16/0.79 thf(in__Cong, axiom, ((in__Cong)<=>![X4:$i, X5:$i]:((((X4)=(X5))=>![X2:$i, X3:$i]:((((X2)=(X3))=>((in @ X2 @ X4)<=>(in @ X3 @ X5))))))), file('/export/starexec/sandbox/tmp/tmp.0juZloQVyw/E---3.1_756803.p', in__Cong)).
% 3.16/0.79 thf(inCongP, axiom, ((inCongP)<=>![X4:$i, X5:$i]:((((X4)=(X5))=>![X2:$i, X3:$i]:((((X2)=(X3))=>((in @ X2 @ X4)=>(in @ X3 @ X5))))))), file('/export/starexec/sandbox/tmp/tmp.0juZloQVyw/E---3.1_756803.p', inCongP)).
% 3.16/0.79 thf(powerset__Cong, axiom, ((powerset__Cong)<=>![X4:$i, X5:$i]:((((X4)=(X5))=>((powerset @ X4)=(powerset @ X5))))), file('/export/starexec/sandbox/tmp/tmp.0juZloQVyw/E---3.1_756803.p', powerset__Cong)).
% 3.16/0.79 thf(eqimpsubset2, axiom, ((eqimpsubset2)<=>![X4:$i, X5:$i]:((((X4)=(X5))=>(subset @ X5 @ X4)))), file('/export/starexec/sandbox/tmp/tmp.0juZloQVyw/E---3.1_756803.p', eqimpsubset2)).
% 3.16/0.79 thf(subsetI1, axiom, ((subsetI1)<=>![X4:$i, X5:$i]:((![X2:$i]:(((in @ X2 @ X4)=>(in @ X2 @ X5)))=>(subset @ X4 @ X5)))), file('/export/starexec/sandbox/tmp/tmp.0juZloQVyw/E---3.1_756803.p', subsetI1)).
% 3.16/0.79 thf(omega__Cong, axiom, ((omega__Cong)<=>((omega)=(omega))), file('/export/starexec/sandbox/tmp/tmp.0juZloQVyw/E---3.1_756803.p', omega__Cong)).
% 3.16/0.79 thf(setunion__Cong, axiom, ((setunion__Cong)<=>![X4:$i, X5:$i]:((((X4)=(X5))=>((setunion @ X4)=(setunion @ X5))))), file('/export/starexec/sandbox/tmp/tmp.0juZloQVyw/E---3.1_756803.p', setunion__Cong)).
% 3.16/0.79 thf(eqimpsubset1, axiom, ((eqimpsubset1)<=>![X4:$i, X5:$i]:((((X4)=(X5))=>(subset @ X4 @ X5)))), file('/export/starexec/sandbox/tmp/tmp.0juZloQVyw/E---3.1_756803.p', eqimpsubset1)).
% 3.16/0.79 thf(notequalI2, axiom, ((notequalI2)<=>![X4:$i, X5:$i, X2:$i]:(((in @ X2 @ X4)=>(~((in @ X2 @ X5))=>((X4)!=(X5)))))), file('/export/starexec/sandbox/tmp/tmp.0juZloQVyw/E---3.1_756803.p', notequalI2)).
% 3.16/0.79 thf(notequalI1, axiom, ((notequalI1)<=>![X4:$i, X5:$i]:((~((subset @ X4 @ X5))=>((X4)!=(X5))))), file('/export/starexec/sandbox/tmp/tmp.0juZloQVyw/E---3.1_756803.p', notequalI1)).
% 3.16/0.79 thf(notsubsetI, axiom, ((notsubsetI)<=>![X4:$i, X5:$i, X2:$i]:(((in @ X2 @ X4)=>(~((in @ X2 @ X5))=>~((subset @ X4 @ X5)))))), file('/export/starexec/sandbox/tmp/tmp.0juZloQVyw/E---3.1_756803.p', notsubsetI)).
% 3.16/0.79 thf(subsetE2, axiom, ((subsetE2)<=>![X4:$i, X5:$i, X2:$i]:(((subset @ X4 @ X5)=>(~((in @ X2 @ X5))=>~((in @ X2 @ X4)))))), file('/export/starexec/sandbox/tmp/tmp.0juZloQVyw/E---3.1_756803.p', subsetE2)).
% 3.16/0.79 thf(subsetE, axiom, ((subsetE)<=>![X4:$i, X5:$i, X2:$i]:(((subset @ X4 @ X5)=>((in @ X2 @ X4)=>(in @ X2 @ X5))))), file('/export/starexec/sandbox/tmp/tmp.0juZloQVyw/E---3.1_756803.p', subsetE)).
% 3.16/0.79 thf(subset2powerset, axiom, ((subset2powerset)<=>![X4:$i, X5:$i]:(((subset @ X4 @ X5)=>(in @ X4 @ (powerset @ X5))))), file('/export/starexec/sandbox/tmp/tmp.0juZloQVyw/E---3.1_756803.p', subset2powerset)).
% 3.16/0.79 thf(setadjoinSub2, axiom, ((setadjoinSub2)<=>![X4:$i, X2:$i, X5:$i]:(((subset @ X4 @ X5)=>(subset @ X4 @ (setadjoin @ X2 @ X5))))), file('/export/starexec/sandbox/tmp/tmp.0juZloQVyw/E---3.1_756803.p', setadjoinSub2)).
% 3.16/0.79 thf(setadjoinSub, axiom, ((setadjoinSub)<=>![X2:$i, X4:$i]:((subset @ X4 @ (setadjoin @ X2 @ X4)))), file('/export/starexec/sandbox/tmp/tmp.0juZloQVyw/E---3.1_756803.p', setadjoinSub)).
% 3.16/0.79 thf(subsetTrans, axiom, ((subsetTrans)<=>![X4:$i, X5:$i, X7:$i]:(((subset @ X4 @ X5)=>((subset @ X5 @ X7)=>(subset @ X4 @ X7))))), file('/export/starexec/sandbox/tmp/tmp.0juZloQVyw/E---3.1_756803.p', subsetTrans)).
% 3.16/0.79 thf(powersetE1, axiom, ((powersetE1)<=>![X4:$i, X5:$i]:(((in @ X5 @ (powerset @ X4))=>(subset @ X5 @ X4)))), file('/export/starexec/sandbox/tmp/tmp.0juZloQVyw/E---3.1_756803.p', powersetE1)).
% 3.16/0.79 thf(binunionIR, axiom, ((binunionIR)<=>![X4:$i, X5:$i, X2:$i]:(((in @ X2 @ X5)=>(in @ X2 @ (binunion @ X4 @ X5))))), file('/export/starexec/sandbox/tmp/tmp.0juZloQVyw/E---3.1_756803.p', binunionIR)).
% 3.16/0.79 thf(upairset2IR, axiom, ((upairset2IR)<=>![X2:$i, X3:$i]:((in @ X3 @ (setadjoin @ X2 @ (setadjoin @ X3 @ emptyset))))), file('/export/starexec/sandbox/tmp/tmp.0juZloQVyw/E---3.1_756803.p', upairset2IR)).
% 3.16/0.79 thf(binunionIL, axiom, ((binunionIL)<=>![X4:$i, X5:$i, X2:$i]:(((in @ X2 @ X4)=>(in @ X2 @ (binunion @ X4 @ X5))))), file('/export/starexec/sandbox/tmp/tmp.0juZloQVyw/E---3.1_756803.p', binunionIL)).
% 3.16/0.79 thf(powersetsubset, axiom, ((powersetsubset)<=>![X4:$i, X5:$i]:(((subset @ X4 @ X5)=>(subset @ (powerset @ X4) @ (powerset @ X5))))), file('/export/starexec/sandbox/tmp/tmp.0juZloQVyw/E---3.1_756803.p', powersetsubset)).
% 3.16/0.79 thf(inPowerset, axiom, ((inPowerset)<=>![X4:$i]:((in @ X4 @ (powerset @ X4)))), file('/export/starexec/sandbox/tmp/tmp.0juZloQVyw/E---3.1_756803.p', inPowerset)).
% 3.16/0.79 thf(binunionE, axiom, ((binunionE)<=>![X4:$i, X5:$i, X2:$i]:(((in @ X2 @ (binunion @ X4 @ X5))=>((in @ X2 @ X4)|(in @ X2 @ X5))))), file('/export/starexec/sandbox/tmp/tmp.0juZloQVyw/E---3.1_756803.p', binunionE)).
% 3.16/0.79 thf(binunionLsub, axiom, ((binunionLsub)<=>![X4:$i, X5:$i]:((subset @ X4 @ (binunion @ X4 @ X5)))), file('/export/starexec/sandbox/tmp/tmp.0juZloQVyw/E---3.1_756803.p', binunionLsub)).
% 3.16/0.79 thf(binunionRsub, axiom, ((binunionRsub)<=>![X4:$i, X5:$i]:((subset @ X5 @ (binunion @ X4 @ X5)))), file('/export/starexec/sandbox/tmp/tmp.0juZloQVyw/E---3.1_756803.p', binunionRsub)).
% 3.16/0.79 thf(binintersectI, axiom, ((binintersectI)<=>![X4:$i, X5:$i, X2:$i]:(((in @ X2 @ X4)=>((in @ X2 @ X5)=>(in @ X2 @ (binintersect @ X4 @ X5)))))), file('/export/starexec/sandbox/tmp/tmp.0juZloQVyw/E---3.1_756803.p', binintersectI)).
% 3.16/0.79 thf(binunionEcases, axiom, ((binunionEcases)<=>![X4:$i, X5:$i, X2:$i, X19:$o]:(((in @ X2 @ (binunion @ X4 @ X5))=>(((in @ X2 @ X4)=>(X19))=>(((in @ X2 @ X5)=>(X19))=>(X19)))))), file('/export/starexec/sandbox/tmp/tmp.0juZloQVyw/E---3.1_756803.p', binunionEcases)).
% 3.16/0.79 thf(notinemptyset, axiom, ((notinemptyset)<=>![X2:$i]:(~((in @ X2 @ emptyset)))), file('/export/starexec/sandbox/tmp/tmp.0juZloQVyw/E---3.1_756803.p', notinemptyset)).
% 3.16/0.79 thf(emptysetimpfalse, axiom, ((emptysetimpfalse)<=>![X2:$i]:(((in @ X2 @ emptyset)=>~($true)))), file('/export/starexec/sandbox/tmp/tmp.0juZloQVyw/E---3.1_756803.p', emptysetimpfalse)).
% 3.16/0.79 thf(emptysetE, axiom, ((emptysetE)<=>![X2:$i]:(((in @ X2 @ emptyset)=>![X11:$o]:((X11))))), file('/export/starexec/sandbox/tmp/tmp.0juZloQVyw/E---3.1_756803.p', emptysetE)).
% 3.16/0.79 thf(prop2setE, axiom, ((prop2setE)<=>![X10:$o, X2:$i]:(((in @ X2 @ (prop2set @ ((X10))))=>(X10)))), file('/export/starexec/sandbox/tmp/tmp.0juZloQVyw/E---3.1_756803.p', prop2setE)).
% 3.16/0.79 thf(wellorderingAx, axiom, ((wellorderingAx)<=>![X4:$i]:(?[X5:$i]:((((![X7:$i]:(((in @ X7 @ X5)=>![X2:$i]:(((in @ X2 @ X7)=>(in @ X2 @ X4)))))&![X2:$i, X3:$i]:((((in @ X2 @ X4)&(in @ X3 @ X4))=>(![X7:$i]:(((in @ X7 @ X5)=>((in @ X2 @ X7)<=>(in @ X3 @ X7))))=>((X2)=(X3))))))&![X7:$i, X8:$i]:((((in @ X7 @ X5)&(in @ X8 @ X5))=>(![X2:$i]:(((in @ X2 @ X7)=>(in @ X2 @ X8)))|![X2:$i]:(((in @ X2 @ X8)=>(in @ X2 @ X7)))))))&![X7:$i]:(((![X2:$i]:(((in @ X2 @ X7)=>(in @ X2 @ X4)))&?[X2:$i]:((in @ X2 @ X7)))=>?[X8:$i, X2:$i]:(((((in @ X8 @ X5)&(in @ X2 @ X7))&~(?[X3:$i]:(((in @ X3 @ X8)&(in @ X3 @ X7)))))&![X9:$i]:(((in @ X9 @ X5)=>(![X3:$i]:(((in @ X3 @ X9)=>(in @ X3 @ X8)))|(in @ X2 @ X9)))))))))))), file('/export/starexec/sandbox/tmp/tmp.0juZloQVyw/E---3.1_756803.p', wellorderingAx)).
% 3.16/0.79 thf(foundationAx, axiom, ((foundationAx)<=>![X4:$i]:((?[X2:$i]:((in @ X2 @ X4))=>?[X5:$i]:(((in @ X5 @ X4)&~(?[X2:$i]:(((in @ X2 @ X5)&(in @ X2 @ X4))))))))), file('/export/starexec/sandbox/tmp/tmp.0juZloQVyw/E---3.1_756803.p', foundationAx)).
% 3.16/0.79 thf(omegaIndAx, axiom, ((omegaIndAx)<=>![X4:$i]:((((in @ emptyset @ X4)&![X2:$i]:((((in @ X2 @ omega)&(in @ X2 @ X4))=>(in @ (setadjoin @ X2 @ X2) @ X4))))=>![X2:$i]:(((in @ X2 @ omega)=>(in @ X2 @ X4)))))), file('/export/starexec/sandbox/tmp/tmp.0juZloQVyw/E---3.1_756803.p', omegaIndAx)).
% 3.16/0.79 thf(omegaSAx, axiom, ((omegaSAx)<=>![X2:$i]:(((in @ X2 @ omega)=>(in @ (setadjoin @ X2 @ X2) @ omega)))), file('/export/starexec/sandbox/tmp/tmp.0juZloQVyw/E---3.1_756803.p', omegaSAx)).
% 3.16/0.79 thf(omega0Ax, axiom, ((omega0Ax)<=>(in @ emptyset @ omega)), file('/export/starexec/sandbox/tmp/tmp.0juZloQVyw/E---3.1_756803.p', omega0Ax)).
% 3.16/0.79 thf(setunionAx, axiom, ((setunionAx)<=>![X4:$i, X2:$i]:(((in @ X2 @ (setunion @ X4))<=>?[X5:$i]:(((in @ X2 @ X5)&(in @ X5 @ X4)))))), file('/export/starexec/sandbox/tmp/tmp.0juZloQVyw/E---3.1_756803.p', setunionAx)).
% 3.16/0.79 thf(powersetAx, axiom, ((powersetAx)<=>![X4:$i, X5:$i]:(((in @ X5 @ (powerset @ X4))<=>![X2:$i]:(((in @ X2 @ X5)=>(in @ X2 @ X4)))))), file('/export/starexec/sandbox/tmp/tmp.0juZloQVyw/E---3.1_756803.p', powersetAx)).
% 3.16/0.79 thf(setadjoinAx, axiom, ((setadjoinAx)<=>![X2:$i, X4:$i, X3:$i]:(((in @ X3 @ (setadjoin @ X2 @ X4))<=>(((X3)=(X2))|(in @ X3 @ X4))))), file('/export/starexec/sandbox/tmp/tmp.0juZloQVyw/E---3.1_756803.p', setadjoinAx)).
% 3.16/0.79 thf(emptysetAx, axiom, ((emptysetAx)<=>![X2:$i]:(~((in @ X2 @ emptyset)))), file('/export/starexec/sandbox/tmp/tmp.0juZloQVyw/E---3.1_756803.p', emptysetAx)).
% 3.16/0.79 thf(setextAx, axiom, ((setextAx)<=>![X4:$i, X5:$i]:((![X2:$i]:(((in @ X2 @ X4)<=>(in @ X2 @ X5)))=>((X4)=(X5))))), file('/export/starexec/sandbox/tmp/tmp.0juZloQVyw/E---3.1_756803.p', setextAx)).
% 3.16/0.79 thf(c_0_134, 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)=>((binunionEcases)=>((binunionE)=>((binunionLsub)=>((binunionRsub)=>((binintersectI)=>((binintersectSubset5)=>((binintersectEL)=>((binintersectLsub)=>((binintersectSubset2)=>((binintersectSubset3)=>((binintersectER)=>((disjointsetsI1)=>((binintersectRsub)=>((binintersectSubset4)=>((binintersectSubset1)=>((bs114d)=>((setminusI)=>((setminusEL)=>((setminusER)=>((setminusSubset2)=>((setminusERneg)=>((setminusELneg)=>((setminusILneg)=>((setminusIRneg)=>((setminusLsub)=>((setminusSubset1)=>((symdiffE)=>((symdiffI1)=>((symdiffI2)=>((symdiffIneg1)=>((symdiffIneg2)=>((secondinupair)=>((setukpairIL)=>![X2:$i, X3:$i]:((in @ X3 @ (setunion @ (setadjoin @ (setadjoin @ X2 @ emptyset) @ (setadjoin @ (setadjoin @ X2 @ (setadjoin @ X3 @ emptyset)) @ emptyset)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))), inference(assume_negation,[status(cth)],[setukpairIR])).
% 3.16/0.79 thf(c_0_135, plain, ((nonemptyI)<=>![X4:$i, X1:$i > $o, X2:$i]:(((in @ X2 @ X4)=>((X1 @ X2)=>(nonempty @ (dsetconstr @ X4 @ (^[Z0:$i]:((X1 @ Z0))))))))), inference(fof_simplification,[status(thm)],[nonemptyI])).
% 3.16/0.79 thf(c_0_136, plain, ((setbeta)<=>![X4:$i, X1:$i > $o, X2:$i]:(((in @ X2 @ X4)=>((in @ X2 @ (dsetconstr @ X4 @ (^[Z0:$i]:((X1 @ Z0)))))<=>(X1 @ X2))))), inference(fof_simplification,[status(thm)],[setbeta])).
% 3.16/0.79 thf(c_0_137, plain, ((setoftrueEq)<=>![X4:$i]:(((dsetconstr @ X4 @ (^[Z0:$i]:(($true))))=(X4)))), inference(fof_simplification,[status(thm)],[setoftrueEq])).
% 3.16/0.79 thf(c_0_138, plain, ((exuE2)<=>![X1:$i > $o]:(((exu @ (^[Z0:$i]:((X1 @ Z0))))=>?[X2:$i]:(![X3:$i]:(((X1 @ X3)<=>((X3)=(X2)))))))), inference(fof_simplification,[status(thm)],[exuE2])).
% 3.16/0.79 thf(c_0_139, plain, ((emptyE1)<=>![X4:$i, X1:$i > $o]:((?[X2:$i]:(((in @ X2 @ X4)&(X1 @ X2)))=>(((dsetconstr @ X4 @ (^[Z0:$i]:((X1 @ Z0))))=(emptyset))=>~($true))))), inference(fof_simplification,[status(thm)],[emptyE1])).
% 3.16/0.79 thf(c_0_140, plain, ((exuI1)<=>![X1:$i > $o]:((?[X2:$i]:(((X1 @ X2)&![X3:$i]:(((X1 @ X3)=>((X2)=(X3))))))=>(exu @ (^[Z0:$i]:((X1 @ Z0))))))), inference(fof_simplification,[status(thm)],[exuI1])).
% 3.16/0.79 thf(c_0_141, plain, ((exuI3)<=>![X1:$i > $o]:((?[X2:$i]:((X1 @ X2))=>(![X2:$i, X3:$i]:(((X1 @ X2)=>((X1 @ X3)=>((X2)=(X3)))))=>(exu @ (^[Z0:$i]:((X1 @ Z0)))))))), inference(fof_simplification,[status(thm)],[exuI3])).
% 3.16/0.79 thf(c_0_142, plain, ((exu__Cong)<=>![X1:$i > $o, X17:$i > $o]:((![X2:$i, X3:$i]:((((X2)=(X3))=>((X1 @ X2)<=>(X17 @ X3))))=>((exu @ (^[Z0:$i]:((X1 @ Z0))))<=>(exu @ (^[Z0:$i]:((X17 @ Z0)))))))), inference(fof_simplification,[status(thm)],[exu__Cong])).
% 3.16/0.79 thf(c_0_143, plain, ((exuE3u)<=>![X1:$i > $o]:(((exu @ (^[Z0:$i]:((X1 @ Z0))))=>![X2:$i, X3:$i]:(((X1 @ X2)=>((X1 @ X3)=>((X2)=(X3)))))))), inference(fof_simplification,[status(thm)],[exuE3u])).
% 3.16/0.79 thf(c_0_144, plain, ((exuI2)<=>![X1:$i > $o]:((?[X2:$i]:(![X3:$i]:(((X1 @ X3)<=>((X3)=(X2)))))=>(exu @ (^[Z0:$i]:((X1 @ Z0))))))), inference(fof_simplification,[status(thm)],[exuI2])).
% 3.16/0.79 thf(c_0_145, plain, ((dsetconstr__Cong)<=>![X4:$i, X5:$i]:((((X4)=(X5))=>![X1:$i > $o, X17:$i > $o]:((![X2:$i]:(((in @ X2 @ X4)=>![X3:$i]:(((in @ X3 @ X5)=>(((X2)=(X3))=>((X1 @ X2)<=>(X17 @ X3)))))))=>((dsetconstr @ X4 @ (^[Z0:$i]:((X1 @ Z0))))=(dsetconstr @ X5 @ (^[Z0:$i]:((X17 @ Z0)))))))))), inference(fof_simplification,[status(thm)],[dsetconstr__Cong])).
% 3.16/0.79 thf(c_0_146, plain, ((descr__Cong)<=>![X1:$i > $o, X17:$i > $o]:((![X2:$i, X3:$i]:((((X2)=(X3))=>((X1 @ X2)<=>(X17 @ X3))))=>((exu @ (^[Z0:$i]:((X1 @ Z0))))=>((exu @ (^[Z0:$i]:((X17 @ Z0))))=>((descr @ (^[Z0:$i]:((X1 @ Z0))))=(descr @ (^[Z0:$i]:((X17 @ Z0)))))))))), inference(fof_simplification,[status(thm)],[descr__Cong])).
% 3.16/0.79 thf(c_0_147, plain, ((exuEu)<=>![X1:$i > $o]:(((exu @ (^[Z0:$i]:((X1 @ Z0))))=>![X2:$i, X3:$i]:(((X1 @ X2)=>((X1 @ X3)=>((X2)=(X3)))))))), inference(fof_simplification,[status(thm)],[exuEu])).
% 3.16/0.79 thf(c_0_148, plain, ((sepSubset)<=>![X4:$i, X1:$i > $o]:((subset @ (dsetconstr @ X4 @ (^[Z0:$i]:((X1 @ Z0)))) @ X4))), inference(fof_simplification,[status(thm)],[sepSubset])).
% 3.16/0.79 thf(c_0_149, plain, ((sepInPowerset)<=>![X4:$i, X1:$i > $o]:((in @ (dsetconstr @ X4 @ (^[Z0:$i]:((X1 @ Z0)))) @ (powerset @ X4)))), inference(fof_simplification,[status(thm)],[sepInPowerset])).
% 3.16/0.79 thf(c_0_150, plain, ((exuE3e)<=>![X1:$i > $o]:(((exu @ (^[Z0:$i]:((X1 @ Z0))))=>?[X2:$i]:((X1 @ X2))))), inference(fof_simplification,[status(thm)],[exuE3e])).
% 3.16/0.79 thf(c_0_151, plain, ((exuE1)<=>![X1:$i > $o]:(((exu @ (^[Z0:$i]:((X1 @ Z0))))=>?[X2:$i]:(((X1 @ X2)&![X3:$i]:(((X1 @ X3)=>((X2)=(X3))))))))), inference(fof_simplification,[status(thm)],[exuE1])).
% 3.16/0.79 thf(c_0_152, plain, ((dsetconstrER)<=>![X4:$i, X1:$i > $o, X2:$i]:(((in @ X2 @ (dsetconstr @ X4 @ (^[Z0:$i]:((X1 @ Z0)))))=>(X1 @ X2)))), inference(fof_simplification,[status(thm)],[dsetconstrER])).
% 3.16/0.79 thf(c_0_153, plain, ((dsetconstrEL)<=>![X4:$i, X1:$i > $o, X2:$i]:(((in @ X2 @ (dsetconstr @ X4 @ (^[Z0:$i]:((X1 @ Z0)))))=>(in @ X2 @ X4)))), inference(fof_simplification,[status(thm)],[dsetconstrEL])).
% 3.16/0.79 thf(c_0_154, plain, ((dsetconstrI)<=>![X4:$i, X1:$i > $o, X2:$i]:(((in @ X2 @ X4)=>((X1 @ X2)=>(in @ X2 @ (dsetconstr @ X4 @ (^[Z0:$i]:((X1 @ Z0))))))))), inference(fof_simplification,[status(thm)],[dsetconstrI])).
% 3.16/0.79 thf(c_0_155, plain, ((descrp)<=>![X1:$i > $o]:(((exu @ (^[Z0:$i]:((X1 @ Z0))))=>(X1 @ (descr @ (^[Z0:$i]:((X1 @ Z0)))))))), inference(fof_simplification,[status(thm)],[descrp])).
% 3.16/0.79 thf(c_0_156, plain, ((replAx)<=>![X6:$i > $i > $o, X4:$i]:((![X2:$i]:(((in @ X2 @ X4)=>(exu @ (^[Z0:$i]:((X6 @ X2 @ Z0))))))=>?[X5:$i]:(![X2:$i]:(((in @ X2 @ X5)<=>?[X3:$i]:(((in @ X3 @ X4)&(X6 @ X3 @ X2))))))))), inference(fof_simplification,[status(thm)],[replAx])).
% 3.16/0.79 thf(c_0_157, plain, ((epred1_0)<=>![X407:$i]:(?[X408:$i]:((((![X409:$i]:(((in @ X409 @ X408)=>![X410:$i]:(((in @ X410 @ X409)=>(in @ X410 @ X407)))))&![X411:$i, X412:$i]:((((in @ X411 @ X407)&(in @ X412 @ X407))=>(![X413:$i]:(((in @ X413 @ X408)=>((in @ X411 @ X413)<=>(in @ X412 @ X413))))=>((X411)=(X412))))))&![X414:$i, X415:$i]:((((in @ X414 @ X408)&(in @ X415 @ X408))=>(![X416:$i]:(((in @ X416 @ X414)=>(in @ X416 @ X415)))|![X417:$i]:(((in @ X417 @ X415)=>(in @ X417 @ X414)))))))&![X418:$i]:(((![X419:$i]:(((in @ X419 @ X418)=>(in @ X419 @ X407)))&?[X420:$i]:((in @ X420 @ X418)))=>?[X421:$i, X422:$i]:(((((in @ X421 @ X408)&(in @ X422 @ X418))&~(?[X423:$i]:(((in @ X423 @ X421)&(in @ X423 @ X418)))))&![X424:$i]:(((in @ X424 @ X408)=>(![X425:$i]:(((in @ X425 @ X424)=>(in @ X425 @ X421)))|(in @ X422 @ X424)))))))))))), introduced(definition)).
% 3.16/0.79 thf(c_0_158, negated_conjecture, ~((![X380:$i, X381:$i]:((![X382:$i]:(((in @ X382 @ X380)<=>(in @ X382 @ X381)))=>((X380)=(X381))))=>(![X383:$i]:(~(in @ X383 @ emptyset))=>(![X384:$i, X385:$i, X386:$i]:(((in @ X386 @ (setadjoin @ X384 @ X385))<=>(((X386)=(X384))|(in @ X386 @ X385))))=>(![X387:$i, X388:$i]:(((in @ X388 @ (powerset @ X387))<=>![X389:$i]:(((in @ X389 @ X388)=>(in @ X389 @ X387)))))=>(![X390:$i, X391:$i]:(((in @ X391 @ (setunion @ X390))<=>?[X392:$i]:(((in @ X391 @ X392)&(in @ X392 @ X390)))))=>((in @ emptyset @ omega)=>(![X393:$i]:(((in @ X393 @ omega)=>(in @ (setadjoin @ X393 @ X393) @ omega)))=>(![X394:$i]:((((in @ emptyset @ X394)&![X395:$i]:((((in @ X395 @ omega)&(in @ X395 @ X394))=>(in @ (setadjoin @ X395 @ X395) @ X394))))=>![X396:$i]:(((in @ X396 @ omega)=>(in @ X396 @ X394)))))=>(![X397:$i > $i > $o, X398:$i]:((![X399:$i]:(((in @ X399 @ X398)=>(exu @ (X397 @ X399))))=>?[X400:$i]:(![X401:$i]:(((in @ X401 @ X400)<=>?[X402:$i]:(((in @ X402 @ X398)&(X397 @ X402 @ X401))))))))=>(![X403:$i]:((?[X404:$i]:((in @ X404 @ X403))=>?[X405:$i]:(((in @ X405 @ X403)&~(?[X406:$i]:(((in @ X406 @ X405)&(in @ X406 @ X403))))))))=>((epred1_0)=>(![X426:$i > $o]:(((exu @ X426)=>(X426 @ (descr @ (^[Z0:$i]:(X426 @ Z0))))))=>(![X427:$i, X428:$i > $o, X429:$i]:(((in @ X429 @ X427)=>((X428 @ X429)=>(in @ X429 @ (dsetconstr @ X427 @ X428)))))=>(![X430:$i, X431:$i > $o, X432:$i]:(((in @ X432 @ (dsetconstr @ X430 @ X431))=>(in @ X432 @ X430)))=>(![X433:$i, X434:$i > $o, X435:$i]:(((in @ X435 @ (dsetconstr @ X433 @ X434))=>(X434 @ X435)))=>(![X436:$i > $o]:(((exu @ X436)=>?[X437:$i]:(((X436 @ X437)&![X438:$i]:(((X436 @ X438)=>((X437)=(X438))))))))=>(![X439:$o, X440:$i]:(((in @ X440 @ (prop2set @ ((X439))))=>(X439)))=>(![X441:$i]:(((in @ X441 @ emptyset)=>![X442:$o]:((X442))))=>(![X443:$i]:(((in @ X443 @ emptyset)=>~($true)))=>(![X444:$i]:(~(in @ X444 @ emptyset))=>(![X445:$i > $o]:(((exu @ X445)=>?[X446:$i]:((X445 @ X446))))=>(![X447:$i, X448:$i]:((![X449:$i]:(((in @ X449 @ X447)=>(in @ X449 @ X448)))=>(![X450:$i]:(((in @ X450 @ X448)=>(in @ X450 @ X447)))=>((X447)=(X448)))))=>(![X451:$i]:((![X452:$i]:(~(in @ X452 @ X451))=>((X451)=(emptyset))))=>(![X453:$i]:((![X454:$i]:(~(in @ X454 @ X453))=>((X453)=(emptyset))))=>(![X455:$i, X456:$i > $o, X457:$i]:(((in @ X457 @ X455)=>((in @ X457 @ (dsetconstr @ X455 @ X456))<=>(X456 @ X457))))=>(![X458:$i]:(((nonempty @ X458)=>?[X459:$i]:((in @ X459 @ X458))))=>(![X460:$i, X461:$i > $o, X462:$i]:(((in @ X462 @ X460)=>((X461 @ X462)=>(nonempty @ (dsetconstr @ X460 @ X461)))))=>(![X463:$i]:((?[X464:$i]:((in @ X464 @ X463))=>(nonempty @ X463)))=>(![X465:$i, X466:$i]:((in @ X465 @ (setadjoin @ X465 @ X466)))=>((in @ emptyset @ (setadjoin @ emptyset @ emptyset))=>(![X467:$i, X468:$i, X469:$i]:(((in @ X469 @ X468)=>(in @ X469 @ (setadjoin @ X467 @ X468))))=>(![X470:$i, X471:$i, X472:$i]:(((in @ X472 @ (setadjoin @ X470 @ X471))=>![X473:$o]:(((((X472)=(X470))=>(X473))=>(((in @ X472 @ X471)=>(X473))=>(X473))))))=>(![X474:$i, X475:$i, X476:$i]:(((in @ X476 @ (setadjoin @ X474 @ X475))=>(((X476)=(X474))|(in @ X476 @ X475))))=>(![X477:$i]:(((dsetconstr @ X477 @ (^[Z0:$i]:($true)))=(X477)))=>(![X478:$i, X479:$i]:((![X480:$i]:(((in @ X480 @ X479)=>(in @ X480 @ X478)))=>(in @ X479 @ (powerset @ X478))))=>(![X481:$i]:((in @ emptyset @ (powerset @ X481)))=>(![X482:$i]:((in @ emptyset @ (powerset @ X482)))=>(![X483:$i, X484:$i, X485:$i]:(((in @ X484 @ (powerset @ X483))=>((in @ X485 @ X484)=>(in @ X485 @ X483))))=>(![X486:$i, X487:$i, X488:$i]:(((in @ X487 @ X488)=>((in @ X488 @ X486)=>(in @ X487 @ (setunion @ X486)))))=>(![X489:$i, X490:$i]:(((in @ X490 @ (setunion @ X489))=>![X491:$o]:((![X492:$i]:(((in @ X490 @ X492)=>((in @ X492 @ X489)=>(X491))))=>(X491)))))=>(![X493:$i, X494:$i]:(((in @ X494 @ X493)=>(in @ X494 @ (powerset @ (setunion @ X493)))))=>(![X495:$i > $o]:(((exu @ X495)=>?[X496:$i]:(![X497:$i]:(((X495 @ X497)<=>((X497)=(X496)))))))=>(![X498:$i]:(((nonempty @ X498)=>?[X499:$i]:(((in @ X499 @ X498)&$true))))=>(![X500:$i, X501:$i]:(((in @ X500 @ (setadjoin @ X501 @ emptyset))=>((X500)=(X501))))=>(![X502:$i, X503:$i]:((((X502)!=(X503))=>~(in @ X503 @ (setadjoin @ X502 @ emptyset))))=>(![X504:$i, X505:$i]:((((X504)=(X505))=>(in @ X504 @ (setadjoin @ X505 @ emptyset))))=>(![X506:$i, X507:$i]:(((in @ X506 @ (setadjoin @ X507 @ emptyset))=>(in @ X507 @ (setadjoin @ X506 @ emptyset))))=>(![X508:$i, X509:$i, X510:$i]:(((in @ X510 @ (setadjoin @ X508 @ (setadjoin @ X509 @ emptyset)))=>(((X510)=(X508))|((X510)=(X509)))))=>(![X511:$i, X512:$i]:((in @ X511 @ (setadjoin @ X511 @ (setadjoin @ X512 @ emptyset))))=>(![X513:$i, X514:$i]:((in @ X514 @ (setadjoin @ X513 @ (setadjoin @ X514 @ emptyset))))=>(![X515:$i, X516:$i > $o]:((?[X517:$i]:(((in @ X517 @ X515)&(X516 @ X517)))=>(((dsetconstr @ X515 @ X516)=(emptyset))=>~($true))))=>(![X518:$i > $o, X519:$i]:(((in @ X519 @ emptyset)=>(X518 @ X519)))=>(![X520:$i, X521:$i > $o]:((~(![X522:$i]:(((in @ X522 @ X520)=>(X521 @ X522))))=>?[X523:$i]:(((in @ X523 @ X520)&~((X521 @ X523))))))=>(![X524:$i, X525:$i > $o]:((![X526:$i]:(((in @ X526 @ X524)=>~((X525 @ X526))))=>~(?[X527:$i]:(((in @ X527 @ X524)&(X525 @ X527))))))=>(![X528:$i, X529:$i > $o]:((~(?[X530:$i]:(((in @ X530 @ X528)&(X529 @ X530))))=>![X531:$i]:(((in @ X531 @ X528)=>~((X529 @ X531))))))=>(![X532:$i, X533:$i > $o]:((?[X534:$i]:(((in @ X534 @ X532)&~((X533 @ X534))))=>~(![X535:$i]:(((in @ X535 @ X532)=>(X533 @ X535))))))=>(![X536:$o]:(((X536)=>(in @ emptyset @ (prop2set @ ((X536))))))=>((prop2set2propI)=>(![X537:$i, X538:$i > $o]:((~(?[X539:$i]:(((in @ X539 @ X537)&(X538 @ X539))))=>![X540:$i]:(((in @ X540 @ X537)=>~((X538 @ X540))))))=>(![X541:$i, X542:$i > $o]:((~(![X543:$i]:(((in @ X543 @ X541)=>(X542 @ X543))))=>?[X544:$i]:(((in @ X544 @ X541)&~((X542 @ X544))))))=>(![X545:$i > $o]:((?[X546:$i]:(((X545 @ X546)&![X547:$i]:(((X545 @ X547)=>((X546)=(X547))))))=>(exu @ X545)))=>(![X548:$i > $o]:((?[X549:$i]:((X548 @ X549))=>(![X550:$i, X551:$i]:(((X548 @ X550)=>((X548 @ X551)=>((X550)=(X551)))))=>(exu @ X548))))=>(![X552:$i > $o]:((?[X553:$i]:(![X554:$i]:(((X552 @ X554)<=>((X554)=(X553)))))=>(exu @ X552)))=>(![X555:$i, X556:$i]:((((X555)=(X556))=>![X557:$i, X558:$i]:((((X557)=(X558))=>((in @ X557 @ X555)=>(in @ X558 @ X556))))))=>(![X559:$i, X560:$i]:((((X559)=(X560))=>![X561:$i, X562:$i]:((((X561)=(X562))=>((in @ X561 @ X559)<=>(in @ X562 @ X560))))))=>(![X563:$i > $o]:(((exu @ X563)=>![X564:$i, X565:$i]:(((X563 @ X564)=>((X563 @ X565)=>((X564)=(X565)))))))=>(![X566:$i > $o, X567:$i > $o]:((![X568:$i, X569:$i]:((((X568)=(X569))=>((X566 @ X568)<=>(X567 @ X569))))=>((exu @ X566)<=>(exu @ X567))))=>(((emptyset)=(emptyset))=>(![X570:$i, X571:$i]:((((X570)=(X571))=>![X572:$i, X573:$i]:((((X572)=(X573))=>((setadjoin @ X570 @ X572)=(setadjoin @ X571 @ X573))))))=>(![X574:$i, X575:$i]:((((X574)=(X575))=>((powerset @ X574)=(powerset @ X575))))=>(![X576:$i, X577:$i]:((((X576)=(X577))=>((setunion @ X576)=(setunion @ X577))))=>(((omega)=(omega))=>(![X578:$i > $o]:(((exu @ X578)=>![X579:$i, X580:$i]:(((X578 @ X579)=>((X578 @ X580)=>((X579)=(X580)))))))=>(![X581:$i > $o, X582:$i > $o]:((![X583:$i, X584:$i]:((((X583)=(X584))=>((X581 @ X583)<=>(X582 @ X584))))=>((exu @ X581)=>((exu @ X582)=>((descr @ X581)=(descr @ X582))))))=>(![X585:$i, X586:$i]:((((X585)=(X586))=>![X587:$i > $o, X588:$i > $o]:((![X589:$i]:(((in @ X589 @ X585)=>![X590:$i]:(((in @ X590 @ X586)=>(((X589)=(X590))=>((X587 @ X589)<=>(X588 @ X590)))))))=>((dsetconstr @ X585 @ X587)=(dsetconstr @ X586 @ X588))))))=>(![X591:$i, X592:$i]:((![X593:$i]:(((in @ X593 @ X591)=>(in @ X593 @ X592)))=>(subset @ X591 @ X592)))=>(![X594:$i, X595:$i]:((((X594)=(X595))=>(subset @ X595 @ X594)))=>(![X596:$i, X597:$i]:((((X596)=(X597))=>(subset @ X596 @ X597)))=>(![X598:$i, X599:$i]:((![X600:$i]:(((in @ X600 @ X598)=>(in @ X600 @ X599)))=>(subset @ X598 @ X599)))=>(![X601:$i]:((subset @ emptyset @ X601))=>(![X602:$i, X603:$i, X604:$i]:(((subset @ X602 @ X603)=>((in @ X604 @ X602)=>(in @ X604 @ X603))))=>(![X605:$i, X606:$i, X607:$i]:(((subset @ X605 @ X606)=>(~(in @ X607 @ X606)=>~(in @ X607 @ X605))))=>(![X608:$i, X609:$i, X610:$i]:(((in @ X610 @ X608)=>(~(in @ X610 @ X609)=>~(subset @ X608 @ X609))))=>(![X611:$i, X612:$i]:((~(subset @ X611 @ X612)=>((X611)!=(X612))))=>(![X613:$i, X614:$i, X615:$i]:(((in @ X615 @ X613)=>(~(in @ X615 @ X614)=>((X613)!=(X614)))))=>(![X616:$i]:((subset @ X616 @ X616))=>(![X617:$i, X618:$i, X619:$i]:(((subset @ X617 @ X618)=>((subset @ X618 @ X619)=>(subset @ X617 @ X619))))=>(![X620:$i, X621:$i]:((subset @ X621 @ (setadjoin @ X620 @ X621)))=>(![X622:$i, X623:$i, X624:$i]:(((subset @ X622 @ X624)=>(subset @ X622 @ (setadjoin @ X623 @ X624))))=>(![X625:$i, X626:$i]:(((subset @ X625 @ X626)=>(in @ X625 @ (powerset @ X626))))=>(![X627:$i, X628:$i]:(((subset @ X627 @ X628)=>((subset @ X628 @ X627)=>((X627)=(X628)))))=>(![X629:$i]:(((subset @ X629 @ emptyset)=>((X629)=(emptyset))))=>(![X630:$i, X631:$i]:(((subset @ X631 @ X630)=>(in @ X631 @ (powerset @ X630))))=>(![X632:$i, X633:$i]:(((in @ X633 @ (powerset @ X632))=>(subset @ X633 @ X632)))=>(![X634:$i]:((in @ X634 @ (powerset @ X634)))=>(![X635:$i, X636:$i]:(((subset @ X635 @ X636)=>(subset @ (powerset @ X635) @ (powerset @ X636))))=>(![X637:$i, X638:$i > $o]:((in @ (dsetconstr @ X637 @ X638) @ (powerset @ X637)))=>(![X639:$i, X640:$i > $o]:((subset @ (dsetconstr @ X639 @ X640) @ X639))=>(![X641:$i, X642:$i, X643:$i]:(((in @ X643 @ X641)=>(in @ X643 @ (binunion @ X641 @ X642))))=>(![X644:$i, X645:$i]:((in @ X645 @ (setadjoin @ X644 @ (setadjoin @ X645 @ emptyset))))=>(![X646:$i, X647:$i, X648:$i]:(((in @ X648 @ X647)=>(in @ X648 @ (binunion @ X646 @ X647))))=>(![X649:$i, X650:$i, X651:$i, X652:$o]:(((in @ X651 @ (binunion @ X649 @ X650))=>(((in @ X651 @ X649)=>(X652))=>(((in @ X651 @ X650)=>(X652))=>(X652)))))=>(![X653:$i, X654:$i, X655:$i]:(((in @ X655 @ (binunion @ X653 @ X654))=>((in @ X655 @ X653)|(in @ X655 @ X654))))=>(![X656:$i, X657:$i]:((subset @ X656 @ (binunion @ X656 @ X657)))=>(![X658:$i, X659:$i]:((subset @ X659 @ (binunion @ X658 @ X659)))=>(![X660:$i, X661:$i, X662:$i]:(((in @ X662 @ X660)=>((in @ X662 @ X661)=>(in @ X662 @ (binintersect @ X660 @ X661)))))=>(![X663:$i, X664:$i, X665:$i]:(((subset @ X665 @ X663)=>((subset @ X665 @ X664)=>(subset @ X665 @ (binintersect @ X663 @ X664)))))=>(![X666:$i, X667:$i, X668:$i]:(((in @ X668 @ (binintersect @ X666 @ X667))=>(in @ X668 @ X666)))=>(![X669:$i, X670:$i]:((subset @ (binintersect @ X669 @ X670) @ X669))=>(![X671:$i, X672:$i]:(((subset @ X671 @ X672)=>((binintersect @ X671 @ X672)=(X671))))=>(![X673:$i, X674:$i]:((((binintersect @ X673 @ X674)=(X674))=>(subset @ X674 @ X673)))=>(![X675:$i, X676:$i, X677:$i]:(((in @ X677 @ (binintersect @ X675 @ X676))=>(in @ X677 @ X676)))=>(![X678:$i, X679:$i]:((~(?[X680:$i]:(((in @ X680 @ X678)&(in @ X680 @ X679))))=>((binintersect @ X678 @ X679)=(emptyset))))=>(![X681:$i, X682:$i]:((subset @ (binintersect @ X681 @ X682) @ X682))=>(![X683:$i, X684:$i]:(((subset @ X684 @ X683)=>((binintersect @ X683 @ X684)=(X684))))=>(![X685:$i, X686:$i]:((((binintersect @ X685 @ X686)=(X685))=>(subset @ X685 @ X686)))=>(![X687:$i, X688:$i, X689:$i]:(((binintersect @ X687 @ (binunion @ X688 @ X689))=(binunion @ (binintersect @ X687 @ X688) @ (binintersect @ X687 @ X689))))=>(![X690:$i, X691:$i, X692:$i]:(((in @ X692 @ X690)=>(~(in @ X692 @ X691)=>(in @ X692 @ (setminus @ X690 @ X691)))))=>(![X693:$i, X694:$i, X695:$i]:(((in @ X695 @ (setminus @ X693 @ X694))=>(in @ X695 @ X693)))=>(![X696:$i, X697:$i, X698:$i]:(((in @ X698 @ (setminus @ X696 @ X697))=>~(in @ X698 @ X697)))=>(![X699:$i, X700:$i]:(((subset @ X699 @ X700)=>((setminus @ X699 @ X700)=(emptyset))))=>(![X701:$i, X702:$i, X703:$i]:((~(in @ X703 @ (setminus @ X701 @ X702))=>((in @ X703 @ X701)=>(in @ X703 @ X702))))=>(![X704:$i, X705:$i, X706:$i]:((~(in @ X706 @ (setminus @ X704 @ X705))=>(~(in @ X706 @ X705)=>~(in @ X706 @ X704))))=>(![X707:$i, X708:$i, X709:$i]:((~(in @ X709 @ X707)=>~(in @ X709 @ (setminus @ X707 @ X708))))=>(![X710:$i, X711:$i, X712:$i]:(((in @ X712 @ X711)=>~(in @ X712 @ (setminus @ X710 @ X711))))=>(![X713:$i, X714:$i]:((subset @ (setminus @ X713 @ X714) @ X713))=>(![X715:$i, X716:$i]:((((setminus @ X715 @ X716)=(emptyset))=>(subset @ X715 @ X716)))=>(![X717:$i, X718:$i, X719:$i]:(((in @ X719 @ (symdiff @ X717 @ X718))=>![X720:$o]:((((in @ X719 @ X717)=>(~(in @ X719 @ X718)=>(X720)))=>((~(in @ X719 @ X717)=>((in @ X719 @ X718)=>(X720)))=>(X720))))))=>(![X721:$i, X722:$i, X723:$i]:(((in @ X723 @ X721)=>(~(in @ X723 @ X722)=>(in @ X723 @ (symdiff @ X721 @ X722)))))=>(![X724:$i, X725:$i, X726:$i]:((~(in @ X726 @ X724)=>((in @ X726 @ X725)=>(in @ X726 @ (symdiff @ X724 @ X725)))))=>(![X727:$i, X728:$i, X729:$i]:(((in @ X729 @ X727)=>((in @ X729 @ X728)=>~(in @ X729 @ (symdiff @ X727 @ X728)))))=>(![X730:$i, X731:$i, X732:$i]:((~(in @ X732 @ X730)=>(~(in @ X732 @ X731)=>~(in @ X732 @ (symdiff @ X730 @ X731)))))=>(![X733:$i, X734:$i]:((in @ X734 @ (setadjoin @ X733 @ (setadjoin @ X734 @ emptyset))))=>(![X735:$i, X736:$i]:((in @ X735 @ (setunion @ (setadjoin @ (setadjoin @ X735 @ emptyset) @ (setadjoin @ (setadjoin @ X735 @ (setadjoin @ X736 @ emptyset)) @ emptyset)))))=>![X2:$i, X3:$i]:((in @ X3 @ (setunion @ (setadjoin @ (setadjoin @ X2 @ emptyset) @ (setadjoin @ (setadjoin @ X2 @ (setadjoin @ X3 @ emptyset)) @ emptyset)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))), inference(apply_def,[status(thm)],[inference(fof_simplification,[status(thm)],[inference(fool_unroll,[status(thm)],[inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[c_0_134, binintersectLsub]), binintersectSubset5]), binintersectEL]), binintersectSubset2]), binintersectSubset3]), binintersectER]), disjointsetsI1]), binintersectRsub]), binintersectSubset4]), nonemptyI1]), binintersectSubset1]), c_0_135]), bs114d]), nonemptyE1]), setminusI]), c_0_136]), setminusEL]), noeltsimpempty]), setminusER]), emptyI]), setminusSubset2]), setext]), setminusERneg]), setadjoinIL]), setminusELneg]), setminusILneg]), setminusIRneg]), setminusLsub]), setminusSubset1]), symdiffE]), symdiffI1]), symdiffI2]), symdiffIneg1]), symdiffIneg2]), secondinupair]), setukpairIL]), emptyinPowerset]), powersetI]), c_0_137]), setadjoinOr]), setadjoinE]), setadjoinIR]), emptyinunitempty]), emptyInPowerset]), uniqinunit]), nonemptyImpWitness]), c_0_138]), subPowSU]), setunionE]), setunionI]), powersetE]), notinsingleton]), emptysetsubset]), subsetI2]), subsetRefl]), powersetI1]), subsetemptysetimpeq]), setextsub]), vacuousDall]), c_0_139]), upairsetIR]), upairsetIL]), upairsetE]), singletonsswitch]), eqinunit]), quantDeMorgan1]), c_0_140]), notdallE]), notdexE]), prop2setI]), quantDeMorgan4]), quantDeMorgan3]), quantDeMorgan2]), c_0_141]), setadjoin__Cong]), emptyset__Cong]), c_0_142]), c_0_143]), in__Cong]), inCongP]), c_0_144]), powerset__Cong]), eqimpsubset2]), subsetI1]), c_0_145]), c_0_146]), c_0_147]), omega__Cong]), setunion__Cong]), eqimpsubset1]), notequalI2]), notequalI1]), notsubsetI]), subsetE2]), subsetE]), subset2powerset]), setadjoinSub2]), setadjoinSub]), subsetTrans]), powersetE1]), binunionIR]), upairset2IR]), binunionIL]), c_0_148]), c_0_149]), powersetsubset]), inPowerset]), binunionE]), binunionLsub]), binunionRsub]), binintersectI]), binunionEcases]), c_0_150]), notinemptyset]), emptysetimpfalse]), emptysetE]), prop2setE]), c_0_151]), c_0_152]), c_0_153]), c_0_154]), c_0_155]), wellorderingAx]), foundationAx]), c_0_156]), omegaIndAx]), omegaSAx]), omega0Ax]), setunionAx]), powersetAx]), setadjoinAx]), emptysetAx]), setextAx])])]), c_0_157])).
% 3.16/0.79 thf(c_0_159, negated_conjecture, ![X737:$i, X738:$i, X740:$i, X741:$i, X742:$i, X743:$i, X744:$i, X745:$i, X746:$i, X747:$i, X748:$i, X750:$i, X751:$i, X753:$i, X754:$i, X755:$i, X756:$i, X757:$i, X759:$i, X760:$i > $i > $o, X761:$i, X764:$i, X766:$i, X767:$i, X768:$i, X769:$i, X771:$i, X772:$i > $o, X773:$i, X774:$i > $o, X775:$i, X776:$i, X777:$i > $o, X778:$i, X779:$i, X780:$i > $o, X781:$i, X782:$i > $o, X784:$i, X785:$o, X786:$i, X787:$i, X788:$o, X789:$i, X790:$i, X791:$i > $o, X793:$i, X794:$i, X797:$i, X799:$i, X801:$i, X802:$i > $o, X803:$i, X804:$i, X806:$i, X807:$i > $o, X808:$i, X809:$i, X810:$i, X811:$i, X812:$i, X813:$i, X814:$i, X815:$i, X816:$i, X817:$i, X818:$i, X819:$o, X820:$i, X821:$i, X822:$i, X823:$i, X824:$i, X825:$i, X827:$i, X828:$i, X829:$i, X830:$i, X831:$i, X832:$i, X833:$i, X834:$i, X835:$i, X836:$i, X837:$o, X839:$i, X840:$i, X841:$i > $o, X843:$i, X844:$i, X845:$i, X847:$i, X848:$i, X849:$i, X850:$i, X851:$i, X852:$i, X853:$i, X854:$i, X855:$i, X856:$i, X857:$i, X858:$i, X859:$i, X860:$i, X861:$i, X862:$i, X863:$i > $o, X864:$i, X865:$i > $o, X866:$i, X867:$i, X868:$i > $o, X869:$i, X871:$i, X872:$i > $o, X874:$i, X875:$i, X876:$i > $o, X878:$i, X879:$i, X880:$i > $o, X881:$i, X883:$o, X884:$i, X885:$i > $o, X887:$i, X888:$i, X889:$i > $o, X890:$i, X892:$i > $o, X893:$i, X895:$i > $o, X896:$i, X899:$i > $o, X900:$i, X902:$i, X903:$i, X904:$i, X905:$i, X906:$i, X907:$i, X908:$i, X909:$i, X910:$i > $o, X911:$i, X912:$i, X913:$i > $o, X914:$i > $o, X917:$i, X918:$i, X919:$i, X920:$i, X921:$i, X922:$i, X923:$i, X924:$i, X925:$i > $o, X926:$i, X927:$i, X928:$i > $o, X929:$i > $o, X932:$i, X933:$i, X934:$i > $o, X935:$i > $o, X938:$i, X939:$i, X941:$i, X942:$i, X943:$i, X944:$i, X945:$i, X946:$i, X948:$i, X949:$i, X950:$i, X951:$i, X952:$i, X953:$i, X954:$i, X955:$i, X956:$i, X957:$i, X958:$i, X959:$i, X960:$i, X961:$i, X962:$i, X963:$i, X964:$i, X965:$i, X966:$i, X967:$i, X968:$i, X969:$i, X970:$i, X971:$i, X972:$i, X973:$i, X974:$i, X975:$i, X976:$i, X977:$i, X978:$i, X979:$i, X980:$i, X981:$i, X982:$i, X983:$i, X984:$i, X985:$i > $o, X986:$i, X987:$i > $o, X988:$i, X989:$i, X990:$i, X991:$i, X992:$i, X993:$i, X994:$i, X995:$i, X996:$i, X997:$i, X998:$i, X999:$o, X1000:$i, X1001:$i, X1002:$i, X1003:$i, X1004:$i, X1005:$i, X1006:$i, X1007:$i, X1008:$i, X1009:$i, X1010:$i, X1011:$i, X1012:$i, X1013:$i, X1014:$i, X1015:$i, X1016:$i, X1017:$i, X1018:$i, X1019:$i, X1020:$i, X1021:$i, X1022:$i, X1023:$i, X1024:$i, X1025:$i, X1026:$i, X1028:$i, X1029:$i, X1030:$i, X1031:$i, X1032:$i, X1033:$i, X1034:$i, X1035:$i, X1036:$i, X1037:$i, X1038:$i, X1039:$i, X1040:$i, X1041:$i, X1042:$i, X1043:$i, X1044:$i, X1045:$i, X1046:$i, X1047:$i, X1048:$i, X1049:$i, X1050:$i, X1051:$i, X1052:$i, X1053:$i, X1054:$i, X1055:$i, X1056:$i, X1057:$i, X1058:$i, X1059:$i, X1060:$i, X1061:$i, X1062:$i, X1063:$i, X1064:$i, X1065:$i, X1066:$i, X1067:$o, X1068:$i, X1069:$i, X1070:$i, X1071:$i, X1072:$i, X1073:$i, X1074:$i, X1075:$i, X1076:$i, X1077:$i, X1078:$i, X1079:$i, X1080:$i, X1081:$i, X1082:$i, X1083:$i]:((((~(in @ (esk1_2 @ X737 @ X738) @ X737)|~(in @ (esk1_2 @ X737 @ X738) @ X738)|((X737)=(X738)))&((in @ (esk1_2 @ X737 @ X738) @ X737)|(in @ (esk1_2 @ X737 @ X738) @ X738)|((X737)=(X738))))&(~(in @ X740 @ emptyset)&(((~(in @ X743 @ (setadjoin @ X741 @ X742))|(((X743)=(X741))|(in @ X743 @ X742)))&((((X743)!=(X741))|(in @ X743 @ (setadjoin @ X741 @ X742)))&(~(in @ X743 @ X742)|(in @ X743 @ (setadjoin @ X741 @ X742)))))&(((~(in @ X745 @ (powerset @ X744))|(~(in @ X746 @ X745)|(in @ X746 @ X744)))&(((in @ (esk2_2 @ X747 @ X748) @ X748)|(in @ X748 @ (powerset @ X747)))&(~(in @ (esk2_2 @ X747 @ X748) @ X747)|(in @ X748 @ (powerset @ X747)))))&(((((in @ X751 @ (esk3_2 @ X750 @ X751))|~(in @ X751 @ (setunion @ X750)))&((in @ (esk3_2 @ X750 @ X751) @ X750)|~(in @ X751 @ (setunion @ X750))))&(~(in @ X754 @ X755)|~(in @ X755 @ X753)|(in @ X754 @ (setunion @ X753))))&((in @ emptyset @ omega)&((~(in @ X756 @ omega)|(in @ (setadjoin @ X756 @ X756) @ omega))&(((((in @ (esk4_1 @ X757) @ omega)|~(in @ emptyset @ X757)|(~(in @ X759 @ omega)|(in @ X759 @ X757)))&((in @ (esk4_1 @ X757) @ X757)|~(in @ emptyset @ X757)|(~(in @ X759 @ omega)|(in @ X759 @ X757))))&(~(in @ (setadjoin @ (esk4_1 @ X757) @ (esk4_1 @ X757)) @ X757)|~(in @ emptyset @ X757)|(~(in @ X759 @ omega)|(in @ X759 @ X757))))&((((((in @ (esk7_3 @ X760 @ X761 @ X764) @ X761)|~(in @ X764 @ (esk6_2 @ X760 @ X761))|(in @ (esk5_2 @ X760 @ X761) @ X761))&((X760 @ (esk7_3 @ X760 @ X761 @ X764) @ X764)|~(in @ X764 @ (esk6_2 @ X760 @ X761))|(in @ (esk5_2 @ X760 @ X761) @ X761)))&(~(in @ X767 @ X761)|~(X760 @ X767 @ X766)|(in @ X766 @ (esk6_2 @ X760 @ X761))|(in @ (esk5_2 @ X760 @ X761) @ X761)))&((((in @ (esk7_3 @ X760 @ X761 @ X764) @ X761)|~(in @ X764 @ (esk6_2 @ X760 @ X761))|~(exu @ (X760 @ (esk5_2 @ X760 @ X761))))&((X760 @ (esk7_3 @ X760 @ X761 @ X764) @ X764)|~(in @ X764 @ (esk6_2 @ X760 @ X761))|~(exu @ (X760 @ (esk5_2 @ X760 @ X761)))))&(~(in @ X767 @ X761)|~(X760 @ X767 @ X766)|(in @ X766 @ (esk6_2 @ X760 @ X761))|~(exu @ (X760 @ (esk5_2 @ X760 @ X761))))))&((((in @ (esk8_1 @ X768) @ X768)|~(in @ X769 @ X768))&(~(in @ X771 @ (esk8_1 @ X768))|~(in @ X771 @ X768)|~(in @ X769 @ X768)))&((epred1_0)&((~(exu @ X772)|(X772 @ (descr @ X772)))&((~(in @ X775 @ X773)|(~(X774 @ X775)|(in @ X775 @ (dsetconstr @ X773 @ X774))))&((~(in @ X778 @ (dsetconstr @ X776 @ X777))|(in @ X778 @ X776))&((~(in @ X781 @ (dsetconstr @ X779 @ X780))|(X780 @ X781))&((((X782 @ (esk9_1 @ X782))|~(exu @ X782))&(~(X782 @ X784)|((esk9_1 @ X782)=(X784))|~(exu @ X782)))&((~(in @ X786 @ (prop2set @ ((X785))))|(X785))&((~(in @ X787 @ emptyset)|(X788))&((~(in @ X789 @ emptyset)|~($true))&(~(in @ X790 @ emptyset)&((~(exu @ X791)|(X791 @ (esk10_1 @ X791)))&(((((in @ (esk12_2 @ X793 @ X794) @ X794)|((X793)=(X794))|(in @ (esk11_2 @ X793 @ X794) @ X793))&(~(in @ (esk12_2 @ X793 @ X794) @ X793)|((X793)=(X794))|(in @ (esk11_2 @ X793 @ X794) @ X793)))&(((in @ (esk12_2 @ X793 @ X794) @ X794)|((X793)=(X794))|~(in @ (esk11_2 @ X793 @ X794) @ X794))&(~(in @ (esk12_2 @ X793 @ X794) @ X793)|((X793)=(X794))|~(in @ (esk11_2 @ X793 @ X794) @ X794))))&(((in @ (esk13_1 @ X797) @ X797)|((X797)=(emptyset)))&(((in @ (esk14_1 @ X799) @ X799)|((X799)=(emptyset)))&(((~(in @ X803 @ (dsetconstr @ X801 @ X802))|(X802 @ X803)|~(in @ X803 @ X801))&(~(X802 @ X803)|(in @ X803 @ (dsetconstr @ X801 @ X802))|~(in @ X803 @ X801)))&((~(nonempty @ X804)|(in @ (esk15_1 @ X804) @ X804))&((~(in @ X808 @ X806)|(~(X807 @ X808)|(nonempty @ (dsetconstr @ X806 @ X807))))&((~(in @ X810 @ X809)|(nonempty @ X809))&((in @ X811 @ (setadjoin @ X811 @ X812))&((in @ emptyset @ (setadjoin @ emptyset @ emptyset))&((~(in @ X815 @ X814)|(in @ X815 @ (setadjoin @ X813 @ X814)))&(((((in @ X818 @ X817)|(X819)|((X818)=(X816))|~(in @ X818 @ (setadjoin @ X816 @ X817)))&(~(X819)|(X819)|((X818)=(X816))|~(in @ X818 @ (setadjoin @ X816 @ X817))))&(((in @ X818 @ X817)|(X819)|~(X819)|~(in @ X818 @ (setadjoin @ X816 @ X817)))&(~(X819)|(X819)|~(X819)|~(in @ X818 @ (setadjoin @ X816 @ X817)))))&((~(in @ X822 @ (setadjoin @ X820 @ X821))|(((X822)=(X820))|(in @ X822 @ X821)))&(((dsetconstr @ X823 @ (^[Z0:$i]:($true)))=(X823))&((((in @ (esk16_2 @ X824 @ X825) @ X825)|(in @ X825 @ (powerset @ X824)))&(~(in @ (esk16_2 @ X824 @ X825) @ X824)|(in @ X825 @ (powerset @ X824))))&((in @ emptyset @ (powerset @ X827))&((in @ emptyset @ (powerset @ X828))&((~(in @ X830 @ (powerset @ X829))|(~(in @ X831 @ X830)|(in @ X831 @ X829)))&((~(in @ X833 @ X834)|(~(in @ X834 @ X832)|(in @ X833 @ (setunion @ X832))))&((((in @ X836 @ (esk17_3 @ X835 @ X836 @ X837))|(X837)|~(in @ X836 @ (setunion @ X835)))&(((in @ (esk17_3 @ X835 @ X836 @ X837) @ X835)|(X837)|~(in @ X836 @ (setunion @ X835)))&(~(X837)|(X837)|~(in @ X836 @ (setunion @ X835)))))&((~(in @ X840 @ X839)|(in @ X840 @ (powerset @ (setunion @ X839))))&(((~(X841 @ X843)|((X843)=(esk18_1 @ X841))|~(exu @ X841))&(((X844)!=(esk18_1 @ X841))|(X841 @ X844)|~(exu @ X841)))&((((in @ (esk19_1 @ X845) @ X845)|~(nonempty @ X845))&(($true)|~(nonempty @ X845)))&((~(in @ X847 @ (setadjoin @ X848 @ emptyset))|((X847)=(X848)))&((((X849)=(X850))|~(in @ X850 @ (setadjoin @ X849 @ emptyset)))&((((X851)!=(X852))|(in @ X851 @ (setadjoin @ X852 @ emptyset)))&((~(in @ X853 @ (setadjoin @ X854 @ emptyset))|(in @ X854 @ (setadjoin @ X853 @ emptyset)))&((~(in @ X857 @ (setadjoin @ X855 @ (setadjoin @ X856 @ emptyset)))|(((X857)=(X855))|((X857)=(X856))))&((in @ X858 @ (setadjoin @ X858 @ (setadjoin @ X859 @ emptyset)))&((in @ X861 @ (setadjoin @ X860 @ (setadjoin @ X861 @ emptyset)))&((~(in @ X864 @ X862)|~(X863 @ X864)|(((dsetconstr @ X862 @ X863)!=(emptyset))|~($true)))&((~(in @ X866 @ emptyset)|(X865 @ X866))&((((in @ (esk20_2 @ X867 @ X868) @ X867)|(~(in @ X869 @ X867)|(X868 @ X869)))&(~(X868 @ (esk20_2 @ X867 @ X868))|(~(in @ X869 @ X867)|(X868 @ X869))))&((((in @ (esk21_2 @ X871 @ X872) @ X871)|(~(in @ X874 @ X871)|~(X872 @ X874)))&((X872 @ (esk21_2 @ X871 @ X872))|(~(in @ X874 @ X871)|~(X872 @ X874))))&((((in @ (esk22_2 @ X875 @ X876) @ X875)|(~(in @ X878 @ X875)|~(X876 @ X878)))&((X876 @ (esk22_2 @ X875 @ X876))|(~(in @ X878 @ X875)|~(X876 @ X878))))&((((in @ (esk23_2 @ X879 @ X880) @ X879)|(~(in @ X881 @ X879)|(X880 @ X881)))&(~(X880 @ (esk23_2 @ X879 @ X880))|(~(in @ X881 @ X879)|(X880 @ X881))))&((~(X883)|(in @ emptyset @ (prop2set @ ((X883)))))&((prop2set2propI)&((((in @ (esk24_2 @ X884 @ X885) @ X884)|(~(in @ X887 @ X884)|~(X885 @ X887)))&((X885 @ (esk24_2 @ X884 @ X885))|(~(in @ X887 @ X884)|~(X885 @ X887))))&((((in @ (esk25_2 @ X888 @ X889) @ X888)|(~(in @ X890 @ X888)|(X889 @ X890)))&(~(X889 @ (esk25_2 @ X888 @ X889))|(~(in @ X890 @ X888)|(X889 @ X890))))&((((X892 @ (esk26_2 @ X892 @ X893))|~(X892 @ X893)|(exu @ X892))&(((X893)!=(esk26_2 @ X892 @ X893))|~(X892 @ X893)|(exu @ X892)))&((((X895 @ (esk27_1 @ X895))|(exu @ X895)|~(X895 @ X896))&(((X895 @ (esk28_1 @ X895))|(exu @ X895)|~(X895 @ X896))&(((esk27_1 @ X895)!=(esk28_1 @ X895))|(exu @ X895)|~(X895 @ X896))))&(((~(X899 @ (esk29_2 @ X899 @ X900))|((esk29_2 @ X899 @ X900)!=(X900))|(exu @ X899))&((X899 @ (esk29_2 @ X899 @ X900))|((esk29_2 @ X899 @ X900)=(X900))|(exu @ X899)))&((((X902)!=(X903))|(((X904)!=(X905))|(~(in @ X904 @ X902)|(in @ X905 @ X903))))&(((~(in @ X908 @ X906)|(in @ X909 @ X907)|((X908)!=(X909))|((X906)!=(X907)))&(~(in @ X909 @ X907)|(in @ X908 @ X906)|((X908)!=(X909))|((X906)!=(X907))))&((~(exu @ X910)|(~(X910 @ X911)|(~(X910 @ X912)|((X911)=(X912)))))&((((~(exu @ X913)|(exu @ X914)|((esk30_2 @ X913 @ X914)=(esk31_2 @ X913 @ X914)))&(~(exu @ X914)|(exu @ X913)|((esk30_2 @ X913 @ X914)=(esk31_2 @ X913 @ X914))))&(((~(exu @ X913)|(exu @ X914)|(~(X913 @ (esk30_2 @ X913 @ X914))|~(X914 @ (esk31_2 @ X913 @ X914))))&(~(exu @ X914)|(exu @ X913)|(~(X913 @ (esk30_2 @ X913 @ X914))|~(X914 @ (esk31_2 @ X913 @ X914)))))&((~(exu @ X913)|(exu @ X914)|((X913 @ (esk30_2 @ X913 @ X914))|(X914 @ (esk31_2 @ X913 @ X914))))&(~(exu @ X914)|(exu @ X913)|((X913 @ (esk30_2 @ X913 @ X914))|(X914 @ (esk31_2 @ X913 @ X914)))))))&(((emptyset)=(emptyset))&((((X917)!=(X918))|(((X919)!=(X920))|((setadjoin @ X917 @ X919)=(setadjoin @ X918 @ X920))))&((((X921)!=(X922))|((powerset @ X921)=(powerset @ X922)))&((((X923)!=(X924))|((setunion @ X923)=(setunion @ X924)))&(((omega)=(omega))&((~(exu @ X925)|(~(X925 @ X926)|(~(X925 @ X927)|((X926)=(X927)))))&(((((esk32_2 @ X928 @ X929)=(esk33_2 @ X928 @ X929))|(~(exu @ X928)|(~(exu @ X929)|((descr @ X928)=(descr @ X929)))))&((~(X928 @ (esk32_2 @ X928 @ X929))|~(X929 @ (esk33_2 @ X928 @ X929))|(~(exu @ X928)|(~(exu @ X929)|((descr @ X928)=(descr @ X929)))))&((X928 @ (esk32_2 @ X928 @ X929))|(X929 @ (esk33_2 @ X928 @ X929))|(~(exu @ X928)|(~(exu @ X929)|((descr @ X928)=(descr @ X929)))))))&((((in @ (esk34_4 @ X932 @ X933 @ X934 @ X935) @ X932)|((dsetconstr @ X932 @ X934)=(dsetconstr @ X933 @ X935))|((X932)!=(X933)))&(((in @ (esk35_4 @ X932 @ X933 @ X934 @ X935) @ X933)|((dsetconstr @ X932 @ X934)=(dsetconstr @ X933 @ X935))|((X932)!=(X933)))&((((esk34_4 @ X932 @ X933 @ X934 @ X935)=(esk35_4 @ X932 @ X933 @ X934 @ X935))|((dsetconstr @ X932 @ X934)=(dsetconstr @ X933 @ X935))|((X932)!=(X933)))&((~(X934 @ (esk34_4 @ X932 @ X933 @ X934 @ X935))|~(X935 @ (esk35_4 @ X932 @ X933 @ X934 @ X935))|((dsetconstr @ X932 @ X934)=(dsetconstr @ X933 @ X935))|((X932)!=(X933)))&((X934 @ (esk34_4 @ X932 @ X933 @ X934 @ X935))|(X935 @ (esk35_4 @ X932 @ X933 @ X934 @ X935))|((dsetconstr @ X932 @ X934)=(dsetconstr @ X933 @ X935))|((X932)!=(X933)))))))&((((in @ (esk36_2 @ X938 @ X939) @ X938)|(subset @ X938 @ X939))&(~(in @ (esk36_2 @ X938 @ X939) @ X939)|(subset @ X938 @ X939)))&((((X941)!=(X942))|(subset @ X942 @ X941))&((((X943)!=(X944))|(subset @ X943 @ X944))&((((in @ (esk37_2 @ X945 @ X946) @ X945)|(subset @ X945 @ X946))&(~(in @ (esk37_2 @ X945 @ X946) @ X946)|(subset @ X945 @ X946)))&((subset @ emptyset @ X948)&((~(subset @ X949 @ X950)|(~(in @ X951 @ X949)|(in @ X951 @ X950)))&((~(subset @ X952 @ X953)|((in @ X954 @ X953)|~(in @ X954 @ X952)))&((~(in @ X957 @ X955)|((in @ X957 @ X956)|~(subset @ X955 @ X956)))&(((subset @ X958 @ X959)|((X958)!=(X959)))&((~(in @ X962 @ X960)|((in @ X962 @ X961)|((X960)!=(X961))))&((subset @ X963 @ X963)&((~(subset @ X964 @ X965)|(~(subset @ X965 @ X966)|(subset @ X964 @ X966)))&((subset @ X968 @ (setadjoin @ X967 @ X968))&((~(subset @ X969 @ X971)|(subset @ X969 @ (setadjoin @ X970 @ X971)))&((~(subset @ X972 @ X973)|(in @ X972 @ (powerset @ X973)))&((~(subset @ X974 @ X975)|(~(subset @ X975 @ X974)|((X974)=(X975))))&((~(subset @ X976 @ emptyset)|((X976)=(emptyset)))&((~(subset @ X978 @ X977)|(in @ X978 @ (powerset @ X977)))&((~(in @ X980 @ (powerset @ X979))|(subset @ X980 @ X979))&((in @ X981 @ (powerset @ X981))&((~(subset @ X982 @ X983)|(subset @ (powerset @ X982) @ (powerset @ X983)))&((in @ (dsetconstr @ X984 @ X985) @ (powerset @ X984))&((subset @ (dsetconstr @ X986 @ X987) @ X986)&((~(in @ X990 @ X988)|(in @ X990 @ (binunion @ X988 @ X989)))&((in @ X992 @ (setadjoin @ X991 @ (setadjoin @ X992 @ emptyset)))&((~(in @ X995 @ X994)|(in @ X995 @ (binunion @ X993 @ X994)))&(((((in @ X998 @ X997)|(X999)|(in @ X998 @ X996)|~(in @ X998 @ (binunion @ X996 @ X997)))&(~(X999)|(X999)|(in @ X998 @ X996)|~(in @ X998 @ (binunion @ X996 @ X997))))&(((in @ X998 @ X997)|(X999)|~(X999)|~(in @ X998 @ (binunion @ X996 @ X997)))&(~(X999)|(X999)|~(X999)|~(in @ X998 @ (binunion @ X996 @ X997)))))&((~(in @ X1002 @ (binunion @ X1000 @ X1001))|((in @ X1002 @ X1000)|(in @ X1002 @ X1001)))&((subset @ X1003 @ (binunion @ X1003 @ X1004))&((subset @ X1006 @ (binunion @ X1005 @ X1006))&((~(in @ X1009 @ X1007)|(~(in @ X1009 @ X1008)|(in @ X1009 @ (binintersect @ X1007 @ X1008))))&((~(subset @ X1012 @ X1010)|(~(subset @ X1012 @ X1011)|(subset @ X1012 @ (binintersect @ X1010 @ X1011))))&((~(in @ X1015 @ (binintersect @ X1013 @ X1014))|(in @ X1015 @ X1013))&((subset @ (binintersect @ X1016 @ X1017) @ X1016)&((~(subset @ X1018 @ X1019)|((binintersect @ X1018 @ X1019)=(X1018)))&((((binintersect @ X1020 @ X1021)!=(X1021))|(subset @ X1021 @ X1020))&((~(in @ X1024 @ (binintersect @ X1022 @ X1023))|(in @ X1024 @ X1023))&((((in @ (esk38_2 @ X1025 @ X1026) @ X1025)|((binintersect @ X1025 @ X1026)=(emptyset)))&((in @ (esk38_2 @ X1025 @ X1026) @ X1026)|((binintersect @ X1025 @ X1026)=(emptyset))))&((subset @ (binintersect @ X1028 @ X1029) @ X1029)&((~(subset @ X1031 @ X1030)|((binintersect @ X1030 @ X1031)=(X1031)))&((((binintersect @ X1032 @ X1033)!=(X1032))|(subset @ X1032 @ X1033))&(((binintersect @ X1034 @ (binunion @ X1035 @ X1036))=(binunion @ (binintersect @ X1034 @ X1035) @ (binintersect @ X1034 @ X1036)))&((~(in @ X1039 @ X1037)|((in @ X1039 @ X1038)|(in @ X1039 @ (setminus @ X1037 @ X1038))))&((~(in @ X1042 @ (setminus @ X1040 @ X1041))|(in @ X1042 @ X1040))&((~(in @ X1045 @ (setminus @ X1043 @ X1044))|~(in @ X1045 @ X1044))&((~(subset @ X1046 @ X1047)|((setminus @ X1046 @ X1047)=(emptyset)))&(((in @ X1050 @ (setminus @ X1048 @ X1049))|(~(in @ X1050 @ X1048)|(in @ X1050 @ X1049)))&(((in @ X1053 @ (setminus @ X1051 @ X1052))|((in @ X1053 @ X1052)|~(in @ X1053 @ X1051)))&(((in @ X1056 @ X1054)|~(in @ X1056 @ (setminus @ X1054 @ X1055)))&((~(in @ X1059 @ X1058)|~(in @ X1059 @ (setminus @ X1057 @ X1058)))&((subset @ (setminus @ X1060 @ X1061) @ X1060)&((((setminus @ X1062 @ X1063)!=(emptyset))|(subset @ X1062 @ X1063))&((((~(in @ X1066 @ X1064)|(X1067)|(in @ X1066 @ X1064)|~(in @ X1066 @ (symdiff @ X1064 @ X1065)))&(((in @ X1066 @ X1065)|(X1067)|(in @ X1066 @ X1064)|~(in @ X1066 @ (symdiff @ X1064 @ X1065)))&(~(X1067)|(X1067)|(in @ X1066 @ X1064)|~(in @ X1066 @ (symdiff @ X1064 @ X1065)))))&(((~(in @ X1066 @ X1064)|(X1067)|~(in @ X1066 @ X1065)|~(in @ X1066 @ (symdiff @ X1064 @ X1065)))&(((in @ X1066 @ X1065)|(X1067)|~(in @ X1066 @ X1065)|~(in @ X1066 @ (symdiff @ X1064 @ X1065)))&(~(X1067)|(X1067)|~(in @ X1066 @ X1065)|~(in @ X1066 @ (symdiff @ X1064 @ X1065)))))&((~(in @ X1066 @ X1064)|(X1067)|~(X1067)|~(in @ X1066 @ (symdiff @ X1064 @ X1065)))&(((in @ X1066 @ X1065)|(X1067)|~(X1067)|~(in @ X1066 @ (symdiff @ X1064 @ X1065)))&(~(X1067)|(X1067)|~(X1067)|~(in @ X1066 @ (symdiff @ X1064 @ X1065)))))))&((~(in @ X1070 @ X1068)|((in @ X1070 @ X1069)|(in @ X1070 @ (symdiff @ X1068 @ X1069))))&(((in @ X1073 @ X1071)|(~(in @ X1073 @ X1072)|(in @ X1073 @ (symdiff @ X1071 @ X1072))))&((~(in @ X1076 @ X1074)|(~(in @ X1076 @ X1075)|~(in @ X1076 @ (symdiff @ X1074 @ X1075))))&(((in @ X1079 @ X1077)|((in @ X1079 @ X1078)|~(in @ X1079 @ (symdiff @ X1077 @ X1078))))&((in @ X1081 @ (setadjoin @ X1080 @ (setadjoin @ X1081 @ emptyset)))&((in @ X1082 @ (setunion @ (setadjoin @ (setadjoin @ X1082 @ emptyset) @ (setadjoin @ (setadjoin @ X1082 @ (setadjoin @ X1083 @ emptyset)) @ emptyset))))&~(in @ esk40_0 @ (setunion @ (setadjoin @ (setadjoin @ esk39_0 @ emptyset) @ (setadjoin @ (setadjoin @ esk39_0 @ (setadjoin @ esk40_0 @ emptyset)) @ emptyset))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))), inference(distribute,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_158])])])])])])])).
% 3.16/0.79 thf(c_0_160, negated_conjecture, ![X2:$i, X3:$i, X4:$i]:(((in @ X2 @ (setunion @ X4))|~((in @ X2 @ X3))|~((in @ X3 @ X4)))), inference(split_conjunct,[status(thm)],[c_0_159])).
% 3.16/0.79 thf(c_0_161, negated_conjecture, ![X3:$i, X2:$i]:((in @ X2 @ (setadjoin @ X3 @ (setadjoin @ X2 @ emptyset)))), inference(split_conjunct,[status(thm)],[c_0_159])).
% 3.16/0.79 thf(c_0_162, negated_conjecture, ~((in @ esk40_0 @ (setunion @ (setadjoin @ (setadjoin @ esk39_0 @ emptyset) @ (setadjoin @ (setadjoin @ esk39_0 @ (setadjoin @ esk40_0 @ emptyset)) @ emptyset))))), inference(split_conjunct,[status(thm)],[c_0_159])).
% 3.16/0.79 thf(c_0_163, negated_conjecture, ![X2:$i, X3:$i, X4:$i]:(((in @ X2 @ (setunion @ (setadjoin @ X3 @ (setadjoin @ X4 @ emptyset))))|~((in @ X2 @ X4)))), inference(spm,[status(thm)],[c_0_160, c_0_161])).
% 3.16/0.79 thf(c_0_164, negated_conjecture, ($false), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_162, c_0_163]), c_0_161])]), ['proof']).
% 3.16/0.79 % SZS output end CNFRefutation
% 3.16/0.79 % Parsed axioms : 293
% 3.16/0.79 % Removed by relevancy pruning/SinE : 159
% 3.16/0.79 % Initial clauses : 214
% 3.16/0.79 % Removed in clause preprocessing : 25
% 3.16/0.79 % Initial clauses in saturation : 189
% 3.16/0.79 % Processed clauses : 6270
% 3.16/0.79 % ...of these trivial : 124
% 3.16/0.79 % ...subsumed : 4907
% 3.16/0.79 % ...remaining for further processing : 1239
% 3.16/0.79 % Other redundant clauses eliminated : 75
% 3.16/0.79 % Clauses deleted for lack of memory : 0
% 3.16/0.79 % Backward-subsumed : 106
% 3.16/0.79 % Backward-rewritten : 11
% 3.16/0.79 % Generated clauses : 41888
% 3.16/0.79 % ...of the previous two non-redundant : 37215
% 3.16/0.79 % ...aggressively subsumed : 0
% 3.16/0.79 % Contextual simplify-reflections : 5
% 3.16/0.79 % Paramodulations : 41805
% 3.16/0.79 % Factorizations : 8
% 3.16/0.79 % NegExts : 0
% 3.16/0.79 % Equation resolutions : 75
% 3.16/0.79 % Disequality decompositions : 0
% 3.16/0.79 % Total rewrite steps : 5564
% 3.16/0.79 % ...of those cached : 5293
% 3.16/0.79 % Propositional unsat checks : 0
% 3.16/0.79 % Propositional check models : 0
% 3.16/0.79 % Propositional check unsatisfiable : 0
% 3.16/0.79 % Propositional clauses : 0
% 3.16/0.79 % Propositional clauses after purity: 0
% 3.16/0.79 % Propositional unsat core size : 0
% 3.16/0.79 % Propositional preprocessing time : 0.000
% 3.16/0.79 % Propositional encoding time : 0.000
% 3.16/0.79 % Propositional solver time : 0.000
% 3.16/0.79 % Success case prop preproc time : 0.000
% 3.16/0.79 % Success case prop encoding time : 0.000
% 3.16/0.79 % Success case prop solver time : 0.000
% 3.16/0.79 % Current number of processed clauses : 1111
% 3.16/0.79 % Positive orientable unit clauses : 129
% 3.16/0.79 % Positive unorientable unit clauses: 0
% 3.16/0.79 % Negative unit clauses : 43
% 3.16/0.79 % Non-unit-clauses : 939
% 3.16/0.79 % Current number of unprocessed clauses: 30401
% 3.16/0.79 % ...number of literals in the above : 88755
% 3.16/0.79 % Current number of archived formulas : 0
% 3.16/0.79 % Current number of archived clauses : 117
% 3.16/0.79 % Clause-clause subsumption calls (NU) : 81222
% 3.16/0.79 % Rec. Clause-clause subsumption calls : 71303
% 3.16/0.79 % Non-unit clause-clause subsumptions : 4105
% 3.16/0.79 % Unit Clause-clause subsumption calls : 1436
% 3.16/0.79 % Rewrite failures with RHS unbound : 0
% 3.16/0.79 % BW rewrite match attempts : 215
% 3.16/0.79 % BW rewrite match successes : 6
% 3.16/0.79 % Condensation attempts : 0
% 3.16/0.79 % Condensation successes : 0
% 3.16/0.79 % Termbank termtop insertions : 472696
% 3.16/0.79 % Search garbage collected termcells : 11797
% 3.16/0.79
% 3.16/0.79 % -------------------------------------------------
% 3.16/0.79 % User time : 0.450 s
% 3.16/0.79 % System time : 0.024 s
% 3.16/0.79 % Total time : 0.474 s
% 3.16/0.79 % Maximum resident set size: 6484 pages
% 3.16/0.79
% 3.16/0.79 % -------------------------------------------------
% 3.16/0.79 % User time : 0.551 s
% 3.16/0.79 % System time : 0.074 s
% 3.16/0.79 % Total time : 0.625 s
% 3.16/0.79 % Maximum resident set size: 5120 pages
% 3.16/0.79 % E exiting
%------------------------------------------------------------------------------